Skip to content

Commit 3ae9159

Browse files
MaximilianAlgehedMaximilianAlgehed
committed
constrained-generators: Get rid of a bunch of uses of dom_ 
1 parent c2df298 commit 3ae9159

File tree

12 files changed

+35
-26
lines changed

12 files changed

+35
-26
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,7 @@ conwayCertExecContextSpec univ wdrlsize = constrained $ \ [var|ccec|] ->
162162
match ccec $ \ [var|withdrawals|] [var|deposits|] _ [var|delegatees|] ->
163163
[ assert $
164164
[ witness univ (dom_ withdrawals)
165-
, assert $ sizeOf_ (dom_ withdrawals) <=. (lit wdrlsize)
165+
, assert $ sizeOf_ withdrawals <=. (lit wdrlsize)
166166
]
167167
, forAll (dom_ deposits) $ \dp -> satisfies dp (witnessDepositPurpose univ)
168168
, satisfies delegatees (delegateeSpec @era univ)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,7 @@ genesisDelegCertSpec ds =
129129
GenDelegs genDelegs = dsGenDelegs ds
130130
in constrained $ \ [var|gdc|] ->
131131
match gdc $ \ [var|gkh|] [var|vkh|] [var|hashVrf|] ->
132-
[ assert $ member_ gkh (dom_ (lit genDelegs))
132+
[ assert $ mapMember_ gkh (lit genDelegs)
133133
, reify gkh coldKeyHashes (\ [var|coldkeys|] -> member_ vkh coldkeys)
134134
, reify gkh vrfKeyHashes (\ [var|vrfkeys|] -> member_ hashVrf vrfkeys)
135135
]

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@ bootstrapDStateSpec univ delegatees withdrawals =
9595
, reify rdMap id $ \ [var|rdmp|] ->
9696
assertExplain (pure "dom sPoolMap is a subset of dom rdMap") $ dom_ sPoolMap `subset_` dom_ rdmp
9797
, -- ptrMap
98-
assertExplain (pure "dom ptrMap is empty") $ dom_ ptrMap ==. mempty
98+
assertExplain (pure "ptrMap is empty") $ ptrMap ==. lit mempty
9999
]
100100
]
101101

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ rewDepMapSpec univ wdrl =
6363
in constrained $ \ [var|rdmap|] ->
6464
[ -- can't be bigger than the witness set (n keys + n scripts)
6565
-- must also have enough slack to accomodate the credentials in wdrl (m)
66-
assert $ sizeOf_ (dom_ rdmap) <=. lit maxRewDepSize -- If this is too large
66+
assert $ sizeOf_ rdmap <=. lit maxRewDepSize -- If this is too large
6767
, assert $ subset_ (lit (wdrlCredentials wdrl)) (dom_ rdmap) -- it is hard to satisfy this
6868
, forAll' rdmap $ \ [var|cred|] [var| rdpair|] ->
6969
[ witness univ cred
@@ -88,7 +88,7 @@ rewDepMapSpec2 univ wdrl =
8888
in constrained $ \ [var|rdmap|] ->
8989
[ -- size of rdmap, can't be bigger than the witness set (n keys + n scripts)
9090
-- must also have enough slack to accomodate the credentials in wdrl (m)
91-
assert $ sizeOf_ (dom_ rdmap) <=. lit maxRewDepSize
91+
assert $ sizeOf_ (rdmap) <=. lit maxRewDepSize
9292
, assertExplain (pure "some rewards (not in withdrawals) are zero") $
9393
forAll rdmap $
9494
\ [var| keycoinpair |] -> match keycoinpair $ \cred [var| rdpair |] ->
@@ -99,7 +99,7 @@ rewDepMapSpec2 univ wdrl =
9999
]
100100
, forAll (lit withdrawalPairs) $ \ [var| pair |] ->
101101
match pair $ \ [var| wcred |] [var| coin |] ->
102-
[ assertExplain (pure "withdrawalKeys are a subset of the rdMap") $ member_ wcred (dom_ rdmap)
102+
[ assertExplain (pure "withdrawalKeys are a subset of the rdMap") $ mapMember_ wcred rdmap
103103
, -- Force the reward in the RDPair to the withdrawal amount.
104104
onJust (lookup_ wcred rdmap) $ \ [var|rdpair|] ->
105105
match rdpair $ \rew _deposit -> assert $ rew ==. coin
@@ -151,7 +151,7 @@ dStateSpec univ wdrls = constrained $ \ [var| dstate |] ->
151151
reify rdMap id $ \ [var|rdmp|] ->
152152
assertExplain (pure "dom sPoolMap is a subset of dom rdMap") $ dom_ sPoolMap `subset_` dom_ rdmp
153153
, -- ptrMapo
154-
assertExplain (pure "dom ptrMap is empty") $ dom_ ptrMap ==. mempty
154+
assertExplain (pure "ptrMap is empty") $ ptrMap ==. lit mempty
155155
]
156156
]
157157

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ proposalExists ::
9090
Pred
9191
proposalExists gasId proposals =
9292
reify proposals proposalsActionsMap $ \ [var|actionMap|] ->
93-
gasId `member_` dom_ actionMap
93+
gasId `mapMember_` actionMap
9494

9595
epochSignalSpec :: EpochNo -> Specification EpochNo
9696
epochSignalSpec curEpoch = constrained $ \e ->

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ vStateSpec ::
4141
vStateSpec univ delegatees = constrained $ \ [var|vstate|] ->
4242
match vstate $ \ [var|dreps|] [var|committeestate|] [var|_numdormant|] ->
4343
[ match committeestate $ \ [var|committeemap|] -> witness univ (dom_ committeemap)
44-
, assert $ dom_ dreps ==. (lit delegatees) -- TODO, there are missing constraints about the (rng_ dreps)
44+
, assert $ dom_ dreps ==. lit delegatees -- TODO, there are missing constraints about the (rng_ dreps)
4545
, forAll dreps $ \ [var|pair|] ->
4646
match pair $ \ [var|drep|] [var|drepstate|] ->
4747
[ dependsOn drepstate drep
@@ -77,7 +77,7 @@ govCertSpec univ ConwayGovCertEnv {..} certState =
7777
-- that each branch is choosen with similar frequency
7878
-- ConwayRegDRep
7979
( branchW 1 $ \ [var|keyreg|] [var|coinreg|] _ ->
80-
[ assert $ not_ $ member_ keyreg (dom_ (lit deposits))
80+
[ assert $ not_ $ mapMember_ keyreg (lit deposits)
8181
, assert $ coinreg ==. lit (cgcePParams ^. ppDRepDepositL)
8282
, witness univ keyreg
8383
]
@@ -139,7 +139,7 @@ govCertEnvSpec univ =
139139
match gce $ \ [var|pp|] _ [var|committee|] [var|proposalmap|] ->
140140
[ satisfies pp pparamsSpec
141141
, unsafeExists (\x -> [satisfies x (committeeWitness univ), assert $ committee ==. cSJust_ x])
142-
, assert $ sizeOf_ (dom_ proposalmap) <=. lit 5
143-
, assert $ sizeOf_ (dom_ proposalmap) >=. lit 1
142+
, assert $ sizeOf_ (proposalmap) <=. lit 5
143+
, assert $ sizeOf_ (proposalmap) >=. lit 1
144144
, forAll (rng_ proposalmap) $ \x -> satisfies x (govActionStateWitness univ)
145145
]

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -199,7 +199,7 @@ goodDrep univ =
199199
, satisfies (snd_ pair) (hasSize (rangeSize 1 5))
200200
, forAll (snd_ pair) (`satisfies` (witCredSpec @era univ))
201201
]
202-
, satisfies (dom_ dRepMap) (hasSize (rangeSize 6 10))
202+
, satisfies dRepMap (hasSize (rangeSize 6 10))
203203
]
204204

205205
-- ========================================================================
@@ -301,7 +301,7 @@ dstateSpec univ acct poolreg = constrained $ \ [var| ds |] ->
301301
[ genHint 5 sPoolMap
302302
, assertExplain (pure "dom sPoolMap is a subset of dom rdMap") $ dom_ sPoolMap `subset_` rdcreds
303303
, assertExplain (pure "The delegations delegate to actual pools") $
304-
forAll (rng_ sPoolMap) (\ [var|keyhash|] -> member_ keyhash (dom_ poolreg))
304+
forAll (rng_ sPoolMap) (\ [var|keyhash|] -> mapMember_ keyhash poolreg)
305305
]
306306
, -- futureGenDelegs and genDelegs and irewards can be solved in any order
307307
satisfies irewards (irewardSpec @era univ acct)
@@ -344,9 +344,9 @@ pstateSpec univ currepoch = constrained $ \ [var|pState|] ->
344344
dom_ stakePoolParams `disjoint_` dom_ futureStakePoolParams
345345
, assertExplain (pure "retiring after current epoch") $
346346
forAll (rng_ retiring) (\ [var|epoch|] -> currepoch <=. epoch)
347-
, assert $ sizeOf_ (dom_ futureStakePoolParams) <=. 4
348-
, assert $ 3 <=. sizeOf_ (dom_ stakePoolParams)
349-
, assert $ sizeOf_ (dom_ stakePoolParams) <=. 8
347+
, assert $ sizeOf_ (futureStakePoolParams) <=. 4
348+
, assert $ 3 <=. sizeOf_ stakePoolParams
349+
, assert $ sizeOf_ stakePoolParams <=. 8
350350
]
351351

352352
accountStateSpec :: Specification ChainAccountState

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -184,7 +184,7 @@ delegatedStakeReference delegs =
184184
constrained $ \ [var|ref|] ->
185185
caseOn
186186
ref
187-
(branchW 9 $ \ [var|base|] -> member_ base (dom_ delegs))
187+
(branchW 9 $ \ [var|base|] -> mapMember_ base delegs)
188188
(branchW 1 $ \_ptr -> True)
189189
(branchW 1 $ \_null -> True) -- just an occaisional NullRef
190190

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -856,11 +856,11 @@ govActionStateWitness univ = ExplainSpec ["Witnessing GovActionState"] $
856856
match govactstate $
857857
\_gaid [var|comVotemap|] [var|drepVotemap|] [var|poolVotemap|] [var|proposalProc|] _proposed _expires ->
858858
[ witness univ (dom_ comVotemap)
859-
, assert $ sizeOf_ (dom_ comVotemap) ==. lit 3
859+
, assert $ sizeOf_ comVotemap ==. lit 3
860860
, witness univ (dom_ drepVotemap)
861-
, assert $ sizeOf_ (dom_ drepVotemap) ==. lit 2
861+
, assert $ sizeOf_ drepVotemap ==. lit 2
862862
, witness univ (dom_ poolVotemap)
863-
, assert $ sizeOf_ (dom_ poolVotemap) ==. lit 2
863+
, assert $ sizeOf_ poolVotemap ==. lit 2
864864
, satisfies proposalProc (proposalProcedureWitness univ)
865865
]
866866

@@ -904,7 +904,7 @@ committeeWitness ::
904904
committeeWitness univ =
905905
constrained $ \ [var|committee|] ->
906906
match committee $ \ [var|epochMap|] _threshold ->
907-
[witness univ (dom_ epochMap), assert $ sizeOf_ (dom_ epochMap) ==. lit 3]
907+
[witness univ (dom_ epochMap), assert $ sizeOf_ epochMap ==. lit 3]
908908

909909
go9 :: IO ()
910910
go9 = do

‎libs/constrained-generators/src/Constrained/API.hs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,7 @@ module Constrained.API (
136136
dom_,
137137
rng_,
138138
lookup_,
139+
mapMember_,
139140
fstSpec,
140141
sndSpec,
141142
var,
@@ -198,6 +199,7 @@ import Constrained.Spec.Map (
198199
dom_,
199200
fstSpec,
200201
lookup_,
202+
mapMember_,
201203
rng_,
202204
sndSpec,
203205
)

0 commit comments

Comments
 (0)