Earlier arguments and reference sources

The main source snapshot is zlib-formal at 0f1428677ebf5b1614ff77f4702bbb382b2bf3c6. The reference review read its source and audit documents. It did not rebuild the snapshot or establish its results in this repository. This is a reuse record; progress owns current work and checking defines acceptance.

Ideas adapted

The table uses paths relative to the reference's lean/ directory. The tables below map the function families and changed representations.

What does not transfer

The reference heap uses typed cells and byte blocks. The present heap uses object records and tables. Heap statements and proof terms need adaptation. Pure arithmetic, bitstream relations, loop measures and decomposition can retain their meaning only after their definitions and domains are compared.

The reference sequence theorem Zlib.Api.seq_safe takes ApiContract as a hypothesis. Its contract audit records instances with false preconditions and false strategy contracts. The call alphabet and induction structure are useful. A conditional sequence theorem does not establish safety here: every library callee needs a theorem about its actual translation, and actual init must establish the invariant. Unrelated witnesses cannot supply that connection.

The reference's ub.patch policy and enabled patches differ. Its build configuration and proof status do not transfer. This repository verifies its own upstream pin plus reviewed patches, under its own public domains and acceptance rules.

flowchart LR
    R[Pinned reference] --> M[Extract mathematics and argument structure]
    M --> T[Restate for the present source and heap]
    T --> K[Kernel check, audit and mutants]
    K --> C[Accept only evidence for this repository]

The tables below locate reusable argument families. Component proof guides explain the present argument structure. Neither a reference link nor a historical reported test is a new validation run.

Reusing an earlier argument

Earlier heaps used tagged cells and byte blocks. Current heaps use records and object tables. Pure arguments transfer only after definitions and domains agree. Heap-level proofs require new execution, frame and ownership arguments. Earlier callee-contract hypotheses cannot replace theorems about actual translated callees.

Deflate engine sources

Deflate lifecycle sources

Inflate sources

Table and trailer sources

Callback sources

Gzip sources

Historical short-distance check

The earlier record reported an experiment on a candidate missing-whave update before the fast path. Raw fixed-Huffman streams used one to three literals followed by a length-three match at distance one to four. The matrix included fast calls with at least six input bytes and 258 output bytes of room, input split one byte at a time, and two-call decoding with a fresh output buffer. The record reports agreement between paths, the expected “invalid distance too far back” error, and no sanitizer finding.

That experiment refuted the candidate only for those ordinary-inflate cases. It did not cover long distances, full or wrapped windows, other window sizes, or the callback decoder. It is historical test evidence, not a kernel proof or a newly repeated validation run.

Evidence boundary

The earlier review recorded 8000 randomized compressor sessions with sanitizers and round-trip comparison. It varied levels, strategies, memory levels, wrappers, chunk sizes down to one output byte, flush modes, parameter changes and copying. It reported no mismatch or sanitizer diagnostic in those sessions. Dictionary setting, priming and custom gzip headers were outside that run. The one-byte-window stored path was also excluded.

These observations do not prove safety for all inputs, initialization history, overlay capacity, other configurations or the C assumptions above. Focused reproducible evidence belongs with its regression. Acceptance rules belong in checking. Progress records current unresolved items and proof acceptance.

Historical gzip seek observation

The earlier record reported reading five bytes to EOF, then seeking five bytes relative to the current position. Seek returned ten while tell remained five. Its interpretation was that forward seek retained past; an older abstract relation instead required the target position and a cleared flag. This was not rerun for this revision. The source interpretation remains unfinished, and the observation does not establish an operational refinement or a new finding.