Skip to content

Commit 1900f29

Browse files
MaximilianAlgehedMaximilianAlgehed
authored
Constrained generators for EPOCH rule (#4740)
1 parent 65ef348 commit 1900f29

File tree

12 files changed

+257
-86
lines changed

12 files changed

+257
-86
lines changed

‎eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -346,10 +346,17 @@ instance
346346
pure $ ProposalsNewActions ps gass
347347

348348
instance
349-
(EraPParams era, Arbitrary (PParamsUpdate era), Arbitrary (PParamsHKD StrictMaybe era)) =>
349+
(EraPParams era, Arbitrary (PParamsHKD StrictMaybe era)) =>
350350
Arbitrary (Proposals era)
351351
where
352352
arbitrary = genProposals (0, 30)
353+
shrink ps =
354+
[ ps'
355+
| gais' <- shrink gais
356+
, let (ps', _) = proposalsRemoveWithDescendants (gais Set.\\ gais') ps
357+
]
358+
where
359+
gais = Set.fromList (toList $ proposalsIds ps)
353360

354361
genProposals ::
355362
forall era.

‎libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs

Lines changed: 18 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
{-# LANGUAGE ScopedTypeVariables #-}
1515
{-# LANGUAGE TypeApplications #-}
1616
{-# LANGUAGE TypeFamilies #-}
17+
{-# LANGUAGE TypeOperators #-}
1718
{-# LANGUAGE UndecidableInstances #-}
1819
{-# LANGUAGE ViewPatterns #-}
1920
{-# OPTIONS_GHC -Wno-orphans #-}
@@ -30,6 +31,8 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
3031
externalFunctions,
3132
) where
3233

34+
import Cardano.Crypto.DSIGN (SignedDSIGN (..), verifySignedDSIGN)
35+
import Cardano.Ledger.Address (RewardAccount)
3336
import Cardano.Ledger.BaseTypes (
3437
EpochInterval (..),
3538
EpochNo (..),
@@ -72,14 +75,18 @@ import Cardano.Ledger.Conway.Rules (
7275
spoAccepted,
7376
spoAcceptedRatio,
7477
)
78+
import Cardano.Ledger.Credential (Credential)
7579
import Cardano.Ledger.DRep (DRep (..))
7680
import Cardano.Ledger.PoolDistr (IndividualPoolStake (..))
7781
import Constrained hiding (inject)
82+
import Data.Either (isRight)
7883
import Data.Foldable (Foldable (..))
7984
import Data.Map.Strict (Map)
8085
import qualified Data.Map.Strict as Map
86+
import Data.Maybe (fromMaybe)
8187
import Data.Ratio (denominator, numerator, (%))
8288
import qualified Data.Sequence.Strict as SSeq
89+
import Data.Set (Set)
8390
import qualified Data.Set as Set
8491
import GHC.Generics (Generic)
8592
import Lens.Micro (Lens', lens, (^.))
@@ -103,29 +110,19 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
103110
signatureFromInteger,
104111
)
105112
import Test.Cardano.Ledger.Constrained.Conway (
106-
EpochExecEnv,
107-
IsConwayUniv,
108-
coerce_,
109-
epochEnvSpec,
110-
epochSignalSpec,
111-
epochStateSpec,
112113
newEpochStateSpec,
113114
)
115+
import Test.Cardano.Ledger.Constrained.Conway.Epoch
116+
import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger
114117
import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams (
115118
committeeMaxTermLength_,
116119
committeeMinSize_,
117120
protocolVersion_,
118121
)
119122

120-
import Cardano.Crypto.DSIGN (SignedDSIGN (..), verifySignedDSIGN)
121123
import Cardano.Crypto.Hash (ByteString, Hash)
122-
import Cardano.Ledger.Address (RewardAccount)
123-
import Cardano.Ledger.Credential (Credential)
124124
import Cardano.Ledger.Crypto (DSIGN, HASH)
125125
import Cardano.Ledger.Keys (KeyRole (..), VKey (..))
126-
import Data.Either (isRight)
127-
import Data.Maybe (fromMaybe)
128-
import Data.Set (Set)
129126
import Test.Cardano.Ledger.Conway.Arbitrary ()
130127
import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var)
131128

@@ -572,15 +569,17 @@ nameGovAction UpdateCommittee {} = "UpdateCommittee"
572569
nameGovAction NewConstitution {} = "NewConstitution"
573570
nameGovAction InfoAction {} = "InfoAction"
574571

575-
instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" ConwayEra where
572+
-- The `fn ~ ConwayFn` thing here is because `ConwayFn` is a type alias
573+
-- and those shouldn't go in instance heads apparently.
574+
instance fn ~ ConwayFn => ExecSpecRule fn "EPOCH" ConwayEra where
576575
type ExecContext fn "EPOCH" ConwayEra = [GovActionState ConwayEra]
577576
type ExecEnvironment fn "EPOCH" ConwayEra = EpochExecEnv ConwayEra
578577

579578
environmentSpec _ = epochEnvSpec
580579

581-
stateSpec _ _ = epochStateSpec
580+
stateSpec _ = epochStateSpec . lit . eeeEpochNo
582581

583-
signalSpec _ _ _ = epochSignalSpec
582+
signalSpec _ env _ = epochSignalSpec (eeeEpochNo env)
584583

585584
runAgdaRule env st sig = unComputationResult_ $ Agda.epochStep env st sig
586585

@@ -589,15 +588,17 @@ instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" ConwayEra where
589588
nameEpoch :: EpochNo -> String
590589
nameEpoch x = show x
591590

592-
instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" ConwayEra where
591+
-- The `fn ~ ConwayFn` thing here is because `ConwayFn` is a type alias
592+
-- and those shouldn't go in instance heads apparently.
593+
instance fn ~ ConwayFn => ExecSpecRule fn "NEWEPOCH" ConwayEra where
593594
type ExecContext fn "NEWEPOCH" ConwayEra = [GovActionState ConwayEra]
594595
type ExecEnvironment fn "NEWEPOCH" ConwayEra = EpochExecEnv ConwayEra
595596

596597
environmentSpec _ = epochEnvSpec
597598

598599
stateSpec _ _ = newEpochStateSpec
599600

600-
signalSpec _ _ _ = epochSignalSpec
601+
signalSpec _ env _ = epochSignalSpec (eeeEpochNo env)
601602

602603
runAgdaRule env st sig = unComputationResult_ $ Agda.newEpochStep env st sig
603604

‎libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Epoch.hs

Lines changed: 84 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,11 @@
11
{-# LANGUAGE DataKinds #-}
22
{-# LANGUAGE DeriveGeneric #-}
33
{-# LANGUAGE FlexibleContexts #-}
4+
{-# LANGUAGE QuasiQuotes #-}
45
{-# LANGUAGE RankNTypes #-}
6+
{-# LANGUAGE RecordWildCards #-}
57
{-# LANGUAGE ScopedTypeVariables #-}
8+
{-# LANGUAGE ViewPatterns #-}
69

710
-- | Specs necessary to generate, environment, state, and signal
811
-- for the EPOCH rule
@@ -11,21 +14,96 @@ module Test.Cardano.Ledger.Constrained.Conway.Epoch where
1114
import Cardano.Ledger.BaseTypes
1215
import Cardano.Ledger.Coin
1316
import Cardano.Ledger.Conway (ConwayEra)
17+
import Cardano.Ledger.Conway.Governance
1418
import Cardano.Ledger.Shelley.API.Types
1519
import Constrained
16-
import Data.Map.Strict
20+
import Data.Foldable
21+
import Data.Map.Strict (Map)
1722
import GHC.Generics (Generic)
23+
import Lens.Micro.Extras
24+
import Test.Cardano.Ledger.Constrained.Conway.Gov
25+
import Test.Cardano.Ledger.Constrained.Conway.Instances
1826

19-
newtype EpochExecEnv era = EpochExecEnv
27+
data EpochExecEnv era = EpochExecEnv
2028
{ eeeStakeDistr :: Map (Credential 'Staking) (CompactForm Coin)
29+
, eeeEpochNo :: EpochNo
2130
}
2231
deriving (Generic, Eq, Show)
2332

2433
epochEnvSpec :: Specification fn (EpochExecEnv ConwayEra)
2534
epochEnvSpec = TrueSpec
2635

27-
epochStateSpec :: Specification fn (EpochState ConwayEra)
28-
epochStateSpec = TrueSpec
36+
epochStateSpec ::
37+
Term ConwayFn EpochNo ->
38+
Specification ConwayFn (EpochState ConwayEra)
39+
epochStateSpec epochNo = constrained $ \es ->
40+
match es $ \_accountState ledgerState _snapShots _nonMyopic ->
41+
match ledgerState $ \utxoState certState ->
42+
match utxoState $ \_utxo _deposited _fees govState _stakeDistr _donation ->
43+
match govState $ \ [var| proposals |] _committee constitution _curPParams _prevPParams _futPParams drepPulsingState ->
44+
[ match constitution $ \_ policy ->
45+
proposals `satisfies` proposalsSpec epochNo policy certState
46+
, caseOn
47+
drepPulsingState
48+
-- DRPulsing
49+
( branch $ \pulser ->
50+
match pulser $ \_size _stakeMap _index _stakeDistr _stakePoolDistr _drepDistr _drepState pulseEpoch _committeeState _enactState pulseProposals _proposalDeposits _poolParams ->
51+
[ assert $ pulseEpoch ==. epochNo
52+
, forAll pulseProposals $ \gas ->
53+
match gas $ \gasId _ _ _ _ _ _ ->
54+
proposalExists gasId proposals
55+
, -- TODO: something is wrong in this case and I haven't figured out what yet
56+
assert False
57+
]
58+
)
59+
-- DRComplete
60+
( branch $ \_snap ratifyState ->
61+
match ratifyState $ \enactState [var| enacted |] expired _delayed ->
62+
[ forAll expired $ \ [var| gasId |] ->
63+
proposalExists gasId proposals
64+
, -- TODO: this isn't enough, we need to ensure it's at most
65+
-- one of each type of action that's being enacted
66+
forAll enacted $ \govact ->
67+
[ reify proposals enactableProposals $ \enactable -> govact `elem_` enactable
68+
, assert $ not_ $ gasId_ govact `member_` expired
69+
]
70+
, -- TODO: this is a hack to get around the todo above!
71+
assert $ sizeOf_ enacted <=. 1
72+
, match enactState $
73+
\_cc _con _cpp _ppp _tr _wth prevGACTIDS ->
74+
reify proposals (toPrevGovActionIds . view pRootsL) (prevGACTIDS ==.)
75+
]
76+
)
77+
]
2978

30-
epochSignalSpec :: Specification fn EpochNo
31-
epochSignalSpec = TrueSpec
79+
proposalExists ::
80+
Term ConwayFn GovActionId ->
81+
Term ConwayFn (Proposals ConwayEra) ->
82+
Pred ConwayFn
83+
proposalExists gasId proposals =
84+
reify proposals proposalsActionsMap $ \actionMap ->
85+
gasId `member_` dom_ actionMap
86+
87+
epochSignalSpec :: EpochNo -> Specification ConwayFn EpochNo
88+
epochSignalSpec curEpoch = constrained $ \e ->
89+
elem_ e (lit [curEpoch, succ curEpoch])
90+
91+
enactableProposals :: Proposals era -> [GovActionState era]
92+
enactableProposals proposals =
93+
[ gact'
94+
| gact <- toList (proposalsActions proposals)
95+
, gact' <- withGovActionParent gact [gact] $
96+
\_ mparent _ ->
97+
case mparent of
98+
SNothing -> [gact]
99+
SJust (GovPurposeId gpid')
100+
| isRoot gpid' proposals -> [gact]
101+
| otherwise -> []
102+
]
103+
104+
isRoot :: GovActionId -> Proposals era -> Bool
105+
isRoot gid (view pRootsL -> GovRelation {..}) =
106+
SJust gid
107+
`elem` [getGID grPParamUpdate, getGID grHardFork, getGID grCommittee, getGID grConstitution]
108+
where
109+
getGID = fmap unGovPurposeId . prRoot

‎libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -47,13 +47,13 @@ govProposalsSpec ::
4747
GovEnv ConwayEra ->
4848
Specification fn (Proposals ConwayEra)
4949
govProposalsSpec GovEnv {geEpoch, gePPolicy, geCertState} =
50-
proposalsSpec (lit geEpoch) (lit gePPolicy) geCertState
50+
proposalsSpec (lit geEpoch) (lit gePPolicy) (lit geCertState)
5151

5252
proposalsSpec ::
5353
IsConwayUniv fn =>
5454
Term fn EpochNo ->
5555
Term fn (StrictMaybe ScriptHash) ->
56-
CertState ConwayEra ->
56+
Term fn (CertState ConwayEra) ->
5757
Specification fn (Proposals ConwayEra)
5858
proposalsSpec geEpoch gePPolicy geCertState =
5959
constrained $ \ [var|props|] ->
@@ -155,11 +155,14 @@ proposalsSpec geEpoch gePPolicy geCertState =
155155
Explain (pure "TreasuryWithdrawal fails") $
156156
Block
157157
[ dependsOn gasOther withdrawMap
158-
, forAll (dom_ withdrawMap) $ \ [var|rewAcnt|] ->
159-
match rewAcnt $ \ [var|network|] [var|credential|] ->
160-
[ network ==. lit Testnet
161-
, credential `member_` lit registeredCredentials
162-
]
158+
, match geCertState $ \_vState _pState [var|dState|] ->
159+
match dState $ \ [var|rewardMap|] _ _ _ ->
160+
reify rewardMap (Map.keysSet . umElems) $ \ [var|registeredCredentials|] ->
161+
forAll (dom_ withdrawMap) $ \ [var|rewAcnt|] ->
162+
match rewAcnt $ \ [var|network|] [var|credential|] ->
163+
[ network ==. lit Testnet
164+
, credential `member_` registeredCredentials
165+
]
163166
, assert $ policy ==. gePPolicy
164167
]
165168
)
@@ -173,7 +176,6 @@ proposalsSpec geEpoch gePPolicy geCertState =
173176
where
174177
treeGenHint = (Just 2, 10)
175178
listSizeHint = 5
176-
registeredCredentials = Map.keysSet $ umElems $ dsUnified $ certDState geCertState
177179

178180
allGASInTree ::
179181
(IsConwayUniv fn, IsPred p fn) =>
@@ -279,6 +281,7 @@ withPrevActId gas k =
279281
-- InfoAction
280282
(branch $ \_ -> True)
281283
]
284+
282285
onHardFork ::
283286
(IsConwayUniv fn, IsPred p fn) =>
284287
Term fn (GovActionState ConwayEra) ->

0 commit comments

Comments
 (0)