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 module Ledger.Dijkstra.Specification.Ledger.Properties.Computational (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where open import Ledger.Prelude open import Ledger.Dijkstra.Specification.Certs govStructure open import Ledger.Dijkstra.Specification.Entities govStructure open import Ledger.Dijkstra.Specification.Entities.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) opaque computeSubutxow : ∀ Γ s x → ComputationResult String (∃ λ s' → Γ ⊢ s ⇀⦇ x ,SUBUTXOW⦈ s') computeSubutxow = comp {STS = _⊢_⇀⦇_,SUBUTXOW⦈_} computeEntities : ∀ Γ s x → ComputationResult String (∃ λ s' → Γ ⊢ s ⇀⦇ x ,ENTITIES⦈ s') computeEntities = comp {STS = _⊢_⇀⦇_,ENTITIES⦈_} computeGov : ∀ Γ s x → ComputationResult String (∃ λ s' → Γ ⊢ s ⇀⦇ x ,GOVS⦈ s') computeGov = comp {STS = _⊢_⇀⦇_,GOVS⦈_} completeGov : ∀ Γ s x s' → Γ ⊢ s ⇀⦇ x ,GOVS⦈ s' → (proj₁ <$> computeGov Γ s x) ≡ success s' completeGov = complete {STS = _⊢_⇀⦇_,GOVS⦈_} completeSubutxow : ∀ Γ s x s' → Γ ⊢ s ⇀⦇ x ,SUBUTXOW⦈ s' → (proj₁ <$> computeSubutxow Γ s x) ≡ success s' completeSubutxow = complete {STS = _⊢_⇀⦇_,SUBUTXOW⦈_} completeEntities : ∀ Γ s x s' → Γ ⊢ s ⇀⦇ x ,ENTITIES⦈ s' → (proj₁ <$> computeEntities Γ s x) ≡ success s' completeEntities = complete {STS = _⊢_⇀⦇_,ENTITIES⦈_} module go (Γ : SubLedgerEnv) (let open SubLedgerEnv Γ renaming (certState to certState')) (s : LedgerState) (let open LedgerState s) (stx : SubLevelTx) where subUtxoΓ : SubUTxOEnv subUtxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{4361}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1185}{\htmlId{4368}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1250}{\htmlId{4378}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1282}{\htmlId{4389}{\htmlClass{Field}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4212}{\htmlId{4397}{\htmlClass{Field}{\text{certState'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1343}{\htmlId{4410}{\htmlClass{Field}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1375}{\htmlId{4423}{\htmlClass{Field}{\text{isTopLevelValid}}}}\, \end{pmatrix}$ certΓ : CertEnv certΓ = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{4480}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{4486}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1185}{\htmlId{4493}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12751}{\htmlId{4503}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4284}{\htmlId{4520}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#3223}{\htmlId{4526}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4284}{\htmlId{4540}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5059}{\htmlId{4546}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2587}{\htmlId{4559}{\htmlClass{Field}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1216}{\htmlId{4565}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13558}{\htmlId{4578}{\htmlClass{Field}{\text{DirectDepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4284}{\htmlId{4595}{\htmlClass{Bound}{\text{stx}}}}\, \end{pmatrix}$ govΓ : CertState → GovEnv govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11338}{\htmlId{4656}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4284}{\htmlId{4663}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{4669}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{4675}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1185}{\htmlId{4682}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1145}{\htmlId{4692}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1216}{\htmlId{4702}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4645}{\htmlId{4715}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{4724}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{4728}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3723}{\htmlId{4729}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4645}{\htmlId{4739}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{4745}{\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) ← computeEntities 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 | completeSubutxow _ _ _ _ utxoStep ... | success (utxoSt' , _) | refl with computeEntities certΓ certState (DCertsOf stx) | completeEntities _ _ _ _ certStep ... | success (certSt' , _) | refl with computeGov (govΓ certSt') govSt (GovProposals+Votes stx) | completeGov (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 | completeSubutxow _ _ _ _ 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) opaque computeSubledgers : ∀ Γ s x → ComputationResult String (∃ λ s' → Γ ⊢ s ⇀⦇ x ,SUBLEDGERS⦈ s') computeSubledgers = comp {STS = _⊢_⇀⦇_,SUBLEDGERS⦈_} computeUtxow : ∀ Γ s x → ComputationResult String (∃ λ s' → Γ ⊢ s ⇀⦇ x ,UTXOW⦈ s') computeUtxow = comp {STS = _⊢_⇀⦇_,UTXOW⦈_} computeEntities : ∀ Γ s x → ComputationResult String (∃ λ s' → Γ ⊢ s ⇀⦇ x ,ENTITIES⦈ s') computeEntities = comp {STS = _⊢_⇀⦇_,ENTITIES⦈_} computeGov : ∀ Γ s x → ComputationResult String (∃ λ s' → Γ ⊢ s ⇀⦇ x ,GOVS⦈ s') computeGov = comp {STS = _⊢_⇀⦇_,GOVS⦈_} completeSubledgers : ∀ Γ s x s' → Γ ⊢ s ⇀⦇ x ,SUBLEDGERS⦈ s' → (proj₁ <$> computeSubledgers Γ s x) ≡ success s' completeSubledgers = complete {STS = _⊢_⇀⦇_,SUBLEDGERS⦈_} completeUtxow : ∀ Γ s x s' → Γ ⊢ s ⇀⦇ x ,UTXOW⦈ s' → (proj₁ <$> computeUtxow Γ s x) ≡ success s' completeUtxow = complete {STS = _⊢_⇀⦇_,UTXOW⦈_} completeEntities : ∀ Γ s x s' → Γ ⊢ s ⇀⦇ x ,ENTITIES⦈ s' → (proj₁ <$> computeEntities Γ s x) ≡ success s' completeEntities = complete {STS = _⊢_⇀⦇_,ENTITIES⦈_} completeGov : ∀ Γ s x s' → Γ ⊢ s ⇀⦇ x ,GOVS⦈ s' → (proj₁ <$> computeGov Γ s x) ≡ success s' completeGov = complete {STS = _⊢_⇀⦇_,GOVS⦈_} 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#1442}{\htmlId{8586}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1465}{\htmlId{8593}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1500}{\htmlId{8603}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1526}{\htmlId{8613}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1555}{\htmlId{8626}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8429}{\htmlId{8637}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2613}{\htmlId{8645}{\htmlClass{Field}{\text{certState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8477}{\htmlId{8657}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13862}{\htmlId{8670}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8391}{\htmlId{8684}{\htmlClass{Bound}{\text{txTop}}}}\, \end{pmatrix}$ certΓ : GovState → CertEnv certΓ govSt' = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{8749}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1442}{\htmlId{8755}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1500}{\htmlId{8762}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12751}{\htmlId{8772}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8391}{\htmlId{8789}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#3223}{\htmlId{8797}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8391}{\htmlId{8811}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5059}{\htmlId{8819}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8738}{\htmlId{8832}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1526}{\htmlId{8839}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13558}{\htmlId{8852}{\htmlClass{Field}{\text{DirectDepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8391}{\htmlId{8869}{\htmlClass{Bound}{\text{txTop}}}}\, \end{pmatrix}$ govΓ : CertState → GovEnv govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11338}{\htmlId{8932}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8391}{\htmlId{8939}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{8947}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1442}{\htmlId{8953}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1500}{\htmlId{8960}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1465}{\htmlId{8970}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1526}{\htmlId{8980}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8921}{\htmlId{8993}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{9002}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{9006}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3723}{\htmlId{9007}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8921}{\htmlId{9017}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{9023}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ utxoΓ : UTxOEnv utxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1442}{\htmlId{9066}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1500}{\htmlId{9073}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1555}{\htmlId{9083}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8429}{\htmlId{9094}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2613}{\htmlId{9102}{\htmlClass{Field}{\text{certState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8477}{\htmlId{9114}{\htmlClass{Function}{\text{allScripts}}}}\, \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) ← computeEntities (certΓ (GovStateOf s₁)) (CertStateOf s₁) (DCertsOf txTop) (govSt₂ , govStep) ← computeGov (govΓ certSt₂) (GovStateOf s₁) (GovProposals+Votes txTop) (utxoSt₂ , utxoStep) ← computeUtxow utxoΓ (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Γ 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 {utxoState₁ = utxoSt₁} {govSt₁} {certSt₁} {certSt₂} {govSt₂} {utxoSt₂} (v , subStep , entitiesStep , govStep , utxoStep)) with IsValidFlagOf txTop ≟ true ... | no ¬v = contradiction v ¬v ... | yes refl with computeSubledgers subΓ s (SubTransactionsOf txTop) | completeSubledgers subΓ s (SubTransactionsOf txTop) ($\begin{pmatrix} \,\htmlId{10732}{\htmlClass{Bound}{\text{utxoSt₁}}}\, \\ \,\htmlId{10742}{\htmlClass{Bound}{\text{govSt₁}}}\, \\ \,\htmlId{10751}{\htmlClass{Bound}{\text{certSt₁}}}\, \end{pmatrix}$) subStep ... | success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10794}{\htmlId{10794}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10804}{\htmlId{10804}{\htmlClass{Bound}{\text{govSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10813}{\htmlId{10813}{\htmlClass{Bound}{\text{certSt₁}}}}\, \end{pmatrix}$ , _) | refl with computeEntities (certΓ govSt₁) certSt₁ (DCertsOf txTop) | completeEntities (certΓ govSt₁) certSt₁ (DCertsOf txTop) certSt₂ entitiesStep ... | success (certSt₂ , _) | refl with computeGov (govΓ certSt₂) govSt₁ (GovProposals+Votes txTop) | completeGov (govΓ certSt₂) govSt₁ (GovProposals+Votes txTop) govSt₂ govStep ... | success (govSt₂ , _) | refl with computeUtxow utxoΓ utxoSt₁ txTop | completeUtxow utxoΓ 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) | completeSubledgers subΓ s (SubTransactionsOf txTop) s subStep ... | success _ | refl with computeUtxow utxoΓ utxoSt txTop | completeUtxow utxoΓ utxoSt txTop utxoSt₁ utxoStep ... | success _ | refl = refl Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String Computational-LEDGERS = it