Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add an experimental backend that uses Lean to discharge goals #850

Merged
merged 33 commits into from
Mar 19, 2024
Merged

Add an experimental backend that uses Lean to discharge goals #850

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
33 commits
Select commit Hold shift + click to select a range
bf36ddf
Translator sufficient for Bubble.bpl to typecheck
atomb Dec 13, 2023
8309d33
Now Bubble.bpl verifies after translation
atomb Dec 14, 2023
4b2eb9e
Control Lean printing with an option
atomb Dec 19, 2023
89b3595
Translator sufficient to verify all but one textbook example
atomb Dec 19, 2023
f6f8ff6
Reorganize unsupported overrides
atomb Dec 19, 2023
637c415
Various improvements
atomb Dec 20, 2023
e4c34dc
Successfully process trivial Dafny program
atomb Dec 22, 2023
2556b26
Cleanups
atomb Dec 22, 2023
7049b6d
Update exception messages
atomb Feb 13, 2024
b2c5b14
Move prelude to external file
atomb Feb 13, 2024
d2193dd
Add configuration files to check Prelude.lean
atomb Feb 13, 2024
7c096c0
Cleanup comments, strings, exceptions
atomb Feb 13, 2024
7fea48d
Clean up error handling
atomb Feb 14, 2024
05b616c
Reorder cases and improve error messages
atomb Feb 14, 2024
005d80d
Add test suite for LeanAuto backend
atomb Feb 14, 2024
df6bb76
Add README for LeanAuto
atomb Feb 14, 2024
6628fea
Add workflow to test the LeanAuto backend
atomb Feb 14, 2024
300ed90
Fill in proofs and definitions in Lean prelude
atomb Feb 14, 2024
359da35
Clean up lakefile
atomb Feb 14, 2024
4fc941d
Fix Lean installation
atomb Feb 14, 2024
bf46f95
Change setup-lean action name
atomb Feb 14, 2024
154fee4
Ensure Lean dependencies are actually built
atomb Feb 14, 2024
9d58eb5
Pin the version of lean-auto for reproducibility
atomb Feb 14, 2024
2896020
Merge remote-tracking branch 'upstream/master' into basic-lean-auto
atomb Mar 6, 2024
a2a40d6
Rename LeanGenerator -> LeanAutoGenerator
atomb Mar 6, 2024
49e1eec
Rename some methods
atomb Mar 6, 2024
2f8b3a9
Move use of passive program to a separate method
atomb Mar 6, 2024
fd7b4c9
Clarify comment
atomb Mar 7, 2024
dd8359f
Merge remote-tracking branch 'upstream/master' into basic-lean-auto
atomb Mar 7, 2024
dc6b667
Merge branch 'master' into basic-lean-auto
atomb Mar 13, 2024
4cc7547
Generalized processing of passive programs
atomb Mar 19, 2024
29979dc
Allow `goto` to have no targets
atomb Mar 19, 2024
fbafb12
Use `foreach` instead of `ForEach`
atomb Mar 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 18 additions & 9 deletions Source/ExecutionEngine/ExecutionEngine.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -571,16 +571,11 @@ 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 (Options.LeanFile is not null) {
var writer = new StreamWriter(Options.LeanFile);
LeanGenerator.EmitPassiveProgramAsLean(Options, processedProgram.Program, writer);
writer.Close();
}
// We unfortunately have to do any processing of the passive program after verification,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, if you change verification to calling VerifyEachImplementation in the comment, then it would be more clear to me.

Copy link
Collaborator

@keyboardDrummer keyboardDrummer Mar 7, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 VCGeneration package, 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).

Copy link
Collaborator

@keyboardDrummer keyboardDrummer Mar 19, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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();
}

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like this approach, and I've pushed some changes that go in roughly that direction.

// 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)
{
Expand All @@ -593,6 +588,20 @@ public async Task<PipelineOutcome> 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
Expand Down
Loading
Loading