veric/superprecise.v

[andrew-appel]

In veric/superprecise.v there are several ill-maintained lemmas that are now Aborted or commented-out. They relate to the superprecise property of an mpred, which is a stronger version of the standard separation-logic notion of precise. Once upon a time, superprecise was used in several ways in proving programs correct in Verifiable C, but now it seems no longer to be needed. (For example, even though many of those lemmas are commented out or Aborted, nobody complains.)

The difficulty in proving those lemmas arises if a val can have more than one representation in memory as a sequence of memvals. That could happen for two reasons:

1. Defining address_mapsto using decode_val instead of encode_val, see issue Define address_mapsto by encode_val instead of decode_val? #602
2. Vfloat or Vsingle could have nonunique representations as bit patterns.

I am not sure that reason 2 is real. That is, at one time I thought that a float val could have more than one flocq bit pattern, but I don't believe it now. And reason 1 might be resolved if issue #602 is resolved in favor of encode_val. Come to think of it, if it's true that Vfloat can have multiple representations, then that's why issue #602 must be resolved as "cannot use encode_val".

So therefore, to resolve this issue:
. Wait until issue #602 is resolved one way or the other. If "keep using decode_val", then simply close this issue with the remark that Fragment will inevitably mean that these predicates are not superprecise.
. Decide whether it's worth keeping the notion of superprecise and the proofs that several mpreds are superprecise; maybe it's not useful for anything. If not useful, delete veric/superprecise.v and close this issue.
. Otherwise, prove these lemmas.