From 4a0f7052cd18dfc0aaae41a2712cc7d6c356f71a Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Mon, 7 Oct 2024 14:48:01 +0200 Subject: [PATCH] Add singletonList_ and (++.) --- .../Conformance/ExecSpecRule/Conway/Base.hs | 1 - .../Constrained/Conway/LedgerTypes/Specs.hs | 2 +- .../constrained-generators/src/Constrained.hs | 4 + .../src/Constrained/Base.hs | 100 ++++++++++++++++-- .../src/Constrained/Examples/List.hs | 28 +++++ .../src/Constrained/Properties.hs | 2 + .../test/Constrained/Test.hs | 12 +++ 7 files changed, 141 insertions(+), 8 deletions(-) diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs index 2b257d9a59a..d2b0e76826a 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs +++ b/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 diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs index d403ecbc449..6c87bc00251 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/LedgerTypes/Specs.hs +++ b/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 diff --git a/libs/constrained-generators/src/Constrained.hs b/libs/constrained-generators/src/Constrained.hs index 651513b6311..9d1924737a7 100644 --- a/libs/constrained-generators/src/Constrained.hs +++ b/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_, diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs index 14ad1f8c2fb..404bd376992 100644 --- a/libs/constrained-generators/src/Constrained/Base.hs +++ b/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,6 +4486,76 @@ 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 @@ -4490,6 +4563,7 @@ instance BaseUniverse fn => Functions (ListFn fn) fn where 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 :: diff --git a/libs/constrained-generators/src/Constrained/Examples/List.hs b/libs/constrained-generators/src/Constrained/Examples/List.hs index 228a9742d7c..113a6ea1442 100644 --- a/libs/constrained-generators/src/Constrained/Examples/List.hs +++ b/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 diff --git a/libs/constrained-generators/src/Constrained/Properties.hs b/libs/constrained-generators/src/Constrained/Properties.hs index 241945165e7..0a984397151 100644 --- a/libs/constrained-generators/src/Constrained/Properties.hs +++ b/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 :: diff --git a/libs/constrained-generators/test/Constrained/Test.hs b/libs/constrained-generators/test/Constrained/Test.hs index 420327d3c72..d396c4c72d0 100644 --- a/libs/constrained-generators/test/Constrained/Test.hs +++ b/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 =