Wip/edsl maxstore stdlib

STATUS.md

@@ -1,6 +1,6 @@
 # Status
 
-Last updated: 2026-02-09
+Last updated: 2026-02-10
 
 ## Current Focus
 - Lean-only specs + implementations + proofs.
@@ -19,8 +19,10 @@ Last updated: 2026-02-09
 - 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.
 
 ## 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.
@@ -43,6 +45,14 @@ Last updated: 2026-02-09
 - Added a minimal EDSL stdlib (`require`, `unless`, `assert`, `sloadSlot`, `sstoreSlot`, `v`, `n`) to reduce syntax noise.
 - Added `sloadVar`/`sstoreVar` helpers to cut boilerplate when using variable slots.
 - Added a `maxStore` example (stores max(a,b) into a slot) plus selector + Foundry test.
+- Added a `requireNonZero` helper and a tiny `setNonZero` example + Foundry test.
+- Aligned direct EVM asm with solc for `setNonZero` (label pushes use `PUSH2`).
+- Added `requireEq`/`requireNeq` helpers plus a `compareAndSwap` example + Foundry test.
+- Added `requireGt` helper plus a `setIfGreater` example + Foundry test (and refactored guarded add to use it).
+- Added `sstoreAdd` helper plus a `bumpSlot` example + Foundry test (and refactored add-slot examples to use it).
+- Added `sstoreMax` helper plus an `updateMax` example + Foundry test (monotonic max update).
+- Added a `revertIf` helper, refactored `checkHealth`, and added a `setIfLess` example + Foundry test.
+- Updated compiler entries + direct EVM asm for `setIfLess`.
 - Minimal docs frontend and compressed docs.
 - Further docs tightening (shorter guide + text).
 - External landscape scan (spec languages, model checkers, prover stacks).

docs/research-log.md

@@ -1,5 +1,76 @@
 # 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.
+- Added Foundry test for `setIfAtLeast`.
+- Updated compiler entries + direct EVM asm for `setIfAtLeast`.
+- Added `sstoreSub` stdlib helper for slot decrements.
+- Refactored `transfer` to use `sstoreSub` for balance subtraction.
+- Added `subIfEnough` example (guarded decrement when slot >= delta) with SpecR + proofs.
+- Added Foundry test for `subIfEnough`.
+- Updated compiler entries + direct EVM asm for `subIfEnough`.
+- Added `requireBetween` stdlib helper for strict range guards.
+- Refactored `setIfBetween` to use `requireBetween`.
+- Added `addIfBetween` example (guarded add on `min < delta < max`) with SpecR + proofs.
+- Added Foundry test for `addIfBetween`.
+- Updated compiler entries + direct EVM asm for `addIfBetween`.
+- 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.
+- Added Foundry test for `updateMax`.
+- Updated compiler entries + direct EVM asm for `updateMax`.
+- 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.
+- Added Foundry test for `setIfNonZeroAndLess`.
+- Updated compiler entries + direct EVM asm for `setIfNonZeroAndLess`.
+- Added `letSload` stdlib helper for caching a slot read via `let_`.
+- Refactored `compareAndSwap` to use `letSload`.
+- Added `initOnce` example (only initialize a zero slot) with SpecR + proofs.
+- Added Foundry test for `initOnce`.
+- Updated compiler entries + direct EVM asm for `initOnce`.
+- Added `requireLt` stdlib helper to mirror `requireGt` for less-than guards.
+- Refactored `setIfLess` to use `requireLt` instead of a manual `revertIf`.
+- Added `setIfBetween` example (guarded store on `min < value < max`) with SpecR + proofs.
+- Added Foundry test for `setIfBetween`.
+- Updated compiler entries + direct EVM asm for `setIfBetween`.
+- Added `revertIf` stdlib helper for guard-style reverts.
+- Refactored `checkHealth` to use `revertIf`.
+- Added `setIfLess` example (guarded store on `value < max`) with SpecR + proofs.
+- Added Foundry test for `setIfLess`.
+- Updated compiler entries + direct EVM asm for `setIfLess`.
+- Added `sstoreAdd` stdlib helper to make slot increments less noisy.
+- Added `bumpSlot` example (increment slot by one) with a basic Spec + proof.
+- Refactored `addSlot` and `guardedAddSlot` to use `sstoreAdd`.
+- Added Foundry test for `bumpSlot`.
+- Updated compiler entries + direct EVM asm for `bumpSlot`.
+- Added `requireGt` stdlib helper to reduce guard boilerplate.
+- Added `setIfGreater` example (guarded store on `value > min`) with SpecR + proofs.
+- Refactored `guardedAddSlot` to use `requireGt`.
+- Added Foundry test for `setIfGreater`.
+- Added `eq`/`neq` plus `requireEq`/`requireNeq` stdlib helpers.
+- Added `compareAndSwap` example (guarded store on expected value match) with SpecR and proofs.
+- Avoided double `sload` in `compareAndSwap` by caching the slot value with `let_` (prevents false reverts).
+- Refactored `setNonZero` to use the new `requireNeq` helper.
+- Updated compiler entries + direct EVM asm for `compareAndSwap`.
+- Added Foundry test for `compareAndSwap`.
+
 ## 2026-02-09
 - Added spec-style wrappers for storage and risk examples.
 - Added `SpecR` (specs with explicit revert predicates) and proofs.
@@ -21,6 +92,8 @@
 - Added a minimal EDSL stdlib with common helpers (`require`, `unless`, `assert`, slot helpers, var/lit helpers).
 - Added `sloadVar`/`sstoreVar` stdlib helpers for variable slot access.
 - Added a tiny `maxStore` example (store max(a,b) into a slot) plus selector + Foundry test.
+- Added a `requireNonZero` helper plus a tiny `setNonZero` example + Foundry test.
+- Updated direct EVM asm to include `setNonZero` and force label pushes to `PUSH2` so bytecode matches solc output.
 - Refreshed external landscape notes (Act, Scribble, Certora, SMTChecker, KEVM, Kontrol).
 - Added selector map artifact (fixed + ABI keccak).
 - Fixed Foundry selectors and moved to Shanghai EVM.

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -131,8 +131,211 @@ def exampleEntry5 : EntryPoint :=
     selector := 0xb61d4088
     returns := false }
 
+def exampleEntry15 : EntryPoint :=
+  { name := "updateMax"
+    args := ["slot", "value"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.gt (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")))
+    -- updateMax(uint256,uint256) -> 0xe9cc4edd
+    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"]
+    body := Lang.Stmt.if_
+      (Lang.Expr.not (Lang.Expr.eq (Lang.Expr.var "value") (Lang.Expr.lit 0)))
+      (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+      Lang.Stmt.revert
+    -- setNonZero(uint256,uint256) -> 0xac1f1f67
+    selector := 0xac1f1f67
+    returns := false }
+
+def exampleEntry7 : EntryPoint :=
+  { name := "compareAndSwap"
+    args := ["slot", "expected", "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.var "expected"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+          Lang.Stmt.revert)
+    -- compareAndSwap(uint256,uint256,uint256) -> 0xc74962fa
+    selector := 0xc74962fa
+    returns := false }
+
+def exampleEntry12 : EntryPoint :=
+  { name := "initOnce"
+    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.var "value"))
+          Lang.Stmt.revert)
+    -- initOnce(uint256,uint256) -> 0xd3b9b05a
+    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"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.gt (Lang.Expr.var "value") (Lang.Expr.var "min"))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfGreater(uint256,uint256,uint256) -> 0x2dbeb1ba
+    selector := 0x2dbeb1ba
+    returns := false }
+
+def exampleEntry19 : EntryPoint :=
+  { name := "setIfAtLeast"
+    args := ["slot", "value", "min"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.not (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "min")))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfAtLeast(uint256,uint256,uint256) -> 0x407cdd03
+    selector := 0x407cdd03
+    returns := false }
+
+def exampleEntry9 : EntryPoint :=
+  { name := "bumpSlot"
+    args := ["slot"]
+    body :=
+      Lang.Stmt.sstore
+        (Lang.Expr.var "slot")
+        (Lang.Expr.add (Lang.Expr.sload (Lang.Expr.var "slot")) (Lang.Expr.lit 1))
+    -- bumpSlot(uint256) -> 0xb8df0e12
+    selector := 0xb8df0e12
+    returns := false }
+
+def exampleEntry10 : EntryPoint :=
+  { name := "setIfLess"
+    args := ["slot", "value", "max"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "max"))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfLess(uint256,uint256,uint256) -> 0x7e5acdb6
+    selector := 0x7e5acdb6
+    returns := false }
+
+def exampleEntry11 : EntryPoint :=
+  { name := "setIfBetween"
+    args := ["slot", "value", "min", "max"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.gt (Lang.Expr.var "value") (Lang.Expr.var "min"))
+        (Lang.Stmt.if_
+          (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "max"))
+          (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+          Lang.Stmt.revert)
+        Lang.Stmt.revert
+    -- setIfBetween(uint256,uint256,uint256,uint256) -> 0x5ebc58db
+    selector := 0x5ebc58db
+    returns := false }
+
+def exampleEntry17 : EntryPoint :=
+  { name := "addIfBetween"
+    args := ["slot", "delta", "min", "max"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.gt (Lang.Expr.var "delta") (Lang.Expr.var "min"))
+        (Lang.Stmt.if_
+          (Lang.Expr.lt (Lang.Expr.var "delta") (Lang.Expr.var "max"))
+          (Lang.Stmt.sstore
+            (Lang.Expr.var "slot")
+            (Lang.Expr.add (Lang.Expr.sload (Lang.Expr.var "slot")) (Lang.Expr.var "delta")))
+          Lang.Stmt.revert)
+        Lang.Stmt.revert
+    -- addIfBetween(uint256,uint256,uint256,uint256) -> 0xbc0fcb79
+    selector := 0xbc0fcb79
+    returns := false }
+
+def exampleEntry18 : EntryPoint :=
+  { name := "subIfEnough"
+    args := ["slot", "delta"]
+    body :=
+      Lang.Stmt.let_ "current" (Lang.Expr.sload (Lang.Expr.var "slot"))
+        (Lang.Stmt.if_
+          (Lang.Expr.not
+            (Lang.Expr.lt (Lang.Expr.var "current") (Lang.Expr.var "delta")))
+          (Lang.Stmt.sstore
+            (Lang.Expr.var "slot")
+            (Lang.Expr.sub (Lang.Expr.var "current") (Lang.Expr.var "delta")))
+          Lang.Stmt.revert)
+    -- subIfEnough(uint256,uint256) -> 0x9ee7809e
+    selector := 0x9ee7809e
+    returns := false }
+
+def exampleEntry13 : EntryPoint :=
+  { name := "setIfNonZeroAndLess"
+    args := ["slot", "value", "max"]
+    body :=
+      Lang.Stmt.if_
+        (Lang.Expr.and
+          (Lang.Expr.not (Lang.Expr.eq (Lang.Expr.var "value") (Lang.Expr.lit 0)))
+          (Lang.Expr.lt (Lang.Expr.var "value") (Lang.Expr.var "max")))
+        (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "value"))
+        Lang.Stmt.revert
+    -- setIfNonZeroAndLess(uint256,uint256,uint256) -> 0x8ba43d8f
+    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]
+  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5, exampleEntry15,
+    exampleEntry16, exampleEntry6, exampleEntry7, exampleEntry12, exampleEntry20, exampleEntry8,
+    exampleEntry9, exampleEntry19, exampleEntry10, exampleEntry11, exampleEntry17, exampleEntry18,
+    exampleEntry13, exampleEntry14]
 
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"