{-# OPTIONS --safe #-}
open import Ledger.Dijkstra.Specification.Abstract
open import Ledger.Dijkstra.Specification.Transaction

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

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Enact govStructure
open import Ledger.Dijkstra.Specification.Ledger txs abs
open import Ledger.Dijkstra.Specification.Rewards txs abs
open import Ledger.Dijkstra.Specification.Utxo txs abs using (totExUnits)

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 TopLevelTx
    bBodySize   : ℕ
    bBodyHash   : KeyHash
    ≡-bBodySize : bBodySize ≡ BHBody.hBbsize (BHeader.bhbody bheader)
    ≡-bBodyHash : bBodyHash ≡ BHBody.bhash (BHeader.bhbody bheader)

BBodyEnv : Type
BBodyEnv = EnactState × Acnt

BBodyState : Type
BBodyState = LedgerState × BlocksMade

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

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

  BBODY-Block-Body :
    {acnt    : Acnt}
    {ls ls'  : LedgerState}
    {b       : BlocksMade}
    {block   : Block}
    {es      : EnactState} →

    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.Dijkstra.Specification.BlockBody.html#1583}{\htmlId{1680}{\htmlClass{Bound}{\text{bhb}}}}\, \,\htmlId{1684}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.BlockBody.html#644}{\htmlId{1685}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Prelude.html#2407}{\htmlId{1692}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.BlockBody.html#1446}{\htmlId{1694}{\htmlClass{Bound}{\text{es}}}}\, \,\htmlId{1697}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.html#741}{\htmlId{1698}{\htmlClass{Field}{\text{constitution}}}}\, \,\href{Ledger.Prelude.html#2407}{\htmlId{1711}{\htmlClass{Function Operator}{\text{∣}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.BlockBody.html#1649}{\htmlId{1715}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.BlockBody.html#1446}{\htmlId{1720}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Prelude.Base.html#889}{\htmlId{1725}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Dijkstra.Specification.BlockBody.html#1348}{\htmlId{1736}{\htmlClass{Bound}{\text{acnt}}}}\, \end{pmatrix}$
     in

    ∙ block .bBodySize ≡ bhb .hBbsize
    ∙ block .bBodyHash ≡ bhb .bhash
    ∙ PParams.maxBlockExUnits pp ≥ᵉ (∑ˡ[ tx ← txs ] totExUnits tx)
    ∙ Γ ⊢ ls ⇀⦇ txs ,LEDGERS⦈ ls'
    ────────────────────────────────
    (es , acnt) ⊢ ls , b ⇀⦇ block ,BBODY⦈ (ls' , incrBlocks hk b)