engine_api.qnt

// Engine API specification in Quint
//
// Models the CL/EL interaction protocol from the CL's perspective.
// Reference: https://github.com/ethereum/execution-apis/tree/main/src/engine
//
// To run:
//   quint run engine_api.qnt
//   quint test engine_api.qnt

module engine_api {
  // ==========================================================================
  // TYPES
  // ==========================================================================

  // Block hashes are the primary identifiers
  type BlockHash = str

  // Payload IDs are tickets to retrieve built blocks
  type PayloadId = str

  // Possible responses from EL to forkchoice/newPayload calls
  type PayloadStatus =
    | Valid
    | Invalid
    | Syncing
    | Accepted  // for newPayload only

  // ==========================================================================
  // STATE
  // ==========================================================================

  // CL's view of the canonical chain head
  var cl_head: BlockHash

  // EL's set of validated block hashes (the "validated payloads pool")
  var el_validated: Set[BlockHash]

  // EL's current canonical head
  var el_head: BlockHash

  // Payloads currently being built: payload_id -> parent_hash
  var el_building: PayloadId -> BlockHash

  // Built payloads ready for retrieval: payload_id -> block_hash
  var el_built: PayloadId -> BlockHash

  // Last response from EL (for property checking)
  var last_response: PayloadStatus

  // ==========================================================================
  // CONSTANTS
  // ==========================================================================

  pure val GENESIS: BlockHash = "genesis"
  pure val BLOCK1: BlockHash = "block1"
  pure val BLOCK2: BlockHash = "block2"
  pure val BLOCK3: BlockHash = "block3"
  pure val PID1: PayloadId = "pid1"
  pure val PID2: PayloadId = "pid2"

  // ==========================================================================
  // INITIALIZATION
  // ==========================================================================

  action init = all {
    cl_head' = GENESIS,
    el_head' = GENESIS,
    el_validated' = Set(GENESIS),
    el_building' = Map(),
    el_built' = Map(),
    last_response' = Valid,
  }

  // ==========================================================================
  // ACTIONS
  // ==========================================================================

  /// ForkchoiceUpdated without payload attributes
  ///
  /// CL tells EL: "make this block the canonical head"
  ///
  /// Maps to Inner::set_latest_forkchoice_state
  ///
  /// The EL will:
  /// - Retrieve the pre-validated block from its pool
  /// - Promote the stored state to canonical state
  /// - Update the canonical chain head pointer
  action forkchoiceUpdated_setHead(block_hash: BlockHash): bool = all {
    el_validated.contains(block_hash),  // precondition: block must be validated by EL
    cl_head' = block_hash,              // CL updates its view of head
    el_head' = block_hash,              // EL updates canonical head
    last_response' = Valid,             // response is VALID
    el_validated' = el_validated,       // no changes to pools
    el_building' = el_building,
    el_built' = el_built,
  }

  /// ForkchoiceUpdated with unknown block hash
  ///
  /// EL returns SYNCING when it doesn't know the block.
  /// Maps to Inner::set_latest_forkchoice_state (SYNCING branch)
  action forkchoiceUpdated_unknown(block_hash: BlockHash): bool = all {
    not(el_validated.contains(block_hash)),  // precondition: block is NOT in validated set
    last_response' = Syncing,                // EL responds SYNCING
    cl_head' = cl_head,                      // no state changes
    el_head' = el_head,
    el_validated' = el_validated,
    el_building' = el_building,
    el_built' = el_built,
  }

  /// ForkchoiceUpdated with payload attributes
  ///
  /// CL tells EL: "build me a new block on top of this parent"
  ///
  /// Maps to Inner::generate_block
  ///
  /// The EL will:
  /// - Set working state to parent_hash
  /// - Start collecting transactions from mempool
  /// - Return a payload_id (ticket to retrieve the built block)
  action forkchoiceUpdated_buildBlock(parent_hash: BlockHash, payload_id: PayloadId): bool = all {
    el_validated.contains(parent_hash),            // precondition: parent must be validated
    not(el_building.keys().contains(payload_id)),  // precondition: payload_id must not be in use
    not(el_built.keys().contains(payload_id)),
    el_building' = el_building.put(payload_id, parent_hash),  // EL starts building
    el_head' = parent_hash,                        // head updates to parent (per Engine API spec)
    cl_head' = parent_hash,
    last_response' = Valid,                        // response is VALID with payload_id
    el_validated' = el_validated,                  // no change to other state
    el_built' = el_built,
  }

  /// EL finishes building a block (internal EL action)
  ///
  /// This models the async nature - block building takes time.
  /// Once complete, the block moves from building to built pool.
  action el_finishBuilding(payload_id: PayloadId, new_block_hash: BlockHash): bool = all {
    el_building.keys().contains(payload_id),      // precondition: must be currently building this payload
    not(el_validated.contains(new_block_hash)),   // precondition: new block hash must be fresh
    el_built' = el_built.put(payload_id, new_block_hash),       // move from building to built
    el_building' = el_building.keys().exclude(Set(payload_id)).mapBy(k => el_building.get(k)),
    el_validated' = el_validated.union(Set(new_block_hash)),    // block is implicitly validated since EL built it
    cl_head' = cl_head,                                         // no change to heads or response
    el_head' = el_head,
    last_response' = last_response,
  }

  /// GetPayload
  ///
  /// CL retrieves a built block by payload_id.
  ///
  /// Maps to EngineAPI::get_payload
  ///
  /// This is a read-only operation - CL gets the ExecutionPayloadV3.
  action getPayload(payload_id: PayloadId): bool = all {
    el_built.keys().contains(payload_id),  // precondition: block must be built
    cl_head' = cl_head,                    // read-only: no state changes
    el_head' = el_head,
    el_validated' = el_validated,
    el_building' = el_building,
    el_built' = el_built,
    last_response' = last_response,
  }

  /// NewPayload - valid block
  ///
  /// CL sends a block to EL for validation.
  ///
  /// Maps to Inner::notify_new_block
  ///
  /// The EL will:
  /// - Set working state to parent_hash
  /// - Execute transactions from the payload
  /// - Compute state and verify against payload's state_root
  /// - Store in "validated payloads pool" indexed by block_hash
  action newPayload_valid(block_hash: BlockHash, parent_hash: BlockHash): bool = all {
    el_validated.contains(parent_hash),            // precondition: parent must be validated (can't validate orphan)
    not(el_validated.contains(block_hash)),        // precondition: block was not already validated
    el_validated' = el_validated.union(Set(block_hash)),  // block becomes validated
    last_response' = Valid,
    cl_head' = cl_head,                            // no change to heads or building state
    el_head' = el_head,
    el_building' = el_building,
    el_built' = el_built,
  }

  /// NewPayload - invalid block
  ///
  /// Block fails validation (bad state root, invalid transactions, etc.)
  action newPayload_invalid(block_hash: BlockHash): bool = all {
    last_response' = Invalid,        // block is NOT added to validated set
    cl_head' = cl_head,              // no state changes
    el_head' = el_head,
    el_validated' = el_validated,
    el_building' = el_building,
    el_built' = el_built,
  }

  // ==========================================================================
  // STATE MACHINE
  // ==========================================================================

  /// All possible block hashes we model (keep small for tractability)
  pure val ALL_BLOCKS: Set[BlockHash] = Set(GENESIS, BLOCK1, BLOCK2, BLOCK3)

  /// All possible payload IDs
  pure val ALL_PAYLOAD_IDS: Set[PayloadId] = Set(PID1, PID2)

  /// Non-deterministic step: any action can happen
  action step = any {
    nondet block_hash = ALL_BLOCKS.oneOf()
    forkchoiceUpdated_setHead(block_hash),

    nondet block_hash = ALL_BLOCKS.oneOf()
    forkchoiceUpdated_unknown(block_hash),

    nondet parent = ALL_BLOCKS.oneOf()
    nondet pid = ALL_PAYLOAD_IDS.oneOf()
    forkchoiceUpdated_buildBlock(parent, pid),

    nondet pid = ALL_PAYLOAD_IDS.oneOf()
    nondet new_hash = ALL_BLOCKS.oneOf()
    el_finishBuilding(pid, new_hash),

    nondet pid = ALL_PAYLOAD_IDS.oneOf()
    getPayload(pid),

    nondet block_hash = ALL_BLOCKS.oneOf()
    nondet parent = ALL_BLOCKS.oneOf()
    newPayload_valid(block_hash, parent),

    nondet block_hash = ALL_BLOCKS.oneOf()
    newPayload_invalid(block_hash),
  }

  // ==========================================================================
  // SAFETY PROPERTIES (invariants)
  // ==========================================================================

  /// EL's canonical head is always a validated block.
  ///
  /// If this fails, EL could report an invalid block as canonical.
  val headIsValidated: bool =
    el_validated.contains(el_head)

  /// After a VALID response, CL and EL agree on head.
  val headsConsistent: bool =
    last_response == Valid implies cl_head == el_head

  /// Genesis is always in the validated set.
  ///
  /// We should never "un-validate" our starting point.
  val genesisAlwaysValid: bool =
    el_validated.contains(GENESIS)

  /// Built blocks are always validated.
  ///
  /// If EL built it, it must be in the validated pool.
  val builtBlocksAreValidated: bool =
    el_built.keys().forall(pid =>
      el_validated.contains(el_built.get(pid))
    )

  /// Combined safety invariant
  val safety: bool = and {
    headIsValidated,
    headsConsistent,
    genesisAlwaysValid,
    builtBlocksAreValidated,
  }

  // ==========================================================================
  // TESTS
  // ==========================================================================

  /// Test: basic forkchoice flow
  run basicForkchoiceTest = {
    init
      .then(newPayload_valid(BLOCK1, GENESIS))
      .then(forkchoiceUpdated_setHead(BLOCK1))
      .then(all {
        assert(cl_head == BLOCK1),
        assert(el_head == BLOCK1),
        assert(last_response == Valid),
        cl_head' = cl_head,
        el_head' = el_head,
        el_validated' = el_validated,
        el_building' = el_building,
        el_built' = el_built,
        last_response' = last_response,
      })
  }

  /// Test: block building flow
  run blockBuildingTest = {
    init
      .then(forkchoiceUpdated_buildBlock(GENESIS, PID1))
      .then(el_finishBuilding(PID1, BLOCK1))
      .then(getPayload(PID1))
      .then(all {
        assert(el_built.get(PID1) == BLOCK1),
        assert(el_validated.contains(BLOCK1)),
        cl_head' = cl_head,
        el_head' = el_head,
        el_validated' = el_validated,
        el_building' = el_building,
        el_built' = el_built,
        last_response' = last_response,
      })
  }

  /// Test: unknown block returns SYNCING
  run unknownBlockTest = {
    init
      .then(forkchoiceUpdated_unknown(BLOCK1))  // BLOCK1 not yet validated
      .then(all {
        assert(last_response == Syncing),
        assert(cl_head == GENESIS),  // head unchanged
        cl_head' = cl_head,
        el_head' = el_head,
        el_validated' = el_validated,
        el_building' = el_building,
        el_built' = el_built,
        last_response' = last_response,
      })
  }
}