{-# 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.Specification.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.Specification.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 : Treasury
record UTxOState : Type where
constructor ⟦_,_,_,_⟧ᵘ
field
utxo : UTxO
fees : Fees
deposits : Deposits
donations : Donations
record HasUTxOState {a} (A : Type a) : Type a where
field UTxOStateOf : A → UTxOState
open HasUTxOState ⦃...⦄ public
instance
HasPParams-UTxOEnv : HasPParams UTxOEnv
HasPParams-UTxOEnv .PParamsOf = UTxOEnv.pparams
HasUTxO-UTxOState : HasUTxO UTxOState
HasUTxO-UTxOState .UTxOOf = UTxOState.utxo
HasFee-UTxOState : HasFees UTxOState
HasFee-UTxOState .FeesOf = UTxOState.fees
HasDeposits-UTxOState : HasDeposits UTxOState
HasDeposits-UTxOState .DepositsOf = UTxOState.deposits
HasDonations-UTxOState : HasDonations UTxOState
HasDonations-UTxOState .DonationsOf = UTxOState.donations
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 txGovProposals 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 ∣ collateralInputs))
× isAdaOnly balance′
× coin balance′ * 100 ≥ txFee * pp .collateralPercentage
× collateralInputs ≢ ∅
where
open Tx tx; open TxBody body
balance′ = balance (utxo ∣ collateralInputs)
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 .txWithdrawals))
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 : Fees
donations : Donations
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.Specification.Utxo.html#11365}{\htmlId{11885}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11379}{\htmlId{11892}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11417}{\htmlId{11899}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11393}{\htmlId{11910}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} \,\htmlId{11938}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#11365}{\htmlId{11939}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{11944}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3034}{\htmlId{11946}{\htmlClass{Function}{\text{txIns}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{11952}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{11953}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{11955}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\htmlId{11958}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#2296}{\htmlId{11959}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#11615}{\htmlId{11964}{\htmlClass{Function}{\text{txb}}}}\,\,\htmlId{11967}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11379}{\htmlId{11971}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11976}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3256}{\htmlId{11978}{\htmlClass{Function}{\text{txFee}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#8112}{\htmlId{11986}{\htmlClass{Function}{\text{updateDeposits}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#11551}{\htmlId{12001}{\htmlClass{Bound}{\text{pp}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#11615}{\htmlId{12004}{\htmlClass{Function}{\text{txb}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#11417}{\htmlId{12008}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11393}{\htmlId{12019}{\htmlClass{Generalizable}{\text{donations}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12029}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3426}{\htmlId{12031}{\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.Specification.Utxo.html#11365}{\htmlId{12353}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11379}{\htmlId{12360}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11417}{\htmlId{12367}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11393}{\htmlId{12378}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#11365}{\htmlId{12406}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{12411}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3106}{\htmlId{12413}{\htmlClass{Function}{\text{collateralInputs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{12430}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11379}{\htmlId{12434}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12439}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#2456}{\htmlId{12441}{\htmlClass{Function}{\text{cbalance}}}}\, \,\htmlId{12450}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#11365}{\htmlId{12451}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{12456}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#3106}{\htmlId{12458}{\htmlClass{Function}{\text{collateralInputs}}}}\,\,\htmlId{12474}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11417}{\htmlId{12478}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#11393}{\htmlId{12489}{\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 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 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)