diff --git a/DESIGN.md b/DESIGN.md index 2e43d5d..1f58c4b 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -1,7 +1,7 @@ # Yul Semantics — Design This repository defines a formal semantics for the [Yul](https://docs.soliditylang.org/en/latest/yul.html) -intermediate language in Lean 4. It is the foundation for a future, separate project: a +intermediate language in Lean 4. It is the foundation for a separate, future project: a **verified optimizing compiler from Yul to EVM bytecode**. That compiler will build *on top* of this repository; the EVM bytecode semantics lives in a *different* repository and is not included here. @@ -10,8 +10,6 @@ Scope of this repo: **the Yul semantics only.** No compiler, no bytecode. ## Guiding decisions -These were decided up front and drive everything below. - ### 1. Gas is not modeled The Yul semantics is **gas-free**. There is no gas field in the machine state and no gas in the @@ -21,8 +19,8 @@ control-flow outcome. Consequences: obligation. We deliberately prove **nothing** about gas going up or down (some passes trade it). - Gas is the optimizer's *motivation*, never a correctness obligation. -The one place gas leaks into the *language* is via built-ins, handled in the Dialect (see §"Effect -classification"). +The one place gas leaks into the *language* is via built-ins, handled in the Dialect (see "Effect +classification" and "Gas" below). Although gas costs are absent, the EVM dialect tracks the active-memory high-water mark because `msize()` exposes it as a functional program result. Memory-touching operations update that mark; @@ -36,15 +34,15 @@ semantics** — an evaluation relation, not an executable function. Rationale: empirical validation against `solc`'s Yul interpreter is **not** a priority for this project, so the main advantage of an executable interpreter (differential testing) does not apply. The relational semantics reads like a specification, is the natural object for inductive -meta-theory (logic soundness, compiler simulation), models non-determinism natively, and — because -we prove the interpreter equivalent to it if/when we build one — its "silent ill-formedness" risk -is caught by that very equivalence proof (a missing rule makes adequacy unprovable). +meta-theory (logic soundness, compiler simulation), and models non-determinism natively. An **executable fuel-indexed interpreter** is a *derived* view (`YulSemantics/Interp.lean`), built over an `ExecDialect` (a `Dialect` plus a computable `builtinFn`). It is not itself a correctness -foundation; **adequacy** — `interp` ⇔ `BigStep` (sound always, complete for terminating runs) — is -the pending proof that ties it to the ground truth. It already lets us *run* programs end-to-end -(see the `native_decide` tests in `YulSemantics/Examples.lean`). +foundation; it is tied to the ground truth by the **adequacy** theorem (`YulSemantics/Adequacy.lean`): +the interpreter is sound at any fuel and complete at sufficiently large fuel for terminating runs. +Together with determinism, this pins the interpreter down as *the* computational content of the +semantics. It also lets us *run* programs end-to-end (see the `native_decide` tests in +`YulSemantics/Examples.lean`). ### 3. The semantics is parameterized over an abstract `Dialect` @@ -55,9 +53,10 @@ independent of the built-in functions. We reflect this with an abstract `Dialect over it (see "AST" below). - `Value` — the value type (for the EVM dialect: `BitVec 256`). - `State` — the machine/world state (memory, storage, environment, logs, …). -- `builtins` — interpretation of built-in functions: names + argument values + state ↦ result - values + new state (+ possible halt). -- `litValue` — interpretation of numeric literals as values. +- `Builtin` — interpretation of built-in functions as a *relation*: operation + argument values + + state ↦ result values + new state (+ possible halt). A relation, not a function, so that + non-deterministic built-ins (`gas()`, external calls) can be modeled. +- `litValue` — interpretation of literals as values. - effect classification of built-ins (see below). This keeps the repository pure Yul. The compiler project instantiates the Dialect using the *real* @@ -81,10 +80,10 @@ same data; `BitVec.toFin`/`BitVec.ofFin` are inverse projections with `simp` sup match relation relates words by this coercion — a definitional coercion, not a real conversion. We do **not** change the EVM repo. -### 5. Concrete-syntax DSL, built early +### 5. Concrete-syntax DSL A `syntax`/macro embedding lets us write real Yul concrete syntax that elaborates to the AST -(similar in spirit to EVMYulLean). Built early so tests and examples read like Yul from the start. +(similar in spirit to EVMYulLean), so tests and examples read like Yul. ## Language model @@ -98,8 +97,8 @@ Yul's grammar (EVM dialect) is small and fixed: `break`, `continue`, `leave`, and expression-statements. - **Objects**: named code block + sub-objects + data. -**Built-ins are a first-class enum, and the AST is parameterized over it (Option D).** A call is -either a dialect built-in (`Expr.builtin op args`, `op : Op`) or a user-defined function call +**Built-ins are a first-class enum, and the AST is parameterized over it.** A call is either a +dialect built-in (`Expr.builtin op args`, `op : Op`) or a user-defined function call (`Expr.call fn args`, `fn : Ident`). The AST is generic in the *type* `Op` (the dialect supplies it), so: @@ -109,11 +108,9 @@ so: - **dialect-specific** optimizations (constant folding, algebraic identities) fix `Op := EVM.Op` and pattern-match on it structurally (exhaustive, type-checked), with correctness proofs connecting `op` directly to the built-in semantics; -- name→`Op` resolution happens at parse time (Phase 4), sound because Yul forbids user functions from +- name→`Op` resolution happens at parse time, sound because Yul forbids user functions from shadowing built-ins. User functions remain `Ident`, resolved via the environment. -Sketch: - ```lean inductive Expr (Op : Type) | lit (l : Literal) @@ -148,23 +145,27 @@ inductive Outcome | normal | break | continue -- caught by the enclosing `for` | leave -- caught by the enclosing function body - | halt (h : HaltData) -- from halting built-ins (return/revert/stop); propagates to the top + | halt -- from halting built-ins (return/revert/stop); propagates to the top; + -- the payload (kind + data) lives in the machine state ``` +Argument lists are evaluated **right-to-left** (Yul's specified order); values are collected in +source order. + ### Scoping Yul is lexically scoped. A block first collects its function definitions (functions may be forward-referenced within a block), then executes its statements. The environment maps variable names to values and function names to definitions. -### Effect classification (the one place gas touches the language) +### Effect classification -The `Dialect` classifies each built-in by effect — e.g. *pure*, *state-reading*, *state-writing*, -*halting*, and whether it is *deterministic*. This classification is what makes optimization proofs -sound (CSE/DCE/reordering may only move or drop calls with the right effects). -The EVM dialect proves that these flags soundly over-approximate `stepOp`: deterministic operations -have at most one result, non-writing operations preserve the entire state, and non-halting -operations only return normally (`EVM.effects_sound`). +The `Dialect` classifies each built-in by effect — whether it is *deterministic*, *reads* state, +*writes* state, and/or *halts*. This classification is what makes optimization proofs sound +(CSE/DCE/reordering may only move or drop calls with the right effects). The EVM dialect proves that +these flags soundly over-approximate `stepOp`: deterministic operations have at most one result, +non-writing operations preserve the entire state, and non-halting operations only return normally +(`EVM.effects_sound`; `EVM.effects_sound_withExternal` for the open-world dialect). Because static-call write protection (see below) lets the state-modifying built-ins halt when the frame is static, and `effects` cannot observe `ExecEnv.static`, `sstore`/`tstore`/`log0`–`log4` and @@ -172,6 +173,11 @@ the whole call/create family carry `halts := true`. This is a faithful over-appr slightly weakens the non-halting guarantee for these writers — a deliberate tradeoff of modeling static context. +(The `reads` flag is documented but its soundness is not yet machine-checked — see "What is not done, +and why".) + +## EVM dialect: external calls and contract creation + External calls and contract creation use the relational dialect directly. `EVM.evmWithExternal calls creates` takes separate `ExternalCalls` and `ExternalCreates` relations from a request and pre-operation state to a completed response; `evmWithCalls` remains the @@ -189,51 +195,47 @@ behavior. It fixes the boundary: zero-value `call` remain permitted (`STATICCALL` sets this bit on the callee frame); - successful non-static calls commit the supplied post-world; - failure and `staticcall` roll back all supplied world changes; -- creation installs the supplied committed world on success or failure (so a creator nonce bump can - survive failed deployment) and returns the created address or zero; +- creation installs the committed post-world on every path (a creator nonce bump can survive failed + deployment) and returns the created address or zero; a *failed* creation commits **only** the + creator nonce bump, rolling everything else back, exactly as a call rolls back on failure + (`finishCreate_failure_storage` / `finishCreate_success_storage`); - return data is retained in full, while only its requested prefix is copied to caller memory; and - the call expression evaluates to the EVM success word. For `create`/`create2`, the init-code memory slice is copied into the request and expands active memory. A successful response installs its selected address and clears returndata; failure returns -zero and may expose revert data. The completed post-world is installed on every path because the -creator nonce can advance even when init code reverts or deployment fails. CREATE2 requests also -carry their salt. Global nonce and storage projections make these responses stable across every -matching concrete world, including storage-dependent callees and reentrant execution. - -The executable `EVM.evm` keeps calls and creations stuck. There is deliberately no universal executable choice -for an open-world relation. Compiler correctness instead instantiates `external` with responses -realized by complete target-EVM executions. Those executions may take any number of steps and use -an arbitrarily deep call stack, so the simulation boundary does not impose a no-reentrancy or -closed-world assumption. - -**Meta-theory scope (which guarantees apply to which dialect).** The determinism lemma, the -fuel-indexed interpreter, and the adequacy theorem are all stated for the **closed-world local -dialect `EVM.evm`**. They do **not** apply to the **open-world `EVM.evmWithExternal` (call/create)**: -that dialect is relational and may be non-deterministic (the environment picks the external response), -so it is not covered by determinism; and because there is no universal executable choice for the -open-world relation, it has neither an interpreter nor an adequacy result — the executable dialect -leaves `gas()` and the whole call/create family stuck. The one meta-theoretic property that *is* -proven for the open world is effect-classification soundness (`EVM.effects_sound_withExternal`). -Consequently, programs that call `gas()` or perform external calls/creations are outside the -determinism and adequacy guarantees. +zero and may expose revert data. CREATE2 requests also carry their salt. Global nonce and storage +projections make these responses stable across every matching concrete world, including +storage-dependent callees and reentrant execution. + +The executable `EVM.evm` keeps calls and creations stuck. There is deliberately no universal +executable choice for an open-world relation. Compiler correctness instead instantiates `external` +with responses realized by complete target-EVM executions. Those executions may take any number of +steps and use an arbitrarily deep call stack, so the simulation boundary does not impose a +no-reentrancy or closed-world assumption. + +### `selfdestruct` `selfdestruct` is local and terminal rather than open-world: it does not invoke unknown code. Its -executable semantics transfers the current balance, appends the executing address to the ordered -destruction schedule, and halts. `ExecEnv.createdThisTx` selects the post-Cancun behavior when the -beneficiary aliases the executing address: a pre-existing account keeps its balance, whereas an -account created in this transaction burns it. Actual fork-dependent account deletion is deferred -to transaction finalization and is intentionally outside this frame semantics. External call and -creation worlds carry newly scheduled destructions so nested executions remain observable. +executable semantics transfers the current balance, appends the executing address (together with its +`createdThisTx` bit) to the ordered destruction schedule, and halts. `ExecEnv.createdThisTx` selects +the post-Cancun behavior when the beneficiary aliases the executing address: a pre-existing account +keeps its balance, whereas an account created in this transaction burns it. Recording the bit +alongside each scheduled address keeps balance-transfer-only distinct from actual deletion. Actual +fork-dependent account deletion is deferred to transaction finalization and is intentionally outside +this frame semantics. External call and creation worlds carry newly scheduled destructions so nested +executions remain observable. -Two built-ins interact with gas and must be classified as **impure / non-deterministic** even -though we do not model gas: +### Gas + +Two built-ins interact with gas and are classified as **impure / non-deterministic** even though we +do not model gas: - `gas()` returns *remaining* gas — a value that changes during execution. It is modeled as an oracle / non-deterministic read (never a constant; two `gas()` calls may differ, so they cannot be - CSE'd). Concretely, the open-world dialects (`evmWithExternal`/`evmWithCalls`) interpret - `gas()` via `builtinWithExternal`: it returns an *arbitrary* word and leaves the state unchanged, - so `call(gas(), …)` — the idiomatic call pattern — is derivable. The executable reference dialect + CSE'd). Concretely, the open-world dialects (`evmWithExternal`/`evmWithCalls`) interpret `gas()` + via `builtinWithExternal`: it returns an *arbitrary* word and leaves the state unchanged, so + `call(gas(), …)` — the idiomatic call pattern — is derivable. The executable reference dialect `evm` has no oracle, so `gas()` stays stuck there (`stepOp .gas = none`); this is why `evm` is deterministic while the open-world dialects are not. - gas forwarding + failure of `call`/`callcode`/`staticcall`/`delegatecall`: external call outcomes @@ -263,31 +265,85 @@ This is what makes dead-effect reasoning sound at the frame level. The raw exact (`EquivStmt`/`EquivBlock`, which compare the full `Step` state) cannot equate a dead write before a revert with the bare revert, because they see the un-rolled-back write. Observed through `committedState` they *are* equal: `EVM.deadStore_revert_obs_eq` proves `{ sstore(0,1); revert(0,0) }` -and `{ revert(0,0) }` have identical committed runs from every initial state. - -## Meta-theory / what we are building toward - -### Yul→Yul optimization correctness (this repo's proof surface) - -Target property: **semantic preservation** = functional equivalence of whole-program behavior. Tools: - -1. **Behavior / observation**: halting result (`return`/`revert`/`stop`/exception + returndata), - resulting storage/logs, and terminate-vs-diverge. (No gas.) The `Step` judgment records *which* - halt fired in the state (`halted`) but, being shared with sub-frames, does not itself roll back a - halted frame's accumulated effects — so a whole-program observation is taken through - **`EVM.committedState`** (see "Frame-boundary observation" below), which commits normal/`stop`/ - `return`/`selfdestruct` halts and rolls a `revert`/`invalid`/`invalidMemoryAccess` frame back to - its initial state (keeping only the outcome marker and exposed return data). `EVM.RunCommitted` - is the observed whole-program run; with `EVM.run_det` it is functional (`RunCommitted.det`). -2. **Contextual equivalence as a congruence**: expression- and statement-equivalence proven to be a - *congruence* w.r.t. every AST constructor. Local rewrites (`add(x,0) → x`, constant folding, …) - are proven locally and lifted into any context by this congruence lemma — the workhorse. -3. **Effect classification** (above): required for CSE, dead-code elimination, reordering. -4. **Binding discipline for inlining**: substitution / α-renaming with capture avoidance. -5. **Determinism lemma**: the EVM-dialect semantics is deterministic given the dialect (modulo the - oracle inputs), which turns "equivalence" into "same result." - -### Yul→EVM compiler correctness (future, separate repo) +and `{ revert(0,0) }` have identical committed runs from every non-static initial state. (The +non-static condition is essential and faithful: under `STATICCALL` the `sstore` itself halts with +`.invalid`, so the two programs genuinely differ.) + +## What is proven + +- **Determinism** (`YulSemantics/Determinism.lean`). `Step.det` by a single rule induction, given + deterministic built-ins; corollaries for the five conceptual relations and whole-program runs. + `EVM.evm_deterministic` discharges the hypothesis for the EVM dialect (`EVM.run_det`). Two design + notes make this a standard tactic proof: (1) `switch` dispatches through `selectSwitch` (requiring + `[DecidableEq D.Value]` on the judgment), so it is deterministic by construction; (2) the semantics + is encoded as a **single indexed judgment** `Step` over a `Code`/`Res` sum rather than five literal + `mutual` relations — Lean's `induction` tactic does not support mutual inductive predicates and the + equation compiler cannot compile mutual structural recursion over them, so the single-judgment + encoding is what makes this (and every future derivation induction) a standard `induction … with` + proof. The five relation names survive as abbreviations with unchanged signatures. +- **Adequacy** (`YulSemantics/Adequacy.lean`). Under `ExecDialect.Lawful` (the executable `builtinFn` + agrees exactly with the relational `Builtin`; definitional for the EVM dialect): **soundness** + (interpreter `.ok` at any fuel ⇒ derivation; induction on fuel) and **completeness** (derivation ⇒ + interpreter `.ok` at every sufficiently large fuel; rule induction — the `∀ n ≥ N` form embeds fuel + monotonicity, so no separate monotonicity lemma). Combined as `Interp.adequacy` / + `Interp.run_adequacy`, instantiated hypothesis-free for EVM as `EVM.run_adequacy`. +- **Effect-classification soundness** (`EVM.effects_sound`, `EVM.effects_sound_withExternal`) — the + `deterministic`/`writes`/`halts` flags are proven to over-approximate the built-in semantics. +- **Optimization meta-theory** (`YulSemantics/Equiv.lean`, `YulSemantics/Rewrites.lean`). Pointwise + semantic equivalences for all five syntactic classes (`EquivExpr`/`EquivArgs`/`EquivStmt`/ + `EquivStmts`/`EquivBlock`, each an equivalence relation); behavior (`EquivBlock.run_iff`); + **congruence lemmas** for built-in/user calls (argument lists via `Forall₂`), + `let`/`assign`/`exprStmt`/`cond`/`switch` (labels + case blocks + default) / `forLoop` + (cond/post/body), sequences, and blocks. Validated by sample EVM rewrites: constant folding + `add(2,3) ≈ 5`, the identity `add(x,0) ≈ x` (stated for a *variable* — `add(e,0) ≈ e` is false for + a multi-valued `e`, a real optimizer precondition surfaced by the proofs), and that identity lifted + through congruence to `sstore(0, add(x,0)) ≈ sstore(0, x)` at statement and whole-program (DSL) + level. +- **Frame-boundary observation** (`YulSemantics/Observation.lean`) — `committedState`, `RunCommitted` + (functional via `RunCommitted.det`), and `deadStore_revert_obs_eq`. +- **Objects** (`YulSemantics/Object.lean`, `YulSemantics/ObjectRun.lean`) — a layout-consistency + predicate relating a compiler's byte layout to an object, and a symbolic proof that the canonical + constructor (`datacopy`/`return`) returns a data segment's bytes. + +### Meta-theory scope (which guarantees apply to which dialect) + +The determinism lemma, the fuel-indexed interpreter, and the adequacy theorem are all stated for the +**closed-world local dialect `EVM.evm`**. They do **not** apply to the **open-world +`EVM.evmWithExternal` (call/create)**: that dialect is relational and may be non-deterministic (the +environment picks the external response), so it is not covered by determinism; and because there is +no universal executable choice for the open-world relation, it has neither an interpreter nor an +adequacy result — the executable dialect leaves `gas()` and the whole call/create family stuck. The +one meta-theoretic property that *is* proven for the open world is effect-classification soundness +(`EVM.effects_sound_withExternal`). Consequently, programs that call `gas()` or perform external +calls/creations are outside the determinism and adequacy guarantees. + +## What is not done, and why + +- **Yul→EVM compiler correctness** — out of scope for this repo (it lives in the separate compiler + project); the target is described under "Toward Yul→EVM compiler correctness" below. +- **Inlining / function-body congruence.** There is no `funDef`-body congruence yet: rewriting inside + a function *body* changes the `FDecl` stored by block-hoisting, so relating the two programs needs a + relation on function environments ("environments with pointwise-equivalent bodies") threaded through + the judgment. That machinery belongs with function-level optimizations (inlining) and is deferred. + Relatedly, block congruence carries a `hoist`-agreement side condition (`rfl` for rewrites that do + not touch top-level `funDef` statements). +- **`reads`-flag soundness.** `EffectsSound` proves the `deterministic`/`writes`/`halts` clauses; a + machine-checked soundness for `reads` (result independent of the unread part of the state) needs a + notion of state observation / read footprint, and is deferred. The flag is documented and currently + unused by any proof. +- **Account-map consistency.** The abstract world maps (`balanceOf`/`nonceOf`/`extCodeOf`/ + `extCodeHashOf`/`storageOf`) are independent; the intended cross-map invariants (e.g. `extcodehash` + = keccak of code for non-empty accounts, zero for empty ones) are captured by an optional + `ExecEnv.WF` predicate available to downstream proofs, not globally enforced. `extcodehash` itself + is computed through `projectedCodeHash` so it is internally consistent with code/nonce/balance. +- **Program logic (Hoare / separation).** An optional convenience layer, deferred until needed — see + below. +- **Divergence reasoning.** Deferred indefinitely — not needed for the main compiler theorem (see + below). +- **Gas.** Not modeled by design (§1). Within-frame out-of-gas is not expressible; out-of-gas in a + callee is subsumed by the open-world call relation. + +## Toward Yul→EVM compiler correctness (future, separate repo) Because the EVM semantics **tracks gas fully**, the EVM machine always terminates (normal halt or out-of-gas). Two consequences: @@ -326,56 +382,8 @@ features, and is deferred until needed: - **Separation logic** for the machine state: memory and storage are finite word→word maps, so points-to assertions + the frame rule give local reasoning about `mload`/`mstore`/`sload`/`sstore`. -Soundness is proven against the relational semantics. This layer is a convenience, not required for -the equivalence/simulation results above. - -## Build plan (phases) - -- **Phase 0** — Toolchain: add Mathlib (pinned to the toolchain), CI, module layout. *(done)* -- **Phase 1** — AST (`Literal`/`Expr`/`Stmt`/`Object`) + `Outcome`. *(done — `YulSemantics/Ast.lean`)* -- **Phase 2** — `Dialect` abstraction + effect classification; gas-free EVM dialect instance - (`Value := BitVec 256`). *(done — `YulSemantics/Dialect.lean`, `YulSemantics/Dialect/EVM.lean`)* -- **Phase 3** — Big-step relational semantics (the ground truth): scoping, block-level function - pre-collection, multiple return values, outcome propagation. *(relation done — - `YulSemantics/BigStep.lean`, smoke-tested in `YulSemantics/Examples.lean`; determinism proven — - see below)* -- **Phase 4** — Concrete-syntax DSL (Yul syntax → AST). *(done — `YulSemantics/Syntax.lean`; - `yul% { … }` → `Block EVM.Op`, round-trip-tested in `YulSemantics/Examples.lean`)* -- **Interpreter** — total fuel-indexed executable interpreter over an `ExecDialect`. *(done — - `YulSemantics/Interp.lean`; runs programs in `Examples.lean` via `native_decide`)* -- **Phase 5** — Meta-theory foundations: behavior/observation, contextual equivalence + congruence - lemma, sample local-rewrite equivalences validating the framework. -- **Determinism** — *(done — `YulSemantics/Determinism.lean`)*. `Step.det` by a single rule - induction, given deterministic built-ins; corollaries for the five conceptual relations and - whole-program runs; `EVM.evm_deterministic` discharges the hypothesis for the EVM dialect - (`EVM.run_det`). Two design notes baked in along the way: (1) `switch` dispatches through - `selectSwitch` (requiring `[DecidableEq D.Value]` on the judgment), making it deterministic by - construction; (2) the semantics is encoded as a **single indexed judgment** `Step` over a - `Code`/`Res` sum rather than five literal `mutual` relations — Lean's `induction` tactic does not - support mutual inductive predicates and the equation compiler cannot compile mutual structural - recursion over them, so the single-judgment encoding is what makes this (and every future - derivation induction: adequacy, compiler simulation) a standard tactic proof. The five relation - names survive as abbreviations with unchanged signatures. -- **Adequacy** — *(done — `YulSemantics/Adequacy.lean`)*. Under `ExecDialect.Lawful` (the executable - `builtinFn` agrees exactly with the relational `Builtin`; definitional for the EVM dialect): - **soundness** (interpreter `.ok` at any fuel ⇒ derivation; induction on fuel) and **completeness** - (derivation ⇒ interpreter `.ok` at every sufficiently large fuel; rule induction — the - `∀ n ≥ N` form embeds fuel monotonicity, so no separate monotonicity lemma). Combined as - `Interp.adequacy` / `Interp.run_adequacy`, instantiated hypothesis-free for EVM as - `EVM.run_adequacy`. With determinism, the interpreter is pinned down as *the* computational - content of the semantics. -- **Phase 5** — optimization meta-theory. *(first cut done — `YulSemantics/Equiv.lean`, - `YulSemantics/Rewrites.lean`)*. Pointwise semantic equivalences for all five syntactic classes - (`EquivExpr`/`EquivArgs`/`EquivStmt`/`EquivStmts`/`EquivBlock`, each an equivalence relation); - behavior (`EquivBlock.run_iff`); **congruence lemmas** for built-in/user calls (argument lists via - `Forall₂`), `let`/`assign`/`exprStmt`/`cond`/`switch` (labels + case blocks + default) /`forLoop` - (cond/post/body), sequences, and blocks. Two honest hoisting-induced side conditions, documented - in the module: block congruence needs `hoist`-agreement (`rfl` for non-`funDef` rewrites), and - `funDef`-body congruence is deferred to the function-environment relation that inlining will need. - Validated by sample EVM rewrites: constant folding `add(2,3) ≈ 5`, the identity `add(x,0) ≈ x` - (stated for a *variable* — `add(e,0) ≈ e` is false for multi-valued `e`, a real optimizer - precondition surfaced by the proofs), and the identity lifted through congruence to - `sstore(0, add(x,0)) ≈ sstore(0, x)` at statement and whole-program (DSL) level. +Soundness would be proven against the relational semantics. This layer is a convenience, not required +for the equivalence/simulation results above. ## Dependencies diff --git a/README.md b/README.md index 39dbcdf..7f5aef4 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ A formal semantics for the [Yul](https://docs.soliditylang.org/en/latest/yul.html) intermediate language, written in Lean 4. -This repository defines **only the Yul semantics**. It is the foundation for a future, separate +This repository defines **only the Yul semantics**. It is the foundation for a separate, future project — a *verified optimizing compiler from Yul to EVM bytecode* — that will build on top of it. The EVM bytecode semantics lives in a different repository. @@ -11,9 +11,10 @@ The EVM bytecode semantics lives in a different repository. See [`DESIGN.md`](./DESIGN.md) for the full design and its rationale. In short: -- **Gas is not modeled.** Optimization correctness is functional equivalence. -- **Ground truth is a big-step relational semantics** (an inductive evaluation relation). A - fuel-indexed executable interpreter is provided as a derived view, proven adequate. +- **Gas is not modeled.** Yul→Yul optimization correctness is functional equivalence, not a gas + obligation. +- **The ground truth is a big-step relational semantics** (an inductive evaluation relation). A + fuel-indexed executable interpreter is a derived view, proven adequate. - The semantics is **parameterized over an abstract `Dialect`** (value type, machine state, built-in interpretation), keeping the core dialect-agnostic. - The **EVM dialect uses `BitVec 256`** for words. @@ -28,58 +29,127 @@ lake exe cache get # fetch prebuilt Mathlib oleans lake build ``` -## Status - -In place: - -- **Core semantics** — the big-step relational ground truth, a determinism proof, and a - fuel-indexed executable interpreter with a proven adequacy (soundness + completeness) theorem. -- **EVM dialect** — the full built-in set (through the upcoming hard fork), over `BitVec 256`, - including an environment-supplied Keccak oracle that is abstract by default and executable when - a client supplies a concrete implementation. CALL and CREATE-family operations have additive - open-world relational interpretations supporting arbitrary nested calls, creations, and - reentrancy; the executable dialect leaves them stuck. `selfdestruct` deterministically transfers - the executing account's balance, records its deferred transaction-finalization destruction, and - halts, including the post-Cancun created-this-transaction/self-beneficiary distinction. A frame - flagged static (`ExecEnv.static`, as set on a `STATICCALL` callee) enforces EVM write protection: - `sstore`/`tstore`/`log0`–`log4`/`selfdestruct`, `create`/`create2`, and value-bearing - `call`/`callcode` halt exceptionally instead of modifying state. -- **Objects** — the Yul object layer (nested `code`/`data`/sub-objects): name resolution, a - layout-consistency predicate relating a compiler's byte layout to an object, and a symbolic proof - that the canonical constructor (`datacopy`/`return`) returns a data segment's bytes. -- **Surface tooling** — the `yul%` / `yulObject%` concrete-syntax DSL and a pretty-printer. -- **Optimization meta-theory** — pointwise program equivalence, congruence lemmas, and a - verified-pass skeleton. -- **Frame-boundary observation** — `revert`/`invalid`/`invalidMemoryAccess` roll the frame's - committed world changes back at the observation boundary (only the outcome marker and exposed - return data survive), while `stop`/`return`/`selfdestruct` and normal termination commit. This is - applied by `committedState` and the observed whole-program run `RunCommitted` (functional, given - determinism), matching real EVM. It lets a dead store before a revert be proven observationally - invisible (`deadStore_revert_obs_eq`) — something the raw exact-state relations cannot see. - -**Scope of the meta-theory (important).** The determinism proof, the executable interpreter, and the -adequacy theorem are established for the **closed-world local dialect `EVM.evm`** only. They do *not* -extend to the **open-world dialect `EVM.evmWithExternal` (call/create)**: - -- `evmWithExternal` is *relational and may be non-deterministic* (an external call/create outcome is - a response chosen by an arbitrary environment), so the determinism theorem does not apply to it. -- It has **no executable interpreter and no adequacy theorem**: there is deliberately no universal +## What is implemented + +- **Core semantics** ([`BigStep.lean`](./YulSemantics/BigStep.lean)) — the big-step relational + ground truth: lexical scoping, block-level function pre-collection (forward references and mutual + recursion), multiple return values, and `break`/`continue`/`leave`/`halt` outcome propagation. It + is a single indexed judgment (`Step`) over the five syntactic classes, with the five conceptual + relations recovered as abbreviations. +- **Determinism** ([`Determinism.lean`](./YulSemantics/Determinism.lean)) — `Step.det`: the judgment + is deterministic given deterministic built-ins, proven by one rule induction. Discharged for the + EVM dialect as `EVM.run_det`. +- **Executable interpreter + adequacy** ([`Interp.lean`](./YulSemantics/Interp.lean), + [`Adequacy.lean`](./YulSemantics/Adequacy.lean)) — a total fuel-indexed interpreter over an + `ExecDialect`, with a proven **adequacy** theorem (soundness at any fuel; completeness at + sufficiently large fuel for terminating runs). Instantiated hypothesis-free for EVM as + `EVM.run_adequacy`. +- **EVM dialect** ([`Dialect/EVM.lean`](./YulSemantics/Dialect/EVM.lean)) — the full user-facing Yul + EVM built-in set over `BitVec 256` (through the Fusaka fork, including `clz`, `mcopy`, `blobhash`, + `blobbasefee`). Covered: arithmetic/comparison/bitwise/shifts, memory (with the `msize` + active-memory high-water mark), storage and transient storage, calldata/code/returndata reads and + copies (`returndatacopy` bounds failure is an exceptional halt), the execution-environment and + world-state readers (via abstract environment maps), logs, the object-data ops, and the halting + ops. `keccak256` uses an environment-supplied oracle, abstract by default and executable when a + client supplies a concrete implementation. +- **Open-world calls and creation** — `call`/`callcode`/`delegatecall`/`staticcall` and + `create`/`create2` are interpreted relationally by `EVM.evmWithExternal calls creates`. The + supplied `ExternalCalls`/`ExternalCreates` relations describe *completed* external executions and + may summarize arbitrary nested calls, creations, and re-entrant callbacks; the semantics fixes only + the caller-observable boundary (memory copy-in, world commit/rollback, return-data copy-out, the + success/address word). `gas()` is a nondeterministic oracle in these dialects. See + [`DESIGN.md`](./DESIGN.md) for the exact boundary. +- **Static write protection** — a frame flagged static (`ExecEnv.static`, as set on a `STATICCALL` + callee) enforces EVM write protection: `sstore`/`tstore`/`log0`–`log4`/`selfdestruct`, + `create`/`create2`, and value-bearing `call`/`callcode` halt exceptionally instead of modifying + state; `staticcall`, `delegatecall`, and zero-value `call` remain permitted. +- **`selfdestruct`** — transfers the executing account's balance and halts, recording the scheduled + destruction together with its `createdThisTx` bit (post-EIP-6780: only an account created in the + current transaction is deletable; the self-beneficiary balance-burn distinction is modeled). Actual + fork-dependent deletion is a transaction-finalization step, outside this frame semantics. +- **Frame-boundary observation** ([`Observation.lean`](./YulSemantics/Observation.lean)) — + `revert`/`invalid`/`invalidMemoryAccess` roll the frame's committed world changes back at the + observation boundary (only the outcome marker and exposed return data survive), while + `stop`/`return`/`selfdestruct` and normal termination commit — matching real EVM. Applied by + `EVM.committedState` and the observed whole-program run `EVM.RunCommitted` (functional given + determinism). This makes dead-effect reasoning sound: `EVM.deadStore_revert_obs_eq` proves a dead + store before a revert is observationally invisible — something the raw exact-state relations cannot + see. +- **Effect classification** ([`Dialect.lean`](./YulSemantics/Dialect.lean)) — each built-in is + classified (deterministic / reads / writes / halts). The EVM dialect proves the classification + soundly over-approximates its semantics (`EVM.effects_sound`, and `EVM.effects_sound_withExternal` + for the open world). +- **Objects** ([`Object.lean`](./YulSemantics/Object.lean), + [`ObjectRun.lean`](./YulSemantics/ObjectRun.lean)) — the Yul object layer (nested + `code`/`data`/sub-objects): name resolution, a layout-consistency predicate relating a compiler's + byte layout to an object, and a symbolic proof that the canonical constructor (`datacopy`/`return`) + returns a data segment's bytes. +- **Surface tooling** ([`Syntax.lean`](./YulSemantics/Syntax.lean), + [`PrettyPrint.lean`](./YulSemantics/PrettyPrint.lean)) — the `yul%` / `yulObject%` concrete-syntax + DSL and a pretty-printer. +- **Optimization meta-theory** ([`Equiv.lean`](./YulSemantics/Equiv.lean), + [`Rewrites.lean`](./YulSemantics/Rewrites.lean)) — pointwise semantic equivalence for all five + syntactic classes, each proven an equivalence relation; congruence lemmas w.r.t. every AST + constructor (the workhorse for lifting local rewrites into any context); and worked sample rewrites + (constant folding, `add(x,0) ≈ x`). + +## What is not (yet) done, and why + +- **Yul→EVM compiler correctness.** Deliberately out of scope for this repo — it belongs to the + separate compiler project, which will instantiate the abstract `Dialect` with the real EVM + semantics and prove a conditional-on-gas forward simulation. See [`DESIGN.md`](./DESIGN.md). +- **Inlining / function-body congruence.** Rewriting *inside* a function body changes the `FDecl` + that block-hoisting stores, so it needs a relation on function environments threaded through the + judgment. That machinery belongs with function-level optimizations (inlining) and is deferred; the + current block congruence carries an explicit `hoist`-agreement side condition (`rfl` for rewrites + that do not touch top-level `funDef`s). +- **`reads`-flag soundness.** `EVM.effects_sound` proves the `deterministic`/`writes`/`halts` flags + sound; a machine-checked soundness for `reads` needs a notion of state observation (a read + footprint) and is deferred. The flag is documented and currently unused by any proof. +- **Program logic (Hoare / separation).** An optional layer on top of the relational semantics; + deferred until needed. Not required for the equivalence/simulation results. +- **Divergence reasoning.** Not needed for the main compiler theorem (the gas-metered target cannot + diverge), and deferred indefinitely. +- **Gas.** Not modeled by design (see [`DESIGN.md`](./DESIGN.md) §1). Within-frame out-of-gas is + therefore not expressible; out-of-gas in a callee is subsumed by the open-world call relation. + +### Scope of the meta-theory (important) + +The determinism proof, the executable interpreter, and the adequacy theorem are established for the +**closed-world local dialect `EVM.evm`** only. They do **not** extend to the **open-world dialect +`EVM.evmWithExternal` (call/create)**: + +- `evmWithExternal` is relational and may be non-deterministic (an external call/create outcome is a + response chosen by an arbitrary environment), so the determinism theorem does not apply to it. +- It has **no executable interpreter and no adequacy theorem** — there is deliberately no universal executable choice for an open-world relation. In the executable dialect (`EVM.evm` / `EVM.exec`), `gas()` and the call/create family are intentionally left **stuck** (no reduction). -- What *does* carry over to the open world is the effect-classification soundness - (`EVM.effects_sound_withExternal`); the call/create/`gas()` semantics are otherwise the boundary - described in [`DESIGN.md`](./DESIGN.md), not covered by the determinism/adequacy guarantees above. +- What *does* carry over to the open world is effect-classification soundness + (`EVM.effects_sound_withExternal`). -So: do not read "deterministic" or "adequate" as statements about programs that call `gas()` or make +So do not read "deterministic" or "adequate" as statements about programs that call `gas()` or make external calls/creations. -See the annotated build plan at the end of [`DESIGN.md`](./DESIGN.md) for details and open threads. +## Tests + +Correctness is carried by the theorems above; in addition the repository is exercised end-to-end: + +- [`Examples.lean`](./YulSemantics/Examples.lean) — interpreter runs via `native_decide` (arithmetic, + storage, memory and `msize`, the `returndatacopy` bounds exception, `selfdestruct`) and `yul%` DSL + round-trips. +- [`FibExample.lean`](./YulSemantics/FibExample.lean) — a full worked contract (see below). +- [`ObjectRun.lean`](./YulSemantics/ObjectRun.lean) — a concrete object whose layout is checked + consistent and whose constructor is run to its returned data segment. +- [`Dialect/EVM.lean`](./YulSemantics/Dialect/EVM.lean) and + [`Observation.lean`](./YulSemantics/Observation.lean) — inline guards for effect flags, the + `selfdestruct` cases, the open-world call/create/`gas()` boundary, static write protection, and the + commit/rollback observation. ## Worked example -[`YulSemantics/FibExample.lean`](./YulSemantics/FibExample.lean) is a first end-to-end verification: -a Yul contract that reads `n` from calldata, computes the `n`-th Fibonacci number, and returns it. -It is proven correct two ways: +[`FibExample.lean`](./YulSemantics/FibExample.lean) is an end-to-end verification: a Yul contract +that reads `n` from calldata, computes the `n`-th Fibonacci number, and returns it. It is proven +correct two ways: - **concretely**, by running the interpreter for several inputs (`native_decide`); and - **generally** (`fibContract_correct`): for *every* initial state the contract halts, writes diff --git a/YulSemantics/Ast.lean b/YulSemantics/Ast.lean index c587f83..fe5ec91 100644 --- a/YulSemantics/Ast.lean +++ b/YulSemantics/Ast.lean @@ -8,17 +8,17 @@ This module is deliberately dependency-light (no Mathlib): it is pure syntax. ## Modeling decisions (see `DESIGN.md`) -* **Built-ins are a first-class enum, parameterized (Option D).** The AST is parameterized over an +* **Built-ins are a first-class enum, and the AST is parameterized over it.** The AST is parameterized over an operation type `Op`; a call is either a dialect built-in (`Expr.builtin op args`, with `op : Op`) or a user-defined function call (`Expr.call fn args`, with `fn : Ident`). The core stays dialect-agnostic (it is generic in the *type* `Op`), while dialect-specific optimizations can pattern-match on `Op` structurally and dialect-agnostic passes are `∀ Op, …` — the type system - enforces the separation. Name→`Op` resolution happens at parse time (Phase 4), sound because Yul + enforces the separation. Name→`Op` resolution happens at parse time, sound because Yul forbids user functions from shadowing built-ins. * **Single-sorted.** The EVM dialect has one type (`u256`); type annotations carry no semantic content and are omitted (the DSL parses and discards optional `: TypeName`). * **Dialect-agnostic literals.** A `Literal` holds only *syntactic* data; a `Dialect` interprets it - (`litValue`, Phase 2). + (`litValue`). * **`Outcome` is dialect-agnostic.** Halting built-ins signal `.halt`; the payload lives in the machine state, not in `Outcome`. -/ @@ -48,7 +48,7 @@ inductive Literal * `call fn args` — a call to the *user-defined* function named `fn`. `DecidableEq`/`BEq` are intentionally not derived (the deriving handlers do not support recursion -through `List`); syntactic equality is first needed for the optimization proofs (Phase 5). -/ +through `List`); syntactic equality is first needed for the optimization proofs. -/ inductive Expr (Op : Type) | lit (l : Literal) | var (x : Ident) @@ -58,7 +58,7 @@ inductive Expr (Op : Type) /-- A Yul statement, parameterized over the built-in operation type `Op`. -Note on scoping (enforced by the semantics in Phase 3, not by the AST): +Note on scoping (enforced by the semantics, not by the AST): * function definitions are visible throughout their enclosing block (forward references allowed); * variables declared in a `forLoop`'s `init` block are visible in its `cond`, `post`, and `body`. -/ inductive Stmt (Op : Type) diff --git a/YulSemantics/Basic.lean b/YulSemantics/Basic.lean index 180189b..a124e6e 100644 --- a/YulSemantics/Basic.lean +++ b/YulSemantics/Basic.lean @@ -3,15 +3,15 @@ import Mathlib /-! # YulSemantics.Basic -Phase 0 placeholder: confirms the toolchain and Mathlib are wired up, and that the EVM word -type `BitVec 256` (see `DESIGN.md` §4) is available with its bitvector automation. +Confirms the toolchain and Mathlib are wired up, and that the EVM word type `BitVec 256` +(see `DESIGN.md` §4) is available with its bitvector automation. -Subsequent phases add: -* `YulSemantics.Ast` — AST + control-flow `Outcome` (Phase 1) -* `YulSemantics.Dialect` — abstract `Dialect` + EVM dialect instance (Phase 2) -* `YulSemantics.BigStep` — big-step relational semantics, the ground truth (Phase 3) -* `YulSemantics.Syntax` — concrete-syntax Yul DSL (Phase 4) -* `YulSemantics.Equiv` — behavior, contextual equivalence, congruence (Phase 5) +Module map: +* `YulSemantics.Ast` — AST + control-flow `Outcome` +* `YulSemantics.Dialect` — abstract `Dialect` + EVM dialect instance +* `YulSemantics.BigStep` — big-step relational semantics, the ground truth +* `YulSemantics.Syntax` — concrete-syntax Yul DSL +* `YulSemantics.Equiv` — behavior, contextual equivalence, congruence -/ namespace YulSemantics diff --git a/YulSemantics/Dialect.lean b/YulSemantics/Dialect.lean index 8818c6f..1243061 100644 --- a/YulSemantics/Dialect.lean +++ b/YulSemantics/Dialect.lean @@ -12,7 +12,7 @@ its built-in functions; a `Dialect` packages everything dialect-specific: * a (possibly non-deterministic) interpretation of built-ins (`Builtin`), and * an effect classification of built-ins (`effects`) used to justify optimizations. -The big-step semantics (Phase 3) is parameterized over a `Dialect`; the EVM instance lives in +The big-step semantics is parameterized over a `Dialect`; the EVM instance lives in `YulSemantics.Dialect.EVM`. See `DESIGN.md` §3. This module is dependency-light (no Mathlib): it only needs the AST. diff --git a/YulSemantics/Dialect/EVM.lean b/YulSemantics/Dialect/EVM.lean index 83e2c7a..16f2975 100644 --- a/YulSemantics/Dialect/EVM.lean +++ b/YulSemantics/Dialect/EVM.lean @@ -6,7 +6,7 @@ import YulSemantics.Dialect A gas-free reference instance of the EVM dialect, with `Value := BitVec 256` (see `DESIGN.md` §4). -Built-ins are a finite enum `Op` (Option D), covering the **full user-facing Yul EVM dialect** +Built-ins are a finite enum `Op`, covering the **full user-facing Yul EVM dialect** (through the Fusaka fork, incl. `clz` (EIP-7939), `mcopy`, `blobhash`, `blobbasefee`). `stepOp`/`effects` dispatch structurally on the constructor — fast to reduce and clean to prove about. The string↔`Op` correspondence (`opName`, `parse`) is confined to the frontend. diff --git a/YulSemantics/Equiv.lean b/YulSemantics/Equiv.lean index ca5fc77..198c3f3 100644 --- a/YulSemantics/Equiv.lean +++ b/YulSemantics/Equiv.lean @@ -4,8 +4,8 @@ import YulSemantics.BigStep /-! # YulSemantics.Equiv -Phase 5 foundations: **semantic equivalence** and its **congruence** properties — the layer -Yul→Yul optimization-pass correctness proofs stand on (see `DESIGN.md`). +The optimization meta-theory foundations: **semantic equivalence** and its **congruence** properties +— the layer Yul→Yul optimization-pass correctness proofs stand on (see `DESIGN.md`). ## Equivalences diff --git a/YulSemantics/Rewrites.lean b/YulSemantics/Rewrites.lean index 3ff974e..c88e888 100644 --- a/YulSemantics/Rewrites.lean +++ b/YulSemantics/Rewrites.lean @@ -5,8 +5,8 @@ import YulSemantics.Syntax # YulSemantics.Rewrites Sample **local rewrites** for the EVM dialect, proven as semantic equivalences and lifted through -the congruence lemmas of `YulSemantics.Equiv` — validating that the Phase 5 framework can carry an -optimizer's proof obligations: +the congruence lemmas of `YulSemantics.Equiv` — validating that the equivalence/congruence framework +can carry an optimizer's proof obligations: * constant folding: `add(2, 3) ≈ 5`; * algebraic identity: `add(x, 0) ≈ x` (for a variable `x`);