Add sstoreIfZero helper and initDouble example

Author: Th0rgal

STATUS.md

@@ -19,9 +19,10 @@ 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 `requireNonZeroAndLt` helper and a tiny `addIfNonZeroAndLess` example + Foundry test.
+ 
 
 ## Recently Done
+- 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.
 - Selector map (fixed + ABI keccak) and Foundry tests.

docs/research-log.md

@@ -110,3 +110,11 @@
 - Added Foundry tests for generated contracts.
 - Compressed docs + tightened minimal frontend.
 - Scanned external tooling landscape (Act, Scribble, Certora, SMTChecker, KEVM/Kontrol, VerX, Move Prover).
+# 2026-02-10
+- Added `sstoreIfZero` stdlib helper to package the common "load + require zero + store" pattern.
+- Refactored `initOnce` and `initToOne` to use `sstoreIfZero`.
+- Added `initDouble` example (initialize to `value * 2` on zero) with SpecR + proofs.
+- Added Foundry test for `initDouble`.
+- 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).

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -220,6 +220,21 @@ def exampleEntry20 : EntryPoint :=
     selector := 0x1ebe7f68
     returns := false }
 
+def exampleEntry23 : EntryPoint :=
+  { name := "initDouble"
+    args := ["slot", "value"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.eq (Lang.Expr.var "current") (Lang.Expr.lit 0))
+          (Lang.Stmt.sstore
+            (Lang.Expr.var "slot")
+            (Lang.Expr.mul (Lang.Expr.var "value") (Lang.Expr.lit 2)))
+          Lang.Stmt.revert)
+    -- initDouble(uint256,uint256) -> 0xa756818e
+    selector := 0xa756818e
+    returns := false }
+
 def exampleEntry8 : EntryPoint :=
   { name := "setIfGreater"
     args := ["slot", "value", "min"]
@@ -363,8 +378,8 @@ def exampleEntry14 : EntryPoint :=
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
     exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry21, exampleEntry12, exampleEntry20,
-    exampleEntry8, exampleEntry9, exampleEntry19, exampleEntry10, exampleEntry11, exampleEntry17,
-    exampleEntry18, exampleEntry13, exampleEntry22, exampleEntry14]
+    exampleEntry23, exampleEntry8, exampleEntry9, exampleEntry19, exampleEntry10, exampleEntry11,
+    exampleEntry17, exampleEntry18, exampleEntry13, exampleEntry22, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -69,6 +69,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_initToOne"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0xa756818e"
+  , "EQ"
+  , "PUSH2 tag_initDouble"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x2dbeb1ba"
   , "EQ"
   , "PUSH2 tag_setIfGreater"
@@ -234,6 +239,16 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setIfGreater:"
   , "STOP"
+  , "tag_initDouble:"
+  , "PUSH2 ret_initDouble"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_initDouble"
+  , "JUMP"
+  , "ret_initDouble:"
+  , "STOP"
   , "tag_initToOne:"
   , "PUSH2 ret_initToOne"
   , "PUSH1 0x04"
@@ -623,6 +638,38 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 initToOne_check"
   , "JUMP"
+  , "fn_initDouble:"
+  , "SWAP1"
+  , "PUSH0"
+  , "SWAP2"
+  , "DUP1"
+  , "SLOAD"
+  , "SWAP2"
+  , "DUP4"
+  , "DUP4"
+  , "EQ"
+  , "PUSH2 initDouble_ok"
+  , "JUMPI"
+  , "initDouble_check:"
+  , "POP"
+  , "POP"
+  , "SUB"
+  , "PUSH2 initDouble_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "initDouble_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "initDouble_ok:"
+  , "PUSH1 0x02"
+  , "MUL"
+  , "SWAP1"
+  , "SSTORE"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH2 initDouble_check"
+  , "JUMP"
   , "fn_setIfGreater:"
   , "DUP2"
   , "SWAP1"

research/lean_only_proto/DumbContracts/Examples.lean

@@ -11,6 +11,7 @@ import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.ClearIfEq
 import DumbContracts.Examples.InitOnce
 import DumbContracts.Examples.InitToOne
+import DumbContracts.Examples.InitDouble
 import DumbContracts.Examples.SetIfGreater
 import DumbContracts.Examples.SetIfAtLeast
 import DumbContracts.Examples.SetIfLess

research/lean_only_proto/DumbContracts/Examples/InitDouble.lean

@@ -0,0 +1,42 @@
+import DumbContracts.Lang
+import DumbContracts.Semantics
+import DumbContracts.Stdlib
+
+namespace DumbContracts.Examples
+
+open DumbContracts.Lang
+open DumbContracts.Semantics
+open DumbContracts
+open DumbContracts.Std
+
+/-- Initialize a slot to double the input if it is currently zero. -/
+
+def initDoubleFun : Fun :=
+  { name := "initDouble"
+    args := ["slot", "value"]
+    body := sstoreIfZero (v "slot") (Expr.mul (v "value") (n 2))
+    ret := none }
+
+def initDoubleSpecR (slot value : Nat) : SpecR Store :=
+  { requires := fun s => s slot = 0
+    ensures := fun s s' => s' = updateStore s slot (value * 2)
+    reverts := fun s => s slot != 0 }
+
+theorem initDouble_meets_specR_ok (s : Store) (slot value : Nat) :
+    (initDoubleSpecR slot value).requires s ->
+    (match execFun initDoubleFun [slot, value] s [] with
+      | ExecResult.ok _ s' => (initDoubleSpecR slot value).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hzero : s slot = 0 := by exact hreq
+  simp [initDoubleSpecR, initDoubleFun, sstoreIfZero, letSload, requireZero, requireEq, eq, require,
+    execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hzero]
+
+theorem initDouble_meets_specR_reverts (s : Store) (slot value : Nat) :
+    (initDoubleSpecR slot value).reverts s ->
+    execFun initDoubleFun [slot, value] s [] = ExecResult.reverted := by
+  intro hrev
+  simp [initDoubleSpecR, initDoubleFun, sstoreIfZero, letSload, requireZero, requireEq, eq, require,
+    execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+
+end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Examples/InitOnce.lean

@@ -14,9 +14,7 @@ open DumbContracts.Std
 def initOnceFun : Fun :=
   { name := "initOnce"
     args := ["slot", "value"]
-    body :=
-      letSload "current" (v "slot")
-        (requireZero (v "current") (sstoreVar "slot" (v "value")))
+    body := sstoreIfZero (v "slot") (v "value")
     ret := none }
 
 def initOnceSpecR (slot value : Nat) : SpecR Store :=
@@ -31,14 +29,14 @@ theorem initOnce_meets_specR_ok (s : Store) (slot value : Nat) :
       | _ => False) := by
   intro hreq
   have hzero : s slot = 0 := by exact hreq
-  simp [initOnceSpecR, initOnceFun, letSload, requireZero, requireEq, eq, require, execFun, execStmt,
-    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hzero]
+  simp [initOnceSpecR, initOnceFun, sstoreIfZero, letSload, requireZero, requireEq, eq, require,
+    execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hzero]
 
 theorem initOnce_meets_specR_reverts (s : Store) (slot value : Nat) :
     (initOnceSpecR slot value).reverts s ->
     execFun initOnceFun [slot, value] s [] = ExecResult.reverted := by
   intro hrev
-  simp [initOnceSpecR, initOnceFun, letSload, requireZero, requireEq, eq, require, execFun, execStmt,
-    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+  simp [initOnceSpecR, initOnceFun, sstoreIfZero, letSload, requireZero, requireEq, eq, require,
+    execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
 
 end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Examples/InitToOne.lean

@@ -14,9 +14,7 @@ open DumbContracts.Std
 def initToOneFun : Fun :=
   { name := "initToOne"
     args := ["slot"]
-    body :=
-      letSload "current" (v "slot")
-        (requireZero (v "current") (sstoreVar "slot" (n 1)))
+    body := sstoreIfZero (v "slot") (n 1)
     ret := none }
 
 def initToOneSpecR (slot : Nat) : SpecR Store :=
@@ -31,14 +29,14 @@ theorem initToOne_meets_specR_ok (s : Store) (slot : Nat) :
       | _ => False) := by
   intro hreq
   have hzero : s slot = 0 := by exact hreq
-  simp [initToOneSpecR, initToOneFun, letSload, requireZero, requireEq, eq, require, execFun,
-    execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hzero]
+  simp [initToOneSpecR, initToOneFun, sstoreIfZero, letSload, requireZero, requireEq, eq, require,
+    execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hzero]
 
 theorem initToOne_meets_specR_reverts (s : Store) (slot : Nat) :
     (initToOneSpecR slot).reverts s ->
     execFun initToOneFun [slot] s [] = ExecResult.reverted := by
   intro hrev
-  simp [initToOneSpecR, initToOneFun, letSload, requireZero, requireEq, eq, require, execFun,
-    execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
+  simp [initToOneSpecR, initToOneFun, sstoreIfZero, letSload, requireZero, requireEq, eq, require,
+    execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
 
 end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Stdlib.lean

@@ -66,6 +66,9 @@ def letSload (name : String) (slot : Expr) (body : Stmt) : Stmt :=
 def sstoreIfEq (slot expected value : Expr) : Stmt :=
   letSload "current" slot (requireEq (Expr.var "current") expected (Stmt.sstore slot value))
 
+def sstoreIfZero (slot value : Expr) : Stmt :=
+  letSload "current" slot (requireZero (Expr.var "current") (Stmt.sstore slot value))
+
 def sstoreAdd (slot delta : Expr) : Stmt :=
   Stmt.sstore slot (Expr.add (Expr.sload slot) delta)
 

research/lean_only_proto/test/GeneratedInitDouble.t.sol

@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedInitDoubleTest is GeneratedBase {
+    function testInitDouble() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selInitDouble = 0xa756818e;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selInitDouble, 12, 7));
+        require(ok, "initDouble failed (first init)");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 12));
+        require(ok, "getSlot failed (slot 12)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 14, "unexpected initDouble value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selInitDouble, 12, 9));
+        require(!ok, "initDouble should revert when slot already set");
+    }
+}