Add sstoreIfGt helper and raiseSlot example

Author: Th0rgal

STATUS.md

@@ -19,10 +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.
+- Iteration: add `sstoreIfGt` helper plus a raise-slot example to avoid redundant writes.
 
 
 ## Recently Done
+- Added `sstoreIfGt` helper, refactored `updateMax`, and added `raiseSlot` example + Foundry test.
 - 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.

docs/research-log.md

@@ -1,6 +1,13 @@
 # Research Log
 
 ## 2026-02-10
+- Added `sstoreIfGt` stdlib helper to avoid redundant stores on monotonic increases.
+- Refactored `updateMax` to use `sstoreIfGt`.
+- Added `raiseSlot` example (raise slot to a floor without reverting) with Spec + proof.
+- Added Foundry test for `raiseSlot`.
+- Updated compiler entries + direct EVM asm wiring for `raiseSlot` and `updateMax`.
+- `end_to_end` initially failed due to cap/raise stub ordering; swapped the `tag_raiseSlot`/`tag_capSlot` order so jumpdest offsets match solc.
+- 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 `requireNonZeroAndLt` stdlib helper for combined nonzero + max guards.
 - Refactored `setIfNonZeroAndLess` to use `requireNonZeroAndLt`.
 - Added `addIfNonZeroAndLess` example (guarded add on `delta != 0` and `delta < max`) with SpecR + proofs.

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -137,9 +137,9 @@ def exampleEntry15 : EntryPoint :=
     body :=
       Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
         (Lang.Stmt.if_
-          (Lang.Expr.gt (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.gt (Lang.Expr.var "value") (Lang.Expr.var "current"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+          Lang.Stmt.skip)
     -- updateMax(uint256,uint256) -> 0xe9cc4edd
     selector := 0xe9cc4edd
     returns := false }
@@ -170,6 +170,19 @@ def exampleEntry24 : EntryPoint :=
     selector := 0x7fdb8622
     returns := false }
 
+def exampleEntry25 : EntryPoint :=
+  { name := "raiseSlot"
+    args := ["slot", "floor"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.gt (Lang.Expr.var "floor") (Lang.Expr.var "current"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "floor"))
+          Lang.Stmt.skip)
+    -- raiseSlot(uint256,uint256) -> 0x84c4b3e1
+    selector := 0x84c4b3e1
+    returns := false }
+
 def exampleEntry6 : EntryPoint :=
   { name := "setNonZero"
     args := ["slot", "value"]
@@ -390,9 +403,10 @@ def exampleEntry14 : EntryPoint :=
 
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
-    exampleEntry16, exampleEntry24, exampleEntry6, exampleEntry7, exampleEntry21, exampleEntry12,
-    exampleEntry20, exampleEntry23, exampleEntry8, exampleEntry9, exampleEntry19, exampleEntry10,
-    exampleEntry11, exampleEntry17, exampleEntry18, exampleEntry13, exampleEntry22, exampleEntry14]
+    exampleEntry16, exampleEntry24, exampleEntry25, 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

@@ -49,6 +49,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_capSlot"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0x84c4b3e1"
+  , "EQ"
+  , "PUSH2 tag_raiseSlot"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xac1f1f67"
   , "EQ"
   , "PUSH2 tag_setNonZero"
@@ -304,6 +309,16 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setNonZero:"
   , "STOP"
+  , "tag_raiseSlot:"
+  , "PUSH2 ret_raiseSlot"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_raiseSlot"
+  , "JUMP"
+  , "ret_raiseSlot:"
+  , "STOP"
   , "tag_capSlot:"
   , "PUSH2 ret_capSlot"
   , "PUSH1 0x24"
@@ -457,33 +472,32 @@ def directProgramAsm : List String :=
   , "PUSH2 maxStore_check"
   , "JUMP"
   , "fn_updateMax:"
-  , "DUP2"
-  , "DUP2"
+  , "SWAP1"
+  , "DUP1"
+  , "DUP3"
   , "SLOAD"
-  , "DUP2"
-  , "DUP2"
+  , "SWAP3"
+  , "DUP4"
+  , "DUP3"
   , "GT"
   , "PUSH2 updateMax_then"
   , "JUMPI"
   , "updateMax_check:"
+  , "POP"
+  , "POP"
   , "GT"
   , "ISZERO"
-  , "PUSH2 updateMax_else"
+  , "PUSH2 updateMax_skip"
   , "JUMPI"
-  , "updateMax_join:"
-  , "POP"
-  , "POP"
+  , "updateMax_out:"
   , "JUMP"
-  , "updateMax_else:"
-  , "SSTORE"
-  , "PUSH0"
-  , "DUP1"
-  , "PUSH2 updateMax_join"
+  , "updateMax_skip:"
+  , "PUSH2 updateMax_out"
   , "JUMP"
   , "updateMax_then:"
-  , "DUP1"
-  , "DUP4"
   , "SSTORE"
+  , "DUP1"
+  , "PUSH0"
   , "PUSH2 updateMax_check"
   , "JUMP"
   , "fn_updateMin:"
@@ -544,6 +558,35 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 capSlot_check"
   , "JUMP"
+  , "fn_raiseSlot:"
+  , "SWAP1"
+  , "DUP1"
+  , "DUP3"
+  , "SLOAD"
+  , "SWAP3"
+  , "DUP4"
+  , "DUP3"
+  , "GT"
+  , "PUSH2 raiseSlot_then"
+  , "JUMPI"
+  , "raiseSlot_check:"
+  , "POP"
+  , "POP"
+  , "GT"
+  , "ISZERO"
+  , "PUSH2 raiseSlot_skip"
+  , "JUMPI"
+  , "raiseSlot_out:"
+  , "JUMP"
+  , "raiseSlot_skip:"
+  , "PUSH2 raiseSlot_out"
+  , "JUMP"
+  , "raiseSlot_then:"
+  , "SSTORE"
+  , "DUP1"
+  , "PUSH0"
+  , "PUSH2 raiseSlot_check"
+  , "JUMP"
   , "fn_setNonZero:"
   , "SWAP1"
   , "DUP1"

research/lean_only_proto/DumbContracts/Examples.lean

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

research/lean_only_proto/DumbContracts/Examples/RaiseSlot.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
+
+/-- Raise a slot to a minimum value without reverting. -/
+
+def raiseSlotFun : Fun :=
+  { name := "raiseSlot"
+    args := ["slot", "floor"]
+    body := sstoreIfGt (v "slot") (v "floor")
+    ret := none }
+
+def raiseSlotSpec (slot floor : Nat) : Spec Store :=
+  { requires := fun _ => True
+    ensures := fun s s' =>
+      s' = updateStore s slot (if floor > s slot then floor else s slot) }
+
+theorem raiseSlot_meets_spec (s : Store) (slot floor : Nat) :
+    (raiseSlotSpec slot floor).requires s ->
+    (match execFun raiseSlotFun [slot, floor] s [] with
+      | ExecResult.ok _ s' => (raiseSlotSpec slot floor).ensures s s'
+      | _ => False) := by
+  intro _hreq
+  by_cases h : floor > s slot
+  · simp [raiseSlotFun, raiseSlotSpec, sstoreIfGt, letSload, v, execFun, execStmt, evalExpr,
+      bindArgs, emptyEnv, updateEnv, updateStore, h]
+  · simp [raiseSlotFun, raiseSlotSpec, sstoreIfGt, letSload, v, execFun, execStmt, evalExpr,
+      bindArgs, emptyEnv, updateEnv, updateStore, h]
+
+end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Examples/UpdateMax.lean

@@ -14,25 +14,23 @@ open DumbContracts.Std
 def updateMaxFun : Fun :=
   { name := "updateMax"
     args := ["slot", "value"]
-    body :=
-      letSload "current" (v "slot")
-        (sstoreMax (v "slot") (v "current") (v "value"))
+    body := sstoreIfGt (v "slot") (v "value")
     ret := none }
 
 def updateMaxSpec (slot value : Nat) : Spec Store :=
   { requires := fun _ => True
-    ensures := fun s s' => s' = updateStore s slot (if s slot > value then s slot else value) }
+    ensures := fun s s' => s' = updateStore s slot (if value > s slot then value else s slot) }
 
 theorem updateMax_meets_spec (s : Store) (slot value : Nat) :
     (updateMaxSpec slot value).requires s ->
     (match execFun updateMaxFun [slot, value] s [] with
       | ExecResult.ok _ s' => (updateMaxSpec slot value).ensures s s'
       | _ => False) := by
   intro _hreq
-  by_cases h : s slot > value
-  · simp [updateMaxFun, updateMaxSpec, letSload, sstoreMax, v, execFun, execStmt, evalExpr,
+  by_cases h : value > s slot
+  · simp [updateMaxFun, updateMaxSpec, sstoreIfGt, letSload, v, execFun, execStmt, evalExpr,
       bindArgs, emptyEnv, updateEnv, updateStore, h]
-  · simp [updateMaxFun, updateMaxSpec, letSload, sstoreMax, v, execFun, execStmt, evalExpr,
+  · simp [updateMaxFun, updateMaxSpec, sstoreIfGt, letSload, v, execFun, execStmt, evalExpr,
       bindArgs, emptyEnv, updateEnv, updateStore, h]
 
 end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Stdlib.lean

@@ -76,6 +76,13 @@ def sstoreIfLt (slot value : Expr) : Stmt :=
       (Stmt.sstore slot value)
       Stmt.skip)
 
+def sstoreIfGt (slot value : Expr) : Stmt :=
+  letSload "current" slot
+    (Stmt.if_
+      (Expr.gt 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/GeneratedRaiseSlot.t.sol

@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedRaiseSlotTest is GeneratedBase {
+    function testRaiseSlot() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selSetSlot = 0xf2c298be;
+        bytes4 selRaiseSlot = 0x84c4b3e1;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSetSlot, 5, 10));
+        require(ok, "setSlot failed");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selRaiseSlot, 5, 20));
+        require(ok, "raiseSlot failed (floor 20)");
+
+        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 == 20, "raiseSlot did not raise value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selRaiseSlot, 5, 5));
+        require(ok, "raiseSlot failed (floor 5)");
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 5));
+        require(ok, "getSlot failed (slot 5, after floor 5)");
+        val = abi.decode(data, (uint256));
+        require(val == 20, "raiseSlot should not lower value");
+    }
+}