feat: Implement two-sided verification check with check modes#487
Draft
MikaelMayer wants to merge 72 commits intomainfrom
Draft
feat: Implement two-sided verification check with check modes#487MikaelMayer wants to merge 72 commits intomainfrom
MikaelMayer wants to merge 72 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
MikaelMayer
commented
Feb 26, 2026
MikaelMayer
commented
Feb 26, 2026
- 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
Update result labels to be more precise about what 'reachable' means: - 'pass and reachable' → 'pass and reachable from declaration entry' - 'refuted and reachable' → 'refuted and reachable from declaration entry' - 'indecisive and reachable' → 'indecisive and reachable from declaration entry' - 'reachable and can be false' → 'reachable from declaration entry and can be false' Also update emoji for unknown from 🟡 to ❓ and consolidate unreachable messages. This clarifies that reachability is checked from the entry point of the procedure/function containing the assertion, not from program entry.
PE (partial evaluation) and SMT can prove both satisfiability and validity even when only one check was requested. This commit masks the outcome properties to only show the checks that were requested, ensuring that validity-only checks show 'pass if reachable' instead of 'pass and reachable'. The check selection logic determines which checks to perform based on: - Metadata annotations (@[fullCheck]) - Check mode (deductive vs bugFinding) - Check amount (minimal vs full) - Property type (assert vs cover) For deductive + minimal + assert (the default), only validity is checked. Known issue: Some outcome labels don't handle masked outcomes well and may show misleading messages like 'reachable and can be false' instead of 'fail'. This will be addressed in a follow-up commit by updating the outcome labels.
…checks don't generate models)
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.
Summary
Implements two-sided verification check with orthogonal check mode and check amount flags, enabling fine-grained control over satisfiability and validity checking.
Problem
Traditional deductive verification only checks validity (whether assertions are always true), but some use cases need satisfiability checks (whether assertions can be true) to verify reachability or detect vacuous proofs. The system needed a clear way to specify both what to verify and how much diagnostic information to gather.
Solution
This PR adds two orthogonal command-line flags:
1. Check Mode (
--check-mode): What are we trying to achieve?deductive(default): Prove correctness - requires validity checksbugFinding: Find bugs - requires satisfiability checks2. Check Amount (
--check-amount): How much checking to do?minimal(default): Only run checks needed for the check modefull: Run both checks for more informative diagnostic messagesAdditional Features
Per-statement annotation:
fullCheckforces both checks for a specific statement, overriding global check-amountNine outcome combinations: Distinguishes between pass/refuted (with reachability info), unreachable, indecisive, and unknown states with clear emoji indicators
Enhanced visual feedback: Updated emoji symbols for better accessibility and distinction between similar outcomes
SARIF output levels: Check mode determines how outcomes are reported in SARIF format
Testing
Backward Compatibility
Default
deductivemode withminimalcheck amount preserves existing verification behavior. Existing programs work without changes.