Change rewardAccount to RewardAddress for stake pools

Author: carlostome

src/Ledger/Dijkstra/Specification/Certs.lagda.md

@@ -142,7 +142,7 @@ record GovCertEnv : Type where
 
 <!--
 ```agda
-open StakePoolParams using (vrf; cost)
+open StakePoolParams
 
 IsConwayCert? : IsConwayCert ⁇¹
 IsConwayCert? {x} .dec with x
@@ -422,6 +422,7 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type wh
   POOL-reg :
     ∙ ¬ (IsPoolRegistered pools kh)
     ∙ ¬ (poolParams .vrf ∈ mapˢ vrf (range pools ∪ range fPools))
+    ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
     ∙ pp .minPoolCost ≤ poolParams .cost
     ────────────────────────────────
     ⟦ e , pp ⟧ ⊢ ⟦ pools
@@ -438,6 +439,7 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type wh
   POOL-rereg :
     ∙ IsPoolRegistered pools kh
     ∙ ¬ (poolParams .vrf ∈ mapˢ vrf (range (pools ∣ ❴ kh ❵ ᶜ) ∪ range (fPools ∣ ❴ kh ❵ ᶜ)))
+    ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
     ∙ pp .minPoolCost ≤ poolParams .cost
     ────────────────────────────────
     ⟦ e , pp ⟧ ⊢ ⟦ pools

src/Ledger/Dijkstra/Specification/Certs/Properties/Computational.lagda.md

@@ -62,11 +62,13 @@ instance
     with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿
   Computational-POOL .computeProof Γ stᵖ (regpool c poolParams) | yes p
     with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ ∣ ❴ c ❵ ᶜ) ∪ range (FuturePoolsOf stᵖ ∣ ❴ c ❵ ᶜ)))
+         ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
          ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿
   ... | yes q = success (-, POOL-rereg (p , q))
   ... | no ¬q = failure (genErrors ¬q)
   Computational-POOL .computeProof Γ stᵖ (regpool c poolParams) | no ¬p
     with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ) ∪ range (FuturePoolsOf stᵖ)))
+         ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
          ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿
   ... | yes q = success (-, (POOL-reg (¬p , q)))
   ... | no ¬q = failure (genErrors ¬q)
@@ -82,6 +84,7 @@ instance
   ... | yes r = ⊥-elim (p r)
   ... | no ¬r
     with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ) ∪ range (FuturePoolsOf stᵖ)))
+         ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
          ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿
   ... | yes _ = refl
   ... | no ¬s = ⊥-elim (¬s q)
@@ -90,6 +93,7 @@ instance
   ... | no ¬r = ⊥-elim (¬r p)
   ... | yes r
     with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ ∣ ❴ c ❵ ᶜ) ∪ range (FuturePoolsOf stᵖ ∣ ❴ c ❵ ᶜ)))
+         ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
          ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿
   ... | yes _ = refl
   ... | no ¬s = ⊥-elim (¬s q)

src/Ledger/Dijkstra/Specification/PoolReap.lagda.md

@@ -61,7 +61,7 @@ data _⊢_⇀⦇_,POOLREAP⦈_ : ⊤ → PoolReapState → Epoch → PoolReapSta
         retired = retiring ⁻¹ e
 
         rewardAccounts : KeyHash ⇀ Credential
-        rewardAccounts = mapValues rewardAccount (pools ∣ retired)
+        rewardAccounts = mapValues (CredentialOf ∘ rewardAccount) (pools ∣ retired)
 
         rewardAccounts' : Credential ⇀ Coin
         rewardAccounts' = aggregateBy (rewardAccounts ˢ) depositsᵖ

src/Ledger/Dijkstra/Specification/Ratify.lagda.md

@@ -255,7 +255,7 @@ module AcceptedBySPO (delegatees : VoteDelegs)
   defaultVote : KeyHash → Vote
   defaultVote kh = case lookupᵐ? pools kh of λ where
     nothing   → Vote.no
-    (just  p) → case lookupᵐ? delegatees (StakePoolParams.rewardAccount p) , gaType action of
+    (just  p) → case lookupᵐ? delegatees (CredentialOf (StakePoolParams.rewardAccount p)) , gaType action of
       λ where
       ( _                        , TriggerHardFork  )  → Vote.no
       ( just vDelegNoConfidence  , NoConfidence     )  → Vote.yes

src/Ledger/Dijkstra/Specification/Rewards.lagda.md

@@ -133,7 +133,7 @@ rewardOnePool pp rewardPot n N poolParams stakeDistr σ σa tot = memberRewards
                             (stakeDistr ∣ owners ᶜ)
 
   ownersRewards : Stake
-  ownersRewards =  ❴ poolParams .StakePoolParams.rewardAccount
+  ownersRewards =  ❴ CredentialOf (poolParams .StakePoolParams.rewardAccount)
                    , stakeMap[ rewardOwners ] ownerStake σ ❵ᵐ
 
 poolStake  : KeyHash → StakeDelegs → Stake → Stake