liblzma lzma_decode proving — per-case proving progress

Cases closed (main lemma Qed, zero admits): 20 / 23 · lane case pages: mlbittree · eopm · rlbittree

mlbittree:stopped eopm:stopped rlbittree:stopped

Recent campaign commits (den/lzma-decode)

9733b9fc ldb_e_rlbittree DEN session 16: ALL THREE mega-SEP RA_return refolds PROVEN (admit 6 -> 3; every remaining admit = the result-2 GATE-COPY-B Copy-guard, blocked on the orchestrator INV/PRE change): Low (L35365-35868) + Mid (L38042-38545) ported from the twin's proven in-file blocks, High (L40692-41188) from a snapshot of their splice-ready high_draft.v, via the mechanical pipeline (matchlen<->replen biswaps, seq_toZ 8->21, twin H69-H84 -> our Hk_* pins with H55-H68 number-identical, Hlcl_a-family -> *_init seeds, Hreach -> H29, in-block Hml_a comp-3 alias seed, "length_decoder_rep at 2" -> "at 3" struct-order flip) + two live-discovered deltas: the decoder_alias_coherent live disjunct moves conjunct 3 -> 4 (our RepLen arm; Low left / Mid right-left / High right-right + seqZ_in_iff), and the High-only residual frame closed by rewrite Haddr_high + the definitional probs_alias_address -> field_address0 change before cancel. Pipeline scripts + donor snapshots + .bak backups in scratchpad/. (verified errors:[] through 0-idx L38560 and L41210 covering ALL edits; tail byte-identical shifted session-15 green text; whole-file receipt still infrastructure-blocked per mcp-problems.md, file now 42591 lines; admit=3)
c639c22f ldb_e_rlbittree DEN session 16 CHECKPOINT: Low + Mid mega-SEP RA_return refolds PROVEN (admits 6 -> 4): ported the twin's proven Low/Mid refold blocks with the name pipeline (H69-H84 -> Hk_* pins, Hlcl_a-family -> *_init seeds, Hreach -> H29, matchlen<->replen biswap, seq_toZ 8 -> 21, "length_decoder_rep at 2" -> "at 3" occurrence flip for our struct order) + the alias-coherent live-disjunct move (conjunct 3 -> 4 = our RepLen arm) + in-block Hml_a comp-3 seed replacing their in-block Hrl_a comp-4 (ours is top-level). Low block new L35365-35868, Mid new L38042-38545. Verified errors:[] through L38560 (0-based, warm) covering ALL edits; tail byte-identical to session-15 committed green text (admit=4: 3 result-2 Copy-guards + High refold at L40692)
142f89b7 ldb_e_mlbittree DEN session 13: fuel-bound helper Admitted CLOSED -- decode_loop_reaches_fuel_input_dict_bound (old L16141, used at 3 main-proof sites) now Qed via verbatim port of the ldb_nested_proof.v measure-termination infrastructure L16120-18045 (seq_dist/decode_measure/measure_decrease sweep/fuel_measure_le/GUARDED_PROTO/seq_len_pos preservation, ~1926 lines, all Qed), closed with the _GUARDED body; one byte-identical duplicate rc_normalize_safe_preserves_df_dict deduped at its later site; the two remaining helper Admitted (range upper-bound one-steps, now L20433/L24889) established FALSE-as-stated (unclamped probability.type := Z; isrep1 L18505 concurs) with zero main-proof consumers -- protocol result-2 fix options (delete, or isrep1 R4.4 restatement + rc_range_ub sweep port) documented in handoff for orchestrator decision (verified errors:[] capped through L25501 covering all session edits, text below byte-identical modulo +1922 line shift to session-12 green-provenance text; whole-file receipt still blocked by box ceiling; admit=0 in-body, Admitted=3: 2 result-2 blocked + terminal receipt)
911b5c63 ldb_e_mlbittree DEN session 12: High-leg splice VERIFIED GREEN -- capped rocq_compile_lsp COMPLETED errors:[] through L41072 (1-based) in a live 50min cold elaboration (co-tenant window at 23GB held), covering the ENTIRE spliced High region L40264-41072; single error found+fixed: post-cancel residual = high prob_array_rep address-spelling mismatch (field_address0 3-step path vs nested field_address from length_decoder_rep), closed via rewrite Haddr_high + definitional change to field_address0 + derives_refl (validated live, goals:[]); prefix L1-40263 and tail byte-identical to green-provenance text (verified offline vs 4ae4de1). Main proof body now has ZERO admit tactics; main lemma closer remains Admitted pending whole-file check (our lsp at 47.7GB vs 49.1GB watchdog after the run) (admit=0 in-body; capped-verified errors:[] through L41072)
2f75da0c ldb_e_rlbittree DEN session 15: PAUSE Phases 1-7 C-side COMPLETE at ALL THREE legs + PROP#3 limit-validity PROVEN (pause residual = mega-SEP refold only): ported the twin's in-progress Low-leg template with our-name deltas (guard rename Hne_uc before clear - H H0 H1 H4; temps _t'52/53/54 -> _t'135/136/137 cross-order) -- Phase 1 five forwards + rewrite Hoieq; Phase 2 freeze[27]/BRK forward_loop with samebase-tc + sem_sub_pp break bullets; Phase 3 do-11-forward thaw; Phase 4 UCP forward_if with dead {4,15,22} chain (seq=21); Phase 5 Hretok_n dead ret==1 + Sreturn Exists with Hmodel_eq; PROP#3 proven via mftrue_* Qed helpers + Phase-0-style free-cap (litmatch2 Hdl_free_eq replaced). THE BLOCK IS LEG-INDEPENDENT: Mid = byte-copy; High = 2 deltas (no-wand freeze shift, UCP 41->40). admit 6 = 3 mega-SEP refolds + 3 result-2 Copy-guards (verified errors:[] through L39760 covering ALL edits (end L39745); whole-file EOF receipt UNOBTAINABLE this session -- file now busts the 49GB box ceiling SOLO at ~L41060, best run error-free through the terminal Admitted., killed at the receipt; see mcp-problems.md 2026-07-19; admit=6)
db2f68c0 ldb_e_mlbittree DEN session 11: wrapper checkpoint