Struct & Class

consider the following C++ class.
      class Point {
        int x;
        int y;
      };

cpp2v will generate mangled names and some notations to help you write predicates more conveniently.

Just like intR defines the memory representation for the type int, we can define PointR to define the memory representation for the class Point. The following says, that the field x contains the integer 1 and field y contains the integer value 5

The above was too concrete; it stored the specific point (1,5). Just like intR takes as agument a z:Z to denote the mathematical number being represented, we define a Gallina record to denote the mathematical model of what is stored:

Then we can define the general class representation as follows:

Tagged Unions

Sometimes, the interpretation of a piece of data depends on another value. For example, consider the following class.
   struct tagged {
     bool tag;
     union { int x; bool y; };
   };

A datatype like this represents *either* an integer, or a boolean. Following the same pattern above, we construct a Coq type to capture this. In this case, rather than writing a Record, we use a Variant.

this has both integers and booleans

these are tagged in Coq, i.e. we can pattern match on a value of type M to determine which case it is.

to write a representation predicate for a tagged union, we can pattern match on the model to comput the value of the tag field for the representation predicate.

note that in this definition, the x_field and y_field are *not* disjoint. an equivalent way to write this definition is the following.

a benefit to this approach is that is is clear that, regardless of the value of the model, it is always safe to access the tag field. in practice, however, it isn't difficult to prove that they are equivalent.

with the above representation predicate, we can represent an object carrying the value 5 and an object carrying the value false as below.

one issue with the above definitions is that they do not capture the possible "slack" bits in the implementation. to understand the intricacies connected to "slack" bits, see slack_bits.v

Untagged Unions

Untagged unions are a little bit more complex. In practice, they should be avoided when possible, but this doesn't always lead to nice code, so we do support them. If you must use them, we write a representation predicate for each of the possibilites of the union and then prove equivalences between them. Concretely, here is an example:
    union OrBytes {
      int32 word;
      struct { int16 high; int16 low; };
    };

The representation for word is easy, the one for the struct is only slightly more complex.

Now, when we write the representation predidate for OrBytes, we pick one of the two representations as primary. Here, we will pick OrBytes_wordR as primary.

It is undefined behavior in C++ to read the element of a union that was not most recently written. To convert from one representation to another by writing, you can first convert the representation back to uninitR "OrBytes" 1, and then re-initialize the desired union member. Some compilers implement a language extension which defines this behaivor. If you wish to rely on this behavior, you can write lemmas similar to the following. This theorem allows you to view an OrBytesR as an OrBytes_high_lowR

this theorem allows you to go the other way

proving these lemmas tends to not be very difficult in most cases, assuming the appropriate axioms about memory layout and alignedness. Bare in mind that these sometimes have compiler or architecture specified behavior. For example, the struct above is relying on a particular endianness, switching to another architecture might get you the opposite values.