Skip to content

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.Conway.Specification.Enact govStructure
open import Ledger.Conway.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 Tx
open GState
open GovActionState
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    : ℙ P1Script × ℙ P2Script
    allData       : DataHash ⇀ Datum

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

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

record LState : Type where

  constructor ⟦_,_,_⟧ˡ

  field
    utxoSt     : UTxOState
    govSt      : GovState
    certState  : CertState

record HasLState {a} (A : Type a) : Type a where
  field LStateOf : A → LState
open HasLState ⦃...⦄ public

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

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

--   HasGovState-LState : HasGovState LState
--   HasGovState-LState .GovStateOf = LState.govSt

--   HasCertState-LState : HasCertState LState
--   HasCertState-LState .CertStateOf = LState.certState

--   HasDeposits-LState : HasDeposits LState
--   HasDeposits-LState .DepositsOf = DepositsOf ∘ UTxOStateOf

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

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

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

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

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

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

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

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

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

-- open CertState
-- open DState
-- open GovVotes

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

-- ## Helper Functions

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

-- 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 (gas .votes) { gvDRep = filterKeys ifDRepRegistered (gas .votes .gvDRep) } }

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

-- ## LEDGER Transition System

private variable
  Γ                     : LedgerEnv
  s s' s''              : LState
  utxoState utxoState'  : UTxOState
  utxo₀                 : UTxO
  govState govState'    : GovState
  certState certState'  : CertState
  stx                   : SubLevelTx
  slot                  : Slot
  ppolicy               : Maybe ScriptHash
  pp                    : PParams
  enactState            : EnactState
  treasury              : Treasury
  isTopLevelValid       : Bool
  allScripts         : ℙ P1Script × ℙ P2Script
  allData            : DataHash ⇀ Datum

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}/SubLedgerEnv{.AgdaDatatype}.} to UTXOW{.AgdaDatatype}/SUBUTXOW{.AgdaDatatype

  • allScripts : ℙ P1Script × ℙ P2Script 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).

  • allData : DataHash ⇀ Datumis the collection of all data relevant to the entire batch: all datums appearing in witnesses and in any (sub)transaction context (computer by getAllData).

data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LState → SubLevelTx → LState → Type where
  SUBLEDGER-V :
    let txb = stx .txBody


        open TxBody txb

    in
      ∙ isTopLevelValid ≡ true
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{6213}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{6220}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5065}{\htmlId{6225}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4781}{\htmlId{6236}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5100}{\htmlId{6244}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5131}{\htmlId{6262}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5178}{\htmlId{6275}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$  ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState'
      ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{6337}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{6343}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{6350}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#7306}{\htmlId{6355}{\htmlClass{Function}{\text{txGovVotes}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#7123}{\htmlId{6368}{\htmlClass{Function}{\text{txWithdrawals}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4405}{\htmlId{6384}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{6397}{\htmlClass{Generalizable}{\text{govState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5028}{\htmlId{6406}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState ⇀⦇ txCerts ,CERTS⦈ certState'
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#6990}{\htmlId{6471}{\htmlClass{Function}{\text{txId}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{6478}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{6484}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{6491}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4951}{\htmlId{6496}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5028}{\htmlId{6506}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4857}{\htmlId{6519}{\htmlClass{Generalizable}{\text{certState'}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6532}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6536}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2034}{\htmlId{6537}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{6547}{\htmlClass{Generalizable}{\text{certState}}}}\,\,\htmlId{6556}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{6683}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4951}{\htmlId{6690}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{6700}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5028}{\htmlId{6705}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5065}{\htmlId{6718}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4781}{\htmlId{6729}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5100}{\htmlId{6737}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5131}{\htmlId{6755}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5178}{\htmlId{6768}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4745}{\htmlId{6782}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{6794}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{6805}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4755}{\htmlId{6838}{\htmlClass{Generalizable}{\text{utxoState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4821}{\htmlId{6851}{\htmlClass{Generalizable}{\text{govState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4857}{\htmlId{6863}{\htmlClass{Generalizable}{\text{certState'}}}}\, \end{pmatrix}$

  SUBLEDGER-I :
      ∙ isTopLevelValid ≡ false
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{6935}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{6942}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5065}{\htmlId{6947}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4781}{\htmlId{6958}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5100}{\htmlId{6966}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5131}{\htmlId{6984}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5178}{\htmlId{6997}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{7094}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4951}{\htmlId{7101}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{7111}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5028}{\htmlId{7116}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5065}{\htmlId{7129}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4781}{\htmlId{7140}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5100}{\htmlId{7148}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5131}{\htmlId{7166}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5178}{\htmlId{7179}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4745}{\htmlId{7193}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{7205}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{7216}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4745}{\htmlId{7249}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{7261}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{7272}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$

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

private variable
  utxoState'' : UTxOState
  govState''  : GovState
  certState'' : CertState
  tx          : TopLevelTx

data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState → Type where
  LEDGER-V :
    let  txb = tx .txBody

         open TxBody txb

         utxo₀ = UTxOOf utxoState

         allScripts : ℙ P1Script × ℙ P2Script
         allScripts = getAllScripts tx utxo₀

         allData : DataHash ⇀ Datum
         allData = setToMap (mapˢ < hash , id > (getAllData tx utxo₀))
    in
      ∙ isValid tx ≡ true
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{8046}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4951}{\htmlId{8053}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{8063}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5028}{\htmlId{8068}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5065}{\htmlId{8081}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7778}{\htmlId{8092}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#6643}{\htmlId{8100}{\htmlClass{Field}{\text{isValid}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#7553}{\htmlId{8108}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7813}{\htmlId{8113}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7905}{\htmlId{8126}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4745}{\htmlId{8140}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{8152}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{8163}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ txSubTransactions ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4755}{\htmlId{8211}{\htmlClass{Generalizable}{\text{utxoState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4821}{\htmlId{8224}{\htmlClass{Generalizable}{\text{govState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4857}{\htmlId{8236}{\htmlClass{Generalizable}{\text{certState'}}}}\, \end{pmatrix}$
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{8259}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{8266}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5065}{\htmlId{8271}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7778}{\htmlId{8282}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#6643}{\htmlId{8290}{\htmlClass{Field}{\text{isValid}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#7553}{\htmlId{8298}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7813}{\htmlId{8303}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7905}{\htmlId{8316}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$  ⊢ utxoState' ⇀⦇ tx ,UTXOW⦈ utxoState''
      ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{8376}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{8382}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{8389}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#7306}{\htmlId{8394}{\htmlClass{Function}{\text{txGovVotes}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#7123}{\htmlId{8407}{\htmlClass{Function}{\text{txWithdrawals}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4405}{\htmlId{8423}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{8436}{\htmlClass{Generalizable}{\text{govState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5028}{\htmlId{8445}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState' ⇀⦇ txCerts ,CERTS⦈ certState''
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#6990}{\htmlId{8512}{\htmlClass{Function}{\text{txId}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{8519}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{8525}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{8532}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4951}{\htmlId{8537}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5028}{\htmlId{8547}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4857}{\htmlId{8560}{\htmlClass{Generalizable}{\text{certState'}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{8573}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{8577}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2034}{\htmlId{8578}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{8588}{\htmlClass{Generalizable}{\text{certState}}}}\,\,\htmlId{8597}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{8724}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4951}{\htmlId{8731}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{8741}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5028}{\htmlId{8746}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5065}{\htmlId{8759}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4745}{\htmlId{8774}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{8786}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{8797}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#7476}{\htmlId{8826}{\htmlClass{Generalizable}{\text{utxoState''}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7502}{\htmlId{8840}{\htmlClass{Generalizable}{\text{govState''}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7527}{\htmlId{8853}{\htmlClass{Generalizable}{\text{certState''}}}}\, \end{pmatrix}$

  LEDGER-I :
    let  txb = tx .txBody

         open TxBody txb

         utxo₀ = UTxOOf utxoState

         allScripts : ℙ P1Script × ℙ P2Script
         allScripts = getAllScripts tx utxo₀

         allData : DataHash ⇀ Datum
         allData = setToMap (mapˢ < hash , id > (getAllData tx utxo₀))
    in
      ∙ isValid tx ≡ false
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{9243}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4951}{\htmlId{9250}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{9260}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5028}{\htmlId{9265}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5065}{\htmlId{9278}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#8974}{\htmlId{9289}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#6643}{\htmlId{9297}{\htmlClass{Field}{\text{isValid}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#7553}{\htmlId{9305}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#9009}{\htmlId{9310}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#9101}{\htmlId{9323}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4745}{\htmlId{9337}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{9349}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{9360}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ txSubTransactions  ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4745}{\htmlId{9409}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{9421}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{9432}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{9454}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{9461}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5065}{\htmlId{9466}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#8974}{\htmlId{9477}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#6643}{\htmlId{9485}{\htmlClass{Field}{\text{isValid}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#7553}{\htmlId{9493}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#9009}{\htmlId{9498}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#9101}{\htmlId{9511}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState ⇀⦇ tx ,UTXOW⦈ utxoState'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4920}{\htmlId{9605}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4951}{\htmlId{9612}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4994}{\htmlId{9622}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5028}{\htmlId{9627}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5065}{\htmlId{9640}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4745}{\htmlId{9655}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{9667}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{9678}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4755}{\htmlId{9707}{\htmlClass{Generalizable}{\text{utxoState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4812}{\htmlId{9720}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4847}{\htmlId{9731}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$

-- <!--

-- pattern LEDGER-V⋯ w x y z = LEDGER-V (w , x , y , z)
-- pattern LEDGER-I⋯ y z     = LEDGER-I (y , z)
-- ```
-- -->

-- ## <span class="AgdaDatatype">LEDGERS</span> Transition System

-- ```agda
-- _⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type
-- _⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}
-- ```