{-# 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


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)


BBodyEnv : Type
BBodyEnv = EnactState × Acnt

BBodyState : Type
BBodyState = LState × BlocksMade

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

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#1388}{\htmlId{1485}{\htmlClass{Bound}{\text{bhb}}}}\, \,\htmlId{1489}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.BlockBody.html#560}{\htmlId{1490}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Prelude.html#2302}{\htmlId{1497}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.BlockBody.html#1270}{\htmlId{1499}{\htmlClass{Bound}{\text{es}}}}\, \,\htmlId{1502}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Enact.html#553}{\htmlId{1503}{\htmlClass{Field}{\text{constitution}}}}\, \,\href{Ledger.Prelude.html#2302}{\htmlId{1516}{\htmlClass{Function Operator}{\text{∣}}}}\, \\ \,\href{Ledger.Conway.Specification.BlockBody.html#1454}{\htmlId{1520}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.BlockBody.html#1270}{\htmlId{1525}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Prelude.Base.html#889}{\htmlId{1530}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Conway.Specification.BlockBody.html#1250}{\htmlId{1541}{\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)