Change state of shelley DelegRule to CertState

Author: teodanciu

eras/shelley/impl/CHANGELOG.md

@@ -2,6 +2,8 @@
 
 ## 1.17.1.0
 
+* Change state of `ShelleyDELEG` rule from `DState` to `CertState`
+* Add `EraCertState` constraint to `STS` instance for `ShelleyDELEG`
 * Added `Generic` instance to `ShelleyTxOut`
 
 ### `testlib`

eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Deleg.hs

@@ -131,10 +131,15 @@ newtype ShelleyDelegEvent era = DelegNewEpoch EpochNo
 instance NFData (ShelleyDelegEvent era)
 
 instance
-  (EraPParams era, ShelleyEraAccounts era, ShelleyEraTxCert era, AtMostEra "Babbage" era) =>
+  ( EraCertState era
+  , EraPParams era
+  , ShelleyEraAccounts era
+  , ShelleyEraTxCert era
+  , AtMostEra "Babbage" era
+  ) =>
   STS (ShelleyDELEG era)
   where
-  type State (ShelleyDELEG era) = DState era
+  type State (ShelleyDELEG era) = CertState era
   type Signal (ShelleyDELEG era) = TxCert era
   type Environment (ShelleyDELEG era) = DelegEnv era
   type BaseM (ShelleyDELEG era) = ShelleyBase
@@ -242,17 +247,23 @@ instance
       k -> invalidKey k
 
 delegationTransition ::
-  (ShelleyEraAccounts era, ShelleyEraTxCert era, EraPParams era, AtMostEra "Babbage" era) =>
+  ( EraCertState era
+  , ShelleyEraAccounts era
+  , ShelleyEraTxCert era
+  , EraPParams era
+  , AtMostEra "Babbage" era
+  ) =>
   TransitionRule (ShelleyDELEG era)
 delegationTransition = do
-  TRC (DelegEnv slot epochNo ptr chainAccountState pp, ds, c) <- judgmentContext
+  TRC (DelegEnv slot epochNo ptr chainAccountState pp, certState, c) <- judgmentContext
   let pv = pp ^. ppProtocolVersionL
+      ds = certState ^. certDStateL
   case c of
     RegTxCert cred -> do
       -- (hk ∉ dom (rewards ds))
       not (isAccountRegistered cred (ds ^. accountsL)) ?! StakeKeyAlreadyRegisteredDELEG cred
       let compactDeposit = compactCoinOrError (pp ^. ppKeyDepositL)
-      pure (ds & accountsL %~ registerShelleyAccount cred ptr compactDeposit Nothing)
+      pure $ certState & certDStateL . accountsL %~ registerShelleyAccount cred ptr compactDeposit Nothing
     UnRegTxCert cred -> do
       let !(mAccountState, !accounts) = unregisterShelleyAccount cred (ds ^. accountsL)
           checkStakeKeyHasZeroRewardBalance = do
@@ -263,13 +274,14 @@ delegationTransition = do
       -- (hk ∈ dom (rewards ds))
       isJust mAccountState ?! StakeKeyNotRegisteredDELEG cred
       failOnJust checkStakeKeyHasZeroRewardBalance StakeKeyNonZeroAccountBalanceDELEG
-      pure $ ds & accountsL .~ accounts
+      pure $ certState & certDStateL . accountsL .~ accounts
     DelegStakeTxCert cred stakePool -> do
       -- note that pattern match is used instead of cwitness and dpool, as in the spec
       -- (hk ∈ dom (rewards ds))
       isAccountRegistered cred (ds ^. accountsL) ?! StakeDelegationImpossibleDELEG cred
       pure $
-        ds & accountsL %~ adjustAccountState (stakePoolDelegationAccountStateL ?~ stakePool) cred
+        certState
+          & certDStateL . accountsL %~ adjustAccountState (stakePoolDelegationAccountStateL ?~ stakePool) cred
     GenesisDelegTxCert gkh vkh vrf -> do
       sp <- liftSTS $ asks stabilityWindow
       -- note that pattern match is used instead of genesisDeleg, as in the spec
@@ -294,13 +306,12 @@ delegationTransition = do
         ?! DuplicateGenesisVRFDELEG vrf
 
       pure $
-        ds
-          { dsFutureGenDelegs =
-              eval (dsFutureGenDelegs ds ⨃ singleton (FutureGenDeleg s' gkh) (GenDelegPair vkh vrf))
-          }
+        certState
+          & certDStateL . dsFutureGenDelegsL
+            .~ eval (dsFutureGenDelegs ds ⨃ singleton (FutureGenDeleg s' gkh) (GenDelegPair vkh vrf))
     RegPoolTxCert _ -> do
       failBecause WrongCertificateTypeDELEG -- this always fails
-      pure ds
+      pure certState
     _ | Just (MIRCert targetPot mirTarget) <- getMirTxCert c -> do
       checkSlotNotTooLate slot epochNo
       case mirTarget of
@@ -327,46 +338,39 @@ delegationTransition = do
               else do
                 all (>= mempty) credCoinMap ?! MIRNegativesNotCurrentlyAllowed
                 pure (Map.union credCoinMap' instantaneousRewards, potAmount)
-          updateReservesAndTreasury targetPot combinedMap available ds
+          updateReservesAndTreasury targetPot combinedMap available certState
         SendToOppositePotMIR coin ->
           if hardforkAlonzoAllowMIRTransfer pv
             then do
               let available = availableAfterMIR targetPot chainAccountState (dsIRewards ds)
               coin >= mempty ?! MIRNegativeTransfer targetPot coin
               coin <= available ?! InsufficientForTransferDELEG targetPot (Mismatch coin available)
-
-              let ir = dsIRewards ds
-                  dr = deltaReserves ir
-                  dt = deltaTreasury ir
               case targetPot of
                 ReservesMIR ->
                   pure $
-                    ds
-                      { dsIRewards =
-                          ir
-                            { deltaReserves = dr <> invert (toDeltaCoin coin)
-                            , deltaTreasury = dt <> toDeltaCoin coin
-                            }
-                      }
+                    certState
+                      & certDStateL . dsIRewardsL . iRDeltaReservesL %~ (<> invert (toDeltaCoin coin))
+                      & certDStateL . dsIRewardsL . iRDeltaTreasuryL %~ (<> toDeltaCoin coin)
                 TreasuryMIR ->
                   pure $
-                    ds
-                      { dsIRewards =
-                          ir
-                            { deltaReserves = dr <> toDeltaCoin coin
-                            , deltaTreasury = dt <> invert (toDeltaCoin coin)
-                            }
-                      }
+                    certState
+                      & certDStateL . dsIRewardsL . iRDeltaReservesL %~ (<> toDeltaCoin coin)
+                      & certDStateL . dsIRewardsL . iRDeltaTreasuryL %~ (<> invert (toDeltaCoin coin))
             else do
               failBecause MIRTransferNotCurrentlyAllowed
-              pure ds
+              pure certState
     _ -> do
       -- The impossible case
       failBecause WrongCertificateTypeDELEG -- this always fails
-      pure ds
+      pure certState
 
 checkSlotNotTooLate ::
-  (ShelleyEraAccounts era, ShelleyEraTxCert era, EraPParams era, AtMostEra "Babbage" era) =>
+  ( EraCertState era
+  , ShelleyEraAccounts era
+  , ShelleyEraTxCert era
+  , EraPParams era
+  , AtMostEra "Babbage" era
+  ) =>
   SlotNo ->
   EpochNo ->
   Rule (ShelleyDELEG era) 'Transition ()
@@ -380,12 +384,13 @@ checkSlotNotTooLate slot curEpochNo = do
   slot < tooLate ?! MIRCertificateTooLateinEpochDELEG (Mismatch slot tooLate)
 
 updateReservesAndTreasury ::
+  EraCertState era =>
   MIRPot ->
   Map.Map (Credential 'Staking) Coin ->
   Coin ->
-  DState era ->
-  Rule (ShelleyDELEG era) 'Transition (DState era)
-updateReservesAndTreasury targetPot combinedMap available ds = do
+  CertState era ->
+  Rule (ShelleyDELEG era) 'Transition (CertState era)
+updateReservesAndTreasury targetPot combinedMap available certState = do
   let requiredForRewards = fold combinedMap
   requiredForRewards
     <= available
@@ -397,5 +402,5 @@ updateReservesAndTreasury targetPot combinedMap available ds = do
           }
   pure $
     case targetPot of
-      ReservesMIR -> ds {dsIRewards = (dsIRewards ds) {iRReserves = combinedMap}}
-      TreasuryMIR -> ds {dsIRewards = (dsIRewards ds) {iRTreasury = combinedMap}}
+      ReservesMIR -> certState & certDStateL . dsIRewardsL . iRReservesL .~ combinedMap
+      TreasuryMIR -> certState & certDStateL . dsIRewardsL . iRTreasuryL .~ combinedMap

eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Delpl.hs

@@ -120,7 +120,7 @@ instance
   , EraCertState era
   , Embed (EraRule "DELEG" era) (ShelleyDELPL era)
   , Environment (EraRule "DELEG" era) ~ DelegEnv era
-  , State (EraRule "DELEG" era) ~ DState era
+  , State (EraRule "DELEG" era) ~ CertState era
   , Embed (EraRule "POOL" era) (ShelleyDELPL era)
   , Environment (EraRule "POOL" era) ~ PoolEnv era
   , State (EraRule "POOL" era) ~ PState era
@@ -183,7 +183,7 @@ delplTransition ::
   forall era.
   ( Embed (EraRule "DELEG" era) (ShelleyDELPL era)
   , Environment (EraRule "DELEG" era) ~ DelegEnv era
-  , State (EraRule "DELEG" era) ~ DState era
+  , State (EraRule "DELEG" era) ~ CertState era
   , State (EraRule "POOL" era) ~ PState era
   , Signal (EraRule "DELEG" era) ~ TxCert era
   , Embed (EraRule "POOL" era) (ShelleyDELPL era)
@@ -201,20 +201,14 @@ delplTransition = do
         trans @(EraRule "POOL" era) $ TRC (PoolEnv eNo pp, d ^. certPStateL, poolCert)
       pure $ d & certPStateL .~ ps
     ShelleyTxCertGenesisDeleg GenesisDelegCert {} -> do
-      ds <-
-        trans @(EraRule "DELEG" era) $
-          TRC (DelegEnv slot eNo ptr chainAccountState pp, d ^. certDStateL, c)
-      pure $ d & certDStateL .~ ds
+      trans @(EraRule "DELEG" era) $
+        TRC (DelegEnv slot eNo ptr chainAccountState pp, d, c)
     ShelleyTxCertDelegCert _ -> do
-      ds <-
-        trans @(EraRule "DELEG" era) $
-          TRC (DelegEnv slot eNo ptr chainAccountState pp, d ^. certDStateL, c)
-      pure $ d & certDStateL .~ ds
+      trans @(EraRule "DELEG" era) $
+        TRC (DelegEnv slot eNo ptr chainAccountState pp, d, c)
     ShelleyTxCertMir _ -> do
-      ds <-
-        trans @(EraRule "DELEG" era) $
-          TRC (DelegEnv slot eNo ptr chainAccountState pp, d ^. certDStateL, c)
-      pure $ d & certDStateL .~ ds
+      trans @(EraRule "DELEG" era) $
+        TRC (DelegEnv slot eNo ptr chainAccountState pp, d, c)
 
 instance
   ( Era era
@@ -230,6 +224,7 @@ instance
 instance
   ( ShelleyEraAccounts era
   , ShelleyEraTxCert era
+  , EraCertState era
   , EraPParams era
   , AtMostEra "Babbage" era
   , PredicateFailure (EraRule "DELEG" era) ~ ShelleyDelegPredFailure era

eras/shelley/test-suite/src/Test/Cardano/Ledger/Shelley/Rules/Deleg.hs

@@ -89,7 +89,7 @@ tests =
 
 -- | Check stake key registration
 keyRegistration ::
-  (EraAccounts era, ShelleyEraTxCert era) =>
+  (EraCertState era, ShelleyEraTxCert era) =>
   SourceSignalTarget (ShelleyDELEG era) ->
   Property
 keyRegistration
@@ -100,18 +100,18 @@ keyRegistration
     conjoin
       [ counterexample
           "a newly registered key should have a reward account"
-          (isAccountRegistered cred (targetSt ^. accountsL))
+          (isAccountRegistered cred (targetSt ^. certDStateL . accountsL))
       , counterexample
           "a newly registered key should have a reward account with 0 balance"
-          ( ((^. balanceAccountStateL) <$> lookupAccountState cred (targetSt ^. accountsL))
+          ( ((^. balanceAccountStateL) <$> lookupAccountState cred (targetSt ^. certDStateL . accountsL))
               === Just mempty
           )
       ]
 keyRegistration _ = property ()
 
 -- | Check stake key de-registration
 keyDeRegistration ::
-  (EraAccounts era, ShelleyEraTxCert era) =>
+  (EraCertState era, ShelleyEraTxCert era) =>
   SourceSignalTarget (ShelleyDELEG era) ->
   Property
 keyDeRegistration
@@ -122,16 +122,16 @@ keyDeRegistration
     conjoin
       [ counterexample
           "a deregistered stake key should no longer be in the rewards mapping"
-          (not (isAccountRegistered cred (targetSt ^. accountsL)))
+          (not (isAccountRegistered cred (targetSt ^. certDStateL . accountsL)))
       , counterexample
           "a deregistered stake key should no longer be in the delegations mapping"
-          (isNothing (lookupStakePoolDelegation cred (targetSt ^. accountsL)))
+          (isNothing (lookupStakePoolDelegation cred (targetSt ^. certDStateL . accountsL)))
       ]
 keyDeRegistration _ = property ()
 
 -- | Check stake key delegation
 keyDelegation ::
-  (EraAccounts era, ShelleyEraTxCert era) =>
+  (EraCertState era, ShelleyEraTxCert era) =>
   SourceSignalTarget (ShelleyDELEG era) ->
   Property
 keyDelegation
@@ -142,21 +142,21 @@ keyDelegation
     conjoin
       [ counterexample
           "a delegated key should have a reward account"
-          (isAccountRegistered stakeCred (targetSt ^. accountsL))
+          (isAccountRegistered stakeCred (targetSt ^. certDStateL . accountsL))
       , counterexample
           "a registered stake credential should be delegated"
-          (lookupStakePoolDelegation stakeCred (targetSt ^. accountsL) === Just poolId)
+          (lookupStakePoolDelegation stakeCred (targetSt ^. certDStateL . accountsL) === Just poolId)
       ]
 keyDelegation _ = property ()
 
 -- | Check that the sum of balances does not change and that each element
 -- that is either removed or added has a zero balance.
-balancesSumInvariant :: EraAccounts era => SourceSignalTarget (ShelleyDELEG era) -> Property
+balancesSumInvariant :: EraCertState era => SourceSignalTarget (ShelleyDELEG era) -> Property
 balancesSumInvariant
   SourceSignalTarget {source, target} =
     let accountsBalances ds = Map.map (^. balanceAccountStateL) (ds ^. accountsL . accountsMapL)
-        sourceBalances = accountsBalances source
-        targetBalances = accountsBalances target
+        sourceBalances = accountsBalances (source ^. certDStateL)
+        targetBalances = accountsBalances (target ^. certDStateL)
         balancesSum = F.foldl' (<>) mempty
      in conjoin
           [ counterexample
@@ -171,7 +171,7 @@ balancesSumInvariant
           ]
 
 checkInstantaneousRewards ::
-  (EraPParams era, ShelleyEraTxCert era, AtMostEra "Babbage" era) =>
+  (EraPParams era, EraCertState era, ShelleyEraTxCert era, AtMostEra "Babbage" era) =>
   DelegEnv era ->
   SourceSignalTarget (ShelleyDELEG era) ->
   Property
@@ -183,36 +183,36 @@ checkInstantaneousRewards
         conjoin
           [ counterexample
               "a ReservesMIR certificate should add all entries to the `irwd` mapping"
-              (Map.keysSet irwd `Set.isSubsetOf` Map.keysSet (iRReserves $ dsIRewards target))
+              (Map.keysSet irwd `Set.isSubsetOf` Map.keysSet (iRReserves $ dsIRewards (target ^. certDStateL)))
           , counterexample
               "a ReservesMIR certificate should add the total value to the `irwd` map, overwriting any existing entries"
               ( if hardforkAlonzoAllowMIRTransfer . view ppProtocolVersionL $ ppDE denv
                   then -- In the Alonzo era, repeated fields are added
-                    fold (iRReserves $ dsIRewards source)
+                    fold (iRReserves $ dsIRewards (source ^. certDStateL))
                       `addDeltaCoin` fold irwd
-                      == fold (iRReserves $ dsIRewards target)
+                      == fold (iRReserves $ dsIRewards (target ^. certDStateL))
                   else -- Prior to the Alonzo era, repeated fields overridden
-                    fold (iRReserves (dsIRewards source) Map.\\ irwd)
+                    fold (iRReserves (dsIRewards (source ^. certDStateL)) Map.\\ irwd)
                       `addDeltaCoin` fold irwd
-                      == fold (iRReserves $ dsIRewards target)
+                      == fold (iRReserves $ dsIRewards (target ^. certDStateL))
               )
           ]
       MirTxCert (MIRCert TreasuryMIR (StakeAddressesMIR irwd)) ->
         conjoin
           [ counterexample
               "a TreasuryMIR certificate should add all entries to the `irwd` mapping"
-              (Map.keysSet irwd `Set.isSubsetOf` Map.keysSet (iRTreasury $ dsIRewards target))
+              (Map.keysSet irwd `Set.isSubsetOf` Map.keysSet (iRTreasury $ dsIRewards (target ^. certDStateL)))
           , counterexample
               "a TreasuryMIR certificate should add* the total value to the `irwd` map"
               ( if hardforkAlonzoAllowMIRTransfer . view ppProtocolVersionL . ppDE $ denv
                   then -- In the Alonzo era, repeated fields are added
-                    fold (iRTreasury $ dsIRewards source)
+                    fold (iRTreasury $ dsIRewards (source ^. certDStateL))
                       `addDeltaCoin` fold irwd
-                      == fold (iRTreasury $ dsIRewards target)
+                      == fold (iRTreasury $ dsIRewards (target ^. certDStateL))
                   else -- Prior to the Alonzo era, repeated fields overridden
-                    fold (iRTreasury (dsIRewards source) Map.\\ irwd)
+                    fold (iRTreasury (dsIRewards (source ^. certDStateL)) Map.\\ irwd)
                       `addDeltaCoin` fold irwd
-                      == fold (iRTreasury $ dsIRewards target)
+                      == fold (iRTreasury $ dsIRewards (target ^. certDStateL))
               )
           ]
       _ -> property ()

eras/shelley/test-suite/src/Test/Cardano/Ledger/Shelley/Rules/TestChain.hs

@@ -220,7 +220,7 @@ delegTraceFromBlock ::
 delegTraceFromBlock chainSt block =
   ( delegEnv
   , runShelleyBase $
-      Trace.closure @(ShelleyDELEG era) delegEnv delegSt0 blockCerts
+      Trace.closure @(ShelleyDELEG era) delegEnv (ledgerSt0 ^. lsCertStateL) blockCerts
   )
   where
     (_tickedChainSt, ledgerEnv, ledgerSt0, txs) = ledgerTraceBase chainSt block
@@ -231,8 +231,6 @@ delegTraceFromBlock chainSt block =
           dummyCertIx = minBound
           ptr = Ptr (SlotNo32 (fromIntegral slot64)) txIx dummyCertIx
        in DelegEnv slot (epochFromSlotNo slot) ptr reserves pp
-    delegSt0 =
-      ledgerSt0 ^. lsCertStateL . certDStateL
     delegCert (RegTxCert _) = True
     delegCert (UnRegTxCert _) = True
     delegCert (DelegStakeTxCert _ _) = True