Prerequisites

The class below specifies the prerequisites for our implementation of MakeProgram. Basically, we need to know how to convert the definition in modules and layers into Compcert program definitions. Note that the types of function and variable definitions in the produced program are not always related to the types of definitions in our modules and layers. For instance, in order to be able to use our layers to construct C as well as assembly programs, their global variable definitions need to store C-style typing information. When building assembly programs they will be converted into low-level types. Hence, we need to distinguish between to output program types Fp and Vp, and the types used in the module and layer Fm and Vm. Another difficulty that arises because of the discrepency between our view and Compcert's is related to what a function definitions is: Compcert's internal functions correspond to functions defined in our modules, whereas external functions correspond to the primitives defined in layer interfaces. In our case,

Often used when defining make_varinfo

Relations

The most important property of make_program takes the form a relational parametricity theorem: module-layer pairs that are related in a given way will yield programs that are related in a corresponding way. The devil is in the details of what we by "related in a given way" and "related in a corresponding way". If fact, we will use general specifications of how function definitions are to be related. From a relation this kind (funrel), we will derive both a relation on module-layer pairs (using module_layer_rel defined below), and a relation on programs (using an appropriate parameter for program_le). The first step is to define some accessors for handling module-layer pairs as a whole.

Those should be moved to coqrel?

A function definition can either be an internal definition as found in modules (given by the type parameter Fm in ProgramFormatOps) or an external definition corresponding to a primitive specification (of the type primsem). We allow the user to specify a different relation at each identifier, which means we can have a fairly precise funrel.

From such a relation (family) Rf : funrel D1 D2, we can derive the corresponding relation on module-layer pairs, module_layer_rel D1 D2 Rf.

We can also derive a relation on program definitions, this time indexed by blocks, suitable for program_le or genv_le.

While we can use a wide range of funrel and varrel to encode different situations, we do have some restrictions. In particular, adding more definitions may trigger an error condition, which is only allowed by res_le to appear on the right, or both sides. Hence, while we allow None on the left to be related to Some on the right, we use OptionRelationForward to forbid the opposite situation. Then, we require that the relations on programs contain the image of the relations on modules as defined using match_fundef and match_vardef.

One specific way to construct relations which satisfy the HasImage constraints above is to simply use rel_proj to compute the image in question.

Establishing MakeProgramRelations then boils down to proving the OptionRelationForward conditions.

Specification of make_program

From and instance of ProgramFormatOps and a module-layer pair, make_program attempts to build a Compcert program. We also define the compound make_globalenv, which builds a Compcert global environment from the program in quesion.

For most part, the specification of make_program consists in a relational parametricity property expressed using the relations defined above. We also use the following inductive type to express the property that if make_program succeeds, then there should have been no conflict between the function and variables in the module and layer. We are now ready to give the specification of make_program.

We can also introduce variants of the relational property based on program_le and genv_le, which are less general but more convenient to use in many contexts.

We're careful not to register these instances of MakeProgramRelations too widely because otherwise it's used for solving ident → OptionRelationForward (option_le eq) and leave us with uninstantiated evars as a result.