…, 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>

…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>

…rview table of the four tests

Documents the antecedent/consequent of each test, the expected booster and
kore status, and which arm of the SMT-discharge logic it exercises — including
why 002 diverges (booster indeterminate vs kore invalid).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…erdict

Booster's implies endpoint can now return status=indeterminate (match
indeterminate / SMT-unknown obligation) as a successful response rather than a
hard abort. The proxy previously only fell back to kore on a booster *error*
(Left), so an indeterminate verdict was handed straight back to the caller and
never escalated — a regression versus the old Aborted path, which the proxy did
fall back on.

Add an explicit arm: on a Right implies result with status=indeterminate,
escalate to kore so the check still gets a decisive answer, emitting the usual
kore-implies-fallback event. Skipped under booster-only, where the indeterminate
result is returned as-is for the client to act on. The shared kore-fallback
block (now used by both the indeterminate and the booster-abort paths) is
factored into a local koreImpliesFallback helper.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…r indeterminate implies (005)

Pins the proxy's escalate-on-indeterminate behaviour. Same query as 002
(X <Int 100 implies X <Int 10), but with assume-defined: true so the proxy runs
booster first. The booster-dev server returns status=indeterminate; the full
proxy escalates that verdict to kore and returns status=invalid. The two goldens
are derived from 002 (kore's implies handler ignores assume-defined, so it
returns the identical decisive answer). README table updated.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>