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,11 @@ 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<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 +466,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 +520,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 +630,7 @@ 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(VerificationCoverageReport, OptionScope.Cli);
     OptionRegistry.RegisterOption(NoTimeStampForCoverageReport, OptionScope.Cli);
     OptionRegistry.RegisterOption(DefaultFunctionOpacity, OptionScope.Module);

Source/DafnyCore/Options/DafnyCommands.cs

@@ -41,6 +41,7 @@ static DafnyCommands() {
     CommonOptionBag.DefaultFunctionOpacity,
     CommonOptionBag.WarnContradictoryAssumptions,
     CommonOptionBag.WarnRedundantAssumptions,
+    CommonOptionBag.SuggestProofRefactoring,
     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

@@ -2,6 +2,7 @@
 using System.Linq;
 using DafnyCore.Verifier;
 using Microsoft.Boogie;
+using Microsoft.Dafny.Triggers;
 using VC;
 
 namespace Microsoft.Dafny;
@@ -22,7 +23,7 @@ public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerabl
     }
   }
 
-  public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) {
+  public static void WarnAboutSuspiciousDependenciesUsingStoredPartialResults(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) {
     var verificationResults = (dafnyOptions.Printer as DafnyConsolePrinter).VerificationResults.ToList();
     var orderedResults =
       verificationResults.OrderBy(vr =>
@@ -32,7 +33,8 @@ 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(dafnyOptions, depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms));
+      WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, implementation.Name, result.VCResults, unusedFunctions);
     }
   }
 
@@ -42,15 +44,98 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions
     if (results.Any(r => r.Outcome != SolverOutcome.Valid)) {
       return;
     }
+    var unusedFunctions = UnusedFunctions(dafnyOptions, depManager, name, results.SelectMany(r => r.CoveredElements), results.Select(DafnyConsolePrinter.DistillVCResult).SelectMany(r => r.AvailableAxioms));
+    WarnAboutSuspiciousDependencies(dafnyOptions, reporter, depManager, name, results.Select(DafnyConsolePrinter.DistillVCResult).ToList(), unusedFunctions);
+  }
+
+  private static List<Function> UnusedFunctions(DafnyOptions dafnyOptions, ProofDependencyManager depManager, string name, IEnumerable<TrackedNodeComponent> coveredElements, IEnumerable<Axiom> axioms) {
+    if (!(dafnyOptions.Get(CommonOptionBag.SuggestProofRefactoring) && depManager.idsByMemberName[name].Decl is Method)) {
+      return new List<Function>();
+    }
+
+    var unusedFunctions = new List<Function>();
+    if (depManager.idsByMemberName[name].Decl is not Method m) {
+      return unusedFunctions;
+    }
+
+    var referencedFunctions = ReferencedFunctions(m);
+
+    var hiddenFunctions = HiddenFunctions(referencedFunctions);
+
+    var usedFunctions = coveredElements.Select(depManager.GetFullIdDependency).OfType<FunctionDefinitionDependency>()
+      .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b));
+
+    unusedFunctions = referencedFunctions.Except(hiddenFunctions).Except(usedFunctions).ToList();
 
-    var coveredElements = results.SelectMany(r => r.CoveredElements);
+    HashSet<Function> HiddenFunctions(HashSet<Function> functions) {
+      var hiddenFunctions = new HashSet<Function>(functions);
 
-    Warn(dafnyOptions, reporter, depManager, name, coveredElements);
+      foreach (var visibleFunction in axioms.Select(GetFunctionFromAttributed).Where(f => f != null)) {
+        hiddenFunctions.Remove(visibleFunction);
+      }
+
+      return hiddenFunctions;
+
+      Function GetFunctionFromAttributed(ICarriesAttributes construct) {
+        var values = construct.FindAllAttributes("id");
+        if (!values.Any()) {
+          return null;
+        }
+        var id = (string)values.Last().Params.First();
+        if (depManager.ProofDependenciesById.TryGetValue(id, out var dep) && dep is FunctionDefinitionDependency fdd) {
+          return fdd.function;
+        }
+        return null;
+      }
+    }
+    return unusedFunctions;
   }
 
-  private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager,
-    string scopeName, IEnumerable<TrackedNodeComponent> coveredElements) {
+  private static HashSet<Function> ReferencedFunctions(Method method) {
+    var functionCallsInMethod = method.Body != null ? method.Body.AllSubExpressions(false, false).OfType<FunctionCallExpr>() : new List<FunctionCallExpr>();
+    var functionDependants = new Dictionary<Function, IEnumerable<Function>>();
+
+    foreach (var fce in functionCallsInMethod) {
+      var fun = fce.Function;
+      if (!functionDependants.ContainsKey(fun)) {
+        functionDependants[fun] = Dependents(fun);
+      }
+
+      continue;
+
+      IEnumerable<Function> Dependents(Function fn) {
+        var queue = new Queue<Function>(new[] { fn });
+        var visited = new HashSet<Function>();
+        while (queue.Any()) {
+          var f = queue.Dequeue();
+          visited.Add(f);
+
+          f.SubExpressions.SelectMany(AllSubFunctions).Where(fn => !visited.Contains(fn)).ForEach(queue.Enqueue);
+          continue;
+
+          IEnumerable<Function> AllSubFunctions(Expression e) {
+            return e.SubExpressions.OfType<FunctionCallExpr>().Select(fce => fce.Function)
+              .Concat(e.SubExpressions.SelectMany(AllSubFunctions));
+          }
+        }
+        return visited.ToList();
+      }
+    }
+
+    var hashSet = new HashSet<Function>();
+    foreach (var (f, deps) in functionDependants) {
+      hashSet.Add(f);
+      hashSet.UnionWith(deps);
+    }
+
+    return hashSet;
+  }
+
+
+  private static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager,
+    string scopeName, IReadOnlyList<DafnyConsolePrinter.VerificationRunResultPartialCopy> assertCoverage, List<Function> unusedFunctions) {
     var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(scopeName);
+    var coveredElements = assertCoverage.SelectMany(tp => tp.CoveredElements);
     var usedDependencies =
       coveredElements
         .Select(depManager.GetFullIdDependency)
@@ -95,6 +180,101 @@ private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, Proo
         }
       }
     }
+
+    if (dafnyOptions.Get(CommonOptionBag.SuggestProofRefactoring) && depManager.idsByMemberName[scopeName].Decl is Method m) {
+      SuggestFunctionHiding(reporter, unusedFunctions, m);
+      SuggestByProofRefactoring(reporter, depManager, scopeName, assertCoverage.ToList());
+    }
+  }
+
+  private static void SuggestFunctionHiding(ErrorReporter reporter, 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(ErrorReporter reporter, ProofDependencyManager depManager,
+    string scopeName, IReadOnlyList<DafnyConsolePrinter.VerificationRunResultPartialCopy> vcResults) {
+    var dependencyTracker = depManager.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 fact in usedFacts) {
+        var dep = depManager.GetFullIdDependency(fact);
+        _ = dep is not EnsuresDependency &&
+            dependencyTracker.TryAdd(dep, new HashSet<DafnyConsolePrinter.AssertCmdPartialCopy>());
+        if (dependencyTracker.ContainsKey(dep)) {
+          dependencyTracker[dep].UnionWith(asserts);
+        }
+      }
+    }
+
+    foreach (var (dep, lAsserts) in dependencyTracker) {
+      foreach (var cmd in lAsserts) {
+        if (depManager.ProofDependenciesById.TryGetValue(cmd.Id, out var cmdDep)) {
+          if (dep == cmdDep || dep is CallRequiresDependency req && req.call == cmdDep) {
+            lAsserts.Remove(cmd);
+          }
+        }
+      }
+    }
+
+    foreach (var (dep, lAsserts) in dependencyTracker) {
+      if (lAsserts.Count != 1) {
+        continue;
+      }
+      var en = lAsserts.GetEnumerator();
+      if (!en.MoveNext()) {
+        continue;
+      }
+
+      var cmd = en.Current;
+      depManager.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 recomendation = "";
+      var completeInformation = true;
+
+      switch (dep) {
+        case AssumedProofObligationDependency:
+        case AssumptionDependency: {
+            range = dep.Range;
+            factProvider = "fact";
+            recomendation = "moving it into";
+            break;
+          }
+        case RequiresDependency: {
+            range = dep.Range;
+            factProvider = "requires clause";
+            recomendation = "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 {recomendation} a by-proof.");
+      }
+    }
   }
 
   /// <summary>

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;

Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs

@@ -22,7 +22,7 @@ public void Check(Function f) {
       Contract.Assert(generator.InVerificationScope(f));
 
       generator.proofDependencies.SetCurrentDefinition(MethodVerboseName(f.FullDafnyName,
-        MethodTranslationKind.SpecWellformedness));
+        MethodTranslationKind.SpecWellformedness), f);
       generator.currentModule = f.EnclosingClass.EnclosingModuleDefinition;
       generator.codeContext = f;
 

Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs

@@ -637,9 +637,16 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
     } else {
       comment += " (opaque)";
     }
-    return new Axiom(f.tok, BplImp(activate, ax), comment) {
+    var axe = new Axiom(f.tok, BplImp(activate, ax), comment) {
       CanHide = true
     };
+    if (proofDependencies == null) {
+      return axe;
+    }
+
+    proofDependencies.SetCurrentDefinition(f.FullSanitizedName, f);
+    proofDependencies.AddProofDependencyId(axe, f.tok, new FunctionDefinitionDependency(f));
+    return axe;
   }