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

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


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 → ℤ
calculateDepositsChange certState certState' = finalCoin - initialCoin
  where
    initialCoin : ℕ
    initialCoin = getCoin (DepositsOf (DStateOf certState))
                  + getCoin (DepositsOf (PStateOf certState))
                  + getCoin (DepositsOf (GStateOf certState))

    finalCoin : ℕ
    finalCoin = getCoin (DepositsOf (DStateOf certState'))
                + getCoin (DepositsOf (PStateOf certState'))
                + getCoin (DepositsOf (GStateOf certState'))



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 → LState → SubLevelTx → LState → Type where

  SUBLEDGER-V :
      ∙ isTopLevelValid ≡ true
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{5644}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{5651}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5311}{\htmlId{5656}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4834}{\htmlId{5667}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5358}{\htmlId{5675}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5401}{\htmlId{5693}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5448}{\htmlId{5706}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
      ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{5768}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{5774}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{5781}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8082}{\htmlId{5786}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5069}{\htmlId{5803}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#1975}{\htmlId{5809}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5069}{\htmlId{5823}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4108}{\htmlId{5829}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4973}{\htmlId{5842}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5262}{\htmlId{5852}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState₀ ⇀⦇ DCertsOf stx ,CERTS⦈ certState₁
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#6811}{\htmlId{5923}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5069}{\htmlId{5930}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{5936}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{5942}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{5949}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5161}{\htmlId{5954}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5262}{\htmlId{5964}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4936}{\htmlId{5977}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{5990}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{5994}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3148}{\htmlId{5995}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4936}{\htmlId{6005}{\htmlClass{Generalizable}{\text{certState₁}}}}\,\,\htmlId{6015}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{6125}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5161}{\htmlId{6132}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{6142}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5262}{\htmlId{6147}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5311}{\htmlId{6160}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4834}{\htmlId{6171}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5358}{\htmlId{6179}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5401}{\htmlId{6197}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5448}{\htmlId{6210}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4877}{\htmlId{6224}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4973}{\htmlId{6237}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4925}{\htmlId{6249}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4888}{\htmlId{6283}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4984}{\htmlId{6296}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4936}{\htmlId{6308}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \end{pmatrix}$

  SUBLEDGER-I :
      ∙ isTopLevelValid ≡ false
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{6380}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{6387}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5311}{\htmlId{6392}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4834}{\htmlId{6403}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5358}{\htmlId{6411}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5401}{\htmlId{6429}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5448}{\htmlId{6442}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{6545}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5161}{\htmlId{6552}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{6562}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5262}{\htmlId{6567}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5311}{\htmlId{6580}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4834}{\htmlId{6591}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5358}{\htmlId{6599}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5401}{\htmlId{6617}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5448}{\htmlId{6630}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4877}{\htmlId{6644}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4973}{\htmlId{6657}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4925}{\htmlId{6669}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4877}{\htmlId{6703}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4973}{\htmlId{6716}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4925}{\htmlId{6728}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$

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


data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState → 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 = calculateDepositsChange certState₀ certState₂
    in
      ∙ IsValidFlagOf tx ≡ true
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{7381}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5161}{\htmlId{7388}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{7398}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5262}{\htmlId{7403}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5311}{\htmlId{7416}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6998}{\htmlId{7427}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8884}{\htmlId{7435}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5020}{\htmlId{7449}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7056}{\htmlId{7454}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7133}{\htmlId{7467}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4877}{\htmlId{7481}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4973}{\htmlId{7494}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4925}{\htmlId{7506}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4888}{\htmlId{7558}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4984}{\htmlId{7571}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4936}{\htmlId{7583}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \end{pmatrix}$
      ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{7606}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{7612}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{7619}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8082}{\htmlId{7624}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5020}{\htmlId{7641}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#1975}{\htmlId{7646}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5020}{\htmlId{7660}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4108}{\htmlId{7665}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4984}{\htmlId{7678}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5262}{\htmlId{7688}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState₁ ⇀⦇ DCertsOf tx ,CERTS⦈ certState₂
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#6811}{\htmlId{7758}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5020}{\htmlId{7765}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{7770}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{7776}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{7783}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5161}{\htmlId{7788}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5262}{\htmlId{7798}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4947}{\htmlId{7811}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{7824}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{7828}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3148}{\htmlId{7829}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4947}{\htmlId{7839}{\htmlClass{Generalizable}{\text{certState₂}}}}\,\,\htmlId{7849}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{7917}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{7924}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5311}{\htmlId{7929}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6998}{\htmlId{7940}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7241}{\htmlId{7948}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7056}{\htmlId{7965}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7133}{\htmlId{7978}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{8077}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5161}{\htmlId{8084}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{8094}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5262}{\htmlId{8099}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5311}{\htmlId{8112}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4877}{\htmlId{8127}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4973}{\htmlId{8140}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4925}{\htmlId{8152}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4899}{\htmlId{8182}{\htmlClass{Generalizable}{\text{utxoState₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#3735}{\htmlId{8195}{\htmlClass{Function}{\text{rmOrphanDRepVotes}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4947}{\htmlId{8213}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4995}{\htmlId{8224}{\htmlClass{Generalizable}{\text{govState₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4947}{\htmlId{8236}{\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#5118}{\htmlId{8556}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5161}{\htmlId{8563}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{8573}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5262}{\htmlId{8578}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5311}{\htmlId{8591}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#8273}{\htmlId{8602}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8884}{\htmlId{8610}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5020}{\htmlId{8624}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#8331}{\htmlId{8629}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#8408}{\htmlId{8642}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4877}{\htmlId{8656}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4973}{\htmlId{8669}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4925}{\htmlId{8681}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4877}{\htmlId{8733}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4973}{\htmlId{8746}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4925}{\htmlId{8758}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{8781}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{8788}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5311}{\htmlId{8793}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#8273}{\htmlId{8804}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{8812}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#8331}{\htmlId{8817}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#8408}{\htmlId{8830}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁
        ────────────────────────────────
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5118}{\htmlId{8929}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5161}{\htmlId{8936}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5216}{\htmlId{8946}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5262}{\htmlId{8951}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5311}{\htmlId{8964}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4877}{\htmlId{8979}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4973}{\htmlId{8992}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4925}{\htmlId{9004}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4888}{\htmlId{9034}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4973}{\htmlId{9047}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4925}{\htmlId{9059}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$

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