[ahrazzle]

Stacked on #2. Merge the containment change first, then retarget this PR to main.

The audit (Proven-Commons/mission#1, F2–F4) found that GNU/pax metadata could silently change filenames, an invalid UTF-8 name or prefix could be lost, and contiguous files were skipped. The reader now rejects unsupported metadata and invalid path fields before either CLI command prints any entries, and extracts typeflag 7 as a data file.

The supported subset is explicit: exact POSIX ustar magic/version, supported typeflags, no payload for non-data entries, block alignment, two end blocks, and only zero trailing record padding. Ambiguous legacy NUL-type directory names are rejected. The header writer rejects values this subset cannot represent. These are intentional compatibility restrictions, documented in the new draft SPEC.md; it still needs independent review.

Proofs and differential tests runs on pull requests and main, with read-only permissions, pinned actions and an installer verified by SHA-256. It builds, runs the regressions and differential tests, checks theorem axioms, and runs the normal sandboxed lake check --paranoid. It retains the generated report and fails if its sandbox cannot start. Branch protection must separately require this check.

Local validation on Lean 4.35.0 and Python 3.12.14:

• 2,641/2,641 checks pass. The new campaign compares 517 accepted archives (1,887 entries) with Python tarfile and rejects 783 archives with exit 1 and no stdout. Every archive checks both list and manifest.
• All 256 typeflag bytes, GNU/pax metadata, invalid UTF-8 in either or both fields, contiguous files, invalid later entries, incomplete trailers, header writing, and UTF-8 decoding are covered.
• Parser seed 20261025: 512 valid random archives and 512 mutated invalid archives. Existing path regressions, create/readback tests, and standard-axiom checks also pass.
• sh -n .github/scripts/setup-lean.sh and git diff --check pass.

GitHub CI run 40165364383 also passed all 2,641 checks and the normal sandboxed lake check --paranoid: all six kernels accepted the exported project, using only Classical.choice, propext, and Quot.sound. The generated test report is attached to the run as tar-test-results.

The parser and writer remain tested rather than proved. This PR supplies neither independent specification approval nor a completed verified-bar assessment.

[ahrazzle]

This PR is part of Set A: #1 → #2 → #3. It competes with #5 and #6 in Set B (#4 → #5 → #6): #5 fixes audit findings F2 to F4 in the same files, and #6 adds a different CI check. Only one set can merge. The choice is tracked in #7.

---

Generated by Claude Code

[ahrazzle]

Head sha: 511465a

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 11 files, with 417 lines added and 27 lines removed. Its
base is the PR 2 branch, so it is stacked on PR 2. At the time of this
reading, the API reported it as not a draft and as mergeable with a clean
state.

The parser contract is now explicit in a new draft SPEC.md. The SPEC
states its own status as draft and awaiting independent specification
review. It states that it is not an approval record and does not establish
the verified bar. That matches the body.

The supported subset is narrow and is stated in both the SPEC and the
code. Magic must be exactly ustar with NUL, and version must be exactly
00. Supported types are NUL, 0, and 7 as data files, and 1 to 6 as
zero-size non-data entries. Every other type rejects the whole archive.
That includes GNU longname and longlink, pax headers, and sparse
extension types.

Several whole-archive rejection rules appear in the diff. A non-data
entry with a payload is rejected. Invalid UTF-8 in either path field is
rejected. Input length must be a multiple of 512. The archive must end
with two zero blocks, and only zero padding may follow the first end
block. A NUL-type entry whose full name ends with a slash is rejected.

Typeflag 7 changes status in this PR. Archive.lean now treats 7 as a data
type through isRegularType. That matches the body claim that contiguous
files are now extracted as data files.

The header writer mirrors the reader restrictions. BuildBlock rejects
unsupported types, non-data entries with payloads, embedded NUL in a
name, and ambiguous NUL-type directory names. Lean regression guards in
HeaderSafety.lean cover those cases, including a guard for type 7 and a
guard for type x.

The no-partial-output claim has code support in the test file. The
parser_cases rejected helper runs both list and manifest for each
rejected case and checks exit code 1 with empty stdout. The SPEC states
that list and manifest parse the whole archive before printing entries.

Test counts in the committed report match the body. The report records
2641 checks and 0 failures. It records 517 accepted archives with 1887
entries, and 783 rejected archives with no output. It records parser seed
20261025, with 512 random valid archives and 512 mutated archives. It
records coverage of all 256 typeflag bytes.

No sorry or admit token appears in the added Lean lines in this diff.
The only axiom wording in the added lines is the CI step name about the
axiom allowlist. The parser and writer remain tested rather than proved,
and the body and the SPEC both state that limit.

The CI workflow is new and is scoped in the file itself. It runs on pull
requests, on pushes to main, and on manual dispatch. It uses read-only
contents permission. It pins checkout, setup-python, and upload-artifact
to commit hashes. The Lean installer script checks a SHA-256 hash. The
steps run the test script and then the normal sandboxed lake check. The
test report is saved as an artifact, with an error if no file is found.

Branch protection is a separate setting, and the body and the SPEC both
say so. The workflow file alone does not set branch protection. The body
also states that the workflow needs a separate branch protection setting
to be required.

The body cites a CI run that passed the same counts and the sandboxed
lake check. This reading review did not open that CI run, so that claim
is recorded here as a body claim, not as a checked result.

The SPEC also states limits that narrow the contract. Header mode,
owner, timestamps, device fields, and link targets are ignored. Payload
padding need not be zero. CLI output is a textual view, not an escaped
wire format, and names with tabs or line breaks print literally.

Context on competition: this PR is the third 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

Has branch protection been set to require the new workflow, or is that
still an open repository setting? The body and the SPEC note it as a
separate step.

Who is the intended independent reviewer for the draft SPEC? The SPEC
states that independent review is still outstanding.

Does the cited CI run cover the exact head sha of this PR? The body
cites run 40165364383, and this review did not open that run.

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 open the cited CI run. 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: 2641 checks, 0 failures, matching the body claim. Axioms in the record are only the standard axioms. No sorry or admit in the Lean sources. The check run on this head shows check completed with success.

This pull request is part of Set A, and it competes with Set B for findings F2 to F4 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 2.

Automated posting by agentic team with human oversight.

[orda-aska]

Main.lean:48 still prints accepted names literally. A ustar entry named a\nOK\t/etc/passwd\t1\t120\nb produces an extra OK record for /etc/passwd. The explicit textual-output limitation does not make this manifest safe for line consumers. Reject control characters or encode every printed name and validate the destination. The local suite passes 2,641 checks but misses this case.