An executable Lean 4 model of FOCIL (EIP-7805), following the
heze fork of consensus-specs,
with machine-checked proofs about that model.
The spec functions are written as plain Lean definitions, so they can be run on concrete inputs and proven about at the same time.
| Module | Spec |
|---|---|
Focil/Store.lean |
InclusionListStore, process_inclusion_list |
Focil/Aggregate.lean |
get_inclusion_list_transactions, get_inclusion_list_bits, is_inclusion_list_bits_inclusive |
Focil/Committee.lean |
get_inclusion_list_committee |
Focil/Satisfaction.lean |
execution engine is_inclusion_list_satisfied |
Focil/Account.lean |
nonce and balance ledger used to instantiate the above |
Focil/ForkChoice.lean |
record_payload_inclusion_list_satisfaction, should_extend_payload |
focil_censorship_resistance: if fork choice extends a payload, that payload contains every transaction listed by any honest, timely committee member, unless the transaction no longer fits in the block or is invalid against the payload's post-state.mem_getInclusionListTransactions: a single non-equivocating, timely member is enough to put a transaction into the inclusion list constraints (1-of-N honesty).lookup_process_of_some,equivocator_of_conflict,equivocator_process: the first list from a validator is never replaced, a conflicting list marks it as an equivocator, and that mark is permanent.mem_of_mem_getInclusionListCommittee,length_getInclusionListCommittee: committee seats are always filled from the slot's beacon committees.applyFields_front_run: a same-sender, same-nonce transaction makes the listed one invalid, which is exactly the case the satisfaction check is allowed to excuse.
Validity is checked against the post-state of the whole payload, as the execution engine does, so dependencies between transactions are part of the model rather than assumed away.
Everything depends only on Lean's standard axioms (propext, Classical.choice, Quot.sound).
BLS signatures, SSZ encoding, gossip validation, the retention window, and the rest of the
ePBS fork choice (should_extend_payload takes those clauses as a single boolean).
lake build
lake test