[ahrazzle]

This is the third of three stacked PRs that fix the org's bar audit (Proven-Commons/mission#1). It is based on #5; merge #4, then #5, then this one.

It adopts the verified bar v2 (Proven-Commons/mission#2), so a machine checks each item of the bar on every change. It finishes the audit's list of fixes except the spec approval, which needs a person. Item numbers below are bar v2's.

What is in it

• Spec.lean: the eleven statements from Proofs/Contain.lean, with sorry. This is the challenge file a spec reviewer approves, together with SPEC.md and Spec/Defs.lean (item 1).
• comparator.json: lake comparator --paranoid checks that each proof proves exactly its statement, under all six kernels shipped with Lean, with the standard axioms only (item 3). It replaces TarPilot/Verify.lean and the test script's axiom check (audit F6).
• SPEC.md: every rule in plain words: the format the pilot reads, the gate, extraction, the exact lines manifest prints, and the commands and exit codes.
• tests/run_tests.py (item 5):
  • 10,000 random archives from a recorded seed, written by tarfile in ustar, GNU and pax formats. They have hostile names, names and prefixes at the edges of their fields, every POSIX entry type, and size fields on entries that store no data.
  • Half are mutated. Most mutations set a header field to a value at the edge of what is valid, then make the checksum right, signed, seven digits, or stale.
  • For each archive, list and manifest must match a model of the format written from SPEC.md. Where the model and tarfile both read an unmutated archive, they must agree on every entry.
  • Fixed cases cover what review found the random cases missed, the usage exit codes, and archives written by GNU tar, which the script now requires.
• README.md: the page in the bar's sections (items 2 and 6). Every claim names its theorem. It says what is not proved, and what you must trust, including Lean's core library and its compiled replacements. The status line says in progress until a spec reviewer approves.
• bar.toml and .github/workflows/bar.yml: the bar record, and the check in CI (item 7), pinned to the bar v2 commit of mission.

How it was checked

• bar/check.py --offline --run-tests (mission at 6ba85c2) gives:
  • items 2 to 6: PASS;
  • item 1: OPEN, because no approval is recorded and mission's bar/reviewers.toml names no reviewer yet;
  • item 7: read in CI, which needs main to require the bar / bar check.
• lake comparator --paranoid accepts all eleven statements.
• The tests: 23,243 checks, 10,055 archives, 0 failures. Python 3.12.3 and 3.13.17 give the same seed, inputs and failures.
• A reviewer planted 37 bugs in the parser and printer, one at a time. 36 still apply to this code, and the tests catch all 36. The first version of these tests missed 12 of them, which led to the field-level mutations and the new fixed cases.

What is still needed

A spec reviewer who did not write the specification approves SPEC.md, Spec.lean, Spec/Defs.lean, and the other files bar.toml lists. The approval is recorded in bar.toml in a pull request the reviewer approves. Until then the page says "in progress".

---

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), which adds a different CI check and its own SPEC.md. Only one set can merge. The choice is tracked in #7.

---

Generated by Claude Code

[ahrazzle]

Head sha: f0e17be

Branch: claude/verified-bar, based on the PR 5 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 third of three stacked PRs, numbered 4, 5, and
6. The body states the ordering as PR 4, then PR 5, then this PR. 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. The title itself states that spec approval
is pending, and that status is central to this draft.

Findings

Finding 1: the spec approval status is stated consistently across
the PR. The title says spec approval is pending. The body says item
1 of bar v2 is OPEN, because no approval is recorded and the mission
reviewers file names no reviewer yet. Bar.toml records status
in-progress, lists spec authors as claude, and leaves the approval
section commented out as a placeholder. The README states in
progress, and states that the specification has not yet been
approved by a reviewer apart from its author, so this is not
verified. A reader cannot mistake this PR for a completed
verification.

Finding 2: what remains open is specific, not general. The approval
covers SPEC.md, Spec.lean, Spec/Defs.lean, and the other files
bar.toml lists. The approval is recorded in bar.toml in a pull
request the reviewer approves. Until that pull request exists, item
1 stays open. The reviewer also has to be someone who did not write
the specification.

Finding 3: the sorry in Spec.lean is intentional, and the file header
says so. Spec.lean holds the eleven statements from Proofs/Contain.lean,
each with sorry, as the challenge file a spec reviewer approves.
Comparator.json lists the same eleven theorem names, with permitted
axioms propext, Quot.sound, and Classical.choice. The sorry here is
not a sorry in the proved code. The proved code lives in Proofs, and
this PR does not change Proofs. A reader who greps for sorry across
the repo needs that distinction, or the count misleads.

Finding 4: the proof check moves, and the move is visible in the
diff. TarPilot/Verify.lean is removed. The test script no longer
runs an axiom check. The body states that lake comparator with the
paranoid flag now checks that each proof proves exactly its
statement, under all six kernels shipped with Lean, with the standard
axioms only. That claim was not verified here, since the suite was
not rerun.

Finding 5: item 7 has a dependency outside this PR. The body states
that item 7 is read in CI, which needs main to require the bar check.
The workflow file pins the mission verified bar workflow at commit
6ba85c27abaaf07905c9316aa96dc29f7b5847a2, and notes that both pin
lines move to a release tag once mission publishes one. The bar v2
proposal itself lives in mission pull request 2. The CI part of this
PR therefore depends on a mission commit and on a branch protection
setting that this PR does not itself set.

Finding 6: the test counts in the body match the results file in the
diff. The results file records seed 20261025, 10055 inputs, 55 fixed
archives plus 10000 random archives, 5000 of them mutated, 23243
checks, and 0 failures. The fixed unsupported count rises from 27
to 33, and the fixed readable count rises from 11 to 17. The script
accepts a seed and a count on the command line, which makes the
default run reproducible in principle.

Finding 7: the tarfile agreement claim has a stated limit. The model
reads 4732 of the random archives. Tarfile agrees with the model on
all 3134 unmutated archives that both read. Mutated archives are
compared with the model only, not with tarfile. The model is written
from SPEC.md, so agreement between the tool and the model tests the
tool against the specification, not the specification against an
independent reader, for the mutated set.

Finding 8: the planted bug claim is stated with a gap that is also
stated. A reviewer planted 37 bugs in the parser and printer, one at
a time. The body states that 36 still apply to this code, and the
tests catch all 36. The body does not name the one bug that does not
apply, or the reason it does not apply. The body also states that
the first version of these tests missed 12 bugs, which led to the
field level mutations and the new fixed cases. That history is
useful, and it shows the test set changed in response to misses.

Finding 9: the Python version claim in the body goes beyond the
results file. The body states that Python 3.12.3 and 3.13.17 give
the same seed, inputs, and failures. The results file in the diff
names Python 3.13.17 only. A reader cannot confirm the 3.12.3 half
of that claim from the results file alone.

Finding 10: SPEC.md states its scope limits plainly. Signed byte
checksum sums are not read. Base-256 size fields are not read. The
parser scope is POSIX ustar plus GNU headers that carry nothing
ustar does not. Anything outside the rules fails the whole parse.
Those limits match the PR 5 parser rules, and they are now written
in a specification document rather than only in code comments.

Questions to the author

Question 1: which planted bug does not apply to this code, and why
does it not apply? Naming it would close the gap between 37 planted
and 36 caught, and would let a reader check that the gap is benign
rather than a blind spot.

Question 2: is the branch protection setting for the bar check part
of this PR's scope, or is it a separate step owned elsewhere? The
body states that item 7 needs main to require the check, and a
reader cannot tell from this PR who sets that requirement.

Question 3: is the mission bar v2 commit pinned here a merged commit
or a commit on mission pull request 2? The workflow comment says
to move both pin lines to a release tag once mission publishes one,
which suggests the pin is provisional. Clarifying the mission side
status would help a reader judge the stability of the CI pin.

Question 4: does any file in this PR record the Python 3.12.3 run?
The results file names 3.13.17 only. If the 3.12.3 run exists, is
there a record of it that a reader can check?

Question 5: does the comparator check run anywhere in this PR's own
test script, or only as a separate lake command? The test script
header states that proofs are checked by lake comparator, not in the
script. A reader running only the test script would therefore not
see the proof check result.

Limits

This is a reading review only. The Lean code was not built, the
comparator was not run, and the test suite was not rerun here.
Test counts, seed values, planted bug figures, and bar item results
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. The spec approval
question is open on the face of the PR, and this draft does not
answer it.

Automated posting by agentic team with human oversight.

[ahrazzle]

Verdict: COMMENT. Not an approval. Two blockers stand, apart from the code.

Built check. I built this head: 21 jobs, passed. I ran the tests: 23243 checks, 0 failures, matching the committed record. Sorry appears only in Spec.lean, as the bar v2 challenge file design requires. Check runs on this head show bar completed with success.

Blocker one: the title and body state spec approval is pending, and that approval is a person decision, not a machine check. Bar v2 item 1 is not met on this pull request alone.

Blocker two: this pull request is part of Set B, and it competes with Set A. Tar issue 7, which decides which set merges, is still open. Only one set can merge. It also adopts bar v2 from mission pull request 2, so that mission pull request is part of the merge order before this one.

This comment records that the code passes its build and tests, and that the merge decision waits on the spec approval and on issue 7.

Automated posting by agentic team with human oversight.

[orda-aska]

SPEC.md:11 ends the archive at the first zero block. This leaves entries after that block outside the manifest while readers using ignore-zeros can extract them. Adopt the strict end rule: two zero blocks, only zero trailing padding, and a whole number of blocks, with matching model and regression tests. README.md:3 also claims every printed line is proved, while SPEC.md explicitly excludes list output from the proofs. Narrow that claim to manifest output. The specification approval remains unrecorded in bar.toml.