feat: Implement two-sided verification check with check modes#487
feat: Implement two-sided verification check with check modes#487MikaelMayer wants to merge 115 commits intomainfrom
Conversation
Implement the two-sided verification check design that distinguishes between 'always true', 'always false', 'indecisive', and 'unreachable' outcomes. Key changes: - Add checkSatAssuming to SMT Solver for assumption-based queries - Replace Outcome inductive with VCOutcome structure containing two SMT.Result fields - Add CheckMode enum (full/validity/satisfiability) to Options - Update encoder to emit two check-sat-assuming commands - Update SARIF output to handle nine possible outcome combinations - Default to validity mode for backward compatibility The two-sided check asks: 1. Can the property be true? (satisfiability check) 2. Can the property be false? (validity check) This enables distinguishing: - pass (sat, unsat): always true and reachable - refuted (unsat, sat): always false and reachable - indecisive (sat, sat): true or false depending on inputs - unreachable (unsat, unsat): path condition contradictory - Five partial outcomes when one check returns unknown Breaking change: VCResult API changed, all consumers must be updated. Tests need updating to reflect new default behavior (validity mode only). See TWO_SIDED_CHECK_IMPLEMENTATION.md for complete implementation details.
- Add CLI parsing for --check-mode flag (full/validity/satisfiability) - Remove deprecated --reach-check flag - Update help message with check mode documentation - Fix StrataVerify to use 'outcome' field instead of 'result' - Update emoji symbols for better visual distinction: - ✅ for pass (valid and reachable) - ✔️ for always true if reachable - ✖️ for refuted if reachable - ❌ for refuted (always false and reachable) - ⛔ for unreachable - 🔶 for indecisive - ➕ for satisfiable - ➖ for reachable and can be false
- Add metadata fields: fullCheck, validityCheck, satisfiabilityCheck - Add helper methods to check for these annotations - Update verifySingleEnv to check metadata before using global checkMode - Annotations override global --check-mode flag for specific statements
- Add VCOutcomeTests.lean with all 9 outcome combinations - Test both predicate methods and emoji/label rendering - Use named arguments for clarity - Update SMTEncoderTests to use full check mode for existing tests - Ensures backward compatibility with expected 'pass' outcome
- Add VCOutcomeTests.lean with all 9 outcome combinations - Each test shows emoji and label in output for easy verification - Use named arguments for clarity - Update SMTEncoderTests to use full check mode for existing tests - Ensures backward compatibility with expected 'pass' outcome
- Add VCOutcomeTests.lean with all 9 outcome combinations - Use formatOutcome helper to avoid repetition - Each test shows emoji and label in output - Use named arguments for clarity - Update SMTEncoderTests to use full check mode - Ensures backward compatibility with expected 'pass' outcome
- Document CLI flag integration - Document per-statement annotations - Document emoji updates - Document comprehensive test suite - Document test fixes for backward compatibility
- Fix StrataVerify to properly format Except String VCOutcome - Update StrataMain to use vcResult.outcome instead of vcResult.result - Use isRefuted/isRefutedIfReachable predicates for failure detection - Format outcomes with emoji and label
Clarifies that refuted outcome means reachable and always false
…ters - Rename isRefuted -> isRefutedAndReachable - Rename isIndecisive -> isIndecisiveAndReachable - Rename isRefutedIfReachable -> isAlwaysFalseIfReachable - Add backward compatibility aliases - Add cross-cutting predicates: isAlwaysFalse, isAlwaysTrue, isReachable - Enables filtering outcomes by properties across multiple cases
…ariants - isPass: true if validityProperty is unsat (always true), regardless of reachability - isPassAndReachable: true if (sat, unsat) - proven reachable and always true - isPassIfReachable: true if (unknown, unsat) - always true if reachable - Update label/emoji to use isPassAndReachable and isPassIfReachable - Update test comments to reflect new naming - Add backward compatibility alias isAlwaysTrueIfReachable
…overs all sat cases - isSatisfiable: true for any sat satisfiabilityProperty - isSatisfiableValidityUnknown: specific case (sat, unknown) - Rename isPassIfReachable -> isPassReachabilityUnknown - Rename isAlwaysFalseIfReachable -> isAlwaysFalseReachabilityUnknown - Rename isReachableAndCanBeFalse -> isCanBeFalseAndReachable - All predicates now have reachability info at the end - Add backward compatibility aliases for all old names
- Nine base cases without 'is': passAndReachable, refutedAndReachable, etc. - Derived predicates with 'is': isPass, isSatisfiable, isReachable, etc. - Base cases represent exact outcome combinations - Derived predicates check properties across multiple outcomes - Update SarifOutput to use base cases in outcomeToLevel/outcomeToMessage - Update label/emoji functions to use base cases - Maintain backward compatibility aliases for all old names
- Add VerificationMode enum: deductive vs bugFinding - Deductive mode: only pass is success, anything not proven is error/warning - Bug finding mode: refuted is error, unknown is acceptable warning - Group outcomes by severity (one .none, one .error, one .warning, one .note per mode) - Default to deductive mode for backward compatibility
…e isAlwaysFalse - Deductive mode: only pass/unreachable are success/note, everything else is error - Bug finding mode: use isAlwaysFalse predicate instead of listing base cases - Cleaner and more maintainable
…achable is warning in deductive - Consistent naming: use 'alwaysFalse' instead of 'refuted' in base cases - Deductive mode: unreachable is warning (dead code detection) - Update all references in Verifier.lean and SarifOutput.lean - Maintain backward compatibility aliases
- Replace isAlwaysFalse with explicit base cases: alwaysFalseAndReachable, alwaysFalseReachabilityUnknown - Add comment listing all error cases in deductive mode - Clearer mapping from base cases to severity levels
- Remove 'Verification succeeded/failed' language - Use neutral descriptions: 'Always true and reachable', 'Always false and reachable' - Messages work for any property type (assertion, invariant, requires, etc.) - Shorter and clearer messages
…nknown outcomes - alwaysFalseReachabilityUnknown has validityProperty = unknown (not sat), no counterexample - unknown outcome can have models from either satisfiability or validity property - Show models from both properties when available for unknown outcome
- alwaysFalseReachabilityUnknown has validityProperty = unknown (no model) - unknown outcome also has no models (Result.unknown carries no data) - Only Result.sat carries counterexample models
…rties - Eliminates redundant predicate checks in outcomeToMessage - Single exhaustive match covers all 9 base cases plus error cases - More concise and easier to verify correctness
- Test predicates, messages, and severity levels for each outcome - Verify deductive and bug finding modes produce correct SARIF levels - Self-contained test outputs with no numbered comments - Tests ensure SARIF output matches predicate semantics
- Add missing validityCheck parameter (now takes satisfiabilityCheck and validityCheck) - Use Except.ok/Except.error to avoid ambiguity
|
I think we should copy the explanation table somewhere more permanent than the PR description. |
On this line, we proved that P ∧ Q is unsat, and P ∧ ¬Q is sat. Hence, P is sat, meaning the path condition makes Q reachable.
Here is the following. In this one, we have P == true, Q == (x > 0), ¬Q == !(x > 0).
That's an excellent question. What this case proves is that, if the line is reached, it will surely cause a failure in the assertion. Since we assume in a well-formed codebase that every line is eventually reachable, and that assertions should never fail if reachable, I consider it as a bug, but I'm open to other narratives.
The problem is modularity. If we prove You are right there was an issue it has to be "can be false and reachable". Excellent finding. Let me fix that.
Let's continue the conversation to see how I could best rephrase those
If you check |
your table misses one case for bug finding, which is the case when something is refuted if reachable, which indicates either dead code or wrong code, but that's exactly my point in the previous discussion and I'm happy to discuss it further. |
| Obligation: unreach_cover | ||
| Property: cover | ||
| Result: ❌ fail (❗path unreachable) | ||
| Result: ⛔ unreachable |
There was a problem hiding this comment.
This assert and this cover should produce pass and fail respectively, even if they are both reachable.
| Obligation: pe_assert_pass | ||
| Property: assert | ||
| Result: ✅ pass (❗path unreachable) | ||
| Result: ✅ pass and reachable from declaration entry |
There was a problem hiding this comment.
I'm concerned about this. We say that the assertion is suddenly provably reachable when before this PR it was proved to be unreachable. Investigate the test and figure out what is wrong and what is right.
|
|
||
| /-- | ||
| info: #["assertion holds vacuously (path unreachable)", "cover property is unreachable"] | ||
| info: #[] |
There was a problem hiding this comment.
It seems that the test stops producing something that was meaningful. Why?
|
Thanks a lot for the detailed answer Mikael! Btw, I find this PR really cool! I have no idea how you came up with all this. The table is impressive as well.
I see, makes sense. I think I would phrase this as that the user is unsure whether they have all the requires clauses they need, so they want us to differentiate between a bug that occurs for every input and one that only occurs on some inputs. Maybe the UX could be: Flags: The success or failure of the verification then depends on the answer to: is there a runtime violation of an assertion?
Note that the above means we never report |
deductive mode has the notion of passing = all assertions are true at minimum if reachable. But more information is usually useful to fix bugs (and also prove code), such as reachability (we need to fix the path) or refutability for validity (wait perhaps we were asserting the opposite of what is true!), This is why there are 2 modes and 2 levels of reporting. Having only three levels means we are not offering one of the original 4 combinations:
Any tool using Strata could however skip one of these modes if they want to. Maybe I'm understanding something else than what you are bringing thought. Is your remark as being about the error level of always false if reachable in the case of bugFinding mode? That it should be decided by the user? I was hoping that if that is the case, since the strata tool would typically be invoked by tools, they would do the filtering themselves. |
- pass and reachable → always true and is reachable - refuted and reachable → always false and is reachable - satisfiable → can be true and is reachable - pass if reachable → always true if reachable
| def defaultSolver : String := "cvc5" | ||
|
|
||
| /-- Check amount: how much information to gather -/ | ||
| inductive CheckAmount where |
There was a problem hiding this comment.
smallest of nits/feel free to ignore: can we say CheckLevel instead? Amount to me signals that something numeric is involved...
| A model expressed as Core `LExpr` values, suitable for display | ||
| using Core's expression formatter and for future use as program metadata. | ||
| -/ | ||
| abbrev LExprModel := List (Expression.Ident × LExpr CoreLParams.mono) |
There was a problem hiding this comment.
Did LExprModel go away in this PR, or am I missing something?
I agree that knowing that something is not reachable is useful information, but I think this information is significantly less important then answering the question "can my program violate an assertion at runtime?" and I would consider these as two separate questions.
I suggested having 3 levels for the main question, and two levels for the reachability question (on/off), so a combination of 6 options. I think with the 4 modes you describe you're leaving out one of the three options of the first question: testing for all proven bugs assuming that the preconditions are complete. It's in between your deductive and bug finding mode. In this mode, the "indecisive and reachable" and "can be false and is reachable" rows from your table would report an error, and otherwise it would behave like the bug finding mode. Do you think this is not a valid use-case? Maybe it's not. If you consider the preconditions to be part of the correctness proof, and the "bug finding mode" is one where you don't want to fail when the proof is incomplete, then indeed you don't care about that case. However, if we think providing complete preconditions is simpler than providing a correctness proof, then I think "test for all proven bugs assuming that the preconditions are complete" could be useful. There are many bugs that only trigger on some inputs, so we could find a lot more bugs with this mode than with the bug finding mode that you're describing. |
4 participants
Summary
Replaces the single-sided
reachCheckflag with a two-sided verification framework using orthogonal check mode and check amount flags. Each proof obligation now produces aVCOutcomewith independent satisfiability and validity properties, enabling richer diagnostic feedback.Problem
We want to perform richer checks on assert statements beyond simple validity. Covers are existential checks where forking into two means the results are linked by an OR, so they are not suitable for detecting assertions that surely fail along a path. To find such failures, checks must be encoded as assertions, and we need extended diagnostics for them.
A previous PR opened the way by adding a reachability check, demonstrating that two checks per command are feasible. However, the reachability check missed an important case for bug-finding mode: from reachability + validity alone, we cannot derive the result of reachability + satisfiability. By testing both
P ∧ Q(satisfiability) andP ∧ ¬Q(validity) wherePis the path condition andQis the property, we get two checks that together determine the validity and satisfiability ofQgivenP, and also derive reachability.Solution
Two orthogonal flags replace
reachCheck:--check-mode):deductive(default) orbugFinding--check-amount):minimal(default) orfullA per-statement
@[fullCheck]annotation can override the global check amount.Possible outcomes by mode
Default mode (
deductive,minimal): validity check only for asserts, satisfiability check only for covers.For assert statements (validity only, satisfiability masked to unknown):
For cover statements (satisfiability only, validity masked to unknown):
Bug-finding mode (
bugFinding,minimal): satisfiability check only for all statement types. Same as the cover table above.Full mode (
full): both checks run, all 9 outcomes possible. The last two columns show the error reporting level in SARIF output for each mode (✅ = pass, 🔴 = error, 🟡 = warning, 🔵 = note).P ∧ QP ∧ ¬QTesting
All existing tests updated. New tests cover the full outcome matrix including per-statement
@[fullCheck]annotations. BoogieToStrata integration tests, Python analysis tests, and SARIF output all updated.