Skip to content

engine-api

Directory actions

More options

Directory actions

More options

Latest commit

 

History

History

engine-api

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
README.md
README.md
 
 
engine_api.qnt
engine_api.qnt
 
 

README.md

Engine API Specification

Models the Ethereum Engine API protocol - the CL/EL interaction from the CL's perspective.

Protocol Overview

CL (consensus layer)              EL (execution layer)
     |                                |
     |-- forkchoiceUpdated ---------> |  "make this block canonical"
     | <-------- VALID/INVALID/SYNC --|
     |                                |
     |-- forkchoiceUpdated + attrs -> |  "build me a block"
     | <-------- VALID + payload_id --|
     |-- getPayload ----------------> |
     | <-------- ExecutionPayloadV3 --|
     |                                |
     |-- newPayload ----------------> |  "validate this block"
     | <-------- VALID/INVALID ------|

Running

make test   SPEC=engine-api  # run tests
make run    SPEC=engine-api  # random simulation
make verify SPEC=engine-api # check safety properties
make help   SPEC=engine-api # see all commands

State Variables

Variable Type Description
cl_head BlockHash CL's view of canonical head
el_head BlockHash EL's canonical head
el_validated Set[BlockHash] EL's validated payloads pool
el_building PayloadId -> BlockHash Blocks being built (parent hash)
el_built PayloadId -> BlockHash Built blocks ready for retrieval
last_response PayloadStatus Last EL response

Actions

forkchoiceUpdated_setHead(block_hash)

CL tells EL to make a block canonical.

Precondition: Block must be in el_validated

Effect: Both cl_head and el_head update to block_hash

forkchoiceUpdated_unknown(block_hash)

CL references a block EL doesn't know.

Precondition: Block NOT in el_validated

Effect: Returns Syncing, no state change

forkchoiceUpdated_buildBlock(parent_hash, payload_id)

CL asks EL to build a new block.

Precondition: Parent validated, payload_id not in use

Effect: EL starts building, returns payload_id

el_finishBuilding(payload_id, new_block_hash)

Internal EL action - block construction completes.

Effect: Block moves from el_building to el_built, added to el_validated

getPayload(payload_id)

CL retrieves built block.

Precondition: Block must be in el_built

Effect: Read-only

newPayload_valid(block_hash, parent_hash)

CL sends block for validation, EL accepts.

Precondition: Parent validated

Effect: Block added to el_validated

newPayload_invalid(block_hash)

CL sends block for validation, EL rejects.

Effect: Returns Invalid, no state change

Safety Properties

headIsValidated

EL's canonical head is always a validated block.

el_validated.contains(el_head)

Why it matters: If violated, EL could report an invalid block as canonical.

headsConsistent

After a successful call, CL and EL agree on head.

last_response == Valid implies cl_head == el_head

Why it matters: CL and EL must have consistent views to avoid forks.

genesisAlwaysValid

Genesis never leaves the validated set.

el_validated.contains(GENESIS)

Why it matters: Genesis is our trust anchor.

builtBlocksAreValidated

EL-built blocks are always in the validated pool.

el_built.keys().forall(pid => el_validated.contains(el_built.get(pid)))

Why it matters: EL trusts its own work.

Modeling Decisions

Why Sets, Not Chains?

The spec models el_validated as a Set[BlockHash], not an ordered chain. We're modeling what the EL knows about (which blocks have been validated), not the chain structure itself.

If we needed to model reorgs, fork choice, or block heights, we'd add structure:

var parent: BlockHash -> BlockHash  // parent pointers

Future Extensions

  1. Reorgs - Model CL switching to a different fork
  2. SYNCING resolution - Model EL catching up
  3. Multiple validators - Concurrent block proposals
  4. Timeouts - What happens when EL doesn't respond
  5. ACCEPTED status - For optimistic sync scenarios

References