All Core Devs - Execution (ACDE) #210, April 24

[nconsigny]

All Core Devs - Execution (ACDE)

• April 24, 2025, 14:00-15:30 UTC
• Stream
• Ethereum Protocol Calls Calendar subscription

Agenda

• Pectra
  • Mainnet announcement
• Fusaka
  • BPO EIP-7892 config format
  • EOF
    • Status updates
    • Moving to Option D
    • RISC-V concerns
  • SFI'ing gas limit defaults change
  • RLP Execution Block Limit
• History Expiry updates
  • Meta EIP
    • Sepolia activation
  • Data endpoints

🤖 config

• Duration in minutes : 90
• Recurring meeting : true
• Call series : ACDE
• Occurrence rate : bi-weekly
• Already a Zoom meeting ID : false #
• Already on Ethereum Calendar : false #
• Need YouTube stream links : true #
• Facilitator email: [email protected]
  Note: The zoom link will be sent to the facilitator via email

[github-actions]

Discourse Topic ID: 23502

• Action: Updated at 2025-04-24 13:42 UTC
• URL: https://ethereum-magicians.org/t/23502

Zoom Meeting: Reusing meeting 88269836469 for series 'acde'.

• Zoom link hidden (sent to facilitator email)

YouTube Stream Links:

• Stream 1 (Apr 24, 2025): https://youtube.com/watch?v=7BKH9C2afNc

Calendar Event Updated

• Google Calendar
• Zoom details unchanged, skipping email notification.

Telegram Notification

• Sent message for this occurrence to Ethereum Protocol Updates channel

[ralexstokes]

we should agree to the EIP-7892 config format EL teams want for the blob parameter config

[Sophia-Gold]

Let's discuss SFIing a gas limit increase in Fusaka: ethereum/EIPs#9678

[benaadams]

Can we discuss RLP Execution Block Size Limit (potentially for Fusaka, as security fix) as without it there is a safe hard blocklimit cap at 100Mgas ethereum/EIPs#9658 and we don't control validators raising gaslimits

---

Post-pectra (with EIP-7623) the max size block is around 104Mgas

All-zero calldata ⇒ 10 gas/byte ⇒ 104 857 600 gas for 10 MiB

Minus other block overheads; so calldata is currently the limit on safe block gaslimit (without capping block bytes). Above that and CLs won't propagate the blocks

---

However, rather than try to mitigate this in a different way easiest it to cap the EL blocksize; was why enable blocks >10MB that are full of zeros, as they won't be doing any useful work (or they wouldn't be full of zeros)

Should be a 1 line check; if block data > (10MB - 512kb) invalid block

[lightclient]

I find the proposal from Vitalik to replace the EVM with RISC-V concerning. We have not even shipped EOF and there are already proposals to replace it.

Clients, compilers, debuggers, FV / static analysis tools, etc should not need to integrate these changes if they will likely become obsolete within a few years. The engineering effort to add EOF to those projects will be substantial. Even if there is a future transition that is backwards compatible, people aren't going to pay an order of magnitude or more to use EVM when they can cheaply use RISC-V.

[benaadams]

For EOF I'd like to pitch changing for option D; where we bring back the gas and introspection opcodes; as the dev experience isn't ready for them to be banned (compiling Uniswap, OpenZep and Solady is problematic)

Can always bring back the ban as an EOF v2 (as EOF allows versioning); and in that the removal will have to be argued on its own merits. However the dev experience isn't ready for it, today.

[gakonst]

+1000 on Ben’s point above

[PetarMax]

Hello everyone - over the past three years I have been working first at Runtime Verification and now at Nethermind on formal verification of EVM bytecode. I have just read some previous discussions (most notably the one in this thread), and would like to offer my perspective, noting that I have only briefly looked at the EOF proposal. From my experience, these are the most important challenges for formal verification of EVM bytecode resulting from Solidity compilation:

1. Trustworthy model of the EVM semantics. This can be done, Nethermind has it, Runtime Verification has it, without simplifications of any kind. Also, I believe that it is ok in the context of formal verification, and not just bug-finding, to have simplifying assumptions as long as they are clearly stated and “reasonable”. For example, Kontrol (RV) has a mode in which stack overflow/underflow checks are disabled, which speeds up execution and assumes that the Solidity compiler never outputs code with such an error. Another such assumption would be to have infinite gas, because symbolic gas computation yields complex formulae that are difficult to reason about, and then gas analysis could be done separately.

2. Brittleness of compiled EVM code. It is possible that the EVM bytecode coming from the same Solidity code changes in unexpected ways between versions of the compiler. This makes reasoning about loop invariants, which is essential for unbounded verification, unmaintainable at the EVM bytecode level. For example, as part of an engagement with RV, I had to write and (automatically) prove an invariant for a simple loop in the Optimism codebase. I am an expert user and this took me almost a week, and on top of that the proof would break in unexpected and difficult-to-debug ways almost every time a change to the codebase was made. This is part of the reason why the Nethermind Clear tool targets Yul and not EVM. I am not sure how EOF would mitigate this issue, as it is intra-code-section is nature. I don't think the relative and static jumps help, because the issue does not come from not being able to identify the loops start and end points. Moreover, I do not believe that having relative jumps only would prevent the Solidity compiler from creating spaghetti EVM bytecode within a code section?

3. Inlining of internal functions. Currently, the execution of calls to internal functions in not performed via a CALL opcode, but their code is instead inlined into the body of the caller at the call site. This, together with point 2, makes compositional reasoning (that is, reasoning about them in isolation) impossible.

4. Reasoning using abstractions in the presence of linear rather than structured memory and storage. Unbounded verification of any algorithm that traverses or manipulates data structures in storage (for example, linked lists, arrays, or Merkle trees) is likely to involve abstractions of said data structures (for example, abstracting the linked list into the a mathematical list of node contents). The organisation of EVM storage makes the writing of these abstractions very difficult and efficient manipulation of these abstractions using EVM bytecode requires imposing additional structure on the storage along the lines of a block-offset memory model of C and also reasoning about properties of keccak using not necessarily sound axiomatisations. I was not able to make this work in Kontrol, for example, despite having extensive expertise on doing exactly the same for JavaScript, C, and Rust.

If the bytecode does not come from compilation of Solidity code, then further challenges arise, but 2-4 above are quite enough to severely impede scalable formal verification in principle. If EOF does not address any of them, then it is not clear to me how much benefit it would bring to real-world formal verification.

[timbeiko]

Closed in favor of #1500