[Dijkstra] Change SNAP invocation in EPOCH to after ledger state update (#1313)

- Inline `StakeDistrs` record into RatifyEnv
- Fix computational instance
- Add prose explaining this change

Author: carlostome

build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs

@@ -40,7 +40,7 @@ import MAlonzo.Code.Ledger.Dijkstra.Foreign.Ledger            as X
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.NewEpoch          as X
   (NewEpochState(..), newEpochStep)
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Ratify            as X
-  (StakeDistrs(..), RatifyEnv(..), RatifyState(..), ratifyStep)
+  (RatifyEnv(..), RatifyState(..), ratifyStep)
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Rewards           as X
   (RewardUpdate(..), Snapshot(..), Snapshots(..))
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Utxo              as X

src/Ledger/Dijkstra/Foreign/Ratify.agda

@@ -23,10 +23,6 @@ open import Ledger.Dijkstra.Specification.Ratify.Properties.Computational it
 open Computational
 
 instance
-  HsTy-StakeDistrs = autoHsType StakeDistrs ⊣ withConstructor "MkStakeDistrs"
-                                              • fieldPrefix "sd"
-  Conv-StakeDistrs = autoConvert StakeDistrs
-
   HsTy-RatifyEnv = autoHsType RatifyEnv ⊣ withConstructor "MkRatifyEnv"
                                           • fieldPrefix "re"
   Conv-RatifyEnv = autoConvert RatifyEnv

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

@@ -398,10 +398,9 @@ applyRUpd rewardUpdate ⟦ ⟦ treasury , reserves ⟧ᵃ
 ## Stake Distributions {#sec:stake-distributions}
 
 This section defines the functions
-`calculatePoolDelegatedStake`{.AgdaFunction},
-`calculateVDelegDelegatedStake`{.AgdaFunction}, and
-`mkStakeDistrs`{.AgdaFunction}, which calculates stake distributions
-for voting purposes.
+`calculatePoolDelegatedStake`{.AgdaFunction} and
+`calculateVDelegDelegatedStake`{.AgdaFunction}, which calculate stake
+distributions for voting purposes.
 
 <!--
 ```agda
@@ -525,20 +524,6 @@ the deposits made to governance actions.
     count deposits on governance actions towards the stake of
     `SPOs`{.AgdaInductiveConstructor} as well.
 
-```agda
-mkStakeDistrs
-  : Snapshot
-  → Epoch
-  → UTxOState
-  → GovState
-  → GState
-  → DState
-  → StakeDistrs
-mkStakeDistrs ss currentEpoch utxoSt govSt gState dState =
-  ⟦ calculateVDelegDelegatedStake currentEpoch utxoSt govSt gState dState
-  , calculatePoolDelegatedStakeForVoting ss govSt ⟧
-```
-
 <!--
 ```agda
 private variable
@@ -730,7 +715,7 @@ module Post-POOLREAPUpdate (es : EnactState)
 
 This section defines the `EPOCH`{.AgdaDatatype} transition rule.
 
-In Conway, the `EPOCH`{.AgdaDatatype} rule invokes `RATIFIES`{.AgdaDatatype},
+In Dijkstra the `EPOCH`{.AgdaDatatype} rule invokes `RATIFIES`{.AgdaDatatype},
 and carries out the following tasks:
 
 +  payout all the enacted treasury withdrawals;
@@ -743,10 +728,16 @@ and carries out the following tasks:
 +  remove all hot keys from the constitutional committee delegation map
    that do not belong to currently elected members;
 
-+  Apply the resulting enact state from the previous epoch boundary
-   `fut`{.AgdaBound} and store the resulting enact state
++  apply the resulting enact state from the previous epoch boundary
+   `fut`{.AgdaBound} and store the new enact state
    `fut’`{.AgdaBound}.
 
+Unlike Conway, where the mark snapshot is taken before updating the
+ledger state, in Dijkstra the `EPOCH`{.AgdaDatatype} rule invokes the
+`SNAP`{.AgdaDatatype} rule _after_ updating the ledger state. This
+change affects the stake distribution used for leader election and
+distributing rewards, and for voting on governance actions.
+
 ```agda
 data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Type where
 ```
@@ -767,19 +758,25 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
       govSt' : GovState
       govSt' = Governance-Update.govSt' govUpd
 
-      stakeDistrs : StakeDistrs
-      stakeDistrs = mkStakeDistrs (Snapshots.mark ss') e utxoSt'
-                                  govSt' (GStateOf ls) (DStateOf ls)
+      ls' : LedgerState
+      ls' = ⟦ utxoSt' , govSt' , ⟦ dState'' , pState'' , gState' ⟧ᶜˢ ⟧
 
       Γ : RatifyEnv
-      Γ = ⟦ stakeDistrs , e , DRepsOf ls , CCHotKeysOf ls , TreasuryOf acnt'' , PoolsOf ls , VoteDelegsOf ls ⟧
+      Γ = ⟦ calculateVDelegDelegatedStake e utxoSt' govSt' gState' dState''
+          , calculatePoolDelegatedStakeForVoting (Snapshots.mark ss') govSt'
+          , e
+          , DRepsOf ls'
+          , CCHotKeysOf ls'
+          , TreasuryOf acnt''
+          , PoolsOf ls'
+          , VoteDelegsOf ls' ⟧
 
     in
-        ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
       ∙ _  ⊢ ⟦ acnt , DStateOf ls , pState' ⟧ ⇀⦇ e ,POOLREAP⦈ ⟦ acnt' , dState' , pState'' ⟧
+      ∙ ls' ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
       ∙ Γ  ⊢ ⟦ es' , ∅ , false ⟧ ⇀⦇ govSt' ,RATIFIES⦈ fut'
       ──────────────────────────────────────────────
-      _ ⊢ ⟦ acnt , ss , ls , es₀ , fut ⟧ ⇀⦇ e ,EPOCH⦈ ⟦ acnt'' , ss' , ⟦ utxoSt' , govSt' , ⟦ dState'' , pState'' , gState' ⟧ᶜˢ ⟧ , es' , fut' ⟧
+      _ ⊢ ⟦ acnt , ss , ls , es₀ , fut ⟧ ⇀⦇ e ,EPOCH⦈ ⟦ acnt'' , ss' , ls' , es' , fut' ⟧
 ```
 
 ## The <span class="AgdaDatatype">NEWEPOCH</span> Transition System {#sec:the-newepoch-transition-system}

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

@@ -36,8 +36,8 @@ module _ {eps : EpochState} {e : Epoch} where
   EPOCH-total : ∃[ eps' ] _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
   EPOCH-total =
     -, EPOCH
-         ( SNAP-total      .proj₂
-         , POOLREAP-total  .proj₂
+         ( POOLREAP-total  .proj₂
+         , SNAP-total      .proj₂
          , RATIFIES-total' .proj₂)
 
   EPOCH-deterministic : ∀ eps' eps''
@@ -50,15 +50,15 @@ module _ {eps : EpochState} {e : Epoch} where
       (EPOCH
         {dState' = dState'₁}
         {acnt' = acnt'₁}
-        {ss' = ss'₁}
         {pState'' = pState'₁}
+        {ss' = ss'₁}
         (p₁ , p₂ , p₃)
       )
       (EPOCH
         {dState' = dState'₂}
         {acnt' = acnt'₂}
-        {ss' = ss'₂}
         {pState'' = pState'₂}
+        {ss' = ss'₂}
         (p₁' , p₂' , p₃')
       ) = eps'≡eps''
        where
@@ -73,9 +73,6 @@ module _ {eps : EpochState} {e : Epoch} where
 
          govSt' = Governance-Update.govSt' govUpd
 
-         ss'₁≡ss'₂ : ss'₁ ≡ ss'₂
-         ss'₁≡ss'₂ = SNAP-deterministic p₁ p₁'
-
          module pPRUpd =  Pre-POOLREAP-Update (Pre-POOLREAPUpdate.updates ls es govUpd)
 
          pPRUpd₁ = Post-POOLREAPUpdate.updates es ls dState'₁ acnt'₁ govUpd
@@ -86,17 +83,37 @@ module _ {eps : EpochState} {e : Epoch} where
 
          prs'≡prs'' : ⟦ acnt'₁ , dState'₁ , pState'₁ ⟧ᵖ ≡
                       ⟦ acnt'₂ , dState'₂ , pState'₂ ⟧ᵖ
-         prs'≡prs'' = POOLREAP-deterministic-≡ refl refl p₂ p₂'
+         prs'≡prs'' = POOLREAP-deterministic-≡ refl refl p₁ p₁'
 
          pPRUpd₁≡pPRUpd₂ : pPRUpd₁ ≡ pPRUpd₂
          pPRUpd₁≡pPRUpd₂ rewrite (cong PoolReapState.dState prs'≡prs'') | (cong PoolReapState.acnt prs'≡prs'') = refl
 
-         stakeDistrs₁≡stakeDistrs₂ : mkStakeDistrs (Snapshots.mark ss'₁) e pPRUpd.utxoSt' govSt' (GStateOf ls) (DStateOf ls)
-                                     ≡ mkStakeDistrs (Snapshots.mark ss'₂) e pPRUpd.utxoSt' govSt' (GStateOf ls) (DStateOf ls)
-         stakeDistrs₁≡stakeDistrs₂ = cong (λ ss' → mkStakeDistrs (Snapshots.mark ss') e pPRUpd.utxoSt' govSt' (GStateOf ls) (DStateOf ls)) ss'₁≡ss'₂
+         ls'₁ = ⟦ pPRUpd.utxoSt' , govSt' , ⟦ pPRUpd₁.dState'' , pState'₁ , pPRUpd.gState' ⟧ᶜˢ ⟧
+         ls'₂ = ⟦ pPRUpd.utxoSt' , govSt' , ⟦ pPRUpd₂.dState'' , pState'₂ , pPRUpd.gState' ⟧ᶜˢ ⟧
 
-         Γ≡Γ' = cong₂ (λ sd acnt → ⟦ sd , e , DRepsOf ls , CCHotKeysOf ls , TreasuryOf acnt , PoolsOf ls , VoteDelegsOf ls ⟧)
-                      stakeDistrs₁≡stakeDistrs₂ (cong Post-POOLREAP-Update.acnt'' pPRUpd₁≡pPRUpd₂)
+         ls'₁≡ls'₂ : ls'₁ ≡ ls'₂
+         ls'₁≡ls'₂ = cong₂ (λ ds ps → ⟦ pPRUpd.utxoSt' , govSt' , ⟦ ds , ps , pPRUpd.gState' ⟧ᶜˢ ⟧)
+                       (cong Post-POOLREAP-Update.dState'' pPRUpd₁≡pPRUpd₂)
+                       (cong PoolReapState.pState prs'≡prs'')
+
+         ss'₁≡ss'₂ : ss'₁ ≡ ss'₂
+         ss'₁≡ss'₂ = SNAP-deterministic-≡ ls'₁≡ls'₂ p₂ p₂'
+
+         mkΓ : Snapshots → Post-POOLREAP-Update → LedgerState → RatifyEnv
+         mkΓ ss'' pPR ls'' =
+           ⟦ calculateVDelegDelegatedStake e pPRUpd.utxoSt' govSt' pPRUpd.gState' (Post-POOLREAP-Update.dState'' pPR)
+           , calculatePoolDelegatedStakeForVoting (Snapshots.mark ss'') govSt'
+           , e
+           , DRepsOf ls''
+           , CCHotKeysOf ls''
+           , TreasuryOf (Post-POOLREAP-Update.acnt'' pPR)
+           , PoolsOf ls''
+           , VoteDelegsOf ls'' ⟧
+
+         Γ≡Γ' : mkΓ ss'₁ pPRUpd₁ ls'₁ ≡ mkΓ ss'₂ pPRUpd₂ ls'₂
+         Γ≡Γ' = trans (cong (λ x → mkΓ x pPRUpd₁ ls'₁) ss'₁≡ss'₂)
+                (trans (cong (λ x → mkΓ ss'₂ x ls'₁) pPRUpd₁≡pPRUpd₂)
+                       (cong (mkΓ ss'₂ pPRUpd₂) ls'₁≡ls'₂))
 
          fut'≡fut'' : RatifyStateOf eps' ≡ RatifyStateOf eps''
          fut'≡fut'' = RATIFIES-deterministic-≡ Γ≡Γ' refl refl p₃ p₃'

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

@@ -90,20 +90,16 @@ threshold pp ccThreshold ga =
 canVote : PParams → GovAction → GovRole → Type
 canVote pp a r = Is-just (threshold pp nothing a r)
 
-record StakeDistrs : Type where
-  field
-    stakeDistrVDeleg  : VDeleg  ⇀ Coin
-    stakeDistrPools   : KeyHash ⇀ Coin
-
 record RatifyEnv : Type where
   field
-    stakeDistrs   : StakeDistrs
-    currentEpoch  : Epoch
-    dreps         : Credential ⇀ Epoch
-    ccHotKeys     : Credential ⇀ Maybe Credential
-    treasury      : Treasury
-    pools         : KeyHash ⇀ StakePoolParams
-    delegatees    : VoteDelegs
+    stakeDistrVDeleg : VDeleg  ⇀ Coin
+    stakeDistrPools  : KeyHash ⇀ Coin
+    currentEpoch     : Epoch
+    dreps            : Credential ⇀ Epoch
+    ccHotKeys        : Credential ⇀ Maybe Credential
+    treasury         : Treasury
+    pools            : KeyHash ⇀ StakePoolParams
+    delegatees       : VoteDelegs
 
 record RatifyState : Type where
   field
@@ -128,9 +124,8 @@ instance
   HasTreasury-RatifyEnv : HasTreasury RatifyEnv
   HasTreasury-RatifyEnv .TreasuryOf = RatifyEnv.treasury
 
-  unquoteDecl HasCast-StakeDistrs HasCast-RatifyEnv HasCast-RatifyState = derive-HasCast
-    (   (quote StakeDistrs , HasCast-StakeDistrs)
-    ∷   (quote RatifyEnv , HasCast-RatifyEnv)
+  unquoteDecl HasCast-RatifyEnv HasCast-RatifyState = derive-HasCast
+    ( (quote RatifyEnv , HasCast-RatifyEnv)
     ∷ [ (quote RatifyState , HasCast-RatifyState) ])
 ```
 -->
@@ -201,8 +196,7 @@ module AcceptedByDRep (Γ : RatifyEnv)
                       where
 
   open EnactState eSt using (cc)
-  open RatifyEnv Γ using (currentEpoch; stakeDistrs)
-  open StakeDistrs stakeDistrs
+  open RatifyEnv Γ using (currentEpoch; stakeDistrVDeleg)
   open GovActionState gaSt
   open GovVotes votes using (gvDRep)
 
@@ -277,7 +271,7 @@ module AcceptedBySPO (delegatees : VoteDelegs)
 
 acceptedBySPO : RatifyEnv → EnactState → GovActionState → Type
 acceptedBySPO Γ = AcceptedBySPO.accepted delegatees pools stakeDistrPools
-  where open RatifyEnv Γ; open StakeDistrs stakeDistrs
+  where open RatifyEnv Γ
 
 
 -- Ratification Functions --

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

@@ -24,22 +24,25 @@ open import Ledger.Dijkstra.Specification.Ledger txs abs
 open import Ledger.Dijkstra.Specification.Rewards txs abs
 
 open Computational ⦃...⦄
-
-module _ {lstate : LedgerState} {ss : Snapshots} where
 ```
 -->
 
 ```agda
-  SNAP-total : ∃[ ss' ] lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
-  SNAP-total = -, SNAP
+module _ {ss : Snapshots} where
+
+  module _ {lstate : LedgerState} where
+
+    SNAP-total : ∃[ ss' ] lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
+    SNAP-total = -, SNAP
 
-  SNAP-complete : ∀ ss' → lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss' → proj₁ SNAP-total ≡ ss'
-  SNAP-complete ss' SNAP = refl
+    SNAP-complete : ∀ ss' → lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss' → proj₁ SNAP-total ≡ ss'
+    SNAP-complete ss' SNAP = refl
 
-  SNAP-deterministic : ∀ {ss' ss''}
-                     → lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
-                     → lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'' → ss' ≡ ss''
-  SNAP-deterministic SNAP SNAP = refl
+  SNAP-deterministic-≡ : ∀ {ls ls' ss' ss''}
+                     → ls ≡ ls'
+                     → ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
+                     → ls' ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'' → ss' ≡ ss''
+  SNAP-deterministic-≡ refl SNAP SNAP = refl
 
 instance
   Computational-SNAP : Computational _⊢_⇀⦇_,SNAP⦈_ ⊥