Blockchain Layer
This section is part of the
Ledger.Conway.Specification.Chain
module of the formal ledger
specification
{-# OPTIONS --safe #-}
open import Ledger.Conway.Specification.Transaction
open import Ledger.Conway.Specification.Abstract
module Ledger.Conway.Specification.Chain
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where
open import Ledger.Conway.Specification.BlockBody txs abs public
open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Epoch txs abs
open import Ledger.Conway.Specification.Gov txs
open import Ledger.Conway.Specification.Ledger txs abs
open import Ledger.Prelude; open Equivalence
open import Ledger.Conway.Specification.Ratify txs
open import Ledger.Conway.Specification.RewardUpdate txs abs
open import Ledger.Conway.Specification.Utxo txs abs
open import Algebra
open import Data.Nat.Properties using (+-0-monoid)
Definitions CHAIN transition system
record ChainState : Type where
field
newEpochState : NewEpochState
instance
HasNewEpochState-ChainState : HasNewEpochState ChainState
HasNewEpochState-ChainState .NewEpochStateOf = ChainState.newEpochState
HasLastEpoch-ChainState : HasLastEpoch ChainState
HasLastEpoch-ChainState .LastEpochOf = LastEpochOf ∘ NewEpochStateOf
HasEpochState-ChainState : HasEpochState ChainState
HasEpochState-ChainState .EpochStateOf = EpochStateOf ∘ NewEpochStateOf
HasEnactState-ChainState : HasEnactState ChainState
HasEnactState-ChainState .EnactStateOf = EnactStateOf ∘ EpochStateOf
HasLState-ChainState : HasLState ChainState
HasLState-ChainState .LStateOf = LStateOf ∘ EpochStateOf
HasUTxOState-ChainState : HasUTxOState ChainState
HasUTxOState-ChainState .UTxOStateOf = UTxOStateOf ∘ LStateOf
HasCertState-ChainState : HasCertState ChainState
HasCertState-ChainState .CertStateOf = CertStateOf ∘ LStateOf
HasDeposits-ChainState : HasDeposits ChainState
HasDeposits-ChainState .DepositsOf = DepositsOf ∘ UTxOStateOf
HasRewards-ChainState : HasRewards ChainState
HasRewards-ChainState .RewardsOf = RewardsOf ∘ CertStateOf
HasPParams-ChainState : HasPParams ChainState
HasPParams-ChainState .PParamsOf = PParamsOf ∘ EnactStateOf
totalRefScriptsSize : LState → List Tx → ℕ
totalRefScriptsSize lst txs = sum $ map (refScriptsSize utxo) txs
where open UTxOState (LState.utxoSt lst)
private variable
ls' : LState
data
Type of the CHAIN transition system
where
CHAIN transition system