Ledger: Computational¶
This module proves that the SUBLEDGER and LEDGER
transition rules are computational.
{-# 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
Subledger: Computational¶
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#1053}{\htmlId{3474}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1121}{\htmlId{3481}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1186}{\htmlId{3491}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1218}{\htmlId{3502}{\htmlClass{Field}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1246}{\htmlId{3510}{\htmlClass{Field}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1274}{\htmlId{3528}{\htmlClass{Field}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1306}{\htmlId{3541}{\htmlClass{Field}{\text{accountBalances}}}}\, \end{pmatrix}$ certΓ : CertEnv certΓ = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{3598}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1053}{\htmlId{3604}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1121}{\htmlId{3611}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12609}{\htmlId{3621}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3397}{\htmlId{3638}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#3223}{\htmlId{3644}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3397}{\htmlId{3658}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5147}{\htmlId{3664}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2675}{\htmlId{3677}{\htmlClass{Field}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{3683}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13416}{\htmlId{3696}{\htmlClass{Field}{\text{DirectDepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3397}{\htmlId{3713}{\htmlClass{Bound}{\text{stx}}}}\, \end{pmatrix}$ govΓ : CertState → GovEnv govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11338}{\htmlId{3774}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3397}{\htmlId{3781}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{3787}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1053}{\htmlId{3793}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1121}{\htmlId{3800}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1081}{\htmlId{3810}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{3820}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3763}{\htmlId{3833}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{3842}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{3846}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{3847}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3763}{\htmlId{3857}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{3863}{\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
Ledger: Computational¶
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#1376}{\htmlId{6615}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1399}{\htmlId{6622}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1434}{\htmlId{6632}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1460}{\htmlId{6642}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1489}{\htmlId{6655}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6458}{\htmlId{6666}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13720}{\htmlId{6674}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6420}{\htmlId{6688}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6506}{\htmlId{6696}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{6709}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2701}{\htmlId{6719}{\htmlClass{Field}{\text{certState}}}}\, \end{pmatrix}$ certΓ : GovState → CertEnv certΓ govSt' = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{6788}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1376}{\htmlId{6794}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1434}{\htmlId{6801}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12609}{\htmlId{6811}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6420}{\htmlId{6828}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#3223}{\htmlId{6836}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6420}{\htmlId{6850}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5147}{\htmlId{6858}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6777}{\htmlId{6871}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1460}{\htmlId{6878}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13416}{\htmlId{6891}{\htmlClass{Field}{\text{DirectDepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6420}{\htmlId{6908}{\htmlClass{Bound}{\text{txTop}}}}\, \end{pmatrix}$ govΓ : CertState → GovEnv govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11338}{\htmlId{6971}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6420}{\htmlId{6978}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{6986}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1376}{\htmlId{6992}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1434}{\htmlId{6999}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1399}{\htmlId{7009}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1460}{\htmlId{7019}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6960}{\htmlId{7032}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{7041}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{7045}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{7046}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6960}{\htmlId{7056}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{7062}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ utxoΓ-valid : CertState → CertState → UTxOEnv utxoΓ-valid certSt₁ certSt₂ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1376}{\htmlId{7165}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1434}{\htmlId{7172}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1489}{\htmlId{7182}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6458}{\htmlId{7193}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5316}{\htmlId{7209}{\htmlClass{Function}{\text{calculateDepositsChange}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2701}{\htmlId{7233}{\htmlClass{Field}{\text{certState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7137}{\htmlId{7243}{\htmlClass{Bound}{\text{certSt₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#7145}{\htmlId{7251}{\htmlClass{Bound}{\text{certSt₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6506}{\htmlId{7269}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{7282}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2701}{\htmlId{7292}{\htmlClass{Field}{\text{certState}}}}\, \end{pmatrix}$ utxoΓ-invalid : UTxOEnv utxoΓ-invalid = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1376}{\htmlId{7359}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1434}{\htmlId{7366}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1489}{\htmlId{7376}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6458}{\htmlId{7387}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \begin{pmatrix} \,\href{Data.Integer.Base.html#1545}{\htmlId{7397}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{7402}{\htmlClass{Function}{\text{0ℤ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#6506}{\htmlId{7409}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3780}{\htmlId{7422}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2701}{\htmlId{7432}{\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{9124}{\htmlClass{Bound}{\text{utxoSt₁}}}\, \\ \,\htmlId{9134}{\htmlClass{Bound}{\text{govSt₁}}}\, \\ \,\htmlId{9143}{\htmlClass{Bound}{\text{certSt₁}}}\, \end{pmatrix}$) subStep ... | success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9186}{\htmlId{9186}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9196}{\htmlId{9196}{\htmlClass{Bound}{\text{govSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9205}{\htmlId{9205}{\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