Skip to content

Commit 163997f

Browse files
ehildenbclaude
ehildenb
and
claude
authored
Booster implies: discharge leftover consequent obligations under the antecedent via SMT (#4156)
The booster `implies` endpoint previously gave up — returning not-implied and forcing a kore fallback — whenever a matched implication left consequent-side obligations that were not already present in the antecedent. This is a significant source of kore fallbacks on the implies endpoint. This change lets booster discharge those leftover obligations itself: after a successful match, each remaining consequent obligation is simplified with the antecedent in scope, and any residue is SMT-closed against the antecedent (the same path the rewrite engine uses to discharge rule requires-clauses). Implications that previously fell back can now be answered directly. The change also introduces a third verdict on the wire. A booster `valid: false` response was previously ambiguous: it could mean "decisively not implied" or "could not determine," and the two were byte-identical (`valid: false`, `condition: null`). A new optional `indeterminate` field disambiguates them so a recover-mode client knows when to escalate to kore rather than trust `valid: false`. **Changes:** - Discharge leftover consequent obligations under the antecedent: simplify each with the antecedent predicates in `knownPredicates`, then SMT-close the non-trivial residue against the antecedent constraints/substitution. Implied → `valid: true`; refuted → decisively not implied; unknown → indeterminate. - Add an optional `indeterminate :: Maybe Bool` field to `ImpliesResult`. Emitted as `true` only on non-decisive `valid: false` results (SMT returns unknown, or the equation engine errors); omitted via `OmitNothingFields` on every decisive result and on all kore-side results. It encodes a real third state not inferrable from `valid`/`condition`. - Consolidate every `ImpliesResult` construction into a single `mkResult` builder. - Add `test-implies-smt` RPC integration tests (bound-weakening, disjoint, vacuous-antecedent, address-bound) and update the `test-implies2` goldens to carry the new field where applicable. **Validation:** - Booster unit tests pass. - New `test-implies-smt` RPC tests and updated `test-implies2` goldens ship with the PR and exercise the implied / decisively-not-implied / indeterminate paths (run in the integration suite, not the unit suite). **Downstream note:** the new `indeterminate` field is additive and optional, but it does appear as `"indeterminate": true` on the affected responses — clients with a strict/closed-schema decoder must tolerate it. --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
1 parent 6f17f7e commit 163997f

62 files changed

Lines changed: 3418 additions & 141 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎booster/library/Booster/Pattern/Implies.hs‎

Lines changed: 100 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -137,32 +137,68 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
137137
(Left err, _) ->
138138
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err)
139139
MatchSuccess subst -> do
140-
let filteredConsequentPreds =
141-
(patR.constraints <> (Set.fromList $ asEquations patR.substitution))
142-
`Set.difference` (patL.constraints <> (Set.fromList $ asEquations patL.substitution))
143-
140+
let sort = sortOfPattern patL
141+
lhs = externaliseExistTerm existsL patL.term
142+
rhs = externaliseExistTerm existsR patR.term
143+
antecedentPreds =
144+
patL.constraints <> Set.fromList (asEquations patL.substitution)
145+
filteredConsequentPreds =
146+
(patR.constraints <> Set.fromList (asEquations patR.substitution))
147+
`Set.difference` antecedentPreds
144148
if null filteredConsequentPreds
145-
then
146-
implies
147-
(sortOfPattern patL)
148-
(externaliseExistTerm existsL patL.term)
149-
(externaliseExistTerm existsR patR.term)
150-
subst
151-
else -- FIXME This is incomplete because patL.constraints are not assumed in the check.
152-
153-
ApplyEquations.evaluateConstraints def mLlvmLibrary solver filteredConsequentPreds >>= \case
154-
Right newPreds ->
155-
if all (== Predicate TrueBool) newPreds
156-
then
157-
implies
158-
(sortOfPattern patL)
159-
(externaliseExistTerm existsL patL.term)
160-
(externaliseExistTerm existsR patR.term)
161-
subst
162-
else -- here we conservatively abort (incomplete)
163-
pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constraints"
164-
Left other ->
165-
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
149+
then implies sort lhs rhs subst
150+
else do
151+
-- Discharge the leftover consequent obligations under
152+
-- the antecedent. Two stages:
153+
-- 1. Simplify each obligation with the antecedent in
154+
-- 'knownPredicates' so function-symbol unfolds
155+
-- (e.g. '#rangeAddress') and boolean structure
156+
-- collapse can fire.
157+
-- 2. SMT-close any non-'TrueBool' residue against
158+
-- 'antecedentPreds' / 'patL.substitution' — the
159+
-- same pattern the rewrite path uses to discharge
160+
-- rule requires-clauses
161+
-- ('Booster.Pattern.Rewrite.checkRequires').
162+
simplified <-
163+
mapM
164+
( fmap fst
165+
. ApplyEquations.simplifyConstraint
166+
def
167+
mLlvmLibrary
168+
solver
169+
mempty
170+
antecedentPreds
171+
)
172+
(Set.toList filteredConsequentPreds)
173+
let impliesResult = implies sort lhs rhs subst
174+
unsure = doesNotImplyIndeterminate sort lhs rhs
175+
disjoint = doesNotImply sort lhs rhs
176+
case sequence simplified of
177+
Left _ ->
178+
-- Equation engine error: route to Unsure
179+
-- rather than the old hard 'Aborted', so the
180+
-- client can escalate via kore fallback.
181+
unsure
182+
Right reduced
183+
| all (== Predicate TrueBool) reduced ->
184+
impliesResult
185+
| otherwise -> do
186+
let residue =
187+
Set.fromList $
188+
filter (/= Predicate TrueBool) reduced
189+
SMT.checkPredicates
190+
solver
191+
antecedentPreds
192+
patL.substitution
193+
residue
194+
>>= \case
195+
SMT.IsValid -> impliesResult
196+
SMT.IsInvalid -> disjoint
197+
-- Vacuous antecedent: any consequent
198+
-- is implied.
199+
SMT.IsUnknown SMT.InconsistentGroundTruth ->
200+
impliesResult
201+
SMT.IsUnknown _ -> unsure
166202

167203
case (internalised antecedent.term, internalised consequent.term) of
168204
(Left patternError, _) -> do
@@ -204,42 +240,46 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
204240
antecedent.term
205241
consequent.term
206242
where
207-
doesNotImply' s condition l r =
208-
pure $
209-
Right $
210-
RpcTypes.Implies
211-
RpcTypes.ImpliesResult
212-
{ implication = addHeader $ Kore.Syntax.KJImplies s l r
213-
, valid = False
214-
, condition
215-
, logs = Nothing
216-
, haskellLogEntries = Nothing
217-
}
243+
-- Single construction point for every implies / does-not-imply result.
244+
-- The call sites differ only in 'status' and 'condition'; centralising
245+
-- the record keeps a future field addition a one-line change.
246+
mkResult s l r status condition =
247+
pure . Right . RpcTypes.Implies $
248+
RpcTypes.ImpliesResult
249+
{ implication = addHeader $ Kore.Syntax.KJImplies s l r
250+
, status
251+
, condition
252+
, logs = Nothing
253+
, haskellLogEntries = Nothing
254+
}
255+
256+
doesNotImply' s condition l r = mkResult s l r RpcTypes.Invalid condition
218257

219258
doesNotImply s' = let s = externaliseSort s' in doesNotImply' s Nothing
259+
260+
-- Variant of 'doesNotImply' that flags the result as indeterminate.
261+
-- Use at non-decisive not-implied outcomes — the 'MatchIndeterminate'
262+
-- retry-ladder no-progress fall-through and the 'MatchSuccess'
263+
-- SMT-discharge 'IsUnknown _' branch — so a recover-mode client
264+
-- escalates to kore rather than trusting @status: invalid@.
265+
doesNotImplyIndeterminate s' l r =
266+
let s = externaliseSort s' in mkResult s l r RpcTypes.Indeterminate Nothing
267+
220268
implies' predicate s l r subst =
221-
pure $
222-
Right $
223-
RpcTypes.Implies
224-
RpcTypes.ImpliesResult
225-
{ implication = addHeader $ Kore.Syntax.KJImplies s l r
226-
, valid = True
227-
, condition =
228-
Just
229-
RpcTypes.Condition
230-
{ predicate = addHeader predicate
231-
, substitution =
232-
addHeader
233-
$ ( \case
234-
[] -> Kore.Syntax.KJTop s
235-
[x] -> x
236-
xs -> Kore.Syntax.KJAnd s xs
237-
)
238-
. map (uncurry $ externaliseSubstitution s)
239-
. Map.toList
240-
$ subst
241-
}
242-
, logs = Nothing
243-
, haskellLogEntries = Nothing
244-
}
269+
mkResult s l r RpcTypes.Valid (Just condition)
270+
where
271+
condition =
272+
RpcTypes.Condition
273+
{ predicate = addHeader predicate
274+
, substitution =
275+
addHeader
276+
$ ( \case
277+
[] -> Kore.Syntax.KJTop s
278+
[x] -> x
279+
xs -> Kore.Syntax.KJAnd s xs
280+
)
281+
. map (uncurry $ externaliseSubstitution s)
282+
. Map.toList
283+
$ subst
284+
}
245285
implies s' = let s = externaliseSort s' in implies' (Kore.Syntax.KJTop s) s

‎booster/test/rpc-integration/resources/implies-smt.k‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// Minimal definition for exercising booster's `implies` check against
2+
// integer / boolean obligations that need SMT discharge.
3+
//
4+
// The test claims send raw KORE `implies` requests whose antecedent and
5+
// consequent share identical configurations (so the matcher returns
6+
// MatchSuccess) but differ in their attached path-condition predicates.
7+
// The interesting cases are the ones where the leftover consequent
8+
// predicate is *implied* by the antecedent under linear-integer reasoning
9+
// (e.g. `X <Int 1000` from `X <Int 100`), so an SMT-aware discharge
10+
// step would close them as `valid : true`.
11+
//
12+
// The configuration is a single `<k>` cell containing an `Int` — enough
13+
// to give us a kompiled definition with `_<Int_`, `andBool`, `true`, and
14+
// the standard cell wrappers without any extra ceremony.
15+
16+
module IMPLIES-SMT
17+
imports INT
18+
imports BOOL
19+
20+
configuration <k> $PGM:Int </k>
21+
22+
endmodule

‎booster/test/rpc-integration/resources/implies-smt.kompile‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
#!/usr/bin/env bash
2+
set -euo pipefail
3+
name=$(basename "$0" .kompile)
4+
kompile --backend haskell "$name.k" --syntax-module IMPLIES-SMT
5+
cp "$name-kompiled/definition.kore" "./$name.kore"
6+
rm -r "$name-kompiled"

‎booster/test/rpc-integration/test-3934-smt/response-003.booster-dev‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
"jsonrpc": "2.0",
33
"id": 3,
44
"result": {
5-
"valid": false,
5+
"status": "invalid",
66
"implication": {
77
"format": "KORE",
88
"version": 1,

‎booster/test/rpc-integration/test-3934-smt/response-003.json‎

Lines changed: 1 addition & 1 deletion
Large diffs are not rendered by default.

‎booster/test/rpc-integration/test-3934-smt/response-005.booster-dev‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
"jsonrpc": "2.0",
33
"id": 5,
44
"result": {
5-
"valid": false,
5+
"status": "invalid",
66
"implication": {
77
"format": "KORE",
88
"version": 1,

‎booster/test/rpc-integration/test-3934-smt/response-005.json‎

Lines changed: 1 addition & 1 deletion
Large diffs are not rendered by default.

‎booster/test/rpc-integration/test-3934-smt/response-007.booster-dev‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
"jsonrpc": "2.0",
33
"id": 7,
44
"result": {
5-
"valid": false,
5+
"status": "invalid",
66
"implication": {
77
"format": "KORE",
88
"version": 1,

‎booster/test/rpc-integration/test-3934-smt/response-007.json‎

Lines changed: 1 addition & 1 deletion
Large diffs are not rendered by default.

‎booster/test/rpc-integration/test-foundry-bug-report/response-006.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
"jsonrpc": "2.0",
33
"id": 6,
44
"result": {
5-
"valid": false,
5+
"status": "invalid",
66
"implication": {
77
"format": "KORE",
88
"version": 1,

0 commit comments

Comments
 (0)