Blockchain Layer¶
The chain layer applies one block at a time. A block without a certificate ticks the new-epoch state to its slot and runs its body on the ticked state. A block whose body certifies the endorser block (EB) announced by its predecessor first applies that EB's closure to the ledger state the predecessor left, in the predecessor's environment, and only then ticks and runs its own body (Step 5; Ledger Management).
Definition of ChainState¶
Beside the NewEpochState, the ChainState records the last applied
block: its slot, the hash of its header, and the EB its header announced, if any.
Every block replaces this record, so an announcement survives exactly one block
and only the immediate successor can certify it (Step 5).
(The consensus specification's record of the same name carries the block
number, the slot, and the header hash.)
record LastAppliedBlock : Type where field slot : Slot headerHash : RBHeaderHash announcedEB : Maybe Announcement record ChainState : Type where field newEpochState : NewEpochState lastApplied : Maybe LastAppliedBlock
Resolved endorser blocks¶
The block carries its certificate alone. The EB it certifies and that EB's closure, its referenced transactions resolved and in reference order, are not chain objects: the node resolves them, and the chain rule reads them from its environment. The rules take the closure as an input.
record ResolvedEB : Type where field eb : EndorserBlock closure : List TopLevelTx record ChainEnv : Type where field resolvedEB : Maybe ResolvedEB pendingEB : LastAppliedBlock → Maybe EBHash pendingEB la = proj₁ <$> LastAppliedBlock.announcedEB la announcingEnv : ChainState → LastAppliedBlock → LedgerEnv announcingEnv cs la = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Chain.html#2621}{\htmlId{4847}{\htmlClass{Field}{\text{LastAppliedBlock.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Chain.html#4838}{\htmlId{4869}{\htmlClass{Bound}{\text{la}}}}\, \\ \,\href{Ledger.Prelude.html#2367}{\htmlId{4874}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Enact.html#926}{\htmlId{4876}{\htmlClass{Function}{\text{constitution}}}}\, \,\href{Ledger.Prelude.html#2367}{\htmlId{4889}{\htmlClass{Function Operator}{\text{∣}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#8103}{\htmlId{4893}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Chain.html#4835}{\htmlId{4903}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Chain.html#4959}{\htmlId{4908}{\htmlClass{Function}{\text{es}}}}\, \\ \,\href{Ledger.Prelude.Base.html#1263}{\htmlId{4913}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\htmlId{4924}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Epoch.html#5386}{\htmlId{4925}{\htmlClass{Field}{\text{NewEpochStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Chain.html#4835}{\htmlId{4941}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{4943}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ where es = EnactStateOf cs open EnactState es using (constitution)
ChainEnv carries the resolved EB, if the node has one for the
pending announcement; a block that certifies nothing ignores it.
pendingEB reads the announced hash; the declared size beside
it is no validity condition (see BlockBody).
announcingEnv uses the announcing slot and the enact state,
parameters, and treasury before the tick.
The CHAIN Transition System¶
CHAIN-None handles a block without a certificate.
It ticks and runs BBODY, whatever the environment resolves.
CHAIN-EB takes the resolved EB from the
environment, checks the certificate in the chain context, applies the EB at
the announcing slot, and then ticks and runs the body. Certificate checking
is read-only; the EB premise produces the ledger state the
tick continues from.
The contextual checks require the previous block to have announced the EB,
the certification delay to have elapsed, the two blocks to share an epoch,
and ValidEBCert to hold for the announcing header's hash and
that epoch's committee and threshold (Step 5;
Certificate Validation). The same-epoch premise also rules
out certification across an era boundary, since era transitions occur at
epoch boundaries. It costs at most one EB per boundary.
The EB premise states full declarative validity and
application (see Leios.Validity). A certifying block carries
no transactions of its own, by ValidLeiosBlock.
data _⊢_⇀⦇_,CHAIN⦈_ : ChainEnv → ChainState → Block → ChainState → Type where CHAIN-None : ∀ {bcur'} {Γ : ChainEnv} {b : Block} {nes : NewEpochState} {cs : ChainState}
let cs' = record cs { newEpochState = record nes { bcur = bcur'; epochState = record (EpochStateOf nes) {ls = ls'} } ; lastApplied = just $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.BlockBody.html#1792}{\htmlId{7274}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.BlockBody.html#2467}{\htmlId{7281}{\htmlClass{Function}{\text{bHeaderHash}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.BlockBody.html#1864}{\htmlId{7295}{\htmlClass{Function}{\text{announcedEB}}}}\, \end{pmatrix}$ } in ∙ ebCert ≡ nothing ∙ tt ⊢ newEpochState ⇀⦇ slot ,TICK⦈ nes ∙ (es , acnt) ⊢ (ls , bcur) ⇀⦇ b ,BBODY⦈ (ls' , bcur') ──────────────────────────────── Γ ⊢ cs ⇀⦇ b ,CHAIN⦈ cs' CHAIN-EB : ∀ {bcur'} {Γ : ChainEnv} {b : Block} {reb : ResolvedEB} {cert : EBCert} {la : LastAppliedBlock} {nes : NewEpochState} {cs : ChainState} {ls₁ : LedgerState}
let pp = PParamsOf cs cmt = NewEpochState.leiosCommittee newEpochState nes₁ = record newEpochState { epochState = record (EpochStateOf cs) {ls = ls₁} } cs' = record cs { newEpochState = record nes { bcur = bcur'; epochState = record (EpochStateOf nes) {ls = ls'} } ; lastApplied = just $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.BlockBody.html#1792}{\htmlId{8420}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.BlockBody.html#2467}{\htmlId{8427}{\htmlClass{Function}{\text{bHeaderHash}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.BlockBody.html#1864}{\htmlId{8441}{\htmlClass{Function}{\text{announcedEB}}}}\, \end{pmatrix}$ } in ∙ ebCert ≡ just cert ∙ resolvedEB ≡ just reb ∙ lastApplied ≡ just la ∙ pendingEB la ≡ just (hashEB eb) ∙ announcingSlot + certificationDelay pp ≤ slot ∙ epoch announcingSlot ≡ epoch slot ∙ ValidEBCert cmt (PParams.leiosQuorumStakeThreshold pp) (rbHeaderHashBytes headerHash) cert ∙ (announcingEnv cs la , closure) ⊢ LedgerStateOf cs ⇀⦇ eb ,EB⦈ ls₁ ∙ tt ⊢ nes₁ ⇀⦇ slot ,TICK⦈ nes ∙ (es , acnt) ⊢ (ls , bcur) ⇀⦇ b ,BBODY⦈ (ls' , bcur') ──────────────────────────────── Γ ⊢ cs ⇀⦇ b ,CHAIN⦈ cs'
A certificate whose environment resolves no EB admits no transition; a resolved
EB that no certificate claims is ignored. Every successful block replaces
lastApplied, retiring the previous announcement and recording its
own announcement, if any, for its successor.