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


record SubLedgerEnv : Type where
  field
    slot             : Slot
    ppolicy          : Maybe ScriptHash
    pparams          : PParams
    enactState       : EnactState
    treasury         : Treasury
    utxo₀            : UTxO
    isTopLevelValid  : Bool
    allScripts       : ℙ Script
    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

  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


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) ∷ [])


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#5376}{\htmlId{4884}{\htmlClass{Function}{\text{coinChangeTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5319}{\htmlId{4900}{\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₁


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
  allData                           : DataHash ⇀ Datum


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

  SUBLEDGER-V :
      ∙ isTopLevelValid ≡ true
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{6269}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{6276}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5926}{\htmlId{6281}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5449}{\htmlId{6292}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5973}{\htmlId{6300}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6016}{\htmlId{6318}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6063}{\htmlId{6331}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
      ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{6393}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{6399}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{6406}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8533}{\htmlId{6411}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5684}{\htmlId{6428}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#1975}{\htmlId{6434}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5684}{\htmlId{6448}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4575}{\htmlId{6454}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5588}{\htmlId{6467}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5877}{\htmlId{6477}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState₀ ⇀⦇ DCertsOf stx ,CERTS⦈ certState₁
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#7262}{\htmlId{6548}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5684}{\htmlId{6555}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{6561}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{6567}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{6574}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5776}{\htmlId{6579}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5877}{\htmlId{6589}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5551}{\htmlId{6602}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6615}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6619}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3152}{\htmlId{6620}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5551}{\htmlId{6630}{\htmlClass{Generalizable}{\text{certState₁}}}}\,\,\htmlId{6640}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{6750}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5776}{\htmlId{6757}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{6767}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5877}{\htmlId{6772}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5926}{\htmlId{6785}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5449}{\htmlId{6796}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5973}{\htmlId{6804}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6016}{\htmlId{6822}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6063}{\htmlId{6835}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5492}{\htmlId{6849}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5588}{\htmlId{6862}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5540}{\htmlId{6874}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5503}{\htmlId{6908}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5599}{\htmlId{6921}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5551}{\htmlId{6933}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \end{pmatrix}$

  SUBLEDGER-I :
      ∙ isTopLevelValid ≡ false
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{7005}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{7012}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5926}{\htmlId{7017}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5449}{\htmlId{7028}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5973}{\htmlId{7036}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6016}{\htmlId{7054}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6063}{\htmlId{7067}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{7170}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5776}{\htmlId{7177}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{7187}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5877}{\htmlId{7192}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5926}{\htmlId{7205}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5449}{\htmlId{7216}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5973}{\htmlId{7224}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6016}{\htmlId{7242}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6063}{\htmlId{7255}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5492}{\htmlId{7269}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5588}{\htmlId{7282}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5540}{\htmlId{7294}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5492}{\htmlId{7328}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5588}{\htmlId{7341}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5540}{\htmlId{7353}{\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₀

         allData : DataHash ⇀ Datum
         allData = setToMap (mapˢ < hash , id > (getAllData tx utxo₀))

         depositsChange : DepositsChange
         depositsChange = calculateDepositsChange certState₀ certState₁ certState₂
    in
      ∙ IsValidFlagOf tx ≡ true
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{8050}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5776}{\htmlId{8057}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{8067}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5877}{\htmlId{8072}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5926}{\htmlId{8085}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7643}{\htmlId{8096}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#9658}{\htmlId{8104}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5635}{\htmlId{8118}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7701}{\htmlId{8123}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7778}{\htmlId{8136}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5492}{\htmlId{8150}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5588}{\htmlId{8163}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5540}{\htmlId{8175}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5503}{\htmlId{8227}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5599}{\htmlId{8240}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5551}{\htmlId{8252}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \end{pmatrix}$
      ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{8275}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{8281}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{8288}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8533}{\htmlId{8293}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5635}{\htmlId{8310}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#1975}{\htmlId{8315}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5635}{\htmlId{8329}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4575}{\htmlId{8334}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5599}{\htmlId{8347}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5877}{\htmlId{8357}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState₁ ⇀⦇ DCertsOf tx ,CERTS⦈ certState₂
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#7262}{\htmlId{8427}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5635}{\htmlId{8434}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{8439}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{8445}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{8452}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5776}{\htmlId{8457}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5877}{\htmlId{8467}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5562}{\htmlId{8480}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{8493}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{8497}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3152}{\htmlId{8498}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5562}{\htmlId{8508}{\htmlClass{Generalizable}{\text{certState₂}}}}\,\,\htmlId{8518}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{8586}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{8593}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5926}{\htmlId{8598}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7643}{\htmlId{8609}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7886}{\htmlId{8617}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7701}{\htmlId{8634}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7778}{\htmlId{8647}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{8746}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5776}{\htmlId{8753}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{8763}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5877}{\htmlId{8768}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5926}{\htmlId{8781}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5492}{\htmlId{8796}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5588}{\htmlId{8809}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5540}{\htmlId{8821}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5514}{\htmlId{8851}{\htmlClass{Generalizable}{\text{utxoState₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4202}{\htmlId{8864}{\htmlClass{Function}{\text{rmOrphanDRepVotes}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5562}{\htmlId{8882}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5610}{\htmlId{8893}{\htmlClass{Generalizable}{\text{govState₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5562}{\htmlId{8905}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \end{pmatrix}$


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

         allScripts : ℙ Script
         allScripts = getAllScripts tx utxo₀

         allData : DataHash ⇀ Datum
         allData = setToMap (mapˢ < hash , id > (getAllData tx utxo₀))
    in
      ∙ IsValidFlagOf tx ≡ false
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{9225}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5776}{\htmlId{9232}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{9242}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5877}{\htmlId{9247}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5926}{\htmlId{9260}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#8942}{\htmlId{9271}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#9658}{\htmlId{9279}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5635}{\htmlId{9293}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#9000}{\htmlId{9298}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#9077}{\htmlId{9311}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5492}{\htmlId{9325}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5588}{\htmlId{9338}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5540}{\htmlId{9350}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5492}{\htmlId{9402}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5588}{\htmlId{9415}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5540}{\htmlId{9427}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{9450}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{9457}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5926}{\htmlId{9462}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#8942}{\htmlId{9473}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \begin{pmatrix} \,\href{Data.Integer.Base.html#1545}{\htmlId{9483}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{9488}{\htmlClass{Function}{\text{0ℤ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#9000}{\htmlId{9495}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#9077}{\htmlId{9508}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5733}{\htmlId{9607}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5776}{\htmlId{9614}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5831}{\htmlId{9624}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5877}{\htmlId{9629}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5926}{\htmlId{9642}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5492}{\htmlId{9657}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5588}{\htmlId{9670}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5540}{\htmlId{9682}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5503}{\htmlId{9712}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5588}{\htmlId{9725}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5540}{\htmlId{9737}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$

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