[ahrazzle]

This is the second of three stacked PRs that fix the org's bar audit (Proven-Commons/mission#1). It is based on #4; merge that first, and GitHub then retargets this one to main.

Why

The page promised that "an archive using them fails to parse instead of being read in a wrong way". That did not hold:

• F2: GNU long names were cut to 100 bytes. Pax headers were skipped, so a pax path or a non-ASCII name was ignored.
• F3: a name split over the prefix and name fields, with invalid UTF-8 in one of them, was placed under the other half.
• F4: typeflag 7 was skipped, unlike POSIX readers and Python's tarfile.

Review of this branch found more of the same kind:

• F7: GNU incremental dumps keep access and change times where ustar keeps its name prefix. The pilot, like tarfile, read them as a prefix, so GNU tar's a.txt came out as 15267276047/a.txt.
• Data after non-regular entries: the pilot skipped size bytes after links, devices, directories and FIFOs. POSIX stores no data for those, and GNU tar and tarfile read the next header straight after. So an archive could hide from the pilot a file both other readers extract.
• Names ending in /: an entry with a regular typeflag and such a name, which older archives use for a directory and GNU tar reads as one, was extracted as a file.

What changes

The parser accepts only:

• the POSIX ustar magic, or GNU's;
• a GNU header with nothing in the ustar prefix area;
• typeflags NUL and 0 to 7;
• name and prefix fields of valid UTF-8.

Anything else makes the whole archive fail to parse, as the page says. The finer rules:

• Types 1 to 6 are followed by no data, whatever their size field says.
• A regular typeflag with a name ending in / and a nonzero size fails to parse, because readers disagree on whether data follows. So does a size field of spaces, which GNU tar refuses.
• isRegular takes typeflag 7, and not a name ending in /. Spec.regularType says the same, so manifest_eq and Spec.line follow it.
• create never splits a long absolute name so that its / is lost.

The page lists exactly what the pilot does not read.

How it was checked

• 100 of 100 checks pass. They include 27 archives that must fail to parse under list and manifest, and 11 readable ones compared with tarfile.
• Among the readable ones are GNU format, GNU tar's own output, names ending in /, and each non-regular type with a nonzero size field followed by two files.
• Run against Prove containment for every line the tool prints (audit F1, F5) #4's binary, 58 of the 100 checks fail.
• The containment theorems do not depend on the parser. The proofs are unchanged except that the name is now passed to the regular-file rule.

---

Generated by Claude Code

[ahrazzle]

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

---

Generated by Claude Code

[ahrazzle]

Head sha: b18427e

Branch: claude/reject-unsupported, based on the PR 4 branch. 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 second of three stacked PRs, numbered 4, 5, and
6. The body states that PR 4 is merged first in ordering, and GitHub
then retargets this PR to main. 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, and it goes beyond
them in a stated way. The body lists F2, F3, and F4, then adds F7,
data after non-regular entries, and names ending in a slash. Each
added item is described as review finding more of the same kind. The
diff touches the parser, the regular file rule, the spec definitions,
the proofs, and the tests, which fits that scope.

Finding 2: the parser restriction matches the body. TarPilot/Header.lean
now accepts only the POSIX ustar magic or the GNU magic. A GNU header
passes only when bytes 345 to 499 are all zero, which is the area
where ustar keeps its prefix and GNU keeps times, sparse maps, and
volume offsets. That rule is the mechanism behind the F7 fix for GNU
incremental dumps, where the pilot previously read times as a prefix.

Finding 3: the typeflag rule matches the body. The new knownTypeflag
accepts NUL and 0 through 7, and nothing else. GNU long name and long
link entries, pax headers, and other types therefore fail the whole
parse. The name and prefix fields must each be valid UTF-8, where the
previous code read invalid UTF-8 as an empty string. That change is
the mechanism behind the F3 fix for a split name with invalid UTF-8
in one half.

Finding 4: the data rule for non-regular entries matches the body.
ParseBlock sets the size to zero for types 1 to 6, whatever the size
field says. The next header therefore follows straight after such an
entry. The test helper hidden_after covers this by placing a file
inside the claimed size bytes of a non-regular entry, followed by a
second file.

Finding 5: the trailing slash rule has two parts, and both are visible
in the diff. A regular typeflag with a name ending in a slash and a
nonzero size fails to parse, in parseBlock. A regular typeflag with a
name ending in a slash and a zero size is not regular, because
isRegular now also requires the name not to end in a slash. That
entry is then skipped rather than extracted.

Finding 6: the regular file rule change is small and consistent.
Spec.regularType now takes the name as well as the typeflag, and it
accepts 0, NUL, and 7, except for a name ending in a slash.
Manifest_eq and manifest_lines_eq in Proofs/Contain.lean change only
to pass the name through, including one changed rfl line. That fits
the body claim that the containment proofs are unchanged except for
passing the name to the regular file rule.

Finding 7: the create fix matches the body. Header.splitUstarName now
requires both parts of a split to be non-empty. A long absolute name
therefore keeps its leading slash instead of losing it in the split.
The test diff adds a case where a 101 character name with no slash
fails create with exit code 1 and writes nothing.

Finding 8: the test counts in the body match the results file in the
diff. The results file records 100 checks with 0 failures, 27
archives in formats the pilot does not read, and 11 readable archives
compared with tarfile. The must-fail archives are checked under both
list and manifest, with exit code 1 and empty standard output.

Finding 9: one comparison in the readable set is stated with an
exclusion, and the exclusion is honest but worth noting. Tarfile
reports an old style directory, typeflag NUL with a name ending in a
slash, as typeflag 5. The readable comparison therefore drops the
typeflag from SKIP lines before comparing. A reader of the headline
count alone would not see that exclusion.

Finding 10: no sorry or admit appears in the added Lean code in this
diff. The axiom check from PR 4 is carried over unchanged in
substance, with 13 axiom related checks inside the 100 total.

Questions to the author

Question 1: is the readable set checked under list as well as
manifest? The must-fail set is checked under both commands, while
the readable loop in the diff runs manifest only. Archive A covers
list for the older cases, but does the readable set add any list
coverage?

Question 2: is the two part trailing slash rule stated in the README
in this PR, or does a reader find it only in code comments? The
parse failure part and the skip part have different visible effects,
and the README text in the diff is short on this point.

Question 3: does the GNU header rule reject any GNU header that GNU
tar writes by default for short names? The body states that short
name GNU archives are among the readable set, and the code requires
an empty prefix area for GNU headers. Is there a default GNU header
field that lands in that area and would break that claim?

Question 4: the body states that 58 of the 100 checks fail against
the PR 4 binary. Is that figure from a recorded run, and does any
file in this PR record it? A reader cannot reproduce that figure
from the results file alone, since the results file records only
this PR's run.

Limits

This is a reading review only. The Lean code was not built, and the
test suite was not rerun here. Test counts, failure counts, and the
58 check figure 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: 100 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 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 B is this pull request after pull request 4.

Automated posting by agentic team with human oversight.

[orda-aska]

TarPilot/Archive.lean:37 returns success at the first zero block without checking the rest of the archive. Reproduced: one zero end block, a hidden valid entry after one zero block, and a nonzero byte after a complete archive all return exit code 0 and print only the visible prefix. Require two zero blocks, only zero trailing padding, and a total length divisible by 512. Add rejection tests with empty stdout for list and manifest, including concatenated archives. This is the end rule requested in issue #7.