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


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


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)


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


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#4408}{\htmlId{4908}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{4915}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4553}{\htmlId{4920}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4269}{\htmlId{4931}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4588}{\htmlId{4939}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4619}{\htmlId{4957}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4666}{\htmlId{4970}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$  ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState'
      ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{5032}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{5038}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{5045}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#4288}{\htmlId{5050}{\htmlClass{Function}{\text{txGovVotes}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#4105}{\htmlId{5063}{\htmlClass{Function}{\text{txWithdrawals}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#3975}{\htmlId{5079}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{5092}{\htmlClass{Generalizable}{\text{govState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4516}{\htmlId{5101}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState ⇀⦇ txCerts ,CERTS⦈ certState'
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#3972}{\htmlId{5166}{\htmlClass{Function}{\text{txId}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{5173}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{5179}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{5186}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4439}{\htmlId{5191}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4516}{\htmlId{5201}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4345}{\htmlId{5214}{\htmlClass{Generalizable}{\text{certState'}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{5227}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{5231}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#1733}{\htmlId{5232}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{5242}{\htmlClass{Generalizable}{\text{certState}}}}\,\,\htmlId{5251}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{5378}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4439}{\htmlId{5385}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{5395}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4516}{\htmlId{5400}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4553}{\htmlId{5413}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4269}{\htmlId{5424}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4588}{\htmlId{5432}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4619}{\htmlId{5450}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4666}{\htmlId{5463}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4233}{\htmlId{5477}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{5489}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{5500}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4243}{\htmlId{5533}{\htmlClass{Generalizable}{\text{utxoState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4309}{\htmlId{5546}{\htmlClass{Generalizable}{\text{govState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4345}{\htmlId{5558}{\htmlClass{Generalizable}{\text{certState'}}}}\, \end{pmatrix}$

  SUBLEDGER-I :
      ∙ isTopLevelValid ≡ false
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{5630}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{5637}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4553}{\htmlId{5642}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4269}{\htmlId{5653}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4588}{\htmlId{5661}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4619}{\htmlId{5679}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4666}{\htmlId{5692}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{5789}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4439}{\htmlId{5796}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{5806}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4516}{\htmlId{5811}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4553}{\htmlId{5824}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4269}{\htmlId{5835}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4588}{\htmlId{5843}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4619}{\htmlId{5861}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4666}{\htmlId{5874}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4233}{\htmlId{5888}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{5900}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{5911}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4233}{\htmlId{5944}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{5956}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{5967}{\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#4408}{\htmlId{6681}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4439}{\htmlId{6688}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{6698}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4516}{\htmlId{6703}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4553}{\htmlId{6716}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6413}{\htmlId{6727}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#3625}{\htmlId{6735}{\htmlClass{Field}{\text{isValid}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6232}{\htmlId{6743}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6448}{\htmlId{6748}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6540}{\htmlId{6761}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4233}{\htmlId{6775}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{6787}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{6798}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ txSubTransactions ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4243}{\htmlId{6846}{\htmlClass{Generalizable}{\text{utxoState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4309}{\htmlId{6859}{\htmlClass{Generalizable}{\text{govState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4345}{\htmlId{6871}{\htmlClass{Generalizable}{\text{certState'}}}}\, \end{pmatrix}$
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{6894}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{6901}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4553}{\htmlId{6906}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6413}{\htmlId{6917}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#3625}{\htmlId{6925}{\htmlClass{Field}{\text{isValid}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6232}{\htmlId{6933}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6448}{\htmlId{6938}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6540}{\htmlId{6951}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$  ⊢ utxoState' ⇀⦇ tx ,UTXOW⦈ utxoState''
      ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{7011}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{7017}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{7024}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#4288}{\htmlId{7029}{\htmlClass{Function}{\text{txGovVotes}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#4105}{\htmlId{7042}{\htmlClass{Function}{\text{txWithdrawals}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#3975}{\htmlId{7058}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{7071}{\htmlClass{Generalizable}{\text{govState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4516}{\htmlId{7080}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState' ⇀⦇ txCerts ,CERTS⦈ certState''
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#3972}{\htmlId{7147}{\htmlClass{Function}{\text{txId}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{7154}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{7160}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{7167}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4439}{\htmlId{7172}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4516}{\htmlId{7182}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4345}{\htmlId{7195}{\htmlClass{Generalizable}{\text{certState'}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{7208}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{7212}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#1733}{\htmlId{7213}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{7223}{\htmlClass{Generalizable}{\text{certState}}}}\,\,\htmlId{7232}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{7359}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4439}{\htmlId{7366}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{7376}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4516}{\htmlId{7381}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4553}{\htmlId{7394}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4233}{\htmlId{7409}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{7421}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{7432}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#6155}{\htmlId{7461}{\htmlClass{Generalizable}{\text{utxoState''}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6181}{\htmlId{7475}{\htmlClass{Generalizable}{\text{govState''}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6206}{\htmlId{7488}{\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#4408}{\htmlId{7849}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4439}{\htmlId{7856}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{7866}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4516}{\htmlId{7871}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4553}{\htmlId{7884}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7580}{\htmlId{7895}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#3625}{\htmlId{7903}{\htmlClass{Field}{\text{isValid}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6232}{\htmlId{7911}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7615}{\htmlId{7916}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7707}{\htmlId{7929}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4233}{\htmlId{7943}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{7955}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{7966}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ txSubTransactions  ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4233}{\htmlId{8015}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{8027}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{8038}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$
      ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{8060}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{8067}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4553}{\htmlId{8072}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7580}{\htmlId{8083}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#3625}{\htmlId{8091}{\htmlClass{Field}{\text{isValid}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#6232}{\htmlId{8099}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7615}{\htmlId{8104}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#7707}{\htmlId{8117}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState ⇀⦇ tx ,UTXOW⦈ utxoState'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4408}{\htmlId{8211}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4439}{\htmlId{8218}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4482}{\htmlId{8228}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4516}{\htmlId{8233}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4553}{\htmlId{8246}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4233}{\htmlId{8261}{\htmlClass{Generalizable}{\text{utxoState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{8273}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{8284}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#4243}{\htmlId{8313}{\htmlClass{Generalizable}{\text{utxoState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4300}{\htmlId{8326}{\htmlClass{Generalizable}{\text{govState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4335}{\htmlId{8337}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$