Skip to content

Add raise-slot helper and example #7

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Th0rgal wants to merge 22 commits into from
Closed

Add raise-slot helper and example #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
8a5a5fb
Add requireNonZero helper and setNonZero example
Th0rgal Feb 9, 2026
461c1bc
Align direct EVM asm with solc labels
Th0rgal Feb 10, 2026
b2719ee
Update status date
Th0rgal Feb 10, 2026
768fadf
Add compareAndSwap helper + example
Th0rgal Feb 10, 2026
de05f3f
Add requireGt helper and setIfGreater example
Th0rgal Feb 10, 2026
c3bf8bf
Add sstoreAdd helper and bumpSlot example
Th0rgal Feb 10, 2026
7dbdf0d
Add revertIf helper and setIfLess example
Th0rgal Feb 10, 2026
1fbe6fe
Add requireLt and setIfBetween example
Th0rgal Feb 10, 2026
083fa13
Add letSload helper and initOnce example
Th0rgal Feb 10, 2026
30c2a2c
Add requireAnd helper and setIfNonZeroAndLess example
Th0rgal Feb 10, 2026
9c078a7
Add sstoreInc helper and bumpIfNonZero example
Th0rgal Feb 10, 2026
d1730da
Add sstoreMax helper and updateMax example
Th0rgal Feb 10, 2026
09ea02d
Add sstoreMin helper and updateMin example
Th0rgal Feb 10, 2026
61e2376
Add requireBetween helper and addIfBetween example
Th0rgal Feb 10, 2026
d77d6fe
Add sstoreSub helper and subIfEnough example
Th0rgal Feb 10, 2026
1670842
Add requireGte helper and setIfAtLeast example
Th0rgal Feb 10, 2026
748b0da
Add requireZero helper and initToOne example
Th0rgal Feb 10, 2026
8652f5a
Add sstoreIfEq helper and clearIfEq example
Th0rgal Feb 10, 2026
99c0cd1
Add requireNonZeroAndLt and addIfNonZeroAndLess example
Th0rgal Feb 10, 2026
8bec91b
Add sstoreIfZero helper and initDouble example
Th0rgal Feb 10, 2026
f8394f3
Add sstoreIfLt helper and capSlot example
Th0rgal Feb 10, 2026
5dac4af
Add sstoreIfGt helper and raiseSlot example
Th0rgal Feb 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 15 additions & 1 deletion STATUS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Status

Last updated: 2026-02-09
Last updated: 2026-02-10

## Current Focus
- Lean-only specs + implementations + proofs.
Expand All @@ -19,8 +19,14 @@ 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 `sstoreIfGt` helper plus a raise-slot example to avoid redundant writes.


## Recently Done
- Added `sstoreIfGt` helper, refactored `updateMax`, and added `raiseSlot` example + Foundry test.
- Added `sstoreIfLt` helper, refactored `updateMin`, and added `capSlot` example + Foundry test.
- Added `sstoreIfZero` helper and an `initDouble` example + Foundry test.
- 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.
Expand All @@ -43,6 +49,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).
Expand Down
105 changes: 105 additions & 0 deletions docs/research-log.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,93 @@
# Research Log

## 2026-02-10
- Added `sstoreIfGt` stdlib helper to avoid redundant stores on monotonic increases.
- Refactored `updateMax` to use `sstoreIfGt`.
- Added `raiseSlot` example (raise slot to a floor without reverting) with Spec + proof.
- Added Foundry test for `raiseSlot`.
- Updated compiler entries + direct EVM asm wiring for `raiseSlot` and `updateMax`.
- `end_to_end` initially failed due to cap/raise stub ordering; swapped the `tag_raiseSlot`/`tag_capSlot` order so jumpdest offsets match solc.
- Ran `PATH=/opt/lean-4.27.0/bin:$PATH lake build`, `./scripts/end_to_end.sh`, and `./scripts/foundry_test_generated.sh` (all green).
- Added `requireNonZeroAndLt` stdlib helper for combined nonzero + max guards.
- Refactored `setIfNonZeroAndLess` to use `requireNonZeroAndLt`.
- Added `addIfNonZeroAndLess` example (guarded add on `delta != 0` and `delta < max`) with SpecR + proofs.
- Added Foundry test for `addIfNonZeroAndLess`.
- Updated compiler entries + direct EVM asm for `addIfNonZeroAndLess`.
- 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.
- 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.
Expand All @@ -21,9 +109,26 @@
- 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.
- Added Foundry tests for generated contracts.
- Compressed docs + tightened minimal frontend.
- Scanned external tooling landscape (Act, Scribble, Certora, SMTChecker, KEVM/Kontrol, VerX, Move Prover).
# 2026-02-10
- Added `sstoreIfZero` stdlib helper to package the common "load + require zero + store" pattern.
- Refactored `initOnce` and `initToOne` to use `sstoreIfZero`.
- Added `initDouble` example (initialize to `value * 2` on zero) with SpecR + proofs.
- Added Foundry test for `initDouble`.
- Updated compiler entries + direct EVM asm wiring for `initDouble`.
- `end_to_end` initially failed due to direct EVM asm mismatch in `initDouble`; fixed by aligning the stack order (`swap1` prelude + `swap1` before `sstore`) with solc output.
- Ran `PATH=/opt/lean-4.27.0/bin:$PATH lake build`, `./scripts/end_to_end.sh`, and `./scripts/foundry_test_generated.sh` (all green).
- Added `sstoreIfLt` stdlib helper to avoid redundant stores when capping a slot.
- Refactored `updateMin` to use `sstoreIfLt` (skip store when the slot is already below the cap).
- Added `capSlot` example (cap a slot to a maximum without reverting) with Spec + proof.
- Added Foundry test for `capSlot`.
- Updated compiler entries + direct EVM asm wiring for `updateMin` and `capSlot`.
- `end_to_end` initially failed due to direct EVM asm block layout for `capSlot`/`updateMin`; fixed by matching solc's `jump(tag_out)` shape and using `PUSH0` for zero.
- Ran `PATH=/opt/lean-4.27.0/bin:$PATH lake build`, `./scripts/end_to_end.sh`, and `./scripts/foundry_test_generated.sh` (all green).
Loading
Loading