Issues

• perf: land the rolling lazy2 deferral at L7 (certified +0.053pp at ~+2.4% matcher; multi-session proof threading)

  kim-em/lean-zip#2837 · Filter by author kim-em opened on Jul 11, 2026
  6

• bench: re-record decode_density.json (native rows predate #2804's extendWithin win)

  enhancement
  kim-em/lean-zip#2810 · Filter by author kim-em opened on Jul 8, 2026

• perf(decode): batched refill + multi-literal decode inside the fastloop (revisit #2630/#2669)

  enhancementtrack-d
  kim-em/lean-zip#2800 · Filter by author kim-em opened on Jul 8, 2026
  1

• perf(decode): de-box the residual per-symbol guards (USize output budget + hoisted input size)

  enhancementtrack-d
  kim-em/lean-zip#2794 · Filter by author kim-em opened on Jul 8, 2026

• perf(explore): data-derived order-0 literal costs for the cheap-optimal cost model

  enhancementtrack-d
  kim-em/lean-zip#2784 · Filter by author kim-em opened on Jul 6, 2026

• perf(explore): true multi-step lazy2 deferral at L7/L8 (the untried half of #2765)

  enhancementtrack-d
  kim-em/lean-zip#2783 · Filter by author kim-em opened on Jul 6, 2026

• perf(tune): shallower lazy lookahead probe (lazyDepth = chainDepth/4 or /8) at L8

  enhancementtrack-d
  kim-em/lean-zip#2781 · Filter by author kim-em opened on Jul 6, 2026

• perf(explore): drop the hash3 singleton probe at the deep lazy levels (L7/L8)

  enhancementtrack-d
  kim-em/lean-zip#2780 · Filter by author kim-em opened on Jul 6, 2026
  1

• perf(explore): beat zopfli's DEFLATE ratio — iterative+exact-cost DP, optimal block split, post-pass re-optimization

  enhancementtrack-d
  kim-em/lean-zip#2701 · Filter by author kim-em opened on Jun 23, 2026
  

• perf(bench): add enwik8 large-text corpus + zopfli ceiling for L9 ratio evaluation

  enhancementtrack-d
  kim-em/lean-zip#2700 · Filter by author kim-em opened on Jun 23, 2026
  

• chore: migrate ByteArray.copyWithin to Lean core once lean#14158 lands

  kim-em/lean-zip#2694 · Filter by author kim-em opened on Jun 23, 2026

• perf(decode): adopt libdeflate's decoder architecture — tracking issue

  enhancement
  kim-em/lean-zip#2668 · Filter by author kim-em opened on Jun 20, 2026
  7

• perf(explore): a cheaper approximate-optimal parser for a usable L9 tier (algorithm, not retune)

  enhancement
  kim-em/lean-zip#2638 · Filter by author kim-em opened on Jun 17, 2026
  1

• perf(explore, needs lean4#14053): compress hash-load — ugetUInt32LE in hash3

  enhancement
  kim-em/lean-zip#2629 · Filter by author kim-em opened on Jun 16, 2026
  1

• test: native-inflate too-many-length/distance-symbols guard regression (numLitLen>286 / numDist>30 → exact #2586 rejection + 286/30 passing boundary; ZipTest/InflateCountGuards.lean — message-pinning complement to #2586, sibling of guard suites #2589/#2593)

  agent-planblockedfeature
  kim-em/lean-zip#2615 · Filter by author kim-em opened on Jun 13, 2026
  1

• Review: BlockSizeModel.lean BitWriter bitLength accounting foundation (landed #2605 / #2489-partial; proof-quality + spec-taxonomy audit; never dedicated-reviewed; distinct from perf audit #2611, scope-bounded against #2604)

  agent-planreview
  kim-em/lean-zip#2614 · Filter by author kim-em opened on Jun 13, 2026
  1

• Review: HuffmanEncode.lean W2b repairBl-completeness / cappedBlCount feasibility-leaf chain (landed #2566/#2579/#2595/#2602 of #2536; never dedicated-reviewed; distinct from de-boxing #2599 / LZ77Optimal #2603 / Gzip-Zlib #2606)

  agent-planreview
  kim-em/lean-zip#2613 · Filter by author kim-em opened on Jun 13, 2026
  1

• test: native gzip optional-field positive-path conformance (FEXTRA/FNAME/FCOMMENT/FHCRC valid+populated → native GzipDecode skips fields, payload==original==FFI; ZipTest/NativeGzipOptional.lean — accept-side complement to malformed fuzz #2584 / framing-reject guards #2590)

  agent-planfeature
  kim-em/lean-zip#2612 · Filter by author kim-em opened on Jun 13, 2026
  1

• Review: PR #2607/#2490 perf — pre-size packed-token array + retire UInt32-tables on measured-negative verdict (proof-quality + equivalence/retirement-soundness audit; never dedicated-reviewed; distinct from fuzz-harness audits #2588/#2609)

  agent-planreview
  kim-em/lean-zip#2611 · Filter by author kim-em opened on Jun 13, 2026
  1

• Review: audit the runDecodeFuzz / DecodeCensus structural-garbage decode census in ZipTest/FuzzInflate.lean (landed #2608/#2573) — verdict-logic soundness, native⊆FFI direction, truncation/concatenated-gzip generator correctness, determinism (sibling of #2588 which audits runDiffFuzz; disjoint function scope)

  agent-planreview
  kim-em/lean-zip#2609 · Filter by author kim-em opened on Jun 13, 2026
  1

• proof: block-byte cost models = emitted .size — counting identity + fixedBlockBytes/dynBlockBytes theorems (successor to #2489)

  agent-planblockedfeature
  kim-em/lean-zip#2604 · Filter by author kim-em opened on Jun 13, 2026
  1

• test: native-gzip concatenated-member-count cap (1000) regression — 1001 minimal members → exact 'too many concatenated members' rejection + 1000-member passing boundary (ZipTest/NativeGzip.lean; distinct from output-size cap #2577 / header-trailer fuzz #2584 / framing guards #2590)

  agent-planfeature
  kim-em/lean-zip#2594 · Filter by author kim-em opened on Jun 13, 2026
  1

• test: native-inflate Huffman-decoding-layer guard regression suite (CL repeat-at-start/exceeds-total + invalid length 286/287 / distance 30/31 codes; exact-message assertions, ZipTest/InflateHuffmanGuards.lean — distinct from block-structure #2589 and framing #2590)

  agent-planfeature
  kim-em/lean-zip#2593 · Filter by author kim-em opened on Jun 13, 2026
  1

• test: native inflate overlapping back-reference (RLE) period sweep + multi-block boundary native↔FFI conformance (deterministic distance∈{1,2,3,length-1,length,length+1} crossing fillDouble doubling thresholds; ZipTest/InflateBoundary.lean — distinct from random roundtrip #2575)

  agent-planfeature
  kim-em/lean-zip#2591 · Filter by author kim-em opened on Jun 13, 2026
  1

• test: targeted native gzip+zlib container framing/trailer-guard regression suite (bad magic / unsupported CM / FDICT / 31-check / CINFO / truncated header+trailer / CRC32+ISIZE+Adler32 mismatch; exact-message assertions, ZipTest/FramingGuards.lean — message-pinning complement to accept/reject fuzz #2584/#2585)

  agent-planfeature
  kim-em/lean-zip#2590 · Filter by author kim-em opened on Jun 13, 2026
  1