Skip to content

Commit deb0945

Browse files
constrained-generators: Improve the public API and separate "use API"
from "extend API"
1 parent 6fdc703 commit deb0945

File tree

37 files changed

+396
-493
lines changed

37 files changed

+396
-493
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -395,7 +395,7 @@ ratifyStateSpec _ RatifyEnv {..} =
395395
preferSmallerCCMinSizeValues pp = match pp $ \simplepp ->
396396
satisfies (committeeMinSize_ simplepp) $
397397
chooseSpec
398-
(1, TrueSpec)
398+
(1, trueSpec)
399399
(1, constrained (<=. committeeSize))
400400
where
401401
committeeSize = lit . fromIntegral . Set.size $ ccColdKeys
@@ -573,7 +573,7 @@ instance ExecSpecRule "ENACT" ConwayEra where
573573
type ExecState "ENACT" ConwayEra = EnactState ConwayEra
574574
type ExecSignal "ENACT" ConwayEra = EnactSignal ConwayEra
575575

576-
environmentSpec _ = TrueSpec
576+
environmentSpec _ = trueSpec
577577
stateSpec = enactStateSpec
578578
signalSpec = enactSignalSpec
579579
runAgdaRule env st sig = unComputationResult $ Agda.enactStep env st sig

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Core.hs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,13 +29,12 @@ module Test.Cardano.Ledger.Conformance.SpecTranslate.Core (
2929
) where
3030

3131
import Cardano.Ledger.BaseTypes (Inject (..))
32-
import Constrained.Base ()
32+
import Constrained.API
3333
import Control.DeepSeq (NFData)
3434
import Control.Monad.Except (ExceptT, MonadError (..), runExceptT)
3535
import Control.Monad.Reader (MonadReader (..), Reader, asks, runReader)
3636
import Data.Foldable (Foldable (..))
3737
import Data.Kind (Type)
38-
import Data.List.NonEmpty (NonEmpty)
3938
import Data.Text (Text)
4039
import qualified Data.Text as T
4140
import Data.Void (Void)

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
@@ -31,7 +31,7 @@ data EpochExecEnv era = EpochExecEnv
3131
deriving (Generic, Eq, Show)
3232

3333
epochEnvSpec :: Specification (EpochExecEnv ConwayEra)
34-
epochEnvSpec = TrueSpec
34+
epochEnvSpec = trueSpec
3535

3636
epochStateSpec ::
3737
Term EpochNo ->

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,6 @@ import Cardano.Ledger.Conway.Rules
2121
import Cardano.Ledger.Conway.State
2222
import Cardano.Ledger.UMap (umElems, umElemsL)
2323
import Constrained.API
24-
import Constrained.Base (IsPred (..))
25-
import Constrained.Spec.Tree (rootLabel_)
2624
import Data.Coerce
2725
import Data.Foldable
2826
import Data.Map qualified as Map
@@ -149,8 +147,8 @@ proposalsSpec geEpoch gePPolicy geCertState =
149147
(branch $ \_ _ -> False) -- HardForkInitiation
150148
-- Treasury Withdrawal
151149
( branch $ \ [var|withdrawMap|] [var|policy|] ->
152-
Explain (pure "TreasuryWithdrawal fails") $
153-
And
150+
explanation (pure "TreasuryWithdrawal fails") $
151+
fold $
154152
[ dependsOn gasOther withdrawMap
155153
, match geCertState $ \_vState _pState [var|dState|] ->
156154
match dState $ \ [var|rewardMap|] _ _ _ ->
@@ -224,7 +222,7 @@ withPrevActId ::
224222
(Term (StrictMaybe GovActionId) -> Pred) ->
225223
Pred
226224
withPrevActId gas k =
227-
And
225+
fold
228226
[ match (gasProposalProcedure_ gas) $ \_deposit [var|retAddr|] _action _anchor ->
229227
match retAddr $ \ [var|net|] _ -> [dependsOn gas net, assert $ net ==. lit Testnet]
230228
, caseOn

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs

Lines changed: 12 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -46,10 +46,8 @@ import Cardano.Ledger.Plutus.CostModels (CostModels)
4646
import Cardano.Ledger.Plutus.ExUnits
4747
import Cardano.Ledger.Shelley.PParams (ProposedPPUpdates (..))
4848
import Constrained.API
49-
import Constrained.Base
5049
import Constrained.GenT
5150
import Constrained.NumOrd
52-
import Constrained.SumList (genListWithSize)
5351
import Control.Monad.Identity (Identity (..))
5452
import Control.Monad.Trans.Fail.String
5553
import Data.Maybe
@@ -105,12 +103,6 @@ instance OrdLike Coin
105103
instance NumLike Coin
106104

107105
instance Foldy Coin where
108-
genList s s' = map fromSimpleRep <$> genList @Word64 (toSimpleRepSpec s) (toSimpleRepSpec s')
109-
theAddFn = AddW
110-
theZero = Coin 0
111-
genSizedList sz elemSpec foldSpec =
112-
map fromSimpleRep
113-
<$> genListWithSize @Word64 sz (toSimpleRepSpec elemSpec) (toSimpleRepSpec foldSpec)
114106
noNegativeValues = True
115107

116108
-- TODO: This is hack to get around the need for `Num` in `NumLike`. We should possibly split
@@ -136,34 +128,34 @@ instance HasSpec EpochInterval
136128
instance HasSpec UnitInterval where
137129
type TypeSpec UnitInterval = ()
138130
emptySpec = ()
139-
combineSpec _ _ = TrueSpec
131+
combineSpec _ _ = trueSpec
140132
genFromTypeSpec _ = pureGen arbitrary
141-
cardinalTypeSpec _ = TrueSpec
133+
cardinalTypeSpec _ = trueSpec
142134
shrinkWithTypeSpec _ = shrink
143135
conformsTo _ _ = True
144-
toPreds _ _ = toPred True
136+
toPreds _ _ = assert True
145137

146138
instance HasSpec NonNegativeInterval where
147139
type TypeSpec NonNegativeInterval = ()
148140
emptySpec = ()
149-
combineSpec _ _ = TrueSpec
141+
combineSpec _ _ = trueSpec
150142
genFromTypeSpec _ = pureGen arbitrary
151-
cardinalTypeSpec _ = TrueSpec
143+
cardinalTypeSpec _ = trueSpec
152144
shrinkWithTypeSpec _ = shrink
153145
conformsTo _ _ = True
154-
toPreds _ _ = toPred True
146+
toPreds _ _ = assert True
155147

156148
instance HasSimpleRep CostModels
157149

158150
instance HasSpec CostModels where
159151
type TypeSpec CostModels = ()
160152
emptySpec = ()
161-
combineSpec _ _ = TrueSpec
153+
combineSpec _ _ = trueSpec
162154
genFromTypeSpec _ = pureGen arbitrary
163-
cardinalTypeSpec _ = TrueSpec
155+
cardinalTypeSpec _ = trueSpec
164156
shrinkWithTypeSpec _ = shrink
165157
conformsTo _ _ = True
166-
toPreds _ _ = toPred True
158+
toPreds _ _ = assert True
167159

168160
instance HasSimpleRep Prices
169161

@@ -240,12 +232,12 @@ succV_ = fromGeneric_ . (+ 1) . toGeneric_
240232
instance Typeable r => HasSpec (KeyHash r) where
241233
type TypeSpec (KeyHash r) = ()
242234
emptySpec = ()
243-
combineSpec _ _ = TrueSpec
235+
combineSpec _ _ = trueSpec
244236
genFromTypeSpec _ = pureGen arbitrary
245-
cardinalTypeSpec _ = TrueSpec
237+
cardinalTypeSpec _ = trueSpec
246238
shrinkWithTypeSpec _ = shrink
247239
conformsTo _ _ = True
248-
toPreds _ _ = toPred True
240+
toPreds _ _ = assert True
249241

250242
-- =========================================================================================
251243

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

Lines changed: 17 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -116,15 +116,10 @@ import Cardano.Ledger.Shelley.TxWits (ShelleyTxWits (..))
116116
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
117117
import Cardano.Ledger.UMap
118118
import Cardano.Ledger.Val (Val)
119-
import Constrained.API
120-
import Constrained.Base
119+
import Constrained.API.Extend hiding (Sized)
120+
import Constrained.API.Extend qualified as C
121121
import Constrained.GenT (pureGen, vectorOfT)
122122
import Constrained.Generic
123-
import Constrained.NumOrd
124-
import Constrained.Spec.Map
125-
import Constrained.Spec.Tree ()
126-
import Constrained.SumList (genListWithSize)
127-
import Constrained.TheKnot qualified as C
128123
import Control.DeepSeq (NFData)
129124
import Crypto.Hash (Blake2b_224)
130125
import Data.ByteString qualified as BS
@@ -233,14 +228,7 @@ instance OrdLike DeltaCoin
233228

234229
instance NumLike DeltaCoin
235230

236-
instance Foldy DeltaCoin where
237-
genList s s' = map fromSimpleRep <$> genList @Integer (toSimpleRepSpec s) (toSimpleRepSpec s')
238-
theAddFn = AddW
239-
theZero = DeltaCoin 0
240-
genSizedList sz elemSpec foldSpec =
241-
map fromSimpleRep
242-
<$> genListWithSize @Integer sz (toSimpleRepSpec elemSpec) (toSimpleRepSpec foldSpec)
243-
noNegativeValues = False
231+
instance Foldy DeltaCoin
244232

245233
deriving via Integer instance Num DeltaCoin
246234

@@ -274,7 +262,7 @@ instance Typeable index => HasSpec (SafeHash index) where
274262
cardinalTypeSpec _ = TrueSpec
275263
shrinkWithTypeSpec _ = shrink
276264
conformsTo _ _ = True
277-
toPreds _ _ = toPred True
265+
toPreds _ _ = assert True
278266

279267
instance HasSimpleRep TxId
280268

@@ -441,7 +429,7 @@ instance HasSpec PV1.Data where
441429
cardinalTypeSpec _ = TrueSpec
442430
shrinkWithTypeSpec _ = shrink
443431
conformsTo _ _ = True
444-
toPreds _ _ = toPred True
432+
toPreds _ _ = assert True
445433

446434
instance Era era => HasSimpleRep (Data era) where
447435
type SimpleRep (Data era) = PV1.Data
@@ -544,7 +532,7 @@ instance
544532
cardinalTypeSpec _ = TrueSpec
545533
shrinkWithTypeSpec _ = shrink
546534
conformsTo _ _ = True
547-
toPreds _ _ = toPred True
535+
toPreds _ _ = assert True
548536

549537
instance HasSimpleRep CompactAddr where
550538
type SimpleRep CompactAddr = SimpleRep Addr
@@ -597,7 +585,7 @@ instance Typeable b => HasSpec (AbstractHash Blake2b_224 b) where
597585
shrinkWithTypeSpec _ _ = []
598586
cardinalTypeSpec _ = TrueSpec
599587
conformsTo _ _ = True
600-
toPreds _ _ = toPred True
588+
toPreds _ _ = assert True
601589

602590
instance HasSimpleRep StakeReference
603591

@@ -654,7 +642,7 @@ instance Typeable r => HasSpec (VRFVerKeyHash r) where
654642
cardinalTypeSpec _ = TrueSpec
655643
shrinkWithTypeSpec _ = shrink
656644
conformsTo _ _ = True
657-
toPreds _ _ = toPred True
645+
toPreds _ _ = assert True
658646

659647
instance (HashAlgorithm a, Typeable b) => HasSpec (Hash a b) where
660648
type TypeSpec (Hash a b) = ()
@@ -664,7 +652,7 @@ instance (HashAlgorithm a, Typeable b) => HasSpec (Hash a b) where
664652
cardinalTypeSpec _ = TrueSpec
665653
shrinkWithTypeSpec _ = shrink
666654
conformsTo _ _ = True
667-
toPreds _ _ = toPred True
655+
toPreds _ _ = assert True
668656

669657
instance HasSimpleRep (ConwayTxCert era)
670658

@@ -694,7 +682,7 @@ instance HasSpec StakePoolRelay where
694682
cardinalTypeSpec _ = TrueSpec
695683
shrinkWithTypeSpec _ = shrink
696684
conformsTo _ _ = True
697-
toPreds _ _ = toPred True
685+
toPreds _ _ = assert True
698686

699687
instance HasSimpleRep Port
700688

@@ -718,7 +706,7 @@ instance HasSpec Url where
718706
cardinalTypeSpec _ = TrueSpec
719707
shrinkWithTypeSpec _ = shrink
720708
conformsTo _ _ = True
721-
toPreds _ _ = toPred True
709+
toPreds _ _ = assert True
722710

723711
instance HasSpec Text where
724712
type TypeSpec Text = ()
@@ -728,7 +716,7 @@ instance HasSpec Text where
728716
cardinalTypeSpec _ = TrueSpec
729717
shrinkWithTypeSpec _ = shrink
730718
conformsTo _ _ = True
731-
toPreds _ _ = toPred True
719+
toPreds _ _ = assert True
732720

733721
newtype StringSpec = StringSpec {strSpecLen :: Specification Int}
734722

@@ -911,7 +899,7 @@ instance HasSpec Char where
911899
cardinalTypeSpec _ = TrueSpec
912900
shrinkWithTypeSpec _ = shrink
913901
conformsTo _ _ = True
914-
toPreds _ _ = toPred True
902+
toPreds _ _ = assert True
915903

916904
instance HasSpec CostModel where
917905
type TypeSpec CostModel = ()
@@ -921,7 +909,7 @@ instance HasSpec CostModel where
921909
cardinalTypeSpec _ = TrueSpec
922910
shrinkWithTypeSpec _ = shrink
923911
conformsTo _ _ = True
924-
toPreds _ _ = toPred True
912+
toPreds _ _ = assert True
925913

926914
instance HasSimpleRep Language
927915

@@ -1690,7 +1678,7 @@ instance Typeable r => HasSpec (WitVKey r) where
16901678
cardinalTypeSpec _ = TrueSpec
16911679
shrinkWithTypeSpec _ = shrink
16921680
conformsTo _ _ = True
1693-
toPreds _ _ = toPred True
1681+
toPreds _ _ = assert True
16941682

16951683
instance HasSpec BootstrapWitness where
16961684
type TypeSpec BootstrapWitness = ()
@@ -1700,7 +1688,7 @@ instance HasSpec BootstrapWitness where
17001688
cardinalTypeSpec _ = TrueSpec
17011689
shrinkWithTypeSpec _ = shrink
17021690
conformsTo _ _ = True
1703-
toPreds _ _ = toPred True
1691+
toPreds _ _ = assert True
17041692

17051693
instance Era era => HasSimpleRep (LedgerEnv era)
17061694

@@ -1843,7 +1831,7 @@ class Coercible a b => CoercibleLike a b where
18431831
Specification b
18441832

18451833
instance Typeable krole => CoercibleLike (KeyHash krole) (KeyHash 'Witness) where
1846-
coerceSpec (ExplainSpec es x) = explainSpecOpt es (coerceSpec x)
1834+
coerceSpec (ExplainSpec es x) = explainSpec es (coerceSpec x)
18471835
coerceSpec (TypeSpec z excl) = TypeSpec z $ coerceKeyRole <$> excl
18481836
coerceSpec (MemberSpec s) = MemberSpec $ coerceKeyRole <$> s
18491837
coerceSpec (ErrorSpec e) = ErrorSpec e

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/TxBody.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ import Cardano.Ledger.Mary.Value (MultiAsset (..))
2828
import Cardano.Ledger.Shelley (ShelleyEra)
2929
import Cardano.Ledger.Shelley.PParams (Update (..))
3030
import Cardano.Ledger.TxIn (TxIn (..))
31-
import Constrained.API
31+
import Constrained.API hiding (Sized)
3232
import Constrained.Generic
3333
import Data.Foldable (toList)
3434
import Data.Map.Strict (Map)

0 commit comments

Comments
 (0)