Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 9da9013

Browse files
rv-auditorrv-auditor
committedMay 26, 2025
Merge remote-tracking branch 'origin/master' into release
2 parents 3032c7b + 79f23bf commit 9da9013

File tree

9 files changed

+544
-88
lines changed

9 files changed

+544
-88
lines changed
 

‎booster/library/Booster/Builtin/LIST.hs

Lines changed: 112 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ import Data.ByteString.Char8 (ByteString, pack)
1717
import Data.Map (Map)
1818
import Data.Map qualified as Map
1919

20+
import Booster.Builtin.BOOL (boolTerm)
2021
import Booster.Builtin.Base
2122
import Booster.Builtin.INT
2223
import Booster.Definition.Attributes.Base (
@@ -29,10 +30,48 @@ builtinsLIST :: Map ByteString BuiltinFunction
2930
builtinsLIST =
3031
Map.mapKeys ("LIST." <>) $
3132
Map.fromList
32-
[ "get" ~~> listGetHook
33+
[ "concat" ~~> listConcatHook
34+
, "element" ~~> listElementHook
35+
, "get" ~~> listGetHook
36+
, "in" ~~> listInHook
37+
, "make" ~~> listMakeHook
38+
, "range" ~~> listRangeHook
3339
, "size" ~~> listSizeHook
40+
, "unit" ~~> listUnitHook
41+
, "update" ~~> listUpdateHook
3442
]
3543

44+
-- | concatenate two lists
45+
listConcatHook :: BuiltinFunction
46+
listConcatHook [KList def1 heads1 rest1, KList def2 heads2 rest2]
47+
-- see Booster.Pattern.Base.internaliseKList
48+
| def1 /= def2 =
49+
pure Nothing -- actually a compiler error
50+
| Nothing <- rest1
51+
, Nothing <- rest2 =
52+
pure $ Just $ KList def1 (heads1 <> heads2) Nothing
53+
| Nothing <- rest1 =
54+
pure $ Just $ KList def2 (heads1 <> heads2) rest2
55+
| Nothing <- rest2
56+
, Just (mid1, tails1) <- rest1 =
57+
pure $ Just $ KList def1 heads1 $ Just (mid1, tails1 <> heads2)
58+
| otherwise -- opaque middle in both lists, unable to simplify
59+
=
60+
pure Nothing
61+
listConcatHook [KList def1 heads Nothing, other] =
62+
pure $ Just $ KList def1 heads (Just (other, []))
63+
listConcatHook [other, KList def2 heads Nothing] =
64+
pure $ Just $ KList def2 [] (Just (other, heads))
65+
listConcatHook other =
66+
arityError "LIST.concat" 2 other
67+
68+
-- | create a singleton list from a given element
69+
listElementHook :: BuiltinFunction
70+
listElementHook [elem'] =
71+
pure $ Just $ KList kItemListDef [elem'] Nothing
72+
listElementHook other =
73+
arityError "LIST.element" 1 other
74+
3675
listGetHook :: BuiltinFunction
3776
listGetHook [KList _ heads mbRest, intArg] =
3877
let headLen = length heads
@@ -67,6 +106,55 @@ listGetHook [_other, _] =
67106
listGetHook args =
68107
arityError "LIST.get" 2 args
69108

109+
listInHook :: BuiltinFunction
110+
listInHook [e, KList _ heads rest] =
111+
case rest of
112+
Nothing -> pure $ Just $ boolTerm (e `elem` heads)
113+
Just (_mid, tails)
114+
| e `elem` tails ->
115+
pure $ Just $ boolTerm True
116+
| otherwise -> -- could be in opaque _mid
117+
pure Nothing
118+
listInHook args =
119+
arityError "LIST.in" 2 args
120+
121+
listMakeHook :: BuiltinFunction
122+
listMakeHook [intArg, value] =
123+
case fromIntegral <$> readIntTerm intArg of
124+
Nothing ->
125+
intArg `shouldHaveSort` "SortInt" >> pure Nothing
126+
Just len ->
127+
pure $ Just $ KList kItemListDef (replicate len value) Nothing
128+
listMakeHook args =
129+
arityError "LIST.make" 2 args
130+
131+
listRangeHook :: BuiltinFunction
132+
listRangeHook [KList def heads rest, fromFront, fromBack] =
133+
case (fromIntegral <$> readIntTerm fromFront, fromIntegral <$> readIntTerm fromBack) of
134+
(Nothing, _) ->
135+
fromFront `shouldHaveSort` "SortInt" >> pure Nothing
136+
(_, Nothing) ->
137+
fromBack `shouldHaveSort` "SortInt" >> pure Nothing
138+
(Just frontDrop, Just backDrop)
139+
| frontDrop < 0 -> pure Nothing -- bottom
140+
| backDrop < 0 -> pure Nothing -- bottom
141+
| Nothing <- rest -> do
142+
let targetLen = length heads - frontDrop - backDrop
143+
if targetLen < 0
144+
then pure Nothing -- bottom
145+
else do
146+
let part = take targetLen $ drop frontDrop heads
147+
pure $ Just $ KList def part Nothing
148+
| Just (mid, tails) <- rest ->
149+
if length tails < backDrop
150+
then pure Nothing -- opaque middle, cannot drop from back
151+
else do
152+
let heads' = drop frontDrop heads
153+
tails' = reverse $ drop backDrop $ reverse tails
154+
pure $ Just $ KList def heads' $ Just (mid, tails')
155+
listRangeHook args =
156+
arityError "LIST.range" 3 args
157+
70158
listSizeHook :: BuiltinFunction
71159
listSizeHook = \case
72160
[KList _ heads Nothing] ->
@@ -78,6 +166,29 @@ listSizeHook = \case
78166
moreArgs ->
79167
arityError "LIST.size" 1 moreArgs
80168

169+
listUnitHook :: BuiltinFunction
170+
listUnitHook [] = pure $ Just $ KList kItemListDef [] Nothing
171+
listUnitHook args =
172+
arityError "LIST.unit" 0 args
173+
174+
listUpdateHook :: BuiltinFunction
175+
listUpdateHook [KList def heads rest, intArg, value] =
176+
case fromIntegral <$> readIntTerm intArg of
177+
Nothing ->
178+
intArg `shouldHaveSort` "SortInt" >> pure Nothing
179+
Just idx
180+
| idx < 0 ->
181+
pure Nothing -- bottom
182+
| otherwise ->
183+
case splitAt idx heads of
184+
(front, _target : back) ->
185+
pure $ Just $ KList def (front <> (value : back)) rest
186+
(_heads, []) ->
187+
-- idx >= length heads, indeterminate
188+
pure Nothing
189+
listUpdateHook args =
190+
arityError "LIST.update" 3 args
191+
81192
kItemListDef :: KListDefinition
82193
kItemListDef =
83194
KListDefinition

‎booster/library/Booster/Pattern/ApplyEquations.hs

Lines changed: 54 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -585,28 +585,60 @@ traverseTerm direction onRecurse onEval trm = do
585585
else
586586
SymbolApplication sym sorts
587587
<$> mapM onRecurse args
588-
-- maps, lists, and sets, are not currently evaluated because
589-
-- the matcher does not provide matches on collections.
590-
KMap def keyVals rest ->
591-
KMap def
592-
<$> mapM (\(k, v) -> (,) <$> onRecurse k <*> onRecurse v) keyVals
593-
<*> maybe (pure Nothing) ((Just <$>) . onRecurse) rest
594-
KList def heads rest ->
595-
KList def
596-
<$> mapM onRecurse heads
597-
<*> maybe
598-
(pure Nothing)
599-
( (Just <$>)
600-
. \(mid, tails) ->
601-
(,)
602-
<$> onRecurse mid
603-
<*> mapM onRecurse tails
604-
)
605-
rest
606-
KSet def keyVals rest ->
607-
KSet def
608-
<$> mapM onRecurse keyVals
609-
<*> maybe (pure Nothing) ((Just <$>) . onRecurse) rest
588+
kmap@(KMap def keyVals rest) -> do
589+
let handlePairs = mapM (\(k, v) -> (,) <$> onRecurse k <*> onRecurse v)
590+
if direction == BottomUp
591+
then do
592+
-- evaluate arguments first
593+
keyVals' <- handlePairs keyVals
594+
rest' <- traverse onRecurse rest
595+
-- then try to apply equations
596+
onEval $ KMap def keyVals' rest'
597+
else {- direction == TopDown -} do
598+
-- try to apply equations
599+
kmap' <- onEval kmap
600+
case kmap' of
601+
-- the result should be another internal KMap
602+
KMap _ keyVals' rest' ->
603+
KMap def
604+
<$> handlePairs keyVals'
605+
<*> traverse onRecurse rest'
606+
other ->
607+
-- unlikely to occur, but won't loop
608+
onRecurse other
609+
klist@(KList def heads rest) -> do
610+
let handleRest =
611+
traverse $ \(mid, tails) -> (,) <$> onRecurse mid <*> mapM onRecurse tails
612+
if direction == BottomUp
613+
then do
614+
heads' <- mapM onRecurse heads
615+
rest' <- handleRest rest
616+
onEval (KList def heads' rest')
617+
else {- direction == TopDown -} do
618+
klist' <- onEval klist
619+
case klist' of
620+
-- the result should be another internal KList
621+
KList _ heads' rest' ->
622+
KList def
623+
<$> mapM onRecurse heads'
624+
<*> handleRest rest'
625+
other ->
626+
onRecurse other
627+
kset@(KSet def elems rest)
628+
| direction == BottomUp -> do
629+
elems' <- mapM onRecurse elems
630+
rest' <- traverse onRecurse rest
631+
onEval $ KSet def elems' rest'
632+
| otherwise {- direction == TopDown -} -> do
633+
kset' <- onEval kset
634+
case kset' of
635+
-- the result should be another internal KSet
636+
KSet _ elems' rest' ->
637+
KSet def
638+
<$> mapM onRecurse elems'
639+
<*> traverse onRecurse rest'
640+
other ->
641+
onRecurse other
610642

611643
cached :: LoggerMIO io => CacheTag -> (Term -> EquationT io Term) -> Term -> EquationT io Term
612644
cached cacheTag cb t@(Term attributes _)

‎booster/library/Booster/Pattern/Match.hs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -246,7 +246,6 @@ match1 _ t1@KList{} t2@DomainValue{}
246246
match1 Eval t1@KList{} t2@Injection{} = addIndeterminate t1 t2
247247
match1 _ t1@KList{} t2@Injection{} = failWith $ DifferentSymbols t1 t2
248248
match1 _ t1@KList{} t2@KMap{} = failWith $ DifferentSymbols t1 t2
249-
match1 Eval t1@KList{} t2@KList{} = addIndeterminate t1 t2
250249
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
251250
match1 _ t1@KList{} t2@KSet{} = failWith $ DifferentSymbols t1 t2
252251
match1 _ t1@KList{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2

‎booster/unit-tests/Test/Booster/Builtin.hs

Lines changed: 302 additions & 55 deletions
Large diffs are not rendered by default.

‎kore/src/Kore/Builtin/List.hs

Lines changed: 27 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -211,6 +211,10 @@ symbolVerifiers =
211211
( updateAllKey
212212
, Builtin.verifySymbol assertSort [assertSort, Int.assertSort, assertSort]
213213
)
214+
,
215+
( rangeKey
216+
, Builtin.verifySymbol assertSort [assertSort, Int.assertSort, Int.assertSort]
217+
)
214218
]
215219

216220
{- | Abort function evaluation if the argument is not a List domain value.
@@ -336,17 +340,17 @@ evalSize _ _ _ = Builtin.wrongArity sizeKey
336340

337341
evalMake :: Builtin.Function
338342
evalMake _ resultSort [_len, value] = do
339-
_len <- fromInteger <$> Int.expectBuiltinInt getKey _len
343+
_len <- fromInteger <$> Int.expectBuiltinInt makeKey _len
340344
if _len >= 0
341345
then lift $ returnList resultSort (Seq.replicate _len value)
342346
else return (Pattern.bottomOf resultSort)
343-
evalMake _ _ _ = Builtin.wrongArity sizeKey
347+
evalMake _ _ _ = Builtin.wrongArity makeKey
344348

345349
evalUpdateAll :: Builtin.Function
346350
evalUpdateAll _ resultSort [_list1, _ix, _list2] = do
347-
_list1 <- expectBuiltinList getKey _list1
348-
_list2 <- expectBuiltinList getKey _list2
349-
_ix <- fromInteger <$> Int.expectBuiltinInt getKey _ix
351+
_list1 <- expectBuiltinList updateAllKey _list1
352+
_list2 <- expectBuiltinList updateAllKey _list2
353+
_ix <- fromInteger <$> Int.expectBuiltinInt updateAllKey _ix
350354
let len1 = Seq.length _list1
351355
len2 = Seq.length _list2
352356
result
@@ -360,6 +364,23 @@ evalUpdateAll _ resultSort [_list1, _ix, _list2] = do
360364
lift result
361365
evalUpdateAll _ _ _ = Builtin.wrongArity updateKey
362366

367+
evalRange :: Builtin.Function
368+
evalRange _ resultSort [list, fromFront, fromBack] = do
369+
baseList <- expectBuiltinList rangeKey list
370+
frontDrop <- fromInteger <$> Int.expectBuiltinInt rangeKey fromFront
371+
backDrop <- fromInteger <$> Int.expectBuiltinInt rangeKey fromBack
372+
let len = Seq.length baseList
373+
bottom = return $ Pattern.bottomOf resultSort
374+
result
375+
| frontDrop < 0 = bottom
376+
| backDrop < 0 = bottom
377+
| len < frontDrop + backDrop = bottom
378+
| otherwise =
379+
let size = len - frontDrop - backDrop
380+
in returnList resultSort (Seq.take size $ Seq.drop frontDrop baseList)
381+
lift result
382+
evalRange _ _ _ = Builtin.wrongArity rangeKey
383+
363384
-- | Implement builtin function evaluation.
364385
builtinFunctions :: Text -> Maybe BuiltinAndAxiomSimplifier
365386
builtinFunctions key
@@ -372,6 +393,7 @@ builtinFunctions key
372393
| key == sizeKey = Just $ Builtin.functionEvaluator evalSize
373394
| key == makeKey = Just $ Builtin.functionEvaluator evalMake
374395
| key == updateAllKey = Just $ Builtin.functionEvaluator evalUpdateAll
396+
| key == rangeKey = Just $ Builtin.functionEvaluator evalRange
375397
| otherwise = Nothing
376398

377399
data FirstElemVarData = FirstElemVarData

‎kore/src/Kore/Builtin/List/List.hs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ module Kore.Builtin.List.List (
2525
sizeKey,
2626
makeKey,
2727
updateAllKey,
28+
rangeKey,
2829
) where
2930

3031
import Data.Sequence (
@@ -165,3 +166,6 @@ makeKey = "LIST.make"
165166

166167
updateAllKey :: IsString s => s
167168
updateAllKey = "LIST.updateAll"
169+
170+
rangeKey :: IsString s => s
171+
rangeKey = "LIST.range"

‎kore/test/Test/Kore/Builtin/Definition.hs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -412,6 +412,9 @@ updateAllListSymbol :: Internal.Symbol
412412
updateAllListSymbol =
413413
builtinSymbol "updateAllList" listSort [listSort, intSort, listSort]
414414
& hook "LIST.updateAll"
415+
rangeListSymbol :: Internal.Symbol
416+
rangeListSymbol =
417+
hook "LIST.range" $ builtinSymbol "rangeList" listSort [listSort, intSort, intSort]
415418
unitList :: TermLike RewritingVariableName
416419
unitList = mkApplySymbol unitListSymbol []
417420
elementList ::
@@ -453,6 +456,12 @@ updateAllList ::
453456
TermLike RewritingVariableName ->
454457
TermLike RewritingVariableName
455458
updateAllList l1 ix l2 = mkApplySymbol updateAllListSymbol [l1, ix, l2]
459+
rangeList ::
460+
TermLike RewritingVariableName ->
461+
TermLike RewritingVariableName ->
462+
TermLike RewritingVariableName ->
463+
TermLike RewritingVariableName
464+
rangeList l start end = mkApplySymbol rangeListSymbol [l, start, end]
456465
-- ** Map
457466
unitMapSymbol :: Internal.Symbol
458467
unitMapSymbol = builtinSymbol "unitMap" mapSort [] & hook "MAP.unit"
@@ -1539,6 +1548,7 @@ listModule =
15391548
, hookedSymbolDecl sizeListSymbol
15401549
, hookedSymbolDecl makeListSymbol
15411550
, hookedSymbolDecl updateAllListSymbol
1551+
, hookedSymbolDecl rangeListSymbol
15421552
, -- A second builtin List sort, to confuse 'asPattern'.
15431553
listSortDecl2
15441554
, hookedSymbolDecl unitList2Symbol

‎kore/test/Test/Kore/Builtin/List.hs

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ module Test.Kore.Builtin.List (
1717
test_updateAll,
1818
hprop_unparse,
1919
test_size,
20+
test_range,
2021
--
2122
asInternal,
2223
asTermLike,
@@ -481,6 +482,36 @@ test_updateAll =
481482
where
482483
original = asInternal . fmap mkInt $ Seq.fromList [1, 2, 3]
483484

485+
test_range :: [TestTree]
486+
test_range =
487+
[ testCaseWithoutSMT "range([1, 2, 3], 4, 5) === \\bottom" $
488+
assertBottom =<< evaluateTerm (rangeList onetwothree (mkInt 4) (mkInt 5))
489+
, testCaseWithoutSMT "range([1, 2, 3], -1, 1) === \\bottom" $
490+
assertBottom =<< evaluateTerm (rangeList onetwothree (mkInt $ negate 1) (mkInt 1))
491+
, testCaseWithoutSMT "range([1, 2, 3], 1, -1) === \\bottom" $
492+
assertBottom =<< evaluateTerm (rangeList onetwothree (mkInt 1) (mkInt $ negate 1))
493+
, testCaseWithoutSMT "range([1, 2, 3], 2, 2) === \\bottom" $
494+
assertBottom =<< evaluateTerm (rangeList onetwothree (mkInt 2) (mkInt 2))
495+
, testCaseWithoutSMT "range([1, 2, 3], 0, 0) === [1, 2, 3]" $ do
496+
result <- evaluateTerm (rangeList onetwothree (mkInt 0) (mkInt 0))
497+
assertEqual' "" (OrPattern.fromTermLike onetwothree) result
498+
, testCaseWithoutSMT "range([1, 2, 3], 1, 1) === [2]" $ do
499+
result <- evaluateTerm (rangeList onetwothree (mkInt 1) (mkInt 1))
500+
let expected = asInternal . fmap mkInt $ Seq.singleton 2
501+
assertEqual' "" (OrPattern.fromTermLike expected) result
502+
, testCaseWithoutSMT "range([1, 2, 3], 0, 3) === []" $ do
503+
result <- evaluateTerm (rangeList onetwothree (mkInt 0) (mkInt 3))
504+
let expected = asInternal Seq.empty
505+
assertEqual' "" (OrPattern.fromTermLike expected) result
506+
, testCaseWithoutSMT "range([1, 2, 3], 2, 1) === []" $ do
507+
result <- evaluateTerm (rangeList onetwothree (mkInt 2) (mkInt 1))
508+
let expected = asInternal Seq.empty
509+
assertEqual' "" (OrPattern.fromTermLike expected) result
510+
]
511+
where
512+
onetwothree = asInternal . fmap mkInt $ Seq.fromList [1 .. 3]
513+
assertBottom = assertEqual' "expected bottom" OrPattern.bottom
514+
484515
-- | Specialize 'List.asPattern' to the builtin sort 'listSort'.
485516
asTermLike ::
486517
InternalVariable variable =>

‎scripts/performance-tests-kontrol.sh

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ done
8080
set -- "${POSITIONAL_ARGS[@]}" # restore positional parameters
8181

8282

83-
# poetry takes too long to clone kevm-pyk, so we just do a shallow clone locally and override pyproject.toml
83+
# it takes long to clone kevm-pyk, so we just do a shallow clone locally and override pyproject.toml
8484
git clone --depth 1 --branch $KEVM_VERSION https://github.com/runtimeverification/evm-semantics.git
8585
cd evm-semantics
8686
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\
9292
sed -i'' -e "s|'forge', 'build'|'forge', 'build', '--no-auto-detect'|g" src/kontrol/foundry.py
9393
sed -i'' -e "s|'forge', 'build'|'forge', 'build', '--no-auto-detect'|g" src/tests/utils.py
9494
sed -i'' -e "s|'forge', 'build'|'forge', 'build', '--no-auto-detect'|g" src/tests/integration/conftest.py
95-
# update the lock file to keep poetry from complaining
96-
poetry lock
95+
# update the lock file to keep the build tool from complaining
96+
uv lock
9797

9898
feature_shell() {
9999
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() {
104104
}
105105

106106
# kompile Kontrol's K dependencies
107-
feature_shell "poetry install && poetry run kdist --verbose build evm-semantics.plugin evm-semantics.haskell kontrol.* --jobs 4"
107+
feature_shell "uv run kdist --verbose build evm-semantics.plugin evm-semantics.haskell kontrol.* --jobs 4"
108108

109109
# kompile the test contracts, to be reused in feature_shell and master_shell. Copy the result from pytest's temp directory
110110
PYTEST_TEMP_DIR=$TEMPD/pytest-temp-dir

0 commit comments

Comments
 (0)
Please sign in to comment.