From f0e17be1d0f97af6a8c312e128199505cc06dbcd Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 25 Oct 2026 04:24:40 +0000 Subject: [PATCH 1/6] Adopt verified bar v2 for tar (in progress: spec approval pending) Adopts bar v2 (Proven-Commons/mission#2), so a machine checks every item of the bar on each change, and finishes the audit's list of fixes except the spec approval, which needs a reviewer. Item numbers below are bar v2's. - `Spec.lean`: the eleven statements of `Proofs/Contain.lean`, with `sorry`, as the challenge file a spec reviewer approves together with `SPEC.md` and `Spec/Defs.lean` (item 1, open until approved). - `comparator.json`: `lake comparator --paranoid` checks that each proof proves exactly its statement, with `propext`, `Quot.sound` and `Classical.choice` only, under all six kernels shipped with Lean (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 tool's commands and exit codes. - `tests/run_tests.py` (item 5): from seed 20261025, 10,000 archives written by tarfile in ustar, GNU and pax formats, with hostile names, names and prefixes at the edges of their fields, every POSIX entry type, size fields on entries that store no data, and random data. Half are mutated, mostly by setting a header field to a value at the edge of what is valid and making the checksum right, signed, seven digits, or stale. For each, `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. 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. - `README.md`: the page in the bar's sections (items 2 and 6), with every claim naming its theorem, what is not proved, what you must trust (Lean's core library and its compiled replacements included), and a status line: 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. `check.py --offline --run-tests` gives items 2 to 6 PASS, item 1 OPEN (no approval; mission's `bar/reviewers.toml` names no reviewer yet), and item 7 to be read in CI. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- .github/workflows/bar.yml | 21 ++ .gitignore | 1 + README.md | 90 ++++---- SPEC.md | 82 ++++++++ Spec.lean | 111 ++++++++++ TarPilot/Verify.lean | 20 -- bar.toml | 38 ++++ comparator.json | 22 ++ lakefile.toml | 1 - tests/TEST-RESULTS.md | 33 +-- tests/run_tests.py | 430 +++++++++++++++++++++++++++++++++----- 11 files changed, 722 insertions(+), 127 deletions(-) create mode 100644 .github/workflows/bar.yml create mode 100644 SPEC.md create mode 100644 Spec.lean delete mode 100644 TarPilot/Verify.lean create mode 100644 bar.toml create mode 100644 comparator.json diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml new file mode 100644 index 0000000..32457ed --- /dev/null +++ b/.github/workflows/bar.yml @@ -0,0 +1,21 @@ +name: verified bar + +on: + push: + pull_request: + # Rerun when the spec reviewer approves, or an approval is dismissed. + pull_request_review: + types: [submitted, dismissed] + +jobs: + bar: + # pull-requests: read lets the check confirm the spec approval on GitHub. + permissions: + contents: read + pull-requests: read + # Both lines pin the same commit of Proven-Commons/mission: bar v2, as + # proposed in its pull request #2. Move both to a release tag once + # mission publishes one. + uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2 + with: + bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2 diff --git a/.gitignore b/.gitignore index 01f8cdb..ae73679 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ .lake/ +__pycache__/ diff --git a/README.md b/README.md index 916dcc9..93ee07e 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,14 @@ # tar: a tar extractor that cannot escape its destination -This repo reads a tar archive (ustar format) and extracts regular files into an in-memory list of paths and file contents. Every path it emits is the destination followed by a cleaned relative path. Machine-checked proofs show that every `OK` line the command-line tool prints is the destination exactly as given, then plain names: none is empty, `.` or `..`, or holds `/`, a control character, or a Unicode line or paragraph separator. So no entry can climb out of the destination, and no name can forge a line or a field of the tool's output. Each line the tool prints is proved to be exactly the line `Spec/Defs.lean` writes out from the rules. +This repo reads a tar archive (ustar format) and works out where each regular file would be extracted, without writing anything to disk. Machine-checked proofs show that every `OK` line the command-line tool prints is the destination exactly as given, then plain names: none is empty, `.` or `..`, or holds `/`, a control character, or a Unicode line or paragraph separator. So no entry can climb out of the destination, and no name can forge a line or a field of the tool's output. The path gate, the extraction rule, and every line the tool prints for a parsed archive are proved to be exactly what this page and `SPEC.md` say. Parsing is tested on ten thousand random and mutated archives against a model of the format written from `SPEC.md`, which Python's `tarfile` checks on every unmutated archive both read, and on fixed archives against `tarfile` and GNU tar. -It is the first Proven Commons project. Status: built, not yet verified. The org's [bar audit](https://github.com/Proven-Commons/mission/pull/1) lists what is still missing against the verified bar in [mission](https://github.com/Proven-Commons/mission). +It is the first Proven Commons project, and the subject of the org's [bar audit](https://github.com/Proven-Commons/mission/pull/1) of 2026-10-24, whose findings it fixes. + +Status: in progress. The specification has not yet been approved by a reviewer apart from its author, so this is not verified. ## Run it -Needs Lean 4.35.0 (install with elan, toolchain pinned in `lean-toolchain`). +Needs Lean 4.35.0 (install with elan; the toolchain is pinned in `lean-toolchain`). ``` lake build @@ -15,65 +17,79 @@ lake build .lake/build/bin/tar-pilot create [more files...] ``` -`manifest` prints what extraction would do, in archive order, and writes nothing to disk: `OK` with the final path, size, and byte sum for an extracted file, `REJECT` for a regular file whose name fails the path gate, `SKIP` for a non-regular entry. Fields are separated by tabs and lines end in a line feed. In `REJECT` and `SKIP` lines, and in `list`, a backslash in a name is printed as two, the line and paragraph separators U+2028 and U+2029 as `\u2028` and `\u2029`, and a control character as `\x` and two hex digits. A destination that holds any of these special characters, or U+FFFD (which the Lean runtime puts in place of bytes that are not UTF-8), is refused (exit code 2). +`manifest` prints what extraction would do, in archive order: `OK` with the final path, size, and byte sum for an extracted file, `REJECT` for a regular file whose name fails the path gate, `SKIP` for any other entry. Fields are separated by tabs and lines end in a line feed. In `REJECT` and `SKIP` lines, and in `list`, a backslash in a name is printed as two, the line and paragraph separators U+2028 and U+2029 as `\u2028` and `\u2029`, and a control character as `\x` and two hex digits. A destination that holds any of these special characters, or U+FFFD (which the Lean runtime puts in place of bytes that are not UTF-8), is refused (exit code 2). `SPEC.md` gives every rule in plain words. ## What is proved -The theorems are in `Proofs/Contain.lean`, about the code in `TarPilot/Path.lean` and `TarPilot/Archive.lean`. Their statements use the definitions in `Spec/Defs.lean`: a special character (a control character, C0, DEL, or C1, or the Unicode line or paragraph separator), a plain name (not empty, `.` or `..`, and free of `/` and special characters), the components of a path string (the parts between `/`), the gate's rules, the regular typeflags, a path under a destination, how a name is printed, the exact line printed for an entry, and lexical resolution of a relative path. They are about the code definitions `Spec/Defs.lean` lists, which a reviewer reads with them. - -The gate rules, which `gate_eq` proves the gate follows exactly: a name that starts with `/` is rejected. A name with a `..` component, or with a special character, is rejected. Empty and `.` components are dropped. A name with nothing left is rejected. Only regular files are extracted, which `manifest_eq` proves: typeflag `0`, NUL from older archives, or `7`, a contiguous file, which POSIX lets a reader treat as regular; and a name that does not end in `/`, which older archives use for a directory and GNU tar reads as one. Directory, link, and other entries are skipped, so a link entry cannot place a later entry outside the destination. +The statements are in `Spec.lean`, the definitions they use in `Spec/Defs.lean`, and the proofs in `Proofs/`. The definitions say what a special character is (a control character, C0, DEL, or C1, or the Unicode line or paragraph separator), what a plain name is, how a path string splits into components, the gate's rules, which entries are regular files, how a path is written under a destination, how a name is printed, the exact line printed for an entry, and how a relative path resolves. The statements are about the code definitions `Spec/Defs.lean` lists, which a reviewer reads with them. -- `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`: what the tool's `manifest` says about each entry. A regular file whose name passes the gate is extracted at the destination followed by the gate's components, with its own data. A regular file whose name fails is rejected, and anything else is skipped. -- `manifest_extracted`: the entries the manifest extracts are exactly the output of the extractor, `extractAll`, in order. -- `manifest_lines_eq`: the lines `tar-pilot manifest ` prints are exactly `Spec.line` for each entry: `OK`, the path, the size and the byte sum; `REJECT` and the printed name; or `SKIP`, the printed name and the typeflag code. The path is the destination exactly as given, then the gate's components joined by `/`: with destination `out` that is `out/a/b`; with `out/` or `/` it is `out/a/b` or `/a/b`, with no doubled `/`. -- `Spec.escape_noSpecial`, proved in `Spec/Defs.lean` itself, since it is about the specification alone: a printed name holds no special character, so it cannot break a line or a field. -- `manifest_lines`: given a destination with no special character, as the tool requires, the only special characters in a line are its tab separators, and every line that starts with `OK` and a tab continues with the destination, then a non-empty list of plain names, then a tab. -- `extractAll_contained`: every path the extractor emits is the destination followed by a non-empty list of plain names. -- `extractAll_joined`: joined with `/`, such a path splits back into exactly the destination components and those names, when no destination component holds `/`. -- `extractAll_resolves_inside` and `extractArchive_resolves_inside`: resolved lexically, it is the resolved destination followed by those names, for an archive given as entries or as bytes. No `..` in an archive reaches above the destination. The resolution reads a path as relative and drops a leading `/`, so for an absolute destination read both sides from `/`. -- `extractArchive_eq`: extracting an archive read from bytes is parsing it, then the extractor. +The gate's rules: a name that starts with `/` is rejected. A name with a `..` component, or with a special character, is rejected. Empty and `.` components are dropped. A name with nothing left is rejected. Only regular files are extracted: typeflag `0`, NUL, or `7` (a contiguous file), with a name that does not end in `/`, which older archives use for a directory and GNU tar reads as one. Directories, links, and other entries are skipped, so a link entry cannot place a later entry outside the destination. -The statements fix what extraction does with a parsed archive. They do not fix how bytes are parsed into entries, which the tests cover. +| Claim | Theorem | +|-------|---------| +| The gate is exactly its rules. | `TarPilot.gate_eq` | +| A name that passes the gate gives a non-empty list of plain names. | `TarPilot.gate_plain` | +| Each entry is extracted, rejected, or skipped exactly as the rules say, an extracted entry at the destination followed by the gate's components and with its own data. | `TarPilot.manifest_eq` | +| The entries the manifest extracts are exactly the extractor's output, in order. | `TarPilot.manifest_extracted` | +| The lines `tar-pilot manifest ` prints are exactly `Spec.line` for each entry: `OK`, the path, the size and the byte sum; `REJECT` and the printed name; or `SKIP`, the printed name and the typeflag code. The path is the destination exactly as given, then the gate's components joined by `/`: `out/a/b` under `out`, and `out/a/b` or `/a/b` under `out/` or `/`, with no doubled `/`. | `TarPilot.manifest_lines_eq` | +| Given a destination with no special character, as the tool requires, the only special characters in a line are its tab separators, and every line that starts with `OK` and a tab continues with the destination, then a non-empty list of plain names, then a tab. | `TarPilot.manifest_lines` | +| Every path the extractor emits is the destination followed by a non-empty list of plain names. | `TarPilot.extractAll_contained` | +| Joined with `/`, such a path splits back into exactly the destination components and those names. | `TarPilot.extractAll_joined` | +| Resolved lexically, it is the resolved destination followed by those names, for an archive given as entries or as bytes: no `..` in an archive reaches above the destination. The resolution reads a path as relative and drops a leading `/`, so for an absolute destination read both sides from `/`. | `TarPilot.extractAll_resolves_inside`, `TarPilot.extractArchive_resolves_inside` | +| Extracting an archive read from bytes is parsing it, then the extractor. | `TarPilot.extractArchive_eq` | -Axiom check: each theorem depends only on the standard Lean axioms (`propext`, `Classical.choice`, `Quot.sound`, or a subset). The test script fails on any other axiom, `sorryAx` included, and if the list of theorems checked is not exactly the list above. Full output is recorded in `tests/TEST-RESULTS.md`. +`Spec/Defs.lean` also proves, about the specification alone, that a printed name holds no special character, so it cannot break a line or a field (`Spec.escape_noSpecial`). ## What is not proved -Read this before trusting the pilot with real archives: - -- Header parsing, octal fields, checksums, and archive writing are tested, not proved. The tests compare the Lean code against Python's `tarfile` module and against an independent copy of the extraction spec. Results are in `tests/TEST-RESULTS.md`: 100 checks, 13 of them on the axioms, 0 failures. They cover 23 archive entries with normal files, hostile names (control characters and line separators among them), and a long name split over the ustar prefix field; eight destinations, and five refused for a special character or U+FFFD; broken inputs (truncated, garbage, bad checksum); 27 archives in formats the pilot does not read; and 11 more archives it does read, among them GNU format, GNU tar's own output, names ending in `/`, and links, devices, directories and FIFOs whose size fields are not zero. -- The `list` output is tested, not proved. So is `Main.lean`: that it prints `o.line` for each outcome of the manifest, and refuses a destination with a special character or U+FFFD. Read it with the statements; it is a few lines. -- Extraction works on an in-memory model. Nothing here writes files to disk, so the step from a proved in-memory path to a safe write on a real filesystem (races, symlinks already on disk, symlinked destination folders) is outside this project for now. The proof resolves paths lexically, as POSIX does when no component is a symlink. -- The destination itself. The proof says where a path lands relative to the destination, not whether the destination is a safe place to write. The destination is the command-line argument as the Lean runtime decodes it from UTF-8. -- Formats beyond POSIX ustar. The pilot reads ustar headers, and GNU headers that carry nothing ustar does not. As POSIX says, and as GNU tar and Python's `tarfile` read them, links, devices, directories and FIFOs store no data, whatever their size field says. An archive that uses anything else fails to parse as a whole, instead of being read in a wrong way: +- Parsing bytes into entries: the header layout, octal fields, checksums, and which formats are read. So are the `list` output, `create`, and `Main.lean`: that it prints `o.line` for each outcome of the manifest, and refuses a destination with a special character or U+FFFD. `Main.lean` is a few lines; read it with the statements. The differential tests cover these, against Python's `tarfile` and against a model of the format written from `SPEC.md`. The statements hold for whatever entries a parse gives. +- Formats beyond POSIX ustar. The pilot reads ustar headers, and GNU headers that carry nothing ustar does not. As POSIX says, and as GNU tar and Python's `tarfile` read them, links, devices, directories and FIFOs store no data, whatever their size field says. An archive that uses anything outside the rules in `SPEC.md` fails to parse as a whole, rather than be read in a way the pilot does not vouch for: - typeflags outside the POSIX set (NUL and `0` to `7`), among them GNU long names and long links (`L`, `K`), pax headers (`x`, `g`), and GNU sparse, incremental and volume entries. GNU tar writes long names this way by default, and Python's `tarfile` writes pax headers for long or non-ASCII names; - a GNU header with anything where ustar keeps its name prefix, such as the access and change times of an incremental dump; - a name or prefix field that is not valid UTF-8; - a base-256 size field, or a size field of spaces, which GNU tar refuses; - a regular typeflag with a name ending in `/`, which reads as a directory, and a size that is not zero, where readers disagree on whether data follows; + - a checksum over signed bytes, which some old tars wrote and GNU tar and `tarfile` accept; - any other magic, such as an old Unix V7 header. -- The Lean compiler, runtime, and kernel are trusted, as in every Lean project. A bug in them is outside the proof. +- Writing to disk. Extraction works on an in-memory list, so the step from a proved path to a safe write on a real filesystem (races, symlinks already on disk, a symlinked destination) is outside this project for now. The proofs resolve paths lexically, as POSIX does when no component is a symlink. +- The destination itself. The proofs say where a path lands relative to the destination, not whether the destination is a safe place to write. The destination is the command-line argument as the Lean runtime decodes it from UTF-8. + +## What you must trust + +- The Lean kernel and the five external kernels shipped with Lean, which all check the proofs. +- `lake comparator`, which builds the statements and the proofs in a sandbox, exports them, and checks that each proof proves exactly its statement. +- bubblewrap and the Linux kernel's namespaces, which keep the untrusted build from tampering with that check. +- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. +- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about (by `implemented_by` and `extern`), such as `Nat.repr` for the printed numbers and string comparison in the gate. +- The operating system and hardware it runs on. +- Python's `tarfile`, and the model of the format in `tests/run_tests.py`, as the oracle in the differential tests. The record names the Python version. + +This project has no dependencies beyond Lean itself. ## Re-check it +Needs Linux, [elan](https://github.com/leanprover/elan), bubblewrap (`apt install bubblewrap`), Python 3, and GNU tar, which writes some of the test archives. + ``` lake build -lake env lean TarPilot/Verify.lean +lake comparator --paranoid python3 tests/run_tests.py ``` -The build fails if a proof breaks, though it accepts a `sorry` with only a warning. The second command prints the axioms each theorem depends on. The test script builds the project first, fails if any theorem depends on an axiom other than the three standard ones, reruns every comparison, and rewrites `tests/TEST-RESULTS.md`. +`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. The test script builds the project, runs the fixed and random cases from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. ## Layout - `TarPilot/Path.lean`: the path gate. - `TarPilot/Octal.lean`: octal fields. -- `TarPilot/Header.lean`: the 512-byte ustar header, checksum, build and parse. -- `TarPilot/Archive.lean`: whole-archive parse and write, extraction, and the manifest the tool prints. -- `Spec/Defs.lean`: the definitions the theorems are stated with. -- `Proofs/Contain.lean`: the theorems and their proofs. -- `TarPilot/Verify.lean`: the axiom check. -- `Main.lean`: the command line front end. -- `tests/run_tests.py`: differential tests against Python's `tarfile`. +- `TarPilot/Header.lean`: the 512-byte header: checksum, build, and parse. +- `TarPilot/Archive.lean`: whole-archive parse and write, extraction, and the manifest and lines the tool prints. +- `Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file. +- `Spec/Defs.lean`: the definitions the statements use, with checks of examples. +- `Proofs.lean` and `Proofs/`: the proofs, under the same names. +- `Main.lean`: the command-line tool. +- `lakefile.toml`: the build. It names the package and its version, its libraries and executable, and the default targets, and sets nothing else. +- `comparator.json`: which theorems `lake comparator` checks, and which axioms it allows. +- `bar.toml`: the record for the bar check: status, authors, approvals, and where things are. +- `SPEC.md`: the specification in plain words. +- `tests/run_tests.py`: the differential tests. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..534790b --- /dev/null +++ b/SPEC.md @@ -0,0 +1,82 @@ +# Specification: tar + +A reader for tar archives that lists them and says where each regular file would be extracted, without letting any entry land outside the destination. A reviewer who did not write this specification approves it, together with `Spec.lean`, `Spec/Defs.lean`, and the other files `bar.toml` lists. + +Archives are bytes. Names are UTF-8 strings. The command-line tool reads a file and prints lines. + +## Reading an archive + +Scope: POSIX ustar, and GNU headers that carry nothing ustar does not. Anything outside the rules below makes the whole archive fail to parse, rather than be read in a way the pilot does not vouch for. + +An archive is a sequence of 512-byte header blocks and ends at a block of zeros. A header of a regular file is followed by its data, padded to a whole number of blocks. Links, devices, directories and FIFOs (types `1` to `6`) store no data, as POSIX says: the next header follows straight after, whatever their size field says, which is how GNU tar and Python's `tarfile` read them. A header is read only when all of these hold: + +- Bytes 257 to 264 are `ustar`, NUL, `00` (POSIX), or `ustar`, two spaces, NUL (GNU). A GNU header must have only zeros in bytes 345 to 499, where ustar keeps its name prefix and GNU keeps times, sparse maps, and volume offsets. +- The checksum field (bytes 148 to 155) is the sum of all 512 bytes, as unsigned numbers, counting the checksum field itself as spaces. A sum over signed bytes, which some old tars wrote and GNU tar and `tarfile` accept, is not read. +- The size field (bytes 124 to 135) and the checksum field are octal: leading spaces, then digits `0` to `7`, then NULs or spaces. A field with no digits reads as zero when it is all NUL, and is not read when it holds a space, as GNU tar refuses it. Base-256 fields are not read. +- The typeflag (byte 156) is NUL or one of `0` to `7`, the POSIX types. GNU long names and long links (`L`, `K`), pax headers (`x`, `g`), and any other type are not read. +- The name field (bytes 0 to 99) and the prefix field (bytes 345 to 499), each up to its first NUL, are valid UTF-8. The entry's name is the name field, or the prefix, `/`, and the name field when the prefix is not empty. +- A regular typeflag (NUL, `0`, `7`) with a name ending in `/`, which older archives use for a directory, has size zero: readers disagree on whether data follows such an entry. + +An archive fails to parse when a header is not read, when an entry's data runs past the end of the input, or when the input ends before a block of zeros. Then the tool prints nothing on standard output and exits with code 1, as it does when the file cannot be read. + +## The path gate + +Each entry's name goes through the gate, which gives the components the entry is extracted under, or rejects the name. The rules: + +- A name that starts with `/` is rejected. +- A name with a `..` component, or with a special character, is rejected. The special characters are the control characters (C0, DEL, and C1) and the Unicode line separator U+2028 and paragraph separator U+2029, which some readers take as line breaks. +- Empty and `.` components are dropped. +- A name with nothing left is rejected. + +So every component the gate gives is a plain name: not empty, not `.` or `..`, and free of `/` and of special characters. + +## Extraction + +Only regular files are extracted: typeflag `0`, NUL from older archives, or `7`, a contiguous file, which POSIX lets a reader treat as regular; and a name that does not end in `/`, which older archives use for a directory and GNU tar reads as one. Directories, links, devices, and FIFOs are skipped, so a link entry cannot place a later entry outside the destination. + +For each entry, in archive order, the outcome is one of: + +- extract: a regular file whose name passes the gate, at the destination followed by the gate's components, with the entry's own data; +- reject: a regular file whose name fails the gate; +- skip: any other entry. + +Extraction works on an in-memory list. Nothing is written to disk. + +## The command-line tool + +`tar-pilot list ` prints one line per entry: the name, its data size, and its typeflag as a decimal code, separated by tabs. + +`tar-pilot manifest ` prints one line per entry, separated by tabs: + +- `OK`, the path, the data size, and the sum of the data bytes, for an extracted entry. The path is the destination exactly as given, then the gate's components joined by `/`: after a `/` when the destination does not end in one, and with nothing before them when the destination is empty. +- `REJECT` and the name, for a rejected entry. +- `SKIP`, the name, and the typeflag code, for a skipped entry. + +In `list`, `REJECT` and `SKIP` lines, a backslash in a name is printed as two backslashes, U+2028 and U+2029 as `\u2028` and `\u2029`, and any other special character as `\x` and two lowercase hex digits. So a printed name holds no special character, which `Spec/Defs.lean` proves (`Spec.escape_noSpecial`). Every line ends in a line feed. A destination that holds a special character, or U+FFFD (which the Lean runtime puts in place of bytes that are not UTF-8), is refused, with exit code 2. + +`tar-pilot create ...` writes a ustar archive of the given files, each under the name given. A long name is split at a `/` into the prefix and name fields, and neither part may be empty, so an absolute name keeps its `/`. A name that does not fit makes it fail with exit code 1, writing nothing. + +Any other use prints a usage message and exits with code 2. + +## What must always hold + +Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use are in `Spec/Defs.lean`. + +| Property | Theorem | +|----------|---------| +| The gate is exactly its rules. | `TarPilot.gate_eq` | +| A name that passes the gate gives a non-empty list of plain names. | `TarPilot.gate_plain` | +| The outcome of each entry is as described under Extraction. | `TarPilot.manifest_eq` | +| The extracted outcomes are exactly the extractor's output, in order. | `TarPilot.manifest_extracted` | +| Each line `manifest` prints is exactly the line described above (`Spec.line`). | `TarPilot.manifest_lines_eq` | +| With a destination free of special characters, a line holds no special character but its tabs, and every `OK` line is the destination as given, then plain names joined by `/`, then a tab. | `TarPilot.manifest_lines` | +| Every extracted path is the destination followed by a non-empty list of plain names. | `TarPilot.extractAll_contained` | +| Joined with `/`, it splits back into the destination components and those names. | `TarPilot.extractAll_joined` | +| Resolved lexically, it is the resolved destination followed by those names, for entries or for an archive read from bytes. | `TarPilot.extractAll_resolves_inside`, `TarPilot.extractArchive_resolves_inside` | +| Extracting an archive read from bytes is parsing it, then extracting the entries. | `TarPilot.extractArchive_eq` | + +The statements fix what extraction, the gate, and the `manifest` output do with the entries of a parsed archive. How bytes are parsed into entries, the `list` output, `create`, and the few lines of `Main.lean` that print the manifest and check the destination are fixed by the rules above and checked by the differential tests, not by a proof. + +## Oracle + +Python's `tarfile` module, and a model of the format above written in `tests/run_tests.py` independently of the Lean code. The model is checked against `tarfile` on every unmutated archive both read. diff --git a/Spec.lean b/Spec.lean new file mode 100644 index 0000000..165aa53 --- /dev/null +++ b/Spec.lean @@ -0,0 +1,111 @@ +/- + The specification as Lean statements: the challenge file. + + A reviewer who did not write this file approves it, together with + `Spec/Defs.lean` and the other files `bar.toml` lists, and `bar.toml` + records the hash they had then. The proofs live in `Proofs/`, under the + same names; `lake comparator` checks that each one proves exactly the + statement written here. The `sorry` below is expected in this file + only. + + The statements are about the code in `TarPilot/`: the gate, the + extraction rule, the manifest, and the lines the command-line tool + prints. They do not cover how bytes are parsed into entries; the + differential tests do. +-/ + +import TarPilot +import Spec.Defs + +open Spec + +namespace TarPilot + +/-- The gate is exactly its rules (`Spec.cleanName`). -/ +theorem gate_eq (name : String) : gate name = Spec.cleanName name := sorry + +/-- The gate gives a non-empty list of plain names. -/ +theorem gate_plain (name : String) (rel : List String) : + gate name = some rel → rel ≠ [] ∧ ∀ c ∈ rel, PlainName c := sorry + +/-- What the manifest says about each entry: a regular file whose name + passes the gate is extracted at the destination followed by the + gate's components, with its data; a regular file whose name fails + is rejected; anything else is skipped. -/ +theorem manifest_eq (dest : List String) (entries : List RawEntry) : + manifest dest entries = entries.map fun e => + if regularType e.typeflag e.name then + match cleanName e.name with + | some rel => .extract (dest ++ rel) e.data + | none => .reject e.name + else .skip e.name e.typeflag := sorry + +/-- Every path `extractAll` emits is the destination followed by a + non-empty list of plain names. -/ +theorem extractAll_contained (dest : List String) (entries : List RawEntry) + (path : List String) (bytes : ByteArray) : + (path, bytes) ∈ extractAll dest entries → + ∃ rel, rel ≠ [] ∧ path = dest ++ rel ∧ ∀ c ∈ rel, PlainName c := sorry + +/-- Joined with `/`, an emitted path splits back into exactly the + destination components and the plain names, when no destination + component holds `/`. -/ +theorem extractAll_joined (dest : List String) (entries : List RawEntry) + (path : List String) (bytes : ByteArray) : + (∀ d ∈ dest, '/' ∉ d.toList) → + (path, bytes) ∈ extractAll dest entries → + ∃ rel, rel ≠ [] ∧ (∀ c ∈ rel, PlainName c) ∧ + pathComponents (joinPath path) = dest ++ rel := sorry + +/-- Resolved lexically, an emitted path is the resolved destination + followed by the plain names: no `..` in an archive reaches above the + destination. (`Spec.resolve` reads a relative path; for an absolute + destination, read both sides from the root.) -/ +theorem extractAll_resolves_inside (dest : List String) (entries : List RawEntry) + (path : List String) (bytes : ByteArray) : + (∀ d ∈ dest, '/' ∉ d.toList) → + (path, bytes) ∈ extractAll dest entries → + ∃ rel, rel ≠ [] ∧ (∀ c ∈ rel, PlainName c) ∧ + resolve [] (pathComponents (joinPath path)) = resolve [] dest ++ rel := sorry + +/-- The same for an archive read from bytes. -/ +theorem extractArchive_resolves_inside (dest : List String) (data : ByteArray) + (out : List (List String × ByteArray)) (path : List String) (bytes : ByteArray) : + (∀ d ∈ dest, '/' ∉ d.toList) → + extractArchive dest data = some out → (path, bytes) ∈ out → + ∃ rel, rel ≠ [] ∧ (∀ c ∈ rel, PlainName c) ∧ + resolve [] (pathComponents (joinPath path)) = resolve [] dest ++ rel := sorry + +/-- The entries the manifest extracts are exactly the output of + `extractAll`, in the same order. -/ +theorem manifest_extracted (dest : List String) (entries : List RawEntry) : + (manifest dest entries).filterMap Outcome.extracted = extractAll dest entries := sorry + +/-- What `tar-pilot manifest ` prints: one line, `o.line`, + for each outcome `o` of the manifest, given a destination with no + special character (the tool refuses any other). The only special + characters in a line are its tab separators, so no name can break a + line. And every line that starts with `OK` and a tab continues with + the given destination, then a non-empty list of plain names joined + by `/`, then a tab. (`manifest_lines_eq` gives each line exactly.) -/ +theorem manifest_lines (dest : String) (entries : List RawEntry) + (hdest : ∀ ch ∈ dest.toList, Spec.isSpecial ch = false) + (o : Outcome) (ho : o ∈ manifest (destComponents dest) entries) : + (∀ ch ∈ o.line.toList, Spec.isSpecial ch = true → ch = '\t') ∧ + (o.line.toList.take 3 = ['O', 'K', '\t'] → + ∃ rel rest, rel ≠ [] ∧ (∀ c ∈ rel, PlainName c) ∧ + o.line = "OK\t" ++ under dest (String.intercalate "/" rel) ++ "\t" ++ rest) := sorry + +/-- What `tar-pilot manifest ` prints, exactly: the line + for each entry is `Spec.line`, which `Spec/Defs.lean` writes out from + the rules. -/ +theorem manifest_lines_eq (dest : String) (entries : List RawEntry) : + (manifest (destComponents dest) entries).map Outcome.line = + entries.map fun e => Spec.line dest e.name e.typeflag e.data := sorry + +/-- Extracting an archive read from bytes is parsing it, then + `extractAll`. -/ +theorem extractArchive_eq (dest : List String) (data : ByteArray) : + extractArchive dest data = (parseArchive data).map (extractAll dest) := sorry + +end TarPilot diff --git a/TarPilot/Verify.lean b/TarPilot/Verify.lean deleted file mode 100644 index aeac8bf..0000000 --- a/TarPilot/Verify.lean +++ /dev/null @@ -1,20 +0,0 @@ -/- - Axiom check for the headline theorems. Building this file prints the - axioms each proof depends on. The expected output is only the three - standard Lean axioms: `propext`, `Classical.choice`, `Quot.sound`, - or a subset of them. Any other name here breaks the verified bar. --/ - -import Proofs - -#print axioms TarPilot.gate_eq -#print axioms TarPilot.gate_plain -#print axioms TarPilot.manifest_eq -#print axioms TarPilot.manifest_extracted -#print axioms TarPilot.manifest_lines -#print axioms TarPilot.manifest_lines_eq -#print axioms TarPilot.extractAll_contained -#print axioms TarPilot.extractAll_joined -#print axioms TarPilot.extractAll_resolves_inside -#print axioms TarPilot.extractArchive_eq -#print axioms TarPilot.extractArchive_resolves_inside diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..b1cf0b4 --- /dev/null +++ b/bar.toml @@ -0,0 +1,38 @@ +# Read by bar/check.py in Proven-Commons/mission. +# See playbook/verified-bar.md there for what each field means. + +[project] +name = "tar" +# "in-progress" until every bar item passes, then "verified". +status = "in-progress" +page = "README.md" +# GitHub handles of everyone who wrote the specification. It was drafted +# by Claude, an AI agent, for the org. +spec_authors = ["claude"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean"] +# The code under proof: the functions and types the statements are about. +code = [ + "TarPilot.gate", "TarPilot.manifest", "TarPilot.extractAll", "TarPilot.extractArchive", + "TarPilot.parseArchive", + "TarPilot.destComponents", "TarPilot.joinPath", + "TarPilot.Outcome", "TarPilot.Outcome.extract", "TarPilot.Outcome.reject", + "TarPilot.Outcome.skip", "TarPilot.Outcome.line", "TarPilot.Outcome.extracted", + "TarPilot.RawEntry", "TarPilot.RawEntry.name", "TarPilot.RawEntry.typeflag", + "TarPilot.RawEntry.data", +] + +# One entry per approval, added in a pull request the reviewer approves. +# [[spec.approval]] +# reviewer = "github-handle" +# date = "2026-11-02" +# sha256 = "..." +# record = "https://github.com/Proven-Commons/tar/pull/" + +[tests] +results = "tests/TEST-RESULTS.md" +command = "python3 tests/run_tests.py" +files = ["tests/run_tests.py"] diff --git a/comparator.json b/comparator.json new file mode 100644 index 0000000..cfa563e --- /dev/null +++ b/comparator.json @@ -0,0 +1,22 @@ +{ + "challenge_module": "Spec", + "solution_module": "Proofs", + "theorem_names": [ + "TarPilot.gate_eq", + "TarPilot.gate_plain", + "TarPilot.manifest_eq", + "TarPilot.extractAll_contained", + "TarPilot.extractAll_joined", + "TarPilot.extractAll_resolves_inside", + "TarPilot.extractArchive_resolves_inside", + "TarPilot.manifest_extracted", + "TarPilot.manifest_lines", + "TarPilot.manifest_lines_eq", + "TarPilot.extractArchive_eq" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ] +} diff --git a/lakefile.toml b/lakefile.toml index 0bda9f5..9fdbd84 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,6 @@ name = "TarPilot" [[lean_lib]] name = "Spec" -roots = ["Spec.Defs"] [[lean_lib]] name = "Proofs" diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 41926c5..1015436 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -1,29 +1,18 @@ # Test results -Run by `tests/run_tests.py` against Python's `tarfile` module. -Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.13.17. +Written by `tests/run_tests.py`. Rerun it to check these numbers. -- Checks run: 100 (13 of them on the axioms of the theorems) -- Failures: 0 +- Oracle: Python 3.13.17 `tarfile`, and the model of the format in `tests/run_tests.py`, which tarfile checks on every unmutated archive both read +- Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) +- Seed: 20261025 +- Inputs: 10055 +- Archives: 55 fixed, 10000 random +- Random archives: 10000, 5000 of them mutated; the model reads 4732, and tarfile agrees with it on all 3134 unmutated ones both read +- Checks run: 23243 - Archive A entries compared (list and manifest): 23 - Manifest outcome on archive A: 10 extracted, 9 rejected by the path gate, 4 skipped as non-regular - Files written by the Lean `create` command and read back by Python: 3 - Broken inputs rejected with exit code 1: truncated archive, random garbage, corrupted checksum -- Archives in formats the pilot does not read, rejected with exit code 1 by `list` and `manifest`: 27 -- Archives in other formats it reads, compared with tarfile: 11 - -Axiom check (`TarPilot/Verify.lean`): - -``` -'TarPilot.gate_eq' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.gate_plain' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.manifest_eq' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.manifest_extracted' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.manifest_lines' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.manifest_lines_eq' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.extractAll_contained' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.extractAll_joined' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.extractAll_resolves_inside' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.extractArchive_eq' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.extractArchive_resolves_inside' depends on axioms: [propext, Classical.choice, Quot.sound] -``` +- Archives in formats the pilot does not read, rejected with exit code 1 by `list` and `manifest`: 33 +- Archives in other formats it reads, compared with tarfile: 17 +- Failures: 0 diff --git a/tests/run_tests.py b/tests/run_tests.py index 3645b02..fa83ad0 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -1,19 +1,37 @@ #!/usr/bin/env python3 """Differential tests for the Proven Commons tar pilot. -Compares the Lean implementation against Python's `tarfile` module and -against an independent implementation of the extraction spec written -below. Run from anywhere: - - python3 tests/run_tests.py - -It builds the Lean project first, so it never checks stale code, runs -all cases in a temporary directory, writes `tests/TEST-RESULTS.md`, and -exits non-zero if any case fails. +Compares the tool's `list` and `manifest` commands against Python's +`tarfile` module and against a model of the format the pilot reads, +written below from SPEC.md, independently of the Lean code. Run from +anywhere: + + python3 tests/run_tests.py [--seed N] [--count N] + +It has two parts: + +- Fixed cases: an archive of normal, hostile and edge-case entries + written with tarfile, eleven destinations, archives written by the + tool and read back by tarfile, broken archives, and the formats the + pilot does not read (the probes of the 2026-10-24 bar audit). +- Random cases, from a recorded seed: archives written by tarfile in + ustar, GNU and pax formats, with hostile names, every POSIX entry + type, and random data, and the same kind of archives mutated (bytes + flipped, header fields overwritten with or without a fixed checksum, + cut, or extended). For each, the tool's output must equal the + model's. Where the model and tarfile both read an unmutated archive, + they must also agree on every entry, which checks the model against + an independent reader. + +It builds the Lean project first, so it never checks stale code, writes +`tests/TEST-RESULTS.md`, and exits non-zero if any case fails. The +proofs are checked by `lake comparator --paranoid`, not here. """ +import argparse import io import os +import platform import random import re import shutil @@ -26,12 +44,6 @@ PILOT_DIR = Path(__file__).resolve().parent.parent EXE = PILOT_DIR / ".lake" / "build" / "bin" / "tar-pilot" RESULTS = PILOT_DIR / "tests" / "TEST-RESULTS.md" -# The theorems `TarPilot/Verify.lean` prints the axioms of. -THEOREMS = ["gate_eq", "gate_plain", "manifest_eq", "manifest_extracted", "manifest_lines", - "manifest_lines_eq", "extractAll_contained", - "extractAll_joined", "extractAll_resolves_inside", "extractArchive_eq", - "extractArchive_resolves_inside"] - checks = 0 failures = [] @@ -180,6 +192,21 @@ def unsupported_archives(work): tarfile.USTAR_FORMAT, name, data=b"x", typ=typ) yield "size field of spaces", patch_header( one_file(tarfile.USTAR_FORMAT, "f", data=b""), 124, b" " * 12) + yield "digit 8 in the size field", patch_header( + one_file(tarfile.USTAR_FORMAT, "a.txt", data=b"x" * 8), 124, b"00000000008\0") + yield "NUL before the digits of the size field", patch_header( + one_file(tarfile.USTAR_FORMAT, "a.txt"), 124, b"\x000000000001\0") + yield "GNU magic with version 00", patch_header( + one_file(tarfile.GNU_FORMAT, "a.txt"), 263, b"00") + yield "GNU header with the last byte of the prefix area set", patch_header( + one_file(tarfile.GNU_FORMAT, "a.txt"), 499, b"\x01") + signed = bytearray(one_file(tarfile.USTAR_FORMAT, "\u00e9.txt", data=b"hi\n")) + signed[148:156] = b" " * 8 + signed[148:156] = b"%06o\0 " % sum(b - 256 if b > 127 else b for b in signed[:512]) + yield "checksum over signed bytes", bytes(signed) + end = bytearray(one_file(tarfile.USTAR_FORMAT, "a.txt")) + end[1024 + 511] = 1 + yield "a block of zeros but its last byte where the end should be", bytes(end) gnu_tar = shutil.which("tar") if gnu_tar: src = work / "systar-long" / "d" @@ -219,6 +246,18 @@ def readable_archives(work): for typ in [tarfile.LNKTYPE, tarfile.SYMTYPE, tarfile.CHRTYPE, tarfile.BLKTYPE, tarfile.DIRTYPE, tarfile.FIFOTYPE]: yield f"typeflag {typ.decode()} with a size field, then two files", hidden_after(typ) + yield "a 100-byte name", one_file(tarfile.USTAR_FORMAT, "f" * 96 + ".txt", data=b"full") + yield "a 155-byte prefix", one_file(tarfile.USTAR_FORMAT, "d" * 155 + "/f.txt", data=b"deep") + yield "a size field of 12 digits and no terminator", patch_header( + one_file(tarfile.USTAR_FORMAT, "a.txt", data=b"x" * 15), 124, b"000000000017") + yield "a size field ending in a space and a NUL", patch_header( + one_file(tarfile.USTAR_FORMAT, "a.txt", data=b"y"), 124, b"0000000001 \0") + seven = bytearray(one_file(tarfile.USTAR_FORMAT, "a.txt", data=b"z")) + seven[148:156] = b" " * 8 + seven[148:156] = b"%07o\0" % sum(seven[:512]) + yield "a checksum of seven digits", bytes(seven) + yield "a header with its last twelve bytes set", patch_header( + one_file(tarfile.USTAR_FORMAT, "a.txt", data=b"pad"), 500, b"padding1234!") gnu_tar = shutil.which("tar") if gnu_tar: src = work / "systar-short" @@ -350,7 +389,307 @@ def list_rows(stdout): return rows +# ---- A model of the format, from SPEC.md -------------------------------- + +USTAR_MAGIC = b"ustar\x0000" +GNU_MAGIC = b"ustar \x00" + + +def model_octal(field): + """An octal field: leading spaces, then digits 0 to 7, then NULs or + spaces. A field with no digits reads as 0 when it is all NUL, and is + invalid (None) when it holds a space. Anything else is invalid.""" + field = bytes(field) + digits = field.lstrip(b" ").rstrip(b"\x00 ") + if any(c < 0x30 or c > 0x37 for c in digits): + return None + if not digits: + return None if b" " in field else 0 + return int(digits, 8) + + +def model_name(field): + """A name field: the bytes before the first NUL, as UTF-8, or None.""" + try: + return bytes(field).split(b"\x00", 1)[0].decode("utf-8") + except UnicodeDecodeError: + return None + + +def model_header(block): + """(name, size, typeflag) of a header block, or None if the pilot + must not read it.""" + magic = block[257:265] + if not (magic == USTAR_MAGIC or (magic == GNU_MAGIC and block[345:500] == bytes(155))): + return None + stored = model_octal(block[148:156]) + if stored is None or stored != sum(block[:148]) + 8 * 32 + sum(block[156:512]): + return None + size = model_octal(block[124:136]) + typeflag = block[156] + if size is None or not (typeflag == 0 or 0x30 <= typeflag <= 0x37): + return None + name, prefix = model_name(block[0:100]), model_name(block[345:500]) + if name is None or prefix is None: + return None + full = name if prefix == "" else prefix + "/" + name + # Only regular typeflags are followed by data. A regular typeflag with + # a name ending in `/` is a directory, and must say size 0. + regular = typeflag in REGULAR_CODES + if regular and full.endswith("/") and size != 0: + return None + return full, (size if regular else 0), typeflag + + +def model_parse(data): + """The entries (name, data, typeflag) of an archive, or None when the + whole archive must fail to parse.""" + off, entries = 0, [] + while True: + if off + 512 > len(data): + return None + block = data[off:off + 512] + if block == bytes(512): + return entries + header = model_header(block) + if header is None: + return None + name, size, typeflag = header + start = off + 512 + if start + size > len(data): + return None + entries.append((name, data[start:start + size], typeflag)) + off = start + (size + 511) // 512 * 512 + + +def model_output(command, data, dest="out"): + """(exit code, stdout lines) the tool must give.""" + entries = model_parse(data) + if entries is None: + return 1, [] + if command == "list": + return 0, [f"{escape_name(n)}\t{len(d)}\t{t}" for n, d, t in entries] + return 0, expected_manifest(entries, dest) + + +# ---- Random archives ---------------------------------------------------- + +PARTS = ["a", "b", "x.txt", "..", ".", "", "é", "日本", "a b", "-", "\\", "..a", ":", + "\n", "\t", "\x7f", "\x85", "
", "n" * 60, "p" * 120] +TYPES = [tarfile.REGTYPE, tarfile.REGTYPE, tarfile.AREGTYPE, tarfile.CONTTYPE, + tarfile.DIRTYPE, tarfile.SYMTYPE, tarfile.LNKTYPE, tarfile.CHRTYPE, + tarfile.BLKTYPE, tarfile.FIFOTYPE] +FORMATS = [tarfile.USTAR_FORMAT, tarfile.USTAR_FORMAT, tarfile.GNU_FORMAT, tarfile.PAX_FORMAT] +DESTS = ["out", "out/", "/", "", "/srv/data", "a//b", "../up", "./o"] + + +def random_name(rng): + if rng.random() < 0.15: + # Lengths at the edges of the name and prefix fields. + kind = rng.randrange(3) + if kind == 0: + return "f" * (rng.choice([99, 100, 101]) - 4) + ".txt" + if kind == 1: + return "d" * rng.choice([154, 155, 156]) + "/f.txt" + return "d" * 150 + "/" + "f" * rng.choice([99, 100, 101]) + name = "/".join(rng.choice(PARTS) for _ in range(rng.randrange(1, 5))) + if rng.random() < 0.15: + name = "/" + name + if rng.random() < 0.1: + name += "/" + return name or "e" + + +def random_archive(rng): + """An archive written by tarfile with random entries.""" + buf = io.BytesIO() + with tarfile.open(fileobj=buf, mode="w", format=rng.choice(FORMATS)) as tf: + for _ in range(rng.randrange(1, 6)): + ti = tarfile.TarInfo(random_name(rng)) + ti.type = rng.choice(TYPES) + ti.mtime = 0 + data = b"" + if ti.type in (tarfile.REGTYPE, tarfile.AREGTYPE, tarfile.CONTTYPE): + # A regular typeflag with a name ending in `/` is a directory + # that must say size 0; give it data only sometimes. + if not ti.name.endswith("/") or rng.random() < 0.3: + data = rng.randbytes(rng.choice([0, 1, 511, 512, 513, rng.randrange(3000)])) + ti.size = len(data) + else: + if ti.type in (tarfile.SYMTYPE, tarfile.LNKTYPE): + ti.linkname = random_name(rng) + # tarfile writes the size field but no data for other types, + # which store none. + ti.size = rng.choice([0, 0, 0, 1, 512, 1024]) + regular = ti.type in (tarfile.REGTYPE, tarfile.AREGTYPE, tarfile.CONTTYPE) + try: + tf.addfile(ti, io.BytesIO(data) if regular else None) + except (ValueError, UnicodeError, tarfile.TarError): + pass + return buf.getvalue() + + +def header_offsets(data): + """Where the header blocks of an archive are, found by following the + size fields as a reader would, whether or not the headers are valid.""" + offs, off = [], 0 + while off + 512 <= len(data) and len(offs) < 64: + block = data[off:off + 512] + if block == bytes(512): + break + offs.append(off) + size = model_octal(block[124:136]) or 0 + off += 512 + ((size + 511) // 512 * 512 if block[156] in REGULAR_CODES else 0) + return offs + + +def field_value(rng, field): + """A value for one header field, often at the edge of what is valid.""" + n = rng.randrange(0, 1200) + if field == "size": + return rng.choice([b"%011o\0" % n, b"%012o" % n, b" %010o\0" % n, b"%010o \0" % n, + b"%010o\0 " % n, b"\0%010o\0" % n, b"%010o8\0" % n, b"%010o9 " % n, + b" " * 12, bytes(12), b"%011o " % n, b"\x80" + bytes(10) + b"\x01"]) + if field == "magic": + return rng.choice([b"ustar\x0000", b"ustar \x00", b"ustar\x00 ", b"ustar 00", + b"ustar\x00\x00\x00", b"ustar 0", b"ustar\x0001", b"USTAR\x0000"]) + if field == "typeflag": + return bytes([rng.choice(b"0123456789\x00LKxgSDAZ")]) + if field == "name": + return rng.choice([b"f" * 96 + b".txt", b"g" * 100, b"a\xffb", b"a\x00b.txt", + b"\xc3\xa9.txt", b"x/../y", b"/abs", b"dir/"]).ljust(100, b"\0") + if field == "prefix": + return rng.choice([b"d" * 155, b"d" * 154, bytes(154) + b"\x01", b"1" + bytes(154), + b"p\xff", b"pre"]).ljust(155, b"\0") + return bytes(rng.randrange(256) for _ in range(8)) + + +FIELDS = {"name": (0, 100), "mode": (100, 8), "size": (124, 12), "typeflag": (156, 1), + "magic": (257, 8), "prefix": (345, 155), "pad": (500, 12)} + + +def set_checksum(block, how): + """Write a checksum into a header block: the right one, the right one + in seven digits, the sum of signed bytes, or none (left stale).""" + if how == "stale": + return + block[148:156] = b" " * 8 + if how == "signed": + total = sum(b - 256 if b > 127 else b for b in block) + block[148:156] = b"%06o\0 " % (total % 0o1000000) + elif how == "seven": + block[148:156] = b"%07o\0" % sum(block) + else: + block[148:156] = b"%06o\0 " % sum(block) + + +def mutate(rng, data): + """One to three random changes to an archive, most of them to a field + of a header, with the checksum then made right, signed, seven digits, + or left stale.""" + out = bytearray(data) + for _ in range(rng.randrange(1, 4)): + kind = rng.randrange(8) + offs = header_offsets(bytes(out)) + if kind <= 3 and offs: + base = rng.choice(offs) + name = rng.choice(list(FIELDS)) + off, width = FIELDS[name] + value = field_value(rng, name)[:width] + if rng.random() < 0.3: + # Only the tail of the field. + cut = rng.randrange(width) + value = value[cut:] + off += cut + out[base + off:base + off + len(value)] = value + block = out[base:base + 512] + set_checksum(block, rng.choice(["right", "right", "right", "signed", "seven", "stale"])) + out[base:base + 512] = block + elif kind == 4 and out: + out[rng.randrange(len(out))] ^= 1 << rng.randrange(8) + elif kind == 5 and out: + del out[rng.randrange(len(out)):] + elif kind == 6: + out += rng.choice([bytes(512), bytes(1024), rng.randbytes(rng.randrange(1, 600))]) + else: + base = rng.randrange(max(1, len(out) // 512)) * 512 + del out[base:base + 512] + return bytes(out) + + +def tarfile_view_bytes(data): + """(name, data, typeflag) as tarfile reads each entry, or None.""" + try: + with tarfile.open(fileobj=io.BytesIO(data)) as tf: + return [(m.name, tf.extractfile(m).read() if m.isreg() else b"", m.type[0]) + for m in tf.getmembers()] + except (tarfile.TarError, UnicodeError, ValueError, OSError): + return None + + +def tarfile_agrees(data, entries): + """Whether tarfile reads what the model reads. tarfile drops the + trailing `/` of a directory name and returns no data for an entry that + is not a regular file. It reads an entry with typeflag NUL and a name + field ending in `/` as a directory, but misses that rule when the name + is split so the name field is empty, and reads typeflag `0` or `7` + with a trailing `/` as a regular file. The model, like GNU tar, reads + any regular typeflag with a name ending in `/` as a directory, so + such entries are compared as directories on both sides.""" + got = tarfile_view_bytes(data) + if got is None: + return False + + def norm(entries): + out = [] + for n, d, t in entries: + if t == 0x35 or (t in REGULAR_CODES and n.endswith("/")): + n, d, t = n.rstrip("/"), b"", 0x35 + out.append((n, d if t in REGULAR_CODES else b"", t)) + return out + return norm(got) == norm(entries) + + +def random_cases(seed, count, work): + """Run `count` random archives, every second one mutated.""" + rng = random.Random(seed) + stats = {"archives": 0, "mutated": 0, "read": 0, "tarfile": 0} + path = work / "random.tar" + for i in range(count): + data = random_archive(rng) + mutated = i % 2 == 1 + if mutated: + data = mutate(rng, data) + path.write_bytes(data) + stats["archives"] += 1 + stats["mutated"] += mutated + dest = rng.choice(DESTS) + for command in ("list", "manifest"): + args = [command, str(path)] + ([dest] if command == "manifest" else []) + r = run_lean(*args) + want_rc, want = model_output(command, data, dest) + got = output_lines(r.stdout) if r.stdout.endswith("\n") or not r.stdout else ["(no LF)"] + check(f"random {i} {command}", (r.returncode, got) == (want_rc, want), + f"seed={seed} rc={r.returncode} want_rc={want_rc} got={got[:3]} want={want[:3]}") + entries = model_parse(data) + if entries is not None: + stats["read"] += 1 + if not mutated: + agrees = tarfile_agrees(data, entries) + stats["tarfile"] += agrees + check(f"random {i} model agrees with tarfile", agrees, + f"seed={seed} model={entries[:3]} tarfile={(tarfile_view_bytes(data) or [])[:3]}") + return stats + + def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--seed", type=int, default=20261025) + ap.add_argument("--count", type=int, default=10000, + help="random archives, half of them mutated") + args = ap.parse_args() + if shutil.which("tar") is None: + sys.exit("needs GNU tar on PATH: some fixed cases are archives it writes") # A run that stops early must not leave an earlier passing record. RESULTS.unlink(missing_ok=True) build = subprocess.run(["lake", "build"], cwd=PILOT_DIR, capture_output=True, text=True) @@ -466,6 +805,12 @@ def main(): r = run_lean("list", str(badsum)) check("bad-checksum-fails", r.returncode == 1, f"rc={r.returncode}") + # 5b. Usage errors exit with code 2. + for bad_use in [[], ["frob"], ["manifest", str(archive_a)], ["list"]]: + r = run_lean(*bad_use) + check(f"usage {bad_use[:1]}", r.returncode == 2 and r.stdout == "", + f"rc={r.returncode}") + # 6. Formats the pilot does not read fail to parse, with exit # code 1 and nothing on standard output, for both commands. unsupported = 0 @@ -497,37 +842,33 @@ def main(): check(f"readable-manifest: {label}", r.returncode == 0 and got == want, f"rc={r.returncode} lean={got} expected={want}") - # 8. Axiom check: Verify.lean prints the axioms of exactly the - # theorems in THEOREMS, and each depends on the three standard axioms - # at most. Any other axiom, `sorryAx` included, fails the check. - ax = subprocess.run(["lake", "env", "lean", "TarPilot/Verify.lean"], - cwd=PILOT_DIR, capture_output=True, text=True) - ax_out = ax.stdout + ax.stderr - check("axioms-run", ax.returncode == 0, ax_out[:400]) - allowed = {"propext", "Classical.choice", "Quot.sound"} - records = {} - for m in re.finditer(r"'([\w.]+)' depends on axioms: \[(.*?)\]", ax_out, re.DOTALL): - records[m.group(1)] = {a.strip() for a in m.group(2).split(",") if a.strip()} - for m in re.finditer(r"'([\w.]+)' does not depend on any axioms", ax_out): - records[m.group(1)] = set() - expected = {f"TarPilot.{t}" for t in THEOREMS} - check("axioms-names", set(records) == expected, - f"printed {sorted(records)}, expected {sorted(expected)}") - for name, used in sorted(records.items()): - check(f"axioms-{name}", used <= allowed, f"axioms: {sorted(used)}") - - axiom_checks = len(records) + 2 - lean_ver = subprocess.run(["lean", "--version"], capture_output=True, - text=True).stdout.strip() + # Archive A, the tool's own archive, three broken ones, and the + # format probes. + fixed_archives = 1 + 1 + 3 + unsupported + readable + + # 8. Random archives from the seed. + stats = random_cases(args.seed, args.count, td) + lean_ver = subprocess.run(["lake", "env", "lean", "--version"], cwd=PILOT_DIR, + capture_output=True, text=True).stdout.strip() + + inputs = fixed_archives + stats["archives"] lines = [ "# Test results", "", - f"Run by `tests/run_tests.py` against Python's `tarfile` module.", - f"Lean: {lean_ver}. Python: {sys.version.split()[0]}.", + "Written by `tests/run_tests.py`. Rerun it to check these numbers.", "", - f"- Checks run: {checks} ({axiom_checks} of them on the axioms of the theorems)", - f"- Failures: {len(failures)}", + f"- Oracle: Python {platform.python_version()} `tarfile`, and the model of the " + f"format in `tests/run_tests.py`, which tarfile checks on every unmutated " + f"archive both read", + f"- Lean: {lean_ver}", + f"- Seed: {args.seed}", + f"- Inputs: {inputs}", + f"- Archives: {fixed_archives} fixed, {stats['archives']} random", + f"- Random archives: {stats['archives']}, {stats['mutated']} of them mutated; " + f"the model reads {stats['read']}, and tarfile agrees with it on all " + f"{stats['tarfile']} unmutated ones both read", + f"- Checks run: {checks}", f"- Archive A entries compared (list and manifest): {len(ref_entries)}", f"- Manifest outcome on archive A: {ok_count} extracted, " f"{rej_count} rejected by the path gate, {skip_count} skipped as non-regular", @@ -537,12 +878,7 @@ def main(): f"- Archives in formats the pilot does not read, rejected with exit code 1 " f"by `list` and `manifest`: {unsupported}", f"- Archives in other formats it reads, compared with tarfile: {readable}", - "", - "Axiom check (`TarPilot/Verify.lean`):", - "", - "```", - ax_out.strip(), - "```", + f"- Failures: {len(failures)}", "", ] if failures: From a923bf7d56adc2ac64e0b576d1f44fbbd59eb512 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 20:10:24 +0000 Subject: [PATCH 2/6] README: say that the test script does not run the comparator The test script checks the tool, not the proofs. A reader who runs it alone does not see the proof check (review question 5 on tar#6). Re-check it now says to run `lake comparator --paranoid` as well, and that CI's bar job runs both. The layout also names tests/compare_old.py, merged from tar#5. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index a8088c8..bd5f053 100644 --- a/README.md +++ b/README.md @@ -76,7 +76,7 @@ lake comparator --paranoid python3 tests/run_tests.py ``` -`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. The test script builds the project, runs the fixed and random cases from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. +`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. The test script builds the project, runs the fixed and random cases from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. It checks the tool, not the proofs, and does not run the comparator, so run the comparator as well. The bar job in CI (`.github/workflows/bar.yml`) runs both, through mission's `bar/check.py`. `python3 tests/compare_old.py --new 1273382` builds the tool as it was before the containment change (commit 7517a86) and the tool of that change (commit 1273382), and compares the two on 3,000 random archives under five destinations, from a recorded seed. Once the new escapes in names are undone, the output must be the same. It writes `tests/COMPARE-OLD.md`. Without `--new`, it compares this checkout's tool, and runs differ on purpose: some random names end in `/` with a regular typeflag, and this tool skips such an entry, or refuses the archive when the entry has data. @@ -99,3 +99,4 @@ python3 tests/run_tests.py - `bar.toml`: the record for the bar check: status, authors, approvals, and where things are. - `SPEC.md`: the specification in plain words. - `tests/run_tests.py`: the differential tests. +- `tests/compare_old.py`: the tool before the containment change and the tool of that change, compared on random archives. From 0fe94fcb0b7352225f31b444296c875015415d79 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 20:10:24 +0000 Subject: [PATCH 3/6] CI: say the pinned mission commit is on main, and what item 7 needs mission#2 merged on 2026-10-26, so 6ba85c27 is on mission's main now. bar/ and .github/ are the same there as at main's head (8ce7225). Mission has no release tag yet. The comment says so, and points to Proven-Commons/mission#10, which tracks both the tag and the branch rule that item 7 needs. Only a maintainer can set that rule (review questions 2 and 3 on tar#6). The pin itself is unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- .github/workflows/bar.yml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml index 32457ed..8bfd7c8 100644 --- a/.github/workflows/bar.yml +++ b/.github/workflows/bar.yml @@ -13,9 +13,12 @@ jobs: permissions: contents: read pull-requests: read - # Both lines pin the same commit of Proven-Commons/mission: bar v2, as - # proposed in its pull request #2. Move both to a release tag once - # mission publishes one. + # Both lines pin the same commit of Proven-Commons/mission: the bar v2 + # check from its pull request #2, now merged into main. Mission has no + # release tag yet. Move both lines to one once it publishes one + # (Proven-Commons/mission#10). + # Item 7 also needs `main` here to require this check. That is a repo + # setting only a maintainer can change, tracked in mission#10 too. uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2 with: bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2 From de0b0d84d99c92f2f11dbcd8f47dc669c96e0430 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 20:31:13 +0000 Subject: [PATCH 4/6] tests: count failures by kind of check, and rerun --tool 1273382 On this branch the random cases run against #4's tool too, and 10,305 of them fail there. Listing each one made the record 10,408 lines long. The record now has a table of each kind of check, with how many ran and how many failed. It lists every failure of a fixed case, and the first 20 failures of random cases. The script still prints them all as it runs. A run with no failures writes the same record as before. tests/TEST-RESULTS-1273382.md is rerun with this branch's script. 10,377 of the 23,269 checks fail against #4's tool: - 29 of the 35 archives that must fail to parse, under both commands; - 8 of the 19 readable archives under `manifest`, and 6 under `list`; - 5,184 of the 10,000 random archives under `list`, and 5,121 under `manifest`. The 3,134 checks of the model against tarfile do not run the tool, and pass. The page gives the new figure in place of #5's 68 of 107. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 2 +- tests/TEST-RESULTS-1273382.md | 88 +++++++++++++++++++++++++++++------ tests/run_tests.py | 29 +++++++++++- 3 files changed, 102 insertions(+), 17 deletions(-) diff --git a/README.md b/README.md index bd5f053..fd6e463 100644 --- a/README.md +++ b/README.md @@ -80,7 +80,7 @@ python3 tests/run_tests.py `python3 tests/compare_old.py --new 1273382` builds the tool as it was before the containment change (commit 7517a86) and the tool of that change (commit 1273382), and compares the two on 3,000 random archives under five destinations, from a recorded seed. Once the new escapes in names are undone, the output must be the same. It writes `tests/COMPARE-OLD.md`. Without `--new`, it compares this checkout's tool, and runs differ on purpose: some random names end in `/` with a regular typeflag, and this tool skips such an entry, or refuses the archive when the entry has data. -`python3 tests/run_tests.py --tool 1273382` runs the same checks against the tool of the containment change (commit 1273382), from before the parser changes. It leaves out the axiom check, which reads this checkout's proofs, not the tool, and writes `tests/TEST-RESULTS-1273382.md`: 68 of the 107 checks fail there. +`python3 tests/run_tests.py --tool 1273382` runs the same checks against the tool of the containment change (commit 1273382), from before the parser changes, and writes `tests/TEST-RESULTS-1273382.md`: 10,377 of the 23,269 checks fail there. The 3,134 checks of the model against `tarfile` do not run the tool, so they pass. `python3 tests/planted_bugs.py` plants, one at a time in a copy, a `sorry`, an axiom, an extra theorem that is not on the list, and a listed theorem left out of `TarPilot/Verify.lean`. It records that `lake build` passes on each and that the test script fails. It writes `tests/PLANTED-BUGS.md`. diff --git a/tests/TEST-RESULTS-1273382.md b/tests/TEST-RESULTS-1273382.md index f8ac273..c9c0052 100644 --- a/tests/TEST-RESULTS-1273382.md +++ b/tests/TEST-RESULTS-1273382.md @@ -1,25 +1,56 @@ # Test results -Run by `tests/run_tests.py --tool 1273382` against Python's `tarfile` module. -The tool was built from commit 1273382, not from this checkout. The axiom -check reads this checkout's proofs, not the tool, so it is left out. -Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.13.17. System tar: tar (GNU tar) 1.35. +Written by `tests/run_tests.py --tool 1273382`. The tool was built from +commit 1273382, not from this checkout. -- Checks run: 107, all on the tool -- Failures: 68 +- Oracle: Python 3.13.17 `tarfile`, and the model of the format in `tests/run_tests.py`, which tarfile checks on every unmutated archive both read +- Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) +- System tar: tar (GNU tar) 1.35 +- Seed: 20261025 +- Inputs: 10059 +- Archives: 59 fixed, 10000 random +- Random archives: 10000, 5000 of them mutated; the model reads 4732, and tarfile agrees with it on all 3134 unmutated ones both read +- Checks run: 23269 - Archive A entries compared (list and manifest): 23 - Manifest outcome on archive A: 10 extracted, 9 rejected by the path gate, 4 skipped as non-regular - Files written by the Lean `create` command and read back by Python: 3 - Broken inputs that must fail with exit code 1: truncated archive, random garbage, corrupted checksum -- Archives in formats the pilot does not read, which must fail with exit code 1 under `list` and `manifest`: 29 -- Archives in other formats it reads, compared with tarfile under `list` and `manifest`: 13 +- Archives in formats the pilot does not read, which must fail with exit code 1 under `list` and `manifest`: 35 +- Archives in other formats it reads, compared with tarfile under `list` and `manifest`: 19 +- Failures: 10377 -How the output is compared with tarfile. tarfile drops the `/` at the end of a -directory name, so directory names in `list` and names in `SKIP` lines are -compared without it. tarfile also reads an entry with typeflag NUL and a name -ending in `/` as a directory, typeflag 5, so for the readable archives the +How the fixed archives are compared with tarfile. tarfile drops the `/` at the +end of a directory name, so directory names in `list` and names in `SKIP` lines +are compared without it. tarfile also reads an entry with typeflag NUL and a +name ending in `/` as a directory, typeflag 5, so for the readable archives the tool's typeflag 0 on such an entry is read as 5. Every other typeflag is -compared as printed. +compared as printed. The random archives are compared with the model, and the +model with tarfile as `tarfile_agrees` in `tests/run_tests.py` says. + +## Failures by check + +| Check | Run | Failed | +|-------|-----|--------| +| list-exit | 1 | 0 | +| list-match | 1 | 0 | +| manifest-exit | 1 | 0 | +| manifest-match | 1 | 0 | +| manifest-dest | 7 | 0 | +| manifest-dest-refused | 6 | 0 | +| create-exit | 1 | 0 | +| create-readback | 1 | 0 | +| create-refuses-long-name | 1 | 0 | +| truncated-fails | 1 | 0 | +| garbage-fails | 1 | 0 | +| bad-checksum-fails | 1 | 0 | +| usage | 4 | 0 | +| unsupported-fails (list) | 35 | 29 | +| unsupported-fails (manifest) | 35 | 29 | +| readable-list | 19 | 6 | +| readable-manifest | 19 | 8 | +| random list | 10000 | 5184 | +| random manifest | 10000 | 5121 | +| random model agrees with tarfile | 3134 | 0 | ## Failures @@ -71,10 +102,14 @@ compared as printed. - unsupported-fails: name ending in / with typeflag b'0' and data (manifest): rc=0 out='OK\tout/e\t1\t120\n' - unsupported-fails: size field of spaces (list): rc=0 out='f\t0\t48\n' - unsupported-fails: size field of spaces (manifest): rc=0 out='OK\tout/f\t0\t0\n' +- unsupported-fails: GNU magic with version 00 (list): rc=0 out='a.txt\t1\t48\n' +- unsupported-fails: GNU magic with version 00 (manifest): rc=0 out='OK\tout/a.txt\t1\t120\n' +- unsupported-fails: GNU header with the last byte of the prefix area set (list): rc=0 out='a.txt\t1\t48\n' +- unsupported-fails: GNU header with the last byte of the prefix area set (manifest): rc=0 out='OK\tout/a.txt\t1\t120\n' - unsupported-fails: system tar, default format, long name (list): rc=0 out='d/\t0\t53\n././@LongLink\t127\t76\nd/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t48\n' - unsupported-fails: system tar, default format, long name (manifest): rc=0 out='SKIP\td/\t53\nSKIP\t././@LongLink\t76\nOK\tout/d/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t120\n' -- unsupported-fails: system tar, incremental dump (times in bytes 345 to 368) (list): rc=0 out='15267725440/a.txt\t3\t48\n' -- unsupported-fails: system tar, incremental dump (times in bytes 345 to 368) (manifest): rc=0 out='OK\tout/15267725440/a.txt\t3\t219\n' +- unsupported-fails: system tar, incremental dump (times in bytes 345 to 368) (list): rc=0 out='15267733331/a.txt\t3\t48\n' +- unsupported-fails: system tar, incremental dump (times in bytes 345 to 368) (manifest): rc=0 out='OK\tout/15267733331/a.txt\t3\t219\n' - unsupported-fails: system tar, sparse file (typeflag S, map in bytes 386 to 494) (list): rc=0 out='sparse\t3\t83\n' - unsupported-fails: system tar, sparse file (typeflag S, map in bytes 386 to 494) (manifest): rc=0 out='SKIP\tsparse\t83\n' - readable-manifest: contiguous file (typeflag 7): rc=0 lean=['SKIP\tcontig.bin\t55'] expected=['OK\tout/contig.bin\t10\t1104'] @@ -91,3 +126,26 @@ compared as printed. - readable-manifest: typeflag 5 with a size field, then two files: rc=0 lean=['SKIP\tnode\t53', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t53', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98'] - readable-list: typeflag 6 with a size field, then two files: rc=0 lean=[('node', 1024, 54), ('b.txt', 1, 48)] expected=[('node', 0, 54), ('hidden.txt', 6, 48), ('b.txt', 1, 48)] - readable-manifest: typeflag 6 with a size field, then two files: rc=0 lean=['SKIP\tnode\t54', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t54', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98'] +- random 0 list: seed=20261025 rc=0 want_rc=1 got=['/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn/\\x09\t0\t50', '\\x7f\t2436\t48', './x.txt\t1024\t54'] want=[] +- random 0 manifest: seed=20261025 rc=0 want_rc=1 got=['SKIP\t/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn/\\x09\t50', 'REJECT\t\\x7f', 'SKIP\t./x.txt\t54'] want=[] +- random 2 list: seed=20261025 rc=1 want_rc=0 got=[] want=['/é/..a/..a/../\t0\t53', '日本/日本\t2431\t0', '//a b/\t0\t53'] +- random 2 manifest: seed=20261025 rc=1 want_rc=0 got=[] want=['SKIP\t/é/..a/..a/../\t53', 'OK\tout/日本/日本\t2431\t315641', 'SKIP\t//a b/\t53'] +- random 3 list: seed=20261025 rc=0 want_rc=1 got=['././@PaxHeader\t135\t120', 'pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp\t0\t52', '././@PaxHeader\t19\t120'] want=[] +- random 3 manifest: seed=20261025 rc=0 want_rc=1 got=['SKIP\t././@PaxHeader\t120', 'SKIP\tpppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp\t52', 'SKIP\t././@PaxHeader\t120'] want=[] +- random 4 list: seed=20261025 rc=0 want_rc=0 got=['\\x85\t0\t50', '/a b/a/-\t513\t0', '/\\x85/é\t1\t52'] want=['\\x85\t0\t50', '/a b/a/-\t513\t0', '/\\x85/é\t0\t52'] +- random 9 list: seed=20261025 rc=0 want_rc=1 got=['..a\t1496\t48', '././@LongLink\t127\t76', 'pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp\t2709\t55'] want=[] +- random 9 manifest: seed=20261025 rc=0 want_rc=1 got=['OK\tout/..a\t1496\t193800', 'SKIP\t././@LongLink\t76', 'SKIP\tpppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp\t55'] want=[] +- random 10 list: seed=20261025 rc=0 want_rc=0 got=['a/\\\\/x.txt\t0\t0', 'a b/\\\\/a\t1024\t51'] want=['a/\\\\/x.txt\t0\t0', 'a b/\\\\/a\t0\t51', '../\\u2028\t0\t49'] +- random 10 manifest: seed=20261025 rc=0 want_rc=0 got=['OK\ta/\\/x.txt\t0\t0', 'SKIP\ta b/\\\\/a\t51'] want=['OK\ta/\\/x.txt\t0\t0', 'SKIP\ta b/\\\\/a\t51', 'SKIP\t../\\u2028\t49'] +- random 12 list: seed=20261025 rc=0 want_rc=1 got=['././@PaxHeader\t80\t120', 'a b/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn/:/?/\t0\t53', 'ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff.txt\t513\t48'] want=[] +- random 12 manifest: seed=20261025 rc=0 want_rc=1 got=['SKIP\t././@PaxHeader\t120', 'SKIP\ta b/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn/:/?/\t53', 'OK\t/ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff.txt\t513\t63981'] want=[] +- random 15 list: seed=20261025 rc=0 want_rc=1 got=['/..a/x.txt\t513\t48', '日本/\\u2028/\\\\\t0\t55', '\\x09/x.txt/-/\\x09\t0\t49'] want=[] +- random 15 manifest: seed=20261025 rc=0 want_rc=1 got=['REJECT\t/..a/x.txt', 'SKIP\t日本/\\u2028/\\\\\t55', 'SKIP\t\\x09/x.txt/-/\\x09\t49'] want=[] +- random 16 list: seed=20261025 rc=0 want_rc=1 got=['\\x0a\t0\t52', '/\\\\/\\\\\t0\t54', 'a b/..a/../.\t0\t55'] want=[] +- random 16 manifest: seed=20261025 rc=0 want_rc=1 got=['SKIP\t\\x0a\t52', 'SKIP\t/\\\\/\\\\\t54', 'SKIP\ta b/..a/../.\t55'] want=[] +- random 20 list: seed=20261025 rc=0 want_rc=1 got=['b/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn/:/\t0\t53', '..\t0\t54', '././@PaxHeader\t198\t120'] want=[] +- random 20 manifest: seed=20261025 rc=0 want_rc=1 got=['SKIP\tb/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn/:/\t53', 'SKIP\t..\t54', 'SKIP\t././@PaxHeader\t120'] want=[] +- random 23 manifest: seed=20261025 rc=0 want_rc=0 got=['SKIP\t\\x85\t54', 'SKIP\ta\t52', 'REJECT\t\\x7f/'] want=['SKIP\t\\x85\t54', 'SKIP\ta\t52', 'SKIP\t\\x7f/\t48'] + +This lists every failure of a fixed case, and the first 20 of the +10305 failures of random cases. The script prints them all as it runs. diff --git a/tests/run_tests.py b/tests/run_tests.py index 8590b8f..91642c7 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -58,12 +58,31 @@ RESULTS = PILOT_DIR / "tests" / "TEST-RESULTS.md" checks = 0 failures = [] +# For each kind of check, how many ran and how many failed. +kinds = {} +# The record lists every failure of a fixed case, and this many of the +# random cases; the script prints them all as it runs. +RANDOM_SHOWN = 20 + + +def kind_of(name): + """A check's name without the archive or destination it ran on.""" + if name.startswith("random "): + return "random " + name.split(" ", 2)[2] + kind = re.split(r"[ :]", name, maxsplit=1)[0] + for cmd in ("list", "manifest"): + if name.endswith(f"({cmd})"): + kind += f" ({cmd})" + return kind def check(name, ok, detail=""): global checks checks += 1 + count = kinds.setdefault(kind_of(name), [0, 0]) + count[0] += 1 if not ok: + count[1] += 1 failures.append(f"{name}: {detail}") print(f"FAIL {name}: {detail}") @@ -1012,7 +1031,15 @@ def main(): "", ] if failures: - lines += ["## Failures", ""] + [f"- {f}" for f in failures] + [""] + lines += ["## Failures by check", "", "| Check | Run | Failed |", "|-------|-----|--------|"] + lines += [f"| {k} | {n} | {f} |" for k, (n, f) in kinds.items()] + fixed = [f for f in failures if not f.startswith("random ")] + rand = [f for f in failures if f.startswith("random ")] + lines += ["", "## Failures", ""] + [f"- {f}" for f in fixed + rand[:RANDOM_SHOWN]] + [""] + if len(rand) > RANDOM_SHOWN: + lines += [f"This lists every failure of a fixed case, and the first {RANDOM_SHOWN} of the", + f"{len(rand)} failures of random cases. The script prints them all as it runs.", + ""] results.write_text("\n".join(lines)) print(f"{checks - len(failures)}/{checks} checks passed; results in {results}") return 1 if failures else 0 From 38696659b4b42a1c7abeadffc55a0a4cd009b46c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 20:47:04 +0000 Subject: [PATCH 5/6] tests: plant the proof faults against lake comparator planted_bugs.py came from tar#5, where TarPilot/Verify.lean and the test script's axiom check catch its faults. Here `lake comparator --paranoid` replaces both, so the faults are planted against it: - a `sorry`, and an axiom, behind the helper lemma resolve_plain; - an extra theorem in Spec.lean and comparator.json that the page does not claim, proved by `sorry`, and proved; - a statement of Spec.lean left out of comparator.json (manifest_lines), in place of a theorem left out of Verify.lean; - a `sorry`, and an axiom, in Spec.escape_noSpecial. On each copy the script runs lake build, the comparator, `#print axioms` for each listed theorem, the tests, and, with --bar, mission's bar/check.py. It records what each says, and runs the unchanged copy first, which must pass. lake build passes on all seven faults, and the tests report no failures. The comparator rejects the five with a `sorry` or an axiom. It accepts the other two, since it checks only the listed theorems. The bar check catches those: the extra theorem in item 2, and the statement left out in item 3. The script keeps both fixes from tar#4 (85ef13a). It stops with an error, and writes no record, when the tests give no check count. Its docstring says that a change that alters an answer a statement fixes stops lake build. Spec.escape_noSpecial is not in comparator.json. It says nothing about the code, and the bar check fails item 3 for a listed theorem whose statement mentions no code under proof: tried by hand, the comparator accepts it on the list, and the bar check then fails item 3. The proof of TarPilot.manifest_lines uses it, so its axioms are checked as axioms of that theorem, as the two rows on it show. The page now says so. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 5 +- tests/PLANTED-BUGS.md | 122 +++++++++++++---- tests/planted_bugs.py | 299 ++++++++++++++++++++++++++++++++---------- 3 files changed, 328 insertions(+), 98 deletions(-) diff --git a/README.md b/README.md index fd6e463..04a3b42 100644 --- a/README.md +++ b/README.md @@ -38,7 +38,7 @@ The gate's rules: a name that starts with `/` is rejected. A name with a `..` co | Resolved lexically, it is the resolved destination followed by those names, for an archive given as entries or as bytes: no `..` in an archive reaches above the destination. The resolution reads a path as relative and drops a leading `/`, so for an absolute destination read both sides from `/`. | `TarPilot.extractAll_resolves_inside`, `TarPilot.extractArchive_resolves_inside` | | Extracting an archive read from bytes is parsing it, then the extractor. | `TarPilot.extractArchive_eq` | -`Spec/Defs.lean` also proves, about the specification alone, that a printed name holds no special character, so it cannot break a line or a field (`Spec.escape_noSpecial`). +`Spec/Defs.lean` also proves, about the specification alone, that a printed name holds no special character, so it cannot break a line or a field (`Spec.escape_noSpecial`). It is not one of the statements in `Spec.lean`, and `comparator.json` does not list it: it says nothing about the code, and the bar check refuses a listed theorem whose statement mentions no code under proof. Its axioms are checked all the same, as axioms of `TarPilot.manifest_lines`, whose proof uses it. So a `sorry` or an axiom in it makes `lake comparator --paranoid` reject the proofs (`tests/PLANTED-BUGS.md`). ## What is not proved @@ -82,7 +82,7 @@ python3 tests/run_tests.py `python3 tests/run_tests.py --tool 1273382` runs the same checks against the tool of the containment change (commit 1273382), from before the parser changes, and writes `tests/TEST-RESULTS-1273382.md`: 10,377 of the 23,269 checks fail there. The 3,134 checks of the model against `tarfile` do not run the tool, so they pass. -`python3 tests/planted_bugs.py` plants, one at a time in a copy, a `sorry`, an axiom, an extra theorem that is not on the list, and a listed theorem left out of `TarPilot/Verify.lean`. It records that `lake build` passes on each and that the test script fails. It writes `tests/PLANTED-BUGS.md`. +`python3 tests/planted_bugs.py --bar /bar/check.py` plants seven faults, one at a time in a copy: a `sorry` and an axiom behind a helper lemma of the proofs; an extra theorem in `Spec.lean` and `comparator.json` that the page does not claim, proved by `sorry`, and proved; a statement of `Spec.lean` left out of `comparator.json`; and a `sorry` and an axiom in `Spec.escape_noSpecial`. Here `` is a checkout of Proven-Commons/mission at the commit `.github/workflows/bar.yml` pins. On each copy the script runs `lake build`, `lake comparator --paranoid`, the tests and the bar check, and it writes `tests/PLANTED-BUGS.md`. `lake build` passes on all seven, and the tests report no failures, since they check the tool. The comparator rejects the five with a `sorry` or an axiom. It checks only the theorems `comparator.json` lists, so it accepts the other two. The bar check catches those, in item 2 and in item 3. ## Layout @@ -100,3 +100,4 @@ python3 tests/run_tests.py - `SPEC.md`: the specification in plain words. - `tests/run_tests.py`: the differential tests. - `tests/compare_old.py`: the tool before the containment change and the tool of that change, compared on random archives. +- `tests/planted_bugs.py`: faults planted in the proofs and in the list of theorems checked, which the comparator or the bar check must catch. diff --git a/tests/PLANTED-BUGS.md b/tests/PLANTED-BUGS.md index f764a8c..460f8b5 100644 --- a/tests/PLANTED-BUGS.md +++ b/tests/PLANTED-BUGS.md @@ -1,17 +1,32 @@ # Planted bugs -Written by `python3 tests/planted_bugs.py`. Each row is one small change to the -proofs or to the axiom check, made in a copy. `lake build` ran on the copy, then -`tests/run_tests.py`. A fault is caught when the tests report failures. - -| Fault | Files | `lake build` | Failures | Failing checks | -|-------|-------|--------------|----------|----------------| -| sorry in a helper lemma (resolve_plain) | `Proofs/Contain.lean` | passes, warns of a `sorry` | 2 | axioms-TarPilot.extractAll_resolves_inside, axioms-TarPilot.extractArchive_resolves_inside | -| axiom cheat : False behind a helper lemma (resolve_plain) | `Proofs/Contain.lean` | passes | 2 | axioms-TarPilot.extractAll_resolves_inside, axioms-TarPilot.extractArchive_resolves_inside | -| extra unlisted theorem, proved by sorry | `Proofs/Contain.lean`, `TarPilot/Verify.lean` | passes, warns of a `sorry` | 2 | axioms-names, axioms-TarPilot.extra_claim | -| extra unlisted theorem, proved | `Proofs/Contain.lean`, `TarPilot/Verify.lean` | passes | 1 | axioms-names | -| listed theorem left out of Verify.lean (manifest_lines) | `TarPilot/Verify.lean` | passes | 1 | axioms-names | -| sorry in Spec.escape_noSpecial | `Spec/Defs.lean` | passes, warns of a `sorry` | 2 | axioms-Spec.escape_noSpecial, axioms-TarPilot.manifest_lines | +Written by `python3 tests/planted_bugs.py --bar /bar/check.py`. + +Each row is one small change to the proofs, the statements, or the list of +theorems checked, made in a copy. On each copy these ran, in this order: + +- `lake build`; +- `lake comparator --paranoid`; +- `#print axioms` for each theorem `comparator.json` lists; +- `tests/run_tests.py --count 1000`; +- mission's `bar/check.py --offline`. + +The first row is the copy left as it is. A fault is caught when the comparator +rejects it, the tests report failures, or the bar check gives an item another +status than it gives the unchanged copy. + +On the unchanged copy, the bar check gives: item 1 OPEN, item 2 PASS, item 3 PASS, item 4 PASS, item 5 PASS, item 6 PASS, item 7 SKIP. + +| Fault | Files | `lake build` | `lake comparator --paranoid` | Axioms beyond the three | Test failures | Bar check, where it differs | Caught | +|-------|-------|--------------|------------------------------|-------------------------|---------------|-----------------------------|--------| +| none: the copy as it is | none | passes | accepts | none | 0 | the same | (none planted) | +| sorry in a helper lemma (resolve_plain) | `Proofs/Contain.lean` | passes, warns of a `sorry` in `Proofs/Contain.lean` | rejects: error: Illegal axiom detected: 'sorryAx' | TarPilot.extractAll_resolves_inside: sorryAx; TarPilot.extractArchive_resolves_inside: sorryAx | 0 | item 3: PASS to OPEN: `lake comparator --paranoid`: a proof is still `sorry`, which an in-progress project may have; item 4: PASS to OPEN: unfinished proofs, which an in-progress project may have: Proofs/Contain.lean:174 sorry | yes | +| axiom cheat : False behind a helper lemma (resolve_plain) | `Proofs/Contain.lean` | passes | rejects: error: Illegal axiom detected: 'TarPilot.Contain.cheat' | TarPilot.extractAll_resolves_inside: TarPilot.Contain.cheat; TarPilot.extractArchive_resolves_inside: TarPilot.Contain.cheat | 0 | item 3: PASS to FAIL: `lake comparator --paranoid` exited 1: ... error: Illegal axiom detected: 'TarPilot.Contain.cheat'; item 4: PASS to FAIL: forbidden features: Proofs/Contain.lean:172 axiom | yes | +| extra theorem the page does not claim, proved by sorry | `Proofs/Contain.lean`, `Spec.lean`, `comparator.json` | passes, warns of a `sorry` in `Proofs/Contain.lean` | rejects: error: Illegal axiom detected: 'sorryAx' | TarPilot.extra_claim: sorryAx | 0 | item 2: PASS to OPEN: 'What is proved' does not name: TarPilot.extra_claim; item 3: PASS to OPEN: `lake comparator --paranoid`: a proof is still `sorry`, which an in-progress project may have; item 4: PASS to OPEN: unfinished proofs, which an in-progress project may have: Proofs/Contain.lean:537 sorry | yes | +| extra theorem the page does not claim, proved | `Proofs/Contain.lean`, `Spec.lean`, `comparator.json` | passes | accepts | none | 0 | item 2: PASS to OPEN: 'What is proved' does not name: TarPilot.extra_claim | yes | +| theorem of Spec.lean left out of comparator.json (manifest_lines) | `comparator.json` | passes | accepts | none | 0 | item 3: PASS to FAIL: `lake comparator --paranoid` passes, but comparator.json does not name these theorems of the challenge file: TarPilot.manifest_lines | yes | +| sorry in Spec.escape_noSpecial | `Spec/Defs.lean` | passes, warns of a `sorry` in `Spec/Defs.lean` | rejects: error: Illegal axiom detected: 'sorryAx' | TarPilot.manifest_lines: sorryAx | 0 | item 3: PASS to OPEN: `lake comparator --paranoid`: a proof is still `sorry`, which an in-progress project may have; item 4: PASS to OPEN: unfinished proofs, which an in-progress project may have: Spec/Defs.lean:123 sorry | yes | +| axiom cheat : False behind Spec.escape_noSpecial | `Spec/Defs.lean` | passes | rejects: error: Illegal axiom detected: 'Spec.cheat' | TarPilot.manifest_lines: Spec.cheat | 0 | item 3: PASS to FAIL: `lake comparator --paranoid` exited 1: ... error: Illegal axiom detected: 'Spec.cheat'; item 4: PASS to FAIL: forbidden features: Spec/Defs.lean:119 axiom | yes | ## The changes @@ -57,7 +72,21 @@ proofs or to the axiom check, made in a copy. `lake build` ran on the copy, then + exact cheat.elim ``` -**extra unlisted theorem, proved by sorry** in `Proofs/Contain.lean`: +**extra theorem the page does not claim, proved by sorry** in `Spec.lean`: + +``` +- (parseArchive data).map (extractAll dest) := sorry +- +- end TarPilot ++ (parseArchive data).map (extractAll dest) := sorry ++ ++ /-- Not a claim of the page. -/ ++ theorem extra_claim : gate ".." = none := sorry ++ ++ end TarPilot +``` + +**extra theorem the page does not claim, proved by sorry** in `Proofs/Contain.lean`: ``` - (extractAll dest) := rfl @@ -70,15 +99,31 @@ proofs or to the axiom check, made in a copy. `lake build` ran on the copy, then + theorem TarPilot.extra_claim : TarPilot.gate ".." = none := sorry ``` -**extra unlisted theorem, proved by sorry** in `TarPilot/Verify.lean`: +**extra theorem the page does not claim, proved by sorry** in `comparator.json`: ``` -- #print axioms Spec.escape_noSpecial -+ #print axioms Spec.escape_noSpecial -+ #print axioms TarPilot.extra_claim +- "TarPilot.extractArchive_eq" +- ], ++ "TarPilot.extractArchive_eq", ++ "TarPilot.extra_claim" ++ ], ``` -**extra unlisted theorem, proved** in `Proofs/Contain.lean`: +**extra theorem the page does not claim, proved** in `Spec.lean`: + +``` +- (parseArchive data).map (extractAll dest) := sorry +- +- end TarPilot ++ (parseArchive data).map (extractAll dest) := sorry ++ ++ /-- Not a claim of the page. -/ ++ theorem extra_claim : gate ".." = none := sorry ++ ++ end TarPilot +``` + +**extra theorem the page does not claim, proved** in `Proofs/Contain.lean`: ``` - (extractAll dest) := rfl @@ -88,21 +133,26 @@ proofs or to the axiom check, made in a copy. `lake build` ran on the copy, then + + end TarPilot + -+ theorem TarPilot.extra_claim : True := trivial ++ theorem TarPilot.extra_claim : TarPilot.gate ".." = none := by ++ rw [TarPilot.gate_eq] ++ simp only [Spec.cleanName, Spec.pathComponents, String.toList_split_char] ++ decide ``` -**extra unlisted theorem, proved** in `TarPilot/Verify.lean`: +**extra theorem the page does not claim, proved** in `comparator.json`: ``` -- #print axioms Spec.escape_noSpecial -+ #print axioms Spec.escape_noSpecial -+ #print axioms TarPilot.extra_claim +- "TarPilot.extractArchive_eq" +- ], ++ "TarPilot.extractArchive_eq", ++ "TarPilot.extra_claim" ++ ], ``` -**listed theorem left out of Verify.lean (manifest_lines)** in `TarPilot/Verify.lean`: +**theorem of Spec.lean left out of comparator.json (manifest_lines)** in `comparator.json`: ``` -- #print axioms TarPilot.manifest_lines +- "TarPilot.manifest_lines", + ``` @@ -120,6 +170,28 @@ proofs or to the axiom check, made in a copy. `lake build` ran on the copy, then + sorry ``` +**axiom cheat : False behind Spec.escape_noSpecial** in `Spec/Defs.lean`: + +``` +- /-- A printed name holds no special character, so it cannot break a line +- or a field of the tool's output. -/ +- theorem escape_noSpecial (s : String) : +- ∀ ch ∈ (escape s).toList, isSpecial ch = false := by +- intro ch hch +- unfold escape at hch +- rw [String.toList_join, List.mem_flatMap] at hch +- obtain ⟨t, ht, hc⟩ := hch +- obtain ⟨c, _, rfl⟩ := List.mem_map.mp ht +- exact escapeChar_noSpecial c ch hc ++ axiom cheat : False ++ ++ /-- A printed name holds no special character, so it cannot break a line ++ or a field of the tool's output. -/ ++ theorem escape_noSpecial (s : String) : ++ ∀ ch ∈ (escape s).toList, isSpecial ch = false := by ++ exact cheat.elim +``` + ## Not here The review rounds the PR describes also built changes to the code under proof. diff --git a/tests/planted_bugs.py b/tests/planted_bugs.py index 6d6d5ac..fbc70f8 100644 --- a/tests/planted_bugs.py +++ b/tests/planted_bugs.py @@ -1,37 +1,51 @@ #!/usr/bin/env python3 -"""Plant each fault below in a copy of the project, and check the tests catch it. +"""Plant each fault below in a copy of the project, and record what catches it. -The faults here are the three the PR for audit F1 and F5 names: a -planted `sorry`, a planted axiom, and an extra theorem that is not on -the list. Two more are added: a listed theorem left out of -`TarPilot/Verify.lean`, and a `sorry` in `Spec.escape_noSpecial`, -which review question 2 asks about. +The faults are the four the PR for audit F1 and F5 names, planted +against the proof check this branch uses, `lake comparator --paranoid`: +a `sorry` and an axiom behind a helper lemma, an extra theorem, and a +theorem left out of the list the comparator checks, `comparator.json`. +Two more are a `sorry` and an axiom in `Spec.escape_noSpecial`, which +`comparator.json` does not list: the proof of `TarPilot.manifest_lines` +uses it, so the comparator checks it with that theorem. What the proofs catch: a change to the code under proof that alters an answer a statement fixes stops `lake build`, since the proof of that statement no longer goes through. What they do not catch: a fault in the proofs themselves, or in the list of theorems checked. That is every fault here, and `lake build` passes on each: Lean accepts a -`sorry` with a warning, and an axiom, an extra theorem or a missing -`#print axioms` line with none. What catches them is the axiom check -in `tests/run_tests.py`, which reads what `TarPilot/Verify.lean` -prints. Nor do the proofs cover header parsing, archive writing, the -`list` output or `Main.lean`. Only the tests cover those, and no fault -is planted there. +`sorry` with a warning, and an axiom, an extra theorem or a name left +out of `comparator.json` with none. `lake comparator --paranoid` +rejects a `sorry` or an axiom in the proof of a theorem it checks, or +in anything that proof uses. It checks only the theorems +`comparator.json` lists. So it cannot see a listed theorem that the +page does not claim, or a statement in `Spec.lean` that the list leaves +out. Mission's `bar/check.py` checks those (items 2 and 3); pass +`--bar` to run it on each copy. The tests in `tests/run_tests.py` check +the tool, not the proofs, so they report no failures here. Nor do the +proofs cover header parsing, archive writing, the `list` output or +`Main.lean`. Only the tests cover those, and no fault is planted there. For each fault, this script copies the project into a temporary -directory, makes the change there, runs `lake build` and records -whether it passes, then runs `python3 tests/run_tests.py` and counts -its failures. A fault is caught when that script reports failures. The -project itself is never changed. The script writes the results to -tests/PLANTED-BUGS.md. It stops with an error, and writes no record, -if a test run gives no check count or a count that does not match its -exit status. It exits with 1 if a fault is not caught and is not -marked as equivalent. - -Usage: python3 tests/planted_bugs.py +directory and makes the change there. On the copy it runs `lake build`, +`lake comparator --paranoid`, `#print axioms` for each theorem +`comparator.json` lists, `python3 tests/run_tests.py --count N`, and, +with `--bar CHECK`, `python3 CHECK COPY --offline`. The first row is the +copy left as it is, and it must pass all of these. A fault is caught +when the comparator rejects it, the tests report failures, or the bar +check gives an item another status than it gives the unchanged copy. +The project itself is never changed. + +The script writes the results to tests/PLANTED-BUGS.md. It stops with +an error, and writes no record, if a test run gives no check count or a +count that does not match its exit status. It exits with 1 if a fault is +caught by nothing it ran and is not marked as equivalent. + +Usage: python3 tests/planted_bugs.py [--count N] [--bar PATH/TO/mission/bar/check.py] """ +import argparse +import json import re import shutil import subprocess @@ -40,6 +54,8 @@ from pathlib import Path ROOT = Path(__file__).resolve().parent.parent +COUNT = 1000 # random archives for each test run; the tests do not read the proofs +STANDARD = {"propext", "Classical.choice", "Quot.sound"} RESOLVE_PLAIN = """theorem resolve_plain : ∀ (rel acc : List String), (∀ c ∈ rel, PlainName c) → resolve acc rel = acc ++ rel := by @@ -57,19 +73,31 @@ RESOLVE_PLAIN_STMT = """theorem resolve_plain : ∀ (rel acc : List String), (∀ c ∈ rel, PlainName c) → resolve acc rel = acc ++ rel """ -ESCAPE_PROOF = """ ∀ ch ∈ (escape s).toList, isSpecial ch = false := by - intro ch hch +ESCAPE_STMT = " ∀ ch ∈ (escape s).toList, isSpecial ch = false := by\n" +ESCAPE_PROOF = ESCAPE_STMT + """ intro ch hch unfold escape at hch rw [String.toList_join, List.mem_flatMap] at hch obtain ⟨t, ht, hc⟩ := hch obtain ⟨c, _, rfl⟩ := List.mem_map.mp ht exact escapeChar_noSpecial c ch hc""" +ESCAPE_HEAD = ("/-- A printed name holds no special character, so it cannot break a line\n" + " or a field of the tool's output. -/\ntheorem escape_noSpecial (s : String) :\n") +SPEC_END = "(parseArchive data).map (extractAll dest) := sorry\n\nend TarPilot\n" +SPEC_EXTRA = ("(parseArchive data).map (extractAll dest) := sorry\n\n" + "/-- Not a claim of the page. -/\n" + "theorem extra_claim : gate \"..\" = none := sorry\n\nend TarPilot\n") CONTAIN_END = "(extractAll dest) := rfl\n\nend TarPilot\n" -VERIFY_END = "#print axioms Spec.escape_noSpecial\n" +EXTRA_STMT = "\ntheorem TarPilot.extra_claim : TarPilot.gate \"..\" = none :=" +EXTRA_PROOF = (" by\n rw [TarPilot.gate_eq]\n" + " simp only [Spec.cleanName, Spec.pathComponents, String.toList_split_char]\n" + " decide\n") +LIST_END = ' "TarPilot.extractArchive_eq"\n ],' +LIST_EXTRA = ' "TarPilot.extractArchive_eq",\n "TarPilot.extra_claim"\n ],' # (name, [(file, text to replace, replacement)], why it is equivalent or None) BUGS = [ + ("none: the copy as it is", [], None), # A helper lemma proved by `sorry` or by an axiom. Two of the listed # theorems use it: extractAll_resolves_inside, and through it # extractArchive_resolves_inside. @@ -80,28 +108,33 @@ [("Proofs/Contain.lean", RESOLVE_PLAIN, "axiom cheat : False\n\n" + RESOLVE_PLAIN_STMT + ":= by\n exact cheat.elim\n")], None), - # An extra theorem that Verify.lean prints but the list does not - # hold. The first row proves it by `sorry`; the second proves it - # without one, so only the check on the names can catch it. - ("extra unlisted theorem, proved by sorry", - [("Proofs/Contain.lean", CONTAIN_END, - CONTAIN_END + "\ntheorem TarPilot.extra_claim : TarPilot.gate \"..\" = none := sorry\n"), - ("TarPilot/Verify.lean", VERIFY_END, VERIFY_END + "#print axioms TarPilot.extra_claim\n")], + # An extra theorem that comparator.json lists, with its statement in + # Spec.lean, but that the page does not claim. The first row proves + # it by `sorry`; the second proves it, so only a check of the names + # against the page can catch it. + ("extra theorem the page does not claim, proved by sorry", + [("Spec.lean", SPEC_END, SPEC_EXTRA), + ("Proofs/Contain.lean", CONTAIN_END, CONTAIN_END + EXTRA_STMT + " sorry\n"), + ("comparator.json", LIST_END, LIST_EXTRA)], None), - ("extra unlisted theorem, proved", - [("Proofs/Contain.lean", CONTAIN_END, - CONTAIN_END + "\ntheorem TarPilot.extra_claim : True := trivial\n"), - ("TarPilot/Verify.lean", VERIFY_END, VERIFY_END + "#print axioms TarPilot.extra_claim\n")], + ("extra theorem the page does not claim, proved", + [("Spec.lean", SPEC_END, SPEC_EXTRA), + ("Proofs/Contain.lean", CONTAIN_END, CONTAIN_END + EXTRA_STMT + EXTRA_PROOF), + ("comparator.json", LIST_END, LIST_EXTRA)], None), - # Not named by the PR. A listed theorem left out of Verify.lean, which - # only the check on the names can catch, and a sorry in the theorem - # review question 2 asks about. - ("listed theorem left out of Verify.lean (manifest_lines)", - [("TarPilot/Verify.lean", "#print axioms TarPilot.manifest_lines\n", "")], + # A statement of Spec.lean, claimed on the page, that comparator.json + # leaves out, so nothing checks its proof. + ("theorem of Spec.lean left out of comparator.json (manifest_lines)", + [("comparator.json", ' "TarPilot.manifest_lines",\n', "")], None), + # Spec.escape_noSpecial is not listed; the proof of manifest_lines + # uses it. ("sorry in Spec.escape_noSpecial", - [("Spec/Defs.lean", ESCAPE_PROOF, - " ∀ ch ∈ (escape s).toList, isSpecial ch = false := by\n sorry")], + [("Spec/Defs.lean", ESCAPE_PROOF, ESCAPE_STMT + " sorry")], + None), + ("axiom cheat : False behind Spec.escape_noSpecial", + [("Spec/Defs.lean", ESCAPE_HEAD + ESCAPE_PROOF, + "axiom cheat : False\n\n" + ESCAPE_HEAD + ESCAPE_STMT + " exact cheat.elim")], None), ] @@ -113,26 +146,85 @@ def failures(out): return int(m.group(2)) - int(m.group(1)) if m else None -def run(): +def sorry_files(out): + """The files `lake build` warns of a `sorry` in, other than + Spec.lean, where every statement has one.""" + files = set(re.findall(r"warning: (\S+?):\d+:\d+: declaration uses `sorry`", out)) + return sorted(files - {"Spec.lean"}) + + +def comparator(work): + """(exit code, what it says) for `lake comparator --paranoid`.""" + r = subprocess.run(["lake", "comparator", "--paranoid"], cwd=work, capture_output=True, + text=True) + out = r.stdout + r.stderr + if r.returncode == 0: + return 0, "accepts" + errors = [l.strip() for l in out.splitlines() if l.strip().startswith("error")] + return r.returncode, "rejects: " + (errors[-1] if errors else out.strip().splitlines()[-1]) + + +def other_axioms(work): + """The theorems comparator.json lists whose axioms go beyond the + three standard ones, with those axioms.""" + names = json.loads((work / "comparator.json").read_text())["theorem_names"] + src = work / "PlantedAxioms.lean" + src.write_text("import Proofs\n" + "".join(f"#print axioms {n}\n" for n in names)) + r = subprocess.run(["lake", "env", "lean", src.name], cwd=work, capture_output=True, + text=True) + src.unlink() + out = r.stdout + r.stderr + found = [] + for m in re.finditer(r"'([\w.]+)' depends on axioms: \[(.*?)\]", out, re.DOTALL): + extra = sorted({a.strip() for a in m.group(2).split(",")} - STANDARD) + if extra: + found.append(f"{m.group(1)}: {', '.join(extra)}") + if r.returncode != 0 and not found: + found.append(f"`#print axioms` failed: {out.strip().splitlines()[-1]}") + return found + + +def short(detail): + """A bar check detail without the middle of a command's output: the + check joins the last lines of that output with " / ".""" + if " / " not in detail: + return detail + return detail.split(": ", 1)[0] + ": ... " + detail.rsplit(" / ", 1)[1] + + +def bar_items(check, work, tmp): + """{item: (status, detail)} from mission's bar check, offline.""" + report = Path(tmp) / "bar.json" + subprocess.run([sys.executable, str(check), str(work), "--offline", "--json", str(report)], + capture_output=True, text=True) + if not report.is_file(): + sys.exit(f"the bar check wrote no report for {work}") + items = {r["item"]: (r["status"], r["detail"]) for r in json.loads(report.read_text())["items"]} + report.unlink() + return items + + +def run(count, check): rows = [] with tempfile.TemporaryDirectory() as tmp: work = Path(tmp) / "project" shutil.copytree(ROOT, work, ignore=shutil.ignore_patterns(".git")) + base_bar = None for name, edits, equivalent in BUGS: originals = {} for rel, old, new in edits: path = work / rel - text = originals.setdefault(rel, (ROOT / rel).read_text()) + originals.setdefault(rel, (ROOT / rel).read_text()) current = path.read_text() if current.count(old) != 1: sys.exit(f"{name}: the text to replace is not in {rel} exactly once") path.write_text(current.replace(old, new)) build = subprocess.run(["lake", "build"], cwd=work, capture_output=True, text=True) - warned = "declaration uses `sorry`" in build.stdout + build.stderr - test = subprocess.run([sys.executable, "tests/run_tests.py"], + warned = sorry_files(build.stdout + build.stderr) + cmp_code, cmp_says = comparator(work) + axioms = other_axioms(work) + test = subprocess.run([sys.executable, "tests/run_tests.py", "--count", str(count)], cwd=work, capture_output=True, text=True) - for rel, text in originals.items(): - (work / rel).write_text(text) out = test.stdout + test.stderr n = failures(out) if n is None: @@ -140,30 +232,84 @@ def run(): if (n > 0) != (test.returncode != 0): sys.exit(f"{name}: the tests report {n} failures but exit with " f"{test.returncode}\n{out[-2000:]}") - fails = [l[5:].split(":")[0] for l in test.stdout.splitlines() if l.startswith("FAIL ")] - rows.append((name, edits, equivalent, build.returncode, warned, n, fails)) - print(f"{name}: build exit {build.returncode}, {n} failures", flush=True) - return rows + bar = None + if check: + items = bar_items(check, work, tmp) + if base_bar is None: + base_bar = items + bar = [f"item {i}: {base_bar.get(i, ('none',))[0]} to {s}: {short(d)}" + for i, (s, d) in sorted(items.items()) if base_bar.get(i, (None,))[0] != s] + for rel, text in originals.items(): + (work / rel).write_text(text) + if not edits and (build.returncode != 0 or cmp_code != 0 or n or axioms): + sys.exit(f"the unchanged copy does not pass: build exit {build.returncode}, " + f"comparator {cmp_says}, {n} test failures, axioms {axioms}") + rows.append((name, edits, equivalent, build.returncode, warned, cmp_code, cmp_says, + axioms, n, bar)) + print(f"{name}: build exit {build.returncode}, comparator exit {cmp_code}, " + f"{n} test failures" + (f", bar check items that differ: {len(bar)}" if check else ""), + flush=True) + return rows, base_bar + +def caught(row): + _, edits, _, _, _, cmp_code, _, _, n, bar = row + return bool(edits) and (cmp_code != 0 or n > 0 or bool(bar)) -def write(rows): + +def write(rows, base_bar, count, check): + steps = ["`lake build`", "`lake comparator --paranoid`", + "`#print axioms` for each theorem `comparator.json` lists", + f"`tests/run_tests.py --count {count}`"] + if check: + steps.append("mission's `bar/check.py --offline`") + command = ("python3 tests/planted_bugs.py" + (f" --count {count}" if count != COUNT else "") + + (" --bar /bar/check.py" if check else "")) lines = [ "# Planted bugs", "", - "Written by `python3 tests/planted_bugs.py`. Each row is one small change to the", - "proofs or to the axiom check, made in a copy. `lake build` ran on the copy, then", - "`tests/run_tests.py`. A fault is caught when the tests report failures.", + f"Written by `{command}`.", + "", + "Each row is one small change to the proofs, the statements, or the list of", + "theorems checked, made in a copy. On each copy these ran, in this order:", + "", + ] + [f"- {step};" for step in steps[:-1]] + [f"- {steps[-1]}.", ""] + if not check: + lines += ["Mission's bar check was not run (no `--bar`).", ""] + lines += [ + "The first row is the copy left as it is. A fault is caught when the comparator", + "rejects it, the tests report failures, or the bar check gives an item another", + "status than it gives the unchanged copy.", "", - "| Fault | Files | `lake build` | Failures | Failing checks |", - "|-------|-------|--------------|----------|----------------|", ] - for name, edits, equivalent, code, warned, n, fails in rows: - files = ", ".join(sorted({f"`{rel}`" for rel, _, _ in edits})) - build = ("passes" if code == 0 else "fails") + (", warns of a `sorry`" if warned else "") - cell = str(n) if n else ("0, equivalent: " + equivalent if equivalent else "0, NOT CAUGHT") - lines.append(f"| {name} | {files} | {build} | {cell} | {', '.join(fails)} |") + if base_bar: + lines += ["On the unchanged copy, the bar check gives: " + + ", ".join(f"item {i} {s}" for i, (s, _) in sorted(base_bar.items())) + ".", ""] + lines += [ + "| Fault | Files | `lake build` | `lake comparator --paranoid` | Axioms beyond the three | " + "Test failures | Bar check, where it differs | Caught |", + "|-------|-------|--------------|------------------------------|-------------------------|" + "---------------|-----------------------------|--------|", + ] + for row in rows: + name, edits, equivalent, code, warned, cmp_code, cmp_says, axioms, n, bar = row + files = ", ".join(sorted({f"`{rel}`" for rel, _, _ in edits})) or "none" + build = ("passes" if code == 0 else "fails") + ( + ", warns of a `sorry` in " + ", ".join(f"`{f}`" for f in warned) if warned else "") + if bar is None: + bar_cell = "not run" + else: + bar_cell = "; ".join(bar).replace("|", "\\|") or "the same" + if not edits: + verdict = "(none planted)" + elif caught(row): + verdict = "yes" + else: + verdict = "equivalent: " + equivalent if equivalent else "NOT CAUGHT" + lines.append(f"| {name} | {files} | {build} | {cmp_says} | {'; '.join(axioms) or 'none'} " + f"| {n} | {bar_cell} | {verdict} |") lines += ["", "## The changes", ""] - for name, edits, _, _, _, _, _ in rows: + for name, edits, *_ in rows: for rel, old, new in edits: lines += [f"**{name}** in `{rel}`:", "", "```", "- " + old.rstrip("\n").replace("\n", "\n- "), "+ " + new.rstrip("\n").replace("\n", "\n+ "), "```", ""] @@ -180,15 +326,26 @@ def write(rows): def main(): + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("--count", type=int, default=COUNT, + help="random archives for each run of the tests") + ap.add_argument("--bar", type=Path, metavar="CHECK", + help="mission's bar/check.py, to run on each copy as well") + args = ap.parse_args() + check = args.bar.resolve() if args.bar else None + if check and not check.is_file(): + sys.exit(f"no such file: {check}") # A run that stops early must not leave an earlier record. (ROOT / "tests" / "PLANTED-BUGS.md").unlink(missing_ok=True) - rows = run() - write(rows) - missed = [r[0] for r in rows if not r[5] and not r[2]] - caught = sum(1 for r in rows if r[5]) - print(f"{caught} of {len(rows)} planted bugs caught; results in tests/PLANTED-BUGS.md") + rows, base_bar = run(args.count, check) + write(rows, base_bar, args.count, check) + planted = [r for r in rows if r[1]] + missed = [r[0] for r in planted if not caught(r) and not r[2]] + print(f"{sum(map(caught, planted))} of {len(planted)} planted faults caught; " + "results in tests/PLANTED-BUGS.md") if missed: - sys.exit("not caught: " + ", ".join(missed)) + sys.exit("not caught by what ran: " + ", ".join(missed) + + ("" if check else " (pass --bar to run mission's bar check too)")) if __name__ == "__main__": From a04d5a47003da0b056720c29da86a0f247a06d7b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 23:02:25 +0000 Subject: [PATCH 6/6] tests: say plainly which faults planted_bugs.py plants The docstring said the faults are "the four the PR for audit F1 and F5 names". That PR's body names three: a sorry, an axiom and an extra theorem. Its version of this script adds a fourth, a theorem left out of the list checked. The docstring now names the faults, and says that the PR's version plants the same kinds against TarPilot/Verify.lean. The script's output does not change. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- tests/planted_bugs.py | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/tests/planted_bugs.py b/tests/planted_bugs.py index fbc70f8..776ba6f 100644 --- a/tests/planted_bugs.py +++ b/tests/planted_bugs.py @@ -1,13 +1,15 @@ #!/usr/bin/env python3 """Plant each fault below in a copy of the project, and record what catches it. -The faults are the four the PR for audit F1 and F5 names, planted -against the proof check this branch uses, `lake comparator --paranoid`: -a `sorry` and an axiom behind a helper lemma, an extra theorem, and a -theorem left out of the list the comparator checks, `comparator.json`. -Two more are a `sorry` and an axiom in `Spec.escape_noSpecial`, which -`comparator.json` does not list: the proof of `TarPilot.manifest_lines` -uses it, so the comparator checks it with that theorem. +The faults are a `sorry` and an axiom behind a helper lemma, an extra +theorem, and a statement of `Spec.lean` left out of `comparator.json`, +the list of theorems the comparator checks. The version of this script +in the PR for audit F1 and F5 plants the same kinds of fault against +`TarPilot/Verify.lean`. Here they are planted against the proof check +this branch uses, `lake comparator --paranoid`. Two more are a `sorry` +and an axiom in `Spec.escape_noSpecial`, which `comparator.json` does +not list: the proof of `TarPilot.manifest_lines` uses it, so the +comparator checks it with that theorem. What the proofs catch: a change to the code under proof that alters an answer a statement fixes stops `lake build`, since the proof of that