Booster: Optimize KMap internal data structure to improve Map operation performance

[Stevengre]

Background

Booster currently uses [(Term, Term)] (a Haskell linked list) as the key-value pair storage for KMapF:

data TermF t = ... | KMapF KMapDefinition [(t, t)] (Maybe t) | ...

This design has several performance bottlenecks when maps grow in size. This issue provides a detailed analysis of the root causes and proposes four possible approaches for discussion.

---

Problem Analysis

1. Core operations have excessive complexity

All key-based lookup operations use O(n) linear scans — lookup, findIndex, partition, and elem on the pairs list:

haskell-backend/booster/library/Booster/Builtin/MAP.hs

Lines 150 to 159 in c7e22cb

	mapLookupHook :: BuiltinFunction
	mapLookupHook args
	| [KMap _ pairs _mbRest, key] <- args =
	-- if the key is not found, return Nothing (no result),
	-- regardless of whether the key _could_ still be there.
	pure $ lookup key pairs
	| [_other, _] <- args =
	pure Nothing -- not an internalised map, maybe a function call
	| otherwise =
	arityError "MAP.lookup" 2 args

haskell-backend/booster/library/Booster/Builtin/MAP.hs

Lines 48 to 68 in c7e22cb

	mapUpdateHook :: BuiltinFunction
	mapUpdateHook args
	| [KMap def pairs mbRest, key, newValue] <- args = do
	case findIndex ((== key) . fst) pairs of
	Just idx ->
	-- key was found (syntactically), update pairs list
	let newPairs = take idx pairs <> ((key, newValue) : drop (idx + 1) pairs)
	in pure $ Just $ KMap def newPairs mbRest
	Nothing -- key could be in unevaluated or opaque part
	| Just _ <- mbRest ->
	pure Nothing -- have opaque part, no result
	| any (not . isConstructorLike_ . fst) pairs ->
	pure Nothing -- have unevaluated keys, no result
	| not $ isConstructorLike_ key ->
	pure Nothing -- unevaluated update key, no result
	| otherwise -> -- key certain to be absent, no rest: add pair
	pure $ Just $ KMap def ((key, newValue) : pairs) Nothing
	| [_other, _, _] <- args =
	pure Nothing -- not an internalised map, maybe a function call
	| otherwise =
	arityError "MAP.update" 3 args

haskell-backend/booster/library/Booster/Builtin/MAP.hs

Lines 118 to 138 in c7e22cb

	mapRemoveHook :: BuiltinFunction
	mapRemoveHook args
	| [m@(KMap def pairs mbRest), key] <- args = do
	case findIndex ((== key) . fst) pairs of
	Just idx ->
	-- key was found (syntactically), remove it
	let newPairs = take idx pairs <> drop (idx + 1) pairs
	in pure $ Just $ KMap def newPairs mbRest
	Nothing -- key could be in unevaluated or opaque part
	| Just _ <- mbRest ->
	pure Nothing -- have opaque part, no result
	| any (not . isConstructorLike_ . fst) pairs ->
	pure Nothing -- have unevaluated keys, no result
	| not $ isConstructorLike_ key ->
	pure Nothing -- remove key unevaluated, no result
	| otherwise -> -- key certain to be absent, no rest: map unchanged
	pure $ Just m
	| [_other, _] <- args =
	pure Nothing -- not an internalised map, maybe a function call
	| otherwise =
	arityError "MAP.remove" 2 args

haskell-backend/booster/library/Booster/Builtin/MAP.hs

Lines 182 to 206 in c7e22cb

	mapInKeysHook :: BuiltinFunction
	mapInKeysHook args
	| [key, KMap _ pairs mbRest] <- args = do
	-- only consider evaluated keys, return Nothing if any unevaluated ones are present
	let (eval'edKeys, uneval'edKeys) =
	partition isConstructorLike_ (map fst pairs)
	case (key `elem` eval'edKeys, key `elem` uneval'edKeys) of
	(True, _) ->
	-- constructor-like (evaluated) key is present
	pure $ Just $ boolTerm True
	(False, True) ->
	-- syntactically-equal unevaluated key is present
	pure $ Just $ boolTerm True
	(False, False)
	| Nothing <- mbRest -- no opaque rest
	, isConstructorLike_ key -- key to search is evaluated
	, null uneval'edKeys -> -- no keys unevaluated
	pure $ Just $ boolTerm False
	| otherwise -> -- key could be present once evaluated
	pure Nothing
	| [_, _other] <- args = do
	-- other `shouldHaveSort` "SortMap"
	pure Nothing -- not an internalised map, maybe a function call
	| otherwise =
	arityError "MAP.in_keys" 2 args

2. Smart constructor unconditionally sorts and deduplicates

Every construction of a KMap via the smart constructor calls sortAndDeduplicate — O(n log n) with expensive Ord. This is triggered after every substitution and evaluation, even when keys have not changed:

haskell-backend/booster/library/Booster/Pattern/Base.hs

Lines 580 to 609 in c7e22cb

	pattern KMap :: KMapDefinition -> [(Term, Term)] -> Maybe Term -> Term
	pattern KMap def keyVals rest <- Term _ (KMapF def keyVals rest)
	where
	KMap def keyVals rest =
	let argAttributes =
	case (keyVals, rest) of
	([], Nothing) -> mempty
	([], Just s) -> getAttributes s
	(_ : _, Nothing) -> foldl1' (<>) $ concatMap (\(k, v) -> [getAttributes k, getAttributes v]) keyVals
	(_ : _, Just r) ->
	foldl' (<>) (getAttributes r) $ concatMap (\(k, v) -> [getAttributes k, getAttributes v]) keyVals
	(keyVals', rest') = case rest of
	Just (KMap def' kvs r) | def' == def -> (kvs, r)
	r -> ([], r)
	newKeyVals = sortAndDeduplicate $ keyVals ++ keyVals'
	newRest = rest'
	in case (newKeyVals, newRest) of
	([], Just r) -> r
	_ ->
	Term
	argAttributes
	{ hash =
	Hashable.hash
	( "KMap" :: ByteString
	, def
	, map (\(k, v) -> (hash $ getAttributes k, hash $ getAttributes v)) newKeyVals
	, hash . getAttributes <$> newRest
	)
	}
	$ KMapF def newKeyVals newRest

haskell-backend/booster/library/Booster/Pattern/Base.hs

Lines 168 to 169 in c7e22cb

	sortAndDeduplicate :: Ord a => [a] -> [a]
	sortAndDeduplicate = Set.toAscList . Set.fromList

3. Ord Term is not optimized

Ord Term is auto-derived, comparing TermAttributes fields in declaration order. The first field compared is variables :: Set Variable (O(k) cost), while the cached hash :: Int (O(1)) is only the third field. In contrast, Eq Term is already manually optimized with hash-first comparison:

haskell-backend/booster/library/Booster/Pattern/Base.hs

Lines 121 to 135 in c7e22cb

	data TermAttributes = TermAttributes
	{ variables :: !(Set Variable)
	, isEvaluated :: !Bool
	-- ^ false for function calls, true for
	-- variables, recursive through AndTerm
	, hash :: !Int
	, isConstructorLike :: !Bool
	-- ^ Means that logic equality is the same as syntactic equality.
	-- True for domain values and constructor symbols (recursive
	-- through arg.s), recursive through AndTerm.
	, canBeEvaluated :: !Bool
	-- ^ false for function calls, variables, and AndTerms
	}
	deriving stock (Eq, Ord, Show, Generic, Data, Lift)
	deriving anyclass (NFData, Hashable)

haskell-backend/booster/library/Booster/Pattern/Base.hs

Lines 155 to 157 in c7e22cb

	instance Eq Term where
	Term TermAttributes{hash = hash1} t1f == Term TermAttributes{hash = hash2} t2f =
	hash1 == hash2 && t1f == t2f -- compare directly to cater for collisions

4. Matching repeatedly creates temporary data structure conversions

matchMaps converts [(Term, Term)] to a temporary Data.Map for intersection/difference on every match. The subject map is converted and discarded each time — pure O(n log n) overhead:

haskell-backend/booster/library/Booster/Pattern/Match.hs

Lines 699 to 715 in c7e22cb

	let patternKeyVals = map (first (Substitution.substituteInTerm st.mSubstitution)) patKeyVals
	-- check for duplicate keys
	checkDuplicateKeys patternKeyVals patRest
	checkDuplicateKeys subjKeyVals subjRest
	let patMap = Map.fromList patternKeyVals
	subjMap = Map.fromList subjKeyVals
	-- handles syntactically identical keys in pattern and subject
	commonMap = Map.intersectionWith (,) patMap subjMap
	patExtra = patMap `Map.withoutKeys` Map.keysSet commonMap
	subjExtra = subjMap `Map.withoutKeys` Map.keysSet commonMap
	rest <-
	matchRemainderMaps
	(toRemainderMap (Map.toList patExtra) patRest)
	(toRemainderMap (Map.toList subjExtra) subjRest)
	enqueueRegularProblems $ (Seq.fromList $ Map.elems commonMap) >< rest

5. No distinction between concrete and symbolic keys

Builtin operations and matching frequently check isConstructorLike_ and call partition, indicating concrete and symbolic keys are semantically different. The current storage does not reflect this, requiring runtime checks every time:

haskell-backend/booster/library/Booster/Pattern/Match.hs

Lines 626 to 635 in c7e22cb

	toRemainderMap :: [(Term, Term)] -> Maybe Term -> RemainderMap
	toRemainderMap kvs rest =
	let (conc, sym) = partitionConcreteKeys kvs
	in foldr
	(uncurry ConstructorKey)
	(Rest $ foldr (uncurry OtherKey) (maybe EmptyMap Remainder rest) sym)
	conc
	where
	partitionConcreteKeys :: [(Term, Term)] -> ([(Term, Term)], [(Term, Term)])
	partitionConcreteKeys = partition (\(Term attrs _, _) -> attrs.isConstructorLike)

---

Proposed Approaches

Approach A: Optimize Ord Term + avoid unnecessary sorting

Keep [(t, t)] unchanged, make two optimizations:

A1. Hand-write Ord Term with hash-first comparison:

instance Ord Term where
    compare (Term a1 t1) (Term a2 t2) =
        compare a1.hash a2.hash <> compare t1 t2

A2. After substitution/evaluation, detect whether keys have changed; skip sortAndDeduplicate if unchanged.

Pros	Cons
Smallest change, lowest risk	Single key operations remain O(n) linear scan
Does not affect TermF's Functor/Foldable/Traversable	Matching still requires temporary Map.fromList conversion
Beneficial regardless of which other approach is adopted	Does not change asymptotic complexity, only optimizes constant factors

Approach B: Data.Map Term Term + optimized Ord Term

Replace [(t, t)] with Data.Map Term Term, with hand-written Ord Term (hash-first).

Pros	Cons
Single key operations drop from O(n) to O(log n)	Requires hand-written Functor/Foldable/Traversable for TermF
Matching needs no temporary conversion	When keys change, still requires O(n log n) rebuild
Built-in sort and dedup, smart constructor simplifies	Does not distinguish concrete/symbolic keys
Output determinism (maintains sorted order)	Relies on Ord Term, still slower than O(1) hash even when optimized
intersection/difference and other set operations directly available

Regarding the TermF Functor constraint: currently [(t,t)] allows derived fmap to automatically apply to both keys and values, while Data.Map's fmap only applies to values. After investigation, only 3 functions implicitly rely on the derived instance to process KMapF keys: modifyVariablesInT, checkTermSymbols, and getCell — none are on performance hot paths (substitution, matching, and evaluation all manually pattern match). Hand-writing Functor/Foldable/Traversable instances resolves this.

Approach C: Data.HashMap Term Term

Leverage Term's existing cached hash (Hashable Term is O(1)), replacing [(t, t)] with Data.HashMap Term Term.

Pros	Cons
Single key operations O(1) amortized	Output non-determinism — HashMap.toList order is unstable, affecting test golden files, serialization consistency, debugging
Construction O(n), no sorting needed	No efficient isSubmapOfBy
Fully utilizes cached hash	Does not distinguish concrete/symbolic keys
Rebuild after substitution/evaluation is O(n)	Externalise needs sorting for deterministic output → additional O(n log n)
Requires hand-written Functor/Foldable/Traversable for TermF	Worst case O(n) on hash collision

Approach D: Separate concrete / symbolic storage

Following the pattern of the old kore backend's NormalizedAc, separate key-value pairs by key type:

KMapF KMapDefinition
    (HashMap Term Term)   -- concrete keys (constructorLike = True, no variables)
    [(Term, Term)]        -- symbolic keys (contain variables or function calls, typically 0-2)
    (Maybe Term)          -- opaque rest

Reference implementation in the old kore backend:

haskell-backend/kore/src/Kore/Internal/NormalizedAc.hs

Lines 169 to 178 in c7e22cb

	data NormalizedAc (collection :: Type -> Type -> Type) key child = NormalizedAc
	{ elementsWithVariables :: [Element collection child]
	-- ^ Non-concrete elements of the structure.
	-- These would be of sorts @(Int, String)@ for a map from @Int@ to @String@.
	, concreteElements :: HashMap key (Value collection child)
	-- ^ Concrete elements of the structure.
	-- These would be of sorts @(Int, String)@ for a map from @Int@ to @String@.
	, opaque :: [child]
	-- ^ Unoptimized (i.e. non-element) parts of the structure.
	}

Pros	Cons
Concrete key lookup O(1)	Largest amount of changes
Substitution can skip concrete keys entirely (no variables)	Requires hand-written Functor/Foldable/Traversable for TermF
Matching needs no temporary conversion or partition	Every operation must handle both parts separately
isConstructorLike_ runtime checks eliminated	After substitution, symbolic keys may become concrete, requiring reclassification
Production-proven in kore's NormalizedAc	Need to ensure consistent criteria for concrete key determination
Perfectly matches the actual concrete/symbolic distinction in K semantics	Externalise needs sorting concrete keys for deterministic output

---

Full Pipeline Comparison Summary

n = map size, p = pattern pairs (typically 1-3), n_s = symbolic pairs (typically 0-2).
Common case: subject map has all concrete keys, pattern has a few symbolic keys.

Stage	Current	A (Ord opt)	B (Map)	C (HashMap)	D (Separate)
Internalise	O(n log n) expensive Ord	O(n log n) fast Ord	O(n log n) fast Ord	O(n)	O(n)
Matching: conversion	O(n log n) expensive Ord	O(n log n) fast Ord	O(0)	O(0)	O(0)
Matching: intersect/diff	O(p + n)	O(p + n)	O(p + n)	O(min(p,n))	O(p)
Matching: partition	O(p + n)	O(p + n)	O(p + n)	O(p + n)	O(0)
Substitution: iterate	O(n) all	O(n) all	O(n) all	O(n) all	O(n) value + O(n_s) key
Substitution: rebuild	O(n log n) unconditional	O(0) common case	O(n) map value	O(n) map value	O(n_s)
Evaluation: iterate	O(n) key+value	O(n) key+value	O(n) key+value	O(n) key+value	O(n) value only
Evaluation: rebuild	O(n log n) unconditional	O(0) common case	O(n) map value	O(n) map value	O(0) key unchanged
Single key lookup	O(n)	O(n)	O(log n)	O(1)	O(1)
Output determinism	Yes	Yes	Yes	No (needs extra sort)	Needs sort for concrete keys
Per-rule total	~O(n log n) × 3 expensive Ord	~O(n log n) × 2 fast Ord	~O(n) × 3	~O(n) × 3	~O(n) + O(p)

Notes

• KSet has similar issues ([t] storage + sortAndDeduplicate on every construction) and could benefit from the same optimization approach.
• KList using [t] is reasonable (ordered, no dedup needed), though LIST.get and other random access operations could benefit from Data.Seq if needed.
• Approach A's Ord Term optimization is beneficial regardless of which other approach is adopted.

[Stevengre]

Full Pipeline Code References

Walkthrough of a single rule execution, showing every step where KMap performance overhead occurs.

1. Internalise

External concat(element(k,v), ...) symbol applications are recursively expanded into [(Term, Term)], then the smart constructor calls sortAndDeduplicate — O(n log n) with expensive Ord:

haskell-backend/booster/library/Booster/Pattern/Base.hs

Lines 292 to 324 in c7e22cb

	internaliseKmap :: KMapDefinition -> Term -> ([(Term, Term)], Maybe Term)
	internaliseKmap def@KMapDefinition{symbolNames = names} = \case
	SymbolApplication s _ []
	| s.name == names.unitSymbolName -> ([], Nothing)
	SymbolApplication s _ [k, v]
	| s.name == names.elementSymbolName -> ([(k, v)], Nothing)
	SymbolApplication s _ [l, r]
	| s.name == names.concatSymbolName -> combine (internaliseKmap def l) (internaliseKmap def r)
	KMap def' keyVals rest
	| def == def' -> (keyVals, rest)
	other -> ([], Just other) -- do we want to recurse into this term in case there are some maps under e.g. function symbol??
	where
	concatSym = concatSymbol (KMapMeta def)
	combine (conc1, sym1) (conc2, sym2) =
	( conc1 ++ conc2
	, case (sym1, sym2) of
	(Nothing, b) -> b
	(a, Nothing) -> a
	(Just a@(Term aAttribs _), Just b@(Term bAttribs _)) ->
	-- directly construct the internal term with functor to avoid a loop
	let attribs =
	(aAttribs <> bAttribs)
	{ isEvaluated = False
	, hash =
	Hashable.hash
	( "SymbolApplication" :: ByteString
	, concatSym
	, map hash [aAttribs, bAttribs]
	)
	, isConstructorLike = False
	}
	in Just $ Term attribs $ SymbolApplicationF concatSym [] [a, b]
	)

haskell-backend/booster/library/Booster/Pattern/Base.hs

Lines 591 to 595 in c7e22cb

	(keyVals', rest') = case rest of
	Just (KMap def' kvs r) | def' == def -> (kvs, r)
	r -> ([], r)
	newKeyVals = sortAndDeduplicate $ keyVals ++ keyVals'
	newRest = rest'

2. Matching

Map matching is delayed until all other matching problems are solved, to obtain a maximal prior substitution before matching map keys:

haskell-backend/booster/library/Booster/Pattern/Match.hs

Lines 692 to 697 in c7e22cb

	st <- get
	if not (Seq.null st.mQueue)
	then -- delay matching 'KMap's until there are no regular
	-- problems left, to obtain a maximal prior substitution
	-- before matching map keys.
	enqueueMapProblem (KMap def patKeyVals patRest) (KMap def subjKeyVals subjRest)

Then substitution is applied to pattern keys — O(p):

haskell-backend/booster/library/Booster/Pattern/Match.hs

Line 699 in c7e22cb

let patternKeyVals = map (first (Substitution.substituteInTerm st.mSubstitution)) patKeyVals

Both maps are temporarily converted to Data.Map for intersection/difference — O(p log p) + O(n log n) with expensive Ord, then discarded:

haskell-backend/booster/library/Booster/Pattern/Match.hs

Lines 704 to 709 in c7e22cb

	let patMap = Map.fromList patternKeyVals
	subjMap = Map.fromList subjKeyVals
	-- handles syntactically identical keys in pattern and subject
	commonMap = Map.intersectionWith (,) patMap subjMap
	patExtra = patMap `Map.withoutKeys` Map.keysSet commonMap
	subjExtra = subjMap `Map.withoutKeys` Map.keysSet commonMap

Remaining keys are partitioned into concrete/symbolic via toRemainderMap — O(p) + O(n):

haskell-backend/booster/library/Booster/Pattern/Match.hs

Lines 626 to 635 in c7e22cb

	toRemainderMap :: [(Term, Term)] -> Maybe Term -> RemainderMap
	toRemainderMap kvs rest =
	let (conc, sym) = partitionConcreteKeys kvs
	in foldr
	(uncurry ConstructorKey)
	(Rest $ foldr (uncurry OtherKey) (maybe EmptyMap Remainder rest) sym)
	conc
	where
	partitionConcreteKeys :: [(Term, Term)] -> ([(Term, Term)], [(Term, Term)])
	partitionConcreteKeys = partition (\(Term attrs _, _) -> attrs.isConstructorLike)

Then matchRemainderMaps handles the remainder — complexity depends on structure:

haskell-backend/booster/library/Booster/Pattern/Match.hs

Lines 729 to 770 in c7e22cb

	matchRemainderMaps ::
	RemainderMap -> RemainderMap -> StateT MatchState (Except MatchResult) (Seq (Term, Term))
	-- match {K -> V, ...} with {...} where K is constructor-like
	-- if `{...}` does not contain `OtherKeys`, fail because we already matched all concrete keys, so we know `K` does not appear in {...}
	-- otherwise, one of the other keys could potentially match `K`, if `{...}` contains some OtherKey `f()` which evaluates to `K`
	matchRemainderMaps pat@(ConstructorKey patKey _ _) subj
	| not (containsOtherKeys subj) = failWith $ KeyNotFound patKey (fromRemainderMap def subj)
	| otherwise = do
	addIndeterminate (fromRemainderMap def pat) (fromRemainderMap def subj) >> pure mempty
	-- match {} with {}
	-- succeeds
	matchRemainderMaps (Rest EmptyMap) (Rest EmptyMap) = pure mempty
	-- match {} with {...REST} or {K -> V, ...}
	-- fails as the size of the maps is different and there is no substitution `subst`, s.t.
	-- subst({}) = {...REST} or {K -> V, ...}
	matchRemainderMaps (Rest EmptyMap) subj =
	failWith $
	DifferentSymbols (fromRemainderMap def (Rest EmptyMap)) (fromRemainderMap def subj)
	-- match {K -> V} with {K' -> V'} where K' is constructor-like and K is not (i.e. a variable or function)
	-- we can proceed matching because each map only has one element, so the two key/value pairs must match
	matchRemainderMaps (SingleOtherKey patKey patVal) (SingleConstructorKey subjKey subjVal) =
	pure $ Seq.fromList [(patKey, subjKey), (patVal, subjVal)]
	-- match {K -> V} with {K' -> V'} where K and K' are both non-constructor like (i.e. a variable or function)
	-- same arguemnt as above
	matchRemainderMaps (SingleOtherKey patKey patVal) (SingleOtherKey subjKey subjVal) =
	pure $ Seq.fromList [(patKey, subjKey), (patVal, subjVal)]
	-- match {K -> V, ...} with {}
	-- fails, maps are different sizes
	matchRemainderMaps pat@(Rest OtherKey{}) subj@(Rest EmptyMap) =
	failWith $ DifferentSymbols (fromRemainderMap def pat) (fromRemainderMap def subj)
	-- match {K -> V, ...} with {...REST} where {K -> V, ...} has no remainder and ...REST is a map variable
	-- fail because there is no substitution `sub` such that sub({K -> V, ...}) = {...REST}
	matchRemainderMaps (Rest pat@OtherKey{}) subj@(Rest (Remainder Var{}))
	| hasNoRemainder pat =
	failWith $ DifferentSymbols (fromRemainderMap def (Rest pat)) (fromRemainderMap def subj)
	-- match {K -> V, ...} with {...} where K is a function/variable
	-- all other cases are indeterminate
	matchRemainderMaps pat@(Rest OtherKey{}) subj = do
	addIndeterminate (fromRemainderMap def pat) (fromRemainderMap def subj) >> pure mempty
	-- match {...REST} with {...}
	-- succeeds as `...REST` is a variable of sort map or a function which evaluates to a map
	matchRemainderMaps (Rest (Remainder pat)) subj = pure $ Seq.singleton (pat, fromRemainderMap def subj)

3. Substitution

goSubst is applied to both keys and values of all pairs — O(n). Concrete keys are quickly skipped (no variables), but iteration still occurs. The result passes through the smart constructor, triggering sortAndDeduplicate — O(n log n) unconditionally:

haskell-backend/booster/library/Booster/Pattern/Substitution.hs

Lines 48 to 65 in c7e22cb

	substituteInTerm :: Substitution -> Term -> Term
	substituteInTerm substitution = goSubst
	where
	targetSet = Map.keysSet substitution
	goSubst t
	| Set.null (targetSet `Set.intersection` (getAttributes t).variables) = t
	| otherwise = case t of
	Var v -> fromMaybe t (Map.lookup v substitution)
	DomainValue{} -> t
	SymbolApplication sym sorts args ->
	SymbolApplication sym sorts $ map goSubst args
	AndTerm t1 t2 -> AndTerm (goSubst t1) (goSubst t2)
	Injection ss s sub -> Injection ss s (goSubst sub)
	KMap attrs keyVals rest -> KMap attrs (bimap goSubst goSubst <$> keyVals) (goSubst <$> rest)
	KList def heads rest ->
	KList def (map goSubst heads) (bimap goSubst (map goSubst) <$> rest)
	KSet def elements rest ->
	KSet def (map goSubst elements) (goSubst <$> rest)

haskell-backend/booster/library/Booster/Pattern/Base.hs

Line 594 in c7e22cb

newKeyVals = sortAndDeduplicate $ keyVals ++ keyVals'

4. Evaluation

traverseTerm recursively evaluates all keys and values — O(n × eval_cost). Concrete keys are already fully evaluated (no-op), but still iterated. The result again passes through the smart constructor, triggering another sortAndDeduplicate — O(n log n):

haskell-backend/booster/library/Booster/Pattern/ApplyEquations.hs

Lines 615 to 635 in c7e22cb

	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

5. Externalise

externaliseKmapUnsafe folds the pairs back into nested concat(element(k,v), ...) symbol applications — O(n):

haskell-backend/booster/library/Booster/Pattern/Base.hs

Lines 267 to 286 in c7e22cb

	externaliseKmapUnsafe :: KMapDefinition -> [(Term, Term)] -> Maybe Term -> Term
	externaliseKmapUnsafe def keyVals rest =
	case (keyVals, rest) of
	([], Nothing) -> unit
	([], Just r) -> r
	((cK, cV) : cs, Nothing) ->
	foldr
	(\(k, v) r -> (k |-> v) `con` r)
	(cK |-> cV)
	cs
	(_, Just s) ->
	foldr
	(\(k, v) r -> (k |-> v) `con` r)
	s
	keyVals
	where
	unit = SymbolApplication (stripCollectionMetadata $ unitSymbol $ KMapMeta def) [] []
	k |-> v = SymbolApplication (stripCollectionMetadata $ kmapElementSymbol def) [] [k, v]
	a `con` b = SymbolApplication (stripCollectionMetadata $ concatSymbol $ KMapMeta def) [] [a, b]
	{-# INLINE externaliseKmapUnsafe #-}

Summary

Per rule execution, sortAndDeduplicate with expensive Ord Term is called at least 2-3 times (after substitution, after evaluation, and possibly during matching), each costing O(n log n). The temporary Map.fromList conversion in matching adds another O(n log n). This is the primary performance bottleneck for large maps.

[Stevengre]

@ehildenb @palinatolmach @tothtamas28 Please let me know your thoughts.

These time costs were calculated by Claude; I did not verify each individual number myself. However, I feel that the current rewriting approach, especially constructing a Map.fromList on every match, introduces unnecessary reconstruction overhead.

Regarding Evaluation, would it make sense to trade space for time in this case? For example, we could record pointers to the locations that require evaluation when they are introduced, and then have Evaluation process only those specific locations instead of traversing everything.

I plan to open a separate issue to discuss this in more detail.

[ehildenb]

@Stevengre we would need to see the data that this is actually a performance issue. It was designed this way because generally the maps we're working with are very small, and this allows us to represent undefined maps (ones with duplicate keys) and maps with symbolic keys easily.

Do you have an example where this particular issue is the performance bottleneck? For KMIR, we've addressed that by removing the large concrete maps.

Also, is this all generated with Claude? It would be nice to have a shorter summary for humans to read, maybe one you write yourself, because otherwise it takes a long time to review this.

[Stevengre]

@ehildenb Thanks for the feedback.

I used Claude to structure the analysis to avoid missing details. I agree it was too long. Next time I’ll include a concise executive summary.

On KMIR, removing large static maps helped. My concern is whether that fix is too case-specific. In another semantics I’m working on, I still have many static maps and also a large map for dynamic variable information. That one grows significantly and lookups become slow. Additionally, I saw Map, List, Bytes in the configuration. I don't know if there are existing performance test for these types.

Before implementation, I can construct a benchmark analyzing performance of Map, List and other builtin datas. It should be useful for future optimization.

For undefined maps with duplicate keys and symbolic keys, I’d like to understand whether they must be represented directly in Map, or whether they could instead be encoded in REST.

Waht do you think?

[Stevengre]

BTW, the kompile in kmir prove-rs process to get the interpreter for the functions also costs a lot of time. But the time cost might not only be related to the store struture, but related to the time that loads json from pyk's call. I'm wondering to provide a feature that haskell-backend can produce profiling information to show optimization oppotunities. What do you think?

[ehildenb]

The haskell backend does support profiling already I think. And I think we were able to address most of the performance issue of compiling the static maps as lookup functions by stratifying the lookup functions.

The main concern I have with this work is that it does not manifest as a problem right now in the haskell backend usage we have for RV (in KEVM or KMir or KWasm), and so we don't have extra funding to pursue it. If you are able to, in your own time, make a performance optimization that benefits your other semantics and also does not degrade the performance of KMIR or KEEVM or KWasm, then that would be fine.

I do like the benchmark you submitted, let's see what Jost says.

[Stevengre]

Then, maybe I can try to provide these kind of optimization in my own time. I think it's also a good way for me to get familiar with the backend things and make me easier to improve the downstream tools.

Additionally, I'd like to investigate the current profiling structure and result. Maybe I can start providing optimization from the first bottle neck in real programs that we are doing. I can learn how to profile for Kontrol proofs, which I think should be helpful for the next engagement using Kontrol.

[Stevengre]

@ehildenb @palinatolmach @tothtamas28
If you have any other todos with higher priorities in mind, please let me know. I want to make our tools better.

[palinatolmach]

I don't have high-priority items for Haskell Backend in mind, I might need some help debugging the backend bug reports for the Solana proofs I'm looking at, will let you know. I believe we've observed degraded performance in some Kontrol engagements/demos when configurations got too big, which seemed to have been mostly caused by growing maps in cells representing memory, storage, accounts, etc., but I don't know how big of an improvement we'd get from these changes. We can use the upcoming Kontrol engagements for profiling if we observe similar behavior in those proofs, you can also see the performance tests referenced here:

haskell-backend/README.md

Line 213 in 00479fb

### Integration/Performance tests of downstream projects

- Jost and Georgy have been using those to make sure HB changes do not negatively affect Kontrol/KEVM proofs.