lean-zip

Standard claim/branch/verify/publish workflow for pod agent sessions. Read this skill at the start of any feature, review, summarize, or meditate session.

Produce before/after native speed-vs-ratio comparison graphs (against the other-language curves), post them to the PR, and show them to Kim BEFORE merging. PROACTIVELY REQUIRED for any lean-zip performance PR (perf:/runtime/throughput change to compress or decode): the moment such a PR goes green, invoke this YOURSELF without being asked — generating and posting the graphs is part of finishing the PR, never a step that waits for Kim to request it. Do not report the PR as done, and do not merely offer to "produce them if she wants", until the graphs are generated and posted; only the merge itself waits for her go-ahead. Most interesting for compression changes.

Use when fixing merge conflicts on agent PRs, rebasing stale branches, or deciding whether to salvage vs. redo a PR. Also use when a rebase/fix-PR plan issue is claimed.

Use when adding a new concrete-shape closed-form rung to a checksum ladder — Adler-32, CRC32, or any future checksum with a Spec/Native split (e.g. XxHash). Covers the three-part Spec identity → Native bridge → public wrapper template, the hypothesis-bearing invariant pattern, `@[simp]` and visibility discipline, and the boundary where the template stops applying (non-Nat algebra).

Use when writing a test that must match an error message thrown by lean-zip — bomb-limit tests, malformed-archive assertThrows, CD/LH consistency assertions, or any `.toBaseIO` + `msg.contains` block. Tabulates the error-substring families so you pick the right match string the first time.

Use when landing a PR that closes a numbered item in `SECURITY_INVENTORY.md` *Recommended policy* or *Missing work*, or when threading a new parameter through public APIs with a deferred default flip. Covers the *Executed past-tense one-liner* phrasing and when to use the half-closed two-step.

Use when Lean 4 proofs involve ByteArray, Array, List indexing, getElem, length lemmas, take/drop, or roundtrip proofs over byte collections.

Use when proving that Lean 4 functions preserve existing bytes (prefix/content preservation), compose getElem_lt proofs through recursive structures, prove append-only buffer invariants, or characterize what new bytes a function produces (raw extract, RLE all-equal, element-wise correspondence).

Use when Lean 4 gives "motive is not type correct", max recursion on List.ofFn, rewriting fails due to dependent types, or cross-file visibility issues with private/protected.

Use when Lean 4 proofs involve fuel-based recursion, proving fuel independence, loop invariants, copyLoop-style patterns, suffix/append extension lemmas, or maxRecDepth/maxHeartbeats tuning.

Use when working on Lean 4 proofs involving Option or Except monad, do-notation unfolding, guard patterns, bind handling, join points, forIn loops in specifications, or Id monad loop invariants (Id.run do with for loops).

Use when proving parsing completeness theorems — that a parsing function returns .ok when given well-formed input, or that spec-level success implies native success. Also use when proving position bounds, eliminator lemmas, or chaining monadic parsing steps in Except/Option.

Use when proving encode/decode roundtrip theorems, suffix invariance (_append lemmas), goR (decode-with-remaining) patterns, padding extraction, or composing per-level roundtrip proofs into a unified theorem.

Use when simp only fails unexpectedly in Lean 4, or when dealing with Bool vs Prop conditions, filter+lambda, let bindings in omega, linter false positives, or hypothesis normalization mismatches.

Use when Lean 4 proofs involve UInt8/UInt16/UInt32/BitVec conversions, bv_decide, or bridging between numeric types and Nat.

Use when Lean 4 proofs involve well-founded recursion, termination_by, f.induct functional induction, unfolding WF functions, or converting fuel-based functions to WF recursion.

Use when implementing Zstd (RFC 8878) decompression features, including FSE table construction, backward bitstream reading, sequence execution, Huffman decoding, or compression mode parsing. Also use when adding tests for Zstd features.

Use when creating or extending Zstd specification files in Zip/Spec/ (Fse.lean, Zstd.lean, ZstdHuffman.lean, ZstdSequence.lean, ZstdFrame.lean). Covers file structure, naming conventions, predicate/Decidable design, position-advancement theorems, table-validity composition, two-block matrix, and frame-level lifting.

Use when authoring new malformed-archive regression fixtures for lean-zip — tar malformed PAX/GNU fixtures, tar symlink/hardlink archive-slip fixtures, or malformed ZIP fixtures under testdata/{tar,zip}/malformed/ or testdata/tar/security/. Covers the fixture-builder script shape, size budgets, determinism checklist, and assertion-writing patterns.

Standard PR-repair workflow for pod `repair` agent sessions. Covers claim/diagnose/fix/verify/push lifecycle and the fix-or-abandon principle.

Use when reviewing Lean proof quality, cleaning up proofs after getting them to work, or performing a review session on a proof file. Also use when the review command targets a Lean file.

Use when converting `]!` runtime bounds checks to proven-bounds `]` access in Lean 4. Covers guard capture, omega proofs, caller propagation, loop bound capture, and common pitfalls.

Use when executing a summarize-wave PR — covers the post-issue-creation tail deferral pattern (PRs that land between the planner's issue creation and the wave block's submission stay out of wave scope and roll into the next wave). Sibling skill to `agent-worker-flow` (which covers the generic claim/branch/verify/publish lifecycle) and `inventory-reconciliation` (which shares the issue-body-as-source-of-truth invariant via its *Half-closed two-step* section).

Create or update Claude Code skills. Use when creating a new SKILL.md, updating an existing skill, or when the meditate command asks you to write skills.