feat: Proof refactoring suggestions

Source/DafnyCore/DafnyConsolePrinter.cs

@@ -26,8 +26,9 @@ public record VCResultLogEntry(
     DateTime StartTime,
     TimeSpan RunTime,
     SolverOutcome Outcome,
-    List<(Boogie.IToken Tok, string Description)> Asserts,
+    List<(Boogie.IToken Tok, string Description, string Id)> Asserts,
     IEnumerable<TrackedNodeComponent> CoveredElements,
+    IEnumerable<Axiom> AvailableAxioms,
     int ResourceCount);
   public record VerificationResultLogEntry(
     VcOutcome Outcome,
@@ -43,10 +44,18 @@ public static VerificationResultLogEntry DistillVerificationResult(Implementatio
       verificationResult.ResourceCount, verificationResult.RunResults.Select(DistillVCResult).ToList(), verificationResult.Errors);
   }
 
-  private static VCResultLogEntry DistillVCResult(VerificationRunResult r) {
+  public 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);
+        r.Asserts.Select(a => (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()) {
+        throw new ArgumentException($"No dependency ID in assertion");
+      }
+      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.1" />
       <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;
@@ -32,7 +33,9 @@ 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 assertCoverage = result.VCResults.Select(e => (e.CoveredElements, new HashSet<(Boogie.IToken Tok, string Description, string Id)>(e.Asserts))).ToList();
+      var unusedFunctions = UnusedFunctions(depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms));
+      Warn(dafnyOptions, reporter, depManager, implementation.Name, assertCoverage, unusedFunctions);
     }
   }
 
@@ -42,15 +45,93 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions
     if (results.Any(r => r.Outcome != SolverOutcome.Valid)) {
       return;
     }
+    var distilled = results.Select(r => (r.CoveredElements, DafnyConsolePrinter.DistillVCResult(r))).ToList();
+    var asserts = distilled.Select(tp => (tp.CoveredElements, new HashSet<(Boogie.IToken Tok, string Description, string Id)>(tp.Item2.Asserts))).ToList();
+    var unusedFunctions = UnusedFunctions(depManager, name, distilled.SelectMany(r => r.CoveredElements), distilled.SelectMany(r => r.Item2.AvailableAxioms));
+    Warn(dafnyOptions, reporter, depManager, name, asserts, unusedFunctions);
+  }
+
+  private static List<Function> UnusedFunctions(ProofDependencyManager depManager, string name, IEnumerable<TrackedNodeComponent> coveredElements, IEnumerable<Axiom> axioms) {
+    var unusedFunctions = new List<Function>();
+    if (depManager.idsByMemberName[name].Decl is Method m) {
+      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();
+
+      HashSet<Function> ReferencedFunctions(Method method) {
+        var fCEsinM = method.Body.AllSubExpressions(false, false).OfType<FunctionCallExpr>();
+        var fToDeps = new Dictionary<Function, IEnumerable<Function>>();
+
+        foreach (var fce in fCEsinM) {
+          var fun = fce.Function;
+          if (!fToDeps.ContainsKey(fun)) {
+            fToDeps[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 fToDeps) {
+          hashSet.Add(f);
+          hashSet.UnionWith(deps);
+        }
+
+        return hashSet;
+      }
+
+      HashSet<Function> HiddenFunctions(HashSet<Function> functions) {
+        var hiddenFunctions = new HashSet<Function>(functions);
 
-    var coveredElements = results.SelectMany(r => r.CoveredElements);
+        foreach (var visibleFunction in axioms.Select(GetFunctionFromAttributed).Where(f => f != null)) {
+          hiddenFunctions.Remove(visibleFunction);
+        }
+
+        return hiddenFunctions;
 
-    Warn(dafnyOptions, reporter, depManager, name, coveredElements);
+        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) {
+    string scopeName, List<(IEnumerable<TrackedNodeComponent> CoveredElements, HashSet<(Boogie.IToken Tok, string Description, string Id)> Asserts)> assertCoverage, List<Function> unusedFunctions) {
     var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(scopeName);
+    var coveredElements = assertCoverage.SelectMany(tp => tp.CoveredElements);
     var usedDependencies =
       coveredElements
         .Select(depManager.GetFullIdDependency)
@@ -95,6 +176,98 @@ private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, Proo
         }
       }
     }
+
+    if (dafnyOptions.Get(CommonOptionBag.SuggestProofRefactoring) && depManager.idsByMemberName[scopeName].Decl is Method m) {
+      // Function hiding suggestion
+      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()}");
+      }
+
+      SuggestByProofRefactoring(reporter, depManager, scopeName, assertCoverage);
+    }
+  }
+
+  private static void SuggestByProofRefactoring(ErrorReporter reporter, ProofDependencyManager depManager,
+    string scopeName, List<(IEnumerable<TrackedNodeComponent> CoveredElements, HashSet<(Boogie.IToken Tok, string Description, string Id)> Asserts)> assertCoverage) {
+    var dependencyTracker = depManager.GetPotentialDependenciesForDefinition(scopeName).Where(dep => dep is not EnsuresDependency).ToDictionary(dep => dep, _ => new HashSet<(Boogie.IToken Tok, string Description, string Id)> { });
+
+    foreach (var (usedFacts, asserts) in assertCoverage) {
+      foreach (var fact in usedFacts) {
+        var dep = depManager.GetFullIdDependency(fact);
+        _ = dep is not EnsuresDependency &&
+            dependencyTracker.TryAdd(dep, new HashSet<(Boogie.IToken Tok, string Description, string Id)>());
+        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 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;
   }
 
 

Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs

@@ -65,7 +65,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) {
       Contract.Ensures(currentModule == null && codeContext == null);
       Contract.Ensures(Contract.Result<Bpl.Procedure>() != null);
 
-      proofDependencies.SetCurrentDefinition(MethodVerboseName(iter.FullDafnyName, kind));
+      proofDependencies.SetCurrentDefinition(MethodVerboseName(iter.FullDafnyName, kind), iter);
       currentModule = iter.EnclosingModuleDefinition;
       codeContext = iter;
 
@@ -138,7 +138,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) {
       Contract.Requires(currentModule == null && codeContext == null);
       Contract.Ensures(currentModule == null && codeContext == null);
 
-      proofDependencies.SetCurrentDefinition(proc.VerboseName);
+      proofDependencies.SetCurrentDefinition(proc.VerboseName, iter);
       currentModule = iter.EnclosingModuleDefinition;
       codeContext = iter;
 
@@ -271,7 +271,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) {
       Contract.Requires(currentModule == null && codeContext == null && yieldCountVariable == null && _tmpIEs.Count == 0);
       Contract.Ensures(currentModule == null && codeContext == null && yieldCountVariable == null && _tmpIEs.Count == 0);
 
-      proofDependencies.SetCurrentDefinition(proc.VerboseName);
+      proofDependencies.SetCurrentDefinition(proc.VerboseName, iter);
       currentModule = iter.EnclosingModuleDefinition;
       codeContext = iter;