fourmolize, address comments

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

@@ -36,7 +36,9 @@ utxoEnvSpec =
        uePParams
        _ueCertState ->
           [ satisfies uePParams pparamsSpec
-          , match uePParams $ \cpp -> [assert $ (lit 3000) <=. maxTxSize_ cpp]
+          , -- NOTE: this is for testing only! We should figure out a nicer way
+            -- of splitting generation and checking constraints here!
+            match uePParams $ \cpp -> [assert $ (lit 3000) <=. maxTxSize_ cpp]
           ]
 
 utxoStateSpec ::

libs/constrained-generators/src/Constrained/Base.hs

@@ -660,8 +660,10 @@ instance (HasSpec fn a, Arbitrary (TypeSpec fn a)) => Arbitrary (Specification f
               TypeSpec <$> arbitrary <*> vectorOf len (genFromSpec @fn TrueSpec)
           )
         , (1, ErrorSpec <$> arbitrary)
-        , --  , (1, pure $ MemberSpec []) -- This is always inconsistent, So I have temporarily remove it subject to discussion T.S.
-          -- Recurse to make sure we apply the tricks for generating suspended specs multiple times
+        , -- This case is always inconsistent, but, since this is an arbitrary instance.
+          -- We want it to generate dumb things once and a while, to catch bugs.
+          (1, pure $ MemberSpec [])
+        , -- Recurse to make sure we apply the tricks for generating suspended specs multiple times
           (4, arbitrary)
         ]
     -- TODO: we probably want smarter ways of generating constraints
@@ -3286,7 +3288,7 @@ instance (Ord a, HasSpec fn a) => HasSpec fn (Set a) where
         | otherwise = do
             n <-
               explain ["Choose a possible size Bounds for the Sets to be generated"] $
-                genFromSpecT (szSpec <> geqSpec @fn (sizeOf must) <> maxSpec (cardinality elemS))
+                genFromSpecT (szSpec <> geqSpec @fn (sizeOf must) <> maxSpecSize (cardinality elemS))
             explain ["Chose size n = " ++ show n] $ go (n - sizeOf must) must
         where
           go 0 s = pure s
@@ -3305,7 +3307,7 @@ instance (Ord a, HasSpec fn a) => HasSpec fn (Set a) where
   genFromTypeSpec (SetSpec must elemS szSpec) = do
     n <-
       explain ["Choose a possible size Bounds for the Sets to be generated"] $
-        genFromSizeSpec (szSpec <> geqSpec @fn (sizeOf must) <> maxSpec (cardinality elemS))
+        genFromSizeSpec (szSpec <> geqSpec @fn (sizeOf must) <> maxSpecSize (cardinality elemS))
     Set.fromList <$> (genDistinctList elemS (n - sizeOf must) (Set.toList must))
 
   typeSpecOpt (SetSpec x y a) [m] | Set.null m = TypeSpec (SetSpec x y (a <> geqSpec 1)) []
@@ -4922,15 +4924,17 @@ rangeSize a b | a < 0 || b < 0 = error ("Negative Int in call to rangeSize: " ++
 rangeSize a b = NumSpecInterval (Just a) (Just b)
 
 -- | The widest interval whose largest element is admitted by the original spec
---   This is a Size, so if the largest element is 0, then (NumSpecInterval (Just 0) (Just 0))
-maxSpec :: BaseUniverse fn => Specification fn Integer -> Specification fn Integer
-maxSpec TrueSpec = TrueSpec
-maxSpec s@(SuspendedSpec _ _) =
-  constrained $ \x -> unsafeExists $ \y -> [y `satisfies` s, Assert ["maxSpec on SuspendedSpec"] (x <=. y)]
-maxSpec (ErrorSpec xs) = ErrorSpec xs
-maxSpec (MemberSpec []) = ErrorSpec ["empty MemberSec in maxSpec."]
-maxSpec (MemberSpec xs) = leqSpec (maximum (0 : xs)) -- TODO IS this right
-maxSpec (TypeSpec (NumSpecInterval _ hi) bad) = TypeSpec (NumSpecInterval Nothing hi) bad
+--   The is only used when compting cardinalities, which are always Sizes. So don't
+--   use this on Specifications not representaing Sizes.
+--   Used only on Sizes, so if the largest element is 0, then we get (NumSpecInterval (Just 0) (Just 0))
+maxSpecSize :: BaseUniverse fn => Specification fn Integer -> Specification fn Integer
+maxSpecSize TrueSpec = TrueSpec
+maxSpecSize s@(SuspendedSpec _ _) =
+  constrained $ \x -> unsafeExists $ \y -> [y `satisfies` s, Assert ["maxSpecSize on SuspendedSpec"] (x <=. y)]
+maxSpecSize (ErrorSpec xs) = ErrorSpec xs
+maxSpecSize (MemberSpec []) = ErrorSpec ["empty MemberSec in maxSpecSize."]
+maxSpecSize (MemberSpec xs) = leqSpec (maximum (0 : xs)) -- TODO IS this right
+maxSpecSize (TypeSpec (NumSpecInterval _ hi) bad) = TypeSpec (NumSpecInterval Nothing hi) bad
 
 -- ================
 -- Sized

libs/constrained-generators/src/Constrained/Examples/Map.hs

@@ -110,30 +110,30 @@ rngSetWithHint = constrained $ \m ->
 
 -- Different ways to constrain the size of a Map
 
-w0 :: Specification BaseFn (Map Int Int)
-w0 = constrained $ \m ->
+sizeOfMap :: Specification BaseFn (Map Int Int)
+sizeOfMap = constrained $ \m ->
   [assert $ sizeOf_ m ==. 10]
 
-w1 :: Specification BaseFn (Map Int Int)
-w1 = constrained $ \m ->
+sizeOfDomMap :: Specification BaseFn (Map Int Int)
+sizeOfDomMap = constrained $ \m ->
   [assert $ sizeOf_ (dom_ m) ==. 10] -- sizeOf_ works on things that are Sized
 
-w2 :: Specification BaseFn (Map Three Int)
-w2 = constrained $ \m -> size_ (dom_ m) <=. 3 -- size_ works on Sets,
+sizeDomMap :: Specification BaseFn (Map Three Int)
+sizeDomMap = constrained $ \m -> size_ (dom_ m) <=. 3 -- size_ works on Sets,
 
-w3 :: Specification BaseFn (Map Int Int)
-w3 = constrained $ \m ->
+sizeOfRngMap :: Specification BaseFn (Map Int Int)
+sizeOfRngMap = constrained $ \m ->
   [assert $ sizeOf_ (rng_ m) ==. 10]
 
-w4 :: Specification BaseFn (Map Int Int)
-w4 = constrained $ \m ->
+sizeOfRngSetMap :: Specification BaseFn (Map Int Int)
+sizeOfRngSetMap = constrained $ \m ->
   [assert $ sizeOf_ (rngSet_ m) ==. 4]
 
-w5 :: Specification BaseFn (Map Int Int)
-w5 = constrained $ \m -> [assert $ m /=. lit mempty]
+sizeNotEqualEmpty :: Specification BaseFn (Map Int Int)
+sizeNotEqualEmpty = constrained $ \m -> [assert $ m /=. lit mempty]
 
-w6 :: Specification BaseFn (Map Int Int)
-w6 = constrained $ \m -> [assert $ m ==. lit mempty]
+sizeEqualEmpty :: Specification BaseFn (Map Int Int)
+sizeEqualEmpty = constrained $ \m -> [assert $ m ==. lit mempty]
 
 -- | When a test on a Map spec fails, this function traces the steps, to help
 --   discover what went wrong.

libs/constrained-generators/src/Constrained/Spec/Map.hs

@@ -486,8 +486,8 @@ genFromMapSpecWithFold m@(MapSpec mHint mustKeys mustVals size (simplifySpec ->
           (sz + Lit (sizeOf mustMap))
           ( maybe TrueSpec (leqSpec . max 0) mHint
               <> size
-              <> maxSpec (cardinality (mapSpec fstFn $ mapSpec toGenericFn kvs))
-              <> maxSpec (cardinalTrueSpec @fn @k)
+              <> maxSpecSize (cardinality (mapSpec fstFn $ mapSpec toGenericFn kvs))
+              <> maxSpecSize (cardinalTrueSpec @fn @k)
           )
 
       foldSpec' = case foldspec of

libs/constrained-generators/test/Constrained/Test.hs

@@ -130,6 +130,15 @@ tests nightly =
     testSpec "richRngSetSpec" richRngSetSpec
     testSpec "rngSetWithHint" rngSetWithHint
     testSpec "richRngSetSpec" richRngSetSpec
+
+    testSpec "sizeOfMap" sizeOfMap
+    testSpec "sizeOfDomMap" sizeOfDomMap
+    testSpec "sizeDomMap" sizeDomMap
+    testSpec "sizeOfRngMap" sizeOfRngMap
+    testSpec "sizeOfRngSetMap" sizeOfRngSetMap
+    testSpec "sizeNotEqualEmpty" sizeNotEqualEmpty
+    testSpec "sizeEqualEmpty" sizeEqualEmpty
+
     testSpec "basicSpec" basicSpec
     testSpec "canFollowLike" canFollowLike
     testSpec "ifElseBackwards" ifElseBackwards
@@ -161,11 +170,10 @@ tests nightly =
       prop "[Int]" $ prop_conformEmpty @BaseFn @[Int]
       prop "[(Int, Int)]" $ prop_conformEmpty @BaseFn @[(Int, Int)]
     prop "prop_univSound @BaseFn" $
-      withMaxSuccess 100 $ -- (if nightly then 100_000 else 10_000) $
+      withMaxSuccess (if nightly then 100_000 else 10_000) $
         prop_univSound @BaseFn
     describe "prop_gen_sound @BaseFn" $ do
-      modifyMaxSuccess (const 100) $ do
-        -- (const $ if nightly then 10_000 else 1000) $ do
+      modifyMaxSuccess (const $ if nightly then 10_000 else 1000) $ do
         prop "Int" $ prop_gen_sound @BaseFn @Int
         prop "Bool" $ prop_gen_sound @BaseFn @Bool
         prop "(Int, Int)" $ prop_gen_sound @BaseFn @(Int, Int)