Define address_mapsto by encode_val instead of decode_val?

[andrew-appel]

The data_at predicate is defined in terms of the underlying mapsto predicate, which in turn is layered on address_mapsto:
res_predicates.address_mapsto: memory_chunk -> val -> share -> pred rmap.

address_mapsto defines the relation between a val and its representation in memory as a sequence of memval, which is CompCert's description of what could be in a single byte of memory. Compcert relates vals with memvals by these two functions:

encode_val: memory_chunk -> val -> list memval
decode_val: memory_chunk -> list memval -> val

These functions are not exactly inverses of each other: decode_val is not injective, because of the Fragment constructor for memvals. And this causes a problem. For example, consider the lemma floyd.data_at_lemmas.data_at_int_bytes, which expresses the equivalence of (data_at (Vint ...)) with the separating conjunction of four different (data_at (Vubyte ...)). Right now this is only provable in 64-bit mode, so this lemma has a premise Archi.ptr64=true, which limits its applicability.

Right now, address_mapsto is defined in terms of decode_val. @xavierleroy suggests that our problem with data_at_int_bytes (and perhaps other problems as well) could be solved if we instead define address_mapsto in terms of encode_val.

If you look at veric/res_predicates.v, just before the definition of address_mapsto you will see the definition of old_address_mapsto in terms of encode_val. There's a comment there, saying "this is not quite right. For example, it doesn't uniquely determine v".

I am not entirely convinced that the comment is correct. I think it would be worth understanding whether it is really true that old_address_mapsto cannot be used as a basis for the semantic model of Verifiable C. If it's true, then augment the comment for old_address_mapsto with a more detailed explanation. If it's false, then switch back to using encode_val and then perhaps a stronger version of data_at_int_bytes can be proved.

In understanding the question of whether encode_val can be used, closely related to the issue of Fragment memvals, the following consideration may turn out to be helpful:
Fragments never arise in the execution of Clight programs, only in the execution of lower-level intermediate languages. Even if they might arise in a "Compositional CompCert" kind of setting, where Clight programs are linked with compiled programs, Fragments never arise from dereferencing pointers visible in the source code; they only arise in dereferencing (offsets from) the stack pointer, which is not visible in the source program.

[andrew-appel]

Is it true that a Vfloat value can have more than one representation (in Flocq) as a 64-bit bitvector? If so, then old_address_mapsto (with encode_val) will never work. So the first thing to do is prove that Vfloat and Vsingle have unique representations, or find a counterexample.

[xavierleroy]

Is it true that a Vfloat value can have more than one representation (in Flocq) as a 64-bit bitvector?

I would be very surprised.

If you look at veric/res_predicates.v, just before the definition of address_mapsto you will see the definition of old_address_mapsto in terms of encode_val. There's a comment there, saying "this is not quite right. For example, it doesn't uniquely determine v".

One way to make sense out of this comment is to notice that different values can encode to the same memvals, e.g.

encode_val Mint8unsigned (Vint 257) = encode_val Mint8unsigned (Vint 1)

so if you know that "at this address we have the encoding of value v with chunk c", you cannot deduce that loading from this address with chunk c gives you value v; but it's guaranteed to give you value Val.load_result c v, see lemma Memdata.decode_encode_val_similar.