From 8a5a5fb137303002c51e1f1232649e457497a98a Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Mon, 9 Feb 2026 23:55:09 +0000
Subject: [PATCH 01/17] Add requireNonZero helper and setNonZero example

---
 STATUS.md                                     |  1 +
 docs/research-log.md                          |  1 +
 .../DumbContracts/Compiler.lean               | 13 +++++-
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/NonZeroStore.lean  | 42 +++++++++++++++++++
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedNonZeroStore.t.sol          | 26 ++++++++++++
 7 files changed, 86 insertions(+), 1 deletion(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/NonZeroStore.lean
 create mode 100644 research/lean_only_proto/test/GeneratedNonZeroStore.t.sol

diff --git a/STATUS.md b/STATUS.md
index 768fff2c9..f49e38f8e 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -43,6 +43,7 @@ Last updated: 2026-02-09
 - 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.
+- Added a `requireNonZero` helper and a tiny `setNonZero` example + 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 1a1fb1ab5..f3a0947a7 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -21,6 +21,7 @@
 - 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.
+- Added a `requireNonZero` helper plus a tiny `setNonZero` example + 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/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 38b31382a..8312f3a14 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -131,8 +131,19 @@ def exampleEntry5 : EntryPoint :=
     selector := 0xb61d4088
     returns := false }
 
+def exampleEntry6 : EntryPoint :=
+  { name := "setNonZero"
+    args := ["slot", "value"]
+    body := Lang.Stmt.if_
+      (Lang.Expr.not (Lang.Expr.eq (Lang.Expr.var "value") (Lang.Expr.lit 0)))
+      (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+      Lang.Stmt.revert
+    -- setNonZero(uint256,uint256) -> 0xac1f1f67
+    selector := 0xac1f1f67
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
-  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5]
+  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/Examples.lean b/research/lean_only_proto/DumbContracts/Examples.lean
index e4764e5f5..2dfba1c7f 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -4,3 +4,4 @@ import DumbContracts.Examples.TokenBase
 import DumbContracts.Examples.Supply
 import DumbContracts.Examples.TokenTransfer
 import DumbContracts.Examples.MaxStore
+import DumbContracts.Examples.NonZeroStore
diff --git a/research/lean_only_proto/DumbContracts/Examples/NonZeroStore.lean b/research/lean_only_proto/DumbContracts/Examples/NonZeroStore.lean
new file mode 100644
index 000000000..86b817eb5
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/NonZeroStore.lean
@@ -0,0 +1,42 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Store a value into a slot, but only if the value is non-zero. -/
+
+def setNonZeroFun : Fun :=
+  { name := "setNonZero"
+    args := ["slot", "value"]
+    body := requireNonZero (v "value") (sstoreVar "slot" (v "value"))
+    ret := none }
+
+def setNonZeroSpecR (slot value : Nat) : SpecR Store :=
+  { requires := fun _ => value != 0
+    ensures := fun s s' => s' = updateStore s slot value
+    reverts := fun _ => value = 0 }
+
+theorem setNonZero_meets_specR_ok (s : Store) (slot value : Nat) :
+    (setNonZeroSpecR slot value).requires s ->
+    (match execFun setNonZeroFun [slot, value] s [] with
+      | ExecResult.ok _ s' => (setNonZeroSpecR slot value).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hnonzero : value != 0 := by exact hreq
+  simp [setNonZeroSpecR, setNonZeroFun, requireNonZero, require, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hnonzero]
+
+theorem setNonZero_meets_specR_reverts (s : Store) (slot value : Nat) :
+    (setNonZeroSpecR slot value).reverts s ->
+    execFun setNonZeroFun [slot, value] s [] = ExecResult.reverted := by
+  intro hrev
+  simp [setNonZeroSpecR, setNonZeroFun, requireNonZero, require, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index c458539d0..be8355646 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -19,6 +19,9 @@ def unless (cond : Expr) (body : Stmt) : Stmt :=
 def assert (cond : Expr) : Stmt :=
   Stmt.if_ cond Stmt.skip Stmt.revert
 
+def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
+  require (Expr.not (Expr.eq value (Expr.lit 0))) body
+
 /-- Shorthand for loading/storing fixed slots. -/
 
 def sloadSlot (slot : Nat) : Expr :=
diff --git a/research/lean_only_proto/test/GeneratedNonZeroStore.t.sol b/research/lean_only_proto/test/GeneratedNonZeroStore.t.sol
new file mode 100644
index 000000000..a63cc91db
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedNonZeroStore.t.sol
@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedNonZeroStoreTest is GeneratedBase {
+    function testSetNonZero() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selSetNonZero = 0xac1f1f67;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSetNonZero, 9, 123));
+        require(ok, "setNonZero failed");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 9));
+        require(ok, "getSlot failed (slot 9)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 123, "unexpected setNonZero value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSetNonZero, 10, 0));
+        require(!ok, "setNonZero should revert on zero");
+    }
+}

From 461c1bc454d524290a1a39532cc229b4f619793d Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 00:00:22 +0000
Subject: [PATCH 02/17] Align direct EVM asm with solc labels

---
 STATUS.md                                     |  1 +
 docs/research-log.md                          |  1 +
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 82 ++++++++++++++-----
 3 files changed, 64 insertions(+), 20 deletions(-)

diff --git a/STATUS.md b/STATUS.md
index f49e38f8e..249336913 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -44,6 +44,7 @@ Last updated: 2026-02-09
 - 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.
 - Added a `requireNonZero` helper and a tiny `setNonZero` example + Foundry test.
+- Aligned direct EVM asm with solc for `setNonZero` (label pushes use `PUSH2`).
 - 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 f3a0947a7..116be28b9 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -22,6 +22,7 @@
 - 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.
 - Added a `requireNonZero` helper plus a tiny `setNonZero` example + Foundry test.
+- Updated direct EVM asm to include `setNonZero` and force label pushes to `PUSH2` so bytecode matches solc output.
 - 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/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index aaac514ec..98c562bd9 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -11,69 +11,84 @@ def directProgramAsm : List String :=
   , "DUP1"
   , "PUSH4 0x7eba7ba6"
   , "EQ"
-  , "PUSH tag_getSlot"
+  , "PUSH2 tag_getSlot"
   , "JUMPI"
   , "DUP1"
   , "PUSH4 0xf2c298be"
   , "EQ"
-  , "PUSH tag_setSlot"
+  , "PUSH2 tag_setSlot"
   , "JUMPI"
   , "DUP1"
   , "PUSH4 0x02222aec"
   , "EQ"
-  , "PUSH tag_addSlot"
+  , "PUSH2 tag_addSlot"
   , "JUMPI"
   , "DUP1"
   , "PUSH4 0x49f583e3"
   , "EQ"
-  , "PUSH tag_guardedAddSlot"
+  , "PUSH2 tag_guardedAddSlot"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xb61d4088"
   , "EQ"
-  , "PUSH tag_maxStore"
+  , "PUSH2 tag_maxStore"
+  , "JUMPI"
+  , "PUSH4 0xac1f1f67"
+  , "EQ"
+  , "PUSH2 tag_setNonZero"
   , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_setNonZero:"
+  , "PUSH2 ret_setNonZero"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setNonZero"
+  , "JUMP"
+  , "ret_setNonZero:"
+  , "STOP"
   , "tag_maxStore:"
-  , "PUSH ret_maxStore"
+  , "PUSH2 ret_maxStore"
   , "PUSH1 0x44"
   , "CALLDATALOAD"
   , "PUSH1 0x24"
   , "CALLDATALOAD"
   , "PUSH1 0x04"
   , "CALLDATALOAD"
-  , "PUSH fn_maxStore"
+  , "PUSH2 fn_maxStore"
   , "JUMP"
   , "ret_maxStore:"
   , "STOP"
   , "tag_guardedAddSlot:"
-  , "PUSH ret_guardedAddSlot"
+  , "PUSH2 ret_guardedAddSlot"
   , "PUSH1 0x24"
   , "CALLDATALOAD"
   , "PUSH1 0x04"
   , "CALLDATALOAD"
-  , "PUSH fn_guardedAddSlot"
+  , "PUSH2 fn_guardedAddSlot"
   , "JUMP"
   , "ret_guardedAddSlot:"
   , "STOP"
   , "tag_addSlot:"
-  , "PUSH ret_addSlot"
+  , "PUSH2 ret_addSlot"
   , "PUSH1 0x24"
   , "CALLDATALOAD"
   , "PUSH1 0x04"
   , "CALLDATALOAD"
-  , "PUSH fn_addSlot"
+  , "PUSH2 fn_addSlot"
   , "JUMP"
   , "ret_addSlot:"
   , "STOP"
   , "tag_setSlot:"
-  , "PUSH ret_setSlot"
+  , "PUSH2 ret_setSlot"
   , "PUSH1 0x24"
   , "CALLDATALOAD"
   , "PUSH1 0x04"
   , "CALLDATALOAD"
-  , "PUSH fn_setSlot"
+  , "PUSH2 fn_setSlot"
   , "JUMP"
   , "ret_setSlot:"
   , "STOP"
@@ -104,13 +119,13 @@ def directProgramAsm : List String :=
   , "DUP3"
   , "DUP3"
   , "GT"
-  , "PUSH guardedAddSlot_ok"
+  , "PUSH2 guardedAddSlot_ok"
   , "JUMPI"
   , "guardedAddSlot_check:"
   , "POP"
   , "GT"
   , "ISZERO"
-  , "PUSH guardedAddSlot_revert"
+  , "PUSH2 guardedAddSlot_revert"
   , "JUMPI"
   , "JUMP"
   , "guardedAddSlot_revert:"
@@ -125,7 +140,7 @@ def directProgramAsm : List String :=
   , "SWAP1"
   , "SSTORE"
   , "PUSH0"
-  , "PUSH guardedAddSlot_check"
+  , "PUSH2 guardedAddSlot_check"
   , "JUMP"
   , "fn_maxStore:"
   , "SWAP1"
@@ -134,12 +149,12 @@ def directProgramAsm : List String :=
   , "DUP2"
   , "DUP2"
   , "GT"
-  , "PUSH maxStore_then"
+  , "PUSH2 maxStore_then"
   , "JUMPI"
   , "maxStore_check:"
   , "GT"
   , "ISZERO"
-  , "PUSH maxStore_else"
+  , "PUSH2 maxStore_else"
   , "JUMPI"
   , "maxStore_join:"
   , "POP"
@@ -149,13 +164,40 @@ def directProgramAsm : List String :=
   , "SSTORE"
   , "PUSH0"
   , "DUP1"
-  , "PUSH maxStore_join"
+  , "PUSH2 maxStore_join"
   , "JUMP"
   , "maxStore_then:"
   , "DUP1"
   , "DUP4"
   , "SSTORE"
-  , "PUSH maxStore_check"
+  , "PUSH2 maxStore_check"
+  , "JUMP"
+  , "fn_setNonZero:"
+  , "SWAP1"
+  , "DUP1"
+  , "PUSH0"
+  , "SWAP3"
+  , "DUP4"
+  , "DUP3"
+  , "SUB"
+  , "PUSH2 setNonZero_ok"
+  , "JUMPI"
+  , "setNonZero_check:"
+  , "POP"
+  , "POP"
+  , "EQ"
+  , "PUSH2 setNonZero_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "setNonZero_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "setNonZero_ok:"
+  , "SSTORE"
+  , "DUP1"
+  , "PUSH0"
+  , "PUSH2 setNonZero_check"
   , "JUMP"
   ]
 

From b2719ee76202696d3329a4eb0b3d2db1e3d223f0 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 00:00:38 +0000
Subject: [PATCH 03/17] Update status date

---
 STATUS.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/STATUS.md b/STATUS.md
index 249336913..6f0fe0b65 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -1,6 +1,6 @@
 # Status
 
-Last updated: 2026-02-09
+Last updated: 2026-02-10
 
 ## Current Focus
 - Lean-only specs + implementations + proofs.

From 768fadf370919b4146a643f583c254fc628dc29b Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 00:31:43 +0000
Subject: [PATCH 04/17] Add compareAndSwap helper + example

---
 STATUS.md                                     |   1 +
 docs/research-log.md                          |   8 ++++
 .../DumbContracts/Compiler.lean               |  15 +++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean |  45 ++++++++++++++++++
 .../DumbContracts/Examples.lean               |   1 +
 .../Examples/CompareAndSwap.lean              |  44 +++++++++++++++++
 .../DumbContracts/Examples/NonZeroStore.lean  |   6 +--
 .../lean_only_proto/DumbContracts/Stdlib.lean |  14 +++++-
 .../test/GeneratedCompareAndSwap.t.sol        |  30 ++++++++++++
 .../compare_evm_asm.cpython-312.pyc           | Bin 6671 -> 0 bytes
 10 files changed, 159 insertions(+), 5 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/CompareAndSwap.lean
 create mode 100644 research/lean_only_proto/test/GeneratedCompareAndSwap.t.sol
 delete mode 100644 research/lean_only_proto/tools/__pycache__/compare_evm_asm.cpython-312.pyc

diff --git a/STATUS.md b/STATUS.md
index 6f0fe0b65..ee7df26be 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -45,6 +45,7 @@ Last updated: 2026-02-10
 - Added a `maxStore` example (stores max(a,b) into a slot) plus selector + Foundry test.
 - Added a `requireNonZero` helper and a tiny `setNonZero` example + Foundry test.
 - Aligned direct EVM asm with solc for `setNonZero` (label pushes use `PUSH2`).
+- Added `requireEq`/`requireNeq` helpers plus a `compareAndSwap` example + 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 116be28b9..cf0629203 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,5 +1,13 @@
 # Research Log
 
+## 2026-02-10
+- Added `eq`/`neq` plus `requireEq`/`requireNeq` stdlib helpers.
+- Added `compareAndSwap` example (guarded store on expected value match) with SpecR and proofs.
+- Avoided double `sload` in `compareAndSwap` by caching the slot value with `let_` (prevents false reverts).
+- Refactored `setNonZero` to use the new `requireNeq` helper.
+- Updated compiler entries + direct EVM asm for `compareAndSwap`.
+- Added Foundry test for `compareAndSwap`.
+
 ## 2026-02-09
 - Added spec-style wrappers for storage and risk examples.
 - Added `SpecR` (specs with explicit revert predicates) and proofs.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 8312f3a14..8a3f065e5 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -142,8 +142,21 @@ def exampleEntry6 : EntryPoint :=
     selector := 0xac1f1f67
     returns := false }
 
+def exampleEntry7 : EntryPoint :=
+  { name := "compareAndSwap"
+    args := ["slot", "expected", "value"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.eq (Lang.Expr.var "current") (Lang.Expr.var "expected"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+          Lang.Stmt.revert)
+    -- compareAndSwap(uint256,uint256,uint256) -> 0xc74962fa
+    selector := 0xc74962fa
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
-  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6]
+  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 98c562bd9..0f9a83755 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -33,13 +33,30 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_maxStore"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xac1f1f67"
   , "EQ"
   , "PUSH2 tag_setNonZero"
   , "JUMPI"
+  , "PUSH4 0xc74962fa"
+  , "EQ"
+  , "PUSH2 tag_compareAndSwap"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_compareAndSwap:"
+  , "PUSH2 ret_compareAndSwap"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_compareAndSwap"
+  , "JUMP"
+  , "ret_compareAndSwap:"
+  , "STOP"
   , "tag_setNonZero:"
   , "PUSH2 ret_setNonZero"
   , "PUSH1 0x24"
@@ -199,6 +216,34 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 setNonZero_check"
   , "JUMP"
+  , "fn_compareAndSwap:"
+  , "SWAP1"
+  , "SWAP2"
+  , "DUP2"
+  , "SLOAD"
+  , "SWAP2"
+  , "DUP4"
+  , "DUP4"
+  , "EQ"
+  , "PUSH2 compareAndSwap_ok"
+  , "JUMPI"
+  , "compareAndSwap_check:"
+  , "POP"
+  , "POP"
+  , "SUB"
+  , "PUSH2 compareAndSwap_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "compareAndSwap_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "compareAndSwap_ok:"
+  , "SSTORE"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH2 compareAndSwap_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 2dfba1c7f..16fdc85c6 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -5,3 +5,4 @@ import DumbContracts.Examples.Supply
 import DumbContracts.Examples.TokenTransfer
 import DumbContracts.Examples.MaxStore
 import DumbContracts.Examples.NonZeroStore
+import DumbContracts.Examples.CompareAndSwap
diff --git a/research/lean_only_proto/DumbContracts/Examples/CompareAndSwap.lean b/research/lean_only_proto/DumbContracts/Examples/CompareAndSwap.lean
new file mode 100644
index 000000000..1f0a0baad
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/CompareAndSwap.lean
@@ -0,0 +1,44 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Store a new value only if the slot matches the expected value. -/
+
+def compareAndSwapFun : Fun :=
+  { name := "compareAndSwap"
+    args := ["slot", "expected", "value"]
+    body :=
+      Stmt.let_ "current" (sloadVar "slot")
+        (requireEq (v "current") (v "expected") (sstoreVar "slot" (v "value")))
+    ret := none }
+
+def compareAndSwapSpecR (slot expected value : Nat) : SpecR Store :=
+  { requires := fun s => s slot = expected
+    ensures := fun s s' => s' = updateStore s slot value
+    reverts := fun s => s slot != expected }
+
+theorem compareAndSwap_meets_specR_ok (s : Store) (slot expected value : Nat) :
+    (compareAndSwapSpecR slot expected value).requires s ->
+    (match execFun compareAndSwapFun [slot, expected, value] s [] with
+      | ExecResult.ok _ s' => (compareAndSwapSpecR slot expected value).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hmatch : s slot = expected := by exact hreq
+  simp [compareAndSwapSpecR, compareAndSwapFun, requireEq, eq, require, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hmatch]
+
+theorem compareAndSwap_meets_specR_reverts (s : Store) (slot expected value : Nat) :
+    (compareAndSwapSpecR slot expected value).reverts s ->
+    execFun compareAndSwapFun [slot, expected, value] s [] = ExecResult.reverted := by
+  intro hrev
+  simp [compareAndSwapSpecR, compareAndSwapFun, requireEq, eq, require, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/NonZeroStore.lean b/research/lean_only_proto/DumbContracts/Examples/NonZeroStore.lean
index 86b817eb5..aef4b51b1 100644
--- a/research/lean_only_proto/DumbContracts/Examples/NonZeroStore.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/NonZeroStore.lean
@@ -14,7 +14,7 @@ open DumbContracts.Std
 def setNonZeroFun : Fun :=
   { name := "setNonZero"
     args := ["slot", "value"]
-    body := requireNonZero (v "value") (sstoreVar "slot" (v "value"))
+    body := requireNeq (v "value") (n 0) (sstoreVar "slot" (v "value"))
     ret := none }
 
 def setNonZeroSpecR (slot value : Nat) : SpecR Store :=
@@ -29,14 +29,14 @@ theorem setNonZero_meets_specR_ok (s : Store) (slot value : Nat) :
       | _ => False) := by
   intro hreq
   have hnonzero : value != 0 := by exact hreq
-  simp [setNonZeroSpecR, setNonZeroFun, requireNonZero, require, execFun, execStmt, evalExpr,
+  simp [setNonZeroSpecR, setNonZeroFun, requireNeq, neq, eq, require, execFun, execStmt, evalExpr,
     bindArgs, emptyEnv, updateEnv, updateStore, hnonzero]
 
 theorem setNonZero_meets_specR_reverts (s : Store) (slot value : Nat) :
     (setNonZeroSpecR slot value).reverts s ->
     execFun setNonZeroFun [slot, value] s [] = ExecResult.reverted := by
   intro hrev
-  simp [setNonZeroSpecR, setNonZeroFun, requireNonZero, require, execFun, execStmt, evalExpr,
+  simp [setNonZeroSpecR, setNonZeroFun, requireNeq, neq, eq, require, execFun, execStmt, evalExpr,
     bindArgs, emptyEnv, updateEnv, updateStore, hrev]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index be8355646..6bad9d99e 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -19,8 +19,20 @@ def unless (cond : Expr) (body : Stmt) : Stmt :=
 def assert (cond : Expr) : Stmt :=
   Stmt.if_ cond Stmt.skip Stmt.revert
 
+def eq (lhs rhs : Expr) : Expr :=
+  Expr.eq lhs rhs
+
+def neq (lhs rhs : Expr) : Expr :=
+  Expr.not (Expr.eq lhs rhs)
+
+def requireEq (lhs rhs : Expr) (body : Stmt) : Stmt :=
+  require (eq lhs rhs) body
+
+def requireNeq (lhs rhs : Expr) (body : Stmt) : Stmt :=
+  require (neq lhs rhs) body
+
 def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
-  require (Expr.not (Expr.eq value (Expr.lit 0))) body
+  requireNeq value (Expr.lit 0) body
 
 /-- Shorthand for loading/storing fixed slots. -/
 
diff --git a/research/lean_only_proto/test/GeneratedCompareAndSwap.t.sol b/research/lean_only_proto/test/GeneratedCompareAndSwap.t.sol
new file mode 100644
index 000000000..c796fe5f7
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedCompareAndSwap.t.sol
@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedCompareAndSwapTest is GeneratedBase {
+    function testCompareAndSwap() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selGet = 0x7eba7ba6;
+        bytes4 selSet = 0xf2c298be;
+        bytes4 selCas = 0xc74962fa;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 10, 41));
+        require(ok, "setSlot failed");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selCas, 10, 41, 99));
+        require(ok, "compareAndSwap should succeed");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 10));
+        require(ok, "getSlot failed");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 99, "unexpected compareAndSwap value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selCas, 10, 1, 123));
+        require(!ok, "compareAndSwap should revert on mismatch");
+    }
+}
diff --git a/research/lean_only_proto/tools/__pycache__/compare_evm_asm.cpython-312.pyc b/research/lean_only_proto/tools/__pycache__/compare_evm_asm.cpython-312.pyc
deleted file mode 100644
index 3d280d139f3b087af842bb67be8c1a2910b14572..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 6671
zcma)BTWk~A8J@An_i^kvcLH=Egv5{ww`Cy^C`*71B-smLVY7hccn0F&8)qhjc*ncm
z-Ac80Q^n~%#M$f?uUK_cu@9)Ks!ElrO06nY`{LB5G1EwmwEMzax=|m>OZ%T0&%~q-
z;YdE`%$)!H^PhA6^ZgfpYqwhoDE+@r`hQkQ5Z~bkwHTBRx%vy}%n&RwM6e{Q3y?wG
zkdDNCeLz2?ms@Ixf|d#xg2o|Z&@^O%ahf&!gc>rlcGd{31zHodR<?pQLu+FltOZ({
zb+T4y?OX+GyVXh%s9r~K4*1zQYLrohS!*AVN?&b1Bq#Ll%IM<ha4_OU9K-q%=M$JS
zZ}qo(d7cXn2PT-|K-hPSXS_GP{tz!Pd^q4^+F>|Y9O<xH2S>E2+B84UaCalXjbj-h
z%#86Ieh&D3et`*ihq(aHw1&JvuFKuVjF0#OoXoj}w_?uWF(EQ0;7L3qcyD@&Gdh^d
z924{kz7b}40@!&$)^NlZX1TroV31?|UIEx}x5v1UkK;S6Pw;Bpq-67kLSexx_`@N7
zz^#+09=}hJs6Ib0_=-Cs?~5L4_>rsEp)*5>_?(C>M2r+PDv?z8jwPc;f?##>z8hG*
zNJe2+3{FxcM=_^$<w5ZoQ(Yw7hJhzK=sm%lC32sn+jkcv(+9YaWC(=EIRsAzA$$v-
z$q^otGR)Jfo#SD2i;s9=d7VK&&%=t^y)Pd<a+o`GsFNKF4*S9(0l~iTorvQ(FY=9a
z1~_lX6AlF?JP{NY!kt1m9N;^B%8`4xJ3$X@c}HYIvWLPb=neRzoM(i)i=6OH2mJWM
zP{oOY*`Dwwh7*?fsU?#&vHznxDe{A8>WvTIFVK$Ej^w!nS+GH8re(V2Q}=?cF-tYB
z!c5|sEru;qw)iiw@EO97H;jnsL}FCiVmwDF>X!8o*ZvAys~7dp+t?T-Qam|XD^jDy
z>!<R;Evp?IvWXN62L}hMyGe+os5=hhlLtgyoSb|KW}8aqDScIvm_dZ2Zh)7gmgi6z
z1)Dl58Z?EWZuP(w#T+QiA%s_M5{;vFm3FOVwOQzhX!_u=Xevu(RCyztfR9QpqDg%V
z++lUHv;a`+i)fr9Sd(a)Bfik9Ge~0cx6hwbLisHPy9cUl9(YQ2J^3#bg!L4ep^~WA
zFI{{UVT622GH#1x<>B%R0e^_&B?B)Ye?&5KA(kKa3nTCX4@!oyNQ6TO?;X$!UL?rF
zvL;GKFARoQw^^bD?yevi6=0G~zA=QjkRa)icU+?I7bF9qnZQfBa75C3(M=vp#1sp{
z8zs>|!E+u3@X&5}RSQ2JBL=8?Q*-=mp~4kES8!BKy`OwP=U{#yT!xl}zTj|8O(Z8i
zc{f2lc2pJUYS8(q?qqkmDsS6XsNIr2n0_VYPn;`kXA);qFDGA<NnDAOxOG;~Sf{O@
z(g{Ps?n>=XUYWX{yq>dfOX!xiY)f-<dos5_>qu~^Qy-7av+ymOU1nXIw=tQE84v#U
zd&&3GY~IndRNIs}ovUq4=?k<Ae`k^2xj^sC3}*)CE9Vc+H)pyZ(fgO589VTZ-o4Tc
z%UIb>(5`qt!b<VX?Zlcd1K{uAAYc4;rpRljUig02ZF)b+N%sacI#v4+IeBaY8cmmh
zrhfw(s)Ubc1DdrPxD_bMU;<lm`(#8htwWSa8BwNS_H(d;HRJn<aiuJ3tw}*n{$>Lj
zi?*6q%HdATC};@7T1#+3lb^Lk;i5tfr~Uw6VJy*ev4f>CZm@QYAzx^_NfIe?(!^GX
zhC2kR0cp#u8(bKx`VDRE&qFE0Xq6&SX|3Y1x^nr;Jw-fn3`9-cN{Lnt0#-1Hi(qpY
zQhb0Y4Gs>YdMZ&}=N^C*@G=no5UR$NjAIzQWH3Yc^id72FiJcnTisSvhac;4wG~(R
z6wwx3VY?~mgWkI`kfCk(T_aR(Gun>(Kf)D*s~x!7i7R|Sk_D`;M=|*n4_3GgY*i?*
zg`F^LwNX3F>x3VF8O&!Xa4l=VwMsCCjtzk8Wb$PCXx`Rb#4&ixHtx&Y_OCssPvmWT
zN*)gZ7Qy2(pdOxlIB(mT5x$On8GCp!-*R*V09>{y0Jy9IVET<|2Y{f>xoB$yPa%Ca
zZ);k{SgOA0$=h};)i-CjTzy-jcd4p2b^G&!>4~`$^QRUX+aK;&*m5vebtuvEEcgx1
z@0zcjzx}Y`p)K2VJWqE&#yl%h&B^11>V}yM(-$)O%p1AtmU(iadQaj^!Ca9TPdXOO
z+ZW8+(_{DEoqcyM_IGpp$|(}|Y^8@Rfyv^vfW0ON>|V$)`Ag`?FuAz{bBrLa0*{zJ
zM%~2Mo!rFX0i}}Zjc^eu(S*HBaBgV0RAqciQM<}uz_-ISFo-%)FS|9}@T3DHO=8E_
z;1{?cFRLWjQKMr0BnqpOWRe|gu+BzS_Rl4X4M%v%>hp$JKMS5UjPS(~9!AP&CoQw^
zD25pwfz7!BKc0gMbhE+<_OyQcJ$ja&tN4L17@CuG!kD58HFXJVVJma*{OtL;z8?sk
zWlypXjAsuR-<0r)Sa5DxbnaMi?#S$Z<aDnXV0^_$G&UzpDdWeE6&o;Gp$WPwKA;%1
z(*3~zq!=`)X9(DN>_oy{Szp%NLz38lLNh)aQs@Qk+ajSt69DAqGpUl9nxpzcGdJh0
znGld$SI)?&U<z*bnWENF*dQS{Yb<B@)?C_{af7`Aodxq?UT+>I_dl23@{A*T4m7v?
zS(UDNlNC*wrp!M5O~R+U25>IlC{xTVn!!1+h^A@XBux=9OANoWpo1HH&#Io~h9_^^
zl%iDT@~fgtco3VMQ?GVT)(vD<PQYHGSK2DzWGcQW)r#`+I5s$ajSr4w*JPf&@FM5M
zI?HO5=CrX+B|i2+mc*xznPaAL!d*EKt!~0u3Fg$renv@F`1x>1BBG8SC1s&tP8Sok
z%LxkYac@6P7eE@JwV2zG5sYa+p(HX&k_+yxsIHBP>e}H4d|X|Sp9mL|3^J~{qsD<S
zz+hMOWIJ;yq`)Ps=0}3w2}qyZxWOUDA7Zq01kZ#K!v*~U&V!6_0f=w-j%amJ>TqN&
zT>+nGTBAltXz*ARi1taVn^N2d91$UG=Ot=1><_tZXdiyFA6EzPYl9qEp@X<@QcxP;
z8q;#DM6!~O4@j0VRc3Su=y=Rj4T_*u;vzeQQY?o&;4y`ffKCIA4-<c;_!o3V{7iwe
z{Iu_bzHDVno@y;Vq+EHbTJ4|w>R{&1{bQN-Y~{W@wO@VR{Z&<F@P0$amaS~dQ|;<&
zJabuPc_L4pEHv)C*FD=kcM{u(uA~EOgz2%(Rj6s0d3*Zp^mwkOC2_VuS5EaM`_c!}
zH_}%!Z_XPtce4%q<dCOiAlv+Mw&BPl`Y5&%U0@{)RxG+K?K0Eywf#%`eaE7+YkDko
zJH7MQ=;xJLXIH#;!P)iL<b;IB6rH3~SMuiV#eTNtt-SfNI`C%RT(3zkZ^oK+(;3=}
z)~(0|rFW<6Gp?^r&r|n%Gsos{WNTi^n-8nJ2Gc$FdS`nx?A&V$HG3bK+rZ8l+QH71
zN(@fd(d5z8r5w0S?1F7)mfHEB)dr&S7*E3){i)k}uGaWxGX-_|sO}*g;tWxe%+jte
zOWt}JbZP4vT(CNU0;X~q#aWwm<r}@~#goJYC1{@hDE6Ay6-cBRuz#$A1tioqqn9%z
z8oh2)dgC+vAsJUTUt;>ktnsA47;16Rn!s!+jiDr3(xM!Qr?hNJi77M*TAU&pAqP`*
z7{RdUM{($|t_V1OkPD_3%@2yMgZ%yCT-aHQ+dA+BA4If!jQ8H;x|sh@+%d-$Z0mqr
z-U;S72EYyo4xp>#Q9FX{3CMy{Hz3QZgfciE@&tb{Y8Vr4v>$;{NX9@S)gQVk$3AXa
z$-)>S$d6Mi`~>#?1V9EPnIc|cB;X&06c2PH3*x-22d8A@G>ROO$iAOs9Y^4ADnl4Z
zAPYo6Hs+3GQ{?qvMv_GiX5_9J<W*j(6mq6Vp^&@w;>=?1$0pA$`kNRCd8}6&s40*}
z1tD{duqXNvruYL?abgKln1?=^NS*rdy(P0fThX5%yu3JgePQtWBQqpgoZq_|X4<CP
z(n99c?0C-A62GwItec^y>GWV`$L!^tvpL?o<fxqzlVZ9jQ#pGs=hzj0b=kFT(bclx
zYI#_fb+zPNN8=X?&W1&2(}J^U{&LpYlyklm@BO}-$u#Dw+vEL9E+*5EbL|E06<gBX
z^Luj@hvVm#DSDBrTcGMbw`YP6-}z%puKs-X($y?gm#3~3Y_#m=N@kA-FU;csBO!;6
zddR9tM#KqYD1?S!l`tR&oVbtPf$AyP9iQ+H(6uo*`Hg$mt^t{BO|D`x*`(l}+gR?c
z%tmGYI*>&z8Y6j3(u2OZD<zZ1!-jnxk7V_DZj6CQoX3N(#-To3org*?3KJ2ma9F(&
zj;Z9(d7T!?CP+R#ykh*10cLt}f`>@v%w4~LuoS-{<UNtk`>FYOFwBkxxD$wlA?)k(
zcn4PWBuV~@qDboBG(k3fM^yZSu>O<SwrZrvt*aHaq-*uSZm8ZQ&1BVT?KZM$^~Yo-
pX<un2C^`}So4(<(wR(Cm-E^;Yw)NBNIqR-0wQEIBP+R10{}1{Dr<4Ey


From de05f3f84a8988dc944742fb60b10f73c7a986e3 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 00:59:03 +0000
Subject: [PATCH 05/17] Add requireGt helper and setIfGreater example

---
 STATUS.md                                     |  1 +
 docs/research-log.md                          |  4 ++
 .../DumbContracts/Compiler.lean               | 15 ++++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 43 ++++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/SetIfGreater.lean  | 44 +++++++++++++++++++
 .../DumbContracts/Examples/StoreOps.lean      | 17 +++----
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedSetIfGreater.t.sol          | 26 +++++++++++
 9 files changed, 145 insertions(+), 9 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/SetIfGreater.lean
 create mode 100644 research/lean_only_proto/test/GeneratedSetIfGreater.t.sol

diff --git a/STATUS.md b/STATUS.md
index ee7df26be..5a49398c1 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -46,6 +46,7 @@ Last updated: 2026-02-10
 - Added a `requireNonZero` helper and a tiny `setNonZero` example + Foundry test.
 - Aligned direct EVM asm with solc for `setNonZero` (label pushes use `PUSH2`).
 - Added `requireEq`/`requireNeq` helpers plus a `compareAndSwap` example + Foundry test.
+- Added `requireGt` helper plus a `setIfGreater` example + Foundry test (and refactored guarded add to use it).
 - 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 cf0629203..17c44a9cf 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,10 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireGt` stdlib helper to reduce guard boilerplate.
+- Added `setIfGreater` example (guarded store on `value > min`) with SpecR + proofs.
+- Refactored `guardedAddSlot` to use `requireGt`.
+- Added Foundry test for `setIfGreater`.
 - Added `eq`/`neq` plus `requireEq`/`requireNeq` stdlib helpers.
 - Added `compareAndSwap` example (guarded store on expected value match) with SpecR and proofs.
 - Avoided double `sload` in `compareAndSwap` by caching the slot value with `let_` (prevents false reverts).
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 8a3f065e5..8467409e3 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -155,8 +155,21 @@ def exampleEntry7 : EntryPoint :=
     selector := 0xc74962fa
     returns := false }
 
+def exampleEntry8 : EntryPoint :=
+  { name := "setIfGreater"
+    args := ["slot", "value", "min"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.gt (Lang.Expr.var "value") (Lang.Expr.var "min"))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfGreater(uint256,uint256,uint256) -> 0x2dbeb1ba
+    selector := 0x2dbeb1ba
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
-  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7]
+  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
+    exampleEntry8]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 0f9a83755..37a98e421 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -38,13 +38,30 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_setNonZero"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xc74962fa"
   , "EQ"
   , "PUSH2 tag_compareAndSwap"
   , "JUMPI"
+  , "PUSH4 0x2dbeb1ba"
+  , "EQ"
+  , "PUSH2 tag_setIfGreater"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_setIfGreater:"
+  , "PUSH2 ret_setIfGreater"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfGreater"
+  , "JUMP"
+  , "ret_setIfGreater:"
+  , "STOP"
   , "tag_compareAndSwap:"
   , "PUSH2 ret_compareAndSwap"
   , "PUSH1 0x44"
@@ -244,6 +261,32 @@ def directProgramAsm : List String :=
   , "DUP1"
   , "PUSH2 compareAndSwap_check"
   , "JUMP"
+  , "fn_setIfGreater:"
+  , "DUP2"
+  , "SWAP1"
+  , "DUP4"
+  , "DUP3"
+  , "GT"
+  , "PUSH2 setIfGreater_ok"
+  , "JUMPI"
+  , "setIfGreater_check:"
+  , "POP"
+  , "POP"
+  , "GT"
+  , "ISZERO"
+  , "PUSH2 setIfGreater_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "setIfGreater_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "setIfGreater_ok:"
+  , "SSTORE"
+  , "DUP1"
+  , "PUSH0"
+  , "PUSH2 setIfGreater_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 16fdc85c6..b5ec49c24 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -6,3 +6,4 @@ import DumbContracts.Examples.TokenTransfer
 import DumbContracts.Examples.MaxStore
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
+import DumbContracts.Examples.SetIfGreater
diff --git a/research/lean_only_proto/DumbContracts/Examples/SetIfGreater.lean b/research/lean_only_proto/DumbContracts/Examples/SetIfGreater.lean
new file mode 100644
index 000000000..ece8d6d6b
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/SetIfGreater.lean
@@ -0,0 +1,44 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Store a value into a slot only if it exceeds a minimum. -/
+
+def setIfGreaterFun : Fun :=
+  { name := "setIfGreater"
+    args := ["slot", "value", "min"]
+    body := requireGt (v "value") (v "min") (sstoreVar "slot" (v "value"))
+    ret := none }
+
+def setIfGreaterSpecR (slot value min : Nat) : SpecR Store :=
+  { requires := fun _ => value > min
+    ensures := fun s s' => s' = updateStore s slot value
+    reverts := fun _ => value <= min }
+
+theorem setIfGreater_meets_specR_ok (s : Store) (slot value min : Nat) :
+    (setIfGreaterSpecR slot value min).requires s ->
+    (match execFun setIfGreaterFun [slot, value, min] s [] with
+      | ExecResult.ok _ s' => (setIfGreaterSpecR slot value min).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hgt : value > min := by exact hreq
+  simp [setIfGreaterSpecR, setIfGreaterFun, requireGt, require, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hgt]
+
+theorem setIfGreater_meets_specR_reverts (s : Store) (slot value min : Nat) :
+    (setIfGreaterSpecR slot value min).reverts s ->
+    execFun setIfGreaterFun [slot, value, min] s [] = ExecResult.reverted := by
+  intro hrev
+  have hnot : ¬ value > min := by
+    exact Nat.not_lt.mpr hrev
+  simp [setIfGreaterSpecR, setIfGreaterFun, requireGt, require, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean b/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
index 1e809ace8..0a82c1fdd 100644
--- a/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
@@ -32,8 +32,9 @@ def addSlotFun : Fun :=
 def guardedAddSlotFun : Fun :=
   { name := "guardedAddSlot"
     args := ["slot", "delta"]
-    body := require
-      (Expr.gt (Expr.var "delta") (Expr.lit 0))
+    body := requireGt
+      (v "delta")
+      (n 0)
       (Stmt.sstore (Expr.var "slot")
         (Expr.add (Expr.sload (Expr.var "slot")) (Expr.var "delta")))
     ret := none }
@@ -80,13 +81,13 @@ 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]
+    updateEnv, updateStore, h, requireGt, v, n]
 
 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]
+    updateEnv, updateStore, h, requireGt, v, n]
 
 -- Storage specs (Store-level).
 
@@ -119,7 +120,7 @@ theorem guardedAddSlot_meets_spec (s : Store) (slot delta : Nat) :
   intro hreq
   have hpos : delta > 0 := by exact hreq
   simp [guardedAddSlotSpec, guardedAddSlotFun, require, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hpos]
+    bindArgs, emptyEnv, updateEnv, updateStore, hpos, requireGt, v, n]
 
 theorem guardedAddSlot_meets_specR_ok (s : Store) (slot delta : Nat) :
     (guardedAddSlotSpecR slot delta).requires s ->
@@ -129,14 +130,14 @@ theorem guardedAddSlot_meets_specR_ok (s : Store) (slot delta : Nat) :
   intro hreq
   have hpos : delta > 0 := by exact hreq
   simp [guardedAddSlotSpecR, guardedAddSlotFun, require, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hpos]
+    bindArgs, emptyEnv, updateEnv, updateStore, hpos, requireGt, v, n]
 
 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]
+    bindArgs, emptyEnv, updateEnv, updateStore, hrev, requireGt, v, n]
 
 theorem guardedAddSlot_reverts_when_not_requires (slot delta : Nat) (h : delta = 0) :
     (guardedAddSlotSpec slot delta).requires (storeOf slot 0) = False ∧
@@ -144,6 +145,6 @@ theorem guardedAddSlot_reverts_when_not_requires (slot delta : Nat) (h : delta =
   constructor
   · simp [guardedAddSlotSpec, h]
   · simp [guardedAddSlotFun, require, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv,
-      updateEnv, updateStore, h]
+      updateEnv, updateStore, h, requireGt, v, n]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index 6bad9d99e..37ca1bf39 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -31,6 +31,9 @@ def requireEq (lhs rhs : Expr) (body : Stmt) : Stmt :=
 def requireNeq (lhs rhs : Expr) (body : Stmt) : Stmt :=
   require (neq lhs rhs) body
 
+def requireGt (lhs rhs : Expr) (body : Stmt) : Stmt :=
+  require (Expr.gt lhs rhs) body
+
 def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
   requireNeq value (Expr.lit 0) body
 
diff --git a/research/lean_only_proto/test/GeneratedSetIfGreater.t.sol b/research/lean_only_proto/test/GeneratedSetIfGreater.t.sol
new file mode 100644
index 000000000..a6a4131e1
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedSetIfGreater.t.sol
@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedSetIfGreaterTest is GeneratedBase {
+    function testSetIfGreater() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selSet = 0x2dbeb1ba;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 11, 10, 5));
+        require(ok, "setIfGreater failed (value > min)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 11));
+        require(ok, "getSlot failed (slot 11)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 10, "unexpected setIfGreater value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSet, 12, 4, 9));
+        require(!ok, "setIfGreater should revert when value <= min");
+    }
+}

From c3bf8bf32f276f9a847022bef823fcb493a6e650 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 01:27:56 +0000
Subject: [PATCH 06/17] Add sstoreAdd helper and bumpSlot example

---
 STATUS.md                                     |  1 +
 docs/research-log.md                          |  5 +++
 .../DumbContracts/Compiler.lean               | 13 +++++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 21 ++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/BumpSlot.lean      | 33 +++++++++++++++++++
 .../DumbContracts/Examples/StoreOps.lean      | 23 ++++++-------
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedBumpSlot.t.sol              | 27 +++++++++++++++
 9 files changed, 115 insertions(+), 12 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/BumpSlot.lean
 create mode 100644 research/lean_only_proto/test/GeneratedBumpSlot.t.sol

diff --git a/STATUS.md b/STATUS.md
index 5a49398c1..cd0928d29 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -47,6 +47,7 @@ Last updated: 2026-02-10
 - Aligned direct EVM asm with solc for `setNonZero` (label pushes use `PUSH2`).
 - Added `requireEq`/`requireNeq` helpers plus a `compareAndSwap` example + Foundry test.
 - Added `requireGt` helper plus a `setIfGreater` example + Foundry test (and refactored guarded add to use it).
+- Added `sstoreAdd` helper plus a `bumpSlot` example + Foundry test (and refactored add-slot examples to use it).
 - 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 17c44a9cf..a2ad76630 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `sstoreAdd` stdlib helper to make slot increments less noisy.
+- Added `bumpSlot` example (increment slot by one) with a basic Spec + proof.
+- Refactored `addSlot` and `guardedAddSlot` to use `sstoreAdd`.
+- Added Foundry test for `bumpSlot`.
+- Updated compiler entries + direct EVM asm for `bumpSlot`.
 - Added `requireGt` stdlib helper to reduce guard boilerplate.
 - Added `setIfGreater` example (guarded store on `value > min`) with SpecR + proofs.
 - Refactored `guardedAddSlot` to use `requireGt`.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 8467409e3..19429d34e 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -167,9 +167,20 @@ def exampleEntry8 : EntryPoint :=
     selector := 0x2dbeb1ba
     returns := false }
 
+def exampleEntry9 : EntryPoint :=
+  { name := "bumpSlot"
+    args := ["slot"]
+    body :=
+      Lang.Stmt.sstore
+        (Lang.Expr.var "slot")
+        (Lang.Expr.add (Lang.Expr.sload (Lang.Expr.var "slot")) (Lang.Expr.lit 1))
+    -- bumpSlot(uint256) -> 0xb8df0e12
+    selector := 0xb8df0e12
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
-    exampleEntry8]
+    exampleEntry8, exampleEntry9]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 37a98e421..0baa76612 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -43,13 +43,26 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_compareAndSwap"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x2dbeb1ba"
   , "EQ"
   , "PUSH2 tag_setIfGreater"
   , "JUMPI"
+  , "PUSH4 0xb8df0e12"
+  , "EQ"
+  , "PUSH2 tag_bumpSlot"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_bumpSlot:"
+  , "PUSH2 ret_bumpSlot"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_bumpSlot"
+  , "JUMP"
+  , "ret_bumpSlot:"
+  , "STOP"
   , "tag_setIfGreater:"
   , "PUSH2 ret_setIfGreater"
   , "PUSH1 0x44"
@@ -287,6 +300,14 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 setIfGreater_check"
   , "JUMP"
+  , "fn_bumpSlot:"
+  , "PUSH1 0x01"
+  , "DUP2"
+  , "SLOAD"
+  , "ADD"
+  , "SWAP1"
+  , "SSTORE"
+  , "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 b5ec49c24..e6a00f9ec 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -7,3 +7,4 @@ import DumbContracts.Examples.MaxStore
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.SetIfGreater
+import DumbContracts.Examples.BumpSlot
diff --git a/research/lean_only_proto/DumbContracts/Examples/BumpSlot.lean b/research/lean_only_proto/DumbContracts/Examples/BumpSlot.lean
new file mode 100644
index 000000000..959d24c0f
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/BumpSlot.lean
@@ -0,0 +1,33 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Increment a slot by one. -/
+
+def bumpSlotFun : Fun :=
+  { name := "bumpSlot"
+    args := ["slot"]
+    body := sstoreAdd (v "slot") (n 1)
+    ret := none }
+
+def bumpSlotSpec (slot : Nat) : Spec Store :=
+  { requires := fun _ => True
+    ensures := fun s s' => s' = updateStore s slot (s slot + 1) }
+
+theorem bumpSlot_meets_spec (s : Store) (slot : Nat) :
+    (bumpSlotSpec slot).requires s ->
+    (match execFun bumpSlotFun [slot] s [] with
+      | ExecResult.ok _ s' => (bumpSlotSpec slot).ensures s s'
+      | _ => False) := by
+  intro _hreq
+  simp [bumpSlotSpec, bumpSlotFun, sstoreAdd, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, v, n]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean b/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
index 0a82c1fdd..fe1cd2238 100644
--- a/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
@@ -26,7 +26,7 @@ def setSlotFun : Fun :=
 def addSlotFun : Fun :=
   { name := "addSlot"
     args := ["slot", "delta"]
-    body := Stmt.sstore (Expr.var "slot") (Expr.add (Expr.sload (Expr.var "slot")) (Expr.var "delta"))
+    body := sstoreAdd (v "slot") (v "delta")
     ret := none }
 
 def guardedAddSlotFun : Fun :=
@@ -35,8 +35,7 @@ def guardedAddSlotFun : Fun :=
     body := requireGt
       (v "delta")
       (n 0)
-      (Stmt.sstore (Expr.var "slot")
-        (Expr.add (Expr.sload (Expr.var "slot")) (Expr.var "delta")))
+      (sstoreAdd (v "slot") (v "delta"))
     ret := none }
 
 /-- A minimal store for point examples. -/
@@ -59,7 +58,7 @@ theorem setSlot_updates (slot value : Nat) :
 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]
+  simp [addSlotFun, sstoreAdd, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv, updateEnv, updateStore]
 
 theorem set_then_get (slot value : Nat) :
     (match execFun setSlotFun [slot, value] (storeOf slot 0) [] with
@@ -75,13 +74,14 @@ theorem add_then_get (slot base delta : Nat) :
           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]
+  simp [addSlotFun, sstoreAdd, 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, requireGt, v, n]
+    updateEnv, updateStore, h, requireGt, v, n, sstoreAdd]
 
 theorem guarded_add_reverts (slot base delta : Nat) (h : delta = 0) :
     execFun guardedAddSlotFun [slot, delta] (storeOf slot base) [] =
@@ -110,7 +110,8 @@ theorem addSlot_meets_spec (s : Store) (slot delta : Nat) :
       | ExecResult.ok _ s' => (addSlotSpec slot delta).ensures s s'
       | _ => False) := by
   intro _hreq
-  simp [addSlotSpec, addSlotFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore]
+  simp [addSlotSpec, addSlotFun, sstoreAdd, execFun, execStmt, evalExpr, bindArgs, emptyEnv,
+    updateEnv, updateStore]
 
 theorem guardedAddSlot_meets_spec (s : Store) (slot delta : Nat) :
     (guardedAddSlotSpec slot delta).requires s ->
@@ -120,7 +121,7 @@ theorem guardedAddSlot_meets_spec (s : Store) (slot delta : Nat) :
   intro hreq
   have hpos : delta > 0 := by exact hreq
   simp [guardedAddSlotSpec, guardedAddSlotFun, require, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hpos, requireGt, v, n]
+    bindArgs, emptyEnv, updateEnv, updateStore, hpos, requireGt, v, n, sstoreAdd]
 
 theorem guardedAddSlot_meets_specR_ok (s : Store) (slot delta : Nat) :
     (guardedAddSlotSpecR slot delta).requires s ->
@@ -130,14 +131,14 @@ theorem guardedAddSlot_meets_specR_ok (s : Store) (slot delta : Nat) :
   intro hreq
   have hpos : delta > 0 := by exact hreq
   simp [guardedAddSlotSpecR, guardedAddSlotFun, require, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hpos, requireGt, v, n]
+    bindArgs, emptyEnv, updateEnv, updateStore, hpos, requireGt, v, n, sstoreAdd]
 
 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, requireGt, v, n]
+    bindArgs, emptyEnv, updateEnv, updateStore, hrev, requireGt, v, n, sstoreAdd]
 
 theorem guardedAddSlot_reverts_when_not_requires (slot delta : Nat) (h : delta = 0) :
     (guardedAddSlotSpec slot delta).requires (storeOf slot 0) = False ∧
@@ -145,6 +146,6 @@ theorem guardedAddSlot_reverts_when_not_requires (slot delta : Nat) (h : delta =
   constructor
   · simp [guardedAddSlotSpec, h]
   · simp [guardedAddSlotFun, require, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv,
-      updateEnv, updateStore, h, requireGt, v, n]
+      updateEnv, updateStore, h, requireGt, v, n, sstoreAdd]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index 37ca1bf39..f179d64a1 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -39,6 +39,9 @@ def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
 
 /-- Shorthand for loading/storing fixed slots. -/
 
+def sstoreAdd (slot delta : Expr) : Stmt :=
+  Stmt.sstore slot (Expr.add (Expr.sload slot) delta)
+
 def sloadSlot (slot : Nat) : Expr :=
   Expr.sload (Expr.lit slot)
 
diff --git a/research/lean_only_proto/test/GeneratedBumpSlot.t.sol b/research/lean_only_proto/test/GeneratedBumpSlot.t.sol
new file mode 100644
index 000000000..0c857f659
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedBumpSlot.t.sol
@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedBumpSlotTest is GeneratedBase {
+    function testBumpSlot() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selBump = 0xb8df0e12;
+        bytes4 selSet = 0xf2c298be;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 5, 41));
+        require(ok, "setSlot failed (slot 5)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selBump, 5));
+        require(ok, "bumpSlot failed");
+
+        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 == 42, "unexpected bumpSlot value");
+    }
+}

From 7dbdf0d96eb804ff0d19c9c32f2902d73fc1dd7e Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 01:59:03 +0000
Subject: [PATCH 07/17] Add revertIf helper and setIfLess example

---
 STATUS.md                                     |  2 +
 docs/research-log.md                          |  5 ++
 .../DumbContracts/Compiler.lean               | 14 +++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 43 +++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/Risk.lean          | 13 +++---
 .../DumbContracts/Examples/SetIfLess.lean     | 46 +++++++++++++++++++
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedSetIfLess.t.sol             | 26 +++++++++++
 9 files changed, 145 insertions(+), 8 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/SetIfLess.lean
 create mode 100644 research/lean_only_proto/test/GeneratedSetIfLess.t.sol

diff --git a/STATUS.md b/STATUS.md
index cd0928d29..ceba0e72d 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -48,6 +48,8 @@ Last updated: 2026-02-10
 - Added `requireEq`/`requireNeq` helpers plus a `compareAndSwap` example + Foundry test.
 - Added `requireGt` helper plus a `setIfGreater` example + Foundry test (and refactored guarded add to use it).
 - Added `sstoreAdd` helper plus a `bumpSlot` example + Foundry test (and refactored add-slot examples to use it).
+- Added a `revertIf` helper, refactored `checkHealth`, and added a `setIfLess` example + Foundry test.
+- Updated compiler entries + direct EVM asm for `setIfLess`.
 - 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 a2ad76630..de6f3cfa5 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `revertIf` stdlib helper for guard-style reverts.
+- Refactored `checkHealth` to use `revertIf`.
+- Added `setIfLess` example (guarded store on `value < max`) with SpecR + proofs.
+- Added Foundry test for `setIfLess`.
+- Updated compiler entries + direct EVM asm for `setIfLess`.
 - Added `sstoreAdd` stdlib helper to make slot increments less noisy.
 - Added `bumpSlot` example (increment slot by one) with a basic Spec + proof.
 - Refactored `addSlot` and `guardedAddSlot` to use `sstoreAdd`.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 19429d34e..e5d423be9 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -178,9 +178,21 @@ def exampleEntry9 : EntryPoint :=
     selector := 0xb8df0e12
     returns := false }
 
+def exampleEntry10 : EntryPoint :=
+  { name := "setIfLess"
+    args := ["slot", "value", "max"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "max"))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfLess(uint256,uint256,uint256) -> 0x7e5acdb6
+    selector := 0x7e5acdb6
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
-    exampleEntry8, exampleEntry9]
+    exampleEntry8, exampleEntry9, exampleEntry10]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 0baa76612..6eb3c228b 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -48,13 +48,30 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_setIfGreater"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xb8df0e12"
   , "EQ"
   , "PUSH2 tag_bumpSlot"
   , "JUMPI"
+  , "PUSH4 0x7e5acdb6"
+  , "EQ"
+  , "PUSH2 tag_setIfLess"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_setIfLess:"
+  , "PUSH2 ret_setIfLess"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfLess"
+  , "JUMP"
+  , "ret_setIfLess:"
+  , "STOP"
   , "tag_bumpSlot:"
   , "PUSH2 ret_bumpSlot"
   , "PUSH1 0x04"
@@ -308,6 +325,32 @@ def directProgramAsm : List String :=
   , "SWAP1"
   , "SSTORE"
   , "JUMP"
+  , "fn_setIfLess:"
+  , "DUP2"
+  , "SWAP1"
+  , "DUP4"
+  , "DUP3"
+  , "LT"
+  , "PUSH2 setIfLess_ok"
+  , "JUMPI"
+  , "setIfLess_check:"
+  , "POP"
+  , "POP"
+  , "LT"
+  , "ISZERO"
+  , "PUSH2 setIfLess_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "setIfLess_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "setIfLess_ok:"
+  , "SSTORE"
+  , "DUP1"
+  , "PUSH0"
+  , "PUSH2 setIfLess_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 e6a00f9ec..1caf07e96 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -7,4 +7,5 @@ import DumbContracts.Examples.MaxStore
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.SetIfGreater
+import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.BumpSlot
diff --git a/research/lean_only_proto/DumbContracts/Examples/Risk.lean b/research/lean_only_proto/DumbContracts/Examples/Risk.lean
index 2fb438d83..a0f397c96 100644
--- a/research/lean_only_proto/DumbContracts/Examples/Risk.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/Risk.lean
@@ -34,9 +34,8 @@ def setRiskFun : Fun :=
 def checkHealthFun : Fun :=
   { name := "checkHealth"
     args := []
-    body := unless
+    body := revertIf
       (Expr.lt (sloadSlot 0) (Expr.mul (sloadSlot 1) (sloadSlot 2)))
-      Stmt.skip
     ret := none }
 
 -- Execution facts.
@@ -52,13 +51,13 @@ theorem setRisk_updates (collateral debt minHF : Nat) :
 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,
+  simp [checkHealthFun, revertIf, 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,
+  simp [checkHealthFun, revertIf, sloadSlot, execFun, execStmt, evalExpr, riskStore,
     bindArgs, emptyEnv, updateEnv, updateStore, h]
 
 -- Risk specs (Store-level).
@@ -95,7 +94,7 @@ theorem checkHealth_meets_spec (s : Store) :
       | ExecResult.ok _ s' => checkHealthSpec.ensures s s'
       | _ => False) := by
   intro hreq
-  simp [checkHealthSpec, riskOk, checkHealthFun, unless, sloadSlot, execFun, execStmt,
+  simp [checkHealthSpec, riskOk, checkHealthFun, revertIf, sloadSlot, execFun, execStmt,
     evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, not_lt_of_ge hreq]
 
 theorem checkHealth_meets_specR_ok (s : Store) :
@@ -104,14 +103,14 @@ theorem checkHealth_meets_specR_ok (s : Store) :
       | ExecResult.ok _ s' => checkHealthSpecR.ensures s s'
       | _ => False) := by
   intro hreq
-  simp [checkHealthSpecR, riskOk, checkHealthFun, unless, sloadSlot, execFun, execStmt,
+  simp [checkHealthSpecR, riskOk, checkHealthFun, revertIf, 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,
+  simp [checkHealthSpecR, checkHealthFun, revertIf, sloadSlot, execFun, execStmt, evalExpr,
     bindArgs, emptyEnv, updateEnv, updateStore, hrev]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/SetIfLess.lean b/research/lean_only_proto/DumbContracts/Examples/SetIfLess.lean
new file mode 100644
index 000000000..01d403fb4
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/SetIfLess.lean
@@ -0,0 +1,46 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Store a value into a slot only if it is below a maximum. -/
+
+def setIfLessFun : Fun :=
+  { name := "setIfLess"
+    args := ["slot", "value", "max"]
+    body :=
+      revertIf (Expr.not (Expr.lt (v "value") (v "max"))) ;;
+      sstoreVar "slot" (v "value")
+    ret := none }
+
+def setIfLessSpecR (slot value max : Nat) : SpecR Store :=
+  { requires := fun _ => value < max
+    ensures := fun s s' => s' = updateStore s slot value
+    reverts := fun _ => value >= max }
+
+theorem setIfLess_meets_specR_ok (s : Store) (slot value max : Nat) :
+    (setIfLessSpecR slot value max).requires s ->
+    (match execFun setIfLessFun [slot, value, max] s [] with
+      | ExecResult.ok _ s' => (setIfLessSpecR slot value max).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hlt : value < max := by exact hreq
+  simp [setIfLessSpecR, setIfLessFun, revertIf, sstoreVar, v, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hlt]
+
+theorem setIfLess_meets_specR_reverts (s : Store) (slot value max : Nat) :
+    (setIfLessSpecR slot value max).reverts s ->
+    execFun setIfLessFun [slot, value, max] s [] = ExecResult.reverted := by
+  intro hrev
+  have hnot : ¬ value < max := by
+    exact Nat.not_lt.mpr hrev
+  simp [setIfLessSpecR, setIfLessFun, revertIf, sstoreVar, v, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index f179d64a1..c4c8f29b3 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -16,6 +16,9 @@ def require (cond : Expr) (body : Stmt) : Stmt :=
 def unless (cond : Expr) (body : Stmt) : Stmt :=
   Stmt.if_ cond Stmt.revert body
 
+def revertIf (cond : Expr) : Stmt :=
+  Stmt.if_ cond Stmt.revert Stmt.skip
+
 def assert (cond : Expr) : Stmt :=
   Stmt.if_ cond Stmt.skip Stmt.revert
 
diff --git a/research/lean_only_proto/test/GeneratedSetIfLess.t.sol b/research/lean_only_proto/test/GeneratedSetIfLess.t.sol
new file mode 100644
index 000000000..a08d3e322
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedSetIfLess.t.sol
@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedSetIfLessTest is GeneratedBase {
+    function testSetIfLess() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selSet = 0x7e5acdb6;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 21, 7, 10));
+        require(ok, "setIfLess failed (value < max)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 21));
+        require(ok, "getSlot failed (slot 21)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 7, "unexpected setIfLess value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSet, 22, 9, 9));
+        require(!ok, "setIfLess should revert when value >= max");
+    }
+}

From 1fbe6fe9b075cd4044283e271fc6bf1e0398c234 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 02:33:44 +0000
Subject: [PATCH 08/17] Add requireLt and setIfBetween example

---
 STATUS.md                                     |  1 +
 docs/research-log.md                          |  5 ++
 .../DumbContracts/Compiler.lean               | 17 ++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 70 +++++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/SetIfBetween.lean  | 57 +++++++++++++++
 .../DumbContracts/Examples/SetIfLess.lean     | 12 ++--
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 +
 .../test/GeneratedSetIfBetween.t.sol          | 29 ++++++++
 9 files changed, 187 insertions(+), 8 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean
 create mode 100644 research/lean_only_proto/test/GeneratedSetIfBetween.t.sol

diff --git a/STATUS.md b/STATUS.md
index ceba0e72d..8f1fb4350 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -19,6 +19,7 @@ Last updated: 2026-02-10
 - 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.
+- Iteration: add `requireLt` guard helper and a range-check example (`setIfBetween`) to reduce boilerplate for bounded updates.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
diff --git a/docs/research-log.md b/docs/research-log.md
index de6f3cfa5..9c9a9afff 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireLt` stdlib helper to mirror `requireGt` for less-than guards.
+- Refactored `setIfLess` to use `requireLt` instead of a manual `revertIf`.
+- Added `setIfBetween` example (guarded store on `min < value < max`) with SpecR + proofs.
+- Added Foundry test for `setIfBetween`.
+- Updated compiler entries + direct EVM asm for `setIfBetween`.
 - Added `revertIf` stdlib helper for guard-style reverts.
 - Refactored `checkHealth` to use `revertIf`.
 - Added `setIfLess` example (guarded store on `value < max`) with SpecR + proofs.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index e5d423be9..d9f157958 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -190,9 +190,24 @@ def exampleEntry10 : EntryPoint :=
     selector := 0x7e5acdb6
     returns := false }
 
+def exampleEntry11 : EntryPoint :=
+  { name := "setIfBetween"
+    args := ["slot", "value", "min", "max"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.gt (Lang.Expr.var "value") (Lang.Expr.var "min"))
+        (Lang.Stmt.if_
+          (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "max"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+          Lang.Stmt.revert)
+        Lang.Stmt.revert
+    -- setIfBetween(uint256,uint256,uint256,uint256) -> 0x5ebc58db
+    selector := 0x5ebc58db
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
-    exampleEntry8, exampleEntry9, exampleEntry10]
+    exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 6eb3c228b..db6b200ee 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -53,13 +53,32 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_bumpSlot"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x7e5acdb6"
   , "EQ"
   , "PUSH2 tag_setIfLess"
   , "JUMPI"
+  , "PUSH4 0x5ebc58db"
+  , "EQ"
+  , "PUSH2 tag_setIfBetween"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_setIfBetween:"
+  , "PUSH2 ret_setIfBetween"
+  , "PUSH1 0x64"
+  , "CALLDATALOAD"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfBetween"
+  , "JUMP"
+  , "ret_setIfBetween:"
+  , "STOP"
   , "tag_setIfLess:"
   , "PUSH2 ret_setIfLess"
   , "PUSH1 0x44"
@@ -351,6 +370,57 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 setIfLess_check"
   , "JUMP"
+  , "fn_setIfBetween:"
+  , "SWAP1"
+  , "DUP1"
+  , "SWAP3"
+  , "SWAP4"
+  , "SWAP2"
+  , "DUP5"
+  , "DUP3"
+  , "GT"
+  , "PUSH2 setIfBetween_outer_ok"
+  , "JUMPI"
+  , "setIfBetween_outer_check:"
+  , "POP"
+  , "POP"
+  , "POP"
+  , "GT"
+  , "ISZERO"
+  , "PUSH2 setIfBetween_revert_outer"
+  , "JUMPI"
+  , "JUMP"
+  , "setIfBetween_revert_outer:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "setIfBetween_outer_ok:"
+  , "DUP3"
+  , "DUP3"
+  , "LT"
+  , "PUSH2 setIfBetween_inner_ok"
+  , "JUMPI"
+  , "setIfBetween_inner_check:"
+  , "POP"
+  , "LT"
+  , "ISZERO"
+  , "PUSH2 setIfBetween_revert_inner"
+  , "JUMPI"
+  , "PUSH0"
+  , "DUP2"
+  , "DUP2"
+  , "PUSH2 setIfBetween_outer_check"
+  , "JUMP"
+  , "setIfBetween_revert_inner:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "setIfBetween_inner_ok:"
+  , "SSTORE"
+  , "DUP2"
+  , "PUSH0"
+  , "PUSH2 setIfBetween_inner_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 1caf07e96..2cbf99f7f 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -8,4 +8,5 @@ import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.SetIfGreater
 import DumbContracts.Examples.SetIfLess
+import DumbContracts.Examples.SetIfBetween
 import DumbContracts.Examples.BumpSlot
diff --git a/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean b/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean
new file mode 100644
index 000000000..4fc32416a
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean
@@ -0,0 +1,57 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Store a value into a slot only if it is strictly between min and max. -/
+
+def setIfBetweenFun : Fun :=
+  { name := "setIfBetween"
+    args := ["slot", "value", "min", "max"]
+    body :=
+      requireGt (v "value") (v "min")
+        (requireLt (v "value") (v "max")
+          (sstoreVar "slot" (v "value")))
+    ret := none }
+
+def setIfBetweenSpecR (slot value min max : Nat) : SpecR Store :=
+  { requires := fun _ => value > min ∧ value < max
+    ensures := fun s s' => s' = updateStore s slot value
+    reverts := fun _ => value <= min ∨ value >= max }
+
+theorem setIfBetween_meets_specR_ok (s : Store) (slot value min max : Nat) :
+    (setIfBetweenSpecR slot value min max).requires s ->
+    (match execFun setIfBetweenFun [slot, value, min, max] s [] with
+      | ExecResult.ok _ s' => (setIfBetweenSpecR slot value min max).ensures s s'
+      | _ => False) := by
+  intro hreq
+  rcases hreq with ⟨hgt, hlt⟩
+  simp [setIfBetweenSpecR, setIfBetweenFun, requireGt, requireLt, require, sstoreVar, v, execFun,
+    execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hlt]
+
+theorem setIfBetween_meets_specR_reverts (s : Store) (slot value min max : Nat) :
+    (setIfBetweenSpecR slot value min max).reverts s ->
+    execFun setIfBetweenFun [slot, value, min, max] s [] = ExecResult.reverted := by
+  intro hrev
+  rcases hrev with hle | hge
+  · have hnot : ¬ value > min := by
+      exact Nat.not_lt.mpr hle
+    simp [setIfBetweenSpecR, setIfBetweenFun, requireGt, requireLt, require, sstoreVar, v, execFun,
+      execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+  · by_cases hgt : value > min
+    · have hnotlt : ¬ value < max := by
+        exact Nat.not_lt.mpr hge
+      simp [setIfBetweenSpecR, setIfBetweenFun, requireGt, requireLt, require, sstoreVar, v,
+        execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hnotlt]
+    · have hnot : ¬ value > min := by
+        exact hgt
+      simp [setIfBetweenSpecR, setIfBetweenFun, requireGt, requireLt, require, sstoreVar, v,
+        execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/SetIfLess.lean b/research/lean_only_proto/DumbContracts/Examples/SetIfLess.lean
index 01d403fb4..b2c7f40f7 100644
--- a/research/lean_only_proto/DumbContracts/Examples/SetIfLess.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/SetIfLess.lean
@@ -14,9 +14,7 @@ open DumbContracts.Std
 def setIfLessFun : Fun :=
   { name := "setIfLess"
     args := ["slot", "value", "max"]
-    body :=
-      revertIf (Expr.not (Expr.lt (v "value") (v "max"))) ;;
-      sstoreVar "slot" (v "value")
+    body := requireLt (v "value") (v "max") (sstoreVar "slot" (v "value"))
     ret := none }
 
 def setIfLessSpecR (slot value max : Nat) : SpecR Store :=
@@ -31,8 +29,8 @@ theorem setIfLess_meets_specR_ok (s : Store) (slot value max : Nat) :
       | _ => False) := by
   intro hreq
   have hlt : value < max := by exact hreq
-  simp [setIfLessSpecR, setIfLessFun, revertIf, sstoreVar, v, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hlt]
+  simp [setIfLessSpecR, setIfLessFun, requireLt, require, sstoreVar, v, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hlt]
 
 theorem setIfLess_meets_specR_reverts (s : Store) (slot value max : Nat) :
     (setIfLessSpecR slot value max).reverts s ->
@@ -40,7 +38,7 @@ theorem setIfLess_meets_specR_reverts (s : Store) (slot value max : Nat) :
   intro hrev
   have hnot : ¬ value < max := by
     exact Nat.not_lt.mpr hrev
-  simp [setIfLessSpecR, setIfLessFun, revertIf, sstoreVar, v, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+  simp [setIfLessSpecR, setIfLessFun, requireLt, require, sstoreVar, v, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index c4c8f29b3..76e5a7987 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -37,6 +37,9 @@ def requireNeq (lhs rhs : Expr) (body : Stmt) : Stmt :=
 def requireGt (lhs rhs : Expr) (body : Stmt) : Stmt :=
   require (Expr.gt lhs rhs) body
 
+def requireLt (lhs rhs : Expr) (body : Stmt) : Stmt :=
+  require (Expr.lt lhs rhs) body
+
 def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
   requireNeq value (Expr.lit 0) body
 
diff --git a/research/lean_only_proto/test/GeneratedSetIfBetween.t.sol b/research/lean_only_proto/test/GeneratedSetIfBetween.t.sol
new file mode 100644
index 000000000..92635e400
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedSetIfBetween.t.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedSetIfBetweenTest is GeneratedBase {
+    function testSetIfBetween() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selSet = 0x5ebc58db;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 21, 7, 5, 10));
+        require(ok, "setIfBetween failed (min < value < max)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 21));
+        require(ok, "getSlot failed (slot 21)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 7, "unexpected setIfBetween value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSet, 22, 5, 5, 10));
+        require(!ok, "setIfBetween should revert when value <= min");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSet, 23, 10, 5, 10));
+        require(!ok, "setIfBetween should revert when value >= max");
+    }
+}

From 083fa131168094d1bceeab4a3a5114f83a331274 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 03:00:46 +0000
Subject: [PATCH 09/17] Add letSload helper and initOnce example

---
 STATUS.md                                     |  2 +-
 docs/research-log.md                          |  5 +++
 .../DumbContracts/Compiler.lean               | 15 ++++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 43 ++++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../Examples/CompareAndSwap.lean              |  6 +--
 .../DumbContracts/Examples/InitOnce.lean      | 44 +++++++++++++++++++
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedInitOnce.t.sol              | 26 +++++++++++
 9 files changed, 140 insertions(+), 5 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/InitOnce.lean
 create mode 100644 research/lean_only_proto/test/GeneratedInitOnce.t.sol

diff --git a/STATUS.md b/STATUS.md
index 8f1fb4350..12724125b 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -19,7 +19,7 @@ Last updated: 2026-02-10
 - 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.
-- Iteration: add `requireLt` guard helper and a range-check example (`setIfBetween`) to reduce boilerplate for bounded updates.
+- Iteration: add `letSload` helper and an `initOnce` example to make cached-slot guards less noisy.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
diff --git a/docs/research-log.md b/docs/research-log.md
index 9c9a9afff..fe5efe09b 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `letSload` stdlib helper for caching a slot read via `let_`.
+- Refactored `compareAndSwap` to use `letSload`.
+- Added `initOnce` example (only initialize a zero slot) with SpecR + proofs.
+- Added Foundry test for `initOnce`.
+- Updated compiler entries + direct EVM asm for `initOnce`.
 - Added `requireLt` stdlib helper to mirror `requireGt` for less-than guards.
 - Refactored `setIfLess` to use `requireLt` instead of a manual `revertIf`.
 - Added `setIfBetween` example (guarded store on `min < value < max`) with SpecR + proofs.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index d9f157958..5d21e4d51 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -155,6 +155,19 @@ def exampleEntry7 : EntryPoint :=
     selector := 0xc74962fa
     returns := false }
 
+def exampleEntry12 : EntryPoint :=
+  { name := "initOnce"
+    args := ["slot", "value"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.eq (Lang.Expr.var "current") (Lang.Expr.lit 0))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+          Lang.Stmt.revert)
+    -- initOnce(uint256,uint256) -> 0xd3b9b05a
+    selector := 0xd3b9b05a
+    returns := false }
+
 def exampleEntry8 : EntryPoint :=
   { name := "setIfGreater"
     args := ["slot", "value", "min"]
@@ -207,7 +220,7 @@ def exampleEntry11 : EntryPoint :=
 
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
-    exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11]
+    exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index db6b200ee..7301791ed 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -44,6 +44,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_compareAndSwap"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0xd3b9b05a"
+  , "EQ"
+  , "PUSH2 tag_initOnce"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x2dbeb1ba"
   , "EQ"
   , "PUSH2 tag_setIfGreater"
@@ -111,6 +116,16 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setIfGreater:"
   , "STOP"
+  , "tag_initOnce:"
+  , "PUSH2 ret_initOnce"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_initOnce"
+  , "JUMP"
+  , "ret_initOnce:"
+  , "STOP"
   , "tag_compareAndSwap:"
   , "PUSH2 ret_compareAndSwap"
   , "PUSH1 0x44"
@@ -310,6 +325,34 @@ def directProgramAsm : List String :=
   , "DUP1"
   , "PUSH2 compareAndSwap_check"
   , "JUMP"
+  , "fn_initOnce:"
+  , "PUSH0"
+  , "SWAP2"
+  , "DUP2"
+  , "SLOAD"
+  , "SWAP2"
+  , "DUP4"
+  , "DUP4"
+  , "EQ"
+  , "PUSH2 initOnce_ok"
+  , "JUMPI"
+  , "initOnce_check:"
+  , "POP"
+  , "POP"
+  , "SUB"
+  , "PUSH2 initOnce_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "initOnce_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "initOnce_ok:"
+  , "SSTORE"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH2 initOnce_check"
+  , "JUMP"
   , "fn_setIfGreater:"
   , "DUP2"
   , "SWAP1"
diff --git a/research/lean_only_proto/DumbContracts/Examples.lean b/research/lean_only_proto/DumbContracts/Examples.lean
index 2cbf99f7f..a164b220d 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -6,6 +6,7 @@ import DumbContracts.Examples.TokenTransfer
 import DumbContracts.Examples.MaxStore
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
+import DumbContracts.Examples.InitOnce
 import DumbContracts.Examples.SetIfGreater
 import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.SetIfBetween
diff --git a/research/lean_only_proto/DumbContracts/Examples/CompareAndSwap.lean b/research/lean_only_proto/DumbContracts/Examples/CompareAndSwap.lean
index 1f0a0baad..292757bc2 100644
--- a/research/lean_only_proto/DumbContracts/Examples/CompareAndSwap.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/CompareAndSwap.lean
@@ -15,7 +15,7 @@ def compareAndSwapFun : Fun :=
   { name := "compareAndSwap"
     args := ["slot", "expected", "value"]
     body :=
-      Stmt.let_ "current" (sloadVar "slot")
+      letSload "current" (v "slot")
         (requireEq (v "current") (v "expected") (sstoreVar "slot" (v "value")))
     ret := none }
 
@@ -32,13 +32,13 @@ theorem compareAndSwap_meets_specR_ok (s : Store) (slot expected value : Nat) :
   intro hreq
   have hmatch : s slot = expected := by exact hreq
   simp [compareAndSwapSpecR, compareAndSwapFun, requireEq, eq, require, execFun, execStmt,
-    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hmatch]
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, letSload, hmatch]
 
 theorem compareAndSwap_meets_specR_reverts (s : Store) (slot expected value : Nat) :
     (compareAndSwapSpecR slot expected value).reverts s ->
     execFun compareAndSwapFun [slot, expected, value] s [] = ExecResult.reverted := by
   intro hrev
   simp [compareAndSwapSpecR, compareAndSwapFun, requireEq, eq, require, execFun, execStmt,
-    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, letSload, hrev]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/InitOnce.lean b/research/lean_only_proto/DumbContracts/Examples/InitOnce.lean
new file mode 100644
index 000000000..b9373264d
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/InitOnce.lean
@@ -0,0 +1,44 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Initialize a slot once, reverting if it was already set. -/
+
+def initOnceFun : Fun :=
+  { name := "initOnce"
+    args := ["slot", "value"]
+    body :=
+      letSload "current" (v "slot")
+        (requireEq (v "current") (n 0) (sstoreVar "slot" (v "value")))
+    ret := none }
+
+def initOnceSpecR (slot value : Nat) : SpecR Store :=
+  { requires := fun s => s slot = 0
+    ensures := fun s s' => s' = updateStore s slot value
+    reverts := fun s => s slot != 0 }
+
+theorem initOnce_meets_specR_ok (s : Store) (slot value : Nat) :
+    (initOnceSpecR slot value).requires s ->
+    (match execFun initOnceFun [slot, value] s [] with
+      | ExecResult.ok _ s' => (initOnceSpecR slot value).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hzero : s slot = 0 := by exact hreq
+  simp [initOnceSpecR, initOnceFun, letSload, requireEq, eq, require, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hzero]
+
+theorem initOnce_meets_specR_reverts (s : Store) (slot value : Nat) :
+    (initOnceSpecR slot value).reverts s ->
+    execFun initOnceFun [slot, value] s [] = ExecResult.reverted := by
+  intro hrev
+  simp [initOnceSpecR, initOnceFun, letSload, requireEq, eq, require, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index 76e5a7987..cf7168456 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -45,6 +45,9 @@ def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
 
 /-- Shorthand for loading/storing fixed slots. -/
 
+def letSload (name : String) (slot : Expr) (body : Stmt) : Stmt :=
+  Stmt.let_ name (Expr.sload slot) body
+
 def sstoreAdd (slot delta : Expr) : Stmt :=
   Stmt.sstore slot (Expr.add (Expr.sload slot) delta)
 
diff --git a/research/lean_only_proto/test/GeneratedInitOnce.t.sol b/research/lean_only_proto/test/GeneratedInitOnce.t.sol
new file mode 100644
index 000000000..fec4ac2cc
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedInitOnce.t.sol
@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedInitOnceTest is GeneratedBase {
+    function testInitOnce() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selInitOnce = 0xd3b9b05a;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selInitOnce, 12, 777));
+        require(ok, "initOnce failed (first init)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 12));
+        require(ok, "getSlot failed (slot 12)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 777, "unexpected initOnce value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selInitOnce, 12, 888));
+        require(!ok, "initOnce should revert when slot already set");
+    }
+}

From 30c2a2cb3dc06fd6cc053afff9c524f8a3b32dce Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 03:31:29 +0000
Subject: [PATCH 10/17] Add requireAnd helper and setIfNonZeroAndLess example

---
 STATUS.md                                     |  2 +-
 docs/research-log.md                          |  5 ++
 .../DumbContracts/Compiler.lean               | 16 +++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 54 ++++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/SetIfBetween.lean  | 15 ++---
 .../Examples/SetIfNonZeroAndLess.lean         | 56 +++++++++++++++++++
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 +
 .../test/GeneratedSetIfNonZeroAndLess.t.sol   | 29 ++++++++++
 9 files changed, 172 insertions(+), 9 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/SetIfNonZeroAndLess.lean
 create mode 100644 research/lean_only_proto/test/GeneratedSetIfNonZeroAndLess.t.sol

diff --git a/STATUS.md b/STATUS.md
index 12724125b..792bf569f 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -19,7 +19,7 @@ Last updated: 2026-02-10
 - 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.
-- Iteration: add `letSload` helper and an `initOnce` example to make cached-slot guards less noisy.
+- Iteration: add `requireAnd` helper plus a `setIfNonZeroAndLess` example to reduce nested guard boilerplate.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
diff --git a/docs/research-log.md b/docs/research-log.md
index fe5efe09b..372f7db0c 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireAnd` stdlib helper to combine guard conditions cleanly.
+- Refactored `setIfBetween` to use `requireAnd` instead of nested guards.
+- Added `setIfNonZeroAndLess` example (nonzero + max guard) with SpecR + proofs.
+- Added Foundry test for `setIfNonZeroAndLess`.
+- Updated compiler entries + direct EVM asm for `setIfNonZeroAndLess`.
 - Added `letSload` stdlib helper for caching a slot read via `let_`.
 - Refactored `compareAndSwap` to use `letSload`.
 - Added `initOnce` example (only initialize a zero slot) with SpecR + proofs.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 5d21e4d51..bd406419b 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -218,9 +218,23 @@ def exampleEntry11 : EntryPoint :=
     selector := 0x5ebc58db
     returns := false }
 
+def exampleEntry13 : EntryPoint :=
+  { name := "setIfNonZeroAndLess"
+    args := ["slot", "value", "max"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.and
+          (Lang.Expr.not (Lang.Expr.eq (Lang.Expr.var "value") (Lang.Expr.lit 0)))
+          (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "max")))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfNonZeroAndLess(uint256,uint256,uint256) -> 0x8ba43d8f
+    selector := 0x8ba43d8f
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
-    exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11]
+    exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11, exampleEntry13]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 7301791ed..1660d8d17 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -63,13 +63,30 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_setIfLess"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x5ebc58db"
   , "EQ"
   , "PUSH2 tag_setIfBetween"
   , "JUMPI"
+  , "PUSH4 0x8ba43d8f"
+  , "EQ"
+  , "PUSH2 tag_setIfNonZeroAndLess"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_setIfNonZeroAndLess:"
+  , "PUSH2 ret_setIfNonZeroAndLess"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfNonZeroAndLess"
+  , "JUMP"
+  , "ret_setIfNonZeroAndLess:"
+  , "STOP"
   , "tag_setIfBetween:"
   , "PUSH2 ret_setIfBetween"
   , "PUSH1 0x64"
@@ -464,6 +481,43 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 setIfBetween_inner_check"
   , "JUMP"
+  , "fn_setIfNonZeroAndLess:"
+  , "SWAP2"
+  , "DUP2"
+  , "PUSH0"
+  , "SWAP3"
+  , "SWAP4"
+  , "DUP3"
+  , "DUP3"
+  , "LT"
+  , "DUP5"
+  , "DUP4"
+  , "EQ"
+  , "ISZERO"
+  , "AND"
+  , "PUSH2 setIfNonZeroAndLess_ok"
+  , "JUMPI"
+  , "setIfNonZeroAndLess_check:"
+  , "POP"
+  , "LT"
+  , "SWAP2"
+  , "EQ"
+  , "ISZERO"
+  , "AND"
+  , "ISZERO"
+  , "PUSH2 setIfNonZeroAndLess_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "setIfNonZeroAndLess_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "setIfNonZeroAndLess_ok:"
+  , "SSTORE"
+  , "DUP3"
+  , "PUSH0"
+  , "PUSH2 setIfNonZeroAndLess_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 a164b220d..09b655302 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -10,4 +10,5 @@ import DumbContracts.Examples.InitOnce
 import DumbContracts.Examples.SetIfGreater
 import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.SetIfBetween
+import DumbContracts.Examples.SetIfNonZeroAndLess
 import DumbContracts.Examples.BumpSlot
diff --git a/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean b/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean
index 4fc32416a..2375d5c56 100644
--- a/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean
@@ -15,9 +15,10 @@ def setIfBetweenFun : Fun :=
   { name := "setIfBetween"
     args := ["slot", "value", "min", "max"]
     body :=
-      requireGt (v "value") (v "min")
-        (requireLt (v "value") (v "max")
-          (sstoreVar "slot" (v "value")))
+      requireAnd
+        (Expr.gt (v "value") (v "min"))
+        (Expr.lt (v "value") (v "max"))
+        (sstoreVar "slot" (v "value"))
     ret := none }
 
 def setIfBetweenSpecR (slot value min max : Nat) : SpecR Store :=
@@ -32,7 +33,7 @@ theorem setIfBetween_meets_specR_ok (s : Store) (slot value min max : Nat) :
       | _ => False) := by
   intro hreq
   rcases hreq with ⟨hgt, hlt⟩
-  simp [setIfBetweenSpecR, setIfBetweenFun, requireGt, requireLt, require, sstoreVar, v, execFun,
+  simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v, execFun,
     execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hlt]
 
 theorem setIfBetween_meets_specR_reverts (s : Store) (slot value min max : Nat) :
@@ -42,16 +43,16 @@ theorem setIfBetween_meets_specR_reverts (s : Store) (slot value min max : Nat)
   rcases hrev with hle | hge
   · have hnot : ¬ value > min := by
       exact Nat.not_lt.mpr hle
-    simp [setIfBetweenSpecR, setIfBetweenFun, requireGt, requireLt, require, sstoreVar, v, execFun,
+    simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v, execFun,
       execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
   · by_cases hgt : value > min
     · have hnotlt : ¬ value < max := by
         exact Nat.not_lt.mpr hge
-      simp [setIfBetweenSpecR, setIfBetweenFun, requireGt, requireLt, require, sstoreVar, v,
+      simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v,
         execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hnotlt]
     · have hnot : ¬ value > min := by
         exact hgt
-      simp [setIfBetweenSpecR, setIfBetweenFun, requireGt, requireLt, require, sstoreVar, v,
+      simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v,
         execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/SetIfNonZeroAndLess.lean b/research/lean_only_proto/DumbContracts/Examples/SetIfNonZeroAndLess.lean
new file mode 100644
index 000000000..37ee878b6
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/SetIfNonZeroAndLess.lean
@@ -0,0 +1,56 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Store a value into a slot only if it is non-zero and below a max. -/
+
+def setIfNonZeroAndLessFun : Fun :=
+  { name := "setIfNonZeroAndLess"
+    args := ["slot", "value", "max"]
+    body :=
+      requireAnd
+        (neq (v "value") (n 0))
+        (Expr.lt (v "value") (v "max"))
+        (sstoreVar "slot" (v "value"))
+    ret := none }
+
+def setIfNonZeroAndLessSpecR (slot value max : Nat) : SpecR Store :=
+  { requires := fun _ => value != 0 ∧ value < max
+    ensures := fun s s' => s' = updateStore s slot value
+    reverts := fun _ => value = 0 ∨ value >= max }
+
+theorem setIfNonZeroAndLess_meets_specR_ok (s : Store) (slot value max : Nat) :
+    (setIfNonZeroAndLessSpecR slot value max).requires s ->
+    (match execFun setIfNonZeroAndLessFun [slot, value, max] s [] with
+      | ExecResult.ok _ s' => (setIfNonZeroAndLessSpecR slot value max).ensures s s'
+      | _ => False) := by
+  intro hreq
+  rcases hreq with ⟨hnonzero, hlt⟩
+  simp [setIfNonZeroAndLessSpecR, setIfNonZeroAndLessFun, requireAnd, require, neq, eq, sstoreVar,
+    v, n, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnonzero, hlt]
+
+theorem setIfNonZeroAndLess_meets_specR_reverts (s : Store) (slot value max : Nat) :
+    (setIfNonZeroAndLessSpecR slot value max).reverts s ->
+    execFun setIfNonZeroAndLessFun [slot, value, max] s [] = ExecResult.reverted := by
+  intro hrev
+  rcases hrev with hzero | hge
+  · simp [setIfNonZeroAndLessSpecR, setIfNonZeroAndLessFun, requireAnd, require, neq, eq, sstoreVar,
+      v, n, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hzero]
+  · by_cases hnonzero : value != 0
+    · have hnotlt : ¬ value < max := by
+        exact Nat.not_lt.mpr hge
+      simp [setIfNonZeroAndLessSpecR, setIfNonZeroAndLessFun, requireAnd, require, neq, eq, sstoreVar,
+        v, n, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnonzero, hnotlt]
+    · have hnot : ¬ value != 0 := by
+        exact hnonzero
+      simp [setIfNonZeroAndLessSpecR, setIfNonZeroAndLessFun, requireAnd, require, neq, eq, sstoreVar,
+        v, n, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index cf7168456..8f61f6079 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -16,6 +16,9 @@ def require (cond : Expr) (body : Stmt) : Stmt :=
 def unless (cond : Expr) (body : Stmt) : Stmt :=
   Stmt.if_ cond Stmt.revert body
 
+def requireAnd (lhs rhs : Expr) (body : Stmt) : Stmt :=
+  require (Expr.and lhs rhs) body
+
 def revertIf (cond : Expr) : Stmt :=
   Stmt.if_ cond Stmt.revert Stmt.skip
 
diff --git a/research/lean_only_proto/test/GeneratedSetIfNonZeroAndLess.t.sol b/research/lean_only_proto/test/GeneratedSetIfNonZeroAndLess.t.sol
new file mode 100644
index 000000000..747b5acfd
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedSetIfNonZeroAndLess.t.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedSetIfNonZeroAndLessTest is GeneratedBase {
+    function testSetIfNonZeroAndLess() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selSet = 0x8ba43d8f;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 21, 7, 10));
+        require(ok, "setIfNonZeroAndLess failed (nonzero and below max)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 21));
+        require(ok, "getSlot failed (slot 21)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 7, "unexpected setIfNonZeroAndLess value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSet, 22, 0, 10));
+        require(!ok, "setIfNonZeroAndLess should revert when value == 0");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSet, 23, 10, 10));
+        require(!ok, "setIfNonZeroAndLess should revert when value >= max");
+    }
+}

From 9c078a7cf5874382e7f6e953e0ed1c29fb048c78 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 03:57:44 +0000
Subject: [PATCH 11/17] Add sstoreInc helper and bumpIfNonZero example

---
 STATUS.md                                     |  2 +-
 docs/research-log.md                          |  5 +++
 .../DumbContracts/Compiler.lean               | 18 +++++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 41 ++++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/BumpIfNonZero.lean | 42 +++++++++++++++++++
 .../DumbContracts/Examples/BumpSlot.lean      |  4 +-
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedBumpIfNonZero.t.sol         | 36 ++++++++++++++++
 9 files changed, 148 insertions(+), 4 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/BumpIfNonZero.lean
 create mode 100644 research/lean_only_proto/test/GeneratedBumpIfNonZero.t.sol

diff --git a/STATUS.md b/STATUS.md
index 792bf569f..fa56ed026 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -19,7 +19,7 @@ Last updated: 2026-02-10
 - 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.
-- Iteration: add `requireAnd` helper plus a `setIfNonZeroAndLess` example to reduce nested guard boilerplate.
+- Iteration: add `sstoreInc` helper plus a `bumpIfNonZero` example to reduce increment boilerplate with guards.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
diff --git a/docs/research-log.md b/docs/research-log.md
index 372f7db0c..637046770 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `sstoreInc` stdlib helper to increment a slot without repeating `add` boilerplate.
+- Refactored `bumpSlot` to use `sstoreInc`.
+- Added `bumpIfNonZero` example (guarded increment when slot is nonzero) with SpecR + proofs.
+- Added Foundry test for `bumpIfNonZero`.
+- Updated compiler entries + direct EVM asm for `bumpIfNonZero`.
 - Added `requireAnd` stdlib helper to combine guard conditions cleanly.
 - Refactored `setIfBetween` to use `requireAnd` instead of nested guards.
 - Added `setIfNonZeroAndLess` example (nonzero + max guard) with SpecR + proofs.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index bd406419b..24ef83b57 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -232,9 +232,25 @@ def exampleEntry13 : EntryPoint :=
     selector := 0x8ba43d8f
     returns := false }
 
+def exampleEntry14 : EntryPoint :=
+  { name := "bumpIfNonZero"
+    args := ["slot"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.not
+          (Lang.Expr.eq (Lang.Expr.sload (Lang.Expr.var "slot")) (Lang.Expr.lit 0)))
+        (Lang.Stmt.sstore
+          (Lang.Expr.var "slot")
+          (Lang.Expr.add (Lang.Expr.sload (Lang.Expr.var "slot")) (Lang.Expr.lit 1)))
+        Lang.Stmt.revert
+    -- bumpIfNonZero(uint256) -> 0xc2311456
+    selector := 0xc2311456
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
-    exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11, exampleEntry13]
+    exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11, exampleEntry13,
+    exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 1660d8d17..1e2e70d9f 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -68,13 +68,26 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_setIfBetween"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x8ba43d8f"
   , "EQ"
   , "PUSH2 tag_setIfNonZeroAndLess"
   , "JUMPI"
+  , "PUSH4 0xc2311456"
+  , "EQ"
+  , "PUSH2 tag_bumpIfNonZero"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_bumpIfNonZero:"
+  , "PUSH2 ret_bumpIfNonZero"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_bumpIfNonZero"
+  , "JUMP"
+  , "ret_bumpIfNonZero:"
+  , "STOP"
   , "tag_setIfNonZeroAndLess:"
   , "PUSH2 ret_setIfNonZeroAndLess"
   , "PUSH1 0x44"
@@ -518,6 +531,34 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 setIfNonZeroAndLess_check"
   , "JUMP"
+  , "fn_bumpIfNonZero:"
+  , "PUSH0"
+  , "SWAP1"
+  , "DUP2"
+  , "DUP2"
+  , "SLOAD"
+  , "SUB"
+  , "PUSH2 bumpIfNonZero_ok"
+  , "JUMPI"
+  , "bumpIfNonZero_check:"
+  , "SLOAD"
+  , "EQ"
+  , "PUSH2 bumpIfNonZero_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "bumpIfNonZero_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "bumpIfNonZero_ok:"
+  , "PUSH1 0x01"
+  , "DUP2"
+  , "SLOAD"
+  , "ADD"
+  , "DUP2"
+  , "SSTORE"
+  , "PUSH2 bumpIfNonZero_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 09b655302..8660f8ae6 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -12,3 +12,4 @@ import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.SetIfBetween
 import DumbContracts.Examples.SetIfNonZeroAndLess
 import DumbContracts.Examples.BumpSlot
+import DumbContracts.Examples.BumpIfNonZero
diff --git a/research/lean_only_proto/DumbContracts/Examples/BumpIfNonZero.lean b/research/lean_only_proto/DumbContracts/Examples/BumpIfNonZero.lean
new file mode 100644
index 000000000..0fc2fe735
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/BumpIfNonZero.lean
@@ -0,0 +1,42 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Increment a slot by one, but only if it is already non-zero. -/
+
+def bumpIfNonZeroFun : Fun :=
+  { name := "bumpIfNonZero"
+    args := ["slot"]
+    body := requireNonZero (Expr.sload (v "slot")) (sstoreInc (v "slot"))
+    ret := none }
+
+def bumpIfNonZeroSpecR (slot : Nat) : SpecR Store :=
+  { requires := fun s => s slot != 0
+    ensures := fun s s' => s' = updateStore s slot (s slot + 1)
+    reverts := fun s => s slot = 0 }
+
+theorem bumpIfNonZero_meets_specR_ok (s : Store) (slot : Nat) :
+    (bumpIfNonZeroSpecR slot).requires s ->
+    (match execFun bumpIfNonZeroFun [slot] s [] with
+      | ExecResult.ok _ s' => (bumpIfNonZeroSpecR slot).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hnonzero : s slot != 0 := by exact hreq
+  simp [bumpIfNonZeroSpecR, bumpIfNonZeroFun, requireNonZero, requireNeq, neq, eq, require, sstoreInc,
+    sstoreAdd, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, v, n, hnonzero]
+
+theorem bumpIfNonZero_meets_specR_reverts (s : Store) (slot : Nat) :
+    (bumpIfNonZeroSpecR slot).reverts s ->
+    execFun bumpIfNonZeroFun [slot] s [] = ExecResult.reverted := by
+  intro hrev
+  simp [bumpIfNonZeroSpecR, bumpIfNonZeroFun, requireNonZero, requireNeq, neq, eq, require, sstoreInc,
+    sstoreAdd, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, v, n, hrev]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/BumpSlot.lean b/research/lean_only_proto/DumbContracts/Examples/BumpSlot.lean
index 959d24c0f..1f1cb4f2b 100644
--- a/research/lean_only_proto/DumbContracts/Examples/BumpSlot.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/BumpSlot.lean
@@ -14,7 +14,7 @@ open DumbContracts.Std
 def bumpSlotFun : Fun :=
   { name := "bumpSlot"
     args := ["slot"]
-    body := sstoreAdd (v "slot") (n 1)
+    body := sstoreInc (v "slot")
     ret := none }
 
 def bumpSlotSpec (slot : Nat) : Spec Store :=
@@ -27,7 +27,7 @@ theorem bumpSlot_meets_spec (s : Store) (slot : Nat) :
       | ExecResult.ok _ s' => (bumpSlotSpec slot).ensures s s'
       | _ => False) := by
   intro _hreq
-  simp [bumpSlotSpec, bumpSlotFun, sstoreAdd, execFun, execStmt, evalExpr,
+  simp [bumpSlotSpec, bumpSlotFun, sstoreInc, sstoreAdd, execFun, execStmt, evalExpr,
     bindArgs, emptyEnv, updateEnv, updateStore, v, n]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index 8f61f6079..f3e31ab63 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -54,6 +54,9 @@ def letSload (name : String) (slot : Expr) (body : Stmt) : Stmt :=
 def sstoreAdd (slot delta : Expr) : Stmt :=
   Stmt.sstore slot (Expr.add (Expr.sload slot) delta)
 
+def sstoreInc (slot : Expr) : Stmt :=
+  sstoreAdd slot (Expr.lit 1)
+
 def sloadSlot (slot : Nat) : Expr :=
   Expr.sload (Expr.lit slot)
 
diff --git a/research/lean_only_proto/test/GeneratedBumpIfNonZero.t.sol b/research/lean_only_proto/test/GeneratedBumpIfNonZero.t.sol
new file mode 100644
index 000000000..9c5b8d987
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedBumpIfNonZero.t.sol
@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedBumpIfNonZeroTest is GeneratedBase {
+    function testBumpIfNonZero() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selBumpIfNonZero = 0xc2311456;
+        bytes4 selSet = 0xf2c298be;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 3, 9));
+        require(ok, "setSlot failed (slot 3)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selBumpIfNonZero, 3));
+        require(ok, "bumpIfNonZero failed");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 3));
+        require(ok, "getSlot failed (slot 3)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 10, "unexpected bumpIfNonZero value");
+    }
+
+    function testBumpIfNonZeroRevertsOnZero() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selBumpIfNonZero = 0xc2311456;
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selBumpIfNonZero, 11));
+        require(!ok, "expected bumpIfNonZero revert on zero slot");
+    }
+}

From d1730da4d3363ce9bdca8f8dc1d5ada0e2e79994 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 04:28:47 +0000
Subject: [PATCH 12/17] Add sstoreMax helper and updateMax example

---
 STATUS.md                                     |  2 +-
 docs/research-log.md                          |  5 +++
 .../DumbContracts/Compiler.lean               | 19 ++++++--
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 45 +++++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/MaxStore.lean      | 14 +++---
 .../DumbContracts/Examples/UpdateMax.lean     | 38 ++++++++++++++++
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedUpdateMax.t.sol             | 35 +++++++++++++++
 9 files changed, 149 insertions(+), 13 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/UpdateMax.lean
 create mode 100644 research/lean_only_proto/test/GeneratedUpdateMax.t.sol

diff --git a/STATUS.md b/STATUS.md
index fa56ed026..518b41c8c 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -19,7 +19,6 @@ Last updated: 2026-02-10
 - 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.
-- Iteration: add `sstoreInc` helper plus a `bumpIfNonZero` example to reduce increment boilerplate with guards.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
@@ -49,6 +48,7 @@ Last updated: 2026-02-10
 - Added `requireEq`/`requireNeq` helpers plus a `compareAndSwap` example + Foundry test.
 - Added `requireGt` helper plus a `setIfGreater` example + Foundry test (and refactored guarded add to use it).
 - Added `sstoreAdd` helper plus a `bumpSlot` example + Foundry test (and refactored add-slot examples to use it).
+- Added `sstoreMax` helper plus an `updateMax` example + Foundry test (monotonic max update).
 - Added a `revertIf` helper, refactored `checkHealth`, and added a `setIfLess` example + Foundry test.
 - Updated compiler entries + direct EVM asm for `setIfLess`.
 - Minimal docs frontend and compressed docs.
diff --git a/docs/research-log.md b/docs/research-log.md
index 637046770..df2846cc1 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `sstoreMax` stdlib helper to reduce max-store boilerplate.
+- Refactored `maxStore` to use `sstoreMax`.
+- Added `updateMax` example (monotonic max update against a stored slot) with Spec + proof.
+- Added Foundry test for `updateMax`.
+- Updated compiler entries + direct EVM asm for `updateMax`.
 - Added `sstoreInc` stdlib helper to increment a slot without repeating `add` boilerplate.
 - Refactored `bumpSlot` to use `sstoreInc`.
 - Added `bumpIfNonZero` example (guarded increment when slot is nonzero) with SpecR + proofs.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 24ef83b57..d64609d5b 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -131,6 +131,19 @@ def exampleEntry5 : EntryPoint :=
     selector := 0xb61d4088
     returns := false }
 
+def exampleEntry15 : EntryPoint :=
+  { name := "updateMax"
+    args := ["slot", "value"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.gt (Lang.Expr.var "current") (Lang.Expr.var "value"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "current"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value")))
+    -- updateMax(uint256,uint256) -> 0xe9cc4edd
+    selector := 0xe9cc4edd
+    returns := false }
+
 def exampleEntry6 : EntryPoint :=
   { name := "setNonZero"
     args := ["slot", "value"]
@@ -248,9 +261,9 @@ def exampleEntry14 : EntryPoint :=
     returns := false }
 
 def exampleEntries : List EntryPoint :=
-  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
-    exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11, exampleEntry13,
-    exampleEntry14]
+  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
+    exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10,
+    exampleEntry11, exampleEntry13, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 1e2e70d9f..15ec71131 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -34,6 +34,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_maxStore"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0xe9cc4edd"
+  , "EQ"
+  , "PUSH2 tag_updateMax"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xac1f1f67"
   , "EQ"
   , "PUSH2 tag_setNonZero"
@@ -178,6 +183,16 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setNonZero:"
   , "STOP"
+  , "tag_updateMax:"
+  , "PUSH2 ret_updateMax"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_updateMax"
+  , "JUMP"
+  , "ret_updateMax:"
+  , "STOP"
   , "tag_maxStore:"
   , "PUSH2 ret_maxStore"
   , "PUSH1 0x44"
@@ -300,6 +315,36 @@ def directProgramAsm : List String :=
   , "SSTORE"
   , "PUSH2 maxStore_check"
   , "JUMP"
+  , "fn_updateMax:"
+  , "DUP2"
+  , "DUP2"
+  , "SLOAD"
+  , "DUP2"
+  , "DUP2"
+  , "GT"
+  , "PUSH2 updateMax_then"
+  , "JUMPI"
+  , "updateMax_check:"
+  , "GT"
+  , "ISZERO"
+  , "PUSH2 updateMax_else"
+  , "JUMPI"
+  , "updateMax_join:"
+  , "POP"
+  , "POP"
+  , "JUMP"
+  , "updateMax_else:"
+  , "SSTORE"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH2 updateMax_join"
+  , "JUMP"
+  , "updateMax_then:"
+  , "DUP1"
+  , "DUP4"
+  , "SSTORE"
+  , "PUSH2 updateMax_check"
+  , "JUMP"
   , "fn_setNonZero:"
   , "SWAP1"
   , "DUP1"
diff --git a/research/lean_only_proto/DumbContracts/Examples.lean b/research/lean_only_proto/DumbContracts/Examples.lean
index 8660f8ae6..f87bf1d11 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -4,6 +4,7 @@ import DumbContracts.Examples.TokenBase
 import DumbContracts.Examples.Supply
 import DumbContracts.Examples.TokenTransfer
 import DumbContracts.Examples.MaxStore
+import DumbContracts.Examples.UpdateMax
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.InitOnce
diff --git a/research/lean_only_proto/DumbContracts/Examples/MaxStore.lean b/research/lean_only_proto/DumbContracts/Examples/MaxStore.lean
index fea620228..7fafe3f3f 100644
--- a/research/lean_only_proto/DumbContracts/Examples/MaxStore.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/MaxStore.lean
@@ -14,11 +14,7 @@ open DumbContracts.Std
 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"))
+    body := sstoreMax (v "slot") (v "a") (v "b")
     ret := none }
 
 def maxStoreSpec (slot a b : Nat) : Spec Store :=
@@ -32,9 +28,9 @@ theorem maxStore_meets_spec (s : Store) (slot a b : Nat) :
       | _ => 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]
+  · simp [maxStoreFun, maxStoreSpec, sstoreMax, sstoreVar, v, execFun, execStmt, evalExpr, bindArgs,
+      emptyEnv, updateEnv, updateStore, h]
+  · simp [maxStoreFun, maxStoreSpec, sstoreMax, sstoreVar, v, execFun, execStmt, evalExpr, bindArgs,
+      emptyEnv, updateEnv, updateStore, h]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/UpdateMax.lean b/research/lean_only_proto/DumbContracts/Examples/UpdateMax.lean
new file mode 100644
index 000000000..ab451291c
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/UpdateMax.lean
@@ -0,0 +1,38 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Update a slot to the max of its current value and a new input. -/
+
+def updateMaxFun : Fun :=
+  { name := "updateMax"
+    args := ["slot", "value"]
+    body :=
+      letSload "current" (v "slot")
+        (sstoreMax (v "slot") (v "current") (v "value"))
+    ret := none }
+
+def updateMaxSpec (slot value : Nat) : Spec Store :=
+  { requires := fun _ => True
+    ensures := fun s s' => s' = updateStore s slot (if s slot > value then s slot else value) }
+
+theorem updateMax_meets_spec (s : Store) (slot value : Nat) :
+    (updateMaxSpec slot value).requires s ->
+    (match execFun updateMaxFun [slot, value] s [] with
+      | ExecResult.ok _ s' => (updateMaxSpec slot value).ensures s s'
+      | _ => False) := by
+  intro _hreq
+  by_cases h : s slot > value
+  · simp [updateMaxFun, updateMaxSpec, letSload, sstoreMax, v, execFun, execStmt, evalExpr,
+      bindArgs, emptyEnv, updateEnv, updateStore, h]
+  · simp [updateMaxFun, updateMaxSpec, letSload, sstoreMax, v, execFun, execStmt, evalExpr,
+      bindArgs, emptyEnv, updateEnv, updateStore, h]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index f3e31ab63..1e739c814 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -57,6 +57,9 @@ def sstoreAdd (slot delta : Expr) : Stmt :=
 def sstoreInc (slot : Expr) : Stmt :=
   sstoreAdd slot (Expr.lit 1)
 
+def sstoreMax (slot a b : Expr) : Stmt :=
+  Stmt.if_ (Expr.gt a b) (Stmt.sstore slot a) (Stmt.sstore slot b)
+
 def sloadSlot (slot : Nat) : Expr :=
   Expr.sload (Expr.lit slot)
 
diff --git a/research/lean_only_proto/test/GeneratedUpdateMax.t.sol b/research/lean_only_proto/test/GeneratedUpdateMax.t.sol
new file mode 100644
index 000000000..7f682d83f
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedUpdateMax.t.sol
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedUpdateMaxTest is GeneratedBase {
+    function testUpdateMax() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selUpdateMax = 0xe9cc4edd;
+        bytes4 selSet = 0xf2c298be;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 4, 10));
+        require(ok, "setSlot failed (slot 4)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selUpdateMax, 4, 7));
+        require(ok, "updateMax failed on smaller value");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 4));
+        require(ok, "getSlot failed (slot 4)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 10, "unexpected updateMax value after smaller input");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selUpdateMax, 4, 12));
+        require(ok, "updateMax failed on larger value");
+
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 4));
+        require(ok, "getSlot failed (slot 4) after update");
+        val = abi.decode(data, (uint256));
+        require(val == 12, "unexpected updateMax value after larger input");
+    }
+}

From 09ea02debdfec5faa7ce04e5dad154efdb825e66 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 04:57:13 +0000
Subject: [PATCH 13/17] Add sstoreMin helper and updateMin example

---
 STATUS.md                                     |  1 +
 docs/research-log.md                          |  4 ++
 .../DumbContracts/Compiler.lean               | 17 ++++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 45 +++++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/UpdateMin.lean     | 38 ++++++++++++++++
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedUpdateMin.t.sol             | 35 +++++++++++++++
 8 files changed, 142 insertions(+), 2 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/UpdateMin.lean
 create mode 100644 research/lean_only_proto/test/GeneratedUpdateMin.t.sol

diff --git a/STATUS.md b/STATUS.md
index 518b41c8c..660dbe6d2 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -19,6 +19,7 @@ Last updated: 2026-02-10
 - 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.
+- Iteration: add a minimal `sstoreMin` helper and a tiny `updateMin` example + Foundry test.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
diff --git a/docs/research-log.md b/docs/research-log.md
index df2846cc1..344069181 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,10 @@
 # Research Log
 
 ## 2026-02-10
+- Added `sstoreMin` stdlib helper to mirror `sstoreMax` for min updates.
+- Added `updateMin` example (monotonic min update against a stored slot) with Spec + proof.
+- Added Foundry test for `updateMin`.
+- Updated compiler entries + direct EVM asm for `updateMin`.
 - Added `sstoreMax` stdlib helper to reduce max-store boilerplate.
 - Refactored `maxStore` to use `sstoreMax`.
 - Added `updateMax` example (monotonic max update against a stored slot) with Spec + proof.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index d64609d5b..02c54c92b 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -144,6 +144,19 @@ def exampleEntry15 : EntryPoint :=
     selector := 0xe9cc4edd
     returns := false }
 
+def exampleEntry16 : EntryPoint :=
+  { name := "updateMin"
+    args := ["slot", "value"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.lt (Lang.Expr.var "current") (Lang.Expr.var "value"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "current"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value")))
+    -- updateMin(uint256,uint256) -> 0x5c34a245
+    selector := 0x5c34a245
+    returns := false }
+
 def exampleEntry6 : EntryPoint :=
   { name := "setNonZero"
     args := ["slot", "value"]
@@ -262,8 +275,8 @@ def exampleEntry14 : EntryPoint :=
 
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
-    exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10,
-    exampleEntry11, exampleEntry13, exampleEntry14]
+    exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9,
+    exampleEntry10, exampleEntry11, exampleEntry13, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 15ec71131..a78047150 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -39,6 +39,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_updateMax"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0x5c34a245"
+  , "EQ"
+  , "PUSH2 tag_updateMin"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xac1f1f67"
   , "EQ"
   , "PUSH2 tag_setNonZero"
@@ -183,6 +188,16 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setNonZero:"
   , "STOP"
+  , "tag_updateMin:"
+  , "PUSH2 ret_updateMin"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_updateMin"
+  , "JUMP"
+  , "ret_updateMin:"
+  , "STOP"
   , "tag_updateMax:"
   , "PUSH2 ret_updateMax"
   , "PUSH1 0x24"
@@ -345,6 +360,36 @@ def directProgramAsm : List String :=
   , "SSTORE"
   , "PUSH2 updateMax_check"
   , "JUMP"
+  , "fn_updateMin:"
+  , "DUP2"
+  , "DUP2"
+  , "SLOAD"
+  , "DUP2"
+  , "DUP2"
+  , "LT"
+  , "PUSH2 updateMin_then"
+  , "JUMPI"
+  , "updateMin_check:"
+  , "LT"
+  , "ISZERO"
+  , "PUSH2 updateMin_else"
+  , "JUMPI"
+  , "updateMin_join:"
+  , "POP"
+  , "POP"
+  , "JUMP"
+  , "updateMin_else:"
+  , "SSTORE"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH2 updateMin_join"
+  , "JUMP"
+  , "updateMin_then:"
+  , "DUP1"
+  , "DUP4"
+  , "SSTORE"
+  , "PUSH2 updateMin_check"
+  , "JUMP"
   , "fn_setNonZero:"
   , "SWAP1"
   , "DUP1"
diff --git a/research/lean_only_proto/DumbContracts/Examples.lean b/research/lean_only_proto/DumbContracts/Examples.lean
index f87bf1d11..d5cd0a9aa 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -5,6 +5,7 @@ import DumbContracts.Examples.Supply
 import DumbContracts.Examples.TokenTransfer
 import DumbContracts.Examples.MaxStore
 import DumbContracts.Examples.UpdateMax
+import DumbContracts.Examples.UpdateMin
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.InitOnce
diff --git a/research/lean_only_proto/DumbContracts/Examples/UpdateMin.lean b/research/lean_only_proto/DumbContracts/Examples/UpdateMin.lean
new file mode 100644
index 000000000..cea7b1bdf
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/UpdateMin.lean
@@ -0,0 +1,38 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Update a slot to the min of its current value and a new input. -/
+
+def updateMinFun : Fun :=
+  { name := "updateMin"
+    args := ["slot", "value"]
+    body :=
+      letSload "current" (v "slot")
+        (sstoreMin (v "slot") (v "current") (v "value"))
+    ret := none }
+
+def updateMinSpec (slot value : Nat) : Spec Store :=
+  { requires := fun _ => True
+    ensures := fun s s' => s' = updateStore s slot (if s slot < value then s slot else value) }
+
+theorem updateMin_meets_spec (s : Store) (slot value : Nat) :
+    (updateMinSpec slot value).requires s ->
+    (match execFun updateMinFun [slot, value] s [] with
+      | ExecResult.ok _ s' => (updateMinSpec slot value).ensures s s'
+      | _ => False) := by
+  intro _hreq
+  by_cases h : s slot < value
+  · simp [updateMinFun, updateMinSpec, letSload, sstoreMin, v, execFun, execStmt, evalExpr,
+      bindArgs, emptyEnv, updateEnv, updateStore, h]
+  · simp [updateMinFun, updateMinSpec, letSload, sstoreMin, v, execFun, execStmt, evalExpr,
+      bindArgs, emptyEnv, updateEnv, updateStore, h]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index 1e739c814..f6b07b663 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -60,6 +60,9 @@ def sstoreInc (slot : Expr) : Stmt :=
 def sstoreMax (slot a b : Expr) : Stmt :=
   Stmt.if_ (Expr.gt a b) (Stmt.sstore slot a) (Stmt.sstore slot b)
 
+def sstoreMin (slot a b : Expr) : Stmt :=
+  Stmt.if_ (Expr.lt a b) (Stmt.sstore slot a) (Stmt.sstore slot b)
+
 def sloadSlot (slot : Nat) : Expr :=
   Expr.sload (Expr.lit slot)
 
diff --git a/research/lean_only_proto/test/GeneratedUpdateMin.t.sol b/research/lean_only_proto/test/GeneratedUpdateMin.t.sol
new file mode 100644
index 000000000..f7cb8e3d9
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedUpdateMin.t.sol
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedUpdateMinTest is GeneratedBase {
+    function testUpdateMin() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selUpdateMin = 0x5c34a245;
+        bytes4 selSet = 0xf2c298be;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 4, 10));
+        require(ok, "setSlot failed (slot 4)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selUpdateMin, 4, 12));
+        require(ok, "updateMin failed on larger value");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 4));
+        require(ok, "getSlot failed (slot 4)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 10, "unexpected updateMin value after larger input");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selUpdateMin, 4, 7));
+        require(ok, "updateMin failed on smaller value");
+
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 4));
+        require(ok, "getSlot failed (slot 4) after update");
+        val = abi.decode(data, (uint256));
+        require(val == 7, "unexpected updateMin value after smaller input");
+    }
+}

From 61e2376cad7c7b36ad893e715e1eceaed674fdc3 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 05:29:16 +0000
Subject: [PATCH 14/17] Add requireBetween helper and addIfBetween example

---
 STATUS.md                                     |  2 +-
 docs/research-log.md                          |  5 ++
 .../DumbContracts/Compiler.lean               | 19 ++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 72 +++++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/AddIfBetween.lean  | 59 +++++++++++++++
 .../DumbContracts/Examples/SetIfBetween.lean  | 15 ++--
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 +
 .../test/GeneratedAddIfBetween.t.sol          | 33 +++++++++
 9 files changed, 200 insertions(+), 9 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/AddIfBetween.lean
 create mode 100644 research/lean_only_proto/test/GeneratedAddIfBetween.t.sol

diff --git a/STATUS.md b/STATUS.md
index 660dbe6d2..b9f9645c5 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -19,7 +19,7 @@ Last updated: 2026-02-10
 - 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.
-- Iteration: add a minimal `sstoreMin` helper and a tiny `updateMin` example + Foundry test.
+- Iteration: add a minimal `requireBetween` helper and a tiny `addIfBetween` example + Foundry test.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
diff --git a/docs/research-log.md b/docs/research-log.md
index 344069181..ecd3b5e73 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireBetween` stdlib helper for strict range guards.
+- Refactored `setIfBetween` to use `requireBetween`.
+- Added `addIfBetween` example (guarded add on `min < delta < max`) with SpecR + proofs.
+- Added Foundry test for `addIfBetween`.
+- Updated compiler entries + direct EVM asm for `addIfBetween`.
 - Added `sstoreMin` stdlib helper to mirror `sstoreMax` for min updates.
 - Added `updateMin` example (monotonic min update against a stored slot) with Spec + proof.
 - Added Foundry test for `updateMin`.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 02c54c92b..11f64cc81 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -244,6 +244,23 @@ def exampleEntry11 : EntryPoint :=
     selector := 0x5ebc58db
     returns := false }
 
+def exampleEntry17 : EntryPoint :=
+  { name := "addIfBetween"
+    args := ["slot", "delta", "min", "max"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.gt (Lang.Expr.var "delta") (Lang.Expr.var "min"))
+        (Lang.Stmt.if_
+          (Lang.Expr.lt (Lang.Expr.var "delta") (Lang.Expr.var "max"))
+          (Lang.Stmt.sstore
+            (Lang.Expr.var "slot")
+            (Lang.Expr.add (Lang.Expr.sload (Lang.Expr.var "slot")) (Lang.Expr.var "delta")))
+          Lang.Stmt.revert)
+        Lang.Stmt.revert
+    -- addIfBetween(uint256,uint256,uint256,uint256) -> 0xbc0fcb79
+    selector := 0xbc0fcb79
+    returns := false }
+
 def exampleEntry13 : EntryPoint :=
   { name := "setIfNonZeroAndLess"
     args := ["slot", "value", "max"]
@@ -276,7 +293,7 @@ def exampleEntry14 : EntryPoint :=
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
     exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9,
-    exampleEntry10, exampleEntry11, exampleEntry13, exampleEntry14]
+    exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry13, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index a78047150..6d6c4d54b 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -79,6 +79,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_setIfBetween"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0xbc0fcb79"
+  , "EQ"
+  , "PUSH2 tag_addIfBetween"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x8ba43d8f"
   , "EQ"
   , "PUSH2 tag_setIfNonZeroAndLess"
@@ -110,6 +115,20 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setIfNonZeroAndLess:"
   , "STOP"
+  , "tag_addIfBetween:"
+  , "PUSH2 ret_addIfBetween"
+  , "PUSH1 0x64"
+  , "CALLDATALOAD"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_addIfBetween"
+  , "JUMP"
+  , "ret_addIfBetween:"
+  , "STOP"
   , "tag_setIfBetween:"
   , "PUSH2 ret_setIfBetween"
   , "PUSH1 0x64"
@@ -584,6 +603,59 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 setIfBetween_inner_check"
   , "JUMP"
+  , "fn_addIfBetween:"
+  , "SWAP3"
+  , "SWAP1"
+  , "SWAP2"
+  , "SWAP3"
+  , "DUP4"
+  , "DUP4"
+  , "GT"
+  , "PUSH2 addIfBetween_outer_ok"
+  , "JUMPI"
+  , "addIfBetween_outer_check:"
+  , "POP"
+  , "POP"
+  , "GT"
+  , "ISZERO"
+  , "PUSH2 addIfBetween_revert_outer"
+  , "JUMPI"
+  , "JUMP"
+  , "addIfBetween_revert_outer:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "addIfBetween_outer_ok:"
+  , "DUP2"
+  , "DUP4"
+  , "LT"
+  , "PUSH2 addIfBetween_inner_ok"
+  , "JUMPI"
+  , "addIfBetween_inner_check:"
+  , "POP"
+  , "DUP2"
+  , "LT"
+  , "ISZERO"
+  , "PUSH2 addIfBetween_revert_inner"
+  , "JUMPI"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH2 addIfBetween_outer_check"
+  , "JUMP"
+  , "addIfBetween_revert_inner:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "addIfBetween_inner_ok:"
+  , "DUP3"
+  , "DUP2"
+  , "SLOAD"
+  , "ADD"
+  , "SWAP1"
+  , "SSTORE"
+  , "PUSH0"
+  , "PUSH2 addIfBetween_inner_check"
+  , "JUMP"
   , "fn_setIfNonZeroAndLess:"
   , "SWAP2"
   , "DUP2"
diff --git a/research/lean_only_proto/DumbContracts/Examples.lean b/research/lean_only_proto/DumbContracts/Examples.lean
index d5cd0a9aa..de350b4fa 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -12,6 +12,7 @@ import DumbContracts.Examples.InitOnce
 import DumbContracts.Examples.SetIfGreater
 import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.SetIfBetween
+import DumbContracts.Examples.AddIfBetween
 import DumbContracts.Examples.SetIfNonZeroAndLess
 import DumbContracts.Examples.BumpSlot
 import DumbContracts.Examples.BumpIfNonZero
diff --git a/research/lean_only_proto/DumbContracts/Examples/AddIfBetween.lean b/research/lean_only_proto/DumbContracts/Examples/AddIfBetween.lean
new file mode 100644
index 000000000..f5220da3a
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/AddIfBetween.lean
@@ -0,0 +1,59 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Add a delta to a slot only if it is strictly between min and max. -/
+
+def addIfBetweenFun : Fun :=
+  { name := "addIfBetween"
+    args := ["slot", "delta", "min", "max"]
+    body :=
+      requireBetween
+        (v "delta")
+        (v "min")
+        (v "max")
+        (sstoreAdd (v "slot") (v "delta"))
+    ret := none }
+
+def addIfBetweenSpecR (slot delta min max : Nat) : SpecR Store :=
+  { requires := fun _ => delta > min ∧ delta < max
+    ensures := fun s s' => s' = updateStore s slot (s slot + delta)
+    reverts := fun _ => delta <= min ∨ delta >= max }
+
+theorem addIfBetween_meets_specR_ok (s : Store) (slot delta min max : Nat) :
+    (addIfBetweenSpecR slot delta min max).requires s ->
+    (match execFun addIfBetweenFun [slot, delta, min, max] s [] with
+      | ExecResult.ok _ s' => (addIfBetweenSpecR slot delta min max).ensures s s'
+      | _ => False) := by
+  intro hreq
+  rcases hreq with ⟨hgt, hlt⟩
+  simp [addIfBetweenSpecR, addIfBetweenFun, requireBetween, requireAnd, require, sstoreAdd, v, execFun,
+    execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hlt]
+
+theorem addIfBetween_meets_specR_reverts (s : Store) (slot delta min max : Nat) :
+    (addIfBetweenSpecR slot delta min max).reverts s ->
+    execFun addIfBetweenFun [slot, delta, min, max] s [] = ExecResult.reverted := by
+  intro hrev
+  rcases hrev with hle | hge
+  · have hnot : ¬ delta > min := by
+      exact Nat.not_lt.mpr hle
+    simp [addIfBetweenSpecR, addIfBetweenFun, requireBetween, requireAnd, require, sstoreAdd, v, execFun,
+      execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+  · by_cases hgt : delta > min
+    · have hnotlt : ¬ delta < max := by
+        exact Nat.not_lt.mpr hge
+      simp [addIfBetweenSpecR, addIfBetweenFun, requireBetween, requireAnd, require, sstoreAdd, v,
+        execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hnotlt]
+    · have hnot : ¬ delta > min := by
+        exact hgt
+      simp [addIfBetweenSpecR, addIfBetweenFun, requireBetween, requireAnd, require, sstoreAdd, v,
+        execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean b/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean
index 2375d5c56..abdf5bde2 100644
--- a/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean
@@ -15,9 +15,10 @@ def setIfBetweenFun : Fun :=
   { name := "setIfBetween"
     args := ["slot", "value", "min", "max"]
     body :=
-      requireAnd
-        (Expr.gt (v "value") (v "min"))
-        (Expr.lt (v "value") (v "max"))
+      requireBetween
+        (v "value")
+        (v "min")
+        (v "max")
         (sstoreVar "slot" (v "value"))
     ret := none }
 
@@ -33,7 +34,7 @@ theorem setIfBetween_meets_specR_ok (s : Store) (slot value min max : Nat) :
       | _ => False) := by
   intro hreq
   rcases hreq with ⟨hgt, hlt⟩
-  simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v, execFun,
+  simp [setIfBetweenSpecR, setIfBetweenFun, requireBetween, requireAnd, require, sstoreVar, v, execFun,
     execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hlt]
 
 theorem setIfBetween_meets_specR_reverts (s : Store) (slot value min max : Nat) :
@@ -43,16 +44,16 @@ theorem setIfBetween_meets_specR_reverts (s : Store) (slot value min max : Nat)
   rcases hrev with hle | hge
   · have hnot : ¬ value > min := by
       exact Nat.not_lt.mpr hle
-    simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v, execFun,
+    simp [setIfBetweenSpecR, setIfBetweenFun, requireBetween, requireAnd, require, sstoreVar, v, execFun,
       execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
   · by_cases hgt : value > min
     · have hnotlt : ¬ value < max := by
         exact Nat.not_lt.mpr hge
-      simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v,
+      simp [setIfBetweenSpecR, setIfBetweenFun, requireBetween, requireAnd, require, sstoreVar, v,
         execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hnotlt]
     · have hnot : ¬ value > min := by
         exact hgt
-      simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v,
+      simp [setIfBetweenSpecR, setIfBetweenFun, requireBetween, requireAnd, require, sstoreVar, v,
         execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index f6b07b663..e01a9f984 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -43,6 +43,9 @@ def requireGt (lhs rhs : Expr) (body : Stmt) : Stmt :=
 def requireLt (lhs rhs : Expr) (body : Stmt) : Stmt :=
   require (Expr.lt lhs rhs) body
 
+def requireBetween (value lo hi : Expr) (body : Stmt) : Stmt :=
+  requireAnd (Expr.gt value lo) (Expr.lt value hi) body
+
 def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
   requireNeq value (Expr.lit 0) body
 
diff --git a/research/lean_only_proto/test/GeneratedAddIfBetween.t.sol b/research/lean_only_proto/test/GeneratedAddIfBetween.t.sol
new file mode 100644
index 000000000..0ef012019
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedAddIfBetween.t.sol
@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedAddIfBetweenTest is GeneratedBase {
+    function testAddIfBetween() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selAdd = 0xbc0fcb79;
+        bytes4 selSet = 0xf2c298be;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 8, 10));
+        require(ok, "setSlot failed (slot 8)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selAdd, 8, 5, 3, 9));
+        require(ok, "addIfBetween failed (min < delta < max)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 8));
+        require(ok, "getSlot failed (slot 8)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 15, "unexpected addIfBetween value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selAdd, 9, 3, 3, 9));
+        require(!ok, "addIfBetween should revert when delta <= min");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selAdd, 10, 9, 3, 9));
+        require(!ok, "addIfBetween should revert when delta >= max");
+    }
+}

From d77d6fe1e7ad11aaaec88cd9fecd91ec0caa995f Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 06:03:01 +0000
Subject: [PATCH 15/17] Add sstoreSub helper and subIfEnough example

---
 STATUS.md                                     |  2 +-
 docs/research-log.md                          |  5 ++
 .../DumbContracts/Compiler.lean               | 18 ++++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 44 +++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/SubIfEnough.lean   | 48 +++++++++++++++++++
 .../DumbContracts/Examples/TokenTransfer.lean | 20 ++++----
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedSubIfEnough.t.sol           | 41 ++++++++++++++++
 9 files changed, 170 insertions(+), 12 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/SubIfEnough.lean
 create mode 100644 research/lean_only_proto/test/GeneratedSubIfEnough.t.sol

diff --git a/STATUS.md b/STATUS.md
index b9f9645c5..18ad1faa0 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -19,7 +19,7 @@ Last updated: 2026-02-10
 - 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.
-- Iteration: add a minimal `requireBetween` helper and a tiny `addIfBetween` example + Foundry test.
+- Iteration: add `sstoreSub` helper and a tiny `subIfEnough` example + Foundry test.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
diff --git a/docs/research-log.md b/docs/research-log.md
index ecd3b5e73..0ad62a685 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `sstoreSub` stdlib helper for slot decrements.
+- Refactored `transfer` to use `sstoreSub` for balance subtraction.
+- Added `subIfEnough` example (guarded decrement when slot >= delta) with SpecR + proofs.
+- Added Foundry test for `subIfEnough`.
+- Updated compiler entries + direct EVM asm for `subIfEnough`.
 - Added `requireBetween` stdlib helper for strict range guards.
 - Refactored `setIfBetween` to use `requireBetween`.
 - Added `addIfBetween` example (guarded add on `min < delta < max`) with SpecR + proofs.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 11f64cc81..dbaecf0f8 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -261,6 +261,22 @@ def exampleEntry17 : EntryPoint :=
     selector := 0xbc0fcb79
     returns := false }
 
+def exampleEntry18 : EntryPoint :=
+  { name := "subIfEnough"
+    args := ["slot", "delta"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.not
+            (Lang.Expr.lt (Lang.Expr.var "current") (Lang.Expr.var "delta")))
+          (Lang.Stmt.sstore
+            (Lang.Expr.var "slot")
+            (Lang.Expr.sub (Lang.Expr.var "current") (Lang.Expr.var "delta")))
+          Lang.Stmt.revert)
+    -- subIfEnough(uint256,uint256) -> 0x9ee7809e
+    selector := 0x9ee7809e
+    returns := false }
+
 def exampleEntry13 : EntryPoint :=
   { name := "setIfNonZeroAndLess"
     args := ["slot", "value", "max"]
@@ -293,7 +309,7 @@ def exampleEntry14 : EntryPoint :=
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
     exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9,
-    exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry13, exampleEntry14]
+    exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18, exampleEntry13, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 6d6c4d54b..7df0274a6 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -84,6 +84,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_addIfBetween"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0x9ee7809e"
+  , "EQ"
+  , "PUSH2 tag_subIfEnough"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x8ba43d8f"
   , "EQ"
   , "PUSH2 tag_setIfNonZeroAndLess"
@@ -115,6 +120,16 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setIfNonZeroAndLess:"
   , "STOP"
+  , "tag_subIfEnough:"
+  , "PUSH2 ret_subIfEnough"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_subIfEnough"
+  , "JUMP"
+  , "ret_subIfEnough:"
+  , "STOP"
   , "tag_addIfBetween:"
   , "PUSH2 ret_addIfBetween"
   , "PUSH1 0x64"
@@ -656,6 +671,35 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 addIfBetween_inner_check"
   , "JUMP"
+  , "fn_subIfEnough:"
+  , "DUP1"
+  , "SLOAD"
+  , "SWAP1"
+  , "DUP3"
+  , "DUP3"
+  , "LT"
+  , "ISZERO"
+  , "PUSH2 subIfEnough_ok"
+  , "JUMPI"
+  , "subIfEnough_check:"
+  , "POP"
+  , "LT"
+  , "PUSH2 subIfEnough_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "subIfEnough_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "subIfEnough_ok:"
+  , "DUP3"
+  , "DUP3"
+  , "SUB"
+  , "SWAP1"
+  , "SSTORE"
+  , "PUSH0"
+  , "PUSH2 subIfEnough_check"
+  , "JUMP"
   , "fn_setIfNonZeroAndLess:"
   , "SWAP2"
   , "DUP2"
diff --git a/research/lean_only_proto/DumbContracts/Examples.lean b/research/lean_only_proto/DumbContracts/Examples.lean
index de350b4fa..e6a4a062d 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -16,3 +16,4 @@ import DumbContracts.Examples.AddIfBetween
 import DumbContracts.Examples.SetIfNonZeroAndLess
 import DumbContracts.Examples.BumpSlot
 import DumbContracts.Examples.BumpIfNonZero
+import DumbContracts.Examples.SubIfEnough
diff --git a/research/lean_only_proto/DumbContracts/Examples/SubIfEnough.lean b/research/lean_only_proto/DumbContracts/Examples/SubIfEnough.lean
new file mode 100644
index 000000000..a3f0295fa
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/SubIfEnough.lean
@@ -0,0 +1,48 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Decrement a slot by delta when the current value is large enough. -/
+
+def subIfEnoughFun : Fun :=
+  { name := "subIfEnough"
+    args := ["slot", "delta"]
+    body := letSload "current" (v "slot")
+      (require
+        (Expr.not (Expr.lt (v "current") (v "delta")))
+        (Stmt.sstore (v "slot") (Expr.sub (v "current") (v "delta"))))
+    ret := none }
+
+def subIfEnoughSpecR (slot delta : Nat) : SpecR Store :=
+  { requires := fun s => s slot >= delta
+    ensures := fun s s' => s' = updateStore s slot (s slot - delta)
+    reverts := fun s => s slot < delta }
+
+theorem subIfEnough_meets_specR_ok (s : Store) (slot delta : Nat) :
+    (subIfEnoughSpecR slot delta).requires s ->
+    (match execFun subIfEnoughFun [slot, delta] s [] with
+      | ExecResult.ok _ s' => (subIfEnoughSpecR slot delta).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hge : s slot >= delta := by exact hreq
+  have hnot : ¬ s slot < delta := by
+    exact not_lt_of_ge hge
+  simp [subIfEnoughSpecR, subIfEnoughFun, letSload, require, v, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+
+theorem subIfEnough_meets_specR_reverts (s : Store) (slot delta : Nat) :
+    (subIfEnoughSpecR slot delta).reverts s ->
+    execFun subIfEnoughFun [slot, delta] s [] = ExecResult.reverted := by
+  intro hrev
+  have hlt : s slot < delta := by exact hrev
+  simp [subIfEnoughSpecR, subIfEnoughFun, letSload, require, v, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hlt]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/TokenTransfer.lean b/research/lean_only_proto/DumbContracts/Examples/TokenTransfer.lean
index df7754156..781e206de 100644
--- a/research/lean_only_proto/DumbContracts/Examples/TokenTransfer.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/TokenTransfer.lean
@@ -1,12 +1,14 @@
 import DumbContracts.Examples.TokenBase
 import DumbContracts.Lang
 import DumbContracts.Semantics
+import DumbContracts.Stdlib
 
 namespace DumbContracts.Examples
 
 open DumbContracts.Lang
 open DumbContracts.Semantics
 open DumbContracts
+open DumbContracts.Std
 
 /-- Simple ERC20-style transfer. -/
 
@@ -19,11 +21,9 @@ def transferFun : Fun :=
       (Stmt.if_
         (Expr.lt (Expr.sload (Expr.add (Expr.lit 1000) (Expr.var "from"))) (Expr.var "amount"))
         Stmt.revert
-        (Stmt.sstore
+        (sstoreSub
             (Expr.add (Expr.lit 1000) (Expr.var "from"))
-            (Expr.sub
-              (Expr.sload (Expr.add (Expr.lit 1000) (Expr.var "from")))
-              (Expr.var "amount"))
+            (Expr.var "amount")
           ;;
           Stmt.sstore
             (Expr.add (Expr.lit 1000) (Expr.var "to"))
@@ -111,7 +111,7 @@ theorem transfer_meets_specR_ok (s : Store) (from to amount : Nat) :
   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,
+  simp [transferSpecR, transferFun, sstoreSub, execFun, execStmt, evalExpr, bindArgs, emptyEnv,
     updateEnv, updateStore, balanceSlot, setBalance, hto, hnotlt]
 
 theorem transfer_meets_specRNoSelf_ok (s : Store) (from to amount : Nat) :
@@ -134,7 +134,7 @@ theorem transfer_meets_specRSeq_ok (s : Store) (from to amount : Nat) :
   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,
+  simp [transferSpecRSeq, transferStoreSeq, transferFun, sstoreSub, execFun, execStmt, evalExpr,
     bindArgs, emptyEnv, updateEnv, updateStore, balanceSlot, setBalance, hto, hnotlt]
 
 theorem transfer_meets_specR_reverts (s : Store) (from to amount : Nat) :
@@ -143,13 +143,13 @@ theorem transfer_meets_specR_reverts (s : Store) (from to amount : Nat) :
   intro hrev
   cases hrev with
   | inl hto =>
-      simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
+      simp [transferFun, sstoreSub, 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,
+      · simp [transferFun, sstoreSub, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
           updateStore, balanceSlot, setBalance, hto]
-      · simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
+      · simp [transferFun, sstoreSub, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
           updateStore, balanceSlot, setBalance, hto, hlt]
 
 -- Aliasing boundary facts.
@@ -168,7 +168,7 @@ theorem transfer_self_noop (s : Store) (from amount : Nat)
             (updateStore s (balanceSlot from) (s (balanceSlot from) - amount))
             (balanceSlot from)
             (s (balanceSlot from) - amount + amount)) := by
-    simp [transferFun, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
+    simp [transferFun, sstoreSub, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv,
       updateStore, balanceSlot, hto, hnotlt]
   have hshadow :
       updateStore
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index e01a9f984..f7d0e3f94 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -57,6 +57,9 @@ def letSload (name : String) (slot : Expr) (body : Stmt) : Stmt :=
 def sstoreAdd (slot delta : Expr) : Stmt :=
   Stmt.sstore slot (Expr.add (Expr.sload slot) delta)
 
+def sstoreSub (slot delta : Expr) : Stmt :=
+  Stmt.sstore slot (Expr.sub (Expr.sload slot) delta)
+
 def sstoreInc (slot : Expr) : Stmt :=
   sstoreAdd slot (Expr.lit 1)
 
diff --git a/research/lean_only_proto/test/GeneratedSubIfEnough.t.sol b/research/lean_only_proto/test/GeneratedSubIfEnough.t.sol
new file mode 100644
index 000000000..a8d9b148f
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedSubIfEnough.t.sol
@@ -0,0 +1,41 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedSubIfEnoughTest is GeneratedBase {
+    function testSubIfEnough() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selSub = 0x9ee7809e;
+        bytes4 selSet = 0xf2c298be;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 30, 20));
+        require(ok, "setSlot failed (slot 30)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSub, 30, 7));
+        require(ok, "subIfEnough failed (20 - 7)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 30));
+        require(ok, "getSlot failed (slot 30)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 13, "unexpected subIfEnough value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSub, 30, 20));
+        require(!ok, "subIfEnough should revert when delta too large");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSet, 31, 5));
+        require(ok, "setSlot failed (slot 31)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSub, 31, 5));
+        require(ok, "subIfEnough failed (5 - 5)");
+
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 31));
+        require(ok, "getSlot failed (slot 31)");
+        val = abi.decode(data, (uint256));
+        require(val == 0, "unexpected subIfEnough zero value");
+    }
+}

From 16708425a37f1f4eb5d63a347d404a95edd5cc82 Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 06:28:36 +0000
Subject: [PATCH 16/17] Add requireGte helper and setIfAtLeast example

---
 STATUS.md                                     |  2 +-
 docs/research-log.md                          |  5 +++
 .../DumbContracts/Compiler.lean               | 15 ++++++-
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 43 ++++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/SetIfAtLeast.lean  | 45 +++++++++++++++++++
 .../DumbContracts/Examples/SubIfEnough.lean   | 13 +++---
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedSetIfAtLeast.t.sol          | 29 ++++++++++++
 9 files changed, 148 insertions(+), 8 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/SetIfAtLeast.lean
 create mode 100644 research/lean_only_proto/test/GeneratedSetIfAtLeast.t.sol

diff --git a/STATUS.md b/STATUS.md
index 18ad1faa0..bf92aaee9 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -19,7 +19,7 @@ Last updated: 2026-02-10
 - 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.
-- Iteration: add `sstoreSub` helper and a tiny `subIfEnough` example + Foundry test.
+- Iteration: add `requireGte` helper and a tiny `setIfAtLeast` example + Foundry test.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
diff --git a/docs/research-log.md b/docs/research-log.md
index 0ad62a685..84f620d89 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireGte` stdlib helper for `>=` guards (via `not lt`).
+- Refactored `subIfEnough` to use `requireGte`.
+- Added `setIfAtLeast` example (guarded store on `value >= min`) with SpecR + proofs.
+- Added Foundry test for `setIfAtLeast`.
+- Updated compiler entries + direct EVM asm for `setIfAtLeast`.
 - Added `sstoreSub` stdlib helper for slot decrements.
 - Refactored `transfer` to use `sstoreSub` for balance subtraction.
 - Added `subIfEnough` example (guarded decrement when slot >= delta) with SpecR + proofs.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index dbaecf0f8..91cb15b8d 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -206,6 +206,18 @@ def exampleEntry8 : EntryPoint :=
     selector := 0x2dbeb1ba
     returns := false }
 
+def exampleEntry19 : EntryPoint :=
+  { name := "setIfAtLeast"
+    args := ["slot", "value", "min"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.not (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "min")))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfAtLeast(uint256,uint256,uint256) -> 0x407cdd03
+    selector := 0x407cdd03
+    returns := false }
+
 def exampleEntry9 : EntryPoint :=
   { name := "bumpSlot"
     args := ["slot"]
@@ -309,7 +321,8 @@ def exampleEntry14 : EntryPoint :=
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
     exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9,
-    exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18, exampleEntry13, exampleEntry14]
+    exampleEntry19, exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18, exampleEntry13,
+    exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 7df0274a6..91578910e 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -69,6 +69,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_bumpSlot"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0x407cdd03"
+  , "EQ"
+  , "PUSH2 tag_setIfAtLeast"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x7e5acdb6"
   , "EQ"
   , "PUSH2 tag_setIfLess"
@@ -170,6 +175,18 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setIfLess:"
   , "STOP"
+  , "tag_setIfAtLeast:"
+  , "PUSH2 ret_setIfAtLeast"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfAtLeast"
+  , "JUMP"
+  , "ret_setIfAtLeast:"
+  , "STOP"
   , "tag_bumpSlot:"
   , "PUSH2 ret_bumpSlot"
   , "PUSH1 0x04"
@@ -541,6 +558,32 @@ def directProgramAsm : List String :=
   , "SWAP1"
   , "SSTORE"
   , "JUMP"
+  , "fn_setIfAtLeast:"
+  , "DUP2"
+  , "SWAP1"
+  , "DUP4"
+  , "DUP3"
+  , "LT"
+  , "ISZERO"
+  , "PUSH2 setIfAtLeast_ok"
+  , "JUMPI"
+  , "setIfAtLeast_check:"
+  , "POP"
+  , "POP"
+  , "LT"
+  , "PUSH2 setIfAtLeast_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "setIfAtLeast_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "setIfAtLeast_ok:"
+  , "SSTORE"
+  , "DUP1"
+  , "PUSH0"
+  , "PUSH2 setIfAtLeast_check"
+  , "JUMP"
   , "fn_setIfLess:"
   , "DUP2"
   , "SWAP1"
diff --git a/research/lean_only_proto/DumbContracts/Examples.lean b/research/lean_only_proto/DumbContracts/Examples.lean
index e6a4a062d..40b298f1e 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -10,6 +10,7 @@ import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.InitOnce
 import DumbContracts.Examples.SetIfGreater
+import DumbContracts.Examples.SetIfAtLeast
 import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.SetIfBetween
 import DumbContracts.Examples.AddIfBetween
diff --git a/research/lean_only_proto/DumbContracts/Examples/SetIfAtLeast.lean b/research/lean_only_proto/DumbContracts/Examples/SetIfAtLeast.lean
new file mode 100644
index 000000000..00d098fac
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/SetIfAtLeast.lean
@@ -0,0 +1,45 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Store a value into a slot only if it meets a minimum (>=). -/
+
+def setIfAtLeastFun : Fun :=
+  { name := "setIfAtLeast"
+    args := ["slot", "value", "min"]
+    body := requireGte (v "value") (v "min") (sstoreVar "slot" (v "value"))
+    ret := none }
+
+def setIfAtLeastSpecR (slot value min : Nat) : SpecR Store :=
+  { requires := fun _ => value >= min
+    ensures := fun s s' => s' = updateStore s slot value
+    reverts := fun _ => value < min }
+
+theorem setIfAtLeast_meets_specR_ok (s : Store) (slot value min : Nat) :
+    (setIfAtLeastSpecR slot value min).requires s ->
+    (match execFun setIfAtLeastFun [slot, value, min] s [] with
+      | ExecResult.ok _ s' => (setIfAtLeastSpecR slot value min).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hge : value >= min := by exact hreq
+  have hnot : ¬ value < min := by
+    exact not_lt_of_ge hge
+  simp [setIfAtLeastSpecR, setIfAtLeastFun, requireGte, require, sstoreVar, v, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+
+theorem setIfAtLeast_meets_specR_reverts (s : Store) (slot value min : Nat) :
+    (setIfAtLeastSpecR slot value min).reverts s ->
+    execFun setIfAtLeastFun [slot, value, min] s [] = ExecResult.reverted := by
+  intro hrev
+  have hlt : value < min := by exact hrev
+  simp [setIfAtLeastSpecR, setIfAtLeastFun, requireGte, require, sstoreVar, v, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hlt]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/SubIfEnough.lean b/research/lean_only_proto/DumbContracts/Examples/SubIfEnough.lean
index a3f0295fa..24a86530d 100644
--- a/research/lean_only_proto/DumbContracts/Examples/SubIfEnough.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/SubIfEnough.lean
@@ -15,8 +15,9 @@ def subIfEnoughFun : Fun :=
   { name := "subIfEnough"
     args := ["slot", "delta"]
     body := letSload "current" (v "slot")
-      (require
-        (Expr.not (Expr.lt (v "current") (v "delta")))
+      (requireGte
+        (v "current")
+        (v "delta")
         (Stmt.sstore (v "slot") (Expr.sub (v "current") (v "delta"))))
     ret := none }
 
@@ -34,15 +35,15 @@ theorem subIfEnough_meets_specR_ok (s : Store) (slot delta : Nat) :
   have hge : s slot >= delta := by exact hreq
   have hnot : ¬ s slot < delta := by
     exact not_lt_of_ge hge
-  simp [subIfEnoughSpecR, subIfEnoughFun, letSload, require, v, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+  simp [subIfEnoughSpecR, subIfEnoughFun, letSload, requireGte, require, v, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
 
 theorem subIfEnough_meets_specR_reverts (s : Store) (slot delta : Nat) :
     (subIfEnoughSpecR slot delta).reverts s ->
     execFun subIfEnoughFun [slot, delta] s [] = ExecResult.reverted := by
   intro hrev
   have hlt : s slot < delta := by exact hrev
-  simp [subIfEnoughSpecR, subIfEnoughFun, letSload, require, v, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hlt]
+  simp [subIfEnoughSpecR, subIfEnoughFun, letSload, requireGte, require, v, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hlt]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index f7d0e3f94..3e04bbb1c 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -43,6 +43,9 @@ def requireGt (lhs rhs : Expr) (body : Stmt) : Stmt :=
 def requireLt (lhs rhs : Expr) (body : Stmt) : Stmt :=
   require (Expr.lt lhs rhs) body
 
+def requireGte (lhs rhs : Expr) (body : Stmt) : Stmt :=
+  require (Expr.not (Expr.lt lhs rhs)) body
+
 def requireBetween (value lo hi : Expr) (body : Stmt) : Stmt :=
   requireAnd (Expr.gt value lo) (Expr.lt value hi) body
 
diff --git a/research/lean_only_proto/test/GeneratedSetIfAtLeast.t.sol b/research/lean_only_proto/test/GeneratedSetIfAtLeast.t.sol
new file mode 100644
index 000000000..822225214
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedSetIfAtLeast.t.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedSetIfAtLeastTest is GeneratedBase {
+    function testSetIfAtLeast() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selSet = 0x407cdd03;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 13, 9, 9));
+        require(ok, "setIfAtLeast failed (value == min)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 13));
+        require(ok, "getSlot failed (slot 13)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 9, "unexpected setIfAtLeast value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSet, 14, 12, 10));
+        require(ok, "setIfAtLeast failed (value > min)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selSet, 15, 4, 9));
+        require(!ok, "setIfAtLeast should revert when value < min");
+    }
+}

From 748b0da51e207604dc49aead697ca44d83347b3f Mon Sep 17 00:00:00 2001
From: "Thomas Marchand (agent)" <agent@thomas.md>
Date: Tue, 10 Feb 2026 07:29:34 +0000
Subject: [PATCH 17/17] Add requireZero helper and initToOne example

---
 STATUS.md                                     |  3 +-
 docs/research-log.md                          |  5 +++
 .../DumbContracts/Compiler.lean               | 19 ++++++--
 .../lean_only_proto/DumbContracts/EvmAsm.lean | 41 +++++++++++++++++
 .../DumbContracts/Examples.lean               |  1 +
 .../DumbContracts/Examples/InitOnce.lean      |  6 +--
 .../DumbContracts/Examples/InitToOne.lean     | 44 +++++++++++++++++++
 .../lean_only_proto/DumbContracts/Stdlib.lean |  3 ++
 .../test/GeneratedInitToOne.t.sol             | 26 +++++++++++
 9 files changed, 141 insertions(+), 7 deletions(-)
 create mode 100644 research/lean_only_proto/DumbContracts/Examples/InitToOne.lean
 create mode 100644 research/lean_only_proto/test/GeneratedInitToOne.t.sol

diff --git a/STATUS.md b/STATUS.md
index bf92aaee9..77b61685e 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -19,9 +19,10 @@ Last updated: 2026-02-10
 - 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.
-- Iteration: add `requireGte` helper and a tiny `setIfAtLeast` example + Foundry test.
+- Iteration: add `requireZero` helper and a tiny `initToOne` example + Foundry test.
 
 ## Recently Done
+- Added `requireZero` helper and an `initToOne` example + Foundry test.
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
 - Selector map (fixed + ABI keccak) and Foundry tests.
 - Spec-style wrappers for storage and Euler-style risk examples.
diff --git a/docs/research-log.md b/docs/research-log.md
index 84f620d89..3885a2b59 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireZero` stdlib helper for zero guards.
+- Refactored `initOnce` to use `requireZero`.
+- Added `initToOne` example (initialize slot to `1` when empty) with SpecR + proofs.
+- Added Foundry test for `initToOne`.
+- Updated compiler entries + direct EVM asm for `initToOne`.
 - Added `requireGte` stdlib helper for `>=` guards (via `not lt`).
 - Refactored `subIfEnough` to use `requireGte`.
 - Added `setIfAtLeast` example (guarded store on `value >= min`) with SpecR + proofs.
diff --git a/research/lean_only_proto/DumbContracts/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 91cb15b8d..faa841ec6 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -194,6 +194,19 @@ def exampleEntry12 : EntryPoint :=
     selector := 0xd3b9b05a
     returns := false }
 
+def exampleEntry20 : EntryPoint :=
+  { name := "initToOne"
+    args := ["slot"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.eq (Lang.Expr.var "current") (Lang.Expr.lit 0))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.lit 1))
+          Lang.Stmt.revert)
+    -- initToOne(uint256) -> 0x1ebe7f68
+    selector := 0x1ebe7f68
+    returns := false }
+
 def exampleEntry8 : EntryPoint :=
   { name := "setIfGreater"
     args := ["slot", "value", "min"]
@@ -320,9 +333,9 @@ def exampleEntry14 : EntryPoint :=
 
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
-    exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9,
-    exampleEntry19, exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18, exampleEntry13,
-    exampleEntry14]
+    exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry20, exampleEntry8,
+    exampleEntry9, exampleEntry19, exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18,
+    exampleEntry13, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
diff --git a/research/lean_only_proto/DumbContracts/EvmAsm.lean b/research/lean_only_proto/DumbContracts/EvmAsm.lean
index 91578910e..88b7cc081 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -59,6 +59,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_initOnce"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0x1ebe7f68"
+  , "EQ"
+  , "PUSH2 tag_initToOne"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x2dbeb1ba"
   , "EQ"
   , "PUSH2 tag_setIfGreater"
@@ -207,6 +212,14 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setIfGreater:"
   , "STOP"
+  , "tag_initToOne:"
+  , "PUSH2 ret_initToOne"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_initToOne"
+  , "JUMP"
+  , "ret_initToOne:"
+  , "STOP"
   , "tag_initOnce:"
   , "PUSH2 ret_initOnce"
   , "PUSH1 0x24"
@@ -524,6 +537,34 @@ def directProgramAsm : List String :=
   , "DUP1"
   , "PUSH2 initOnce_check"
   , "JUMP"
+  , "fn_initToOne:"
+  , "PUSH0"
+  , "SWAP1"
+  , "DUP1"
+  , "SLOAD"
+  , "SWAP1"
+  , "DUP3"
+  , "DUP3"
+  , "EQ"
+  , "PUSH2 initToOne_ok"
+  , "JUMPI"
+  , "initToOne_check:"
+  , "POP"
+  , "SUB"
+  , "PUSH2 initToOne_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "initToOne_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "initToOne_ok:"
+  , "PUSH1 0x01"
+  , "SWAP1"
+  , "SSTORE"
+  , "PUSH0"
+  , "PUSH2 initToOne_check"
+  , "JUMP"
   , "fn_setIfGreater:"
   , "DUP2"
   , "SWAP1"
diff --git a/research/lean_only_proto/DumbContracts/Examples.lean b/research/lean_only_proto/DumbContracts/Examples.lean
index 40b298f1e..e2f90d16e 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -9,6 +9,7 @@ import DumbContracts.Examples.UpdateMin
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.InitOnce
+import DumbContracts.Examples.InitToOne
 import DumbContracts.Examples.SetIfGreater
 import DumbContracts.Examples.SetIfAtLeast
 import DumbContracts.Examples.SetIfLess
diff --git a/research/lean_only_proto/DumbContracts/Examples/InitOnce.lean b/research/lean_only_proto/DumbContracts/Examples/InitOnce.lean
index b9373264d..36bcc5426 100644
--- a/research/lean_only_proto/DumbContracts/Examples/InitOnce.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/InitOnce.lean
@@ -16,7 +16,7 @@ def initOnceFun : Fun :=
     args := ["slot", "value"]
     body :=
       letSload "current" (v "slot")
-        (requireEq (v "current") (n 0) (sstoreVar "slot" (v "value")))
+        (requireZero (v "current") (sstoreVar "slot" (v "value")))
     ret := none }
 
 def initOnceSpecR (slot value : Nat) : SpecR Store :=
@@ -31,14 +31,14 @@ theorem initOnce_meets_specR_ok (s : Store) (slot value : Nat) :
       | _ => False) := by
   intro hreq
   have hzero : s slot = 0 := by exact hreq
-  simp [initOnceSpecR, initOnceFun, letSload, requireEq, eq, require, execFun, execStmt,
+  simp [initOnceSpecR, initOnceFun, letSload, requireZero, requireEq, eq, require, execFun, execStmt,
     evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hzero]
 
 theorem initOnce_meets_specR_reverts (s : Store) (slot value : Nat) :
     (initOnceSpecR slot value).reverts s ->
     execFun initOnceFun [slot, value] s [] = ExecResult.reverted := by
   intro hrev
-  simp [initOnceSpecR, initOnceFun, letSload, requireEq, eq, require, execFun, execStmt,
+  simp [initOnceSpecR, initOnceFun, letSload, requireZero, requireEq, eq, require, execFun, execStmt,
     evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
 
 end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Examples/InitToOne.lean b/research/lean_only_proto/DumbContracts/Examples/InitToOne.lean
new file mode 100644
index 000000000..a196895af
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/InitToOne.lean
@@ -0,0 +1,44 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Initialize a slot to 1 if it is currently zero. -/
+
+def initToOneFun : Fun :=
+  { name := "initToOne"
+    args := ["slot"]
+    body :=
+      letSload "current" (v "slot")
+        (requireZero (v "current") (sstoreVar "slot" (n 1)))
+    ret := none }
+
+def initToOneSpecR (slot : Nat) : SpecR Store :=
+  { requires := fun s => s slot = 0
+    ensures := fun s s' => s' = updateStore s slot 1
+    reverts := fun s => s slot != 0 }
+
+theorem initToOne_meets_specR_ok (s : Store) (slot : Nat) :
+    (initToOneSpecR slot).requires s ->
+    (match execFun initToOneFun [slot] s [] with
+      | ExecResult.ok _ s' => (initToOneSpecR slot).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hzero : s slot = 0 := by exact hreq
+  simp [initToOneSpecR, initToOneFun, letSload, requireZero, requireEq, eq, require, execFun,
+    execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hzero]
+
+theorem initToOne_meets_specR_reverts (s : Store) (slot : Nat) :
+    (initToOneSpecR slot).reverts s ->
+    execFun initToOneFun [slot] s [] = ExecResult.reverted := by
+  intro hrev
+  simp [initToOneSpecR, initToOneFun, letSload, requireZero, requireEq, eq, require, execFun,
+    execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+
+end DumbContracts.Examples
diff --git a/research/lean_only_proto/DumbContracts/Stdlib.lean b/research/lean_only_proto/DumbContracts/Stdlib.lean
index 3e04bbb1c..2cee29c9f 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -52,6 +52,9 @@ def requireBetween (value lo hi : Expr) (body : Stmt) : Stmt :=
 def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
   requireNeq value (Expr.lit 0) body
 
+def requireZero (value : Expr) (body : Stmt) : Stmt :=
+  requireEq value (Expr.lit 0) body
+
 /-- Shorthand for loading/storing fixed slots. -/
 
 def letSload (name : String) (slot : Expr) (body : Stmt) : Stmt :=
diff --git a/research/lean_only_proto/test/GeneratedInitToOne.t.sol b/research/lean_only_proto/test/GeneratedInitToOne.t.sol
new file mode 100644
index 000000000..ea400eb93
--- /dev/null
+++ b/research/lean_only_proto/test/GeneratedInitToOne.t.sol
@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedInitToOneTest is GeneratedBase {
+    function testInitToOne() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selInitToOne = 0x1ebe7f68;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selInitToOne, 20));
+        require(ok, "initToOne failed (first init)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 20));
+        require(ok, "getSlot failed (slot 20)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 1, "unexpected initToOne value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selInitToOne, 20));
+        require(!ok, "initToOne should revert when slot already set");
+    }
+}