From 1273382dbc5c13738810ad75638f6b91c7add03c Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 25 Oct 2026 03:47:39 +0000 Subject: [PATCH 1/7] Prove containment for every line the tool prints (audit F1, F5) The bar audit (Proven-Commons/mission#1) found that `extractAll_safe` says less than the claim: nothing stopped a component from holding `/`, so a gate that kept "a/../../etc/passwd" as one component proved the same statement. And the command-line tool re-implemented the extraction loop and the join instead of calling the proved function. Code: - The gate also rejects a component that holds `/` or a special character: a control character (C0, DEL, C1) or the Unicode line or paragraph separator. Entry names are split with `splitPath` (`String.split`). - `Main.lean` prints `o.line` for each outcome `o` of the proved `manifest`. REJECT and SKIP lines, and `list`, escape names (`\\`, `\xNN`, `\u2028`, `\u2029`). A destination that holds a special character, or U+FFFD (which the Lean runtime puts for bytes that are not UTF-8), is refused, and a destination ending in `/` no longer gives a doubled `/`. - On 3,000 random hostile archives under five destinations, the tool prints what it printed before, once escaped names are unescaped. It differs only where this commit means it to: names with special characters, which are now rejected and escaped, and destinations ending in `/` or holding special characters. Spec and proofs, with the standard axioms only: - `Spec/Defs.lean`: special characters, plain names, path components, the gate's rules, the regular typeflags, a path under a destination, how a name is printed, the exact line printed for an entry, lexical resolution. - `gate_eq` (the gate is exactly its rules), `gate_plain`, `manifest_eq` (what the manifest says about each entry), `manifest_extracted` (its extracted entries are exactly `extractAll`), `extractAll_contained`, `extractAll_joined`, `extractAll_resolves_inside`, `extractArchive_eq`, `extractArchive_resolves_inside`. - About the printed output: `manifest_lines_eq` (each line is exactly `Spec.line` for its entry) and `manifest_lines` (the only special characters in a line are its tabs, and every OK line is the destination exactly as given, then plain names joined by `/`, then a tab). `Spec/Defs.lean` proves `Spec.escape_noSpecial`: a printed name holds no special character, so it cannot break a line or a field. Tests: the script always builds first, checks that Verify.lean prints exactly the listed theorems and that each uses only the standard axioms, reads output on LF only, deletes the old record before it runs, and adds names with special characters and twelve destinations, five of them refused. A planted `sorry`, a planted axiom, and an extra unlisted theorem each fail it. The page states the theorems actually proved, drops "pilot complete" for "built, not yet verified", and links the audit. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Main.lean | 35 +-- Proofs.lean | 1 + Proofs/Contain.lean | 535 ++++++++++++++++++++++++++++++++++++++++++ README.md | 43 ++-- Spec/Defs.lean | 182 ++++++++++++++ TarPilot/Archive.lean | 121 ++++++---- TarPilot/Path.lean | 108 +++------ TarPilot/Verify.lean | 17 +- lakefile.toml | 9 +- tests/TEST-RESULTS.md | 23 +- tests/run_tests.py | 155 +++++++++--- 11 files changed, 1024 insertions(+), 205 deletions(-) create mode 100644 Proofs.lean create mode 100644 Proofs/Contain.lean create mode 100644 Spec/Defs.lean diff --git a/Main.lean b/Main.lean index 13448dc..2ce98ec 100644 --- a/Main.lean +++ b/Main.lean @@ -2,11 +2,19 @@ Command line front end for the tar pilot. tar-pilot list - Print one line per entry: name, data size, typeflag code. + Print one line per entry: name (escaped as in `manifest`), data + size, typeflag code. tar-pilot manifest Print what extraction would do, in archive order, without - writing anything to disk: + writing anything to disk. Each line is `o.line` for an outcome `o` + of the proved `manifest` of the parsed archive, in order + (`Proofs/Contain.lean`, `manifest_lines`). Names in REJECT and + SKIP lines are escaped: a backslash as two, a control character + as `\x` and two hex digits, U+2028 and U+2029 as `\u2028` and + `\u2029`. A destination with a special character, or with U+FFFD + (which the runtime puts for bytes that are not UTF-8), is + refused: OK for an extracted file REJECT for a regular file whose name fails the path gate @@ -20,9 +28,6 @@ import TarPilot open TarPilot -def byteSum (b : ByteArray) : Nat := - b.toList.foldl (fun a x => a + x.toNat) 0 - def runList (file : String) : IO UInt32 := do let data ← IO.FS.readBinFile file match parseArchive data with @@ -31,26 +36,24 @@ def runList (file : String) : IO UInt32 := do return 1 | some entries => for e in entries do - IO.println s!"{e.name}\t{e.data.size}\t{e.typeflag.toNat}" + IO.println s!"{escapeName e.name}\t{e.data.size}\t{e.typeflag.toNat}" return 0 def runManifest (file dest : String) : IO UInt32 := do + if dest.toList.any isSpecialChar then + IO.eprintln "error: the destination holds a control character or a line separator" + return 2 + if dest.toList.contains '\uFFFD' then + IO.eprintln "error: the destination is not valid UTF-8, or holds U+FFFD" + return 2 let data ← IO.FS.readBinFile file match parseArchive data with | none => IO.eprintln s!"error: cannot parse {file} as a ustar archive" return 1 | some entries => - let destCs := if dest = "" then [] else dest.splitOn "/" - for e in entries do - if isRegular e then - match gate e.name with - | none => IO.println s!"REJECT\t{e.name}" - | some rel => - let path := String.intercalate "/" (destCs ++ rel) - IO.println s!"OK\t{path}\t{e.data.size}\t{byteSum e.data}" - else - IO.println s!"SKIP\t{e.name}\t{e.typeflag.toNat}" + for o in manifest (destComponents dest) entries do + IO.println o.line return 0 def runCreate (out : String) (files : List String) : IO UInt32 := do diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..cbe883b --- /dev/null +++ b/Proofs.lean @@ -0,0 +1 @@ +import Proofs.Contain diff --git a/Proofs/Contain.lean b/Proofs/Contain.lean new file mode 100644 index 0000000..9da005a --- /dev/null +++ b/Proofs/Contain.lean @@ -0,0 +1,535 @@ +/- + The theorems about the path gate, extraction, and what the + command-line tool prints. + + The statements use the definitions in `Spec/Defs.lean`: what a plain + name and a control character are, the components of a path string, + the gate's rules, the regular typeflags, a path under a destination, + and lexical path resolution. The helper lemmas are in + `TarPilot.Contain`. +-/ + +import TarPilot.Archive +import Spec.Defs + +open Spec + +namespace TarPilot.Contain + +theorem not_mem_of_mem_splitOn {α} [BEq α] [LawfulBEq α] (a : α) : + ∀ (xs l : List α), l ∈ xs.splitOn a → a ∉ l := by + intro xs + induction xs with + | nil => intro l h; simp [List.splitOn_nil] at h; subst h; simp + | cons x xs ih => + intro l h + rw [List.splitOn_cons_eq_ite_modifyHead] at h + split at h + · simp only [List.mem_cons] at h + rcases h with rfl | h + · simp + · exact ih l h + · rename_i hx + obtain ⟨y, ys, hys⟩ := List.exists_cons_of_ne_nil (List.splitOn_ne_nil a xs) + rw [hys] at h ih + simp only [List.modifyHead_cons, List.mem_cons] at h + rcases h with rfl | h + · intro hmem + simp only [List.mem_cons] at hmem + rcases hmem with rfl | hmem + · simp at hx + · exact ih y (by simp) hmem + · exact ih l (by simp [h]) + +theorem splitPath_eq (s : String) : + splitPath s = (s.toList.splitOn '/').map String.ofList := by + unfold splitPath + rw [String.toList_split_char] + +theorem splitPath_ne_nil (s : String) : splitPath s ≠ [] := by + rw [splitPath_eq]; simp + +theorem splitPath_noSlash (s : String) : ∀ d ∈ splitPath s, '/' ∉ d.toList := by + intro d hd + rw [splitPath_eq] at hd + simp only [List.mem_map] at hd + obtain ⟨l, hl, rfl⟩ := hd + simpa using not_mem_of_mem_splitOn '/' _ l hl + +theorem intercalate_ofList (L : List (List Char)) : + String.intercalate "/" (L.map String.ofList) = String.ofList (['/'].intercalate L) := by + apply String.toList_inj.mp + simp [Function.comp_def] + +theorem joinPath_splitPath (s : String) : joinPath (splitPath s) = s := by + unfold joinPath + rw [splitPath_eq, intercalate_ofList, List.intercalate_splitOn] + simp + +theorem mem_intercalate (L : List String) (ch : Char) : + ch ∈ (String.intercalate "/" L).toList → ch = '/' ∨ ∃ s ∈ L, ch ∈ s.toList := by + intro h + rw [String.toList_intercalate] at h + induction L with + | nil => simp at h + | cons s L ih => + cases L with + | nil => exact Or.inr ⟨s, by simp, by simpa using h⟩ + | cons t L => + simp only [List.map_cons, List.intercalate_cons_cons, List.mem_append] at h + rcases h with (h | h) | h + · exact Or.inr ⟨s, by simp, h⟩ + · left; simpa using h + · rcases ih (by simpa using h) with h | ⟨u, hu, hc⟩ + · exact Or.inl h + · exact Or.inr ⟨u, by simp [hu], hc⟩ + +theorem isSpecialChar_eq : isSpecialChar = Spec.isSpecial := rfl + +theorem cleanComponents_plain : ∀ (cs out : List String), + cleanComponents cs = some out → ∀ c ∈ out, PlainName c := by + intro cs + induction cs with + | nil => + intro out h + simp [cleanComponents] at h + subst h + simp + | cons c cs ih => + intro out h + unfold cleanComponents at h + split at h + · simp at h + · rename_i hbad + cases hrec : cleanComponents cs with + | none => + rw [hrec] at h + simp at h + | some rest => + rw [hrec] at h + simp only [Option.map_some, Option.some.injEq] at h + have ih' := ih rest hrec + split at h + · subst h + exact ih' + · rename_i hskip + subst h + intro x hx + simp only [List.mem_cons] at hx + rcases hx with rfl | hx + · simp only [not_or, List.any_eq_true, not_exists, not_and, Bool.not_eq_true, + isSpecialChar_eq] at hbad hskip + exact ⟨hskip.1, hskip.2, hbad.1, + fun ch hch => ⟨fun h => hbad.2.1 (h ▸ hch), hbad.2.2 ch hch⟩⟩ + · exact ih' x hx + +theorem cleanComponents_eq : ∀ cs : List String, (∀ c ∈ cs, '/' ∉ c.toList) → + cleanComponents cs = + if cs.any (fun c => c == ".." || c.toList.any Spec.isSpecial) then none + else some (cs.filter (fun c => !(c == "" || c == "."))) := by + intro cs + induction cs with + | nil => intro _; rfl + | cons c cs ih => + intro h + have hc : '/' ∉ c.toList := h c (by simp) + have hcs : ∀ x ∈ cs, '/' ∉ x.toList := fun x hx => h x (by simp [hx]) + rw [cleanComponents, ih hcs, isSpecialChar_eq] + by_cases h1 : c = ".." + · simp [h1] + · by_cases h2 : c.toList.any Spec.isSpecial = true + · simp [h1, h2] + · by_cases h3 : ∃ x, x ∈ cs ∧ (x = ".." ∨ ∃ ch ∈ x.toList, Spec.isSpecial ch = true) + · simp [h1, h2, hc, h3] + · by_cases h4 : c = "" ∨ c = "." + · rcases h4 with h4 | h4 <;> simp [h4, h3] + · simp only [not_or] at h4 + simp only [Bool.not_eq_true] at h2 + simp [h1, h2, hc, h3, h4.1, h4.2] + +theorem pathComponents_join (l : List String) (hl : ∀ s ∈ l, '/' ∉ s.toList) + (hne : l ≠ []) : pathComponents (String.intercalate "/" l) = l := by + have h := String.toList_split_intercalate (c := '/') hl + simp only [hne, ite_false] at h + exact h + +theorem resolve_append : ∀ (xs ys acc : List String), + resolve acc (xs ++ ys) = resolve (resolve acc xs) ys := by + intro xs + induction xs with + | nil => intro ys acc; simp [resolve] + | cons c cs ih => + intro ys acc + simp only [List.cons_append, resolve] + split + · exact ih ys _ + · split + · split + · exact ih ys _ + · exact ih ys _ + · exact ih ys _ + +theorem resolve_plain : ∀ (rel acc : List String), (∀ c ∈ rel, PlainName c) → + resolve acc rel = acc ++ rel := by + intro rel + induction rel with + | nil => intro acc _; simp [resolve] + | cons c cs ih => + intro acc h + have ⟨h1, h2, h3, _⟩ := h c (by simp) + have hcs : ∀ x ∈ cs, PlainName x := fun x hx => h x (by simp [hx]) + simp only [resolve, h1, h2, h3, or_self, ite_false] + rw [ih _ hcs] + simp + +theorem destComponents_noSlash (dest : String) : + ∀ d ∈ destComponents dest, '/' ∉ d.toList := by + unfold destComponents + split + · simp + · split + · intro d hd + exact splitPath_noSlash dest d (List.dropLast_subset _ hd) + · exact splitPath_noSlash dest + +/-- The path the tool prints for `rel` is the destination string, as + given, followed by `rel`. -/ +theorem joinPath_dest (dest : String) (rel : List String) (hrel : rel ≠ []) : + joinPath (destComponents dest ++ rel) = under dest (joinPath rel) := by + unfold destComponents under + split + · simp + · rename_i hd + split + · rename_i hlast + have hsplit : dest.toList = dest.toList.dropLast ++ ['/'] := by + have hne : dest.toList ≠ [] := by intro h; simp [h] at hlast + have := List.dropLast_concat_getLast hne + rw [List.getLast?_eq_some_getLast hne] at hlast + injection hlast with hl + rw [hl] at this + exact this.symm + have hdl : splitPath dest = splitPath (String.ofList dest.toList.dropLast) ++ [""] := by + rw [splitPath_eq, splitPath_eq, hsplit, List.splitOn_append_cons_self] + simp + rw [hdl, List.dropLast_concat] + unfold joinPath + rw [String.intercalate_append_of_ne_nil (splitPath_ne_nil _) hrel] + have := joinPath_splitPath (String.ofList dest.toList.dropLast) + unfold joinPath at this + rw [this] + apply String.toList_inj.mp + conv => rhs; rw [String.toList_append, hsplit] + simp + · unfold joinPath + rw [String.intercalate_append_of_ne_nil (splitPath_ne_nil _) hrel] + have := joinPath_splitPath dest + unfold joinPath at this + rw [this] + +theorem toString_noSpecial (n : Nat) : ∀ ch ∈ (toString n).toList, Spec.isSpecial ch = false := by + intro ch hch + have hrepr : (toString n) = String.ofList (Nat.toDigits 10 n) := Nat.repr_eq_ofList_toDigits + rw [hrepr, String.toList_ofList] at hch + have hd := Nat.isDigit_of_mem_toDigits (by decide) (by decide) hch + simp only [Char.isDigit, Bool.and_eq_true, decide_eq_true_eq, + UInt32.le_iff_toNat_le] at hd + simp only [Char.reduceVal, UInt32.reduceToNat] at hd + have h1 : 48 ≤ ch.toNat := hd.1 + have h2 : ch.toNat ≤ 57 := hd.2 + simp only [Spec.isSpecial, Bool.or_eq_false_iff, decide_eq_false_iff_not, + Bool.and_eq_false_iff, beq_eq_false_iff_ne, ne_eq] + omega + +theorem escapeChar_eq (c : Char) : escapeChar c = (Spec.escapeChar c).toList := by + unfold escapeChar Spec.escapeChar + by_cases h1 : c = '\\' + · subst h1; decide + · by_cases h2 : c.toNat = 0x2028 + · simp [h1, h2] + · by_cases h3 : c.toNat = 0x2029 + · simp [h1, h3] + · by_cases h4 : Spec.isSpecial c = true + · simp [h1, h2, h3, isSpecialChar_eq, h4, Spec.hexDigit] + · simp only [Bool.not_eq_true] at h4 + simp [h1, h2, h3, isSpecialChar_eq, h4] + +theorem escapeName_eq (s : String) : escapeName s = Spec.escape s := by + apply String.toList_inj.mp + unfold escapeName Spec.escape + rw [String.toList_ofList, String.toList_join, List.flatMap_map] + congr 1 + funext c + exact escapeChar_eq c + +theorem escapeName_noSpecial (s : String) : + ∀ ch ∈ (escapeName s).toList, Spec.isSpecial ch = false := by + rw [escapeName_eq] + exact Spec.escape_noSpecial s + +theorem byteSum_eq (b : ByteArray) : byteSum b = Spec.byteSum b := by + unfold byteSum Spec.byteSum + have : ∀ (l : List UInt8) (acc : Nat), + l.foldl (fun a x => a + x.toNat) acc = acc + (l.map UInt8.toNat).sum := by + intro l + induction l with + | nil => intro acc; simp + | cons x xs ih => intro acc; simp [ih]; omega + rw [this]; simp + +end TarPilot.Contain + +namespace TarPilot + +open TarPilot.Contain + +/-- The gate is exactly its rules (`Spec.cleanName`). -/ +theorem gate_eq (name : String) : gate name = Spec.cleanName name := by + unfold gate Spec.cleanName components + split + · rfl + · have hp : splitPath name = pathComponents name := rfl + rw [cleanComponents_eq _ (splitPath_noSlash name), hp] + by_cases ha : (pathComponents name).any + (fun c => c == ".." || c.toList.any Spec.isSpecial) = true + · simp only [ha, ite_true] + · simp only [ha] + cases hk : (pathComponents name).filter (fun c => !(c == "" || c == ".")) with + | nil => simp + | cons r rs => simp + +/-- 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 := by + intro hg + unfold gate at hg + split at hg + · simp at hg + · split at hg + · rename_i r rs hc + injection hg with hg + subst hg + exact ⟨by simp, cleanComponents_plain _ _ hc⟩ + · simp at hg + +/-- 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 then + match cleanName e.name with + | some rel => .extract (dest ++ rel) e.data + | none => .reject e.name + else .skip e.name e.typeflag := by + unfold manifest + congr 1 + funext e + unfold outcome isRegular regularType + rw [gate_eq] + split + · cases cleanName e.name <;> rfl + · rfl + +/-- 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 := by + intro h + unfold extractAll at h + rw [List.mem_filterMap] at h + obtain ⟨e, _, hfe⟩ := h + split at hfe + · cases hg : gate e.name with + | none => + rw [hg] at hfe + simp at hfe + | some rel => + rw [hg] at hfe + simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at hfe + obtain ⟨hne, hplain⟩ := gate_plain e.name rel hg + exact ⟨rel, hne, hfe.1.symm, hplain⟩ + · simp at hfe + +/-- 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 := by + intro hdest h + obtain ⟨rel, hne, hpath, hplain⟩ := extractAll_contained dest entries path bytes h + refine ⟨rel, hne, hplain, ?_⟩ + subst hpath + apply pathComponents_join + · intro s hs + rcases List.mem_append.mp hs with hs | hs + · exact hdest s hs + · exact fun h => ((hplain s hs).2.2.2 '/' h).1 rfl + · simp [hne] + +/-- 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 := by + intro hdest h + obtain ⟨rel, hne, hplain, hjoin⟩ := extractAll_joined dest entries path bytes hdest h + exact ⟨rel, hne, hplain, by rw [hjoin, resolve_append, resolve_plain rel _ hplain]⟩ + +/-- 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 := by + intro hdest h hmem + unfold extractArchive at h + cases hp : parseArchive data with + | none => + rw [hp] at h + simp at h + | some entries => + rw [hp] at h + simp only [Option.map_some, Option.some.injEq] at h + subst h + exact extractAll_resolves_inside dest entries path bytes hdest hmem + +/-- 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 := by + have h : ∀ e : RawEntry, (outcome dest e).extracted = + if isRegular e then (gate e.name).map fun rel => (dest ++ rel, e.data) else none := by + intro e + unfold outcome + by_cases hr : isRegular e + · cases gate e.name <;> simp [hr, Outcome.extracted] + · simp [hr, Outcome.extracted] + simp only [manifest, extractAll, List.filterMap_map] + congr 1 + funext e + exact h e + +/-- 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) := by + unfold manifest at ho + obtain ⟨e, _, rfl⟩ := List.mem_map.mp ho + unfold outcome + split + · split + · rename_i rel hg + obtain ⟨hne, hplain⟩ := gate_plain e.name rel hg + have hjoin := joinPath_dest dest rel hne + have hpath : ∀ ch ∈ (joinPath (destComponents dest ++ rel)).toList, + Spec.isSpecial ch = false := by + rw [hjoin] + intro ch hch + unfold under at hch + have hrel : ∀ ch ∈ (joinPath rel).toList, Spec.isSpecial ch = false := by + intro ch hch + rcases mem_intercalate rel ch hch with rfl | ⟨s, hs, hcs⟩ + · decide + · exact ((hplain s hs).2.2.2 ch hcs).2 + split at hch + · exact hrel ch hch + · split at hch + · simp only [String.toList_append, List.mem_append] at hch + rcases hch with h | h + · exact hdest ch h + · exact hrel ch h + · simp only [String.toList_append, List.mem_append] at hch + rcases hch with (h | h) | h + · exact hdest ch h + · simp at h; subst h; decide + · exact hrel ch h + constructor + · intro ch hch hc + simp only [Outcome.line, String.toList_append, List.mem_append] at hch + rcases hch with ((((h | h) | h) | h) | h) | h + · simp at h; rcases h with rfl | rfl | rfl <;> (revert hc; decide) + · rw [hpath ch h] at hc; simp at hc + · simpa using h + · rw [toString_noSpecial _ ch h] at hc; simp at hc + · simpa using h + · rw [toString_noSpecial _ ch h] at hc; simp at hc + · intro _ + refine ⟨rel, toString e.data.size ++ "\t" ++ toString (byteSum e.data), hne, hplain, ?_⟩ + simp only [Outcome.line] + rw [hjoin] + unfold joinPath + simp only [String.append_assoc] + · constructor + · intro ch hch hc + simp only [Outcome.line, String.toList_append, List.mem_append] at hch + rcases hch with h | h + · simp at h; rcases h with h | h | h | h | h | h | h <;> subst h <;> (revert hc; decide) + · rw [escapeName_noSpecial _ ch h] at hc; simp at hc + · intro h + simp [Outcome.line] at h + · constructor + · intro ch hch hc + simp only [Outcome.line, String.toList_append, List.mem_append] at hch + rcases hch with ((h | h) | h) | h + · simp at h; rcases h with h | h | h | h | h <;> subst h <;> (revert hc; decide) + · rw [escapeName_noSpecial _ ch h] at hc; simp at hc + · simpa using h + · rw [toString_noSpecial _ ch h] at hc; simp at hc + · intro h + simp [Outcome.line] at h + +/-- 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 := by + unfold manifest + rw [List.map_map] + congr 1 + funext e + simp only [Function.comp_apply] + unfold outcome Spec.line + have hreg : isRegular e = regularType e.typeflag := rfl + rw [hreg, gate_eq] + split + · split + · rename_i rel hc + have hne : rel ≠ [] := (gate_plain e.name rel (by rw [gate_eq]; exact hc)).1 + simp only [Outcome.line] + rw [joinPath_dest dest rel hne, byteSum_eq, hc] + rfl + · rename_i hc + simp only [Outcome.line, escapeName_eq, hc] + · simp only [Outcome.line, escapeName_eq] + +/-- 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) := rfl + +end TarPilot diff --git a/README.md b/README.md index 84910ee..1e41ac4 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,8 @@ # 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 built by joining the destination with a cleaned relative path. A machine-checked proof shows the cleaned path can never climb out of the 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. -It is the first Proven Commons project, built to the verified bar published in the org's home repo, [proven-commons](https://github.com/Proven-Commons/proven-commons). Status: pilot complete, October 2026. +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). ## Run it @@ -15,27 +15,38 @@ 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. +`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). ## What is proved -The path gate and the extraction rule, in `TarPilot/Path.lean` and `TarPilot/Archive.lean`: +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. -- `gate_sound`: a name that passes the gate gives relative components with no `..`, no empty component, no `.`, and the list is not empty. -- `cleanComponents_sound`: the component cleaner behind the gate has the same properties. -- `extractAll_safe`: every path the extractor emits is the destination components followed by a gated relative path, so no emitted path escapes the destination. -- `extractArchive_safe`: the same guarantee for an archive read from bytes. +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: absolute names are rejected. Any `..` component is rejected. Empty and `.` components are dropped. A name with nothing left is rejected. Only regular files (typeflag `0` or NUL) are extracted. 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. +- `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. -Axiom check: each proof depends only on the standard Lean axioms (`propext`, `Classical.choice`, `Quot.sound`, or a subset). Full output is recorded in `tests/TEST-RESULTS.md`. +The statements fix what extraction does with a parsed archive. They do not fix how bytes are parsed into entries, which the tests cover. + +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`. ## 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`: 16 checks, 0 failures, on 14 archive entries covering normal files, hostile names, a long name split over the ustar prefix field, and broken inputs (truncated, garbage, bad checksum). -- 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, symlinked destination folders) is outside this project for now. +- 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). +- 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. - The Lean compiler, runtime, and kernel are trusted, as in every Lean project. A bug in them is outside the proof. @@ -47,14 +58,16 @@ lake env lean TarPilot/Verify.lean python3 tests/run_tests.py ``` -The build fails if a proof breaks. The second command prints the axiom list. The test script rebuilds if needed, reruns every comparison, and rewrites `tests/TEST-RESULTS.md`. +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`. ## Layout -- `TarPilot/Path.lean`: the path gate and its proofs. +- `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 safety theorems. +- `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`. diff --git a/Spec/Defs.lean b/Spec/Defs.lean new file mode 100644 index 0000000..e707289 --- /dev/null +++ b/Spec/Defs.lean @@ -0,0 +1,182 @@ +/- + The definitions the statements in `Proofs/Contain.lean` use, written + from the rules in `SPEC.md` and from POSIX. + + The statements are about these code definitions in `TarPilot/`, which + a reviewer should read with them: `gate`, `manifest` and its + `Outcome`s, `Outcome.line`, `destComponents`, `joinPath`, + `extractAll`, and `extractArchive`; and `Main.lean`, which prints + `o.line` for each outcome `o` of `manifest (destComponents dest) + entries`. Where a statement says a code definition equals one of the + definitions here, the one here is what to read. +-/ + +namespace Spec + +/-- A special character: one the tool never prints raw. These are the + control characters (C0 below space, DEL, and C1; tab, line feed and + carriage return among them) and the Unicode line separator U+2028 + and paragraph separator U+2029, which some readers take as line + breaks. -/ +def isSpecial (c : Char) : Bool := + c.toNat < 0x20 || (0x7F ≤ c.toNat && c.toNat < 0xA0) || c.toNat == 0x2028 || + c.toNat == 0x2029 + +/-- A component that names one entry inside its directory: not empty, + not `.` or `..`, and free of `/` and of special characters (NUL + among them). -/ +def PlainName (c : String) : Prop := + c ≠ "" ∧ c ≠ "." ∧ c ≠ ".." ∧ ∀ ch ∈ c.toList, ch ≠ '/' ∧ isSpecial ch = false + +/-- The components a system sees in a path string: the parts between `/`. + An absolute path starts with an empty part. -/ +def pathComponents (s : String) : List String := + (s.split '/').toList.map (·.copy) + +/-- The path gate, from its rules: an absolute name (one that starts with + `/`) is rejected; a name with a `..` component, or with a special + character, is rejected; + empty and `.` components are dropped; and a name with nothing left + is rejected. Otherwise the result is the components that are left. -/ +def cleanName (name : String) : Option (List String) := + if name.toList.head? = some '/' then none + else + let parts := pathComponents name + if parts.any (fun c => c == ".." || c.toList.any isSpecial) then none + else + 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 + +/-- A relative path `rel` under the destination `dest`, as a string: `rel` + alone when `dest` is empty, `dest` then `rel` when `dest` ends in `/`, + and `dest`, `/`, `rel` otherwise. -/ +def under (dest rel : String) : String := + if dest = "" then rel + else if dest.toList.getLast? = some '/' then dest ++ rel + else dest ++ "/" ++ rel + +/-- A hex digit, `0` to `9` then `a` to `f`. -/ +def hexDigit (n : Nat) : Char := + "0123456789abcdef".toList.getD n '0' + +/-- How the tool prints one character of a name: a backslash as two; + U+2028 and U+2029 as `\u2028` and `\u2029`; any other special + character, all of which are below 0xA0, as `\x` and two hex digits; + and any other character as itself. -/ +def escapeChar (c : Char) : String := + if c = '\\' then "\\\\" + else if c.toNat = 0x2028 then "\\u2028" + else if c.toNat = 0x2029 then "\\u2029" + else if isSpecial c then + String.ofList ['\\', 'x', hexDigit (c.toNat / 16), hexDigit (c.toNat % 16)] + else c.toString + +/-- How the tool prints a name. -/ +def escape (s : String) : String := + String.join (s.toList.map escapeChar) + +/-- A hex digit is never special. -/ +theorem hexDigit_noSpecial (n : Nat) : isSpecial (hexDigit n) = false := by + have hex : ∀ i : Fin 16, isSpecial (hexDigit i.val) = false := by decide + by_cases h : n < 16 + · exact hex ⟨n, h⟩ + · have : hexDigit n = '0' := by + unfold hexDigit + rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by simp; omega)] + rfl + rw [this]; decide + +/-- A printed character of a name is never special. -/ +theorem escapeChar_noSpecial (c : Char) : + ∀ ch ∈ (escapeChar c).toList, isSpecial ch = false := by + intro ch hch + unfold escapeChar at hch + split at hch + · simp at hch; subst hch; decide + · split at hch + · simp at hch; rcases hch with rfl | rfl | rfl | rfl | rfl | rfl <;> decide + · split at hch + · simp at hch; rcases hch with rfl | rfl | rfl | rfl | rfl | rfl <;> decide + · split at hch + · simp only [String.toList_ofList, List.mem_cons, List.mem_nil_iff, or_false] at hch + rcases hch with rfl | rfl | rfl | rfl + · decide + · decide + · exact hexDigit_noSpecial _ + · exact hexDigit_noSpecial _ + · rename_i _ _ _ hc + simp at hch + subst hch + simpa using hc + +/-- 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 + +/-- The sum of the bytes of a file. -/ +def byteSum (b : ByteArray) : Nat := + (b.toList.map UInt8.toNat).sum + +/-- The line `tar-pilot manifest ` prints for an entry with + name `name`, typeflag `t`, and data `data`, with fields separated by + tabs: `OK`, the path, the size, and the byte sum, for a regular file + whose name passes the gate; `REJECT` and the name, for a regular file + 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 + match cleanName name with + | some rel => + "OK\t" ++ under dest (String.intercalate "/" rel) ++ "\t" ++ toString data.size ++ + "\t" ++ toString (byteSum data) + | none => "REJECT\t" ++ escape name + else "SKIP\t" ++ escape name ++ "\t" ++ toString t.toNat + +/-- Resolve the components of a relative path lexically, as POSIX does + when no component is a symlink, after the components already + resolved in `acc`: an empty part and `.` change nothing, `..` removes + the last component (or is kept when there is none to remove, or the + last is itself `..`), and any other part is appended. An absolute + path's leading empty part changes nothing, so the root is dropped: + read an absolute path's result from `/`. -/ +def resolve : List String → List String → List String + | acc, [] => acc + | acc, c :: cs => + if c = "" ∨ c = "." then resolve acc cs + else if c = ".." then + if acc = [] ∨ acc.getLast? = some ".." then resolve (acc ++ [".."]) cs + else resolve acc.dropLast cs + else resolve (acc ++ [c]) cs + +example : pathComponents "out/a//b/" = ["out", "a", "", "b", ""] := by + simp only [pathComponents, String.toList_split_char]; decide + +example : resolve [] (pathComponents "out/a/../../../etc/./passwd") = + ["..", "etc", "passwd"] := by + simp only [pathComponents, String.toList_split_char]; decide + +example : cleanName "a/./b//c" = some ["a", "b", "c"] := by + simp only [cleanName, pathComponents, String.toList_split_char]; decide + +example : cleanName "a/../b" = none ∧ cleanName "/etc/passwd" = none ∧ + cleanName "./" = none ∧ cleanName "a\nb" = none ∧ cleanName "a\u2028b" = none := by + simp only [cleanName, pathComponents, String.toList_split_char]; decide + +example : under "out" "a/b" = "out/a/b" ∧ under "/" "a" = "/a" ∧ under "" "a" = "a" := by + decide + +example : escape "a\\b\tc\u2028d\u0085" = "a\\\\b\\x09c\\u2028d\\x85" := by + decide + +end Spec diff --git a/TarPilot/Archive.lean b/TarPilot/Archive.lean index b3af75d..b6d8268 100644 --- a/TarPilot/Archive.lean +++ b/TarPilot/Archive.lean @@ -2,10 +2,10 @@ Whole-archive parsing, extraction, and writing. The extraction rule is the proved part, together with the path gate - in `Path.lean`: `extractAll` only emits a path built as - `dest ++ rel`, where `rel` passed the gate, and the theorem - `extractAll_safe` states that every emitted relative path has no - `..`, no empty component, no `.`, and is not empty. + in `Path.lean`: `extractAll` only emits a path built as `dest ++ rel`, + where `rel` passed the gate. `manifest` is what the command-line tool + prints, and its extracted entries are exactly the output of + `extractAll`. The proofs are in `Proofs/Contain.lean`. Parsing and writing are covered by differential tests against Python's `tarfile` module (see `tests/`), not by a proof. @@ -67,57 +67,78 @@ def extractAll (dest : List String) (entries : List RawEntry) : (gate e.name).map fun rel => (dest ++ rel, e.data) else none -/-- Every path `extractAll` emits is the destination followed by a - gated relative path: no `..`, no empty component, no `.`, and the - relative path is not empty. So no emitted path escapes the - destination. -/ -theorem extractAll_safe : ∀ (dest : List String) (entries : List RawEntry) - (path : List String) (bytes : ByteArray), - (path, bytes) ∈ extractAll dest entries → - ∃ rel, path = dest ++ rel ∧ - ".." ∉ rel ∧ "" ∉ rel ∧ "." ∉ rel ∧ rel ≠ [] := by - intro dest entries path bytes h - unfold extractAll at h - rw [List.mem_filterMap] at h - obtain ⟨e, _, hfe⟩ := h - by_cases hreg : isRegular e - · rw [if_pos hreg] at hfe - cases hg : gate e.name with - | none => - rw [hg] at hfe - simp at hfe - | some rel => - rw [hg] at hfe - simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at hfe - obtain ⟨hpath, _⟩ := hfe - obtain ⟨h1, h2, h3, h4⟩ := gate_sound e.name rel hg - exact ⟨rel, hpath.symm, h1, h2, h3, h4⟩ - · rw [if_neg hreg] at hfe - exact absurd hfe (by simp) - /-- Parse, then extract. -/ def extractArchive (dest : List String) (data : ByteArray) : Option (List (List String × ByteArray)) := (parseArchive data).map (extractAll dest) -/-- The same guarantee for a whole archive read from bytes. -/ -theorem extractArchive_safe : ∀ (dest : List String) (data : ByteArray) - (out : List (List String × ByteArray)) (path : List String) - (bytes : ByteArray), - extractArchive dest data = some out → (path, bytes) ∈ out → - ∃ rel, path = dest ++ rel ∧ - ".." ∉ rel ∧ "" ∉ rel ∧ "." ∉ rel ∧ rel ≠ [] := by - intro dest data out path bytes h hmem - unfold extractArchive at h - cases hp : parseArchive data with - | none => - rw [hp] at h - simp at h - | some entries => - rw [hp] at h - simp only [Option.map_some, Option.some.injEq] at h - subst h - exact extractAll_safe dest entries path bytes hmem +/-- What extraction does with one entry. -/ +inductive Outcome where + /-- A regular file, written at this path. -/ + | extract (path : List String) (data : ByteArray) + /-- A regular file whose name fails the gate. -/ + | reject (name : String) + /-- An entry that is not a regular file. -/ + | skip (name : String) (typeflag : Char) + +/-- The outcome for one entry, under the destination `dest`. -/ +def outcome (dest : List String) (e : RawEntry) : Outcome := + if isRegular e then + match gate e.name with + | some rel => .extract (dest ++ rel) e.data + | none => .reject e.name + else .skip e.name e.typeflag + +/-- The path and data of an extracted entry. -/ +def Outcome.extracted : Outcome → Option (List String × ByteArray) + | .extract path data => some (path, data) + | _ => none + +/-- The outcome for every entry, in archive order: what the command-line + tool prints. -/ +def manifest (dest : List String) (entries : List RawEntry) : List Outcome := + entries.map (outcome dest) + +/-- The components of the destination the command-line tool is given. + An empty destination means the current directory. A final `/` adds + no empty component, so the path under `out/` is `out/a`, not + `out//a`. -/ +def destComponents (dest : String) : List String := + if dest = "" then [] + else if dest.toList.getLast? = some '/' then (splitPath dest).dropLast + else splitPath dest + +/-- A path as one string, its components joined with `/`. -/ +def joinPath (path : List String) : String := + String.intercalate "/" path + +/-- The sum of the bytes, printed as a check on the data. -/ +def byteSum (b : ByteArray) : Nat := + b.toList.foldl (fun a x => a + x.toNat) 0 + +/-- One character of a printed name: a backslash as `\\`, a control + character as `\x` and two hex digits, the line and paragraph + separators as `\u2028` and `\u2029`, any other as itself. -/ +def escapeChar (c : Char) : List Char := + if c = '\\' then ['\\', '\\'] + else if c.toNat == 0x2028 then "\\u2028".toList + else if c.toNat == 0x2029 then "\\u2029".toList + else if isSpecialChar c then + let hex := "0123456789abcdef".toList + ['\\', 'x', hex.getD (c.toNat / 16) '0', hex.getD (c.toNat % 16) '0'] + else [c] + +/-- A name as the tool prints it, with no special character left, so it + cannot break a line or a field. -/ +def escapeName (s : String) : String := + String.ofList (s.toList.flatMap escapeChar) + +/-- The line the command-line tool prints for one outcome. -/ +def Outcome.line : Outcome → String + | .extract path data => + "OK\t" ++ joinPath path ++ "\t" ++ toString data.size ++ "\t" ++ toString (byteSum data) + | .reject name => "REJECT\t" ++ escapeName name + | .skip name typeflag => "SKIP\t" ++ escapeName name ++ "\t" ++ toString typeflag.toNat /-- Build an archive from `(name, data)` pairs as regular files. Ends with two zero blocks, as the format expects. -/ diff --git a/TarPilot/Path.lean b/TarPilot/Path.lean index 300ee2b..ce07078 100644 --- a/TarPilot/Path.lean +++ b/TarPilot/Path.lean @@ -2,102 +2,52 @@ Path safety for tar entry names. A tar entry name is untrusted input. Before an entry may be extracted, - its name goes through `gate`, which produces a list of path components - that is proved to contain no `..`, no empty component, and no `.`, - and to be non-empty. Extraction joins those components under a - destination, so every extracted path stays under the destination by - construction (see `Archive.extractAll_safe`). + its name goes through `gate`, which gives a non-empty list of plain + names: no component is empty, `.` or `..`, or holds `/` or a special + character (a control character or a Unicode line or paragraph + separator). + Extraction puts those components after a destination, so every + extracted path stays under the destination. The proofs are in + `Proofs/Contain.lean`. -/ namespace TarPilot +/-- The parts of a path string between `/`. Used for entry names and for + the destination the command-line tool is given. -/ +def splitPath (s : String) : List String := + (s.split '/').toList.map (·.copy) + +/-- A special character: a control character (C0 below space, DEL, or + C1), or the Unicode line separator U+2028 or paragraph separator + U+2029. Any of these could make a printed name read as a line break. -/ +def isSpecialChar (c : Char) : Bool := + c.toNat < 32 || (127 ≤ c.toNat && c.toNat < 160) || c.toNat == 0x2028 || c.toNat == 0x2029 + /-- Split a tar entry name into path components. -/ def components (name : String) : List String := - name.splitOn "/" + splitPath name -/-- Drop empty and `.` components. Fail if any component is `..`. -/ +/-- Drop empty and `.` components. Fail if any component is `..`, or + holds `/` or a special character. Components from `splitPath` hold + no `/`; that check makes the proof direct. A special character, such + as a line break, could make a printed name read as a different line, + so a name holding one is never extracted. -/ def cleanComponents : List String → Option (List String) | [] => some [] | c :: cs => - if c = ".." then none + if c = ".." ∨ '/' ∈ c.toList ∨ c.toList.any isSpecialChar then none else (cleanComponents cs).map (fun rest => if c = "" ∨ c = "." then rest else c :: rest) -theorem cleanComponents_sound : ∀ (cs : List String) (out : List String), - cleanComponents cs = some out → - ".." ∉ out ∧ "" ∉ out ∧ "." ∉ out := by - intro cs - induction cs with - | nil => - intro out h - simp [cleanComponents] at h - subst h - simp - | cons c cs ih => - intro out h - rw [cleanComponents] at h - by_cases hpar : c = ".." - · rw [if_pos hpar] at h - exact absurd h (by simp) - · rw [if_neg hpar] at h - cases hrec : cleanComponents cs with - | none => - rw [hrec] at h - simp at h - | some rest => - rw [hrec] at h - obtain ⟨h1, h2, h3⟩ := ih rest hrec - by_cases hskip : c = "" ∨ c = "." - · rw [Option.map_some] at h - rw [if_pos hskip] at h - injection h with h' - subst h' - exact ⟨h1, h2, h3⟩ - · rw [Option.map_some] at h - rw [if_neg hskip] at h - injection h with h' - subst h' - have hn1 : c ≠ "" := fun hc => hskip (Or.inl hc) - have hn2 : c ≠ "." := fun hc => hskip (Or.inr hc) - refine ⟨?_, ?_, ?_⟩ - · simp only [List.mem_cons, not_or] - exact ⟨fun hh => hpar hh.symm, h1⟩ - · simp only [List.mem_cons, not_or] - exact ⟨fun hh => hn1 hh.symm, h2⟩ - · simp only [List.mem_cons, not_or] - exact ⟨fun hh => hn2 hh.symm, h3⟩ - /-- The gate every entry name must pass before extraction. - Absolute names are rejected. `..` is rejected. Empty and `.` - components are dropped. A name with nothing left is rejected. -/ + Absolute names are rejected. `..` and special characters are + rejected. Empty and `.` components are dropped. A name with nothing + left is rejected. -/ def gate (name : String) : Option (List String) := - if name.startsWith "/" then none + if name.toList.head? = some '/' then none else match cleanComponents (components name) with | some (r :: rs) => some (r :: rs) | _ => none -theorem gate_sound : ∀ (name : String) (rel : List String), - gate name = some rel → - ".." ∉ rel ∧ "" ∉ rel ∧ "." ∉ rel ∧ rel ≠ [] := by - intro name rel h - unfold gate at h - by_cases habs : name.startsWith "/" = true - · rw [if_pos habs] at h - exact absurd h (by simp) - · rw [if_neg habs] at h - cases hclean : cleanComponents (components name) with - | none => - rw [hclean] at h - exact absurd h (by simp) - | some out => - rw [hclean] at h - obtain ⟨h1, h2, h3⟩ := cleanComponents_sound _ _ hclean - cases out with - | nil => - exact absurd h (by simp) - | cons r rs => - injection h with h' - subst h' - exact ⟨h1, h2, h3, by simp⟩ - end TarPilot diff --git a/TarPilot/Verify.lean b/TarPilot/Verify.lean index 483c242..aeac8bf 100644 --- a/TarPilot/Verify.lean +++ b/TarPilot/Verify.lean @@ -5,9 +5,16 @@ or a subset of them. Any other name here breaks the verified bar. -/ -import TarPilot.Archive +import Proofs -#print axioms TarPilot.gate_sound -#print axioms TarPilot.cleanComponents_sound -#print axioms TarPilot.extractAll_safe -#print axioms TarPilot.extractArchive_safe +#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/lakefile.toml b/lakefile.toml index 31ddda4..0bda9f5 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,10 +1,17 @@ name = "tar-pilot" version = "0.1.0" -defaultTargets = ["TarPilot", "tar-pilot"] +defaultTargets = ["TarPilot", "Spec", "Proofs", "tar-pilot"] [[lean_lib]] name = "TarPilot" +[[lean_lib]] +name = "Spec" +roots = ["Spec.Defs"] + +[[lean_lib]] +name = "Proofs" + [[lean_exe]] name = "tar-pilot" root = "Main" diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index df8d2eb..514b31f 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -1,20 +1,27 @@ # 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.12.3. +Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.13.17. -- Checks run: 16 +- Checks run: 35 (13 of them on the axioms of the theorems) - Failures: 0 -- Archive A entries compared (list and manifest): 14 -- Manifest outcome on archive A: 9 extracted, 3 rejected by the path gate, 2 skipped as non-regular +- 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 Axiom check (`TarPilot/Verify.lean`): ``` -'TarPilot.gate_sound' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.cleanComponents_sound' depends on axioms: [propext] -'TarPilot.extractAll_safe' depends on axioms: [propext, Classical.choice, Quot.sound] -'TarPilot.extractArchive_safe' depends on axioms: [propext, Classical.choice, Quot.sound] +'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] ``` diff --git a/tests/run_tests.py b/tests/run_tests.py index 10fbf25..74400bd 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -7,14 +7,15 @@ python3 tests/run_tests.py -It builds the Lean project if the executable is missing, runs all -cases in a temporary directory, writes `tests/TEST-RESULTS.md`, and +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. """ import io import os import random +import re import subprocess import sys import tarfile @@ -24,6 +25,11 @@ 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 = [] @@ -38,17 +44,44 @@ def check(name, ok, detail=""): def run_lean(*args, cwd=None): - return subprocess.run([str(EXE), *args], capture_output=True, text=True, cwd=cwd) + """Run the tool. Its output is decoded without newline translation, + so a stray CR shows up as a mismatch.""" + r = subprocess.run([str(EXE), *args], capture_output=True, cwd=cwd) + return subprocess.CompletedProcess( + r.args, r.returncode, r.stdout.decode("utf-8", "surrogateescape"), + r.stderr.decode("utf-8", "surrogateescape")) + + +def is_special(c): + """A control character (C0 below space, DEL, or C1), or the line + separator U+2028 or the paragraph separator U+2029.""" + return ord(c) < 0x20 or 0x7F <= ord(c) < 0xA0 or c in "\u2028\u2029" + + +def escape_char(c): + if c == "\\": + return "\\\\" + if c in "\u2028\u2029": + return f"\\u{ord(c):04x}" + return f"\\x{ord(c):02x}" if is_special(c) else c + + +def escape_name(name): + """A name as the tool prints it: a backslash as two, U+2028 and + U+2029 as `\\u2028` and `\\u2029`, any other special character as + `\\x` and two hex digits.""" + return "".join(escape_char(c) for c in name) def spec_gate(name): """The extraction spec, implemented independently of the Lean code. Returns the cleaned relative components, or None to reject. - Absolute names are rejected. Any `..` is rejected. Empty and `.` - components are dropped. An empty result is rejected. + Absolute names are rejected. Any `..`, and any special character, + is rejected. Empty and `.` components are dropped. An empty result + is rejected. """ - if name.startswith("/"): + if name.startswith("/") or any(is_special(c) for c in name): return None out = [] for comp in name.split("/"): @@ -81,6 +114,15 @@ def build_archive_a(path): ("a//b.txt", b"ab", tarfile.REGTYPE), ("a/./c.txt", b"ac", tarfile.REGTYPE), ("link.txt", b"hello.txt", tarfile.SYMTYPE), + ("x\nOK\t/etc/passwd", b"line break in a name", tarfile.REGTYPE), + ("../y\nOK\t/etc/cron.d/z", b"line break in a rejected name", tarfile.REGTYPE), + ("tab\there.txt", b"tab", tarfile.REGTYPE), + ("del\x7f.txt", b"del", tarfile.REGTYPE), + ("nel\x85.txt", b"next line", tarfile.REGTYPE), + ("back\\slash.txt", b"backslash", tarfile.REGTYPE), + ("ls\u2028OK\t/etc/passwd", b"line separator in a name", tarfile.REGTYPE), + ("ps\u2029.txt", b"paragraph separator", tarfile.SYMTYPE), + ("link\nOK\t/etc/shadow", b"x", tarfile.SYMTYPE), ("p" * 50 + "/" + "x" * 70 + ".txt", b"long name split over prefix", tarfile.REGTYPE), ("deep/" + "/".join(f"d{i}" for i in range(8)) + "/leaf.txt", b"leaf", tarfile.REGTYPE), ] @@ -102,26 +144,57 @@ def build_archive_a(path): return entries -def expected_manifest(entries_data): +def under(dest, rel): + """The printed path of `rel` under `dest`.""" + if dest == "": + return rel + return dest + rel if dest.endswith("/") else dest + "/" + rel + + +def expected_manifest(entries_data, dest="out"): """Expected manifest lines from the spec, in archive order. entries_data: list of (name, data, typeflag_byte).""" lines = [] for name, data, tcode in entries_data: if tcode not in (ord("0"), 0): - lines.append(f"SKIP\t{name}\t{tcode}") + lines.append(f"SKIP\t{escape_name(name)}\t{tcode}") continue rel = spec_gate(name) if rel is None: - lines.append(f"REJECT\t{name}") + lines.append(f"REJECT\t{escape_name(name)}") else: - joined = "/".join(["out"] + rel) - lines.append(f"OK\t{joined}\t{len(data)}\t{sum(data)}") + lines.append(f"OK\t{under(dest, '/'.join(rel))}\t{len(data)}\t{sum(data)}") return lines +def output_lines(stdout): + """The lines a command printed: split on LF only, as the format is. + Output that does not end in LF gives a line that matches nothing.""" + if stdout and not stdout.endswith("\n"): + return stdout.split("\n") + ["(no LF at the end)"] + return stdout.split("\n")[:-1] if stdout else [] + + +def list_rows(stdout): + """(name, size, typeflag) for each line `list` printed, or a row + that matches nothing when a line has not three fields.""" + rows = [] + for line in output_lines(stdout): + parts = line.split("\t") + try: + rows.append((parts[0], int(parts[1]), int(parts[2])) if len(parts) == 3 else (line,)) + except ValueError: + rows.append((line,)) + return rows + + def main(): - if not EXE.exists(): - subprocess.run(["lake", "build"], cwd=PILOT_DIR, check=True) + # 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) + if build.returncode != 0: + print(build.stdout + build.stderr) + sys.exit("lake build failed") with tempfile.TemporaryDirectory() as td: td = Path(td) @@ -140,15 +213,13 @@ def main(): # 1. list: Lean agrees with tarfile on name, size, typeflag. r = run_lean("list", str(archive_a)) check("list-exit", r.returncode == 0, r.stderr) - lean_list = [] - for line in r.stdout.splitlines(): - parts = line.split("\t") - lean_list.append((parts[0], int(parts[1]), int(parts[2]))) + lean_list = [row for row in list_rows(r.stdout)] # tarfile strips the trailing slash from directory names when # reading; the raw header keeps it. Normalize both sides. - norm = lambda nl: [(n.rstrip("/") if t == 53 else n, s, t) for (n, s, t) in nl] + norm = lambda nl: [(n[0].rstrip("/"),) + tuple(n[1:]) if len(n) == 3 and n[2] == 53 else n + for n in nl] lean_list, ref_list = norm(lean_list), norm( - [(n, len(d), t) for (n, d, t) in ref_entries]) + [(escape_name(n), len(d), t) for (n, d, t) in ref_entries]) check("list-match", lean_list == ref_list, f"lean={lean_list} ref={ref_list}") @@ -156,12 +227,25 @@ def main(): r = run_lean("manifest", str(archive_a), "out") check("manifest-exit", r.returncode == 0, r.stderr) norm_skip = lambda ls: [ - "\t".join([p[0], p[1].rstrip("/")] + p[2:]) if l.startswith("SKIP") + "\t".join([p[0], p[1].rstrip("/")] + p[2:]) if l.startswith("SKIP") and len(p) > 1 else l for l in ls for p in [l.split("\t")]] - lean_manifest = norm_skip(r.stdout.splitlines()) + lean_manifest = norm_skip(output_lines(r.stdout)) exp_manifest = norm_skip(expected_manifest(ref_entries)) check("manifest-match", lean_manifest == exp_manifest, f"lean={lean_manifest} expected={exp_manifest}") + + # 2b. Other destinations: the printed path is the destination as + # given, then the entry's components, with no doubled `/`. + for dest in ["out/", "/", "", "/srv/data", "a//b", "../up", "./o"]: + r = run_lean("manifest", str(archive_a), dest) + check(f"manifest-dest {dest!r}", + r.returncode == 0 and + norm_skip(output_lines(r.stdout)) == norm_skip(expected_manifest(ref_entries, dest)), + f"rc={r.returncode} lean={output_lines(r.stdout)[:3]}") + for dest in ["out\nOK", "o\tut", "o\x7f", "o\u2028ut", "o\ufffdut"]: + r = run_lean("manifest", str(archive_a), dest) + check(f"manifest-dest-refused {dest!r}", r.returncode == 2 and r.stdout == "", + f"rc={r.returncode} out={r.stdout[:100]!r}") ok_count = sum(1 for l in exp_manifest if l.startswith("OK")) rej_count = sum(1 for l in exp_manifest if l.startswith("REJECT")) skip_count = sum(1 for l in exp_manifest if l.startswith("SKIP")) @@ -193,8 +277,8 @@ def main(): for rel, data in files.items(): joined = "/".join(["out"] + spec_gate(rel)) exp2.append(f"OK\t{joined}\t{len(data)}\t{sum(data)}") - check("self-manifest", r2.stdout.splitlines() == exp2, - f"lean={r2.stdout.splitlines()} expected={exp2}") + check("self-manifest", output_lines(r2.stdout) == exp2, + f"lean={output_lines(r2.stdout)} expected={exp2}") # 5. Hostile and broken input must fail cleanly, not crash. raw = archive_a.read_bytes() @@ -213,17 +297,26 @@ def main(): r = run_lean("list", str(badsum)) check("bad-checksum-fails", r.returncode == 1, f"rc={r.returncode}") - # 6. Axiom check: only the three standard axioms. + # 6. 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]) - for thm in ["gate_sound", "cleanComponents_sound", "extractAll_safe", - "extractArchive_safe"]: - check(f"axioms-{thm}", thm in ax_out, ax_out[:400]) - bad_axioms = [w for w in ["sorryAx"] if w in ax_out] - check("axioms-no-sorry", not bad_axioms, 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() @@ -233,7 +326,7 @@ def main(): f"Run by `tests/run_tests.py` against Python's `tarfile` module.", f"Lean: {lean_ver}. Python: {sys.version.split()[0]}.", "", - f"- Checks run: {checks}", + f"- Checks run: {checks} ({axiom_checks} of them on the axioms of the theorems)", f"- Failures: {len(failures)}", f"- Archive A entries compared (list and manifest): {len(ref_entries)}", f"- Manifest outcome on archive A: {ok_count} extracted, " From 1e72bb44974af40ab63fcca924a4501c27a11ecc Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 13:37:41 +0000 Subject: [PATCH 2/7] Check escape_noSpecial by name, and a destination that is not UTF-8 The page lists Spec.escape_noSpecial among the theorems and says the test script fails if the list it checks is not exactly that list. But TarPilot/Verify.lean did not print its axioms. A sorry in it was caught only because manifest_lines uses it: in a copy, the run gave 34 of 35, with only manifest_lines failing. Verify.lean now prints it, and the test script expects it. The tests refused a destination with a typed U+FFFD, but never one given as bytes that are not UTF-8, the case the page names. They now pass b"o\xffut" as well. The generated main makes each argument with lean_mk_string(argv[i]) (.lake/build/ir/Main.c), which puts U+FFFD in place of such bytes, so both reach runManifest as the same string. The page says a typed U+FFFD is refused too, and why. 37 checks, 14 of them on the axioms, 0 failures. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 4 ++-- TarPilot/Verify.lean | 1 + tests/TEST-RESULTS.md | 3 ++- tests/run_tests.py | 15 +++++++++------ 4 files changed, 14 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index 1e41ac4..99afe26 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,7 @@ 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, 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). A U+FFFD typed as such is refused too: by the time the tool reads its arguments, it cannot tell one from the other. ## What is proved @@ -43,7 +43,7 @@ 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`: 37 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; and broken inputs (truncated, garbage, bad checksum). - 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. diff --git a/TarPilot/Verify.lean b/TarPilot/Verify.lean index aeac8bf..a86b624 100644 --- a/TarPilot/Verify.lean +++ b/TarPilot/Verify.lean @@ -18,3 +18,4 @@ import Proofs #print axioms TarPilot.extractAll_resolves_inside #print axioms TarPilot.extractArchive_eq #print axioms TarPilot.extractArchive_resolves_inside +#print axioms Spec.escape_noSpecial diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 514b31f..0a22413 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -3,7 +3,7 @@ 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: 37 (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 @@ -24,4 +24,5 @@ Axiom check (`TarPilot/Verify.lean`): '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] +'Spec.escape_noSpecial' depends on axioms: [propext, Classical.choice, Quot.sound] ``` diff --git a/tests/run_tests.py b/tests/run_tests.py index 74400bd..8a0b164 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -26,10 +26,11 @@ 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"] +THEOREMS = ["TarPilot." + t for t in [ + "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"]] + ["Spec.escape_noSpecial"] checks = 0 failures = [] @@ -242,7 +243,9 @@ def main(): r.returncode == 0 and norm_skip(output_lines(r.stdout)) == norm_skip(expected_manifest(ref_entries, dest)), f"rc={r.returncode} lean={output_lines(r.stdout)[:3]}") - for dest in ["out\nOK", "o\tut", "o\x7f", "o\u2028ut", "o\ufffdut"]: + # The last is bytes that are not UTF-8, which the Lean runtime + # reads as U+FFFD before `main` runs. + for dest in ["out\nOK", "o\tut", "o\x7f", "o\u2028ut", "o\ufffdut", b"o\xffut"]: r = run_lean("manifest", str(archive_a), dest) check(f"manifest-dest-refused {dest!r}", r.returncode == 2 and r.stdout == "", f"rc={r.returncode} out={r.stdout[:100]!r}") @@ -310,7 +313,7 @@ def main(): 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} + expected = set(THEOREMS) check("axioms-names", set(records) == expected, f"printed {sorted(records)}, expected {sorted(expected)}") for name, used in sorted(records.items()): From 5daa2231e33a21f37d36c20d18d4c9fa8a9aa16e Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 13:57:28 +0000 Subject: [PATCH 3/7] tests: record the old and new tool comparison MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The PR reports a run over 3,000 random hostile archives under five destinations, but the script was in the session's scratch space, not here. tests/compare_old.py is that script, with the same seed (20261025), name parts, entry types and destinations (out, the empty string, /srv/x, a//b, ./o). It builds the tool at 7517a86 from git archive in a temporary directory and the tool in this checkout, and compares `manifest` on each pair. It also undoes 
 and 
, which the first script did not need to. tests/COMPARE-OLD.md is what it wrote: 15000 runs, 4200 differ as printed (a backslash in a name is now printed as two), 0 once the escapes are undone. That matches the session's run. The names hold no special character and no destination ends in `/`, so the run shows that nothing else changed. The changes the PR means to make are covered by the fixed cases in tests/run_tests.py. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 3 + tests/COMPARE-OLD.md | 19 +++++ tests/compare_old.py | 188 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 210 insertions(+) create mode 100644 tests/COMPARE-OLD.md create mode 100644 tests/compare_old.py diff --git a/README.md b/README.md index 99afe26..969dbca 100644 --- a/README.md +++ b/README.md @@ -60,6 +60,8 @@ 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`. + ## Layout - `TarPilot/Path.lean`: the path gate. @@ -71,3 +73,4 @@ The build fails if a proof breaks, though it accepts a `sorry` with only a warni - `TarPilot/Verify.lean`: the axiom check. - `Main.lean`: the command line front end. - `tests/run_tests.py`: differential tests against Python's `tarfile`. +- `tests/compare_old.py`: the old tool and the new one compared on random archives. diff --git a/tests/COMPARE-OLD.md b/tests/COMPARE-OLD.md new file mode 100644 index 0000000..b0e8d65 --- /dev/null +++ b/tests/COMPARE-OLD.md @@ -0,0 +1,19 @@ +# Old and new tool compared + +Written by `tests/compare_old.py`. Rerun it to check these numbers. + +- Old tool: commit 7517a86. New tool: this checkout. +- 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 +- Destinations: `out`, the empty string, `/srv/x`, `a//b`, `./o` +- `manifest` runs: 15000 +- Lines the new tool printed: 16360 OK, 11065 REJECT, 18195 SKIP +- Runs that differ as printed: 4200. The names hold no special character, so + the only escape the new tool can print in them is a backslash as two. +- Runs that differ, after the new escapes are undone: 0 + +The names hold no special character, and no destination ends in `/` or holds +a special character. So this run checks that nothing else changed. The +changes the PR means to make are covered by the fixed cases in +`tests/run_tests.py`. diff --git a/tests/compare_old.py b/tests/compare_old.py new file mode 100644 index 0000000..71aba4c --- /dev/null +++ b/tests/compare_old.py @@ -0,0 +1,188 @@ +#!/usr/bin/env python3 +"""Compare the tool with the tool before the containment change. + +The run the PR for audit F1 and F5 reports: 3,000 random hostile +archives under five destinations, with `manifest` from the old tool +(commit 7517a86, the base of that change) and from this checkout. The +new tool escapes names in REJECT and SKIP lines, so the script undoes +that escaping first: two backslashes give one, `\\xNN` gives that +character, and `\\u2028` and `\\u2029` give theirs. After that the two +outputs and exit codes must be the same. + +The names are drawn from plain parts, `..`, `.`, empty parts, a +backslash and non-ASCII letters, with a leading or trailing `/` at +times. They hold no special character, and no destination ends in `/` +or holds a special character. So the run checks that nothing else +changed. It does not cover the changes the PR means to make; the fixed +cases in `tests/run_tests.py` cover those. + +Run from anywhere (needs git, and the old commit in the history): + + python3 tests/compare_old.py [--seed N] [--count N] + +It builds both tools, writes `tests/COMPARE-OLD.md`, and exits non-zero +if any run differs. +""" + +import argparse +import io +import os +import platform +import random +import re +import subprocess +import sys +import tarfile +import tempfile +from pathlib import Path + +PILOT_DIR = Path(__file__).resolve().parent.parent +RESULTS = PILOT_DIR / "tests" / "COMPARE-OLD.md" +OLD = "7517a86" +DESTS = ["out", "", "/srv/x", "a//b", "./o"] +PARTS = ["a", "b", "..", ".", "", "x.txt", "é", "日本", "a b", "-", "~", "\\", "..a", "a..", + "...", ":"] +TYPES = [tarfile.REGTYPE, tarfile.REGTYPE, tarfile.AREGTYPE, tarfile.DIRTYPE, tarfile.SYMTYPE] + + +def build(where): + r = subprocess.run(["lake", "build", "tar-pilot"], cwd=where, capture_output=True, text=True) + if r.returncode != 0: + print(r.stdout + r.stderr) + sys.exit(f"lake build failed in {where}") + return Path(where) / ".lake" / "build" / "bin" / "tar-pilot" + + +def old_tool(td): + """Build the tool at commit OLD in a directory of its own. The + checkout is not changed.""" + src = Path(td) / "old" + src.mkdir() + r = subprocess.run(["git", "archive", "--format=tar", OLD], cwd=PILOT_DIR, + capture_output=True) + if r.returncode != 0: + sys.exit(f"git archive {OLD} failed: {r.stderr.decode()}") + with tarfile.open(fileobj=io.BytesIO(r.stdout)) as tf: + tf.extractall(src, filter="data") + return build(src) + + +def name(rng): + k = rng.randrange(1, 6) + s = "/".join(rng.choice(PARTS) for _ in range(k)) + if rng.random() < 0.2: + s = "/" + s + if rng.random() < 0.1: + s = s + "/" + return s + + +def write_archive(rng, path): + with tarfile.open(path, "w", format=tarfile.USTAR_FORMAT) as tf: + for _ in range(rng.randrange(1, 6)): + n = name(rng) + if len(n.encode()) > 100: + continue + ti = tarfile.TarInfo(n) + ti.mtime = 0 + ti.type = rng.choice(TYPES) + data = rng.randbytes(rng.randrange(0, 40)) \ + if ti.type in (tarfile.REGTYPE, tarfile.AREGTYPE) else b"" + ti.size = len(data) + try: + tf.addfile(ti, io.BytesIO(data)) + except Exception: + pass + + +ESCAPE = re.compile(rb"\\\\|\\x([0-9a-f]{2})|\\u(2028|2029)") + + +def unescape_char(m): + if m.group(0) == b"\\\\": + return b"\\" + if m.group(1): + return chr(int(m.group(1), 16)).encode() + return chr(int(m.group(2), 16)).encode() + + +def unescape(out): + """The new tool's output with the names in REJECT and SKIP lines + as the old tool printed them.""" + lines = [] + for line in out.split(b"\n"): + if line.startswith(b"REJECT\t") or line.startswith(b"SKIP\t"): + fields = line.split(b"\t") + fields[1] = ESCAPE.sub(unescape_char, fields[1]) + line = b"\t".join(fields) + lines.append(line) + return b"\n".join(lines) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--seed", type=int, default=20261025) + ap.add_argument("--count", type=int, default=3000, help="random archives") + args = ap.parse_args() + RESULTS.unlink(missing_ok=True) + + rng = random.Random(args.seed) + new = build(PILOT_DIR) + runs = 0 + raw = 0 + diffs = [] + lines = {"OK": 0, "REJECT": 0, "SKIP": 0} + with tempfile.TemporaryDirectory() as td: + old = old_tool(td) + path = os.path.join(td, "t.tar") + for _ in range(args.count): + write_archive(rng, path) + for dest in DESTS: + a = subprocess.run([old, "manifest", path, dest], capture_output=True) + b = subprocess.run([new, "manifest", path, dest], capture_output=True) + runs += 1 + for line in b.stdout.split(b"\n"): + kind = line.split(b"\t")[0].decode() + if kind in lines: + lines[kind] += 1 + raw += (a.returncode, a.stdout) != (b.returncode, b.stdout) + if (a.returncode, a.stdout) != (b.returncode, unescape(b.stdout)): + diffs.append((dest, a.stdout[:300], b.stdout[:300])) + + lean_ver = subprocess.run(["lean", "--version"], capture_output=True, + text=True).stdout.strip() + out = [ + "# Old and new tool compared", + "", + "Written by `tests/compare_old.py`. Rerun it to check these numbers.", + "", + f"- Old tool: commit {OLD}. New tool: this checkout.", + f"- Lean: {lean_ver}. Python: {platform.python_version()}.", + f"- Seed: {args.seed}", + f"- Random archives: {args.count}, written by Python's `tarfile` in ustar format", + "- Destinations: " + ", ".join(f"`{d}`" if d else "the empty string" for d in DESTS), + f"- `manifest` runs: {runs}", + f"- Lines the new tool printed: {lines['OK']} OK, {lines['REJECT']} REJECT, " + f"{lines['SKIP']} SKIP", + f"- Runs that differ as printed: {raw}. The names hold no special character, so", + " the only escape the new tool can print in them is a backslash as two.", + f"- Runs that differ, after the new escapes are undone: {len(diffs)}", + "", + "The names hold no special character, and no destination ends in `/` or holds", + "a special character. So this run checks that nothing else changed. The", + "changes the PR means to make are covered by the fixed cases in", + "`tests/run_tests.py`.", + "", + ] + if diffs: + out += ["## Differences", ""] + for dest, a, b in diffs[:20]: + out += [f"- destination {dest!r}: old {a!r}, new {b!r}"] + out += [""] + RESULTS.write_text("\n".join(out)) + print(f"{runs} manifest runs, {len(diffs)} differ; results in {RESULTS}") + return 1 if diffs else 0 + + +if __name__ == "__main__": + sys.exit(main()) From 2135996be6a109614841a8189f3477422ba51a17 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 14:00:27 +0000 Subject: [PATCH 4/7] tests: record the planted sorry, axiom and extra theorem The PR says a planted sorry, a planted axiom, and an extra unlisted theorem each fail the test script, but no file recorded those runs. tests/planted_bugs.py makes each change in a copy, word for word as in the session's run, runs lake build, then tests/run_tests.py. tests/PLANTED-BUGS.md is what it wrote: lake build passes on every one (with a warning for a sorry), and the test script fails on every one, on the axiom checks. The session's extra theorem was proved by sorry, so the sorry check caught it too. A second row proves it with `trivial`, and only the check on the names fails. Two rows follow from the reviews: a listed theorem left out of Verify.lean, and a sorry in Spec.escape_noSpecial. The mutations the review rounds built change the code and its proofs, so they are named in the record but not planted. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 3 + tests/PLANTED-BUGS.md | 128 ++++++++++++++++++++++++++++++ tests/planted_bugs.py | 177 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 308 insertions(+) create mode 100644 tests/PLANTED-BUGS.md create mode 100644 tests/planted_bugs.py diff --git a/README.md b/README.md index 969dbca..f4f6da1 100644 --- a/README.md +++ b/README.md @@ -62,6 +62,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/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 - `TarPilot/Path.lean`: the path gate. @@ -74,3 +76,4 @@ The build fails if a proof breaks, though it accepts a `sorry` with only a warni - `Main.lean`: the command line front end. - `tests/run_tests.py`: differential tests against Python's `tarfile`. - `tests/compare_old.py`: the old tool and the new one compared on random archives. +- `tests/planted_bugs.py`: faults planted in the proofs, which the axiom check must catch. diff --git a/tests/PLANTED-BUGS.md b/tests/PLANTED-BUGS.md new file mode 100644 index 0000000..23a4eb0 --- /dev/null +++ b/tests/PLANTED-BUGS.md @@ -0,0 +1,128 @@ +# 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 | + +## The changes + +**sorry in a helper lemma (resolve_plain)** in `Proofs/Contain.lean`: + +``` +- theorem resolve_plain : ∀ (rel acc : List String), (∀ c ∈ rel, PlainName c) → +- resolve acc rel = acc ++ rel := by +- intro rel +- induction rel with +- | nil => intro acc _; simp [resolve] +- | cons c cs ih => +- intro acc h +- have ⟨h1, h2, h3, _⟩ := h c (by simp) +- have hcs : ∀ x ∈ cs, PlainName x := fun x hx => h x (by simp [hx]) +- simp only [resolve, h1, h2, h3, or_self, ite_false] +- rw [ih _ hcs] +- simp ++ theorem resolve_plain : ∀ (rel acc : List String), (∀ c ∈ rel, PlainName c) → ++ resolve acc rel = acc ++ rel := by ++ exact sorry +``` + +**axiom cheat : False behind a helper lemma (resolve_plain)** in `Proofs/Contain.lean`: + +``` +- theorem resolve_plain : ∀ (rel acc : List String), (∀ c ∈ rel, PlainName c) → +- resolve acc rel = acc ++ rel := by +- intro rel +- induction rel with +- | nil => intro acc _; simp [resolve] +- | cons c cs ih => +- intro acc h +- have ⟨h1, h2, h3, _⟩ := h c (by simp) +- have hcs : ∀ x ∈ cs, PlainName x := fun x hx => h x (by simp [hx]) +- simp only [resolve, h1, h2, h3, or_self, ite_false] +- rw [ih _ hcs] +- simp ++ axiom cheat : False ++ ++ theorem resolve_plain : ∀ (rel acc : List String), (∀ c ∈ rel, PlainName c) → ++ resolve acc rel = acc ++ rel := by ++ exact cheat.elim +``` + +**extra unlisted theorem, proved by sorry** in `Proofs/Contain.lean`: + +``` +- (extractAll dest) := rfl +- +- end TarPilot ++ (extractAll dest) := rfl ++ ++ end TarPilot ++ ++ theorem TarPilot.extra_claim : TarPilot.gate ".." = none := sorry +``` + +**extra unlisted theorem, proved by sorry** in `TarPilot/Verify.lean`: + +``` +- #print axioms Spec.escape_noSpecial ++ #print axioms Spec.escape_noSpecial ++ #print axioms TarPilot.extra_claim +``` + +**extra unlisted theorem, proved** in `Proofs/Contain.lean`: + +``` +- (extractAll dest) := rfl +- +- end TarPilot ++ (extractAll dest) := rfl ++ ++ end TarPilot ++ ++ theorem TarPilot.extra_claim : True := trivial +``` + +**extra unlisted theorem, proved** in `TarPilot/Verify.lean`: + +``` +- #print axioms Spec.escape_noSpecial ++ #print axioms Spec.escape_noSpecial ++ #print axioms TarPilot.extra_claim +``` + +**listed theorem left out of Verify.lean (manifest_lines)** in `TarPilot/Verify.lean`: + +``` +- #print axioms TarPilot.manifest_lines ++ +``` + +**sorry in Spec.escape_noSpecial** in `Spec/Defs.lean`: + +``` +- ∀ 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 ++ ∀ ch ∈ (escape s).toList, isSpecial ch = false := by ++ sorry +``` + +## Not here + +The PR also says that each mutation the two review rounds built now breaks a +statement. Those mutations change the code, and the reviewers changed its +proofs with it to show a statement was too weak. They are not faults the +tests are meant to catch, so they are not planted here. diff --git a/tests/planted_bugs.py b/tests/planted_bugs.py new file mode 100644 index 0000000..71e8f3a --- /dev/null +++ b/tests/planted_bugs.py @@ -0,0 +1,177 @@ +#!/usr/bin/env python3 +"""Plant each fault below in a copy of the project, and check the tests catch it. + +The faults here are the ones 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 follow from the reviews: a listed theorem left out +of the check, and a `sorry` in `Spec.escape_noSpecial`. None of them +stops `lake build`: Lean accepts a `sorry` with +a warning, and an axiom or an extra theorem with none. What catches +them is the axiom check in `tests/run_tests.py`, which reads what +`TarPilot/Verify.lean` prints. Each row is caught when that script +reports failures. + +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. The project itself is never changed. The script writes +the results to tests/PLANTED-BUGS.md, and exits with 1 if a fault is +not caught and is not marked as equivalent. + +Usage: python3 tests/planted_bugs.py +""" + +import re +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent + +RESOLVE_PLAIN = """theorem resolve_plain : ∀ (rel acc : List String), (∀ c ∈ rel, PlainName c) → + resolve acc rel = acc ++ rel := by + intro rel + induction rel with + | nil => intro acc _; simp [resolve] + | cons c cs ih => + intro acc h + have ⟨h1, h2, h3, _⟩ := h c (by simp) + have hcs : ∀ x ∈ cs, PlainName x := fun x hx => h x (by simp [hx]) + simp only [resolve, h1, h2, h3, or_self, ite_false] + rw [ih _ hcs] + simp +""" +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 + 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""" + +CONTAIN_END = "(extractAll dest) := rfl\n\nend TarPilot\n" +VERIFY_END = "#print axioms Spec.escape_noSpecial\n" + +# (name, [(file, text to replace, replacement)], why it is equivalent or None) +BUGS = [ + # The changes of the session's run, word for word: a helper lemma + # that every containment theorem uses, proved by `sorry` or by an axiom. + ("sorry in a helper lemma (resolve_plain)", + [("Proofs/Contain.lean", RESOLVE_PLAIN, RESOLVE_PLAIN_STMT + ":= by\n exact sorry\n")], + None), + ("axiom cheat : False behind a helper lemma (resolve_plain)", + [("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 session's run proved it by `sorry`; the second row 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")], + 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")], + None), + # Not named by the PR. The second review round left a listed theorem + # out of Verify.lean; review question 2 asks about escape_noSpecial. + ("listed theorem left out of Verify.lean (manifest_lines)", + [("TarPilot/Verify.lean", "#print axioms TarPilot.manifest_lines\n", "")], + None), + ("sorry in Spec.escape_noSpecial", + [("Spec/Defs.lean", ESCAPE_PROOF, + " ∀ ch ∈ (escape s).toList, isSpecial ch = false := by\n sorry")], + None), +] + + +def failures(out): + """The failures the test script reports, or None if it did not + finish (for example, if the build failed).""" + m = re.search(r"(\d+)/(\d+) checks passed", out) + return int(m.group(2)) - int(m.group(1)) if m else None + + +def run(): + rows = [] + with tempfile.TemporaryDirectory() as tmp: + work = Path(tmp) / "project" + shutil.copytree(ROOT, work, ignore=shutil.ignore_patterns(".git")) + for name, edits, equivalent in BUGS: + originals = {} + for rel, old, new in edits: + path = work / rel + 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"], + cwd=work, capture_output=True, text=True) + for rel, text in originals.items(): + (work / rel).write_text(text) + n = failures(test.stdout + test.stderr) + 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 + + +def write(rows): + 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.", + "", + "| 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 "") + if n is None: + cell = "the tests did not finish" + 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)} |") + lines += ["", "## The changes", ""] + 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+ "), "```", ""] + lines += [ + "## Not here", + "", + "The PR also says that each mutation the two review rounds built now breaks a", + "statement. Those mutations change the code, and the reviewers changed its", + "proofs with it to show a statement was too weak. They are not faults the", + "tests are meant to catch, so they are not planted here.", + "", + ] + (ROOT / "tests" / "PLANTED-BUGS.md").write_text("\n".join(lines)) + + +def main(): + 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") + if missed: + sys.exit("not caught: " + ", ".join(missed)) + + +if __name__ == "__main__": + main() From c6154fa283c16c123f6ba63ebaa34820b3fd44c6 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 14:02:00 +0000 Subject: [PATCH 5/7] Say what the parser does now with GNU, pax and invalid UTF-8 names The page said an archive with GNU or pax extensions fails to parse, and that a name that is not valid UTF-8 is rejected. On this branch neither holds (audit F2, F3), and the PR left the sentence for #5, which changes the parser. A reader of this branch alone read it as true. The audit's probe script, run against this branch's tool, still prints what the audit found: a GNU long name cut to 100 bytes, a pax path ignored, and a split name with one invalid field extracted under another name. The page now says that. A base-256 size field does fail to parse, which a hand-made header confirms, and the page keeps that. 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 f4f6da1..570aa98 100644 --- a/README.md +++ b/README.md @@ -47,7 +47,7 @@ Read this before trusting the pilot with real archives: - 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. GNU tar extensions (long name entries, pax headers), base-256 size fields, and sparse files are not supported. A base-256 size field fails to parse, but an archive with a GNU long name or a pax header is not refused, as the bar audit's probes show (findings F2 and F3). Such a header is skipped as a non-regular entry, so the file after it is read under the name in its own ustar header: a long name is cut to 100 bytes, and a pax path is ignored. A name or prefix field that is not valid UTF-8 reads as empty. So a short name like that is rejected, but a name split over both fields, with one field invalid, is extracted under another name. In every probe the path stays inside the destination, since the gate still runs. - The Lean compiler, runtime, and kernel are trusted, as in every Lean project. A bug in them is outside the proof. ## Re-check it From 8fa75117cf2971cb2a3ec8ff08f905fe30a0c577 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 14:08:34 +0000 Subject: [PATCH 6/7] tests: let compare_old.py build the new tool from a commit On the branch above this one, the parser rejects archives it cannot read, so the comparison with the checkout differs there on purpose: a trial merge into claude/reject-unsupported gave 675 of 3000 runs that differ, on 600 archives. `--new 1273382` builds the new tool from the containment change itself, so the PR's run can be rerun on any later branch. On this branch it gives the same result as the checkout: 1000 of 1000 runs agree on 200 archives. The default is still the checkout, and the record is unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- tests/compare_old.py | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/tests/compare_old.py b/tests/compare_old.py index 71aba4c..a419e5e 100644 --- a/tests/compare_old.py +++ b/tests/compare_old.py @@ -18,7 +18,13 @@ Run from anywhere (needs git, and the old commit in the history): - python3 tests/compare_old.py [--seed N] [--count N] + python3 tests/compare_old.py [--seed N] [--count N] [--new REV] + +With `--new REV`, the new tool is built from commit REV instead of this +checkout. The PR's run compared 7517a86 with its own commit, 1273382, +whose tool is the one in this checkout. A later change to the parser +changes the output on purpose, so on a later branch pass +`--new 1273382` to rerun the PR's run. It builds both tools, writes `tests/COMPARE-OLD.md`, and exits non-zero if any run differs. @@ -53,15 +59,15 @@ def build(where): return Path(where) / ".lake" / "build" / "bin" / "tar-pilot" -def old_tool(td): - """Build the tool at commit OLD in a directory of its own. The +def tool_at(rev, td): + """Build the tool at commit `rev` in a directory of its own. The checkout is not changed.""" - src = Path(td) / "old" + src = Path(td) / rev src.mkdir() - r = subprocess.run(["git", "archive", "--format=tar", OLD], cwd=PILOT_DIR, + r = subprocess.run(["git", "archive", "--format=tar", rev], cwd=PILOT_DIR, capture_output=True) if r.returncode != 0: - sys.exit(f"git archive {OLD} failed: {r.stderr.decode()}") + 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") return build(src) @@ -123,17 +129,18 @@ def main(): ap = argparse.ArgumentParser() ap.add_argument("--seed", type=int, default=20261025) ap.add_argument("--count", type=int, default=3000, help="random archives") + ap.add_argument("--new", help="build the new tool from this commit, not the checkout") args = ap.parse_args() RESULTS.unlink(missing_ok=True) rng = random.Random(args.seed) - new = build(PILOT_DIR) runs = 0 raw = 0 diffs = [] lines = {"OK": 0, "REJECT": 0, "SKIP": 0} with tempfile.TemporaryDirectory() as td: - old = old_tool(td) + old = tool_at(OLD, td) + new = tool_at(args.new, td) if args.new else build(PILOT_DIR) path = os.path.join(td, "t.tar") for _ in range(args.count): write_archive(rng, path) @@ -156,7 +163,8 @@ def main(): "", "Written by `tests/compare_old.py`. Rerun it to check these numbers.", "", - f"- Old tool: commit {OLD}. New tool: this checkout.", + f"- Old tool: commit {OLD}. New tool: " + + (f"commit {args.new}." if args.new else "this checkout."), f"- Lean: {lean_ver}. Python: {platform.python_version()}.", f"- Seed: {args.seed}", f"- Random archives: {args.count}, written by Python's `tarfile` in ustar format", From 85ef13ad66e682b13662ff63506e5987c83ab220 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 19:24:01 +0000 Subject: [PATCH 7/7] tests: stop on a run with no check count, and say what the proofs catch planted_bugs.py counted a test run that printed no check count as a row that "did not finish" and went on, so a fault whose copy did not build was reported as not caught. It now stops with an error and writes no record, as it does when the count does not match the exit status of the test script. It deletes the old record first. Its docstring now says what the proofs catch and what they do not. A change to the code under proof that alters an answer a statement fixes stops lake build. A fault in the proofs or in the list of theorems checked does not, which is every fault here, and neither does a change to header parsing, archive writing, list or Main.lean. A comment said every containment theorem uses resolve_plain. Only extractAll_resolves_inside and extractArchive_resolves_inside do, which is why each plant there fails two checks. The comments and the record no longer rest on the session's own runs, which a reader cannot see. The same holds for compare_old.py, which said the PR's run compared 7517a86 with 1273382. Rerun: planted_bugs.py, 6 of 6 caught, the same table. compare_old.py, 15000 runs, 0 differ, the record unchanged. run_tests.py, 37/37. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- tests/PLANTED-BUGS.md | 8 ++--- tests/compare_old.py | 8 ++--- tests/planted_bugs.py | 74 +++++++++++++++++++++++++++---------------- 3 files changed, 54 insertions(+), 36 deletions(-) diff --git a/tests/PLANTED-BUGS.md b/tests/PLANTED-BUGS.md index 23a4eb0..f764a8c 100644 --- a/tests/PLANTED-BUGS.md +++ b/tests/PLANTED-BUGS.md @@ -122,7 +122,7 @@ proofs or to the axiom check, made in a copy. `lake build` ran on the copy, then ## Not here -The PR also says that each mutation the two review rounds built now breaks a -statement. Those mutations change the code, and the reviewers changed its -proofs with it to show a statement was too weak. They are not faults the -tests are meant to catch, so they are not planted here. +The review rounds the PR describes also built changes to the code under proof. +A change that alters an answer a statement fixes stops `lake build`, so it is +for the proofs to catch, not for these checks. Those changes were not kept in +the repo, so they are not planted here, and this record says nothing about them. diff --git a/tests/compare_old.py b/tests/compare_old.py index a419e5e..5240447 100644 --- a/tests/compare_old.py +++ b/tests/compare_old.py @@ -21,10 +21,10 @@ python3 tests/compare_old.py [--seed N] [--count N] [--new REV] With `--new REV`, the new tool is built from commit REV instead of this -checkout. The PR's run compared 7517a86 with its own commit, 1273382, -whose tool is the one in this checkout. A later change to the parser -changes the output on purpose, so on a later branch pass -`--new 1273382` to rerun the PR's run. +checkout. The comparison is about the tool at 1273382, the commit of +the containment change. A later change to the parser changes the +output on purpose, so on a later branch pass `--new 1273382` to rerun +it. It builds both tools, writes `tests/COMPARE-OLD.md`, and exits non-zero if any run differs. diff --git a/tests/planted_bugs.py b/tests/planted_bugs.py index 71e8f3a..6d6d5ac 100644 --- a/tests/planted_bugs.py +++ b/tests/planted_bugs.py @@ -1,22 +1,33 @@ #!/usr/bin/env python3 """Plant each fault below in a copy of the project, and check the tests catch it. -The faults here are the ones the PR for audit F1 and F5 names: a +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 follow from the reviews: a listed theorem left out -of the check, and a `sorry` in `Spec.escape_noSpecial`. None of them -stops `lake build`: Lean accepts a `sorry` with -a warning, and an axiom or an extra theorem with none. What catches -them is the axiom check in `tests/run_tests.py`, which reads what -`TarPilot/Verify.lean` prints. Each row is caught when that script -reports failures. +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. + +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. 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. The project itself is never changed. The script writes -the results to tests/PLANTED-BUGS.md, and exits with 1 if a fault is -not caught and is not marked as equivalent. +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 """ @@ -59,8 +70,9 @@ # (name, [(file, text to replace, replacement)], why it is equivalent or None) BUGS = [ - # The changes of the session's run, word for word: a helper lemma - # that every containment theorem uses, proved by `sorry` or by an axiom. + # 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. ("sorry in a helper lemma (resolve_plain)", [("Proofs/Contain.lean", RESOLVE_PLAIN, RESOLVE_PLAIN_STMT + ":= by\n exact sorry\n")], None), @@ -69,8 +81,8 @@ "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 session's run proved it by `sorry`; the second row proves - # it without one, so only the check on the names can catch it. + # 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"), @@ -81,8 +93,9 @@ CONTAIN_END + "\ntheorem TarPilot.extra_claim : True := trivial\n"), ("TarPilot/Verify.lean", VERIFY_END, VERIFY_END + "#print axioms TarPilot.extra_claim\n")], None), - # Not named by the PR. The second review round left a listed theorem - # out of Verify.lean; review question 2 asks about escape_noSpecial. + # 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", "")], None), @@ -94,8 +107,8 @@ def failures(out): - """The failures the test script reports, or None if it did not - finish (for example, if the build failed).""" + """The failures the test script reports, or None if it gave no + check count (for example, if the build failed).""" m = re.search(r"(\d+)/(\d+) checks passed", out) return int(m.group(2)) - int(m.group(1)) if m else None @@ -120,7 +133,13 @@ def run(): cwd=work, capture_output=True, text=True) for rel, text in originals.items(): (work / rel).write_text(text) - n = failures(test.stdout + test.stderr) + out = test.stdout + test.stderr + n = failures(out) + if n is None: + sys.exit(f"{name}: the tests gave no check count\n{out[-2000:]}") + 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) @@ -141,10 +160,7 @@ def write(rows): 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 "") - if n is None: - cell = "the tests did not finish" - else: - cell = str(n) if n else ("0, equivalent: " + equivalent if equivalent else "0, NOT CAUGHT") + cell = str(n) if n else ("0, equivalent: " + equivalent if equivalent else "0, NOT CAUGHT") lines.append(f"| {name} | {files} | {build} | {cell} | {', '.join(fails)} |") lines += ["", "## The changes", ""] for name, edits, _, _, _, _, _ in rows: @@ -154,16 +170,18 @@ def write(rows): lines += [ "## Not here", "", - "The PR also says that each mutation the two review rounds built now breaks a", - "statement. Those mutations change the code, and the reviewers changed its", - "proofs with it to show a statement was too weak. They are not faults the", - "tests are meant to catch, so they are not planted here.", + "The review rounds the PR describes also built changes to the code under proof.", + "A change that alters an answer a statement fixes stops `lake build`, so it is", + "for the proofs to catch, not for these checks. Those changes were not kept in", + "the repo, so they are not planted here, and this record says nothing about them.", "", ] (ROOT / "tests" / "PLANTED-BUGS.md").write_text("\n".join(lines)) def main(): + # 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]]