Computational
{-# OPTIONS --safe #-}
open import Ledger.Dijkstra.Specification.Abstract
open import Ledger.Dijkstra.Specification.Transaction
module Ledger.Dijkstra.Specification.Utxo.Properties.Computational
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where
open import Prelude
open import Ledger.Prelude
open import stdlib-meta.Tactic.GenError using (genErrors)
open import Ledger.Dijkstra.Specification.Utxo txs abs
open import Ledger.Dijkstra.Specification.Script.Validation txs abs
open import Relation.Binary.PropositionalEquality
import Data.Sum.Relation.Unary.All as Sum
open PParams
instance
_ = Functor-ComputationResult
instance
Computational-SUBUTXO : Computational _⊢_⇀⦇_,SUBUTXO⦈_ String
Computational-SUBUTXO = record {go} where
module go (Γ : SubUTxOEnv) (s₀ : UTxOState) (txSub : SubLevelTx)
(let H , ⁇ H? = SUBUTXO-premises {txSub = txSub} {Γ = Γ} {s₀ = s₀})
where
computeProof : ComputationResult String (Σ UTxOState (_⊢_⇀⦇_,SUBUTXO⦈_ Γ s₀ txSub))
computeProof
with IsTopLevelValidFlagOf Γ | inspect IsTopLevelValidFlagOf Γ
... | false | [ refl ]
with H?
... | (yes p) = success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#5761}{\htmlId{1386}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#1004}{\htmlId{1393}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{1398}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#1004}{\htmlId{1405}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{1410}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#1004}{\htmlId{1422}{\htmlClass{Bound}{\text{s₀}}}}\, \end{pmatrix}$ , SUBUTXO {txSub = txSub} p)
... | (no ¬p) = failure "genErrors"
computeProof | true | [ refl ]
with H?
... | (yes p) = success ( $\begin{pmatrix} \,\htmlId{1603}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5761}{\htmlId{1604}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#1004}{\htmlId{1611}{\htmlClass{Bound}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{1614}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#11809}{\htmlId{1616}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#1021}{\htmlId{1630}{\htmlClass{Bound}{\text{txSub}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{1636}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{1637}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{1639}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7810}{\htmlId{1642}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#1021}{\htmlId{1647}{\htmlClass{Bound}{\text{txSub}}}}\,
\\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{1688}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#1004}{\htmlId{1695}{\htmlClass{Bound}{\text{s₀}}}}\,
\\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{1732}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#1004}{\htmlId{1744}{\htmlClass{Bound}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1747}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#650}{\htmlId{1749}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#1021}{\htmlId{1761}{\htmlClass{Bound}{\text{txSub}}}}\,
\end{pmatrix}$
, SUBUTXO {txSub = txSub} p
)
... | (no ¬p) = failure "genErrors"
completeness : ∀ s₁ → Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXO⦈ s₁ → map proj₁ computeProof ≡ success s₁
completeness s₁ (SUBUTXO p)
with IsTopLevelValidFlagOf Γ | inspect IsTopLevelValidFlagOf Γ
... | false | [ refl ]
with H?
... | (yes p) = refl
... | (no ¬p) = ⊥-elim (¬p p)
completeness s₁ (SUBUTXO p) | true | [ refl ]
with H?
... | (yes p) = refl
... | (no ¬p) = ⊥-elim (¬p p)
Computational-UTXOS : Computational _⊢_⇀⦇_,UTXOS⦈_ String
Computational-UTXOS = MkComputational computeProof completeness
where
computeProof : (Γ : UTxOEnv) (_ : ⊤) (txTop : TopLevelTx)
→ ComputationResult String (Σ ⊤ (Γ ⊢ tt ⇀⦇ txTop ,UTXOS⦈_))
computeProof Γ _ txTop
with ¿ evalP2Scripts (allP2ScriptsWithContext Γ txTop) ≡ IsValidFlagOf txTop ¿
... | yes p = success (tt , UTXOS p)
... | no ¬p = failure (genErrors ¬p)
completeness : (Γ : UTxOEnv) (_ : ⊤) (txTop : TopLevelTx) (_ : ⊤)
→ Γ ⊢ tt ⇀⦇ txTop ,UTXOS⦈ tt
→ (map proj₁ $ computeProof Γ _ txTop) ≡ success tt
completeness Γ _ txTop _ (UTXOS p)
with ¿ evalP2Scripts (allP2ScriptsWithContext Γ txTop) ≡ IsValidFlagOf txTop ¿
... | yes p = refl
... | no ¬p = ⊥-elim (¬p p)
Computational-UTXO : Computational _⊢_⇀⦇_,UTXO⦈_ String
<!--
Computational-UTXOInductiveConstructor"> =="5981" href="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#5981" class="Bound"> recordion.Utxo.Properties.Computational.html#5981" class="Bound"> {html#5981" class="Bound">gos="Function">}93" class="Symbol"> whereef="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#5981" class="Bound">
modulea> goiveConstructor"> (0" class="Symbol">Γ,legacyMode.html#13350" class="Function"> :S.computeProof UTxOEnvfication.Utxo.Properties.Computational.html#3795" class="Bound"> × Boolml#636" class="Field">) id="6174" class="Symbol"> ( id="6176" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">s₀kstra.Specification.Utxo.Properties.Computational.html#3844" class="Bound"> :s.Computational.html#3844" class="Bound"> UTxOState87" href="Interface.ComputationalRelation.html#13567" class="Function">)Relation.html#13567" class="Function"> (on">txTop="Symbol"> :="Symbol"> TopLevelTxclass="Symbol">) href="Interface.ComputationalRelation.html#10518" class="InductiveConstructor">
(">letace.ComputationalRelation.html#13350" class="Function"> H> ,lass="Bound"> ⁇.Base.html#636" class="Field"> H?tml#212" class="InductiveConstructor"> =or"> UTXO-premisesclass="Bound"> {5" class="Symbol">txTopef="Interface.ComputationalRelation.html#13567" class="Function"> =n.html#13567" class="Function"> txTop">}l"> {l">Γ> =ymbol"> proj₁erface.ComputationalRelation.html#10518" class="InductiveConstructor"> Γ,legacyModeification.Utxo.Properties.Computational.html#6236" class="Bound">}tional.html#6236" class="Bound"> {/a>s₀> =Equality.html#207" class="InductiveConstructor"> s₀gda.Builtin.Equality.html#207" class="InductiveConstructor">}ass="InductiveConstructor"> {>legacyMode = proj₂ Γ,legacyMode})
where>
module UTXOS = Computational Computational-UTXOS
computeProof : ComputationResult String (∃[ s₁ ] Γ,legacyMode ⊢ s₀ ⇀⦇ txTop ,UTXO⦈ s₁)
computeProof
with IsValidFlagOf txTop | inspect IsValidFlagOf txTop
... | false | [ refl ]
with H?
... | (no ¬p) = failure "UTXO"
... | yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)
with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop
... | success h = success (-, UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , proj₂ h))
... | failure ¬h = failure "UTXOS"
computeProof | true | [ refl ]
with H?
... | (no ¬p) = failure "UTXO"
... | yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)
with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop
... | success h = success (-, UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , proj₂ h))
... | failure ¬h = failure "UTXOS"
completeness : ∀ s₁ → Γ,legacyMode ⊢ s₀ ⇀⦇ txTop ,UTXO⦈ s₁ → map proj₁ computeProof ≡ success s₁
completeness s₁ (UTXO-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ p₁₇ p₁₈ h)
with IsValidFlagOf txTop | inspect IsValidFlagOf txTop
... | false | [ refl ]
with H?
... | no ¬p = ⊥-elim (¬p ((p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)))
... | yes _
with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop | UTXOS.completeness _ _ _ _ h
... | success h | refl = refl
completeness s₁ (UTXO-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ p₁₇ p₁₈ h) | true | [ refl ]
with H?
... | no ¬p = ⊥-elim (¬p ((p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)))
... | yes _
with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop | UTXOS.completeness _ _ _ _ h
... | success h | refl = refl