feat: Proof refactoring suggestions #5812
Conversation
There was a problem hiding this comment.
I think warnings that are turned off by default are anti-patterns. Turning them off by default implies that we do not recommend using this warning.
I think in this case the opposite is true: we do recommend using this warning! The only thing is that it drags down verification to do the analysis that enables it. I think it would be better to have a single option --analyse-proofs that turns on TrackVerificationCoverage and automatically all the warnings/suggestion that are associated with it.
We could then still have options that allow turning off some of the warning associated with --analyse-proofs, but I would be OK with not having those.
| var factProvider = ""; | ||
| var factConsumer = ""; | ||
| var recomendation = ""; | ||
| var completeInformation = true; |
There was a problem hiding this comment.
Can you say more about this completeInformation variable? What's an example program in which it is false?
There was a problem hiding this comment.
It's when the dependency isn't of a type that we know how to handle.
There was a problem hiding this comment.
Do you have an example?
There was a problem hiding this comment.
FunctionDefinitionDependency? No point in moving that.
Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect
Outdated
Show resolved
Hide resolved
Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy.expect
Outdated
Show resolved
Hide resolved
Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy
Outdated
Show resolved
Hide resolved
Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy
Outdated
Show resolved
Hide resolved
Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy
Outdated
Show resolved
Hide resolved
Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy
Outdated
Show resolved
Hide resolved
Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofRefactorings.dfy
Outdated
Show resolved
Hide resolved
| 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) |
There was a problem hiding this comment.
What's the .Where for? Could you add a clarifying comment? If a fact is used to prove an ensures clause and an assertion (could be make sure we have a test for this?), then we should not recommend moving that fact to a by block right?
There was a problem hiding this comment.
It's the other way around, proving something using on ensures doesn't make much sense, so we exclude it.
There was a problem hiding this comment.
Is it a performance optimization then? Wouldn't assertionsProvenUsingFact[ensuresDependency].Any() always be false?
Also, do you do the same optimization on line 222?
There was a problem hiding this comment.
Isn't this convenient... dafny-lang/blog#37 (comment)
There was a problem hiding this comment.
It's an example of an ensures dependency being the singular dependency. Didn't you ask for that?
| 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) |
There was a problem hiding this comment.
Is it a performance optimization then? Wouldn't assertionsProvenUsingFact[ensuresDependency].Any() always be false?
Also, do you do the same optimization on line 222?
| continue; | ||
| } | ||
|
|
||
| assertionsProvenUsingFact.TryAdd(factDependency, new HashSet<AssertCmdPartialCopy>()); |
There was a problem hiding this comment.
Didn't you already fill this dictionary with values? Why do you sometimes need to add another value?
There was a problem hiding this comment.
Yes, but not with the function definition axioms
| var factProvider = ""; | ||
| var factConsumer = ""; | ||
| var recomendation = ""; | ||
| var completeInformation = true; |
There was a problem hiding this comment.
Do you have an example?
|
|
||
| bool IsNotSelfReferential(AssertCmdPartialCopy assert) => | ||
| !manager.ProofDependenciesById.TryGetValue(assert.Id, out var assertDependency) | ||
| || !(factDependency == assertDependency || factDependency is CallRequiresDependency req && req.call == assertDependency); |
There was a problem hiding this comment.
factDependency == assertDependency when does that occur? Is this for things like a loop invariant?
There was a problem hiding this comment.
We don't count the assertion itself when considering what was needed to proof it.
There was a problem hiding this comment.
I guess that this is not about a case where an expression is both an assumptions and assertion, as is the case with invariants, but this is about an assertion always being used in the VC in which it occurs.
| IsHidden = true | ||
| }; | ||
| public static readonly Option<bool> AnalyzeProofs = new("--analyze-proofs", @" | ||
| Uses data from to prover to suggest ways to refine the proof: |
There was a problem hiding this comment.
Maybe indicate that this only works for proofs that verify? Use data from verified proofs
I find refine ambiguous. I would go for to provide additional warnings and suggestions, or to warn about potential specification bugs and suggest changes to improve verification performance
Our documentation uses verifier, solver and prover. I'd use the term verifier (referring to the whole verification pipeline) or SMT solver in externally facing documentation.
Warning if any assertions are proved
I don't think that's valid English. I would use an imperative sentence Warn if ..
|
Approved and set to auto-merge. I had one remaining comment about documentation. If you want to address that we can do it in a follow-up. |
Description
This PR adds suggestions for proof refactoring in two scenarios. It suggests moving single-use assertions into by-proofs and hiding functions that are unused for the proof of a method.
How has this been tested?
New tests
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.