Add sstoreInc helper and bumpIfNonZero 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 `requireAnd` helper plus a `setIfNonZeroAndLess` example to reduce nested guard boilerplate.
+- Iteration: add `sstoreInc` helper plus a `bumpIfNonZero` example to reduce increment boilerplate with guards.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.

docs/research-log.md

@@ -1,6 +1,11 @@
 # Research Log
 
 ## 2026-02-10
+- Added `sstoreInc` stdlib helper to increment a slot without repeating `add` boilerplate.
+- Refactored `bumpSlot` to use `sstoreInc`.
+- Added `bumpIfNonZero` example (guarded increment when slot is nonzero) with SpecR + proofs.
+- Added Foundry test for `bumpIfNonZero`.
+- Updated compiler entries + direct EVM asm for `bumpIfNonZero`.
 - Added `requireAnd` stdlib helper to combine guard conditions cleanly.
 - Refactored `setIfBetween` to use `requireAnd` instead of nested guards.
 - Added `setIfNonZeroAndLess` example (nonzero + max guard) with SpecR + proofs.

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -232,9 +232,25 @@ def exampleEntry13 : EntryPoint :=
     selector := 0x8ba43d8f
     returns := false }
 
+def exampleEntry14 : EntryPoint :=
+  { name := "bumpIfNonZero"
+    args := ["slot"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.not
+          (Lang.Expr.eq (Lang.Expr.sload (Lang.Expr.var "slot")) (Lang.Expr.lit 0)))
+        (Lang.Stmt.sstore
+          (Lang.Expr.var "slot")
+          (Lang.Expr.add (Lang.Expr.sload (Lang.Expr.var "slot")) (Lang.Expr.lit 1)))
+        Lang.Stmt.revert
+    -- bumpIfNonZero(uint256) -> 0xc2311456
+    selector := 0xc2311456
+    returns := false }
+
 def exampleEntries : List EntryPoint :=
   [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry6, exampleEntry7,
-    exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11, exampleEntry13]
+    exampleEntry12, exampleEntry8, exampleEntry9, exampleEntry10, exampleEntry11, exampleEntry13,
+    exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -68,13 +68,26 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH2 tag_setIfBetween"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x8ba43d8f"
   , "EQ"
   , "PUSH2 tag_setIfNonZeroAndLess"
   , "JUMPI"
+  , "PUSH4 0xc2311456"
+  , "EQ"
+  , "PUSH2 tag_bumpIfNonZero"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_bumpIfNonZero:"
+  , "PUSH2 ret_bumpIfNonZero"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH2 fn_bumpIfNonZero"
+  , "JUMP"
+  , "ret_bumpIfNonZero:"
+  , "STOP"
   , "tag_setIfNonZeroAndLess:"
   , "PUSH2 ret_setIfNonZeroAndLess"
   , "PUSH1 0x44"
@@ -518,6 +531,34 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH2 setIfNonZeroAndLess_check"
   , "JUMP"
+  , "fn_bumpIfNonZero:"
+  , "PUSH0"
+  , "SWAP1"
+  , "DUP2"
+  , "DUP2"
+  , "SLOAD"
+  , "SUB"
+  , "PUSH2 bumpIfNonZero_ok"
+  , "JUMPI"
+  , "bumpIfNonZero_check:"
+  , "SLOAD"
+  , "EQ"
+  , "PUSH2 bumpIfNonZero_revert"
+  , "JUMPI"
+  , "JUMP"
+  , "bumpIfNonZero_revert:"
+  , "PUSH0"
+  , "DUP1"
+  , "REVERT"
+  , "bumpIfNonZero_ok:"
+  , "PUSH1 0x01"
+  , "DUP2"
+  , "SLOAD"
+  , "ADD"
+  , "DUP2"
+  , "SSTORE"
+  , "PUSH2 bumpIfNonZero_check"
+  , "JUMP"
   ]
 
 def pretty (lines : List String) : String :=

research/lean_only_proto/DumbContracts/Examples.lean

@@ -12,3 +12,4 @@ import DumbContracts.Examples.SetIfLess
 import DumbContracts.Examples.SetIfBetween
 import DumbContracts.Examples.SetIfNonZeroAndLess
 import DumbContracts.Examples.BumpSlot
+import DumbContracts.Examples.BumpIfNonZero

research/lean_only_proto/DumbContracts/Examples/BumpIfNonZero.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
+
+/-- Increment a slot by one, but only if it is already non-zero. -/
+
+def bumpIfNonZeroFun : Fun :=
+  { name := "bumpIfNonZero"
+    args := ["slot"]
+    body := requireNonZero (Expr.sload (v "slot")) (sstoreInc (v "slot"))
+    ret := none }
+
+def bumpIfNonZeroSpecR (slot : Nat) : SpecR Store :=
+  { requires := fun s => s slot != 0
+    ensures := fun s s' => s' = updateStore s slot (s slot + 1)
+    reverts := fun s => s slot = 0 }
+
+theorem bumpIfNonZero_meets_specR_ok (s : Store) (slot : Nat) :
+    (bumpIfNonZeroSpecR slot).requires s ->
+    (match execFun bumpIfNonZeroFun [slot] s [] with
+      | ExecResult.ok _ s' => (bumpIfNonZeroSpecR slot).ensures s s'
+      | _ => False) := by
+  intro hreq
+  have hnonzero : s slot != 0 := by exact hreq
+  simp [bumpIfNonZeroSpecR, bumpIfNonZeroFun, requireNonZero, requireNeq, neq, eq, require, sstoreInc,
+    sstoreAdd, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, v, n, hnonzero]
+
+theorem bumpIfNonZero_meets_specR_reverts (s : Store) (slot : Nat) :
+    (bumpIfNonZeroSpecR slot).reverts s ->
+    execFun bumpIfNonZeroFun [slot] s [] = ExecResult.reverted := by
+  intro hrev
+  simp [bumpIfNonZeroSpecR, bumpIfNonZeroFun, requireNonZero, requireNeq, neq, eq, require, sstoreInc,
+    sstoreAdd, execFun, execStmt, evalExpr, bindArgs, emptyEnv, updateEnv, updateStore, v, n, hrev]
+
+end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Examples/BumpSlot.lean

@@ -14,7 +14,7 @@ open DumbContracts.Std
 def bumpSlotFun : Fun :=
   { name := "bumpSlot"
     args := ["slot"]
-    body := sstoreAdd (v "slot") (n 1)
+    body := sstoreInc (v "slot")
     ret := none }
 
 def bumpSlotSpec (slot : Nat) : Spec Store :=
@@ -27,7 +27,7 @@ theorem bumpSlot_meets_spec (s : Store) (slot : Nat) :
       | ExecResult.ok _ s' => (bumpSlotSpec slot).ensures s s'
       | _ => False) := by
   intro _hreq
-  simp [bumpSlotSpec, bumpSlotFun, sstoreAdd, execFun, execStmt, evalExpr,
+  simp [bumpSlotSpec, bumpSlotFun, sstoreInc, sstoreAdd, execFun, execStmt, evalExpr,
     bindArgs, emptyEnv, updateEnv, updateStore, v, n]
 
 end DumbContracts.Examples

research/lean_only_proto/DumbContracts/Stdlib.lean

@@ -54,6 +54,9 @@ def letSload (name : String) (slot : Expr) (body : Stmt) : Stmt :=
 def sstoreAdd (slot delta : Expr) : Stmt :=
   Stmt.sstore slot (Expr.add (Expr.sload slot) delta)
 
+def sstoreInc (slot : Expr) : Stmt :=
+  sstoreAdd slot (Expr.lit 1)
+
 def sloadSlot (slot : Nat) : Expr :=
   Expr.sload (Expr.lit slot)
 

research/lean_only_proto/test/GeneratedBumpIfNonZero.t.sol

@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import "./GeneratedBase.t.sol";
+
+contract GeneratedBumpIfNonZeroTest is GeneratedBase {
+    function testBumpIfNonZero() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selBumpIfNonZero = 0xc2311456;
+        bytes4 selSet = 0xf2c298be;
+        bytes4 selGet = 0x7eba7ba6;
+
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selSet, 3, 9));
+        require(ok, "setSlot failed (slot 3)");
+
+        (ok,) = deployed.call(abi.encodeWithSelector(selBumpIfNonZero, 3));
+        require(ok, "bumpIfNonZero failed");
+
+        bytes memory data;
+        (ok, data) = deployed.call(abi.encodeWithSelector(selGet, 3));
+        require(ok, "getSlot failed (slot 3)");
+        uint256 val = abi.decode(data, (uint256));
+        require(val == 10, "unexpected bumpIfNonZero value");
+    }
+
+    function testBumpIfNonZeroRevertsOnZero() public {
+        bytes memory creation = _readHexFile("out/example.creation.bin");
+        address deployed = _deploy(creation);
+
+        bytes4 selBumpIfNonZero = 0xc2311456;
+        (bool ok,) = deployed.call(abi.encodeWithSelector(selBumpIfNonZero, 11));
+        require(!ok, "expected bumpIfNonZero revert on zero slot");
+    }
+}