docs: reorganize README/DESIGN, drop phased-plan framing

README.md

@@ -3,17 +3,18 @@
 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.
 
 ## Design
 
 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

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)

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

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.

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.

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
 

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`);