Add sstoreIfEq helper and clearIfEq example

Author: Th0rgal

STATUS.md

@@ -19,7 +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 `requireZero` helper and a tiny `initToOne` example + Foundry test.
+- Iteration: add `sstoreIfEq` helper and a tiny `clearIfEq` example + Foundry test.
 
 ## Recently Done
 - Added `requireZero` helper and an `initToOne` example + Foundry test.

docs/research-log.md

@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `sstoreIfEq` stdlib helper for guarded stores on slot equality.
+- Refactored `compareAndSwap` to use `sstoreIfEq`.
+- Added `clearIfEq` example (clear slot when it matches expected) with SpecR + proofs.
+- Added Foundry test for `clearIfEq`.
+- Updated compiler entries + direct EVM asm for `clearIfEq`.
 - Added `requireZero` stdlib helper for zero guards.
 - Refactored `initOnce` to use `requireZero`.
 - Added `initToOne` example (initialize slot to `1` when empty) with SpecR + proofs.

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -181,6 +181,19 @@ def exampleEntry7 : EntryPoint :=
     selector := 0xc74962fa
     returns := false }
 
+def exampleEntry21 : EntryPoint :=
+  { name := "clearIfEq"
+    args := ["slot", "expected"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.eq (Lang.Expr.var "current") (Lang.Expr.var "expected"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.lit 0))
+          Lang.Stmt.revert)
+    -- clearIfEq(uint256,uint256) -> 0xb41535b4
+    selector := 0xb41535b4
+    returns := false }
+
 def exampleEntry12 : EntryPoint :=
   { name := "initOnce"
     args := ["slot", "value"]
@@ -333,9 +346,9 @@ def exampleEntry14 : EntryPoint :=
 
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
-    exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry20, exampleEntry8,
-    exampleEntry9, exampleEntry19, exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18,
-    exampleEntry13, exampleEntry14]
+    exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry21, exampleEntry12, exampleEntry20,
+    exampleEntry8, exampleEntry9, exampleEntry19, exampleEntry10, exampleEntry11, exampleEntry17,
+    exampleEntry18, exampleEntry13, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -54,6 +54,11 @@ def directProgramAsm : List String :=
   , "PUSH2 tag_compareAndSwap"
   , "JUMPI"
   , "DUP1"
+  , "PUSH4 0xb41535b4"
+  , "EQ"
+  , "PUSH2 tag_clearIfEq"
+  , "JUMPI"
+  , "DUP1"
   , "PUSH4 0xd3b9b05a"
   , "EQ"
   , "PUSH2 tag_initOnce"
@@ -230,6 +235,16 @@ def directProgramAsm : List String :=
   , "JUMP"
   , "ret_initOnce:"
   , "STOP"
+  , "tag_clearIfEq:"
+  , "PUSH2 ret_clearIfEq"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_clearIfEq"
+  , "JUMP"
+  , "ret_clearIfEq:"
+  , "STOP"
   , "tag_compareAndSwap:"
   , "PUSH2 ret_compareAndSwap"
   , "PUSH1 0x44"
@@ -509,6 +524,32 @@ def directProgramAsm : List String :=
   , "DUP1"
   , "PUSH2 compareAndSwap_check"
   , "JUMP"
+  , "fn_clearIfEq:"
+  , "DUP1"
+  , "SLOAD"
+  , "SWAP1"
+  , "DUP3"
+  , "DUP3"
+  , "EQ"
+  , "PUSH2 clearIfEq_ok"
+  , "JUMPI"
+  , "clearIfEq_check:"
+  , "POP"
+  , "SUB"
+  , "PUSH2 clearIfEq_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "clearIfEq_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "clearIfEq_ok:"
+  , "PUSH0"
+  , "SWAP1"
+  , "SSTORE"
+  , "PUSH0"
+  , "PUSH2 clearIfEq_check"
+  , "JUMP"
   , "fn_initOnce:"
   , "PUSH0"
   , "SWAP2"

research/lean_only_proto/DumbContracts/Examples.lean

@@ -8,6 +8,7 @@ import DumbContracts.Examples.UpdateMax
 import DumbContracts.Examples.UpdateMin
 import DumbContracts.Examples.NonZeroStore
 import DumbContracts.Examples.CompareAndSwap
+import DumbContracts.Examples.ClearIfEq
 import DumbContracts.Examples.InitOnce
 import DumbContracts.Examples.InitToOne
 import DumbContracts.Examples.SetIfGreater

research/lean_only_proto/DumbContracts/Examples/ClearIfEq.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
+
+/-- Clear a slot (store 0) only if it matches an expected value. -/
+
+def clearIfEqFun : Fun :=
+  { name := "clearIfEq"
+    args := ["slot", "expected"]
+    body := sstoreIfEq (v "slot") (v "expected") (n 0)
+    ret := none }
+
+def clearIfEqSpecR (slot expected : Nat) : SpecR Store :=
+  { requires := fun s => s slot = expected
+    ensures := fun s s' => s' = updateStore s slot 0
+    reverts := fun s => s slot != expected }
+
+theorem clearIfEq_meets_specR_ok (s : Store) (slot expected : Nat) :
+    (clearIfEqSpecR slot expected).requires s ->
+    (match execFun clearIfEqFun [slot, expected] s [] with
+      | ExecResult.ok _ s' => (clearIfEqSpecR slot expected).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hmatch : s slot = expected := by exact hreq
+  simp [clearIfEqSpecR, clearIfEqFun, sstoreIfEq, requireEq, eq, require, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, letSload, hmatch]
+
+theorem clearIfEq_meets_specR_reverts (s : Store) (slot expected : Nat) :
+    (clearIfEqSpecR slot expected).reverts s ->
+    execFun clearIfEqFun [slot, expected] s [] = ExecResult.reverted := by
+  intro hrev
+  simp [clearIfEqSpecR, clearIfEqFun, sstoreIfEq, requireEq, eq, require, execFun, execStmt,
+    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, letSload, hrev]
+
+end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Examples/CompareAndSwap.lean

@@ -14,9 +14,7 @@ open DumbContracts.Std
 def compareAndSwapFun : Fun :=
   { name := "compareAndSwap"
     args := ["slot", "expected", "value"]
-    body :=
-      letSload "current" (v "slot")
-        (requireEq (v "current") (v "expected") (sstoreVar "slot" (v "value")))
+    body := sstoreIfEq (v "slot") (v "expected") (v "value")
     ret := none }
 
 def compareAndSwapSpecR (slot expected value : Nat) : SpecR Store :=
@@ -31,14 +29,14 @@ theorem compareAndSwap_meets_specR_ok (s : Store) (slot expected value : Nat) :
       | _ => False) := by
   intro hreq
   have hmatch : s slot = expected := by exact hreq
-  simp [compareAndSwapSpecR, compareAndSwapFun, requireEq, eq, require, execFun, execStmt,
-    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, letSload, hmatch]
+  simp [compareAndSwapSpecR, compareAndSwapFun, sstoreIfEq, requireEq, eq, require, execFun,
+    execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, letSload, hmatch]
 
 theorem compareAndSwap_meets_specR_reverts (s : Store) (slot expected value : Nat) :
     (compareAndSwapSpecR slot expected value).reverts s ->
     execFun compareAndSwapFun [slot, expected, value] s [] = ExecResult.reverted := by
   intro hrev
-  simp [compareAndSwapSpecR, compareAndSwapFun, requireEq, eq, require, execFun, execStmt,
-    evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, letSload, hrev]
+  simp [compareAndSwapSpecR, compareAndSwapFun, sstoreIfEq, requireEq, eq, require, execFun,
+    execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, letSload, hrev]
 
 end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Stdlib.lean

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

research/lean_only_proto/test/GeneratedClearIfEq.t.sol

@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedClearIfEqTest is GeneratedBase {
+    function testClearIfEq() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selGet = 0x7eba7ba6;
+        bytes4 selSet = 0xf2c298be;
+        bytes4 selClear = 0xb41535b4;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 22, 55));
+        require(ok, "setSlot failed");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selClear, 22, 55));
+        require(ok, "clearIfEq should succeed");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 22));
+        require(ok, "getSlot failed");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 0, "unexpected clearIfEq value");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selClear, 22, 7));
+        require(!ok, "clearIfEq should revert on mismatch");
+    }
+}