Skip to content

Commit 9e94415

Browse files
TimSheardTimSheard
committed
added totalDiff, incorporated State (EraRule POOL) ~ (Diff PState) in POOL rule, fixed tests.
1 parent 306b4e8 commit 9e94415

File tree

14 files changed

+99
-49
lines changed

14 files changed

+99
-49
lines changed

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -453,6 +453,7 @@ instance ILC (EnactState era) where
453453
applyDiff x (EnactState' y) = applyTotal x y
454454
extend (EnactState' x) (EnactState' y) = EnactState' $ extend x y
455455
zero = EnactState' Zero
456+
totalDiff x = EnactState' (Total' x)
456457

457458
deriving instance Eq (PParamsHKD Identity era) => Eq (Diff (EnactState era))
458459
deriving instance Show (PParamsHKD Identity era) => Show (Diff (EnactState era))
@@ -541,6 +542,7 @@ instance ILC (RatifyState era) where
541542
, diffRsFuture = extend (diffRsFuture x) (diffRsFuture y)
542543
}
543544
zero = RatifyState' zero zero
545+
totalDiff (RatifyState x y) = RatifyState' (totalDiff x) (Total' y)
544546

545547
deriving instance EraPParams era => Eq (Diff (RatifyState era))
546548
deriving instance EraPParams era => Show (Diff (RatifyState era))
@@ -608,6 +610,8 @@ instance ILC (ConwayGovernance era) where
608610
, diffCgVoterRoles = extend (diffCgVoterRoles x) (diffCgVoterRoles y)
609611
}
610612
zero = ConwayGovernance' zero zero zero
613+
totalDiff (ConwayGovernance (ConwayTallyState x) y z) =
614+
ConwayGovernance' (totalDiff x) (totalDiff y) (totalDiff z)
611615

612616
deriving instance (EraPParams era) => (Eq (Diff (ConwayGovernance era)))
613617
deriving instance (EraPParams era) => (Show (Diff (ConwayGovernance era)))

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,7 @@ instance ILC (ShelleyPPUPState era) where
9494
, diffFutureProposals = extend (diffFutureProposals x) (diffFutureProposals y)
9595
}
9696
zero = ShelleyPPUPState' zero zero
97+
totalDiff _ = ShelleyPPUPState' zero zero
9798

9899
deriving instance Show (PParamsUpdate era) => Show (Diff (ShelleyPPUPState era))
99100

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -262,6 +262,7 @@ instance ILC (IncrementalStake c) where
262262
, diffPtrMap = extend (diffPtrMap x) (diffPtrMap y)
263263
}
264264
zero = IStake' mempty mempty
265+
totalDiff (IStake x y) = IStake' (totalDiff (MM x)) (totalDiff (MM y))
265266

266267
deriving instance Eq (Diff (IncrementalStake c))
267268
deriving instance Show (Diff (IncrementalStake c))
@@ -344,6 +345,8 @@ instance ILC (GovernanceState era) => ILC (UTxOState era) where
344345
, diffUtxosStakeDistr = extend (diffUtxosStakeDistr x) (diffUtxosStakeDistr y)
345346
}
346347
zero = UTxOState' zero zero zero zero zero
348+
totalDiff (UTxOState (UTxO v) w x y z) =
349+
UTxOState' (totalDiff v) (totalDiff w) (totalDiff x) (totalDiff y) (totalDiff z)
347350

348351
deriving instance (Eq (Diff (GovernanceState era)), Eq (TxOut era)) => Eq (Diff (UTxOState era))
349352
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
559562
applyDiff (LedgerState x y) (LedgerState' xD yD) = LedgerState (x $$ xD) (y $$ yD)
560563
zero = LedgerState' zero zero
561564
extend (LedgerState' x y) (LedgerState' a b) = LedgerState' (extend x a) (extend y b)
565+
totalDiff (LedgerState x y) = LedgerState' (totalDiff x) (totalDiff y)
562566

563567
deriving instance
564568
(Eq (Diff (GovernanceState era)), Eq (TxOut era)) =>

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

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,7 @@ import Cardano.Ledger.Shelley.TxBody (
5151
import Cardano.Ledger.Slot (SlotNo)
5252
import Control.DeepSeq
5353
import Control.State.Transition
54+
import Data.Incremental (ILC (..))
5455
import Data.Typeable (Typeable)
5556
import Data.Word (Word8)
5657
import GHC.Generics (Generic)
@@ -104,7 +105,7 @@ instance
104105
, Signal (EraRule "DELEG" era) ~ DCert (EraCrypto era)
105106
, Embed (EraRule "POOL" era) (ShelleyDELPL era)
106107
, Environment (EraRule "POOL" era) ~ PoolEnv era
107-
, State (EraRule "POOL" era) ~ PState (EraCrypto era)
108+
, State (EraRule "POOL" era) ~ Diff (PState (EraCrypto era))
108109
, Signal (EraRule "POOL" era) ~ DCert (EraCrypto era)
109110
) =>
110111
STS (ShelleyDELPL era)
@@ -165,21 +166,22 @@ delplTransition ::
165166
, Signal (EraRule "DELEG" era) ~ DCert (EraCrypto era)
166167
, Embed (EraRule "POOL" era) (ShelleyDELPL era)
167168
, Environment (EraRule "POOL" era) ~ PoolEnv era
168-
, State (EraRule "POOL" era) ~ PState (EraCrypto era)
169+
, State (EraRule "POOL" era) ~ Diff (PState (EraCrypto era))
169170
, Signal (EraRule "POOL" era) ~ DCert (EraCrypto era)
170171
) =>
171172
TransitionRule (ShelleyDELPL era)
172173
delplTransition = do
173174
TRC (DelplEnv slot ptr pp acnt, d, c) <- judgmentContext
175+
let pstate = dpsPState d
174176
case c of
175177
DCertPool (RegPool _) -> do
176-
ps <-
177-
trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp, dpsPState d, c)
178-
pure $ d {dpsPState = ps}
178+
dps <-
179+
trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp pstate, totalDiff pstate, c)
180+
pure $ d {dpsPState = applyDiff pstate dps}
179181
DCertPool (RetirePool _ _) -> do
180-
ps <-
181-
trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp, dpsPState d, c)
182-
pure $ d {dpsPState = ps}
182+
dps <-
183+
trans @(EraRule "POOL" era) $ TRC (PoolEnv slot pp pstate, totalDiff pstate, c)
184+
pure $ d {dpsPState = applyDiff pstate dps}
183185
DCertGenesis ConstitutionalDelegCert {} -> do
184186
ds <-
185187
trans @(EraRule "DELEG" era) $ TRC (DelegEnv slot ptr acnt pp, dpsDState d, c)

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

Lines changed: 12 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -39,10 +39,11 @@ import Cardano.Ledger.Binary (
3939
import Cardano.Ledger.Coin (Coin)
4040
import Cardano.Ledger.Core
4141
import qualified Cardano.Ledger.Crypto as CC (Crypto (HASH))
42+
import Cardano.Ledger.DPState (Diff (..))
4243
import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..))
4344
import Cardano.Ledger.Shelley.Era (ShelleyPOOL)
4445
import qualified Cardano.Ledger.Shelley.HardForks as HardForks
45-
import Cardano.Ledger.Shelley.LedgerState (PState (..), payPoolDeposit, Diff)
46+
import Cardano.Ledger.Shelley.LedgerState (PState (..), payPoolDeposit)
4647
import qualified Cardano.Ledger.Shelley.SoftForks as SoftForks
4748
import Cardano.Ledger.Shelley.TxBody (
4849
DCert (..),
@@ -67,12 +68,11 @@ import Control.State.Transition (
6768
(?!),
6869
)
6970
import qualified Data.ByteString as BS
71+
import Data.Incremental (deleteD, insertD, ($$))
7072
import Data.Word (Word8)
7173
import GHC.Generics (Generic)
7274
import Lens.Micro ((^.))
7375
import NoThunks.Class (NoThunks (..))
74-
import Cardano.Ledger.DPState (Diff (..))
75-
import Data.Incremental (insertD, deleteD, ($$))
7676

7777
data PoolEnv era
7878
= PoolEnv !SlotNo !(PParams era) !(PState (EraCrypto era))
@@ -200,13 +200,14 @@ poolDelegationTransition = do
200200
-- register new, Pool-Reg
201201
tellEvent $ RegisterPool hk
202202
pure $
203-
payPoolDeposit
204-
hk
203+
payPoolDeposit
204+
hk
205205
pp
206-
ps
207-
(ps'
208-
{ diffPsStakePoolParams = insertD hk poolParam
209-
})
206+
(ps $$ ps')
207+
( ps'
208+
{ diffPsStakePoolParams = insertD hk poolParam <> diffPsStakePoolParams ps'
209+
}
210+
)
210211
else do
211212
tellEvent $ ReregisterPool hk
212213
-- hk is already registered, so we want to reregister it. That means adding it to the
@@ -218,8 +219,8 @@ poolDelegationTransition = do
218219
-- if that has happened, we cannot be in this branch of the if statement.
219220
pure $
220221
ps'
221-
{ diffPsFutureStakePoolParams = insertD hk poolParam
222-
, diffPsRetiring = deleteD hk
222+
{ diffPsFutureStakePoolParams = insertD hk poolParam <> diffPsFutureStakePoolParams ps'
223+
, diffPsRetiring = deleteD hk <> diffPsRetiring ps'
223224
}
224225
DCertPool (RetirePool hk e) -> do
225226
-- note that pattern match is used instead of cwitness, as in the spec

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,3 +81,14 @@ commonTests =
8181
, ByronTranslation.testGroupByronTranslation
8282
, ShelleyTranslation.testGroupShelleyTranslation
8383
]
84+
85+
-- ================================
86+
-- an example how one might debug one test, which can be replayed
87+
-- import Test.Tasty (defaultMain)
88+
-- import Cardano.Ledger.Crypto(StandardCrypto)
89+
-- import Cardano.Ledger.Shelley(ShelleyEra)
90+
-- main :: IO ()
91+
-- main = main = defaultMain (Pool.tests @(ShelleyEra StandardCrypto))
92+
-- Then in ghci, one can just type
93+
-- :main --quickcheck-replay=443873
94+
-- =================================

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

Lines changed: 28 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ import Cardano.Protocol.TPraos.BHeader (
3232
bheaderSlotNo,
3333
)
3434
import Control.SetAlgebra (dom, eval, (∈), (∉))
35+
import Control.State.Transition (STS (State))
3536
import Control.State.Transition.Trace (
3637
SourceSignalTarget (..),
3738
TraceOrder (OldestFirst),
@@ -97,9 +98,9 @@ poolRetirement ::
9798
Property
9899
poolRetirement SourceSignalTarget {source = chainSt, signal = block} =
99100
conjoin $
100-
map (poolRetirementProp currentEpoch maxEpoch) (sourceSignalTargets poolTr)
101+
map (poolRetirementProp unDiff currentEpoch maxEpoch) (sourceSignalTargets poolTr)
101102
where
102-
(chainSt', poolTr) = poolTraceFromBlock chainSt block
103+
(chainSt', poolTr, unDiff) = poolTraceFromBlock chainSt block
103104
bhb = bhbody $ bheader block
104105
currentEpoch = (epochFromSlotNo . bheaderSlotNo) bhb
105106
maxEpoch = (view ppEMaxL . esPp . nesEs . chainNes) chainSt'
@@ -116,9 +117,9 @@ poolRegistration ::
116117
Property
117118
poolRegistration (SourceSignalTarget {source = chainSt, signal = block}) =
118119
conjoin $
119-
map poolRegistrationProp (sourceSignalTargets poolTr)
120+
map (poolRegistrationProp unDiff) (sourceSignalTargets poolTr)
120121
where
121-
(_, poolTr) = poolTraceFromBlock chainSt block
122+
(_, poolTr, unDiff) = poolTraceFromBlock chainSt block
122123

123124
-- | Assert that PState maps are in sync with each other after each `Signal
124125
-- POOL` transition.
@@ -132,49 +133,56 @@ poolStateIsInternallyConsistent ::
132133
Property
133134
poolStateIsInternallyConsistent (SourceSignalTarget {source = chainSt, signal = block}) =
134135
conjoin $
135-
map poolStateIsInternallyConsistentProp (traceStates OldestFirst poolTr)
136+
map (poolStateIsInternallyConsistentProp . unDiff) (traceStates OldestFirst poolTr)
136137
where
137-
(_, poolTr) = poolTraceFromBlock chainSt block
138+
(_, poolTr, unDiff) = poolTraceFromBlock chainSt block
138139

139-
poolRegistrationProp :: SourceSignalTarget (ShelleyPOOL era) -> Property
140+
poolRegistrationProp :: (State (ShelleyPOOL era) -> PState (EraCrypto era)) -> SourceSignalTarget (ShelleyPOOL era) -> Property
140141
poolRegistrationProp
142+
unDiff
141143
SourceSignalTarget
142144
{ signal = (DCertPool (RegPool poolParams))
143145
, source = sourceSt
144146
, target = targetSt
145147
} =
146148
let hk = ppId poolParams
147-
reRegistration = eval (hk ∈ dom (psStakePoolParams sourceSt))
149+
reRegistration = eval (hk ∈ dom (psStakePoolParams (unDiff sourceSt)))
148150
in if reRegistration
149151
then
150152
conjoin
151153
[ counterexample
152154
"Pre-existing PoolParams must still be registered in pParams"
153-
(eval (hk ∈ dom (psStakePoolParams targetSt)) :: Bool)
155+
(eval (hk ∈ dom (psStakePoolParams (unDiff targetSt))) :: Bool)
154156
, counterexample
155157
"New PoolParams are registered in future Params map"
156-
(Map.lookup hk (psFutureStakePoolParams targetSt) === Just poolParams)
158+
(Map.lookup hk (psFutureStakePoolParams (unDiff targetSt)) === Just poolParams)
157159
, counterexample
158160
"PoolParams are removed in 'retiring'"
159-
(eval (hk ∉ dom (psRetiring targetSt)) :: Bool)
161+
(eval (hk ∉ dom (psRetiring (unDiff targetSt))) :: Bool)
160162
]
161163
else -- first registration
162164

163165
conjoin
164166
[ counterexample
165167
"New PoolParams are registered in pParams"
166-
(Map.lookup hk (psStakePoolParams targetSt) === Just poolParams)
168+
(Map.lookup hk (psStakePoolParams (unDiff targetSt)) === Just poolParams)
167169
, counterexample
168170
"PoolParams are not present in 'future pool params'"
169-
(eval (hk ∉ dom (psFutureStakePoolParams targetSt)) :: Bool)
171+
(eval (hk ∉ dom (psFutureStakePoolParams (unDiff targetSt))) :: Bool)
170172
, counterexample
171173
"PoolParams are removed in 'retiring'"
172-
(eval (hk ∉ dom (psRetiring targetSt)) :: Bool)
174+
(eval (hk ∉ dom (psRetiring (unDiff targetSt))) :: Bool)
173175
]
174-
poolRegistrationProp _ = property ()
176+
poolRegistrationProp _ _ = property ()
175177

176-
poolRetirementProp :: EpochNo -> EpochNo -> SourceSignalTarget (ShelleyPOOL era) -> Property
178+
poolRetirementProp ::
179+
(State (ShelleyPOOL era) -> PState (EraCrypto era)) ->
180+
EpochNo ->
181+
EpochNo ->
182+
SourceSignalTarget (ShelleyPOOL era) ->
183+
Property
177184
poolRetirementProp
185+
unDiff
178186
currentEpoch@(EpochNo ce)
179187
(EpochNo maxEpoch)
180188
SourceSignalTarget {source = sourceSt, target = targetSt, signal = (DCertPool (RetirePool hk e))} =
@@ -184,15 +192,15 @@ poolRetirementProp
184192
(currentEpoch < e && e < EpochNo (ce + maxEpoch))
185193
, counterexample
186194
"hk must be in source stPools"
187-
(eval (hk ∈ dom (psStakePoolParams sourceSt)) :: Bool)
195+
(eval (hk ∈ dom (psStakePoolParams (unDiff sourceSt))) :: Bool)
188196
, counterexample
189197
"hk must be in target stPools"
190-
(eval (hk ∈ dom (psStakePoolParams targetSt)) :: Bool)
198+
(eval (hk ∈ dom (psStakePoolParams (unDiff targetSt))) :: Bool)
191199
, counterexample
192200
"hk must be in target's retiring"
193-
(eval (hk ∈ dom (psRetiring targetSt)) :: Bool)
201+
(eval (hk ∈ dom (psRetiring (unDiff targetSt))) :: Bool)
194202
]
195-
poolRetirementProp _ _ _ = property ()
203+
poolRetirementProp _ _ _ _ = property ()
196204

197205
poolStateIsInternallyConsistentProp :: PState c -> Property
198206
poolStateIsInternallyConsistentProp PState {psStakePoolParams = pParams_, psRetiring = retiring_} = do

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

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ import Cardano.Ledger.Shelley.LedgerState (
3636
EpochState (..),
3737
LedgerState (..),
3838
NewEpochState (..),
39+
PState,
3940
UTxOState (..),
4041
)
4142
import Cardano.Ledger.Shelley.Rules (
@@ -65,6 +66,7 @@ import Control.State.Transition.Trace.Generator.QuickCheck (forAllTraceFromInitS
6566
import qualified Control.State.Transition.Trace.Generator.QuickCheck as QC
6667
import Data.Foldable (toList)
6768
import Data.Functor.Identity (Identity)
69+
import Data.Incremental (ILC (..))
6870
import qualified Data.Map.Strict as Map
6971
import Data.Proxy
7072
import qualified Data.Set as Set
@@ -185,19 +187,19 @@ poolTraceFromBlock ::
185187
) =>
186188
ChainState era ->
187189
Block (BHeader (EraCrypto era)) era ->
188-
(ChainState era, Trace (ShelleyPOOL era))
190+
(ChainState era, Trace (ShelleyPOOL era), State (ShelleyPOOL era) -> PState (EraCrypto era))
189191
poolTraceFromBlock chainSt block =
190192
( tickedChainSt
191-
, runShelleyBase $
192-
Trace.closure @(ShelleyPOOL era) poolEnv poolSt0 poolCerts
193+
, runShelleyBase $ Trace.closure @(ShelleyPOOL era) poolEnv (totalDiff poolSt0) poolCerts
194+
, applyDiff poolSt0
193195
)
194196
where
195197
(tickedChainSt, ledgerEnv, ledgerSt0, txs) = ledgerTraceBase chainSt block
196198
certs = concatMap (toList . view certsTxBodyL . view bodyTxL)
197199
poolCerts = filter poolCert (certs txs)
198200
poolEnv =
199201
let (LedgerEnv s _ pp _) = ledgerEnv
200-
in PoolEnv s pp
202+
in PoolEnv s pp poolSt0
201203
poolSt0 =
202204
let LedgerState _ (DPState _ poolSt0_) = ledgerSt0
203205
in poolSt0_

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ import Cardano.Ledger.Shelley.Core
2121
import Cardano.Ledger.Slot (SlotNo (..))
2222
import Control.State.Transition.Extended hiding (Assertion)
2323
import Data.Default.Class (def)
24+
import Data.Incremental (ILC (..))
2425
import Lens.Micro
2526
import Test.Cardano.Ledger.Shelley.ConcreteCryptoTypes (C_Crypto)
2627
import qualified Test.Cardano.Ledger.Shelley.Examples.Cast as Cast
@@ -49,8 +50,8 @@ testPoolNetworkID pv poolParams e = do
4950
runShelleyBase $
5051
applySTSTest @(ShelleyPOOL ShelleyTest)
5152
( TRC
52-
( PoolEnv (SlotNo 0) $ emptyPParams & ppProtocolVersionL .~ pv
53-
, def
53+
( PoolEnv (SlotNo 0) (emptyPParams & ppProtocolVersionL .~ pv) def
54+
, totalDiff def
5455
, DCertPool (RegPool poolParams)
5556
)
5657
)

0 commit comments

Comments
 (0)