Add singletonList_ and (++.)

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

@@ -76,7 +76,6 @@ import Cardano.Ledger.Conway.Rules (
 import Cardano.Ledger.DRep (DRep (..))
 import Cardano.Ledger.PoolDistr (IndividualPoolStake (..))
 import Constrained hiding (inject)
-import Constrained.Base (fromList_)
 import Data.Bifunctor (Bifunctor (..))
 import Data.Foldable (Foldable (..))
 import qualified Data.List.NonEmpty as NE

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

@@ -54,7 +54,7 @@ import Cardano.Ledger.UMap (CompactForm (..))
 import qualified Cardano.Ledger.UMap as UMap
 import Cardano.Ledger.UTxO (UTxO (..))
 import Constrained hiding (Value)
-import Constrained.Base (Pred (..), fromList_, hasSize, rangeSize)
+import Constrained.Base (Pred (..), hasSize, rangeSize)
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Typeable

libs/constrained-generators/src/Constrained.hs

@@ -95,10 +95,14 @@ module Constrained (
   subset_,
   disjoint_,
   singleton_,
+  union_,
+  fromList_,
   elem_,
   not_,
   foldMap_,
   sum_,
+  (++.),
+  singletonList_,
   size_,
   rng_,
   dom_,

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

@@ -55,7 +55,7 @@ import Control.Monad.Identity
 import Control.Monad.Writer (Writer, runWriter, tell)
 import Data.Foldable
 import Data.Kind
-import Data.List (intersect, nub, partition, (\\))
+import Data.List (intersect, isPrefixOf, isSuffixOf, nub, partition, (\\))
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe
@@ -4458,20 +4458,23 @@ data ListFn fn args res where
     ) =>
     fn '[a] b ->
     ListFn fn '[[a]] b
-
-{- TODO add these?
-  AppendFn :: ListFn fn '[[a],[a]] [a]
-  ConsFn :: ListFn fn '[a.[a]] [a]
--}
+  SingletonList :: ListFn fn '[a] [a]
+  AppendFn :: ListFn fn '[[a], [a]] [a]
 
 deriving instance Show (ListFn fn args res)
 
 instance Typeable fn => Eq (ListFn fn args res) where
   FoldMap f == FoldMap g = cast f == Just g
+  SingletonList == SingletonList = True
+  SingletonList == _ = False
+  _ == SingletonList = False
+  AppendFn == AppendFn = True
 
 instance FunctionLike fn => FunctionLike (ListFn fn) where
   sem = \case
     FoldMap f -> adds @fn . map (sem f)
+    SingletonList -> (: [])
+    AppendFn -> (++)
 
 instance BaseUniverse fn => Functions (ListFn fn) fn where
   propagateSpecFun _ _ (ErrorSpec err) = ErrorSpec err
@@ -4483,13 +4486,84 @@ instance BaseUniverse fn => Functions (ListFn 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) (x :-> p)
     FoldMap f | NilCtx HOLE <- ctx -> typeSpec (ListSpec Nothing [] TrueSpec TrueSpec $ FoldSpec f spec)
+    SingletonList | NilCtx HOLE <- ctx -> case spec of
+      TrueSpec -> TrueSpec
+      MemberSpec xss -> MemberSpec [a | [a] <- xss]
+      TypeSpec (ListSpec _ m sz e f) cant
+        | length m > 1 ->
+            ErrorSpec $
+              NE.fromList
+                [ "Too many required elements for SingletonList: "
+                , "  " ++ show m
+                ]
+        | not $ 1 `conformsToSpec` sz ->
+            ErrorSpec $ pure $ "Size spec requires too many elements for SingletonList: " ++ show sz
+        | bad@(_ : _) <- filter (not . (`conformsToSpec` e)) m ->
+            ErrorSpec $
+              NE.fromList
+                [ "The following elements of the must spec do not conforms to the elem spec:"
+                , show bad
+                ]
+        -- There is precisely one required element in the final list, so the argumen to singletonList_ has to
+        -- be that element and we have to respect the cant and fold specs
+        | [a] <- m -> MemberSpec [a] <> notMemberSpec [a | [a] <- cant] <> reverseFoldSpec f
+        -- We have to respect the elem-spec, the can't spec, and the fold spec.
+        | otherwise -> e <> notMemberSpec [a | [a] <- cant] <> reverseFoldSpec f
+        where
+          reverseFoldSpec NoFold = TrueSpec
+          -- The single element list has to sum to something that obeys spec, i.e. `conformsToSpec (f a) spec`
+          reverseFoldSpec (FoldSpec fn spec) = propagateSpecFun fn (NilCtx HOLE) spec
+    AppendFn -> case spec of
+      TrueSpec -> TrueSpec
+      MemberSpec xss
+        | HOLE :? Value (ys :: [a]) :> Nil <- ctx
+        , Evidence <- prerequisites @fn @[a] ->
+            -- Only keep the prefixes of the elements of xss that can
+            -- give you the correct resulting list
+            MemberSpec (suffixedBy ys xss)
+        | Value (ys :: [a]) :! NilCtx HOLE <- ctx
+        , Evidence <- prerequisites @fn @[a] ->
+            -- Only keep the suffixes of the elements of xss that can
+            -- give you the correct resulting list
+            MemberSpec (prefixedBy ys xss)
+      TypeSpec ts@ListSpec {listSpecElem = e} cant
+        | HOLE :? Value (ys :: [a]) :> Nil <- ctx
+        , Evidence <- prerequisites @fn @[a]
+        , all (`conformsToSpec` e) ys ->
+            TypeSpec (alreadyHave ys ts) (suffixedBy ys cant)
+        | Value (ys :: [a]) :! NilCtx HOLE <- ctx
+        , Evidence <- prerequisites @fn @[a]
+        , all (`conformsToSpec` e) ys ->
+            TypeSpec (alreadyHave ys ts) (prefixedBy ys cant)
+      _ -> ErrorSpec $ pure "The spec given to propagateSpecFun AppendSpec is inconsistent!"
+      where
+        prefixedBy ys xss = [drop (length ys) xs | xs <- xss, ys `isPrefixOf` xs]
+        suffixedBy ys xss = [take (length xs - length ys) xs | xs <- xss, ys `isSuffixOf` xs]
+
+        alreadyHave ys (ListSpec h m sz e f) =
+          ListSpec
+            -- Reduce the hint
+            (fmap (subtract (sizeOf ys)) h)
+            -- The things in `ys` have already been added to the list, no need to
+            -- require them too
+            (m \\ ys)
+            -- Reduce the required size
+            (constrained $ \x -> (x + lit (sizeOf ys)) `satisfies` sz)
+            -- Nothing changes about what's a correct element
+            e
+            -- we have fewer things to sum now
+            (alreadyHaveFold ys f)
+
+        alreadyHaveFold _ NoFold = NoFold
+        alreadyHaveFold ys (FoldSpec fn spec) = FoldSpec fn (constrained $ \s -> app theAddFn s (foldMap_ (app fn) (lit ys)) `satisfies` spec)
 
   -- NOTE: this function over-approximates and returns a liberal spec.
   mapTypeSpec f ts = case f of
     FoldMap g ->
       constrained $ \x ->
         unsafeExists $ \x' ->
           assert (x ==. app (foldMapFn g) x') <> toPreds x' ts
+    SingletonList -> typeSpec (ListSpec Nothing [] (equalSpec 1) (typeSpec ts) NoFold)
 
 foldMapFn ::
   forall fn a b.
@@ -4502,6 +4576,12 @@ foldMapFn ::
   fn '[[a]] b
 foldMapFn f = injectFn $ FoldMap @fn f
 
+singletonListFn :: forall fn a. HasSpec fn a => fn '[a] [a]
+singletonListFn = injectFn $ SingletonList @fn
+
+appendFn :: forall fn a. HasSpec fn a => fn '[[a], [a]] [a]
+appendFn = injectFn $ AppendFn @fn
+
 -- Number functions -------------------------------------------------------
 
 addFn :: forall fn a. NumLike fn a => fn '[a, a] a
@@ -4663,6 +4743,7 @@ infixr 2 ||.
   Term fn Bool
 (||.) = app orFn
 
+infix 4 `elem_`
 elem_ ::
   forall a fn.
   HasSpec fn a =>
@@ -4834,6 +4915,13 @@ foldMap_ f = app $ foldMapFn $ toFn $ f (V v)
     toFn (V v') | Just Refl <- eqVar v v' = idFn
     toFn _ = error "foldMap_ has not been given a function of the form \\ x -> f (g ... (h x))"
 
+infixr 5 ++.
+(++.) :: HasSpec fn a => Term fn [a] -> Term fn [a] -> Term fn [a]
+(++.) = app appendFn
+
+singletonList_ :: HasSpec fn a => Term fn a -> Term fn [a]
+singletonList_ = app singletonListFn
+
 -- Language constructs ----------------------------------------------------
 
 constrained ::

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

@@ -114,3 +114,31 @@ listSumShort = constrained $ \ [var| xs |] ->
           whenTrue b $ x <=. 10000000
       ]
   ]
+
+appendSize :: Specification BaseFn ([Int], [Int])
+appendSize = constrained' $ \ [var| xs |] [var| ys |] ->
+  [ assert $ sizeOf_ xs <=. 10
+  , assert $ sizeOf_ (ys ++. xs) <=. 15
+  ]
+
+appendSingleton :: Specification BaseFn Int
+appendSingleton = constrained $ \ [var| x |] ->
+  10 `elem_` singletonList_ x ++. lit [1, 2, 3]
+
+singletonSubset :: Specification BaseFn Int
+singletonSubset = constrained $ \ [var| x |] ->
+  fromList_ (singletonList_ x) `subset_` fromList_ (lit [1, 2, 3])
+
+-- Some notable error cases that shouldn't succeed
+
+singletonErrorTooMany :: Specification BaseFn Int
+singletonErrorTooMany = constrained $ \ [var| x |] ->
+  fromList_ (lit [1, 2, 3]) `subset_` fromList_ (singletonList_ x)
+
+singletonErrorTooLong :: Specification BaseFn Int
+singletonErrorTooLong = constrained $ \ [var| x |] ->
+  2 <=. length_ (singletonList_ x)
+
+appendTooLong :: Specification BaseFn [Int]
+appendTooLong = constrained $ \ [var| xs |] ->
+  sizeOf_ (lit [1, 2, 3, 4] ++. xs) <=. 3

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

@@ -219,6 +219,8 @@ instance fn ~ BaseFn => QC.Arbitrary (TestableFn fn) where
       , TestableFn $ domFn @fn @Int @Int
       , TestableFn $ fromListFn @fn @Int
       , TestableFn $ lookupFn @fn @Int @Int
+      , TestableFn $ singletonListFn @fn @Int
+      , TestableFn $ appendFn @fn @Int
       ]
 
 prop_mapSpec ::

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

@@ -123,6 +123,9 @@ tests nightly =
     -- TODO: turn this on when we bump quickcheck version
     -- testSpec "listSumShort" listSumShort
     testSpec "existsUnfree" existsUnfree
+    testSpec "appendSize" appendSize
+    testSpecNoShrink "appendSingleton" appendSingleton
+    testSpec "singletonSubset" singletonSubset
     -- TODO: double shrinking
     testSpecNoShrink "reifyYucky" reifyYucky
     testSpec "fixedRange" fixedRange
@@ -200,6 +203,15 @@ negativeTests =
               (pure "You can't constrain the variable introduced by reify as its already decided")
               $ reify x id
               $ \y -> y ==. 10
+    prop "singletonErrorTooMany" $
+      expectFailure $
+        prop_complete singletonErrorTooMany
+    prop "singletonErrorTooLong" $
+      expectFailure $
+        prop_complete singletonErrorTooLong
+    prop "appendTooLong" $
+      expectFailure $
+        prop_complete appendTooLong
 
 numberyTests :: Spec
 numberyTests =