Add sstoreIfLt helper and capSlot example

Author: Th0rgal

STATUS.md

@@ -19,9 +19,11 @@ 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 `sstoreIfLt` helper plus a capped-slot example to avoid redundant writes.
 
 
 ## Recently Done
+- Added `sstoreIfLt` helper, refactored `updateMin`, and added `capSlot` example + Foundry test.
 - Added `sstoreIfZero` helper and an `initDouble` example + Foundry test.
 - Added `requireZero` helper and an `initToOne` example + Foundry test.
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.

docs/research-log.md

@@ -118,3 +118,10 @@
 - Updated compiler entries + direct EVM asm wiring for `initDouble`.
 - `end_to_end` initially failed due to direct EVM asm mismatch in `initDouble`; fixed by aligning the stack order (`swap1` prelude + `swap1` before `sstore`) with solc output.
 - Ran `PATH=/opt/lean-4.27.0/bin:$PATH lake build`, `./scripts/end_to_end.sh`, and `./scripts/foundry_test_generated.sh` (all green).
+- Added `sstoreIfLt` stdlib helper to avoid redundant stores when capping a slot.
+- Refactored `updateMin` to use `sstoreIfLt` (skip store when the slot is already below the cap).
+- Added `capSlot` example (cap a slot to a maximum without reverting) with Spec + proof.
+- Added Foundry test for `capSlot`.
+- Updated compiler entries + direct EVM asm wiring for `updateMin` and `capSlot`.
+- `end_to_end` initially failed due to direct EVM asm block layout for `capSlot`/`updateMin`; fixed by matching solc's `jump(tag_out)` shape and using `PUSH0` for zero.
+- Ran `PATH=/opt/lean-4.27.0/bin:$PATH lake build`, `./scripts/end_to_end.sh`, and `./scripts/foundry_test_generated.sh` (all green).

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -150,13 +150,26 @@ def exampleEntry16 : EntryPoint :=
     body :=
       Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
         (Lang.Stmt.if_
-          (Lang.Expr.lt (Lang.Expr.var "current") (Lang.Expr.var "value"))
-          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "current"))
-          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value")))
+          (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "current"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+          Lang.Stmt.skip)
     -- updateMin(uint256,uint256) -> 0x5c34a245
     selector := 0x5c34a245
     returns := false }
 
+def exampleEntry24 : EntryPoint :=
+  { name := "capSlot"
+    args := ["slot", "cap"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.lt (Lang.Expr.var "cap") (Lang.Expr.var "current"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "cap"))
+          Lang.Stmt.skip)
+    -- capSlot(uint256,uint256) -> 0x7fdb8622
+    selector := 0x7fdb8622
+    returns := false }
+
 def exampleEntry6 : EntryPoint :=
   { name := "setNonZero"
     args := ["slot", "value"]
@@ -377,9 +390,9 @@ def exampleEntry14 : EntryPoint :=
 
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
-    exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry21, exampleEntry12, exampleEntry20,
-    exampleEntry23, exampleEntry8, exampleEntry9, exampleEntry19, exampleEntry10, exampleEntry11,
-    exampleEntry17, exampleEntry18, exampleEntry13, exampleEntry22, exampleEntry14]
+    exampleEntry16, exampleEntry24, exampleEntry6, exampleEntry7, exampleEntry21, exampleEntry12,
+    exampleEntry20, exampleEntry23, exampleEntry8, exampleEntry9, exampleEntry19, exampleEntry10,
+    exampleEntry11, exampleEntry17, exampleEntry18, exampleEntry13, exampleEntry22, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -44,6 +44,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_updateMin"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0x7fdb8622"
+  , "EQ"
+  , "PUSH2 tag_capSlot"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xac1f1f67"
   , "EQ"
   , "PUSH2 tag_setNonZero"
@@ -299,6 +304,16 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setNonZero:"
   , "STOP"
+  , "tag_capSlot:"
+  , "PUSH2 ret_capSlot"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_capSlot"
+  , "JUMP"
+  , "ret_capSlot:"
+  , "STOP"
   , "tag_updateMin:"
   , "PUSH2 ret_updateMin"
   , "PUSH1 0x24"
@@ -472,34 +487,62 @@ def directProgramAsm : List String :=
   , "PUSH2 updateMax_check"
   , "JUMP"
   , "fn_updateMin:"
-  , "DUP2"
-  , "DUP2"
+  , "SWAP1"
+  , "DUP1"
+  , "DUP3"
   , "SLOAD"
-  , "DUP2"
-  , "DUP2"
+  , "SWAP3"
+  , "DUP4"
+  , "DUP3"
   , "LT"
   , "PUSH2 updateMin_then"
   , "JUMPI"
   , "updateMin_check:"
+  , "POP"
+  , "POP"
   , "LT"
   , "ISZERO"
-  , "PUSH2 updateMin_else"
+  , "PUSH2 updateMin_skip"
   , "JUMPI"
-  , "updateMin_join:"
-  , "POP"
-  , "POP"
+  , "updateMin_out:"
   , "JUMP"
-  , "updateMin_else:"
+  , "updateMin_skip:"
+  , "PUSH2 updateMin_out"
+  , "JUMP"
+  , "updateMin_then:"
   , "SSTORE"
-  , "PUSH0"
   , "DUP1"
-  , "PUSH2 updateMin_join"
+  , "PUSH0"
+  , "PUSH2 updateMin_check"
   , "JUMP"
-  , "updateMin_then:"
+  , "fn_capSlot:"
+  , "SWAP1"
   , "DUP1"
+  , "DUP3"
+  , "SLOAD"
+  , "SWAP3"
   , "DUP4"
+  , "DUP3"
+  , "LT"
+  , "PUSH2 capSlot_then"
+  , "JUMPI"
+  , "capSlot_check:"
+  , "POP"
+  , "POP"
+  , "LT"
+  , "ISZERO"
+  , "PUSH2 capSlot_skip"
+  , "JUMPI"
+  , "capSlot_out:"
+  , "JUMP"
+  , "capSlot_skip:"
+  , "PUSH2 capSlot_out"
+  , "JUMP"
+  , "capSlot_then:"
   , "SSTORE"
-  , "PUSH2 updateMin_check"
+  , "DUP1"
+  , "PUSH0"
+  , "PUSH2 capSlot_check"
   , "JUMP"
   , "fn_setNonZero:"
   , "SWAP1"

research/lean_only_proto/DumbContracts/Examples.lean

@@ -6,6 +6,7 @@ import DumbContracts.Examples.TokenTransfer
 import DumbContracts.Examples.MaxStore
 import DumbContracts.Examples.UpdateMax
 import DumbContracts.Examples.UpdateMin
+import DumbContracts.Examples.CapSlot
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.ClearIfEq

research/lean_only_proto/DumbContracts/Examples/CapSlot.lean

@@ -0,0 +1,37 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Cap a slot to a maximum value without reverting. -/
+
+def capSlotFun : Fun :=
+  { name := "capSlot"
+    args := ["slot", "cap"]
+    body := sstoreIfLt (v "slot") (v "cap")
+    ret := none }
+
+def capSlotSpec (slot cap : Nat) : Spec Store :=
+  { requires := fun _ => True
+    ensures := fun s s' =>
+      s' = updateStore s slot (if s slot > cap then cap else s slot) }
+
+theorem capSlot_meets_spec (s : Store) (slot cap : Nat) :
+    (capSlotSpec slot cap).requires s ->
+    (match execFun capSlotFun [slot, cap] s [] with
+      | ExecResult.ok _ s' => (capSlotSpec slot cap).ensures s s'
+      | _ => False) := by
+  intro _hreq
+  by_cases h : cap < s slot
+  · simp [capSlotFun, capSlotSpec, sstoreIfLt, letSload, v, execFun, execStmt, evalExpr,
+      bindArgs, emptyEnv, updateEnv, updateStore, h]
+  · simp [capSlotFun, capSlotSpec, sstoreIfLt, letSload, v, execFun, execStmt, evalExpr,
+      bindArgs, emptyEnv, updateEnv, updateStore, h]
+
+end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Examples/UpdateMin.lean

@@ -15,8 +15,7 @@ def updateMinFun : Fun :=
   { name := "updateMin"
     args := ["slot", "value"]
     body :=
-      letSload "current" (v "slot")
-        (sstoreMin (v "slot") (v "current") (v "value"))
+      sstoreIfLt (v "slot") (v "value")
     ret := none }
 
 def updateMinSpec (slot value : Nat) : Spec Store :=
@@ -29,10 +28,10 @@ theorem updateMin_meets_spec (s : Store) (slot value : Nat) :
       | ExecResult.ok _ s' => (updateMinSpec slot value).ensures s s'
       | _ => False) := by
   intro _hreq
-  by_cases h : s slot < value
-  · simp [updateMinFun, updateMinSpec, letSload, sstoreMin, v, execFun, execStmt, evalExpr,
+  by_cases h : value < s slot
+  · simp [updateMinFun, updateMinSpec, sstoreIfLt, letSload, v, execFun, execStmt, evalExpr,
       bindArgs, emptyEnv, updateEnv, updateStore, h]
-  · simp [updateMinFun, updateMinSpec, letSload, sstoreMin, v, execFun, execStmt, evalExpr,
+  · simp [updateMinFun, updateMinSpec, sstoreIfLt, letSload, v, execFun, execStmt, evalExpr,
       bindArgs, emptyEnv, updateEnv, updateStore, h]
 
 end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Stdlib.lean

@@ -69,6 +69,13 @@ def sstoreIfEq (slot expected value : Expr) : Stmt :=
 def sstoreIfZero (slot value : Expr) : Stmt :=
   letSload "current" slot (requireZero (Expr.var "current") (Stmt.sstore slot value))
 
+def sstoreIfLt (slot value : Expr) : Stmt :=
+  letSload "current" slot
+    (Stmt.if_
+      (Expr.lt value (Expr.var "current"))
+      (Stmt.sstore slot value)
+      Stmt.skip)
+
 def sstoreAdd (slot delta : Expr) : Stmt :=
   Stmt.sstore slot (Expr.add (Expr.sload slot) delta)
 

research/lean_only_proto/test/GeneratedCapSlot.t.sol

@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedCapSlotTest is GeneratedBase {
+    function testCapSlot() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selSetSlot = 0xf2c298be;
+        bytes4 selCapSlot = 0x7fdb8622;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSetSlot, 5, 20));
+        require(ok, "setSlot failed");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selCapSlot, 5, 15));
+        require(ok, "capSlot failed (cap 15)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 5));
+        require(ok, "getSlot failed (slot 5)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 15, "capSlot did not lower value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selCapSlot, 5, 30));
+        require(ok, "capSlot failed (cap 30)");
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 5));
+        require(ok, "getSlot failed (slot 5, after cap 30)");
+        val = abi.decode(data, (uint256));
+        require(val == 15, "capSlot should not raise value");
+    }
+}