From b5b139886c2eb90bd5f05caa46fc9f887fcabbbc Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 12 Feb 2026 08:36:32 -0600 Subject: [PATCH 1/6] Fix cover diagnostic messages to distinguish from assertions --- Strata/Languages/Core/Verifier.lean | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean index d52d5f8dc..42f53b024 100644 --- a/Strata/Languages/Core/Verifier.lean +++ b/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" From a56b8ce71ea3a5eaa8c458144e03b73c95762def Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 12 Feb 2026 20:51:12 +0000 Subject: [PATCH 2/6] Add tests for cover diagnostic messages - Test that cover failures produce 'cover property is not satisfiable' - Test that assert failures produce 'assertion does not hold' - Test that passing statements produce no diagnostics - Extract only messages to avoid unstable byteIdx in test expectations --- .../Core/Examples/CoverDiagnostics.lean | 86 +++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 StrataTest/Languages/Core/Examples/CoverDiagnostics.lean diff --git a/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean b/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean new file mode 100644 index 000000000..ea1dd0be0 --- /dev/null +++ b/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean @@ -0,0 +1,86 @@ +/- + 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 diagnostic messages are different for cover vs assert +def mixedFailuresPgm := +#strata +program Core; +procedure Test() returns () +{ + var x : int; + + cover [cover_fail]: (false); + assert [assert_fail]: (false); +}; +#end + +/-- +info: #["cover property is not satisfiable", "assertion does not hold"] +-/ +#guard_msgs in +#eval do + let results ← verify "cvc5" mixedFailuresPgm (options := Options.quiet) + let diagnostics := results.filterMap toDiagnosticModel + return diagnostics.map DiagnosticModel.message + +--------------------------------------------------------------------- + +--------------------------------------------------------------------- From ccd776ccaffc43e595eed7393407bf6214600046 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 12 Feb 2026 20:52:57 +0000 Subject: [PATCH 3/6] Remove redundant test case --- .../Core/Examples/CoverDiagnostics.lean | 30 ++----------------- 1 file changed, 2 insertions(+), 28 deletions(-) diff --git a/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean b/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean index ea1dd0be0..cdf2d9e49 100644 --- a/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean +++ b/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean @@ -27,7 +27,7 @@ info: #["cover property is not satisfiable", "assertion does not hold"] -/ #guard_msgs in #eval do - let results ← verify "cvc5" coverDiagnosticsPgm (options := Options.quiet) + let results ← verify "z3" coverDiagnosticsPgm (options := Options.quiet) let diagnostics := results.filterMap toDiagnosticModel return diagnostics.map DiagnosticModel.message @@ -53,34 +53,8 @@ info: #[] -/ #guard_msgs in #eval do - let results ← verify "cvc5" passingPgm (options := Options.quiet) + let results ← verify "z3" passingPgm (options := Options.quiet) let diagnostics := results.filterMap toDiagnosticModel return diagnostics.map DiagnosticModel.message --------------------------------------------------------------------- - --- Test diagnostic messages are different for cover vs assert -def mixedFailuresPgm := -#strata -program Core; -procedure Test() returns () -{ - var x : int; - - cover [cover_fail]: (false); - assert [assert_fail]: (false); -}; -#end - -/-- -info: #["cover property is not satisfiable", "assertion does not hold"] --/ -#guard_msgs in -#eval do - let results ← verify "cvc5" mixedFailuresPgm (options := Options.quiet) - let diagnostics := results.filterMap toDiagnosticModel - return diagnostics.map DiagnosticModel.message - ---------------------------------------------------------------------- - ---------------------------------------------------------------------- From a9a68b4d40abe6db5b40d6cce41eab51f3dbbc4f Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 12 Feb 2026 20:53:33 +0000 Subject: [PATCH 4/6] Restore cvc5 as default SMT solver --- Strata/Languages/Core/Options.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Strata/Languages/Core/Options.lean b/Strata/Languages/Core/Options.lean index 519c1395c..5d6c1150a 100644 --- a/Strata/Languages/Core/Options.lean +++ b/Strata/Languages/Core/Options.lean @@ -37,7 +37,7 @@ instance : DecidableRel (fun a b : VerboseMode => a ≤ b) := fun a b => decidable_of_iff (a.toNat ≤ b.toNat) Iff.rfl /-- Default SMT solver to use -/ -def defaultSolver : String := "z3" +def defaultSolver : String := "cvc5" structure Options where verbose : VerboseMode From 078bce904c4d1b13e516f982f952400be09b31a6 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 12 Feb 2026 20:56:27 +0000 Subject: [PATCH 5/6] Add test for cover pass with assert unknown Tests that same expression (x > 0) produces no diagnostic for cover (satisfiable) but produces 'assertion could not be proved' for assert (unprovable) --- .../Core/Examples/CoverDiagnostics.lean | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean b/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean index cdf2d9e49..d06ade39f 100644 --- a/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean +++ b/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean @@ -58,3 +58,28 @@ info: #[] 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 "z3" coverPassAssertFailPgm (options := Options.quiet) + let diagnostics := results.filterMap toDiagnosticModel + return diagnostics.map DiagnosticModel.message + +--------------------------------------------------------------------- From 48d5ce482ff2fb760f4fd17d8c1a2579117cc88a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 12 Feb 2026 20:56:54 +0000 Subject: [PATCH 6/6] Add test for cover pass with assert unknown, use cvc5 Tests that same expression (x > 0) produces no diagnostic for cover (satisfiable) but produces 'assertion could not be proved' for assert (unprovable) --- StrataTest/Languages/Core/Examples/CoverDiagnostics.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean b/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean index d06ade39f..dedacf856 100644 --- a/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean +++ b/StrataTest/Languages/Core/Examples/CoverDiagnostics.lean @@ -27,7 +27,7 @@ info: #["cover property is not satisfiable", "assertion does not hold"] -/ #guard_msgs in #eval do - let results ← verify "z3" coverDiagnosticsPgm (options := Options.quiet) + let results ← verify "cvc5" coverDiagnosticsPgm (options := Options.quiet) let diagnostics := results.filterMap toDiagnosticModel return diagnostics.map DiagnosticModel.message @@ -53,7 +53,7 @@ info: #[] -/ #guard_msgs in #eval do - let results ← verify "z3" passingPgm (options := Options.quiet) + let results ← verify "cvc5" passingPgm (options := Options.quiet) let diagnostics := results.filterMap toDiagnosticModel return diagnostics.map DiagnosticModel.message @@ -78,7 +78,7 @@ info: #["assertion could not be proved"] -/ #guard_msgs in #eval do - let results ← verify "z3" coverPassAssertFailPgm (options := Options.quiet) + let results ← verify "cvc5" coverPassAssertFailPgm (options := Options.quiet) let diagnostics := results.filterMap toDiagnosticModel return diagnostics.map DiagnosticModel.message