blob: 3c544ee5fe6e80ca0ab0c02551217788fe956c99 [file] [log] [blame]
// Copyright 2020 The Wuffs Authors.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// https://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// --------
// Filter 1: Sub.
pri func decoder.filter_1!(curr: slice base.u8),
choosy,
{
var filter_distance : base.u64[..= 8]
var fa : base.u8
var i_start : base.u64
var i : base.u64
filter_distance = this.filter_distance as base.u64
i_start = 0
while i_start < filter_distance {
assert i_start < 8 via "a < b: a < c; c <= b"(c: filter_distance)
fa = 0
i = i_start
while i < args.curr.length(),
inv i_start < 8,
{
args.curr[i] = args.curr[i] ~mod+ fa
fa = args.curr[i]
i ~mod+= filter_distance
} endwhile
i_start += 1
} endwhile
}
pri func decoder.filter_1_distance_3_fallback!(curr: slice base.u8) {
var curr : slice base.u8
var fa0 : base.u8
var fa1 : base.u8
var fa2 : base.u8
iterate (curr = args.curr)(length: 3, advance: 3, unroll: 2) {
fa0 = fa0 ~mod+ curr[0]
curr[0] = fa0
fa1 = fa1 ~mod+ curr[1]
curr[1] = fa1
fa2 = fa2 ~mod+ curr[2]
curr[2] = fa2
}
}
pri func decoder.filter_1_distance_4_fallback!(curr: slice base.u8) {
var curr : slice base.u8
var fa0 : base.u8
var fa1 : base.u8
var fa2 : base.u8
var fa3 : base.u8
iterate (curr = args.curr)(length: 4, advance: 4, unroll: 1) {
fa0 = fa0 ~mod+ curr[0]
curr[0] = fa0
fa1 = fa1 ~mod+ curr[1]
curr[1] = fa1
fa2 = fa2 ~mod+ curr[2]
curr[2] = fa2
fa3 = fa3 ~mod+ curr[3]
curr[3] = fa3
}
}
// Filter 2: Up.
pri func decoder.filter_2!(curr: slice base.u8, prev: slice base.u8) {
var n : base.u64
var i : base.u64
n = args.curr.length().min(a: args.prev.length())
i = 0
while i < n,
inv n <= args.curr.length(),
inv n <= args.prev.length(),
{
assert i < 0xFFFF_FFFF_FFFF_FFFF via "a < b: a < c; c <= b"(c: n)
assert i < args.curr.length() via "a < b: a < c; c <= b"(c: n)
assert i < args.prev.length() via "a < b: a < c; c <= b"(c: n)
args.curr[i] = args.curr[i] ~mod+ (args.prev[i])
i += 1
} endwhile
}
// Filter 3: Average.
pri func decoder.filter_3!(curr: slice base.u8, prev: slice base.u8),
choosy,
{
var filter_distance : base.u64[..= 8]
var n : base.u64
var i : base.u64
filter_distance = this.filter_distance as base.u64
if args.prev.length() == 0 {
i = filter_distance
assert i >= filter_distance via "a >= b: a == b"()
while i < args.curr.length(),
inv i >= filter_distance,
{
assert i < 0xFFFF_FFFF_FFFF_FFFF via "a < b: a < c; c <= b"(c: args.curr.length())
assert (i - filter_distance) < args.curr.length() via "(a - b) < c: a < c; 0 <= b"()
args.curr[i] = args.curr[i] ~mod+ (args.curr[i - filter_distance] / 2)
i += 1
assert i >= filter_distance via "a >= b: a >= (b + c); 0 <= c"(c: 1)
} endwhile
} else {
n = args.curr.length().min(a: args.prev.length())
i = 0
while (i < n) and (i < filter_distance),
inv n <= args.curr.length(),
inv n <= args.prev.length(),
{
assert i < 0xFFFF_FFFF_FFFF_FFFF via "a < b: a < c; c <= b"(c: n)
assert i < args.curr.length() via "a < b: a < c; c <= b"(c: n)
assert i < args.prev.length() via "a < b: a < c; c <= b"(c: n)
args.curr[i] = args.curr[i] ~mod+ (args.prev[i] / 2)
i += 1
} endwhile
i = filter_distance
assert i >= filter_distance via "a >= b: a == b"()
while i < n,
inv i >= filter_distance,
inv n <= args.curr.length(),
inv n <= args.prev.length(),
{
assert i < 0xFFFF_FFFF_FFFF_FFFF via "a < b: a < c; c <= b"(c: n)
assert i < args.curr.length() via "a < b: a < c; c <= b"(c: n)
assert i < args.prev.length() via "a < b: a < c; c <= b"(c: n)
assert (i - filter_distance) < args.curr.length() via "(a - b) < c: a < c; 0 <= b"()
args.curr[i] = args.curr[i] ~mod+ (((
(args.curr[i - filter_distance] as base.u32) +
(args.prev[i] as base.u32)) / 2) as base.u8)
i += 1
assert i >= filter_distance via "a >= b: a >= (b + c); 0 <= c"(c: 1)
} endwhile
}
}
pri func decoder.filter_3_distance_3_fallback!(curr: slice base.u8, prev: slice base.u8) {
var curr : slice base.u8
var prev : slice base.u8
var fa0 : base.u8
var fa1 : base.u8
var fa2 : base.u8
if args.prev.length() == 0 {
iterate (curr = args.curr)(length: 3, advance: 3, unroll: 2) {
fa0 = (fa0 / 2) ~mod+ curr[0]
curr[0] = fa0
fa1 = (fa1 / 2) ~mod+ curr[1]
curr[1] = fa1
fa2 = (fa2 / 2) ~mod+ curr[2]
curr[2] = fa2
}
} else {
iterate (curr = args.curr, prev = args.prev)(length: 3, advance: 3, unroll: 2) {
fa0 = ((((fa0 as base.u32) + (prev[0] as base.u32)) / 2) as base.u8) ~mod+ curr[0]
curr[0] = fa0
fa1 = ((((fa1 as base.u32) + (prev[1] as base.u32)) / 2) as base.u8) ~mod+ curr[1]
curr[1] = fa1
fa2 = ((((fa2 as base.u32) + (prev[2] as base.u32)) / 2) as base.u8) ~mod+ curr[2]
curr[2] = fa2
}
}
}
pri func decoder.filter_3_distance_4_fallback!(curr: slice base.u8, prev: slice base.u8) {
var curr : slice base.u8
var prev : slice base.u8
var fa0 : base.u8
var fa1 : base.u8
var fa2 : base.u8
var fa3 : base.u8
if args.prev.length() == 0 {
iterate (curr = args.curr)(length: 4, advance: 4, unroll: 1) {
fa0 = (fa0 / 2) ~mod+ curr[0]
curr[0] = fa0
fa1 = (fa1 / 2) ~mod+ curr[1]
curr[1] = fa1
fa2 = (fa2 / 2) ~mod+ curr[2]
curr[2] = fa2
fa3 = (fa3 / 2) ~mod+ curr[3]
curr[3] = fa3
}
} else {
iterate (curr = args.curr, prev = args.prev)(length: 4, advance: 4, unroll: 1) {
fa0 = ((((fa0 as base.u32) + (prev[0] as base.u32)) / 2) as base.u8) ~mod+ curr[0]
curr[0] = fa0
fa1 = ((((fa1 as base.u32) + (prev[1] as base.u32)) / 2) as base.u8) ~mod+ curr[1]
curr[1] = fa1
fa2 = ((((fa2 as base.u32) + (prev[2] as base.u32)) / 2) as base.u8) ~mod+ curr[2]
curr[2] = fa2
fa3 = ((((fa3 as base.u32) + (prev[3] as base.u32)) / 2) as base.u8) ~mod+ curr[3]
curr[3] = fa3
}
}
}
// Filter 4: Paeth.
pri func decoder.filter_4!(curr: slice base.u8, prev: slice base.u8),
choosy,
{
var filter_distance : base.u64[..= 8]
var n : base.u64
var i : base.u64
var fa : base.u32
var fb : base.u32
var fc : base.u32
var pp : base.u32
var pa : base.u32
var pb : base.u32
var pc : base.u32
filter_distance = this.filter_distance as base.u64
n = args.curr.length().min(a: args.prev.length())
i = 0
while (i < n) and (i < filter_distance),
inv n <= args.curr.length(),
inv n <= args.prev.length(),
{
assert i < 0xFFFF_FFFF_FFFF_FFFF via "a < b: a < c; c <= b"(c: n)
assert i < args.curr.length() via "a < b: a < c; c <= b"(c: n)
assert i < args.prev.length() via "a < b: a < c; c <= b"(c: n)
args.curr[i] = args.curr[i] ~mod+ args.prev[i]
i += 1
} endwhile
i = filter_distance
assert i >= filter_distance via "a >= b: a == b"()
while i < n,
inv i >= filter_distance,
inv n <= args.curr.length(),
inv n <= args.prev.length(),
{
assert i < 0xFFFF_FFFF_FFFF_FFFF via "a < b: a < c; c <= b"(c: n)
assert i < args.curr.length() via "a < b: a < c; c <= b"(c: n)
assert i < args.prev.length() via "a < b: a < c; c <= b"(c: n)
assert (i - filter_distance) < args.curr.length() via "(a - b) < c: a < c; 0 <= b"()
assert (i - filter_distance) < args.prev.length() via "(a - b) < c: a < c; 0 <= b"()
fa = args.curr[i - filter_distance] as base.u32
fb = args.prev[i] as base.u32
fc = args.prev[i - filter_distance] as base.u32
pp = (fa ~mod+ fb) ~mod- fc
pa = pp ~mod- fa
if pa >= 0x8000_0000 {
pa = 0 ~mod- pa
}
pb = pp ~mod- fb
if pb >= 0x8000_0000 {
pb = 0 ~mod- pb
}
pc = pp ~mod- fc
if pc >= 0x8000_0000 {
pc = 0 ~mod- pc
}
if (pa <= pb) and (pa <= pc) {
// No-op.
} else if pb <= pc {
fa = fb
} else {
fa = fc
}
args.curr[i] = args.curr[i] ~mod+ ((fa & 0xFF) as base.u8)
i += 1
assert i >= filter_distance via "a >= b: a >= (b + c); 0 <= c"(c: 1)
} endwhile
}
pri func decoder.filter_4_distance_3_fallback!(curr: slice base.u8, prev: slice base.u8) {
var curr : slice base.u8
var prev : slice base.u8
var fa0 : base.u32
var fa1 : base.u32
var fa2 : base.u32
var fb0 : base.u32
var fb1 : base.u32
var fb2 : base.u32
var fc0 : base.u32
var fc1 : base.u32
var fc2 : base.u32
var pp0 : base.u32
var pp1 : base.u32
var pp2 : base.u32
var pa0 : base.u32
var pa1 : base.u32
var pa2 : base.u32
var pb0 : base.u32
var pb1 : base.u32
var pb2 : base.u32
var pc0 : base.u32
var pc1 : base.u32
var pc2 : base.u32
iterate (curr = args.curr, prev = args.prev)(length: 3, advance: 3, unroll: 1) {
fb0 = prev[0] as base.u32
pp0 = (fa0 ~mod+ fb0) ~mod- fc0
pa0 = pp0 ~mod- fa0
if pa0 >= 0x8000_0000 {
pa0 = 0 ~mod- pa0
}
pb0 = pp0 ~mod- fb0
if pb0 >= 0x8000_0000 {
pb0 = 0 ~mod- pb0
}
pc0 = pp0 ~mod- fc0
if pc0 >= 0x8000_0000 {
pc0 = 0 ~mod- pc0
}
if (pa0 <= pb0) and (pa0 <= pc0) {
// No-op.
} else if pb0 <= pc0 {
fa0 = fb0
} else {
fa0 = fc0
}
curr[0] = curr[0] ~mod+ ((fa0 & 0xFF) as base.u8)
fa0 = curr[0] as base.u32
fc0 = fb0
fb1 = prev[1] as base.u32
pp1 = (fa1 ~mod+ fb1) ~mod- fc1
pa1 = pp1 ~mod- fa1
if pa1 >= 0x8000_0000 {
pa1 = 0 ~mod- pa1
}
pb1 = pp1 ~mod- fb1
if pb1 >= 0x8000_0000 {
pb1 = 0 ~mod- pb1
}
pc1 = pp1 ~mod- fc1
if pc1 >= 0x8000_0000 {
pc1 = 0 ~mod- pc1
}
if (pa1 <= pb1) and (pa1 <= pc1) {
// No-op.
} else if pb1 <= pc1 {
fa1 = fb1
} else {
fa1 = fc1
}
curr[1] = curr[1] ~mod+ ((fa1 & 0xFF) as base.u8)
fa1 = curr[1] as base.u32
fc1 = fb1
fb2 = prev[2] as base.u32
pp2 = (fa2 ~mod+ fb2) ~mod- fc2
pa2 = pp2 ~mod- fa2
if pa2 >= 0x8000_0000 {
pa2 = 0 ~mod- pa2
}
pb2 = pp2 ~mod- fb2
if pb2 >= 0x8000_0000 {
pb2 = 0 ~mod- pb2
}
pc2 = pp2 ~mod- fc2
if pc2 >= 0x8000_0000 {
pc2 = 0 ~mod- pc2
}
if (pa2 <= pb2) and (pa2 <= pc2) {
// No-op.
} else if pb2 <= pc2 {
fa2 = fb2
} else {
fa2 = fc2
}
curr[2] = curr[2] ~mod+ ((fa2 & 0xFF) as base.u8)
fa2 = curr[2] as base.u32
fc2 = fb2
}
}
pri func decoder.filter_4_distance_4_fallback!(curr: slice base.u8, prev: slice base.u8) {
var curr : slice base.u8
var prev : slice base.u8
var fa0 : base.u32
var fa1 : base.u32
var fa2 : base.u32
var fa3 : base.u32
var fb0 : base.u32
var fb1 : base.u32
var fb2 : base.u32
var fb3 : base.u32
var fc0 : base.u32
var fc1 : base.u32
var fc2 : base.u32
var fc3 : base.u32
var pp0 : base.u32
var pp1 : base.u32
var pp2 : base.u32
var pp3 : base.u32
var pa0 : base.u32
var pa1 : base.u32
var pa2 : base.u32
var pa3 : base.u32
var pb0 : base.u32
var pb1 : base.u32
var pb2 : base.u32
var pb3 : base.u32
var pc0 : base.u32
var pc1 : base.u32
var pc2 : base.u32
var pc3 : base.u32
iterate (curr = args.curr, prev = args.prev)(length: 4, advance: 4, unroll: 1) {
fb0 = prev[0] as base.u32
pp0 = (fa0 ~mod+ fb0) ~mod- fc0
pa0 = pp0 ~mod- fa0
if pa0 >= 0x8000_0000 {
pa0 = 0 ~mod- pa0
}
pb0 = pp0 ~mod- fb0
if pb0 >= 0x8000_0000 {
pb0 = 0 ~mod- pb0
}
pc0 = pp0 ~mod- fc0
if pc0 >= 0x8000_0000 {
pc0 = 0 ~mod- pc0
}
if (pa0 <= pb0) and (pa0 <= pc0) {
// No-op.
} else if pb0 <= pc0 {
fa0 = fb0
} else {
fa0 = fc0
}
curr[0] = curr[0] ~mod+ ((fa0 & 0xFF) as base.u8)
fa0 = curr[0] as base.u32
fc0 = fb0
fb1 = prev[1] as base.u32
pp1 = (fa1 ~mod+ fb1) ~mod- fc1
pa1 = pp1 ~mod- fa1
if pa1 >= 0x8000_0000 {
pa1 = 0 ~mod- pa1
}
pb1 = pp1 ~mod- fb1
if pb1 >= 0x8000_0000 {
pb1 = 0 ~mod- pb1
}
pc1 = pp1 ~mod- fc1
if pc1 >= 0x8000_0000 {
pc1 = 0 ~mod- pc1
}
if (pa1 <= pb1) and (pa1 <= pc1) {
// No-op.
} else if pb1 <= pc1 {
fa1 = fb1
} else {
fa1 = fc1
}
curr[1] = curr[1] ~mod+ ((fa1 & 0xFF) as base.u8)
fa1 = curr[1] as base.u32
fc1 = fb1
fb2 = prev[2] as base.u32
pp2 = (fa2 ~mod+ fb2) ~mod- fc2
pa2 = pp2 ~mod- fa2
if pa2 >= 0x8000_0000 {
pa2 = 0 ~mod- pa2
}
pb2 = pp2 ~mod- fb2
if pb2 >= 0x8000_0000 {
pb2 = 0 ~mod- pb2
}
pc2 = pp2 ~mod- fc2
if pc2 >= 0x8000_0000 {
pc2 = 0 ~mod- pc2
}
if (pa2 <= pb2) and (pa2 <= pc2) {
// No-op.
} else if pb2 <= pc2 {
fa2 = fb2
} else {
fa2 = fc2
}
curr[2] = curr[2] ~mod+ ((fa2 & 0xFF) as base.u8)
fa2 = curr[2] as base.u32
fc2 = fb2
fb3 = prev[3] as base.u32
pp3 = (fa3 ~mod+ fb3) ~mod- fc3
pa3 = pp3 ~mod- fa3
if pa3 >= 0x8000_0000 {
pa3 = 0 ~mod- pa3
}
pb3 = pp3 ~mod- fb3
if pb3 >= 0x8000_0000 {
pb3 = 0 ~mod- pb3
}
pc3 = pp3 ~mod- fc3
if pc3 >= 0x8000_0000 {
pc3 = 0 ~mod- pc3
}
if (pa3 <= pb3) and (pa3 <= pc3) {
// No-op.
} else if pb3 <= pc3 {
fa3 = fb3
} else {
fa3 = fc3
}
curr[3] = curr[3] ~mod+ ((fa3 & 0xFF) as base.u8)
fa3 = curr[3] as base.u32
fc3 = fb3
}
}