{-# 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 where
computeProof : (Γ : SubUTxOEnv) (s : UTxOState) (txSub : SubLevelTx)
→ ComputationResult String (Σ UTxOState (_⊢_⇀⦇_,SUBUTXO⦈_ Γ s txSub))
computeProof Γ s txSub
with IsTopLevelValidFlagOf Γ | inspect IsTopLevelValidFlagOf Γ
... | false | [ refl ]
with ¿ SpendInputsOf txSub ≢ ∅
× inInterval (SlotOf Γ) (ValidIntervalOf txSub)
× MaybeNetworkIdOf txSub ~ just NetworkId ¿
... | (yes p) = success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#3518}{\htmlId{1502}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{1509}{\htmlClass{Bound}{\text{s}}}\, \\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{1513}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\htmlId{1520}{\htmlClass{Bound}{\text{s}}}\, \\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{1524}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{1536}{\htmlClass{Bound}{\text{s}}}\, \end{pmatrix}$ , SUBUTXO {txSub = txSub} p)
... | (no ¬p) = failure (genErrors ¬p)
computeProof Γ s txSub | true | [ refl ]
with ¿ SpendInputsOf txSub ≢ ∅
× inInterval (SlotOf Γ) (ValidIntervalOf txSub)
× MaybeNetworkIdOf txSub ~ just NetworkId ¿
... | (yes p) = success ( $\begin{pmatrix} \,\htmlId{1853}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#3518}{\htmlId{1854}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{1861}{\htmlClass{Bound}{\text{s}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{1863}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#7269}{\htmlId{1865}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\htmlId{1879}{\htmlClass{Bound}{\text{txSub}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{1885}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{1886}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{1888}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4820}{\htmlId{1891}{\htmlClass{Function}{\text{outs}}}}\, \,\htmlId{1896}{\htmlClass{Bound}{\text{txSub}}}\,
\\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{1936}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\htmlId{1943}{\htmlClass{Bound}{\text{s}}}\,
\\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{1979}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{1991}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1993}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#554}{\htmlId{1995}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{2007}{\htmlClass{Bound}{\text{txSub}}}\,
\end{pmatrix}$
, SUBUTXO {txSub = txSub} p
)
... | (no ¬p) = failure (genErrors ¬p)
completeness : (Γ : SubUTxOEnv) (s : UTxOState) (txSub : SubLevelTx)
→ ∀ s' → Γ ⊢ s ⇀⦇ txSub ,SUBUTXO⦈ s' → map proj₁ (computeProof Γ s txSub) ≡ success s'
completeness Γ s txSub s' (SUBUTXO p)
with IsTopLevelValidFlagOf Γ | inspect IsTopLevelValidFlagOf Γ
... | false | [ refl ]
with ¿ SpendInputsOf txSub ≢ ∅
× inInterval (SlotOf Γ) (ValidIntervalOf txSub)
× MaybeNetworkIdOf txSub ~ just NetworkId ¿
... | (yes p) = refl
... | (no ¬p) = ⊥-elim (¬p p)
completeness Γ s txSub s' (SUBUTXO p) | true | [ refl ]
with ¿ SpendInputsOf txSub ≢ ∅
× inInterval (SlotOf Γ) (ValidIntervalOf txSub)
× MaybeNetworkIdOf txSub ~ just NetworkId ¿
... | (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-UTXO = MkComputational computeProof completeness
where
open Computational Computational-UTXOS renaming ( computeProof to computeProof-UTXOS
; completeness to completeness-UTXOS)
genErr-prem : (Γ×lm : UTxOEnv × Bool)(s₀ : UTxOState)(txTop : TopLevelTx)
→ ¬ (UTXO-Premises Γ×lm s₀ txTop) → String
genErr-prem Γ×lm s₀ txTop ¬p = case dec-de-morgan ¬p of λ where
(inj₁ _) → "¬ (SpendInputsOf txTop ≢ ∅)"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (inInterval (SlotOf Γ) (ValidIntervalOf txTop))"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (minfee (PParamsOf Γ) txTop (UTxOOf s₀) ≤ TxFeesOf txTop)"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (consumedBatch (DepositsChangeOf Γ) txTop (UTxOOf Γ) ≡ producedBatch (DepositsChangeOf Γ) txTop)"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (legacyMode ≡ true → consumed (DepositsChangeOf Γ) txTop (UTxOOf Γ) ≡ produced (DepositsChangeOf Γ) txTop)"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (SizeOf txTop ≤ maxTxSize (PParamsOf Γ))"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (refScriptsSize txTop (UTxOOf Γ) ≤ (PParamsOf Γ) .maxRefScriptSizePerTx)"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (allSpendInputs txTop ⊆ dom (UTxOOf Γ))"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (allReferenceInputs txTop ⊆ dom (UTxOOf Γ))"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (NoOverlappingSpendInputs txTop)"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ ((RedeemersOf txTop ˢ ≢ ∅) → collateralCheck (PParamsOf Γ) txTop (UTxOOf Γ))"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (allMintedCoin txTop ≡ 0)"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (∀[ (_ , o) ∈ ∣ TxOutsOf txTop ∣ ] ( (inject ((160 + utxoEntrySize o) * coinsPerUTxOByte (PParamsOf Γ)) ≤ᵗ txOutToValue o) × (serializedSize (txOutToValue o) ≤ maxValSize (PParamsOf Γ)) ))"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (∀[ (a , _) ∈ range (TxOutsOf txTop) ] ( ((Sum.All (const ⊤) (λ a → AttrSizeOf a ≤ 64)) a) × (netId a ≡ NetworkId) ))"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (∀[ a ∈ dom (WithdrawalsOf txTop)] NetworkIdOf a ≡ NetworkId)"
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ _) → "¬ (MaybeNetworkIdOf txTop ~ just NetworkId)"
(inj₂ b) → "¬ (CurrentTreasuryOf txTop ~ just (TreasuryOf Γ))"
computeProof : (Γ×lm : UTxOEnv × Bool) (s : UTxOState) (txTop : TopLevelTx)
→ ComputationResult String (∃[ s' ] Γ×lm ⊢ s ⇀⦇ txTop ,UTXO⦈ s')
computeProof (Γ , lm) s txTop
with IsValidFlagOf txTop in isValid | computeProof-UTXOS Γ tt txTop | ¿ UTXO-Premises (Γ , lm) s txTop ¿
... | true | success (tt , utxosProof) | yes prem = success ( $\begin{pmatrix} \,\htmlId{8398}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#3518}{\htmlId{8399}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{8406}{\htmlClass{Bound}{\text{s}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8408}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#7269}{\htmlId{8410}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\htmlId{8424}{\htmlClass{Bound}{\text{txTop}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8430}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{8431}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{8433}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4820}{\htmlId{8436}{\htmlClass{Function}{\text{outs}}}}\, \,\htmlId{8441}{\htmlClass{Bound}{\text{txTop}}}\,
\\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{8520}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\htmlId{8527}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8529}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#6330}{\htmlId{8531}{\htmlClass{Field}{\text{TxFeesOf}}}}\, \,\htmlId{8540}{\htmlClass{Bound}{\text{txTop}}}\,
\\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{8619}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{8631}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8633}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#554}{\htmlId{8635}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{8647}{\htmlClass{Bound}{\text{txTop}}}\,
\end{pmatrix}$
, UTXO-valid (isValid , utxosProof , prem )
)
... | false | success (tt , utxosProof) | yes prem = success ( $\begin{pmatrix} \,\htmlId{8983}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#3518}{\htmlId{8984}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{8991}{\htmlClass{Bound}{\text{s}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8993}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#6165}{\htmlId{8995}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\htmlId{9014}{\htmlClass{Bound}{\text{txTop}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9020}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{9021}{\htmlClass{Symbol}{\text{)}}}\,
\\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{9096}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\htmlId{9103}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9105}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4957}{\htmlId{9107}{\htmlClass{Function}{\text{cbalance}}}}\, \,\htmlId{9116}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#3518}{\htmlId{9117}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{9124}{\htmlClass{Bound}{\text{s}}}\, \,\href{Axiom.Set.Map.html#13536}{\htmlId{9126}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#6165}{\htmlId{9128}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\htmlId{9147}{\htmlClass{Bound}{\text{txTop}}}\,\,\htmlId{9152}{\htmlClass{Symbol}{\text{)}}}\,
\\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{9227}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{9239}{\htmlClass{Bound}{\text{s}}}\,
\end{pmatrix}$
, UTXO-invalid (isValid , utxosProof , prem)
)
... | _ | _ | no ¬prem = failure (genErr-prem (Γ , lm) s txTop ¬prem)
... | _ | failure es | _ = failure es
completeness : (Γ×lm : UTxOEnv × Bool) (s : UTxOState) (txTop : TopLevelTx)
→ ∀ s' → Γ×lm ⊢ s ⇀⦇ txTop ,UTXO⦈ s' → (map proj₁ $ computeProof Γ×lm s txTop) ≡ success s'
completeness (Γ , lm) s txTop s' (UTXO-valid (refl , h-utxos , h-prem))
with computeProof-UTXOS Γ tt txTop in eqU | ¿ UTXO-Premises (Γ , lm) s txTop ¿
... | success (tt , utxosProof) | yes prem = refl
... | success (tt , utxosProof) | no ¬prem = ⊥-elim (¬prem h-prem)
... | failure es | _ = ⊥-elim $ case trans (sym (map-failure {f = proj₁} eqU))
(completeness-UTXOS Γ tt txTop tt h-utxos)
of λ ()
completeness (Γ , lm) s txTop s' (UTXO-invalid (refl , h-utxos , h-prem))
with computeProof-UTXOS Γ tt txTop in eqU | ¿ UTXO-Premises (Γ , lm) s txTop ¿
... | success (tt , utxosProof) | yes prem = refl
... | success (tt , utxosProof) | no ¬prem = ⊥-elim (¬prem h-prem)
... | failure es | _ = ⊥-elim $ case trans (sym (map-failure {f = proj₁} eqU))
(completeness-UTXOS Γ tt txTop tt h-utxos)
of λ ()