Discharge implies-check consequent obligations under the antecedent via SMT#4150
Closed
ehildenb wants to merge 4 commits into
Closed
Discharge implies-check consequent obligations under the antecedent via SMT#4150ehildenb wants to merge 4 commits into
ehildenb wants to merge 4 commits into
Conversation
…ate field on ImpliesResult
Plumbing-only change: introduces the new optional 'indeterminate ::
Maybe Bool' field on 'ImpliesResult' and sets it to 'Nothing' at every
existing construction site.
* 'kore-rpc-types': field added with doc comment; 'OmitNothingFields'
keeps the JSON output unchanged when absent.
* 'Booster.Pattern.Implies': 'doesNotImply'' and 'implies'' record
constructions extended with 'indeterminate = Nothing'.
* 'Kore.JsonRpc': positional 'ImpliesResult' constructions extended
with trailing 'Nothing' (kore checks are always decisive).
No call site sets the field to a non-'Nothing' value yet; that wiring
lands in subsequent commits.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…, scripts/booster-integration-tests: add failing RPC tests for implies SMT discharge Pins booster's current `implies` behaviour on four cases where the antecedent and consequent share an identical term skeleton (so the matcher returns `MatchSuccess`) but differ in their attached path-condition predicates. The leftover obligations are direct consequences of the antecedent under linear-integer reasoning, so an SMT-aware discharge step under the antecedent would close them as `valid : true` (or `valid : false` for the doesNotImply case). Cases: - 001-bound-weakening: X<100 ⇒ X<1000 - 002-does-not-imply: X<100 ⇒ X<10 (counterexample exists) - 003-vacuous-antecedent: X<10 ∧ X>20 ⇒ anything - 004-address-bound: 0<=X<pow160 ⇒ X<pow256 (KEVM-faithful) `response-N.booster-dev` documents today's `Aborted: unknown constraints` on cases 001/002/004 (the FIXME on `Implies.hs:161`'s `MatchSuccess` branch — antecedent constraints are not assumed when discharging the leftover consequent predicates). Case 003 already passes on booster-dev via earlier bottom-detection. `response-N.json` shows the `kore-rpc-booster` ground truth that the fix should match. The `.kore` definition is built on demand from `implies-smt.k` via the shipped `.kompile` script (mirrors the `escalate-partial-match` pattern). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…implies2}: discharge consequent obligations under antecedent via SMT
Resolves the FIXME in 'checkImpliesMatchTerms''s 'MatchSuccess' branch.
Previously the leftover consequent predicates were passed to
'evaluateConstraints' with no known context — i.e. SMT was asked
whether each obligation is valid 'under the assumption of itself',
which trivially holds for self-discharging predicates but cannot
close anything that depends on the antecedent's path condition (the
57 'kore-implies' handoffs observed in KEVM recover-mode).
The new flow mirrors the rewrite path's two-stage discharge
('Booster.Pattern.Rewrite.checkRequires'):
1. Simplify each leftover obligation under the antecedent context
('patL.constraints' + 'asEquations patL.substitution') via
'simplifyConstraint' — this unfolds K-level vocabulary
('#rangeAddress', boolean structure, ...) so SMT sees only
SMT-tractable predicates.
2. SMT-close any non-'TrueBool' residue with
'SMT.checkPredicates solver antecedentPreds patL.substitution
residue':
- 'IsValid' → 'implies'
- 'IsInvalid' → 'doesNotImply'
- 'IsUnknown InconsistentGroundTruth' → 'implies' (vacuous antecedent)
- 'IsUnknown _' → 'doesNotImplyIndeterminate'
The previous hard 'Aborted "unknown constraints"' path is gone:
unresolvable obligations now return the 'Unsure' verdict
('valid: false, indeterminate: Just True'), so a recover-mode client
escalates to kore rather than seeing an RPC error.
Test response updates (booster-dev expected outputs, flipped from
the prior 'Aborted' verdict):
- test-implies-smt/response-{001-bound-weakening,004-address-bound}.booster-dev:
'Aborted' → 'valid: true' (SMT closes under antecedent).
- test-implies-smt/response-002-does-not-imply.booster-dev:
'Aborted' → 'valid: false, indeterminate: true' (SMT
'ImplicationIndeterminate' — both polarities sat).
- test-implies2/response-{consequent-constraint,refutation-1,
refutation-3,refutation-4}.booster-dev:
'Aborted' → 'valid: false, indeterminate: true' (same
mechanism on the existing implies2 cases that triggered the
bug pre-fix).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
ehildenb
force-pushed
the
implies-smt-discharge
branch
from
c894061 to
4662846
Compare
…a single mkResult builder
The four result builders ('implies'', 'doesNotImply'',
'doesNotImplyIndeterminate', and the implied 'implies'/'doesNotImply'
wrappers) each spelled out the same 'pure . Right . Implies . ImpliesResult'
record, differing only in 'valid', 'condition', and 'indeterminate'. Collapse
the shared skeleton into one 'mkResult' helper so the record lives in a single
place — a future field addition (as 'haskellLogEntries' was upstream) becomes a
one-line change rather than four. No behavioural change.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Member
Author
|
Going to close this for now, will re-open when it has a measureable effect on KEVM (other issues are in the way). |
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
1 participant
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.
When booster's
impliescheck matches the consequent against the antecedent and finds leftover consequent obligations, it previously passed them toevaluateConstraintswith no path-condition context — effectively asking SMT whether each obligation holds "under the assumption of itself". Anything depending on the antecedent's constraints couldn't be closed, and unresolved obligations aborted the RPC withAborted "unknown constraints"(the source of 57kore-implieshandoffs observed in KEVM recover-mode). This change discharges those obligations under the antecedent, mirroring the rewrite path's two-stage approach (Booster.Pattern.Rewrite.checkRequires): each obligation is first simplified with the antecedent inknownPredicates(so K-level vocabulary like#rangeAddressunfolds), then any non-TrueBoolresidue is SMT-closed against the antecedent's predicates and substitution. Unresolvable obligations now return an indeterminatevalid: falseverdict instead of an RPC error, so a recover-mode client escalates to kore rather than failing.Changes:
Booster.Pattern.Implies: replace theMatchSuccessFIXME path with simplify-under-antecedent +SMT.checkPredicates; mapIsValid→implies,IsInvalid→does-not-imply,IsUnknown InconsistentGroundTruth→implies (vacuous antecedent),IsUnknown _→indeterminate.kore-rpc-types: add an optionalindeterminate :: Maybe Boolfield toImpliesResult(omitted when absent) so clients can distinguish a decisivevalid: falsefrom an indeterminate one.kore/JsonRpc: set the new field toNothingon kore-side results (always decisive).test-implies-smtRPC integration tests (bound-weakening, does-not-imply, vacuous-antecedent, address-bound) and updatetest-implies2goldens for the cases that previously aborted.mkResulthelps build implication results in a standard way, and we pre-compute several terms that are used on several branches of the implication check.Validation:
-Wall -Werror(stack, GHC 9.6.5); fourmolu-clean.Implieschecks directly in booster that were not cleared before and relied on Kore (collecting data on that now).