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 _ SUBLEDGERS-[] = refl SUBLEDGERS-noop isI (SUBLEDGERS-∷ 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#1210}{\htmlId{4339}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1278}{\htmlId{4346}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1343}{\htmlId{4356}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1375}{\htmlId{4367}{\htmlClass{Field}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1434}{\htmlId{4375}{\htmlClass{Field}{\text{pState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1464}{\htmlId{4385}{\htmlClass{Field}{\text{precedingDCerts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1498}{\htmlId{4403}{\htmlClass{Field}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1530}{\htmlId{4416}{\htmlClass{Field}{\text{isTopLevelValid}}}}\, \end{pmatrix}$ subentitiesΓ : SubEntitiesEnv subentitiesΓ = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{4494}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1210}{\htmlId{4500}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1278}{\htmlId{4507}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5214}{\htmlId{4517}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#2742}{\htmlId{4530}{\htmlClass{Field}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1309}{\htmlId{4536}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1403}{\htmlId{4549}{\htmlClass{Field}{\text{rewards₀}}}}\, \end{pmatrix}$ govΓ : CertState → GovEnv govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11562}{\htmlId{4616}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4261}{\htmlId{4623}{\htmlClass{Bound}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{4629}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1210}{\htmlId{4635}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1278}{\htmlId{4642}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1238}{\htmlId{4652}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1309}{\htmlId{4662}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4605}{\htmlId{4675}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{4684}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{4688}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#7094}{\htmlId{4689}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#4605}{\htmlId{4699}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{4705}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s')
computeProof = case isTopLevelValid ≟ true of λ where (yes p) → do (certSt' , certStep) ← computeSubentities subentitiesΓ certState stx (govSt' , govStep) ← computeGov (govΓ certSt') govSt (GovProposals+Votes stx) (utxoSt' , utxoStep) ← computeSubutxow subUtxoΓ utxoSt stx success (_ , SUBLEDGER-V (p , certStep , govStep , utxoStep )) (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 , certStep , govStep , utxoStep)) with isTopLevelValid ≟ true ... | no ¬v = contradiction v ¬v ... | yes 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 with computeSubutxow subUtxoΓ utxoSt stx | completeSubutxow _ _ _ _ utxoStep ... | success (utxoSt' , _) | 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 instance
Computational-SUBLEDGERS : Computational _⊢_⇀⦇_,SUBLEDGERS⦈_ String
Computational-SUBLEDGERS = record {go} where open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete) opaque computeSubLedger : ∀ Γ s x → ComputationResult String (∃ λ s' → Γ ⊢ s ⇀⦇ x ,SUBLEDGER⦈ s') computeSubLedger = comp {STS = _⊢_⇀⦇_,SUBLEDGER⦈_} completeSubLedger : ∀ Γ s x s' → Γ ⊢ s ⇀⦇ x ,SUBLEDGER⦈ s' → (proj₁ <$> computeSubLedger Γ s x) ≡ success s' completeSubLedger = complete {STS = _⊢_⇀⦇_,SUBLEDGER⦈_} module go where computeProof : ∀ (Γ : SubLedgerEnv) (s : LedgerState) (stxs : List SubLevelTx) → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ stxs ,SUBLEDGERS⦈ s') computeProof Γ s [] = success (s , SUBLEDGERS-[]) computeProof Γ s (stx ∷ stxs) = do (s' , p) ← computeSubLedger Γ s stx (s'' , q) ← computeProof (record Γ { precedingDCerts = SubLedgerEnv.precedingDCerts Γ ++ DCertsOf stx }) s' stxs success (s'' , SUBLEDGERS-∷ p q) completeness : ∀ (Γ : SubLedgerEnv) (s : LedgerState) (stxs : List SubLevelTx) (s' : LedgerState) → Γ ⊢ s ⇀⦇ stxs ,SUBLEDGERS⦈ s' → (proj₁ <$> computeProof Γ s stxs) ≡ success s' completeness Γ s [] s' SUBLEDGERS-[] = refl completeness Γ s (stx ∷ stxs) s' (SUBLEDGERS-∷ p q) with computeSubLedger Γ s stx | completeSubLedger _ _ _ _ p ... | success (s' , _) | refl with computeProof (record Γ { precedingDCerts = SubLedgerEnv.precedingDCerts Γ ++ DCertsOf stx }) s' stxs | completeness _ _ _ _ q ... | success (_ , _) | refl = refl 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 pState₀ : PState pState₀ = PStateOf certState allScripts : ℙ Script allScripts = getAllScripts txTop utxo₀ legacyMode : Bool legacyMode = isLegacyMode utxo₀ allScripts txTop subΓ : SubLedgerEnv subΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1597}{\htmlId{10290}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1620}{\htmlId{10297}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1655}{\htmlId{10307}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1681}{\htmlId{10317}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1710}{\htmlId{10330}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9994}{\htmlId{10341}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7094}{\htmlId{10349}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\htmlId{10359}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#7766}{\htmlId{10360}{\htmlClass{Field}{\text{CertStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9903}{\htmlId{10372}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{10373}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10042}{\htmlId{10377}{\htmlClass{Function}{\text{pState₀}}}}\, \\ \,\href{Agda.Builtin.List.html#184}{\htmlId{10387}{\htmlClass{InductiveConstructor}{\text{[]}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10101}{\htmlId{10392}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#14431}{\htmlId{10405}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9956}{\htmlId{10419}{\htmlClass{Bound}{\text{txTop}}}}\, \end{pmatrix}$ entitiesΓ : GovState → CertState → EntitiesEnv entitiesΓ govSt certSt = $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{10514}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1597}{\htmlId{10520}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1655}{\htmlId{10527}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5214}{\htmlId{10537}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10497}{\htmlId{10550}{\htmlClass{Bound}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1681}{\htmlId{10556}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10175}{\htmlId{10569}{\htmlClass{Function}{\text{legacyMode}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7094}{\htmlId{10582}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10503}{\htmlId{10592}{\htmlClass{Bound}{\text{certSt}}}}\, \end{pmatrix}$ govΓ : CertState → GovEnv govΓ certSt = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#11562}{\htmlId{10656}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9956}{\htmlId{10663}{\htmlClass{Bound}{\text{txTop}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{10671}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#1597}{\htmlId{10677}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1655}{\htmlId{10684}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1620}{\htmlId{10694}{\htmlClass{Field}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1681}{\htmlId{10704}{\htmlClass{Field}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10645}{\htmlId{10717}{\htmlClass{Bound}{\text{certSt}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{10726}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{10730}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#7094}{\htmlId{10731}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10645}{\htmlId{10741}{\htmlClass{Bound}{\text{certSt}}}}\,\,\htmlId{10747}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ utxoΓ : UTxOEnv utxoΓ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#1597}{\htmlId{10790}{\htmlClass{Field}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1655}{\htmlId{10797}{\htmlClass{Field}{\text{pparams}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#1710}{\htmlId{10807}{\htmlClass{Field}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#9994}{\htmlId{10818}{\htmlClass{Function}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10042}{\htmlId{10826}{\htmlClass{Function}{\text{pState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10101}{\htmlId{10836}{\htmlClass{Function}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#10175}{\htmlId{10849}{\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{12476}{\htmlClass{Bound}{\text{utxoSt₁}}}\, \\ \,\htmlId{12486}{\htmlClass{Bound}{\text{govSt₁}}}\, \\ \,\htmlId{12495}{\htmlClass{Bound}{\text{certSt₁}}}\, \end{pmatrix}$) subStep ... | success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#12538}{\htmlId{12538}{\htmlClass{Bound}{\text{utxoSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#12548}{\htmlId{12548}{\htmlClass{Bound}{\text{govSt₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.Properties.Computational.html#12557}{\htmlId{12557}{\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