Add requireGt helper and setIfGreater example

Author: Th0rgal

STATUS.md

@@ -46,6 +46,7 @@ Last updated: 2026-02-10
 - Added a `requireNonZero` helper and a tiny `setNonZero` example + Foundry test.
 - Aligned direct EVM asm with solc for `setNonZero` (label pushes use `PUSH2`).
 - Added `requireEq`/`requireNeq` helpers plus a `compareAndSwap` example + Foundry test.
+- Added `requireGt` helper plus a `setIfGreater` example + Foundry test (and refactored guarded add to use it).
 - Minimal docs frontend and compressed docs.
 - Further docs tightening (shorter guide + text).
 - External landscape scan (spec languages, model checkers, prover stacks).

docs/research-log.md

@@ -1,6 +1,10 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireGt` stdlib helper to reduce guard boilerplate.
+- Added `setIfGreater` example (guarded store on `value > min`) with SpecR + proofs.
+- Refactored `guardedAddSlot` to use `requireGt`.
+- Added Foundry test for `setIfGreater`.
 - Added `eq`/`neq` plus `requireEq`/`requireNeq` stdlib helpers.
 - Added `compareAndSwap` example (guarded store on expected value match) with SpecR and proofs.
 - Avoided double `sload` in `compareAndSwap` by caching the slot value with `let_` (prevents false reverts).

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -155,8 +155,21 @@ def exampleEntry7 : EntryPoint :=
     selector := 0xc74962fa
     returns := false }
 
+def exampleEntry8 : EntryPoint :=
+  { name := "setIfGreater"
+    args := ["slot", "value", "min"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.gt (Lang.Expr.var "value") (Lang.Expr.var "min"))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfGreater(uint256,uint256,uint256) -> 0x2dbeb1ba
+    selector := 0x2dbeb1ba
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
-  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7]
+  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
+    exampleEntry8]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -38,13 +38,30 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_setNonZero"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xc74962fa"
   , "EQ"
   , "PUSH2 tag_compareAndSwap"
   , "JUMPI"
+  , "PUSH4 0x2dbeb1ba"
+  , "EQ"
+  , "PUSH2 tag_setIfGreater"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_setIfGreater:"
+  , "PUSH2 ret_setIfGreater"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfGreater"
+  , "JUMP"
+  , "ret_setIfGreater:"
+  , "STOP"
   , "tag_compareAndSwap:"
   , "PUSH2 ret_compareAndSwap"
   , "PUSH1 0x44"
@@ -244,6 +261,32 @@ def directProgramAsm : List String :=
   , "DUP1"
   , "PUSH2 compareAndSwap_check"
   , "JUMP"
+  , "fn_setIfGreater:"
+  , "DUP2"
+  , "SWAP1"
+  , "DUP4"
+  , "DUP3"
+  , "GT"
+  , "PUSH2 setIfGreater_ok"
+  , "JUMPI"
+  , "setIfGreater_check:"
+  , "POP"
+  , "POP"
+  , "GT"
+  , "ISZERO"
+  , "PUSH2 setIfGreater_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "setIfGreater_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "setIfGreater_ok:"
+  , "SSTORE"
+  , "DUP1"
+  , "PUSH0"
+  , "PUSH2 setIfGreater_check"
+  , "JUMP"
   ]
 
 def pretty (lines : List String) : String :=

research/lean_only_proto/DumbContracts/Examples.lean

@@ -6,3 +6,4 @@ import DumbContracts.Examples.TokenTransfer
 import DumbContracts.Examples.MaxStore
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
+import DumbContracts.Examples.SetIfGreater

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

research/lean_only_proto/DumbContracts/Examples/StoreOps.lean

@@ -32,8 +32,9 @@ def addSlotFun : Fun :=
 def guardedAddSlotFun : Fun :=
   { name := "guardedAddSlot"
     args := ["slot", "delta"]
-    body := require
-      (Expr.gt (Expr.var "delta") (Expr.lit 0))
+    body := requireGt
+      (v "delta")
+      (n 0)
       (Stmt.sstore (Expr.var "slot")
         (Expr.add (Expr.sload (Expr.var "slot")) (Expr.var "delta")))
     ret := none }
@@ -80,13 +81,13 @@ theorem guarded_add_updates (slot base delta : Nat) (h : delta > 0) :
     execFun guardedAddSlotFun [slot, delta] (storeOf slot base) [] =
       ExecResult.ok (bindArgs emptyEnv ["slot", "delta"] [slot, delta]) (storeOf slot (base + delta)) := by
   simp [guardedAddSlotFun, require, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv,
-    updateEnv, updateStore, h]
+    updateEnv, updateStore, h, requireGt, v, n]
 
 theorem guarded_add_reverts (slot base delta : Nat) (h : delta = 0) :
     execFun guardedAddSlotFun [slot, delta] (storeOf slot base) [] =
       ExecResult.reverted := by
   simp [guardedAddSlotFun, require, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv,
-    updateEnv, updateStore, h]
+    updateEnv, updateStore, h, requireGt, v, n]
 
 -- Storage specs (Store-level).
 
@@ -119,7 +120,7 @@ theorem guardedAddSlot_meets_spec (s : Store) (slot delta : Nat) :
   intro hreq
   have hpos : delta > 0 := by exact hreq
   simp [guardedAddSlotSpec, guardedAddSlotFun, require, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hpos]
+    bindArgs, emptyEnv, updateEnv, updateStore, hpos, requireGt, v, n]
 
 theorem guardedAddSlot_meets_specR_ok (s : Store) (slot delta : Nat) :
     (guardedAddSlotSpecR slot delta).requires s ->
@@ -129,21 +130,21 @@ theorem guardedAddSlot_meets_specR_ok (s : Store) (slot delta : Nat) :
   intro hreq
   have hpos : delta > 0 := by exact hreq
   simp [guardedAddSlotSpecR, guardedAddSlotFun, require, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hpos]
+    bindArgs, emptyEnv, updateEnv, updateStore, hpos, requireGt, v, n]
 
 theorem guardedAddSlot_meets_specR_reverts (s : Store) (slot delta : Nat) :
     (guardedAddSlotSpecR slot delta).reverts s ->
     execFun guardedAddSlotFun [slot, delta] s [] = ExecResult.reverted := by
   intro hrev
   simp [guardedAddSlotSpecR, guardedAddSlotFun, require, execFun, execStmt, evalExpr,
-    bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+    bindArgs, emptyEnv, updateEnv, updateStore, hrev, requireGt, v, n]
 
 theorem guardedAddSlot_reverts_when_not_requires (slot delta : Nat) (h : delta = 0) :
     (guardedAddSlotSpec slot delta).requires (storeOf slot 0) = False ∧
     execFun guardedAddSlotFun [slot, delta] (storeOf slot 0) [] = ExecResult.reverted := by
   constructor
   · simp [guardedAddSlotSpec, h]
   · simp [guardedAddSlotFun, require, execFun, execStmt, evalExpr, storeOf, bindArgs, emptyEnv,
-      updateEnv, updateStore, h]
+      updateEnv, updateStore, h, requireGt, v, n]
 
 end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Stdlib.lean

@@ -31,6 +31,9 @@ def requireEq (lhs rhs : Expr) (body : Stmt) : Stmt :=
 def requireNeq (lhs rhs : Expr) (body : Stmt) : Stmt :=
   require (neq lhs rhs) body
 
+def requireGt (lhs rhs : Expr) (body : Stmt) : Stmt :=
+  require (Expr.gt lhs rhs) body
+
 def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
   requireNeq value (Expr.lit 0) body
 

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