Added MinValSize

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

@@ -137,7 +137,7 @@ import Cardano.Ledger.UTxO
 import Cardano.Ledger.Val (Val)
 import Constrained hiding (Value)
 import Constrained qualified as C
-import Constrained.Base (HasGenHint (..), Term (..))
+import Constrained.Base (Binder (..), HasGenHint (..), Pred (..), Term (..))
 import Constrained.Spec.Map
 import Constrained.Univ ()
 import Control.Monad.Trans.Fail.String
@@ -1389,8 +1389,8 @@ instance (IsConwayUniv fn, Crypto c) => HasSpec fn (IncrementalStake c)
 instance HasSimpleRep (UTxO era)
 instance (Era era, HasSpec fn (TxOut era), IsConwayUniv fn) => HasSpec fn (UTxO era)
 
-instance HasSimpleRep (FuturePParams (ConwayEra StandardCrypto))
-instance IsConwayUniv fn => HasSpec fn (FuturePParams (ConwayEra StandardCrypto))
+instance HasSimpleRep (FuturePParams era)
+instance (EraPP era, IsConwayUniv fn) => HasSpec fn (FuturePParams era)
 
 instance HasSimpleRep (ConwayGovState (ConwayEra StandardCrypto))
 instance IsConwayUniv fn => HasSpec fn (ConwayGovState (ConwayEra StandardCrypto))

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

@@ -53,7 +53,7 @@ import Cardano.Ledger.UMap (CompactForm (..), RDPair)
 import qualified Cardano.Ledger.UMap as UMap
 import Cardano.Ledger.UTxO (UTxO (..))
 import Constrained hiding (Value)
-import Constrained.Base (Sized (..), hasSize, rangeSize, (>=.))
+import Constrained.Base (Pred (..), Sized (..), hasSize, rangeSize, (>=.))
 import Constrained.Spec.Map (rngSet_)
 import Data.Default.Class (Default (def))
 import Data.Map (Map)
@@ -536,7 +536,7 @@ shelleyGovStateSpec ::
   forall era fn. Constrain era fn => PParams era -> Specification fn (ShelleyGovState era)
 shelleyGovStateSpec pp =
   constrained $ \sgs ->
-    match sgs $ \curpro futpro curpp _futpp ->
+    match sgs $ \curpro futpro curpp _prevpp _futpp ->
       match curpro $ \cm ->
         [ satisfies cm (hasSize (rangeSize 1 2))
         , match futpro $ \fm -> satisfies fm (hasSize (rangeSize 1 2))
@@ -563,7 +563,7 @@ conwayGovStateSpec ::
   Specification fn (ConwayGovState Conway)
 conwayGovStateSpec pp govenv =
   constrained $ \conwaygs ->
-    match conwaygs $ \proposals _mcommittee _consti curpp _prevpp _derepPulstate ->
+    match conwaygs $ \proposals _mcommittee _consti curpp _prevpp _futurepp _derepPulstate ->
       [ assert $ curpp ==. lit pp
       , satisfies proposals (govProposalsSpec govenv)
       ]

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

@@ -2819,8 +2819,8 @@ pcFuturePParams p = \case
   PotentialPParamsUpdate mpp -> ppSexp "PotentialPParamsUpdate" [ppMaybe (pcPParamsSynopsis p) mpp]
   DefinitePParamsUpdate pp -> ppSexp "DefinitePParamsUpdate" [pcPParamsSynopsis p pp]
 
-pcShelleyGovState :: Proof era -> ShelleyGovState era -> PDoc  
-pcShelleyGovState p (ShelleyGovState proposal futproposal pp prevpp) =
+pcShelleyGovState :: Proof era -> ShelleyGovState era -> PDoc
+pcShelleyGovState p (ShelleyGovState proposal futproposal pp prevpp futurepp) =
   ppRecord
     "ShelleyGovState"
     [ ("proposals", ppProposedPPUpdates p proposal)
@@ -3240,11 +3240,11 @@ psEpochState proof es@(EpochState (AccountState tre res) ls sss _) =
     ]
 
 pcNewEpochState :: Reflect era => Proof era -> NewEpochState era -> PDoc
-pcNewEpochState proof (NewEpochState en (BlocksMade pbm) (BlocksMade cbm) es pulrew (PoolDistr pd) avm) =
+pcNewEpochState proof (NewEpochState en (BlocksMade pbm) (BlocksMade cbm) es pulrew pd avm) =
   ppRecord
     "NewEpochState"
     [ ("EpochState", pcEpochState proof es)
-    , ("PoolDistr", ppMap pcKeyHash pcIndividualPoolStake pd)
+    , ("PoolDistr", pcPoolDistr pd)
     , ("Prev Blocks", ppMap pcKeyHash ppNatural pbm)
     , ("Current Blocks", ppMap pcKeyHash ppNatural cbm)
     , ("EpochNo", ppEpochNo en)
@@ -3264,11 +3264,11 @@ instance Reflect era => PrettyA (NewEpochState era) where prettyA = pcNewEpochSt
 
 -- | Like pcEpochState.but it only prints a summary of the UTxO
 psNewEpochState :: Reflect era => Proof era -> NewEpochState era -> PDoc
-psNewEpochState proof (NewEpochState en (BlocksMade pbm) (BlocksMade cbm) es pulrew (PoolDistr pd) avm) =
+psNewEpochState proof (NewEpochState en (BlocksMade pbm) (BlocksMade cbm) es pulrew pd avm) =
   ppRecord
     "NewEpochState"
     [ ("EpochState", psEpochState proof es)
-    , ("PoolDistr", ppMap pcKeyHash pcIndividualPoolStake pd)
+    , ("PoolDistr", pcPoolDistr pd)
     , ("Prev Blocks", ppMap pcKeyHash ppNatural pbm)
     , ("Current Blocks", ppMap pcKeyHash ppNatural cbm)
     , ("EpochNo", ppEpochNo en)

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

@@ -43,8 +43,6 @@
 -- depends in turn on `Pred` and so on.
 module Constrained.Base where
 
-import Debug.Trace
-
 import Control.Applicative
 import Control.Arrow (first)
 import Control.Monad
@@ -864,7 +862,7 @@ conformsToSpecProp :: forall fn a. HasSpec fn a => a -> Specification fn a -> Pr
 conformsToSpecProp a s = fromGEProp $ conformsToSpecM a (simplifySpec s)
 
 conformsToSpec :: forall fn a. HasSpec fn a => a -> Specification fn a -> Bool
-conformsToSpec a s = trace ("\nCONFORMSTOSPEC " ++ show s) $ isOk $ conformsToSpecM a s
+conformsToSpec a s = isOk $ conformsToSpecM a s
 
 satisfies :: forall fn a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn
 satisfies _ TrueSpec = TruePred
@@ -1019,7 +1017,7 @@ prepareLinearization p = do
       graph = transitiveClosure $ hints <> respecting hints (foldMap computeDependencies preds)
 
   -- (,graph) <$> linearize preds graph
-  (,graph) <$> explain ["While linerearizing", show p] $ linearize preds graph
+  explain ["While linerearizing", show p] $ (,graph) <$> linearize preds graph
 
 -- | Generate a satisfying `Env` for a `p : Pred fn`. The `Env` contains values for
 -- all the free variables in `flattenPred p`.

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

@@ -104,8 +104,8 @@ errorGE :: GE a -> a
 errorGE = fromGE (error . unlines)
 
 isOk :: GE a -> Bool
-isOk GenError {} = False
-isOk FatalError {} = False
+isOk (GenError {}) = False
+isOk (FatalError {}) = False
 isOk Result {} = True
 
 runGE :: MonadGenError m => GE r -> m r

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

@@ -44,9 +44,10 @@ instance Ord a => Sized (Map.Map a b) where
   sizeOf = toInteger . Map.size
   liftSizeSpec sz = typeSpec $ defaultMapSpec {mapSpecSize = typeSpec sz}
   liftMemberSpec xs = typeSpec $ defaultMapSpec {mapSpecSize = MemberSpec xs}
-  sizeOfTypeSpec (MapSpec _ mustk mustv size _ _) =
+  sizeOfTypeSpec (MapSpec _ mustk mustv size _ _ smallest) =
     typeSpec (atLeastSize (sizeOf mustk))
       <> typeSpec (atLeastSize (sizeOf mustv))
+      <> smallestSpec smallest
       <> size
 
 data MapSpec fn k v = MapSpec
@@ -56,11 +57,21 @@ data MapSpec fn k v = MapSpec
   , mapSpecSize :: Specification fn Integer
   , mapSpecElem :: Specification fn (k, v)
   , mapSpecFold :: FoldSpec fn v
+  , mapSpecMinValSize :: Maybe (MinValSize v)
+  -- The smallest number of unique Values that meet spec.
+  -- This should look like: Nothing or (Just n),
+  -- if it is (Just n), it means the size of the rngSet is constrained by (NumspecInterval (Just n) Nothing)
   }
 
+data MinValSize v where
+  MinValSize :: Ord v => Integer -> MinValSize v
+
+deriving instance Eq (MinValSize v)
+deriving instance Show (MinValSize v)
+
 -- | emptySpec without all the constraints
 defaultMapSpec :: Ord k => MapSpec fn k v
-defaultMapSpec = MapSpec Nothing mempty mempty TrueSpec TrueSpec NoFold
+defaultMapSpec = MapSpec Nothing mempty mempty TrueSpec TrueSpec NoFold Nothing
 
 deriving instance
   ( HasSpec fn (k, v)
@@ -74,7 +85,7 @@ instance Ord k => Forallable (Map k v) (k, v) where
   forAllToList = Map.toList
 
 instance
-  (Ord k, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) =>
+  (Ord k, Functions fn fn, HasSpec fn (Prod k v), HasSpec fn k, HasSpec fn v, HasSpec fn [v]) =>
   HasSpec fn (Map k v)
   where
   type TypeSpec fn (Map k v) = MapSpec fn k v
@@ -83,31 +94,34 @@ instance
   emptySpec = defaultMapSpec
 
   combineSpec
-    (MapSpec mHint mustKeys mustVals size kvs foldSpec)
-    (MapSpec mHint' mustKeys' mustVals' size' kvs' foldSpec') = fromGESpec $ do
+    (MapSpec mHint mustKeys mustVals size kvs foldSpec acceptable)
+    (MapSpec mHint' mustKeys' mustVals' size' kvs' foldSpec' acceptable') = fromGESpec $ do
       typeSpec
-        . MapSpec
-          -- This is min because that allows more compositionality - if a spec specifies a
-          -- low upper bound because some part of the spec will be slow it doesn't make sense
-          -- to increase it somewhere else because that part isn't slow.
-          (unionWithMaybe min mHint mHint')
-          (mustKeys <> mustKeys')
-          (nub $ mustVals <> mustVals')
-          (size <> size')
-          (kvs <> kvs')
-        <$> combineFoldSpec foldSpec foldSpec'
-
-  conformsTo m (MapSpec _ mustKeys mustVals size kvs foldSpec) =
+        <$> ( MapSpec
+                -- This is min because that allows more compositionality - if a spec specifies a
+                -- low upper bound because some part of the spec will be slow it doesn't make sense
+                -- to increase it somewhere else because that part isn't slow.
+                (unionWithMaybe min mHint mHint')
+                (mustKeys <> mustKeys')
+                (nub $ mustVals <> mustVals')
+                (size <> size')
+                (kvs <> kvs')
+                <$> (combineFoldSpec foldSpec foldSpec')
+                <*> (pure (smallestAcceptableSize acceptable acceptable'))
+            )
+
+  conformsTo m (MapSpec _ mustKeys mustVals size kvs foldSpec minval) =
     trace ("\nCONFORMSTO MAP") $
       and
-        [ tell "mustkeys" $ mustKeys `Set.isSubsetOf` Map.keysSet m
-        , tell "mustvalues" $ all (`elem` Map.elems m) mustVals
-        , tell "size" $ sizeOf m `conformsToSpec` size
-        , tell "conforms pairs" $ all (`conformsToSpec` kvs) (Map.toList m)
-        , tell "conforms fold" $ Map.elems m `conformsToFoldSpec` foldSpec
+        [ trace "mustkeys" $ mustKeys `Set.isSubsetOf` Map.keysSet m
+        , trace "mustvalues" $ all (`elem` Map.elems m) mustVals
+        , trace "size" $ sizeOf m `conformsToSpec` size
+        , trace "conforms pairs" $ all (`conformsToSpec` kvs) (Map.toList m)
+        , trace "conforms fold" $ Map.elems m `conformsToFoldSpec` foldSpec
+        , trace "conformms smallest" $ conformsToSpec @fn (sizeOf (nub (Map.elems m))) (smallestSpec minval)
         ]
 
-  genFromTypeSpec (MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) foldSpec) = do
+  genFromTypeSpec m@(MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) foldSpec _smallest) = trace ("\nGENMAP\n" ++ show m) $ do
     mustMap <- explain ["Make the mustMap"] $ forM (Set.toList mustKeys) $ \k -> do
       let vSpec = constrained $ \v -> satisfies (pair_ (lit k) v) kvs
       v <- explain [show $ "vSpec =" <+> pretty vSpec] $ genFromSpec vSpec
@@ -153,14 +167,17 @@ instance
           go (Map.insert k v m) restVals'
     go (Map.fromList mustMap) restVals
 
-  shrinkWithTypeSpec (MapSpec _ _ _ _ kvs _) m = map Map.fromList $ shrinkList (shrinkWithSpec kvs) (Map.toList m)
+  shrinkWithTypeSpec (MapSpec _ _ _ _ kvs _ _) m = map Map.fromList $ shrinkList (shrinkWithSpec kvs) (Map.toList m)
 
-  toPreds m (MapSpec mHint mustKeys mustVals size kvs foldSpec) =
+  toPreds m (MapSpec mHint mustKeys mustVals size kvs foldSpec minvalsize) =
     toPred
       [ assert $ lit mustKeys `subset_` dom_ m
       , forAll (Lit mustVals) $ \val ->
           val `elem_` rng_ m
       , sizeOf_ (rng_ m) `satisfies` size
+      , case minvalsize of
+          Nothing -> TruePred
+          Just (MinValSize n) -> sizeOf_ (rngSet_ m) `satisfies` (leqSpec n)
       , forAll m $ \kv -> satisfies kv kvs
       , toPredsFoldSpec (rng_ m) foldSpec
       , maybe TruePred (`genHint` m) mHint
@@ -196,7 +213,7 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
               case spec of
                 MemberSpec [s] ->
                   typeSpec $
-                    MapSpec Nothing s [] (exactSizeSpec $ sizeOf s) TrueSpec NoFold
+                    MapSpec Nothing s [] (exactSizeSpec $ sizeOf s) TrueSpec NoFold Nothing
                 TypeSpec (SetSpec must elemspec size) [] ->
                   typeSpec $
                     MapSpec
@@ -206,6 +223,7 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
                       size
                       (constrained $ \kv -> satisfies (app (fstFn @fn) (app (toGenericFn @fn) kv)) elemspec)
                       NoFold
+                      Nothing
                 _ -> ErrorSpec ["Dom on bad map spec", show spec]
     Rng ->
       -- No TypeAbstractions in ghc-8.10
@@ -215,17 +233,17 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
           , Evidence <- prerequisites @fn @(Map k v) ->
               case spec of
                 MemberSpec [r] ->
-                  typeSpec $ MapSpec Nothing Set.empty r (equalSpec $ sizeOf r) TrueSpec NoFold
+                  typeSpec $ MapSpec Nothing Set.empty r (equalSpec $ sizeOf r) TrueSpec NoFold Nothing
                 TypeSpec (ListSpec listHint must size elemspec foldspec) [] ->
                   typeSpec $
                     MapSpec
                       listHint
                       Set.empty
                       must
                       size
-                      -- (constrained $ \kv -> satisfies (app (sndFn @fn) (app (toGenericFn @fn) kv)) elemspec)
                       (constrained $ \kv -> satisfies (snd_ kv) elemspec)
                       foldspec
+                      Nothing
                 _ -> ErrorSpec ["Rng on bad map spec", show spec]
     RngSet ->
       case fn of
@@ -236,9 +254,16 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
                 MemberSpec [r] ->
                   trace ("\nRngSet MemberSpec " ++ show r) $
                     typeSpec $
-                      MapSpec Nothing Set.empty (Set.toList r) (equalSpec $ sizeOf r) TrueSpec NoFold
+                      MapSpec
+                        Nothing
+                        Set.empty
+                        (Set.toList r)
+                        (equalSpec $ sizeOf r)
+                        TrueSpec
+                        NoFold
+                        (Just (MinValSize (sizeOf r)))
                 TypeSpec (ss@(SetSpec must elemspec setsize)) [] ->
-                  trace ("\nTypeSpec (" ++ show ss ++ ")") $
+                  trace ("\nSETSPEC (" ++ show ss ++ ")") $
                     let mp =
                           MapSpec
                             Nothing
@@ -247,6 +272,7 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
                             ((geqSpec (fromIntegral (Set.size must))) <> setsize) -- This might be overconstrained.
                             (constrained $ \kv -> satisfies (app (sndFn @fn) (app (toGenericFn @fn) kv)) elemspec)
                             NoFold
+                            (smallest setsize)
                      in trace ("\nMAPSPEC " ++ show mp) (typeSpec mp)
                 {-
 
@@ -268,20 +294,20 @@ instance BaseUniverse fn => Functions (MapFn fn) fn where
       -- No TypeAbstractions in ghc-8.10
       case f of
         (_ :: MapFn fn '[Map k v] (Set k))
-          | MapSpec _ mustSet _ sz kvSpec _ <- ts
+          | MapSpec _ mustSet _ sz kvSpec _ _ <- ts
           , Evidence <- prerequisites @fn @(Map k v) ->
               typeSpec $ SetSpec mustSet (mapSpec (fstFn @fn) $ toSimpleRepSpec kvSpec) sz
     Rng ->
       -- No TypeAbstractions in ghc-8.10
       case f of
         (_ :: MapFn fn '[Map k v] [v])
-          | MapSpec _ _ mustList sz kvSpec foldSpec <- ts
+          | MapSpec _ _ mustList sz kvSpec foldSpec _ <- ts
           , Evidence <- prerequisites @fn @(Map k v) ->
               typeSpec $ ListSpec Nothing mustList sz (mapSpec (sndFn @fn) $ toSimpleRepSpec kvSpec) foldSpec
     RngSet ->
       case f of
         (_ :: MapFn fn '[Map k v] (Set v))
-          | MapSpec _ _ mustList sz kvSpec _foldSpec <- ts
+          | MapSpec _ _ mustList sz kvSpec _foldSpec _ <- ts
           , Evidence <- prerequisites @fn @(Map k v) ->
               typeSpec $ SetSpec (Set.fromList mustList) (mapSpec (sndFn @fn) $ toSimpleRepSpec kvSpec) sz
 
@@ -323,5 +349,29 @@ soundSpec specx = do
       property $
         (conformsToSpec x specx)
 
-tell :: Show a => String -> a -> a
-tell s a = trace ("\n" ++ s ++ " " ++ show a) a
+_zzz :: Bool
+_zzz = conformsToSpec (Map.fromList [(-1, 0), (0, 0), (1, 0)] :: Map Int Int) rngSpec
+
+-- ====================
+{-
+smallestAcceptableSize :: NumSpec Integer -> NumSpec Integer -> NumSpec Integer
+smallestAcceptableSize (NumSpecInterval x y) (NumSpecInterval a b) = NumSpecInterval (maxL x a) (max <$> y <*> b)
+  where maxL Nothing Nothing = Nothing
+        maxL Nothing (Just x) = Just x
+        maxL (Just x) Nothing = Just x
+        maxL (Just x) (Just y) = Just(max x y)
+-}
+
+smallestAcceptableSize :: Maybe (MinValSize v) -> Maybe (MinValSize v) -> Maybe (MinValSize v)
+smallestAcceptableSize Nothing Nothing = Nothing
+smallestAcceptableSize Nothing (Just x) = Just x
+smallestAcceptableSize (Just x) Nothing = Just x
+smallestAcceptableSize (Just (MinValSize x)) (Just (MinValSize y)) = Just (MinValSize (max x y))
+
+smallestSpec :: BaseUniverse fn => Maybe (MinValSize v) -> Specification fn Integer
+smallestSpec smallest = case smallest of
+  Just (MinValSize n) -> leqSpec n
+  Nothing -> TrueSpec
+
+smallest :: Ord v => Specification fn Integer -> Maybe (MinValSize v)
+smallest TrueSpec = Nothing