Detect and report use of mixing options that change semantics

[davidcok]

Summary

Mixing code that has been verified or compiled with values of certain options that modify the semantics of Dafny, such as --unicode-char, could lead to soundness problems.

Background and Motivation

Dafny 4 has a default of unicode-char:true, previous versions had unicode-char:false

Proposed Feature

Detect whether modules are setting different values -- ideally only where it actually matters.

Alternatives

No response

[atomb]

I updated the text to generalize it a bit to any option that changes language semantics.

[robin-aws]

To me the root cause here is not having any mechanisms to enforce sound separate verification and compilation of Dafny code. I say the best solution is to define some kind of build artifact for Dafny that attaches metadata to the Dafny source, so that when consuming a library, rather than trusting the code was previously verified and assuming the details of how it was verified, the Dafny tooling can look for hard evidence and metadata about how the library was built, and fail if the consuming environment is not compatible.

To that end, I propose the following:

1. Define a file type similar to *.dll or *.jar to contain the results of successful verification.

   • Likely an alias for a compressed archive in the style of *.jar or *.nupkg etc.
   • Would contain:
     • The source for the Dafny program, embedded in a similar style to how the C# backend adds the DafnySourceAttribute.
     • The version of Dafny used to verify the program, and the identity/version of the solver
     • The options passed when verifying (possibly convenient to use a dfyconfig.toml file)
     • (maybe, if useful?) Metrics such as verification time or resource count
     • (future versions) Some kind of verification certificate a solver can use to quickly re-verify
     • A version number for the format of this metadata (so we can improve it over time, for example to store the verified program more efficiently than in source text)
   • I cheekily propose using the *.doo extension, for Dafny Output Object (or Dafny Object, Obviously?)
     • Can't help thinking about the other Daphne :)

2. Change the dafny tooling in general to produce a *.doo file unless verification is skipped

   • Even better, discourage the use of --no-verify entirely. The flag is often used (especially in our own test suite) to avoid re-verifying repeatedly when (for example) compiling the same source to multiple backends. We can instead encourage calling dafny translate on the *.doo result of a previous dafny verify call.

3. Support passing *.doo files directly to dafny as well as *.dfy files.

   • Fail if the options used to produce the *.doo file are incompatible with the current options/Dafny version. We can start conservative and reject ANY mismatch, but then allow-list mismatches that are known to be safe.

4. Deprecate features that unsafely skip verification, such as:

   • include without --verify-included-files (users are often surprised that included files are not verified by default)
   • --library <*.dfy> as opposed to --library <*.doo>
     • Or perhaps even deprecate --library in favor of directly passing *.doo files.

*.doo files would become the standard artifact for distributing Dafny projects, independently of how these artifacts are identified and distributed. It implies that #3007 should not be satisfied by just git cloning the source of a Dafny library, unless such a repository regularly checked-in *.doo files, which is not the best practice. Such a library could attach a *.doo file to GitHub releases, however, which would be easily downloadable via URLs like https://github.com/dafny-lang/libraries/releases/download/v0.1.0/wrappers.doo.

*.doo files could also be embedded inside the compiled and assembled artifacts for any target language Dafny supports, e.g. as a META-INF entry in a Java .jar file. Kotlin does something similar in embedding a *.kotlin_module in jars compiled from Kotlin source, so that other Kotlin projects can link with them using Kotlin signatures: https://blog.jetbrains.com/kotlin/2015/06/improving-java-interop-top-level-functions-and-properties/#Asmallbitonmetadata

[robin-aws]

Note that although a URL pointing to a *.doo file is technically enough for a remote dependency, I still wouldn't recommend that as a production-grade solution, since GitHub releases don't have any standards for including checksums or signatures. This makes building on top of existing systems like Maven/Gradle via plugins like #3169 appealing: https://docs.gradle.org/current/userguide/dependency_verification.html

[keyboardDrummer]

The introduction of .doo files has I think mostly resolved this issue.

What I think is left, is to let --library=<nonDooFile> emit a warning, saying that the referenced file might have been verified with other options, or might not even have been verified at all.