Adopt verified bar v2 for tar (in progress: spec approval pending)

.github/workflows/bar.yml

@@ -0,0 +1,24 @@
+name: verified bar
+
+on:
+  push:
+  pull_request:
+  # Rerun when the spec reviewer approves, or an approval is dismissed.
+  pull_request_review:
+    types: [submitted, dismissed]
+
+jobs:
+  bar:
+    # pull-requests: read lets the check confirm the spec approval on GitHub.
+    permissions:
+      contents: read
+      pull-requests: read
+    # Both lines pin the same commit of Proven-Commons/mission: the bar v2
+    # check from its pull request #2, now merged into main. Mission has no
+    # release tag yet. Move both lines to one once it publishes one
+    # (Proven-Commons/mission#10).
+    # Item 7 also needs `main` here to require this check. That is a repo
+    # setting only a maintainer can change, tracked in mission#10 too.
+    uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2
+    with:
+      bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2

.gitignore

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

SPEC.md

@@ -0,0 +1,82 @@
+# Specification: tar
+
+A reader for tar archives that lists them and says where each regular file would be extracted, without letting any entry land outside the destination. A reviewer who did not write this specification approves it, together with `Spec.lean`, `Spec/Defs.lean`, and the other files `bar.toml` lists.
+
+Archives are bytes. Names are UTF-8 strings. The command-line tool reads a file and prints lines.
+
+## Reading an archive
+
+Scope: POSIX ustar, and GNU headers that carry nothing ustar does not. Anything outside the rules below makes the whole archive fail to parse, rather than be read in a way the pilot does not vouch for.
+
+An archive is a sequence of 512-byte header blocks and ends at a block of zeros. A header of a regular file is followed by its data, padded to a whole number of blocks. Links, devices, directories and FIFOs (types `1` to `6`) store no data, as POSIX says: the next header follows straight after, whatever their size field says, which is how GNU tar and Python's `tarfile` read them. A header is read only when all of these hold:
+
+- Bytes 257 to 264 are `ustar`, NUL, `00` (POSIX), or `ustar`, two spaces, NUL (GNU). A GNU header must have only zeros in bytes 345 to 499, where ustar keeps its name prefix and GNU keeps times, sparse maps, and volume offsets.
+- The checksum field (bytes 148 to 155) is the sum of all 512 bytes, as unsigned numbers, counting the checksum field itself as spaces. A sum over signed bytes, which some old tars wrote and GNU tar and `tarfile` accept, is not read.
+- The size field (bytes 124 to 135) and the checksum field are octal: leading spaces, then digits `0` to `7`, then NULs or spaces. A field with no digits reads as zero when it is all NUL, and is not read when it holds a space, as GNU tar refuses it. Base-256 fields are not read.
+- The typeflag (byte 156) is NUL or one of `0` to `7`, the POSIX types. GNU long names and long links (`L`, `K`), pax headers (`x`, `g`), and any other type are not read.
+- The name field (bytes 0 to 99) and the prefix field (bytes 345 to 499), each up to its first NUL, are valid UTF-8. The entry's name is the name field, or the prefix, `/`, and the name field when the prefix is not empty.
+- A regular typeflag (NUL, `0`, `7`) with a name ending in `/`, which older archives use for a directory, has size zero: readers disagree on whether data follows such an entry.
+
+An archive fails to parse when a header is not read, when an entry's data runs past the end of the input, or when the input ends before a block of zeros. Then the tool prints nothing on standard output and exits with code 1, as it does when the file cannot be read.
+
+## The path gate
+
+Each entry's name goes through the gate, which gives the components the entry is extracted under, or rejects the name. The rules:
+
+- A name that starts with `/` is rejected.
+- A name with a `..` component, or with a special character, is rejected. The special characters are the control characters (C0, DEL, and C1) and the Unicode line separator U+2028 and paragraph separator U+2029, which some readers take as line breaks.
+- Empty and `.` components are dropped.
+- A name with nothing left is rejected.
+
+So every component the gate gives is a plain name: not empty, not `.` or `..`, and free of `/` and of special characters.
+
+## Extraction
+
+Only regular files are extracted: 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. Directories, links, devices, and FIFOs are skipped, so a link entry cannot place a later entry outside the destination.
+
+For each entry, in archive order, the outcome is one of:
+
+- extract: a regular file whose name passes the gate, at the destination followed by the gate's components, with the entry's own data;
+- reject: a regular file whose name fails the gate;
+- skip: any other entry.
+
+Extraction works on an in-memory list. Nothing is written to disk.
+
+## The command-line tool
+
+`tar-pilot list <file>` prints one line per entry: the name, its data size, and its typeflag as a decimal code, separated by tabs.
+
+`tar-pilot manifest <file> <dest>` prints one line per entry, separated by tabs:
+
+- `OK`, the path, the data size, and the sum of the data bytes, for an extracted entry. The path is the destination exactly as given, then the gate's components joined by `/`: after a `/` when the destination does not end in one, and with nothing before them when the destination is empty.
+- `REJECT` and the name, for a rejected entry.
+- `SKIP`, the name, and the typeflag code, for a skipped entry.
+
+In `list`, `REJECT` and `SKIP` lines, a backslash in a name is printed as two backslashes, U+2028 and U+2029 as `\u2028` and `\u2029`, and any other special character as `\x` and two lowercase hex digits. So a printed name holds no special character, which `Spec/Defs.lean` proves (`Spec.escape_noSpecial`). Every line ends in a line feed. A destination that holds a special character, or U+FFFD (which the Lean runtime puts in place of bytes that are not UTF-8), is refused, with exit code 2.
+
+`tar-pilot create <out> <file>...` writes a ustar archive of the given files, each under the name given. A long name is split at a `/` into the prefix and name fields, and neither part may be empty, so an absolute name keeps its `/`. A name that does not fit makes it fail with exit code 1, writing nothing.
+
+Any other use prints a usage message and exits with code 2.
+
+## What must always hold
+
+Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use are in `Spec/Defs.lean`.
+
+| Property | Theorem |
+|----------|---------|
+| The gate is exactly its rules. | `TarPilot.gate_eq` |
+| A name that passes the gate gives a non-empty list of plain names. | `TarPilot.gate_plain` |
+| The outcome of each entry is as described under Extraction. | `TarPilot.manifest_eq` |
+| The extracted outcomes are exactly the extractor's output, in order. | `TarPilot.manifest_extracted` |
+| Each line `manifest` prints is exactly the line described above (`Spec.line`). | `TarPilot.manifest_lines_eq` |
+| With a destination free of special characters, a line holds no special character but its tabs, and every `OK` line is the destination as given, then plain names joined by `/`, then a tab. | `TarPilot.manifest_lines` |
+| Every extracted path is the destination followed by a non-empty list of plain names. | `TarPilot.extractAll_contained` |
+| Joined with `/`, it splits back into the destination components and those names. | `TarPilot.extractAll_joined` |
+| Resolved lexically, it is the resolved destination followed by those names, for entries or for an archive read from bytes. | `TarPilot.extractAll_resolves_inside`, `TarPilot.extractArchive_resolves_inside` |
+| Extracting an archive read from bytes is parsing it, then extracting the entries. | `TarPilot.extractArchive_eq` |
+
+The statements fix what extraction, the gate, and the `manifest` output do with the entries of a parsed archive. How bytes are parsed into entries, the `list` output, `create`, and the few lines of `Main.lean` that print the manifest and check the destination are fixed by the rules above and checked by the differential tests, not by a proof.
+
+## Oracle
+
+Python's `tarfile` module, and a model of the format above written in `tests/run_tests.py` independently of the Lean code. The model is checked against `tarfile` on every unmutated archive both read.

Spec.lean

@@ -0,0 +1,111 @@
+/-
+  The specification as Lean statements: the challenge file.
+
+  A reviewer who did not write this file approves it, together with
+  `Spec/Defs.lean` and the other files `bar.toml` lists, and `bar.toml`
+  records the hash they had then. The proofs live in `Proofs/`, under the
+  same names; `lake comparator` checks that each one proves exactly the
+  statement written here. The `sorry` below is expected in this file
+  only.
+
+  The statements are about the code in `TarPilot/`: the gate, the
+  extraction rule, the manifest, and the lines the command-line tool
+  prints. They do not cover how bytes are parsed into entries; the
+  differential tests do.
+-/
+
+import TarPilot
+import Spec.Defs
+
+open Spec
+
+namespace TarPilot
+
+/-- The gate is exactly its rules (`Spec.cleanName`). -/
+theorem gate_eq (name : String) : gate name = Spec.cleanName name := sorry
+
+/-- 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 := sorry
+
+/-- 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 e.name then
+        match cleanName e.name with
+        | some rel => .extract (dest ++ rel) e.data
+        | none => .reject e.name
+      else .skip e.name e.typeflag := sorry
+
+/-- 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 := sorry
+
+/-- 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 := sorry
+
+/-- 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 := sorry
+
+/-- 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 := sorry
+
+/-- 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 := sorry
+
+/-- What `tar-pilot manifest <file> <dest>` 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) := sorry
+
+/-- What `tar-pilot manifest <file> <dest>` 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 := sorry
+
+/-- 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) := sorry
+
+end TarPilot

bar.toml

@@ -0,0 +1,38 @@
+# Read by bar/check.py in Proven-Commons/mission.
+# See playbook/verified-bar.md there for what each field means.
+
+[project]
+name = "tar"
+# "in-progress" until every bar item passes, then "verified".
+status = "in-progress"
+page = "README.md"
+# GitHub handles of everyone who wrote the specification. It was drafted
+# by Claude, an AI agent, for the org.
+spec_authors = ["claude"]
+# The program people run. A change to it voids the approval.
+entry_points = ["Main.lean"]
+
+[spec]
+files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean"]
+# The code under proof: the functions and types the statements are about.
+code = [
+  "TarPilot.gate", "TarPilot.manifest", "TarPilot.extractAll", "TarPilot.extractArchive",
+  "TarPilot.parseArchive",
+  "TarPilot.destComponents", "TarPilot.joinPath",
+  "TarPilot.Outcome", "TarPilot.Outcome.extract", "TarPilot.Outcome.reject",
+  "TarPilot.Outcome.skip", "TarPilot.Outcome.line", "TarPilot.Outcome.extracted",
+  "TarPilot.RawEntry", "TarPilot.RawEntry.name", "TarPilot.RawEntry.typeflag",
+  "TarPilot.RawEntry.data",
+]
+
+# One entry per approval, added in a pull request the reviewer approves.
+# [[spec.approval]]
+# reviewer = "github-handle"
+# date = "2026-11-02"
+# sha256 = "..."
+# record = "https://github.com/Proven-Commons/tar/pull/<n>"
+
+[tests]
+results = "tests/TEST-RESULTS.md"
+command = "python3 tests/run_tests.py"
+files = ["tests/run_tests.py"]

comparator.json

@@ -0,0 +1,22 @@
+{
+  "challenge_module": "Spec",
+  "solution_module": "Proofs",
+  "theorem_names": [
+    "TarPilot.gate_eq",
+    "TarPilot.gate_plain",
+    "TarPilot.manifest_eq",
+    "TarPilot.extractAll_contained",
+    "TarPilot.extractAll_joined",
+    "TarPilot.extractAll_resolves_inside",
+    "TarPilot.extractArchive_resolves_inside",
+    "TarPilot.manifest_extracted",
+    "TarPilot.manifest_lines",
+    "TarPilot.manifest_lines_eq",
+    "TarPilot.extractArchive_eq"
+  ],
+  "permitted_axioms": [
+    "propext",
+    "Quot.sound",
+    "Classical.choice"
+  ]
+}

lakefile.toml

@@ -7,7 +7,6 @@ name = "TarPilot"
 
 [[lean_lib]]
 name = "Spec"
-roots = ["Spec.Defs"]
 
 [[lean_lib]]
 name = "Proofs"