From 645b7be3faabf905508f182ef5a4aae891d122d3 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 19 Jun 2026 22:02:36 +0000 Subject: [PATCH 1/6] docs/2026-06-19-definedness-checking-design: static+dynamic definedness 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 --- .../2026-06-19-definedness-checking-design.md | 233 ++++++++++++++++++ 1 file changed, 233 insertions(+) create mode 100644 docs/2026-06-19-definedness-checking-design.md diff --git a/docs/2026-06-19-definedness-checking-design.md b/docs/2026-06-19-definedness-checking-design.md new file mode 100644 index 0000000000..bb892b76f2 --- /dev/null +++ b/docs/2026-06-19-definedness-checking-design.md @@ -0,0 +1,233 @@ +# Definedness checking in Booster — static vs dynamic, and the right obligation + +Status: design exploration, 2026-06-19. +This document describes how `master` checks definedness today (§2), a proposed redesign (§3), the soundness question it raises (§4–§7), and a synthesis resolving it (§8) from three research threads (matching/reachability-logic literature, booster git history, in-repo docs). +Resolution: the implication `#Ceil(LHS) → #Ceil(RHS)` ("preserves definedness"), read in assume-defined mode, is the correct obligation for symbolic execution — see §8. + +This document works out *how Booster should decide that applying an equation/simplification rule is sound with respect to definedness*, statically (at load) and dynamically (at rule-application time). +It is motivated by KEVM's recurring definedness fallbacks: Booster declines a simplification that involves a partial symbol and falls back to the complete (but slow) Kore engine, even in cases where the rule is in fact sound to apply. + +## 1. Background: what "definedness" buys us + +Booster rewrites/simplifies terms by applying equations `LHS = RHS requires P`. +Some symbols are *partial* (`[function]`, not `[total]`): an application like `X /Int Y` or `#newAddr(A,B)` may denote nothing (⊥) for some arguments. +Applying an equation that involves a partial symbol can be unsound unless we know the relevant definedness conditions hold. +Booster's conservative stance today: if a rule mentions a partial symbol it cannot statically discharge, it *declines* (aborts) and the proxy falls back to Kore. +A large fraction of KEVM's Booster→Kore fallbacks are exactly these definedness declines. + +## 2. The current implementation on `master` + +It helps to separate what is computed once at load, what is stored on the rule, and what is computed on every rule application. + +**Computed once, at load (internalisation):** + +- `notPreservesDefinednessReasons` — a *blame list* of the partial-symbol names found in the rule, computed for every rule kind. + Rewrite and function rules scan the **RHS only** (`booster/library/Booster/Syntax/ParsedKore/Internalise.hs:828`). + Simplification rules scan **both LHS and RHS** (`Internalise.hs:892`, comment: *"checking the lhs term, too, as a safe approximation (rhs may introduce undefined, lhs may hide it)"*). + It is a list of symbol *names* — a yes/no-with-blame flag, not a condition. +- The static ceil analysis `computeCeilsDefinition` (`Booster/Definition/Ceil.hs`, PR #402), run unconditionally at startup (`Server.hs:245`, `booster-dev/Server.hs:79`) over the **rewrite theory only**. + For each flagged rewrite rule it computes the residual `simplify( computeCeil(rhs) ∖ computeCeil(lhs) ∖ computeCeil(requires) )` — i.e. `#Ceil(RHS)` under `#Ceil(LHS) ∧ requires` (this is "Model A" of §4). + +**Stored on the rule:** + +- The blame list, in `computedAttributes.notPreservesDefinednessReasons`. +- The static ceil analysis result is stored **only as a mutation** of the rule: when the computed residual is empty, the rule is rewritten to `preserving = True` and the blame list is cleared, so the rule then applies freely. + The residual itself is **not** stored — `RewriteRule` has no field for it — and when the residual is **non-empty it is discarded** (logged as a `ComputeCeilSummary` only; `newRule = Nothing`; the comment at `Ceil.hs:125` notes that attaching it is future work). +- `simplifications` and `functionEquations` get **no** ceil analysis at all, so for them only the blame list is stored. + +**Computed at every rule / equation / simplification application:** + +- Nothing definedness-related is recomputed. + The gate (`ApplyEquations.hs:716`) is a single read of the stored blame list: + `unless (null rule.computedAttributes.notPreservesDefinednessReasons) $ throwE … RuleNotPreservingDefinedness`. + Any rule still flagged after the load-time analysis is **rejected outright** — there is no runtime discharge of any kind. + `RuleNotPreservingDefinedness` routes through the `ResultHandler`: function equations → `abort`, simplification equations → `continue` (skip to the next rule), and in practice the proxy falls back to Kore. + +**Consequence.** +Rewrite rules can be cleared by the static analysis; simplification and function rules never are. +So a simplification rule declines whenever it carries any partial symbol on either side. +The dominant KEVM definedness fallbacks (`#newAddr`, `_< true` | `#Ceil(#newAddr(A,B)) → #Top` = **#Top** | `#Ceil(#newAddr(A,B))` | partial symbol in **LHS**, RHS total | +| `0 <=Int (X < true` | `(Y>=0) → #Top` = **#Top** | `Y>=0` | partial symbol in **LHS** | +| `X => 1 /Int X` | `#Top → (X=/=0)` = **X=/=0** | `X=/=0` | partial symbol introduced in **RHS** | + +Key observation: A and B agree when the partiality is *introduced in the RHS*, but diverge when it is *in the matched LHS*. +For the LHS cases, Model A declares the rule definedness-preserving (residual `#Top`, apply freely), while Model B demands a runtime `#Ceil` discharge. +The KEVM declines are overwhelmingly LHS cases — so under Model A they would simply be recognised as preserving definedness at load and applied with no runtime work, and today's declines are an artefact of the conservative "any partial symbol ⇒ bail" approximation (`master` never even computes the implication for simplification rules). + +If Model A is the correct soundness model, then: +- the redesign's load-time step should compute and simplify `#Ceil(LHS) ⟹ #Ceil(RHS)`; +- most KEVM declines vanish at load with no runtime discharge needed; +- the only rules needing a *runtime* residual check are those where the implication does not statically reduce to `#Top` (typically RHS-introduced partiality, e.g. `1 /Int X`), and there the residual is discharged against the path condition / σ. + +If Model B is correct (no assume-defined), the implication is unsound for the LHS-hiding case and the obligation must be the conjunction. + +This is the question §8 settles. +It hinges on the semantics of symbolic execution in matching/reachability logic: is the configuration assumed defined, and does `#Ceil(config) → #Ceil(subterm)` hold for the subterms we simplify (i.e. is ordinary symbol application strict w.r.t. ⊥)? + +## 5. Static vs dynamic, restated + +- **Static (load):** for each rule, build the definedness obligation (A or B per §4), simplify with the `#Ceil` machinery (`booster/library/Booster/Definition/Ceil.hs`) and totality information. + Outcome is either `#Top` (no check ever needed) or a residual predicate attached to the rule. + No σ and no path condition are available yet, so conditional obligations remain symbolic. +- **Dynamic (apply, post-match):** substitute σ into the residual, simplify, and discharge — by structural trivially-defined check, by reduction to a domain value, and/or by SMT against the known constraints / path condition. + Accept → apply the rule; fail → abort indeterminate and let the caller (function-equation vs simplification vs rewrite vs implies) decide. + +## 6. The "trivially defined" checker + +`#Ceil(t) = #Top` when `t` is built entirely from total functions, constructors, domain values, and variables (a variable denotes a defined element of its sort; ordinary application of total/constructor symbols to defined args is defined). +Operationally this is a structural check: `t` has no maximal sub-term rooted at a partial (`Function Partial`) symbol — a recursion over `isDefinedSymbol` (`booster/library/Booster/Pattern/Util.hs:200`). +The same check serves both the load-time residual computation and the runtime accept-test. +(Settled in §8: a free variable is always `#Ceil`-true — the matching-logic `∀x. ⌈x⌉` axiom — so variables need no special handling beyond freshly-introduced existentials.) + +## 7. Open research questions (driving the three threads) + +These drove the research; §8 answers them. + +1. **Literature (matching/reachability logic).** + In reachability-logic symbolic execution, is the configuration assumed defined? + Is `#Ceil(LHS)` assumable when simplifying a subterm of a defined configuration (does `#Ceil(C[t]) → #Ceil(t)` hold; is application strict w.r.t. ⊥)? + What is the standard "preserves definedness" / equation-application soundness obligation — implication, conjunction, or other? +2. **Git history (haskell-backend + the former hs-backend-booster repo).** + How did `notPreservesDefinednessReasons`, the `preserves-definedness` attribute, the static `#Ceil` analysis, and `assumeDefined` evolve? + What rationale was recorded for the conservative check vs an assume-defined model? +3. **In-repo docs.** + What do the existing docs say about definedness, `#Ceil`, totality/partiality, `assumeDefined`, and the assumptions made about the configuration being defined? + +## 8. Synthesis: how to check definedness safely (static + dynamic) + +Synthesised from three research threads: matching/reachability-logic literature, the booster git history (incl. the former `hs-backend-booster` repo), and the in-repo docs. +Bottom line up front: **Model A is the correct obligation for symbolic execution**, provided it is read in "assume-defined" mode — which is precisely the mode symbolic execution operates in, and the mode the complete engine (Kore) already uses. +The §4 "Model B" conjunction is the *blind-application* stance and is needlessly strict here. +The literature's "preserve-bottom" contract is also real, but it is a *different mode* (see below), not a refutation of Model A. + +### 8.1 The two soundness modes + +There are two distinct, each-internally-sound contracts for replacing a matched `LHS[σ]` with `RHS[σ]`, and they correspond to two different operating assumptions: + +- **Blind application — "preserve bottom": `#Ceil(RHS) → #Ceil(LHS)`** (equivalently `LHS = ⊥ ⟹ RHS = ⊥`). + Sound *without* knowing anything about the redex's definedness: if you might be rewriting a ⊥ redex, the result must also be ⊥ so you never fabricate definedness. + This is exactly what the **K User Manual requires of `simplification` rules** ("the RHS must be `#Bottom` when the LHS is `#Bottom`, or a `requires`/`ensures` clause must be false when the LHS is `#Bottom`"). + It is a *frontend well-formedness* contract so a rule can be applied by the simplifier wherever it matches, with no σ and no configuration in hand. + +- **Assume-defined application — Model A: `#Ceil(LHS) → #Ceil(RHS)`** (equivalently: discharge `#Ceil(RHS)` under the assumptions `#Ceil(LHS) ∧ requires`). + Sound *given* that the redex is known defined. + Under that assumption it reduces to "the rule must not introduce new undefinedness in its result" — i.e. each rule must **preserve** definedness. + +These two are logically duals, not the same statement, and they genuinely differ for rules whose partial symbol sits in the **LHS** with a total RHS (the KEVM pattern): preserve-bottom *rejects* such a rule, assume-defined *accepts* it. +Note also that "discharge `#Ceil(RHS)` under assumption `#Ceil(LHS)`" is logically identical to "prove `#Ceil(LHS) → #Ceil(RHS)`" — so the literature thread's "correct obligation" and Model A are the same thing; the only substantive literature finding is that K's *blind* contract is the converse. + +### 8.2 Why assume-defined is the right mode for Booster (and is sound) + +1. **⊥-strictness of application (general, not symbol-specific).** + In matching logic, symbol application is interpreted pointwise with `∅ • A = A • ∅ = ∅` (Roșu, *Matching Logic Explained*, Def. 2.3–2.4; OOPSLA'16 Def. 3). + Hence `#Ceil(f(t₁,…,tₙ)) → #Ceil(t₁) ∧ … ∧ #Ceil(tₙ)` for **every** symbol `f` (total or partial). + So a subterm of a defined term is itself defined: `#Ceil(C[t]) → #Ceil(t)`. + (The converse, `⋀#Ceil(tᵢ) → #Ceil(f(t̄))`, holds only for total/constructor `f` — that is precisely the §6 "trivially defined" checker.) + +2. **Symbolic execution reasons about *defined instances*.** + A symbolic state `t ∧ P` denotes `{ρ(t) | ρ ⊨ P}`; for valuations where any partial subterm is ⊥, `ρ(t) = ⊥` and that valuation contributes nothing — it is silently excluded (reachability-logic semantics; One-Path/All-Path papers use a total state model with no ⊥-configuration). + So assuming `#Ceil(config)` — and therefore, by (1), `#Ceil(LHS[σ])` at any configuration subterm — does not lose soundness: the only instances it "ignores" are the vacuous ⊥ ones the claim never quantified over. + This is the standard meaning of Kore's `assumeDefined` `SideCondition`. + +3. **It matches the complete engine, empirically.** + The KEVM declines are *rescued by Kore*. + Kore applies `0 <=Int #newAddr(A,B) => true` etc. precisely because it operates in assume-defined mode. + Matching Kore's behaviour is the goal, so Model A is the target. + +4. **The codebase already committed to this — statically.** + The 2023 ceil work (PR #402, `Booster/Definition/Ceil.hs`) computes the residual as `ceil(RHS) ∖ ceil(LHS) ∖ ceil(requires)` — the set-difference *is* Model A (partial symbols shared by LHS cancel, i.e. `#Ceil(LHS)` is assumed). + Its commit message states the assumption in the open: *"we … assume (but should eventually check) that the given configuration is defined."* + So the static analyzer is Model A; only the runtime application gate stayed cruder/conservative (reject any partial symbol it can't statically clear), which is the gap this redesign closes. + +Conclusion: read `#Ceil(LHS) → #Ceil(RHS)` as "discharge `#Ceil(RHS)` assuming the redex (and `requires`) — the redex being defined for free from the assume-defined configuration." That is sound for symbolic execution and is what we want. + +### 8.3 What this means for the KEVM cases + +- `0 <=Int #newAddr(A,B) => true`, `0 <=Int (X < true`, `#lookup((K1|->V) M, K1) => V` (partial symbol in LHS, total/defined RHS): residual `#Ceil(RHS) ∖ #Ceil(LHS) = #Top`. + **Apply freely; no runtime discharge needed.** + The current decline is purely the conservative gate; under Model A these never even produce an obligation. + In particular the genuinely-partial LHS arithmetic (`X < 1 /Int X` and other **RHS-introduced** partiality: residual `#Ceil(1 /Int X) = (X =/= 0)` survives the set difference. + This is the one family that needs a **runtime** discharge of the residual against σ + the path condition (SMT) — the KEVM-team ask in `kevm-doc.md` §5.3, but now scoped to *only* RHS-introduced partiality, not the whole problem. +- "Semantically total but declared `[function]`" symbols (`#newAddr`, `#WordPack*`, `#hashedLocation`, `#bufStrict`): these are an **annotation issue**. + Marking them `[total]` makes both modes agree (`#Ceil(f(defined args)) = #Top`, and preserve-bottom holds trivially) and is the clean fix the KEVM team already plans. + Model A buys correctness here without the annotation, but `[total]` is still the right hygiene. + +### 8.4 Recommended design (static + dynamic) + +**Static (load), per rule:** +- Compute the Model A residual `R = simplify( #Ceil(RHS) ∖ #Ceil(LHS) ∖ #Ceil(requires) )`, reusing/extending the existing `Definition/Ceil.hs` machinery (this already exists for rewrite rules; generalise to the other rule kinds and store the result). +- If `R = ∅`/`#Top`: mark the rule definedness-preserving — applies with no runtime check. +- Else: attach the residual predicate `R` (a conjunction of `#Ceil(partial subterm)` over RHS-introduced partiality) to the rule (a new field on the rule, which does not exist today). +- This replaces the load-time *symbol-name blame list* with a real symbolic obligation, and drops the conservative LHS∪RHS scan: LHS-only partiality must **not** flag the rule (it is discharged by assume-defined). + +**Dynamic (apply), only for rules carrying a residual `R`, after a successful match:** +- Substitute σ into `R`. +- Discharge by: (a) structural trivially-defined check (the term has no partial-symbol subterm after simplification — §6, covering reduction to DVs/variables/total terms), then (b) if a symbolic predicate remains, check it against the known constraints / path condition via SMT (the existing `checkRequires` machinery, and the implies endpoint's SMT discharge, are the model). +- Accept → apply the rule; fail → abort *indeterminate* and let the caller (function-eqn / simplification / rewrite / implies) decide (function-eqn priorities are binding → abort; simplification priorities advisory → continue to next rule). + +### 8.5 Caveats and guardrails + +- **No circular assume-defined.** + Assume-defined is valid for subterms of the configuration we are simplifying/proving about; it must **not** be used while computing a term's *own* definedness (that would assume what we are trying to decide). + The nested evaluation used to discharge a residual must run with the definedness assumption **off** — i.e. one level deep, never recursing into another ceil-discharge. +- **Per-site applicability.** + Assume-defined is justified where the redex is genuinely a subterm of an assumed-defined configuration (execute/simplify of the state, implies under `assumeDefined`). + It is *less* obviously justified for arbitrary internal evaluations, so the discharge should be controllable per call-site (implies / equation evaluation / simplification / rewrite side conditions) and switched on only where the premise holds; default off / opt-in. +- **Empirical caution (the #440 revert).** + When the inferred-definedness marking was first enabled (PR #426) it fired a rule that introduced an existential/`?`-variable (`Ex#Var'Ques'STORAGE`) and broke a Kontrol/Optimism proof; it was reverted (#440) and only re-landed (#441) once understood. + So loosening the gate has a track record of surfacing interactions with existential/question-mark variables — roll out opt-in, and test against Kontrol/KEVM before flipping defaults. +- **`requires` vs definedness are orthogonal.** + Under assume-defined, LHS-position partiality contributes *no* definedness obligation; the side conditions that look definedness-shaped (`0 <=Int Y` for a shift) are really *correctness* `requires` discharged by `checkRequires`/SMT as today. + Do not double-count them as definedness residuals. + +### 8.6 Correction to §4 + +§4's "Model A" is the right target; its worked-examples table is correct once read in assume-defined mode (the LHS-partial rows really do reduce to `#Top` and should apply freely). +§4's "Model B" (the unconditional conjunction) is the *blind-application* obligation and is over-strong for symbolic execution — it would force needless `#Ceil(LHS)` discharges that assume-defined gives for free. +The only genuine residual to discharge at runtime is RHS-introduced partiality (`#Ceil(RHS) ∖ #Ceil(LHS) ∖ #Ceil(requires)`), against the path condition. + +### 8.7 Source pointers + +- K User Manual — `simplification` rules must preserve `#Bottom` (the blind-application contract): kframework.org/docs/user_manual. +- Roșu, *Matching Logic* (LMCS 2017) and *Matching Logic Explained* (JLAMP 2021) — `⌈_⌉` semantics, the `∀x. ⌈x⌉` definedness axiom, total vs partial symbol axioms, the `⌈x/y⌉ = (y ≠ 0)` example; OOPSLA'16 *Semantics-Based Program Verifiers* — set-valued application and `∅`-strictness. +- One-Path (LICS'13) / All-Path (RTA'14) reachability logic — total state model; symbolic states as denotation sets; vacuity of ⊥ instances. +- This repo: `booster/library/Booster/Definition/Ceil.hs` (PR #402, the static Model-A residual via `ceil(RHS) ∖ ceil(LHS) ∖ ceil(requires)`, with the explicit "assume the configuration is defined … should eventually check"); `Internalise.hs:892` (the conservative LHS∪RHS load scan to be replaced); `ApplyEquations.hs:716` (`master`'s binary definedness gate, to be replaced); PRs #426/#440/#441 (the empirical-caution episode); `docs/2020-06-17-Checking-Implication.md` (the in-repo note that checking `⌈t(X)⌉ ∧ P(X)` "could … infer that the configuration is defined, allowing … subsequent rewriting without generating extra definedness conditions" — assume-defined, in our own docs). From 934351fe16b11c72efd93110c4b20331ebcb5103 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 19 Jun 2026 22:43:12 +0000 Subject: [PATCH 2/6] booster/{Definition/Base,Definition/Ceil,Pattern/Util,Pattern/ApplyEquations,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 --- booster/library/Booster/Definition/Base.hs | 5 ++ booster/library/Booster/Definition/Ceil.hs | 14 +++-- .../library/Booster/Pattern/ApplyEquations.hs | 5 +- booster/library/Booster/Pattern/Util.hs | 55 +++++++++++++++++++ .../Booster/Syntax/ParsedKore/Internalise.hs | 22 ++++++++ .../Test/Booster/Pattern/ApplyEquations.hs | 15 ++++- .../Test/Booster/Pattern/Rewrite.hs | 1 + 7 files changed, 106 insertions(+), 11 deletions(-) diff --git a/booster/library/Booster/Definition/Base.hs b/booster/library/Booster/Definition/Base.hs index fc9766d795..1ee712a811 100644 --- a/booster/library/Booster/Definition/Base.hs +++ b/booster/library/Booster/Definition/Base.hs @@ -74,6 +74,11 @@ data RewriteRule (tag :: k) = RewriteRule , attributes :: AxiomAttributes , computedAttributes :: ComputedAxiomAttributes , existentials :: Set Variable + , definednessResidual :: [Either Predicate Term] + -- ^ leftover definedness obligations: the rule preserves definedness (may be + -- applied) iff this is empty (≡ @#Top@). A @Left p@ is a residual predicate, a + -- @Right t@ an unresolved @#Ceil(t)@. Computed at load (see + -- 'Booster.Syntax.ParsedKore.Internalise' and 'Booster.Definition.Ceil'). } deriving stock (Eq, Ord, Show, GHC.Generic) deriving anyclass (NFData) diff --git a/booster/library/Booster/Definition/Ceil.hs b/booster/library/Booster/Definition/Ceil.hs index 370d9e5cbe..bf4325a3f7 100644 --- a/booster/library/Booster/Definition/Ceil.hs +++ b/booster/library/Booster/Definition/Ceil.hs @@ -115,16 +115,18 @@ computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attribut { rule = r , ceils = requiresCeils <> rhsCeils , newRule = - if null requiresCeils && null rhsCeils - then - Just + Just $ + if null requiresCeils && null rhsCeils + then -- implication residual empty: rule preserves definedness + r { RewriteRule.attributes = attributes{preserving = Flag True} , RewriteRule.computedAttributes = computedAttributes{notPreservesDefinednessReasons = []} + , RewriteRule.definednessResidual = [] } - else -- we could add a case when ceils are fully resolved into predicates, which we would then - -- add to the requires clause of a rule - Nothing + else -- attach the leftover implication residual; the rule is applied + -- only where this discharges (currently: never, matching master) + r{RewriteRule.definednessResidual = Set.toList (requiresCeils <> rhsCeils)} } case res of diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 928c941afe..d4b232261c 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -941,8 +941,9 @@ 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 + -- immediately cancel if the rule has a non-empty definedness residual + -- (i.e. its definedness obligation does not reduce to #Top) + unless (null rule.definednessResidual) $ do throwE ( \ctxt -> ctxt $ diff --git a/booster/library/Booster/Pattern/Util.hs b/booster/library/Booster/Pattern/Util.hs index 6e15748c13..689d76dbad 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,60 @@ filterTermSymbols check = cata $ \case more -> filter check [concatSym, elemSym] <> fromMaybe [] rest <> concat more +{- | Collect the maximal sub-terms rooted at a partial (non-total, non-constructor) + symbol — the rule's runtime definedness obligations (each collected term must not + evaluate to bottom). The traversal mirrors @'filterTermSymbols' (not . 'isDefinedSymbol')@ + case-for-case, so the result is empty exactly when that scan finds no partial symbol; + where the scan would report a (partial) collection meta-symbol, the whole collection + term is returned as the obligation. +-} +collectUndefinedSubterms :: Term -> [Term] +collectUndefinedSubterms = go + where + partial = not . isDefinedSymbol + go t = case t of + SymbolApplication sym _ args + | partial sym -> [t] + | otherwise -> concatMap go args + AndTerm t1 t2 -> go t1 <> go t2 + DomainValue{} -> [] + Var{} -> [] + Injection _ _ inner -> go inner + KMap def [] Nothing -> [t | partial (unitSymbol $ KMapMeta def)] + KMap def [(k, v)] Nothing -> go k <> go v <> [t | partial (kmapElementSymbol def)] + KMap _ [] (Just rest) -> go rest + KMap def kvs rest -> + [t | partial (concatSymbol $ KMapMeta def) || partial (kmapElementSymbol def)] + <> concatMap (\(k, v) -> go k <> go v) kvs + <> maybe [] go rest + KList def heads Nothing -> case heads of + [] -> [t | partial (unitSymbol $ KListMeta def)] + [x] -> [t | partial (klistElementSymbol def)] <> go x + more -> + [t | partial (concatSymbol $ KListMeta def) || partial (klistElementSymbol def)] + <> concatMap go more + KList def heads (Just (mid, tails)) -> + go mid + <> ( let ends = heads <> tails + in if null ends + then [] + else + [t | partial (concatSymbol $ KListMeta def) || partial (klistElementSymbol def)] + <> concatMap go ends + ) + KSet def elements rest -> case elements of + [] -> maybe [t | partial (unitSymbol $ KSetMeta def)] go rest + [single] -> + go single + <> maybe + [t | partial (klistElementSymbol def)] + (\r -> [t | partial (concatSymbol $ KSetMeta def) || partial (klistElementSymbol def)] <> go r) + rest + more -> + [t | partial (concatSymbol $ KSetMeta def) || partial (klistElementSymbol def)] + <> maybe [] go rest + <> concatMap go more + -- | Calculate size of a term in bytes sizeOfTerm :: Term -> Int sizeOfTerm = cata $ \case diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 4031315d62..cb6b5c07fe 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -847,6 +847,12 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do , attributes = axAttributes , computedAttributes , existentials + , -- conservative RHS-scan residual; refined to the implication residual + -- (#Ceil(RHS) \ #Ceil(LHS) \ #Ceil(requires)) by Booster.Definition.Ceil + definednessResidual = + if coerce axAttributes.preserving + then [] + else map Right (Util.collectUndefinedSubterms rhs) } where mkVar (name, sort) = do @@ -915,6 +921,12 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs , attributes , computedAttributes , existentials = Set.empty + , -- conjunction-form residual over LHS and RHS, matching the + -- LHS∪RHS partial-symbol scan above (no LHS subtraction) + definednessResidual = + if coerce attrs.preserving + then [] + else map Right (Util.collectUndefinedSubterms lhs <> Util.collectUndefinedSubterms rhs) } | otherwise = -- we hit a simplification with top level ML connective or an @@ -960,6 +972,7 @@ internaliseCeil partialDef left right sortVars attrs = do , attributes , computedAttributes , existentials = Set.empty + , definednessResidual = [] -- ceil axioms preserve definedness by construction } where uninternaliseCollections (Def.KMap def keyVals rest) = Def.externaliseKmapUnsafe def keyVals rest @@ -1059,6 +1072,15 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att , attributes , computedAttributes , existentials = Set.empty + , -- residual over the LHS arguments and RHS, matching the + -- args(LHS)∪RHS scan above (total-head/preserving exempt) + definednessResidual = + if coerce attrs.preserving || functionSymbolIsTotal lhs + then [] + else + map + Right + (concatMap (Util.collectUndefinedSubterms . snd) argPairs <> Util.collectUndefinedSubterms rhs) } where functionSymbolIsTotal = \case diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index 0839726ccf..cadf2db2aa 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -37,7 +37,7 @@ import Booster.Pattern.ApplyEquations import Booster.Pattern.Base import Booster.Pattern.Bool import Booster.Pattern.Index (CellIndex (..), TermIndex (..)) -import Booster.Pattern.Util (sortOfTerm) +import Booster.Pattern.Util (collectUndefinedSubterms, sortOfTerm) import Booster.SMT.Interface (noSolver) import Booster.Syntax.Json.Internalise (trm) import Booster.Util (Flag (..)) @@ -533,6 +533,7 @@ equation ruleLabel lhs rhs priority = } , computedAttributes = ComputedAxiomAttributes False [] , existentials = mempty + , definednessResidual = [] } withAttributes :: RewriteRule t -> (AxiomAttributes -> AxiomAttributes) -> RewriteRule t @@ -540,8 +541,16 @@ r@RewriteRule{lhs, attributes, computedAttributes} `withAttributes` f = r{lhs, computedAttributes, attributes = f attributes} withComputedAttributes :: RewriteRule t -> ComputedAxiomAttributes -> RewriteRule t -r@RewriteRule{lhs} `withComputedAttributes` computedAttributes = - r{lhs, computedAttributes} +r@RewriteRule{lhs, rhs} `withComputedAttributes` computedAttributes = + r + { lhs + , computedAttributes + , -- keep the residual gate consistent with the (manually set) reasons + definednessResidual = + if null computedAttributes.notPreservesDefinednessReasons + then [] + else map Right (collectUndefinedSubterms lhs <> collectUndefinedSubterms rhs) + } mkTheory :: [(TermIndex, [RewriteRule t])] -> Theory (RewriteRule t) mkTheory = Map.map mkPriorityGroups . Map.fromList diff --git a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs index 3c715d20fa..60746f0fca 100644 --- a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs +++ b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs @@ -168,6 +168,7 @@ rule ruleLabel lhs rhs priority = } , computedAttributes = ComputedAxiomAttributes False [] , existentials = mempty + , definednessResidual = [] } ruleWithRequires :: Maybe Text -> Term -> Term -> Priority -> [Predicate] -> RewriteRule "Rewrite" From 1a8da8b93f20475a4f200777e1e053b7f7268a83 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 19 Jun 2026 23:26:18 +0000 Subject: [PATCH 3/6] booster/Definition/Ceil: compute ceil residuals uniformly for all rule kinds, per-kind formula MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- booster/library/Booster/Definition/Ceil.hs | 123 ++++++++++++++++----- 1 file changed, 95 insertions(+), 28 deletions(-) diff --git a/booster/library/Booster/Definition/Ceil.hs b/booster/library/Booster/Definition/Ceil.hs index bf4325a3f7..b4b5f9d180 100644 --- a/booster/library/Booster/Definition/Ceil.hs +++ b/booster/library/Booster/Definition/Ceil.hs @@ -76,12 +76,26 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods ComputeCeilSumm (Set.toList ceils) ] +{- | Which #Ceil formula to use when computing a rule's definedness residual. + Each rule kind picks one; changing the per-kind choice in 'computeCeilsDefinition' + is how we experiment with the definedness check. +-} +data DefinednessFormula + = -- | rewrite rules: @#Ceil(rhs)@ minus @#Ceil(lhs)@ minus @#Ceil(requires)@, plus @#Ceil(requires)@ + Implication + | -- | function equations: @#Ceil(args of lhs) ∧ #Ceil(rhs)@ — the LHS *head* (the function + -- being defined) is excluded, since requiring its definedness would be circular + ConjunctionArgs + | -- | simplification rules: @#Ceil(lhs) ∧ #Ceil(rhs)@ + Conjunction + deriving stock (Eq, Show) + computeCeilsDefinition :: LoggerMIO io => Maybe LLVM.API -> KoreDefinition -> io (KoreDefinition, [ComputeCeilSummary]) -computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do +computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory, functionEquations, simplifications} = do (rewriteTheory', ceilSummaries) <- runWriterT $ let ceilComputation r = do @@ -91,50 +105,103 @@ computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do tell (Seq.singleton summary) pure $ fromMaybe r newRule in mapM (mapM (mapM ceilComputation)) rewriteTheory - pure (def{rewriteTheory = rewriteTheory'}, toList ceilSummaries) + functionEquations' <- + mapM (mapM (mapM (refineRuleResidual mllvm def ConjunctionArgs))) functionEquations + simplifications' <- mapM (mapM (mapM (refineRuleResidual mllvm def Conjunction))) simplifications + pure + ( def + { rewriteTheory = rewriteTheory' + , functionEquations = functionEquations' + , simplifications = simplifications' + } + , toList ceilSummaries + ) + +-- | Attach a rule's definedness residual (function/simplification rules: no logging summary). +refineRuleResidual :: + LoggerMIO io => + Maybe LLVM.API -> + KoreDefinition -> + DefinednessFormula -> + RewriteRule.RewriteRule tag -> + io (RewriteRule.RewriteRule tag) +refineRuleResidual mllvm def formula r = + computeRuleResidual mllvm def formula r >>= \case + Nothing -> pure r + Just newRule -> pure newRule +-- | Rewrite-rule ceil computation that additionally produces a logging summary. computeCeilRule :: LoggerMIO io => Maybe LLVM.API -> KoreDefinition -> RewriteRule.RewriteRule "Rewrite" -> io (Maybe ComputeCeilSummary) -computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes} +computeCeilRule mllvm def r = + computeRuleResidual mllvm def Implication r >>= \case + Nothing -> pure Nothing + Just newRule -> + pure . Just $ + ComputeCeilSummary + { rule = r + , ceils = Set.fromList (RewriteRule.definednessResidual newRule) + , newRule = Just newRule + } + +{- | Compute a rule's definedness residual under the given formula and attach it + (replacing 'definednessResidual'). Returns 'Nothing' for rules already known to + preserve definedness (empty 'notPreservesDefinednessReasons'), which are left + untouched. When the residual discharges to empty, the rule is additionally marked + @preserving@. Polymorphic in the rule tag so it serves all three theories. +-} +computeRuleResidual :: + LoggerMIO io => + Maybe LLVM.API -> + KoreDefinition -> + DefinednessFormula -> + RewriteRule.RewriteRule tag -> + io (Maybe (RewriteRule.RewriteRule tag)) +computeRuleResidual mllvm def formula r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes} | null computedAttributes.notPreservesDefinednessReasons = pure Nothing | otherwise = do ns <- noSolver (res, _) <- runEquationT def mllvm ns mempty mempty $ do - lhsCeils <- Set.fromList <$> computeCeil lhs - requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) requires - let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList - rhsCeils <- simplifyCeils =<< (subtractLHSAndRequiresCeils <$> computeCeil rhs) - - pure $ - Just $ - ComputeCeilSummary - { rule = r - , ceils = requiresCeils <> rhsCeils - , newRule = - Just $ - if null requiresCeils && null rhsCeils - then -- implication residual empty: rule preserves definedness - - r - { RewriteRule.attributes = attributes{preserving = Flag True} - , RewriteRule.computedAttributes = computedAttributes{notPreservesDefinednessReasons = []} - , RewriteRule.definednessResidual = [] - } - else -- attach the leftover implication residual; the rule is applied - -- only where this discharges (currently: never, matching master) - r{RewriteRule.definednessResidual = Set.toList (requiresCeils <> rhsCeils)} - } + ceils <- case formula of + Implication -> do + lhsCeils <- Set.fromList <$> computeCeil lhs + requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) requires + let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList + rhsCeils <- simplifyCeils =<< (subtractLHSAndRequiresCeils <$> computeCeil rhs) + pure (requiresCeils <> rhsCeils) + ConjunctionArgs -> do + argsCeils <- Set.fromList <$> concatMapM computeCeil (functionArgs lhs) + rhsCeils <- Set.fromList <$> computeCeil rhs + simplifyCeils (argsCeils <> rhsCeils) + Conjunction -> do + lhsCeils <- Set.fromList <$> computeCeil lhs + rhsCeils <- Set.fromList <$> computeCeil rhs + simplifyCeils (lhsCeils <> rhsCeils) + pure . Just $ + if null ceils + then -- residual discharges to #Top: the rule preserves definedness + r + { RewriteRule.attributes = attributes{preserving = Flag True} + , RewriteRule.computedAttributes = computedAttributes{notPreservesDefinednessReasons = []} + , RewriteRule.definednessResidual = [] + } + else r{RewriteRule.definednessResidual = Set.toList ceils} case res of Left err -> do liftIO $ print err pure Nothing - Right r' -> pure r' + Right newRule -> pure newRule where + -- arguments of a function-equation LHS, excluding the (function) head symbol + functionArgs = \case + SymbolApplication _ _ args -> args + other -> [other] + simplifyCeils ceils = (.llvmApi) <$> getConfig >>= \case Nothing -> pure ceils From f515219bb9de89863adfb03b17bbcb8fef458bee Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 19 Jun 2026 23:44:18 +0000 Subject: [PATCH 4/6] booster/Pattern/ApplyEquations: dynamic ceil discharge at rule application 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 --- .../library/Booster/Pattern/ApplyEquations.hs | 79 ++++++++++++++++--- 1 file changed, 68 insertions(+), 11 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index d4b232261c..3b488fc21f 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -152,6 +152,11 @@ data EquationConfig = EquationConfig , maxLocalSteps :: Bound "LocalSteps" , logger :: Logger LogMessage , prettyModifiers :: ModifiersRep + , dischargeDefinedness :: Bool + -- ^ when True, a rule blocked by a non-empty static definedness residual gets a + -- dynamic discharge attempt (substitute the match, simplify, re-check) before being + -- rejected. Set False for the discharge's own nested simplification, so the attempt + -- is at most one level deep (no recursive dynamic discharge). } data EquationState = EquationState @@ -367,6 +372,7 @@ runEquationT definition llvmApi smtSolver sCache known (EquationT m) = do , maxLocalSteps = globalEquationOptions.maxLocalSteps , logger , prettyModifiers + , dischargeDefinedness = True } -- NB the returned cache assumes the known predicates pure (res, endState.cache) @@ -923,6 +929,45 @@ applyEquations theory handler term = do ) err +{- | Dynamic ceil discharge. Given the match substitution and a rule's leftover + definedness residual, substitute and simplify each obligation and report whether they + are now all trivially satisfied: a @#Ceil(t)@ obligation (@Right t@) when the simplified + term has no remaining partial sub-terms (the same "trivially defined" check used at load), + a predicate obligation (@Left p@) when it simplifies to @true@. + + The nested simplification runs with 'dischargeDefinedness' disabled, so a rule blocked + during the discharge is simply not applied rather than triggering a further (recursive) + discharge — the attempt is at most one level deep. +-} +dischargeDefinednessResidual :: + LoggerMIO io => + Substitution -> + [Either Predicate Term] -> + EquationT io Bool +dischargeDefinednessResidual subst residual = do + cfg <- getConfig + st <- getState + and <$> mapM (dischargeObligation cfg st) residual + where + -- run the residual's simplification in an *isolated* equation state (fresh iteration + -- state, copied cache/known predicates) so it cannot corrupt the outer evaluation, and + -- with dynamic discharge disabled so it does not recurse (at most one level deep) + dischargeObligation cfg st obligation = + eqState . lift $ do + let substituted = substituteInTerm subst (either coerce id obligation) + (result, _) <- + runEquationT cfg.definition cfg.llvmApi cfg.smtSolver st.cache st.predicates $ + withoutDynamicDischarge (evaluateTerm' BottomUp substituted) + pure $ case (obligation, result) of + -- #Ceil(t): satisfied once the simplified term has no partial sub-terms + (Right{}, Right simplified) -> null (collectUndefinedSubterms simplified) + -- predicate obligation: satisfied once it simplifies to true + (Left{}, Right simplified) -> simplified == TrueBool + (_, Left _) -> False + + withoutDynamicDischarge (EquationT m) = + EquationT $ withReaderT (\cfg -> cfg{dischargeDefinedness = False}) m + applyEquation :: forall io tag. LoggerMIO io => @@ -941,18 +986,22 @@ applyEquation term rule = logMessage ("Equation with existentials" :: Text) lift . throw . InternalError $ "Equation with existentials: " <> Text.pack (show rule) - -- immediately cancel if the rule has a non-empty definedness residual - -- (i.e. its definedness obligation does not reduce to #Top) + let rejectNotPreservingDefinedness = + throwE + ( \ctxt -> + ctxt $ + logMessage $ + renderOneLineText $ + "Uncertain about definedness of rule due to:" + <+> hsep (intersperse "," $ map pretty rule.computedAttributes.notPreservesDefinednessReasons) + , RuleNotPreservingDefinedness + ) + -- A non-empty static definedness residual blocks the rule. When dynamic + -- discharge is enabled we defer the decision to after matching (where the + -- match substitution is available); otherwise we reject up front. unless (null rule.definednessResidual) $ do - throwE - ( \ctxt -> - ctxt $ - logMessage $ - renderOneLineText $ - "Uncertain about definedness of rule due to:" - <+> hsep (intersperse "," $ map pretty rule.computedAttributes.notPreservesDefinednessReasons) - , RuleNotPreservingDefinedness - ) + discharge <- (.dischargeDefinedness) <$> lift getConfig + unless discharge rejectNotPreservingDefinedness -- immediately cancel if rule has concrete() flag and term has variables when (allMustBeConcrete rule.attributes.concreteness && not (Set.null (freeVariables term))) $ do throwE @@ -1007,6 +1056,14 @@ applyEquation term rule = Map.toList subst ) + -- dynamic ceil discharge: substitute the match into the (non-empty) + -- static residual and try to simplify it to trivially-satisfied before + -- committing to the rule. One level deep: the nested simplification runs + -- with discharge disabled, so it does not itself attempt discharge. + unless (null rule.definednessResidual) $ do + discharged <- lift $ dischargeDefinednessResidual subst rule.definednessResidual + unless discharged rejectNotPreservingDefinedness + -- check required constraints from lhs. -- Reaction on false/indeterminate varies depending on the equation's type (function/simplification), -- see @handleSimplificationEquation@ and @handleFunctionEquation@ From 2565e5e0fa714413bf2a7f037298b526e1918f3d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 19 Jun 2026 23:51:28 +0000 Subject: [PATCH 5/6] booster/unit-tests/ApplyEquations: tests for dynamic ceil discharge 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 --- .../Test/Booster/Pattern/ApplyEquations.hs | 61 +++++++++++++++++++ 1 file changed, 61 insertions(+) diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index cadf2db2aa..202c4f4640 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -15,6 +15,7 @@ module Test.Booster.Pattern.ApplyEquations ( test_localFixpoint, test_errors, test_soundnessGap, + test_dynamicCeilDischarge, ) where import Control.Exception (finally) @@ -358,6 +359,28 @@ test_soundnessGap = @?>>= Right result ] +test_dynamicCeilDischarge :: TestTree +test_dynamicCeilDischarge = + testGroup + "Dynamic discharge of definedness residuals at rule application" + [ testCase "applies once the match makes the residual defined" $ do + -- con3(f2(X), Y) => Y carries residual #Ceil(f2(X)); here the match binds + -- X to con2(A), and f2(con2(A)) simplifies to con2(A) (defined), so the + -- residual discharges and the rule fires (top-down, before the argument is + -- simplified away). + evalD TopDown [trm| con3{}(f2{}(con2{}(A:SomeSort{})), B:SomeSort{}) |] + @?>>= Right [trm| B:SomeSort{} |] + , testCase "stays blocked when the match keeps the residual undefined" $ do + -- f2(con1(A)) has no rule, so #Ceil(f2(con1(A))) cannot be discharged and the + -- rule does not fire. + let subj = [trm| con3{}(f2{}(con1{}(A:SomeSort{})), B:SomeSort{}) |] + evalD TopDown subj @?>>= Right subj + ] + where + evalD direction t = do + ns <- noSolver + runNoLoggingT $ fst <$> evaluateTerm direction dischargeDef Nothing ns mempty mempty t + ---------------------------------------- index :: (ByteString -> CellIndex) -> SymbolName -> TermIndex @@ -478,6 +501,44 @@ soundnessGapSimplDef = mkTheory [(index IdxFun "f1", soundnessGapRules)] } +{- | Definition for 'test_dynamicCeilDischarge'. @f2@ is partial with one total-result +rule @f2(con2(X)) => con2(X)@ (so @f2(con2(_))@ reduces to a defined term, @f2(con1(_))@ +is stuck), plus a simplification @con3(f2(X), Y) => Y@ that carries the static residual +@#Ceil(f2(X))@. Whether the simplification fires turns on discharging that residual +against the match. +-} +dischargeDef :: KoreDefinition +dischargeDef = + testDefinition + { functionEquations = + mkTheory + [ + ( index IdxFun "f2" + , + [ equation + Nothing + [trm| f2{}(con2{}(X:SomeSort{})) |] + [trm| con2{}(X:SomeSort{}) |] + 50 + ] + ) + ] + , simplifications = + mkTheory + [ + ( index IdxCons "con3" + , + [ equation + Nothing + [trm| con3{}(f2{}(X:SomeSort{}), Y:SomeSort{}) |] + [trm| Y:SomeSort{} |] + 50 + `withComputedAttributes` ComputedAxiomAttributes False [UndefinedSymbol "f2"] + ] + ) + ] + } + f1Equations, f2Equations :: [RewriteRule t] f1Equations = [ equation -- f1(con1(X)) == con2(f1(X)) From a4fa98cd0eb6086ea84c3aef4a9f740f498a3bce Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 19 Jun 2026 23:52:23 +0000 Subject: [PATCH 6/6] =?UTF-8?q?docs/2026-06-19-definedness-checking-design?= =?UTF-8?q?:=20record=20implementation=20status=20and=20decisions=20(?= =?UTF-8?q?=C2=A79)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../2026-06-19-definedness-checking-design.md | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/docs/2026-06-19-definedness-checking-design.md b/docs/2026-06-19-definedness-checking-design.md index bb892b76f2..35baa6c9b7 100644 --- a/docs/2026-06-19-definedness-checking-design.md +++ b/docs/2026-06-19-definedness-checking-design.md @@ -231,3 +231,35 @@ The only genuine residual to discharge at runtime is RHS-introduced partiality ( - Roșu, *Matching Logic* (LMCS 2017) and *Matching Logic Explained* (JLAMP 2021) — `⌈_⌉` semantics, the `∀x. ⌈x⌉` definedness axiom, total vs partial symbol axioms, the `⌈x/y⌉ = (y ≠ 0)` example; OOPSLA'16 *Semantics-Based Program Verifiers* — set-valued application and `∅`-strictness. - One-Path (LICS'13) / All-Path (RTA'14) reachability logic — total state model; symbolic states as denotation sets; vacuity of ⊥ instances. - This repo: `booster/library/Booster/Definition/Ceil.hs` (PR #402, the static Model-A residual via `ceil(RHS) ∖ ceil(LHS) ∖ ceil(requires)`, with the explicit "assume the configuration is defined … should eventually check"); `Internalise.hs:892` (the conservative LHS∪RHS load scan to be replaced); `ApplyEquations.hs:716` (`master`'s binary definedness gate, to be replaced); PRs #426/#440/#441 (the empirical-caution episode); `docs/2020-06-17-Checking-Implication.md` (the in-repo note that checking `⌈t(X)⌉ ∧ P(X)` "could … infer that the configuration is defined, allowing … subsequent rewriting without generating extra definedness conditions" — assume-defined, in our own docs). + +## 9. Implementation status on this branch (`ceil-simplifier`) + +What has actually been built so far, and the decisions taken (some made autonomously — flag for review). + +### 9.1 What is implemented + +1. **Residuals attached to rules.** `RewriteRule` gained `definednessResidual :: [Either Predicate Term]` (`Left p` = residual predicate, `Right t` = unresolved `#Ceil(t)`); a rule preserves definedness iff it is empty. `Pattern.Util.collectUndefinedSubterms` mirrors `filterTermSymbols`. Commit: *"gate rule application on a definedness residual"* — a behaviour-preserving switch of the gate from the `notPreservesDefinednessReasons` boolean to the residual. +2. **Uniform static computation.** `Definition/Ceil.computeCeilsDefinition` now walks **all three theories** via a polymorphic `computeRuleResidual` parameterised by a `DefinednessFormula`: rewrite → `Implication` (`#Ceil(rhs) ∖ #Ceil(lhs) ∖ #Ceil(requires)`, unchanged from master), function → `ConjunctionArgs` (`#Ceil(args(lhs)) ∧ #Ceil(rhs)`, head excluded), simplification → `Conjunction` (`#Ceil(lhs) ∧ #Ceil(rhs)`). Commit: *"compute ceil residuals uniformly for all rule kinds, per-kind formula"*. Switching a kind's formula is now a one-line change. +3. **Dynamic discharge.** `ApplyEquations.applyEquation` defers the residual check to after matching and calls `dischargeDefinednessResidual`: substitute the match `σ`, simplify each obligation in an **isolated `runEquationT`** (copied cache/known predicates, fresh iteration state) with discharge disabled, and accept when a `#Ceil(t)` obligation simplifies to a term with no partial sub-terms (the load-time "trivially defined" check) or a predicate simplifies to `true`. Commit: *"dynamic ceil discharge at rule application"* (+ unit tests). + +### 9.2 Decisions taken (review these) + +- **Dynamic discharge is always on**, not behind a flag. `EquationConfig.dischargeDefinedness` defaults `True` (set in `runEquationT`) and is flipped `False` only for the discharge's own nested simplification, giving a **one-level-deep** guard (no recursive discharge). The earlier per-site `--evaluate-ceils-*` flags were *not* reintroduced; if per-site control is wanted, the flag now exists and just needs threading from `GlobalState`/CLI. +- **Isolation via a fresh `runEquationT`** (not `local`/`withReaderT` over the live state). An in-place nested simplify corrupted the outer traversal's iteration state (`changed`, cache) — caught by the `f2` unit tests, which returned the whole term unevaluated. The isolated run (copying `cache`/`predicates`) fixes it and mirrors the rebased-out prototype. +- **Discharge check = the load-time "trivially defined" test**, per the request: `collectUndefinedSubterms == []` for `#Ceil(t)`, `== TrueBool` for predicates. No SMT / path-condition entailment for residual *predicates* yet — only structural/concrete discharge. (Symbolic conditions like `Y =/= 0` provable only from the path condition still do **not** discharge. That is the obvious next increment if wanted.) +- **`internalise` keeps a cheap raw-scan residual as a fallback**; `computeCeilsDefinition` (run at server load) overwrites it with the real `computeCeil` residual. So a definition loaded *without* the ceil pass is more conservative than one loaded with it, and **the unit tests exercise the fallback** (they do not run `computeCeilsDefinition`), while the per-kind `computeCeil` formulas run at the server. +- **`notPreservesDefinednessReasons` is retained** (not removed) for the abort message and to select which rules `computeCeilRule` refines. Retiring it is a clean follow-up once the residual is the sole source of truth. + +### 9.3 Behaviour change vs master, and validation gaps + +- Rewrite rules: unchanged (same implication residual as master). +- Function/simplification rules: now more permissive — residuals that discharge **at load** (concrete arithmetic, concrete collection distinctness, explicit `#Ceil` rules) and, with dynamic discharge, residuals that discharge **once the match is known** now let the rule apply. Symbolic partial subterms still reject, so the KEVM LHS-partial declines are **not** expected to move (matching the analysis in §8.3); the genuinely-partial-arithmetic family needs the SMT/path-condition step that is not yet built. +- **Validation:** 982 booster unit tests pass (incl. a positive + negative dynamic-discharge test). The new per-kind `computeCeil` formulas and the always-on dynamic discharge are **not yet exercised against the booster/KEVM integration suite** (needs the K toolchain) — that is the outstanding validation before trusting the behaviour change or flipping anything KEVM-facing. + +### 9.4 Commit sequence (on the `#4156` base `163997f9b`) + +1. `docs/…definedness-checking-design` — this document. +2. `…: gate rule application on a definedness residual` — residual field + gate switch (behaviour-preserving). +3. `Definition/Ceil: compute ceil residuals uniformly for all rule kinds, per-kind formula`. +4. `Pattern/ApplyEquations: dynamic ceil discharge at rule application`. +5. `unit-tests/ApplyEquations: tests for dynamic ceil discharge`.