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 = MkComputational computeProof completeness where open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete) computeSubutxow = comp {STS = _⊢_⇀⦇_,SUBUTXOW⦈_} computeCerts = comp {STS = _⊢_⇀⦇_,CERTS⦈_} computeGov = comp {STS = _⊢_⇀⦇_,GOVS⦈_} -- Helper env constructors (avoid `let ... in with ...` parse issues) subUtxoΓ : SubLedgerEnv → SubUTxOEnv subUtxoΓ Γ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1053}{\htmlId{3428}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1121}{\htmlId{3435}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1186}{\htmlId{3445}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1218}{\htmlId{3456}{\htmlClass{Field}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1246}{\htmlId{3464}{\htmlClass{Field}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1274}{\htmlId{3482}{\htmlClass{Field}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1306}{\htmlId{3495}{\htmlClass{Field}{\text{allData}}}}\, \end{pmatrix}$ where open SubLedgerEnv Γ certΓ : SubLedgerEnv → LedgerState → SubLevelTx → CertEnv certΓ Γ s stx = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{3622}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1053}{\htmlId{3628}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1121}{\htmlId{3635}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12597}{\htmlId{3645}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3614}{\htmlId{3662}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2976}{\htmlId{3668}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3614}{\htmlId{3682}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5002}{\htmlId{3688}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\htmlId{3701}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#2530}{\htmlId{3702}{\htmlClass{Field}{\text{LedgerState.govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3612}{\htmlId{3720}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{3721}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{3723}{\htmlClass{Function}{\text{enactState}}}}\, \end{pmatrix}$ where open SubLedgerEnv Γ govΓ : SubLedgerEnv → SubLevelTx → CertState → GovEnv govΓ Γ stx certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11326}{\htmlId{3853}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3838}{\htmlId{3860}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{3866}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1053}{\htmlId{3872}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1121}{\htmlId{3879}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1081}{\htmlId{3889}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{3899}{\htmlClass{Function}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3842}{\htmlId{3912}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{3921}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{3925}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3713}{\htmlId{3926}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#3842}{\htmlId{3936}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{3942}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ where open SubLedgerEnv Γ
computeProof : (Γ : SubLedgerEnv) (s : LedgerState) (stx : SubLevelTx) → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s')
computeProof Γ s stx with SubLedgerEnv.isTopLevelValid Γ ≟ true ... | yes isV = let open SubLedgerEnv Γ open LedgerState s subUtxoΓ : SubUTxOEnv subUtxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1053}{\htmlId{4361}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1121}{\htmlId{4368}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1186}{\htmlId{4378}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1218}{\htmlId{4389}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1246}{\htmlId{4397}{\htmlClass{Function}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1274}{\htmlId{4415}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1306}{\htmlId{4428}{\htmlClass{Function}{\text{allData}}}}\, \end{pmatrix}$ certΓ : CertEnv certΓ = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{4484}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1053}{\htmlId{4490}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1121}{\htmlId{4497}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12597}{\htmlId{4507}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\htmlId{4524}{\htmlClass{Bound}{\text{stx}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2976}{\htmlId{4530}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\htmlId{4544}{\htmlClass{Bound}{\text{stx}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5002}{\htmlId{4568}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2530}{\htmlId{4581}{\htmlClass{Function}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{4587}{\htmlClass{Function}{\text{enactState}}}}\, \end{pmatrix}$ in computeSubutxow subUtxoΓ utxoSt stx >>= λ where (utxoSt' , utxoStep) → computeCerts certΓ certState (DCertsOf stx) >>= λ where (certSt' , certStep) → let govΓ : GovEnv govΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11326}{\htmlId{4854}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\htmlId{4861}{\htmlClass{Bound}{\text{stx}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{4867}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1053}{\htmlId{4873}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1121}{\htmlId{4880}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1081}{\htmlId{4890}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1152}{\htmlId{4900}{\htmlClass{Function}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4773}{\htmlId{4937}{\htmlClass{Bound}{\text{certSt'}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{4947}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{4951}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3713}{\htmlId{4952}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4773}{\htmlId{4962}{\htmlClass{Bound}{\text{certSt'}}}}\,\,\htmlId{4969}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ in computeGov govΓ govSt (GovProposals+Votes stx) >>= λ where (govSt' , govStep) → success ( $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4672}{\htmlId{5130}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#5080}{\htmlId{5140}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4773}{\htmlId{5149}{\htmlClass{Bound}{\text{certSt'}}}}\, \end{pmatrix}$ , SUBLEDGER-V (isV , utxoStep , certStep , govStep)) ... | no ¬isV = let open SubLedgerEnv Γ; open LedgerState s isI : isTopLevelValid ≡ false isI = ¬-not ¬isV subUtxoΓ : SubUTxOEnv subUtxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1053}{\htmlId{5432}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1121}{\htmlId{5439}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1186}{\htmlId{5449}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1218}{\htmlId{5460}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1246}{\htmlId{5468}{\htmlClass{Function}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1274}{\htmlId{5486}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1306}{\htmlId{5499}{\htmlClass{Function}{\text{allData}}}}\, \end{pmatrix}$ in case computeSubutxow subUtxoΓ utxoSt stx of λ where (failure e) → failure e (success (utxoSt' , utxoStep)) → success ( $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#2503}{\htmlId{5665}{\htmlClass{Function}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2530}{\htmlId{5674}{\htmlClass{Function}{\text{govSt}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2556}{\htmlId{5682}{\htmlClass{Function}{\text{certState}}}}\, \end{pmatrix}$ , SUBLEDGER-I ( isI , subst (subUtxoΓ ⊢ utxoSt ⇀⦇ stx ,SUBUTXOW⦈_) (SUBUTXOW-noop isI utxoStep) utxoStep ))
completeness : (Γ : SubLedgerEnv) (s : LedgerState) (stx : SubLevelTx) (s' : LedgerState) → Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s' → (proj₁ <$> computeProof Γ s stx) ≡ success s'
completeness Γ s stx s' (SUBLEDGER-V {utxoState₁ = utxoSt₁} {certState₁ = certSt₁} {govState₁ = govSt₁} (isV , utxoStep , certStep , govStep)) with SubLedgerEnv.isTopLevelValid Γ ≟ true ... | no ¬isV = contradiction isV ¬isV ... | yes refl with computeSubutxow (subUtxoΓ Γ) (LedgerState.utxoSt s) stx | complete {STS = _⊢_⇀⦇_,SUBUTXOW⦈_} (subUtxoΓ Γ) (LedgerState.utxoSt s) stx utxoSt₁ utxoStep ... | success (utxoSt₁ , _) | refl with computeCerts (certΓ Γ s stx) (LedgerState.certState s) (DCertsOf stx) | complete {STS = _⊢_⇀⦇_,CERTS⦈_} (certΓ Γ s stx) (LedgerState.certState s) (DCertsOf stx) certSt₁ certStep ... | success (certSt₁ , _) | refl with computeGov (govΓ Γ stx certSt₁) (LedgerState.govSt s) (GovProposals+Votes stx) | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ Γ stx certSt₁) (LedgerState.govSt s) (GovProposals+Votes stx) govSt₁ govStep ... | success (govSt₁ , _) | refl = refl completeness Γ s stx s' (SUBLEDGER-I (isI , utxoStep)) with SubLedgerEnv.isTopLevelValid Γ ≟ true ... | yes isV = case trans (sym isV) isI of λ () ... | no ¬isV with computeSubutxow (subUtxoΓ Γ) (LedgerState.utxoSt s) stx | complete {STS = _⊢_⇀⦇_,SUBUTXOW⦈_} (subUtxoΓ Γ) (LedgerState.utxoSt s) stx (LedgerState.utxoSt s) utxoStep ... | success _ | refl = refl Computational-SUBLEDGERS : Computational _⊢_⇀⦇_,SUBLEDGERS⦈_ String Computational-SUBLEDGERS = it instance
Ledger: Computational¶
Computational-LEDGER : Computational _⊢_⇀⦇_,LEDGER⦈_ String
Computational-LEDGER = MkComputational computeProof completeness 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⦈_} -- Helper builders (avoid `let ... in with ...`) utxo₀Of : LedgerState → UTxO utxo₀Of s = UTxOOf (LedgerState.utxoSt s) allScriptsOf : TopLevelTx → LedgerState → ℙ Script allScriptsOf tx s = getAllScripts tx (utxo₀Of s) allDataOf : TopLevelTx → LedgerState → DataHash ⇀ Datum allDataOf tx s = setToMap (mapˢ < hash , id > (getAllData tx)) subΓOf : LedgerEnv → LedgerState → TopLevelTx → SubLedgerEnv subΓOf Γ s tx = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{8564}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8547}{\htmlId{8579}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1408}{\htmlId{8589}{\htmlClass{Field}{\text{LedgerEnv.ppolicy}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8547}{\htmlId{8607}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{8617}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8547}{\htmlId{8635}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{8645}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8547}{\htmlId{8666}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{8676}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8547}{\htmlId{8695}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8158}{\htmlId{8705}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8549}{\htmlId{8713}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13708}{\htmlId{8723}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8551}{\htmlId{8737}{\htmlClass{Bound}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8238}{\htmlId{8748}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8551}{\htmlId{8761}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8549}{\htmlId{8764}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8347}{\htmlId{8774}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8551}{\htmlId{8784}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8549}{\htmlId{8787}{\htmlClass{Bound}{\text{s}}}}\, \end{pmatrix}$ certΓOf : LedgerEnv → TopLevelTx → GovState → CertEnv certΓOf Γ tx govSt = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{8889}{\htmlClass{Function}{\text{epoch}}}}\, \,\htmlId{8895}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{8896}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8868}{\htmlId{8911}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{8912}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{8922}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8868}{\htmlId{8940}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12597}{\htmlId{8950}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8870}{\htmlId{8967}{\htmlClass{Bound}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2976}{\htmlId{8978}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8870}{\htmlId{8992}{\htmlClass{Bound}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5002}{\htmlId{9003}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8873}{\htmlId{9016}{\htmlClass{Bound}{\text{govSt}}}}\, \,\htmlId{9022}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{9023}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8868}{\htmlId{9044}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{9045}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ govΓOf : LedgerEnv → TopLevelTx → CertState → GovEnv govΓOf Γ tx certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11326}{\htmlId{9146}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9126}{\htmlId{9153}{\htmlClass{Bound}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{9164}{\htmlClass{Function}{\text{epoch}}}}\, \,\htmlId{9170}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{9171}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9124}{\htmlId{9186}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{9187}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{9197}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9124}{\htmlId{9215}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1408}{\htmlId{9225}{\htmlClass{Field}{\text{LedgerEnv.ppolicy}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9124}{\htmlId{9243}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{9253}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9124}{\htmlId{9274}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9129}{\htmlId{9284}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{9299}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{9303}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3713}{\htmlId{9304}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9129}{\htmlId{9314}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{9320}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ utxoΓ-valid : LedgerEnv → LedgerState → TopLevelTx → CertState → CertState → UTxOEnv utxoΓ-valid Γ s tx certSt₁ certSt₂ = let depositsChange = calculateDepositsChange (LedgerState.certState s) certSt₁ certSt₂ in $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{9565}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9436}{\htmlId{9580}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{9593}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9436}{\htmlId{9611}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{9624}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9436}{\htmlId{9643}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8158}{\htmlId{9656}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9438}{\htmlId{9664}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9471}{\htmlId{9677}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8238}{\htmlId{9703}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9440}{\htmlId{9716}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9438}{\htmlId{9719}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8347}{\htmlId{9732}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9440}{\htmlId{9742}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9438}{\htmlId{9745}{\htmlClass{Bound}{\text{s}}}}\, \end{pmatrix}$ utxoΓ-invalid : LedgerEnv → LedgerState → TopLevelTx → UTxOEnv utxoΓ-invalid Γ s tx = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{9861}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9844}{\htmlId{9876}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{9886}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9844}{\htmlId{9904}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{9914}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9844}{\htmlId{9933}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8158}{\htmlId{9943}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9846}{\htmlId{9951}{\htmlClass{Bound}{\text{s}}}}\, \\ \begin{pmatrix} \,\href{Data.Integer.Base.html#1545}{\htmlId{9963}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{9968}{\htmlClass{Function}{\text{0ℤ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8238}{\htmlId{9981}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9848}{\htmlId{9994}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9846}{\htmlId{9997}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8347}{\htmlId{10007}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9848}{\htmlId{10017}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9846}{\htmlId{10020}{\htmlClass{Bound}{\text{s}}}}\, \end{pmatrix}$
computeProof : (Γ : LedgerEnv) (s : LedgerState) (txTop : TopLevelTx) → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s')
computeProof Γ s txTop = let open LedgerEnv Γ open LedgerState s utxo₀ : UTxO utxo₀ = UTxOOf utxoSt allScripts : ℙ Script allScripts = getAllScripts txTop utxo₀ allData : DataHash ⇀ Datum allData = setToMap (mapˢ < hash , id > (getAllData txTop)) subΓ : SubLedgerEnv subΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{10585}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1408}{\htmlId{10592}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{10602}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{10612}{\htmlClass{Function}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{10625}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10304}{\htmlId{10652}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13708}{\htmlId{10660}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10230}{\htmlId{10674}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10359}{\htmlId{10682}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10440}{\htmlId{10695}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ in case IsValidFlagOf txTop ≟ true of λ where (yes isV) → computeSubledgers subΓ s (SubTransactionsOf txTop) >>= λ where (s₁ , subStep) → let open LedgerState s₁ renaming ( utxoSt to utxoSt₁ ; govSt to govSt₁ ; certState to certState₁ ) certΓ : CertEnv certΓ = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{11145}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{11151}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{11158}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12597}{\htmlId{11168}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10230}{\htmlId{11185}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2976}{\htmlId{11193}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10230}{\htmlId{11207}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5002}{\htmlId{11241}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11019}{\htmlId{11254}{\htmlClass{Function}{\text{govSt₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{11261}{\htmlClass{Function}{\text{enactState}}}}\, \end{pmatrix}$ in computeCerts certΓ certState₁ (DCertsOf txTop) >>= λ where (certSt₂ , certStep) → let govΓ : GovEnv govΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11326}{\htmlId{11470}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10230}{\htmlId{11477}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{11485}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{11491}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{11498}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1408}{\htmlId{11508}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{11518}{\htmlClass{Function}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11381}{\htmlId{11559}{\htmlClass{Bound}{\text{certSt₂}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{11569}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{11573}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3713}{\htmlId{11574}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11381}{\htmlId{11584}{\htmlClass{Bound}{\text{certSt₂}}}}\,\,\htmlId{11591}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ in computeGov govΓ govSt₁ (GovProposals+Votes txTop) >>= λ where (govSt₂ , govStep) → let certState₀ : CertState certState₀ = CertStateOf s depositsChange : DepositsChange depositsChange = calculateDepositsChange certState₀ certState₁ certSt₂ utxoΓ : UTxOEnv utxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{12072}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{12079}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{12089}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10304}{\htmlId{12100}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11865}{\htmlId{12108}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10359}{\htmlId{12125}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10440}{\htmlId{12138}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ in -- UTXOW must run from the post-SUBLEDGERS UTxOState (utxoSt₁) computeUtxow utxoΓ utxoSt₁ txTop >>= λ where (utxoSt₂ , utxoStep) → let finalGov = rmOrphanDRepVotes certSt₂ govSt₂ in success ( $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#12350}{\htmlId{12513}{\htmlClass{Bound}{\text{utxoSt₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#12402}{\htmlId{12523}{\htmlClass{Bound}{\text{finalGov}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11381}{\htmlId{12534}{\htmlClass{Bound}{\text{certSt₂}}}}\, \end{pmatrix}$ , LEDGER-V (isV , subStep , certStep , govStep , utxoStep)) (no ¬isV) → let isI : IsValidFlagOf txTop ≡ false isI = ¬-not ¬isV in case computeSubledgers (subΓOf Γ s txTop) s (SubTransactionsOf txTop) of λ where (failure e) → failure e (success (s₁ , subStep)) → computeUtxow (utxoΓ-invalid Γ s txTop) (LedgerState.utxoSt s) txTop >>= λ where (utxoSt₁ , utxoStep) → success ( $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#13019}{\htmlId{13071}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2530}{\htmlId{13081}{\htmlClass{Field}{\text{LedgerState.govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10228}{\htmlId{13099}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2556}{\htmlId{13103}{\htmlClass{Field}{\text{LedgerState.certState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10228}{\htmlId{13125}{\htmlClass{Bound}{\text{s}}}}\, \end{pmatrix}$ , LEDGER-I ( isI , subst (subΓOf Γ s txTop ⊢ s ⇀⦇ SubTransactionsOf txTop ,SUBLEDGERS⦈_) (SUBLEDGERS-noop isI subStep) subStep , utxoStep ))
completeness : (Γ : LedgerEnv) (s : LedgerState) (txTop : TopLevelTx) (s' : LedgerState) → Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s' → (proj₁ <$> computeProof Γ s txTop) ≡ success s'
completeness Γ s txTop s' (LEDGER-V {certState₁ = certSt₁} {certSt₂} {utxoState₁ = utxoSt₁} {govSt₁} {govSt₂} {utxoSt₂} (isV , subStep , certStep , govStep , utxoStep)) with IsValidFlagOf txTop ≟ true ... | no ¬isV = contradiction isV ¬isV ... | yes refl with computeSubledgers (subΓOf Γ s txTop) s (SubTransactionsOf txTop) | complete {STS = _⊢_⇀⦇_,SUBLEDGERS⦈_} (subΓOf Γ s txTop) s (SubTransactionsOf txTop) ($\begin{pmatrix} \,\htmlId{14185}{\htmlClass{Bound}{\text{utxoSt₁}}}\, \\ \,\htmlId{14195}{\htmlClass{Bound}{\text{govSt₁}}}\, \\ \,\htmlId{14204}{\htmlClass{Bound}{\text{certSt₁}}}\, \end{pmatrix}$) subStep ... | success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#14245}{\htmlId{14245}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#14255}{\htmlId{14255}{\htmlClass{Bound}{\text{govSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#14264}{\htmlId{14264}{\htmlClass{Bound}{\text{certSt₁}}}}\, \end{pmatrix}$ , _) | refl with computeCerts (certΓOf Γ txTop govSt₁) certSt₁ (DCertsOf txTop) | complete {STS = _⊢_⇀⦇_,CERTS⦈_} (certΓOf Γ txTop govSt₁) certSt₁ (DCertsOf txTop) certSt₂ certStep ... | success (certSt₂ , _) | refl with computeGov (govΓOf Γ txTop certSt₂) govSt₁ (GovProposals+Votes txTop) | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓOf Γ txTop certSt₂) govSt₁ (GovProposals+Votes txTop) govSt₂ govStep ... | success (govSt₂ , _) | refl with computeUtxow (utxoΓ-valid Γ s txTop certSt₁ certSt₂) utxoSt₁ txTop | complete {STS = _⊢_⇀⦇_,UTXOW⦈_} (utxoΓ-valid Γ s txTop certSt₁ certSt₂) utxoSt₁ txTop utxoSt₂ utxoStep ... | success (utxoSt₂ , _) | refl = refl completeness Γ s txTop s' (LEDGER-I {utxoState₁ = utxoSt₁} (isI , subStep , utxoStep)) with IsValidFlagOf txTop ≟ true ... | yes isV = case trans (sym isV) isI of λ () ... | no ¬isV with computeSubledgers (subΓOf Γ s txTop) s (SubTransactionsOf txTop) | complete {STS = _⊢_⇀⦇_,SUBLEDGERS⦈_} (subΓOf Γ s txTop) s (SubTransactionsOf txTop) s subStep ... | success _ | refl with computeUtxow (utxoΓ-invalid Γ s txTop) (LedgerState.utxoSt s) txTop | complete {STS = _⊢_⇀⦇_,UTXOW⦈_} (utxoΓ-invalid Γ s txTop) (LedgerState.utxoSt s) txTop utxoSt₁ utxoStep ... | success _ | refl = refl Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String Computational-LEDGERS = it