The decoder proof argument

The decoder's promise is to recover the bytes described by the compressed input, in order. Reading ahead, using a lookup table, copying several bytes in one loop, or pausing for another buffer must preserve that promise. It must also stay within valid memory and handle detected bad data through defined error returns.

The starting information is the unconsumed compressed input, the decoder's saved work and historical bytes, and the caller's offered buffers. The result is a justified output prefix and an exact continuation state, or the specified completion/error result. “Justified” means the independent format rules explain those output bytes. It does not mean that any buffered prefix is already a complete valid stream. Fragmented input, small output buffers, malformed data and admitted failures remain in the stated domain.

Check the promise on the examples

The previous chapters followed source bits, installed tables and output copies. Keep these small calculations in view:

These examples locate the obligations; they do not prove all inputs. The formal argument needs relations that continue to express these facts after every admitted step. Such a preserved relation is an invariant. To prove it about the C translation, first establish it from actual initialization, then show how each actual branch preserves it. An array bound alone cannot identify a symbol, and an abstractly correct symbol cannot justify an invalid read.

Unconsumed input

For the first two rows, compare all unread bits before and after the step. The saved integer hold contains the next bits, and the count bits says how many are valid. Unread caller bytes follow them. Call this combined bit sequence remainingBits. In the following teaching equation, low_bits lists the valid reservoir positions in reading order, byte_bits(unread_input_bytes) expands the remaining bytes in that same order, and ++ joins lists. It is explanatory notation, not a copied Lean definition:

remainingBits = low_bits(hold, bits) ++ byte_bits(unread_input_bytes)

Pulling a byte changes where that sequence resides without changing its values or order. Dropping a decoded field removes exactly its prefix. Here is the actual consuming operation used by inflate, from pinned inflate.c, lines 387–391:

#define DROPBITS(n) \
    do { \
        hold >>= (n); \
        bits -= (unsigned)(n); \
    } while (0)

For A, the caller must supply n=1: shifting 1110 gives 111 and the count falls from four to three. Supplying two would still leave an in-bounds integer operation, but it would delete D's first bit. The proof must establish both defined shifts and the correct removal amount. The source BitInv and stream connect locals to an actual readable input range and the normalized hold value.

PULLBYTE_succ states a real translated pull under that invariant and an explicit shift bound. NEEDBITS_run includes both success and input-exhaustion exits, preserving the unconsumed sequence while accounting for pulled bytes. These local statements do not themselves establish every main-decoder entry condition.

A decoded symbol depends on its supporting prefix. It need not describe every speculative bit already buffered. For AD, A consumes only the first bit although the root lookup inspects two. The same distinction must survive fast-path byte backtracking and resumption with new input views.

Actual table content

For the subtable row, having a table with enough cells is insufficient: its cells must return D. The constructor's output must be the very table the decoder later reads. The construction chapter explains the producer's stages: count tallies each code length, offs locates its scratch positions, and work lists symbols in code order. Follow those actual updates, reversed codes, repeated stores and subtable links, then establish what the written cells mean for the supplied lengths.

The declaration inflate_table_content retains actual execution, return classification and table contents. Its target definition makes the connection concrete: the returned heap contains the array, and the internal environment is an execution result tied to input lengths, kind, location and root width. Here “geometry” means the table regions, index bounds and links. These cannot be caller-supplied substitutes for running the constructor.

This still differs from a complete decoder interface. inflate_table_complete_decoder_safe explicitly requires a complete alphabet: the assigned codes leave no unused branches in the binary code tree. It does not cover empty or accepted incomplete single-symbol alphabets merely because the constructor can handle them. inflate_table_codes_decoder_safe addresses the code-length-table interface under its constructor premises. Read each statement's domain separately.

Table storage bounds and symbol meaning

LenTableSafe and DistTableSafe describe bounded root regions, bounded one-level links and suitable leaves. Their length and extra-bit bounds justify the fast decoder's refills and shifts. The 1444-entry default reservation combines 852 literal/length-table entries with 592 distance-table entries. Merely allocating that many cells does not establish their contents or link bounds.

In our teaching table, root 11 must lead to two readable cells; this is geometry. Subtable 1 must contain D with one-bit consumption; this is agreement with the independent code. Both are required. A mutation that swaps C and D can preserve every index bound while changing decoded output. The producer-to-consumer connection must retain each entry's exact operation tag op, consumption count bits, and returned value or link offset val, including invalid and end markers, at the same heap and returned width.

A caller invokes the theorem about the translated constructor after establishing its premises. It cannot assume an unproved callee specification or silently exclude a valid input because a convenient intermediate theorem has a narrower domain.

Output and logical history

For the copy and pause rows, compare bytes rather than just pointer positions. A literal extends output by that byte. A match follows the independent repetition rule: take the byte at the stated distance behind the current end, append it, and repeat. The available past consists of any preset dictionary followed by output so far, called the logical history. This definition includes newly written match bytes, as the AB example requires. The physical source can switch from the ring's tail to its start, then to current output, as in the six-byte worked match.

The proof therefore carries both shape and content. Window indices, live storage and initialized ranges justify access; a suffix relation says the retained window contains the most recent part of logical history, in its exact order. It identifies which historical byte each physical cell contains. A dictionary supplies history without being counted as new output. Replacing output buffers must preserve logical values without pretending old borrowed memory remains available forever.

copyMatch_run records the actual fast copy's successful or too-far-distance behavior under explicit context, distance, length and room premises. It is an internal execution result, not the entire public decoder or a proof that initialization and every history establish those premises.

Fast and slow composition

Safety also includes preserving unrelated memory, called the frame requirement. The source inflate_fast_safe states the helper's safety, termination, frame, normalization and writeback goal. actual_body_refines_token relates one actual fast body to an independent token, block end or rejected token. A one-body refinement and a complete helper safety statement supply different conclusions.

The optimization can only be used after its premises are established. At the actual guard, the main decoder must derive enough room for one complete instruction: six input bytes for the worst refill sequence and 258 output bytes for the longest match. It also needs fewer than eight held bits for exact byte backtracking, plus the table properties and valid history. Slow dispatch must preserve a compatible relation for smaller buffers, unfinished fields and returned matches. LOAD and RESTORE connect local registers with boundary state; they do not hold those representations equal throughout the body. Some mode changes consume no input and write no output. Such a silent transition needs a decreasing rank: a measure showing that the decoder cannot keep changing modes forever without progressing or returning.

Memory, termination and public scope

Every access additionally needs liveness, writable or readable permission, bounds and the correct object. Writes must preserve unrelated memory, as required by the frame condition. Cleanup accounts for allocations on success, failure and End. The C/runtime correspondence still includes pointer, alignment and uninitialized-memory limitations recorded in safety and the trusted base.

The executable model gives loops a finite iteration budget, called fuel. Termination must exclude exhaustion of that actual budget. Finite copy counts, bounded table links, progress measures and silent-transition ranks need composition into that concrete budget. The theorem's internal premises must come from actual initialization and allowed history operations, including refused calls.

The complete decoder composition is unfinished: the input, table-content, history-copy and exit relations must hold together in the same actual execution. Progress records accepted scope and remaining work; inflate states the public behavior to establish. Continue to stream state to follow this argument across call boundaries. As a separate comparison, compression block output follows the reverse direction: symbols becoming bits, pending bytes and delivered output.