From bf36ddfed5d85b73341359d848d96af062fe5dd9 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 12 Dec 2023 17:10:12 -0800 Subject: [PATCH 01/30] Translator sufficient for Bubble.bpl to typecheck --- Source/Boogie.sln | 15 + Source/ExecutionEngine/ExecutionEngine.cs | 6 +- Source/ExecutionEngine/ExecutionEngine.csproj | 1 + Source/Provers/LeanAuto/LeanAuto.cs | 602 ++++++++++++++++++ Source/Provers/LeanAuto/LeanAuto.csproj | 18 + Source/VCGeneration/Checker.cs | 1 - 6 files changed, 639 insertions(+), 4 deletions(-) create mode 100644 Source/Provers/LeanAuto/LeanAuto.cs create mode 100644 Source/Provers/LeanAuto/LeanAuto.csproj diff --git a/Source/Boogie.sln b/Source/Boogie.sln index 0715831b5..554d06d74 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -41,6 +41,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CoreTests", "UnitTests\Core EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngineTests", "UnitTests\ExecutionEngineTests\ExecutionEngineTests.csproj", "{473CF455-4306-46E3-9A44-FB7DBA42CA38}" EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "LeanAuto", "Provers\LeanAuto\LeanAuto.csproj", "{FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|Any CPU = Debug|Any CPU @@ -294,6 +296,18 @@ Global {473CF455-4306-46E3-9A44-FB7DBA42CA38}.Release|x64.Build.0 = Release|Any CPU {473CF455-4306-46E3-9A44-FB7DBA42CA38}.Release|x86.ActiveCfg = Release|Any CPU {473CF455-4306-46E3-9A44-FB7DBA42CA38}.Release|x86.Build.0 = Release|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Debug|Any CPU.Build.0 = Debug|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Debug|x64.ActiveCfg = Debug|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Debug|x64.Build.0 = Debug|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Debug|x86.ActiveCfg = Debug|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Debug|x86.Build.0 = Debug|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Release|Any CPU.ActiveCfg = Release|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Release|Any CPU.Build.0 = Release|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Release|x64.ActiveCfg = Release|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Release|x64.Build.0 = Release|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Release|x86.ActiveCfg = Release|Any CPU + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC}.Release|x86.Build.0 = Release|Any CPU EndGlobalSection GlobalSection(NestedProjects) = preSolution {FDF25D38-01A2-4EAA-8A3E-6F8F7CD254D2} = {EC2B5ECD-B97D-43D6-86F8-28163710B717} @@ -301,5 +315,6 @@ Global {10F866A2-6A9B-4B3D-AEAB-43314BD0475D} = {91134A3E-0D5D-4017-B04E-48BA254B3CF8} {D2D77420-CFDB-4DA1-B7E7-844C8E8CC686} = {91134A3E-0D5D-4017-B04E-48BA254B3CF8} {473CF455-4306-46E3-9A44-FB7DBA42CA38} = {91134A3E-0D5D-4017-B04E-48BA254B3CF8} + {FF9CFE2D-AB94-4973-B0E3-FB00F707ACDC} = {EC2B5ECD-B97D-43D6-86F8-28163710B717} EndGlobalSection EndGlobal diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 18202b600..c7b9070d3 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -7,14 +7,12 @@ using System.Threading; using System.Threading.Tasks; using VC; -using BoogiePL = Microsoft.Boogie; using System.Runtime.Caching; using System.Diagnostics; using System.Reactive.Linq; using System.Reactive.Subjects; using System.Reactive.Threading.Tasks; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices.ComTypes; +using Microsoft.Boogie.LeanAuto; using VCGeneration; namespace Microsoft.Boogie @@ -577,6 +575,8 @@ public async Task InferAndVerify( PrintBplFile(Options.PrintFile, processedProgram.Program, true, true, Options.PrettyPrint); } + LeanGenerator.EmitPassiveProgramAsLean(processedProgram.Program, Console.Out); + if (1 < Options.VerifySnapshots && programId != null) { program.FreezeTopLevelDeclarations(); diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj index 897f68d9b..ef5f7e2a3 100644 --- a/Source/ExecutionEngine/ExecutionEngine.csproj +++ b/Source/ExecutionEngine/ExecutionEngine.csproj @@ -20,6 +20,7 @@ + diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs new file mode 100644 index 000000000..05e09d68f --- /dev/null +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -0,0 +1,602 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Xml.Linq; + +namespace Microsoft.Boogie.LeanAuto; + +public class LeanGenerator : ReadOnlyVisitor +{ + private TextWriter writer; + + private readonly string header = @" +import Auto +import Auto.Tactic +open Lean Std + +set_option auto.smt true +set_option trace.auto.smt.printCommands false +set_option auto.smt.trust true +set_option auto.duper false +set_option auto.smt.solver.name ""z3"" +set_option trace.auto.buildChecker false + +def assert (ψ β: Prop): Prop := ψ ∧ β +def assume (ψ β: Prop): Prop := ψ → β +def skip (β: Prop): Prop := β +def ret: Prop := true +def goto: Prop -> Prop := id + +-- SMT Array definition +def SMTArray (s1 s2: Type) := s1 -> s2 + +def store [BEq s1] (m: SMTArray s1 s2) (i: s1) (v: s2): SMTArray s1 s2 := + fun i' => if i' == i then v else m i' + +def select (m: SMTArray s1 s2) (i: s1): s2 := m i +"; + + public LeanGenerator(TextWriter writer) + { + this.writer = writer; + } + + public static void EmitPassiveProgramAsLean(Program p, TextWriter writer) + { + var generator = new LeanGenerator(writer); + generator.EmitHeader(); + try { + generator.Visit(p); + } catch (LeanConversionException e) { + writer.WriteLine($"-- failed translation: {e.Msg}"); + } + } + + private void EmitHeader() + { + writer.WriteLine(header); + } + + public override Block VisitBlock(Block node) + { + writer.WriteLine($" {node.Label} :="); + node.Cmds.ForEach(c => Visit(c)); + if (node.TransferCmd is ReturnCmd r) { + VisitReturnCmd(r); + } + if (node.TransferCmd is GotoCmd g) { + VisitGotoCmd(g); + } + writer.WriteLine(); + return node; + } + + public override Cmd VisitAssertCmd(AssertCmd node) + { + writer.Write($" assert "); + VisitExpr(node.Expr); + writer.WriteLine(" $"); + return node; + } + + public override Cmd VisitAssumeCmd(AssumeCmd node) + { + writer.Write($" assume "); + VisitExpr(node.Expr); + writer.WriteLine(" $"); + return node; + } + + public override GotoCmd VisitGotoCmd(GotoCmd node) + { + var gotoText = node.labelTargets.Select(l => + $"goto {l.Label}").Aggregate((a, b) => $"{a} \u2227 {b}"); + writer.WriteLine(" " + gotoText); + return node; + } + + public override ReturnCmd VisitReturnCmd(ReturnCmd node) + { + writer.WriteLine(" ret"); + return node; + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + writer.Write(SanitizeNameForLean(node.Name)); + return node; + } + + public override Type VisitBasicType(BasicType node) + { + if (node.IsBool) { + writer.Write("Bool"); + } else if (node.IsInt) { + writer.Write("Int"); + } else if (node.IsMap) { + var mapType = node.AsMap; + var domain = mapType.Arguments[0]; + var range = mapType.Result; + writer.Write("SMTArray "); + Visit(mapType.Arguments[0]); + writer.Write(" "); + Visit(mapType.Result); + } else { + writer.Write("(TODO: BasicType)"); + } + + return node; + } + + public override Expr VisitBvConcatExpr(BvConcatExpr node) + { + throw new LeanConversionException("Unsupported: BvConcatExpr"); + } + + public override Type VisitBvType(BvType node) + { + throw new LeanConversionException("Unsupported: BvType"); + } + + public override BoundVariable VisitBoundVariable(BoundVariable node) + { + throw new LeanConversionException("Unsupported: BoundVariable"); + } + + public override Constant VisitConstant(Constant node) + { + writer.Write("variable "); + Visit(node.TypedIdent); + writer.WriteLine(); + return node; + } + + public override CtorType VisitCtorType(CtorType node) + { + throw new LeanConversionException("Unsupported: CtorType"); + } + + public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) + { + var kind = node switch + { + ForallExpr => "forall", + ExistsExpr => "exists", + _ => "" + }; + writer.Write($"({kind}"); + foreach (var x in node.Dummies) { + writer.Write(" "); + VisitTypedIdent(x.TypedIdent); + } + writer.Write(", "); + Visit(node.Body); + writer.Write(")"); + + return node; + } + + public override TypedIdent VisitTypedIdent(TypedIdent node) + { + writer.Write("("); + writer.Write(SanitizeNameForLean(node.Name)); + writer.Write(" : "); + Visit(node.Type); + writer.Write(")"); + return node; + } + + public override Expr VisitBvExtractExpr(BvExtractExpr node) + { + throw new LeanConversionException("Unsupported: BvExtractExpr"); + } + + public override Expr VisitLambdaExpr(LambdaExpr node) + { + throw new LeanConversionException("Unsupported: LambdaExpr"); + } + + public override Expr VisitLetExpr(LetExpr node) + { + throw new LeanConversionException("Unsupported: LetExpr"); + } + + public override Formal VisitFormal(Formal node) + { + throw new LeanConversionException("Unsupported: Formal"); + } + + public override GlobalVariable VisitGlobalVariable(GlobalVariable node) + { + writer.Write("variable "); + Visit(node.TypedIdent); + writer.WriteLine(); + return node; + } + + public override Expr VisitLiteralExpr(LiteralExpr node) + { + writer.Write(node.ToString()); // TODO: make sure this is right + return node; + } + + public override LocalVariable VisitLocalVariable(LocalVariable node) + { + throw new LeanConversionException("Unsupported: LocalVariable"); + } + + public override Type VisitMapType(MapType node) + { + writer.Write("SMTArray "); + Visit(node.Arguments[0]); + writer.Write(" "); + Visit(node.Result); + return node; + } + + public override Expr VisitNAryExpr(NAryExpr node) + { + var fun = node.Fun; + var args = node.Args; + writer.Write("("); + if (fun is BinaryOperator op && args.Count == 2) { + Visit(args[0]); + writer.Write($" {BinaryOpToLean(op.Op)} "); + Visit(args[1]); + } else { + VisitIAppliable(fun); + foreach (var arg in args) { + writer.Write(" "); + Visit(arg); + } + } + writer.Write(")"); + + return node; + } + + private void VisitIAppliable(IAppliable fun) + { + switch (fun) { + case MapSelect: + writer.Write("select"); + break; + case MapStore: + writer.Write("store"); + break; + case BinaryOperator op: + writer.Write(BinaryOpToLean(op.Op)); + break; + case UnaryOperator op: + writer.Write(UnaryOpToLean(op.Op)); + break; + case FunctionCall fc: + writer.Write(SanitizeNameForLean(fc.Func.Name)); + break; + default: + throw new LeanConversionException($"Unsupported: IAppliable: {fun}"); + } + } + + public override Expr VisitOldExpr(OldExpr node) + { + throw new LeanConversionException("Unsupported: OldExpr"); + } + + public override Type VisitFloatType(FloatType node) + { + throw new LeanConversionException("Unsupported: FloatType"); + } + + public override Requires VisitRequires(Requires requires) + { + return requires; // TODO: do something with it + } + + public override Ensures VisitEnsures(Ensures ensures) + { + return ensures; // TODO: do something with it + } + + public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) + { + return node; // TODO: do something + } + + public override Cmd VisitAssignCmd(AssignCmd node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Cmd VisitUnpackCmd(UnpackCmd node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override AtomicRE VisitAtomicRE(AtomicRE node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Type VisitBvTypeProxy(BvTypeProxy node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Expr VisitCodeExpr(CodeExpr node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Cmd VisitCallCmd(CallCmd node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Cmd VisitParCallCmd(ParCallCmd node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Choice VisitChoice(Choice node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Cmd VisitCommentCmd(CommentCmd node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override List VisitRequiresSeq(List requiresSeq) + { + return requiresSeq; // TODO: do something + } + + public override List VisitEnsuresSeq(List ensuresSeq) + { + return ensuresSeq; // TODO: do something + } + + public override Cmd VisitHavocCmd(HavocCmd node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Type VisitMapTypeProxy(MapTypeProxy node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override QKeyValue VisitQKeyValue(QKeyValue node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Cmd VisitRE(RE node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override List VisitRESeq(List reSeq) + { + throw new LeanConversionException($"Unsupported: {reSeq}"); + } + + public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Sequential VisitSequential(Sequential node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Cmd VisitStateCmd(StateCmd node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Declaration VisitTypeCtorDecl(TypeCtorDecl node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Declaration VisitTypeSynonymDecl(TypeSynonymDecl node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Type VisitTypeVariable(TypeVariable node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Type VisitTypeProxy(TypeProxy node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) + { + writer.Write($" assert "); + VisitExpr(node.Expr); + writer.WriteLine(" $"); + return node; + } + + public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override List VisitCallCmdSeq(List callCmds) + { + throw new LeanConversionException($"Unsupported: CallCmds"); + } + + public override AssignLhs VisitFieldAssignLhs(FieldAssignLhs node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override ActionDeclRef VisitActionDeclRef(ActionDeclRef node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override ElimDecl VisitElimDecl(ElimDecl node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override List VisitElimDeclSeq(List node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Procedure VisitActionDecl(ActionDecl node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override YieldingLoop VisitYieldingLoop(YieldingLoop node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Dictionary VisitYieldingLoops(Dictionary node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Procedure VisitYieldInvariantDecl(YieldInvariantDecl node) + { + throw new LeanConversionException($"Unsupported: {node}"); + } + + public override Axiom VisitAxiom(Axiom node) + { + // This will take two more steps: + // * A named lemma with a definition of `by sorry` (using a `name` attribute?) (or `id`, so it's also useful for proof dependencies?) + // * A named lemma that's defined by a call to a previously-defined proof of the same thing + var name = $"ax_l{node.tok.line}c{node.tok.col}"; + writer.Write($"axiom {name}: "); + VisitExpr(node.Expr); + writer.WriteLine(); + return node; + } + + public override Function VisitFunction(Function node) + { + writer.WriteLine($"-- function {node.Name}"); + return node; + } + + private string BinaryOpToLean(BinaryOperator.Opcode op) + { + return op switch + { + BinaryOperator.Opcode.Add => "+", + BinaryOperator.Opcode.Sub => "-", + BinaryOperator.Opcode.Mul => "*", + BinaryOperator.Opcode.Div => "/", + BinaryOperator.Opcode.Mod => "%", + BinaryOperator.Opcode.Lt => "<", + BinaryOperator.Opcode.Gt => ">", + BinaryOperator.Opcode.Le => "<=", + BinaryOperator.Opcode.Ge => ">=", + BinaryOperator.Opcode.Eq => "=", + BinaryOperator.Opcode.Neq => "!=", + BinaryOperator.Opcode.And => "\u2227", + BinaryOperator.Opcode.Or => "||", + BinaryOperator.Opcode.Iff => "=", + BinaryOperator.Opcode.Imp => "->", + BinaryOperator.Opcode.Pow => "TODO", + BinaryOperator.Opcode.FloatDiv => "TODO", + BinaryOperator.Opcode.RealDiv => "TODO", + _ => throw new LeanConversionException($"unsupported binary operator: {op.ToString()}") + }; + } + + private string UnaryOpToLean(UnaryOperator.Opcode op) + { + return op switch + { + UnaryOperator.Opcode.Not => "!", + UnaryOperator.Opcode.Neg => "-", + _ => throw new LeanConversionException($"unsupported unary operator: {op.ToString()}") + }; + } + + private string SanitizeNameForLean(string name) + { + return name.Replace('@', '_'); + } + + public override Procedure VisitProcedure(Procedure node) + { + return node; + } + + public override Implementation VisitImplementation(Implementation node) + { + + writer.WriteLine(); + writer.WriteLine($"namespace impl_{node.Name}"); + writer.WriteLine(); + + foreach (var x in node.LocVars) { + writer.Write("variable "); + VisitTypedIdent(x.TypedIdent); + writer.WriteLine(); + } + + writer.WriteLine(); + writer.Write($"def {node.Name}_correct "); + node.InParams.ForEach(x => VisitTypedIdent(x.TypedIdent)); + node.OutParams.ForEach(x => VisitTypedIdent(x.TypedIdent)); + writer.WriteLine($" : Prop := {node.Blocks[0].Label}"); + writer.WriteLine(" where"); + node.Blocks.ForEach(b => VisitBlock(b)); + writer.WriteLine($"end impl_{node.Name}"); + writer.WriteLine(); + return node; + } +} + +internal class LeanConversionException : Exception +{ + public string Msg { get; } + public LeanConversionException(string s) + { + Msg = s; + } +} diff --git a/Source/Provers/LeanAuto/LeanAuto.csproj b/Source/Provers/LeanAuto/LeanAuto.csproj new file mode 100644 index 000000000..1c541a93b --- /dev/null +++ b/Source/Provers/LeanAuto/LeanAuto.csproj @@ -0,0 +1,18 @@ + + + + Library + Boogie.Provers.LeanAuto + + + + + + + + + + + + + diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index 125552d7d..0224d9cf1 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -6,7 +6,6 @@ using Microsoft.Boogie.VCExprAST; using System.Diagnostics; using System.Threading.Tasks; -using Microsoft.Boogie.SMTLib; using VC; namespace Microsoft.Boogie From 8309d33a803b862ea5992098a6c367b0f54b62e8 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 14 Dec 2023 15:46:09 -0800 Subject: [PATCH 02/30] Now Bubble.bpl verifies after translation --- Source/Provers/LeanAuto/LeanAuto.cs | 139 ++++++++++++++++++++++------ 1 file changed, 109 insertions(+), 30 deletions(-) diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index 05e09d68f..2b1745a54 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -2,19 +2,30 @@ using System.Collections.Generic; using System.IO; using System.Linq; -using System.Xml.Linq; namespace Microsoft.Boogie.LeanAuto; public class LeanGenerator : ReadOnlyVisitor { private TextWriter writer; + private List globalVars = new(); + private List axiomNames = + new(new[] + { + "SelectStoreSame", "SelectStoreDistinct" + }); + private List defNames = + new(new[] + { + "assert", "assume", "goto", "ret", "skip" + }); private readonly string header = @" import Auto import Auto.Tactic open Lean Std +set_option linter.unusedVariables false set_option auto.smt true set_option trace.auto.smt.printCommands false set_option auto.smt.trust true @@ -35,6 +46,12 @@ def store [BEq s1] (m: SMTArray s1 s2) (i: s1) (v: s2): SMTArray s1 s2 := fun i' => if i' == i then v else m i' def select (m: SMTArray s1 s2) (i: s1): s2 := m i + +axiom SelectStoreSame (s1 s2: Type) [BEq s1] (a: SMTArray s1 s2) (i: s1) (e: s2): + select (store a i e) i = e + +axiom SelectStoreDistinct (s1 s2: Type) [BEq s1] (a: SMTArray s1 s2) (i: s1) (j: s1) (e: s2): + i ≠ j → select (store a i e) j = select a j "; public LeanGenerator(TextWriter writer) @@ -58,9 +75,34 @@ private void EmitHeader() writer.WriteLine(header); } + private void Indent(int n = 1, string str = null) + { + for (var i = 0; i < n; i++) { + writer.Write(" "); + } + + if (str is not null) { + writer.Write(str); + } + } + + private void NL() + { + writer.WriteLine(); + } + + private void List(IEnumerable strings) + { + writer.Write("["); + writer.Write(String.Join(", ", strings)); + writer.Write("]"); + } + public override Block VisitBlock(Block node) { - writer.WriteLine($" {node.Label} :="); + var label = SanitizeNameForLean(node.Label); + Indent(1, $"{label} :="); + NL(); node.Cmds.ForEach(c => Visit(c)); if (node.TransferCmd is ReturnCmd r) { VisitReturnCmd(r); @@ -68,13 +110,13 @@ public override Block VisitBlock(Block node) if (node.TransferCmd is GotoCmd g) { VisitGotoCmd(g); } - writer.WriteLine(); + NL(); return node; } public override Cmd VisitAssertCmd(AssertCmd node) { - writer.Write($" assert "); + Indent(2, "assert "); VisitExpr(node.Expr); writer.WriteLine(" $"); return node; @@ -82,7 +124,7 @@ public override Cmd VisitAssertCmd(AssertCmd node) public override Cmd VisitAssumeCmd(AssumeCmd node) { - writer.Write($" assume "); + Indent(2, "assume "); VisitExpr(node.Expr); writer.WriteLine(" $"); return node; @@ -92,13 +134,13 @@ public override GotoCmd VisitGotoCmd(GotoCmd node) { var gotoText = node.labelTargets.Select(l => $"goto {l.Label}").Aggregate((a, b) => $"{a} \u2227 {b}"); - writer.WriteLine(" " + gotoText); + Indent(2, gotoText); return node; } public override ReturnCmd VisitReturnCmd(ReturnCmd node) { - writer.WriteLine(" ret"); + Indent(2, "ret"); return node; } @@ -148,7 +190,8 @@ public override Constant VisitConstant(Constant node) { writer.Write("variable "); Visit(node.TypedIdent); - writer.WriteLine(); + NL(); + globalVars.Add(node); return node; } @@ -211,7 +254,8 @@ public override GlobalVariable VisitGlobalVariable(GlobalVariable node) { writer.Write("variable "); Visit(node.TypedIdent); - writer.WriteLine(); + NL(); + globalVars.Add(node); return node; } @@ -441,7 +485,7 @@ public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) { - writer.Write($" assert "); + Indent(2, "assert "); VisitExpr(node.Expr); writer.WriteLine(" $"); return node; @@ -510,13 +554,14 @@ public override Axiom VisitAxiom(Axiom node) var name = $"ax_l{node.tok.line}c{node.tok.col}"; writer.Write($"axiom {name}: "); VisitExpr(node.Expr); - writer.WriteLine(); + NL(); + axiomNames.Add(name); return node; } public override Function VisitFunction(Function node) { - writer.WriteLine($"-- function {node.Name}"); + writer.WriteLine($"-- function {Name(node)}"); return node; } @@ -561,33 +606,67 @@ private string SanitizeNameForLean(string name) return name.Replace('@', '_'); } + private string Name(NamedDeclaration d) + { + return SanitizeNameForLean(d.Name); + } + public override Procedure VisitProcedure(Procedure node) { return node; } + + private void WriteParams(Implementation node) + { + node.InParams.ForEach(x => + { + Indent(); + VisitTypedIdent(x.TypedIdent); + NL(); + }); + node.OutParams.ForEach(x => + { + Indent(); + VisitTypedIdent(x.TypedIdent); + NL(); + }); + node.LocVars.ForEach(x => + { + Indent(); + VisitTypedIdent(x.TypedIdent); + NL(); + }); + } public override Implementation VisitImplementation(Implementation node) { - writer.WriteLine(); - writer.WriteLine($"namespace impl_{node.Name}"); - writer.WriteLine(); - - foreach (var x in node.LocVars) { - writer.Write("variable "); - VisitTypedIdent(x.TypedIdent); - writer.WriteLine(); - } - - writer.WriteLine(); - writer.Write($"def {node.Name}_correct "); - node.InParams.ForEach(x => VisitTypedIdent(x.TypedIdent)); - node.OutParams.ForEach(x => VisitTypedIdent(x.TypedIdent)); - writer.WriteLine($" : Prop := {node.Blocks[0].Label}"); - writer.WriteLine(" where"); + NL(); + writer.WriteLine($"namespace impl_{Name(node)}"); + NL(); + + writer.WriteLine($"def {Name(node)}"); + WriteParams(node); + Indent(1, $": Prop := {node.Blocks[0].Label}"); + NL(); + Indent(1, "where"); + NL(); node.Blocks.ForEach(b => VisitBlock(b)); - writer.WriteLine($"end impl_{node.Name}"); - writer.WriteLine(); + NL(); + writer.WriteLine($"theorem {Name(node)}_correct"); + WriteParams(node); + var paramNames = + globalVars.Select(Name) + .Concat(node.InParams.Select(Name)) + .Concat(node.OutParams.Select(Name)) + .Concat(node.LocVars.Select(Name)); + var paramString = String.Join(' ', paramNames); + Indent(1, $": {Name(node)} {paramString} := by"); NL(); + Indent(2, "auto"); NL(); + Indent(3); List(axiomNames); NL(); + Indent(3); writer.Write("u"); List(defNames); NL(); + NL(); + writer.WriteLine($"end impl_{Name(node)}"); NL(); return node; } } From 4b2eb9eb1944e1641fc20145e33a14194d11ef56 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 19 Dec 2023 11:07:56 -0800 Subject: [PATCH 03/30] Control Lean printing with an option Currently undocumented. Change that eventually. --- Source/ExecutionEngine/CommandLineOptions.cs | 9 +++++++++ Source/ExecutionEngine/ExecutionEngine.cs | 6 +++++- Source/ExecutionEngine/ExecutionEngineOptions.cs | 1 + 3 files changed, 15 insertions(+), 1 deletion(-) diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index ff4755836..f242d1479 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -66,6 +66,7 @@ void ObjectInvariant2() public bool VerifySeparately { get; set; } public string PrintFile { get; set; } public string PrintPrunedFile { get; set; } + public string LeanFile { get; set; } /** * Whether to emit {:qid}, {:skolemid} and set-info :boogie-vc-id @@ -676,6 +677,14 @@ protected override bool ParseOption(string name, CommandLineParseState ps) return true; + case "printLean": + if (ps.ConfirmArgumentCount(1)) + { + LeanFile = args[ps.i]; + } + + return true; + case "pretty": int val = 1; if (ps.GetIntArgument(x => val = x, 2)) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index c7b9070d3..8094e9a19 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -575,7 +575,11 @@ public async Task InferAndVerify( PrintBplFile(Options.PrintFile, processedProgram.Program, true, true, Options.PrettyPrint); } - LeanGenerator.EmitPassiveProgramAsLean(processedProgram.Program, Console.Out); + if (Options.LeanFile is not null) { + var writer = new StreamWriter(Options.LeanFile); + LeanGenerator.EmitPassiveProgramAsLean(processedProgram.Program, writer); + writer.Close(); + } if (1 < Options.VerifySnapshots && programId != null) { diff --git a/Source/ExecutionEngine/ExecutionEngineOptions.cs b/Source/ExecutionEngine/ExecutionEngineOptions.cs index 34af05aef..e65435dc7 100644 --- a/Source/ExecutionEngine/ExecutionEngineOptions.cs +++ b/Source/ExecutionEngine/ExecutionEngineOptions.cs @@ -14,6 +14,7 @@ public interface ExecutionEngineOptions : HoudiniOptions, ConcurrencyOptions string DescriptiveToolName { get; } bool TraceProofObligations { get; } string PrintFile { get; } + string LeanFile { get; } string PrintCFGPrefix { get; } string CivlDesugaredFile { get; } bool CoalesceBlocks { get; } From 89b359548dcdf1f72c26490da8f8a7b8047ffbdf Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 19 Dec 2023 11:08:52 -0800 Subject: [PATCH 04/30] Translator sufficient to verify all but one textbook example BQueue uses a lot of features and is rejected by the translator for now. --- Source/Provers/LeanAuto/LeanAuto.cs | 182 +++++++++++++++++++--------- 1 file changed, 123 insertions(+), 59 deletions(-) diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index 2b1745a54..3394e2329 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -7,14 +7,14 @@ namespace Microsoft.Boogie.LeanAuto; public class LeanGenerator : ReadOnlyVisitor { - private TextWriter writer; - private List globalVars = new(); - private List axiomNames = + private readonly TextWriter writer; + private readonly List globalVars = new(); + private readonly List axiomNames = new(new[] { "SelectStoreSame", "SelectStoreDistinct" }); - private List defNames = + private readonly List defNames = new(new[] { "assert", "assume", "goto", "ret", "skip" @@ -28,16 +28,17 @@ open Lean Std set_option linter.unusedVariables false set_option auto.smt true set_option trace.auto.smt.printCommands false +--set_option auto.smt.proof false set_option auto.smt.trust true -set_option auto.duper false +--set_option auto.duper false set_option auto.smt.solver.name ""z3"" set_option trace.auto.buildChecker false -def assert (ψ β: Prop): Prop := ψ ∧ β -def assume (ψ β: Prop): Prop := ψ → β -def skip (β: Prop): Prop := β -def ret: Prop := true -def goto: Prop -> Prop := id +@[simp] def assert (ψ β: Prop): Prop := ψ ∧ β +@[simp] def assume (ψ β: Prop): Prop := ψ → β +@[simp] def skip (β: Prop): Prop := β +@[simp] def ret: Prop := true +@[simp] def goto: Prop -> Prop := id -- SMT Array definition def SMTArray (s1 s2: Type) := s1 -> s2 @@ -54,7 +55,7 @@ axiom SelectStoreDistinct (s1 s2: Type) [BEq s1] (a: SMTArray s1 s2) (i: s1) (j: i ≠ j → select (store a i e) j = select a j "; - public LeanGenerator(TextWriter writer) + private LeanGenerator(TextWriter writer) { this.writer = writer; } @@ -64,7 +65,11 @@ public static void EmitPassiveProgramAsLean(Program p, TextWriter writer) var generator = new LeanGenerator(writer); generator.EmitHeader(); try { - generator.Visit(p); + p.Constants.ForEach(c => generator.Visit(c)); + p.GlobalVariables.ForEach(gv => generator.Visit(gv)); + p.Functions.ForEach(f => generator.Visit(f)); + p.Axioms.ForEach(a => generator.Visit(a)); + p.Implementations.ForEach(i => generator.Visit(i)); } catch (LeanConversionException e) { writer.WriteLine($"-- failed translation: {e.Msg}"); } @@ -86,6 +91,12 @@ private void Indent(int n = 1, string str = null) } } + private void IndentL(int n = 1, string str = null) + { + Indent(n, str); + NL(); + } + private void NL() { writer.WriteLine(); @@ -100,9 +111,10 @@ private void List(IEnumerable strings) public override Block VisitBlock(Block node) { + // TODO: names less likely to clash var label = SanitizeNameForLean(node.Label); - Indent(1, $"{label} :="); - NL(); + IndentL(1, "@[simp]"); + IndentL(1, $"{label} :="); node.Cmds.ForEach(c => Visit(c)); if (node.TransferCmd is ReturnCmd r) { VisitReturnCmd(r); @@ -156,16 +168,21 @@ public override Type VisitBasicType(BasicType node) writer.Write("Bool"); } else if (node.IsInt) { writer.Write("Int"); + } else if (node.IsReal) { + writer.Write("Real"); + } else if (node.IsRMode) { + throw new LeanConversionException("Unsupported: RMode type"); + } else if (node.IsRegEx) { + throw new LeanConversionException("Unsupported: RegEx type"); } else if (node.IsMap) { var mapType = node.AsMap; - var domain = mapType.Arguments[0]; - var range = mapType.Result; - writer.Write("SMTArray "); + writer.Write("(SMTArray "); Visit(mapType.Arguments[0]); writer.Write(" "); Visit(mapType.Result); + writer.Write(")"); } else { - writer.Write("(TODO: BasicType)"); + throw new LeanConversionException($"Unsupported BasicType: {node}"); } return node; @@ -206,7 +223,7 @@ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) { ForallExpr => "forall", ExistsExpr => "exists", - _ => "" + _ => throw new LeanConversionException($"Unsupported quantifier type: {node.Kind}") }; writer.Write($"({kind}"); foreach (var x in node.Dummies) { @@ -261,13 +278,24 @@ public override GlobalVariable VisitGlobalVariable(GlobalVariable node) public override Expr VisitLiteralExpr(LiteralExpr node) { - writer.Write(node.ToString()); // TODO: make sure this is right + if(node.IsTrue) { + // Use lowercase version to ensure Bool, which can be coerced to Prop + writer.Write("true"); + } else if (node.IsFalse) { + // Use lowercase version to ensure Bool, which can be coerced to Prop + writer.Write("false"); + } else if (node.isBvConst) { + // Use lowercase version to ensure Bool, which can be coerced to Prop + writer.Write(node + "/- TODO: bit vector constants -/"); + } else { + writer.Write(node); // TODO: make sure this is right + } return node; } public override LocalVariable VisitLocalVariable(LocalVariable node) { - throw new LeanConversionException("Unsupported: LocalVariable"); + throw new LeanConversionException("Internal error: LocalVariable should never be visited implicitly"); } public override Type VisitMapType(MapType node) @@ -288,6 +316,18 @@ public override Expr VisitNAryExpr(NAryExpr node) Visit(args[0]); writer.Write($" {BinaryOpToLean(op.Op)} "); Visit(args[1]); + } else if (fun is IfThenElse && args.Count == 3) { + writer.Write("if "); + Visit(args[0]); + writer.Write(" then "); + Visit(args[1]); + writer.Write(" else "); + Visit(args[2]); + } else if (fun is TypeCoercion typeCoercion && args.Count == 1) { + // TODO: actually coerce to target type + Visit(args[0]); + writer.Write(" : "); + Visit(typeCoercion.Type); } else { VisitIAppliable(fun); foreach (var arg in args) { @@ -350,47 +390,48 @@ public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) public override Cmd VisitAssignCmd(AssignCmd node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: assign: {node}"); } public override Cmd VisitUnpackCmd(UnpackCmd node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: unpack: {node}"); } public override AtomicRE VisitAtomicRE(AtomicRE node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: atomicre: {node}"); } public override Type VisitBvTypeProxy(BvTypeProxy node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: bvtypeproxy: {node}"); } public override Expr VisitCodeExpr(CodeExpr node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: codexpr: {node}"); } public override Cmd VisitCallCmd(CallCmd node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: callcmd: {node}"); } public override Cmd VisitParCallCmd(ParCallCmd node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: parcallcmd: {node}"); } public override Choice VisitChoice(Choice node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: choice: {node}"); } public override Cmd VisitCommentCmd(CommentCmd node) { - throw new LeanConversionException($"Unsupported: {node}"); + // Comments are safe to ignore + return node; } public override List VisitRequiresSeq(List requiresSeq) @@ -405,82 +446,82 @@ public override List VisitEnsuresSeq(List ensuresSeq) public override Cmd VisitHavocCmd(HavocCmd node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: havoc: {node}"); } public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: mapassignlhs: {node}"); } public override Type VisitMapTypeProxy(MapTypeProxy node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: maptypeproxy: {node}"); } public override QKeyValue VisitQKeyValue(QKeyValue node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: qkeyvalue: {node}"); } public override Cmd VisitRE(RE node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: re: {node}"); } public override List VisitRESeq(List reSeq) { - throw new LeanConversionException($"Unsupported: {reSeq}"); + throw new LeanConversionException($"Unsupported: reseq: {reSeq}"); } public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: returnexprcmd: {node}"); } public override Sequential VisitSequential(Sequential node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: sequential: {node}"); } public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: simpleassignlhs: {node}"); } public override Cmd VisitStateCmd(StateCmd node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: statecmd: {node}"); } public override Declaration VisitTypeCtorDecl(TypeCtorDecl node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: typectordecl: {node}"); } public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: typesynonymannotation: {node}"); } public override Declaration VisitTypeSynonymDecl(TypeSynonymDecl node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: typesynonymdecl: {node}"); } public override Type VisitTypeVariable(TypeVariable node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: typevariable: {node}"); } public override Type VisitTypeProxy(TypeProxy node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: typeproxy: {node}"); } public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node) { - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: UnresolvedTypeIdentifier: {node}"); } public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) @@ -493,7 +534,10 @@ public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) { - throw new LeanConversionException($"Unsupported: {node}"); + Indent(2, "assert "); + VisitExpr(node.Expr); + writer.WriteLine(" $"); + return node; } public override List VisitCallCmdSeq(List callCmds) @@ -561,7 +605,26 @@ public override Axiom VisitAxiom(Axiom node) public override Function VisitFunction(Function node) { - writer.WriteLine($"-- function {Name(node)}"); + // In the long run, this should define functions when possible. + writer.Write($"def {Name(node)} : "); + node.InParams.ForEach(x => + { + Visit(x.TypedIdent.Type); writer.Write(" -> "); + }); + if (node.OutParams.Count == 1) { + Visit(node.OutParams[0].TypedIdent.Type); + } else { + writer.Write("("); + node.OutParams.ForEach(x => + { + Visit(x.TypedIdent.Type); writer.Write(", "); + }); + writer.Write(")"); + } + writer.WriteLine(" := by sorry"); + NL(); + // Note: definition axioms will be emitted later + // node.DefinitionAxioms.ForEach(ax => VisitAxiom(ax)); return node; } @@ -640,20 +703,20 @@ private void WriteParams(Implementation node) public override Implementation VisitImplementation(Implementation node) { + var name = Name(node); NL(); - writer.WriteLine($"namespace impl_{Name(node)}"); + writer.WriteLine($"namespace impl_{name}"); NL(); - writer.WriteLine($"def {Name(node)}"); + writer.WriteLine("@[simp]"); + writer.WriteLine($"def {name}"); WriteParams(node); - Indent(1, $": Prop := {node.Blocks[0].Label}"); - NL(); - Indent(1, "where"); - NL(); + IndentL(1, $": Prop := {node.Blocks[0].Label}"); + IndentL(1, "where"); node.Blocks.ForEach(b => VisitBlock(b)); NL(); - writer.WriteLine($"theorem {Name(node)}_correct"); + writer.WriteLine($"theorem {name}_correct"); WriteParams(node); var paramNames = globalVars.Select(Name) @@ -661,12 +724,13 @@ public override Implementation VisitImplementation(Implementation node) .Concat(node.OutParams.Select(Name)) .Concat(node.LocVars.Select(Name)); var paramString = String.Join(' ', paramNames); - Indent(1, $": {Name(node)} {paramString} := by"); NL(); - Indent(2, "auto"); NL(); + Indent(1, $": {name} {paramString} := by"); NL(); + IndentL(2, "simp"); + IndentL(2, "auto"); Indent(3); List(axiomNames); NL(); - Indent(3); writer.Write("u"); List(defNames); NL(); + IndentL(3, "u[]"); NL(); - writer.WriteLine($"end impl_{Name(node)}"); NL(); + writer.WriteLine($"end impl_{name}"); NL(); return node; } } From f6f8ff637aae6a2761eba822380f80c704957be0 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 19 Dec 2023 13:02:06 -0800 Subject: [PATCH 05/30] Reorganize unsupported overrides --- Source/Provers/LeanAuto/LeanAuto.cs | 337 +++++++++++++++++----------- 1 file changed, 204 insertions(+), 133 deletions(-) diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index 3394e2329..c545012f3 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -190,19 +190,16 @@ public override Type VisitBasicType(BasicType node) public override Expr VisitBvConcatExpr(BvConcatExpr node) { + // TODO: implement throw new LeanConversionException("Unsupported: BvConcatExpr"); } public override Type VisitBvType(BvType node) { + // TODO: implement throw new LeanConversionException("Unsupported: BvType"); } - public override BoundVariable VisitBoundVariable(BoundVariable node) - { - throw new LeanConversionException("Unsupported: BoundVariable"); - } - public override Constant VisitConstant(Constant node) { writer.Write("variable "); @@ -214,6 +211,7 @@ public override Constant VisitConstant(Constant node) public override CtorType VisitCtorType(CtorType node) { + // TODO: implement (next) throw new LeanConversionException("Unsupported: CtorType"); } @@ -249,24 +247,22 @@ public override TypedIdent VisitTypedIdent(TypedIdent node) public override Expr VisitBvExtractExpr(BvExtractExpr node) { + // TODO: implement throw new LeanConversionException("Unsupported: BvExtractExpr"); } public override Expr VisitLambdaExpr(LambdaExpr node) { + // TODO: implement throw new LeanConversionException("Unsupported: LambdaExpr"); } public override Expr VisitLetExpr(LetExpr node) { + // TODO: implement throw new LeanConversionException("Unsupported: LetExpr"); } - public override Formal VisitFormal(Formal node) - { - throw new LeanConversionException("Unsupported: Formal"); - } - public override GlobalVariable VisitGlobalVariable(GlobalVariable node) { writer.Write("variable "); @@ -293,11 +289,6 @@ public override Expr VisitLiteralExpr(LiteralExpr node) return node; } - public override LocalVariable VisitLocalVariable(LocalVariable node) - { - throw new LeanConversionException("Internal error: LocalVariable should never be visited implicitly"); - } - public override Type VisitMapType(MapType node) { writer.Write("SMTArray "); @@ -365,11 +356,13 @@ private void VisitIAppliable(IAppliable fun) public override Expr VisitOldExpr(OldExpr node) { + // TODO: implement throw new LeanConversionException("Unsupported: OldExpr"); } public override Type VisitFloatType(FloatType node) { + // TODO: implement (but low priority) throw new LeanConversionException("Unsupported: FloatType"); } @@ -388,46 +381,18 @@ public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) return node; // TODO: do something } - public override Cmd VisitAssignCmd(AssignCmd node) - { - throw new LeanConversionException($"Unsupported: assign: {node}"); - } - - public override Cmd VisitUnpackCmd(UnpackCmd node) - { - throw new LeanConversionException($"Unsupported: unpack: {node}"); - } - - public override AtomicRE VisitAtomicRE(AtomicRE node) - { - throw new LeanConversionException($"Unsupported: atomicre: {node}"); - } - public override Type VisitBvTypeProxy(BvTypeProxy node) { + // TODO: implement throw new LeanConversionException($"Unsupported: bvtypeproxy: {node}"); } public override Expr VisitCodeExpr(CodeExpr node) { + // TODO: what is this? throw new LeanConversionException($"Unsupported: codexpr: {node}"); } - public override Cmd VisitCallCmd(CallCmd node) - { - throw new LeanConversionException($"Unsupported: callcmd: {node}"); - } - - public override Cmd VisitParCallCmd(ParCallCmd node) - { - throw new LeanConversionException($"Unsupported: parcallcmd: {node}"); - } - - public override Choice VisitChoice(Choice node) - { - throw new LeanConversionException($"Unsupported: choice: {node}"); - } - public override Cmd VisitCommentCmd(CommentCmd node) { // Comments are safe to ignore @@ -444,86 +409,42 @@ public override List VisitEnsuresSeq(List ensuresSeq) return ensuresSeq; // TODO: do something } - public override Cmd VisitHavocCmd(HavocCmd node) - { - throw new LeanConversionException($"Unsupported: havoc: {node}"); - } - - public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) - { - throw new LeanConversionException($"Unsupported: mapassignlhs: {node}"); - } - public override Type VisitMapTypeProxy(MapTypeProxy node) { + // TODO: implement throw new LeanConversionException($"Unsupported: maptypeproxy: {node}"); } public override QKeyValue VisitQKeyValue(QKeyValue node) { - throw new LeanConversionException($"Unsupported: qkeyvalue: {node}"); - } - - public override Cmd VisitRE(RE node) - { - throw new LeanConversionException($"Unsupported: re: {node}"); - } - - public override List VisitRESeq(List reSeq) - { - throw new LeanConversionException($"Unsupported: reseq: {reSeq}"); - } - - public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) - { - throw new LeanConversionException($"Unsupported: returnexprcmd: {node}"); - } - - public override Sequential VisitSequential(Sequential node) - { - throw new LeanConversionException($"Unsupported: sequential: {node}"); - } - - public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node) - { - throw new LeanConversionException($"Unsupported: simpleassignlhs: {node}"); - } - - public override Cmd VisitStateCmd(StateCmd node) - { - throw new LeanConversionException($"Unsupported: statecmd: {node}"); + // Implement this if we want to visit attributes? Or maybe extract them more directly. + return node; } public override Declaration VisitTypeCtorDecl(TypeCtorDecl node) { + // TODO: implement throw new LeanConversionException($"Unsupported: typectordecl: {node}"); } public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) { + // TODO: implement throw new LeanConversionException($"Unsupported: typesynonymannotation: {node}"); } public override Declaration VisitTypeSynonymDecl(TypeSynonymDecl node) { + // TODO: implement throw new LeanConversionException($"Unsupported: typesynonymdecl: {node}"); } - public override Type VisitTypeVariable(TypeVariable node) - { - throw new LeanConversionException($"Unsupported: typevariable: {node}"); - } - public override Type VisitTypeProxy(TypeProxy node) { + // TODO: implement throw new LeanConversionException($"Unsupported: typeproxy: {node}"); } - public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node) - { - throw new LeanConversionException($"Unsupported: UnresolvedTypeIdentifier: {node}"); - } - public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) { Indent(2, "assert "); @@ -540,53 +461,21 @@ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) return node; } - public override List VisitCallCmdSeq(List callCmds) - { - throw new LeanConversionException($"Unsupported: CallCmds"); - } - - public override AssignLhs VisitFieldAssignLhs(FieldAssignLhs node) - { - throw new LeanConversionException($"Unsupported: {node}"); - } - public override ActionDeclRef VisitActionDeclRef(ActionDeclRef node) { + // TODO: what is this? throw new LeanConversionException($"Unsupported: {node}"); } public override ElimDecl VisitElimDecl(ElimDecl node) { + // TODO: support this? throw new LeanConversionException($"Unsupported: {node}"); } public override List VisitElimDeclSeq(List node) { - throw new LeanConversionException($"Unsupported: {node}"); - } - - public override Procedure VisitActionDecl(ActionDecl node) - { - throw new LeanConversionException($"Unsupported: {node}"); - } - - public override YieldingLoop VisitYieldingLoop(YieldingLoop node) - { - throw new LeanConversionException($"Unsupported: {node}"); - } - - public override Dictionary VisitYieldingLoops(Dictionary node) - { - throw new LeanConversionException($"Unsupported: {node}"); - } - - public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node) - { - throw new LeanConversionException($"Unsupported: {node}"); - } - - public override Procedure VisitYieldInvariantDecl(YieldInvariantDecl node) - { + // TODO: support this? throw new LeanConversionException($"Unsupported: {node}"); } @@ -700,11 +589,11 @@ private void WriteParams(Implementation node) NL(); }); } - + public override Implementation VisitImplementation(Implementation node) { var name = Name(node); - + NL(); writer.WriteLine($"namespace impl_{name}"); NL(); @@ -733,6 +622,188 @@ public override Implementation VisitImplementation(Implementation node) writer.WriteLine($"end impl_{name}"); NL(); return node; } + + /* ==== Nodes that should never be visited ==== */ + + public override Program VisitProgram(Program node) + { + throw new LeanConversionException($"Internal: Program should never be directly visited {node.tok}"); + } + + public override Declaration VisitDeclaration(Declaration node) + { + throw new LeanConversionException($"Internal: Declaration should never be directly visited {node.tok}"); + } + + public override List VisitDeclarationList(List declarationList) + { + throw new LeanConversionException($"Internal: List should never be directly visited {declarationList}"); + } + + public override List VisitBlockSeq(List blockSeq) + { + throw new LeanConversionException($"Internal: List should never be directly visited {blockSeq}"); + } + + public override List VisitBlockList(List blocks) + { + throw new LeanConversionException($"Internal: List should never be directly visited {blocks}"); + } + + public override Trigger VisitTrigger(Trigger node) + { + throw new LeanConversionException($"Internal: Trigger should never be directly visited {node.tok}"); + } + + public override IList VisitExprSeq(IList exprSeq) + { + throw new LeanConversionException($"Internal: List should never be directly visited {exprSeq}"); + } + + public override BoundVariable VisitBoundVariable(BoundVariable node) + { + throw new LeanConversionException($"Internal: BoundVariable should never be directly visited {node.tok}"); + } + + public override Formal VisitFormal(Formal node) + { + throw new LeanConversionException($"Internal: Formal should never be directly visited {node.tok}"); + } + + public override LocalVariable VisitLocalVariable(LocalVariable node) + { + throw new LeanConversionException($"Internal error: LocalVariable should never be directly visited {node.tok}"); + } + + public override Type VisitTypeVariable(TypeVariable node) + { + throw new LeanConversionException($"Internal: TypeVariable should never be directly visited {node.tok}"); + } + + public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node) + { + throw new LeanConversionException($"Internal: UnresolvedTypeIdentifier should never appear ({node.tok})"); + } + + public override Variable VisitVariable(Variable node) + { + throw new LeanConversionException($"Internal: Variable should never be directly visited {node.tok}"); + } + + public override List VisitVariableSeq(List variableSeq) + { + throw new LeanConversionException($"Internal: List should never be directly visited {variableSeq}"); + } + + public override HashSet VisitVariableSet(HashSet node) + { + throw new LeanConversionException($"Internal: HashSet should never be directly visited {node}"); + } + + public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) + { + throw new LeanConversionException($"Internal: MapAssignLhs should never appear in passive program ({node.tok})."); + } + + public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node) + { + throw new LeanConversionException($"Internal: SimpleAssignLhs should never appear in passive program ({node.tok})."); + } + + public override AssignLhs VisitFieldAssignLhs(FieldAssignLhs node) + { + throw new LeanConversionException($"Internal: FieldAssignLhs should never appear in passive program ({node.tok})."); + } + + public override Cmd VisitAssignCmd(AssignCmd node) + { + throw new LeanConversionException($"Internal: AssignCmd should never appear in passive program ({node.tok})."); + } + + public override Cmd VisitUnpackCmd(UnpackCmd node) + { + throw new LeanConversionException($"Internal: UnpackCmd should never appear in passive program ({node.tok})."); + } + + public override Cmd VisitCallCmd(CallCmd node) + { + throw new LeanConversionException($"Internal: CallCmd should never appear in passive program ({node.tok})."); + } + + public override Cmd VisitParCallCmd(ParCallCmd node) + { + throw new LeanConversionException($"Internal: ParCallCmd should never appear in passive program ({node.tok})."); + } + + public override Cmd VisitHavocCmd(HavocCmd node) + { + throw new LeanConversionException($"Internal: HavocCmd should never appear in passive program ({node.tok})."); + } + + public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) + { + throw new LeanConversionException($"Internal: ReturnExprCmd should never appear in passive program ({node.tok})"); + } + + public override Cmd VisitStateCmd(StateCmd node) + { + throw new LeanConversionException($"Internal: StateCmd should never appear in passive program ({node.tok})"); + } + + public override List VisitCallCmdSeq(List callCmds) + { + throw new LeanConversionException($"Internal: List should never appear in passive program ({callCmds})."); + } + + public override Procedure VisitActionDecl(ActionDecl node) + { + throw new LeanConversionException($"Internal: ActionDecl should never appear in passive program ({node.tok})."); + } + + public override YieldingLoop VisitYieldingLoop(YieldingLoop node) + { + throw new LeanConversionException($"Internal: YieldingLoop should never appear in passive program ({node})."); + } + + public override Dictionary VisitYieldingLoops(Dictionary node) + { + throw new LeanConversionException($"Internal: YieldingLoops should never appear in passive program."); + } + + public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node) + { + throw new LeanConversionException($"Internal: YieldProcedureDecl should never appear in passive program ({node.tok})."); + } + + public override Procedure VisitYieldInvariantDecl(YieldInvariantDecl node) + { + throw new LeanConversionException($"Internal: YieldInvariantDecl should never appear in passive program ({node.tok})."); + } + + public override Cmd VisitRE(RE node) + { + throw new LeanConversionException($"Internal: RE should never appear in passive program ({node.tok})"); + } + + public override List VisitRESeq(List reSeq) + { + throw new LeanConversionException($"Internal: List should never appear in passive program ({reSeq})"); + } + + public override AtomicRE VisitAtomicRE(AtomicRE node) + { + throw new LeanConversionException($"Internal: AtomicRE should never appear in passive program ({node.tok})"); + } + + public override Choice VisitChoice(Choice node) + { + throw new LeanConversionException($"Internal: Choice should never appear in passive program ({node.tok})."); + } + + public override Sequential VisitSequential(Sequential node) + { + throw new LeanConversionException($"Internal: Sequential should never appear in passive program ({node.tok})"); + } } internal class LeanConversionException : Exception From 637c41546ceab261352b39ffd55f167f3a6fbbf8 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 19 Dec 2023 17:22:57 -0800 Subject: [PATCH 06/30] Various improvements --- Source/Core/AST/AbsyType.cs | 2 +- Source/Provers/LeanAuto/LeanAuto.cs | 383 +++++++++++++++++++++------- 2 files changed, 293 insertions(+), 92 deletions(-) diff --git a/Source/Core/AST/AbsyType.cs b/Source/Core/AST/AbsyType.cs index 2fd81a309..335fb48ff 100644 --- a/Source/Core/AST/AbsyType.cs +++ b/Source/Core/AST/AbsyType.cs @@ -2011,7 +2011,7 @@ public class TypeProxy : Type { static int proxies = 0; - protected readonly string /*!*/ + public readonly string /*!*/ Name; [ContractInvariantMethod] diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index c545012f3..ffe098fa6 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -9,19 +9,18 @@ public class LeanGenerator : ReadOnlyVisitor { private readonly TextWriter writer; private readonly List globalVars = new(); - private readonly List axiomNames = + private readonly HashSet usedNames = new(); + private bool usesMaps; + private readonly List mapAxiomNames = new(new[] { - "SelectStoreSame", "SelectStoreDistinct" - }); - private readonly List defNames = - new(new[] - { - "assert", "assume", "goto", "ret", "skip" + "SelectStoreSame", "SelectStoreDistinct", + "SelectStoreSame2", "SelectStoreDistinct2" }); + private readonly List userAxiomNames = new(); + private Dictionary> uniqueConsts = new(); - private readonly string header = @" -import Auto + private readonly string header = @"import Auto import Auto.Tactic open Lean Std @@ -38,21 +37,37 @@ @[simp] def assert (ψ β: Prop): Prop := ψ ∧ β @[simp] def assume (ψ β: Prop): Prop := ψ → β @[simp] def skip (β: Prop): Prop := β @[simp] def ret: Prop := true -@[simp] def goto: Prop -> Prop := id +@[simp] def goto: Prop → Prop := id -- SMT Array definition -def SMTArray (s1 s2: Type) := s1 -> s2 +def SMTArray1 (s1 s2: Type) := s1 → s2 + +def SMTArray2 (s1 s2 s3 : Type) := s1 → s2 → s3 -def store [BEq s1] (m: SMTArray s1 s2) (i: s1) (v: s2): SMTArray s1 s2 := +def store1 [BEq s1] (m: SMTArray1 s1 s2) (i: s1) (v: s2): SMTArray1 s1 s2 := fun i' => if i' == i then v else m i' -def select (m: SMTArray s1 s2) (i: s1): s2 := m i +def select1 (m: SMTArray1 s1 s2) (i: s1): s2 := m i + +def store2 [BEq s1] [BEq s2] (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (v: s3): SMTArray2 s1 s2 s3 := + fun i' j' => if i' == i && j' == j then v else m i' j' + +def select2 (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2): s3 := m i j + +axiom SelectStoreSame (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (e: s2): + select1 (store1 a i e) i = e -axiom SelectStoreSame (s1 s2: Type) [BEq s1] (a: SMTArray s1 s2) (i: s1) (e: s2): - select (store a i e) i = e +axiom SelectStoreDistinct (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (j: s1) (e: s2): + i ≠ j → select1 (store1 a i e) j = select1 a j -axiom SelectStoreDistinct (s1 s2: Type) [BEq s1] (a: SMTArray s1 s2) (i: s1) (j: s1) (e: s2): - i ≠ j → select (store a i e) j = select a j +axiom SelectStoreSame2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (e: s3): + select2 (store2 a i j e) i j = e + +axiom SelectStoreDistinct2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s2 s3) (i: s1) (i': s1) (j: s2) (j' : s2) (e: s3): + i ≠ i' \/ j ≠ j' → select2 (store2 a i j e) i' j' = select2 a i' j' + +-- TODO: provide either a definition or some functional axioms (or a definition plus some lemmas) +axiom distinct : {a : Type} → List a → Prop "; private LeanGenerator(TextWriter writer) @@ -65,19 +80,67 @@ public static void EmitPassiveProgramAsLean(Program p, TextWriter writer) var generator = new LeanGenerator(writer); generator.EmitHeader(); try { + generator.writer.WriteLine("-- Type constructors"); + p.TopLevelDeclarations.OfType().ForEach(tcd => generator.Visit(tcd)); + generator.NL(); + + generator.writer.WriteLine("-- Type synonyms"); + p.TopLevelDeclarations.OfType().ForEach(tcd => generator.Visit(tcd)); + generator.NL(); + + generator.writer.WriteLine("-- Constants"); p.Constants.ForEach(c => generator.Visit(c)); + generator.NL(); + + generator.writer.WriteLine("-- Unique const axioms"); + generator.EmitUniqueConstAxioms(); + generator.NL(); + + generator.writer.WriteLine("-- Variables"); p.GlobalVariables.ForEach(gv => generator.Visit(gv)); + generator.NL(); + + generator.writer.WriteLine("-- Functions"); p.Functions.ForEach(f => generator.Visit(f)); + generator.NL(); + + generator.writer.WriteLine("-- Axioms"); p.Axioms.ForEach(a => generator.Visit(a)); + generator.NL(); + + generator.writer.WriteLine("-- Implementations"); p.Implementations.ForEach(i => generator.Visit(i)); } catch (LeanConversionException e) { - writer.WriteLine($"-- failed translation: {e.Msg}"); + Console.WriteLine($"Failed translation: {e.Msg}"); + } + } + + private void AddUniqueConst(Type t, string name) + { + if (!uniqueConsts.ContainsKey(t)) { + uniqueConsts[t] = new(); + } + if (!uniqueConsts[t].Contains(name)) { + uniqueConsts[t].Add(name); + } + } + + private void EmitUniqueConstAxioms() + { + int i = 0; + foreach (var kv in uniqueConsts) { + var axiomName = $"unique{i}"; + userAxiomNames.Add(axiomName); + writer.Write($"axiom {axiomName}: distinct "); + List(kv.Value); + NL(); + i++; } } private void EmitHeader() { - writer.WriteLine(header); + writer.WriteLine(header.ReplaceLineEndings()); } private void Indent(int n = 1, string str = null) @@ -111,8 +174,7 @@ private void List(IEnumerable strings) public override Block VisitBlock(Block node) { - // TODO: names less likely to clash - var label = SanitizeNameForLean(node.Label); + var label = BlockName(node); IndentL(1, "@[simp]"); IndentL(1, $"{label} :="); node.Cmds.ForEach(c => Visit(c)); @@ -145,7 +207,7 @@ public override Cmd VisitAssumeCmd(AssumeCmd node) public override GotoCmd VisitGotoCmd(GotoCmd node) { var gotoText = node.labelTargets.Select(l => - $"goto {l.Label}").Aggregate((a, b) => $"{a} \u2227 {b}"); + $"goto {BlockName(l)}").Aggregate((a, b) => $"{a} \u2227 {b}"); Indent(2, gotoText); return node; } @@ -158,10 +220,37 @@ public override ReturnCmd VisitReturnCmd(ReturnCmd node) public override Expr VisitIdentifierExpr(IdentifierExpr node) { - writer.Write(SanitizeNameForLean(node.Name)); + var name = SanitizeNameForLean(node.Name); + usedNames.Add(name); + writer.Write(name); return node; } + public override Type VisitType(Type node) + { + if (node is BasicType basicType) { + return VisitBasicType(basicType); + } else if (node is BvType bvType) { + return VisitBvType(bvType); + } else if (node is CtorType ctorType) { + return VisitCtorType(ctorType); + } else if (node is FloatType floatType) { + return VisitFloatType(floatType); + } else if (node is MapType mapType) { + return VisitMapType(mapType); + } else if (node is TypeProxy typeProxy) { + return VisitTypeProxy(typeProxy); + } else if (node is TypeSynonymAnnotation typeSynonymAnnotation) { + return VisitTypeSynonymAnnotation(typeSynonymAnnotation); + } else if (node is TypeVariable typeVariable) { + return VisitTypeVariable(typeVariable); + } else if (node is UnresolvedTypeIdentifier uti) { + return VisitUnresolvedTypeIdentifier(uti); + } else { + throw new LeanConversionException("Unreachable type case."); + } + } + public override Type VisitBasicType(BasicType node) { if (node.IsBool) { @@ -176,11 +265,7 @@ public override Type VisitBasicType(BasicType node) throw new LeanConversionException("Unsupported: RegEx type"); } else if (node.IsMap) { var mapType = node.AsMap; - writer.Write("(SMTArray "); - Visit(mapType.Arguments[0]); - writer.Write(" "); - Visit(mapType.Result); - writer.Write(")"); + VisitMapType(mapType); } else { throw new LeanConversionException($"Unsupported BasicType: {node}"); } @@ -190,20 +275,26 @@ public override Type VisitBasicType(BasicType node) public override Expr VisitBvConcatExpr(BvConcatExpr node) { - // TODO: implement - throw new LeanConversionException("Unsupported: BvConcatExpr"); + Visit(node.E0); + writer.Write(" ++ "); + Visit(node.E1); + return node; } public override Type VisitBvType(BvType node) { - // TODO: implement - throw new LeanConversionException("Unsupported: BvType"); + writer.Write($"(BitVec {node.Bits})"); + return node; } public override Constant VisitConstant(Constant node) { + var ti = node.TypedIdent; writer.Write("variable "); - Visit(node.TypedIdent); + Visit(ti); + if (node.Unique) { + AddUniqueConst(ti.Type, SanitizeNameForLean(ti.Name)); + } NL(); globalVars.Add(node); return node; @@ -211,8 +302,20 @@ public override Constant VisitConstant(Constant node) public override CtorType VisitCtorType(CtorType node) { - // TODO: implement (next) - throw new LeanConversionException("Unsupported: CtorType"); + if (node.Arguments.Any()) { + writer.Write("("); + } + + writer.Write(Name(node.Decl)); + node.Arguments.ForEach(a => + { + writer.Write(" "); + Visit(a); + }); + if (node.Arguments.Any()) { + writer.Write(")"); + } + return node; } public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) @@ -224,6 +327,9 @@ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) _ => throw new LeanConversionException($"Unsupported quantifier type: {node.Kind}") }; writer.Write($"({kind}"); + foreach (var tv in node.TypeParameters) { + writer.Write($" ({SanitizeNameForLean(tv.Name)} : Type)"); + } foreach (var x in node.Dummies) { writer.Write(" "); VisitTypedIdent(x.TypedIdent); @@ -238,7 +344,8 @@ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) public override TypedIdent VisitTypedIdent(TypedIdent node) { writer.Write("("); - writer.Write(SanitizeNameForLean(node.Name)); + var name = SanitizeNameForLean(node.Name); + writer.Write(name); writer.Write(" : "); Visit(node.Type); writer.Write(")"); @@ -247,20 +354,36 @@ public override TypedIdent VisitTypedIdent(TypedIdent node) public override Expr VisitBvExtractExpr(BvExtractExpr node) { - // TODO: implement - throw new LeanConversionException("Unsupported: BvExtractExpr"); + // TODO: double-check range values + writer.Write($"(BitVec.extractLsb {node.End - 1} {node.Start} "); + Visit(node.Bitvector); + writer.Write(")"); + return node; } public override Expr VisitLambdaExpr(LambdaExpr node) { - // TODO: implement - throw new LeanConversionException("Unsupported: LambdaExpr"); + writer.Write("(λ"); + node.Dummies.ForEach(x => Visit(x.TypedIdent)); + writer.Write("=>"); + Visit(node.Body); + writer.Write(")"); + return node; } public override Expr VisitLetExpr(LetExpr node) { - // TODO: implement - throw new LeanConversionException("Unsupported: LetExpr"); + if (node.Dummies.Count > 1) { + throw new LeanConversionException("Unsupported: LetExpr with more than one binder"); + } + writer.Write("(let"); + node.Dummies.ForEach(x => Visit(x.TypedIdent)); + writer.Write(" := "); + node.Rhss.ForEach(e => Visit(e)); + writer.Write("; "); + Visit(node.Body); + writer.Write(")"); + return node; } public override GlobalVariable VisitGlobalVariable(GlobalVariable node) @@ -281,20 +404,34 @@ public override Expr VisitLiteralExpr(LiteralExpr node) // Use lowercase version to ensure Bool, which can be coerced to Prop writer.Write("false"); } else if (node.isBvConst) { - // Use lowercase version to ensure Bool, which can be coerced to Prop - writer.Write(node + "/- TODO: bit vector constants -/"); + var bvConst = node.asBvConst; + writer.Write("("); + writer.Write(bvConst.Value); + writer.Write($" : BitVec {bvConst.Bits}"); + writer.Write(")"); } else { - writer.Write(node); // TODO: make sure this is right + writer.Write(node); // TODO: make sure this is right for all other literal types } return node; } public override Type VisitMapType(MapType node) { - writer.Write("SMTArray "); - Visit(node.Arguments[0]); - writer.Write(" "); + if (node.Arguments.Count > 2) { + throw new LeanConversionException($"Unsupported: MapType with too many index types ({node})"); + } + if (node.TypeParameters.Any()) { + var args = node.TypeParameters.Select(a => SanitizeNameForLean(a.Name)); + writer.Write($"forall ({String.Join(" ", args)} : Type), "); + } + writer.Write($"(SMTArray{node.Arguments.Count} "); + node.Arguments.ForEach(a => + { + Visit(a); + writer.Write(" "); + }); Visit(node.Result); + writer.Write(")"); return node; } @@ -315,10 +452,20 @@ public override Expr VisitNAryExpr(NAryExpr node) writer.Write(" else "); Visit(args[2]); } else if (fun is TypeCoercion typeCoercion && args.Count == 1) { - // TODO: actually coerce to target type + // TODO: might need to actually call a coercion function + Console.WriteLine($"Coerce: {args[0].Type} -> {typeCoercion.Type}"); + writer.Write("("); Visit(args[0]); writer.Write(" : "); Visit(typeCoercion.Type); + writer.Write(")"); + } else if (fun is FieldAccess fieldAccess) { + throw new LeanConversionException("Unsupported: field access (since the semantics are complex)"); + // TODO: implement + /* + Visit(args[0]); + writer.Write($".{SanitizeNameForLean(fieldAccess.FieldName)}"); + */ } else { VisitIAppliable(fun); foreach (var arg in args) { @@ -335,10 +482,12 @@ private void VisitIAppliable(IAppliable fun) { switch (fun) { case MapSelect: - writer.Write("select"); + usesMaps = true; + writer.Write($"select{fun.ArgumentCount - 1}"); break; case MapStore: - writer.Write("store"); + usesMaps = true; + writer.Write($"store{fun.ArgumentCount - 2}"); break; case BinaryOperator op: writer.Write(BinaryOpToLean(op.Op)); @@ -349,6 +498,10 @@ private void VisitIAppliable(IAppliable fun) case FunctionCall fc: writer.Write(SanitizeNameForLean(fc.Func.Name)); break; + case IsConstructor isConstructor: + // TODO: declare these discriminator functions + writer.Write($"is_{SanitizeNameForLean(isConstructor.ConstructorName)}"); + break; default: throw new LeanConversionException($"Unsupported: IAppliable: {fun}"); } @@ -356,34 +509,33 @@ private void VisitIAppliable(IAppliable fun) public override Expr VisitOldExpr(OldExpr node) { - // TODO: implement throw new LeanConversionException("Unsupported: OldExpr"); } public override Type VisitFloatType(FloatType node) { - // TODO: implement (but low priority) throw new LeanConversionException("Unsupported: FloatType"); } public override Requires VisitRequires(Requires requires) { - return requires; // TODO: do something with it + return requires; // Already inlined } public override Ensures VisitEnsures(Ensures ensures) { - return ensures; // TODO: do something with it + return ensures; // Already inlined } public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) { - return node; // TODO: do something + Console.WriteLine($"DeclWithFormals: {node}"); + return node; // TODO: do something? } public override Type VisitBvTypeProxy(BvTypeProxy node) { - // TODO: implement + // TODO: confirm that this is unreachable throw new LeanConversionException($"Unsupported: bvtypeproxy: {node}"); } @@ -401,17 +553,17 @@ public override Cmd VisitCommentCmd(CommentCmd node) public override List VisitRequiresSeq(List requiresSeq) { - return requiresSeq; // TODO: do something + return requiresSeq; // Already inlined } public override List VisitEnsuresSeq(List ensuresSeq) { - return ensuresSeq; // TODO: do something + return ensuresSeq; // Already inlined } public override Type VisitMapTypeProxy(MapTypeProxy node) { - // TODO: implement + // TODO: confirm that this is unreachable throw new LeanConversionException($"Unsupported: maptypeproxy: {node}"); } @@ -423,26 +575,61 @@ public override QKeyValue VisitQKeyValue(QKeyValue node) public override Declaration VisitTypeCtorDecl(TypeCtorDecl node) { - // TODO: implement - throw new LeanConversionException($"Unsupported: typectordecl: {node}"); + // TODO: wrap in `mutual ... end` when necessary + if (node is DatatypeTypeCtorDecl dt) { + writer.WriteLine($"inductive {SanitizeNameForLean(dt.Name)} where"); + foreach (var ctor in dt.Constructors) { + Indent(1, $"| {SanitizeNameForLean(ctor.Name)} : "); + ctor.InParams.ForEach(p => + { + Visit(p.TypedIdent.Type); + writer.Write(" → "); + }); + writer.WriteLine($" {SanitizeNameForLean(dt.Name)}"); + } + } else { + var name = Name(node); + var tyStr = String.Join(" → ", Enumerable.Repeat("Type", node.Arity + 1).ToList()); + writer.WriteLine($"axiom {name} : {tyStr}"); + + if(node.Arity == 0) { + writer.WriteLine($"instance {name}BEq : BEq {name} := by sorry"); + } + } + return node; } public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) { - // TODO: implement - throw new LeanConversionException($"Unsupported: typesynonymannotation: {node}"); + return VisitType(node.ExpandedType); } public override Declaration VisitTypeSynonymDecl(TypeSynonymDecl node) { - // TODO: implement - throw new LeanConversionException($"Unsupported: typesynonymdecl: {node}"); + var name = Name(node); + writer.Write($"def {name}"); + node.TypeParameters.ForEach(tp => writer.Write($" ({SanitizeNameForLean(tp.Name)} : Type)")); + writer.Write(" := "); + Visit(node.Body); + NL(); + return node; } public override Type VisitTypeProxy(TypeProxy node) { - // TODO: implement - throw new LeanConversionException($"Unsupported: typeproxy: {node}"); + var p = node.ProxyFor; + if (p is null) { + writer.Write(SanitizeNameForLean(node.Name)); + } else { + VisitType(p); + } + return node; + } + + public override Type VisitTypeVariable(TypeVariable node) + { + writer.Write(SanitizeNameForLean(node.Name)); + return node; } public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) @@ -484,21 +671,26 @@ public override Axiom VisitAxiom(Axiom node) // This will take two more steps: // * A named lemma with a definition of `by sorry` (using a `name` attribute?) (or `id`, so it's also useful for proof dependencies?) // * A named lemma that's defined by a call to a previously-defined proof of the same thing - var name = $"ax_l{node.tok.line}c{node.tok.col}"; + int n = 0; + var name = $"ax_l{node.tok.line}c{node.tok.col}_{n}"; + while (userAxiomNames.Contains(name)) { + n += 1; + name = $"ax_l{node.tok.line}c{node.tok.col}_{n}"; + } writer.Write($"axiom {name}: "); VisitExpr(node.Expr); NL(); - axiomNames.Add(name); + userAxiomNames.Add(name); return node; } public override Function VisitFunction(Function node) { // In the long run, this should define functions when possible. - writer.Write($"def {Name(node)} : "); + writer.Write($"axiom {Name(node)} : "); node.InParams.ForEach(x => { - Visit(x.TypedIdent.Type); writer.Write(" -> "); + Visit(x.TypedIdent.Type); writer.Write(" \u2192 "); }); if (node.OutParams.Count == 1) { Visit(node.OutParams[0].TypedIdent.Type); @@ -510,7 +702,7 @@ public override Function VisitFunction(Function node) }); writer.Write(")"); } - writer.WriteLine(" := by sorry"); + NL(); // Note: definition axioms will be emitted later // node.DefinitionAxioms.ForEach(ax => VisitAxiom(ax)); @@ -530,15 +722,15 @@ private string BinaryOpToLean(BinaryOperator.Opcode op) BinaryOperator.Opcode.Gt => ">", BinaryOperator.Opcode.Le => "<=", BinaryOperator.Opcode.Ge => ">=", - BinaryOperator.Opcode.Eq => "=", + BinaryOperator.Opcode.Eq => "==", BinaryOperator.Opcode.Neq => "!=", - BinaryOperator.Opcode.And => "\u2227", - BinaryOperator.Opcode.Or => "||", + BinaryOperator.Opcode.And => "\u2227", /* ∧ */ + BinaryOperator.Opcode.Or => "\u2228", /* ∨ */ BinaryOperator.Opcode.Iff => "=", - BinaryOperator.Opcode.Imp => "->", - BinaryOperator.Opcode.Pow => "TODO", - BinaryOperator.Opcode.FloatDiv => "TODO", - BinaryOperator.Opcode.RealDiv => "TODO", + BinaryOperator.Opcode.Imp => "\u2192", /* → */ + BinaryOperator.Opcode.Pow => "^", + BinaryOperator.Opcode.RealDiv => "/", + BinaryOperator.Opcode.FloatDiv => "/", _ => throw new LeanConversionException($"unsupported binary operator: {op.ToString()}") }; } @@ -555,7 +747,10 @@ private string UnaryOpToLean(UnaryOperator.Opcode op) private string SanitizeNameForLean(string name) { - return name.Replace('@', '_'); + return name + .Replace('@', '_') + .Replace('#', '_') + .Replace("$", "_dollar_"); } private string Name(NamedDeclaration d) @@ -563,6 +758,11 @@ private string Name(NamedDeclaration d) return SanitizeNameForLean(d.Name); } + private string BlockName(Block b) + { + return "β_" + SanitizeNameForLean(b.Label); + } + public override Procedure VisitProcedure(Procedure node) { return node; @@ -593,6 +793,7 @@ private void WriteParams(Implementation node) public override Implementation VisitImplementation(Implementation node) { var name = Name(node); + var entryLabel = BlockName(node.Blocks[0]); NL(); writer.WriteLine($"namespace impl_{name}"); @@ -601,25 +802,30 @@ public override Implementation VisitImplementation(Implementation node) writer.WriteLine("@[simp]"); writer.WriteLine($"def {name}"); WriteParams(node); - IndentL(1, $": Prop := {node.Blocks[0].Label}"); + IndentL(1, $": Prop := {entryLabel}"); IndentL(1, "where"); node.Blocks.ForEach(b => VisitBlock(b)); NL(); writer.WriteLine($"theorem {name}_correct"); WriteParams(node); var paramNames = - globalVars.Select(Name) + globalVars.Select(Name).Where(x => usedNames.Contains(x)) .Concat(node.InParams.Select(Name)) .Concat(node.OutParams.Select(Name)) .Concat(node.LocVars.Select(Name)); var paramString = String.Join(' ', paramNames); Indent(1, $": {name} {paramString} := by"); NL(); - IndentL(2, "simp"); - IndentL(2, "auto"); + IndentL(2, "try simp"); // Uses `try` because it may make no progress + IndentL(2, "try auto"); // Uses `try` because there may be no goals remaining + var axiomNames = usesMaps ? mapAxiomNames.Concat(userAxiomNames) : userAxiomNames; Indent(3); List(axiomNames); NL(); IndentL(3, "u[]"); NL(); - writer.WriteLine($"end impl_{name}"); NL(); + writer.WriteLine($"end impl_{name}"); + + usesMaps = false; // Skip map axioms in the next implementation if it doesn't need them + usedNames.Clear(); // Skip any globals not used by the next implementation + return node; } @@ -675,11 +881,6 @@ public override LocalVariable VisitLocalVariable(LocalVariable node) throw new LeanConversionException($"Internal error: LocalVariable should never be directly visited {node.tok}"); } - public override Type VisitTypeVariable(TypeVariable node) - { - throw new LeanConversionException($"Internal: TypeVariable should never be directly visited {node.tok}"); - } - public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node) { throw new LeanConversionException($"Internal: UnresolvedTypeIdentifier should never appear ({node.tok})"); From e4c34dc4ef907496b30a3e761ecaf333f0d8e376 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 22 Dec 2023 09:51:33 -0800 Subject: [PATCH 07/30] Successfully process trivial Dafny program When using the version of the prelude that uses a monomorphic heap, and turning on pruning, Lean can prove correctness of a trivial Dafny program. --- Source/ExecutionEngine/ExecutionEngine.cs | 3 +- Source/Provers/LeanAuto/LeanAuto.cs | 67 +++++++++++++++++------ Source/Provers/LeanAuto/LeanAuto.csproj | 1 + 3 files changed, 52 insertions(+), 19 deletions(-) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 8094e9a19..661ad4a15 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -13,6 +13,7 @@ using System.Reactive.Subjects; using System.Reactive.Threading.Tasks; using Microsoft.Boogie.LeanAuto; +using Microsoft.Boogie.VCExprAST; using VCGeneration; namespace Microsoft.Boogie @@ -577,7 +578,7 @@ public async Task InferAndVerify( if (Options.LeanFile is not null) { var writer = new StreamWriter(Options.LeanFile); - LeanGenerator.EmitPassiveProgramAsLean(processedProgram.Program, writer); + LeanGenerator.EmitPassiveProgramAsLean(Options, processedProgram.Program, writer); writer.Close(); } diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index ffe098fa6..efa9020be 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -14,7 +14,7 @@ public class LeanGenerator : ReadOnlyVisitor private readonly List mapAxiomNames = new(new[] { - "SelectStoreSame", "SelectStoreDistinct", + "SelectStoreSame1", "SelectStoreDistinct1", "SelectStoreSame2", "SelectStoreDistinct2" }); private readonly List userAxiomNames = new(); @@ -22,7 +22,8 @@ public class LeanGenerator : ReadOnlyVisitor private readonly string header = @"import Auto import Auto.Tactic -open Lean Std +import Auto.MathlibEmulator.Basic -- For `Real` +open Lean Std Auto set_option linter.unusedVariables false set_option auto.smt true @@ -54,10 +55,10 @@ def store2 [BEq s1] [BEq s2] (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (v: s3): SM def select2 (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2): s3 := m i j -axiom SelectStoreSame (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (e: s2): +axiom SelectStoreSame1 (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (e: s2): select1 (store1 a i e) i = e -axiom SelectStoreDistinct (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (j: s1) (e: s2): +axiom SelectStoreDistinct1 (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (j: s1) (e: s2): i ≠ j → select1 (store1 a i e) j = select1 a j axiom SelectStoreSame2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (e: s3): @@ -68,6 +69,10 @@ axiom SelectStoreDistinct2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s -- TODO: provide either a definition or some functional axioms (or a definition plus some lemmas) axiom distinct : {a : Type} → List a → Prop + +axiom realToInt : Real → Int +axiom intToReal : Int → Real +instance BEqReal: BEq Real := by sorry "; private LeanGenerator(TextWriter writer) @@ -75,21 +80,25 @@ private LeanGenerator(TextWriter writer) this.writer = writer; } - public static void EmitPassiveProgramAsLean(Program p, TextWriter writer) + public static void EmitPassiveProgramAsLean(VCGenOptions options, Program p, TextWriter writer) { var generator = new LeanGenerator(writer); generator.EmitHeader(); try { + var allBlocks = p.Implementations.SelectMany(i => i.Blocks); + var liveDeclarations = Prune.GetLiveDeclarations(options, p, allBlocks.ToList()); + generator.writer.WriteLine("-- Type constructors"); + // Include all type constructors p.TopLevelDeclarations.OfType().ForEach(tcd => generator.Visit(tcd)); generator.NL(); generator.writer.WriteLine("-- Type synonyms"); - p.TopLevelDeclarations.OfType().ForEach(tcd => generator.Visit(tcd)); + liveDeclarations.OfType().ForEach(tcd => generator.Visit(tcd)); generator.NL(); generator.writer.WriteLine("-- Constants"); - p.Constants.ForEach(c => generator.Visit(c)); + liveDeclarations.OfType().ForEach(c => generator.Visit(c)); generator.NL(); generator.writer.WriteLine("-- Unique const axioms"); @@ -97,15 +106,15 @@ public static void EmitPassiveProgramAsLean(Program p, TextWriter writer) generator.NL(); generator.writer.WriteLine("-- Variables"); - p.GlobalVariables.ForEach(gv => generator.Visit(gv)); + liveDeclarations.OfType().ForEach(gv => generator.Visit(gv)); generator.NL(); generator.writer.WriteLine("-- Functions"); - p.Functions.ForEach(f => generator.Visit(f)); + liveDeclarations.OfType().ForEach(f => generator.Visit(f)); generator.NL(); generator.writer.WriteLine("-- Axioms"); - p.Axioms.ForEach(a => generator.Visit(a)); + liveDeclarations.OfType().ForEach(a => generator.Visit(a)); generator.NL(); generator.writer.WriteLine("-- Implementations"); @@ -254,7 +263,7 @@ public override Type VisitType(Type node) public override Type VisitBasicType(BasicType node) { if (node.IsBool) { - writer.Write("Bool"); + writer.Write("Prop"); } else if (node.IsInt) { writer.Write("Int"); } else if (node.IsReal) { @@ -452,8 +461,10 @@ public override Expr VisitNAryExpr(NAryExpr node) writer.Write(" else "); Visit(args[2]); } else if (fun is TypeCoercion typeCoercion && args.Count == 1) { - // TODO: might need to actually call a coercion function - Console.WriteLine($"Coerce: {args[0].Type} -> {typeCoercion.Type}"); + if (!args[0].Type.Equals(typeCoercion.Type)) { + // TODO: might need to actually call a coercion function + Console.WriteLine($"Coerce: {args[0].Type} -> {typeCoercion.Type}"); + } writer.Write("("); Visit(args[0]); writer.Write(" : "); @@ -502,6 +513,15 @@ private void VisitIAppliable(IAppliable fun) // TODO: declare these discriminator functions writer.Write($"is_{SanitizeNameForLean(isConstructor.ConstructorName)}"); break; + case ArithmeticCoercion arithmeticCoercion: + var func = arithmeticCoercion.Coercion switch + { + ArithmeticCoercion.CoercionType.ToInt => "realToInt", + ArithmeticCoercion.CoercionType.ToReal => "intToReal", + _ => throw new LeanConversionException($"Internal: unknown arithmetic coercion: {arithmeticCoercion.Coercion}") + }; + writer.Write(func); + break; default: throw new LeanConversionException($"Unsupported: IAppliable: {fun}"); } @@ -688,9 +708,18 @@ public override Function VisitFunction(Function node) { // In the long run, this should define functions when possible. writer.Write($"axiom {Name(node)} : "); + node.TypeParameters.ForEach(x => + { + var name = SanitizeNameForLean(x.Name); + writer.Write($"{{{name} : Type}}"); + writer.Write(" \u2192 "); + //writer.Write($"[BEq {name}]"); + //writer.Write(" \u2192 "); + }); node.InParams.ForEach(x => { - Visit(x.TypedIdent.Type); writer.Write(" \u2192 "); + Visit(x.TypedIdent.Type); + writer.Write(" \u2192 "); }); if (node.OutParams.Count == 1) { Visit(node.OutParams[0].TypedIdent.Type); @@ -722,8 +751,8 @@ private string BinaryOpToLean(BinaryOperator.Opcode op) BinaryOperator.Opcode.Gt => ">", BinaryOperator.Opcode.Le => "<=", BinaryOperator.Opcode.Ge => ">=", - BinaryOperator.Opcode.Eq => "==", - BinaryOperator.Opcode.Neq => "!=", + BinaryOperator.Opcode.Eq => "=", + BinaryOperator.Opcode.Neq => "\u2260", /* ≠ */ BinaryOperator.Opcode.And => "\u2227", /* ∧ */ BinaryOperator.Opcode.Or => "\u2228", /* ∨ */ BinaryOperator.Opcode.Iff => "=", @@ -739,7 +768,7 @@ private string UnaryOpToLean(UnaryOperator.Opcode op) { return op switch { - UnaryOperator.Opcode.Not => "!", + UnaryOperator.Opcode.Not => "Not", UnaryOperator.Opcode.Neg => "-", _ => throw new LeanConversionException($"unsupported unary operator: {op.ToString()}") }; @@ -747,8 +776,9 @@ private string UnaryOpToLean(UnaryOperator.Opcode op) private string SanitizeNameForLean(string name) { - return name + return "_boogie_" + name .Replace('@', '_') + .Replace('.', '_') .Replace('#', '_') .Replace("$", "_dollar_"); } @@ -795,6 +825,7 @@ public override Implementation VisitImplementation(Implementation node) var name = Name(node); var entryLabel = BlockName(node.Blocks[0]); + usedNames.Clear(); // Skip any globals used only by axioms, etc. NL(); writer.WriteLine($"namespace impl_{name}"); NL(); diff --git a/Source/Provers/LeanAuto/LeanAuto.csproj b/Source/Provers/LeanAuto/LeanAuto.csproj index 1c541a93b..dd35d8d18 100644 --- a/Source/Provers/LeanAuto/LeanAuto.csproj +++ b/Source/Provers/LeanAuto/LeanAuto.csproj @@ -9,6 +9,7 @@ + From 2556b26827a7f7b056f3134508e5ae2c93a34856 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 22 Dec 2023 12:01:19 -0800 Subject: [PATCH 08/30] Cleanups --- Source/Provers/LeanAuto/LeanAuto.cs | 285 +++++++++++++++------------- 1 file changed, 149 insertions(+), 136 deletions(-) diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index efa9020be..372411ecb 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -8,6 +8,7 @@ namespace Microsoft.Boogie.LeanAuto; public class LeanGenerator : ReadOnlyVisitor { private readonly TextWriter writer; + private readonly VCGenOptions options; private readonly List globalVars = new(); private readonly HashSet usedNames = new(); private bool usesMaps; @@ -18,7 +19,7 @@ public class LeanGenerator : ReadOnlyVisitor "SelectStoreSame2", "SelectStoreDistinct2" }); private readonly List userAxiomNames = new(); - private Dictionary> uniqueConsts = new(); + private readonly Dictionary> uniqueConsts = new(); private readonly string header = @"import Auto import Auto.Tactic @@ -28,9 +29,8 @@ open Lean Std Auto set_option linter.unusedVariables false set_option auto.smt true set_option trace.auto.smt.printCommands false ---set_option auto.smt.proof false +set_option trace.auto.smt.result true set_option auto.smt.trust true ---set_option auto.duper false set_option auto.smt.solver.name ""z3"" set_option trace.auto.buildChecker false @@ -75,49 +75,53 @@ axiom SelectStoreDistinct2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s instance BEqReal: BEq Real := by sorry "; - private LeanGenerator(TextWriter writer) + private LeanGenerator(VCGenOptions options, TextWriter writer) { + this.options = options; this.writer = writer; } public static void EmitPassiveProgramAsLean(VCGenOptions options, Program p, TextWriter writer) { - var generator = new LeanGenerator(writer); + var generator = new LeanGenerator(options, writer); generator.EmitHeader(); try { var allBlocks = p.Implementations.SelectMany(i => i.Blocks); - var liveDeclarations = Prune.GetLiveDeclarations(options, p, allBlocks.ToList()); - - generator.writer.WriteLine("-- Type constructors"); - // Include all type constructors + var liveDeclarations = + options.Prune + ? Prune.GetLiveDeclarations(options, p, allBlocks.ToList()).ToList() + : p.TopLevelDeclarations; + + generator.Line("-- Type constructors"); + // Always include all type constructors p.TopLevelDeclarations.OfType().ForEach(tcd => generator.Visit(tcd)); generator.NL(); - generator.writer.WriteLine("-- Type synonyms"); + generator.Line("-- Type synonyms"); liveDeclarations.OfType().ForEach(tcd => generator.Visit(tcd)); generator.NL(); - generator.writer.WriteLine("-- Constants"); + generator.Line("-- Constants"); liveDeclarations.OfType().ForEach(c => generator.Visit(c)); generator.NL(); - generator.writer.WriteLine("-- Unique const axioms"); + generator.Line("-- Unique const axioms"); generator.EmitUniqueConstAxioms(); generator.NL(); - generator.writer.WriteLine("-- Variables"); + generator.Line("-- Variables"); liveDeclarations.OfType().ForEach(gv => generator.Visit(gv)); generator.NL(); - generator.writer.WriteLine("-- Functions"); + generator.Line("-- Functions"); liveDeclarations.OfType().ForEach(f => generator.Visit(f)); generator.NL(); - generator.writer.WriteLine("-- Axioms"); + generator.Line("-- Axioms"); liveDeclarations.OfType().ForEach(a => generator.Visit(a)); generator.NL(); - generator.writer.WriteLine("-- Implementations"); + generator.Line("-- Implementations"); p.Implementations.ForEach(i => generator.Visit(i)); } catch (LeanConversionException e) { Console.WriteLine($"Failed translation: {e.Msg}"); @@ -140,7 +144,7 @@ private void EmitUniqueConstAxioms() foreach (var kv in uniqueConsts) { var axiomName = $"unique{i}"; userAxiomNames.Add(axiomName); - writer.Write($"axiom {axiomName}: distinct "); + Text($"axiom {axiomName}: distinct "); List(kv.Value); NL(); i++; @@ -155,11 +159,11 @@ private void EmitHeader() private void Indent(int n = 1, string str = null) { for (var i = 0; i < n; i++) { - writer.Write(" "); + Text(" "); } if (str is not null) { - writer.Write(str); + Text(str); } } @@ -174,11 +178,21 @@ private void NL() writer.WriteLine(); } + private void Text(string text) + { + writer.Write(text); + } + + private void Line(string text) + { + writer.WriteLine(text); + } + private void List(IEnumerable strings) { - writer.Write("["); - writer.Write(String.Join(", ", strings)); - writer.Write("]"); + Text("["); + Text(String.Join(", ", strings)); + Text("]"); } public override Block VisitBlock(Block node) @@ -201,7 +215,7 @@ public override Cmd VisitAssertCmd(AssertCmd node) { Indent(2, "assert "); VisitExpr(node.Expr); - writer.WriteLine(" $"); + Line(" $"); return node; } @@ -209,7 +223,7 @@ public override Cmd VisitAssumeCmd(AssumeCmd node) { Indent(2, "assume "); VisitExpr(node.Expr); - writer.WriteLine(" $"); + Line(" $"); return node; } @@ -231,43 +245,35 @@ public override Expr VisitIdentifierExpr(IdentifierExpr node) { var name = SanitizeNameForLean(node.Name); usedNames.Add(name); - writer.Write(name); + Text(name); return node; } public override Type VisitType(Type node) { - if (node is BasicType basicType) { - return VisitBasicType(basicType); - } else if (node is BvType bvType) { - return VisitBvType(bvType); - } else if (node is CtorType ctorType) { - return VisitCtorType(ctorType); - } else if (node is FloatType floatType) { - return VisitFloatType(floatType); - } else if (node is MapType mapType) { - return VisitMapType(mapType); - } else if (node is TypeProxy typeProxy) { - return VisitTypeProxy(typeProxy); - } else if (node is TypeSynonymAnnotation typeSynonymAnnotation) { - return VisitTypeSynonymAnnotation(typeSynonymAnnotation); - } else if (node is TypeVariable typeVariable) { - return VisitTypeVariable(typeVariable); - } else if (node is UnresolvedTypeIdentifier uti) { - return VisitUnresolvedTypeIdentifier(uti); - } else { - throw new LeanConversionException("Unreachable type case."); - } + return node switch + { + BasicType basicType => VisitBasicType(basicType), + BvType bvType => VisitBvType(bvType), + CtorType ctorType => VisitCtorType(ctorType), + FloatType floatType => VisitFloatType(floatType), + MapType mapType => VisitMapType(mapType), + TypeProxy typeProxy => VisitTypeProxy(typeProxy), + TypeSynonymAnnotation typeSynonymAnnotation => VisitTypeSynonymAnnotation(typeSynonymAnnotation), + TypeVariable typeVariable => VisitTypeVariable(typeVariable), + UnresolvedTypeIdentifier uti => VisitUnresolvedTypeIdentifier(uti), + _ => throw new LeanConversionException("Unreachable type case.") + }; } public override Type VisitBasicType(BasicType node) { if (node.IsBool) { - writer.Write("Prop"); + Text("Prop"); } else if (node.IsInt) { - writer.Write("Int"); + Text("Int"); } else if (node.IsReal) { - writer.Write("Real"); + Text("Real"); } else if (node.IsRMode) { throw new LeanConversionException("Unsupported: RMode type"); } else if (node.IsRegEx) { @@ -285,24 +291,24 @@ public override Type VisitBasicType(BasicType node) public override Expr VisitBvConcatExpr(BvConcatExpr node) { Visit(node.E0); - writer.Write(" ++ "); + Text(" ++ "); Visit(node.E1); return node; } public override Type VisitBvType(BvType node) { - writer.Write($"(BitVec {node.Bits})"); + Text($"(BitVec {node.Bits})"); return node; } public override Constant VisitConstant(Constant node) { var ti = node.TypedIdent; - writer.Write("variable "); + Text("variable "); Visit(ti); if (node.Unique) { - AddUniqueConst(ti.Type, SanitizeNameForLean(ti.Name)); + AddUniqueConst(ti.Type, Name(node)); } NL(); globalVars.Add(node); @@ -312,17 +318,17 @@ public override Constant VisitConstant(Constant node) public override CtorType VisitCtorType(CtorType node) { if (node.Arguments.Any()) { - writer.Write("("); + Text("("); } - writer.Write(Name(node.Decl)); + Text(Name(node.Decl)); node.Arguments.ForEach(a => { - writer.Write(" "); + Text(" "); Visit(a); }); if (node.Arguments.Any()) { - writer.Write(")"); + Text(")"); } return node; } @@ -335,48 +341,48 @@ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) ExistsExpr => "exists", _ => throw new LeanConversionException($"Unsupported quantifier type: {node.Kind}") }; - writer.Write($"({kind}"); + Text($"({kind}"); foreach (var tv in node.TypeParameters) { - writer.Write($" ({SanitizeNameForLean(tv.Name)} : Type)"); + Text($" ({Name(tv)} : Type)"); } foreach (var x in node.Dummies) { - writer.Write(" "); + Text(" "); VisitTypedIdent(x.TypedIdent); } - writer.Write(", "); + Text(", "); Visit(node.Body); - writer.Write(")"); + Text(")"); return node; } public override TypedIdent VisitTypedIdent(TypedIdent node) { - writer.Write("("); + Text("("); var name = SanitizeNameForLean(node.Name); - writer.Write(name); - writer.Write(" : "); + Text(name); + Text(" : "); Visit(node.Type); - writer.Write(")"); + Text(")"); return node; } public override Expr VisitBvExtractExpr(BvExtractExpr node) { // TODO: double-check range values - writer.Write($"(BitVec.extractLsb {node.End - 1} {node.Start} "); + Text($"(BitVec.extractLsb {node.End - 1} {node.Start} "); Visit(node.Bitvector); - writer.Write(")"); + Text(")"); return node; } public override Expr VisitLambdaExpr(LambdaExpr node) { - writer.Write("(λ"); + Text("(λ"); node.Dummies.ForEach(x => Visit(x.TypedIdent)); - writer.Write("=>"); + Text("=>"); Visit(node.Body); - writer.Write(")"); + Text(")"); return node; } @@ -385,19 +391,19 @@ public override Expr VisitLetExpr(LetExpr node) if (node.Dummies.Count > 1) { throw new LeanConversionException("Unsupported: LetExpr with more than one binder"); } - writer.Write("(let"); + Text("(let"); node.Dummies.ForEach(x => Visit(x.TypedIdent)); - writer.Write(" := "); + Text(" := "); node.Rhss.ForEach(e => Visit(e)); - writer.Write("; "); + Text("; "); Visit(node.Body); - writer.Write(")"); + Text(")"); return node; } public override GlobalVariable VisitGlobalVariable(GlobalVariable node) { - writer.Write("variable "); + Text("variable "); Visit(node.TypedIdent); NL(); globalVars.Add(node); @@ -408,18 +414,18 @@ public override Expr VisitLiteralExpr(LiteralExpr node) { if(node.IsTrue) { // Use lowercase version to ensure Bool, which can be coerced to Prop - writer.Write("true"); + Text("true"); } else if (node.IsFalse) { // Use lowercase version to ensure Bool, which can be coerced to Prop - writer.Write("false"); + Text("false"); } else if (node.isBvConst) { var bvConst = node.asBvConst; - writer.Write("("); - writer.Write(bvConst.Value); - writer.Write($" : BitVec {bvConst.Bits}"); - writer.Write(")"); + Text("("); + Text(bvConst.Value.ToString()); + Text($" : BitVec {bvConst.Bits}"); + Text(")"); } else { - writer.Write(node); // TODO: make sure this is right for all other literal types + Text(node.ToString()); // TODO: make sure this is right for all other literal types } return node; } @@ -430,17 +436,17 @@ public override Type VisitMapType(MapType node) throw new LeanConversionException($"Unsupported: MapType with too many index types ({node})"); } if (node.TypeParameters.Any()) { - var args = node.TypeParameters.Select(a => SanitizeNameForLean(a.Name)); - writer.Write($"forall ({String.Join(" ", args)} : Type), "); + var args = node.TypeParameters.Select(Name); + Text($"forall ({String.Join(" ", args)} : Type), "); } - writer.Write($"(SMTArray{node.Arguments.Count} "); + Text($"(SMTArray{node.Arguments.Count} "); node.Arguments.ForEach(a => { Visit(a); - writer.Write(" "); + Text(" "); }); Visit(node.Result); - writer.Write(")"); + Text(")"); return node; } @@ -448,43 +454,43 @@ public override Expr VisitNAryExpr(NAryExpr node) { var fun = node.Fun; var args = node.Args; - writer.Write("("); + Text("("); if (fun is BinaryOperator op && args.Count == 2) { Visit(args[0]); - writer.Write($" {BinaryOpToLean(op.Op)} "); + Text($" {BinaryOpToLean(op.Op)} "); Visit(args[1]); } else if (fun is IfThenElse && args.Count == 3) { - writer.Write("if "); + Text("if "); Visit(args[0]); - writer.Write(" then "); + Text(" then "); Visit(args[1]); - writer.Write(" else "); + Text(" else "); Visit(args[2]); } else if (fun is TypeCoercion typeCoercion && args.Count == 1) { if (!args[0].Type.Equals(typeCoercion.Type)) { // TODO: might need to actually call a coercion function Console.WriteLine($"Coerce: {args[0].Type} -> {typeCoercion.Type}"); } - writer.Write("("); + Text("("); Visit(args[0]); - writer.Write(" : "); + Text(" : "); Visit(typeCoercion.Type); - writer.Write(")"); + Text(")"); } else if (fun is FieldAccess fieldAccess) { throw new LeanConversionException("Unsupported: field access (since the semantics are complex)"); // TODO: implement /* Visit(args[0]); - writer.Write($".{SanitizeNameForLean(fieldAccess.FieldName)}"); + Text($".{SanitizeNameForLean(fieldAccess.FieldName)}"); */ } else { VisitIAppliable(fun); foreach (var arg in args) { - writer.Write(" "); + Text(" "); Visit(arg); } } - writer.Write(")"); + Text(")"); return node; } @@ -494,24 +500,24 @@ private void VisitIAppliable(IAppliable fun) switch (fun) { case MapSelect: usesMaps = true; - writer.Write($"select{fun.ArgumentCount - 1}"); + Text($"select{fun.ArgumentCount - 1}"); break; case MapStore: usesMaps = true; - writer.Write($"store{fun.ArgumentCount - 2}"); + Text($"store{fun.ArgumentCount - 2}"); break; case BinaryOperator op: - writer.Write(BinaryOpToLean(op.Op)); + Text(BinaryOpToLean(op.Op)); break; case UnaryOperator op: - writer.Write(UnaryOpToLean(op.Op)); + Text(UnaryOpToLean(op.Op)); break; case FunctionCall fc: - writer.Write(SanitizeNameForLean(fc.Func.Name)); + Text(Name(fc.Func)); break; case IsConstructor isConstructor: // TODO: declare these discriminator functions - writer.Write($"is_{SanitizeNameForLean(isConstructor.ConstructorName)}"); + Text($"is_{SanitizeNameForLean(isConstructor.ConstructorName)}"); break; case ArithmeticCoercion arithmeticCoercion: var func = arithmeticCoercion.Coercion switch @@ -520,7 +526,7 @@ private void VisitIAppliable(IAppliable fun) ArithmeticCoercion.CoercionType.ToReal => "intToReal", _ => throw new LeanConversionException($"Internal: unknown arithmetic coercion: {arithmeticCoercion.Coercion}") }; - writer.Write(func); + Text(func); break; default: throw new LeanConversionException($"Unsupported: IAppliable: {fun}"); @@ -596,24 +602,24 @@ public override QKeyValue VisitQKeyValue(QKeyValue node) public override Declaration VisitTypeCtorDecl(TypeCtorDecl node) { // TODO: wrap in `mutual ... end` when necessary + var name = Name(node); if (node is DatatypeTypeCtorDecl dt) { - writer.WriteLine($"inductive {SanitizeNameForLean(dt.Name)} where"); + Line($"inductive {name} where"); foreach (var ctor in dt.Constructors) { - Indent(1, $"| {SanitizeNameForLean(ctor.Name)} : "); + Indent(1, $"| {Name(ctor)} : "); ctor.InParams.ForEach(p => { Visit(p.TypedIdent.Type); - writer.Write(" → "); + Text(" → "); }); - writer.WriteLine($" {SanitizeNameForLean(dt.Name)}"); + Line($" {name}"); } } else { - var name = Name(node); var tyStr = String.Join(" → ", Enumerable.Repeat("Type", node.Arity + 1).ToList()); - writer.WriteLine($"axiom {name} : {tyStr}"); + Line($"axiom {name} : {tyStr}"); if(node.Arity == 0) { - writer.WriteLine($"instance {name}BEq : BEq {name} := by sorry"); + Line($"instance {name}BEq : BEq {name} := by sorry"); } } return node; @@ -627,9 +633,9 @@ public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) public override Declaration VisitTypeSynonymDecl(TypeSynonymDecl node) { var name = Name(node); - writer.Write($"def {name}"); - node.TypeParameters.ForEach(tp => writer.Write($" ({SanitizeNameForLean(tp.Name)} : Type)")); - writer.Write(" := "); + Text($"def {name}"); + node.TypeParameters.ForEach(tp => Text($" ({Name(tp)} : Type)")); + Text(" := "); Visit(node.Body); NL(); return node; @@ -639,7 +645,7 @@ public override Type VisitTypeProxy(TypeProxy node) { var p = node.ProxyFor; if (p is null) { - writer.Write(SanitizeNameForLean(node.Name)); + Text(Name(node)); } else { VisitType(p); } @@ -648,7 +654,7 @@ public override Type VisitTypeProxy(TypeProxy node) public override Type VisitTypeVariable(TypeVariable node) { - writer.Write(SanitizeNameForLean(node.Name)); + Text(Name(node)); return node; } @@ -656,7 +662,7 @@ public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) { Indent(2, "assert "); VisitExpr(node.Expr); - writer.WriteLine(" $"); + Line(" $"); return node; } @@ -664,7 +670,7 @@ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) { Indent(2, "assert "); VisitExpr(node.Expr); - writer.WriteLine(" $"); + Line(" $"); return node; } @@ -697,7 +703,7 @@ public override Axiom VisitAxiom(Axiom node) n += 1; name = $"ax_l{node.tok.line}c{node.tok.col}_{n}"; } - writer.Write($"axiom {name}: "); + Text($"axiom {name}: "); VisitExpr(node.Expr); NL(); userAxiomNames.Add(name); @@ -707,29 +713,26 @@ public override Axiom VisitAxiom(Axiom node) public override Function VisitFunction(Function node) { // In the long run, this should define functions when possible. - writer.Write($"axiom {Name(node)} : "); + Text($"axiom {Name(node)} : "); node.TypeParameters.ForEach(x => { - var name = SanitizeNameForLean(x.Name); - writer.Write($"{{{name} : Type}}"); - writer.Write(" \u2192 "); - //writer.Write($"[BEq {name}]"); - //writer.Write(" \u2192 "); + Text($"{{{Name(x)} : Type}}"); + Text(" \u2192 "); }); node.InParams.ForEach(x => { Visit(x.TypedIdent.Type); - writer.Write(" \u2192 "); + Text(" \u2192 "); }); if (node.OutParams.Count == 1) { Visit(node.OutParams[0].TypedIdent.Type); } else { - writer.Write("("); + Text("("); node.OutParams.ForEach(x => { - Visit(x.TypedIdent.Type); writer.Write(", "); + Visit(x.TypedIdent.Type); Text(", "); }); - writer.Write(")"); + Text(")"); } NL(); @@ -788,6 +791,16 @@ private string Name(NamedDeclaration d) return SanitizeNameForLean(d.Name); } + private string Name(TypeVariable tv) + { + return SanitizeNameForLean(tv.Name); + } + + private string Name(TypeProxy tp) + { + return SanitizeNameForLean(tp.Name); + } + private string BlockName(Block b) { return "β_" + SanitizeNameForLean(b.Label); @@ -827,17 +840,17 @@ public override Implementation VisitImplementation(Implementation node) usedNames.Clear(); // Skip any globals used only by axioms, etc. NL(); - writer.WriteLine($"namespace impl_{name}"); + Line($"namespace impl_{name}"); NL(); - writer.WriteLine("@[simp]"); - writer.WriteLine($"def {name}"); + Line("@[simp]"); + Line($"def {name}"); WriteParams(node); IndentL(1, $": Prop := {entryLabel}"); IndentL(1, "where"); node.Blocks.ForEach(b => VisitBlock(b)); NL(); - writer.WriteLine($"theorem {name}_correct"); + Line($"theorem {name}_correct"); WriteParams(node); var paramNames = globalVars.Select(Name).Where(x => usedNames.Contains(x)) @@ -852,7 +865,7 @@ public override Implementation VisitImplementation(Implementation node) Indent(3); List(axiomNames); NL(); IndentL(3, "u[]"); NL(); - writer.WriteLine($"end impl_{name}"); + Line($"end impl_{name}"); usesMaps = false; // Skip map axioms in the next implementation if it doesn't need them usedNames.Clear(); // Skip any globals not used by the next implementation From 7049b6d9a55e9deca737fdbc19512ec67d16caba Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 13 Feb 2024 10:50:42 -0800 Subject: [PATCH 09/30] Update exception messages --- Source/Provers/LeanAuto/LeanAuto.cs | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index 372411ecb..8d4f902c8 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -877,72 +877,72 @@ public override Implementation VisitImplementation(Implementation node) public override Program VisitProgram(Program node) { - throw new LeanConversionException($"Internal: Program should never be directly visited {node.tok}"); + throw new LeanConversionException($"Internal: Program should never be directly visited ({node.tok})."); } public override Declaration VisitDeclaration(Declaration node) { - throw new LeanConversionException($"Internal: Declaration should never be directly visited {node.tok}"); + throw new LeanConversionException($"Internal: Declaration should never be directly visited ({node.tok})."); } public override List VisitDeclarationList(List declarationList) { - throw new LeanConversionException($"Internal: List should never be directly visited {declarationList}"); + throw new LeanConversionException($"Internal: List should never be directly visited ({declarationList})."); } public override List VisitBlockSeq(List blockSeq) { - throw new LeanConversionException($"Internal: List should never be directly visited {blockSeq}"); + throw new LeanConversionException($"Internal: List should never be directly visited ({blockSeq})."); } public override List VisitBlockList(List blocks) { - throw new LeanConversionException($"Internal: List should never be directly visited {blocks}"); + throw new LeanConversionException($"Internal: List should never be directly visited ({blocks})."); } public override Trigger VisitTrigger(Trigger node) { - throw new LeanConversionException($"Internal: Trigger should never be directly visited {node.tok}"); + throw new LeanConversionException($"Internal: Trigger should never be directly visited ({node.tok})."); } public override IList VisitExprSeq(IList exprSeq) { - throw new LeanConversionException($"Internal: List should never be directly visited {exprSeq}"); + throw new LeanConversionException($"Internal: List should never be directly visited ({exprSeq})."); } public override BoundVariable VisitBoundVariable(BoundVariable node) { - throw new LeanConversionException($"Internal: BoundVariable should never be directly visited {node.tok}"); + throw new LeanConversionException($"Internal: BoundVariable should never be directly visited ({node.tok})."); } public override Formal VisitFormal(Formal node) { - throw new LeanConversionException($"Internal: Formal should never be directly visited {node.tok}"); + throw new LeanConversionException($"Internal: Formal should never be directly visited ({node.tok})."); } public override LocalVariable VisitLocalVariable(LocalVariable node) { - throw new LeanConversionException($"Internal error: LocalVariable should never be directly visited {node.tok}"); + throw new LeanConversionException($"Internal error: LocalVariable should never be directly visited ({node.tok})."); } public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node) { - throw new LeanConversionException($"Internal: UnresolvedTypeIdentifier should never appear ({node.tok})"); + throw new LeanConversionException($"Internal: UnresolvedTypeIdentifier should never appear ({node.tok})."); } public override Variable VisitVariable(Variable node) { - throw new LeanConversionException($"Internal: Variable should never be directly visited {node.tok}"); + throw new LeanConversionException($"Internal: Variable should never be directly visited ({node.tok})."); } public override List VisitVariableSeq(List variableSeq) { - throw new LeanConversionException($"Internal: List should never be directly visited {variableSeq}"); + throw new LeanConversionException($"Internal: List should never be directly visited ({variableSeq})."); } public override HashSet VisitVariableSet(HashSet node) { - throw new LeanConversionException($"Internal: HashSet should never be directly visited {node}"); + throw new LeanConversionException($"Internal: HashSet should never be directly visited ({node})."); } public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) From b2c5b143e891741f86823895aa467e4f779b3e81 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 13 Feb 2024 10:50:52 -0800 Subject: [PATCH 10/30] Move prelude to external file --- Source/Provers/LeanAuto/LeanAuto.cs | 61 +++---------------------- Source/Provers/LeanAuto/LeanAuto.csproj | 6 +++ Source/Provers/LeanAuto/Prelude.lean | 52 +++++++++++++++++++++ 3 files changed, 65 insertions(+), 54 deletions(-) create mode 100644 Source/Provers/LeanAuto/Prelude.lean diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index 8d4f902c8..a629b1775 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -21,60 +21,6 @@ public class LeanGenerator : ReadOnlyVisitor private readonly List userAxiomNames = new(); private readonly Dictionary> uniqueConsts = new(); - private readonly string header = @"import Auto -import Auto.Tactic -import Auto.MathlibEmulator.Basic -- For `Real` -open Lean Std Auto - -set_option linter.unusedVariables false -set_option auto.smt true -set_option trace.auto.smt.printCommands false -set_option trace.auto.smt.result true -set_option auto.smt.trust true -set_option auto.smt.solver.name ""z3"" -set_option trace.auto.buildChecker false - -@[simp] def assert (ψ β: Prop): Prop := ψ ∧ β -@[simp] def assume (ψ β: Prop): Prop := ψ → β -@[simp] def skip (β: Prop): Prop := β -@[simp] def ret: Prop := true -@[simp] def goto: Prop → Prop := id - --- SMT Array definition -def SMTArray1 (s1 s2: Type) := s1 → s2 - -def SMTArray2 (s1 s2 s3 : Type) := s1 → s2 → s3 - -def store1 [BEq s1] (m: SMTArray1 s1 s2) (i: s1) (v: s2): SMTArray1 s1 s2 := - fun i' => if i' == i then v else m i' - -def select1 (m: SMTArray1 s1 s2) (i: s1): s2 := m i - -def store2 [BEq s1] [BEq s2] (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (v: s3): SMTArray2 s1 s2 s3 := - fun i' j' => if i' == i && j' == j then v else m i' j' - -def select2 (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2): s3 := m i j - -axiom SelectStoreSame1 (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (e: s2): - select1 (store1 a i e) i = e - -axiom SelectStoreDistinct1 (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (j: s1) (e: s2): - i ≠ j → select1 (store1 a i e) j = select1 a j - -axiom SelectStoreSame2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (e: s3): - select2 (store2 a i j e) i j = e - -axiom SelectStoreDistinct2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s2 s3) (i: s1) (i': s1) (j: s2) (j' : s2) (e: s3): - i ≠ i' \/ j ≠ j' → select2 (store2 a i j e) i' j' = select2 a i' j' - --- TODO: provide either a definition or some functional axioms (or a definition plus some lemmas) -axiom distinct : {a : Type} → List a → Prop - -axiom realToInt : Real → Int -axiom intToReal : Int → Real -instance BEqReal: BEq Real := by sorry -"; - private LeanGenerator(VCGenOptions options, TextWriter writer) { this.options = options; @@ -153,6 +99,13 @@ private void EmitUniqueConstAxioms() private void EmitHeader() { + var assembly = System.Reflection.Assembly.GetExecutingAssembly(); + var preludeStream = assembly.GetManifestResourceStream("Prelude.lean"); + if (preludeStream is null) { + throw new LeanConversionException("Internal: failed to find Lean prelude in assembly."); + } + var header = new StreamReader(preludeStream).ReadToEnd(); + Console.WriteLine(header.Length); writer.WriteLine(header.ReplaceLineEndings()); } diff --git a/Source/Provers/LeanAuto/LeanAuto.csproj b/Source/Provers/LeanAuto/LeanAuto.csproj index dd35d8d18..46e028edc 100644 --- a/Source/Provers/LeanAuto/LeanAuto.csproj +++ b/Source/Provers/LeanAuto/LeanAuto.csproj @@ -16,4 +16,10 @@ + + + Prelude.lean + + + diff --git a/Source/Provers/LeanAuto/Prelude.lean b/Source/Provers/LeanAuto/Prelude.lean new file mode 100644 index 000000000..51bf156b2 --- /dev/null +++ b/Source/Provers/LeanAuto/Prelude.lean @@ -0,0 +1,52 @@ +import Auto +import Auto.Tactic +import Auto.MathlibEmulator.Basic -- For `Real` +open Lean Std Auto + +set_option linter.unusedVariables false +set_option auto.smt true +set_option trace.auto.smt.printCommands false +set_option trace.auto.smt.result true +set_option auto.smt.trust true +set_option auto.smt.solver.name "z3" +set_option trace.auto.buildChecker false + +@[simp] def assert (ψ β: Prop): Prop := ψ ∧ β +@[simp] def assume (ψ β: Prop): Prop := ψ → β +@[simp] def skip (β: Prop): Prop := β +@[simp] def ret: Prop := true +@[simp] def goto: Prop → Prop := id + +-- SMT Array definition +def SMTArray1 (s1 s2: Type) := s1 → s2 + +def SMTArray2 (s1 s2 s3 : Type) := s1 → s2 → s3 + +def store1 [BEq s1] (m: SMTArray1 s1 s2) (i: s1) (v: s2): SMTArray1 s1 s2 := + fun i' => if i' == i then v else m i' + +def select1 (m: SMTArray1 s1 s2) (i: s1): s2 := m i + +def store2 [BEq s1] [BEq s2] (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (v: s3): SMTArray2 s1 s2 s3 := + fun i' j' => if i' == i && j' == j then v else m i' j' + +def select2 (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2): s3 := m i j + +axiom SelectStoreSame1 (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (e: s2): + select1 (store1 a i e) i = e + +axiom SelectStoreDistinct1 (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (j: s1) (e: s2): + i ≠ j → select1 (store1 a i e) j = select1 a j + +axiom SelectStoreSame2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (e: s3): + select2 (store2 a i j e) i j = e + +axiom SelectStoreDistinct2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s2 s3) (i: s1) (i': s1) (j: s2) (j' : s2) (e: s3): + i ≠ i' \/ j ≠ j' → select2 (store2 a i j e) i' j' = select2 a i' j' + +-- TODO: provide either a definition or some functional axioms (or a definition plus some lemmas) +axiom distinct : {a : Type} → List a → Prop + +axiom realToInt : Real → Int +axiom intToReal : Int → Real +instance BEqReal: BEq Real := by sorry From d2193dd7a2886b450cef04c001532bade4f5c26e Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 13 Feb 2024 11:08:32 -0800 Subject: [PATCH 11/30] Add configuration files to check Prelude.lean --- Source/Provers/LeanAuto/.gitignore | 2 ++ Source/Provers/LeanAuto/lakefile.lean | 14 ++++++++++++++ Source/Provers/LeanAuto/lean-toolchain | 1 + 3 files changed, 17 insertions(+) create mode 100644 Source/Provers/LeanAuto/.gitignore create mode 100644 Source/Provers/LeanAuto/lakefile.lean create mode 100644 Source/Provers/LeanAuto/lean-toolchain diff --git a/Source/Provers/LeanAuto/.gitignore b/Source/Provers/LeanAuto/.gitignore new file mode 100644 index 000000000..3c2fe0de4 --- /dev/null +++ b/Source/Provers/LeanAuto/.gitignore @@ -0,0 +1,2 @@ +.lake +lake-manifest.json diff --git a/Source/Provers/LeanAuto/lakefile.lean b/Source/Provers/LeanAuto/lakefile.lean new file mode 100644 index 000000000..91898e289 --- /dev/null +++ b/Source/Provers/LeanAuto/lakefile.lean @@ -0,0 +1,14 @@ +import Lake +open Lake DSL + +package «prelude» { + -- add any package configuration options here +} + +require auto from git + "https://github.com/leanprover-community/lean-auto"@"main" + +@[default_target] +lean_lib «Prelude» { + -- add any library configuration options here +} diff --git a/Source/Provers/LeanAuto/lean-toolchain b/Source/Provers/LeanAuto/lean-toolchain new file mode 100644 index 000000000..cfcdd3277 --- /dev/null +++ b/Source/Provers/LeanAuto/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.6.0-rc1 From 7c096c02d6fe0f798a66b2dd8bd7074c5996b88f Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 13 Feb 2024 11:29:56 -0800 Subject: [PATCH 12/30] Cleanup comments, strings, exceptions --- Source/Provers/LeanAuto/LeanAuto.cs | 58 +++++++++++++---------------- 1 file changed, 25 insertions(+), 33 deletions(-) diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index a629b1775..b5122f5cc 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -21,6 +21,11 @@ public class LeanGenerator : ReadOnlyVisitor private readonly List userAxiomNames = new(); private readonly Dictionary> uniqueConsts = new(); + private const string AndString = "\u2227"; /* ∧ */ + private const string OrString = "\u2228"; /* ∨ */ + private const string NeqString = "\u2260"; /* ≠ */ + private const string ArrowString = "\u2192"; /* → */ + private LeanGenerator(VCGenOptions options, TextWriter writer) { this.options = options; @@ -105,7 +110,6 @@ private void EmitHeader() throw new LeanConversionException("Internal: failed to find Lean prelude in assembly."); } var header = new StreamReader(preludeStream).ReadToEnd(); - Console.WriteLine(header.Length); writer.WriteLine(header.ReplaceLineEndings()); } @@ -183,7 +187,7 @@ public override Cmd VisitAssumeCmd(AssumeCmd node) public override GotoCmd VisitGotoCmd(GotoCmd node) { var gotoText = node.labelTargets.Select(l => - $"goto {BlockName(l)}").Aggregate((a, b) => $"{a} \u2227 {b}"); + $"goto {BlockName(l)}").Aggregate((a, b) => $"{a} {AndString} {b}"); Indent(2, gotoText); return node; } @@ -322,7 +326,6 @@ public override TypedIdent VisitTypedIdent(TypedIdent node) public override Expr VisitBvExtractExpr(BvExtractExpr node) { - // TODO: double-check range values Text($"(BitVec.extractLsb {node.End - 1} {node.Start} "); Visit(node.Bitvector); Text(")"); @@ -431,11 +434,6 @@ public override Expr VisitNAryExpr(NAryExpr node) Text(")"); } else if (fun is FieldAccess fieldAccess) { throw new LeanConversionException("Unsupported: field access (since the semantics are complex)"); - // TODO: implement - /* - Visit(args[0]); - Text($".{SanitizeNameForLean(fieldAccess.FieldName)}"); - */ } else { VisitIAppliable(fun); foreach (var arg in args) { @@ -469,9 +467,10 @@ private void VisitIAppliable(IAppliable fun) Text(Name(fc.Func)); break; case IsConstructor isConstructor: - // TODO: declare these discriminator functions - Text($"is_{SanitizeNameForLean(isConstructor.ConstructorName)}"); - break; + throw new LeanConversionException($"Unsupported: Constructor: {isConstructor.ConstructorName}"); + // Discriminator functions not declared yet + //Text($"is_{SanitizeNameForLean(isConstructor.ConstructorName)}"); + //break; case ArithmeticCoercion arithmeticCoercion: var func = arithmeticCoercion.Coercion switch { @@ -508,20 +507,17 @@ public override Ensures VisitEnsures(Ensures ensures) public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) { - Console.WriteLine($"DeclWithFormals: {node}"); - return node; // TODO: do something? + throw new LeanConversionException($"Unsupported: DeclWithFormals ({node})."); } public override Type VisitBvTypeProxy(BvTypeProxy node) { - // TODO: confirm that this is unreachable - throw new LeanConversionException($"Unsupported: bvtypeproxy: {node}"); + throw new LeanConversionException($"Unsupported: BvTypeProxy ({node})."); } public override Expr VisitCodeExpr(CodeExpr node) { - // TODO: what is this? - throw new LeanConversionException($"Unsupported: codexpr: {node}"); + throw new LeanConversionException($"Unsupported: CodeExpr ({node})."); } public override Cmd VisitCommentCmd(CommentCmd node) @@ -542,7 +538,6 @@ public override List VisitEnsuresSeq(List ensuresSeq) public override Type VisitMapTypeProxy(MapTypeProxy node) { - // TODO: confirm that this is unreachable throw new LeanConversionException($"Unsupported: maptypeproxy: {node}"); } @@ -629,32 +624,29 @@ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) public override ActionDeclRef VisitActionDeclRef(ActionDeclRef node) { - // TODO: what is this? - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: ActionDeclRef ({node})."); } public override ElimDecl VisitElimDecl(ElimDecl node) { - // TODO: support this? - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: ElimDecl ({node})."); } public override List VisitElimDeclSeq(List node) { - // TODO: support this? - throw new LeanConversionException($"Unsupported: {node}"); + throw new LeanConversionException($"Unsupported: List ({node})."); } public override Axiom VisitAxiom(Axiom node) { // This will take two more steps: - // * A named lemma with a definition of `by sorry` (using a `name` attribute?) (or `id`, so it's also useful for proof dependencies?) + // * A named lemma with a definition of `by sorry` (using a `name` attribute?) (or `id`, so it's also useful for coverage?) // * A named lemma that's defined by a call to a previously-defined proof of the same thing int n = 0; - var name = $"ax_l{node.tok.line}c{node.tok.col}_{n}"; + var name = $"ax_l{node.tok.line}c{node.tok.col}"; while (userAxiomNames.Contains(name)) { - n += 1; name = $"ax_l{node.tok.line}c{node.tok.col}_{n}"; + n += 1; } Text($"axiom {name}: "); VisitExpr(node.Expr); @@ -670,12 +662,12 @@ public override Function VisitFunction(Function node) node.TypeParameters.ForEach(x => { Text($"{{{Name(x)} : Type}}"); - Text(" \u2192 "); + Text($" {ArrowString} "); }); node.InParams.ForEach(x => { Visit(x.TypedIdent.Type); - Text(" \u2192 "); + Text($" {ArrowString} "); }); if (node.OutParams.Count == 1) { Visit(node.OutParams[0].TypedIdent.Type); @@ -708,11 +700,11 @@ private string BinaryOpToLean(BinaryOperator.Opcode op) BinaryOperator.Opcode.Le => "<=", BinaryOperator.Opcode.Ge => ">=", BinaryOperator.Opcode.Eq => "=", - BinaryOperator.Opcode.Neq => "\u2260", /* ≠ */ - BinaryOperator.Opcode.And => "\u2227", /* ∧ */ - BinaryOperator.Opcode.Or => "\u2228", /* ∨ */ + BinaryOperator.Opcode.Neq => NeqString, + BinaryOperator.Opcode.And => AndString, + BinaryOperator.Opcode.Or => OrString, BinaryOperator.Opcode.Iff => "=", - BinaryOperator.Opcode.Imp => "\u2192", /* → */ + BinaryOperator.Opcode.Imp => ArrowString, BinaryOperator.Opcode.Pow => "^", BinaryOperator.Opcode.RealDiv => "/", BinaryOperator.Opcode.FloatDiv => "/", From 7fea48dfcecfa8b49af2616b5275551e46724c3a Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 13 Feb 2024 16:19:45 -0800 Subject: [PATCH 13/30] Clean up error handling --- Source/Provers/LeanAuto/LeanAuto.cs | 121 ++++++++++++++-------------- 1 file changed, 61 insertions(+), 60 deletions(-) diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index b5122f5cc..aa82c25b4 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -76,6 +76,7 @@ public static void EmitPassiveProgramAsLean(VCGenOptions options, Program p, Tex p.Implementations.ForEach(i => generator.Visit(i)); } catch (LeanConversionException e) { Console.WriteLine($"Failed translation: {e.Msg}"); + Environment.Exit(1); } } @@ -107,7 +108,7 @@ private void EmitHeader() var assembly = System.Reflection.Assembly.GetExecutingAssembly(); var preludeStream = assembly.GetManifestResourceStream("Prelude.lean"); if (preludeStream is null) { - throw new LeanConversionException("Internal: failed to find Lean prelude in assembly."); + throw new LeanConversionException(Token.NoToken, "Internal: failed to find Lean prelude in assembly."); } var header = new StreamReader(preludeStream).ReadToEnd(); writer.WriteLine(header.ReplaceLineEndings()); @@ -219,7 +220,7 @@ public override Type VisitType(Type node) TypeSynonymAnnotation typeSynonymAnnotation => VisitTypeSynonymAnnotation(typeSynonymAnnotation), TypeVariable typeVariable => VisitTypeVariable(typeVariable), UnresolvedTypeIdentifier uti => VisitUnresolvedTypeIdentifier(uti), - _ => throw new LeanConversionException("Unreachable type case.") + _ => throw new LeanConversionException(node.tok, $"Unsupported type: {node}.") }; } @@ -232,14 +233,14 @@ public override Type VisitBasicType(BasicType node) } else if (node.IsReal) { Text("Real"); } else if (node.IsRMode) { - throw new LeanConversionException("Unsupported: RMode type"); + throw new LeanConversionException(node.tok, "Unsupported type: RMode."); } else if (node.IsRegEx) { - throw new LeanConversionException("Unsupported: RegEx type"); + throw new LeanConversionException(node.tok, "Unsupported type: RegEx."); } else if (node.IsMap) { var mapType = node.AsMap; VisitMapType(mapType); } else { - throw new LeanConversionException($"Unsupported BasicType: {node}"); + throw new LeanConversionException(node.tok, $"Unsupported type: {node}."); } return node; @@ -296,7 +297,7 @@ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) { ForallExpr => "forall", ExistsExpr => "exists", - _ => throw new LeanConversionException($"Unsupported quantifier type: {node.Kind}") + _ => throw new LeanConversionException(node.tok, $"Unsupported quantifier type: {node.Kind}") }; Text($"({kind}"); foreach (var tv in node.TypeParameters) { @@ -345,7 +346,7 @@ public override Expr VisitLambdaExpr(LambdaExpr node) public override Expr VisitLetExpr(LetExpr node) { if (node.Dummies.Count > 1) { - throw new LeanConversionException("Unsupported: LetExpr with more than one binder"); + throw new LeanConversionException(node.tok, "Unsupported: LetExpr with more than one binder"); } Text("(let"); node.Dummies.ForEach(x => Visit(x.TypedIdent)); @@ -389,7 +390,7 @@ public override Expr VisitLiteralExpr(LiteralExpr node) public override Type VisitMapType(MapType node) { if (node.Arguments.Count > 2) { - throw new LeanConversionException($"Unsupported: MapType with too many index types ({node})"); + throw new LeanConversionException(node.tok, $"Unsupported: MapType with too many index types ({node})"); } if (node.TypeParameters.Any()) { var args = node.TypeParameters.Select(Name); @@ -433,7 +434,7 @@ public override Expr VisitNAryExpr(NAryExpr node) Visit(typeCoercion.Type); Text(")"); } else if (fun is FieldAccess fieldAccess) { - throw new LeanConversionException("Unsupported: field access (since the semantics are complex)"); + throw new LeanConversionException(node.tok, "Unsupported: field access (since the semantics are complex)"); } else { VisitIAppliable(fun); foreach (var arg in args) { @@ -467,7 +468,7 @@ private void VisitIAppliable(IAppliable fun) Text(Name(fc.Func)); break; case IsConstructor isConstructor: - throw new LeanConversionException($"Unsupported: Constructor: {isConstructor.ConstructorName}"); + throw new LeanConversionException(isConstructor.tok, $"Unsupported: Constructor: {isConstructor.ConstructorName}"); // Discriminator functions not declared yet //Text($"is_{SanitizeNameForLean(isConstructor.ConstructorName)}"); //break; @@ -476,23 +477,23 @@ private void VisitIAppliable(IAppliable fun) { ArithmeticCoercion.CoercionType.ToInt => "realToInt", ArithmeticCoercion.CoercionType.ToReal => "intToReal", - _ => throw new LeanConversionException($"Internal: unknown arithmetic coercion: {arithmeticCoercion.Coercion}") + _ => throw new LeanConversionException(Token.NoToken, $"Internal: unknown arithmetic coercion: {arithmeticCoercion.Coercion}") }; Text(func); break; default: - throw new LeanConversionException($"Unsupported: IAppliable: {fun}"); + throw new LeanConversionException(Token.NoToken, $"Unsupported: IAppliable: {fun}"); } } public override Expr VisitOldExpr(OldExpr node) { - throw new LeanConversionException("Unsupported: OldExpr"); + throw new LeanConversionException(node.tok, "Unsupported: OldExpr"); } public override Type VisitFloatType(FloatType node) { - throw new LeanConversionException("Unsupported: FloatType"); + throw new LeanConversionException(node.tok, "Unsupported: FloatType"); } public override Requires VisitRequires(Requires requires) @@ -507,17 +508,17 @@ public override Ensures VisitEnsures(Ensures ensures) public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) { - throw new LeanConversionException($"Unsupported: DeclWithFormals ({node})."); + throw new LeanConversionException(node.tok, $"Unsupported: DeclWithFormals ({node})."); } public override Type VisitBvTypeProxy(BvTypeProxy node) { - throw new LeanConversionException($"Unsupported: BvTypeProxy ({node})."); + throw new LeanConversionException(node.tok, $"Unsupported: BvTypeProxy ({node})."); } public override Expr VisitCodeExpr(CodeExpr node) { - throw new LeanConversionException($"Unsupported: CodeExpr ({node})."); + throw new LeanConversionException(node.tok, $"Unsupported: CodeExpr ({node})."); } public override Cmd VisitCommentCmd(CommentCmd node) @@ -538,7 +539,7 @@ public override List VisitEnsuresSeq(List ensuresSeq) public override Type VisitMapTypeProxy(MapTypeProxy node) { - throw new LeanConversionException($"Unsupported: maptypeproxy: {node}"); + throw new LeanConversionException(node.tok, $"Unsupported: MapTypeProxy: {node}"); } public override QKeyValue VisitQKeyValue(QKeyValue node) @@ -624,17 +625,17 @@ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) public override ActionDeclRef VisitActionDeclRef(ActionDeclRef node) { - throw new LeanConversionException($"Unsupported: ActionDeclRef ({node})."); + throw new LeanConversionException(node.tok, $"Unsupported: ActionDeclRef ({node})."); } public override ElimDecl VisitElimDecl(ElimDecl node) { - throw new LeanConversionException($"Unsupported: ElimDecl ({node})."); + throw new LeanConversionException(node.tok, $"Unsupported: ElimDecl ({node})."); } public override List VisitElimDeclSeq(List node) { - throw new LeanConversionException($"Unsupported: List ({node})."); + throw new LeanConversionException(Token.NoToken, $"Unsupported: List ({node})."); } public override Axiom VisitAxiom(Axiom node) @@ -708,7 +709,7 @@ private string BinaryOpToLean(BinaryOperator.Opcode op) BinaryOperator.Opcode.Pow => "^", BinaryOperator.Opcode.RealDiv => "/", BinaryOperator.Opcode.FloatDiv => "/", - _ => throw new LeanConversionException($"unsupported binary operator: {op.ToString()}") + _ => throw new LeanConversionException(Token.NoToken, $"Unsupported binary operator: {op.ToString()}") }; } @@ -718,7 +719,7 @@ private string UnaryOpToLean(UnaryOperator.Opcode op) { UnaryOperator.Opcode.Not => "Not", UnaryOperator.Opcode.Neg => "-", - _ => throw new LeanConversionException($"unsupported unary operator: {op.ToString()}") + _ => throw new LeanConversionException(Token.NoToken, $"Unsupported unary operator: {op.ToString()}") }; } @@ -822,185 +823,185 @@ public override Implementation VisitImplementation(Implementation node) public override Program VisitProgram(Program node) { - throw new LeanConversionException($"Internal: Program should never be directly visited ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: Program should never be directly visited."); } public override Declaration VisitDeclaration(Declaration node) { - throw new LeanConversionException($"Internal: Declaration should never be directly visited ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: Declaration should never be directly visited."); } public override List VisitDeclarationList(List declarationList) { - throw new LeanConversionException($"Internal: List should never be directly visited ({declarationList})."); + throw new LeanConversionException(Token.NoToken, $"Internal: List should never be directly visited ({declarationList})."); } public override List VisitBlockSeq(List blockSeq) { - throw new LeanConversionException($"Internal: List should never be directly visited ({blockSeq})."); + throw new LeanConversionException(Token.NoToken, $"Internal: List should never be directly visited ({blockSeq})."); } public override List VisitBlockList(List blocks) { - throw new LeanConversionException($"Internal: List should never be directly visited ({blocks})."); + throw new LeanConversionException(Token.NoToken, $"Internal: List should never be directly visited ({blocks})."); } public override Trigger VisitTrigger(Trigger node) { - throw new LeanConversionException($"Internal: Trigger should never be directly visited ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: Trigger should never be directly visited."); } public override IList VisitExprSeq(IList exprSeq) { - throw new LeanConversionException($"Internal: List should never be directly visited ({exprSeq})."); + throw new LeanConversionException(Token.NoToken, $"Internal: List should never be directly visited ({exprSeq})."); } public override BoundVariable VisitBoundVariable(BoundVariable node) { - throw new LeanConversionException($"Internal: BoundVariable should never be directly visited ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: BoundVariable should never be directly visited."); } public override Formal VisitFormal(Formal node) { - throw new LeanConversionException($"Internal: Formal should never be directly visited ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: Formal should never be directly visited."); } public override LocalVariable VisitLocalVariable(LocalVariable node) { - throw new LeanConversionException($"Internal error: LocalVariable should never be directly visited ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal error: LocalVariable should never be directly visited."); } public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node) { - throw new LeanConversionException($"Internal: UnresolvedTypeIdentifier should never appear ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: UnresolvedTypeIdentifier should never appear."); } public override Variable VisitVariable(Variable node) { - throw new LeanConversionException($"Internal: Variable should never be directly visited ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: Variable should never be directly visited."); } public override List VisitVariableSeq(List variableSeq) { - throw new LeanConversionException($"Internal: List should never be directly visited ({variableSeq})."); + throw new LeanConversionException(Token.NoToken, $"Internal: List should never be directly visited ({variableSeq})."); } public override HashSet VisitVariableSet(HashSet node) { - throw new LeanConversionException($"Internal: HashSet should never be directly visited ({node})."); + throw new LeanConversionException(Token.NoToken, $"Internal: HashSet should never be directly visited ({node})."); } public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) { - throw new LeanConversionException($"Internal: MapAssignLhs should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: MapAssignLhs should never appear in passive program."); } public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node) { - throw new LeanConversionException($"Internal: SimpleAssignLhs should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: SimpleAssignLhs should never appear in passive program."); } public override AssignLhs VisitFieldAssignLhs(FieldAssignLhs node) { - throw new LeanConversionException($"Internal: FieldAssignLhs should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: FieldAssignLhs should never appear in passive program."); } public override Cmd VisitAssignCmd(AssignCmd node) { - throw new LeanConversionException($"Internal: AssignCmd should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: AssignCmd should never appear in passive program."); } public override Cmd VisitUnpackCmd(UnpackCmd node) { - throw new LeanConversionException($"Internal: UnpackCmd should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: UnpackCmd should never appear in passive program."); } public override Cmd VisitCallCmd(CallCmd node) { - throw new LeanConversionException($"Internal: CallCmd should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: CallCmd should never appear in passive program."); } public override Cmd VisitParCallCmd(ParCallCmd node) { - throw new LeanConversionException($"Internal: ParCallCmd should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: ParCallCmd should never appear in passive program."); } public override Cmd VisitHavocCmd(HavocCmd node) { - throw new LeanConversionException($"Internal: HavocCmd should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: HavocCmd should never appear in passive program."); } public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) { - throw new LeanConversionException($"Internal: ReturnExprCmd should never appear in passive program ({node.tok})"); + throw new LeanConversionException(node.tok, $"Internal: ReturnExprCmd should never appear in passive program."); } public override Cmd VisitStateCmd(StateCmd node) { - throw new LeanConversionException($"Internal: StateCmd should never appear in passive program ({node.tok})"); + throw new LeanConversionException(node.tok, $"Internal: StateCmd should never appear in passive program."); } public override List VisitCallCmdSeq(List callCmds) { - throw new LeanConversionException($"Internal: List should never appear in passive program ({callCmds})."); + throw new LeanConversionException(Token.NoToken, $"Internal: List should never appear in passive program ({callCmds})."); } public override Procedure VisitActionDecl(ActionDecl node) { - throw new LeanConversionException($"Internal: ActionDecl should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: ActionDecl should never appear in passive program."); } public override YieldingLoop VisitYieldingLoop(YieldingLoop node) { - throw new LeanConversionException($"Internal: YieldingLoop should never appear in passive program ({node})."); + throw new LeanConversionException(Token.NoToken,$"Internal: YieldingLoop should never appear in passive program ({node})."); } public override Dictionary VisitYieldingLoops(Dictionary node) { - throw new LeanConversionException($"Internal: YieldingLoops should never appear in passive program."); + throw new LeanConversionException(Token.NoToken, $"Internal: YieldingLoops should never appear in passive program."); } public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node) { - throw new LeanConversionException($"Internal: YieldProcedureDecl should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: YieldProcedureDecl should never appear in passive program."); } public override Procedure VisitYieldInvariantDecl(YieldInvariantDecl node) { - throw new LeanConversionException($"Internal: YieldInvariantDecl should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: YieldInvariantDecl should never appear in passive program."); } public override Cmd VisitRE(RE node) { - throw new LeanConversionException($"Internal: RE should never appear in passive program ({node.tok})"); + throw new LeanConversionException(node.tok, $"Internal: RE should never appear in passive program."); } public override List VisitRESeq(List reSeq) { - throw new LeanConversionException($"Internal: List should never appear in passive program ({reSeq})"); + throw new LeanConversionException(Token.NoToken, $"Internal: List should never appear in passive program ({reSeq})"); } public override AtomicRE VisitAtomicRE(AtomicRE node) { - throw new LeanConversionException($"Internal: AtomicRE should never appear in passive program ({node.tok})"); + throw new LeanConversionException(node.tok, $"Internal: AtomicRE should never appear in passive program."); } public override Choice VisitChoice(Choice node) { - throw new LeanConversionException($"Internal: Choice should never appear in passive program ({node.tok})."); + throw new LeanConversionException(node.tok, $"Internal: Choice should never appear in passive program."); } public override Sequential VisitSequential(Sequential node) { - throw new LeanConversionException($"Internal: Sequential should never appear in passive program ({node.tok})"); + throw new LeanConversionException(node.tok, $"Internal: Sequential should never appear in passive program."); } } internal class LeanConversionException : Exception { public string Msg { get; } - public LeanConversionException(string s) + public LeanConversionException(IToken tok, string s) { - Msg = s; + Msg = tok + ": " + s; } } From 05b616c4c1845722acfe4e54909747349c9fae65 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 10:19:18 -0800 Subject: [PATCH 14/30] Reorder cases and improve error messages --- Source/Provers/LeanAuto/LeanAuto.cs | 126 +++++++++++++++++----------- 1 file changed, 77 insertions(+), 49 deletions(-) diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAuto.cs index aa82c25b4..956989630 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAuto.cs @@ -5,6 +5,15 @@ namespace Microsoft.Boogie.LeanAuto; +internal class LeanConversionException : Exception +{ + public string Msg { get; } + public LeanConversionException(IToken tok, string s) + { + Msg = tok + ": " + s; + } +} + public class LeanGenerator : ReadOnlyVisitor { private readonly TextWriter writer; @@ -108,7 +117,8 @@ private void EmitHeader() var assembly = System.Reflection.Assembly.GetExecutingAssembly(); var preludeStream = assembly.GetManifestResourceStream("Prelude.lean"); if (preludeStream is null) { - throw new LeanConversionException(Token.NoToken, "Internal: failed to find Lean prelude in assembly."); + throw new LeanConversionException(Token.NoToken, + "Internal: failed to find Lean prelude in assembly."); } var header = new StreamReader(preludeStream).ReadToEnd(); writer.WriteLine(header.ReplaceLineEndings()); @@ -116,9 +126,7 @@ private void EmitHeader() private void Indent(int n = 1, string str = null) { - for (var i = 0; i < n; i++) { - Text(" "); - } + Text(String.Concat(Enumerable.Repeat(" ", n))); if (str is not null) { Text(str); @@ -161,9 +169,11 @@ public override Block VisitBlock(Block node) node.Cmds.ForEach(c => Visit(c)); if (node.TransferCmd is ReturnCmd r) { VisitReturnCmd(r); - } - if (node.TransferCmd is GotoCmd g) { + } else if (node.TransferCmd is GotoCmd g) { VisitGotoCmd(g); + } else { + throw new LeanConversionException(node.TransferCmd.tok, + $"Unsupported transfer command: {node.TransferCmd}"); } NL(); return node; @@ -217,10 +227,12 @@ public override Type VisitType(Type node) FloatType floatType => VisitFloatType(floatType), MapType mapType => VisitMapType(mapType), TypeProxy typeProxy => VisitTypeProxy(typeProxy), - TypeSynonymAnnotation typeSynonymAnnotation => VisitTypeSynonymAnnotation(typeSynonymAnnotation), + TypeSynonymAnnotation typeSynonymAnnotation => + VisitTypeSynonymAnnotation(typeSynonymAnnotation), TypeVariable typeVariable => VisitTypeVariable(typeVariable), UnresolvedTypeIdentifier uti => VisitUnresolvedTypeIdentifier(uti), - _ => throw new LeanConversionException(node.tok, $"Unsupported type: {node}.") + _ => throw new LeanConversionException(node.tok, + $"Internal: Branch should be unreachable for Type: {node}.") }; } @@ -236,11 +248,11 @@ public override Type VisitBasicType(BasicType node) throw new LeanConversionException(node.tok, "Unsupported type: RMode."); } else if (node.IsRegEx) { throw new LeanConversionException(node.tok, "Unsupported type: RegEx."); - } else if (node.IsMap) { - var mapType = node.AsMap; - VisitMapType(mapType); + } else if (node.IsString) { + throw new LeanConversionException(node.tok, "Unsupported type: String."); } else { - throw new LeanConversionException(node.tok, $"Unsupported type: {node}."); + throw new LeanConversionException(node.tok, + $"Internal: Branch should be unreachable for BasicType: {node}."); } return node; @@ -297,7 +309,8 @@ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) { ForallExpr => "forall", ExistsExpr => "exists", - _ => throw new LeanConversionException(node.tok, $"Unsupported quantifier type: {node.Kind}") + _ => throw new LeanConversionException(node.tok, + $"Unsupported quantifier type: {node.Kind}") }; Text($"({kind}"); foreach (var tv in node.TypeParameters) { @@ -346,7 +359,8 @@ public override Expr VisitLambdaExpr(LambdaExpr node) public override Expr VisitLetExpr(LetExpr node) { if (node.Dummies.Count > 1) { - throw new LeanConversionException(node.tok, "Unsupported: LetExpr with more than one binder"); + throw new LeanConversionException(node.tok, + "Unsupported: LetExpr with more than one binder"); } Text("(let"); node.Dummies.ForEach(x => Visit(x.TypedIdent)); @@ -381,8 +395,21 @@ public override Expr VisitLiteralExpr(LiteralExpr node) Text(bvConst.Value.ToString()); Text($" : BitVec {bvConst.Bits}"); Text(")"); + } else if (node.isBigDec) { + throw new LeanConversionException(node.tok, + "Unsupported literal: BigDec"); + } else if (node.isBigNum) { + var bigNumConst = node.asBigNum; + Text(bigNumConst.ToString()); + } else if (node.isBigFloat) { + throw new LeanConversionException(node.tok, + "Unsupported literal: BigFloat"); + } else if (node.isRoundingMode) { + throw new LeanConversionException(node.tok, + "Unsupported literal: RoundingMode"); } else { - Text(node.ToString()); // TODO: make sure this is right for all other literal types + throw new LeanConversionException(node.tok, + "Internal: Branch should be unreachable for literal: {node}"); } return node; } @@ -390,7 +417,8 @@ public override Expr VisitLiteralExpr(LiteralExpr node) public override Type VisitMapType(MapType node) { if (node.Arguments.Count > 2) { - throw new LeanConversionException(node.tok, $"Unsupported: MapType with too many index types ({node})"); + throw new LeanConversionException(node.tok, + $"Unsupported: MapType with more than 2 index types ({node})"); } if (node.TypeParameters.Any()) { var args = node.TypeParameters.Select(Name); @@ -416,6 +444,12 @@ public override Expr VisitNAryExpr(NAryExpr node) Visit(args[0]); Text($" {BinaryOpToLean(op.Op)} "); Visit(args[1]); + } else if (fun is FieldAccess fieldAccess) { + throw new LeanConversionException(node.tok, + "Unsupported: field access (since the semantics are complex)"); + } else if (fun is FieldUpdate fieldUpdate) { + throw new LeanConversionException(node.tok, + "Unsupported: field update (since the semantics are complex)"); } else if (fun is IfThenElse && args.Count == 3) { Text("if "); Visit(args[0]); @@ -433,8 +467,6 @@ public override Expr VisitNAryExpr(NAryExpr node) Text(" : "); Visit(typeCoercion.Type); Text(")"); - } else if (fun is FieldAccess fieldAccess) { - throw new LeanConversionException(node.tok, "Unsupported: field access (since the semantics are complex)"); } else { VisitIAppliable(fun); foreach (var arg in args) { @@ -450,39 +482,42 @@ public override Expr VisitNAryExpr(NAryExpr node) private void VisitIAppliable(IAppliable fun) { switch (fun) { - case MapSelect: - usesMaps = true; - Text($"select{fun.ArgumentCount - 1}"); - break; - case MapStore: - usesMaps = true; - Text($"store{fun.ArgumentCount - 2}"); + case ArithmeticCoercion arithmeticCoercion: + var func = arithmeticCoercion.Coercion switch + { + ArithmeticCoercion.CoercionType.ToInt => "realToInt", + ArithmeticCoercion.CoercionType.ToReal => "intToReal", + _ => throw new LeanConversionException(Token.NoToken, + $"Internal: unknown arithmetic coercion: {arithmeticCoercion.Coercion}") + }; + Text(func); break; case BinaryOperator op: Text(BinaryOpToLean(op.Op)); break; - case UnaryOperator op: - Text(UnaryOpToLean(op.Op)); - break; case FunctionCall fc: Text(Name(fc.Func)); break; case IsConstructor isConstructor: - throw new LeanConversionException(isConstructor.tok, $"Unsupported: Constructor: {isConstructor.ConstructorName}"); + throw new LeanConversionException(isConstructor.tok, + $"Unsupported: Constructor: {isConstructor.ConstructorName}"); // Discriminator functions not declared yet //Text($"is_{SanitizeNameForLean(isConstructor.ConstructorName)}"); //break; - case ArithmeticCoercion arithmeticCoercion: - var func = arithmeticCoercion.Coercion switch - { - ArithmeticCoercion.CoercionType.ToInt => "realToInt", - ArithmeticCoercion.CoercionType.ToReal => "intToReal", - _ => throw new LeanConversionException(Token.NoToken, $"Internal: unknown arithmetic coercion: {arithmeticCoercion.Coercion}") - }; - Text(func); + case MapSelect: + usesMaps = true; + Text($"select{fun.ArgumentCount - 1}"); + break; + case MapStore: + usesMaps = true; + Text($"store{fun.ArgumentCount - 2}"); + break; + case UnaryOperator op: + Text(UnaryOpToLean(op.Op)); break; default: - throw new LeanConversionException(Token.NoToken, $"Unsupported: IAppliable: {fun}"); + throw new LeanConversionException(Token.NoToken, + $"Unsupported: IAppliable: {fun}"); } } @@ -709,7 +744,8 @@ private string BinaryOpToLean(BinaryOperator.Opcode op) BinaryOperator.Opcode.Pow => "^", BinaryOperator.Opcode.RealDiv => "/", BinaryOperator.Opcode.FloatDiv => "/", - _ => throw new LeanConversionException(Token.NoToken, $"Unsupported binary operator: {op.ToString()}") + _ => throw new LeanConversionException(Token.NoToken, + $"Unsupported binary operator: {op.ToString()}") }; } @@ -719,7 +755,8 @@ private string UnaryOpToLean(UnaryOperator.Opcode op) { UnaryOperator.Opcode.Not => "Not", UnaryOperator.Opcode.Neg => "-", - _ => throw new LeanConversionException(Token.NoToken, $"Unsupported unary operator: {op.ToString()}") + _ => throw new LeanConversionException(Token.NoToken, + $"Unsupported unary operator: {op.ToString()}") }; } @@ -996,12 +1033,3 @@ public override Sequential VisitSequential(Sequential node) throw new LeanConversionException(node.tok, $"Internal: Sequential should never appear in passive program."); } } - -internal class LeanConversionException : Exception -{ - public string Msg { get; } - public LeanConversionException(IToken tok, string s) - { - Msg = tok + ": " + s; - } -} From 005d80d348cfa808e7e4736a077bbb53a7d7ff55 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 10:34:41 -0800 Subject: [PATCH 15/30] Add test suite for LeanAuto backend --- Test/lean-auto/.gitignore | 1 + Test/lean-auto/lake-manifest.json | 23 +++++++++++++++++++++++ Test/lean-auto/lakefile.lean | 14 ++++++++++++++ Test/lean-auto/lean-tests | 6 ++++++ Test/lean-auto/lean-toolchain | 1 + Test/lean-auto/test.sh | 9 +++++++++ Test/lean-auto/testall.sh | 7 +++++++ 7 files changed, 61 insertions(+) create mode 100644 Test/lean-auto/.gitignore create mode 100644 Test/lean-auto/lake-manifest.json create mode 100644 Test/lean-auto/lakefile.lean create mode 100644 Test/lean-auto/lean-tests create mode 100644 Test/lean-auto/lean-toolchain create mode 100755 Test/lean-auto/test.sh create mode 100755 Test/lean-auto/testall.sh diff --git a/Test/lean-auto/.gitignore b/Test/lean-auto/.gitignore new file mode 100644 index 000000000..2b0095269 --- /dev/null +++ b/Test/lean-auto/.gitignore @@ -0,0 +1 @@ +.lake diff --git a/Test/lean-auto/lake-manifest.json b/Test/lean-auto/lake-manifest.json new file mode 100644 index 000000000..47bbee834 --- /dev/null +++ b/Test/lean-auto/lake-manifest.json @@ -0,0 +1,23 @@ +{"version": 7, + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover/std4.git", + "type": "git", + "subDir": null, + "rev": "276953b13323ca151939eafaaec9129bf7970306", + "name": "std", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.6.0-rc1", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/lean-auto", + "type": "git", + "subDir": null, + "rev": "93105204453ca14cea9ae0c58bddb6809676db50", + "name": "auto", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "prelude", + "lakeDir": ".lake"} diff --git a/Test/lean-auto/lakefile.lean b/Test/lean-auto/lakefile.lean new file mode 100644 index 000000000..c5a3d2dbe --- /dev/null +++ b/Test/lean-auto/lakefile.lean @@ -0,0 +1,14 @@ +import Lake +open Lake DSL + +package «test» { + -- add any package configuration options here +} + +require auto from git + "https://github.com/leanprover-community/lean-auto"@"main" + +--@[default_target] +--lean_lib «Find» { +-- -- add any library configuration options here +--} diff --git a/Test/lean-auto/lean-tests b/Test/lean-auto/lean-tests new file mode 100644 index 000000000..549901577 --- /dev/null +++ b/Test/lean-auto/lean-tests @@ -0,0 +1,6 @@ +../textbook/TuringFactorial.bpl +../textbook/DutchFlag.bpl +../textbook/Bubble.bpl +../textbook/DivMod.bpl +../textbook/Find.bpl +../textbook/McCarthy-91.bpl diff --git a/Test/lean-auto/lean-toolchain b/Test/lean-auto/lean-toolchain new file mode 100644 index 000000000..cfcdd3277 --- /dev/null +++ b/Test/lean-auto/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.6.0-rc1 diff --git a/Test/lean-auto/test.sh b/Test/lean-auto/test.sh new file mode 100755 index 000000000..66fe08eac --- /dev/null +++ b/Test/lean-auto/test.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +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 +lake env lean $lean_file diff --git a/Test/lean-auto/testall.sh b/Test/lean-auto/testall.sh new file mode 100755 index 000000000..62be2246a --- /dev/null +++ b/Test/lean-auto/testall.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +set -e + +for test in `cat lean-tests` ; do + ./test.sh $test +done From df6bb76bba44dd6027b101e9d05a2b232af2cabf Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 10:35:59 -0800 Subject: [PATCH 16/30] Add README for LeanAuto --- Source/Provers/LeanAuto/README.md | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 Source/Provers/LeanAuto/README.md diff --git a/Source/Provers/LeanAuto/README.md b/Source/Provers/LeanAuto/README.md new file mode 100644 index 000000000..571101f00 --- /dev/null +++ b/Source/Provers/LeanAuto/README.md @@ -0,0 +1,31 @@ +# Overview + +This project provides a printer that renders passive Boogie programs in +Lean syntax. The generated Lean programs include a theorem for every +proof obligation, discharged by `lean-auto` (which uses an automated +theorem prover such as Z3, CVC5, or a first-order prover). + +Although it would be possible to write interactive proofs for the +generated goals, the primary purpose of this package is to use Lean as +an enhanced SMT solver, with support for tactics that pre-process goals +and custom decision procedures that, in some cases, may be able to +discharge goals without depending on an external solver. None of those +tactics or decision procedures have been written yet, however. + +For the moment, it works manually. The `/printLean:file.lean` option +will print the Lean source text (with `Prelude.lean` prepended) into +`file.lean` after completing normal verification. Ultimately, the code +will call out to Lean as an external process, like Boogie does with SMT +solvers at the moment, but doing that will require building some new +Lean infrastructure. + +# Checking the prelude + +Two files in this directory, `lean-toolchain` and `lakefile.lean` exist +primarily as development conveniences. With them in place, it's possible +to run `lake build` in this directory and check the code in +`Prelude.lean`. + +These files are also used in the test suite for this project, and can be +used as examples of the configuration needed to use the backend in +practice. From 6628fea8a3d406de8fce1b72a3bdd37328528a3d Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 10:36:59 -0800 Subject: [PATCH 17/30] Add workflow to test the LeanAuto backend --- .github/workflows/test-lean-auto.yml | 43 ++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 .github/workflows/test-lean-auto.yml diff --git a/.github/workflows/test-lean-auto.yml b/.github/workflows/test-lean-auto.yml new file mode 100644 index 000000000..0065a187f --- /dev/null +++ b/.github/workflows/test-lean-auto.yml @@ -0,0 +1,43 @@ +name: LeanAuto CI + +on: + workflow_dispatch: + push: + tags: + - 'v*' + pull_request: + branches: + - master + +jobs: + job0: + name: LeanAuto CI + runs-on: ubuntu-22.04 + steps: + - name: Setup dotnet + uses: actions/setup-dotnet@v3 + with: + dotnet-version: '6.0.x' + - name: Setup Z3 + uses: cda-tum/setup-z3@v1 + with: + version: 4.12.5 + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + - name: Checkout Boogie + uses: actions/checkout@v3 + with: + fetch-depth: 0 + - name: Install tools, build Boogie + run: | + dotnet tool restore + dotnet build -warnaserror Source/Boogie.sln + - name: Setup Lean + uses: actions/setup-lean@v1 + # Lean version will be chosen based on Test/lean-auto/lean-toolchain + working-directory: Test/lean-auto + - name: Test Lean generator on textbook examples + working-directory: Test/lean-auto + run: | + lake build + ./testall.sh From 300ed902cce65e6a5658b20dc5a61cc65ccb30a4 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 10:57:52 -0800 Subject: [PATCH 18/30] Fill in proofs and definitions in Lean prelude --- Source/Provers/LeanAuto/Prelude.lean | 63 +++++++++++++++++++++------- 1 file changed, 49 insertions(+), 14 deletions(-) diff --git a/Source/Provers/LeanAuto/Prelude.lean b/Source/Provers/LeanAuto/Prelude.lean index 51bf156b2..3bda453b3 100644 --- a/Source/Provers/LeanAuto/Prelude.lean +++ b/Source/Provers/LeanAuto/Prelude.lean @@ -22,30 +22,65 @@ def SMTArray1 (s1 s2: Type) := s1 → s2 def SMTArray2 (s1 s2 s3 : Type) := s1 → s2 → s3 -def store1 [BEq s1] (m: SMTArray1 s1 s2) (i: s1) (v: s2): SMTArray1 s1 s2 := - fun i' => if i' == i then v else m i' +def store1 + [BEq s1] + (m: SMTArray1 s1 s2) (i: s1) (v: s2): SMTArray1 s1 s2 := + fun i' => if i' == i then v else m i' def select1 (m: SMTArray1 s1 s2) (i: s1): s2 := m i -def store2 [BEq s1] [BEq s2] (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (v: s3): SMTArray2 s1 s2 s3 := - fun i' j' => if i' == i && j' == j then v else m i' j' +def store2 + [BEq s1] [BEq s2] + (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (v: s3): SMTArray2 s1 s2 s3 := + fun i' j' => if i' == i && j' == j then v else m i' j' def select2 (m: SMTArray2 s1 s2 s3) (i: s1) (j: s2): s3 := m i j -axiom SelectStoreSame1 (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (e: s2): - select1 (store1 a i e) i = e +theorem SelectStoreSame1 + (s1 s2: Type) + [BEq s1] [LawfulBEq s1] + (a: SMTArray1 s1 s2) (i: s1) (e: s2): + select1 (store1 a i e) i = e := + by simp [select1, store1] -axiom SelectStoreDistinct1 (s1 s2: Type) [BEq s1] (a: SMTArray1 s1 s2) (i: s1) (j: s1) (e: s2): - i ≠ j → select1 (store1 a i e) j = select1 a j +theorem SelectStoreDistinct1 + (s1 s2: Type) + [BEq s1] [LawfulBEq s1] + (a: SMTArray1 s1 s2) (i: s1) (j: s1) (e: s2): + i ≠ j → select1 (store1 a i e) j = select1 a j := + by simp [select1, store1] + intro neq eq1 + have eq2: i = j := Eq.symm eq1 + contradiction -axiom SelectStoreSame2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (e: s3): - select2 (store2 a i j e) i j = e +theorem SelectStoreSame2 + (s1 s2 s3: Type) + [BEq s1] [BEq s2] + [LawfulBEq s1] [LawfulBEq s2] + (a: SMTArray2 s1 s2 s3) (i: s1) (j: s2) (e: s3): + select2 (store2 a i j e) i j = e := + by simp [select2, store2] -axiom SelectStoreDistinct2 (s1 s2 s3: Type) [BEq s1] [BEq s2] (a: SMTArray2 s1 s2 s3) (i: s1) (i': s1) (j: s2) (j' : s2) (e: s3): - i ≠ i' \/ j ≠ j' → select2 (store2 a i j e) i' j' = select2 a i' j' +theorem SelectStoreDistinct2 + (s1 s2 s3: Type) + [BEq s1] [BEq s2] + [LawfulBEq s1] [LawfulBEq s2] + (a: SMTArray2 s1 s2 s3) (i: s1) (i': s1) (j: s2) (j' : s2) (e: s3): + i ≠ i' \/ j ≠ j' → select2 (store2 a i j e) i' j' = select2 a i' j' := + by simp [select2, store2] + intro either eq1 eq2 + cases either + have eq3: i = i' := Eq.symm eq1 + contradiction + have eq4: j = j' := Eq.symm eq2 + contradiction --- TODO: provide either a definition or some functional axioms (or a definition plus some lemmas) -axiom distinct : {a : Type} → List a → Prop +-- TODO: make this translate to the appropriate thing in SMT or prove some +-- theorems and include them as SMT axioms. +def distinct {a : Type} [BEq a] (xs: List a) : Prop := + match xs with + | [] => true + | x :: rest => x ∉ rest ∧ distinct rest axiom realToInt : Real → Int axiom intToReal : Int → Real From 359da35f8c7f5069f5866ba5455e7c12eea9b26f Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 11:24:15 -0800 Subject: [PATCH 19/30] Clean up lakefile --- Test/lean-auto/lakefile.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/Test/lean-auto/lakefile.lean b/Test/lean-auto/lakefile.lean index c5a3d2dbe..d86967b69 100644 --- a/Test/lean-auto/lakefile.lean +++ b/Test/lean-auto/lakefile.lean @@ -7,8 +7,3 @@ package «test» { require auto from git "https://github.com/leanprover-community/lean-auto"@"main" - ---@[default_target] ---lean_lib «Find» { --- -- add any library configuration options here ---} From 4fc941dda1a3dd7ee12e08388d07be669dc9d598 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 11:24:24 -0800 Subject: [PATCH 20/30] Fix Lean installation --- .github/workflows/test-lean-auto.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/test-lean-auto.yml b/.github/workflows/test-lean-auto.yml index 0065a187f..fa9c8307d 100644 --- a/.github/workflows/test-lean-auto.yml +++ b/.github/workflows/test-lean-auto.yml @@ -34,8 +34,9 @@ jobs: dotnet build -warnaserror Source/Boogie.sln - name: Setup Lean uses: actions/setup-lean@v1 - # Lean version will be chosen based on Test/lean-auto/lean-toolchain - working-directory: Test/lean-auto + with: + # Lean version will be chosen based on Test/lean-auto/lean-toolchain + default-toolchain-file: Test/lean-auto/lean-toolchain - name: Test Lean generator on textbook examples working-directory: Test/lean-auto run: | From bf46f9549356134bfda8d587d0d3740336f86f81 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 11:25:39 -0800 Subject: [PATCH 21/30] Change setup-lean action name --- .github/workflows/test-lean-auto.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-lean-auto.yml b/.github/workflows/test-lean-auto.yml index fa9c8307d..0b118e539 100644 --- a/.github/workflows/test-lean-auto.yml +++ b/.github/workflows/test-lean-auto.yml @@ -33,7 +33,7 @@ jobs: dotnet tool restore dotnet build -warnaserror Source/Boogie.sln - name: Setup Lean - uses: actions/setup-lean@v1 + uses: Julian/setup-lean@v1 with: # Lean version will be chosen based on Test/lean-auto/lean-toolchain default-toolchain-file: Test/lean-auto/lean-toolchain From 154fee435c645e1cf5ace0f98d87df1a6be7a0dd Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 11:30:18 -0800 Subject: [PATCH 22/30] Ensure Lean dependencies are actually built --- Test/lean-auto/ToBuild.lean | 1 + Test/lean-auto/lakefile.lean | 5 +++++ 2 files changed, 6 insertions(+) create mode 100644 Test/lean-auto/ToBuild.lean diff --git a/Test/lean-auto/ToBuild.lean b/Test/lean-auto/ToBuild.lean new file mode 100644 index 000000000..1bc751345 --- /dev/null +++ b/Test/lean-auto/ToBuild.lean @@ -0,0 +1 @@ +import Auto diff --git a/Test/lean-auto/lakefile.lean b/Test/lean-auto/lakefile.lean index d86967b69..9b51c835b 100644 --- a/Test/lean-auto/lakefile.lean +++ b/Test/lean-auto/lakefile.lean @@ -7,3 +7,8 @@ package «test» { require auto from git "https://github.com/leanprover-community/lean-auto"@"main" + +@[default_target] +lean_lib «ToBuild» { + -- add any library configuration options here +} From 9d58eb54f04d625080b583fb0f6029cb275da992 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 14 Feb 2024 14:04:56 -0800 Subject: [PATCH 23/30] Pin the version of lean-auto for reproducibility --- Source/Provers/LeanAuto/lakefile.lean | 2 +- Test/lean-auto/lake-manifest.json | 23 ----------------------- Test/lean-auto/lakefile.lean | 2 +- 3 files changed, 2 insertions(+), 25 deletions(-) delete mode 100644 Test/lean-auto/lake-manifest.json diff --git a/Source/Provers/LeanAuto/lakefile.lean b/Source/Provers/LeanAuto/lakefile.lean index 91898e289..b82b0c3e4 100644 --- a/Source/Provers/LeanAuto/lakefile.lean +++ b/Source/Provers/LeanAuto/lakefile.lean @@ -6,7 +6,7 @@ package «prelude» { } require auto from git - "https://github.com/leanprover-community/lean-auto"@"main" + "https://github.com/leanprover-community/lean-auto"@"v0.0.6" @[default_target] lean_lib «Prelude» { diff --git a/Test/lean-auto/lake-manifest.json b/Test/lean-auto/lake-manifest.json deleted file mode 100644 index 47bbee834..000000000 --- a/Test/lean-auto/lake-manifest.json +++ /dev/null @@ -1,23 +0,0 @@ -{"version": 7, - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover/std4.git", - "type": "git", - "subDir": null, - "rev": "276953b13323ca151939eafaaec9129bf7970306", - "name": "std", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0-rc1", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/lean-auto", - "type": "git", - "subDir": null, - "rev": "93105204453ca14cea9ae0c58bddb6809676db50", - "name": "auto", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}], - "name": "prelude", - "lakeDir": ".lake"} diff --git a/Test/lean-auto/lakefile.lean b/Test/lean-auto/lakefile.lean index 9b51c835b..6bc2f376f 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"@"main" + "https://github.com/leanprover-community/lean-auto"@"v0.0.6" @[default_target] lean_lib «ToBuild» { From a2a40d6352ffd24130dddea18c70048010e1a7a9 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 6 Mar 2024 11:25:42 -0800 Subject: [PATCH 24/30] Rename LeanGenerator -> LeanAutoGenerator --- Source/ExecutionEngine/ExecutionEngine.cs | 2 +- .../Provers/LeanAuto/{LeanAuto.cs => LeanAutoGenerator.cs} | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) rename Source/Provers/LeanAuto/{LeanAuto.cs => LeanAutoGenerator.cs} (99%) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 661ad4a15..260abbd02 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -578,7 +578,7 @@ public async Task InferAndVerify( if (Options.LeanFile is not null) { var writer = new StreamWriter(Options.LeanFile); - LeanGenerator.EmitPassiveProgramAsLean(Options, processedProgram.Program, writer); + LeanAutoGenerator.EmitPassiveProgramAsLean(Options, processedProgram.Program, writer); writer.Close(); } diff --git a/Source/Provers/LeanAuto/LeanAuto.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs similarity index 99% rename from Source/Provers/LeanAuto/LeanAuto.cs rename to Source/Provers/LeanAuto/LeanAutoGenerator.cs index 956989630..6de6f9538 100644 --- a/Source/Provers/LeanAuto/LeanAuto.cs +++ b/Source/Provers/LeanAuto/LeanAutoGenerator.cs @@ -14,7 +14,7 @@ public LeanConversionException(IToken tok, string s) } } -public class LeanGenerator : ReadOnlyVisitor +public class LeanAutoGenerator : ReadOnlyVisitor { private readonly TextWriter writer; private readonly VCGenOptions options; @@ -35,7 +35,7 @@ public class LeanGenerator : ReadOnlyVisitor private const string NeqString = "\u2260"; /* ≠ */ private const string ArrowString = "\u2192"; /* → */ - private LeanGenerator(VCGenOptions options, TextWriter writer) + private LeanAutoGenerator(VCGenOptions options, TextWriter writer) { this.options = options; this.writer = writer; @@ -43,7 +43,7 @@ private LeanGenerator(VCGenOptions options, TextWriter writer) public static void EmitPassiveProgramAsLean(VCGenOptions options, Program p, TextWriter writer) { - var generator = new LeanGenerator(options, writer); + var generator = new LeanAutoGenerator(options, writer); generator.EmitHeader(); try { var allBlocks = p.Implementations.SelectMany(i => i.Blocks); From 49e1eec7eecfb5420be7e530942c4643af911eab Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 6 Mar 2024 11:52:59 -0800 Subject: [PATCH 25/30] Rename some methods --- Source/Provers/LeanAuto/LeanAutoGenerator.cs | 270 +++++++++---------- 1 file changed, 135 insertions(+), 135 deletions(-) diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs index 6de6f9538..cb09966c4 100644 --- a/Source/Provers/LeanAuto/LeanAutoGenerator.cs +++ b/Source/Provers/LeanAuto/LeanAutoGenerator.cs @@ -52,36 +52,36 @@ public static void EmitPassiveProgramAsLean(VCGenOptions options, Program p, Tex ? Prune.GetLiveDeclarations(options, p, allBlocks.ToList()).ToList() : p.TopLevelDeclarations; - generator.Line("-- Type constructors"); + generator.WriteLine("-- Type constructors"); // Always include all type constructors p.TopLevelDeclarations.OfType().ForEach(tcd => generator.Visit(tcd)); - generator.NL(); + generator.WriteLine(); - generator.Line("-- Type synonyms"); + generator.WriteLine("-- Type synonyms"); liveDeclarations.OfType().ForEach(tcd => generator.Visit(tcd)); - generator.NL(); + generator.WriteLine(); - generator.Line("-- Constants"); + generator.WriteLine("-- Constants"); liveDeclarations.OfType().ForEach(c => generator.Visit(c)); - generator.NL(); + generator.WriteLine(); - generator.Line("-- Unique const axioms"); + generator.WriteLine("-- Unique const axioms"); generator.EmitUniqueConstAxioms(); - generator.NL(); + generator.WriteLine(); - generator.Line("-- Variables"); + generator.WriteLine("-- Variables"); liveDeclarations.OfType().ForEach(gv => generator.Visit(gv)); - generator.NL(); + generator.WriteLine(); - generator.Line("-- Functions"); + generator.WriteLine("-- Functions"); liveDeclarations.OfType().ForEach(f => generator.Visit(f)); - generator.NL(); + generator.WriteLine(); - generator.Line("-- Axioms"); + generator.WriteLine("-- Axioms"); liveDeclarations.OfType().ForEach(a => generator.Visit(a)); - generator.NL(); + generator.WriteLine(); - generator.Line("-- Implementations"); + generator.WriteLine("-- Implementations"); p.Implementations.ForEach(i => generator.Visit(i)); } catch (LeanConversionException e) { Console.WriteLine($"Failed translation: {e.Msg}"); @@ -105,9 +105,9 @@ private void EmitUniqueConstAxioms() foreach (var kv in uniqueConsts) { var axiomName = $"unique{i}"; userAxiomNames.Add(axiomName); - Text($"axiom {axiomName}: distinct "); - List(kv.Value); - NL(); + WriteText($"axiom {axiomName}: distinct "); + WriteList(kv.Value); + WriteLine(); i++; } } @@ -126,46 +126,46 @@ private void EmitHeader() private void Indent(int n = 1, string str = null) { - Text(String.Concat(Enumerable.Repeat(" ", n))); + WriteText(String.Concat(Enumerable.Repeat(" ", n))); if (str is not null) { - Text(str); + WriteText(str); } } - private void IndentL(int n = 1, string str = null) + private void IndentLine(int n = 1, string str = null) { Indent(n, str); - NL(); + WriteLine(); } - private void NL() + private void WriteLine() { writer.WriteLine(); } - private void Text(string text) + private void WriteText(string text) { writer.Write(text); } - private void Line(string text) + private void WriteLine(string text) { writer.WriteLine(text); } - private void List(IEnumerable strings) + private void WriteList(IEnumerable strings) { - Text("["); - Text(String.Join(", ", strings)); - Text("]"); + WriteText("["); + WriteText(String.Join(", ", strings)); + WriteText("]"); } public override Block VisitBlock(Block node) { var label = BlockName(node); - IndentL(1, "@[simp]"); - IndentL(1, $"{label} :="); + IndentLine(1, "@[simp]"); + IndentLine(1, $"{label} :="); node.Cmds.ForEach(c => Visit(c)); if (node.TransferCmd is ReturnCmd r) { VisitReturnCmd(r); @@ -175,7 +175,7 @@ public override Block VisitBlock(Block node) throw new LeanConversionException(node.TransferCmd.tok, $"Unsupported transfer command: {node.TransferCmd}"); } - NL(); + WriteLine(); return node; } @@ -183,7 +183,7 @@ public override Cmd VisitAssertCmd(AssertCmd node) { Indent(2, "assert "); VisitExpr(node.Expr); - Line(" $"); + WriteLine(" $"); return node; } @@ -191,7 +191,7 @@ public override Cmd VisitAssumeCmd(AssumeCmd node) { Indent(2, "assume "); VisitExpr(node.Expr); - Line(" $"); + WriteLine(" $"); return node; } @@ -213,7 +213,7 @@ public override Expr VisitIdentifierExpr(IdentifierExpr node) { var name = SanitizeNameForLean(node.Name); usedNames.Add(name); - Text(name); + WriteText(name); return node; } @@ -239,11 +239,11 @@ public override Type VisitType(Type node) public override Type VisitBasicType(BasicType node) { if (node.IsBool) { - Text("Prop"); + WriteText("Prop"); } else if (node.IsInt) { - Text("Int"); + WriteText("Int"); } else if (node.IsReal) { - Text("Real"); + WriteText("Real"); } else if (node.IsRMode) { throw new LeanConversionException(node.tok, "Unsupported type: RMode."); } else if (node.IsRegEx) { @@ -261,26 +261,26 @@ public override Type VisitBasicType(BasicType node) public override Expr VisitBvConcatExpr(BvConcatExpr node) { Visit(node.E0); - Text(" ++ "); + WriteText(" ++ "); Visit(node.E1); return node; } public override Type VisitBvType(BvType node) { - Text($"(BitVec {node.Bits})"); + WriteText($"(BitVec {node.Bits})"); return node; } public override Constant VisitConstant(Constant node) { var ti = node.TypedIdent; - Text("variable "); + WriteText("variable "); Visit(ti); if (node.Unique) { AddUniqueConst(ti.Type, Name(node)); } - NL(); + WriteLine(); globalVars.Add(node); return node; } @@ -288,17 +288,17 @@ public override Constant VisitConstant(Constant node) public override CtorType VisitCtorType(CtorType node) { if (node.Arguments.Any()) { - Text("("); + WriteText("("); } - Text(Name(node.Decl)); + WriteText(Name(node.Decl)); node.Arguments.ForEach(a => { - Text(" "); + WriteText(" "); Visit(a); }); if (node.Arguments.Any()) { - Text(")"); + WriteText(")"); } return node; } @@ -312,47 +312,47 @@ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) _ => throw new LeanConversionException(node.tok, $"Unsupported quantifier type: {node.Kind}") }; - Text($"({kind}"); + WriteText($"({kind}"); foreach (var tv in node.TypeParameters) { - Text($" ({Name(tv)} : Type)"); + WriteText($" ({Name(tv)} : Type)"); } foreach (var x in node.Dummies) { - Text(" "); + WriteText(" "); VisitTypedIdent(x.TypedIdent); } - Text(", "); + WriteText(", "); Visit(node.Body); - Text(")"); + WriteText(")"); return node; } public override TypedIdent VisitTypedIdent(TypedIdent node) { - Text("("); + WriteText("("); var name = SanitizeNameForLean(node.Name); - Text(name); - Text(" : "); + WriteText(name); + WriteText(" : "); Visit(node.Type); - Text(")"); + WriteText(")"); return node; } public override Expr VisitBvExtractExpr(BvExtractExpr node) { - Text($"(BitVec.extractLsb {node.End - 1} {node.Start} "); + WriteText($"(BitVec.extractLsb {node.End - 1} {node.Start} "); Visit(node.Bitvector); - Text(")"); + WriteText(")"); return node; } public override Expr VisitLambdaExpr(LambdaExpr node) { - Text("(λ"); + WriteText("(λ"); node.Dummies.ForEach(x => Visit(x.TypedIdent)); - Text("=>"); + WriteText("=>"); Visit(node.Body); - Text(")"); + WriteText(")"); return node; } @@ -362,21 +362,21 @@ public override Expr VisitLetExpr(LetExpr node) throw new LeanConversionException(node.tok, "Unsupported: LetExpr with more than one binder"); } - Text("(let"); + WriteText("(let"); node.Dummies.ForEach(x => Visit(x.TypedIdent)); - Text(" := "); + WriteText(" := "); node.Rhss.ForEach(e => Visit(e)); - Text("; "); + WriteText("; "); Visit(node.Body); - Text(")"); + WriteText(")"); return node; } public override GlobalVariable VisitGlobalVariable(GlobalVariable node) { - Text("variable "); + WriteText("variable "); Visit(node.TypedIdent); - NL(); + WriteLine(); globalVars.Add(node); return node; } @@ -385,22 +385,22 @@ public override Expr VisitLiteralExpr(LiteralExpr node) { if(node.IsTrue) { // Use lowercase version to ensure Bool, which can be coerced to Prop - Text("true"); + WriteText("true"); } else if (node.IsFalse) { // Use lowercase version to ensure Bool, which can be coerced to Prop - Text("false"); + WriteText("false"); } else if (node.isBvConst) { var bvConst = node.asBvConst; - Text("("); - Text(bvConst.Value.ToString()); - Text($" : BitVec {bvConst.Bits}"); - Text(")"); + WriteText("("); + WriteText(bvConst.Value.ToString()); + WriteText($" : BitVec {bvConst.Bits}"); + WriteText(")"); } else if (node.isBigDec) { throw new LeanConversionException(node.tok, "Unsupported literal: BigDec"); } else if (node.isBigNum) { var bigNumConst = node.asBigNum; - Text(bigNumConst.ToString()); + WriteText(bigNumConst.ToString()); } else if (node.isBigFloat) { throw new LeanConversionException(node.tok, "Unsupported literal: BigFloat"); @@ -422,16 +422,16 @@ public override Type VisitMapType(MapType node) } if (node.TypeParameters.Any()) { var args = node.TypeParameters.Select(Name); - Text($"forall ({String.Join(" ", args)} : Type), "); + WriteText($"forall ({String.Join(" ", args)} : Type), "); } - Text($"(SMTArray{node.Arguments.Count} "); + WriteText($"(SMTArray{node.Arguments.Count} "); node.Arguments.ForEach(a => { Visit(a); - Text(" "); + WriteText(" "); }); Visit(node.Result); - Text(")"); + WriteText(")"); return node; } @@ -439,10 +439,10 @@ public override Expr VisitNAryExpr(NAryExpr node) { var fun = node.Fun; var args = node.Args; - Text("("); + WriteText("("); if (fun is BinaryOperator op && args.Count == 2) { Visit(args[0]); - Text($" {BinaryOpToLean(op.Op)} "); + WriteText($" {BinaryOpToLean(op.Op)} "); Visit(args[1]); } else if (fun is FieldAccess fieldAccess) { throw new LeanConversionException(node.tok, @@ -451,30 +451,30 @@ public override Expr VisitNAryExpr(NAryExpr node) throw new LeanConversionException(node.tok, "Unsupported: field update (since the semantics are complex)"); } else if (fun is IfThenElse && args.Count == 3) { - Text("if "); + WriteText("if "); Visit(args[0]); - Text(" then "); + WriteText(" then "); Visit(args[1]); - Text(" else "); + WriteText(" else "); Visit(args[2]); } else if (fun is TypeCoercion typeCoercion && args.Count == 1) { if (!args[0].Type.Equals(typeCoercion.Type)) { // TODO: might need to actually call a coercion function Console.WriteLine($"Coerce: {args[0].Type} -> {typeCoercion.Type}"); } - Text("("); + WriteText("("); Visit(args[0]); - Text(" : "); + WriteText(" : "); Visit(typeCoercion.Type); - Text(")"); + WriteText(")"); } else { VisitIAppliable(fun); foreach (var arg in args) { - Text(" "); + WriteText(" "); Visit(arg); } } - Text(")"); + WriteText(")"); return node; } @@ -490,13 +490,13 @@ private void VisitIAppliable(IAppliable fun) _ => throw new LeanConversionException(Token.NoToken, $"Internal: unknown arithmetic coercion: {arithmeticCoercion.Coercion}") }; - Text(func); + WriteText(func); break; case BinaryOperator op: - Text(BinaryOpToLean(op.Op)); + WriteText(BinaryOpToLean(op.Op)); break; case FunctionCall fc: - Text(Name(fc.Func)); + WriteText(Name(fc.Func)); break; case IsConstructor isConstructor: throw new LeanConversionException(isConstructor.tok, @@ -506,14 +506,14 @@ private void VisitIAppliable(IAppliable fun) //break; case MapSelect: usesMaps = true; - Text($"select{fun.ArgumentCount - 1}"); + WriteText($"select{fun.ArgumentCount - 1}"); break; case MapStore: usesMaps = true; - Text($"store{fun.ArgumentCount - 2}"); + WriteText($"store{fun.ArgumentCount - 2}"); break; case UnaryOperator op: - Text(UnaryOpToLean(op.Op)); + WriteText(UnaryOpToLean(op.Op)); break; default: throw new LeanConversionException(Token.NoToken, @@ -588,22 +588,22 @@ public override Declaration VisitTypeCtorDecl(TypeCtorDecl node) // TODO: wrap in `mutual ... end` when necessary var name = Name(node); if (node is DatatypeTypeCtorDecl dt) { - Line($"inductive {name} where"); + WriteLine($"inductive {name} where"); foreach (var ctor in dt.Constructors) { Indent(1, $"| {Name(ctor)} : "); ctor.InParams.ForEach(p => { Visit(p.TypedIdent.Type); - Text(" → "); + WriteText(" → "); }); - Line($" {name}"); + WriteLine($" {name}"); } } else { var tyStr = String.Join(" → ", Enumerable.Repeat("Type", node.Arity + 1).ToList()); - Line($"axiom {name} : {tyStr}"); + WriteLine($"axiom {name} : {tyStr}"); if(node.Arity == 0) { - Line($"instance {name}BEq : BEq {name} := by sorry"); + WriteLine($"instance {name}BEq : BEq {name} := by sorry"); } } return node; @@ -617,11 +617,11 @@ public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) public override Declaration VisitTypeSynonymDecl(TypeSynonymDecl node) { var name = Name(node); - Text($"def {name}"); - node.TypeParameters.ForEach(tp => Text($" ({Name(tp)} : Type)")); - Text(" := "); + WriteText($"def {name}"); + node.TypeParameters.ForEach(tp => WriteText($" ({Name(tp)} : Type)")); + WriteText(" := "); Visit(node.Body); - NL(); + WriteLine(); return node; } @@ -629,7 +629,7 @@ public override Type VisitTypeProxy(TypeProxy node) { var p = node.ProxyFor; if (p is null) { - Text(Name(node)); + WriteText(Name(node)); } else { VisitType(p); } @@ -638,7 +638,7 @@ public override Type VisitTypeProxy(TypeProxy node) public override Type VisitTypeVariable(TypeVariable node) { - Text(Name(node)); + WriteText(Name(node)); return node; } @@ -646,7 +646,7 @@ public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) { Indent(2, "assert "); VisitExpr(node.Expr); - Line(" $"); + WriteLine(" $"); return node; } @@ -654,7 +654,7 @@ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) { Indent(2, "assert "); VisitExpr(node.Expr); - Line(" $"); + WriteLine(" $"); return node; } @@ -684,9 +684,9 @@ public override Axiom VisitAxiom(Axiom node) name = $"ax_l{node.tok.line}c{node.tok.col}_{n}"; n += 1; } - Text($"axiom {name}: "); + WriteText($"axiom {name}: "); VisitExpr(node.Expr); - NL(); + WriteLine(); userAxiomNames.Add(name); return node; } @@ -694,29 +694,29 @@ public override Axiom VisitAxiom(Axiom node) public override Function VisitFunction(Function node) { // In the long run, this should define functions when possible. - Text($"axiom {Name(node)} : "); + WriteText($"axiom {Name(node)} : "); node.TypeParameters.ForEach(x => { - Text($"{{{Name(x)} : Type}}"); - Text($" {ArrowString} "); + WriteText($"{{{Name(x)} : Type}}"); + WriteText($" {ArrowString} "); }); node.InParams.ForEach(x => { Visit(x.TypedIdent.Type); - Text($" {ArrowString} "); + WriteText($" {ArrowString} "); }); if (node.OutParams.Count == 1) { Visit(node.OutParams[0].TypedIdent.Type); } else { - Text("("); + WriteText("("); node.OutParams.ForEach(x => { - Visit(x.TypedIdent.Type); Text(", "); + Visit(x.TypedIdent.Type); WriteText(", "); }); - Text(")"); + WriteText(")"); } - NL(); + WriteLine(); // Note: definition axioms will be emitted later // node.DefinitionAxioms.ForEach(ax => VisitAxiom(ax)); return node; @@ -800,19 +800,19 @@ private void WriteParams(Implementation node) { Indent(); VisitTypedIdent(x.TypedIdent); - NL(); + WriteLine(); }); node.OutParams.ForEach(x => { Indent(); VisitTypedIdent(x.TypedIdent); - NL(); + WriteLine(); }); node.LocVars.ForEach(x => { Indent(); VisitTypedIdent(x.TypedIdent); - NL(); + WriteLine(); }); } @@ -822,18 +822,18 @@ public override Implementation VisitImplementation(Implementation node) var entryLabel = BlockName(node.Blocks[0]); usedNames.Clear(); // Skip any globals used only by axioms, etc. - NL(); - Line($"namespace impl_{name}"); - NL(); + WriteLine(); + WriteLine($"namespace impl_{name}"); + WriteLine(); - Line("@[simp]"); - Line($"def {name}"); + WriteLine("@[simp]"); + WriteLine($"def {name}"); WriteParams(node); - IndentL(1, $": Prop := {entryLabel}"); - IndentL(1, "where"); + IndentLine(1, $": Prop := {entryLabel}"); + IndentLine(1, "where"); node.Blocks.ForEach(b => VisitBlock(b)); - NL(); - Line($"theorem {name}_correct"); + WriteLine(); + WriteLine($"theorem {name}_correct"); WriteParams(node); var paramNames = globalVars.Select(Name).Where(x => usedNames.Contains(x)) @@ -841,14 +841,14 @@ public override Implementation VisitImplementation(Implementation node) .Concat(node.OutParams.Select(Name)) .Concat(node.LocVars.Select(Name)); var paramString = String.Join(' ', paramNames); - Indent(1, $": {name} {paramString} := by"); NL(); - IndentL(2, "try simp"); // Uses `try` because it may make no progress - IndentL(2, "try auto"); // Uses `try` because there may be no goals remaining + Indent(1, $": {name} {paramString} := by"); WriteLine(); + IndentLine(2, "try simp"); // Uses `try` because it may make no progress + IndentLine(2, "try auto"); // Uses `try` because there may be no goals remaining var axiomNames = usesMaps ? mapAxiomNames.Concat(userAxiomNames) : userAxiomNames; - Indent(3); List(axiomNames); NL(); - IndentL(3, "u[]"); - NL(); - Line($"end impl_{name}"); + Indent(3); WriteList(axiomNames); WriteLine(); + IndentLine(3, "u[]"); + WriteLine(); + WriteLine($"end impl_{name}"); usesMaps = false; // Skip map axioms in the next implementation if it doesn't need them usedNames.Clear(); // Skip any globals not used by the next implementation From 2f8b3a968a392fe67246faa9f5e39760208ee748 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 6 Mar 2024 11:53:53 -0800 Subject: [PATCH 26/30] Move use of passive program to a separate method --- Source/ExecutionEngine/ExecutionEngine.cs | 27 +++++++++++++++-------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 260abbd02..4b6f0679f 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -571,16 +571,11 @@ public async Task InferAndVerify( } var outcome = await VerifyEachImplementation(output, processedProgram, stats, programId, er, requestId, stablePrioritizedImpls); - if (Options.PrintPassive) { - Options.PrintUnstructured = 1; - PrintBplFile(Options.PrintFile, processedProgram.Program, true, true, Options.PrettyPrint); - } - if (Options.LeanFile is not null) { - var writer = new StreamWriter(Options.LeanFile); - LeanAutoGenerator.EmitPassiveProgramAsLean(Options, processedProgram.Program, writer); - writer.Close(); - } + // We unfortunately have to do any processing of the passive program after verification, + // because passification happens during verification. Refactoring the code to passify + // the program as an independent step would be a valuable thing to do eventually. + UsePassiveProgram(processedProgram.Program); if (1 < Options.VerifySnapshots && programId != null) { @@ -593,6 +588,20 @@ public async Task InferAndVerify( return outcome; } + private void UsePassiveProgram(Program passiveProgram) + { + if (Options.PrintPassive) { + Options.PrintUnstructured = 1; + PrintBplFile(Options.PrintFile, passiveProgram, true, true, Options.PrettyPrint); + } + + if (Options.LeanFile is not null) { + var writer = new StreamWriter(Options.LeanFile); + LeanAutoGenerator.EmitPassiveProgramAsLean(Options, passiveProgram, writer); + writer.Close(); + } + } + private ProcessedProgram PreProcessProgramVerification(Program program) { // Doing lambda expansion before abstract interpretation means that the abstract interpreter From fd7b4c9e1bba4a2ddf14283017010345ef7d4170 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 7 Mar 2024 15:54:13 -0800 Subject: [PATCH 27/30] Clarify comment --- Source/ExecutionEngine/ExecutionEngine.cs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 4b6f0679f..2f39df001 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -572,9 +572,10 @@ public async Task InferAndVerify( var outcome = await VerifyEachImplementation(output, processedProgram, stats, programId, er, requestId, stablePrioritizedImpls); - // We unfortunately have to do any processing of the passive program after verification, - // because passification happens during verification. Refactoring the code to passify - // the program as an independent step would be a valuable thing to do eventually. + // We unfortunately have to do any processing of the passive program + // after running VerifyEachImplementation, because it passifies the + // program in place. We should eventually refactor the code to + // passify the program as an independent step. UsePassiveProgram(processedProgram.Program); if (1 < Options.VerifySnapshots && programId != null) From 4cc7547fba84cec0423fb9d87596b003d5ba2fa5 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 19 Mar 2024 13:55:27 -0700 Subject: [PATCH 28/30] Generalized processing of passive programs --- Source/ExecutionEngine/CommandLineOptions.cs | 45 ++++++++++++++++--- Source/ExecutionEngine/ExecutionEngine.cs | 24 ++-------- .../ExecutionEngine/ExecutionEngineOptions.cs | 3 +- 3 files changed, 45 insertions(+), 27 deletions(-) diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index db3811be4..5c1966e04 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -3,7 +3,9 @@ using System.Collections.Specialized; using System.Diagnostics.Contracts; using System.IO; +using Microsoft.Boogie.LeanAuto; using Microsoft.Boogie.SMTLib; +using VC; namespace Microsoft.Boogie { @@ -64,7 +66,6 @@ void ObjectInvariant2() public bool VerifySeparately { get; set; } public string PrintFile { get; set; } public string PrintPrunedFile { get; set; } - public string LeanFile { get; set; } /** * Whether to emit {:qid}, {:skolemid} and set-info :boogie-vc-id @@ -92,6 +93,37 @@ public bool PrintPassive { set => printPassive = value; } + public List> UseResolvedProgram { get; } = new(); + + static void PassifyAllImplementations(ExecutionEngineOptions options, ProcessedProgram processedProgram) + { + // All three of these objects can be new instances because they're essentially not used by PrepareImplementation. + var callback = new VerifierCallback(options.PrintProverWarnings); + var checkerPool = new CheckerPool(options); + var vcGenerator = new VerificationConditionGenerator(processedProgram.Program, checkerPool); + + foreach(var implementation in processedProgram.Program.Implementations) { + vcGenerator.PrepareImplementation(new ImplementationRun(implementation, options.OutputWriter), + callback, out _, out _, out _); + } + } + + public static void PrintPassiveProgram(ExecutionEngineOptions options, ProcessedProgram processedProgram) + { + options.PrintUnstructured = 1; + PassifyAllImplementations(options, processedProgram); + ExecutionEngine.PrintBplFile(options, options.PrintFile, processedProgram.Program, true, true, options.PrettyPrint); + } + + public static void PrintPassiveProgramAsLean(string fileName, ExecutionEngineOptions options, ProcessedProgram processedProgram) + { + var writer = new StreamWriter(fileName); + PassifyAllImplementations(options, processedProgram); + LeanAutoGenerator.EmitPassiveProgramAsLean(options, processedProgram.Program, writer); + writer.Close(); + + } + public bool PrintLambdaLifting { get; set; } public bool FreeVarLambdaLifting { get; set; } public string ProverLogFilePath { get; set; } @@ -406,7 +438,7 @@ public bool TrustRefinement { get => trustRefinement; set => trustRefinement = value; } - + public int TrustLayersUpto { get; set; } = -1; public int TrustLayersDownto { get; set; } = int.MaxValue; @@ -682,9 +714,10 @@ protected override bool ParseOption(string name, CommandLineParseState ps) return true; case "printLean": - if (ps.ConfirmArgumentCount(1)) - { - LeanFile = args[ps.i]; + if (ps.ConfirmArgumentCount(1)) { + var fileName = args[ps.i]; + UseResolvedProgram.Add((o, p) => + PrintPassiveProgramAsLean(fileName, o, p)); } return true; @@ -1285,7 +1318,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps) if (ps.CheckBooleanFlag("printDesugared", x => printDesugarings = x) || ps.CheckBooleanFlag("printLambdaLifting", x => PrintLambdaLifting = x) || ps.CheckBooleanFlag("printInstrumented", x => printInstrumented = x) || - ps.CheckBooleanFlag("printPassive", x => printPassive = x) || + ps.CheckBooleanFlag("printPassive", x => UseResolvedProgram.Add(PrintPassiveProgram)) || ps.CheckBooleanFlag("printWithUniqueIds", x => printWithUniqueAstIds = x) || ps.CheckBooleanFlag("wait", x => Wait = x) || ps.CheckBooleanFlag("trace", x => Verbosity = CoreOptions.VerbosityLevel.Trace) || diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 890101f99..09bfb4cd1 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -553,6 +553,10 @@ public async Task InferAndVerify( var processedProgram = PreProcessProgramVerification(program); + if (Options.UseResolvedProgram.Any()) { + Options.UseResolvedProgram.ForEach(action => action(Options, processedProgram)); + } + if (!Options.Verify) { return PipelineOutcome.Done; @@ -572,12 +576,6 @@ public async Task InferAndVerify( var outcome = await VerifyEachImplementation(output, processedProgram, stats, programId, er, requestId, stablePrioritizedImpls); - // We unfortunately have to do any processing of the passive program - // after running VerifyEachImplementation, because it passifies the - // program in place. We should eventually refactor the code to - // passify the program as an independent step. - UsePassiveProgram(processedProgram.Program); - if (1 < Options.VerifySnapshots && programId != null) { program.FreezeTopLevelDeclarations(); @@ -589,20 +587,6 @@ public async Task InferAndVerify( return outcome; } - private void UsePassiveProgram(Program passiveProgram) - { - if (Options.PrintPassive) { - Options.PrintUnstructured = 1; - PrintBplFile(Options.PrintFile, passiveProgram, true, true, Options.PrettyPrint); - } - - if (Options.LeanFile is not null) { - var writer = new StreamWriter(Options.LeanFile); - LeanAutoGenerator.EmitPassiveProgramAsLean(Options, passiveProgram, writer); - writer.Close(); - } - } - private ProcessedProgram PreProcessProgramVerification(Program program) { // Doing lambda expansion before abstract interpretation means that the abstract interpreter diff --git a/Source/ExecutionEngine/ExecutionEngineOptions.cs b/Source/ExecutionEngine/ExecutionEngineOptions.cs index e65435dc7..d18eda87e 100644 --- a/Source/ExecutionEngine/ExecutionEngineOptions.cs +++ b/Source/ExecutionEngine/ExecutionEngineOptions.cs @@ -14,7 +14,8 @@ public interface ExecutionEngineOptions : HoudiniOptions, ConcurrencyOptions string DescriptiveToolName { get; } bool TraceProofObligations { get; } string PrintFile { get; } - string LeanFile { get; } + List> UseResolvedProgram { get; } + string PrintCFGPrefix { get; } string CivlDesugaredFile { get; } bool CoalesceBlocks { get; } From 29979dc812de2c8d19edc426c455b87b7c105d98 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 19 Mar 2024 13:59:50 -0700 Subject: [PATCH 29/30] Allow `goto` to have no targets --- Source/Provers/LeanAuto/LeanAutoGenerator.cs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs index cb09966c4..bd9712afb 100644 --- a/Source/Provers/LeanAuto/LeanAutoGenerator.cs +++ b/Source/Provers/LeanAuto/LeanAutoGenerator.cs @@ -197,9 +197,13 @@ public override Cmd VisitAssumeCmd(AssumeCmd node) public override GotoCmd VisitGotoCmd(GotoCmd node) { - var gotoText = node.labelTargets.Select(l => - $"goto {BlockName(l)}").Aggregate((a, b) => $"{a} {AndString} {b}"); - Indent(2, gotoText); + string cmd = node.labelTargets.Any() + ? node + .labelTargets + .Select(l => $"goto {BlockName(l)}") + .Aggregate((a, b) => $"{a} {AndString} {b}") + : "ret"; + Indent(2, cmd); return node; } From fbafb12d0dd3623d7c98156b910118eb5479b047 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 19 Mar 2024 14:54:58 -0700 Subject: [PATCH 30/30] Use `foreach` instead of `ForEach` --- Source/ExecutionEngine/ExecutionEngine.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 09bfb4cd1..25553a0a0 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -553,8 +553,8 @@ public async Task InferAndVerify( var processedProgram = PreProcessProgramVerification(program); - if (Options.UseResolvedProgram.Any()) { - Options.UseResolvedProgram.ForEach(action => action(Options, processedProgram)); + foreach (var action in Options.UseResolvedProgram) { + action(Options, processedProgram); } if (!Options.Verify)