Utxo
{-# OPTIONS --safe #-} open import Algebra using (CommutativeMonoid) open import Data.Nat.Properties using (+-0-monoid) import Data.Maybe as M import Data.Sum.Relation.Unary.All as Sum import Data.Integer as ℤ import Data.Rational as ℚ open import Ledger.Prelude open import Ledger.Conway.Specification.Abstract open import Ledger.Conway.Specification.Transaction module Ledger.Conway.Conformance.Utxo (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where open import Ledger.Conway.Specification.Script.Validation txs abs open import Ledger.Conway.Specification.Fees using (scriptsCost) open import Ledger.Conway.Conformance.Certs govStructure private module L where open import Ledger.Conway.Specification.Utxo txs abs public open PParams instance _ = +-0-monoid open L public using (UTxOEnv; UTxOState; ⟦_,_,_,_⟧ᵘ; HasCast-UTxOState; updateDeposits ; cbalance; balance; depositRefunds; consumed ; produced; outs; newDeposits; refScriptsSize ) private variable Γ : UTxOEnv s s' : UTxOState tx : Tx open PParams data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type where Scripts-Yes : ∀ {Γ} {s} {tx} → let open Tx tx renaming (body to txb); open TxBody txb open UTxOEnv Γ renaming (pparams to pp) open UTxOState s p2Scripts = collectP2ScriptsWithContext pp tx utxo in ∙ evalP2Scripts p2Scripts ≡ isValid ∙ isValid ≡ true ──────────────────────────────── Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} \,\htmlId{1708}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#3084}{\htmlId{1709}{\htmlClass{Function}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{1714}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#4816}{\htmlId{1716}{\htmlClass{Function}{\text{txIns}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{1722}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{1723}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{1725}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\htmlId{1728}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#4858}{\htmlId{1729}{\htmlClass{Function}{\text{L.outs}}}}\, \,\href{Ledger.Conway.Conformance.Utxo.html#1394}{\htmlId{1736}{\htmlClass{Field}{\text{txb}}}}\,\,\htmlId{1739}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3106}{\htmlId{1773}{\htmlClass{Function}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1778}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#5038}{\htmlId{1780}{\htmlClass{Function}{\text{txFee}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3128}{\htmlId{1818}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3154}{\htmlId{1859}{\htmlClass{Function}{\text{donations}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1869}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#5208}{\htmlId{1871}{\htmlClass{Function}{\text{txDonation}}}}\, \end{pmatrix}$ Scripts-No : ∀ {Γ} {s} {tx} → let open Tx tx renaming (body to txb); open TxBody txb open UTxOEnv Γ renaming (pparams to pp) open UTxOState s p2Scripts = collectP2ScriptsWithContext pp tx utxo in ∙ evalP2Scripts p2Scripts ≡ isValid ∙ isValid ≡ false ──────────────────────────────── Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3084}{\htmlId{2303}{\htmlClass{Function}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2308}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#4888}{\htmlId{2310}{\htmlClass{Function}{\text{collateralInputs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2327}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3106}{\htmlId{2361}{\htmlClass{Function}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{2366}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#5018}{\htmlId{2368}{\htmlClass{Function}{\text{L.cbalance}}}}\, \,\htmlId{2379}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#3084}{\htmlId{2380}{\htmlClass{Function}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#13536}{\htmlId{2385}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#4888}{\htmlId{2387}{\htmlClass{Function}{\text{collateralInputs}}}}\,\,\htmlId{2403}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3128}{\htmlId{2437}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3154}{\htmlId{2478}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ unquoteDecl Scripts-Yes-premises = genPremises Scripts-Yes-premises (quote Scripts-Yes) unquoteDecl Scripts-No-premises = genPremises Scripts-No-premises (quote Scripts-No) data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type where UTXO-inductive : let open Tx tx renaming (body to txb); open TxBody txb; open TxWitnesses wits open UTxOEnv Γ renaming (pparams to pp) open UTxOState s txOutsʰ = (mapValues txOutHash txOuts) overhead = 160 in ∙ txIns ≢ ∅ ∙ txIns ∪ refInputs ∪ collateralInputs ⊆ dom utxo ∙ L.inInterval slot txVldt ∙ L.minfee pp utxo tx ≤ txFee ∙ (txrdmrs ˢ ≢ ∅ → L.collateralCheck pp tx utxo) ∙ consumed pp s txb ≡ produced pp s txb ∙ coin mint ≡ 0 ∙ (∅ᵐ ≢ᵐ txrdmrs × nothing ≢ proj₂ txVldt → map epochInfoSlotToUTCTime (proj₂ txVldt) ≢ nothing ) ∙ txsize ≤ maxTxSize pp ∙ L.refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx ∙ ∀[ (_ , txout) ∈ ∣ txOutsʰ ∣ ] inject ((overhead + L.utxoEntrySize txout) * coinsPerUTxOByte pp) ≤ᵗ getValueʰ txout ∙ ∀[ (_ , txout) ∈ ∣ txOutsʰ ∣ ] serSize (getValueʰ txout) ≤ maxValSize pp ∙ ∀[ (a , _) ∈ range txOutsʰ ] Sum.All (const ⊤) (λ a → a .BootstrapAddr.attrsSize ≤ 64) a ∙ ∀[ (a , _) ∈ range txOutsʰ ] netId a ≡ NetworkId ∙ ∀[ a ∈ dom txWithdrawals ] NetworkIdOf a ≡ NetworkId ∙ txNetworkId ~ just NetworkId ∙ currentTreasury ~ just treasury ∙ Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s' ──────────────────────────────── Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s' pattern UTXO-inductive⋯ tx Γ s x y w k l m c d v j n o p q r t u h = UTXO-inductive {tx}{Γ}{s} (x , y , w , k , l , m , c , d , v , j , n , o , p , q , r , t , u , h) unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO-inductive)