From e778b6e866f6898afadc90dec9f45e47adcfdea9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 8 Sep 2026 22:16:27 +0000 Subject: [PATCH 1/9] Add announced endorser block to block header --- .../agda-spec/src/Spec/BlockDefinitions.lagda | 52 +++++++++++++------ .../Foreign/HSConsensus/BlockDefinitions.agda | 5 ++ .../HSConsensus/ExternalStructures.agda | 1 + docs/agda-spec/src/Spec/hs-src/Lib.hs | 2 +- .../src/Spec/hs-src/test/ChainHeadSpec.hs | 29 +++++++---- .../hs-src/test/OperationalCertificateSpec.hs | 29 +++++++---- .../src/Spec/hs-src/test/ProtocolSpec.hs | 29 +++++++---- 7 files changed, 98 insertions(+), 49 deletions(-) diff --git a/docs/agda-spec/src/Spec/BlockDefinitions.lagda b/docs/agda-spec/src/Spec/BlockDefinitions.lagda index a238de9ae8..fed62f5691 100644 --- a/docs/agda-spec/src/Spec/BlockDefinitions.lagda +++ b/docs/agda-spec/src/Spec/BlockDefinitions.lagda @@ -28,20 +28,30 @@ record BlockStructure : Type₁ where HashHeader : Type -- hash of a block header HashBBody : Type -- hash of a block body VRFRes : Type -- VRF result value + HashEB : Type -- hash of endorser block \end{code} \begin{code}[hide] ⦃ DecEq-HashHeader ⦄ : DecEq HashHeader ⦃ DecEq-HashBBody ⦄ : DecEq HashBBody ⦃ DecEq-VRFRes ⦄ : DecEq VRFRes + ⦃ DecEq-HashEB ⦄ : DecEq HashEB ⦃ Show-HashHeader ⦄ : Show HashHeader ⦃ Show-HashBBody ⦄ : Show HashBBody ⦃ Show-VRFRes ⦄ : Show VRFRes + ⦃ Show-HashEB ⦄ : Show HashEB \end{code} \emph{Concrete types} \begin{code} BlockNo = ℕ -- block number Certifiedℕ = ∃[ n ] n < 2 ^ 512 -- [0, 2^512) (64-byte VRF output) \end{code} +\emph{Announced Endorser Block} +\begin{code} + record AnnouncedEB : Type where + field + hash : HashEB + size : ℕ +\end{code} \emph{Operational Certificate} \begin{AgdaSuppressSpace} \begin{code} @@ -58,6 +68,13 @@ record BlockStructure : Type₁ where σ : Sigˢ -- cold key signature \end{code} \end{AgdaSuppressSpace} +\end{AgdaAlign} +\caption{Block definitions} +\label{fig:defs:blocks} +\end{figure*} + +\begin{figure*}[h] +\begin{AgdaAlign} \emph{Block Header Body} \begin{AgdaSuppressSpace} \begin{code} @@ -67,17 +84,18 @@ record BlockStructure : Type₁ where field \end{code} \begin{code} - prevHeader : Maybe HashHeader -- hash of previous block header - issuerVk : VKeyˢ -- block issuer - vrfVk : VKeyᵛ -- VRF verification key - blockNo : BlockNo -- block number - slot : Slot -- block slot - vrfRes : VRFRes -- VRF result value - vrfPrf : Proof -- VRF proof - bodySize : ℕ -- size of the block body - bodyHash : HashBBody -- block body hash - oc : OCert -- operational certificate - pv : ProtVer -- protocol version + prevHeader : Maybe HashHeader -- hash of previous block header + issuerVk : VKeyˢ -- block issuer + vrfVk : VKeyᵛ -- VRF verification key + blockNo : BlockNo -- block number + slot : Slot -- block slot + vrfRes : VRFRes -- VRF result value + vrfPrf : Proof -- VRF proof + bodySize : ℕ -- size of the block body + bodyHash : HashBBody -- block body hash + oc : OCert -- operational certificate + pv : ProtVer -- protocol version + announcedEB : Maybe AnnouncedEB -- announced endorser block \end{code} \end{AgdaSuppressSpace} \emph{Block Types} @@ -101,6 +119,11 @@ record BlockStructure : Type₁ where serHashToℕ : SerHash → Certifiedℕ serHashToNonce : SerHash → Nonce \end{code} +\end{AgdaAlign} +\caption{Block header definitions} +\label{fig:defs:block-header} +\end{figure*} + \begin{code}[hide] open BlockStructure open import Tactic.Derive.Show @@ -111,6 +134,9 @@ instance Show-Certifiedℕ : ∀ {bs} → Show (Certifiedℕ bs) Show-Certifiedℕ .show = show ∘ proj₁ + unquoteDecl Show-AnnouncedEB = derive-Show + [(quote AnnouncedEB , Show-AnnouncedEB)] + unquoteDecl Show-OCert = derive-Show [(quote OCert , Show-OCert)] @@ -120,7 +146,3 @@ instance unquoteDecl Show-BHeader = derive-Show [(quote BHeader , Show-BHeader)] \end{code} -\end{AgdaAlign} -\caption{Block definitions} -\label{fig:defs:blocks} -\end{figure*} diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/BlockDefinitions.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/BlockDefinitions.agda index a7b3885fa9..2ff98c3d51 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/BlockDefinitions.agda +++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/BlockDefinitions.agda @@ -10,6 +10,11 @@ instance Conv-Certifiedℕ = λ where .to → proj₁; .from → (λ n → if n <ℕ 2 ^ 512 then (λ{n<2^512} → from n , n<2^512) else 0 , s≤s z≤n) where open import Data.Nat renaming (_<_ to _<ℕ_) + HsTy-AnnouncedEB = autoHsType AnnouncedEB ⊣ withConstructor "MkAnnouncedEB" + • fieldPrefix "aeb" + + Conv-AnnouncedEB = autoConvert AnnouncedEB + HsTy-OCert = autoHsType OCert ⊣ withConstructor "MkOCert" • fieldPrefix "oc" diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda index cf56807788..71d86816b4 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda +++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda @@ -93,6 +93,7 @@ instance { HashHeader = ℕ ; HashBBody = ℕ ; VRFRes = ℕ + ; HashEB = ℕ ; DecEq-HashHeader = DecEq-ℕ } diff --git a/docs/agda-spec/src/Spec/hs-src/Lib.hs b/docs/agda-spec/src/Spec/hs-src/Lib.hs index 73282dc8da..5d946255e8 100644 --- a/docs/agda-spec/src/Spec/hs-src/Lib.hs +++ b/docs/agda-spec/src/Spec/hs-src/Lib.hs @@ -10,7 +10,7 @@ import MAlonzo.Code.Spec.Foreign.HSConsensus.TickNonce a import MAlonzo.Code.Spec.Foreign.HSConsensus.UpdateNonce as X (UpdateNonceEnv(..), UpdateNonceState(..), updnStep) import MAlonzo.Code.Spec.Foreign.HSConsensus.BlockDefinitions as X - (BHeader(..), BHBody(..), OCert(..)) + (BHeader(..), BHBody(..), OCert(..), AnnouncedEB(..)) import MAlonzo.Code.Spec.Foreign.HSConsensus.OperationalCertificate as X (OCertEnv(..), OCertState(..), OCertCounters, ocertStep, ocertDebug) import MAlonzo.Code.Spec.Foreign.HSConsensus.Protocol as X diff --git a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs index 10f3908405..8a4853f683 100644 --- a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs +++ b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs @@ -38,19 +38,26 @@ oc = MkOCert , ocΣ = 345 } +aeb :: AnnouncedEB +aeb = MkAnnouncedEB + { aebHash = 1000 + , aebSize = 10 + } + bhb :: BHBody bhb = MkBHBody - { bhbPrevHeader = Just 2 - , bhbIssuerVk = 456 - , bhbVrfVk = 567 - , bhbBlockNo = 1 - , bhbSlot = 2 - , bhbVrfRes = 678 - , bhbVrfPrf = 789 - , bhbBodySize = 1 - , bhbBodyHash = 890 - , bhbOc = oc - , bhbPv = (1, 0) + { bhbPrevHeader = Just 2 + , bhbIssuerVk = 456 + , bhbVrfVk = 567 + , bhbBlockNo = 1 + , bhbSlot = 2 + , bhbVrfRes = 678 + , bhbVrfPrf = 789 + , bhbBodySize = 1 + , bhbBodyHash = 890 + , bhbOc = oc + , bhbPv = (1, 0) + , bhbAnnouncedEB = Just aeb } bh :: BHeader diff --git a/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs index 9fa3c8fc68..f93f68f588 100644 --- a/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs +++ b/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs @@ -33,19 +33,26 @@ oc = MkOCert , ocΣ = 345 } +aeb :: AnnouncedEB +aeb = MkAnnouncedEB + { aebHash = 1000 + , aebSize = 10 + } + bhb :: BHBody bhb = MkBHBody - { bhbPrevHeader = Nothing - , bhbIssuerVk = 456 - , bhbVrfVk = 567 - , bhbBlockNo = 1 - , bhbSlot = 0 - , bhbVrfRes = 678 - , bhbVrfPrf = 789 - , bhbBodySize = 100 - , bhbBodyHash = 890 - , bhbOc = oc - , bhbPv = (1, 0) + { bhbPrevHeader = Nothing + , bhbIssuerVk = 456 + , bhbVrfVk = 567 + , bhbBlockNo = 1 + , bhbSlot = 0 + , bhbVrfRes = 678 + , bhbVrfPrf = 789 + , bhbBodySize = 100 + , bhbBodyHash = 890 + , bhbOc = oc + , bhbPv = (1, 0) + , bhbAnnouncedEB = Just aeb } bh :: BHeader diff --git a/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs index b8a46c1981..6579817e3b 100644 --- a/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs +++ b/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs @@ -35,19 +35,26 @@ oc = MkOCert , ocΣ = 345 } +aeb :: AnnouncedEB +aeb = MkAnnouncedEB + { aebHash = 1000 + , aebSize = 10 + } + bhb :: BHBody bhb = MkBHBody - { bhbPrevHeader = Nothing - , bhbIssuerVk = 456 - , bhbVrfVk = 567 - , bhbBlockNo = 1 - , bhbSlot = 0 - , bhbVrfRes = 678 - , bhbVrfPrf = 789 - , bhbBodySize = 100 - , bhbBodyHash = 890 - , bhbOc = oc - , bhbPv = (1, 0) + { bhbPrevHeader = Nothing + , bhbIssuerVk = 456 + , bhbVrfVk = 567 + , bhbBlockNo = 1 + , bhbSlot = 0 + , bhbVrfRes = 678 + , bhbVrfPrf = 789 + , bhbBodySize = 100 + , bhbBodyHash = 890 + , bhbOc = oc + , bhbPv = (1, 0) + , bhbAnnouncedEB = Just aeb } bh :: BHeader From 667c313fdc07ad763db95000946aa67c3574f6dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Wed, 9 Sep 2026 21:43:58 +0000 Subject: [PATCH 2/9] Add certified endorser block flag to block header --- docs/agda-spec/src/Spec/BlockDefinitions.lagda | 1 + docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs | 1 + .../agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs | 1 + docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs | 1 + 4 files changed, 4 insertions(+) diff --git a/docs/agda-spec/src/Spec/BlockDefinitions.lagda b/docs/agda-spec/src/Spec/BlockDefinitions.lagda index fed62f5691..b5b633965d 100644 --- a/docs/agda-spec/src/Spec/BlockDefinitions.lagda +++ b/docs/agda-spec/src/Spec/BlockDefinitions.lagda @@ -96,6 +96,7 @@ record BlockStructure : Type₁ where oc : OCert -- operational certificate pv : ProtVer -- protocol version announcedEB : Maybe AnnouncedEB -- announced endorser block + certifiedEB : Bool -- certifies the preceding endorser block \end{code} \end{AgdaSuppressSpace} \emph{Block Types} diff --git a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs index 8a4853f683..5902105e80 100644 --- a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs +++ b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs @@ -58,6 +58,7 @@ bhb = MkBHBody , bhbOc = oc , bhbPv = (1, 0) , bhbAnnouncedEB = Just aeb + , bhbCertifiedEB = False } bh :: BHeader diff --git a/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs index f93f68f588..d0d7d2f614 100644 --- a/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs +++ b/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs @@ -53,6 +53,7 @@ bhb = MkBHBody , bhbOc = oc , bhbPv = (1, 0) , bhbAnnouncedEB = Just aeb + , bhbCertifiedEB = False } bh :: BHeader diff --git a/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs index 6579817e3b..8a9bb1049d 100644 --- a/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs +++ b/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs @@ -55,6 +55,7 @@ bhb = MkBHBody , bhbOc = oc , bhbPv = (1, 0) , bhbAnnouncedEB = Just aeb + , bhbCertifiedEB = False } bh :: BHeader From b96091b1897e6700d7b82b21e6a2771cb798b9d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= <32520015+javierdiaz72@users.noreply.github.com> Date: Wed, 9 Sep 2026 20:09:38 -0300 Subject: [PATCH 3/9] Validate endorser block certification in block headers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add two header-level checks to CHAINHEAD, derived from the certificate inclusion rules of CIP-164: a header may only set certifiedEB if the last applied block announced an endorser block, and if at least 3*leiosHeaderPeriod + leiosVotingPeriod + leiosDiffusionPeriod has elapsed since that block. The certifying header does not repeat the hash of the endorser block it certifies, so LastAppliedBlock gains an aeb field recording what the last block announced. The three Leios periods are protocol parameters on PParams, read through getPParams as maxHeaderSize already is, and named after their counterparts in the ledger specification. They are wall-clock durations rather than slot counts: constants in slots could be changed neither by governance nor by a change of slot length. Milliseconds accordingly joins Coin in Ledger.Prelude.Base, matching where the ledger specification defines it. Comparing a duration against two slots needs a way to place a slot in time, so EpochStructure gains slotToTime. Expressing the check as slotToTime sℓ + certificationDelay ps ≤ slotToTime s rather than converting the delay into a slot count keeps certificationDelay in the units CIP-164 states it in, and leaves the rounding implicit in the arithmetic instead of fixing a rounding policy the CIP does not specify. A function rather than a slot-length constant, so that an instantiation with era-varying slot lengths remains expressible. Note that the announced endorser block size is deliberately left unchecked: per CIP-164 an incorrect size invalidates neither the header nor the block, and only costs the producer the votes of honest nodes. Split the Chain Head types figure in two, as it no longer fits on a page, and give LastAppliedBlock and ChainHeadState separate AgdaSuppressSpace blocks: sharing one made Agda emit an alignment preamble anchored past the column of the ChainHeadState declaration, which LaTeX rejects. Co-Authored-By: Claude Opus 5 (1M context) --- docs/agda-spec/src/Ledger/PParams.lagda | 21 ++++- docs/agda-spec/src/Ledger/Prelude/Base.agda | 4 + docs/agda-spec/src/Ledger/Types/Epoch.agda | 9 ++ docs/agda-spec/src/Spec/ChainHead.lagda | 90 ++++++++++++++++--- .../src/Spec/ChainHead/Properties.agda | 29 ++++-- .../Spec/Foreign/HSConsensus/ChainHead.agda | 2 + .../src/Spec/Foreign/HSConsensus/Core.agda | 1 + .../HSConsensus/ExternalStructures.agda | 10 ++- .../src/Spec/hs-src/test/ChainHeadSpec.hs | 82 ++++++++++++++--- .../agda-spec/src/latex/agda-latex-macros.sty | 2 + docs/agda-spec/src/latex/blockchain.tex | 3 + docs/agda-spec/src/latex/references.bib | 8 ++ 12 files changed, 222 insertions(+), 39 deletions(-) diff --git a/docs/agda-spec/src/Ledger/PParams.lagda b/docs/agda-spec/src/Ledger/PParams.lagda index 673f98750f..82ce8c9990 100644 --- a/docs/agda-spec/src/Ledger/PParams.lagda +++ b/docs/agda-spec/src/Ledger/PParams.lagda @@ -53,9 +53,15 @@ record PParams : Type where \end{code} \emph{Network group} \begin{code} - maxHeaderSize : ℕ - maxBlockSize : ℕ - pv : ProtVer + maxHeaderSize : ℕ + maxBlockSize : ℕ + pv : ProtVer +\end{code} +\emph{Network group (Leios)} +\begin{code} + leiosHeaderPeriod : Milliseconds + leiosVotingPeriod : Milliseconds + leiosDiffusionPeriod : Milliseconds \end{code} \end{AgdaMultiCode} \caption{Protocol parameter definitions} @@ -100,6 +106,15 @@ to the general purpose that each parameter serves. \item \NetworkGroup: parameters related to the network settings; \end{itemize} +The Leios parameters governing the timing of endorser block announcement, voting +and diffusion belong to the \NetworkGroup. They are wall-clock durations rather +than slot counts, so that they remain meaningful across a change of slot length; +where a slot must be compared against them, it is mapped to a wall-clock time by +\slotToTime. + +They are deliberately absent from \positivePParams: zero values are the +protocol's disabled state, and governance must be able to reach it. + Figure~\ref{fig:protocol-parameter-declarations} also defines the function \paramsWellFormed. It performs some sanity checks on protocol parameters. diff --git a/docs/agda-spec/src/Ledger/Prelude/Base.agda b/docs/agda-spec/src/Ledger/Prelude/Base.agda index a339c7e449..ff7aa998ef 100644 --- a/docs/agda-spec/src/Ledger/Prelude/Base.agda +++ b/docs/agda-spec/src/Ledger/Prelude/Base.agda @@ -5,3 +5,7 @@ module Ledger.Prelude.Base where open import Data.Nat Coin = ℕ + +-- A wall-clock duration in whole milliseconds. The implementation bounds this +-- to 32 bits (`Milliseconds32`); we do not model the bound here. +Milliseconds = ℕ diff --git a/docs/agda-spec/src/Ledger/Types/Epoch.agda b/docs/agda-spec/src/Ledger/Types/Epoch.agda index 3e531e3b68..2b7cdf2d77 100644 --- a/docs/agda-spec/src/Ledger/Types/Epoch.agda +++ b/docs/agda-spec/src/Ledger/Types/Epoch.agda @@ -30,6 +30,12 @@ record EpochStructure : Type₁ where firstSlot : Epoch → Slot StabilityWindow : Slot RandomnessStabilisationWindow : Slot + -- The wall-clock time at which a slot begins, measured from the same + -- origin for every slot. Used to interpret the Leios timing protocol + -- parameters, which CIP-164 specifies as durations rather than as slot + -- counts. A function rather than a slot-length constant, so that it + -- remains meaningful when the slot length changes between eras. + slotToTime : Slot → Milliseconds sucᵉ : Epoch → Epoch kesPeriod : Slot → KESPeriod _+ᵏ_ : KESPeriod → ℕ → KESPeriod @@ -86,6 +92,7 @@ record GlobalConstants : Type₁ where SlotsPerEpochᶜ : ℕ; ⦃ NonZero-SlotsPerEpochᶜ ⦄ : NonZero SlotsPerEpochᶜ StabilityWindowᶜ : ℕ RandomnessStabilisationWindowᶜ : ℕ + SlotLengthᶜ : ℕ -- in milliseconds Quorum : ℕ NetworkId : Network SlotsPerKESPeriodᶜ : ℕ; ⦃ NonZero-SlotsPerKESPeriodᶜ ⦄ : NonZero SlotsPerKESPeriodᶜ @@ -106,6 +113,8 @@ record GlobalConstants : Type₁ where .firstSlot e → e * SlotsPerEpochᶜ .StabilityWindow → StabilityWindowᶜ .RandomnessStabilisationWindow → RandomnessStabilisationWindowᶜ + -- A uniform slot length; the abstract interface does not require one. + .slotToTime s → s * SlotLengthᶜ .sucᵉ → suc ._+ᵉ'_ → _+_ .kesPeriod slot → slot / SlotsPerKESPeriodᶜ diff --git a/docs/agda-spec/src/Spec/ChainHead.lagda b/docs/agda-spec/src/Spec/ChainHead.lagda index 28f47da8c7..a582472515 100644 --- a/docs/agda-spec/src/Spec/ChainHead.lagda +++ b/docs/agda-spec/src/Spec/ChainHead.lagda @@ -64,14 +64,18 @@ ChainHeadEnv = NewEpochState record LastAppliedBlock : Type where \end{code} \begin{code}[hide] - constructor ⟦_,_,_⟧ℓ + constructor ⟦_,_,_,_⟧ℓ field \end{code} -\begin{code} - bℓ : BlockNo -- last block number - sℓ : Slot -- last slot - h : HashHeader -- latest header hash - +\begin{code} + bℓ : BlockNo -- last block number + sℓ : Slot -- last slot + h : HashHeader -- latest header hash + aeb : Maybe AnnouncedEB -- endorser block announced by the last block +\end{code} +\end{AgdaSuppressSpace} +\begin{AgdaSuppressSpace} +\begin{code} record ChainHeadState : Type where \end{code} \begin{code}[hide] @@ -94,6 +98,13 @@ data \begin{code} _⊢_⇀⦇_,CHAINHEAD⦈_ : ChainHeadEnv → ChainHeadState → BHeader → ChainHeadState → Type \end{code} +\end{AgdaAlign} +\caption{Chain Head transition system types} +\label{fig:ts-types:chainhead} +\end{figure*} + +\begin{figure*}[h] +\begin{AgdaAlign} \emph{Chain Head helper functions} \begin{code} extractPoolDistr : PoolDelegatedStake → PoolDistr @@ -115,23 +126,42 @@ chainChecks maxpv (maxBHSize , maxBBSize , protocolVersion) bh = open BHeader; open BHBody (bh .body) lastAppliedHash : Maybe LastAppliedBlock → Maybe HashHeader -lastAppliedHash nothing = nothing -lastAppliedHash (just ⟦ _ , _ , h ⟧ℓ) = just h +lastAppliedHash nothing = nothing +lastAppliedHash (just ⟦ _ , _ , h , _ ⟧ℓ) = just h prtlSeqChecks : Maybe LastAppliedBlock → BHeader → Type -prtlSeqChecks nothing bh = ⊤ -prtlSeqChecks lab@(just ⟦ bℓ , sℓ , _ ⟧ℓ) bh = sℓ < slot × bℓ + 1 ≡ blockNo × ph ≡ prevHeader +prtlSeqChecks nothing bh = ⊤ +prtlSeqChecks lab@(just ⟦ bℓ , sℓ , _ , _ ⟧ℓ) bh = sℓ < slot × bℓ + 1 ≡ blockNo × ph ≡ prevHeader where open BHeader; open BHBody (bh .body) ph = lastAppliedHash lab \end{code} +\begin{code} +LeiosPeriods : Type +LeiosPeriods = Milliseconds × Milliseconds × Milliseconds + +leiosPeriods : PParams → LeiosPeriods +leiosPeriods pp = leiosHeaderPeriod , leiosVotingPeriod , leiosDiffusionPeriod + where open PParams pp + +certificationDelay : LeiosPeriods → Milliseconds +certificationDelay (hdr , vote , diff) = 3 * hdr + vote + diff + +certChecks : LeiosPeriods → Maybe LastAppliedBlock → Bool → Slot → Type +certChecks _ _ false _ = ⊤ +certChecks _ nothing true _ = ⊥ +certChecks _ (just ⟦ _ , _ , _ , nothing ⟧ℓ) true _ = ⊥ +certChecks ps (just ⟦ _ , sℓ , _ , just _ ⟧ℓ) true s = + slotToTime sℓ + certificationDelay ps ≤ slotToTime s +\end{code} \end{AgdaAlign} -\caption{Chain Head transition system types and functions} -\label{fig:ts-types:chainhead} +\caption{Chain Head transition system functions} +\label{fig:ts-funs:chainhead} \end{figure*} The transition checks the following things -(via the functions \afun{chainChecks} and \afun{prtlSeqChecks} from Figure~\ref{fig:ts-types:chainhead}): +(via the functions \afun{chainChecks}, \afun{prtlSeqChecks} and \afun{certChecks} +from Figure~\ref{fig:ts-funs:chainhead}): \begin{itemize} \item The slot in the block header body is larger than the last slot recorded. \item The block number increases by exactly one. @@ -143,8 +173,33 @@ The transition checks the following things maximal size that the protocol parameters allow for block bodies. \item The node is not obsolete, meaning that the major component of the protocol version in the protocol parameters is not bigger than the constant \afld{MaxMajorPV}. +\item If the block header claims to certify an endorser block, then the last applied + block announced one, and enough slots have elapsed since it did. \end{itemize} +The last of these checks deserves comment, since it is the only one concerned with +endorser blocks. A block header carries a flag \afld{certifiedEB} recording whether the +block certifies the endorser block announced by its predecessor; the hash of that +endorser block is not repeated in the header, as it is already available from the +predecessor's \afld{announcedEB} field. Consequently the last applied block must +retain what it announced, which is why \afld{LastAppliedBlock} carries an +\afld{aeb} field. + +A certificate may only be included once $3 L_\text{hdr} + L_\text{vote} + +L_\text{diff}$ has elapsed since the block that announced the endorser +block~\cite{cip_164}, so that the endorser block has had time to reach the whole +network. These three protocol parameters are wall-clock durations, so the comparison +is made in wall-clock time: the two slots are mapped to times by \slotToTime, rather +than the delay being converted to a number of slots. Because a header +that sets \afld{certifiedEB} obliges the corresponding body to carry a matching +certificate, this constraint can be checked on the header alone --- exactly the kind +of check that Property~\ref{prop:header-only-validation} exists to license. + +Note that the \afld{size} component of \afld{announcedEB} is deliberately \emph{not} +checked here. As specified in \cite{cip_164}, an incorrect announced size invalidates +neither the header nor the block; it merely costs the block producer the votes of +honest nodes, which validate the endorser block itself. + \begin{figure*}[h] \begin{code}[hide] private variable @@ -165,11 +220,12 @@ data _⊢_⇀⦇_,CHAINHEAD⦈_ where pp = getPParams forecast; open PParams nₚₕ = prevHashToNonce (lastAppliedHash lab) pd = extractPoolDistr (getPoolDelegatedStake forecast) - lab′ = just ⟦ blockNo , slot , headerHash bh ⟧ℓ + lab′ = just ⟦ blockNo , slot , headerHash bh , announcedEB ⟧ℓ in ∙ prtlSeqChecks lab bh ∙ _ ⊢ nes ⇀⦇ slot ,TICKF⦈ forecast ∙ chainChecks MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh + ∙ certChecks (leiosPeriods pp) lab certifiedEB slot ∙ ⟦ ηc , nₚₕ ⟧ᵗᵉ ⊢ ⟦ η₀ , ηh ⟧ᵗˢ ⇀⦇ ne ,TICKN⦈ ⟦ η₀′ , ηh′ ⟧ᵗˢ ∙ ⟦ pd , η₀′ ⟧ᵖᵉ ⊢ ⟦ cs , ηv , ηc ⟧ᵖˢ ⇀⦇ bh ,PRTCL⦈ ⟦ cs′ , ηv′ , ηc′ ⟧ᵖˢ ──────────────────────────────── @@ -195,4 +251,10 @@ has the following predicate failures: there is a \emph{BlockSizeTooLarge} failure. \item If the major component of the protocol version is larger than \afld{MaxMajorPV}, there is a \emph{ObsoleteNode} failure. +\item If the block header certifies an endorser block but there is no last applied + block, or the last applied block announced no endorser block, there is a + \emph{NoEndorserBlockToCertify} failure. +\item If the block header certifies an endorser block but less than + $3 L_\text{hdr} + L_\text{vote} + L_\text{diff}$ has elapsed since the last + applied block, there is a \emph{CertifiedTooEarly} failure. \end{enumerate} diff --git a/docs/agda-spec/src/Spec/ChainHead/Properties.agda b/docs/agda-spec/src/Spec/ChainHead/Properties.agda index 04a878a1f8..3fa0d9ee2a 100644 --- a/docs/agda-spec/src/Spec/ChainHead/Properties.agda +++ b/docs/agda-spec/src/Spec/ChainHead/Properties.agda @@ -31,8 +31,8 @@ open import Spec.ChainHead crypto nonces es bs af li rs instance prtlSeqChecks⁇ : prtlSeqChecks ⁇² - prtlSeqChecks⁇ {nothing} {_} .dec = yes tt - prtlSeqChecks⁇ {lab@(just ⟦ bℓ , sℓ , _ ⟧ℓ)} {bh} .dec = + prtlSeqChecks⁇ {nothing} {_} .dec = yes tt + prtlSeqChecks⁇ {lab@(just ⟦ bℓ , sℓ , _ , _ ⟧ℓ)} {bh} .dec = sℓ computeProof) ≡ success s′ - completeness ⟦ cs′ , η₀′ , ηv′ , ηc′ , ηh′ , lab′ ⟧ᶜˢ (Chain-Head (psc , tickfStep , cc , ticknStep , prtclStep)) + completeness ⟦ cs′ , η₀′ , ηv′ , ηc′ , ηh′ , lab′ ⟧ᶜˢ (Chain-Head (psc , tickfStep , cc , ec , ticknStep , prtclStep)) with ¿ prtlSeqChecks ¿² lab bh ... | no ¬psc = contradiction psc ¬psc ... | yes _ @@ -100,6 +110,9 @@ instance (let pp = getPParams forecast; open PParams in chainChecks? MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh) ... | no ¬cc = contradiction cc ¬cc + ... | yes _ + with certChecks? (leiosPeriods (getPParams forecast)) lab certifiedEB slot + ... | no ¬ec = contradiction ec ¬ec ... | yes _ with (let e₂ = getEpoch forecast; ne = (e₁ ≠ e₂) diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ChainHead.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ChainHead.agda index 3b4b69cfcc..619b78573d 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ChainHead.agda +++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ChainHead.agda @@ -5,6 +5,8 @@ open import Spec.Foreign.ExternalFunctions open import Foreign.Haskell.Coerce open import Spec.Foreign.HSConsensus.BaseTypes +-- NOTE: Needed for the `AnnouncedEB` instances used by `LastAppliedBlock` below. +open import Spec.Foreign.HSConsensus.BlockDefinitions open import Spec.ChainHead DummyCrypto DummyNonces DummyEpochStructure DummyBlockStructure DummyAbstractFunctions DummyLedgerInterface DummyRationalExtStructure unquoteDecl = do diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda index fa8ba59212..385effcce4 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda +++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda @@ -50,6 +50,7 @@ module Implementation where SlotsPerEpochᶜ = 100 StabilityWindowᶜ = 10 RandomnessStabilisationWindowᶜ = 20 + SlotLengthᶜ = 1000 -- one second per slot Quorum = 1 NetworkId = 0 SlotsPerKESPeriodᶜ = 5 diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda index 71d86816b4..04a85e4163 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda +++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda @@ -142,7 +142,15 @@ instance HSLedgerInterface : LedgerInterface HSLedgerInterface = record { NewEpochState = ℕ - ; getPParams = const $ record { maxHeaderSize = 1; maxBlockSize = 2; pv = 1 , 0 } + -- NOTE: With a slot length of 1000ms, the certification delay these imply is + -- 3 * 1000 + 2000 + 3000 = 8000ms, i.e. 8 slots. + ; getPParams = const $ record + { maxHeaderSize = 1 + ; maxBlockSize = 2 + ; pv = 1 , 0 + ; leiosHeaderPeriod = 1000 + ; leiosVotingPeriod = 2000 + ; leiosDiffusionPeriod = 3000 } ; getEpoch = const 1 ; getPoolDelegatedStake = const $ fromListᵐ ((457 , (10 , 568)) ∷ (111 , (10 , 222)) ∷ (333 , (10 , 444)) ∷ []) ; adoptGenesisDelegs = _+_ diff --git a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs index 5902105e80..021672da58 100644 --- a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs +++ b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs @@ -13,11 +13,16 @@ import Lib che :: ChainHeadEnv che = 123 +isFailure :: ComputationResult e a -> Bool +isFailure (Failure _) = True +isFailure (Success _) = False + lab :: LastAppliedBlock lab = MkLastAppliedBlock - { labBℓ = 0 - , labSℓ = 0 - , labH = 2 + { labBℓ = 0 + , labSℓ = 0 + , labH = 2 + , labAeb = Just aeb } chs :: ChainHeadState @@ -69,9 +74,10 @@ bh = MkBHeader lab' :: LastAppliedBlock lab' = MkLastAppliedBlock - { labBℓ = 1 - , labSℓ = 2 - , labH = 2 + { labBℓ = 1 + , labSℓ = 2 + , labH = 2 + , labAeb = Just aeb } chs' :: ChainHeadState @@ -90,7 +96,8 @@ chs' = MkChainHeadState Given nes = 123 - lab = Just ⟦ 0 , 0 , 2 ⟧ℓ + aeb = ⟨ hash = 1000 , size = 10 ⟩ + lab = Just ⟦ 0 , 0 , 2 , Just aeb ⟧ℓ cs = [ 457 .-> 233 , 999 .-> 888 ] ⟦ cs , η₀ , ηv , ηc , ηh , lab ⟧ᶜˢ = ⟦ cs , 3 , 4 , 2 , 4 , lab ⟧ᶜˢ @@ -100,28 +107,41 @@ chs' = MkChainHeadState Also, - lastAppliedHash lab = lastAppliedHash (Just ⟦ 0 , 0 , 2 ⟧ℓ) = Just 2 + lastAppliedHash lab = lastAppliedHash (Just ⟦ 0 , 0 , 2 , Just aeb ⟧ℓ) = Just 2 e₁ = getEpoch nes = getEpoch 123 = 1 e₂ = getEpoch forecast = getEpoch 126 = 1 ne = (e₁ ≠ e₂) = (1 ≠ 1) = False - pp = getPParams forecast = getPParams 126 = { maxHeaderSize = 1; maxBlockSize = 2; pv = (1 , 0) } + pp = getPParams forecast = getPParams 126 + = { maxHeaderSize = 1; maxBlockSize = 2; pv = (1 , 0) + ; leiosHeaderPeriod = 1000; leiosVotingPeriod = 2000 + ; leiosDiffusionPeriod = 3000 } + certificationDelay (leiosPeriods pp) = 3 * 1000 + 2000 + 3000 = 8000ms + slotToTime s = s * 1000, so certifying at slot s requires + slotToTime sℓ + 8000 ≤ slotToTime s, i.e. s ≥ sℓ + 8 nₚₕ = prevHashToNonce (lastAppliedHash lab) = prevHashToNonce 2 = 0 pd = extractPoolDistr (getPoolDelegatedStake forecast) = extractPoolDistr (getPoolDelegatedStake 126) = extractPoolDistr ({(457 , (10 , 568)), (111 , (10 , 222)), (333 , (10 , 444))}) = {(457 , (1 / 3 , 568)), (111 , (1 / 3 , 222)), (333 , (1 / 3 , 444))} - lab′ = Just ⟦ blockNo , slot , headerHash bh ⟧ℓ = Just ⟦ 1 , 2 , 2 ⟧ℓ + lab′ = Just ⟦ blockNo , slot , headerHash bh , announcedEB ⟧ℓ = Just ⟦ 1 , 2 , 2 , Just aeb ⟧ℓ then - prtlSeqChecks lab bh = prtlSeqChecks (just ⟦ 0 , 0 , 2 ⟧ℓ) bh = 0 < 2 × 0 + 1 ≡ 1 × Just 2 ≡ Just 2 = True + prtlSeqChecks lab bh = prtlSeqChecks (just ⟦ 0 , 0 , 2 , Just aeb ⟧ℓ) bh + = 0 < 2 × 0 + 1 ≡ 1 × Just 2 ≡ Just 2 + = True chainChecks MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh = chainChecks 1 (1 , 2 , (1 , 0)) bh = 1 ≤ 1 × 1 ≤ 1 × 1 ≤ 2 = True + certChecks (leiosPeriods pp) lab certifiedEB slot + = certChecks (1000 , 2000 , 3000) lab False 2 + = ⊤ -- the header certifies nothing + = True + ⟦ ηc , nₚₕ ⟧ᵗᵉ ⊢ ⟦ η₀ , ηh ⟧ᵗˢ ⇀⦇ ne ,TICKN⦈ ⟦ η₀′ , ηh′ ⟧ᵗˢ <===> ⟦ 2 , 0 ⟧ᵗᵉ ⊢ ⟦ 3 , 4 ⟧ᵗˢ ⇀⦇ False ,TICKN⦈ ⟦ 3 , 4 ⟧ᵗˢ @@ -135,16 +155,52 @@ chs' = MkChainHeadState nes ⊢ ⟦ cs , η₀ , ηv , ηc , ηh , lab ⟧ᶜˢ ⇀⦇ bh ,CHAINHEAD⦈ ⟦ cs′ , η₀′ , ηv′ , ηc′ , ηh′ , lab′ ⟧ᶜˢ <===> 123 ⊢ - ⟦ [ 457 .-> 233 , 999 .-> 888 ] , 3 , 4 , 2 , 4 , Just ⟦ 0 , 0 , 2 ⟧ℓ ⟧ᶜˢ + ⟦ [ 457 .-> 233 , 999 .-> 888 ] , 3 , 4 , 2 , 4 , Just ⟦ 0 , 0 , 2 , Just aeb ⟧ℓ ⟧ᶜˢ ⇀⦇ bh ,CHAINHEAD⦈ - ⟦ [ 457 .-> 234 , 999 .-> 888 ] , 3 , 5 , 2 , 4 , Just ⟦ 1 , 2 , 2 ⟧ℓ ⟧ᶜˢ + ⟦ [ 457 .-> 234 , 999 .-> 888 ] , 3 , 5 , 5 , 4 , Just ⟦ 1 , 2 , 2 , Just aeb ⟧ℓ ⟧ᶜˢ -} +-- Headers that certify the endorser block announced by `lab`. The certification +-- delay is 3 * leiosHeaderPeriod + leiosVotingPeriod + leiosDiffusionPeriod = +-- 8000ms, which at a slot length of 1000ms is 8 slots; `lab` is at slot 0, so +-- slot 8 is the earliest slot at which certification is permitted. + +certifyingBhbAt :: Slot -> BHBody +certifyingBhbAt s = bhb { bhbSlot = s , bhbCertifiedEB = True } + +-- Certifies at slot 2, i.e. 6 slots too early. +bhTooEarly :: BHeader +bhTooEarly = bh { bhBody = certifyingBhbAt 2 } + +-- Certifies at slot 10, comfortably past the delay. +bhInTime :: BHeader +bhInTime = bh { bhBody = certifyingBhbAt 10 } + +-- As `chs`, but the last applied block announced no endorser block, so there is +-- nothing for `bhInTime` to certify. +chsNoAnnouncement :: ChainHeadState +chsNoAnnouncement = chs { chsLab = Just lab { labAeb = Nothing } } + +-- Expected result of applying `bhInTime` to `chs`. Only the slot recorded in the +-- last applied block differs from `chs'`: the nonces evolve identically because +-- hBNonce does not depend on the slot, and slot 10 is still far enough from the +-- end of the epoch (100) for UPDN to update both nonces. +chsCertified :: ChainHeadState +chsCertified = chs' + { chsLab = Just lab' { labSℓ = 10 } + } + spec :: Spec spec = do describe "chainheadStep" $ do it "chainheadStep results in the expected state" $ chainheadStep dummyExternalFunctions che chs bh @?= Success chs' + it "chainheadStep accepts a header certifying after the required delay" $ + chainheadStep dummyExternalFunctions che chs bhInTime @?= Success chsCertified + it "chainheadStep rejects a header certifying before the required delay" $ + isFailure (chainheadStep dummyExternalFunctions che chs bhTooEarly) @?= True + it "chainheadStep rejects a header certifying an unannounced endorser block" $ + isFailure (chainheadStep dummyExternalFunctions che chsNoAnnouncement bhInTime) @?= True -- NOTE: Uncomment to run the debug version. -- describe (unpack $ chainheadDebug dummyExternalFunctions che chs bh) $ do -- it "shows its argument" True diff --git a/docs/agda-spec/src/latex/agda-latex-macros.sty b/docs/agda-spec/src/latex/agda-latex-macros.sty index a07ae489c4..400fb2ef74 100644 --- a/docs/agda-spec/src/latex/agda-latex-macros.sty +++ b/docs/agda-spec/src/latex/agda-latex-macros.sty @@ -336,6 +336,8 @@ \newcommand{\NeedsHash}{\AgdaFunction{NeedsHash}\xspace} \newcommand{\negInduction}{\AgdaFunction{negInduction}\xspace} \newcommand{\NetworkGroup}{\AgdaInductiveConstructor{NetworkGroup}\xspace} +\newcommand{\slotToTime}{\AgdaField{slotToTime}\xspace} +\newcommand{\positivePParams}{\AgdaFunction{positivePParams}\xspace} \newcommand{\new}{\AgdaGeneralizable{new}\xspace} \newcommand{\NewCommittee}{\AgdaInductiveConstructor{NewCommittee}\xspace} \newcommand{\NewConstitution}{\AgdaInductiveConstructor{NewConstitution}\xspace} diff --git a/docs/agda-spec/src/latex/blockchain.tex b/docs/agda-spec/src/latex/blockchain.tex index 61203f12fa..15f5375940 100644 --- a/docs/agda-spec/src/latex/blockchain.tex +++ b/docs/agda-spec/src/latex/blockchain.tex @@ -5,6 +5,9 @@ \section{Blockchain Layer} consensus. The main transition rule is $\mathsf{CHAINHEAD}$ which calls the subrules $\mathsf{TICKF}$, $\mathsf{TICKN}$ and $\mathsf{PRTCL}$. +Block headers additionally carry the fields by which a block announces and certifies +an \emph{endorser block}, as introduced by Ouroboros Linear Leios~\cite{cip_164}. + \input{Spec/BlockDefinitions} \clearpage diff --git a/docs/agda-spec/src/latex/references.bib b/docs/agda-spec/src/latex/references.bib index d273840922..28cfedff68 100644 --- a/docs/agda-spec/src/latex/references.bib +++ b/docs/agda-spec/src/latex/references.bib @@ -21,6 +21,14 @@ @misc{ouroboros_praos url = {https://eprint.iacr.org/2017/573} } +@misc{cip_164, + title = {{CIP-0164: Ouroboros Linear Leios --- Greater Transaction Throughput}}, + author = {William Wolff and Brian W. Bush and Sebastian Nagel and Nicolas Frisby and Giorgos Panagiotakos and Andre Knispel and Yves Hauser and Simon Gellis and Paul Clark}, + year = {2025}, + note = {Status: Proposed}, + howpublished = {\url{https://cips.cardano.org/cip/CIP-164}} +} + @misc{delegation_design, title ={Design Specification for Delegation and Incentives in Cardano, IOHK Deliverable SL-D1}, author = {IOHK Formal Methods Team}, From b3aedfa6be5d943039b9b54b8fe21254c34c9c82 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= <32520015+javierdiaz72@users.noreply.github.com> Date: Mon, 28 Sep 2026 12:49:53 -0300 Subject: [PATCH 4/9] Convert the Leios periods to slots with the genesis slot length MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The ledger specification's Leios design note settles how the summed periods become a slot bound (docs/leios/design-note.md, "Alignment with the consensus specification", item 2): CIP-164 converts them with the genesis slotLength, rounded up, and both specifications are to share one definition of the conversion and agree on the boundary sℓ + certificationDelay ≤ s. So SlotLengthᶜ, nonzero, joins GlobalConstants, and durationToSlots sits beside Milliseconds in Ledger.Prelude.Base. It takes the slot length as an argument rather than naming SlotLengthᶜ, because the note has the conversion travelling with Milliseconds and the constant travelling with the epoch structure when both move to the common library; naming the constant would fuse the two units. This replaces the slotToTime formulation, which compared wall-clock times instead of converting. That agreed with this one at every boundary, but it was a second shape for a quantity the two specifications are meant to share, which is what the note exists to prevent. EpochStructure keeps a field for the conversion, as Slot is abstract and only the structure can present durationToSlots' result as one. The ledger specification's Slot is abstract in the same way, so its certificationDelay will need the same; if it lands a different shape, this should follow. Co-Authored-By: Claude Opus 5 (1M context) --- docs/agda-spec/src/Ledger/PParams.lagda | 4 ++-- docs/agda-spec/src/Ledger/Prelude/Base.agda | 8 ++++++++ docs/agda-spec/src/Ledger/Types/Epoch.agda | 17 ++++++++--------- docs/agda-spec/src/Spec/ChainHead.lagda | 12 ++++++------ .../src/Spec/ChainHead/Properties.agda | 3 +-- .../src/Spec/hs-src/test/ChainHeadSpec.hs | 6 +++--- docs/agda-spec/src/latex/agda-latex-macros.sty | 2 +- 7 files changed, 29 insertions(+), 23 deletions(-) diff --git a/docs/agda-spec/src/Ledger/PParams.lagda b/docs/agda-spec/src/Ledger/PParams.lagda index 82ce8c9990..d8683849ce 100644 --- a/docs/agda-spec/src/Ledger/PParams.lagda +++ b/docs/agda-spec/src/Ledger/PParams.lagda @@ -109,8 +109,8 @@ to the general purpose that each parameter serves. The Leios parameters governing the timing of endorser block announcement, voting and diffusion belong to the \NetworkGroup. They are wall-clock durations rather than slot counts, so that they remain meaningful across a change of slot length; -where a slot must be compared against them, it is mapped to a wall-clock time by -\slotToTime. +where they must be compared against a slot, their sum is converted to a number of +slots by \slotsFromDuration. They are deliberately absent from \positivePParams: zero values are the protocol's disabled state, and governance must be able to reach it. diff --git a/docs/agda-spec/src/Ledger/Prelude/Base.agda b/docs/agda-spec/src/Ledger/Prelude/Base.agda index ff7aa998ef..6c2c7d15dc 100644 --- a/docs/agda-spec/src/Ledger/Prelude/Base.agda +++ b/docs/agda-spec/src/Ledger/Prelude/Base.agda @@ -3,9 +3,17 @@ module Ledger.Prelude.Base where open import Data.Nat +open import Data.Nat.DivMod using (_/_) Coin = ℕ -- A wall-clock duration in whole milliseconds. The implementation bounds this -- to 32 bits (`Milliseconds32`); we do not model the bound here. Milliseconds = ℕ + +-- The number of slots spanning a duration, rounded up. CIP-164 converts the +-- Leios periods to a slot count using the genesis slot length. Defined here +-- rather than against the genesis constant itself, so that it travels with +-- `Milliseconds` when both move to the common library. +durationToSlots : (slotLength : Milliseconds) → ⦃ NonZero slotLength ⦄ → Milliseconds → ℕ +durationToSlots l d = (d + l ∸ 1) / l diff --git a/docs/agda-spec/src/Ledger/Types/Epoch.agda b/docs/agda-spec/src/Ledger/Types/Epoch.agda index 2b7cdf2d77..19f5ac7a15 100644 --- a/docs/agda-spec/src/Ledger/Types/Epoch.agda +++ b/docs/agda-spec/src/Ledger/Types/Epoch.agda @@ -30,12 +30,12 @@ record EpochStructure : Type₁ where firstSlot : Epoch → Slot StabilityWindow : Slot RandomnessStabilisationWindow : Slot - -- The wall-clock time at which a slot begins, measured from the same - -- origin for every slot. Used to interpret the Leios timing protocol - -- parameters, which CIP-164 specifies as durations rather than as slot - -- counts. A function rather than a slot-length constant, so that it - -- remains meaningful when the slot length changes between eras. - slotToTime : Slot → Milliseconds + -- The number of slots spanning a wall-clock duration, rounded up. Used + -- to interpret the Leios timing protocol parameters, which CIP-164 + -- specifies as durations rather than as slot counts. A field because + -- Slot is abstract here: `durationToSlots` yields a number, which only + -- the structure can present as a Slot. + slotsFromDuration : Milliseconds → Slot sucᵉ : Epoch → Epoch kesPeriod : Slot → KESPeriod _+ᵏ_ : KESPeriod → ℕ → KESPeriod @@ -92,7 +92,7 @@ record GlobalConstants : Type₁ where SlotsPerEpochᶜ : ℕ; ⦃ NonZero-SlotsPerEpochᶜ ⦄ : NonZero SlotsPerEpochᶜ StabilityWindowᶜ : ℕ RandomnessStabilisationWindowᶜ : ℕ - SlotLengthᶜ : ℕ -- in milliseconds + SlotLengthᶜ : Milliseconds; ⦃ NonZero-SlotLengthᶜ ⦄ : NonZero SlotLengthᶜ Quorum : ℕ NetworkId : Network SlotsPerKESPeriodᶜ : ℕ; ⦃ NonZero-SlotsPerKESPeriodᶜ ⦄ : NonZero SlotsPerKESPeriodᶜ @@ -113,8 +113,7 @@ record GlobalConstants : Type₁ where .firstSlot e → e * SlotsPerEpochᶜ .StabilityWindow → StabilityWindowᶜ .RandomnessStabilisationWindow → RandomnessStabilisationWindowᶜ - -- A uniform slot length; the abstract interface does not require one. - .slotToTime s → s * SlotLengthᶜ + .slotsFromDuration d → durationToSlots SlotLengthᶜ d .sucᵉ → suc ._+ᵉ'_ → _+_ .kesPeriod slot → slot / SlotsPerKESPeriodᶜ diff --git a/docs/agda-spec/src/Spec/ChainHead.lagda b/docs/agda-spec/src/Spec/ChainHead.lagda index a582472515..07f48c7a43 100644 --- a/docs/agda-spec/src/Spec/ChainHead.lagda +++ b/docs/agda-spec/src/Spec/ChainHead.lagda @@ -144,15 +144,15 @@ leiosPeriods : PParams → LeiosPeriods leiosPeriods pp = leiosHeaderPeriod , leiosVotingPeriod , leiosDiffusionPeriod where open PParams pp -certificationDelay : LeiosPeriods → Milliseconds -certificationDelay (hdr , vote , diff) = 3 * hdr + vote + diff +certificationDelay : LeiosPeriods → Slot +certificationDelay (hdr , vote , diff) = slotsFromDuration (3 * hdr + vote + diff) certChecks : LeiosPeriods → Maybe LastAppliedBlock → Bool → Slot → Type certChecks _ _ false _ = ⊤ certChecks _ nothing true _ = ⊥ certChecks _ (just ⟦ _ , _ , _ , nothing ⟧ℓ) true _ = ⊥ certChecks ps (just ⟦ _ , sℓ , _ , just _ ⟧ℓ) true s = - slotToTime sℓ + certificationDelay ps ≤ slotToTime s + sℓ + certificationDelay ps ≤ s \end{code} \end{AgdaAlign} \caption{Chain Head transition system functions} @@ -188,9 +188,9 @@ retain what it announced, which is why \afld{LastAppliedBlock} carries an A certificate may only be included once $3 L_\text{hdr} + L_\text{vote} + L_\text{diff}$ has elapsed since the block that announced the endorser block~\cite{cip_164}, so that the endorser block has had time to reach the whole -network. These three protocol parameters are wall-clock durations, so the comparison -is made in wall-clock time: the two slots are mapped to times by \slotToTime, rather -than the delay being converted to a number of slots. Because a header +network. These three protocol parameters are wall-clock durations, so their sum is +converted to a number of slots by \slotsFromDuration, using the genesis slot length +and rounding up. Because a header that sets \afld{certifiedEB} obliges the corresponding body to carry a matching certificate, this constraint can be checked on the header alone --- exactly the kind of check that Property~\ref{prop:header-only-validation} exists to license. diff --git a/docs/agda-spec/src/Spec/ChainHead/Properties.agda b/docs/agda-spec/src/Spec/ChainHead/Properties.agda index 3fa0d9ee2a..53249eff12 100644 --- a/docs/agda-spec/src/Spec/ChainHead/Properties.agda +++ b/docs/agda-spec/src/Spec/ChainHead/Properties.agda @@ -53,8 +53,7 @@ certChecks? : ∀ ps lab b s → Dec (certChecks ps lab b s) certChecks? _ _ false _ = yes tt certChecks? _ nothing true _ = no λ () certChecks? _ (just ⟦ _ , _ , _ , nothing ⟧ℓ) true _ = no λ () -certChecks? ps (just ⟦ _ , sℓ , _ , just _ ⟧ℓ) true s = - slotToTime sℓ + certificationDelay ps ≤? slotToTime s +certChecks? ps (just ⟦ _ , sℓ , _ , just _ ⟧ℓ) true s = sℓ + certificationDelay ps ≤? s instance diff --git a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs index 021672da58..d31df111ee 100644 --- a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs +++ b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs @@ -116,9 +116,9 @@ chs' = MkChainHeadState = { maxHeaderSize = 1; maxBlockSize = 2; pv = (1 , 0) ; leiosHeaderPeriod = 1000; leiosVotingPeriod = 2000 ; leiosDiffusionPeriod = 3000 } - certificationDelay (leiosPeriods pp) = 3 * 1000 + 2000 + 3000 = 8000ms - slotToTime s = s * 1000, so certifying at slot s requires - slotToTime sℓ + 8000 ≤ slotToTime s, i.e. s ≥ sℓ + 8 + certificationDelay (leiosPeriods pp) + = slotsFromDuration (3 * 1000 + 2000 + 3000) + = ⌈ 8000 / SlotLengthᶜ ⌉ = ⌈ 8000 / 1000 ⌉ = 8 slots nₚₕ = prevHashToNonce (lastAppliedHash lab) = prevHashToNonce 2 = 0 pd = extractPoolDistr (getPoolDelegatedStake forecast) = extractPoolDistr (getPoolDelegatedStake 126) diff --git a/docs/agda-spec/src/latex/agda-latex-macros.sty b/docs/agda-spec/src/latex/agda-latex-macros.sty index 400fb2ef74..1c2f7d4d32 100644 --- a/docs/agda-spec/src/latex/agda-latex-macros.sty +++ b/docs/agda-spec/src/latex/agda-latex-macros.sty @@ -336,7 +336,7 @@ \newcommand{\NeedsHash}{\AgdaFunction{NeedsHash}\xspace} \newcommand{\negInduction}{\AgdaFunction{negInduction}\xspace} \newcommand{\NetworkGroup}{\AgdaInductiveConstructor{NetworkGroup}\xspace} -\newcommand{\slotToTime}{\AgdaField{slotToTime}\xspace} +\newcommand{\slotsFromDuration}{\AgdaField{slotsFromDuration}\xspace} \newcommand{\positivePParams}{\AgdaFunction{positivePParams}\xspace} \newcommand{\new}{\AgdaGeneralizable{new}\xspace} \newcommand{\NewCommittee}{\AgdaInductiveConstructor{NewCommittee}\xspace} From 8dff1db9f85fbb7479cae58ef34c5bc92256a29e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= <32520015+javierdiaz72@users.noreply.github.com> Date: Fri, 16 Oct 2026 16:02:54 -0300 Subject: [PATCH 5/9] Exercise the certification delay boundary and its rounding MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The dummy periods summed to 8000ms against a slot length of 1000ms, so the delay was a whole number of slots and rounding down would have given the same answer; the cases also certified at slots 2 and 10 against a delay of 8, leaving the boundary untested. leiosDiffusionPeriod becomes 3500ms, so the delay is ⌈8500/1000⌉ = 9 where rounding down would give 8, and two cases pin the boundary: slot 8 is rejected, slot 9 accepted. Replacing the ceiling with a floor now fails the first of those and nothing else. Co-Authored-By: Claude Opus 5 (1M context) --- .../HSConsensus/ExternalStructures.agda | 8 +++-- .../src/Spec/hs-src/test/ChainHeadSpec.hs | 33 +++++++++++++++---- 2 files changed, 32 insertions(+), 9 deletions(-) diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda index 04a85e4163..f1f1443d4e 100644 --- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda +++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda @@ -142,15 +142,17 @@ instance HSLedgerInterface : LedgerInterface HSLedgerInterface = record { NewEpochState = ℕ - -- NOTE: With a slot length of 1000ms, the certification delay these imply is - -- 3 * 1000 + 2000 + 3000 = 8000ms, i.e. 8 slots. + -- NOTE: The certification delay these imply is 3 * 1000 + 2000 + 3500 = + -- 8500ms, which at a slot length of 1000ms is ⌈8500/1000⌉ = 9 slots. The + -- sum is deliberately not a whole number of slots, so that the tests + -- distinguish rounding up from rounding down. ; getPParams = const $ record { maxHeaderSize = 1 ; maxBlockSize = 2 ; pv = 1 , 0 ; leiosHeaderPeriod = 1000 ; leiosVotingPeriod = 2000 - ; leiosDiffusionPeriod = 3000 } + ; leiosDiffusionPeriod = 3500 } ; getEpoch = const 1 ; getPoolDelegatedStake = const $ fromListᵐ ((457 , (10 , 568)) ∷ (111 , (10 , 222)) ∷ (333 , (10 , 444)) ∷ []) ; adoptGenesisDelegs = _+_ diff --git a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs index d31df111ee..904761c6e9 100644 --- a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs +++ b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs @@ -115,10 +115,10 @@ chs' = MkChainHeadState pp = getPParams forecast = getPParams 126 = { maxHeaderSize = 1; maxBlockSize = 2; pv = (1 , 0) ; leiosHeaderPeriod = 1000; leiosVotingPeriod = 2000 - ; leiosDiffusionPeriod = 3000 } + ; leiosDiffusionPeriod = 3500 } certificationDelay (leiosPeriods pp) - = slotsFromDuration (3 * 1000 + 2000 + 3000) - = ⌈ 8000 / SlotLengthᶜ ⌉ = ⌈ 8000 / 1000 ⌉ = 8 slots + = slotsFromDuration (3 * 1000 + 2000 + 3500) + = ⌈ 8500 / SlotLengthᶜ ⌉ = ⌈ 8500 / 1000 ⌉ = 9 slots nₚₕ = prevHashToNonce (lastAppliedHash lab) = prevHashToNonce 2 = 0 pd = extractPoolDistr (getPoolDelegatedStake forecast) = extractPoolDistr (getPoolDelegatedStake 126) @@ -162,16 +162,27 @@ chs' = MkChainHeadState -- Headers that certify the endorser block announced by `lab`. The certification -- delay is 3 * leiosHeaderPeriod + leiosVotingPeriod + leiosDiffusionPeriod = --- 8000ms, which at a slot length of 1000ms is 8 slots; `lab` is at slot 0, so --- slot 8 is the earliest slot at which certification is permitted. +-- 8500ms, which at a slot length of 1000ms is ⌈8500/1000⌉ = 9 slots; `lab` is +-- at slot 0, so slot 9 is the earliest slot at which certification is +-- permitted. Note that rounding down would give 8 instead, so the boundary +-- cases below also pin the direction of the rounding. certifyingBhbAt :: Slot -> BHBody certifyingBhbAt s = bhb { bhbSlot = s , bhbCertifiedEB = True } --- Certifies at slot 2, i.e. 6 slots too early. +-- Certifies at slot 2, i.e. 7 slots too early. bhTooEarly :: BHeader bhTooEarly = bh { bhBody = certifyingBhbAt 2 } +-- Certifies at slot 8: the latest slot that is still too early, and the slot a +-- conversion that rounded down would wrongly permit. +bhOneShort :: BHeader +bhOneShort = bh { bhBody = certifyingBhbAt 8 } + +-- Certifies at slot 9: the earliest slot permitted. +bhAtBoundary :: BHeader +bhAtBoundary = bh { bhBody = certifyingBhbAt 9 } + -- Certifies at slot 10, comfortably past the delay. bhInTime :: BHeader bhInTime = bh { bhBody = certifyingBhbAt 10 } @@ -190,6 +201,12 @@ chsCertified = chs' { chsLab = Just lab' { labSℓ = 10 } } +-- As `chsCertified`, for `bhAtBoundary`. +chsAtBoundary :: ChainHeadState +chsAtBoundary = chs' + { chsLab = Just lab' { labSℓ = 9 } + } + spec :: Spec spec = do describe "chainheadStep" $ do @@ -199,6 +216,10 @@ spec = do chainheadStep dummyExternalFunctions che chs bhInTime @?= Success chsCertified it "chainheadStep rejects a header certifying before the required delay" $ isFailure (chainheadStep dummyExternalFunctions che chs bhTooEarly) @?= True + it "chainheadStep rejects a header certifying one slot short of the delay" $ + isFailure (chainheadStep dummyExternalFunctions che chs bhOneShort) @?= True + it "chainheadStep accepts a header certifying exactly at the delay" $ + chainheadStep dummyExternalFunctions che chs bhAtBoundary @?= Success chsAtBoundary it "chainheadStep rejects a header certifying an unannounced endorser block" $ isFailure (chainheadStep dummyExternalFunctions che chsNoAnnouncement bhInTime) @?= True -- NOTE: Uncomment to run the debug version. From fcbc907e1b1060db8459aa809d3513d9620f10e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= <32520015+javierdiaz72@users.noreply.github.com> Date: Fri, 16 Oct 2026 16:03:17 -0300 Subject: [PATCH 6/9] Hold every epoch structure to rounding the certification delay up MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit slotsFromDuration was a field, so only ℕEpochStructure rounded up and any other instance could shorten the delay, or ignore the duration entirely, without the specification noticing. The rounding is what CIP-164's Step 5 specifies and what its security argument depends on. EpochStructure now takes the genesis SlotLength as a constant and derives slotsFromDuration from it, so the rounding holds by construction. ℕtoSlot injects the resulting count into the slot semiring, as ℕtoEpoch already does for epochs; this relies on 1# denoting one slot, which addSlot and firstSlot assume too. Co-Authored-By: Claude Opus 5 (1M context) --- docs/agda-spec/src/Ledger/Types/Epoch.agda | 24 +++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/docs/agda-spec/src/Ledger/Types/Epoch.agda b/docs/agda-spec/src/Ledger/Types/Epoch.agda index 19f5ac7a15..f2d771c218 100644 --- a/docs/agda-spec/src/Ledger/Types/Epoch.agda +++ b/docs/agda-spec/src/Ledger/Types/Epoch.agda @@ -30,12 +30,13 @@ record EpochStructure : Type₁ where firstSlot : Epoch → Slot StabilityWindow : Slot RandomnessStabilisationWindow : Slot - -- The number of slots spanning a wall-clock duration, rounded up. Used - -- to interpret the Leios timing protocol parameters, which CIP-164 - -- specifies as durations rather than as slot counts. A field because - -- Slot is abstract here: `durationToSlots` yields a number, which only - -- the structure can present as a Slot. - slotsFromDuration : Milliseconds → Slot + -- The genesis slot length, with which CIP-164's Leios timing protocol + -- parameters are converted from durations to slot counts. A constant + -- rather than the conversion itself, so that `slotsFromDuration` below + -- rounds up in every instance and not merely in ℕEpochStructure: the + -- security argument depends on the delay not being shortened. + SlotLength : Milliseconds + ⦃ NonZero-SlotLength ⦄ : NonZero SlotLength sucᵉ : Epoch → Epoch kesPeriod : Slot → KESPeriod _+ᵏ_ : KESPeriod → ℕ → KESPeriod @@ -76,6 +77,15 @@ record EpochStructure : Type₁ where ℕtoEpoch zero = epoch 0# ℕtoEpoch (suc n) = sucᵉ (ℕtoEpoch n) + -- The canonical image of a number in the slot semiring, i.e. that many + -- slots. Relies on 1# denoting one slot, as `addSlot` below already does. + ℕtoSlot : ℕ → Slot + ℕtoSlot n = additionVia (1# +ˢ_) n 0# + + -- The number of slots spanning a wall-clock duration, rounded up. + slotsFromDuration : Milliseconds → Slot + slotsFromDuration d = ℕtoSlot (durationToSlots SlotLength d) + instance addSlot : HasAdd Slot addSlot ._+_ = _+ˢ_ @@ -113,7 +123,7 @@ record GlobalConstants : Type₁ where .firstSlot e → e * SlotsPerEpochᶜ .StabilityWindow → StabilityWindowᶜ .RandomnessStabilisationWindow → RandomnessStabilisationWindowᶜ - .slotsFromDuration d → durationToSlots SlotLengthᶜ d + .SlotLength → SlotLengthᶜ .sucᵉ → suc ._+ᵉ'_ → _+_ .kesPeriod slot → slot / SlotsPerKESPeriodᶜ From 3736be270f86dfec6cfc65ea0245056c6703d6a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= <32520015+javierdiaz72@users.noreply.github.com> Date: Fri, 16 Oct 2026 15:42:35 -0300 Subject: [PATCH 7/9] Attribute the header/body agreement to the ledger rules The header's certifiedEB bit obliging the body to carry a matching certificate is enforced by the ledger, not here, so do not present it as a header-only check. --- docs/agda-spec/src/Spec/ChainHead.lagda | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/docs/agda-spec/src/Spec/ChainHead.lagda b/docs/agda-spec/src/Spec/ChainHead.lagda index 07f48c7a43..883a64ba6f 100644 --- a/docs/agda-spec/src/Spec/ChainHead.lagda +++ b/docs/agda-spec/src/Spec/ChainHead.lagda @@ -190,10 +190,8 @@ L_\text{diff}$ has elapsed since the block that announced the endorser block~\cite{cip_164}, so that the endorser block has had time to reach the whole network. These three protocol parameters are wall-clock durations, so their sum is converted to a number of slots by \slotsFromDuration, using the genesis slot length -and rounding up. Because a header -that sets \afld{certifiedEB} obliges the corresponding body to carry a matching -certificate, this constraint can be checked on the header alone --- exactly the kind -of check that Property~\ref{prop:header-only-validation} exists to license. +and rounding up. A header that sets \afld{certifiedEB} obliges the corresponding body +to carry a matching certificate, thus this constraint is checked by the ledger rules. Note that the \afld{size} component of \afld{announcedEB} is deliberately \emph{not} checked here. As specified in \cite{cip_164}, an incorrect announced size invalidates From 427dc836ef92e12cc906c4a1ebb6644bb8c39661 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= <32520015+javierdiaz72@users.noreply.github.com> Date: Fri, 16 Oct 2026 16:01:50 -0300 Subject: [PATCH 8/9] Take PParams in certificationDelay and certChecks The ledger specification will define certificationDelay over its own PParams, so matching the signature keeps the correspondence between the two specifications a matter of reading, not translation. This also removes LeiosPeriods and the leiosPeriods accessor. The accessor existed only because spelling the three fields out at the call site overran the width of the figure, and passing the whole record is narrower than either form. What it costs is that the type of certChecks no longer records that it reads just three of the parameters. Co-Authored-By: Claude Opus 5 (1M context) --- docs/agda-spec/src/Spec/ChainHead.lagda | 19 +++++++------------ .../src/Spec/ChainHead/Properties.agda | 8 ++++---- .../src/Spec/hs-src/test/ChainHeadSpec.hs | 6 +++--- 3 files changed, 14 insertions(+), 19 deletions(-) diff --git a/docs/agda-spec/src/Spec/ChainHead.lagda b/docs/agda-spec/src/Spec/ChainHead.lagda index 883a64ba6f..0546aa774f 100644 --- a/docs/agda-spec/src/Spec/ChainHead.lagda +++ b/docs/agda-spec/src/Spec/ChainHead.lagda @@ -137,22 +137,17 @@ prtlSeqChecks lab@(just ⟦ bℓ , sℓ , _ , _ ⟧ℓ) bh = sℓ < slot × bℓ ph = lastAppliedHash lab \end{code} \begin{code} -LeiosPeriods : Type -LeiosPeriods = Milliseconds × Milliseconds × Milliseconds - -leiosPeriods : PParams → LeiosPeriods -leiosPeriods pp = leiosHeaderPeriod , leiosVotingPeriod , leiosDiffusionPeriod +certificationDelay : PParams → Slot +certificationDelay pp = slotsFromDuration + (3 * leiosHeaderPeriod + leiosVotingPeriod + leiosDiffusionPeriod) where open PParams pp -certificationDelay : LeiosPeriods → Slot -certificationDelay (hdr , vote , diff) = slotsFromDuration (3 * hdr + vote + diff) - -certChecks : LeiosPeriods → Maybe LastAppliedBlock → Bool → Slot → Type +certChecks : PParams → Maybe LastAppliedBlock → Bool → Slot → Type certChecks _ _ false _ = ⊤ certChecks _ nothing true _ = ⊥ certChecks _ (just ⟦ _ , _ , _ , nothing ⟧ℓ) true _ = ⊥ -certChecks ps (just ⟦ _ , sℓ , _ , just _ ⟧ℓ) true s = - sℓ + certificationDelay ps ≤ s +certChecks pp (just ⟦ _ , sℓ , _ , just _ ⟧ℓ) true s = + sℓ + certificationDelay pp ≤ s \end{code} \end{AgdaAlign} \caption{Chain Head transition system functions} @@ -223,7 +218,7 @@ data _⊢_⇀⦇_,CHAINHEAD⦈_ where ∙ prtlSeqChecks lab bh ∙ _ ⊢ nes ⇀⦇ slot ,TICKF⦈ forecast ∙ chainChecks MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh - ∙ certChecks (leiosPeriods pp) lab certifiedEB slot + ∙ certChecks pp lab certifiedEB slot ∙ ⟦ ηc , nₚₕ ⟧ᵗᵉ ⊢ ⟦ η₀ , ηh ⟧ᵗˢ ⇀⦇ ne ,TICKN⦈ ⟦ η₀′ , ηh′ ⟧ᵗˢ ∙ ⟦ pd , η₀′ ⟧ᵖᵉ ⊢ ⟦ cs , ηv , ηc ⟧ᵖˢ ⇀⦇ bh ,PRTCL⦈ ⟦ cs′ , ηv′ , ηc′ ⟧ᵖˢ ──────────────────────────────── diff --git a/docs/agda-spec/src/Spec/ChainHead/Properties.agda b/docs/agda-spec/src/Spec/ChainHead/Properties.agda index 53249eff12..b1f923cd42 100644 --- a/docs/agda-spec/src/Spec/ChainHead/Properties.agda +++ b/docs/agda-spec/src/Spec/ChainHead/Properties.agda @@ -49,11 +49,11 @@ chainChecks? maxpv (maxBHSize , maxBBSize , protocolVersion) bh = m = proj₁ protocolVersion open BHeader; open BHBody (bh .body) -certChecks? : ∀ ps lab b s → Dec (certChecks ps lab b s) +certChecks? : ∀ pp lab b s → Dec (certChecks pp lab b s) certChecks? _ _ false _ = yes tt certChecks? _ nothing true _ = no λ () certChecks? _ (just ⟦ _ , _ , _ , nothing ⟧ℓ) true _ = no λ () -certChecks? ps (just ⟦ _ , sℓ , _ , just _ ⟧ℓ) true s = sℓ + certificationDelay ps ≤? s +certChecks? pp (just ⟦ _ , sℓ , _ , just _ ⟧ℓ) true s = sℓ + certificationDelay pp ≤? s instance @@ -91,7 +91,7 @@ instance case chainChecks? MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh of λ where (no ¬cc) → failure (genErrors ¬cc) (yes cc) → - case certChecks? (leiosPeriods pp) lab certifiedEB slot of λ where + case certChecks? pp lab certifiedEB slot of λ where (no ¬ec) → failure (genErrors ¬ec) (yes ec) → do (⟦ η₀′ , _ ⟧ᵗˢ , ticknStep) ← computeTICKN ticknΓ ticknSt ne @@ -110,7 +110,7 @@ instance in chainChecks? MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh) ... | no ¬cc = contradiction cc ¬cc ... | yes _ - with certChecks? (leiosPeriods (getPParams forecast)) lab certifiedEB slot + with certChecks? (getPParams forecast) lab certifiedEB slot ... | no ¬ec = contradiction ec ¬ec ... | yes _ with diff --git a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs index 904761c6e9..325c31fc99 100644 --- a/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs +++ b/docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs @@ -116,7 +116,7 @@ chs' = MkChainHeadState = { maxHeaderSize = 1; maxBlockSize = 2; pv = (1 , 0) ; leiosHeaderPeriod = 1000; leiosVotingPeriod = 2000 ; leiosDiffusionPeriod = 3500 } - certificationDelay (leiosPeriods pp) + certificationDelay pp = slotsFromDuration (3 * 1000 + 2000 + 3500) = ⌈ 8500 / SlotLengthᶜ ⌉ = ⌈ 8500 / 1000 ⌉ = 9 slots nₚₕ = prevHashToNonce (lastAppliedHash lab) = prevHashToNonce 2 = 0 @@ -137,8 +137,8 @@ chs' = MkChainHeadState = 1 ≤ 1 × 1 ≤ 1 × 1 ≤ 2 = True - certChecks (leiosPeriods pp) lab certifiedEB slot - = certChecks (1000 , 2000 , 3000) lab False 2 + certChecks pp lab certifiedEB slot + = certChecks pp lab False 2 = ⊤ -- the header certifies nothing = True From f5816398eb5e8d2ec5ea17fe218ddaa682d5f076 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= <32520015+javierdiaz72@users.noreply.github.com> Date: Fri, 16 Oct 2026 16:43:51 -0300 Subject: [PATCH 9/9] List the announced endorser block among the chain head state The subsection enumerates what the chain head state consists of, and adding the aeb field to LastAppliedBlock left that list describing a state one component smaller than the figure beside it shows. Co-Authored-By: Claude Opus 5 (1M context) --- docs/agda-spec/src/Spec/ChainHead.lagda | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/agda-spec/src/Spec/ChainHead.lagda b/docs/agda-spec/src/Spec/ChainHead.lagda index 0546aa774f..cf07755fdf 100644 --- a/docs/agda-spec/src/Spec/ChainHead.lagda +++ b/docs/agda-spec/src/Spec/ChainHead.lagda @@ -18,6 +18,7 @@ state is shown in Figure~\ref{fig:ts-types:chainhead} and it consists of the fol \item The last header hash \afld{h}. \item The last slot \afld{sℓ}. \item The last block number \afld{bℓ}. + \item The endorser block announced by the last block \afld{aeb}. \end{itemize} \begin{code}[hide]