From eca243fad90430677e249aeaa2c9d99c1391b204 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 22 Apr 2025 22:42:47 +1000 Subject: [PATCH 01/15] implement LIST.range in legacy kore --- kore/src/Kore/Builtin/List.hs | 32 +++++++++++++++++++---- kore/src/Kore/Builtin/List/List.hs | 4 +++ kore/test/Test/Kore/Builtin/Definition.hs | 10 +++++++ kore/test/Test/Kore/Builtin/List.hs | 31 ++++++++++++++++++++++ 4 files changed, 72 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Builtin/List.hs b/kore/src/Kore/Builtin/List.hs index 68be15e031..ae53a819bc 100644 --- a/kore/src/Kore/Builtin/List.hs +++ b/kore/src/Kore/Builtin/List.hs @@ -211,6 +211,10 @@ symbolVerifiers = ( updateAllKey , Builtin.verifySymbol assertSort [assertSort, Int.assertSort, assertSort] ) + , + ( rangeKey + , Builtin.verifySymbol assertSort [assertSort, Int.assertSort, Int.assertSort] + ) ] {- | Abort function evaluation if the argument is not a List domain value. @@ -336,17 +340,17 @@ evalSize _ _ _ = Builtin.wrongArity sizeKey evalMake :: Builtin.Function evalMake _ resultSort [_len, value] = do - _len <- fromInteger <$> Int.expectBuiltinInt getKey _len + _len <- fromInteger <$> Int.expectBuiltinInt makeKey _len if _len >= 0 then lift $ returnList resultSort (Seq.replicate _len value) else return (Pattern.bottomOf resultSort) -evalMake _ _ _ = Builtin.wrongArity sizeKey +evalMake _ _ _ = Builtin.wrongArity makeKey evalUpdateAll :: Builtin.Function evalUpdateAll _ resultSort [_list1, _ix, _list2] = do - _list1 <- expectBuiltinList getKey _list1 - _list2 <- expectBuiltinList getKey _list2 - _ix <- fromInteger <$> Int.expectBuiltinInt getKey _ix + _list1 <- expectBuiltinList updateAllKey _list1 + _list2 <- expectBuiltinList updateAllKey _list2 + _ix <- fromInteger <$> Int.expectBuiltinInt updateAllKey _ix let len1 = Seq.length _list1 len2 = Seq.length _list2 result @@ -360,6 +364,23 @@ evalUpdateAll _ resultSort [_list1, _ix, _list2] = do lift result evalUpdateAll _ _ _ = Builtin.wrongArity updateKey +evalRange :: Builtin.Function +evalRange _ resultSort [list, fromFront, fromBack] = do + baseList <- expectBuiltinList rangeKey list + frontDrop <- fromInteger <$> Int.expectBuiltinInt rangeKey fromFront + backDrop <- fromInteger <$> Int.expectBuiltinInt rangeKey fromBack + let len = Seq.length baseList + bottom = return $ Pattern.bottomOf resultSort + result + | frontDrop < 0 = bottom + | backDrop < 0 = bottom + | len < frontDrop + backDrop = bottom + | otherwise = + let size = len - frontDrop - backDrop + in returnList resultSort (Seq.take size $ Seq.drop frontDrop baseList) + lift result +evalRange _ _ _ = Builtin.wrongArity rangeKey + -- | Implement builtin function evaluation. builtinFunctions :: Text -> Maybe BuiltinAndAxiomSimplifier builtinFunctions key @@ -372,6 +393,7 @@ builtinFunctions key | key == sizeKey = Just $ Builtin.functionEvaluator evalSize | key == makeKey = Just $ Builtin.functionEvaluator evalMake | key == updateAllKey = Just $ Builtin.functionEvaluator evalUpdateAll + | key == rangeKey = Just $ Builtin.functionEvaluator evalRange | otherwise = Nothing data FirstElemVarData = FirstElemVarData diff --git a/kore/src/Kore/Builtin/List/List.hs b/kore/src/Kore/Builtin/List/List.hs index 8be82ac416..ff73634d61 100644 --- a/kore/src/Kore/Builtin/List/List.hs +++ b/kore/src/Kore/Builtin/List/List.hs @@ -25,6 +25,7 @@ module Kore.Builtin.List.List ( sizeKey, makeKey, updateAllKey, + rangeKey, ) where import Data.Sequence ( @@ -165,3 +166,6 @@ makeKey = "LIST.make" updateAllKey :: IsString s => s updateAllKey = "LIST.updateAll" + +rangeKey :: IsString s => s +rangeKey = "LIST.range" diff --git a/kore/test/Test/Kore/Builtin/Definition.hs b/kore/test/Test/Kore/Builtin/Definition.hs index c84db24474..8a3a9a7a3d 100644 --- a/kore/test/Test/Kore/Builtin/Definition.hs +++ b/kore/test/Test/Kore/Builtin/Definition.hs @@ -412,6 +412,9 @@ updateAllListSymbol :: Internal.Symbol updateAllListSymbol = builtinSymbol "updateAllList" listSort [listSort, intSort, listSort] & hook "LIST.updateAll" +rangeListSymbol :: Internal.Symbol +rangeListSymbol = + hook "LIST.range" $ builtinSymbol "rangeList" listSort [listSort, intSort, intSort] unitList :: TermLike RewritingVariableName unitList = mkApplySymbol unitListSymbol [] elementList :: @@ -453,6 +456,12 @@ updateAllList :: TermLike RewritingVariableName -> TermLike RewritingVariableName updateAllList l1 ix l2 = mkApplySymbol updateAllListSymbol [l1, ix, l2] +rangeList :: + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + TermLike RewritingVariableName +rangeList l start end = mkApplySymbol rangeListSymbol [l, start, end] -- ** Map unitMapSymbol :: Internal.Symbol unitMapSymbol = builtinSymbol "unitMap" mapSort [] & hook "MAP.unit" @@ -1539,6 +1548,7 @@ listModule = , hookedSymbolDecl sizeListSymbol , hookedSymbolDecl makeListSymbol , hookedSymbolDecl updateAllListSymbol + , hookedSymbolDecl rangeListSymbol , -- A second builtin List sort, to confuse 'asPattern'. listSortDecl2 , hookedSymbolDecl unitList2Symbol diff --git a/kore/test/Test/Kore/Builtin/List.hs b/kore/test/Test/Kore/Builtin/List.hs index 6bf29a769d..6ba37fe23b 100644 --- a/kore/test/Test/Kore/Builtin/List.hs +++ b/kore/test/Test/Kore/Builtin/List.hs @@ -17,6 +17,7 @@ module Test.Kore.Builtin.List ( test_updateAll, hprop_unparse, test_size, + test_range, -- asInternal, asTermLike, @@ -481,6 +482,36 @@ test_updateAll = where original = asInternal . fmap mkInt $ Seq.fromList [1, 2, 3] +test_range :: [TestTree] +test_range = + [ testCaseWithoutSMT "range([1, 2, 3], 4, 5) === \\bottom" $ + assertBottom =<< evaluateTerm (rangeList onetwothree (mkInt 4) (mkInt 5)) + , testCaseWithoutSMT "range([1, 2, 3], -1, 1) === \\bottom" $ + assertBottom =<< evaluateTerm (rangeList onetwothree (mkInt $ negate 1) (mkInt 1)) + , testCaseWithoutSMT "range([1, 2, 3], 1, -1) === \\bottom" $ + assertBottom =<< evaluateTerm (rangeList onetwothree (mkInt 1) (mkInt $ negate 1)) + , testCaseWithoutSMT "range([1, 2, 3], 2, 2) === \\bottom" $ + assertBottom =<< evaluateTerm (rangeList onetwothree (mkInt 2) (mkInt 2)) + , testCaseWithoutSMT "range([1, 2, 3], 0, 0) === [1, 2, 3]" $ do + result <- evaluateTerm (rangeList onetwothree (mkInt 0) (mkInt 0)) + assertEqual' "" (OrPattern.fromTermLike onetwothree) result + , testCaseWithoutSMT "range([1, 2, 3], 1, 1) === [2]" $ do + result <- evaluateTerm (rangeList onetwothree (mkInt 1) (mkInt 1)) + let expected = asInternal . fmap mkInt $ Seq.singleton 2 + assertEqual' "" (OrPattern.fromTermLike expected) result + , testCaseWithoutSMT "range([1, 2, 3], 0, 3) === []" $ do + result <- evaluateTerm (rangeList onetwothree (mkInt 0) (mkInt 3)) + let expected = asInternal Seq.empty + assertEqual' "" (OrPattern.fromTermLike expected) result + , testCaseWithoutSMT "range([1, 2, 3], 2, 1) === []" $ do + result <- evaluateTerm (rangeList onetwothree (mkInt 2) (mkInt 1)) + let expected = asInternal Seq.empty + assertEqual' "" (OrPattern.fromTermLike expected) result + ] + where + onetwothree = asInternal . fmap mkInt $ Seq.fromList [1 .. 3] + assertBottom = assertEqual' "expected bottom" OrPattern.bottom + -- | Specialize 'List.asPattern' to the builtin sort 'listSort'. asTermLike :: InternalVariable variable => From 30e74ef98a9a1708c4145295d4a4b00807b9e2cd Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 15 May 2025 22:16:39 +1000 Subject: [PATCH 02/15] WIP implementing most list hooks in booster --- booster/library/Booster/Builtin/LIST.hs | 109 +++++++++++++++++++++++- 1 file changed, 108 insertions(+), 1 deletion(-) diff --git a/booster/library/Booster/Builtin/LIST.hs b/booster/library/Booster/Builtin/LIST.hs index 2f67395e95..76533ce079 100644 --- a/booster/library/Booster/Builtin/LIST.hs +++ b/booster/library/Booster/Builtin/LIST.hs @@ -18,6 +18,7 @@ import Data.Map (Map) import Data.Map qualified as Map import Booster.Builtin.Base +import Booster.Builtin.BOOL (boolTerm) import Booster.Builtin.INT import Booster.Definition.Attributes.Base ( KCollectionSymbolNames (..), @@ -29,10 +30,49 @@ builtinsLIST :: Map ByteString BuiltinFunction builtinsLIST = Map.mapKeys ("LIST." <>) $ Map.fromList - [ "get" ~~> listGetHook + [ "concat" ~~> listConcatHook + , "element" ~~> listElementHook + , "get" ~~> listGetHook + , "in" ~~> listInHook + , "make" ~~> listMakeHook + , "range" ~~> listRangeHook , "size" ~~> listSizeHook + , "unit" ~~> listUnitHook + , "update" ~~> listUpdateHook ] +-- | concatenate two lists +listConcatHook :: BuiltinFunction +listConcatHook [KList def1 heads1 rest1, KList def2 heads2 rest2] + -- see Booster.Pattern.Base.internaliseKList + | def1 /= def2 = + pure Nothing -- actually a compiler error + | Nothing <- rest1 + , Nothing <- rest2 = + pure $ Just $ KList def1 (heads1 <> heads2) Nothing + | Nothing <- rest1 = + pure $ Just $ KList def2 (heads1 <> heads2) rest2 + | Nothing <- rest2 + , Just (mid1, tails1) <- rest1 = + pure $ Just $ KList def1 heads1 $ Just (mid1, tails1 <> heads2) + | otherwise = -- opaque middle in both lists, unable to simplify + pure Nothing +listConcatHook [KList def1 heads Nothing, other] = + pure $ Just $ KList def1 heads (Just (other, [])) +listConcatHook [other, KList def2 heads Nothing] = + pure $ Just $ KList def2 [] (Just (other, heads)) +listConcatHook [_, _] = + pure Nothing +listConcatHook other = + arityError "LIST.concat" 2 other + +-- | create a singleton list from a given element +listElementHook :: BuiltinFunction +listElementHook [elem'] = + pure $ Just $ KList kItemListDef [elem'] Nothing +listElementHook other = + arityError "LIST.element" 1 other + listGetHook :: BuiltinFunction listGetHook [KList _ heads mbRest, intArg] = let headLen = length heads @@ -67,6 +107,52 @@ listGetHook [_other, _] = listGetHook args = arityError "LIST.get" 2 args +listInHook :: BuiltinFunction +listInHook [e, KList _ heads rest] = + case rest of + Nothing -> pure $ Just $ boolTerm (e `elem` heads) + Just (_mid, tails) + | e `elem` tails -> + pure $ Just $ boolTerm True + | otherwise -> -- could be in opaque _mid + pure Nothing +listInHook args = + arityError "LIST.in" 2 args + +listMakeHook :: BuiltinFunction +listMakeHook [intArg, value] = + case fromIntegral <$> readIntTerm intArg of + Nothing -> + intArg `shouldHaveSort` "SortInt" >> pure Nothing + Just len -> + pure $ Just $ KList kItemListDef (replicate len value) Nothing +listMakeHook args = + arityError "LIST.make" 2 args + +listRangeHook :: BuiltinFunction +listRangeHook [KList def heads rest, fromFront, fromBack] = + case (fromIntegral <$> readIntTerm fromFront, fromIntegral <$> readIntTerm fromBack) of + (Nothing, _) -> + fromFront `shouldHaveSort` "SortInt" >> pure Nothing + (_, Nothing) -> + fromBack `shouldHaveSort` "SortInt" >> pure Nothing + (Just frontDrop, Just backDrop) + | frontDrop < 0 -> pure Nothing -- bottom + | backDrop < 0 -> pure Nothing -- bottom + | otherwise -> do + let targetLen = length heads - frontDrop - backDrop + case rest of + Just _ -> pure Nothing -- opaque middle, cannot drop from back + Nothing + | targetLen < 0 -> + pure Nothing -- bottom + | otherwise -> do + let part = + take targetLen $ drop frontDrop heads + pure $ Just $ KList def part Nothing +listRangeHook args = + arityError "LIST.range" 3 args + listSizeHook :: BuiltinFunction listSizeHook = \case [KList _ heads Nothing] -> @@ -78,6 +164,27 @@ listSizeHook = \case moreArgs -> arityError "LIST.size" 1 moreArgs +listUnitHook :: BuiltinFunction +listUnitHook [] = pure $ Just $ KList kItemListDef [] Nothing +listUnitHook args = + arityError "LIST.unit" 0 args + +listUpdateHook :: BuiltinFunction +listUpdateHook [KList def heads rest, intArg, value] = + case fromIntegral <$> readIntTerm intArg of + Nothing -> + intArg `shouldHaveSort` "SortInt" >> pure Nothing + Just idx + | idx < 0 -> + pure Nothing -- bottom + | idx >= length heads -> + pure Nothing -- indeterminate + | otherwise -> do + let ~(front, _target : back) = splitAt idx heads + pure $ Just $ KList def (front <> (value : back)) rest +listUpdateHook args = + arityError "LIST.update" 3 args + kItemListDef :: KListDefinition kItemListDef = KListDefinition From 04876da6dc3e97c75848af9dfd780d9c6260a086 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 19 May 2025 14:08:54 +1000 Subject: [PATCH 03/15] Formatting for new hooks --- booster/library/Booster/Builtin/LIST.hs | 49 ++++++++++++------------- 1 file changed, 24 insertions(+), 25 deletions(-) diff --git a/booster/library/Booster/Builtin/LIST.hs b/booster/library/Booster/Builtin/LIST.hs index 76533ce079..1a144611a8 100644 --- a/booster/library/Booster/Builtin/LIST.hs +++ b/booster/library/Booster/Builtin/LIST.hs @@ -17,8 +17,8 @@ import Data.ByteString.Char8 (ByteString, pack) import Data.Map (Map) import Data.Map qualified as Map -import Booster.Builtin.Base import Booster.Builtin.BOOL (boolTerm) +import Booster.Builtin.Base import Booster.Builtin.INT import Booster.Definition.Attributes.Base ( KCollectionSymbolNames (..), @@ -46,23 +46,22 @@ listConcatHook :: BuiltinFunction listConcatHook [KList def1 heads1 rest1, KList def2 heads2 rest2] -- see Booster.Pattern.Base.internaliseKList | def1 /= def2 = - pure Nothing -- actually a compiler error + pure Nothing -- actually a compiler error | Nothing <- rest1 , Nothing <- rest2 = - pure $ Just $ KList def1 (heads1 <> heads2) Nothing + pure $ Just $ KList def1 (heads1 <> heads2) Nothing | Nothing <- rest1 = - pure $ Just $ KList def2 (heads1 <> heads2) rest2 + pure $ Just $ KList def2 (heads1 <> heads2) rest2 | Nothing <- rest2 , Just (mid1, tails1) <- rest1 = - pure $ Just $ KList def1 heads1 $ Just (mid1, tails1 <> heads2) - | otherwise = -- opaque middle in both lists, unable to simplify - pure Nothing + pure $ Just $ KList def1 heads1 $ Just (mid1, tails1 <> heads2) + | otherwise -- opaque middle in both lists, unable to simplify + = + pure Nothing listConcatHook [KList def1 heads Nothing, other] = pure $ Just $ KList def1 heads (Just (other, [])) listConcatHook [other, KList def2 heads Nothing] = pure $ Just $ KList def2 [] (Just (other, heads)) -listConcatHook [_, _] = - pure Nothing listConcatHook other = arityError "LIST.concat" 2 other @@ -113,9 +112,9 @@ listInHook [e, KList _ heads rest] = Nothing -> pure $ Just $ boolTerm (e `elem` heads) Just (_mid, tails) | e `elem` tails -> - pure $ Just $ boolTerm True + pure $ Just $ boolTerm True | otherwise -> -- could be in opaque _mid - pure Nothing + pure Nothing listInHook args = arityError "LIST.in" 2 args @@ -140,16 +139,16 @@ listRangeHook [KList def heads rest, fromFront, fromBack] = | frontDrop < 0 -> pure Nothing -- bottom | backDrop < 0 -> pure Nothing -- bottom | otherwise -> do - let targetLen = length heads - frontDrop - backDrop - case rest of - Just _ -> pure Nothing -- opaque middle, cannot drop from back - Nothing - | targetLen < 0 -> - pure Nothing -- bottom - | otherwise -> do - let part = - take targetLen $ drop frontDrop heads - pure $ Just $ KList def part Nothing + let targetLen = length heads - frontDrop - backDrop + case rest of + Just _ -> pure Nothing -- opaque middle, cannot drop from back + Nothing + | targetLen < 0 -> + pure Nothing -- bottom + | otherwise -> do + let part = + take targetLen $ drop frontDrop heads + pure $ Just $ KList def part Nothing listRangeHook args = arityError "LIST.range" 3 args @@ -176,12 +175,12 @@ listUpdateHook [KList def heads rest, intArg, value] = intArg `shouldHaveSort` "SortInt" >> pure Nothing Just idx | idx < 0 -> - pure Nothing -- bottom + pure Nothing -- bottom | idx >= length heads -> - pure Nothing -- indeterminate + pure Nothing -- indeterminate | otherwise -> do - let ~(front, _target : back) = splitAt idx heads - pure $ Just $ KList def (front <> (value : back)) rest + let ~(front, _target : back) = splitAt idx heads + pure $ Just $ KList def (front <> (value : back)) rest listUpdateHook args = arityError "LIST.update" 3 args From 2878defd1fa00e06c9ac578d8d719cdb4f621bcc Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 19 May 2025 14:09:13 +1000 Subject: [PATCH 04/15] WIP unit tests for new list hooks --- booster/unit-tests/Test/Booster/Builtin.hs | 152 ++++++++++++++++++--- 1 file changed, 133 insertions(+), 19 deletions(-) diff --git a/booster/unit-tests/Test/Booster/Builtin.hs b/booster/unit-tests/Test/Booster/Builtin.hs index 8ebc4d1082..b591eb2610 100644 --- a/booster/unit-tests/Test/Booster/Builtin.hs +++ b/booster/unit-tests/Test/Booster/Builtin.hs @@ -39,8 +39,7 @@ import Test.Booster.Fixture as Fixture test_builtins :: [TestTree] test_builtins = [ testIntHooks - , testListSizeHooks - , testListGetHooks + , testListHooks , testMapHooks ] @@ -82,10 +81,111 @@ testIntHooks = assertException $ f [dv_a] assertException $ f [dv_a, dv_a, dv_a] -testListSizeHooks :: TestTree -testListSizeHooks = +testListHooks :: TestTree +testListHooks = testGroup - "LIST.size hooks" + "LIST hooks" + [ testListArityChecks + , testListConcatHook + , testListSizeHook + , testListGetHook + , testListUpdateHook + ] + +-- helpers +listOfThings :: Int -> Term +listOfThings n = + let things = map numDV [1 .. n] + in KList Fixture.testKListDef things Nothing + +numDV :: Int -> Term +numDV n = dv Fixture.someSort $ BS.pack $ show n + +evalHook :: MonadFail m => BS.ByteString -> [Term] -> m (Maybe Term) +evalHook name args = either (fail . show) pure $ runExcept $ runHook name args + +testListArityChecks :: TestTree +testListArityChecks = + testGroup + "Arity of list hooks is checked" + [ testCase "LIST.concat: 2 list arg.s" $ do + assertException "LIST.concat" [] + assertException "LIST.concat" [[trm| X:SortList |]] + assertException "LIST.concat" $ replicate 3 [trm| X:SortList |] + , testCase "LIST.size: list arg." $ do + assertException "LIST.size" [] + assertException "LIST.size" $ replicate 2 [trm| X:SortList |] + , testCase "LIST.get: list and int arg.s" $ do + assertException "LIST.get" [] + assertException "LIST.get" [[trm| X:SortList |]] + assertException "LIST.get" $ replicate 3 [trm| X:SortList{} |] + , testCase "LIST.update: list, index, and element" $ do + assertException "LIST.update" [] + assertException "LIST.update" [[trm| X:SortList |]] + assertException "LIST.update" $ replicate 2 [trm| X:SortList{} |] + assertException "LIST.update" $ replicate 4 [trm| X:SortList{} |] + ] + where + assertException name = + assertBool "Unexpected success" . isLeft . runExcept . runHook name + +testListConcatHook :: TestTree +testListConcatHook = + testGroup + "LIST.concat hook" + [ testCase "LIST.concat on two empty lists" $ do + let empty = listOfThings 0 + result <- evalHook "LIST.concat" [empty, empty] + Just empty @=? result + , testProperty "LIST.concat with an empty list argument" . property $ do + l <- forAll smallNat + let aList = listOfThings l + empty = listOfThings 0 + resultR <- evalHook "LIST.concat" [aList, empty] + Just aList === resultR + resultL <- evalHook "LIST.concat" [empty, aList] + Just aList === resultL + , testProperty "LIST.concat with concrete lists" . property $ do + l1 <- forAll smallNat + l2 <- forAll smallNat + let list1 = listOfThings l1 + list2 = listOfThings l2 + expected = map numDV $ [1 .. l1] <> [1 .. l2] + result <- evalHook "LIST.concat" [list1, list2] + Just (KList Fixture.testKListDef expected Nothing) === result + , testProperty "LIST.concat with one opaque middle term" . property $ do + l1 <- forAll smallNat + l1t <- forAll smallNat + l2 <- forAll smallNat + let heads1 = map numDV [1 .. l1] + tail1 = Just ([trm| M1:SortList |], map numDV [1 .. l1t]) + heads2 = map numDV [1 .. l2] + list1 = KList Fixture.testKListDef heads1 tail1 + list2 = KList Fixture.testKListDef heads2 Nothing + result <- evalHook "LIST.concat" [list1, list2] + let expectedTail = Just ([trm| M1:SortList |], map numDV $ [1 .. l1t] <> [1 .. l2]) + Just (KList Fixture.testKListDef heads1 expectedTail) === result + result2 <- evalHook "LIST.concat" [list2, list1] + Just (KList Fixture.testKListDef (heads2 <> heads1) tail1) === result2 + , testProperty "LIST.concat with two opaque middle terms: indeterminate" . property $ do + l1 <- forAll smallNat + l1t <- forAll smallNat + l2 <- forAll smallNat + l2t <- forAll smallNat + let list1 = + KList Fixture.testKListDef (map numDV [1 .. l1]) $ + Just ([trm| M1:SortList |], map numDV [1 .. l1t]) + let list2 = + KList Fixture.testKListDef (map numDV [1 .. l2]) $ + Just ([trm| M2:SortList |], map numDV [1 .. l2t]) + result <- evalHook "LIST.concat" [list1, list2] + Nothing === result + ] + +testListSizeHook :: TestTree +testListSizeHook = + testGroup + "LIST.size hook" [ testProperty "LIST.size on concrete lists" . property $ do l <- forAll smallNat let aList = @@ -99,25 +199,15 @@ testListSizeHooks = Just ([trm| INIT:SortList|], replicate l [trm| \dv{SomeSort{}}("thing")|]) result <- evalEither $ runExcept $ hook [aList] Nothing === result - , testCase "LIST.size arity is checked" $ do - let assertException = assertBool "Unexpected success" . isLeft . runExcept - assertException $ hook [] - assertException $ hook $ replicate 2 [trm| X:SortList{} |] - assertException $ hook $ replicate 3 [trm| X:SortList{} |] ] where hook = runHook "LIST.size" -testListGetHooks :: TestTree -testListGetHooks = +testListGetHook :: TestTree +testListGetHook = testGroup - "LIST.get hooks" - [ testCase "LIST.get arity is checked" $ do - let assertException = assertBool "Unexpected success" . isLeft . runExcept - assertException $ hook [] - assertException $ hook [[trm| X:SortList{} |]] - assertException $ hook $ replicate 3 [trm| X:SortList{} |] - , testProperty "LIST.get with empty lists has no result" . property $ do + "LIST.get hook" + [ testProperty "LIST.get with empty lists has no result" . property $ do i <- forAll $ Gen.int (Range.constant (-42) 42) let iTerm = Builtin.intTerm $ fromIntegral i result <- evalEither $ runExcept $ hook [aList [] Nothing, iTerm] @@ -202,6 +292,30 @@ testListGetHooks = -- FIXME strictly-speaking, we would need injections to KItem here mkDV = dv someSort . BS.pack . show +testListUpdateHook :: TestTree +testListUpdateHook = + testGroup + "LIST.update hook" + [ testProperty "LIST.update within concrete head of a list" . property $ do + l <- forAll $ between1And 42 + i <- forAll $ between0And (l - 1) + let list = listOfThings l + thing = [trm| \dv{SomeSort}("thing") |] + result <- evalHook "LIST.update" [list, Builtin.intTerm (fromIntegral i), thing] + let expectedHeads = map numDV [1 .. i] <> [thing] <> map numDV [i + 2 .. l] + Just (KList Fixture.testKListDef expectedHeads Nothing) === result + , testProperty "LIST.update outside length of concrete head of a list" . property $ do + l <- forAll smallNat + i <- forAll smallNat + let list = + KList Fixture.testKListDef (map numDV [1 .. l]) $ + Just ([trm| X:SortList |], []) + thing = [trm| \dv{SomeSort}("thing") |] + idxTerm = Builtin.intTerm $ fromIntegral $ l + i + result <- evalHook "LIST.update" [list, idxTerm, thing] + Nothing === result + ] + testMapHooks :: TestTree testMapHooks = testGroup From 36643c1f473115f5553bc8681be915b8af4ed17c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 19 May 2025 16:14:37 +1000 Subject: [PATCH 05/15] refactor listUpdateHook to avoid an incomplete match --- booster/library/Booster/Builtin/LIST.hs | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/booster/library/Booster/Builtin/LIST.hs b/booster/library/Booster/Builtin/LIST.hs index 1a144611a8..6012e5e6e5 100644 --- a/booster/library/Booster/Builtin/LIST.hs +++ b/booster/library/Booster/Builtin/LIST.hs @@ -176,11 +176,14 @@ listUpdateHook [KList def heads rest, intArg, value] = Just idx | idx < 0 -> pure Nothing -- bottom - | idx >= length heads -> - pure Nothing -- indeterminate - | otherwise -> do - let ~(front, _target : back) = splitAt idx heads - pure $ Just $ KList def (front <> (value : back)) rest + | otherwise -> + case splitAt idx heads of + (front, _target : back) -> + pure $ Just $ KList def (front <> (value : back)) rest + (_heads, []) -> + -- idx >= length heads, indeterminate + pure Nothing + listUpdateHook args = arityError "LIST.update" 3 args From b31d5d780d66ef8da3fee94f86297c24c13e27c7 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 19 May 2025 16:39:59 +1000 Subject: [PATCH 06/15] refactor list hook tests to use single helpers --- booster/library/Booster/Builtin/LIST.hs | 1 - booster/unit-tests/Test/Booster/Builtin.hs | 54 +++++++++------------- 2 files changed, 21 insertions(+), 34 deletions(-) diff --git a/booster/library/Booster/Builtin/LIST.hs b/booster/library/Booster/Builtin/LIST.hs index 6012e5e6e5..49545a25b3 100644 --- a/booster/library/Booster/Builtin/LIST.hs +++ b/booster/library/Booster/Builtin/LIST.hs @@ -183,7 +183,6 @@ listUpdateHook [KList def heads rest, intArg, value] = (_heads, []) -> -- idx >= length heads, indeterminate pure Nothing - listUpdateHook args = arityError "LIST.update" 3 args diff --git a/booster/unit-tests/Test/Booster/Builtin.hs b/booster/unit-tests/Test/Booster/Builtin.hs index b591eb2610..6841a2290b 100644 --- a/booster/unit-tests/Test/Booster/Builtin.hs +++ b/booster/unit-tests/Test/Booster/Builtin.hs @@ -98,8 +98,10 @@ listOfThings n = let things = map numDV [1 .. n] in KList Fixture.testKListDef things Nothing +-- wrap an Int into an injection to KItem here numDV :: Int -> Term -numDV n = dv Fixture.someSort $ BS.pack $ show n +numDV n = + Fixture.inj Fixture.someSort Fixture.kItemSort $ dv Fixture.someSort $ BS.pack $ show n evalHook :: MonadFail m => BS.ByteString -> [Term] -> m (Maybe Term) evalHook name args = either (fail . show) pure $ runExcept $ runHook name args @@ -190,18 +192,16 @@ testListSizeHook = l <- forAll smallNat let aList = KList Fixture.testKListDef (replicate l [trm| \dv{SomeSort{}}("thing")|]) Nothing - result <- evalEither $ runExcept $ hook [aList] + result <- evalHook "LIST.size" [aList] Just (Builtin.intTerm (fromIntegral l)) === result , testProperty "LIST.size on symbolic lists has no result" . property $ do l <- forAll $ between1And 5 let aList = KList Fixture.testKListDef [] $ Just ([trm| INIT:SortList|], replicate l [trm| \dv{SomeSort{}}("thing")|]) - result <- evalEither $ runExcept $ hook [aList] + result <- evalHook "LIST.size" [aList] Nothing === result ] - where - hook = runHook "LIST.size" testListGetHook :: TestTree testListGetHook = @@ -210,33 +210,30 @@ testListGetHook = [ testProperty "LIST.get with empty lists has no result" . property $ do i <- forAll $ Gen.int (Range.constant (-42) 42) let iTerm = Builtin.intTerm $ fromIntegral i - result <- evalEither $ runExcept $ hook [aList [] Nothing, iTerm] + result <- evalHook "LIST.get" [aList [] Nothing, iTerm] Nothing === result , -- positive index testProperty "LIST.get with idx >= 0 on concrete lists" . property $ do l <- forAll smallNat i <- forAll $ between0And l let iTerm = Builtin.intTerm $ fromIntegral i - result <- evalEither $ runExcept $ hook [aList [0 .. l] Nothing, iTerm] - Just (mkDV i) === result + result <- evalHook "LIST.get" [aList [0 .. l] Nothing, iTerm] + Just (numDV i) === result , testProperty "LIST.get with idx >= 0 on list with symbolic tail" . property $ do l <- forAll smallNat i <- forAll $ between0And l let iTerm = Builtin.intTerm $ fromIntegral i result <- - evalEither . runExcept $ - hook [aList [0 .. l] (Just ([trm|X:SortList|], [])), iTerm] - Just (mkDV i) === result + evalHook "LIST.get" [aList [0 .. l] (Just ([trm|X:SortList|], [])), iTerm] + Just (numDV i) === result , testProperty "List.get with idx >= 0 where concrete head too short" . property $ do l <- forAll smallNat delta <- forAll $ between1And 42 let iTerm = Builtin.intTerm $ fromIntegral (l + delta) result <- - evalEither . runExcept $ - hook [aList [0 .. l] Nothing, iTerm] + evalHook "LIST.get" [aList [0 .. l] Nothing, iTerm] result2 <- - evalEither . runExcept $ - hook [aList [0 .. l] (Just ([trm|X:SortList|], [])), iTerm] + evalHook "LIST.get" [aList [0 .. l] (Just ([trm|X:SortList|], [])), iTerm] Nothing === result Nothing === result2 , testProperty "LIST.get with idx >= 0 on list with symbolic head" . property $ do @@ -244,33 +241,30 @@ testListGetHook = i <- forAll $ between0And l let symList = aList [] $ Just ([trm| X:SortList|], [0 .. l]) iTerm = Builtin.intTerm $ fromIntegral i - result <- evalEither $ runExcept $ hook [symList, iTerm] + result <- evalHook "LIST.get" [symList, iTerm] Nothing === result , -- negative indexes testProperty "LIST.get with idx < 0 on concrete lists" . property $ do l <- forAll smallNat i <- forAll $ between1And (l + 1) let iTerm = Builtin.intTerm $ fromIntegral $ negate i - result <- evalEither $ runExcept $ hook [aList [0 .. l] Nothing, iTerm] - Just (mkDV (l + 1 - i)) === result + result <- evalHook "LIST.get" [aList [0 .. l] Nothing, iTerm] + Just (numDV (l + 1 - i)) === result , testProperty "LIST.get with idx < 0 on list with symbolic tail" . property $ do l <- forAll smallNat i <- forAll $ between1And (l + 1) let iTerm = Builtin.intTerm $ fromIntegral $ negate i result <- - evalEither . runExcept $ - hook [aList [0 .. l] (Just ([trm|X:SortList|], [])), iTerm] + evalHook "LIST.get" [aList [0 .. l] (Just ([trm|X:SortList|], [])), iTerm] Nothing === result , testProperty "List.get with idx < 0 where concrete tail too short" . property $ do l <- forAll smallNat delta <- forAll $ between1And 42 let iTerm = Builtin.intTerm $ fromIntegral $ negate (l + 1 + delta) result <- - evalEither . runExcept $ - hook [aList [] (Just ([trm|X:SortList|], [0 .. l])), iTerm] + evalHook "LIST.get" [aList [] (Just ([trm|X:SortList|], [0 .. l])), iTerm] result2 <- - evalEither . runExcept $ - hook [aList [0 .. l] (Just ([trm|X:SortList|], [0 .. l])), iTerm] + evalHook "LIST.get" [aList [0 .. l] (Just ([trm|X:SortList|], [0 .. l])), iTerm] Nothing === result Nothing === result2 , testProperty "LIST.get on list with symbolic head, concrete tail" . property $ do @@ -278,19 +272,13 @@ testListGetHook = i <- forAll $ between1And (l + 1) let iTerm = Builtin.intTerm $ fromIntegral $ negate i result <- - evalEither . runExcept $ - hook [aList [] $ Just ([trm| X:SortList|], [0 .. l]), iTerm] - Just (mkDV (l + 1 - i)) === result + evalHook "LIST.get" [aList [] $ Just ([trm| X:SortList|], [0 .. l]), iTerm] + Just (numDV (l + 1 - i)) === result ] where - hook = runHook "LIST.get" - aList :: [Int] -> Maybe (Term, [Int]) -> Term aList heads mbTail = - KList Fixture.testKListDef (map mkDV heads) (fmap (second $ map mkDV) mbTail) - - -- FIXME strictly-speaking, we would need injections to KItem here - mkDV = dv someSort . BS.pack . show + KList Fixture.testKListDef (map numDV heads) (fmap (second $ map numDV) mbTail) testListUpdateHook :: TestTree testListUpdateHook = From 87ce11f9c87c9b331480225d91678e9da06cf9f2 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 19 May 2025 19:43:31 +1000 Subject: [PATCH 07/15] enable list matching for simplifications in matching module --- booster/library/Booster/Pattern/Match.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 9aa409613f..1fbc9d31c8 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -246,7 +246,6 @@ match1 _ t1@KList{} t2@DomainValue{} match1 Eval t1@KList{} t2@Injection{} = addIndeterminate t1 t2 match1 _ t1@KList{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@KList{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 Eval t1@KList{} t2@KList{} = addIndeterminate t1 t2 match1 _ t1@(KList def1 heads1 rest1) t2@(KList def2 heads2 rest2) = if def1 == def2 then matchLists def1 heads1 rest1 heads2 rest2 else failWith $ DifferentSorts t1 t2 match1 _ t1@KList{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@KList{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 From 6e6fc9bf27a68e7c3e12a66dd2d7a4828c2286cf Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 20 May 2025 12:30:26 +1000 Subject: [PATCH 08/15] try to apply equations to internalised maps, lists, and sets --- .../library/Booster/Pattern/ApplyEquations.hs | 75 +++++++++++++------ 1 file changed, 53 insertions(+), 22 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 059c7ac1ba..45bc9ca933 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -585,28 +585,59 @@ traverseTerm direction onRecurse onEval trm = do else SymbolApplication sym sorts <$> mapM onRecurse args - -- maps, lists, and sets, are not currently evaluated because - -- the matcher does not provide matches on collections. - KMap def keyVals rest -> - KMap def - <$> mapM (\(k, v) -> (,) <$> onRecurse k <*> onRecurse v) keyVals - <*> maybe (pure Nothing) ((Just <$>) . onRecurse) rest - KList def heads rest -> - KList def - <$> mapM onRecurse heads - <*> maybe - (pure Nothing) - ( (Just <$>) - . \(mid, tails) -> - (,) - <$> onRecurse mid - <*> mapM onRecurse tails - ) - rest - KSet def keyVals rest -> - KSet def - <$> mapM onRecurse keyVals - <*> maybe (pure Nothing) ((Just <$>) . onRecurse) rest + kmap@(KMap def keyVals rest) -> do + let handlePairs = mapM (\(k, v) -> (,) <$> onRecurse k <*> onRecurse v) + if direction == BottomUp + then do + -- evaluate arguments first + keyVals' <- handlePairs keyVals + rest' <- traverse onRecurse rest + -- then try to apply equations + onEval $ KMap def keyVals' rest' + else {- direction == TopDown -} do + -- try to apply equations + kmap' <- onEval kmap + case kmap' of + -- the result should be another internal KMap + KMap _ keyVals' rest' -> + KMap def + <$> handlePairs keyVals' + <*> traverse onRecurse rest' + other -> -- unlikely to occur, but won't loop + onRecurse other + klist@(KList def heads rest) -> do + let handleRest = + traverse $ \(mid, tails) -> (,) <$> onRecurse mid <*> mapM onRecurse tails + if direction == BottomUp + then do + heads' <- mapM onRecurse heads + rest' <- handleRest rest + onEval (KList def heads' rest') + else {- direction == TopDown -} do + klist' <- onEval klist + case klist' of + -- the result should be another internal KList + KList _ heads' rest' -> + KList def + <$> mapM onRecurse heads' + <*> handleRest rest' + other -> + onRecurse other + kset@(KSet def elems rest) + | direction == BottomUp -> do + elems' <- mapM onRecurse elems + rest' <- traverse onRecurse rest + onEval $ KSet def elems' rest' + | otherwise {- direction == TopDown -} -> do + kset' <- onEval kset + case kset' of + -- the result should be another internal KSet + KSet _ elems' rest' -> + KSet def + <$> mapM onRecurse elems' + <*> traverse onRecurse rest' + other -> + onRecurse other cached :: LoggerMIO io => CacheTag -> (Term -> EquationT io Term) -> Term -> EquationT io Term cached cacheTag cb t@(Term attributes _) From dc2e190fafefadee152cefcc7f9b151af7dd75b6 Mon Sep 17 00:00:00 2001 From: github-actions Date: Tue, 20 May 2025 02:34:15 +0000 Subject: [PATCH 09/15] Format with fourmolu --- booster/library/Booster/Pattern/ApplyEquations.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 45bc9ca933..cd4df2fae7 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -603,7 +603,8 @@ traverseTerm direction onRecurse onEval trm = do KMap def <$> handlePairs keyVals' <*> traverse onRecurse rest' - other -> -- unlikely to occur, but won't loop + other -> + -- unlikely to occur, but won't loop onRecurse other klist@(KList def heads rest) -> do let handleRest = From 78cbe0d80114168c1f0c937669a7115028a525fe Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 20 May 2025 13:22:46 +1000 Subject: [PATCH 10/15] use uv in kontrol perf script --- scripts/performance-tests-kontrol.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/performance-tests-kontrol.sh b/scripts/performance-tests-kontrol.sh index 2c95cc3cb1..239895e593 100755 --- a/scripts/performance-tests-kontrol.sh +++ b/scripts/performance-tests-kontrol.sh @@ -80,7 +80,7 @@ done set -- "${POSITIONAL_ARGS[@]}" # restore positional parameters -# poetry takes too long to clone kevm-pyk, so we just do a shallow clone locally and override pyproject.toml +# it takes long to clone kevm-pyk, so we just do a shallow clone locally and override pyproject.toml git clone --depth 1 --branch $KEVM_VERSION https://github.com/runtimeverification/evm-semantics.git cd evm-semantics git submodule update --init --recursive --depth 1 kevm-pyk/src/kevm_pyk/kproj/plugin @@ -92,8 +92,8 @@ sed -i'' -e "s|git = \"https://github.com/runtimeverification/evm-semantics.git\ sed -i'' -e "s|'forge', 'build'|'forge', 'build', '--no-auto-detect'|g" src/kontrol/foundry.py sed -i'' -e "s|'forge', 'build'|'forge', 'build', '--no-auto-detect'|g" src/tests/utils.py sed -i'' -e "s|'forge', 'build'|'forge', 'build', '--no-auto-detect'|g" src/tests/integration/conftest.py -# update the lock file to keep poetry from complaining -poetry lock +# update the lock file to keep the build tool from complaining +uv lock feature_shell() { GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/haskell-backend $SCRIPT_DIR/../ --ignore-environment --command bash -c "$1" @@ -104,7 +104,7 @@ master_shell() { } # kompile Kontrol's K dependencies -feature_shell "poetry install && poetry run kdist --verbose build evm-semantics.plugin evm-semantics.haskell kontrol.* --jobs 4" +feature_shell "uv run kdist --verbose build evm-semantics.plugin evm-semantics.haskell kontrol.* --jobs 4" # kompile the test contracts, to be reused in feature_shell and master_shell. Copy the result from pytest's temp directory PYTEST_TEMP_DIR=$TEMPD/pytest-temp-dir From 7d8207a8211e5f4336cd9b8971c65c0256bb9c37 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 23 May 2025 17:23:58 +1000 Subject: [PATCH 11/15] WIP more unit tests for list hooks --- booster/unit-tests/Test/Booster/Builtin.hs | 128 +++++++++++++++++---- 1 file changed, 108 insertions(+), 20 deletions(-) diff --git a/booster/unit-tests/Test/Booster/Builtin.hs b/booster/unit-tests/Test/Booster/Builtin.hs index 6841a2290b..de5531496c 100644 --- a/booster/unit-tests/Test/Booster/Builtin.hs +++ b/booster/unit-tests/Test/Booster/Builtin.hs @@ -87,25 +87,15 @@ testListHooks = "LIST hooks" [ testListArityChecks , testListConcatHook - , testListSizeHook + , testListElementHook , testListGetHook + , testListInHook + , testListMakeHook + , testListRangeHook + , testListSizeHook , testListUpdateHook ] --- helpers -listOfThings :: Int -> Term -listOfThings n = - let things = map numDV [1 .. n] - in KList Fixture.testKListDef things Nothing - --- wrap an Int into an injection to KItem here -numDV :: Int -> Term -numDV n = - Fixture.inj Fixture.someSort Fixture.kItemSort $ dv Fixture.someSort $ BS.pack $ show n - -evalHook :: MonadFail m => BS.ByteString -> [Term] -> m (Maybe Term) -evalHook name args = either (fail . show) pure $ runExcept $ runHook name args - testListArityChecks :: TestTree testListArityChecks = testGroup @@ -114,6 +104,7 @@ testListArityChecks = assertException "LIST.concat" [] assertException "LIST.concat" [[trm| X:SortList |]] assertException "LIST.concat" $ replicate 3 [trm| X:SortList |] +-- , error "missing arity checks!" , testCase "LIST.size: list arg." $ do assertException "LIST.size" [] assertException "LIST.size" $ replicate 2 [trm| X:SortList |] @@ -131,6 +122,21 @@ testListArityChecks = assertException name = assertBool "Unexpected success" . isLeft . runExcept . runHook name +-- list and element helpers +listOfThings :: Int -> Term +listOfThings n = + let things = map numDV [1 .. n] + in KList Fixture.testKListDef things Nothing + +-- wrap an Int into an injection to KItem here +numDV :: Int -> Term +numDV n = + Fixture.inj Fixture.someSort Fixture.kItemSort $ dv Fixture.someSort $ BS.pack $ show n + +-- this assumes all terms are sort KItem or that sorts are irrelevant +kitemList :: [Term] -> Term +kitemList items = KList Builtin.kItemListDef items Nothing + testListConcatHook :: TestTree testListConcatHook = testGroup @@ -184,6 +190,88 @@ testListConcatHook = Nothing === result ] +testListElementHook :: TestTree +testListElementHook = + testGroup + "LIST.element" + [ testCase "making a singleton list" $ do + let thing = [trm| THING:SortKItem |] + result <- evalHook "LIST.element" [thing] + -- this will return the fixed built-in list metadata + Just (kitemList [thing]) @=? result + ] + +testListInHook :: TestTree +testListInHook = + testGroup + "LIST.in" + [ testCase "LIST.in is false when the list is empty" $ do + let thing = numDV 0 + empty = listOfThings 0 + result <- evalHook "LIST.in" [thing, empty] + result `_shouldBe_` False + , testProperty "LIST.in is true when an item is present in the head" . property $ do + l <- forAll $ between1And 42 + k <- forAll $ between1And l + let list = listOfThings l -- [1 .. l] + target = numDV k + result <- evalHook "LIST.in" [target, list] + result `shouldBe` True + , testProperty "LIST.in is true when an item is present in the tail" . property $ do + l <- forAll $ between1And 42 + k <- forAll $ between1And l + let elems = map numDV [1 .. l] + list = KList Fixture.testKListDef [] $ Just ([trm| INIT:SortList |], elems) + target = numDV k + result <- evalHook "LIST.in" [target, list] + result `shouldBe` True + , testProperty "LIST.in is false when an item is not present (concrete list)" . property $ do + l <- forAll smallNat + let list = listOfThings l -- [1 .. l] + target = numDV 0 + result <- evalHook "LIST.in" [target, list] + result `shouldBe` False + , testProperty "LIST.in is indeterminate when an item is not present (list with opaque middle)" . property $ do + l <- forAll smallNat + let elems = map numDV [1 .. l] + list = KList Fixture.testKListDef elems $ Just ([trm| INIT:SortList |], []) + target = numDV 0 + result <- evalHook "LIST.in" [target, list] + Nothing === result + ] + where + x `_shouldBe_` b = Just (Builtin.boolTerm b) @=? x + x `shouldBe` b = Just (Builtin.boolTerm b) === x + + +testListMakeHook :: TestTree +testListMakeHook = + testGroup + "LIST.make" + [ testCase "LIST.in makes empty lists when size 0 is given" $ do + let thing = numDV 0 + size = Builtin.intTerm 0 + result <- evalHook "LIST.make" [size, thing] + Just (KList Builtin.kItemListDef [] Nothing) @=? result + , testProperty "LIST.in makes a list of given length" . property $ do + let thing = numDV 0 + size <- forAll smallNat + let sizeTerm = Builtin.intTerm $ fromIntegral size + result <- evalHook "LIST.make" [sizeTerm, thing] + case result of + Nothing -> failure + Just (KList _ concrete Nothing) -> + concrete === replicate size thing + Just other -> failure + ] + +testListRangeHook :: TestTree +testListRangeHook = + testGroup + "LIST.range" + [ -- TODO + ] + testListSizeHook :: TestTree testListSizeHook = testGroup @@ -336,9 +424,6 @@ genAssocs range = noDupKeys <$> Gen.list range genAssoc mapWith :: [(Term, Term)] -> Maybe Term -> Term mapWith = KMap Fixture.testKMapDefinition -concreteList :: [Term] -> Term -concreteList items = KList Builtin.kItemListDef items Nothing - testMapUpdateHook :: TestTree testMapUpdateHook = testGroup @@ -690,7 +775,7 @@ testMapKeysListHook = result <- runKeysList [mapWith assocs Nothing] let expected = -- map assocs are sorted and deduplicated - concreteList . map fst . Set.toAscList . Set.fromList $ assocs + kitemList . map fst . Set.toAscList . Set.fromList $ assocs Just expected === result ] where @@ -716,7 +801,7 @@ testMapValuesHook = result <- runValues [mapWith assocs Nothing] let expected = -- map assocs are sorted and deduplicated - concreteList . map snd . Set.toAscList . Set.fromList $ assocs + kitemList . map snd . Set.toAscList . Set.fromList $ assocs Just expected === result ] where @@ -826,6 +911,9 @@ runHook name = fromMaybe (error $ show name <> " hook not found") $ Map.lookup name Builtin.hooks +evalHook :: MonadFail m => BS.ByteString -> [Term] -> m (Maybe Term) +evalHook name args = either (fail . show) pure $ runExcept $ runHook name args + smallNat :: Gen Int smallNat = Gen.int (Range.linear 0 42) From d3975ef24b95a0cc427d4bf4605c9006792b1c0a Mon Sep 17 00:00:00 2001 From: github-actions Date: Fri, 23 May 2025 07:25:24 +0000 Subject: [PATCH 12/15] Format with fourmolu --- booster/unit-tests/Test/Booster/Builtin.hs | 61 +++++++++++----------- 1 file changed, 31 insertions(+), 30 deletions(-) diff --git a/booster/unit-tests/Test/Booster/Builtin.hs b/booster/unit-tests/Test/Booster/Builtin.hs index de5531496c..786c55facd 100644 --- a/booster/unit-tests/Test/Booster/Builtin.hs +++ b/booster/unit-tests/Test/Booster/Builtin.hs @@ -104,8 +104,8 @@ testListArityChecks = assertException "LIST.concat" [] assertException "LIST.concat" [[trm| X:SortList |]] assertException "LIST.concat" $ replicate 3 [trm| X:SortList |] --- , error "missing arity checks!" - , testCase "LIST.size: list arg." $ do + , -- , error "missing arity checks!" + testCase "LIST.size: list arg." $ do assertException "LIST.size" [] assertException "LIST.size" $ replicate 2 [trm| X:SortList |] , testCase "LIST.get: list and int arg.s" $ do @@ -211,39 +211,39 @@ testListInHook = result <- evalHook "LIST.in" [thing, empty] result `_shouldBe_` False , testProperty "LIST.in is true when an item is present in the head" . property $ do - l <- forAll $ between1And 42 - k <- forAll $ between1And l - let list = listOfThings l -- [1 .. l] - target = numDV k - result <- evalHook "LIST.in" [target, list] - result `shouldBe` True + l <- forAll $ between1And 42 + k <- forAll $ between1And l + let list = listOfThings l -- [1 .. l] + target = numDV k + result <- evalHook "LIST.in" [target, list] + result `shouldBe` True , testProperty "LIST.in is true when an item is present in the tail" . property $ do - l <- forAll $ between1And 42 - k <- forAll $ between1And l - let elems = map numDV [1 .. l] - list = KList Fixture.testKListDef [] $ Just ([trm| INIT:SortList |], elems) - target = numDV k - result <- evalHook "LIST.in" [target, list] - result `shouldBe` True + l <- forAll $ between1And 42 + k <- forAll $ between1And l + let elems = map numDV [1 .. l] + list = KList Fixture.testKListDef [] $ Just ([trm| INIT:SortList |], elems) + target = numDV k + result <- evalHook "LIST.in" [target, list] + result `shouldBe` True , testProperty "LIST.in is false when an item is not present (concrete list)" . property $ do - l <- forAll smallNat - let list = listOfThings l -- [1 .. l] - target = numDV 0 - result <- evalHook "LIST.in" [target, list] - result `shouldBe` False - , testProperty "LIST.in is indeterminate when an item is not present (list with opaque middle)" . property $ do - l <- forAll smallNat - let elems = map numDV [1 .. l] - list = KList Fixture.testKListDef elems $ Just ([trm| INIT:SortList |], []) - target = numDV 0 - result <- evalHook "LIST.in" [target, list] - Nothing === result + l <- forAll smallNat + let list = listOfThings l -- [1 .. l] + target = numDV 0 + result <- evalHook "LIST.in" [target, list] + result `shouldBe` False + , testProperty "LIST.in is indeterminate when an item is not present (list with opaque middle)" + . property $ do + l <- forAll smallNat + let elems = map numDV [1 .. l] + list = KList Fixture.testKListDef elems $ Just ([trm| INIT:SortList |], []) + target = numDV 0 + result <- evalHook "LIST.in" [target, list] + Nothing === result ] where x `_shouldBe_` b = Just (Builtin.boolTerm b) @=? x x `shouldBe` b = Just (Builtin.boolTerm b) === x - testListMakeHook :: TestTree testListMakeHook = testGroup @@ -269,8 +269,9 @@ testListRangeHook :: TestTree testListRangeHook = testGroup "LIST.range" - [ -- TODO - ] + [] + +-- TODO testListSizeHook :: TestTree testListSizeHook = From 55749abbad6bed2e0f70a16382b831864068f195 Mon Sep 17 00:00:00 2001 From: github-actions Date: Fri, 23 May 2025 07:26:47 +0000 Subject: [PATCH 13/15] Format with fourmolu --- booster/unit-tests/Test/Booster/Builtin.hs | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/booster/unit-tests/Test/Booster/Builtin.hs b/booster/unit-tests/Test/Booster/Builtin.hs index 786c55facd..18de5f4f06 100644 --- a/booster/unit-tests/Test/Booster/Builtin.hs +++ b/booster/unit-tests/Test/Booster/Builtin.hs @@ -232,13 +232,14 @@ testListInHook = result <- evalHook "LIST.in" [target, list] result `shouldBe` False , testProperty "LIST.in is indeterminate when an item is not present (list with opaque middle)" - . property $ do - l <- forAll smallNat - let elems = map numDV [1 .. l] - list = KList Fixture.testKListDef elems $ Just ([trm| INIT:SortList |], []) - target = numDV 0 - result <- evalHook "LIST.in" [target, list] - Nothing === result + . property + $ do + l <- forAll smallNat + let elems = map numDV [1 .. l] + list = KList Fixture.testKListDef elems $ Just ([trm| INIT:SortList |], []) + target = numDV 0 + result <- evalHook "LIST.in" [target, list] + Nothing === result ] where x `_shouldBe_` b = Just (Builtin.boolTerm b) @=? x From 8e07919d1ff9d1e2443a7de61784d7db23e7a987 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 26 May 2025 22:35:37 +1000 Subject: [PATCH 14/15] LIST.range tests and corrected hook implementation --- booster/library/Booster/Builtin/LIST.hs | 23 +++++---- booster/unit-tests/Test/Booster/Builtin.hs | 56 +++++++++++++++++++--- 2 files changed, 63 insertions(+), 16 deletions(-) diff --git a/booster/library/Booster/Builtin/LIST.hs b/booster/library/Booster/Builtin/LIST.hs index 49545a25b3..d9225c3dbe 100644 --- a/booster/library/Booster/Builtin/LIST.hs +++ b/booster/library/Booster/Builtin/LIST.hs @@ -138,17 +138,20 @@ listRangeHook [KList def heads rest, fromFront, fromBack] = (Just frontDrop, Just backDrop) | frontDrop < 0 -> pure Nothing -- bottom | backDrop < 0 -> pure Nothing -- bottom - | otherwise -> do + | Nothing <- rest -> do let targetLen = length heads - frontDrop - backDrop - case rest of - Just _ -> pure Nothing -- opaque middle, cannot drop from back - Nothing - | targetLen < 0 -> - pure Nothing -- bottom - | otherwise -> do - let part = - take targetLen $ drop frontDrop heads - pure $ Just $ KList def part Nothing + if targetLen < 0 + then pure Nothing -- bottom + else do + let part = take targetLen $ drop frontDrop heads + pure $ Just $ KList def part Nothing + | Just (mid, tails) <- rest -> + if length tails < backDrop + then pure Nothing -- opaque middle, cannot drop from back + else do + let heads' = drop frontDrop heads + tails' = reverse $ drop backDrop $ reverse tails + pure $ Just $ KList def heads' $ Just (mid, tails') listRangeHook args = arityError "LIST.range" 3 args diff --git a/booster/unit-tests/Test/Booster/Builtin.hs b/booster/unit-tests/Test/Booster/Builtin.hs index 18de5f4f06..46d637f598 100644 --- a/booster/unit-tests/Test/Booster/Builtin.hs +++ b/booster/unit-tests/Test/Booster/Builtin.hs @@ -261,18 +261,62 @@ testListMakeHook = result <- evalHook "LIST.make" [sizeTerm, thing] case result of Nothing -> failure - Just (KList _ concrete Nothing) -> - concrete === replicate size thing - Just other -> failure + Just (KList _ concreteElems Nothing) -> + concreteElems === replicate size thing + Just _ -> failure ] testListRangeHook :: TestTree testListRangeHook = testGroup "LIST.range" - [] - --- TODO + [ testProperty "LIST.range with zero indexes is identity" . property $ do + size <- forAll smallNat + let list = listOfThings size + result <- evalHook "LIST.range" [list, Builtin.intTerm 0, Builtin.intTerm 0] + Just list === result + , testProperty "LIST.range with valid range in concrete list" . property $ do + size <- forAll smallNat + a <- forAll $ between0And size + let maxB = size - a + b <- forAll $ between0And maxB + let list = listOfThings size -- [1..size] + expected = + KList Fixture.testKListDef (map numDV [a + 1 .. size - b]) Nothing + aTerm = Builtin.intTerm $ fromIntegral a + bTerm = Builtin.intTerm $ fromIntegral b + result <- evalHook "LIST.range" [list, aTerm, bTerm] + Just expected === result + , testProperty "LIST.range with opaque middle but feasible range" . property $ do + front <- forAll $ between1And 42 -- NB list must not be just the variable + back <- forAll smallNat + frontDrop <- forAll $ between0And front + backDrop <- forAll $ between0And back + let frontElems = map numDV [1..front] + backElems = map numDV [1..back] + midVar = [trm| MID:List |] + list = + KList Fixture.testKListDef frontElems $ Just (midVar, backElems) + frontTerm = Builtin.intTerm $ fromIntegral frontDrop + backTerm = Builtin.intTerm $ fromIntegral backDrop + result <- evalHook "LIST.range" [list, frontTerm, backTerm] + let expected = + KList + Fixture.testKListDef + (map numDV [frontDrop + 1 .. front]) + (Just (midVar, map numDV [1 .. back - backDrop])) + Just expected === result + , testProperty "LIST.range concrete list, parameters too large" . property $ do + size <- forAll smallNat + plus <- forAll $ between1And 42 + let zero = Builtin.intTerm 0 + tooMuch = Builtin.intTerm $ fromIntegral (size + plus) + list = listOfThings size + result1 <- evalHook "LIST.range" [list, zero, tooMuch] + Nothing === result1 + result2 <- evalHook "LIST.range" [list, tooMuch, zero] + Nothing === result2 + ] testListSizeHook :: TestTree testListSizeHook = From d281b4bf1dfa2330c352ebdd8509193e2627aed5 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 26 May 2025 23:11:34 +1000 Subject: [PATCH 15/15] LIST hook arity check tests, formatting --- booster/library/Booster/Builtin/LIST.hs | 12 +++++------ booster/unit-tests/Test/Booster/Builtin.hs | 23 ++++++++++++++++------ 2 files changed, 23 insertions(+), 12 deletions(-) diff --git a/booster/library/Booster/Builtin/LIST.hs b/booster/library/Booster/Builtin/LIST.hs index d9225c3dbe..89b02a1754 100644 --- a/booster/library/Booster/Builtin/LIST.hs +++ b/booster/library/Booster/Builtin/LIST.hs @@ -146,12 +146,12 @@ listRangeHook [KList def heads rest, fromFront, fromBack] = let part = take targetLen $ drop frontDrop heads pure $ Just $ KList def part Nothing | Just (mid, tails) <- rest -> - if length tails < backDrop - then pure Nothing -- opaque middle, cannot drop from back - else do - let heads' = drop frontDrop heads - tails' = reverse $ drop backDrop $ reverse tails - pure $ Just $ KList def heads' $ Just (mid, tails') + if length tails < backDrop + then pure Nothing -- opaque middle, cannot drop from back + else do + let heads' = drop frontDrop heads + tails' = reverse $ drop backDrop $ reverse tails + pure $ Just $ KList def heads' $ Just (mid, tails') listRangeHook args = arityError "LIST.range" 3 args diff --git a/booster/unit-tests/Test/Booster/Builtin.hs b/booster/unit-tests/Test/Booster/Builtin.hs index 46d637f598..c394926f9a 100644 --- a/booster/unit-tests/Test/Booster/Builtin.hs +++ b/booster/unit-tests/Test/Booster/Builtin.hs @@ -104,14 +104,25 @@ testListArityChecks = assertException "LIST.concat" [] assertException "LIST.concat" [[trm| X:SortList |]] assertException "LIST.concat" $ replicate 3 [trm| X:SortList |] - , -- , error "missing arity checks!" - testCase "LIST.size: list arg." $ do - assertException "LIST.size" [] - assertException "LIST.size" $ replicate 2 [trm| X:SortList |] , testCase "LIST.get: list and int arg.s" $ do assertException "LIST.get" [] assertException "LIST.get" [[trm| X:SortList |]] assertException "LIST.get" $ replicate 3 [trm| X:SortList{} |] + , testCase "LIST.in: element and list arg." $ do + assertException "LIST.in" [] + assertException "LIST.in" [[trm| X:SortList |]] + assertException "LIST.in" $ replicate 3 [trm| X:SortList |] + , testCase "LIST.make: element and size arg." $ do + assertException "LIST.make" [] + assertException "LIST.make" [[trm| X:SortList |]] + assertException "LIST.make" $ replicate 3 [trm| X:SortList |] + , testCase "LIST.range: list and two int arg.s" $ do + assertException "LIST.range" [] + assertException "LIST.range" [[trm| X:SortList |]] + assertException "LIST.range" $ replicate 4 [trm| X:SortList |] + , testCase "LIST.size: list arg." $ do + assertException "LIST.size" [] + assertException "LIST.size" $ replicate 2 [trm| X:SortList |] , testCase "LIST.update: list, index, and element" $ do assertException "LIST.update" [] assertException "LIST.update" [[trm| X:SortList |]] @@ -292,8 +303,8 @@ testListRangeHook = back <- forAll smallNat frontDrop <- forAll $ between0And front backDrop <- forAll $ between0And back - let frontElems = map numDV [1..front] - backElems = map numDV [1..back] + let frontElems = map numDV [1 .. front] + backElems = map numDV [1 .. back] midVar = [trm| MID:List |] list = KList Fixture.testKListDef frontElems $ Just (midVar, backElems)