Add requireZero helper and initToOne 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 `requireGte` helper and a tiny `setIfAtLeast` example + Foundry test.
+- Iteration: add `requireZero` helper and a tiny `initToOne` example + Foundry test.
 
 ## Recently Done
+- 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.
 - Spec-style wrappers for storage and Euler-style risk examples.

docs/research-log.md

@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `requireZero` stdlib helper for zero guards.
+- Refactored `initOnce` to use `requireZero`.
+- Added `initToOne` example (initialize slot to `1` when empty) with SpecR + proofs.
+- Added Foundry test for `initToOne`.
+- Updated compiler entries + direct EVM asm for `initToOne`.
 - Added `requireGte` stdlib helper for `>=` guards (via `not lt`).
 - Refactored `subIfEnough` to use `requireGte`.
 - Added `setIfAtLeast` example (guarded store on `value >= min`) with SpecR + proofs.

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -194,6 +194,19 @@ def exampleEntry12 : EntryPoint :=
     selector := 0xd3b9b05a
     returns := false }
 
+def exampleEntry20 : EntryPoint :=
+  { name := "initToOne"
+    args := ["slot"]
+    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.lit 1))
+          Lang.Stmt.revert)
+    -- initToOne(uint256) -> 0x1ebe7f68
+    selector := 0x1ebe7f68
+    returns := false }
+
 def exampleEntry8 : EntryPoint :=
   { name := "setIfGreater"
     args := ["slot", "value", "min"]
@@ -320,9 +333,9 @@ def exampleEntry14 : EntryPoint :=
 
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
-    exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry8, exampleEntry9,
-    exampleEntry19, exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18, exampleEntry13,
-    exampleEntry14]
+    exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry20, exampleEntry8,
+    exampleEntry9, exampleEntry19, exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18,
+    exampleEntry13, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -59,6 +59,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_initOnce"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0x1ebe7f68"
+  , "EQ"
+  , "PUSH2 tag_initToOne"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x2dbeb1ba"
   , "EQ"
   , "PUSH2 tag_setIfGreater"
@@ -207,6 +212,14 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_setIfGreater:"
   , "STOP"
+  , "tag_initToOne:"
+  , "PUSH2 ret_initToOne"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_initToOne"
+  , "JUMP"
+  , "ret_initToOne:"
+  , "STOP"
   , "tag_initOnce:"
   , "PUSH2 ret_initOnce"
   , "PUSH1 0x24"
@@ -524,6 +537,34 @@ def directProgramAsm : List String :=
   , "DUP1"
   , "PUSH2 initOnce_check"
   , "JUMP"
+  , "fn_initToOne:"
+  , "PUSH0"
+  , "SWAP1"
+  , "DUP1"
+  , "SLOAD"
+  , "SWAP1"
+  , "DUP3"
+  , "DUP3"
+  , "EQ"
+  , "PUSH2 initToOne_ok"
+  , "JUMPI"
+  , "initToOne_check:"
+  , "POP"
+  , "SUB"
+  , "PUSH2 initToOne_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "initToOne_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "initToOne_ok:"
+  , "PUSH1 0x01"
+  , "SWAP1"
+  , "SSTORE"
+  , "PUSH0"
+  , "PUSH2 initToOne_check"
+  , "JUMP"
   , "fn_setIfGreater:"
   , "DUP2"
   , "SWAP1"

research/lean_only_proto/DumbContracts/Examples.lean

@@ -9,6 +9,7 @@ import DumbContracts.Examples.UpdateMin
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
 import DumbContracts.Examples.InitOnce
+import DumbContracts.Examples.InitToOne
 import DumbContracts.Examples.SetIfGreater
 import DumbContracts.Examples.SetIfAtLeast
 import DumbContracts.Examples.SetIfLess

research/lean_only_proto/DumbContracts/Examples/InitOnce.lean

@@ -16,7 +16,7 @@ def initOnceFun : Fun :=
     args := ["slot", "value"]
     body :=
       letSload "current" (v "slot")
-        (requireEq (v "current") (n 0) (sstoreVar "slot" (v "value")))
+        (requireZero (v "current") (sstoreVar "slot" (v "value")))
     ret := none }
 
 def initOnceSpecR (slot value : Nat) : SpecR Store :=
@@ -31,14 +31,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, requireEq, eq, require, execFun, execStmt,
+  simp [initOnceSpecR, initOnceFun, 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, requireEq, eq, require, execFun, execStmt,
+  simp [initOnceSpecR, initOnceFun, letSload, requireZero, requireEq, eq, require, execFun, execStmt,
     evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, hrev]
 
 end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Examples/InitToOne.lean

@@ -0,0 +1,44 @@
+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 1 if it is currently zero. -/
+
+def initToOneFun : Fun :=
+  { name := "initToOne"
+    args := ["slot"]
+    body :=
+      letSload "current" (v "slot")
+        (requireZero (v "current") (sstoreVar "slot" (n 1)))
+    ret := none }
+
+def initToOneSpecR (slot : Nat) : SpecR Store :=
+  { requires := fun s => s slot = 0
+    ensures := fun s s' => s' = updateStore s slot 1
+    reverts := fun s => s slot != 0 }
+
+theorem initToOne_meets_specR_ok (s : Store) (slot : Nat) :
+    (initToOneSpecR slot).requires s ->
+    (match execFun initToOneFun [slot] s [] with
+      | ExecResult.ok _ s' => (initToOneSpecR slot).ensures s s'
+      | _ => 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]
+
+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]
+
+end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Stdlib.lean

@@ -52,6 +52,9 @@ def requireBetween (value lo hi : Expr) (body : Stmt) : Stmt :=
 def requireNonZero (value : Expr) (body : Stmt) : Stmt :=
   requireNeq value (Expr.lit 0) body
 
+def requireZero (value : Expr) (body : Stmt) : Stmt :=
+  requireEq value (Expr.lit 0) body
+
 /-- Shorthand for loading/storing fixed slots. -/
 
 def letSload (name : String) (slot : Expr) (body : Stmt) : Stmt :=

research/lean_only_proto/test/GeneratedInitToOne.t.sol

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