Prove that EPOCH not depends on expired dreps (#941)

Author: carlostome

flake.lock

@@ -0,0 +1,48 @@
+{-# OPTIONS --safe --no-import-sorts #-}
+open import Axiom.Set using (Theory)
+
+module abstract-set-theory.Axiom.Set.Properties {ℓ} (th : Theory {ℓ}) where
+
+open import abstract-set-theory.Prelude hiding (isEquivalence; trans; map; map₂)
+open Theory th
+
+open Equivalence
+
+private variable
+  A B C : Type ℓ
+  X Y Z : Set A
+
+module _ {P Q : A → Type} {sp-P : specProperty P} {sp-Q : specProperty Q} where
+
+  open import Relation.Unary using (_⇒_; Universal)
+
+  filter-⇒ : (P⇒Q : Universal (P ⇒ Q)) → filter sp-P (filter sp-Q X) ≡ᵉ filter sp-P X
+  filter-⇒ P⇒Q = filter-⇒-⊆ , filter-⇒-⊇
+    where
+      filter-⇒-⊆ : filter sp-P (filter sp-Q X) ⊆ filter sp-P X
+      filter-⇒-⊆ p with from ∈-filter p
+      ... | (q , p) with from ∈-filter p
+      ... | (_ , p) = to ∈-filter (q , p)
+
+      filter-⇒-⊇ : filter sp-P X ⊆ filter sp-P (filter sp-Q X)
+      filter-⇒-⊇ p with from ∈-filter p
+      ... | (q , p) = to ∈-filter (q , (to ∈-filter (P⇒Q _ q , p)))
+
+module _ {P : A → Type} {sp-P : specProperty P} {Q : B → Type} {sp-Q : specProperty Q} where
+
+  open import Relation.Unary using (_⇒_; Universal)
+
+  filter-map : ∀ {f : A → B} (Qf⇒P : Universal ((Q ∘ f) ⇒ P))
+             → filter sp-Q (map f X) ≡ᵉ filter sp-Q (map f (filter sp-P X))
+  filter-map {f = f} Qf⇒P = filter-map-⊆ , filter-map-⊇
+    where
+      filter-map-⊆ : filter sp-Q (map f X) ⊆ filter sp-Q (map f (filter sp-P X))
+      filter-map-⊆ p with from ∈-filter p
+      ... | Qa , p with from ∈-map p
+      ... | (a , refl , p) = to ∈-filter (Qa , (to ∈-map (_ , (refl , (to ∈-filter (Qf⇒P a Qa , p))))))
+
+      filter-map-⊇ : filter sp-Q (map f (filter sp-P X)) ⊆ filter sp-Q (map f X)
+      filter-map-⊇ p with from ∈-filter p
+      ... | Qfa , p with from ∈-map p
+      ... | (a , refl , p) with from ∈-filter p
+      ... | (Pa , p) = to ∈-filter (Qfa , (to ∈-map (a , (refl , p))))

src-lib-exts/abstract-set-theory/Axiom/Set/Properties.agda

@@ -19,6 +19,21 @@ open EnactState
 
 open Computational ⦃...⦄
 
+module _ {Γ : EnactEnv} {eSt : EnactState} {ga : GovAction} where
+
+  -- TODO: Make this follow from computationalness or viceversa
+  ENACT-deterministic : ∀ {eSt' eSt''}
+                      → Γ ⊢ eSt ⇀⦇ ga ,ENACT⦈ eSt'
+                      → Γ ⊢ eSt ⇀⦇ ga ,ENACT⦈ eSt''
+                      → eSt' ≡ eSt''
+  ENACT-deterministic Enact-NoConf Enact-NoConf = refl
+  ENACT-deterministic (Enact-UpdComm _) (Enact-UpdComm _) = refl
+  ENACT-deterministic Enact-NewConst Enact-NewConst = refl
+  ENACT-deterministic Enact-HF Enact-HF = refl
+  ENACT-deterministic Enact-PParams Enact-PParams = refl
+  ENACT-deterministic (Enact-Wdrl _) (Enact-Wdrl _) = refl
+  ENACT-deterministic Enact-Info Enact-Info = refl
+
 instance
   Computational-ENACT : Computational _⊢_⇀⦇_,ENACT⦈_ String
   Computational-ENACT .computeProof Γᵉ s =

src/Ledger/Conway/Specification/Enact/Properties/Computational.lagda.md

@@ -713,34 +713,35 @@ module Post-POOLREAPUpdate (es : EnactState)
 ```agda
   open LState
   open Governance-Update govUpd
-  opaque
 ```
 -->
 ```agda
+  opaque
     govActionReturns : RwdAddr ⇀ Coin
     govActionReturns =
       aggregate₊ (mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ)
 
     payout : RwdAddr ⇀ Coin
     payout = govActionReturns ∪⁺ WithdrawalsOf es
 
+  opaque
     refunds : Credential ⇀ Coin
     refunds = pullbackMap payout toRwdAddr (dom (RewardsOf dState'))
 
-    dState'' : DState
-    dState'' = ⟦ VoteDelegsOf dState' , StakeDelegsOf dState' , RewardsOf dState' ∪⁺ refunds ⟧
+  dState'' : DState
+  dState'' = ⟦ VoteDelegsOf dState' , StakeDelegsOf dState' , RewardsOf dState' ∪⁺ refunds ⟧
 
-    unclaimed : Coin
-    unclaimed = getCoin payout - getCoin refunds
+  unclaimed : Coin
+  unclaimed = getCoin payout - getCoin refunds
 
-    totWithdrawals : Coin
-    totWithdrawals = ∑[ x ← WithdrawalsOf es ] x
+  totWithdrawals : Coin
+  totWithdrawals = ∑[ x ← WithdrawalsOf es ] x
 
-    acnt'' : Acnt
-    acnt'' = ⟦ TreasuryOf acnt' ∸ totWithdrawals + DonationsOf ls + unclaimed , ReservesOf acnt' ⟧
+  acnt'' : Acnt
+  acnt'' = ⟦ TreasuryOf acnt' ∸ totWithdrawals + DonationsOf ls + unclaimed , ReservesOf acnt' ⟧
 
-    updates : Post-POOLREAP-Update
-    updates = Post-POOLREAPUpdate dState'' acnt''
+  updates : Post-POOLREAP-Update
+  updates = Post-POOLREAPUpdate dState'' acnt''
 ```
 
 ### Transition Rule

src/Ledger/Conway/Specification/Epoch.lagda.md

@@ -10,6 +10,7 @@ module Ledger.Conway.Specification.Epoch.Properties where
 
 open import Ledger.Conway.Specification.Epoch.Properties.Computational
 open import Ledger.Conway.Specification.Epoch.Properties.ConstRwds
+open import Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps
 open import Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch
 open import Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps
 ```