Add maxStore example and stdlib helpers

Author: Th0rgal

STATUS.md

@@ -8,14 +8,17 @@ Last updated: 2026-02-09
 - Keep the repo small and auditable.
 - Track the external tooling landscape (specs + formal verification).
 - Resolve spec aliasing hazards (sequential reads vs. forbid `from = to`).
+- Make examples smaller + build an ergonomic EDSL surface (stdlib, macros, patterns).
 
 ## In Progress
 - First compiler correctness lemma (arith + storage).
 - Memory model for ABI return encoding.
 - Spec shape for reverts (keep `Spec` minimal, add `SpecR`).
 - External landscape refresh (Act/Scribble/Certora/SMTChecker/KEVM).
- - Reconcile sequential-read vs old-state transfer specs (aliasing boundary).
+- Reconcile sequential-read vs old-state transfer specs (aliasing boundary).
 - 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.
 
 ## Recently Done
 - Lean -> Yul pipeline with runtime + creation bytecode artifacts.
@@ -35,6 +38,11 @@ Last updated: 2026-02-09
 - Added a self-transfer counterexample lemma showing `transferSpecR` cannot hold for `from = to` when `amount > 0`.
 - Proved sequential transfer spec is equivalent to old-state spec when `from ≠ to`.
 - Added a guarded transfer spec (`transferSpecRNoSelf`) and proof it meets execution when `from ≠ to`.
+- Added a counterexample lemma showing list-based supply accounting breaks with duplicates.
+- Split `Examples.lean` into multiple focused example modules (store ops, risk, token base, supply, transfer).
+- 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.
 - 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

@@ -16,6 +16,11 @@
 - Added a self-transfer counterexample lemma showing `transferSpecR` cannot hold for `from = to` when `amount > 0`.
 - Proved sequential transfer spec is equivalent to old-state spec when `from ≠ to`.
 - Added a guarded transfer spec (`transferSpecRNoSelf`) and proof it meets execution when `from ≠ to`.
+- Added a small counterexample lemma showing list-based supply accounting breaks with duplicates (motivation for sets/dedup).
+- Split `Examples.lean` into multiple focused example modules.
+- 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.
 - 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

@@ -120,6 +120,17 @@ def exampleEntry4 : EntryPoint :=
     selector := 0x49f583e3
     returns := false }
 
+def exampleEntry5 : EntryPoint :=
+  { name := "maxStore"
+    args := ["slot", "a", "b"]
+    body := Lang.Stmt.if_
+      (Lang.Expr.gt (Lang.Expr.var "a") (Lang.Expr.var "b"))
+      (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "a"))
+      (Lang.Stmt.sstore (Lang.Expr.var "slot") (Lang.Expr.var "b"))
+    -- maxStore(uint256,uint256,uint256) -> 0xb61d4088
+    selector := 0xb61d4088
+    returns := false }
+
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
     args := ["collateral", "debt", "minHF"]