Skip to content 
{-# OPTIONS --safe #-}
open import Ledger.Prelude
open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction
 
module Ledger.Conway.Specification.BlockBody
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Ledger txs abs
open import Ledger.Conway.Specification.Rewards txs abs

Blocks

The block follows mostly the definition of the Shelley specification. One notable difference is that the size and the hash of the block body are fields of the block, instead of functions.

record BHBody : Type where
  field
    bvkcold : VKey
    bsize   : ℕ
    slot    : Slot
    bhash   : KeyHash
    hBbsize : ℕ

record BHeader : Type where
  field
    bhbody : BHBody
    bhsig  : Sig

record Block : Type where
  field
    bheader     : BHeader
    ts          : List Tx
    bBodySize   : ℕ
    bBodyHash   : KeyHash
    ≡-bBodySize : bBodySize ≡ BHBody.hBbsize (BHeader.bhbody bheader)
    ≡-bBodyHash : bBodyHash ≡ BHBody.bhash (BHeader.bhbody bheader)

Block Body Transition

The Block Body Transition updates the block body state which comprises the ledger state and the map describing the produced blocks. The environment of the BBODY transition includes the protocol parameters and the accounting state.

The helper function incrBlocks counts the number of non-overlay blocks produced by each stake pool.

The signal of the BBODY rule is a block from which we extract:

  • the sequence of transactions, txs = block .ts, of the block;
  • the block header body bhb = block .bheader .bhbody;
  • the hash of the verification key of the issuer of the block, hk = hash (bhb .bvkcold).

The transition is executed if the following preconditions are met:

  • The size of the block body matches the value given in the block header body.
  • The hash of the block body matches the value given in the block header body.
  • The LEDGERS transition succeeds.

After this, the transition system updates the mapping of the hashed stake pool keys to the incremented value of produced blocks n + 1, provided the current slot is not an overlay slot.

The BBODY rule has two predicate failures:

  • if the size of the block body in the header is not equal to the real size of the block body, there is a WrongBlockBodySize failure.
  • if the hash of the block body is not also the hash of transactions, there is an InvalidBodyHash failure.
BBodyEnv : Type
BBodyEnv = EnactState × Acnt

BBodyState : Type
BBodyState = LState × BlocksMade

incrBlocks : KeyHash → BlocksMade → BlocksMade
incrBlocks hk b = b ∪⁺ singletonᵐ hk 1

data _⊢_⇀⦇_,BBODY⦈_
  : BBodyEnv → BBodyState → Block → BBodyState → Type where

  BBODY-Block-Body : ∀ {acnt ls ls' b block es} →
    let
      open BHeader
      open BHBody
      open Block
      open EnactState
      txs = block .ts
      bhb = block .bheader .bhbody
      hk = hash (bhb .bvkcold)
      pp = PParamsOf es
      Γ  = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.BlockBody.html#3236}{\htmlId{3333}{\htmlClass{Bound}{\text{bhb}}}}\, \,\htmlId{3337}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.BlockBody.html#786}{\htmlId{3338}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Prelude.html#2381}{\htmlId{3345}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.BlockBody.html#3118}{\htmlId{3347}{\htmlClass{Bound}{\text{es}}}}\, \,\htmlId{3350}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Enact.html#1739}{\htmlId{3351}{\htmlClass{Field}{\text{constitution}}}}\, \,\href{Ledger.Prelude.html#2381}{\htmlId{3364}{\htmlClass{Function Operator}{\text{∣}}}}\, \\ \,\href{Ledger.Conway.Specification.BlockBody.html#3302}{\htmlId{3368}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.BlockBody.html#3118}{\htmlId{3373}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Prelude.Base.html#985}{\htmlId{3378}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Conway.Specification.BlockBody.html#3098}{\htmlId{3389}{\htmlClass{Bound}{\text{acnt}}}}\, \end{pmatrix}$

     in
    ∙ block .bBodySize ≡ bhb .hBbsize
    ∙ block .bBodyHash ≡ bhb .bhash
    ∙ Γ ⊢ ls ⇀⦇ txs ,LEDGERS⦈ ls'
    ────────────────────────────────
    (es , acnt) ⊢ ls , b ⇀⦇ block ,BBODY⦈ (ls' , incrBlocks hk b)