Define a step function to run the EPOCH rule from the specification

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

@@ -23,7 +23,7 @@ import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Certs             as X
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Enact             as X
   (EnactState(..), EnactEnv(..), enactStep)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Epoch             as X
-  (EpochState(..), epochStep)
+  (EpochState(..), epochStep, specEpochStep)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Gov.Core          as X
   (GovRole(..), Anchor(..), VDeleg(..), Vote(..), GovVote(..), GovVoter, GovVotes(..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Gov               as X
@@ -33,7 +33,7 @@ import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Gov.Actions       as X
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Ledger            as X
   (LEnv(..), LState(..), ledgerStep, ledgersStep)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.NewEpoch          as X
-  (NewEpochState(..), newEpochStep)
+  (NewEpochState(..), newEpochStep, specNewEpochStep)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Ratify            as X
   (StakeDistrs(..), RatifyEnv(..), RatifyState(..), ratifyStep)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Rewards           as X

src/Ledger/Conway/Conformance/Epoch.agda

@@ -18,13 +18,17 @@ open import Data.List using (filter)
 open import Agda.Builtin.FromNat
 
 open import Ledger.Conway.Specification.Enact govStructure
+open import Ledger.Conway.Conformance.Equivalence txs abs
+open import Ledger.Conway.Conformance.Equivalence.Convert
+open import Ledger.Conway.Conformance.Equivalence.Deposits txs abs
 open import Ledger.Conway.Conformance.Ledger txs abs
 open import Ledger.Conway.Specification.Ratify txs
 open import Ledger.Conway.Conformance.Utxo txs abs
 open import Ledger.Conway.Conformance.Certs govStructure
 open import Ledger.Conway.Conformance.Rewards txs abs
 open import Ledger.Conway.Specification.Epoch txs abs
   using (getStakeCred; getOrphans; mkStakeDistrs; toRwdAddr) public
+import Ledger.Conway.Specification.Epoch txs abs as EpochSpec
 
 record EpochState : Type where
   constructor ⟦_,_,_,_,_⟧ᵉ'
@@ -35,17 +39,44 @@ record EpochState : Type where
     es         : EnactState
     fut        : RatifyState
 
+PoolDelegatedStake : Type
+PoolDelegatedStake = KeyHash ⇀ Coin
+
 record NewEpochState : Type where
   field
     lastEpoch   : Epoch
+    bprev       : BlocksMade
+    bcur        : BlocksMade
     epochState  : EpochState
     ru          : Maybe RewardUpdate
+    pd          : PoolDelegatedStake
 
 instance
   unquoteDecl HasCast-EpochState HasCast-NewEpochState = derive-HasCast
     ( (quote EpochState     , HasCast-EpochState)
     ∷ [ (quote NewEpochState  , HasCast-NewEpochState)])
 
+  EpochStateFromConf : EpochState ⭆ EpochSpec.EpochState
+  EpochStateFromConf .convⁱ _ epochState =
+    let open EpochState epochState in
+    ⟦ acnt , ss , conv ls , es , fut ⟧
+
+  EpochStateToConf : EpochSpec.EpochState ⭆ EpochState
+  EpochStateToConf .convⁱ deposits epochSt =
+    let open EpochSpec.EpochState epochSt in
+    ⟦ acnt , ss , certDeposits ls ⊢conv ls , es , fut ⟧ᵉ'
+
+  NewEpochStateFromConf : NewEpochState ⭆ EpochSpec.NewEpochState
+  NewEpochStateFromConf .convⁱ _ newEpochState =
+    let open NewEpochState newEpochState in
+    ⟦ lastEpoch , bprev , bcur , conv epochState , ru , pd ⟧
+
+  NewEpochStateToConf : EpochSpec.NewEpochState ⭆ NewEpochState
+  NewEpochStateToConf .convⁱ deposits newEpochSt =
+    let open EpochSpec.NewEpochState newEpochSt in
+    ⟦ lastEpoch , bcur , bprev , conv epochState , ru , pd ⟧
+
+
 applyRUpd : RewardUpdate → EpochState → EpochState
 applyRUpd rewardUpdate
   ⟦ ⟦ treasury , reserves ⟧ᵃ
@@ -70,6 +101,24 @@ applyRUpd rewardUpdate
     unregRU   = rs ∣ dom rewards ᶜ
     unregRU'  = ∑[ x ← unregRU ] x
 
+opaque
+  calculatePoolDelegatedStake : Snapshot → PoolDelegatedStake
+  calculatePoolDelegatedStake ss =
+      -- Shelley spec: the output map must contain keys appearing in both
+      -- sd and the pool parameters.
+      sd ∣ dom (ss .pools)
+    where
+      open Snapshot
+
+      -- stake credentials delegating to each pool
+      stakeCredentialsPerPool : Rel KeyHash Credential
+      stakeCredentialsPerPool = (StakeDelegsOf ss ˢ) ⁻¹ʳ
+
+      -- delegated stake per pool
+      sd : KeyHash ⇀ Coin
+      sd = aggregate₊ ((stakeCredentialsPerPool ∘ʳ (StakeOf ss ˢ)) ᶠˢ)
+
+
 private variable
   nes nes' : NewEpochState
   e lastEpoch : Epoch
@@ -166,21 +215,30 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
 
 data _⊢_⇀⦇_,NEWEPOCH⦈_ : ⊤ → NewEpochState → Epoch → NewEpochState → Type where
 
-  NEWEPOCH-New : let
-      eps' = applyRUpd ru eps
-    in
-    ∙ e ≡ lastEpoch + 1
-    ∙ _ ⊢ eps' ⇀⦇ e ,EPOCH⦈ eps''
-      ────────────────────────────────
-      _ ⊢ ⟦ lastEpoch , eps , just ru ⟧ ⇀⦇ e ,NEWEPOCH⦈ ⟦ e , eps'' , nothing ⟧
-
-  NEWEPOCH-Not-New :
+  NEWEPOCH-New :
+    ∀ {bprev bcur : BlocksMade} {pd : PoolDelegatedStake} →
+    let
+       eps' = applyRUpd ru eps
+       ss   = EpochState.ss eps''
+       pd'  = calculatePoolDelegatedStake (Snapshots.set ss)
+     in
+       ∙ e ≡ lastEpoch + 1
+       ∙ _ ⊢ eps' ⇀⦇ e ,EPOCH⦈ eps''
+       ────────────────────────────────
+       _ ⊢ ⟦ lastEpoch , bprev , bcur , eps , just ru , pd ⟧ ⇀⦇ e ,NEWEPOCH⦈ ⟦ e , bcur , ∅ᵐ  , eps'' , nothing , pd' ⟧
+
+  NEWEPOCH-Not-New : ∀ {bprev bcur : BlocksMade} {pd : PoolDelegatedStake} →
     ∙ e ≢ lastEpoch + 1
       ────────────────────────────────
-      _ ⊢ ⟦ lastEpoch , eps , mru ⟧ ⇀⦇ e ,NEWEPOCH⦈ ⟦ lastEpoch , eps , mru ⟧
+      _ ⊢ ⟦ lastEpoch , bprev , bcur , eps , mru , pd ⟧ ⇀⦇ e ,NEWEPOCH⦈ ⟦ lastEpoch , bprev , bcur , eps , mru , pd ⟧
 
   NEWEPOCH-No-Reward-Update :
-    ∙ e ≡ lastEpoch + 1
-    ∙ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
+    ∀ {bprev bcur : BlocksMade} {pd : PoolDelegatedStake} →
+    let
+      ss  = EpochState.ss eps'
+      pd' = calculatePoolDelegatedStake (Snapshots.set ss)
+    in
+      ∙ e ≡ lastEpoch + 1
+      ∙ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
       ────────────────────────────────
-      _ ⊢ ⟦ lastEpoch , eps , nothing ⟧ ⇀⦇ e ,NEWEPOCH⦈ ⟦ e , eps' , nothing ⟧
+      _ ⊢ ⟦ lastEpoch , bprev , bcur , eps , nothing , pd ⟧ ⇀⦇ e ,NEWEPOCH⦈ ⟦ e , bcur , ∅ᵐ , eps' , nothing , pd' ⟧

src/Ledger/Conway/Conformance/Epoch/Properties.agda

@@ -90,15 +90,15 @@ module _ {e : Epoch} where
 
   NEWEPOCH-total : ∀ nes'' → ∃[ nes' ] _ ⊢ nes'' ⇀⦇ e ,NEWEPOCH⦈ nes'
   NEWEPOCH-total nes with e ≟ NewEpochState.lastEpoch nes + 1 | NewEpochState.ru nes | inspect NewEpochState.ru nes
-  ... | yes p | just ru | PE.[ refl ] =  ⟦ e , EPOCH-total' .proj₁ , nothing ⟧
+  ... | yes p | just ru | PE.[ refl ] =  ⟦ e , _ , _ , EPOCH-total' .proj₁ , nothing , _ ⟧
                                       , NEWEPOCH-New (p , EPOCH-total' .proj₂)
-  ... | yes p | nothing | PE.[ refl ] = ⟦ e , proj₁ EPOCH-total' , nothing ⟧
+  ... | yes p | nothing | PE.[ refl ] = ⟦ e , _ , _ , proj₁ EPOCH-total' , nothing , _ ⟧
                                       , NEWEPOCH-No-Reward-Update (p , EPOCH-total' .proj₂)
   ... | no ¬p | _ | _ = -, NEWEPOCH-Not-New ¬p
 
   NEWEPOCH-complete : ∀ nes nes' → _ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes' → proj₁ (NEWEPOCH-total nes) ≡ nes'
   -- NEWEPOCH-complete nes nes' h with e ≟ NewEpochState.lastEpoch nes + 1 | NewEpochState.ru nes | h
-  NEWEPOCH-complete nes nes' h with e ≟ NewEpochState.lastEpoch nes + 1 | NewEpochState.ru nes | inspect NewEpochState.ru nes | h 
+  NEWEPOCH-complete nes nes' h with e ≟ NewEpochState.lastEpoch nes + 1 | NewEpochState.ru nes | inspect NewEpochState.ru nes | h
   ... | yes p | just ru | PE.[ refl ] | NEWEPOCH-New (x , x₁) rewrite EPOCH-complete' _ x₁ = refl
   ... | yes p | ru | PE.[ refl ] | NEWEPOCH-Not-New x = ⊥-elim $ x p
   ... | yes p | nothing | PE.[ refl ] | NEWEPOCH-No-Reward-Update (x , x₁) rewrite EPOCH-complete' _ x₁ = refl

src/Ledger/Conway/Foreign/HSLedger/Epoch.agda

@@ -7,14 +7,23 @@ open import Ledger.Conway.Foreign.HSLedger.PParams
 open import Ledger.Conway.Foreign.HSLedger.Ratify
 open import Ledger.Conway.Foreign.HSLedger.Rewards
 
+open import Ledger.Conway.Conformance.Equivalence.Convert
 open import Ledger.Conway.Conformance.Epoch it it
 open import Ledger.Conway.Conformance.Epoch.Properties it it
 
+module EpochSpec where
+  open import Ledger.Conway.Specification.Epoch it it public
+  open import Ledger.Conway.Specification.Epoch.Properties it it public
+
 import Data.String as S
 
 instance
   Show-EPOCH : ∀ {eps e eps'} → Show (_ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps')
-  Show-EPOCH .show (EPOCH e s) = "EPOCH\n" S.++ show s S.++ " " S.++ show e 
+  Show-EPOCH .show (EPOCH e s) = "EPOCH\n" S.++ show s S.++ " " S.++ show e
+
+  Show-SPEC-EPOCH : ∀ {eps e eps'} → Show (_ EpochSpec.⊢ eps ⇀⦇ e ,EPOCH⦈ eps')
+  Show-SPEC-EPOCH .show (EpochSpec.EPOCH (s , r , pr)) =
+    "SPEC-EPOCH\n" S.++ "SNAP" S.++ " " S.++ show r
 
     -- record { currentEpoch = e
     --        ; stakeDistrs = mkStakeDistrs  (Snapshots.mark ss') govSt'
@@ -31,3 +40,15 @@ epoch-step _ epochSt e =
     (success (s , p)) → to (success (s , show p))
 
 {-# COMPILE GHC epoch-step as epochStep #-}
+
+-- An alternative implementation of EPOCH that connects the conformance state
+-- with the specification rule.
+
+spec-epoch-step
+  : HsType (⊤ → EpochState → Epoch → ComputationResult ⊥ (EpochState × String))
+spec-epoch-step _ epochSt e =
+  let r = EpochSpec.Computational-EPOCH .computeProof _ (conv (from epochSt)) e
+  in case r of λ where
+    (success (s , p)) → to (success (conv s , show p))
+
+{-# COMPILE GHC spec-epoch-step as specEpochStep #-}

src/Ledger/Conway/Foreign/HSLedger/Gov.agda

@@ -109,8 +109,14 @@ unquoteDecl = do
 
 -- Computational function
 
-gov-step : HsType (GovEnv → GovState → List (GovVote ⊎ GovProposal) → ComputationResult String GovState)
-gov-step Γ govSt gvps = to (compute Computational-GOVS ⟦ txid , e' , pparams , ppolicy , enactState , to certState , rewardCreds ⟧ (from govSt) (from gvps))
+gov-step
+  : HsType (GovEnv → GovState → List (GovVote ⊎ GovProposal)
+  → ComputationResult String GovState)
+gov-step Γ govSt gvps =
+    to $ compute Computational-GOVS
+      ⟦ txid , e' , pparams , ppolicy , enactState , to certState , rewardCreds ⟧
+      (from govSt)
+      (from gvps)
   where open GovEnv (from Γ) renaming (epoch to e')
 
 {-# COMPILE GHC gov-step as govStep #-}

src/Ledger/Conway/Foreign/HSLedger/NewEpoch.agda

@@ -4,6 +4,7 @@ open import Ledger.Conway.Foreign.HSLedger.BaseTypes
 open import Ledger.Conway.Foreign.HSLedger.Epoch
 open import Ledger.Conway.Foreign.HSLedger.Rewards
 
+open import Ledger.Conway.Conformance.Equivalence.Convert
 open import Ledger.Conway.Conformance.Epoch it it
 open import Ledger.Conway.Conformance.Epoch.Properties it it
 
@@ -15,6 +16,11 @@ instance
   Show-NEWEPOCH .show (NEWEPOCH-Not-New x)          = "NEWEPOCH-Not-New"
   Show-NEWEPOCH .show (NEWEPOCH-No-Reward-Update x) = "NEWEPOCH-No-Reward-Update"
 
+  Show-SPEC-NEWEPOCH : ∀ {eps e eps'} → Show (_ EpochSpec.⊢ eps ⇀⦇ e ,NEWEPOCH⦈ eps')
+  Show-SPEC-NEWEPOCH .show (EpochSpec.NEWEPOCH-New (_ , e))        = "NEWEPOCH-New " S.++ show e
+  Show-SPEC-NEWEPOCH .show (EpochSpec.NEWEPOCH-Not-New x)          = "NEWEPOCH-Not-New"
+  Show-SPEC-NEWEPOCH .show (EpochSpec.NEWEPOCH-No-Reward-Update x) = "NEWEPOCH-No-Reward-Update"
+
 instance
   HsTy-NewEpochState = autoHsType NewEpochState ⊣ withConstructor "MkNewEpochState"
   Conv-NewEpochState = autoConvert NewEpochState
@@ -27,3 +33,14 @@ newepoch-step _ newEpochSt e =
 
 {-# COMPILE GHC newepoch-step as newEpochStep #-}
 
+-- An alternative implementation of NEWEPOCH that connects the conformance state
+-- with the specification rule.
+
+spec-newepoch-step
+  : HsType (⊤ → NewEpochState → Epoch → ComputationResult ⊥ (NewEpochState × String))
+spec-newepoch-step _ neSt e =
+  let r = EpochSpec.Computational-NEWEPOCH .computeProof _ (conv (from neSt)) e
+  in case r of λ where
+    (success (s , p)) → to (success (conv s , show p))
+
+{-# COMPILE GHC spec-newepoch-step as specNewEpochStep #-}

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

@@ -55,13 +55,13 @@ open import Ledger.Conway.Specification.Utxo txs abs
 ```agda
 record EpochState : Type where
 ```
- 
+
 <!--
 ```agda
   constructor ⟦_,_,_,_,_⟧ᵉ'
 ```
 -->
- 
+
 ```agda
   field
     acnt       : Acnt
@@ -126,13 +126,13 @@ record NewEpochState : Type where
     The formal specification utilizes the type `PoolDelegatedStake`{.AgdaDatatype}
     in lieu of the derived type `PoolDistr`{.AgdaDatatype} (Figure 5, Shelley
     specification [CVG19](#shelley-ledger-spec)). The latter can be computed from the
-    former by divinding the associated `Coin`{.AgdaDatatype} to each `KeyHash`{.AgdaDatatype} 
+    former by divinding the associated `Coin`{.AgdaDatatype} to each `KeyHash`{.AgdaDatatype}
     by the total stake in the map.
 
     In addition, the formal specification omits the VRF key hashes in the
     codomain of `PoolDelegatedStake`{.AgdaDatatype} as they are not implemented at
     the moment.
- 
+
 <!--
 ```agda
 record HasNewEpochState {a} (A : Type a) : Type a where
@@ -625,7 +625,7 @@ EPOCH-updates fut ls dState' acnt' =
 
 ### Transition Rule
 
-This section defines the `EPOCH`{.AgdaDatatype} transition rule. 
+This section defines the `EPOCH`{.AgdaDatatype} transition rule.
 
 In Conway, the `EPOCH`{.AgdaDatatype} rule invokes `RATIFIES`{.AgdaDatatype},
 and carries out the following tasks:
@@ -694,7 +694,7 @@ data
 ```
 -->
 ```agda
-  NEWEPOCH-New : 
+  NEWEPOCH-New :
 ```
 <!--
 ```agda
@@ -717,7 +717,7 @@ data
       ──────────────────────────────────────────────
       _ ⊢ ⟦ lastEpoch , bprev , bcur , eps , mru , pd ⟧ ⇀⦇ e ,NEWEPOCH⦈ ⟦ lastEpoch , bprev , bcur , eps , mru , pd ⟧
 
-  NEWEPOCH-No-Reward-Update : 
+  NEWEPOCH-No-Reward-Update :
 ```
 <!--
 ```agda