Implement work-around for Carbon being slow with IO heavy programs

[vakaras]

As mentioned in this issue, Carbon is slow when it needs to deal with a sequence of conditional exhale statements, which, for example, are used to encode IO. The problem is that to be able to show that current activation record does not have bounded obligation, the prover needs to traverse entire inhale-exhale history for each exhale. In most cases, the prover cannot reuse information from previous queries because the token for which the permission is queried is almost always fresh. However, Nagini in many cases knows that the token is fresh, which implies that it has no bounded obligations associated with it, and, therefore, can emit assumption assume perm(MustInvokeBounded(t_100)) == none;, which would prevent the prover from exploring the entire history. Modified example from the Carbon issue would look like this:

predicate MustInvokeBounded(r: Ref)
predicate MustInvokeUnbounded(r: Ref)
method test()
{
    var t_0: Ref;
    assert perm(MustInvokeBounded(t_0)) >= none;
    inhale MustInvokeBounded(t_0);



    var t_1: Ref;
    exhale perm(MustInvokeBounded(t_0)) > none ? acc(MustInvokeBounded(t_0)) : acc(MustInvokeUnbounded(t_0))
    inhale MustInvokeUnbounded(t_1);
    assume perm(MustInvokeBounded(t_1)) == none;


    var t_2: Ref;
    exhale perm(MustInvokeBounded(t_1)) > none ? acc(MustInvokeBounded(t_1)) : acc(MustInvokeUnbounded(t_1))
    inhale MustInvokeUnbounded(t_2);
    assume perm(MustInvokeBounded(t_2)) == none;


    var t_3: Ref;
    exhale perm(MustInvokeBounded(t_2)) > none ? acc(MustInvokeBounded(t_2)) : acc(MustInvokeUnbounded(t_2))
    inhale MustInvokeUnbounded(t_3);
    assume perm(MustInvokeBounded(t_3)) == none;
}