Proof progress and remaining work
b6f2139fa30f8b18 · Source at the matching commit ↗This page records evidence and unfinished work. For the statement and proof architecture, read the overview.
Contents
- All targets and dependencies
- Exact target evidence
- Current proof scope
- Remaining work
- Public API prerequisites
- Specification review
- Inflate
- Deflate
- Trees
- End-to-end claims
Proof progress graph
Follow the dependency edges, then inspect a target’s input range, proof state, and evidence.
- Fixed targets
- 181
- Registered exact proofs
- 81
- Local, not registered
- 33
- Uncompleted targets
- 67
2 uncompleted targets have recorded blockers. Input coverage and registration are listed separately inside each target.
Read dependencies from left to right. Edge numbers count connections between components; nodes count internal connections. Select a node to inspect actual targets.
Hover or focus a node to highlight connected paths. In the target graph, select a neighbor to continue along the dependencies.
Inspect targets and dependencies
Choose a component, or filter by name and evidence state. Every target links to its full evidence entry and recorded source.
Library queries6 targets
compressBoundRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 1
compressBound_zRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Implementations calling this entry 1
zlibVersionRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Implementations calling this entry 1
zlibCompileFlagsRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
zErrorRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Implementations calling this entry 2
get_crc_tableRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
Checksums11 targets
adler32Registered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proof dependencies 1
Entries called by this implementation 1
Implementations calling this entry 5
adler32_combineRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
adler32_combine64Registered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
crc32Registered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proof dependencies 1
Entries called by this implementation 1
Implementations calling this entry 4
crc32_zRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proof dependencies 1
Implementations calling this entry 2
crc32_combine_genRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 1
crc32_combine_gen64Registered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Implementations calling this entry 2
crc32_combine_opRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Implementations calling this entry 1
crc32_combineRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 1
crc32_combine64Registered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 2
Implementations calling this entry 1
Byte-address model9 targets
address_read_is_pureRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
raw_block_unchangedRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
every_layout_is_representableRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
every_existing_heap_accepts_layoutRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
mask_refines_base_plus_offsetRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
pointer_advance_preserves_low_bitsRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proofs depending on this target 1
first_aligned_offsetRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proof dependencies 1
byte_stores_preserve_basesRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
byte_modifies_preserve_basesRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
Inflate streams18 targets
inflateCopyNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
inflateInit2_Blocked- Input coverage
- No complete input coverage
- Evidence state
- Blocked
Entries called by this implementation 1
Implementations calling this entry 7
inflateInit_Registered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 1
Implementations calling this entry 1
inflateResetKeepRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Implementations calling this entry 1
inflateResetRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 1
Implementations calling this entry 8
inflateReset2Registered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 1
Implementations calling this entry 1
inflateEndRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Implementations calling this entry 2
inflateGetDictionaryRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
inflateGetHeaderRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
inflateSetDictionaryRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 1
inflateSyncPointRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
inflateMarkRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
inflateCodesUsedRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
inflateUndermineRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
inflateValidateRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
inflatePrimeRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
inflateSyncNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
Fast decoder obligations19 targets
actual_body_preserves_originLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 3
Proofs depending on this target 1
actual_body_refines_tokenLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 3
actual_fast_preserves_originLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
actual_distance_block_preserves_originLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 2
Proofs depending on this target 1
actual_distance_refines_lz77Local proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 2
Proofs depending on this target 1
distance_lookup_matches_formatLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
Proofs depending on this target 1
fast_safeLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
Proofs depending on this target 1
step_safeLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 3
length_lookup_matches_formatLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
Proofs depending on this target 1
actual_body_retains_selected_lengthLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
actual_copy_match_refines_lz77Local proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
Proofs depending on this target 1
match_array_refines_lz77Local proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 3
Proofs depending on this target 1
actual_drop_preserves_originLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
Proofs depending on this target 1
actual_pull_preserves_originLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
actual_rollback_preserves_originLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
Proofs depending on this target 1
drop_preserves_originLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 2
initial_originLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 1
pull_preserves_originLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 3
rollback_preserves_originLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 1
Decode-table obligations19 targets
decode_table_classifies_inputNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
decode_table_matches_formatNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
short_decode_table_leaf_soundNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
decode_table_leaf_soundNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
decode_table_read_preservedLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 1
constructor_establishes_decode_table_invariantNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
decode_table_invariant_of_prefixNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
constructor_establishes_query_stabilityNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
query_stability_of_prefixLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
short_rejected_leaf_stays_invalidLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 2
constructor_establishes_fast_leaf_flagsNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
fast_leaf_flags_of_prefixNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
fixed_tables_have_fast_leaf_flagsNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
leaf_classification_agreesNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
inflate_table_contentRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proofs depending on this target 1
inflate_table_decoder_safeRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proof dependencies 1
Proofs depending on this target 1
inflate_table_read_extentRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proof dependencies 1
constructor_root_bitsNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
constructor_subtable_bitsNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
Back-reference copying6 targets
output_copy_refines_lz77Local proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 1
window_copy_refines_lz77Local proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 1
copy_back_composeLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 1
copy_back_extends_historyLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
This record has no direct connection to another fixed target.
retained_history_agreesLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proofs depending on this target 2
window_distance_check_agreesLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
This record has no direct connection to another fixed target.
Deflate streams17 targets
deflateCopyNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
deflateInit2_Not completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
Implementations calling this entry 9
deflateInit_Registered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 1
Implementations calling this entry 1
deflateGetDictionaryRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
deflateEndRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Implementations calling this entry 3
deflateResetKeepRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 2
Implementations calling this entry 1
deflateResetRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 1
Implementations calling this entry 9
deflatePendingRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
deflateUsedRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
deflateTuneRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
deflateSetHeaderRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
deflateNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 4
Implementations calling this entry 10
deflateBound_zNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Implementations calling this entry 1
deflateBoundNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
deflatePrimeNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
deflateParamsNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
Implementations calling this entry 1
Callback decoding3 targets
inflateBackInit_Registered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proofs depending on this target 1
inflateBackNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
inflateBackEndRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
Gzip files32 targets
gzclose_rNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
Implementations calling this entry 1
gzclose_wNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 4
Implementations calling this entry 1
gzbufferRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
gzeofRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
gztell64Not completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Implementations calling this entry 1
gztellNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
gzoffset64Registered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Implementations calling this entry 1
gzoffsetRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Entries called by this implementation 1
gzerrorRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
gzclearerrRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
gzrewindRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Implementations calling this entry 1
gzseekNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
gzopenNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
gzopen64Not completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
gzdopenNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
gzreadNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
gzfreadNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
gzgetcNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
Implementations calling this entry 1
gzgetc_Not completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
gzungetcNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
gzgetsNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
gzdirectNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 2
gzwriteNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
gzfwriteNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
gzputcNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
gzputsNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
gzvprintfNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
Implementations calling this entry 1
gzprintfNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
gzflushNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
gzsetparamsNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 4
Whole-buffer operations8 targets
compress2_zNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 4
Implementations calling this entry 2
compress2Not completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
Implementations calling this entry 1
compress_zNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
compressNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
uncompress2_zNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 3
Implementations calling this entry 2
uncompress2Not completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
Implementations calling this entry 1
uncompress_zNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
uncompressNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
Entries called by this implementation 1
Format and API models20 targets
format_deterministicRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
format_prefix_freeRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
inflate_decodesRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proofs depending on this target 1
inflate_completesRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proofs depending on this target 1
inflate_rejects_invalidNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
deflate_validRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proofs depending on this target 4
deflate_completesRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
deflate_full_flush_resyncRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
roundtripRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proof dependencies 3
roundtrip_completesRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proof dependencies 3
dict_roundtripLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
header_roundtripLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
Proof dependencies 1
deflate_bound_adequateRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
compress_bound_adequateRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
compress_roundtripRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
gz_roundtripRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
gz_seek_readBlocked- Input coverage
- No complete input coverage
- Evidence state
- Blocked
This record has no direct connection to another fixed target.
compress_bound_valueRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
compress2_z_first_alloc_failureRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
inflate_deferred_distanceRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
Call sequences and initialization8 targets
inflate_sequenceNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
deflate_sequenceNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
inflate_back_sequenceNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
gz_sequenceNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
inflate_initialisation_domainRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
This record has no direct connection to another fixed target.
deflate_initialisation_domainNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
inflate_back_initialisation_domainRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proof dependencies 1
gz_initialisation_domainNot completed- Input coverage
- No complete input coverage
- Evidence state
- Not completed
This record has no direct connection to another fixed target.
Other internal obligations5 targets
crc32_z_all_byte_viewsRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proofs depending on this target 1
crc32_all_byte_viewsRegistered proof- Input coverage
- All stated inputs
- Evidence state
- Registered proof
Proofs depending on this target 1
rejected_has_no_symbolsLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
This record has no direct connection to another fixed target.
step_composes_symbolsLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
This record has no direct connection to another fixed target.
symbols_exposes_stepLocal proof, not registered- Input coverage
- All stated inputs
- Evidence state
- Local proof, not registered
This record has no direct connection to another fixed target.
No matching target. Clear the filters or use a shorter name.
41 observed proof-reuse connections · 95 C-call connections. The evidence index below retains specification references and other support relationships.
Open a component, then a target, to inspect its evidence and dependencies. The evidence index retains target and proof links at recorded revision 7f4311a.
| Blocked targets | Reason and next step |
|---|---|
| gz_seek_read | Gzip seek mode |
| inflateInit2_ | Inflate initialization cleanup |
Target evidence
Proof narrative · All-target graph · Input configurations
This index contains 181 fixed targets: public execution, sequence and initialization targets, internal obligations and abstract models. There is one status graph, in progress. A model result is not implementation refinement. Input coverage and proof registration are separate. An exact local proof can cover its complete stated domain while still awaiting registration and CI. Internal premises remain part of the statement; green does not remove them. A source-only candidate never grants coverage. Disallowed axioms stop generation.
Why can an isolated node be unfinished? Its proof dependencies have not been established. Missing arrows neither prove independence nor supply a proof plan. Some Markdown viewers disable diagram links; use these ordinary source links.
Status key
Registered proof: an exact checked theorem is listed. Locally checked: an exact theorem exists but is not listed. Not proved: no exact theorem covers this target. Blocked: a documented obstacle applies to the target. These labels do not assign input coverage or replace named-commit CI acceptance.
Library queries
| Target statement | Coverage / evidence state | Contract / input range | Proof evidence | Reviewed next work |
|---|---|---|---|---|
| compressBound | All stated inputs / Registered proof | Contract; input range | ZlibF.Spec.Public.Proofs.compressBound | — |
| compressBound_z | All stated inputs / Registered proof | Contract; input range | ZlibF.Spec.Public.Proofs.compressBound_z | — |
| zlibVersion | All stated inputs / Registered proof | Contract; input range | ZlibF.Spec.Public.Proofs.zlibVersion | — |
| zlibCompileFlags | All stated inputs / Registered proof | Contract; input range | ZlibF.Spec.Public.Proofs.zlibCompileFlags | — |
| zError | All stated inputs / Registered proof | Contract; input range | ZlibF.Spec.Public.Proofs.zError | — |
| get_crc_table | All stated inputs / Registered proof | Contract; input range | ZlibF.Spec.Public.Proofs.get_crc_table | — |
Checksums
Byte-address model
Inflate streams
Fast decoder obligations
Decode-table obligations
| Target statement | Coverage / evidence state | Contract / input range | Proof evidence | Reviewed next work |
|---|---|---|---|---|
| decode_table_classifies_input | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| decode_table_matches_format | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| short_decode_table_leaf_sound | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| decode_table_leaf_sound | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| decode_table_read_preserved | All stated inputs / Locally checked | Exact target statement; input range | Zlib.Inftrees.Proofs.decode_table_read_preserved | — |
| constructor_establishes_decode_table_invariant | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| decode_table_invariant_of_prefix | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| constructor_establishes_query_stability | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| query_stability_of_prefix | All stated inputs / Locally checked | Exact target statement; input range | Zlib.Inftrees.Proofs.query_stability_of_prefix | — |
| short_rejected_leaf_stays_invalid | All stated inputs / Locally checked | Exact target statement; input range | Zlib.Inftrees.Proofs.short_rejected_leaf_stays_invalid | — |
| constructor_establishes_fast_leaf_flags | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| fast_leaf_flags_of_prefix | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| fixed_tables_have_fast_leaf_flags | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| leaf_classification_agrees | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| inflate_table_content | All stated inputs / Registered proof | Exact target statement; input range | Zlib.Inftrees.Proofs.inflate_table_content | — |
| inflate_table_decoder_safe | All stated inputs / Registered proof | Exact target statement; input range | Zlib.Inftrees.Proofs.inflate_table_decoder_safe | — |
| inflate_table_read_extent | All stated inputs / Registered proof | Exact target statement; input range | Zlib.Inftrees.Proofs.inflate_table_read_extent | — |
| constructor_root_bits | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| constructor_subtable_bits | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
Back-reference copying
| Target statement | Coverage / evidence state | Contract / input range | Proof evidence | Reviewed next work |
|---|---|---|---|---|
| output_copy_refines_lz77 | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Math.LZ77Copy.output_copy_refines_lz77 | — |
| window_copy_refines_lz77 | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Math.LZ77Copy.window_copy_refines_lz77 | — |
| copy_back_compose | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Math.LZ77History.copy_back_compose | — |
| copy_back_extends_history | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Math.LZ77History.copy_back_extends_history | — |
| retained_history_agrees | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Math.LZ77History.retained_history_agrees | — |
| window_distance_check_agrees | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Math.LZ77History.window_distance_check_agrees | — |
Deflate streams
Callback decoding
| Target statement | Coverage / evidence state | Contract / input range | Proof evidence | Reviewed next work |
|---|---|---|---|---|
| inflateBackInit_ | All stated inputs / Registered proof | Contract; input range | ZlibF.Spec.Public.InflateBackInitProof.back_init_public | — |
| inflateBack | Not proved / Not proved | Contract; input range | — | Needs: tables, window and callbacks |
| inflateBackEnd | All stated inputs / Registered proof | Contract; input range | ZlibF.Spec.Public.InflateBackEndProof.back_end_public | — |
Gzip files
Whole-buffer operations
| Target statement | Coverage / evidence state | Contract / input range | Proof evidence | Reviewed next work |
|---|---|---|---|---|
| compress2_z | Not proved / Not proved | Contract; input range | — | Needs: compressor execution |
| compress2 | Not proved / Not proved | Contract; input range | — | Needs: compressor execution |
| compress_z | Not proved / Not proved | Contract; input range | — | Needs: compressor execution |
| compress | Not proved / Not proved | Contract; input range | — | Needs: compressor execution |
| uncompress2_z | Not proved / Not proved | Contract; input range | — | Needs: decoder execution |
| uncompress2 | Not proved / Not proved | Contract; input range | — | Needs: decoder execution |
| uncompress_z | Not proved / Not proved | Contract; input range | — | Needs: decoder execution |
| uncompress | Not proved / Not proved | Contract; input range | — | Needs: decoder execution |
Format and API models
| Target statement | Coverage / evidence state | Contract / input range | Proof evidence | Reviewed next work |
|---|---|---|---|---|
| format_deterministic | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.format_deterministic | — |
| format_prefix_free | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.format_prefix_free | — |
| inflate_decodes | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.inflate_decodes | — |
| inflate_completes | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.inflate_completes | — |
| inflate_rejects_invalid | Not proved / Not proved | Exact target statement; input range | — | Prerequisites unreviewed |
| deflate_valid | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.deflate_valid | — |
| deflate_completes | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.deflate_completes | — |
| deflate_full_flush_resync | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.deflate_full_flush_resync | — |
| roundtrip | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.roundtrip | — |
| roundtrip_completes | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.roundtrip_completes | — |
| dict_roundtrip | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Spec.Api.Proofs.dict_roundtrip | — |
| header_roundtrip | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Spec.Api.Proofs.header_roundtrip | — |
| deflate_bound_adequate | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.deflate_bound_adequate | — |
| compress_bound_adequate | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.compress_bound_adequate | — |
| compress_roundtrip | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.compress_roundtrip | — |
| gz_roundtrip | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.gz_roundtrip | — |
| gz_seek_read | Not proved / Blocked | Exact target statement; input range | — Blocker: Gzip seek mode | — |
| compress_bound_value | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.compress_bound_value | — |
| compress2_z_first_alloc_failure | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.compress2_z_first_alloc_failure | — |
| inflate_deferred_distance | All stated inputs / Registered proof | Exact target statement; input range | ZlibF.Spec.Api.Proofs.inflate_deferred_distance | — |
Lifecycles and call sequences
Internal proof obligations
| Target statement | Coverage / evidence state | Contract / input range | Proof evidence | Reviewed next work |
|---|---|---|---|---|
| crc32_z_all_byte_views | All stated inputs / Registered proof | Exact target statement; input range | Zlib.Crc32.Proofs.crc32_z_all_byte_views | — |
| crc32_all_byte_views | All stated inputs / Registered proof | Exact target statement; input range | Zlib.Crc32.Proofs.crc32_all_byte_views | — |
| rejected_has_no_symbols | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Spec.Token.rejected_has_no_symbols | — |
| step_composes_symbols | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Spec.Token.step_composes_symbols | — |
| symbols_exposes_step | All stated inputs / Locally checked | Exact target statement; input range | ZlibF.Spec.Token.symbols_exposes_step | — |
Observed proof dependencies
A theorem for the destination actually uses a proof of the source target.
C function calls
The destination implementation calls the source entry. This does not require the complete source-entry contract as a proof premise.
Specification references
The destination target definition references the source target or implementation. This is not a proof dependency.
Proof support relationships
These are observed theorem references grouped by source family. Groups carry no whole-file proof status. Every direct grouped connection is retained here, including arrows reduced in the graph.
| Supporting source | Direct destinations |
|---|---|
| API-model lemmas | compress_bound_adequate, compress_roundtrip, deflate_bound_adequate, deflate_completes, deflate_full_flush_resync, deflate_valid, dict_roundtrip, gz_roundtrip, header_roundtrip, inflate_completes, inflate_decodes, inflate_deferred_distance, roundtrip, roundtrip_completes, deflateInit_, api-model proofs, deflate construction proofs |
| ByteAddress proofs | first_aligned_offset, mask_refines_base_plus_offset, pointer_advance_preserves_low_bits |
| actual_body_preserves_origin | inffast.c proofs |
| actual_distance_block_preserves_origin | inffast.c proofs |
| step_safe | inffast.c proofs |
| actual_copy_match_refines_lz77 | inffast.c proofs |
| actual_drop_preserves_origin | inffast.c proofs |
| actual_rollback_preserves_origin | inffast.c proofs |
| drop_preserves_origin | inffast.c proofs |
| pull_preserves_origin | inffast.c proofs |
| inflate_table_content | inftrees.c proofs |
| retained_history_agrees | format proofs |
| deflate_valid | api-model proofs |
| inflate_completes | api-model proofs |
| inflate_decodes | api-model proofs |
| inflateBackInit_ | public entry composition |
| adler32.c proofs | inflateSetDictionary, inflate entry composition, inflate storage and bit proofs, public entry composition |
| api-model proofs | output_copy_refines_lz77, retained_history_agrees, compress2_z_first_alloc_failure, compress_bound_adequate, compress_bound_value, compress_roundtrip, deflate_bound_adequate, deflate_completes, deflate_full_flush_resync, deflate_valid, dict_roundtrip, gz_roundtrip, header_roundtrip, inflate_completes, inflate_decodes, inflate_deferred_distance, roundtrip, roundtrip_completes, inflateCodesUsed, heap-free mathematics |
| crc32.c proofs | crc32_all_byte_views, crc32_z_all_byte_views, crc32, crc32_z, public entry composition |
| deflate construction proofs | deflateInit_ |
| deflate entry composition | deflateEnd, deflateGetDictionary, deflatePending, deflateReset, deflateResetKeep, deflateSetHeader, deflateTune, deflateUsed |
| deflate lifecycle proofs | deflateEnd, deflateGetDictionary, deflateInit_, deflatePending, deflateReset, deflateResetKeep, deflateSetHeader, deflateTune, deflateUsed, deflate construction proofs, deflate entry composition |
| deflate window and match proofs | deflate lifecycle proofs, inflate storage and bit proofs |
| format proofs | short_rejected_leaf_stays_invalid, compress_roundtrip, format_deterministic, format_prefix_free, header_roundtrip, inflate_completes, rejected_has_no_symbols, api-model proofs, heap-free mathematics, inffast.c proofs |
| gzlib.c proofs | gzclearerr, public entry composition |
| heap-free mathematics | match_array_refines_lz77, output_copy_refines_lz77, window_copy_refines_lz77, copy_back_compose, retained_history_agrees, window_distance_check_agrees, api-model proofs, inftrees.c proofs |
| infback.c proofs | inflateBackEnd, inflateBackInit_, public entry composition |
| inffast.c proofs | actual_body_preserves_origin, actual_body_refines_token, actual_fast_preserves_origin, actual_distance_block_preserves_origin, actual_distance_refines_lz77, distance_lookup_matches_format, fast_safe, step_safe, length_lookup_matches_format, actual_body_retains_selected_length, actual_copy_match_refines_lz77, match_array_refines_lz77, actual_drop_preserves_origin, actual_pull_preserves_origin, actual_rollback_preserves_origin, drop_preserves_origin, initial_origin, pull_preserves_origin, rollback_preserves_origin, output_copy_refines_lz77, heap-free mathematics |
| inflate entry composition | inflateEnd, inflateGetDictionary, inflateGetHeader, inflateInit_, inflateMark, inflatePrime, inflateReset, inflateReset2, inflateSetDictionary, inflateSyncPoint, inflateUndermine, inflateValidate, inflate_initialisation_domain |
| inflate storage and bit proofs | deflateReset, deflateResetKeep, inflateBackEnd, inflateBackInit_, inflateEnd, inflateGetDictionary, inflateInit_, inflateMark, inflateReset, inflateReset2, inflateResetKeep, inflateSetDictionary, inflateSyncPoint, inflateUndermine, inflateValidate, api-model proofs, infback.c proofs, inflate entry composition, public entry composition |
| inftrees.c proofs | decode_table_read_preserved, short_rejected_leaf_stays_invalid, inflate_table_content, inflate_table_decoder_safe, inflate_table_read_extent, heap-free mathematics |
| public entry composition | adler32_combine, adler32_combine64, adler32_z, compressBound, compressBound_z, crc32_combine, crc32_combine64, crc32_combine_gen, crc32_combine_gen64, crc32_combine_op, get_crc_table, gzbuffer, gzeof, gzerror, gzoffset, gzoffset64, gzrewind, inflateBackEnd, inflateBackInit_, inflate_back_initialisation_domain, zError, zlibVersion, adler32.c proofs |
| runtime object and arithmetic lemmas | byte_modifies_preserve_bases, byte_stores_preserve_bases, every_layout_is_representable, crc32_all_byte_views, crc32_z_all_byte_views, actual_body_preserves_origin, actual_body_refines_token, actual_fast_preserves_origin, actual_distance_block_preserves_origin, actual_distance_refines_lz77, fast_safe, step_safe, actual_body_retains_selected_length, actual_copy_match_refines_lz77, actual_pull_preserves_origin, actual_rollback_preserves_origin, inflate_table_content, inflate_table_decoder_safe, inflate_table_read_extent, compress2_z_first_alloc_failure, adler32, adler32_z, crc32, crc32_z, deflateEnd, deflateGetDictionary, deflateInit_, deflatePending, deflateReset, deflateResetKeep, deflateSetHeader, deflateTune, deflateUsed, get_crc_table, gzclearerr, gzerror, gzoffset, gzoffset64, gzrewind, inflateBackEnd, inflateBackInit_, inflateCodesUsed, inflateEnd, inflateGetDictionary, inflateGetHeader, inflateInit_, inflateMark, inflatePrime, inflateReset, inflateReset2, inflateResetKeep, inflateSetDictionary, inflateSyncPoint, inflateUndermine, inflateValidate, inflate_back_initialisation_domain, inflate_initialisation_domain, zError, zlibVersion, adler32.c proofs, api-model proofs, crc32.c proofs, deflate construction proofs, deflate entry composition, deflate lifecycle proofs, deflate window and match proofs, gzlib.c proofs, infback.c proofs, inffast.c proofs, inflate entry composition, inflate storage and bit proofs, inftrees.c proofs, public entry composition, tree construction and emission proofs, zutil.c proofs |
| specification lemmas | every_existing_heap_accepts_layout, actual_body_refines_token, distance_lookup_matches_format, length_lookup_matches_format, actual_body_retains_selected_length, drop_preserves_origin, pull_preserves_origin, rollback_preserves_origin, short_rejected_leaf_stays_invalid, inffast.c proofs |
| tree construction and emission proofs | deflate construction proofs, deflate lifecycle proofs |
| zutil.c proofs | inflate_table_content, deflate construction proofs, deflate lifecycle proofs, inflate entry composition, inflate storage and bit proofs, inftrees.c proofs |
Other registered theorems
These declarations are registered supporting execution results, lemmas or witnesses. They are not additional fixed targets and do not grant a caller coverage colour.
Refresh
Regenerate after proof or registry changes. The generator builds and inspects exact compiled theorem types. It never changes a proof, target or registry. Acceptance remains subject to checking.
Input fingerprint: 49a33d32fca62884e1eba9ca62dd3bd9d8c5fb803e7b11fa90ab23abeabd9977.
Current proof scope
The current proof scope includes default initialization, the platform-scoped fast-decoder interface and the three constructed-table content/safety/extent results. The generated index above is authoritative for exact registered and local theorem matches. These internal results do not establish the complete public inflate or deflate goals.
CI acceptance is tied to a named commit. Read the main-branch runs and checking rules; a merge or local build alone does not establish final acceptance. The platform object-size premise is an accepted environment assumption, not an outstanding scope decision.
Remaining work
Targets with red borders have a documented blocker with evidence and a next step below. A long proof attempt alone does not establish a blocker. Gray targets may be started; their missing internal lemmas and state-sequence invariants are not all drawn in the graph.
Public API proof readiness
Gray means unproved, not blocked. Start independent work now. Green callees do not establish the caller's own preconditions, loops, results or memory effects. A directly callable API can still have a false contract or a confirmed source defect; only evidence of that kind warrants a blocker border. Do not infer readiness solely from missing arrows.
The evidence index separates proof references, C calls and specification references. The work below names composition obligations, unfinished against the exact targets. It does not introduce public assumptions or grant input coverage.
Open, query and close prerequisites
Opening a file does not require the complete engine. Its main work is the common gz_open
mode loop, real allocations, string copying, descriptor effects and invariant establishment.
For a tell query, the missing producer is the position invariant over permitted histories.
For close, it is ownership over those histories, including allocation failures.
Local execution proofs now cover:
- Open entries: NULL arguments, negative descriptors and first-allocation failure. They give the unchanged file system and exact heap, including the allocation-attempt counter.
- Reader close: NULL, wrong mode and complete
unbuffered execution under
GzGood, including descriptor errors, freeing the message, path and handle, and a frame over unrelated allocations. - Priming entry: refused streams and invalid bit counts, before pending-byte compaction.
These are scoped internal results, not proofs of the complete public targets. In particular,
GzGood still has to be derived from the permitted public histories. Do not replace a gray
public node with green on the strength of one branch.
Callback decoder prerequisites
inflateBack need not wait for the complete ordinary inflate target. Setup and teardown
are already registered. Existing entry, bit-input, window-flush and stored-block arguments
can be reused. Compressed blocks and the full public callback protocol still need composition.
A fast-path theorem requiring separate output and history buffers does not cover output inside the window. A table return-code theorem does not establish installed entry contents. The callback proof guide locates the reusable arguments and states the limits of their callback domain. These missing premises do not stop independent work on another block type or error path.
Next work for every unfinished public target
"Start" means work can begin without a complete engine theorem. "Compose" names a prerequisite for full closure; independent branches can still proceed. No row grants checked status or assumes a callee's specification.
| Public targets | Proof work shown in graph | Next work and missing prerequisite |
|---|---|---|
gzopen, gzopen64, gzdopen, gz_initialisation_domain |
Start: open and cleanup | Start: common mode loop, allocation outcomes, path formatting/copy, descriptor effects, OpenState and witnesses. Entry/failure branches are locally checked above. |
gztell64, gztell |
Needs: position invariants | Compose: derive PosInv from reads, writes, seeking and pushback; then reuse the existing arithmetic execution proof. |
gzclose_r |
Needs: resource ownership | Start: initialized-buffer cleanup and its ownership producer over histories. Unbuffered execution and frame are locally checked; inflateEnd alone is insufficient. |
gzclose_w, gzclose |
Needs: flush and cleanup | Compose: actual zero-fill/final compression and file writes, all cleanup/error paths, then dispatch using both complete close results. |
gzseek64, gzseek |
Needs: seek and history | Start: position/pointer state-sequence invariants, buffered and transparent paths, exact error frames. Negative-position reachability and historical overflow reports remain unfinished. |
gzdirect, gzread, gzfread, gzgetc, gzgetc_, gzgets, gzungetc |
Needs: reader path proofs | Start: common lazy setup, transparent reads and buffer/state-sequence invariants. Compose: actual decoder execution for compressed paths, then EOF/count/pushback/error clauses. gzdirect needs detection and init, not the full data-decoding loop. |
gzwrite, gzfwrite, gzputc, gzputs, gzvprintf, gzprintf, gzflush, gzsetparams |
Needs: writer path proofs | Start: buffering, formatting, transparent writes and failures. Compose: actual compressor execution for compressed output and parameter changes. |
deflateInit2_, deflate_initialisation_domain |
Start: init and allocation | Start: parameter normalization, five allocations, all failure cleanup, actual DGood/tree establishment and witnesses. Reset proofs require the invariant; they do not establish it for fresh storage. |
deflatePrime |
Start: compaction and bits | Start: pending-byte compaction, checked shifts, bit insertion/flush and invariant/frame preservation. Refusal branches are locally checked; accepted counts remain open. |
deflateBound_z, deflateBound |
Start: bound and header review | Start: connect existing execution formulas to the saturated mathematical bound, including header strings and extra lengths. The historical extra-length report is unfinished, not a newly confirmed blocker. |
deflateSetDictionary |
Start: window and hash | Start: window fill, hash-chain insertion, saved-input restoration, then checksum and exact state/frame effects. Green checksum calls cover only that part. |
inflateCopy, deflateCopy |
Start: copy and relocation | Start: allocation failures, buffer copies, pointer relocation and independent ownership. Resolve the recorded copy/history investigations before claiming the full domain; do not add silent premises. |
deflateParams |
Needs: block flush and parameter state | Compose: actual old-block flushing, return-code handling and canonical tuning-row updates. Check exact state preservation on refusal before full closure. |
inflateSync |
Needs: scan and history | Start: compose existing first/resume scans, held bits, marker search, reset and accounting/frame results. Derive window/reset premises from histories. |
compress2_z, compress2, compress_z, compress |
Needs: compressor execution | Start: arguments, scalar lengths and cleanup. Compose: actual init/compress/end with exact output, then wrappers. Abstract roundtrip is insufficient. |
uncompress2_z, uncompress2, uncompress_z, uncompress |
Needs: decoder execution | Start: scalar results, insufficient space and cleanup. Compose: actual init/decompress/end, exact consumption/output, then wrappers. |
inflate, deflate |
Needs: dispatch invariants | Compose: decoder-table or hash-chain meaning, dispatch invariants, loop termination and output/accounting. Green checksums do not establish these premises. |
inflate_sequence, deflate_sequence, inflate_back_sequence, gz_sequence |
Needs: execution and format | Compose: actual per-call safety, history preservation, independent format refinement and completion across input/output splits. |
inflateBack |
Needs: tables, window and callbacks | Compose: compressed TABLE/LEN execution, output inside the window, public callback ownership, loop termination and exact input/output accounting. Existing stored and entry paths can progress independently. |
inflateInit2_ |
Blocked: cleanup contract | The confirmed cleanup-contract counterexample is recorded below. Successful init and independent targets can proceed. |
The immediate order is independent entry/cleanup and arithmetic paths, then common open, position and ownership invariants, then complete function composition. Callback compressed blocks can progress alongside these. Record an unknown prerequisite here with its exact question; do not invent a dependency or treat elapsed time as evidence of a blocker.
Integration
Review the focused function-manual scopes and regenerate the documentation source-policy lock in a reviewed audit update. Independently review the new source and kernel-syntax locks and the first verification baseline. Maintain repository protections for the four checks and protected-path review. Register newly checked results only after their required checks.
Public contracts
Independently approve the 103 target statements, caller domains and representation limits before accepting a verification baseline. Extend the ordinary data-epoch refinement to advanced raw dictionary replacement and all header/priming/recovery combinations; retain their exact per-entry effects and unconditional sequence safety. No final correctness claim may silently drop those obligations.
Specification review
Gzip seek mode
The abstract gz_seek_read goal is false: GzSeek permits the resulting handle
to change from read mode to write mode, so the subsequent modeled read can return no data.
The checked counterexample
uses an opened two-byte reader. Review the seek relation before proving this goal.
This is a model issue, not a confirmed zlib issue.
Inflate initialization cleanup
The current inflateInit2_ goal is false for an invalid window parameter. Its
SameObjects postcondition requires a structurally unchanged state table, but allocation
followed by free expands that table. The checked counterexample
uses a valid caller heap and proves the sizes are four and zero. Review the contract and
model before proving this goal. This is not a confirmed zlib issue.
Review the corrected shared Uncompress2 relation independently. The deferred-distance and
exact-free corrections have independent counterexamples and checked regression proofs;
implementation refinement remains open. Its former empty-output clause on memory failure and
extension clause on buffer error have been removed using the existing paired counterexample.
Complete the older abstract gz and dictionary models before using them as complete operational
refinements; the concrete public targets do not assume their callee contracts.
Translation review
Review the C language edition and implementation extensions used by the selected
build. In particular, establish definedness for reachable null-plus-zero and
null-minus-null operations. The current model permits some of them, and the
Ptr.diff source comment incorrectly attributes null subtraction to C23. The
comparison table records
the actual definitions and language references. This documentation change does
not alter the runtime or establish that a reachable upstream bug exists.
Continue the statement-by-statement review beyond the corrected compressor automatic storage. The compressor slide now checks signed subtraction in source order. Its internal-state regression compares three defined boundaries and rejects an artificial overflow in both C and Lean. Restoring unchecked subtraction changes only the overflow observation. Reachability of that artificial state is not claimed; derive the signed bound from legal call sequences. The source-level selected-depth reread in tree merging has been restored with a six-case regression and a required structural check that rejects the former cached expression. Prove the temporal initialization history of internal depth reads. Review scalar-pointer aliasing and the null-minus-null special case in compressor pointer subtraction (unfinished).
CRC address model
The CRC translation now observes a stable origin residue for every represented static or embedded byte array. Local proofs cover all residues, seeds and readable lengths for both public CRC update entries, with the same immutable-heap result. The original 47-byte static input is now a positive regression. The public contracts and caller domains are unchanged. Local evidence still needs final acceptance checks on the integrated commit.
Extend the representation relation to general ABI layout, effective types, scalar-cell aliases and byte views of other records. The current address abstraction represents only the low three bits observed by the CRC alignment test; it is not a complete address-space model.
Inflate causal model
Complete the universal output and unknown-dictionary refinement against the C. The earlier
whole-lookahead consistency is false; the supporting-bit-prefix correction is reviewed. The fixed
data-error detection lag of eight bytes also has a counterexample; derive a justified replacement
rather than raising the constant without proof. Register the checked inflate_decodes model proof,
then establish these conditions for actual decoder runs. Prove the general negative-value priming
bridge, beyond the checked model witnesses and finite execution matrix.
Differential harness
Keep the new allocation-failure and negative-prime regressions in automated validation. The test-owned gz handles, input line and deflate buffers are now released. Normal and unsuppressed sanitizer runs compare all 47,890 inputs. A cleanup mutation confirms that the harness still reports library state leaked by a missing end call.
Proof mutants
Complete the remaining legacy lists. Every newly proved public entry must supply direct translation mutants in the locked mapping and demonstrate failure in its function proof. Unproved entries acquire their records with their proofs.
Decode tables
Connect the proved canonical-code coverage and entry-shape lemmas to the heap written by
inflate_table; establish the table predicates used by the decoders.
Inflate
The internal code-length root lookup has a bounded execution result for the actual constructed table. It pulls at most one input byte, preserves the exact input cursor and bit stream, and leaves on input exhaustion. This supporting result does not complete CODELENS, the dispatch invariant or the public inflate goal. See the lookup proof and the cursor proof.
The actual window updater preserves the per-byte-object platform bound and static storage for an existing window, fresh allocation and genuine allocation failure. It uses the proved default allocator and ring copies. The platform bound is an environment premise; this theorem proves preservation through the operation. It does not complete the public inflate goal, ownership, accounting or the full caller frame. See the window proof.
The locally checked internal fast body now emits one independent literal/copy token, ends the block, or rejects an invalid length code, invalid distance code or too-far match without output. The actual distance result preserves exact remaining bits and equates copying with independent bytewise history copying. The token relation has checked composition, decomposition and rejection results against the original format grammar. Whole-fast-call bit origin also checks through the loop, byte rollback and final writeback. All these results retain the original safety conclusions.
Establish table meaning, suffix stability, compatible leaf flags and saved-window history from actual construction, installation and init. Complete whole-fast-call output composition and cover all legal buffer views. Finish the other decode modes, across-call composition, copy and recovery. These remain internal-domain results, not registered public proofs. The public inflate and sequence goals remain open.
Inflate back
Finish table construction, compressed blocks, callback composition and the complete function.
Deflate
Finish general initialization (deflateInit2_), dictionary setting, priming, copying, fill_window,
strategy loops and the complete function. The recovered dictionary-query proof builds and rejects
three translation mutants in its own proof; registration remains.
The exact Goal.deflateInit_ now has a locally checked proof in
public-deflate-init. It expands the actual fixed-parameter call at window
15, memory level 8 and strategy 0. Compression level remains arbitrary.
The proof covers version and parameter refusal, all five allocation
outcomes, failure cleanup, the old-object frame and the exact live-object
ledger. Successful execution establishes DGood; it is not a caller
premise. A concrete default caller successfully returns that invariant.
The universal deflateInit2_ theorem remains open and is not a dependency.
The complete root build, full fresh kernel replay, allowed-axiom inspection and zero-placeholder scan pass locally. Three direct wrapper mutants reject the original exact public proof in a fresh kernel. Wrong-symbol-limit and dropped-cleanup mutants retain the synchronized whole-source equality but fail their execution proofs with type errors. Resource failures are not counted. The strict entry mutation list also passes.
The exact default-entry proof and its concrete witness are registered. Generated locks add 72 semantic records and two theorem-type records. Existing semantic and theorem-type records are unchanged. Acceptance on a named CI commit remains. These are local results, not CI approval.
Trees
Actual gen_codes, leaf preparation, heap ordering, and the complete merge/root-storage
prefix have checked internal execution proofs. Node bounds and queue facts derive from the
actual descriptor/reset/scan/repair/order execution. Old heap contents, lengths and depths
remain unrestricted. Each merge executes child selection, tail stores, frequency/depth
updates, parent stores and sift-down in source order. The loop terminates and the final root
store has its exact state effect. Actual callee execution theorems are used.
The actual forest and final root store now establish the bit-length representation premises.
The complete actual build_tree executes both code-generation calls under explicit storage
and static-table conditions. The installed literal, distance and bit-length descriptors
discharge the table conditions. Every originally nonzero-frequency symbol receives a positive
limited length and its exact reversed canonical word, which fits that length. No callee
contract is assumed. The actual lengths and stored words now agree with the independent
format's canonical codes and complete-code rule. Its decoder returns each originally used
symbol and preserves every trailing bit suffix.
The constructor's exact frame preserves the caller's output invariant and existing bits. Actual construction followed by sending one used symbol composes on the same heap, with independently decodable output. Its fifteen-bit room condition is an explicit internal obligation; derive it from the block/overlay bound. Initialization and arbitrary legal call histories remain open. These are internal-state results, not a public deflate theorem.
Actual scan_tree terminates, writes its sentinel and records exact wrapping frequency
increments for every run. Actual build_bl_tree composes both scans, bit-length-tree
construction, the descending search and the unsigned cost update. Source-code words and
descriptors are preserved. Generic search returns 2..18. Actual block initialization and
source-tree construction establish the stronger 3..18 range, literal/distance count ranges
257..286 and 1..30, and all nineteen bit-length values at most seven. A new call-composition
proof retains the END_BLOCK frequency and unchanged bit-length tree through any list of valid
actual tallies that fits the current block. Actual init_block, those tallies and all three
constructors then establish the same header-field ranges on one returned heap. This proves
neither the strategy's input-to-tally history nor preservation across block flushes.
The complete actual send_tree now terminates and emits exactly the shared run-length
model. The direct-repeat loop includes its final signed decrement. All repetition branches,
the early continue, next-length reads and the final for-loop iteration execute in source
order. The exact heap frame retains both tree arrays and the existing output prefix.
Actual bit-length construction now supplies the two senders' source capacities, length
bounds and fitted words for every positively scanned symbol. Each such word also has its
independent symbol-decoding result on every suffix. These data follow on one returned heap
from actual init_block, any legal within-block tally list and all three constructors.
Exact total bit room remains an internal obligation. Finish send_all_trees, independent
run-length/header decoding and the output/symbol overlay bound; individual word decoding
does not establish decoding of the complete run-length sequence.
Three code-assignment, eleven scan/reset/repair, five heapify/descriptor, and seventeen
merge/guard/root-store mutants fail their execution proofs. Complete source equality still
checks independently for the synchronized variants. The three code-assignment mutants also
reject with the complete constructor in the build target. Three direct send_code mutations
of its length entry, code entry and emitted length fail its emission proof with the complete
build/send composition as the build target. Five scan and eight bit-length-construction
mutants fail their execution proofs while synchronized whole-function equalities still check.
Three tally mutations of the literal index, match index and full-buffer flag fail their
execution proofs while the complete source equality still checks. Eight send_tree
mutations of the repeat decrement, first-code decrement, zero-run threshold, extra-bit
width/base, continue guard, next read and final iteration fail their execution proofs.
Their complete synchronized source equalities still check. These results are not registered
or CI-approved. Finish tree-description emission, full bit-cost refinement, block compression
and the overlay bound, including the small memory levels.
Other APIs
Finish the compression utilities and the gz read/write/open paths.
End-to-end claims
Instantiate the heap API, connect the state-sequence invariant to the format model, and prove sequence safety, ownership, termination and functional correctness on the supported configurations.
Boundary cases to review
Recheck gzip extra-length arithmetic, partial-read recovery, negative-position
seeking, lost parameter changes, failed-finish recovery and forward seek after EOF
against the current pin. Conditional seek fault lemmas do not prove reachability:
establish signed-position and borrowed-pointer conditions from actual call sequences.
The inflateBack boundary-case review remains unconfirmed for that callback API;
ordinary-inflate sanitizer examples do not settle it.
The external string allocator and fixed loop fuel also need review before full
gzip ownership or arbitrary finite callback termination is claimed.
A suspected defect is not permission to exclude a public case.
Findings records evidence and confidence; current patches are in
patches/README.md. No blanket UB patch is applied.
The architecture guide records design decisions D1–D6. The safety specification defines the fresh-memory obligations.