Handle partial predicate accesses for pre-/postconditions

[ionathanch]

Consider this modified example from the tutorial:

field left: Int
field right: Int

method addTuple(this: Ref)
  returns (sum: Int)
  requires acc(tuple(this), 1/2)
{
  unfold acc(tuple(this), 1/2)
  sum := this.left + this.right
}

We currently expand this (I think) into the following:

method addTuple(this: Ref) returns (sum: Int)
  requires acc(this.left) && acc(this.right)
{
  sum := this.left + this.right
}

This is incorrect because if we call addTuple like this:

method callAddTupleTwice(this: Ref)
  returns (sum: Int)
{
  var tup: Ref
  tup := new(left, right)

  tup.left := 6
  tup.right := 9
  fold tuple(tup)

  sum := addTuple2(tup)
  sum := addTuple2(tup)
}

After inlining, callAddTupleTwice will fail to verify. During expansion, we need to propagate permission values (or yeet the problem into Future Work).

I'm also wary about removing things like [un]fold acc(tuple(this), 1/2), there might be some intricacies with partial (un)folding we might not be aware of, but I haven't come up with any counterexamples yet.

[jyoo980]

Ideally we want the following program transformation

field left: Int
field right: Int

method addTuple(this: Ref)
  returns (sum: Int)
  requires acc(tuple(this), 1/2)
{
  unfold acc(tuple(this), 1/2)
  sum := this.left + this.right
}

should expand into

method addTuple(this: Ref)
  returns (sum: Int) 
  requires acc(this.left, 1/2) && acc(this.right, 1/2) 
{
  sum := this.left + this.right
}

[jyoo980]

Resolved by #19