diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
new file mode 100644
index 0000000..c48bd68
--- /dev/null
+++ b/.github/workflows/lean_action_ci.yml
@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v5
+      - uses: leanprover/lean-action@v1
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..bfb30ec
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/FidelityMain.lean b/FidelityMain.lean
new file mode 100644
index 0000000..2f322ce
--- /dev/null
+++ b/FidelityMain.lean
@@ -0,0 +1,6 @@
+import ShellWall.Fidelity
+
+/-- Entry point for the `fidelity` executable (`lake exe fidelity`). Runs the
+fidelity harness, which shells out to real bash in a temp sandbox. Kept out of
+`lake build`'s default targets so the core build stays pure and hermetic. -/
+def main : IO Unit := ShellWall.Fidelity.runFidelity
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..0b1d924
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,5 @@
+import ShellWall
+
+-- Entry point placeholder; real invocation of `gate` deferred to a later prompt.
+def main : IO Unit :=
+  IO.println "ShellWall"
diff --git a/ShellWall.lean b/ShellWall.lean
new file mode 100644
index 0000000..9acd4ba
--- /dev/null
+++ b/ShellWall.lean
@@ -0,0 +1,46 @@
+-- Root of the ShellWall library. Import all submodules.
+import ShellWall.Basic
+import ShellWall.Syntax
+import ShellWall.Policy
+import ShellWall.Semantics
+import ShellWall.Provenance
+import ShellWall.Safety
+import ShellWall.Decide
+import ShellWall.Gate
+
+/-! # ShellWall — ARCHITECTURE (trusted kernel vs. untrusted layer)
+
+The library is deliberately split into a small TRUSTED KERNEL — inductive definitions
+audited by inspection — and a larger UNTRUSTED LAYER of fast functions and models that
+are believed only through soundness/fidelity, never trusted directly. The security
+value rests on the kernel being small enough to read and believe.
+
+TRUSTED BASE (audit these by eye — the whole guarantee rests on them):
+- `classify`, `ownerOf`  (Policy.lean) — the policy table: which paths are public and
+  who owns them. Configuration, not proof.
+- `CanWrite`, `SafeCmd`, `SafePipeline`  (Safety.lean) — the inductive SAFETY spec: what
+  it means for a command/pipeline to be safe to run.
+- `PublicProv`, `PipeProv`  (Provenance.lean) — the inductive PUBLIC-PROVENANCE kernel:
+  what it means for content to be derived only from public sources. Provenance, not
+  value (the third-hole correction); no aggregation constructor (statistical-channel
+  exclusion).
+
+UNTRUSTED, BUT PROVEN SOUND against the kernel (a `true` answer yields a kernel proof):
+- `cmdOutIsPublic` / `provOut`  ⟶  `cmdOutIsPublic_sound` / `provOut_sound` (Provenance).
+- `checkCmd` / `checkFull` / `checkSafe`  ⟶  `checkSafe_sound` / `checkFull_sound`
+  (Decide.lean): the fast prove-or-reject gate implies `SafePipeline`.
+
+UNTRUSTED MODEL (fidelity-tested against real bash, NOT proven):
+- `evalCmd` / `evalPipelineFull`  (Semantics.lean) — the execution model. The kernel
+  inductives are stated relative to it (§4 central assumption); its faithfulness is
+  checked by the `fidelity` executable, not proved.
+- the bash→`Pipeline` parser and the executor — the two remaining unverified edges.
+
+TOP-LEVEL GUARANTEE: `shellwall_noninterference` (Safety.lean) — a pipeline `SafePipeline`
+in two states agreeing on public paths cannot leak private data into the public
+projection. Proved (0 `sorry`), axiom-clean. It survived four soundness attacks; the
+four historical holes and their fixes are recorded in its docstring.
+
+So "how small is the kernel?": five inductive families (`classify`/`ownerOf` tables +
+`CanWrite`/`SafeCmd`/`SafePipeline` + `PublicProv`/`PipeProv`). Everything else is a
+function proven sound against them, or a model checked for fidelity. -/
diff --git a/ShellWall/Basic.lean b/ShellWall/Basic.lean
new file mode 100644
index 0000000..21702b1
--- /dev/null
+++ b/ShellWall/Basic.lean
@@ -0,0 +1,63 @@
+/-- A filesystem path. Lean's standard path type: a structure wrapping a `String`,
+with real path operations (`components`, `join`, `/`, `parent`, ...).
+`DecidableEq` comes from the underlying `String` and is available without a manual
+instance. Policy subtree-matching decomposes to `components` inside
+`classify`/`ownerOf`; everywhere else `Path` flows opaquely. -/
+abbrev Path := System.FilePath
+
+/-- The content of a file or a pipe stage's stdin/stdout: UTF-8 text, raw bytes,
+or nothing. Note the three distinct "no bytes" representations (`.text ""`,
+`.binary ByteArray.empty`, `.empty`); the semantics canonicalise empty results to
+`.empty`. -/
+inductive Content where
+  /-- Text content, held as a `String`. -/
+  | text   (s : String)
+  /-- Binary content, held as a raw `ByteArray`. -/
+  | binary (b : ByteArray)
+  /-- No content — the canonical empty value. -/
+  | empty
+
+/-- How a `write` deposits its stdin at the target path. -/
+inductive WriteMode where
+  /-- Replace the target's content outright (`> p`). -/
+  | overwrite
+  /-- Append to the target's existing content (`>> p`). -/
+  | append
+  deriving DecidableEq
+
+/-- A command/pipeline exit status. `failure` carries the nonzero code, mirroring
+POSIX exit codes; drives `&&`/`||` short-circuiting in the semantics. -/
+inductive ExitCode where
+  /-- Exit 0. -/
+  | success
+  /-- Nonzero exit, carrying the code. -/
+  | failure (code : Nat)
+  deriving DecidableEq
+
+/-- Two `ByteArray`s with equal underlying `data` arrays are equal. Bridges the
+gap that `ByteArray` exposes no `DecidableEq` in core; the `Content` equality
+decision below relies on it. -/
+theorem byteArray_eq_of_data_eq {b₁ b₂ : ByteArray} (h : b₁.data = b₂.data) : b₁ = b₂ := by
+  cases b₁; cases b₂; simp only [ByteArray.mk.injEq]; exact h
+
+/-- Decidable equality on `Content`, deciding the `binary` case through the
+underlying `Array UInt8` (`ByteArray` has no core `DecidableEq`, so `Content`
+cannot simply `deriving DecidableEq`).
+
+NOTE: this instance is NOT load-bearing for execution — the stream operations in
+`Semantics.lean` compare *lines* (`String`s), never whole `Content` values. It is
+provided for completeness and for later proof/testing use. -/
+instance : DecidableEq Content
+  | .text s₁, .text s₂ =>
+      if h : s₁ = s₂ then isTrue (by rw [h])
+      else isFalse (by intro hc; injection hc with h'; exact h h')
+  | .binary b₁, .binary b₂ =>
+      if h : b₁.data = b₂.data then isTrue (by rw [byteArray_eq_of_data_eq h])
+      else isFalse (by intro hc; injection hc with h'; exact h (by rw [h']))
+  | .empty, .empty => isTrue rfl
+  | .text _,   .binary _ => isFalse (fun h => Content.noConfusion h)
+  | .text _,   .empty    => isFalse (fun h => Content.noConfusion h)
+  | .binary _, .text _   => isFalse (fun h => Content.noConfusion h)
+  | .binary _, .empty    => isFalse (fun h => Content.noConfusion h)
+  | .empty,    .text _   => isFalse (fun h => Content.noConfusion h)
+  | .empty,    .binary _ => isFalse (fun h => Content.noConfusion h)
diff --git a/ShellWall/Decide.lean b/ShellWall/Decide.lean
new file mode 100644
index 0000000..9184eee
--- /dev/null
+++ b/ShellWall/Decide.lean
@@ -0,0 +1,295 @@
+import ShellWall.Safety
+
+/-! # UNTRUSTED DECISION LAYER (proven sound)
+
+`canWriteB`/`checkCmd`/`checkFull`/`checkSafe` are FAST Bool decision procedures — the
+untrusted layer. They are not trusted directly: `checkSafe_sound`/`checkFull_sound`
+(below) prove a `true` verdict implies the trusted `SafePipeline` kernel (Safety.lean),
+and `provOut_sound` (Provenance.lean) links the provenance flag they thread to the
+`PublicProv` kernel. Completeness is intentionally NOT claimed — the gate may reject
+some genuinely-safe pipelines. See the ARCHITECTURE note in `ShellWall.lean`. -/
+
+/-! ## Deciding `CanWrite` -/
+
+/-- Boolean decision of `CanWrite a p`, which in v1 reduces to `ownerOf p = a`
+(`self` is `CanWrite`'s only constructor). Proved sound by `canWriteB_sound`.
+
+TODO(v2): if delegation constructors are added to `CanWrite`, this becomes an
+UNDER-approximation (rejecting writes a delegate is entitled to). Sound in that
+direction, but must be revisited. -/
+def canWriteB (a : Owner) (p : Path) : Bool := decide (ownerOf p = a)
+
+-- Provenance is tracked FORWARD by `cmdOutIsPublic`/`provOut` (in `Semantics`),
+-- shared by both the decider here and `SafeCmd`/`SafePipeline`. There is
+-- deliberately no `isPublicB : FileState → Content → Bool` (a backward, value-based
+-- decision): `Content` carries no trace of its derivation, and value-based public-ness
+-- is relationally unsound anyway (a private value coinciding with a public path's bytes
+-- would satisfy it). Forward provenance is the right notion.
+
+/-! ## Deciding safety -/
+
+/-- Boolean decision of `SafeCmd` for a single command, given stdin public-ness
+`stdinPub`. Mirrors `SafeCmd`'s constructors case-for-case (which
+`checkFull_sound`'s single case follows).
+
+NOTE: the state parameter `_s` is deliberately unused. `SafeCmd`'s only state-
+dependent premise is the public-provenance of `stdin`, whose decision is factored out
+into `stdinPub` (computed by `cmdOutIsPublic` at the producing stage, where the state
+IS consulted); `classify`/`ownerOf` are state-independent. The parameter is kept for
+signature parallelism with `SafeCmd`. -/
+def checkCmd (a : Owner) (c : Cmd) (_s : FileState) (stdinPub : Bool) : Bool :=
+  match c with
+  -- read_ok / grep_ok / sort_ok / uniq_ok / wc_ok are all unconditional
+  | .read _ => true
+  | .grep _ => true
+  | .sort   => true
+  | .uniq   => true
+  | .wc     => true
+  | .write p _ =>
+      match classify p with
+      -- write_public_ok: needs CanWrite AND public-provenance stdin (`stdinPub`).
+      -- For `.append` the content written is `concatContent (s p) stdin`; since `p`
+      -- is publicRW its existing content is public-provenance, so the append obligation
+      -- reduces to exactly `stdinPub` -- the same check as `.overwrite`. (When
+      -- `s p = none`, `concatContent .empty stdin` reduces to `stdin`, same obligation.)
+      | .publicRW  => canWriteB a p && stdinPub
+      -- write_private_ok: CanWrite only, no provenance obligation
+      | .privateRW => canWriteB a p
+      -- read-only classes: NO write rule accepts them, so no write is ever safe
+      | .publicRO  => false
+      | .privateRO => false
+  | .rm p    => canWriteB a p
+  | .mkdir p => canWriteB a p
+
+/-- The lockstep decision walk. Returns `(isSafe, stdoutIsPublic)`, threading
+filesystem state and stdin EXACTLY as `evalPipelineFull` does. Public-ness is
+tracked FORWARD as provenance (`stdinPub`/`cmdOutIsPublic`), never by backward
+search. The `andThen`/`orElse` output-public flag is exit-aware (branches on
+stage 1's exit like the semantics), while the safety component checks both
+branches (v1 conservatism, matching `SafePipeline`).
+
+CONSEQUENCE (intended, load-bearing): `checkSafe`'s notion of "the content written"
+is DEFINED by `evalPipelineFull`, so its correctness is downstream of the
+semantics' fidelity — this project's central assumption. -/
+def checkFull (a : Owner) : Pipeline → FileState → Content → Bool → Bool × Bool
+  | .single c, s, _stdin, pub => (checkCmd a c s pub, cmdOutIsPublic c s pub)
+  -- `pipe` feeds stage 1's stdout into stage 2, and stage 2 is checked in the
+  -- state stage 1 left behind -- mirroring both the semantics and SafePipeline.
+  | .pipe p₁ p₂, s, stdin, pub =>
+      let (ok₁, pub₁) := checkFull a p₁ s stdin pub
+      let (s₁, out₁, _) := evalPipelineFull p₁ s stdin
+      let (ok₂, pub₂) := checkFull a p₂ s₁ out₁ pub₁
+      (ok₁ && ok₂, pub₂)
+  -- `;` gives stage 2 FRESH `.empty` stdin, which no constructor certifies as
+  -- public, so its stdin public-ness resets to `false`.
+  | .seq p₁ p₂, s, stdin, pub =>
+      let (ok₁, _) := checkFull a p₁ s stdin pub
+      let (s₁, _, _) := evalPipelineFull p₁ s stdin
+      let (ok₂, pub₂) := checkFull a p₂ s₁ .empty false
+      (ok₁ && ok₂, pub₂)
+  -- MATCHES SafePipeline's DELIBERATE v1 CONSERVATISM: both branches are checked
+  -- regardless of exit code, even though at runtime `&&` only runs `b` on success
+  -- and `||` only on failure. v1 does not short-circuit the SAFETY check; that
+  -- refinement needs ExitCode reasoning and is deferred.
+  | .andThen p₁ p₂, s, stdin, pub =>
+      let (ok₁, pub₁) := checkFull a p₁ s stdin pub
+      let (s₁, _, ec₁) := evalPipelineFull p₁ s stdin
+      let (ok₂, pub₂) := checkFull a p₂ s₁ .empty false
+      -- SAFETY: both branches safe AND public-guard: `p₁` touches only public PATHS
+      -- AND its incoming STDIN is public-provenance (`pub`) or `.empty` — closing the
+      -- guard-stdin channel; matches SafePipeline.andThen.
+      -- FAITHFUL output flag: `&&` runs stage 2 only on SUCCESS, so on failure the
+      -- pipeline's output — and its flag — is stage 1's.
+      (ok₁ && ok₂ && touchesOnlyPublic p₁ && (pub || decide (stdin = .empty)),
+       match ec₁ with | .success => pub₂ | .failure _ => pub₁)
+  | .orElse p₁ p₂, s, stdin, pub =>
+      let (ok₁, pub₁) := checkFull a p₁ s stdin pub
+      let (s₁, _, ec₁) := evalPipelineFull p₁ s stdin
+      let (ok₂, pub₂) := checkFull a p₂ s₁ .empty false
+      -- SAFETY: both branches safe AND public-guard (paths + stdin), as andThen.
+      -- FAITHFUL output flag (unchanged): `||` runs stage 2 only on FAILURE, so on
+      -- success the output — and its flag — is stage 1's.
+      (ok₁ && ok₂ && touchesOnlyPublic p₁ && (pub || decide (stdin = .empty)),
+       match ec₁ with | .success => pub₁ | .failure _ => pub₂)
+
+/-- The v1 prove-or-reject gate's decision: `true` iff the pipeline is provably
+safe. A whole pipeline starts with `.empty` stdin (nothing piped from a terminal),
+not certified public — hence the initial `false`. Proved sound by `checkSafe_sound`
+(soundness only; completeness is intentionally not claimed). -/
+def checkSafe (a : Owner) (p : Pipeline) (s : FileState) : Bool :=
+  (checkFull a p s .empty false).1
+
+/-! ## Soundness
+
+Soundness only: `checkSafe = true → SafePipeline`. Completeness (the converse) is
+intentionally NOT claimed and is known to be unattainable -- the forward
+provenance walk rejects some genuinely-safe pipelines. -/
+
+/-- `canWriteB` is sound: if it returns `true`, `CanWrite` holds (v1: `self` is the
+only constructor). -/
+theorem canWriteB_sound {a : Owner} {p : Path} : canWriteB a p = true → CanWrite a p := by
+  intro h
+  exact CanWrite.self a p (of_decide_eq_true h)
+
+/-- The soundness bridge, by induction mirroring the decider's walk. Two facts are
+threaded together (the second feeds the first in `pipe`):
+- (safety) the safety flag implies a `SafePipeline` derivation, THREADING the same
+  provenance flag `pub` that the spec now consumes;
+- (prov)   the decider's output flag equals `provOut` — so the flag `checkFull`
+  threads into the next stage is exactly the one `SafePipeline` expects.
+
+The write obligation is the checkable `pub = true` (no value-predicate
+reconstruction), because spec and decider share the same forward-provenance notion. -/
+theorem checkFull_sound (a : Owner) (p : Pipeline) :
+    ∀ (s : FileState) (stdin : Content) (pub : Bool),
+      ((checkFull a p s stdin pub).1 = true → SafePipeline a p s stdin pub) ∧
+      ((checkFull a p s stdin pub).2 = provOut p s stdin pub) := by
+  induction p with
+  | single c =>
+    intro s stdin pub
+    refine ⟨?_, ?_⟩
+    · intro hok
+      apply SafePipeline.single
+      simp only [checkFull] at hok
+      cases c with
+      | read q => exact SafeCmd.read_ok a q s stdin pub
+      | grep pat => exact SafeCmd.grep_ok a pat s stdin pub
+      | sort => exact SafeCmd.sort_ok a s stdin pub
+      | uniq => exact SafeCmd.uniq_ok a s stdin pub
+      | wc => exact SafeCmd.wc_ok a s stdin pub
+      | write q mode =>
+        simp only [checkCmd] at hok
+        split at hok
+        · rename_i hcls
+          rw [Bool.and_eq_true] at hok
+          exact SafeCmd.write_public_ok a q mode s stdin pub hcls (canWriteB_sound hok.1) hok.2
+        · rename_i hcls
+          exact SafeCmd.write_private_ok a q mode s stdin pub hcls (canWriteB_sound hok)
+        · simp at hok
+        · simp at hok
+      | rm q => simp only [checkCmd] at hok; exact SafeCmd.rm_ok a q s stdin pub (canWriteB_sound hok)
+      | mkdir q => simp only [checkCmd] at hok; exact SafeCmd.mkdir_ok a q s stdin pub (canWriteB_sound hok)
+    · rfl
+  | pipe p₁ p₂ ih₁ ih₂ =>
+    intro s stdin pub
+    rcases h1 : checkFull a p₁ s stdin pub with ⟨ok₁, pub₁⟩
+    rcases he1 : evalPipelineFull p₁ s stdin with ⟨s₁, out₁, ec₁⟩
+    rcases h2 : checkFull a p₂ s₁ out₁ pub₁ with ⟨ok₂, pub₂⟩
+    obtain ⟨H1safe, H1eq⟩ := ih₁ s stdin pub
+    rw [h1] at H1safe H1eq
+    obtain ⟨H2safe, H2eq⟩ := ih₂ s₁ out₁ pub₁
+    rw [h2] at H2safe H2eq
+    have hcf : checkFull a (.pipe p₁ p₂) s stdin pub = (ok₁ && ok₂, pub₂) := by
+      simp only [checkFull, h1, he1, h2]
+    refine ⟨?_, ?_⟩
+    · simp only [hcf]; intro hok
+      rw [Bool.and_eq_true] at hok
+      refine SafePipeline.pipe a p₁ p₂ s stdin pub (H1safe hok.1) ?_
+      rw [he1, ← H1eq]; exact H2safe hok.2
+    · -- restate the flag equations at their reduced (defeq) types so `simp` matches
+      have e1 : pub₁ = provOut p₁ s stdin pub := H1eq
+      have e2 : pub₂ = provOut p₂ s₁ out₁ pub₁ := H2eq
+      simp only [hcf, e2, provOut, he1, e1]
+  | seq p₁ p₂ ih₁ ih₂ =>
+    intro s stdin pub
+    rcases h1 : checkFull a p₁ s stdin pub with ⟨ok₁, pub₁⟩
+    rcases he1 : evalPipelineFull p₁ s stdin with ⟨s₁, out₁, ec₁⟩
+    rcases h2 : checkFull a p₂ s₁ .empty false with ⟨ok₂, pub₂⟩
+    obtain ⟨H1safe, _⟩ := ih₁ s stdin pub
+    rw [h1] at H1safe
+    obtain ⟨H2safe, H2eq⟩ := ih₂ s₁ .empty false
+    rw [h2] at H2safe H2eq
+    have hcf : checkFull a (.seq p₁ p₂) s stdin pub = (ok₁ && ok₂, pub₂) := by
+      simp only [checkFull, h1, he1, h2]
+    refine ⟨?_, ?_⟩
+    · simp only [hcf]; intro hok
+      rw [Bool.and_eq_true] at hok
+      refine SafePipeline.seq a p₁ p₂ s stdin pub (H1safe hok.1) ?_
+      rw [he1]; exact H2safe hok.2
+    · simp only [hcf, H2eq, provOut, he1]
+  | andThen p₁ p₂ ih₁ ih₂ =>
+    intro s stdin pub
+    rcases h1 : checkFull a p₁ s stdin pub with ⟨ok₁, pub₁⟩
+    rcases he1 : evalPipelineFull p₁ s stdin with ⟨s₁, out₁, ec₁⟩
+    rcases h2 : checkFull a p₂ s₁ .empty false with ⟨ok₂, pub₂⟩
+    obtain ⟨H1safe, H1eq⟩ := ih₁ s stdin pub
+    rw [h1] at H1safe H1eq
+    obtain ⟨H2safe, H2eq⟩ := ih₂ s₁ .empty false
+    rw [h2] at H2safe H2eq
+    -- case on stage-1 exit so the exit-aware `.2` match resolves concretely
+    cases ec₁ with
+    | success =>
+      have hcf : checkFull a (.andThen p₁ p₂) s stdin pub
+               = (ok₁ && ok₂ && touchesOnlyPublic p₁ && (pub || decide (stdin = .empty)), pub₂) := by
+        simp only [checkFull, h1, he1, h2]
+      refine ⟨?_, ?_⟩
+      · simp only [hcf]; intro hok
+        simp only [Bool.and_eq_true] at hok
+        obtain ⟨⟨⟨h_ok1, h_ok2⟩, h_g⟩, h_sd⟩ := hok
+        rw [Bool.or_eq_true] at h_sd
+        refine SafePipeline.andThen a p₁ p₂ s stdin pub h_g (h_sd.imp id of_decide_eq_true)
+          (H1safe h_ok1) ?_
+        rw [he1]; exact H2safe h_ok2
+      · simp only [hcf, provOut, he1]; exact H2eq
+    | failure n =>
+      have hcf : checkFull a (.andThen p₁ p₂) s stdin pub
+               = (ok₁ && ok₂ && touchesOnlyPublic p₁ && (pub || decide (stdin = .empty)), pub₁) := by
+        simp only [checkFull, h1, he1, h2]
+      refine ⟨?_, ?_⟩
+      · simp only [hcf]; intro hok
+        simp only [Bool.and_eq_true] at hok
+        obtain ⟨⟨⟨h_ok1, h_ok2⟩, h_g⟩, h_sd⟩ := hok
+        rw [Bool.or_eq_true] at h_sd
+        refine SafePipeline.andThen a p₁ p₂ s stdin pub h_g (h_sd.imp id of_decide_eq_true)
+          (H1safe h_ok1) ?_
+        rw [he1]; exact H2safe h_ok2
+      · simp only [hcf, provOut, he1]; exact H1eq
+  | orElse p₁ p₂ ih₁ ih₂ =>
+    intro s stdin pub
+    rcases h1 : checkFull a p₁ s stdin pub with ⟨ok₁, pub₁⟩
+    rcases he1 : evalPipelineFull p₁ s stdin with ⟨s₁, out₁, ec₁⟩
+    rcases h2 : checkFull a p₂ s₁ .empty false with ⟨ok₂, pub₂⟩
+    obtain ⟨H1safe, H1eq⟩ := ih₁ s stdin pub
+    rw [h1] at H1safe H1eq
+    obtain ⟨H2safe, H2eq⟩ := ih₂ s₁ .empty false
+    rw [h2] at H2safe H2eq
+    cases ec₁ with
+    | success =>
+      have hcf : checkFull a (.orElse p₁ p₂) s stdin pub
+               = (ok₁ && ok₂ && touchesOnlyPublic p₁ && (pub || decide (stdin = .empty)), pub₁) := by
+        simp only [checkFull, h1, he1, h2]
+      refine ⟨?_, ?_⟩
+      · simp only [hcf]; intro hok
+        simp only [Bool.and_eq_true] at hok
+        obtain ⟨⟨⟨h_ok1, h_ok2⟩, h_g⟩, h_sd⟩ := hok
+        rw [Bool.or_eq_true] at h_sd
+        refine SafePipeline.orElse a p₁ p₂ s stdin pub h_g (h_sd.imp id of_decide_eq_true)
+          (H1safe h_ok1) ?_
+        rw [he1]; exact H2safe h_ok2
+      · simp only [hcf, provOut, he1]; exact H1eq
+    | failure n =>
+      have hcf : checkFull a (.orElse p₁ p₂) s stdin pub
+               = (ok₁ && ok₂ && touchesOnlyPublic p₁ && (pub || decide (stdin = .empty)), pub₂) := by
+        simp only [checkFull, h1, he1, h2]
+      refine ⟨?_, ?_⟩
+      · simp only [hcf]; intro hok
+        simp only [Bool.and_eq_true] at hok
+        obtain ⟨⟨⟨h_ok1, h_ok2⟩, h_g⟩, h_sd⟩ := hok
+        rw [Bool.or_eq_true] at h_sd
+        refine SafePipeline.orElse a p₁ p₂ s stdin pub h_g (h_sd.imp id of_decide_eq_true)
+          (H1safe h_ok1) ?_
+        rw [he1]; exact H2safe h_ok2
+      · simp only [hcf, provOut, he1]; exact H2eq
+
+/-- SOUNDNESS of the gate: if `checkSafe` permits, the pipeline really is
+`SafePipeline` (indexed by `.empty` top-level stdin, matching how `checkSafe` and
+`evalPipeline` start). This is the theorem that makes a permit verdict meaningful.
+
+Completeness (`SafePipeline → checkSafe = true`) is intentionally NOT claimed and
+is unattainable in general — v1 may reject some genuinely-safe pipelines (an
+accepted, deliberate limitation). -/
+theorem checkSafe_sound (a : Owner) (p : Pipeline) (s : FileState) :
+    checkSafe a p s = true → SafePipeline a p s .empty false := by
+  intro h
+  -- top-level stdin is `.empty` with provenance flag `false`
+  exact (checkFull_sound a p s .empty false).1 h
diff --git a/ShellWall/Fidelity.lean b/ShellWall/Fidelity.lean
new file mode 100644
index 0000000..5d33c9b
--- /dev/null
+++ b/ShellWall/Fidelity.lean
@@ -0,0 +1,337 @@
+import ShellWall
+open System
+
+/-! # Fidelity harness
+
+The first code that runs REAL bash, to validate `evalPipelineFull` against actual
+shell behavior. This module is IO/impure tooling: it is NOT imported by the
+verified core (`ShellWall.lean`), and `lake build` never runs it. It is driven by
+the `fidelity` executable (`lake exe fidelity`).
+
+All real execution is sandboxed to a fresh temp directory — never real paths.
+
+Windows note: bare `bash` often resolves to the WSL launcher
+(`C:\Windows\System32\bash.exe`), which on this class of machine may be broken or
+do path translation. `detectShell` therefore probes candidates (Git Bash first)
+and only uses one that echoes a sentinel correctly. -/
+
+namespace ShellWall.Fidelity
+
+/-! ## Executor -/
+
+/-- Captured result of running a real shell command. -/
+structure ShellResult where
+  stdout   : String
+  exitCode : Nat
+  deriving Repr, Inhabited
+
+/-- Candidate shells, in preference order. Git Bash full paths first (most
+POSIX-faithful here); bare `bash` last (it may be the WSL launcher). -/
+def shellCandidates : List String :=
+  [ "C:/Program Files/Git/usr/bin/bash.exe",
+    "C:/Program Files/Git/bin/bash.exe",
+    "/usr/bin/bash",
+    "sh",
+    "bash" ]
+
+/-- Probe a shell: it must run and echo a sentinel exactly (guards against a
+spawnable-but-broken shell, e.g. a misconfigured WSL). -/
+def probeShell (sh : String) : IO Bool := do
+  try
+    let out ← IO.Process.output { cmd := sh, args := #["-c", "printf __sw_ok__"] }
+    let clean := (out.stdout.replace "\n" "").replace "\r" ""
+    return out.exitCode == 0 && clean == "__sw_ok__"
+  catch _ => return false
+
+/-- The first working shell from `shellCandidates`, or `none` if none work. -/
+def detectShell : IO (Option String) := do
+  for c in shellCandidates do
+    if (← probeShell c) then return (some c)
+  return none
+
+/-- Run `command` in `shell` with working directory `cwd`, capturing stdout and
+exit code. stderr is captured but discarded (the model has no stderr channel). -/
+def runBash (shell command : String) (cwd : FilePath) : IO ShellResult := do
+  let out ← IO.Process.output { cmd := shell, args := #["-c", command], cwd := some cwd }
+  return { stdout := out.stdout, exitCode := out.exitCode.toNat }
+
+/-! ## Renderer (`Pipeline → String`)
+
+The easy direction: a structured term to its bash string. NOT a parser. Each
+command renders to the bash it is SUPPOSED to model, so the fidelity test checks
+the model's actual claim (e.g. `grep -F`, `LC_ALL=C sort`), not a stricter one. -/
+
+/-- Single-quote for POSIX sh, escaping embedded single quotes. -/
+def shq (s : String) : String :=
+  "'" ++ s.replace "'" "'\\''" ++ "'"
+
+/-- Model path → sandbox-relative path (drops the leading `/`; normalizes `\`). -/
+def relPath (p : Path) : String :=
+  let s := p.toString.replace "\\" "/"
+  if s.startsWith "/" then String.ofList (s.toList.drop 1) else s
+
+/-- Render one command to bash. Fidelity choices are commented. -/
+def renderCmd : Cmd → String
+  | .read p             => "cat " ++ shq (relPath p)
+  -- write consumes stdin and emits no stdout: `cat > f` / `cat >> f` (NOT `tee`,
+  -- which would also echo to stdout).
+  | .write p .overwrite => "cat > " ++ shq (relPath p)
+  | .write p .append    => "cat >> " ++ shq (relPath p)
+  -- FIDELITY: model grep is literal-substring, so render `grep -F` (not BRE). `-e`
+  -- gives the pattern explicitly (handles empty / leading-dash patterns).
+  | .grep pat           => "grep -F -e " ++ shq pat
+  -- FIDELITY: model sorts by Unicode codepoint (C locale); render `LC_ALL=C sort`
+  -- so bash matches the model's claim, not a locale-dependent order.
+  | .sort               => "LC_ALL=C sort"
+  | .uniq               => "uniq"
+  | .wc                 => "wc"
+  | .rm p               => "rm " ++ shq (relPath p)
+  | .mkdir p            => "mkdir " ++ shq (relPath p)
+
+-- Render a whole pipeline, parenthesizing compound operands so bash operator
+-- precedence matches the model's binary-tree structure. `partial` because the
+-- `renderChild p → renderPipeline p` step is not structural; this is runtime
+-- tooling, not proof-bearing (the verified core is `partial`-free).
+mutual
+  /-- Render a whole pipeline to its bash string (see the note above the block). -/
+  partial def renderPipeline : Pipeline → String
+    | .single c    => renderCmd c
+    | .pipe a b    => renderChild a ++ " | "  ++ renderChild b
+    | .seq a b     => renderChild a ++ " ; "  ++ renderChild b
+    | .andThen a b => renderChild a ++ " && " ++ renderChild b
+    | .orElse a b  => renderChild a ++ " || " ++ renderChild b
+  /-- A pipeline as a sub-expression: bare if single, parenthesized if compound. -/
+  partial def renderChild : Pipeline → String
+    | .single c => renderCmd c
+    | p         => "( " ++ renderPipeline p ++ " )"
+end
+
+/-! ## Model helpers -/
+
+/-- Best-effort `Content` → `String` for comparing model output to bash stdout. -/
+def contentToString : Content → String
+  | .text s   => s
+  | .empty    => ""
+  | .binary b => (String.fromUTF8? b).getD ""
+
+/-- `ExitCode` → the numeric exit status bash would report. -/
+def exitToNat : ExitCode → Nat
+  | .success   => 0
+  | .failure n => n
+
+/-- The empty filesystem (stream ops never consult it). -/
+def emptyState : FileState := fun _ => none
+
+/-- Digit-runs of a string, as `Nat`s — for comparing `wc`'s numbers while ignoring
+its spacing. (Manual fold to avoid the in-flux `String.split` iterator API.) -/
+def numbersOf (s : String) : List Nat :=
+  let rec go : List Char → String → List Nat → List Nat
+    | [],      cur, acc => if cur.isEmpty then acc else acc ++ [cur.toNat?.getD 0]
+    | c :: cs, cur, acc =>
+        if c.isDigit then go cs (cur.push c) acc
+        else go cs "" (if cur.isEmpty then acc else acc ++ [cur.toNat?.getD 0])
+  go s.toList "" []
+
+/-! ## Tier 1: stream fidelity (stdin → stdout, no filesystem) -/
+
+/-- Whether a corpus case is expected to agree with bash, or to diverge on purpose. -/
+inductive FidelityExpectation
+  /-- Model MUST agree with bash; a mismatch is a real fidelity bug. -/
+  | shouldMatch
+  /-- Model deliberately differs; the reason records how. -/
+  | knownDivergence (reason : String)
+
+/-- A Tier 1 case: feed `input` as stdin to `pipeline`, compare model vs bash. -/
+structure StreamCase where
+  name     : String
+  input    : Content
+  pipeline : Pipeline
+  expect   : FidelityExpectation
+  /-- Naive bash to demonstrate a divergence (e.g. default `grep`/`sort`/`wc`
+  instead of the faithful render). When `none`, the faithful render is used. -/
+  bashOverride : Option String := none
+
+/-- Escape newlines for one-line reporting. -/
+def vis (s : String) : String := s.replace "\n" "\\n"
+
+/-- Run one Tier 1 case and return a report line. -/
+def runStreamCase (shell : String) (sandbox : FilePath) (c : StreamCase) : IO String := do
+  let (_, outC, ec) := evalPipelineFull c.pipeline emptyState c.input
+  let modelOut  := contentToString outC
+  let modelExit := exitToNat ec
+  IO.FS.writeBinFile (sandbox / "__stdin") (contentBytes c.input)
+  let body := c.bashOverride.getD (renderPipeline c.pipeline)
+  let r ← runBash shell ("{ " ++ body ++ " ; } < __stdin") sandbox
+  let outMatch  := modelOut == r.stdout
+  let exitMatch := modelExit == r.exitCode
+  let full := outMatch && exitMatch
+  let detail := s!"model(out={vis modelOut} exit={modelExit}) bash(out={vis r.stdout} exit={r.exitCode})"
+  match c.expect with
+  | .shouldMatch =>
+      if full then
+        return s!"  [PASS ] {c.name}"
+      else
+        return s!"  [❌BUG] {c.name} — shouldMatch but DIFFERS: {detail}"
+  | .knownDivergence reason =>
+      let numsMatch := numbersOf modelOut == numbersOf r.stdout
+      if full then
+        return s!"  [SURPRISE-MATCH] {c.name} — expected divergence ({reason}) but agrees: {detail}"
+      else
+        let hasNums := !(numbersOf modelOut).isEmpty
+        let nums := if hasNums && numsMatch then " (numbers agree)" else ""
+        return s!"  [diverges✓] {c.name} — as documented: {reason}{nums}"
+
+/-- The Tier 1 corpus: every `FIDELITY:` note turned into a case. -/
+def streamCorpus : List StreamCase :=
+  [ -- shouldMatch
+    { name := "uniq adjacent-only (b a b unchanged)", input := .text "b\na\nb\n",
+      pipeline := .single .uniq, expect := .shouldMatch },
+    { name := "sort | uniq full dedup", input := .text "b\na\nb\n",
+      pipeline := .pipe (.single .sort) (.single .uniq), expect := .shouldMatch },
+    { name := "grep substring present → exit 0", input := .text "abc\nxyz\n",
+      pipeline := .single (.grep "bc"), expect := .shouldMatch },
+    { name := "grep substring absent → exit 1", input := .text "abc\n",
+      pipeline := .single (.grep "zzz"), expect := .shouldMatch },
+    { name := "grep empty pattern matches all", input := .text "x\ny\n",
+      pipeline := .single (.grep ""), expect := .shouldMatch },
+    { name := "sort orders lines", input := .text "banana\napple\ncherry\n",
+      pipeline := .single .sort, expect := .shouldMatch },
+    { name := "sort adds trailing newline (unterminated input)", input := .text "a\nb",
+      pipeline := .single .sort, expect := .shouldMatch },
+    { name := "empty input → empty output", input := .empty,
+      pipeline := .single .sort, expect := .shouldMatch },
+    -- knownDivergence
+    { name := "grep 'a.c' on abc", input := .text "abc\n",
+      pipeline := .single (.grep "a.c"),
+      expect := .knownDivergence "model is grep -F (substring), not BRE regex",
+      bashOverride := some "grep -e 'a.c'" },
+    { name := "wc output format (file-redirect stdin)", input := .text "a b c\n",
+      pipeline := .single .wc,
+      expect := .knownDivergence "model emits 'L W B' single-spaced; real wc right-aligns (+ filename)",
+      bashOverride := some "wc" },
+    { name := "wc output format (pipe stdin)", input := .text "a b c\n",
+      pipeline := .single .wc,
+      expect := .knownDivergence "GNU wc pads to width 7 when reading a non-seekable pipe; model is single-spaced",
+      bashOverride := some "cat | wc" },
+    { name := "sort mixed-case locale", input := .text "B\na\nA\nb\n",
+      pipeline := .single .sort,
+      expect := .knownDivergence "model is codepoint/C-locale; real sort is locale-dependent",
+      bashOverride := some "sort" } ]
+
+/-! ## Tier 2: filesystem fidelity (proof-of-concept only) -/
+
+/-- A Tier 2 case: materialize `initFiles`, run `pipeline` in the sandbox, and
+compare the resulting files at `checkPaths` to `evalPipelineFull`'s prediction. -/
+structure FsCase where
+  name       : String
+  initFiles  : List (Path × Content)
+  pipeline   : Pipeline
+  checkPaths : List Path
+
+/-- The model filesystem seeded from an explicit file list. -/
+def stateOf (files : List (Path × Content)) : FileState :=
+  fun p => (files.find? (fun x => decide (x.1 = p))).map (·.2)
+
+/-- Write a model file to disk under `base`, creating parent directories. -/
+def writeModelFile (base : FilePath) (p : Path) (c : Content) : IO Unit := do
+  let full := base / relPath p
+  match full.parent with
+  | some d => IO.FS.createDirAll d
+  | none   => pure ()
+  IO.FS.writeBinFile full (contentBytes c)
+
+/-- Ensure the parent directory of a model path exists under `base`. -/
+def ensureParent (base : FilePath) (p : Path) : IO Unit := do
+  match (base / relPath p).parent with
+  | some d => IO.FS.createDirAll d
+  | none   => pure ()
+
+/-- Read a model file back from disk (as text), or `none` if absent. -/
+def readModelFile (base : FilePath) (p : Path) : IO (Option Content) := do
+  let full := base / relPath p
+  if (← full.pathExists) then return some (.text (← IO.FS.readFile full))
+  else return none
+
+/-- Structural comparison of a predicted vs actual file (by string content). -/
+def sameContent : Option Content → Option Content → Bool
+  | none,   none   => true
+  | some a, some b => contentToString a == contentToString b
+  | _,      _      => false
+
+/-- Run one Tier 2 case in a fresh sub-sandbox; return a report line. -/
+def runFsCase (shell : String) (sandbox : FilePath) (idx : Nat) (c : FsCase) : IO String := do
+  let sub := sandbox / s!"fs{idx}"
+  IO.FS.createDirAll sub
+  -- materialize starting state + ensure write-target parents exist
+  for (p, cont) in c.initFiles do writeModelFile sub p cont
+  for p in c.checkPaths do ensureParent sub p
+  -- run real bash
+  let _ ← runBash shell (renderPipeline c.pipeline) sub
+  -- model prediction
+  let predicted := (evalPipelineFull c.pipeline (stateOf c.initFiles) .empty).1
+  -- compare each checked path
+  let mut allOk := true
+  let mut parts : List String := []
+  for p in c.checkPaths do
+    let actual ← readModelFile sub p
+    let pred := predicted p
+    let ok := sameContent pred actual
+    allOk := allOk && ok
+    let mark := if ok then "ok" else "MISMATCH"
+    parts := parts ++ [s!"{relPath p}:{mark}"]
+  let tag := if allOk then "[PASS ]" else "[❌BUG]"
+  let joined := String.intercalate ", " parts
+  return s!"  {tag} {c.name} — {joined}"
+
+/-- The Tier 2 corpus (small proof-of-concept). -/
+def fsCorpus : List FsCase :=
+  [ { name := "simple write (cat shared > pub)",
+      initFiles := [("/shared/ref.txt", .text "PUBDATA\n")],
+      pipeline := .pipe (.single (.read "/shared/ref.txt"))
+                        (.single (.write "/home/alice/public/out.txt" .overwrite)),
+      checkPaths := ["/home/alice/public/out.txt"] },
+    { name := "append (cat shared >> pub, existing)",
+      initFiles := [("/shared/ref.txt", .text "PUB\n"),
+                    ("/home/alice/public/out.txt", .text "existing\n")],
+      pipeline := .pipe (.single (.read "/shared/ref.txt"))
+                        (.single (.write "/home/alice/public/out.txt" .append)),
+      checkPaths := ["/home/alice/public/out.txt"] },
+    { name := "rm (remove an existing file)",
+      initFiles := [("/home/alice/notes.txt", .text "SECRET\n")],
+      pipeline := .single (.rm "/home/alice/notes.txt"),
+      checkPaths := ["/home/alice/notes.txt"] },
+    { name := "read | write chain (cat notes > notes2)",
+      initFiles := [("/home/alice/notes.txt", .text "SECRET\n")],
+      pipeline := .pipe (.single (.read "/home/alice/notes.txt"))
+                        (.single (.write "/home/alice/notes2.txt" .overwrite)),
+      checkPaths := ["/home/alice/notes2.txt"] } ]
+
+/-! ## Driver -/
+
+/-- Run the whole fidelity harness: detect a shell, run Tier 1 then Tier 2 in a
+temp sandbox, print a fidelity map, and clean up. Fails gracefully if no shell. -/
+def runFidelity : IO Unit := do
+  IO.println "=== ShellWall fidelity harness ==="
+  match ← detectShell with
+  | none =>
+      let tried := String.intercalate ", " shellCandidates
+      IO.println s!"no bash found (tried: {tried})."
+      IO.println "Skipping fidelity checks; the build and proofs are unaffected."
+  | some shell =>
+      IO.println s!"shell: {shell}"
+      let sandbox ← IO.FS.createTempDir
+      try
+        IO.println "\n-- Tier 1: stream ops (model vs real bash) --"
+        for c in streamCorpus do IO.println (← runStreamCase shell sandbox c)
+        IO.println "\n-- Tier 2: filesystem (proof-of-concept) --"
+        let mut i := 0
+        for c in fsCorpus do
+          IO.println (← runFsCase shell sandbox i c)
+          i := i + 1
+      finally
+        try IO.FS.removeDirAll sandbox catch _ => pure ()
+      IO.println "\nNote: comprehensive Tier 2 differential testing (all commands, all"
+      IO.println "path classes, mkdir/directory semantics) is future work — the model's"
+      IO.println "no-directory gap in particular is expected to surface there."
+
+end ShellWall.Fidelity
diff --git a/ShellWall/Gate.lean b/ShellWall/Gate.lean
new file mode 100644
index 0000000..f29e0f6
--- /dev/null
+++ b/ShellWall/Gate.lean
@@ -0,0 +1,17 @@
+import ShellWall.Decide
+
+/-- The gate's outward result: allow the pipeline, or reject it with a reason. -/
+inductive Verdict where
+  /-- The pipeline is permitted to run. -/
+  | permit
+  /-- The pipeline is rejected, with a human-readable diagnostic. -/
+  | reject (reason : String)
+
+/-- The top-level v1 entry point: prove-or-reject. Returns `.permit` iff `checkSafe`
+returns `true`, else `.reject` with a diagnostic reason.
+
+A `.permit` verdict is backed by `checkSafe_sound`: permit ⇒ the pipeline satisfies
+`SafePipeline`. A `.reject` may be conservative — completeness is not claimed, so
+some genuinely-safe pipelines are rejected (an accepted v1 limitation). -/
+def gate (a : Owner) (p : Pipeline) (s : FileState) : Verdict :=
+  if checkSafe a p s then .permit else .reject "checkSafe: no safety proof found"
diff --git a/ShellWall/Parser.lean b/ShellWall/Parser.lean
new file mode 100644
index 0000000..425f838
--- /dev/null
+++ b/ShellWall/Parser.lean
@@ -0,0 +1,208 @@
+import ShellWall
+open System
+
+/-! # bash → `Pipeline` parser (UNVERIFIED tooling)
+
+Parses the closed fragment the model supports into a `Pipeline` term. This sits
+ENTIRELY UPSTREAM of the verified core — it is not imported by any spec/decider/
+proof module, and a parse bug can only produce the wrong `Pipeline` (which the CLI
+always echoes before gating), never affect a proof.
+
+DENY-BY-DEFAULT: anything outside the fragment ($(...), variables, globs, quotes we
+don't handle, `<`, unknown commands/flags, background `&`) is REJECTED with a
+message — never coerced into a nearest in-fragment term. This is a security
+property: silently approximating an out-of-fragment command would gate the wrong
+thing.
+
+Supported grammar (bash precedence: `|` tightest, then `&&`/`||`, then `;`; all
+left-associative):
+```
+  seq     := andor (';' andor)*
+  andor   := pipe (('&&' | '||') pipe)*
+  pipe    := elem ('|' elem)*
+  elem    := ( '(' seq ')' | simpleCmd ) redirect?
+  simpleCmd:
+    cat <path>            → read
+    grep [-F] [-e] <pat>  → grep      (model grep is substring; -F and -e accepted)
+    [LC_ALL=C] sort       → sort
+    uniq | wc
+    rm <path> | mkdir <path>
+    cat                   → (bare) identity; only valid with a redirect ⇒ write
+  redirect := ('>' | '>>') <path>     → wraps the element in a write stage
+```
+`partial` (unverified tooling); it is total in practice on finite input. -/
+
+namespace ShellWall.Parser
+
+/-- A path word → `Path`. -/
+private def toPath (w : String) : Path := ⟨w⟩
+
+/-! ## Tokenizer -/
+
+inductive Tok
+  | word (s : String)
+  | pipe | seq | andOp | orOp | gt | gtgt | lp | rp
+  deriving Repr, BEq
+
+private def isDelim (c : Char) : Bool :=
+  c == ' ' || c == '\t' || c == '|' || c == '&' || c == ';' ||
+  c == '>' || c == '<' || c == '(' || c == ')'
+
+-- PARSE-FIDELITY: these unquoted characters trigger bash EXPANSION/GLOBBING, which
+-- the model cannot represent. We reject rather than parse them literally — matching
+-- bash would require implementing expansion, and a literal reading would be wrong.
+private def isForbidden (c : Char) : Bool :=
+  c == '$' || c == '`' || c == '"' || c == '*' || c == '?' ||
+  c == '[' || c == ']' || c == '{' || c == '}' || c == '~' || c == '!' || c == '\\'
+
+/-- Read the interior of a single-quoted string (up to the closing quote). shq-style
+`'\''` escaping is handled by `readWord` concatenating adjacent segments. -/
+private partial def readQuoted : List Char → String → Except String (String × List Char)
+  | [], _ => .error "unterminated single quote"
+  | c :: rest, acc => if c == '\'' then .ok (acc, rest) else readQuoted rest (acc.push c)
+
+/-- Read one word (bash tokenization): unquoted chars, `'...'` segments, and `\c`
+escapes, all concatenated until a delimiter. Rejects forbidden unquoted chars. -/
+private partial def readWord : List Char → String → Except String (String × List Char)
+  | [], acc => .ok (acc, [])
+  | c :: rest, acc =>
+    if c == '\'' then
+      match readQuoted rest "" with
+      | .error e => .error e
+      | .ok (inner, rest2) => readWord rest2 (acc ++ inner)
+    else if isDelim c then .ok (acc, c :: rest)
+    else if isForbidden c then
+      .error s!"out-of-fragment character '{c}' (shell expansion/glob not supported)"
+    else readWord rest (acc.push c)
+
+private partial def tokenize : List Char → Except String (List Tok)
+  | [] => .ok []
+  | c :: rest =>
+    if c == ' ' || c == '\t' then tokenize rest
+    else if c == '|' then
+      match rest with
+      | '|' :: r => (tokenize r).map (Tok.orOp :: ·)
+      | _ => (tokenize rest).map (Tok.pipe :: ·)
+    else if c == '&' then
+      match rest with
+      | '&' :: r => (tokenize r).map (Tok.andOp :: ·)
+      | _ => .error "single '&' (background execution) not supported"
+    else if c == ';' then (tokenize rest).map (Tok.seq :: ·)
+    else if c == '>' then
+      match rest with
+      | '>' :: r => (tokenize r).map (Tok.gtgt :: ·)
+      | _ => (tokenize rest).map (Tok.gt :: ·)
+    else if c == '<' then .error "input redirection '<' not supported"
+    else if c == '(' then (tokenize rest).map (Tok.lp :: ·)
+    else if c == ')' then (tokenize rest).map (Tok.rp :: ·)
+    else
+      match readWord (c :: rest) "" with
+      | .error e => .error e
+      | .ok (w, rest2) =>
+        if w.isEmpty then tokenize rest2 else (tokenize rest2).map (Tok.word w :: ·)
+
+/-! ## Command mapping -/
+
+/-- What a simple command's words denote before a possible redirect. -/
+private inductive Base
+  | cmd (c : Cmd)     -- a concrete command
+  | bareCat           -- `cat` with no file: identity, only valid with a redirect
+  | group (p : Pipeline)  -- a parenthesized sub-pipeline
+
+/-- Parse a `grep`'s flags/pattern: `[-F] [-e] <pat>`, exactly one pattern. -/
+private def parseGrep : List String → Except String Cmd
+  | [] => .error "grep: missing pattern"
+  | "-F" :: rest => parseGrep rest
+  | "-e" :: pat :: [] => .ok (.grep pat)
+  | "-e" :: _ => .error "grep: -e expects exactly one pattern"
+  | pat :: [] =>
+      if pat.startsWith "-" then .error s!"grep: unsupported flag '{pat}'"
+      else .ok (.grep pat)
+  | _ => .error "grep: only a single literal pattern is supported"
+
+/-- Map a simple command's words to a `Base`. -/
+private def wordsToBase : List String → Except String Base
+  | ["cat"] => .ok .bareCat
+  | ["cat", p] => .ok (.cmd (.read (toPath p)))
+  | "grep" :: rest => (parseGrep rest).map .cmd
+  | ["sort"] => .ok (.cmd .sort)
+  | ["LC_ALL=C", "sort"] => .ok (.cmd .sort)   -- the renderer's C-locale form
+  | ["uniq"] => .ok (.cmd .uniq)
+  | ["wc"] => .ok (.cmd .wc)
+  | ["rm", p] => .ok (.cmd (.rm (toPath p)))
+  | ["mkdir", p] => .ok (.cmd (.mkdir (toPath p)))
+  | [] => .error "empty command"
+  | ws => .error ("unsupported command: " ++ String.intercalate " " ws)
+
+/-- Apply an optional redirect to a base, yielding a `Pipeline`. -/
+private def applyRedirect : Base → Option (WriteMode × String) → Except String Pipeline
+  | .bareCat, some (m, p) => .ok (.single (.write (toPath p) m))
+  | .bareCat, none => .error "bare 'cat' with no file and no redirect is not representable"
+  | .cmd c, none => .ok (.single c)
+  | .cmd c, some (m, p) => .ok (.pipe (.single c) (.single (.write (toPath p) m)))
+  | .group g, none => .ok g
+  | .group g, some (m, p) => .ok (.pipe g (.single (.write (toPath p) m)))
+
+/-! ## Recursive-descent parser -/
+
+mutual
+  private partial def parseSeq (ts : List Tok) : Except String (Pipeline × List Tok) := do
+    let (l, ts) ← parseAndOr ts
+    parseSeqTail l ts
+  private partial def parseSeqTail (l : Pipeline) : List Tok → Except String (Pipeline × List Tok)
+    | .seq :: [] => .ok (l, [])            -- trailing `;` is allowed
+    | .seq :: ts => do let (r, ts) ← parseAndOr ts; parseSeqTail (.seq l r) ts
+    | ts => .ok (l, ts)
+
+  private partial def parseAndOr (ts : List Tok) : Except String (Pipeline × List Tok) := do
+    let (l, ts) ← parsePipe ts
+    parseAndOrTail l ts
+  private partial def parseAndOrTail (l : Pipeline) : List Tok → Except String (Pipeline × List Tok)
+    | .andOp :: ts => do let (r, ts) ← parsePipe ts; parseAndOrTail (.andThen l r) ts
+    | .orOp :: ts => do let (r, ts) ← parsePipe ts; parseAndOrTail (.orElse l r) ts
+    | ts => .ok (l, ts)
+
+  private partial def parsePipe (ts : List Tok) : Except String (Pipeline × List Tok) := do
+    let (l, ts) ← parseElem ts
+    parsePipeTail l ts
+  private partial def parsePipeTail (l : Pipeline) : List Tok → Except String (Pipeline × List Tok)
+    | .pipe :: ts => do let (r, ts) ← parseElem ts; parsePipeTail (.pipe l r) ts
+    | ts => .ok (l, ts)
+
+  private partial def parseElem (ts : List Tok) : Except String (Pipeline × List Tok) := do
+    -- base: either a parenthesized group, or a run of words
+    let (base, ts) ← (
+      match ts with
+      | .lp :: ts => do
+          let (g, ts) ← parseSeq ts
+          match ts with
+          | .rp :: ts => .ok (Base.group g, ts)
+          | _ => .error "expected ')'"
+      | _ => do
+          let (ws, ts) := takeWords ts []
+          let b ← wordsToBase ws
+          .ok (b, ts))
+    -- optional redirect
+    match ts with
+    | .gt :: .word p :: ts => (applyRedirect base (some (.overwrite, p))).map (·, ts)
+    | .gtgt :: .word p :: ts => (applyRedirect base (some (.append, p))).map (·, ts)
+    | .gt :: _ | .gtgt :: _ => .error "redirection '>' expects a path"
+    | ts => (applyRedirect base none).map (·, ts)
+
+  /-- Consume leading `word` tokens. -/
+  private partial def takeWords : List Tok → List String → (List String × List Tok)
+    | .word w :: ts, acc => takeWords ts (acc ++ [w])
+    | ts, acc => (acc, ts)
+end
+
+/-- Parse a bash command string into a `Pipeline`, or an error message. Rejects
+anything outside the supported fragment (deny-by-default). -/
+partial def parsePipeline (s : String) : Except String Pipeline := do
+  let ts ← tokenize s.toList
+  if ts.isEmpty then .error "empty command"
+  else
+    let (p, rest) ← parseSeq ts
+    if rest.isEmpty then .ok p
+    else .error s!"unexpected trailing tokens ({rest.length} left)"
+
+end ShellWall.Parser
diff --git a/ShellWall/Policy.lean b/ShellWall/Policy.lean
new file mode 100644
index 0000000..19f917e
--- /dev/null
+++ b/ShellWall/Policy.lean
@@ -0,0 +1,110 @@
+import ShellWall.Basic
+
+/-- The confidentiality/writability class the policy assigns to a path. Two axes:
+public vs. private (may its content flow to a public sink?) and RW vs. RO (may it
+be written?). `cmdOutIsPublic` seeds public PROVENANCE from reads of `public*` paths;
+the `write_*` safety rules gate writes on the `*RW` classes. -/
+inductive PathClass where
+  /-- Public and writable: readable as public data, and a valid public write sink. -/
+  | publicRW
+  /-- Public and read-only: a frozen, world-readable source; never a write target. -/
+  | publicRO
+  /-- Private and writable: writable by its owner; never a public sink. -/
+  | privateRW
+  /-- Private and read-only: e.g. system config; readable, never written. -/
+  | privateRO
+  deriving DecidableEq
+
+-- Externally configured policy table. In a real deployment this would be loaded
+-- from config; v1 fixes a small, legible, illustrative table so that `checkSafe`
+-- is computable and testable. Total and deterministic.
+--
+-- DENY-BY-DEFAULT: the final catch-all is a deliberate policy stance, not a
+-- throwaway. The safest classification for an *unknown* path is the most
+-- restrictive one that still lets its owner use it -- `privateRW`: writable by
+-- its owner, never a public sink. Defaulting unknown paths to any `public` class
+-- would let unmodeled paths act as leak sinks, because `cmdOutIsPublic` seeds public
+-- provenance from exactly the paths classified public.
+--
+-- SUBTREE MATCHING: each rule matches a path PREFIX with a `List`-cons tail
+-- (`_`) absorbing arbitrary remaining depth, so a rule governs its whole subtree
+-- at any depth. Totality is structural and needs no termination argument: each
+-- pattern inspects a bounded number of leading segments, the trailing `_` absorbs
+-- any remainder, and the final catch-all makes the match exhaustive. There is no
+-- recursion here.
+--
+-- PRECEDENCE IS A CORRECTNESS REQUIREMENT, NOT STYLE: `home/<a>/public/...` is
+-- tested BEFORE the general `home/<a>/...` rule, because every public path also
+-- matches the general rule. Ordered matching therefore implements longest-match.
+-- Reversing these two would classify public subtrees as `privateRW` -- the safe
+-- direction, but wrong, and it would make `write_public_ok` unreachable for
+-- agents, silently killing the public-output flow.
+--
+-- `publicRO` (/shared) = public AND read-only: a published, frozen,
+-- world-readable artifact. No `SafeCmd` write rule accepts `publicRO`
+-- (`write_public_ok` needs `publicRW`, `write_private_ok` needs `privateRW`), so
+-- /shared is unwritable by everyone -- including `system`. It is exactly the kind
+-- of source `cmdOutIsPublic` certifies public-provenance from, so making it reachable
+-- means the noninterference proof must discharge a real public-read case rather than
+-- a vacuous one.
+/-- A path's segment list for policy matching (approach (A)). `FilePath.components`
+yields a leading `""` for absolute paths (`/home/a` → `["", "home", "a"]`);
+filtering empty segments normalizes absolute, relative, and trailing-slash forms
+to the bare segment list the subtree patterns expect. -/
+def segments (p : Path) : List String := p.components.filter (· ≠ "")
+
+/-- Classify a path per the policy table (see the design notes above for the
+deny-by-default, longest-match, and `publicRO` rationale). Total and deterministic;
+subtree matching via ordered patterns over `segments p`. -/
+def classify (p : Path) : PathClass :=
+  match segments p with
+  | "home" :: _ :: "public" :: _ => .publicRW   -- agent's public output subtree, any depth
+  | "home" :: _ :: _             => .privateRW  -- rest of an agent's home, any depth
+  | "shared" :: _                => .publicRO   -- world-readable frozen reference tree
+  | "tmp" :: _                   => .publicRW   -- scratch space
+  | "etc" :: _                   => .privateRO  -- system config: readable, never written
+  -- DELIBERATELY REDUNDANT: `/private` gets the same class (`privateRW`) as the
+  -- default catch-all, so this arm changes no behavior. Kept as an explicit entry
+  -- documenting that `/private` is intentionally private data, not an unclassified
+  -- path that merely happens to land on the default.
+  | "private" :: _               => .privateRW
+  | _                            => .privateRW  -- DEFAULT: deny-by-default (see above)
+
+/-- Who owns a path, i.e. who has write-authority over it via `CanWrite`. Either a
+named agent or the system. -/
+inductive Owner where
+  /-- An agent, identified by `id` (e.g. the owner of `/home/<id>/...`). -/
+  | agent  (id : String)
+  /-- The system — owns everything not under an agent's home. -/
+  | system
+  deriving DecidableEq
+
+-- DENY-BY-DEFAULT: `CanWrite` (Safety.lean) currently has only the `self`
+-- constructor, which requires `ownerOf p = a`. Defaulting unknown paths to
+-- `.system` therefore means no *agent* can write them without an explicit
+-- ownership entry: an agent cannot write a path it does not provably own. This
+-- is the correct deny-by-default direction.
+--
+-- Intended interaction with `classify`: a default-unknown path is `privateRW`
+-- AND `.system`-owned, so an agent gets neither a public-write path nor
+-- ownership of it -- it simply cannot write there at all.
+--
+-- SUBTREE MATCHING: as in `classify`, and total for the same structural reason.
+-- One rule now covers an agent's ENTIRE home subtree, public or not: the separate
+-- `public` entry that exact-shape matching needed is subsumed, because
+-- `"home" :: a :: _` already matches every depth under `home/<a>`. Ownership is
+-- therefore uniform across an agent's home, while `classify` is what varies
+-- between its public and private parts.
+/-- The owner of a path (see the design notes above). Total and deterministic;
+one rule covers an agent's entire home subtree, everything else is `system`. -/
+def ownerOf (p : Path) : Owner :=
+  match segments p with
+  | "home" :: agentId :: _ => .agent agentId  -- an agent owns its whole home subtree
+  | "shared" :: _          => .system         -- frozen reference tree, owned by system
+  -- CHOICE: /tmp is `.system`-owned. Combined with `classify`'s `.publicRW`, this
+  -- means NO agent can write /tmp in v1 (CanWrite has only `self`, and delegation
+  -- is deferred to v2). That is the safe direction, but /tmp is labelled "scratch
+  -- space" yet is agent-unwritable until v2 delegation lands.
+  | "tmp" :: _             => .system
+  | "etc" :: _             => .system
+  | _                      => .system         -- DEFAULT: unowned-by-agents => system
diff --git a/ShellWall/Provenance.lean b/ShellWall/Provenance.lean
new file mode 100644
index 0000000..298a1fd
--- /dev/null
+++ b/ShellWall/Provenance.lean
@@ -0,0 +1,146 @@
+import ShellWall.Semantics
+
+/-! # TRUSTED KERNEL — public-provenance (audit by inspection)
+
+This module is the small, auditable inductive characterization of *public-provenance*
+content: content that is DERIVED from reads of public paths through public-preserving
+transforms. A reviewer audits the handful of constructors below and believes them
+directly; nothing in the fast decision layer (`cmdOutIsPublic`/`provOut`,
+`checkFull`/`checkSafe`) need be trusted beyond the BRIDGE theorems here
+(`cmdOutIsPublic_sound`, `provOut_sound`), which prove the fast Bool functions sound
+against this kernel.
+
+PROVENANCE, NOT VALUE. This is deliberately NOT a value-based predicate of the form
+`FileState → Content → Prop` used as the write obligation — such a predicate is
+relationally unsound (a private value coinciding with a public path's bytes satisfies
+it). The difference is structural: a proposition over `(state, content)` alone cannot
+tell "read from a public path" from "happens to equal a public file's bytes." So the
+kernel is indexed by the COMMAND / EXECUTION that
+produced the content, not by the content value. Consequently
+`PublicProv (.read privatePath) s b` has NO applicable constructor even when
+`s privatePath` coincides byte-for-byte with a public file — provenance is pinned to
+the path actually read.
+
+NO AGGREGATION (load-bearing omission). There is deliberately NO
+constructor for `wc`/count/hash/statistics. Aggregation is the covert statistical
+disclosure channel; certifying it public would reopen a leak. Do NOT add such a
+constructor. This mirrors `cmdOutIsPublic`'s `| .wc => false`.
+
+TRUST BOUNDARY. Trusted (audit these inductives): `PublicProv`, `PipeProv` (here);
+`SafeCmd`, `SafePipeline`, `CanWrite` (Safety.lean); `classify`, `ownerOf` (Policy).
+Untrusted-but-proven-sound: `cmdOutIsPublic`/`provOut`/`checkFull`/`checkSafe` (via the
+bridges here + `checkSafe_sound`). Untrusted model (fidelity-tested, not proven):
+`evalCmd`/`evalPipelineFull` and the parser/executor. The kernel inductives reference
+the semantics (`evalPipelineFull`) as the shared execution MODEL — exactly as
+`SafePipeline` does — but never reference the decision functions. -/
+
+/-- KERNEL (command level): `PublicProv c s stdinPub` — the STDOUT of command `c`, run
+in state `s` with a stdin whose public-provenance is `stdinPub`, is public-provenance.
+
+Genuinely provenance: the only base source is reading a path that IS public
+(`isPublicPath p = true`) and present; a private read has no constructor no matter the
+bytes. The stream transforms preserve provenance (public in ⇒ public out), so they
+require `stdinPub = true`. `wc`/`write`/`rm`/`mkdir` have NO constructor — their output
+is never public-provenance (see the aggregation note). Mirrors `cmdOutIsPublic`. -/
+inductive PublicProv : Cmd → FileState → Bool → Prop where
+  /-- BASE: reading a PUBLIC, present path yields public-provenance stdout (any
+  incoming `stdinPub`, since `read` ignores stdin). Provenance is pinned to `p`. -/
+  | read (p : Path) (s : FileState) (stdinPub : Bool)
+      (hpath : isPublicPath p = true) (hpresent : (s p).isSome = true) :
+      PublicProv (.read p) s stdinPub
+  /-- TRANSFORM: `grep` of public-provenance stdin is public-provenance. -/
+  | grep (pat : String) (s : FileState) : PublicProv (.grep pat) s true
+  /-- TRANSFORM: `sort` of public-provenance stdin is public-provenance. -/
+  | sort (s : FileState) : PublicProv .sort s true
+  /-- TRANSFORM: `uniq` of public-provenance stdin is public-provenance. -/
+  | uniq (s : FileState) : PublicProv .uniq s true
+
+/-- BRIDGE (command level): the untrusted Bool `cmdOutIsPublic` is SOUND w.r.t. the
+kernel — a `true` answer yields a kernel proof. So the fast function need not be
+trusted, only this theorem. (Completeness — the converse — is intentionally not
+claimed; the project's stance is soundness-only.) -/
+theorem cmdOutIsPublic_sound {c : Cmd} {s : FileState} {stdinPub : Bool} :
+    cmdOutIsPublic c s stdinPub = true → PublicProv c s stdinPub := by
+  intro h
+  cases c with
+  | read p =>
+    simp only [cmdOutIsPublic, Bool.and_eq_true] at h
+    exact PublicProv.read p s stdinPub h.1 h.2
+  | grep pat => simp only [cmdOutIsPublic] at h; subst h; exact PublicProv.grep pat s
+  | sort => simp only [cmdOutIsPublic] at h; subst h; exact PublicProv.sort s
+  | uniq => simp only [cmdOutIsPublic] at h; subst h; exact PublicProv.uniq s
+  | wc => simp [cmdOutIsPublic] at h
+  | write p m => simp [cmdOutIsPublic] at h
+  | rm p => simp [cmdOutIsPublic] at h
+  | mkdir p => simp [cmdOutIsPublic] at h
+
+/-- KERNEL (pipeline level): `PipeProv p s stdin pub` — the STDOUT of pipeline `p`, run
+in `s` on `stdin` whose provenance is `pub`, is public-provenance. Lifts `PublicProv`
+through the operators exactly as execution threads them (`evalPipelineFull`), so it
+references the execution MODEL but NOT the decision functions.
+
+The `pipe` case is the subtle one: stage 2 runs on stage 1's stdout with input
+provenance `b`, and `b = true` is only allowed WITH a proof that stage 1's output is
+itself public-provenance (`hb`). Without that guard the relation would be unsound
+(one could spuriously claim `b = true` to satisfy a stage-2 `grep`); with it,
+`cat privatefile | grep x` is correctly NOT `PipeProv`. -/
+inductive PipeProv : Pipeline → FileState → Content → Bool → Prop where
+  | single {c : Cmd} {s : FileState} {stdin : Content} {pub : Bool}
+      (h : PublicProv c s pub) : PipeProv (.single c) s stdin pub
+  | pipe {p₁ p₂ : Pipeline} {s : FileState} {stdin : Content} {pub b : Bool}
+      (hb : b = true → PipeProv p₁ s stdin pub)
+      (h₂ : PipeProv p₂ (evalPipelineFull p₁ s stdin).1 (evalPipelineFull p₁ s stdin).2.1 b) :
+      PipeProv (.pipe p₁ p₂) s stdin pub
+  | seq {p₁ p₂ : Pipeline} {s : FileState} {stdin : Content} {pub : Bool}
+      (h₂ : PipeProv p₂ (evalPipelineFull p₁ s stdin).1 .empty false) :
+      PipeProv (.seq p₁ p₂) s stdin pub
+  | andThen_succ {p₁ p₂ : Pipeline} {s : FileState} {stdin : Content} {pub : Bool}
+      (hexit : (evalPipelineFull p₁ s stdin).2.2 = .success)
+      (h₂ : PipeProv p₂ (evalPipelineFull p₁ s stdin).1 .empty false) :
+      PipeProv (.andThen p₁ p₂) s stdin pub
+  | andThen_fail {p₁ p₂ : Pipeline} {s : FileState} {stdin : Content} {pub : Bool} {n : Nat}
+      (hexit : (evalPipelineFull p₁ s stdin).2.2 = .failure n)
+      (h₁ : PipeProv p₁ s stdin pub) :
+      PipeProv (.andThen p₁ p₂) s stdin pub
+  | orElse_succ {p₁ p₂ : Pipeline} {s : FileState} {stdin : Content} {pub : Bool}
+      (hexit : (evalPipelineFull p₁ s stdin).2.2 = .success)
+      (h₁ : PipeProv p₁ s stdin pub) :
+      PipeProv (.orElse p₁ p₂) s stdin pub
+  | orElse_fail {p₁ p₂ : Pipeline} {s : FileState} {stdin : Content} {pub : Bool} {n : Nat}
+      (hexit : (evalPipelineFull p₁ s stdin).2.2 = .failure n)
+      (h₂ : PipeProv p₂ (evalPipelineFull p₁ s stdin).1 .empty false) :
+      PipeProv (.orElse p₁ p₂) s stdin pub
+
+/-- BRIDGE (pipeline level): the untrusted Bool `provOut` is SOUND w.r.t. the kernel —
+`provOut p s stdin pub = true` yields a `PipeProv` proof. Proved by induction mirroring
+`provOut`'s recursion; each `true`-producing branch maps to exactly one kernel
+constructor — the interpreter hands the kernel a proof, at the pipeline level.
+Soundness only (no converse). -/
+theorem provOut_sound (p : Pipeline) :
+    ∀ (s : FileState) (stdin : Content) (pub : Bool),
+      provOut p s stdin pub = true → PipeProv p s stdin pub := by
+  induction p with
+  | single c =>
+    intro s stdin pub h
+    simp only [provOut] at h
+    exact PipeProv.single (cmdOutIsPublic_sound h)
+  | pipe p₁ p₂ ih₁ ih₂ =>
+    intro s stdin pub h
+    simp only [provOut] at h
+    exact PipeProv.pipe (b := provOut p₁ s stdin pub) (fun hb => ih₁ _ _ _ hb) (ih₂ _ _ _ h)
+  | seq p₁ p₂ ih₁ ih₂ =>
+    intro s stdin pub h
+    simp only [provOut] at h
+    exact PipeProv.seq (ih₂ _ _ _ h)
+  | andThen p₁ p₂ ih₁ ih₂ =>
+    intro s stdin pub h
+    simp only [provOut] at h
+    cases hexit : (evalPipelineFull p₁ s stdin).2.2 with
+    | success => rw [hexit] at h; exact PipeProv.andThen_succ hexit (ih₂ _ _ _ h)
+    | failure n => rw [hexit] at h; exact PipeProv.andThen_fail hexit (ih₁ _ _ _ h)
+  | orElse p₁ p₂ ih₁ ih₂ =>
+    intro s stdin pub h
+    simp only [provOut] at h
+    cases hexit : (evalPipelineFull p₁ s stdin).2.2 with
+    | success => rw [hexit] at h; exact PipeProv.orElse_succ hexit (ih₁ _ _ _ h)
+    | failure n => rw [hexit] at h; exact PipeProv.orElse_fail hexit (ih₂ _ _ _ h)
diff --git a/ShellWall/Safety.lean b/ShellWall/Safety.lean
new file mode 100644
index 0000000..89b899c
--- /dev/null
+++ b/ShellWall/Safety.lean
@@ -0,0 +1,571 @@
+import ShellWall.Semantics
+
+/-! ## TRUSTED KERNEL — the safety spec
+
+`CanWrite`, `SafeCmd`, `SafePipeline` below are TRUSTED inductive definitions: the
+guarantee is only as good as reading these and believing they capture "safe to run".
+Audit them by inspection. Everything downstream (`checkFull`/`checkSafe` in Decide,
+the noninterference proof further down this file) is proven RELATIVE to them and need
+not be trusted directly. See the ARCHITECTURE note in `ShellWall.lean` and the
+public-provenance kernel in `Provenance.lean` (`PublicProv`/`PipeProv`).
+
+PROVENANCE, NOT A VALUE PREDICATE (design note). Public-ness of content is tracked
+FORWARD, along execution, by the Bool `cmdOutIsPublic`/`provOut` (in `Semantics`),
+pinned to the PATHS a stage reads, and characterized inductively by `PublicProv`
+(`Provenance.lean`). A per-state value predicate of the form
+`FileState → Content → Prop` as the `write_public_ok` obligation would be relationally
+UNSOUND (a private value coinciding with a public path's bytes satisfies it in each
+state yet differs across agreeing states — e.g. `cat /private/secret > public`);
+provenance (`pub = true`) avoids this because it is pinned to the paths READ, so
+agreeing states force the same value. The load-bearing omission is that
+`cmdOutIsPublic`/`PublicProv` NEVER certify `wc` (or any aggregation) as public,
+closing the covert statistical channel. Do NOT reintroduce a value-based public
+predicate. -/
+
+/-- `CanWrite a p`: owner `a` has write-authority over path `p`. In v1 the only
+way to hold it is to own `p` outright; delegation is deferred to v2. -/
+inductive CanWrite : Owner → Path → Prop where
+  /-- An owner may write a path it owns (`ownerOf p = a`). The sole v1 constructor;
+  delegation constructors are deferred to v2. -/
+  | self (a : Owner) (p : Path) (h : ownerOf p = a) : CanWrite a p
+
+/-- `SafeCmd a cmd s stdin pub`: owner `a` may execute `cmd` in state `s` with the
+given `stdin` content flowing in, where `pub : Bool` records whether that stdin is
+public-PROVENANCE (produced by reads of public paths / public-preserving transforms
+— see `provOut`). Only `write_public_ok` consumes `pub`.
+
+`write_public_ok` requires `pub = true` (provenance) rather than a per-state value
+predicate. A value-based obligation would be relationally UNSOUND: a private value
+coinciding with a public path's bytes satisfies it in each state separately, yet
+differs across agreeing states (e.g. `cat /private/secret > public`). Provenance is
+pinned to the paths READ, so agreeing states force the same value. This aligns the
+spec with the decider (`checkCmd`/`cmdOutIsPublic`).
+
+The four stream-transform commands (grep/sort/uniq/wc) touch no path directly, so
+they are unconditionally safe *as commands*; their provenance effect is in
+`cmdOutIsPublic`, not here. -/
+inductive SafeCmd : Owner → Cmd → FileState → Content → Bool → Prop where
+  /-- Reading is UNCONDITIONALLY safe at the command layer. Confidentiality is
+  enforced at the write boundary, not the read boundary — reading private data is
+  never itself the violation, only publishing it is. -/
+  | read_ok (a : Owner) (p : Path) (s : FileState) (stdin : Content) (pub : Bool) :
+      SafeCmd a (.read p) s stdin pub
+
+  /-- Writing to a public (`publicRW`) path is safe iff the writer owns it AND the
+  content flowing in is public-PROVENANCE (`pub = true`). See the type note: the
+  obligation is on provenance, not per-state value (relational soundness). -/
+  | write_public_ok (a : Owner) (p : Path) (mode : WriteMode) (s : FileState)
+      (stdin : Content) (pub : Bool)
+      (hclass : classify p = .publicRW)
+      (hown : CanWrite a p)
+      (hpub : pub = true) :                -- ← stdin is public-PROVENANCE
+      SafeCmd a (.write p mode) s stdin pub
+
+  /-- Writing to a private (`privateRW`) path is safe iff the writer owns it — no
+  provenance obligation, because a private path is not a public sink. -/
+  | write_private_ok (a : Owner) (p : Path) (mode : WriteMode) (s : FileState)
+      (stdin : Content) (pub : Bool)
+      (hclass : classify p = .privateRW)
+      (hown : CanWrite a p) :
+      SafeCmd a (.write p mode) s stdin pub
+
+  /-- `grep` is unconditionally safe as a command (a content transform). -/
+  | grep_ok (a : Owner) (pat : String) (s : FileState) (stdin : Content) (pub : Bool) :
+      SafeCmd a (.grep pat) s stdin pub
+  /-- `sort` is unconditionally safe as a command. -/
+  | sort_ok (a : Owner) (s : FileState) (stdin : Content) (pub : Bool) : SafeCmd a .sort s stdin pub
+  /-- `uniq` is unconditionally safe as a command. -/
+  | uniq_ok (a : Owner) (s : FileState) (stdin : Content) (pub : Bool) : SafeCmd a .uniq s stdin pub
+  /-- `wc` is unconditionally safe as a command. (Its output is never certified
+  public — see `cmdOutIsPublic`.) -/
+  | wc_ok   (a : Owner) (s : FileState) (stdin : Content) (pub : Bool) : SafeCmd a .wc s stdin pub
+
+  /-- `rm` is a destructive write and requires write-authority over the target. No
+  provenance obligation (removing data cannot leak private content to a public
+  sink), but `CanWrite` is mandatory — the most dangerous command in the set. -/
+  | rm_ok (a : Owner) (p : Path) (s : FileState) (stdin : Content) (pub : Bool)
+      (hown : CanWrite a p) :
+      SafeCmd a (.rm p) s stdin pub
+
+  /-- `mkdir` requires write-authority over the target path. NOTE: ownership of the
+  *newly created* directory is design open-question 5.4, unresolved here; for v1,
+  `CanWrite a p` is the gate. -/
+  | mkdir_ok (a : Owner) (p : Path) (s : FileState) (stdin : Content) (pub : Bool)
+      (hown : CanWrite a p) :
+      SafeCmd a (.mkdir p) s stdin pub
+
+/-- `SafePipeline a pipe s stdin`: owner `a` may execute `pipe` in state `s` with
+the given `stdin`. Each second stage is checked against the state AND stdin it
+ACTUALLY runs in, threaded EXACTLY as `evalPipelineFull` threads them (not
+`evalPipeline`, which forces `.empty` stdin) — so the safety obligations match real
+execution. This is why `Safety` depends on `Semantics`.
+
+DELIBERATE v1 CONSERVATISM: `andThen`/`orElse` require BOTH branches safe, even
+though at runtime `a && b` runs `b` only on success and `a || b` only on failure.
+v1 does not reason about which branch executes for the SAFETY check (sound but
+conservative — it may reject a pipeline whose unsafe branch never runs). Refining
+this needs ExitCode reasoning and is deferred. (Note: the *decider*'s output-public
+flag IS exit-aware — see `checkFull` — but the safety judgment here is not.) -/
+inductive SafePipeline : Owner → Pipeline → FileState → Content → Bool → Prop where
+  /-- A single command is safe iff the command is safe (same stdin/`pub`). -/
+  | single (a : Owner) (c : Cmd) (s : FileState) (stdin : Content) (pub : Bool) :
+      SafeCmd a c s stdin pub → SafePipeline a (.single c) s stdin pub
+
+  /-- `a | b`: `a` safe, and `b` safe in the state AFTER `a`, on `a`'s stdout as its
+  stdin, with `pub` updated to `a`'s output provenance (`provOut p₁ s stdin pub`) —
+  threaded exactly as `evalPipelineFull` and the decider run. -/
+  | pipe (a : Owner) (p₁ p₂ : Pipeline) (s : FileState) (stdin : Content) (pub : Bool) :
+      SafePipeline a p₁ s stdin pub →
+      SafePipeline a p₂ (evalPipelineFull p₁ s stdin).1 (evalPipelineFull p₁ s stdin).2.1
+        (provOut p₁ s stdin pub) →
+      SafePipeline a (.pipe p₁ p₂) s stdin pub
+
+  /-- `a ; b`: `a` safe, and `b` safe in the post-`a` state with FRESH `.empty` stdin
+  and `pub = false` (a fresh terminal-empty stdin is not public-provenance). -/
+  | seq (a : Owner) (p₁ p₂ : Pipeline) (s : FileState) (stdin : Content) (pub : Bool) :
+      SafePipeline a p₁ s stdin pub →
+      SafePipeline a p₂ (evalPipelineFull p₁ s stdin).1 .empty false →
+      SafePipeline a (.seq p₁ p₂) s stdin pub
+
+  /-- `a && b`: BOTH branches safe (v1 conservatism), `b` in the post-`a` state with
+  fresh `.empty` stdin and `pub = false`. PUBLIC-GUARD requirement — the guard `a`'s
+  exit code (which decides whether `b` runs) must be public-determined, so it agrees
+  across states that agree on public paths. That needs BOTH:
+  - `hguard`: `a` touches only public PATHS (closes the path channel);
+  - `hstdin`: `a`'s incoming STDIN is public-provenance (`pub = true`) or the
+    canonical empty content (`.empty`, which is constant hence trivially agrees).
+    Without this, a guard like `grep` reads private data through a piped stdin and
+    leaks it via the exit code. -/
+  | andThen (a : Owner) (p₁ p₂ : Pipeline) (s : FileState) (stdin : Content) (pub : Bool)
+      (hguard : touchesOnlyPublic p₁ = true)
+      (hstdin : pub = true ∨ stdin = .empty) :
+      SafePipeline a p₁ s stdin pub →
+      SafePipeline a p₂ (evalPipelineFull p₁ s stdin).1 .empty false →
+      SafePipeline a (.andThen p₁ p₂) s stdin pub
+
+  /-- `a || b`: BOTH branches safe (v1 conservatism), `b` in the post-`a` state with
+  fresh `.empty` stdin and `pub = false`. PUBLIC-GUARD requirement, same as
+  `andThen`: the guard's exit must be public-determined — `hguard` (public paths)
+  AND `hstdin` (public-provenance or empty stdin). -/
+  | orElse (a : Owner) (p₁ p₂ : Pipeline) (s : FileState) (stdin : Content) (pub : Bool)
+      (hguard : touchesOnlyPublic p₁ = true)
+      (hstdin : pub = true ∨ stdin = .empty) :
+      SafePipeline a p₁ s stdin pub →
+      SafePipeline a p₂ (evalPipelineFull p₁ s stdin).1 .empty false →
+      SafePipeline a (.orElse p₁ p₂) s stdin pub
+
+/-! ## Noninterference proof infrastructure
+
+The relational (two-execution) machinery proving `shellwall_noninterference`. Built
+bottom-up: agreement algebra → command-level agreement (`evalCmd_agrees`) → the
+public-program-counter lemma (`touchesOnlyPublic_agrees`) → the main relational
+invariant (`eval_agrees`) → the theorem. See the `eval_agrees` docstring for where
+each of the four safety requirements is consumed. -/
+
+/-- `updateState` preserves public-path agreement when the SAME content is written to
+the SAME path. -/
+theorem updateState_agrees {s₁ s₂ : FileState} (p : Path) (c : Option Content)
+    (hag : agreeOnPublicPaths s₁ s₂) :
+    agreeOnPublicPaths (updateState s₁ p c) (updateState s₂ p c) := by
+  intro q hq
+  simp only [updateState]
+  split
+  · rfl
+  · exact hag q hq
+
+/-- Writing to a PRIVATE path preserves public-path agreement, regardless of the
+(possibly differing) content written — the write cannot touch a public path. -/
+theorem updateState_private_agrees {s₁ s₂ : FileState} {p : Path} (c₁ c₂ : Option Content)
+    (hpriv : isPublicPath p = false) (hag : agreeOnPublicPaths s₁ s₂) :
+    agreeOnPublicPaths (updateState s₁ p c₁) (updateState s₂ p c₂) := by
+  intro q hq
+  simp only [updateState]
+  have hqp : ¬ (q = p) := by
+    intro h; rw [h] at hq; rw [hpriv] at hq; exact Bool.noConfusion hq
+  simp only [if_neg hqp]
+  exact hag q hq
+
+/-- `agreeOnPublicPaths` is symmetric. -/
+theorem agree_symm {s₁ s₂ : FileState} (h : agreeOnPublicPaths s₁ s₂) :
+    agreeOnPublicPaths s₂ s₁ := fun p hp => (h p hp).symm
+
+/-- `agreeOnPublicPaths` is transitive. -/
+theorem agree_trans {s₁ s₂ s₃ : FileState} (h₁ : agreeOnPublicPaths s₁ s₂)
+    (h₂ : agreeOnPublicPaths s₂ s₃) : agreeOnPublicPaths s₁ s₃ :=
+  fun p hp => (h₁ p hp).trans (h₂ p hp)
+
+/-- Updating a PRIVATE path leaves the public projection unchanged (agrees with the
+pre-update state). -/
+theorem updateState_private_self {s : FileState} {q : Path} (c : Option Content)
+    (hpriv : isPublicPath q = false) : agreeOnPublicPaths (updateState s q c) s := by
+  intro p hp
+  simp only [updateState]
+  have hpq : ¬ (p = q) := by intro h; rw [h, hpriv] at hp; exact Bool.noConfusion hp
+  rw [if_neg hpq]
+
+/-- Public-path agreement gives equal public projections. -/
+theorem publicProjection_eq_of_agree {s₁ s₂ : FileState} (hag : agreeOnPublicPaths s₁ s₂) :
+    publicProjection s₁ = publicProjection s₂ := by
+  funext p
+  simp only [publicProjection]
+  split
+  · rename_i h; exact hag p h
+  · rfl
+
+/-- `read` leaves the state unchanged. -/
+theorem evalCmd_fst_read (q : Path) (s : FileState) (stdin : Content) :
+    (evalCmd (.read q) s stdin).1 = s := by simp only [evalCmd]; split <;> rfl
+
+/-- `grep` leaves the state unchanged. -/
+theorem evalCmd_fst_grep (pat : String) (s : FileState) (stdin : Content) :
+    (evalCmd (.grep pat) s stdin).1 = s := by simp only [evalCmd]; split <;> rfl
+
+/-- COMMAND-LEVEL RELATIONAL AGREEMENT (the `single` base case). For a command safe in
+both runs, from agreeing states with stdin that agrees when public-provenance
+(`pub = true`): the resulting states agree on public paths; the stdout is EQUAL when
+the command's output is public-provenance (`cmdOutIsPublic = true`); and the output
+provenance flag agrees. Consumes: the `write_public_ok` `pub = true` obligation forces
+equal written content into public paths; `write_private_ok` sends (possibly differing)
+content only to a private path, invisible to the projection. -/
+theorem evalCmd_agrees (a : Owner) (c : Cmd) (s₁ s₂ : FileState)
+    (stdin₁ stdin₂ : Content) (pub : Bool)
+    (hag : agreeOnPublicPaths s₁ s₂)
+    (hc₁ : SafeCmd a c s₁ stdin₁ pub) (hc₂ : SafeCmd a c s₂ stdin₂ pub)
+    (hin : pub = true → stdin₁ = stdin₂) :
+    agreeOnPublicPaths (evalCmd c s₁ stdin₁).1 (evalCmd c s₂ stdin₂).1
+    ∧ (cmdOutIsPublic c s₁ pub = true →
+        (evalCmd c s₁ stdin₁).2.1 = (evalCmd c s₂ stdin₂).2.1)
+    ∧ cmdOutIsPublic c s₁ pub = cmdOutIsPublic c s₂ pub := by
+  cases c with
+  | read q =>
+    refine ⟨?_, ?_, ?_⟩
+    · rw [evalCmd_fst_read, evalCmd_fst_read]; exact hag
+    · intro hp
+      simp only [cmdOutIsPublic, Bool.and_eq_true] at hp
+      obtain ⟨hqpub, _⟩ := hp
+      simp only [evalCmd]; rw [hag q hqpub]; split <;> rfl
+    · simp only [cmdOutIsPublic]
+      cases hq : isPublicPath q with
+      | false => rfl
+      | true => rw [hag q hq]
+  | write q mode =>
+    cases hc₁ with
+    | write_public_ok =>
+      rename_i hclass hown hpub
+      have hqpub : isPublicPath q = true := by simp only [isPublicPath, hclass]
+      have hstdineq : stdin₁ = stdin₂ := hin hpub
+      refine ⟨?_, ?_, ?_⟩
+      · cases mode with
+        | overwrite =>
+          simp only [evalCmd]; rw [hstdineq]; exact updateState_agrees q _ hag
+        | append =>
+          simp only [evalCmd]; rw [hstdineq, hag q hqpub]; exact updateState_agrees q _ hag
+      · intro hp; simp [cmdOutIsPublic] at hp
+      · simp only [cmdOutIsPublic]
+    | write_private_ok =>
+      rename_i hclass hown
+      have hpriv : isPublicPath q = false := by simp only [isPublicPath, hclass]
+      refine ⟨?_, ?_, ?_⟩
+      · simp only [evalCmd]; exact updateState_private_agrees _ _ hpriv hag
+      · intro hp; simp [cmdOutIsPublic] at hp
+      · simp only [cmdOutIsPublic]
+  | grep pat =>
+    refine ⟨?_, ?_, ?_⟩
+    · rw [evalCmd_fst_grep, evalCmd_fst_grep]; exact hag
+    · intro hp; simp only [cmdOutIsPublic] at hp
+      have hstdineq : stdin₁ = stdin₂ := hin hp
+      simp only [evalCmd]; rw [hstdineq]; split <;> rfl
+    · simp only [cmdOutIsPublic]
+  | sort =>
+    refine ⟨hag, ?_, ?_⟩
+    · intro hp; simp only [cmdOutIsPublic] at hp
+      simp only [evalCmd]; rw [hin hp]
+    · simp only [cmdOutIsPublic]
+  | uniq =>
+    refine ⟨hag, ?_, ?_⟩
+    · intro hp; simp only [cmdOutIsPublic] at hp
+      simp only [evalCmd]; rw [hin hp]
+    · simp only [cmdOutIsPublic]
+  | wc =>
+    refine ⟨hag, ?_, ?_⟩
+    · intro hp; simp [cmdOutIsPublic] at hp
+    · simp only [cmdOutIsPublic]
+  | rm q =>
+    refine ⟨?_, ?_, ?_⟩
+    · simp only [evalCmd]
+      cases hq : isPublicPath q with
+      | true =>
+        rw [hag q hq]; split
+        · exact updateState_agrees q none hag
+        · exact hag
+      | false =>
+        split <;> split
+        · exact updateState_private_agrees none none hq hag
+        · exact agree_trans (updateState_private_self none hq) hag
+        · exact agree_trans hag (agree_symm (updateState_private_self none hq))
+        · exact hag
+    · intro hp; simp [cmdOutIsPublic] at hp
+    · simp only [cmdOutIsPublic]
+  | mkdir q =>
+    refine ⟨?_, ?_, ?_⟩
+    · simp only [evalCmd]
+      cases hq : isPublicPath q with
+      | true =>
+        rw [hag q hq]; split
+        · exact hag
+        · exact updateState_agrees q (some .empty) hag
+      | false =>
+        split <;> split
+        · exact hag
+        · exact agree_trans hag (agree_symm (updateState_private_self (some .empty) hq))
+        · exact agree_trans (updateState_private_self (some .empty) hq) hag
+        · exact updateState_private_agrees (some .empty) (some .empty) hq hag
+    · intro hp; simp [cmdOutIsPublic] at hp
+    · simp only [cmdOutIsPublic]
+
+/-- GUARD-EXIT AGREEMENT (the `hguard` payoff). A pipeline that touches only PUBLIC
+paths, run on two states agreeing on public paths WITH THE SAME stdin, produces
+agreeing public state, EQUAL stdout, and EQUAL exit code. Its control flow and output
+are functions of the public part of the state only — the "public program counter"
+discipline. Proved by induction over the pipeline structure, so compound and nested
+guards are covered automatically. -/
+theorem touchesOnlyPublic_agrees (p : Pipeline) :
+    ∀ (s₁ s₂ : FileState) (stdin : Content),
+      touchesOnlyPublic p = true → agreeOnPublicPaths s₁ s₂ →
+      agreeOnPublicPaths (evalPipelineFull p s₁ stdin).1 (evalPipelineFull p s₂ stdin).1
+      ∧ (evalPipelineFull p s₁ stdin).2.1 = (evalPipelineFull p s₂ stdin).2.1
+      ∧ (evalPipelineFull p s₁ stdin).2.2 = (evalPipelineFull p s₂ stdin).2.2 := by
+  induction p with
+  | single c =>
+    intro s₁ s₂ stdin htp hag
+    simp only [touchesOnlyPublic, cmdTouchesOnlyPublic] at htp
+    cases c with
+    | read q =>
+      have hqp : s₁ q = s₂ q := hag q htp
+      simp only [evalPipelineFull, evalCmd, hqp]
+      split <;> exact ⟨hag, by trivial, by trivial⟩
+    | write q mode =>
+      have hqp : s₁ q = s₂ q := hag q htp
+      cases mode with
+      | overwrite =>
+        simp only [evalPipelineFull, evalCmd]
+        exact ⟨updateState_agrees q (some stdin) hag, by trivial, by trivial⟩
+      | append =>
+        simp only [evalPipelineFull, evalCmd, hqp]
+        exact ⟨updateState_agrees q _ hag, by trivial, by trivial⟩
+    | grep pat =>
+      simp only [evalPipelineFull, evalCmd]
+      split <;> exact ⟨hag, by trivial, by trivial⟩
+    | sort => simp only [evalPipelineFull, evalCmd]; exact ⟨hag, by trivial, by trivial⟩
+    | uniq => simp only [evalPipelineFull, evalCmd]; exact ⟨hag, by trivial, by trivial⟩
+    | wc => simp only [evalPipelineFull, evalCmd]; exact ⟨hag, by trivial, by trivial⟩
+    | rm q =>
+      have hqp : s₁ q = s₂ q := hag q htp
+      simp only [evalPipelineFull, evalCmd, hqp]
+      split
+      · exact ⟨updateState_agrees q none hag, by trivial, by trivial⟩
+      · exact ⟨hag, by trivial, by trivial⟩
+    | mkdir q =>
+      have hqp : s₁ q = s₂ q := hag q htp
+      simp only [evalPipelineFull, evalCmd, hqp]
+      split
+      · exact ⟨hag, by trivial, by trivial⟩
+      · exact ⟨updateState_agrees q (some .empty) hag, by trivial, by trivial⟩
+  | pipe p₁ p₂ ih₁ ih₂ =>
+    intro s₁ s₂ stdin htp hag
+    simp only [touchesOnlyPublic, Bool.and_eq_true] at htp
+    obtain ⟨ht1, ht2⟩ := htp
+    obtain ⟨ha1, ho1, _⟩ := ih₁ s₁ s₂ stdin ht1 hag
+    simp only [evalPipelineFull]
+    rw [ho1]
+    exact ih₂ _ _ (evalPipelineFull p₁ s₂ stdin).2.1 ht2 ha1
+  | seq p₁ p₂ ih₁ ih₂ =>
+    intro s₁ s₂ stdin htp hag
+    simp only [touchesOnlyPublic, Bool.and_eq_true] at htp
+    obtain ⟨ht1, ht2⟩ := htp
+    obtain ⟨ha1, _, _⟩ := ih₁ s₁ s₂ stdin ht1 hag
+    simp only [evalPipelineFull]
+    exact ih₂ _ _ .empty ht2 ha1
+  | andThen p₁ p₂ ih₁ ih₂ =>
+    intro s₁ s₂ stdin htp hag
+    simp only [touchesOnlyPublic, Bool.and_eq_true] at htp
+    obtain ⟨ht1, ht2⟩ := htp
+    obtain ⟨ha1, ho1, he1⟩ := ih₁ s₁ s₂ stdin ht1 hag
+    simp only [evalPipelineFull]
+    rw [he1, ho1]
+    cases hec : (evalPipelineFull p₁ s₂ stdin).2.2 with
+    | success => exact ih₂ _ _ .empty ht2 ha1
+    | failure n => exact ⟨ha1, rfl, rfl⟩
+  | orElse p₁ p₂ ih₁ ih₂ =>
+    intro s₁ s₂ stdin htp hag
+    simp only [touchesOnlyPublic, Bool.and_eq_true] at htp
+    obtain ⟨ht1, ht2⟩ := htp
+    obtain ⟨ha1, ho1, he1⟩ := ih₁ s₁ s₂ stdin ht1 hag
+    simp only [evalPipelineFull]
+    rw [he1, ho1]
+    cases hec : (evalPipelineFull p₁ s₂ stdin).2.2 with
+    | success => exact ⟨ha1, rfl, rfl⟩
+    | failure n => exact ih₂ _ _ .empty ht2 ha1
+
+/-- THE RELATIONAL INVARIANT (main induction). For a pipeline safe in two runs from
+agreeing states, with stdin that agrees when public-provenance (`pub = true`):
+(1) resulting public state agrees; (2) the stdout is EQUAL when the pipeline's output
+is public-provenance (`provOut = true`) — the provenance-transport payoff; (3) the
+output provenance flag agrees across runs.
+
+Where the four safety requirements are consumed:
+- `evalCmd_agrees` (single/write case): the content-indexed write obligation and the
+  `pub` provenance flag force equal content into public paths.
+- `andThen`/`orElse`: `hguard` lets `touchesOnlyPublic_agrees` fire, and `hstdin` —
+  combined across BOTH runs — forces `stdin₁ = stdin₂`, so the guard's exit agrees and
+  the SAME branch runs in both. -/
+theorem eval_agrees (a : Owner) (p : Pipeline) :
+    ∀ (s₁ s₂ : FileState) (stdin₁ stdin₂ : Content) (pub : Bool),
+      agreeOnPublicPaths s₁ s₂ →
+      SafePipeline a p s₁ stdin₁ pub →
+      SafePipeline a p s₂ stdin₂ pub →
+      (pub = true → stdin₁ = stdin₂) →
+      agreeOnPublicPaths (evalPipelineFull p s₁ stdin₁).1 (evalPipelineFull p s₂ stdin₂).1
+      ∧ (provOut p s₁ stdin₁ pub = true →
+          (evalPipelineFull p s₁ stdin₁).2.1 = (evalPipelineFull p s₂ stdin₂).2.1)
+      ∧ provOut p s₁ stdin₁ pub = provOut p s₂ stdin₂ pub := by
+  induction p with
+  | single c =>
+    intro s₁ s₂ stdin₁ stdin₂ pub hag hs₁ hs₂ hin
+    cases hs₁ with
+    | single _ _ _ _ hc₁ =>
+    cases hs₂ with
+    | single _ _ _ _ hc₂ =>
+    exact evalCmd_agrees a c s₁ s₂ stdin₁ stdin₂ pub hag hc₁ hc₂ hin
+  | pipe p₁ p₂ ih₁ ih₂ =>
+    intro s₁ s₂ stdin₁ stdin₂ pub hag hs₁ hs₂ hin
+    cases hs₁ with
+    | pipe _ _ _ _ _ S1₁ S2₁ =>
+    cases hs₂ with
+    | pipe _ _ _ _ _ S1₂ S2₂ =>
+    obtain ⟨ha1, hb1, hc1⟩ := ih₁ s₁ s₂ stdin₁ stdin₂ pub hag S1₁ S1₂ hin
+    rw [← hc1] at S2₂
+    obtain ⟨ha2, hb2, hc2⟩ :=
+      ih₂ (evalPipelineFull p₁ s₁ stdin₁).1 (evalPipelineFull p₁ s₂ stdin₂).1
+        (evalPipelineFull p₁ s₁ stdin₁).2.1 (evalPipelineFull p₁ s₂ stdin₂).2.1
+        (provOut p₁ s₁ stdin₁ pub) ha1 S2₁ S2₂ hb1
+    refine ⟨?_, ?_, ?_⟩
+    · simp only [evalPipelineFull]; exact ha2
+    · simp only [evalPipelineFull, provOut]; exact hb2
+    · simp only [provOut]; rw [← hc1]; exact hc2
+  | seq p₁ p₂ ih₁ ih₂ =>
+    intro s₁ s₂ stdin₁ stdin₂ pub hag hs₁ hs₂ hin
+    cases hs₁ with
+    | seq _ _ _ _ _ S1₁ S2₁ =>
+    cases hs₂ with
+    | seq _ _ _ _ _ S1₂ S2₂ =>
+    obtain ⟨ha1, _, _⟩ := ih₁ s₁ s₂ stdin₁ stdin₂ pub hag S1₁ S1₂ hin
+    obtain ⟨ha2, hb2, hc2⟩ :=
+      ih₂ (evalPipelineFull p₁ s₁ stdin₁).1 (evalPipelineFull p₁ s₂ stdin₂).1
+        .empty .empty false ha1 S2₁ S2₂ (fun _ => rfl)
+    refine ⟨?_, ?_, ?_⟩
+    · simp only [evalPipelineFull]; exact ha2
+    · simp only [evalPipelineFull, provOut]; exact hb2
+    · simp only [provOut]; exact hc2
+  | andThen p₁ p₂ ih₁ ih₂ =>
+    intro s₁ s₂ stdin₁ stdin₂ pub hag hs₁ hs₂ hin
+    cases hs₁ with
+    | andThen _ _ _ _ _ hguard₁ hstdin₁ S1₁ S2₁ =>
+    cases hs₂ with
+    | andThen _ _ _ _ _ hguard₂ hstdin₂ S1₂ S2₂ =>
+    have hstdineq : stdin₁ = stdin₂ := by
+      rcases hstdin₁ with h | h
+      · exact hin h
+      · rcases hstdin₂ with h2 | h2
+        · exact hin h2
+        · rw [h, h2]
+    rw [hstdineq] at S1₁ S2₁ ⊢
+    obtain ⟨hga, hgo, hge⟩ := touchesOnlyPublic_agrees p₁ s₁ s₂ stdin₂ hguard₁ hag
+    obtain ⟨_, _, hpc1⟩ := ih₁ s₁ s₂ stdin₂ stdin₂ pub hag S1₁ S1₂ (fun _ => rfl)
+    obtain ⟨ha2, hb2, hc2⟩ :=
+      ih₂ (evalPipelineFull p₁ s₁ stdin₂).1 (evalPipelineFull p₁ s₂ stdin₂).1
+        .empty .empty false hga S2₁ S2₂ (fun _ => rfl)
+    refine ⟨?_, ?_, ?_⟩
+    · simp only [evalPipelineFull]; rw [hge]
+      cases hec : (evalPipelineFull p₁ s₂ stdin₂).2.2 with
+      | success => exact ha2
+      | failure n => exact hga
+    · simp only [evalPipelineFull, provOut]; rw [hge]
+      cases hec : (evalPipelineFull p₁ s₂ stdin₂).2.2 with
+      | success => exact hb2
+      | failure n => intro _; exact hgo
+    · simp only [provOut]; rw [hge]
+      cases hec : (evalPipelineFull p₁ s₂ stdin₂).2.2 with
+      | success => exact hc2
+      | failure n => exact hpc1
+  | orElse p₁ p₂ ih₁ ih₂ =>
+    intro s₁ s₂ stdin₁ stdin₂ pub hag hs₁ hs₂ hin
+    cases hs₁ with
+    | orElse _ _ _ _ _ hguard₁ hstdin₁ S1₁ S2₁ =>
+    cases hs₂ with
+    | orElse _ _ _ _ _ hguard₂ hstdin₂ S1₂ S2₂ =>
+    have hstdineq : stdin₁ = stdin₂ := by
+      rcases hstdin₁ with h | h
+      · exact hin h
+      · rcases hstdin₂ with h2 | h2
+        · exact hin h2
+        · rw [h, h2]
+    rw [hstdineq] at S1₁ S2₁ ⊢
+    obtain ⟨hga, hgo, hge⟩ := touchesOnlyPublic_agrees p₁ s₁ s₂ stdin₂ hguard₁ hag
+    obtain ⟨_, _, hpc1⟩ := ih₁ s₁ s₂ stdin₂ stdin₂ pub hag S1₁ S1₂ (fun _ => rfl)
+    obtain ⟨ha2, hb2, hc2⟩ :=
+      ih₂ (evalPipelineFull p₁ s₁ stdin₂).1 (evalPipelineFull p₁ s₂ stdin₂).1
+        .empty .empty false hga S2₁ S2₂ (fun _ => rfl)
+    refine ⟨?_, ?_, ?_⟩
+    · simp only [evalPipelineFull]; rw [hge]
+      cases hec : (evalPipelineFull p₁ s₂ stdin₂).2.2 with
+      | success => exact hga
+      | failure n => exact ha2
+    · simp only [evalPipelineFull, provOut]; rw [hge]
+      cases hec : (evalPipelineFull p₁ s₂ stdin₂).2.2 with
+      | success => intro _; exact hgo
+      | failure n => exact hb2
+    · simp only [provOut]; rw [hge]
+      cases hec : (evalPipelineFull p₁ s₂ stdin₂).2.2 with
+      | success => exact hpc1
+      | failure n => exact hc2
+
+/-- NONINTERFERENCE (the top-level security guarantee): if two filesystems agree on
+all public paths and the same pipeline is safe in both, then running it in either
+yields the same public projection — a safe pipeline cannot leak private data into
+public paths. Top-level pipelines start from `.empty` stdin.
+
+SCOPE: over the FILESYSTEM public projection only; does NOT cover stdout — see the
+`THREAT MODEL — stdout (v1)` note at the top of `Semantics.lean`.
+
+FOUR leak channels the spec closes — each was a real counterexample to an earlier,
+weaker spec, and each is defended by a specific mechanism:
+- unconstrained write witness → the content-indexed `write_public_ok` obligation;
+- implicit exit-code flow via a private-PATH guard → the `touchesOnlyPublic` guard;
+- per-state value-predicate coincidence → provenance-based `write_public_ok` (the
+  `pub = true` obligation, not a per-state value);
+- implicit exit-code flow via a private-STDIN guard → the
+  `hstdin : pub = true ∨ stdin = .empty` premise on `andThen`/`orElse`. Example:
+  `cat /private/secret | (grep yes && (cat /shared/ref > pub))` — the guard reads
+  private data through its piped stdin; `touchesOnlyPublic` checks the guard's paths
+  but not its stdin, so `hstdin` is what rejects it (the conditional's incoming stdin
+  is private-provenance).
+
+With all four channels closed, this theorem is PROVED (`eval_agrees`), with a clean
+axiom footprint (`propext`, `Classical.choice`, `Quot.sound` — no `sorryAx`, no
+`native_decide`). Top-level pipelines start from `.empty` stdin with `pub = false`;
+`.empty` counts as public-provenance for the guard-stdin check (it is constant, hence
+agrees across states — the `fun _ => rfl` witness below, since `pub = false`).
+
+PROOF: specialise the relational invariant `eval_agrees` to top-level `.empty` stdin
+(where the `pub = true → stdin₁ = stdin₂` obligation is vacuous), extract its
+public-state-agreement conjunct, and turn agreement into equal public projections. -/
+theorem shellwall_noninterference
+    (a : Owner) (p : Pipeline) (s₁ s₂ : FileState)
+    (hagree : agreeOnPublicPaths s₁ s₂)
+    (h₁ : SafePipeline a p s₁ .empty false) (h₂ : SafePipeline a p s₂ .empty false) :
+    publicProjection (evalPipeline p s₁).1 = publicProjection (evalPipeline p s₂).1 := by
+  obtain ⟨ha, _, _⟩ :=
+    eval_agrees a p s₁ s₂ .empty .empty false hagree h₁ h₂ (fun _ => rfl)
+  simp only [evalPipeline]
+  exact publicProjection_eq_of_agree ha
diff --git a/ShellWall/Semantics.lean b/ShellWall/Semantics.lean
new file mode 100644
index 0000000..21f9c64
--- /dev/null
+++ b/ShellWall/Semantics.lean
@@ -0,0 +1,396 @@
+import ShellWall.Basic
+import ShellWall.Syntax
+import ShellWall.Policy
+
+/-! # THREAT MODEL — stdout (v1)
+
+`evalPipeline` returns only `(FileState × ExitCode)`, so a pipeline sending private
+data to
+unredirected stdout (`cat /private/secret`) has no filesystem effect and is
+invisible to this model — and because v1's `read_ok` is unconditional, such a
+command is *permitted* by `SafeCmd` while `shellwall_noninterference` remains
+provable (it quantifies only over the filesystem's public projection).
+
+> **DECISION (v1):** stdout is out of scope for v1's threat model. ShellWall's
+> guarantee covers filesystem writes to modeled paths only. This is sound under
+> the explicit deployment assumption that the execution proxy does NOT return
+> unredirected stdout to the agent. Under that assumption, an unredirected
+> stdout channel is not agent-observable and therefore not a leak path. If that
+> assumption ever fails to hold, stdout must be modeled as a public sink (a
+> public-provenance obligation on writes to it), which is a signature change to
+> `evalPipeline` — tracked as a v2 item. This is consistent with the existing
+> decision to treat covert/side channels (timing, file size) as out of scope for
+> v1.
+
+This is accept-and-document: no code or signature change accompanies it. The
+deployment assumption above is load-bearing — if the proxy ever returns
+unredirected stdout to the agent, v1's guarantee does not cover that channel.
+-/
+
+/-- The filesystem: a total map from paths to their content (or `none` if absent).
+There is no directory/file distinction (see `evalCmd`'s `mkdir`).
+
+`def` (per spec) rather than `abbrev`: `FileState` is semireducible, so it unfolds
+during application elaboration but not at `instances` transparency. If later proof
+work needs it to reduce transparently, revisit this. -/
+def FileState := Path → Option Content
+
+/-! ## Line model
+
+Every text operation below shares one line convention. It is stated once here and
+used everywhere; `wc` deliberately does NOT use it (see `countLineBytes`). -/
+
+/-- Split text into lines under the shared line model.
+
+FIDELITY: strip at most one trailing `"\n"`, then split on `"\n"`:
+`"a\nb\n" → ["a","b"]` (a trailing newline TERMINATES the last line, it is not a
+separator introducing an empty final line), `"a\nb" → ["a","b"]` (an unterminated
+final line is still a line), `"" → []`, `"\n" → [""]`. This is the Unix text-file
+convention; the naive `s.splitOn "\n"` would yield a spurious trailing `""` for
+every newline-terminated file, corrupting `uniq` output and line counts. -/
+def textToLines (s : String) : List String :=
+  if s.isEmpty then []
+  else
+    let parts := s.splitOn "\n"
+    if s.endsWith "\n" then parts.dropLast else parts
+
+/-- Render lines back to text.
+
+FIDELITY: always newline-TERMINATES a non-empty result, matching grep/sort/uniq
+(which emit `"a\nb\n"` even when their input lacked a final newline). Consequence:
+these ops are not the identity on unterminated input — exactly as real coreutils. -/
+def linesToText (ls : List String) : String :=
+  match ls with
+  | [] => ""
+  | _  => String.intercalate "\n" ls ++ "\n"
+
+/-- Render lines to `Content`, canonicalising the empty result to `.empty`.
+(The model has three "no bytes" values — `.empty`, `.text ""`,
+`.binary ByteArray.empty` — a `Content` wart; every empty result here is `.empty`.) -/
+def linesToContent (ls : List String) : Content :=
+  match ls with
+  | [] => .empty
+  | _  => .text (linesToText ls)
+
+/-- A content's lines, if it has line structure.
+
+FIDELITY: binary content is decoded as UTF-8 when valid then treated as text;
+bytes that are not valid UTF-8 yield `none` (no line structure). Real coreutils
+operate bytewise with no decode step. -/
+def contentLines? : Content → Option (List String)
+  | .empty    => some []
+  | .text s   => some (textToLines s)
+  | .binary b => (String.fromUTF8? b).map textToLines
+
+/-! ## Content helpers -/
+
+/-- Concatenate two contents (the `cat a b` operation).
+
+FIDELITY: real bash has no text/binary distinction — a file is just bytes. The
+`text`/`binary` split is a model artifact, so cross-type cases concatenate the
+UTF-8 encodings and return `.binary` (byte-exact, never fails). `.empty` is the
+identity on both sides. -/
+def concatContent : Content → Content → Content
+  | .empty, c => c
+  | c, .empty => c
+  | .text s₁,   .text s₂   => .text (s₁ ++ s₂)
+  | .binary b₁, .binary b₂ => .binary (b₁ ++ b₂)
+  | .text s,    .binary b  => .binary (s.toUTF8 ++ b)
+  | .binary b,  .text s    => .binary (b ++ s.toUTF8)
+
+/-- Whether a single line matches a grep pattern.
+
+FIDELITY: substring only, not BRE regex. Real `grep` matches POSIX basic regular
+expressions; a regex engine is out of scope for v1, so this is `grep -F`: a line
+matches iff it contains `pat` as a literal substring. An empty pattern matches
+every line (as real grep does). -/
+def lineMatches (pat : String) (line : String) : Bool :=
+  if pat.isEmpty then true
+  else (line.splitOn pat).length > 1
+
+/-- Keep the lines of `c` matching `pat` (the `grep pat` content transform). -/
+def grepFilter (pat : String) (c : Content) : Content :=
+  match contentLines? c with
+  | some ls => linesToContent (ls.filter (lineMatches pat))
+  -- FIDELITY: on undecodable bytes real grep prints "Binary file ... matches" and
+  -- exits 0 if the pattern occurs; this model reports no match instead.
+  | none    => .empty
+
+/-- Insert `x` into a sorted line list, before the first `y` with `x ≤ y`.
+
+FIDELITY: collation is Lean's `String ≤`, i.e. lexicographic by Unicode codepoint,
+matching `LC_ALL=C sort`. Real `sort` is locale-dependent (LC_COLLATE) and would
+fold case / ignore punctuation under e.g. en_US.UTF-8; v1 fixes the C locale. -/
+def insertSortedLine (x : String) : List String → List String
+  | [] => [x]
+  | y :: ys => if x ≤ y then x :: y :: ys else y :: insertSortedLine x ys
+
+/-- Sort a line list. Stable and deterministic: `foldr` inserts from the right and
+`insertSortedLine` places `x` before the first `y ≥ x`, so equal lines keep input
+order. (Insertion sort — a specification, not a production sorter.) -/
+def sortLines (ls : List String) : List String :=
+  ls.foldr insertSortedLine []
+
+/-- Sort a content's lines (the `sort` content transform). -/
+def sortContent (c : Content) : Content :=
+  match contentLines? c with
+  | some ls => linesToContent (sortLines ls)
+  -- FIDELITY: undecodable bytes pass through unsorted rather than being dropped;
+  -- real `sort` would reorder them bytewise.
+  | none    => c
+
+/-- Collapse ADJACENT duplicate lines.
+
+FIDELITY: adjacent-only, exactly like real `uniq` — `uniq` alone does NOT dedup an
+unsorted file, only `sort | uniq` does. Deliberately no sort here; collapsing all
+duplicates would be the convenient-but-wrong implementation. -/
+def uniqAdjacent : List String → List String
+  | [] => []
+  | [x] => [x]
+  | x :: y :: rest =>
+      if x == y then uniqAdjacent (y :: rest) else x :: uniqAdjacent (y :: rest)
+
+/-- Collapse adjacent duplicate lines of a content (the `uniq` content transform). -/
+def uniqContent (c : Content) : Content :=
+  match contentLines? c with
+  | some ls => linesToContent (uniqAdjacent ls)
+  | none    => c
+
+/-! ## wc
+
+`wc` is specified over BYTES, not over the line model above -- see below. -/
+
+/-- The raw bytes of a content (UTF-8 encoding for text). Basis for `wc`, which is
+specified bytewise, not over the line model. -/
+def contentBytes : Content → ByteArray
+  | .empty    => ByteArray.empty
+  | .text s   => s.toUTF8
+  | .binary b => b
+
+/-- Whether a byte is ASCII whitespace (space, tab, NL, VT, FF, CR). -/
+def isSpaceByte (b : UInt8) : Bool :=
+  b == 0x20 || b == 0x09 || b == 0x0A || b == 0x0B || b == 0x0C || b == 0x0D
+
+/-- Count newline bytes.
+
+FIDELITY: `wc -l` counts NEWLINE BYTES, not "lines" as `textToLines` models them —
+on unterminated input they differ (`"a\nb"` has 1 newline but 2 lines). Counting
+newline bytes is the faithful choice; deliberately NOT `(textToLines s).length`. -/
+def countLineBytes (bs : List UInt8) : Nat :=
+  bs.foldl (fun acc b => if b == 0x0A then acc + 1 else acc) 0
+
+/-- Count words. FIDELITY: `wc -w` counts maximal runs of non-whitespace bytes. -/
+def countWordBytes (bs : List UInt8) : Nat :=
+  (bs.foldl (fun (st : Nat × Bool) b =>
+      if isSpaceByte b then (st.1, false)
+      else if st.2 then st else (st.1 + 1, true))
+    ((0 : Nat), false)).1
+
+/-- The `wc` content transform: emit line/word/byte counts of stdin.
+
+FIDELITY: default `wc` counts BYTES (`-c`), not codepoints (`-m`) — `"héllo"` is 6
+bytes but 5 codepoints; we count bytes. FIDELITY: output format is `"L W B\n"` with
+single spaces; real `wc` right-aligns in width-dependent columns and appends the
+filename. The three numbers are faithful; the spacing is not. -/
+def wcContent (c : Content) : Content :=
+  let bs := (contentBytes c).toList
+  .text s!"{countLineBytes bs} {countWordBytes bs} {bs.length}\n"
+
+/-! ## Command evaluation -/
+
+/-- Point update: the returned state differs from `s` only at `p` (set to `c`).
+Drives `write` (set) and `rm` (`none`). -/
+def updateState (s : FileState) (p : Path) (c : Option Content) : FileState :=
+  fun q => if q = p then c else s q
+
+/-- Execute a single command. The input `Content` is stdin (the previous stage's
+stdout); the output `Content` is stdout; the `FileState` in/out is the filesystem.
+Total and deterministic. Per-command exit codes and edge cases are the FIDELITY
+notes on each arm. -/
+def evalCmd : Cmd → FileState → Content → (FileState × Content × ExitCode)
+  -- FIDELITY: `read` ignores stdin, like `cat p`. A missing file yields no stdout
+  -- and exit 1, matching `cat`. The specific code 1 is a decision: `cat` uses 1,
+  -- but this model has no stderr on which to carry the diagnostic message.
+  | .read p, s, _ =>
+      match s p with
+      | some c => (s, c, .success)
+      | none   => (s, .empty, .failure 1)
+  -- `write` consumes stdin and produces NO stdout, like `> p` / `>> p`.
+  | .write p mode, s, stdin =>
+      let newC := match mode with
+        | .overwrite => stdin
+        | .append    => concatContent ((s p).getD .empty) stdin
+      (updateState s p (some newC), .empty, .success)
+  -- FIDELITY: grep exits 0 iff at least one line matched, else 1. (Real grep uses
+  -- 2 for errors, which this model cannot raise.) This exit code drives `&&`/`||`
+  -- and must be right even though v1's SafePipeline checks both branches anyway.
+  | .grep pat, s, stdin =>
+      let out := grepFilter pat stdin
+      match out with
+      | .empty => (s, .empty, .failure 1)
+      | _      => (s, out, .success)
+  | .sort, s, stdin => (s, sortContent stdin, .success)
+  | .uniq, s, stdin => (s, uniqContent stdin, .success)
+  | .wc,   s, stdin => (s, wcContent stdin, .success)
+  -- FIDELITY: `rm` without `-f` exits 1 on a missing path and removes nothing.
+  | .rm p, s, _ =>
+      match s p with
+      | some _ => (updateState s p none, .empty, .success)
+      | none   => (s, .empty, .failure 1)
+  -- FIDELITY: model has no directory concept. `FileState` is `Path → Option
+  -- Content`, so there is nothing that distinguishes a directory from a file.
+  -- Least-bad v1 behaviour: mark `p` as existing with `.empty` content, and fail
+  -- with exit 1 if `p` already exists (real `mkdir` without `-p` fails on an
+  -- existing path). Consequence: the model cannot distinguish "file exists" from
+  -- "directory exists", and a subsequent `read p` succeeds with empty output
+  -- whereas real `cat` on a directory errors. Real `mkdir` also fails when the
+  -- parent is missing; `Path` has no parent structure here, so that is not modeled.
+  | .mkdir p, s, _ =>
+      match s p with
+      | some _ => (s, .empty, .failure 1)
+      | none   => (updateState s p (some .empty), .empty, .success)
+
+/-! ## Pipeline evaluation -/
+
+/-- Execute a pipeline, threading state, stdin/stdout, and exit codes between
+stages. This is the internal helper that carries the final stdout; `evalPipeline`
+is the public wrapper that drops it. The operator-specific threading (pipe feeds
+stdout→stdin; `;`/`&&`/`||` give fresh stdin and branch on exit) is the FIDELITY
+notes on each arm, and is what `SafePipeline`/`checkFull` mirror. -/
+def evalPipelineFull : Pipeline → FileState → Content → (FileState × Content × ExitCode)
+  | .single c, s, stdin => evalCmd c s stdin
+  -- FIDELITY: `a`'s stdout becomes `b`'s stdin, and the pipeline's exit code is
+  -- the LAST command's exit -- bash's default without `set -o pipefail`. `a`'s
+  -- exit is discarded, so `false | true` exits 0.
+  | .pipe a b, s, stdin =>
+      let (s₁, outA, _) := evalPipelineFull a s stdin
+      evalPipelineFull b s₁ outA
+  -- FIDELITY: `;` is NOT a pipe. `b` runs regardless of `a`'s exit, on the
+  -- filesystem `a` left behind, with FRESH empty stdin -- it does not receive
+  -- `a`'s stdout. Exit is `b`'s exit.
+  | .seq a b, s, stdin =>
+      let (s₁, _, _) := evalPipelineFull a s stdin
+      evalPipelineFull b s₁ .empty
+  -- FIDELITY: `b` runs only when `a` succeeded, with fresh empty stdin.
+  | .andThen a b, s, stdin =>
+      let (s₁, outA, ecA) := evalPipelineFull a s stdin
+      match ecA with
+      | .success   => evalPipelineFull b s₁ .empty
+      | .failure n => (s₁, outA, .failure n)
+  -- FIDELITY: `b` runs only when `a` FAILED, with fresh empty stdin.
+  | .orElse a b, s, stdin =>
+      let (s₁, outA, ecA) := evalPipelineFull a s stdin
+      match ecA with
+      | .success   => (s₁, outA, .success)
+      | .failure _ => evalPipelineFull b s₁ .empty
+
+/-- Run a whole pipeline: the public denotation, returning only
+`(FileState × ExitCode)`. Starts from `.empty` stdin (nothing piped from a
+terminal) and drops the final stdout.
+
+SCOPE: dropping stdout means a pipeline that sends private data to unredirected
+stdout has no filesystem effect and is invisible to this model — a stated v1
+decision, not an oversight. See the `THREAT MODEL — stdout (v1)` note at the top of
+this file for the decision and the deployment assumption it rests on. -/
+def evalPipeline (p : Pipeline) (s : FileState) : FileState × ExitCode :=
+  let (s', _, ec) := evalPipelineFull p s .empty
+  (s', ec)
+
+/-! ## Noninterference helpers -/
+
+/-- Whether a path is public (class `publicRW` or `publicRO`) — i.e. observable in
+the noninterference guarantee. A boolean view of `classify`. -/
+def isPublicPath (p : Path) : Bool :=
+  match classify p with
+  | .publicRW  => true
+  | .publicRO  => true
+  | .privateRW => false
+  | .privateRO => false
+
+/-- Whether a single command touches only public paths: a path-carrying command
+(`read`/`write`/`rm`/`mkdir`) must be on a public path; stream ops carry no path
+and are unconstrained. -/
+def cmdTouchesOnlyPublic : Cmd → Bool
+  | .read p    => isPublicPath p
+  | .write p _ => isPublicPath p
+  | .rm p      => isPublicPath p
+  | .mkdir p   => isPublicPath p
+  | .grep _    => true
+  | .sort      => true
+  | .uniq      => true
+  | .wc        => true
+
+/-- `touchesOnlyPublic p` holds iff every path mentioned by any command in `p` is
+public. Used to gate conditional guards (`&&`/`||`): if a guard touches only public
+paths, its execution — hence its exit code — is determined solely by the public
+part of the state, so two states agreeing on all public paths run (or skip) the
+body identically. That closes an implicit exit-code flow channel: a guard reading a
+private path could otherwise branch on private state. Conservative (it rejects any
+conditional whose guard reads/writes/removes a private path) but sound — the standard "public
+program-counter" discipline from information-flow security. -/
+def touchesOnlyPublic : Pipeline → Bool
+  | .single c    => cmdTouchesOnlyPublic c
+  | .pipe a b    => touchesOnlyPublic a && touchesOnlyPublic b
+  | .seq a b     => touchesOnlyPublic a && touchesOnlyPublic b
+  | .andThen a b => touchesOnlyPublic a && touchesOnlyPublic b
+  | .orElse a b  => touchesOnlyPublic a && touchesOnlyPublic b
+
+/-- Restrict a filesystem to its public paths (private paths become `none`). The
+observable projection over which `shellwall_noninterference` is stated. -/
+def publicProjection (s : FileState) : FileState :=
+  fun p => if isPublicPath p then s p else none
+
+/-- Two filesystems agree on every public path. The hypothesis of
+`shellwall_noninterference`. Stated in pointwise `∀` form (rather than
+`publicProjection s₁ = publicProjection s₂`) as the more primitive form to consume
+in proofs. -/
+def agreeOnPublicPaths (s₁ s₂ : FileState) : Prop :=
+  ∀ p : Path, isPublicPath p = true → s₁ p = s₂ p
+
+/-! ## Forward provenance
+
+`cmdOutIsPublic`/`provOut` compute, FORWARD along execution, whether a command's or
+pipeline's stdout is "public-provenance": built only from reads of PUBLIC paths and
+public-preserving transforms. This is the notion that makes the safety spec
+relationally sound: unlike a per-state, value-based public predicate (which a private
+value coinciding with a public one satisfies), provenance is pinned to the paths READ,
+so agreeing states yield the same value. The decider and `SafeCmd`/`SafePipeline` both
+consume it, and it is defined here so both can. -/
+
+/-- Whether a command's stdout is public-PROVENANCE, given the state it runs in and
+whether its stdin is public-provenance. Reading a PRIVATE path yields `false` even if
+the bytes coincide with a public file's — provenance is pinned to the path read.
+Stream transforms preserve the flag; `wc`/writes/`rm`/`mkdir` are never public. -/
+def cmdOutIsPublic (c : Cmd) (s : FileState) (stdinPub : Bool) : Bool :=
+  match c with
+  -- a read is public-provenance iff the path is PUBLIC and present (a missing read
+  -- yields `.empty`, not certified public). Reading a private path ⇒ false.
+  | .read p => isPublicPath p && (s p).isSome
+  | .grep _ => stdinPub   -- public-preserving transform
+  | .sort   => stdinPub
+  | .uniq   => stdinPub
+  | .wc     => false      -- aggregation: never public (disclosure-leak exclusion)
+  | .write _ _ => false   -- emits `.empty`
+  | .rm _      => false
+  | .mkdir _   => false
+
+/-- Whether a whole pipeline's stdout is public-provenance, given whether its stdin
+is. Threads FORWARD exactly as `evalPipelineFull` runs (and as `checkFull`'s second
+component computes — `provOut_eq_checkFull_snd` in `Decide` proves they coincide).
+`;`/`&&`/`||` give the second stage fresh non-public (`false`) stdin; `&&`/`||` are
+exit-aware. -/
+def provOut : Pipeline → FileState → Content → Bool → Bool
+  | .single c, s, _stdin, pub => cmdOutIsPublic c s pub
+  | .pipe p₁ p₂, s, stdin, pub =>
+      provOut p₂ (evalPipelineFull p₁ s stdin).1 (evalPipelineFull p₁ s stdin).2.1
+        (provOut p₁ s stdin pub)
+  | .seq p₁ p₂, s, stdin, _pub =>
+      provOut p₂ (evalPipelineFull p₁ s stdin).1 .empty false
+  | .andThen p₁ p₂, s, stdin, pub =>
+      match (evalPipelineFull p₁ s stdin).2.2 with
+      | .success   => provOut p₂ (evalPipelineFull p₁ s stdin).1 .empty false
+      | .failure _ => provOut p₁ s stdin pub
+  | .orElse p₁ p₂, s, stdin, pub =>
+      match (evalPipelineFull p₁ s stdin).2.2 with
+      | .success   => provOut p₁ s stdin pub
+      | .failure _ => provOut p₂ (evalPipelineFull p₁ s stdin).1 .empty false
diff --git a/ShellWall/Syntax.lean b/ShellWall/Syntax.lean
new file mode 100644
index 0000000..d565ab9
--- /dev/null
+++ b/ShellWall/Syntax.lean
@@ -0,0 +1,38 @@
+import ShellWall.Basic
+
+/-- The closed-world set of commands v1 can represent. Anything not listed here is,
+by design, unrepresentable and therefore out of scope (and so cannot be certified
+safe). Closed-worldness is a security property, not an oversight. -/
+inductive Cmd where
+  /-- Read a file's content to stdout (`cat p`); ignores stdin. -/
+  | read    (p : Path)
+  /-- Write stdin to `p` under `mode` (`> p` / `>> p`); produces no stdout. -/
+  | write   (p : Path) (mode : WriteMode)
+  /-- Filter stdin to the lines matching `pattern` (fixed-substring; see
+  `grepFilter`). -/
+  | grep    (pattern : String)
+  /-- Sort stdin's lines (C-locale/codepoint order). -/
+  | sort
+  /-- Collapse adjacent duplicate lines of stdin (not a global dedup). -/
+  | uniq
+  /-- Emit line/word/byte counts of stdin. -/
+  | wc
+  /-- Remove `p` from the filesystem; ignores stdin, no stdout. -/
+  | rm      (p : Path)
+  /-- Create `p` as a directory (modeled as an empty entry; see `evalCmd`). -/
+  | mkdir   (p : Path)
+
+/-- A shell pipeline: a single command or two sub-pipelines joined by an operator.
+The operator determines how state, stdin/stdout, and exit codes thread between the
+two sides (see `evalPipelineFull`). -/
+inductive Pipeline where
+  /-- A lone command. -/
+  | single  (c : Cmd)
+  /-- `a | b` — `a`'s stdout feeds `b`'s stdin. -/
+  | pipe    (a b : Pipeline)
+  /-- `a ; b` — run `a` then `b` regardless of `a`'s exit; `b` gets fresh stdin. -/
+  | seq     (a b : Pipeline)
+  /-- `a && b` — run `b` only if `a` succeeds; `b` gets fresh stdin. -/
+  | andThen (a b : Pipeline)
+  /-- `a || b` — run `b` only if `a` fails; `b` gets fresh stdin. -/
+  | orElse  (a b : Pipeline)
diff --git a/Test.lean b/Test.lean
new file mode 100644
index 0000000..ae5ccf2
--- /dev/null
+++ b/Test.lean
@@ -0,0 +1,3 @@
+-- Root of the `Test` library: build-time test assertions. Elaborating this (part
+-- of `lake build`) checks the `checkSafe` battery; a moved verdict fails the build.
+import Test.Battery
diff --git a/Test/Battery.lean b/Test/Battery.lean
new file mode 100644
index 0000000..fe128e8
--- /dev/null
+++ b/Test/Battery.lean
@@ -0,0 +1,147 @@
+import Test.Fixtures
+open System
+
+/-! # Build-time `checkSafe` validation battery
+
+The 26-case battery (20 core + 6 conditional) as `#guard` assertions checked at
+ELABORATION time: any future change that moves a verdict fails `lake build`. Each
+guard is annotated with its bash-equivalent and the expected verdict + reason.
+
+(Plain `--` comments, not `/-- -/` docstrings: `#guard` is a command, not a
+declaration, so a doc comment has nothing to attach to.) -/
+
+namespace ShellWall.Test
+
+-- Case 1: `cat /home/alice/notes.txt` → permit (reading is never the violation).
+#guard checkSafe alice rdP s0 == true
+
+-- Case 2: `cat notes | > notes` (write own private file) → permit (write_private_ok).
+#guard checkSafe alice (.pipe rdP (.single (.write priv .overwrite))) s0 == true
+
+-- Case 3: `cat notes | > public/out` → reject (private content to a public path).
+#guard checkSafe alice (.pipe rdP (.single (.write pub .overwrite))) s0 == false
+
+-- Case 4: `cat /shared/ref | > public/out` → permit (public content to public path).
+#guard checkSafe alice (.pipe rdS (.single (.write pub .overwrite))) s0 == true
+
+-- Case 5a: write to `/shared/ref` (publicRO) → reject (read-only class).
+#guard checkSafe alice (.pipe rdS (.single (.write shr .overwrite))) s0 == false
+
+-- Case 5b: write to `/etc/passwd` (privateRO) → reject (read-only class).
+#guard checkSafe alice (.pipe rdS (.single (.write etcf .overwrite))) s0 == false
+
+-- Case 6a: write to `/home/bob/public/o` (unowned) → reject (CanWrite fails).
+#guard checkSafe alice (.pipe rdS (.single (.write bobpub .overwrite))) s0 == false
+
+-- Case 6b: write to `/tmp/t` (publicRW but system-owned) → reject (CanWrite fails).
+#guard checkSafe alice (.pipe rdS (.single (.write tmpf .overwrite))) s0 == false
+
+-- Case 7a: `rm /home/alice/notes.txt` (owned) → permit.
+#guard checkSafe alice (.single (.rm priv)) s0 == true
+
+-- Case 7b: `rm /etc/passwd` (unowned) → reject (CanWrite fails).
+#guard checkSafe alice (.single (.rm etcf)) s0 == false
+
+-- Case 8: `(cat shared | > notes) ; (cat notes | > public/out)` → reject
+-- (second stage writes private-sourced content to a public path).
+#guard checkSafe alice
+  (.seq (.pipe rdS (.single (.write priv .overwrite)))
+        (.pipe rdP (.single (.write pub .overwrite)))) s0 == false
+
+-- Case 8b: `(cat shared | > notes) ; (cat shared | > public/out)` → permit
+-- (control: both public-sourced).
+#guard checkSafe alice
+  (.seq (.pipe rdS (.single (.write priv .overwrite)))
+        (.pipe rdS (.single (.write pub .overwrite)))) s0 == true
+
+-- Case 9a: `cat shared | grep -F PUB | > public/out` → permit (grep of public is public).
+#guard checkSafe alice
+  (.pipe (.pipe rdS (.single (.grep "PUB"))) (.single (.write pub .overwrite))) s0 == true
+
+-- Case 9b: `cat shared | sort | > public/out` → permit (sort of public is public).
+#guard checkSafe alice
+  (.pipe (.pipe rdS (.single .sort)) (.single (.write pub .overwrite))) s0 == true
+
+-- Case 9c: `cat shared | uniq | > public/out` → permit (uniq preserves public provenance).
+#guard checkSafe alice
+  (.pipe (.pipe rdS (.single .uniq)) (.single (.write pub .overwrite))) s0 == true
+
+-- Case 9d: `cat shared | wc | > public/out` → reject (aggregation is never public).
+#guard checkSafe alice
+  (.pipe (.pipe rdS (.single .wc)) (.single (.write pub .overwrite))) s0 == false
+
+-- Case 10a: `cat shared | >> public/out` (append, existing public) → permit.
+#guard checkSafe alice (.pipe rdS (.single (.write pub .append))) s0 == true
+
+-- Case 10b: `cat notes | >> public/out` (append, private source) → reject.
+#guard checkSafe alice (.pipe rdP (.single (.write pub .append))) s0 == false
+
+-- Case 10c: `cat shared | >> public/o2` (append, absent target) → permit.
+#guard checkSafe alice (.pipe rdS (.single (.write pub2 .append))) s0 == true
+
+-- Case X: `cat /shared/nope | > public/out` (read absent public path) → reject
+-- (missing read yields non-public `.empty`).
+#guard checkSafe alice
+  (.pipe (.single (.read "/shared/nope")) (.single (.write pub .overwrite))) s0 == false
+
+/-! ## Conditional C-cases: `(cond) | write`, exercising the exit-aware output flag
+AND the public-guard requirement: a conditional whose guard touches a private path is
+rejected (`touchesOnlyPublic`). -/
+
+-- C1: `(cat gone && cat shared) | > public/out` → reject. The guard `cat gone`
+-- reads a PRIVATE path → touchesOnlyPublic fails. (Also rejected via the exit-aware
+-- flag, since stage 1 fails → non-public output.)
+#guard checkSafe alice (.pipe (.andThen rdG rdS) wr) s0 == false
+
+-- C2: `(cat shared && cat shared) | > public/out` → permit (stage 1 succeeds →
+-- stage 2 runs → public output).
+#guard checkSafe alice (.pipe (.andThen rdS rdS) wr) s0 == true
+
+-- C3: `(cat shared && cat notes) | > public/out` → reject (stage 2 runs → private).
+#guard checkSafe alice (.pipe (.andThen rdS rdP) wr) s0 == false
+
+-- C4: `(cat gone || cat shared) | > public/out` → REJECT. The guard `cat gone` reads
+-- a PRIVATE path, so the `||` could branch on private state (does the file exist?) →
+-- touchesOnlyPublic fails on the guard. This closes a real implicit-flow channel.
+#guard checkSafe alice (.pipe (.orElse rdG rdS) wr) s0 == false
+
+-- C5: `(cat shared || cat notes) | > public/out` → permit (stage 1 succeeds →
+-- output is stage 1's, public).
+#guard checkSafe alice (.pipe (.orElse rdS rdP) wr) s0 == true
+
+-- C6: `(cat notes || cat shared) | > public/out` → reject. The guard `cat notes`
+-- reads a PRIVATE path → touchesOnlyPublic fails. (Also: guard succeeds → stage 1's
+-- private output feeds the public write.)
+#guard checkSafe alice (.pipe (.orElse rdP rdS) wr) s0 == false
+
+-- Exit-code implicit-flow leak via a private-PATH guard, REJECTED by the public-guard
+-- rule: `(cat notes | grep SECRET) && (cat shared > public/out)` — the guard reads the
+-- private /home/alice/notes.txt, so touchesOnlyPublic fails and checkSafe rejects.
+-- Regression witness that the exit-code implicit flow stays closed.
+#guard checkSafe alice
+  (.andThen (.pipe rdP (.single (.grep "SECRET"))) (.pipe rdS wr)) s0 == false
+
+/-! ## Guard-STDIN implicit-flow channel and its controls -/
+
+-- The fourth counterexample, now REJECTED: `cat notes | (grep SECRET && (cat shared
+-- > public/out))`. The `&&` is fed (via the outer pipe) private stdin from `cat
+-- notes`; the guard `grep SECRET` filters that private stdin, so its exit — and
+-- thus whether the public write runs — leaks private data. `touchesOnlyPublic`
+-- passes (grep has no path), but the new stdin premise (`pub = true ∨ stdin =
+-- .empty`) fails: the conditional's incoming stdin is private-provenance.
+#guard checkSafe alice
+  (.pipe rdP (.andThen (.single (.grep "SECRET")) (.pipe rdS wr))) s0 == false
+
+-- Control A (`.empty`-stdin conditional must still permit): top-level
+-- `(cat shared && (cat shared > public/out))`. The guard reads a public path and
+-- the `&&`'s incoming stdin is the canonical `.empty` — this is the case that
+-- breaks if `.empty` isn't accepted as public-provenance.
+#guard checkSafe alice (.andThen rdS (.pipe rdS wr)) s0 == true
+
+-- Control B (public-fed conditional must still permit): `cat shared | (grep PUB &&
+-- (cat shared > public/out))`. The `&&`'s incoming stdin is public-provenance
+-- (`pub = true`, from the public read feeding the pipe), so the guard's stdin is
+-- public and the stdin premise holds.
+#guard checkSafe alice (.pipe rdS (.andThen (.single (.grep "PUB")) (.pipe rdS wr))) s0 == true
+
+end ShellWall.Test
diff --git a/Test/Fixtures.lean b/Test/Fixtures.lean
new file mode 100644
index 0000000..d66907a
--- /dev/null
+++ b/Test/Fixtures.lean
@@ -0,0 +1,54 @@
+import ShellWall
+open System
+
+/-! # Shared test fixtures
+
+Concrete `Owner`/`Path`/`FileState`/`Pipeline` values used by both the build-time
+`checkSafe` battery (`Test/Battery.lean`) and the runtime fidelity harness. Kept in
+one place so the two stay in sync. -/
+
+namespace ShellWall.Test
+
+/-- The agent under test. -/
+def alice : Owner := .agent "alice"
+
+/-! ## Model paths (abstract; the fidelity harness remaps these into a sandbox) -/
+
+/-- `/home/alice/notes.txt` — privateRW, alice-owned, present with SECRET content. -/
+def priv   : Path := "/home/alice/notes.txt"
+/-- `/home/alice/public/out.txt` — publicRW, alice-owned. -/
+def pub    : Path := "/home/alice/public/out.txt"
+/-- `/home/alice/public/o2.txt` — publicRW, alice-owned, absent. -/
+def pub2   : Path := "/home/alice/public/o2.txt"
+/-- `/shared/ref.txt` — publicRO, present with PUBDATA content. -/
+def shr    : Path := "/shared/ref.txt"
+/-- `/home/bob/public/o.txt` — publicRW, bob-owned (alice cannot write). -/
+def bobpub : Path := "/home/bob/public/o.txt"
+/-- `/tmp/t.txt` — publicRW but system-owned (agents cannot write in v1). -/
+def tmpf   : Path := "/tmp/t.txt"
+/-- `/etc/passwd` — privateRO. -/
+def etcf   : Path := "/etc/passwd"
+/-- `/home/alice/gone.txt` — privateRW, alice-owned, ABSENT (a read of it fails). -/
+def gone   : Path := "/home/alice/gone.txt"
+
+/-- The starting filesystem: `priv`, `shr`, `pub`, `tmpf` present; everything else
+absent. -/
+def s0 : FileState := fun p =>
+  if p = priv then some (.text "SECRET\n")
+  else if p = shr then some (.text "PUBDATA\n")
+  else if p = pub then some (.text "already\n")
+  else if p = tmpf then some (.text "tmp\n")
+  else none
+
+/-! ## Building-block pipelines -/
+
+/-- `cat /home/alice/notes.txt` (read a private file). -/
+def rdP : Pipeline := .single (.read priv)
+/-- `cat /shared/ref.txt` (read a public file). -/
+def rdS : Pipeline := .single (.read shr)
+/-- `cat /home/alice/gone.txt` (read an absent file → exit failure). -/
+def rdG : Pipeline := .single (.read gone)
+/-- `> /home/alice/public/out.txt` (overwrite a public path alice owns). -/
+def wr  : Pipeline := .single (.write pub .overwrite)
+
+end ShellWall.Test
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..35ecbef
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,96 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "ShellWall",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..afab67f
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,38 @@
+name = "ShellWall"
+version = "0.1.0"
+# `Test` is included so `lake build` elaborates Test/Battery.lean, whose `#guard`
+# assertions fail the build if any `checkSafe` verdict moves. The `fidelity` exe is
+# deliberately NOT a default target: it shells out to real bash, so it must be run
+# explicitly (`lake exe fidelity`), keeping `lake build` pure and hermetic.
+defaultTargets = ["shellwall", "Test"]
+
+# `autoImplicit` silently binds an unknown identifier appearing in a type as an
+# implicit type variable. In Prompt 04 that turned an accidentally-deleted
+# `Owner` declaration into an auto-bound generic, letting a meaningless
+# definition typecheck; the error surfaced several lines away as a confusing
+# "invalid dotted identifier". For a project whose entire value rests on a green
+# build MEANING something, that failure mode is unacceptable.
+# Applies to ShellWall's own modules only -- dependencies compile with their own
+# options, so Mathlib is unaffected.
+[leanOptions]
+autoImplicit = false
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+rev = "v4.31.0"
+
+
+[[lean_lib]]
+name = "ShellWall"
+
+[[lean_lib]]
+name = "Test"
+
+[[lean_exe]]
+name = "shellwall"
+root = "Main"
+
+[[lean_exe]]
+name = "fidelity"
+root = "FidelityMain"
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..18640c8
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.31.0