Pruning axioms and functions

[typerSniper]

feat: pruning, enabled with flag /prune.

Before checking an implementation I, it prunes away all axioms and functions that are "unreachable" from I. For defining reachability, think of every axiom and function as nodes of a directed graph. There is an edge from node A to node B, if A mentions a declaration for which B can say something.

More precisely, for every axiom and function I define a set of incoming and outgoing edges. Edges may be labelled with a function or a constant. Incoming (dependency) edges consist of those functions and constants that a node may be useful for.
that the declaration may be useful for. For example, an axiom of the form:

                       axiom forall x, y :: {P(x, y)} {Q(x)} P(x, y) ==> Q(x) && R(y)

has two incoming edges: the function P and the function Q. Outgoing edges consist of functions and constants that a declaration mentions. For the axiom above, there are 3 outgoing edges: P, Q, and R.

Rule-wise:

	Axiom	Function	Implementation
Incoming	Triggers if the axiom has quantified expressions with triggers; otherwise everything in the body of the axiom	Itself (function name)	None
Outgoing	Functions/Constants mentioned in the expression	Functions/Constants mentioned in the definition (if there is one)	Functions/Constants mentioned

In this setup, a declaration A depends on B, if the outgoing edges of A match with some incoming edge of B. Because this is all very syntactic, pruning does not preserve verification outcome. For example, if there is an axiom that says false without mentioning any functions or constants, it will be pruned away and verification may fail.

I also add an attribute on declarations: exclude_dep. The pruning process ignores such declarations while computing dependencies---it removes such declarations from the outgoing set of all others.

[shazqadeer]

@typerSniper :

Why does the axiom in your PR description have incoming edges only for P and Q?

How are incoming and outgoing edges of a function determined?

[typerSniper]

Its not a well-written description, sorry about that.

Rule-wise:

	Axiom	Function	Implementation
Incoming	Triggers	Itself (function name)	None
Outgoing	Functions/Constants mentioned in the expression	Functions/Constants mentioned in the definition (if there is one)	Functions/Constants mentioned

To answer your original question, the axiom's incoming edges are just the triggers---that particular axiom is only useful if somebody mentions P or Q. Otherwise, we can delete it.

[shazqadeer]

Please revise the PR description and include your response to my earlier question. Also indicate what is the motivation for this new feature.

[shazqadeer]

Suppose an axiom does not have any triggers. Would it not have any incoming edges? If yes, then it would always be pruned away. This seems like strange behavior.

[shazqadeer]

What is the purpose? The description is mysterious and does not make sense even after reading the PR description.

[typerSniper]

The pruning process ignores declarations with this attribute. It removes such declarations from the outgoing set of all others.

[typerSniper]

Added this to the PR description

[typerSniper]

Suppose an axiom does not have any triggers. Would it not have any incoming edges? If yes, then it would always be pruned away. This seems like strange behavior.

Good point.

If an axiom is like
axiom C == 3 for some constant C, then C would be its incoming edge. However, if an axiom is just axiom false then it is pruned---thus changing the verification outcome. In such cases, pruning makes verification "incomplete", which is somewhat unavoidable.

[RustanLeino]

Here's some more information.

Motivation

A Boogie program typically contains many declarations (functions, axioms, etc.) that are not needed to verify the implementations. Such functions and axioms may, for example, be part of a standard prelude that is always included in a verifier's translation into Boogie. It may also happen that some functions and axioms are needed to prove some implementation, but not others. Furthermore, in the presence of :split_here and :focus, the same argument applies to each piece of an implementation--that is, some functions and axioms are needed to prove some pieces of an implementation, but not others.

By pruning away declarations that are not needed for a given piece of an implementation, each verification condition passed to the SMT solver is physically independent of other declarations in the input Boogie program. This

• reduces the chance that the SMT solver gets confused by the non-relevant declarations, and thus increases its chances of coming up with a proof
• reduces butterfly effects, since any change in the source/Boogie program that does not affect the verification of a piece of an implementation does not affect the verification condition generated
• potentially improves verification-result caching, since caching would be insensitive to changes in declarations that are not relevant

Dependencies

In general, the incoming edges of a declaration axiom E; are all of the constants and functions mentioned in E. However, this set of incoming edges can be made smaller in two important cases.

• The Boogie program may elect to ignore certain constants or functions, which is done by marking the constant or function with {:exclude_dep}. This is useful for some symbols that are used in every axiom. For example, Dafny places the axioms it generates into different stratospheres, which is done by writing axioms like

  axiom 17 <= height ==> E;
  

  Since this height constant appears in almost every axiom, naive dependency tracking would never prune away any axiom. But by marking height as {:exclude_dep}, the height symbol is not included in dependency edges.

  (I notice I'm describing {:exclude_dep} as having an effect on incoming edges, whereas @typerSniper said {:exclude_dep} affects outgoing edges. I don't think that makes a difference, but if it does, then take my description with a grain of salt.)

• Often, axioms have the form axiom P ==> (forall x: X :: {Trigger(x)} Body(x));, where the forall is known to always end up in a positive position in the verification condition's antecedent. The only way the SMT solver will be able to use such a quantifier is if the trigger Trigger(x) appears elsewhere in the verification condition. Therefore, when such a forall has one or more triggers, the incoming edges are not computed as the free symbols in P, Trigger, and Body, but instead as the free symbols in just P and Trigger. The outgoing edges are computed from P and Body, with no regard to the triggers.

  What I said applies only to those quantifiers that are guaranteed to end up as forall in a positive position in the verification condition's antecedent. For example, it applies to the quantifiers shown in the following axioms:

  axiom A && (B ==> C && (forall ...) && D);
  axiom (exists ...) ==> E;
  

  but it does not apply to all quantifiers. For example, the incoming edges computed for

  axiom (forall x: X :: {TriggerA(x)} P(x)) <==> (forall y: Y :: {TriggerB(x)} Q(y));
  

  is still going to be all the free symbols in TriggerA and TriggerB as well as P and Q.

  Note that this trigger optimization applies only when such a quantifier has one or more user-specified triggers. If the quantifier has no explicit triggers, all of the free symbols in its body are included among the incoming edges.

  Lastly, if a trigger mentions several symbols, then all of those symbols must be present in order to take the incoming edge. For example, the declaration

  axiom (forall x: X :: { A(x), B(x) } { C(x) } P(x));
  

  is included

  • if both A and B are reachable from the piece of the implementation, or
  • if C is reachable from the piece of the implementation.

Unreachable axioms

As mentioned in the PR description, /prune might drop some useful axioms, which would cause Boogie to report more errors on a pruned program than for the original Boogie input without pruning. For example, axiom false; has no incoming edges, so /prune will always exclude it. As another example, the following the set of 3 declarations

const c: Y;
axiom (forall x: X :: P(x) == c);
axiom (forall x: X :: P(x) != c);

would be excluded, unless P or c is used elsewhere.

So, since /prune may drop some useful axioms, it is not for every Boogie user. But this particular issue does not affect Boogie programs generated by a verifier like Dafny.

Types

Boogie type declarations also affect what gets sent to the SMT solver. After /prune has determined which constants, functions, and axioms a particular piece of an implementation needs, it additionally includes any type mentioned among those constants, functions, axioms, and piece of the implementation.