{-# 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#8533}{\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#7262}{\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#3152}{\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#8533}{\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#7262}{\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#3152}{\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 (utxo₀Of s)))

    subΓOf : LedgerEnv → LedgerState → TopLevelTx → SubLedgerEnv
    subΓOf Γ s tx =
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{8033}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8016}{\htmlId{8048}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1091}{\htmlId{8058}{\htmlClass{Field}{\text{LedgerEnv.ppolicy}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8016}{\htmlId{8076}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{8086}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8016}{\htmlId{8104}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{8114}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8016}{\htmlId{8135}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1181}{\htmlId{8145}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8016}{\htmlId{8164}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7615}{\htmlId{8174}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8018}{\htmlId{8182}{\htmlClass{Bound}{\text{s}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#9658}{\htmlId{8192}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8020}{\htmlId{8206}{\htmlClass{Bound}{\text{tx}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7695}{\htmlId{8217}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8020}{\htmlId{8230}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8018}{\htmlId{8233}{\htmlClass{Bound}{\text{s}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7804}{\htmlId{8243}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8020}{\htmlId{8253}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8018}{\htmlId{8256}{\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{8358}{\htmlClass{Function}{\text{epoch}}}}\, \,\htmlId{8364}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{8365}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8337}{\htmlId{8380}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{8381}{\htmlClass{Symbol}{\text{)}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{8391}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8337}{\htmlId{8409}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8533}{\htmlId{8419}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8339}{\htmlId{8436}{\htmlClass{Bound}{\text{tx}}}}\,
      \\ \,\href{Ledger.Core.Specification.Address.html#1975}{\htmlId{8447}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8339}{\htmlId{8461}{\htmlClass{Bound}{\text{tx}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4575}{\htmlId{8472}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8342}{\htmlId{8485}{\htmlClass{Bound}{\text{govSt}}}}\, \,\htmlId{8491}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{8492}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8337}{\htmlId{8513}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{8514}{\htmlClass{Symbol}{\text{)}}}\,
      \end{pmatrix}$

    govΓOf : LedgerEnv → TopLevelTx → CertState → GovEnv
    govΓOf Γ tx certSt =
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#7262}{\htmlId{8615}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8595}{\htmlId{8622}{\htmlClass{Bound}{\text{tx}}}}\,
      \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{8633}{\htmlClass{Function}{\text{epoch}}}}\, \,\htmlId{8639}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{8640}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8593}{\htmlId{8655}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{8656}{\htmlClass{Symbol}{\text{)}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{8666}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8593}{\htmlId{8684}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1091}{\htmlId{8694}{\htmlClass{Field}{\text{LedgerEnv.ppolicy}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8593}{\htmlId{8712}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{8722}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8593}{\htmlId{8743}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8598}{\htmlId{8753}{\htmlClass{Bound}{\text{certSt}}}}\,
      \\ \,\href{Class.IsSet.html#916}{\htmlId{8768}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{8772}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3152}{\htmlId{8773}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8598}{\htmlId{8783}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{8789}{\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{9034}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8905}{\htmlId{9049}{\htmlClass{Bound}{\text{Γ}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{9062}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8905}{\htmlId{9080}{\htmlClass{Bound}{\text{Γ}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1181}{\htmlId{9093}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8905}{\htmlId{9112}{\htmlClass{Bound}{\text{Γ}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7615}{\htmlId{9125}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8907}{\htmlId{9133}{\htmlClass{Bound}{\text{s}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8940}{\htmlId{9146}{\htmlClass{Bound}{\text{depositsChange}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7695}{\htmlId{9172}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8909}{\htmlId{9185}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8907}{\htmlId{9188}{\htmlClass{Bound}{\text{s}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7804}{\htmlId{9201}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8909}{\htmlId{9211}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8907}{\htmlId{9214}{\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{9330}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9313}{\htmlId{9345}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{9355}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9313}{\htmlId{9373}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1181}{\htmlId{9383}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9313}{\htmlId{9402}{\htmlClass{Bound}{\text{Γ}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7615}{\htmlId{9412}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9315}{\htmlId{9420}{\htmlClass{Bound}{\text{s}}}}\,
      \\ \begin{pmatrix} \,\href{Data.Integer.Base.html#1545}{\htmlId{9432}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{9437}{\htmlClass{Function}{\text{0ℤ}}}}\, \end{pmatrix}
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7695}{\htmlId{9450}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9317}{\htmlId{9463}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9315}{\htmlId{9466}{\htmlClass{Bound}{\text{s}}}}\,
      \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7804}{\htmlId{9476}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9317}{\htmlId{9486}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9315}{\htmlId{9489}{\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 utxo₀))
          subΓ : SubLedgerEnv
          subΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{10029}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1091}{\htmlId{10036}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{10046}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{10056}{\htmlClass{Function}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1181}{\htmlId{10069}{\htmlClass{Function}{\text{treasury}}}}\,
                \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9742}{\htmlId{10096}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#9658}{\htmlId{10104}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9668}{\htmlId{10118}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9797}{\htmlId{10126}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9878}{\htmlId{10139}{\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{10589}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{10595}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{10602}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8533}{\htmlId{10612}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9668}{\htmlId{10629}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#1975}{\htmlId{10637}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9668}{\htmlId{10651}{\htmlClass{Bound}{\text{txTop}}}}\,
                          \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4575}{\htmlId{10685}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10463}{\htmlId{10698}{\htmlClass{Function}{\text{govSt₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{10705}{\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#7262}{\htmlId{10914}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9668}{\htmlId{10921}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{10929}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1068}{\htmlId{10935}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{10942}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1091}{\htmlId{10952}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{10962}{\htmlClass{Function}{\text{enactState}}}}\,
                            \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10825}{\htmlId{11003}{\htmlClass{Bound}{\text{certSt₂}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{11013}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{11017}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3152}{\htmlId{11018}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10825}{\htmlId{11028}{\htmlClass{Bound}{\text{certSt₂}}}}\,\,\htmlId{11035}{\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{11516}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1126}{\htmlId{11523}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1181}{\htmlId{11533}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9742}{\htmlId{11544}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11309}{\htmlId{11552}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9797}{\htmlId{11569}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9878}{\htmlId{11582}{\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#11794}{\htmlId{11957}{\htmlClass{Bound}{\text{utxoSt₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11846}{\htmlId{11967}{\htmlClass{Bound}{\text{finalGov}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10825}{\htmlId{11978}{\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#12463}{\htmlId{12515}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2155}{\htmlId{12525}{\htmlClass{Field}{\text{LedgerState.govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9666}{\htmlId{12543}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2181}{\htmlId{12547}{\htmlClass{Field}{\text{LedgerState.certState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9666}{\htmlId{12569}{\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{13598}{\htmlClass{Bound}{\text{utxoSt₁}}}\, \\ \,\htmlId{13608}{\htmlClass{Bound}{\text{govSt₁}}}\, \\ \,\htmlId{13617}{\htmlClass{Bound}{\text{certSt₁}}}\, \end{pmatrix}$) subStep
    ... | success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#13658}{\htmlId{13658}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#13668}{\htmlId{13668}{\htmlClass{Bound}{\text{govSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#13677}{\htmlId{13677}{\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