Module ConcreteOp

Require Import Coqlib.
Require Import Cplusconcepts.
Require Import CplusWf.
Require Import LayoutConstraints.
Require Import LibLists.
Require Import Tactics.
Require Import LibMaps.
Require Import Relations.
Load Param.
Open Scope Z_scope.

Notation var := (ident) (only parsing).

Section SimpleCompiler.
Variable (A : ATOM.t).
 
Record NATIVEOP : Type := NativeOp {
  nativeop : Type;
  sem : nativeop -> list (sigT (ATOM.val (t := A))) -> sigT (ATOM.val (t := A)) -> Prop;
  sembool : sigT (ATOM.val (t := A)) -> option bool;
  tyTRUE : (ATOM.ty A);
  TRUE : (ATOM.val (t := A)) tyTRUE;
  sembool_true : sembool (existT _ _ TRUE) = Some true;
  tyFALSE : (ATOM.ty A);
  FALSE : (ATOM.val (t := A)) tyFALSE;
  sembool_false : sembool (existT _ _ FALSE) = Some false;
  semZ : sigT (ATOM.val (t := A)) -> option Z;
  Zsem : Z -> sigT (ATOM.val (t := A));
  Zsem_semZ : forall z, semZ (Zsem z) = Some z
}.


Variable NO : NATIVEOP.
Variable OP : OPTIM A.

4.3
Hypothesis is_dynamic_virtual_base : forall hierarchy a b,
  is_virtual_base_of hierarchy b a -> is_dynamic OP hierarchy a.

    Section Common.

        Variable value : Type.
        Variable atom : forall ty, (ATOM.val (t := A)) ty -> value.
        Variable specific_stmt : Type.

      Inductive common_stmt : Type :=
      | skip
      | seq (_ _ : common_stmt)
      | test (test : var) (ifso ifnot : common_stmt)
      | block (body : common_stmt)
      | exit (n : nat)
      | loop (body : common_stmt)
      | native (op : nativeop NO) (source : list var) (target : var)
      | specific (_ : specific_stmt)
        .

      Variable globals : Type.

      Record state : Type := State {
        pc : list (list common_stmt);
        vars : PTree.t value;
        global : globals
      }.

      Inductive common_step : state -> state -> Prop :=

      | common_step_skip : forall stl blocks vars global,
        common_step
        (State ((skip :: stl) :: blocks) vars global)
        (State (stl :: blocks) vars global)

      | common_step_seq : forall stl s1 s2 vars blocks global,
        common_step
        (State ((seq s1 s2 :: stl) :: blocks) vars global)
        (State ((s1 :: s2 :: stl) :: blocks) vars global)

      | common_step_test : forall vars varb tyb valb,
        vars ! varb = Some (@atom tyb valb) ->
        forall b, sembool NO (existT _ tyb valb) = Some b ->
          forall s ifso ifnot, s = (if b then ifso else ifnot) ->
            forall stl blocks global,
            common_step
            (State ((test varb ifso ifnot :: stl) :: blocks) vars global)
            (State ((s :: stl) :: blocks) vars global)

      | common_step_block : forall stm stl blocks vars global,
        common_step
        (State ((block stm :: stl) :: blocks) vars global)
        (State ((stm :: nil) :: stl :: blocks) vars global)

      | common_step_exit_O : forall stl blocks vars global,
        common_step
        (State ((exit O :: stl) :: blocks) vars global)
        (State blocks vars global)

      | common_step_exit_S : forall n stl stl' blocks vars global,
        common_step
        (State ((exit (S n) :: stl) :: (stl' :: blocks)) vars global)
        (State ((exit n :: stl') :: blocks) vars global)
        
      | common_step_native :
        forall args source vars,
          map (fun a : sigT (ATOM.val (t := A)) => let (ty, va) := a in Some (atom va)) args =
          map (fun v => PTree.get v vars) source ->
          forall op rty rva,
            sem (n := NO) op args (existT _ rty rva) ->
            forall vars' target,
              vars' = PTree.set target (atom rva) vars ->
                forall stl blocks global,
                  common_step
                  (State ((native op source target :: stl) :: blocks) vars global)
                  (State (stl :: blocks) vars' global)
        .

    End Common.

    Section Source.
            
      Inductive source_specific_stmt : Type :=

C++ object-oriented features
      | source_null (class : ident) (target : var)
      | source_ptreq (ptr1 ptr2 : var) (target : var)
      | source_getfield (class : ident) (field : FieldSignature.t A) (source : var) (target : var)
      | source_putfield (class : ident) (field : FieldSignature.t A) (source : ident) (newvalue : var)
      | source_statcast (from : ident) (to : ident) (source : var) (target : var)
      | source_dyncast (from : ident) (to : ident) (source : var) (target : var)
      | source_arrayindex (class : ident) (index : var) (source : var) (target : var)
        .

      Section Sem.

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

        Inductive valid_pointer_or_null (g : Globals.t A) : Value.pointer A -> Prop :=
        | valid_pointer_valid :
          forall ptr,
            Globals.valid_pointer hierarchy g ptr ->
            valid_pointer_or_null g ptr
        | valid_pointer_null : forall ty,
          valid_pointer_or_null g (Value.null A ty)
.

        Notation state := (state (Value.t A) source_specific_stmt (Globals.t A)) (only parsing).

      Inductive source_step : state -> state -> Prop :=
      | source_step_common : forall s1 s2,
        common_step (@Value.atom A) s1 s2 ->
        source_step s1 s2

null pointer
      | source_step_null : forall vars vars' class target,
        vars' = PTree.set target (Value.ptr (Value.null A class)) vars ->
          forall stl blocks global,
            source_step
            (State ((specific (source_null class target) :: stl) :: blocks) vars global)
            (State (stl :: blocks) vars' global)

      | step_ptreq : forall v1 ptr1 vars,
        vars ! v1 = Some (Value.ptr ptr1) ->
        forall global,
        valid_pointer_or_null global ptr1 ->
        forall v2 ptr2,
          vars ! v2 = Some (Value.ptr ptr2) ->
          valid_pointer_or_null global ptr2 ->
          Value.type_of (Value.ptr ptr1) = Value.type_of (Value.ptr ptr2) ->
          forall b : bool,
            (if b then (Value.ptr ptr1 = Value.ptr ptr2) else (Value.ptr ptr1 <> Value.ptr ptr2)) ->
              forall v, v = (if b then Value.atom _ (TRUE NO) else Value.atom _ (FALSE NO)) ->
          forall vars' target,
            vars' = PTree.set target v vars ->
              forall stl blocks,
                source_step
                (State ((specific (source_ptreq v1 v2 target) :: stl) :: blocks) vars global)
                (State (stl :: blocks) vars' global)

get field
      | step_getfield : forall vars source obj ar i h p hp,
        vars ! source = Some (Value.ptr (@Value.subobject _ obj ar i h p hp)) ->
        forall global,
          Globals.valid_pointer hierarchy global (Value.subobject obj ar i h _ hp) ->
          forall o, (Globals.heap global) ! obj = Some o ->
            forall class c, hierarchy ! class = Some c ->
              last p = Some class ->
              forall fs, In fs (Class.fields c) ->
                forall v, Object.get_field o (ar, i, (h, p), fs) = Some v ->
                  forall vars' target,
                    vars' = PTree.set target v vars ->
                      forall stl blocks,
                        source_step
                        (State ((specific (source_getfield class fs source target) :: stl) :: blocks) vars global)
                        (State (stl :: blocks) vars' global)

put field
      | step_putfield : forall vars source obj ar i h p hp,
        vars ! source = Some (Value.ptr (@Value.subobject _ obj ar i h p hp)) ->
        forall global,
          Globals.valid_pointer hierarchy global (Value.subobject obj ar i h _ hp) ->
          forall o, (Globals.heap global) ! obj = Some o ->
            forall class c, hierarchy ! class = Some c ->
              last p = Some class ->
              forall fs, In fs (Class.fields c) ->
                forall newvalue v,
                  vars ! newvalue = Some v ->
                  forall o', Object.put_field o (ar, i, (h, p), fs) v = Some o' ->
                    forall global', global' = Globals.update global obj o' ->
                      forall stl blocks,
                        source_step
                        (State ((specific (source_putfield class fs source newvalue) :: stl) :: blocks) vars global)
                        (State (stl :: blocks) vars global')


static cast
      | step_statcast : forall vars source obj ar i h p hp,
        vars ! source = Some (Value.ptr (@Value.subobject _ obj ar i h p hp)) ->
real : class of the most derived object
from : static type of the pointer
to : class to which to cast
        forall o global,
          (Globals.heap global) ! obj = Some o ->
          forall real from,
          valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) ar real i h p from ->
          forall to h' p',
          static_cast hierarchy real h p from to h' p' ->
          forall hp' target vars',
            vars' = PTree.set target (Value.ptr (@Value.subobject _ obj ar i h' p' hp')) vars ->
              forall stl blocks,
              source_step
              (State ((specific (source_statcast from to source target) :: stl) :: blocks) vars global)
              (State (stl :: blocks) vars' global)

dynamic cast
      | step_dyncast : forall vars source obj ar i h p hp,
        vars ! source = Some (Value.ptr (@Value.subobject _ obj ar i h p hp)) ->
real : class of the most derived object
from : static type of the pointer
to : class to which to cast
        forall o global,
          (Globals.heap global) ! obj = Some o ->
          forall real from,
          valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) ar real i h p from ->
          is_dynamic OP hierarchy from ->
          forall newptr to,
          (forall h' p',
          dynamic_cast hierarchy real h p from to h' p' -> exists hp', newptr = (@Value.subobject _ obj ar i h' p' hp')) ->
          ((forall h' p', dynamic_cast hierarchy real h p from to h' p' -> False) -> newptr = (Value.null _ to))->
          (forall h'' p'', path hierarchy to p'' from h'' -> False) ->
          forall target vars',
            vars' = PTree.set target (Value.ptr newptr) vars ->
              forall stl blocks,
              source_step
              (State ((specific (source_dyncast from to source target) :: stl) :: blocks) vars global)
              (State (stl :: blocks) vars' global)

array index
      | step_arrayindex : forall vars source obj ar i class hp,
        vars ! source = Some (Value.ptr (@Value.subobject _ obj ar i Class.Inheritance.Repeated (class :: nil) hp)) ->
        forall o global n,
          (Globals.heap global) ! obj = Some o ->
          valid_array_path hierarchy class n (Object.class o) (Object.arraysize o) ar ->
          0 <= i < n ->
          forall index tyj vaj, vars ! index = Some (Value.atom _ vaj) ->
            forall j,
              semZ NO (existT _ tyj vaj) = Some j ->
              0 <= i + j < n ->
              forall vars' target,
                vars' = PTree.set target (Value.ptr (Value.subobject obj ar (i + j) Class.Inheritance.Repeated _ hp)) vars ->
                  forall stl blocks,
                    source_step
                    (State ((specific (source_arrayindex class index source target) :: stl) :: blocks) vars global)
                    (State (stl :: blocks) vars' global)
.

    End Sem.

    End Source.

  Section Target.
    Variable (PF : PLATFORM A).
    
    Inductive val : Type :=
    | Ptr (_ : option Z)
    | Atom (ty : (ATOM.ty A)) (_ : (ATOM.val (t := A)) ty)
      .
    
    Inductive memval : Type :=
    | Vptr (class : ident) (_ : Class.Inheritance.t * list ident)
    | Val (_ : val)
    .

We assume all pointers to subobjects have the same size and alignment
    Variable ptrsize : Z.

  Function val_size (m : val) : Z :=
    match m with
      | Ptr _ => ptrsize
      | Atom ty _ => typ_size PF (Typ.atom ty)
    end.

  Function memval_size (m : memval) : Z :=
    match m with
      | Vptr _ _ => dynamic_type_data_size PF
      | Val v => val_size v
    end.

    Variable ptralign : Z.

  Function val_align (m : val) : Z :=
    match m with
      | Ptr _ => ptralign
      | Atom ty _ => typ_align PF (Typ.atom ty)
    end.

  Function memval_align (m : memval) : Z :=
    match m with
      | Vptr _ _ => dynamic_type_data_align PF
      | Val v => val_align v
    end.

  Record MEMORY : Type := Memory {
    mem : Type;
    load : Z -> mem -> Z -> option memval;
    store : Z -> mem -> Z -> memval -> option mem;

Assume infinite memory

The following axiom is the only needed way to store a value into memory: it requires the alignment to divide the offset, and the chunk size to be equal to the size of the actual data being written.

   store_some : forall i mv,
     (memval_align mv | i) ->
     forall m, store (memval_size mv) m i mv <> None;

   load_store_same : forall i sz mv m m',
       store sz m i mv = Some m' ->
       load sz m' i = Some mv;

   load_store_other : forall m i mv sz' m',
     store sz' m i mv = Some m' ->
     forall j sz,
       j + sz <= i \/ i + sz' <= j ->
       load sz m' j = load sz m j;

    H_ptrsize : forall cn, typ_size PF (Typ.class cn) = ptrsize;
    H_ptralign : forall cn, typ_align PF (Typ.class cn) = ptralign
}.

      Inductive target_specific_stmt : Type :=

low-level memory operations
      | target_load (chunksize : Z) (ptr : var) (off : Z) (target : var)
      | target_store (chunksize : Z) (ptr : var) (off : Z) (newvalue : var)

vtable operations
      | dyncast_exists (_ : ident) (vptr : var) (target : var)
      | dyncast_offset (_ : ident) (vptr : var) (target : var)
      | vbase_offset (_ : ident) (vptr : var) (target : var)

pointer arith
      | null (ptr' : var)
      | ptrshift (ptr : var) (off : Z) (ptr' : var)
      | ptrshiftmult (ptr : var) (delta : var) (factor : Z) (ptr' : var)
      | ptreq (ptr1 ptr2 : var) (target : var)
.

The following record type abstracts accesses to virtual tables (e.g. dynamic cast via RTTI). Virtual tables themselves are assumed to be located at a non-writable memory zone.

      Record vtable : Type := VTable {
        dyncast_offsets : ident -> option (option Z);
        vbase_offsets : ident -> option Z
      }.

      Section Sem.

        Variable vtables : ident -> (Class.Inheritance.t * list ident) -> option vtable.

        Variable MEM : MEMORY.

        Notation state := (state memval target_specific_stmt (mem MEM)) (only parsing).

      Inductive step : state -> state -> Prop :=
        
      | step_common : forall s1 s2,
        common_step (fun ty va => Val (@Atom ty va)) s1 s2 ->
        step s1 s2

low-level memory load
      | step_load : forall ptr z vars,
        vars ! ptr = Some (Val (Ptr (Some z))) ->
        forall sz m off v,
        load (m := MEM) sz m (z + off) = Some v ->
          forall target vars', vars' = PTree.set target v vars ->
            forall stl blocks,
            step
            (State ((specific (target_load sz ptr off target) :: stl) :: blocks) vars m)
            (State (stl :: blocks) vars' m)

low-level memory store
      | step_store : forall ptr z vars,
        vars ! ptr = Some (Val (Ptr (Some z))) ->
        forall newvalue v,
          vars ! newvalue = Some v ->
          forall m off m' sz,
            store (m := MEM) sz m (z + off) v = Some m' ->
            forall stl blocks,
              step
              (State ((specific (target_store sz ptr off newvalue) :: stl) :: blocks) vars m)
              (State (stl :: blocks) vars m')

dynamic cast offset retrieval from VTable : status
      | step_dyncast_exists : forall vptr cn hp vars,
        vars ! vptr = Some (Vptr cn hp) ->
        forall vtbl, vtables cn hp = Some vtbl ->
cn : most derived class, class : class to which dynamically cast
          forall oz class, dyncast_offsets vtbl class = Some oz ->
          forall b, match oz with
           | None => b = Atom (FALSE NO)
           | _ => b = Atom (TRUE NO)
           end ->
            forall target vars',
              vars' = PTree.set target (Val b) vars ->
                forall stl blocks m,
                step
                (State ((specific (dyncast_exists class vptr target) :: stl) :: blocks) vars m)
                (State (stl :: blocks) vars' m)

dynamic cast offset retrieval from VTable when successful
      | step_dyncast_offset : forall vptr cn hp vars,
        vars ! vptr = Some (Vptr cn hp) ->
        forall vtbl, vtables cn hp = Some vtbl ->
cn : most derived class, class : class to which dynamically cast
          forall z class, dyncast_offsets vtbl class = Some (Some z) ->
            forall target vars',
              vars' = PTree.set target (Val (let (ty, va) := Zsem NO z in Atom va)) vars ->
                forall stl blocks m,
                step
                (State ((specific (dyncast_offset class vptr target) :: stl) :: blocks) vars m)
                (State (stl :: blocks) vars' m)

virtual base offset retrieval from VTable
      | step_vbase_offset: forall vptr cn hp vars,
        vars ! vptr = Some (Vptr cn hp) ->
        forall vtbl, vtables cn hp = Some vtbl ->
cn : most derived class, class : virtual base of which to find the offset
          forall z class, vbase_offsets vtbl class = Some z ->
            forall target vars',
              vars' = PTree.set target (Val (let (ty, va) := Zsem NO z in Atom va)) vars ->
                forall stl blocks m,
                step
                (State ((specific (vbase_offset class vptr target) :: stl) :: blocks) vars m)
                (State (stl :: blocks) vars' m)

null pointer
      | step_null : forall vars vars' target,
        vars' = PTree.set target (Val (Ptr None)) vars ->
          forall stl blocks m,
            step
            (State ((specific (null target) :: stl) :: blocks) vars m)
            (State (stl :: blocks) vars' m)

constant shift
      | step_ptrshift : forall z vars ptr,
        vars ! ptr = Some (Val (Ptr (Some z))) ->
        forall off vars' target,
          vars' = PTree.set target (Val (Ptr (Some (z + off)))) vars ->
          forall stl blocks m,
            step
            (State ((specific (ptrshift ptr off target) :: stl) :: blocks) vars m)
            (State (stl :: blocks) vars' m)

variable shift (up to a constant factor)
      | step_ptrshiftmult : forall z vars ptr,
        vars ! ptr = Some (Val (Ptr (Some z))) ->
        forall delta tyoff vaoff,
          vars ! delta = Some (Val (@Atom tyoff vaoff)) ->
          forall off, semZ NO (existT _ _ vaoff) = Some off ->
        forall factor vars' target,
          vars' = PTree.set target (Val (Ptr (Some (z + off * factor)))) vars ->
          forall stl blocks m,
            step
            (State ((specific (ptrshiftmult ptr delta factor target) :: stl) :: blocks) vars m)
            (State (stl :: blocks) vars' m)

      | target_step_ptreq : forall ptr1 oz1 vars,
        vars ! ptr1 = Some (Val (Ptr oz1)) ->
        forall ptr2 oz2, vars ! ptr2 = Some (Val (Ptr oz2)) ->
        forall b : bool,
        (if b then (oz1 = oz2) else (oz1 <> oz2)) ->
        forall v, v = (if b then Val (Atom (TRUE NO)) else Val (Atom (FALSE NO))) ->
        forall vars' target, vars' = PTree.set target v vars ->
        forall stl blocks m,
        step
        (State ((specific (ptreq ptr1 ptr2 target) :: stl) :: blocks) vars m)
        (State (stl :: blocks) vars' m)
      .

    End Sem.

    End Target.

    Section Compiler.
      Variable PF : PLATFORM A.

      Variables psize palign : Z.

      Variable MEM : MEMORY PF psize palign.


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

      Variable offsets : PTree.t (LayoutConstraints.t A).

      Hypothesis Hhier : Well_formed_hierarchy.prop hierarchy.

We need this decision procedure to prove the invariant. Remember for instance that Theorem 5.4 is split into two parts: the empty part, and the non-empty part.
      Variable is_empty_dec : forall cl, {is_empty OP hierarchy cl} + {~ is_empty OP hierarchy cl}.
      
      Hypothesis intro : forall ci o, offsets ! ci = Some o -> class_level_prop OP PF offsets hierarchy ci o.
      
      Hypothesis guard : forall ci, offsets ! ci <> None -> hierarchy ! ci <> None.

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

      Hypothesis empty_prop : forall (ci : positive) (oc : LayoutConstraints.t A),
        offsets ! ci = Some oc ->
        disjoint_empty_base_offsets OP offsets hierarchy ci oc.

      Notation GARBAGE := (skip _) (only parsing).

      Definition paths := let (T, _) := Well_formed_hierarchy.paths Hhier in T.

      Notation SrcVar := (xO) (only parsing).
      Notation TmpVar := (xI) (only parsing).

      Function specific_compiler (s' : source_specific_stmt) {struct s'} : common_stmt target_specific_stmt :=
Compilation of C++ specific instructions
        match s' with

Null pointer
        | source_null _ target => specific (null (SrcVar target))

Pointer equality
        | source_ptreq ptr1 ptr2 target => specific (ptreq (SrcVar ptr1) (SrcVar ptr2) (SrcVar target))

get field (scalar or structure)
        | source_getfield class field source target =>
          match offsets ! class with
          | None => GARBAGE
          | Some o =>
            match assoc (FieldSignature.eq_dec (A := A)) field (field_offsets o) with
            | None => GARBAGE
            | Some fo =>
              match FieldSignature.type field with
              | FieldSignature.Scalar ty => specific (target_load (typ_size PF ty) (SrcVar source) fo (SrcVar target))
              | _ => specific (ptrshift (SrcVar source) fo (SrcVar target))
              end
            end
          end

put field (scalar only, cf. Object.put_field)
        | source_putfield class field source newvalue =>
          match offsets ! class with
          | None => GARBAGE
          | Some o =>
            match assoc (FieldSignature.eq_dec (A := A)) field (field_offsets o) with
            | None => GARBAGE
            | Some fo =>
              match FieldSignature.type field with
                | FieldSignature.Scalar ty =>
                  specific (target_store (typ_size PF ( ty)) (SrcVar source) fo (SrcVar newvalue))
                | _ => GARBAGE
              end
            end
          end

dynamic cast : directly read into Vtable
        | source_dyncast from to source target =>
          seq
          (specific (target_load (dynamic_type_data_size PF) (SrcVar source) 0 (TmpVar xH)))
          (seq
            (specific (dyncast_exists to (TmpVar xH) (TmpVar (xI xH))))
            (test (TmpVar (xI xH))
                (seq
                   (specific (dyncast_offset to (TmpVar xH) (TmpVar (xO xH))))
                   (specific (ptrshiftmult (SrcVar source) (TmpVar (xO xH)) 1 (SrcVar target)))
                )
                (specific (null (SrcVar target)))
            )
          )

static cast : two cases
        | source_statcast from to source target =>
          match peq from to with
            | left _ => specific (ptrshift (SrcVar source) 0 (SrcVar target))
            | _ =>
          match plt from to with
          | left _ =>
            match paths ! from with
            | None => GARBAGE
            | Some pfrom =>
              match pfrom ! to with
              | None => GARBAGE
              | Some l =>
                match filter (fun hp : _ * _ => match hp with
                                 | (Class.Inheritance.Repeated, _) => true
                                 | _ => false
                                end) l with
               | nil => GARBAGE
               | (_, p) :: _ =>
                 match non_virtual_subobject_offset offsets 0 p with
                 | None => GARBAGE
                 | Some off => specific (ptrshift (SrcVar source) (0 - off) (SrcVar target))
                 end
               end
              end
             end
           | right _ =>
           match paths ! to with
           | None => GARBAGE
           | Some pto =>
             match pto ! from with
             | Some ((Class.Inheritance.Repeated, p) :: _) =>
               match non_virtual_subobject_offset offsets 0 p with
               | None => GARBAGE
               | Some off => specific (ptrshift (SrcVar source) off (SrcVar target))
               end
             | Some ((Class.Inheritance.Shared, b :: p) :: _) =>
               match non_virtual_subobject_offset offsets 0 (b :: p) with
               | None => GARBAGE
               | Some off => seq
                 (specific (target_load (dynamic_type_data_size PF) (SrcVar source) 0 (TmpVar xH)))
                 (seq
                   (specific (vbase_offset b (TmpVar xH) (TmpVar (xO xH))))
                   (seq
                     (specific (ptrshiftmult (SrcVar source) (TmpVar (xO xH)) 1 (TmpVar (xI xH))))
                     (specific (ptrshift (TmpVar (xI xH)) off (SrcVar target)))
                   )
                 )
               end
             | _ => GARBAGE
             end
           end
          end
          end

array index
          | source_arrayindex class index source target =>
            match offsets ! class with
            | None => GARBAGE
            | Some o => specific (ptrshiftmult (SrcVar source) (SrcVar index) (size o) (SrcVar target))
            end

      end.
      
      Function compile (s : common_stmt source_specific_stmt) {struct s} : common_stmt target_specific_stmt :=
      match s with
      | skip => skip _
      | seq s1 s2 => seq (compile s1) (compile s2)
      | test var ifso ifnot => test (SrcVar var) (compile ifso) (compile ifnot)
      | block s' => block (compile s')
      | exit n => exit _ n
      | loop s' => loop (compile s')
      | native op args res => native _ op (map SrcVar args) (SrcVar res)
      | specific s' => specific_compiler s'
      end.
      

Construction of virtual tables

Dynamic cast for non-bases : show that if C is a class defining some behaviour (success or failure) to dyncast to X, if X is not a base of C, then, for any base B of C, the dynamic cast to X has the same behaviour.

      Lemma non_base_dyncast_stable : forall real c x, (forall h p, path hierarchy x p c h -> False) ->
      forall h p h' p',
         dynamic_cast hierarchy real h p c x h' p' ->
         forall hc, hierarchy ! c = Some hc ->
         forall b l, path hierarchy b (c :: l) c Class.Inheritance.Repeated ->
         dynamic_cast hierarchy real h (p ++ l) b x h' p'.
Proof.
        inversion 2; subst.
        destruct (H _ _ H2).

        intros.
        assert (path hierarchy b (p0 ++ l) x Class.Inheritance.Repeated).
         eapply path_concat.
         eassumption.
         eassumption.
         simpl.
         rewrite (path_last H2).
         destruct (peq c c); congruence.
        eapply dynamic_cast_downcast.
        assumption.
        eassumption.
        inversion H2; subst.
        revert H3.
        simpl.
        rewrite (path_last H1).
        destruct (peq x x); try congruence.
        rewrite <- app_ass.
        congruence.
       intros.
       eapply dynamic_cast_crosscast.
       eapply path_concat.
       eexact H1.
       eassumption.
       simpl.
       rewrite (path_last H1).
       destruct (peq c c); congruence.
       assumption.
       assumption.
Qed.

      Lemma non_base_dyncast_stable_recip : forall real c x, (forall h p, path hierarchy x p c h -> False) ->
         forall hc, hierarchy ! c = Some hc ->
         forall b l, path hierarchy b (c :: l) c Class.Inheritance.Repeated ->
         forall h p,
         path hierarchy c p real h ->
         forall h' p',
         dynamic_cast hierarchy real h (p ++ l) b x h' p' ->
         dynamic_cast hierarchy real h p c x h' p'.
Proof.
        inversion 5; subst.
        generalize (path_concat H1 H5).
        case_eq (concat (Class.Inheritance.Repeated, c :: l)
   (k, p0)
        ).
        intros.
        generalize (H9 _ _ (refl_equal _)).
        intro.
        destruct (H _ _ H10).
       generalize (path_concat H2 H1).
       simpl.
       rewrite (path_last H2).
       destruct (peq c c); try congruence.
       intros.
       generalize (H7 _ _ (refl_equal _)).
       intros.
       inversion H5; subst.
       revert H6.
       simpl.
       rewrite (path_last H4).
       destruct (peq x x); try congruence.
       injection 1; intros; subst.
       destruct (last_correct (path_last H4)).
       subst.
       revert H9.
       rewrite app_ass.
       simpl.
       destruct (last_correct (path_last H2)).
       subst.
       intros.
       assert (In c (x0 ++ x :: lf)).
       rewrite <- H9.
       eauto using in_or_app.
       destruct (in_app_or _ _ _ H12).
        destruct (member_extract H13).
        invall; subst.
        assert (
          is_valid_repeated_subobject hierarchy ((x2 ++ c :: x3) ++ x :: nil) = true
        ).
          generalize (path_path0 H4).
          inversion 1; congruence.
        rewrite app_ass in H14.
        simpl in H14.
        generalize (is_valid_repeated_subobject_split_right H14).
        intro.
        destruct (H Class.Inheritance.Repeated ((c :: x3) ++ x :: nil)).
        eleft.
        reflexivity.
        reflexivity.
        assumption.
     destruct (member_extract H13).
     invall.
     assert (exists l', x :: l' = x2 ++ c :: nil).
       destruct x2; simpl in *.
       exists nil.
        congruence.
       injection H15; intros; subst.
       esplit.
       reflexivity.
      invall.
     assert (path hierarchy c (x2 ++ c :: nil) x Class.Inheritance.Repeated).
     eleft.
     symmetry; eassumption.
     reflexivity.
     generalize H11.
     rewrite H15.
     intro.
     eauto using is_valid_repeated_subobject_split_left.
    eapply dynamic_cast_downcast.
    assumption.
    eassumption.
    simpl.
    rewrite <- H16.
    simpl.
    rewrite last_complete.
    destruct (peq x x); try congruence.
    assert (x4 ++ x3 = lf).
     cut ((x :: x4) ++ x3 = x :: lf).
     simpl; congruence.
     rewrite H16.
     rewrite app_ass.
     simpl.
     auto.
    subst.
    rewrite app_ass.
    simpl.
    rewrite H16.
    cut (x1 = x0 ++ x2).
     rewrite <- app_ass.
     congruence.
    revert H9.
    rewrite H15.
    rewrite app_ass.
    simpl.
    rewrite <- app_ass.
    assert (is_valid_repeated_subobject hierarchy (x1 ++ c :: nil) = true).
      generalize (path_path0 H2).
      inversion 1; congruence.
    inversion H1; subst.
    generalize (is_valid_repeated_subobject_join H9 H19).
    intro.
    generalize (Well_formed_hierarchy.is_valid_repeated_subobject_sorted Hhier H20).
    intros.
    refine (_ (sorted_decomp_unique _ (sorted_elim _ H21) (refl_equal _) H22)).
    congruence.
    apply Plt_irrefl.
    intros; eauto using Plt_trans.
   eapply dynamic_cast_crosscast.
   assumption.
   assumption.
   assumption.

Qed.

Inductive dyncast_offset_spec : ident -> (Class.Inheritance.t * list ident) -> ident -> option Z -> Prop :=
| dyncast_offset_not_base_some :
  forall real h p cn,
  last p = Some cn ->
  forall x, (forall h' p', path hierarchy x p' cn h' -> False) ->
  forall h' p',
  dynamic_cast hierarchy real h p cn x h' p' ->
  forall z, subobject_offset offsets real p = Some z ->
  forall z', subobject_offset offsets real p' = Some z' ->
  forall res, res = z' - z ->
  dyncast_offset_spec real (h, p) x (Some res)

| dyncast_offset_not_base_none :
  forall real h p cn,
  last p = Some cn ->
  forall x, (forall h' p', path hierarchy x p' cn h' -> False) ->
  (forall h' p',
  dynamic_cast hierarchy real h p cn x h' p' -> False) ->
  dyncast_offset_spec real (h, p) x None
  
| dyncast_offset_base_with_primary :
  forall real h p cn,
  last p = Some cn ->
  forall x h' p', path hierarchy x p' cn h' ->
  forall of, offsets ! cn = Some of ->
  forall b, primary_base of = Some b ->
  forall res, dyncast_offset_spec real (h, p ++ b :: nil) x res ->
  dyncast_offset_spec real (h, p) x res
.

Lemma dyncast_offset_spec_correct : forall l d,
is_primary_path offsets (d :: l) = true ->
forall c, path hierarchy c (d :: l) d Class.Inheritance.Repeated ->
forall x, (forall h' p', path hierarchy x p' c h' -> False) ->
forall real h p, path hierarchy d p real h ->
(forall h' p', dynamic_cast hierarchy real h (p ++ l) c x h' p' ->
forall z, subobject_offset offsets real (p ++ l) = Some z ->
forall z', subobject_offset offsets real p' = Some z' ->
dyncast_offset_spec real (h, p) x (Some (z' - z))) /\
((forall h' p', dynamic_cast hierarchy real h (p ++ l) c x h' p' -> False) ->
dyncast_offset_spec real (h, p) x None).
Proof.
  induction l.
  intros until 2.
  generalize (path_last H0).
  injection 1; intro; subst.
  intros.
  rewrite <- app_nil_end.
  split.
   intros.
   econstructor.
   eapply path_last.
   eassumption.
   assumption.
   eassumption.
   eassumption.
   eassumption.
   trivial.
intros.
econstructor.
eapply path_last.
eassumption.
assumption.
assumption.

intros until 1.
generalize H.
rewrite is_primary_path_equation.
case_eq (offsets ! d); try congruence.
intros until 1.
destruct (
option_eq_dec peq (primary_base t) (Some a)
); try congruence.
intros.
assert (path hierarchy c (a :: l) a Class.Inheritance.Repeated).
 inversion H2; subst.
 injection H5; intros; subst.
 generalize H6.
 destruct lt; simpl; try congruence.
 injection 1; intros; subst.
 functional inversion H7; subst.
 eleft.
   reflexivity.
   eassumption.
   assumption.
assert (path hierarchy a (d :: a :: nil) d Class.Inheritance.Repeated).
 inversion H2; subst.
 generalize (is_valid_repeated_subobject_split_left (l1 := d :: nil) H8).
 intros.
 eleft with (lt := d :: nil).
 reflexivity.
 reflexivity.
 assumption.
generalize (path_concat H4 H6).
intro.
simpl in H7.
rewrite (path_last H4) in H7.
destruct (peq d d); try congruence.
generalize (H7 _ _ (refl_equal _)).
intros.
destruct (Well_formed_hierarchy.paths Hhier).
invall.
assert (
 (exists h', exists p', path hierarchy x p' d h') \/ forall h' p',
 path hierarchy x p' d h' -> False
).
case_eq (hierarchy ! x).
 intros.
 assert (hierarchy ! x <> None) by congruence.
 assert (x0 ! x <> None) by eauto.
 case_eq (x0 ! x); try congruence.
 intros.
 generalize (H10 _ _ H14).
 destruct 1.
 assert (hierarchy ! d <> None) by eauto using path_defined_to.
 assert (t1 ! d <> None) by eauto.
 case_eq (t1 ! d); try congruence.
 intros.
 destruct l0.
  right.
  intros.
  generalize (H16 _ _ H19 (h', p')).
  simpl; tauto.
 generalize (H16 _ _ H19 p0).
 destruct 1.
 destruct p0.
 generalize (H20 (or_introl _ (refl_equal _))).
 eauto.
 intros.
 right.
  intros.
  eapply path_defined_to.
  eexact H12.
  assumption.
destruct H11.
 invall.
 generalize (IHl _ H1 _ H5 _ H3 _ _ _ H8).
 repeat rewrite app_ass.
 simpl.
 destruct 1.
split.
intros.
eapply dyncast_offset_base_with_primary.
 eauto using path_last.
 eassumption.
 eassumption.
 eassumption.
 eauto.
intros.
eapply dyncast_offset_base_with_primary.
 eauto using path_last.
 eassumption.
 eassumption.
 eassumption.
 eauto.
split.
intros.
assert (hierarchy ! d <> None) by eauto using path_defined_from.
case_eq (hierarchy ! d); try congruence.
intros.
functional inversion H13; subst.
destruct (last_correct (path_last H4)).
subst.
assert (exists y, b :: y = x1 ++ d :: nil).
 revert H17.
 destruct x1; simpl.
  injection 1; intros; subst; eauto.
 injection 1; intros; subst; eauto.
invall.
generalize H18.
rewrite H17.
rewrite app_ass.
simpl.
intro.
generalize (non_virtual_subobject_offset_app_recip H20).
intros; invall; subst.
rewrite (primary_path_offset intro H) in H25.
injection H25; intro; subst.
eapply dyncast_offset_not_base_some.
eauto using path_last.
assumption.
eapply non_base_dyncast_stable_recip.
assumption.
eassumption.
eexact H2.
assumption.
eassumption.
rewrite <- H22.
unfold subobject_offset.
rewrite H19.
rewrite H21.
rewrite H22.
eassumption.
eassumption.
reflexivity.

intros.
eapply dyncast_offset_not_base_none.
eauto using path_last.
assumption.
intros.
assert (hierarchy ! d <> None) by eauto using path_defined_from.
case_eq (hierarchy ! d); try congruence.
intros.
eapply H12.
eapply non_base_dyncast_stable.
eassumption.
eassumption.
eassumption.
assumption.

Qed.

Corollary dyncast_offset_spec_reduce_path :
forall c x, (forall h' p', path hierarchy x p' c h' -> False) ->
forall real h p, path hierarchy c p real h ->
(forall h' p', dynamic_cast hierarchy real h p c x h' p' ->
forall z, subobject_offset offsets real p = Some z ->
forall z', subobject_offset offsets real p' = Some z' ->
dyncast_offset_spec real (h, reduce_path offsets p) x (Some (z' - z))) /\
((forall h' p', dynamic_cast hierarchy real h p c x h' p' -> False) ->
dyncast_offset_spec real (h, reduce_path offsets p) x None).
Proof.
 intros.
 destruct (reduce_path_prefix offsets Hhier H0).
 invall.
revert H1 H3.
generalize (reduce_path offsets p).
intros; subst.
eauto using dyncast_offset_spec_correct.
Qed.

Lemma dyncast_offset_spec_func : forall real hp x oz1,
dyncast_offset_spec real hp x oz1 ->
forall oz2, dyncast_offset_spec real hp x oz2 ->
oz1 = oz2.
Proof.
 induction 1; inversion 1; subst; try congruence;
 replace cn0 with cn in * by congruence.
 generalize (Well_formed_hierarchy.dynamic_cast_unique Hhier H1 H10).
 congruence.
 destruct (H13 _ _ H1).
 destruct (H0 _ _ H9).
 destruct (H1 _ _ H7).
 destruct (H0 _ _ H6).
 destruct (H8 _ _ H0).
 destruct (H9 _ _ H0).
 replace of0 with of in * by congruence.
 replace b0 with b in * by congruence.
 eauto.
Qed.

Lemma dyncast_offset_spec_exists : forall real hp x,
  {oz | dyncast_offset_spec real hp x oz} + {forall oz, dyncast_offset_spec real hp x oz -> False}.
Proof.
  destruct hp.
  intros.
  destruct (Well_formed_hierarchy.paths Hhier).
  invall.
  case_eq (last l).
   Focus 2.
   intro.
   right.
   inversion 1; congruence.
  intro i.
  revert t l x.
  induction i using (well_founded_induction Plt_wf).
  intros.
  case_eq (hierarchy ! x).
   Focus 2.
   intros.
   left.
   exists None.
   eapply dyncast_offset_not_base_none.
   eassumption.
   intros.
   generalize (path_defined_to H4).
   tauto.
   intros.
   assert (path hierarchy x p' real h').
    inversion H4; eauto using path_concat.
   generalize (path_defined_to H5).
   tauto.
  intros.
  assert (hierarchy ! x <> None) by congruence.
  assert (x0 ! x <> None) by eauto.
  case_eq (x0 ! x); try congruence.
  case_eq (hierarchy ! i).
   Focus 2.
   intros.
   left.
   exists None.
   eapply dyncast_offset_not_base_none.
   eassumption.
   intros.
   generalize (path_defined_from H8).
   tauto.
   intros.
   assert (path hierarchy i l real t).
    inversion H8; subst; eauto using path_concat.
   generalize (path_defined_to H9).
   tauto.
  intros.
  assert (hierarchy ! i <> None) by congruence.
  destruct (H0 _ _ H7).
  assert (t2 ! i <> None) by eauto.
  case_eq (t2 ! i); try congruence.
  destruct l0.
   intros.
   generalize (fun k p => let (_, l) := H10 _ _ H12 (k, p) in l).
   simpl.
   intros.
   destruct (Well_formed_hierarchy.dynamic_cast_dec Hhier real t l i x).
    invall.
   assert (path hierarchy i l real t).
    inversion H15; subst; eauto using path_concat.
   assert (path hierarchy x x2 real x1).
    inversion H15; eauto using path_concat.
   refine (_ (subobject_offset_exist Hhier intro guard _ (Plt_succ _) H14)).
   2 : eauto.
   case_eq (subobject_offset offsets real l); try congruence.
   refine (_ (subobject_offset_exist Hhier intro guard _ (Plt_succ _) H16)).
   2 : eauto.
   case_eq (subobject_offset offsets real x2); try congruence.
   intros.
   left.
   exists (Some (z - z0)).
   eapply dyncast_offset_not_base_some.
   eassumption.
   assumption.
   eassumption.
   eassumption.
   eassumption.
   trivial.
  left.
  exists None.
  eapply dyncast_offset_not_base_none.
  eassumption.
  assumption.
  assumption.
 intro.
 destruct (H10 _ _ H12 p).
 generalize (H13 (or_introl _ (refl_equal _))).
 destruct p.
 intros.
 assert (offsets ! i <> None) by eauto.
 case_eq (offsets ! i); try congruence.
 intros.
 case_eq (primary_base t4).
 intros.
 generalize (non_virtual_primary_base_offset (intro H17) H18).
 intros.
 assert ((non_virtual_direct_base_offsets t4) ! i0 <> None) by congruence.
 generalize (non_virtual_direct_base_offsets_guard (intro H17) H20 H6).
 intros.
 assert (Plt i0 i) by eauto using Well_formed_hierarchy.well_founded.
 assert (last (l ++ i0 :: nil) = Some i0) by eauto using last_complete.
 destruct (H1 _ H22 t _ x H23).
  invall.
  left.
  exists x1.
  eapply dyncast_offset_base_with_primary.
  eassumption.
  eassumption.
  eassumption.
  eassumption.
  assumption.
 right.
 inversion 1; subst; replace cn with i in * by congruence.
  destruct (H28 _ _ H15).
  destruct (H29 _ _ H15).
  replace i0 with b in * by congruence.
  destruct (f _ H34).
right.
inversion 1; intros; subst; replace cn with i in * by congruence.
 destruct (H23 _ _ H15).
 destruct (H24 _ _ H15).
congruence.

Qed.

Corollary dyncast_offset_strong : forall real hp, {
  dyo | forall x y, dyo x = Some y <-> dyncast_offset_spec real hp x y
}.
Proof.
  intros.
  exists (fun x => match dyncast_offset_spec_exists real hp x with
                     | inleft y2 => let (y, _) := y2 in Some y
                     | _ => None
                   end).
  intros.
  destruct (dyncast_offset_spec_exists real hp x).
   destruct s.
   split.
   congruence.
   intros. f_equal. eauto using dyncast_offset_spec_func.
  split. congruence.
  intros.
  destruct (f _ H).
Qed.


Function vboffsets (class : ident) (hp : Class.Inheritance.t * list ident) (vb : ident) : option Z :=
      let (h, p) := hp in
      match subobject_offset offsets class p with
      | None => None
      | Some off =>
      match offsets ! class with
      | None => None
      | Some o =>
        match (virtual_base_offsets o) ! vb with
        | None => None
        | Some off' => Some (off' - off)
        end
        end
       end
      .

Definition vtables i hp := Some (VTable
  (let (y, _) := dyncast_offset_strong i hp in y)
  (vboffsets i hp)
).

Lemma vtables_exist : forall class h p to, path hierarchy to p class h -> is_dynamic OP hierarchy to -> vtables class (h, p) <> None.
Proof.
  unfold vtables; congruence.
Qed.

Lemma vtables_prop : forall class h p to, path hierarchy to p class h -> is_dynamic OP hierarchy to -> forall dyncast_tbl vb_tbl, vtables class (h, p) = Some (VTable dyncast_tbl vb_tbl) -> (
(forall cn ooz, dyncast_tbl cn = Some ooz <-> dyncast_offset_spec class (h, p) cn ooz) /\
vb_tbl = vboffsets class (h, p)).
Proof.
  unfold vtables.
  injection 3; intros; subst.
  split; auto.
  intros.
  destruct (dyncast_offset_strong class (h, p)).
  auto.
Qed.

Opaque vtables.
   
offsets of objects (assumed to already exist)
  Variable objects : ident -> option Z.

 Section Invariant.

  Variables (s : state (Value.t A) source_specific_stmt (Globals.t A)) (t : state memval target_specific_stmt (mem MEM)).

  Fixpoint match_values (v : Value.t A) (w : memval) {struct v} : Prop :=
  match v with
  | Value.atom ty va => w = Val (Atom va)
  | Value.ptr (Value.null _) => w = Val (Ptr None)
  | Value.ptr (Value.subobject obj ar i h p hp) => exists off, w = Val (Ptr (Some off)) /\
    forall o, (Globals.heap (global s)) ! obj = Some o ->
      forall real from, valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) ar real i h p from ->
        forall oh, objects obj = Some oh ->
          relative_pointer_offset offsets (Object.class o) real ar i p = Some (off - oh)
  end.
   
  Record invariant := invariant_intro {
    invariant_stmt : pc t = map (map compile) (pc s);
    invariant_valid : Globals.valid (global s);
    invariant_vars : forall v vr, (vars s) ! v = Some vr -> exists vs, (vars t) ! (SrcVar v) = Some vs /\ match_values vr vs;
    invariant_objects : forall obj o,
      (Globals.heap (global s)) ! obj = Some o ->
      exists c, offsets ! (Object.class o) = Some c /\
        exists off, objects obj = Some off /\ (align c | off);
    invariant_fields : forall obj o,
      (Globals.heap (global s)) ! obj = Some o ->
      forall ar real i h p from,
        valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) ar real i h p from ->
        forall cfrom, hierarchy ! from = Some cfrom ->
          forall fs, In fs (Class.fields cfrom) ->
            forall ty, FieldSignature.type fs = FieldSignature.Scalar ty ->
              forall vr, Object.get_field o (ar, i, (h, p), fs) = Some vr ->
                forall oh, objects obj = Some oh ->
                  forall off, relative_pointer_offset offsets (Object.class o) real ar i p = Some off ->
                    forall ofrom, offsets ! from = Some ofrom ->
                      forall foff, assoc (FieldSignature.eq_dec (A := A)) fs (field_offsets ofrom) = Some foff ->
                        exists vs, load (m := MEM) (typ_size PF ( ty)) (global t) (oh + off + foff) = Some vs /\ match_values vr vs
                          ;
    invariant_vptr : forall obj o,
      (Globals.heap (global s)) ! obj = Some o ->
      forall ar real i h p from,
        valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) ar real i h p from ->
        is_dynamic OP hierarchy from ->
        forall oh, objects obj = Some oh ->
          forall off, relative_pointer_offset offsets (Object.class o) real ar i (reduce_path offsets p) = Some off ->
            load (m := MEM) (dynamic_type_data_size PF) (global t) (oh + off) = Some (Vptr real (h, reduce_path offsets p))
              ;
    invariant_disjoint_objects : forall obj1 obj2,
      obj1 <> obj2 ->
      forall o1, ((Globals.heap (global s)) ! obj1 = Some o1) ->
        forall o2, ((Globals.heap (global s)) ! obj2 = Some o2) ->
          forall of1, offsets ! (Object.class o1) = Some of1 ->
            forall of2, offsets ! (Object.class o2) = Some of2 ->
              forall off1, objects obj1 = Some off1 ->
                forall off2, objects obj2 = Some off2 ->
                  off1 + Object.arraysize o1 * size of1 <= off2 \/ off2 + Object.arraysize o2 * size of2 <= off1
  }.

  End Invariant.

  Section Preservation.

  Variables (s : state (Value.t A) source_specific_stmt (Globals.t A)) (t : state memval target_specific_stmt (mem MEM)) (invar : invariant s t).

  Variables (s' : state (Value.t A) source_specific_stmt (Globals.t A)) (Hst : source_step hierarchy s s').

  Lemma map_variables : forall source args,
    map
    (fun a : sigT (ATOM.val (t := A)) =>
      let (ty, va) := a in Some (Value.atom _ va)) args =
    map (fun v : positive => (vars s) ! v) source ->
    map
    (fun a : sigT (ATOM.val (t := A)) =>
      let (ty, va) := a in Some (Val (Atom va))) args =
    map (fun v : positive => (vars t) ! v) (map SrcVar source).
Proof.
    induction source; destruct args; simpl; try congruence.
    destruct s0.
    injection 1; intros; subst.
    f_equal.
    symmetry in H1; symmetry.
    destruct (invariant_vars invar H1).
    destruct H2.
    simpl in H3.
    subst.
    assumption.
    eauto.
  Qed.

  Lemma array_path_offset_right : forall cn ar n cn' n', valid_array_path hierarchy cn' n' cn n ar -> forall accu o,
    array_path_offset offsets accu cn ar = Some o ->

      forall co', offsets ! cn' = Some co' ->
      forall i, 0 <= i < n' -> forall h p cl, path hierarchy cl p cn' h ->
        forall z, subobject_offset offsets cn' p = Some z ->
          forall co, offsets ! cl = Some co ->
            forall fs fz, assoc (FieldSignature.eq_dec (A := A)) fs (field_offsets co) = Some fz ->
              forall ty n'', FieldSignature.type fs = FieldSignature.Struct ty n'' ->
              array_path_offset offsets accu cn (ar ++ (i, (h, p), fs) :: nil) = Some (o + i * size co' + z + fz).
Proof.
    induction 1;
    functional inversion 1; subst; simpl.
     intros.
     rewrite H2.
     rewrite H5.
     rewrite (path_last H4).
     rewrite H6.
     rewrite H8.
     rewrite H7.
     trivial.
    intros.
    rewrite H13.
    rewrite H16.
    rewrite H18.
    rewrite H19.
    rewrite H20.
    rewrite H21.
    replace ci'0 with by in * by congruence.
    replace _x0 with by_n in * by congruence.
    erewrite IHvalid_array_path.
    reflexivity.
    assumption.
    assumption.
    assumption.
    eassumption.
    assumption.
    eassumption.
    assumption.
    eassumption.
Qed.

Lemma match_values_align : forall v w,
match_values s v w ->
typ_align PF
( (Value.type_of v))
= memval_align PF palign w
.
Proof.
  destruct v; simpl; intros; subst; simpl; trivial.
  destruct p; subst; simpl; eauto using H_ptralign.
  invall; subst; simpl; trivial.
  destruct ( is_some_constr (x:=last l) i); simpl; eauto using H_ptralign.
Qed.
  
Lemma match_values_size : forall v w,
match_values s v w ->
typ_size PF
( (Value.type_of v))
= memval_size PF psize w
.
Proof.
  destruct v; simpl; intros; subst; simpl; trivial.
  destruct p; subst; simpl; eauto using H_ptrsize.
  invall; subst; simpl; trivial.
  destruct ( is_some_constr (x:=last l) i); eauto using H_ptrsize.
Qed.
 
Lemma subobject_offset_reduce_path : forall class h p to,
path hierarchy to p class h ->
subobject_offset offsets class p = subobject_offset offsets class (reduce_path offsets p).
Proof.
intros.
refine (_ (subobject_offset_exist Hhier intro guard _ (Plt_succ _) H)).
2 : eauto.
case_eq (subobject_offset offsets class p); try congruence.
functional inversion 1; subst.
  destruct (reduce_path_prefix offsets Hhier H).
  invall.
  revert H3 H6.
  case_eq (reduce_path offsets (b :: _x)).
   intros.
    generalize (path_path0 H6).
    inversion 1; discriminate.
  intros.
  generalize H7.
  intro.
  simpl in H9.
  injection H9; intros; subst.
  unfold subobject_offset.
  rewrite H2.
  rewrite H5.
  destruct (last_correct (path_last H6)).
  revert H1.
  change (i :: l ++ x0) with ((i :: l) ++ x0).
  rewrite e.
  rewrite app_ass.
  simpl.
  intros.
  destruct (non_virtual_subobject_offset_app_recip H1).
  invall.
  rewrite (primary_path_offset intro H8) in H12.
  injection H12; intros; subst.
  congruence.
Qed.

Corollary relative_pointer_offset_reduce_path : forall class size ar real i h p from,
        valid_relative_pointer hierarchy class size ar real i h p from ->
        relative_pointer_offset offsets class real ar i p = relative_pointer_offset offsets class real ar i (reduce_path offsets p)
.
Proof.
  inversion 1; subst.
  refine (_ (relative_pointer_offset_exist Hhier intro guard _ (Plt_succ _) H)).
  2 : eauto.
  case_eq (relative_pointer_offset offsets class real ar i p); try congruence.
  functional inversion 1; subst.
  unfold relative_pointer_offset.
  rewrite H6.
  rewrite H7.
  rewrite <- (subobject_offset_reduce_path H3).
  rewrite H8.
  trivial.
Qed.

Lemma path_repeated_virtual_base : forall l to from,
  path hierarchy to l from Class.Inheritance.Repeated ->
  forall b, is_virtual_base_of hierarchy b to ->
    is_virtual_base_of hierarchy b from.
Proof.
  induction l; inversion 1; subst; try congruence.
  injection H0; intros; subst.
  functional inversion H2; subst.
   generalize (path_last H).
   injection 1; intros; subst.
   assumption.
   destruct lt; simpl in H1; try discriminate.
   injection H1; intros; subst.
   eright.
   eassumption.
   eassumption.
   eapply IHl.
   eleft.
   reflexivity.
   eassumption.
   assumption.
   assumption.
Qed.

Corollary path_virtual_base : forall to l from h, path hierarchy to l from h ->
  forall b, is_virtual_base_of hierarchy b to ->
    is_virtual_base_of hierarchy b from.
Proof.
  intros until 1.
  generalize (path_path1 H).
  induction 1.
  eauto using path_repeated_virtual_base.
  intros.
  eapply is_virtual_base_of_trans.
  eauto using path_repeated_virtual_base.
  eauto using path_repeated_virtual_base.
Qed.

Lemma valid_array_path_offset : forall to zto from zfrom p,
  valid_array_path hierarchy to zto from zfrom p ->
  offsets ! from <> None ->
  offsets ! to <> None.
Proof.
  induction 1.
   tauto.
  intros.
  apply IHvalid_array_path.
  eapply exist.
  eauto using Well_formed_hierarchy.complete_struct.
Qed.

  Theorem preservation : exists t', clos_trans _ (step vtables (MEM := MEM)) t t' /\ invariant s' t'.
Proof.
    generalize map_variables match_values_align match_values_size.
    intros map_vars0 match_values_align0 match_values_size0.
    inversion invar.
    Opaque Object.get_field Object.put_field PTree.get PTree.set non_virtual_subobject_offset.

    inversion Hst; subst; destruct t; simpl in *; subst.

common
    inversion H; subst; simpl in *; subst; try abstract (
      esplit;
        split; [
          eleft;
            econstructor;
              econstructor |
                constructor; simpl; trivial
        ]
    ).

test
    destruct (invariant_vars0 _ _ H0).
    destruct H2.
    simpl in H3.
    subst.
    esplit.
    split.
     eleft.
     econstructor.
     econstructor.
     eassumption.
     eassumption.
     reflexivity.
    constructor; simpl; trivial.
    destruct b; trivial.

native
    generalize (map_vars0 _ _ H0).
    intros.
    esplit.
    split.
    eleft.
    econstructor.
    econstructor.
    eexact H2.
    eassumption.
    reflexivity.
    constructor; simpl; trivial.
    intro.
    destruct (peq v target).
     subst.
     rewrite PTree.gss.
     rewrite PTree.gss.
     injection 1; intros; subst.
     esplit.
     split.
      reflexivity.
     simpl.
     trivial.
    rewrite PTree.gso; eauto.
    rewrite PTree.gso; eauto.
    intros.
    destruct (invariant_vars0 _ _ H3).
    destruct H4.
    esplit.
    split.
     eassumption.
    destruct vr; simpl in *; trivial.
    congruence.

null pointer
  esplit.
  split.
   eleft.
   eapply step_null.
   reflexivity.
  econstructor; simpl; trivial.
  intro.
    destruct (peq v target).
     subst.
     rewrite PTree.gss.
     rewrite PTree.gss.
     injection 1; intros; subst.
     esplit.
     split.
      reflexivity.
     simpl.
     trivial.
    rewrite PTree.gso; eauto.
    rewrite PTree.gso; eauto.
    intros.
    destruct (invariant_vars0 _ _ H).
    destruct H0.
    esplit.
    split.
     eassumption.
    destruct vr; simpl in *; trivial.
    congruence.

ptreq
    destruct (invariant_vars0 _ _ H).
    destruct H5.
    simpl in H6.
    destruct (invariant_vars0 _ _ H1).
    destruct H7.
    simpl in H8.
    assert (exists pi2, x0 = Val (Ptr pi2)).
     destruct ptr2; invall; eauto.
    assert (exists pi1, x = Val (Ptr pi1)).
     destruct ptr1; invall; eauto.
    invall; subst.
    esplit.
    split.
    eleft.
    eapply target_step_ptreq with (b := b).
    eassumption.
    eassumption.
    2 : reflexivity.
    2 : reflexivity.
    destruct b.
     injection H4; intros; subst.
     destruct ptr2; subst; try congruence.
     invall; subst.
     injection H6; intros; subst.
     injection H8; intros; subst.
     inversion H2; subst.
     inversion H9; subst.
     inversion H19; subst.
     refine (_ (relative_pointer_offset_exist Hhier intro guard _ (Plt_succ _) H19)).
     2 : intros; eauto.
     intros.
     case_eq ( relative_pointer_offset offsets (Object.class o) through
         arraypath index l); try congruence.
     intros.
     destruct (invariant_objects0 _ _ H15).
     invall.
     generalize (H10 _ H15 _ _ H19 _ H21).
     generalize (H11 _ H15 _ _ H19 _ H21).
     intros.
     f_equal.
     assert (x - x3 = x0 - x3) by congruence.
     omega.
  destruct ptr1; destruct ptr2; invall; try congruence.
  injection H6; intros; subst.
  injection H8; intros; subst.
  inversion H0; subst.
  inversion H9; subst.
  inversion H19; subst.
  inversion H2; subst.
  inversion H17; subst.
  inversion H26; subst.
  assert (forall i1,
    (let (c, _) := is_some_constr (x:=last l0) i1 in
      Typ.class c) = Typ.class (A := A) to0).
  rewrite (path_last H23).
      simpl.
      intro i1.
      destruct (is_some_constr (x := Some to0) i1).
      congruence.
   assert (forall i2,
        (let (c, _) := is_some_constr (x:=last l) i2 in
          Typ.class c) = Typ.class (A := A) to).
   rewrite (path_last H16).
   simpl.
   intro i1.
   destruct (is_some_constr (x := Some to) i1).
   congruence.
   generalize i i0 H3.
   intros ? ?.
   rewrite H24.
   rewrite H25.
   injection 1; intros; subst.
   refine (_ (relative_pointer_offset_exist Hhier intro guard _ (Plt_succ _) H19)).
   2 : intros; eauto.
   intros.
   case_eq ( relative_pointer_offset offsets (Object.class o) through
     arraypath index l); try congruence.
   intros.
   destruct (invariant_objects0 _ _ H15).
   invall.
   generalize (H11 _ H15 _ _ H19 _ H31).
   intros.
   refine (_ (relative_pointer_offset_exist Hhier intro guard _ (Plt_succ _) H26)).
   2 : intros; eauto.
   intros.
   case_eq ( relative_pointer_offset offsets (Object.class o0) through0
     arraypath0 index0 l0); try congruence.
   intros.
   destruct (invariant_objects0 _ _ H22).
   invall.
   generalize (H10 _ H22 _ _ H26 _ H36).
   intros.
   cut (x <> x0).
     congruence.
   destruct (peq (Object.index o0) (Object.index o)).
    replace o0 with o in * by congruence.
    replace x5 with x2 in * by congruence.
    replace x6 with x3 in * by congruence.
    assert (offsets ! to0 <> None) by eauto using path_defined_to.
    destruct (is_empty_dec to0).
    intro; subst.
Theorem 4 empty
    generalize (disjoint_empty_base_offsets_disjoint_pointer_paths Hhier intro guard empty_prop i3 H38 H19 H26 H29 H34).
    injection 1; intros; subst.
    generalize (is_some_eq i i0).
    congruence.
    assert (
      ((arraypath, index, (inhkind, l)) <> (arraypath0, index0, (inhkind0, l0)))
      ).
     intro Habs.
     injection Habs; intros; subst.
     generalize (is_some_eq i i0).
     congruence.
Theorem 4 non-empty
     generalize (nonempty_distinct_offsets Hhier intro n H38 H19 H26 H29 H34 H39).
     omega.
objets differents
   generalize (invariant_disjoint_objects0 _ _ n _ H22 _ H15 _ H35 _ H30 _ H36 _ H31).
   intros.
   destruct (relative_pointer_offset_size intro H26 H34).
   assert (offsets ! to0 <> None) by eauto using path_defined_to.
   case_eq (offsets ! to0); try congruence.
   intros.
   generalize (H40 _ H35 _ H42).
   intros.
   generalize (non_virtual_size_positive (intro H42)).
   intro.
   destruct (relative_pointer_offset_size intro H19 H29).
   generalize (H46 _ H30 _ H42).
   omega.
et maintenant l'invariant
  constructor; simpl; trivial.
  intro.
    destruct (peq v target).
     subst.
     rewrite PTree.gss.
     rewrite PTree.gss.
     injection 1; intros; subst.
     esplit.
     split.
      reflexivity.
      destruct b; simpl; trivial.
    rewrite PTree.gso; eauto.
    rewrite PTree.gso; eauto.
    intros.
    destruct (invariant_vars0 _ _ H9).
    destruct H10.
    esplit.
    split.
     eassumption.
    destruct vr; simpl in *; trivial.
    congruence.

getfield
    assert (hierarchy ! class <> None) by congruence.
    assert (offsets ! class <> None) by eauto.
    case_eq (offsets ! class); try congruence.
    intros.
    generalize (field_offsets_exist (intro H8) H2 H4).
    case_eq (assoc (FieldSignature.eq_dec (A := A)) fs (field_offsets t0)); try congruence.
    intros.
    inversion H0; subst.
    inversion H18; subst.
    generalize (path_last H15).
    intros.
    replace to with class in * by congruence.
    replace o0 with o in * by congruence.
    case_eq (FieldSignature.type fs).
scalaire
     intros.
     destruct (invariant_objects0 _ _ H1).
     invall.
     refine (_ (relative_pointer_offset_exist Hhier intro guard _ (Plt_succ _) H18)).
     2 : eauto.
     case_eq (
       relative_pointer_offset offsets (Object.class o) through ar i p
     ); try congruence.
     intros.
     destruct (invariant_fields0 _ _ H1 _ _ _ _ _ _ H18 _ H2 _ H4 _ H17 _ H5 _ H21 _ H19 _ H8 _ H9).
     invall.
     destruct (invariant_vars0 _ _ H).
     invall.
     simpl in H27.
     invall; subst.
     generalize (H28 _ H1 _ _ H18 _ H21).
     rewrite H19.
     injection 1; intros; subst.
     esplit.
     split.
     eleft.
     eapply step_load.
     eassumption.
     replace (x4 + z) with (x0 + (x4 - x0) + z) by omega.
     eassumption.
     reflexivity.
    constructor; simpl; trivial.
    intro v0.
    destruct (peq v0 target).
     subst.
     repeat rewrite PTree.gss.
     injection 1; intros; subst.
     esplit.
     split.
     reflexivity.
     destruct vr; simpl in H25; trivial.
    repeat rewrite PTree.gso; eauto.
    intros.
    destruct (invariant_vars0 _ _ H27).
    destruct H29.
    esplit.
    split.
     eassumption.
    destruct vr; simpl in H30; trivial.
    congruence.
structure
    intros.
   generalize H5.
   Transparent Object.get_field.
   unfold Object.get_field.
   Opaque Object.get_field.
   rewrite H17.
   injection 1; intros; subst.
   assert (hierarchy ! struct <> None) by eauto using Well_formed_hierarchy.complete_struct.
   assert (
     valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) (ar ++ (i, (h, p), fs) :: nil) struct 0 Class.Inheritance.Repeated (struct :: nil) struct
   ).
   econstructor.
   eapply valid_array_path_concat.
   eassumption.
   econstructor.
   assumption.
   assumption.
   eassumption.
   eassumption.
   assumption.
   eassumption.
   eleft with (to_n := Zpos arraysize).
   compute; congruence.
   omega.
   omega.
   compute; trivial.
   eleft with (lt := nil).
   reflexivity.
   reflexivity.
   simpl.
   case_eq (hierarchy ! struct); congruence.
   assert (offsets ! struct <> None) by eauto.
   refine (_ (relative_pointer_offset_exist Hhier intro guard _ (Plt_succ _) H18)).
   2 : eauto.
   case_eq (
 relative_pointer_offset offsets (Object.class o) through ar i
     p
   ); try congruence.
   functional inversion 1.
   intros; subst.
   generalize (array_path_offset_right
H11 H25 H26 (conj H12 H13) H15 H27 H8 H9 H17).
   intros.
   case_eq (offsets ! struct); try congruence.
   intros.
   assert (relative_pointer_offset offsets (Object.class o)
     struct (ar ++ (i, (h, p), fs) :: nil)
 0 (struct :: nil) = Some
       (z1 + i * size ofto + z2 + z)
     ).
    unfold relative_pointer_offset.
    rewrite H24.
    rewrite H28.
    unfold subobject_offset.
    rewrite H28.
    rewrite (virtual_base_offsets_self (intro H28)).
    Transparent non_virtual_subobject_offset.
    simpl.
    Opaque non_virtual_subobject_offset.
    f_equal; omega.
    destruct (invariant_vars0 _ _ H).
    invall.
    simpl in H32.
    invall.
    subst.
    destruct (invariant_objects0 _ _ H1).
    invall.
    generalize (H33 _ H1 _ _ H18 _ H34).
    rewrite H23.
    injection 1; intros; subst.
    esplit.
    split.
    eleft.
    eapply step_ptrshift.
    eassumption.
    reflexivity.
    constructor; simpl; trivial.
    intro.
    destruct (peq v target).
     subst.
     repeat rewrite PTree.gss.
     injection 1; intros; subst.
     esplit.
     split.
      reflexivity.
     simpl.
     esplit.
     split.
      reflexivity.
     rewrite H1.
     injection 1; intro; subst.
     intros until 1.
     rewrite H34.
     injection 1; intros; subst.
     inversion H39; subst.
     inversion H21; subst.
     generalize (valid_array_path_last H41 H45).
     intros; subst.
     rewrite H29.
     f_equal; omega.
    repeat rewrite PTree.gso; eauto.
    intros.
    destruct (invariant_vars0 _ _ H37).
    invall.
    esplit.
    split.
    eassumption.
    destruct vr; simpl in *; trivial.
    congruence.

putfield
    assert (hierarchy ! class <> None) by congruence.
    assert (offsets ! class <> None) by eauto.
    case_eq (offsets ! class); try congruence.
    intros.
    generalize (field_offsets_exist (intro H9) H2 H4).
    case_eq (assoc (FieldSignature.eq_dec (A := A)) fs (field_offsets t0)); try congruence.
    intros.
    inversion H0; subst.
    inversion H19; subst.
    generalize (path_last H16).
    intros.
    replace to with class in * by congruence.
    replace o0 with o in * by congruence.
     destruct (invariant_objects0 _ _ H1).
     invall.
     refine (_ (relative_pointer_offset_exist Hhier intro guard _ (Plt_succ _) H19)).
     2 : eauto.
     case_eq (
       relative_pointer_offset offsets (Object.class o) through ar i p
     ); try congruence.
     intros.
     generalize (Object.put_field_type H6).
     intro.
Theorem 2
     generalize (field_align_prop Hhier intro H19 H18 H20 H9 (f := fs)).
     unfold field_align.
     rewrite H23.
     intro.
     destruct (H24 _ (refl_equal _) _ H10).
     destruct (invariant_vars0 _ _ H).
     invall.
     simpl in H29.
     invall; subst.
     generalize (H30 _ H1 _ _ H19 _ H21).
     rewrite H18.
     injection 1; intros; subst.
     destruct (invariant_vars0 _ _ H5).
     destruct H29.
     generalize (Zdivide_trans _ _ _ H25 H22).
     intros.
     generalize (Zdivide_plus_r _ _ _ H26 H32).
     replace (x3 - x0 + z + x0) with (x3 + z) by omega.
     rewrite (match_values_align0 _ _ H31).
     intro.
     generalize (store_some H33 (m0 := global1)).
     case_eq (store (memval_size PF psize x2) global1 (x3 + z) x2); try congruence.
     intros.
     esplit.
     split.
     eleft.
     eapply step_store.
     eassumption.
     eassumption.
     rewrite (match_values_size0 _ _ H31).
     eassumption.
    constructor; simpl; trivial.
    
    eapply Globals.valid_update.
    assumption.
    eassumption.
    eauto using Object.index_put_field.

    intros.
    destruct (invariant_vars0 _ _ H36).
    destruct H37.
    esplit.
    split.
     eassumption.
     destruct vr; simpl; trivial.
     destruct p0; simpl; trivial.
     simpl in H38.
     destruct H38.
     destruct H38.
     esplit.
     split.
     eassumption.
     destruct (peq array (Object.index o)).
      subst.
      rewrite PTree.gss.
      injection 1; intro; subst.
      rewrite (Object.class_put_field H6).
      rewrite (Object.arraysize_put_field H6).
      eauto.
     rewrite PTree.gso; try congruence; eauto.
    
    intro.
    destruct (peq obj (Object.index o)).
     subst.
     rewrite PTree.gss.
     injection 1; intros; subst.
     rewrite (Object.class_put_field H6).
     eauto.
    rewrite PTree.gso; try congruence; eauto.

    intro obj.
    destruct (peq obj (Object.index o)).
     subst.
     rewrite PTree.gss.
     injection 1; intro; subst.
     rewrite (Object.class_put_field H6).
     rewrite (Object.arraysize_put_field H6).
     intros.
     replace oh with x0 in * by congruence.
     destruct (cfield_dec (ar0, i0, (h0, p0), fs0) (ar, i, (h, p), fs)).
      injection e; intros until 5; subst.
      generalize (Object.get_put_field_same H6).
      rewrite H41.
      injection 1; intros; subst.
      inversion H37; subst.
      generalize (valid_array_path_last H12 H47).
      intros; subst.
      replace off with (x3 - x0) in * by congruence.
      generalize (path_last H50).
      generalize (path_last H16).
      intros.
      replace from with class in * by congruence.
      replace foff with z in * by congruence.
      replace (x0 + (x3 - x0) + z) with (x3 + z) by omega.
      replace ty with (Value.type_of v) by congruence.
      rewrite (match_values_size0 _ _ H31).
      rewrite (load_store_same H34).
      esplit.
      split.
       reflexivity.
      destruct v; trivial.
      destruct p0; trivial.
      revert H31.
      simpl.
      destruct 1.
      invall.
      esplit.
      split.
      eassumption.
      destruct (peq array (Object.index o)).
       subst.
       rewrite PTree.gss.
       injection 1; intro; subst.
       rewrite (Object.class_put_field H6).
       rewrite (Object.arraysize_put_field H6).
       eauto.
      rewrite PTree.gso; eauto.
      generalize (Object.get_field_type_scalar H41 H40).
      intro; subst.
      assert (
        (ar, i, (h, p), fs) <> (ar0, i0, (h0, p0), fs0)
      ) by congruence.
      rewrite (Object.get_put_field_other H6 H46) in H41.
      generalize (invariant_fields invar H1 H37 H38 H39 H40 H41 H42 H43 H44 H45).
     simpl.
     destruct 1.
     destruct H47.
Theorem 1
     generalize (scalar_fields_disjoint
Hhier intro guard H37 H19 H43 H18 H44 H9 H45 H40 H10 H23 n).
     repeat rewrite (match_values_size0 _ _ H48).
     repeat rewrite (match_values_size0 _ _ H31).
     intro.
     rewrite (match_values_size0 _ _ H48) in H47.
     rewrite (load_store_other H34).
     esplit.
     split.
      eassumption.
     destruct vr; trivial.
     destruct p1; trivial.
     simpl in H48; simpl.
     destruct H48.
     destruct H48.
     esplit.
     split.
      eassumption.
     destruct (peq array (Object.index o)).
      subst.
      repeat rewrite PTree.gss.
      injection 1; intro; subst.
      rewrite (Object.class_put_field H6).
      rewrite (Object.arraysize_put_field H6).
      eauto.
     rewrite PTree.gso; eauto.
     omega.
autres objets
     rewrite PTree.gso; eauto.
     intros.
     generalize (invariant_fields invar H36 H37 H38 H39 H40 H41 H42 H43 H44 H45).
     simpl.
     destruct 1.
     destruct H46.
     destruct (relative_pointer_offset_size intro H19 H18).
     generalize (H49 _ H20 _ H9).
     intros.
     destruct (relative_pointer_offset_size intro H37 H43).
     destruct (invariant_objects0 _ _ H36).
     invall; subst.
     replace x6 with oh in * by congruence.
     generalize (H52 _ H54 _ H44).
     intros.
     generalize (invariant_disjoint_objects0 _ _ n _ H36 _ H15 _ H54 _ H20 _ H55 _ H21).
     intros.
     generalize (field_offsets_low_bound (intro H44) H45).
     intros.
     generalize (non_virtual_size_field_offsets (intro H44) H45).
     unfold field_size.
     generalize (Object.get_field_type_scalar H41 H40).
     intro; subst.
     rewrite H40.
     intro.
     generalize (H59 _ (refl_equal _)).
     generalize (field_offsets_low_bound (intro H9) H10).
     intro.
     generalize (non_virtual_size_field_offsets (intro H9) H10).
     unfold field_size.
     rewrite H23.
     intro.
     generalize (H61 _ (refl_equal _)).
     revert H46.
     repeat rewrite (match_values_size0 _ _ H47).
     repeat rewrite (match_values_size0 _ _ H31).
     intros.
     rewrite (load_store_other H34).
     2 : omega.
     esplit.
     split.
       eassumption.
       destruct vr; trivial.
       destruct p1; trivial.
       destruct H47.
       destruct H47.
       esplit.
       split.
       eassumption.
       simpl.
       destruct (peq array (Object.index o)).
        subst.
        rewrite PTree.gss.
        injection 1; intro; subst.
        rewrite (Object.class_put_field H6).
        rewrite (Object.arraysize_put_field H6).
        eauto.
       rewrite PTree.gso; try congruence; eauto.

  intro.
  destruct (peq obj (Object.index o)).
   subst.
   rewrite PTree.gss.
   injection 1; intro; subst.
   rewrite (Object.class_put_field H6).
   rewrite (Object.arraysize_put_field H6).
   intros.
   replace x0 with oh in * by congruence.
   rewrite (load_store_other H34).
   eauto.
   generalize H40.
   rewrite <- (relative_pointer_offset_reduce_path H37).
   intro.
   assert (offsets ! from <> None).
    inversion H37; subst; eauto using path_defined_to.
Theorem 5
   generalize (scalar_field_dynamic_type_data_disjoint
   Hhier intro guard H19 H37 H18 H41 H9 H42 H10 H23 H38).
   rewrite (match_values_size0 _ _ H31).
   omega.
   rewrite PTree.gso; try congruence; eauto.
   intros.
   rewrite (load_store_other H34).
   eauto.
   destruct (invariant_objects invar H36).
   invall.
   replace x5 with oh in * by congruence.
   generalize (invariant_disjoint_objects invar n H36 H1 H42 H20 H43 H21).
   assert (offsets ! from <> None).
     inversion H37; subst; eauto using path_defined_to.
   case_eq (offsets ! from); try congruence.
   intros until 1.
   generalize H40.
   rewrite <- (relative_pointer_offset_reduce_path H37).
   intro.
   generalize (own_fields_offset_dynamic_low_bound (intro H45) H38).
   generalize (non_virtual_data_size_own_fields_offset (intro H45)).
   generalize (dynamic_nonempty H38).
   intro.
   destruct (relative_pointer_data_incl intro H37 H47 H46).
   generalize (H49 _ H42 _ H45).
   generalize (data_size_high_bound (intro H42)).
   assert ((Object.arraysize o1 - 1) * size x4 + size x4 = Object.arraysize o1 * size x4).
    ring.
   destruct (relative_pointer_offset_size intro H19 H18).
   generalize (H52 _ H20 _ H9).
   generalize (field_offsets_low_bound (intro H9) H10).
   generalize (non_virtual_size_field_offsets (intro H9) H10).
   unfold field_size.
   rewrite H23.
   intro.
   generalize (H53 _ (refl_equal _)).
   rewrite (match_values_size0 _ _ H31).
   omega.

   intros until 1.
   destruct (peq obj1 (Object.index o)).
     subst.
     rewrite PTree.gss.
     injection 1; intro; subst.
     rewrite (Object.class_put_field H6).
     rewrite (Object.arraysize_put_field H6).
     rewrite PTree.gso; try congruence; eauto.
    rewrite PTree.gso; try congruence; eauto.
    destruct (peq obj2 (Object.index o)).
      subst.
      rewrite PTree.gss.
      injection 2; intro; subst.
      rewrite (Object.class_put_field H6).
      rewrite (Object.arraysize_put_field H6).
      eauto.
     rewrite PTree.gso; try congruence; eauto.

destruct (peq from to).
 subst.
 assert (
   (h', p') = (h, p)
 ).
 inversion H2; subst.
 generalize (Well_formed_hierarchy.self_path_trivial Hhier H4).
 injection 1; intros; subst.
 generalize H6.
 simpl.
 rewrite (path_last H3).
 destruct (peq to to); try congruence.
 rewrite <- app_nil_end.
 tauto.
generalize (Well_formed_hierarchy.self_path_trivial Hhier H4).
injection 1; intros; subst.
generalize H6.
simpl.
rewrite (path_last H3).
destruct (peq to to); try congruence.
rewrite <- app_nil_end.
eauto.
injection H3; intros; subst.
 generalize (invariant_vars invar H).
 simpl.
 intro.
 invall.
 subst.
 esplit.
 split.
 eleft.
 eapply step_ptrshift.
 eassumption.
 reflexivity.
 constructor; simpl; trivial.
 intro.
 destruct (peq v target).
  subst.
  rewrite PTree.gss.
  rewrite PTree.gss.
  replace (x0 + 0) with x0 by omega.
  injection 1; intro; subst.
  esplit.
  split.
  reflexivity.
  simpl.
  eauto.
 rewrite PTree.gso; eauto.
 intros.
 generalize (invariant_vars invar H5).
 simpl.
 destruct 1; invall.
 rewrite PTree.gso; try congruence.
 esplit.
 split.
 eassumption.
 destruct vr; trivial.
inversion H2; subst.
  generalize (Well_formed_hierarchy.path_le Hhier H4).
  intro.
  destruct (plt from to).
    apply False_rect.
    generalize (Ple_Plt_trans H7 p1).
    apply Plt_irrefl.
    unfold paths.
    destruct (Well_formed_hierarchy.paths Hhier).
    invall.
    assert (hierarchy ! to <> None) by eauto using path_defined_to.
    assert (x ! to <> None) by eauto.
    case_eq (x ! to); try contradiction.
    intros.
    destruct (H9 _ _ H12).
    assert (hierarchy ! from <> None) by eauto using path_defined_from.
    assert (t0 ! from <> None) by eauto.
    case_eq (t0 ! from); try contradiction.
    intros.
    generalize (H14 _ _ H17).
    intro.
    destruct (H18 (k, p0)).
    generalize (H20 H4).
    intros.
    destruct l.
     contradiction.
    destruct (H18 p1).
    destruct p1.
    generalize (H22 (or_introl _ (refl_equal _))).
    intro.
    generalize (H5 _ _ H24).
    injection 1; intros; subst.
    destruct t1.
     refine (_ (non_virtual_subobject_offset_exist Hhier intro _ (Plt_succ _) H4 (accu := 0))).
     2 : eauto.
     case_eq (non_virtual_subobject_offset offsets 0 l0); try congruence.
     intros.
     destruct (invariant_vars0 _ _ H).
     invall.
     simpl in H29.
     invall.
     subst.
     destruct (invariant_objects0 _ _ H0).
     invall.
     generalize (H30 _ H0 _ _ H1 _ H31).
     intros.
     esplit.
     split.
     eleft.
     eapply step_ptrshift.
     eassumption.
     reflexivity.
    constructor; simpl; trivial.
    intro.
    destruct (peq v target).
     subst.
     rewrite PTree.gss.
     injection 1; intros; subst.
     rewrite PTree.gss.
     esplit.
     split.
      reflexivity.
     simpl.
     esplit.
     split.
      reflexivity.
     rewrite H0.
     injection 1; intro; subst.
     intros until 1.
     rewrite H31.
     injection 1; intros; subst.
     generalize H6.
     simpl.
     inversion H24; subst.
     simpl.
     rewrite (path_last H3).
     destruct (peq from from); try congruence.
     injection 1; intros; subst.
     functional inversion H27; subst.
     inversion H35; subst.
     inversion H1; subst.
     generalize (valid_array_path_last H48 H44).
     intros; subst.
     unfold relative_pointer_offset.
     rewrite H41.
     rewrite H42.
     functional inversion H43; subst.
     simpl.
     unfold subobject_offset.
     rewrite H53.
     rewrite H56.
     destruct (last_correct (path_last H3)).
     change (b :: _x ++ lf) with ((b :: _x) ++ lf).
     generalize H52.
     rewrite e0.
     rewrite app_ass.
     simpl.
     intros.
     generalize (non_virtual_subobject_offset_rewrite H26 z2).
     intro.
     rewrite (non_virtual_subobject_offset_app H54).
     rewrite H55.
     f_equal.
     omega.
     intro; repeat rewrite PTree.gso; try congruence.
     intros.
     destruct (invariant_vars0 _ _ H33).
     invall.
     esplit.
     split.
      eassumption.
     destruct vr; trivial.
   generalize (path_path1 H4).
   inversion 1; subst.
   inversion H28; subst.
   refine (_ (non_virtual_subobject_offset_exist Hhier intro _ (Plt_succ _) H28 (accu := 0))).
   2 : eauto.
   case_eq ( non_virtual_subobject_offset offsets 0 (base :: lf)); try congruence.
   intros.
   destruct (invariant_vars0 _ _ H).
   simpl in H32.
   invall.
   subst.
   destruct (invariant_objects0 _ _ H0).
   invall.
   assert (is_dynamic OP hierarchy from).
    eapply is_dynamic_virtual_base.
    eassumption.
   generalize (H35 _ H0 _ _ H1 _ H36).
   intro.
   generalize H38.
   rewrite (relative_pointer_offset_reduce_path H1).
   intro.
   generalize (invariant_vptr invar H0 H1 H32 H36 H39).
   simpl.
   replace (x3 + (x2 - x3)) with x2 by omega.
   intro.
   destruct (reduce_path_prefix offsets Hhier H3).
   invall.
   assert (DYN : is_dynamic OP hierarchy x4).
    eapply primary_path_dynamic.
    eassumption.
    2 : eassumption.
    eapply path_last.
    eassumption.
    assumption.
    auto.
   generalize (vtables_exist H41 DYN).
   case_eq (vtables real (h, reduce_path offsets p)); try congruence.
   intros.
   destruct v.
   destruct (vtables_prop H41 DYN H44).
   subst vbase_offsets0.
   functional inversion H38.
   assert ((virtual_base_offsets ofto) ! base <> None).
     eapply virtual_base_offsets_exist.
     eauto.
     eauto using path_virtual_base.
   case_eq ((virtual_base_offsets ofto) ! base); try congruence.
   intros.
   case_eq (Zsem NO (z0 - z2)).
   intros.
   esplit.
   split.
   eright.
   eleft.
   econstructor.
   econstructor.
   eright.
   eleft.
   eapply step_load.
   eassumption.
   replace (x2 + 0) with x2 by omega.
   eassumption.
   reflexivity.
   eright.
   eleft.
   econstructor.
   econstructor.
   eright.
   eleft.
   eapply step_vbase_offset.
   rewrite PTree.gss.
   reflexivity.
   eassumption.
   unfold vbase_offsets.
   unfold vboffsets.
   rewrite <- (subobject_offset_reduce_path H3).
   rewrite H51.
   rewrite H50.
   rewrite H53.
   reflexivity.
   reflexivity.
   eright.
   eleft.
   econstructor.
   econstructor.
   eright.
   eleft.
   eapply step_ptrshiftmult.
   rewrite PTree.gso; try congruence.
   rewrite PTree.gso; try congruence.
   eassumption.
   rewrite PTree.gss.
   rewrite H54.
   reflexivity.
   rewrite <- H54.
   eapply Zsem_semZ.
   reflexivity.
   eleft.
   eapply step_ptrshift.
   rewrite PTree.gss.
   replace ((z0 - z2) * 1) with (z0 - z2) by omega.
   reflexivity.
   reflexivity.
  constructor; simpl; trivial.
  intro.
  destruct (peq v0 target).
   subst v0.
   rewrite PTree.gss.
   injection 1; intros; subst vr.
   rewrite PTree.gss.
   esplit.
   split.
   reflexivity.
   simpl.
   esplit.
   split.
    reflexivity.
   rewrite H0.
   injection 1; intro; subst o0.
   intros until 1.
   inversion H57.
   inversion H1.
   generalize (valid_array_path_last H58 H62).
   intro.
   subst real0.
   rewrite H36.
   injection 1; intros; subst x3.
   generalize H6.
   simpl.
   injection 1; intros; subst h' p'.
   unfold relative_pointer_offset.
   rewrite H49.
   rewrite H50.
   unfold subobject_offset.
   rewrite H50.
   rewrite H53.
   rewrite (non_virtual_subobject_offset_rewrite H29 z0).
   f_equal.
   omega.
   rewrite PTree.gso.
   intros.
   destruct (invariant_vars invar H55).
   simpl in H56.
   invall.
   repeat (rewrite PTree.gso; try congruence).
   esplit.
   split.
   eassumption.
   destruct vr; trivial.
  assumption.
 generalize (Well_formed_hierarchy.path_le Hhier H4).
 intro.
 destruct (plt from to).
  assert (hierarchy ! from <> None) by eauto using path_defined_to.
  unfold paths.
  destruct (Well_formed_hierarchy.paths Hhier).
  invall.
  assert (x ! from <> None) by eauto.
  case_eq (x ! from); try congruence.
  intros.
  destruct (H10 _ _ H12).
  assert (hierarchy ! to <> None) by eauto using path_defined_from.
  assert (t0 ! to <> None) by eauto.
  case_eq (t0 ! to); try congruence.
  intros.
  generalize (
    H14 _ _ H17
  ).
  intros.
   pose (F :=(fun hp0 : Class.Inheritance.t * list ident =>
         let (y, _) := hp0 in
         match y with
         | Class.Inheritance.Repeated => true
         | Class.Inheritance.Shared => false
         end)).
   fold F.
  case_eq (filter F l).
   intros.
   destruct (H18 (Class.Inheritance.Repeated, p0)).
   generalize (H21 H4).
   intro.
   assert (F (Class.Inheritance.Repeated, p0) = true).
    reflexivity.
   destruct (filter_In F (Class.Inheritance.Repeated, p0) l).
   generalize (H25 (conj H22 H23)).
   rewrite H19.
   simpl.
   tauto.
  intros.
  destruct (filter_In F p2 l).
  generalize H20.
  rewrite H19.
  intro.
  destruct (H22 (or_introl _ (refl_equal _))).
  destruct (H18 p2).
  generalize (H25 H23).
  destruct p2; simpl in H24.
  destruct t1; try discriminate.
  intro.
  generalize (H5 _ H27).
  intros; subst.
  refine (_ (non_virtual_subobject_offset_exist Hhier intro _ (Plt_succ _) H27 (accu := 0))).
  2 : eauto.
  case_eq ( non_virtual_subobject_offset offsets 0 p0); try congruence.
  intros.
  generalize (invariant_vars invar H).
  simpl.
  destruct 1.
  invall.
  subst.
  destruct (invariant_objects invar H0).
  invall.
  generalize (H32 _ H0 _ _ H1 _ H33).
  intros.
  inversion H1; subst.
  inversion H4; subst.
  generalize H6.
  simpl.
  rewrite (path_last H3).
  destruct (peq to to); try congruence.
  injection 1; intros; subst.
  assert (
    valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) ar real i h' p' to
  ).
   econstructor.
   eassumption.
   assumption.
   assumption.
   assumption.
  refine (_ (relative_pointer_offset_exist Hhier intro guard _ (Plt_succ _) H42)).
  2 : eauto.
  case_eq (
relative_pointer_offset offsets (Object.class o) real ar i p'
  ); try congruence.
  intros.
  functional inversion H43; subst.
  generalize H29.
  unfold relative_pointer_offset.
  rewrite H45.
  rewrite H46.
  functional inversion H47; subst.
  replace o0 with ofto in * by congruence.
  simpl.
  unfold subobject_offset.
  rewrite H48.
  rewrite H51.
  destruct (last_correct (path_last H3)).
  revert H44.
  change (b :: _x ++ lf) with ((b :: _x) ++ lf).
  intros.
  rewrite e0 in H44, H49.
  revert H49.
  rewrite app_ass; simpl.
  rewrite (non_virtual_subobject_offset_app H44).
  rewrite (non_virtual_subobject_offset_rewrite H28).
  injection 1; intros.
  esplit.
  split.
   eleft.
   eapply step_ptrshift.
   eassumption.
   reflexivity.
  constructor; simpl; trivial.
  intro.
  destruct (peq v target).
   subst.
   rewrite PTree.gss.
   injection 1; intros; subst.
   rewrite PTree.gss.
   esplit.
   split.
    reflexivity.
   simpl.
   esplit.
   split.
    reflexivity.
   rewrite H0.
   injection 1; intro; subst.
   inversion 1; subst.
   generalize (valid_array_path_last H35 H55).
   intros; subst.
   rewrite H43.
   f_equal.
   replace x3 with oh in * by congruence.
   omega.
  rewrite PTree.gso; eauto.
  intros.
  generalize (invariant_vars invar H52).
  simpl.
  destruct 1; invall.
  rewrite PTree.gso; try congruence.
  esplit.
  split.
   eassumption.
  destruct vr; trivial.
  assert (Zpos to <> Zpos from) by congruence.
  unfold Plt, Ple in *.
  omegaContradiction.
 
generalize (invariant_vars invar H).
simpl.
intro.
invall.
subst.
destruct (invariant_objects invar H0).
invall.
generalize (H9 _ H0 _ _ H1 _ H10).
intros.
functional inversion H7; intros; subst.
generalize H7.
rewrite (relative_pointer_offset_reduce_path H1).
intro.
generalize (invariant_vptr invar H0 H1 H2 H10 H16).
simpl.
replace (x1 + (x0 - x1)) with x0 by omega.
intros.
inversion H1; subst.
destruct (reduce_path_prefix offsets Hhier H21).
invall.
assert (is_dynamic OP hierarchy x2).
 eapply primary_path_dynamic.
 eassumption.
 2 : eassumption.
 eauto using path_last.
 assumption.
 auto.
generalize (vtables_exist H22 H25).
case_eq (vtables real (h, reduce_path offsets p)); try congruence.
intros.
destruct v.
destruct (vtables_prop H22 H25 H27).
destruct (dyncast_offset_spec_reduce_path H5 H21).
destruct (Well_formed_hierarchy.dynamic_cast_dec Hhier real h p from to).
 invall.
 assert (path hierarchy to x5 real x4).
  inversion H34; eauto using path_concat.
  refine (_ (subobject_offset_exist Hhier intro guard _ (Plt_succ _) H33)).
  2 : eauto.
  case_eq (subobject_offset offsets real x5); try congruence.
  intros.
  generalize (H31 _ _ H34 _ H15 _ H35).
  intros.
  destruct (H29 to (Some (z - z2))).
  generalize (H38 H36).
  intros.
  case_eq (Zsem NO (z - z2)).
  intros.
  destruct (H3 _ _ H34).
  subst newptr.
  esplit.
  split.
  eright.
  eleft.
  econstructor.
  econstructor.
  eright.
  eleft.
  eapply step_load.
  eassumption.
  replace (x0 + 0) with x0 by omega.
  eassumption.
  reflexivity.
  eright.
  eleft.
  econstructor.
  econstructor.
  eright.
  eleft.
  eapply step_dyncast_exists.
  rewrite PTree.gss.
  reflexivity.
  eassumption.
  eassumption.
  simpl.
  reflexivity.
  reflexivity.
  eright.
  eleft.
  econstructor.
  econstructor.
  rewrite PTree.gss.
  reflexivity.
  eapply sembool_true.
  simpl.
  reflexivity.
  eright.
  eleft.
  econstructor.
  econstructor.
  eright.
  eleft.
  eapply step_dyncast_offset.
  rewrite PTree.gso; try congruence.
  rewrite PTree.gss.
  reflexivity.
  eassumption.
  eassumption.
  reflexivity.
  eleft.
  eapply step_ptrshiftmult.
  repeat (rewrite PTree.gso; try congruence).
  eassumption.
  rewrite PTree.gss.
  rewrite H40.
  reflexivity.
  rewrite <- H40.
  eapply Zsem_semZ.
  reflexivity.
 constructor; simpl; trivial.
 intro.
 destruct (peq v0 target).
  subst v0.
  rewrite PTree.gss.
  injection 1; intro; subst vr.
  rewrite PTree.gss.
  replace ((z - z2) * 1) with (z - z2) by omega.
  esplit.
  split.
  reflexivity.
  simpl.
  esplit.
  split.
   reflexivity.
  rewrite H0.
  injection 1; intro; subst o0.
  inversion 1.
  generalize (valid_array_path_last H44 H18).
  intro; subst real0.
  rewrite H10.
  injection 1; intro; subst x1.
  unfold relative_pointer_offset.
  rewrite H13.
  rewrite H14.
  rewrite H35.
  f_equal.
  omega.
 rewrite PTree.gso; eauto.
 intros.
 repeat (rewrite PTree.gso; try congruence).
 generalize (invariant_vars invar H41).
 simpl.
 destruct 1; invall.
 esplit.
 split.
 eassumption.
 destruct vr; trivial.
generalize (H32 f).
intros.
destruct (H29 to None).
generalize (H35 H33 ).
intros.
generalize (H4 f).
intros; subst newptr.
esplit.
split.
eright.
eleft.
econstructor.
econstructor.
eright.
eleft.
eapply step_load.
eassumption.
replace (x0 + 0) with x0 by omega.
eassumption.
reflexivity.
eright.
eleft.
econstructor.
econstructor.
eright.
eleft.
eapply step_dyncast_exists.
rewrite PTree.gss.
reflexivity.
eassumption.
eassumption.
simpl.
reflexivity.
reflexivity.
eright.
eleft.
econstructor.
econstructor.
rewrite PTree.gss.
reflexivity.
eapply sembool_false.
simpl.
reflexivity.
eleft.
eapply step_null.
reflexivity.
constructor; simpl; trivial.
intro.
destruct (peq v target).
 subst v.
 rewrite PTree.gss.
 injection 1; intro; subst vr.
 rewrite PTree.gss.
 esplit.
 split.
  reflexivity.
 simpl; trivial.
rewrite PTree.gso; eauto.
intros.
repeat (rewrite PTree.gso; try congruence).
generalize (invariant_vars invar H37).
simpl.
destruct 1; invall.
esplit.
split.
eassumption.
destruct vr; trivial.

destruct (invariant_objects invar H0).
invall.
assert (offsets ! (Object.class o) <> None) by congruence.
assert (offsets ! class <> None) by eauto using valid_array_path_offset.
case_eq (offsets ! class); try congruence.
intros.
assert (hierarchy ! class <> None) by eauto.
assert (
  valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) ar class i Class.Inheritance.Repeated (class :: nil) class
).
 econstructor.
 eassumption.
 assumption.
 assumption.
 eleft with (lt := nil).
 reflexivity.
 reflexivity.
 simpl.
 case_eq (hierarchy ! class); congruence.
assert (
  valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) ar class (i + j) Class.Inheritance.Repeated (class :: nil) class
).
 econstructor.
 eassumption.
 assumption.
 assumption.
eleft with (lt := nil).
 reflexivity.
 reflexivity.
 simpl.
 case_eq (hierarchy ! class); congruence.
generalize (invariant_vars invar H).
simpl.
destruct 1; invall; subst.
generalize (H20 _ H0 _ _ H15 _ H8).
functional inversion 1; subst.
replace t0 with ofto in * by congruence.
generalize H23.
unfold subobject_offset.
rewrite H22.
rewrite (virtual_base_offsets_self (intro H22)).
Transparent non_virtual_subobject_offset. simpl.
injection 1; intros; subst.
generalize (invariant_vars invar H3).
simpl.
destruct 1; invall; subst.
esplit.
split.
eleft.
eapply step_ptrshiftmult.
eassumption.
eassumption.
eassumption.
reflexivity.
constructor; simpl; trivial.
intro.
destruct (peq v target).
 subst.
 rewrite PTree.gss.
 injection 1; intro; subst.
 rewrite PTree.gss.
 esplit.
 split.
 reflexivity.
 simpl.
 esplit.
 split.
 reflexivity.
 rewrite H0.
 injection 1; intro; subst o0.
 inversion 1; subst.
  generalize (valid_array_path_last H29 H1).
  intro; subst.
  rewrite H8.
  injection 1; intros; subst.
  unfold relative_pointer_offset.
  rewrite H21.
  rewrite H22.
  rewrite H23.
  f_equal.
  replace ((i + j) * size ofto) with (i * size ofto + j * size ofto) by ring.
  omega.
rewrite PTree.gso; eauto.
intros.
repeat (rewrite PTree.gso; try congruence).
generalize (invariant_vars invar H25).
simpl.
destruct 1; invall; subst.
esplit.
split.
eassumption.
destruct vr; trivial.

Qed.

End Preservation.

End Compiler.

End SimpleCompiler.
coq2html.mll by Xavier Leroy, part of Compcert 1.7