Created shell

.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

.gitignore

@@ -0,0 +1 @@
+/.lake

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

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"

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. -/

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)