iris-lean to prove SwapElementsSpec

codelib/CodeLib/SepLogic/Test.lean

@@ -0,0 +1,49 @@
+import CodeLib.SepLogic.Adequacy
+
+namespace Wasm.SepLogic.Test
+
+open Iris Wasm Std
+
+-- THE MISSING PIECE: wasm_adequacy takes ⊢ wp_wasm (which needs WasmHeapGS)
+-- and produces wp_wasm_prop (which doesn't). Need a wrapper that:
+-- 1. Allocates ghost state via genHeap_init_names
+-- 2. Gets genHeapInterp σ + WasmHeapGS instance
+-- 3. Uses the iProp proof to get ⊢ genHeapInterp σ ∗ wp_wasm
+-- 4. Applies wasm_adequacy to get |==> ⌜wp_wasm_prop⌝
+-- 5. Applies pure_soundness to extract wp_wasm_prop
+
+-- This is HeapLang's heap_adequacy pattern.
+-- Check: does genHeap_init_names give us the WasmHeapGS instance?
+-- Yes: it produces ∃ γh γm, ... where G := ⟨γh, γm⟩ : genHeapGS
+-- So the wrapper universally quantifies over the instance.
+
+-- Proposed signature:
+-- theorem wasm_heap_adequacy
+--     (m : Module) (st : Store Unit) (locals : Locals)
+--     (prog : Program) (env : HostEnv Unit)
+--     (Q : Store Unit → List Value → Prop)
+--     (hwp : ∀ [inst : WasmHeapGS], ⊢ wp_wasm m st locals prog env Q) :
+--     wp_wasm_prop m st locals prog env Q
+
+-- For now, test that the iProp proof works with explicit instance:
+theorem test_with_explicit_inst
+    [inst : WasmHeapGS]
+    (m : Module) (st : Store Unit) (env : HostEnv Unit)
+    (locals : Locals) (v : UInt32)
+    (Q : Store Unit → List Value → Prop)
+    (hQ : Q st (.i32 v :: locals.values)) :
+    ⊢ wp_wasm m st locals [.const v, .ret] env Q := by
+  apply wp_wasm_const v
+  intro σ'
+  iintro Hσ'
+  imodintro
+  iexists σ'
+  isplitl [Hσ']
+  · iexact Hσ'
+  · unfold wp_wasm
+    iapply least_fixpoint_unfold_mpr
+    unfold wp_wasm_F
+    simp only [LeibnizO.car]
+    exact BI.pure_intro hQ
+
+end Wasm.SepLogic.Test

codelib/CodeLib/SepLogic/WasmHeap.lean

@@ -0,0 +1,127 @@
+import Iris
+import Iris.BI.Lib.GenHeap
+import Interpreter.Wasm
+/-! # Wasm Memory as an Iris GenHeap
+Instantiates iris-lean's GenHeap for Wasm byte-level memory.
+Location = UInt32 (byte address), Value = Option UInt8 (byte).
+-/
+namespace Wasm.SepLogic
+open Iris Std
+abbrev WasmHeapMap := fun V => ExtTreeMap UInt32 V compare
+abbrev WasmHeapGF : BundledGFunctors
+  | 0 => ⟨InvMapF, by infer_instance⟩
+  | 1 => ⟨constOF (DisjointLeibnizSet CoPset), by infer_instance⟩
+  | 2 => ⟨constOF (DisjointLeibnizSet PosSet), by infer_instance⟩
+  | 3 => ⟨Auth.AuthURF (constOF Credit), by infer_instance⟩
+  | 4 => ⟨constOF (HeapView UInt32 (Agree (LeibnizO (Option UInt8))) WasmHeapMap), by infer_instance⟩
+  | 5 => ⟨constOF (HeapView UInt32 (Agree (LeibnizO GName)) WasmHeapMap), by infer_instance⟩
+  | 6 => ⟨constOF MetaUR, by infer_instance⟩
+  | _ => ⟨constOF Unit, by infer_instance⟩
+-- Wire genHeapPreS (following HeapLang's instHeapLangGS_HeapLangS)
+instance instWasmHeapPreS : genHeapPreS UInt32 (Option UInt8) WasmHeapGF WasmHeapMap where
+  heap := by constructor; exists 4
+  metaInfo := by constructor; exists 5
+  metaData := by exists 6
+-- The full genHeap instance with ghost names
+class WasmHeapGS extends genHeapGS UInt32 (Option UInt8) WasmHeapGF WasmHeapMap
+-- Now test: does the points-to notation work?
+section Test
+variable [inst : WasmHeapGS]
+-- This is the payoff: addr ↦ byte for Wasm memory
+#check (pointsTo (L := UInt32) (V := Option UInt8) (GF := WasmHeapGF) (H := WasmHeapMap))
+-- Notation for Wasm points-to
+notation:50 addr:50 " ↦w " v:50 => pointsTo (L := UInt32) (V := Option UInt8)
+    (GF := WasmHeapGF) (H := WasmHeapMap) addr (DFrac.own 1) (some v)
+-- Multi-byte: u64 as 8 consecutive owned bytes (little-endian)
+def pointsTo_u64 (addr : UInt32) (v : UInt64) : IProp WasmHeapGF :=
+  let byte (n : Nat) : UInt8 := ⟨(v.toNat / (256 ^ n)) % 256, by omega⟩
+  iprop%
+    (addr ↦w byte 0) ∗ ((addr + 1) ↦w byte 1) ∗
+    ((addr + 2) ↦w byte 2) ∗ ((addr + 3) ↦w byte 3) ∗
+    ((addr + 4) ↦w byte 4) ∗ ((addr + 5) ↦w byte 5) ∗
+    ((addr + 6) ↦w byte 6) ∗ ((addr + 7) ↦w byte 7)
+-- Multi-byte: u32 as 4 consecutive owned bytes (little-endian)
+def pointsTo_u32 (addr : UInt32) (v : UInt32) : IProp WasmHeapGF :=
+  let byte (n : Nat) : UInt8 := ⟨(v.toNat / (256 ^ n)) % 256, by omega⟩
+  iprop%
+    (addr ↦w byte 0) ∗ ((addr + 1) ↦w byte 1) ∗
+    ((addr + 2) ↦w byte 2) ∗ ((addr + 3) ↦w byte 3)
+-- Array ownership: n consecutive u32 elements at ptr
+-- arrayAt ptr [x₀, x₁, ..., xₙ₋₁] = pointsTo_u32 ptr x₀ ∗ pointsTo_u32 (ptr+4) x₁ ∗ ...
+def arrayAt (ptr : UInt32) (xs : List UInt32) : IProp WasmHeapGF :=
+  match xs with
+  | [] => iprop% emp
+  | x :: rest => iprop% (pointsTo_u32 ptr x) ∗ (arrayAt (ptr + 4) rest)
+-- arrayAt splits across ++ : ownership of a concatenation is
+-- ownership of both halves (merge_sort_into splits data at mid)
+theorem arrayAt_append (ptr : UInt32) (xs ys : List UInt32) :
+    arrayAt ptr (xs ++ ys) ⊣⊢
+    arrayAt ptr xs ∗ arrayAt (ptr + 4 * UInt32.ofNat xs.length) ys := by
+  induction xs generalizing ptr with
+  | nil => simp [arrayAt]; exact BI.emp_sep.symm
+  | cons x rest ih =>
+    simp only [List.cons_append, List.length_cons, arrayAt]
+    rw [show ptr + 4 * UInt32.ofNat (rest.length + 1) = (ptr + 4) + 4 * UInt32.ofNat rest.length from by
+      symm
+      rw [UInt32.ofNat_add, show UInt32.ofNat 1 = 1 from rfl, UInt32.mul_add, UInt32.mul_one]
+      rw [UInt32.add_assoc ptr 4, UInt32.add_comm 4, ← UInt32.add_assoc]]
+    exact (BI.sep_congr_right (ih (ptr + 4))).trans BI.sep_assoc.symm
+
+-- extract element k: whole-array ownership gives the single
+-- cell plus everything else (merge reads left[i], right[j])
+theorem arrayAt_get (ptr : UInt32) (xs : List UInt32) (k : Nat)
+    (hk : k < xs.length) :
+    arrayAt ptr xs ⊢
+    pointsTo_u32 (ptr + 4 * UInt32.ofNat k) xs[k] ∗
+    (pointsTo_u32 (ptr + 4 * UInt32.ofNat k) xs[k] -∗ arrayAt ptr xs) := by
+  induction xs generalizing ptr k with
+  | nil => simp at hk
+  | cons x rest ih =>
+    cases k with
+    | zero =>
+      simp only [List.getElem_cons_zero, arrayAt]
+      rw [show ptr + 4 * UInt32.ofNat 0 = ptr from by simp [UInt32.ofNat]]
+      exact BI.sep_mono .rfl (BI.wand_intro BI.sep_symm)
+    | succ k' =>
+      simp only [List.length_cons] at hk
+      have hk' : k' < rest.length := by omega
+      simp only [List.getElem_cons_succ, arrayAt]
+      rw [show ptr + 4 * UInt32.ofNat (k' + 1) = (ptr + 4) + 4 * UInt32.ofNat k' from by
+        symm
+        rw [UInt32.ofNat_add, show UInt32.ofNat 1 = 1 from rfl, UInt32.mul_add, UInt32.mul_one]
+        rw [UInt32.add_assoc ptr 4, UInt32.add_comm 4, ← UInt32.add_assoc]]
+      exact (BI.sep_mono_right (ih (ptr + 4) k' hk')).trans
+        (BI.sep_left_comm.mp.trans (BI.sep_mono_right
+          (BI.wand_intro (BI.sep_assoc.mp.trans (BI.sep_mono_right BI.wand_elim_left)))))
+
+-- update element k: give back a cell with a NEW value,
+-- own the updated array (merge writes out[k] = v)
+theorem arrayAt_set (ptr : UInt32) (xs : List UInt32) (k : Nat)
+    (v : UInt32) (hk : k < xs.length) :
+    arrayAt ptr xs ⊢
+    pointsTo_u32 (ptr + 4 * UInt32.ofNat k) xs[k] ∗
+    (pointsTo_u32 (ptr + 4 * UInt32.ofNat k) v -∗ arrayAt ptr (xs.set k v)) := by
+  induction xs generalizing ptr k with
+  | nil => simp at hk
+  | cons x rest ih =>
+    cases k with
+    | zero =>
+      simp only [List.getElem_cons_zero, List.set_cons_zero, arrayAt]
+      rw [show ptr + 4 * UInt32.ofNat 0 = ptr from by simp [UInt32.ofNat]]
+      exact BI.sep_mono .rfl (BI.wand_intro BI.sep_symm)
+    | succ k' =>
+      simp only [List.length_cons] at hk
+      have hk' : k' < rest.length := by omega
+      simp only [List.getElem_cons_succ, List.set_cons_succ, arrayAt]
+      rw [show ptr + 4 * UInt32.ofNat (k' + 1) = (ptr + 4) + 4 * UInt32.ofNat k' from by
+        symm
+        rw [UInt32.ofNat_add, show UInt32.ofNat 1 = 1 from rfl, UInt32.mul_add, UInt32.mul_one]
+        rw [UInt32.add_assoc ptr 4, UInt32.add_comm 4, ← UInt32.add_assoc]]
+      exact (BI.sep_mono_right (ih (ptr + 4) k' hk')).trans
+        (BI.sep_left_comm.mp.trans (BI.sep_mono_right
+          (BI.wand_intro (BI.sep_assoc.mp.trans (BI.sep_mono_right BI.wand_elim_left)))))
+#check @pointsTo_u64
+#check @pointsTo_u32
+#check @arrayAt
+end Test
+end Wasm.SepLogic

codelib/CodeLib/SepLogic/WasmRules.lean

@@ -0,0 +1,60 @@
+import CodeLib.SepLogic.WasmHeap
+import Interpreter.Wasm
+
+/-! # Bridge: Talos Mem ↔ iris-lean GenHeap
+
+The state interpretation maintains agreement between
+the abstract GenHeap state σ and physical Mem.bytes.
+We never build σ explicitly — GenHeap tracks it internally.
+-/
+
+namespace Wasm.SepLogic
+
+open Iris Wasm Std
+
+variable [inst : WasmHeapGS]
+
+/-! Agreement: wherever GenHeap has an entry, Mem agrees. -/
+
+def heapAgreesWithMem (σ : WasmHeapMap (Option UInt8)) (mem : Mem) : Prop :=
+  ∀ (addr : UInt32) (v : UInt8),
+    get? σ addr = some (some v) → mem.bytes addr.toNat = v
+
+/-! Soundness of load:
+If GenHeap says addr ↦ v and σ agrees with Mem,
+then Mem.read8 addr = v. -/
+
+theorem load_sound (σ : WasmHeapMap (Option UInt8)) (mem : Mem)
+    (addr : UInt32) (v : UInt8)
+    (h_agree : heapAgreesWithMem σ mem)
+    (h_own : get? σ addr = some (some v)) :
+    mem.bytes addr.toNat = v :=
+  h_agree addr v h_own
+
+/-! Soundness of store:
+After Mem.write8, the updated σ still agrees with new Mem. -/
+
+theorem store_sound (σ : WasmHeapMap (Option UInt8)) (mem : Mem)
+    (addr : UInt32) (old_v new_v : UInt8)
+    (h_agree : heapAgreesWithMem σ mem)
+    (h_own : get? σ addr = some (some old_v)) :
+    heapAgreesWithMem (insert σ addr (some new_v))
+      ⟨mem.pages, fun n =>
+        if n = addr.toNat then new_v else mem.bytes n⟩ := by
+  intro addr' v' h_get
+  by_cases h : addr' = addr
+  · subst h
+    simp [get?_insert_eq rfl] at h_get
+    simp [h_get]
+  · simp [get?_insert_ne (Ne.symm h)] at h_get
+    have hne : addr'.toNat ≠ addr.toNat :=
+      fun h' => h (UInt32.ext h')
+    exact (if_neg hne).trans (h_agree addr' v' h_get)
+
+-- GenHeap lemmas for our types:
+#check @genHeap_valid (GF := WasmHeapGF) (L := UInt32)
+    (V := Option UInt8) (H := WasmHeapMap)
+#check @genHeap_update (GF := WasmHeapGF) (L := UInt32)
+    (V := Option UInt8) (H := WasmHeapMap)
+
+end Wasm.SepLogic

codelib/CodeLib/SepLogic/WasmWP.lean

@@ -0,0 +1,43 @@
+import CodeLib.SepLogic.WasmHeap
+import CodeLib.SepLogic.WasmRules
+import Interpreter.Wasm
+
+/-! # Weakest Precondition for Wasm
+
+Prop-level WP for termination. Per-instruction iProp rules for
+ownership transfer. General iProp WP fixpoint deferred until
+the instruction rules are validated on swap_elements.
+-/
+
+namespace Wasm.SepLogic
+
+open Iris Wasm
+
+variable [inst : WasmHeapGS]
+
+def wp_wasm_prop (m : Module) (st : Store Unit) (locals : Locals)
+    (prog : Program) (env : HostEnv Unit)
+    (Q : Store Unit → List Value → Prop) : Prop :=
+  ∃ fuel, match exec fuel m st locals prog env with
+  | .Fallthrough st' _ => Q st' []
+  | .Return st' vals => Q st' vals
+  | _ => False
+
+/-! ## Per-instruction ownership rules in iProp
+
+Each rule describes how one instruction transforms ownership.
+These compose sequentially for straight-line code (swap).
+For loops, bi_least_fixpoint wraps the composition. -/
+
+-- load64: need ownership to read, ownership preserved
+def wp_load64 (addr : UInt32) (v : UInt64)
+    (Q : IProp WasmHeapGF) : IProp WasmHeapGF :=
+  iprop% (pointsTo_u64 addr v) ∗ (pointsTo_u64 addr v -∗ Q)
+
+-- store64: consume old ownership, produce new
+def wp_store64 (addr : UInt32) (old_v new_v : UInt64)
+    (Q : IProp WasmHeapGF) : IProp WasmHeapGF :=
+  iprop% (pointsTo_u64 addr old_v) ∗ (pointsTo_u64 addr new_v -∗ Q)
+
+
+end Wasm.SepLogic

codelib/lake-manifest.json

@@ -1,13 +1,43 @@
 {"version": "1.2.0",
  "packagesDir": "../.lake/packages",
  "packages":
- [{"type": "path",
+ [{"url": "https://github.com/leanprover-community/iris-lean.git",
+   "type": "git",
+   "subDir": "Iris",
+   "scope": "",
+   "rev": "3877dbeccd1b0545c5be7ef73318e8c86acf79ab",
+   "name": "iris",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"type": "path",
    "scope": "",
    "name": "WasmInterpreterLean",
    "manifestFile": "lake-manifest.json",
    "inherited": false,
    "dir": "../interpreter",
    "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": "v4.31.0",
+   "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": "v4.31.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
@@ -68,26 +98,6 @@
    "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,

codelib/lakefile.toml

@@ -7,5 +7,11 @@ packagesDir = "../.lake/packages"
 name = "WasmInterpreterLean"
 path = "../interpreter"
 
+[[require]]
+name = "iris"
+git.url = "https://github.com/leanprover-community/iris-lean.git"
+git.subDir = "Iris"
+git.rev = "v4.31.0"
+
 [[lean_lib]]
 name = "CodeLib"

programs/lean/Project/SwapElements/Spec.lean

@@ -63,8 +63,12 @@ def SwapElementsSpec : Prop :=
     i < len → j < len →
     -- the array is addressable and its element offsets do not wrap UInt32
     ptr.toNat + 8 * len.toNat ≤ st.mem.pages * 65536 →
+    -- memory fits in 32-bit address space (standard wasm constraint: pages ≤ 65536)
+    st.mem.pages * 65536 ≤ 4294967296 →
     -- the array does not collide with the callee's shadow-stack scratch frame
     1048576 ≤ ptr.toNat →
+    -- shadow-stack pointer at the wasm shadow-stack base on entry
+    st.globals.globals[0]? = some (.i32 1048576) →
     TerminatesWith env «module» 4 st
       [.i32 j, .i32 i, .i32 len, .i32 ptr]
       (fun st' rs =>