Heap chunk removal is more efficient for certain orderings of information in specs

[jennalwise]

In consume, heap chunk removal is defined in such a way where ordering matters for performance of run-time checks (this is likely not just inherent to the specific heap removal functions, but also the structure of consume itself). For example, consider the symbolic states and specifications to be consumed:

state: ? && acc(x.f) && p(y)
consume: acc(y.f) && acc(x.f)

First, acc(y.f) is looked up in the state. Since, it does not exist in the state ? provides acc(y.f) and then all possibly overlapping permissions are removed from the state, e.g. acc(x.f) and p(y). Even though the consume tells us that acc(x.f) is separated from acc(y.f), the verifier does recognize this information, and so the resulting state is ? and a run-time check for acc(y.f) is produced. Then, acc(x.f) is asserted and consumed in the ? state, so a run-time check is produced for acc(x.f) and ? is the resulting state after the consume. To summarize, this consume produces two run-time checks: acc(y.f) and acc(x.f) and results in the ? state after consumption. If the order of acc(y.f) and acc(x.f) is flipped, then only the run-time check for acc(y.f) is created and ? is the resulting state.

Of course, this issue is worse if the run-time check that could be statically discharged with one ordering is a predicate rather than an accessibility predicate. Recursive predicates can be expensive to check at run time, so choosing the wrong ordering of permissions in the spec to be consumed can be costly.

It is possible this can be fixed by leveraging information across the specification to be consumed. This next example can also benefit from such a solution:

state: ? && acc(x.f)
consume: acc(y.f) && x == y

Here, currently, the verifier will produce run-time checks for acc(y.f) and x == y and result in the ? state. Even if the order is changed to x == y && acc(y.f), the result will be the same. This is because information across a consume is asserted individually.