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#12712}{\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#11441}{\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#3324}{\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#12712}{\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#11441}{\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#3324}{\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 (utxo₀Of s))) subΓOf : LedgerEnv → LedgerState → TopLevelTx → SubLedgerEnv subΓOf Γ s tx = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{8576}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8559}{\htmlId{8591}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1408}{\htmlId{8601}{\htmlClass{Field}{\text{LedgerEnv.ppolicy}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8559}{\htmlId{8619}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{8629}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8559}{\htmlId{8647}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{8657}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8559}{\htmlId{8678}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{8688}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8559}{\htmlId{8707}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8158}{\htmlId{8717}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8561}{\htmlId{8725}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13837}{\htmlId{8735}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8563}{\htmlId{8749}{\htmlClass{Bound}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8238}{\htmlId{8760}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8563}{\htmlId{8773}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8561}{\htmlId{8776}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8347}{\htmlId{8786}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8563}{\htmlId{8796}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8561}{\htmlId{8799}{\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{8901}{\htmlClass{Function}{\text{epoch}}}}\, \,\htmlId{8907}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{8908}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8880}{\htmlId{8923}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{8924}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{8934}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8880}{\htmlId{8952}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12712}{\htmlId{8962}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8882}{\htmlId{8979}{\htmlClass{Bound}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2976}{\htmlId{8990}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8882}{\htmlId{9004}{\htmlClass{Bound}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5002}{\htmlId{9015}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8885}{\htmlId{9028}{\htmlClass{Bound}{\text{govSt}}}}\, \,\htmlId{9034}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{9035}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8880}{\htmlId{9056}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{9057}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ govΓOf : LedgerEnv → TopLevelTx → CertState → GovEnv govΓOf Γ tx certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11441}{\htmlId{9158}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9138}{\htmlId{9165}{\htmlClass{Bound}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{9176}{\htmlClass{Function}{\text{epoch}}}}\, \,\htmlId{9182}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{9183}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9136}{\htmlId{9198}{\htmlClass{Bound}{\text{Γ}}}}\,\,\htmlId{9199}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{9209}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9136}{\htmlId{9227}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1408}{\htmlId{9237}{\htmlClass{Field}{\text{LedgerEnv.ppolicy}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9136}{\htmlId{9255}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{9265}{\htmlClass{Field}{\text{LedgerEnv.enactState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9136}{\htmlId{9286}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9141}{\htmlId{9296}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{9311}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{9315}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3324}{\htmlId{9316}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9141}{\htmlId{9326}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{9332}{\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{9577}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9448}{\htmlId{9592}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{9605}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9448}{\htmlId{9623}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{9636}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9448}{\htmlId{9655}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8158}{\htmlId{9668}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9450}{\htmlId{9676}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9483}{\htmlId{9689}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8238}{\htmlId{9715}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9452}{\htmlId{9728}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9450}{\htmlId{9731}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8347}{\htmlId{9744}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9452}{\htmlId{9754}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9450}{\htmlId{9757}{\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{9873}{\htmlClass{Field}{\text{LedgerEnv.slot}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9856}{\htmlId{9888}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{9898}{\htmlClass{Field}{\text{LedgerEnv.pparams}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9856}{\htmlId{9916}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{9926}{\htmlClass{Field}{\text{LedgerEnv.treasury}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9856}{\htmlId{9945}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8158}{\htmlId{9955}{\htmlClass{Function}{\text{utxo₀Of}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9858}{\htmlId{9963}{\htmlClass{Bound}{\text{s}}}}\, \\ \begin{pmatrix} \,\href{Data.Integer.Base.html#1545}{\htmlId{9975}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{9980}{\htmlClass{Function}{\text{0ℤ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8238}{\htmlId{9993}{\htmlClass{Function}{\text{allScriptsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9860}{\htmlId{10006}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9858}{\htmlId{10009}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#8347}{\htmlId{10019}{\htmlClass{Function}{\text{allDataOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9860}{\htmlId{10029}{\htmlClass{Bound}{\text{tx}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9858}{\htmlId{10032}{\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 utxo₀)) subΓ : SubLedgerEnv subΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{10603}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1408}{\htmlId{10610}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{10620}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{10630}{\htmlClass{Function}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{10643}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10316}{\htmlId{10670}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#13837}{\htmlId{10678}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10242}{\htmlId{10692}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10371}{\htmlId{10700}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10452}{\htmlId{10713}{\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{11163}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{11169}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{11176}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12712}{\htmlId{11186}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10242}{\htmlId{11203}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2976}{\htmlId{11211}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10242}{\htmlId{11225}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5002}{\htmlId{11259}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11037}{\htmlId{11272}{\htmlClass{Function}{\text{govSt₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{11279}{\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#11441}{\htmlId{11488}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10242}{\htmlId{11495}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{11503}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1385}{\htmlId{11509}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{11516}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1408}{\htmlId{11526}{\htmlClass{Function}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1469}{\htmlId{11536}{\htmlClass{Function}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11399}{\htmlId{11577}{\htmlClass{Bound}{\text{certSt₂}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{11587}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{11591}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3324}{\htmlId{11592}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11399}{\htmlId{11602}{\htmlClass{Bound}{\text{certSt₂}}}}\,\,\htmlId{11609}{\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{12090}{\htmlClass{Function}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1443}{\htmlId{12097}{\htmlClass{Function}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{12107}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10316}{\htmlId{12118}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11883}{\htmlId{12126}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10371}{\htmlId{12143}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10452}{\htmlId{12156}{\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#12368}{\htmlId{12531}{\htmlClass{Bound}{\text{utxoSt₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#12420}{\htmlId{12541}{\htmlClass{Bound}{\text{finalGov}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#11399}{\htmlId{12552}{\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#13037}{\htmlId{13089}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2530}{\htmlId{13099}{\htmlClass{Field}{\text{LedgerState.govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10240}{\htmlId{13117}{\htmlClass{Bound}{\text{s}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#2556}{\htmlId{13121}{\htmlClass{Field}{\text{LedgerState.certState}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10240}{\htmlId{13143}{\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{14203}{\htmlClass{Bound}{\text{utxoSt₁}}}\, \\ \,\htmlId{14213}{\htmlClass{Bound}{\text{govSt₁}}}\, \\ \,\htmlId{14222}{\htmlClass{Bound}{\text{certSt₁}}}\, \end{pmatrix}$) subStep ... | success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#14263}{\htmlId{14263}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#14273}{\htmlId{14273}{\htmlClass{Bound}{\text{govSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#14282}{\htmlId{14282}{\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