{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Transaction
open import Ledger.Dijkstra.Specification.Abstract
import Ledger.Dijkstra.Specification.Certs

module Ledger.Dijkstra.Specification.Ledger.Properties.Computational
  (txs : _) (open TransactionStructure txs) (open Ledger.Dijkstra.Specification.Certs govStructure)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Certs.Properties.Computational govStructure
open import Ledger.Dijkstra.Specification.Gov govStructure
open import Ledger.Dijkstra.Specification.Gov.Properties.Computational txs
open import Ledger.Dijkstra.Specification.Ledger txs abs
open import Ledger.Dijkstra.Specification.Utxo txs abs
open import Ledger.Dijkstra.Specification.Utxow txs abs
open import Ledger.Dijkstra.Specification.Utxow.Properties.Computational txs abs

open import Data.Bool.Properties using (¬-not)

instance
  _ = Monad-ComputationResult

-- When isTopLevelValid ≡ false, SUBUTXO is a UTxO no-op,
-- so SUBUTXOW leaves the UTxOState unchanged.
private
  SUBUTXOW-noop
    : ∀ {Γ : SubUTxOEnv} {s s' : UTxOState} {stx : SubLevelTx}
    → IsTopLevelValidFlagOf Γ ≡ false
    → Γ ⊢ s ⇀⦇ stx ,SUBUTXOW⦈ s'
    → s' ≡ s
  SUBUTXOW-noop isI (SUBUTXOW (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , SUBUTXO _)) rewrite isI = refl
  -- After `rewrite isI`, `IsTopLevelValidFlagOf Γ` reduces to `false`,
  -- so the SUBUTXO post-state index reduces to `⟦ UTxOOf s , FeesOf s , DonationsOf s ⟧`
  -- which is s by eta-expansion of the UTxOState record, giving refl.

-- When isTopLevelValid ≡ false, a single SUBLEDGER step is a no-op.
-- SUBLEDGER-V is impossible (its first premise is isTopLevelValid ≡ true).
  SUBLEDGER-step-noop
    : ∀ {Γ : SubLedgerEnv} {s s' : LedgerState} {stx : SubLevelTx}
    → Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s'
    → SubLedgerEnv.isTopLevelValid Γ ≡ false
    → s' ≡ s
  SUBLEDGER-step-noop (SUBLEDGER-I _)         _   = refl
  SUBLEDGER-step-noop (SUBLEDGER-V (isV , _)) isI =
    ⊥-elim (case trans (sym isV) isI of λ ())

-- The reflexive-transitive closure of no-ops is a no-op.
  SUBLEDGERS-noop
    : ∀ {Γ : SubLedgerEnv} {s s' : LedgerState} {stxs : List SubLevelTx}
    → SubLedgerEnv.isTopLevelValid Γ ≡ false
    → Γ ⊢ s ⇀⦇ stxs ,SUBLEDGERS⦈ s'
    → s' ≡ s
  SUBLEDGERS-noop _   (BS-base Id-nop)   = refl
  SUBLEDGERS-noop isI (BS-ind step rest) =
    trans (SUBLEDGERS-noop isI rest) (SUBLEDGER-step-noop step isI)

instance


  Computational-SUBLEDGER : Computational _⊢_⇀⦇_,SUBLEDGER⦈_ String


  Computational-SUBLEDGER = MkComputational computeProof completeness
    where
    open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete)

    computeSubutxow = comp {STS = _⊢_⇀⦇_,SUBUTXOW⦈_}
    computeCerts    = comp {STS = _⊢_⇀⦇_,CERTS⦈_}
    computeGov      = comp {STS = _⊢_⇀⦇_,GOVS⦈_}

    -- Helper env constructors (avoid `let ... in with ...` parse issues)
    subUtxoΓ : SubLedgerEnv → SubUTxOEnv
    subUtxoΓ Γ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#736}{\htmlId{3032}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#804}{\htmlId{3039}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#869}{\htmlId{3049}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#901}{\htmlId{3060}{\htmlClass{Field}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#929}{\htmlId{3068}{\htmlClass{Field}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#957}{\htmlId{3086}{\htmlClass{Field}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#989}{\htmlId{3099}{\htmlClass{Field}{\text{allData}}}}\, \end{pmatrix}$
      where open SubLedgerEnv Γ

    certΓ : SubLedgerEnv → LedgerState → SubLevelTx → CertEnv
    certΓ Γ s stx = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{3226}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#736}{\htmlId{3232}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#804}{\htmlId{3239}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8418}{\htmlId{3249}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3218}{\htmlId{3266}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#1975}{\htmlId{3272}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3218}{\htmlId{3286}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4575}{\htmlId{3292}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\htmlId{3305}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#2155}{\htmlId{3306}{\htmlClass{Field}{\text{LedgerState.govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3216}{\htmlId{3324}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{3325}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#835}{\htmlId{3327}{\htmlClass{Function}{\text{enactState}}}}\, \end{pmatrix}$
      where open SubLedgerEnv Γ

    govΓ : SubLedgerEnv → SubLevelTx → CertState → GovEnv
    govΓ Γ stx certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#7147}{\htmlId{3457}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3442}{\htmlId{3464}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{3470}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#736}{\htmlId{3476}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#804}{\htmlId{3483}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#764}{\htmlId{3493}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#835}{\htmlId{3503}{\htmlClass{Function}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3446}{\htmlId{3516}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{3525}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{3529}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3206}{\htmlId{3530}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3446}{\htmlId{3540}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{3546}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
      where open SubLedgerEnv Γ


    computeProof : (Γ : SubLedgerEnv) (s : LedgerState) (stx : SubLevelTx)
      → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s')


    computeProof Γ s stx with SubLedgerEnv.isTopLevelValid Γ ≟ true
    ... | yes isV =
      let open SubLedgerEnv Γ
          open LedgerState s
          subUtxoΓ : SubUTxOEnv
          subUtxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#736}{\htmlId{3934}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#804}{\htmlId{3941}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#869}{\htmlId{3951}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#901}{\htmlId{3962}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#929}{\htmlId{3970}{\htmlClass{Function}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#957}{\htmlId{3988}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#989}{\htmlId{4001}{\htmlClass{Function}{\text{allData}}}}\, \end{pmatrix}$
          certΓ : CertEnv
          certΓ = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{4057}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#736}{\htmlId{4063}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#804}{\htmlId{4070}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8418}{\htmlId{4080}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\htmlId{4097}{\htmlClass{Bound}{\text{stx}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#1975}{\htmlId{4103}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\htmlId{4117}{\htmlClass{Bound}{\text{stx}}}\,
                  \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4575}{\htmlId{4141}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2155}{\htmlId{4154}{\htmlClass{Function}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#835}{\htmlId{4160}{\htmlClass{Function}{\text{enactState}}}}\, \end{pmatrix}$
      in
      computeSubutxow subUtxoΓ utxoSt stx >>= λ where
        (utxoSt' , utxoStep) →
          computeCerts certΓ certState (DCertsOf stx) >>= λ where
            (certSt' , certStep) →
              let govΓ : GovEnv
                  govΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#7147}{\htmlId{4427}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\htmlId{4434}{\htmlClass{Bound}{\text{stx}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{4440}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#736}{\htmlId{4446}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#804}{\htmlId{4453}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#764}{\htmlId{4463}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#835}{\htmlId{4473}{\htmlClass{Function}{\text{enactState}}}}\,
                        \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4346}{\htmlId{4510}{\htmlClass{Bound}{\text{certSt'}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{4520}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{4524}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3206}{\htmlId{4525}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4346}{\htmlId{4535}{\htmlClass{Bound}{\text{certSt'}}}}\,\,\htmlId{4542}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
              in
              computeGov govΓ govSt (GovProposals+Votes stx) >>= λ where
                (govSt' , govStep) →
                  success ( $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4245}{\htmlId{4703}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4653}{\htmlId{4713}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4346}{\htmlId{4722}{\htmlClass{Bound}{\text{certSt'}}}}\, \end{pmatrix}$
                          , SUBLEDGER-V (isV , utxoStep , certStep , govStep))

    ... | no ¬isV =
      let open SubLedgerEnv Γ; open LedgerState s
          isI : isTopLevelValid ≡ false
          isI = ¬-not ¬isV
          subUtxoΓ : SubUTxOEnv
          subUtxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#736}{\htmlId{5005}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#804}{\htmlId{5012}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#869}{\htmlId{5022}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#901}{\htmlId{5033}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#929}{\htmlId{5041}{\htmlClass{Function}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#957}{\htmlId{5059}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#989}{\htmlId{5072}{\htmlClass{Function}{\text{allData}}}}\, \end{pmatrix}$
      in case computeSubutxow subUtxoΓ utxoSt stx of λ where
        (failure e) → failure e
        (success (utxoSt' , utxoStep)) →
          success ( $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#2128}{\htmlId{5238}{\htmlClass{Function}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2155}{\htmlId{5247}{\htmlClass{Function}{\text{govSt}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2181}{\htmlId{5255}{\htmlClass{Function}{\text{certState}}}}\, \end{pmatrix}$
                  , SUBLEDGER-I ( isI , subst (subUtxoΓ ⊢ utxoSt ⇀⦇ stx ,SUBUTXOW⦈_) (SUBUTXOW-noop isI utxoStep) utxoStep ))



    completeness : (Γ : SubLedgerEnv) (s : LedgerState) (stx : SubLevelTx) (s' : LedgerState)
      → Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s' → (proj₁ <$> computeProof Γ s stx) ≡ success s'


    completeness Γ s stx s'
      (SUBLEDGER-V {utxoState₁ = utxoSt₁} {certState₁ = certSt₁} {govState₁ = govSt₁}
        (isV , utxoStep , certStep , govStep))
      with SubLedgerEnv.isTopLevelValid Γ ≟ true
    ... | no ¬isV = contradiction isV ¬isV
    ... | yes refl
      with computeSubutxow (subUtxoΓ Γ) (LedgerState.utxoSt s) stx
         | complete {STS = _⊢_⇀⦇_,SUBUTXOW⦈_}
             (subUtxoΓ Γ) (LedgerState.utxoSt s) stx utxoSt₁ utxoStep
    ... | success (utxoSt₁ , _) | refl
      with computeCerts (certΓ Γ s stx) (LedgerState.certState s) (DCertsOf stx)
         | complete {STS = _⊢_⇀⦇_,CERTS⦈_}
             (certΓ Γ s stx) (LedgerState.certState s) (DCertsOf stx) certSt₁ certStep
    ... | success (certSt₁ , _) | refl
      with computeGov (govΓ Γ stx certSt₁) (LedgerState.govSt s) (GovProposals+Votes stx)
         | complete {STS = _⊢_⇀⦇_,GOVS⦈_}
             (govΓ Γ stx certSt₁) (LedgerState.govSt s) (GovProposals+Votes stx) govSt₁ govStep
    ... | success (govSt₁ , _) | refl = refl

    completeness Γ s stx s' (SUBLEDGER-I (isI , utxoStep))
      with SubLedgerEnv.isTopLevelValid Γ ≟ true
    ... | yes isV = case trans (sym isV) isI of λ ()
    ... | no ¬isV
      with computeSubutxow (subUtxoΓ Γ) (LedgerState.utxoSt s) stx
         | complete {STS = _⊢_⇀⦇_,SUBUTXOW⦈_}
             (subUtxoΓ Γ) (LedgerState.utxoSt s) stx (LedgerState.utxoSt s) utxoStep
    ... | success _ | refl = refl

Computational-SUBLEDGERS : Computational _⊢_⇀⦇_,SUBLEDGERS⦈_ String
Computational-SUBLEDGERS = it

instance


  Computational-LEDGER : Computational _⊢_⇀⦇_,LEDGER⦈_ String


  Computational-LEDGER = MkComputational computeProof completeness
    where
    open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete)
    computeSubledgers = comp {STS = _⊢_⇀⦇_,SUBLEDGERS⦈_}
    computeCerts      = comp {STS = _⊢_⇀⦇_,CERTS⦈_}
    computeGov        = comp {STS = _⊢_⇀⦇_,GOVS⦈_}
    computeUtxow      = comp {STS = _⊢_⇀⦇_,UTXOW⦈_}

    -- Helper builders (avoid `let ... in with ...`)
    utxo₀Of : LedgerState → UTxO
    utxo₀Of s = UTxOOf (LedgerState.utxoSt s)

    allScriptsOf : TopLevelTx → LedgerState → ℙ Script
    allScriptsOf tx s = getAllScripts tx (utxo₀Of s)

    allDataOf : TopLevelTx → LedgerState → DataHash ⇀ Datum
    allDataOf tx s = setToMap (mapˢ < hash , id > (getAllData tx))

    subΓOf : LedgerEnv → LedgerState → TopLevelTx → SubLedgerEnv
    subΓOf Γ s tx =
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{8021}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8004}{\htmlId{8036}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1091}{\htmlId{8046}{\htmlClass{Field}{\text{LedgerEnv.ppolicy}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8004}{\htmlId{8064}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{8074}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8004}{\htmlId{8092}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{8102}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8004}{\htmlId{8123}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1181}{\htmlId{8133}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8004}{\htmlId{8152}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7615}{\htmlId{8162}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8006}{\htmlId{8170}{\htmlClass{Bound}{\text{s}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#9529}{\htmlId{8180}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8008}{\htmlId{8194}{\htmlClass{Bound}{\text{tx}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7695}{\htmlId{8205}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8008}{\htmlId{8218}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8006}{\htmlId{8221}{\htmlClass{Bound}{\text{s}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7804}{\htmlId{8231}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8008}{\htmlId{8241}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8006}{\htmlId{8244}{\htmlClass{Bound}{\text{s}}}}\,
      \end{pmatrix}$

    certΓOf : LedgerEnv → TopLevelTx → GovState → CertEnv
    certΓOf Γ tx govSt =
      $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{8346}{\htmlClass{Function}{\text{epoch}}}}\, \,\htmlId{8352}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{8353}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8325}{\htmlId{8368}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{8369}{\htmlClass{Symbol}{\text{)}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{8379}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8325}{\htmlId{8397}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8418}{\htmlId{8407}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8327}{\htmlId{8424}{\htmlClass{Bound}{\text{tx}}}}\,
      \\ \,\href{Ledger.Core.Specification.Address.html#1975}{\htmlId{8435}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8327}{\htmlId{8449}{\htmlClass{Bound}{\text{tx}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4575}{\htmlId{8460}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8330}{\htmlId{8473}{\htmlClass{Bound}{\text{govSt}}}}\, \,\htmlId{8479}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{8480}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8325}{\htmlId{8501}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{8502}{\htmlClass{Symbol}{\text{)}}}\,
      \end{pmatrix}$

    govΓOf : LedgerEnv → TopLevelTx → CertState → GovEnv
    govΓOf Γ tx certSt =
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#7147}{\htmlId{8603}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8583}{\htmlId{8610}{\htmlClass{Bound}{\text{tx}}}}\,
      \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{8621}{\htmlClass{Function}{\text{epoch}}}}\, \,\htmlId{8627}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{8628}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8581}{\htmlId{8643}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{8644}{\htmlClass{Symbol}{\text{)}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{8654}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8581}{\htmlId{8672}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1091}{\htmlId{8682}{\htmlClass{Field}{\text{LedgerEnv.ppolicy}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8581}{\htmlId{8700}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{8710}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8581}{\htmlId{8731}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8586}{\htmlId{8741}{\htmlClass{Bound}{\text{certSt}}}}\,
      \\ \,\href{Class.IsSet.html#916}{\htmlId{8756}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{8760}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3206}{\htmlId{8761}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8586}{\htmlId{8771}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{8777}{\htmlClass{Symbol}{\text{)}}}\,
      \end{pmatrix}$

    utxoΓ-valid : LedgerEnv → LedgerState → TopLevelTx → CertState → CertState → UTxOEnv
    utxoΓ-valid Γ s tx certSt₁ certSt₂ =
      let depositsChange = calculateDepositsChange (LedgerState.certState s) certSt₁ certSt₂
      in $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{9022}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8893}{\htmlId{9037}{\htmlClass{Bound}{\text{Γ}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{9050}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8893}{\htmlId{9068}{\htmlClass{Bound}{\text{Γ}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1181}{\htmlId{9081}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8893}{\htmlId{9100}{\htmlClass{Bound}{\text{Γ}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7615}{\htmlId{9113}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8895}{\htmlId{9121}{\htmlClass{Bound}{\text{s}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8928}{\htmlId{9134}{\htmlClass{Bound}{\text{depositsChange}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7695}{\htmlId{9160}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8897}{\htmlId{9173}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8895}{\htmlId{9176}{\htmlClass{Bound}{\text{s}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7804}{\htmlId{9189}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8897}{\htmlId{9199}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8895}{\htmlId{9202}{\htmlClass{Bound}{\text{s}}}}\,
         \end{pmatrix}$

    utxoΓ-invalid : LedgerEnv → LedgerState → TopLevelTx → UTxOEnv
    utxoΓ-invalid Γ s tx =
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{9318}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9301}{\htmlId{9333}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{9343}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9301}{\htmlId{9361}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1181}{\htmlId{9371}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9301}{\htmlId{9390}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7615}{\htmlId{9400}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9303}{\htmlId{9408}{\htmlClass{Bound}{\text{s}}}}\,
      \\ \begin{pmatrix} \,\href{Data.Integer.Base.html#1545}{\htmlId{9420}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{9425}{\htmlClass{Function}{\text{0ℤ}}}}\, \end{pmatrix}
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7695}{\htmlId{9438}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9305}{\htmlId{9451}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9303}{\htmlId{9454}{\htmlClass{Bound}{\text{s}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7804}{\htmlId{9464}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9305}{\htmlId{9474}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9303}{\htmlId{9477}{\htmlClass{Bound}{\text{s}}}}\,
      \end{pmatrix}$


    computeProof : (Γ : LedgerEnv) (s : LedgerState) (txTop : TopLevelTx)
      → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s')


    computeProof Γ s txTop =
      let open LedgerEnv Γ
          open LedgerState s
          utxo₀ : UTxO
          utxo₀ = UTxOOf utxoSt
          allScripts : ℙ Script
          allScripts = getAllScripts txTop utxo₀
          allData : DataHash ⇀ Datum
          allData = setToMap (mapˢ < hash , id > (getAllData txTop))
          subΓ : SubLedgerEnv
          subΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{10011}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1091}{\htmlId{10018}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{10028}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{10038}{\htmlClass{Function}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1181}{\htmlId{10051}{\htmlClass{Function}{\text{treasury}}}}\,
                \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9730}{\htmlId{10078}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#9529}{\htmlId{10086}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9656}{\htmlId{10100}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9785}{\htmlId{10108}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9866}{\htmlId{10121}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$
      in
      case IsValidFlagOf txTop ≟ true of λ where
        (yes isV) →
          computeSubledgers subΓ s (SubTransactionsOf txTop) >>= λ where
            (s₁ , subStep) →
              let open LedgerState s₁
                    renaming ( utxoSt    to utxoSt₁
                             ; govSt     to govSt₁
                             ; certState to certState₁ )
                  certΓ : CertEnv
                  certΓ = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{10571}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{10577}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{10584}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8418}{\htmlId{10594}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9656}{\htmlId{10611}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#1975}{\htmlId{10619}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9656}{\htmlId{10633}{\htmlClass{Bound}{\text{txTop}}}}\,
                          \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4575}{\htmlId{10667}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10445}{\htmlId{10680}{\htmlClass{Function}{\text{govSt₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{10687}{\htmlClass{Function}{\text{enactState}}}}\, \end{pmatrix}$
              in
              computeCerts certΓ certState₁ (DCertsOf txTop) >>= λ where
                (certSt₂ , certStep) →
                  let govΓ : GovEnv
                      govΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#7147}{\htmlId{10896}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9656}{\htmlId{10903}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{10911}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{10917}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{10924}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1091}{\htmlId{10934}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{10944}{\htmlClass{Function}{\text{enactState}}}}\,
                            \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10807}{\htmlId{10985}{\htmlClass{Bound}{\text{certSt₂}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{10995}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{10999}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3206}{\htmlId{11000}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10807}{\htmlId{11010}{\htmlClass{Bound}{\text{certSt₂}}}}\,\,\htmlId{11017}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
                  in
                  computeGov govΓ govSt₁ (GovProposals+Votes txTop) >>= λ where
                    (govSt₂ , govStep) →
                      let certState₀ : CertState
                          certState₀ = CertStateOf s
                          depositsChange : DepositsChange
                          depositsChange = calculateDepositsChange certState₀ certState₁ certSt₂
                          utxoΓ : UTxOEnv
                          utxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{11498}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{11505}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1181}{\htmlId{11515}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9730}{\htmlId{11526}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11291}{\htmlId{11534}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9785}{\htmlId{11551}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9866}{\htmlId{11564}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$
                      in
                      -- UTXOW must run from the post-SUBLEDGERS UTxOState (utxoSt₁)
                      computeUtxow utxoΓ utxoSt₁ txTop >>= λ where
                        (utxoSt₂ , utxoStep) →
                          let finalGov = rmOrphanDRepVotes certSt₂ govSt₂
                          in
                          success ( $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11776}{\htmlId{11939}{\htmlClass{Bound}{\text{utxoSt₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11828}{\htmlId{11949}{\htmlClass{Bound}{\text{finalGov}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10807}{\htmlId{11960}{\htmlClass{Bound}{\text{certSt₂}}}}\, \end{pmatrix}$
                                  , LEDGER-V (isV , subStep , certStep , govStep , utxoStep))

        (no ¬isV) →
          let isI : IsValidFlagOf txTop ≡ false
              isI = ¬-not ¬isV
          in case computeSubledgers (subΓOf Γ s txTop) s (SubTransactionsOf txTop) of λ where
            (failure e) → failure e
            (success (s₁ , subStep)) →
              computeUtxow (utxoΓ-invalid Γ s txTop) (LedgerState.utxoSt s) txTop >>= λ where
                (utxoSt₁ , utxoStep) →
                  success ( $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#12445}{\htmlId{12497}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2155}{\htmlId{12507}{\htmlClass{Field}{\text{LedgerState.govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9654}{\htmlId{12525}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2181}{\htmlId{12529}{\htmlClass{Field}{\text{LedgerState.certState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9654}{\htmlId{12551}{\htmlClass{Bound}{\text{s}}}}\, \end{pmatrix}$
                          , LEDGER-I
                              ( isI
                              , subst (subΓOf Γ s txTop ⊢ s ⇀⦇ SubTransactionsOf txTop ,SUBLEDGERS⦈_)
                                  (SUBLEDGERS-noop isI subStep)
                                  subStep
                              , utxoStep
                              ))


    completeness : (Γ : LedgerEnv) (s : LedgerState) (txTop : TopLevelTx) (s' : LedgerState)
      → Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s' → (proj₁ <$> computeProof Γ s txTop) ≡ success s'


    completeness Γ s txTop s'
      (LEDGER-V {certState₁ = certSt₁} {certSt₂} {utxoState₁ = utxoSt₁} {govSt₁} {govSt₂} {utxoSt₂}
        (isV , subStep , certStep , govStep , utxoStep))
      with IsValidFlagOf txTop ≟ true
    ... | no ¬isV = contradiction isV ¬isV
    ... | yes refl
      with computeSubledgers (subΓOf Γ s txTop) s (SubTransactionsOf txTop)
         | complete {STS = _⊢_⇀⦇_,SUBLEDGERS⦈_}
             (subΓOf Γ s txTop) s (SubTransactionsOf txTop)
             ($\begin{pmatrix} \,\htmlId{13580}{\htmlClass{Bound}{\text{utxoSt₁}}}\, \\ \,\htmlId{13590}{\htmlClass{Bound}{\text{govSt₁}}}\, \\ \,\htmlId{13599}{\htmlClass{Bound}{\text{certSt₁}}}\, \end{pmatrix}$) subStep
    ... | success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#13640}{\htmlId{13640}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#13650}{\htmlId{13650}{\htmlClass{Bound}{\text{govSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#13659}{\htmlId{13659}{\htmlClass{Bound}{\text{certSt₁}}}}\, \end{pmatrix}$ , _) | refl
      with computeCerts (certΓOf Γ txTop govSt₁) certSt₁ (DCertsOf txTop)
         | complete {STS = _⊢_⇀⦇_,CERTS⦈_}
             (certΓOf Γ txTop govSt₁) certSt₁ (DCertsOf txTop) certSt₂ certStep
    ... | success (certSt₂ , _) | refl
      with computeGov (govΓOf Γ txTop certSt₂) govSt₁ (GovProposals+Votes txTop)
         | complete {STS = _⊢_⇀⦇_,GOVS⦈_}
             (govΓOf Γ txTop certSt₂) govSt₁ (GovProposals+Votes txTop) govSt₂ govStep
    ... | success (govSt₂ , _) | refl
      with computeUtxow (utxoΓ-valid Γ s txTop certSt₁ certSt₂) utxoSt₁ txTop
         | complete {STS = _⊢_⇀⦇_,UTXOW⦈_}
             (utxoΓ-valid Γ s txTop certSt₁ certSt₂) utxoSt₁ txTop utxoSt₂ utxoStep
    ... | success (utxoSt₂ , _) | refl = refl

    completeness Γ s txTop s' (LEDGER-I {utxoState₁ = utxoSt₁} (isI , subStep , utxoStep))
      with IsValidFlagOf txTop ≟ true
    ... | yes isV = case trans (sym isV) isI of λ ()
    ... | no ¬isV
      with computeSubledgers (subΓOf Γ s txTop) s (SubTransactionsOf txTop)
         | complete {STS = _⊢_⇀⦇_,SUBLEDGERS⦈_}
             (subΓOf Γ s txTop) s (SubTransactionsOf txTop) s subStep
    ... | success _ | refl
      with computeUtxow (utxoΓ-invalid Γ s txTop) (LedgerState.utxoSt s) txTop
         | complete {STS = _⊢_⇀⦇_,UTXOW⦈_}
             (utxoΓ-invalid Γ s txTop) (LedgerState.utxoSt s) txTop utxoSt₁ utxoStep
    ... | success _ | refl = refl

Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String
Computational-LEDGERS = it