// 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] ~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 c   : slice base.u8
	var fa0 : base.u8
	var fa1 : base.u8
	var fa2 : base.u8

	iterate (c = args.curr)(length: 3, advance: 3, unroll: 1) {
		fa0 ~mod+= c[0]
		c[0] = fa0
		fa1 ~mod+= c[1]
		c[1] = fa1
		fa2 ~mod+= c[2]
		c[2] = fa2
	}
}

pri func decoder.filter_1_distance_4_fallback!(curr: slice base.u8) {
	var c   : slice base.u8
	var fa0 : base.u8
	var fa1 : base.u8
	var fa2 : base.u8
	var fa3 : base.u8

	iterate (c = args.curr)(length: 4, advance: 4, unroll: 1) {
		fa0 ~mod+= c[0]
		c[0] = fa0
		fa1 ~mod+= c[1]
		c[1] = fa1
		fa2 ~mod+= c[2]
		c[2] = fa2
		fa3 ~mod+= c[3]
		c[3] = fa3
	}
}

// Filter 2: Up.

pri func decoder.filter_2!(curr: slice base.u8, prev: slice base.u8),
	choosy,
{
	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] ~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] ~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] ~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] ~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 c   : slice base.u8
	var p   : slice base.u8
	var fa0 : base.u8
	var fa1 : base.u8
	var fa2 : base.u8

	if args.prev.length() == 0 {
		iterate (c = args.curr)(length: 3, advance: 3, unroll: 1) {
			fa0 = (fa0 / 2) ~mod+ c[0]
			c[0] = fa0
			fa1 = (fa1 / 2) ~mod+ c[1]
			c[1] = fa1
			fa2 = (fa2 / 2) ~mod+ c[2]
			c[2] = fa2
		}

	} else {
		iterate (c = args.curr, p = args.prev)(length: 3, advance: 3, unroll: 1) {
			fa0 = ((((fa0 as base.u32) + (p[0] as base.u32)) / 2) as base.u8) ~mod+ c[0]
			c[0] = fa0
			fa1 = ((((fa1 as base.u32) + (p[1] as base.u32)) / 2) as base.u8) ~mod+ c[1]
			c[1] = fa1
			fa2 = ((((fa2 as base.u32) + (p[2] as base.u32)) / 2) as base.u8) ~mod+ c[2]
			c[2] = fa2
		}
	}
}

pri func decoder.filter_3_distance_4_fallback!(curr: slice base.u8, prev: slice base.u8) {
	var c   : slice base.u8
	var p   : 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 (c = args.curr)(length: 4, advance: 4, unroll: 1) {
			fa0 = (fa0 / 2) ~mod+ c[0]
			c[0] = fa0
			fa1 = (fa1 / 2) ~mod+ c[1]
			c[1] = fa1
			fa2 = (fa2 / 2) ~mod+ c[2]
			c[2] = fa2
			fa3 = (fa3 / 2) ~mod+ c[3]
			c[3] = fa3
		}

	} else {
		iterate (c = args.curr, p = args.prev)(length: 4, advance: 4, unroll: 1) {
			fa0 = ((((fa0 as base.u32) + (p[0] as base.u32)) / 2) as base.u8) ~mod+ c[0]
			c[0] = fa0
			fa1 = ((((fa1 as base.u32) + (p[1] as base.u32)) / 2) as base.u8) ~mod+ c[1]
			c[1] = fa1
			fa2 = ((((fa2 as base.u32) + (p[2] as base.u32)) / 2) as base.u8) ~mod+ c[2]
			c[2] = fa2
			fa3 = ((((fa3 as base.u32) + (p[3] as base.u32)) / 2) as base.u8) ~mod+ c[3]
			c[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] ~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] ~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 c   : slice base.u8
	var p   : 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 (c = args.curr, p = args.prev)(length: 3, advance: 3, unroll: 1) {
		fb0 = p[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
		}
		c[0] ~mod+= (fa0 & 0xFF) as base.u8
		fa0 = c[0] as base.u32
		fc0 = fb0

		fb1 = p[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
		}
		c[1] ~mod+= (fa1 & 0xFF) as base.u8
		fa1 = c[1] as base.u32
		fc1 = fb1

		fb2 = p[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
		}
		c[2] ~mod+= (fa2 & 0xFF) as base.u8
		fa2 = c[2] as base.u32
		fc2 = fb2
	}
}

pri func decoder.filter_4_distance_4_fallback!(curr: slice base.u8, prev: slice base.u8) {
	var c   : slice base.u8
	var p   : 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 (c = args.curr, p = args.prev)(length: 4, advance: 4, unroll: 1) {
		fb0 = p[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
		}
		c[0] ~mod+= (fa0 & 0xFF) as base.u8
		fa0 = c[0] as base.u32
		fc0 = fb0

		fb1 = p[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
		}
		c[1] ~mod+= (fa1 & 0xFF) as base.u8
		fa1 = c[1] as base.u32
		fc1 = fb1

		fb2 = p[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
		}
		c[2] ~mod+= (fa2 & 0xFF) as base.u8
		fa2 = c[2] as base.u32
		fc2 = fb2

		fb3 = p[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
		}
		c[3] ~mod+= (fa3 & 0xFF) as base.u8
		fa3 = c[3] as base.u32
		fc3 = fb3
	}
}