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#5756}{\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#5756}{\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#11706}{\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#7717}{\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-UTXOef="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#5916" class="Bound"> =Utxo.Properties.Computational.html#5916" class="Bound"> record class="Bound"> { class="Symbol">gotor">}="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#5927" class="Bound"> whereoperties.Computational.html#5927" class="Bound">
moduleth go? (mbol">Γ,legacyModeuctiveConstructor"> :075" href="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#6075" class="Bound"> UTxOEnvnd"> ×1069" class="Function"> Bool"6088" href="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#6075" class="Bound">)ification.Utxo.Properties.Computational.html#6075" class="Bound"> (ional.html#6075" class="Bound">s₀d="6096" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator"> :html#235" class="InductiveConstructor Operator"> UTxOState"6101" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">)tml#235" class="InductiveConstructor Operator"> (or Operator">txToptiveConstructor Operator"> : id="6108" class="Bound"> TopLevelTxtor Operator">)class="Bound">
(..let H6075" href="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#6075" class="Bound"> ,und"> ⁇Function"> H?perties.Computational.html#6075" class="Bound"> =lass="Bound"> UTXO-premiseshref="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator"> { class="InductiveConstructor Operator">txTop, =₁ txTopss="Bound">}ef="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator"> {lass="InductiveConstructor Operator">Γ"> => proj₁eConstructor Operator"> Γ,legacyModeuctiveConstructor Operator">} { s₀ma.html#235" class="InductiveConstructor Operator"> =ructor Operator"> s₀"InductiveConstructor Operator">} {legacyModetml#235" class="InductiveConstructor Operator"> =or Operator"> proj₂"Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator"> Γ,legacyModehref="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">}) class="InductiveConstructor Operator">
where>
module UTXOSonstructor"> =8" href="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#6348" class="Bound"> Computational/a> Computational-UTXOSd="6357" class="Symbol">
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₁₈ , 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₁₈ , 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₁₈ , 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₁₈ , 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₁₈ 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₁₈ , 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₁₈ 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₁₈ , p₁₉ , p₂₀ , p₂₁)))
... | yes _
with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop | UTXOS.completeness _ _ _ _ h
... | success h | refl = refl