std/deflate/decode_deflate.wuffs

// Copyright 2017 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.

pub status "?bad Huffman code (over-subscribed)"
pub status "?bad Huffman code (under-subscribed)"
pub status "?bad Huffman code length count"
pub status "?bad Huffman code length repetition"
pub status "?bad Huffman code"
pub status "?bad Huffman minimum code length"
pub status "?bad block"
pub status "?bad distance"
pub status "?bad distance code count"
pub status "?bad literal/length code count"
pub status "?inconsistent stored block length"
pub status "?missing end-of-block code"
pub status "?no Huffman codes"

pri status "?internal error: inconsistent Huffman decoder state"
pri status "?internal error: inconsistent I/O"
pri status "?internal error: inconsistent distance"
pri status "?internal error: inconsistent n_bits"

pub const decoder_workbuf_len_max_incl_worst_case base.u64 = 32768 + 512

// The next two tables were created by script/print-deflate-magic-numbers.go.
//
// The u32 values' meanings are the same as the decoder.huffs u32 values. In
// particular, bit 30 indicates a base number + extra bits, bits 23-8 are the
// base number and bits 7-4 are the number of those extra bits.
//
// Some trailing elements are 0x08000000. Bit 27 indicates an invalid value.

pri const lcode_magic_numbers array[32] base.u32 = [
	0x40000000, 0x40000100, 0x40000200, 0x40000300, 0x40000400, 0x40000500, 0x40000600, 0x40000700,
	0x40000810, 0x40000A10, 0x40000C10, 0x40000E10, 0x40001020, 0x40001420, 0x40001820, 0x40001C20,
	0x40002030, 0x40002830, 0x40003030, 0x40003830, 0x40004040, 0x40005040, 0x40006040, 0x40007040,
	0x40008050, 0x4000A050, 0x4000C050, 0x4000E050, 0x4000FF00, 0x08000000, 0x08000000, 0x08000000,
]

pri const dcode_magic_numbers array[32] base.u32 = [
	0x40000000, 0x40000100, 0x40000200, 0x40000300, 0x40000410, 0x40000610, 0x40000820, 0x40000C20,
	0x40001030, 0x40001830, 0x40002040, 0x40003040, 0x40004050, 0x40006050, 0x40008060, 0x4000C060,
	0x40010070, 0x40018070, 0x40020080, 0x40030080, 0x40040090, 0x40060090, 0x400800A0, 0x400C00A0,
	0x401000B0, 0x401800B0, 0x402000C0, 0x403000C0, 0x404000D0, 0x406000D0, 0x08000000, 0x08000000,
]

// TODO: replace the magic "big enough" 1024 with something more principled,
// perhaps discovered via an exhaustive search.
pri const huffs_table_size base.u32 = 1024

pub struct decoder?(
	// These fields yield src's bits in Least Significant Bits order.
	bits   base.u32,
	n_bits base.u32,

	// history_index indexes the history array, defined below.
	history_index base.u32,

	// end_of_block is whether decode_huffman_xxx saw an end-of-block code.
	//
	// TODO: can decode_huffman_xxx signal this in band instead of out of band?
	end_of_block base.bool,

	// huffs and n_huffs_bits are the lookup tables for Huffman decodings.
	//
	// There are up to 2 Huffman decoders active at any one time. As per this
	// package's README.md:
	//  - huffs[0] is used for clcode and lcode.
	//  - huffs[1] is used for dcode.
	//
	// The initial table key is the low n_huffs_bits of the decoder.bits field.
	// Keys longer than 9 bits require a two step lookup, the first step
	// examines the low 9 bits, the second step examines the remaining bits.
	// Two steps are required at most, as keys are at most 15 bits long.
	//
	// Using decoder.bits's low n_huffs_bits as a table key is valid even if
	// decoder.n_bits is less than n_huffs_bits, because the immediate next
	// step after indexing the table by the key is to compare decoder.n_bits to
	// the table value's number of decoder.bits to consume. If it compares
	// less, then more source bytes are read and the table lookup re-tried.
	//
	// The table value's bits:
	//  - bit        31 indicates a literal.
	//  - bit        30 indicates a base number + extra bits.
	//  - bit        29 indicates end-of-block.
	//  - bit        28 indicates a redirect to another part of the table.
	//  - bit        27 indicates an invalid value.
	//  - bits 26 .. 24 are zero.
	//  - bits 23 ..  8 are the redirect offset, literal (in bits 15-8) or base number.
	//  - bits  7 ..  4 are the redirected table's bits or number of extra bits.
	//  - bits  3 ..  0 are the number of decoder.bits to consume.
	//
	// Exactly one of the eight bits 31-24 should be set.
	huffs        array[2] array[huffs_table_size] base.u32,
	n_huffs_bits array[2] base.u32[..9],

	// history holds up to the last 32KiB of decoded output, if the decoding
	// was incomplete (e.g. due to a short read or write). RFC 1951 (DEFLATE)
	// gives the maximum distance in a length-distance back-reference as 32768,
	// or 0x8000.
	//
	// It is a ringbuffer, so that the most distant byte in the decoding isn't
	// necessarily history[0]. The ringbuffer is full (i.e. it holds 32KiB of
	// history) if and only if history_index >= 0x8000.
	//
	// history[history_index & 0x7FFF] is where the next byte of decoded output
	// will be written.
	history array[0x8000] base.u8,  // 32 KiB.

	// code_lengths is used to pass out-of-band data to init_huff.
	//
	// code_lengths[args.n_codes0 + i] holds the number of bits in the i'th
	// code.
	code_lengths array[320] base.u8[..15],

	util base.utility,
)

pub func decoder.workbuf_len() base.range_ii_u64 {
	return this.util.make_range_ii_u64(
		min_incl:decoder_workbuf_len_max_incl_worst_case,
		max_incl:decoder_workbuf_len_max_incl_worst_case)
}

pub func decoder.decode_io_writer?(dst base.io_writer, src base.io_reader, workbuf slice base.u8) {
	var status       base.status
	var written      slice base.u8
	var n_copied     base.u64
	var already_full base.u32[..0x8000]

	while true {
		args.dst.set_mark!()
		status =? this.decode_blocks?(dst:args.dst, src:args.src)
		if not status.is_suspension() {
			return status
		}
		// TODO: should "since_mark" be "since_mark!", as the return value lets
		// you modify the state of args.dst, so future mutations (via the
		// slice) can change the veracity of any args.dst assertions?
		written = args.dst.since_mark()
		// Append written, the decoded output, to the history ringbuffer.
		if written.length() >= 0x8000 {
			// If written is longer than the ringbuffer, we can ignore the
			// previous value of history_index, as we will overwrite the whole
			// ringbuffer.
			written = written.suffix(up_to:0x8000)
			this.history[:].copy_from_slice!(s:written)
			this.history_index = 0x8000
		} else {
			// Otherwise, append written to the history ringbuffer starting at
			// the previous history_index (modulo 0x8000).
			n_copied = this.history[this.history_index & 0x7FFF:].copy_from_slice!(s:written)
			if n_copied < written.length() {
				// a_slice.copy_from(s:b_slice) returns the minimum of the two
				// slice lengths. If that value is less than b_slice.length(),
				// then not all of b_slice was copied.
				//
				// In terms of the history ringbuffer, that means that we have
				// to wrap around and copy the remainder of written over the
				// start of the history ringbuffer.
				written = written[n_copied:]
				n_copied = this.history[:].copy_from_slice!(s:written)
				// Set history_index (modulo 0x8000) to the length of this
				// remainder. The &0x7FFF is redundant, but proves to the
				// compiler that the conversion to u32 will not overflow. The
				// +0x8000 is to maintain that the history ringbuffer is full
				// if and only if history_index >= 0x8000.
				this.history_index = ((n_copied & 0x7FFF) as base.u32) + 0x8000
			} else {
				// We didn't need to wrap around.
				already_full = 0
				if this.history_index >= 0x8000 {
					already_full = 0x8000
				}
				this.history_index = (this.history_index & 0x7FFF) + ((n_copied & 0x7FFF) as base.u32) + already_full
			}
		}
		yield status
	}
}

pri func decoder.decode_blocks?(dst base.io_writer, src base.io_reader) {
	var final  base.u32
	var b0     base.u32[..255]
	var type   base.u32
	var status base.status

	while:outer final == 0 {
		while this.n_bits < 3,
			post this.n_bits >= 3,
		{
			b0 = args.src.read_u8_as_u32?()
			this.bits |= b0 << this.n_bits
			this.n_bits += 8
		}
		final = this.bits & 0x01
		type = (this.bits >> 1) & 0x03
		this.bits >>= 3
		this.n_bits -= 3

		if type == 0 {
			this.decode_uncompressed?(dst:args.dst, src:args.src)
			continue
		} else if type == 1 {
			status = this.init_fixed_huffman!()
			// TODO: "if status.is_error()" is probably more idiomatic, but for
			// some mysterious, idiosyncratic reason, performs noticably worse
			// for gcc (but not for clang).
			//
			// See git commit 3bf9573 "Work around strange status.is_error
			// performance".
			if not status.is_ok() {
				return status
			}
		} else if type == 2 {
			this.init_dynamic_huffman?(src:args.src)
		} else {
			return "?bad block"
		}

		this.end_of_block = false
		while true {
			status = this.decode_huffman_fast!(dst:args.dst, src:args.src)
			if status.is_error() {
				return status
			}
			if this.end_of_block {
				continue:outer
			}
			this.decode_huffman_slow?(dst:args.dst, src:args.src)
			if this.end_of_block {
				continue:outer
			}
		}
	}
}

// decode_uncompressed decodes an uncompresed block as per the RFC section
// 3.2.4.
pri func decoder.decode_uncompressed?(dst base.io_writer, src base.io_reader) {
	var length   base.u32
	var n_copied base.u32

	// TODO: make this "if" into a function invariant?
	//
	// Ditto for decode_huffman_slow and decode_huffman_fast.
	if (this.n_bits >= 8) or ((this.bits >> (this.n_bits & 7)) != 0) {
		return "?internal error: inconsistent n_bits"
	}
	this.n_bits = 0
	this.bits = 0

	length = args.src.read_u32le?()
	if (length.low_bits(n:16) + length.high_bits(n:16)) != 0xFFFF {
		return "?inconsistent stored block length"
	}
	length = length.low_bits(n:16)
	while true {
		n_copied = args.dst.copy_n_from_reader!(n:length, r:args.src)
		if length <= n_copied {
			return ok
		}
		length -= n_copied
		if args.dst.available() == 0 {
			yield base."$short write"
		} else {
			yield base."$short read"
		}
	}
}

// init_fixed_huffman initializes this.huffs as per the RFC section 3.2.6.
pri func decoder.init_fixed_huffman!() base.status {
	var i      base.u32
	var status base.status

	while i < 144 {
		this.code_lengths[i] = 8
		i += 1
	}
	while i < 256 {
		this.code_lengths[i] = 9
		i += 1
	}
	while i < 280 {
		this.code_lengths[i] = 7
		i += 1
	}
	while i < 288 {
		this.code_lengths[i] = 8
		i += 1
	}
	while i < 320 {
		this.code_lengths[i] = 5
		i += 1
	}

	status = this.init_huff!(which:0, n_codes0:0, n_codes1:288, base_symbol:257)
	if status.is_error() {
		return status
	}
	status = this.init_huff!(which:1, n_codes0:288, n_codes1:320, base_symbol:0)
	if status.is_error() {
		return status
	}
	return ok
}

// init_dynamic_huffman initializes this.huffs as per the RFC section 3.2.7.
pri func decoder.init_dynamic_huffman?(src base.io_reader) {
	var bits               base.u32
	var n_bits             base.u32
	var b0                 base.u32[..255]
	var n_lit              base.u32[..288]
	var n_dist             base.u32[..32]
	var n_clen             base.u32[..19]
	var i                  base.u32
	var b1                 base.u32[..255]
	var status             base.status
	var mask               base.u32[..511]
	var table_entry        base.u32
	var table_entry_n_bits base.u32[..15]
	var b2                 base.u32[..255]
	var n_extra_bits       base.u32[..7]
	var rep_symbol         base.u8[..15]
	var rep_count          base.u32
	var b3                 base.u32[..255]

	bits = this.bits
	n_bits = this.n_bits
	while n_bits < 14,
		post n_bits >= 14,
	{
		b0 = args.src.read_u8_as_u32?()
		bits |= b0 << n_bits
		n_bits += 8
	}
	n_lit = bits.low_bits(n:5) + 257
	if n_lit > 286 {
		return "?bad literal/length code count"
	}
	bits >>= 5
	n_dist = bits.low_bits(n:5) + 1
	if n_dist > 30 {
		return "?bad distance code count"
	}
	bits >>= 5
	n_clen = bits.low_bits(n:4) + 4
	bits >>= 4
	n_bits -= 14

	// Read the clcode Huffman table: H-CL.
	i = 0
	while i < n_clen {
		while n_bits < 3,
			inv i < n_clen,
			post n_bits >= 3,
		{
			b1 = args.src.read_u8_as_u32?()
			bits |= b1 << n_bits
			n_bits += 8
		}
		assert i < 19 via "a < b: a < c; c <= b"(c:n_clen)
		this.code_lengths[code_order[i]] = (bits & 0x07) as base.u8
		bits >>= 3
		n_bits -= 3
		i += 1
	}
	while i < 19 {
		this.code_lengths[code_order[i]] = 0
		i += 1
	}
	status = this.init_huff!(which:0, n_codes0:0, n_codes1:19, base_symbol:0xFFF)
	if status.is_error() {
		return status
	}

	// Decode the code lengths for the next two Huffman tables.
	mask = ((1 as base.u32) << this.n_huffs_bits[0]) - 1
	i = 0
	while i < (n_lit + n_dist) {
		assert i < (288 + 32) via "a < (b + c): a < (b0 + c0); b0 <= b; c0 <= c"(b0:n_lit, c0:n_dist)

		// Decode a clcode symbol from H-CL.
		while true,
			inv i < 320,
		{
			table_entry = this.huffs[0][bits & mask]
			table_entry_n_bits = table_entry & 15
			if n_bits >= table_entry_n_bits {
				bits >>= table_entry_n_bits
				n_bits -= table_entry_n_bits
				break
			}
			assert n_bits < 15 via "a < b: a < c; c <= b"(c:table_entry_n_bits)
			b2 = args.src.read_u8_as_u32?()
			bits |= b2 << n_bits
			n_bits += 8
		}
		// For H-CL, there should be no redirections and all symbols should be
		// literals.
		if (table_entry >> 24) != 0x80 {
			return "?internal error: inconsistent Huffman decoder state"
		}
		table_entry = (table_entry >> 8) & 0xFF

		// Write a literal code length.
		if table_entry < 16 {
			this.code_lengths[i] = table_entry as base.u8
			i += 1
			continue
		}

		// Write a repeated code length.
		n_extra_bits = 0
		rep_symbol = 0
		rep_count = 0
		if table_entry == 16 {
			n_extra_bits = 2
			if i <= 0 {
				return "?bad Huffman code length repetition"
			}
			rep_symbol = this.code_lengths[i - 1]
			rep_count = 3
			assert rep_count <= 11
		} else if table_entry == 17 {
			n_extra_bits = 3
			rep_symbol = 0
			rep_count = 3
			assert rep_count <= 11
		} else if table_entry == 18 {
			n_extra_bits = 7
			rep_symbol = 0
			rep_count = 11
			assert rep_count <= 11
		} else {
			return "?internal error: inconsistent Huffman decoder state"
		}
		while n_bits < n_extra_bits,
			inv i < 320,
			inv rep_count <= 11,
			post n_bits >= n_extra_bits,
		{
			assert n_bits < 7 via "a < b: a < c; c <= b"(c:n_extra_bits)
			b3 = args.src.read_u8_as_u32?()
			bits |= b3 << n_bits
			n_bits += 8
		}
		rep_count += bits.low_bits(n:n_extra_bits)
		bits >>= n_extra_bits
		n_bits -= n_extra_bits

		while rep_count > 0 {
			// TODO: hoist this check up one level?
			if i >= (n_lit + n_dist) {
				return "?bad Huffman code length count"
			}
			assert i < (288 + 32) via "a < (b + c): a < (b0 + c0); b0 <= b; c0 <= c"(b0:n_lit, c0:n_dist)
			this.code_lengths[i] = rep_symbol
			i += 1
			rep_count -= 1
		}
	}

	if i != (n_lit + n_dist) {
		return "?bad Huffman code length count"
	}
	if this.code_lengths[256] == 0 {
		return "?missing end-of-block code"
	}

	status = this.init_huff!(which:0, n_codes0:0, n_codes1:n_lit, base_symbol:257)
	if status.is_error() {
		return status
	}
	status = this.init_huff!(which:1, n_codes0:n_lit, n_codes1:n_lit + n_dist, base_symbol:0)
	if status.is_error() {
		return status
	}

	this.bits = bits
	this.n_bits = n_bits
}

// TODO: make named constants for 15, 19, 319, etc.

pri func decoder.init_huff!(which base.u32[..1], n_codes0 base.u32[..320], n_codes1 base.u32[..320], base_symbol base.u32) base.status {
	var counts            array[16] base.u16[..320]
	var i                 base.u32
	var remaining         base.u32
	var offsets           array[16] base.u16[..320]
	var n_symbols         base.u32[..320]
	var count             base.u32[..320]
	var symbols           array[320] base.u16[..319]
	var min_cl            base.u32[..9]
	var max_cl            base.u32[..15]
	var initial_high_bits base.u32
	var prev_cl           base.u32[..15]
	var prev_redirect_key base.u32
	var top               base.u32[..huffs_table_size]
	var next_top          base.u32[..huffs_table_size]
	var code              base.u32
	var key               base.u32
	var value             base.u32
	var cl                base.u32[..15]
	var redirect_key      base.u32[..511]
	var j                 base.u32[..16]
	var reversed_key      base.u32[..511]
	var symbol            base.u32[..319]
	var high_bits         base.u32
	var delta             base.u32

	// For the clcode example in this package's README.md:
	//  - n_codes0 = 0
	//  - n_codes1 = 19
	//  - code_lengths[ 0] = 3
	//  - code_lengths[ 1] = 0
	//  - code_lengths[ 2] = 0
	//  - code_lengths[ 3] = 5
	//  - code_lengths[ 4] = 3
	//  - code_lengths[ 5] = 3
	//  - code_lengths[ 6] = 3
	//  - code_lengths[ 7] = 3
	//  - code_lengths[ 8] = 3
	//  - code_lengths[ 9] = 3
	//  - code_lengths[10] = 0
	//  - code_lengths[11] = 0
	//  - code_lengths[12] = 0
	//  - code_lengths[13] = 0
	//  - code_lengths[14] = 0
	//  - code_lengths[15] = 0
	//  - code_lengths[16] = 0
	//  - code_lengths[17] = 4
	//  - code_lengths[18] = 5

	// Calculate counts.
	//
	// For the clcode example in this package's README.md:
	//  - counts[0] = 9
	//  - counts[1] = 0
	//  - counts[2] = 0
	//  - counts[3] = 7
	//  - counts[4] = 1
	//  - counts[5] = 2
	//  - all other counts elements are 0.
	i = args.n_codes0
	while i < args.n_codes1 {
		assert i < 320 via "a < b: a < c; c <= b"(c:args.n_codes1)
		// TODO: this if should be unnecessary. Have some way to assert that,
		// for all j, counts[j] <= i, and thus counts[j]++ will not overflow.
		if counts[this.code_lengths[i]] >= 320 {
			return "?internal error: inconsistent Huffman decoder state"
		}
		counts[this.code_lengths[i]] += 1
		i += 1
	}
	if ((counts[0] as base.u32) + args.n_codes0) == args.n_codes1 {
		return "?no Huffman codes"
	}

	// Check that the Huffman code completely covers all possible input bits.
	remaining = 1  // There is 1 possible 0-bit code.
	i = 1
	while i <= 15 {
		if remaining > (1 << 30) {
			return "?internal error: inconsistent Huffman decoder state"
		}
		// Each iteration doubles the number of possible remaining codes.
		remaining <<= 1
		if remaining < (counts[i] as base.u32) {
			return "?bad Huffman code (over-subscribed)"
		}
		remaining -= counts[i] as base.u32
		i += 1
	}
	if remaining != 0 {
		// TODO: when is a degenerate Huffman table valid?
		return "?bad Huffman code (under-subscribed)"
	}

	// Calculate offsets and n_symbols.
	//
	// For the clcode example in this package's README.md:
	//  - offsets[0] =  0
	//  - offsets[1] =  0
	//  - offsets[2] =  0
	//  - offsets[3] =  0
	//  - offsets[4] =  7
	//  - offsets[5] =  8
	//  - offsets[6] = 10
	//  - all other offsets elements are 10.
	//  - n_symbols = 10
	i = 1
	while i <= 15 {
		offsets[i] = n_symbols as base.u16
		count = counts[i] as base.u32
		if n_symbols > (320 - count) {
			return "?internal error: inconsistent Huffman decoder state"
		}
		assert (n_symbols + count) <= 320 via "(a + b) <= c: a <= (c - b)"()
		// TODO: change this to n_symbols += count, once the proof engine's
		// bounds checking can handle it.
		n_symbols = n_symbols + count
		i += 1
	}
	if n_symbols > 288 {
		return "?internal error: inconsistent Huffman decoder state"
	}

	// Calculate symbols.
	//
	// For the clcode example in this package's README.md:
	//  - symbols[0] =  0
	//  - symbols[1] =  4
	//  - symbols[2] =  5
	//  - symbols[3] =  6
	//  - symbols[4] =  7
	//  - symbols[5] =  8
	//  - symbols[6] =  9
	//  - symbols[7] = 17
	//  - symbols[8] =  3
	//  - symbols[9] = 18
	//
	// As a (local variable) side effect, offsets' values will be updated:
	//  - offsets[3] =  7, formerly 0
	//  - offsets[4] =  8, formerly 7
	//  - offsets[5] = 10, formerly 8
	i = args.n_codes0
	while i < args.n_codes1,
		inv n_symbols <= 288,
	{
		assert i < 320 via "a < b: a < c; c <= b"(c:args.n_codes1)
		// TODO: this if check should be unnecessary.
		if i < args.n_codes0 {
			return "?internal error: inconsistent Huffman decoder state"
		}
		if this.code_lengths[i] != 0 {
			if offsets[this.code_lengths[i]] >= 320 {
				return "?internal error: inconsistent Huffman decoder state"
			}
			symbols[offsets[this.code_lengths[i]]] = (i - args.n_codes0) as base.u16
			offsets[this.code_lengths[i]] += 1
		}
		i += 1
	}

	// Calculate min_cl and max_cl.
	//
	// For the clcode example in this package's README.md:
	//  - min_cl = 3
	//  - max_cl = 5
	min_cl = 1
	while true,
		inv n_symbols <= 288,
	{
		if counts[min_cl] != 0 {
			break
		}
		if min_cl >= 9 {
			return "?bad Huffman minimum code length"
		}
		min_cl += 1
	}
	max_cl = 15
	while true,
		inv n_symbols <= 288,
	{
		if counts[max_cl] != 0 {
			break
		}
		if max_cl <= 1 {
			// TODO: when is a degenerate Huffman table valid?
			return "?no Huffman codes"
		}
		max_cl -= 1
	}
	if max_cl <= 9 {
		this.n_huffs_bits[args.which] = max_cl
	} else {
		this.n_huffs_bits[args.which] = 9
	}

	// Calculate this.huffs[args.which].
	//
	// For the clcode example in this package's README.md:
	//  - this.huffs[0][0b..000] = 0x80000003 (literal, symbols[0]=0x00, code_length=3)
	//  - this.huffs[0][0b..100] = 0x80000403 (literal, symbols[1]=0x04, code_length=3)
	//  - this.huffs[0][0b..010] = 0x80000503 (literal, symbols[2]=0x05, code_length=3)
	//  - this.huffs[0][0b..110] = 0x80000603 (literal, symbols[3]=0x06, code_length=3)
	//  - this.huffs[0][0b..001] = 0x80000703 (literal, symbols[4]=0x07, code_length=3)
	//  - this.huffs[0][0b..101] = 0x80000803 (literal, symbols[5]=0x08, code_length=3)
	//  - this.huffs[0][0b..011] = 0x80000903 (literal, symbols[6]=0x09, code_length=3)
	//  - this.huffs[0][0b.0111] = 0x80001104 (literal, symbols[7]=0x11, code_length=4)
	//  - this.huffs[0][0b01111] = 0x80000305 (literal, symbols[8]=0x03, code_length=5)
	//  - this.huffs[0][0b11111] = 0x80001805 (literal, symbols[9]=0x18, code_length=5)
	i = 0
	if (n_symbols != (offsets[max_cl] as base.u32)) or (n_symbols != (offsets[15] as base.u32)) {
		return "?internal error: inconsistent Huffman decoder state"
	}
	if (args.n_codes0 + (symbols[0] as base.u32)) >= 320 {
		return "?internal error: inconsistent Huffman decoder state"
	}

	initial_high_bits = 1 << 9
	if max_cl < 9 {
		initial_high_bits = (1 as base.u32) << max_cl
	}
	prev_cl = this.code_lengths[args.n_codes0 + (symbols[0] as base.u32)] as base.u32
	prev_redirect_key = 0xFFFFFFFF
	top = 0
	next_top = 512
	code = 0
	key = 0
	value = 0
	while true,
		pre code < (1 << 15),
		pre i < 288,
		inv n_symbols <= 288,
	{
		if (args.n_codes0 + (symbols[i] as base.u32)) >= 320 {
			return "?internal error: inconsistent Huffman decoder state"
		}
		cl = this.code_lengths[args.n_codes0 + (symbols[i] as base.u32)] as base.u32
		if cl > prev_cl {
			code <<= cl - prev_cl
			if code >= (1 << 15) {
				return "?internal error: inconsistent Huffman decoder state"
			}
		}
		// For the remainder of this loop body, prev_cl is the original code
		// length, cl is possibly clipped by 9, if in the 2nd-level table.
		prev_cl = cl

		key = code
		if cl > 9 {
			cl -= 9
			assert cl <= 9

			redirect_key = (key >> cl) & 511
			key = key.low_bits(n:cl)
			if prev_redirect_key != redirect_key {
				prev_redirect_key = redirect_key

				// Calculate the number of bits needed for the 2nd level table.
				// This computation is similar to "check that the Huffman code
				// completely covers all possible input bits" above.
				remaining = (1 as base.u32) << cl
				j = prev_cl
				while j <= 15,
					inv cl <= 9,
					inv code < (1 << 15),
					inv i < 288,
					inv n_symbols <= 288,
				{
					if remaining <= (counts[j] as base.u32) {
						break
					}
					remaining -= counts[j] as base.u32
					if remaining > (1 << 30) {
						return "?internal error: inconsistent Huffman decoder state"
					}
					remaining <<= 1
					j += 1
				}
				if (j <= 9) or (15 < j) {
					return "?internal error: inconsistent Huffman decoder state"
				}
				j -= 9
				initial_high_bits = (1 as base.u32) << j

				top = next_top
				if (top + ((1 as base.u32) << j)) > huffs_table_size {
					return "?internal error: inconsistent Huffman decoder state"
				}
				assert (top + ((1 as base.u32) << j)) <= 1024 via "a <= b: a <= c; c <= b"(c:huffs_table_size)
				next_top = top + ((1 as base.u32) << j)

				redirect_key = (reverse8[redirect_key >> 1] as base.u32) | ((redirect_key & 1) << 8)
				this.huffs[args.which][redirect_key] = 0x10000009 | (top << 8) | (j << 4)
			}
		}
		if (key >= (1 << 9)) or (counts[prev_cl] <= 0) {
			return "?internal error: inconsistent Huffman decoder state"
		}
		counts[prev_cl] -= 1

		reversed_key = (reverse8[key >> 1] as base.u32) | ((key & 1) << 8)
		reversed_key >>= 9 - cl

		symbol = symbols[i] as base.u32
		if symbol == 256 {
			// End-of-block.
			value = 0x20000000 | cl
		} else if (symbol < 256) and (args.which == 0) {
			// Literal.
			value = 0x80000000 | (symbol << 8) | cl
		} else if symbol >= args.base_symbol {
			// Base number + extra bits.
			symbol -= args.base_symbol
			if args.which == 0 {
				value = lcode_magic_numbers[symbol & 31] | cl
			} else {
				value = dcode_magic_numbers[symbol & 31] | cl
			}
		} else {
			return "?internal error: inconsistent Huffman decoder state"
		}

		// The table uses log2(initial_high_bits) bits, but reversed_key only
		// has cl bits. We duplicate the key-value pair across all possible
		// values of the high (log2(initial_high_bits) - cl) bits.
		high_bits = initial_high_bits
		delta = (1 as base.u32) << cl
		while high_bits >= delta,
			inv code < (1 << 15),
			inv i < 288,
			inv n_symbols <= 288,
		{
			high_bits -= delta
			if (top + ((high_bits | reversed_key) & 511)) >= huffs_table_size {
				return "?internal error: inconsistent Huffman decoder state"
			}
			assert (top + ((high_bits | reversed_key) & 511)) < 1024 via "a < b: a < c; c <= b"(c:huffs_table_size)
			this.huffs[args.which][top + ((high_bits | reversed_key) & 511)] = value
		}

		i += 1
		if i >= n_symbols {
			break
		}
		assert i < 288 via "a < b: a < c; c <= b"(c:n_symbols)
		code += 1
		if code >= (1 << 15) {
			return "?internal error: inconsistent Huffman decoder state"
		}
	}
	return ok
}