docs: retarget EIP pin from PR 12057 to b759aae8 / #12120 - #2
Conversation
sys-asm@83f9801 is unchanged. The working EIP text is now lfglabs-dev/EIPs@b759aae8 (INHIBITOR, constructor split, stacked ethereum/EIPs#12120). Point at eip-8282-proof-closure@85dab78e for concrete-trace Lean; F1–F7 remain proposed, not proved here.
![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: 508bea411b
ℹ️ 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".
| **EIP REQUIREMENT.** The updated fee section says that only the exit contract starts inhibited. It says that deposits can queue before the fork. The Deployment section still says that each init code sets the inhibitor. | ||
|
|
||
| **OPEN SPECIFICATION DIFFERENCE.** The updated fee section agrees with the code. The Deployment section and the `EXCESS_INHIBITOR` constant comment do not agree with the code or with the updated fee section. Presigned transaction bytes are absent, so the stated addresses cannot be derived. | ||
| **OPEN SPECIFICATION DIFFERENCE (partially closed in the working text).** The working EIP at `lfglabs-dev/EIPs@b759aae8` (PR [ethereum/EIPs#12120](https://github.com/ethereum/EIPs/pull/12120)) names the latch `INHIBITOR` and documents the constructor split: only the exit ctor writes it. Presigned transaction bytes are still absent, so the stated addresses cannot be derived from these ctor bytes. The older PR 12057 pin (`EXCESS_INHIBITOR`, both-ctors inhibit) is superseded. |
There was a problem hiding this comment.
This new paragraph says the working EIP documents the constructor split and that the conflicting PR 12057 wording is superseded, but the adjacent EIP REQUIREMENT still says the Deployment section requires both constructors to inhibit, and the F1 status remains blocked by that alleged conflict. Readers using the retargeted proof plan therefore receive mutually exclusive requirements and an obsolete blocker; update the requirement and status to reflect the new pin.
Useful? React with 👍 / 👎.
| - Queue and system calls: Queue | ||
| - Fee / activation / `fake_exponential`: Fee | ||
| - Deposits / exits: Deposits, Exits | ||
| - Upgrade (SYSTEM inhibit old, keep draining): Rationale, Contract upgrade |
There was a problem hiding this comment.
The new source summary identifies “SYSTEM inhibit old, keep draining” as part of the working EIP's Contract upgrade text, while eip-8282-flow-map.md F6 and diagram/README.md still say the EIP does not define this post-deployment disable operation and classify it as requiring a specification decision. Under the new pin this leaves a normative upgrade flow mislabeled as an implementation-only extension, so update those dependent classifications when introducing this reference.
Useful? React with 👍 / 👎.
| All EIP links use PR 12057 head commit `ab06dfac0bf3531ac267efb011ae8864c3eb70ab`. | ||
| Working text: `lfglabs-dev/EIPs` commit used by proof-closure | ||
| (`b759aae8`, PR [ethereum/EIPs#12120](https://github.com/ethereum/EIPs/pull/12120)). | ||
| Line numbers below are for that file, not PR 12057. |
There was a problem hiding this comment.
This sentence promises line numbers, but every replacement entry below it contains only a section name and no line range or immutable blob link. Consequently SOURCES.md and diagram/README.md continue to advertise exact EIP line references that no longer exist, making the retargeted normative claims substantially harder to audit against the pinned commit; provide commit-pinned links and actual ranges as before.
Useful? React with 👍 / 👎.
| The artifacts are copied byte-for-byte from \`ethereum/sys-asm@83f9801245ff56878a450b5625801101b9a225a1\`. The source declares geas \`0.3.3\` and build command \`make build\`, expanding to \`bin/geas-0.3.3 -a -no-nl -o bytecode/... src/...\`. Reproduction was attempted. It stopped before compilation because \`go\` is not installed, so a fresh geas binary could not be built. Checked-in SHA-256 checksums do match pinned \`checksums.txt\`. | ||
|
|
||
| The EIP pin is PR 12057 head \`ab06dfac0bf3531ac267efb011ae8864c3eb70ab\` (immutable PR base \`78525144ee85c57f50e5e6675ca3561d3101caeb\`, distinct from mutable current \`master\`); semantics pin \`601183cb2d959748243d59093c144652a6f10716\`; consensus pin \`53a9d0ce366f665eb682102f67d9f722fb260506\`. Runtime target fork in both \`.eas\` files is Prague. | ||
| The working EIP pin is \`lfglabs-dev/EIPs@b759aae809235802e23df47adeea50a1e6a7befb\` (PR ethereum/EIPs#12120). The previous map pin was PR 12057 \`ab06dfac\` — superseded. Consensus pin remains \`53a9d0ce366f665eb682102f67d9f722fb260506\`. Executed EVM semantics for Lean traces is EVMYulLean \`f7e4ee0\`. Runtime target fork in both \`.eas\` files is Prague. |
There was a problem hiding this comment.
After dependencies are available, running scripts/generate-manifest.mjs will rewrite the committed manifest's updated pin paragraph: this template emits only EVMYulLean f7e4ee0 and omits the #11869/base and planning-only semantics details that were added to verity/targets/eip-8282-artifact-manifest.md:7. The generator therefore no longer reproduces its checked-in artifact and silently drops immutable provenance; make its template match the committed manifest.
Useful? React with 👍 / 👎.
1 participant
Why
This map still advertised
ethereum/EIPsPR 12057 (ab06dfac,EXCESS_INHIBITOR, “no Lean theorem is claimed proved”). The code pinsys-asm@83f9801is still correct. The EIP text and Lean surface moved:lfglabs-dev/EIPs@b759aae809235802e23df47adeea50a1e6a7befb(ethereum/EIPs#12120)INHIBITOR(2^256-1); only the exit ctor writes iteip-8282-proof-closure85dab78eunderEvmYul.EVM.ΞWhat this PR does
Updates README, SOURCES, diagram README/caption, flow-map/proof-plan/manifest pins, and
generate-manifest.mjs.Not in this PR: regenerating SVG/PNG or rewriting every
data-source=\"PR12057\"edge. The diagram artwork is still dated 2026-08-04; the caption now says so. F1–F7 relational theorems stay proposed.Out of scope
diagram/exports/*∀/Reptheorems in this repo