Skip to content

Commit f22cd52

Browse files
authored
Refactor the constrained generators to get rid of the Fn stuff (#4921)
* Started refactoring constrained generators to get rid of the Fn stuff. Broke up src/Constrained/Base into several files src/Constrained/Experiment/Genrics src/Constrained/Experiment/Base defines Specification, HasSpec, Term, Pred, Generic default methods for HasSpec replaces the FunctionLike and Functions classes with Syntax, Semantics and Logic classes src/Constrained/Experiment/Syntax src/Constrained/Experiment/Conformance conformance functions, Monoid and Semigroup instances for Specification src/Constrained/Experiment/NumSpec OrdLike and NumLike src/Constrained/Experiment/TheKnot Ties the mutually recursive objects genfromSpecT, simplifySpec, HasSpec Integer, HasSpec Sum, HasSpec Prod, HasSpec Bool This mutual recursion is why the old Base.hs was so large 6400 lines Added the Constrained/Experiment/Specs directory with files that define HasSpec instances for List, Fold, Set, Map, Tree Translated all the examples Constrained/Experiment/Examples Translated all the tests Constrained/Experiment/Tests * Applied the changes to the module constrained-generators * Applied the changes to the cardano-ledger-test module * Applied the changes to the cardano-ledger-conformance module. * Finally fixed the type of mapTypeSpec * final self review * Remove references to Proof and PrettyCore * Address comments and fix conflicts * added Manual.md
1 parent 655b552 commit f22cd52

File tree

82 files changed

+11249
-9281
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

82 files changed

+11249
-9281
lines changed

docs/constrained-generators/manual.md

Lines changed: 448 additions & 0 deletions
Large diffs are not rendered by default.

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

Lines changed: 36 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ import Cardano.Ledger.State (
7979
CommitteeState (..),
8080
IndividualPoolStake (..),
8181
)
82-
import Constrained hiding (inject)
82+
import Constrained.API
8383
import Data.Either (isRight)
8484
import Data.Foldable (Foldable (..))
8585
import Data.Map.Strict (Map)
@@ -89,6 +89,7 @@ import Data.Ratio (denominator, numerator, (%))
8989
import qualified Data.Sequence.Strict as SSeq
9090
import Data.Set (Set)
9191
import qualified Data.Set as Set
92+
import Data.Typeable (Typeable)
9293
import GHC.Generics (Generic)
9394
import Lens.Micro (Lens', lens, (^.))
9495
import qualified Lib as Agda
@@ -149,25 +150,25 @@ data ConwayCertExecContext era
149150
}
150151
deriving (Generic, Eq, Show)
151152

152-
instance HasSimpleRep (ConwayCertExecContext era)
153-
instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayCertExecContext era)
153+
instance Typeable era => HasSimpleRep (ConwayCertExecContext era)
154+
instance Era era => HasSpec (ConwayCertExecContext era)
154155

155156
-- No particular constraints, other than witnessing
156157
conwayCertExecContextSpec ::
157-
forall fn era.
158-
(Reflect era, IsConwayUniv fn) =>
159-
WitUniv era -> Integer -> Specification fn (ConwayCertExecContext era)
158+
forall era.
159+
Era era =>
160+
WitUniv era -> Integer -> Specification (ConwayCertExecContext era)
160161
conwayCertExecContextSpec univ wdrlsize = constrained $ \ [var|ccec|] ->
161162
match ccec $ \ [var|withdrawals|] [var|deposits|] _ [var|delegatees|] ->
162163
[ assert $
163164
[ witness univ (dom_ withdrawals)
164165
, assert $ sizeOf_ (dom_ withdrawals) <=. (lit wdrlsize)
165166
]
166167
, forAll (dom_ deposits) $ \dp -> satisfies dp (witnessDepositPurpose univ)
167-
, satisfies delegatees (delegateeSpec @fn @era univ)
168+
, satisfies delegatees (delegateeSpec @era univ)
168169
]
169170

170-
instance Reflect era => Arbitrary (ConwayCertExecContext era) where
171+
instance Era era => Arbitrary (ConwayCertExecContext era) where
171172
arbitrary =
172173
ConwayCertExecContext
173174
<$> arbitrary
@@ -259,23 +260,19 @@ instance
259260
where
260261
inject = crecGovActionMap
261262

262-
instance HasSimpleRep (ConwayRatifyExecContext era)
263+
instance Typeable era => HasSimpleRep (ConwayRatifyExecContext era)
263264
instance
264-
( IsConwayUniv fn
265-
, EraPParams era
266-
, HasSpec fn (GovActionState era)
265+
( EraPParams era
266+
, HasSpec (GovActionState era)
267267
) =>
268-
HasSpec fn (ConwayRatifyExecContext era)
268+
HasSpec (ConwayRatifyExecContext era)
269269

270270
instance EraPParams era => NFData (ConwayRatifyExecContext era)
271271

272272
ratifyEnvSpec ::
273-
( IsConwayUniv fn
274-
, HasSpec fn (RatifyEnv ConwayEra)
275-
, HasSpec fn (SimpleRep (RatifyEnv ConwayEra))
276-
) =>
273+
HasSpec (SimpleRep (RatifyEnv ConwayEra)) =>
277274
ConwayRatifyExecContext ConwayEra ->
278-
Specification fn (RatifyEnv ConwayEra)
275+
Specification (RatifyEnv ConwayEra)
279276
ratifyEnvSpec ConwayRatifyExecContext {crecGovActionMap} =
280277
constrained' $ \_ poolDistr drepDistr drepState _ committeeState _ _ ->
281278
[ -- Bias the generator towards generating DReps that have stake and are registered
@@ -351,10 +348,9 @@ ratifyEnvSpec ConwayRatifyExecContext {crecGovActionMap} =
351348
crecGovActionMap
352349

353350
ratifyStateSpec ::
354-
IsConwayUniv fn =>
355351
ConwayRatifyExecContext ConwayEra ->
356352
RatifyEnv ConwayEra ->
357-
Specification fn (RatifyState ConwayEra)
353+
Specification (RatifyState ConwayEra)
358354
ratifyStateSpec _ RatifyEnv {..} =
359355
constrained' $ \ens enacted expired _ ->
360356
mconcat
@@ -387,15 +383,14 @@ ratifyStateSpec _ RatifyEnv {..} =
387383
let CommitteeState m = reCommitteeState
388384
in Map.keysSet m
389385
-- Bootstrap is not in the spec
390-
disableBootstrap :: IsConwayUniv fn => Term fn (PParams ConwayEra) -> Pred fn
386+
disableBootstrap :: Term (PParams ConwayEra) -> Pred
391387
disableBootstrap pp = match pp $ \simplepp ->
392388
match (protocolVersion_ simplepp) $ \major _ ->
393389
assert $ not_ (major ==. lit (natVersion @9))
394390

395391
preferSmallerCCMinSizeValues ::
396-
IsConwayUniv fn =>
397-
Term fn (PParams ConwayEra) ->
398-
Pred fn
392+
Term (PParams ConwayEra) ->
393+
Pred
399394
preferSmallerCCMinSizeValues pp = match pp $ \simplepp ->
400395
satisfies (committeeMinSize_ simplepp) $
401396
chooseSpec
@@ -405,18 +400,17 @@ ratifyStateSpec _ RatifyEnv {..} =
405400
committeeSize = lit . fromIntegral . Set.size $ ccColdKeys
406401

407402
ratifySignalSpec ::
408-
IsConwayUniv fn =>
409403
ConwayRatifyExecContext ConwayEra ->
410-
Specification fn (RatifySignal ConwayEra)
404+
Specification (RatifySignal ConwayEra)
411405
ratifySignalSpec ConwayRatifyExecContext {crecGovActionMap} =
412406
constrained $ \sig ->
413407
match sig $ \gasS ->
414408
match gasS $ \gasL ->
415409
forAll gasL $ \gas ->
416410
gas `elem_` lit crecGovActionMap
417411

418-
instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" ConwayEra where
419-
type ExecContext fn "RATIFY" ConwayEra = ConwayRatifyExecContext ConwayEra
412+
instance ExecSpecRule "RATIFY" ConwayEra where
413+
type ExecContext "RATIFY" ConwayEra = ConwayRatifyExecContext ConwayEra
420414

421415
genExecContext = arbitrary
422416

@@ -471,7 +465,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" ConwayEra where
471465

472466
testConformance ctx env st@(RatifyState {rsEnactState}) sig@(RatifySignal actions) =
473467
labelRatios $
474-
defaultTestConformance @fn @ConwayEra @"RATIFY" ctx env st sig
468+
defaultTestConformance @ConwayEra @"RATIFY" ctx env st sig
475469
where
476470
bucket r
477471
| r == 0 % 1 = "=0%"
@@ -531,11 +525,10 @@ instance Era era => EncCBOR (ConwayEnactExecContext era) where
531525
encCBOR (ConwayEnactExecContext x) = encCBOR x
532526

533527
enactSignalSpec ::
534-
IsConwayUniv fn =>
535528
ConwayEnactExecContext ConwayEra ->
536529
ConwayExecEnactEnv ConwayEra ->
537530
EnactState ConwayEra ->
538-
Specification fn (EnactSignal ConwayEra)
531+
Specification (EnactSignal ConwayEra)
539532
enactSignalSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} EnactState {..} =
540533
constrained' $ \gid action ->
541534
[ assert $ gid ==. lit ceeeGid
@@ -563,22 +556,21 @@ enactSignalSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} EnactState {
563556
]
564557

565558
enactStateSpec ::
566-
IsConwayUniv fn =>
567559
ConwayEnactExecContext ConwayEra ->
568560
ConwayExecEnactEnv ConwayEra ->
569-
Specification fn (EnactState ConwayEra)
561+
Specification (EnactState ConwayEra)
570562
enactStateSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} =
571563
constrained' $ \_ _ curPParams _ treasury wdrls _ ->
572564
[ match curPParams $ \simplepp -> committeeMaxTermLength_ simplepp ==. lit ceecMaxTerm
573565
, assert $ sum_ (rng_ wdrls) <=. treasury
574566
, assert $ treasury ==. lit ceeeTreasury
575567
]
576568

577-
instance IsConwayUniv fn => ExecSpecRule fn "ENACT" ConwayEra where
578-
type ExecContext fn "ENACT" ConwayEra = ConwayEnactExecContext ConwayEra
579-
type ExecEnvironment fn "ENACT" ConwayEra = ConwayExecEnactEnv ConwayEra
580-
type ExecState fn "ENACT" ConwayEra = EnactState ConwayEra
581-
type ExecSignal fn "ENACT" ConwayEra = EnactSignal ConwayEra
569+
instance ExecSpecRule "ENACT" ConwayEra where
570+
type ExecContext "ENACT" ConwayEra = ConwayEnactExecContext ConwayEra
571+
type ExecEnvironment "ENACT" ConwayEra = ConwayExecEnactEnv ConwayEra
572+
type ExecState "ENACT" ConwayEra = EnactState ConwayEra
573+
type ExecSignal "ENACT" ConwayEra = EnactSignal ConwayEra
582574

583575
environmentSpec _ = TrueSpec
584576
stateSpec = enactStateSpec
@@ -602,11 +594,9 @@ nameGovAction UpdateCommittee {} = "UpdateCommittee"
602594
nameGovAction NewConstitution {} = "NewConstitution"
603595
nameGovAction InfoAction {} = "InfoAction"
604596

605-
-- The `fn ~ ConwayFn` thing here is because `ConwayFn` is a type alias
606-
-- and those shouldn't go in instance heads apparently.
607-
instance fn ~ ConwayFn => ExecSpecRule fn "EPOCH" ConwayEra where
608-
type ExecContext fn "EPOCH" ConwayEra = [GovActionState ConwayEra]
609-
type ExecEnvironment fn "EPOCH" ConwayEra = EpochExecEnv ConwayEra
597+
instance ExecSpecRule "EPOCH" ConwayEra where
598+
type ExecContext "EPOCH" ConwayEra = [GovActionState ConwayEra]
599+
type ExecEnvironment "EPOCH" ConwayEra = EpochExecEnv ConwayEra
610600

611601
environmentSpec _ = epochEnvSpec
612602

@@ -621,11 +611,9 @@ instance fn ~ ConwayFn => ExecSpecRule fn "EPOCH" ConwayEra where
621611
nameEpoch :: EpochNo -> String
622612
nameEpoch x = show x
623613

624-
-- The `fn ~ ConwayFn` thing here is because `ConwayFn` is a type alias
625-
-- and those shouldn't go in instance heads apparently.
626-
instance fn ~ ConwayFn => ExecSpecRule fn "NEWEPOCH" ConwayEra where
627-
type ExecContext fn "NEWEPOCH" ConwayEra = [GovActionState ConwayEra]
628-
type ExecEnvironment fn "NEWEPOCH" ConwayEra = EpochExecEnv ConwayEra
614+
instance ExecSpecRule "NEWEPOCH" ConwayEra where
615+
type ExecContext "NEWEPOCH" ConwayEra = [GovActionState ConwayEra]
616+
type ExecEnvironment "NEWEPOCH" ConwayEra = EpochExecEnv ConwayEra
629617

630618
environmentSpec _ = epochEnvSpec
631619

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

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert (nameTxCert) whe
1515

1616
import Cardano.Ledger.Conway
1717
import Cardano.Ledger.Conway.TxCert (ConwayTxCert (..))
18-
import Constrained
18+
import Constrained.API
1919
import qualified Lib as Agda
2020
import Test.Cardano.Ledger.Conformance
2121
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
@@ -25,23 +25,20 @@ import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool (namePoolCert)
2525
import Test.Cardano.Ledger.Constrained.Conway
2626
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
2727

28-
instance
29-
IsConwayUniv fn =>
30-
ExecSpecRule fn "CERT" ConwayEra
31-
where
32-
type ExecContext fn "CERT" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
28+
instance ExecSpecRule "CERT" ConwayEra where
29+
type ExecContext "CERT" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
3330

3431
genExecContext = do
3532
univ <- genWitUniv @ConwayEra 300
36-
ccec <- genFromSpec @ConwayFn (conwayCertExecContextSpec univ 5)
33+
ccec <- genFromSpec (conwayCertExecContextSpec univ 5)
3734
pure (univ, ccec)
3835

39-
environmentSpec (univ, _) = certEnvSpec @fn @ConwayEra univ
36+
environmentSpec (univ, _) = certEnvSpec @ConwayEra univ
4037

4138
stateSpec (univ, ccec) _ =
42-
certStateSpec @ConwayEra @fn univ (ccecDelegatees ccec) (ccecWithdrawals ccec)
39+
certStateSpec @ConwayEra univ (ccecDelegatees ccec) (ccecWithdrawals ccec)
4340

44-
signalSpec (univ, _) env state = conwayTxCertSpec @fn @ConwayEra univ env state
41+
signalSpec (univ, _) env state = conwayTxCertSpec @ConwayEra univ env state
4542

4643
runAgdaRule env st sig =
4744
unComputationResult $

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

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs (nameCerts) whe
1313
import Cardano.Ledger.Address (RewardAccount (..))
1414
import Cardano.Ledger.Conway
1515
import Cardano.Ledger.Conway.TxCert
16-
import Constrained
16+
import Constrained.API
1717
import Data.Bifunctor (first)
1818
import qualified Data.Map.Strict as Map
1919
import Data.Sequence (Seq)
@@ -26,29 +26,26 @@ import Test.Cardano.Ledger.Constrained.Conway
2626
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
2727
import Test.Cardano.Ledger.Imp.Common hiding (context)
2828

29-
instance
30-
IsConwayUniv fn =>
31-
ExecSpecRule fn "CERTS" ConwayEra
32-
where
33-
type ExecContext fn "CERTS" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
29+
instance ExecSpecRule "CERTS" ConwayEra where
30+
type ExecContext "CERTS" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
3431

3532
genExecContext = do
3633
univ <- genWitUniv @ConwayEra 300
37-
ccec <- genFromSpec @fn (conwayCertExecContextSpec univ 5)
34+
ccec <- genFromSpec (conwayCertExecContextSpec univ 5)
3835
pure (univ, ccec)
3936

4037
environmentSpec _ = certsEnvSpec
4138

4239
stateSpec (univ, context) _ =
4340
constrained $ \x ->
4441
match x $ \vstate pstate dstate ->
45-
[ satisfies vstate (vStateSpec @_ @ConwayEra univ (ccecDelegatees context))
46-
, satisfies pstate (pStateSpec @_ @ConwayEra univ)
42+
[ satisfies vstate (vStateSpec @ConwayEra univ (ccecDelegatees context))
43+
, satisfies pstate (pStateSpec @ConwayEra univ)
4744
, -- temporary workaround because Spec does some extra tests, that the implementation does not, in the bootstrap phase.
4845
satisfies dstate (bootstrapDStateSpec univ (ccecDelegatees context) (ccecWithdrawals context))
4946
]
5047

51-
signalSpec (univ, _) env state = txCertsSpec @ConwayEra @fn univ env state
48+
signalSpec (univ, _) env state = txCertsSpec @ConwayEra univ env state
5249

5350
runAgdaRule env st sig = unComputationResult $ Agda.certsStep env st sig
5451
classOf = Just . nameCerts
@@ -57,10 +54,10 @@ instance
5754
-- The results of runConformance are Agda types, the `ctx` is a Haskell type, we extract and translate the Withdrawal keys.
5855
specWithdrawalCredSet <-
5956
translateWithContext () (Map.keysSet (Map.mapKeys raCredential (ccecWithdrawals ccec)))
60-
(implResTest, agdaResTest, _) <- runConformance @"CERTS" @fn @ConwayEra ctx env st sig
57+
(implResTest, agdaResTest, _) <- runConformance @"CERTS" @ConwayEra ctx env st sig
6158
case (implResTest, agdaResTest) of
6259
(Right haskell, Right spec) ->
63-
checkConformance @"CERTS" @ConwayEra @fn
60+
checkConformance @"CERTS" @ConwayEra
6461
ctx
6562
env
6663
st
@@ -77,7 +74,7 @@ instance
7774
zeroRewards (Agda.MkHSMap pairs) =
7875
Agda.MkHSMap (map (\(c, r) -> if c `Set.member` credsSet then (c, 0) else (c, r)) pairs)
7976
_ ->
80-
checkConformance @"CERTS" @ConwayEra @fn
77+
checkConformance @"CERTS" @ConwayEra
8178
ctx
8279
env
8380
st

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ import Cardano.Ledger.Conway
1414
import Cardano.Ledger.Conway.TxCert (ConwayDelegCert (..))
1515
import Cardano.Ledger.Credential (Credential)
1616
import Cardano.Ledger.Keys (KeyRole (..))
17-
import Constrained
17+
import Constrained.API
1818
import Data.Bifunctor (second)
1919
import Data.Set (Set)
2020
import qualified Lib as Agda
@@ -37,12 +37,12 @@ instance
3737
where
3838
inject (_, x) = ccecDelegatees x
3939

40-
instance IsConwayUniv fn => ExecSpecRule fn "DELEG" ConwayEra where
41-
type ExecContext fn "DELEG" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
40+
instance ExecSpecRule "DELEG" ConwayEra where
41+
type ExecContext "DELEG" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
4242

4343
genExecContext = do
4444
univ <- genWitUniv @ConwayEra 300
45-
ccec <- genFromSpec @ConwayFn (conwayCertExecContextSpec univ 5)
45+
ccec <- genFromSpec (conwayCertExecContextSpec univ 5)
4646
pure (univ, ccec)
4747

4848
environmentSpec _ = delegEnvSpec

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -24,12 +24,10 @@ import Test.Cardano.Ledger.Conway.Arbitrary ()
2424
import Test.Cardano.Ledger.Imp.Common
2525

2626
instance
27-
( NFData (SpecRep (ConwayGovPredFailure ConwayEra))
28-
, IsConwayUniv fn
29-
) =>
30-
ExecSpecRule fn "GOV" ConwayEra
27+
NFData (SpecRep (ConwayGovPredFailure ConwayEra)) =>
28+
ExecSpecRule "GOV" ConwayEra
3129
where
32-
type ExecContext fn "GOV" ConwayEra = EnactState ConwayEra
30+
type ExecContext "GOV" ConwayEra = EnactState ConwayEra
3331

3432
environmentSpec _ = govEnvSpec
3533

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

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ import Cardano.Ledger.Coin (Coin)
1616
import Cardano.Ledger.Conway
1717
import Cardano.Ledger.Conway.Governance (VotingProcedures)
1818
import Cardano.Ledger.Conway.TxCert
19-
import Constrained
19+
import Constrained.API
2020
import Data.Bifunctor (Bifunctor (..))
2121
import Data.Map.Strict (Map)
2222
import qualified Lib as Agda
@@ -34,21 +34,18 @@ instance Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (Map Reward
3434
instance Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (VotingProcedures ConwayEra) where
3535
inject (_, x) = ccecVotes x
3636

37-
instance
38-
IsConwayUniv fn =>
39-
ExecSpecRule fn "GOVCERT" ConwayEra
40-
where
41-
type ExecContext fn "GOVCERT" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
37+
instance ExecSpecRule "GOVCERT" ConwayEra where
38+
type ExecContext "GOVCERT" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
4239

4340
genExecContext = do
4441
univ <- genWitUniv @ConwayEra 300
45-
ccec <- genFromSpec @ConwayFn (conwayCertExecContextSpec univ 5)
42+
ccec <- genFromSpec (conwayCertExecContextSpec univ 5)
4643
pure (univ, ccec)
4744

4845
environmentSpec (univ, _) = govCertEnvSpec univ
4946

5047
stateSpec (univ, ccec) _env =
51-
certStateSpec @ConwayEra @fn univ (ccecDelegatees ccec) (ccecWithdrawals ccec)
48+
certStateSpec @ConwayEra univ (ccecDelegatees ccec) (ccecWithdrawals ccec)
5249

5350
signalSpec (univ, _) = govCertSpec univ
5451

0 commit comments

Comments
 (0)