feat: parametric ResultClassifier for pyAnalyzeLaurel success/failure#666
Merged
feat: parametric ResultClassifier for pyAnalyzeLaurel success/failure#666
Conversation
Add a `ResultClassifier` structure to `StrataMain` holding pluggable `isSuccess` and `isFailure` predicates (defaulting to the existing `VCResult` methods). Pass it through `printPyAnalyzeSummary` and the per-VC display loop so that both the summary counts/exit-code and the "Assertion failed" location prefix are driven by the same definition. `nInconclusive` is now computed as the remainder after subtracting success, failure, unreachable, and implementation-error counts, so narrowing `isFailure` automatically widens inconclusive without further changes. In bug-finding mode (`bugFinding` / `bugFindingAssumingCompleteSpec`) the classifier narrows `isFailure` to `alwaysFalseAndReachable` only — the outcome where the validity check confirms the property is always false on a reachable path. Also add `VCOutcome.hasSMTError` and `VCResult.hasSMTError` to `Verifier.lean` alongside the other nine-case predicates, and use them to simplify the `nImplError` filter in `printPyAnalyzeSummary`. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
MikaelMayer
reviewed
Mar 26, 2026
Contributor
There was a problem hiding this comment.
Clean PR — the ResultClassifier abstraction is well-scoped and the remainder-based nInconclusive is a nice simplification. The hasSMTError extraction into Verifier.lean is a good cleanup. One observations below which is worth discussing before merge.
Replace independent counting + Nat-subtraction remainder with successive list partitioning (implError → success → failure → inconclusive), which guarantees disjointness by construction and eliminates the Nat underflow risk. Unreachable is now an informational overlay rather than a separate partition, so it flows through the classifier — correctly handling future cover obligations where unreachable is a failure, not a success. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
MikaelMayer
approved these changes
Mar 26, 2026
joscoh
approved these changes
Mar 26, 2026
olivier-aws
pushed a commit
that referenced
this pull request
Mar 30, 2026
…#666) ## Summary - Add `ResultClassifier` structure with pluggable `isSuccess`/`isFailure` predicates (defaults preserve existing behavior) so callers can control what counts as a failure without touching `printPyAnalyzeSummary`. - In bug-finding mode, narrow `isFailure` to `alwaysFalseAndReachable` only — the outcome where validity confirms the property is always false on a reachable path. Other failure modes become inconclusive. - Apply the classifier consistently: both the per-VC `"Assertion failed"` prefix and the summary counts/exit-code now use the same `classifier.isFailure`. - `nInconclusive` is now the remainder (total minus success, failure, unreachable, impl-error), so narrowing `isFailure` automatically widens inconclusive. - Add `VCOutcome.hasSMTError` / `VCResult.hasSMTError` to `Verifier.lean` alongside the other nine-case predicates, and use them to simplify `nImplError` in `printPyAnalyzeSummary`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
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
3 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.
Summary
ResultClassifierstructure with pluggableisSuccess/isFailurepredicates (defaults preserve existing behavior) so callers can control what counts as a failure without touchingprintPyAnalyzeSummary.isFailuretoalwaysFalseAndReachableonly — the outcome where validity confirms the property is always false on a reachable path. Other failure modes become inconclusive."Assertion failed"prefix and the summary counts/exit-code now use the sameclassifier.isFailure.nInconclusiveis now the remainder (total minus success, failure, unreachable, impl-error), so narrowingisFailureautomatically widens inconclusive.VCOutcome.hasSMTError/VCResult.hasSMTErrortoVerifier.leanalongside the other nine-case predicates, and use them to simplifynImplErrorinprintPyAnalyzeSummary.🤖 Generated with Claude Code