feat: Standard library support + DafnyStdLibs.Wrappers (#4678)

### Description
This change adds support for "standard libraries" that are packaged
together with the Dafny distribution, at least for now. They are
automatically available for import with the option
`--standard-libraries`, which will likely become true by default in
Dafny 5. To avoid Dafny's footprint from getting larger and larger over
time, some portion of them may be moved into separately distributed
packages at a later date. They will remain optional and the Dafny
language itself should not depend on them.

A later change will likely add pre-translated source to the runtimes as
well, and a translation option such as `--include-standard-libraries`
similar to `--include-runtime` to rely on this copy of them instead of
translating them into every component.

Implementation notes:

* The primary implementation approach, which is mostly not user-visible,
is to pre-build one or more `.doo` files and embed them in
`DafnyPipeline.dll`, just as we already do with the various runtime
files such as `DafnyRuntime.dll`. They are added as input `DafnyFiles`,
using URIs of the form `dllresource://DafnyPipeline/<name>.doo`, so they
are not re-verified but are in scope for compilation.
* I've fixed/improved a few things around `.doo` files, such as
loosening the library checks for some options, and no longer checking
options that only affect compilation (it may make sense to leverage
these files for compilation compatibility checking in the future but
that's not currently in scope).
* The current limitations of the standard library support are documented
in `Source/DafnyStandardLibraries/CONTRIBUTING.md`, and should make it
clear which pending libraries are still partially blocked.

### How has this been tested?
* The general standard library support is tested with the integration
tests under `stdlibs` and `metatests/StdLibsOffByDefaultInTests.dfy`
* The Wrappers library is tested via `WrappersExamples.dfy`

---------

Co-authored-by: Remy Willems <[email protected]>

.github/workflows/standard-libraries.yml

@@ -0,0 +1,37 @@
+name: Build and Test Dafny Standard Libraries
+
+on:
+  workflow_dispatch:
+  pull_request:
+    branches: [ master, main-* ]
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  check-deep-tests:
+     uses: ./.github/workflows/check-deep-tests-reusable.yml
+
+  build:
+    needs: check-deep-tests
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout Dafny
+        uses: actions/checkout@v3
+        with:
+          submodules: true
+      - name: Set up JDK 18
+        uses: actions/setup-java@v3
+        with:
+          java-version: 18
+          distribution: corretto
+      - name: Build Dafny
+        run: dotnet build Source/Dafny.sln
+      - name: Get Z3
+        run: make z3-ubuntu
+      - run: npm install bignumber.js
+      - name: Test DafnyStandardLibraries
+        run: make -C Source/DafnyStandardLibraries all
+

.gitignore

@@ -58,6 +58,9 @@ Source/.vs
 # Generated by VS Code
 .vscode/*
 
+# Generated by Dafny tooling
+/Source/DafnyStandardLibraries/build
+
 # Generated by Java tools (gradle/javac/etc)
 
 /Source/DafnyRuntime/DafnyRuntimeJava/.gradle
@@ -70,3 +73,5 @@ package-lock.json
 docs/dev/*.fix
 docs/dev/*.feat
 docs/dev/*.break
+
+

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -1236,6 +1236,7 @@ public void PrintStatement(Statement stmt, int indent) {
         } else if (expectStmt != null && expectStmt.Message != null) {
           wr.Write(", ");
           PrintExpression(expectStmt.Message, true);
+          wr.Write(";");
         } else {
           wr.Write(";");
         }

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -35,11 +35,12 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
     CancellationToken cancellationToken) {
     var options = errorReporter.Options;
     var builtIns = new SystemModuleManager(options);
-    var defaultModule = new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList());
+    var defaultModule = new DefaultModuleDefinition();
 
+    var rootSourceUris = files.Select(f => f.Uri).ToList();
     var verifiedRoots = files.Where(df => df.IsPreverified).Select(df => df.Uri).ToHashSet();
     var compiledRoots = files.Where(df => df.IsPrecompiled).Select(df => df.Uri).ToHashSet();
-    var compilation = new CompilationData(errorReporter, defaultModule.Includes, defaultModule.RootSourceUris, verifiedRoots,
+    var compilation = new CompilationData(errorReporter, defaultModule.Includes, rootSourceUris, verifiedRoots,
       compiledRoots);
     var program = new Program(
       programName,

Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs

@@ -6,16 +6,13 @@ namespace Microsoft.Dafny;
 
 public class DefaultModuleDefinition : ModuleDefinition, ICloneable<DefaultModuleDefinition> {
   public List<Include> Includes { get; } = new();
-  public IList<Uri> RootSourceUris { get; }
 
   public DefaultModuleDefinition(Cloner cloner, DefaultModuleDefinition original) : base(cloner, original, original.NameNode) {
-    RootSourceUris = original.RootSourceUris;
   }
 
-  public DefaultModuleDefinition(IList<Uri> rootSourceUris)
+  public DefaultModuleDefinition()
     : base(RangeToken.NoToken, new Name("_module"), new List<IToken>(), false, false,
       null, null, null) {
-    RootSourceUris = rootSourceUris;
   }
 
   public override bool IsDefaultModule => true;

Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs

@@ -18,7 +18,7 @@ static PrintStmt() {
 
     DooFile.RegisterLibraryChecks(
       checks: new Dictionary<Option, DooFile.OptionCheck> {
-        { TrackPrintEffectsOption, DooFile.CheckOptionMatches }
+        { TrackPrintEffectsOption, DooFile.CheckOptionLocalImpliesLibrary }
       });
   }
 

Source/DafnyCore/Compilers/Library/LibraryBackend.cs

@@ -31,6 +31,9 @@ public override string TargetBaseDir(string dafnyProgramName) =>
     Feature.LegacyCLI
   };
 
+  // Necessary since Compiler is null
+  public override string ModuleSeparator => ".";
+
   protected override SinglePassCompiler CreateCompiler() {
     return null;
   }

Source/DafnyCore/DafnyFile.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.IO;
+using System.Reflection;
 using System.Reflection.Metadata;
 using System.Reflection.PortableExecutable;
 using DafnyCore;
@@ -10,6 +11,7 @@ namespace Microsoft.Dafny;
 
 public class DafnyFile {
   public string FilePath { get; private set; }
+  public string Extension { get; private set; }
   public string CanonicalPath { get; private set; }
   public string BaseName { get; private set; }
   public bool IsPreverified { get; set; }
@@ -23,29 +25,33 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
     Origin = origin;
     var filePath = uri.LocalPath;
 
-    var extension = ".dfy";
+    Extension = ".dfy";
     if (uri.IsFile) {
-      extension = Path.GetExtension(uri.LocalPath).ToLower();
+      Extension = Path.GetExtension(uri.LocalPath).ToLower();
       BaseName = Path.GetFileName(uri.LocalPath);
-    }
-    if (uri.Scheme == "stdin") {
+      // Normalizing symbolic links appears to be not
+      // supported in .Net APIs, because it is very difficult in general
+      // So we will just use the absolute path, lowercased for all file systems.
+      // cf. IncludeComparer.CompareTo
+      CanonicalPath = Canonicalize(filePath).LocalPath;
+    } else if (uri.Scheme == "stdin") {
       getContentOverride = () => options.Input;
       BaseName = "<stdin>";
+      CanonicalPath = "<stdin>";
+    } else if (uri.Scheme == "dllresource") {
+      Extension = Path.GetExtension(uri.LocalPath).ToLower();
+      BaseName = uri.LocalPath;
+      CanonicalPath = uri.ToString();
     }
 
-    // Normalizing symbolic links appears to be not
-    // supported in .Net APIs, because it is very difficult in general
-    // So we will just use the absolute path, lowercased for all file systems.
-    // cf. IncludeComparer.CompareTo
-    CanonicalPath = getContentOverride == null ? Canonicalize(filePath).LocalPath : "<stdin>";
     FilePath = CanonicalPath;
 
     var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath;
     if (getContentOverride != null) {
       IsPreverified = false;
       IsPrecompiled = false;
       GetContent = getContentOverride;
-    } else if (extension == ".dfy" || extension == ".dfyi") {
+    } else if (Extension == ".dfy" || Extension == ".dfyi") {
       IsPreverified = false;
       IsPrecompiled = false;
       if (!File.Exists(filePath)) {
@@ -61,15 +67,30 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
       } else {
         GetContent = () => new StreamReader(filePath);
       }
-    } else if (extension == ".doo") {
+    } else if (Extension == ".doo") {
       IsPreverified = true;
       IsPrecompiled = false;
 
-      if (!File.Exists(filePath)) {
-        options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found");
-        throw new IllegalDafnyFile(true);
+      DooFile dooFile;
+      if (uri.Scheme == "dllresource") {
+        var assembly = Assembly.Load(uri.Host);
+        // Skip the leading "/"
+        var resourceName = uri.LocalPath[1..];
+        using var stream = assembly.GetManifestResourceStream(resourceName);
+        if (stream is null) {
+          throw new Exception($"Cannot find embedded resource: {resourceName}");
+        }
+
+        dooFile = DooFile.Read(stream);
+      } else {
+        if (!File.Exists(filePath)) {
+          options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found");
+          throw new IllegalDafnyFile(true);
+        }
+
+        dooFile = DooFile.Read(filePath);
       }
-      var dooFile = DooFile.Read(filePath);
+
       if (!dooFile.Validate(filePathForErrors, options, options.CurrentCommand)) {
         throw new IllegalDafnyFile(true);
       }
@@ -81,7 +102,7 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
       // the DooFile class should encapsulate the serialization logic better
       // and expose a Program instead of the program text.
       GetContent = () => new StringReader(dooFile.ProgramText);
-    } else if (extension == ".dll") {
+    } else if (Extension == ".dll") {
       IsPreverified = true;
       // Technically only for C#, this is for backwards compatability
       IsPrecompiled = true;

Source/DafnyCore/DooFile.cs

@@ -69,9 +69,18 @@ public void Write(TextWriter writer) {
   private static DafnyOptions ProgramSerializationOptions => DafnyOptions.Default;
 
   public static DooFile Read(string path) {
+    using var archive = ZipFile.Open(path, ZipArchiveMode.Read);
+    return Read(archive);
+  }
+
+  public static DooFile Read(Stream stream) {
+    using var archive = new ZipArchive(stream);
+    return Read(archive);
+  }
+
+  private static DooFile Read(ZipArchive archive) {
     var result = new DooFile();
 
-    using var archive = ZipFile.Open(path, ZipArchiveMode.Read);
     var manifestEntry = archive.GetEntry(ManifestFileEntry);
     if (manifestEntry == null) {
       throw new ArgumentException(".doo file missing manifest entry");
@@ -119,12 +128,12 @@ public bool Validate(string filePath, DafnyOptions options, Command currentComma
     }
 
     var success = true;
-    var revelantOptions = currentCommand.Options.ToHashSet();
+    var relevantOptions = currentCommand.Options.ToHashSet();
     foreach (var (option, check) in OptionChecks) {
       // It's important to only look at the options the current command uses,
       // because other options won't be initialized to the correct default value.
       // See CommandRegistry.Create().
-      if (!revelantOptions.Contains(option)) {
+      if (!relevantOptions.Contains(option)) {
         continue;
       }
 
@@ -212,6 +221,30 @@ public static bool CheckOptionMatches(DafnyOptions options, Option option, objec
     return false;
   }
 
+  /// Checks that the library option ==> the local option.
+  /// E.g. --no-verify: the only incompatibility is if it's on in the library but not locally.
+  /// Generally the right check for options that weaken guarantees.
+  public static bool CheckOptionLibraryImpliesLocal(DafnyOptions options, Option option, object localValue, string libraryFile, object libraryValue) {
+    if (OptionValuesImplied(option, libraryValue, localValue)) {
+      return true;
+    }
+
+    options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: Cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
+    return false;
+  }
+
+  /// Checks that the local option ==> the library option.
+  /// E.g. --track-print-effects: the only incompatibility is if it's on locally but not in the library.
+  /// Generally the right check for options that strengthen guarantees.
+  public static bool CheckOptionLocalImpliesLibrary(DafnyOptions options, Option option, object localValue, string libraryFile, object libraryValue) {
+    if (OptionValuesImplied(option, localValue, libraryValue)) {
+      return true;
+    }
+
+    options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: Cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
+    return false;
+  }
+
   private static bool OptionValuesEqual(Option option, object first, object second) {
     if (first.Equals(second)) {
       return true;
@@ -224,6 +257,12 @@ private static bool OptionValuesEqual(Option option, object first, object second
     return false;
   }
 
+  private static bool OptionValuesImplied(Option option, object first, object second) {
+    var lhs = (bool)first;
+    var rhs = (bool)second;
+    return !lhs || rhs;
+  }
+
   private static string OptionValueToString(Option option, object value) {
     if (option.ValueType == typeof(IEnumerable<string>)) {
       var values = (IEnumerable<string>)value;

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -136,7 +136,7 @@ static BoogieOptionBag() {
       new Dictionary<Option, DooFile.OptionCheck> {
         { BoogieArguments, DooFile.CheckOptionMatches },
         { BoogieFilter, DooFile.CheckOptionMatches },
-        { NoVerify, DooFile.CheckOptionMatches },
+        { NoVerify, DooFile.CheckOptionLibraryImpliesLocal },
       }
     );
     DooFile.RegisterNoChecksNeeded(

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -258,6 +258,13 @@ public enum DefaultFunctionOpacityOptions {
 `opaque` means functions are always opaque so the opaque keyword is not needed, and functions must be revealed everywhere needed for a proof.".TrimStart()) {
   };
 
+  public static readonly Option<bool> UseStandardLibraries = new("--standard-libraries", () => false,
+    @"
+Allow Dafny code to depend on the standard libraries included with the Dafny distribution.
+See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for more information.
+Not compatible with the --unicode-char:false option.
+");
+
   static CommonOptionBag() {
     DafnyOptions.RegisterLegacyUi(Target, DafnyOptions.ParseString, "Compilation options", "compileTarget", @"
 cs (default) - Compile to .NET via C#.
@@ -438,18 +445,9 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
     DooFile.RegisterLibraryChecks(
       new Dictionary<Option, DooFile.OptionCheck>() {
         { UnicodeCharacters, DooFile.CheckOptionMatches },
-        { EnforceDeterminism, DooFile.CheckOptionMatches },
-        { RelaxDefiniteAssignment, DooFile.CheckOptionMatches },
-        // Ideally this feature shouldn't affect separate compilation,
-        // because it's automatically disabled on {:extern} signatures.
-        // Realistically though, we don't have enough strong mechanisms to stop
-        // target language code from referencing compiled internal code,
-        // so to be conservative we flag this as not compatible in general.
-        { OptimizeErasableDatatypeWrapper, DooFile.CheckOptionMatches },
-        // Similarly this shouldn't matter if external code ONLY refers to {:extern}s,
-        // but in practice it does.
-        { AddCompileSuffix, DooFile.CheckOptionMatches },
-        { ReadsClausesOnMethods, DooFile.CheckOptionMatches },
+        { EnforceDeterminism, DooFile.CheckOptionLocalImpliesLibrary },
+        { RelaxDefiniteAssignment, DooFile.CheckOptionLibraryImpliesLocal },
+        { ReadsClausesOnMethods, DooFile.CheckOptionLocalImpliesLibrary },
       }
     );
     DooFile.RegisterNoChecksNeeded(
@@ -485,7 +483,10 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       WarnRedundantAssumptions,
       VerificationCoverageReport,
       NoTimeStampForCoverageReport,
-      DefaultFunctionOpacity
+      DefaultFunctionOpacity,
+      UseStandardLibraries,
+      OptimizeErasableDatatypeWrapper,
+      AddCompileSuffix
     );
   }
 

Source/DafnyCore/Options/DafnyCommands.cs

@@ -85,7 +85,8 @@ static DafnyCommands() {
     CommonOptionBag.TypeSystemRefresh,
     CommonOptionBag.TypeInferenceDebug,
     CommonOptionBag.NewTypeInferenceDebug,
-    CommonOptionBag.ReadsClausesOnMethods
+    CommonOptionBag.ReadsClausesOnMethods,
+    CommonOptionBag.UseStandardLibraries
   });
 
   public static IReadOnlyList<Option> ResolverOptions = new List<Option>(new Option[] {

Source/DafnyDriver/Commands/DafnyCli.cs

@@ -31,6 +31,8 @@ public static class DafnyCli {
   private const string ToolchainDebuggingHelpName = "--help-internal";
   private static readonly RootCommand RootCommand = new("The Dafny CLI enables working with Dafny, a verification-aware programming language. Use 'dafny -?' to see help for the previous CLI format.");
 
+  private static readonly Uri StandardLibrariesDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries.doo");
+
   public static int Main(string[] args) {
     return MainWithWriters(Console.Out, Console.Error, Console.In, args);
   }
@@ -481,6 +483,14 @@ public static ExitValue GetDafnyFiles(DafnyOptions options,
       return ExitValue.PREPROCESSING_ERROR;
     }
 
+    // Add standard library .doo files after explicitly provided source files,
+    // only because if they are added first, one might be used as the program name,
+    // which is not handled well.
+    if (options.Get(CommonOptionBag.UseStandardLibraries)) {
+      options.CliRootSourceUris.Add(StandardLibrariesDooUri);
+      dafnyFiles.Add(new DafnyFile(options, StandardLibrariesDooUri));
+    }
+
     return ExitValue.SUCCESS;
   }