From 2989081179f40df43d9ba2275efb43c604db96b4 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 27 May 2026 00:37:40 +0000 Subject: [PATCH 1/4] Pattern/Util: add collectUndefinedSubterms MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Collects all maximal sub-terms of a term that are rooted at a partial (non-total, non-constructor) symbol. These sub-terms represent the definedness conditions that must hold for the enclosing rule to be applied soundly — i.e. each collected sub-term must not evaluate to bottom. Used by ApplyEquations for runtime definedness discharge. Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit 9b7b65ce2b5ed3139c4326b92f1bdbc1aa8e679a) --- booster/library/Booster/Pattern/Util.hs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/booster/library/Booster/Pattern/Util.hs b/booster/library/Booster/Pattern/Util.hs index 6e15748c13..855a4950e3 100644 --- a/booster/library/Booster/Pattern/Util.hs +++ b/booster/library/Booster/Pattern/Util.hs @@ -19,6 +19,7 @@ module Booster.Pattern.Util ( checkTermSymbols, isConcrete, filterTermSymbols, + collectUndefinedSubterms, sizeOfTerm, termVarStats, termSymbolStats, @@ -268,6 +269,18 @@ filterTermSymbols check = cata $ \case more -> filter check [concatSym, elemSym] <> fromMaybe [] rest <> concat more +{- | Collect all maximal sub-terms rooted at a partial (non-total, non-constructor) symbol. + These represent the definedness conditions: each collected sub-term must be defined + (i.e. not evaluate to bottom) for the overall term to be defined. +-} +collectUndefinedSubterms :: Term -> [Term] +collectUndefinedSubterms t@(SymbolApplication sym _ args) + | not (isDefinedSymbol sym) = [t] + | otherwise = concatMap collectUndefinedSubterms args +collectUndefinedSubterms (AndTerm l r) = collectUndefinedSubterms l <> collectUndefinedSubterms r +collectUndefinedSubterms (Injection _ _ inner) = collectUndefinedSubterms inner +collectUndefinedSubterms _ = [] + -- | Calculate size of a term in bytes sizeOfTerm :: Term -> Int sizeOfTerm = cata $ \case From 8759dfaa30f14dbd31608803303e8b3cb299459b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 27 May 2026 00:37:51 +0000 Subject: [PATCH 2/4] Pattern/ApplyEquations: add evaluateCeils mode for runtime definedness discharge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds an evaluateCeils flag to EquationConfig controlling whether the equation engine attempts to discharge definedness conditions for rules whose RHS contains partial-function applications. When evaluateCeils=True (via runEquationTWithCeils / evaluatePatternWithCeils): - Rules with notPreservesDefinednessReasons=[] proceed unconditionally (already guaranteed by the preserves-definedness attribute). - Rules with no undefined sub-terms in the RHS also proceed unconditionally. - Rules that have undefined sub-terms require runtime discharge: each partial- function sub-term is evaluated with evaluateCeils=False; if the result changed (i.e. the term was defined), the condition is considered discharged. All conditions must discharge for the rule to apply. The tryEvaluate heuristic — "if evaluating with evaluateCeils=False changes the term, it was defined" — is an under-approximation: it may miss some cases (returning false negatives), but never unsoundly accepts an undefined term. Also exports evaluatePatternWithCeils for use in the implies checker. Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit b37c3cdafcc077a82e389a9988d9cfc47660c961) --- .../library/Booster/Pattern/ApplyEquations.hs | 170 ++++++++++++++++-- 1 file changed, 156 insertions(+), 14 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 928c941afe..70c4be8f13 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -10,9 +10,11 @@ License : BSD-3-Clause module Booster.Pattern.ApplyEquations ( evaluateTerm, evaluatePattern, + evaluatePatternWithCeils, Direction (..), EquationT (..), runEquationT, + runEquationTWithCeils, EquationConfig (..), getConfig, EquationPreference (..), @@ -72,7 +74,7 @@ import Booster.Prettyprinter (renderOneLineText) import Booster.SMT.Interface qualified as SMT import Booster.Syntax.Json.Externalise (externaliseTerm) import Booster.Syntax.Json.Internalise (extractSubstitution) -import Booster.Util (Bound (..)) +import Booster.Util (Bound (..), secWithUnit, timed) import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached)) import Kore.Util (showHashHex) @@ -152,6 +154,10 @@ data EquationConfig = EquationConfig , maxLocalSteps :: Bound "LocalSteps" , logger :: Logger LogMessage , prettyModifiers :: ModifiersRep + , evaluateCeils :: Bool + -- ^ When True, attempt to discharge definedness conditions at runtime + -- by evaluating partial-function sub-terms of rule RHS with evaluateCeils=False. + -- Sound because the sub-evaluation only applies total-RHS equations. } data EquationState = EquationState @@ -349,7 +355,33 @@ runEquationT :: Set Predicate -> EquationT io a -> io (Either EquationFailure a, SimplifierCache) -runEquationT definition llvmApi smtSolver sCache known (EquationT m) = do +runEquationT = runEquationT' False + +{- | Like 'runEquationT' but with the @evaluateCeils@ flag enabled, allowing +runtime discharge of definedness conditions for rules with partial-function RHS. +-} +runEquationTWithCeils :: + LoggerMIO io => + KoreDefinition -> + Maybe LLVM.API -> + SMT.SMTContext -> + SimplifierCache -> + Set Predicate -> + EquationT io a -> + io (Either EquationFailure a, SimplifierCache) +runEquationTWithCeils = runEquationT' True + +runEquationT' :: + LoggerMIO io => + Bool -> + KoreDefinition -> + Maybe LLVM.API -> + SMT.SMTContext -> + SimplifierCache -> + Set Predicate -> + EquationT io a -> + io (Either EquationFailure a, SimplifierCache) +runEquationT' withCeils definition llvmApi smtSolver sCache known (EquationT m) = do globalEquationOptions <- liftIO GlobalState.readGlobalEquationOptions logger <- getLogger prettyModifiers <- getPrettyModifiers @@ -367,6 +399,7 @@ runEquationT definition llvmApi smtSolver sCache known (EquationT m) = do , maxLocalSteps = globalEquationOptions.maxLocalSteps , logger , prettyModifiers + , evaluateCeils = withCeils } -- NB the returned cache assumes the known predicates pure (res, endState.cache) @@ -582,6 +615,31 @@ evaluatePattern def mLlvmLibrary smtSolver cache pat = . evaluatePattern' $ pat +{- | Like 'evaluatePattern' but with the @evaluateCeils@ flag enabled. + Used during implies checking, where we may need to apply simplification + equations whose RHS contains partial-function applications. The + definedness conditions for each such equation are discharged at runtime + by evaluating them with the standard (evaluateCeils=False) evaluator and + checking whether the term changed. +-} +evaluatePatternWithCeils :: + LoggerMIO io => + KoreDefinition -> + Maybe LLVM.API -> + SMT.SMTContext -> + SimplifierCache -> + Pattern -> + io (Either EquationFailure Pattern, SimplifierCache) +evaluatePatternWithCeils def mLlvmLibrary smtSolver cache pat = + runEquationTWithCeils + def + mLlvmLibrary + smtSolver + cache + (pat.constraints <> (Set.fromList . asEquations $ pat.substitution)) + . evaluatePattern' + $ pat + -- version for internal nested evaluation evaluatePattern' :: LoggerMIO io => @@ -941,18 +999,49 @@ applyEquation term rule = logMessage ("Equation with existentials" :: Text) lift . throw . InternalError $ "Equation with existentials: " <> Text.pack (show rule) - -- immediately cancel if not preserving definedness - unless (null rule.computedAttributes.notPreservesDefinednessReasons) $ do - throwE - ( \ctxt -> - ctxt $ - logMessage $ - renderOneLineText $ - "Uncertain about definedness of rule due to:" - <+> hsep (intersperse "," $ map pretty rule.computedAttributes.notPreservesDefinednessReasons) - , RuleNotPreservingDefinedness - ) - -- immediately cancel if rule has concrete() flag and term has variables + -- Gate on definedness preservation. + -- Four cases based on (preserves-definedness attribute, definedness conditions, evaluateCeils flag): + -- + -- notPreservingReasons=[] + conditions=[] → totally defined, proceed silently + -- notPreservingReasons=[] + conditions≠[] → user set preserves-definedness, log and proceed + -- notPreservingReasons≠[] + conditions=[] → can't prove definedness, reject + -- notPreservingReasons≠[] + conditions≠[] + evaluateCeils=False → ceils disabled, reject + -- notPreservingReasons≠[] + conditions≠[] + evaluateCeils=True → defer to runtime check after match + let notPreservingReasons = rule.computedAttributes.notPreservesDefinednessReasons + definednessConditions = collectUndefinedSubterms rule.rhs + preservedByAttr = null notPreservingReasons + hasConditions = not (null definednessConditions) + case (preservedByAttr, hasConditions) of + (True, True) -> + -- user marked preserves-definedness; log so the path is visible in traces + withContext CtxDefinedness $ + logMessage ("Rule is marked as preserving definedness" :: Text) + (False, False) -> + -- no conditions to check at runtime, conservatively reject + throwE + ( \ctxt -> + ctxt $ + logMessage $ + renderOneLineText $ + "Uncertain about definedness of rule due to:" + <+> hsep (intersperse "," $ map pretty notPreservingReasons) + , RuleNotPreservingDefinedness + ) + (False, True) -> do + -- conditions present; reject now unless evaluateCeils enabled (runtime check deferred) + cfg <- lift getConfig + unless (cfg.evaluateCeils) $ + throwE + ( \ctxt -> + ctxt $ + logMessage $ + renderOneLineText $ + "Uncertain about definedness of rule due to:" + <+> hsep (intersperse "," $ map pretty notPreservingReasons) + , RuleNotPreservingDefinedness + ) + (True, False) -> pure () -- totally defined, proceed silently + -- immediately cancel if rule has concrete() flag and term has variables when (allMustBeConcrete rule.attributes.concreteness && not (Set.null (freeVariables term))) $ do throwE ( \ctxt -> ctxt $ logMessage ("Concreteness constraint violated: term has variables" :: Text) @@ -1006,6 +1095,11 @@ applyEquation term rule = Map.toList subst ) + -- when evaluateCeils is enabled and the rule has definedness conditions, + -- check them now (after match, with the substitution applied) + when (not preservedByAttr && hasConditions) $ + checkDefinednessConditions subst definednessConditions + -- check required constraints from lhs. -- Reaction on false/indeterminate varies depending on the equation's type (function/simplification), -- see @handleSimplificationEquation@ and @handleFunctionEquation@ @@ -1034,6 +1128,54 @@ applyEquation term rule = <+> hsep (intersperse "," $ map (pretty' @mods) knownTrue) pure toCheck + -- Runtime definedness discharge: for each definedness condition (a partial-function + -- sub-term of the rule's RHS, after substitution), try to evaluate it using the + -- standard equation evaluator (evaluateCeils=False — only total-RHS rules apply). + -- If the term changes, it was defined. If any condition fails, the rule is rejected. + checkDefinednessConditions :: + Map Variable Term -> + [Term] -> + ExceptT + ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) + (EquationT io) + () + checkDefinednessConditions subst conditions = withContext CtxDefinedness $ do + cfg <- lift getConfig + st <- lift getState + let substituted = map (substituteInTerm subst) conditions + (allDefined, elapsed) <- lift . (eqState . lift) . timed $ do + results <- mapM (tryEvaluate cfg st) substituted + pure $ and results + withContext CtxTiming $ + logMessage $ + WithJsonMessage (object ["time" .= elapsed]) $ + "Checked definedness conditions in " <> Text.pack (secWithUnit elapsed) + unless allDefined $ + throwE + ( \ctxt -> + ctxt $ + logMessage ("Definedness conditions could not be established" :: Text) + , RuleNotPreservingDefinedness + ) + + tryEvaluate :: + EquationConfig -> + EquationState -> + Term -> + io Bool + tryEvaluate cfg st cond = do + (result, _) <- + runEquationT + cfg.definition + cfg.llvmApi + cfg.smtSolver + st.cache + st.predicates + (evaluateTerm' BottomUp cond) + pure $ case result of + Right evaluated -> evaluated /= cond + Left _ -> False + -- Simplify given predicate in a nested EquationT execution. -- Call 'whenBottom' if it is Bottom, return Nothing if it is Top, -- otherwise return the simplified remaining predicate. From 673ad290a29430c9147310e50d50bb602c1c8eab Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 3 Jun 2026 04:56:06 +0000 Subject: [PATCH 3/4] booster/Pattern/Implies: switch MatchIndeterminate LHS-simplify to evaluatePatternWithCeils When matching during implies returns MatchIndeterminate, the handler simplifies the LHS pattern and retries; switch that simplification call from 'evaluatePattern' to 'evaluatePatternWithCeils' so the LHS-simplify pass can discharge runtime definedness side-conditions (the capability the prior commit added). No structural change to the retry logic. Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit 1c7164d5d1734fd71bf437939bc446d691613c9b) --- booster/library/Booster/Pattern/Implies.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index bf521a00e0..f2e83a3f11 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -122,7 +122,7 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = (externaliseExistTerm existsL patL.term) (externaliseExistTerm existsR patR.term) MatchIndeterminate _partialSubst _remainder -> - ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty patL >>= \case + ApplyEquations.evaluatePatternWithCeils def mLlvmLibrary solver mempty patL >>= \case (Right simplifedSubstPatL, _) -> if patL == simplifedSubstPatL then -- we are being conservative here for now and returning "not-implied". From 7ca9fd69fea8f92a40bce04b36b7d3c961af6bf2 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 27 May 2026 00:37:59 +0000 Subject: [PATCH 4/4] Pattern/Implies: simplify consequent under antecedent constraints In the MatchIndeterminate branch: after failing to change the LHS with evaluatePatternWithCeils, also attempt simplifying the RHS with the LHS constraints added to its context. If the RHS term changes, retry matching. This handles cases like hashLoc(...) => keccak(buf(...) +Bytes buf(32, 0)) where the consequent can be simplified to match the antecedent once LHS constraints are propagated. Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit 373d1446e66559bda7e860307e3f67bd9e210b10) --- booster/library/Booster/Pattern/Implies.hs | 28 +++++++++++++++------- 1 file changed, 19 insertions(+), 9 deletions(-) diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index f2e83a3f11..90a6fee7a2 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -124,16 +124,26 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = MatchIndeterminate _partialSubst _remainder -> ApplyEquations.evaluatePatternWithCeils def mLlvmLibrary solver mempty patL >>= \case (Right simplifedSubstPatL, _) -> - if patL == simplifedSubstPatL - then -- we are being conservative here for now and returning "not-implied". - -- We could return implies, but the condition will contain the remainder - -- as an equality contraint, predicating the implication on that equality being true. + if patL /= simplifedSubstPatL + then checkImpliesMatchTerms existsL simplifedSubstPatL existsR patR + else -- LHS didn't change; try simplifying RHS under LHS constraints so + -- that e.g. hashLoc("Solidity",...) can discharge its requires. - doesNotImply - (sortOfPattern patL) - (externaliseExistTerm existsL patL.term) - (externaliseExistTerm existsR patR.term) - else checkImpliesMatchTerms existsL simplifedSubstPatL existsR patR + let patRWithLhsContext = patR{constraints = patR.constraints <> patL.constraints} + in ApplyEquations.evaluatePatternWithCeils def mLlvmLibrary solver mempty patRWithLhsContext >>= \case + (Right simplifiedPatR, _) -> + if patR.term /= simplifiedPatR.term + then checkImpliesMatchTerms existsL patL existsR simplifiedPatR{constraints = patR.constraints} + else + doesNotImply + (sortOfPattern patL) + (externaliseExistTerm existsL patL.term) + (externaliseExistTerm existsR patR.term) + (Left _, _) -> + doesNotImply + (sortOfPattern patL) + (externaliseExistTerm existsL patL.term) + (externaliseExistTerm existsR patR.term) (Left err, _) -> pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err) MatchSuccess subst -> do