diff --git a/STATUS.md b/STATUS.md
index 768fff2c9..77b61685e 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.
@@ -19,8 +19,10 @@ Last updated: 2026-02-09
 - 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 `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.
@@ -43,6 +45,14 @@ 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.
+- 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).
+- 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.
 - 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..3885a2b59 100644
--- a/docs/research-log.md
+++ b/docs/research-log.md
@@ -1,5 +1,76 @@
 # 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.
+- 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.
+- 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.
+- 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`.
+- 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.
+- 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.
+- 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.
+- 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.
+- 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.
+- 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.
+- 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`.
+- 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`.
+- 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).
+- 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.
@@ -21,6 +92,8 @@
 - 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.
+- 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/Compiler.lean b/research/lean_only_proto/DumbContracts/Compiler.lean
index 38b31382a..faa841ec6 100644
--- a/research/lean_only_proto/DumbContracts/Compiler.lean
+++ b/research/lean_only_proto/DumbContracts/Compiler.lean
@@ -131,8 +131,211 @@ 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 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"]
+    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 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 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 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"]
+    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 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"]
+    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 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 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 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 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"]
+    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 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]
+  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
+    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 aaac514ec..88b7cc081 100644
--- a/research/lean_only_proto/DumbContracts/EvmAsm.lean
+++ b/research/lean_only_proto/DumbContracts/EvmAsm.lean
@@ -11,69 +11,306 @@ 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"
+  , "DUP1"
+  , "PUSH4 0xe9cc4edd"
+  , "EQ"
+  , "PUSH2 tag_updateMax"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0x5c34a245"
+  , "EQ"
+  , "PUSH2 tag_updateMin"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0xac1f1f67"
+  , "EQ"
+  , "PUSH2 tag_setNonZero"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0xc74962fa"
+  , "EQ"
+  , "PUSH2 tag_compareAndSwap"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0xd3b9b05a"
+  , "EQ"
+  , "PUSH2 tag_initOnce"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0x1ebe7f68"
+  , "EQ"
+  , "PUSH2 tag_initToOne"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0x2dbeb1ba"
+  , "EQ"
+  , "PUSH2 tag_setIfGreater"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0xb8df0e12"
+  , "EQ"
+  , "PUSH2 tag_bumpSlot"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0x407cdd03"
+  , "EQ"
+  , "PUSH2 tag_setIfAtLeast"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0x7e5acdb6"
+  , "EQ"
+  , "PUSH2 tag_setIfLess"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0x5ebc58db"
+  , "EQ"
+  , "PUSH2 tag_setIfBetween"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0xbc0fcb79"
+  , "EQ"
+  , "PUSH2 tag_addIfBetween"
+  , "JUMPI"
+  , "DUP1"
+  , "PUSH4 0x9ee7809e"
+  , "EQ"
+  , "PUSH2 tag_subIfEnough"
+  , "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"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfNonZeroAndLess"
+  , "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"
+  , "CALLDATALOAD"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_addIfBetween"
+  , "JUMP"
+  , "ret_addIfBetween:"
+  , "STOP"
+  , "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"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfLess"
+  , "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"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_bumpSlot"
+  , "JUMP"
+  , "ret_bumpSlot:"
+  , "STOP"
+  , "tag_setIfGreater:"
+  , "PUSH2 ret_setIfGreater"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfGreater"
+  , "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"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_initOnce"
+  , "JUMP"
+  , "ret_initOnce:"
+  , "STOP"
+  , "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"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setNonZero"
+  , "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"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_updateMax"
+  , "JUMP"
+  , "ret_updateMax:"
+  , "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 +341,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 +362,7 @@ def directProgramAsm : List String :=
   , "SWAP1"
   , "SSTORE"
   , "PUSH0"
-  , "PUSH guardedAddSlot_check"
+  , "PUSH2 guardedAddSlot_check"
   , "JUMP"
   , "fn_maxStore:"
   , "SWAP1"
@@ -134,12 +371,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 +386,468 @@ 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_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_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"
+  , "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"
+  , "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"
+  , "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_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"
+  , "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"
+  , "fn_bumpSlot:"
+  , "PUSH1 0x01"
+  , "DUP2"
+  , "SLOAD"
+  , "ADD"
+  , "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"
+  , "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"
+  , "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"
+  , "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_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"
+  , "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"
+  , "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"
   ]
 
diff --git a/research/lean_only_proto/DumbContracts/Examples.lean b/research/lean_only_proto/DumbContracts/Examples.lean
index e4764e5f5..e2f90d16e 100644
--- a/research/lean_only_proto/DumbContracts/Examples.lean
+++ b/research/lean_only_proto/DumbContracts/Examples.lean
@@ -4,3 +4,18 @@ import DumbContracts.Examples.TokenBase
 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
+import DumbContracts.Examples.InitToOne
+import DumbContracts.Examples.SetIfGreater
+import DumbContracts.Examples.SetIfAtLeast
+import DumbContracts.Examples.SetIfLess
+import DumbContracts.Examples.SetIfBetween
+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/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/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
new file mode 100644
index 000000000..1f1cb4f2b
--- /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 := sstoreInc (v "slot")
+    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, sstoreInc, sstoreAdd, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, v, n]
+
+end DumbContracts.Examples
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..292757bc2
--- /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 :=
+      letSload "current" (v "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, 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, 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..36bcc5426
--- /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")
+        (requireZero (v "current") (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, 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, 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/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/NonZeroStore.lean b/research/lean_only_proto/DumbContracts/Examples/NonZeroStore.lean
new file mode 100644
index 000000000..aef4b51b1
--- /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 := requireNeq (v "value") (n 0) (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, 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, requireNeq, neq, eq, require, execFun, execStmt, evalExpr,
+    bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+
+end DumbContracts.Examples
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/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/SetIfBetween.lean b/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean
new file mode 100644
index 000000000..abdf5bde2
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/SetIfBetween.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
+
+/-- 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 :=
+      requireBetween
+        (v "value")
+        (v "min")
+        (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, 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) :
+    (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, 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, requireBetween, requireAnd, require, sstoreVar, v,
+        execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hnotlt]
+    · have hnot : ¬ value > min := by
+        exact hgt
+      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/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/SetIfLess.lean b/research/lean_only_proto/DumbContracts/Examples/SetIfLess.lean
new file mode 100644
index 000000000..b2c7f40f7
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/SetIfLess.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 is below a maximum. -/
+
+def setIfLessFun : Fun :=
+  { name := "setIfLess"
+    args := ["slot", "value", "max"]
+    body := requireLt (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, 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 ->
+    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, requireLt, 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/Examples/StoreOps.lean b/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
index 1e809ace8..fe1cd2238 100644
--- a/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
+++ b/research/lean_only_proto/DumbContracts/Examples/StoreOps.lean
@@ -26,16 +26,16 @@ 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 :=
   { name := "guardedAddSlot"
     args := ["slot", "delta"]
-    body := require
-      (Expr.gt (Expr.var "delta") (Expr.lit 0))
-      (Stmt.sstore (Expr.var "slot")
-        (Expr.add (Expr.sload (Expr.var "slot")) (Expr.var "delta")))
+    body := requireGt
+      (v "delta")
+      (n 0)
+      (sstoreAdd (v "slot") (v "delta"))
     ret := none }
 
 /-- A minimal store for point examples. -/
@@ -58,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
@@ -74,19 +74,20 @@ 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]
+    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) [] =
       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).
 
@@ -109,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 ->
@@ -119,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]
+    bindArgs, emptyEnv, updateEnv, updateStore, hpos, requireGt, v, n, sstoreAdd]
 
 theorem guardedAddSlot_meets_specR_ok (s : Store) (slot delta : Nat) :
     (guardedAddSlotSpecR slot delta).requires s ->
@@ -129,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]
+    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]
+    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 ∧
@@ -144,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]
+      updateEnv, updateStore, h, requireGt, v, n, sstoreAdd]
 
 end DumbContracts.Examples
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..24a86530d
--- /dev/null
+++ b/research/lean_only_proto/DumbContracts/Examples/SubIfEnough.lean
@@ -0,0 +1,49 @@
+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")
+      (requireGte
+        (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, 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, requireGte, 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/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/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 c458539d0..2cee29c9f 100644
--- a/research/lean_only_proto/DumbContracts/Stdlib.lean
+++ b/research/lean_only_proto/DumbContracts/Stdlib.lean
@@ -16,11 +16,65 @@ 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
+
 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 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 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
+
+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 :=
+  Stmt.let_ name (Expr.sload slot) body
+
+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)
+
+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/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");
+    }
+}
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");
+    }
+}
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");
+    }
+}
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/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");
+    }
+}
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");
+    }
+}
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");
+    }
+}
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");
+    }
+}
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");
+    }
+}
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");
+    }
+}
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");
+    }
+}
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");
+    }
+}
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");
+    }
+}
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");
+    }
+}
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");
+    }
+}
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 3d280d139..000000000
Binary files a/research/lean_only_proto/tools/__pycache__/compare_evm_asm.cpython-312.pyc and /dev/null differ