diff --git a/src/Ledger/Conway/Conformance/Gov.agda b/src/Ledger/Conway/Conformance/Gov.agda index 4a10bfd27..82f5abee4 100644 --- a/src/Ledger/Conway/Conformance/Gov.agda +++ b/src/Ledger/Conway/Conformance/Gov.agda @@ -13,6 +13,7 @@ open import Ledger.GovernanceActions govStructure using (Vote) open import Ledger.Enact govStructure open import Ledger.Ratify txs hiding (vote) open import Ledger.Conway.Conformance.Certs govStructure +import Ledger.Gov txs as L open import Data.List.Ext using (subpermutations; sublists) open import Data.List.Ext.Properties2 @@ -59,186 +60,14 @@ private variable open GState open PState -govActionPriority : GovAction → ℕ -govActionPriority NoConfidence = 0 -govActionPriority (UpdateCommittee _ _ _) = 1 -govActionPriority (NewConstitution _ _) = 2 -govActionPriority (TriggerHF _) = 3 -govActionPriority (ChangePParams _) = 4 -govActionPriority (TreasuryWdrl _) = 5 -govActionPriority Info = 6 - -_∼_ : ℕ → ℕ → Type -n ∼ m = (n ≡ m) ⊎ (n ≡ 0 × m ≡ 1) ⊎ (n ≡ 1 × m ≡ 0) - -_≈ᵍ_ : GovAction → GovAction → Type -a ≈ᵍ a' = (govActionPriority a) ∼ (govActionPriority a') - -_∼?_ : (n m : ℕ) → Dec (n ∼ m) -n ∼? m = n ≟ m ⊎-dec (n ≟ 0 ×-dec m ≟ 1) ⊎-dec (n ≟ 1 ×-dec m ≟ 0) - -_≈?_ : (a a' : GovAction) → Dec (a ≈ᵍ a') -a ≈? a' = (govActionPriority a) ∼? (govActionPriority a') - - -insertGovAction : GovState → GovActionID × GovActionState → GovState -insertGovAction [] gaPr = [ gaPr ] -insertGovAction ((gaID₀ , gaSt₀) ∷ gaPrs) (gaID₁ , gaSt₁) - = if (govActionPriority (action gaSt₀)) ≤? (govActionPriority (action gaSt₁)) - then (gaID₀ , gaSt₀) ∷ insertGovAction gaPrs (gaID₁ , gaSt₁) - else (gaID₁ , gaSt₁) ∷ (gaID₀ , gaSt₀) ∷ gaPrs - -mkGovStatePair : Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash a - → GovActionID × GovActionState -mkGovStatePair e aid addr a prev = (aid , record - { votes = ∅ ; returnAddr = addr ; expiresIn = e ; action = a ; prevAction = prev }) - -addAction : GovState - → Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash a - → GovState -addAction s e aid addr a prev = insertGovAction s (mkGovStatePair e aid addr a prev) - opaque - addVote : GovState → GovActionID → Voter → Vote → GovState - addVote s aid voter v = map modifyVotes s - where modifyVotes : GovActionID × GovActionState → GovActionID × GovActionState - modifyVotes = λ (gid , s') → gid , record s' - { votes = if gid ≡ aid then insert (votes s') voter v else votes s'} - isRegistered : GovEnv → Voter → Type isRegistered ⟦ _ , _ , _ , _ , _ , ⟦ _ , pState , gState ⟧ᶜˢ ⟧ᵍ (r , c) = case r of λ where CC → just c ∈ range (gState .ccHotKeys) DRep → c ∈ dom (gState .dreps) SPO → c ∈ mapˢ KeyHashObj (dom (pState .pools)) - validHFAction : GovProposal → GovState → EnactState → Type - validHFAction (record { action = TriggerHF v ; prevAction = prev }) s e = - (let (v' , aid) = EnactState.pv e in aid ≡ prev × pvCanFollow v' v) - ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ TriggerHF v' × pvCanFollow v' v - validHFAction _ _ _ = ⊤ - -data - _⊢_⇀⦇_,GOV'⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type - -_⊢_⇀⦇_,GOV⦈_ : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type - --- Convert list of (GovActionID,GovActionState)-pairs to list of GovActionID pairs. -getAidPairsList : GovState → List (GovActionID × GovActionID) -getAidPairsList aid×states = - mapMaybe (λ (aid , aState) → (aid ,_) <$> getHash (prevAction aState)) $ aid×states - --- A list of GovActionID pairs connects the first GovActionID to the second. -_connects_to_ : List (GovActionID × GovActionID) → GovActionID → GovActionID → Type -[] connects aidNew to aidOld = aidNew ≡ aidOld -((aid , aidPrev) ∷ s) connects aidNew to aidOld = - aid ≡ aidNew × s connects aidPrev to aidOld ⊎ s connects aidNew to aidOld - -enactable : EnactState → List (GovActionID × GovActionID) - → GovActionID × GovActionState → Type -enactable e aidPairs = λ (aidNew , as) → case getHashES e (action as) of - - λ where - - nothing → ⊤ - (just aidOld) → ∃[ t ] fromList t ⊆ fromList aidPairs - × Unique t × t connects aidNew to aidOld - -allEnactable : EnactState → GovState → Type -allEnactable e aid×states = All (enactable e (getAidPairsList aid×states)) aid×states - -hasParentE : EnactState → GovActionID → GovAction → Type -hasParentE e aid a = case getHashES e a of - - λ where - - nothing → ⊤ - (just id) → id ≡ aid - -hasParent : EnactState → GovState → (a : GovAction) → NeedsHash a → Type -hasParent e s a aid with getHash aid -... | just aid' = hasParentE e aid' a - ⊎ Any (λ (gid , gas) → gid ≡ aid' × action gas ≈ᵍ a) s -... | nothing = ⊤ - -open Equivalence - -hasParentE? : ∀ e aid a → Dec (hasParentE e aid a) -hasParentE? e aid a with getHashES e a -... | nothing = yes _ -... | (just id) = id ≟ aid - -hasParent? : ∀ e s a aid → Dec (hasParent e s a aid) -hasParent? e s a aid with getHash aid -... | just aid' = hasParentE? e aid' a - ⊎-dec any? (λ (gid , gas) → gid ≟ aid' ×-dec action gas ≈? a) s -... | nothing = yes _ - --- newtype to make the instance resolution work -data hasParent' : EnactState → GovState → (a : GovAction) → NeedsHash a → Type where - HasParent' : ∀ {x y z w} → hasParent x y z w → hasParent' x y z w - -instance - hasParent?' : ∀ {x y z w} → hasParent' x y z w ⁇ - hasParent?' = ⁇ map′ HasParent' (λ where (HasParent' x) → x) (hasParent? _ _ _ _) - -[_connects_to_?] : ∀ l aidNew aidOld → Dec (l connects aidNew to aidOld) -[ [] connects aidNew to aidOld ?] = aidNew ≟ aidOld - -[ (aid , aidPrev) ∷ s connects aidNew to aidOld ?] = - ((aid ≟ aidNew) ×-dec [ s connects aidPrev to aidOld ?]) ⊎-dec [ s connects aidNew to aidOld ?] - -any?-connecting-subperm : ∀ {u} {v} → ∀ L → Dec (Any(λ l → Unique l × l connects u to v) (subpermutations L)) -any?-connecting-subperm {u} {v} L = any? (λ l → unique? _≟_ l ×-dec [ l connects u to v ?]) (subpermutations L) - -∃?-connecting-subperm : ∀ {u} {v} → ∀ L → Dec (∃[ l ] l ∈ˡ subpermutations L × Unique l × l connects u to v) -∃?-connecting-subperm L = from (map′⇔ (↔⇒ Any↔)) (any?-connecting-subperm L) - -∃?-connecting-subset : ∀ {u} {v} → ∀ L → Dec (∃[ l ] l ⊆ˡ L × Unique l × l connects u to v) -∃?-connecting-subset L = from (map′⇔ ∃uniqueSubset⇔∃uniqueSubperm) (∃?-connecting-subperm L) - -enactable? : ∀ eState aidPairs aidNew×st → Dec (enactable eState aidPairs aidNew×st) -enactable? eState aidPairs (aidNew , as) with getHashES eState (GovActionState.action as) -... | nothing = yes tt -... | just aidOld = from (map′⇔ ∃-sublist-⇔) (∃?-connecting-subset aidPairs) - -allEnactable? : ∀ eState aid×states → Dec (allEnactable eState aid×states) -allEnactable? eState aid×states = - all? (λ aid×st → enactable? eState (getAidPairsList aid×states) aid×st) aid×states - --- newtype to make the instance resolution work -data allEnactable' : EnactState → GovState → Type where - AllEnactable' : ∀ {x y} → allEnactable x y → allEnactable' x y - -instance - allEnactable?' : ∀ {x y} → allEnactable' x y ⁇ - allEnactable?' = ⁇ map′ AllEnactable' (λ where (AllEnactable' x) → x) (allEnactable? _ _) - --- `maxAllEnactable` returns a list `ls` of sublists of the given --- list (`aid×states : List (GovActionID × GovActionState)`) such that --- (i) each sublist `l ∈ ls` satisfies `allEnactable e l` and --- (ii) each sublist `l ∈ ls` is of maximal length among sublists of `aid×states` satisfying `allEnactable`. -maxAllEnactable : EnactState → List (GovActionID × GovActionState) → List (List (GovActionID × GovActionState)) -maxAllEnactable e = maxsublists⊧P (allEnactable? e) - --- Every sublist returned by `maxAllEnactable` satisfies (i). -∈-maxAllEnactable→allEnactable : ∀ {e} {aid×states} l - → l ∈ˡ maxAllEnactable e aid×states → allEnactable e l -∈-maxAllEnactable→allEnactable {e} {aid×states} l l∈ = - proj₂ (∈-filter⁻ (allEnactable? e) {l} {sublists aid×states} - (proj₁ (∈-filter⁻ (λ l → length l ≟ maxlen (sublists⊧P (allEnactable? e) aid×states)) l∈))) - --- Every sublist returned by `maxAllEnactable` satisfies (ii). -∈-maxAllEnactable→maxLength : ∀ {e aid×states l l'} - → l ∈ˡ sublists aid×states → allEnactable e l - → l' ∈ˡ maxAllEnactable e aid×states - → length l ≤ length l' -∈-maxAllEnactable→maxLength {e} {aid×states} {l} {l'} l∈ el l'∈ = - let ls = sublists⊧P (allEnactable? e) aid×states in - subst (length l ≤_) - (sym (proj₂ (∈-filter⁻ (λ l → length l ≟ maxlen ls) {xs = ls} l'∈))) - (∈-maxlen-≤ l (∈-filter⁺ (allEnactable? e) l∈ el)) - -data _⊢_⇀⦇_,GOV'⦈_ where +data _⊢_⇀⦇_,GOV'⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type where GOV-Vote : ∀ {x ast} → let open GovEnv Γ @@ -248,13 +77,13 @@ data _⊢_⇀⦇_,GOV'⦈_ where ∙ canVote pparams (action ast) (proj₁ voter) ∙ isRegistered Γ voter ─────────────────────────────────────── - (Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ addVote s aid voter v + (Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ L.addVote s aid voter v GOV-Propose : ∀ {x} → let open GovEnv Γ; open PParams pparams hiding (a) prop = record { returnAddr = addr ; action = a ; anchor = x ; policy = p ; deposit = d ; prevAction = prev } - s' = addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev + s' = L.addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev in ∙ actionWellFormed a ∙ d ≡ govActionDeposit @@ -262,10 +91,11 @@ data _⊢_⇀⦇_,GOV'⦈_ where ∙ (¬ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w) → p ≡ nothing) ∙ (∀ {new rem q} → a ≡ UpdateCommittee new rem q → ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅) - ∙ validHFAction prop s enactState - ∙ hasParent enactState s a prev + ∙ L.validHFAction prop s enactState + ∙ L.hasParent enactState s a prev ∙ addr .RwdAddr.net ≡ NetworkId ─────────────────────────────────────── (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' +_⊢_⇀⦇_,GOV⦈_ : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type _⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV'⦈_} diff --git a/src/Ledger/Conway/Conformance/Gov/Properties.agda b/src/Ledger/Conway/Conformance/Gov/Properties.agda index 5f9ec1bbe..8a2553134 100644 --- a/src/Ledger/Conway/Conformance/Gov/Properties.agda +++ b/src/Ledger/Conway/Conformance/Gov/Properties.agda @@ -27,6 +27,10 @@ open import Relation.Binary using (IsEquivalence) open import Tactic.Defaults open import Tactic.GenError +private module L where + open import Ledger.Gov txs public + open import Ledger.Gov.Properties txs public + open Equivalence open GovActionState open Inverse @@ -76,25 +80,7 @@ private hasPrev record { action = Info } v = no λ () opaque - unfolding validHFAction isRegistered - - instance - validHFAction? : ∀ {p s e} → validHFAction p s e ⁇ - validHFAction? {record { action = NoConfidence }} = Dec-⊤ - validHFAction? {record { action = UpdateCommittee _ _ _ }} = Dec-⊤ - validHFAction? {record { action = NewConstitution _ _ }} = Dec-⊤ - validHFAction? {record { action = TriggerHF v ; prevAction = prev }} {s} {record { pv = (v' , aid') }} - with aid' ≟ prev ×-dec pvCanFollow? {v'} {v} | any? (λ (aid , x) → aid ≟ prev ×-dec hasPrev x v) s - ... | yes p | _ = ⁇ yes (inj₁ p) - ... | no _ | yes p with ((aid , x) , x∈xs , (refl , v , h)) ← P.find p = ⁇ yes (inj₂ - (x , v , to ∈-fromList x∈xs , h)) - ... | no ¬p₁ | no ¬p₂ = ⁇ no λ - { (inj₁ x) → ¬p₁ x - ; (inj₂ (s , v , (h₁ , h₂ , h₃))) → ¬p₂ $ - ∃∈-Any ((prev , s) , (from ∈-fromList h₁ , refl , (v , h₂ , h₃))) } - validHFAction? {record { action = ChangePParams _ }} = Dec-⊤ - validHFAction? {record { action = TreasuryWdrl _ }} = Dec-⊤ - validHFAction? {record { action = Info }} = Dec-⊤ + unfolding isRegistered isRegistered? : ∀ Γ v → Dec (isRegistered Γ v) isRegistered? _ (CC , _) = ¿ _ ∈ _ ¿ @@ -134,27 +120,27 @@ instance H = ¿ actionWellFormed a × d ≡ govActionDeposit - × validHFAction prop s enactState + × L.validHFAction prop s enactState × (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy) × (¬ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w) → p ≡ nothing) - × hasParent' enactState s a prev + × L.hasParent' enactState s a prev × addr .RwdAddr.net ≡ NetworkId ¿ ,′ isUpdateCommittee a computeProof = case H of λ where - (yes (wf , dep , vHFA , pol , ¬pol , HasParent' en , goodAddr) , yes (new , rem , q , refl)) → + (yes (wf , dep , vHFA , pol , ¬pol , L.HasParent' en , goodAddr) , yes (new , rem , q , refl)) → case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where (yes newOk) → success (_ , GOV-Propose (wf , dep , pol , ¬pol , (λ where refl → newOk) , vHFA , en , goodAddr)) (no ¬p) → failure (genErrors ¬p) - (yes (wf , dep , vHFA , pol , ¬pol , HasParent' en , goodAddr) , no notNewComm) → success + (yes (wf , dep , vHFA , pol , ¬pol , L.HasParent' en , goodAddr) , no notNewComm) → success (-, GOV-Propose (wf , dep , pol , ¬pol , (λ isNewComm → ⊥-elim (notNewComm (-, -, -, isNewComm))) , vHFA , en , goodAddr)) (no ¬p , _) → failure (genErrors ¬p) completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' → map proj₁ computeProof ≡ success s' completeness s' (GOV-Propose (wf , dep , pol , ¬pol , newOk , vHFA , en , goodAddr)) with H - ... | (no ¬p , _) = ⊥-elim (¬p (wf , dep , vHFA , pol , ¬pol , HasParent' en , goodAddr)) - ... | (yes (_ , _ , _ , _ , _ , HasParent' _ , _) , no notNewComm) = refl - ... | (yes (_ , _ , _ , _ , _ , HasParent' _ , _) , yes (new , rem , q , refl)) + ... | (no ¬p , _) = ⊥-elim (¬p (wf , dep , vHFA , pol , ¬pol , L.HasParent' en , goodAddr)) + ... | (yes (_ , _ , _ , _ , _ , L.HasParent' _ , _) , no notNewComm) = refl + ... | (yes (_ , _ , _ , _ , _ , L.HasParent' _ , _) , yes (new , rem , q , refl)) rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (newOk refl) .proj₂ = refl computeProof : (sig : GovVote ⊎ GovProposal) → _ @@ -167,16 +153,3 @@ instance Computational-GOV : Computational _⊢_⇀⦇_,GOV⦈_ String Computational-GOV = it - -allEnactable-singleton : ∀ {aid s es} → getHash (s .prevAction) ≡ getHashES es (s .action) - → allEnactable es [ (aid , s) ] -allEnactable-singleton {aid} {s} {es} eq = helper All.∷ All.[] - where - module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence th) - - helper : enactable es (getAidPairsList [ (aid , s) ]) (aid , s) - helper with getHashES es (s .action) | getHash (s .prevAction) - ... | just x | just x' with refl <- just-injective eq = - [ (aid , x) ] , proj₁ ≡ᵉ.refl , All.[] ∷ [] , inj₁ (refl , refl) - ... | just x | nothing = case eq of λ () - ... | nothing | _ = _ diff --git a/src/Ledger/Conway/Conformance/Ledger.agda b/src/Ledger/Conway/Conformance/Ledger.agda index f2a9f3e47..68754c52e 100644 --- a/src/Ledger/Conway/Conformance/Ledger.agda +++ b/src/Ledger/Conway/Conformance/Ledger.agda @@ -14,7 +14,7 @@ module Ledger.Conway.Conformance.Ledger open import Ledger.Enact govStructure open import Ledger.Conway.Conformance.Gov txs -open import Ledger.Conway.Conformance.Utxo txs abs +open import Ledger.Conway.Conformance.Utxo txs abs hiding (module L) open import Ledger.Conway.Conformance.Utxow txs abs open import Ledger.Conway.Conformance.Certs govStructure @@ -70,7 +70,7 @@ data LEDGER-V : let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ - utxoSt'' = record utxoSt' { deposits = updateDeposits pparams txb (deposits utxoSt') } + utxoSt'' = record utxoSt' { deposits = L.updateDeposits pparams txb (deposits utxoSt') } in ∙ isValid tx ≡ true ∙ record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt' diff --git a/src/Ledger/Conway/Conformance/Utxo.agda b/src/Ledger/Conway/Conformance/Utxo.agda index 7dcccab7c..ce5495833 100644 --- a/src/Ledger/Conway/Conformance/Utxo.agda +++ b/src/Ledger/Conway/Conformance/Utxo.agda @@ -32,26 +32,6 @@ open PParams instance _ = +-0-monoid -updateCertDeposits : PParams → List DCert → Deposits → Deposits -updateCertDeposits pp [] deposits = deposits -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 ∪⁺ ❴ PoolDeposit kh , pp .poolDeposit ❵) -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 - -updateDeposits : PParams → TxBody → Deposits → Deposits -updateDeposits pp txb = updateCertDeposits pp txcerts - ∘ L.updateProposalDeposits txprop txid (pp .govActionDeposit) - where open TxBody txb - open L public using (UTxOEnv; UTxOState; ⟦_,_,_,_⟧ᵘ) private variable @@ -97,31 +77,6 @@ data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Typ unquoteDecl Scripts-Yes-premises = genPremises Scripts-Yes-premises (quote Scripts-Yes) unquoteDecl Scripts-No-premises = genPremises Scripts-No-premises (quote Scripts-No) -depositsChange : PParams → TxBody → Deposits → ℤ -depositsChange pp txb deposits = - getCoin (updateDeposits pp txb deposits) - getCoin deposits - -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 - = L.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 - = L.balance (L.outs txb) - + inject (txb .txfee) - + inject (newDeposits pp st txb) - + inject (txb .txdonation) - data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type where UTXO-inductive : @@ -133,7 +88,7 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type in ∙ txins ≢ ∅ ∙ txins ∪ refInputs ⊆ dom utxo ∙ txins ∩ refInputs ≡ ∅ ∙ L.inInterval slot txvldt - ∙ L.feesOK pp tx utxo ≡ true ∙ consumed pp s txb ≡ produced pp s txb + ∙ L.feesOK pp tx utxo ≡ true ∙ L.consumed pp s txb ≡ L.produced pp s txb ∙ coin mint ≡ 0 ∙ txsize ≤ maxTxSize pp ∙ L.refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx diff --git a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda index 78eb17fa2..7f2759120 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda @@ -54,15 +54,15 @@ module _ (ext : ExternalFunctions) where "Consumed:" ∷ ("\tInputs: \t" +ˢ show (L.balance (utxo ∣ txins))) ∷ ("\tMint: \t" +ˢ show mint) ∷ - ("\tRefunds: \t" +ˢ show (inject (depositRefunds pparams (from st) body))) ∷ + ("\tRefunds: \t" +ˢ show (inject (L.depositRefunds pparams (from st) body))) ∷ ("\tWithdrawals: \t" +ˢ show (inject (getCoin txwdrls))) ∷ - ("\tTotal: \t" +ˢ show (consumed pparams (from st) body)) ∷ + ("\tTotal: \t" +ˢ show (L.consumed pparams (from st) body)) ∷ "Produced:" ∷ ("\tOutputs: \t" +ˢ show (L.balance (L.outs body))) ∷ ("\tDonations: \t" +ˢ show (inject txdonation)) ∷ - ("\tDeposits: \t" +ˢ show (inject (newDeposits pparams (from st) body))) ∷ + ("\tDeposits: \t" +ˢ show (inject (L.newDeposits pparams (from st) body))) ∷ ("\tFees: \t" +ˢ show (inject txfee)) ∷ - ("\tTotal: \t" +ˢ show (produced pparams (from st) body)) ∷ + ("\tTotal: \t" +ˢ show (L.produced pparams (from st) body)) ∷ [] {-# COMPILE GHC utxo-debug as utxoDebug #-}