Skip to content 
{-# OPTIONS --safe #-}

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

module Ledger.Dijkstra.Specification.Leios.Validity
  (transactionStructure : _) (open TransactionStructure transactionStructure)
  (abs : AbstractFunctions transactionStructure) (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 transactionStructure abs
open import Ledger.Dijkstra.Specification.Ledgers transactionStructure abs
open import Ledger.Dijkstra.Specification.Utxo transactionStructure 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)

Endorser-Block Validity

An Endorser Block is valid for a ledger state when:

  1. the referenced transactions (resolved and taken in reference order) are exactly what it describes,

  2. it satisfies the size limits given by Leios-specific protocol parameters, and

  3. the list of transactions forms a valid extension of the ledger state.

The present module defines the EB transition system to validate endorser blocks.

private
  variable
    Γ : LedgerEnv
    ls ls' : LedgerState
    eb : EndorserBlock
    txs : List TopLevelTx

  open PParams
  open EndorserBlock

Auxiliary Types and Functions

The predicate EBWellFormed ensures the EndorserBlock is well-formed:

EBWellFormed : EndorserBlock → Type
EBWellFormed eb = ebTxRefs eb ≢ [] × Unique (map proj₁ (ebTxRefs eb))

EB Transition System

data  _⊢_⇀⦇_,EB⦈_ : LedgerEnv × List TopLevelTx → LedgerState → EndorserBlock → LedgerState → Type where
  EB :
    let
      pp = PParamsOf Γ
    in
      ∙ EBWellFormed eb
      ∙ ebTxRefs eb ≡ map (λ tx → txRefHash tx , SizeOf tx) txs
      ∙ ebSize eb ≤ pp .leiosMaxEBSize
      ∙ ∑ˡ[ tx ← txs ] SizeOf tx ≤ pp .leiosMaxEBTxsSize
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Leios.Validity.html#1651}{\htmlId{2637}{\htmlClass{Generalizable}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Leios.Validity.html#2419}{\htmlId{2641}{\htmlClass{Bound}{\text{pp}}}}\, \,\htmlId{2644}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#3393}{\htmlId{2645}{\htmlClass{Field}{\text{leiosMaxRefScriptSizePerEB}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Leios.Validity.html#2419}{\htmlId{2674}{\htmlClass{Bound}{\text{pp}}}}\, \,\htmlId{2677}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#3349}{\htmlId{2678}{\htmlClass{Field}{\text{leiosMaxEBExUnits}}}}\, \end{pmatrix}$ ⊢ ls ⇀⦇ txs ,LEDGERS⦈ ls'
      ────────────────────────────────
      (Γ , txs) ⊢ ls ⇀⦇ eb ,EB⦈ ls'

The EB enforces the size bounds of CIP-164's Table 3 on endorser blocks:

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

The table's remaining rows are enforced by LEDGERS:

  • the execution units of Plutus scripts fit leiosMaxEBExUnits, and
  • the total size of the referenced transactions' reference scripts is at most S_EB-ref (leiosMaxRefScriptSizePerEB).