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 txs open import Ledger.Dijkstra.Specification.Entities.Properties.Computational txs 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⦈_} computeSubentities : ∀ Γ s x → ComputationResult String (∃ λ s' → Γ ⊢ s ⇀⦇ x ,SUBENTITIES⦈ s') computeSubentities = comp {STS = _⊢_⇀⦇_,SUBENTITIES⦈_} 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⦈_} completeSubentities : ∀ Γ s x s' → Γ ⊢ s ⇀⦇ x ,SUBENTITIES⦈ s' → (proj₁ <$> computeSubentities Γ s x) ≡ success s' completeSubentities = complete {STS = _⊢_⇀⦇_,SUBENTITIES⦈_} 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#1108}{\htmlId{4335}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1176}{\htmlId{4342}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1241}{\htmlId{4352}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1273}{\htmlId{4363}{\htmlClass{Field}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1332}{\htmlId{4371}{\htmlClass{Field}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1364}{\htmlId{4384}{\htmlClass{Field}{\text{isTopLevelValid}}}}\, \end{pmatrix}$ subentitiesΓ : SubEntitiesEnv subentitiesΓ = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{4462}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1108}{\htmlId{4468}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1176}{\htmlId{4475}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5048}{\htmlId{4485}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2576}{\htmlId{4498}{\htmlClass{Field}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1207}{\htmlId{4504}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1301}{\htmlId{4517}{\htmlClass{Field}{\text{rewards₀}}}}\, \end{pmatrix}$ govΓ : CertState → GovEnv govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11069}{\htmlId{4584}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4258}{\htmlId{4591}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{4597}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1108}{\htmlId{4603}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1176}{\htmlId{4610}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1136}{\htmlId{4620}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1207}{\htmlId{4630}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4573}{\htmlId{4643}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{4652}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{4656}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#4508}{\htmlId{4657}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4573}{\htmlId{4667}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{4673}{\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) ← computeSubentities subentitiesΓ certState 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 computeSubentities subentitiesΓ certState stx | completeSubentities _ _ _ _ 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₀ legacyMode : Bool legacyMode = isLegacyMode utxo₀ allScripts txTop subΓ : SubLedgerEnv subΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1431}{\htmlId{8595}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1454}{\htmlId{8602}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1489}{\htmlId{8612}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1515}{\htmlId{8622}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1544}{\htmlId{8635}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8358}{\htmlId{8646}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4508}{\htmlId{8654}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\htmlId{8664}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#5180}{\htmlId{8665}{\htmlClass{Field}{\text{CertStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8267}{\htmlId{8677}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{8678}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8406}{\htmlId{8682}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13753}{\htmlId{8695}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8320}{\htmlId{8709}{\htmlClass{Bound}{\text{txTop}}}}\, \end{pmatrix}$ entitiesΓ : GovState → CertState → EntitiesEnv entitiesΓ govSt certSt = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{8804}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1431}{\htmlId{8810}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1489}{\htmlId{8817}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5048}{\htmlId{8827}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8787}{\htmlId{8840}{\htmlClass{Bound}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1515}{\htmlId{8846}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8480}{\htmlId{8859}{\htmlClass{Function}{\text{legacyMode}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4508}{\htmlId{8872}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8793}{\htmlId{8882}{\htmlClass{Bound}{\text{certSt}}}}\, \end{pmatrix}$ govΓ : CertState → GovEnv govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11069}{\htmlId{8946}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8320}{\htmlId{8953}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{8961}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1431}{\htmlId{8967}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1489}{\htmlId{8974}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1454}{\htmlId{8984}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1515}{\htmlId{8994}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8935}{\htmlId{9007}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{9016}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{9020}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#4508}{\htmlId{9021}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8935}{\htmlId{9031}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{9037}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ utxoΓ : UTxOEnv utxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1431}{\htmlId{9080}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1489}{\htmlId{9087}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1544}{\htmlId{9097}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8358}{\htmlId{9108}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4286}{\htmlId{9116}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\htmlId{9124}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#5180}{\htmlId{9125}{\htmlClass{Field}{\text{CertStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8267}{\htmlId{9137}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{9138}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8406}{\htmlId{9142}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8480}{\htmlId{9155}{\htmlClass{Function}{\text{legacyMode}}}}\, \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 (entitiesΓ (GovStateOf s₁) (CertStateOf s)) (CertStateOf s₁) 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{10782}{\htmlClass{Bound}{\text{utxoSt₁}}}\, \\ \,\htmlId{10792}{\htmlClass{Bound}{\text{govSt₁}}}\, \\ \,\htmlId{10801}{\htmlClass{Bound}{\text{certSt₁}}}\, \end{pmatrix}$) subStep ... | success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10844}{\htmlId{10844}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10854}{\htmlId{10854}{\htmlClass{Bound}{\text{govSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10863}{\htmlId{10863}{\htmlClass{Bound}{\text{certSt₁}}}}\, \end{pmatrix}$ , _) | refl with computeEntities (entitiesΓ govSt₁ (CertStateOf s)) certSt₁ txTop | completeEntities (entitiesΓ govSt₁ (CertStateOf s)) certSt₁ 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