feat: Build artifacts ("library" backend and .doo files)

[robin-aws]

Provides a build artifact for outputting after successful verification, with enough metadata attached to support safe consumption as a library, as loosely described in this comment: #3556 (comment)

Also refactors the functionality used by dafny audit to ensure the library backend rejects assume statements as the other backends do, without having to implement a proper SinglePassCompiler subclass.

Also hides the internal "Simple Dafny" backend, which isn't intended to be publicly documented, while the new library backend is.

Provides a solution for #3556, but I'm not calling that resolved until we at least deprecate separate verification features that don't use .doo files (which isn't in scope for this PR).

TODO:

• Clean up doo file generation (generic Backend/Compiler interface is creating an extra unused file entry)
• Eliminate useless LibraryCompiler if possible without rathole-ing on the general interface design
• Attempt asserting that DooFile.ProgramSerializationOptions doesn't change over time. (too tricky given options are only initialized for the current command)
• Bit more testing
• Address change in behavior in auditor
• Reference manual updates
• Release note

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[robin-aws]

Note the failing TestAuditor.dfy test: it's due to my filling in more cases of Node.Assumptions(). I think my changes improve the accuracy of that method so I'd prefer to keep them, but the AuditReport logic has to be adjusted a little to account for that to maintain current behavior. It would be simpler if we ditched the behavior of only reporting on explicit assumptions if there are any in a given "scope", since getting the scope right is now a bit trickier.

[atomb]

Does this mean that we wouldn't support proof-only libraries?

[robin-aws]

Oh sure we will - the IsToBeCompiled field really just means "was not provided by --library". So you can work just with .doo files and never compile any of them with the other backends. Perhaps the name could be "IsToBeBuilt" instead, but I don't think that's enough of an improvement to bother with personally. :)

[atomb]

Ah, right. Sounds good!

[atomb]

I think this looks good. CI will ensure that we can't merge without fixing that last test. :)

[keyboardDrummer]

Hey, you don't have to inherit from SinglePassCompiler, that's convenient 😄

[keyboardDrummer]

I think Dafny projects should specify whether they're an executable or a library, and depending on this, the default for dafny build should produce an executable or a *.doo file.

Also, I think the "lib" target should not exist for dafny run and dafny translate. Currently, it's not mentioned in the --help documentation for those (and for build).

I think the ideal end-game is that Dafny's standard library is large enough that dafny run and dafny build can generally be used without supplying additional non-Dafny files that implement externs, and that dafny translate is used for integration scenarios. If that's the case, the --target option for dafny run and build would generally not be used, and *.doo files would be generated when doing dafny build on a Dafny project that's marked as a library.

For now, could you show an error when using the lib target with run, and have lib be the default for projects without a main method?

Currently I get:

rwillems@bcd0745419f2 dafny2 % ./Scripts/dafny run -t:lib /Users/rwillems/SourceCode/dafny2/Test/c++/hello.dfy                

Dafny program verifier finished with 0 verified, 0 errors
Unhandled exception. System.NullReferenceException: Object reference not set to an instance of an object.
   at DafnyCore.DooFile.Validate(String filePath, DafnyOptions options, Command currentCommand) in /Users/rwillems/SourceCode/dafny2/Source/DafnyCore/DooFile.cs:line 122
   at Microsoft.Dafny.DafnyFile..ctor(DafnyOptions options, String filePath, Boolean useStdin) in /Users/rwillems/SourceCode/dafny2/Source/DafnyCore/DafnyMain.cs:line 99
   at Microsoft.Dafny.DafnyDriver.ProcessCommandLineArguments(String[] args, DafnyOptions& options, List`1& dafnyFiles, List`1& otherFiles) in /Users/rwillems/SourceCode/dafny2/Source/DafnyDriver/DafnyDriver.cs:line 263
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /Users/rwillems/SourceCode/dafny2/Source/DafnyDriver/DafnyDriver.cs:line 112
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0() in /Users/rwillems/SourceCode/dafny2/Source/DafnyDriver/DafnyDriver.cs:line 102
   at System.Threading.Thread.StartCallback()
 Process exited with exit code 134

and

rwillems@bcd0745419f2 dafny2 % ./Scripts/dafny translate lib /Users/rwillems/SourceCode/dafny2/Test/c++/hello.dfy 

Dafny program verifier finished with 0 verified, 0 errors

[robin-aws]

I think Dafny projects should specify whether they're an executable or a library, and depending on this, the default for dafny build should produce an executable or a *.doo file.

Also, I think the "lib" target should not exist for dafny run and dafny translate. Currently, it's not mentioned in the --help documentation for those (and for build).

I think the ideal end-game is that Dafny's standard library is large enough that dafny run and dafny build can generally be used without supplying additional non-Dafny files that implement externs, and that dafny translate is used for integration scenarios. If that's the case, the --target option for dafny run and build would generally not be used, and *.doo files would be generated when doing dafny build on a Dafny project that's marked as a library.

For now, could you show an error when using the lib target with run, and have lib be the default for projects without a main method?

You make some good points, but I think the real issue is us using "lib" as an identifier for the ".doo target", because it implies the result is a library and not an executable, when that aspect should be orthogonal to which backend you're targeting. We could just call it "the doo backend": I didn't love that, but also couldn't think of a better label.

I'd much rather have the .doo backend support all operations, so that it's easier to get better coverage through generic utilities like %testDafnyForEachCompiler. Hopefully changing the label would make that seem more reasonable.

Currently I get:

rwillems@bcd0745419f2 dafny2 % ./Scripts/dafny run -t:lib /Users/rwillems/SourceCode/dafny2/Test/c++/hello.dfy                

Dafny program verifier finished with 0 verified, 0 errors
Unhandled exception. System.NullReferenceException: Object reference not set to an instance of an object.
   at DafnyCore.DooFile.Validate(String filePath, DafnyOptions options, Command currentCommand) in /Users/rwillems/SourceCode/dafny2/Source/DafnyCore/DooFile.cs:line 122
   at Microsoft.Dafny.DafnyFile..ctor(DafnyOptions options, String filePath, Boolean useStdin) in /Users/rwillems/SourceCode/dafny2/Source/DafnyCore/DafnyMain.cs:line 99
   at Microsoft.Dafny.DafnyDriver.ProcessCommandLineArguments(String[] args, DafnyOptions& options, List`1& dafnyFiles, List`1& otherFiles) in /Users/rwillems/SourceCode/dafny2/Source/DafnyDriver/DafnyDriver.cs:line 263
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /Users/rwillems/SourceCode/dafny2/Source/DafnyDriver/DafnyDriver.cs:line 112
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0() in /Users/rwillems/SourceCode/dafny2/Source/DafnyDriver/DafnyDriver.cs:line 102
   at System.Threading.Thread.StartCallback()
 Process exited with exit code 134

and

rwillems@bcd0745419f2 dafny2 % ./Scripts/dafny translate lib /Users/rwillems/SourceCode/dafny2/Test/c++/hello.dfy 

Dafny program verifier finished with 0 verified, 0 errors

The first case is a legit bug which I've got a fix for, thanks for finding that: #3967

The second case is working as advertised AFAICT: it should have created a hello-lib directory with the entries for a doo file (which I don't love as discussed above, but I didn't think it was actively harmful, and I found it handy for debugging).

[keyboardDrummer]

I think your view sees the .doo file as a generic Dafny build artifact that is useful for both Dafny executables and libraries. In that case, I would recommend changing the TargetId from lib to dfy.

However, I don't see a use-case for a .doo file other than producing a library.

If you have an executable Dafny application, would you ever want to produce an intermediate .doo unless you're doing differential testing on Dafny's back-ends ? If you have an executable Dafny application, you won't be using translate, so there is no reason to first produce a .doo and then translate it multiple times.

If you want to get a fast executable that can be run multiple times, which is the use-case of dafny build, .doo is not ideal, and you'd better generate a .dll or a .jar.

Again, I think our endgame is that there is no reason for dafny run and dafny build to use the --target option, and that for executable Dafny applications the default for dafny build should be to generate a fast executable for either the current arch/platform, or a platform independent one, like a .NET dll. The default of dafny build for Dafny libraries should be to generate a .doo file.

[keyboardDrummer]

Based on offline discussions with @robin-aws , created this issue: #3976