Open mschwerhoff opened 2 months ago
While playing with a forall-introduction lemma, I noticed that Silicon and Carbon handle perm() nested inside inhale-exhale expressions differently:
perm()
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 }
While playing with a forall-introduction lemma, I noticed that Silicon and Carbon handle
perm()
nested inside inhale-exhale expressions differently: