Ask TaDA authors about region predicate instances and implied equalities

[viper-admin]

Created by @mschwerhoff on 2017-10-10 09:52 Last updated on 2019-12-17 17:26

• From the Caper paper: if R1_id1(args1) * R2_id1(args2) then R1 == R2 && args1 == args2. Correct?
• From a proof in the TaDA TR: if R1_id1(args1) * R2_id2(args2) and if both instances abstract over the same (or a non-disjoint subset of) heap cells, then R1 == R2 && id1 == id2 && args1 == args2. Correct?

[viper-admin]

@mschwerhoff commented on 2019-12-17 12:33

@Felalolf Do you agree with my observations above? In the BagStack example, these implied equalities are necessary for getting the proof through, and they are currently explicitly assumed.

[viper-admin]

@Felalolf commented on 2019-12-17 12:54

I recently looked for the equalities in the Caper paper, but I did not find them (I was not looking for long thought), but these are the equalities I remember for Caper.

Your formulation for TaDA seems off and vague. I can have to region that share part of a heap cell (fractional permissions) which or not the same region instance because of that.

I would have to look at the BagStack example in detail, but I think there we had a different assumption.

The assumption there is that the physical node next to the head node has not changed if the head node has not changed. Then we assume that the state of this next node is therefore the same.

The region instance, in theory, should not matter (We might still use it to simplify the reasoning, but even then it is a different assumption than what you wrote).

[viper-admin]

@mschwerhoff commented on 2019-12-17 17:26

AFAIR Caper’s BagStack, there is a step where two BagList regions BagList(s1,y1,val1,z1) and BagList(s2,y,val2,z2) are available, and val1 == val2 and/or z1 == z2 needs to be known. The Caper paper says that if s1 == s2, then the two regions are equal, and thus all other arguments. However, AFAIR, s1 == s2 is not directly known, and the only way that I can see (and could confirm via experimenting with Caper) that would imply s1 == s2 is because both regions share the same memory footprint, via y.

Without fractional permissions (not sure if I also experimented with these), this makes sense, since folding the first region instance consumes all permissions, so all regions that hold full permissions to a particular memory cell must be equal regions.