Add an experimental backend that uses Lean to discharge goals

.github/workflows/test-lean-auto.yml

@@ -0,0 +1,44 @@
+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: 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
+      - name: Test Lean generator on textbook examples
+        working-directory: Test/lean-auto
+        run: |
+          lake build
+          ./testall.sh

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,12 +296,25 @@ 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}
 		{65A3F7E9-3E13-4C26-A72A-F60B9943E1B2} = {91134A3E-0D5D-4017-B04E-48BA254B3CF8}
 		{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

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]

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
 {
@@ -91,6 +93,37 @@ public bool PrintPassive {
       set => printPassive = value;
     }
 
+    public List<Action<ExecutionEngineOptions, ProcessedProgram>> 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; }
@@ -405,7 +438,7 @@ public bool TrustRefinement {
       get => trustRefinement;
       set => trustRefinement = value;
     }
-    
+
     public int TrustLayersUpto { get; set; } = -1;
 
     public int TrustLayersDownto { get; set; } = int.MaxValue;
@@ -680,6 +713,15 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
 
           return true;
 
+        case "printLean":
+          if (ps.ConfirmArgumentCount(1)) {
+            var fileName = args[ps.i];
+            UseResolvedProgram.Add((o, p) =>
+              PrintPassiveProgramAsLean(fileName, o, p));
+          }
+
+          return true;
+
         case "pretty":
           int val = 1;
           if (ps.GetIntArgument(x => val = x, 2))
@@ -1276,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) ||

Source/ExecutionEngine/ExecutionEngine.cs

@@ -7,14 +7,13 @@
 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 Microsoft.Boogie.VCExprAST;
 using VCGeneration;
 
 namespace Microsoft.Boogie
@@ -554,6 +553,10 @@ public async Task<PipelineOutcome> InferAndVerify(
 
       var processedProgram = PreProcessProgramVerification(program);
 
+      foreach (var action in Options.UseResolvedProgram) {
+        action(Options, processedProgram);
+      }
+
       if (!Options.Verify)
       {
         return PipelineOutcome.Done;
@@ -572,10 +575,6 @@ public async Task<PipelineOutcome> 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 (1 < Options.VerifySnapshots && programId != null)
       {

Source/ExecutionEngine/ExecutionEngine.csproj

@@ -20,6 +20,7 @@
     <ProjectReference Include="..\Graph\Graph.csproj" />
     <ProjectReference Include="..\Houdini\Houdini.csproj" />
     <ProjectReference Include="..\Model\Model.csproj" />
+    <ProjectReference Include="..\Provers\LeanAuto\LeanAuto.csproj" />
     <ProjectReference Include="..\VCGeneration\VCGeneration.csproj" />
     <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj" />
   </ItemGroup>

Source/ExecutionEngine/ExecutionEngineOptions.cs

@@ -14,6 +14,8 @@ public interface ExecutionEngineOptions : HoudiniOptions, ConcurrencyOptions
   string DescriptiveToolName { get; }
   bool TraceProofObligations { get; }
   string PrintFile { get; }
+  List<Action<ExecutionEngineOptions, ProcessedProgram>> UseResolvedProgram { get; }
+
   string PrintCFGPrefix { get; }
   string CivlDesugaredFile { get; }
   bool CoalesceBlocks { get; }

Source/Provers/LeanAuto/.gitignore

@@ -0,0 +1,2 @@
+.lake
+lake-manifest.json

Source/Provers/LeanAuto/LeanAuto.csproj

@@ -0,0 +1,25 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+  <PropertyGroup>
+    <OutputType>Library</OutputType>
+    <AssemblyName>Boogie.Provers.LeanAuto</AssemblyName>
+  </PropertyGroup>
+
+  <ItemGroup>
+    <ProjectReference Include="..\..\BaseTypes\BaseTypes.csproj" />
+    <ProjectReference Include="..\..\CodeContractsExtender\CodeContractsExtender.csproj" />
+    <ProjectReference Include="..\..\Core\Core.csproj" />
+    <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj" />
+  </ItemGroup>
+
+  <ItemGroup>
+    <PackageReference Include="System.Linq.Async" Version="6.0.1" />
+  </ItemGroup>
+
+  <ItemGroup>
+    <EmbeddedResource Include="Prelude.lean">
+      <LogicalName>Prelude.lean</LogicalName>
+    </EmbeddedResource>
+  </ItemGroup>
+
+</Project>