Introduce aggressive pruning and the related 'uses' keyword for constants and functions

[keyboardDrummer]

Related Dafny issue: dafny-lang/dafny#1585

Introduce the aggressive pruning option /prune:2, which will remove any axioms that aren't reachable as a definition axiom. To prevent removing most axioms, the keyword uses is introduced that can be used to provide, for functions and constants, a definition axiom that only partially defines the definition, and it can be used to define multiple definition axioms. Here's an example:

const unique fourOrThree : int uses {
    axiom four == 4 || four == 3;
}

function returnsThree(x: int): int uses {
    axiom (forall x: int :: x != 0 ==> returnsThree(x) == 3);
    axiom (forall x: int :: x == 0 ==> returnsThree(x) == 3);
}

procedure validates()
  requires fourOrThree != 3
  ensures returnsThree(4) == 3;
  ensures fourOrThree == 4;
{
  
}

The uses keyword can also be used to handle situation where automatic pruning and exclude_dep would otherwise incorrectly remove an axiom.

An example is the following:

function {:exclude_dep} $Box<T>(T): Box;
function {:identity} {:exclude_dep} Lit<T>(x: T): T { x } uses {
  axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
}

Without the uses keyword, the axiom would be pruned since $Box and Lit are marked as {:exclude_dep}.

[MikaelMayer]

function returnsThree(x: int): bool uses {
    axiom (forall x: int :: returnsThree(x) == 3);
}

Did you mean function returnsThree(x: int):int ?

[fabiomadge]

Why don't we need !ExcludeDep(newIncoming) here?

[keyboardDrummer]

How you use it here?

[shazqadeer]

To prevent removing most axioms, the keyword uses is introduced that can be used to provide multiple definition axioms for functions and constants, like so:...

The sentence above in the PR description seems to suggest that it is possible to provide more than one axiom for each function or constant symbol. Yet, the code after the sentence does not contain any example of multiple axioms for a single symbol. Please clarify.

[keyboardDrummer]

@RustanLeino : I request your input here. This PR (and earlier PRs by your intern) are addressing an important problem. In the course of this work, several attributes and features are being added. Is it time to take a step back and rethink the approach?

Hey, I understand the apprehension towards this and related PRs. I think the problem could also be resolved at the SMT level.

Let me restate the problem: the Z3 solver can strongly change its behavior in terms of solve time and output of check-sat when making changes to the sent commands for which we wouldn't expect a change in behavior.

We're currently working around this problem by making sure that Dafny's verification pipeline, which includes Boogie, sends the exact same SMT commands to the Z3 solver when verifying two proofs that we can easily normalise to the same proof. The advantage of this approach, as opposed to changing the solver, is that it will work for any solver. A disadvantage is, I think, that we're more limited in detecting the equivalence between two proofs. Tackling this problem at the solver level might allow constant solver behavior for much larger classes of equivalent input.

[shazqadeer]

@keyboardDrummer: You are indeed addressing an important problem. Thank you for your efforts which will help all Boogie users.

Based on the PR description, I detect three players in this game: uses keyword, prune option, and exclude_dep attribute. Am I missing anything?

I would love to see one description of what a Boogie user could expect once this PR lands. If the description is compact, it should find its way into a comment into the code also.

[keyboardDrummer]

@keyboardDrummer: You are indeed addressing an important problem. Thank you for your efforts which will help all Boogie users.

Based on the PR description, I detect three players in this game: uses keyword, prune option, and exclude_dep attribute. Am I missing anything?

I would love to see one description of what a Boogie user could expect once this PR lands. If the description is compact, it should find its way into a comment into the code also.

Added a description here:

boogie/Source/Core/CommandLineOptions.cs

Line 574 in 56b011f

* Automatic pruning will remove any declarations that are guaranteed not to be useful for verifying the current implementation.

[RustanLeino]

Good comment. (Otherwise, I would be tempted to suggest we only support None and UsesClauses, and drop support for Automatic and {:exclude_dep}.)

[RustanLeino]

This makes uses a reserved keyword in Boogie. Any previous program that used uses as an identifier will no longer parse. I think this is okay, but we should make sure to bump the Boogie version accordingly (to a new minor number, probably).

If there's concern about making uses a keyword, an alternative would be to add it as a contextual keyword. That's a little tricky here, because

function F(x: int): MyType uses {
  x + 5
}

could mean one thing with

type MyType = int;

and something different with

type MyType T = int;
type uses;

[keyboardDrummer]

I bumped the minor version number

[RustanLeino]

Approved (but see my comment by the version number; I think you may have intended 2.10.0, not 2.10.6).

[shazqadeer]

The discussion about automatic pruning assumes that the reader already understands the basic algorithm for adding edges among various declarations. Is that description already present in some documentation? If not, please add it here. The description should mention the declarations among which edges are present and for each edge a short intuitive description of what that edge means.

[keyboardDrummer]

I don't fully understand the automatic pruning option, so I can't easily provide the detailed description you ask for. I think the summary is that any reference between declarations, except for those in quantifiers with triggers, is considered bidirectional.

I would be okay with removing automatic pruning once Dafny uses UsesClauses pruning.

[shazqadeer]

Ok, removing Automatic seems desirable since currently there are multiple overlapping ways of doing the same thing. Would removing Automatic also mean that :exclude_dep will be dropped?

@RustanLeino : Any objection to dropping Automatic once Dafny uses UsesClauses pruning. What is the timeline on that move?

[keyboardDrummer]

Would removing Automatic also mean that :exclude_dep will be dropped?

Yes

What is the timeline on that move?

I'm working on it. About a month.

[RustanLeino]

I have no objection to dropping the Automatic mode and the :exclude_dep attribute. Instead, we would only support the new uses clauses.

[keyboardDrummer]

@shazqadeer can we merge this? I don't have a strong opinion on the name of the UsesClauses enum. I think the difference with Automatic pruning, is that it only automatically detects outgoing edges in axioms, so something like OnlyUseOutgoingAxiomEdges could be the name.

[shazqadeer]

Based on the description of "UsesClauses", a more appropriate name for it would be "ExploitUses" or "ExploitUsesDecls".

[keyboardDrummer]

I picked the name to indicate 'pruning based on uses clauses'.

The word 'exploit' gives me the impression that uses clauses are already present and ExploitUses pruning will then use them, but actually uses clauses are only useful if you're also using UsesClauses pruning.

I've updated the text a bit, to make sure we're on the same page as to what UsesClauses pruning does.

[shazqadeer]

The word clause in the context of Uses declarations is misleading because clauses are also used in logic to represent disjunctions. By UsesClauses, I think you mean UsesDecls (i.e., the set of uses declarations in the program).

The word 'exploit' gives me the impression that uses clauses are already present and ExploitUses pruning will then use them, but actually uses clauses are only useful if you're also using UsesClauses pruning.

So, if UsesClauses is not used, the uses declarations in the program are ignored?

Perhaps rename the option to UsesDecls.

[keyboardDrummer]

If UsesClauses is not used, the axioms defined in uses clauses are treated as if they were defined top-level.

[shazqadeer]

Do you mean:

If Automatic pruning in combination with {:exclude_dep} does not enable good enough pruning, consider migrating from Automatic to UsesClauses pruning.

[keyboardDrummer]

Not exactly. I've changed the text slightly:

Using Automatic pruning in combination with {:exclude_dep} can be useful if this provides good enough pruning, or to migrate from None to UsesClauses pruning.

[shazqadeer]

Using Automatic pruning in combination with {:exclude_dep} can be useful if this provides good enough pruning, or to migrate from None to UsesClauses pruning.

I still don't understand what this sentence means, specifically the part after the comma. Perhaps you are trying to communicate two separate thoughts in one sentence by reusing words. If you write down those two thoughts separately in two sentences, I might be able to understand better and suggest a coalescing.

Can the part before the comma not be written more compactly as:
Using Automatic pruning in combination with {:exclude_dep} may provide good enough pruning, ...

[keyboardDrummer]

I'm trying to say that there's two use-cases for the Automatic pruning option:

• As a pruning method, although this misses pruning opportunities.
• As a way of migrating from None to UsesClauses pruning.
  Automatic pruning, in combination with an {:exclude_dep} attribute added to each function and constant, behaves the same as UsesClauses pruning. By using Automatic pruning and incrementally adding {:exclude_dep} attributes, one can migrate from None to UsesClauses pruning.
  For each added {:exclude_dep} attribute, one might have to add uses clauses to define the edges that are no longer detected automatically.

[shazqadeer]

Ok, let us merge after renaming UsesClauses to UsesDecls.

…

On Tue, Nov 23, 2021, 1:56 PM Remy Willems ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In Source/Core/CommandLineOptions.cs <#450 (comment)>: > @@ -569,7 +566,77 @@ void ObjectInvariant2() public bool InstrumentWithAsserts = false; public string ProverPreamble { get; set; }= null; public bool WarnNotEliminatedVars = false; - public bool PruneFunctionsAndAxioms = false; + + public enum PruneMode { + None, @shazqadeer <https://github.com/shazqadeer> can we merge this? I don't have a strong opinion on the name of the UsesClauses enum. I think the difference with Automatic pruning, is that it only automatically detects *outgoing* edges in axioms, so something like OnlyUseOutgoingAxiomEdges could be the name. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#450 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AB2RCFVHF4RTAD3FDE7TMQDUNQEZNANCNFSM5HVSEH7Q> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[shazqadeer]

@keyboardDrummer : Do you have a timeline on the dropping of :exclude_dep and Automatic?

[keyboardDrummer]

@keyboardDrummer : Do you have a timeline on the dropping of :exclude_dep and Automatic?

I think a month is a pretty safe upper bound.