Validity

Endorser-Block Validity

An endorser block is valid for a ledger state when its closure (that is, its referenced transactions, resolved and taken in reference order) is exactly what its references describe, and applies to that state as a block's transactions would.

The present module defines this property and denotes it by ValidEB. It is what an honest committee member checks before voting and what a certificate certifies. The block rules name it as a premise, and the quorum-safety argument names it as what a voter checked.

{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Abstract
open import Ledger.Dijkstra.Specification.Transaction

module Ledger.Dijkstra.Specification.Leios.Validity
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Prelude
open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
open import Data.List.Relation.Unary.Unique.DecPropositional using (unique?)
open import Ledger.Dijkstra.Specification.Ledger txs abs
open import Ledger.Dijkstra.Specification.Ledgers txs abs
open import Ledger.Dijkstra.Specification.Utxo txs abs using (totalExUnits; totalRefScriptsSize)
open import Ledger.Dijkstra.Specification.Leios.Types cryptoStructure leiosCryptoStructure
open import Ledger.Dijkstra.Specification.Crypto using (LeiosCryptoStructure)
open LeiosCryptoStructure leiosCryptoStructure using (TxRefHash)

The references match the closure

refOf : TopLevelTx → TxRefHash × ℕ
refOf tx = txRefHash tx , SizeOf tx

The rules receive the closure resolved, and refOf is what the EB's reference to a transaction must be: the hash of its complete bytes paired with its declared size. ValidEB below requires the reference list to be, entry for entry, refOf of the closure; order is part of the agreement, since the closure applies in reference order.

The bounds

The environment and state are those of the announcing block. The closure of the EB is judged against the ledger state the announcing block left and the parameters in force there.

module _ {Γ : LedgerEnv} {ls : LedgerState} where
  open PParams (PParamsOf Γ)

  record WithinEBBounds (eb : EndorserBlock) (closure : List TopLevelTx) : Type where
    field
      ebSizeOK          : ebSize eb ≤ leiosMaxEBSize
      txsSizeOK         : ∑ˡ[ tx ← closure ] SizeOf tx ≤ leiosMaxEBTxsSize

The fields of WithinEBBounds are the endorser-block bounds of CIP-164's Table 3, as follows:

• ebSizeOK: the size of the EB itself is at most S_EB (leiosMaxEBSize);
• txsSizeOK: the total size of the referenced transactions is at most S_EB-tx (leiosMaxEBTxsSize).

The table's remaining rows are enforced by LEDGERS: the closure's Plutus steps and memory fit leiosMaxEBExUnits, one ExUnits value for the table's two budget rows; and the total size of the closure's reference scripts is at most S_EB-ref (leiosMaxRefScriptSizePerEB).

Validity

  record ValidEB (eb : EndorserBlock) (closure : List TopLevelTx) : Type where
    field
      nonemptyOK    : closure ≢ []
      uniqueRefsOK  : Unique (map proj₁ (EndorserBlock.ebTxRefs eb))
      refsOK        : EndorserBlock.ebTxRefs eb ≡ map refOf closure
      boundsOK      : WithinEBBounds eb closure
      extensionOK   : ∃[ ls' ] $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Leios.Validity.html#2347}{\htmlId{3706}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#3393}{\htmlId{3710}{\htmlClass{Function}{\text{leiosMaxRefScriptSizePerEB}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#3349}{\htmlId{3739}{\htmlClass{Function}{\text{leiosMaxEBExUnits}}}}\, \end{pmatrix}$ ⊢ ls ⇀⦇ closure ,LEDGERS⦈ ls'

Of CIP-164's six vote-casting conditions (Step 3), the two that the ledger can check land here, namely,

• the closure is a valid extension, through the same LEDGERS relation the block rules use;
• the block is nonempty.

The other four (header arrival within the header diffusion period, equivocation detection, the validation deadline, chain position) are node-local checks, so they stay at the protocol level.

Duplicate-freedom of the references is not a vote condition but an invariant of the EB structure itself: the CIP's reference list is an insertion-ordered map that admits no duplicate keys (Appendix B). The list type here does not encode that invariant, so ValidEB states it as uniqueRefsOK.

private
  nonempty? : ∀ {A : Type} (xs : List A) → Dec (xs ≢ [])
  nonempty? []       = no λ p → p refl
  nonempty? (_ ∷ _)  = yes λ ()

module _ {Γ : LedgerEnv} {ls : LedgerState} where
  open PParams (PParamsOf Γ)

  instance
    Dec-WithinEBBounds : ∀ {eb closure} → WithinEBBounds {Γ} {ls} eb closure ⁇
    Dec-WithinEBBounds {eb} {closure} = ⁇ map′
      (λ (a , b) → record { ebSizeOK = a ; txsSizeOK = b })
      (λ w → let open WithinEBBounds w in ebSizeOK , txsSizeOK)
      ¿ ebSize eb ≤ leiosMaxEBSize
      × ∑ˡ[ tx ← closure ] SizeOf tx ≤ leiosMaxEBTxsSize ¿

  -- Given the extension, the remaining conditions decide validity.
  ValidEB? : ∀ eb closure → (∃[ ls' ] _ ⊢ ls ⇀⦇ closure ,LEDGERS⦈ ls') → Dec (ValidEB {Γ} {ls} eb closure)
  ValidEB? eb closure ext = map′
    (λ (n , u , r , b) → record { nonemptyOK = n ; uniqueRefsOK = u ; refsOK = r ; boundsOK = b ; extensionOK = ext })
    (λ v → let open ValidEB v in nonemptyOK , uniqueRefsOK , refsOK , boundsOK)
    (nonempty? closure ×-dec unique? _≟_ (map proj₁ (EndorserBlock.ebTxRefs eb))
                       ×-dec ¿ EndorserBlock.ebTxRefs eb ≡ map refOf closure × WithinEBBounds {Γ} {ls} eb closure ¿)