Add revertIf helper and setIfLess example

Author: Th0rgal

STATUS.md

@@ -48,6 +48,8 @@ Last updated: 2026-02-10
 - 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 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).

docs/research-log.md

@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- 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`.

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -178,9 +178,21 @@ def exampleEntry9 : EntryPoint :=
     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 exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
-    exampleEntry8, exampleEntry9]
+    exampleEntry8, exampleEntry9, exampleEntry10]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -48,13 +48,30 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_setIfGreater"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xb8df0e12"
   , "EQ"
   , "PUSH2 tag_bumpSlot"
   , "JUMPI"
+  , "PUSH4 0x7e5acdb6"
+  , "EQ"
+  , "PUSH2 tag_setIfLess"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_setIfLess:"
+  , "PUSH2 ret_setIfLess"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_setIfLess"
+  , "JUMP"
+  , "ret_setIfLess:"
+  , "STOP"
   , "tag_bumpSlot:"
   , "PUSH2 ret_bumpSlot"
   , "PUSH1 0x04"
@@ -308,6 +325,32 @@ def directProgramAsm : List String :=
   , "SWAP1"
   , "SSTORE"
   , "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"
   ]
 
 def pretty (lines : List String) : String :=

research/lean_only_proto/DumbContracts/Examples.lean

@@ -7,4 +7,5 @@ import DumbContracts.Examples.MaxStore
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.SetIfGreater
+import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.BumpSlot

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

research/lean_only_proto/DumbContracts/Examples/SetIfLess.lean

@@ -0,0 +1,46 @@
+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 :=
+      revertIf (Expr.not (Expr.lt (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, revertIf, 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, revertIf, sstoreVar, v, 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 revertIf (cond : Expr) : Stmt :=
+  Stmt.if_ cond Stmt.revert Stmt.skip
+
 def assert (cond : Expr) : Stmt :=
   Stmt.if_ cond Stmt.skip Stmt.revert
 

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