Prove joined-path containment and share extraction with the CLI

Main.lean

@@ -43,14 +43,12 @@ def runManifest (file dest : String) : IO UInt32 := do
   | 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}"
+      match extractEntry destCs e with
+      | some (path, bytes) =>
+        IO.println s!"OK\t{joinPath path}\t{bytes.size}\t{byteSum bytes}"
+      | none =>
+        if isRegular e then IO.println s!"REJECT\t{e.name}"
+        else IO.println s!"SKIP\t{e.name}\t{e.typeflag.toNat}"
     return 0
 
 def runCreate (out : String) (files : List String) : IO UInt32 := do

README.md

@@ -1,6 +1,6 @@
 # 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 built by joining the destination with a cleaned relative path. A machine-checked proof covers the joined string: resolving a relative POSIX path lexically, without symlinks, leaves it inside the resolved destination. This tool writes no extracted files to disk.
 
 It is the first Proven Commons project. The org's home repo, [mission](https://github.com/Proven-Commons/mission), publishes the verified bar it is measured against. Status: built, not yet verified. The [bar audit of 2026-10-24](https://github.com/Proven-Commons/mission/blob/main/reviews/tar/2026-10-24-bar-audit.md) found that the bar is not yet met, and lists the fixes.
 
@@ -21,23 +21,26 @@ lake build
 
 The path gate and the extraction rule, in `TarPilot/Path.lean` and `TarPilot/Archive.lean`:
 
-- `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.
+- `cleanComponents_plain` and `gate_plain`: accepted components are plain names, with no empty name, `.`, `..`, embedded `/`, or NUL. The gate also requires a nonempty result. The original `cleanComponents_sound` and `gate_sound` guarantees remain available.
+- `extractEntry_contained` and `extractAll_contained`: every accepted path is the destination components followed by a nonempty list of plain names.
+- `extractAll_joined`: rendering those components with `joinPath` and splitting the string on `/` recovers the destination followed by the plain names. This assumes the destination components themselves contain no `/`, as when the CLI splits its destination argument.
+- `extractAll_resolves_inside` and `extractEntry_resolves_inside`: resolving that rendered string with the relative POSIX lexical resolver in `Path.lean` gives the resolved destination followed by the plain names, under the same destination assumption. Archive names cannot add a parent traversal above the destination. The resolver preserves leading `..`; it does not model absolute-root handling, Windows paths, or symlinks.
+- `extractAll_safe` and `extractArchive_safe`: the original component-list guarantee, including extraction from archive bytes.
 
-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.
+The CLI's `OK` lines call `extractEntry` and `joinPath`, the same functions used by these statements. `extractAll` filters the results of `extractEntry`. The CLI adds only `REJECT` and `SKIP` diagnostics for entries with no extracted result, preserving archive order. Parsing, diagnostics, and formatting sizes and byte sums remain outside the proof.
+
+The gate rules: absolute names are rejected. Any `..` component is rejected, as is a component containing `/` or NUL. 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.
 
 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`.
 
 ## 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).
+- 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`: the original 14 archive entries and create/readback checks, plus 524 path cases (512 random, seed `20261024`) under eight destinations. Manifest comparisons preserve duplicate names and entry order; `posixpath` independently checks containment of emitted paths. Lean regressions cover embedded separators, NUL, the old theorem's traversal counterexample, and lexical resolution. Broken inputs cover truncated archives, garbage, and bad checksums.
 - 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.
-- 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.
+- Invalid UTF-8 becomes an empty header field. With a split ustar name, a valid prefix or name can survive while the invalid field is lost. GNU longname and pax path overrides are ignored rather than reliably rejected, so extension-bearing archives can produce incorrect names. Base-256 sizes and sparse files are not supported. Typeflag `7` (contiguous file) is skipped even though Python treats it as regular. These parser and compatibility findings from the audit remain open; use the pilot only for its supported ustar subset.
+- The Lean compiler, runtime, kernel, and hardware are trusted. The tests also rely on Python's `tarfile` and `posixpath` as oracles. Bugs in these are outside the proof.
 
 ## Re-check it
 
@@ -47,7 +50,7 @@ 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 checks the proofs, but accepts `sorry` with a warning. The second command prints the axiom list. The test script always rebuilds, runs the Lean regressions and every comparison, and rewrites `tests/TEST-RESULTS.md`. It requires each named theorem's axiom list to contain only `propext`, `Classical.choice`, and `Quot.sound`, so `sorryAx` and custom axioms fail the tests.
 
 ## Layout
 
@@ -58,3 +61,4 @@ The build fails if a proof breaks. The second command prints the axiom list. The
 - `TarPilot/Verify.lean`: the axiom check.
 - `Main.lean`: the command line front end.
 - `tests/run_tests.py`: differential tests against Python's `tarfile`.
+- `tests/PathSafety.lean`: path safety regressions, including the old statement's counterexample.

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`: the CLI and `extractAll` both call `extractEntry`.
+  Each emitted path is `dest ++ rel`, where `rel` is a nonempty list
+  of plain names. The containment theorems also cover joining the
+  components into a string and resolving that relative path lexically.
 
   Parsing and writing are covered by differential tests against
   Python's `tarfile` module (see `tests/`), not by a proof.
@@ -57,43 +57,96 @@ def parseArchive (data : ByteArray) : Option (List RawEntry) :=
 def isRegular (e : RawEntry) : Bool :=
   e.typeflag == '0' || e.typeflag == Char.ofNat 0
 
+/-- The extraction decision shared by the CLI and the in-memory model. -/
+def extractEntry (dest : List String) (e : RawEntry) : Option (List String × ByteArray) :=
+  if isRegular e then
+    (gate e.name).map fun rel => (dest ++ rel, e.data)
+  else none
+
+/-- An accepted entry extends the destination by nonempty plain names. -/
+theorem extractEntry_contained (dest : List String) (e : RawEntry)
+    (path : List String) (bytes : ByteArray)
+    (h : extractEntry dest e = some (path, bytes)) :
+    ∃ rel, rel ≠ [] ∧ path = dest ++ rel ∧ ∀ c ∈ rel, PlainName c := by
+  unfold extractEntry at h
+  split at h
+  · cases hg : gate e.name with
+    | none => simp [hg] at h
+    | some rel =>
+      simp only [hg, Option.map_some, Option.some.injEq, Prod.mk.injEq] at h
+      obtain ⟨hp, hne⟩ := gate_plain e.name rel hg
+      exact ⟨rel, hne, h.1.symm, hp⟩
+  · simp at h
+
 /-- Extract entries into a list of `(path, data)` pairs, in memory.
     The path of each pair is the destination components followed by the
     gated relative components of the entry name. -/
 def extractAll (dest : List String) (entries : List RawEntry) :
     List (List String × ByteArray) :=
-  entries.filterMap fun e =>
-    if isRegular e then
-      (gate e.name).map fun rel => (dest ++ rel, e.data)
-    else none
+  entries.filterMap (extractEntry dest)
+
+/-- Every emitted relative path is nonempty and contains only plain names,
+    including the absence of embedded separators and NUL. -/
+theorem extractAll_contained (dest : List String) (entries : List RawEntry)
+    (path : List String) (bytes : ByteArray)
+    (h : (path, bytes) ∈ extractAll dest entries) :
+    ∃ rel, rel ≠ [] ∧ path = dest ++ rel ∧ ∀ c ∈ rel, PlainName c := by
+  obtain ⟨e, _, he⟩ := List.mem_filterMap.mp h
+  exact extractEntry_contained dest e path bytes he
 
 /-- 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. -/
+    relative path is not empty. This is the original component-list
+    guarantee; see `extractAll_resolves_inside` for the joined string. -/
 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)
+  obtain ⟨rel, hne, heq, hp⟩ := extractAll_contained dest entries path bytes h
+  exact ⟨rel, heq, fun hm => (hp _ hm).2.2.1 rfl,
+    fun hm => (hp _ hm).1 rfl, fun hm => (hp _ hm).2.1 rfl, hne⟩
+
+/-- Rendering a path and splitting it again preserves the destination
+    and plain relative names. Destination components must be slash-free. -/
+theorem extractAll_joined (dest : List String) (entries : List RawEntry)
+    (path : List String) (bytes : ByteArray)
+    (hdest : ∀ d ∈ dest, '/' ∉ d.toList)
+    (h : (path, bytes) ∈ extractAll dest entries) :
+    ∃ rel, rel ≠ [] ∧ (∀ c ∈ rel, PlainName c) ∧
+      pathComponents (joinPath path) = dest ++ rel := by
+  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 (hplain s hs).2.2.2.1
+  · simp [hne]
+
+/-- The rendered path resolves to the resolved destination followed by
+    plain names. This is lexical containment of a relative POSIX path,
+    without symlinks; it is not a theorem about filesystem writes. -/
+theorem extractAll_resolves_inside (dest : List String) (entries : List RawEntry)
+    (path : List String) (bytes : ByteArray)
+    (hdest : ∀ d ∈ dest, '/' ∉ d.toList)
+    (h : (path, bytes) ∈ extractAll dest entries) :
+    ∃ rel, rel ≠ [] ∧ (∀ c ∈ rel, PlainName c) ∧
+      resolve [] (pathComponents (joinPath path)) = resolve [] dest ++ rel := by
+  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 joined-string guarantee for the decision the CLI calls. -/
+theorem extractEntry_resolves_inside (dest : List String) (e : RawEntry)
+    (path : List String) (bytes : ByteArray)
+    (hdest : ∀ d ∈ dest, '/' ∉ d.toList)
+    (h : extractEntry dest e = some (path, bytes)) :
+    ∃ rel, rel ≠ [] ∧ (∀ c ∈ rel, PlainName c) ∧
+      resolve [] (pathComponents (joinPath path)) = resolve [] dest ++ rel := by
+  apply extractAll_resolves_inside dest [e] path bytes hdest
+  exact List.mem_filterMap.mpr ⟨e, by simp, h⟩
 
 /-- Parse, then extract. -/
 def extractArchive (dest : List String) (data : ByteArray) :