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 Γ) (s : LedgerState) (let open LedgerState s) (stx : SubLevelTx) where subUtxoΓ : SubUTxOEnv subUtxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{4326}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1185}{\htmlId{4333}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1250}{\htmlId{4343}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1282}{\htmlId{4354}{\htmlClass{Field}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1310}{\htmlId{4362}{\htmlClass{Field}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1338}{\htmlId{4380}{\htmlClass{Field}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1370}{\htmlId{4393}{\htmlClass{Field}{\text{accountBalances}}}}\, \end{pmatrix}$ certΓ : CertEnv certΓ = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{4450}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{4456}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1185}{\htmlId{4463}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12751}{\htmlId{4473}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4249}{\htmlId{4490}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#3223}{\htmlId{4496}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4249}{\htmlId{4510}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5211}{\htmlId{4516}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2739}{\htmlId{4529}{\htmlClass{Field}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1216}{\htmlId{4535}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13558}{\htmlId{4548}{\htmlClass{Field}{\text{DirectDepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4249}{\htmlId{4565}{\htmlClass{Bound}{\text{stx}}}}\, \end{pmatrix}$ govΓ : CertState → GovEnv govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11338}{\htmlId{4626}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4249}{\htmlId{4633}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{4639}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1117}{\htmlId{4645}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1185}{\htmlId{4652}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1145}{\htmlId{4662}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1216}{\htmlId{4672}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4615}{\htmlId{4685}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{4694}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{4698}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3723}{\htmlId{4699}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4615}{\htmlId{4709}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{4715}{\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#1440}{\htmlId{8556}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1463}{\htmlId{8563}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{8573}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1524}{\htmlId{8583}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1553}{\htmlId{8596}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8399}{\htmlId{8607}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13862}{\htmlId{8615}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8361}{\htmlId{8629}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8447}{\htmlId{8637}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3723}{\htmlId{8650}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2765}{\htmlId{8660}{\htmlClass{Field}{\text{certState}}}}\, \end{pmatrix}$ certΓ : GovState → CertEnv certΓ govSt' = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{8729}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1440}{\htmlId{8735}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{8742}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12751}{\htmlId{8752}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8361}{\htmlId{8769}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#3223}{\htmlId{8777}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8361}{\htmlId{8791}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5211}{\htmlId{8799}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8718}{\htmlId{8812}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1524}{\htmlId{8819}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13558}{\htmlId{8832}{\htmlClass{Field}{\text{DirectDepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8361}{\htmlId{8849}{\htmlClass{Bound}{\text{txTop}}}}\, \end{pmatrix}$ govΓ : CertState → GovEnv govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11338}{\htmlId{8912}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8361}{\htmlId{8919}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{8927}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1440}{\htmlId{8933}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{8940}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1463}{\htmlId{8950}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1524}{\htmlId{8960}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8901}{\htmlId{8973}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{8982}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{8986}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3723}{\htmlId{8987}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8901}{\htmlId{8997}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{9003}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ utxoΓ : UTxOEnv utxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1440}{\htmlId{9046}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{9053}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1553}{\htmlId{9063}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8399}{\htmlId{9074}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2765}{\htmlId{9082}{\htmlClass{Field}{\text{certState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8447}{\htmlId{9094}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3723}{\htmlId{9107}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2765}{\htmlId{9117}{\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) ← 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{10734}{\htmlClass{Bound}{\text{utxoSt₁}}}\, \\ \,\htmlId{10744}{\htmlClass{Bound}{\text{govSt₁}}}\, \\ \,\htmlId{10753}{\htmlClass{Bound}{\text{certSt₁}}}\, \end{pmatrix}$) subStep ... | success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10796}{\htmlId{10796}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10806}{\htmlId{10806}{\htmlClass{Bound}{\text{govSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10815}{\htmlId{10815}{\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