feat: Implement two-sided verification check with check modes

DiffTestCore.lean

@@ -104,11 +104,12 @@ def checkMatch (pyRegex testStr : String) (mode : MatchMode)
       let vcResults ← verify pgm inputCtx none .quiet
       match vcResults[0]? with
       | none    => return .smtError "no VCs generated"
-      | some vc => return match vc.result with
-        | .pass                    => .match
-        | .fail                    => .noMatch
-        | .unknown                 => .smtError "unknown"
-        | .implementationError msg => .smtError s!"impl: {msg}"
+      | some vc => return match vc.outcome with
+        | .ok o => 
+          if o.isPass then .match 
+          else if o.isRefuted || o.isCanBeTrueOrFalse then .noMatch 
+          else .smtError "unknown"
+        | .error msg => .smtError s!"impl: {msg}"
 
 def main (args : List String) : IO UInt32 := do
   let logDir : Option String ← match args with

Strata/DL/Imperative/EvalContext.lean

@@ -75,6 +75,12 @@ inductive PropertyType where
   | divisionByZero
   deriving Repr, DecidableEq
 
+/-- Whether an unreachable path counts as pass for this property type.
+    Assertions pass vacuously when unreachable; covers fail. -/
+def PropertyType.passWhenUnreachable : PropertyType → Bool
+  | .assert | .divisionByZero => true
+  | .cover => false
+
 instance : ToFormat PropertyType where
   format p := match p with
     | .cover => "cover"

Strata/DL/Imperative/MetaData.lean

@@ -180,6 +180,12 @@ def MetaData.fileRange : MetaDataElem.Field P := .label "fileRange"
 
 def MetaData.reachCheck : MetaDataElem.Field P := .label "reachCheck"
 
+def MetaData.fullCheck : MetaDataElem.Field P := .label "fullCheck"
+
+def MetaData.validityCheck : MetaDataElem.Field P := .label "validityCheck"
+
+def MetaData.satisfiabilityCheck : MetaDataElem.Field P := .label "satisfiabilityCheck"
+
 def MetaData.hasReachCheck {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Bool :=
   match md.findElem MetaData.reachCheck with
   | some elem =>
@@ -188,6 +194,32 @@ def MetaData.hasReachCheck {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Bool
     | _ => false
   | none => false
 
+def MetaData.hasFullCheck {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Bool :=
+  match md.findElem MetaData.fullCheck with
+  | some elem =>
+    match elem.value with
+    | .switch true => true
+    | _ => false
+  | none =>
+    -- Backward compatibility: reachCheck maps to fullCheck
+    md.hasReachCheck
+
+def MetaData.hasValidityCheck {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Bool :=
+  match md.findElem MetaData.validityCheck with
+  | some elem =>
+    match elem.value with
+    | .switch true => true
+    | _ => false
+  | none => false
+
+def MetaData.hasSatisfiabilityCheck {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Bool :=
+  match md.findElem MetaData.satisfiabilityCheck with
+  | some elem =>
+    match elem.value with
+    | .switch true => true
+    | _ => false
+  | none => false
+
 def getFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option FileRange := do
   let fileRangeElement <- md.findElem Imperative.MetaData.fileRange
   match fileRangeElement.value with

Strata/DL/Imperative/SMTUtils.lean

@@ -184,54 +184,62 @@ private def processModel {P : PureExpr} [ToFormat P.Ident]
 /--
 Interprets the output of SMT solver.
 
-Both the verdict line (sat/unsat/unknown) and the model (when sat) are
-parsed using the SMTResponse DDM dialect. The verdict is parsed as a full
-`Command`, while the model is parsed by targeting the
-`SMTResponse.GetValueResponse` category directly via
-`parseCategoryFromDialect`.
-
-When `reachCheck` is `true`, the solver output contains two verdict lines:
-the first is the reachability check result (are the path-condition assumptions
-satisfiable?), and the second is the proof check result. The reachability
-result is returned as `some Result`; when `reachCheck` is `false`, it is
-`none`.
+When two-sided checking is enabled, the solver output contains two verdict lines:
+the first is the satisfiability check result (can the property be true?),
+and the second is the validity check result (can the property be false?).
+The satisfiability result is returned as the first element of the pair;
+the validity result is the second element.
+
+When only one check is enabled, the other is returned as `unknown`.
 -/
 def solverResult {P : PureExpr} [ToFormat P.Ident]
     (typedVarToSMTFn : P.Ident → P.Ty → Except Format (String × Strata.SMT.TermType))
     (vars : List P.TypedIdent) (output : IO.Process.Output)
     (E : Strata.SMT.EncoderState) (smtsolver : String)
-    (reachCheck : Bool := false)
-    : IO (Except Format (Option (Result P.Ident) × Result P.Ident)) := do
+    (satisfiabilityCheck validityCheck : Bool)
+    : IO (Except Format (Result P.Ident × Result P.Ident)) := do
   let stdout := output.stdout
-  -- Split the next line from the remaining stdout, returning (line, rest).
-  let splitLine (s : String) : String × String :=
-    let pos := s.find (· == '\n')
-    let line := (s.extract s.startPos pos).trimAscii.toString
-    let rest := s.extract pos s.endPos
-    (line, rest)
-  -- When reachCheck is true, the first line is the reachability verdict.
-  let (reachResult, proofStdout) ← if reachCheck then do
-    let (reachLine, remaining) := splitLine stdout
-    let reachResult : Result P.Ident ← do
-      match ← parseVerdict reachLine with
-      | some (.sat _) => pure (.sat [])
-      | some .unsat   => pure .unsat
-      | _             => pure .unknown
-    pure (some reachResult, remaining.drop 1 |>.toString)
-  else
-    pure (none, stdout)
-  -- Parse the proof verdict from the (possibly trimmed) stdout.
-  let (verdictStr, rest) := splitLine proofStdout
-  match ← parseVerdict verdictStr with
-  | some (.sat _) =>
-    -- Parse model via SMTDDM targeting GetValueResponse category directly.
-    let pairs ← parseModelDDM rest
-    match processModel typedVarToSMTFn vars pairs E with
-    | .ok model => return .ok (reachResult, .sat model)
-    | .error _  => return .ok (reachResult, .sat [])
-  | some .unsat   => return .ok (reachResult, .unsat)
-  | some .unknown => return .ok (reachResult, .unknown)
-  | _ =>
+
+  -- Helper to parse a single verdict and model
+  -- Skip lines until we find a verdict (sat/unsat/unknown) or run out of input.
+  -- This is needed because get-value commands in the file may produce error
+  -- output when the preceding check-sat returned unsat.
+  let skipToNextVerdict (input : String) : String :=
+    let lines := input.splitOn "\n"
+    let rest := lines.dropWhile (fun l =>
+      let t := l.trimAscii.toString
+      t != "sat" && t != "unsat" && t != "unknown" && !t.isEmpty)
+    "\n".intercalate rest
+
+  let parseVerdict (input : String) : IO (Option (Result P.Ident × String)) := do
+    let pos := input.find (· == '\n')
+    let verdict := input.extract input.startPos pos |>.trimAscii
+    let rest := (input.extract pos input.endPos |>.drop 1).toString
+    match verdict with
+    | "sat" =>
+      let rawModel ← parseModelDDM rest
+      match (processModel typedVarToSMTFn vars rawModel E) with
+      | .ok model => return some (.sat model, skipToNextVerdict rest)
+      | .error _ => return some (.sat [], skipToNextVerdict rest)
+    | "unsat" => return some (.unsat, skipToNextVerdict rest)
+    | "unknown" => return some (.unknown, skipToNextVerdict rest)
+    | _ => return none
+
+  -- Parse results based on which checks are enabled
+  match ← (if satisfiabilityCheck then parseVerdict stdout else pure (some (.unknown, stdout))) with
+  | some (satResult, remaining) =>
+    match ← (if validityCheck then parseVerdict remaining else pure (some (.unknown, remaining))) with
+    | some (validityResult, _) => return .ok (satResult, validityResult)
+    | none =>
+      let stderr := output.stderr
+      let hasExecError := stderr.contains "could not execute external process"
+      let hasFileError := stderr.contains "No such file or directory"
+      let suggestion :=
+        if (hasExecError || hasFileError) && smtsolver == Core.defaultSolver then
+          s!" \nEnsure {Core.defaultSolver} is on your PATH or use --solver to specify another SMT solver."
+        else ""
+      return .error s!"stderr:{stderr}{suggestion}\nsolver stdout: {output.stdout}\n"
+  | none =>
     let stderr := output.stderr
     let hasExecError := stderr.contains "could not execute external process"
     let hasFileError := stderr.contains "No such file or directory"
@@ -258,34 +266,31 @@ def addLocationInfo {P : PureExpr} [BEq P.Ident]
 Writes the proof obligation to file, discharge the obligation using SMT solver,
 and parse the output of the SMT solver.
 
-When `reachCheck` is `true`, the generated SMT file will contain two
-`(check-sat)` commands (one for reachability, one for the proof obligation),
-and the return value includes the reachability decision.
+When two-sided checking is enabled, the generated SMT file will contain two
+`(check-sat-assuming)` commands, one for `P ∧ Q` and one for `P ∧ ¬Q`,
+and the return value includes both decisions.
 -/
 def dischargeObligation {P : PureExpr} [ToFormat P.Ident] [BEq P.Ident]
   (encodeSMT : Strata.SMT.SolverM (List String × Strata.SMT.EncoderState))
   (typedVarToSMTFn : P.Ident → P.Ty → Except Format (String × Strata.SMT.TermType))
   (vars : List P.TypedIdent)
-  (md : Imperative.MetaData P)
+  (_md : Imperative.MetaData P)
   (smtsolver filename : String)
   (solver_options : Array String) (printFilename : Bool)
-  (reachCheck : Bool := false) :
-  IO (Except Format (Option (Result P.Ident) × Result P.Ident × Strata.SMT.EncoderState)) := do
+  (satisfiabilityCheck validityCheck : Bool) :
+  IO (Except Format (Result P.Ident × Result P.Ident × Strata.SMT.EncoderState)) := do
   let handle ← IO.FS.Handle.mk filename IO.FS.Mode.write
   let solver ← Strata.SMT.Solver.fileWriter handle
 
-  let encodeAndCheck : Strata.SMT.SolverM (List String × Strata.SMT.EncoderState) := do
-    let result ← encodeSMT
-    addLocationInfo md ("sat-message", s!"\"Assertion cannot be proven\"")
-    let _ ← Strata.SMT.Solver.checkSat result.1 -- Will return unknown for Solver.fileWriter
-    return result
-  let ((_ids, estate), _solverState) ← encodeAndCheck.run solver
+  -- encodeSMT (which calls encodeCore) emits check-sat commands internally
+  let ((_ids, estate), _solverState) ← encodeSMT.run solver
+
   if printFilename then IO.println s!"Wrote problem to {filename}."
 
   let solver_output ← runSolver smtsolver (#[filename] ++ solver_options)
-  match ← solverResult typedVarToSMTFn vars solver_output estate smtsolver (reachCheck := reachCheck) with
+  match ← solverResult typedVarToSMTFn vars solver_output estate smtsolver satisfiabilityCheck validityCheck with
   | .error e => return .error e
-  | .ok (reachDecision, result) => return .ok (reachDecision, result, estate)
+  | .ok (satResult, validityResult) => return .ok (satResult, validityResult, estate)
 
 ---------------------------------------------------------------------
 end -- public section

Strata/DL/SMT/Solver.lean

@@ -265,6 +265,22 @@ def checkSat (vars : List String) : SolverM Decision := do
     return Decision.unknown
   | other     => throw (IO.userError s!"Unrecognized solver output: {other}")
 
+def checkSatAssuming (assumptions : List String) (vars : List String) : SolverM Decision := do
+  let assumptionsStr := String.intercalate " " assumptions
+  emitln s!"(check-sat-assuming ({assumptionsStr}))"
+  let result := (← readlnD "unknown").trimAscii.toString
+  match result with
+  | "sat"     =>
+    if !vars.isEmpty then
+      getValue vars
+    return Decision.sat
+  | "unsat"   => return Decision.unsat
+  | "unknown" =>
+    if !vars.isEmpty then
+      getValue vars
+    return Decision.unknown
+  | other     => throw (IO.userError s!"Unrecognized solver output: {other}")
+
 def reset : SolverM Unit :=
   emitln "(reset)"
 

Strata/Languages/Core/Options.lean

@@ -22,6 +22,16 @@ def VerboseMode.toNat (v : VerboseMode) : Nat :=
   | .normal => 2
   | .debug => 3
 
+/-- Verification mode for SARIF error level mapping -/
+inductive VerificationMode where
+  | deductive  -- Prove correctness (unknown is error)
+  | bugFinding -- Find bugs assuming incomplete preconditions (only definite bugs are errors)
+  | bugFindingAssumingCompleteSpec -- Find bugs assuming complete preconditions (any counterexample is error)
+  deriving Repr, DecidableEq
+
+instance : Inhabited VerificationMode where
+  default := .deductive
+
 def VerboseMode.ofBool (b : Bool) : VerboseMode :=
   match b with
   | false => .quiet
@@ -45,6 +55,16 @@ instance : DecidableRel (fun a b : VerboseMode => a ≤ b) :=
 /-- Default SMT solver to use -/
 def defaultSolver : String := "cvc5"
 
+/-- Check level: how much information to gather and display -/
+inductive CheckLevel where
+  | minimal         -- One check, simple messages (pass/fail/unknown)
+  | minimalVerbose  -- One check, detailed messages (always true if reached, etc.)
+  | full            -- Both checks, detailed messages (all 9 outcomes)
+  deriving Repr, DecidableEq
+
+instance : Inhabited CheckLevel where
+  default := .minimal
+
 structure VerifyOptions where
   verbose : VerboseMode
   parseOnly : Bool
@@ -62,22 +82,10 @@ structure VerifyOptions where
   solver : String
   /-- Directory to store VCs -/
   vcDirectory : Option System.FilePath
-  /--
-  Enable reachability checks for all assert and cover statements.
-  When enabled, the verifier emits an extra `(check-sat)` before each
-  proof obligation to test whether the path-condition assumptions are
-  satisfiable. If they are not (i.e., the code path is unreachable),
-  the obligation is reported as `❗ unreachable` instead of the
-  normal pass/fail outcome.
-
-  This flag applies to **every** obligation that reaches the verifier,
-  including obligations generated by transforms such as call elimination
-  (precondition asserts) and procedure inlining. Individual statements
-  can also opt in via the `@[reachCheck]` annotation without enabling
-  this global flag.
-
-  Off by default. CLI: `--reach-check`. -/
-  reachCheck : Bool
+  /-- Check mode: deductive (prove correctness) or bugFinding (find bugs) -/
+  checkMode : VerificationMode
+  /-- Check amount: minimal (only necessary checks) or full (both checks for better messages) -/
+  checkLevel : CheckLevel
 
 def VerifyOptions.default : VerifyOptions := {
   verbose := .normal,
@@ -91,7 +99,8 @@ def VerifyOptions.default : VerifyOptions := {
   outputSarif := false,
   solver := defaultSolver
   vcDirectory := .none
-  reachCheck := false
+  checkMode := .deductive
+  checkLevel := .minimal
 }
 
 instance : Inhabited VerifyOptions where

Strata/Languages/Core/SMTEncoder.lean

@@ -650,26 +650,9 @@ def toSMTTerms (E : Env) (es : List (LExpr CoreLParams.mono)) (ctx : SMT.Context
     .ok ((et :: erestt), ctx)
 
 /--
-Encode a proof obligation -- which may be of type `assert` or `cover` -- into
-SMTLIB.
-
-Under conditions `P`, `assert(Q)` is encoded into SMTLib as follows:
-```
-(assert P)
-(assert (not Q))
-(check-sat)
-```
-If the result is `unsat`, then `P ∧ ¬Q` is unsatisfiable, which means `P => Q`
-is valid. If the result is `sat`, then the assertion is violated.
-
-Under conditions `P`, `cover(Q)` is encoded into SMTLib as follows:
-```
-(assert P)
-(assert Q)
-(check-sat)
-```
-If the result is `unsat`, then `P ∧ Q` is unsatisfiable, which means that the
-cover is violated. If the result is `sat`, then the cover succeeds.
+Encode a proof obligation into SMT terms: path conditions (P) and obligation (Q).
+The obligation Q is returned without negation; see `encodeCore` in Verifier.lean
+for the check-sat encoding that applies negation for validity checks.
 -/
 def ProofObligation.toSMTTerms (E : Env)
   (d : Imperative.ProofObligation Expression) (ctx : SMT.Context := SMT.Context.default)
@@ -682,11 +665,7 @@ def ProofObligation.toSMTTerms (E : Env)
     (λ ts => Term.app (.core .distinct) ts .bool)
   let (assumptions_terms, ctx) ← Core.toSMTTerms E assumptions ctx useArrayTheory
   let (obligation_pos_term, ctx) ← Core.toSMTTerm E [] d.obligation ctx useArrayTheory
-  let obligation_term :=
-    if d.property == .cover then
-      obligation_pos_term
-    else
-      Factory.not obligation_pos_term
+  let obligation_term := obligation_pos_term
   .ok (distinct_assumptions ++ assumptions_terms, obligation_term, ctx)
 
 ---------------------------------------------------------------------