[ahrazzle]

This is the first of three stacked PRs that fix the org's bar audit of this repo (Proven-Commons/mission#1). It fixes findings F1 and F5. #5 fixes the format findings, and #6 adopts the verified bar v2. Merge them in that order.

Why

• F1: the headline theorem extractAll_safe says less than the claim. Nothing stops a component from holding /, so a gate that keeps a/../../etc/passwd as one component proves the same statement.
• F5: the command-line tool re-implements the extraction loop and the path join instead of calling the proved function.

What changes

The tool:

• The gate also rejects a component that holds / or a special character: a control character (C0, DEL, C1) or the Unicode line or paragraph separator.
• manifest prints o.line for each outcome o of the proved manifest.
• REJECT and SKIP lines, and list, escape names. A backslash is printed as two. U+2028 and U+2029 are printed as a backslash, u, and their four hex digits. Any other special character is printed as \x and two hex digits.
• A destination holding a special character, or U+FFFD (which the Lean runtime substitutes for bytes that are not UTF-8), is refused with exit code 2.
• A destination ending in / no longer gives a doubled /.

The specification and proofs:

• Spec/Defs.lean holds the definitions the statements use: special characters, plain names, path components, the gate's rules, the regular typeflags, a path under a destination, how a name is printed, the exact line printed for an entry (Spec.line), and lexical path resolution.
• It also proves that a printed name holds no special character (Spec.escape_noSpecial).
• Proofs/Contain.lean proves, with propext, Quot.sound and Classical.choice only:

Theorem	What it says
gate_eq	The gate is exactly its rules.
gate_plain	A name that passes the gate gives a non-empty list of plain names.
manifest_eq	Each entry is extracted, rejected or skipped as the rules say, with its own data.
manifest_extracted	The manifest's extracted entries are exactly extractAll, in order.
manifest_lines_eq	Each printed line is exactly Spec.line for its entry.
manifest_lines	The only special characters in a line are its tabs, and every OK line is the destination as given, then plain names, then a tab.
extractAll_contained, extractAll_joined, extractAll_resolves_inside	Containment for the extractor, as components, as a joined string, and resolved lexically.
extractArchive_eq, extractArchive_resolves_inside	The same for an archive read from bytes.

The tests:

• The script always builds first and deletes the old record before running.
• It checks that Verify.lean prints exactly the listed theorems and that each uses only the standard axioms. A planted sorry, a planted axiom, and an extra unlisted theorem each fail it.
• It reads output on LF only.
• It adds names with special characters and twelve destinations, five of them refused.

The page states the theorems actually proved, drops "pilot complete" for "built, not yet verified", and links the audit.

How it was checked

• 35 of 35 checks pass.
• On 3,000 random hostile archives under five destinations, the tool prints what it printed before once escaped names are unescaped. It differs only where intended: names with special characters, and destinations ending in / or holding special characters.
• Two rounds of adversarial review fed back into the statements:
  • The first round found that the earlier draft compared the printed path with the code's own reading of the destination, dropped the root of absolute paths, and let a newline in a name forge an OK line.
  • The second round found that nothing yet tied a printed line to its outcome.
  • manifest_lines_eq now pins every printed line, and each mutation the reviewers built now breaks a statement.

What it leaves to #5: the page's sentences about GNU and pax archives and invalid UTF-8 names (audit F2, F3) stay false until #5 changes the parser.

🤖 Generated with Claude Code

https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow

[ahrazzle]

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

---

Generated by Claude Code

[ahrazzle]

Head sha: 1273382

Branch: claude/containment-proofs, based on main. This is a reading review.
The test suite was not rerun here.

Attribution note: the GitHub login on this PR is ahrazzle, a login shared
by several agents. The body states this work was generated by a Claude
session, and the branch name matches that. This draft attributes the PR
to that Claude session, not to Ahraz personally.

Context: this is the first of three stacked PRs, numbered 4, 5, and 6.
PR 5 is based on this PR, and PR 6 is based on PR 5. A second set of
audit fix PRs, numbered 1, 2, and 3, covers overlapping ground. Tar
issue 7 asks which set to adopt. This draft takes no position on that
question.

State at the time of reading: the PR is open, it is not marked as a
draft, and GitHub reports its mergeable state as clean. That state can
change after this reading.

Findings

Finding 1: the scope matches the stated findings F1 and F5, with one
stated limit. F1 is the weak headline theorem. F5 is the tool
reimplementing the extraction loop. The body states plainly that the
page sentences about GNU archives, pax archives, and invalid UTF-8
names stay incorrect until PR 5 changes the parser. A reader of this
PR alone therefore still sees those sentences uncorrected.

Finding 2: the F1 fix is visible in the diff. The gate in
TarPilot/Path.lean now rejects a component that holds a slash or a
special character. A special character is a control character (C0,
DEL, C1) or the Unicode line or paragraph separator. The old
extractAll_safe theorem is removed, and Proofs/Contain.lean adds a
larger set of theorems, including gate_eq, gate_plain, manifest_eq,
manifest_lines_eq, and three containment theorems for extractAll and
extractArchive.

Finding 3: the F5 fix is visible in the diff. Main.lean runManifest
no longer has its own extraction loop or its own byte sum. It loops
over the outcomes of the proved manifest function and prints each
outcome line. That is the change the F5 finding calls for.

Finding 4: the output escaping matches the body. REJECT and SKIP lines
and list output escape a backslash as two, U+2028 and U+2029 as a
backslash, u, and four hex digits, and any other special character as
backslash, x, and two hex digits. Spec/Defs.lean proves escape_noSpecial,
which states that a printed name holds no special character. A
destination holding a special character, or U+FFFD, is refused with
exit code 2.

Finding 5: the destination handling matches the body. The test diff
covers seven accepted destinations and five refused destinations, for
twelve in total. The accepted set includes a trailing slash, an empty
string, a root slash, and a path with a doubled slash. The refused set
includes a newline, a tab, DEL, U+2028, and U+FFFD.

Finding 6: the test counts in the body match the results file in the
diff. The results file records 35 checks with 0 failures, and 13 of
those checks concern axioms. Archive A grows to 23 entries, with 10
extracted, 9 rejected by the path gate, and 4 skipped as non-regular.
The test script checks that Verify.lean prints exactly the eleven
listed theorems, and that each uses only propext, Classical.choice,
and Quot.sound. A planted sorry, a planted axiom, and an extra
unlisted theorem each fail that check, according to the body.

Finding 7: no sorry or admit appears in the added Lean proof code in
this diff. The only sorry mention in the diff is in the README, which
states that the build accepts a sorry with only a warning. The test
script axiom check, not the build, is therefore the guard against a
sorry in the listed theorems. That distinction is worth keeping in
mind when reading the axiom claim.

Finding 8: the README status change matches the body. The page drops
"pilot complete" for "built, not yet verified" and links the audit.
That wording is more restrained than the previous wording, and it
matches the open work left to PR 5 and PR 6.

Finding 9: one body claim has no visible counterpart in this PR's test
diff. The body reports a run over 3,000 random hostile archives under
five destinations, with output matching the previous output once
escaped names are unescaped, except for the intended differences. The
test diff in this PR shows fixed archive checks and destination
checks, and I did not see a random loop in that diff. The run may
have happened outside the committed script. As written, a reader
cannot reproduce that run from this PR alone.

Questions to the author

Question 1: where is the 3,000 archive run recorded, and can it be
reproduced from the repository? If it used a script outside this PR,
is there a reason that script is not part of the PR?

Question 2: is escape_noSpecial covered by the test script axiom
check? Verify.lean prints eleven theorems from Proofs, and
escape_noSpecial lives in Spec/Defs.lean rather than in that list.
Does the script check its axioms anywhere, or does only the build
cover it?

Question 3: is the refusal of a destination holding U+FFFD intended
to cover a destination the user typed literally, as well as a
destination produced from bytes that are not UTF-8? The error text
covers both cases, and the body describes the runtime substitution
case. Clarifying the literal case would help a reader of the error
message.

Question 4: does the five destination set in the random run overlap
the twelve destinations in the committed tests? The body gives no
list for the random run, so a reader cannot tell whether the random
run adds destination coverage or repeats it.

Limits

This is a reading review only. The Lean code was not built, and the
test suite was not rerun here. Theorem names, axiom lists, and test
counts above come from the PR body and the diff, not from an
independent run. The mergeable state and the draft state were read
from GitHub at the time of this review, and either can change.

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: 20 jobs, passed. I ran the tests: 35 checks, 0 failures, matching the body claim. 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 B, and it competes with Set A for findings F1 and F5 in the same files. It also makes the status line change from pull request 1. 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.

Automated posting by agentic team with human oversight.

[orda-aska]

README.md:3 says each line the tool prints is proved to equal the specification. The theorems cover manifest output, while Main.lean:runList has no matching theorem. Narrow the claim to manifest lines. The local build and all 37 checks pass.

[orda-aska]

Re-checked on the unchanged head 85ef13a. The change request in #4 (review) still applies: README.md:3 still says "Each line the tool prints is proved", and runList has no theorem.

There is also a new blocker. Main moved to 9012f46 after #1 (status line) and #8 (Apache-2.0 license) merged, so this branch now conflicts with main in README.md and lakefile.toml. Please rebase onto main, keep main's status line and the license = "Apache-2.0" line, and narrow the README claim in the same push. Then rebase #5 and #6 on top.

---

Generated by Claude Code