refactor: strip lean-zip to the verified DEFLATE core - #2893
Merged
Conversation
Split the monorepo into four repositories (everything removed here is preserved at the pre-split tag): - the zlib FFI bindings move to kim-em/lean-zlib - the tar/ZIP archive layer moves to kim-em/lean-archive - the benchmark dashboard and comparator harness move to kim-em/lean-zip-benchmark (frozen at the August 2026 refresh) - process artifacts (PLAN.md, PROGRESS.md, progress/, plans/, SECURITY_INVENTORY.md, agent-harness skills/commands, video drafts) are deleted from HEAD What remains is the pure-Lean verified codec: Zip/Native/, Zip/Spec/, the four stopgap C primitives, and the native test suite. The library now builds with no system C dependencies; the native-vs-zlib conformance tests (including RFC interop and the inflate fuzz harness) live in the new dev-only conformance/ sub-package, which requires lean-zlib from git — solving Lake's lack of test-only dependencies via the same pattern the bench/ sub-package used. The two hero graphs are committed as frozen artifacts under graphs/; the README's usage, requirements, and organization sections are rewritten for the reduced scope, and the four SECURITY_INVENTORY docstring citations in the core are now self-contained. Corpus-backed tests (PackedTokens, L7Adaptive, OptimalParse) read real corpora only when LEAN_ZIP_CORPORA_DIR points at a lean-zip-benchmark checkout, falling back to deterministic synthetic data. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Findings from an adversarial second-opinion review: point docstrings at lean-archive's Archive.Zip and lean-zlib's Zlib modules instead of the removed Zip.Archive / Zip/Gzip.lean / Zip/RawDeflate.lean; state explicitly that the proofs are about the C primitives' Lean reference bodies (the C is trusted to match, cross-checked by the conformance sweeps) and that these plus the runtime are the codec's trusted computing base; document level 0 and the above-10 clamp; and soften 'proofs re-checked from scratch on every commit' to what CI actually does under caching. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
'lake -R build' in conformance/ was a no-op (no default targets), so the CI build step verified nothing; mirror the old bench package's @[default_target, test_driver] annotation. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR strip the repository down to the pure-Lean verified DEFLATE codec, splitting everything else into sibling repositories. Everything removed here remains available at the pre-split tag.
This PR remove the zlib FFI bindings (now lean-zlib), the tar/ZIP archive layer (moving to lean-archive), the benchmark lab (moving to lean-zip-benchmark, dashboard frozen at the August 2026 refresh), and the process artifacts of the agent-driven development campaign (PLAN.md, PROGRESS.md, 1,131 progress files, plans/, the 557KB SECURITY_INVENTORY.md, pod skills/commands, and the video drafts).
What remains is Zip/Native/, Zip/Spec/ (~32k lines of proof, sorry-free), the four stopgap C primitives, and the native test suite — the library and its tests now build with no system C dependencies (CI's main job installs nothing but elan). The native-vs-zlib conformance suite, RFC-interop checks, and the inflate fuzz harness move to a new dev-only
conformance/sub-package that requires lean-zlib from git, using the same pattern the oldbench/sub-package used to keep test-only dependencies out of the shipped library. The two hero graphs are committed as frozen artifacts undergraphs/, the README is rewritten for the reduced scope, and corpus-backed tests fall back to deterministic synthetic data unlessLEAN_ZIP_CORPORA_DIRpoints at a corpora checkout.Verified locally:
lake build && lake testgreen on a bare shell with no zlib;lake -d conformance build && lake -d conformance testgreen under nix-shell; sorry count 0.🤖 Prepared with Claude Code