Better errors/warning messages for Loom (#23)

* add dummy measure to model omitted decreasing clause

* better errors/warning for decreasing clause

* require at least one invariant

* fix chashmere

* add test suite for new error/warning messages

* Refactor invariant handling in Loom: rename 'invariants' to 'invariantSeq' for consistency and clarity across multiple files.

* Make invariantGadget infer MAlg instance to determine the type of assertion language

* Add option to off warnings and errors relted to decreasing clause

* add warning for empty invariant clauses

* Add options to control warnings and errors for Loom program annotations

* fix velvet case studies

Author: volodeyka

CaseStudies/Cashmere/Syntax_Cashmere.lean

@@ -247,6 +247,7 @@ macro_rules
           for _ in Lean.Loop.mk do
             invariantGadget [ $[$inv:term],* ]
             onDoneGadget ($invd_some:term)
+            decreasingGadget none
             if $t then
               $seq:doSeq
             else break)

CaseStudies/Macro.lean

@@ -10,20 +10,55 @@ open Lean Elab Command
 
 macro "assert" t:term : term => `(assertGadget $t)
 
-macro "decreasing" t:term : term => `(decreasingGadget $t)
+/--
+Elaboration rule for the `decreasing` annotation. Here we will
+  - Throw an error if the termination semantics is unspecified.
+  - Throw an error if the decreasing annotation is missing in total correctness semantics.
+  - Throw a warning if the decreasing annotation is present in partial correctness semantics.
+-/
+elab "decreasing" t:term : term => do
+  let opts <- getOptions
+  let semantics := opts.getString (defVal := "unspecified") `loom.semantics.termination
+  if semantics = "unspecified" then
+    throwError "First, you need to specify the termination semantics using `set_option loom.semantics.termination <partial/total>`"
+  let decr <- `(decreasingGadget $t)
+  let decrIsNone := match t with
+    | `(none) => true
+    | _ => false
+  let errorsEnabled := opts.getBool (defVal := true) `loom.linter.errors
+  let warningsEnabled := opts.getBool (defVal := true) `loom.linter.warnings
+  if semantics = "total" && decrIsNone && errorsEnabled then
+    throwError "Decreasing annotations are required in total correctness semantics
+To turn off this error, use `set_option loom.linter.errors false`."
+  if semantics = "partial" && !decrIsNone && warningsEnabled then
+    logWarningAt (<- getRef) "Decreasing annotations are not checked in partial correctness semantics
+To turn off this warning, use `set_option loom.linter.warnings false`."
+  Term.elabTerm decr none
+
+elab "invariants" invs:term : term => do
+  let opts <- getOptions
+  let invsIsEmpty := match invs with
+    | `([]) => true
+    | _ => false
+  let warningsEnabled := opts.getBool (defVal := true) `loom.linter.warnings
+  if invsIsEmpty && warningsEnabled then
+    logWarningAt (<- getRef) "Invariant annotations are not specified, so the loop invariant is assumed to be just `True`.
+To turn off this warning, use `set_option loom.linter.warnings false`."
+  Term.elabTerm (<- `(invariantGadget $invs:term)) none
+
 
 declare_syntax_cat doneWith
 declare_syntax_cat decreasingTerm
 declare_syntax_cat invariantClause
-declare_syntax_cat invariants
+declare_syntax_cat invariantClauses
 syntax "invariant" termBeforeDo linebreak : invariantClause
 syntax "done_with" termBeforeDo : doneWith
 syntax "decreasing" termBeforeDo : decreasingTerm
-syntax (invariantClause linebreak)* : invariants
+syntax (invariantClause linebreak)* : invariantClauses
 
 syntax "let" term ":|" term : doElem
 syntax "while" term
-  (invariantClause)+
+  (invariantClause)*
   (doneWith)?
   (decreasingTerm)?
   "do" doSeq : doElem
@@ -39,32 +74,76 @@ syntax "for" ident "in" termBeforeInvariant
 macro_rules
   | `(doElem| let $x:term :| $t) => `(doElem| let $x:term <- pickSuchThat _ (fun $x => $t))
 
+/-
+### While loop elaboration rules
+
+The general syntax for a while loop is:
+```lean
+while <condition>
+  [invariant <invariant1>]
+  [invariant <invariant2>]
+  ...
+  [done_with <termination_condition>]?
+  [decreasing <measure>]?
+do <body>
+```
+Unlike ordinary Lean's `while` loop, `Velvet` loops require at least one
+invariant annotation. Invariant annotations are followed by an optional `done_with` statement.
+In a nutshell, `done_with` is a condition that is true upon loop termination. Such condition is
+usefull to specify when the loop contains `break` or `continue` statements. Which means that loop
+might terminate without reaching the stated where the loop condition is false.
+If unspecified, it is assumed to be the negation of the loop condition.
+
+The optional `decreasing` annotation is used to specify a measure function that is used to prove termination.
+This measure elaborates to a term of type `β → Option ℕ` where `β` is a record of the loop variables. We need
+`Option ℕ` to incorporate the cases when the measure is not specified, which should be the case for partial
+correctness semantics.
+If `decreasing` is unspecified, measure is assumed to be `none`.
+-/
 macro_rules
+  | `(doElem| while $t do $seq:doSeq) => do
+    let decr <- withRef (<- getRef) `(decreasing none)
+    let invs <- withRef (<- getRef) `(invariants [])
+    `(doElem|
+      for _ in Lean.Loop.mk do
+        $invs:term
+        onDoneGadget (with_name_prefix `done ¬$t:term)
+        $decr:term
+        if $t then
+          $seq:doSeq
+        else break)
   | `(doElem| while $t
               $[invariant $inv:term
               ]*
               $[done_with $inv_done]?
               $[decreasing $measure]?
               do $seq:doSeq) => do
+      let invs <- `(invariants [ $[(with_name_prefix `invariant $inv:term)],* ])
       let invd_some ← match inv_done with
       | some invd_some => withRef invd_some ``($invd_some)
       | none => ``(¬$t:term)
       match measure with
-      | some measure_some => `(doElem|
-        for _ in Lean.Loop.mk do
-          invariantGadget [ $[(with_name_prefix `invariant $inv:term)],* ]
-          onDoneGadget (with_name_prefix `done $invd_some:term)
-          decreasingGadget (type_with_name_prefix `decreasing $measure_some:term)
-          if $t then
-            $seq:doSeq
-          else break)
-      | none => `(doElem|
-        for _ in Lean.Loop.mk do
-          invariantGadget [ $[(with_name_prefix `invariant $inv:term)],* ]
-          onDoneGadget (with_name_prefix `done $invd_some:term)
-          if $t then
-            $seq:doSeq
-          else break)
+      | some measure_some =>
+        let decr <- withRef measure_some `(decreasing type_with_name_prefix `decreasing $measure_some)
+        `(doElem|
+          for _ in Lean.Loop.mk do
+            $invs:term
+            onDoneGadget (with_name_prefix `done $invd_some:term)
+            $decr:term
+            if $t then
+              $seq:doSeq
+            else break)
+      | none => do
+        let decr <- withRef (<- getRef) `(decreasing none)
+        let invs <- `(invariants [ $[(with_name_prefix `invariant $inv:term)],* ])
+        `(doElem|
+          for _ in Lean.Loop.mk do
+            $invs:term
+            onDoneGadget (with_name_prefix `done $invd_some:term)
+            $decr:term
+            if $t then
+              $seq:doSeq
+            else break)
   | `(doElem| while_some $x:ident :| $t do $seq:doSeq) =>
     match seq with
     | `(doSeq| $[$seq:doElem]*)
@@ -80,34 +159,36 @@ macro_rules
               ]*
               $[done_with $inv_done]? do
                 $seq:doSeq) => do
+    let invs <- `(invariants [ $[(with_name_prefix `invariant $inv:term)],* ])
     let invd_some ← match inv_done with
     | some invd_some => withRef invd_some ``($invd_some)
     | none => ``(¬$t:term)
     match seq with
     | `(doSeq| $[$seq:doElem]*)
     | `(doSeq| $[$seq:doElem;]*)
     | `(doSeq| { $[$seq:doElem]* }) =>
+      let decr <- withRef (<- getRef) `(decreasing none)
       `(doElem|
         for _ in Lean.Loop.mk do
-          invariantGadget [ $[(with_name_prefix `invariant $inv:term)],* ]
+          $invs:term
           onDoneGadget (with_name_prefix `done $invd_some:term)
+          $decr:term
           if ∃ $x:ident, $t then
             let $x :| $t
             $[$seq:doElem]*
           else break)
     | _ => Lean.Macro.throwError "while_some expects a sequence of do-elements"
   | `(doElem| for $x:ident in $t
-            invariant $inv':term
             $[invariant $inv:term
             ]*
-            do $seq:doSeq) =>
+            do $seq:doSeq) => do
+      let invs <- `(invariants [ $[(with_name_prefix `invariant $inv:term)],* ])
       match seq with
       | `(doSeq| $[$seq:doElem]*)
       | `(doSeq| $[$seq:doElem;]*)
       | `(doSeq| { $[$seq:doElem]* }) =>
-        -- let inv := invs.push inv
         `(doElem|
           for $x:ident in $t do
-            invariantGadget [ $inv':term, $[$inv:term],* ]
+            $invs:term
             $[$seq:doElem]*)
       | _ => Lean.Macro.throwError "for expects a sequence of do-elements"

CaseStudies/Tactic.lean

@@ -73,7 +73,7 @@ elab_rules : tactic
       wpgen
       try simp only [loomWpSimp]
       try unfold spec
-      try simp only [invariants]
+      try simp only [invariantSeq]
       try simp only [WithName.mk']
       try simp only [WithName.erase]
       try simp only [typeWithName.erase]
@@ -151,17 +151,17 @@ elab "loom_solve?" : tactic => withMainContext do
   try simp only [$(mkIdent `loomAbstractionSimp):ident] at *
   wpgen
   try simp only [$(mkIdent `loomWpSimp):ident]
-  try simp only [$(mkIdent `WithName):ident]
-  try simp only [$(mkIdent `typeWithName):ident]
+  try simp only [$(mkIdent ``WithName):ident]
+  try simp only [$(mkIdent ``typeWithName):ident]
   try unfold spec
-  try simp only [$(mkIdent `invariants):ident]
-  try simp only [$(mkIdent `WithName.mk'):ident]
-  try simp only [$(mkIdent `WithName.erase):ident]
-  try simp only [$(mkIdent `typeWithName.erase):ident]
-  try simp only [$(mkIdent `List.foldr):ident]
+  try simp only [$(mkIdent ``invariantSeq):ident]
+  try simp only [$(mkIdent ``WithName.mk'):ident]
+  try simp only [$(mkIdent ``WithName.erase):ident]
+  try simp only [$(mkIdent ``typeWithName.erase):ident]
+  try simp only [$(mkIdent ``List.foldr):ident]
   try simp only [$(mkIdent `loomLogicSimp):ident]
   try simp only [$(mkIdent `simpMAlg):ident]
-  repeat' (apply $(mkIdent `And.intro) <;> (repeat loom_intro))
+  repeat' (apply $(mkIdent ``And.intro) <;> (repeat loom_intro))
   any_goals auto [$hints,*]
   ))
   Tactic.TryThis.addSuggestion (<-getRef) tac

CaseStudies/Velvet/VelvetExamples/TestSyntaxErrors.lean

@@ -0,0 +1,80 @@
+import Auto
+import Lean
+
+import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Algebra.Ring.Int.Defs
+
+import Loom.MonadAlgebras.NonDetT.Extract
+import Loom.MonadAlgebras.WP.Tactic
+import Loom.MonadAlgebras.WP.DoNames'
+
+import CaseStudies.Velvet.Std
+
+section
+
+set_option loom.semantics.termination "partial"
+set_option loom.semantics.choice "demonic"
+
+/--
+warning: Invariant annotations are not specified, so the loop invariant is assumed to be just `True`.
+To turn off this warning, use `set_option loom.linter.warnings false`.
+-/
+#guard_msgs in
+method zero_invariant (mut n : Nat) return (res : Nat) do
+  while n > 0 do
+    n := n - 1
+  return n
+
+end
+
+section
+set_option loom.semantics.termination "partial"
+set_option loom.semantics.choice "demonic"
+
+/--
+warning: Decreasing annotations are not checked in partial correctness semantics
+To turn off this warning, use `set_option loom.linter.warnings false`.
+-/
+#guard_msgs in
+method redundant_decreasing (mut n : Nat) return (res : Nat) do
+  while n > 0
+    invariant n >= 0
+    decreasing n
+  do
+    n := n - 1
+  return n
+
+end
+
+section
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
+
+/--
+error: Decreasing annotations are required in total correctness semantics
+To turn off this error, use `set_option loom.linter.errors false`.
+-/
+#guard_msgs in
+method missing_decreasing (mut n : Nat) return (res : Nat) do
+  while n > 0
+    invariant n >= 0
+    done_with n = 0
+  do
+    n := n - 1
+  return n
+
+end
+
+section
+set_option loom.semantics.termination "partial"
+set_option loom.semantics.choice "demonic"
+
+set_option loom.linter.errors false
+set_option loom.linter.warnings false
+
+#guard_msgs in
+method no_msg (mut n : Nat) return (res : Nat) do
+  while n > 0 do
+    n := n - 1
+  return n
+end

CaseStudies/Velvet/VelvetExamples/Total_Partial_example.lean

@@ -95,6 +95,10 @@ end
 set_option loom.semantics.termination "total"
 set_option loom.semantics.choice "demonic"
 
+set_option loom.linter.errors false
+set_option loom.linter.warnings false
+
+
 method insertionSort_result
   (mut arr: Array Int) return (u: Unit)
   ensures forall i j, 0 ≤ i ∧ i ≤ j ∧ j < arr.size → arr[i]! ≤ arr[j]!
@@ -107,13 +111,9 @@ method insertionSort_result
       return
     else
       let mut n := 1
-      while n ≠ arr.size
-      invariant True
-      do
+      while n ≠ arr.size do
         let mut mind := n
-        while mind ≠ 0
-        invariant True
-        do
+        while mind ≠ 0 do
           if arr[mind]! < arr[mind - 1]! then
             swap! arr[mind]! arr[mind - 1]!
           mind := mind - 1