while loops with multiple invariants (#382)

This PR adds support for multiple loop invariants in while statements.
The parser and translation phase are extended to accept multiple
invariant clauses and translate them into a list, while keeping the Core
backend and invariant semantics unchanged.

The example `LoopSimple.core.st` has been adapted to demonstrate the
change.

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution under the terms of your choice.

---------

Co-authored-by: Shilpi Goel <shigoel@gmail.com>
Co-authored-by: Josh Cohen <cohenjo@amazon.com>

Author: 3 people

Examples/LoopSimple.core.st

@@ -11,7 +11,8 @@ spec {
   sum := 0;
   i := 0;
   while(i < n)
-    invariant (i <= n && ((i * (i-1)) div 2 == sum));
+    invariant i <= n
+    invariant ((i * (i-1)) div 2 == sum)
   {
     sum := sum + i;
     i := i + 1;

Examples/expected/LoopSimple.core.expected

@@ -1,6 +1,6 @@
 Successfully parsed.
 LoopSimple.core.st(13, 2) [entry_invariant_0]: ✅ pass
 LoopSimple.core.st(13, 2) [arbitrary_iter_maintain_invariant_0]: ✅ pass
-LoopSimple.core.st(19, 2) [sum_assert]: ✅ pass
-LoopSimple.core.st(20, 2) [neg_cond]: ✅ pass
+LoopSimple.core.st(20, 2) [sum_assert]: ✅ pass
+LoopSimple.core.st(21, 2) [neg_cond]: ✅ pass
 All 4 goals passed.

Strata/Languages/Core/DDMTransform/Parse.lean

@@ -203,8 +203,13 @@ op havoc_statement (v : Ident) : Statement => "havoc " v ";\n";
 category Invariant;
 op invariant (e : Expr) : Invariant => "invariant" e ";";
 
-op while_statement (c : bool, i : Option Invariant, body : Block) : Statement =>
-  "while" "(" c ")" i body;
+category Invariants;
+op nilInvariants : Invariants => ;
+op consInvariants(e : Expr, is : Invariants) : Invariants =>
+  "invariant" e is;
+
+op while_statement (c : bool, is : Invariants, body : Block) : Statement =>
+  "while" "(" c ")" is body;
 
 op call_statement (vs : CommaSepBy Ident, f : Ident, expr : CommaSepBy Expr) : Statement =>
    "call" vs ":=" f "(" expr ")" ";\n";

Strata/Languages/Core/DDMTransform/Translate.lean

@@ -918,6 +918,29 @@ def translateInvariant (p : Program) (bindings : TransBindings) (arg : Arg) : Tr
     translateExpr p bindings args[0]!
   | _ => pure none
 
+partial def translateInvariants (p : Strata.Program) (bindings : TransBindings) (arg : Arg) :
+  TransM (List Expression.Expr) := do
+  let .op op := arg
+    | TransM.error s!"translateInvariants expects an op {repr arg}"
+  match op.name with
+  | q`Core.nilInvariants =>
+    pure []
+  | q`Core.consInvariants =>
+    let args ← checkOpArg arg q`Core.consInvariants 2
+    let i ← translateExpr p bindings args[0]!
+    let is ← translateInvariants p bindings args[1]!
+    pure (i::is)
+  | _ => TransM.error s!"translateInvariants unimplemented for {repr op}"
+
+private def invariantsToOption (invs : List Core.Expression.Expr) : Option Core.Expression.Expr :=
+  match invs with
+  | [] => none
+  | i :: is =>
+    -- ((i ∧ i2) ∧ i3) ∧ ...
+    some <| is.foldl
+      (fun acc j => .app () (.app () Core.boolAndOp acc) j)
+      i
+
 def initVarStmts (tpids : ListMap Expression.Ident LTy) (bindings : TransBindings) :
   TransM ((List Core.Statement) × TransBindings) := do
   match tpids with
@@ -1005,10 +1028,11 @@ partial def translateStmt (p : Program) (bindings : TransBindings) (arg : Arg) :
     return ([.ite c tss fss md], bindings)
   | q`Core.while_statement, #[ca, ia, ba] =>
     let c ← translateExpr p bindings ca
-    let i ← translateInvariant p bindings ia
+    let invs ← translateInvariants p bindings ia
+    let inv? := invariantsToOption invs
     let (bodyss, bindings) ← translateBlock p bindings ba
     let md ← getOpMetaData op
-    return ([.loop c .none i bodyss md], bindings)
+    return ([.loop c .none inv? bodyss md], bindings)
   | q`Core.call_statement, #[lsa, fa, esa] =>
     let ls  ← translateCommaSep (translateIdent CoreIdent) lsa
     let f   ← translateIdent String fa

StrataTest/Languages/Core/Examples/Loops.lean

@@ -23,9 +23,9 @@ spec {
   i := 0;
   s := 0;
   while (i < n)
-    invariant 0 <= i &&
-              i <= n &&
-              s == (i * (i + 1)) div 2;
+    invariant 0 <= i
+    invariant i <= n
+    invariant s == (i * (i + 1)) div 2
   {
     i := (i + 1);
     s := (s + i);
@@ -99,11 +99,14 @@ spec {
   var y: int;
   x := 0;
   while (x < n)
-    invariant x >= 0 && x <= n && n < top;
+    invariant x >= 0
+    invariant x <= n
+    invariant n < top
   {
     y := 0;
     while (y < x)
-      invariant y >= 0 && y <= x;
+      invariant y >= 0
+      invariant y <= x
     {
       y := y + 1;
     }

Tools/BoogieToStrata/Source/StrataGenerator.cs

@@ -927,12 +927,10 @@ private void EmitWhileCmd(WhileCmd whileCmd) {
         }
 
         WriteLine(")");
-        if (whileCmd.Invariants.Count != 0) {
-            IncIndent();
-            Indent("invariant");
-            EmitSeparated(whileCmd.Invariants, i => VisitExpr(i.Expr), " && ");
-            WriteLine(";");
-            DecIndent();
+        foreach (var inv in whileCmd.Invariants) {
+            Indent("invariant ");
+            VisitExpr(inv.Expr);
+            WriteLine("");
         }
         IndentLine("{");
         IncIndent();

Tools/BoogieToStrata/Tests/Bubble.expect

@@ -1,14 +1,14 @@
 Successfully parsed.
 Bubble.core.st(31, 4) [entry_invariant_0]: ✅ pass
 Bubble.core.st(31, 4) [arbitrary_iter_maintain_invariant_0]: ✅ pass
-Bubble.core.st(43, 4) [entry_invariant_0]: ✅ pass
+Bubble.core.st(44, 4) [entry_invariant_0]: ✅ pass
 Bubble.core.st(20, 2) [BubbleSort_ensures_1]: ✅ pass
 Bubble.core.st(21, 2) [BubbleSort_ensures_2]: ✅ pass
 Bubble.core.st(22, 2) [BubbleSort_ensures_3]: ✅ pass
 Bubble.core.st(23, 2) [BubbleSort_ensures_4]: ✅ pass
-Bubble.core.st(57, 8) [entry_invariant_1]: ✅ pass
-Bubble.core.st(57, 8) [arbitrary_iter_maintain_invariant_1]: ✅ pass
-Bubble.core.st(43, 4) [arbitrary_iter_maintain_invariant_0]: ✅ pass
+Bubble.core.st(62, 8) [entry_invariant_1]: ✅ pass
+Bubble.core.st(62, 8) [arbitrary_iter_maintain_invariant_1]: ✅ pass
+Bubble.core.st(44, 4) [arbitrary_iter_maintain_invariant_0]: ✅ pass
 Bubble.core.st(20, 2) [BubbleSort_ensures_1]: ✅ pass
 Bubble.core.st(21, 2) [BubbleSort_ensures_2]: ✅ pass
 Bubble.core.st(22, 2) [BubbleSort_ensures_3]: ✅ pass