diff --git a/.cursor/Dockerfile b/.cursor/Dockerfile deleted file mode 100644 index ce07d3a..0000000 --- a/.cursor/Dockerfile +++ /dev/null @@ -1,16 +0,0 @@ -FROM ubuntu:24.04 - -RUN apt-get update && apt-get install -y --no-install-recommends \ - ca-certificates \ - curl \ - git \ - python3 \ - build-essential \ - && rm -rf /var/lib/apt/lists/* - -ENV ELAN_HOME=/usr/local/elan -ENV PATH=/usr/local/elan/bin:$PATH - -RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \ - | sh -s -- -y --default-toolchain none --no-modify-path \ - && chmod -R a+w "$ELAN_HOME" diff --git a/.cursor/environment.json b/.cursor/environment.json deleted file mode 100644 index b7fe22b..0000000 --- a/.cursor/environment.json +++ /dev/null @@ -1,7 +0,0 @@ -{ - "name": "eip-8282 Lean 4.31", - "install": "bash .cursor/install.sh", - "build": { - "dockerfile": "Dockerfile" - } -} diff --git a/.cursor/install.sh b/.cursor/install.sh deleted file mode 100755 index 88636d1..0000000 --- a/.cursor/install.sh +++ /dev/null @@ -1,16 +0,0 @@ -#!/usr/bin/env bash -# Idempotent Cloud Agent install. Runs from the repo root on every Build. -set -euo pipefail - -export PATH="${ELAN_HOME:-$HOME/.elan}/bin:/usr/local/elan/bin:$PATH" - -if ! command -v elan >/dev/null 2>&1; then - curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \ - | sh -s -- -y --default-toolchain none - export PATH="$HOME/.elan/bin:$PATH" -fi - -elan toolchain install "$(cat lean-toolchain)" -lake update -# native_decide traces (and later kill-lines) need the keccak/sha2 FFI. -lake build EvmYul.FFI.ffi:dynlib diff --git a/AGENTS.md b/AGENTS.md deleted file mode 100644 index a4621d0..0000000 --- a/AGENTS.md +++ /dev/null @@ -1,33 +0,0 @@ -# Agent instructions - -This repository is Lean 4.31 evidence for three EIP-8282 predeploy guarantees -(P-SUBMIT-1, P-DRAIN-1, P-CONTROL-1). Lean theorem statements are authoritative. -`audit/guarantees.yaml` classifies them and must not overclaim. - -## Cursor Cloud specific instructions - -- Read `audit/CAMPAIGN.md` before writing proofs. That file is the campaign - source of truth (workers, modules, PR stack, bars). -- If you are the **orchestrator**, follow `audit/CLOUD_ORCHESTRATOR.md`. -- Environment: `elan` + toolchain in `lean-toolchain` (4.31.0). Always - `lake build EvmYul.FFI.ffi:dynlib` before compiling Eip8282 modules. -- Verify with `make prove` and the relevant kill-line module. Run - `python3 scripts/audit_metadata.py` before opening a PR. -- Do not add more finite `native_decide` traces as a substitute for `∀`. - Wave 5 (P-CONTROL-1 nonempty) and Wave 6 (P-SUBMIT-1 underpay + second - image; P-DRAIN-1 more stale slots) already landed on `main` at `85dab78`. -- Keep existing kill-lines. A new parent that a one-byte mutant cannot - refute is not load-bearing. -- No `sorry`. No project `axiom`. `native_decide` only for finite jumpdest - tables in `Eip8282/Audit/Jumpdests.lean` if still forced by `D_J_aux`. -- Do not edit sibling guarantee files from a claim worker. Integrators only - edit parent theorems, `Eip8282.lean`, `Trust.lean`, YAML, README. -- Do not merge the three campaign PRs to `main`. Humans review them in order - P-SUBMIT-1 → P-CONTROL-1 → P-DRAIN-1. - -## Local prove - -```bash -lake build EvmYul.FFI.ffi:dynlib -make prove -``` diff --git a/README.md b/README.md index 6db08e5..5c57748 100644 --- a/README.md +++ b/README.md @@ -1,237 +1,101 @@ # EIP-8282 Proof Closure -This repo holds Lean evidence for **three** EIP-8282 predeploy guarantees, -against pinned `ethereum/sys-asm@83f9801245ff56878a450b5625801101b9a225a1` -and the working EIP text at `lfglabs-dev/EIPs@b759aae8` (PR -[ethereum/EIPs#12120](https://github.com/ethereum/EIPs/pull/12120), stacked -diff [lfglabs-dev/EIPs#1](https://github.com/lfglabs-dev/EIPs/pull/1)). +This repository covers three guarantees: `P-SUBMIT-1`, `P-DRAIN-1`, and `P-CONTROL-1`. The bytes come from `ethereum/sys-asm@83f9801`. The working EIP text is `lfglabs-dev/EIPs@b759aae8` ([ethereum/EIPs#12120](https://github.com/ethereum/EIPs/pull/12120)). Lean decides what holds. `audit/guarantees.yaml` only classifies it. -Lean theorems decide what is proved. `audit/guarantees.yaml` only classifies -them. +## What is proved, and what is not -Each guarantee is evidenced in two layers: +The repository contains an executable Lean specification (`userCall` / `systemCall`) and proofs about the pinned hex. They are not yet proved equal. The remaining goal is, under a well-formed queue and enough gas: -1. **Abstract Lean 4 model** — the high-level algorithm. Supporting, not a substitute for bytecode. -2. **Pinned runtime bytecode under `EvmYul.EVM.Ξ`** — the real bytes, really executed. This is the load-bearing layer. +``` +Ξ(hex, call) = CFG stepper = Model +``` -| # | ID | Abstract Lean | Pinned bytecode | -| --- | --- | --- | --- | -| 1 | `P-SUBMIT-1` | CHECKED | CHECKED (`∀` under WellFormed / CallHyp, plus kill-line traces) | -| 2 | `P-DRAIN-1` | CHECKED | CHECKED (`∀` under WellFormed / CallHyp, system path, plus kill-line traces) | -| 3 | `P-CONTROL-1` | CHECKED | CHECKED (`∀` under WellFormed / CallHyp, plus kill-line traces) | - -### What the bytecode layer does and does not say - -`Eip8282.Audit.Guarantees.PSubmit1.psubmit1_forall_parent` is the registered -P-SUBMIT-1 parent. It is a CFG-level `∀` under `WellFormed` / `CallHyp` -(gas ≥ 30M, fuel ≥ 80000, user caller): every user-path `JUMPI @revert` -(bad `calldatasize`, underpay parameterized by the quoted fee, inhibitor, -value-on-getter, min-amount, stake) sits before the first `SSTORE`/`LOG0`; -a paying 184-byte deposit appends six calldata words at `tail*6` and -`LOG0`s the calldata; a paying 48-byte exit writes `CALLER` then pubkey -and `LOG0`s the 68-byte `msg.sender ‖ pubkey`; the empty-calldata getter -returns 32 bytes, and its completing CFG run records an empty `SSTORE` -overlay, so post-storage slots 0–3 read through that overlay equal the -pre-state (machine-derived, not a copy of the pre-state into the -observation); `fakeExponential` equals `Model.go` / `asmLoop` for all -excess (CFG fragment, **not** a proof that `Ξ` computes it). F4 left -`A-ABSTRACT-TX` open, so this is not `Ξ ↔ Model` and not -`unfold userCall`. - -The Wave-6 theorem `psubmit1_bytecode_parent` stays as a conjunct: it still -runs the pinned bytes of `pinned/bytecode/builder_{deposits,exits}/main.hex` -inside `EvmYul.EVM.Ξ` at two reachable-shaped images. What makes the parent -load-bearing rather than decorative is `Eip8282.Tests.PSubmit1Mutant`: -flipping **one byte** of the pinned deposit runtime (offset 158, `RETURN` → -`REVERT`) makes the *same* `submitFacts` evaluate to `false`; flipping the -user-path `LOG0` size at offset 274 (`PUSH1 184` → `PUSH1 0`) leaves the -six-word append intact but empties the log; and flipping the handle_input -fee `CALLVALUE` at offset 161 (`CALLVALUE` → `GAS`) lets an underpaying -184-byte deposit succeed and write. Those PCs are named on the CFG -fragments (`RETURN` suffix local 30, `CALLVALUE` handle_input relative 2, -`PUSH1 184` relative 114). The mutation is to bytecode, not to a model -function. `log_mutant_leaves_siblings_intact` and -`underpay_mutant_leaves_siblings_intact` prove those cuts leave -`PDrain1.drainFacts` and `PControl1.controlFacts` true. - -`Eip8282.Audit.Guarantees.PControl1.pcontrol1_forall_parent` is the registered -P-CONTROL-1 parent. It is a CFG-level `∀` under `WellFormed` / `CallHyp` -(gas ≥ 30M, caller class): `CALLER = SYSTEM_ADDR` iff the opening `EQ` / -`JUMPI` lands on `read_requests`; nonempty system calldata stores -`INHIBITOR`, inhibited+empty stores `0`, else `max(0, excess+count−TARGET)` -for targets 8 and 2 (queue length unused); a paid user wraps -`SLOT_COUNT += 1` and leaves excess, while a system `store_excess` writes -`SLOT_COUNT := 0` (mod 2^256); exit init stores `INHIBITOR` at slot 0 then -returns runtime, and deposit init does not `SSTORE`. F4 left -`A-ABSTRACT-TX` open, so this is not `Ξ ↔ Model` and not -`unfold userCall` / `systemCall`. - -The Wave-1 theorem `pcontrol1_bytecode_parent` and Wave-5 theorem -`pcontrol1_nonempty_bytecode_parent` stay as conjuncts: they still run the -pinned bytes inside `EvmYul.EVM.Ξ`. Wave 5's nonempty images -(`QUEUE_HEAD = 0`, `QUEUE_TAIL ∈ {2,17,65}`) drain (`368` / `11776` -deposit bytes, `136` / `1088` exit bytes) *and* fold `SLOT_EXCESS` to -`97` / `103` (or latch `INHIBITOR` / clear to `0`). Those return sizes -and `HEAD`/`TAIL` moves are false if the queue were empty, so the -nonempty traces are not a restatement of Wave 1. - -`Eip8282.Audit.Guarantees.PDrain1.pdrain1_forall_parent` is the registered -P-DRAIN-1 parent. It is a CFG-level `∀` under `WellFormed` / `CallHyp` -(gas ≥ 30M, fuel ≥ 80000, system caller `isUser = false`): system `SSTORE` -keys sit in `{SLOT_EXCESS, SLOT_COUNT, QUEUE_HEAD, QUEUE_TAIL}` so every -slot `n ≥ 4` is unchanged; `n = min(tail-head, capOf)` with wrap-free -`SUB`/`ADD`, the oldest `n` packed items, full-drain pointers `(0,0)` and -partial `HEAD += n` with `TAIL` unchanged, caps 64/16; deposit amount -bytes 80–87 are little-endian of the big-endian packed field `∀` drained -index; a user fee quote does not move `HEAD`/`TAIL`. F4 left -`A-ABSTRACT-TX` open, so this is not `Ξ ↔ Model` and does **not** claim -`Ξ` computes FIFO for every excess. - -The Wave-6 theorem `pdrain1_bytecode_parent` stays as a conjunct: it still -runs the pinned bytes inside `EvmYul.EVM.Ξ` at the sampled queue depths. - -P-CONTROL-1's kill-line, `Eip8282.Tests.PControl1Mutant`, feeds the same -`controlFacts` / `nonemptyControlFacts` the `∀` parent still contains: -builder_deposits offset 22 (`EQ` → `LT`), offset 571 (`PUSH1 8` → `9`), -and builder_exits offset 401 (`PUSH1 2` → `3`). With the gate cut, -`SYSTEM_ADDR` is answered as a user. With the deposit TARGET cut, -`depositQueue 2` stores excess `96` not `97`; with the exit cut, -`exitQueue 2` stores `102` not `103`. Those PCs are named on the CFG -fragments (`gateEqPc`, `update_excess` local 70). `wave5_mutants_leave_psubmit1_intact` -proves the TARGET cuts leave `PSubmit1.submitFacts` **true**. P-SUBMIT-1 -never calls from `SYSTEM_ADDR` and never reaches `compute_excess`, so the -parent is not a restatement of a sibling. - -P-DRAIN-1's kill-line, `Eip8282.Tests.PDrain1Mutant`, cuts six drain-only -bytes: the exit `MAX_PER_BLOCK` clamp at offset 244 (`PUSH1 16` → `PUSH1 8`), -the exit system `RECORD_SIZE` multiplier at offset 450 (`PUSH1 68` → -`PUSH1 64`), the deposit `MAX_PER_BLOCK` clamp at offset 304 -(`PUSH1 64` → `PUSH1 32`), the partial-drain `QUEUE_HEAD` store at -deposit offset 483 (`PUSH1 2` → `PUSH1 9`), the same deposit store -retargeted onto slot 196 (`PUSH1 2` → `PUSH1 196`, first word of drained -item 32), and the exit partial-drain `QUEUE_HEAD` store at offset 313 -(`PUSH1 2` → `PUSH1 25`, src word of drained exit item 7). Each makes the -*same* `drainFacts` evaluate to `false`, so `pdrain1_forall_parent` is -false of that bytecode. Those PCs are named on the CFG fragments -(exitClamp relative 18, depositClamp relative 19, `update_head+12`, -`store_excess+8`). With the exit-cap cut, seventeen -queued exits return 8 records and the head advances to 8; the under-cap -two-record drain is untouched. With the deposit-cap cut, sixty-five -queued deposits return 32 records and the head advances to 32; the -empty-queue and under-cap deposit drains are untouched. With the -Wave-3 head-slot cut, the 64-record drain still returns 11776 bytes but -writes the new head `64` into slot 9 (last remaining word of drained -item 0) instead of `QUEUE_HEAD`, so the remaining-word conjunct fails. -With the Wave-6 deposit head-slot cut, that same `64` is written into -slot 196 so `staleDepositPk1Is 32` fails. With the Wave-6 exit head-slot -cut, the new head `16` is written into slot 25 so `staleExitSrcIs 7` -fails. After the same traces the parent also pins leftover storage: all -six words of deposit item 0, all five remaining words of deposit item 1, -the first word of deposit item 32, all six words of deposit item 63, -still-queued deposit item 64, and all three words of exit items 0, 7 and -15. `drain_mutants_leave_siblings_intact` proves all six mutants leave -`PSubmit1.submitFacts` and `PControl1.controlFacts` **true**: -P-SUBMIT-1 never calls from `SYSTEM_ADDR`, and P-CONTROL-1's empty-queue -facts hold `QUEUE_HEAD = QUEUE_TAIL = 0`, so the partial-drain head -stores are never taken and `0 * RECORD_SIZE` is still 0. - -Two disclosed costs, both in `audit/assumptions.yaml`: - -- `A-NATIVE-DECIDE` — a cost limitation, not an irreducible definition. The - four pinned images contain no `SHA3`, `BLOCKHASH`, call/create or - precompile-dispatch opcode and `EvmRunner.run` applies `EVM.Ξ` directly - instead of decoding transaction RLP, so the `opaque` `@[extern]` FFI - constants and the `partial` RLP decoders are never reached; what the - kernel cannot do is evaluate up to 80 000 interpreter steps of `Ξ`. - `native_decide` is forced on the kept - P-SUBMIT-1, P-CONTROL-1, and P-DRAIN-1 traces; the Lean compiler and the - EVMYulLean interpreter join the trusted base for those theorems. - `Eip8282.Audit.Trust` prints exactly which theorems carry it. The CFG - `∀` conjuncts of `psubmit1_forall_parent`, `pcontrol1_forall_parent`, - and `pdrain1_forall_parent` must not add `sorryAx`. - It no longer covers the jumpdest tables. EVMYulLean `0ff72b2` makes `D_J` - structurally recursive, so `deposit_D_J` / `exit_D_J` / `depositInit_D_J` / - `exitInit_D_J` are `decide +kernel`. The three parents now say so in their - own statements: `psubmit1_forall_parent`'s revert conjuncts quantify over - `D_J depositRuntime ⟨0⟩` / `D_J exitRuntime ⟨0⟩` directly, and - `pdrain1_forall_parent` / `pcontrol1_forall_parent` carry - `Eip8282.Audit.Step.validJumps_are_Xi_tables` as their leading conjunct. - The table the CFG layer steps is Ξ's own analysis of the pinned bytes, - kernel-checked, not a hand-written array that happens to look right. -- `A-EVM-WORLD` — the world is synthetic (two accounts). All three `∀` - parents are under `WellFormed` / `CallHyp`. `A-ABSTRACT-TX` stays: F4 - did not prove `Ξ ↔ Model`. - -Deployment provenance is still out of the current claim, but C4 no longer -stops at a CFG prefix. `PControl1.CtorXi.pcontrol1_ctor_xi_parent` runs the -full pinned 638-byte deposit and 503-byte exit init images under -`EvmYul.EVM.Ξ` and pins the buffer each returns to be `depositRuntime` / -`exitRuntime` byte for byte — the `code` that `Λ`'s step (115) installs — -with the exit ctor leaving slot 0 at `INHIBITOR`. That is what ties -`pinned/bytecode/*/ctor.hex` to `pinned/bytecode/*/main.hex`; -`audit/artifacts.lock.json` hashes the two files independently. - -It is deliberately not `Λ` itself. `Λ` derives its address as -`KEC(RLP(sender, nonce))`, and the EIP-8282 contracts are genesis -predeploys, not `CREATE` outputs — so driving `Λ` would pin an address -that is provably not the predeploy address. No address derivation is -claimed, and `A-PINNED-SOURCE` stays **open**: nothing here observes chain -state. What remains is a single observation — the live codehash at -`0x0000bFF4…` / `0x000064D6…` against keccak of the pinned `main.hex`. - -The three IDs are the smallest coherent audit surface: - -1. **submission** — admission, money, atomic rejection, authentic append, caller binding; -2. **drain** — FIFO conservation, caps, encoding, queue reuse; -3. **control state** — fee, count, initial gating, reversible inhibition. - -Wording, assumptions, source spans, next gates: `audit/guarantees.yaml`. - -## Reproduce +If that equality is proved, a universal Model theorem becomes a universal EVM theorem. It is still open as `A-ABSTRACT-TX`. + +Each bytecode guarantee is also checked against a one-byte mutant of the pinned runtime. The same parent fact must become false. These mutants are the kill-lines. + +## Three kinds of evidence + +**Abstract theorems.** `userCall` and `systemCall` are functions on a small state where the queue is a list. Their theorems cover the product rules: paid admission, FIFO caps, and the excess fold. They do not execute the predeploy bytes. + +**Universal theorems.** For every well-formed queue (slots 0-3 packed, `HEAD ≤ TAIL`), named claims hold. Some claims execute one opcode at one program counter in a small CFG stepper. Others are algebraic, such as FIFO pointer motion, amount encoding, and `fakeExponential`. Algebraic lemmas are not stepped bytecode. + +The jumpdest tables used by those CFG proofs are now kernel-checked as the same `D_J` tables computed from the pinned bytes by `EvmYul.EVM.Ξ`. This removed four uses of `native_decide`. It did not prove the full equality above. + +**Concrete Ξ traces.** `Ξ` executes one fixed call against one fixed storage image. This is an instance, not a universal theorem. These traces still use `native_decide`, which adds a compiler-generated axiom per theorem. The Lean compiler and EVMYulLean interpreter therefore remain in the trusted base for those facts (`A-NATIVE-DECIDE`). + +## Ξ transport and reachability + +`Eip8282.Audit.XiTransport` carries the three registered parents from the CFG layer to complete-`Ξ` observations. Three layers there are unconditional: the `X` → `Ξ` observation wrapper, the jumpdest agreement (`Ξ` derives the kernel-checked `D_J` tables from the pinned bytes itself), and the exit-instruction layer — the call observes exactly the halting instruction the run exits on, and `RETURN` / `REVERT` publish exactly the memory slice their own operands select. + +What is still assumed is the endpoint: `ExitAgrees` — that `Ξ` on the pinned runtime realises `userCall` / `systemCall` — remains an explicit hypothesis. It is the same premise previously called `EndpointAgrees`. Four branches now discharge that residual outright rather than assume it: `P-SUBMIT-1`'s inhibited and accepting paths, `P-DRAIN-1`'s empty-window branch, and `P-CONTROL-1`'s paid fee-getter branch. The universal endpoint proof, over every user and system path, is not there. `A-ABSTRACT-TX` stays open. + +`Eip8282.Audit.UserXiCorrespondence` and `Eip8282.Audit.SystemXiCorrespondence` compose whole user-call and SYSTEM-call `Ξ` observations against `Model.step`. The user side is joined to the packed world by `Eip8282.Audit.Represents`; the SYSTEM side carries its own minimal relation over the pinned predeploy account rather than reusing that API. What they compare is an observation — status and return bytes — not equality of EVM and model states, and they too take the endpoint premise explicitly. They narrow what is assumed without discharging it, and they introduce no parent IDs. + +`Eip8282.Audit.Reachable` closes the coverage direction inside the packed-storage layer: the constructor post-images are `WellFormed` and map to `Model.Reachable`, and both an append and a system call preserve that. So every reachable image satisfies the guard the three parents quantify over, and `A-REACHABLE` is no longer assumed for coverage. This layer never runs `Ξ`, so it does not discharge `ExitAgrees` either; the realisation gap stays under `A-ABSTRACT-TX`. + +## Constructor evidence + +The full pinned deposit and exit init images are also executed under `Ξ`. The proof checks that each returns the pinned runtime byte for byte, and that the exit constructor writes `INHIBITOR` to slot 0. + +This closes the constructor-to-runtime half of provenance. It does not identify deployed chain state. `A-PINNED-SOURCE` remains open until the live predeploy codehashes can be compared with the pinned runtimes. + +## Build and test Needs [elan](https://github.com/leanprover/elan) and Lean 4.31.0. ```bash -make audit-check +# Check the Lean toolchain. +make bootstrap + +# Build the full proof project. make prove + +# Build the proof project and all model/bytecode mutant tests. +make test + +# Run every local gate: metadata, proofs, and mutant tests. make check ``` -`make prove` first runs `lake build EvmYul.FFI.ffi:dynlib`. That is not -optional: `native_decide` runs the compiled EVMYulLean interpreter, which -needs the keccak/sha2 FFI as shared objects. `lakefile.lean` passes both to -`lean` via `--load-dynlib`, `libleanffi.so` first (otherwise `memset_zero` is -unresolved). - -One guarantee, plus its kill-line: +Successful runs end with: -```bash -lake build EvmYul.FFI.ffi:dynlib -lake build Eip8282.Audit.Guarantees.PSubmit1 Eip8282.Tests.PSubmit1Mutant +```text +prove ok: abstract model, three guarantees, and the P-SUBMIT-1 / P-DRAIN-1 / P-CONTROL-1 bytecode parents built +test ok: model mutants and the P-SUBMIT-1 / P-DRAIN-1 / P-CONTROL-1 bytecode kill-lines compiled +check ok ``` -## Layout +`make check` is the simplest way to reproduce the full CI gate locally. The GitHub Actions `prove` job runs the same build, kill-line modules, and metadata check on every pull request. + +## Snapshot status + +This snapshot is `main` at `25036b8`. Verified against GitHub on 2026-09-01: + +| Work | PR | Merge commit | State | +| --- | --- | --- | --- | +| Node 3 — jumpdest tables as `Ξ`'s own `D_J` | [#18](https://github.com/lfglabs-dev/eip-8282-proof-closure/pull/18) | `7204723` | merged into `main` | +| R5 — reachable `WellFormed` storage closure | [#25](https://github.com/lfglabs-dev/eip-8282-proof-closure/pull/25) | `8693add` | merged into `main` | +| R4 — transport the three parents to complete-`Ξ` `∀` | [#24](https://github.com/lfglabs-dev/eip-8282-proof-closure/pull/24) | `0ddb6c4` | merged into `main` | +| R4 — discharge `P-SUBMIT-1`'s rejected branch | [#26](https://github.com/lfglabs-dev/eip-8282-proof-closure/pull/26) | `f1bd9d0` | merged into `main` | +| R3 — whole SYSTEM-call `Ξ` correspondence | [#23](https://github.com/lfglabs-dev/eip-8282-proof-closure/pull/23) | `10bab70` | merged into `main` | +| Node 4 — C4 code-deposit half under `Ξ` | [#19](https://github.com/lfglabs-dev/eip-8282-proof-closure/pull/19) | `18227b9` | merged into `main` | +| R2 — whole user-call `Ξ` correspondence | [#22](https://github.com/lfglabs-dev/eip-8282-proof-closure/pull/22) | `25036b8` | merged into `main` | +| R1 — packed EVM world to `Model.State` | [#21](https://github.com/lfglabs-dev/eip-8282-proof-closure/pull/21) | — | closed unmerged; superseded by #22 | + +Every line of work described above is now on `main`. `R1` was closed without merging: its `Represents` relation reached `main` through `R2` instead, so `Eip8282.Audit.Represents` is present even though `#21` is not. + +That the correspondence PRs merged does not mean the endpoint premise is proved. `R2` and `R3` compose whole-call observations *under* `ExitAgrees`; none of them discharges it universally. -- `Eip8282/Audit/` — abstract model, `Bytecode` pins, the `EvmRunner` Ξ driver, - guarantee modules, trust report, facade -- `Eip8282/Tests/` — model mutants and the P-SUBMIT-1 / P-DRAIN-1 / P-CONTROL-1 bytecode kill-lines; not public guarantees -- `audit/` — registry, source map, assumptions, pins, universal-`∀` campaign (`CAMPAIGN.md`, orchestrator prompt) -- `AGENTS.md` / `.cursor/` — Cloud Agent environment (Lean 4.31) and campaign rules -- `pinned/` — frozen sys-asm sources, bytecode and EIP text (sha256-locked; - `scripts/audit_metadata.py` also checks the Lean hex literals against them) -- `scripts/` — fail-closed checks +Two `HIGH` assumptions remain open, and this snapshot does not close either: -## Scope +- `A-ABSTRACT-TX` — no universal proof that `Ξ` agrees with `Model.userCall` / `systemCall`. R4 makes the `X` → `Ξ`, jumpdest, and exit-instruction layers unconditional and discharges four named branches; R2 and R3 compose whole calls under the same explicit premise; R5 works on the packed-storage side only. The `∀`-endpoint proof is absent. +- `A-PINNED-SOURCE` — the pinned files are snapshots, not observed chain state. Node 4 closes the ctor-to-runtime half within the pin; no deployed codehash is claimed. It stays open until chain activation lets the live codehashes be observed. -In scope: Builder Deposit `0x0000bFF46984e3725691FA540a8C7589300D8282` and -Builder Exit `0x000064D678505ad48F8cCb093BC65613800E8282`. +Pinned references: `ethereum/sys-asm@83f9801`, `lfglabs-dev/EIPs@b759aae8`, EVMYulLean `b6258665`. -Out of scope: EIP-7732 bidding, consensus-layer handling, BLS validity, -EIP-7685 wrapping, and on-chain deployment identity. +## Out of scope -## Universal `∀` campaign +EIP-7732 bidding, consensus-layer handling, BLS validity, EIP-7685 wrapping, and on-chain deployment identity. -P-SUBMIT-1, P-CONTROL-1, and P-DRAIN-1 public parents are now those `∀` -theorems (`forall/psubmit1`, `forall/pcontrol1`, `forall/pdrain1`). -Plan, worker split, and PR stack: `audit/CAMPAIGN.md`. Single Cloud -orchestrator prompt: `audit/CLOUD_ORCHESTRATOR.md`. +Addresses: deposit `0x0000bFF46984e3725691FA540a8C7589300D8282`, exit `0x000064D678505ad48F8cCb093BC65613800E8282`. diff --git a/audit/CAMPAIGN.md b/audit/CAMPAIGN.md deleted file mode 100644 index fc7b4ef..0000000 --- a/audit/CAMPAIGN.md +++ /dev/null @@ -1,215 +0,0 @@ -# Universal bytecode campaign - -Replace finite `EvmYul.EVM.Ξ` traces with `∀` parents under well-formed -storage and enough gas. The abstract `Model` stays as the spec; -correspondence (`A-ABSTRACT-TX`) is how those `∀` lemmas become bytecode -facts. More `native_decide` images are **not** this campaign. - -Orchestrator prompt: `audit/CLOUD_ORCHESTRATOR.md`. - -## Status (main @ `fca9c1b`) - -Waves A–D are **done**: #11 (P-SUBMIT-1), #12 (P-CONTROL-1), #13 -(P-DRAIN-1) landed the CFG `∀` parents with the Wave-1/5/6 Ξ traces kept -as kill-line witnesses. `A-ABSTRACT-TX` (Ξ ↔ Model/CFG) remains open and -is honestly classified PARTIAL in `audit/guarantees.yaml`; closing it needs -a Ξ ↔ Model/CFG correspondence, not more traces here. (The `D_J_aux` -half of that blocker is gone: EVMYulLean `0ff72b2` made it structurally -recursive and the jumpdest tables are now `decide +kernel`.) - -**#14 merged** (`cursor/psubmit1-parent-honesty-5c89`, branch kept): -P-SUBMIT-1 parent strength — the fee-getter conjunct observes post-storage -from the CFG machine (the completing run's `SSTORE` overlay is proved -empty) instead of copying pre-state slots into the observation, and the -exit append conjunct exports the LOG0 payload `msg.sender ‖ pubkey` from -`Append.exit_handle_input_append`. No new IDs, no new traces, kill-line -unchanged. This closes the "P-SUBMIT-1 honesty / parent strength" gap; -no campaign gaps remain except `A-ABSTRACT-TX` (blocked upstream). - -## Baseline (do not redo) - -`origin/main` at **`85dab78`** already has: - -| Landed | What it is | Still not | -| --- | --- | --- | -| P-CONTROL-1 Wave 5 (#8) | Nonempty-queue excess fold on `Ξ`; parent `pcontrol1_nonempty_bytecode_parent` | `∀` excess/count; exit ctor | -| P-SUBMIT-1 Wave 6 (#9) | Underpay revert + second storage image (`50/3/2/6`) | `∀` calldata/value/storage; `revertFreezesSlots` is runner-API (`storageSlotAfter = none` on any revert), load-bearing part is the revert itself | -| P-DRAIN-1 Wave 6 (#10) | More leftover words (deposit 0/1/32/63/64, exit 0/7/15) | `∀` drained indices; SSTORE-footprint lemma | - -Closed as superseded: PR **#7** (same Wave 5 as #8, conflicted). - -Do **not** spend workers on extra trace depths, extra stale indices, or a -third submit image. Jump to CFG / correspondence / `∀`. - -## Method - -`native_decide` only closes ground terms. A `∀` parent cannot be discharged -that way. Two further points: - -1. `D_J_aux` is **no longer** `partial` — EVMYulLean `0ff72b2` made it - structurally recursive (fuel = `c.size`), so the JUMPDEST sets of the - **pinned** images are ground terms the kernel reduces. Prove them once - (F1) with `decide +kernel`, not `native_decide`; later lemmas use those - tables and the `validJumps = D_J _ ⟨0⟩` bridges. Already landed for the - two runtime and two init images. -2. `∀` over raw EVM storage is the wrong theorem. Use `WellFormed` (packed - records, `head ≤ tail`, slots 0–3). The model already uses a list queue. - -Preferred path: prove `Ξ` agrees with `Model.userCall` / `systemCall` on -well-formed states (F4). Claim workers then transport model `∀` and add -what the model omitted (`LOG0`, stale slots, ctors). - -Fallback if F4 slips: CFG-direct `∀` for revert/append/gate/excess/footprint; -leave `A-ABSTRACT-TX` open; do not block ctors or drain footprint on a -complete simulation. - -Hypotheses allowed on every `∀`: `WellFormed`, gas ≥ 30M, interpreter fuel -bound, caller class (`SYSTEM_ADDR` vs not). Not “whatever is in storage.” - -## Counts - -| Role | IDs | How many | -| --- | --- | --- | -| Foundation workers | F1–F4 | **4** | -| Claim workers | S1–S4, C1–C4, D1–D3 | **11** | -| Integrators | IS, IC, ID | **3** | -| Public PRs | stacked on `main` | **3** | -| **Total agents** | orchestrator + above | **1 + 18** if fully fan-out; orchestrator may do integrate itself | - -Best-of-n (run 2–3, keep the one that builds): **F1**, **F4**, **S4**, **D2**. - -## Waves - -``` -F1 Jumpdests F2 WellFormed - \ / - F3 Stepper - | - F4 Model ↔ Ξ - / | \ - S1–S4 C1–C4 D1–D3 - | | | - IS IC ID - | | | - PR1 → PR2, PR3 (PR3 rebases onto PR2 after PR2 merges) -``` - -- **Wave A** — F1 and F2 in parallel from `main`. F3 after F1. F4 after F2+F3. - Merge onto `forall/foundation`. Do not open a PR to `main` yet. -- **Wave B** — 11 claim workers from `forall/foundation`, parallel, each on - its own `cursor/…` branch. Start only after `lake build` of foundation. -- **Wave C** — integrators write the three parent theorems + YAML. -- **Wave D** — humans review and merge **PR1 then PR2 then PR3**. Agents - do **not** merge to `main`. - -## Git - -| Branch | Base | Touches | -| --- | --- | --- | -| `forall/foundation` | `main` @ `85dab78` | `Jumpdests.lean`, `WellFormed.lean`, `Step.lean`, `Correspondence.lean` | -| `forall/psubmit1` | `forall/foundation` | `PSubmit1/*` + parent/YAML/Trust for submit | -| `forall/pcontrol1` | `forall/psubmit1` | `PControl1/*` + control YAML | -| `forall/pdrain1` | `forall/psubmit1` | `PDrain1/*` + drain YAML; rebase onto `pcontrol1` after PR2 merges | - -Each cloud worker uses a **new** `cursor/…` branch (`workOnCurrentBranch: false`). -Do not have two workers push the same branch. - -## Shared modules (Wave A only) - -| File | Owner | Done when | -| --- | --- | --- | -| `Eip8282/Audit/Jumpdests.lean` | F1 | `D_J` of `depositRuntime` and `exitRuntime` is a concrete finite set | -| `Eip8282/Audit/WellFormed.lean` | F2 | Packed queue, `head ≤ tail`, slot 0–3 meaning, both predeploys | -| `Eip8282/Audit/Step.lean` | F3 | Opcode-at-PC; `CALLER == SYSTEM_ADDR` iff `read_requests`; enough-gas explicit | -| `Eip8282/Audit/Correspondence.lean` | F4 | Well-formed storage: `EvmRunner`/`Ξ` matches `userCall`/`systemCall` | - -Claim workers treat these as **read-only**. - -## Claim workers - -User path = caller ≠ `SYSTEM_ADDR`. System path = `SYSTEM_ADDR`. - -### P-SUBMIT-1 (PR1, merge first; carries foundation) - -| ID | Module | Done when | -| --- | --- | --- | -| S1 | `PSubmit1/Revert.lean` | Every `jumpi @revert` is before first `SSTORE`/`LOG0`. Inhibitor, **bad `calldatasize`** (not just empty vs 184/48 — Wave 6 did not cover this), value-on-getter, underpay (Wave 6 sampled; now `∀` fee), min-amount, stake | -| S2 | `PSubmit1/Append.lean` | `∀` 184-byte paying deposit: six words at `tail*6`, `LOG0` = calldata. `∀` 48-byte paying exit: slot0 = `CALLER`, `LOG0` = sender‖pubkey | -| S3 | `PSubmit1/Fee.lean` | Empty calldata, value 0: 32-byte return, slots 0–3 unchanged, `∀` excess/count. **Not** `fake_expo` equality | -| S4 | `PSubmit1/FakeExpo.lean` | Pinned `fake_expo` equals `Model.fakeExponential` for all excess. Hardest submit lemma. Shared with control quotes | - -Wave 6 already samples underpay at two quotes (357/427 and 18/19). S1 must -generalise, not add a third image. - -### P-CONTROL-1 (PR2, merge second) - -Excess **does not use queue length**. C2 ignores FIFO. Ctor is init bytecode. - -| ID | Module | Done when | -| --- | --- | --- | -| C1 | `PControl1/Gate.lean` | `∀` callers: `CALLER = SYSTEM_ADDR` iff system subroutine | -| C2 | `PControl1/Excess.lean` | `∀` excess, count, calldata length: nonempty → `INHIBITOR`; inhibited+empty → 0; else `max(0, excess+count−TARGET)` for targets 8 and 2 | -| C3 | `PControl1/Count.lean` | Paid user: `SLOT_COUNT += 1`, excess unchanged. System: `SLOT_COUNT := 0`. `∀` prior count (mod 2^256) | -| C4 | `PControl1/Ctor.lean` | `exitInit` / `depositInit` under `Ξ`. Exit stores `INHIBITOR` at slot 0 then returns runtime. Deposit leaves storage zero. Closes `initial_gating` on bytes | - -Wave 5 already samples nonempty drain+fold. C2 is the `∀` recurrence, not -more `TAIL ∈ {2,17,65}` traces. - -### P-DRAIN-1 (PR3, merge last) - -| ID | Module | Done when | -| --- | --- | --- | -| D1 | `PDrain1/Footprint.lean` | System `SSTORE` targets ⊆ `{SLOT_EXCESS, SLOT_COUNT, QUEUE_HEAD, QUEUE_TAIL}` → `∀` stale-slot non-erasure (Wave 6 only sampled indices) | -| D2 | `PDrain1/Fifo.lean` | `accum_loop`: oldest `min(length, cap)` records; HEAD advances or both pointers zero on full drain; caps 64 and 16. Hardest drain lemma | -| D3 | `PDrain1/Encode.lean` | Deposit amount BE storage → LE return, `∀` queued items. User fee quote does not move HEAD/TAIL | - -## Integrators - -Only IS/IC/ID edit `PSubmit1.lean` / `PControl1.lean` / `PDrain1.lean` -parents, `Eip8282.lean` imports, `Trust.lean`, `audit/guarantees.yaml`, -README. - -Re-register the public parent as the `∀` conjunction. **Keep** -`submitFacts` / `drainFacts` / `controlFacts` traces as kill-line -witnesses. The existing one-byte mutants must still make the **new** parent -false. Sibling independence must still hold. - -YAML: `evm.scope` moves off `CONCRETE_TRACES` toward the stated hypotheses. -Close or shrink `A-EVM-WORLD` and `A-ABSTRACT-TX` only when Lean actually -does. `python3 scripts/audit_metadata.py` must pass. - -## Three PRs (Wave D — humans merge) - -1. **P-SUBMIT-1 `∀` on pinned user path** — foundation + S*. First time - reviewers see the stepper. Largest diff. -2. **P-CONTROL-1 `∀` control plane** — stacks on 1. Gate, excess, count, ctors. -3. **P-DRAIN-1 `∀` FIFO** — stacks on 1, rebase onto 2 after it merges. - -`autoCreatePR: true` only for these three. Foundation/claim workers push -branches only. - -## Worker rules - -1. One module, named above. Do not edit sibling guarantee files. -2. No `sorry`. No new `axiom`. F1 finite tables are `decide +kernel`; - `native_decide` stays only on the kept `Ξ` trace and mutant theorems. -3. Do not delete `Model.lean`. Correspondence uses it. Do not re-register - `unfold userCall` as the parent. -4. Do not weaken existing concrete traces until the `∀` parent implies them. -5. Do not merge to `main`. - -## PR allow-list (integrator) - -A guarantee PR is allowed only when: - -- `lake build` of the guarantee + its mutant module succeeds -- Kill-line still falsifies the **new** parent -- Sibling facts stay true on that mutant -- YAML `parent` matches the Lean name -- `Trust.lean` `#print axioms` for the new parent has no undisclosed axiom - -## Fallback - -If F4 correspondence slips: ship PR1 with CFG-direct `∀` for revert and -append only, keep fee numeric traces, leave `A-ABSTRACT-TX` open. C4 and D1 -must not wait on a complete Model simulation. diff --git a/audit/CLOUD_ORCHESTRATOR.md b/audit/CLOUD_ORCHESTRATOR.md deleted file mode 100644 index d2476f8..0000000 --- a/audit/CLOUD_ORCHESTRATOR.md +++ /dev/null @@ -1,28 +0,0 @@ -# Cloud orchestrator prompt - -Paste the block below as the **entire** first message of a Cursor Cloud -agent on `lfglabs-dev/eip-8282-proof-closure`, base `main`. Runtime: Cloud. -`autoCreatePR` only for the three guarantee PRs at the end. - ---- - -You are the orchestrator for the universal-bytecode campaign in this repo. - -Read `audit/CAMPAIGN.md` and `AGENTS.md` first. They are the source of truth. -Baseline is `main` at `85dab78` (P-CONTROL-1 Wave 5 and P-SUBMIT-1 / P-DRAIN-1 Wave 6 already merged). Do not add more finite `native_decide` traces. Do not revive closed PR #7. - -You create and drive **18 workers** and **3 stacked PRs**: - -- Wave A — 4 foundation workers: F1 Jumpdests, F2 WellFormed, F3 Stepper, F4 Correspondence (F1 and F2 in parallel from `main`; F3 after F1; F4 after F2+F3). Best-of-3 on F1 and F4. Merge their branches into `forall/foundation`. Do not open a PR to `main` for foundation. -- Wave B — 11 claim workers in parallel from `forall/foundation`, each on its own `cursor/…` branch, each owning exactly one module listed in `audit/CAMPAIGN.md`: S1 Revert, S2 Append, S3 Fee, S4 FakeExpo (best-of-3); C1 Gate, C2 Excess, C3 Count, C4 Ctor; D1 Footprint, D2 Fifo (best-of-3), D3 Encode. -- Wave C — 3 integrators: IS, IC, ID. They re-register the public parents as `∀` theorems, keep the existing kill-lines, update `Trust.lean` / `audit/guarantees.yaml` / README / `Eip8282.lean` imports. YAML must match Lean. `python3 scripts/audit_metadata.py` must pass. -- Wave D — open **exactly 3 PRs**, do not merge them: - 1. P-SUBMIT-1 `∀` (includes foundation) — base `main`, branch `forall/psubmit1` - 2. P-CONTROL-1 `∀` — stacked on PR 1 - 3. P-DRAIN-1 `∀` — stacked on PR 1; rebase onto PR 2 after PR 2 exists - -Humans merge those PRs later in order submit → control → drain. - -Fan-out with Cloud subagents / parallel Cloud agents, one module per worker. `workOnCurrentBranch: false`. No `sorry`. No project `axiom`. F1 jumpdest tables are `decide +kernel` (EVMYulLean `0ff72b2` made `D_J_aux` structurally recursive); `native_decide` stays only on the kept `Ξ` trace and mutant theorems. `lake build EvmYul.FFI.ffi:dynlib` before compiling. Stop when the three PRs are open and green, and reply with their URLs. - ---- diff --git a/audit/WAVE0.md b/audit/WAVE0.md deleted file mode 100644 index d19a68c..0000000 --- a/audit/WAVE0.md +++ /dev/null @@ -1,249 +0,0 @@ -# Wave 0 — load-bearing review (2026-08-19; honesty pass after #11–#14) - -Bar: a registered parent is load-bearing only if -1. its conclusion is not a tautology / restated hypothesis / definitional fact, -2. a kill-line mutant refutes *that parent*, not a sibling or disconnected model, -3. YAML/report scope matches what Lean actually proves, -4. the execution plane is **pinned EIP-8282 bytecode** under **EVMYulLean `EVM.Ξ`**, - not an abstract `userCall`/`systemCall` model. - -Live `main` at `739a4e7` (and this foundation commit) **failed the bar for all three IDs**. -Waves 1–6 re-registered the parents on pinned bytecode under `EVM.Ξ`. Waves A–D -(#11 P-SUBMIT-1, #12 P-CONTROL-1, #13 P-DRAIN-1) then re-registered each parent -as a CFG-level `∀` under `WellFormed` / `CallHyp`, keeping the Wave-1/5/6 `Ξ` -traces as kill-line witnesses. #14 closed the P-SUBMIT-1 parent-strength honesty -gap. Live YAML matches that: `P-SUBMIT-1` is `WELL_FORMED_FORALL`, `P-DRAIN-1` -and `P-CONTROL-1` are `CFG_FORALL`. `A-EVM-WORLD` is the synthetic two-account -world around those `∀` parents plus the kill-line traces — **not** “drain and -control are finite traces only.” `A-ABSTRACT-TX` remains open; F4 did not close -Ξ ↔ Model. - -BYTECODE, LOG0, and STALE-SLOTS are **no longer exclusions**. They landed -(Waves 1–6 + CFG `∀`). Still excluded: BLS PoP, EIP-7732 bidding, CONSENSUS -credit / request-hash. - -## P-SUBMIT-1 — DEFECTIVE (addressed; see below) - -> **Wave 1 status.** The registered parent is now -> `PSubmit1.psubmit1_bytecode_parent`, which executes -> `pinned/bytecode/builder_{deposits,exits}/main.hex` under `EVM.Ξ`. The -> kill-line `Eip8282.Tests.PSubmit1Mutant.mutant_refutes_parent` flips one -> byte of the deposit runtime and refutes that same parent. Bar items 1, 2 -> and 4 are met; item 3 held for the Wave-1 declared scope, which was -> concrete traces at one storage image. That is no longer the registered -> scope: live YAML is `WELL_FORMED_FORALL` (`psubmit1_forall_parent`) plus -> these traces as the kill-line. `A-EVM-WORLD` is the synthetic world around -> that `∀` + traces, not “finite traces only.” `native_decide` is forced -> by `D_J_aux` being `partial` (`A-NATIVE-DECIDE`). -> -> **Wave 4 status.** The same parent now also asserts the anonymous `LOG0` -> the write path actually emits. After a paid deposit, `Ξ` pushes one log -> with zero topics and 184 data bytes equal to the calldata; after a paid -> exit, one log with zero topics and 68 data bytes equal to -> `msg.sender || pubkey`. `EvmRunner` projects `Aₗ` from the successful -> `Ξ` `Substate` (topics length, data size, data bytes) — it does not -> invent a receipt. The kill-line additionally flips the user-path -> `PUSH1 RECORD_SIZE` at deposit offset 274 (`0xb8` → `0x00`), so the -> paid append still writes six words but `LOG0` data size is 0 and the -> same `submitFacts` is false. The calldatacopy size at 269, the `LOG0` -> opcode at 276, the exit user-path size at 215, and P-DRAIN-1's system -> `RETURN` size at exit 450 are left alone. -> `log_mutant_leaves_siblings_intact` proves the new mutant leaves -> `PDrain1.drainFacts` and `PControl1.controlFacts` **true**. -> -> **Wave 6 status.** The same parent now also asserts underpay and a -> second reachable-shaped storage image. A well-formed 184-byte deposit -> / 48-byte exit whose `msg.value` is strictly below the quoted fee -> (`356` vs `357` deposits, `426` vs `427` exits at image 1) reverts; -> `Ξ` returns no account map, so slots 0–3 and the live-tail queue words -> are not observable as writes. The fee getter, paid append, LOG0, -> inhibited revert, and underpay freeze are re-run at -> `excess=50 count=3 head=2 tail=6` (quotes `18` / `19`). The kill-line -> additionally flips the handle_input fee `CALLVALUE` at deposit offset -> 161 (`0x34` → `GAS` `0x5a`), so an underpaying 184-byte deposit -> succeeds and writes, and `depositUnderpayFact` / -> `altDepositUnderpayFact` fail. Wave-1 RETURN@158 and Wave-4 LOG -> size@274 are left alone on that mutant. The getter-path `CALLVALUE` -> at 148, the stake-check `CALLVALUE` at 198, and the exit fee-check -> `CALLVALUE` at 159 are left alone. -> `underpay_mutant_leaves_siblings_intact` proves the new mutant leaves -> `PDrain1.drainFacts` and `PControl1.controlFacts` **true**. -> -> **∀ / #11 / #14 status.** The registered parent is now -> `PSubmit1.psubmit1_forall_parent` (`WELL_FORMED_FORALL`): CFG-direct `∀` -> under `WellFormed` / `CallHyp`, conjoined with `psubmit1_bytecode_parent`. -> #14 made the fee-getter conjunct observe post-storage from the CFG machine -> and exported the exit LOG0 payload from `Append.exit_handle_input_append`. -> That honesty gap is closed. Still not Ξ ↔ Model (`A-ABSTRACT-TX`). - -Registered parent was `success_count_and_balance`. -It unfolds `userCall` and `simp`s `appendRecord`. The conclusion restates the -definition of the abstract interpreter. Mutants in `Eip8282/Tests/Mutants.lean` -are examples about the same interpreter (`capOf = 64`, fee-getter revert); -none is a kill-line against a bytecode parent. - -YAML claims 184-byte admission, authentic append, `sourceAddress = caller`. -Lean does not execute `pinned/bytecode/builder_deposits/main.hex`. - -## P-DRAIN-1 — DEFECTIVE (addressed; see below) - -> **Wave 1 status.** The registered parent is now -> `PDrain1.pdrain1_bytecode_parent`, which executes -> `pinned/bytecode/builder_{deposits,exits}/main.hex` under `EVM.Ξ` via -> `EvmRunner.runDepositSystem` / `runExitSystem`. The kill-line -> `Eip8282.Tests.PDrain1Mutant.mutant_refutes_parent` flips two drain-only -> bytes of the exit runtime — the `MAX_PER_BLOCK` clamp at offset 244 and -> the system `RECORD_SIZE` multiplier at offset 450 — and refutes that same -> `drainFacts`. Bar items 1, 2 and 4 are met; item 3 held for the Wave-1 -> declared scope, which was concrete traces at a handful of queue depths. -> That is no longer the registered scope: live YAML is `CFG_FORALL` -> (`pdrain1_forall_parent`) plus these traces as the kill-line. -> `A-EVM-WORLD` is the synthetic world around that `∀` + traces, not -> “finite traces only.” `native_decide` is forced by `D_J_aux` being -> `partial` (`A-NATIVE-DECIDE`). -> -> On bar item 2 specifically, -> `drain_mutants_leave_siblings_intact` proves both mutants leave -> `PSubmit1.submitFacts` and `PControl1.controlFacts` **true**: these bytes -> are invisible to the sibling guarantees (P-SUBMIT-1 never calls from -> `SYSTEM_ADDR`; P-CONTROL-1 holds an empty queue), so the P-DRAIN-1 parent -> is carrying weight nothing else in this repository carries. -> -> **Wave 2 status.** The same parent now also exercises the deposit -> per-block cap of 64 (65 queued deposits → 64 records / 11776 bytes, -> `QUEUE_HEAD = 64`, `QUEUE_TAIL = 65`) and the empty-queue deposit drain -> as a separate conjunct. The kill-line additionally flips the deposit -> `MAX_PER_BLOCK` clamp at offset 304 (`PUSH1 64` → `PUSH1 32`) and -> refutes the extended `drainFacts`. The comparison immediate at offset -> 296 is left alone, so under-cap deposit drains stay true. Sibling -> independence is re-proved for the new mutant. -> -> **Wave 3 status.** Stale-slot non-erasure is now load-bearing for more -> than deposit item 0's first word. After the 64-record deposit drain the -> parent asserts the remaining five words of item 0, the first word of -> drained item 63, and the first word of still-queued item 64. After the -> 16-record exit drain it asserts the first two words of item 0 and the -> first word of item 15 (`QUEUE_HEAD = 16`, `QUEUE_TAIL = 17`). The -> kill-line additionally flips the partial-drain `QUEUE_HEAD` SSTORE -> immediate at deposit offset 483 (`PUSH1 2` → `PUSH1 9`), so the -> advanced head value 64 is written into slot 9 (last remaining word of -> drained item 0) instead of slot 2; `staleDepositRestIs 0` fails and -> the same `drainFacts` is false. The empty-queue reset operand at offset 494 is -> left alone, so under-cap full drains stay true. Sibling independence -> is re-proved for the new mutant. -> -> **Wave 6 status.** Remaining words of other drained indices, and the -> remaining words of items 0/15/63 that Wave 3 left out, are now pinned. -> After the 64-record deposit drain the parent additionally asserts the -> five remaining words of drained item 1, the first word of drained item -> 32, and the remaining five words of drained item 63 (`QUEUE_HEAD = 64`, -> `QUEUE_TAIL = 65`). After the 16-record exit drain it additionally -> asserts the pk2 word of item 0, all three words of drained item 15, and -> all three words of drained item 7. The kill-line additionally flips -> the same deposit `QUEUE_HEAD` SSTORE at offset 483 to slot 196 -> (`PUSH1 2` → `PUSH1 196`, first word of item 32) and the exit -> `QUEUE_HEAD` SSTORE at offset 313 to slot 25 (`PUSH1 2` → `PUSH1 25`, -> src word of item 7); both make the same `drainFacts` false on the new -> conjuncts while the empty-queue reset operands at deposit 494 and exit -> 324 are left alone. Sibling independence is re-proved for both new -> mutants (`drain_mutants_leave_siblings_intact` now covers six mutants -> against `PSubmit1.submitFacts` and empty-queue `PControl1.controlFacts`). -> P-SUBMIT-1 / P-CONTROL-1 registered parents are not changed. -> -> **∀ / #13 status.** The registered parent is now -> `PDrain1.pdrain1_forall_parent` (`CFG_FORALL`): system SSTORE footprint, -> FIFO count/pointers (caps 64/16), and deposit BE→LE encode under -> `WellFormed` / `CallHyp`, conjoined with `pdrain1_bytecode_parent`. -> Stale-slot non-erasure is in that footprint `∀` (`n ≥ 4` unchanged), not -> an exclusion. Still not Ξ ↔ Model (`A-ABSTRACT-TX`). - -Registered parent was `fifo_bounded` = `systemCall s b |>.state.queue = s.queue.drop (capOf s.kind)`. -Definitional. `system_always_succeeds` is `rfl` on `.success`. No mutant -refuted a drain of the real runtime. YAML claimed SYSTEM_ADDRESS, 30M gas, -LE amount conversion; none was an `EVM.Ξ` fact. - -## P-CONTROL-1 — DEFECTIVE (addressed; see below) - -> **Wave 1 status.** The registered parent is now -> `PControl1.pcontrol1_bytecode_parent`, which executes -> `pinned/bytecode/builder_{deposits,exits}/main.hex` under `EVM.Ξ`. System -> calls reach the runtimes through `EvmRunner.runDepositSystem` / -> `runExitSystem`, which differ from the user runners only in `msg.sender`, so -> the caller gate is exercised by two runs of the same bytes rather than -> assumed. Bar items 1, 2 and 4 are met; item 3 held for the Wave-1 declared -> scope, which was concrete traces over a fixed family of storage images at -> an empty queue. That is no longer the registered scope: live YAML is -> `CFG_FORALL` (`pcontrol1_forall_parent`) plus the Wave-1/5 traces as the -> kill-line. `A-EVM-WORLD` is the synthetic world around that `∀` + traces, -> not “finite traces only.” -> -> The kill-line `Eip8282.Tests.PControl1Mutant.mutant_refutes_parent` cuts -> three single bytes — the `EQ` at offset 22 of each runtime, which compares -> `CALLER` against `SYSTEM_ADDR`, and the `TARGET_PER_BLOCK` operand at offset -> 571 of the deposit runtime, inside the `compute_excess` block only the system -> subroutine reaches — and refutes that same `controlFacts`. On bar item 2 -> specifically, `control_mutants_leave_psubmit1_intact` proves both deposit -> mutants leave `PSubmit1.submitFacts` **true**: these bytes are invisible to -> the sibling guarantee, so the P-CONTROL-1 parent is carrying weight nothing -> else in this repository carries. -> -> Still open after Wave 1 and recorded in `audit/guarantees.yaml`: the -> empty-queue parent left the drain/excess interaction unexercised, -> `fake_exponential` is pinned only relationally, and `initial_gating` is -> still abstract because the exits ctor is not executed. -> -> **Wave 5 status.** The registered parent is now -> `PControl1.pcontrol1_nonempty_bytecode_parent`. The same pinned runtimes -> run under `EVM.Ξ`, but against nonempty queue images (`QUEUE_HEAD = 0`, -> `QUEUE_TAIL ∈ {2,17,65}`) with distinctive 6-slot deposit / 3-slot exit -> records. A system call must *both* drain (`2*184=368`, `64*184=11776`, -> `2*68=136`, `16*68=1088`) *and* fold `SLOT_EXCESS` via -> `max(0, excess+count-TARGET)` (`100+5-8=97` / `100+5-2=103`) or latch -> `INHIBITOR`. A fee quote on the same image leaves `HEAD 0 TAIL 2` -> untouched. Those return sizes and pointer moves are false on an empty -> queue, so the claim is not a restatement of Wave 1. -> -> The kill-line `Eip8282.Tests.PControl1Mutant.wave5_mutant_refutes_nonempty_parent` -> feeds two system-side `TARGET_PER_BLOCK` cuts to the same -> `nonemptyControlFacts`: deposit offset 571 (`PUSH1 8` → `9`) and exit -> offset 401 (`PUSH1 2` → `3`). With the deposit cut, `depositQueue 2` -> stores excess 96 not 97; with the exit cut, `exitQueue 2` stores 102 -> not 103. The Wave-1 gate cut at offset 22 also falsifies the nonempty -> parent. `wave5_mutants_leave_psubmit1_intact` proves both new cuts -> leave `PSubmit1.submitFacts` **true**. `nonempty_is_not_empty` shows -> the under-cap nonempty fact is not the empty-queue observation -> (`368` vs `0` return bytes). -> -> **∀ / #12 status.** The registered parent is now -> `PControl1.pcontrol1_forall_parent` (`CFG_FORALL`): caller gate, excess -> recurrence (targets 8 and 2), count increment/reset, and init-bytecode -> gating under `WellFormed` / `CallHyp`, conjoined with -> `pcontrol1_bytecode_parent` and `pcontrol1_nonempty_bytecode_parent`. -> C4 closes `initial_gating` on the pinned init prefixes (CFG, not Ξ -> CREATE). Still not Ξ ↔ Model (`A-ABSTRACT-TX`). - -Registered parent was `empty_updates_excess`, which unfolds `nextExcess`. -`targets` is `rfl`. `initial_gating` is `rfl` on abstract constructors, not on -`exitInit` bytecode (`PUSH 0xff..ff; SSTORE slot 0`). YAML claimed -`fake_exponential` and reversible inhibition of the deployed contracts; Lean -never ran the hex. - -## Foundation this wave adds (not a closed guarantee) - -- Pin `bytecode/*/main.hex` and `ctor.hex` with sha256 in `audit/artifacts.lock.json`. -- `Eip8282.Audit.Bytecode` — hex literals matching those files. -- `Eip8282.Audit.EvmRunner` — `EVM.Ξ` driver. -- `lakefile.lean` requires `EVMYulLean@0ff72b2db35302305fccb1d4f42b480434b77bfe`. - -Those pins and the driver landed. The Wave-0 “next” (re-register each parent -on `EvmRunner` / `Ξ`, kill-line on bytecode not `Model.userCall`) is done -through Waves 1–6 and the CFG `∀` PRs #11–#13. Remaining campaign gap is -only `A-ABSTRACT-TX`. The `D_J_aux` half of that blocker is gone: EVMYulLean -`0ff72b2` makes it structurally recursive, so the jumpdest tables and the -`validJumps = D_J _ ⟨0⟩` bridges are `decide +kernel`. What still blocks -`A-ABSTRACT-TX` is the Ξ ↔ Model/CFG correspondence itself, not an -irreducible definition: the pinned images reach no keccak/sha2/BLAKE2 FFI -constant and no RLP decoder (see `A-NATIVE-DECIDE`), so the kept traces stay -on `native_decide` only because kernel evaluation of a full `Ξ` run is too -expensive. Do not claim F4 closed. Do not reopen the parent-strength gap -#14 closed. diff --git a/audit/guarantees.yaml b/audit/guarantees.yaml index 8194099..c39bfa0 100644 --- a/audit/guarantees.yaml +++ b/audit/guarantees.yaml @@ -6,7 +6,7 @@ { "id": "P-SUBMIT-1", "parent": "Eip8282.Audit.Guarantees.PSubmit1.psubmit1_forall_parent", - "parent_note": "The registered parent is the CFG-level ∀ theorem under WellFormed/CallHyp, conjoined with the Wave-6 psubmit1_bytecode_parent traces that the kill-line still refutes. R4 (Eip8282.Audit.XiTransport.psubmit1_xi_forall_parent) carries this same theorem as a conjunct alongside (a) XiExitTransport, an unconditional complete-Ξ exit-observation ∀ — the whole call observes exactly the halting instruction the code run exits on, that opcode is one of RETURN / REVERT / STOP / SELFDESTRUCT, RETURN and REVERT publish exactly the requested memory slice, and STOP and SELFDESTRUCT publish nothing, with the H side condition itself derived from the run (RunUntil.stop_of_rem_pos composed with H_eq_none_iff) rather than assumed, so the published bytes are a function of the machine and not a quantified ByteArray — no hypothesis beyond the run, no native_decide; (b) a model-facing observational transport that still takes ExitAgrees / A-ABSTRACT-TX as an explicit OPEN hypothesis; and (c) psubmit1_exitAgrees_iff, which reduces that hypothesis on the inhibited path to exactly the two EVM-side facts op = REVERT and bytes out = nil, with no Model reference; (d) XiWidthTransport, an unconditional complete-Ξ width ∀ — the slice a RETURN / REVERT publishes has exactly the size its own length operand names, since readWithPadding zero-pads up to the requested length (the ≤ direction unconditional, the equality under the machine-word bound μ₁ < USize.size), no hypothesis beyond the run and no native_decide; and (e) psubmit1_exitAgrees_iff_operand, which uses (d) to restate the residual of (c) as op = REVERT ∧ μ₁ = 0 — a statement about the exit instruction alone, with no ByteArray left in it. The YAML parent ID is unchanged. R4 also identifies the last two JUMPI @revert sites whose branch condition was previously opaque, deposit 190 and 204, so all ten pinned sites now branch on a word the image itself computes: amountFloorGuard_pinned / atRevertPush_of_atAmountFloorGuard build a five-instruction XRuns prefix (PUSH8 mask; AND; DUP1; PUSH4 1gwei; GT) onto site 190 carrying gt 1gwei (u64Mask &&& w), and coverGuard_pinned / atRevertPush_of_atCoverGuard build a six-instruction prefix (PUSH4 1gwei; MUL; SWAP1; CALLVALUE; SUB; LT) onto site 204 carrying lt (Iv - req) (1gwei * amt); amountFloor_taken_iff and cover_taken_iff turn each word into its arithmetic predicate, so 190 is exactly the one-gwei floor on the masked uint64 amount and 204 is exactly the check that the value left after the fee covers the deposit total. Both prefixes are kernel-checked over the pinned literals and add no native_decide axiom. Site 190 now also has an observational consequence rather than only a description: psubmit1_xi_rejected_reverts_of_reaches_amountFloorGuard concludes observe c.result = reverted with empty return data from arrival at the amount-floor guard, deriving inadmissibility on the model side from the same sub-gwei amount the pinned GT branched on, via admissible_eq_false_of_depositAmount_lt and depositWellFormed_eq_false_of_amount_lt — the model's floor amount * gwei >= builderMinDepositWei is amount * 10^9 >= 10^18, i.e. exactly the PUSH4 1gwei immediate, so this is arithmetic over the model's own constants and not a correspondence. Alone among the rejected branches it therefore carries no hreq and assumes nothing about fake_exponential; the model kind is read off the Represents witness (Represents.kind_eq) rather than assumed. Site 204 has a conditional observational consequence rather than none: psubmit1_xi_rejected_reverts_of_reaches_coverGuard concludes observe c.result = reverted with empty return data from arrival at the cover guard, with admissible_eq_false_of_cover_short turning the short remainder back into admissible = false through requiredWei, hpaid (that the fee does not exceed the value sent, so the SUB does not underflow) remaining an explicit hypothesis of psubmit1_xi_rejected_reverts_of_reaches_coverGuard rather than being discharged from the fee guard's surviving branch, and the MUL overflow side condition derived from the image's own 64-bit AND (toNat_land_u64Mask_lt, toNat_depositWei) rather than hypothesised. Unlike site 190 it does retain hpaid and hfee, the latter being that the word it subtracts is the model's currentFee — the fake_exponential correspondence — along with hamt and arrival at the guard. Arriving at either guard from c.entry is still assumed: no XRuns from c.entry to any guard exists end-to-end, and for site 190 the masked word is still assumed to be the model's depositAmount, since the CALLDATALOAD of bytes 80-87 is not run. So this identifies what the sites test and, for both 190 and 204, what taking it does — not that they are reached. EndpointAgrees is NOT discharged and A-ABSTRACT-TX stays OPEN at HIGH. R5 adds a kernel-checked reachability conjunct: ReachableStorage images satisfy WellFormed and Model.Reachable, and append preserves the guard and queue controls. That packed-storage proof never runs Ξ and does not discharge ExitAgrees. The abstract-model theorem below is supporting evidence, not a substitute: per audit/WAVE0.md, abstract CHECKED does not stand in for bytecode CHECKED. This parent is not Ξ ↔ Model.", + "parent_note": "The registered parent is the CFG-level ∀ theorem under WellFormed/CallHyp, conjoined with the Wave-6 psubmit1_bytecode_parent traces that the kill-line still refutes. R4 (Eip8282.Audit.XiTransport.psubmit1_xi_forall_parent) carries this same theorem as a conjunct alongside (a) XiExitTransport, an unconditional complete-Ξ exit-observation ∀ — the whole call observes exactly the halting instruction the code run exits on, that opcode is one of RETURN / REVERT / STOP / SELFDESTRUCT, RETURN and REVERT publish exactly the requested memory slice, and STOP and SELFDESTRUCT publish nothing, with the H side condition itself derived from the run (RunUntil.stop_of_rem_pos composed with H_eq_none_iff) rather than assumed, so the published bytes are a function of the machine and not a quantified ByteArray — no hypothesis beyond the run, no native_decide; (b) a model-facing observational transport that still takes ExitAgrees / A-ABSTRACT-TX as an explicit OPEN hypothesis; and (c) psubmit1_exitAgrees_iff, which reduces that hypothesis on the inhibited path to exactly the two EVM-side facts op = REVERT and bytes out = nil, with no Model reference; (d) XiWidthTransport, an unconditional complete-Ξ width ∀ — the slice a RETURN / REVERT publishes has exactly the size its own length operand names, since readWithPadding zero-pads up to the requested length (the ≤ direction unconditional, the equality under the machine-word bound μ₁ < USize.size), no hypothesis beyond the run and no native_decide; and (e) psubmit1_exitAgrees_iff_operand, which uses (d) to restate the residual of (c) as op = REVERT ∧ μ₁ = 0 — a statement about the exit instruction alone, with no ByteArray left in it. The YAML parent ID is unchanged. R4 also identifies the last two JUMPI @revert sites whose branch condition was previously opaque, deposit 190 and 204, so all ten pinned sites now branch on a word the image itself computes: amountFloorGuard_pinned / atRevertPush_of_atAmountFloorGuard build a five-instruction XRuns prefix (PUSH8 mask; AND; DUP1; PUSH4 1gwei; GT) onto site 190 carrying gt 1gwei (u64Mask &&& w), and coverGuard_pinned / atRevertPush_of_atCoverGuard build a six-instruction prefix (PUSH4 1gwei; MUL; SWAP1; CALLVALUE; SUB; LT) onto site 204 carrying lt (Iv - req) (1gwei * amt); amountFloor_taken_iff and cover_taken_iff turn each word into its arithmetic predicate, so 190 is exactly the one-gwei floor on the masked uint64 amount and 204 is exactly the check that the value left after the fee covers the deposit total. Both prefixes are kernel-checked over the pinned literals and add no native_decide axiom. Site 190 now also has an observational consequence rather than only a description: psubmit1_xi_rejected_reverts_of_reaches_amountFloorGuard concludes observe c.result = reverted with empty return data from arrival at the amount-floor guard, deriving inadmissibility on the model side from the same sub-gwei amount the pinned GT branched on, via admissible_eq_false_of_depositAmount_lt and depositWellFormed_eq_false_of_amount_lt — the model's floor amount * gwei >= builderMinDepositWei is amount * 10^9 >= 10^18, i.e. exactly the PUSH4 1gwei immediate, so this is arithmetic over the model's own constants and not a correspondence. Alone among the rejected branches it therefore carries no hreq and assumes nothing about fake_exponential; the model kind is read off the Represents witness (Represents.kind_eq) rather than assumed. Site 204 has a conditional observational consequence rather than none: psubmit1_xi_rejected_reverts_of_reaches_coverGuard concludes observe c.result = reverted with empty return data from arrival at the cover guard, with admissible_eq_false_of_cover_short turning the short remainder back into admissible = false through requiredWei, hpaid (that the fee does not exceed the value sent, so the SUB does not underflow) remaining an explicit hypothesis of psubmit1_xi_rejected_reverts_of_reaches_coverGuard rather than being discharged from the fee guard's surviving branch, and the MUL overflow side condition derived from the image's own 64-bit AND (toNat_land_u64Mask_lt, toNat_depositWei) rather than hypothesised. Unlike site 190 it does retain hpaid and hfee, the latter being that the word it subtracts is the model's currentFee — the fake_exponential correspondence — along with hamt and arrival at the guard. Arriving at either guard from c.entry is still assumed: no XRuns from c.entry to any guard exists end-to-end, and for site 190 the masked word is still assumed to be the model's depositAmount, since the CALLDATALOAD of bytes 80-87 is not run. So this identifies what the sites test and, for both 190 and 204, what taking it does — not that they are reached. EndpointAgrees is NOT discharged and A-ABSTRACT-TX stays OPEN at HIGH. R5 adds a kernel-checked reachability conjunct: ReachableStorage images satisfy WellFormed and Model.Reachable, and append preserves the guard and queue controls. That packed-storage proof never runs Ξ and does not discharge ExitAgrees. The abstract-model theorem below is supporting evidence, not a substitute: abstract CHECKED does not stand in for bytecode CHECKED. This parent is not Ξ ↔ Model.", "assumptions": [ "A-ABSTRACT-TX", "A-REACHABLE", @@ -76,7 +76,7 @@ { "id": "P-DRAIN-1", "parent": "Eip8282.Audit.Guarantees.PDrain1.pdrain1_forall_parent", - "parent_note": "The registered parent is the CFG-level ∀ theorem under WellFormed/CallHyp (system path isUser = false, gas ≥ 30M), conjoined with the Wave-6 pdrain1_bytecode_parent traces that the kill-line still refutes. R4 (Eip8282.Audit.XiTransport.pdrain1_xi_forall_parent) carries this same theorem as a conjunct alongside (a) XiExitTransport, an unconditional complete-Ξ exit-observation ∀ — the whole call observes exactly the halting instruction the code run exits on, that opcode is one of RETURN / REVERT / STOP / SELFDESTRUCT, RETURN and REVERT publish exactly the requested memory slice, and STOP and SELFDESTRUCT publish nothing, with the H side condition itself derived from the run (RunUntil.stop_of_rem_pos composed with H_eq_none_iff) rather than assumed, so the published bytes are a function of the machine and not a quantified ByteArray — no hypothesis beyond the run, no native_decide; (b) a model-facing observational transport that still takes ExitAgrees / A-ABSTRACT-TX as an explicit OPEN hypothesis; and (c) pdrain1_xi_exit_publishes, which refutes the two silent-halt exit branches whenever the bounded FIFO window is non-empty, so the residual only has to be checked on RETURN / REVERT; (d) XiWidthTransport, an unconditional complete-Ξ width ∀ — the slice a RETURN / REVERT publishes has exactly the size its own length operand names, since readWithPadding zero-pads up to the requested length (the ≤ direction unconditional, the equality under the machine-word bound μ₁ < USize.size), no hypothesis beyond the run and no native_decide; and (e) pdrain1_xi_exit_length_ge / pdrain1_xi_exit_length_eq, which use (d) to pin the exit's length operand to the width of the drained FIFO window concatReturned (queue.take (capOf kind)). The YAML parent ID is unchanged. The abstract-model theorem below is supporting evidence, not a substitute: per audit/WAVE0.md, abstract CHECKED does not stand in for bytecode CHECKED. This parent is not Ξ ↔ Model and does not claim Ξ computes FIFO for every excess. R4 additionally carries (f) the gap-drain layer for the 68-byte exit window: GapStores admits an arbitrary memory-neutral gap before every store, supplying only that store's offset and value, which is the shape builder_exits' accum_loop has, and StoresCovered / covered_exitStores derive the SpacedStores frontier conditions from the 68-byte stride, so endpointAgrees_of_gapExitDrain_return and exitAgrees_of_gapExitDrain_return state EndpointAgrees / ExitAgrees in conclusion position for a drain whose run is built rather than assumed, with no pre-staged operand stack and with pre.memory.size <= 32 in place of the empty-frame hypothesis; gapStores_exitStores_of_stack embeds the flat pre-staged run with every gap empty, so nothing proved from the earlier statements is lost. That does not discharge A-ABSTRACT-TX: reachability of the store loop in the pinned runtime is still assumed. R4 additionally carries (g) the same gap-drain layer for the 184-byte deposit window: GapMixedStores admits an arbitrary memory-neutral gap before every store, word or byte, supplying only that store's offset and value, and computes each store's post-state as mstorePost / mstore8Post, so the relation carries none of the per-store frame conditions SpacedMixedStores asks for - off <= size <= off + 32 on each MSTORE and off < size on each %MSTORE64_le MSTORE8, seven assertions per record about the size of memory between two stores of builder_deposits' own loop. SplicesCovered with splicesCovered_byteRun_append, splicesCovered_depositRecord and covered_depositStores derive that frontier arithmetically at the offsets main.eas gives the seven stores - +0, +32, +64 walk the frame out to b + 96, the eight amount bytes at +80 .. +87 land strictly inside it, +96, +128, +160 walk it out to b + 192, and the next record's base b + 184 is within one word of that - so endpointAgrees_of_gapDepositDrain_return and exitAgrees_of_gapDepositDrain_return state EndpointAgrees / ExitAgrees in conclusion position for the deposit window asking only pre.memory.size <= 32 about memory for the whole drain; MixedStores.gap embeds the adjacency-shaped relation with every gap empty, so mixedStores_depositPrefix still inhabits it with real MSTORE / MSTORE8 opcodes and nothing proved from MixedStores is lost. Both drain layouts are now at that shape. That does not discharge A-ABSTRACT-TX either: reachability of the store loop in the pinned runtime is still assumed.", + "parent_note": "The registered parent is the CFG-level ∀ theorem under WellFormed/CallHyp (system path isUser = false, gas ≥ 30M), conjoined with the Wave-6 pdrain1_bytecode_parent traces that the kill-line still refutes. R4 (Eip8282.Audit.XiTransport.pdrain1_xi_forall_parent) carries this same theorem as a conjunct alongside (a) XiExitTransport, an unconditional complete-Ξ exit-observation ∀ — the whole call observes exactly the halting instruction the code run exits on, that opcode is one of RETURN / REVERT / STOP / SELFDESTRUCT, RETURN and REVERT publish exactly the requested memory slice, and STOP and SELFDESTRUCT publish nothing, with the H side condition itself derived from the run (RunUntil.stop_of_rem_pos composed with H_eq_none_iff) rather than assumed, so the published bytes are a function of the machine and not a quantified ByteArray — no hypothesis beyond the run, no native_decide; (b) a model-facing observational transport that still takes ExitAgrees / A-ABSTRACT-TX as an explicit OPEN hypothesis; and (c) pdrain1_xi_exit_publishes, which refutes the two silent-halt exit branches whenever the bounded FIFO window is non-empty, so the residual only has to be checked on RETURN / REVERT; (d) XiWidthTransport, an unconditional complete-Ξ width ∀ — the slice a RETURN / REVERT publishes has exactly the size its own length operand names, since readWithPadding zero-pads up to the requested length (the ≤ direction unconditional, the equality under the machine-word bound μ₁ < USize.size), no hypothesis beyond the run and no native_decide; and (e) pdrain1_xi_exit_length_ge / pdrain1_xi_exit_length_eq, which use (d) to pin the exit's length operand to the width of the drained FIFO window concatReturned (queue.take (capOf kind)). The YAML parent ID is unchanged. The abstract-model theorem below is supporting evidence, not a substitute: abstract CHECKED does not stand in for bytecode CHECKED. This parent is not Ξ ↔ Model and does not claim Ξ computes FIFO for every excess. R4 additionally carries (f) the gap-drain layer for the 68-byte exit window: GapStores admits an arbitrary memory-neutral gap before every store, supplying only that store's offset and value, which is the shape builder_exits' accum_loop has, and StoresCovered / covered_exitStores derive the SpacedStores frontier conditions from the 68-byte stride, so endpointAgrees_of_gapExitDrain_return and exitAgrees_of_gapExitDrain_return state EndpointAgrees / ExitAgrees in conclusion position for a drain whose run is built rather than assumed, with no pre-staged operand stack and with pre.memory.size <= 32 in place of the empty-frame hypothesis; gapStores_exitStores_of_stack embeds the flat pre-staged run with every gap empty, so nothing proved from the earlier statements is lost. That does not discharge A-ABSTRACT-TX: reachability of the store loop in the pinned runtime is still assumed. R4 additionally carries (g) the same gap-drain layer for the 184-byte deposit window: GapMixedStores admits an arbitrary memory-neutral gap before every store, word or byte, supplying only that store's offset and value, and computes each store's post-state as mstorePost / mstore8Post, so the relation carries none of the per-store frame conditions SpacedMixedStores asks for - off <= size <= off + 32 on each MSTORE and off < size on each %MSTORE64_le MSTORE8, seven assertions per record about the size of memory between two stores of builder_deposits' own loop. SplicesCovered with splicesCovered_byteRun_append, splicesCovered_depositRecord and covered_depositStores derive that frontier arithmetically at the offsets main.eas gives the seven stores - +0, +32, +64 walk the frame out to b + 96, the eight amount bytes at +80 .. +87 land strictly inside it, +96, +128, +160 walk it out to b + 192, and the next record's base b + 184 is within one word of that - so endpointAgrees_of_gapDepositDrain_return and exitAgrees_of_gapDepositDrain_return state EndpointAgrees / ExitAgrees in conclusion position for the deposit window asking only pre.memory.size <= 32 about memory for the whole drain; MixedStores.gap embeds the adjacency-shaped relation with every gap empty, so mixedStores_depositPrefix still inhabits it with real MSTORE / MSTORE8 opcodes and nothing proved from MixedStores is lost. Both drain layouts are now at that shape. That does not discharge A-ABSTRACT-TX either: reachability of the store loop in the pinned runtime is still assumed.", "assumptions": [ "A-ABSTRACT-TX", "A-REACHABLE", @@ -144,7 +144,7 @@ { "id": "P-CONTROL-1", "parent": "Eip8282.Audit.Guarantees.PControl1.pcontrol1_forall_parent", - "parent_note": "The registered parent is the CFG-level ∀ theorem under WellFormed/CallHyp (gas ≥ 30M, caller class), conjoined with the Wave-1 pcontrol1_bytecode_parent, Wave-5 pcontrol1_nonempty_bytecode_parent, and fold-discrimination traces that the kill-line still refutes. The fold-discrimination conjunct (pcontrol1_fold_discriminate_parent) asserts that the user-path bump_excess fold (excess + max(0, count−TARGET)) and the system-path update_excess fold (max(0, excess+count−TARGET)) produce different values on both runtimes. R4 (Eip8282.Audit.XiTransport.pcontrol1_xi_forall_parent) carries this same theorem as a conjunct alongside (a) XiExitTransport, an unconditional complete-Ξ exit-observation ∀ — the whole call observes exactly the halting instruction the code run exits on, that opcode is one of RETURN / REVERT / STOP / SELFDESTRUCT, RETURN and REVERT publish exactly the requested memory slice, and STOP and SELFDESTRUCT publish nothing, with the H side condition itself derived from the run (RunUntil.stop_of_rem_pos composed with H_eq_none_iff) rather than assumed, so the published bytes are a function of the machine and not a quantified ByteArray — no hypothesis beyond the run, no native_decide; (b) a model-facing observational transport that still takes ExitAgrees / A-ABSTRACT-TX as an explicit OPEN hypothesis; and (c) pcontrol1_xi_exit_is_RETURN, which pins the exit opcode of the fee quote to RETURN, since a 32-byte big-endian fee can come from neither a silent halt nor a revert; (d) XiWidthTransport, an unconditional complete-Ξ width ∀ — the slice a RETURN / REVERT publishes has exactly the size its own length operand names, since readWithPadding zero-pads up to the requested length (the ≤ direction unconditional, the equality under the machine-word bound μ₁ < USize.size), no hypothesis beyond the run and no native_decide; and (e) pcontrol1_xi_exit_length_ge_32 / pcontrol1_xi_exit_length_eq_32, which use (d) to sharpen the fee quote's length operand from non-zero to exactly 32. The YAML parent ID is unchanged. The abstract-model theorem below is supporting evidence, not a substitute: per audit/WAVE0.md, abstract CHECKED does not stand in for bytecode CHECKED. This parent is not Ξ ↔ Model. C4 now also carries a code-deposit conjunct: Eip8282.Audit.Guarantees.PControl1.CtorXi.pcontrol1_ctor_xi_parent runs the full pinned ctor.hex images under EvmYul.EVM.Xi and pins the buffer each returns to be the pinned main.hex byte for byte, which is the code Lambda step (115) installs. It is not Lambda itself: the predeploys are genesis-installed, so Lambda's KEC(RLP(sender,nonce)) address is not the predeploy address and no address derivation or Reachable claim is made.", + "parent_note": "The registered parent is the CFG-level ∀ theorem under WellFormed/CallHyp (gas ≥ 30M, caller class), conjoined with the Wave-1 pcontrol1_bytecode_parent, Wave-5 pcontrol1_nonempty_bytecode_parent, and fold-discrimination traces that the kill-line still refutes. The fold-discrimination conjunct (pcontrol1_fold_discriminate_parent) asserts that the user-path bump_excess fold (excess + max(0, count−TARGET)) and the system-path update_excess fold (max(0, excess+count−TARGET)) produce different values on both runtimes. R4 (Eip8282.Audit.XiTransport.pcontrol1_xi_forall_parent) carries this same theorem as a conjunct alongside (a) XiExitTransport, an unconditional complete-Ξ exit-observation ∀ — the whole call observes exactly the halting instruction the code run exits on, that opcode is one of RETURN / REVERT / STOP / SELFDESTRUCT, RETURN and REVERT publish exactly the requested memory slice, and STOP and SELFDESTRUCT publish nothing, with the H side condition itself derived from the run (RunUntil.stop_of_rem_pos composed with H_eq_none_iff) rather than assumed, so the published bytes are a function of the machine and not a quantified ByteArray — no hypothesis beyond the run, no native_decide; (b) a model-facing observational transport that still takes ExitAgrees / A-ABSTRACT-TX as an explicit OPEN hypothesis; and (c) pcontrol1_xi_exit_is_RETURN, which pins the exit opcode of the fee quote to RETURN, since a 32-byte big-endian fee can come from neither a silent halt nor a revert; (d) XiWidthTransport, an unconditional complete-Ξ width ∀ — the slice a RETURN / REVERT publishes has exactly the size its own length operand names, since readWithPadding zero-pads up to the requested length (the ≤ direction unconditional, the equality under the machine-word bound μ₁ < USize.size), no hypothesis beyond the run and no native_decide; and (e) pcontrol1_xi_exit_length_ge_32 / pcontrol1_xi_exit_length_eq_32, which use (d) to sharpen the fee quote's length operand from non-zero to exactly 32. The YAML parent ID is unchanged. The abstract-model theorem below is supporting evidence, not a substitute: abstract CHECKED does not stand in for bytecode CHECKED. This parent is not Ξ ↔ Model. C4 now also carries a code-deposit conjunct: Eip8282.Audit.Guarantees.PControl1.CtorXi.pcontrol1_ctor_xi_parent runs the full pinned ctor.hex images under EvmYul.EVM.Xi and pins the buffer each returns to be the pinned main.hex byte for byte, which is the code Lambda step (115) installs. It is not Lambda itself: the predeploys are genesis-installed, so Lambda's KEC(RLP(sender,nonce)) address is not the predeploy address and no address derivation or Reachable claim is made.", "assumptions": [ "A-ABSTRACT-TX", "A-REACHABLE",