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
IntersectMBO · Nov 21, 2024 · 363b1f6 · 363b1f6
1 parent bccb83b
commit 363b1f6
Show file tree

Hide file tree

Showing 21 changed files with 69 additions and 878 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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