docs: EF-shareable EIP-8282 proof snapshot - #20
Open
Th0rgal wants to merge 13 commits into
Open
Conversation
…guidance
The receipt claimed in guarantees.yaml ("the four D_J jumpdest tables and
their validJumps bridges") stopped after the two runtime bridges. Add
#print axioms for depositInit_validJumps_eq_D_J, exitInit_validJumps_eq_D_J
and the parent-facing validJumps_are_Xi_tables so the printed output matches
the claim, and list them in the A-NATIVE-DECIDE validation text.
The campaign Method section still told workers D_J_aux was `partial` and to
reach for native_decide on the F1 tables, a constraint EVMYulLean 0ff72b2
removed. Restate it as structurally recursive / decide +kernel in CAMPAIGN.md
and CLOUD_ORCHESTRATOR.md.
No new IDs, no proof or gate changes.
The A-NATIVE-DECIDE justification named EvmYul.FFI.keccak256 / sha256 / BLAKE2Compress and the partial RLP decoders as what forces native_decide on the kept Xi traces. Neither is reachable on this path. Disassembling the four pinned images (depositRuntime 628, depositInit 638, exitRuntime 458, exitInit 503 bytes) finds no SHA3, no BLOCKHASH, no call/create opcode and therefore no precompile dispatch, so the evaluator branches that mention those opaque @[extern] constants are never entered; importing them does not put them into kernel reduction. EvmRunner.run builds a world and applies EVM.Xi to it directly, so no transaction RLP is decoded and separateListRLP / deserializeRLP are never called. What actually blocks decide +kernel is the cost of evaluating the trace: up to FUEL = 80000 interpreter steps (300000 for the deposit-cap traces) over EVMYulLean's monad-transformer stack, AccountMap / TreeSet lookups and UInt256 / ByteArray operations. Restate the assumption, its removal_path and the repeated copies of the same claim in Trust.lean, the three bytecode parent docstrings, WAVE0.md and README.md as a cost limitation. The FFI dynlib build step stays, because native_decide links the whole interpreter. Documentation only: no proof, tactic, gate or #print change. audit-check ok.
The Wave-5 nonempty-queue docstring still deferred to "the same FFI reason as the Wave-1 parent" after Wave 1 in this file was corrected to state the cost reason. Spell the cost reason out here too: the pinned images reach neither the opaque @[extern] FFI constants nor the partial RLP decoders, so the blocker is kernel evaluation of the interpreter steps, not irreducibility. Docstring only; no proof, assumption YAML or bytecode change.
C4's ctor lemmas are a no-jump init preamble and step against no jumpdest table, so validJumps_are_Xi_tables cannot transport into or constrain pcontrol1_c4_ctor_forall; its two init-image equalities are independent facts carried alongside. P-DRAIN carries the same over-claim and has no ctor fragment at all.
…t half C4 previously stopped at a CFG prefix: Ctor.lean's opcode facts are `rfl` on the first `++` chunk of each init hex -- 32 of 638 bytes for deposit, 64 of 503 for exit -- and never execute the image. Three things were therefore unchecked: that the init image reaches its RETURN, that the buffer it returns is the pinned runtime byte for byte rather than merely a copy starting at a plausible offset, and that the exit ctor's SSTORE actually lands. PControl1/CtorXi.lean executes the full pinned init images under EvmYul.EVM.Xi and compares the returned buffer -- the value Lambda's step (115) installs as the new account's code -- against the pinned runtime images. `pcontrol1_ctor_xi_parent` is added as a conjunct of `pcontrol1_c4_ctor_forall`, so the registered parent `pcontrol1_forall_parent` is strictly stronger. No new parent ID. This is deliberately not Lambda itself. Lambda derives its address as KEC(RLP(sender, nonce)); the EIP-8282 contracts are genesis predeploys, not CREATE outputs, so driving Lambda would pin an address that is provably not the predeploy address and would pull the opaque @[extern] keccak FFI into the trusted base for no gain. Kill-line, on the init images rather than the runtimes: deposit ctor byte 5 CODECOPY source 0x0a -> 0x0b (shifts the deployed copy one byte) and exit ctor byte 34 SSTORE 0x55 -> POP 0x50 (leaves the exit contract un-inhibited at genesis). `ctor_mutants_leave_runtime_guarantees_intact` shows both cuts leave controlFacts and submitFacts true on the pinned runtimes, so the new conjunct is load-bearing on bytes nothing else in this repository constrained. A-PINNED-SOURCE stays OPEN. This links ctor.hex to main.hex inside the pin; it observes nothing on chain. The residual open part -- the deployed-address / deployed-codehash observation -- is recorded verbatim in audit/assumptions.yaml along with the now-single-step removal path. P-SUBMIT-1 and P-DRAIN-1 registered parents are unchanged.
Remove agent and campaign machinery. Keep the current Node 3 and Node 4 claims, limits, trust boundary, pins, proofs, tests, and audit metadata.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2c11cc9428
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| - `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 | ||
| **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. |
There was a problem hiding this comment.
The parenthetical misstates the storage invariant presented to readers: WellFormed.lean defines slots 0–3 as SLOT_EXCESS, SLOT_COUNT, QUEUE_HEAD, and QUEUE_TAIL, while packed records begin at QUEUE_OFFSET = 4; its actual predicate constrains HEAD ≤ TAIL, the tail bound, and item-base non-wrapping. For an EF-facing proof summary, saying “slots 0-3 packed” gives the wrong storage layout and overstates what well-formedness validates, so this should identify those slots as control words and describe the packed record window separately.
Useful? React with 👍 / 👎.
Th0rgal
changed the base branch from
feat/node4-create-pinned-source-356667ce
to
main
August 28, 2026 10:48
Retarget the EF-shareable snapshot onto main (R5 #25, Node 3 #18) instead of the Node 4 feature branch. Resolutions: - Lean/build pins take main's truth: EVMYulLean d164b61b in lakefile.lean, lake-manifest.json, audit/artifacts.lock.json. - Import and Trust.lean #print axioms conflicts are additive; both main's XiTransport/Reachable blocks and the branch's Node 4 CtorXi block are kept, since both modules are present in the merged tree. - audit/guarantees.yaml keeps main's R4/R5 parent_note, summary and coverage text and re-applies the Node 4 CtorXi conjunct, whose modules the merged tree still contains. - Internal campaign docs (audit/CAMPAIGN.md, audit/WAVE0.md, audit/CLOUD_ORCHESTRATOR.md, AGENTS.md, .cursor/) stay deleted per the EF-shareable intent of this branch; dangling "per audit/WAVE0.md" references are dropped from the YAML.
Record the Ξ-transport and reachability layers that landed on main (R5 #25, Node 3 #18) and state the campaign heads as they actually stand on GitHub: R1 #21, R2 #22, R3 #23, R4 #24 and Node 4 #19 are open drafts, not merged. Both HIGH assumptions stay open and are named as such: A-ABSTRACT-TX is not discharged (R4 transports only under the explicit EndpointAgrees hypothesis, R5 is packed-storage only), and A-PINNED-SOURCE is not discharged (Node 4 closes the ctor-to-runtime half within the pin; no chain state is observed).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Share-only review artifact for the Ethereum Foundation. Not intended to merge.
Stacked on the live Node 4 branch (#19), so future Node 4 commits remain underneath this PR automatically.
Validation:
python3 scripts/audit_metadata.py→audit-check ok.