feat(correspondence): compiled Lean model as differential test oracle

Advances the Lean->Rust correspondence toward mechanization by making the
compiled proof artifact the test oracle.

- proofs/lean4/ModelOracle.lean + lean_exe model_oracle: compiles the exact
  proven model defs (mkdir/rmdir/createFile/deleteFile/fsUpdate from
  FilesystemModel + FileOperations) into a standalone executable that reports
  the node type (DIR/FILE/NONE) at probe paths.
- impl/rust-cli/tests/model_oracle_correspondence.rs: generates
  precondition-respecting op sequences (shadow tracker ensures validity),
  applies them to the real Rust ShellState, drives the same sequence through
  the Lean oracle, and asserts model and impl agree at every touched path.
  1218 probes agree across 200 sequences. Skips cleanly if the oracle is not
  built (no Lean toolchain required for ).
- just build-model-oracle / test-correspondence-model; wired into
  lean-verification.yml CI.
- docs/LEAN4_RUST_CORRESPONDENCE.md: documents the harness and, honestly, its
  limits — this is differential testing against the proof artifact, not a full
  refinement proof (still the v1.0 blocker). Records why the Coq extraction is
  not executable (Path -> option FSNode function domain + classical axioms in
  is_empty_dir_dec; needs FMaps.t FSNode migration) and the mechanization
  roadmap.

Verified: lake build model_oracle OK; oracle smoke test matches model
semantics (incl. non-recursive rmdir leaving orphan children); differential
test passes with and without VSH_MODEL_ORACLE env (auto-detects .lake path).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU

Author: claude

.github/workflows/lean-verification.yml

@@ -106,6 +106,18 @@ jobs:
           cargo test --test correspondence_tests
           cargo test --test property_correspondence_tests
 
+      - name: Build Lean model oracle (proof artifact as test oracle)
+        run: |
+          source $HOME/.elan/env
+          cd proofs/lean4
+          lake build model_oracle
+          ls -lh .lake/build/bin/model_oracle
+
+      - name: Differential correspondence (proven Lean model vs Rust impl)
+        run: |
+          cd impl/rust-cli
+          cargo test --test model_oracle_correspondence -- --nocapture
+
       - name: Report Rust binary size
         run: |
           echo "Rust binary: $(stat -c%s impl/rust-cli/target/release/vsh) bytes"

CHANGELOG.adoc

@@ -19,6 +19,24 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 === Added — 2026-07-17
 
+==== Correspondence (mechanized differential oracle)
+- `proofs/lean4/ModelOracle.lean` + `lean_exe model_oracle` — compiles the
+  **proven** Lean model definitions (`mkdir`/`rmdir`/`createFile`/`deleteFile`/
+  `fsUpdate`) into a standalone oracle that reports the node type at probe paths.
+- `impl/rust-cli/tests/model_oracle_correspondence.rs` — differential test that
+  generates precondition-respecting operation sequences, applies them to the real
+  Rust `ShellState`, runs the same sequence through the compiled Lean model, and
+  asserts they agree at every touched path. **1218 probes agree across 200
+  sequences.** This makes the proof artifact itself the test oracle (stronger
+  than hand-transcribed property tests); it remains differential testing, not a
+  full refinement proof — the latter is still the v1.0 blocker. The test skips
+  cleanly when the oracle is not built.
+- `just build-model-oracle` / `just test-correspondence-model`; wired into
+  `lean-verification.yml` CI.
+- `docs/LEAN4_RUST_CORRESPONDENCE.md` documents the harness, why the Coq
+  extraction is not executable (function-typed filesystem + classical axioms;
+  needs `FMaps.t FSNode` migration), and the roadmap to full mechanization.
+
 ==== Launcher (E-Grade Launcher Standard)
 - `launch.sh` — a standard-conformant launcher implementing the Hyperpolymath
   E-Grade Launcher Standard mode surface: `--auto` (default), `--start`,

Justfile

@@ -43,6 +43,18 @@ build-lean4:
     cd proofs/lean4 && lean FileOperations.lean
     @echo "✓ Lean 4 proofs checked"
 
+# Build the executable model oracle (the compiled proven Lean model) used by the
+# differential correspondence test impl/rust-cli/tests/model_oracle_correspondence.rs
+build-model-oracle:
+    @echo "Building Lean model oracle..."
+    cd proofs/lean4 && lake build model_oracle
+    @echo "✓ model oracle -> proofs/lean4/.lake/build/bin/model_oracle"
+
+# Run the differential correspondence test (proven Lean model vs Rust impl).
+# Builds the oracle first so the test does not skip.
+test-correspondence-model: build-model-oracle
+    cd impl/rust-cli && cargo test --test model_oracle_correspondence -- --nocapture
+
 # Build Agda proofs
 build-agda:
     @echo "Building Agda proofs..."

docs/LEAN4_RUST_CORRESPONDENCE.md

@@ -36,12 +36,74 @@ This document establishes the **correspondence** between:
 └──────────────────────────────┘
 ```
 
-**Verification Strategy**:
+**Verification Strategy** (weakest → strongest):
 - **Manual proofs**: Argue why Rust code matches Lean 4 spec
-- **Integration tests**: Validate behavior (28/28 passing)
-- **Echidna**: Property-based testing (planned)
+- **Integration tests**: Validate behavior
+- **Property tests**: Hand-transcribed reversibility laws checked generatively
+- **Mechanized differential oracle** *(new, 2026-07-17)*: the **compiled proven
+  Lean model** is executed as the test oracle — see below.
 - **Code review**: Multiple reviewers check correspondence
 
+## Mechanized differential correspondence (model-as-oracle)
+
+`proofs/lean4/ModelOracle.lean` compiles the **exact** proven model definitions
+(`mkdir`, `rmdir`, `createFile`, `deleteFile`, `fsUpdate` from `FilesystemModel`
++ `FileOperations`) into a standalone executable. Given an operation sequence and
+a set of probe paths, it reports the node type (`DIR`/`FILE`/`NONE`) the *model*
+computes at each path.
+
+`impl/rust-cli/tests/model_oracle_correspondence.rs` then:
+
+1. generates **precondition-respecting** operation sequences (the regime where the
+   reversibility theorems hold — a shadow tracker guarantees every op is valid);
+2. applies each sequence to the real Rust `ShellState` (a sandboxed temp dir);
+3. runs the same sequence through the compiled Lean model oracle;
+4. asserts the model and the implementation agree at **every** touched path.
+
+This is stronger than the property tests: the oracle is the **proof artifact
+itself**, not a hand-written re-statement of the laws. A divergence is a genuine
+model↔implementation mismatch. Current status: **1218 probes agree across 200
+sequences** (`just test-correspondence-model`).
+
+```mermaid
+flowchart LR
+  G[precondition-respecting<br/>op sequence] --> R[Rust ShellState<br/>real temp dir]
+  G --> O[compiled Lean model<br/>ModelOracle]
+  R --> C{agree at<br/>every probe?}
+  O --> C
+  C -->|yes| P[pass]
+  C -->|no| D[correspondence<br/>divergence]
+```
+
+### What this does and does not establish
+
+- ✅ It executes the **proven** model (not a paraphrase) as the reference.
+- ✅ It is reproducible and CI-gatable (`just build-model-oracle`).
+- ⚠️ It is still **differential testing**, not a mechanized *refinement proof*.
+  Full mechanization (a machine-checked proof that the Rust semantics refine the
+  model) remains the v1.0 blocker.
+
+### Why not extraction-based (Coq → OCaml)?
+
+The Coq model extracts (`proofs/coq/extraction.v`) but is **not executable**: the
+filesystem is modelled as a total function `Path → option FSNode` over an infinite
+domain, and `is_empty_dir_dec` pulls in classical axioms
+(`constructive_indefinite_description`, `excluded_middle_informative`) that the
+extracted OCaml leaves unrealized. Making the *Coq* model executable requires
+migrating the representation to a finite map (`FMaps.t FSNode`) and re-proving the
+theorems over it — the same migration the proof-holes audit already recommends.
+The Lean model sidesteps this because its operations are ordinary computable
+`def`s that can be evaluated at any finite probe path, even though the state is
+also a function.
+
+### Roadmap to full mechanization
+
+1. **(done)** Compiled-model differential oracle (this section).
+2. Migrate the Coq filesystem model to `FMaps.t FSNode`; re-prove; extract an
+   executable OCaml oracle and cross-check it against the Lean oracle.
+3. Model the Rust operational semantics (or a shared IR) and prove refinement —
+   the machine-checked correspondence that closes the v1.0 gap.
+
 ---
 
 ## Filesystem Model Correspondence