Proven Commons

Document Source: reviews/tar/2026-10-24-bar-audit.md

Contents

Bar audit: tar pilot, 2026-10-24

  • Subject: Proven-Commons/tar at commit 7517a86 (main on 2026-10-24).
  • Measured against: the verified bar in README.md and FOUNDING-BRIEF.md of this repo at commit ca367b1.
  • Written by: Claude, an AI agent working for the org owner. This is an adversarial review (factory step 5). It is not the spec approval that bar item 1 asks for. See reviews/README.md.
  • Tools: Lean 4.35.0 (commit eb6cafb), Python 3.13.17, GNU tar 1.35, bubblewrap 0.9.0, Linux x86_64.

Verdict

The pilot does not yet meet the verified bar. Three items are met, one is partly met, and two are not met.

The proofs that exist are sound. Lean’s kernel and the five other kernels shipped with Lean 4.35 accept them, and they use only the standard axioms. The problem is what they state. The headline theorem says less than the public claim that no file in an archive can be written outside the destination folder (F1). On every input tried here, no emitted path left the destination. The proof does not yet show that this always holds.

The project page overstates what the theorem proves, and two statements under “What is not proved” are false (F2, F3). The command-line tool calls the proved gate but not the proved extraction function (F5).

Until the fixes below land, neither repo should call the pilot verified or complete. This repo’s README now calls it built, not yet verified.

Item by item

# Bar item Status Evidence
1 Specification public and approved by a separate reviewer Not met The repo has no specification file and no approval record. The head of verification post is not filled yet (brief, “Decisions needed now”, 2).
2 No sorry or admit Met None in the sources, and #print axioms shows no sorryAx. Caveat (F6): lake build exits 0 when a proof is sorry, so the page’s “The build fails if a proof breaks” does not hold for sorry.
3 #print axioms shows only the standard axioms Met TarPilot/Verify.lean prints only propext, Classical.choice, and Quot.sound for all four theorems. lake check --paranoid accepts the project under all six kernels. Caveats: the test script’s own axiom check is a denylist (F6), and the theorem it checks is too weak (F1).
4 Differential tests ran; count, seed, and result in the repo Met tests/TEST-RESULTS.md records 16 checks and 0 failures, and the seeds (42, 7, 1) are in tests/run_tests.py. Caveats: the results file does not repeat the seeds, and the inputs fall short of factory step 5 (“random and mutated inputs”). They are 14 fixed archive entries, 3 files for the create round trip, and 3 broken files. One of the broken files is random and one has a flipped byte, but those two are only checked for exit code 1, not compared with tarfile. Every probe in F2 to F4 falls outside these inputs.
5 Public page lists what is outside the proof Not met It names the kernel, compiler, and runtime, not hardware. Two statements under “What is not proved” are false (F2, F3). It does not say that the command-line tool re-implements the proved extraction loop (F5), or that joining the components into one path string is outside the proof (F1).
6 A stranger can clone, run one command, and re-check Partly met The page’s re-check is three commands: lake build, lake env lean TarPilot/Verify.lean, python3 tests/run_tests.py. All pass on a clean clone, but no one of them re-checks the proof alone: lake build accepts a sorry, and the test script accepts a new axiom (F6). Lean 4.35’s lake check --paranoid is one command that does, and it passes (8 minutes here), but the page does not give it. Separately, there is no CI, so nothing re-checks the proof on each change (factory step 7).

Findings

F1. The headline theorem does not state the headline claim

The claim, on this repo’s README and on the tar page: no file in an archive can be written outside the destination folder, and “a machine-checked proof shows the cleaned path can never climb out of the destination”.

The theorem, extractAll_safe (TarPilot/Archive.lean line 74): every emitted path is the destination followed by a non-empty list of components, none of which is .., empty, or ..

The gap: nothing says a component cannot contain /. The one-component list ["../../etc/passwd"] satisfies the statement. runManifest joins components with / (Main.lean line 50), which gives out/../../etc/passwd. A gate that never splits the name on / proves the exact statement of gate_sound.

Evidence: evidence/WeakStatement.lean. Inside a tar checkout, lake env lean WeakStatement.lean prints:

some ["a/../../etc/passwd"]
'escaping_path_is_published_safe' depends on axioms: [propext]
'badGate_sound' depends on axioms: [propext, Classical.choice, Quot.sound]

Is the code unsafe? No. Its components come from splitOn "/", so none holds a /. That is an unproved fact about String.splitOn. The proof does not carry it.

Fix: evidence/Contained.lean. It adds one check to the cleaner: reject a component that holds / or NUL. On any archive parseArchive reads, that changes no output, and the new gate agrees with the old one on all 17 names in the pilot’s tests. It then proves three statements, with the standard axioms only:

  • extractAll_contained: every emitted path is the destination followed by a non-empty list of plain names (not empty, . or .., and free of / and NUL).
  • extractAll_joined: the path string the tool builds, by joining with /, splits back into exactly those components.
  • extractAll_resolves_inside: resolving that string lexically, as POSIX resolves a relative path when no component is a symlink, gives the resolved destination followed by the plain names.

The last two assume the destination’s own components hold no /, which holds for the destination the tool builds. Unlike the published statement, these fail for the broken gate. Its output joins and resolves to etc/passwd, which the file shows.

Why this matters past tar: every machine check in the current bar passed. No sorry, standard axioms, tests green. None of them can notice that a theorem states less than its claim. Only a reviewer reading the statement against the claim can, which makes bar item 1 the item everything else rests on.

F2. GNU and pax archives are accepted, not rejected, and some are read wrongly

The page says GNU extensions and pax headers are not supported, and “an archive using them fails to parse instead of being read in a wrong way” (README.md line 39).

What happens: such archives are accepted, with exit code 0. The extension headers are skipped as non-regular entries. When the extension carries nothing the ustar header lacks, as with short ASCII names, the right name and data come out. When it does carry something, the pilot reads a different archive from other tools:

  • A long name is cut to its first 100 bytes and loses .txt. This includes the default output of GNU tar 1.35 (--format=gnu) for any name over 100 bytes.
  • A pax path override is ignored, so the file is read under its old name.
  • A pax non-ASCII name is read as caf?/notes.txt.

Every path still lands inside the destination, because the gate still runs. Even a pax override that climbs out (../../etc/cron.d/x) is read as out/safe.txt. But the page says such archives are not read at all.

Evidence: evidence/probe_formats.py, run as python3 -I probe_formats.py <tar>/.lake/build/bin/tar-pilot. Three of its blocks, with each long run of one letter cut to nnn… (here 120 n in the name, 98 in the pilot’s output):

## system tar, default format (tar (GNU tar) 1.35)
tarfile reads:   [('d/nnn….txt', '0')]
tar-pilot exit:  0
tar-pilot says:  SKIP	d/	53
tar-pilot says:  SKIP	././@LongLink	76
tar-pilot says:  OK	out/d/nnn…	1	120

## pax path override that climbs out
tarfile reads:   [('../../etc/cron.d/x', '0')]
tar-pilot exit:  0
tar-pilot says:  SKIP	././@PaxHeader	120
tar-pilot says:  OK	out/safe.txt	1	120

## pax non-ASCII name
tarfile reads:   [('café/notes.txt', '0')]
tar-pilot exit:  0
tar-pilot says:  SKIP	././@PaxHeader	120
tar-pilot says:  OK	out/caf?/notes.txt	1	120

Fix: reject entries with typeflags L, K (GNU long name and long link), x, g (pax), and any other type outside the supported set, so the page becomes true. Or implement them.

F3. A split name with invalid UTF-8 in one field is misplaced, not rejected

The page says “names that are not valid UTF-8 read as empty and are rejected by the gate” (README.md line 39). That holds for a short name, one that fits the name field with no prefix. It does not hold for a name split over the prefix and name fields.

What happens: bytesToName reads invalid UTF-8 as the empty string (TarPilot/Header.lean line 38), and parseBlock then joins the two fields as if that one were empty (line 57). With an invalid prefix and a valid name, the prefix is dropped and the file lands at out/qqq…/file.txt. With a valid prefix and an invalid name, the file lands at out/ppp…, the name of the prefix directory itself. Only when both fields are invalid is the entry rejected. The same evidence script runs all four cases, here without its tarfile reads lines and with runs of one letter cut:

## split name, invalid UTF-8 in the prefix field only
tar-pilot exit:  0
tar-pilot says:  OK	out/qqq…/file.txt	1	120

## split name, invalid UTF-8 in the name field only
tar-pilot exit:  0
tar-pilot says:  OK	out/ppp…	1	120

## split name, invalid UTF-8 in both fields
tar-pilot exit:  0
tar-pilot says:  REJECT

## short name (no prefix), invalid UTF-8
tar-pilot exit:  0
tar-pilot says:  REJECT

Fix: have bytesToName return Option String and reject the header when either field is not valid UTF-8.

F4. Contiguous files are skipped, unlike other readers

An entry with typeflag 7 (contiguous file) is skipped. The page’s rule covers this: only typeflag 0 or NUL is extracted. But POSIX lets a reader treat 7 as a regular file, and Python’s tarfile does. So the pilot extracts fewer files than other tools, without the page naming this case. Same evidence script:

## contiguous file, typeflag 7
tarfile reads:   [('contig.bin', '7')]
tar-pilot exit:  0
tar-pilot says:  SKIP	contig.bin	55

Fix: extract typeflag 7 as a regular file, or name it on the page as a case that differs from other readers.

F5. The command-line tool does not call the proved extraction function

runManifest (Main.lean lines 37 to 54) calls parseArchive, isRegular, and the proved gate. But it re-implements the loop of the proved extractAll, and joins the path itself. The differential tests drive the command-line tool, so they test that loop and join, not extractAll or extractArchive. Today the two agree when read side by side. Nothing checks it.

Fix: take the OK lines from extractArchive, and work out the REJECT and SKIP lines from the parsed entries, since extractArchive drops those. Or prove that the OK lines runManifest prints are exactly the output of extractAll.

F6. The pilot’s own checks let faults through

Evidence: evidence/plant_faults.py copies a checkout to a temporary directory, plants each fault in TarPilot/Path.lean, and records the exit codes. Its output, with the temporary paths cut:

## fault: sorry
lake build exit:          0
tests/run_tests.py exit:  1  (15/16 checks passed; ...)
TEST-RESULTS.md records:  'TarPilot.gate_sound' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
TEST-RESULTS.md records:  - axioms-no-sorry: 'TarPilot.gate_sound' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]

## fault: axiom
lake build exit:          0
tests/run_tests.py exit:  0  (16/16 checks passed; ...)
TEST-RESULTS.md records:  'TarPilot.gate_sound' depends on axioms: [propext, Classical.choice, Quot.sound, TarPilot.cheat]

The test script catches a sorry, but lake build alone does not. With axiom cheat : False behind gate_sound, every check passes, and the results file lists the bad axiom without failing. The cause is tests/run_tests.py line 224, which looks only for sorryAx.

Fix: check the axiom list against the allowed set propext, Classical.choice, Quot.sound, or use lake check, which fails on any other axiom.

What holds

  • A clean clone builds, and all 16 differential checks pass.
  • All four theorems use only propext, Classical.choice, and Quot.sound.
  • lake check --paranoid passes. Lean’s kernel, leanchecker-paranoid, lean4lean (58011 declarations), nanoda, con-leche, and con-ron (58014 declarations each) all accept the project.
  • No probe in F2 to F4 made the pilot emit a path outside the destination.

Fixes for the tar repo, in order

  1. F1: adopt the cleaner and theorems from evidence/Contained.lean, and state on the page the theorem actually proved.
  2. F5: have runManifest take its OK lines from extractArchive.
  3. F2, F3, F4: reject unsupported typeflags and part-invalid names, add the probes as test cases, and correct the page.
  4. F6 and item 6: check axioms against the allowed set, and make lake check --paranoid the one re-check command on the page.
  5. Item 4: add seeded random and mutated inputs compared with tarfile (for example, valid headers with fields flipped), and record the seed, input count, and oracle version in tests/TEST-RESULTS.md.
  6. Item 5: add hardware, the test oracle, and the filesystem to what a reader must trust.
  7. Item 1: write the specification, have a reviewer who did not write it approve it, and record the approval.
  8. Factory step 7: run the check in CI on every push.
  9. On the page’s status line, drop “built to the verified bar” and “pilot complete” until the bar is met, and point the link to the org’s home repo at mission (it says proven-commons, which now redirects).

Re-run this audit

git clone https://github.com/Proven-Commons/tar && cd tar && git checkout 7517a86
lake build
lake env lean TarPilot/Verify.lean
python3 tests/run_tests.py           # rewrites tests/TEST-RESULTS.md
cp <mission>/reviews/tar/evidence/*.lean .
lake env lean WeakStatement.lean
lake env lean Contained.lean
python3 -I <mission>/reviews/tar/evidence/probe_formats.py .lake/build/bin/tar-pilot
python3 -I <mission>/reviews/tar/evidence/plant_faults.py .
lake check --paranoid                # needs bubblewrap

Limits of this audit

  • It checks the six bar items and the probes above. It is not a full review of the header parser, and it ran no fuzzing campaign.
  • It ran on Linux x86_64 only.
  • An agent wrote it. It can find problems. It cannot approve a specification.