Add the ability to specify how much "fuel" a function should have,

i.e., how many times Z3 is permitted to unfold it's definition.  The
new {:fuel} annotation can be added to the function itself, it which
case it will apply to all uses of that function, or it can overridden
within the scope of a module, function, method, iterator, calc, forall,
while, assert, or assume.  The general format is:

{:fuel functionName,lowFuel,highFuel}

When applied as an annotation to the function itself, omit functionName.
If highFuel is omitted, it defaults to lowFuel + 1.

The default fuel setting for recursive functions is 1,2.  Setting the fuel higher,
say, to 3,4, will give more unfoldings, which may make some proofs go through
with less programmer assistance (e.g., with fewer assert statements), but it may
also increase verification time, so use it with care.  Setting the fuel to 0,0 is
similar to making the definition opaque, except when used with all literal arguments.

1 files changed, 423 insertions, 0 deletions

diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy
new file mode 100644
index 00000000..c8a1fc2f
--- /dev/null
+++ b/Test/dafny0/Fuel.dfy
@@ -0,0 +1,423 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+module TestModule1 {

+    function pos(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos(x - 1)

+    }

+

+    method test(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert pos(z) == 0;

+        assert pos(-1) == 0;

+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel

+        assert pos(y) == 4 + pos(y - 4);    // Succeeds, thanks to the assume from the preceding assert

+    }

+}

+

+// Test with function-level fuel boost

+module TestModule2 {

+    function {:fuel 3} pos1(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos1(x - 1)

+    }

+

+    function {:fuel 3,5} pos2(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos2(x - 1)

+    }

+

+    function {:fuel 3,5} pos3(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos3(x - 1)

+    }

+

+    function {:opaque} {:fuel 3,5} pos4(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos3(x - 1)

+    }

+

+    method test(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert pos1(z) == 0;

+        assert pos1(-1) == 0;

+        assert pos1(y) == 3 + pos1(y - 3);

+        assert pos1(y) == 4 + pos1(y - 4);

+

+        assert pos2(z) == 0;

+        assert pos2(-1) == 0;

+        assert pos2(y) == 3 + pos2(y - 3);

+        assert pos2(y) == 4 + pos2(y - 4);

+

+        if (*) {

+            assert pos3(y) == 5 + pos3(y - 5);  // Just enough fuel to get here

+        } else {

+            assert pos3(y) == 6 + pos3(y - 6);  // error: Should fail even with a boost, since boost is too small

+        }

+

+        if (*) {

+            assert pos4(z) == 0;    // error: Fuel shouldn't overcome opaque

+        } else {

+            reveal_pos4();

+            assert pos4(y) == 5 + pos4(y - 5);  // With reveal, everything should work as above

+        }

+

+

+    }

+}

+

+

+module TestModule3 {

+    // This fuel setting is equivalent to opaque, except for literals

+    function {:fuel 0,0} pos(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos(x - 1)

+    }

+

+    method test(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert pos(z) == 0;             // error: Opaque setting hides body

+        assert pos(-1) == 0;            // Passes, since Dafny's computation mode for lits ignore fuel

+        assert pos(y) == 3 + pos(y - 3);// error: Opaque setting hides body

+    }

+}

+

+// Test fuel settings via different contexts

+module TestModule4 {

+    function pos(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos(x - 1)

+    }

+

+    // Should pass

+    method {:fuel pos,3,5} test1(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert pos(z) == 0;

+        assert pos(-1) == 0;

+        assert pos(y) == 3 + pos(y - 3);

+    }

+

+    method {:fuel pos,0,0} test2(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert pos(z) == 0;               // error: Should fail due to "opaque" fuel setting

+        assert pos(-1) == 0;

+        assert pos(y) == 3 + pos(y - 3);  // error: Should fail due to "opaque" fuel setting

+    }

+

+    method test3(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        assert {:fuel pos,0,0} pos(z) == 0;               // error: Should fail due to "opaque" fuel setting

+        assert pos(-1) == 0;

+        if (*) {

+            assert pos(y) == 3 + pos(y - 3);  // error: Should fail without extra fuel setting

+            assert pos(y) == 6 + pos(y - 6);  // error: Should fail even with previous assert turned into assume

+        } else {

+            assert {:fuel pos,3,5} pos(y) == 3 + pos(y - 3);  // Should succeed with extra fuel setting

+            assert pos(y) == 6 + pos(y - 6);  // Should succeed thanks to previous assert turned into assume

+        } 

+    }

+

+    method test4(y:int, z:int) 

+        requires y > 5;

+        requires z < 0;

+    {

+        forall t:int {:fuel pos,3} | t > 0 

+            ensures true;

+        {

+            assert pos(y) == 3 + pos(y - 3);    // Expected to pass, due to local fuel boost

+        }

+

+        if (*) {

+            calc {:fuel pos,3} {

+                pos(y);

+                3 + pos(y - 3);

+            }

+        }

+

+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel outside the forall

+    }

+}

+

+// Test fuel settings via different module contexts

+module TestModule5 {

+    // Test module level fuel settings, with nested modules

+

+    module TestModule5a {

+        module {:fuel TestModule5aiA.pos,3} TestModule5ai {

+            module TestModule5aiA {

+                function pos(x:int) : int 

+                {

+                    if x < 0 then 0

+                    else 1 + pos(x - 1)

+                }

+

+                method test(y:int, z:int) 

+                    requires y > 5;

+                    requires z < 0;

+                {

+                    assert pos(z) == 0;

+                    assert pos(-1) == 0;

+                    assert pos(y) == 3 + pos(y - 3);    // Should pass due to intermediate module's fuel setting

+                }

+            }

+

+            method test(y:int, z:int) 

+                requires y > 5;

+                requires z < 0;

+            {

+                assert TestModule5aiA.pos(z) == 0;

+                assert TestModule5aiA.pos(-1) == 0;

+                assert TestModule5aiA.pos(y) == 3 + TestModule5aiA.pos(y - 3);    // Should pass due to module level fuel

+            }

+        }

+  

+        method test(y:int, z:int) 

+            requires y > 5;

+            requires z < 0;

+        {

+            assert TestModule5ai.TestModule5aiA.pos(z) == 0;

+            assert TestModule5ai.TestModule5aiA.pos(-1) == 0;

+            assert TestModule5ai.TestModule5aiA.pos(y) == 3 + TestModule5ai.TestModule5aiA.pos(y - 3);    // error: Should fail, due to lack of fuel

+        }

+    }

+

+    module {:fuel TestModule5bi.TestModule5biA.pos,3} TestModule5b {

+        module  TestModule5bi {

+            module TestModule5biA {

+                function pos(x:int) : int 

+                {

+                    if x < 0 then 0

+                    else 1 + pos(x - 1)

+                }

+

+                method test(y:int, z:int) 

+                    requires y > 5;

+                    requires z < 0;

+                {

+                    assert pos(z) == 0;

+                    assert pos(-1) == 0;

+                    assert pos(y) == 3 + pos(y - 3);    // Should succceed due to outer module fuel setting

+                }

+            }

+        }

+    }

+}

+

+// Test fuel setting for multiple functions

+module TestModule6 {

+    function pos(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos(x - 1)

+    }

+

+    function neg(x:int) : int

+        decreases 1 - x;

+    {

+        if x > 0 then 0

+        else 1 + neg(x + 1)

+    }

+

+    method test1(y:int, z:int) 

+        requires y > 5;

+        requires z < 5;

+    {

+        assert pos(y) == 3 + pos(y - 3);    // error: Should fail, due to lack of fuel

+

+        assert neg(z) == 3 + neg(z + 3);    // error: Should fail, due to lack of fuel

+    }

+

+    method {:fuel pos,3} {:fuel neg,4} test2(y:int, z:int) 

+        requires y > 5;

+        requires z < -5;

+    {

+        assert pos(y) == 3 + pos(y - 3);    

+

+        assert neg(z) == 3 + neg(z + 3);    

+    }

+}

+

+// Test fuel settings with multiple overlapping contexts

+module TestModule7 {

+    function {:fuel 3} pos(x:int) : int 

+    {

+        if x < 0 then 0

+        else 1 + pos(x - 1)

+    }

+

+    function {:fuel 0,0} neg(x:int) : int

+        decreases 1 - x;

+    {

+        if x > 0 then 0

+        else 1 + neg(x + 1)

+    }

+

+    method {:fuel neg,4} {:fuel pos,0,0} test1(y:int, z:int) 

+        requires y > 5;

+        requires z < -5;

+    {

+        if (*) {

+            assert pos(y) == 3 + pos(y - 3);    // error: Method fuel should override function fuel, so this should fail

+            assert neg(z) == 3 + neg(z + 3);    // Method fuel should override function fuel, so this succeeds

+        }

+

+        forall t:int {:fuel pos,3} | t > 0 

+            ensures true;

+        {

+            assert pos(y) == 3 + pos(y - 3);    // Statement fuel should override method fuel, so this should succeed

+        }

+    }

+}

+

+// Test fuel in a slightly more complicated setting

+module TestModule8 {

+

+    newtype byte = i:int | 0 <= i < 0x100

+    newtype uint64 = i:int | 0 <= i < 0x10000000000000000

+

+    datatype G = GUint64

+               | GArray(elt:G)

+               | GTuple(t:seq<G>)

+               | GByteArray

+               | GTaggedUnion(cases:seq<G>)

+

+        datatype V = VUint64(u:uint64)

+                   | VTuple(t:seq<V>)

+                   | VCase(c:uint64, val:V)

+

+        predicate {:fuel 2} ValInGrammar(val:V, grammar:G)

+        {

+            match val

+                case VUint64(_) => grammar.GUint64?

+                case VTuple(t)  => grammar.GTuple? && |t| == |grammar.t|

+                                      && forall i :: 0 <= i < |t| ==> ValInGrammar(t[i], grammar.t[i])

+                case VCase(c, val) => grammar.GTaggedUnion? && int(c) < |grammar.cases| && ValInGrammar(val, grammar.cases[c])

+        }

+

+        datatype CRequest = CRequest(client:EndPoint, seqno:uint64, request:CAppMessage) | CRequestNoOp()

+

+        type EndPoint

+        function method EndPoint_grammar() : G { GUint64 }

+        function method CRequest_grammar() : G { GTaggedUnion([ GTuple([EndPoint_grammar(), GUint64, CAppMessage_grammar()]), GUint64]) }

+

+        function method parse_EndPoint(val:V) : EndPoint

+            requires ValInGrammar(val, EndPoint_grammar());

+

+        type CAppMessage

+        function method CAppMessage_grammar() : G { GTaggedUnion([GUint64, GUint64, GUint64]) }

+        function method parse_AppMessage(val:V) : CAppMessage

+            requires ValInGrammar(val, CAppMessage_grammar());

+

+        function method {:fuel ValInGrammar,1,2} parse_Request1(val:V) : CRequest

+            requires ValInGrammar(val, CRequest_grammar());

+        {

+            if val.c == 0 then

+                var ep := parse_EndPoint(val.val.t[0]); // With default fuel, error: function precondition, destructor, index

+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]))    // error: index out of range, destructor

+            else 

+                CRequestNoOp()

+        }

+

+        function method parse_Request2(val:V) : CRequest

+            requires ValInGrammar(val, CRequest_grammar());

+        {

+            if val.c == 0 then

+                var ep := parse_EndPoint(val.val.t[0]);                      // With fuel boosted to 2 this succeeds

+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2])) // error: destructor

+            else 

+                CRequestNoOp()

+        }

+

+        function method {:fuel ValInGrammar,3} parse_Request3(val:V) : CRequest

+            requires ValInGrammar(val, CRequest_grammar());

+        {

+            if val.c == 0 then

+                var ep := parse_EndPoint(val.val.t[0]); 

+                CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]))    // With one more boost, everything succeeds

+            else 

+                CRequestNoOp()

+        }

+

+        // With the method, everything succeeds with one less fuel boost (i.e., 2, rather than 3, as in parse_Request3)

+        method parse_Request4(val:V) returns (req:CRequest)     

+            requires ValInGrammar(val, CRequest_grammar());

+        {

+            if val.c == 0 {

+                var ep := parse_EndPoint(val.val.t[0]);

+                req := CRequest(ep, val.val.t[1].u, parse_AppMessage(val.val.t[2]));

+            } else {

+                req := CRequestNoOp();

+            }

+        }

+}

+

+

+// Test fuel when it's applied to a non-recursive function

+module TestModule9 {

+    function abs(x:int) : int

+    {

+        if x < 0 then -1 * x else x

+    }

+

+    // All should pass.

+    method test1(y:int, z:int)

+        requires y > 5;

+        requires z < 0;

+    {

+        assert abs(z) == -1*z;

+        assert abs(y) == y;

+        assert abs(-1) == 1;

+    }

+

+    // Method-level fuel override

+    method {:fuel abs,0,0} test2(y:int, z:int)

+        requires y > 5;

+        requires z < 0;

+    {

+        assert abs(z) == -1*z;  // error: Cannot see the body of abs

+        assert abs(y) == y;     // error: Cannot see the body of abs

+        assert abs(-1) == 1;    // lit bypasses fuel, so this should succeed

+    }

+

+    // Statement-level fuel override

+    method test3(y:int, z:int)

+        requires y > 5;

+        requires z < 0;

+    {

+        assert {:fuel abs,0,0} abs(z) == -1*z;  // error: Cannot see the body of abs

+        assert abs(y) == y;     // Normal success

+        assert abs(-1) == 1;    // lit bypasses fuel, so this should succeed

+    }

+

+    // Giving more fuel to a non-recursive function won't help,

+    // but it shouldn't hurt either.

+    method {:fuel abs,5,7} test4(y:int, z:int)

+        requires y > 5;

+        requires z < 0;

+    {

+        assert abs(z) == -1*z;

+        assert abs(y) == y;

+        assert abs(-1) == 1;

+    }

+}

+