Perm under inhale-exhale expression handled differently by Silicon vs. Carbon

[mschwerhoff]

While playing with a forall-introduction lemma, I noticed that Silicon and Carbon handle perm() nested inside inhale-exhale expressions differently:

field f: Int

function foo(x: Ref, p: Perm): Bool
  requires p > none
  requires acc(x.f, p)

method lemma_forall_intro()
  ensures [forall y: Ref :: perm(y.f) > none ==> foo(y, write), true]
    // Silicon: Rejected as illformed
    // Carbon: Not rejected

method test0() {
  var a: Ref

  inhale acc(a.f, 1/2)
  lemma_forall_intro()
  assert perm(a.f) > none ==> foo(a, write)
    // Silicon: OK
    // Carbon: Fails with insufficient permission
}

method test1() {
  var a: Ref

  inhale acc(a.f, 1/2)
  lemma_forall_intro()
  assert perm(a.f) > none ==> foo(a, 1/2)
    // Silicon: OK
    // Carbon: Fails with "might not hold"
}

method test2() {
  var a: Ref

  inhale acc(a.f, write) 
  lemma_forall_intro()
  assert perm(a.f) > none ==> foo(a, write)
    // Silicon: Fails with "might not hold"
    // Carbon: OK
}