From 2e6938dc3315f64eee9737b241ee583a83cedc3a Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Tue, 30 Apr 2024 08:07:16 -0700
Subject: [PATCH] feat: Translation records (#5346)

---
 .../ClientApp/GroceryListPrinter.dfy.expect   |   1 +
 Source/DafnyCore/AST/CompilationData.cs       |   3 +
 Source/DafnyCore/AST/Members/Method.cs        |   3 +-
 .../DafnyCore/AST/Members/MethodOrFunction.cs |   3 +-
 .../AST/Statements/Methods/PrintStmt.cs       |   5 +-
 .../Backends/DafnyExecutableBackend.cs        |   4 +-
 .../DafnyCore/Backends/ExecutableBackend.cs   |  68 ++++++-
 .../Backends/Library/LibraryBackend.cs        |   2 +-
 Source/DafnyCore/DooFile.cs                   | 102 +----------
 Source/DafnyCore/Options/BoogieOptionBag.cs   |   7 +-
 Source/DafnyCore/Options/CommonOptionBag.cs   |  17 +-
 Source/DafnyCore/Options/DafnyCommands.cs     |   8 +-
 .../DafnyCore/Options/OptionCompatibility.cs  |  87 +++++++++
 Source/DafnyCore/Options/TranslationRecord.cs | 172 ++++++++++++++++++
 .../DafnyCore/Pipeline/NoExecutableBackend.cs |   2 +-
 .../DafnyCore/Plugins/IExecutableBackend.cs   |  26 ++-
 .../DafnyDriver/Commands/TranslateCommand.cs  |   3 +-
 Source/DafnyDriver/Commands/VerifyCommand.cs  |   2 +
 .../Legacy/SynchronousCliCompilation.cs       |  14 +-
 .../CompileAndThenRun.dfy.expect              | 157 ++++++++--------
 .../LitTest/comp/compile3/JustRun.dfy.expect  | 156 ++++++++--------
 .../manualcompile/ManualCompile.dfy.expect    | 158 ++++++++--------
 .../translation-records/Bar.dtr               |   4 +
 .../translation-records/DuplicateModules.dfy  |  11 ++
 .../DuplicateModules.dfy.expect               |  10 +
 .../translation-records/DuplicateModules.dtr  |   3 +
 .../translation-records/Foo.dtr               |   4 +
 .../translation-records/InvalidFormat.dfy     |   7 +
 .../InvalidFormat.dfy.expect                  |   8 +
 .../translation-records/NoGood.dtr            |   1 +
 .../translation-records/WrongDafnyVersion.dtr |   2 +
 .../separate-compilation/usesTimesTwo.dfy     |   8 +-
 docs/DafnyRef/UserGuide.md                    |  29 ++-
 docs/dev/news/5346.feat                       |   4 +
 34 files changed, 721 insertions(+), 370 deletions(-)
 create mode 100644 Source/DafnyCore/Options/OptionCompatibility.cs
 create mode 100644 Source/DafnyCore/Options/TranslationRecord.cs
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/Bar.dtr
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dtr
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/Foo.dtr
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/NoGood.dtr
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/WrongDafnyVersion.dtr
 create mode 100644 docs/dev/news/5346.feat

diff --git a/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect b/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect
index 03a358a4c2b..44366de2ee0 100644
--- a/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect
+++ b/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect
@@ -2,6 +2,7 @@ Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help
 
 Dafny program verifier did not attempt verification
 Wrote textual form of target program to GroceryListPrinter.cs
+Additional output written to GroceryListPrinter-cs.dtr
 # Printing a grocery list
    (2 items in the list)
 ## Apple: 3 @ 1.00
diff --git a/Source/DafnyCore/AST/CompilationData.cs b/Source/DafnyCore/AST/CompilationData.cs
index 45f9c30a283..ce827a7c0d9 100644
--- a/Source/DafnyCore/AST/CompilationData.cs
+++ b/Source/DafnyCore/AST/CompilationData.cs
@@ -1,5 +1,6 @@
 using System;
 using System.Collections.Generic;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny;
 
@@ -28,4 +29,6 @@ public class CompilationData {
   // TODO move to DocumentAfterParsing once that's used by the CLI
   [FilledInDuringResolution]
   public ISet<Uri> UrisToCompile;
+
+  public TranslationRecord AlreadyTranslatedRecord { get; set; }
 }
\ No newline at end of file
diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs
index f99df5613f6..1d615e908a7 100644
--- a/Source/DafnyCore/AST/Members/Method.cs
+++ b/Source/DafnyCore/AST/Members/Method.cs
@@ -4,6 +4,7 @@
 using System.Linq;
 using System.Numerics;
 using DafnyCore;
+using DafnyCore.Options;
 using Microsoft.Dafny.Auditor;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
@@ -20,7 +21,7 @@ public class Method : MethodOrFunction, TypeParameter.ParentType,
     DafnyOptions.RegisterLegacyUi(ReadsClausesOnMethods, DafnyOptions.ParseBoolean, "Language feature selection", "readsClausesOnMethods", @"
 0 (default) - Reads clauses on methods are forbidden.
 1 - Reads clauses on methods are permitted (with a default of 'reads *').".TrimStart(), defaultValue: false);
-    DooFile.RegisterLibraryCheck(ReadsClausesOnMethods, DooFile.CheckOptionLocalImpliesLibrary);
+    DooFile.RegisterLibraryCheck(ReadsClausesOnMethods, OptionCompatibility.CheckOptionLocalImpliesLibrary);
   }
 
   public override IEnumerable<INode> Children => new Node[] { Body, Decreases }.Where(x => x != null).
diff --git a/Source/DafnyCore/AST/Members/MethodOrFunction.cs b/Source/DafnyCore/AST/Members/MethodOrFunction.cs
index 74d375af2b3..76e791c6b8b 100644
--- a/Source/DafnyCore/AST/Members/MethodOrFunction.cs
+++ b/Source/DafnyCore/AST/Members/MethodOrFunction.cs
@@ -2,6 +2,7 @@
 using System.CommandLine;
 using System.Linq;
 using DafnyCore;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny;
 
@@ -10,7 +11,7 @@ public abstract class MethodOrFunction : MemberDecl {
     "Allow exporting callables with preconditions, and importing callables with postconditions");
 
   static MethodOrFunction() {
-    DooFile.RegisterLibraryCheck(AllowExternalContracts, DooFile.CheckOptionLibraryImpliesLocal);
+    DooFile.RegisterLibraryCheck(AllowExternalContracts, OptionCompatibility.CheckOptionLibraryImpliesLocal);
   }
 
   public readonly List<TypeParameter> TypeArgs;
diff --git a/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs b/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs
index a12311e6521..cf08c54bfa6 100644
--- a/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs
+++ b/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs
@@ -3,6 +3,7 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using DafnyCore;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny;
 
@@ -17,8 +18,8 @@ public class PrintStmt : Statement, ICloneable<PrintStmt>, ICanFormat {
     });
 
     DooFile.RegisterLibraryChecks(
-      checks: new Dictionary<Option, DooFile.OptionCheck> {
-        { TrackPrintEffectsOption, DooFile.CheckOptionLocalImpliesLibrary }
+      checks: new Dictionary<Option, OptionCompatibility.OptionCheck> {
+        { TrackPrintEffectsOption, OptionCompatibility.CheckOptionLocalImpliesLibrary }
       });
   }
 
diff --git a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs
index 18c955848cd..baa2446c162 100644
--- a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs
+++ b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs
@@ -31,9 +31,11 @@ public abstract class DafnyExecutableBackend : ExecutableBackend {
     DafnyCodeGenerator = CreateDafnyWrittenCompiler();
   }
 
-  public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
+  public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
+    ProcessTranslationRecords(dafnyProgram, dafnyProgramName, output);
     CheckInstantiationReplaceableModules(dafnyProgram);
     ProcessOuterModules(dafnyProgram);
+
     ((DafnyCodeGenerator)codeGenerator).Start();
     codeGenerator.Compile(dafnyProgram, new ConcreteSyntaxTree());
     var dast = ((DafnyCodeGenerator)codeGenerator).Build();
diff --git a/Source/DafnyCore/Backends/ExecutableBackend.cs b/Source/DafnyCore/Backends/ExecutableBackend.cs
index cd4c50a8a1a..0c6ce2785ba 100644
--- a/Source/DafnyCore/Backends/ExecutableBackend.cs
+++ b/Source/DafnyCore/Backends/ExecutableBackend.cs
@@ -6,6 +6,7 @@
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
+using DafnyCore.Options;
 using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.Plugins;
 
@@ -25,12 +26,33 @@ public abstract class ExecutableBackend : IExecutableBackend {
 
   public override string ModuleSeparator => CodeGenerator.ModuleSeparator;
 
-  public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
+  public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
+    ProcessTranslationRecords(dafnyProgram, dafnyProgramName, output);
     CheckInstantiationReplaceableModules(dafnyProgram);
     ProcessOuterModules(dafnyProgram);
+
     CodeGenerator.Compile(dafnyProgram, output);
   }
 
+  protected void ProcessTranslationRecords(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
+    // Process --translation-record options, since translation may need that data to translate correctly.
+    dafnyProgram.Compilation.AlreadyTranslatedRecord = TranslationRecord.Empty(dafnyProgram);
+    var records = dafnyProgram.Options.Get(TranslationRecords);
+    if (records != null) {
+      foreach (var path in records) {
+        TranslationRecord.ReadValidateAndMerge(dafnyProgram, path.FullName, Token.Cli);
+      }
+    }
+
+    // Write out the translation record for THIS translation before compiling,
+    // in case the compilation process mutates the program.
+    var translationRecord = new TranslationRecord(dafnyProgram);
+    var baseName = Path.GetFileNameWithoutExtension(dafnyProgramName);
+    var dtrFilePath = dafnyProgram.Options.Get(TranslationRecordOutput)?.FullName ?? $"{baseName}-{TargetId}.dtr";
+    var dtrWriter = output.NewFile(dtrFilePath);
+    translationRecord.Write(dtrWriter);
+  }
+
   protected void CheckInstantiationReplaceableModules(Program dafnyProgram) {
     foreach (var compiledModule in dafnyProgram.Modules()) {
       if (compiledModule.Implements is { Kind: ImplementationKind.Replacement }) {
@@ -50,17 +72,27 @@ public abstract class ExecutableBackend : IExecutableBackend {
   }
 
   protected void ProcessOuterModules(Program dafnyProgram) {
-    var outerModules = GetOuterModules();
-    ModuleDefinition rootUserModule = null;
-    foreach (var outerModule in outerModules) {
-      var newRoot = new ModuleDefinition(RangeToken.NoToken, new Name(outerModule), new List<IToken>(),
-        ModuleKindEnum.Concrete, false,
-        null, null, null);
-      newRoot.EnclosingModule = rootUserModule;
-      rootUserModule = newRoot;
+    // Apply the --outer-module option from any translation records for libraries,
+    // but only to top-level modules.
+    var outerModules = new Dictionary<string, ModuleDefinition>();
+    foreach (var module in dafnyProgram.CompileModules) {
+      if (module.EnclosingModule is not DefaultModuleDefinition) {
+        continue;
+      }
+
+      var recordedOuterModuleName = (string)dafnyProgram.Compilation.AlreadyTranslatedRecord.Get(null, module.FullDafnyName, OuterModule);
+      if (recordedOuterModuleName == null) {
+        continue;
+      }
+
+      var outerModule = outerModules.GetOrCreate(recordedOuterModuleName, () => CreateOuterModule(recordedOuterModuleName));
+      module.EnclosingModule = outerModule;
     }
 
-    if (rootUserModule != null) {
+    // Apply the local --output-module option if there is one
+    var outerModuleName = Options.Get(OuterModule);
+    if (outerModuleName != null) {
+      var rootUserModule = outerModules.GetOrCreate(outerModuleName, () => CreateOuterModule(outerModuleName));
       dafnyProgram.DefaultModuleDef.NameNode = rootUserModule.NameNode;
       dafnyProgram.DefaultModuleDef.EnclosingModule = rootUserModule.EnclosingModule;
     }
@@ -70,6 +102,22 @@ public abstract class ExecutableBackend : IExecutableBackend {
     }
   }
 
+  private static ModuleDefinition CreateOuterModule(string moduleName) {
+    var outerModules = moduleName.Split(".");
+
+    ModuleDefinition module = null;
+    foreach (var outerModule in outerModules) {
+      var thisModule = new ModuleDefinition(RangeToken.NoToken, new Name(outerModule), new List<IToken>(),
+        ModuleKindEnum.Concrete, false,
+        null, null, null) {
+        EnclosingModule = module
+      };
+      module = thisModule;
+    }
+
+    return module;
+  }
+
   public override void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection<string> otherFileNames) {
     base.OnPreCompile(reporter, otherFileNames);
     codeGenerator = CreateCodeGenerator();
diff --git a/Source/DafnyCore/Backends/Library/LibraryBackend.cs b/Source/DafnyCore/Backends/Library/LibraryBackend.cs
index 5f125bab805..185a7f0678e 100644
--- a/Source/DafnyCore/Backends/Library/LibraryBackend.cs
+++ b/Source/DafnyCore/Backends/Library/LibraryBackend.cs
@@ -52,7 +52,7 @@ public class LibraryBackend : ExecutableBackend {
     throw new NotSupportedException();
   }
 
-  public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
+  public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
     if (!Options.UsingNewCli) {
       throw new UnsupportedFeatureException(dafnyProgram.GetStartOfFirstFileToken(), Feature.LegacyCLI);
     }
diff --git a/Source/DafnyCore/DooFile.cs b/Source/DafnyCore/DooFile.cs
index cc49b4ed32d..9d7bddf4df0 100644
--- a/Source/DafnyCore/DooFile.cs
+++ b/Source/DafnyCore/DooFile.cs
@@ -8,6 +8,7 @@
 using System.Text;
 using System.Threading.Tasks;
 using DafnyCore.Generic;
+using DafnyCore.Options;
 using Microsoft.Dafny;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 using Tomlyn;
@@ -48,7 +49,7 @@ public class ManifestData {
 
       Options = new Dictionary<string, object>();
       foreach (var (option, _) in OptionChecks) {
-        var optionValue = GetOptionValue(options, option);
+        var optionValue = options.Get((dynamic)option);
         Options.Add(option.Name, optionValue);
       }
     }
@@ -173,7 +174,8 @@ public class ManifestData {
       }
 
       result.Options.OptionArguments[option] = libraryValue;
-      success = success && check(reporter, origin, option, localValue, options.GetPrintPath(libraryFile), libraryValue);
+      var prefix = $"cannot load {options.GetPrintPath(libraryFile)}";
+      success = success && check(reporter, origin, prefix, option, localValue, libraryValue);
     }
 
     if (!success) {
@@ -183,25 +185,6 @@ public class ManifestData {
     return result;
   }
 
-  private static object GetOptionValue(DafnyOptions options, Option option) {
-    // This is annoyingly necessary because only DafnyOptions.Get<T>(Option<T> option)
-    // handles falling back to the configured default option value,
-    // whereas the non-generic DafnyOptions.Get(Option option) doesn't.
-    // TODO: Move somewhere more generic if this is useful in other cases?
-    var optionType = option.ValueType;
-    if (optionType == typeof(bool)) {
-      return options.Get((Option<bool>)option);
-    }
-    if (optionType == typeof(string)) {
-      return options.Get((Option<string>)option);
-    }
-    if (optionType == typeof(IEnumerable<string>)) {
-      return options.Get((Option<IEnumerable<string>>)option);
-    }
-
-    throw new ArgumentException();
-  }
-
   public void Write(ConcreteSyntaxTree wr) {
     var manifestWr = wr.NewFile(ManifestFileEntry);
     using var manifestWriter = new StringWriter();
@@ -237,88 +220,17 @@ public class ManifestData {
   // more difficult to completely categorize, which is the main reason the LibraryBackend
   // is restricted to only the new CLI.
 
-  public delegate bool OptionCheck(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue);
-  private static readonly Dictionary<Option, OptionCheck> OptionChecks = new();
+  private static readonly Dictionary<Option, OptionCompatibility.OptionCheck> OptionChecks = new();
   private static readonly HashSet<Option> NoChecksNeeded = new();
 
-  public static bool CheckOptionMatches(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue) {
-    if (OptionValuesEqual(option, localValue, libraryValue)) {
-      return true;
-    }
-
-    reporter.Error(MessageSource.Project, origin,
-      $"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 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(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue) {
-    if (OptionValuesImplied(libraryValue, localValue)) {
-      return true;
-    }
-
-    reporter.Error(MessageSource.Project, origin, $"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(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue) {
-    if (OptionValuesImplied(localValue, libraryValue)) {
-      return true;
-    }
-    reporter.Error(MessageSource.Project, origin, LocalImpliesLibraryMessage(option, localValue, libraryFile, libraryValue));
-    return false;
-  }
-
-  public static string LocalImpliesLibraryMessage(Option option, object localValue, string libraryFile, object libraryValue) {
-    return $"cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}";
-  }
-
-  private static bool OptionValuesEqual(Option option, object first, object second) {
-    if (first.Equals(second)) {
-      return true;
-    }
-
-    if (option.ValueType == typeof(IEnumerable<string>)) {
-      return ((IEnumerable<string>)first).SequenceEqual((IEnumerable<string>)second);
-    }
-
-    return false;
-  }
-
-  public static bool OptionValuesImplied(object first, object second) {
-    try {
-      return !(bool)first || (bool)second;
-    } catch (NullReferenceException) {
-      throw new Exception("Comparing options of Doo files created by different Dafny builds. You are probably using a locally built Dafny that has the same version as a different built.");
-    }
-  }
-
-  private static string OptionValueToString(Option option, object value) {
-    if (option.ValueType == typeof(IEnumerable<string>)) {
-      var values = (IEnumerable<string>)value;
-      return $"[{string.Join(',', values)}]";
-    }
-
-    if (value == null) {
-      return "a version of Dafny that does not have this option";
-    }
-    return value.ToString();
-  }
-
-  public static void RegisterLibraryCheck(Option option, OptionCheck check) {
+  public static void RegisterLibraryCheck(Option option, OptionCompatibility.OptionCheck check) {
     if (NoChecksNeeded.Contains(option)) {
       throw new ArgumentException($"Option already registered as not needing a library check: {option.Name}");
     }
     OptionChecks.Add(option, check);
   }
 
-  public static void RegisterLibraryChecks(IDictionary<Option, OptionCheck> checks) {
+  public static void RegisterLibraryChecks(IDictionary<Option, OptionCompatibility.OptionCheck> checks) {
     foreach (var (option, check) in checks) {
       RegisterLibraryCheck(option, check);
     }
diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs
index 359acea2fc7..71a66fc4600 100644
--- a/Source/DafnyCore/Options/BoogieOptionBag.cs
+++ b/Source/DafnyCore/Options/BoogieOptionBag.cs
@@ -5,6 +5,7 @@
 using System.Linq;
 using System.Transactions;
 using DafnyCore;
+using DafnyCore.Options;
 using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
@@ -138,9 +139,9 @@ public static class BoogieOptionBag {
 
 
     DooFile.RegisterLibraryChecks(
-      new Dictionary<Option, DooFile.OptionCheck> {
-        { BoogieArguments, DooFile.CheckOptionMatches },
-        { NoVerify, DooFile.CheckOptionLibraryImpliesLocal },
+      new Dictionary<Option, OptionCompatibility.OptionCheck> {
+        { BoogieArguments, OptionCompatibility.CheckOptionMatches },
+        { NoVerify, OptionCompatibility.CheckOptionLibraryImpliesLocal },
       }
     );
     DooFile.RegisterNoChecksNeeded(
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index 5b0f1cf083a..a4fec14df0b 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -3,6 +3,7 @@
 using System.IO;
 using System.Linq;
 using DafnyCore;
+using DafnyCore.Options;
 using Serilog.Events;
 
 namespace Microsoft.Dafny;
@@ -579,16 +580,16 @@ public enum DefaultFunctionOpacityOptions {
     });
 
     DooFile.RegisterLibraryChecks(
-      new Dictionary<Option, DooFile.OptionCheck>() {
-        { UnicodeCharacters, DooFile.CheckOptionMatches },
-        { EnforceDeterminism, DooFile.CheckOptionLocalImpliesLibrary },
-        { RelaxDefiniteAssignment, DooFile.CheckOptionLibraryImpliesLocal },
-        { AllowAxioms, DooFile.CheckOptionLibraryImpliesLocal },
-        { AllowWarnings, (reporter, origin, option, localValue, libraryFile, libraryValue) => {
-            if (DooFile.OptionValuesImplied(libraryValue, localValue)) {
+      new Dictionary<Option, OptionCompatibility.OptionCheck>() {
+        { UnicodeCharacters, OptionCompatibility.CheckOptionMatches },
+        { EnforceDeterminism, OptionCompatibility.CheckOptionLocalImpliesLibrary },
+        { RelaxDefiniteAssignment, OptionCompatibility.CheckOptionLibraryImpliesLocal },
+        { AllowAxioms, OptionCompatibility.CheckOptionLibraryImpliesLocal },
+        { AllowWarnings, (reporter, origin, prefix, option, localValue, libraryValue) => {
+            if (OptionCompatibility.OptionValuesImplied(libraryValue, localValue)) {
               return true;
             }
-            string message = DooFile.LocalImpliesLibraryMessage(option, localValue, libraryFile, libraryValue);
+            string message = OptionCompatibility.LocalImpliesLibraryMessage(prefix, option, localValue, libraryValue);
             reporter.Warning(MessageSource.Project, ResolutionErrors.ErrorId.none, origin, message);
             return false;
           }
diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs
index 51551086dc0..fe91047573b 100644
--- a/Source/DafnyCore/Options/DafnyCommands.cs
+++ b/Source/DafnyCore/Options/DafnyCommands.cs
@@ -3,6 +3,7 @@
 using System.IO;
 using System.Linq;
 using DafnyCore;
+using Microsoft.Dafny.Plugins;
 
 namespace Microsoft.Dafny;
 
@@ -24,7 +25,7 @@ public static class DafnyCommands {
     CommonOptionBag.FormatPrint,
   }.Concat(ParserOptions);
 
-  public static IReadOnlyList<Option> VerificationOptions = new Option[] {
+  public static readonly IReadOnlyList<Option> VerificationOptions = new Option[] {
     CommonOptionBag.ProgressOption,
     CommonOptionBag.RelaxDefiniteAssignment,
     BoogieOptionBag.VerificationTimeLimit,
@@ -52,14 +53,15 @@ public static class DafnyCommands {
     CommonOptionBag.ShowProofObligationExpressions
   }.ToList();
 
-  public static IReadOnlyList<Option> TranslationOptions = new Option[] {
+  public static readonly IReadOnlyList<Option> TranslationOptions = new Option[] {
     BoogieOptionBag.NoVerify,
     CommonOptionBag.EnforceDeterminism,
     CommonOptionBag.OptimizeErasableDatatypeWrapper,
     CommonOptionBag.TestAssumptions,
     DeveloperOptionBag.Bootstrapping,
     CommonOptionBag.AddCompileSuffix,
-    CommonOptionBag.SystemModule
+    CommonOptionBag.SystemModule,
+    IExecutableBackend.TranslationRecords,
   }.Concat(VerificationOptions).ToList();
 
   public static readonly IReadOnlyList<Option> ExecutionOptions = new Option[] {
diff --git a/Source/DafnyCore/Options/OptionCompatibility.cs b/Source/DafnyCore/Options/OptionCompatibility.cs
new file mode 100644
index 00000000000..f3b5f8fa57c
--- /dev/null
+++ b/Source/DafnyCore/Options/OptionCompatibility.cs
@@ -0,0 +1,87 @@
+using System;
+using System.Collections.Generic;
+using System.CommandLine;
+using Microsoft.Dafny;
+using System.Linq;
+
+namespace DafnyCore.Options;
+
+public class OptionCompatibility {
+  public delegate bool OptionCheck(ErrorReporter reporter, IToken origin, string prefix, Option option, object localValue, object libraryValue);
+
+  public static bool CheckOptionMatches(ErrorReporter reporter, IToken origin, string prefix, Option option, object localValue, object libraryValue) {
+    if (OptionValuesEqual(option, localValue, libraryValue)) {
+      return true;
+    }
+
+    reporter.Error(MessageSource.Project, origin,
+      $"{prefix}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, " +
+      $"but the library was built with {OptionValueToString(option, libraryValue)}");
+    return false;
+  }
+
+  private static string OptionValueToString(Option option, object value) {
+    if (option.ValueType == typeof(IEnumerable<string>)) {
+      var values = (IEnumerable<string>)value;
+      return $"[{string.Join(',', values)}]";
+    }
+
+    if (value == null) {
+      return "a version of Dafny that does not have this option";
+    }
+    return value.ToString();
+  }
+
+  private static bool OptionValuesEqual(Option option, object first, object second) {
+    if (first.Equals(second)) {
+      return true;
+    }
+
+    if (option.ValueType == typeof(IEnumerable<string>)) {
+      return ((IEnumerable<string>)first).SequenceEqual((IEnumerable<string>)second);
+    }
+
+    return false;
+  }
+
+  public static bool OptionValuesImplied(object first, object second) {
+    try {
+      return !(bool)first || (bool)second;
+    } catch (NullReferenceException) {
+      throw new Exception("Comparing options of Doo files created by different Dafny builds. You are probably using a locally built Dafny that has the same version as a different built.");
+    }
+  }
+
+  /// 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(ErrorReporter reporter, IToken origin, string prefix, Option option, object localValue, object libraryValue) {
+    if (OptionValuesImplied(libraryValue, localValue)) {
+      return true;
+    }
+
+    reporter.Error(MessageSource.Project, origin, $"{prefix}: --{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(ErrorReporter reporter, IToken origin, string prefix, Option option, object localValue, object libraryValue) {
+    if (OptionValuesImplied(localValue, libraryValue)) {
+      return true;
+    }
+    reporter.Error(MessageSource.Project, origin, LocalImpliesLibraryMessage(prefix, option, localValue, libraryValue));
+    return false;
+  }
+
+  public static string LocalImpliesLibraryMessage(string prefix, Option option, object localValue, object libraryValue) {
+    return $"{prefix}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}";
+  }
+
+
+  // Placeholder no-op check, used for options that need to be recorded but don't require any compatibility check.
+  public static bool NoOpOptionCheck(ErrorReporter reporter, IToken origin, string prefix, Option option, object localValue, object libraryValue) {
+    return true;
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyCore/Options/TranslationRecord.cs b/Source/DafnyCore/Options/TranslationRecord.cs
new file mode 100644
index 00000000000..06f7e64bffc
--- /dev/null
+++ b/Source/DafnyCore/Options/TranslationRecord.cs
@@ -0,0 +1,172 @@
+using System.Collections.Generic;
+using System.CommandLine;
+using System.IO;
+using System.Linq;
+using DafnyCore.Generic;
+using Microsoft.Dafny;
+using Microsoft.Dafny.Plugins;
+using Tomlyn;
+
+namespace DafnyCore.Options;
+
+// Model class for the .dtr file format for Dafny Translation Records.
+// Contains the validation logic for safely consuming pre-translated libraries as well.
+// See https://dafny.org/dafny/DafnyRef/DafnyRef#sec-dtr-files.
+public class TranslationRecord {
+
+  public const string CurrentFileFormatVersion = "1.0";
+  public string FileFormatVersion { get; set; }
+
+  public string DafnyVersion { get; set; }
+
+  public Dictionary<string, Dictionary<string, object>> OptionsByModule { get; set; }
+
+
+  public TranslationRecord(Program program) {
+    FileFormatVersion = CurrentFileFormatVersion;
+    DafnyVersion = program.Options.VersionNumber;
+
+    OptionsByModule = new();
+
+    foreach (var module in program.RawModules()) {
+      if (module is DefaultModuleDefinition || !module.ShouldCompile(program.Compilation)) {
+        continue;
+      }
+
+      Dictionary<string, object> recordedOptions = new();
+      OptionsByModule[module.FullDafnyName] = recordedOptions;
+
+      foreach (var (option, _) in OptionChecks) {
+        var optionValue = program.Options.Get((dynamic)option);
+        recordedOptions.Add(option.Name, optionValue);
+      }
+    }
+  }
+
+  public static TranslationRecord Empty(Program program) {
+    return new TranslationRecord() {
+      FileFormatVersion = CurrentFileFormatVersion,
+      DafnyVersion = program.Options.VersionNumber,
+      OptionsByModule = new()
+    };
+  }
+
+  public TranslationRecord() {
+    // Only for TOML deserialization!
+  }
+
+  public static void ReadValidateAndMerge(Program program, string filePath, IToken origin) {
+    var pathForErrors = program.Options.GetPrintPath(filePath);
+    try {
+      using TextReader reader = new StreamReader(filePath);
+      var record = Read(reader);
+      if (record.Validate(program, pathForErrors, origin)) {
+        program.Compilation.AlreadyTranslatedRecord.Merge(program.Reporter, record, pathForErrors, origin);
+      }
+    } catch (FileNotFoundException) {
+      program.Reporter.Error(MessageSource.Project, origin, $"file {pathForErrors} not found");
+    } catch (TomlException) {
+      program.Reporter.Error(MessageSource.Project, origin, $"malformed dtr file {pathForErrors}");
+    }
+  }
+
+  private static TranslationRecord Read(TextReader reader) {
+    return Toml.ToModel<TranslationRecord>(reader.ReadToEnd(), null, new TomlModelOptions());
+  }
+
+  public void Write(TextWriter writer) {
+    writer.Write(Toml.FromModel(this, new TomlModelOptions()).Replace("\r\n", "\n"));
+  }
+
+  public void Write(ConcreteSyntaxTree writer) {
+    using var textWriter = new StringWriter();
+    Write(textWriter);
+    writer.Write(textWriter.ToString());
+  }
+
+  private bool Validate(Program dafnyProgram, string filePath, IToken origin) {
+    var messagePrefix = $"cannot load {filePath}";
+    if (!dafnyProgram.Options.UsingNewCli) {
+      dafnyProgram.Reporter.Error(MessageSource.Project, origin,
+        $"{messagePrefix}: .dtr files cannot be used with the legacy CLI");
+      return false;
+    }
+
+    if (dafnyProgram.Options.VersionNumber != DafnyVersion) {
+      dafnyProgram.Reporter.Error(MessageSource.Project, origin,
+        $"{messagePrefix}: it was built with Dafny {DafnyVersion}, which cannot be used by Dafny {dafnyProgram.Options.VersionNumber}");
+      return false;
+    }
+
+    // Modules should be either previously compiled or to be compiled now, not both
+    foreach (var module in dafnyProgram.CompileModules) {
+      if (module.ShouldCompile(dafnyProgram.Compilation) && OptionsByModule.ContainsKey(module.FullDafnyName)) {
+        dafnyProgram.Reporter.Error(MessageSource.Project, origin,
+          $"{messagePrefix}: it contains translation metadata for the module {module.FullDafnyName}, which is in scope for translation in the current program");
+      }
+    }
+
+    var success = true;
+    // Yo dawg, we heard you liked options so we put Options in your Options... :)
+    var relevantOptions = dafnyProgram.Options.Options.OptionArguments.Keys.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 (!relevantOptions.Contains(option)) {
+        continue;
+      }
+
+      var localValue = dafnyProgram.Options.Get(option);
+
+      foreach (var moduleName in OptionsByModule.Keys) {
+        var libraryValue = Get(dafnyProgram.Reporter, moduleName, option);
+        success = success && check(dafnyProgram.Reporter, origin, messagePrefix, option, localValue, libraryValue);
+      }
+    }
+
+    return success;
+  }
+
+  public object Get(ErrorReporter reporter, string moduleName, Option option) {
+    if (OptionsByModule.TryGetValue(moduleName, out var moduleOptions)) {
+      if (moduleOptions.TryGetValue(option.Name, out var manifestValue)) {
+        if (TomlUtil.TryGetValueFromToml(reporter, Token.NoToken, null,
+              option.Name, option.ValueType, manifestValue, out var libraryValue)) {
+          return libraryValue;
+        }
+      }
+    }
+
+    return null;
+  }
+
+  private void Merge(ErrorReporter reporter, TranslationRecord other, string filePath, IToken origin) {
+    // Assume both this and other have been Validate()-d already.
+
+    var duplicateModules = OptionsByModule
+      .Union(other.OptionsByModule)
+      .GroupBy(p => p.Key)
+      .Where(g => g.Count() > 1)
+      .Select(g => g.Key)
+      .ToList();
+    if (duplicateModules.Any()) {
+      var messagePrefix = $"cannot load {filePath}";
+      foreach (var duplicateModule in duplicateModules) {
+        reporter.Error(MessageSource.Project, origin,
+          $"{messagePrefix}: module {duplicateModule} already appears in another translation record");
+      }
+      return;
+    }
+
+    OptionsByModule = OptionsByModule.Union(other.OptionsByModule).ToDictionary(p => p.Key, p => p.Value);
+  }
+
+  private static readonly Dictionary<Option, OptionCompatibility.OptionCheck> OptionChecks = new();
+
+  public static void RegisterLibraryChecks(IDictionary<Option, OptionCompatibility.OptionCheck> checks) {
+    foreach (var (option, check) in checks) {
+      OptionChecks.Add(option, check);
+    }
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyCore/Pipeline/NoExecutableBackend.cs b/Source/DafnyCore/Pipeline/NoExecutableBackend.cs
index 4d610e7c850..569c4019268 100644
--- a/Source/DafnyCore/Pipeline/NoExecutableBackend.cs
+++ b/Source/DafnyCore/Pipeline/NoExecutableBackend.cs
@@ -22,7 +22,7 @@ public class NoExecutableBackend : IExecutableBackend {
   public override bool SupportsInMemoryCompilation => throw new NotSupportedException();
   public override string ModuleSeparator => ".";
 
-  public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
+  public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
     throw new NotSupportedException();
   }
 
diff --git a/Source/DafnyCore/Plugins/IExecutableBackend.cs b/Source/DafnyCore/Plugins/IExecutableBackend.cs
index 4cbd363e6bf..9a0e88266df 100644
--- a/Source/DafnyCore/Plugins/IExecutableBackend.cs
+++ b/Source/DafnyCore/Plugins/IExecutableBackend.cs
@@ -9,6 +9,7 @@
 using System.Linq;
 using System.Threading.Tasks;
 using DafnyCore;
+using DafnyCore.Options;
 using Microsoft.Dafny.Compilers;
 
 namespace Microsoft.Dafny.Plugins;
@@ -140,7 +141,7 @@ public abstract class IExecutableBackend {
   /// <param name="sourceDirectory">Name of the directory to delete.</param>
   public virtual void CleanSourceDirectory(string sourceDirectory) { }
 
-  public abstract void Compile(Program dafnyProgram, ConcreteSyntaxTree output);
+  public abstract void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output);
 
   /// <summary>
   /// Emits a call to <c>mainMethod</c> as the program's entry point, if such an explicit call is
@@ -190,12 +191,27 @@ public abstract class IExecutableBackend {
   public static readonly Option<string> OuterModule =
     new("--outer-module", "Nest all code in this module. Can be used to customize generated code. Use dots as separators (foo.baz.zoo) for deeper nesting. The first specified module will be the outermost one.");
 
-  public virtual IEnumerable<string> GetOuterModules() {
-    return Options.Get(OuterModule)?.Split(".") ?? Enumerable.Empty<string>();
-  }
+  public static readonly Option<IList<FileInfo>> TranslationRecords = new("--translation-record",
+    @"
+A translation record file for previously translated Dafny code. Can be specified multiple times. See https://dafny.org/dafny/DafnyRef/DafnyRef#sec-dtr-files for details.".TrimStart()) {
+  };
+
+  public static readonly Option<FileInfo> TranslationRecordOutput = new("--translation-record-output",
+    @"
+Where to output the translation record file. Defaults to the output directory. See https://dafny.org/dafny/DafnyRef/DafnyRef#sec-dtr-files for details.".TrimStart()) {
+  };
 
   static IExecutableBackend() {
-    DooFile.RegisterNoChecksNeeded(OuterModule);
+    DooFile.RegisterNoChecksNeeded(
+      OuterModule,
+      TranslationRecords,
+      TranslationRecordOutput
+      );
+    TranslationRecord.RegisterLibraryChecks(
+      new Dictionary<Option, OptionCompatibility.OptionCheck> {
+        { OuterModule, OptionCompatibility.NoOpOptionCheck },
+      }
+    );
   }
 
   public virtual Command GetCommand() {
diff --git a/Source/DafnyDriver/Commands/TranslateCommand.cs b/Source/DafnyDriver/Commands/TranslateCommand.cs
index ed88de6db3c..0bac685a930 100644
--- a/Source/DafnyDriver/Commands/TranslateCommand.cs
+++ b/Source/DafnyDriver/Commands/TranslateCommand.cs
@@ -16,7 +16,8 @@ static class TranslateCommand {
       CommonOptionBag.Output,
       IExecutableBackend.OuterModule,
       CommonOptionBag.IncludeRuntimeOption,
-      RunAllTestsMainMethod.IncludeTestRunner
+      RunAllTestsMainMethod.IncludeTestRunner,
+      IExecutableBackend.TranslationRecordOutput
     }.Concat(DafnyCommands.TranslationOptions).
       Concat(DafnyCommands.ConsoleOutputOptions).
       Concat(DafnyCommands.ResolverOptions);
diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs
index 02c9fa99971..ac382132f96 100644
--- a/Source/DafnyDriver/Commands/VerifyCommand.cs
+++ b/Source/DafnyDriver/Commands/VerifyCommand.cs
@@ -15,6 +15,8 @@ namespace Microsoft.Dafny;
 public static class VerifyCommand {
 
   static VerifyCommand() {
+    // Note these don't need checks because they are only "dafny verify" options;
+    // they can't be specified when building a doo file.
     DooFile.RegisterNoChecksNeeded(FilterSymbol);
     DooFile.RegisterNoChecksNeeded(FilterPosition);
   }
diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
index d60cd636f86..7ccb87601a6 100644
--- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
+++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
@@ -23,6 +23,7 @@
 using Microsoft.Boogie;
 using Bpl = Microsoft.Boogie;
 using System.Diagnostics;
+using DafnyCore.Options;
 using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.Plugins;
 using VC;
@@ -335,6 +336,7 @@ public class SynchronousCliCompilation : IDisposable {
       if (dafnyProgram != null && options.ExtractCounterexample && exitValue == ExitValue.VERIFICATION_ERROR) {
         PrintCounterexample(options);
       }
+
       return exitValue;
     }
 
@@ -582,11 +584,11 @@ private record TargetPaths(string Directory, string Filename) {
         outputWriter.WriteLine("Wrote textual form of target program to {0}", relativeTarget);
       }
 
-      foreach (var entry in otherFiles) {
-        var filename = entry.Key;
-        WriteFile(Path.Join(paths.SourceDirectory, filename), entry.Value);
+      foreach (var (filename, value) in otherFiles) {
+        var absoluteFilename = Path.IsPathRooted(filename) ? filename : Path.Join(paths.SourceDirectory, filename);
+        WriteFile(absoluteFilename, value);
         if (options.Verbose) {
-          outputWriter.WriteLine("Additional target code written to {0}", NormalizeRelativeFilename(Path.Join(paths.RelativeDirectory, filename)));
+          outputWriter.WriteLine("Additional output written to {0}", NormalizeRelativeFilename(Path.Join(paths.RelativeDirectory, filename)));
         }
       }
     }
@@ -667,7 +669,9 @@ private record TargetPaths(string Directory, string Filename) {
       var otherFiles = new Dictionary<string, string>();
       {
         var output = new ConcreteSyntaxTree();
-        await DafnyMain.LargeStackFactory.StartNew(() => compiler.Compile(dafnyProgram, output));
+
+        await DafnyMain.LargeStackFactory.StartNew(() => compiler.Compile(dafnyProgram, dafnyProgramName, output));
+
         var writerOptions = new WriterState();
         var targetProgramTextWriter = new StringWriter();
         var files = new Queue<FileSyntax>();
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy.expect
index ce6eb176e3d..e6db659bdd6 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy.expect
@@ -5,97 +5,102 @@ hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to CompileAndThenRun.js
+Additional output written to CompileAndThenRun-js.dtr
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to CompileAndThenRun-go/src/CompileAndThenRun.go
-Additional target code written to CompileAndThenRun-go/src/dafny/dafny.go
-Additional target code written to CompileAndThenRun-go/src/dafny/dafnyFromDafny.go
-Additional target code written to CompileAndThenRun-go/src/System_/System_.go
+Additional output written to CompileAndThenRun-go/src/CompileAndThenRun-go.dtr
+Additional output written to CompileAndThenRun-go/src/dafny/dafny.go
+Additional output written to CompileAndThenRun-go/src/dafny/dafnyFromDafny.go
+Additional output written to CompileAndThenRun-go/src/System_/System_.go
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to CompileAndThenRun-java/CompileAndThenRun.java
-Additional target code written to CompileAndThenRun-java/dafny/Array.java
-Additional target code written to CompileAndThenRun-java/dafny/BigOrdinal.java
-Additional target code written to CompileAndThenRun-java/dafny/BigRational.java
-Additional target code written to CompileAndThenRun-java/dafny/CodePoint.java
-Additional target code written to CompileAndThenRun-java/dafny/DafnyEuclidean.java
-Additional target code written to CompileAndThenRun-java/dafny/DafnyHaltException.java
-Additional target code written to CompileAndThenRun-java/dafny/DafnyMap.java
-Additional target code written to CompileAndThenRun-java/dafny/DafnyMultiset.java
-Additional target code written to CompileAndThenRun-java/dafny/DafnySequence.java
-Additional target code written to CompileAndThenRun-java/dafny/DafnySet.java
-Additional target code written to CompileAndThenRun-java/dafny/Helpers.java
-Additional target code written to CompileAndThenRun-java/dafny/TypeDescriptor.java
-Additional target code written to CompileAndThenRun-java/dafny/Array1.java
-Additional target code written to CompileAndThenRun-java/dafny/Array10.java
-Additional target code written to CompileAndThenRun-java/dafny/Array11.java
-Additional target code written to CompileAndThenRun-java/dafny/Array12.java
-Additional target code written to CompileAndThenRun-java/dafny/Array13.java
-Additional target code written to CompileAndThenRun-java/dafny/Array14.java
-Additional target code written to CompileAndThenRun-java/dafny/Array15.java
-Additional target code written to CompileAndThenRun-java/dafny/Array16.java
-Additional target code written to CompileAndThenRun-java/dafny/Array2.java
-Additional target code written to CompileAndThenRun-java/dafny/Array3.java
-Additional target code written to CompileAndThenRun-java/dafny/Array4.java
-Additional target code written to CompileAndThenRun-java/dafny/Array5.java
-Additional target code written to CompileAndThenRun-java/dafny/Array6.java
-Additional target code written to CompileAndThenRun-java/dafny/Array7.java
-Additional target code written to CompileAndThenRun-java/dafny/Array8.java
-Additional target code written to CompileAndThenRun-java/dafny/Array9.java
-Additional target code written to CompileAndThenRun-java/dafny/Function0.java
-Additional target code written to CompileAndThenRun-java/dafny/Function1.java
-Additional target code written to CompileAndThenRun-java/dafny/Function10.java
-Additional target code written to CompileAndThenRun-java/dafny/Function11.java
-Additional target code written to CompileAndThenRun-java/dafny/Function12.java
-Additional target code written to CompileAndThenRun-java/dafny/Function13.java
-Additional target code written to CompileAndThenRun-java/dafny/Function14.java
-Additional target code written to CompileAndThenRun-java/dafny/Function15.java
-Additional target code written to CompileAndThenRun-java/dafny/Function16.java
-Additional target code written to CompileAndThenRun-java/dafny/Function2.java
-Additional target code written to CompileAndThenRun-java/dafny/Function3.java
-Additional target code written to CompileAndThenRun-java/dafny/Function4.java
-Additional target code written to CompileAndThenRun-java/dafny/Function5.java
-Additional target code written to CompileAndThenRun-java/dafny/Function6.java
-Additional target code written to CompileAndThenRun-java/dafny/Function7.java
-Additional target code written to CompileAndThenRun-java/dafny/Function8.java
-Additional target code written to CompileAndThenRun-java/dafny/Function9.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple0.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple1.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple10.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple11.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple12.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple13.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple14.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple15.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple16.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple17.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple18.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple19.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple2.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple20.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple3.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple4.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple5.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple6.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple7.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple8.java
-Additional target code written to CompileAndThenRun-java/dafny/Tuple9.java
-Additional target code written to CompileAndThenRun-java/_System/nat.java
-Additional target code written to CompileAndThenRun-java/_System/__default.java
+Additional output written to CompileAndThenRun-java/CompileAndThenRun-java.dtr
+Additional output written to CompileAndThenRun-java/dafny/Array.java
+Additional output written to CompileAndThenRun-java/dafny/BigOrdinal.java
+Additional output written to CompileAndThenRun-java/dafny/BigRational.java
+Additional output written to CompileAndThenRun-java/dafny/CodePoint.java
+Additional output written to CompileAndThenRun-java/dafny/DafnyEuclidean.java
+Additional output written to CompileAndThenRun-java/dafny/DafnyHaltException.java
+Additional output written to CompileAndThenRun-java/dafny/DafnyMap.java
+Additional output written to CompileAndThenRun-java/dafny/DafnyMultiset.java
+Additional output written to CompileAndThenRun-java/dafny/DafnySequence.java
+Additional output written to CompileAndThenRun-java/dafny/DafnySet.java
+Additional output written to CompileAndThenRun-java/dafny/Helpers.java
+Additional output written to CompileAndThenRun-java/dafny/TypeDescriptor.java
+Additional output written to CompileAndThenRun-java/dafny/Array1.java
+Additional output written to CompileAndThenRun-java/dafny/Array10.java
+Additional output written to CompileAndThenRun-java/dafny/Array11.java
+Additional output written to CompileAndThenRun-java/dafny/Array12.java
+Additional output written to CompileAndThenRun-java/dafny/Array13.java
+Additional output written to CompileAndThenRun-java/dafny/Array14.java
+Additional output written to CompileAndThenRun-java/dafny/Array15.java
+Additional output written to CompileAndThenRun-java/dafny/Array16.java
+Additional output written to CompileAndThenRun-java/dafny/Array2.java
+Additional output written to CompileAndThenRun-java/dafny/Array3.java
+Additional output written to CompileAndThenRun-java/dafny/Array4.java
+Additional output written to CompileAndThenRun-java/dafny/Array5.java
+Additional output written to CompileAndThenRun-java/dafny/Array6.java
+Additional output written to CompileAndThenRun-java/dafny/Array7.java
+Additional output written to CompileAndThenRun-java/dafny/Array8.java
+Additional output written to CompileAndThenRun-java/dafny/Array9.java
+Additional output written to CompileAndThenRun-java/dafny/Function0.java
+Additional output written to CompileAndThenRun-java/dafny/Function1.java
+Additional output written to CompileAndThenRun-java/dafny/Function10.java
+Additional output written to CompileAndThenRun-java/dafny/Function11.java
+Additional output written to CompileAndThenRun-java/dafny/Function12.java
+Additional output written to CompileAndThenRun-java/dafny/Function13.java
+Additional output written to CompileAndThenRun-java/dafny/Function14.java
+Additional output written to CompileAndThenRun-java/dafny/Function15.java
+Additional output written to CompileAndThenRun-java/dafny/Function16.java
+Additional output written to CompileAndThenRun-java/dafny/Function2.java
+Additional output written to CompileAndThenRun-java/dafny/Function3.java
+Additional output written to CompileAndThenRun-java/dafny/Function4.java
+Additional output written to CompileAndThenRun-java/dafny/Function5.java
+Additional output written to CompileAndThenRun-java/dafny/Function6.java
+Additional output written to CompileAndThenRun-java/dafny/Function7.java
+Additional output written to CompileAndThenRun-java/dafny/Function8.java
+Additional output written to CompileAndThenRun-java/dafny/Function9.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple0.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple1.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple10.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple11.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple12.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple13.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple14.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple15.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple16.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple17.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple18.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple19.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple2.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple20.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple3.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple4.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple5.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple6.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple7.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple8.java
+Additional output written to CompileAndThenRun-java/dafny/Tuple9.java
+Additional output written to CompileAndThenRun-java/_System/nat.java
+Additional output written to CompileAndThenRun-java/_System/__default.java
 Wrote executable jar CompileAndThenRun.jar
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to CompileAndThenRun.cpp
-Additional target code written to CompileAndThenRun.h
-Additional target code written to DafnyRuntime.h
+Additional output written to CompileAndThenRun-cpp.dtr
+Additional output written to CompileAndThenRun.h
+Additional output written to DafnyRuntime.h
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to CompileAndThenRun-py/__main__.py
-Additional target code written to CompileAndThenRun-py/System_.py
-Additional target code written to CompileAndThenRun-py/_dafny.py
-Additional target code written to CompileAndThenRun-py/module_.py
+Additional output written to CompileAndThenRun-py/CompileAndThenRun-py.dtr
+Additional output written to CompileAndThenRun-py/System_.py
+Additional output written to CompileAndThenRun-py/_dafny.py
+Additional output written to CompileAndThenRun-py/module_.py
 hello, Dafny
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy.expect
index 6a44bc98d33..9a175e6acda 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy.expect
@@ -12,83 +12,85 @@ hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to JustRun-go/src/JustRun.go
-Additional target code written to JustRun-go/src/dafny/dafny.go
-Additional target code written to JustRun-go/src/dafny/dafnyFromDafny.go
-Additional target code written to JustRun-go/src/System_/System_.go
+Additional output written to JustRun-go/src/JustRun-go.dtr
+Additional output written to JustRun-go/src/dafny/dafny.go
+Additional output written to JustRun-go/src/dafny/dafnyFromDafny.go
+Additional output written to JustRun-go/src/System_/System_.go
 Running...
 
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to JustRun-java/JustRun.java
-Additional target code written to JustRun-java/dafny/Array.java
-Additional target code written to JustRun-java/dafny/BigOrdinal.java
-Additional target code written to JustRun-java/dafny/BigRational.java
-Additional target code written to JustRun-java/dafny/CodePoint.java
-Additional target code written to JustRun-java/dafny/DafnyEuclidean.java
-Additional target code written to JustRun-java/dafny/DafnyHaltException.java
-Additional target code written to JustRun-java/dafny/DafnyMap.java
-Additional target code written to JustRun-java/dafny/DafnyMultiset.java
-Additional target code written to JustRun-java/dafny/DafnySequence.java
-Additional target code written to JustRun-java/dafny/DafnySet.java
-Additional target code written to JustRun-java/dafny/Helpers.java
-Additional target code written to JustRun-java/dafny/TypeDescriptor.java
-Additional target code written to JustRun-java/dafny/Array1.java
-Additional target code written to JustRun-java/dafny/Array10.java
-Additional target code written to JustRun-java/dafny/Array11.java
-Additional target code written to JustRun-java/dafny/Array12.java
-Additional target code written to JustRun-java/dafny/Array13.java
-Additional target code written to JustRun-java/dafny/Array14.java
-Additional target code written to JustRun-java/dafny/Array15.java
-Additional target code written to JustRun-java/dafny/Array16.java
-Additional target code written to JustRun-java/dafny/Array2.java
-Additional target code written to JustRun-java/dafny/Array3.java
-Additional target code written to JustRun-java/dafny/Array4.java
-Additional target code written to JustRun-java/dafny/Array5.java
-Additional target code written to JustRun-java/dafny/Array6.java
-Additional target code written to JustRun-java/dafny/Array7.java
-Additional target code written to JustRun-java/dafny/Array8.java
-Additional target code written to JustRun-java/dafny/Array9.java
-Additional target code written to JustRun-java/dafny/Function0.java
-Additional target code written to JustRun-java/dafny/Function1.java
-Additional target code written to JustRun-java/dafny/Function10.java
-Additional target code written to JustRun-java/dafny/Function11.java
-Additional target code written to JustRun-java/dafny/Function12.java
-Additional target code written to JustRun-java/dafny/Function13.java
-Additional target code written to JustRun-java/dafny/Function14.java
-Additional target code written to JustRun-java/dafny/Function15.java
-Additional target code written to JustRun-java/dafny/Function16.java
-Additional target code written to JustRun-java/dafny/Function2.java
-Additional target code written to JustRun-java/dafny/Function3.java
-Additional target code written to JustRun-java/dafny/Function4.java
-Additional target code written to JustRun-java/dafny/Function5.java
-Additional target code written to JustRun-java/dafny/Function6.java
-Additional target code written to JustRun-java/dafny/Function7.java
-Additional target code written to JustRun-java/dafny/Function8.java
-Additional target code written to JustRun-java/dafny/Function9.java
-Additional target code written to JustRun-java/dafny/Tuple0.java
-Additional target code written to JustRun-java/dafny/Tuple1.java
-Additional target code written to JustRun-java/dafny/Tuple10.java
-Additional target code written to JustRun-java/dafny/Tuple11.java
-Additional target code written to JustRun-java/dafny/Tuple12.java
-Additional target code written to JustRun-java/dafny/Tuple13.java
-Additional target code written to JustRun-java/dafny/Tuple14.java
-Additional target code written to JustRun-java/dafny/Tuple15.java
-Additional target code written to JustRun-java/dafny/Tuple16.java
-Additional target code written to JustRun-java/dafny/Tuple17.java
-Additional target code written to JustRun-java/dafny/Tuple18.java
-Additional target code written to JustRun-java/dafny/Tuple19.java
-Additional target code written to JustRun-java/dafny/Tuple2.java
-Additional target code written to JustRun-java/dafny/Tuple20.java
-Additional target code written to JustRun-java/dafny/Tuple3.java
-Additional target code written to JustRun-java/dafny/Tuple4.java
-Additional target code written to JustRun-java/dafny/Tuple5.java
-Additional target code written to JustRun-java/dafny/Tuple6.java
-Additional target code written to JustRun-java/dafny/Tuple7.java
-Additional target code written to JustRun-java/dafny/Tuple8.java
-Additional target code written to JustRun-java/dafny/Tuple9.java
-Additional target code written to JustRun-java/_System/nat.java
-Additional target code written to JustRun-java/_System/__default.java
+Additional output written to JustRun-java/JustRun-java.dtr
+Additional output written to JustRun-java/dafny/Array.java
+Additional output written to JustRun-java/dafny/BigOrdinal.java
+Additional output written to JustRun-java/dafny/BigRational.java
+Additional output written to JustRun-java/dafny/CodePoint.java
+Additional output written to JustRun-java/dafny/DafnyEuclidean.java
+Additional output written to JustRun-java/dafny/DafnyHaltException.java
+Additional output written to JustRun-java/dafny/DafnyMap.java
+Additional output written to JustRun-java/dafny/DafnyMultiset.java
+Additional output written to JustRun-java/dafny/DafnySequence.java
+Additional output written to JustRun-java/dafny/DafnySet.java
+Additional output written to JustRun-java/dafny/Helpers.java
+Additional output written to JustRun-java/dafny/TypeDescriptor.java
+Additional output written to JustRun-java/dafny/Array1.java
+Additional output written to JustRun-java/dafny/Array10.java
+Additional output written to JustRun-java/dafny/Array11.java
+Additional output written to JustRun-java/dafny/Array12.java
+Additional output written to JustRun-java/dafny/Array13.java
+Additional output written to JustRun-java/dafny/Array14.java
+Additional output written to JustRun-java/dafny/Array15.java
+Additional output written to JustRun-java/dafny/Array16.java
+Additional output written to JustRun-java/dafny/Array2.java
+Additional output written to JustRun-java/dafny/Array3.java
+Additional output written to JustRun-java/dafny/Array4.java
+Additional output written to JustRun-java/dafny/Array5.java
+Additional output written to JustRun-java/dafny/Array6.java
+Additional output written to JustRun-java/dafny/Array7.java
+Additional output written to JustRun-java/dafny/Array8.java
+Additional output written to JustRun-java/dafny/Array9.java
+Additional output written to JustRun-java/dafny/Function0.java
+Additional output written to JustRun-java/dafny/Function1.java
+Additional output written to JustRun-java/dafny/Function10.java
+Additional output written to JustRun-java/dafny/Function11.java
+Additional output written to JustRun-java/dafny/Function12.java
+Additional output written to JustRun-java/dafny/Function13.java
+Additional output written to JustRun-java/dafny/Function14.java
+Additional output written to JustRun-java/dafny/Function15.java
+Additional output written to JustRun-java/dafny/Function16.java
+Additional output written to JustRun-java/dafny/Function2.java
+Additional output written to JustRun-java/dafny/Function3.java
+Additional output written to JustRun-java/dafny/Function4.java
+Additional output written to JustRun-java/dafny/Function5.java
+Additional output written to JustRun-java/dafny/Function6.java
+Additional output written to JustRun-java/dafny/Function7.java
+Additional output written to JustRun-java/dafny/Function8.java
+Additional output written to JustRun-java/dafny/Function9.java
+Additional output written to JustRun-java/dafny/Tuple0.java
+Additional output written to JustRun-java/dafny/Tuple1.java
+Additional output written to JustRun-java/dafny/Tuple10.java
+Additional output written to JustRun-java/dafny/Tuple11.java
+Additional output written to JustRun-java/dafny/Tuple12.java
+Additional output written to JustRun-java/dafny/Tuple13.java
+Additional output written to JustRun-java/dafny/Tuple14.java
+Additional output written to JustRun-java/dafny/Tuple15.java
+Additional output written to JustRun-java/dafny/Tuple16.java
+Additional output written to JustRun-java/dafny/Tuple17.java
+Additional output written to JustRun-java/dafny/Tuple18.java
+Additional output written to JustRun-java/dafny/Tuple19.java
+Additional output written to JustRun-java/dafny/Tuple2.java
+Additional output written to JustRun-java/dafny/Tuple20.java
+Additional output written to JustRun-java/dafny/Tuple3.java
+Additional output written to JustRun-java/dafny/Tuple4.java
+Additional output written to JustRun-java/dafny/Tuple5.java
+Additional output written to JustRun-java/dafny/Tuple6.java
+Additional output written to JustRun-java/dafny/Tuple7.java
+Additional output written to JustRun-java/dafny/Tuple8.java
+Additional output written to JustRun-java/dafny/Tuple9.java
+Additional output written to JustRun-java/_System/nat.java
+Additional output written to JustRun-java/_System/__default.java
 Wrote executable jar JustRun.jar
 Running...
 
@@ -96,17 +98,19 @@ hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to JustRun.cpp
-Additional target code written to JustRun.h
-Additional target code written to DafnyRuntime.h
+Additional output written to JustRun-cpp.dtr
+Additional output written to JustRun.h
+Additional output written to DafnyRuntime.h
 Running...
 
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to JustRun-py/__main__.py
-Additional target code written to JustRun-py/System_.py
-Additional target code written to JustRun-py/_dafny.py
-Additional target code written to JustRun-py/module_.py
+Additional output written to JustRun-py/JustRun-py.dtr
+Additional output written to JustRun-py/System_.py
+Additional output written to JustRun-py/_dafny.py
+Additional output written to JustRun-py/module_.py
 Running...
 
 hello, Dafny
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy.expect
index 5fb4df5cbc3..4c7fa20c8bb 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy.expect
@@ -1,100 +1,106 @@
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to ManualCompile.cs
+Additional output written to ManualCompile-cs.dtr
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to ManualCompile.js
+Additional output written to ManualCompile-js.dtr
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to ManualCompile-go/src/ManualCompile.go
-Additional target code written to ManualCompile-go/src/dafny/dafny.go
-Additional target code written to ManualCompile-go/src/dafny/dafnyFromDafny.go
-Additional target code written to ManualCompile-go/src/System_/System_.go
+Additional output written to ManualCompile-go/src/ManualCompile-go.dtr
+Additional output written to ManualCompile-go/src/dafny/dafny.go
+Additional output written to ManualCompile-go/src/dafny/dafnyFromDafny.go
+Additional output written to ManualCompile-go/src/System_/System_.go
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to ManualCompile-java/ManualCompile.java
-Additional target code written to ManualCompile-java/dafny/Array.java
-Additional target code written to ManualCompile-java/dafny/BigOrdinal.java
-Additional target code written to ManualCompile-java/dafny/BigRational.java
-Additional target code written to ManualCompile-java/dafny/CodePoint.java
-Additional target code written to ManualCompile-java/dafny/DafnyEuclidean.java
-Additional target code written to ManualCompile-java/dafny/DafnyHaltException.java
-Additional target code written to ManualCompile-java/dafny/DafnyMap.java
-Additional target code written to ManualCompile-java/dafny/DafnyMultiset.java
-Additional target code written to ManualCompile-java/dafny/DafnySequence.java
-Additional target code written to ManualCompile-java/dafny/DafnySet.java
-Additional target code written to ManualCompile-java/dafny/Helpers.java
-Additional target code written to ManualCompile-java/dafny/TypeDescriptor.java
-Additional target code written to ManualCompile-java/dafny/Array1.java
-Additional target code written to ManualCompile-java/dafny/Array10.java
-Additional target code written to ManualCompile-java/dafny/Array11.java
-Additional target code written to ManualCompile-java/dafny/Array12.java
-Additional target code written to ManualCompile-java/dafny/Array13.java
-Additional target code written to ManualCompile-java/dafny/Array14.java
-Additional target code written to ManualCompile-java/dafny/Array15.java
-Additional target code written to ManualCompile-java/dafny/Array16.java
-Additional target code written to ManualCompile-java/dafny/Array2.java
-Additional target code written to ManualCompile-java/dafny/Array3.java
-Additional target code written to ManualCompile-java/dafny/Array4.java
-Additional target code written to ManualCompile-java/dafny/Array5.java
-Additional target code written to ManualCompile-java/dafny/Array6.java
-Additional target code written to ManualCompile-java/dafny/Array7.java
-Additional target code written to ManualCompile-java/dafny/Array8.java
-Additional target code written to ManualCompile-java/dafny/Array9.java
-Additional target code written to ManualCompile-java/dafny/Function0.java
-Additional target code written to ManualCompile-java/dafny/Function1.java
-Additional target code written to ManualCompile-java/dafny/Function10.java
-Additional target code written to ManualCompile-java/dafny/Function11.java
-Additional target code written to ManualCompile-java/dafny/Function12.java
-Additional target code written to ManualCompile-java/dafny/Function13.java
-Additional target code written to ManualCompile-java/dafny/Function14.java
-Additional target code written to ManualCompile-java/dafny/Function15.java
-Additional target code written to ManualCompile-java/dafny/Function16.java
-Additional target code written to ManualCompile-java/dafny/Function2.java
-Additional target code written to ManualCompile-java/dafny/Function3.java
-Additional target code written to ManualCompile-java/dafny/Function4.java
-Additional target code written to ManualCompile-java/dafny/Function5.java
-Additional target code written to ManualCompile-java/dafny/Function6.java
-Additional target code written to ManualCompile-java/dafny/Function7.java
-Additional target code written to ManualCompile-java/dafny/Function8.java
-Additional target code written to ManualCompile-java/dafny/Function9.java
-Additional target code written to ManualCompile-java/dafny/Tuple0.java
-Additional target code written to ManualCompile-java/dafny/Tuple1.java
-Additional target code written to ManualCompile-java/dafny/Tuple10.java
-Additional target code written to ManualCompile-java/dafny/Tuple11.java
-Additional target code written to ManualCompile-java/dafny/Tuple12.java
-Additional target code written to ManualCompile-java/dafny/Tuple13.java
-Additional target code written to ManualCompile-java/dafny/Tuple14.java
-Additional target code written to ManualCompile-java/dafny/Tuple15.java
-Additional target code written to ManualCompile-java/dafny/Tuple16.java
-Additional target code written to ManualCompile-java/dafny/Tuple17.java
-Additional target code written to ManualCompile-java/dafny/Tuple18.java
-Additional target code written to ManualCompile-java/dafny/Tuple19.java
-Additional target code written to ManualCompile-java/dafny/Tuple2.java
-Additional target code written to ManualCompile-java/dafny/Tuple20.java
-Additional target code written to ManualCompile-java/dafny/Tuple3.java
-Additional target code written to ManualCompile-java/dafny/Tuple4.java
-Additional target code written to ManualCompile-java/dafny/Tuple5.java
-Additional target code written to ManualCompile-java/dafny/Tuple6.java
-Additional target code written to ManualCompile-java/dafny/Tuple7.java
-Additional target code written to ManualCompile-java/dafny/Tuple8.java
-Additional target code written to ManualCompile-java/dafny/Tuple9.java
-Additional target code written to ManualCompile-java/_System/nat.java
-Additional target code written to ManualCompile-java/_System/__default.java
+Additional output written to ManualCompile-java/ManualCompile-java.dtr
+Additional output written to ManualCompile-java/dafny/Array.java
+Additional output written to ManualCompile-java/dafny/BigOrdinal.java
+Additional output written to ManualCompile-java/dafny/BigRational.java
+Additional output written to ManualCompile-java/dafny/CodePoint.java
+Additional output written to ManualCompile-java/dafny/DafnyEuclidean.java
+Additional output written to ManualCompile-java/dafny/DafnyHaltException.java
+Additional output written to ManualCompile-java/dafny/DafnyMap.java
+Additional output written to ManualCompile-java/dafny/DafnyMultiset.java
+Additional output written to ManualCompile-java/dafny/DafnySequence.java
+Additional output written to ManualCompile-java/dafny/DafnySet.java
+Additional output written to ManualCompile-java/dafny/Helpers.java
+Additional output written to ManualCompile-java/dafny/TypeDescriptor.java
+Additional output written to ManualCompile-java/dafny/Array1.java
+Additional output written to ManualCompile-java/dafny/Array10.java
+Additional output written to ManualCompile-java/dafny/Array11.java
+Additional output written to ManualCompile-java/dafny/Array12.java
+Additional output written to ManualCompile-java/dafny/Array13.java
+Additional output written to ManualCompile-java/dafny/Array14.java
+Additional output written to ManualCompile-java/dafny/Array15.java
+Additional output written to ManualCompile-java/dafny/Array16.java
+Additional output written to ManualCompile-java/dafny/Array2.java
+Additional output written to ManualCompile-java/dafny/Array3.java
+Additional output written to ManualCompile-java/dafny/Array4.java
+Additional output written to ManualCompile-java/dafny/Array5.java
+Additional output written to ManualCompile-java/dafny/Array6.java
+Additional output written to ManualCompile-java/dafny/Array7.java
+Additional output written to ManualCompile-java/dafny/Array8.java
+Additional output written to ManualCompile-java/dafny/Array9.java
+Additional output written to ManualCompile-java/dafny/Function0.java
+Additional output written to ManualCompile-java/dafny/Function1.java
+Additional output written to ManualCompile-java/dafny/Function10.java
+Additional output written to ManualCompile-java/dafny/Function11.java
+Additional output written to ManualCompile-java/dafny/Function12.java
+Additional output written to ManualCompile-java/dafny/Function13.java
+Additional output written to ManualCompile-java/dafny/Function14.java
+Additional output written to ManualCompile-java/dafny/Function15.java
+Additional output written to ManualCompile-java/dafny/Function16.java
+Additional output written to ManualCompile-java/dafny/Function2.java
+Additional output written to ManualCompile-java/dafny/Function3.java
+Additional output written to ManualCompile-java/dafny/Function4.java
+Additional output written to ManualCompile-java/dafny/Function5.java
+Additional output written to ManualCompile-java/dafny/Function6.java
+Additional output written to ManualCompile-java/dafny/Function7.java
+Additional output written to ManualCompile-java/dafny/Function8.java
+Additional output written to ManualCompile-java/dafny/Function9.java
+Additional output written to ManualCompile-java/dafny/Tuple0.java
+Additional output written to ManualCompile-java/dafny/Tuple1.java
+Additional output written to ManualCompile-java/dafny/Tuple10.java
+Additional output written to ManualCompile-java/dafny/Tuple11.java
+Additional output written to ManualCompile-java/dafny/Tuple12.java
+Additional output written to ManualCompile-java/dafny/Tuple13.java
+Additional output written to ManualCompile-java/dafny/Tuple14.java
+Additional output written to ManualCompile-java/dafny/Tuple15.java
+Additional output written to ManualCompile-java/dafny/Tuple16.java
+Additional output written to ManualCompile-java/dafny/Tuple17.java
+Additional output written to ManualCompile-java/dafny/Tuple18.java
+Additional output written to ManualCompile-java/dafny/Tuple19.java
+Additional output written to ManualCompile-java/dafny/Tuple2.java
+Additional output written to ManualCompile-java/dafny/Tuple20.java
+Additional output written to ManualCompile-java/dafny/Tuple3.java
+Additional output written to ManualCompile-java/dafny/Tuple4.java
+Additional output written to ManualCompile-java/dafny/Tuple5.java
+Additional output written to ManualCompile-java/dafny/Tuple6.java
+Additional output written to ManualCompile-java/dafny/Tuple7.java
+Additional output written to ManualCompile-java/dafny/Tuple8.java
+Additional output written to ManualCompile-java/dafny/Tuple9.java
+Additional output written to ManualCompile-java/_System/nat.java
+Additional output written to ManualCompile-java/_System/__default.java
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to ManualCompile.cpp
-Additional target code written to ManualCompile.h
-Additional target code written to DafnyRuntime.h
+Additional output written to ManualCompile-cpp.dtr
+Additional output written to ManualCompile.h
+Additional output written to DafnyRuntime.h
 hello, Dafny
 
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to ManualCompile-py/__main__.py
-Additional target code written to ManualCompile-py/System_.py
-Additional target code written to ManualCompile-py/_dafny.py
-Additional target code written to ManualCompile-py/module_.py
+Additional output written to ManualCompile-py/ManualCompile-py.dtr
+Additional output written to ManualCompile-py/System_.py
+Additional output written to ManualCompile-py/_dafny.py
+Additional output written to ManualCompile-py/module_.py
 hello, Dafny
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/Bar.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/Bar.dtr
new file mode 100644
index 00000000000..7b20ab49a16
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/Bar.dtr
@@ -0,0 +1,4 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module.Bar]
+outer-module = "Barfle"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dfy
new file mode 100644
index 00000000000..db41fbca6f8
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dfy
@@ -0,0 +1,11 @@
+
+// RUN: %baredafny translate cs %args %s --translation-record %S/Bar.dtr &> %t
+// RUN: %exits-with 3 %baredafny translate cs %args %s --translation-record %S/Foo.dtr &>> %t
+// RUN: %exits-with 3 %baredafny translate cs %args %s --translation-record %S/Bar.dtr --translation-record %S/Bar.dtr &>> %t
+// RUN: %diff "%s.expect" "%t"
+
+module Foo {
+  method Main() {
+
+  }
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dfy.expect
new file mode 100644
index 00000000000..851dfdf855e
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dfy.expect
@@ -0,0 +1,10 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+
+Dafny program verifier finished with 0 verified, 0 errors
+CLI: Error: cannot load Foo.dtr: it contains translation metadata for the module Foo, which is in scope for translation in the current program
+Translation was aborted because errors were found
+
+Dafny program verifier finished with 0 verified, 0 errors
+CLI: Error: cannot load Bar.dtr: module Bar already appears in another translation record
+Translation was aborted because errors were found
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dtr
new file mode 100644
index 00000000000..7f97382f971
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/DuplicateModules.dtr
@@ -0,0 +1,3 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module.Foo]
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/Foo.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/Foo.dtr
new file mode 100644
index 00000000000..8f9d162d979
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/Foo.dtr
@@ -0,0 +1,4 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module.Foo]
+outer-module = "Arfle"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy
new file mode 100644
index 00000000000..161262c4116
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy
@@ -0,0 +1,7 @@
+// RUN: %exits-with 3 %baredafny translate cs %args %s --translation-record %S/NoGood.dtr &> %t
+// RUN: %exits-with 3 %baredafny translate cs %args %s --translation-record %S/WrongDafnyVersion.dtr &>> %t
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect
new file mode 100644
index 00000000000..c31783a3968
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect
@@ -0,0 +1,8 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+CLI: Error: malformed dtr file NoGood.dtr
+Translation was aborted because errors were found
+
+Dafny program verifier finished with 0 verified, 0 errors
+CLI: Error: cannot load WrongDafnyVersion.dtr: it was built with Dafny 10.6.0.0, which cannot be used by Dafny 4.6.0.0
+Translation was aborted because errors were found
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/NoGood.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/NoGood.dtr
new file mode 100644
index 00000000000..4925891c42b
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/NoGood.dtr
@@ -0,0 +1 @@
+Not even close
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/WrongDafnyVersion.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/WrongDafnyVersion.dtr
new file mode 100644
index 00000000000..c2c53d3def8
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/WrongDafnyVersion.dtr
@@ -0,0 +1,2 @@
+file_format_version = "1.0"
+dafny_version = "10.6.0.0"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo.dfy
index e9392e5809e..2022c41ae75 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo.dfy
@@ -2,19 +2,19 @@
 
 // C#
 
-// RUN: %baredafny translate cs %args --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy
+// RUN: %baredafny translate cs %args --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy --outer-module TestProducer.DafnyInternal
 // RUN: dotnet build %S/Inputs/producer
 
-// RUN: %baredafny translate cs %args --output=%S/consumer/usesTimesTwo --library=%S/Inputs/producer/timesTwo.dfy %s
+// RUN: %baredafny translate cs %args --output=%S/consumer/usesTimesTwo --library=%S/Inputs/producer/timesTwo.dfy %s --translation-record %S/Inputs/producer/timesTwo-cs.dtr
 
 // RUN: dotnet run --project %S/consumer > "%t"
 
 // Java
 
-// RUN: %baredafny translate java --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy
+// RUN: %baredafny translate java --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy --outer-module testproducer.dafnyinternal --translation-record-output %S/timesTwo-customName.dtr
 // RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java %S/Inputs/producer/timesTwo-java/timesTwo.java %S/Inputs/producer/timesTwo-java/*/*.java
 
-// RUN: %baredafny translate java --output=%S/consumer/usesTimesTwo --library=%S/Inputs/producer/timesTwo.dfy %s
+// RUN: %baredafny translate java --output=%S/consumer/usesTimesTwo --library=%S/Inputs/producer/timesTwo.dfy %s --translation-record %S/timesTwo-customName.dtr
 // RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java%{pathsep}%S/consumer/usesTimesTwo-java %S/consumer/usesTimesTwo-java/usesTimesTwo.java %S/consumer/usesTimesTwo-java/*/*.java
 
 // RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java%{pathsep}%S/consumer/usesTimesTwo-java usesTimesTwo >> "%t"
diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md
index 6ad372623c0..1aecb219f38 100644
--- a/docs/DafnyRef/UserGuide.md
+++ b/docs/DafnyRef/UserGuide.md
@@ -96,7 +96,7 @@ These commands are described in [Section 13.6.1](#sec-dafny-commands).
 [^fn-duplicate-files]: Files may be included more than once or both included and listed on the command line. Duplicate inclusions are detected and each file processed only once.
 For the purpose of detecting duplicates, file names are considered equal if they have the same absolute path, compared as case-sensitive strings (regardless of whether the underlying file-system is case sensitive).  Using symbolic links may make the same file have a different absolute path; this will generally cause duplicate declaration errors.
 
-### 13.3.1. Dafny Build Artifacts: the Library Backend and .doo Files {#sec-doo-files}
+### 13.3.1. Dafny Verification Artifacts: the Library Backend and .doo Files {#sec-doo-files}
 
 As of Dafny 4.1, `dafny` now supports outputting a single file containing
 a fully-verified program along with metadata about how it was verified.
@@ -131,6 +131,33 @@ The exact file format is internal and may evolve over time to support additional
 
 Note that the library backend only supports the [newer command-style CLI interface](#sec-dafny-commands).
 
+### 13.3.2. Dafny Translation Artifacts: .dtr Files {#sec-dtr-files}
+
+Some options, such as `--outer-module` or `--optimize-erasable-datatype-wrapper`,
+affect what target language code the same Dafny code is translated to.
+In order to translate Dafny libaries separately from their consuming codebases,
+the translation process for consuming code needs to be aware
+of what options were used when translating the library.
+
+For example, if a library defines a `Foo()` function in an `A` module,
+but `--outer-module org.coolstuff.foolibrary.dafnyinternal` is specified when translating the library to Java,
+then a reference to `A.Foo()` in a consuming Dafny project
+needs to be translated to `org.coolstuff.foolibrary.dafnyinternal.A.Foo()`,
+independently of what value of `--outer-module` is used for the consuming project.
+
+To meet this need,
+`dafny translate` also outputs a `<program-name>-<target id>.dtr` Dafny Translation Record file.
+Like `.doo` files, `.dtr` files record all the relevant options that were used,
+in this case relevant to translation rather than verification.
+These files can be provided to future calls to `dafny translate` using the `--translation-record` option,
+in order to provide the details of how various libraries provided with the `--library` flag were translated.
+
+Currently `--outer-module` is the only option recorded in `.dtr` files,
+but more relevant options will be added in the future.
+A later version of Dafny will also require `.dtr` files that cover all modules
+that are defined in `--library` options,
+to support checking that all relevant options are compatible.
+
 ## 13.4. Dafny Standard Libraries
 
 As of Dafny 4.4, the `dafny` tool includes standard libraries that any Dafny code base can depend on.
diff --git a/docs/dev/news/5346.feat b/docs/dev/news/5346.feat
new file mode 100644
index 00000000000..92fed52249d
--- /dev/null
+++ b/docs/dev/news/5346.feat
@@ -0,0 +1,4 @@
+Add support for "translation records", which record the options used when translating library code.
+* `--translation-record` - Provides a `.dtr` file from a previous translation of library code. Can be specified multiple times.
+* `--translation-record-output` - Customizes where to write the translation record for the current translation. Defaults to the output directory.
+Providing translation records is necessary to handle options such as `--outer-module` that affect how code is translated.