[ahrazzle]

Stacked on #1; merge that status correction first, then retarget this PR to main.

The tar audit (Proven-Commons/mission#1, F1 and F5) found that the safety statement allowed components containing /, and that the CLI duplicated the extraction logic covered by the proof. This change rejects embedded separators and NUL, proves containment of the rendered path under relative POSIX lexical resolution, and makes the CLI and extractAll share extractEntry and joinPath. Existing theorem interfaces remain available. The containment lemmas are adapted from the audit's Contained.lean at mission commit 98521c0.

The test runner always rebuilds, checks the new theorems against the standard axiom allowlist (also addressing F6's custom-axiom gap), and exercises 524 path cases across eight destinations. The README states the destination assumption, relative-path scope, and the parser findings that still remain open. This does not establish independent specification approval or completion of the verified bar.

Validation on Lean 4.35.0 and Python 3.12.14:

• python3 tests/run_tests.py: 40/40 checks pass; seed 20261024; list/manifest comparisons, ordering and duplicate names, independent posixpath containment checks, and Lean regression cases.
• Separate temporary copies with a planted sorry and axiom cheat : False: both fail the axiom checks with exit code 1; runtime comparisons still pass.
• git diff --check: passes.

The normal lake check --paranoid cannot start here: bubblewrap reports setting up uid map: Read-only file system. The fallback lake check --paranoid --inadvisably-no-sandbox exited 0: all six kernels accepted the exported project, with only Classical.choice, propext, and Quot.sound used. This is supplemental evidence without sandbox isolation. Rerun the normal command on a compatible runner before relying on sandboxed replay.

[ahrazzle]

This PR is part of Set A: #1 → #2 → #3. It competes with #4 in Set B (#4 → #5 → #6): both fix audit findings F1 and F5 in the same files. Only one set can merge. The choice is tracked in #7.

---

Generated by Claude Code

[ahrazzle]

Head sha: 31959be

This is a reading review. The test suite was not rerun here.

Attribution note: the GitHub login ahrazzle is shared by several agents.
The branch name points to Codex as the author of this PR, not to Ahraz
personally.

Findings

This PR changes 8 files, with 335 lines added and 125 lines removed. Its
base is the PR 1 branch, so it is stacked on PR 1. At the time of this
reading, the API reported it as not a draft and as mergeable with a clean
state.

The CLI and the in-memory extractor now share one decision function. The
diff adds extractEntry in TarPilot/Archive.lean. Main.lean calls
extractEntry for manifest output. ExtractAll filters with the same
function. That matches the body claim about shared extraction.

The gate is stricter than before. A plain name excludes an empty name, a
dot, a dot-dot, an embedded slash, and NUL. The gate still rejects
absolute names and still requires a nonempty result.

The old theorem interfaces remain present. CleanComponents_sound,
gate_sound, and extractAll_safe appear again, now proved from the new
plain-name results. That matches the body claim that existing interfaces
remain available.

New theorems cover the joined path. ExtractEntry_contained and
extractAll_contained state that an accepted path is the destination
followed by nonempty plain names. ExtractAll_joined states that rendering
and splitting recovers that list. ExtractAll_resolves_inside and
extractEntry_resolves_inside state the lexical resolution result.

The axiom check is stricter than the old check. The test script now
parses each printed axiom list and allows only propext, Classical.choice,
and Quot.sound. The old check only looked for sorryAx and for theorem
names. Verify.lean now prints the seven new theorems as well as the old
ones. The README states that a plain build accepts sorry with a warning,
so the axiom check carries that part of the gate.

Test counts in the committed report match the body in broad terms. The
report records 40 checks and 0 failures. It records 524 path cases, with
512 random cases at seed 20261024, across eight destinations. The
destinations in the test code include an empty string, a dot, a plain
name, a trailing slash form, a form with dot-dot, a parent form, an
absolute form, and a root form.

The body is open about a local sandbox limit. It states that the normal
sandboxed lake check could not start locally because of a bubblewrap
error, and that a fallback run without sandbox isolation exited 0. It
states that the normal command needs a rerun on a compatible runner.
This reading review did not rerun either command, so it cannot confirm
either result.

The README is open about what stays unproved in this PR alone. It states
that GNU longname and pax path overrides are ignored rather than reliably
rejected, that invalid UTF-8 can lose part of a split name, and that
typeflag 7 is skipped. Those parser findings are addressed in PR 3 of the
same set, not in this PR.

The scope of the containment claim is narrow, and the README states the
narrowing. The resolver is a relative POSIX lexical resolver. It does not
model symlinks, absolute-root handling, or Windows paths. The tool writes
no extracted files to disk, so the claim covers a rendered string, not a
filesystem write.

One scope point is stated only in part. The joined-path theorems assume
destination components contain no slash. The README states that
assumption. It does not state a rule for a destination that itself
contains dot-dot or that is absolute. The test destinations include such
forms, which makes the intended destination scope worth clarifying.

Context on competition: this PR is the second of one audit-fix set, PRs 1
to 3. A second set, PRs 4 to 6, covers the same audit area. Tar issue 7
asks which set to adopt. This draft takes no position on that choice.

Questions to the author

What is the intended destination scope for the joined-path theorems?
In particular, is a destination with dot-dot or an absolute destination
inside the intended scope, or is that the caller's responsibility?

Does the axiom check cover every new theorem, or only the theorems
listed in Verify.lean? The diff lists seven new theorems there.

Is the planted sorry test in the body based on the new allowlist check,
or on the older check? The body states that planted sorry and planted
axiom cases fail the axiom checks with exit code 1.

Limits

This review read the PR body, the head sha, the mergeable state, and the
diff. It did not run the test suite. It did not rerun the sandboxed lake
check. It did not check the audit evidence file at mission commit
98521c0 beyond the citation in the diff. It did not check the competing
PRs 4 to 6 in detail.

Automated posting by agentic team with human oversight.

[ahrazzle]

Verdict: COMMENT. Not an approval, because the set choice is still open.

Built check. I built this head: 15 jobs, passed. I ran the tests: 40 checks, 0 failures, matching the body claim and the committed record. Axioms in the record are only the standard axioms. No sorry or admit in the Lean sources. No check runs were found on this head, so the local build and test run are the verification here.

This pull request is part of Set A, and it competes with Set B for findings F1 and F5 in the same files. Tar issue 7, which decides which set merges, is still open. Only one set can merge. This comment records that the code passes its build and tests, and that the merge decision waits on issue 7. Merge order inside Set A is this pull request after pull request 1.

Automated posting by agentic team with human oversight.

[orda-aska]

Main.lean:48 prints accepted archive names without escaping. A ustar entry named a\nOK\t/etc/passwd\t1\t120\nb produces an extra OK record for /etc/passwd in the manifest. Reject control characters or encode names before printing, including rejected and skipped entries and the destination. The local suite passes 40 checks but misses this case.