Add requireBetween helper and addIfBetween example

Author: Th0rgal

STATUS.md

@@ -19,7 +19,7 @@ Last updated: 2026-02-10
 - Decide whether to guard old-state specs with `from ≠ to` or adopt sequential reads by default.
 - Supply accounting abstraction (list vs set/dedup semantics).
 - EDSL ergonomics: add helpers, notations, and a minimal stdlib for common patterns.
-- Iteration: add a minimal `sstoreMin` helper and a tiny `updateMin` example + Foundry test.
+- Iteration: add a minimal `requireBetween` helper and a tiny `addIfBetween` example + Foundry test.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.

docs/research-log.md

@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireBetween` stdlib helper for strict range guards.
+- Refactored `setIfBetween` to use `requireBetween`.
+- Added `addIfBetween` example (guarded add on `min < delta < max`) with SpecR + proofs.
+- Added Foundry test for `addIfBetween`.
+- Updated compiler entries + direct EVM asm for `addIfBetween`.
 - Added `sstoreMin` stdlib helper to mirror `sstoreMax` for min updates.
 - Added `updateMin` example (monotonic min update against a stored slot) with Spec + proof.
 - Added Foundry test for `updateMin`.

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -244,6 +244,23 @@ def exampleEntry11 : EntryPoint :=
     selector := 0x5ebc58db
     returns := false }
 
+def exampleEntry17 : EntryPoint :=
+  { name := "addIfBetween"
+    args := ["slot", "delta", "min", "max"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.gt (Lang.Expr.var "delta") (Lang.Expr.var "min"))
+        (Lang.Stmt.if_
+          (Lang.Expr.lt (Lang.Expr.var "delta") (Lang.Expr.var "max"))
+          (Lang.Stmt.sstore
+            (Lang.Expr.var "slot")
+            (Lang.Expr.add (Lang.Expr.sload (Lang.Expr.var "slot")) (Lang.Expr.var "delta")))
+          Lang.Stmt.revert)
+        Lang.Stmt.revert
+    -- addIfBetween(uint256,uint256,uint256,uint256) -> 0xbc0fcb79
+    selector := 0xbc0fcb79
+    returns := false }
+
 def exampleEntry13 : EntryPoint :=
   { name := "setIfNonZeroAndLess"
     args := ["slot", "value", "max"]
@@ -276,7 +293,7 @@ def exampleEntry14 : EntryPoint :=
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
     exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9,
-    exampleEntry10, exampleEntry11, exampleEntry13, exampleEntry14]
+    exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry13, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -79,6 +79,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_setIfBetween"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0xbc0fcb79"
+  , "EQ"
+  , "PUSH2 tag_addIfBetween"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x8ba43d8f"
   , "EQ"
   , "PUSH2 tag_setIfNonZeroAndLess"
@@ -110,6 +115,20 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setIfNonZeroAndLess:"
   , "STOP"
+  , "tag_addIfBetween:"
+  , "PUSH2 ret_addIfBetween"
+  , "PUSH1 0x64"
+  , "CALLDATALOAD"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_addIfBetween"
+  , "JUMP"
+  , "ret_addIfBetween:"
+  , "STOP"
   , "tag_setIfBetween:"
   , "PUSH2 ret_setIfBetween"
   , "PUSH1 0x64"
@@ -584,6 +603,59 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 setIfBetween_inner_check"
   , "JUMP"
+  , "fn_addIfBetween:"
+  , "SWAP3"
+  , "SWAP1"
+  , "SWAP2"
+  , "SWAP3"
+  , "DUP4"
+  , "DUP4"
+  , "GT"
+  , "PUSH2 addIfBetween_outer_ok"
+  , "JUMPI"
+  , "addIfBetween_outer_check:"
+  , "POP"
+  , "POP"
+  , "GT"
+  , "ISZERO"
+  , "PUSH2 addIfBetween_revert_outer"
+  , "JUMPI"
+  , "JUMP"
+  , "addIfBetween_revert_outer:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "addIfBetween_outer_ok:"
+  , "DUP2"
+  , "DUP4"
+  , "LT"
+  , "PUSH2 addIfBetween_inner_ok"
+  , "JUMPI"
+  , "addIfBetween_inner_check:"
+  , "POP"
+  , "DUP2"
+  , "LT"
+  , "ISZERO"
+  , "PUSH2 addIfBetween_revert_inner"
+  , "JUMPI"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH2 addIfBetween_outer_check"
+  , "JUMP"
+  , "addIfBetween_revert_inner:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "addIfBetween_inner_ok:"
+  , "DUP3"
+  , "DUP2"
+  , "SLOAD"
+  , "ADD"
+  , "SWAP1"
+  , "SSTORE"
+  , "PUSH0"
+  , "PUSH2 addIfBetween_inner_check"
+  , "JUMP"
   , "fn_setIfNonZeroAndLess:"
   , "SWAP2"
   , "DUP2"

research/lean_only_proto/DumbContracts/Examples.lean

@@ -12,6 +12,7 @@ import DumbContracts.Examples.InitOnce
 import DumbContracts.Examples.SetIfGreater
 import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.SetIfBetween
+import DumbContracts.Examples.AddIfBetween
 import DumbContracts.Examples.SetIfNonZeroAndLess
 import DumbContracts.Examples.BumpSlot
 import DumbContracts.Examples.BumpIfNonZero

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

research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean

@@ -15,9 +15,10 @@ def setIfBetweenFun : Fun :=
   { name := "setIfBetween"
     args := ["slot", "value", "min", "max"]
     body :=
-      requireAnd
-        (Expr.gt (v "value") (v "min"))
-        (Expr.lt (v "value") (v "max"))
+      requireBetween
+        (v "value")
+        (v "min")
+        (v "max")
         (sstoreVar "slot" (v "value"))
     ret := none }
 
@@ -33,7 +34,7 @@ theorem setIfBetween_meets_specR_ok (s : Store) (slot value min max : Nat) :
       | _ => False) := by
   intro hreq
   rcases hreq with ⟨hgt, hlt⟩
-  simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v, execFun,
+  simp [setIfBetweenSpecR, setIfBetweenFun, requireBetween, requireAnd, require, sstoreVar, v, execFun,
     execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hlt]
 
 theorem setIfBetween_meets_specR_reverts (s : Store) (slot value min max : Nat) :
@@ -43,16 +44,16 @@ theorem setIfBetween_meets_specR_reverts (s : Store) (slot value min max : Nat)
   rcases hrev with hle | hge
   · have hnot : ¬ value > min := by
       exact Nat.not_lt.mpr hle
-    simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v, execFun,
+    simp [setIfBetweenSpecR, setIfBetweenFun, requireBetween, requireAnd, require, sstoreVar, v, execFun,
       execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
   · by_cases hgt : value > min
     · have hnotlt : ¬ value < max := by
         exact Nat.not_lt.mpr hge
-      simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v,
+      simp [setIfBetweenSpecR, setIfBetweenFun, requireBetween, requireAnd, require, sstoreVar, v,
         execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hgt, hnotlt]
     · have hnot : ¬ value > min := by
         exact hgt
-      simp [setIfBetweenSpecR, setIfBetweenFun, requireAnd, require, sstoreVar, v,
+      simp [setIfBetweenSpecR, setIfBetweenFun, requireBetween, requireAnd, require, sstoreVar, v,
         execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
 
 end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Stdlib.lean

@@ -43,6 +43,9 @@ def requireGt (lhs rhs : Expr) (body : Stmt) : Stmt :=
 def requireLt (lhs rhs : Expr) (body : Stmt) : Stmt :=
   require (Expr.lt lhs rhs) body
 
+def requireBetween (value lo hi : Expr) (body : Stmt) : Stmt :=
+  requireAnd (Expr.gt value lo) (Expr.lt value hi) body
+
 def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
   requireNeq value (Expr.lit 0) body
 

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");
+    }
+}