Add sstoreMin helper and updateMin example

Author: Th0rgal

STATUS.md

@@ -19,6 +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 a minimal `sstoreMin` helper and a tiny `updateMin` example + Foundry test.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.

docs/research-log.md

@@ -1,6 +1,10 @@
 # Research Log
 
 ## 2026-02-10
+- Added `sstoreMin` stdlib helper to mirror `sstoreMax` for min updates.
+- Added `updateMin` example (monotonic min update against a stored slot) with Spec + proof.
+- Added Foundry test for `updateMin`.
+- Updated compiler entries + direct EVM asm for `updateMin`.
 - Added `sstoreMax` stdlib helper to reduce max-store boilerplate.
 - Refactored `maxStore` to use `sstoreMax`.
 - Added `updateMax` example (monotonic max update against a stored slot) with Spec + proof.

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -144,6 +144,19 @@ def exampleEntry15 : EntryPoint :=
     selector := 0xe9cc4edd
     returns := false }
 
+def exampleEntry16 : EntryPoint :=
+  { name := "updateMin"
+    args := ["slot", "value"]
+    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")))
+    -- updateMin(uint256,uint256) -> 0x5c34a245
+    selector := 0x5c34a245
+    returns := false }
+
 def exampleEntry6 : EntryPoint :=
   { name := "setNonZero"
     args := ["slot", "value"]
@@ -262,8 +275,8 @@ def exampleEntry14 : EntryPoint :=
 
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
-    exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10,
-    exampleEntry11, exampleEntry13, exampleEntry14]
+    exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9,
+    exampleEntry10, exampleEntry11, exampleEntry13, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -39,6 +39,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_updateMax"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0x5c34a245"
+  , "EQ"
+  , "PUSH2 tag_updateMin"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xac1f1f67"
   , "EQ"
   , "PUSH2 tag_setNonZero"
@@ -183,6 +188,16 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setNonZero:"
   , "STOP"
+  , "tag_updateMin:"
+  , "PUSH2 ret_updateMin"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_updateMin"
+  , "JUMP"
+  , "ret_updateMin:"
+  , "STOP"
   , "tag_updateMax:"
   , "PUSH2 ret_updateMax"
   , "PUSH1 0x24"
@@ -345,6 +360,36 @@ def directProgramAsm : List String :=
   , "SSTORE"
   , "PUSH2 updateMax_check"
   , "JUMP"
+  , "fn_updateMin:"
+  , "DUP2"
+  , "DUP2"
+  , "SLOAD"
+  , "DUP2"
+  , "DUP2"
+  , "LT"
+  , "PUSH2 updateMin_then"
+  , "JUMPI"
+  , "updateMin_check:"
+  , "LT"
+  , "ISZERO"
+  , "PUSH2 updateMin_else"
+  , "JUMPI"
+  , "updateMin_join:"
+  , "POP"
+  , "POP"
+  , "JUMP"
+  , "updateMin_else:"
+  , "SSTORE"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH2 updateMin_join"
+  , "JUMP"
+  , "updateMin_then:"
+  , "DUP1"
+  , "DUP4"
+  , "SSTORE"
+  , "PUSH2 updateMin_check"
+  , "JUMP"
   , "fn_setNonZero:"
   , "SWAP1"
   , "DUP1"

research/lean_only_proto/DumbContracts/Examples.lean

@@ -5,6 +5,7 @@ import DumbContracts.Examples.Supply
 import DumbContracts.Examples.TokenTransfer
 import DumbContracts.Examples.MaxStore
 import DumbContracts.Examples.UpdateMax
+import DumbContracts.Examples.UpdateMin
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.InitOnce

research/lean_only_proto/DumbContracts/Examples/UpdateMin.lean

@@ -0,0 +1,38 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Update a slot to the min of its current value and a new input. -/
+
+def updateMinFun : Fun :=
+  { name := "updateMin"
+    args := ["slot", "value"]
+    body :=
+      letSload "current" (v "slot")
+        (sstoreMin (v "slot") (v "current") (v "value"))
+    ret := none }
+
+def updateMinSpec (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) }
+
+theorem updateMin_meets_spec (s : Store) (slot value : Nat) :
+    (updateMinSpec slot value).requires s ->
+    (match execFun updateMinFun [slot, value] s [] with
+      | 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,
+      bindArgs, emptyEnv, updateEnv, updateStore, h]
+  · simp [updateMinFun, updateMinSpec, letSload, sstoreMin, v, execFun, execStmt, evalExpr,
+      bindArgs, emptyEnv, updateEnv, updateStore, h]
+
+end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Stdlib.lean

@@ -60,6 +60,9 @@ def sstoreInc (slot : Expr) : Stmt :=
 def sstoreMax (slot a b : Expr) : Stmt :=
   Stmt.if_ (Expr.gt a b) (Stmt.sstore slot a) (Stmt.sstore slot b)
 
+def sstoreMin (slot a b : Expr) : Stmt :=
+  Stmt.if_ (Expr.lt a b) (Stmt.sstore slot a) (Stmt.sstore slot b)
+
 def sloadSlot (slot : Nat) : Expr :=
   Expr.sload (Expr.lit slot)
 

research/lean_only_proto/test/GeneratedUpdateMin.t.sol

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedUpdateMinTest is GeneratedBase {
+    function testUpdateMin() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selUpdateMin = 0x5c34a245;
+        bytes4 selSet = 0xf2c298be;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 4, 10));
+        require(ok, "setSlot failed (slot 4)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selUpdateMin, 4, 12));
+        require(ok, "updateMin failed on larger value");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 4));
+        require(ok, "getSlot failed (slot 4)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 10, "unexpected updateMin value after larger input");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selUpdateMin, 4, 7));
+        require(ok, "updateMin failed on smaller value");
+
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 4));
+        require(ok, "getSlot failed (slot 4) after update");
+        val = abi.decode(data, (uint256));
+        require(val == 7, "unexpected updateMin value after smaller input");
+    }
+}