Repository navigation
Ceil simplifier - #4157
Draft
ehildenb wants to merge 6 commits into
Draft
Ceil simplifier#4157ehildenb wants to merge 6 commits into
ehildenb wants to merge 6 commits into
Conversation
…ss checking design Design exploration of how Booster should decide that applying an equation/simplification rule is sound w.r.t. definedness, statically (load) and dynamically (apply). Describes the current master implementation (load-time flagging + static rewrite-rule ceil analysis, with non-empty residuals discarded, and an outright reject of any still-flagged rule at apply time), then a proposed redesign and the soundness analysis behind it. Resolution (synthesised from matching/reachability-logic literature, the booster git history, and the in-repo docs): the obligation #Ceil(LHS) => #Ceil(RHS), read in assume-defined mode, is the correct one for symbolic execution (matches Kore's assumeDefined behaviour); the unconditional conjunction is the blind-application stance and is over-strong. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…uations,Syntax/ParsedKore/Internalise}, unit-tests: gate rule application on a definedness residual Reimplement the definedness check using a residual attached to each rule instead of the boolean notPreservesDefinednessReasons gate, preserving master's behaviour exactly. - Add RewriteRule.definednessResidual :: [Either Predicate Term] (Left p = residual predicate, Right t = unresolved #Ceil(t)); the rule preserves definedness (may be applied) iff it is empty. - Add Pattern.Util.collectUndefinedSubterms, mirroring filterTermSymbols's traversal case-for-case (incl. collections), so it is empty exactly when the partial-symbol scan is. - Populate the residual at load, per rule kind, to match master's decision exactly: rewrite uses the implication residual computed in Definition/Ceil (which now attaches it rather than discarding non-empty ones); function uses #Ceil of the args(LHS)+RHS partial subterms (total-head/preserving exempt); simplification uses #Ceil of the LHS+RHS partial subterms. - Switch the applyEquation gate from `null notPreservesDefinednessReasons` to `null definednessResidual`. notPreservesDefinednessReasons is retained for the abort message and to select which rewrite rules Ceil refines. Behaviour-preserving: 980 unit tests pass; the residual's emptiness is bit-exact to the previous gate per rule kind. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…e kinds, per-kind formula Route function and simplification rules through computeCeil at load (like rewrite rules already are), so definedness residuals are stored uniformly and the per-kind formula becomes a single knob to experiment with. - Add DefinednessFormula = Implication | ConjunctionArgs | Conjunction. - Extract computeRuleResidual: polymorphic in the rule tag, computes the residual under the given formula and attaches it (marking the rule preserving when it discharges to empty). computeCeilRule is now a thin rewrite-only wrapper that also emits the logging summary. - computeCeilsDefinition now also walks functionEquations and simplifications: rewrite -> Implication, function -> ConjunctionArgs (#Ceil(args)∧#Ceil(rhs), excluding the function head), simplification -> Conjunction (#Ceil(lhs)∧#Ceil(rhs)). This is a behaviour change (not bit-exact) for function/simplification: rules whose ceils discharge at load (concrete arithmetic, concrete collection distinctness, explicit #Ceil rules) now apply instead of being rejected. Symbolic partial subterms (incl. KEVM's LHS-partial declines) still reject, so the conservative behaviour and the KEVM fallbacks are unchanged. Internalise keeps its raw-scan residual as the fallback for definition-loading paths that do not run computeCeilsDefinition (e.g. unit tests), which is why the 980 unit tests are unaffected; the new formulas are exercised at the server and want booster/KEVM integration validation. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ation When a rule is blocked by a non-empty static definedness residual, attempt to discharge it dynamically against the match before rejecting the rule. - EquationConfig gains dischargeDefinedness (default True via runEquationT); it is flipped off for the discharge's own nested simplification, so the attempt is at most one level deep (no recursive dynamic discharge). - The applyEquation gate no longer rejects a non-empty residual up front when discharge is enabled: it defers to after matching (where the substitution is available) and there calls dischargeDefinednessResidual; only if that fails is the rule rejected. With discharge disabled (the nested case) the pre-match reject is kept. - dischargeDefinednessResidual substitutes the match into each residual obligation and simplifies it in an *isolated* runEquationT (copied cache/known predicates, fresh iteration state) so it cannot corrupt the outer evaluation, with discharge disabled. An obligation is satisfied when a #Ceil(t) term simplifies to one with no partial sub-terms (the load-time "trivially defined" check) or a predicate simplifies to true. This is the dynamic counterpart to the static (load-time) ceil simplification: a rule whose residual only clears once the match is known (e.g. #newAddr(a,b) with concrete arguments evaluating to an address) now applies. 980 unit tests pass; the negative path (non-dischargeable partials such as a symbolic f2 stay rejected) is covered, and the isolation fix prevents the outer-traversal corruption an in-place nested simplify caused. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adds a small self-contained definition (dischargeDef) and two cases: - a rule con3(f2(X), Y) => Y carrying residual #Ceil(f2(X)) fires for con3(f2(con2(A)), B) because the match makes f2(con2(A)) reduce to a defined term; - it stays blocked for con3(f2(con1(A)), B), where f2(con1(A)) has no rule and the residual cannot be discharged. The positive case genuinely requires dynamic discharge: without it the rule's non-empty residual would reject it outright. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…atus and decisions (§9) Document what is built on this branch (residual storage, uniform per-kind static computation, dynamic discharge), the decisions taken autonomously (always-on dynamic discharge with a one-level guard, isolated runEquationT for the nested simplify, the load-time "trivially defined" discharge check with no SMT yet, the internalise raw-scan fallback, retaining notPreservesDefinednessReasons), the behaviour change vs master, and the outstanding integration/KEVM validation. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
jberthold
reviewed
Jun 27, 2026
| -- notPreservingReasons≠[] + conditions≠[] + evaluateCeils=True → defer to runtime check after match | ||
| let notPreservingReasons = rule.computedAttributes.notPreservesDefinednessReasons | ||
| definednessConditions = collectUndefinedSubterms rule.rhs | ||
| preservedByAttr = null notPreservingReasons |
Collaborator
There was a problem hiding this comment.
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
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 |
| definednessConditions = collectUndefinedSubterms rule.rhs | ||
| preservedByAttr = null notPreservingReasons | ||
| hasConditions = not (null definednessConditions) | ||
| case (preservedByAttr, hasConditions) of |
Collaborator
There was a problem hiding this comment.
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.
Comment on lines
+277
to
+282
| 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 _ = [] |
Collaborator
There was a problem hiding this comment.
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.
ehildenb
force-pushed
the
ceil-simplifier
branch
from
September 30, 2026 13:31
7ca9fd6 to
a4fa98c
Compare
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.