{-# 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 = record {go}
    where
    open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete)
    computeSubutxow = comp {STS = _⊢_⇀⦇_,SUBUTXOW⦈_}
    computeCerts    = comp {STS = _⊢_⇀⦇_,CERTS⦈_}
    computeGov      = comp {STS = _⊢_⇀⦇_,GOVS⦈_}

    module go
      (Γ   : SubLedgerEnv) (let open SubLedgerEnv Γ)
      (s   : LedgerState)  (let open LedgerState s)
      (stx : SubLevelTx)
      where
      subUtxoΓ : SubUTxOEnv
      subUtxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#736}{\htmlId{3078}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#804}{\htmlId{3085}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#869}{\htmlId{3095}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#901}{\htmlId{3106}{\htmlClass{Field}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#929}{\htmlId{3114}{\htmlClass{Field}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#957}{\htmlId{3132}{\htmlClass{Field}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#989}{\htmlId{3145}{\htmlClass{Field}{\text{accountBalances}}}}\, \end{pmatrix}$

      certΓ : CertEnv
      certΓ = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{3202}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#736}{\htmlId{3208}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#804}{\htmlId{3215}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8430}{\htmlId{3225}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3001}{\htmlId{3242}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2222}{\htmlId{3248}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3001}{\htmlId{3262}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4720}{\htmlId{3268}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2300}{\htmlId{3281}{\htmlClass{Field}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#835}{\htmlId{3287}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#9237}{\htmlId{3300}{\htmlClass{Field}{\text{DirectDepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3001}{\htmlId{3317}{\htmlClass{Bound}{\text{stx}}}}\, \end{pmatrix}$

      govΓ : CertState → GovEnv
      govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#7159}{\htmlId{3378}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3001}{\htmlId{3385}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{3391}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#736}{\htmlId{3397}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#804}{\htmlId{3404}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#764}{\htmlId{3414}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#835}{\htmlId{3424}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3367}{\htmlId{3437}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{3446}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{3450}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3273}{\htmlId{3451}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3367}{\htmlId{3461}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{3467}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$


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


      computeProof = case isTopLevelValid ≟ true of λ where
        (yes p) → do
          (utxoSt' , utxoStep) ← computeSubutxow subUtxoΓ utxoSt stx
          (certSt' , certStep) ← computeCerts certΓ certState (DCertsOf stx)
          (govSt'  , govStep)  ← computeGov (govΓ certSt') govSt (GovProposals+Votes stx)
          success (_ , SUBLEDGER-V (p , utxoStep , certStep , govStep))
        (no ¬p) → do
          (utxoSt' , utxoStep) ← computeSubutxow subUtxoΓ utxoSt stx
          let utxoStep' = subst (subUtxoΓ ⊢ utxoSt ⇀⦇ stx ,SUBUTXOW⦈_)
                                (SUBUTXOW-noop (¬-not ¬p) utxoStep) utxoStep
          success (_ , SUBLEDGER-I (¬-not ¬p , utxoStep'))


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


      completeness sub' (SUBLEDGER-V (v , utxoStep , certStep , govStep))
        with isTopLevelValid ≟ true
      ... | no ¬v = contradiction v ¬v
      ... | yes refl
        with computeSubutxow subUtxoΓ utxoSt stx | complete _ _ _ _ utxoStep
      ... | success (utxoSt' , _) | refl
        with computeCerts certΓ certState (DCertsOf stx) | complete _ _ _ _ certStep
      ... | success (certSt' , _) | refl
        with computeGov (govΓ certSt') govSt (GovProposals+Votes stx)
           | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ certSt') _ _ _ govStep
      ... | success (govSt' , _) | refl = refl
      completeness sub' (SUBLEDGER-I (i , utxoStep))
        with isTopLevelValid ≟ true
      ... | yes v = case trans (sym v) i of λ ()
      ... | no ¬v
        with computeSubutxow subUtxoΓ utxoSt stx | complete _ _ _ _ utxoStep
      ... | success (utxoSt' , _) | refl = refl

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

instance


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


  Computational-LEDGER = record {go}
    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⦈_}

    module go
      (Γ     : LedgerEnv)   (let open LedgerEnv Γ)
      (s     : LedgerState) (let open LedgerState s)
      (txTop : TopLevelTx)
      where
      utxo₀ : UTxO
      utxo₀ = UTxOOf utxoSt

      allScripts : ℙ Script
      allScripts = getAllScripts txTop utxo₀

      subΓ : SubLedgerEnv
      subΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1059}{\htmlId{6072}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1082}{\htmlId{6079}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{6089}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1143}{\htmlId{6099}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1172}{\htmlId{6112}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5915}{\htmlId{6123}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#9541}{\htmlId{6131}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5877}{\htmlId{6145}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5963}{\htmlId{6153}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3273}{\htmlId{6166}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2326}{\htmlId{6176}{\htmlClass{Field}{\text{certState}}}}\, \end{pmatrix}$

      certΓ : GovState → CertEnv
      certΓ govSt' = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{6245}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1059}{\htmlId{6251}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{6258}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#8430}{\htmlId{6268}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5877}{\htmlId{6285}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2222}{\htmlId{6293}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5877}{\htmlId{6307}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4720}{\htmlId{6315}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6234}{\htmlId{6328}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1143}{\htmlId{6335}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#9237}{\htmlId{6348}{\htmlClass{Field}{\text{DirectDepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5877}{\htmlId{6365}{\htmlClass{Bound}{\text{txTop}}}}\, \end{pmatrix}$

      govΓ : CertState → GovEnv
      govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#7159}{\htmlId{6428}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5877}{\htmlId{6435}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#858}{\htmlId{6443}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1059}{\htmlId{6449}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{6456}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1082}{\htmlId{6466}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1143}{\htmlId{6476}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6417}{\htmlId{6489}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6498}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6502}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3273}{\htmlId{6503}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6417}{\htmlId{6513}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{6519}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$

      utxoΓ-valid : CertState → CertState → UTxOEnv
      utxoΓ-valid certSt₁ certSt₂ =
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1059}{\htmlId{6622}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{6629}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1172}{\htmlId{6639}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5915}{\htmlId{6650}{\htmlClass{Function}{\text{utxo₀}}}}\,
        \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4889}{\htmlId{6666}{\htmlClass{Function}{\text{calculateDepositsChange}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2326}{\htmlId{6690}{\htmlClass{Field}{\text{certState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6594}{\htmlId{6700}{\htmlClass{Bound}{\text{certSt₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6602}{\htmlId{6708}{\htmlClass{Bound}{\text{certSt₂}}}}\,
        \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5963}{\htmlId{6726}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3273}{\htmlId{6739}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2326}{\htmlId{6749}{\htmlClass{Field}{\text{certState}}}}\, \end{pmatrix}$

      utxoΓ-invalid : UTxOEnv
      utxoΓ-invalid = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1059}{\htmlId{6816}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{6823}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1172}{\htmlId{6833}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5915}{\htmlId{6844}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \begin{pmatrix} \,\href{Data.Integer.Base.html#1545}{\htmlId{6854}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{6859}{\htmlClass{Function}{\text{0ℤ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5963}{\htmlId{6866}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3273}{\htmlId{6879}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2326}{\htmlId{6889}{\htmlClass{Field}{\text{certState}}}}\, \end{pmatrix}$


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


      computeProof = case IsValidFlagOf txTop ≟ true of λ where
        (yes p) → do
          (s₁      , subStep)  ← computeSubledgers subΓ s (SubTransactionsOf txTop)
          (certSt₂ , certStep) ← computeCerts (certΓ (GovStateOf s₁)) (CertStateOf s₁) (DCertsOf txTop)
          (govSt₂  , govStep)  ← computeGov (govΓ certSt₂) (GovStateOf s₁) (GovProposals+Votes txTop)
          (utxoSt₂ , utxoStep) ← computeUtxow (utxoΓ-valid (CertStateOf s₁) certSt₂) (UTxOStateOf s₁) txTop
          success (_ , LEDGER-V (p , subStep , certStep , govStep , utxoStep))
        (no ¬p) → do
          (s₁      , subStep)  ← computeSubledgers subΓ s (SubTransactionsOf txTop)
          (utxoSt₁ , utxoStep) ← computeUtxow utxoΓ-invalid utxoSt txTop
          let subStep' = subst (subΓ ⊢ s ⇀⦇ SubTransactionsOf txTop ,SUBLEDGERS⦈_)
                               (SUBLEDGERS-noop (¬-not ¬p) subStep) subStep
          success (_ , LEDGER-I (¬-not ¬p , subStep' , utxoStep))


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


      completeness ledgerSt
        (LEDGER-V {certState₁ = certSt₁} {certSt₂} {utxoState₁ = utxoSt₁} {govSt₁} {govSt₂} {utxoSt₂}
                  (v , subStep , certStep , govStep , utxoStep))
        with IsValidFlagOf txTop ≟ true
      ... | no ¬v = contradiction v ¬v
      ... | yes refl
        with computeSubledgers subΓ s (SubTransactionsOf txTop)
           | complete {STS = _⊢_⇀⦇_,SUBLEDGERS⦈_} subΓ s (SubTransactionsOf txTop)
                      ($\begin{pmatrix} \,\htmlId{8519}{\htmlClass{Bound}{\text{utxoSt₁}}}\, \\ \,\htmlId{8529}{\htmlClass{Bound}{\text{govSt₁}}}\, \\ \,\htmlId{8538}{\htmlClass{Bound}{\text{certSt₁}}}\, \end{pmatrix}$) subStep
      ... | success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8581}{\htmlId{8581}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8591}{\htmlId{8591}{\htmlClass{Bound}{\text{govSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8600}{\htmlId{8600}{\htmlClass{Bound}{\text{certSt₁}}}}\, \end{pmatrix}$ , _) | refl
        with computeCerts (certΓ govSt₁) certSt₁ (DCertsOf txTop)
           | complete {STS = _⊢_⇀⦇_,CERTS⦈_} (certΓ govSt₁) certSt₁ (DCertsOf txTop) certSt₂ certStep
      ... | success (certSt₂ , _) | refl
        with computeGov (govΓ certSt₂) govSt₁ (GovProposals+Votes txTop)
           | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ certSt₂) govSt₁ (GovProposals+Votes txTop) govSt₂ govStep
      ... | success (govSt₂ , _) | refl
        with computeUtxow (utxoΓ-valid certSt₁ certSt₂) utxoSt₁ txTop
           | complete {STS = _⊢_⇀⦇_,UTXOW⦈_} (utxoΓ-valid certSt₁ certSt₂) utxoSt₁ txTop utxoSt₂ utxoStep
      ... | success (utxoSt₂ , _) | refl = refl
      completeness ledgerSt
        (LEDGER-I {utxoState₁ = utxoSt₁} (i , subStep , utxoStep))
        with IsValidFlagOf txTop ≟ true
      ... | yes v = case trans (sym v) i of λ ()
      ... | no ¬v
        with computeSubledgers subΓ s (SubTransactionsOf txTop)
           | complete {STS = _⊢_⇀⦇_,SUBLEDGERS⦈_} subΓ s (SubTransactionsOf txTop) s subStep
      ... | success _ | refl
        with computeUtxow utxoΓ-invalid utxoSt txTop
           | complete {STS = _⊢_⇀⦇_,UTXOW⦈_} utxoΓ-invalid utxoSt txTop utxoSt₁ utxoStep
      ... | success _ | refl = refl

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