Fix cover diagnostic messages to distinguish from assertions

Strata/Languages/Core/Verifier.lean

@@ -492,12 +492,35 @@ def verify
     panic! s!"DDM Transform Error: {repr errors}"
 
 def toDiagnosticModel (vcr : Core.VCResult) : Option DiagnosticModel := do
+  let isCover := vcr.obligation.property == .cover
   match vcr.result with
   | .pass => none  -- Verification succeeded, no diagnostic
+  | .unknown =>
+    -- For unknown results on cover statements, only report in debug/verbose mode
+    -- (it's informational, not an error). For asserts, unknown is always a problem.
+    if isCover && vcr.verbose ≤ .normal then
+      none
+    else
+      let message := if isCover then "cover property could not be checked"
+                     else "assertion could not be proved"
+      let .some fileRangeElem := vcr.obligation.metadata.findElem Imperative.MetaData.fileRange
+        | some {
+            fileRange := default
+            message := s!"Internal error: diagnostics without position! obligation label: {repr vcr.obligation.label}"
+          }
+      match fileRangeElem.value with
+      | .fileRange fileRange =>
+        some { fileRange := fileRange, message := message }
+      | _ =>
+        some {
+          fileRange := default
+          message := s!"Internal error: diagnostics without position! Metadata value for fileRange key was not a fileRange. obligation label: {repr vcr.obligation.label}"
+        }
   | result =>
     let message := match result with
-      | .fail => "assertion does not hold"
-      | .unknown => "assertion could not be proved"
+      | .fail =>
+        if isCover then "cover property is not satisfiable"
+        else "assertion does not hold"
       | .implementationError msg => s!"verification error: {msg}"
       | _ => panic "impossible"
 

StrataTest/Languages/Core/Examples/CoverDiagnostics.lean

@@ -0,0 +1,85 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Core.Verifier
+
+---------------------------------------------------------------------
+namespace Strata
+
+def coverDiagnosticsPgm :=
+#strata
+program Core;
+procedure Test() returns ()
+{
+  var x : int;
+  assume (x >= 0);
+
+  cover [unsatisfiable_cover]: (x < 0);
+  assert [failing_assert]: (x < 0);
+};
+#end
+
+/--
+info: #["cover property is not satisfiable", "assertion does not hold"]
+-/
+#guard_msgs in
+#eval do
+  let results ← verify "cvc5" coverDiagnosticsPgm (options := Options.quiet)
+  let diagnostics := results.filterMap toDiagnosticModel
+  return diagnostics.map DiagnosticModel.message
+
+---------------------------------------------------------------------
+
+
+-- Test that passing cover and assert produce no diagnostics
+def passingPgm :=
+#strata
+program Core;
+procedure Test() returns ()
+{
+  var x : int;
+  assume (x >= 0);
+
+  cover [satisfiable_cover]: (x >= 0);
+  assert [passing_assert]: (x >= 0);
+};
+#end
+
+/--
+info: #[]
+-/
+#guard_msgs in
+#eval do
+  let results ← verify "cvc5" passingPgm (options := Options.quiet)
+  let diagnostics := results.filterMap toDiagnosticModel
+  return diagnostics.map DiagnosticModel.message
+
+---------------------------------------------------------------------
+
+
+-- Test that satisfiable cover produces no diagnostic while unprovable assert does
+def coverPassAssertFailPgm :=
+#strata
+program Core;
+procedure Test() returns ()
+{
+  var x : int;
+
+  cover [satisfiable_cover]: (x > 0);
+  assert [unprovable_assert]: (x > 0);
+};
+#end
+
+/--
+info: #["assertion could not be proved"]
+-/
+#guard_msgs in
+#eval do
+  let results ← verify "cvc5" coverPassAssertFailPgm (options := Options.quiet)
+  let diagnostics := results.filterMap toDiagnosticModel
+  return diagnostics.map DiagnosticModel.message
+
+---------------------------------------------------------------------