Verification mode to check if path conditions are satisfiable

Examples/expected/ProcedureTypeError.core.expected

@@ -1,3 +1,3 @@
 Successfully parsed.
-ProcedureTypeError.core.st(21,(4-32)) ❌ Type checking error.
+ProcedureTypeError.core.st(21,(4-32)) ❌ Error.
 [SumPositive:precond2]: Cannot find this fvar in the context! c

Examples/expected/TypeError.core.expected

@@ -1,4 +1,4 @@
 Successfully parsed.
-TypeError.core.st(25,(2-18)) ❌ Type checking error.
+TypeError.core.st(25,(2-18)) ❌ Error.
 Impossible to unify (Map int (Map bool bool)) with (Map int int).
 First mismatch: (Map bool bool) with int.

Strata/DL/Imperative/CmdEval.lean

@@ -14,10 +14,16 @@ open Std (ToFormat Format format)
 
 --------------------------------------------------------------------
 
+def checkAssumptionsSatMode [BEq P.Ident] (md : MetaData P) :
+    Imperative.AssumptionSatCheckMode :=
+  match Imperative.MetaData.getCheckAssumptionsSat md with
+    | none => .globalDefault
+    | some b => if b then .check else .noCheck
+
 /--
 Partial evaluator for an Imperative Command.
 -/
-def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
+def Cmd.eval [EC : EvalContext P S] [BEq P.Ident] (σ : S) (c : Cmd P) : Cmd P × S :=
   match EC.lookupError σ with
   | some _ => (c, σ)
   | none =>
@@ -56,16 +62,17 @@ def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
       let e := EC.eval σ e
       let assumptions := EC.getPathConditions σ
       let c' := .assert label e md
+      let checkAssum := checkAssumptionsSatMode md
       match EC.denoteBool e with
       | some true => -- Proved via evaluation.
-        (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+        (c', EC.deferObligation σ (ProofObligation.mk label .assert checkAssum assumptions e md))
       | some false =>
         if assumptions.isEmpty then
           (c', EC.updateError σ (.AssertFail label e))
         else
-          (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+          (c', EC.deferObligation σ (ProofObligation.mk label .assert checkAssum assumptions e md))
       | none =>
-        (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+        (c', EC.deferObligation σ (ProofObligation.mk label .assert checkAssum assumptions e md))
 
     | .assume label e md =>
       let (e, σ) := EC.preprocess σ c e
@@ -85,12 +92,13 @@ def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
       let e := EC.eval σ e
       let assumptions := EC.getPathConditions σ
       let c' := .cover label e md
-      (c', EC.deferObligation σ (ProofObligation.mk label .cover assumptions e md))
+      let checkAssum := checkAssumptionsSatMode md
+      (c', EC.deferObligation σ (ProofObligation.mk label .cover checkAssum assumptions e md))
 
 /--
 Partial evaluator for Imperative's Commands.
 -/
-def Cmds.eval [EvalContext P S] (σ : S) (cs : Cmds P) : Cmds P × S :=
+def Cmds.eval [EvalContext P S] [BEq P.Ident] (σ : S) (cs : Cmds P) : Cmds P × S :=
   match cs with
   | [] => ([], σ)
   | c :: crest =>

Strata/DL/Imperative/EvalContext.lean

@@ -73,6 +73,12 @@ inductive PropertyType where
   | assert
   deriving Repr, DecidableEq
 
+inductive AssumptionSatCheckMode where
+  | check
+  | noCheck
+  | globalDefault
+  deriving Repr, DecidableEq
+
 instance : ToFormat PropertyType where
   format p := match p with
     | .cover => "cover"
@@ -85,6 +91,8 @@ decision procedure or via denotation into Lean.
 structure ProofObligation (P : PureExpr) where
   label : String
   property : PropertyType
+  /-- Check if assumptions are satisfiable. -/
+  checkAssumptionsSat : AssumptionSatCheckMode := .globalDefault
   assumptions : PathConditions P
   obligation : P.Expr
   metadata : MetaData P

Strata/DL/Imperative/MetaData.lean

@@ -75,12 +75,15 @@ inductive MetaDataElem.Value (P : PureExpr) where
   | msg (s : String)
   /-- Metadata value in the form of a fileRange. -/
   | fileRange (r: FileRange)
+  /-- Metadata value in the form of a boolean switch. -/
+  | switch (b : Bool)
 
 instance [ToFormat P.Expr] : ToFormat (MetaDataElem.Value P) where
   format f := match f with
               | .expr e => f!"{e}"
               | .msg s => f!"{s}"
               | .fileRange r => f!"{r}"
+              | .switch a => f!"{a}"
 
 instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
   reprPrec v prec :=
@@ -89,13 +92,15 @@ instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
       | .expr e => f!".expr {reprPrec e prec}"
       | .msg s => f!".msg {s}"
       | .fileRange fr => f!".fileRange {fr}"
+      | .switch a => f!".switch {a}"
     Repr.addAppParen res prec
 
 def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=
   match v1, v2 with
   | .expr e1, .expr e2 => e1 == e2
   | .msg m1, .msg m2 => m1 == m2
   | .fileRange r1, .fileRange r2 => r1 == r2
+  | .switch r1, .switch r2 => r1 == r2
   | _, _ => false
 
 instance [BEq P.Expr] : BEq (MetaDataElem.Value P) where
@@ -172,7 +177,7 @@ instance [Repr P.Expr] [Repr P.Ident] : Repr (MetaDataElem P) where
 def MetaData.fileRange : MetaDataElem.Field P := .label "fileRange"
 
 def getFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option FileRange := do
-  let fileRangeElement <- md.findElem Imperative.MetaData.fileRange
+  let fileRangeElement ← md.findElem Imperative.MetaData.fileRange
   match fileRangeElement.value with
     | .fileRange fileRange =>
       some fileRange
@@ -192,11 +197,20 @@ def MetaData.toDiagnosticF {P : PureExpr} [BEq P.Ident] (md : MetaData P) (msg :
 /-- Get the file range from metadata as a DiagnosticModel (for formatting).
     This is a compatibility function that formats the file range using byte offsets.
     For proper line/column display, use toDiagnostic and format with a FileMap at the top level. -/
-def MetaData.formatFileRangeD {P : PureExpr} [BEq P.Ident] (md : MetaData P) (fileMap : Option Lean.FileMap := none) (includeEnd? : Bool := false) : Format :=
+def MetaData.formatFileRangeD {P : PureExpr} [BEq P.Ident] (md : MetaData P)
+    (fileMap : Option Lean.FileMap := none) (includeEnd? : Bool := false) : Format :=
   match getFileRange md with
   | some fr => fr.format fileMap includeEnd?
   | none => f!""
 
+def MetaData.checkAssumptionsSat : MetaDataElem.Field P := .label "checkAssumptionsSat"
+
+def MetaData.getCheckAssumptionsSat {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option Bool := do
+  let elem ← md.findElem Imperative.MetaData.checkAssumptionsSat
+  match elem.value with
+    | .switch b => some b
+    | _ => none
+
 ---------------------------------------------------------------------
 
 end Imperative

Strata/DL/Imperative/SMTUtils.lean

@@ -151,7 +151,8 @@ def dischargeObligation {P : PureExpr} [ToFormat P.Ident]
   let handle ← IO.FS.Handle.mk filename IO.FS.Mode.write
   let solver ← Strata.SMT.Solver.fileWriter handle
   let (ids, estate) ← encodeTerms terms solver
-  let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter
+  let _ ← solver.checkSat
+  let _ ← solver.getDecision ids -- Will return unknown for Solver.fileWriter
   let produce_models ←
     if smtsolver.endsWith "z3" then
       -- No need to specify -model because we already have `get-value` in the

Strata/DL/SMT/Solver.lean

@@ -150,8 +150,10 @@ private def readlnD (dflt : String) : SolverM String := do
   | .some stdout => stdout.getLine
   | .none        => pure dflt
 
-def checkSat (vars : List String) : SolverM Decision := do
+def checkSat : SolverM Unit :=
   emitln "(check-sat)"
+
+def getDecision (vars : List String) : SolverM Decision := do
   let result := (← readlnD "unknown").trim
   match result with
   | "sat"     =>

Strata/Languages/B3/Verifier/Diagnosis.lean

@@ -91,7 +91,8 @@ partial def diagnoseFailureGeneric
       let _ ← push checkState
       let runCheck : SolverM Decision := do
         Solver.assert (formatTermDirect convResult.term)
-        Solver.checkSat []
+        Solver.checkSat
+        Solver.getDecision []
       let decision ← runCheck.run checkState.smtState.solver
       let _ ← pop checkState
       let isProvablyFalse := decision == .unsat

Strata/Languages/B3/Verifier/State.lean

@@ -138,7 +138,8 @@ def prove (state : B3VerificationState) (term : Term) (ctx : VerificationContext
   let _ ← push state
   let runCheck : SolverM (Decision × Option String) := do
     Solver.assert s!"(not {formatTermDirect term})"
-    let decision ← Solver.checkSat []
+    let _ ← Solver.checkSat
+    let decision ← Solver.getDecision []
     let model := if decision == .sat then some "model available" else none
     return (decision, model)
   let (decision, model) ← runCheck.run state.smtState.solver
@@ -154,7 +155,8 @@ def reach (state : B3VerificationState) (term : Term) (ctx : VerificationContext
   let _ ← push state
   let runCheck : SolverM (Decision × Option String) := do
     Solver.assert (formatTermDirect term)
-    let decision ← Solver.checkSat []
+    let _ ← Solver.checkSat
+    let decision ← Solver.getDecision []
     let model := if decision == .sat then some "reachable" else none
     return (decision, model)
   let (decision, model) ← runCheck.run state.smtState.solver

Strata/Languages/Core/DDMTransform/Parse.lean

@@ -187,14 +187,18 @@ category Label;
 
 op label (l : Ident) : Label => "[" l "]:";
 
+category CheckAssumptionsSat;
+op checkAssumOn : CheckAssumptionsSat => "@[" "checkAssumptionsSat" ":" "true" "]";
+op checkAssumOff : CheckAssumptionsSat => "@[" "checkAssumptionsSat" ":" "false" "]";
+
 @[scope(dl)]
 op varStatement (dl : DeclList) : Statement => "var " dl ";\n";
 @[declare(v, tp)]
 op initStatement (tp : Type, v : Ident, e : tp) : Statement => "var " v " : " tp " := " e ";\n";
 op assign (tp : Type, v : Lhs, e : tp) : Statement => v " := " e ";\n";
 op assume (label : Option Label, c : bool) : Statement => "assume " label c ";\n";
-op assert (label : Option Label, c : bool) : Statement => "assert " label c ";\n";
-op cover (label : Option Label, c : bool) : Statement => "cover " label c ";\n";
+op assert (checkAssum? : Option CheckAssumptionsSat, label : Option Label, c : bool) : Statement => checkAssum? "assert " label c ";\n";
+op cover (checkAssum? : Option CheckAssumptionsSat, label : Option Label, c : bool) : Statement => checkAssum? "cover " label c ";\n";
 op if_statement (c : bool, t : Block, f : Else) : Statement => "if" "(" c ")" t f;
 op else0 () : Else =>;
 op else1 (f : Block) : Else => "else" f;

Strata/Languages/Core/DDMTransform/Translate.lean

@@ -133,6 +133,19 @@ def translateReal (arg : Arg) : TransM Decimal := do
     | TransM.error s!"translateReal expects decimal lit"
   return d
 
+def translateOptionCheckAssum (arg : Arg) : TransM (Option Bool) := do
+  translateOption
+    (fun maybe_arg => do
+        match maybe_arg with
+        | none => return default
+        | some c =>
+          let .op op := c | TransM.error s!"translateLhs expected op {repr arg}"
+          match op.name with
+          | q`Core.checkAssumOn => return (some true)
+          | q`Core.checkAssumOff => return (some false)
+          | _ => return .none)
+    arg
+
 ---------------------------------------------------------------------
 
 inductive GenKind where
@@ -976,19 +989,27 @@ partial def translateStmt (p : Program) (bindings : TransBindings) (arg : Arg) :
     let id ← translateIdent CoreIdent ida
     let md ← getOpMetaData op
     return ([.havoc id md], bindings)
-  | q`Core.assert, #[la, ca] =>
+  | q`Core.assert, #[checkAssum, la, ca] =>
     let c ← translateExpr p bindings ca
     let default_name := s!"assert_{bindings.gen.assert_def}"
     let bindings := incrNum .assert_def bindings
     let l ← translateOptionLabel default_name la
+    let checkAssumMode ← translateOptionCheckAssum checkAssum
     let md ← getOpMetaData op
+    let md := if h: checkAssumMode.isSome then
+                md.pushElem Imperative.MetaData.checkAssumptionsSat (.switch (checkAssumMode.get h))
+              else md
     return ([.assert l c md], bindings)
-  | q`Core.cover, #[la, ca] =>
+  | q`Core.cover, #[checkAssum, la, ca] =>
     let c ← translateExpr p bindings ca
     let default_name := s!"cover_{bindings.gen.assert_def}"
     let bindings := incrNum .cover_def bindings
     let l ← translateOptionLabel default_name la
+    let checkAssumMode ← translateOptionCheckAssum checkAssum
     let md ← getOpMetaData op
+    let md := if h: checkAssumMode.isSome then
+                md.pushElem Imperative.MetaData.checkAssumptionsSat (.switch (checkAssumMode.get h))
+              else md
     return ([.cover l c md], bindings)
   | q`Core.assume, #[la, ca] =>
     let c ← translateExpr p bindings ca

Strata/Languages/Core/Env.lean

@@ -97,32 +97,6 @@ instance : ToFormat (ProofObligation Expression) where
 instance : ToFormat (ProofObligations Expression) where
   format os := Std.Format.joinSep (Array.map format os).toList Format.line
 
--- (FIXME) Parameterize by EvalContext typeclass.
-def ProofObligation.create
-  (label : String) (propertyType : PropertyType)
-  (assumptions : PathConditions Expression) (obligation : Procedure.Check):
-  Option (ProofObligation Expression) :=
-  open Lambda.LExpr.SyntaxMono in
-  if obligation.attr == .Free then
-    dbg_trace f!"{Format.line}Obligation {label} is free!{Format.line}"
-    none
-  else
-    some (ProofObligation.mk label propertyType assumptions obligation.expr obligation.md)
-
-def ProofObligations.createAssertions
-  (assumptions : PathConditions Expression)
-  (obligations : ListMap String Procedure.Check)
-  : ProofObligations Expression :=
-  match obligations with
-  | [] => #[]
-  | o :: orest =>
-    let orest' := ProofObligations.createAssertions assumptions orest
-    let o' :=
-      match (ProofObligation.create o.fst .assert assumptions o.snd) with
-      | none => #[]
-      | some o' => #[o']
-    o' ++ orest'
-
 /--
 A substitution map from variable identifiers to expressions.
 -/

Strata/Languages/Core/Options.lean

@@ -43,6 +43,9 @@ structure Options where
   checkOnly : Bool
   stopOnFirstError : Bool
   removeIrrelevantAxioms : Bool
+  /-- Check if assumptions are satisfiable; global setting can be overridden by
+    obligation-specific setting. -/
+  checkAssumptionsSat : Bool := false
   /-- Solver time limit in seconds -/
   solverTimeout : Nat
   /-- Output results in SARIF format -/
@@ -55,6 +58,7 @@ def Options.default : Options := {
   checkOnly := false,
   stopOnFirstError := false,
   removeIrrelevantAxioms := false,
+  checkAssumptionsSat := false,
   solverTimeout := 10,
   outputSarif := false
 }

Strata/Languages/Core/SMTEncoder.lean

@@ -565,6 +565,11 @@ def toSMTTerms (E : Env) (es : List (LExpr CoreLParams.mono)) (ctx : SMT.Context
     let (erestt, ctx) ← toSMTTerms E erest ctx
     .ok ((et :: erestt), ctx)
 
+structure SMT.Obligation where
+  assumptions : List Term
+  obligation : Term
+  checkAssumptionsSat : Bool
+
 /--
 Encode a proof obligation -- which may be of type `assert` or `cover` -- into
 SMTLIB.
@@ -587,9 +592,16 @@ Under conditions `P`, `cover(Q)` is encoded into SMTLib as follows:
 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.
 -/
-def ProofObligation.toSMTTerms (E : Env)
-  (d : Imperative.ProofObligation Expression) (ctx : SMT.Context := SMT.Context.default) :
-  Except Format ((List Term) × SMT.Context) := do
+def ProofObligation.toSMTObligation (E : Env)
+    (d : Imperative.ProofObligation Expression) (ctx : SMT.Context := SMT.Context.default) :
+    Except Format (SMT.Obligation × SMT.Context) := do
+  let checkAssumptionsSat ← match d.checkAssumptionsSat with
+    | .check => .ok true
+    | .noCheck => .ok false
+    | .globalDefault =>
+      .error "Implementation Error in ProofObligation.toSMTObligation: \
+              Global default for checking satisfiability of assumptions \
+              not supported in this context."
   let assumptions := d.assumptions.flatten.map (fun a => a.snd)
   let (ctx, distinct_terms) ← E.distinct.foldlM (λ (ctx, tss) es =>
     do let (ts, ctx') ← Core.toSMTTerms E es ctx; pure (ctx', ts :: tss)) (ctx, [])
@@ -602,7 +614,10 @@ def ProofObligation.toSMTTerms (E : Env)
       obligation_pos_term
     else
       Factory.not obligation_pos_term
-  .ok ((distinct_assumptions ++ assumptions_terms ++ [obligation_term]), ctx)
+  .ok ({assumptions := distinct_assumptions ++ assumptions_terms,
+        obligation := obligation_term,
+        checkAssumptionsSat := checkAssumptionsSat },
+       ctx)
 
 ---------------------------------------------------------------------
 

Strata/Languages/Core/SarifOutput.lean

@@ -56,8 +56,8 @@ def extractLocation (files : Map Strata.Uri Lean.FileMap) (md : Imperative.MetaD
 /-- Convert a VCResult to a SARIF Result -/
 def vcResultToSarifResult (files : Map Strata.Uri Lean.FileMap) (vcr : VCResult) : Strata.Sarif.Result :=
   let ruleId := vcr.obligation.label
-  let level := outcomeToLevel vcr.result
-  let messageText := outcomeToMessage vcr.result vcr.smtResult
+  let level := outcomeToLevel vcr.result.result
+  let messageText := outcomeToMessage vcr.result.result vcr.result.solverResult
   let message : Strata.Sarif.Message := { text := messageText }
 
   let locations := match extractLocation files vcr.obligation.metadata with