{-# 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.Abstract
open import Ledger.Conway.Transaction
module Ledger.Conway.Utxo
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where
open import Ledger.Conway.Script.Validation txs abs
open import Ledger.Conway.Fees txs using (scriptsCost)
open import Ledger.Conway.Certs govStructure
instance
_ = +-0-monoid
totExUnits : Tx → ExUnits
totExUnits tx = ∑[ (_ , eu) ← tx .wits .txrdmrs ] eu
where open Tx; open TxWitnesses
utxoEntrySizeWithoutVal : MemoryEstimate
utxoEntrySizeWithoutVal = 8
utxoEntrySize : TxOutʰ → MemoryEstimate
utxoEntrySize o = utxoEntrySizeWithoutVal + size (getValueʰ o)
open PParams
record UTxOEnv : Type where
field
slot : Slot
pparams : PParams
treasury : Coin
instance
HasPParams-UTxOEnv : HasPParams UTxOEnv
HasPParams-UTxOEnv .PParamsOf = UTxOEnv.pparams
HasgovActionDeposit-UTxOEnv : HasgovActionDeposit UTxOEnv
HasgovActionDeposit-UTxOEnv .govActionDepositOf = govActionDepositOf ∘ PParamsOf
record UTxOState : Type where
constructor ⟦_,_,_,_⟧ᵘ
field
utxo : UTxO
fees : Coin
deposits : Deposits
donations : Coin
record HasUTxOState {a} (A : Type a) : Type a where
field UTxOStateOf : A → UTxOState
open HasUTxOState ⦃...⦄ public
instance
HasDeposits-UTxOState : HasDeposits UTxOState
HasDeposits-UTxOState .DepositsOf = UTxOState.deposits
HasUTxO-UTxOState : HasUTxO UTxOState
HasUTxO-UTxOState .UTxOOf = UTxOState.utxo
unquoteDecl HasCast-UTxOEnv HasCast-UTxOState = derive-HasCast
( (quote UTxOEnv , HasCast-UTxOEnv ) ∷
[ (quote UTxOState , HasCast-UTxOState) ])
data
_⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type
module _ (let open Tx; open TxBody; open TxWitnesses) where opaque
outs : TxBody → UTxO
outs tx = mapKeys (tx .txid ,_) (tx .txouts)
balance : UTxO → Value
balance utxo = ∑[ x ← mapValues txOutHash utxo ] getValueʰ x
cbalance : UTxO → Coin
cbalance utxo = coin (balance utxo)
refScriptsSize : UTxO → Tx → ℕ
refScriptsSize utxo tx = sum (map scriptSize (setToList (refScripts tx utxo)))
minfee : PParams → UTxO → Tx → Coin
minfee pp utxo tx = pp .a * tx .txsize + pp .b
+ txscriptfee (pp .prices) (totExUnits tx)
+ scriptsCost pp (refScriptsSize utxo tx)
instance
HasCoin-UTxO : HasCoin UTxO
HasCoin-UTxO .getCoin = cbalance
certDeposit : DCert → PParams → Deposits
certDeposit (delegate c _ _ v) _ = ❴ CredentialDeposit c , v ❵
certDeposit (reg c _) pp = ❴ CredentialDeposit c , pp .keyDeposit ❵
certDeposit (regpool kh _) pp = ❴ PoolDeposit kh , pp .poolDeposit ❵
certDeposit (regdrep c v _) _ = ❴ DRepDeposit c , v ❵
certDeposit _ _ = ∅
certRefund : DCert → ℙ DepositPurpose
certRefund (dereg c _) = ❴ CredentialDeposit c ❵
certRefund (deregdrep c _) = ❴ DRepDeposit c ❵
certRefund _ = ∅
data ValidCertDeposits (pp : PParams) (deps : Deposits) : List DCert → Set
where
[] : ValidCertDeposits pp deps []
delegate : ∀ {c del kh v certs}
→ ValidCertDeposits pp (deps ∪⁺ ❴ CredentialDeposit c , v ❵) certs
→ ValidCertDeposits pp deps (delegate c del kh v ∷ certs)
regpool : ∀ {kh p certs}
→ ValidCertDeposits pp (deps ∪⁺ ❴ PoolDeposit kh , pp .poolDeposit ❵) certs
→ ValidCertDeposits pp deps (regpool kh p ∷ certs)
regdrep : ∀ {c v a certs}
→ ValidCertDeposits pp (deps ∪⁺ ❴ DRepDeposit c , v ❵) certs
→ ValidCertDeposits pp deps (regdrep c v a ∷ certs)
reg : ∀ {c v certs}
→ ValidCertDeposits pp (deps ∪⁺ ❴ CredentialDeposit c , pp .keyDeposit ❵) certs
→ ValidCertDeposits pp deps (reg c v ∷ certs)
dereg : ∀ {c md d certs}
→ (CredentialDeposit c , d) ∈ deps
→ md ≡ nothing ⊎ md ≡ just d
→ ValidCertDeposits pp (deps ∣ ❴ CredentialDeposit c ❵ ᶜ) certs
→ ValidCertDeposits pp deps (dereg c md ∷ certs)
deregdrep : ∀ {c d certs}
→ (DRepDeposit c , d) ∈ deps
→ ValidCertDeposits pp (deps ∣ ❴ DRepDeposit c ❵ ᶜ) certs
→ ValidCertDeposits pp deps (deregdrep c d ∷ certs)
ccreghot : ∀ {c v certs}
→ ValidCertDeposits pp deps certs
→ ValidCertDeposits pp deps (ccreghot c v ∷ certs)
retirepool : ∀ {kh e certs}
→ ValidCertDeposits pp deps certs
→ ValidCertDeposits pp deps (retirepool kh e ∷ certs)
private
validCertDeposits? : ∀ {pp} deps certs → Dec (ValidCertDeposits pp deps certs)
validCertDeposits? deps [] = yes []
validCertDeposits? deps (delegate _ _ _ _ ∷ certs) =
mapDec delegate (λ where (delegate p) → p) (validCertDeposits? _ _)
validCertDeposits? deps (regpool _ _ ∷ certs) =
mapDec regpool (λ where (regpool p) → p) (validCertDeposits? _ _)
validCertDeposits? deps (regdrep _ _ _ ∷ certs) =
mapDec regdrep (λ where (regdrep p) → p) (validCertDeposits? _ _)
validCertDeposits? deps (retirepool _ _ ∷ certs) =
mapDec retirepool (λ where (retirepool p) → p) (validCertDeposits? _ _)
validCertDeposits? deps (ccreghot _ _ ∷ certs) =
mapDec ccreghot (λ where (ccreghot p) → p) (validCertDeposits? _ _)
validCertDeposits? deps (reg _ _ ∷ certs) =
mapDec reg (λ where (reg p) → p) (validCertDeposits? _ _)
validCertDeposits? deps (dereg c nothing ∷ certs) with ¿ CredentialDeposit c ∈ dom deps ¿
... | yes p = mapDec (dereg (proj₂ (Equivalence.from dom∈ p)) (inj₁ refl)) (λ { (dereg _ _ p) → p }) (validCertDeposits? _ _)
... | no ¬p = no λ { (dereg x _ _) → ¬p (Equivalence.to dom∈ (_ , x)) }
validCertDeposits? deps (dereg c (just d) ∷ certs) with ¿ (CredentialDeposit c , d) ∈ deps ¿
... | yes p = mapDec (dereg p (inj₂ refl)) (λ { (dereg _ _ p) → p }) (validCertDeposits? _ _)
... | no ¬p = no λ { (dereg x (inj₂ refl) _) → ¬p x }
validCertDeposits? deps (deregdrep c d ∷ certs) with ¿ (DRepDeposit c , d) ∈ deps ¿
... | yes p = mapDec (deregdrep p) (λ where (deregdrep _ v) → v) (validCertDeposits? _ _)
... | no ¬p = no (λ where (deregdrep p _) → ¬p p)
instance
Dec-ValidCertDeposits : ∀ {pp deps certs} → ValidCertDeposits pp deps certs ⁇
Dec-ValidCertDeposits = ⁇ (validCertDeposits? _ _)
updateCertDeposits : PParams → List DCert → Deposits → Deposits
updateCertDeposits pp [] deposits = deposits
updateCertDeposits pp (reg c v ∷ certs) deposits
= updateCertDeposits pp certs (deposits ∪⁺ certDeposit (reg c v) pp)
updateCertDeposits pp (delegate c vd khs v ∷ certs) deposits
= updateCertDeposits pp certs (deposits ∪⁺ certDeposit (delegate c vd khs v) pp)
updateCertDeposits pp (regpool kh p ∷ certs) deposits
= updateCertDeposits pp certs (deposits ∪⁺ certDeposit (regpool kh p) pp)
updateCertDeposits pp (regdrep c v a ∷ certs) deposits
= updateCertDeposits pp certs (deposits ∪⁺ certDeposit (regdrep c v a) pp)
updateCertDeposits pp (dereg c v ∷ certs) deposits
= updateCertDeposits pp certs (deposits ∣ certRefund (dereg c v)ᶜ)
updateCertDeposits pp (deregdrep c v ∷ certs) deposits
= updateCertDeposits pp certs (deposits ∣ certRefund (deregdrep c v)ᶜ)
updateCertDeposits pp (_ ∷ certs) deposits
= updateCertDeposits pp certs deposits
updateProposalDeposits : List GovProposal → TxId → Coin → Deposits → Deposits
updateProposalDeposits [] _ _ deposits = deposits
updateProposalDeposits (_ ∷ ps) txid gaDep deposits =
updateProposalDeposits ps txid gaDep deposits
∪⁺ ❴ GovActionDeposit (txid , length ps) , gaDep ❵
updateDeposits : PParams → TxBody → Deposits → Deposits
updateDeposits pp txb = updateCertDeposits pp txcerts
∘ updateProposalDeposits txprop txid (pp .govActionDeposit)
where open TxBody txb
proposalDepositsΔ : List GovProposal → PParams → TxBody → Deposits
proposalDepositsΔ props pp txb = updateProposalDeposits props txid (pp .govActionDeposit) ∅
where open TxBody txb
depositsChange : PParams → TxBody → Deposits → ℤ
depositsChange pp txb deposits =
getCoin (updateDeposits pp txb deposits) - getCoin deposits
data inInterval (slot : Slot) : (Maybe Slot × Maybe Slot) → Type where
both : ∀ {l r} → l ≤ slot × slot ≤ r → inInterval slot (just l , just r)
lower : ∀ {l} → l ≤ slot → inInterval slot (just l , nothing)
upper : ∀ {r} → slot ≤ r → inInterval slot (nothing , just r)
none : inInterval slot (nothing , nothing)
instance
Dec-inInterval : inInterval ⁇²
Dec-inInterval {slot} {just x , just y } .dec with x ≤? slot | slot ≤? y
... | no ¬p₁ | _ = no λ where (both (h₁ , h₂)) → ¬p₁ h₁
... | yes p₁ | no ¬p₂ = no λ where (both (h₁ , h₂)) → ¬p₂ h₂
... | yes p₁ | yes p₂ = yes (both (p₁ , p₂))
Dec-inInterval {slot} {just x , nothing} .dec with x ≤? slot
... | no ¬p = no (λ where (lower h) → ¬p h)
... | yes p = yes (lower p)
Dec-inInterval {slot} {nothing , just x } .dec with slot ≤? x
... | no ¬p = no (λ where (upper h) → ¬p h)
... | yes p = yes (upper p)
Dec-inInterval {slot} {nothing , nothing} .dec = yes none
HasCoin-UTxOState : HasCoin UTxOState
HasCoin-UTxOState .getCoin s = getCoin (UTxOState.utxo s)
+ (UTxOState.fees s)
+ getCoin (UTxOState.deposits s)
+ UTxOState.donations s
coinPolicies : ℙ ScriptHash
coinPolicies = policies (inject 1)
isAdaOnly : Value → Type
isAdaOnly v = policies v ≡ᵉ coinPolicies
collateralCheck : PParams → Tx → UTxO → Type
collateralCheck pp tx utxo =
All (λ (addr , _) → isVKeyAddr addr) (range (utxo ∣ collateral))
× isAdaOnly balance′
× coin balance′ * 100 ≥ txfee * pp .collateralPercentage
× collateral ≢ ∅
where
open Tx tx; open TxBody body
balance′ = balance (utxo ∣ collateral)
module _ (let open UTxOState; open TxBody) where
depositRefunds : PParams → UTxOState → TxBody → Coin
depositRefunds pp st txb = negPart (depositsChange pp txb (st .deposits))
newDeposits : PParams → UTxOState → TxBody → Coin
newDeposits pp st txb = posPart (depositsChange pp txb (st .deposits))
consumed : PParams → UTxOState → TxBody → Value
consumed pp st txb
= balance (st .utxo ∣ txb .txins)
+ txb .mint
+ inject (depositRefunds pp st txb)
+ inject (getCoin (txb .txwdrls))
produced : PParams → UTxOState → TxBody → Value
produced pp st txb = balance (outs txb)
+ inject (txb .txfee)
+ inject (newDeposits pp st txb)
+ inject (txb .txdonation)
open PParams
private variable
Γ : UTxOEnv
s s' : UTxOState
tx : Tx
utxo : UTxO
fees donations : Coin
deposits : Deposits
open UTxOEnv
data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type where
Scripts-Yes :
let pp = Γ .pparams
open Tx tx renaming (body to txb); open TxBody txb
p2Scripts = collectP2ScriptsWithContext pp tx utxo
in
∙ ValidCertDeposits pp deposits txcerts
∙ evalP2Scripts p2Scripts ≡ isValid
∙ isValid ≡ true
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#11212}{\htmlId{11718}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#11226}{\htmlId{11725}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#11250}{\htmlId{11732}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#11231}{\htmlId{11743}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} (\,\href{Ledger.Conway.Utxo.html#11212}{\htmlId{11772}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{11777}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Transaction.html#2750}{\htmlId{11779}{\htmlClass{Function}{\text{txins}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{11785}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,) \,\href{Axiom.Set.Map.html#6320}{\htmlId{11788}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, (\,\href{Ledger.Conway.Utxo.html#2168}{\htmlId{11792}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Conway.Utxo.html#11448}{\htmlId{11797}{\htmlClass{Function}{\text{txb}}}}\,) \\ \,\href{Ledger.Conway.Utxo.html#11226}{\htmlId{11804}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11809}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Transaction.html#2844}{\htmlId{11811}{\htmlClass{Function}{\text{txfee}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#7988}{\htmlId{11819}{\htmlClass{Function}{\text{updateDeposits}}}}\, \,\href{Ledger.Conway.Utxo.html#11384}{\htmlId{11834}{\htmlClass{Bound}{\text{pp}}}}\, \,\href{Ledger.Conway.Utxo.html#11448}{\htmlId{11837}{\htmlClass{Function}{\text{txb}}}}\, \,\href{Ledger.Conway.Utxo.html#11250}{\htmlId{11841}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#11231}{\htmlId{11852}{\htmlClass{Generalizable}{\text{donations}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11862}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Transaction.html#3086}{\htmlId{11864}{\htmlClass{Function}{\text{txdonation}}}}\, \end{pmatrix}$
Scripts-No :
let pp = Γ .pparams
open Tx tx renaming (body to txb); open TxBody txb
p2Scripts = collectP2ScriptsWithContext pp tx utxo
in
∙ evalP2Scripts p2Scripts ≡ isValid
∙ isValid ≡ false
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#11212}{\htmlId{12188}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#11226}{\htmlId{12195}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#11250}{\htmlId{12202}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#11231}{\htmlId{12213}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#11212}{\htmlId{12241}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{12246}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Transaction.html#3285}{\htmlId{12248}{\htmlClass{Function}{\text{collateral}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{12259}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#11226}{\htmlId{12263}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12268}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Utxo.html#2328}{\htmlId{12270}{\htmlClass{Function}{\text{cbalance}}}}\, (\,\href{Ledger.Conway.Utxo.html#11212}{\htmlId{12280}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{12285}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Transaction.html#3285}{\htmlId{12287}{\htmlClass{Function}{\text{collateral}}}}\,) \\ \,\href{Ledger.Conway.Utxo.html#11250}{\htmlId{12301}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#11231}{\htmlId{12312}{\htmlClass{Generalizable}{\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⦈_ where
UTXO-inductive :
let pp = Γ .pparams
slot = Γ .slot
treasury = Γ .treasury
utxo = s .UTxOState.utxo
open Tx tx renaming (body to txb); open TxBody txb
open TxWitnesses wits
txoutsʰ = mapValues txOutHash txouts
overhead = 160
in
∙ txins ≢ ∅ ∙ txins ∪ refInputs ⊆ dom utxo
∙ txins ∩ refInputs ≡ ∅ ∙ inInterval slot txvldt
∙ minfee pp utxo tx ≤ txfee ∙ (txrdmrs ˢ ≢ ∅ → collateralCheck pp tx utxo)
∙ consumed pp s txb ≡ produced pp s txb ∙ coin mint ≡ 0
∙ txsize ≤ maxTxSize pp
∙ refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx
∙ ∀[ (_ , txout) ∈ ∣ txoutsʰ ∣ ]
inject ((overhead + 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 {Γ = Γ} {s = s} {tx = tx} (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)