Skip to content

Ceil simplifier #4157

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
ehildenb wants to merge 4 commits into
base: master
Choose a base branch
from
+189 −24
Draft

Ceil simplifier #4157

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2989081
Pattern/Util: add collectUndefinedSubterms
ehildenb May 27, 2026
8759dfa
Pattern/ApplyEquations: add evaluateCeils mode for runtime definednes…
ehildenb May 27, 2026
673ad29
booster/Pattern/Implies: switch MatchIndeterminate LHS-simplify to ev…
ehildenb Jun 3, 2026
7ca9fd6
Pattern/Implies: simplify consequent under antecedent constraints
ehildenb May 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
170 changes: 156 additions & 14 deletions booster/library/Booster/Pattern/ApplyEquations.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,11 @@ License : BSD-3-Clause
module Booster.Pattern.ApplyEquations (
evaluateTerm,
evaluatePattern,
evaluatePatternWithCeils,
Direction (..),
EquationT (..),
runEquationT,
runEquationTWithCeils,
EquationConfig (..),
getConfig,
EquationPreference (..),
Expand Down Expand Up @@ -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)

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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 =>
Expand Down Expand Up @@ -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

@jberthold jberthold Jun 27, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Detail: The list being empty does not imply that the attribute is present (the other way round yes, but not this way round). There is an explicit attribute for preserves-definedness:

haskell-backend/booster/library/Booster/Definition/Attributes/Base.hs

Lines 91 to 98 in 7ca9fd6

data AxiomAttributes = AxiomAttributes
{ location :: Maybe Location
, priority :: Priority -- priorities are <= 200
, ruleLabel :: Maybe Label
, uniqueId :: UniqueId
, simplification :: Flag "isSimplification"
, preserving :: Flag "preservingDefinedness" -- this will override the computed attribute
, concreteness :: Concreteness

and if it is set we don't start computing the list, but the list can also just be empty.

Suggested change
preservedByAttr = null notPreservingReasons
preservedByAttr = coerce rule.attributes.preserving

hasConditions = not (null definednessConditions)
case (preservedByAttr, hasConditions) of

@jberthold jberthold Jun 27, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Given the above, maybe pull the preserves-definedness logging out to cut this short (and make the logic of the case easier to understand).

if (coerce rule.attributes.preserving)
then logMessage ... 
else 
case (notPreservingReasons, definednesConditions) of
        ([], []) -> pure () -- proceed silently
        (reasons, []) -> -- no conditions to check at runtime (but reasons present), conservatively reject
        (reasons, ts) -> -- conditions present, reject unless evaluateCeils

The case that was previously logged (no reasons but definednessConditions) falls into the last case here but is not reached when the rule is marked.

(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)
Expand Down Expand Up @@ -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@
Expand Down Expand Up @@ -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.
Expand Down
30 changes: 20 additions & 10 deletions booster/library/Booster/Pattern/Implies.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,18 +122,28 @@ 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".
-- 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
Expand Down
13 changes: 13 additions & 0 deletions booster/library/Booster/Pattern/Util.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ module Booster.Pattern.Util (
checkTermSymbols,
isConcrete,
filterTermSymbols,
collectUndefinedSubterms,
sizeOfTerm,
termVarStats,
termSymbolStats,
Expand Down Expand Up @@ -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 _ = []
Comment on lines +277 to +282

@jberthold jberthold Jun 27, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are missing cases: known elements of a KList or KSet and keys as well as values of a KMap must be collected as well.


-- | Calculate size of a term in bytes
sizeOfTerm :: Term -> Int
sizeOfTerm = cata $ \case
Expand Down