added totalDiff, incorporated State (EraRule POOL) ~ (Diff PState) in…

… POOL rule, fixed tests.

eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs

@@ -453,6 +453,7 @@ instance ILC (EnactState era) where
   applyDiff x (EnactState' y) = applyTotal x y
   extend (EnactState' x) (EnactState' y) = EnactState' $ extend x y
   zero = EnactState' Zero
+  totalDiff x = EnactState' (Total' x)
 
 deriving instance Eq (PParamsHKD Identity era) => Eq (Diff (EnactState era))
 deriving instance Show (PParamsHKD Identity era) => Show (Diff (EnactState era))
@@ -541,6 +542,7 @@ instance ILC (RatifyState era) where
       , diffRsFuture = extend (diffRsFuture x) (diffRsFuture y)
       }
   zero = RatifyState' zero zero
+  totalDiff (RatifyState x y) = RatifyState' (totalDiff x) (Total' y)
 
 deriving instance EraPParams era => Eq (Diff (RatifyState era))
 deriving instance EraPParams era => Show (Diff (RatifyState era))
@@ -608,6 +610,8 @@ instance ILC (ConwayGovernance era) where
       , diffCgVoterRoles = extend (diffCgVoterRoles x) (diffCgVoterRoles y)
       }
   zero = ConwayGovernance' zero zero zero
+  totalDiff (ConwayGovernance (ConwayTallyState x) y z) =
+    ConwayGovernance' (totalDiff x) (totalDiff y) (totalDiff z)
 
 deriving instance (EraPParams era) => (Eq (Diff (ConwayGovernance era)))
 deriving instance (EraPParams era) => (Show (Diff (ConwayGovernance era)))

eras/shelley/impl/src/Cardano/Ledger/Shelley/Governance.hs

@@ -94,6 +94,7 @@ instance ILC (ShelleyPPUPState era) where
       , diffFutureProposals = extend (diffFutureProposals x) (diffFutureProposals y)
       }
   zero = ShelleyPPUPState' zero zero
+  totalDiff _ = ShelleyPPUPState' zero zero
 
 deriving instance Show (PParamsUpdate era) => Show (Diff (ShelleyPPUPState era))
 

eras/shelley/impl/src/Cardano/Ledger/Shelley/LedgerState/Types.hs

@@ -262,6 +262,7 @@ instance ILC (IncrementalStake c) where
       , diffPtrMap = extend (diffPtrMap x) (diffPtrMap y)
       }
   zero = IStake' mempty mempty
+  totalDiff (IStake x y) = IStake' (totalDiff (MM x)) (totalDiff (MM y))
 
 deriving instance Eq (Diff (IncrementalStake c))
 deriving instance Show (Diff (IncrementalStake c))
@@ -344,6 +345,8 @@ instance ILC (GovernanceState era) => ILC (UTxOState era) where
       , diffUtxosStakeDistr = extend (diffUtxosStakeDistr x) (diffUtxosStakeDistr y)
       }
   zero = UTxOState' zero zero zero zero zero
+  totalDiff (UTxOState (UTxO v) w x y z) =
+    UTxOState' (totalDiff v) (totalDiff w) (totalDiff x) (totalDiff y) (totalDiff z)
 
 deriving instance (Eq (Diff (GovernanceState era)), Eq (TxOut era)) => Eq (Diff (UTxOState era))
 deriving instance (Show (Diff (GovernanceState era)), Show (TxOut era)) => Show (Diff (UTxOState era))
@@ -559,6 +562,7 @@ instance ILC (GovernanceState era) => ILC (LedgerState era) where
   applyDiff (LedgerState x y) (LedgerState' xD yD) = LedgerState (x $$ xD) (y $$ yD)
   zero = LedgerState' zero zero
   extend (LedgerState' x y) (LedgerState' a b) = LedgerState' (extend x a) (extend y b)
+  totalDiff (LedgerState x y) = LedgerState' (totalDiff x) (totalDiff y)
 
 deriving instance
   (Eq (Diff (GovernanceState era)), Eq (TxOut era)) =>

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

@@ -51,6 +51,7 @@ import Cardano.Ledger.Shelley.TxBody (
 import Cardano.Ledger.Slot (SlotNo)
 import Control.DeepSeq
 import Control.State.Transition
+import Data.Incremental (ILC (..))
 import Data.Typeable (Typeable)
 import Data.Word (Word8)
 import GHC.Generics (Generic)
@@ -104,7 +105,7 @@ instance
   , Signal (EraRule "DELEG" era) ~ DCert (EraCrypto era)
   , Embed (EraRule "POOL" era) (ShelleyDELPL era)
   , Environment (EraRule "POOL" era) ~ PoolEnv era
-  , State (EraRule "POOL" era) ~ PState (EraCrypto era)
+  , State (EraRule "POOL" era) ~ Diff (PState (EraCrypto era))
   , Signal (EraRule "POOL" era) ~ DCert (EraCrypto era)
   ) =>
   STS (ShelleyDELPL era)
@@ -165,21 +166,22 @@ delplTransition ::
   , Signal (EraRule "DELEG" era) ~ DCert (EraCrypto era)
   , Embed (EraRule "POOL" era) (ShelleyDELPL era)
   , Environment (EraRule "POOL" era) ~ PoolEnv era
-  , State (EraRule "POOL" era) ~ PState (EraCrypto era)
+  , State (EraRule "POOL" era) ~ Diff (PState (EraCrypto era))
   , Signal (EraRule "POOL" era) ~ DCert (EraCrypto era)
   ) =>
   TransitionRule (ShelleyDELPL era)
 delplTransition = do
   TRC (DelplEnv slot ptr pp acnt, d, c) <- judgmentContext
+  let pstate = dpsPState d
   case c of
     DCertPool (RegPool _) -> do
-      ps <-
-        trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp, dpsPState d, c)
-      pure $ d {dpsPState = ps}
+      dps <-
+        trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp pstate, totalDiff pstate, c)
+      pure $ d {dpsPState = applyDiff pstate dps}
     DCertPool (RetirePool _ _) -> do
-      ps <-
-        trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp, dpsPState d, c)
-      pure $ d {dpsPState = ps}
+      dps <-
+        trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp pstate, totalDiff pstate, c)
+      pure $ d {dpsPState = applyDiff pstate dps}
     DCertGenesis ConstitutionalDelegCert {} -> do
       ds <-
         trans @(EraRule "DELEG" era) $ TRC (DelegEnv slot ptr acnt pp, dpsDState d, c)

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

@@ -39,10 +39,11 @@ import Cardano.Ledger.Binary (
 import Cardano.Ledger.Coin (Coin)
 import Cardano.Ledger.Core
 import qualified Cardano.Ledger.Crypto as CC (Crypto (HASH))
+import Cardano.Ledger.DPState (Diff (..))
 import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..))
 import Cardano.Ledger.Shelley.Era (ShelleyPOOL)
 import qualified Cardano.Ledger.Shelley.HardForks as HardForks
-import Cardano.Ledger.Shelley.LedgerState (PState (..), payPoolDeposit, Diff)
+import Cardano.Ledger.Shelley.LedgerState (PState (..), payPoolDeposit)
 import qualified Cardano.Ledger.Shelley.SoftForks as SoftForks
 import Cardano.Ledger.Shelley.TxBody (
   DCert (..),
@@ -67,12 +68,11 @@ import Control.State.Transition (
   (?!),
  )
 import qualified Data.ByteString as BS
+import Data.Incremental (deleteD, insertD, ($$))
 import Data.Word (Word8)
 import GHC.Generics (Generic)
 import Lens.Micro ((^.))
 import NoThunks.Class (NoThunks (..))
-import Cardano.Ledger.DPState (Diff (..))
-import Data.Incremental (insertD, deleteD, ($$))
 
 data PoolEnv era
   = PoolEnv !SlotNo !(PParams era) !(PState (EraCrypto era))
@@ -200,13 +200,14 @@ poolDelegationTransition = do
           -- register new, Pool-Reg
           tellEvent $ RegisterPool hk
           pure $
-            payPoolDeposit 
-              hk 
+            payPoolDeposit
+              hk
               pp
-              ps
-              (ps'
-                { diffPsStakePoolParams = insertD hk poolParam
-                })
+              (ps $$ ps')
+              ( ps'
+                  { diffPsStakePoolParams = insertD hk poolParam <> diffPsStakePoolParams ps'
+                  }
+              )
         else do
           tellEvent $ ReregisterPool hk
           -- hk is already registered, so we want to reregister it. That means adding it to the
@@ -218,8 +219,8 @@ poolDelegationTransition = do
           -- if that has happened, we cannot be in this branch of the if statement.
           pure $
             ps'
-              { diffPsFutureStakePoolParams = insertD hk poolParam
-              , diffPsRetiring = deleteD hk
+              { diffPsFutureStakePoolParams = insertD hk poolParam <> diffPsFutureStakePoolParams ps'
+              , diffPsRetiring = deleteD hk <> diffPsRetiring ps'
               }
     DCertPool (RetirePool hk e) -> do
       -- note that pattern match is used instead of cwitness, as in the spec

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

@@ -81,3 +81,14 @@ commonTests =
   , ByronTranslation.testGroupByronTranslation
   , ShelleyTranslation.testGroupShelleyTranslation
   ]
+
+-- ================================
+-- an example how one might debug one test, which can be replayed
+-- import Test.Tasty (defaultMain)
+-- import Cardano.Ledger.Crypto(StandardCrypto)
+-- import Cardano.Ledger.Shelley(ShelleyEra)
+-- main :: IO ()
+-- main = main = defaultMain (Pool.tests @(ShelleyEra StandardCrypto))
+-- Then in ghci, one can just type
+-- :main --quickcheck-replay=443873
+-- =================================

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

@@ -32,6 +32,7 @@ import Cardano.Protocol.TPraos.BHeader (
   bheaderSlotNo,
  )
 import Control.SetAlgebra (dom, eval, (∈), (∉))
+import Control.State.Transition (STS (State))
 import Control.State.Transition.Trace (
   SourceSignalTarget (..),
   TraceOrder (OldestFirst),
@@ -97,9 +98,9 @@ poolRetirement ::
   Property
 poolRetirement SourceSignalTarget {source = chainSt, signal = block} =
   conjoin $
-    map (poolRetirementProp currentEpoch maxEpoch) (sourceSignalTargets poolTr)
+    map (poolRetirementProp unDiff currentEpoch maxEpoch) (sourceSignalTargets poolTr)
   where
-    (chainSt', poolTr) = poolTraceFromBlock chainSt block
+    (chainSt', poolTr, unDiff) = poolTraceFromBlock chainSt block
     bhb = bhbody $ bheader block
     currentEpoch = (epochFromSlotNo . bheaderSlotNo) bhb
     maxEpoch = (view ppEMaxL . esPp . nesEs . chainNes) chainSt'
@@ -116,9 +117,9 @@ poolRegistration ::
   Property
 poolRegistration (SourceSignalTarget {source = chainSt, signal = block}) =
   conjoin $
-    map poolRegistrationProp (sourceSignalTargets poolTr)
+    map (poolRegistrationProp unDiff) (sourceSignalTargets poolTr)
   where
-    (_, poolTr) = poolTraceFromBlock chainSt block
+    (_, poolTr, unDiff) = poolTraceFromBlock chainSt block
 
 -- | Assert that PState maps are in sync with each other after each `Signal
 -- POOL` transition.
@@ -132,49 +133,56 @@ poolStateIsInternallyConsistent ::
   Property
 poolStateIsInternallyConsistent (SourceSignalTarget {source = chainSt, signal = block}) =
   conjoin $
-    map poolStateIsInternallyConsistentProp (traceStates OldestFirst poolTr)
+    map (poolStateIsInternallyConsistentProp . unDiff) (traceStates OldestFirst poolTr)
   where
-    (_, poolTr) = poolTraceFromBlock chainSt block
+    (_, poolTr, unDiff) = poolTraceFromBlock chainSt block
 
-poolRegistrationProp :: SourceSignalTarget (ShelleyPOOL era) -> Property
+poolRegistrationProp :: (State (ShelleyPOOL era) -> PState (EraCrypto era)) -> SourceSignalTarget (ShelleyPOOL era) -> Property
 poolRegistrationProp
+  unDiff
   SourceSignalTarget
     { signal = (DCertPool (RegPool poolParams))
     , source = sourceSt
     , target = targetSt
     } =
     let hk = ppId poolParams
-        reRegistration = eval (hk ∈ dom (psStakePoolParams sourceSt))
+        reRegistration = eval (hk ∈ dom (psStakePoolParams (unDiff sourceSt)))
      in if reRegistration
           then
             conjoin
               [ counterexample
                   "Pre-existing PoolParams must still be registered in pParams"
-                  (eval (hk ∈ dom (psStakePoolParams targetSt)) :: Bool)
+                  (eval (hk ∈ dom (psStakePoolParams (unDiff targetSt))) :: Bool)
               , counterexample
                   "New PoolParams are registered in future Params map"
-                  (Map.lookup hk (psFutureStakePoolParams targetSt) === Just poolParams)
+                  (Map.lookup hk (psFutureStakePoolParams (unDiff targetSt)) === Just poolParams)
               , counterexample
                   "PoolParams are removed in 'retiring'"
-                  (eval (hk ∉ dom (psRetiring targetSt)) :: Bool)
+                  (eval (hk ∉ dom (psRetiring (unDiff targetSt))) :: Bool)
               ]
           else -- first registration
 
             conjoin
               [ counterexample
                   "New PoolParams are registered in pParams"
-                  (Map.lookup hk (psStakePoolParams targetSt) === Just poolParams)
+                  (Map.lookup hk (psStakePoolParams (unDiff targetSt)) === Just poolParams)
               , counterexample
                   "PoolParams are not present in 'future pool params'"
-                  (eval (hk ∉ dom (psFutureStakePoolParams targetSt)) :: Bool)
+                  (eval (hk ∉ dom (psFutureStakePoolParams (unDiff targetSt))) :: Bool)
               , counterexample
                   "PoolParams are removed in 'retiring'"
-                  (eval (hk ∉ dom (psRetiring targetSt)) :: Bool)
+                  (eval (hk ∉ dom (psRetiring (unDiff targetSt))) :: Bool)
               ]
-poolRegistrationProp _ = property ()
+poolRegistrationProp _ _ = property ()
 
-poolRetirementProp :: EpochNo -> EpochNo -> SourceSignalTarget (ShelleyPOOL era) -> Property
+poolRetirementProp ::
+  (State (ShelleyPOOL era) -> PState (EraCrypto era)) ->
+  EpochNo ->
+  EpochNo ->
+  SourceSignalTarget (ShelleyPOOL era) ->
+  Property
 poolRetirementProp
+  unDiff
   currentEpoch@(EpochNo ce)
   (EpochNo maxEpoch)
   SourceSignalTarget {source = sourceSt, target = targetSt, signal = (DCertPool (RetirePool hk e))} =
@@ -184,15 +192,15 @@ poolRetirementProp
           (currentEpoch < e && e < EpochNo (ce + maxEpoch))
       , counterexample
           "hk must be in source stPools"
-          (eval (hk ∈ dom (psStakePoolParams sourceSt)) :: Bool)
+          (eval (hk ∈ dom (psStakePoolParams (unDiff sourceSt))) :: Bool)
       , counterexample
           "hk must be in target stPools"
-          (eval (hk ∈ dom (psStakePoolParams targetSt)) :: Bool)
+          (eval (hk ∈ dom (psStakePoolParams (unDiff targetSt))) :: Bool)
       , counterexample
           "hk must be in target's retiring"
-          (eval (hk ∈ dom (psRetiring targetSt)) :: Bool)
+          (eval (hk ∈ dom (psRetiring (unDiff targetSt))) :: Bool)
       ]
-poolRetirementProp _ _ _ = property ()
+poolRetirementProp _ _ _ _ = property ()
 
 poolStateIsInternallyConsistentProp :: PState c -> Property
 poolStateIsInternallyConsistentProp PState {psStakePoolParams = pParams_, psRetiring = retiring_} = do

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

@@ -36,6 +36,7 @@ import Cardano.Ledger.Shelley.LedgerState (
   EpochState (..),
   LedgerState (..),
   NewEpochState (..),
+  PState,
   UTxOState (..),
  )
 import Cardano.Ledger.Shelley.Rules (
@@ -65,6 +66,7 @@ import Control.State.Transition.Trace.Generator.QuickCheck (forAllTraceFromInitS
 import qualified Control.State.Transition.Trace.Generator.QuickCheck as QC
 import Data.Foldable (toList)
 import Data.Functor.Identity (Identity)
+import Data.Incremental (ILC (..))
 import qualified Data.Map.Strict as Map
 import Data.Proxy
 import qualified Data.Set as Set
@@ -185,19 +187,19 @@ poolTraceFromBlock ::
   ) =>
   ChainState era ->
   Block (BHeader (EraCrypto era)) era ->
-  (ChainState era, Trace (ShelleyPOOL era))
+  (ChainState era, Trace (ShelleyPOOL era), State (ShelleyPOOL era) -> PState (EraCrypto era))
 poolTraceFromBlock chainSt block =
   ( tickedChainSt
-  , runShelleyBase $
-      Trace.closure @(ShelleyPOOL era) poolEnv poolSt0 poolCerts
+  , runShelleyBase $ Trace.closure @(ShelleyPOOL era) poolEnv (totalDiff poolSt0) poolCerts
+  , applyDiff poolSt0
   )
   where
     (tickedChainSt, ledgerEnv, ledgerSt0, txs) = ledgerTraceBase chainSt block
     certs = concatMap (toList . view certsTxBodyL . view bodyTxL)
     poolCerts = filter poolCert (certs txs)
     poolEnv =
       let (LedgerEnv s _ pp _) = ledgerEnv
-       in PoolEnv s pp
+       in PoolEnv s pp poolSt0
     poolSt0 =
       let LedgerState _ (DPState _ poolSt0_) = ledgerSt0
        in poolSt0_

eras/shelley/test-suite/test/Test/Cardano/Ledger/Shelley/Examples/NetworkID.hs

@@ -21,6 +21,7 @@ import Cardano.Ledger.Shelley.Core
 import Cardano.Ledger.Slot (SlotNo (..))
 import Control.State.Transition.Extended hiding (Assertion)
 import Data.Default.Class (def)
+import Data.Incremental (ILC (..))
 import Lens.Micro
 import Test.Cardano.Ledger.Shelley.ConcreteCryptoTypes (C_Crypto)
 import qualified Test.Cardano.Ledger.Shelley.Examples.Cast as Cast
@@ -49,8 +50,8 @@ testPoolNetworkID pv poolParams e = do
         runShelleyBase $
           applySTSTest @(ShelleyPOOL ShelleyTest)
             ( TRC
-                ( PoolEnv (SlotNo 0) $ emptyPParams & ppProtocolVersionL .~ pv
-                , def
+                ( PoolEnv (SlotNo 0) (emptyPParams & ppProtocolVersionL .~ pv) def
+                , totalDiff def
                 , DCertPool (RegPool poolParams)
                 )
             )