{-# OPTIONS --safe #-}
open import Algebra using (CommutativeMonoid)
open import Data.Integer.Ext using (posPart; negPart)
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 Tactic.Derive.DecEq
open import Ledger.Prelude
open import Ledger.Abstract
open import Ledger.Transaction
module Ledger.Utxo
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where
open import Ledger.ScriptValidation txs abs
open import Ledger.Fees txs using (scriptsCost)
open import Ledger.Certs govStructure
instance
_ = +-0-monoid
isTwoPhaseScriptAddress : Tx → UTxO → Addr → Type
isTwoPhaseScriptAddress tx utxo a =
if isScriptAddr a then
(λ {p} → if lookupScriptHash (getScriptHash a p) tx utxo
then (λ {s} → isP2Script s)
else ⊥)
else
⊥
isTwoPhaseScriptAddress? : ∀ {tx utxo a} → isTwoPhaseScriptAddress tx utxo a ⁇
isTwoPhaseScriptAddress? {tx} {utxo} {a} .dec
with decide (isScriptAddr a)
... | inj₂ _ = no λ ()
... | inj₁ p
with decide (lookupScriptHash (getScriptHash a p) tx utxo)
... | inj₂ _ = no λ ()
... | inj₁ s = isP2Script? {s} .dec
record isTwoPhaseScriptAddress′ (tx : Tx) (utxo : UTxO) (a : Addr) : Type where
constructor wrap
field unwrap : isTwoPhaseScriptAddress tx utxo a
instance
isTwoPhaseScriptAddress′? : ∀ {tx utxo a} → isTwoPhaseScriptAddress′ tx utxo a ⁇
isTwoPhaseScriptAddress′? {tx} {utxo} {a} = ⁇ (map′ wrap unwrap (isTwoPhaseScriptAddress? {tx} {utxo} {a} .dec))
where open isTwoPhaseScriptAddress′
opaque
getDataHashes : ℙ TxOut → ℙ DataHash
getDataHashes txo = mapPartial isInj₂ (mapPartial (proj₁ ∘ proj₂ ∘ proj₂) txo)
getInputHashes : Tx → UTxO → ℙ DataHash
getInputHashes tx utxo = getDataHashes
(filterˢ (λ (a , _ ) → isTwoPhaseScriptAddress′ tx utxo a)
(range (utxo ∣ txins)))
where open Tx; open TxBody (tx .body)
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
record UTxOState : Type where
constructor ⟦_,_,_,_⟧ᵘ
field
utxo : UTxO
fees : Coin
deposits : Deposits
donations : Coin
instance
unquoteDecl To-UTxOEnv To-UTxOState = derive-To
( (quote UTxOEnv , To-UTxOEnv ) ∷
[ (quote UTxOState , To-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 (refScripts tx utxo)
minfee : PParams → UTxO → Tx → Coin
minfee pp utxo tx = pp .a * tx .body .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
feesOK : PParams → Tx → UTxO → Type
feesOK pp tx utxo = ( minfee pp utxo tx ≤ txfee × (txrdmrs ˢ ≢ ∅
→ ( All (λ (addr , _) → isVKeyAddr addr) collateralRange
× isAdaOnly bal
× coin bal * 100 ≥ txfee * pp .collateralPercentage
× collateral ≢ ∅
)
)
)
where
open Tx tx; open TxBody body; open TxWitnesses wits; open PParams pp
collateralRange = range ((mapValues txOutHash utxo) ∣ collateral)
bal = 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
data _⊢_⇀⦇_,UTXOS⦈_ where
Scripts-Yes :
let pp = Γ .pparams
open Tx tx renaming (body to txb); open TxBody txb
sLst = collectPhaseTwoScriptInputs pp tx utxo
in
∙ ValidCertDeposits pp deposits txcerts
∙ evalScripts tx sLst ≡ isValid
∙ isValid ≡ true
────────────────────────────────
Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXOS⦈ ⟦ (utxo ∣ txins ᶜ) ∪ˡ (outs txb) , fees + txfee , updateDeposits pp txb deposits , donations + txdonation ⟧
Scripts-No :
let pp = Γ .pparams
open Tx tx renaming (body to txb); open TxBody txb
sLst = collectPhaseTwoScriptInputs pp tx utxo
in
∙ evalScripts tx sLst ≡ isValid
∙ isValid ≡ false
────────────────────────────────
Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXOS⦈ ⟦ utxo ∣ collateral ᶜ , fees + cbalance (utxo ∣ collateral) , deposits , donations ⟧
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
txoutsʰ = mapValues txOutHash txouts
overhead = 160
in
∙ txins ≢ ∅ ∙ txins ∪ refInputs ⊆ dom utxo
∙ txins ∩ refInputs ≡ ∅ ∙ inInterval slot txvldt
∙ feesOK pp tx utxo ∙ consumed pp s txb ≡ produced pp s txb
∙ coin mint ≡ 0 ∙ txsize ≤ maxTxSize pp
∙ refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx
∙ ∀[ (_ , txout) ∈ txoutsʰ .proj₁ ]
inject ((overhead + utxoEntrySize txout) * coinsPerUTxOByte pp) ≤ᵗ getValueʰ txout
∙ ∀[ (_ , txout) ∈ txoutsʰ .proj₁ ]
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 ] a .RwdAddr.net ≡ 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 v j n o p q r t u h
= UTXO-inductive {Γ = Γ} {s = s} {tx = tx} (x , y , z , w , k , l , m , v , j , n , o , p , q , r , t , u , h)
unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO-inductive)