feat: Proof refactoring suggestions

.github/workflows/doc-tests.yml

@@ -37,7 +37,7 @@ jobs:
         path: dafny
     - name: Load Z3
       run: |
-        sudo apt-get install -qq libarchive-tools
+        sudo apt-get update && sudo apt-get install -qq libarchive-tools
         mkdir -p dafny/Binaries/z3/bin
         wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
         mv z3-* dafny/Binaries/z3/bin/

.github/workflows/integration-tests-reusable.yml

@@ -142,7 +142,7 @@ jobs:
     - name: Load Z3
       if: "!inputs.all_platforms"
       run: |
-        sudo apt-get install -qq libarchive-tools
+        sudo apt-get update && sudo apt-get install -qq libarchive-tools
         mkdir -p dafny/Binaries/z3/bin
         wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
         mv z3-4.12.1 dafny/Binaries/z3/bin/

Source/DafnyCore/DafnyConsolePrinter.cs

@@ -9,6 +9,17 @@
 
 namespace Microsoft.Dafny;
 
+public record AssertCmdPartialCopy(Boogie.IToken Tok, string Description, string Id);
+public record VerificationRunResultPartialCopy(
+  int VCNum,
+  DateTime StartTime,
+  TimeSpan RunTime,
+  SolverOutcome Outcome,
+  List<AssertCmdPartialCopy> Asserts,
+  IEnumerable<TrackedNodeComponent> CoveredElements,
+  IEnumerable<Axiom> AvailableAxioms,
+  int ResourceCount);
+
 public class DafnyConsolePrinter : ConsolePrinter {
   public new DafnyOptions Options {
     get => options;
@@ -21,19 +32,11 @@ public class DafnyConsolePrinter : ConsolePrinter {
   private DafnyOptions options;
 
   public record ImplementationLogEntry(string Name, Boogie.IToken Tok);
-  public record VCResultLogEntry(
-    int VCNum,
-    DateTime StartTime,
-    TimeSpan RunTime,
-    SolverOutcome Outcome,
-    List<(Boogie.IToken Tok, string Description)> Asserts,
-    IEnumerable<TrackedNodeComponent> CoveredElements,
-    int ResourceCount);
   public record VerificationResultLogEntry(
     VcOutcome Outcome,
     TimeSpan RunTime,
     int ResourceCount,
-    List<VCResultLogEntry> VCResults,
+    List<VerificationRunResultPartialCopy> VCResults,
     List<Counterexample> Counterexamples);
   public record ConsoleLogEntry(ImplementationLogEntry Implementation, VerificationResultLogEntry Result);
 
@@ -43,10 +46,18 @@ public static VerificationResultLogEntry DistillVerificationResult(Implementatio
       verificationResult.ResourceCount, verificationResult.RunResults.Select(DistillVCResult).ToList(), verificationResult.Errors);
   }
 
-  private static VCResultLogEntry DistillVCResult(VerificationRunResult r) {
-    return new VCResultLogEntry(r.VcNum, r.StartTime, r.RunTime, r.Outcome,
-        r.Asserts.Select(a => (a.tok, a.Description.SuccessDescription)).ToList(), r.CoveredElements,
-        r.ResourceCount);
+  public static VerificationRunResultPartialCopy DistillVCResult(VerificationRunResult r) {
+    return new VerificationRunResultPartialCopy(r.VcNum, r.StartTime, r.RunTime, r.Outcome,
+        r.Asserts.Select(a => new AssertCmdPartialCopy(a.tok, a.Description.SuccessDescription, GetId(a))).ToList(), r.CoveredElements,
+        r.DeclarationsAfterPruning.OfType<Axiom>(), r.ResourceCount);
+
+    string GetId(ICarriesAttributes construct) {
+      var values = construct.FindAllAttributes("id");
+      if (!values.Any()) {
+        return "";
+      }
+      return (string)values.Last().Params.First();
+    }
   }
 
   public ConcurrentBag<ConsoleLogEntry> VerificationResults { get; } = new();

Source/DafnyCore/DafnyCore.csproj

@@ -34,7 +34,7 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.5" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.3.3" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -288,6 +288,15 @@ May produce spurious warnings.
 May produce spurious warnings.") {
     IsHidden = true
   };
+  public static readonly Option<bool> SuggestProofRefactoring = new("--suggest-proof-refactoring", @"
+(experimental) Emits suggestions for moving assertions into by-proofs and hiding unused function definitions.
+May produce spurious suggestions. Use with --show-hints on the CLI.") {
+    IsHidden = true
+  };
+  public static readonly Option<bool> AnalyseProofs = new("--analyse-proofs", @"
+(experimental) Implies --warn-contradictory-assumptions, --warn-redundant-assumptions, and --suggest-proof-refactoring") {
+    IsHidden = true
+  };
   public static readonly Option<string> VerificationCoverageReport = new("--verification-coverage-report",
     "Emit verification coverage report to a given directory, in the same format as a test coverage report.") {
     ArgumentHelpName = "directory"
@@ -461,6 +470,7 @@ statements in implementation methods. It also disables anything
 
     DafnyOptions.RegisterLegacyUi(WarnContradictoryAssumptions, DafnyOptions.ParseImplicitEnable, "Verification options", "warnContradictoryAssumptions");
     DafnyOptions.RegisterLegacyUi(WarnRedundantAssumptions, DafnyOptions.ParseImplicitEnable, "Verification options", "warnRedundantAssumptions");
+    DafnyOptions.RegisterLegacyUi(SuggestProofRefactoring, DafnyOptions.ParseImplicitEnable, "Verification options", "suggestProofRefactoring");
 
     void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps, DafnyOptions options) {
       if (ps.ConfirmArgumentCount(1)) {
@@ -514,6 +524,9 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
     DafnyOptions.RegisterLegacyBinding(WarnRedundantAssumptions, (options, value) => {
       if (value) { options.TrackVerificationCoverage = true; }
     });
+    DafnyOptions.RegisterLegacyBinding(SuggestProofRefactoring, (options, value) => {
+      if (value) { options.TrackVerificationCoverage = true; }
+    });
 
     DafnyOptions.RegisterLegacyBinding(Target, (options, value) => { options.CompilerName = value; });
 
@@ -621,6 +634,8 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
     OptionRegistry.RegisterOption(InternalIncludeRuntimeOptionForExecution, OptionScope.Cli);
     OptionRegistry.RegisterOption(WarnContradictoryAssumptions, OptionScope.Module);
     OptionRegistry.RegisterOption(WarnRedundantAssumptions, OptionScope.Module);
+    OptionRegistry.RegisterOption(SuggestProofRefactoring, OptionScope.Module);
+    OptionRegistry.RegisterOption(AnalyseProofs, OptionScope.Module);
     OptionRegistry.RegisterOption(VerificationCoverageReport, OptionScope.Cli);
     OptionRegistry.RegisterOption(NoTimeStampForCoverageReport, OptionScope.Cli);
     OptionRegistry.RegisterOption(DefaultFunctionOpacity, OptionScope.Module);

Source/DafnyCore/Options/DafnyCommands.cs

@@ -41,6 +41,8 @@ static DafnyCommands() {
     CommonOptionBag.DefaultFunctionOpacity,
     CommonOptionBag.WarnContradictoryAssumptions,
     CommonOptionBag.WarnRedundantAssumptions,
+    CommonOptionBag.SuggestProofRefactoring,
+    CommonOptionBag.AnalyseProofs,
     CommonOptionBag.NoTimeStampForCoverageReport,
     CommonOptionBag.VerificationCoverageReport,
     CommonOptionBag.ExtractCounterexample,

Source/DafnyCore/Pipeline/Compilation.cs

@@ -3,7 +3,6 @@
 using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
-using System.Collections.Immutable;
 using System.IO;
 using System.Linq;
 using System.Reactive;