[FEAT] - Adapt the formal spec to include Linear Leios

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,13 @@ 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 sub-second delivery periods can be expressed.
+
+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.

docs/agda-spec/src/Ledger/Prelude/Base.agda

@@ -3,5 +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

docs/agda-spec/src/Ledger/Types/Epoch.agda

@@ -30,6 +30,13 @@ record EpochStructure : Type₁ where
         firstSlot                     : Epoch → Slot
         StabilityWindow               : Slot
         RandomnessStabilisationWindow : 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
@@ -70,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 ._+_ = _+ˢ_
@@ -86,6 +102,7 @@ record GlobalConstants : Type₁ where
          SlotsPerEpochᶜ : ℕ; ⦃ NonZero-SlotsPerEpochᶜ ⦄ : NonZero SlotsPerEpochᶜ
          StabilityWindowᶜ : ℕ
          RandomnessStabilisationWindowᶜ : ℕ
+         SlotLengthᶜ : Milliseconds; ⦃ NonZero-SlotLengthᶜ ⦄ : NonZero SlotLengthᶜ
          Quorum : ℕ
          NetworkId : Network
          SlotsPerKESPeriodᶜ : ℕ; ⦃ NonZero-SlotsPerKESPeriodᶜ ⦄ : NonZero SlotsPerKESPeriodᶜ
@@ -106,6 +123,7 @@ record GlobalConstants : Type₁ where
     .firstSlot e                   → e * SlotsPerEpochᶜ
     .StabilityWindow               → StabilityWindowᶜ
     .RandomnessStabilisationWindow → RandomnessStabilisationWindowᶜ
+    .SlotLength                    → SlotLengthᶜ
     .sucᵉ                          → suc
     ._+ᵉ'_                         → _+_
     .kesPeriod slot                → slot / SlotsPerKESPeriodᶜ

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,19 @@ 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
+      certifiesEB : Bool              -- claims to certify the preceding block's EB
 \end{code}
 \end{AgdaSuppressSpace}
 \emph{Block Types}
@@ -101,6 +120,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 +135,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 +147,3 @@ instance
   unquoteDecl Show-BHeader = derive-Show
     [(quote BHeader , Show-BHeader)]
 \end{code}
-\end{AgdaAlign}
-\caption{Block definitions}
-\label{fig:defs:blocks}
-\end{figure*}

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]
@@ -64,14 +65,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 +99,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 +127,37 @@ 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}
+certificationDelay : PParams → Slot
+certificationDelay pp = slotsFromDuration
+    (3 * leiosHeaderPeriod + leiosVotingPeriod + leiosDiffusionPeriod)
+  where open PParams pp
+
+certChecks : PParams → Maybe LastAppliedBlock → Bool → Slot → Type
+certChecks _  _                                false _ = ⊤
+certChecks _  nothing                          true  _ = ⊥
+certChecks _  (just ⟦ _ , _  , _ , nothing ⟧ℓ) true  _ = ⊥
+certChecks pp (just ⟦ _ , sℓ , _ , just _  ⟧ℓ) true  s =
+  sℓ + certificationDelay pp ≤ 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 +169,31 @@ 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{certifiesEB} 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 their sum is
+converted to a number of slots by \slotsFromDuration, using the genesis slot length
+and rounding up. A header that sets \afld{certifiesEB} 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
+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 +214,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 pp lab certifiesEB slot
     ∙ ⟦ ηc , nₚₕ ⟧ᵗᵉ ⊢ ⟦ η₀ , ηh ⟧ᵗˢ ⇀⦇ ne ,TICKN⦈ ⟦ η₀′ , ηh′ ⟧ᵗˢ
     ∙ ⟦ pd , η₀′ ⟧ᵖᵉ ⊢ ⟦ cs , ηv , ηc ⟧ᵖˢ ⇀⦇ bh ,PRTCL⦈ ⟦ cs′ , ηv′ , ηc′ ⟧ᵖˢ
     ────────────────────────────────
@@ -195,4 +245,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}