From 363b1f6f6fe3f4eeb6a89456659413a4ad35e79a Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Thu, 21 Nov 2024 13:50:52 +0100 Subject: [PATCH] Prepare for conformance equivalence (#614) * Remove Conformance version of Ratify * Remove conformance version of ScriptValidation * Reuse Ledger code in Conformance.Utxow * Reuse Ledger code in Conformance.Utxo * spell out conformance updateCertDeposit for each DCert to make it line up with ledger * Fix wrong PParams in Conformance GOVCERT rules * Remove unused conformance ratify modules --- src/Ledger/Conway/Conformance/Certs.agda | 15 +- .../Conway/Conformance/Certs/Properties.agda | 4 +- src/Ledger/Conway/Conformance/Chain.agda | 2 +- src/Ledger/Conway/Conformance/Epoch.agda | 4 +- .../Conway/Conformance/Epoch/Properties.agda | 4 +- src/Ledger/Conway/Conformance/Gov.agda | 2 +- .../Conway/Conformance/Gov/Properties.agda | 2 +- src/Ledger/Conway/Conformance/Ledger.agda | 14 +- .../Conway/Conformance/Ledger/Properties.agda | 4 +- src/Ledger/Conway/Conformance/PDF.agda | 6 +- src/Ledger/Conway/Conformance/Ratify.agda | 332 ------------------ .../Conway/Conformance/Ratify/Properties.agda | 72 ---- .../Conway/Conformance/ScriptValidation.agda | 186 ---------- src/Ledger/Conway/Conformance/Utxo.agda | 170 +-------- .../Conway/Conformance/Utxo/Properties.agda | 2 +- src/Ledger/Conway/Conformance/Utxow.agda | 102 +----- .../Conway/Foreign/HSLedger/Ratify.agda | 4 +- src/Ledger/Conway/Foreign/HSLedger/Utxo.agda | 12 +- src/ScriptVerification/HelloWorld.agda | 4 +- src/ScriptVerification/Lib.agda | 2 +- src/ScriptVerification/SucceedIfNumber.agda | 4 +- 21 files changed, 69 insertions(+), 878 deletions(-) delete mode 100644 src/Ledger/Conway/Conformance/Ratify.agda delete mode 100644 src/Ledger/Conway/Conformance/Ratify/Properties.agda delete mode 100644 src/Ledger/Conway/Conformance/ScriptValidation.agda diff --git a/src/Ledger/Conway/Conformance/Certs.agda b/src/Ledger/Conway/Conformance/Certs.agda index 0932a01ec..38d502316 100644 --- a/src/Ledger/Conway/Conformance/Certs.agda +++ b/src/Ledger/Conway/Conformance/Certs.agda @@ -53,8 +53,15 @@ certRefund (deregdrep c _) = ❴ DRepDeposit c ❵ certRefund _ = ∅ updateCertDeposit : PParams → DCert → Deposits → Deposits -updateCertDeposit pp cert deposits - = (deposits ∪⁺ certDeposit cert pp) ∣ certRefund cert ᶜ +updateCertDeposit pp (delegate c _ _ v) deposits = deposits ∪⁺ ❴ CredentialDeposit c , v ❵ +updateCertDeposit pp (regdrep c v _) deposits = deposits ∪⁺ ❴ DRepDeposit c , v ❵ +updateCertDeposit pp (dereg c _) deposits = deposits ∣ ❴ CredentialDeposit c ❵ ᶜ +updateCertDeposit pp (deregdrep c _) deposits = deposits ∣ ❴ DRepDeposit c ❵ ᶜ +updateCertDeposit pp (regpool kh _) deposits = deposits ∪⁺ ❴ PoolDeposit kh , pp .PParams.poolDeposit ❵ +updateCertDeposit _ (retirepool _ _) deposits = deposits +updateCertDeposit _ (ccreghot _ _) deposits = deposits +-- updateCertDeposit pp cert deposits +-- = (deposits ∪⁺ certDeposit cert pp) ∣ certRefund cert ᶜ private variable rwds rewards : Credential ⇀ Coin @@ -145,14 +152,14 @@ data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → T ──────────────────────────────── Γ ⊢ ⟦ dReps , ccKeys , dep ⟧ᵛ ⇀⦇ deregdrep c d ,GOVCERT⦈ - ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , updateCertDeposit pp (deregdrep c d) dep ⟧ᵛ + ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , updateCertDeposit (CertEnv.pp Γ) (deregdrep c d) dep ⟧ᵛ GOVCERT-ccreghot : ∙ (c , nothing) ∉ ccKeys ──────────────────────────────── Γ ⊢ ⟦ dReps , ccKeys , dep ⟧ᵛ ⇀⦇ ccreghot c mc ,GOVCERT⦈ - ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , updateCertDeposit pp (ccreghot c mc) dep ⟧ᵛ + ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , updateCertDeposit (CertEnv.pp Γ) (ccreghot c mc) dep ⟧ᵛ data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where CERT-deleg : diff --git a/src/Ledger/Conway/Conformance/Certs/Properties.agda b/src/Ledger/Conway/Conformance/Certs/Properties.agda index 4c4993053..46a6a9132 100644 --- a/src/Ledger/Conway/Conformance/Certs/Properties.agda +++ b/src/Ledger/Conway/Conformance/Certs/Properties.agda @@ -61,11 +61,11 @@ instance (no ¬p) → failure (genErrors ¬p) Computational-GOVCERT .computeProof ⟦ _ , pp , _ , _ ⟧ᶜ ⟦ dReps , _ , dep ⟧ᵛ (deregdrep c _) = case c ∈? dom dReps of λ where - (yes p) → success (-, GOVCERT-deregdrep {pp = pp} p) + (yes p) → success (-, GOVCERT-deregdrep p) (no ¬p) → failure (genErrors ¬p) Computational-GOVCERT .computeProof ⟦ _ , pp , _ , _ ⟧ᶜ ⟦ _ , ccKeys , dep ⟧ᵛ (ccreghot c _) = case ¬? ((c , nothing) ∈? (ccKeys ˢ)) of λ where - (yes p) → success (-, GOVCERT-ccreghot{pp = pp} p) + (yes p) → success (-, GOVCERT-ccreghot p) (no ¬p) → failure (genErrors ¬p) Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT" Computational-GOVCERT .completeness ⟦ _ , pp , _ , _ ⟧ᶜ ⟦ dReps , _ , dep ⟧ᵛ diff --git a/src/Ledger/Conway/Conformance/Chain.agda b/src/Ledger/Conway/Conformance/Chain.agda index 7dd802c25..0abd04b85 100644 --- a/src/Ledger/Conway/Conformance/Chain.agda +++ b/src/Ledger/Conway/Conformance/Chain.agda @@ -15,7 +15,7 @@ module Ledger.Conway.Conformance.Chain open import Ledger.Enact govStructure open import Ledger.Conway.Conformance.Ledger txs abs -open import Ledger.Conway.Conformance.Ratify txs +open import Ledger.Ratify txs open import Ledger.Conway.Conformance.Utxo txs abs open import Ledger.Conway.Conformance.Epoch txs abs open import Ledger.Conway.Conformance.Certs govStructure diff --git a/src/Ledger/Conway/Conformance/Epoch.agda b/src/Ledger/Conway/Conformance/Epoch.agda index 445e139be..b1517dbfb 100644 --- a/src/Ledger/Conway/Conformance/Epoch.agda +++ b/src/Ledger/Conway/Conformance/Epoch.agda @@ -20,7 +20,7 @@ module Ledger.Conway.Conformance.Epoch open import Ledger.Conway.Conformance.Gov txs open import Ledger.Enact govStructure open import Ledger.Conway.Conformance.Ledger txs abs -open import Ledger.Conway.Conformance.Ratify txs +open import Ledger.Ratify txs open import Ledger.Conway.Conformance.Utxo txs abs open import Ledger.Conway.Conformance.Certs govStructure @@ -119,7 +119,7 @@ applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ stakeDistr : UTxO → DState → PState → Snapshot stakeDistr utxo ⟦ _ , stakeDelegs , rewards , _ ⟧ᵈ pState = ⟦ aggregate₊ (stakeRelation ᶠˢ) , stakeDelegs ⟧ˢ where - m = mapˢ (λ a → (a , cbalance (utxo ∣^' λ i → getStakeCred i ≡ just a))) (dom rewards) + m = mapˢ (λ a → (a , L.cbalance (utxo ∣^' λ i → getStakeCred i ≡ just a))) (dom rewards) stakeRelation = m ∪ proj₁ rewards gaDepositStake : GovState → Deposits → Credential ⇀ Coin diff --git a/src/Ledger/Conway/Conformance/Epoch/Properties.agda b/src/Ledger/Conway/Conformance/Epoch/Properties.agda index 5009dd3ab..380830101 100644 --- a/src/Ledger/Conway/Conformance/Epoch/Properties.agda +++ b/src/Ledger/Conway/Conformance/Epoch/Properties.agda @@ -13,8 +13,8 @@ module Ledger.Conway.Conformance.Epoch.Properties open import Ledger.Conway.Conformance.Epoch txs abs open import Ledger.Conway.Conformance.Ledger txs abs -open import Ledger.Conway.Conformance.Ratify txs -open import Ledger.Conway.Conformance.Ratify.Properties txs +open import Ledger.Ratify txs +open import Ledger.Ratify.Properties txs open import Ledger.Conway.Conformance.Certs govStructure open import Data.List using (filter) diff --git a/src/Ledger/Conway/Conformance/Gov.agda b/src/Ledger/Conway/Conformance/Gov.agda index 8d24842be..93fc0994c 100644 --- a/src/Ledger/Conway/Conformance/Gov.agda +++ b/src/Ledger/Conway/Conformance/Gov.agda @@ -11,7 +11,7 @@ open import Axiom.Set.Properties th using (∃-sublist-⇔) open import Ledger.GovernanceActions govStructure using (Vote) open import Ledger.Enact govStructure -open import Ledger.Conway.Conformance.Ratify txs hiding (vote) +open import Ledger.Ratify txs hiding (vote) open import Ledger.Conway.Conformance.Certs govStructure open import Data.List.Ext using (subpermutations; sublists) diff --git a/src/Ledger/Conway/Conformance/Gov/Properties.agda b/src/Ledger/Conway/Conformance/Gov/Properties.agda index 00ad0c73e..5f9ec1bbe 100644 --- a/src/Ledger/Conway/Conformance/Gov/Properties.agda +++ b/src/Ledger/Conway/Conformance/Gov/Properties.agda @@ -14,7 +14,7 @@ open import Axiom.Set.Properties open import Ledger.Enact govStructure open import Ledger.Conway.Conformance.Gov txs open import Ledger.GovernanceActions govStructure hiding (yes; no) -open import Ledger.Conway.Conformance.Ratify txs +open import Ledger.Ratify txs import Data.List.Membership.Propositional as P open import Data.List.Membership.Propositional.Properties diff --git a/src/Ledger/Conway/Conformance/Ledger.agda b/src/Ledger/Conway/Conformance/Ledger.agda index 5016dc0ff..f7ccdd78c 100644 --- a/src/Ledger/Conway/Conformance/Ledger.agda +++ b/src/Ledger/Conway/Conformance/Ledger.agda @@ -18,21 +18,13 @@ open import Ledger.Conway.Conformance.Utxo txs abs open import Ledger.Conway.Conformance.Utxow txs abs open import Ledger.Conway.Conformance.Certs govStructure +open import Ledger.Ledger txs abs public + using (LEnv; ⟦_,_,_,_,_⟧ˡᵉ) + open Tx open GState open GovActionState -record LEnv : Type where - - constructor ⟦_,_,_,_,_⟧ˡᵉ - field - - slot : Slot - ppolicy : Maybe ScriptHash - pparams : PParams - enactState : EnactState - treasury : Coin - record LState : Type where constructor ⟦_,_,_⟧ˡ diff --git a/src/Ledger/Conway/Conformance/Ledger/Properties.agda b/src/Ledger/Conway/Conformance/Ledger/Properties.agda index 978a08d7e..b87aba406 100644 --- a/src/Ledger/Conway/Conformance/Ledger/Properties.agda +++ b/src/Ledger/Conway/Conformance/Ledger/Properties.agda @@ -18,8 +18,8 @@ open import Ledger.Conway.Conformance.Certs.Properties govStructure open import Ledger.Conway.Conformance.Gov txs open import Ledger.Conway.Conformance.Gov.Properties txs open import Ledger.Conway.Conformance.Ledger txs abs -open import Ledger.Conway.Conformance.Ratify txs hiding (vote) -open import Ledger.Conway.Conformance.Utxo txs abs +open import Ledger.Ratify txs hiding (vote) +open import Ledger.Conway.Conformance.Utxo txs abs hiding (module L) open import Ledger.Conway.Conformance.Utxo.Properties txs abs open import Ledger.Conway.Conformance.Utxow txs abs open import Ledger.Conway.Conformance.Utxow.Properties txs abs diff --git a/src/Ledger/Conway/Conformance/PDF.agda b/src/Ledger/Conway/Conformance/PDF.agda index d88ee905c..b73185beb 100644 --- a/src/Ledger/Conway/Conformance/PDF.agda +++ b/src/Ledger/Conway/Conformance/PDF.agda @@ -4,7 +4,7 @@ module Ledger.Conway.Conformance.PDF where open import Ledger.Conway.Conformance.Script -open import Ledger.Conway.Conformance.ScriptValidation +open import Ledger.ScriptValidation open import Ledger.PParams open import Ledger.Types.GovStructure @@ -21,12 +21,12 @@ open import Ledger.Conway.Conformance.Utxow.Properties open import Ledger.Conway.Conformance.Ledger open import Ledger.Conway.Conformance.Ledger.Properties -open import Ledger.Conway.Conformance.Ratify.Properties +open import Ledger.Ratify.Properties open import Ledger.Conway.Conformance.Chain.Properties open import Ledger.Conway.Conformance.Gov open import Ledger.Enact -open import Ledger.Conway.Conformance.Ratify +open import Ledger.Ratify open import Ledger.Conway.Conformance.Chain diff --git a/src/Ledger/Conway/Conformance/Ratify.agda b/src/Ledger/Conway/Conformance/Ratify.agda deleted file mode 100644 index 593a7e26d..000000000 --- a/src/Ledger/Conway/Conformance/Ratify.agda +++ /dev/null @@ -1,332 +0,0 @@ - -{-# OPTIONS --safe #-} - -import Data.Integer as ℤ -open import Data.Rational as ℚ using (ℚ; 0ℚ; _⊔_) -open import Data.Nat.Properties hiding (_≟_; _≤?_) -open import Data.Nat.Properties.Ext - -open import Ledger.Prelude hiding (_∧_; _⊔_) renaming (filterᵐ to filter) -open import Ledger.Transaction hiding (Vote) - -module Ledger.Conway.Conformance.Ratify (txs : _) (open TransactionStructure txs) where - -open import Ledger.Certs govStructure -open import Ledger.Enact govStructure -open import Ledger.GovernanceActions govStructure using (Vote) - -infixr 2 _∧_ -_∧_ = _×_ - -instance - _ = +-0-commutativeMonoid - -private - ∣_∣_∣_∣ : {A : Type} → A → A → A → GovRole → A - ∣ q₁ ∣ q₂ ∣ q₃ ∣ = λ { CC → q₁ ; DRep → q₂ ; SPO → q₃ } - - ∣_∥_∣ : {A : Type} → A → A × A → GovRole → A - ∣ q₁ ∥ (q₂ , q₃) ∣ = λ { CC → q₁ ; DRep → q₂ ; SPO → q₃ } - -vote : ℚ → Maybe ℚ -vote = just - -defer : ℚ -defer = ℚ.1ℚ ℚ.+ ℚ.1ℚ - -maxThreshold : ℙ (Maybe ℚ) → Maybe ℚ -maxThreshold x = foldl comb nothing (proj₁ $ finiteness x) - where - comb : Maybe ℚ → Maybe ℚ → Maybe ℚ - comb (just x) (just y) = just (x ⊔ y) - comb (just x) nothing = just x - comb nothing (just y) = just y - comb nothing nothing = nothing - -─ : Maybe ℚ -─ = nothing -✓† = vote defer - -threshold : PParams → Maybe ℚ → GovAction → GovRole → Maybe ℚ -threshold pp ccThreshold = - - λ where - - NoConfidence → ∣ ─ ∣ vote P1 ∣ vote Q1 ∣ - (UpdateCommittee _ _ _) → ∣ ─ ∥ P/Q2a/b ∣ - (NewConstitution _ _) → ∣ ✓ ∣ vote P3 ∣ ─ ∣ - (TriggerHF _) → ∣ ✓ ∣ vote P4 ∣ vote Q4 ∣ - (ChangePParams x) → ∣ ✓ ∥ P/Q5 x ∣ - (TreasuryWdrl _) → ∣ ✓ ∣ vote P6 ∣ ─ ∣ - Info → ∣ ✓† ∣ ✓† ∣ ✓† ∣ - where - - open PParams pp - open DrepThresholds drepThresholds - open PoolThresholds poolThresholds - - ✓ = maybe just ✓† ccThreshold - - P/Q2a/b : Maybe ℚ × Maybe ℚ - P/Q2a/b = case ccThreshold of - - λ where - - (just _) → (vote P2a , vote Q2a) - nothing → (vote P2b , vote Q2b) - - pparamThreshold : PParamGroup → Maybe ℚ × Maybe ℚ - pparamThreshold NetworkGroup = (vote P5a , ─ ) - pparamThreshold EconomicGroup = (vote P5b , ─ ) - pparamThreshold TechnicalGroup = (vote P5c , ─ ) - pparamThreshold GovernanceGroup = (vote P5d , ─ ) - pparamThreshold SecurityGroup = (─ , vote Q5e ) - - P/Q5 : PParamsUpdate → Maybe ℚ × Maybe ℚ - P/Q5 ppu = maxThreshold (mapˢ (proj₁ ∘ pparamThreshold) (updateGroups ppu)) - , maxThreshold (mapˢ (proj₂ ∘ pparamThreshold) (updateGroups ppu)) - -canVote : PParams → GovAction → GovRole → Type -canVote pp a r = Is-just (threshold pp nothing a r) - -record StakeDistrs : Type where - - field - - stakeDistr : VDeleg ⇀ Coin - -record RatifyEnv : Type where - - field - - stakeDistrs : StakeDistrs - currentEpoch : Epoch - dreps : Credential ⇀ Epoch - ccHotKeys : Credential ⇀ Maybe Credential - treasury : Coin - pools : KeyHash ⇀ PoolParams - delegatees : Credential ⇀ VDeleg - -record RatifyState : Type where - - constructor ⟦_,_,_⟧ʳ - field - - es : EnactState - removed : ℙ (GovActionID × GovActionState) - delay : Bool - -CCData : Type -CCData = Maybe ((Credential ⇀ Epoch) × ℚ) - -govRole : VDeleg → GovRole -govRole (credVoter gv _) = gv -govRole abstainRep = DRep -govRole noConfidenceRep = DRep - -IsCC IsDRep IsSPO : VDeleg → Type -IsCC v = govRole v ≡ CC -IsDRep v = govRole v ≡ DRep -IsSPO v = govRole v ≡ SPO - -open StakeDistrs - -actualVotes : RatifyEnv → PParams → CCData → GovAction - → (GovRole × Credential ⇀ Vote) → (VDeleg ⇀ Vote) -actualVotes Γ pparams cc ga votes - = mapKeys (credVoter CC) actualCCVotes ∪ˡ actualPDRepVotes ga - ∪ˡ actualDRepVotes ∪ˡ actualSPOVotes ga - where - - open RatifyEnv Γ - open PParams pparams - - roleVotes : GovRole → VDeleg ⇀ Vote - roleVotes r = mapKeys (uncurry credVoter) (filter (λ (x , _) → r ≡ proj₁ x) votes) - - activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps) - spos = filterˢ IsSPO (dom (stakeDistr stakeDistrs)) - - getCCHotCred : Credential × Epoch → Maybe Credential - getCCHotCred (c , e) = case ¿ currentEpoch ≤ e ¿ᵇ , lookupᵐ? ccHotKeys c of - - λ where - - (true , just (just c')) → just c' - _ → nothing -- expired, no hot key or resigned - - SPODefaultVote : GovAction → VDeleg → Vote - SPODefaultVote ga (credVoter SPO (KeyHashObj kh)) = case lookupᵐ? pools kh of - λ where - nothing → Vote.no - (just p) → case lookupᵐ? delegatees (PoolParams.rewardAddr p) , ga of - λ where - (just noConfidenceRep , NoConfidence) → Vote.yes - (_ , TriggerHF _) → Vote.no - (just abstainRep , _) → Vote.abstain - _ → Vote.no - SPODefaultVote _ _ = Vote.no - - actualCCVote : Credential → Epoch → Vote - actualCCVote c e = case getCCHotCred (c , e) of - - λ where - - (just c') → maybe id Vote.no (lookupᵐ? votes (CC , c')) - _ → Vote.abstain - - actualCCVotes : Credential ⇀ Vote - actualCCVotes = case cc of - - λ where - - nothing → ∅ - (just (m , q)) → if ccMinSize ≤ lengthˢ (mapFromPartialFun getCCHotCred (m ˢ)) - then mapWithKey actualCCVote m - else constMap (dom m) Vote.no - - actualPDRepVotes : GovAction → VDeleg ⇀ Vote - actualPDRepVotes NoConfidence - = ❴ abstainRep , Vote.abstain ❵ ∪ˡ ❴ noConfidenceRep , Vote.yes ❵ - actualPDRepVotes _ = ❴ abstainRep , Vote.abstain ❵ ∪ˡ ❴ noConfidenceRep , Vote.no ❵ - - actualDRepVotes : VDeleg ⇀ Vote - actualDRepVotes = roleVotes DRep - ∪ˡ constMap (mapˢ (credVoter DRep) activeDReps) Vote.no - - actualSPOVotes : GovAction → VDeleg ⇀ Vote - actualSPOVotes a = roleVotes SPO ∪ˡ mapFromFun (SPODefaultVote a) spos - -open RatifyEnv using (stakeDistrs) - -abstract - -- unused, keep until we know for sure that there'll be no minimum AVS - -- activeVotingStake : ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin - -- activeVotingStake cc dists votes = - -- ∑[ x ← getStakeDist DRep cc dists ∣ dom votes ᶜ ᶠᵐ ] x - - -- TODO: explain this notation in the prose and it's purpose: - -- if there's no stake, accept only if threshold is zero - _/₀_ : ℕ → ℕ → ℚ - x /₀ 0 = 0ℚ - x /₀ y@(suc _) = ℤ.+ x ℚ./ y - - getStakeDist : GovRole → ℙ VDeleg → StakeDistrs → VDeleg ⇀ Coin - getStakeDist CC cc sd = constMap (filterˢ IsCC cc) 1 - getStakeDist DRep _ sd = filterKeys IsDRep (sd .stakeDistr) - getStakeDist SPO _ sd = filterKeys IsSPO (sd .stakeDistr) - - acceptedStakeRatio : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → ℚ - acceptedStakeRatio r cc dists votes = acceptedStake /₀ totalStake - where - dist : VDeleg ⇀ Coin - dist = getStakeDist r cc dists - acceptedStake totalStake : Coin - acceptedStake = ∑[ x ← dist ∣ votes ⁻¹ Vote.yes ] x - totalStake = ∑[ x ← dist ∣ dom (votes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x - - acceptedBy : RatifyEnv → EnactState → GovActionState → GovRole → Type - acceptedBy Γ (record { cc = cc , _; pparams = pparams , _ }) gs role = - let open GovActionState gs; open PParams pparams - votes' = actualVotes Γ pparams cc action votes - mbyT = threshold pparams (proj₂ <$> cc) action role - t = maybe id 0ℚ mbyT - in acceptedStakeRatio role (dom votes') (stakeDistrs Γ) votes' ≥ t - ∧ (role ≡ CC → maybe (λ (m , _) → lengthˢ m) 0 cc ≥ ccMinSize ⊎ Is-nothing mbyT) - - accepted : RatifyEnv → EnactState → GovActionState → Type - accepted Γ es gs = acceptedBy Γ es gs CC ∧ acceptedBy Γ es gs DRep ∧ acceptedBy Γ es gs SPO - - expired : Epoch → GovActionState → Type - expired current record { expiresIn = expiresIn } = expiresIn < current - -open EnactState - -verifyPrev : (a : GovAction) → NeedsHash a → EnactState → Type -verifyPrev NoConfidence h es = h ≡ es .cc .proj₂ -verifyPrev (UpdateCommittee _ _ _) h es = h ≡ es .cc .proj₂ -verifyPrev (NewConstitution _ _) h es = h ≡ es .constitution .proj₂ -verifyPrev (TriggerHF _) h es = h ≡ es .pv .proj₂ -verifyPrev (ChangePParams _) h es = h ≡ es .pparams .proj₂ -verifyPrev (TreasuryWdrl _) _ _ = ⊤ -verifyPrev Info _ _ = ⊤ - -delayingAction : GovAction → Bool -delayingAction NoConfidence = true -delayingAction (UpdateCommittee _ _ _) = true -delayingAction (NewConstitution _ _) = true -delayingAction (TriggerHF _) = true -delayingAction (ChangePParams _) = false -delayingAction (TreasuryWdrl _) = false -delayingAction Info = false - -delayed : (a : GovAction) → NeedsHash a → EnactState → Bool → Type -delayed a h es d = ¬ verifyPrev a h es ⊎ d ≡ true - -acceptConds : RatifyEnv → RatifyState → GovActionID × GovActionState → Type -acceptConds Γ ⟦ es , removed , d ⟧ʳ (id , st) = let open RatifyEnv Γ; open GovActionState st in - accepted Γ es st - × ¬ delayed action prevAction es d - × ∃[ es' ] ⟦ id , treasury , currentEpoch ⟧ᵉ ⊢ es ⇀⦇ action ,ENACT⦈ es' - -abstract - verifyPrev? : ∀ a h es → Dec (verifyPrev a h es) - verifyPrev? NoConfidence h es = dec - verifyPrev? (UpdateCommittee x x₁ x₂) h es = dec - verifyPrev? (NewConstitution x x₁) h es = dec - verifyPrev? (TriggerHF x) h es = dec - verifyPrev? (ChangePParams x) h es = dec - verifyPrev? (TreasuryWdrl x) h es = dec - verifyPrev? Info h es = dec - - delayed? : ∀ a h es d → Dec (delayed a h es d) - delayed? a h es d = let instance _ = ⁇ verifyPrev? a h es in dec - - Is-nothing? : ∀ {A : Set} {x : Maybe A} → Dec (Is-nothing x) - Is-nothing? {x = x} = All.dec (const $ no id) x - where - import Data.Maybe.Relation.Unary.All as All - - acceptedBy? : ∀ Γ es st role → Dec (acceptedBy Γ es st role) - acceptedBy? _ _ _ _ = _ ℚ.≤? _ ×-dec _ ≟ _ →-dec (_ ≥? _ ⊎-dec Is-nothing?) - where - import Relation.Nullary.Decidable as Dec - - accepted? : ∀ Γ es st → Dec (accepted Γ es st) - accepted? Γ es st = let a = λ {x} → acceptedBy? Γ es st x in a ×-dec a ×-dec a - - expired? : ∀ e st → Dec (expired e st) - expired? e st = ¿ expired e st ¿ - -private variable - es es' : EnactState - a : GovActionID × GovActionState - removed : ℙ (GovActionID × GovActionState) - d : Bool - -data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × GovActionState → RatifyState → Type where - - - RATIFY-Accept : ∀ {Γ} {es} {removed} {d} {a} {es'} → let open RatifyEnv Γ; st = a .proj₂; open GovActionState st in - ∙ acceptConds Γ ⟦ es , removed , d ⟧ʳ a - ∙ ⟦ a .proj₁ , treasury , currentEpoch ⟧ᵉ ⊢ es ⇀⦇ action ,ENACT⦈ es' - ──────────────────────────────── - Γ ⊢ ⟦ es , removed , d ⟧ʳ ⇀⦇ a ,RATIFY'⦈ - ⟦ es' , ❴ a ❵ ∪ removed , delayingAction action ⟧ʳ - - RATIFY-Reject : ∀ {Γ} {es} {removed} {d} {a} → let open RatifyEnv Γ; st = a .proj₂ in - ∙ ¬ acceptConds Γ ⟦ es , removed , d ⟧ʳ a - ∙ expired currentEpoch st - ──────────────────────────────── - Γ ⊢ ⟦ es , removed , d ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es , ❴ a ❵ ∪ removed , d ⟧ʳ - - RATIFY-Continue : ∀ {Γ} {es} {removed} {d} {a} → let open RatifyEnv Γ; st = a .proj₂ in - ∙ ¬ acceptConds Γ ⟦ es , removed , d ⟧ʳ a - ∙ ¬ expired currentEpoch st - ──────────────────────────────── - Γ ⊢ ⟦ es , removed , d ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es , removed , d ⟧ʳ - -_⊢_⇀⦇_,RATIFY⦈_ : RatifyEnv → RatifyState → List (GovActionID × GovActionState) - → RatifyState → Type -_⊢_⇀⦇_,RATIFY⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,RATIFY'⦈_ - diff --git a/src/Ledger/Conway/Conformance/Ratify/Properties.agda b/src/Ledger/Conway/Conformance/Ratify/Properties.agda deleted file mode 100644 index 50fde0a47..000000000 --- a/src/Ledger/Conway/Conformance/Ratify/Properties.agda +++ /dev/null @@ -1,72 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Ledger.Prelude -open import Ledger.Transaction - -module Ledger.Conway.Conformance.Ratify.Properties (txs : _) (open TransactionStructure txs) where - -open import Ledger.Conway.Conformance.Gov txs -open import Ledger.GovernanceActions.Properties govStructure -open import Ledger.Enact govStructure -open import Ledger.Conway.Conformance.Ratify txs - -open Computational ⦃...⦄ hiding (computeProof; completeness) - -private - module Implementation - Γ (s : RatifyState) (sig : _ × _) - (let ⟦ es , removed , d ⟧ʳ = s) - (let gid , st = sig) - where - open RatifyEnv Γ; open GovActionState st - es' = compute ⟦ gid , treasury , currentEpoch ⟧ᵉ es action - acc? = accepted? Γ es st - exp? = expired? currentEpoch st - del? = delayed? action prevAction es d - - opaque - acceptConds? : ∀ a → Dec (acceptConds Γ s a) - acceptConds? _ = Dec-× ⦃ ⁇ accepted? _ _ _ ⦄ - ⦃ Dec-× ⦃ Dec-→ ⦃ ⁇ delayed? _ _ _ _ ⦄ ⦄ ⦃ ⁇ Computational⇒Dec' ⦄ ⦄ .dec - - RATIFY'-total : ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY'⦈ s' - RATIFY'-total - with acceptConds? sig | exp? - ... | yes p@(_ , _ , (_ , q)) | _ = -, RATIFY-Accept (p , q) - ... | no ¬p | no ¬a = -, RATIFY-Continue (¬p , ¬a) - ... | no ¬p | yes a = -, RATIFY-Reject (¬p , a) - - computeProof = success {Err = ⊥} RATIFY'-total - - RATIFY'-completeness : ∀ s' → Γ ⊢ s ⇀⦇ sig ,RATIFY'⦈ s' → RATIFY'-total .proj₁ ≡ s' - RATIFY'-completeness ⟦ x , _ , _ ⟧ʳ (RATIFY-Accept (p , a)) with acceptConds? sig - ... | no ¬h = ⊥-elim (¬h p) - ... | yes (_ , _ , _ , h) = cong ⟦_, _ , _ ⟧ʳ $ computational⇒rightUnique Computational-ENACT h a - RATIFY'-completeness s' (RATIFY-Reject (¬p , a)) - rewrite dec-no (acceptConds? _) ¬p | dec-yes exp? a .proj₂ = refl - RATIFY'-completeness s' (RATIFY-Continue (¬p , ¬a)) - rewrite dec-no (acceptConds? _) ¬p | dec-no exp? ¬a = refl - - completeness = cong (success {Err = ⊥}) ∘₂ RATIFY'-completeness - -instance - Computational-RATIFY' : Computational _⊢_⇀⦇_,RATIFY'⦈_ ⊥ - Computational-RATIFY' = record {Implementation} - -Computational-RATIFY : Computational _⊢_⇀⦇_,RATIFY⦈_ ⊥ -Computational-RATIFY = it - -RATIFY-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' -RATIFY-total = ReflexiveTransitiveClosure-total (Implementation.RATIFY'-total _ _ _) - -RATIFY-complete : ∀ {Γ s sig s'} → - Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' → RATIFY-total {Γ} {s} {sig} .proj₁ ≡ s' -RATIFY-complete = computational⇒rightUnique Computational-RATIFY (RATIFY-total .proj₂) - -opaque - RATIFY-total' : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' - RATIFY-total' = RATIFY-total - - RATIFY-complete' : ∀ {Γ s sig s'} → - Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' → RATIFY-total' {Γ} {s} {sig} .proj₁ ≡ s' - RATIFY-complete' = RATIFY-complete diff --git a/src/Ledger/Conway/Conformance/ScriptValidation.agda b/src/Ledger/Conway/Conformance/ScriptValidation.agda deleted file mode 100644 index 928107dba..000000000 --- a/src/Ledger/Conway/Conformance/ScriptValidation.agda +++ /dev/null @@ -1,186 +0,0 @@ -{-# OPTIONS --safe #-} - -import Data.Maybe as M - -open import Tactic.AnyOf -open import Tactic.Assumption - -open import Ledger.Prelude; open Properties -open import Ledger.Transaction -open import Ledger.Abstract -open import Ledger.Crypto - -module Ledger.Conway.Conformance.ScriptValidation - (txs : _) (open TransactionStructure txs) - (abs : AbstractFunctions txs) (open AbstractFunctions abs) (open indexOf indexOfImp) - where - -open import Ledger.Certs govStructure - -instance - _ = DecEq-Slot - -data ScriptPurpose : Type where - Cert : DCert → ScriptPurpose - Rwrd : RwdAddr → ScriptPurpose - Mint : ScriptHash → ScriptPurpose - Spend : TxIn → ScriptPurpose - Vote : Voter → ScriptPurpose - Propose : GovProposal → ScriptPurpose - -rdptr : TxBody → ScriptPurpose → Maybe RdmrPtr -rdptr txb = λ where - (Cert h) → M.map (Cert ,_) $ indexOfDCert h txcerts - (Rwrd h) → M.map (Rewrd ,_) $ indexOfRwdAddr h txwdrls - (Mint h) → M.map (Mint ,_) $ indexOfPolicyId h (policies mint) - (Spend h) → M.map (Spend ,_) $ indexOfTxIn h txins - (Vote h) → M.map (Vote ,_) $ indexOfVote h (map GovVote.voter txvote) - (Propose h) → M.map (Propose ,_) $ indexOfProposal h txprop - where open TxBody txb - -indexedRdmrs : Tx → ScriptPurpose → Maybe (Redeemer × ExUnits) -indexedRdmrs tx sp = maybe (λ x → lookupᵐ? txrdmrs x) nothing (rdptr body sp) - where open Tx tx; open TxWitnesses wits - -getDatum : Tx → UTxO → ScriptPurpose → List Datum -getDatum tx utxo (Spend txin) = let open Tx tx; open TxWitnesses wits in - maybe - (λ { (_ , _ , just (inj₂ h), _) → maybe [_] [] (lookupᵐ? txdats h) - ; (_ , _ , just (inj₁ d), _) → [ d ] - ; (_ , _ , nothing , _) → [] }) - [] - (lookupᵐ? utxo txin) -getDatum tx utxo _ = [] - -record TxInfo : Type where - field realizedInputs : UTxO - txouts : Ix ⇀ TxOut - fee : Value - mint : Value - txcerts : List DCert - txwdrls : Wdrl - txvldt : Maybe Slot × Maybe Slot - vkKey : ℙ KeyHash - txdats : DataHash ⇀ Datum - txid : TxId - -txInfo : Language → PParams - → UTxO - → Tx - → TxInfo -txInfo l pp utxo tx = record - { TxBody body - ; TxWitnesses wits - ; realizedInputs = utxo ∣ txins - ; fee = inject txfee - ; mint = mint - ; vkKey = reqSigHash - } where open Tx tx; open TxBody body - -data DelegateOrDeReg : DCert → Type where instance - delegate : ∀ {x y z w} → DelegateOrDeReg (delegate x y z w) - dereg : ∀ {x y} → DelegateOrDeReg (dereg x y) - regdrep : ∀ {x y z} → DelegateOrDeReg (regdrep x y z) - deregdrep : ∀ {x y} → DelegateOrDeReg (deregdrep x y) - -instance - Dec-DelegateOrDeReg : DelegateOrDeReg ⁇¹ - Dec-DelegateOrDeReg {dc} .dec with dc - ... | delegate _ _ _ _ = yes it - ... | dereg _ _ = yes it - ... | regdrep _ _ _ = yes it - ... | deregdrep _ _ = yes it - ... | regpool _ _ = no λ () - ... | retirepool _ _ = no λ () - ... | ccreghot _ _ = no λ () - -UTxOSH = TxIn ⇀ (TxOut × ScriptHash) - -scriptOutWithHash : TxIn → TxOut → Maybe (TxOut × ScriptHash) -scriptOutWithHash txin (addr , r) = - if isScriptAddr addr then - (λ {p} → just ((addr , r) , getScriptHash addr p)) - else - nothing - -scriptOutsWithHash : UTxO → UTxOSH -scriptOutsWithHash utxo = mapMaybeWithKeyᵐ scriptOutWithHash utxo - -spendScripts : TxIn → UTxOSH → Maybe (ScriptPurpose × ScriptHash) -spendScripts txin utxo = - if txin ∈ dom utxo then - (λ {p} → just (Spend txin , proj₂ (lookupᵐ utxo txin))) - else - nothing - -rwdScripts : RwdAddr → Maybe (ScriptPurpose × ScriptHash) -rwdScripts a = - if isScriptRwdAddr a then - (λ where {SHisScript sh} → just (Rwrd a , sh)) - else - nothing - -certScripts : DCert → Maybe (ScriptPurpose × ScriptHash) -certScripts d with ¿ DelegateOrDeReg d ¿ -... | no ¬p = nothing -certScripts c@(delegate (KeyHashObj x) _ _ _) | yes p = nothing -certScripts c@(delegate (ScriptObj y) _ _ _) | yes p = just (Cert c , y) -certScripts c@(dereg (KeyHashObj x) _) | yes p = nothing -certScripts c@(dereg (ScriptObj y) _) | yes p = just (Cert c , y) -certScripts c@(regdrep (KeyHashObj x) _ _) | yes p = nothing -certScripts c@(regdrep (ScriptObj y) _ _) | yes p = just (Cert c , y) -certScripts c@(deregdrep (KeyHashObj x) _) | yes p = nothing -certScripts c@(deregdrep (ScriptObj y) _) | yes p = just (Cert c , y) - -private - scriptsNeeded : UTxO → TxBody → ℙ (ScriptPurpose × ScriptHash) - scriptsNeeded utxo txb - = mapPartial (λ x → spendScripts x (scriptOutsWithHash utxo)) txins - ∪ mapPartial (λ x → rwdScripts x) (dom $ txwdrls .proj₁) - ∪ mapPartial (λ x → certScripts x) (fromList txcerts) - ∪ mapˢ (λ x → Mint x , x) (policies mint) - where open TxBody txb - -valContext : TxInfo → ScriptPurpose → Data -valContext txinfo sp = toData (txinfo , sp) - --- need to get map from language script ↦ cm --- need to update costmodels to add the language map in order to check --- (Language ↦ CostModel) ∈ costmdls ↦ (Language ↦ CostModel) - - -opaque - - collectPhaseTwoScriptInputs' : PParams → Tx → UTxO → (ScriptPurpose × ScriptHash) - → Maybe (Script × List Data × ExUnits × CostModel) - collectPhaseTwoScriptInputs' pp tx utxo (sp , sh) - with lookupScriptHash sh tx utxo - ... | nothing = nothing - ... | just s - with isInj₂ s | indexedRdmrs tx sp - ... | just p2s | just (rdmr , eu) - = just (s , - ( (getDatum tx utxo sp ++ rdmr ∷ valContext (txInfo (language p2s) pp utxo tx) sp ∷ []) - , eu - , PParams.costmdls pp) - ) - ... | x | y = nothing - - collectPhaseTwoScriptInputs : PParams → Tx → UTxO - → List (Script × List Data × ExUnits × CostModel) - collectPhaseTwoScriptInputs pp tx utxo - = setToList - $ mapPartial (collectPhaseTwoScriptInputs' pp tx utxo) - $ scriptsNeeded utxo (tx .Tx.body) - -open TxBody -open Tx - -⟦_⟧,_,_,_ : P2Script → CostModel → ExUnits → List Data → Bool -⟦ s ⟧, cm , eu , d = runPLCScript cm s eu d - -evalScripts : Tx → List (Script × List Data × ExUnits × CostModel) → Bool -evalScripts tx [] = true -evalScripts tx ((inj₁ tl , d , eu , cm) ∷ Γ) = - ¿ validP1Script (reqSigHash (body tx)) (txvldt (body tx)) tl ¿ᵇ ∧ evalScripts tx Γ -evalScripts tx ((inj₂ ps , d , eu , cm) ∷ Γ) = ⟦ ps ⟧, cm , eu , d ∧ evalScripts tx Γ diff --git a/src/Ledger/Conway/Conformance/Utxo.agda b/src/Ledger/Conway/Conformance/Utxo.agda index 1470791f1..7dcccab7c 100644 --- a/src/Ledger/Conway/Conformance/Utxo.agda +++ b/src/Ledger/Conway/Conformance/Utxo.agda @@ -20,10 +20,13 @@ module Ledger.Conway.Conformance.Utxo (abs : AbstractFunctions txs) (open AbstractFunctions abs) where -open import Ledger.Conway.Conformance.ScriptValidation txs abs +open import Ledger.ScriptValidation txs abs open import Ledger.Fees txs using (scriptsCost) open import Ledger.Conway.Conformance.Certs govStructure +module L where + open import Ledger.Utxo txs abs public + open PParams instance @@ -44,31 +47,12 @@ updateCertDeposits pp (deregdrep c v ∷ certs) deposits updateCertDeposits pp (_ ∷ certs) deposits = updateCertDeposits pp certs deposits --- -- Unchanged/defined in Utxo module: -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) + ∘ L.updateProposalDeposits txprop txid (pp .govActionDeposit) where open TxBody txb -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 +open L public using (UTxOEnv; UTxOState; ⟦_,_,_,_⟧ᵘ) private variable Γ : UTxOEnv @@ -77,50 +61,6 @@ private variable open PParams -_*↓_ : ℚ.ℚ → ℕ → ℕ -q *↓ n = ℤ.∣ ℚ.⌊ q ℚ.* (ℤ.+ n ℚ./ 1) ⌋ ∣ - -isTwoPhaseScriptAddress : Tx → UTxO → Addr → Bool -isTwoPhaseScriptAddress tx utxo a = - if isScriptAddr a then - (λ {p} → if lookupScriptHash (getScriptHash a p) tx utxo - then (λ {s} → isP2Script s) - else false) - else - false - -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 ≡ true) - (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 - -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 = ∑[ x ← mapValues scriptSize (setToHashMap (refScripts tx utxo)) ] x - - minfee : (pp : 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) - data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type where Scripts-Yes : ∀ {Γ} {s} {tx} @@ -132,7 +72,7 @@ data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Typ ∙ evalScripts tx sLst ≡ isValid ∙ isValid ≡ true ──────────────────────────────── - Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ ⟦ (utxo ∣ txins ᶜ) ∪ˡ (outs txb) + Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ ⟦ (utxo ∣ txins ᶜ) ∪ˡ (L.outs txb) , fees + txfee , deposits , donations + txdonation @@ -149,7 +89,7 @@ data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Typ ∙ isValid ≡ false ──────────────────────────────── Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ ⟦ utxo ∣ collateral ᶜ - , fees + cbalance (utxo ∣ collateral) + , fees + L.cbalance (utxo ∣ collateral) , deposits , donations ⟧ᵘ @@ -157,67 +97,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) -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 - HasCoin-UTxO : HasCoin UTxO - HasCoin-UTxO .getCoin = cbalance - -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 - --- Boolean implication -_=>ᵇ_ : Bool → Bool → Bool -a =>ᵇ b = if a then b else true - --- Boolean-valued inequalities on natural numbers -_≤ᵇ_ _≥ᵇ_ : ℕ → ℕ → Bool -m ≤ᵇ n = ¿ m ≤ n ¿ᵇ -_≥ᵇ_ = flip _≤ᵇ_ - -≟-∅ᵇ : {A : Type} ⦃ _ : DecEq A ⦄ → (X : ℙ A) → Bool -≟-∅ᵇ X = ¿ X ≡ ∅ ¿ᵇ - -coinPolicies : ℙ ScriptHash -coinPolicies = policies (inject 1) - -isAdaOnlyᵇ : Value → Bool -isAdaOnlyᵇ v = toBool (policies v ≡ᵉ coinPolicies) - -feesOK : PParams → Tx → UTxO → Bool -feesOK pp tx utxo = ( minfee pp utxo tx ≤ᵇ txfee ∧ not (≟-∅ᵇ (txrdmrs ˢ)) - =>ᵇ ( allᵇ (λ (addr , _) → ¿ isVKeyAddr addr ¿) collateralRange - ∧ isAdaOnlyᵇ bal - ∧ (coin bal * 100) ≥ᵇ (txfee * pp .collateralPercentage) - ∧ not (≟-∅ᵇ collateral) - ) - ) - where - open Tx tx; open TxBody body; open TxWitnesses wits; open PParams pp - collateralRange = range ((mapValues txOutHash utxo) ∣ collateral) - bal = balance (utxo ∣ collateral) - depositsChange : PParams → TxBody → Deposits → ℤ depositsChange pp txb deposits = getCoin (updateDeposits pp txb deposits) - getCoin deposits @@ -231,35 +110,18 @@ module _ (let open UTxOState; open TxBody) where consumed : PParams → UTxOState → TxBody → Value consumed pp st txb - = balance (st .utxo ∣ txb .txins) + = 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 - = balance (outs txb) + = L.balance (L.outs txb) + inject (txb .txfee) + inject (newDeposits pp st txb) + inject (txb .txdonation) -utxoEntrySizeWithoutVal : MemoryEstimate -utxoEntrySizeWithoutVal = 8 - -utxoEntrySize : TxOutʰ → MemoryEstimate -utxoEntrySize o = utxoEntrySizeWithoutVal + size (getValueʰ o) - -data _≡?_ {A : Type} : Maybe A → A → Type where - ≡?-nothing : ∀ {x : A} → nothing ≡? x - ≡?-just : ∀ {x : A} → (just x) ≡? x - -instance - ≟? : {A : Type} {x : Maybe A} {y : A} → ⦃ DecEq A ⦄ → (x ≡? y) ⁇ - ≟? {x = just x} {y} with x ≟ y - ... | yes refl = ⁇ yes ≡?-just - ... | no ¬p = ⁇ no λ where ≡?-just → ¬p refl - ≟? {x = nothing} = ⁇ yes ≡?-nothing - data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type where UTXO-inductive : @@ -270,21 +132,21 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type overhead = 160 in ∙ txins ≢ ∅ ∙ txins ∪ refInputs ⊆ dom utxo - ∙ txins ∩ refInputs ≡ ∅ ∙ inInterval slot txvldt - ∙ feesOK pp tx utxo ≡ true ∙ consumed pp s txb ≡ produced pp s txb + ∙ txins ∩ refInputs ≡ ∅ ∙ L.inInterval slot txvldt + ∙ L.feesOK pp tx utxo ≡ true ∙ consumed pp s txb ≡ produced pp s txb ∙ coin mint ≡ 0 ∙ txsize ≤ maxTxSize pp - ∙ refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx + ∙ L.refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx ∙ ∀[ (_ , txout) ∈ txoutsʰ .proj₁ ] - inject ((overhead + utxoEntrySize txout) * coinsPerUTxOByte pp) ≤ᵗ getValueʰ txout + inject ((overhead + L.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 ≡? NetworkId - ∙ curTreasury ≡? treasury + ∙ txNetworkId L.≡? NetworkId + ∙ curTreasury L.≡? treasury ∙ Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s' ──────────────────────────────── Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s' diff --git a/src/Ledger/Conway/Conformance/Utxo/Properties.agda b/src/Ledger/Conway/Conformance/Utxo/Properties.agda index a0d072235..66d2a108d 100644 --- a/src/Ledger/Conway/Conformance/Utxo/Properties.agda +++ b/src/Ledger/Conway/Conformance/Utxo/Properties.agda @@ -12,7 +12,7 @@ open import Data.Nat.Properties hiding (_≟_) open import Data.String.Base renaming (_++_ to _+ˢ_) using () open import Interface.ComputationalRelation open import Ledger.Prelude hiding (≤-trans; ≤-antisym; All); open Properties -open import Ledger.Conway.Conformance.ScriptValidation txs abs +open import Ledger.ScriptValidation txs abs open import Ledger.Conway.Conformance.Utxo txs abs open import Ledger.Conway.Conformance.Certs govStructure open import Prelude diff --git a/src/Ledger/Conway/Conformance/Utxow.agda b/src/Ledger/Conway/Conformance/Utxow.agda index 3ef1b1ce5..cb689b920 100644 --- a/src/Ledger/Conway/Conformance/Utxow.agda +++ b/src/Ledger/Conway/Conformance/Utxow.agda @@ -10,93 +10,13 @@ module Ledger.Conway.Conformance.Utxow (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where -open import Ledger.Conway.Conformance.Utxo txs abs -open import Ledger.Conway.Conformance.ScriptValidation txs abs +open import Ledger.Conway.Conformance.Utxo txs abs hiding (module L) +open import Ledger.ScriptValidation txs abs open import Ledger.Certs govStructure -module _ (o : TxOut) where - d = proj₁ (proj₂ (proj₂ o)) - data HasInlineDatum : Set where - InlineDatum : ∀ {d'} → d ≡ just (inj₁ d') → HasInlineDatum - -instance - Dec-HasInlineDatum : ∀ {o} → HasInlineDatum o ⁇ - Dec-HasInlineDatum {_ , _ , just (inj₁ x) , _} = ⁇ yes (InlineDatum refl) - Dec-HasInlineDatum {_ , _ , just (inj₂ x) , _} = ⁇ no λ where - (InlineDatum x) → case x of λ () - Dec-HasInlineDatum {_ , _ , nothing , _} = ⁇ no λ where - (InlineDatum x) → case x of λ () - -module _ (txb : TxBody) (let open TxBody txb) where - data UsesV3Features : Set where - HasVotes : txvote ≢ [] → UsesV3Features - HasProps : txprop ≢ [] → UsesV3Features - HasDonation : txdonation ≢ 0 → UsesV3Features - HasTreasury : curTreasury ≢ nothing → UsesV3Features - -instance - Dec-UsesV3Features : ∀ {txb} → UsesV3Features txb ⁇ - Dec-UsesV3Features {record { txvote = [] ; txprop = [] ; txdonation = zero ; curTreasury = nothing }} - = ⁇ no λ where (HasVotes x) → x refl - (HasProps x) → x refl - (HasDonation x) → x refl - (HasTreasury x) → x refl - Dec-UsesV3Features {record { txvote = [] ; txprop = [] ; txdonation = zero ; curTreasury = just x }} - = ⁇ yes (HasTreasury (λ ())) - Dec-UsesV3Features {record { txvote = [] ; txprop = [] ; txdonation = suc txdonation }} - = ⁇ yes (HasDonation (λ ())) - Dec-UsesV3Features {record { txvote = [] ; txprop = x ∷ txprop }} = ⁇ yes (HasProps (λ ())) - Dec-UsesV3Features {record { txvote = x ∷ txvote }} = ⁇ yes (HasVotes (λ ())) - -languages : Tx → UTxO → ℙ Language -languages tx utxo = mapPartial getLanguage (txscripts tx utxo) - where - getLanguage : Script → Maybe Language - getLanguage (inj₁ _) = nothing - getLanguage (inj₂ s) = just (language s) - -getVKeys : ℙ Credential → ℙ KeyHash -getVKeys = mapPartial isKeyHashObj - -allowedLanguages : Tx → UTxO → ℙ Language -allowedLanguages tx utxo = - if (∃[ o ∈ os ] isBootstrapAddr (proj₁ o)) - then ∅ - else if UsesV3Features txb - then fromList (PlutusV3 ∷ []) - else if ∃[ o ∈ os ] HasInlineDatum o - then fromList (PlutusV2 ∷ PlutusV3 ∷ []) - else - fromList (PlutusV1 ∷ PlutusV2 ∷ PlutusV3 ∷ []) - where - txb = tx .Tx.body; open TxBody txb - os = range (outs txb) ∪ range (utxo ∣ (txins ∪ refInputs)) - -getScripts : ℙ Credential → ℙ ScriptHash -getScripts = mapPartial isScriptObj - -credsNeeded : UTxO → TxBody → ℙ (ScriptPurpose × Credential) -credsNeeded utxo txb - = mapˢ (λ (i , o) → (Spend i , payCred (proj₁ o))) ((utxo ∣ txins) ˢ) - ∪ mapˢ (λ a → (Rwrd a , stake a)) (dom (txwdrls .proj₁)) - ∪ mapˢ (λ c → (Cert c , cwitness c)) (fromList txcerts) - ∪ mapˢ (λ x → (Mint x , ScriptObj x)) (policies mint) - ∪ mapˢ (λ v → (Vote v , proj₂ v)) (fromList (map voter txvote)) - ∪ mapPartial (λ p → case p .policy of - - λ where - - (just sh) → just (Propose p , ScriptObj sh) - nothing → nothing) (fromList txprop) - - where open TxBody txb; open GovVote; open RwdAddr; open GovProposal - - -witsVKeyNeeded : UTxO → TxBody → ℙ KeyHash -witsVKeyNeeded = getVKeys ∘ mapˢ proj₂ ∘ credsNeeded - -scriptsNeeded : UTxO → TxBody → ℙ ScriptHash -scriptsNeeded = getScripts ∘ mapˢ proj₂ ∘ credsNeeded +module L where + open import Ledger.Utxow txs abs public + open import Ledger.Utxo txs abs public data @@ -114,19 +34,19 @@ data _⊢_⇀⦇_,UTXOW⦈_ where open UTxOState s witsKeyHashes = mapˢ hash (dom vkSigs) witsScriptHashes = mapˢ hash scripts - inputHashes = getInputHashes tx utxo + inputHashes = L.getInputHashes tx utxo refScriptHashes = mapˢ hash (refScripts tx utxo) - neededHashes = scriptsNeeded utxo txb + neededHashes = L.scriptsNeeded utxo txb txdatsHashes = dom txdats - allOutHashes = getDataHashes (range txouts) + allOutHashes = L.getDataHashes (range txouts) in ∙ ∀[ (vk , σ) ∈ vkSigs ] isSigned vk (txidBytes txid) σ ∙ ∀[ s ∈ mapPartial isInj₁ (txscripts tx utxo) ] validP1Script witsKeyHashes txvldt s - ∙ witsVKeyNeeded utxo txb ⊆ witsKeyHashes + ∙ L.witsVKeyNeeded utxo txb ⊆ witsKeyHashes ∙ neededHashes ＼ refScriptHashes ≡ᵉ witsScriptHashes ∙ inputHashes ⊆ txdatsHashes - ∙ txdatsHashes ⊆ inputHashes ∪ allOutHashes ∪ getDataHashes (range (utxo ∣ refInputs)) - ∙ languages tx utxo ⊆ allowedLanguages tx utxo + ∙ txdatsHashes ⊆ inputHashes ∪ allOutHashes ∪ L.getDataHashes (range (utxo ∣ refInputs)) + ∙ L.languages tx utxo ⊆ L.allowedLanguages tx utxo ∙ txADhash ≡ map hash txAD ∙ Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s' ──────────────────────────────── diff --git a/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda b/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda index afd2f7989..0cb0d4411 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda @@ -13,8 +13,8 @@ open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length) import Data.Rational.Show as Rational import Foreign.Haskell.Pair as F -open import Ledger.Conway.Conformance.Ratify it -open import Ledger.Conway.Conformance.Ratify.Properties it +open import Ledger.Ratify it +open import Ledger.Ratify.Properties it instance HsTy-StakeDistrs = autoHsType StakeDistrs diff --git a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda index 3c0d56f42..78eb17fa2 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda @@ -36,14 +36,14 @@ module _ (ext : ExternalFunctions) where utxo-step : HsType (UTxOEnv → UTxOState → Tx → ComputationResult String UTxOState) utxo-step = to (coerce ⦃ TrustMe ⦄ $ compute Computational-UTXO) - + {-# COMPILE GHC utxo-step as utxoStep #-} utxow-step : HsType (UTxOEnv → UTxOState → Tx → ComputationResult String UTxOState) utxow-step = to (coerce ⦃ TrustMe ⦄ $ compute Computational-UTXOW) - + {-# COMPILE GHC utxow-step as utxowStep #-} - + utxo-debug : HsType (UTxOEnv → UTxOState → Tx → String) utxo-debug env st tx = let open Tx (from tx) @@ -52,17 +52,17 @@ module _ (ext : ExternalFunctions) where open UTxOEnv (from env) in unlines $ "Consumed:" ∷ - ("\tInputs: \t" +ˢ show (balance (utxo ∣ txins))) ∷ + ("\tInputs: \t" +ˢ show (L.balance (utxo ∣ txins))) ∷ ("\tMint: \t" +ˢ show mint) ∷ ("\tRefunds: \t" +ˢ show (inject (depositRefunds pparams (from st) body))) ∷ ("\tWithdrawals: \t" +ˢ show (inject (getCoin txwdrls))) ∷ ("\tTotal: \t" +ˢ show (consumed pparams (from st) body)) ∷ "Produced:" ∷ - ("\tOutputs: \t" +ˢ show (balance (outs body))) ∷ + ("\tOutputs: \t" +ˢ show (L.balance (L.outs body))) ∷ ("\tDonations: \t" +ˢ show (inject txdonation)) ∷ ("\tDeposits: \t" +ˢ show (inject (newDeposits pparams (from st) body))) ∷ ("\tFees: \t" +ˢ show (inject txfee)) ∷ ("\tTotal: \t" +ˢ show (produced pparams (from st) body)) ∷ [] - + {-# COMPILE GHC utxo-debug as utxoDebug #-} diff --git a/src/ScriptVerification/HelloWorld.agda b/src/ScriptVerification/HelloWorld.agda index 3669e905e..f78807f65 100644 --- a/src/ScriptVerification/HelloWorld.agda +++ b/src/ScriptVerification/HelloWorld.agda @@ -10,7 +10,7 @@ scriptImp = record { serialise = id ; open import ScriptVerification.LedgerImplementation String String scriptImp open import ScriptVerification.Lib String String scriptImp -open import Ledger.Conway.Conformance.ScriptValidation SVTransactionStructure SVAbstractFunctions +open import Ledger.ScriptValidation SVTransactionStructure SVAbstractFunctions open import Data.Empty open import Ledger.Conway.Conformance.Utxo SVTransactionStructure SVAbstractFunctions open import Ledger.Transaction @@ -127,7 +127,7 @@ evalFailScript = evalScripts failTx failState opaque unfolding collectPhaseTwoScriptInputs unfolding setToList - unfolding outs + unfolding L.outs _ : notEmpty succeedState ≡ ⊤ _ = refl diff --git a/src/ScriptVerification/Lib.agda b/src/ScriptVerification/Lib.agda index a81467104..f64f015b3 100644 --- a/src/ScriptVerification/Lib.agda +++ b/src/ScriptVerification/Lib.agda @@ -6,7 +6,7 @@ module ScriptVerification.Lib (A D : Type) where open import ScriptVerification.LedgerImplementation A D scriptImp -open import Ledger.Conway.Conformance.ScriptValidation SVTransactionStructure SVAbstractFunctions +open import Ledger.ScriptValidation SVTransactionStructure SVAbstractFunctions open import Data.Empty open import Ledger.Conway.Conformance.Utxo SVTransactionStructure SVAbstractFunctions open import Ledger.Transaction diff --git a/src/ScriptVerification/SucceedIfNumber.agda b/src/ScriptVerification/SucceedIfNumber.agda index 2d1d821d9..cc25d6c98 100644 --- a/src/ScriptVerification/SucceedIfNumber.agda +++ b/src/ScriptVerification/SucceedIfNumber.agda @@ -10,7 +10,7 @@ scriptImp = record { serialise = id ; open import ScriptVerification.LedgerImplementation ℕ ℕ scriptImp open import ScriptVerification.Lib ℕ ℕ scriptImp -open import Ledger.Conway.Conformance.ScriptValidation SVTransactionStructure SVAbstractFunctions +open import Ledger.ScriptValidation SVTransactionStructure SVAbstractFunctions open import Data.Empty open import Ledger.Conway.Conformance.Utxo SVTransactionStructure SVAbstractFunctions open import Ledger.Transaction @@ -148,7 +148,7 @@ exampleDatum' = getDatum failTx initStateRedeemer (Spend (6 , 6)) opaque unfolding collectPhaseTwoScriptInputs unfolding setToList - unfolding outs + unfolding L.outs gotScript : lookupScriptHash 777 succeedTx initStateDatum ≡ just (inj₂ succeedIf1Datum) gotScript = refl