Add requireAnd helper and setIfNonZeroAndLess 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 `letSload` helper and an `initOnce` example to make cached-slot guards less noisy.
+- Iteration: add `requireAnd` helper plus a `setIfNonZeroAndLess` example to reduce nested guard boilerplate.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.

docs/research-log.md

@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireAnd` stdlib helper to combine guard conditions cleanly.
+- Refactored `setIfBetween` to use `requireAnd` instead of nested guards.
+- Added `setIfNonZeroAndLess` example (nonzero + max guard) with SpecR + proofs.
+- Added Foundry test for `setIfNonZeroAndLess`.
+- Updated compiler entries + direct EVM asm for `setIfNonZeroAndLess`.
 - Added `letSload` stdlib helper for caching a slot read via `let_`.
 - Refactored `compareAndSwap` to use `letSload`.
 - Added `initOnce` example (only initialize a zero slot) with SpecR + proofs.

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -218,9 +218,23 @@ def exampleEntry11 : EntryPoint :=
     selector := 0x5ebc58db
     returns := false }
 
+def exampleEntry13 : EntryPoint :=
+  { name := "setIfNonZeroAndLess"
+    args := ["slot", "value", "max"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.and
+          (Lang.Expr.not (Lang.Expr.eq (Lang.Expr.var "value") (Lang.Expr.lit 0)))
+          (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "max")))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfNonZeroAndLess(uint256,uint256,uint256) -> 0x8ba43d8f
+    selector := 0x8ba43d8f
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
-    exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11]
+    exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11, exampleEntry13]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -63,13 +63,30 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_setIfLess"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x5ebc58db"
   , "EQ"
   , "PUSH2 tag_setIfBetween"
   , "JUMPI"
+  , "PUSH4 0x8ba43d8f"
+  , "EQ"
+  , "PUSH2 tag_setIfNonZeroAndLess"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_setIfNonZeroAndLess:"
+  , "PUSH2 ret_setIfNonZeroAndLess"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfNonZeroAndLess"
+  , "JUMP"
+  , "ret_setIfNonZeroAndLess:"
+  , "STOP"
   , "tag_setIfBetween:"
   , "PUSH2 ret_setIfBetween"
   , "PUSH1 0x64"
@@ -464,6 +481,43 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 setIfBetween_inner_check"
   , "JUMP"
+  , "fn_setIfNonZeroAndLess:"
+  , "SWAP2"
+  , "DUP2"
+  , "PUSH0"
+  , "SWAP3"
+  , "SWAP4"
+  , "DUP3"
+  , "DUP3"
+  , "LT"
+  , "DUP5"
+  , "DUP4"
+  , "EQ"
+  , "ISZERO"
+  , "AND"
+  , "PUSH2 setIfNonZeroAndLess_ok"
+  , "JUMPI"
+  , "setIfNonZeroAndLess_check:"
+  , "POP"
+  , "LT"
+  , "SWAP2"
+  , "EQ"
+  , "ISZERO"
+  , "AND"
+  , "ISZERO"
+  , "PUSH2 setIfNonZeroAndLess_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "setIfNonZeroAndLess_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "setIfNonZeroAndLess_ok:"
+  , "SSTORE"
+  , "DUP3"
+  , "PUSH0"
+  , "PUSH2 setIfNonZeroAndLess_check"
+  , "JUMP"
   ]
 
 def pretty (lines : List String) : String :=

research/lean_only_proto/DumbContracts/Examples.lean

@@ -10,4 +10,5 @@ import DumbContracts.Examples.InitOnce
 import DumbContracts.Examples.SetIfGreater
 import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.SetIfBetween
+import DumbContracts.Examples.SetIfNonZeroAndLess
 import DumbContracts.Examples.BumpSlot

research/lean_only_proto/DumbContracts/Examples/SetIfBetween.lean

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

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

research/lean_only_proto/DumbContracts/Stdlib.lean

@@ -16,6 +16,9 @@ def require (cond : Expr) (body : Stmt) : Stmt :=
 def unless (cond : Expr) (body : Stmt) : Stmt :=
   Stmt.if_ cond Stmt.revert body
 
+def requireAnd (lhs rhs : Expr) (body : Stmt) : Stmt :=
+  require (Expr.and lhs rhs) body
+
 def revertIf (cond : Expr) : Stmt :=
   Stmt.if_ cond Stmt.revert Stmt.skip
 

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