Unsoundness with quantified permissions

[zgrannan]

Silicon accepts this code, but it should not (see the "ensures false" postcondition of foo()):

domain ResourceHolder {

    function ghostBalance(rh: ResourceHolder, resource: Int): Ref

    function mkHolder(rh: Int): ResourceHolder

    axiom mkInjective {
        forall rh1 : Int, rh2: Int :: rh1 != rh2 ==> mkHolder(rh1) != mkHolder(rh2)
    }

    axiom balanceInjective {
        forall owner1: ResourceHolder, owner2: ResourceHolder, resource1: Int, resource2: Int :: 
        (owner1 != owner2 || resource1 != resource2) ==> ghostBalance(owner1, resource1) != ghostBalance(owner2, resource2)
    }

}

field resourceAmount: Int

method foo() 
    requires forall rr: Int :: acc(ghostBalance(mkHolder(0), rr).resourceAmount)
    requires acc(ghostBalance(mkHolder(1), 1).resourceAmount)
    ensures false
{
}

Carbon raises the expected verification error.

[zgrannan]

I think that the unsoundness here is due to the inverse function for the quantified permission in foo() with Silicon generating an unsound axiom of the form, forall rr: Ref :: ghostBalance(mkHolder(0), inv(rr)) == rr. I think then #342, is a special case of this issue.

I think the solution here should work: https://pm.inf.ethz.ch/publications/Schwerhoff16.pdf#page=122

[mschwerhoff]

Duplicate of #342