From e7a229e912c8a79ddbd1fe9a47f6270711693716 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 19 Aug 2024 02:41:10 -0700 Subject: [PATCH] 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 | 13 ++++-- Source/Provers/LeanAuto/Prelude.lean | 3 +- Test/lean-auto/Triggers0Valid.bpl | 47 ++++++++++++++++++++ Test/lean-auto/lakefile.lean | 2 +- Test/lean-auto/lean-tests | 1 + Test/lean-auto/lean-toolchain | 2 +- Test/lean-auto/test.sh | 2 +- Test/textbook/Bubble.bpl | 5 ++- Test/textbook/DivMod.bpl | 8 ++-- Test/textbook/TuringFactorial.bpl | 12 ++--- 10 files changed, 77 insertions(+), 18 deletions(-) create mode 100644 Test/lean-auto/Triggers0Valid.bpl diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs index e3a5310b4..7bd3c533f 100644 --- a/Source/Provers/LeanAuto/LeanAutoGenerator.cs +++ b/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(); + 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]); diff --git a/Source/Provers/LeanAuto/Prelude.lean b/Source/Provers/LeanAuto/Prelude.lean index 3bda453b3..038702266 100644 --- a/Source/Provers/LeanAuto/Prelude.lean +++ b/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 diff --git a/Test/lean-auto/Triggers0Valid.bpl b/Test/lean-auto/Triggers0Valid.bpl new file mode 100644 index 000000000..ad40c3b75 --- /dev/null +++ b/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(C a T, a) returns (int); +function f2(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) returns (a) uses { + axiom (forall x:b :: {h(x)} x == x); +} + +function k(C a a) returns (bool) uses { + axiom (forall x:C b b :: k(x)); + axiom (forall x:C b b :: {k(x)} k(x)); +} + +function l(a) returns (bool); +function o(a) returns (bool) uses { + axiom (forall 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); +} diff --git a/Test/lean-auto/lakefile.lean b/Test/lean-auto/lakefile.lean index 6bc2f376f..8d422d5e3 100644 --- a/Test/lean-auto/lakefile.lean +++ b/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» { diff --git a/Test/lean-auto/lean-tests b/Test/lean-auto/lean-tests index 549901577..516c1604a 100644 --- a/Test/lean-auto/lean-tests +++ b/Test/lean-auto/lean-tests @@ -4,3 +4,4 @@ ../textbook/DivMod.bpl ../textbook/Find.bpl ../textbook/McCarthy-91.bpl +./Triggers0Valid.bpl diff --git a/Test/lean-auto/lean-toolchain b/Test/lean-auto/lean-toolchain index cfcdd3277..4ef27c472 100644 --- a/Test/lean-auto/lean-toolchain +++ b/Test/lean-auto/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.6.0-rc1 +leanprover/lean4:v4.9.0 diff --git a/Test/lean-auto/test.sh b/Test/lean-auto/test.sh index 66fe08eac..bb47d1942 100755 --- a/Test/lean-auto/test.sh +++ b/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 diff --git a/Test/textbook/Bubble.bpl b/Test/textbook/Bubble.bpl index ac3453941..55e31111e 100644 --- a/Test/textbook/Bubble.bpl +++ b/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'. diff --git a/Test/textbook/DivMod.bpl b/Test/textbook/DivMod.bpl index fb18a7ef7..dcd72da27 100644 --- a/Test/textbook/DivMod.bpl +++ b/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; diff --git a/Test/textbook/TuringFactorial.bpl b/Test/textbook/TuringFactorial.bpl index b5f1b3037..07a042874 100644 --- a/Test/textbook/TuringFactorial.bpl +++ b/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)); +}