{-# 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 txs 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} (\,\href{Ledger.Conway.Specification.Utxo.html#1538}{\htmlId{1618}{\htmlClass{Function}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{1623}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3023}{\htmlId{1625}{\htmlClass{Function}{\text{txins}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{1631}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,) \,\href{Axiom.Set.Map.html#6320}{\htmlId{1634}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, (\,\href{Ledger.Conway.Specification.Utxo.html#2252}{\htmlId{1638}{\htmlClass{Function}{\text{L.outs}}}}\, \,\href{Ledger.Conway.Conformance.Utxo.html#1303}{\htmlId{1645}{\htmlClass{Field}{\text{txb}}}}\,)
\\ \,\href{Ledger.Conway.Specification.Utxo.html#1560}{\htmlId{1682}{\htmlClass{Function}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1687}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3117}{\htmlId{1689}{\htmlClass{Function}{\text{txfee}}}}\,
\\ \,\href{Ledger.Conway.Specification.Utxo.html#1582}{\htmlId{1727}{\htmlClass{Function}{\text{deposits}}}}\,
\\ \,\href{Ledger.Conway.Specification.Utxo.html#1608}{\htmlId{1768}{\htmlClass{Function}{\text{donations}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1778}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3359}{\htmlId{1780}{\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#1538}{\htmlId{2212}{\htmlClass{Function}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{2217}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3558}{\htmlId{2219}{\htmlClass{Function}{\text{collateral}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{2230}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Conway.Specification.Utxo.html#1560}{\htmlId{2264}{\htmlClass{Function}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{2269}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#2412}{\htmlId{2271}{\htmlClass{Function}{\text{L.cbalance}}}}\, (\,\href{Ledger.Conway.Specification.Utxo.html#1538}{\htmlId{2283}{\htmlClass{Function}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{2288}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3558}{\htmlId{2290}{\htmlClass{Function}{\text{collateral}}}}\,)
\\ \,\href{Ledger.Conway.Specification.Utxo.html#1582}{\htmlId{2334}{\htmlClass{Function}{\text{deposits}}}}\,
\\ \,\href{Ledger.Conway.Specification.Utxo.html#1608}{\htmlId{2375}{\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 ⊆ dom utxo
∙ txins ∩ refInputs ≡ ∅ ∙ 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
∙ 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 txwdrls ] NetworkIdOf a ≡ NetworkId
∙ txNetworkId ~ just NetworkId
∙ curTreasury ~ just treasury
∙ Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s'
────────────────────────────────
Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
pattern UTXO-inductive⋯ tx Γ s x y z w k l m c v j n o p q r t u h
= UTXO-inductive {tx}{Γ}{s} (x , y , z , w , k , l , m , c , v , j , n , o , p , q , r , t , u , h)
unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO-inductive)