Skip to content

Types

Leios Primitive Types

Leios adds the endorser block (EB) to the chain's traffic; this module defines it and its identifier. The announcement that names an EB is a header field, defined with the block in BlockBody.

The hash carriers (TxRefHash, EBHash, hashEBRefs) are fields of the era's LeiosCryptoStructure record, which this module takes as a parameter.

Declared byte sizes are represented as ℕ.

{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Core.Specification.Crypto using (CryptoStructure)
open import Ledger.Dijkstra.Specification.Crypto using (LeiosCryptoStructure)

module Ledger.Dijkstra.Specification.Leios.Types
  (cs : CryptoStructure) (lc : LeiosCryptoStructure cs)
  (open LeiosCryptoStructure lc using (TxRefHash; EBHash; hashEBRefs))
  where

Endorser blocks

record EndorserBlock : Type where
  field
    ebTxRefs : List (TxRefHash × ℕ)

An endorser block (EB) is the ordered list of its transaction references, each the pair of a reference hash and a declared byte size.

A reference hash is not a transaction id

A TxRefHash covers the complete transaction bytes, witnesses included. The ledger's transaction id identifies only the transaction body; this is true of every transaction, not only those an endorser block references, and it is why an id could not pin the exact transactions the voters validated.

The list type keeps the ordering of the references but does not forbid repeated reference hashes: duplicate-freedom is a validity condition on the announced block, stated beside the nonemptiness and size conditions.

Endorser block identifiers

hashEB : EndorserBlock → EBHash
hashEB eb = hashEBRefs (EndorserBlock.ebTxRefs eb)

hashEB fixes the identity of an endorser block as the CIP does, "computed from the complete EB structure": the identifier is the hash of the reference structure itself, so it is checkable before any referenced transaction data arrives.

What hashEB deliberately does not fix is the preimage, since hashEBRefs is abstract and no byte-exact serialization of the reference list is pinned.1

unquoteDecl DecEq-EndorserBlock = derive-DecEq ((quote EndorserBlock , DecEq-EndorserBlock) ∷ [])

  1. This boundary is a known conformance obstacle: an implementation can agree with the spec on every rule yet disagree on which endorser block an identifier denotes, so pinning the preimage is a prerequisite for conformance testing. (A precedent for this is the block-body hash, whose segmented preimage exists only in implementation internals.) ↩