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.

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 :=

      | 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

      | 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)

      | 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)

      | 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')


      | step_statcast : forall vars source obj ar i h p hp,
        vars ! source = Some (Value.ptr (@Value.subobject _ obj ar i h p hp)) ->
        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)

      | step_dyncast : forall vars source obj ar i h p hp,
        vars ! source = Some (Value.ptr (@Value.subobject _ obj ar i h p hp)) ->
        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)

      | 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)
    .

    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;



   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 :=

      | target_load (chunksize : Z) (ptr : var) (off : Z) (target : var)
      | target_store (chunksize : Z) (ptr : var) (off : Z) (newvalue : var)

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

      | 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)
.


      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

      | 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)

      | 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')

      | step_dyncast_exists : forall vptr cn hp vars,
        vars ! vptr = Some (Vptr cn hp) ->
        forall vtbl, vtables cn hp = Some vtbl ->
          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)

      | step_dyncast_offset : forall vptr cn hp vars,
        vars ! vptr = Some (Vptr cn hp) ->
        forall vtbl, vtables cn hp = Some vtbl ->
          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)

      | step_vbase_offset: forall vptr cn hp vars,
        vars ! vptr = Some (Vptr cn hp) ->
        forall vtbl, vtables cn hp = Some vtbl ->
          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)

      | 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)

      | 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)

      | 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.

      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 :=
        match s' with

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

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

        | 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

        | 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

        | 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)))
            )
          )

        | 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

          | 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.
      



      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'.

      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'.

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).

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).

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.

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}.

Corollary dyncast_offset_strong : forall real hp, {
  dyo | forall x y, dyo x = Some y <-> dyncast_offset_spec real hp x y
}.


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.

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)).

Opaque vtables.
   
  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).

  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).

Lemma match_values_align : forall v w,
match_values s v w ->
typ_align PF
( (Value.type_of v))
= memval_align PF palign w
.
  
Lemma match_values_size : forall v w,
match_values s v w ->
typ_size PF
( (Value.type_of v))
= memval_size PF psize w
.
 
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).

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)
.

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.

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.

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.

  Theorem preservation : exists t', clos_trans _ (step vtables (MEM := MEM)) t t' /\ invariant s' t'.

End Preservation.

End Compiler.

End SimpleCompiler.