adding initial implementation of permission passthrough

[jyoo980]

Initial work for #9

Unit tested + tested via CLI with

field left: Int
field right: Int

predicate tuple(this: Ref)
{
    acc(this.left) && acc(this.right)
}

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

expanding into

field left: Int

field right: Int

predicate tuple(this: Ref) {
  acc(this.left, write) && acc(this.right, write)
}

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

[ionathanch]

Looks good to me!