diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 78826f9e0..dc2e9f25f 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -101,3 +101,26 @@ jobs:
         env:
           RPC_URL: http://127.0.0.1:8545
         run: ./scripts/deploy_example.sh
+
+  foundry-legacy:
+    name: Foundry legacy contract tests
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          persist-credentials: false
+          submodules: recursive
+
+      - name: Install Foundry
+        working-directory: research/lean_only_proto
+        run: ./scripts/install_foundry.sh
+
+      - name: Install solc
+        working-directory: research/lean_only_proto
+        run: ./scripts/install_solc.sh
+
+      - name: Run legacy Foundry tests
+        working-directory: legacy/foundry
+        run: forge test
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 000000000..5c26c82b3
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "legacy/foundry/lib/forge-std"]
+	path = legacy/foundry/lib/forge-std
+	url = https://github.com/foundry-rs/forge-std
diff --git a/STATUS.md b/STATUS.md
index 2abc9c36d..768fff2c9 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -8,14 +8,17 @@ Last updated: 2026-02-09
 - Keep the repo small and auditable.
 - Track the external tooling landscape (specs + formal verification).
 - Resolve spec aliasing hazards (sequential reads vs. forbid `from = to`).
+- Make examples smaller + build an ergonomic EDSL surface (stdlib, macros, patterns).
 
 ## In Progress
 - First compiler correctness lemma (arith + storage).
 - Memory model for ABI return encoding.
 - Spec shape for reverts (keep `Spec` minimal, add `SpecR`).
 - External landscape refresh (Act/Scribble/Certora/SMTChecker/KEVM).
- - Reconcile sequential-read vs old-state transfer specs (aliasing boundary).
+- Reconcile sequential-read vs old-state transfer specs (aliasing boundary).
 - Decide whether to guard old-state specs with `from ≠ to` or adopt sequential reads by default.
+- Supply accounting abstraction (list vs set/dedup semantics).
+- EDSL ergonomics: add helpers, notations, and a minimal stdlib for common patterns.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
@@ -35,6 +38,11 @@ Last updated: 2026-02-09
 - Added a self-transfer counterexample lemma showing `transferSpecR` cannot hold for `from = to` when `amount > 0`.
 - Proved sequential transfer spec is equivalent to old-state spec when `from ≠ to`.
 - Added a guarded transfer spec (`transferSpecRNoSelf`) and proof it meets execution when `from ≠ to`.
+- Added a counterexample lemma showing list-based supply accounting breaks with duplicates.
+- Split `Examples.lean` into multiple focused example modules (store ops, risk, token base, supply, transfer).
+- Added a minimal EDSL stdlib (`require`, `unless`, `assert`, `sloadSlot`, `sstoreSlot`, `v`, `n`) to reduce syntax noise.
+- Added `sloadVar`/`sstoreVar` helpers to cut boilerplate when using variable slots.
+- Added a `maxStore` example (stores max(a,b) into a slot) plus selector + Foundry test.
 - Minimal docs frontend and compressed docs.
 - Further docs tightening (shorter guide + text).
 - External landscape scan (spec languages, model checkers, prover stacks).
diff --git a/docs/research-log.md b/docs/research-log.md
index 545d2c776..1a1fb1ab5 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -16,6 +16,11 @@
 - Added a self-transfer counterexample lemma showing `transferSpecR` cannot hold for `from = to` when `amount > 0`.
 - Proved sequential transfer spec is equivalent to old-state spec when `from ≠ to`.
 - Added a guarded transfer spec (`transferSpecRNoSelf`) and proof it meets execution when `from ≠ to`.
+- Added a small counterexample lemma showing list-based supply accounting breaks with duplicates (motivation for sets/dedup).
+- Split `Examples.lean` into multiple focused example modules.
+- Added a minimal EDSL stdlib with common helpers (`require`, `unless`, `assert`, slot helpers, var/lit helpers).
+- Added `sloadVar`/`sstoreVar` stdlib helpers for variable slot access.
+- Added a tiny `maxStore` example (store max(a,b) into a slot) plus selector + Foundry test.
 - Refreshed external landscape notes (Act, Scribble, Certora, SMTChecker, KEVM, Kontrol).
 - Added selector map artifact (fixed + ABI keccak).
 - Fixed Foundry selectors and moved to Shanghai EVM.
diff --git a/legacy/foundry/foundry.lock b/legacy/foundry/foundry.lock
new file mode 100644
index 000000000..d0c0159b3
--- /dev/null
+++ b/legacy/foundry/foundry.lock
@@ -0,0 +1,8 @@
+{
+  "lib/forge-std": {
+    "tag": {
+      "name": "v1.14.0",
+      "rev": "1801b0541f4fda118a10798fd3486bb7051c5dd6"
+    }
+  }
+}
\ No newline at end of file
diff --git a/legacy/foundry/lib/forge-std b/legacy/foundry/lib/forge-std
new file mode 160000
index 000000000..1801b0541
--- /dev/null
+++ b/legacy/foundry/lib/forge-std
@@ -0,0 +1 @@
+Subproject commit 1801b0541f4fda118a10798fd3486bb7051c5dd6
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index d0c286a65..38b31382a 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -120,6 +120,20 @@ def exampleEntry4 : EntryPoint :=
     selector := 0x49f583e3
     returns := false }
 
+def exampleEntry5 : EntryPoint :=
+  { name := "maxStore"
+    args := ["slot", "a", "b"]
+    body := Lang.Stmt.if_
+      (Lang.Expr.gt (Lang.Expr.var "a") (Lang.Expr.var "b"))
+      (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "a"))
+      (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "b"))
+    -- maxStore(uint256,uint256,uint256) -> 0xb61d4088
+    selector := 0xb61d4088
+    returns := false }
+
+def exampleEntries : List EntryPoint :=
+  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5]
+
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
     args := ["collateral", "debt", "minHF"]
@@ -143,4 +157,7 @@ def healthEntryCheck : EntryPoint :=
     selector := 0x1753bbd7
     returns := false }
 
+def healthEntries : List EntryPoint :=
+  [healthEntrySet, healthEntryCheck]
+
 end DumbContracts.Compiler
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index cc89e5bd7..aaac514ec 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -23,13 +23,30 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH tag_addSlot"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x49f583e3"
   , "EQ"
   , "PUSH tag_guardedAddSlot"
   , "JUMPI"
+  , "PUSH4 0xb61d4088"
+  , "EQ"
+  , "PUSH tag_maxStore"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_maxStore:"
+  , "PUSH ret_maxStore"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH fn_maxStore"
+  , "JUMP"
+  , "ret_maxStore:"
+  , "STOP"
   , "tag_guardedAddSlot:"
   , "PUSH ret_guardedAddSlot"
   , "PUSH1 0x24"
@@ -110,6 +127,36 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH guardedAddSlot_check"
   , "JUMP"
+  , "fn_maxStore:"
+  , "SWAP1"
+  , "DUP3"
+  , "SWAP1"
+  , "DUP2"
+  , "DUP2"
+  , "GT"
+  , "PUSH maxStore_then"
+  , "JUMPI"
+  , "maxStore_check:"
+  , "GT"
+  , "ISZERO"
+  , "PUSH maxStore_else"
+  , "JUMPI"
+  , "maxStore_join:"
+  , "POP"
+  , "POP"
+  , "JUMP"
+  , "maxStore_else:"
+  , "SSTORE"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH maxStore_join"
+  , "JUMP"
+  , "maxStore_then:"
+  , "DUP1"
+  , "DUP4"
+  , "SSTORE"
+  , "PUSH maxStore_check"
+  , "JUMP"
   ]
 
 def pretty (lines : List String) : String :=
diff --git a/research/lean_only_proto/DumbContracts/Examples.lean b/research/lean_only_proto/DumbContracts/Examples.lean
index c703a1376..e4764e5f5 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -1,666 +1,6 @@
-import DumbContracts.Lang
-import DumbContracts.Semantics
-
-namespace DumbContracts.Examples
-
-open DumbContracts.Lang
-open DumbContracts.Semantics
-open DumbContracts
-
-def getSlotFun : Fun :=
-  { name := "getSlot"
-    args := ["slot"]
-    body := Stmt.return_ (Expr.sload (Expr.var "slot"))
-    ret := none }
-
-def setSlotFun : Fun :=
-  { name := "setSlot"
-    args := ["slot", "value"]
-    body := Stmt.sstore (Expr.var "slot") (Expr.var "value")
-    ret := none }
-
-def addSlotFun : Fun :=
-  { name := "addSlot"
-    args := ["slot", "delta"]
-    body := Stmt.sstore (Expr.var "slot") (Expr.add (Expr.sload (Expr.var "slot")) (Expr.var "delta"))
-    ret := none }
-
-def guardedAddSlotFun : Fun :=
-  { name := "guardedAddSlot"
-    args := ["slot", "delta"]
-    body := Stmt.if_
-      (Expr.gt (Expr.var "delta") (Expr.lit 0))
-      (Stmt.sstore (Expr.var "slot")
-        (Expr.add (Expr.sload (Expr.var "slot")) (Expr.var "delta")))
-      Stmt.revert
-    ret := none }
-
-def storeOf (k v : Nat) : Store :=
-  fun x => if x = k then v else 0
-
-def riskStore (collateral debt minHF : Nat) : Store :=
-  fun x =>
-    if x = 0 then collateral
-    else if x = 1 then debt
-    else if x = 2 then minHF
-    else 0
-
-def setRiskFun : Fun :=
-  { name := "setRisk"
-    args := ["collateral", "debt", "minHF"]
-    body :=
-      Stmt.sstore (Expr.lit 0) (Expr.var "collateral") ;;
-      Stmt.sstore (Expr.lit 1) (Expr.var "debt") ;;
-      Stmt.sstore (Expr.lit 2) (Expr.var "minHF")
-    ret := none }
-
-def checkHealthFun : Fun :=
-  { name := "checkHealth"
-    args := []
-    body := Stmt.if_
-      (Expr.lt (Expr.sload (Expr.lit 0))
-        (Expr.mul (Expr.sload (Expr.lit 1)) (Expr.sload (Expr.lit 2))))
-      Stmt.revert
-      Stmt.skip
-    ret := none }
-
-def balanceSlot (addr : Nat) : Nat :=
-  1000 + addr
-
-def totalSupplySlot : Nat :=
-  0
-
-def totalSupply (s : Store) : Nat :=
-  s totalSupplySlot
-
-def setBalance (s : Store) (addr val : Nat) : Store :=
-  updateStore s (balanceSlot addr) val
-
-def sum2 (s : Store) (a b : Nat) : Nat :=
-  s (balanceSlot a) + s (balanceSlot b)
-
-def sumBalances (s : Store) : List Nat -> Nat
-  | [] => 0
-  | a :: rest => s (balanceSlot a) + sumBalances rest
-
-theorem updateStore_same (s : Store) (k : Nat) :
-    updateStore s k (s k) = s := by
-  funext a
-  by_cases h : a = k
-  · simp [updateStore, updateNat, h]
-  · simp [updateStore, updateNat, h]
-
-theorem updateStore_shadow (s : Store) (k v1 v2 : Nat) :
-    updateStore (updateStore s k v1) k v2 = updateStore s k v2 := by
-  funext a
-  by_cases h : a = k
-  · simp [updateStore, updateNat, h]
-  · simp [updateStore, updateNat, h]
-
-theorem balanceSlot_ne (a b : Nat) (h : a ≠ b) : balanceSlot a ≠ balanceSlot b := by
-  intro h'
-  apply h
-  exact Nat.add_left_cancel h'
-
-theorem balanceSlot_ne_total (addr : Nat) : balanceSlot addr ≠ totalSupplySlot := by
-  simp [balanceSlot, totalSupplySlot]
-
-def transferFun : Fun :=
-  { name := "transfer"
-    args := ["from", "to", "amount"]
-    body := Stmt.if_
-      (Expr.eq (Expr.var "to") (Expr.lit 0))
-      Stmt.revert
-      (Stmt.if_
-        (Expr.lt (Expr.sload (Expr.add (Expr.lit 1000) (Expr.var "from"))) (Expr.var "amount"))
-        Stmt.revert
-        (Stmt.sstore
-            (Expr.add (Expr.lit 1000) (Expr.var "from"))
-            (Expr.sub
-              (Expr.sload (Expr.add (Expr.lit 1000) (Expr.var "from")))
-              (Expr.var "amount"))
-          ;;
-          Stmt.sstore
-            (Expr.add (Expr.lit 1000) (Expr.var "to"))
-            (Expr.add
-              (Expr.sload (Expr.add (Expr.lit 1000) (Expr.var "to")))
-              (Expr.var "amount"))))
-    ret := none }
-
-theorem getSlot_returns (slot value : Nat) :
-    execFun getSlotFun [slot] (storeOf slot value) [] =
-      ExecResult.returned [value] (bindArgs emptyEnv ["slot"] [slot]) (storeOf slot value) := by
-  simp [getSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv]
-
-theorem setSlot_updates (slot value : Nat) :
-    execFun setSlotFun [slot, value] (storeOf slot 0) [] =
-      ExecResult.ok (bindArgs emptyEnv ["slot", "value"] [slot, value]) (storeOf slot value) := by
-  simp [setSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore]
-
-theorem addSlot_updates (slot base delta : Nat) :
-    execFun addSlotFun [slot, delta] (storeOf slot base) [] =
-      ExecResult.ok (bindArgs emptyEnv ["slot", "delta"] [slot, delta]) (storeOf slot (base + delta)) := by
-  simp [addSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore]
-
-theorem set_then_get (slot value : Nat) :
-    (match execFun setSlotFun [slot, value] (storeOf slot 0) [] with
-      | ExecResult.ok _ store1 =>
-          execFun getSlotFun [slot] store1 [] =
-            ExecResult.returned [value] (bindArgs emptyEnv ["slot"] [slot]) (storeOf slot value)
-      | _ => False) := by
-  simp [setSlotFun, getSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore]
-
-theorem add_then_get (slot base delta : Nat) :
-    (match execFun addSlotFun [slot, delta] (storeOf slot base) [] with
-      | ExecResult.ok _ store1 =>
-          execFun getSlotFun [slot] store1 [] =
-            ExecResult.returned [base + delta] (bindArgs emptyEnv ["slot"] [slot]) (storeOf slot (base + delta))
-      | _ => False) := by
-  simp [addSlotFun, getSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore]
-
-theorem guarded_add_updates (slot base delta : Nat) (h : delta > 0) :
-    execFun guardedAddSlotFun [slot, delta] (storeOf slot base) [] =
-      ExecResult.ok (bindArgs emptyEnv ["slot", "delta"] [slot, delta]) (storeOf slot (base + delta)) := by
-  simp [guardedAddSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore, h]
-
-theorem guarded_add_reverts (slot base delta : Nat) (h : delta = 0) :
-    execFun guardedAddSlotFun [slot, delta] (storeOf slot base) [] =
-      ExecResult.reverted := by
-  simp [guardedAddSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore, h]
-
--- Storage specs (Store-level).
-def addSlotSpec (slot delta : Nat) : Spec Store :=
-  { requires := fun _ => True
-    ensures := fun s s' => s' = updateStore s slot (s slot + delta) }
-
-def guardedAddSlotSpec (slot delta : Nat) : Spec Store :=
-  { requires := fun _ => delta > 0
-    ensures := fun s s' => s' = updateStore s slot (s slot + delta) }
-
-def guardedAddSlotSpecR (slot delta : Nat) : SpecR Store :=
-  { requires := fun _ => delta > 0
-    ensures := fun s s' => s' = updateStore s slot (s slot + delta)
-    reverts := fun _ => delta = 0 }
-
-theorem addSlot_meets_spec (s : Store) (slot delta : Nat) :
-    (addSlotSpec slot delta).requires s ->
-    (match execFun addSlotFun [slot, delta] s [] with
-      | ExecResult.ok _ s' => (addSlotSpec slot delta).ensures s s'
-      | _ => False) := by
-  intro _hreq
-  simp [addSlotSpec, addSlotFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore]
-
-theorem guardedAddSlot_meets_spec (s : Store) (slot delta : Nat) :
-    (guardedAddSlotSpec slot delta).requires s ->
-    (match execFun guardedAddSlotFun [slot, delta] s [] with
-      | ExecResult.ok _ s' => (guardedAddSlotSpec slot delta).ensures s s'
-      | _ => False) := by
-  intro hreq
-  have hpos : delta > 0 := by exact hreq
-  simp [guardedAddSlotSpec, guardedAddSlotFun, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hpos]
-
-theorem guardedAddSlot_meets_specR_ok (s : Store) (slot delta : Nat) :
-    (guardedAddSlotSpecR slot delta).requires s ->
-    (match execFun guardedAddSlotFun [slot, delta] s [] with
-      | ExecResult.ok _ s' => (guardedAddSlotSpecR slot delta).ensures s s'
-      | _ => False) := by
-  intro hreq
-  have hpos : delta > 0 := by exact hreq
-  simp [guardedAddSlotSpecR, guardedAddSlotFun, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hpos]
-
-theorem guardedAddSlot_meets_specR_reverts (s : Store) (slot delta : Nat) :
-    (guardedAddSlotSpecR slot delta).reverts s ->
-    execFun guardedAddSlotFun [slot, delta] s [] = ExecResult.reverted := by
-  intro hrev
-  simp [guardedAddSlotSpecR, guardedAddSlotFun, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hrev]
-
-theorem guardedAddSlot_reverts_when_not_requires (slot delta : Nat) (h : delta = 0) :
-    (guardedAddSlotSpec slot delta).requires (storeOf slot 0) = False ∧
-    execFun guardedAddSlotFun [slot, delta] (storeOf slot 0) [] = ExecResult.reverted := by
-  constructor
-  · simp [guardedAddSlotSpec, h]
-  · simp [guardedAddSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv,
-      updateEnv, updateStore, h]
-
-theorem setRisk_updates (collateral debt minHF : Nat) :
-    execFun setRiskFun [collateral, debt, minHF] (riskStore 0 0 0) [] =
-      ExecResult.ok
-        (bindArgs emptyEnv ["collateral", "debt", "minHF"] [collateral, debt, minHF])
-        (riskStore collateral debt minHF) := by
-  simp [setRiskFun, execFun, execStmt, evalExpr, riskStore, bindArgs, emptyEnv, updateEnv, updateStore]
-
-theorem checkHealth_ok (collateral debt minHF : Nat) (h : debt * minHF <= collateral) :
-    execFun checkHealthFun [] (riskStore collateral debt minHF) [] =
-      ExecResult.ok (bindArgs emptyEnv [] []) (riskStore collateral debt minHF) := by
-  simp [checkHealthFun, execFun, execStmt, evalExpr, riskStore, bindArgs, emptyEnv, updateEnv, updateStore,
-    not_lt_of_ge h]
-
-theorem checkHealth_reverts (collateral debt minHF : Nat) (h : collateral < debt * minHF) :
-    execFun checkHealthFun [] (riskStore collateral debt minHF) [] =
-      ExecResult.reverted := by
-  simp [checkHealthFun, execFun, execStmt, evalExpr, riskStore, bindArgs, emptyEnv, updateEnv, updateStore, h]
-
--- Risk specs (Store-level).
-def setRiskSpec (collateral debt minHF : Nat) : Spec Store :=
-  { requires := fun _ => True
-    ensures := fun s s' =>
-      s' = updateStore (updateStore (updateStore s 0 collateral) 1 debt) 2 minHF }
-
-def riskOk (store : Store) : Prop :=
-  store 1 * store 2 <= store 0
-
-def checkHealthSpec : Spec Store :=
-  { requires := riskOk
-    ensures := fun s s' => s' = s }
-
-def checkHealthSpecR : SpecR Store :=
-  { requires := riskOk
-    ensures := fun s s' => s' = s
-    reverts := fun s => s 0 < s 1 * s 2 }
-
-theorem setRisk_meets_spec (s : Store) (collateral debt minHF : Nat) :
-    (setRiskSpec collateral debt minHF).requires s ->
-    (match execFun setRiskFun [collateral, debt, minHF] s [] with
-      | ExecResult.ok _ s' => (setRiskSpec collateral debt minHF).ensures s s'
-      | _ => False) := by
-  intro _hreq
-  simp [setRiskSpec, setRiskFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore]
-
-theorem checkHealth_meets_spec (s : Store) :
-    checkHealthSpec.requires s ->
-    (match execFun checkHealthFun [] s [] with
-      | ExecResult.ok _ s' => checkHealthSpec.ensures s s'
-      | _ => False) := by
-  intro hreq
-  simp [checkHealthSpec, riskOk, checkHealthFun, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, not_lt_of_ge hreq]
-
-theorem checkHealth_meets_specR_ok (s : Store) :
-    checkHealthSpecR.requires s ->
-    (match execFun checkHealthFun [] s [] with
-      | ExecResult.ok _ s' => checkHealthSpecR.ensures s s'
-      | _ => False) := by
-  intro hreq
-  simp [checkHealthSpecR, riskOk, checkHealthFun, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, not_lt_of_ge hreq]
-
-theorem checkHealth_meets_specR_reverts (s : Store) :
-    checkHealthSpecR.reverts s ->
-    execFun checkHealthFun [] s [] = ExecResult.reverted := by
-  intro hrev
-  simp [checkHealthSpecR, checkHealthFun, execFun, execStmt, evalExpr, bindArgs,
-    emptyEnv, updateEnv, updateStore, hrev]
-
--- Token-style specs (Store-level).
-def transferSpecR (from to amount : Nat) : SpecR Store :=
-  { requires := fun s => to ≠ 0 ∧ s (balanceSlot from) >= amount
-    ensures := fun s s' =>
-      s' =
-        setBalance
-          (setBalance s from (s (balanceSlot from) - amount))
-          to (s (balanceSlot to) + amount)
-    reverts := fun s => to = 0 ∨ s (balanceSlot from) < amount }
-
-def transferSpecRNoSelf (from to amount : Nat) : SpecR Store :=
-  { requires := fun s => to ≠ 0 ∧ from ≠ to ∧ s (balanceSlot from) >= amount
-    ensures := (transferSpecR from to amount).ensures
-    reverts := fun s => to = 0 ∨ from = to ∨ s (balanceSlot from) < amount }
-
-def transferStoreSeq (s : Store) (from to amount : Nat) : Store :=
-  let s1 := setBalance s from (s (balanceSlot from) - amount)
-  setBalance s1 to (s1 (balanceSlot to) + amount)
-
-def transferSpecRSeq (from to amount : Nat) : SpecR Store :=
-  { requires := fun s => to ≠ 0 ∧ s (balanceSlot from) >= amount
-    ensures := fun s s' => s' = transferStoreSeq s from to amount
-    reverts := fun s => to = 0 ∨ s (balanceSlot from) < amount }
-
-theorem transferStoreSeq_eq_transferSpecR_update (s : Store) (from to amount : Nat)
-    (hneq : from ≠ to) :
-    transferStoreSeq s from to amount =
-      setBalance
-        (setBalance s from (s (balanceSlot from) - amount))
-        to (s (balanceSlot to) + amount) := by
-  have hslot : balanceSlot from ≠ balanceSlot to := by
-    exact balanceSlot_ne from to hneq
-  have hs1 :
-      (setBalance s from (s (balanceSlot from) - amount)) (balanceSlot to) =
-        s (balanceSlot to) := by
-    simp [setBalance, updateStore, updateNat, hslot]
-  simp [transferStoreSeq, setBalance, updateStore, updateNat, hs1]
-
-theorem transferSpecRSeq_ensures_eq_transferSpecR (s s' : Store) (from to amount : Nat)
-    (hneq : from ≠ to) :
-    (transferSpecRSeq from to amount).ensures s s' ↔
-      (transferSpecR from to amount).ensures s s' := by
-  constructor
-  · intro hens
-    have hs : s' = transferStoreSeq s from to amount := by
-      simpa [transferSpecRSeq] using hens
-    have hs' :
-        s' =
-          setBalance
-            (setBalance s from (s (balanceSlot from) - amount))
-            to (s (balanceSlot to) + amount) := by
-      simpa [transferStoreSeq_eq_transferSpecR_update s from to amount hneq] using hs
-    simpa [transferSpecR] using hs'
-  · intro hens
-    have hs :
-        s' =
-          setBalance
-            (setBalance s from (s (balanceSlot from) - amount))
-            to (s (balanceSlot to) + amount) := by
-      simpa [transferSpecR] using hens
-    have hs' : s' = transferStoreSeq s from to amount := by
-      simpa [transferStoreSeq_eq_transferSpecR_update s from to amount hneq] using hs
-    simpa [transferSpecRSeq] using hs'
-
-theorem transfer_meets_specR_ok (s : Store) (from to amount : Nat) :
-    (transferSpecR from to amount).requires s ->
-    (match execFun transferFun [from, to, amount] s [] with
-      | ExecResult.ok _ s' => (transferSpecR from to amount).ensures s s'
-      | _ => False) := by
-  intro hreq
-  have hto : to ≠ 0 := hreq.left
-  have hbal : s (balanceSlot from) >= amount := hreq.right
-  have hnotlt : ¬ s (balanceSlot from) < amount := by
-    exact not_lt_of_ge hbal
-  simp [transferSpecR, transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv,
-    updateEnv, updateStore, balanceSlot, setBalance, hto, hnotlt]
-
-theorem transfer_meets_specRNoSelf_ok (s : Store) (from to amount : Nat) :
-    (transferSpecRNoSelf from to amount).requires s ->
-    (match execFun transferFun [from, to, amount] s [] with
-      | ExecResult.ok _ s' => (transferSpecRNoSelf from to amount).ensures s s'
-      | _ => False) := by
-  intro hreq
-  have hreq' : (transferSpecR from to amount).requires s := by
-    exact And.intro hreq.left hreq.right.right
-  simpa [transferSpecRNoSelf] using (transfer_meets_specR_ok s from to amount hreq')
-
-theorem transfer_meets_specRSeq_ok (s : Store) (from to amount : Nat) :
-    (transferSpecRSeq from to amount).requires s ->
-    (match execFun transferFun [from, to, amount] s [] with
-      | ExecResult.ok _ s' => (transferSpecRSeq from to amount).ensures s s'
-      | _ => False) := by
-  intro hreq
-  have hto : to ≠ 0 := hreq.left
-  have hbal : s (balanceSlot from) >= amount := hreq.right
-  have hnotlt : ¬ s (balanceSlot from) < amount := by
-    exact not_lt_of_ge hbal
-  simp [transferSpecRSeq, transferStoreSeq, transferFun, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, balanceSlot, setBalance, hto, hnotlt]
-
-theorem transfer_meets_specR_reverts (s : Store) (from to amount : Nat) :
-    (transferSpecR from to amount).reverts s ->
-    execFun transferFun [from, to, amount] s [] = ExecResult.reverted := by
-  intro hrev
-  cases hrev with
-  | inl hto =>
-      simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
-        updateStore, balanceSlot, setBalance, hto]
-  | inr hlt =>
-      by_cases hto : to = 0
-      · simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
-          updateStore, balanceSlot, setBalance, hto]
-      · simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
-          updateStore, balanceSlot, setBalance, hto, hlt]
-
-theorem transfer_self_noop (s : Store) (from amount : Nat)
-    (hto : from ≠ 0) (hbal : s (balanceSlot from) >= amount) :
-    execFun transferFun [from, from, amount] s [] =
-      ExecResult.ok (bindArgs emptyEnv ["from", "to", "amount"] [from, from, amount]) s := by
-  have hnotlt : ¬ s (balanceSlot from) < amount := by
-    exact not_lt_of_ge hbal
-  have hs :
-      execFun transferFun [from, from, amount] s [] =
-        ExecResult.ok
-          (bindArgs emptyEnv ["from", "to", "amount"] [from, from, amount])
-          (updateStore
-            (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
-            (balanceSlot from)
-            (s (balanceSlot from) - amount + amount)) := by
-    simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
-      updateStore, balanceSlot, hto, hnotlt]
-  have hshadow :
-      updateStore
-        (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
-        (balanceSlot from)
-        (s (balanceSlot from) - amount + amount)
-        =
-        updateStore s (balanceSlot from) (s (balanceSlot from) - amount + amount) := by
-    exact updateStore_shadow s (balanceSlot from)
-      (s (balanceSlot from) - amount) (s (balanceSlot from) - amount + amount)
-  have hval : s (balanceSlot from) - amount + amount = s (balanceSlot from) := by
-    exact Nat.sub_add_cancel hbal
-  have hs' :
-      updateStore
-        (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
-        (balanceSlot from)
-        (s (balanceSlot from) - amount + amount)
-        = s := by
-    calc
-      updateStore
-          (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
-          (balanceSlot from)
-          (s (balanceSlot from) - amount + amount)
-          =
-          updateStore s (balanceSlot from) (s (balanceSlot from) - amount + amount) := by
-            exact hshadow
-      _ = updateStore s (balanceSlot from) (s (balanceSlot from)) := by
-            simp [hval]
-      _ = s := by
-            exact updateStore_same s (balanceSlot from)
-  simpa [hs'] using hs
-
-theorem transferSpecRSeq_self_ensures_noop (s s' : Store) (from amount : Nat)
-    (hbal : s (balanceSlot from) >= amount)
-    (hens : (transferSpecRSeq from from amount).ensures s s') :
-    s' = s := by
-  have hval : s (balanceSlot from) - amount + amount = s (balanceSlot from) := by
-    exact Nat.sub_add_cancel hbal
-  have hs :
-      s' =
-        updateStore
-          (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
-          (balanceSlot from)
-          (s (balanceSlot from) - amount + amount) := by
-    simpa [transferSpecRSeq, transferStoreSeq, setBalance, updateStore, updateNat] using hens
-  have hshadow :
-      updateStore
-        (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
-        (balanceSlot from)
-        (s (balanceSlot from) - amount + amount)
-        =
-        updateStore s (balanceSlot from) (s (balanceSlot from) - amount + amount) := by
-    exact updateStore_shadow s (balanceSlot from)
-      (s (balanceSlot from) - amount) (s (balanceSlot from) - amount + amount)
-  have hs' :
-      s' = updateStore s (balanceSlot from) (s (balanceSlot from) - amount + amount) := by
-    calc
-      s' =
-          updateStore
-            (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
-            (balanceSlot from)
-            (s (balanceSlot from) - amount + amount) := by
-              exact hs
-      _ = updateStore s (balanceSlot from) (s (balanceSlot from) - amount + amount) := by
-              exact hshadow
-  calc
-    s' = updateStore s (balanceSlot from) (s (balanceSlot from)) := by
-          simpa [hval] using hs'
-    _ = s := by
-          exact updateStore_same s (balanceSlot from)
-
-theorem transferSpecR_self_balance_increases (s s' : Store) (from amount : Nat)
-    (hens : (transferSpecR from from amount).ensures s s') :
-    s' (balanceSlot from) = s (balanceSlot from) + amount := by
-  have hs :
-      s' =
-        setBalance
-          (setBalance s from (s (balanceSlot from) - amount))
-          from (s (balanceSlot from) + amount) := by
-    simpa [transferSpecR] using hens
-  have hshadow :
-      setBalance
-          (setBalance s from (s (balanceSlot from) - amount))
-          from (s (balanceSlot from) + amount)
-        =
-        setBalance s from (s (balanceSlot from) + amount) := by
-    simp [setBalance, updateStore_shadow]
-  calc
-    s' (balanceSlot from)
-        = (setBalance s from (s (balanceSlot from) + amount)) (balanceSlot from) := by
-            simpa [hs, hshadow]
-    _ = s (balanceSlot from) + amount := by
-            simp [setBalance, updateStore, updateNat]
-
-theorem transferSpecR_self_ensures_not_s (s : Store) (from amount : Nat)
-    (hpos : amount > 0) :
-    ¬ (transferSpecR from from amount).ensures s s := by
-  intro hens
-  have hbal :
-      s (balanceSlot from) = s (balanceSlot from) + amount := by
-    simpa using (transferSpecR_self_balance_increases s s from amount hens)
-  have h' : s (balanceSlot from) + amount = s (balanceSlot from) + 0 := by
-    simpa using hbal.symm
-  have hzero : amount = 0 := by
-    exact Nat.add_left_cancel h'
-  exact (ne_of_gt hpos) hzero
-
-theorem transfer_preserves_sum2 (s s' : Store) (from to amount : Nat)
-    (hreq : (transferSpecR from to amount).requires s) (hneq : from ≠ to) :
-    (transferSpecR from to amount).ensures s s' ->
-    sum2 s from to = sum2 s' from to := by
-  intro h
-  have hbal : amount <= s (balanceSlot from) := by
-    exact hreq.right
-  have hslot : balanceSlot from ≠ balanceSlot to := by
-    exact balanceSlot_ne from to hneq
-  have hs :
-      s' =
-        setBalance
-          (setBalance s from (s (balanceSlot from) - amount))
-          to (s (balanceSlot to) + amount) := by
-    simpa [transferSpecR] using h
-  calc
-    sum2 s from to
-        = s (balanceSlot from) + s (balanceSlot to) := by
-            simp [sum2]
-    _ = (s (balanceSlot from) - amount + amount) + s (balanceSlot to) := by
-            simp [Nat.sub_add_cancel hbal, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
-    _ = (s (balanceSlot from) - amount) + (s (balanceSlot to) + amount) := by
-            simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
-    _ = sum2 s' from to := by
-            simp [sum2, hs, setBalance, updateStore, updateNat, balanceSlot, hslot, Nat.add_assoc]
-
-theorem transfer_preserves_other_balance (s s' : Store) (from to amount addr : Nat)
-    (hfrom : addr ≠ from) (hto : addr ≠ to) :
-    (transferSpecR from to amount).ensures s s' ->
-    s' (balanceSlot addr) = s (balanceSlot addr) := by
-  intro h
-  have hs :
-      s' =
-        setBalance
-          (setBalance s from (s (balanceSlot from) - amount))
-          to (s (balanceSlot to) + amount) := by
-    simpa [transferSpecR] using h
-  have hslot_from : balanceSlot addr ≠ balanceSlot from := by
-    exact balanceSlot_ne addr from hfrom
-  have hslot_to : balanceSlot addr ≠ balanceSlot to := by
-    exact balanceSlot_ne addr to hto
-  simp [hs, setBalance, updateStore, updateNat, hslot_to, hslot_from]
-
-theorem transfer_preserves_sum_list (s s' : Store) (from to amount : Nat) (addrs : List Nat)
-    (hnotfrom : from ∉ addrs) (hnotto : to ∉ addrs)
-    (hens : (transferSpecR from to amount).ensures s s') :
-    sumBalances s addrs = sumBalances s' addrs := by
-  induction addrs with
-  | nil =>
-      simp [sumBalances]
-  | cons a rest ih =>
-      have hnotfrom' : a ≠ from := by
-        intro h
-        apply hnotfrom
-        simp [h]
-      have hnotto' : a ≠ to := by
-        intro h
-        apply hnotto
-        simp [h]
-      have hnotfrom_tail : from ∉ rest := by
-        intro hmem
-        apply hnotfrom
-        simp [hmem]
-      have hnotto_tail : to ∉ rest := by
-        intro hmem
-        apply hnotto
-        simp [hmem]
-      have hbal :
-          s' (balanceSlot a) = s (balanceSlot a) :=
-        transfer_preserves_other_balance s s' from to amount hnotfrom' hnotto' hens
-      have htail :
-          sumBalances s rest = sumBalances s' rest :=
-        ih hnotfrom_tail hnotto_tail hens
-      simp [sumBalances, hbal, htail]
-
-theorem transfer_preserves_sum_from_to_rest (s s' : Store) (from to amount : Nat) (rest : List Nat)
-    (hreq : (transferSpecR from to amount).requires s) (hneq : from ≠ to)
-    (hnotfrom : from ∉ rest) (hnotto : to ∉ rest)
-    (hens : (transferSpecR from to amount).ensures s s') :
-    sumBalances s (from :: to :: rest) = sumBalances s' (from :: to :: rest) := by
-  have hsum2 : sum2 s from to = sum2 s' from to :=
-    transfer_preserves_sum2 s s' from to amount hreq hneq hens
-  have hrest : sumBalances s rest = sumBalances s' rest :=
-    transfer_preserves_sum_list s s' from to amount rest hnotfrom hnotto hens
-  calc
-    sumBalances s (from :: to :: rest)
-        = (s (balanceSlot from) + s (balanceSlot to)) + sumBalances s rest := by
-            simp [sumBalances, Nat.add_assoc]
-    _ = (s' (balanceSlot from) + s' (balanceSlot to)) + sumBalances s rest := by
-            simpa [sum2] using hsum2
-    _ = (s' (balanceSlot from) + s' (balanceSlot to)) + sumBalances s' rest := by
-            simp [hrest]
-    _ = sumBalances s' (from :: to :: rest) := by
-            simp [sumBalances, Nat.add_assoc]
-
-theorem transfer_preserves_totalSupply (s s' : Store) (from to amount : Nat)
-    (hens : (transferSpecR from to amount).ensures s s') :
-    totalSupply s' = totalSupply s := by
-  have hs :
-      s' =
-        setBalance
-          (setBalance s from (s (balanceSlot from) - amount))
-          to (s (balanceSlot to) + amount) := by
-    simpa [transferSpecR] using hens
-  have hslot_from : balanceSlot from ≠ totalSupplySlot := by
-    exact balanceSlot_ne_total from
-  have hslot_to : balanceSlot to ≠ totalSupplySlot := by
-    exact balanceSlot_ne_total to
-  simp [totalSupply, hs, setBalance, updateStore, updateNat, hslot_to, hslot_from, totalSupplySlot]
-
-theorem transfer_preserves_supply_list (s s' : Store) (from to amount : Nat) (rest : List Nat)
-    (hreq : (transferSpecR from to amount).requires s) (hneq : from ≠ to)
-    (hnotfrom : from ∉ rest) (hnotto : to ∉ rest)
-    (hsupply : sumBalances s (from :: to :: rest) = totalSupply s)
-    (hens : (transferSpecR from to amount).ensures s s') :
-    sumBalances s' (from :: to :: rest) = totalSupply s' := by
-  have hsum :
-      sumBalances s (from :: to :: rest) = sumBalances s' (from :: to :: rest) :=
-    transfer_preserves_sum_from_to_rest s s' from to amount rest hreq hneq hnotfrom hnotto hens
-  have htot : totalSupply s' = totalSupply s :=
-    transfer_preserves_totalSupply s s' from to amount hens
-  calc
-    sumBalances s' (from :: to :: rest)
-        = sumBalances s (from :: to :: rest) := by
-            symm
-            exact hsum
-    _ = totalSupply s := by
-            exact hsupply
-    _ = totalSupply s' := by
-            symm
-            exact htot
-
-end DumbContracts.Examples
+import DumbContracts.Examples.StoreOps
+import DumbContracts.Examples.Risk
+import DumbContracts.Examples.TokenBase
+import DumbContracts.Examples.Supply
+import DumbContracts.Examples.TokenTransfer
+import DumbContracts.Examples.MaxStore
diff --git a/research/lean_only_proto/DumbContracts/Examples/MaxStore.lean b/research/lean_only_proto/DumbContracts/Examples/MaxStore.lean
new file mode 100644
index 000000000..fea620228
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/MaxStore.lean
@@ -0,0 +1,40 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Store the max of two inputs into a chosen slot. -/
+
+def maxStoreFun : Fun :=
+  { name := "maxStore"
+    args := ["slot", "a", "b"]
+    body :=
+      Stmt.if_
+        (Expr.gt (v "a") (v "b"))
+        (sstoreVar "slot" (v "a"))
+        (sstoreVar "slot" (v "b"))
+    ret := none }
+
+def maxStoreSpec (slot a b : Nat) : Spec Store :=
+  { requires := fun _ => True
+    ensures := fun s s' => s' = updateStore s slot (if a > b then a else b) }
+
+theorem maxStore_meets_spec (s : Store) (slot a b : Nat) :
+    (maxStoreSpec slot a b).requires s ->
+    (match execFun maxStoreFun [slot, a, b] s [] with
+      | ExecResult.ok _ s' => (maxStoreSpec slot a b).ensures s s'
+      | _ => False) := by
+  intro _hreq
+  by_cases h : a > b
+  · simp [maxStoreFun, maxStoreSpec, sstoreVar, v, execFun, execStmt, evalExpr, bindArgs, emptyEnv,
+      updateEnv, updateStore, h]
+  · simp [maxStoreFun, maxStoreSpec, sstoreVar, v, execFun, execStmt, evalExpr, bindArgs, emptyEnv,
+      updateEnv, updateStore, h]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/Risk.lean b/research/lean_only_proto/DumbContracts/Examples/Risk.lean
new file mode 100644
index 000000000..2fb438d83
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/Risk.lean
@@ -0,0 +1,117 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Storage layout for the simple risk model. -/
+
+def riskStore (collateral debt minHF : Nat) : Store :=
+  fun x =>
+    if x = 0 then collateral
+    else if x = 1 then debt
+    else if x = 2 then minHF
+    else 0
+
+/-- Set collateral, debt, and minHF in slots 0/1/2. -/
+
+def setRiskFun : Fun :=
+  { name := "setRisk"
+    args := ["collateral", "debt", "minHF"]
+    body :=
+      sstoreSlot 0 (v "collateral") ;;
+      sstoreSlot 1 (v "debt") ;;
+      sstoreSlot 2 (v "minHF")
+    ret := none }
+
+/-- Revert when collateral < debt * minHF. -/
+
+def checkHealthFun : Fun :=
+  { name := "checkHealth"
+    args := []
+    body := unless
+      (Expr.lt (sloadSlot 0) (Expr.mul (sloadSlot 1) (sloadSlot 2)))
+      Stmt.skip
+    ret := none }
+
+-- Execution facts.
+
+theorem setRisk_updates (collateral debt minHF : Nat) :
+    execFun setRiskFun [collateral, debt, minHF] (riskStore 0 0 0) [] =
+      ExecResult.ok
+        (bindArgs emptyEnv ["collateral", "debt", "minHF"] [collateral, debt, minHF])
+        (riskStore collateral debt minHF) := by
+  simp [setRiskFun, sstoreSlot, v, execFun, execStmt, evalExpr, riskStore, bindArgs,
+    emptyEnv, updateEnv, updateStore]
+
+theorem checkHealth_ok (collateral debt minHF : Nat) (h : debt * minHF <= collateral) :
+    execFun checkHealthFun [] (riskStore collateral debt minHF) [] =
+      ExecResult.ok (bindArgs emptyEnv [] []) (riskStore collateral debt minHF) := by
+  simp [checkHealthFun, unless, sloadSlot, execFun, execStmt, evalExpr, riskStore,
+    bindArgs, emptyEnv, updateEnv, updateStore, not_lt_of_ge h]
+
+theorem checkHealth_reverts (collateral debt minHF : Nat) (h : collateral < debt * minHF) :
+    execFun checkHealthFun [] (riskStore collateral debt minHF) [] =
+      ExecResult.reverted := by
+  simp [checkHealthFun, unless, sloadSlot, execFun, execStmt, evalExpr, riskStore,
+    bindArgs, emptyEnv, updateEnv, updateStore, h]
+
+-- Risk specs (Store-level).
+
+def setRiskSpec (collateral debt minHF : Nat) : Spec Store :=
+  { requires := fun _ => True
+    ensures := fun s s' =>
+      s' = updateStore (updateStore (updateStore s 0 collateral) 1 debt) 2 minHF }
+
+def riskOk (store : Store) : Prop :=
+  store 1 * store 2 <= store 0
+
+def checkHealthSpec : Spec Store :=
+  { requires := riskOk
+    ensures := fun s s' => s' = s }
+
+def checkHealthSpecR : SpecR Store :=
+  { requires := riskOk
+    ensures := fun s s' => s' = s
+    reverts := fun s => s 0 < s 1 * s 2 }
+
+theorem setRisk_meets_spec (s : Store) (collateral debt minHF : Nat) :
+    (setRiskSpec collateral debt minHF).requires s ->
+    (match execFun setRiskFun [collateral, debt, minHF] s [] with
+      | ExecResult.ok _ s' => (setRiskSpec collateral debt minHF).ensures s s'
+      | _ => False) := by
+  intro _hreq
+  simp [setRiskSpec, setRiskFun, sstoreSlot, v, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore]
+
+theorem checkHealth_meets_spec (s : Store) :
+    checkHealthSpec.requires s ->
+    (match execFun checkHealthFun [] s [] with
+      | ExecResult.ok _ s' => checkHealthSpec.ensures s s'
+      | _ => False) := by
+  intro hreq
+  simp [checkHealthSpec, riskOk, checkHealthFun, unless, sloadSlot, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, not_lt_of_ge hreq]
+
+theorem checkHealth_meets_specR_ok (s : Store) :
+    checkHealthSpecR.requires s ->
+    (match execFun checkHealthFun [] s [] with
+      | ExecResult.ok _ s' => checkHealthSpecR.ensures s s'
+      | _ => False) := by
+  intro hreq
+  simp [checkHealthSpecR, riskOk, checkHealthFun, unless, sloadSlot, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, not_lt_of_ge hreq]
+
+theorem checkHealth_meets_specR_reverts (s : Store) :
+    checkHealthSpecR.reverts s ->
+    execFun checkHealthFun [] s [] = ExecResult.reverted := by
+  intro hrev
+  simp [checkHealthSpecR, checkHealthFun, unless, sloadSlot, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean b/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
new file mode 100644
index 000000000..1e809ace8
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
@@ -0,0 +1,149 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Simple storage helpers. -/
+
+def getSlotFun : Fun :=
+  { name := "getSlot"
+    args := ["slot"]
+    body := Stmt.return_ (Expr.sload (Expr.var "slot"))
+    ret := none }
+
+def setSlotFun : Fun :=
+  { name := "setSlot"
+    args := ["slot", "value"]
+    body := Stmt.sstore (Expr.var "slot") (Expr.var "value")
+    ret := none }
+
+def addSlotFun : Fun :=
+  { name := "addSlot"
+    args := ["slot", "delta"]
+    body := Stmt.sstore (Expr.var "slot") (Expr.add (Expr.sload (Expr.var "slot")) (Expr.var "delta"))
+    ret := none }
+
+def guardedAddSlotFun : Fun :=
+  { name := "guardedAddSlot"
+    args := ["slot", "delta"]
+    body := require
+      (Expr.gt (Expr.var "delta") (Expr.lit 0))
+      (Stmt.sstore (Expr.var "slot")
+        (Expr.add (Expr.sload (Expr.var "slot")) (Expr.var "delta")))
+    ret := none }
+
+/-- A minimal store for point examples. -/
+
+def storeOf (k v : Nat) : Store :=
+  fun x => if x = k then v else 0
+
+-- Tests and execution facts.
+
+theorem getSlot_returns (slot value : Nat) :
+    execFun getSlotFun [slot] (storeOf slot value) [] =
+      ExecResult.returned [value] (bindArgs emptyEnv ["slot"] [slot]) (storeOf slot value) := by
+  simp [getSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv]
+
+theorem setSlot_updates (slot value : Nat) :
+    execFun setSlotFun [slot, value] (storeOf slot 0) [] =
+      ExecResult.ok (bindArgs emptyEnv ["slot", "value"] [slot, value]) (storeOf slot value) := by
+  simp [setSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore]
+
+theorem addSlot_updates (slot base delta : Nat) :
+    execFun addSlotFun [slot, delta] (storeOf slot base) [] =
+      ExecResult.ok (bindArgs emptyEnv ["slot", "delta"] [slot, delta]) (storeOf slot (base + delta)) := by
+  simp [addSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore]
+
+theorem set_then_get (slot value : Nat) :
+    (match execFun setSlotFun [slot, value] (storeOf slot 0) [] with
+      | ExecResult.ok _ store1 =>
+          execFun getSlotFun [slot] store1 [] =
+            ExecResult.returned [value] (bindArgs emptyEnv ["slot"] [slot]) (storeOf slot value)
+      | _ => False) := by
+  simp [setSlotFun, getSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore]
+
+theorem add_then_get (slot base delta : Nat) :
+    (match execFun addSlotFun [slot, delta] (storeOf slot base) [] with
+      | ExecResult.ok _ store1 =>
+          execFun getSlotFun [slot] store1 [] =
+            ExecResult.returned [base + delta] (bindArgs emptyEnv ["slot"] [slot]) (storeOf slot (base + delta))
+      | _ => False) := by
+  simp [addSlotFun, getSlotFun, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore]
+
+theorem guarded_add_updates (slot base delta : Nat) (h : delta > 0) :
+    execFun guardedAddSlotFun [slot, delta] (storeOf slot base) [] =
+      ExecResult.ok (bindArgs emptyEnv ["slot", "delta"] [slot, delta]) (storeOf slot (base + delta)) := by
+  simp [guardedAddSlotFun, require, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv,
+    updateEnv, updateStore, h]
+
+theorem guarded_add_reverts (slot base delta : Nat) (h : delta = 0) :
+    execFun guardedAddSlotFun [slot, delta] (storeOf slot base) [] =
+      ExecResult.reverted := by
+  simp [guardedAddSlotFun, require, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv,
+    updateEnv, updateStore, h]
+
+-- Storage specs (Store-level).
+
+def addSlotSpec (slot delta : Nat) : Spec Store :=
+  { requires := fun _ => True
+    ensures := fun s s' => s' = updateStore s slot (s slot + delta) }
+
+def guardedAddSlotSpec (slot delta : Nat) : Spec Store :=
+  { requires := fun _ => delta > 0
+    ensures := fun s s' => s' = updateStore s slot (s slot + delta) }
+
+def guardedAddSlotSpecR (slot delta : Nat) : SpecR Store :=
+  { requires := fun _ => delta > 0
+    ensures := fun s s' => s' = updateStore s slot (s slot + delta)
+    reverts := fun _ => delta = 0 }
+
+theorem addSlot_meets_spec (s : Store) (slot delta : Nat) :
+    (addSlotSpec slot delta).requires s ->
+    (match execFun addSlotFun [slot, delta] s [] with
+      | ExecResult.ok _ s' => (addSlotSpec slot delta).ensures s s'
+      | _ => False) := by
+  intro _hreq
+  simp [addSlotSpec, addSlotFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore]
+
+theorem guardedAddSlot_meets_spec (s : Store) (slot delta : Nat) :
+    (guardedAddSlotSpec slot delta).requires s ->
+    (match execFun guardedAddSlotFun [slot, delta] s [] with
+      | ExecResult.ok _ s' => (guardedAddSlotSpec slot delta).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hpos : delta > 0 := by exact hreq
+  simp [guardedAddSlotSpec, guardedAddSlotFun, require, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hpos]
+
+theorem guardedAddSlot_meets_specR_ok (s : Store) (slot delta : Nat) :
+    (guardedAddSlotSpecR slot delta).requires s ->
+    (match execFun guardedAddSlotFun [slot, delta] s [] with
+      | ExecResult.ok _ s' => (guardedAddSlotSpecR slot delta).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hpos : delta > 0 := by exact hreq
+  simp [guardedAddSlotSpecR, guardedAddSlotFun, require, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hpos]
+
+theorem guardedAddSlot_meets_specR_reverts (s : Store) (slot delta : Nat) :
+    (guardedAddSlotSpecR slot delta).reverts s ->
+    execFun guardedAddSlotFun [slot, delta] s [] = ExecResult.reverted := by
+  intro hrev
+  simp [guardedAddSlotSpecR, guardedAddSlotFun, require, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+
+theorem guardedAddSlot_reverts_when_not_requires (slot delta : Nat) (h : delta = 0) :
+    (guardedAddSlotSpec slot delta).requires (storeOf slot 0) = False ∧
+    execFun guardedAddSlotFun [slot, delta] (storeOf slot 0) [] = ExecResult.reverted := by
+  constructor
+  · simp [guardedAddSlotSpec, h]
+  · simp [guardedAddSlotFun, require, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv,
+      updateEnv, updateStore, h]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/Supply.lean b/research/lean_only_proto/DumbContracts/Examples/Supply.lean
new file mode 100644
index 000000000..15b75429a
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/Supply.lean
@@ -0,0 +1,25 @@
+import DumbContracts.Examples.TokenBase
+
+namespace DumbContracts.Examples
+
+open DumbContracts
+
+-- Counterexample: list-based sums are sensitive to duplicates.
+
+theorem sumBalances_dup (s : Store) (a : Nat) :
+    sumBalances s [a, a] = s (balanceSlot a) + s (balanceSlot a) := by
+  simp [sumBalances]
+
+theorem sumBalances_dup_ne_totalSupply (s : Store) (a : Nat)
+    (hsupply : totalSupply s = s (balanceSlot a)) (hpos : s (balanceSlot a) > 0) :
+    sumBalances s [a, a] ≠ totalSupply s := by
+  intro h
+  have hsum : s (balanceSlot a) + s (balanceSlot a) = s (balanceSlot a) := by
+    simpa [sumBalances, hsupply] using h
+  have hx : s (balanceSlot a) + s (balanceSlot a) = s (balanceSlot a) + 0 := by
+    simpa using (hsum.trans (by simp))
+  have hzero : s (balanceSlot a) = 0 := by
+    exact Nat.add_left_cancel hx
+  exact (ne_of_gt hpos) hzero
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/TokenBase.lean b/research/lean_only_proto/DumbContracts/Examples/TokenBase.lean
new file mode 100644
index 000000000..b4a67ae65
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/TokenBase.lean
@@ -0,0 +1,59 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+
+/-- Storage slots for a tiny ERC20-style layout. -/
+
+def balanceSlot (addr : Nat) : Nat :=
+  1000 + addr
+
+def totalSupplySlot : Nat :=
+  0
+
+def totalSupply (s : Store) : Nat :=
+  s totalSupplySlot
+
+def setBalance (s : Store) (addr val : Nat) : Store :=
+  updateStore s (balanceSlot addr) val
+
+def sum2 (s : Store) (a b : Nat) : Nat :=
+  s (balanceSlot a) + s (balanceSlot b)
+
+/-- Sum of balances for a list of addresses. -/
+
+def sumBalances (s : Store) : List Nat -> Nat
+  | [] => 0
+  | a :: rest => s (balanceSlot a) + sumBalances rest
+
+-- Common store lemmas.
+
+theorem updateStore_same (s : Store) (k : Nat) :
+    updateStore s k (s k) = s := by
+  funext a
+  by_cases h : a = k
+  · simp [updateStore, updateNat, h]
+  · simp [updateStore, updateNat, h]
+
+theorem updateStore_shadow (s : Store) (k v1 v2 : Nat) :
+    updateStore (updateStore s k v1) k v2 = updateStore s k v2 := by
+  funext a
+  by_cases h : a = k
+  · simp [updateStore, updateNat, h]
+  · simp [updateStore, updateNat, h]
+
+-- Slot distinctness.
+
+theorem balanceSlot_ne (a b : Nat) (h : a ≠ b) : balanceSlot a ≠ balanceSlot b := by
+  intro h'
+  apply h
+  exact Nat.add_left_cancel h'
+
+theorem balanceSlot_ne_total (addr : Nat) : balanceSlot addr ≠ totalSupplySlot := by
+  simp [balanceSlot, totalSupplySlot]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/TokenTransfer.lean b/research/lean_only_proto/DumbContracts/Examples/TokenTransfer.lean
new file mode 100644
index 000000000..df7754156
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/TokenTransfer.lean
@@ -0,0 +1,413 @@
+import DumbContracts.Examples.TokenBase
+import DumbContracts.Lang
+import DumbContracts.Semantics
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+
+/-- Simple ERC20-style transfer. -/
+
+def transferFun : Fun :=
+  { name := "transfer"
+    args := ["from", "to", "amount"]
+    body := Stmt.if_
+      (Expr.eq (Expr.var "to") (Expr.lit 0))
+      Stmt.revert
+      (Stmt.if_
+        (Expr.lt (Expr.sload (Expr.add (Expr.lit 1000) (Expr.var "from"))) (Expr.var "amount"))
+        Stmt.revert
+        (Stmt.sstore
+            (Expr.add (Expr.lit 1000) (Expr.var "from"))
+            (Expr.sub
+              (Expr.sload (Expr.add (Expr.lit 1000) (Expr.var "from")))
+              (Expr.var "amount"))
+          ;;
+          Stmt.sstore
+            (Expr.add (Expr.lit 1000) (Expr.var "to"))
+            (Expr.add
+              (Expr.sload (Expr.add (Expr.lit 1000) (Expr.var "to")))
+              (Expr.var "amount"))))
+    ret := none }
+
+-- Token-style specs (Store-level).
+
+def transferSpecR (from to amount : Nat) : SpecR Store :=
+  { requires := fun s => to ≠ 0 ∧ s (balanceSlot from) >= amount
+    ensures := fun s s' =>
+      s' =
+        setBalance
+          (setBalance s from (s (balanceSlot from) - amount))
+          to (s (balanceSlot to) + amount)
+    reverts := fun s => to = 0 ∨ s (balanceSlot from) < amount }
+
+def transferSpecRNoSelf (from to amount : Nat) : SpecR Store :=
+  { requires := fun s => to ≠ 0 ∧ from ≠ to ∧ s (balanceSlot from) >= amount
+    ensures := (transferSpecR from to amount).ensures
+    reverts := fun s => to = 0 ∨ from = to ∨ s (balanceSlot from) < amount }
+
+def transferStoreSeq (s : Store) (from to amount : Nat) : Store :=
+  let s1 := setBalance s from (s (balanceSlot from) - amount)
+  setBalance s1 to (s1 (balanceSlot to) + amount)
+
+def transferSpecRSeq (from to amount : Nat) : SpecR Store :=
+  { requires := fun s => to ≠ 0 ∧ s (balanceSlot from) >= amount
+    ensures := fun s s' => s' = transferStoreSeq s from to amount
+    reverts := fun s => to = 0 ∨ s (balanceSlot from) < amount }
+
+-- Sequential read equivalence when from != to.
+
+theorem transferStoreSeq_eq_transferSpecR_update (s : Store) (from to amount : Nat)
+    (hneq : from ≠ to) :
+    transferStoreSeq s from to amount =
+      setBalance
+        (setBalance s from (s (balanceSlot from) - amount))
+        to (s (balanceSlot to) + amount) := by
+  have hslot : balanceSlot from ≠ balanceSlot to := by
+    exact balanceSlot_ne from to hneq
+  have hs1 :
+      (setBalance s from (s (balanceSlot from) - amount)) (balanceSlot to) =
+        s (balanceSlot to) := by
+    simp [setBalance, updateStore, updateNat, hslot]
+  simp [transferStoreSeq, setBalance, updateStore, updateNat, hs1]
+
+theorem transferSpecRSeq_ensures_eq_transferSpecR (s s' : Store) (from to amount : Nat)
+    (hneq : from ≠ to) :
+    (transferSpecRSeq from to amount).ensures s s' ↔
+      (transferSpecR from to amount).ensures s s' := by
+  constructor
+  · intro hens
+    have hs : s' = transferStoreSeq s from to amount := by
+      simpa [transferSpecRSeq] using hens
+    have hs' :
+        s' =
+          setBalance
+            (setBalance s from (s (balanceSlot from) - amount))
+            to (s (balanceSlot to) + amount) := by
+      simpa [transferStoreSeq_eq_transferSpecR_update s from to amount hneq] using hs
+    simpa [transferSpecR] using hs'
+  · intro hens
+    have hs :
+        s' =
+          setBalance
+            (setBalance s from (s (balanceSlot from) - amount))
+            to (s (balanceSlot to) + amount) := by
+      simpa [transferSpecR] using hens
+    have hs' : s' = transferStoreSeq s from to amount := by
+      simpa [transferStoreSeq_eq_transferSpecR_update s from to amount hneq] using hs
+    simpa [transferSpecRSeq] using hs'
+
+-- Execution matches specs.
+
+theorem transfer_meets_specR_ok (s : Store) (from to amount : Nat) :
+    (transferSpecR from to amount).requires s ->
+    (match execFun transferFun [from, to, amount] s [] with
+      | ExecResult.ok _ s' => (transferSpecR from to amount).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hto : to ≠ 0 := hreq.left
+  have hbal : s (balanceSlot from) >= amount := hreq.right
+  have hnotlt : ¬ s (balanceSlot from) < amount := by
+    exact not_lt_of_ge hbal
+  simp [transferSpecR, transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv,
+    updateEnv, updateStore, balanceSlot, setBalance, hto, hnotlt]
+
+theorem transfer_meets_specRNoSelf_ok (s : Store) (from to amount : Nat) :
+    (transferSpecRNoSelf from to amount).requires s ->
+    (match execFun transferFun [from, to, amount] s [] with
+      | ExecResult.ok _ s' => (transferSpecRNoSelf from to amount).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hreq' : (transferSpecR from to amount).requires s := by
+    exact And.intro hreq.left hreq.right.right
+  simpa [transferSpecRNoSelf] using (transfer_meets_specR_ok s from to amount hreq')
+
+theorem transfer_meets_specRSeq_ok (s : Store) (from to amount : Nat) :
+    (transferSpecRSeq from to amount).requires s ->
+    (match execFun transferFun [from, to, amount] s [] with
+      | ExecResult.ok _ s' => (transferSpecRSeq from to amount).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hto : to ≠ 0 := hreq.left
+  have hbal : s (balanceSlot from) >= amount := hreq.right
+  have hnotlt : ¬ s (balanceSlot from) < amount := by
+    exact not_lt_of_ge hbal
+  simp [transferSpecRSeq, transferStoreSeq, transferFun, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, balanceSlot, setBalance, hto, hnotlt]
+
+theorem transfer_meets_specR_reverts (s : Store) (from to amount : Nat) :
+    (transferSpecR from to amount).reverts s ->
+    execFun transferFun [from, to, amount] s [] = ExecResult.reverted := by
+  intro hrev
+  cases hrev with
+  | inl hto =>
+      simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
+        updateStore, balanceSlot, setBalance, hto]
+  | inr hlt =>
+      by_cases hto : to = 0
+      · simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
+          updateStore, balanceSlot, setBalance, hto]
+      · simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
+          updateStore, balanceSlot, setBalance, hto, hlt]
+
+-- Aliasing boundary facts.
+
+theorem transfer_self_noop (s : Store) (from amount : Nat)
+    (hto : from ≠ 0) (hbal : s (balanceSlot from) >= amount) :
+    execFun transferFun [from, from, amount] s [] =
+      ExecResult.ok (bindArgs emptyEnv ["from", "to", "amount"] [from, from, amount]) s := by
+  have hnotlt : ¬ s (balanceSlot from) < amount := by
+    exact not_lt_of_ge hbal
+  have hs :
+      execFun transferFun [from, from, amount] s [] =
+        ExecResult.ok
+          (bindArgs emptyEnv ["from", "to", "amount"] [from, from, amount])
+          (updateStore
+            (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
+            (balanceSlot from)
+            (s (balanceSlot from) - amount + amount)) := by
+    simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
+      updateStore, balanceSlot, hto, hnotlt]
+  have hshadow :
+      updateStore
+        (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
+        (balanceSlot from)
+        (s (balanceSlot from) - amount + amount)
+        =
+        updateStore s (balanceSlot from) (s (balanceSlot from) - amount + amount) := by
+    exact updateStore_shadow s (balanceSlot from)
+      (s (balanceSlot from) - amount) (s (balanceSlot from) - amount + amount)
+  have hval : s (balanceSlot from) - amount + amount = s (balanceSlot from) := by
+    exact Nat.sub_add_cancel hbal
+  have hs' :
+      updateStore
+        (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
+        (balanceSlot from)
+        (s (balanceSlot from) - amount + amount)
+        = s := by
+    calc
+      updateStore
+          (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
+          (balanceSlot from)
+          (s (balanceSlot from) - amount + amount)
+          =
+          updateStore s (balanceSlot from) (s (balanceSlot from) - amount + amount) := by
+            exact hshadow
+      _ = updateStore s (balanceSlot from) (s (balanceSlot from)) := by
+            simp [hval]
+      _ = s := by
+            exact updateStore_same s (balanceSlot from)
+  simpa [hs'] using hs
+
+theorem transferSpecRSeq_self_ensures_noop (s s' : Store) (from amount : Nat)
+    (hbal : s (balanceSlot from) >= amount)
+    (hens : (transferSpecRSeq from from amount).ensures s s') :
+    s' = s := by
+  have hval : s (balanceSlot from) - amount + amount = s (balanceSlot from) := by
+    exact Nat.sub_add_cancel hbal
+  have hs :
+      s' =
+        updateStore
+          (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
+          (balanceSlot from)
+          (s (balanceSlot from) - amount + amount) := by
+    simpa [transferSpecRSeq, transferStoreSeq, setBalance, updateStore, updateNat] using hens
+  have hshadow :
+      updateStore
+        (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
+        (balanceSlot from)
+        (s (balanceSlot from) - amount + amount)
+        =
+        updateStore s (balanceSlot from) (s (balanceSlot from) - amount + amount) := by
+    exact updateStore_shadow s (balanceSlot from)
+      (s (balanceSlot from) - amount) (s (balanceSlot from) - amount + amount)
+  have hs' :
+      s' = updateStore s (balanceSlot from) (s (balanceSlot from) - amount + amount) := by
+    calc
+      s' =
+          updateStore
+            (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
+            (balanceSlot from)
+            (s (balanceSlot from) - amount + amount) := by
+              exact hs
+      _ = updateStore s (balanceSlot from) (s (balanceSlot from) - amount + amount) := by
+              exact hshadow
+  calc
+    s' = updateStore s (balanceSlot from) (s (balanceSlot from)) := by
+          simpa [hval] using hs'
+    _ = s := by
+          exact updateStore_same s (balanceSlot from)
+
+theorem transferSpecR_self_balance_increases (s s' : Store) (from amount : Nat)
+    (hens : (transferSpecR from from amount).ensures s s') :
+    s' (balanceSlot from) = s (balanceSlot from) + amount := by
+  have hs :
+      s' =
+        setBalance
+          (setBalance s from (s (balanceSlot from) - amount))
+          from (s (balanceSlot from) + amount) := by
+    simpa [transferSpecR] using hens
+  have hshadow :
+      setBalance
+          (setBalance s from (s (balanceSlot from) - amount))
+          from (s (balanceSlot from) + amount)
+        =
+        setBalance s from (s (balanceSlot from) + amount) := by
+    simp [setBalance, updateStore_shadow]
+  calc
+    s' (balanceSlot from)
+        = (setBalance s from (s (balanceSlot from) + amount)) (balanceSlot from) := by
+            simpa [hs, hshadow]
+    _ = s (balanceSlot from) + amount := by
+            simp [setBalance, updateStore, updateNat]
+
+theorem transferSpecR_self_ensures_not_s (s : Store) (from amount : Nat)
+    (hpos : amount > 0) :
+    ¬ (transferSpecR from from amount).ensures s s := by
+  intro hens
+  have hbal :
+      s (balanceSlot from) = s (balanceSlot from) + amount := by
+    simpa using (transferSpecR_self_balance_increases s s from amount hens)
+  have h' : s (balanceSlot from) + amount = s (balanceSlot from) + 0 := by
+    simpa using hbal.symm
+  have hzero : amount = 0 := by
+    exact Nat.add_left_cancel h'
+  exact (ne_of_gt hpos) hzero
+
+-- Sum preservation properties.
+
+theorem transfer_preserves_sum2 (s s' : Store) (from to amount : Nat)
+    (hreq : (transferSpecR from to amount).requires s) (hneq : from ≠ to) :
+    (transferSpecR from to amount).ensures s s' ->
+    sum2 s from to = sum2 s' from to := by
+  intro h
+  have hbal : amount <= s (balanceSlot from) := by
+    exact hreq.right
+  have hslot : balanceSlot from ≠ balanceSlot to := by
+    exact balanceSlot_ne from to hneq
+  have hs :
+      s' =
+        setBalance
+          (setBalance s from (s (balanceSlot from) - amount))
+          to (s (balanceSlot to) + amount) := by
+    simpa [transferSpecR] using h
+  calc
+    sum2 s from to
+        = s (balanceSlot from) + s (balanceSlot to) := by
+            simp [sum2]
+    _ = (s (balanceSlot from) - amount + amount) + s (balanceSlot to) := by
+            simp [Nat.sub_add_cancel hbal, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
+    _ = (s (balanceSlot from) - amount) + (s (balanceSlot to) + amount) := by
+            simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
+    _ = sum2 s' from to := by
+            simp [sum2, hs, setBalance, updateStore, updateNat, balanceSlot, hslot, Nat.add_assoc]
+
+theorem transfer_preserves_other_balance (s s' : Store) (from to amount addr : Nat)
+    (hfrom : addr ≠ from) (hto : addr ≠ to) :
+    (transferSpecR from to amount).ensures s s' ->
+    s' (balanceSlot addr) = s (balanceSlot addr) := by
+  intro h
+  have hs :
+      s' =
+        setBalance
+          (setBalance s from (s (balanceSlot from) - amount))
+          to (s (balanceSlot to) + amount) := by
+    simpa [transferSpecR] using h
+  have hslot_from : balanceSlot addr ≠ balanceSlot from := by
+    exact balanceSlot_ne addr from hfrom
+  have hslot_to : balanceSlot addr ≠ balanceSlot to := by
+    exact balanceSlot_ne addr to hto
+  simp [hs, setBalance, updateStore, updateNat, hslot_to, hslot_from]
+
+theorem transfer_preserves_sum_list (s s' : Store) (from to amount : Nat) (addrs : List Nat)
+    (hnotfrom : from ∉ addrs) (hnotto : to ∉ addrs)
+    (hens : (transferSpecR from to amount).ensures s s') :
+    sumBalances s addrs = sumBalances s' addrs := by
+  induction addrs with
+  | nil =>
+      simp [sumBalances]
+  | cons a rest ih =>
+      have hnotfrom' : a ≠ from := by
+        intro h
+        apply hnotfrom
+        simp [h]
+      have hnotto' : a ≠ to := by
+        intro h
+        apply hnotto
+        simp [h]
+      have hnotfrom_tail : from ∉ rest := by
+        intro hmem
+        apply hnotfrom
+        simp [hmem]
+      have hnotto_tail : to ∉ rest := by
+        intro hmem
+        apply hnotto
+        simp [hmem]
+      have hbal :
+          s' (balanceSlot a) = s (balanceSlot a) :=
+        transfer_preserves_other_balance s s' from to amount hnotfrom' hnotto' hens
+      have htail :
+          sumBalances s rest = sumBalances s' rest :=
+        ih hnotfrom_tail hnotto_tail hens
+      simp [sumBalances, hbal, htail]
+
+theorem transfer_preserves_sum_from_to_rest (s s' : Store) (from to amount : Nat) (rest : List Nat)
+    (hreq : (transferSpecR from to amount).requires s) (hneq : from ≠ to)
+    (hnotfrom : from ∉ rest) (hnotto : to ∉ rest)
+    (hens : (transferSpecR from to amount).ensures s s') :
+    sumBalances s (from :: to :: rest) = sumBalances s' (from :: to :: rest) := by
+  have hsum2 : sum2 s from to = sum2 s' from to :=
+    transfer_preserves_sum2 s s' from to amount hreq hneq hens
+  have hrest : sumBalances s rest = sumBalances s' rest :=
+    transfer_preserves_sum_list s s' from to amount rest hnotfrom hnotto hens
+  calc
+    sumBalances s (from :: to :: rest)
+        = (s (balanceSlot from) + s (balanceSlot to)) + sumBalances s rest := by
+            simp [sumBalances, Nat.add_assoc]
+    _ = (s' (balanceSlot from) + s' (balanceSlot to)) + sumBalances s rest := by
+            simpa [sum2] using hsum2
+    _ = (s' (balanceSlot from) + s' (balanceSlot to)) + sumBalances s' rest := by
+            simp [hrest]
+    _ = sumBalances s' (from :: to :: rest) := by
+            simp [sumBalances, Nat.add_assoc]
+
+theorem transfer_preserves_totalSupply (s s' : Store) (from to amount : Nat)
+    (hens : (transferSpecR from to amount).ensures s s') :
+    totalSupply s' = totalSupply s := by
+  have hs :
+      s' =
+        setBalance
+          (setBalance s from (s (balanceSlot from) - amount))
+          to (s (balanceSlot to) + amount) := by
+    simpa [transferSpecR] using hens
+  have hslot_from : balanceSlot from ≠ totalSupplySlot := by
+    exact balanceSlot_ne_total from
+  have hslot_to : balanceSlot to ≠ totalSupplySlot := by
+    exact balanceSlot_ne_total to
+  simp [totalSupply, hs, setBalance, updateStore, updateNat, hslot_to, hslot_from, totalSupplySlot]
+
+theorem transfer_preserves_supply_list (s s' : Store) (from to amount : Nat) (rest : List Nat)
+    (hreq : (transferSpecR from to amount).requires s) (hneq : from ≠ to)
+    (hnotfrom : from ∉ rest) (hnotto : to ∉ rest)
+    (hsupply : sumBalances s (from :: to :: rest) = totalSupply s)
+    (hens : (transferSpecR from to amount).ensures s s') :
+    sumBalances s' (from :: to :: rest) = totalSupply s' := by
+  have hsum :
+      sumBalances s (from :: to :: rest) = sumBalances s' (from :: to :: rest) :=
+    transfer_preserves_sum_from_to_rest s s' from to amount rest hreq hneq hnotfrom hnotto hens
+  have htot : totalSupply s' = totalSupply s :=
+    transfer_preserves_totalSupply s s' from to amount hens
+  calc
+    sumBalances s' (from :: to :: rest)
+        = sumBalances s (from :: to :: rest) := by
+            symm
+            exact hsum
+    _ = totalSupply s := by
+            exact hsupply
+    _ = totalSupply s' := by
+            symm
+            exact htot
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
new file mode 100644
index 000000000..c458539d0
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -0,0 +1,44 @@
+import DumbContracts.Lang
+
+namespace DumbContracts.Std
+
+open DumbContracts.Lang
+
+/--
+Small convenience helpers for writing contracts as Lean data.
+These are definitional wrappers so they should reduce syntax noise
+without changing semantics.
+-/
+
+def require (cond : Expr) (body : Stmt) : Stmt :=
+  Stmt.if_ cond body Stmt.revert
+
+def unless (cond : Expr) (body : Stmt) : Stmt :=
+  Stmt.if_ cond Stmt.revert body
+
+def assert (cond : Expr) : Stmt :=
+  Stmt.if_ cond Stmt.skip Stmt.revert
+
+/-- Shorthand for loading/storing fixed slots. -/
+
+def sloadSlot (slot : Nat) : Expr :=
+  Expr.sload (Expr.lit slot)
+
+def sstoreSlot (slot : Nat) (value : Expr) : Stmt :=
+  Stmt.sstore (Expr.lit slot) value
+
+def sloadVar (name : String) : Expr :=
+  Expr.sload (Expr.var name)
+
+def sstoreVar (name : String) (value : Expr) : Stmt :=
+  Stmt.sstore (Expr.var name) value
+
+/-- Shorthand for variables and literals. -/
+
+def v (name : String) : Expr :=
+  Expr.var name
+
+def n (value : Nat) : Expr :=
+  Expr.lit value
+
+end DumbContracts.Std
diff --git a/research/lean_only_proto/Main.lean b/research/lean_only_proto/Main.lean
index 0d333527c..6a3a1e79c 100644
--- a/research/lean_only_proto/Main.lean
+++ b/research/lean_only_proto/Main.lean
@@ -8,10 +8,10 @@ open DumbContracts.Yul
 
 -- Emit Yul/EVM artifacts.
 def main : IO Unit := do
-  let exampleProg := compileProgram [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4]
+  let exampleProg := compileProgram exampleEntries
   let exampleYul := Yul.Pretty.program exampleProg
   IO.FS.writeFile "out/example.yul" exampleYul
-  let healthProg := compileProgram [healthEntrySet, healthEntryCheck]
+  let healthProg := compileProgram healthEntries
   let healthYul := Yul.Pretty.program healthProg
   IO.FS.writeFile "out/health.yul" healthYul
   let evmAsm := DumbContracts.EvmAsm.pretty DumbContracts.EvmAsm.directProgramAsm
diff --git a/research/lean_only_proto/README.md b/research/lean_only_proto/README.md
index c12346842..cb9cd834d 100644
--- a/research/lean_only_proto/README.md
+++ b/research/lean_only_proto/README.md
@@ -8,11 +8,14 @@ PATH=/opt/lean-4.27.0/bin:$PATH lake build
 ```
 
 Write a contract:
-1. Add a `Fun` in `DumbContracts/Examples.lean`.
+1. Add a `Fun` under `DumbContracts/Examples/` (e.g. `StoreOps.lean`).
 2. Add a `Spec` or `SpecR` + proof next to it.
 3. Wire the selector in `DumbContracts/Compiler.lean`.
 4. Re-run `./scripts/end_to_end.sh`.
 
+Convenience helpers:
+- Small EDSL helpers live in `DumbContracts/Stdlib.lean` (`require`, `unless`, `assert`, slot helpers).
+
 Minimal spec pattern:
 ```
 def mySpecR : SpecR Store := { requires := ..., ensures := ..., reverts := ... }
diff --git a/research/lean_only_proto/test/GeneratedMaxStore.t.sol b/research/lean_only_proto/test/GeneratedMaxStore.t.sol
new file mode 100644
index 000000000..256384b41
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedMaxStore.t.sol
@@ -0,0 +1,31 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedMaxStoreTest is GeneratedBase {
+    function testMaxStore() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selMax = 0xb61d4088;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selMax, 5, 10, 7));
+        require(ok, "maxStore failed (a > b)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 5));
+        require(ok, "getSlot failed (slot 5)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 10, "unexpected maxStore value (slot 5)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selMax, 6, 3, 9));
+        require(ok, "maxStore failed (b >= a)");
+
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 6));
+        require(ok, "getSlot failed (slot 6)");
+        val = abi.decode(data, (uint256));
+        require(val == 9, "unexpected maxStore value (slot 6)");
+    }
+}