Optimize uses clauses (#4428)

(Note that this is @zafer-esen's work. I created the PR for permissions
reasons.)

Dafny uses the Boogie option `prune` by default. (Introduced in [Boogie
PR #427](boogie-org/boogie#427), although the
semantics explained there is [out of
date](boogie-org/boogie#767 (comment)).).

The `prune` option, when enabled, runs a reachability analysis in
Boogie, and prunes away functions, constants and axioms that are not
reachable from root nodes. This greatly reduces resource counts, and
leads to less brittleness; which is why pruning is intentionally made as
strong as possible.

The semantics of pruning, at a high level, is as follows.

If an axiom is inside a `uses` clause of some symbol `s`:
* without quantifiers or without triggers:  do not prune if `s`
   is reachable.
* with both quantifiers and triggers: do not prune if (a) `s` is
   reachable _or_ (b) all symbols in one of its triggers are
   reachable.
If an axiom is not inside a `uses` clause:
* without quantifiers or without triggers: always pruned.
* with both quantifiers and triggers: do not prune if (b) all
   symbols in one of its triggers are reachable.

If (a) holds but (b) does not, this leads to a weaker pruning if an
axiom with quantifiers and triggers is inside a `uses` clause. (b)
matches the semantics of how axioms with triggers are instantiated
(AFAIK), so axioms with both quantifiers and triggers should not be
inside `uses` clauses (with the exception of purely polymorphic
quantifiers, more on this at the end of this comment).

Consider the [following
lines](https://github.com/dafny-lang/dafny/blob/c31932b4b4f77a38e5da9c9f6a7689d8f57346bf/Source/DafnyCore/DafnyPrelude.bpl#L230-L290)
from `DafnyPrelude.bpl`:
```
function $Is<T>(T,Ty): bool uses {           // no heap for now
    axiom(forall v : int  :: { $Is(v,TInt) }  $Is(v,TInt));
    axiom(forall v : real :: { $Is(v,TReal) } $Is(v,TReal));
    axiom(forall v : bool :: { $Is(v,TBool) } $Is(v,TBool));
    axiom(forall v : char :: { $Is(v,TChar) } $Is(v,TChar));
    axiom(forall v : ORDINAL :: { $Is(v,TORDINAL) } $Is(v,TORDINAL));
    [...] // more axioms for every type
 }
```

`$Is` is a function symbol and `TInt`, `TReal` etc. are constant
symbols, i.e., the axioms shown are quantified and all have triggers
with two function or constant symbols. Since they are inside the `uses`
clause of `$Is`, none of these axioms can be pruned if `$Is` is
reachable. However, if the second symbol inside the triggers, say
`TReal` in the second axiom, is still unreachable, that axiom cannot be
triggered despite being preserved (but will negatively affect resource
counts).

This PR moves all quantified axioms with triggers outside of their
`uses` clauses. The one exception is purely polymorphic quantifiers
([example](https://github.com/dafny-lang/dafny/blob/2a2e1c41af9b89c10437abc71cca92eb818e02a8/Source/DafnyCore/DafnyPrelude.bpl#L970-L972)),
which should remain inside a `uses` clause, as these quantifiers
disappear if monomorphization is used in Boogie.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.

---------

Co-authored-by: Zafer Esen <[email protected]>
Co-authored-by: Remy Willems <[email protected]>

Source/DafnyCore/Verifier/Translator.cs

@@ -38,6 +38,17 @@ public partial class Translator {
     public bool UseOptimizationInZ3 { get; set; }
 
     void AddOtherDefinition(Bpl.Declaration declaration, Axiom axiom) {
+      sink.AddTopLevelDeclaration(axiom);
+
+      // Axioms that have triggers and bound variables do not need to be inside
+      // uses clauses. Putting such axioms inside uses clauses weakens pruning
+      // when the trigger contains more than one function or constant symbol combined.
+      // The early return would happen whenever axiom is of the form:
+      // axiom (<quantifier> <(optionally) type variables> <at least one dummy variable> :: { ... } ...
+      if (axiom.Expr is Microsoft.Boogie.QuantifierExpr qe && qe.Dummies != null && qe.Dummies.Any() &&
+          qe.Triggers != null && qe.Triggers.Tr != null && qe.Triggers.Tr.Any()) {
+        return;
+      }
 
       switch (declaration) {
         case null:
@@ -50,8 +61,6 @@ void AddOtherDefinition(Bpl.Declaration declaration, Axiom axiom) {
           break;
         default: throw new ArgumentException("Declaration must be a function or constant");
       }
-
-      sink.AddTopLevelDeclaration(axiom);
     }
 
     public class TranslatorFlags {

Test/dafny0/Fuel.dfy.expect

@@ -21,19 +21,19 @@ Fuel.dfy(324,21): Related location
 Fuel.dfy(313,41): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(312,43): Related location
+Fuel.dfy(314,72): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(312,58): Related location
+Fuel.dfy(314,93): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,46): Related location
+Fuel.dfy(312,43): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,72): Related location
+Fuel.dfy(312,58): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,93): Related location
+Fuel.dfy(314,46): Related location
 Fuel.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'
 Fuel.dfy(335,50): Error: index out of range
 Fuel.dfy(336,38): Error: index out of range
@@ -46,7 +46,7 @@ Fuel.dfy(329,21): Related location
 Fuel.dfy(313,41): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(312,43): Related location
+Fuel.dfy(312,58): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
 Fuel.dfy(314,72): Related location
@@ -55,7 +55,7 @@ Fuel.dfy(329,21): Related location
 Fuel.dfy(314,93): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(312,58): Related location
+Fuel.dfy(312,43): Related location
 Fuel.dfy(336,71): Error: index out of range
 Fuel.dfy(397,22): Error: assertion might not hold
 Fuel.dfy(398,22): Error: assertion might not hold

Test/dafny4/NipkowKlein-chapter7.dfy

@@ -240,6 +240,7 @@ least lemma star_transitive_aux(c0: com, s0: state, c1: com, s1: state, c2: com,
   requires small_step_star(c0, s0, c1, s1)
   ensures small_step_star(c1, s1, c2, s2) ==> small_step_star(c0, s0, c2, s2)
 {
+  if small_step_star(c1, s1, c2, s2) {}
 }
 
 // The big-step semantics can be simulated by some number of small steps

Test/git-issues/git-issue-2026.dfy.expect

@@ -8,25 +8,25 @@ git-issue-2026.dfy(12,0): initial state:
 	ret : _System.array<seq<char>> = ()
 git-issue-2026.dfy(13,24):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 39)] := @0, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	@0 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(15,14):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 39)] := @0, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	i : int = 0
 	@0 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(16,4): after some loop iterations:
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 39)] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0)
 	i : int = 0
 	@0 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(22,27):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 39)] := @0, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	i : int = 0
 	@0 : seq<char> = ['o', 'd', 'd']
 git-issue-2026.dfy(26,18):
 	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 39)] := @0, [0] := @0)
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	i : int = 1
 	@0 : seq<char> = ['o', 'd', 'd']

Test/git-issues/git-issue-2299.dfy.expect

@@ -7,13 +7,13 @@ git-issue-2299.dfy(21,4): Related location
 git-issue-2299.dfy(67,13): Error: assertion might not hold
 git-issue-2299.dfy(21,4): Related location
 git-issue-2299.dfy(81,11): Error: assertion might not hold
-git-issue-2299.dfy(27,18): Related location
-git-issue-2299.dfy(16,4): Related location
+git-issue-2299.dfy(27,4): Related location
+git-issue-2299.dfy(10,11): Related location
 git-issue-2299.dfy(81,11): Error: assertion might not hold
 git-issue-2299.dfy(27,32): Related location
 git-issue-2299.dfy(21,4): Related location
 git-issue-2299.dfy(81,11): Error: assertion might not hold
-git-issue-2299.dfy(27,4): Related location
-git-issue-2299.dfy(10,11): Related location
+git-issue-2299.dfy(27,18): Related location
+git-issue-2299.dfy(16,4): Related location
 
 Dafny program verifier finished with 7 verified, 7 errors

Test/git-issues/git-issue-3855.dfy

@@ -666,26 +666,26 @@ method {:rlimit 30000} {:vcs_split_on_every_assert} fNullify(o : Object, f : str
 
       var nedge :=  Edge(o,f, o.fields[f]); //edge to be nullified
 
-      assert nedge in edges(objects);
+      //assert nedge in edges(objects);
 
       o.fields := RemoveKey(o.fields,f);
 
-      assert nedge !in edges(objects);
+      //assert nedge !in edges(objects);
 
       var zedges := edges(objects); 
 
-      assert zedges + {nedge} == xedges;
+      //assert zedges + {nedge} == xedges;
 
       RefCountIsMonotonic(xisos,xedges,zedges);
 
-      assert heapExternalsZeroOrOneEdges(xedges);
-      assert zedges <= xedges;
-      assert justHeapExternalEdges(zedges) <= justHeapExternalEdges(xedges);
-      assert (set he <- justHeapExternalEdges(zedges) :: he.t.region) <= 
-             (set he <- justHeapExternalEdges(xedges) :: he.t.region);
-      assert forall r <- allRegions(old(objects)) ::
-             externalEdges(r, justHeapExternalEdges(zedges)) <= 
-             externalEdges(r, justHeapExternalEdges(xedges));
+      //assert heapExternalsZeroOrOneEdges(xedges);
+      //assert zedges <= xedges;
+      //assert justHeapExternalEdges(zedges) <= justHeapExternalEdges(xedges);
+      //assert (set he <- justHeapExternalEdges(zedges) :: he.t.region) <= 
+      //       (set he <- justHeapExternalEdges(xedges) :: he.t.region);
+      //assert forall r <- allRegions(old(objects)) ::
+      //       externalEdges(r, justHeapExternalEdges(zedges)) <= 
+      //       externalEdges(r, justHeapExternalEdges(xedges));
 
       assert heapExternalsZeroOrOneEdges(xedges);