Reject what the pilot cannot read, extract contiguous files (audit F2-F4)

Proofs/Contain.lean

@@ -318,7 +318,7 @@ theorem gate_plain (name : String) (rel : List String) :
     is rejected; anything else is skipped. -/
 theorem manifest_eq (dest : List String) (entries : List RawEntry) :
     manifest dest entries = entries.map fun e =>
-      if regularType e.typeflag then
+      if regularType e.typeflag e.name then
         match cleanName e.name with
         | some rel => .extract (dest ++ rel) e.data
         | none => .reject e.name
@@ -514,7 +514,7 @@ theorem manifest_lines_eq (dest : String) (entries : List RawEntry) :
   funext e
   simp only [Function.comp_apply]
   unfold outcome Spec.line
-  have hreg : isRegular e = regularType e.typeflag := rfl
+  have hreg : isRegular e = regularType e.typeflag e.name := rfl
   rw [hreg, gate_eq]
   split
   · split

README.md

@@ -21,7 +21,7 @@ lake build
 
 The theorems are in `Proofs/Contain.lean`, about the code in `TarPilot/Path.lean` and `TarPilot/Archive.lean`. Their statements use the definitions in `Spec/Defs.lean`: a special character (a control character, C0, DEL, or C1, or the Unicode line or paragraph separator), a plain name (not empty, `.` or `..`, and free of `/` and special characters), the components of a path string (the parts between `/`), the gate's rules, the regular typeflags, a path under a destination, how a name is printed, the exact line printed for an entry, and lexical resolution of a relative path. They are about the code definitions `Spec/Defs.lean` lists, which a reviewer reads with them.
 
-The gate rules, which `gate_eq` proves the gate follows exactly: a name that starts with `/` is rejected. A name with a `..` component, or with a special character, is rejected. Empty and `.` components are dropped. A name with nothing left is rejected. Only regular files (typeflag `0` or NUL) are extracted, which `manifest_eq` proves. Directory, link, and other entries are skipped, so a link entry cannot place a later entry outside the destination.
+The gate rules, which `gate_eq` proves the gate follows exactly: a name that starts with `/` is rejected. A name with a `..` component, or with a special character, is rejected. Empty and `.` components are dropped. A name with nothing left is rejected. Only regular files are extracted, which `manifest_eq` proves: typeflag `0`, NUL from older archives, or `7`, a contiguous file, which POSIX lets a reader treat as regular; and a name that does not end in `/`, which older archives use for a directory and GNU tar reads as one. So an entry with a regular typeflag and a name ending in `/` gets a `SKIP` line when its size is zero. When its size is not zero, the whole archive fails to parse, since readers disagree on whether data follows (see the list under What is not proved). Directory, link, and other entries are skipped, so a link entry cannot place a later entry outside the destination.
 
 - `gate_eq`: the gate is exactly its rules.
 - `gate_plain`: a name that passes the gate gives a non-empty list of plain names.
@@ -43,11 +43,17 @@ Axiom check: each theorem depends only on the standard Lean axioms (`propext`, `
 
 Read this before trusting the pilot with real archives:
 
-- Header parsing, octal fields, checksums, and archive writing are tested, not proved. The tests compare the Lean code against Python's `tarfile` module and against an independent copy of the extraction spec. Results are in `tests/TEST-RESULTS.md`: 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).
+- Header parsing, octal fields, checksums, and archive writing are tested, not proved. The tests compare the Lean code against Python's `tarfile` module and against an independent copy of the extraction spec. Results are in `tests/TEST-RESULTS.md`: 121 checks, 14 of them on the axioms, 0 failures. They cover 23 archive entries with normal files, hostile names (control characters and line separators among them), and a long name split over the ustar prefix field; eight destinations, and six refused: five for a special character or U+FFFD, and one given as bytes that are not UTF-8; broken inputs (truncated, garbage, bad checksum); 29 archives in formats the pilot does not read; and 13 more archives it does read, among them GNU format, GNU tar's own output in its default, `gnu` and `oldgnu` formats, names ending in `/`, and links, devices, directories and FIFOs whose size fields are not zero. Both commands are compared with `tarfile` on each of them. `tarfile` reads typeflag NUL with a name ending in `/` as a directory, typeflag 5, so the tool's typeflag 0 on such an entry is compared as 5. Every other typeflag is compared as printed.
 - The `list` output is tested, not proved. So is `Main.lean`: that it prints `o.line` for each outcome of the manifest, and refuses a destination with a special character or U+FFFD. Read it with the statements; it is a few lines.
 - Extraction works on an in-memory model. Nothing here writes files to disk, so the step from a proved in-memory path to a safe write on a real filesystem (races, symlinks already on disk, symlinked destination folders) is outside this project for now. The proof resolves paths lexically, as POSIX does when no component is a symlink.
 - The destination itself. The proof says where a path lands relative to the destination, not whether the destination is a safe place to write. The destination is the command-line argument as the Lean runtime decodes it from UTF-8.
-- Formats beyond POSIX ustar. 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.
+- Formats beyond POSIX ustar. The pilot reads ustar headers, and GNU headers that carry nothing ustar does not. As POSIX says, and as GNU tar and Python's `tarfile` read them, links, devices, directories and FIFOs store no data, whatever their size field says. An archive that uses anything else fails to parse as a whole, instead of being read in a wrong way:
+  - typeflags outside the POSIX set (NUL and `0` to `7`), among them GNU long names and long links (`L`, `K`), pax headers (`x`, `g`), and GNU sparse, incremental and volume entries. GNU tar writes long names this way by default, and Python's `tarfile` writes pax headers for long or non-ASCII names;
+  - a GNU header with anything where ustar keeps its name prefix (bytes 345 to 499), such as the access and change times of an incremental dump. GNU tar 1.35 puts nothing there for short names, in its default, `gnu` and `oldgnu` formats, unless it is asked for an incremental dump, a sparse file or a multi-volume archive;
+  - a name or prefix field that is not valid UTF-8;
+  - a base-256 size field, or a size field of spaces, which GNU tar refuses;
+  - a regular typeflag with a name ending in `/`, which reads as a directory, and a size that is not zero, where readers disagree on whether data follows;
+  - any other magic, such as an old Unix V7 header.
 - The Lean compiler, runtime, and kernel are trusted, as in every Lean project. A bug in them is outside the proof.
 
 ## Re-check it
@@ -60,7 +66,9 @@ python3 tests/run_tests.py
 
 The build fails if a proof breaks, though it accepts a `sorry` with only a warning. The second command prints the axioms each theorem depends on. The test script builds the project first, fails if any theorem depends on an axiom other than the three standard ones, reruns every comparison, and rewrites `tests/TEST-RESULTS.md`.
 
-`python3 tests/compare_old.py` builds the tool as it was before the containment change (commit 7517a86) and compares the two on 3,000 random archives under five destinations, from a recorded seed. Once the new escapes in names are undone, the output must be the same. It writes `tests/COMPARE-OLD.md`.
+`python3 tests/compare_old.py --new 1273382` builds the tool as it was before the containment change (commit 7517a86) and the tool of that change (commit 1273382), and compares the two on 3,000 random archives under five destinations, from a recorded seed. Once the new escapes in names are undone, the output must be the same. It writes `tests/COMPARE-OLD.md`. Without `--new`, it compares this checkout's tool, and runs differ on purpose: some random names end in `/` with a regular typeflag, and this tool skips such an entry, or refuses the archive when the entry has data.
+
+`python3 tests/run_tests.py --tool 1273382` runs the same checks against the tool of the containment change (commit 1273382), from before the parser changes. It leaves out the axiom check, which reads this checkout's proofs, not the tool, and writes `tests/TEST-RESULTS-1273382.md`: 68 of the 107 checks fail there.
 
 `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`.
 

Spec/Defs.lean

@@ -47,9 +47,12 @@ def cleanName (name : String) : Option (List String) :=
       let kept := parts.filter (fun c => !(c == "" || c == "."))
       if kept = [] then none else some kept
 
-/-- The typeflags of regular files: `0`, and NUL from older archives. -/
-def regularType (t : Char) : Bool :=
-  t == '0' || t == Char.ofNat 0
+/-- Whether an entry with typeflag `t` and name `name` is a regular file:
+    typeflag `0`, NUL from older archives, or `7`, a contiguous file,
+    which POSIX lets a reader treat as regular; and a name that does not
+    end in `/`, which older archives use for a directory. -/
+def regularType (t : Char) (name : String) : Bool :=
+  (t == '0' || t == Char.ofNat 0 || t == '7') && name.toList.getLast? != some '/'
 
 /-- A relative path `rel` under the destination `dest`, as a string: `rel`
     alone when `dest` is empty, `dest` then `rel` when `dest` ends in `/`,
@@ -135,7 +138,7 @@ def byteSum (b : ByteArray) : Nat :=
     whose name fails; `SKIP`, the name, and the typeflag as a decimal
     code, for anything else. -/
 def line (dest : String) (name : String) (t : Char) (data : ByteArray) : String :=
-  if regularType t then
+  if regularType t name then
     match cleanName name with
     | some rel =>
       "OK\t" ++ under dest (String.intercalate "/" rel) ++ "\t" ++ toString data.size ++

TarPilot/Archive.lean

@@ -51,11 +51,16 @@ def parseBlocks (data : ByteArray) (off : Nat) : Nat → Option (List RawEntry)
 def parseArchive (data : ByteArray) : Option (List RawEntry) :=
   parseBlocks data 0 (data.size / 512 + 1)
 
-/-- Regular files only: typeflag `0` or NUL. Directories, links, and
-    everything else are never extracted, so a link entry cannot be used
-    to place a later entry outside the destination. -/
+/-- Regular files only: typeflag `0`, NUL, or `7` (a contiguous file,
+    which POSIX lets a reader treat as regular, as Python's `tarfile`
+    does), and a name that does not end in `/`. Older archives mark a
+    directory with that `/`, and GNU tar reads any entry named so as a
+    directory. Directories, links, and everything else are never
+    extracted, so a link entry cannot be used to place a later entry
+    outside the destination. -/
 def isRegular (e : RawEntry) : Bool :=
-  e.typeflag == '0' || e.typeflag == Char.ofNat 0
+  (e.typeflag == '0' || e.typeflag == Char.ofNat 0 || e.typeflag == '7') &&
+    e.name.toList.getLast? != some '/'
 
 /-- Extract entries into a list of `(path, data)` pairs, in memory.
     The path of each pair is the destination components followed by the

TarPilot/Header.lean

@@ -16,7 +16,8 @@ import TarPilot.Octal
 
 namespace TarPilot
 
-/-- A parsed header. Only the fields the pilot uses. -/
+/-- A parsed header. Only the fields the pilot uses. `size` is the size
+    of the data that follows the header. -/
 structure Header where
   name : String
   size : Nat
@@ -31,32 +32,65 @@ def byteAt (b : ByteArray) (i : Nat) : UInt8 :=
 def sliceList (b : ByteArray) (off len : Nat) : List UInt8 :=
   (b.extract off (off + len)).toList
 
-/-- A name field: bytes up to the first NUL, read as UTF-8.
-    Invalid UTF-8 reads as the empty string. -/
-def bytesToName (bs : List UInt8) : String :=
+/-- A name field: bytes up to the first NUL, read as UTF-8, or `none`
+    when they are not valid UTF-8. -/
+def bytesToName (bs : List UInt8) : Option String :=
   let raw := bs.takeWhile (fun b => b ≠ 0)
-  (String.fromUTF8? (ByteArray.mk raw.toArray)).getD ""
+  String.fromUTF8? (ByteArray.mk raw.toArray)
+
+/-- The magic and version of a POSIX ustar header: `ustar`, NUL, `00`. -/
+def ustarMagic : List UInt8 := [117, 115, 116, 97, 114, 0, 48, 48]
+
+/-- The magic and version of a GNU header: `ustar`, two spaces, NUL. -/
+def gnuMagic : List UInt8 := [117, 115, 116, 97, 114, 32, 32, 0]
+
+/-- The typeflags the pilot reads: NUL and `0` to `7`, the types POSIX
+    ustar defines. Any other typeflag, among them the GNU long name and
+    long link entries `L` and `K`, the pax headers `x` and `g`, and GNU
+    sparse and incremental entries, makes the archive fail to parse:
+    such entries change how other entries read, or carry data the pilot
+    does not read. -/
+def knownTypeflag (t : Char) : Bool :=
+  t == Char.ofNat 0 || ('0' ≤ t && t ≤ '7')
 
 /-- The header checksum: sum of all 512 bytes, with the checksum field
     itself (bytes 148 to 155) counted as spaces. -/
 def blockChecksum (bs : List UInt8) : Nat :=
   (bs.zipIdx).foldl
     (fun acc p => acc + (if 148 ≤ p.2 ∧ p.2 < 156 then 32 else p.1.toNat)) 0
 
-/-- Parse one 512-byte header block. Fails on a short block, a bad
-    magic, a checksum mismatch, or a bad size field. -/
+/-- Parse one 512-byte header block. Fails on a short block; a magic
+    that is neither POSIX ustar nor GNU; a GNU header with anything in
+    the area where ustar keeps its prefix (GNU keeps access and change
+    times, sparse maps and volume offsets there); a checksum mismatch; a
+    bad size field; a typeflag outside `knownTypeflag`; a name or prefix
+    field that is not valid UTF-8; or a regular typeflag with a name
+    ending in `/`, which reads as a directory, and a size that is not
+    zero, where readers disagree on whether data follows.
+
+    Only regular typeflags (NUL, `0`, `7`) are followed by data. POSIX
+    stores no data for links, devices, directories and FIFOs (types 1 to
+    6), whatever their size field says, and GNU tar and Python's tarfile
+    read the next header straight after them, so the size given for
+    those is 0. -/
 def parseBlock (block : ByteArray) : Option Header :=
   if block.size < 512 then none
   else do
-    if sliceList block 257 5 ≠ [117, 115, 116, 97, 114] then none else
+    let magic := sliceList block 257 8
+    let gnuPlain := magic = gnuMagic ∧ (sliceList block 345 155).all (· = 0)
+    if ¬(magic = ustarMagic ∨ gnuPlain) then none else
     let stored ← parseOctal (sliceList block 148 8)
     if stored ≠ blockChecksum (sliceList block 0 512) then none else
     let size ← parseOctal (sliceList block 124 12)
-    let name := bytesToName (sliceList block 0 100)
-    let pfx := bytesToName (sliceList block 345 155)
+    let typeflag := Char.ofNat (byteAt block 156).toNat
+    if !knownTypeflag typeflag then none else
+    let name ← bytesToName (sliceList block 0 100)
+    let pfx ← bytesToName (sliceList block 345 155)
     let fullName := if pfx = "" then name else pfx ++ "/" ++ name
-    some { name := fullName, size := size,
-           typeflag := Char.ofNat (byteAt block 156).toNat }
+    let regular := typeflag == '0' || typeflag == Char.ofNat 0 || typeflag == '7'
+    let dirName := fullName.toList.getLast? == some '/'
+    if regular && dirName && size != 0 then none else
+    some { name := fullName, size := if regular then size else 0, typeflag := typeflag }
 
 /-- Content padded on the right with NUL bytes to width `w`,
     or cut to `w` when longer. -/
@@ -65,15 +99,16 @@ def fieldBytes (content : List UInt8) (w : Nat) : List UInt8 :=
 
 /-- Split a long name at a `/` so the part before it fits the 155-byte
     prefix field and the part after it fits the 100-byte name field.
-    Short names get an empty prefix. Fails when no split works. -/
+    Short names get an empty prefix. Neither part of a split may be
+    empty, so an absolute name keeps its `/`. Fails when no split works. -/
 def splitUstarName (name : String) : Option (String × String) :=
   if name.toUTF8.size ≤ 100 then some ("", name)
   else
     let cs := name.splitOn "/"
     let tries := (List.range cs.length).map fun k =>
       (String.intercalate "/" (cs.take (k + 1)), String.intercalate "/" (cs.drop (k + 1)))
     tries.find? (fun p =>
-      p.1.toUTF8.size ≤ 155 ∧ p.2.toUTF8.size ≤ 100 ∧ p.2 ≠ "")
+      p.1 ≠ "" ∧ p.1.toUTF8.size ≤ 155 ∧ p.2.toUTF8.size ≤ 100 ∧ p.2 ≠ "")
 
 /-- Build a 512-byte header block for a regular file or directory.
     Mode is fixed at 0644, uid, gid, and mtime at 0.

TarPilot/Octal.lean

@@ -14,9 +14,11 @@ def trimField (bs : List UInt8) : List UInt8 :=
   (noLead.reverse.dropWhile (fun b => b = 0 ∨ b = 32)).reverse
 
 /-- Parse an octal field. Fails on any byte that is not an octal digit
-    after trimming. An empty field parses as 0. -/
+    after trimming. A field with no digits parses as 0 when it is all
+    NUL, and fails when it holds a space, as GNU tar refuses it. -/
 def parseOctal (bs : List UInt8) : Option Nat :=
   let digits := trimField bs
+  if digits.isEmpty && bs.any (· == 32) then none else
   digits.foldl (fun acc b =>
     match acc with
     | none => none

tests/COMPARE-OLD.md

@@ -2,7 +2,7 @@
 
 Written by `tests/compare_old.py`. Rerun it to check these numbers.
 
-- Old tool: commit 7517a86. New tool: this checkout.
+- Old tool: commit 7517a86. New tool: commit 1273382.
 - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.13.17.
 - Seed: 20261025
 - Random archives: 3000, written by Python's `tarfile` in ustar format