Module Interm2Target

Require Import Coqlib.
Require Import Tactics.
Require Import LibLists.
Require Import LibMaps.
Require Import Cplusconcepts.
Require Import CplusWf.
Require Import LayoutConstraints.
Require Import Dynamic.
Require Import DynamicWf.
Require Import CPP.
Require Import Interm.
Require Import IntermSetDynType.
Require Import IntermSetDynTypeWf.
Require Memory.
Require Import Events.
Require Import Smallstep.
Require Import Target.
Require Import Vtables.
Require Import CompileSetDynType.
Require Import Eqdep_dec.
Open Scope Z_scope.
Load Param.

Function oapply (A B : Type) (f : A -> B) (oa : option A) {struct oa} : option B :=
  match oa with
    | None => None
    | Some a => Some (f a)
  end.

Notation OldVar := (xO) (only parsing).
Notation NewVar := (xI) (only parsing).

Section Common.

  Variable A : ATOM.t.

  Variable nativeop : Type.

  Variable prog : Interm.program A nativeop.

  Notation hierarchy := (Interm.hierarchy prog) (only parsing).

  Hypothesis Hhier : Well_formed_hierarchy.prop hierarchy.

Notation is_dynamic := (Dynamic.is_dynamic).

Variable COP : CPPOPTIM A.

Variable vop' : valop' A Z.

Hypothesis vop'_pos : forall k t, 0 < vop' k t.

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

      
      Hypothesis intro : forall ci o, offsets ! ci = Some o -> class_level_prop (OP COP) (PF vop'_pos) offsets hierarchy ci o.
      
      Hypothesis guard : forall ci, offsets ! ci <> None -> hierarchy ! ci <> None.

      Hypothesis exis: 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 COP) offsets hierarchy ci oc.

      Variable mblock : Type.
   
        Notation GARBAGE := (skip _ _) (only parsing).
        
        Notation paths := (let (T, _) := Well_formed_hierarchy.paths Hhier in T) (only parsing).

        Notation STATIC := (xO) (only parsing).
        Notation NONSTATIC := (xI) (only parsing).

        Function compile_method_name (cn : ident) (ms : MethodSignature.t A) : ident :=
          match hierarchy ! cn with
            | None => xH
            | Some c =>
              match Method.find ms (Class.methods c) with
                | None => xH
                | Some m =>
                  match Method.kind m with
                    | Method.concrete k => NONSTATIC k
                    | _ => xH
                  end
              end
          end.

Function compile_callkind (ct : callkind A) : ident :=
  match ct with
    | Interm.Static id => STATIC id
    | NonVirtual id ms => compile_method_name id ms
  end.

Function repeated_criterion (hp : Class.Inheritance.t * list ident) : bool :=
  match hp with
    | (Class.Inheritance.Repeated, _) => true
    | _ => false
  end.
  
Function compile_statcast (from to : ident) (source target : var) : Target.stmt nativeop (romty A) :=
  match peq from to with
    | left _ => move _ _ (OldVar source) (OldVar 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 repeated_criterion l with
                    | nil => GARBAGE
                    | (_, p) :: _ =>
                      match non_virtual_subobject_offset offsets 0 p with
                        | None => GARBAGE
                        | Some off => ptrshift _ _ (OldVar source) (0 - off) (OldVar 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 => ptrshift _ _ (OldVar source) off (OldVar target)
                  end
                | Some ((Class.Inheritance.Shared, b :: p) :: _) =>
                  match non_virtual_subobject_offset offsets 0 (b :: p) with
                    | None => GARBAGE
                    | Some off => seq
                      (Target.load _ _ (vop' Size (tyVptr _)) (OldVar source) 0 (NewVar xH))
                      (seq
                        (romop _ (Some (NewVar xH)) (vbase_offset (romty := romty A) from b) (NewVar (xO xH)))
                        (seq
                          (ptrshiftmult _ _ (OldVar source) (NewVar (xO xH)) 1 (NewVar (xH)))
                          (ptrshift _ _ (NewVar (xH)) off (OldVar target))
                        )
                      )
                  end
                | _ => GARBAGE
              end
          end
      end
  end.

Function compile_invoke (use_thunks : bool) (source : var) (class : ident) (ms : MethodSignature.t A) (args : list var) (retval : option var) : Target.stmt nativeop (romty A) :=
  if use_thunks
    then
      thunkcall (romty := romty A) _ (OldVar source) class ms (map OldVar args) (oapply OldVar retval)
    else
      seq
      (Target.load _ _ (vop' Size (tyVptr _)) (OldVar source) 0 (NewVar xH)) (seq
        (romop _ (Some (NewVar xH)) (Target.dispatch_offset (romty := romty A) class ms) (NewVar (xI xH)))
        (seq
          (ptrshiftmult _ _ (OldVar source) (NewVar (xI xH)) 1 (NewVar (xI xH)))
          (seq
            (romop _ (Some (NewVar xH)) (Target.dispatch_function (romty := romty A) class ms) (NewVar xH))
            (call _ _ Dynamic (NewVar xH) (NewVar (xI xH) :: map OldVar args) (oapply OldVar retval))
          )
        )
      ).
      
Function compile_pathop (path_oper : path_operation) (source : option var) (target : var) : Target.stmt nativeop (romty A) :=
  match path_oper with
    | rootpath cn =>
      if is_dynamic_dec Hhier cn
        then
          (romop _ None (Target.initVTT (romty := romty A) cn) (OldVar target))
        else
          (null _ _ (OldVar target))

    | addbase cn h b =>
      if is_dynamic_dec Hhier b
        then
          (romop _ (oapply OldVar source) (Target.subVTT (romty := romty A) cn (h, b)) (OldVar target))
        else
          (null _ _ (OldVar target))
          
  end.

Variable use_thunks : Interm.stmt A nativeop -> bool.

        Function compile (s : Interm.stmt A nativeop) {struct s} : Target.stmt nativeop (romty A) :=
          match s with
            | Interm.skip => skip _ _
            | Interm.seq s1 s2 => seq (compile s1) (compile s2)
            | Interm.test var ifso ifnot => test (OldVar var) (compile ifso) (compile ifnot)
            | Interm.block None s' => block None (compile s')
            | Interm.block (Some (var, (cn, ncells))) s' =>
              match offsets ! cn with
                | None => GARBAGE
                | Some o => block (Some (OldVar var, ncells * size o)) (compile s')
              end
            | Interm.exit n => exit _ _ n
            | Interm.loop s' => loop (compile s')
            | Interm.native op args ores => native _ op (map OldVar args) (oapply OldVar ores)
            | Interm.move src tgt => move _ _ (OldVar src) (OldVar tgt)
            | Interm.ret ores => ret _ _ (oapply OldVar ores)
            | Interm.call ck vargs ores =>
              call _ _ Static (compile_callkind ck) (map OldVar vargs) (oapply OldVar ores)



            | Interm.null _ target => (null _ _ (OldVar target))
              
            | Interm.ptreq ptr1 ptr2 target => ptreq _ _ (OldVar ptr1) (OldVar ptr2) (OldVar target)

            | Interm.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 => Target.load _ _ (vop' Size (valtype_of_typ ty)) (OldVar source) fo (OldVar target)
                        | _ => (ptrshift _ _ (OldVar source) fo (OldVar target))
                      end
                  end
              end

            | Interm.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 =>
                          Target.store _ _ (vop' Size (valtype_of_typ ty)) (OldVar source) fo (OldVar newvalue)
                        | _ => GARBAGE
                      end
                  end
              end

            | statcast from to source target => compile_statcast from to source target


            | Interm.dyncast from to source target =>
              seq
              (Target.load _ _ (vop' Size (tyVptr _)) (OldVar source) 0 (NewVar xH))
              (seq
                (romop _ (Some (NewVar xH)) (Target.dyncast_exists (romty := romty A) to) (NewVar (xI xH)))
                (test (NewVar (xI xH))
                  (seq
                    (romop _ (Some (NewVar xH)) (Target.dyncast_offset (romty := romty A) to) (NewVar (xI xH)))
                    (ptrshiftmult _ _ (OldVar source) (NewVar (xI xH)) 1 (OldVar target))
                  )
                  (null _ _ (OldVar target))
                )
              )

            | arrayindex class index source target =>
              match offsets ! class with
                | None => GARBAGE
                | Some o => ptrshiftmult _ _ (OldVar source) (OldVar index) (size o) (OldVar target)
              end
              
            | invoke source class ms args retval =>
              compile_invoke (use_thunks s) source class ms args retval

            | pathop p osrc tgt =>
              compile_pathop p osrc tgt

            | setdyntype ismostderived class source path =>
              compile_set_dynamic_type Hhier vop' offsets nativeop ( source) ( path) xH class ismostderived

            | casttobase source cn k b target =>
              match offsets ! cn with
                | None => GARBAGE
                | Some o =>
                  match k with
                    | Class.Inheritance.Repeated =>
                      match (non_virtual_direct_base_offsets o) ! b with
                        | None => GARBAGE
                        | Some off => ptrshift _ _ (OldVar source) off (OldVar target)
                      end
                    | _ =>
                      match (virtual_base_offsets o) ! b with
                        | None => GARBAGE
                        | Some off => ptrshift _ _ (OldVar source) off (OldVar target)
                      end
                  end
              end
              
      end.

Function compile_method_body (mb : method_body A nativeop) : Target.func nativeop (romty A) :=
  match mb with
    | Method_body mthis margs mcode =>
      Func (OldVar mthis :: map OldVar margs) (compile mcode)
  end.

Definition f_compile_method (i : ident) (mb : method_body A nativeop) : option (ident * Target.func nativeop (romty A)) := Some (NONSTATIC i, compile_method_body mb).

Function compile_static_fun (sf : static_fun A nativeop) : Target.func nativeop (romty A) :=
  match sf with
    | Static_fun sargs scode => Func (map OldVar sargs) (compile scode)
  end.

Definition f_compile_static (i : ident) (sf : static_fun A nativeop) : option (ident * Target.func nativeop (romty A)) := Some (STATIC i, compile_static_fun sf).

Definition prog' : Target.program nativeop (romty A) :=
  Target.Program
  (ptree_to_ptree f_compile_static (Interm.statics prog) (ptree_to_ptree f_compile_method (Interm.methods prog) (PTree.empty _)))
  (compile (Interm.main prog))
  (rom := rom Hhier intro guard exis compile_method_name)
  (vtable_access_wf Hhier intro guard)
  .


        Variables memblocks memvalues : Type.

        Variable memop : Memory.op (val A (romty A) mblock) memblocks memvalues mblock.

        Hypothesis memprop : Memory.prop memop (valop (romty A) mblock vop').

        Section Match_values.

          Variable global : Globals.t A.
          Variable objmap : PTree.t mblock.

          Inductive match_values : Interm.value A -> Target.val A (romty A) mblock -> Prop
  :=
          | match_values_atom : forall ty va,
            match_values (Interm.Val (Value.atom ty va)) (Target.Atom _ _ va)

          | match_values_pvtt : forall from h p,
            forall v,
              (forall to, path hierarchy to p from h -> is_dynamic hierarchy to -> v = Target.VTTptr (romty := romty A) _ _ (from, (h, p))) ->
              match_values (Interm.Path _ from h p) v
            
          | match_values_null : forall cn,
            match_values (Interm.Val (Value.ptr (Value.null _ cn))) (Target.Ptr _ _ None)

          | match_values_ptr : forall obj,
            Plt obj (Globals.next_object global) ->
            forall ar i h p v,
              (forall o, (Globals.heap global) ! obj = Some o ->
                forall ato to,
                  valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) ar ato i h p to ->
                  exists bl, objmap ! obj = Some bl /\
                    exists off, relative_pointer_offset offsets (Object.class o) ato ar i p = Some off /\
                      v = (Some (bl, off)))
              ->
              forall hp,
                match_values (Interm.Val (Value.ptr (Value.subobject obj ar i h p hp))) (Target.Ptr _ _ v)
              .

          Definition match_values' (_ _ : True) := match_values.

        End Match_values.

        Lemma match_values_alloc :
          forall global cn cells obj global',
          Globals.new global cn cells = (obj, global') ->
          forall objmap mb objmap',
            PTree.set obj mb objmap = objmap' ->
              forall v1 v2, match_values global objmap v1 v2 ->
                match_values global' objmap' v1 v2.

        Lemma match_values_free :
          forall global obj global',
            Globals.remove global obj = global' ->
            forall objmap objmap',
              PTree.remove obj objmap = objmap' ->
              forall v1 v2, match_values global objmap v1 v2 ->
                match_values global' objmap' v1 v2.

        Lemma match_values_update : forall global fd global',
          Globals.update global fd = global' ->
          forall objmap v1 v2, match_values global objmap v1 v2 ->
            match_values global' objmap v1 v2.

        Section Match_frames.

          Variable global : Globals.t A.
          Variable objmap : PTree.t mblock.

          Inductive match_frames : list ident -> list ident -> Interm.frame A nativeop -> Target.frame A nativeop (romty A) mblock -> Prop :=
          | match_frames_block : forall bo bo' lo lo',
            match bo with
              | None => bo' = None /\ lo = lo'
              | Some o => Plt o (Globals.next_object global) /\ lo = o :: lo' /\ exists o', objmap ! o = Some o' /\ bo' = Some o'
            end ->
            forall stl stl', stl' = map compile stl ->
              match_frames lo lo' (Interm.Block bo stl) (Target.Block _ bo' stl')

          | match_frames_callframe : forall stl stl',
            stl' = map compile stl ->
            forall vars vars',
              (forall i v, vars ! i = Some v -> exists v', vars' ! (OldVar i) = Some v' /\ match_values global objmap v v') ->
              forall lo fret fret',
                fret' = oapply OldVar fret ->
                match_frames lo lo (Interm.Callframe stl vars fret) (Target.Callframe stl' vars' fret').

        Lemma match_frames_not_a_member : forall q q' u v,
          match_frames q q' u v ->
          forall p, (In p q -> False) -> (In p q' -> False).

        End Match_frames.

        Lemma match_frames_alloc :
          forall global cn cells obj global',
          Globals.new global cn cells = (obj, global') ->
          forall objmap mb objmap',
            PTree.set obj mb objmap = objmap' ->
              forall lo lo' v1 v2, match_frames global objmap lo lo' v1 v2 ->
                match_frames global' objmap' lo lo' v1 v2.

        Lemma match_frames_free :
          forall global obj global',
            Globals.remove global obj = global' ->
            forall objmap objmap',
              PTree.remove obj objmap = objmap' ->
              forall lo,
                (In obj lo -> False) ->
                forall lo' v1 v2, match_frames global objmap lo lo' v1 v2 ->
                  match_frames global' objmap' lo lo' v1 v2.

        Lemma match_frames_update : forall global fd global',
          Globals.update global fd = global' ->
          forall objmap lo lo' v1 v2, match_frames global objmap lo lo' v1 v2 ->
                  match_frames global' objmap lo lo' v1 v2.
              
        Section Bilist.
          
          Variables Q U V : Type.

          Section BDef.
            
          Variable P : Q -> Q -> U -> V -> Type.

          Inductive bilist : Q -> list U -> list V -> Prop :=
          | bilist_nil : forall q, bilist q nil nil
          | bilist_cons : forall q u v q',
            P q q' u v ->
            forall lu lv, bilist q' lu lv ->
              bilist q (u :: lu) (v :: lv)
              .

        End BDef.

        Variables P P' : Q -> Q -> U -> V -> Type.
        Variable R : Q -> Type.
        Hypothesis HimpP : forall q q' u v, P q q' u v -> R q -> R q'.
        Hypothesis Himp : forall q, R q -> forall q' u v, P q q' u v -> P' q q' u v.

        Lemma bilist_imp : forall lo, R lo -> forall lu lv, bilist P lo lu lv -> bilist P' lo lu lv.

        End Bilist.


        Section State.
          
          Variable st : Interm.state A nativeop.
          Variable st' : Target.state A nativeop (romty A) mblock memblocks memvalues.

          Section Invariant'.

            Variable objmap : PTree.t mblock.
            Variable lo : list ident.
          
              Record invariant' : Type := invariant'_intro {
                invariant_current : Target.current st' = compile (Interm.current st);
                invariant_further : Target.further st' = map compile (Interm.further st);
                invariant_vars : forall v vr, (Interm.vars st) ! v = Some vr -> exists vs, (Target.vars st') ! (OldVar v) = Some vs /\ match_values (Interm.globals (Interm.global st)) objmap vr vs
                  ;
                invariant_stack : bilist (match_frames (Interm.globals (Interm.global st)) objmap) lo (Interm.stack st) (Target.stack st');
                invariant_stack_lt : forall i, In i lo -> Plt i (Globals.next_object (Interm.globals (Interm.global st)));
                invariant_stack_no_dup : NoDup lo;
                invariant_object_offsets : forall obj o,
                  (Globals.heap (Interm.globals (Interm.global st))) ! obj = Some o ->
                  offsets ! (Object.class o) <> None
                  ;
                invariant_objects : forall obj,
                  (Globals.heap (Interm.globals (Interm.global st))) ! obj <> None ->
                  objmap ! obj <> None
                  ;
                invariant_fields_guard : forall obj ar i h p fs, Globals.get_field (Globals.field_values (Interm.globals (Interm.global st))) (obj, ar, i, (h, p), fs) <> None ->
                  forall ty, FieldSignature.type fs = FieldSignature.Scalar ty ->
                    Plt obj (Globals.next_object (Interm.globals (Interm.global st)))
                    ;
                invariant_fields : forall obj o,
                  (Globals.heap (Interm.globals (Interm.global st))) ! 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, Globals.get_field (Globals.field_values (Interm.globals (Interm.global st))) (obj, ar, i, (h, p), fs) = Some vr ->
                            forall oh, objmap ! 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, Memory.load memop (vop' Size (valtype_of_typ ty)) (Target.mblocks (Target.memory st')) (Target.mvalues (Target.memory st')) (oh, off + foff) = Some vs /\ match_values (Interm.globals (Interm.global st)) objmap (Interm.Val vr) vs
                                      ;
                invariant_dynamic_type_guard : forall obj ar i h p ,
                  assoc (@pointer_eq_dec _) (obj, (ar, i, (h, p))) (Interm.dynamic_type (Interm.global st)) <> None ->
                  Plt obj (Globals.next_object (Interm.globals (Interm.global st)))
                  ;
                invariant_dynamic_type : forall obj o,
                  (Globals.heap (Interm.globals (Interm.global st))) ! 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 hierarchy from ->
                    forall h0 p0 h1 p1,
                      assoc (@pointer_eq_dec _) (obj, (ar, i, (h, p))) (Interm.dynamic_type (Interm.global st)) = Some ((h0, p0), (h1, p1)) ->
                  exists through,
                    path hierarchy through p0 real h0 /\
                    path hierarchy from p1 through h1 /\
                    (h, p) = concat (h0, p0) (h1, p1)
                    ;
                invariant_vptr : forall obj o,
                  (Globals.heap (Interm.globals (Interm.global st))) ! 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 hierarchy from ->
                    forall h0 p0 h1 p1,
                      assoc (@pointer_eq_dec _) (obj, (ar, i, (h, p))) (Interm.dynamic_type (Interm.global st)) = Some ((h0, p0), (h1, p1)) ->
                      forall oh, objmap ! obj = Some oh ->
                        forall off, relative_pointer_offset offsets (Object.class o) real ar i p = Some off ->
                          Memory.load memop (vop' Size (tyVptr _)) (Target.mblocks (Target.memory st')) (Target.mvalues (Target.memory st')) (oh, off) = Some (Vptr (romty := romty A) _ _ (real, (h0, p0), (h1, reduce_path offsets p1)))
                            ;
                invariant_disjoint_objects : forall obj1 obj2,
                  obj1 <> obj2 ->
                  forall o1,
                    objmap ! obj1 = Some o1 ->
                    forall o2,
                      objmap ! obj2 = Some o2 ->
                      o1 <> o2
                      ;
                invariant_valid_blocks : forall obj of, objmap ! obj = Some of ->
                  Memory.valid_block memop (Target.mblocks (Target.memory st')) of
              ;
              invariant_object_sizes : forall obj o,
                (Globals.heap (Interm.globals (Interm.global st))) ! obj = Some o ->
                forall of, offsets ! (Object.class o) = Some of ->
                  forall ob, objmap ! obj = Some ob ->
                    Object.arraysize o * size of <= Memory.block_size memop (Target.mblocks (Target.memory st')) ob
              }.

            End Invariant'.

            Inductive invariant : Prop :=
              | invariant_intro (objmap : _) (lo : _) (_ : invariant' objmap lo).

    End State.

    Variable sem : semparam A nativeop.

    Variable tsp : targetsemparam.

    Theorem init : forall st, Interm.initial_state prog st ->
      exists st1, Target.initial_state memop prog' st1 /\
        exists st2,
          star _ (Target.step (sem := sem) vop' memop prog' tsp)
          st1 E0 st2 /\
          invariant st st2.

    Theorem fin : forall st1 st2 r,
      invariant st1 st2 ->
      Interm.final_state (sem := sem) st1 r ->
      exists st2',
        star _ (Target.step (sem := sem) vop' memop prog' tsp)
        st2 E0 st2' /\
        Target.final_state st2' r.
      
     Hypothesis Htsp_thunks : allow_thunk_call tsp = false ->
       forall s, use_thunks s = false.

     Lemma Htsp_thunks' : forall s, use_thunks s = true ->
       allow_thunk_call tsp = true.

     Hypothesis Htsp_function_pointers : allow_function_pointers tsp = false ->
       forall s, use_thunks s = true.

     Lemma Htsp_function_pointers' : forall s, use_thunks s = false ->
       allow_function_pointers tsp = true.

     Hypothesis is_empty_dec : forall cn, {is_empty COP hierarchy cn} + {~ is_empty COP hierarchy cn}.

     Section Step.

     Variable st1 : Interm.state A nativeop.
     Variable t : trace (evtr sem).
     Variable st1' : Interm.state A nativeop.

     Hypothesis Hstep : Interm.step prog (is_primary_path offsets) st1 t st1'.

     Variable st2 : Target.state A nativeop (romty A) mblock memblocks memvalues.

     Hypothesis Hinv : invariant st1 st2.

     Notation goal := (exists st2',
       plus _ (step (sem := sem) vop' memop prog' tsp) st2 t st2' /\
       invariant st1' st2') (only parsing).

     Lemma preservation_skip : forall stm stl vars stack global,
       Interm.State (Interm.skip A nativeop) (stm :: stl) vars stack global =
       st1 -> goal.

     Lemma preservation_seq : forall s1 s2 stl vars stack global,
       Interm.State (Interm.seq s1 s2) stl vars stack global = st1 ->
       goal.

     Lemma preservation_move : forall source target stl vars stack global,
       Interm.State (Interm.move A nativeop source target) stl vars stack global = st1 ->
       goal.

     Lemma preservation_test : forall varb ifso ifnot stl vars stack global,
       Interm.State (Interm.test varb ifso ifnot) stl vars stack global = st1 ->
       goal.

     Lemma preservation_loop : forall stmt stl vars stack global,
       Interm.State (Interm.loop stmt) stl vars stack global = st1 ->
       goal.

     Lemma preservation_block_None : forall stm stl vars stack global,
       Interm.State (Interm.block None stm) stl vars stack global = st1 ->
       goal.

     Lemma preservation_block_Some : forall c cn sz stm stl vars stack gl dt,
       Interm.State (Interm.block (Some (c, (cn, sz))) stm) stl vars stack (Global gl dt) = st1 ->
       goal.

Lemma preservation_exit_O : forall stl vars stack global,
  Interm.State (Interm.exit A nativeop 0) stl vars stack global = st1 ->
  goal.

Lemma preservation_exit_S : forall stm stl vars oobj stl' stack gl dt,
  Interm.State stm stl vars (Interm.Block oobj stl' :: stack)
         (Global gl dt) = st1 ->
  forall stm', Interm.exit_succ stm = Some stm' ->

         goal.

Lemma preservation_return : forall ov stl vars stl' vars' orv stack global,
  Interm.State (Interm.ret A nativeop ov) stl vars
  (Interm.Callframe stl' vars' orv :: stack) global = st1
  -> goal.

Section Set_params.
  Variable vars : PTree.t (Interm.value A).
  Variable gl : Globals.t A.
  Variable objmap : PTree.t mblock.

  Variable vars0 : PTree.t (val A (romty A) mblock).
  
  Hypothesis Hvars: forall (v : positive) (vr : value A),
    vars ! v = Some vr ->
    exists vs : val A (romty A) mblock,
      vars0 ! (v~0) = Some vs /\
      match_values gl objmap vr vs
      .

  Lemma set_params_exist : forall l vargs,
    map (@Some _) l = map (fun v => vars ! v) vargs ->
    exists l',
      map (@Some _) l' = map (fun v => vars0 ! v) (map xO vargs) /\
      forall lp (v : positive) (vr : value A),
        (Interm.set_params l lp) ! v = Some vr ->
        exists vs : val A (romty A) mblock,
          (Target.set_params l' (map xO lp)) ! (v~0) = Some vs /\
          match_values gl objmap vr vs
      .

Lemma map_atom : forall args source,
  map
  (fun a : sigT (ATOM.val (t:=A)) =>
    let (ty, va) := a in Some (Val (Value.atom ty va))) args =
  map (fun v : positive => vars ! v) (source) ->
  map (fun a : sigT (ATOM.val (t := A)) => let (ty, va) := a in Some (Target.Atom (romty A) _ va)) args =
  map (fun v => PTree.get v vars0) (map xO source).

End Set_params.

Lemma preservation_call : forall kind vargs oret stl vars stack global,
  Interm.State (Interm.call nativeop kind vargs oret) stl vars stack global = st1 ->
  goal.
  
Lemma preservation_native : forall op source target stl vars stack global,
  Interm.State (Interm.native A op source target) stl vars stack global = st1->
  goal.

Lemma preservation_null : forall class target stl vars stack global,
  Interm.State (Interm.null A nativeop class target) stl vars stack global = st1 ->
  goal.

Lemma preservation_ptreq : forall v1 v2 target stl vars stack global dt,
  Interm.State (Interm.ptreq A nativeop v1 v2 target) stl vars stack (Global global dt) = st1 ->
  goal.

  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 preservation_getfield : forall class fs source target stl vars stack global dt,
  Interm.State (getfield nativeop class fs source target) stl vars stack (Global global dt) = st1 ->
  goal.

Lemma preservation_putfield : forall class fs source newvalue stl vars stack global dt,
  Interm.State (putfield nativeop class fs source newvalue) stl vars stack (Global global dt) = st1 ->
  goal.

Lemma primary_vtable_access_le : forall l, is_primary_path offsets l = true -> forall x2 x3, l = x2 :: x3 -> forall from, last l = Some from ->
  vtable_access_le (romty:=romty A)
  (Target.vtable_access_sharing (Target.rom prog')) from x2
.

Lemma preservation_static_cast : forall from to source target stl vars stack global dt,
  Interm.State (statcast A nativeop from to source target) stl vars stack (Global global dt) = st1 ->
  goal.

Lemma preservation_dynamic_cast : forall from to source target stl vars stack global dt,
  Interm.State (Interm.dyncast A nativeop from to source target) stl vars stack (Global global dt) = st1 ->
  goal.

Lemma preservation_invoke : forall source from ms vargs vres stl vars0 stack global dt,
Interm.State (invoke nativeop source from ms vargs vres) stl vars0
          stack (Global global dt) = st1
->
  goal.

Lemma preservation_array_index : forall class index source target stl vars stack global dt,
  Interm.State (arrayindex A nativeop class index source target) stl vars stack (Global global dt) = st1 ->
  goal.

Lemma is_dynamic_defined : forall d, is_dynamic hierarchy d -> hierarchy ! d <> None.
  
Lemma preservation_rootpath : forall cn ovar target stl vars stack global,
  Interm.State (pathop A nativeop (rootpath cn) ovar target) stl vars stack global = st1 ->
  goal.

Lemma preservation_addbase : forall i t0 cn ovar target stl vars stack global,
  Interm.State (pathop A nativeop (addbase i t0 cn) ovar target) stl vars stack global = st1 ->
  goal.

Lemma list_concat_prefix_left : forall (U : Type) (lu1l lu1r lu2l lu2r : list U),
  lu1l ++ lu1r = lu2l ++ lu2r ->
  (length lu1l <= length lu2l)%nat ->
  exists l, lu2l = lu1l ++ l /\ lu1r = l ++ lu2r.

Lemma reduce_non_primary_path : forall hyperreal to0 h0 p0,
  path hierarchy to0 p0 hyperreal h0 ->
  forall to1 h1 p1, path hierarchy to1 p1 hyperreal h1 -> (
    forall h' p', path hierarchy to1 p' to0 h' ->
      (h1, p1) <> concat (h0, p0) (h', p')
  ) -> (
    (forall p'', is_primary_path offsets (to1 :: p'') = true -> (h0, p0) <> concat (h1, p1) (Class.Inheritance.Repeated, to1 :: p''))
  ) ->
  forall to2 h' p', path hierarchy to2 p' to0 h' ->
    forall h2 p2, (h2, p2) = concat (h0, p0) (h', p') ->
      reduce_path offsets p1 <> reduce_path offsets p2.


Lemma preservation_set_dynamic_type : forall ismostderived_flag from vptr vpath stl vars stack gl dt,
  Interm.State
  (setdyntype A nativeop ismostderived_flag from vptr vpath) stl vars stack (Global gl dt) = st1 ->
  goal.

Lemma preservation_casttobase_repeated : forall vptr from b target stl vars stack global dt,
  Interm.State
  (casttobase A nativeop vptr from Class.Inheritance.Repeated b target)
  stl vars stack (Global global dt) = st1 ->
  goal.

Lemma preservation_casttobase_shared : forall vptr from b target stl vars stack global dt,
  Interm.State
  (casttobase A nativeop vptr from Class.Inheritance.Shared b target)
  stl vars stack (Global global dt) = st1 ->
  goal.

  

     Theorem preservation : goal.

End Step.

Corollary simulation : forall beh,
  not_wrong beh ->
  program_behaves (Interm.step prog (sem := sem) (is_primary_path offsets)) (Interm.initial_state prog) (@Interm.final_state A nativeop sem) beh ->
  program_behaves (Target.step (sem:=sem) vop' memop prog' tsp) (Target.initial_state memop prog') (@Target.final_state A (nativeop) (sem) (romty A) mblock memblocks memvalues) beh.

End Common.

Check simulation.