feat: Implement two-sided verification check with check modes

Examples/expected/HeapReasoning.core.expected

@@ -1,55 +1,55 @@
 Successfully parsed.
-HeapReasoning.core.st(99, 2) [modifiesFrameRef1]: ✅ pass
-HeapReasoning.core.st(104, 2) [modifiesFrameRef1]: ✅ pass
-HeapReasoning.core.st(109, 2) [modifiesFrameRef1]: ✅ pass
- [Container_ctor_ensures_4]: ✅ pass
-HeapReasoning.core.st(87, 2) [Container_ctor_ensures_7]: ✅ pass
-HeapReasoning.core.st(88, 2) [Container_ctor_ensures_8]: ✅ pass
-HeapReasoning.core.st(89, 2) [Container_ctor_ensures_9]: ✅ pass
-HeapReasoning.core.st(91, 2) [Container_ctor_ensures_10]: ✅ pass
-HeapReasoning.core.st(165, 2) [modifiesFrameRef1]: ✅ pass
-HeapReasoning.core.st(170, 2) [modifiesFrameRef2]: ✅ pass
-HeapReasoning.core.st(173, 2) [modifiesFrameRef1Next]: ✅ pass
-HeapReasoning.core.st(178, 2) [modifiesFrameRef2Next]: ✅ pass
-HeapReasoning.core.st(133, 2) [UpdateContainers_ensures_5]: ✅ pass
- [UpdateContainers_ensures_6]: ✅ pass
-HeapReasoning.core.st(151, 2) [UpdateContainers_ensures_14]: ✅ pass
-HeapReasoning.core.st(152, 2) [UpdateContainers_ensures_15]: ✅ pass
-HeapReasoning.core.st(153, 2) [UpdateContainers_ensures_16]: ✅ pass
-HeapReasoning.core.st(154, 2) [UpdateContainers_ensures_17]: ✅ pass
-HeapReasoning.core.st(156, 2) [UpdateContainers_ensures_18]: ✅ pass
-HeapReasoning.core.st(157, 2) [UpdateContainers_ensures_19]: ✅ pass
-HeapReasoning.core.st(75, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_1]: ✅ pass
-HeapReasoning.core.st(76, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_2]: ✅ pass
-HeapReasoning.core.st(77, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_3]: ✅ pass
-HeapReasoning.core.st(85, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_5]: ✅ pass
-HeapReasoning.core.st(86, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_6]: ✅ pass
-HeapReasoning.core.st(216, 2) [c1Lychees0]: ✅ pass
-HeapReasoning.core.st(217, 2) [c1Pineapple1]: ✅ pass
-HeapReasoning.core.st(75, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_1]: ✅ pass
-HeapReasoning.core.st(76, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_2]: ✅ pass
-HeapReasoning.core.st(77, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_3]: ✅ pass
-HeapReasoning.core.st(85, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_5]: ✅ pass
-HeapReasoning.core.st(86, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_6]: ✅ pass
-HeapReasoning.core.st(227, 2) [assert_9]: ✅ pass
-HeapReasoning.core.st(232, 2) [assert_10]: ✅ pass
-HeapReasoning.core.st(127, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_1]: ✅ pass
-HeapReasoning.core.st(128, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_2]: ✅ pass
-HeapReasoning.core.st(130, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_3]: ✅ pass
-HeapReasoning.core.st(131, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_4]: ✅ pass
-HeapReasoning.core.st(141, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_7]: ✅ pass
-HeapReasoning.core.st(143, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_8]: ✅ pass
-HeapReasoning.core.st(144, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_9]: ✅ pass
-HeapReasoning.core.st(146, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_10]: ✅ pass
-HeapReasoning.core.st(147, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_11]: ✅ pass
-HeapReasoning.core.st(148, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_12]: ✅ pass
-HeapReasoning.core.st(149, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_13]: ✅ pass
-HeapReasoning.core.st(238, 2) [c1Lychees1]: ✅ pass
-HeapReasoning.core.st(239, 2) [c1Pineapple2]: ✅ pass
-HeapReasoning.core.st(240, 2) [c2Lychees0]: ✅ pass
-HeapReasoning.core.st(241, 2) [c2Pineapple0]: ✅ pass
-HeapReasoning.core.st(243, 2) [c1NextEqC2]: ✅ pass
-HeapReasoning.core.st(244, 2) [c2NextEqC1]: ✅ pass
-HeapReasoning.core.st(198, 2) [Main_ensures_2]: ✅ pass
- [Main_ensures_3]: ✅ pass
+HeapReasoning.core.st(99, 2) [modifiesFrameRef1]: ✔️ always true if reached
+HeapReasoning.core.st(104, 2) [modifiesFrameRef1]: ✔️ always true if reached
+HeapReasoning.core.st(109, 2) [modifiesFrameRef1]: ✔️ always true if reached
+ [Container_ctor_ensures_4]: ✔️ always true if reached
+HeapReasoning.core.st(87, 2) [Container_ctor_ensures_7]: ✔️ always true if reached
+HeapReasoning.core.st(88, 2) [Container_ctor_ensures_8]: ✔️ always true if reached
+HeapReasoning.core.st(89, 2) [Container_ctor_ensures_9]: ✔️ always true if reached
+HeapReasoning.core.st(91, 2) [Container_ctor_ensures_10]: ✔️ always true if reached
+HeapReasoning.core.st(165, 2) [modifiesFrameRef1]: ✔️ always true if reached
+HeapReasoning.core.st(170, 2) [modifiesFrameRef2]: ✔️ always true if reached
+HeapReasoning.core.st(173, 2) [modifiesFrameRef1Next]: ✔️ always true if reached
+HeapReasoning.core.st(178, 2) [modifiesFrameRef2Next]: ✔️ always true if reached
+HeapReasoning.core.st(133, 2) [UpdateContainers_ensures_5]: ✔️ always true if reached
+ [UpdateContainers_ensures_6]: ✔️ always true if reached
+HeapReasoning.core.st(151, 2) [UpdateContainers_ensures_14]: ✔️ always true if reached
+HeapReasoning.core.st(152, 2) [UpdateContainers_ensures_15]: ✔️ always true if reached
+HeapReasoning.core.st(153, 2) [UpdateContainers_ensures_16]: ✔️ always true if reached
+HeapReasoning.core.st(154, 2) [UpdateContainers_ensures_17]: ✔️ always true if reached
+HeapReasoning.core.st(156, 2) [UpdateContainers_ensures_18]: ✔️ always true if reached
+HeapReasoning.core.st(157, 2) [UpdateContainers_ensures_19]: ✔️ always true if reached
+HeapReasoning.core.st(75, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_1]: ✔️ always true if reached
+HeapReasoning.core.st(76, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_2]: ✔️ always true if reached
+HeapReasoning.core.st(77, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_3]: ✔️ always true if reached
+HeapReasoning.core.st(85, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_5]: ✔️ always true if reached
+HeapReasoning.core.st(86, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_6]: ✔️ always true if reached
+HeapReasoning.core.st(216, 2) [c1Lychees0]: ✔️ always true if reached
+HeapReasoning.core.st(217, 2) [c1Pineapple1]: ✔️ always true if reached
+HeapReasoning.core.st(75, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_1]: ✔️ always true if reached
+HeapReasoning.core.st(76, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_2]: ✔️ always true if reached
+HeapReasoning.core.st(77, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_3]: ✔️ always true if reached
+HeapReasoning.core.st(85, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_5]: ✔️ always true if reached
+HeapReasoning.core.st(86, 2) [(Origin_Container_ctor_Requires)Container_ctor_requires_6]: ✔️ always true if reached
+HeapReasoning.core.st(227, 2) [assert_9]: ✔️ always true if reached
+HeapReasoning.core.st(232, 2) [assert_10]: ✔️ always true if reached
+HeapReasoning.core.st(127, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_1]: ✔️ always true if reached
+HeapReasoning.core.st(128, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_2]: ✔️ always true if reached
+HeapReasoning.core.st(130, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_3]: ✔️ always true if reached
+HeapReasoning.core.st(131, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_4]: ✔️ always true if reached
+HeapReasoning.core.st(141, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_7]: ✔️ always true if reached
+HeapReasoning.core.st(143, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_8]: ✔️ always true if reached
+HeapReasoning.core.st(144, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_9]: ✔️ always true if reached
+HeapReasoning.core.st(146, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_10]: ✔️ always true if reached
+HeapReasoning.core.st(147, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_11]: ✔️ always true if reached
+HeapReasoning.core.st(148, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_12]: ✔️ always true if reached
+HeapReasoning.core.st(149, 2) [(Origin_UpdateContainers_Requires)UpdateContainers_requires_13]: ✔️ always true if reached
+HeapReasoning.core.st(238, 2) [c1Lychees1]: ✔️ always true if reached
+HeapReasoning.core.st(239, 2) [c1Pineapple2]: ✔️ always true if reached
+HeapReasoning.core.st(240, 2) [c2Lychees0]: ✔️ always true if reached
+HeapReasoning.core.st(241, 2) [c2Pineapple0]: ✔️ always true if reached
+HeapReasoning.core.st(243, 2) [c1NextEqC2]: ✔️ always true if reached
+HeapReasoning.core.st(244, 2) [c2NextEqC1]: ✔️ always true if reached
+HeapReasoning.core.st(198, 2) [Main_ensures_2]: ✔️ always true if reached
+ [Main_ensures_3]: ✔️ always true if reached
 All 53 goals passed.

Examples/expected/LoopSimple.core.expected

@@ -1,8 +1,8 @@
 Successfully parsed.
-LoopSimple.core.st(13, 2) [entry_invariant_0_0]: ✅ pass
-LoopSimple.core.st(13, 2) [entry_invariant_0_1]: ✅ pass
-LoopSimple.core.st(13, 2) [arbitrary_iter_maintain_invariant_0_0]: ✅ pass
-LoopSimple.core.st(13, 2) [arbitrary_iter_maintain_invariant_0_1]: ✅ pass
-LoopSimple.core.st(20, 2) [sum_assert]: ✅ pass
-LoopSimple.core.st(21, 2) [neg_cond]: ✅ pass
+LoopSimple.core.st(13, 2) [entry_invariant_0_0]: ✔️ always true if reached
+LoopSimple.core.st(13, 2) [entry_invariant_0_1]: ✔️ always true if reached
+LoopSimple.core.st(13, 2) [arbitrary_iter_maintain_invariant_0_0]: ✔️ always true if reached
+LoopSimple.core.st(13, 2) [arbitrary_iter_maintain_invariant_0_1]: ✔️ always true if reached
+LoopSimple.core.st(20, 2) [sum_assert]: ✔️ always true if reached
+LoopSimple.core.st(21, 2) [neg_cond]: ✔️ always true if reached
 All 6 goals passed.

Examples/expected/LoopSimple.csimp.expected

@@ -1,10 +1,10 @@
 Successfully parsed.
- [entry_invariant_0]: ✅ pass
- [assert_measure_pos]: ✅ pass
- [measure_decreases]: ✅ pass
- [measure_imp_not_guard]: ✅ pass
- [arbitrary_iter_maintain_invariant_0]: ✅ pass
- [sum_assert]: ✅ pass
- [neg_cond]: ✅ pass
- [post]: ✅ pass
+ [entry_invariant_0]: ✔️ always true if reached
+ [assert_measure_pos]: ✔️ always true if reached
+ [measure_decreases]: ✔️ always true if reached
+ [measure_imp_not_guard]: ✔️ always true if reached
+ [arbitrary_iter_maintain_invariant_0]: ✔️ always true if reached
+ [sum_assert]: ✔️ always true if reached
+ [neg_cond]: ✔️ always true if reached
+ [post]: ✔️ always true if reached
 All 8 goals passed.

Examples/expected/SimpleProc.core.expected

@@ -1,5 +1,5 @@
 Successfully parsed.
-SimpleProc.core.st(22, 2) [Test_ensures_0]: ✅ pass
-SimpleProc.core.st(23, 2) [Test_ensures_1]: ✅ pass
-SimpleProc.core.st(24, 2) [Test_ensures_2]: ✅ pass
+SimpleProc.core.st(22, 2) [Test_ensures_0]: ✔️ always true if reached
+SimpleProc.core.st(23, 2) [Test_ensures_1]: ✔️ always true if reached
+SimpleProc.core.st(24, 2) [Test_ensures_2]: ✔️ always true if reached
 All 3 goals passed.

Examples/expected/TwoLoops.core.expected

@@ -1,6 +1,6 @@
 Successfully parsed.
-TwoLoops.core.st(12, 2) [entry_invariant_0_0]: ✅ pass
-TwoLoops.core.st(12, 2) [arbitrary_iter_maintain_invariant_0_0]: ✅ pass
-TwoLoops.core.st(19, 2) [entry_invariant_1_0]: ✅ pass
-TwoLoops.core.st(19, 2) [arbitrary_iter_maintain_invariant_1_0]: ✅ pass
+TwoLoops.core.st(12, 2) [entry_invariant_0_0]: ✔️ always true if reached
+TwoLoops.core.st(12, 2) [arbitrary_iter_maintain_invariant_0_0]: ✔️ always true if reached
+TwoLoops.core.st(19, 2) [entry_invariant_1_0]: ✔️ always true if reached
+TwoLoops.core.st(19, 2) [arbitrary_iter_maintain_invariant_1_0]: ✔️ always true if reached
 All 4 goals passed.

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