Add an experimental backend that uses Lean to discharge goals #850
Conversation
Currently undocumented. Change that eventually.
BQueue uses a lot of features and is rejected by the translator for now.
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.
atomb
changed the title
Any chance you could write this as a plugin, so that no references from the existing Boogie projects are made to the code of this PR, and this PR can be compiled as a separate .dll that can be included or omitted? That would also allow you to bypass a code review for this PR, because you could put the code in a separate repository. With this PR being in this repository, I think it's better to do a code review at the same bar as any other PR. Given that, could you add tests? |
Unfortunately, I don't believe the current plugin infrastructure operates at the right stage in the verification pipeline, at least as this new code is currently written. There is some refactoring I think I'll eventually do that might make it able to fit in as a plugin, but a number of external things need to change before I think that'll be feasible. And I'd rather not have this code stay separate from CI and code review until then.
This PR has tests, running in a new CI job (but located under the |
I have considered the idea of making this an entirely separate top-level executable which uses Boogie as a library and behaves just like the normal Boogie other than having support for an additional option. I'm definitely still open to doing that, and that would allow it to live in a separate repository. |
| @@ -577,6 +576,12 @@ public void Inline(Program program) | |||
| PrintBplFile(Options.PrintFile, processedProgram.Program, true, true, Options.PrettyPrint); | |||
| } | |||
|
|
|||
| if (Options.LeanFile is not null) { | |||
There was a problem hiding this comment.
I think adding more and more features to existing methods, like what happens here, makes the code less and less readable. Consider making this pipeline pluggable, so you can write the new code somewhere else.
For example, instead of:
var processedProgram = PreProcessProgramVerification(program);
if (!Options.Verify)
{
return PipelineOutcome.Done;
}
if (Options.ContractInfer)
{
return await RunHoudini(program, stats, er);
}
if (Options.LeanFile is not null) {
var writer = new StreamWriter(Options.LeanFile);
LeanGenerator.EmitPassiveProgramAsLean(Options, processedProgram.Program, writer);
writer.Close();
return PipelineOutcome.Cancelled;
}write
var processedProgram = PreProcessProgramVerification(program);
if (!Options.Verify)
{
return PipelineOutcome.Done;
}
if (Options.UsePassiveProgram != null && Options.UsePassiveProgram(processedProgram))
{
return;
}Note that the Houdini code has also moved to a different place.
There was a problem hiding this comment.
Yeah, I think you're right. I'll restructure it a bit.
Source/Provers/LeanAuto/LeanAuto.cs
Outdated
| generator.NL(); | ||
|
|
||
| generator.Line("-- Type synonyms"); | ||
| liveDeclarations.OfType<TypeSynonymDecl>().ForEach(tcd => generator.Visit(tcd)); |
There was a problem hiding this comment.
Not blocking: is it good to mix up the order of liveDeclarations? I think a more 1-to-1 translation, ideally even keeping comments, could be nicer.
There was a problem hiding this comment.
At the moment, doing it this way makes for easier debugging the translation, in my experience so far. Once the approach is more stable, I think preserving more of the original structure would be good (though there may be some cases where Lean could require a slightly different order).
Source/Provers/LeanAuto/LeanAuto.cs
Outdated
| writer.WriteLine(); | ||
| } | ||
|
|
||
| private void Text(string text) |
There was a problem hiding this comment.
Please rename to Write
Source/Provers/LeanAuto/LeanAuto.cs
Outdated
| writer.Write(text); | ||
| } | ||
|
|
||
| private void Line(string text) |
There was a problem hiding this comment.
Please rename to WriteLine
Source/Provers/LeanAuto/LeanAuto.cs
Outdated
| NL(); | ||
| } | ||
|
|
||
| private void NL() |
There was a problem hiding this comment.
Please rename to WriteLine
Source/Provers/LeanAuto/LeanAuto.cs
Outdated
| } | ||
| } | ||
|
|
||
| private void IndentL(int n = 1, string str = null) |
There was a problem hiding this comment.
Please rename to IndentLine
| LeanGenerator.EmitPassiveProgramAsLean(Options, processedProgram.Program, writer); | ||
| writer.Close(); | ||
| } | ||
| // We unfortunately have to do any processing of the passive program after verification, |
There was a problem hiding this comment.
I don't understand this comment. These lines seems contradictory, both saying that processedProgram.Program is an already passified program, and that it's not yet passified because that only happens during verification.
By the way, what step do you mean by "verification" in the context of Boogie? The whole pipeline could be considered verification.
There was a problem hiding this comment.
What I mean is that ProcessPassiveProgram needs to be called after VerifyEachImplementation instead of before, because VerifyEachImplementation turns processedProgram into a passive program, destructively. I would love it if everything happened in PreProcessProgramVerification, but it doesn't right now, and I think it'd take a pretty big refactoring to get it there.
There was a problem hiding this comment.
Ah, if you change verification to calling VerifyEachImplementation in the comment, then it would be more clear to me.
There was a problem hiding this comment.
Btw, extracting out the passive-ication is already done in the method vcGenerator.PrepareImplementation, although it only does it for a single implementation. GetVerificationTasks gives an example of how to call it. Maybe you want to use that, so you don't have to actually generate SMT each time?
There was a problem hiding this comment.
It would generally make sense to generate Lean code as an alternative to SMT-Lib, so it could make sense for it to be called from the VCGeneration package. I took a stab at refactoring things to do that, but as things currently stand there are two issues:
- The Lean generator depends on the
VCGenerationpackage, and we can't create a cyclic dependency. - The Lean generator currently translates the whole program in one go, which doesn't really fit with the current structure of the VC generator.
I think it's possible to refactor things further to not require that cyclic dependency, and I'm considering whether the Lean generator should work on a per-implementation basis, but I think I'd prefer to leave both for a future PR (probably one in the pretty near future, though).
There was a problem hiding this comment.
To me it's already a problem that ExecutionEngine is calling out to LeanGenerator, because it bloats the scope of ExecutionEngine.
I would go for the combination of my previous two suggestions, to remove the dependency of ExecutionEngine on LeanGenerator, and make use of vcGenerator.PrepareImplementation
Change
var processedProgram = PreProcessProgramVerification(program);
if (!Options.Verify)
{
return PipelineOutcome.Done;
}
if (Options.ContractInfer)
{
return await RunHoudini(program, stats, er);
}
...
var outcome = await VerifyEachImplementation(output, processedProgram, stats, programId, er, requestId, stablePrioritizedImpls);
if (Options.LeanFile is not null) {
var writer = new StreamWriter(Options.LeanFile);
LeanAutoGenerator.EmitPassiveProgramAsLean(Options, passiveProgram, writer);
writer.Close();
}Into
var processedProgram = PreProcessProgramVerification(program);
if (!Options.Verify)
{
return PipelineOutcome.Done;
}
if (Options.UseResolvedProgram != null && Options.UseResolvedProgram(processedProgram))
{
return;
}
...
var outcome = await VerifyEachImplementation(output, processedProgram, stats, programId, er, requestId, stablePrioritizedImpls);Note that both Houdini and Lean are no longer mentioned.
Then instead of setting LeanFile, set Options.UseResolvedProgram with:
void LetLeanUseResolvedProgram(Program program) {
foreach(var implementation in program.Implementations) {
vcGenerator.PrepareImplementation(new ImplementationRun(implementation, options.OutputWriter), ..)
}
var writer = new StreamWriter(Options.LeanFile);
EmitPassiveProgramAsLean(Options, program, writer);
writer.Close();
}There was a problem hiding this comment.
I like this approach, and I've pushed some changes that go in roughly that direction.
| @@ -553,6 +553,10 @@ public void Inline(Program program) | |||
|
|
|||
| var processedProgram = PreProcessProgramVerification(program); | |||
|
|
|||
| if (Options.UseResolvedProgram.Any()) { | |||
There was a problem hiding this comment.
Could drop the if and always do the foreach.
| @@ -553,6 +553,10 @@ public void Inline(Program program) | |||
|
|
|||
| var processedProgram = PreProcessProgramVerification(program); | |||
|
|
|||
| if (Options.UseResolvedProgram.Any()) { | |||
| Options.UseResolvedProgram.ForEach(action => action(Options, processedProgram)); | |||
There was a problem hiding this comment.
I would use a C# foreach construct here, but it's a bit of style thing. One advantage is that it's nicer to step through the iterations with a debugger. Another is that IDEs will be able to analyze it better.
This experimental new backend translates passive Boogie programs into Lean programs including theorems that can be automatically discharged by the
lean-autopackage.Note: The code is almost entirely separate from the existing Boogie codebase, and modifies that code in only tiny ways (to provide an additional command and invoke the new backend when it's enabled). Because of this, and because of its current experimental nature, I'm happy to do as little or as much code review on the new directory as other folks want.
It has several goals:
lean-auto).mathlib4.At the moment, completing proofs with the backend is manual. When given the
/printLean:file.leanoption, it prints the Lean program to a file after completing normal verification. It will probably need to stay this way until we build some additional Lean infrastructure. Ultimately, however, the plan is to make it as integrated and automatic as the current SMT-based verification pipeline.It includes a new test workflow with test files in
Test/lean-auto. This currently checks that it succeeds on several of the tests inTest/textbookbut will gradually expand to cover more of the test suite.