Add requireGte helper and setIfAtLeast 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 `sstoreSub` helper and a tiny `subIfEnough` example + Foundry test.
+- Iteration: add `requireGte` helper and a tiny `setIfAtLeast` example + Foundry test.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.

docs/research-log.md

@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireGte` stdlib helper for `>=` guards (via `not lt`).
+- Refactored `subIfEnough` to use `requireGte`.
+- Added `setIfAtLeast` example (guarded store on `value >= min`) with SpecR + proofs.
+- Added Foundry test for `setIfAtLeast`.
+- Updated compiler entries + direct EVM asm for `setIfAtLeast`.
 - Added `sstoreSub` stdlib helper for slot decrements.
 - Refactored `transfer` to use `sstoreSub` for balance subtraction.
 - Added `subIfEnough` example (guarded decrement when slot >= delta) with SpecR + proofs.

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -206,6 +206,18 @@ def exampleEntry8 : EntryPoint :=
     selector := 0x2dbeb1ba
     returns := false }
 
+def exampleEntry19 : EntryPoint :=
+  { name := "setIfAtLeast"
+    args := ["slot", "value", "min"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.not (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "min")))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfAtLeast(uint256,uint256,uint256) -> 0x407cdd03
+    selector := 0x407cdd03
+    returns := false }
+
 def exampleEntry9 : EntryPoint :=
   { name := "bumpSlot"
     args := ["slot"]
@@ -309,7 +321,8 @@ def exampleEntry14 : EntryPoint :=
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
     exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9,
-    exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18, exampleEntry13, exampleEntry14]
+    exampleEntry19, exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18, exampleEntry13,
+    exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -69,6 +69,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_bumpSlot"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0x407cdd03"
+  , "EQ"
+  , "PUSH2 tag_setIfAtLeast"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x7e5acdb6"
   , "EQ"
   , "PUSH2 tag_setIfLess"
@@ -170,6 +175,18 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setIfLess:"
   , "STOP"
+  , "tag_setIfAtLeast:"
+  , "PUSH2 ret_setIfAtLeast"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfAtLeast"
+  , "JUMP"
+  , "ret_setIfAtLeast:"
+  , "STOP"
   , "tag_bumpSlot:"
   , "PUSH2 ret_bumpSlot"
   , "PUSH1 0x04"
@@ -541,6 +558,32 @@ def directProgramAsm : List String :=
   , "SWAP1"
   , "SSTORE"
   , "JUMP"
+  , "fn_setIfAtLeast:"
+  , "DUP2"
+  , "SWAP1"
+  , "DUP4"
+  , "DUP3"
+  , "LT"
+  , "ISZERO"
+  , "PUSH2 setIfAtLeast_ok"
+  , "JUMPI"
+  , "setIfAtLeast_check:"
+  , "POP"
+  , "POP"
+  , "LT"
+  , "PUSH2 setIfAtLeast_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "setIfAtLeast_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "setIfAtLeast_ok:"
+  , "SSTORE"
+  , "DUP1"
+  , "PUSH0"
+  , "PUSH2 setIfAtLeast_check"
+  , "JUMP"
   , "fn_setIfLess:"
   , "DUP2"
   , "SWAP1"

research/lean_only_proto/DumbContracts/Examples.lean

@@ -10,6 +10,7 @@ import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.InitOnce
 import DumbContracts.Examples.SetIfGreater
+import DumbContracts.Examples.SetIfAtLeast
 import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.SetIfBetween
 import DumbContracts.Examples.AddIfBetween

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

research/lean_only_proto/DumbContracts/Examples/SubIfEnough.lean

@@ -15,8 +15,9 @@ def subIfEnoughFun : Fun :=
   { name := "subIfEnough"
     args := ["slot", "delta"]
     body := letSload "current" (v "slot")
-      (require
-        (Expr.not (Expr.lt (v "current") (v "delta")))
+      (requireGte
+        (v "current")
+        (v "delta")
         (Stmt.sstore (v "slot") (Expr.sub (v "current") (v "delta"))))
     ret := none }
 
@@ -34,15 +35,15 @@ theorem subIfEnough_meets_specR_ok (s : Store) (slot delta : Nat) :
   have hge : s slot >= delta := by exact hreq
   have hnot : ¬ s slot < delta := by
     exact not_lt_of_ge hge
-  simp [subIfEnoughSpecR, subIfEnoughFun, letSload, require, v, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hnot]
+  simp [subIfEnoughSpecR, subIfEnoughFun, letSload, requireGte, require, v, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hnot]
 
 theorem subIfEnough_meets_specR_reverts (s : Store) (slot delta : Nat) :
     (subIfEnoughSpecR slot delta).reverts s ->
     execFun subIfEnoughFun [slot, delta] s [] = ExecResult.reverted := by
   intro hrev
   have hlt : s slot < delta := by exact hrev
-  simp [subIfEnoughSpecR, subIfEnoughFun, letSload, require, v, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hlt]
+  simp [subIfEnoughSpecR, subIfEnoughFun, letSload, requireGte, require, v, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hlt]
 
 end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Stdlib.lean

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

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