Add Verified Bar review for zip (1cbcc1f) and cross-library path predicate check

reviews/zip/2026-11-11-bar-audit.md

@@ -0,0 +1,42 @@
+# Verified Bar Review: Proven-Commons/zip (`1cbcc1f`) and Cross-Library Path Predicate Check
+
+- **Target repository:** `Proven-Commons/zip` (commit `1cbcc1f`)
+- **Cross-checked repository:** `Proven-Commons/tar` (PR #6 `SafeEntry` / `PlainName`)
+- **Playbook standard:** `playbook/verified-bar.md` (Verified Bar v2)
+- **Date:** 2026-11-11
+- **Verdict:** Keep `status = "in-progress"` until `Z-F1` through `Z-F5` are resolved.
+
+## Summary
+
+`Proven-Commons/zip` at `1cbcc1f` proves pure parsing and encoding round-trip lemmas (`parseArchive`, `encode`, `extractSafe`, `gate_sound`) with zero `sorry` and clean standard axioms. Five specification and extraction-boundary gaps remain before `gate_sound` can guarantee safe archive extraction across POSIX and language-runtime extractors. Each finding below was verified (`VERIFIED`) on concrete binary ZIP test archives in Python 3.11 (`zipfile`) against the exact Lean 4 predicates in `Zip/Safe.lean` and `Zip/Parse.lean`.
+
+## Findings
+
+### Z-F1 (High, VERIFIED): Embedded `0x00` NUL-byte parser differential in `SafeName` (affects `zip` `1cbcc1f` and `tar` PR #6 `PlainName`)
+
+- **Location:** `Zip/Safe.lean` (`SafeName`, `gate`, `gate_sound`) and `Proven-Commons/tar` PR #6 (`PlainName`).
+- **Mechanism:** In Lean 4, `String.fromUTF8?` decodes `0x00` to `Char.ofNat 0` (`U+0000`). A 13-byte filename `safe.txt\x00evil` decodes to a 13-character Lean `String` and satisfies `SafeName` (`s != ""`, `!s.startsWith "/"`, no `"."` or `".."` in `s.splitOn "/"`, and `'\\' not-in s.toList`).
+- **Differential behavior:** Python 3.11 `zipfile.ZipFile.namelist()` and C/POSIX `open(2)` truncate at `0x00`, resolving `"safe.txt"`, whereas length-prefixed writers see all 13 bytes. Furthermore, an archive containing both `"safe.txt"` and `"safe.txt\x00evil"` satisfies Lean's `Nodup` check while colliding on `"safe.txt"` in C/Python extractors.
+- **Required fix:** Strengthen `Zip.SafeName` and `Tar.PlainName` to reject `0x00..0x1F` and `0x7F` (`c.val >= 0x20 && c.val != 0x7F`).
+
+### Z-F2 (Medium, PROVEN): `gate_sound` omits `'/' not-in c.toList` on split path components
+
+- **Location:** `Zip/Safe.lean` (`gate_sound`).
+- **Required fix:** Prove a `splitOn_char_mem_ne` lemma showing `'/' not-in c.toList` for every `c in s.splitOn "/"` and include that conjunct in `gate_sound`.
+
+### Z-F3 (High, VERIFIED): UNIX `S_IFLNK` symlink attributes in Central Directory headers are ignored
+
+- **Location:** `Zip/Parse.lean` and `Zip/Safe.lean`.
+- **Mechanism:** Central Directory headers carry `versionMadeBy` and `externalFileAttributes` (upper 16 bits = POSIX `st_mode`, e.g., `0o120777 << 16` for a symbolic link). `Parse.lean` ignores file mode, allowing a symlink entry named `"link"` with target bytes `"/etc/hosts"` to pass `SafeName`.
+- **Required fix:** Parse `versionMadeBy` and `externalFileAttributes`, classify `EntryKind`, and restrict `SafeEntry` to regular files and directories (matching `Tar` PR #6's `typeflag` check).
+
+### Z-F4 (High, VERIFIED): Non-disjoint `localOffset` entries allow overlapping-extent amplification
+
+- **Location:** `Zip/Parse.lean` (`parseArchive`).
+- **Mechanism:** Multiple Central Directory headers in a 188-byte archive can all set `localOffset = 0` and read the same Local File Header and payload slice, multiplying extracted bytes `N`-fold without enlarging the archive payload.
+- **Required fix:** Require pairwise disjoint byte intervals `[localOffset_i, dataEnd_i)` in `SafeArchive` plus an explicit total uncompressed byte budget.
+
+### Z-F5 (Medium, VERIFIED): `Main.lean` CLI wrapper sits outside `[spec].code`
+
+- **Location:** `Main.lean` and `bar.toml`.
+- **Required fix:** Move CLI argument dispatch into a pure function `Zip.runCli` inside `Zip` so `Main.lean` is a minimal I/O shell.