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.
Require Import Dynamic.
Require Import DynamicWf.

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.

  constructor.
  inversion 1; congruence.
  inversion 1. intros until 1. replace c0 with c in * by congruence. rewrite H_no_fields; simpl; tauto.
  inversion 1. intros until 1. replace c0 with c in * by congruence. rewrite H_no_fields; simpl; tauto.
  inversion 1; intros; subst. replace c0 with c in * by congruence.
   destruct h.
    eauto.
    destruct (H_no_virtual_bases b).
    assumption.
Qed.

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

Proof.

  induction 1 ; inversion 1 ; subst ; replace c0 with c in * by congruence.
  destruct H_methods.
  destruct H0.
  eauto.
  eauto.
  destruct h ; eauto.
Qed.

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.

  intros.
  revert H.
  induction H0.
   inversion 1; subst.
   replace c0 with c in * by congruence.
   eauto.
   intros.
   apply IHis_virtual_base_of.
   inversion H2.
   subst.
   replace c0 with c in * by congruence.
   destruct h'.
    eauto.
   apply False_rect.
   eauto.
Qed.

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

Proof.

induction i using (well_founded_induction Plt_wf).
rename H into IHi.
case_eq (hierarchy ! i).
  intros c Hc.
  case_eq (Class.fields c).
   intros.
   case_eq (List.filter (Method.virtual (A := A)) (Class.methods c)).
   intros.
   pose (f := fun (x : _ * ident) =>
     match x with
       | (Class.Inheritance.Shared, _) => true
       | (Class.Inheritance.Repeated, j) =>
         match plt j i with
           | left Hlt =>
             if IHi _ Hlt then false else true
           | _ => false
         end
     end
   ).
   case_eq (filter f (Class.super c)).
    intros Hnil.
    left.
    econstructor.
    eassumption.
    assumption.

    intros.
    generalize (filter_In (Method.virtual (A := A)) m (Class.methods c)).
    rewrite H0.
    simpl.
    tauto.

    intros b Hb.
    generalize (filter_In f (Class.Inheritance.Shared, b) (Class.super c)).
    intros [_ Hb_abs].
    rewrite Hnil in Hb_abs.
    simpl in Hb_abs.
    apply Hb_abs.
    tauto.
    intros b Hb.
    generalize (filter_In f (Class.Inheritance.Repeated, b) (Class.super c)).
    intros [_ Hb_empty].
    rewrite Hnil in Hb_empty.
    simpl in Hb_empty.
    destruct (plt b i).
    destruct (IHi b p).
     assumption.
    destruct Hb_empty.
    tauto.
    destruct n.
    eauto using Well_formed_hierarchy.well_founded.
   intros p l Hp_aux.
   assert (In p (filter f (Class.super c))) as Hp.
   rewrite Hp_aux.
   auto.
   destruct p as (h, j).
   generalize (filter_In f (h, j) (Class.super c)).
   intros [Hp_destr _].
   generalize (Hp_destr Hp).
   intros [Hp_c Hp_f].
   right.
   intro Habs.
   inversion Habs.
   subst.
   replace c0 with c in * by congruence.
   unfold f in Hp_f.
   destruct h.
    destruct (plt j i).
     destruct (IHi j p).
      discriminate.
     destruct n.
     eauto.
    discriminate.
   eauto.

  intros.
  right.
  intro Habs.
  generalize (filter_In (Method.virtual (A := A)) t (Class.methods c)).
  rewrite H0.
  simpl.
  inversion Habs.
  replace c0 with c in * by congruence.
  generalize (H_no_virtual_methods t).
  tauto.

  intros ; right ; intro Habs ; inversion Habs ; congruence.
right ; intro Habs ; inversion Habs ; congruence.
Qed.

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.

         unfold virtual_bases.
         destruct Well_formed_hierarchy.virtual_bases.
         assumption.
       Qed.

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.

             destruct (nvl_exist prop a).
             apply H0.
             rewrite Htodo.
             auto.
           Qed.

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

Proof.

eauto using Well_formed_hierarchy.well_founded.
Qed.

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

Proof.

             assert ((offsets ld) ! a <> None) by eauto using offsets_exist, Well_formed_hierarchy.complete.
             case_eq ((offsets ld) ! a); try congruence.
             intros.
             repeat esplit.
           Qed.

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

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

Proof.

             unfold o'.
             destruct orig_offset.
             assumption.
           Qed.

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

Proof.

             generalize (nvebo_exist ( Hld) Hlt).
             case_eq ((nvebo ld) ! a); try congruence.
             intros.
             repeat esplit.
           Qed.

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

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

Proof.

             unfold e.
             destruct e0.
             assumption.
           Qed.

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.

exact (non_virtual_align_low_bound (offsets_intro Hld Ho')).
Qed.

           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.

              intros.
              unfold nv_offset.
              case_eq cond.
               unfold cond.
               case em; try congruence.
               case_eq (filter f_empty e); try congruence.
               intros.
               simpl.
               intro; subst.
               generalize (filter_In f_empty (b, co + bo) e).
               rewrite H2.
               simpl.
               destruct 1.
               apply H5.
               split.
               generalize (nvebo_prop Hld He b (co + bo)).
               tauto.
               unfold f_empty.
               case (In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) (nvl_nvebo nvldata)).
                trivial.
               intros.
               destruct n.
               destruct (nvl_nvebo_prop prop b (co + bo)).
               apply H7.
               esplit.
               esplit.
               split.
               eassumption.
               replace (co + bo - co) with bo by omega.
               assumption.
              intros _.
              destruct (bounded_offset align_pos (nvl_nvds nvldata) (nvl_nvsize nvldata) f').
              destruct a0.
              destruct H3.
              assert (Plt ci (cilimit ld)).
               destruct (nvl_exist prop ci).
               eapply Well_formed_hierarchy.well_founded.
               eauto.
               eauto.
               eapply H6.
               left.
               congruence.
              destruct (non_virtual_empty_base_offset_wf
               hierarchy_wf (offsets_intro ( Hld)) (offsets_guard ( Hld)) H0).
              assert ((offsets ld) ! b <> None).
               eapply offsets_exist.
               eauto.
               eauto using Ple_Plt_trans.
               assumption.
              case_eq ((offsets ld) ! b) ; try congruence.
              intros.
              generalize (non_virtual_empty_base_offset_incl hierarchy_wf
                 (offsets_intro ( Hld)) (offsets_guard ( Hld))
                 H1 H8 Ho').
              intros.
              assert (hierarchy ! ci <> None).
               destruct (nvl_exist prop ci).
               eapply Well_formed_hierarchy.complete.
               eauto.
               eassumption.
               eapply H12.
               left.
               congruence.
              assert ((offsets ld) ! ci <> None) by eauto using offsets_exist.
              case_eq ((offsets ld) ! ci); try congruence.
              intros.
              generalize (non_virtual_empty_base_offset_incl hierarchy_wf
                 (offsets_intro ( Hld)) (offsets_guard ( Hld))
                 H0 H8 H13).
              intros.
              destruct H4.
               generalize (nvl_high_bound prop H H13).
               omega.
              destruct (is_empty_dec hierarchy_wf ci).
               revert H4.
               unfold f'.
               case_eq (filter (f x) e); try congruence.
               intros.
               intro Habs.
               generalize (filter_In (f x) (b, bo') e).
               rewrite H4.
               simpl.
               destruct 1.
               apply H17.
               split.
               generalize (nvebo_prop Hld He b bo').
               tauto.
               rewrite <- Habs.
               assert (
                 (if In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) (nvl_nvebo' nvldata)
                   then true
                   else false) = true
               ).
                destruct (In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) (nvl_nvebo' nvldata)); try congruence.
                destruct n.
                generalize (nvl_nvebo'_prop prop b (co + bo)).
                destruct 1.
                apply H19.
                esplit.
                esplit.
                split.
                eassumption.
                split.
                assumption.
                replace (co + bo - co) with bo by omega.
                assumption.
               assumption.
              generalize (nvl_nonempty_high_bound prop n H H13).
              omega.
            Qed.

Lemma nv_offset_low_bound : 0 <= nv_offset.

Proof.

              unfold nv_offset.
              case cond.
               omega.
              destruct (bounded_offset align_pos (nvl_nvds nvldata) (nvl_nvsize nvldata) f').
              generalize (nvl_data_low_bound prop).
              omega.
            Qed.

Lemma nv_offset_align : (non_virtual_align o' | nv_offset).

Proof.

              unfold nv_offset.
              case cond.
               exists 0; omega.
              destruct (bounded_offset align_pos (nvl_nvds nvldata) (nvl_nvsize nvldata) f').
              tauto.
            Qed.

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

Proof.

              unfold nv_offset.
              unfold cond.
              case em.
               contradiction.
             destruct (bounded_offset align_pos (nvl_nvds nvldata) (nvl_nvsize nvldata) f').
             tauto.
            Qed.

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.

           split.
            inversion prop.
            constructor; simpl; try assumption.

            intro.
            destruct (nvl_exist0 ci).
            rewrite Htodo in H, H0.
            simpl in H, H0.
             destruct (peq ci a).
             subst.
             rewrite PTree.gss.
             split.
             intros.
             left; congruence.
             intros.
             assumption.
            rewrite PTree.gso.
            assert (a = ci -> False) by congruence.
            split; tauto.
           assumption.

            intros.
            rewrite PTree.gso.
            eauto.
            generalize (nvl_primary_base0 _ H).
            intros.
            congruence.

            case em; intro.
             assumption.
            generalize (non_virtual_size_positive (offsets_intro ( Hld) Ho')).
            generalize (nv_offset_low_bound).
            omega.

            intros.
            case em.
             eauto.
            intro.
            apply Zle_trans with (nvl_nvds nvldata).
             eauto.
            generalize (nv_offset_nonempty_low_bound n).
            generalize (non_virtual_size_positive (offsets_intro ( Hld) Ho')).
            omega.

            case em.
             intros.
             destruct (Z_le_dec (nv_offset + non_virtual_size o') (nvl_nvsize nvldata)).
              eauto.
             eapply Zle_trans with (nvl_nvsize nvldata).
              eauto.
             omega.
            intro.
            destruct (Z_le_dec (nv_offset + non_virtual_size o') (nvl_nvsize nvldata)).
             assumption.
            omega.

            destruct (Z_le_dec (nv_offset + non_virtual_size o') (nvl_nvsize nvldata)).
             assumption.
            apply Zlt_trans with (nvl_nvsize nvldata).
             assumption.
            omega.

            intros ? ?.
            destruct (peq ci a).
             subst.
             rewrite PTree.gss.
             injection 1; intros; subst of.
             exact nv_offset_low_bound.
            rewrite PTree.gso.
            eauto.
            assumption.

            intros ? ? ? ?.
            destruct (peq ci a).
             subst.
             rewrite PTree.gss.
             injection 1; intros; subst of.
             generalize (nv_offset_nonempty_low_bound H1).
             intros.
             apply Zle_trans with (nvl_nvds nvldata).
              eauto.
             assumption.
            rewrite PTree.gso; eauto.

          intros ? ?.
          destruct (peq ci1 a).
           subst.
           rewrite PTree.gss.
           injection 1; intro; subst o1.
           intros.
           rewrite PTree.gso in H1.
           generalize (nvl_nonempty_high_bound prop H2 H1 H5).
           generalize (nv_offset_nonempty_low_bound H0).
           omega.
           congruence.
          rewrite PTree.gso.
          intros ? ? ? ?.
          destruct (peq ci2 a).
           subst.
           rewrite PTree.gss.
           injection 1; intros; subst o2.
           generalize (nvl_nonempty_high_bound prop H0 H H5).
           generalize (nv_offset_nonempty_low_bound H3).
           omega.
           rewrite PTree.gso.
           eauto.
           assumption.
          assumption.

          intros ? ?.
          destruct (peq ci1 a).
           subst.
           rewrite PTree.gss.
           injection 1; intro; subst o1.
           intros.
           rewrite PTree.gso in H0.
           cut (o2 + bo2 <> nv_offset + bo1).
            congruence.
            eauto using nv_offsets_non_overlap.
           congruence.
          rewrite PTree.gso.
          intros ? ? ?.
          destruct (peq ci2 a).
           subst.
           rewrite PTree.gss.
           injection 1; intros; subst o2.
           eauto using nv_offsets_non_overlap.
          rewrite PTree.gso.
          eauto.
          assumption.
          assumption.

          intros ? ? ?.
          destruct (peq ci a).
           subst ci.
           rewrite PTree.gss.
           injection 1; intro; subst of.
           rewrite Ho'.
           injection 1; intro; subst o'0.
           case em.
            contradiction.
           intro; omega.
          rewrite PTree.gso.
          intros.
          eapply Zle_trans with (nvl_nvds nvldata).
          eauto.
          case em.
           intros; omega.
          intros.
          generalize (nv_offset_nonempty_low_bound n0).
          generalize (non_virtual_size_positive (offsets_intro ( Hld) Ho')).
          omega.
          assumption.

          intros ? ?.
          destruct (peq ci a).
           subst.
           rewrite PTree.gss.
           injection 1; intros; subst of.
           destruct ( Z_le_dec (nv_offset + non_virtual_size o') (nvl_nvsize nvldata)).
            congruence.
           replace o'0 with o' by congruence.
           omega.
          rewrite PTree.gso.
          intros.
          destruct ( Z_le_dec (nv_offset + non_virtual_size o') (nvl_nvsize nvldata)).
           eauto.
          apply Zle_trans with (nvl_nvsize nvldata).
           eauto.
          omega.
         assumption.

         apply lcm_positive.
         assumption.
         eauto using non_virtual_align_low_bound.

         intro.
         apply Zdivide_trans with (nvl_align nvldata).
         eauto.
         apply lcm_divides_left.

         intro.
         destruct (peq ci a).
          subst.
          intros.
          replace of with o' by congruence.
          apply lcm_divides_right.
          eauto using non_virtual_align_low_bound.
         rewrite PTree.gso.
         intros.
         apply Zdivides_trans with (nvl_align nvldata).
          eauto.
         apply lcm_divides_left.
         assumption.

         intros ? ?.
         destruct (peq ci a).
          subst.
          rewrite PTree.gss.
          injection 1; intro; subst of.
          rewrite Ho'.
          injection 1; intros; subst co.
          exact nv_offset_align.
         rewrite PTree.gso; eauto.

         intros.
         split.
         intros.
         destruct (in_app_or _ _ _ H).
          destruct (list_in_map_inv _ _ _ H0).
          destruct H1.
          unfold g in H1.
          unfold map_snd in H1.
          destruct x.
          injection H1; intros; subst.
          destruct (nvebo_prop ( Hld) He i z).
          exists a.
          exists nv_offset.
          rewrite PTree.gss.
          split.
          trivial.
          replace (nv_offset + z - nv_offset) with z by omega.
          auto.
         destruct (nvl_nvebo_prop0 b o).
         destruct (H1 H0).
         destruct H3.
         destruct H3.
         exists x.
         exists x0.
         rewrite PTree.gso.
         eauto.
         congruence.
        destruct 1.
        destruct H.
        destruct H.
        destruct (peq x a).
         subst.
         rewrite PTree.gss in H.
         injection H; intro; subst x0.
         apply in_or_app.
         left.
         replace (b, o) with (g (b, o - nv_offset)).
         apply in_map.
         destruct (nvebo_prop ( Hld) He b (o - nv_offset)).
         auto.
         simpl.
         f_equal.
         omega.
        rewrite PTree.gso in H.
        apply in_or_app.
        right.
        destruct (nvl_nvebo_prop0 b o).
         apply H2.
         eauto.
        assumption.

         intros.
         split.
          intros.
          destruct (in_app_or _ _ _ H).
           revert H0.
           case em.
            intros.
            destruct (list_in_map_inv _ _ _ H0).
            destruct H1.
            unfold g in H1.
            unfold map_snd in H1.
            destruct x.
            injection H1; intros; subst.
            destruct (nvl_nvebo'_prop prop i0 z).
            exists a.
            exists nv_offset.
            rewrite PTree.gss.
            split.
             trivial.
            split.
             assumption.
            replace (nv_offset + z - nv_offset) with z by omega.
            generalize (nvebo_prop Hld He i0 z).
            tauto.
           simpl; tauto.
          destruct (nvl_nvebo'_prop prop b o).
          destruct (H1 H0).
          destruct H3.
          exists x.
          exists x0.
          rewrite PTree.gso.
          assumption.
          destruct H3.
          destruct H4.
          congruence.
         destruct 1.
         destruct H.
         destruct H.
         destruct (peq x a).
          subst.
          rewrite PTree.gss in H.
          injection H; intro; subst x0.
          apply in_or_app.
          left.
          replace (b, o) with (g (b, o - nv_offset)).
          case em; intro.
           apply in_map.
           destruct (nvebo_prop ( Hld) He b (o - nv_offset)).
           tauto.
          destruct H0.
          contradiction.
          simpl.
          f_equal.
          omega.
         rewrite PTree.gso in H.
         apply in_or_app.
         right.
         destruct (nvl_nvebo'_prop0 b o).
         apply H2.
         eauto.
        assumption.

        simpl.
        trivial.

      Qed.

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.

      intro.
      var (nvl_todo nvldata).
      revert v nvldata H.
      induction v.
       intros.
       exists nvldata.
       split.
       assumption.
       assumption.
      intros.
      case_eq ((nvl_offsets nvldata) ! a).
       intros.
       apply (IHv (
         make_nvl
         v
         (nvl_offsets nvldata)
         (nvl_nvebo nvldata)
         (nvl_nvebo' nvldata)
         (nvl_nvds nvldata)
         (nvl_nvsize nvldata)
         (nvl_pbase nvldata)
         (nvl_align nvldata)
       )).
        reflexivity.
        inversion x.
        constructor; simpl; try trivial.
        intros.
        rewrite H in nvl_exist0.
        simpl in nvl_exist0.
        destruct (nvl_exist0 ci).
        split.
         destruct (peq a ci).
          subst.
          intros.
          left.
          congruence.
          tauto.
         tauto.

         intros.
        destruct (non_virtual_direct_base_layout_step x H).
         assumption.
        destruct a0.
        eauto.
      Qed.

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.

        destruct (filter_In g a nvbases).
        unfold dynbases in some_dynbase.
        rewrite some_dynbase in H.
        destruct (H (or_introl _ (refl_equal _))).
        destruct (member_flatten_elim H1).
        destruct H3.
        destruct (list_in_map_inv _ _ _ H3).
        destruct H5.
        destruct x0.
        subst.
        destruct t; simpl in H4; try contradiction.
        inversion H4; try contradiction.
        subst.
        assumption.
      Qed.

Let inh := nveb_inh.

Lemma nveb_dyn : is_dynamic hierarchy a.

Proof.

        destruct (filter_In g a nvbases).
        unfold dynbases in some_dynbase.
        rewrite some_dynbase in H.
        destruct (H (or_introl _ (refl_equal _))).
        unfold g in H2.
        destruct (is_dynamic_dec hierarchy_wf a).
         assumption.
        discriminate.
      Qed.

Let dyn := nveb_dyn.

Let Hlt : Plt a (cilimit ld).

Proof.

eauto using Well_formed_hierarchy.well_founded.
Qed.

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

Proof.

        assert ((offsets ld) ! a <> None) by eauto using offsets_exist, Well_formed_hierarchy.complete.
        case_eq ((offsets ld) ! a).
         intros.
         repeat esplit.
        contradiction.
      Qed.

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

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

Proof.

        unfold of'.
        destruct of'0.
        assumption.
      Qed.

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

Proof.

             generalize (nvebo_exist ( Hld) Hlt).
             case_eq ((nvebo ld) ! a); try congruence.
             intros.
             repeat esplit.
           Qed.

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

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

Proof.

             unfold e.
             destruct e0.
             assumption.
           Qed.

Let ne : is_empty hierarchy a -> False.

Proof.

eauto using dynamic_nonempty.
Qed.

      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.

     constructor; simpl.

     split.
     intros.
     right.
     unfold nvbases.
     eapply member_flatten_intro with (f (Class.Inheritance.Repeated, ci)).
     eapply in_map.
     assumption.
     simpl.
     auto.
     inversion 1.
      destruct (peq ci a).
       subst ci.
       assumption.
      rewrite PTree.gso in H0.
      rewrite PTree.gempty in H0.
      congruence.
      assumption.
      unfold nvbases in H0.
      destruct (member_flatten_elim H0).
      destruct H1.
      destruct (list_in_map_inv _ _ _ H1).
      destruct H3.
      subst x.
      destruct x0.
      destruct t; simpl in H2.
       inversion H2; try contradiction.
       congruence.
      contradiction.

      injection 1; intros; subst ci.
      rewrite PTree.gss.
      trivial.

      congruence.

      generalize (non_virtual_size_positive (offsets_intro (Hld) Hof')).
      omega.

      intros.
      generalize (own_fields_offset_dynamic_low_bound (offsets_intro ( Hld) Hof' ) dyn).
      generalize (non_virtual_data_size_own_fields_offset (offsets_intro ( Hld) Hof')).
      generalize (non_virtual_data_size_non_virtual_size Hld Hof').
      omega.

      omega.

      exact (non_virtual_size_positive (offsets_intro ( Hld) Hof' )).

      intros ? ?.
      destruct (peq ci a).
       subst ci.
       rewrite PTree.gss.
       injection 1; intros; subst of; omega.
       rewrite PTree.gso.
       rewrite PTree.gempty.
       congruence.
       assumption.

     congruence.

     intros ? ?.
     destruct (peq ci1 a).
      subst ci1.
      intros.
      rewrite PTree.gso in H1.
      rewrite PTree.gempty in H1.
      discriminate.
      congruence.
     rewrite PTree.gso.
     rewrite PTree.gempty.
     congruence.
     assumption.

     intros ? ?.
     destruct (peq ci1 a).
      subst ci1.
      intros.
      rewrite PTree.gso in H0.
      rewrite PTree.gempty in H0.
      discriminate.
      congruence.
     rewrite PTree.gso.
     rewrite PTree.gempty.
     congruence.
     assumption.

     intros ? ? ?.
     destruct (peq ci a).
      subst ci.
      rewrite PTree.gss.
      injection 1; intros; subst of.
      replace o' with of' by congruence.
      omega.
      rewrite PTree.gso.
      rewrite PTree.gempty.
      congruence.
      assumption.

      intros ? ?.
      destruct (peq ci a).
      subst ci.
      rewrite PTree.gss.
      injection 1; intros; subst of.
      replace o' with of' by congruence.
      omega.
      rewrite PTree.gso.
      rewrite PTree.gempty.
      congruence.
      assumption.

      exact (non_virtual_align_low_bound (offsets_intro ( Hld) Hof' )).

      intros.
      eapply non_virtual_align_dynamic.
      eapply offsets_intro.
      eauto.
      eauto.
      eauto.

      intro.
      destruct (peq ci a).
       subst ci.
       intros.
       replace of with of' by congruence.
       apply Zdivide_refl.
       rewrite PTree.gso.
       rewrite PTree.gempty.
       congruence.
       assumption.

      intros ? ?.
      destruct (peq ci a).
       subst ci.
       rewrite PTree.gss.
       injection 1; intros; subst of.
       exists 0.
       omega.
      rewrite PTree.gso.
      rewrite PTree.gempty.
      congruence.
      assumption.

      intros.
      destruct (nvebo_prop ( Hld) He b o).
      split.
      intros.
      exists a.
      exists 0.
      split.
       rewrite PTree.gss.
       trivial.
     replace (o - 0) with o by omega.
     auto.
     destruct 1.
     destruct H1.
     destruct H1.
     apply H0.
     destruct (peq x a).
      subst x.
      rewrite PTree.gss in H1.
      injection H1; intros; subst x0.
     replace o with (o - 0) by omega.
     assumption.
     rewrite PTree.gso in H1.
     rewrite PTree.gempty in H1.
     discriminate.
     assumption.

     intros.
      split.
       tauto.
      destruct 1.
      destruct H.
      destruct H.
      destruct (peq x a).
       subst x.
       rewrite PTree.gss in H.
       injection H; intro; subst x0.
       tauto.
      rewrite PTree.gso in H.
      rewrite PTree.gempty in H.
      discriminate.
      assumption.
   Qed.

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.

     constructor; simpl; try rewrite PTree.gempty; try congruence.

     split.
     intros.
     right.
     unfold nvbases.
     eapply member_flatten_intro with (f (Class.Inheritance.Repeated, ci)).
     eapply in_map.
     assumption.
     simpl.
     auto.
     rewrite PTree.gempty.
     inversion 1.
      congruence.
      unfold nvbases in H0.
      destruct (member_flatten_elim H0).
      destruct H1.
      destruct (list_in_map_inv _ _ _ H1).
      destruct H3.
      subst.
      destruct x0.
      destruct t; simpl in H2.
       inversion H2; try contradiction.
       congruence.
      contradiction.

      generalize (dynamic_type_data_size_low_bound PF).
      omega.

      omega.

      omega.

      apply dynamic_type_data_size_low_bound.

      intros ? ?.
      rewrite PTree.gempty.
      congruence.

      intros until 3.
      intros ?.
      rewrite PTree.gempty.
      congruence.

      intros ? ?.
      rewrite PTree.gempty.
      congruence.

      intros ? ?.
      rewrite PTree.gempty.
      congruence.

      intros ? ? ?.
      rewrite PTree.gempty.
      congruence.

      intros ? ?.
      rewrite PTree.gempty.
      congruence.

      apply dynamic_type_data_align_low_bound.

      intros; apply Zdivide_refl.

      intros ?.
      rewrite PTree.gempty.
      congruence.

      intros ? ?.
      rewrite PTree.gempty.
      congruence.

      split.
       tauto.
      destruct 1.
      destruct H.
      destruct H.
      rewrite PTree.gempty in H.
      discriminate.

      split.
       tauto.
      destruct 1.
      destruct H.
      destruct H.
      rewrite PTree.gempty in H.
      discriminate.
    Qed.

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.

     constructor; simpl; try rewrite PTree.gempty; try congruence; try omega.

     split.
     intros.
     right.
     unfold nvbases.
     eapply member_flatten_intro with (f (Class.Inheritance.Repeated, ci)).
     eapply in_map.
     assumption.
     simpl.
     auto.
     rewrite PTree.gempty.
     inversion 1.
      congruence.
      unfold nvbases in H0.
      destruct (member_flatten_elim H0).
      destruct H1.
      destruct (list_in_map_inv _ _ _ H1).
      destruct H3.
      subst.
      destruct x0.
      destruct t; simpl in H2.
       inversion H2; try contradiction.
       congruence.
      contradiction.

      intros ? ?.
      rewrite PTree.gempty.
      congruence.

      intros ? ?.
      rewrite PTree.gempty.
      congruence.

      intros ? ?.
      rewrite PTree.gempty.
      congruence.

      intros ? ? ?.
      rewrite PTree.gempty.
      congruence.

      intros ? ?.
      rewrite PTree.gempty.
      congruence.

      intros ?.
      rewrite PTree.gempty.
      congruence.

      intros ? ?.
      rewrite PTree.gempty.
      congruence.

      split.
       tauto.
      destruct 1.
      destruct H.
      destruct H.
      rewrite PTree.gempty in H.
      discriminate.

      split.
       tauto.
      destruct 1.
      destruct H.
      destruct H.
      rewrite PTree.gempty in H.
      discriminate.
    Qed.

  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.

   case_eq dynbases.
    intros.
    destruct (is_dynamic_dec hierarchy_wf (cilimit ld)).
     destruct (nvl_init_dynamic_no_primary_base).
     eauto using non_virtual_direct_base_layout_end.
    destruct (nvl_init_non_dynamic).
     assumption.
    eauto using non_virtual_direct_base_layout_end.
    intros.
    destruct (nvl_init_some_primary_base H).
    eauto using non_virtual_direct_base_layout_end.
  Qed.

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.

  unfold nvldata.
  destruct non_virtual_direct_base_layout.
  tauto.
Qed.

Let H_nvldata_2 : nvl_todo nvldata = nil.

Proof.

  unfold nvldata.
  destruct non_virtual_direct_base_layout.
  tauto.
Qed.

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.

             intros.
             assert ( assoc (FieldSignature.eq_dec (A := A)) fs1 (fl_offsets fldata) <> None) by congruence.
             destruct (fl_exist prop fs1).
             assert (In fs1 (Class.fields h)) by eauto.
             assert (Plt ci1 (cilimit ld)) by eauto using Well_formed_hierarchy.well_founded_struct.
             destruct (empty_base_offset_wf
               hierarchy_wf (offsets_intro ( Hld)) (offsets_guard ( Hld)) H4).
             assert ((offsets ld) ! b <> None) by eauto using Ple_Plt_trans, offsets_exist.
             destruct (empty_base_offset_incl hierarchy_wf (offsets_intro ( Hld)) (offsets_guard ( Hld))
               H4 H19 H3
             ).
             destruct (empty_base_offset_incl hierarchy_wf (offsets_intro (Hld)) (offsets_guard ( Hld))
               H10 H19 H9
             ).
             generalize (fl_non_overlap prop H H5 H11).
             unfold field_size.
             rewrite H0.
             rewrite H6.
             rewrite H3.
             rewrite H9.
             intros.
             generalize (H24 _ (refl_equal _) _ (refl_equal _)).
             intro.
             generalize (fl_low_bound prop H).
             intros.
             generalize (fl_low_bound prop H5).
             intros.
             generalize (nvl_data_low_bound H_nvldata).
             intros.
             assert (z1 <= Zpos p1 - 1) by omega.
             assert (0 <= size so1) by omega.
             generalize (Zmult_le_compat_r _ _ _ H29 H30).
             intros.
             assert (0 <= size so2) by omega.
             assert (z2 <= Zpos p2 - 1) by omega.
             generalize (Zmult_le_compat_r _ _ _ H33 H32).
             intros.
             generalize (Zmult_ge H1 H30).
             generalize (Zmult_ge H7 H32).
             omega.
           Qed.

           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.

               destruct (fl_exist prop fs0).
               apply H0.
               rewrite Htodo.
               auto.
             Qed.

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.

eauto using Well_formed_hierarchy.well_founded_struct.
Qed.

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

Proof.

             assert ((offsets ld) ! a <> None) by eauto using offsets_exist, Well_formed_hierarchy.complete_struct.
             case_eq ((offsets ld) ! a); try congruence.
             intros.
             repeat esplit.
           Qed.

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

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

Proof.

             unfold o'.
             destruct fstruct_orig_offset.
             assumption.
           Qed.

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

Proof.

             generalize (ebo_exist ( Hld) Hlt).
             case_eq ((ebo ld) ! a); try congruence.
             intros.
             repeat esplit.
           Qed.

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

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

Proof.

             unfold e.
             destruct fstruct_e0.
             assumption.
           Qed.

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.

             intros until 1.
             pattern k.
             eapply Z_lt_rec; try eassumption.
             intros.
             clear k H.
             destruct (Z_eq_dec x 0).
              subst.
              replace (Zpos na - 0) with (Zpos na) in H2 by omega.
              exists l; assumption.
             assert (0 <= x - 1 <= Zpos na) by omega.
             assert (0 <= x - 1 < x) by omega.
             apply (H0 _ H3 H (map (map_snd (fun o => o + (Zpos na - x) * size o')) e ++ l)).
             intros.
             assert (forall A B C : Prop, (A <-> B) -> (B <-> C) -> (A <-> C)) by tauto.
             refine (H4 _ _ _ (in_app (b, o) _ _) _).
             split.
              destruct 1.
               destruct (list_in_map_inv _ _ _ H5).
               destruct H6.
               destruct x0.
               Opaque Zmult Zplus Zminus. simpl in H6.
               injection H6; intros; subst.
               exists (Zpos na - x).
                split.
                Transparent Zminus. omega.
                split.
                 omega.
                replace (z + (Zpos na - x) * size o' - (Zpos na - x) * size o') with z by omega.
                assumption.
               destruct (H2 b o).
               destruct (H6 H5).
               destruct H8.
               destruct H9.
               exists x0.
               split.
                omega.
               split.
                omega.
               assumption.
              destruct 1.
              destruct H5.
              destruct H6.
              pattern (b, o) at 1.
              replace (b, o) with (map_snd (fun o0 => o0 + (Zpos na - x) * size o') (b, o - (Zpos na - x) * size o')).
              destruct (Z_eq_dec x0 (Zpos na - x)).
               subst.
               left.
               apply in_map.
               assumption.
              right.
              destruct (H2 b o).
              apply H9.
              exists x0.
              split.
               omega.
              split.
               omega.
              assumption.
             Opaque Zminus. simpl.
             f_equal.
             Transparent Zminus. omega.
           Qed.

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.

             refine (@fstruct_e'0_aux (Zpos na) _ _ nil _).
             generalize (Zpos_positive na).
             omega.
             generalize (Zpos_positive na).
             omega.
             Opaque Zminus. simpl.
             split.
              tauto.
             destruct 1.
             Transparent Zminus. omega.
           Qed.

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.

             unfold e'.
             destruct fstruct_e'0.
             assumption.
           Qed.

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.

               destruct (bounded_offset (align_low_bound (offsets_intro ( Hld) Ho')) (fl_nvds fldata) (fl_nvsize fldata) (fun z => match List.filter (f z) e' with nil => true | _ => false end)).
               destruct a0.
               destruct H0.
               esplit.
               split.
               eassumption.
               split.
               assumption.
               destruct H1.
                tauto.
               destruct (filter (f x) e'); try discriminate.
               auto.
             Qed.

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.

              unfold off.
              destruct fstruct_off0.
              assumption.
            Qed.

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.

              intros.
              inversion Hoff.
              destruct H5.
              generalize (fl_size_low_bound prop).
              intro.
              assert (Plt ci (cilimit ld)).
               destruct (nvl_exist H_nvldata ci).
               eapply Well_formed_hierarchy.well_founded.
               eauto.
               eauto.
               eapply H9.
               left.
               congruence.
              destruct (non_virtual_empty_base_offset_wf
                 hierarchy_wf (offsets_intro ( Hld)) (offsets_guard ( Hld)) H0).
              assert ((offsets ld) ! b <> None).
               eapply offsets_exist.
                eauto.
                eauto using Ple_Plt_trans.
                assumption.
               case_eq ((offsets ld) ! b) ; try congruence.
               intros.
               generalize (empty_base_offset_incl hierarchy_wf
                 (offsets_intro ( Hld)) (offsets_guard ( Hld))
                 H3 H11 Ho').
               intros.
               assert (hierarchy ! ci <> None).
                destruct (nvl_exist H_nvldata ci).
                eapply Well_formed_hierarchy.complete.
                eauto.
                eassumption.
                eapply H15.
                left.
                congruence.
               assert ((offsets ld) ! ci <> None) by eauto using offsets_exist.
               case_eq ((offsets ld) ! ci); try congruence.
               intros.
               generalize (non_virtual_empty_base_offset_incl hierarchy_wf
                 (offsets_intro ( Hld)) (offsets_guard ( Hld))
                 H0 H11 H16).
               intros.
               generalize (nvl_high_bound H_nvldata H H16).
               intros.
               assert (0 <= size o') by omega.
               generalize (Zmult_ge H1 H19).
               intros.
              inversion H6.
               omega.
              destruct (is_empty_dec hierarchy_wf ci).
               destruct (ebo_prop ( Hld) He b bo').
               generalize (H23 H3).
               intros.
               intro Habs.
               destruct (filter_In (f off) (b, i * size o' + bo') e').
               rewrite H21 in H26.
               simpl in H26.
               apply H26.
               split.
                destruct (He' b (i * size o' + bo')).
                apply H28.
                exists i.
                split.
                 assumption.
                split.
                 assumption.
                replace ( i * size o' + bo' - i * size o') with bo' by omega.
                assumption.
               rewrite Zplus_assoc.
               rewrite <- Habs.
               assert (
                 (if In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) (nvl_nvebo' nvldata)
                   then true
                   else false) = true
               ).
               case (In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) (nvl_nvebo' nvldata) ).
                tauto.
               intros.
               destruct n.
               destruct (nvl_nvebo'_prop H_nvldata b (co + bo)).
               apply H28.
               esplit.
               esplit.
               split.
               eassumption.
               split.
               assumption.
               replace (co + bo - co) with bo by omega.
               assumption.
              assumption.
             generalize (nvl_nonempty_high_bound H_nvldata n H H16).
             generalize (fl_data_low_bound prop).
             omega.
           Qed.

           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.

           split; simpl; try trivial.
            inversion prop.
            constructor; simpl; try assumption.

            intro.
            destruct (fl_exist0 fs).
            rewrite Htodo in H, H0.
            simpl in H, H0.
             destruct ((FieldSignature.eq_dec (A := A)) fs0 fs).
             subst fs.
             split.
             intros.
             left; congruence.
             intros.
             assumption.
            assert (fs0 = fs -> False) by congruence.
            split; tauto.

            apply Zle_trans with (fl_nvds fldata).
             eauto.
            assert (0 < size o') by eauto using size_positive, offsets_intro.
            assert (0 < Zpos na) by eauto using Zpos_positive.
            generalize (Zmult_gt H0 H).
            destruct fl_offset_prop.
            omega.

            destruct (Z_le_dec (fl_offset + Zpos na * size o') (fl_nvsize fldata)); omega.

            apply Zle_trans with (fl_nvsize fldata).
             eauto.
            destruct (Z_le_dec (fl_offset + Zpos na * size o') (fl_nvsize fldata)); omega.

            intros ? ?.
            destruct ((FieldSignature.eq_dec (A := A)) fs0 fs).
             subst fs.
             injection 1; intro; subst of.
             destruct fl_offset_prop.
             omega.
            eauto.

            intros ? ?.
            destruct ((FieldSignature.eq_dec (A := A)) fs0 fs1).
             subst fs1.
             injection 1; intro; subst o1.
             intros ? ?.
             destruct ((FieldSignature.eq_dec (A := A)) fs0 fs2).
              subst fs2.
              congruence.
             unfold field_size at 1.
             rewrite Hstruct.
             rewrite Ho'.
             intros.
             Opaque Zminus.
             injection H2.
             intros; subst s1.
             right.
             apply Zle_trans with (fl_nvds fldata).
              eauto.
             destruct fl_offset_prop.
             omega.
             intros ? ? ?.
             destruct ((FieldSignature.eq_dec (A := A)) fs0 fs2).
             subst fs2.
              injection 1; intro; subst o2.
              unfold field_size at 2.
              rewrite Hstruct.
              rewrite Ho'.
              injection 3; intros; subst.
              left.
              apply Zle_trans with (fl_nvds fldata).
              eauto.
              destruct fl_offset_prop.
              omega.
             eauto.

             intros ? ?.
             destruct ((FieldSignature.eq_dec (A := A)) fs0 fs1).
              subst fs1.
              injection 1; intro; subst o1.
              rewrite Hstruct.
              injection 1; intros until 2; subst ci1 p1.
              rewrite Ho'.
              injection 3; intros; subst so1.
              intros.
              cut (o2 + bo2 <> fl_offset + z1 * size o' + bo1).
               congruence.
              eauto using fl_offsets_non_overlap.
             eauto.

             intros ? ?.
             destruct ((FieldSignature.eq_dec (A := A)) fs0 fs).
              subst fs.
              injection 1; intro; subst of.
              unfold field_size.
              rewrite Hstruct.
              rewrite Ho'.
              injection 1; intros; subst.
              pattern (size o') at 2.
              replace (size o') with (1 * size o') by omega.
              rewrite <- Zmult_plus_distr_l.
              replace (Zpos na - 1 + 1) with (Zpos na).
              omega.
              Transparent Zminus. omega.
             intros.
             apply Zle_trans with (fl_nvds fldata).
              eauto.
            assert (0 < size o') by eauto using size_positive, offsets_intro.
            assert (0 < Zpos na) by eauto using Zpos_positive.
            generalize (Zmult_gt H2 H1).
            destruct fl_offset_prop.
            omega.

         apply lcm_positive.
         assumption.
         eauto using align_low_bound, offsets_intro.

         apply Zdivide_trans with (fl_align fldata).
         eauto.
         apply lcm_divides_left.

         intro.
         destruct ((FieldSignature.eq_dec (A := A)) fs0 fs).
          subst fs.
          intros _ ?.
          unfold field_align.
          rewrite Hstruct.
          rewrite Ho'.
          injection 1; intro; subst al.
          apply lcm_divides_right.
          eauto using align_low_bound, offsets_intro.
         intros.
         apply Zdivides_trans with (fl_align fldata).
          eauto.
         apply lcm_divides_left.

         intros ? ?.
         destruct ((FieldSignature.eq_dec (A := A)) fs0 fs).
          subst fs.
          injection 1; intro; subst fo.
          destruct fl_offset_prop.
          destruct H1.
          unfold field_align.
          rewrite Hstruct.
          rewrite Ho'.
          congruence.
         eauto.

         intros.
         split.
         intros.
         destruct (in_app_or _ _ _ H).
          destruct (list_in_map_inv _ _ _ H0).
          destruct H1.
          unfold g in H1.
          unfold map_snd in H1.
          destruct x.
          injection H1; intros; subst.
          destruct (He' i z).
          destruct (H3 H2).
          destruct H5.
          destruct H6.
          destruct (ebo_prop ( Hld) He i (z - x * size o')).
          exists fs0.
          exists fl_offset.
          destruct ((FieldSignature.eq_dec (A := A)) fs0 fs0); try congruence.
          split.
           trivial.
          exists a.
          exists na.
          split.
          assumption.
          exists x.
          split.
           assumption.
          split.
           assumption.
          exists o'.
          split.
           assumption.
          replace (fl_offset + z - fl_offset - x * size o') with (z - x * size o') by omega.
          auto.
         destruct (fl_ebo_prop0 b o).
         destruct (H1 H0).
         destruct H3.
         destruct H3.
         exists x.
         exists x0.
         destruct ((FieldSignature.eq_dec (A := A)) fs0 x).
          congruence.
         eauto.
        destruct 1.
        destruct H.
        destruct H.
        destruct ((FieldSignature.eq_dec (A := A)) fs0 x).
         subst x.
         replace x0 with fl_offset in * by congruence.
         apply in_or_app.
         left.
         destruct H0.
         destruct H0.
         destruct H0.
         rewrite Hstruct in H0.
         injection H0; intros; subst x x1.
         destruct H1.
         destruct H1.
         destruct H2.
         destruct H3.
         destruct H3.
         rewrite Ho' in H3.
         injection H3; intros; subst x1.
         replace (b, o) with (g (b, o - fl_offset)).
         apply in_map.
         destruct (He' b (o - fl_offset)).
         apply H6.
         exists x.
         split.
          assumption.
         split.
          assumption.
         destruct (ebo_prop ( Hld) He b (o - fl_offset - x * size o')).
         auto.
         simpl.
         f_equal.
         omega.
        apply in_or_app.
        right.
        destruct (fl_ebo_prop0 b o).
         apply H2.
         eauto.
       Qed.

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.

      split; simpl; try trivial.
      inversion prop.
      constructor; simpl; try assumption.

            intro.
            destruct (fl_exist0 fs).
            rewrite Htodo in H2, H3.
            simpl in H2, H3.
             destruct ((FieldSignature.eq_dec (A := A)) fs0 fs).
             subst fs.
             split.
             intros.
             left; congruence.
             intros.
             assumption.
            assert (fs0 = fs -> False) by congruence.
            split; tauto.

            apply Zle_trans with (fl_nvds fldata).
             eauto.
            generalize (typ_size_positive PF (t)).
            omega.

            destruct ( Z_le_dec (x + typ_size PF ( t))
         (fl_nvsize fldata)); omega.

            apply Zle_trans with (fl_nvsize fldata).
             eauto.
            destruct (Z_le_dec (x + typ_size PF (t))
         (fl_nvsize fldata)); omega.

            intros ? ?.
            destruct ((FieldSignature.eq_dec (A := A)) fs0 fs).
             subst fs.
             injection 1; intro; subst of.
             omega.
            eauto.

            intros ? ?.
            destruct ((FieldSignature.eq_dec (A := A)) fs0 fs1).
             subst fs1.
             injection 1; intro; subst o1.
             intros ? ?.
             destruct ((FieldSignature.eq_dec (A := A)) fs0 fs2).
              subst fs2.
              congruence.
             unfold field_size at 1.
             rewrite H.
             intros.
             injection H5.
             intros; subst s1.
             right.
             apply Zle_trans with (fl_nvds fldata).
              eauto.
             omega.
             intros ? ? ?.
             destruct ((FieldSignature.eq_dec (A := A)) fs0 fs2).
             subst fs2.
              injection 1; intro; subst o2.
              unfold field_size at 2.
              rewrite H.
              injection 3; intros; subst.
              left.
              apply Zle_trans with (fl_nvds fldata).
              eauto.
              omega.
             eauto.

             intros ? ?.
             destruct ((FieldSignature.eq_dec (A := A)) fs0 fs1).
              intros; congruence.
             eauto.

             intros ? ?.
             destruct ((FieldSignature.eq_dec (A := A)) fs0 fs).
              subst fs.
              injection 1; intro; subst of.
              unfold field_size.
              rewrite H.
              injection 1; intros; subst.
              omega.
             intros.
             apply Zle_trans with (fl_nvds fldata).
              eauto.
              generalize (typ_size_positive PF ( t)).
              omega.

         apply lcm_positive.
         apply typ_align_positive.
         assumption.

         apply Zdivide_trans with (fl_align fldata).
         eauto.
         apply lcm_divides_right.
         auto.

         intro.
         destruct ((FieldSignature.eq_dec (A := A)) fs0 fs).
          subst fs.
          intros _ ?.
          unfold field_align.
          rewrite H.
          injection 1; intro; subst al.
          apply lcm_divides_left.
          eauto using align_low_bound.
         intros.
         apply Zdivides_trans with (fl_align fldata).
          eauto.
         apply lcm_divides_right.
         auto.

         intros ? ?.
         destruct ((FieldSignature.eq_dec (A := A)) fs0 fs).
          subst fs.
          injection 1; intro; subst fo.
          unfold field_align.
          rewrite H.
          congruence.
         eauto.

         intros.
         destruct (fl_ebo_prop0 b o).
         split.
          intros.
          destruct (H2 H4).
          exists x0.
          destruct ((FieldSignature.eq_dec (A := A)) fs0 x0).
           destruct H5.
           destruct H5.
           destruct H6.
           destruct H6.
           destruct H6.
           congruence.
          assumption.
         destruct 1.
         destruct H4.
         destruct ((FieldSignature.eq_dec (A := A)) fs0 x0).
          destruct H4.
          destruct H5.
          destruct H5.
          destruct H5.
          congruence.
         eauto.
       Qed.

End Step.

Finally, pack all cases together

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

Proof.

      cut (forall l fldata, fl_todo fldata = l -> fl_prop fldata -> {fldata' | fl_prop fldata' /\ fl_todo fldata' = nil}).
     intros.
   refine (X (Class.fields h) (
     make_fl
     (Class.fields h)
     nil
     nil
     (nvl_nvds nvldata)
     (nvl_nvsize nvldata)
     (nvl_align nvldata)
   ) (refl_equal _) _).
   constructor; simpl; try congruence.
    tauto.
    omega.
    eauto using nvl_data_size.
    omega.
    eauto using nvl_align_pos.
    apply Zdivide_refl.
    split.
     tauto.
    destruct 1.
    destruct H.
    destruct H.
    discriminate.

  induction l.
  intros.
  exists fldata.
  split; assumption.

  intros.
  case_eq (assoc (FieldSignature.eq_dec (A := A)) a (fl_offsets fldata)).
   intros.
   destruct (IHl (
     make_fl
     l
     (fl_offsets fldata)
     (fl_ebo fldata)
     (fl_nvds fldata)
     (fl_nvsize fldata)
     (fl_align fldata)
   )).
    reflexivity.
   inversion H0.
   constructor; simpl; try assumption.
   assert (assoc (FieldSignature.eq_dec (A := A)) a (fl_offsets fldata) <> None) by congruence.
   intros.
   generalize (fl_exist0 fs).
   rewrite H.
   simpl.
   destruct ((FieldSignature.eq_dec (A := A)) a fs).
    rewrite e in H2.
    tauto.
   tauto.
  exists x; assumption.

  intros.
  destruct (field_layout_step H0 H H1).
  destruct a0.
  eauto.
Qed.

End Field_layout.

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

  Let H_fldata : fl_prop fldata.

Proof.

    unfold fldata.
    destruct field_layout.
    tauto.
  Qed.

Let H_fldata_2 : fl_todo fldata = nil.

Proof.

    unfold fldata.
    destruct field_layout.
    tauto.
  Qed.

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.

    unfold nvebo0.
    intros.
    destruct (in_app_or _ _ _ H).
     cut (0 <= o < nvl_nvsize nvldata).
      generalize (fl_size_low_bound H_fldata).
      omega.
     destruct (nvl_nvebo_prop H_nvldata b o).
     destruct (H1 H0).
     destruct H3.
     destruct H3.
     assert ((nvl_offsets nvldata) ! x <> None) by congruence.
     destruct (nvl_exist H_nvldata x).
     generalize (H7 (or_introl _ H5)).
     intros.
     assert (Plt x (cilimit ld)) by eauto using Well_formed_hierarchy.well_founded.
     assert (hierarchy ! x <> None) by eauto using Well_formed_hierarchy.complete.
     assert ((offsets ld) ! x <> None) by eauto using offsets_exist.
     case_eq ((offsets ld) ! x); try congruence.
     intros.
     destruct (non_virtual_empty_base_offset_wf
       hierarchy_wf (offsets_intro ( Hld)) (offsets_guard ( Hld)) H4).
     assert (Plt b (cilimit ld)) by eauto using Ple_Plt_trans.
     assert ((offsets ld) ! b <> None) by eauto using offsets_exist.
     destruct (non_virtual_empty_base_offset_incl hierarchy_wf
       (offsets_intro ( Hld)) (offsets_guard ( Hld))
       H4 H16 H12).
     generalize (nvl_low_bound H_nvldata H3).
     generalize (nvl_high_bound H_nvldata H3 H12).
     omega.
    cut (0 <= o < fl_nvds fldata).
     generalize (fl_data_size H_fldata).
     omega.
    destruct (fl_ebo_prop H_fldata b o).
    destruct (H1 H0).
    destruct H3.
    destruct H3.
    destruct H4.
    destruct H4.
    destruct H4.
    destruct H5.
    destruct H5.
    destruct H6.
    destruct H7.
    destruct H7.
    generalize (size_positive (offsets_intro Hld) H7).
    intros.
    assert (0 <= size x4) by omega.
    generalize (Zmult_ge H5 H10).
    intros.
    assert (x3 <= Zpos x2 - 1) by omega.
    generalize (Zmult_le_compat_r _ _ _ H12 H10).
    rewrite Zmult_minus_distr_r.
    replace (1 * size x4) with (size x4) by omega.
    intros.
    destruct (empty_base_offset_wf hierarchy_wf (offsets_intro Hld) (offsets_guard Hld) H8).
    assert (
      assoc (FieldSignature.eq_dec (A := A)) x (fl_offsets fldata) <> None
    ) by congruence.
    generalize (fl_exist H_fldata x).
    rewrite H_fldata_2.
    simpl.
    destruct 1.
    assert ((offsets ld) ! b <> None).
     eapply offsets_exist.
     eauto.
     eauto using Ple_Plt_trans, Well_formed_hierarchy.well_founded_struct.
     assumption.
    generalize (empty_base_offset_incl hierarchy_wf (offsets_intro Hld) (offsets_guard Hld) H8 H19 H7).
    intros.
    generalize (fl_low_bound H_fldata H3).
    generalize (nvl_data_low_bound H_nvldata).
    generalize (fl_high_bound H_fldata H3).
    unfold field_size.
    rewrite H4.
    rewrite H7.
    intros.
    generalize (H21 _ (refl_equal _)).
    rewrite Zmult_minus_distr_r.
    rewrite Zmult_1_l.
    omega.
  Qed.

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

Proof.

    unfold nvebo0.
    intros.
    destruct (in_app_or _ _ _ H).
     cut (0 <= o < nvl_nvds nvldata).
      generalize (fl_data_low_bound H_fldata).
      omega.
     destruct (nvl_nvebo_prop H_nvldata b o).
     destruct (H2 H1).
     destruct H4.
     destruct H4.
     assert ((nvl_offsets nvldata) ! x <> None) by congruence.
     destruct (nvl_exist H_nvldata x).
     generalize (H8 (or_introl _ H6)).
     intros.
     assert (Plt x (cilimit ld)) by eauto using Well_formed_hierarchy.well_founded.
     assert (hierarchy ! x <> None) by eauto using Well_formed_hierarchy.complete.
     assert ((offsets ld) ! x <> None) by eauto using offsets_exist.
     case_eq ((offsets ld) ! x); try congruence.
     intros.
     destruct (non_virtual_empty_base_offset_wf
       hierarchy_wf (offsets_intro ( Hld)) (offsets_guard ( Hld)) H5).
     assert (Plt b (cilimit ld)) by eauto using Ple_Plt_trans.
     assert ((offsets ld) ! b <> None) by eauto using offsets_exist.
     destruct (non_virtual_empty_base_offset_incl hierarchy_wf
       (offsets_intro ( Hld)) (offsets_guard ( Hld))
       H5 H17 H13).
     destruct (is_empty_dec hierarchy_wf x).
      destruct H0.
      destruct (nvl_nvebo'_prop H_nvldata b o).
      apply H20.
      esplit.
      esplit.
      split.
      eassumption.
      split.
      assumption.
      assumption.
     generalize (nvl_low_bound H_nvldata H4).
     generalize (nvl_nonempty_high_bound H_nvldata n H4 H13).
     omega.
    clear H0.
    rename H1 into H0.
    destruct (fl_ebo_prop H_fldata b o).
    destruct (H1 H0).
    destruct H3.
    destruct H3.
    destruct H4.
    destruct H4.
    destruct H4.
    destruct H5.
    destruct H5.
    destruct H6.
    destruct H7.
    destruct H7.
    generalize (size_positive (offsets_intro Hld) H7).
    intros.
    assert (0 <= size x4) by omega.
    generalize (Zmult_ge H5 H10).
    intros.
    assert (x3 <= Zpos x2 - 1) by omega.
    generalize (Zmult_le_compat_r _ _ _ H12 H10).
    rewrite Zmult_minus_distr_r.
    replace (1 * size x4) with (size x4) by omega.
    intros.
    destruct (empty_base_offset_wf hierarchy_wf (offsets_intro Hld) (offsets_guard Hld) H8).
    assert (
      assoc (FieldSignature.eq_dec (A := A)) x (fl_offsets fldata) <> None
    ) by congruence.
    generalize (fl_exist H_fldata x).
    rewrite H_fldata_2.
    simpl.
    destruct 1.
    assert ((offsets ld) ! b <> None).
     eapply offsets_exist.
     eauto.
     eauto using Ple_Plt_trans, Well_formed_hierarchy.well_founded_struct.
     assumption.
    generalize (empty_base_offset_incl hierarchy_wf (offsets_intro Hld) (offsets_guard Hld) H8 H19 H7).
    intros.
    generalize (fl_low_bound H_fldata H3).
    generalize (nvl_data_low_bound H_nvldata).
    generalize (fl_high_bound H_fldata H3).
    unfold field_size.
    rewrite H4.
    rewrite H7.
    intros.
    generalize (H21 _ (refl_equal _)).
    rewrite Zmult_minus_distr_r.
    rewrite Zmult_1_l.
    omega.
  Qed.

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.

             destruct (vl_exist prop a).
             apply H0.
             rewrite Htodo.
             auto.
           Qed.

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

Proof.

eauto using Well_formed_hierarchy.is_virtual_base_of_lt.
Qed.

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

Proof.

             assert ((offsets ld) ! a <> None) by eauto using offsets_exist, Well_formed_hierarchy.is_virtual_base_of_defined_base.
             case_eq ((offsets ld) ! a); try congruence.
             intros.
             repeat esplit.
           Qed.

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

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

Proof.

             unfold o'.
             destruct v_orig_offset.
             assumption.
           Qed.

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

Proof.

             generalize (nvebo_exist ( Hld) Hlt).
             case_eq ((nvebo ld) ! a); try congruence.
             intros.
             repeat esplit.
           Qed.

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

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

Proof.

             unfold e.
             destruct e0.
             assumption.
           Qed.

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

Proof.

intros; eauto using no_virtual_bases.
Qed.

Corollary nvebo_eq_nvebo0 : Nvebo = nvebo0.

Proof.

             unfold Nvebo.
             case (is_empty_dec hierarchy_wf (cilimit ld)); try contradiction; reflexivity.
           Qed.

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.

exact (non_virtual_align_low_bound (offsets_intro Hld Ho')).
Qed.

           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.

              intros.
              unfold v_offset.
              case_eq cond.
               unfold cond.
               case em; try congruence.
               case_eq (filter f_empty e); try congruence.
               intros.
               simpl.
               intro; subst.
               generalize (filter_In f_empty (b, co + bo) e).
               rewrite H2.
               simpl.
               destruct 1.
               apply H5.
               split.
               generalize (nvebo_prop Hld He b (co + bo)).
               tauto.
               unfold f_empty.
               case (In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) (vl_nvebo vldata)).
                destruct (In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) nvebo0); trivial.
               intros.
               destruct n.
               destruct (vl_nvebo_prop prop b (co + bo)).
               apply H7.
               esplit.
               esplit.
               split.
               eassumption.
               replace (co + bo - co) with bo by omega.
               assumption.
              intros _.
              destruct (bounded_offset align_pos (vl_ds vldata) (vl_size vldata) f').
              destruct a0.
              destruct H3.
              assert (Plt ci (cilimit ld)).
               destruct (vl_exist prop ci).
               eapply Well_formed_hierarchy.is_virtual_base_of_lt.
               eauto.
               eapply H6.
               left.
               congruence.
              destruct (non_virtual_empty_base_offset_wf
               hierarchy_wf (offsets_intro ( Hld)) (offsets_guard ( Hld)) H0).
              assert ((offsets ld) ! b <> None).
               eapply offsets_exist.
               eauto.
               eauto using Ple_Plt_trans.
               assumption.
              case_eq ((offsets ld) ! b) ; try congruence.
              intros.
              generalize (non_virtual_empty_base_offset_incl hierarchy_wf
                 (offsets_intro ( Hld)) (offsets_guard ( Hld))
                 H1 H8 Ho').
              intros.
              assert (hierarchy ! ci <> None).
               destruct (vl_exist prop ci).
               eapply Well_formed_hierarchy.is_virtual_base_of_defined_base.
               eauto.
               eapply H12.
               left.
               congruence.
              assert ((offsets ld) ! ci <> None) by eauto using offsets_exist.
              case_eq ((offsets ld) ! ci); try congruence.
              intros.
              generalize (non_virtual_empty_base_offset_incl hierarchy_wf
                 (offsets_intro ( Hld)) (offsets_guard ( Hld))
                 H0 H8 H13).
              intros.
              destruct H4.
               generalize (vl_high_bound prop H H13).
               omega.
              destruct (is_empty_dec hierarchy_wf ci).
               revert H4.
               unfold f'.
               case_eq (filter (f x) e); try congruence.
               intros.
               intro Habs.
               generalize (filter_In (f x) (b, bo') e).
               rewrite H4.
               simpl.
               destruct 1.
               apply H17.
               split.
               generalize (nvebo_prop Hld He b bo').
               tauto.
               rewrite <- Habs.
               assert (
                 (if In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) (nvl_nvebo' nvldata)
                   then true
                   else
                     if In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) (vl_nvebo' vldata)
                       then true
                       else false) = true
               ).
                destruct (In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) (vl_nvebo' vldata)).
                 destruct ( In_dec (prod_eq_dec peq Z_eq_dec) (b, co + bo) (nvl_nvebo' nvldata)); trivial.
                destruct n.
                generalize (vl_nvebo'_prop prop b (co + bo)).
                destruct 1.
                apply H19.
                esplit.
                esplit.
                split.
                eassumption.
                split.
                assumption.
                replace (co + bo - co) with bo by omega.
                assumption.
               assumption.
              generalize (vl_nonempty_high_bound prop n H H13).
              omega.
            Qed.

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.

              rewrite nvebo_eq_nvebo0.
              intros until 1.
              generalize (non_virtual_empty_base_offset_wf hierarchy_wf (offsets_intro Hld) (offsets_guard Hld) H).
              destruct 1.
              assert ((offsets ld) ! b <> None) by eauto using offsets_exist, Ple_Plt_trans.
              generalize (non_virtual_empty_base_offset_incl hierarchy_wf (offsets_intro Hld) (offsets_guard Hld) H H2 Ho').
              intro.
              unfold v_offset.
              case_eq cond.
               simpl.
               unfold cond.
               case em; try congruence.
               case_eq (filter f_empty e); try congruence.
               intros.
               generalize (filter_In f_empty (b, bo') e).
               rewrite H4.
               simpl.
               destruct 1.
               apply H8.
               split.
               generalize (nvebo_prop Hld He b bo').
               tauto.
               unfold f_empty.
               case (In_dec (prod_eq_dec peq Z_eq_dec) (b, bo') nvebo0).
                trivial.
               intros; contradiction.
              intros _.
              destruct (bounded_offset align_pos (vl_ds vldata) (vl_size vldata)).
              destruct a0.
              destruct H5.
              intro.
              destruct H6.
               generalize (nvebo0_incl H7).
               generalize (vl_size_low_bound prop).
              omega.
             revert H6.
             unfold f'.
             case_eq (filter (f x) e); try congruence.
             intros.
             generalize (filter_In (f x) (b, bo') e).
             rewrite H6.
             simpl.
             destruct 1.
             apply H10.
             split.
              generalize (nvebo_prop Hld He b bo').
              tauto.
             assert (
   (if In_dec (prod_eq_dec peq Z_eq_dec) (b, x + bo') (nvl_nvebo' nvldata)
    then true
    else
     if In_dec (prod_eq_dec peq Z_eq_dec) (b, x + bo') (vl_nvebo' vldata)
     then true
     else false) = true
             ).
             case ( In_dec (prod_eq_dec peq Z_eq_dec) (b, x + bo') (nvl_nvebo' nvldata)).
              trivial.
             intros.
             apply False_rect.
             generalize (nvebo0_data_incl H7 n).
             generalize (vl_data_low_bound prop).
             omega.
            assumption.
          Qed.

Lemma v_offset_low_bound : 0 <= v_offset.

Proof.

              unfold v_offset.
              case cond.
               omega.
              destruct (bounded_offset align_pos (vl_ds vldata) (vl_size vldata) f').
              generalize (vl_data_low_bound prop).
              generalize (fl_data_low_bound H_fldata).
              generalize (nvl_data_low_bound H_nvldata).
              omega.
            Qed.

Lemma v_offset_align : (non_virtual_align o' | v_offset).

Proof.

              unfold v_offset.
              case cond.
               exists 0; omega.
              destruct (bounded_offset align_pos (vl_ds vldata) (vl_size vldata) f').
              tauto.
            Qed.

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

Proof.

              unfold v_offset.
              unfold cond.
              case em.
               contradiction.
             destruct (bounded_offset align_pos (vl_ds vldata) (vl_size vldata) f').
             tauto.
            Qed.

         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.

           split; simpl; try trivial.
            inversion prop.
            constructor; simpl; try assumption.

            intro.
            destruct (vl_exist0 ci).
            rewrite Htodo in H, H0.
            simpl in H, H0.
             destruct (peq ci a).
             subst.
             rewrite PTree.gss.
             split.
             intros.
             left; congruence.
             intros.
             assumption.
            rewrite PTree.gso.
            assert (a = ci -> False) by congruence.
            split; tauto.
           assumption.

            case em; intro.
             assumption.
            apply Zle_trans with (vl_ds vldata).
             assumption.
            generalize (v_offset_nonempty_low_bound n).
            generalize (non_virtual_size_positive (offsets_intro ( Hld) Ho')).
            omega.

            apply Zle_trans with (vl_size vldata).
            assumption.
            destruct (Z_le_dec (v_offset + non_virtual_size o') (vl_size vldata)).
             omega.
            omega.

            case em; intro.
             apply Zle_trans with (vl_size vldata).
              assumption.
            destruct (Z_le_dec (v_offset + non_virtual_size o') (vl_size vldata)); omega.
            destruct (Z_le_dec (v_offset + non_virtual_size o') (vl_size vldata)); omega.

            intros ? ?.
            destruct (peq ci a).
             subst.
             rewrite PTree.gss.
             injection 1; intros; subst of.
             exact (v_offset_low_bound).
            rewrite PTree.gso.
            eauto.
            assumption.

            intros ? ? ?.
            destruct (peq ci a).
             subst.
             rewrite PTree.gss.
             injection 1; intros; subst of.
             generalize (v_offset_nonempty_low_bound H).
             omega.
            rewrite PTree.gso; eauto.

          intros ? ?.
          destruct (peq ci1 a).
           subst.
           rewrite PTree.gss.
           injection 1; intro; subst o1.
           intros.
           rewrite PTree.gso in H1.
           generalize (vl_nonempty_high_bound prop H2 H1 H5).
           generalize (v_offset_nonempty_low_bound H0).
           omega.
           congruence.
          rewrite PTree.gso.
          intros ? ? ? ?.
          destruct (peq ci2 a).
           subst.
           rewrite PTree.gss.
           injection 1; intros; subst o2.
           generalize (vl_nonempty_high_bound prop H0 H H5).
           generalize (v_offset_nonempty_low_bound H3).
           omega.
           rewrite PTree.gso.
           eauto.
           assumption.
          assumption.

          intros ? ?.
          destruct (peq ci1 a).
           subst.
           rewrite PTree.gss.
           injection 1; intro; subst o1.
           intros.
           rewrite PTree.gso in H0.
           cut (o2 + bo2 <> v_offset + bo1).
            congruence.
           eauto using v_offsets_non_overlap.
           congruence.
          rewrite PTree.gso.
          intros ? ? ?.
          destruct (peq ci2 a).
           subst.
           rewrite PTree.gss.
           injection 1; intros; subst o2.
           eauto using v_offsets_non_overlap.
          rewrite PTree.gso.
          eauto.
          assumption.
          assumption.

          intros ? ?.
          destruct (peq ci a).
           subst.
           rewrite PTree.gss.
           injection 1; intro; subst o.
           intros; eauto using v_offsets_non_overlap_main.
          rewrite PTree.gso; eauto.

          case em.
           intros ? ? ?.
           rewrite PTree.gso.
           eauto.
           intro.
           subst ci.
           contradiction.
          intros ? ? ?.
          destruct (peq ci a).
           subst.
           rewrite PTree.gss.
           injection 1; intros; subst of.
           replace o'0 with o' in * by congruence.
           omega.
          rewrite PTree.gso.
          intros.
          eapply Zle_trans with (vl_ds vldata).
          eauto.
          generalize (v_offset_nonempty_low_bound n).
          generalize (non_virtual_size_positive (offsets_intro ( Hld) Ho')).
            omega.
          assumption.

          intros ? ?.
          destruct (peq ci a).
           subst.
           rewrite PTree.gss.
           injection 1; intros; subst of.
           destruct ( Z_le_dec (v_offset + non_virtual_size o') (vl_size vldata)).
            congruence.
           replace o'0 with o' by congruence.
           omega.
          rewrite PTree.gso.
          intros.
          destruct ( Z_le_dec (v_offset + non_virtual_size o') (vl_size vldata)).
           eauto.
          apply Zle_trans with (vl_size vldata).
           eauto.
          omega.
         assumption.

         apply lcm_positive.
         assumption.
         eauto using non_virtual_align_low_bound.

         apply Zdivide_trans with (vl_align vldata).
         eauto.
         apply lcm_divides_left.

         intro.
         destruct (peq ci a).
          subst.
          intros.
          replace of with o' by congruence.
          apply lcm_divides_right.
          eauto using non_virtual_align_low_bound.
         rewrite PTree.gso.
         intros.
         apply Zdivides_trans with (vl_align vldata).
          eauto.
         apply lcm_divides_left.
         assumption.

         intros ? ?.
         destruct (peq ci a).
          subst ci.
          rewrite PTree.gss.
          injection 1; intro; subst of.
          rewrite Ho'.
          injection 1; intros; subst co.
          exact v_offset_align.
         rewrite PTree.gso; eauto.

         intros.
         split.
         intros.
         destruct (in_app_or _ _ _ H).
          destruct (list_in_map_inv _ _ _ H0).
          destruct H1.
          unfold g in H1.
          unfold map_snd in H1.
          destruct x.
          injection H1; intros; subst.
          destruct (nvebo_prop ( Hld) He i z).
          exists a.
          exists v_offset.
          rewrite PTree.gss.
          split.
          trivial.
          replace (v_offset + z - v_offset) with z by omega.
          auto.
         destruct (vl_nvebo_prop0 b o).
         destruct (H1 H0).
         destruct H3.
         destruct H3.
         exists x.
         exists x0.
         rewrite PTree.gso.
         eauto.
         congruence.
        destruct 1.
        destruct H.
        destruct H.
        destruct (peq x a).
         subst.
         rewrite PTree.gss in H.
         injection H; intro; subst x0.
         apply in_or_app.
         left.
         replace (b, o) with (g (b, o - v_offset)).
         apply in_map.
         destruct (nvebo_prop ( Hld) He b (o - v_offset)).
         auto.
         simpl.
         f_equal.
         omega.
        rewrite PTree.gso in H.
        apply in_or_app.
        right.
        destruct (vl_nvebo_prop0 b o).
         apply H2.
         eauto.
        assumption.

         intros.
         split.
         intros.
         destruct (in_app_or _ _ _ H).
          revert H0.
          case em.
          intros.
          destruct (list_in_map_inv _ _ _ H0).
          destruct H1.
          unfold g in H1.
          unfold map_snd in H1.
          destruct x.
          injection H1; intros; subst.
          destruct (nvebo_prop ( Hld) He i0 z).
          exists a.
          exists v_offset.
          rewrite PTree.gss.
          split.
          trivial.
          split.
          assumption.
          replace (v_offset + z - v_offset) with z by omega.
          auto.
          simpl.
          tauto.
         destruct (vl_nvebo'_prop0 b o).
         destruct (H1 H0).
         destruct H3.
         destruct H3.
         exists x.
         exists x0.
         rewrite PTree.gso.
         eauto.
         congruence.
        destruct 1.
        destruct H.
        destruct H.
        destruct (peq x a).
         subst.
         rewrite PTree.gss in H.
         injection H; intro; subst x0.
         apply in_or_app.
         left.
         replace (b, o) with (g (b, o - v_offset)).
         case em.
          intros _.
         apply in_map.
         destruct (nvebo_prop ( Hld) He b (o - v_offset)).
         destruct H0.
         auto.
         tauto.
         simpl.
         f_equal.
         omega.
        rewrite PTree.gso in H.
        apply in_or_app.
        right.
        destruct (vl_nvebo'_prop0 b o).
         apply H2.
         eauto.
        assumption.
      Qed.

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.

      case_eq (virtual_bases ! (cilimit ld)).
       intros.
       exists l.
       destruct (virtual_bases_prop).
       eauto.
      intros.
      apply False_rect.
      destruct (virtual_bases_prop).
      eapply H0.
      2 : eassumption.
      congruence.
    Qed.

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.

      unfold vbases.
      destruct vbases_aux.
      assumption.
    Qed.

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

Proof.

   cut (forall l vl, vl_todo vl = l -> vl_prop vl -> {
     vldata | vl_prop vldata /\ vl_todo vldata = nil
   }).
    intros.
    refine (H _ (make_vl
      vbases
      (@PTree.empty _)
      nil
      nil
      (fl_nvds fldata)
      (fl_nvsize fldata)
      (fl_align fldata)
    ) _ _).
     reflexivity.
    constructor; simpl; try (intros; rewrite PTree.gempty in *; congruence).
    intro.
    rewrite PTree.gempty.
    generalize (H_vbases ci).
    tauto.
    omega.
    omega.
    eauto using fl_data_size.
    eauto using fl_align_pos.
    apply Zdivide_refl.
    split.
     tauto.
    destruct 1.
    destruct H0.
    destruct H0.
    rewrite PTree.gempty in *; congruence.
    split.
     tauto.
    destruct 1.
    destruct H0.
    destruct H0.
    rewrite PTree.gempty in *; congruence.

   induction l.
   intros.
   esplit.
   split.
    eassumption.
   assumption.

   intros.
   case_eq ((vl_offsets vl0) ! a).
    intros.
    apply IHl with (make_vl
      l
      (vl_offsets vl0)
      (vl_nvebo vl0)
      (vl_nvebo' vl0)
      (vl_ds vl0)
      (vl_size vl0)
      (vl_align vl0)
    ).
     reflexivity.
    inversion H0.
    constructor; simpl; try assumption.
    intro.
    generalize (vl_exist0 ci).
    rewrite H.
    simpl.
    destruct (peq a ci).
     subst.
     rewrite H1.
     assert (forall A B C: Prop, (B <-> C) -> (A <-> B) -> (A <-> C)) by tauto.
     apply H2.
     split; left; congruence.
    tauto.

    intros.
    destruct (virtual_base_layout_step H0 H H1).
    destruct a0.
    eauto.
  Qed.

  End Virtual_base_layout.

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

  Let H_vldata : vl_prop vldata.

Proof.

    unfold vldata.
    destruct virtual_base_layout.
    tauto.
  Qed.

Let H_vldata_2 : vl_todo vldata = nil.

Proof.

    unfold vldata.
    destruct virtual_base_layout.
    tauto.
  Qed.

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.

    unfold size.
    destruct size0.
    tauto.
  Qed.

Let H_size_2 : (vl_align vldata | size).

Proof.

    unfold size.
    destruct size0.
    tauto.
  Qed.

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.

    unfold offsets'.
    intros.
    rewrite PTree.gso.
    trivial.
    intro; subst.
    eapply Plt_irrefl; eauto.
  Qed.

  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.

    intros.
    assert (ci <> cilimit ld).
     intro.
     subst.
     eapply Plt_irrefl.
     eassumption.
    generalize H0.
     unfold offsets' at 1.
     rewrite PTree.gso.
     intros.
    eapply class_level_prop_eq with (offsets1 := offsets ld) (cilimit := cilimit ld).
     eauto.
     intros; symmetry; eauto using offsets'_eq.
    eauto using offsets_guard.
    assumption.
    eassumption.
    eauto using offsets_intro.
    assumption.
    assumption.
  Qed.

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

Proof.

   unfold offsets'.
   rewrite PTree.gss.
   trivial.
  Qed.

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

Proof.

    intros.
    assert ((nvl_offsets nvldata) ! bi <> None) by congruence.
    destruct (nvl_exist H_nvldata bi).
    generalize (H2 (or_introl _ H0)).
    intros.
    eauto using Well_formed_hierarchy.well_founded.
  Qed.

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

Proof.

    intros.
    assert ((nvl_offsets nvldata) ! bi <> None) by congruence.
    destruct (nvl_exist H_nvldata bi).
    generalize (H2 (or_introl _ H0)).
    intros.
    assert (Plt bi (cilimit ld)) by eauto using Well_formed_hierarchy.well_founded.
    eauto using offsets'_eq.
  Qed.

  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.

    intros.
    assert (assoc (FieldSignature.eq_dec (A := A)) f (fl_offsets fldata) <> None) by congruence.
    destruct (fl_exist H_fldata f).
    generalize (H3 (or_introl _ H1)).
    intros.
    assert (Plt ci (cilimit ld)) by eauto using Well_formed_hierarchy.well_founded_struct.
    eauto using offsets'_eq.
  Qed.

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

Proof.

    intros.
    assert ((vl_offsets vldata) ! bi <> None) by congruence.
    destruct (vl_exist H_vldata bi).
    generalize (H2 (or_introl _ H0)).
    intros.
    assert (Plt bi (cilimit ld)) by eauto using Well_formed_hierarchy.is_virtual_base_of_lt.
    eauto using offsets'_eq.
  Qed.

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.

    constructor; unfold o'; simpl.

    intros.
    eapply nvl_primary_base_dynamic.
    eauto.
    assumption.

    intros.
    generalize (nvl_primary_base H_nvldata H).
    intros.
    assert ((nvl_offsets nvldata) ! b <> None) by congruence.
    destruct (nvl_exist H_nvldata b).
    generalize (H3 (or_introl _ H1)).
    intros.
    assert (Plt b (cilimit ld)) by eauto using Well_formed_hierarchy.well_founded.
    rewrite (offsets'_eq H5).
    eauto using Well_formed_hierarchy.complete, offsets_exist.

    intros.
    case_eq (nvl_pbase nvldata); try congruence.
    intros.
    generalize (nvl_primary_base_dynamic H_nvldata H0).
    intros.
    generalize (nvl_primary_base H_nvldata H0).
    intros.
    assert ((nvl_offsets nvldata) ! i <> None) by congruence.
    destruct (nvl_exist H_nvldata i).
    generalize (H5 (or_introl _ H3)).
    intros.
    eapply is_dynamic_base.
    eassumption.
    eassumption.
    assumption.

    intros until 1.
    intro.
    replace c with h by congruence.
    generalize (nvl_exist H_nvldata bi).
    rewrite H_nvldata_2.
    simpl .
    tauto.

    intros.
    replace c with h by congruence.
    revert H.
    generalize (nvl_exist H_nvldata bi).
    rewrite H_nvldata_2.
    simpl.
    tauto.

    intros; eauto using nvl_primary_base.

    intros; eauto using nvl_low_bound.

    intros; eauto using nvl_dynamic_no_primary_low_bound.

    intros; eauto using nvl_align_dynamic, fl_align_nvl, Zdivide_trans.

    intros until 1.
    rewrite (nvl_offsets_offsets' H).
    intros; eauto using nvl_offset_align.

    intros until 4.
    rewrite (nvl_offsets_offsets' H).
    rewrite (nvl_offsets_offsets' H1).
    intros.
    generalize (nvl_nonempty_non_overlap H_nvldata H H0 H1 H2 H3 H4 H5).
    generalize (non_virtual_data_size_non_virtual_size Hld H4).
    generalize (non_virtual_data_size_non_virtual_size Hld H5).
    omega.

    intros until 2.
    rewrite (nvl_offsets_offsets' H0).
    intros.
    generalize (nvl_nonempty_high_bound H_nvldata H H0 H1).
    generalize (non_virtual_data_size_non_virtual_size Hld H1).
    omega.

    eauto using nvl_data_low_bound.

    eauto using nvl_data_dynamic_low_bound.

    intros.
    replace c with h in * by congruence.
    generalize (fl_exist H_fldata f).
    rewrite H_fldata_2.
    simpl.
    tauto.

    intros.
    replace c with h in * by congruence.
    generalize (fl_exist H_fldata f).
    rewrite H_fldata_2.
    simpl.
    tauto.

    intros.
    apply Zle_trans with (nvl_nvds nvldata).
     eauto using nvl_data_low_bound.
    eauto using fl_low_bound.

    intros; eauto using fl_low_bound.

    intros until 1.
    generalize (fl_offset_align H_fldata H).
    unfold field_align.
    case_eq (FieldSignature.type f).
     tauto.
    intros until 1.
    rewrite (fl_offsets_offsets' H H0).
    tauto.

    intros until 5.
    generalize (fl_non_overlap H_fldata H H0 H3).
    unfold field_size, field_data_size.
    case_eq (FieldSignature.type f1).
     case_eq (FieldSignature.type f2).
      tauto.
      intros until 1.
      rewrite (fl_offsets_offsets' H0 H4).
      case_eq ((offsets ld) ! struct); try congruence.
       intros.
       generalize (data_size_high_bound (offsets_intro ( Hld) H5)).
       generalize (virtual_base_offsets_data_size (offsets_intro Hld H5) (virtual_base_offsets_self (offsets_intro Hld H5))(H2 _ _ H4) H5).
       generalize (non_virtual_data_size_own_fields_offset (offsets_intro Hld H5)).
       generalize (own_fields_offset_low_bound (offsets_intro Hld H5)).
       generalize (H7 _ (refl_equal _) _ (refl_equal _)).
       injection H8; intro; subst.
       Opaque Zminus. injection H9; intro; subst.
       Transparent Zminus. omega.
     intros until 1.
   rewrite (fl_offsets_offsets' H H4).
   case_eq ((offsets ld) ! struct); try congruence.
   intros until 1.
   generalize (data_size_high_bound (offsets_intro ( Hld) H5)).
   intro.
       generalize (virtual_base_offsets_data_size (offsets_intro Hld H5) (virtual_base_offsets_self (offsets_intro Hld H5))(H1 _ _ H4) H5).
       generalize (non_virtual_data_size_own_fields_offset (offsets_intro Hld H5)).
       generalize (own_fields_offset_low_bound (offsets_intro Hld H5)).
  intros until 3.
  case_eq (FieldSignature.type f2).
   Opaque Zminus. injection 3; intro; subst.
   injection 1; intro; subst.
   generalize (H11 _ (refl_equal _) _ (refl_equal _)).
   omega.
  intros until 1.
  rewrite (fl_offsets_offsets' H0 H10).
  case_eq ((offsets ld) ! struct0); try congruence.
  intros until 1.
   generalize (data_size_high_bound (offsets_intro ( Hld) H11)).
   intro.
       generalize (virtual_base_offsets_data_size (offsets_intro Hld H11) (virtual_base_offsets_self (offsets_intro Hld H11))(H2 _ _ H10) H11).
       generalize (non_virtual_data_size_own_fields_offset (offsets_intro Hld H11)).
       generalize (own_fields_offset_low_bound (offsets_intro Hld H11)).
  injection 5; intro; subst.
  injection 1; intro; subst.
  generalize (H16 _ (refl_equal _) _ (refl_equal _)).
  omega.

  intros.
  destruct (is_dynamic_dec hierarchy_wf (cilimit ld)).
   generalize (nvl_data_dynamic_low_bound H_nvldata i).
   generalize (fl_data_low_bound H_fldata).
   generalize (dynamic_type_data_size_low_bound PF).
   omega.
  case_eq (Class.fields h).
   intros.
   pose (F := fun cl => match cl with
                          | (Class.Inheritance.Repeated, ci) => if is_empty_dec hierarchy_wf ci then false else true
                          | _ => false
                        end).
   case_eq (filter F (Class.super h)).
    intros.
    destruct H.
    econstructor.
    eassumption.
    assumption.
    intros.
    destruct n.
    eapply is_dynamic_virtual_methods.
    eassumption.
    eauto.
   intros.
   destruct n.
   eapply is_dynamic_virtual_base.
   eleft.
   eassumption.
   eassumption.
   intros.
   generalize (filter_In F (Class.Inheritance.Repeated, b) (Class.super h)).
   rewrite H1.
   simpl.
   destruct 1.
   destruct (is_empty_dec hierarchy_wf b).
    assumption.
   destruct H3.
   auto.
   intros.
   generalize (filter_In F p (Class.super h)).
   destruct p.
   rewrite H1.
   simpl.
   destruct 1.
   destruct (H2 (or_introl _ (refl_equal _))).
   destruct t; try discriminate.
   destruct (is_empty_dec hierarchy_wf i); try discriminate.
   assert ((offsets ld) ! i <> None) by eauto using Well_formed_hierarchy.well_founded, Well_formed_hierarchy.complete, offsets_exist.
   case_eq ((offsets ld) ! i); try congruence.
   intros.
   generalize (nonempty_non_virtual_data_size_positive (offsets_intro ( Hld) H7) n0).
   intros.
   destruct (nvl_exist H_nvldata i).
   generalize (H9 H4).
   rewrite H_nvldata_2.
   simpl.
   destruct 1; try contradiction.
   case_eq ((nvl_offsets nvldata) ! i); try congruence.
   intros.
   generalize (nvl_low_bound H_nvldata H12).
   generalize (nvl_nonempty_high_bound H_nvldata n0 H12 H7).
   generalize (fl_data_low_bound H_fldata).
   generalize (non_virtual_size_positive (offsets_intro Hld H7)).
   omega.
   intros.
   generalize (fl_exist H_fldata t).
   rewrite H0.
   rewrite H_fldata_2.
   simpl.
   destruct 1.
   destruct (H1 (or_introl _ (refl_equal _))); try contradiction.
   case_eq (assoc (FieldSignature.eq_dec (A := A)) t (fl_offsets fldata)); try congruence.
   intros.
   generalize (fl_low_bound H_fldata H4).
   generalize (nvl_data_low_bound H_nvldata).
   generalize (fl_high_bound H_fldata H4).
   unfold field_size.
   case_eq (FieldSignature.type t).
    intros.
    generalize (H6 _ (refl_equal _)).
    generalize (typ_size_positive PF ( t0)).
    omega.
   intros until 1.
   case_eq ((offsets ld) ! struct); try congruence.
   intros.
   generalize (H7 _ (refl_equal _)).
   generalize (size_positive (offsets_intro ( Hld)) H6).
   intros.
   generalize (Zpos_positive arraysize).
   intros.
   Transparent Zminus. assert (0 <= Zpos arraysize - 1) by omega.
   assert (0 <= LayoutConstraints.size t0) by omega.
   generalize (Zmult_ge H13 H14).
   omega.
   intros.
   assert (In t (Class.fields h)).
     rewrite H0; auto.
   assert ((offsets ld) ! struct <> None) by eauto using Well_formed_hierarchy.well_founded_struct, Well_formed_hierarchy.complete_struct, offsets_exist.
   contradiction.

   intros until 1.
   intros _.
   generalize (fl_high_bound H_fldata H).
   unfold field_data_size, field_size.
   case_eq (FieldSignature.type f).
    injection 3; intro; subst.
    generalize (H1 _ (refl_equal _)).
   tauto.
   intros until 1.
   rewrite (fl_offsets_offsets' H H0).
   case_eq ((offsets ld) ! struct); try congruence.
   Opaque Zminus. injection 3; intros; subst.
   generalize (H2 _ (refl_equal _)).
   generalize (data_size_high_bound (offsets_intro ( Hld) H1)).
   omega.

   intros until 1.
   generalize (fl_high_bound H_fldata H).
   unfold field_size.
   generalize (fl_data_size H_fldata).
   case_eq (FieldSignature.type f).
    injection 4; intros; subst.
    generalize (H2 _ (refl_equal _ )).
  omega.
   intros until 1.
   rewrite (fl_offsets_offsets' H H0).
   case_eq ((offsets ld) ! struct); try congruence.
   injection 4; intros; subst.
   generalize (H3 _ (refl_equal _)).
   omega.

   eauto using fl_data_low_bound, Zle_trans, fl_size_low_bound.

   intros until 1.
   rewrite (nvl_offsets_offsets' H).
   intros; eauto using nvl_high_bound, fl_size_low_bound, Zle_trans.

   intros until 1.
   case_eq ((nvl_offsets nvldata) ! bi); try congruence.
   intros until 1.
   rewrite (nvl_offsets_offsets' H0).
   intros; eauto using nvl_align_prop, Zdivide_trans, fl_align_nvl.

   intros until 1.
   case_eq ( assoc (FieldSignature.eq_dec (A := A)) f (fl_offsets fldata)); try congruence.
   intros until 1.
   generalize (fl_align_prop H_fldata H).
   unfold field_align.
   case_eq (FieldSignature.type f).
    tauto.
   intros until 1.
   rewrite (fl_offsets_offsets' H0 H1).
   tauto.

   intros.
   rewrite PTree.gso.
   destruct (vl_exist H_vldata b).
   generalize (H0 H).
   rewrite H_vldata_2.
   simpl.
   tauto.
   intro; subst b.
   generalize (Well_formed_hierarchy.is_virtual_base_of_lt hierarchy_wf H).
   apply Plt_irrefl.

   intro.
   destruct (peq b (cilimit ld)).
    tauto.
   rewrite PTree.gso.
   destruct (vl_exist H_vldata b).
   rewrite H_vldata_2 in H0.
   simpl in H0.
   tauto.
   assumption.

   apply PTree.gss.

   intro.
   destruct (peq b (cilimit ld)).
    subst.
    rewrite PTree.gss.
    injection 1; intros; subst.
    exists 0; omega.
   rewrite PTree.gso.
   intros until 1.
   rewrite (vl_offsets_offsets' H).
   eauto using vl_offset_align.
   assumption.

   intros ? ?.
   destruct (peq b (cilimit ld)).
    subst.
    rewrite PTree.gss.
    injection 1; intros; subst.
    omega.
   rewrite PTree.gso.
   eauto using vl_low_bound.
   assumption.

   intros ? ?.
   destruct (peq b1 (cilimit ld)).
    subst.
    rewrite PTree.gss.
    injection 1; intro; subst.
    simpl.
    intros.
    rewrite PTree.gso in H1.
    unfold offsets' in H0.
    rewrite PTree.gss in H0.
    rewrite (vl_offsets_offsets' H1) in H2.
    left.
    injection H0; intro; subst bo1.
    simpl.
    eauto using vl_nonempty_low_bound.
    congruence.
   rewrite PTree.gso.
   intro.
   rewrite (vl_offsets_offsets' H).
   intros until 1.
   intros ? ?.
   destruct (peq b2 (cilimit ld)).
    subst.
    rewrite PTree.gss.
    injection 1; intro; subst.
    unfold offsets'.
    rewrite PTree.gss.
    injection 1; intro; subst bo2.
    simpl.
    intros.
    right.
    eauto using vl_nonempty_low_bound.
   rewrite PTree.gso.
   intro.
   rewrite (vl_offsets_offsets' H1).
   intros.
   generalize (non_virtual_data_size_non_virtual_size Hld H0).
   generalize (non_virtual_data_size_non_virtual_size Hld H2).
   generalize (vl_nonempty_non_overlap H_vldata H H3 H1 H4 H5 H0 H2).
   omega.
   assumption.
   assumption.

  intros ? ?.
  destruct (peq bi (cilimit ld)).
   subst.
   rewrite PTree.gss.
   injection 1; intro; subst.
   unfold offsets'.
   rewrite PTree.gss.
   injection 2; intro; subst bo.
   simpl.
   eauto using vl_data_low_bound.
  rewrite PTree.gso.
  unfold offsets'.
  rewrite PTree.gso.
  intros.
  generalize (vl_nonempty_high_bound H_vldata H0 H H1).
  generalize (non_virtual_data_size_non_virtual_size Hld H1).
  omega.
  assumption.
  assumption.

  apply Zle_trans with (vl_size vldata).
  eauto using vl_data_size.
  assumption.

  unfold offsets'.
  intro.
  destruct (peq bi (cilimit ld)).
   subst.
   rewrite PTree.gss.
   rewrite PTree.gss.
   injection 1; intro; subst.
   injection 1; intro; subst bo.
   simpl.
   eauto using Zle_trans, vl_size_low_bound.
  rewrite PTree.gso.
  rewrite PTree.gso.
  intros.
  eauto using Zle_trans, vl_high_bound.
  assumption.
  assumption.

  unfold offsets'.
  intro.
  destruct (peq b (cilimit ld)).
   subst.
   rewrite PTree.gss.
   rewrite PTree.gss.
   injection 2; intro; subst bo.
   simpl.
   eauto using vl_align_field.
  rewrite PTree.gso.
  rewrite PTree.gso.
  eauto using vl_align_prop.
  assumption.
  assumption.

  assumption.

  eauto using vl_align_pos.

  eauto using fl_align_pos.

  generalize (nvl_size_pos H_nvldata).
  generalize (fl_size_low_bound H_fldata).
  omega.

Qed.

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.

  apply non_virtual_empty_base_offsets_eq with (PF := PF).
   eauto.
   intros; symmetry; eauto using offsets'_eq.
   eauto using offsets_guard.
   eauto using offsets_preserve_old, offsets_intro.
Qed.

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.

  apply empty_base_offsets_eq with (PF := PF).
   eauto.
   intros; symmetry; eauto using offsets'_eq.
   eauto using offsets_guard.
   eauto using offsets_preserve_old, offsets_intro.
Qed.

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.

  intros.
  eapply disjoint_empty_base_offsets_eq.
  eauto.
  intros.
  symmetry.
  eapply offsets'_eq.
  eassumption.
  eauto using offsets_guard.
  unfold offsets'.
  intro.
  destruct (peq ci0 (cilimit ld)).
   subst.
   rewrite PTree.gss.
   intros; congruence.
  rewrite PTree.gso; eauto using offsets_guard.
  eauto using offsets'_preserve, offsets_intro.
  assumption.
  rewrite (offsets'_eq H) in H0.
  eassumption.
  rewrite (offsets'_eq H) in H0.
  eauto using disjoint_ebo.
  assumption.
Qed.

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.

  apply non_virtual_empty_base_offsets_eq with (PF := PF).
   eauto.
   intros; eauto using offsets'_eq.
   unfold offsets'.
   intro.
   destruct (peq ci (cilimit ld)).
    subst.
    rewrite PTree.gss.
    congruence.
   rewrite PTree.gso; eauto using offsets_guard.
   eauto using offsets_preserve_old.
Qed.

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.

  apply empty_base_offsets_eq with (PF := PF).
   eauto.
   intros; eauto using offsets'_eq.
   unfold offsets'.
   intro.
   destruct (peq ci (cilimit ld)).
    subst.
    rewrite PTree.gss.
    congruence.
   rewrite PTree.gso; eauto using offsets_guard.
   eauto using offsets_preserve_old.
Qed.

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

Proof.

  unfold Nvebo.
  unfold nvebo0.
  split.
   intro.
   destruct (in_app_or _ _ _ H).
    revert H0.
    case (is_empty_dec hierarchy_wf (cilimit ld)); simpl; try tauto.
    destruct 2; try contradiction.
    injection H0; intros; subst b o.
    constructor.
    assumption.
    trivial.
   destruct (in_app_or _ _ _ H0).
    destruct (nvl_nvebo_prop H_nvldata b o).
    destruct (H2 H1).
    destruct H4.
    destruct H4.
    eapply non_virtual_empty_base_offset_non_virtual_base.
    unfold offsets'.
    rewrite PTree.gss.
    reflexivity.
    simpl.
    eassumption.
    eauto using non_virtual_empty_base_offset_old, nvl_offsets_lt.
   destruct (fl_ebo_prop H_fldata b o).
   destruct (H2 H1).
   destruct H4.
   destruct H4.
   destruct H5.
   destruct H5.
   destruct H5.
   destruct H6.
   destruct H6.
   destruct H7.
   destruct H8.
   destruct H8.
   assert (assoc (FieldSignature.eq_dec (A := A)) x (fl_offsets fldata) <> None) by congruence.
   destruct (fl_exist H_fldata x).
   generalize (H12 (or_introl _ H10)).
   intros.
   assert (Plt x1 (cilimit ld)) by eauto using Well_formed_hierarchy.well_founded_struct.
   eapply non_virtual_empty_base_offset_field.
   unfold offsets'.
   rewrite PTree.gss.
   reflexivity.
   simpl.
   eassumption.
   eassumption.
   rewrite (offsets'_eq H14).
   eassumption.
   eassumption.
   assumption.
   eapply empty_base_offset_old.
   assumption.
   assumption.
  intro.
  apply in_or_app.
  inversion H; subst.
   left.
   case (is_empty_dec hierarchy_wf (cilimit ld)); simpl; tauto.
  right.
  apply in_or_app.
   revert H0.
   unfold offsets'.
   rewrite PTree.gss.
   injection 1; intro; subst oc.
   simpl in H1.
   left.
   destruct (nvl_nvebo_prop H_nvldata b o).
   apply H4.
   esplit.
   esplit.
   split.
   eassumption.
   eapply non_virtual_empty_base_offset_new.
   eauto using nvl_offsets_lt.
   assumption.
  right.
  apply in_or_app.
  right.
  revert H0.
  unfold offsets'.
  rewrite PTree.gss.
  injection 1; intro; subst oc.
  destruct (fl_ebo_prop H_fldata b o).
  apply H8.
  simpl in H1.
  assert ( assoc (FieldSignature.eq_dec (A := A)) f (fl_offsets fldata) <> None) by congruence.
  generalize (fl_exist H_fldata f).
  rewrite H_fldata_2.
  simpl.
  destruct 1.
  generalize (H11 (or_introl _ H9)).
  intros.
  esplit.
  esplit.
  split.
  eassumption.
  esplit.
  esplit.
  split.
  eassumption.
  esplit.
  split.
  eassumption.
  split.
  assumption.
  assert (Plt cif (cilimit ld)) by eauto using Well_formed_hierarchy.well_founded_struct.
  esplit.
  split.
  rewrite <- (offsets'_eq H13).
  eassumption.
  eapply empty_base_offset_new.
  assumption.
  assumption.
Qed.

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

Proof.

  constructor.

  destruct 1.
  subst.
  simpl.
  intros.
  eauto 6 using nvl_disjoint_empty_bases, non_virtual_empty_base_offset_new, nvl_offsets_lt.

  subst.
  simpl.
  intro.
  destruct (peq ci1 (cilimit ld)).
   subst.
   rewrite PTree.gss.
   injection 1; intro; subst.
   intros until 2.
   rewrite PTree.gso in H0.
   simpl.
   intros.
   intro.
   subst.
   destruct (Nvebo_prop bi (o2 + x2)).
   generalize (H5 H2).
   intro.
   destruct (vl_exist H_vldata ci2).
   assert ((vl_offsets vldata) ! ci2 <> None) by congruence.
    generalize (H8 (or_introl _ H9)).
    intros.
    eapply vl_disjoint_empty_bases_main.
    eauto.
    eassumption.
    eapply non_virtual_empty_base_offset_new.
    eauto using Well_formed_hierarchy.is_virtual_base_of_lt.
    eassumption.
    assumption.
    congruence.
   rewrite PTree.gso.
   intros until 1.
   intro.
   destruct (peq ci2 (cilimit ld)).
    subst.
    rewrite PTree.gss.
    injection 1; intro; subst.
    simpl.
    intros.
    intro.
    subst.
   destruct (Nvebo_prop bi (o1 + x1)).
   generalize (H5 H3).
   intro.
   destruct (vl_exist H_vldata ci1).
   assert ((vl_offsets vldata) ! ci1 <> None) by congruence.
    generalize (H8 (or_introl _ H9)).
    intros.
    eapply vl_disjoint_empty_bases_main.
    eauto.
    eassumption.
    eapply non_virtual_empty_base_offset_new.
    eauto using Well_formed_hierarchy.is_virtual_base_of_lt.
    eassumption.
    assumption.
   rewrite PTree.gso.
   intros.
   eapply vl_disjoint_empty_bases.
   eauto.
   eassumption.
   eassumption.
   assumption.
   eapply non_virtual_empty_base_offset_new.
   destruct (vl_exist H_vldata ci1).
   eapply Well_formed_hierarchy.is_virtual_base_of_lt.
   eauto.
   apply H5.
   left; congruence.
   eassumption.
   eapply non_virtual_empty_base_offset_new.
   destruct (vl_exist H_vldata ci2).
   eapply Well_formed_hierarchy.is_virtual_base_of_lt.
   eauto.
   apply H5.
   left; congruence.
   eassumption.
   assumption.
   assumption.

  simpl.
  intros.
  cut (o2 + p2 * LayoutConstraints.size of2 + x2 <> o1 + x1).
   congruence.
  assert (Plt ci1 (cilimit ld)).
   destruct (nvl_exist H_nvldata ci1).
   eapply Well_formed_hierarchy.well_founded.
   eauto.
   eassumption.
   eapply H8.
   left.
   congruence.
  assert (Plt ci2 (cilimit ld)).
   destruct (fl_exist H_fldata f2).
   eapply Well_formed_hierarchy.well_founded_struct.
   eauto.
   eassumption.
   eapply H9.
   left.
   congruence.
   eassumption.
  eapply fl_disjoint_empty_bases.
  eauto.
  eassumption.
  eassumption.
  assumption.
  assumption.
  rewrite <- (offsets'_eq H8).
  assumption.
  eapply empty_base_offset_new.
  assumption.
  eassumption.
  eassumption.
  eapply non_virtual_empty_base_offset_new.
  assumption.
  assumption.

  simpl.
  intros.
  assert (Plt ci1 (cilimit ld)).
   destruct (fl_exist H_fldata f1).
   eapply Well_formed_hierarchy.well_founded_struct.
   eauto.
   eassumption.
   eapply H13.
   left.
   congruence.
   eassumption.
  assert (Plt ci2 (cilimit ld)).
   destruct (fl_exist H_fldata f2).
   eapply Well_formed_hierarchy.well_founded_struct.
   eauto.
   eassumption.
   eapply H14.
   left.
   congruence.
   eassumption.
  eapply fl_disjoint_field_empty_bases.
  eauto.
  eassumption.
  eassumption.
  assumption.
  assumption.
  rewrite <- (offsets'_eq H12).
  assumption.
  eapply empty_base_offset_new.
  assumption.
  eassumption.
  eassumption.
  eassumption.
  assumption.
  assumption.
  rewrite <- (offsets'_eq H13).
  assumption.
  eapply empty_base_offset_new.
  assumption.
  assumption.
  assumption.
Qed.

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.

  constructor; simpl.

   unfold offsets'.
   intro.
   case (peq ci (cilimit ld)).
    intros; subst.
    congruence.
   intro.
   rewrite PTree.gso; eauto using offsets_guard.

   unfold offsets' at 1.
   intros ? ?.
   destruct (peq ci (cilimit ld)).
    subst.
    rewrite PTree.gss.
    injection 1; intro; subst of.
    eauto using offsets'_preserve.
   rewrite PTree.gso.
   intros.
   assert ((offsets ld) ! ci <> None) by congruence.
   generalize (offsets_guard2 ( Hld) H0).
   intros.
   rewrite <- (offsets'_eq H1) in H.
   eauto using offsets_preserve_old.
   assumption.

   unfold offsets'.
   intro.
   destruct (peq ci (cilimit ld)).
    subst.
    rewrite PTree.gss.
    intros.
    apply Plt_succ.
   rewrite PTree.gso.
   intros.
   generalize (offsets_guard2 ( Hld) H).
   intros; eauto using Plt_trans, Plt_succ.
   assumption.

   intros ? ?.
   unfold offsets'.
   destruct (peq ci (cilimit ld)).
    subst.
    rewrite PTree.gss.
    injection 1; intro; subst of.
    simpl.
    eauto using fl_data_size.
   rewrite PTree.gso; eauto using non_virtual_data_size_non_virtual_size.

   intros.
   unfold offsets'.
   destruct (peq ci (cilimit ld)).
    subst.
    rewrite PTree.gss.
    congruence.
   rewrite PTree.gso.
   destruct (Plt_succ_inv _ _ H).
    eauto using offsets_exist.
   contradiction.
   assumption.

   intros.
   generalize H.
   unfold offsets' at 1.
   destruct (peq ci (cilimit ld)).
    subst.
    rewrite PTree.gss.
    injection 1; intro; subst o'0.
    eauto using disjoint_empty_base_offsets_new.
   rewrite PTree.gso.
   intros.
   assert (Plt ci (cilimit ld)).
    eapply offsets_guard2.
    eauto.
    congruence.
   eauto using disjoint_empty_base_offsets_old.
   assumption.

   intros ? ?.
   destruct (peq ci (cilimit ld)).
    subst.
    rewrite PTree.gss.
    injection 1; intro; subst.
    split.
    intros.
    destruct (in_app_or _ _ _ H0).
     destruct (Nvebo_prop b o'0).
      econstructor.
      unfold offsets'.
      rewrite PTree.gss.
      reflexivity.
      simpl.
      rewrite PTree.gss.
      reflexivity.
      replace (o'0 - 0) with o'0.
      auto.
      Transparent Zminus. omega.
    destruct (vl_nvebo_prop H_vldata b o'0).
    destruct (H2 H1).
    destruct H4.
    destruct H4.
    assert ((vl_offsets vldata) ! x <> None) by congruence.
    destruct (vl_exist H_vldata x).
    generalize (H8 (or_introl _ H6)).
    intros.
    assert (Plt x (cilimit ld)) by eauto using Well_formed_hierarchy.is_virtual_base_of_lt.
    econstructor.
    unfold offsets'.
    rewrite PTree.gss.
    reflexivity.
    simpl.
    rewrite PTree.gso.
    eassumption.
    intro; subst.
    eapply Plt_irrefl.
    eauto.
   eauto using non_virtual_empty_base_offset_old.
  inversion 1.
  subst.
  revert H1.
  unfold offsets'.
  rewrite PTree.gss.
  injection 1; intro; subst oc.
  apply in_or_app.
  revert H2.
  simpl.
  destruct (peq ci' (cilimit ld)).
   subst.
   rewrite PTree.gss.
   injection 1; intro; subst.
   left.
   destruct (Nvebo_prop b o'0).
    apply H5.
    replace o'0 with (o'0 - 0) by omega.
    assumption.
   rewrite PTree.gso.
   intros.
   right.
    destruct (vl_nvebo_prop H_vldata b o'0).
    apply H5.
    esplit.
    esplit.
    split.
    eassumption.
    eapply non_virtual_empty_base_offset_new.
    eapply Well_formed_hierarchy.is_virtual_base_of_lt.
    eauto.
    destruct (vl_exist H_vldata ci').
    apply H7.
    left.
    congruence.
   assumption.
   assumption.
  rewrite PTree.gso.
  intros.
  assert ((ebo ld) ! ci <> None) by congruence.
  generalize (ebo_guard ( Hld) H0) .
  intros.
  generalize (@empty_base_offset_new _ H1 b o'0).
  generalize (@empty_base_offset_old _ H1 b o'0).
  generalize (ebo_prop ( Hld) H b o'0).
  tauto.
  assumption.

  intros.
  destruct (peq ci (cilimit ld)).
   subst.
   rewrite PTree.gss.
   congruence.
  rewrite PTree.gso.
  eapply ebo_exist.
  eauto.
  destruct (Plt_succ_inv _ _ H).
   assumption.
  contradiction.
  assumption.

  intro.
  destruct (peq ci (cilimit ld)).
   subst.
   intros; apply Plt_succ.
  rewrite PTree.gso; intros; eauto using Plt_trans, Plt_succ, ebo_guard.

  intros ? ?.
  destruct (peq ci (cilimit ld)).
   subst.
   rewrite PTree.gss.
   injection 1; intro; subst e.
   eapply Nvebo_prop.
  rewrite PTree.gso.
  intros.
  assert ((nvebo ld) ! ci <> None) by congruence.
  assert (Plt ci (cilimit ld)) by eauto using nvebo_guard.
  generalize (@non_virtual_empty_base_offset_old _ H1 b o'0).
  generalize (@non_virtual_empty_base_offset_new _ H1 b o'0).
  generalize (nvebo_prop ( Hld) H b o'0).
  tauto.
  assumption.

  intros.
  destruct (peq ci (cilimit ld)).
   subst.
   rewrite PTree.gss.
   congruence.
  rewrite PTree.gso.
  eapply nvebo_exist.
  eauto.
  destruct (Plt_succ_inv _ _ H).
   assumption.
  contradiction.
  assumption.

  intro.
  destruct (peq ci (cilimit ld)).
   subst.
   intros; apply Plt_succ.
  rewrite PTree.gso; intros; eauto using Plt_trans, Plt_succ, nvebo_guard.

Qed.

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

Proof.

  split.
  apply step'.
  reflexivity.
Qed.

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.

  split; try trivial.
  inversion Hld.
  constructor; simpl; try assumption.

  intros; eauto using Plt_succ, Plt_trans.

  intros.
  eapply offsets_exist.
  eassumption.
  destruct (peq ci (cilimit ld)).
   subst.
   contradiction.
  destruct (Plt_succ_inv _ _ H).
   assumption.
  contradiction.
  assumption.

  intros ? ?.
  destruct (peq ci (cilimit ld)).
   subst.
   rewrite PTree.gss.
   injection 1; intros; subst; simpl.
   split.
    tauto.
   inversion 1; subst.
   assert ((offsets ld) ! (cilimit ld) <> None) by congruence.
   assert (hierarchy ! (cilimit ld) <> None) by eauto.
   contradiction.
   rewrite PTree.gso; eauto.

  intros.
  destruct (peq ci (cilimit ld)).
   subst.
   rewrite PTree.gss.
   congruence.
  rewrite PTree.gso.
  eapply ebo_exist.
  eauto.
  destruct (Plt_succ_inv _ _ H).
   assumption.
  contradiction.
  assumption.

  intro.
  destruct (peq ci (cilimit ld)).
   subst.
   intros; apply Plt_succ.
  rewrite PTree.gso; intros; eauto using Plt_trans, Plt_succ, ebo_guard.

  intros ? ?.
  destruct (peq ci (cilimit ld)).
   subst.
   rewrite PTree.gss.
   injection 1; intro; subst e.
   simpl.
   split.
    tauto.
   inversion 1; subst.
    inversion H1; congruence.
   assert ((offsets ld) ! (cilimit ld) <> None) by congruence.
   assert (hierarchy ! (cilimit ld) <> None) by eauto.
   contradiction.
   assert ((offsets ld) ! (cilimit ld) <> None) by congruence.
   assert (hierarchy ! (cilimit ld) <> None) by eauto.
   contradiction.
  rewrite PTree.gso; eauto.

  intros.
  destruct (peq ci (cilimit ld)).
   subst.
   rewrite PTree.gss.
   congruence.
  rewrite PTree.gso.
  eapply nvebo_exist.
  eauto.
  destruct (Plt_succ_inv _ _ H).
   assumption.
  contradiction.
  assumption.

  intro.
  destruct (peq ci (cilimit ld)).
   subst.
   intros; apply Plt_succ.
  rewrite PTree.gso; intros; eauto using Plt_trans, Plt_succ, nvebo_guard.

Qed.

End Undef.

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

Proof.

case_eq (hierarchy ! (cilimit ld)); eauto using layout_step_defined, layout_step_undefined.
Qed.

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.

  split; try trivial.
  constructor; simpl; try (intros; rewrite PTree.gempty in *; simpl in *); try congruence.

  destruct ci; simpl in *; discriminate.

  destruct ci; simpl in *; discriminate.

  destruct ci; simpl in *; discriminate.

Qed.

Let max0 := max_index hierarchy.

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

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

Proof.

  unfold max.
  destruct max0.
  assumption.
Qed.

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

Proof.

  cut (forall j, Plt j max -> forall ld,
    prop hierarchy ld ->
    cilimit ld = j -> {
  ld'0 | prop hierarchy ld'0 /\ cilimit ld'0 = max
  }).
  intros.
  destruct (plt xH max).
   destruct (empty_layout).
   destruct a.
   eauto.
  unfold Plt in n.
  destruct (peq max xH).
   rewrite e.
   exact empty_layout.
  assert (Zpos max <> Zpos xH) by congruence.
  assert (Plt max xH).
   unfold Plt.
   omega.
  generalize H0.
  generalize max.
  intro.
  intro.
  destruct max1; simpl in *; discriminate.
induction j using (well_founded_induction_type (bounded_gt_wf max)).
intros.
subst.
destruct (layout_step H0).
destruct a.
destruct (peq (Psucc (cilimit ld)) max).
  rewrite <- e.
  esplit.
  esplit.
   eassumption.
   assumption.
  assert (Plt (Psucc (cilimit ld)) max).
  unfold Plt in *.
  assert (Zpos (Psucc (cilimit ld)) <> Zpos max) by congruence.
  rewrite Psucc_Zsucc in *.
  unfold Zsucc in *.
  omega.
  eapply (X (Psucc (cilimit ld))).
  split.
    apply Plt_succ.
    assumption.
   assumption.
   eassumption.
   assumption.
Qed.

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.

destruct (layout_end).
destruct a.
inversion H.
exists (offsets x).
split.
  split.
  intros.
  eapply offsets_exist.
  eassumption.
  rewrite H0.
  eauto.
assumption.
auto.
  split; eauto.
Qed.

End Layout.

End CVABI.

Module CommonVendorABILayout

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