Preliminaries

Specialize rel_incr to use (≤).

Simulation relations blueprints

Components

This is the most general definition of a simulation relation toolkit that we use. We are given two memory models, and a carrier type for the relation (which generalizes meminj). We also have two basic relation components, indexed by elements of the carrier type: match_mem specifies how memory states should be related, whereas match_block specifies how block identifiers should be related. From these two components, it is possible to build up ways to relate more complex states such as Clight.state or Asm.state. The carrier type ensures that the constituent memory state, values, pointers, etc. are related in a consistent way. We also specify a preorder on the carrier type (which generalizes inject_incr), which match_block (and derived relations) should be consistent with. This is because the simulation diagram of some memory operations (namely Mem.alloc) use a final parameter p' : param different from the initial parameter p : param. To ensure that other components of the state remain related, in such cases we require that p ≤ p'. Finally, the relations on Compcert values (val, memval) are built from match_block in nearly the same way for all of our simulation relations (identical values are related, as well as pointers with related block identifiers and identical offsets). But there is one aspect that differs between different simulation relations: with some relations we want Vundef and Undef on the left to be related to any values on the right (ie. be bottom elements), whereas for other relations we only want them to be related to themselves. The obvious solution is to specify for each relation a flag indicating which case we're in. However this is incompatible with composition. Consider a relation R1 which relates Vundef to anything (flag set), and a relation R2 which only relates it to itself (flag cleared). The composite relation R1;R2 will relate Vundef to most values, but there may be a block b' on the right such that there is no b related to it on the left by R2 (∀ b, ¬ b R2 b'). In this case Vundef on the left will not be related by R1;R2 to Vptr b' 0 on the right, because there is no intermediate value for the composition to use. Because of these contradictory situations, there is no setting for the flag that describes the composite relation appropriately. To address this, we generalize from there and split the flag into two part: the proposition simrel_undef_matches_values determines whether Vundef matches all non-pointer values, and the predicate simrel_undef_matches_pointer indicates which pointer values Vundef additionnaly matches. If some pointer are related to Vundef, then non-pointer values should all be related to Vundef as well. Conversely, if simrel_undef_matches_values is set, then any block b2 related to some block b1 on the left by match_block should be related to Vundef as well.

In what follows we declare many typeclass instances with a simrel_undef_matches_× premise. To make sure they work as expected, we declare them as typeclasses. We also show that simrel_undef_matches_values is decidable, since it is defined from a boolean.

Relations derived from simrel_meminj

Compcert usually passes pointers around as separate block and offset arguments. Since we can't relate those independently (because the offset shift is specific to each block), we instead relate (block, offset) pairs and use rel_curry to construct our Monotonicity} relations. Relating pointers is complicated because of the interaction between the abstract [Z] offsets that are used by the memory model and the [ptrofs] concrete machine representations that are used to build [val]ues. The basic relation [match_ptr] relates abstract pointers in the obvious way, while [match_ptrbits] relates concrete pointers as is done in [Val.inject].

For Mem.free we need to relate a whole range of abstract pointers in the form of an (ofs, lo, hi) triple.

For operations that manipulate blocks, we can use the two relations below: the weaker match_block relates two blocks according to simrel_meminj, no matter what the offset shift is. The stronger match_block_sameofs only relates blocks that correspond to one another with no shift in offset.

From match_ptr and simrel_undef_matches_×, we can derive relation for val and memval.

Note that in the Undef case, even though we use match_val we still need a simrel_undef_matches_values guard. This is because we want to exclude match_memval Undef (Fragment Vundef _ _) when the guard is not satisfied, otherwise for example we lose the fact that match_memval id = eq.

simrel_option_le

This is a version of option_le sensitive to the simrel_undef_matches_values component of a given simulation relation. It is particularly useful in the SimValues library. Some operations are formulated in terms of intermediate option results. Often when some input is Vundef, these intermediate results are set to None. Then Val.of_optbool maps None back to Vundef. This means that whether we want None to act as a bottom element depend on whether Vundef does -- option_le is in general too weak and option_rel is too strong. To solve this problem we introduce this relator, which behaves like one or the other depending on simrel_undef_matches_values. Note that it still might be too weak in some corner cases, because it does not take simrel_undef_matches_block into account. Fortunately, so far this has not been an issue because it seems in practice option val is never used with pointers. The one function that cannot be characterized is Val.make_total, fortunately it is only used in a few places where it can be worked around fairly easily. To define simrel_option_le, we start with a more general flex_option_le parametrized with a proposition P which determines whether None is allowed as a bottom element.

Assuming P is a known typeclass, flex_option_le_none_lb can be used when using lower_bound directly. However the path to RAuto through Related does not work. This is because in that context, the relation from the goal is not available during the LowerBound search; instead we search for a LowerBound instance for an arbitrary relation, which is lated connected to the relation in the goal through a subrel search. This works great with most relations, but in this case this means that at LowerBound resolution time, the value of P is unknown, and we cannot resolve the corresponding premise in flex_option_le_none_lb. We can work around this issue with the following RIntro hint.

For similar reasons, we will also need a corresponding version of leb to relate the results of operations such as Mem.valid_pointer, which are involved in pointer comparisons.

Then, we use simrel_undef_matches_values as the parameter in order to obtain the behavior we want for simrel_option_le. We use a notation so that the instances defined above for flex_option_le can apply directly.

Initial memory

The simrel_new_glbl field is enough to formulate a sufficient condition on programs for the initial memory states to be related. Here we use program_rel to express this condition. Note that we're careful to define simrel_program_rel in such a way that, when applied to simrel_components which have the same simrel_new_glbl and simrel_undef_matches_values_bool, the results will be convertible. This is why the components are parametrized by those directly, rather than by the simrel_components under consideration. The relation on function definitions is straightforward. If R permits Vundef as a bottom element, we also allow new function definitions to be introduced on the right-hand side. Otherwise, the function definitions should either both be None, or both use Some. Since the initial memory is constructed in a way does not actually depend on the details of a function definition, we don't enforce any other requirements.

For variables, we need to distinguish two cases depending on whether they're listed in simrel_new_glbl or not. If they are, then the variable must not appear on the left-hand side, and must appear on the right-hand side, and contain the specified initialization data. Note that for composition to work, we need to make sure that the variable does not appear twice in simrel_new_glbl. Otherwise, it would be possible to have a situation where v appears in both R12 and R23, and None [R23 ∘ R12] (Some v) holds as a result, but there would be no intermediate value x that would satisfy both None [R12] x and x [R23] (Some v). For variables not in simrel_new_glbl, we allow new variables on the right-hand side if simrel_undef_matches_values, and otherwise require that the definitions be identical.

Properties

Properties of the accessibility relation.

Consistency of simrel_undef_matches_values and simrel_undef_matches_block.

The following condition is necessary for the subtraction and comparison of two pointers.

Properties of match_block_delta.

Initial memory

Properties for memory operations.

When comparing two weakly valid pointers of the same block using Val.cmpu, we need to compare their offsets, and so comparing the injected offsets must have the same result. To this end, it is necessary to show that all weakly valid pointers be shifted by the same mathematical (not machine) integer amount. However, contrary to the situation with Mem.address_inject for valid pointers, here for weakly valid pointers we do not know whether this amount is delta. The best we know, thanks to Mem.weak_valid_pointer_inject_no_overflow, is that Ptrofs.unsigned (Ptrofs.repr delta) works, but proving composition would be much harder than for the following weak version:

Packaging them up

Though it is convenient to be able to define a simulation relation's operations and proofs separately, in most other contexts it is simpler to have a single object which bundles them together. Because simrel_ops is a coercion, a simrel can be used with match_val, match_block, etc. One thing to keep in mind is that if a parameter of your definition is only used in conjunction with one of these, its type will be inferred as simrel_components, not simrel.

Properties of derived relations

Compatibility with the accessibility relation

Functionality

Shift-invariance

Relationships between match_foo relations

We call each lemma match_foo_bar that establishes match_bar from a match_foo premise. When this can be done in several ways, we add a suffix to disambiguate.

Global blocks

Miscellaneous

Properties of derived memory operations

XXX: Use a separate SimGlobalenvs.v ?

Maybe it's possible to prove simrel_storebytes from simrel_store as well. But if it is, it's tricky.

Strengthened properties for memory operations

When pointers are extracted from Compcert values, they use machine integers and we know related values contain pointers that are related by match_ptrbits. Often we then convert this machine pointer with offset ofs into an mathematical pointer with offset Ptrofs.unsigned ofs. This is made explicit for our block-offset pair pointers using the following function.