iris-lean to prove SwapElementsSpec

codelib/CodeLib.lean

@@ -31,6 +31,10 @@ 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
 
 /-!
 # CodeLib — umbrella import for downstream code

codelib/CodeLib/SepLogic/WasmHeap.lean

@@ -0,0 +1,136 @@
+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 (DiscreteO (Option UInt8))) WasmHeapMap), by infer_instance⟩
+  | 5 => ⟨constOF (HeapView UInt32 (Agree (DiscreteO 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
+/-! ## Points-to assertions
+
+Byte-level `↦w` plus multi-byte and array derived forms.
+
+**Address arithmetic caveat:** the multi-byte assertions below compute
+their footprint with `UInt32` addition (`addr + 1`, …), which wraps
+mod 2^32, whereas the interpreter's `Mem.read64`/`write64` index bytes at
+`addr.toNat + k : Nat` with no wraparound. The two footprints agree only
+when the access does not overflow the 32-bit address space (e.g.
+`addr.toNat + 8 ≤ 2^32` for `pointsTo_u64`, and
+`ptr.toNat + 4 * xs.length ≤ 2^32` for `arrayAt`). Any future rule
+bridging these assertions to `Mem.read*/write*` must carry such a
+no-overflow side condition — without it the ghost footprint at high
+addresses wraps to low addresses and the bridge would be unprovable (or
+unsound if forced). -/
+section PointsTo
+variable [inst : WasmHeapGS]
+-- 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)))))
+end PointsTo
+end Wasm.SepLogic

codelib/CodeLib/SepLogic/WasmRules.lean

@@ -0,0 +1,61 @@
+import CodeLib.SepLogic.WasmHeap
+import Interpreter.Wasm
+
+/-! # Bridge: Talos Mem ↔ iris-lean GenHeap
+
+Defines `heapAgreesWithMem` — the agreement predicate between an abstract
+GenHeap state σ and physical `Mem.bytes` — together with per-byte load/store
+soundness lemmas for it.
+
+**Status: not yet wired into the WP.** Nothing in `wp_wasm_F`,
+`wasm_adequacy`, or `wasm_heap_adequacy` currently asserts this agreement:
+the ghost heap threaded through `wp_wasm` is a free-floating resource, so a
+`pointsTo` fact does not (yet) imply anything about `st.mem`. These
+definitions are the intended ingredient for a future state interpretation
+that maintains `heapAgreesWithMem σ st.mem` across steps; until that lands,
+memory facts in program proofs must come from pure hypotheses about
+`st.mem` (as the load/store rules in `Adequacy.lean` require).
+-/
+
+namespace Wasm.SepLogic
+
+open Iris Wasm Std
+
+/-! 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)
+
+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": "c2485783af2626575d171398c86cea8b3a6e79ad",
+   "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": "023ce7d62a0531e22a5331e20b587817a80d49ff",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.32.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.32.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": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
-   "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": "023ce7d62a0531e22a5331e20b587817a80d49ff",
-   "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,12 @@ packagesDir = "../.lake/packages"
 name = "WasmInterpreterLean"
 path = "../interpreter"
 
+[[require]]
+name = "iris"
+git.url = "https://github.com/leanprover-community/iris-lean.git"
+git.subDir = "Iris"
+# post-v4.32 bump (iris-lean#514); no v4.32.0 tag cut yet, so pin the commit
+git.rev = "c2485783af2626575d171398c86cea8b3a6e79ad"
+
 [[lean_lib]]
 name = "CodeLib"

programs/lean/Project.lean

@@ -6,6 +6,7 @@ import Project.RustArrayTests.Spec
 import Project.RustU64.Spec
 import Project.RustU64Tests.Spec
 import Project.SwapElements.Spec
+import Project.SwapElements.SwapSepLogic
 import Project.TotalVariation.Spec
 import Project.FloatTrunc.Spec
 import Project.FloatRound.Spec