Blocks¶
A block is a header and a body; the body's size and hash are fields of the block rather than functions of it. Leios (CIP-164) extends a ranking block in two places (Ranking Blocks): the header may announce an endorser block (EB) and flags whether the body certifies the EB announced by the previous block, and the body may carry that certificate.
An announcement is the pair a header may carry: the announced EB's identifier and its declared byte size.
Announcement : Type Announcement = EBHash × ℕ
A wrong declared size invalidates nothing (the CIP has honest nodes decline to vote instead), so size agreement belongs to the voters' checks, not to block validity.
record BHBody : Type where field bvkcold : VKey bsize : ℕ slot : Slot bhash : KeyHash hBbsize : ℕ announcedEB : Maybe Announcement certifiesEB : Bool record BHeader : Type where field bhbody : BHBody bhsig : Sig
A certifying body carries the certificate and nothing else of Leios (Ranking Blocks): the EB it certifies and that EB's closure, its referenced transactions resolved and in reference order, are not part of the block. The chain-level rules receive them beside the block, resolved by consensus, and check them against the certificate; the block itself says only that it certifies.
record Block : Type where field bheader : BHeader bHeaderHash : RBHeaderHash ts : List TopLevelTx ebCert : Maybe EBCert bBodySize : ℕ bBodyHash : KeyHash ≡-bBodySize : bBodySize ≡ BHBody.hBbsize (BHeader.bhbody bheader) ≡-bBodyHash : bBodyHash ≡ BHBody.bhash (BHeader.bhbody bheader)
The header hash is a field for the same reason the body hash is: it is computed
from the header's bytes, which the specification does not model, so consensus
supplies it. It is the message a later certificate is verified against
(ValidEBCert in Leios).
The BBODY Transition System¶
The transition updates the ledger state and the map of blocks produced per pool,
in an environment of the enact state and the accounting state.
incrBlocks counts a certifying block like any other.
BBodyEnv : Type BBodyEnv = EnactState × Acnt BBodyState : Type BBodyState = LedgerState × BlocksMade incrBlocks : KeyHash → BlocksMade → BlocksMade incrBlocks hk b = b ∪⁺ singletonᵐ hk 1
CIP-164 fixes two rules about a block alone (Inclusion Rules;
Step 5): a header that sets certified_eb obliges its body to
carry a certificate, and a body carrying a certificate carries no transactions
of its own. ValidLeiosBlock states both as a disjoint union,
one alternative for a body without a certificate and one for a body with one,
so the bit is required in both directions and a false bit cannot hide a
certificate.
ValidLeiosBlock : Block → Type ValidLeiosBlock b = (Is-nothing ebCert × certifiesEB ≡ false) ⊎ (Is-just ebCert × certifiesEB ≡ true × length ts ≡ 0) where open Block b open BHBody (BHeader.bhbody bheader)
The bit is an input the rule checks, not a value computed from the body. Header validation sees the bit but not the body, so a check it gates on the bit is sound only if the ledger verifies the bit.
The rule requires the body's size and hash to agree with the header, the block
to satisfy ValidLeiosBlock, and LEDGERS to
accept the transactions within the block's limits on reference-script size and
execution units.
The checks that need the announcing block, which BBODY does
not see, belong to CHAIN: the certification delay, the epoch
the two blocks share, the certificate's validity against the committee pinned at
announcement (ValidEBCert), and the certified EB's validity and
application (ValidEB).
data _⊢_⇀⦇_,BBODY⦈_ : BBodyEnv → BBodyState → Block → BBodyState → Type where BBODY-Block-Body : {acnt : Acnt} {ls ls' : LedgerState} {b : BlocksMade} {block : Block} {es : EnactState} → let open BHeader open BHBody open Block open EnactState txs = block .ts bhb = block .bheader .bhbody hk = hash (bhb .bvkcold) pp = PParamsOf es Γ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.BlockBody.html#5440}{\htmlId{5537}{\htmlClass{Bound}{\text{bhb}}}}\, \,\htmlId{5541}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.BlockBody.html#1792}{\htmlId{5542}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Prelude.html#2367}{\htmlId{5549}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.BlockBody.html#5303}{\htmlId{5551}{\htmlClass{Bound}{\text{es}}}}\, \,\htmlId{5554}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.html#926}{\htmlId{5555}{\htmlClass{Field}{\text{constitution}}}}\, \,\href{Ledger.Prelude.html#2367}{\htmlId{5568}{\htmlClass{Function Operator}{\text{∣}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.BlockBody.html#5506}{\htmlId{5572}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.BlockBody.html#5303}{\htmlId{5577}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Prelude.Base.html#1263}{\htmlId{5582}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Dijkstra.Specification.BlockBody.html#5205}{\htmlId{5593}{\htmlClass{Bound}{\text{acnt}}}}\, \end{pmatrix}$ Γw = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.BlockBody.html#5530}{\htmlId{5613}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#3945}{\htmlId{5617}{\htmlClass{Field}{\text{PParams.maxRefScriptSizePerBlock}}}}\, \,\href{Ledger.Dijkstra.Specification.BlockBody.html#5506}{\htmlId{5650}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#2820}{\htmlId{5655}{\htmlClass{Field}{\text{PParams.maxBlockExUnits}}}}\, \,\href{Ledger.Dijkstra.Specification.BlockBody.html#5506}{\htmlId{5679}{\htmlClass{Bound}{\text{pp}}}}\, \end{pmatrix}$ in ∙ block .bBodySize ≡ bhb .hBbsize ∙ block .bBodyHash ≡ bhb .bhash ∙ ValidLeiosBlock block ∙ Γw ⊢ ls ⇀⦇ txs ,LEDGERS⦈ ls' ──────────────────────────────── (es , acnt) ⊢ ls , b ⇀⦇ block ,BBODY⦈ (ls' , incrBlocks hk b)