Ledger¶

This module defines the ledger transition system where valid transactions transform the ledger state.

{-# OPTIONS --safe #-}

import Data.List as L

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Abstract
open import Ledger.Dijkstra.Specification.Transaction using (TransactionStructure)

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

open import Ledger.Dijkstra.Specification.Enact govStructure
open import Ledger.Dijkstra.Specification.Gov govStructure
open import Ledger.Dijkstra.Specification.Utxo txs abs
open import Ledger.Dijkstra.Specification.Utxow txs abs
open import Ledger.Dijkstra.Specification.Certs govStructure

open EnactState using (cc)

LEDGER Transition System Types¶

record SubLedgerEnv : Type where
  field
    slot             : Slot
    ppolicy          : Maybe ScriptHash
    pparams          : PParams
    enactState       : EnactState
    treasury         : Treasury
    utxo₀            : UTxO
    isTopLevelValid  : Bool
    allScripts       : ℙ Script
    accountBalances  : Rewards

record LedgerEnv : Type where
  field
    slot        : Slot
    ppolicy     : Maybe ScriptHash
    pparams     : PParams
    enactState  : EnactState
    treasury    : Treasury

instance
  unquoteDecl HasCast-LedgerEnv HasCast-SubLedgerEnv = derive-HasCast
    ((quote LedgerEnv , HasCast-LedgerEnv) ∷ (quote SubLedgerEnv , HasCast-SubLedgerEnv) ∷ [])

  HasPParams-LedgerEnv : HasPParams LedgerEnv
  HasPParams-LedgerEnv .PParamsOf = LedgerEnv.pparams

  HasEnactState-LedgerEnv : HasEnactState LedgerEnv
  HasEnactState-LedgerEnv .EnactStateOf = LedgerEnv.enactState

  HasPParams-SubLedgerEnv : HasPParams SubLedgerEnv
  HasPParams-SubLedgerEnv .PParamsOf = SubLedgerEnv.pparams

  HasEnactState-SubLedgerEnv : HasEnactState SubLedgerEnv
  HasEnactState-SubLedgerEnv .EnactStateOf = SubLedgerEnv.enactState

  HasUTxO-SubLedgerEnv : HasUTxO SubLedgerEnv
  HasUTxO-SubLedgerEnv .UTxOOf = SubLedgerEnv.utxo₀

  HasTreasury-SubLedgerEnv : HasTreasury SubLedgerEnv
  HasTreasury-SubLedgerEnv .TreasuryOf = SubLedgerEnv.treasury

  HasAccountBalances-SubLedgerEnv : HasAccountBalances SubLedgerEnv
  HasAccountBalances-SubLedgerEnv .AccountBalancesOf = SubLedgerEnv.accountBalances

record LedgerState : Type where

  constructor ⟦_,_,_⟧ˡ

  field
    utxoSt     : UTxOState
    govSt      : GovState
    certState  : CertState

record HasLedgerState {a} (A : Type a) : Type a where
  field LedgerStateOf : A → LedgerState
open HasLedgerState ⦃...⦄ public

instance
  HasUTxOState-LedgerState : HasUTxOState LedgerState
  HasUTxOState-LedgerState .UTxOStateOf = LedgerState.utxoSt

  HasUTxO-LedgerState : HasUTxO LedgerState
  HasUTxO-LedgerState .UTxOOf = UTxOOf ∘ UTxOStateOf

  HasGovState-LedgerState : HasGovState LedgerState
  HasGovState-LedgerState .GovStateOf = LedgerState.govSt

  HasCertState-LedgerState : HasCertState LedgerState
  HasCertState-LedgerState .CertStateOf = LedgerState.certState

  HasPools-LedgerState : HasPools LedgerState
  HasPools-LedgerState .PoolsOf = PoolsOf ∘ CertStateOf

  HasGState-LedgerState : HasGState LedgerState
  HasGState-LedgerState .GStateOf = GStateOf ∘ CertStateOf

  HasDState-LedgerState : HasDState LedgerState
  HasDState-LedgerState .DStateOf = DStateOf ∘ CertStateOf

  HasPState-LedgerState : HasPState LedgerState
  HasPState-LedgerState .PStateOf = PStateOf ∘ CertStateOf

  HasVoteDelegs-LedgerState : HasVoteDelegs LedgerState
  HasVoteDelegs-LedgerState .VoteDelegsOf = VoteDelegsOf ∘ DStateOf ∘ CertStateOf

  HasDonations-LedgerState : HasDonations LedgerState
  HasDonations-LedgerState .DonationsOf = DonationsOf ∘ UTxOStateOf

  HasFees-LedgerState : HasFees LedgerState
  HasFees-LedgerState .FeesOf = FeesOf ∘ UTxOStateOf

  HasCCHotKeys-LedgerState : HasCCHotKeys LedgerState
  HasCCHotKeys-LedgerState .CCHotKeysOf = CCHotKeysOf ∘ GStateOf

  HasDReps-LedgerState : HasDReps LedgerState
  HasDReps-LedgerState .DRepsOf = DRepsOf ∘ CertStateOf

  unquoteDecl HasCast-LedgerState = derive-HasCast
    ((quote LedgerState , HasCast-LedgerState) ∷ [])

Helper Functions¶

txgov : ∀ {ℓ} → TxBody ℓ → List (GovVote ⊎ GovProposal)
txgov txb = map inj₂ txGovProposals ++ map inj₁ txGovVotes
  where open TxBody txb

GovProposals+Votes : ∀ {ℓ} → Tx ℓ → List (GovVote ⊎ GovProposal)
GovProposals+Votes tx = map inj₂ (ListOfGovProposalsOf tx) ++ map inj₁ (ListOfGovVotesOf tx)

rmOrphanDRepVotes : CertState → GovState → GovState
rmOrphanDRepVotes cs govSt = L.map (map₂ go) govSt
  where
   ifDRepRegistered : Credential → Type
   ifDRepRegistered c = c ∈ dom (DRepsOf cs)

   go : GovActionState → GovActionState
   go gas = record gas { votes = record (GovVotesOf gas) { gvDRep = filterKeys ifDRepRegistered (GovVotes.gvDRep (GovVotesOf gas)) } }

allColdCreds : GovState → EnactState → ℙ Credential
allColdCreds govSt es =
  ccCreds (es .cc) ∪ concatMapˢ (λ (_ , st) → proposedCC (GovActionOf st)) (fromList govSt)

calculateDepositsChange : CertState → CertState → CertState → DepositsChange
calculateDepositsChange certState₀ certState₁ certState₂
  = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5948}{\htmlId{5456}{\htmlClass{Function}{\text{coinChangeTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5891}{\htmlId{5472}{\htmlClass{Function}{\text{coinChangeSub}}}}\, \end{pmatrix}$
  where
    coinFromDeposit : CertState → Coin
    coinFromDeposit certState =
      getCoin (DepositsOf (DStateOf certState))
      + getCoin (DepositsOf (PStateOf certState))
      + getCoin (DepositsOf (GStateOf certState))

    coin₀ : Coin
    coin₀ = coinFromDeposit certState₀

    coin₁ : Coin
    coin₁ = coinFromDeposit certState₁

    coin₂ : Coin
    coin₂ = coinFromDeposit certState₂

    coinChangeSub : ℤ
    coinChangeSub = coin₁ - coin₀

    coinChangeTop : ℤ
    coinChangeTop = coin₂ - coin₁

LEDGER Transition System¶

private variable
  utxo₀                             : UTxO
  utxoState₀ utxoState₁ utxoState₂  : UTxOState
  certState₀ certState₁ certState₂  : CertState
  govState₀  govState₁  govState₂   : GovState
  tx                                : TopLevelTx
  stx                               : SubLevelTx
  slot                              : Slot
  ppolicy                           : Maybe ScriptHash
  pp                                : PParams
  enactState                        : EnactState
  treasury                          : Treasury
  isTopLevelValid                   : Bool
  allScripts                        : ℙ Script
  accountBalances                   : Rewards

New in Dijkstra¶

In Dijkstra we compute the set of "global" scripts and data once at the top-level in the LEDGER{.AgdaDatatype} rule. This is threaded through SUBLEDGER via UTxOEnv{.AgdaDatatype}/SubUTxOEnv{.AgdaDatatype}.} to UTXOW{.AgdaDatatype}/SUBUTXOW{.AgdaDatatype

allScripts : ℙ Script is the union of all scripts relevant to the entire batch: scripts referenced/witnessed by the top-level transaction plus scripts referenced/witnessed by every subtransaction (computed by getAllScripts).

Design Rationale for Ledger Rule Premises¶

Batch-scoped phase-2 context.

We compute allScripts once, from the pre-batch UTxO snapshot and the full batch (top-level transaction and all subtransactions). This ensures a shared, batch-scoped pool of scripts for phase-2 validation.

Subtransactions are conditional on top-level validity.
If IsValidFlagOf txTop ≡ true, then each subtransaction parametrizes its own UTXOW/CERTS/GOVS relation and the resulting (codomain) states are carried forward (via SUBLEDGERS).
If IsValidFlagOf txTop ≡ false, then SUBLEDGERS is the identity relation (no subtransaction effects are applied).
Connecting top-level CERTS and GOVS relations relative to UTXOW.

We check top-level CERTS and GOVS relations before top-level UTXOW because:

CERTS tracks deposit updates (now included in CertState),
UTXO accounting needs the net deposit change of the whole batch in the UTxOEnv (used in newDepositsBatch / depositRefundsBatch in the Utxo.Accounting module).
CertState and GovState Dependencies.
Top-level CERTS relates the post-SUBLEDGERS CertState (which reflects subtransaction certificates) to the final CertState.
Top-level GOVS relates the post-SUBLEDGERS GovState (which relfects proposals/votes of subtransactions) to the final GovState, and is parameterized by the final CertState (so it sees the final registered DRep set after certificates).
Orphan DRep votes are removed using the final (post-CERTS) CertState.
allColdCreds uses the final GovState

The CertEnv assumed in the CERTS relation includes allColdCreds govState₁ enactState to so that CC hot key registration can account for both enacted CC credentials and any newly proposed CC actions that appear in the final (post-subtransaction processing) GovState.

data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx → LedgerState → Type where

  SUBLEDGER-V :
      ∙ isTopLevelValid ≡ true
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{9887}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{9894}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6577}{\htmlId{9899}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6100}{\htmlId{9910}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6624}{\htmlId{9918}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6667}{\htmlId{9936}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6714}{\htmlId{9949}{\htmlClass{Generalizable}{\text{accountBalances}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
      ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{10019}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{10025}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{10032}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12609}{\htmlId{10037}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6335}{\htmlId{10054}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#3223}{\htmlId{10060}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6335}{\htmlId{10074}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5147}{\htmlId{10080}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6239}{\htmlId{10093}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6528}{\htmlId{10103}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13416}{\htmlId{10116}{\htmlClass{Field}{\text{DirectDepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6335}{\htmlId{10133}{\htmlClass{Generalizable}{\text{stx}}}}\, \end{pmatrix}$ ⊢ certState₀ ⇀⦇ DCertsOf stx ,CERTS⦈ certState₁
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11338}{\htmlId{10197}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6335}{\htmlId{10204}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{10210}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{10216}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{10223}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6427}{\htmlId{10228}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6528}{\htmlId{10238}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6202}{\htmlId{10251}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{10264}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{10268}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{10269}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6202}{\htmlId{10279}{\htmlClass{Generalizable}{\text{certState₁}}}}\,\,\htmlId{10289}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{10399}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6427}{\htmlId{10406}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{10416}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6528}{\htmlId{10421}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6577}{\htmlId{10434}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6100}{\htmlId{10445}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6624}{\htmlId{10453}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6667}{\htmlId{10471}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6714}{\htmlId{10484}{\htmlClass{Generalizable}{\text{accountBalances}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6143}{\htmlId{10506}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6239}{\htmlId{10519}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{10531}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6154}{\htmlId{10565}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6250}{\htmlId{10578}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6202}{\htmlId{10590}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \end{pmatrix}$

  SUBLEDGER-I :
      ∙ isTopLevelValid ≡ false
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{10662}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{10669}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6577}{\htmlId{10674}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6100}{\htmlId{10685}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6624}{\htmlId{10693}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6667}{\htmlId{10711}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6714}{\htmlId{10724}{\htmlClass{Generalizable}{\text{accountBalances}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{10835}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6427}{\htmlId{10842}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{10852}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6528}{\htmlId{10857}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6577}{\htmlId{10870}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6100}{\htmlId{10881}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6624}{\htmlId{10889}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6667}{\htmlId{10907}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6714}{\htmlId{10920}{\htmlClass{Generalizable}{\text{accountBalances}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6143}{\htmlId{10942}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6239}{\htmlId{10955}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{10967}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6143}{\htmlId{11001}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6239}{\htmlId{11014}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{11026}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$

_⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LedgerState → List SubLevelTx → LedgerState → Type
_⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_}


data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → LedgerState → Type where

  LEDGER-V :
    let  utxo₀ : UTxO
         utxo₀ = UTxOOf utxoState₀

         allScripts : ℙ Script
         allScripts = getAllScripts tx utxo₀

         depositsChange : DepositsChange
         depositsChange = calculateDepositsChange certState₀ certState₁ certState₂
    in
      ∙ IsValidFlagOf tx ≡ true
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{11615}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6427}{\htmlId{11622}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{11632}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6528}{\htmlId{11637}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6577}{\htmlId{11650}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#11316}{\htmlId{11661}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13720}{\htmlId{11669}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6286}{\htmlId{11683}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#11374}{\htmlId{11688}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{11701}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{11711}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6143}{\htmlId{11728}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6239}{\htmlId{11741}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{11753}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6154}{\htmlId{11805}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6250}{\htmlId{11818}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6202}{\htmlId{11830}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \end{pmatrix}$
      ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{11853}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{11859}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{11866}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12609}{\htmlId{11871}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6286}{\htmlId{11888}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#3223}{\htmlId{11893}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6286}{\htmlId{11907}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5147}{\htmlId{11912}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6250}{\htmlId{11925}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6528}{\htmlId{11935}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13416}{\htmlId{11948}{\htmlClass{Field}{\text{DirectDepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6286}{\htmlId{11965}{\htmlClass{Generalizable}{\text{tx}}}}\, \end{pmatrix}$ ⊢ certState₁ ⇀⦇ DCertsOf tx ,CERTS⦈ certState₂
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11338}{\htmlId{12027}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6286}{\htmlId{12034}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{12039}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{12045}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{12052}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6427}{\htmlId{12057}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6528}{\htmlId{12067}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6213}{\htmlId{12080}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{12093}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{12097}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{12098}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6213}{\htmlId{12108}{\htmlClass{Generalizable}{\text{certState₂}}}}\,\,\htmlId{12118}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{12186}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{12193}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6577}{\htmlId{12198}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#11316}{\htmlId{12209}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#11451}{\htmlId{12217}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#11374}{\htmlId{12234}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{12247}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{12257}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{12359}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6427}{\htmlId{12366}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{12376}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6528}{\htmlId{12381}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6577}{\htmlId{12394}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6143}{\htmlId{12409}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6239}{\htmlId{12422}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{12434}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6165}{\htmlId{12464}{\htmlClass{Generalizable}{\text{utxoState₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4774}{\htmlId{12477}{\htmlClass{Function}{\text{rmOrphanDRepVotes}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6213}{\htmlId{12495}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6261}{\htmlId{12506}{\htmlClass{Generalizable}{\text{govState₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6213}{\htmlId{12518}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \end{pmatrix}$

  LEDGER-I :
    let  utxo₀ : UTxO
         utxo₀ = UTxOOf utxoState₀

         allScripts : ℙ Script
         allScripts = getAllScripts tx utxo₀
    in
      ∙ IsValidFlagOf tx ≡ false
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{12729}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6427}{\htmlId{12736}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{12746}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6528}{\htmlId{12751}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6577}{\htmlId{12764}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12554}{\htmlId{12775}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13720}{\htmlId{12783}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6286}{\htmlId{12797}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12612}{\htmlId{12802}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{12815}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{12825}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6143}{\htmlId{12842}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6239}{\htmlId{12855}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{12867}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6143}{\htmlId{12919}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6239}{\htmlId{12932}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{12944}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{12967}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{12974}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6577}{\htmlId{12979}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12554}{\htmlId{12990}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \begin{pmatrix} \,\href{Data.Integer.Base.html#1545}{\htmlId{13000}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{13005}{\htmlClass{Function}{\text{0ℤ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12612}{\htmlId{13012}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{13025}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{13035}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6384}{\htmlId{13137}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6427}{\htmlId{13144}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6482}{\htmlId{13154}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6528}{\htmlId{13159}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6577}{\htmlId{13172}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6143}{\htmlId{13187}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6239}{\htmlId{13200}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{13212}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6154}{\htmlId{13242}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6239}{\htmlId{13255}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6191}{\htmlId{13267}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$

_⊢_⇀⦇_,LEDGERS⦈_ : LedgerEnv → LedgerState → List TopLevelTx → LedgerState → Type
_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}