Merge pull request #4121 from IntersectMBO/s-newconstaintsPhase3-addSize

Add `cardinality` and generalize `length` and `setSize`.

libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs

@@ -291,3 +291,11 @@ utxoTests =
     , testProperty "prop_UTXOW" prop_UTXOW
     , testProperty "prop_UTXOS" prop_UTXOS
     ]
+
+epoch :: TestTree
+epoch =
+  testGroup
+    "STS property tests"
+    [ govTests
+    , testProperty "prop_EPOCH" prop_EPOCH
+    ]

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

@@ -159,6 +159,9 @@ instance Monad m => Monad (GenT m) where
 strictGen :: GenT m a -> Gen (m a)
 strictGen gen = runGenT gen Strict
 
+genFromGenT :: GenT GE a -> Gen a
+genFromGenT genT = errorGE <$> runGenT genT Strict
+
 resizeT :: (Int -> Int) -> GenT m a -> GenT m a
 resizeT f (GenT gm) = GenT $ \mode -> sized $ \sz -> resize (f sz) (gm mode)
 

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

@@ -67,21 +67,11 @@ instance BaseUniverse fn => Functions (BoolFn fn) fn where
       let args = appendList (mapList (\(Value a) -> Lit a) pre) (v' :> mapList (\(Value a) -> Lit a) suf)
        in Let (App (injectFn fn) args) (v :-> ps)
   propagateSpecFun Not (NilCtx HOLE) spec = caseBoolSpec spec (equalSpec . not)
-  propagateSpecFun And (HOLE :? Value (s :: Bool) :> Nil) spec = caseBoolSpec spec (okAnd s)
-  propagateSpecFun And (Value (s :: Bool) :! NilCtx HOLE) spec = caseBoolSpec spec (okAnd s)
   propagateSpecFun Or (HOLE :? Value (s :: Bool) :> Nil) spec = caseBoolSpec spec (okOr s)
   propagateSpecFun Or (Value (s :: Bool) :! NilCtx HOLE) spec = caseBoolSpec spec (okOr s)
 
   mapTypeSpec Not _ = typeSpec ()
 
--- | We have something like ('constant' &&. HOLE) must evaluate to 'need'. Return a (Spec fn Bool) for HOLE, that makes that True.
-okAnd :: Bool -> Bool -> Spec fn Bool
-okAnd constant need = case (constant, need) of
-  (True, True) -> MemberSpec [True]
-  (True, False) -> MemberSpec [False]
-  (False, False) -> TrueSpec
-  (False, True) -> ErrorSpec ["(" ++ show constant ++ " &&. HOLE) must equal True. That cannot be the case."]
-
 -- | We have something like ('constant' ||. HOLE) must evaluate to 'need'. Return a (Spec fn Bool) for HOLE, that makes that True.
 okOr :: Bool -> Bool -> Spec fn Bool
 okOr constant need = case (constant, need) of

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

@@ -13,6 +13,12 @@
 
 module Constrained.Spec.Maps (MapSpec (..), dom_, rng_) where
 
+import Constrained.Base
+import Constrained.Core
+import Constrained.GenT
+import Constrained.Instances ()
+import Constrained.List
+import Constrained.Univ
 import Control.Monad
 import Data.List (nub)
 import Data.Map (Map)
@@ -21,21 +27,23 @@ import Data.Set (Set)
 import Data.Set qualified as Set
 import Prettyprinter
 
-import Constrained.Base
-import Constrained.Core
-import Constrained.GenT
-import Constrained.Instances ()
-import Constrained.List
-import Constrained.Univ
-
 ------------------------------------------------------------------------
 -- HasSpec
 ------------------------------------------------------------------------
 
+instance Ord a => Sized (Map.Map a b) where
+  sizeOf = toInteger . Map.size
+  liftSizeSpec sizespec = TypeSpec (MapSpec mempty mempty (typeSpec sizespec) TrueSpec NoFold) []
+  liftMemberSpec xs = typeSpec (MapSpec mempty mempty (MemberSpec xs) TrueSpec NoFold)
+  sizeOfTypeSpec (MapSpec mustk mustv size _ _) =
+    typeSpec (atLeastSize (sizeOf mustk))
+      <> typeSpec (atLeastSize (sizeOf mustv))
+      <> size
+
 data MapSpec fn k v = MapSpec
   { mapSpecMustKeys :: Set k
   , mapSpecMustValues :: [v]
-  , mapSpecSize :: Spec fn Int
+  , mapSpecSize :: Spec fn Integer
   , mapSpecElem :: Spec fn (k, v)
   , mapSpecFold :: FoldSpec fn v
   }
@@ -75,7 +83,7 @@ instance
     and
       [ mustKeys `Set.isSubsetOf` Map.keysSet m
       , all (`elem` Map.elems m) mustVals
-      , Map.size m `conformsToSpec` size
+      , sizeOf m `conformsToSpec` size
       , all (`conformsToSpec` kvs) (Map.toList m)
       , Map.elems m `conformsToFoldSpec` foldSpec
       ]
@@ -88,7 +96,10 @@ instance
     let haveVals = map snd mustMap
         mustVals' = filter (`notElem` haveVals) mustVals
         size' = constrained $ \sz ->
-          satisfies (sz + Lit (length mustMap)) (size <> specSizeBound (mapSpec fstFn $ mapSpec toGenericFn kvs))
+          -- TODO, we should make sure size' is greater than or equal to 0
+          satisfies
+            (sz + Lit (sizeOf mustMap))
+            (size <> cardinality (mapSpec fstFn $ mapSpec toGenericFn kvs))
         foldSpec' = case foldSpec of
           NoFold -> NoFold
           FoldSpec fn sumSpec -> FoldSpec fn $ propagateSpecFun (theAddFn @fn) (HOLE :? Value mustSum :> Nil) sumSpec
@@ -133,7 +144,7 @@ instance
       , forAll (Lit mustVals) $ \val ->
           app (elemFn @fn) val (app (rngFn @fn) m)
       , -- TODO: make nice
-        satisfies (app (injectFn $ ListSize @fn) $ app (rngFn @fn) m) size
+        satisfies (app (injectFn $ SizeOf @fn) $ app (rngFn @fn) m) size
       , forAll m $ \kv -> satisfies kv kvs
       , toPredsFoldSpec (app (rngFn @fn) m) foldSpec
       ]
@@ -160,9 +171,16 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
           , Evidence <- prerequisites @fn @(Map k v) ->
               case spec of
                 MemberSpec [s] ->
-                  typeSpec $ MapSpec s [] (equalSpec $ Set.size s) TrueSpec NoFold
+                  typeSpec $
+                    MapSpec s [] (exactSizeSpec $ sizeOf s) TrueSpec NoFold
                 TypeSpec (SetSpec must elemspec size) [] ->
-                  typeSpec $ MapSpec must [] size (constrained $ \kv -> satisfies (app (fstFn @fn) (app (toGenericFn @fn) kv)) elemspec) NoFold
+                  typeSpec $
+                    MapSpec
+                      must
+                      []
+                      size
+                      (constrained $ \kv -> satisfies (app (fstFn @fn) (app (toGenericFn @fn) kv)) elemspec)
+                      NoFold
                 _ -> ErrorSpec ["Dom on bad map spec", show spec]
     Rng ->
       -- No TypeAbstractions in ghc-8.10
@@ -172,7 +190,7 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
           , Evidence <- prerequisites @fn @(Map k v) ->
               case spec of
                 MemberSpec [r] ->
-                  typeSpec $ MapSpec Set.empty r (equalSpec $ length r) TrueSpec NoFold
+                  typeSpec $ MapSpec Set.empty r (equalSpec $ sizeOf r) TrueSpec NoFold
                 TypeSpec (ListSpec must size elemspec foldspec) [] ->
                   typeSpec $ MapSpec Set.empty must size (constrained $ \kv -> satisfies (app (sndFn @fn) (app (toGenericFn @fn) kv)) elemspec) foldspec
                 _ -> ErrorSpec ["Rng on bad map spec", show spec]

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

@@ -52,6 +52,8 @@ instance (HasSpec fn a, HasSpec fn b) => HasSpec fn (Prod a b) where
     satisfies (app fstFn x) sf
       <> satisfies (app sndFn x) ss
 
+  cardinalTypeSpec (Cartesian x y) = multSpecInt (cardinality x) (cardinality y)
+
 deriving instance (HasSpec fn a, HasSpec fn b) => Show (PairSpec fn a b)
 
 -- Functions for working on pairs -----------------------------------------

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

@@ -39,7 +39,7 @@ data RoseTree a = RoseNode a [RoseTree a]
 -- HasSpec for BinTree
 ------------------------------------------------------------------------
 
-data BinTreeSpec fn a = BinTreeSpec Int (Spec fn (BinTree a, a, BinTree a))
+data BinTreeSpec fn a = BinTreeSpec Integer (Spec fn (BinTree a, a, BinTree a))
   deriving (Show)
 
 instance Forallable (BinTree a) (BinTree a, a, BinTree a) where
@@ -88,16 +88,16 @@ instance HasSpec fn a => HasSpec fn (BinTree a) where
       <> genHint sz t
 
 instance HasSpec fn a => HasGenHint fn (BinTree a) where
-  type Hint (BinTree a) = Int
+  type Hint (BinTree a) = Integer
   giveHint h = typeSpec $ BinTreeSpec h TrueSpec
 
 ------------------------------------------------------------------------
 -- HasSpec for RoseTree
 ------------------------------------------------------------------------
 
 data RoseTreeSpec fn a = RoseTreeSpec
-  { roseTreeAvgLength :: Maybe Int
-  , roseTreeMaxSize :: Int
+  { roseTreeAvgLength :: Maybe Integer
+  , roseTreeMaxSize :: Integer
   , roseTreeRootSpec :: Spec fn a
   , roseTreeCtxSpec :: Spec fn (a, [RoseTree a])
   }
@@ -166,7 +166,7 @@ instance (HasSpec fn a, Member (RoseTreeFn fn) fn) => HasSpec fn (RoseTree a) wh
       <> genHint (mal, sz) t
 
 instance (Member (RoseTreeFn fn) fn, HasSpec fn a) => HasGenHint fn (RoseTree a) where
-  type Hint (RoseTree a) = (Maybe Int, Int)
+  type Hint (RoseTree a) = (Maybe Integer, Integer)
   giveHint (avgLen, sz) = typeSpec $ RoseTreeSpec avgLen sz TrueSpec TrueSpec
 
 data RoseTreeFn (fn :: [Type] -> Type -> Type) args res where

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

@@ -15,6 +15,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
 
 module Constrained.Test where
 
@@ -164,8 +165,9 @@ tests =
     , testSpec "successiveChildren8" successiveChildren8
     , testSpec "roseTreeList" roseTreeList
     , numberyTests
-    , testSpec "andPair" andPair
     , testSpec "orPair" orPair
+    , sizeTests
+    , numNumSpecTree
     ]
       ++ [ testSpec ("intRangeSpec " ++ show i) (intRangeSpec i)
          | i <- [-1000, -100, -10, 0, 10, 100, 1000]
@@ -192,6 +194,23 @@ numberyTests =
     , testNumberyListSpec "listSumElemRange" listSumElemRange
     ]
 
+sizeTests :: TestTree
+sizeTests =
+  testGroup "SizeTests" $
+    [ testSpec "sizeAddOrSub1" sizeAddOrSub1
+    , testSpec "sizeAddOrSub2" sizeAddOrSub2
+    , testSpec "sizeAddOrSub3" sizeAddOrSub3
+    , testSpec "sizeAddOrSub4 returns Negative Size" sizeAddOrSub4
+    , testSpec "sizeAddOrSub5" sizeAddOrSub5
+    , testSpec "sizeAddOrSub5" sizeAddOrSub5
+    , testSpec "listSubSize" listSubSize
+    , testSpec "listSubSize" setSubSize
+    , testSpec "listSubSize" mapSubSize
+    , testSpec "hasSizeList" hasSizeList
+    , testSpec "hasSizeSet" hasSizeSet
+    , testSpec "hasSizeMap" hasSizeMap
+    ]
+
 type Numbery a =
   ( Foldy BaseFn a
   , OrdLike BaseFn a
@@ -356,7 +375,7 @@ mapPairSpec = constrained' $ \m s ->
 
 mapEmptyDomainSpec :: Spec BaseFn (Map Int Int)
 mapEmptyDomainSpec = constrained $ \m ->
-  subset_ (dom_ m) mempty
+  subset_ (dom_ m) mempty -- mempty in the Monoid instance (Term fn (Set a))
 
 setPairSpec :: Spec BaseFn (Set Int, Set Int)
 setPairSpec = constrained' $ \s s' ->
@@ -578,11 +597,6 @@ instance BaseUniverse fn => HasSpec fn Three
 mapSizeConstrained :: Spec BaseFn (Map Three Int)
 mapSizeConstrained = constrained $ \m -> size_ (dom_ m) <=. 3
 
-andPair :: Spec BaseFn [(Int, Int)]
-andPair = constrained $ \ps ->
-  forAll' ps $ \x y ->
-    x <=. 5 &&. y <=. 1
-
 orPair :: Spec BaseFn [(Int, Int)]
 orPair = constrained $ \ps ->
   forAll' ps $ \x y ->
@@ -677,3 +691,117 @@ listMustSizeIssue = constrained $ \xs ->
   [ 1 `elem_` xs
   , length_ xs ==. 1
   ]
+
+sizeAddOrSub1 :: Spec BaseFn Integer
+sizeAddOrSub1 = constrained $ \s ->
+  4 ==. s + 2
+
+sizeAddOrSub2 :: Spec BaseFn Integer
+sizeAddOrSub2 = constrained $ \s ->
+  4 ==. 2 + s
+
+sizeAddOrSub3 :: Spec BaseFn Integer
+sizeAddOrSub3 = constrained $ \s ->
+  4 ==. s - 2
+
+-- | We expect a negative Integer, so ltSpec tests for that.
+sizeAddOrSub4 :: Spec BaseFn Integer
+sizeAddOrSub4 = ltSpec 0 <> (constrained $ \s -> 4 ==. 2 - s)
+
+sizeAddOrSub5 :: Spec BaseFn Integer
+sizeAddOrSub5 = constrained $ \s ->
+  2 ==. 12 - s
+
+listSubSize :: Spec BaseFn [Int]
+listSubSize = constrained $ \s ->
+  2 ==. 12 - (sizeOf_ s)
+
+setSubSize :: Spec BaseFn (Set Int)
+setSubSize = constrained $ \s ->
+  2 ==. 12 - (sizeOf_ s)
+
+mapSubSize :: Spec BaseFn (Map Int Int)
+mapSubSize = constrained $ \s ->
+  2 ==. 12 - (sizeOf_ s)
+
+hasSizeList :: Spec BaseFn [Int]
+hasSizeList = hasSize (rangeSize 0 4)
+
+hasSizeSet :: Spec BaseFn (Set Int)
+hasSizeSet = hasSize (rangeSize 1 3)
+
+hasSizeMap :: Spec BaseFn (Map Int Int)
+hasSizeMap = hasSize (rangeSize 1 3)
+
+-- ========================================================
+-- Test properties of the instance Num(NumSpec Integer)
+
+instance Arbitrary (NumSpec Integer) where
+  arbitrary = do
+    lo <- arbitrary
+    hi <- next lo
+    pure $ NumSpecInterval lo hi
+    where
+      next Nothing = arbitrary
+      next (Just n) = frequency [(1, pure Nothing), (3, Just <$> suchThat arbitrary (> n))]
+
+-- | When we multiply intervals, we get a bounding box, around the possible values.
+--   When the intervals have infinities, the bounding box can be very loose. In fact the
+--   order in which we multiply intervals with infinities can affect how loose the bounding box is.
+--   So ((NegInf, n) * (a, b)) * (c,d)  AND  (NegInf, n) * ((a, b) * (c,d)) may have different bounding boxes
+--   To test the associative laws we must have no infinities, and then the associative law will hold.
+noInfinity :: Gen (NumSpec Integer)
+noInfinity = do
+  lo <- arbitrary
+  hi <- suchThat arbitrary (> lo)
+  pure $ NumSpecInterval (Just lo) (Just hi)
+
+plusNegate :: NumSpec Integer -> NumSpec Integer -> Property
+plusNegate x y = x - y === x + negate y
+
+commutesNumSpec :: NumSpec Integer -> NumSpec Integer -> Property
+commutesNumSpec x y = x + y === y + x
+
+assocNumSpec :: NumSpec Integer -> NumSpec Integer -> NumSpec Integer -> Property
+assocNumSpec x y z = x + (y + z) === (x + y) + z
+
+commuteTimes :: (NumSpec Integer) -> (NumSpec Integer) -> Property
+commuteTimes x y = x * y === y * x
+
+assocNumSpecTimes :: Gen Property
+assocNumSpecTimes = do
+  x <- noInfinity
+  y <- noInfinity
+  z <- noInfinity
+  pure (x * (y * z) === (x * y) * z)
+
+negNegate :: NumSpec Integer -> Property
+negNegate x = x === negate (negate x)
+
+scaleNumSpec :: NumSpec Integer -> Property
+scaleNumSpec y = y + y === 2 * y
+
+scaleOne :: NumSpec Integer -> Property
+scaleOne y = y === 1 * y
+
+numNumSpecTree :: TestTree
+numNumSpecTree =
+  testGroup
+    "Num (NumSpec Integer) properties"
+    [ testProperty "plusNegate(x - y == x + negate y)" plusNegate
+    , testProperty "scaleNumSpec(y + y = 2 * y)" scaleNumSpec
+    , testProperty "scaleOne(y = 1 * y)" scaleOne
+    , testProperty "negNagate(x = x == negate (negate x))" negNegate
+    , testProperty "commutesNumSpec(x+y = y+x)" commutesNumSpec
+    , testProperty "assocNumSpec(x+(y+z) == (x+y)+z)" assocNumSpec
+    , testProperty "assocNumSpecTimes(x*(y*z) == (x*y)*z)" assocNumSpecTimes
+    , testProperty "commuteTimes" commuteTimes
+    ]
+
+-- ==========================================================
+
+runTestSpec :: HasSpec BaseFn t => Spec BaseFn t -> IO ()
+runTestSpec spec = defaultMain (testSpec "interactive test with runTestSpec" spec)
+
+generateSpec :: forall fn a. HasSpec fn a => Spec fn a -> IO a
+generateSpec spec = generate (genFromSpec_ @fn spec)