feat: Proof refactoring suggestions

Source/DafnyCore/DafnyConsolePrinter.cs

@@ -21,19 +21,21 @@ public class DafnyConsolePrinter : ConsolePrinter {
   private DafnyOptions options;
 
   public record ImplementationLogEntry(string Name, Boogie.IToken Tok);
-  public record VCResultLogEntry(
+  public record AssertCmdPartialCopy(Boogie.IToken Tok, string Description, string Id);
+  public record VerificationRunResultPartialCopy(
     int VCNum,
     DateTime StartTime,
     TimeSpan RunTime,
     SolverOutcome Outcome,
-    List<(Boogie.IToken Tok, string Description)> Asserts,
+    List<AssertCmdPartialCopy> Asserts,
     IEnumerable<TrackedNodeComponent> CoveredElements,
+    IEnumerable<Axiom> AvailableAxioms,
     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 +45,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;

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -1,28 +1,36 @@
+using System;
 using System.Collections.Generic;
 using System.Linq;
 using DafnyCore.Verifier;
 using Microsoft.Boogie;
+using Microsoft.Dafny.Triggers;
 using VC;
 
 namespace Microsoft.Dafny;
 
 public record VerificationTaskResult(IVerificationTask Task, VerificationRunResult Result);
 
 public class ProofDependencyWarnings {
+  private static DafnyOptions options;
+  private static ErrorReporter reporter;
+  private static ProofDependencyManager manager;
 
 
-  public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerable<VerificationTaskResult> parts,
-    ErrorReporter reporter, ProofDependencyManager manager) {
+  public static void ReportSuspiciousDependencies(DafnyOptions dafnyOptions, IEnumerable<VerificationTaskResult> parts,
+    ErrorReporter reporter, ProofDependencyManager depManager) {
+    manager = depManager;
+    ProofDependencyWarnings.reporter = reporter;
+    options = dafnyOptions;
     foreach (var resultsForScope in parts.GroupBy(p => p.Task.ScopeId)) {
-      WarnAboutSuspiciousDependenciesForImplementation(options,
-        reporter,
-        manager,
-        resultsForScope.Key,
+      WarnAboutSuspiciousDependenciesForImplementation(resultsForScope.Key,
         resultsForScope.Select(p => p.Result).ToList());
     }
   }
 
-  public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) {
+  public static void WarnAboutSuspiciousDependenciesUsingStoredPartialResults(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) {
+    manager = depManager;
+    ProofDependencyWarnings.reporter = reporter;
+    options = dafnyOptions;
     var verificationResults = (dafnyOptions.Printer as DafnyConsolePrinter).VerificationResults.ToList();
     var orderedResults =
       verificationResults.OrderBy(vr =>
@@ -32,28 +40,68 @@ public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, Er
       if (result.Outcome != VcOutcome.Correct) {
         continue;
       }
-      Warn(dafnyOptions, reporter, depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements));
+      var unusedFunctions = UnusedFunctions(implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms));
+      WarnAboutSuspiciousDependencies(implementation.Name, result.VCResults, unusedFunctions);
     }
   }
 
-  public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter,
-    ProofDependencyManager depManager, string name,
+  public static void WarnAboutSuspiciousDependenciesForImplementation(string name,
     IReadOnlyList<VerificationRunResult> results) {
     if (results.Any(r => r.Outcome != SolverOutcome.Valid)) {
       return;
     }
+    var unusedFunctions = UnusedFunctions(name, results.SelectMany(r => r.CoveredElements), results.Select(DafnyConsolePrinter.DistillVCResult).SelectMany(r => r.AvailableAxioms));
+    WarnAboutSuspiciousDependencies(name, results.Select(DafnyConsolePrinter.DistillVCResult).ToList(), unusedFunctions);
+  }
+
+  private static List<Function> UnusedFunctions(string implementationName, IEnumerable<TrackedNodeComponent> coveredElements,
+    IEnumerable<Axiom> axioms) {
+    if (!((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[implementationName].Decl is Method)) {
+      return new List<Function>();
+    }
+
+    var unusedFunctions = new List<Function>();
+    if (manager.idsByMemberName[implementationName].Decl is not Method method) {
+      return unusedFunctions;
+    }
+
+    var usedFunctions = coveredElements.Select(manager.GetFullIdDependency).OfType<FunctionDefinitionDependency>()
+      .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b));
+
+    unusedFunctions = VisibleFunctions().Except(usedFunctions).ToList();
 
-    var coveredElements = results.SelectMany(r => r.CoveredElements);
+    return unusedFunctions;
 
-    Warn(dafnyOptions, reporter, depManager, name, coveredElements);
+    HashSet<Function> VisibleFunctions() {
+      var functions = new HashSet<Function>();
+
+      foreach (var visibleFunction in axioms.Select(GetFunctionFromAttributed).Where(f => f != null)) {
+        functions.Add(visibleFunction);
+      }
+
+      return functions;
+
+      Function GetFunctionFromAttributed(ICarriesAttributes construct) {
+        var values = construct.FindAllAttributes("id");
+        if (!values.Any()) {
+          return null;
+        }
+        var id = (string)values.Last().Params.First();
+        if (manager.ProofDependenciesById.TryGetValue(id, out var dep) && dep is FunctionDefinitionDependency fdd) {
+          return fdd.function;
+        }
+        return null;
+      }
+    }
   }
 
-  private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager,
-    string scopeName, IEnumerable<TrackedNodeComponent> coveredElements) {
-    var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(scopeName);
+  private static void WarnAboutSuspiciousDependencies(string scopeName,
+    IReadOnlyList<DafnyConsolePrinter.VerificationRunResultPartialCopy> assertCoverage, List<Function> unusedFunctions) {
+    var potentialDependencies = manager.GetPotentialDependenciesForDefinition(scopeName);
+    var coveredElements = assertCoverage.SelectMany(tp => tp.CoveredElements);
     var usedDependencies =
       coveredElements
-        .Select(depManager.GetFullIdDependency)
+        .Select(manager.GetFullIdDependency)
         .OrderBy(dep => dep.Range)
         .ThenBy(dep => dep.Description);
     var unusedDependencies =
@@ -63,9 +111,9 @@ private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, Proo
         .ThenBy(dep => dep.Description).ToList();
 
     foreach (var unusedDependency in unusedDependencies) {
-      if (dafnyOptions.Get(CommonOptionBag.WarnContradictoryAssumptions)) {
+      if (options.Get(CommonOptionBag.WarnContradictoryAssumptions) || options.Get(CommonOptionBag.AnalyseProofs)) {
         if (unusedDependency is ProofObligationDependency obligation) {
-          if (ShouldWarnVacuous(dafnyOptions, scopeName, obligation)) {
+          if (ShouldWarnVacuous(scopeName, obligation)) {
             var message = $"proved using contradictory assumptions: {obligation.Description}";
             if (obligation.ProofObligation is AssertStatementDescription) {
               message += ". (Use the `{:contradiction}` attribute on the `assert` statement to silence.)";
@@ -75,14 +123,14 @@ private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, Proo
         }
 
         if (unusedDependency is EnsuresDependency ensures) {
-          if (ShouldWarnVacuous(dafnyOptions, scopeName, ensures)) {
+          if (ShouldWarnVacuous(scopeName, ensures)) {
             reporter.Warning(MessageSource.Verifier, "", ensures.Range,
               $"ensures clause proved using contradictory assumptions");
           }
         }
       }
 
-      if (dafnyOptions.Get(CommonOptionBag.WarnRedundantAssumptions)) {
+      if (options.Get(CommonOptionBag.WarnRedundantAssumptions) || options.Get(CommonOptionBag.AnalyseProofs)) {
         if (unusedDependency is RequiresDependency requires) {
           reporter.Warning(MessageSource.Verifier, "", requires.Range, $"unnecessary requires clause");
         }
@@ -95,6 +143,106 @@ private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, Proo
         }
       }
     }
+
+    if ((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[scopeName].Decl is Method m) {
+      SuggestFunctionHiding(unusedFunctions, m);
+      SuggestByProofRefactoring(scopeName, assertCoverage.ToList());
+    }
+  }
+
+  private static void SuggestFunctionHiding(List<Function> unusedFunctions, Method m) {
+    if (unusedFunctions.Any()) {
+      reporter.Info(MessageSource.Verifier, m.Body.StartToken,
+        $"Consider hiding {(unusedFunctions.Count > 1 ? "these functions, which are" : "this function, which is")} unused by the proof: {unusedFunctions.Comma()}");
+    }
+  }
+
+  private static void SuggestByProofRefactoring(string scopeName,
+    IReadOnlyList<DafnyConsolePrinter.VerificationRunResultPartialCopy> verificationRunResults) {
+    foreach (var (dep, lAsserts) in ComputeAssertionsUsedByFact(scopeName, verificationRunResults)) {
+      var factIsOnlyUsedByOneAssertion = lAsserts.Count == 1;
+      if (!factIsOnlyUsedByOneAssertion) {
+        continue;
+      }
+
+      DafnyConsolePrinter.AssertCmdPartialCopy cmd = null;
+      foreach (var assert in lAsserts) {
+        cmd = assert;
+      }
+
+      manager.ProofDependenciesById.TryGetValue(cmd.Id, out var consumer);
+
+      if (consumer != null && (dep == consumer || consumer.Range.Intersects(dep.Range))) {
+        continue;
+      }
+
+      RangeToken range = null;
+      var factProvider = "";
+      var factConsumer = "";
+      var recommendation = "";
+      var completeInformation = true;
+
+      switch (dep) {
+        case AssumedProofObligationDependency:
+        case AssumptionDependency: {
+            range = dep.Range;
+            factProvider = "fact";
+            recommendation = "moving it into";
+            break;
+          }
+        case RequiresDependency: {
+            range = dep.Range;
+            factProvider = "requires clause";
+            recommendation = "labelling it and revealing it in";
+            break;
+          }
+        default: completeInformation = false; break;
+      }
+
+      switch (consumer) {
+        case CallDependency call: {
+            factConsumer = $"precondtion{(call.call.Method.Req.Count > 1 ? "s" : "")} of the method call {call.RangeString()}";
+            break;
+          }
+        case ProofObligationDependency { ProofObligation: AssertStatementDescription }: {
+            factConsumer = $"assertion {consumer.RangeString()}";
+            break;
+          }
+        default: completeInformation = false; break;
+      }
+
+      if (completeInformation) {
+        reporter.Info(MessageSource.Verifier, range,
+          $"This {factProvider} was only used to prove the {factConsumer}. Consider {recommendation} a by-proof.");
+      }
+    }
+  }
+
+  private static Dictionary<ProofDependency, HashSet<DafnyConsolePrinter.AssertCmdPartialCopy>>
+    ComputeAssertionsUsedByFact(string scopeName, IReadOnlyList<DafnyConsolePrinter.VerificationRunResultPartialCopy> vcResults) {
+    var assertionsUsedByFact = manager.GetPotentialDependenciesForDefinition(scopeName)
+      .Where(dep => dep is not EnsuresDependency)
+      .ToDictionary(dep => dep, _ => new HashSet<DafnyConsolePrinter.AssertCmdPartialCopy> { });
+
+    foreach (var (usedFacts, asserts) in vcResults.Select(r => (r.CoveredElements, r.Asserts))) {
+      foreach (var factReference in usedFacts) {
+        var factDependency = manager.GetFullIdDependency(factReference);
+        var excludedDependencies = factDependency is EnsuresDependency;
+        if (excludedDependencies) {
+          continue;
+        }
+
+        assertionsUsedByFact.TryAdd(factDependency, new HashSet<DafnyConsolePrinter.AssertCmdPartialCopy>());
+
+        bool NotSelfReferential(DafnyConsolePrinter.AssertCmdPartialCopy assert) =>
+           !manager.ProofDependenciesById.TryGetValue(assert.Id, out var assertDependency)
+                 || !(factDependency == assertDependency || factDependency is CallRequiresDependency req && req.call == assertDependency);
+
+        assertionsUsedByFact[factDependency].UnionWith(asserts.Where(NotSelfReferential));
+      }
+    }
+
+    return assertionsUsedByFact;
   }
 
   /// <summary>
@@ -107,10 +255,11 @@ private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, Proo
   /// to not generate vacuous proof goals, but that may be a difficult
   /// change to make.
   /// </summary>
+  /// <param name="verboseName"></param>
   /// <param name="dep">the dependency to examine</param>
   /// <returns>false to skip warning about the absence of this
   /// dependency, true otherwise</returns>
-  private static bool ShouldWarnVacuous(DafnyOptions options, string verboseName, ProofDependency dep) {
+  private static bool ShouldWarnVacuous(string verboseName, ProofDependency dep) {
     if (dep is ProofObligationDependency poDep) {
       // Dafny generates some assertions about definite assignment whose
       // proofs are always vacuous. Since these aren't written by Dafny

Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs

@@ -155,7 +155,7 @@ void AddWellformednessCheck(ConstantField decl) {
       Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null);
       Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null);
 
-      proofDependencies.SetCurrentDefinition(MethodVerboseName(decl.FullDafnyName, MethodTranslationKind.SpecWellformedness));
+      proofDependencies.SetCurrentDefinition(MethodVerboseName(decl.FullDafnyName, MethodTranslationKind.SpecWellformedness), null);
       if (!InVerificationScope(decl)) {
         // Checked in other file
         return;