Implement support for triggers with lean-auto (#942)

Updates lean-auto dependency to get this functionality, and Lean itself
along the way. Improve some messages, too.

Source/Provers/LeanAuto/LeanAutoGenerator.cs

@@ -10,7 +10,7 @@ internal class LeanConversionException : Exception
   public string Msg { get; }
   public LeanConversionException(IToken tok, string s)
   {
-    Msg = tok + ": " + s;
+    Msg = $"{tok.filename}({tok.line},{tok.col}): {s}";
   }
 }
 
@@ -325,7 +325,14 @@ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
       VisitTypedIdent(x.TypedIdent);
     }
     WriteText(", ");
+    var triggers = node?.Triggers?.Tr ?? new List<Expr>();
+    foreach (var trigger in triggers) {
+      WriteText("(trigger (");
+      VisitExpr(trigger);
+      WriteText(") ");
+    }
     Visit(node.Body);
+    triggers.ForEach(_ => WriteText(")"));
     WriteText(")");
 
     return node;
@@ -450,10 +457,10 @@ public override Expr VisitNAryExpr(NAryExpr node)
       Visit(args[1]);
     } else if (fun is FieldAccess fieldAccess) {
       throw new LeanConversionException(node.tok,
-        "Unsupported: field access (since the semantics are complex)");
+        $"Unsupported: field access (field = {fieldAccess.FieldName}) (since the semantics are complex)");
     } else if (fun is FieldUpdate fieldUpdate) {
       throw new LeanConversionException(node.tok,
-        "Unsupported: field update (since the semantics are complex)");
+        $"Unsupported: field update (field = {fieldUpdate.FieldAccess.FieldName}) (since the semantics are complex)");
     } else if (fun is IfThenElse && args.Count == 3) {
       WriteText("if ");
       Visit(args[0]);

Source/Provers/LeanAuto/Prelude.lean

@@ -1,7 +1,8 @@
 import Auto
 import Auto.Tactic
 import Auto.MathlibEmulator.Basic -- For `Real`
-open Lean Std Auto
+import Auto.Translation.SMTAttributes
+open Lean Std Auto Auto.SMT.Attribute
 
 set_option linter.unusedVariables false
 set_option auto.smt true

Test/lean-auto/Triggers0Valid.bpl

@@ -0,0 +1,47 @@
+// RUN: %parallel-boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
+// RUN: %parallel-boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
+
+const ar : [int]bool;
+axiom {:include_dep} (forall x:int :: {ar[x]} !ar[x]);
+
+type S, T, C a b;
+
+function m(T,S) returns (bool);
+function n(T,T) returns (bool) uses {
+  axiom (forall x:S, y:T :: l(x) && n(y, con) == m(y,x));
+}
+
+function f<a>(C a T, a) returns (int);
+function f2<a>(C a T, a) returns (int) uses {
+  axiom (forall x:C S T, y : S :: f(x,y) == f2(x,y));
+}
+
+function g(T) returns (T) uses {
+  axiom (forall x:T :: {g(h(x))} {g(x)} x == x);
+}
+
+function h<a>(a) returns (a) uses {
+  axiom (forall <b> x:b :: {h(x)} x == x);
+}
+
+function k<a>(C a a) returns (bool) uses {
+  axiom (forall <b> x:C b b :: k(x));
+  axiom (forall <b> x:C b b :: {k(x)} k(x));
+}
+
+function l<a>(a) returns (bool);
+function o<a>(a) returns (bool) uses {
+  axiom (forall <b> x:b, y:b :: {o(x), o(y)} o(x) ==> someConst == 42);
+}
+
+const con : T;
+const someConst : int;
+
+procedure P() returns () {
+  var v0 : C S S, v1 : C S T, v2 : S, v3 : T;
+
+  assert ar[27] == false;
+  assert k(v0);
+  assert f(v1, v2) == f2(v1, v2);
+  assert n(v3, con) == m(v3, v2);
+}

Test/lean-auto/lakefile.lean

@@ -6,7 +6,7 @@ package «test» {
 }
 
 require auto from git
-  "https://github.com/leanprover-community/lean-auto"@"v0.0.6"
+  "https://github.com/leanprover-community/lean-auto"@"0831a6eff8cbb456e90c616bd2f4db51aefea3d0"
 
 @[default_target]
 lean_lib «ToBuild» {

Test/lean-auto/lean-tests

@@ -4,3 +4,4 @@
 ../textbook/DivMod.bpl
 ../textbook/Find.bpl
 ../textbook/McCarthy-91.bpl
+./Triggers0Valid.bpl

Test/lean-auto/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:v4.9.0

Test/lean-auto/test.sh

@@ -5,5 +5,5 @@ set -e
 boogie_file=$1
 base=`basename $boogie_file .bpl`
 lean_file="$base.lean"
-dotnet ../../Source/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll /printLean:$lean_file $boogie_file
+dotnet ../../Source/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll /prune:1 /printLean:$lean_file $boogie_file
 lake env lean $lean_file

Test/textbook/Bubble.bpl

@@ -4,8 +4,9 @@
 // the input.
 
 // Introduce a constant 'N' and postulate that it is non-negative
-const N: int;
-axiom 0 <= N;
+const N: int uses {
+  axiom 0 <= N;
+}
 
 // Declare a map from integers to integers.  In the procedure below, 'a' will be
 // treated as an array of 'N' elements, indexed from 0 to less than 'N'.

Test/textbook/DivMod.bpl

@@ -12,16 +12,16 @@ function abs(x: int): int { if 0 <= x then x else -x }
 function divt(int, int): int;
 function modt(int, int): int;
 
-axiom (forall a,b: int :: divt(a,b)*b + modt(a,b) == a);
-axiom (forall a,b: int ::
+axiom {:include_dep} (forall a,b: int :: divt(a,b)*b + modt(a,b) == a);
+axiom {:include_dep} (forall a,b: int ::
   (0 <= a ==> 0 <= modt(a,b) && modt(a,b) < abs(b)) &&
   (a < 0 ==> -abs(b) < modt(a,b) && modt(a,b) <= 0));
 
 function dive(int, int): int;
 function mode(int, int): int;
 
-axiom (forall a,b: int :: dive(a,b)*b + mode(a,b) == a);
-axiom (forall a,b: int :: 0 <= mode(a,b) && mode(a,b) < abs(b));
+axiom {:include_dep} (forall a,b: int :: dive(a,b)*b + mode(a,b) == a);
+axiom {:include_dep} (forall a,b: int :: 0 <= mode(a,b) && mode(a,b) < abs(b));
 
 procedure T_from_E(a,b: int) returns (q,r: int)
   requires b != 0;

Test/textbook/TuringFactorial.bpl

@@ -28,9 +28,11 @@ INNER:  // E
   goto TOP;
 }
 
-function Factorial(int): int;
-axiom Factorial(0) == 1;
-axiom (forall n: int :: {Factorial(n)}  1 <= n ==> Factorial(n) == n * Factorial_Aux(n-1));
+function Factorial(int): int uses {
+  axiom Factorial(0) == 1;
+  axiom (forall n: int :: {Factorial(n)}  1 <= n ==> Factorial(n) == n * Factorial_Aux(n-1));
+}
 
-function Factorial_Aux(int): int;
-axiom (forall n: int :: {Factorial(n)} Factorial(n) == Factorial_Aux(n));
+function Factorial_Aux(int): int uses {
+  axiom (forall n: int :: {Factorial(n)} Factorial(n) == Factorial_Aux(n));
+}