Integrate Iris small-step Wasm semantics

.github/workflows/lean_action_ci.yml

@@ -7,12 +7,29 @@ on:
   workflow_dispatch:
 
 jobs:
-  build:
-    name: Build & verify proofs
-    runs-on: ubuntu-latest
+  codelib:
+    name: Build CodeLib proofs
+    runs-on: macos-latest
+    steps:
+      - uses: actions/checkout@v5
+      - uses: actions/cache@v5
+        with:
+          path: .lake/packages
+          key: lake-pkgs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('interpreter/lake-manifest.json') }}
+          restore-keys: |
+            lake-pkgs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: codelib
+          build-args: "--wfail"
+          use-mathlib-cache: true
+
+  programs:
+    name: Build program proofs
+    runs-on: macos-latest
     steps:
-      - uses: actions/checkout@v4
-      - uses: actions/cache@v4
+      - uses: actions/checkout@v5
+      - uses: actions/cache@v5
         with:
           path: .lake/packages
           key: lake-pkgs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('interpreter/lake-manifest.json') }}
@@ -21,27 +38,16 @@ jobs:
       - uses: leanprover/lean-action@v1
         with:
           lake-package-directory: programs/lean
+          build-args: "Project --wfail"
           use-mathlib-cache: true
-      - name: Fail on build warnings
-        working-directory: programs/lean
-        run: |
-          set -o pipefail
-          # Rebuild (cached) and capture output. Warnings (e.g. `sorry`,
-          # unused-variable lints) are re-emitted on every build but do not
-          # change lake's exit code, so scan the log and fail if any appear.
-          lake build 2>&1 | tee build.log
-          if grep -E '(^|[[:space:]])warning:' build.log; then
-            echo "::error::Build produced warnings; warnings are not allowed."
-            exit 1
-          fi
 
   test:
     name: Smoke test
     runs-on: ubuntu-latest
-    needs: build
+    needs: [codelib, programs]
     steps:
-      - uses: actions/checkout@v4
-      - uses: actions/cache@v4
+      - uses: actions/checkout@v5
+      - uses: actions/cache@v5
         with:
           path: .lake/packages
           key: lake-pkgs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('interpreter/lake-manifest.json') }}

.github/workflows/testsuite-report.yml

@@ -13,11 +13,11 @@ jobs:
     name: Check testsuite_report.txt is up to date
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
         with:
           submodules: true
 
-      - uses: actions/cache@v4
+      - uses: actions/cache@v5
         with:
           path: .lake/packages
           key: lake-pkgs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('interpreter/lake-manifest.json') }}

.github/workflows/verifier-freshness.yml

@@ -11,7 +11,7 @@ jobs:
     name: Programs up to date
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
 
       # The verifier executable doesn't need Mathlib (see PR #12), so we
       # skip the mathlib cache entirely.

.github/workflows/verifier-report-preview.yml

@@ -27,7 +27,7 @@ jobs:
       VERCEL_ORG_ID: ${{ secrets.VERCEL_ORG_ID }}
       VERCEL_PROJECT_ID: ${{ secrets.VERCEL_PROJECT_ID }}
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
         with:
           # `verifier extract` records the repo commit; full history isn't
           # needed but a real .git is.

README.md

@@ -45,7 +45,7 @@ See [`interpreter/samples/factorial.wat`](interpreter/samples/factorial.wat) for
 
 **Prove something about it:**
 
-[`interpreter/Interpreter/Wasm/Examples/Factorial.lean`](interpreter/Interpreter/Wasm/Examples/Factorial.lean) shows a complete correctness proof using the WP tactic layer.
+[`interpreter/Interpreter/Wasm/Examples/Factorial.lean`](interpreter/Interpreter/Wasm/Examples/Factorial.lean) shows a complete correctness proof by composing instruction-granular small-step traces.
 
 ## Repository layout
 

codelib/CodeLib.lean

@@ -26,15 +26,18 @@ import CodeLib.RustStd.U64.Shr
 import CodeLib.RustStd.Array.Basic
 import CodeLib.RustStd.Array.Len
 import CodeLib.RustStd.Array.IsEmpty
+import CodeLib.RustStd.Array.SmallStep
 import CodeLib.RustStd.Option
 import CodeLib.Near.State
 import CodeLib.Near.Env
 import CodeLib.Near.Proof
 import CodeLib.IEEE32.Exec
 import CodeLib.SepLogic.WasmHeap
 import CodeLib.SepLogic.WasmRules
-import CodeLib.SepLogic.WasmWP
-import CodeLib.SepLogic.Adequacy
+import CodeLib.SepLogic.SmallStepLanguage
+import CodeLib.SepLogic.SmallStepState
+import CodeLib.SepLogic.SmallStepLifting
+import CodeLib.SepLogic.SmallStepAdequacy
 
 /-!
 # CodeLib — umbrella import for downstream code

codelib/CodeLib/Equivalence.lean

@@ -189,4 +189,157 @@ theorem ObservationallyEquiv.trans {env : HostEnv α}
     ObservationallyEquiv env m₁ id₁ m₃ id₃ initial args :=
   ObservationallyEquivOn.trans h₁₂ h₂₃
 
+/-! ## Authoritative small-step equivalence
+
+This is the cutover form of the relation above.  It observes finite executions
+of `SmallStep.Step` directly and therefore has no fuel or dependency on the
+legacy `run` function. -/
+
+namespace SmallStep
+
+/-- Terminal outcomes observed by equivalence.  Traps remain structural and
+are not collapsed into divergence. -/
+inductive ObservableOutcome where
+  | done (values : List Value)
+  | trapped (reason : TrapReason)
+  deriving BEq, Repr
+
+def ObservableOutcome.toExpr : ObservableOutcome → Expr α
+  | .done values => .done values
+  | .trapped reason => .trapped reason
+
+/-- A finite authoritative trace reaches a particular terminal outcome. -/
+def Reaches (config : Config α)
+    (outcome : ObservableOutcome) (store : MachineStore α) : Prop :=
+  ∃ trace, Steps config trace ⟨outcome.toExpr, store⟩
+
+/-- Two initialized configurations have exactly the same successful or
+trapping observable outcomes. -/
+def ObservationallyEquivOn
+    (config₁ config₂ : Config α) (obs : MachineStore α → β) : Prop :=
+  ∀ (outcome : ObservableOutcome) (o : β),
+    (∃ store, Reaches config₁ outcome store ∧ obs store = o) ↔
+    (∃ store, Reaches config₂ outcome store ∧ obs store = o)
+
+private theorem ObservableOutcome.toExpr_injective :
+    Function.Injective (ObservableOutcome.toExpr : ObservableOutcome → Expr α) := by
+  intro first second heq
+  cases first <;> cases second <;>
+    simp_all [ObservableOutcome.toExpr]
+
+/-- Determinism and terminal irreducibility make a reached outcome unique. -/
+theorem Reaches.outcome_unique_on
+    {config : Config α} {obs : MachineStore α → β}
+    {outcome outcome' : ObservableOutcome}
+    {store store' : MachineStore α} {o o' : β}
+    (first : Reaches config outcome store) (hfirst : obs store = o)
+    (second : Reaches config outcome' store') (hsecond : obs store' = o') :
+    outcome = outcome' ∧ o = o' := by
+  obtain ⟨trace, execution⟩ := first
+  obtain ⟨trace', execution'⟩ := second
+  have terminal (terminalOutcome : ObservableOutcome)
+      (kind : StepKind) (next : Config α) :
+      ¬Step ⟨terminalOutcome.toExpr, store⟩ kind next := by
+    cases terminalOutcome with
+    | done => exact done_terminal
+    | trapped => exact trapped_terminal
+  have terminal' (terminalOutcome : ObservableOutcome)
+      (kind : StepKind) (next : Config α) :
+      ¬Step ⟨terminalOutcome.toExpr, store'⟩ kind next := by
+    cases terminalOutcome with
+    | done => exact done_terminal
+    | trapped => exact trapped_terminal
+  have hconfig := steps_irreducible_deterministic execution execution'
+    (terminal outcome) (terminal' outcome')
+  have hparts := Config.mk.inj hconfig
+  have houtcome := ObservableOutcome.toExpr_injective hparts.1
+  exact
+    ⟨houtcome,
+      hfirst.symm.trans ((congrArg obs hparts.2).trans hsecond)⟩
+
+/-- A common reached terminal outcome discharges equivalence. -/
+theorem ObservationallyEquivOn.of_common_reached
+    {config₁ config₂ : Config α} {obs : MachineStore α → β}
+    {outcome : ObservableOutcome} {store₁ store₂ : MachineStore α} {o : β}
+    (first : Reaches config₁ outcome store₁) (hfirst : obs store₁ = o)
+    (second : Reaches config₂ outcome store₂) (hsecond : obs store₂ = o) :
+    ObservationallyEquivOn config₁ config₂ obs := by
+  intro candidate observed
+  constructor
+  · rintro ⟨store, reached, hobs⟩
+    obtain ⟨rfl, rfl⟩ :=
+      Reaches.outcome_unique_on reached hobs first hfirst
+    exact ⟨store₂, second, hsecond⟩
+  · rintro ⟨store, reached, hobs⟩
+    obtain ⟨rfl, rfl⟩ :=
+      Reaches.outcome_unique_on reached hobs second hsecond
+    exact ⟨store₁, first, hfirst⟩
+
+/-- A common normally terminating result is the main success-specialized
+discharge rule. -/
+theorem ObservationallyEquivOn.of_common_outcome
+    {config₁ config₂ : Config α} {obs : MachineStore α → β}
+    {r : List Value} {o : β}
+    (first : TerminatesWith config₁
+      (fun values store => values = r ∧ obs store = o))
+    (second : TerminatesWith config₂
+      (fun values store => values = r ∧ obs store = o)) :
+    ObservationallyEquivOn config₁ config₂ obs := by
+  obtain ⟨trace₁, values₁, store₁, execution₁, hvalues₁, hobs₁⟩ := first
+  obtain ⟨trace₂, values₂, store₂, execution₂, hvalues₂, hobs₂⟩ := second
+  subst values₁
+  subst values₂
+  apply ObservationallyEquivOn.of_common_reached
+    (outcome := .done r) (store₁ := store₁) (store₂ := store₂)
+  · exact ⟨trace₁, execution₁⟩
+  · exact hobs₁
+  · exact ⟨trace₂, execution₂⟩
+  · exact hobs₂
+
+/-- A common structural trap is an observable common outcome. -/
+theorem ObservationallyEquivOn.of_common_trap
+    {config₁ config₂ : Config α} {obs : MachineStore α → β}
+    {reason : TrapReason} {store₁ store₂ : MachineStore α} {o : β}
+    (first : Reaches config₁ (.trapped reason) store₁)
+    (hfirst : obs store₁ = o)
+    (second : Reaches config₂ (.trapped reason) store₂)
+    (hsecond : obs store₂ = o) :
+    ObservationallyEquivOn config₁ config₂ obs :=
+  ObservationallyEquivOn.of_common_reached first hfirst second hsecond
+
+theorem ObservationallyEquivOn.refl
+    (config : Config α) (obs : MachineStore α → β) :
+    ObservationallyEquivOn config config obs :=
+  fun _ _ => Iff.rfl
+
+theorem ObservationallyEquivOn.symm
+    {config₁ config₂ : Config α} {obs : MachineStore α → β}
+    (equivalent : ObservationallyEquivOn config₁ config₂ obs) :
+    ObservationallyEquivOn config₂ config₁ obs :=
+  fun outcome observed => (equivalent outcome observed).symm
+
+theorem ObservationallyEquivOn.trans
+    {config₁ config₂ config₃ : Config α} {obs : MachineStore α → β}
+    (first : ObservationallyEquivOn config₁ config₂ obs)
+    (second : ObservationallyEquivOn config₂ config₃ obs) :
+    ObservationallyEquivOn config₁ config₃ obs :=
+  fun outcome observed =>
+    (first outcome observed).trans (second outcome observed)
+
+/-- Host-state observation, deliberately ignoring module-private scratch
+memory as in the legacy relation. -/
+def ObservationallyEquiv (config₁ config₂ : Config α) : Prop :=
+  ObservationallyEquivOn config₁ config₂ (fun store => store.wasm.host)
+
+theorem ObservationallyEquiv.of_common_outcome
+    {config₁ config₂ : Config α} {r : List Value} {h : α}
+    (first : TerminatesWith config₁
+      (fun values store => values = r ∧ store.wasm.host = h))
+    (second : TerminatesWith config₂
+      (fun values store => values = r ∧ store.wasm.host = h)) :
+    ObservationallyEquiv config₁ config₂ :=
+  ObservationallyEquivOn.of_common_outcome first second
+
+end SmallStep
+
 end Wasm