Library support

[keyboardDrummer]

No description provided.

[parno]

Thanks for writing this up! If I understand it correctly, it seems like if a file A.dfy currently has 5 different include directives today, then under your proposal, we would instead need to specify those 5 different files on the command line (using /library) when verifying/compiling A.dfy? If so, I'm not sure that's a usability win, in that I'll now either have quite complex command-lines, or I'll have to store all of this dependency information for each file in a build script, and there may be a fair bit of redundancy across those dependency specifications (i.e., many files may depend on the standard library, but I'll have to write the path for the standard library out for each of those files).

It seems like some version of @jayb's Rust-based proposal (dafny-lang/dafny#1236 (comment)) would help here. For example, if we have:

// Producer.dfy
module Export {
  const A := 1
}

// Consumer.dfy
module Bar {
  import Export
  import Std
  const myA :=Std.max(Export.A + 1, 5)
}

we would also have something like:

// Dafny.toc
Export = { path = "./Producer.dfy"}
Std = { path = "/usr/lib/Standard.dfy" }

(alternatively, we could just paths, and rely on Dafny to extract the names of the modules they contain).
When we run Dafny on Consumer.dfy, it sees the references to Export and Std, looks them up in Dafny.toc and imports Producer.dfy and /usr/lib/Standard.dfy as trusted (meaning they won't be reverified), and marks them as dependencies of Consumer.dfy.

This would still require you to specify the files included in your project, but at least you only specify them once, in a single place, rather than many times in include directives scattered throughout your files, or in multiple lines in your build script of choice.

[keyboardDrummer]

Thanks for writing this up! If I understand it correctly, it seems like if a file A.dfy currently has 5 different include directives today, then under your proposal, we would instead need to specify those 5 different files on the command line (using /library) when verifying/compiling A.dfy

I'd like to remove the need for include directives all-together.

I think we should distinguish two kinds of included files:

1. Ones that are part of your Dafny project, that you want to verify at some point, and possibly again after you've made changes.
2. Ones that come from a library, that have already been verified, and won't be modified by you so they don't need re-verification.

This proposal only removes the need for including files of the second kind.

For removing the need for includes of the first kind I have another proposal, maybe I should have shared that first. The summary of the changes there is:

• Allow Dafny to take a glob path as an input source, for example src/**/*.dfy
• Add parallelisation to Dafny so it will optimally utilise the machine's cores. This removes the need to do multiple parallel calls to the CLI, where each call passes in different source files, to get the most out of your cores.
• Enable persistent caching of verification results between calls to dafny so changing one file doesn't mean all files in your project need to verified again.

The end goal of those changes and the ones in this proposal is that you can work on a project by only doing calls of the form

dafny containsAllMySources/**/*.dfy /library:libs/Library1.dfy /library:libs/Library2.dfy /persistentCache.

It'll create a dafny.cache file which remembers what has already been verified in a previous call, so if you change a single lemma only that will be verified again. If you delete the cache and call Dafny again then it'll verify all the Dafny files under containsAllMySources but not Library1.dfy and Library2.dfy.

It seems like some version of @jayb's Rust-based proposal (dafny-lang/dafny#1236 (comment)) would help here.

I think we can distinguish the feature of allowing customers to specify Dafny command line arguments through a configuration file and features that improve Dafny's parallelisation, caching and support for libraries.

I'm not against supporting a TOML based configuration file, but I'd like to see whether there is still a need for one once we implement the changes I described above and in the proposal.

[robin-aws]

I've been tacking this problem recently, and just recalled that this RFC already existed and overlapped a lot with my plans, so let me append them here to close the loop.

Since @keyboardDrummer wrote this, he has given us --library in Dafny with exactly the proposed semantics, and (in the pending 4.1 release of Dafny) support for a dfyconfig.toml project file that specifies what files to include and what CLI options to provide.

However, there is one thing I'm doing differently than proposed in this RFC: rather than reusing *.dfy source files as library files, I'm defining a distinct file format for a "built" Dafny library: *.doo, for Dafny Output Object (really just a backronym: I can't resist making a Scooby Doo reference because of the Daphne homonym :).

The main reason I want a distinct build artifact is to make it much harder to accidentally skip verification in the build process: I've noticed users are often surprised that included files are not verified by default, for example. Verifying once and then compiling to multiple target languages is a common workflow (especially in our own test suite), and it is much safer to only skip verification when given a *.doo file that can only be created after verification, rather than arbitrary source files. I also want to attach metadata about how a file was verified, to prevent mixing options like --unicode-char unsafely.

There are more details about the *.doo file format in this comment, and I'm planning to cut the PR to implement it in a few days. One thing I wasn't yet sure about is when to emit the .doo file: I was thinking of it as an artifact of verification that would always be output, but I also kind of like the idea of -t:library, as long as we don't think emitting it as a side-effect of building to an actual target language will be a common need.

cc @parno since you had some great input on this RFC earlier!

[parno]

I like the idea of a Dafny issued file that certifies verification took place. A number of our build scripts already create (empty) *.v files to help orchestrate build dependencies, so having something more official would already be a useful step. Recording meta-data about how the verification was done, so we can check for incompatible options makes it even more useful.

@robin-aws I do have one concern about item 4 in the comment you link to above. I may be misreading it, but it sounds like you're suggesting deprecation of a developer's ability to verify a single Dafny file without verifying all of its includes. We have found that feature critical for individual developer productivity as well as for doing massive scale out for CI purposes on large projects, so I'd be sad to see it go. Apologies if I've misunderstood your suggestion!

[robin-aws]

I like the idea of a Dafny issued file that certifies verification took place. A number of our build scripts already create (empty) *.v files to help orchestrate build dependencies, so having something more official would already be a useful step. Recording meta-data about how the verification was done, so we can check for incompatible options makes it even more useful.

Great to hear! I will just carefully clarify that a *.doo file won't really strongly "certify" verification took place, at least not in the same sense as a digital certificate certifies an identity, it will only record the metadata. I'll be relying on the package manager (whether Dafny-native or something like Gradle) to manage signing when required to certify provenance. I also think it will be very useful to have some kind of proof certificate that can be fed to a solver to much more quickly re-verify the program, but that definitely won't be in v1 of this feature.

@robin-aws I do have one concern about item 4 in the comment you link to above. I may be misreading it, but it sounds like you're suggesting deprecation of a developer's ability to verify a single Dafny file without verifying all of its includes. We have found that feature critical for individual developer productivity as well as for doing massive scale out for CI purposes on large projects, so I'd be sad to see it go. Apologies if I've misunderstood your suggestion!

I'm definitely not suggesting making that impossible, just safer by default (and even then only after a deprecation period with lots of warning). If A.dfy depends on B.dfy, the idea would be that by default verifying A.dfy transitively verifies B.dfy as well, but if a B.doo exists then the verification could be safe to skip. I think this will get easier to work with as we move away from include statements and towards other mechanisms for providing dependencies, and only re-verifying a single file and not its dependencies is a feature Dafny tooling should provide directly.