Require Import LibLists.
Require Import Cplusconcepts.
Require Import Coqlib.
Require Import Tactics.
Require Import CplusWf.
Require Import LibMaps.
Require Import LayoutConstraints.
Require Import LibPos.
Require Import CPP.

Load Param.

The proof of correctness of an algorithm based on the Common Vendor ABI (POPL 2011, Section 6.1)

Section CVABI.
Variable A : ATOM.t.

Empty classes

A class is empty if, and only if, all the following conditions hold:

it has no fields
it has no virtual methods
it has no virtual bases
all its direct non-virtual bases are empty

Section Is_empty.

Variable hierarchy : PTree.t (Class.t A).

Inductive is_empty : ident -> Prop :=
| is_empty_intro : forall ci c
  (H_ci_c : hierarchy ! ci = Some c)
  (H_no_fields : Class.fields c = nil)
  (H_no_virtual_methods : forall m, In m (Class.methods c) -> Method.virtual m = true -> False)
  (H_no_virtual_bases : forall b, In (Class.Inheritance.Shared, b) (Class.super c) -> False)
  (H_bases_empty : forall b, In (Class.Inheritance.Repeated, b) (Class.super c) -> is_empty b),
  is_empty ci
.

This definition meets the constraints for empty classes stated in 4.3

Lemma is_empty_prop : Is_empty.prop hierarchy is_empty.

Proof.

Lemma dynamic_nonempty : forall i,
is_dynamic hierarchy i -> is_empty i -> False.

Proof.

Hypothesis hierarchy_wf : Well_formed_hierarchy.prop hierarchy.

Lemma no_virtual_bases : forall ci,
is_empty ci ->
forall vb, is_virtual_base_of hierarchy vb ci -> False.

Proof.

Lemma is_empty_dec : forall i, {is_empty i} + {~ is_empty i}.

Proof.

End Is_empty.

Definition Optim := CPP.Optim (CppOptim is_empty_prop dynamic_nonempty).

Variable (PF : PLATFORM A).

Overview of the layout algorithm

Computed values

Apart from the values expected in 4.1 and computed in offsets, this algorithm computes the ebo and nvebo sets of empty base offsets and non-virtual empty base offsets, incrementally as in 4.5.5. cilimit is the identifier of the class being laid out.

     Record LD : Type := Ld {
       offsets : PTree.t (LayoutConstraints.t A);
       cilimit : ident;
       ebo : PTree.t (list (ident * Z));
       nvebo : PTree.t (list (ident * Z))
     }.

     Section prop.

       Variable hierarchy : PTree.t (Class.t A).

       Variable o : LD.

Invariant

Guard conditions: offsets, ebo and nvebo are defined for all classes with an identifier less than cilimit:
Soundness condition: for all such classes, the conditions stated in 4.5 hold
specification of the sets ebo, nvebo of (non-virtual) empty base offsets

Record prop : Prop := intro {

Guard

offsets_guard : forall ci, (offsets o) ! ci <> None -> hierarchy ! ci <> None;

Section 4

offsets_intro : forall ci of, (offsets o) ! ci = Some of -> class_level_prop Optim PF (offsets o) hierarchy ci of
;

Guard

offsets_guard2 : forall ci, (offsets o) ! ci <> None -> Plt ci (cilimit o);

This algorithm mandates the following additional invariant that the non-virtual data of a class be entirely included in the non-virtual part (which is not required by the soundness conditions, as stated in 4.5.1). As we show a generalized condition of non-overlapping of total sizes of non-empty non-virtual bases, this additional invariant is necessary to show C6.

         non_virtual_data_size_non_virtual_size:
           forall ci of, (offsets o) ! ci = Some of ->
             non_virtual_data_size of <= non_virtual_size of
             ;

Guard

offsets_exist : forall ci, Plt ci (cilimit o) -> hierarchy ! ci <> None -> (offsets o) ! ci <> None
;

4.5.5 for empty bases

disjoint_ebo : forall ci o', (offsets o) ! ci = Some o' -> disjoint_empty_base_offsets Optim (offsets o) hierarchy ci o'
;

Specification and guard conditions for ebo, nvebo the sets of (non-virtual) empty base offsets

         ebo_prop : forall ci e, (ebo o) ! ci = Some e -> forall b o', (In (b, o') e <-> empty_base_offset Optim (offsets o) hierarchy ci b o')
           ;
         ebo_exist : forall ci, Plt ci (cilimit o) -> (ebo o) ! ci <> None
           ;
         ebo_guard : forall ci, (ebo o) ! ci <> None -> Plt ci (cilimit o)
           ;
         nvebo_prop : forall ci e, (nvebo o) ! ci = Some e -> forall b o', (In (b, o') e <-> non_virtual_empty_base_offset Optim (offsets o) hierarchy ci b o')
           ;
         nvebo_exist : forall ci, Plt ci (cilimit o) -> (nvebo o) ! ci <> None;
         nvebo_guard : forall ci, (nvebo o) ! ci <> None -> Plt ci (cilimit o)
       }.

   End prop.

       Hint Resolve offsets_guard offsets_intro offsets_exist disjoint_ebo ebo_prop ebo_exist nvebo_prop nvebo_exist.


Section Layout.

       Variable hierarchy : PTree.t (Class.t A).

       Hypothesis hierarchy_wf : Well_formed_hierarchy.prop hierarchy.

       Let virtual_bases := let (t, _) := Well_formed_hierarchy.virtual_bases hierarchy_wf in t.

       Let virtual_bases_prop : (forall cn,
         hierarchy ! cn <> None -> virtual_bases ! cn <> None) /\
       forall cn l, virtual_bases ! cn = Some l ->
         forall i, (In i l <-> is_virtual_base_of hierarchy i cn)
           .

Proof.

Incremental layout

The identifier of the class being laid out is LD.cilimit ld. All classes with an identifier less that LD.cilimit ld are assumed to be already laid out.

    Section Step.

       Variable ld : LD.

       Hypothesis Hld : prop hierarchy ld.

       Section Def.

       Variable h : Class.t A.

       Hypothesis Hh : hierarchy ! (cilimit ld) = Some h.

Layout of non-virtual direct bases

Section Non_virtual_direct_base_layout.

nvl_todo: the list of non-virtual direct bases to which an offset has not yet been assigned
nvl_offsets: the mapping between non-virtual direct bases and offsets
nvl_nvebo: the set of non-virtual empty base offsets reachable through a direct non-virtual base that has already been assigned an offset
nvl_nvebo': the set of non-virtual empty base offsets reachable through an *empty* direct non-virtual base that has already been assigned an offset
nvl_nvds: the non-virtual data size so far. This is also the field boundary so far (because fields will be laid out no sooner than after the last non-virtual direct base).
nvl_nvsize: the non-virtual size so far.
nvl_pbase: the primary base, if any
nvl_align: the non-virtual alignment so far

         Record nvl : Set := make_nvl {
           nvl_todo : list ident;
           nvl_offsets : PTree.t Z;
           nvl_nvebo : list (ident * Z);
           nvl_nvebo' : list (ident * Z);
           nvl_nvds : Z;
           nvl_nvsize : Z;
           nvl_pbase : option ident;
           nvl_align : Z
         }.

         Section prop.

           Variable nvldata : nvl.

           Record nvl_prop : Prop := nvl_intro {

Guard

nvl_exist : forall ci, (In (Class.Inheritance.Repeated, ci) (Class.super h) <-> ((nvl_offsets nvldata) ! ci <> None \/ In ci (nvl_todo nvldata)));

C21

nvl_primary_base : forall ci, nvl_pbase nvldata = Some ci -> (nvl_offsets nvldata) ! ci = Some 0;

4.3

nvl_primary_base_dynamic : forall ci, nvl_pbase nvldata = Some ci -> is_dynamic hierarchy ci;

Guard

nvl_data_low_bound : 0 <= nvl_nvds nvldata;

C19

nvl_data_dynamic_low_bound : is_dynamic hierarchy (cilimit ld) -> dynamic_type_data_size PF <= nvl_nvds nvldata;

Additional invariant stated in 6.1, helper for both C1 and C6

nvl_data_size : nvl_nvds nvldata <= nvl_nvsize nvldata;

Guard

nvl_size_pos : 0 < nvl_nvsize nvldata;

Guard

nvl_low_bound : forall ci of, (nvl_offsets nvldata) ! ci = Some of -> 0 <= of;

C20

nvl_dynamic_no_primary_low_bound : is_dynamic hierarchy (cilimit ld) -> nvl_pbase nvldata = None -> forall ci, (is_empty hierarchy ci -> False) -> forall of, (nvl_offsets nvldata) ! ci = Some of -> dynamic_type_data_size PF <= of;

C6 generalized to total sizes. The additional invariant nvl_data_size helps show C6

nvl_nonempty_non_overlap : forall ci1 o1, (nvl_offsets nvldata) ! ci1 = Some o1 -> (is_empty hierarchy ci1 -> False) -> forall ci2 o2, (nvl_offsets nvldata) ! ci2 = Some o2 -> (is_empty hierarchy ci2 -> False) -> ci1 <> ci2 -> forall of1, (offsets ld) ! ci1 = Some of1 -> forall of2, (offsets ld) ! ci2 = Some of2 -> o1 + non_virtual_size of1 <= o2 \/ o2 + non_virtual_size of2 <= o1;

C23

nvl_disjoint_empty_bases : forall ci1 o1, (nvl_offsets nvldata) ! ci1 = Some o1 -> forall ci2 o2, (nvl_offsets nvldata) ! ci2 = Some o2 -> ci1 <> ci2 -> forall b bo1, non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci1 b bo1 -> forall bo2, non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci2 b bo2 -> o1 + bo1 <> o2 + bo2;

nvl_nonempty_high_bound : forall ci, (is_empty hierarchy ci -> False) -> forall of, (nvl_offsets nvldata) ! ci = Some of -> forall o', (offsets ld) ! ci = Some o' -> of + non_virtual_size o' <= nvl_nvds nvldata;

nvl_high_bound : forall ci, forall of, (nvl_offsets nvldata) ! ci = Some of -> forall o', (offsets ld) ! ci = Some o' -> of + non_virtual_size o' <= nvl_nvsize nvldata;

Guard

nvl_align_pos : 0 < nvl_align nvldata;

C16

nvl_align_dynamic : is_dynamic hierarchy (cilimit ld) -> (dynamic_type_data_align PF | nvl_align nvldata);

C15

nvl_align_prop : forall ci, (nvl_offsets nvldata) ! ci <> None -> forall of, (offsets ld) ! ci = Some of -> (non_virtual_align of | nvl_align nvldata);
nvl_offset_align : forall ci of, (nvl_offsets nvldata) ! ci = Some of -> forall co, (offsets ld) ! ci = Some co -> (non_virtual_align co | of);

Specification of nvl_nvebo non-virtual empty base offsets

nvl_nvebo_prop : forall b o, (In (b, o) (nvl_nvebo nvldata) <-> exists ci, exists of, (nvl_offsets nvldata) ! ci = Some of /\ non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b (o - of));

Specification of nvl_nvebo' non-virtual empty base offsets through empty direct bases

             nvl_nvebo'_prop : forall b o, (In (b, o) (nvl_nvebo' nvldata) <-> exists ci, exists of, (nvl_offsets nvldata) ! ci = Some of /\ is_empty hierarchy ci /\ non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b (o - of))
           }.

           End prop.

           Section Step.

             Variable nvldata : nvl.

           Hypothesis prop : nvl_prop nvldata.

Trying to assign an offset to the non-virtual direct base a of cilimit ld

           Variable a : ident.

           Variable q : list ident.

           Hypothesis Htodo : nvl_todo nvldata = a :: q.

           Hypothesis undef: (nvl_offsets nvldata) ! a = None.

           Let son : In (Class.Inheritance.Repeated, a) (Class.super h).

Proof.

Let Hlt : (Plt a (cilimit ld)).

Proof.

Let orig_offset : {o' | (offsets ld) ! a = Some o'}.

Proof.

Let o' := let (o', _) := orig_offset in o'.

Let Ho' : (offsets ld) ! a = Some o'.

Proof.

Let e0 : {e | (nvebo ld) ! a = Some e}.

Proof.

Let e := let (e, _) := e0 in e.

Let He : (nvebo ld) ! a = Some e.

Proof.

Let em := is_empty_dec hierarchy_wf a.

The offset nv_offset assigned to a is computed as follows:

if a is empty, and if the set e of non-virtual empty base offsets reachable from a is disjoint from nvl_nvebo the offsets of non-virtual empty base offsets so far, then nv_offsets = 0
otherwise, nv_offset is the least offset o multiple of the non-virtual alignment of a starting from nvl_nvds nvldata the non-virtual data size so far, and such that there is no conflict with non-virtual empty base offsets reachable through empty direct non-virtual bases, knowing that:
- there will be no conflict if o >= nvl_nvsize nvldata
- there will be no conflict with non-virtual empty base offsets reachable through non-empty direct non-virtual bases, as those latter are laid out completely disjointly (not only their data) from a. See LibPos for a definition of bounded_offset.

           Let f_empty x :=
             if In_dec (prod_eq_dec peq Z_eq_dec) x (nvl_nvebo nvldata)
               then true
               else false.

           Let cond :=
             if em
               then
                 match List.filter f_empty e with
                   | nil => true
                   | _ => false
                 end
               else false
                 .

           Let f z (x : _ * _) :=
             let (b, o) := x in
               if In_dec (prod_eq_dec peq Z_eq_dec) (b, z + o) (nvl_nvebo' nvldata) then true else false.

           Let f' z :=
             match List.filter (f z) e with
               | nil => true
               | _ => false
             end.

           Let align_pos : 0 < non_virtual_align o'.

Proof.

           Definition nv_offset :=
             if cond then 0 else
               let (z, _) := bounded_offset align_pos (nvl_nvds nvldata) (nvl_nvsize nvldata) f' in z.

            Lemma nv_offsets_non_overlap : forall ci co, (nvl_offsets nvldata) ! ci = Some co -> forall b bo, non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b bo -> forall bo', non_virtual_empty_base_offset Optim (offsets ld) hierarchy a b bo' -> co + bo <> nv_offset + bo'.

Proof.

Lemma nv_offset_low_bound : 0 <= nv_offset.

Proof.

Lemma nv_offset_align : (non_virtual_align o' | nv_offset).

Proof.

Lemma nv_offset_nonempty_low_bound : (is_empty hierarchy a -> False) -> nvl_nvds nvldata <= nv_offset.

Proof.

Let g := map_snd (key := ident) (fun o => nv_offset + o).

Update the data to assign nv_offset to the non-virtual base.

         Definition non_virtual_direct_base_layout_step : {
           nvldata' | nvl_prop nvldata' /\ nvl_todo nvldata' = q
         }.
           exists (
             make_nvl

remove a from nvl_todo = a :: q

assign nv_offset to a

(PTree.set a nv_offset (nvl_offsets nvldata))

add non-virtual empty base offsets of a to nvl_nvebo

(List.map g e ++ nvl_nvebo nvldata)

add non-virtual empty base offsets of a to nvl_nvebo' if a is empty

((if em then List.map g e else nil) ++ nvl_nvebo' nvldata)

update data size if a is not empty

(if em then nvl_nvds nvldata else (nv_offset + non_virtual_size o'))

update size to the max

(if Z_le_dec (nv_offset + non_virtual_size o') (nvl_nvsize nvldata) then (nvl_nvsize nvldata) else (nv_offset + non_virtual_size o'))

keep the same primary base

(nvl_pbase nvldata)

update alignment to the least common multiple

(lcm (nvl_align nvldata) (non_virtual_align o'))
).

Proof.

End Step.

Finalization: if at some point, some direct non-virtual bases have already been assigned an offset, then the following lemma tells how to deal with all the remaining direct non-virtual bases

    Definition non_virtual_direct_base_layout_end :
      forall nvldata, nvl_prop nvldata -> {
        nvldata' | nvl_prop nvldata' /\ nvl_todo nvldata' = nil
      }.

Proof.

Initialization: there are three cases.

If there is a dynamic direct non-virtual base, then choose it as the primary base
Otherwise, if the class is dynamic, then explicitly reserve its dynamic type data
Otherwise, start with an empty layout

    Section Init.

      Let f (x : _ * ident) :=
        match x with
          | (Class.Inheritance.Repeated, b) => b :: nil
          | _ => nil
        end.

      Let nvbases := flatten (map f (Class.super h)).

      Let g b :=
        if is_dynamic_dec hierarchy_wf b then true else false
          .

      Let dynbases := filter g nvbases.

There is a direct non-virtual primary base a of cilimit ld: choose it as the primary base

     Section Primary_base.

      Variable a : ident.

      Variable q : list ident.

      Hypothesis some_dynbase : dynbases = a :: q.

      Lemma nveb_inh : In (Class.Inheritance.Repeated, a) (Class.super h).

Proof.

Let inh := nveb_inh.

Lemma nveb_dyn : is_dynamic hierarchy a.

Proof.

Let dyn := nveb_dyn.

Let Hlt : Plt a (cilimit ld).

Proof.

Let of'0 : {of' | (offsets ld) ! a = Some of'}.

Proof.

Let of' := let (of', _) := of'0 in of'.

Let Hof' : (offsets ld) ! a = Some of'.

Proof.

Let e0 : {e | (nvebo ld) ! a = Some e}.

Proof.

Let e := let (e, _) := e0 in e.

Let He : (nvebo ld) ! a = Some e.

Proof.

Let ne : is_empty hierarchy a -> False.

Proof.

      Definition nvl_init_some_primary_base : {
        nv | nvl_prop nv
      }.
       exists (
         make_nvl
         nvbases
         (PTree.set a 0 (PTree.empty _))
         e
         nil
         (non_virtual_size of')
         (non_virtual_size of')
         (Some a)
         (non_virtual_align of')
       ).

Proof.

End Primary_base.

The class is dynamic, but has no primary base

   Section No_primary_base.

     Section Dynamic.

       Hypothesis dyn : is_dynamic hierarchy (cilimit ld).

     Definition nvl_init_dynamic_no_primary_base : {
        nv | nvl_prop nv
      }.
       exists (
         make_nvl
         nvbases
         (PTree.empty _)
         nil
         nil
         (dynamic_type_data_size PF)
         (dynamic_type_data_size PF)
         None
         (dynamic_type_data_align PF)
       ).

Proof.

End Dynamic.

The class is not dynamic

  Section Non_dynamic.

       Hypothesis dyn : is_dynamic hierarchy (cilimit ld) -> False.

     Definition nvl_init_non_dynamic : {
        nv | nvl_prop nv
      }.
       exists (
         make_nvl
         nvbases
         (PTree.empty _)
         nil
         nil
         0
         1
         None
         1
       ).

Proof.

  End Non_dynamic.

  End No_primary_base.

Finally, pack all together

  Definition non_virtual_direct_base_layout : {
    nvldata | nvl_prop nvldata /\ nvl_todo nvldata = nil
  }.

Proof.

End Init.

End Non_virtual_direct_base_layout.

Let nvldata be the layout of direct non-virtual bases. Then, nvl_nvdsize nvldata, the data size so far before laying out fields, is the field boundary.

Let nvldata := let (k, _) := non_virtual_direct_base_layout in k.

Let H_nvldata : nvl_prop nvldata.

Proof.

Let H_nvldata_2 : nvl_todo nvldata = nil.

Proof.

Layout of fields

Section Field_layout.

fl_todo: the list of fields to which an offset has not yet been assigned
fl_offsets: the mapping between fields and offsets
fl_ebo: the set of empty base offsets reachable through a field that has already been assigned an offset
fl_nvds: the non-virtual data size so far.
fl_nvsize: the non-virtual size so far.
fl_align: the non-virtual alignment so far.

         Record fl : Type := make_fl {
           fl_todo : list (FieldSignature.t A);
           fl_offsets : list (FieldSignature.t A * Z);
           fl_ebo : list (ident * Z);
           fl_nvds : Z;
           fl_nvsize : Z;
           fl_align : Z
         }.

         Section prop.

           Variable fldata : fl.

           Record fl_prop : Prop := fl_intro {

Guard

fl_exist : forall fs, (In fs (Class.fields h) <-> (assoc (FieldSignature.eq_dec (A := A)) fs (fl_offsets fldata) <> None \/ In fs (fl_todo fldata)));

C11

fl_data_low_bound : nvl_nvds nvldata <= fl_nvds fldata;

Additional invariant on non-virtual data size and non-virtual size (including C2)

fl_data_size : fl_nvds fldata <= fl_nvsize fldata;

Helper for C1

fl_size_low_bound : nvl_nvsize nvldata <= fl_nvsize fldata;

C8 generalized to all fields

fl_low_bound : forall fs of, assoc (FieldSignature.eq_dec (A := A)) fs (fl_offsets fldata) = Some of -> nvl_nvds nvldata <= of;

C9 generalized to all fields, and to their whole sizes (not only their data)

fl_non_overlap : forall fs1 o1, assoc (FieldSignature.eq_dec (A := A)) fs1 (fl_offsets fldata) = Some o1 -> forall fs2 o2, assoc (FieldSignature.eq_dec (A := A)) fs2 (fl_offsets fldata) = Some o2 -> fs1 <> fs2 -> forall s1, field_size PF (offsets ld) fs1 = Some s1 -> forall s2, field_size PF (offsets ld) fs2 = Some s2 -> o1 + s1 <= o2 \/ o2 + s2 <= o1;

C24

fl_disjoint_empty_bases : forall fs1 o1, assoc (FieldSignature.eq_dec (A := A)) fs1 (fl_offsets fldata) = Some o1 -> forall ci1 p1, FieldSignature.type fs1 = FieldSignature.Struct ci1 p1 -> forall z1, 0 <= z1 -> z1 < Zpos p1 -> forall so1, (offsets ld) ! ci1 = Some so1 -> forall b bo1, empty_base_offset Optim (offsets ld) hierarchy ci1 b bo1 -> forall ci2 o2, (nvl_offsets nvldata) ! ci2 = Some o2 -> forall bo2, non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci2 b bo2 -> o1 + z1 * size so1 + bo1 <> o2 + bo2;

Helper for C2 and C10 (C10 being generalized to the whole sizes)

fl_high_bound : forall fs of, assoc (FieldSignature.eq_dec (A := A)) fs (fl_offsets fldata) = Some of -> forall s, field_size PF (offsets ld) fs = Some s -> of + s <= fl_nvds fldata;

Guard

fl_align_pos : 0 < fl_align fldata;

Helper for C15 and C16

fl_align_nvl : (nvl_align nvldata | fl_align fldata);

C14

fl_align_prop : forall fs, assoc (FieldSignature.eq_dec (A := A)) fs (fl_offsets fldata) <> None -> forall al, field_align PF (offsets ld) fs = Some al -> (al | fl_align fldata);
fl_offset_align : forall fs fo, assoc (FieldSignature.eq_dec (A := A)) fs (fl_offsets fldata) = Some fo -> forall al, field_align PF (offsets ld) fs = Some al -> (al | fo);

Specification of fl_ebo, the set of the empty base offsets reachable through a field of cilimit ld

             fl_ebo_prop : forall b o, (In (b, o) (fl_ebo fldata) <-> exists fs, exists of, assoc (FieldSignature.eq_dec (A := A)) fs (fl_offsets fldata) = Some of /\ exists ci, exists n, FieldSignature.type fs = FieldSignature.Struct ci n /\ exists i, 0 <= i /\ i < Zpos n /\ exists oo, (offsets ld) ! ci = Some oo /\ empty_base_offset Optim (offsets ld) hierarchy ci b (o - of - i * size oo))
           }.

           Hypothesis prop : fl_prop.

C25 can be actually proved, thanks to the fact that all fields (even empty) are laid out completely disjointly from each other

           Lemma fl_disjoint_field_empty_bases : forall fs1 o1, assoc (FieldSignature.eq_dec (A := A)) fs1 (fl_offsets fldata) = Some o1 -> forall ci1 p1, FieldSignature.type fs1 = FieldSignature.Struct ci1 p1 -> forall z1, 0 <= z1 -> z1 < Zpos p1 -> forall so1, (offsets ld) ! ci1 = Some so1 -> forall b bo1, empty_base_offset Optim (offsets ld) hierarchy ci1 b bo1 ->
             forall fs2 o2, assoc (FieldSignature.eq_dec (A := A)) fs2 (fl_offsets fldata) = Some o2 -> forall ci2 p2, FieldSignature.type fs2 = FieldSignature.Struct ci2 p2 -> forall z2, 0 <= z2 -> z2 < Zpos p2 -> forall so2, (offsets ld) ! ci2 = Some so2 -> forall bo2, empty_base_offset Optim (offsets ld) hierarchy ci2 b bo2 ->
               fs1 <> fs2 ->
               o1 + z1 * size so1 + bo1 <> o2 + z2 * size so2 + bo2.

Proof.

           End prop.

           Section Step.

             Variable fldata : fl.

           Hypothesis prop : fl_prop fldata.

Trying to assign an offset to the field fs0 of cilimit ld

           Variable fs0 : FieldSignature.t A.

           Variable q : list (FieldSignature.t A).

           Hypothesis Htodo : fl_todo fldata = fs0 :: q.

           Hypothesis undef: assoc (FieldSignature.eq_dec (A := A)) fs0 (fl_offsets fldata) = None.

             Let son : In fs0 (Class.fields h).

Proof.

fs0 is a structure array field of type a

           Section Struct.

             Variable a : ident.

             Variable na : positive.

             Hypothesis Hstruct : FieldSignature.type fs0 = FieldSignature.Struct a na.

           Let Hlt : (Plt a (cilimit ld)).

Proof.

Definition fstruct_orig_offset : {o' | (offsets ld) ! a = Some o'}.

Proof.

Let o' := let (o', _) := fstruct_orig_offset in o'.

Let Ho' : (offsets ld) ! a = Some o'.

Proof.

Definition fstruct_e0 : {e | (ebo ld) ! a = Some e}.

Proof.

Let e := let (e, _) := fstruct_e0 in e.

Let He : (ebo ld) ! a = Some e.

Proof.

fstruct_e'0_aux constructs the union of all << j * sizeof(a) + ebo(a) >> for each j such that 0 <= j < n

           Definition fstruct_e'0_aux : forall k, 0 <= k -> 0 <= k <= Zpos na ->
             forall l, (forall b o, In (b, o) l <-> exists j, 0 <= j /\ j < Zpos na - k /\ In (b, o - j * size o') e) ->
               {l | forall b o, In (b, o) l <-> exists j, 0 <= j /\ j < Zpos na /\ In (b, o - j * size o') e}.

Proof.

Definition fstruct_e'0 :
{l | forall b o, In (b, o) l <-> exists j, 0 <= j /\ j < Zpos na /\ In (b, o - j * size o') e}.

Proof.

Let e' := let (e', _) := fstruct_e'0 in e'.

Let He' : forall b o, In (b, o) e' <-> exists j, 0 <= j /\ j < Zpos na /\ In (b, o - j * size o') e.

Proof.

The offset fl_offset to be assigned to the field, is the least z no less than the current data size, and aligned to the alignment of a (the type of the structure), with no conflicts between the empty base offsets reachable from the field, and the non-virtual empty base offsets accessible from an empty non-virtual base, knowing that:

there will be no conflict if o >= fl_nvsize nvldata
there will be no conflict with non-virtual empty base offsets reachable through non-empty direct non-virtual bases, as those latter are laid out completely disjointly (not only their data) from fields.

             Let f z (x : _ * _) :=
               let (b, o) := x in
                 if In_dec (prod_eq_dec peq Z_eq_dec) (b, z + o) (nvl_nvebo' nvldata) then true else false.

             Definition fstruct_off0 : {z | fl_nvds fldata <= z /\ (align o' | z) /\ (fl_nvsize fldata <= z \/ List.filter (f z) e' = nil)}.

Proof.

Let off := let (z, _) := fstruct_off0 in z.

Let Hoff : fl_nvds fldata <= off /\ (align o' | off) /\ (fl_nvsize fldata <= off \/ List.filter (f off) e' = nil).

Proof.

Lemma fl_offsets_non_overlap_aux : forall ci co, (nvl_offsets nvldata) ! ci = Some co -> forall b bo, non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b bo -> forall i, 0 <= i -> i < Zpos na -> forall bo', empty_base_offset Optim (offsets ld) hierarchy a b bo' -> co + bo <> off + i * size o' + bo'.

Proof.

           Definition fl_offset := off.

           Lemma fl_offset_prop : fl_nvds fldata <= fl_offset /\ (align o' | fl_offset) /\ (fl_nvsize fldata <= fl_offset \/ List.filter (f fl_offset) e' = nil).
           Proof Hoff.

           Lemma fl_offsets_non_overlap : forall ci co, (nvl_offsets nvldata) ! ci = Some co -> forall b bo, non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b bo -> forall i, 0 <= i -> i < Zpos na -> forall bo', empty_base_offset Optim (offsets ld) hierarchy a b bo' -> co + bo <> fl_offset + i * size o' + bo'.
           Proof fl_offsets_non_overlap_aux.

           Let g := map_snd (key := ident) (fun o => fl_offset + o).

           Definition field_layout_step_struct : {
             fldata' | fl_prop fldata' /\ fl_todo fldata' = q
           }.
           exists (
             make_fl

remove fs0 from fl_todo fldata = fs0 :: q

assign fl_offset to fs0

((fs0, fl_offset) :: (fl_offsets fldata))

add the empty base offsets reachable from fs0

(List.map g e' ++ fl_ebo fldata)

update the data size

(fl_offset + Zpos na * size o')

update the size to the max

(if Z_le_dec (fl_offset + Zpos na * size o') (fl_nvsize fldata) then (fl_nvsize fldata) else (fl_offset + Zpos na * size o'))

update the alignment to the least common multiple

(lcm (fl_align fldata) (align o'))
).

Proof.

End Struct.

General case

    Definition field_layout_step : {
      fldata' | fl_prop fldata' /\ fl_todo fldata' = q
    }.

case struct: use the results of section Struct above

case_eq (FieldSignature.type fs0); eauto using field_layout_step_struct.

only case scalar is left

      intros.
      destruct (incr_align (typ_align_positive PF ( t)) (fl_nvds fldata)).
      destruct a.
      exists (
        make_fl
        q
        ((fs0, x) :: fl_offsets fldata)
        (fl_ebo fldata)
        (x + typ_size PF (t))
        (if Z_le_dec (x + typ_size PF ( t)) (fl_nvsize fldata) then (fl_nvsize fldata) else (x + typ_size PF ( t)))
        (lcm (typ_align PF ( t)) (fl_align fldata))
      ).

Proof.

End Step.

Finally, pack all cases together

    Definition field_layout : {
      fldata' | fl_prop fldata' /\ fl_todo fldata' = nil
    }.

Proof.

End Field_layout.

  Let fldata := (let (f, _) := field_layout in f).

  Let H_fldata : fl_prop fldata.

Proof.

Let H_fldata_2 : fl_todo fldata = nil.

Proof.

At this point, all non-virtual layout is done. The field boundary is nvl_nvdsize nvldata, whereas all other non-virtual values are defined in fldata.

nvebo0 is the set of all non-virtual empty base offsets, except the offset of cilimit ld itself.

  Let nvebo0 := nvl_nvebo nvldata ++ fl_ebo fldata.

  Lemma nvebo0_incl : forall b o,
    In (b, o) nvebo0 -> 0 <= o < fl_nvsize fldata.

Proof.

  Lemma nvebo0_data_incl : forall b o,
    In (b, o) nvebo0 ->
    (In (b, o) (nvl_nvebo' nvldata) -> False) ->
    0 <= o < fl_nvds fldata.

Proof.

Nvebo is the set of all non-virtual empty base offsets, including the offset of cilimit ld itself if it is empty.

Let Nvebo := (if is_empty_dec hierarchy_wf (cilimit ld) then (cons (cilimit ld, 0) nil) else nil) ++ nvebo0.

Virtual base layout

In this algorithm, we do not consider generalized virtual bases, but only virtual bases. Indeed, the non-virtual parts of the virtual bases of cilimit ld make the conditions of 4.5 hold, which is not yet known for cilimit ld itself. So we have to treat the non-virtual part of the class differently from the non-virtual parts of its virtual bases.

  Section Virtual_base_layout.

         Record vl : Set := make_vl {
           vl_todo : list ident;
           vl_offsets : PTree.t Z;
           vl_nvebo : list (ident * Z);
           vl_nvebo' : list (ident * Z);
           vl_ds : Z;
           vl_size : Z;
           vl_align : Z
         }.

         Section prop.

           Variable vldata : vl.

           Record vl_prop : Prop := vl_intro {

Guard

vl_exist : forall ci, (is_virtual_base_of hierarchy ci (cilimit ld) <-> ((vl_offsets vldata) ! ci <> None \/ In ci (vl_todo vldata)));

C13 for the class itself

vl_data_low_bound : fl_nvds fldata <= vl_ds vldata;

C3 for the class itself

vl_size_low_bound : fl_nvsize fldata <= vl_size vldata;

vl_data_size : vl_ds vldata <= vl_size vldata;

Guard

vl_low_bound : forall ci of, (vl_offsets vldata) ! ci = Some of -> 0 <= of;

C12 between the class itself and one of its virtual bases, but not generalized to the non-virtual size of the class itself

vl_nonempty_low_bound : forall ci, (is_empty hierarchy ci -> False) -> forall of, (vl_offsets vldata) ! ci = Some of -> fl_nvds fldata <= of;

C12 between two virtual bases, generalized to their non-virtual sizes

vl_nonempty_non_overlap : forall ci1 o1, (vl_offsets vldata) ! ci1 = Some o1 -> (is_empty hierarchy ci1 -> False) -> forall ci2 o2, (vl_offsets vldata) ! ci2 = Some o2 -> (is_empty hierarchy ci2 -> False) -> ci1 <> ci2 -> forall of1, (offsets ld) ! ci1 = Some of1 -> forall of2, (offsets ld) ! ci2 = Some of2 -> o1 + non_virtual_size of1 <= o2 \/ o2 + non_virtual_size of2 <= o1;

C26 between two virtual bases

vl_disjoint_empty_bases : forall ci1 o1, (vl_offsets vldata) ! ci1 = Some o1 -> forall ci2 o2, (vl_offsets vldata) ! ci2 = Some o2 -> ci1 <> ci2 -> forall b bo1, non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci1 b bo1 -> forall bo2, non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci2 b bo2 -> o1 + bo1 <> o2 + bo2;

C26 between the class itself and one of its virtual bases

vl_disjoint_empty_bases_main : forall ci o, (vl_offsets vldata) ! ci = Some o -> forall b bo, non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b bo -> In (b, o + bo) Nvebo -> False;

C13 for a virtual base

vl_nonempty_high_bound : forall ci, (is_empty hierarchy ci -> False) -> forall of, (vl_offsets vldata) ! ci = Some of -> forall o', (offsets ld) ! ci = Some o' -> of + non_virtual_size o' <= vl_ds vldata;

C3 for a virtual base

vl_high_bound : forall ci, forall of, (vl_offsets vldata) ! ci = Some of -> forall o', (offsets ld) ! ci = Some o' -> of + non_virtual_size o' <= vl_size vldata;

Guard

vl_align_pos : 0 < vl_align vldata;

C17 for the class itself

vl_align_field : (fl_align fldata | vl_align vldata);

C17 for a virtual base

vl_align_prop : forall ci, (vl_offsets vldata) ! ci <> None -> forall of, (offsets ld) ! ci = Some of -> (non_virtual_align of | vl_align vldata);
vl_offset_align : forall ci of, (vl_offsets vldata) ! ci = Some of -> forall co, (offsets ld) ! ci = Some co -> (non_virtual_align co | of);

Specification of the set vl_nvebo of non-virtual empty base offsets accessible from some virtual base.

vl_nvebo_prop : forall b o, (In (b, o) (vl_nvebo vldata) <-> exists ci, exists of, (vl_offsets vldata) ! ci = Some of /\ non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b (o - of));

Specification of the set vl_nvebo' of non-virtual empty base offsets accessible from some empty virtual base.

             vl_nvebo'_prop : forall b o, (In (b, o) (vl_nvebo' vldata) <-> exists ci, exists of, (vl_offsets vldata) ! ci = Some of /\ is_empty hierarchy ci /\ non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b (o - of))
           }.

           End prop.

           Section Step.

             Variable vldata : vl.

           Hypothesis prop : vl_prop vldata.

Trying to assign an offset to the virtual base a of cilimit ld

           Variable a : ident.

           Variable q : list ident.

           Hypothesis Htodo : vl_todo vldata = a :: q.

           Hypothesis undef: (vl_offsets vldata) ! a = None.

           Let son : is_virtual_base_of hierarchy a (cilimit ld).

Proof.

Let Hlt : (Plt a (cilimit ld)).

Proof.

Definition v_orig_offset : {o' | (offsets ld) ! a = Some o'}.

Proof.

Let o' := let (o', _) := v_orig_offset in o'.

Let Ho' : (offsets ld) ! a = Some o'.

Proof.

Let e0 : {e | (nvebo ld) ! a = Some e}.

Proof.

Let e := let (e, _) := e0 in e.

Let He : (nvebo ld) ! a = Some e.

Proof.

Let cilimit_nonempty : is_empty hierarchy (cilimit ld) -> False.

Proof.

Corollary nvebo_eq_nvebo0 : Nvebo = nvebo0.

Proof.

Let em := is_empty_dec hierarchy_wf a.

The offset v_offset assigned to a is computed as follows:

if a is empty, and if the set e of non-virtual empty base offsets reachable from a is disjoint from nvebo0 the set of non-virtual empty base offsets of the class, and from vl_nvebo the set of empty base offsets so far, then nv_offsets = 0
otherwise, v_offset is the least offset o multiple of the non-virtual alignment of a starting from vl_ds vldata the data size so far, and such that there is no conflict with empty base offsets reachable through empty virtual bases or empty direct non-virtual bases, knowing that:
- there will be no conflict if o >= vl_size nvldata
- there will be no conflict with non-virtual empty base offsets reachable through fields, non-empty direct non-virtual bases, or non-empty virtual bases, as those latter are laid out completely disjointly (not only their data) from a. See LibPos for a definition of bounded_offset.

           Let f_empty x :=
             if In_dec (prod_eq_dec peq Z_eq_dec) x nvebo0
               then true
               else
                 if In_dec (prod_eq_dec peq Z_eq_dec) x (vl_nvebo vldata)
                   then true
                   else false.

           Let cond :=
             if em
               then
                 match List.filter f_empty e with
                   | nil => true
                   | _ => false
                 end
               else false
                 .

           Let f z (x : _ * _) :=
             let (b, o) := x in
               if In_dec (prod_eq_dec peq Z_eq_dec) (b, z + o) (nvl_nvebo' nvldata)
                 then true
                 else if In_dec (prod_eq_dec peq Z_eq_dec) (b, z + o) (vl_nvebo' vldata)
                   then true
                   else false.

           Let f' z :=
             match List.filter (f z) e with
               | nil => true
               | _ => false
             end.

           Let align_pos : 0 < non_virtual_align o'.

Proof.

           Definition v_offset :=
             if cond then 0 else
               let (z, _) := bounded_offset align_pos (vl_ds vldata) (vl_size vldata) f' in z.

            Lemma v_offsets_non_overlap : forall ci co, (vl_offsets vldata) ! ci = Some co -> forall b bo, non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b bo -> forall bo', non_virtual_empty_base_offset Optim (offsets ld) hierarchy a b bo' -> co + bo <> v_offset + bo'.

Proof.

Lemma v_offsets_non_overlap_main : forall b bo', non_virtual_empty_base_offset Optim (offsets ld) hierarchy a b bo' -> In (b, v_offset + bo') Nvebo -> False.

Proof.

Lemma v_offset_low_bound : 0 <= v_offset.

Proof.

Lemma v_offset_align : (non_virtual_align o' | v_offset).

Proof.

Lemma v_offset_nonempty_low_bound : (is_empty hierarchy a -> False) -> vl_ds vldata <= v_offset.

Proof.

         Let g := map_snd (key := ident) (fun o => v_offset + o).

         Definition virtual_base_layout_step : {
           vldata' | vl_prop vldata' /\ vl_todo vldata' = q
         }.
           exists (
             make_vl

remove a from vl_todo vldata = a :: q

assign v_offset to a

(PTree.set a v_offset (vl_offsets vldata))

add the non-virtual empty base offsets of a to the empty base offsets of cilimit ld

(List.map g e ++ vl_nvebo vldata)

add the non-virtual empty base offsets of a to the empty base offsets of cilimit ld reachable through an empty virtual base, if a is empty

((if em then List.map g e else nil) ++ vl_nvebo' vldata)

update the data size if a is not empty

(if em then vl_ds vldata else (v_offset + non_virtual_size o'))

update the size to the max

(if Z_le_dec (v_offset + non_virtual_size o') (vl_size vldata) then (vl_size vldata) else (v_offset + non_virtual_size o'))

update the alignment to the least common multiple

(lcm (vl_align vldata) (non_virtual_align o'))
).

Proof.

End Step.

Finally, lay out all the virtual bases

Definition vbases_aux : {l | forall x, In x l <-> is_virtual_base_of hierarchy x (cilimit ld)}.

Proof.

Let vbases := let (v, _) := vbases_aux in v.

Let H_vbases : forall x, In x vbases <-> is_virtual_base_of hierarchy x (cilimit ld).

Proof.

  Definition virtual_base_layout : {
    vldata | vl_prop vldata /\ vl_todo vldata = nil
  }.

Proof.

  End Virtual_base_layout.

  Let vldata := let (v, _) := virtual_base_layout in v.

  Let H_vldata : vl_prop vldata.

Proof.

Let H_vldata_2 : vl_todo vldata = nil.

Proof.

Finalization and proof of correctness

Now, round the size up to the nearest multiple of the alignment.

  Let size0 := incr_align (vl_align_pos H_vldata) (vl_size vldata).

  Let size := let (s, _) := size0 in s.

  Let H_size : vl_size vldata <= size.

Proof.

Let H_size_2 : (vl_align vldata | size).

Proof.

Construction of the layout data as expected in 4.2

  Let o' := (LayoutConstraints.make
    (nvl_pbase nvldata)
    (nvl_offsets nvldata)
    (nvl_nvds nvldata)
    (fl_offsets fldata)
    (fl_nvds fldata)
    (fl_nvsize fldata)
    (fl_align fldata)
    (PTree.set (cilimit ld) 0 (vl_offsets vldata))
    (vl_ds vldata)
    size
    (vl_align vldata)
  ).

  Definition offsets' := PTree.set (cilimit ld) o' (offsets ld).

  Lemma offsets'_eq : forall ci', Plt ci' (cilimit ld) ->
    offsets' ! ci' = (offsets ld) ! ci'.

Proof.

  Lemma offsets_preserve_old : forall ci,
    Plt ci (cilimit ld) ->
    forall o, offsets' ! ci = Some o ->
      class_level_prop Optim PF offsets' hierarchy ci o.

Proof.

Lemma offsets'_defined : offsets' ! (cilimit ld) = Some o'.

Proof.

  Lemma nvl_offsets_lt : forall bi of,
    (nvl_offsets nvldata) ! bi = Some of ->
    Plt bi (cilimit ld).

Proof.

  Lemma nvl_offsets_offsets' : forall bi of,
    (nvl_offsets nvldata) ! bi = Some of ->
    offsets' ! bi = (offsets ld) ! bi.

Proof.

  Lemma fl_offsets_offsets' : forall f of,
    assoc (FieldSignature.eq_dec (A := A)) f (fl_offsets fldata) = Some of ->
    forall ci n, FieldSignature.type f = FieldSignature.Struct ci n ->
      offsets' ! ci = (offsets ld) ! ci.

Proof.

  Lemma vl_offsets_offsets' : forall bi of,
    (vl_offsets vldata) ! bi = Some of ->
    offsets' ! bi = (offsets ld) ! bi.

Proof.

The proof that the new offsets computed for the current class satisfy the soundness conditions

Lemma offsets'_preserve :
class_level_prop Optim PF offsets' hierarchy (cilimit ld) o'.

Proof.

Lemma non_virtual_empty_base_offset_old : forall ci,
  Plt ci (cilimit ld) -> forall b o,
    non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b o ->
    non_virtual_empty_base_offset Optim offsets' hierarchy ci b o.

Proof.

Lemma empty_base_offset_old : forall ci,
  Plt ci (cilimit ld) -> forall b o,
    empty_base_offset Optim (offsets ld) hierarchy ci b o ->
    empty_base_offset Optim offsets' hierarchy ci b o.

Proof.

Lemma disjoint_empty_base_offsets_old : forall ci,
  Plt ci (cilimit ld) -> forall of,
    offsets' ! ci = Some of ->
    disjoint_empty_base_offsets Optim offsets' hierarchy ci of.

Proof.

Lemma non_virtual_empty_base_offset_new : forall ci,
  Plt ci (cilimit ld) -> forall b o,
    non_virtual_empty_base_offset Optim offsets' hierarchy ci b o ->
    non_virtual_empty_base_offset Optim (offsets ld) hierarchy ci b o.

Proof.

Lemma empty_base_offset_new : forall ci,
  Plt ci (cilimit ld) -> forall b o,
    empty_base_offset Optim offsets' hierarchy ci b o ->
    empty_base_offset Optim (offsets ld) hierarchy ci b o.

Proof.

Lemma Nvebo_prop : forall b o, In (b, o) Nvebo <-> non_virtual_empty_base_offset Optim offsets' hierarchy (cilimit ld) b o.

Proof.

Lemma disjoint_empty_base_offsets_new :
disjoint_empty_base_offsets Optim offsets' hierarchy (cilimit ld) o'.

Proof.

Let ld' := Ld
  offsets'
  (Psucc (cilimit ld))
  (PTree.set (cilimit ld) (Nvebo ++ vl_nvebo vldata) (ebo ld))
  (PTree.set (cilimit ld) Nvebo (nvebo ld))
.

The proof of the stronger invariant of the algorithm

Lemma step' : prop hierarchy ld'.

Proof.

Definition layout_step_defined : {
ld'0 | prop hierarchy ld'0 /\ cilimit ld'0 = Psucc (cilimit ld)
}.
exists ld'.

Proof.

End Def.

What to do if cilimit ld is not an identifier of a defined class

Section Undef.

Hypothesis undef : hierarchy ! (cilimit ld) = None.

Definition layout_step_undefined : {
  ld'0 | prop hierarchy ld'0 /\ cilimit ld'0 = Psucc (cilimit ld)
}.
  exists (Ld
    (offsets ld)
    (Psucc (cilimit ld))
    (PTree.set (cilimit ld) nil (ebo ld))
    (PTree.set (cilimit ld) nil (nvebo ld))
  ); simpl.

Proof.

End Undef.

Definition layout_step : {
ld'0 | prop hierarchy ld'0 /\ cilimit ld'0 = Psucc (cilimit ld)
}.

Proof.

End Step.

Packing all together

Definition empty_layout : {
  ld'0 | prop hierarchy ld'0 /\ cilimit ld'0 = xH
}.
  exists (Ld
    (PTree.empty _)
    xH
    (PTree.empty _)
    (PTree.empty _)
  ); simpl.

Proof.

Let max0 := max_index hierarchy.

Let max := let (m, _) := max0 in m.

Let H_max : forall j, hierarchy ! j <> None -> Plt j max.

Proof.

Definition layout_end : {
ld'0 | prop hierarchy ld'0 /\ cilimit ld'0 = max
}.

Proof.

Definition layout : {
  offsets |
    (forall ci, hierarchy ! ci <> None <-> offsets ! ci <> None) /\
    forall ci of, offsets ! ci = Some of -> (
      class_level_prop Optim PF (offsets ) hierarchy ci of /\
      disjoint_empty_base_offsets Optim (offsets) hierarchy ci of
    )
}.

Proof.

End Layout.

Require Import ConcreteOp.

Variable hierarchy : PTree.t (Class.t A).

Hypothesis Hhier : Well_formed_hierarchy.prop (A:=A) hierarchy.

Definition off := let (l, _) := layout Hhier in l.

Lemma ointro : (forall (ci : positive) (o : t A),
off ! ci = Some o ->
class_level_prop Optim PF off hierarchy ci o).

Proof.

Lemma oexist : (forall ci : positive, off ! ci <> None -> hierarchy ! ci <> None).

Proof.

Lemma oguard : (forall ci : positive, hierarchy ! ci <> None -> off ! ci <> None).

Proof.

Definition vtbl := vtables Hhier ointro oexist oguard.

Theorem preservation : forall (NO : NATIVEOP A) (psize palign : Z)
         (MEM : MEMORY PF psize palign)
          (objects : ident -> option Z)
         (s : state NO (Value.t A) (source_specific_stmt A) (Globals.t A))
         (t0 : state NO (memval A) target_specific_stmt (mem MEM)),
       invariant Optim (MEM:=MEM) off Hhier objects s t0 ->
       forall
         s' : state NO (Value.t A) (source_specific_stmt A) (Globals.t A),
       source_step Optim hierarchy s s' ->
       exists t' : state NO (memval A) target_specific_stmt (mem MEM),
         Relation_Operators.clos_trans
           (state NO (memval A) target_specific_stmt (mem MEM))
           (step vtbl (MEM:=MEM)) t0 t' /\
         invariant Optim (MEM:=MEM) off Hhier objects s' t'.

Proof.

End CVABI.

Module CommonVendorABI

Empty classes

Overview of the layout algorithm

Computed values

Invariant

Incremental layout

Layout of non-virtual direct bases

Layout of fields

Virtual base layout

Finalization and proof of correctness

What to do if cilimit ld is not an identifier of a defined class

Packing all together