Require Import LibLists.
Require Import Maps.
Require Import Cplusconcepts.
Require Import Coqlib.
Require Import Tactics.
Require Import CplusWf.
Require Import LibMaps.

General-purpose tools

Load Param.

  Ltac try_dependent_revert i :=
    match goal with
      | h: ?P |- _ =>
        match P with
          | context [ i ] => revert h
        end
    end.
  Ltac dependent_revert i :=
    repeat try_dependent_revert i;
      revert i.


Remark option_eq_dec : forall (T : Type) (T_eq_dec : forall t1 t2 : T, {t1 = t2} + {t1 <> t2}),
  forall l1 l2 : option T, {l1 = l2} + {l1 <> l2}.

Remark prod_eq_dec : forall (U : Type) (U_eq_dec : forall u1 u2 : U, {u1 = u2} + {u1 <> u2})
  (V : Type) (V_eq_dec : forall v1 v2 : V, {v1 = v2} + {v1 <> v2})
  (p1 p2 : U * V), {p1 = p2} + {p1 <> p2}.


    Remark Zpos_positive : forall n, 0 < Zpos n.

Remark Zpos_minus_1_nonnegative : forall n, 0 <= Zpos n - 1.

    Remark Zmult_ge : forall a b, 0 <= a -> 0 <= b -> 0 <= a * b.

    Remark Zmult_gt : forall a b, 0 < a -> 0 < b -> 0 < a * b.

    Remark Zmult_distr_1: forall x y, x * y + y = (x + 1) * y.

    Remark array_cells_disjoint : forall i j, i <> j -> forall s, 0 < s ->
      i * s + s <= j * s \/ j * s + s <= i * s.

     Remark distinct_paths_cases : forall (A : Type) (aeq : forall a1 a2 : A, {a1 = a2} + {a1 <> a2}) (l1 l2 : _ A),
       (length l1 <= length l2)%nat ->
       l1 <> l2 ->
       {a : _ & {l2' | l2 = l1 ++ a :: l2'}} +
       {l : _ & { a1 : _ & { a2 : _ & { l1' : _ & { l2' |
         l1 = l ++ a1 :: l1' /\ l2 = l ++ a2 :: l2' /\ a1 <> a2}}}}}.

Remark distinct_lists_rect : forall (A : Type) (aeq : forall a1 a2 : A, {a1 = a2} + {a1 <> a2}) (P : list A -> list A -> Type),
       (forall l1 l2, P l1 l2 -> P l2 l1) ->
       (forall l1 a l2', P l1 (l1 ++ a :: l2')) ->
       (forall l a1 l1' a2 l2', a1 <> a2 -> P (l ++ a1 :: l1') (l ++ a2 :: l2')) ->
       forall l1 l2, l1 <> l2 -> P l1 l2.

Requirements for a class to be empty (4.3)

Module Is_empty.

Section Is_empty.

Variable A : ATOM.t.

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

Variable is_empty : ident -> Prop.

Record prop : Prop := intro {
  defined: forall i, is_empty i -> hierarchy ! i <> None;
  fields_struct: forall i,
    is_empty i -> forall c,
      hierarchy ! i = Some c ->
      forall f, In f (Class.fields c) -> exists e, exists he, FieldSignature.type f = FieldSignature.Struct e he
        ;
  fields_struct_empty: forall i,
    is_empty i ->
    forall c, hierarchy ! i = Some c ->
      forall f, In f (Class.fields c) ->
        forall e he, FieldSignature.type f = FieldSignature.Struct e he ->
          is_empty e
          ;
  bases_empty : forall i,
    is_empty i ->
    forall c, hierarchy ! i = Some c ->
      forall h b, In (h, b) (Class.super c) ->
        is_empty b
}.

Hypothesis Hprop : prop.

Lemma no_scalar_fields : forall ci,
  is_empty ci -> forall c,
    hierarchy ! ci = Some c -> forall f,
      In f (Class.fields c) -> forall t,
        FieldSignature.type f = FieldSignature.Scalar t ->
        False.

Lemma path_to : forall to via from by
  (Hpath : path hierarchy to via from by)
  (H_empty_from : is_empty from),
  is_empty to.

Lemma path_from : forall l h to from,
  path hierarchy to l from h ->
    (is_empty to -> False) ->
    (is_empty from -> False).

Lemma array_path_to : forall from zfrom to zto p,
  valid_array_path hierarchy to zto from zfrom p ->
  is_empty from ->
  is_empty to
.

Lemma array_path_from : forall from zfrom to zto p,
  valid_array_path hierarchy to zto from zfrom p ->
  (is_empty to -> False) ->
  is_empty from -> False
.

Lemma relative_pointer_to : forall afrom zfrom a ato i h' p' pto,
   valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
   is_empty afrom ->
   is_empty pto.

Lemma relative_pointer_from : forall afrom zfrom a ato i h' p' pto,
   valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
   (is_empty pto -> False) ->
   is_empty afrom -> False.

End Is_empty.

End Is_empty.

Section OPTIM.

Variable A : ATOM.t.

Record OPTIM : Type := Optim {
  is_empty : PTree.t (Class.t A) -> ident -> Prop;
  is_empty_prop : forall hierarchy, Is_empty.prop hierarchy (is_empty hierarchy);
  is_dynamic : PTree.t (Class.t A) -> ident -> Prop;
  dynamic_nonempty : forall hierarchy id, is_dynamic hierarchy id -> is_empty hierarchy id -> False
}.
 
End OPTIM.

Platform-dependent parameters (4.1)

Section PLATFORM.

Variable A : ATOM.t.

Record PLATFORM : Type := Platform {
  typ_size : Typ.t A -> Z;
  typ_size_positive : forall ty, 0 < typ_size ty;
  typ_align : Typ.t A -> Z;
  typ_align_positive : forall ty, 0 < typ_align ty;
  dynamic_type_data_size : Z;
  dynamic_type_data_size_low_bound : 0 < dynamic_type_data_size;
  dynamic_type_data_align : Z;
  dynamic_type_data_align_low_bound : 0 < dynamic_type_data_align
}.

End PLATFORM.

Section Offsets.

Variable A : ATOM.t.
Variable OP : OPTIM A.
Variable PF : PLATFORM A.

What a layout algorithm is expected to compute (4.2)

    Record t : Type := make {
primary_base : option ident;
non_virtual_direct_base_offsets : PTree.t Z;
own_fields_offset : Z;
field_offsets : list (FieldSignature.t A * Z);
non_virtual_data_size : Z;
non_virtual_size : Z;
non_virtual_align : Z;
virtual_base_offsets : PTree.t Z;
data_size : Z;
size : Z;
align : Z
    }.

  Section OF.

  Variable offsets : PTree.t t.

Computation of offsets (4.4)

    Function field_data_size (f : FieldSignature.t A) : option Z :=
      match FieldSignature.type f with
        | FieldSignature.Scalar ty => Some (typ_size PF ty)
        | FieldSignature.Struct c n =>
          match offsets ! c with
            | Some o => Some ((Zpos n - 1) * size o + data_size o)
            | None => None
          end
      end.

    Function field_size (f : FieldSignature.t A) : option Z :=
      match FieldSignature.type f with
        | FieldSignature.Scalar ty => Some (typ_size PF ty)
        | FieldSignature.Struct c n =>
          match offsets ! c with
            | Some o => Some ((Zpos n - 1) * size o + size o)
            | None => None
          end
      end.
    

    Function field_align (f : FieldSignature.t A) : option Z :=
      match FieldSignature.type f with
        | FieldSignature.Scalar ty => Some (typ_align PF ty)
        | FieldSignature.Struct c n =>
          match offsets ! c with
            | Some o => Some (align o)
            | _ => None
          end
      end.

  Function non_virtual_subobject_offset (accu : Z) (l : list ident) {struct l} : option Z :=
    match l with
      | nil => None
      | a :: l' =>
        match l' with
          | nil => Some accu
          | b :: _ =>
            match offsets ! a with
              | None => None
              | Some o =>
                match (non_virtual_direct_base_offsets o) ! b with
                  | Some of => non_virtual_subobject_offset (accu + of) l'
                  | _ => None
                end
            end
        end
    end.

Fact non_virtual_subobject_offset_app : forall l1 a accu accu',
  non_virtual_subobject_offset accu (l1 ++ a :: nil) = Some accu' ->
  forall l2,
  non_virtual_subobject_offset accu (l1 ++ a :: l2) = non_virtual_subobject_offset accu' (a :: l2)
.

Fact non_virtual_subobject_offset_app_recip : forall l1 a l2 accu accu',
  non_virtual_subobject_offset accu (l1 ++ a :: l2) = Some accu' ->
  exists accu1,
    non_virtual_subobject_offset accu (l1 ++ a :: nil) = Some accu1 /\
    non_virtual_subobject_offset accu1 (a :: l2) = Some accu'
.

Fact non_virtual_subobject_offset_rewrite : forall l accu v,
  non_virtual_subobject_offset accu l = Some v ->
  forall accu',
    non_virtual_subobject_offset accu' l = Some (v + accu' - accu).

Function subobject_offset (ci : ident) (l : list ident) {struct l} : option Z :=
  match offsets ! ci with
    | None => None
    | Some o =>
      match l with
        | nil => None
        | b :: _ =>
          match (virtual_base_offsets o) ! b with
            | None => None
            | Some of => non_virtual_subobject_offset of l
          end
      end
  end.

Function array_path_offset (accu : Z) (ci : ident) (l : array_path A) {struct l} : option Z :=
  match l with
    | nil => Some accu
    | (z, (_, p), f) :: l' =>
      match offsets ! ci with
        | Some o =>
          match subobject_offset ci p with
            | Some off =>
              match Cplusconcepts.last p with
                | Some clast =>
                  match offsets ! clast with
                    | Some olast =>
                      match FieldSignature.type f with
                        | FieldSignature.Struct ci'0 _ =>
                          match assoc (FieldSignature.eq_dec (A := A)) f (field_offsets olast) with
                            | Some fo =>
                              array_path_offset (accu + z * size o + off + fo) ci'0 l'
                            | _ => None
                          end
                        | _ => None
                      end
                    | _ => None
                  end
                | _ => None
              end
            | _ => None
          end
        | _ => None
      end
  end.

 Fact array_path_offset_rewrite : forall accu ci l1 z1,
    array_path_offset accu ci l1 = Some z1 ->
    forall accu',
      array_path_offset accu' ci l1 = Some (z1 + accu' - accu)
      .

 Function relative_pointer_offset (afrom ato : ident) (apath: array_path A) (i : Z) (p : list ident) : option Z :=
   match array_path_offset 0 afrom apath with
     | Some z1 =>
       match offsets ! ato with
         | None => None
         | Some ofto =>
           match subobject_offset ato p with
             | Some z2 => Some (z1 + i * size ofto + z2)
             | _ => None
           end
       end
     | _ => None
   end.

Alternate definition for pointers (relative to a given structure array)

 Inductive relative_pointer_alt: Type :=
   | relative_pointer_alt_intro
     (i : Z) (p : Class.Inheritance.t * list ident)
     (f : option (FieldSignature.t A * array_path A * Z * (Class.Inheritance.t * list ident)))
     .
     
 Function relative_pointer_alt_of_relative_pointer (a : array_path A) (i : Z) (p : Class.Inheritance.t * list ident) {struct a} : relative_pointer_alt :=
   match a with
     | nil => relative_pointer_alt_intro i p None
     | (i', p', f') :: a' => relative_pointer_alt_intro i' p' (Some (f', a', i, p))
   end.
 
 Function relative_pointer_of_relative_pointer_alt (rpa : relative_pointer_alt) : (array_path A * Z * (Class.Inheritance.t * list ident)) :=
   match rpa with
     | relative_pointer_alt_intro i p None => (nil, i, p)
     | relative_pointer_alt_intro i' p' (Some (f', a, i, p)) => ((i', p', f') :: a, i, p)
   end.

 Fact relative_pointer_alt_to_default_to_alt : forall rpa a i p,
   relative_pointer_of_relative_pointer_alt rpa = (a, i, p) ->
   relative_pointer_alt_of_relative_pointer a i p = rpa.

 Fact relative_pointer_default_to_alt_to_default: forall a i p,
   relative_pointer_of_relative_pointer_alt (relative_pointer_alt_of_relative_pointer a i p) = (a, i, p).

 Function relative_pointer_alt_length (rpa : relative_pointer_alt) : nat :=
   match rpa with
     | relative_pointer_alt_intro _ _ None => O
     | relative_pointer_alt_intro _ _ (Some (_, a, _, _)) => S (length a)
   end.

 Fact relative_pointer_alt_length_correct: forall a i p,
   relative_pointer_alt_length (relative_pointer_alt_of_relative_pointer a i p) = length a.


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

 Inductive valid_relative_pointer_alt (afrom : ident) (zfrom : Z) (ato : ident) (pto : ident) : relative_pointer_alt -> Prop :=
 | valid_relative_pointer_alt_intro : forall i',
   0 <= i' -> i' < zfrom -> forall h' p' through,
     path hierarchy through p' afrom h' ->
     forall f',
       match f' with
         | None => ato = afrom /\ pto = through
         | Some (f, a, i, (h, p)) =>
           exists cthrough, hierarchy ! through = Some cthrough /\
             In f (Class.fields cthrough) /\
             exists bfrom, exists bn,
               FieldSignature.type f = FieldSignature.Struct bfrom bn /\
               valid_relative_pointer hierarchy bfrom (Zpos bn) a ato i h p pto
       end ->
       valid_relative_pointer_alt afrom zfrom ato pto (relative_pointer_alt_intro i' (h', p') f')
.

 Fact valid_relative_pointer_alt_valid_relative_pointer : forall p afrom zfrom ato pto,
   valid_relative_pointer_alt afrom zfrom ato pto p ->
   forall a i h' p', relative_pointer_of_relative_pointer_alt p = (a, i, (h', p')) ->
     valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto
.

 Fact valid_relative_pointer_valid_relative_pointer_alt : forall afrom zfrom a ato i h' p' pto,
   valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
   valid_relative_pointer_alt afrom zfrom ato pto (relative_pointer_alt_of_relative_pointer a i (h', p')).

 Function relative_pointer_alt_offset (rpa: relative_pointer_alt) (from : ident) (ato : ident) : option Z :=
   match rpa with
     | relative_pointer_alt_intro i' (h', p') f' =>
       match offsets ! from with
         | None => None
         | Some ofrom =>
           match subobject_offset from p' with
             | Some of =>
               match f' with
                 | None => Some (i' * size ofrom + of)
                 | Some (f, a, i, (_, p)) =>
                   match FieldSignature.type f with
                     | FieldSignature.Struct afrom _ =>
                       match Cplusconcepts.last p' with
                         | Some pto =>
                           match offsets ! pto with
                             | None => None
                             | Some opto =>
                               match assoc (FieldSignature.eq_dec (A := A)) f (field_offsets opto) with
                                 | Some fo =>
                                   match relative_pointer_offset afrom ato a i p with
                                     | Some o => Some (i' * size ofrom + of + fo + o)
                                     | _ => None
                                   end
                                 | _ => None
                               end
                           end
                         | _ => None
                       end
                     | _ => None
                   end
               end
             | _ => None
           end
       end
   end.

 Fact relative_pointer_alt_offset_correct : forall afrom zfrom a ato i h' p' pto,
   valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
   forall of,
     relative_pointer_offset afrom ato a i p' = Some of ->
     relative_pointer_alt_offset (relative_pointer_alt_of_relative_pointer a i (h', p')) afrom ato = Some of.

Soundness conditions (4.5)

Sizes, field separation, field alignment and dynamic type data (4.5.1, 4.5.2, 4.5.3, 4.5.4)

  Notation Is_empty := (is_empty OP hierarchy) (only parsing).

  Notation Is_dynamic := (is_dynamic OP hierarchy) (only parsing).


  Record class_level_prop (ci : ident) (o : t) : Prop := class_level_intro {


    primary_base_dynamic : forall b,
      primary_base o = Some b ->
      Is_dynamic b
      ;
    primary_base_offsets_exist : forall b,
      primary_base o = Some b ->
      offsets ! b <> None
      ;
    primary_base_exist_dynamic :
      primary_base o <> None ->
      Is_dynamic ci
      ;
    non_virtual_direct_base_offsets_exist :
      forall c,
        hierarchy ! ci = Some c ->
        forall bi,
          In (Class.Inheritance.Repeated, bi) (Class.super c) ->
          (non_virtual_direct_base_offsets o) ! bi <> None
          ;
    non_virtual_direct_base_offsets_guard :
      forall bi,
        (non_virtual_direct_base_offsets o) ! bi <> None ->
        forall c,
          hierarchy ! ci = Some c ->
          In (Class.Inheritance.Repeated, bi) (Class.super c)
          ;
    non_virtual_primary_base_offset : forall b,
      primary_base o = Some b ->
      (non_virtual_direct_base_offsets o) ! b = Some 0
      ;
    non_virtual_direct_base_offsets_low_bound :
      forall bi of,
        (non_virtual_direct_base_offsets o) ! bi = Some of ->
        0 <= of
        ;
    non_virtual_direct_base_offsets_dynamic_type_data_size :
      Is_dynamic ci ->
      primary_base o = None ->
      forall bi,
        (Is_empty bi -> False) ->
        forall of,
        (non_virtual_direct_base_offsets o) ! bi = Some of ->
        dynamic_type_data_size PF <= of
        ;
    non_virtual_align_dynamic :
      Is_dynamic ci ->
      (dynamic_type_data_align PF | non_virtual_align o)
      ;
    non_virtual_direct_base_offsets_align : forall bi of,
      (non_virtual_direct_base_offsets o) ! bi = Some of ->
      forall bo,
        offsets ! bi = Some bo ->
        (non_virtual_align bo | of)
        ;
    non_virtual_direct_base_nonempty_data_non_overlap : forall bi1 of1,
      (non_virtual_direct_base_offsets o) ! bi1 = Some of1 ->
      (Is_empty bi1 -> False) ->
      forall bi2 of2,
      (non_virtual_direct_base_offsets o) ! bi2 = Some of2 ->
      (Is_empty bi2 -> False) ->
      bi1 <> bi2 ->
      forall o1, offsets ! bi1 = Some o1 ->
        forall o2, offsets ! bi2 = Some o2 ->
      of1 + non_virtual_data_size o1 <= of2 \/
      of2 + non_virtual_data_size o2 <= of1
      ;
    non_virtual_direct_base_offsets_nonempty_high_bound :
      forall bi,
        (Is_empty bi -> False) ->
        forall of,
        (non_virtual_direct_base_offsets o) ! bi = Some of ->
        forall bo,
          offsets ! bi = Some bo ->
          of + non_virtual_data_size bo <= own_fields_offset o
          ;
    own_fields_offset_low_bound :
      0 <= own_fields_offset o
      ;
    own_fields_offset_dynamic_low_bound :
      Is_dynamic ci ->
      dynamic_type_data_size PF <= own_fields_offset o
      ;
    field_offsets_exist :
      forall c,
        hierarchy ! ci = Some c ->
        forall f,
          In f (Class.fields c) ->
          assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o) <> None
          ;
    field_offsets_guard :
      forall f,
        assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o) <> None ->
        forall c,
          hierarchy ! ci = Some c ->
          In f (Class.fields c)
          ;
    field_offsets_low_bound :
      forall f fi,
        assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o) = Some fi ->
        0 <= fi
        ;
    field_offsets_nonempty_low_bound :
      forall f fi,
        assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o) = Some fi ->
        (forall ty n, FieldSignature.type f = FieldSignature.Struct ty n -> Is_empty ty -> False) ->
        own_fields_offset o <= fi
        ;
    field_offsets_align :
      forall f fo,
        assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o) = Some fo ->
        forall al, field_align f = Some al ->
        (al | fo)
        ;
    field_offsets_non_overlap :
      forall f1 fi1,
        assoc (FieldSignature.eq_dec (A := A)) f1 (field_offsets o) = Some fi1 ->
        forall f2 fi2,
          assoc (FieldSignature.eq_dec (A := A)) f2 (field_offsets o) = Some fi2 ->
          (forall ty n, FieldSignature.type f1 = FieldSignature.Struct ty n -> Is_empty ty -> False) ->
          (forall ty n, FieldSignature.type f2 = FieldSignature.Struct ty n -> Is_empty ty -> False) ->
          f1 <> f2 ->
          forall s1, field_data_size f1 = Some s1 ->
            forall s2, field_data_size f2 = Some s2 ->
          fi1 + s1 <= fi2 \/
          fi2 + s2 <= fi1
          ;
    nonempty_non_virtual_data_size_positive :
      (Is_empty ci -> False) ->
      0 < non_virtual_data_size o
      ;
    non_virtual_data_size_field_offsets :
      forall f fi,
        assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o) = Some fi ->
        (forall ty n, FieldSignature.type f = FieldSignature.Struct ty n -> Is_empty ty -> False) ->
        forall s1, field_data_size f = Some s1 ->
          fi + s1 <= non_virtual_data_size o
          ;
    non_virtual_size_field_offsets :
      forall f fi,
        assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o) = Some fi ->
        forall s1, field_size f = Some s1 ->
          fi + s1 <= non_virtual_size o
          ;
    non_virtual_data_size_own_fields_offset :
      own_fields_offset o <= non_virtual_data_size o
      ;
    non_virtual_size_non_virtual_direct_bases : forall bi of,
      (non_virtual_direct_base_offsets o) ! bi = Some of ->
      forall bo, offsets ! bi = Some bo ->
        of + non_virtual_size bo <= non_virtual_size o
        ;
    non_virtual_align_non_virtual_direct_bases : forall bi,
      (non_virtual_direct_base_offsets o) ! bi <> None ->
      forall bo,
        offsets ! bi = Some bo ->
        (non_virtual_align bo | non_virtual_align o)
        ;
    non_virtual_align_fields : forall f,
      assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o) <> None ->
      forall al, field_align f = Some al ->
        (al | (non_virtual_align o))
        ;
    virtual_base_offsets_exist : forall b,
      is_virtual_base_of hierarchy b ci ->
      (virtual_base_offsets o) ! b <> None
      ;
    virtual_base_offsets_guard : forall b,
      (virtual_base_offsets o) ! b <> None ->
      is_virtual_base_of hierarchy b ci \/ b = ci
      ;
    virtual_base_offsets_self :
      (virtual_base_offsets o) ! ci = Some 0
      ;
    virtual_base_offsets_align : forall b of,
      (virtual_base_offsets o) ! b = Some of ->
      forall bo, offsets ! b = Some bo ->
        (non_virtual_align bo | of)
        ;
    virtual_base_offsets_low_bound : forall b of,
      (virtual_base_offsets o) ! b = Some of ->
      0 <= of
      ;
    virtual_base_offsets_nonempty_non_overlap : forall b1 of1,
      (virtual_base_offsets o) ! b1 = Some of1 ->
      forall bo1,
        offsets ! b1 = Some bo1 ->
      forall b2 of2,
        (virtual_base_offsets o) ! b2 = Some of2 ->
        forall bo2,
          offsets ! b2 = Some bo2 ->
          (Is_empty b1 -> False) ->
          (Is_empty b2 -> False) ->
          b1 <> b2 ->
          of1 + non_virtual_data_size bo1 <= of2 \/
          of2 + non_virtual_data_size bo2 <= of1
          ;
    virtual_base_offsets_data_size : forall bi of,
      (virtual_base_offsets o) ! bi = Some of ->
      (Is_empty bi -> False) ->
      forall bo,
        offsets ! bi = Some bo ->
        of + non_virtual_data_size bo <= data_size o
        ;
    data_size_high_bound :
      data_size o <= size o
      ;
    virtual_base_offsets_high_bound : forall bi of,
      (virtual_base_offsets o) ! bi = Some of ->
      forall bo,
        offsets ! bi = Some bo ->
      of + non_virtual_size bo <= size o
      ;
    align_virtual_base_offsets_align : forall b,
      (virtual_base_offsets o) ! b <> None ->
      forall bo, offsets ! b = Some bo ->
        (non_virtual_align bo | align o)
        ;
    align_size :
      (align o | size o)
      ;
    align_low_bound :
      0 < align o
      ;
    non_virtual_align_low_bound :
      0 < non_virtual_align o
      ;
    non_virtual_size_positive :
      0 < non_virtual_size o
  }.

Hypothesis Hhier : Well_formed_hierarchy.prop hierarchy.

Hypothesis intro : forall ci o, offsets ! ci = Some o -> class_level_prop ci o.

Hypothesis guard : forall ci, offsets ! ci <> None -> hierarchy ! ci <> None.

Existence theorems

Section Exist.



Variable cilimit : ident.

Hypothesis exist : forall ci, Plt ci cilimit -> hierarchy ! ci <> None -> offsets ! ci <> None.


Fact is_valid_repeated_subobject_offset_exist :
  forall l a l', l = a :: l' -> is_valid_repeated_subobject hierarchy l = true ->
    Plt a cilimit ->
    forall accu, non_virtual_subobject_offset accu l <> None.

Fact non_virtual_subobject_offset_exist : forall from,
  Plt from cilimit ->
  forall p to,
    path hierarchy to p from Class.Inheritance.Repeated ->
      forall accu, non_virtual_subobject_offset accu p <> None.

Fact subobject_offset_exist : forall from,
  Plt from cilimit ->
  forall p to h,
    path hierarchy to p from h ->
    subobject_offset from p <> None.

Fact array_path_offset_exist : forall from zfrom to zto p,
  valid_array_path hierarchy to zto from zfrom p ->
  Plt from cilimit ->
  hierarchy ! to <> None ->
  forall accu,
    array_path_offset accu from p <> None
.

Lemma relative_pointer_offset_exist : forall afrom,
  Plt afrom cilimit ->
  forall zfrom a ato i h' p' pto,
    valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
    relative_pointer_offset afrom ato a i p' <> None.

Fact non_virtual_path_field_align_exist : forall l from to,
  path hierarchy to l from Class.Inheritance.Repeated ->
    Plt from cilimit ->
    forall hto, hierarchy ! to = Some hto ->
      forall f, In f (Class.fields hto) ->
        field_align f <> None.

Fact path_field_align_exist : forall l from to h,
  path hierarchy to l from h ->
    Plt from cilimit ->
    forall hto, hierarchy ! to = Some hto ->
      forall f, In f (Class.fields hto) ->
        field_align f <> None.

Lemma relative_pointer_field_align_exist : forall afrom,
  Plt afrom cilimit ->
  forall zfrom a ato i h' p' pto,
    valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
    forall hto, hierarchy ! pto = Some hto ->
      forall f, In f (Class.fields hto) ->
        field_align f <> None.

End Exist.

Proofs of alignment properties (5.2)

Section Alignment.

Fact non_virtual_path_align : forall l from to,
  path hierarchy to l from Class.Inheritance.Repeated ->
    forall accu of, non_virtual_subobject_offset accu l = Some of ->
      forall ofrom, offsets ! from = Some ofrom ->
        forall oto, offsets ! to = Some oto ->
        (non_virtual_align oto | non_virtual_align ofrom) /\
        ((non_virtual_align oto | accu) -> (non_virtual_align oto | of)).

Fact path_align : forall l from to h,
  path hierarchy to l from h ->
    forall of, subobject_offset from l = Some of ->
      forall ofrom, offsets ! from = Some ofrom ->
        forall oto, offsets ! to = Some oto ->
          (non_virtual_align oto | align ofrom) /\
          (non_virtual_align oto | of).

Lemma relative_pointer_align : forall afrom zfrom a ato i h' p' pto,
  valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
  forall of,
    relative_pointer_offset afrom ato a i p' = Some of ->
    forall ofrom, offsets ! afrom = Some ofrom ->
      forall oto, offsets ! pto = Some oto ->
        (non_virtual_align oto | align ofrom) /\
        (non_virtual_align oto | of).

Theorem field_align_prop : forall afrom zfrom a ato i h' p' pto,
  valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
  forall of,
    relative_pointer_offset afrom ato a i p' = Some of ->
    forall ofrom, offsets ! afrom = Some ofrom ->
      forall oto, offsets ! pto = Some oto ->
        forall f fa, field_align f = Some fa ->
          forall foff, assoc (FieldSignature.eq_dec (A := A)) f (field_offsets oto) = Some foff ->
            (fa | align ofrom) /\ (fa | of + foff).

Theorem dynamic_align : forall afrom zfrom a ato i h' p' pto,
  valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
  forall of,
    relative_pointer_offset afrom ato a i p' = Some of ->
    forall ofrom, offsets ! afrom = Some ofrom ->
    offsets ! pto <> None ->
    Is_dynamic pto ->
    (dynamic_type_data_align PF | align ofrom) /\
    (dynamic_type_data_align PF | of).
  

End Alignment.

Total size inclusion

Section Bounds.

Lemma size_positive : forall c o, offsets ! c = Some o ->
  0 < size o.
  
Fact non_virtual_subobject_offset_size : forall l to from,
  path hierarchy to l from Class.Inheritance.Repeated ->
    forall accu o, non_virtual_subobject_offset accu l = Some o ->
      accu <= o /\
        forall ofrom, offsets ! from = Some ofrom ->
          forall oto, offsets ! to = Some oto ->
            o + non_virtual_size oto <= accu + non_virtual_size ofrom.

Fact subobject_offset_size : forall l to from h,
  path hierarchy to l from h ->
  forall so, subobject_offset from l = Some so ->
    0 <= so /\
    forall ofrom, offsets ! from = Some ofrom ->
      forall oto, offsets ! to = Some oto ->
        so + non_virtual_size oto <= size ofrom
    .

Fact array_path_offset_size : forall to to_n from from_n l,
  valid_array_path hierarchy to to_n from from_n l ->
  forall accu z, array_path_offset accu from l = Some z ->
    accu <= z /\
    forall ofrom, offsets ! from = Some ofrom ->
      forall oto, offsets ! to = Some oto ->
        z + to_n * size oto <= accu + from_n * size ofrom
.

Lemma relative_pointer_offset_size : forall afrom zfrom a ato i h' p' pto,
  valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
  forall of, relative_pointer_offset afrom ato a i p' = Some of ->
    0 <= of /\ forall ofrom,
      offsets ! afrom = Some ofrom ->
      forall opto, offsets ! pto = Some opto ->
        of + non_virtual_size opto <= zfrom * size ofrom.

Fact relative_pointer_alt_offset_size : forall i h p f afrom zfrom ato pto,
  valid_relative_pointer_alt afrom zfrom ato pto (relative_pointer_alt_intro i (h, p) f) ->
  forall ofrom, offsets ! afrom = Some ofrom ->
    forall op, subobject_offset afrom p = Some op ->
      forall of, relative_pointer_alt_offset (relative_pointer_alt_intro i (h, p) f) afrom ato = Some of ->
        i * size ofrom + op <= of /\
        forall through, last p = Some through ->
          forall othrough, offsets ! through = Some othrough ->
            forall opto, offsets ! pto = Some opto ->
              of + non_virtual_size opto <= i * size ofrom + op + non_virtual_size othrough
.

End Bounds.

Let Is_empty_prop := is_empty_prop OP hierarchy.

Section Empty_base_offsets.

Specification of the sets of (non-virtual) empty base offsets (4.5.5)

Inductive non_virtual_empty_base_offset : ident -> ident -> Z -> Prop :=
| non_virtual_empty_base_offset_self : forall ci,
  Is_empty ci ->
  forall z, z = 0 ->
  non_virtual_empty_base_offset ci ci z
| non_virtual_empty_base_offset_non_virtual_base : forall ci oc,
  offsets ! ci = Some oc ->
  forall ci' o',
    (non_virtual_direct_base_offsets oc) ! ci' = Some o' ->
    forall b o,
      non_virtual_empty_base_offset ci' b (o - o') ->
      non_virtual_empty_base_offset ci b o
| non_virtual_empty_base_offset_field : forall ci oc,
  offsets ! ci = Some oc ->
  forall f fo,
    assoc (FieldSignature.eq_dec (A := A)) f (field_offsets oc) = Some fo ->
    forall cif arraysize, FieldSignature.type f = FieldSignature.Struct cif arraysize ->
      forall ocf, offsets ! cif = Some ocf ->
        forall ai, 0 <= ai -> ai < Zpos arraysize ->
          forall b x,
            empty_base_offset cif b (x - fo - ai * size ocf) ->
            non_virtual_empty_base_offset ci b x

with empty_base_offset : ident -> ident -> Z -> Prop :=
| empty_base_offset_intro : forall ci oc,
  offsets ! ci = Some oc ->
  forall ci' o', (virtual_base_offsets oc) ! ci' = Some o' ->
    forall b x,
      non_virtual_empty_base_offset ci' b (x - o') ->
      empty_base_offset ci b x
.

Scheme empty_base_offset_rec_mu := Minimality for empty_base_offset Sort Prop
with non_virtual_empty_base_offset_rec_mu := Minimality for non_virtual_empty_base_offset Sort Prop.

Combined Scheme combined_empty_base_offset_rec from empty_base_offset_rec_mu, non_virtual_empty_base_offset_rec_mu.

Fact non_virtual_empty_base_offset_intro_non_virtual_path :
  forall from,
    forall p by,
      path hierarchy by p from Class.Inheritance.Repeated ->
        forall of accu,
          non_virtual_subobject_offset accu p = Some of ->
          forall to oz,
            non_virtual_empty_base_offset by to oz ->
            non_virtual_empty_base_offset from to (oz + of - accu)
            .
   

Fact non_virtual_path_empty_base_offsets : forall p to (to_empty : Is_empty to) from,
  path hierarchy to p from Class.Inheritance.Repeated ->
    forall of accu,
      non_virtual_subobject_offset accu p = Some of ->
      non_virtual_empty_base_offset from to (of - accu)
.

Fact empty_base_offset_intro_path : forall from,
    forall p by h,
      path hierarchy by p from h ->
        forall of,
          subobject_offset from p = Some of ->
          forall to oz,
            non_virtual_empty_base_offset by to oz ->
            empty_base_offset from to (oz + of)
            .

Fact path_empty_base_offsets : forall p to (to_empty : Is_empty to) from,
  forall h,
    path hierarchy to p from h ->
    forall of,
      subobject_offset from p = Some of ->
      empty_base_offset from to of
      .

Fact field_non_virtual_empty_base_offsets : forall l from to1 p1,
  path hierarchy to1 p1 from Class.Inheritance.Repeated ->
    forall accu1 z1, non_virtual_subobject_offset accu1 p1 = Some z1 ->
      forall o1, offsets ! to1 = Some o1 ->
        forall f fz, assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o1) = Some fz ->
          forall to2 ars2,
            FieldSignature.type f = FieldSignature.Struct to2 ars2 ->
            forall to3 arsz3,
              valid_array_path hierarchy to3 arsz3 to2 (Zpos ars2) l ->
              forall lz,
                array_path_offset (z1 + fz) to2 l = Some lz ->
                forall o3, offsets ! to3 = Some o3 ->
                  forall x, 0 <= x -> x < arsz3 ->
                    forall to4,
                      Is_empty to4 ->
                      forall p4 h4,
                        path hierarchy to4 p4 to3 h4 ->
                        forall p4z,
                          subobject_offset to3 p4 = Some p4z ->
                          non_virtual_empty_base_offset from to4 (lz + x * size o3 + p4z - accu1)
.

Fact field_empty_base_offsets : forall l from to1 p1 h1,
  path hierarchy to1 p1 from h1 ->
    forall z1, subobject_offset from p1 = Some z1 ->
      forall o1, offsets ! to1 = Some o1 ->
        forall f fz, assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o1) = Some fz ->
          forall to2 ars2,
            FieldSignature.type f = FieldSignature.Struct to2 ars2 ->
            forall to3 arsz3,
              valid_array_path hierarchy to3 arsz3 to2 (Zpos ars2) l ->
              forall lz,
                array_path_offset (z1 + fz) to2 l = Some lz ->
                forall o3, offsets ! to3 = Some o3 ->
                  forall x, 0 <= x -> x < arsz3 ->
                    forall to4,
                      Is_empty to4 ->
                      forall p4 h4,
                        path hierarchy to4 p4 to3 h4 ->
                        forall p4z,
                          subobject_offset to3 p4 = Some p4z ->
                          empty_base_offset from to4 (lz + x * size o3 + p4z)
.

Fact combined_empty_base_offset_elim :
  (forall from to z, empty_base_offset from to z -> (
    Is_empty to /\
    exists p1, exists h1, exists to1,
      path hierarchy to1 p1 from h1 /\
      exists z1, subobject_offset from p1 = Some z1 /\
        ((
          to = to1 /\
          z1 = z
        ) \/
        exists o1, offsets ! to1 = Some o1 /\
          exists f, exists fz, assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o1) = Some fz /\
            exists to2, exists ars2,
              FieldSignature.type f = FieldSignature.Struct to2 ars2 /\
              exists to3, exists arsz3, exists l,
                valid_array_path hierarchy to3 arsz3 to2 (Zpos ars2) l /\
                exists lz,
                  array_path_offset (z1 + fz) to2 l = Some lz /\
                  exists o3, offsets ! to3 = Some o3 /\
                    exists x, 0 <= x /\ x < arsz3 /\
                      exists p4, exists h4,
                        path hierarchy to p4 to3 h4 /\
                        exists p4z,
                          subobject_offset to3 p4 = Some p4z /\
                          z = lz + x * size o3 + p4z
      )
  )) /\
  (forall from to z, non_virtual_empty_base_offset from to z -> (
    Is_empty to /\
    exists to1, exists p1,
      path hierarchy to1 p1 from Class.Inheritance.Repeated /\
      exists z1, non_virtual_subobject_offset 0 p1 = Some z1 /\
        ((
          to = to1 /\
          z1 = z
        ) \/
        exists o1, offsets ! to1 = Some o1 /\
          exists f, exists fz, assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o1) = Some fz /\
            exists to2, exists ars2,
              FieldSignature.type f = FieldSignature.Struct to2 ars2 /\
              exists to3, exists arsz3, exists l,
                valid_array_path hierarchy to3 arsz3 to2 (Zpos ars2) l /\
                exists lz,
                  array_path_offset (z1 + fz) to2 l = Some lz /\
                  exists o3, offsets ! to3 = Some o3 /\
                    exists x, 0 <= x /\ x < arsz3 /\
                      exists p4, exists h4,
                        path hierarchy to p4 to3 h4 /\
                        exists p4z,
                          subobject_offset to3 p4 = Some p4z /\
                          z = (lz + x * size o3 + p4z)
        )
  )).

Lemma combined_empty_base_offset_equiv :
  (forall from to z, empty_base_offset from to z <-> (
    Is_empty to /\
    exists p1, exists h1, exists to1,
      path hierarchy to1 p1 from h1 /\
      exists z1, subobject_offset from p1 = Some z1 /\
        ((
          to = to1 /\
          z1 = z
        ) \/
        exists o1, offsets ! to1 = Some o1 /\
          exists f, exists fz, assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o1) = Some fz /\
            exists to2, exists ars2,
              FieldSignature.type f = FieldSignature.Struct to2 ars2 /\
              exists to3, exists arsz3, exists l,
                valid_array_path hierarchy to3 arsz3 to2 (Zpos ars2) l /\
                exists lz,
                  array_path_offset (z1 + fz) to2 l = Some lz /\
                  exists o3, offsets ! to3 = Some o3 /\
                    exists x, 0 <= x /\ x < arsz3 /\
                      exists p4, exists h4,
                        path hierarchy to p4 to3 h4 /\
                        exists p4z,
                          subobject_offset to3 p4 = Some p4z /\
                          z = lz + x * size o3 + p4z
      )
  )) /\
  (forall from to z, non_virtual_empty_base_offset from to z <-> (
    Is_empty to /\
    exists to1, exists p1,
      path hierarchy to1 p1 from Class.Inheritance.Repeated /\
      exists z1, non_virtual_subobject_offset 0 p1 = Some z1 /\
        ((
          to = to1 /\
          z1 = z
        ) \/
        exists o1, offsets ! to1 = Some o1 /\
          exists f, exists fz, assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o1) = Some fz /\
            exists to2, exists ars2,
              FieldSignature.type f = FieldSignature.Struct to2 ars2 /\
              exists to3, exists arsz3, exists l,
                valid_array_path hierarchy to3 arsz3 to2 (Zpos ars2) l /\
                exists lz,
                  array_path_offset (z1 + fz) to2 l = Some lz /\
                  exists o3, offsets ! to3 = Some o3 /\
                    exists x, 0 <= x /\ x < arsz3 /\
                      exists p4, exists h4,
                        path hierarchy to p4 to3 h4 /\
                        exists p4z,
                          subobject_offset to3 p4 = Some p4z /\
                          z = (lz + x * size o3 + p4z)
        )
  )).

  

Soundness conditions for empty base offsets (4.5.5)

Record disjoint_empty_base_offsets (ci : ident) (oc : t) : Prop := disjoint_empty_base_offsets_intro {
  disjoint_empty_base_offsets_bases :
  forall baseref,
    (baseref = non_virtual_direct_base_offsets \/ baseref = virtual_base_offsets) ->
    forall ci1 o1,
      (baseref oc) ! ci1 = Some o1 ->
      forall ci2 o2,
        (baseref oc) ! ci2 = Some o2 ->
        ci1 <> ci2 ->
        forall bi x1, non_virtual_empty_base_offset ci1 bi x1 ->
          forall x2, non_virtual_empty_base_offset ci2 bi x2 ->
            o1 + x1 <> o2 + x2
            ;
  disjoint_empty_base_offsets_field_base :
    forall ci1 o1,
      (non_virtual_direct_base_offsets oc) ! ci1 = Some o1 ->
      forall f2 o2,
          assoc (FieldSignature.eq_dec (A := A)) f2 (field_offsets oc) = Some o2 ->
          forall ci2 n2, FieldSignature.type f2 = FieldSignature.Struct ci2 n2 ->
            forall p2, 0 <= p2 -> p2 < Zpos n2 ->
              forall of2, offsets ! ci2 = Some of2 ->
                forall bi x1, non_virtual_empty_base_offset ci1 bi x1 ->
                  forall x2, empty_base_offset ci2 bi x2 ->
                    o1 + x1 <> o2 + p2 * size of2 + x2
                    ;
  disjoint_empty_base_offsets_fields :
      forall f1 o1,
          assoc (FieldSignature.eq_dec (A := A)) f1 (field_offsets oc) = Some o1 ->
          forall ci1 n1, FieldSignature.type f1 = FieldSignature.Struct ci1 n1 ->
            forall of1, offsets ! ci1 = Some of1 ->
              forall p1, 0 <= p1 -> p1 < Zpos n1 ->
      forall f2 o2,
          assoc (FieldSignature.eq_dec (A := A)) f2 (field_offsets oc) = Some o2 ->
          forall ci2 n2, FieldSignature.type f2 = FieldSignature.Struct ci2 n2 ->
            forall of2, offsets ! ci2 = Some of2 ->
              forall p2, 0 <= p2 -> p2 < Zpos n2 ->
                f1 <> f2 ->
                forall bi x1, empty_base_offset ci1 bi x1 ->
                  forall x2, empty_base_offset ci2 bi x2 ->
                    o1 + p1 * size of1 + x1 <> o2 + p2 * size of2 + x2
}.

  

Soundness proof of identity of subobjects for empty base offsets (5.3)

Section Disjoint_empty_base_offsets.


  Hypothesis disjoint : forall ci oc,
    offsets ! ci = Some oc ->
    disjoint_empty_base_offsets ci oc.
  
Fact disjoint_empty_base_offsets_disjoint_non_virtual_paths :
  forall p1 ci to, path hierarchy to p1 ci Class.Inheritance.Repeated ->
    forall (to_empty : Is_empty to),
      forall accu o, non_virtual_subobject_offset accu p1 = Some o ->
        forall p2, path hierarchy to p2 ci Class.Inheritance.Repeated ->
          non_virtual_subobject_offset accu p2 = Some o ->
          p1 = p2.

Fact disjoint_empty_base_offsets_disjoint_paths :
  forall p1 h1 ci to, path hierarchy to p1 ci h1 ->
    forall (to_empty : Is_empty to),
    forall o, subobject_offset ci p1 = Some o ->
      forall p2 h2, path hierarchy to p2 ci h2 ->
        subobject_offset ci p2 = Some o ->
        (h1, p1) = (h2, p2).

Theorem disjoint_empty_base_offsets_disjoint_pointer_paths :
  forall pto (pto_isempty : Is_empty pto) (pto_offsets_def: offsets ! pto <> None) ap1 afrom asfrom ato1 i1 h1 p1,
    valid_relative_pointer hierarchy afrom asfrom ap1 ato1 i1 h1 p1 pto ->
  forall ap2 ato2 i2 h2 p2,
    valid_relative_pointer hierarchy afrom asfrom ap2 ato2 i2 h2 p2 pto ->
    forall o, relative_pointer_offset afrom ato1 ap1 i1 p1 = Some o ->
      relative_pointer_offset afrom ato2 ap2 i2 p2 = Some o ->
      (ap1, i1, h1, p1) = (ap2, i2, h2, p2)
      .
  
End Disjoint_empty_base_offsets.



  Lemma non_virtual_empty_base_offset_incl : forall ci b z,
    non_virtual_empty_base_offset ci b z ->
    ((offsets ) ! b <> None) ->
    forall o', (offsets ) ! ci = Some o' ->
      0 <= z /\ z < non_virtual_size o'.

  Lemma empty_base_offset_incl : forall ci b z,
    empty_base_offset ci b z ->
    ((offsets ) ! b <> None) ->
    forall o', (offsets ) ! ci = Some o' ->
      0 <= z /\ z < size o'.

  Lemma non_virtual_empty_base_offset_wf : forall ci b z,
    non_virtual_empty_base_offset ci b z ->
    Ple b ci /\ hierarchy ! b <> None.


  Lemma empty_base_offset_wf : forall ci b z,
    empty_base_offset ci b z ->
    Ple b ci /\ hierarchy ! b <> None.
  
End Empty_base_offsets.


Section Nonempty_base_offsets.

Data inclusion for non-empty bases

Fact non_virtual_path_non_virtual_data_incl : forall l to from,
  path hierarchy to l from Class.Inheritance.Repeated ->
    (Is_empty to -> False) ->
    forall accu o, non_virtual_subobject_offset accu l = Some o ->
      accu <= o /\
      forall oto, offsets ! to = Some oto ->
        forall ofrom, offsets ! from = Some ofrom ->
          o + non_virtual_data_size oto <= accu + non_virtual_data_size ofrom.
     
Fact non_virtual_path_disjoint_field_zones : forall l1 l2,
  l1 <> l2 ->
  forall to1,
    (Is_empty to1 -> False) ->
    forall from,
      path hierarchy to1 l1 from Class.Inheritance.Repeated ->
        forall to2,
          (Is_empty to2 -> False) ->
          path hierarchy to2 l2 from Class.Inheritance.Repeated ->
            forall accu z1, non_virtual_subobject_offset accu l1 = Some z1 ->
              forall z2, non_virtual_subobject_offset accu l2 = Some z2 ->
                forall o1, offsets ! to1 = Some o1 ->
                  forall o2, offsets ! to2 = Some o2 ->
                    z1 + non_virtual_data_size o1 <= z2 + own_fields_offset o2 \/
                    z2 + non_virtual_data_size o2 <= z1 + own_fields_offset o1
                    .

Fact path_disjoint_field_zones : forall h1 l1 h2 l2,
  (h1, l1) <> (h2, l2) ->
  forall to1,
    (Is_empty to1 -> False) ->
    forall from,
      path hierarchy to1 l1 from h1 ->
        forall to2,
          (Is_empty to2 -> False) ->
          path hierarchy to2 l2 from h2 ->
            forall z1, subobject_offset from l1 = Some z1 ->
              forall z2, subobject_offset from l2 = Some z2 ->
                forall o1, offsets ! to1 = Some o1 ->
                  forall o2, offsets ! to2 = Some o2 ->
                    z1 + non_virtual_data_size o1 <= z2 + own_fields_offset o2 \/
                    z2 + non_virtual_data_size o2 <= z1 + own_fields_offset o1
                    .

Definition Dynamic_nonempty : forall id, Is_dynamic id -> Is_empty id -> False := dynamic_nonempty (o := OP) (hierarchy := hierarchy).

Hint Resolve Dynamic_nonempty.

Fact non_virtual_path_dynamic_own_fields_offset :
 forall l from
to,
  path hierarchy to l from Class.Inheritance.Repeated ->
  Is_dynamic from ->
  forall (to_nonempty : Is_empty to -> False)
   oto, offsets ! to = Some oto ->
  forall accu z,
   non_virtual_subobject_offset accu l = Some z ->
  accu + dynamic_type_data_size PF <= z + own_fields_offset oto
.

Fact non_virtual_path_own_fields_offset_dynamic :
 forall l from to,
  path hierarchy to l from Class.Inheritance.Repeated ->
  Is_dynamic to ->
  forall ofrom, offsets ! from = Some ofrom ->
    offsets ! to <> None ->
  forall accu z,
   non_virtual_subobject_offset accu l = Some z ->
  z + dynamic_type_data_size PF <= accu + own_fields_offset ofrom
.

Fact non_virtual_paths_disjoint_field_dynamic_type :
 forall l1 b to1,
   path hierarchy to1 l1 b Class.Inheritance.Repeated ->
     (Is_empty to1 -> False) ->
     forall accu so1, non_virtual_subobject_offset accu l1 = Some so1 ->
       forall o1, offsets ! to1 = Some o1 ->
         forall to2, Is_dynamic to2 ->
           forall l2,
             path hierarchy to2 l2 b Class.Inheritance.Repeated ->
               forall so2, non_virtual_subobject_offset accu l2 = Some so2 ->
                 offsets ! to2 <> None ->
                   so1 + non_virtual_data_size o1 <= so2 \/
                   so2 + dynamic_type_data_size PF <= so1 + own_fields_offset o1.

Fact paths_disjoint_field_dynamic_type: forall l1 b to1 h1,
   path hierarchy to1 l1 b h1 ->
     (Is_empty to1 -> False) ->
     forall so1, subobject_offset b l1 = Some so1 ->
       forall o1, offsets ! to1 = Some o1 ->
         forall to2, Is_dynamic to2 ->
           forall l2 h2,
             path hierarchy to2 l2 b h2 ->
               forall so2, subobject_offset b l2 = Some so2 ->
                 offsets ! to2 <> None ->
                   so1 + non_virtual_data_size o1 <= so2 \/
                   so2 + dynamic_type_data_size PF <= so1 + own_fields_offset o1.

Fact path_data_incl : forall l to from h,
  path hierarchy to l from h ->
  (Is_empty to -> False) ->
    forall o, subobject_offset from l = Some o ->
      0 <= o /\
      forall oto, offsets ! to = Some oto ->
        forall ofrom, offsets ! from = Some ofrom ->
          o + non_virtual_data_size oto <= data_size ofrom.

Fact relative_pointer_data_incl : forall ap1 pto1 afrom asfrom ato1 i1 h1 p1,
    valid_relative_pointer hierarchy afrom asfrom ap1 ato1 i1 h1 p1 pto1 ->
    forall (pto1_nonempty : Is_empty pto1 -> False) o1, relative_pointer_offset afrom ato1 ap1 i1 p1 = Some o1 ->
          0 <= o1 /\
          forall ofrom, offsets ! afrom = Some ofrom ->
            forall of1, offsets ! pto1 = Some of1 ->
              o1 + non_virtual_data_size of1 <= (asfrom - 1) * size ofrom + data_size ofrom
              .

Fact relative_pointer_alt_fields_incl : forall afrom zfrom ato pto i h p f,
  valid_relative_pointer_alt afrom zfrom ato pto (relative_pointer_alt_intro i (h, p) f) ->
  forall (is_empty_pto : Is_empty pto -> False) of, relative_pointer_alt_offset (relative_pointer_alt_intro i (h, p) f) afrom ato = Some of ->
    forall ofrom, offsets ! afrom = Some ofrom ->
      forall ofp, subobject_offset afrom p = Some ofp ->
        forall pato, last p = Some pato ->
          forall oato, offsets ! pato = Some oato ->
            forall opto, offsets ! pto = Some opto ->
              i * size ofrom + ofp <= of /\
              i * size ofrom + ofp + own_fields_offset oato <= of + own_fields_offset opto /\
              of + non_virtual_data_size opto <= i * size ofrom + ofp + non_virtual_data_size oato.

Proof of field access (5.1)

Theorem scalar_fields_disjoint :
  forall ap1 pto1 afrom asfrom ato1 i1 h1 p1,
    valid_relative_pointer hierarchy afrom asfrom ap1 ato1 i1 h1 p1 pto1 ->
    forall ap2 pto2 ato2 i2 h2 p2,
    valid_relative_pointer hierarchy afrom asfrom ap2 ato2 i2 h2 p2 pto2 ->
    forall o1, relative_pointer_offset afrom ato1 ap1 i1 p1 = Some o1 ->
      forall o2, relative_pointer_offset afrom ato2 ap2 i2 p2 = Some o2 ->
        forall of1, offsets ! pto1 = Some of1 ->
          forall of2, offsets ! pto2 = Some of2 ->
            forall f1 fo1, assoc (FieldSignature.eq_dec (A := A)) f1 (field_offsets of1) = Some fo1 ->
              forall ty1, FieldSignature.type f1 = FieldSignature.Scalar ty1 ->
                forall f2 fo2, assoc (FieldSignature.eq_dec (A := A)) f2 (field_offsets of2) = Some fo2 ->
                  forall ty2, FieldSignature.type f2 = FieldSignature.Scalar ty2 ->
                    ((ap1, i1, (h1, p1)), f1) <> ((ap2, i2, (h2, p2)), f2) ->
                    o1 + fo1 + typ_size PF ty1 <= o2 + fo2 \/
                    o2 + fo2 + typ_size PF ty2 <= o1 + fo1
                    .

Proof of field access in the presence of dynamic type data (5.4)

Theorem scalar_field_dynamic_type_data_disjoint :
  forall ap1 pto1 afrom asfrom ato1 i1 h1 p1,
    valid_relative_pointer hierarchy afrom asfrom ap1 ato1 i1 h1 p1 pto1 ->
    forall ap2 pto2 ato2 i2 h2 p2,
    valid_relative_pointer hierarchy afrom asfrom ap2 ato2 i2 h2 p2 pto2 ->
    forall o1, relative_pointer_offset afrom ato1 ap1 i1 p1 = Some o1 ->
      forall o2, relative_pointer_offset afrom ato2 ap2 i2 p2 = Some o2 ->
        forall of1, offsets ! pto1 = Some of1 ->
          offsets ! pto2 <> None ->
            forall f1 fo1, assoc (FieldSignature.eq_dec (A := A)) f1 (field_offsets of1) = Some fo1 ->
              forall ty1, FieldSignature.type f1 = FieldSignature.Scalar ty1 ->
                Is_dynamic pto2 ->
                o1 + fo1 + typ_size PF ty1 <= o2 \/
                o2 + dynamic_type_data_size PF <= o1 + fo1
                .

Preservation of dynamic type data (5.4)

Section Primary_paths.

Function is_primary_path (p : list ident) {struct p} : bool :=
match p with
| nil => false
| a :: p' =>
  match p' with
    | nil => true
    | a' :: _ =>
      match offsets ! a with
        | None => false
        | Some o =>
          if (option_eq_dec peq (primary_base o) (Some a')) then is_primary_path p' else false
      end
  end
end.

Fact primary_path_offset : forall p,
 is_primary_path p = true ->
 forall accu, non_virtual_subobject_offset accu p = Some accu.

Fact non_primary_path_offset : forall p,
  is_primary_path p = false ->
  forall from to, path hierarchy to p from Class.Inheritance.Repeated ->
    (Is_dynamic from) ->
    (Is_empty to -> False) ->
    offsets ! to <> None ->
    forall accu of, non_virtual_subobject_offset accu p = Some of -> accu + dynamic_type_data_size PF <= of.

Fact non_virtual_direct_base_non_primary_offset_low_bound : forall cl,
  Is_dynamic cl ->
  forall of (Hof : offsets ! cl = Some of)
    cl', primary_base of <> Some cl' ->
      (Is_empty cl' -> False) ->
      offsets ! cl' <> None ->
      forall o' (Ho' : (non_virtual_direct_base_offsets of) ! cl' = Some o'),
        dynamic_type_data_size PF <= o'.
  
Fact primary_path_join : forall l1 p l2,
  is_primary_path (l1 ++ p :: nil) = true ->
  is_primary_path (p :: l2) = true ->
  is_primary_path (l1 ++ p :: l2) = true.
  
Fact primary_path_split_left : forall l1 p l2,
  is_primary_path (l1 ++ p :: l2) = true ->
  is_primary_path (l1 ++ p :: nil) = true.

Fact primary_path_split_right : forall l1 p l2,
  is_primary_path (l1 ++ p :: l2) = true ->
  is_primary_path (p :: l2) = true.
  
Fact minimal_path_unique : forall l1 p1 q1,
  is_primary_path (p1 :: q1 :: nil) = false ->
  forall l1', is_primary_path (q1 :: l1') = true ->
    forall l2 p2 q2,
  is_primary_path (p2 :: q2 :: nil) = false ->
  forall l2', is_primary_path (q2 :: l2') = true ->
    l1 ++ p1 :: q1 :: l1' = l2 ++ p2 :: q2 :: l2' ->
    (l1, p1, q1, l1') = (l2, p2, q2, l2').

Fact minimal_path_exist : forall l, l <> nil ->
  is_primary_path l = false -> {
    l2 : _ & {
      p2 : _ & {
        q2 : _ & {
          l2' |
            is_primary_path (p2 :: q2 :: nil) = false /\
            is_primary_path (q2 :: l2') = true /\
            l = l2 ++ p2 :: q2 :: l2'
        }
      }
    }
  }.

Fact reduce_path_aux : {f | forall l,
  l <> nil ->
  if is_primary_path l
    then exists p, exists q, l = p :: q /\ f l = p :: nil
    else exists l1, exists p, exists q, exists l2, l = l1 ++ p :: q :: l2 /\ is_primary_path (p :: q :: nil) = false /\ is_primary_path (q :: l2) = true /\ f l = l1 ++ p :: q :: nil
}.
 
Definition reduce_path := let (f, _) := reduce_path_aux in f.

Lemma reduce_path_prop : forall l,
  l <> nil ->
  if is_primary_path l
    then exists p, exists q, l = p :: q /\ reduce_path l = p :: nil
    else exists l1, exists p, exists q, exists l2, l = l1 ++ p :: q :: l2 /\ is_primary_path (p :: q :: nil) = false /\ is_primary_path (q :: l2) = true /\ reduce_path l = l1 ++ p :: q :: nil
.

Opaque reduce_path.

Lemma reduce_path_primary : forall l,
  is_primary_path l = true ->
  exists p, exists q, l = p :: q /\ reduce_path l = p :: nil
.

Lemma reduce_path_non_primary : forall l,
  l <> nil ->
  is_primary_path l = false ->
  exists l1, exists p, exists q, exists l2, l = l1 ++ p :: q :: l2 /\ is_primary_path (p :: q :: nil) = false /\ is_primary_path (q :: l2) = true /\ reduce_path l = l1 ++ p :: q :: nil
.

Lemma reduce_path_offset : forall l from to,
  path hierarchy to l from Class.Inheritance.Repeated ->
    forall accu,
      non_virtual_subobject_offset accu l = non_virtual_subobject_offset accu (reduce_path l).

Lemma reduce_path_valid : forall l,
  is_valid_repeated_subobject hierarchy l = true ->
  is_valid_repeated_subobject hierarchy (reduce_path l) = true.

Lemma reduce_path_idem : forall l,
  l <> nil ->
  reduce_path (reduce_path l) = reduce_path l.

Lemma reduce_path_primary_right : forall l from to,
  path hierarchy to l from Class.Inheritance.Repeated ->
    forall l2, is_primary_path (to :: l2) = true ->
      reduce_path (l ++ l2) = reduce_path l.
 
Lemma reduce_path_prefix_repeated : forall l from to,
  path hierarchy to l from Class.Inheritance.Repeated ->
    exists through, exists l',
      path hierarchy through (reduce_path l) from Class.Inheritance.Repeated /\
        path hierarchy to (through :: l') through Class.Inheritance.Repeated /\
          l = reduce_path l ++ l' /\
          is_primary_path (through :: l') = true.
   
Lemma reduce_path_prefix : forall l from to h,
  path hierarchy to l from h ->
    exists through, exists l',
      path hierarchy through (reduce_path l) from h /\
        path hierarchy to (through :: l') through Class.Inheritance.Repeated /\
          l = reduce_path l ++ l' /\
          is_primary_path (through :: l') = true.

Fact primary_path_dynamic : forall l a,
 Cplusconcepts.last l = Some a ->
 is_primary_path l = true ->
 Is_dynamic a ->
 forall b, In b l ->
 Is_dynamic b.

Fact reduce_path_dynamic_type_disjoint_non_primary : forall l1 from to1,
  path hierarchy to1 l1 from Class.Inheritance.Repeated ->
    is_primary_path l1 = false ->
    Is_dynamic to1 ->
    forall (to1_offsets : offsets ! to1 <> None) accu z1,
      non_virtual_subobject_offset accu l1 = Some z1 ->
      forall l2 to2,
        path hierarchy to2 l2 from Class.Inheritance.Repeated ->
          is_primary_path l2 = false ->
          Is_dynamic to2 ->
          forall (to2_offsets : offsets ! to2 <> None) z2,
            non_virtual_subobject_offset accu l2 = Some z2 ->
            reduce_path l1 <> reduce_path l2 ->
            z1 + dynamic_type_data_size PF <= z2 \/ z2 + dynamic_type_data_size PF <= z1
.

Fact reduce_path_dynamic_type_disjoint_non_virtual_paths : forall l1 from to1,
  path hierarchy to1 l1 from Class.Inheritance.Repeated ->
    forall accu z1,
      non_virtual_subobject_offset accu l1 = Some z1 ->
      forall l2 to2,
        path hierarchy to2 l2 from Class.Inheritance.Repeated ->
          forall z2,
            non_virtual_subobject_offset accu l2 = Some z2 ->
            Is_dynamic to1 ->
            Is_dynamic to2 ->
            offsets ! to1 <> None ->
            offsets ! to2 <> None ->
            reduce_path l1 <> reduce_path l2 ->
            z1 + dynamic_type_data_size PF <= z2 \/ z2 + dynamic_type_data_size PF <= z1
.

Fact reduce_path_dynamic_type_disjoint_paths : forall l1 from to1 h1,
  path hierarchy to1 l1 from h1 ->
    forall z1,
      subobject_offset from l1 = Some z1 ->
      forall l2 to2 h2,
        path hierarchy to2 l2 from h2 ->
          forall z2,
            subobject_offset from l2 = Some z2 ->
            Is_dynamic to1 ->
            Is_dynamic to2 ->
            offsets ! to1 <> None ->
            offsets ! to2 <> None ->
            reduce_path l1 <> reduce_path l2 ->
            z1 + dynamic_type_data_size PF <= z2 \/ z2 + dynamic_type_data_size PF <= z1
.

Theorem reduce_path_dynamic_type_disjoint : forall afrom zfrom a1 ato1 i1 h1 p1 pto1,
   valid_relative_pointer hierarchy afrom zfrom a1 ato1 i1 h1 p1 pto1 ->
   forall a2 ato2 i2 h2 p2 pto2,
     valid_relative_pointer hierarchy afrom zfrom a2 ato2 i2 h2 p2 pto2 ->
     (a1, i1) <> (a2, i2) \/ reduce_path p1 <> reduce_path p2 ->
     offsets ! pto1 <> None ->
     offsets ! pto2 <> None ->
     Is_dynamic pto1 ->
     Is_dynamic pto2 ->
     forall of1, relative_pointer_offset afrom ato1 a1 i1 p1 = Some of1 ->
       forall of2, relative_pointer_offset afrom ato2 a2 i2 p2 = Some of2 ->
         of1 + dynamic_type_data_size PF <= of2 \/ of2 + dynamic_type_data_size PF <= of1
.


End Primary_paths.

Identity of subobjects for non-empty bases (5.1)

     
Fact non_virtual_path_nonempty_distinct_offsets : forall to,
  (Is_empty to -> False) ->
  offsets ! to <> None ->
  forall l1 l2,
    l1 <> l2 ->
    forall from,
        path hierarchy to l1 from Class.Inheritance.Repeated ->
          path hierarchy to l2 from Class.Inheritance.Repeated ->
            forall accu z1, non_virtual_subobject_offset accu l1 = Some z1 ->
              forall z2, non_virtual_subobject_offset accu l2 = Some z2 ->
                z1 <> z2.

Fact path_nonempty_distinct_offsets :
  forall to,
    (Is_empty to -> False) ->
    offsets ! to <> None ->
    forall h1 l1 h2 l2,
      (h1, l1) <> (h2, l2) ->
      forall from,
        path hierarchy to l1 from h1 ->
        path hierarchy to l2 from h2 ->
        forall z1, subobject_offset from l1 = Some z1 ->
          forall z2, subobject_offset from l2 = Some z2 ->
            z1 <> z2.

Remark paths_cases : forall (A : Type) (aeq : forall a1 a2 : A, {a1 = a2} + {a1 <> a2}) (l1 l2 : _ A),
  {l' | l1 = l2 ++ l'} +
  {a : _ & {l2' | l2 = l1 ++ a :: l2'}} +
  {l : _ & { a1 : _ & { a2 : _ & { l1' : _ & { l2' |
    l1 = l ++ a1 :: l1' /\ l2 = l ++ a2 :: l2' /\ a1 <> a2}}}}}.

Theorem nonempty_distinct_offsets :
  forall pto,
    (Is_empty pto -> False) ->
    offsets ! pto <> None ->
    forall ap1 afrom asfrom ato1 i1 h1 p1,
      valid_relative_pointer hierarchy afrom asfrom ap1 ato1 i1 h1 p1 pto ->
      forall ap2 ato2 i2 h2 p2,
        valid_relative_pointer hierarchy afrom asfrom ap2 ato2 i2 h2 p2 pto ->
        forall o1, relative_pointer_offset afrom ato1 ap1 i1 p1 = Some o1 ->
          forall o2, relative_pointer_offset afrom ato2 ap2 i2 p2 = Some o2 ->
            (ap1, i1, (h1, p1)) <> (ap2, i2, (h2, p2)) ->
            o1 <> o2.


End Nonempty_base_offsets.

End OF.

Incremental computing of offsets

Section OF_compare.


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

Hypothesis hierarchy_wf : Well_formed_hierarchy.prop hierarchy.

Section OF1.

Variables offsets1 offsets2 : PTree.t t.

Variable cilimit : positive.

Hypothesis offsets_eq : forall j, Plt j cilimit -> offsets1 ! j = offsets2 ! j.

Variable guard1 : forall ci, offsets1 ! ci <> None -> hierarchy ! ci <> None.

Section Class_level_prop_eq.

Variable ci : ident.

Hypothesis Hci : Plt ci cilimit.

Variable o1 : t.

Hypothesis Ho1 : offsets1 ! ci = Some o1.

Let Hhier1 : hierarchy ! ci <> None.

Let h0 : {h | hierarchy ! ci = Some h}.

Let h := let (h, _) := h0 in h.

Let Hh : hierarchy ! ci = Some h.

Hypothesis Hprop1 : class_level_prop offsets1 hierarchy ci o1.

Fact non_virtual_direct_base_offsets_lt : forall b,
  (non_virtual_direct_base_offsets o1) ! b <> None ->
  Plt b ci.

Fact non_virtual_direct_base_offsets_eq : forall b,
  (non_virtual_direct_base_offsets o1) ! b <> None ->
  offsets1 ! b = offsets2 ! b.

Fact non_virtual_direct_base_offsets_eq_some : forall b c,
  (non_virtual_direct_base_offsets o1) ! b = Some c ->
  offsets1 ! b = offsets2 ! b.

Fact virtual_base_offsets_le : forall b,
  (virtual_base_offsets o1) ! b <> None ->
  Ple b ci.

Fact virtual_base_offsets_eq : forall b,
  (virtual_base_offsets o1) ! b <> None ->
  offsets1 ! b = offsets2 ! b.

Fact virtual_base_offsets_eq_some : forall b c,
  (virtual_base_offsets o1) ! b = Some c ->
  offsets1 ! b = offsets2 ! b.

Fact field_offsets_lt : forall f,
  assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o1) <> None ->
  forall ty n, FieldSignature.type f = FieldSignature.Struct ty n ->
    Plt ty ci.

Let Hfo : forall f,
  assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o1) <> None ->
  (field_data_size offsets1 f = field_data_size offsets2 f /\ field_size offsets1 f = field_size offsets2 f /\ field_align offsets1 f = field_align offsets2 f).

Let Hsfo : forall f fo,
  assoc (FieldSignature.eq_dec (A := A)) f (field_offsets o1) = Some fo ->
  (field_data_size offsets1 f = field_data_size offsets2 f /\ field_size offsets1 f = field_size offsets2 f /\ field_align offsets1 f = field_align offsets2 f).

Let Hfod := fun f h => match @Hfo f h with conj j _ => j end.

Let Hfos := fun f h => match @Hfo f h with conj _ (conj j _) => j end.

Let Hfoa := fun f h => match @Hfo f h with conj _ (conj _ j) => j end.

Let Hsfod := fun f c h => match @Hsfo f c h with conj j _ => j end.

Let Hsfos := fun f c h => match @Hsfo f c h with conj _ (conj j _) => j end.

Let Hsfoa := fun f c h => match @Hsfo f c h with conj _ (conj _ j) => j end.

Variable o2 : t.

Hypothesis Ho2 : offsets2 ! ci = Some o2.

Lemma class_level_prop_eq :
    class_level_prop offsets2 hierarchy ci o2.

End Class_level_prop_eq.

Hypothesis intro1 : forall ci, Plt ci cilimit -> forall o, offsets1 ! ci = Some o -> class_level_prop offsets1 hierarchy ci o.

Lemma combined_empty_base_offsets_eq : forall ci, Plt ci cilimit ->
(forall b z,
  non_virtual_empty_base_offset offsets1 hierarchy ci b z ->
   non_virtual_empty_base_offset offsets2 hierarchy ci b z)
  /\
  (forall b z,
    empty_base_offset offsets1 hierarchy ci b z ->
    empty_base_offset offsets2 hierarchy ci b z).

Definition non_virtual_empty_base_offsets_eq := fun ci h =>
  let (j, _) := @combined_empty_base_offsets_eq ci h in j.

Definition empty_base_offsets_eq := fun ci h =>
  let (_, j) := @combined_empty_base_offsets_eq ci h in j.

End OF1.

Variables offsets1 offsets2 : PTree.t t.

Variable cilimit : positive.

Hypothesis offsets_eq : forall j, Plt j cilimit -> offsets1 ! j = offsets2 ! j.

Let offsets_eq2 : forall j, Plt j cilimit -> offsets2 ! j = offsets1 ! j.

Hypothesis guard1 : forall ci, offsets1 ! ci <> None -> hierarchy ! ci <> None.

Hypothesis guard2 : forall ci, offsets2 ! ci <> None -> hierarchy ! ci <> None.

Hypothesis intro1 : forall ci, Plt ci cilimit -> forall o, offsets1 ! ci = Some o -> class_level_prop offsets1 hierarchy ci o.

Let intro2 : forall ci, Plt ci cilimit -> forall o, offsets2 ! ci = Some o -> class_level_prop offsets2 hierarchy ci o.

Lemma disjoint_empty_base_offsets_eq : forall ci, Plt ci cilimit -> forall o1, offsets1 ! ci = Some o1 -> disjoint_empty_base_offsets offsets1 hierarchy ci o1 -> forall o2, offsets2 ! ci = Some o2 -> disjoint_empty_base_offsets offsets2 hierarchy ci o2.

End OF_compare.

End Offsets.