Reject unsupported tar metadata and check the pilot in CI

.github/scripts/setup-lean.sh

@@ -0,0 +1,22 @@
+#!/bin/sh
+# Install the pinned toolchain manager and require a working kernel-check sandbox.
+# Adapted from Proven-Commons/mission's proposed verified bar v2 setup script.
+set -eu
+
+ELAN_VERSION=v4.2.4
+ELAN_SHA256=42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63
+task_tmp=$(mktemp -d)
+trap 'rm -rf "$task_tmp"' EXIT
+curl -sSfL -o "$task_tmp/elan.tar.gz" \
+  "https://github.com/leanprover/elan/releases/download/$ELAN_VERSION/elan-x86_64-unknown-linux-gnu.tar.gz"
+printf '%s  %s\n' "$ELAN_SHA256" "$task_tmp/elan.tar.gz" | sha256sum -c -
+tar -xzf "$task_tmp/elan.tar.gz" -C "$task_tmp"
+"$task_tmp/elan-init" -y --no-modify-path --default-toolchain none
+printf '%s\n' "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+sudo apt-get update -q
+sudo apt-get install -yq bubblewrap
+if [ -f /proc/sys/kernel/apparmor_restrict_unprivileged_userns ]; then
+  sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0
+fi
+bwrap --ro-bind / / --dev /dev --proc /proc --unshare-all true

.github/workflows/check.yml

@@ -0,0 +1,41 @@
+name: Proofs and differential tests
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  check:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 45
+    steps:
+      - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@ece7cb06caefa5fff74198d8649806c4678c61a1 # v6
+        with:
+          python-version: "3.12"
+      - name: Install Lean and bubblewrap
+        run: sh .github/scripts/setup-lean.sh
+      - name: Build, regressions, differential tests and axiom allowlist
+        run: |
+          rm -f tests/TEST-RESULTS.md
+          python3 tests/run_tests.py
+      - name: Replay proofs under all six kernels in the sandbox
+        run: lake check --paranoid
+      - name: Save the differential test report
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
+        with:
+          name: tar-test-results
+          path: tests/TEST-RESULTS.md
+          if-no-files-found: error

.gitignore

@@ -1 +1,2 @@
 .lake/
+__pycache__/

README.md

@@ -4,6 +4,8 @@ This repo reads a tar archive (ustar format) and extracts regular files into an
 
 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.
 
+The [draft specification](SPEC.md) defines the supported ustar subset and extraction contract. It awaits independent review. GNU magic, extension metadata, invalid UTF-8 path fields, incomplete end blocks, and nonzero trailing data reject the whole archive before `list` or `manifest` prints entries.
+
 ## Run it
 
 Needs Lean 4.35.0 (install with elan, toolchain pinned in `lean-toolchain`).
@@ -29,17 +31,17 @@ The path gate and the extraction rule, in `TarPilot/Path.lean` and `TarPilot/Arc
 
 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.
+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. Data files (typeflag `0`, NUL, or `7`) are extracted. Directory, link, and other supported non-data 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`: 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.
+- 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. The [test report](tests/TEST-RESULTS.md) records the original archive and create/readback checks, 524 path cases across eight destinations, and the parser campaign (seed `20261025`: 512 random valid archives and 512 mutated invalid archives, plus fixed regressions). Every parser case checks both `list` and `manifest`; rejected cases must print no stdout. All 256 typeflag bytes are covered. `posixpath` independently checks emitted paths. Lean regressions cover separators, NUL, UTF-8 decoding, header writing, and the old theorem's traversal counterexample.
 - 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.
-- 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 reader intentionally rejects formats outside its [supported subset](SPEC.md): GNU magic, pax/GNU extension headers, sparse extension types, base-256 sizes, non-data entries with payloads, and ambiguous NUL-type directory names. It requires block alignment, two zero end blocks, and only zero record padding after them. Some other tar readers accept inputs this pilot rejects. UTF-8 is required for both path fields; other encodings are not converted. The CLI prints tabs and line breaks in names literally; its text output is not an escaped wire format.
 - 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
@@ -48,10 +50,13 @@ Read this before trusting the pilot with real archives:
 lake build
 lake env lean TarPilot/Verify.lean
 python3 tests/run_tests.py
+lake check --paranoid
 ```
 
 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.
 
+`lake check --paranoid` needs a working `bubblewrap` sandbox on Linux. It replays proofs through all six bundled kernels and rejects nonstandard axioms. The `Proofs and differential tests` workflow runs the test script and the sandboxed proof check on pull requests and pushes to `main`, and saves the test report as an artifact. Branch protection must separately require this workflow; independent specification approval is still outstanding.
+
 ## Layout
 
 - `TarPilot/Path.lean`: the path gate and its proofs.
@@ -62,3 +67,6 @@ The build checks the proofs, but accepts `sorry` with a warning. The second comm
 - `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.
+- `tests/HeaderSafety.lean`: UTF-8 decoding and header-builder regressions.
+- `tests/parser_cases.py`: format regressions and seeded parser comparisons.
+- `SPEC.md`: the draft contract for review.

SPEC.md

@@ -0,0 +1,99 @@
+# Tar pilot specification
+
+Status: **draft, awaiting independent specification review**. This document
+records the intended contract of this implementation. It is not an approval
+record and does not establish the org's verified bar.
+
+## Supported archive input
+
+The reader accepts a strict subset of POSIX ustar. It returns the complete
+entry list or an error; it never returns a successfully parsed prefix of an
+invalid archive.
+
+- Input length is a multiple of 512 bytes. Every entry has a complete
+  512-byte header and enough bytes for its declared payload and block padding.
+- Header magic is exactly `ustar` followed by NUL, and version is exactly
+  `00`. GNU's different magic/version is rejected.
+- The checksum is the unsigned sum of all 512 header bytes, treating bytes
+  148 through 155 as ASCII spaces. Both checksum and size are octal fields:
+  leading spaces and trailing spaces/NUL are removed, remaining bytes must
+  be `0` through `7`, and an empty field means zero. Base-256 sizes fail.
+- Types NUL, `0`, and `7` are data files. Types `1` through `6` are accepted
+  only with size zero and are skipped by extraction. Every other type
+  rejects the whole archive, including GNU longname/longlink, pax per-file
+  and global headers, and sparse extension types.
+- The name and prefix fields are each decoded as UTF-8 up to their first
+  NUL. Invalid UTF-8 in either field rejects the whole archive. Bytes after
+  a terminating NUL are outside the field value. A nonempty prefix is
+  joined to the name with `/`. No invalid field is replaced with empty text.
+- A NUL-type entry whose full name ends with `/` is rejected: legacy readers
+  can interpret it as a directory rather than a regular file.
+- The archive ends with at least two consecutive all-zero blocks. All bytes
+  after the first end block must also be zero. Missing end blocks, partial
+  blocks, concatenated nonempty archives, and nonzero trailing data are rejected.
+
+Extension-free output from a tool using its pax option can still satisfy
+this subset; format labels alone do not determine acceptance. Header mode,
+owner, timestamps, device fields, and link targets are ignored. They do not
+affect the emitted in-memory file paths or contents. Payload padding need
+not be zero. This reader does not decompress archives or write extracted
+files to disk.
+
+## Extraction
+
+The parser returns names, original typeflags, and payload bytes in archive
+order. `extractEntry` emits a result only for NUL, `0`, or `7` entries whose
+names pass the path gate. `extractAll` preserves the order and duplicates of
+those results. Non-data entries are skipped; a rejected data-file name does
+not reject the archive.
+
+The gate rejects names beginning with `/`, any `..` component, and any
+component containing `/` or NUL. It drops empty and `.` components and
+requires a nonempty result. It joins those relative components after the
+caller-supplied destination components.
+
+`PlainName`, `gate_plain`, `extractAll_contained`, `extractAll_joined`, and
+`extractAll_resolves_inside` state the formal guarantees. With slash-free
+destination components, the rendered string splits into exactly the
+destination followed by nonempty plain names. Resolving it with the relative
+POSIX lexical resolver gives the resolved destination followed by those
+names. This does not model absolute-root handling, Windows paths, existing
+filesystem symlinks, or filesystem races.
+
+## Commands and archive writing
+
+`list` and `manifest` parse the whole archive before printing any entries.
+Malformed or unsupported archives exit 1, print an error to stderr, and
+produce no stdout. Accepted archives exit 0. `manifest` calls `extractEntry`
+and `joinPath` for `OK` results, printing `REJECT` for a data-file name that
+fails the gate and `SKIP` for a non-data entry.
+
+The CLI output is a textual view, not an escaped wire format: names containing
+tabs or line breaks are printed literally. Formatting, I/O handling, byte sums,
+and exit behavior are outside the proof. Tests cover formatting, byte sums,
+and archive-rejection exits; they do not cover every I/O failure.
+
+`create` emits regular ustar entries followed by two zero blocks. It fails
+when a name cannot fit the ustar name/prefix fields or a size cannot fit an
+octal size field. The header builder rejects embedded NUL, unsupported
+types, non-data entries with payloads, and ambiguous NUL-type directories.
+Mode is fixed at 0644; owner IDs and timestamps are zero. Archive writing is
+tested rather than proved.
+
+## Evidence and limits
+
+`python3 tests/run_tests.py` builds the current sources, runs the Lean
+regressions, compares accepted archives with Python `tarfile`, checks
+rejected cases for exit 1 and no stdout, and checks every printed theorem's
+axioms against the standard three. The committed report records seeds,
+case counts, versions, and failures. `tests/parser_cases.py` includes the
+format and UTF-8 failures from the
+[2026-10-24 audit](https://github.com/Proven-Commons/mission/pull/1), all 256
+typeflag bytes, valid random archives, and mutated invalid archives.
+
+`lake check --paranoid` replays the built proof declarations through all six
+bundled kernels in a sandbox. CI runs both commands. Passing them does not
+prove the byte parser or writer, validate this specification's adequacy, or
+supply independent approval. The compiler, runtime, kernels, hardware, and
+test oracles remain trusted. Requiring the CI check through branch protection
+is a separate repository setting.

TarPilot/Archive.lean

@@ -34,7 +34,12 @@ def parseBlocks (data : ByteArray) (off : Nat) : Nat → Option (List RawEntry)
     if off + 512 > data.size then none
     else
       let block := data.extract off (off + 512)
-      if block.toList.all (· = 0) then some []
+      if block.toList.all (· = 0) then
+        -- Require two end blocks, then only zero record padding. Reject
+        -- hidden trailing entries instead of returning a clean prefix.
+        if off + 1024 > data.size then none
+        else if (data.extract off data.size).toList.all (· = 0) then some []
+        else none
       else match parseBlock block with
         | none => none
         | some h =>
@@ -49,13 +54,14 @@ def parseBlocks (data : ByteArray) (off : Nat) : Nat → Option (List RawEntry)
 
 /-- Parse a whole archive. -/
 def parseArchive (data : ByteArray) : Option (List RawEntry) :=
-  parseBlocks data 0 (data.size / 512 + 1)
+  if data.size % 512 != 0 then none
+  else parseBlocks data 0 (data.size / 512 + 1)
 
-/-- Regular files only: typeflag `0` or NUL. Directories, links, and
+/-- Data files only: typeflag `0`, NUL, or `7`. 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
+  isRegularType e.typeflag
 
 /-- The extraction decision shared by the CLI and the in-memory model. -/
 def extractEntry (dest : List String) (e : RawEntry) : Option (List String × ByteArray) :=

TarPilot/Header.lean

@@ -31,32 +31,49 @@ 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, decoded without replacement.
+    Invalid UTF-8 rejects the header instead of losing half a split name. -/
+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)
+
+/-- Ustar data files, including the POSIX contiguous-file type. -/
+def isRegularType (typeflag : Char) : Bool :=
+  typeflag == '0' || typeflag == Char.ofNat 0 || typeflag == '7'
+
+/-- Types this reader understands. Extension metadata must reject the
+    archive: skipping it could silently substitute a different pathname. -/
+def isSupportedType (typeflag : Char) : Bool :=
+  isRegularType typeflag || typeflag == '1' || typeflag == '2' ||
+    typeflag == '3' || typeflag == '4' || typeflag == '5' || typeflag == '6'
 
 /-- 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 the supported POSIX ustar subset: exact magic and version,
+    supported types, octal size and checksum, and UTF-8 pathname fields.
+    Non-data entries must have zero size. -/
 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
+    if sliceList block 257 6 ≠ [117, 115, 116, 97, 114, 0] then none else
+    if sliceList block 263 2 ≠ [48, 48] then none else
     let stored ← parseOctal (sliceList block 148 8)
     if stored ≠ blockChecksum (sliceList block 0 512) then none else
+    let typeflag := Char.ofNat (byteAt block 156).toNat
+    if !isSupportedType typeflag then none else
     let size ← parseOctal (sliceList block 124 12)
-    let name := bytesToName (sliceList block 0 100)
-    let pfx := bytesToName (sliceList block 345 155)
+    if !isRegularType typeflag && size != 0 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 }
+    -- Old tar readers interpret a NUL-type trailing slash as a directory.
+    -- Reject that ambiguous form rather than disagree about its payload.
+    if typeflag == Char.ofNat 0 && fullName.endsWith "/" then none else
+    some { name := fullName, size := size, typeflag := typeflag }
 
 /-- Content padded on the right with NUL bytes to width `w`,
     or cut to `w` when longer. -/
@@ -79,6 +96,10 @@ def splitUstarName (name : String) : Option (String × String) :=
     Mode is fixed at 0644, uid, gid, and mtime at 0.
     Fails when the size or the name does not fit. -/
 def buildBlock (name : String) (size : Nat) (typeflag : Char) : Option ByteArray := do
+  if Char.ofNat 0 ∈ name.toList then none else
+  if !isSupportedType typeflag then none else
+  if !isRegularType typeflag && size != 0 then none else
+  if typeflag == Char.ofNat 0 && name.endsWith "/" then none else
   let (pfx, short) ← splitUstarName name
   let sizeF ← formatOctal size 12
   let modeF ← formatOctal 0o644 8