From b18427eac1103493a2337d3ed9d3a3e59fb5648a Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 25 Oct 2026 03:50:48 +0000 Subject: [PATCH 1/5] Reject what the pilot cannot read, extract contiguous files (audit F2-F4) The bar audit (Proven-Commons/mission#1) found that the page's promise "an archive using them fails to parse instead of being read in a wrong way" did not hold: GNU long names were cut to 100 bytes, pax headers were skipped so a pax path or non-ASCII name was ignored, and a name split over the prefix and name fields with invalid UTF-8 in one of them was placed under the other half. Typeflag 7 was skipped, unlike POSIX readers and Python's tarfile. And, found by the random tests in the next commit: an entry with a regular typeflag and a name ending in `/`, which older archives use for a directory and GNU tar reads as one, was extracted as a regular file. A further case, found while fixing these (call it F7): GNU incremental dumps keep access and change times where ustar keeps its name prefix. The pilot, like Python's tarfile, read them as a prefix, so GNU tar's `a.txt` came out as `15267276047/a.txt`. - `parseBlock` accepts only the POSIX ustar magic (`ustar`, NUL, `00`) or GNU's (`ustar`, two spaces, NUL), and a GNU header only when the area where ustar keeps its prefix is all zero. It rejects any typeflag outside NUL and `0` to `7`, and a name or prefix field that is not valid UTF-8. Each of these makes the whole archive fail to parse, as the page says. - Links, devices, directories and FIFOs (types 1 to 6) are followed by no data, whatever their size field says, as POSIX specifies and GNU tar and tarfile read them. The pilot used to skip `size` bytes after them, so an archive could hide from it a file both other readers extract. A regular typeflag with a name ending in `/` (a directory) and a nonzero size, where readers disagree, fails to parse, and so does a size field of spaces, which GNU tar refuses. - `create` never splits a long absolute name so that its `/` is lost. - `isRegular` also takes typeflag `7`, and no longer takes a name that ends in `/`. `Spec.regularType`, the rule `manifest_eq` states, says the same and now looks at the name. - The tests add the audit's probes and more of the same kinds: 27 archives that must fail with exit code 1 under `list` and `manifest`, and 11 in readable formats compared with tarfile, including GNU format, GNU tar's own output, names ending in `/`, and each non-regular type with a nonzero size field. Run against the previous commit's binary, 58 of the 100 checks fail. - The page lists exactly what the pilot does not read. The containment theorems do not depend on the parser. `manifest_eq` and `Spec.line` follow the new regular-file rule; their proofs are unchanged but for passing the name to it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Proofs/Contain.lean | 4 +- README.md | 12 ++- Spec/Defs.lean | 11 ++- TarPilot/Archive.lean | 13 ++- TarPilot/Header.lean | 63 ++++++++++--- TarPilot/Octal.lean | 4 +- tests/TEST-RESULTS.md | 4 +- tests/run_tests.py | 207 +++++++++++++++++++++++++++++++++++++++++- 8 files changed, 287 insertions(+), 31 deletions(-) diff --git a/Proofs/Contain.lean b/Proofs/Contain.lean index 9da005a..ab355e0 100644 --- a/Proofs/Contain.lean +++ b/Proofs/Contain.lean @@ -318,7 +318,7 @@ theorem gate_plain (name : String) (rel : List String) : 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 then + if regularType e.typeflag e.name then match cleanName e.name with | some rel => .extract (dest ++ rel) e.data | none => .reject e.name @@ -514,7 +514,7 @@ theorem manifest_lines_eq (dest : String) (entries : List RawEntry) : funext e simp only [Function.comp_apply] unfold outcome Spec.line - have hreg : isRegular e = regularType e.typeflag := rfl + have hreg : isRegular e = regularType e.typeflag e.name := rfl rw [hreg, gate_eq] split · split diff --git a/README.md b/README.md index 1e41ac4..916dcc9 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ lake build 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 (typeflag `0` or NUL) are extracted, which `manifest_eq` proves. Directory, link, and other entries are skipped, so a link entry cannot place a later entry outside the destination. +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. - `gate_eq`: the gate is exactly its rules. - `gate_plain`: a name that passes the gate gives a non-empty list of plain names. @@ -43,11 +43,17 @@ Axiom check: each theorem depends only on the standard Lean axioms (`propext`, ` 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`: 35 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; and broken inputs (truncated, garbage, bad checksum). +- 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. -- Names that are not valid UTF-8 read as empty and are rejected by the gate. GNU tar extensions (longname entries, pax headers), base-256 size fields, and sparse files are not supported. An archive using them fails to parse instead of being read in a wrong way. +- 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: + - 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; + - 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. ## Re-check it diff --git a/Spec/Defs.lean b/Spec/Defs.lean index e707289..338d34d 100644 --- a/Spec/Defs.lean +++ b/Spec/Defs.lean @@ -47,9 +47,12 @@ def cleanName (name : String) : Option (List String) := let kept := parts.filter (fun c => !(c == "" || c == ".")) if kept = [] then none else some kept -/-- The typeflags of regular files: `0`, and NUL from older archives. -/ -def regularType (t : Char) : Bool := - t == '0' || t == Char.ofNat 0 +/-- Whether an entry with typeflag `t` and name `name` is a regular file: + 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. -/ +def regularType (t : Char) (name : String) : Bool := + (t == '0' || t == Char.ofNat 0 || t == '7') && name.toList.getLast? != some '/' /-- A relative path `rel` under the destination `dest`, as a string: `rel` alone when `dest` is empty, `dest` then `rel` when `dest` ends in `/`, @@ -135,7 +138,7 @@ def byteSum (b : ByteArray) : Nat := whose name fails; `SKIP`, the name, and the typeflag as a decimal code, for anything else. -/ def line (dest : String) (name : String) (t : Char) (data : ByteArray) : String := - if regularType t then + if regularType t name then match cleanName name with | some rel => "OK\t" ++ under dest (String.intercalate "/" rel) ++ "\t" ++ toString data.size ++ diff --git a/TarPilot/Archive.lean b/TarPilot/Archive.lean index b6d8268..1131d41 100644 --- a/TarPilot/Archive.lean +++ b/TarPilot/Archive.lean @@ -51,11 +51,16 @@ def parseBlocks (data : ByteArray) (off : Nat) : Nat → Option (List RawEntry) def parseArchive (data : ByteArray) : Option (List RawEntry) := parseBlocks data 0 (data.size / 512 + 1) -/-- Regular files only: typeflag `0` or NUL. Directories, links, and - everything else are never extracted, so a link entry cannot be used - to place a later entry outside the destination. -/ +/-- Regular files only: typeflag `0`, NUL, or `7` (a contiguous file, + which POSIX lets a reader treat as regular, as Python's `tarfile` + does), and a name that does not end in `/`. Older archives mark a + directory with that `/`, and GNU tar reads any entry named so as a + directory. Directories, links, and everything else are never + extracted, so a link entry cannot be used to place a later entry + outside the destination. -/ def isRegular (e : RawEntry) : Bool := - e.typeflag == '0' || e.typeflag == Char.ofNat 0 + (e.typeflag == '0' || e.typeflag == Char.ofNat 0 || e.typeflag == '7') && + e.name.toList.getLast? != some '/' /-- Extract entries into a list of `(path, data)` pairs, in memory. The path of each pair is the destination components followed by the diff --git a/TarPilot/Header.lean b/TarPilot/Header.lean index 68885a7..d948491 100644 --- a/TarPilot/Header.lean +++ b/TarPilot/Header.lean @@ -16,7 +16,8 @@ import TarPilot.Octal namespace TarPilot -/-- A parsed header. Only the fields the pilot uses. -/ +/-- A parsed header. Only the fields the pilot uses. `size` is the size + of the data that follows the header. -/ structure Header where name : String size : Nat @@ -31,11 +32,26 @@ def byteAt (b : ByteArray) (i : Nat) : UInt8 := def sliceList (b : ByteArray) (off len : Nat) : List UInt8 := (b.extract off (off + len)).toList -/-- A name field: bytes up to the first NUL, read as UTF-8. - Invalid UTF-8 reads as the empty string. -/ -def bytesToName (bs : List UInt8) : String := +/-- A name field: bytes up to the first NUL, read as UTF-8, or `none` + when they are not valid UTF-8. -/ +def bytesToName (bs : List UInt8) : Option String := let raw := bs.takeWhile (fun b => b ≠ 0) - (String.fromUTF8? (ByteArray.mk raw.toArray)).getD "" + String.fromUTF8? (ByteArray.mk raw.toArray) + +/-- The magic and version of a POSIX ustar header: `ustar`, NUL, `00`. -/ +def ustarMagic : List UInt8 := [117, 115, 116, 97, 114, 0, 48, 48] + +/-- The magic and version of a GNU header: `ustar`, two spaces, NUL. -/ +def gnuMagic : List UInt8 := [117, 115, 116, 97, 114, 32, 32, 0] + +/-- The typeflags the pilot reads: NUL and `0` to `7`, the types POSIX + ustar defines. Any other typeflag, among them the GNU long name and + long link entries `L` and `K`, the pax headers `x` and `g`, and GNU + sparse and incremental entries, makes the archive fail to parse: + such entries change how other entries read, or carry data the pilot + does not read. -/ +def knownTypeflag (t : Char) : Bool := + t == Char.ofNat 0 || ('0' ≤ t && t ≤ '7') /-- The header checksum: sum of all 512 bytes, with the checksum field itself (bytes 148 to 155) counted as spaces. -/ @@ -43,20 +59,38 @@ def blockChecksum (bs : List UInt8) : Nat := (bs.zipIdx).foldl (fun acc p => acc + (if 148 ≤ p.2 ∧ p.2 < 156 then 32 else p.1.toNat)) 0 -/-- Parse one 512-byte header block. Fails on a short block, a bad - magic, a checksum mismatch, or a bad size field. -/ +/-- Parse one 512-byte header block. Fails on a short block; a magic + that is neither POSIX ustar nor GNU; a GNU header with anything in + the area where ustar keeps its prefix (GNU keeps access and change + times, sparse maps and volume offsets there); a checksum mismatch; a + bad size field; a typeflag outside `knownTypeflag`; a name or prefix + field that is not valid UTF-8; or 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. + + Only regular typeflags (NUL, `0`, `7`) are followed by data. POSIX + stores no data for links, devices, directories and FIFOs (types 1 to + 6), whatever their size field says, and GNU tar and Python's tarfile + read the next header straight after them, so the size given for + those is 0. -/ def parseBlock (block : ByteArray) : Option Header := if block.size < 512 then none else do - if sliceList block 257 5 ≠ [117, 115, 116, 97, 114] then none else + let magic := sliceList block 257 8 + let gnuPlain := magic = gnuMagic ∧ (sliceList block 345 155).all (· = 0) + if ¬(magic = ustarMagic ∨ gnuPlain) then none else let stored ← parseOctal (sliceList block 148 8) if stored ≠ blockChecksum (sliceList block 0 512) then none else let size ← parseOctal (sliceList block 124 12) - let name := bytesToName (sliceList block 0 100) - let pfx := bytesToName (sliceList block 345 155) + let typeflag := Char.ofNat (byteAt block 156).toNat + if !knownTypeflag typeflag then none else + let name ← bytesToName (sliceList block 0 100) + let pfx ← bytesToName (sliceList block 345 155) let fullName := if pfx = "" then name else pfx ++ "/" ++ name - some { name := fullName, size := size, - typeflag := Char.ofNat (byteAt block 156).toNat } + let regular := typeflag == '0' || typeflag == Char.ofNat 0 || typeflag == '7' + let dirName := fullName.toList.getLast? == some '/' + if regular && dirName && size != 0 then none else + some { name := fullName, size := if regular then size else 0, typeflag := typeflag } /-- Content padded on the right with NUL bytes to width `w`, or cut to `w` when longer. -/ @@ -65,7 +99,8 @@ def fieldBytes (content : List UInt8) (w : Nat) : List UInt8 := /-- Split a long name at a `/` so the part before it fits the 155-byte prefix field and the part after it fits the 100-byte name field. - Short names get an empty prefix. Fails when no split works. -/ + Short names get an empty prefix. Neither part of a split may be + empty, so an absolute name keeps its `/`. Fails when no split works. -/ def splitUstarName (name : String) : Option (String × String) := if name.toUTF8.size ≤ 100 then some ("", name) else @@ -73,7 +108,7 @@ def splitUstarName (name : String) : Option (String × String) := let tries := (List.range cs.length).map fun k => (String.intercalate "/" (cs.take (k + 1)), String.intercalate "/" (cs.drop (k + 1))) tries.find? (fun p => - p.1.toUTF8.size ≤ 155 ∧ p.2.toUTF8.size ≤ 100 ∧ p.2 ≠ "") + p.1 ≠ "" ∧ p.1.toUTF8.size ≤ 155 ∧ p.2.toUTF8.size ≤ 100 ∧ p.2 ≠ "") /-- Build a 512-byte header block for a regular file or directory. Mode is fixed at 0644, uid, gid, and mtime at 0. diff --git a/TarPilot/Octal.lean b/TarPilot/Octal.lean index 8973946..df9c4d0 100644 --- a/TarPilot/Octal.lean +++ b/TarPilot/Octal.lean @@ -14,9 +14,11 @@ def trimField (bs : List UInt8) : List UInt8 := (noLead.reverse.dropWhile (fun b => b = 0 ∨ b = 32)).reverse /-- Parse an octal field. Fails on any byte that is not an octal digit - after trimming. An empty field parses as 0. -/ + after trimming. A field with no digits parses as 0 when it is all + NUL, and fails when it holds a space, as GNU tar refuses it. -/ def parseOctal (bs : List UInt8) : Option Nat := let digits := trimField bs + if digits.isEmpty && bs.any (· == 32) then none else digits.foldl (fun acc b => match acc with | none => none diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 514b31f..41926c5 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -3,12 +3,14 @@ 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. -- Checks run: 35 (13 of them on the axioms of the theorems) +- Checks run: 100 (13 of them on the axioms of the theorems) - Failures: 0 - 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`): diff --git a/tests/run_tests.py b/tests/run_tests.py index 74400bd..3645b02 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -16,6 +16,7 @@ import os import random import re +import shutil import subprocess import sys import tarfile @@ -97,6 +98,167 @@ def is_regular(ti): return ti.isreg() +# Typeflags of regular files: `0`, NUL, and `7` (contiguous file). +REGULAR_CODES = (ord("0"), 0, ord("7")) + + +def is_regular_entry(name, tcode): + """A regular file: typeflag `0`, NUL or `7`, and a name that does not + end in `/`, which older archives use for a directory.""" + return tcode in REGULAR_CODES and not name.endswith("/") + + +def one_file(fmt, name, data=b"x", typ=tarfile.REGTYPE, pax=None): + """An archive of one entry, written by Python's tarfile.""" + buf = io.BytesIO() + with tarfile.open(fileobj=buf, mode="w", format=fmt) as t: + ti = tarfile.TarInfo(name) + ti.size = len(data) + ti.type = typ + ti.mtime = 0 + if pax: + ti.pax_headers = pax + t.addfile(ti, io.BytesIO(data)) + return buf.getvalue() + + +def patch_header(raw, offset, new_bytes): + """Overwrite bytes in the first header and fix its checksum.""" + hdr = bytearray(raw[:512]) + hdr[offset:offset + len(new_bytes)] = new_bytes + hdr[148:156] = b" " * 8 + hdr[148:156] = ("%06o\0 " % sum(hdr)).encode() + return bytes(hdr) + raw[512:] + + +LONG = "d/" + "n" * 120 + ".txt" +SPLIT = "p" * 30 + "/" + "q" * 90 + "/file.txt" + + +def unsupported_archives(work): + """Archives that use what the pilot does not read. Each must fail to + parse: these are the probes of findings F2, F3 and F7 of the bar + audit, and more of the same kinds.""" + yield "GNU long name entry (typeflag L)", one_file(tarfile.GNU_FORMAT, LONG) + yield "GNU long link entry (typeflag K)", patch_header( + one_file(tarfile.GNU_FORMAT, "l.txt"), 156, b"K") + yield "pax long path (typeflag x)", one_file(tarfile.PAX_FORMAT, LONG) + yield "pax path override", one_file(tarfile.PAX_FORMAT, "safe.txt", + pax={"path": "other/dir/real.txt"}) + yield "pax path override that climbs out", one_file( + tarfile.PAX_FORMAT, "safe.txt", pax={"path": "../../etc/cron.d/x"}) + yield "pax non-ASCII name", one_file(tarfile.PAX_FORMAT, "café/notes.txt") + buf = io.BytesIO() + with tarfile.open(fileobj=buf, mode="w", format=tarfile.PAX_FORMAT, + pax_headers={"comment": "global"}) as t: + ti = tarfile.TarInfo("g.txt") + ti.size = 1 + t.addfile(ti, io.BytesIO(b"g")) + yield "pax global header (typeflag g)", buf.getvalue() + split = one_file(tarfile.USTAR_FORMAT, SPLIT) + yield "split name, invalid UTF-8 in the prefix field only", patch_header(split, 345, b"\xff") + yield "split name, invalid UTF-8 in the name field only", patch_header(split, 0, b"\xff") + yield "split name, invalid UTF-8 in both fields", patch_header( + patch_header(split, 0, b"\xff"), 345, b"\xff") + yield "short name, invalid UTF-8", patch_header( + one_file(tarfile.USTAR_FORMAT, "short.txt"), 0, b"\xff") + gnu = one_file(tarfile.GNU_FORMAT, "a.txt") + yield "GNU header with access and change times (incremental dump)", patch_header( + gnu, 345, b"15267276047\x0015267276047\x00") + yield "GNU header with a sparse map", patch_header(gnu, 386, b"00000000001") + for code in b"DMNSVAZ": + yield f"unknown typeflag {chr(code)}", patch_header( + one_file(tarfile.USTAR_FORMAT, "u.txt"), 156, bytes([code])) + yield "base-256 size field", patch_header( + one_file(tarfile.USTAR_FORMAT, "b.txt"), 124, b"\x80" + b"\x00" * 10 + b"\x01") + yield "ustar magic with a GNU version", patch_header( + one_file(tarfile.USTAR_FORMAT, "m.txt"), 263, b" \x00") + yield "no magic (old Unix V7 header)", patch_header( + one_file(tarfile.USTAR_FORMAT, "v.txt"), 257, b"\x00" * 8) + for name, typ in [("d/", tarfile.AREGTYPE), ("e/", tarfile.REGTYPE)]: + yield f"name ending in / with typeflag {typ!r} and data", one_file( + 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) + gnu_tar = shutil.which("tar") + if gnu_tar: + src = work / "systar-long" / "d" + src.mkdir(parents=True) + (src / ("n" * 120 + ".txt")).write_bytes(b"x") + out = work / "systar-long.tar" + subprocess.run([gnu_tar, "cf", str(out), "d"], cwd=work / "systar-long", check=True) + yield "system tar, default format, long name", out.read_bytes() + + +def readable_archives(work): + """Archives in formats the pilot reads. Each must read as Python's + tarfile reads it.""" + yield "contiguous file (typeflag 7)", one_file( + tarfile.USTAR_FORMAT, "contig.bin", data=b"contiguous", typ=tarfile.CONTTYPE) + buf = io.BytesIO() + with tarfile.open(fileobj=buf, mode="w", format=tarfile.GNU_FORMAT) as t: + for name, data in [("gnu.txt", b"gnu"), ("dir/inner.bin", bytes(range(40)))]: + ti = tarfile.TarInfo(name) + ti.size = len(data) + ti.mtime = 0 + t.addfile(ti, io.BytesIO(data)) + yield "GNU format, short names", buf.getvalue() + yield "pax format, short ASCII name (no pax header)", one_file( + tarfile.PAX_FORMAT, "plain.txt", data=b"plain") + buf = io.BytesIO() + with tarfile.open(fileobj=buf, mode="w", format=tarfile.USTAR_FORMAT) as t: + for name, typ, data in [("olddir/", tarfile.AREGTYPE, b""), + ("olddir/f.txt", tarfile.AREGTYPE, b"old"), + ("slashdir/", tarfile.REGTYPE, b"")]: + ti = tarfile.TarInfo(name) + ti.type = typ + ti.size = len(data) + ti.mtime = 0 + t.addfile(ti, io.BytesIO(data)) + yield "names ending in / with typeflags NUL and 0, read as directories", buf.getvalue() + 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) + gnu_tar = shutil.which("tar") + if gnu_tar: + src = work / "systar-short" + (src / "d").mkdir(parents=True) + (src / "a.txt").write_bytes(b"hi\n") + (src / "d" / "b.txt").write_bytes(b"x\n") + out = work / "systar-short.tar" + subprocess.run([gnu_tar, "cf", str(out), "a.txt", "d"], cwd=src, check=True) + yield "system tar, default format, short names", out.read_bytes() + + +def hidden_after(typ): + """An entry of type `typ` whose size field says 1024, then a header and + data that fill those 1024 bytes, then one more file. Types 1 to 6 + store no data, so a reader must see all three entries.""" + buf = io.BytesIO() + with tarfile.open(fileobj=buf, mode="w", format=tarfile.USTAR_FORMAT) as t: + for name, kind, data in [("node", typ, b""), ("hidden.txt", tarfile.REGTYPE, b"hidden"), + ("b.txt", tarfile.REGTYPE, b"b")]: + ti = tarfile.TarInfo(name) + ti.type = kind + ti.size = len(data) + ti.mtime = 0 + if kind in (tarfile.SYMTYPE, tarfile.LNKTYPE): + ti.linkname = "target" + t.addfile(ti, io.BytesIO(data)) + return patch_header(buf.getvalue(), 124, b"00000002000\0") + + +def tarfile_view(path): + """(name, data, typeflag code) for each entry, as tarfile reads it.""" + out = [] + with tarfile.open(path) as tf: + for m in tf.getmembers(): + data = tf.extractfile(m).read() if m.isreg() else b"" + tcode = m.type[0] if isinstance(m.type, bytes) else ord(m.type) + out.append((m.name, data, tcode)) + return out + + def build_archive_a(path): """Archive with normal, hostile, and edge-case entries, built with Python's tarfile as the reference implementation.""" @@ -156,7 +318,7 @@ def expected_manifest(entries_data, dest="out"): entries_data: list of (name, data, typeflag_byte).""" lines = [] for name, data, tcode in entries_data: - if tcode not in (ord("0"), 0): + if not is_regular_entry(name, tcode): lines.append(f"SKIP\t{escape_name(name)}\t{tcode}") continue rel = spec_gate(name) @@ -269,6 +431,13 @@ def main(): if m.isreg(): got[m.name] = tf.extractfile(m).read() check("create-readback", got == files, f"got={list(got)} want={list(files)}") + # A name too long for the name field, with no `/` to split it at, + # fails with exit code 1 and writes nothing. + target = td / "bad.tar" + (src / ("n" * 101)).write_bytes(b"x") + r = run_lean("create", str(target), "n" * 101, cwd=src) + check("create-refuses-long-name", r.returncode == 1 and not target.exists(), + f"rc={r.returncode} exists={target.exists()}") # 4. Lean reads its own archive back with the same manifest. if r.returncode == 0: @@ -297,7 +466,38 @@ def main(): r = run_lean("list", str(badsum)) check("bad-checksum-fails", r.returncode == 1, f"rc={r.returncode}") - # 6. Axiom check: Verify.lean prints the axioms of exactly the + # 6. Formats the pilot does not read fail to parse, with exit + # code 1 and nothing on standard output, for both commands. + unsupported = 0 + for i, (label, raw) in enumerate(unsupported_archives(td)): + unsupported += 1 + path = td / f"unsupported{i}.tar" + path.write_bytes(raw) + for cmd in (["list", str(path)], ["manifest", str(path), "out"]): + r = run_lean(*cmd) + check(f"unsupported-fails: {label} ({cmd[0]})", + r.returncode == 1 and r.stdout == "", + f"rc={r.returncode} out={r.stdout[:200]!r}") + + # 7. Formats the pilot reads give what tarfile reads. + readable = 0 + for i, (label, raw) in enumerate(readable_archives(td)): + readable += 1 + path = td / f"readable{i}.tar" + path.write_bytes(raw) + ref = tarfile_view(path) + r = run_lean("manifest", str(path), "out") + # tarfile reports an old-style directory (typeflag NUL, name + # ending in `/`) as typeflag 5, so SKIP lines are compared + # without their typeflag here. + drop_code = lambda ls: [l.rsplit("\t", 1)[0] if l.startswith("SKIP") else l + for l in norm_skip(ls)] + got = drop_code(output_lines(r.stdout)) + want = drop_code(expected_manifest(ref)) + 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"], @@ -334,6 +534,9 @@ def main(): f"- Files written by the Lean `create` command and read back by Python: {len(files)}", "- Broken inputs rejected with exit code 1: truncated archive, " "random garbage, corrupted checksum", + 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`):", "", From 0873ad544a6cb9d24760ee6447a8ddddd3ff2aa2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 14:20:13 +0000 Subject: [PATCH 2/5] tests: compare the readable set under list too, and GNU tar's formats The readable archives were compared with tarfile under manifest only. They are now compared under list as well. The SKIP typeflag is no longer dropped: only typeflag NUL with a name ending in `/` is read as 5, as tarfile reads it, and the results file and README say so. GNU tar's own output is now read in its default, gnu and oldgnu formats, with files, a directory, a hard link, a symlink and a FIFO, all with nothing in bytes 345 to 499. Its incremental dump and its sparse file, which do use those bytes, must fail to parse. 121 of 121 checks pass. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 4 +- tests/TEST-RESULTS.md | 15 +++++-- tests/run_tests.py | 96 +++++++++++++++++++++++++++++++++++++------ 3 files changed, 97 insertions(+), 18 deletions(-) diff --git a/README.md b/README.md index 713f89f..3eda3ba 100644 --- a/README.md +++ b/README.md @@ -43,13 +43,13 @@ Axiom check: each theorem depends only on the standard Lean axioms (`propext`, ` 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`: 102 checks, 14 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 six refused: five for a special character or U+FFFD, and one given as bytes that are not UTF-8; 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. +- 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`: 121 checks, 14 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 six refused: five for a special character or U+FFFD, and one given as bytes that are not UTF-8; broken inputs (truncated, garbage, bad checksum); 29 archives in formats the pilot does not read; and 13 more archives it does read, among them GNU format, GNU tar's own output in its default, `gnu` and `oldgnu` formats, names ending in `/`, and links, devices, directories and FIFOs whose size fields are not zero. Both commands are compared with `tarfile` on each of them. `tarfile` reads typeflag NUL with a name ending in `/` as a directory, typeflag 5, so the tool's typeflag 0 on such an entry is compared as 5. Every other typeflag is compared as printed. - 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: - 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 GNU header with anything where ustar keeps its name prefix (bytes 345 to 499), such as the access and change times of an incremental dump. GNU tar 1.35 puts nothing there for short names, in its default, `gnu` and `oldgnu` formats, unless it is asked for an incremental dump, a sparse file or a multi-volume archive; - 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; diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index da0f091..76bc8d7 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -1,16 +1,23 @@ # 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. +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. -- Checks run: 102 (14 of them on the axioms of the theorems) +- Checks run: 121 (14 of them on the axioms of the theorems) - Failures: 0 - 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 +- Archives in formats the pilot does not read, rejected with exit code 1 by `list` and `manifest`: 29 +- Archives in other formats it reads, compared with tarfile under `list` and `manifest`: 13 + +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 +tool's typeflag 0 on such an entry is read as 5. Every other typeflag is +compared as printed. Axiom check (`TarPilot/Verify.lean`): diff --git a/tests/run_tests.py b/tests/run_tests.py index dfa882a..0c7369b 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -189,6 +189,23 @@ def unsupported_archives(work): out = work / "systar-long.tar" subprocess.run([gnu_tar, "cf", str(out), "d"], cwd=work / "systar-long", check=True) yield "system tar, default format, long name", out.read_bytes() + if gnu_tar and is_gnu_tar(gnu_tar): + # GNU tar's own output for the GNU fields in bytes 345 to 499. + src = work / "systar-gnu-fields" + src.mkdir() + (src / "a.txt").write_bytes(b"hi\n") + with open(src / "sparse", "wb") as f: + f.seek(1 << 20) + f.write(b"end") + out = work / "systar-incremental.tar" + subprocess.run([gnu_tar, "cf", str(out), "--format=gnu", + f"--listed-incremental={work / 'systar.snar'}", "a.txt"], + cwd=src, check=True) + yield "system tar, incremental dump (times in bytes 345 to 368)", out.read_bytes() + out = work / "systar-sparse.tar" + subprocess.run([gnu_tar, "cf", str(out), "--format=gnu", "--sparse", "sparse"], + cwd=src, check=True) + yield "system tar, sparse file (typeflag S, map in bytes 386 to 494)", out.read_bytes() def readable_archives(work): @@ -222,13 +239,38 @@ def readable_archives(work): yield f"typeflag {typ.decode()} with a size field, then two files", hidden_after(typ) gnu_tar = shutil.which("tar") if gnu_tar: + # Every kind of entry GNU tar writes for short names in its own + # formats: GNU keeps nothing in bytes 345 to 499 for these unless + # it is asked for an incremental dump, a sparse file or a + # multi-volume archive. src = work / "systar-short" (src / "d").mkdir(parents=True) (src / "a.txt").write_bytes(b"hi\n") + (src / "empty").write_bytes(b"") (src / "d" / "b.txt").write_bytes(b"x\n") - out = work / "systar-short.tar" - subprocess.run([gnu_tar, "cf", str(out), "a.txt", "d"], cwd=src, check=True) - yield "system tar, default format, short names", out.read_bytes() + os.link(src / "a.txt", src / "hard.txt") + os.symlink("a.txt", src / "sym") + os.mkfifo(src / "fifo") + names = ["a.txt", "empty", "d", "hard.txt", "sym", "fifo"] + for fmt in ["default"] + (["gnu", "oldgnu"] if is_gnu_tar(gnu_tar) else []): + out = work / f"systar-short-{fmt}.tar" + opts = [] if fmt == "default" else [f"--format={fmt}"] + subprocess.run([gnu_tar, "cf", str(out), *opts, *names], cwd=src, check=True) + yield (f"system tar, {fmt} format, short names: files, a directory, " + "a hard link, a symlink, a FIFO"), out.read_bytes() + + +def is_gnu_tar(tar): + r = subprocess.run([tar, "--version"], capture_output=True, text=True) + return r.stdout.startswith("tar (GNU tar)") + + +def tar_version(): + tar = shutil.which("tar") + if not tar: + return "none" + r = subprocess.run([tar, "--version"], capture_output=True, text=True) + return (r.stdout.splitlines() or ["unknown"])[0] def hidden_after(typ): @@ -351,6 +393,25 @@ def list_rows(stdout): return rows +def as_tarfile_reads(row): + """A `list` row as tarfile reads the entry. tarfile reads typeflag + NUL with a name ending in `/` as a directory, typeflag 5 ("Old V7 + tar format represents a directory as a regular file with a trailing + slash", in tarfile.py). Every other row is left as it is.""" + if len(row) == 3 and row[2] == 0 and row[0].endswith("/"): + return (row[0], row[1], 53) + return row + + +def skip_as_tarfile_reads(line): + """A `manifest` line as tarfile reads the entry: the same rule, for + SKIP lines.""" + p = line.split("\t") + if len(p) == 3 and p[0] == "SKIP" and p[2] == "0" and p[1].endswith("/"): + return "\t".join([p[0], p[1], "53"]) + return line + + def main(): # A run that stops early must not leave an earlier passing record. RESULTS.unlink(missing_ok=True) @@ -489,14 +550,17 @@ def main(): path = td / f"readable{i}.tar" path.write_bytes(raw) ref = tarfile_view(path) - r = run_lean("manifest", str(path), "out") # tarfile reports an old-style directory (typeflag NUL, name - # ending in `/`) as typeflag 5, so SKIP lines are compared - # without their typeflag here. - drop_code = lambda ls: [l.rsplit("\t", 1)[0] if l.startswith("SKIP") else l - for l in norm_skip(ls)] - got = drop_code(output_lines(r.stdout)) - want = drop_code(expected_manifest(ref)) + # ending in `/`) as typeflag 5. The tool's output is read the + # same way (`as_tarfile_reads`); no other typeflag changes. + r = run_lean("list", str(path)) + got = norm([as_tarfile_reads(row) for row in list_rows(r.stdout)]) + want = norm([(escape_name(n), len(d), t) for (n, d, t) in ref]) + check(f"readable-list: {label}", r.returncode == 0 and got == want, + f"rc={r.returncode} lean={got} expected={want}") + r = run_lean("manifest", str(path), "out") + got = norm_skip([skip_as_tarfile_reads(l) for l in output_lines(r.stdout)]) + want = norm_skip(expected_manifest(ref)) check(f"readable-manifest: {label}", r.returncode == 0 and got == want, f"rc={r.returncode} lean={got} expected={want}") @@ -527,7 +591,7 @@ def main(): "# Test results", "", f"Run by `tests/run_tests.py` against Python's `tarfile` module.", - f"Lean: {lean_ver}. Python: {sys.version.split()[0]}.", + f"Lean: {lean_ver}. Python: {sys.version.split()[0]}. System tar: {tar_version()}.", "", f"- Checks run: {checks} ({axiom_checks} of them on the axioms of the theorems)", f"- Failures: {len(failures)}", @@ -539,7 +603,15 @@ def main(): "random garbage, corrupted checksum", 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}", + f"- Archives in other formats it reads, compared with tarfile under `list` and " + f"`manifest`: {readable}", + "", + "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", + "tool's typeflag 0 on such an entry is read as 5. Every other typeflag is", + "compared as printed.", "", "Axiom check (`TarPilot/Verify.lean`):", "", From f6dfeb55c9e1a5dfe1d4b0ef5ea57ede13961aac Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 14:20:38 +0000 Subject: [PATCH 3/5] README: state both parts of the rule for names ending in `/` Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 3eda3ba..c3fb7ef 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ lake build 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 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. So an entry with a regular typeflag and a name ending in `/` gets a `SKIP` line when its size is zero. When its size is not zero, the whole archive fails to parse, since readers disagree on whether data follows (see the list under What is not proved). Directory, link, and other entries are skipped, so a link entry cannot place a later entry outside the destination. - `gate_eq`: the gate is exactly its rules. - `gate_plain`: a name that passes the gate gives a non-empty list of plain names. From e036a3d89e938d8b55539cd1a52d1345c227752d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 19:37:53 +0000 Subject: [PATCH 4/5] tests: run the checks against a tool built from a given commit The PR said that 58 of the 100 checks fail against #4's binary, but no file recorded it. That count came from b18427e's test script with the tool built from 1273382: 50 must-fail checks and 8 readable-manifest checks fail. The 13 axiom checks pass, since they read b18427e's proofs, not the tool. `python3 tests/run_tests.py --tool REV` now builds the tool at REV with git archive in a temporary directory and runs the checks against it. The checkout is not changed or built. The axiom check is left out, and the record goes to tests/TEST-RESULTS-REV.md. With --tool 1273382, 68 of the 107 checks fail: 54 must-fail checks (27 of the 29 archives, under both commands), 8 readable-manifest checks and 6 readable-list checks. The record now says which inputs must fail with exit code 1, not that they were rejected, so it reads right when checks fail. The run without --tool still gives 121/121. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 2 + tests/TEST-RESULTS-1273382.md | 93 ++++++++++++++++++++++++ tests/TEST-RESULTS.md | 4 +- tests/run_tests.py | 131 ++++++++++++++++++++++++---------- 4 files changed, 192 insertions(+), 38 deletions(-) create mode 100644 tests/TEST-RESULTS-1273382.md diff --git a/README.md b/README.md index c3fb7ef..736b354 100644 --- a/README.md +++ b/README.md @@ -68,6 +68,8 @@ The build fails if a proof breaks, though it accepts a `sorry` with only a warni `python3 tests/compare_old.py` builds the tool as it was before the containment change (commit 7517a86) 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`. +`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/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`. ## Layout diff --git a/tests/TEST-RESULTS-1273382.md b/tests/TEST-RESULTS-1273382.md new file mode 100644 index 0000000..f8ac273 --- /dev/null +++ b/tests/TEST-RESULTS-1273382.md @@ -0,0 +1,93 @@ +# 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. + +- Checks run: 107, all on the tool +- Failures: 68 +- 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 + +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 +tool's typeflag 0 on such an entry is read as 5. Every other typeflag is +compared as printed. + +## Failures + +- unsupported-fails: GNU long name entry (typeflag L) (list): rc=0 out='././@LongLink\t127\t76\nd/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t48\n' +- unsupported-fails: GNU long name entry (typeflag L) (manifest): rc=0 out='SKIP\t././@LongLink\t76\nOK\tout/d/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t120\n' +- unsupported-fails: GNU long link entry (typeflag K) (list): rc=0 out='l.txt\t1\t75\n' +- unsupported-fails: GNU long link entry (typeflag K) (manifest): rc=0 out='SKIP\tl.txt\t75\n' +- unsupported-fails: pax long path (typeflag x) (list): rc=0 out='././@PaxHeader\t136\t120\nd/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t48\n' +- unsupported-fails: pax long path (typeflag x) (manifest): rc=0 out='SKIP\t././@PaxHeader\t120\nOK\tout/d/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t120\n' +- unsupported-fails: pax path override (list): rc=0 out='././@PaxHeader\t27\t120\nsafe.txt\t1\t48\n' +- unsupported-fails: pax path override (manifest): rc=0 out='SKIP\t././@PaxHeader\t120\nOK\tout/safe.txt\t1\t120\n' +- unsupported-fails: pax path override that climbs out (list): rc=0 out='././@PaxHeader\t27\t120\nsafe.txt\t1\t48\n' +- unsupported-fails: pax path override that climbs out (manifest): rc=0 out='SKIP\t././@PaxHeader\t120\nOK\tout/safe.txt\t1\t120\n' +- unsupported-fails: pax non-ASCII name (list): rc=0 out='././@PaxHeader\t24\t120\ncaf?/notes.txt\t1\t48\n' +- unsupported-fails: pax non-ASCII name (manifest): rc=0 out='SKIP\t././@PaxHeader\t120\nOK\tout/caf?/notes.txt\t1\t120\n' +- unsupported-fails: pax global header (typeflag g) (list): rc=0 out='././@PaxHeader\t18\t103\ng.txt\t1\t48\n' +- unsupported-fails: pax global header (typeflag g) (manifest): rc=0 out='SKIP\t././@PaxHeader\t103\nOK\tout/g.txt\t1\t103\n' +- unsupported-fails: split name, invalid UTF-8 in the prefix field only (list): rc=0 out='qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq/file.txt\t1\t48\n' +- unsupported-fails: split name, invalid UTF-8 in the prefix field only (manifest): rc=0 out='OK\tout/qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq/file.txt\t1\t120\n' +- unsupported-fails: split name, invalid UTF-8 in the name field only (list): rc=0 out='pppppppppppppppppppppppppppppp/\t1\t48\n' +- unsupported-fails: split name, invalid UTF-8 in the name field only (manifest): rc=0 out='OK\tout/pppppppppppppppppppppppppppppp\t1\t120\n' +- unsupported-fails: split name, invalid UTF-8 in both fields (list): rc=0 out='\t1\t48\n' +- unsupported-fails: split name, invalid UTF-8 in both fields (manifest): rc=0 out='REJECT\t\n' +- unsupported-fails: short name, invalid UTF-8 (list): rc=0 out='\t1\t48\n' +- unsupported-fails: short name, invalid UTF-8 (manifest): rc=0 out='REJECT\t\n' +- unsupported-fails: GNU header with access and change times (incremental dump) (list): rc=0 out='15267276047/a.txt\t1\t48\n' +- unsupported-fails: GNU header with access and change times (incremental dump) (manifest): rc=0 out='OK\tout/15267276047/a.txt\t1\t120\n' +- unsupported-fails: GNU header with a sparse map (list): rc=0 out='a.txt\t1\t48\n' +- unsupported-fails: GNU header with a sparse map (manifest): rc=0 out='OK\tout/a.txt\t1\t120\n' +- unsupported-fails: unknown typeflag D (list): rc=0 out='u.txt\t1\t68\n' +- unsupported-fails: unknown typeflag D (manifest): rc=0 out='SKIP\tu.txt\t68\n' +- unsupported-fails: unknown typeflag M (list): rc=0 out='u.txt\t1\t77\n' +- unsupported-fails: unknown typeflag M (manifest): rc=0 out='SKIP\tu.txt\t77\n' +- unsupported-fails: unknown typeflag N (list): rc=0 out='u.txt\t1\t78\n' +- unsupported-fails: unknown typeflag N (manifest): rc=0 out='SKIP\tu.txt\t78\n' +- unsupported-fails: unknown typeflag S (list): rc=0 out='u.txt\t1\t83\n' +- unsupported-fails: unknown typeflag S (manifest): rc=0 out='SKIP\tu.txt\t83\n' +- unsupported-fails: unknown typeflag V (list): rc=0 out='u.txt\t1\t86\n' +- unsupported-fails: unknown typeflag V (manifest): rc=0 out='SKIP\tu.txt\t86\n' +- unsupported-fails: unknown typeflag A (list): rc=0 out='u.txt\t1\t65\n' +- unsupported-fails: unknown typeflag A (manifest): rc=0 out='SKIP\tu.txt\t65\n' +- unsupported-fails: unknown typeflag Z (list): rc=0 out='u.txt\t1\t90\n' +- unsupported-fails: unknown typeflag Z (manifest): rc=0 out='SKIP\tu.txt\t90\n' +- unsupported-fails: ustar magic with a GNU version (list): rc=0 out='m.txt\t1\t48\n' +- unsupported-fails: ustar magic with a GNU version (manifest): rc=0 out='OK\tout/m.txt\t1\t120\n' +- unsupported-fails: name ending in / with typeflag b'\x00' and data (list): rc=0 out='d/\t1\t0\n' +- unsupported-fails: name ending in / with typeflag b'\x00' and data (manifest): rc=0 out='OK\tout/d\t1\t120\n' +- unsupported-fails: name ending in / with typeflag b'0' and data (list): rc=0 out='e/\t1\t48\n' +- 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: 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, 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'] +- readable-manifest: names ending in / with typeflags NUL and 0, read as directories: rc=0 lean=['OK\tout/olddir\t0\t0', 'OK\tout/olddir/f.txt\t3\t319', 'OK\tout/slashdir\t0\t0'] expected=['SKIP\tolddir\t53', 'OK\tout/olddir/f.txt\t3\t319', 'SKIP\tslashdir\t48'] +- readable-list: typeflag 1 with a size field, then two files: rc=0 lean=[('node', 1024, 49), ('b.txt', 1, 48)] expected=[('node', 0, 49), ('hidden.txt', 6, 48), ('b.txt', 1, 48)] +- readable-manifest: typeflag 1 with a size field, then two files: rc=0 lean=['SKIP\tnode\t49', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t49', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98'] +- readable-list: typeflag 2 with a size field, then two files: rc=0 lean=[('node', 1024, 50), ('b.txt', 1, 48)] expected=[('node', 0, 50), ('hidden.txt', 6, 48), ('b.txt', 1, 48)] +- readable-manifest: typeflag 2 with a size field, then two files: rc=0 lean=['SKIP\tnode\t50', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t50', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98'] +- readable-list: typeflag 3 with a size field, then two files: rc=0 lean=[('node', 1024, 51), ('b.txt', 1, 48)] expected=[('node', 0, 51), ('hidden.txt', 6, 48), ('b.txt', 1, 48)] +- readable-manifest: typeflag 3 with a size field, then two files: rc=0 lean=['SKIP\tnode\t51', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t51', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98'] +- readable-list: typeflag 4 with a size field, then two files: rc=0 lean=[('node', 1024, 52), ('b.txt', 1, 48)] expected=[('node', 0, 52), ('hidden.txt', 6, 48), ('b.txt', 1, 48)] +- readable-manifest: typeflag 4 with a size field, then two files: rc=0 lean=['SKIP\tnode\t52', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t52', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98'] +- readable-list: typeflag 5 with a size field, then two files: rc=0 lean=[('node', 1024, 53), ('b.txt', 1, 48)] expected=[('node', 0, 53), ('hidden.txt', 6, 48), ('b.txt', 1, 48)] +- 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'] diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 76bc8d7..7070a4f 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -8,8 +8,8 @@ Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f29 - 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`: 29 +- 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 How the output is compared with tarfile. tarfile drops the `/` at the end of a diff --git a/tests/run_tests.py b/tests/run_tests.py index 0c7369b..1638769 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -10,8 +10,19 @@ 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. + +With `--tool REV`, the checks on the tool run against the tool built +from commit REV, in a temporary directory, instead of this checkout's. +The checkout is not changed or built. The axiom check reads this +checkout's proofs, not the tool, so it is left out. The record goes to +`tests/TEST-RESULTS-REV.md`, with REV as a short hash, and +`tests/TEST-RESULTS.md` is left as it is. This shows which of these +checks an earlier tool fails: + + python3 tests/run_tests.py --tool 1273382 """ +import argparse import io import os import random @@ -412,16 +423,56 @@ def skip_as_tarfile_reads(line): return line -def main(): - # 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) +def commit_of(rev): + """The short hash of commit `rev`.""" + r = subprocess.run(["git", "rev-parse", "--short=7", "--verify", rev + "^{commit}"], + cwd=PILOT_DIR, capture_output=True, text=True) + if r.returncode != 0: + sys.exit(f"not a commit: {rev}") + return r.stdout.strip() + + +def tool_at(rev, td): + """Build the tool at commit `rev` in `td`. The checkout is not + changed.""" + src = td / "tool-src" + src.mkdir() + r = subprocess.run(["git", "archive", "--format=tar", rev], cwd=PILOT_DIR, + capture_output=True) + if r.returncode != 0: + sys.exit(f"git archive {rev} failed: {r.stderr.decode()}") + with tarfile.open(fileobj=io.BytesIO(r.stdout)) as tf: + tf.extractall(src, filter="data") + build = subprocess.run(["lake", "build", "tar-pilot"], cwd=src, capture_output=True, + text=True) if build.returncode != 0: print(build.stdout + build.stderr) - sys.exit("lake build failed") + sys.exit(f"lake build failed at {rev}") + return src / ".lake" / "build" / "bin" / "tar-pilot" + + +def main(): + global EXE + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("--tool", metavar="REV", + help="check the tool built from commit REV instead of this checkout's, " + "and leave out the axiom check") + args = ap.parse_args() + rev = commit_of(args.tool) if args.tool else None + results = RESULTS if rev is None else PILOT_DIR / "tests" / f"TEST-RESULTS-{rev}.md" + # A run that stops early must not leave an earlier passing record. + results.unlink(missing_ok=True) + if rev is None: + build = subprocess.run(["lake", "build"], cwd=PILOT_DIR, capture_output=True, + text=True) + if build.returncode != 0: + print(build.stdout + build.stderr) + sys.exit("lake build failed") with tempfile.TemporaryDirectory() as td: td = Path(td) + if rev is not None: + EXE = tool_at(rev, td) archive_a = td / "a.tar" entries = build_archive_a(archive_a) @@ -566,43 +617,55 @@ def main(): # 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 = set(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 + # at most. Any other axiom, `sorryAx` included, fails the check. It + # reads this checkout's proofs, so it is left out with `--tool`. + if rev is None: + 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 = set(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() + if rev is None: + header = [f"Run by `tests/run_tests.py` against Python's `tarfile` module."] + count = f"- Checks run: {checks} ({axiom_checks} of them on the axioms of the theorems)" + else: + header = [ + f"Run by `tests/run_tests.py --tool {rev}` against Python's `tarfile` module.", + f"The tool was built from commit {rev}, not from this checkout. The axiom", + "check reads this checkout's proofs, not the tool, so it is left out.", + ] + count = f"- Checks run: {checks}, all on the tool" lines = [ "# Test results", "", - f"Run by `tests/run_tests.py` against Python's `tarfile` module.", + *header, f"Lean: {lean_ver}. Python: {sys.version.split()[0]}. System tar: {tar_version()}.", "", - f"- Checks run: {checks} ({axiom_checks} of them on the axioms of the theorems)", + count, f"- Failures: {len(failures)}", 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", f"- Files written by the Lean `create` command and read back by Python: {len(files)}", - "- Broken inputs rejected with exit code 1: truncated archive, " + "- Broken inputs that must fail with exit code 1: truncated archive, " "random garbage, corrupted checksum", - f"- Archives in formats the pilot does not read, rejected with exit code 1 " - f"by `list` and `manifest`: {unsupported}", + f"- Archives in formats the pilot does not read, which must fail with exit code 1 " + f"under `list` and `manifest`: {unsupported}", f"- Archives in other formats it reads, compared with tarfile under `list` and " f"`manifest`: {readable}", "", @@ -613,17 +676,13 @@ def main(): "tool's typeflag 0 on such an entry is read as 5. Every other typeflag is", "compared as printed.", "", - "Axiom check (`TarPilot/Verify.lean`):", - "", - "```", - ax_out.strip(), - "```", - "", ] + if rev is None: + lines += ["Axiom check (`TarPilot/Verify.lean`):", "", "```", ax_out.strip(), "```", ""] if failures: lines += ["## Failures", ""] + [f"- {f}" for f in failures] + [""] - RESULTS.write_text("\n".join(lines)) - print(f"{checks - len(failures)}/{checks} checks passed; results in {RESULTS}") + results.write_text("\n".join(lines)) + print(f"{checks - len(failures)}/{checks} checks passed; results in {results}") return 1 if failures else 0 From 5efda8cf3bc1c16f6a33cd215f6cfc018f7b31f3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 19:46:20 +0000 Subject: [PATCH 5/5] tests: rerun the old and new tool comparison with --new 1273382 The record merged from claude/containment-proofs says the new tool is this checkout. On this branch that is not the tool it was run on: this parser refuses or skips entries with a regular typeflag and a name ending in `/`, which the random names include, so a run against the checkout differs on purpose. A run of compare_old.py deletes its record first, and one that was stopped had left the file deleted in the working tree. The record is now from `python3 tests/compare_old.py --new 1273382`: 15000 runs, 0 differ once the new escapes are undone. Only the line naming the new tool changes. Without --new, the script reports 3480 of the 15000 runs that differ, on 696 archives. The page now gives the command with --new and says why. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 2 +- tests/COMPARE-OLD.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 736b354..8458d62 100644 --- a/README.md +++ b/README.md @@ -66,7 +66,7 @@ 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`. -`python3 tests/compare_old.py` builds the tool as it was before the containment change (commit 7517a86) 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`. +`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. diff --git a/tests/COMPARE-OLD.md b/tests/COMPARE-OLD.md index b0e8d65..11e2cc6 100644 --- a/tests/COMPARE-OLD.md +++ b/tests/COMPARE-OLD.md @@ -2,7 +2,7 @@ Written by `tests/compare_old.py`. Rerun it to check these numbers. -- Old tool: commit 7517a86. New tool: this checkout. +- Old tool: commit 7517a86. New tool: commit 1273382. - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.13.17. - Seed: 20261025 - Random archives: 3000, written by Python's `tarfile` in ustar format