WIP: maxStore example + stdlib slot helpers

.github/workflows/test.yml

@@ -101,3 +101,26 @@ jobs:
         env:
           RPC_URL: http://127.0.0.1:8545
         run: ./scripts/deploy_example.sh
+
+  foundry-legacy:
+    name: Foundry legacy contract tests
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          persist-credentials: false
+          submodules: recursive
+
+      - name: Install Foundry
+        working-directory: research/lean_only_proto
+        run: ./scripts/install_foundry.sh
+
+      - name: Install solc
+        working-directory: research/lean_only_proto
+        run: ./scripts/install_solc.sh
+
+      - name: Run legacy Foundry tests
+        working-directory: legacy/foundry
+        run: forge test

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "legacy/foundry/lib/forge-std"]
+	path = legacy/foundry/lib/forge-std
+	url = https://github.com/foundry-rs/forge-std

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.

legacy/foundry/foundry.lock

@@ -0,0 +1,8 @@
+{
+  "lib/forge-std": {
+    "tag": {
+      "name": "v1.14.0",
+      "rev": "1801b0541f4fda118a10798fd3486bb7051c5dd6"
+    }
+  }
+}

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -120,6 +120,20 @@ 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 exampleEntries : List EntryPoint :=
+  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5]
+
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
     args := ["collateral", "debt", "minHF"]
@@ -143,4 +157,7 @@ def healthEntryCheck : EntryPoint :=
     selector := 0x1753bbd7
     returns := false }
 
+def healthEntries : List EntryPoint :=
+  [healthEntrySet, healthEntryCheck]
+
 end DumbContracts.Compiler

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -23,13 +23,30 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH tag_addSlot"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x49f583e3"
   , "EQ"
   , "PUSH tag_guardedAddSlot"
   , "JUMPI"
+  , "PUSH4 0xb61d4088"
+  , "EQ"
+  , "PUSH tag_maxStore"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_maxStore:"
+  , "PUSH ret_maxStore"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH fn_maxStore"
+  , "JUMP"
+  , "ret_maxStore:"
+  , "STOP"
   , "tag_guardedAddSlot:"
   , "PUSH ret_guardedAddSlot"
   , "PUSH1 0x24"
@@ -110,6 +127,36 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH guardedAddSlot_check"
   , "JUMP"
+  , "fn_maxStore:"
+  , "SWAP1"
+  , "DUP3"
+  , "SWAP1"
+  , "DUP2"
+  , "DUP2"
+  , "GT"
+  , "PUSH maxStore_then"
+  , "JUMPI"
+  , "maxStore_check:"
+  , "GT"
+  , "ISZERO"
+  , "PUSH maxStore_else"
+  , "JUMPI"
+  , "maxStore_join:"
+  , "POP"
+  , "POP"
+  , "JUMP"
+  , "maxStore_else:"
+  , "SSTORE"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH maxStore_join"
+  , "JUMP"
+  , "maxStore_then:"
+  , "DUP1"
+  , "DUP4"
+  , "SSTORE"
+  , "PUSH maxStore_check"
+  , "JUMP"
   ]
 
 def pretty (lines : List String) : String :=