std/png/decode_filter_fallback.wuffs - external/github.com/google/wuffs - Git at Google

 // 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
 	}
 }
	// 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
	}
	}