Module Cppsem2IntermAux

Require Import Coqlib.
Require Import Cplusconcepts.
Require Import CplusWf.
Require Import LibLists.
Require Import Tactics.
Require Import LibMaps.
Require Import Relations.
Require Import Dynamic.
Require Import Events.
Require Import Smallstep.
Require Import Cppsem.
Require Import Interm.
Require Import IntermSetDynType.
Require Import IntermSetDynTypeWf.
Require Import Eqdep_dec.
Require Import Invariant.
Require Import Preservation.
Require Import ForLoop.
Require Import SubobjectOrdering.
Require Import ConstrSubobjectOrdering.
Require Import Dyntype.
Require Import Constrorder.
Require Import ScalarFields.
Load Param.
Open Scope Z_scope.

Section Compiler.

Variable A : ATOM.t.

Variable nativeop : Type.

Notation GARBAGE := (Interm.skip A nativeop) (only parsing).

Inductive newvar : Type :=
| Oldvar (_ : var)
| Newvar (_ : positive)
.


Inductive newstatic : Type :=
| Newstatic (_ : ident)
| Oldstatic (_ : ident)
.


Variable sem : semparam A nativeop.

Variable prog : Program.t A nativeop.

Variable compile_var : newvar -> var.
Hypothesis compile_var_inj : forall v1 v2, compile_var v1 = compile_var v2 -> v1 = v2.

Lemma compile_var_other : forall v1 v2, v1 <> v2 -> compile_var v1 <> compile_var v2.

Variable compile_static : newstatic -> ident.


Inductive constrdestr : Type :=
| StaticConstructor (_ : list (Typ.t A))
| StaticDestructor
.

Variable compile_constrdestr : ident -> constrdestr -> bool -> ident.

Definition compile_initcell (cn : ident) (blockvar index newobj newpath : var) (i : Z) (init : Interm.stmt A nativeop) :=
  let (ty, va) := Zsem sem i in
    seq
    (Interm.native _ (CONST sem va) nil (Some (compile_var (Newvar index))))
    (seq
      (Interm.arrayindex _ _ cn (compile_var (Newvar index)) (compile_var (Newvar blockvar)) (compile_var (Newvar newobj)))
      (seq
        (Interm.pathop _ _ (Interm.rootpath cn) None (compile_var (Newvar newpath)))
        init
      )
    ).

Definition compile_constrarray_aux (cn : ident) (sz : Z) (blockvar index newobj newpath : var) (instr : Z -> Interm.stmt A nativeop) (q : Interm.stmt A nativeop) :=
  forup q
  (fun j => seq (compile_initcell cn blockvar index newobj newpath j (instr j))) sz
.

Definition compile_destrarray_aux (cn : ident) (blockvar index newobj newpath : var) (q : Interm.stmt A nativeop) :=
  fordown q
  (fun j => seq
    (compile_initcell cn blockvar index newobj newpath j
      (call _ (Static _ (compile_static (Newstatic (compile_constrdestr cn (StaticDestructor ) true)))) (compile_var (Newvar newobj) :: compile_var (Newvar newpath) :: nil) None)
    )
  ) (-1).

Definition compile_destrarray cn blockvar maxvar :=
  let index := Psucc maxvar in
    let newobj := Psucc index in
      let newpath := Psucc newobj in
        compile_destrarray_aux cn blockvar index newobj newpath.
  
Fixpoint compile_discard (n : nat) (blocks : list (option (var * var * (ident * Z)))) maxvar (q : Interm.stmt A nativeop) {struct n} : Interm.stmt A nativeop :=
  match n with
    | O => q
    | S n' =>
      match blocks with
        | nil => q
        | None :: blocks' => seq (skip _ _) (compile_discard n' blocks' maxvar q)
        | Some (blockvar, maxvar', (cn, sz)) :: blocks' =>
          seq (
            block None
            (compile_destrarray cn blockvar maxvar (exit _ _ 1%nat) (sz-1))
          )
          (compile_discard n' blocks' maxvar' q)
      end
  end.

Record context : Type := Context {
  maxvar : positive;
  curobjpathfield : option ((positive * positive * bool) * option (ident * FieldSignature.t A));
  blocks : list (option (var * var * (ident * Z)));
  further_blocks : nat;
  is_destructor_body : bool
}.

Hypothesis hierarchy_wf : Well_formed_hierarchy.prop (Program.hierarchy prog).

Fixpoint compile (c : context) (s : Cppsem.stmt A nativeop) {struct s} : Interm.stmt A nativeop :=
  match s with
    | Sskip => skip _ _
    | Sif var iftrue iffalse =>
      test (compile_var (Oldvar var)) (compile c iftrue) (compile c iffalse)
    | Sloop st => loop (compile c st)
    | Sseq s1 s2 => seq (compile c s1) (compile c s2)
    | Sblock localstruct initializers body =>
      match localstruct with
        | None => block None (
          let bl' := (None :: blocks c) in
            seq
            (compile (Context (maxvar c) (curobjpathfield c) bl' (further_blocks c) (is_destructor_body c)) body)
            (
              (compile_discard 1%nat bl' (maxvar c) (Interm.exit _ _ 1%nat))
            )
        )
        | Some (v, cn, sz) =>
          let blockvar := Psucc (maxvar c) in
            let midvar := Psucc blockvar in
              let blockvar' := Psucc midvar in
              block
              (Some (compile_var (Newvar blockvar), (cn, sz)))
              (seq
                (seq
                  (Interm.move _ _ (compile_var (Newvar blockvar)) (compile_var (Oldvar v)))
                  (Interm.move _ _ (compile_var (Newvar blockvar)) (compile_var (Newvar blockvar')))
                )
                (
                  let index := Psucc blockvar' in
                    let newobj := Psucc index in
                      let newpath := Psucc newobj in
                        let maxvar' := Psucc newpath in
                          seq (
                            block None (
                              compile_constrarray_aux cn sz blockvar' index newobj newpath (fun j =>
                                block None
                                (
                                  (seq
                                    (compile (Context maxvar' (Some ((newobj, newpath, true), None)) nil O false) (initializers j))
                                    (compile_discard 1%nat nil maxvar' (Interm.exit _ _ 1%nat))
                                  )
                                )
                              ) (exit _ _ 1%nat) 0
                            )
                          )
                          (
                            let bl' := (Some (blockvar, maxvar c, (cn, sz)) :: blocks c) in
                              seq
                              (compile (Context midvar (curobjpathfield c) bl' (further_blocks c) (is_destructor_body c)) body)
                              (compile_discard 1%nat bl' midvar (Interm.exit _ _ 1%nat))
                          )
                )
              )
      end
    | Sexit n =>
      compile_discard n (blocks c) (maxvar c) (Interm.exit _ _ (further_blocks c + n)%nat)
    | Sreturn ov =>
      compile_discard (length (blocks c)) (blocks c) (maxvar c) (
        if is_destructor_body c
          then (Interm.exit _ _ (S (further_blocks c + length (blocks c))))
          else Interm.ret _ _
            (match ov with
               None => None
               | Some v => Some (compile_var (Oldvar v))
             end))

    | Sconstructor cn vargs =>
      match curobjpathfield c with
        | Some ((curobj, curpath, ismostderived), None) =>
          seq (
            call _ (Static _ (compile_static (Newstatic (compile_constrdestr cn (StaticConstructor (map (fun tyv : _ * _ => let (ty, _) := tyv in ty) vargs)) ismostderived)))) (compile_var (Newvar (curobj )) :: compile_var (Newvar (curpath )) :: map (fun v => compile_var (Oldvar v)) (map (fun tyv : _ * _ => let (_, v) := tyv in v) vargs)) None
          ) (
            exit _ _ 1%nat
          )
        | _ => GARBAGE
      end

    | Sinitscalar v =>
      match curobjpathfield c with
        | Some ((curobj, _, _), Some (cn, f)) => seq
          (Interm.putfield _ cn f (compile_var (Newvar (curobj ))) (compile_var (Oldvar v)))
          (exit _ _ 1%nat)
        | _ => GARBAGE
      end

    | Scall kind vargs vret =>
      call _ (
        match kind with
          | Cppsem.Static f => Static _ (compile_static (Oldstatic f))
          | Cppsem.NonVirtual cn ms => NonVirtual cn ms
        end
      ) (map (fun v => compile_var (Oldvar v)) vargs)
      (match vret with
         None => None
         | Some v => Some (compile_var (Oldvar v))
       end)

    | Snative n l tg => Interm.native _ ( n) (map (fun v => compile_var (Oldvar v)) l) (
      match tg with
        None => None
        | Some v => Some (compile_var (Oldvar v))
      end)

    | Smove src tgt => Interm.move _ _ (compile_var (Oldvar src)) (compile_var (Oldvar tgt))

    | Sgetfield obj cn fs tgt => Interm.getfield _ cn fs (compile_var (Oldvar obj)) (compile_var (Oldvar tgt))

    | Sputfield obj cn fs val => Interm.putfield _ cn fs (compile_var (Oldvar obj)) (compile_var (Oldvar val))

    | Sindex obj cn idx tgt => Interm.arrayindex _ _ cn (compile_var (Oldvar idx)) (compile_var (Oldvar obj)) (compile_var (Oldvar tgt))

    | Sinvoke obj class method args retval => Interm.invoke _ (compile_var (Oldvar obj)) class method (map (fun v => compile_var (Oldvar v)) args)
      (match retval with
         None => None
         | Some v => Some (compile_var (Oldvar v))
       end)

    | Sdyncast obj cfrom cto res =>
      let (tree, _) := Well_formed_hierarchy.path_to hierarchy_wf cto in
        match (tree ! cfrom) with
          | None => GARBAGE
          | Some nil => Interm.dyncast _ _ cfrom cto (compile_var (Oldvar obj)) (compile_var (Oldvar res))
          | Some l =>
            match at_most_list path_eq_dec l with
              | inleft _ => Interm.null _ _ cto (compile_var (Oldvar res))
              | inright _ => Interm.statcast _ _ cfrom cto (compile_var (Oldvar obj)) (compile_var (Oldvar res))
            end
        end
        
    | Sstatcast obj cfrom cto res => Interm.statcast _ _ cfrom cto (compile_var (Oldvar obj)) (compile_var (Oldvar res))
    | Sptreq ptr1 ptr2 vres => Interm.ptreq _ _ (compile_var (Oldvar ptr1)) (compile_var (Oldvar ptr2)) (compile_var (Oldvar vres))

  end.

Lemma compile_exit_succ : forall cur cur', Cppsem.exit_succ cur = Some cur' ->
  forall maxvar maxvar' curobjpathfield q' n' bo blockvar cn sz,
    compile (Context maxvar curobjpathfield (Some (blockvar, maxvar', (cn, sz)) :: q') n' bo) cur =
    seq (
      block None
      (compile_destrarray cn blockvar maxvar (exit _ _ 1%nat) (sz-1))
    )
    (compile (Context maxvar' curobjpathfield q' (S n') bo) cur').

Definition compile' (c : context) (s : Cppsem.stmt A nativeop) : Interm.stmt A nativeop :=
  seq
  (compile c s)
  (compile_discard 1%nat (blocks c) (maxvar c) (Interm.exit _ _ 1%nat))
.

Definition compile_base_initializer (class : ident) (init : option (Cppsem.stmt A nativeop)) (h : Class.Inheritance.t) (b : ident) (curobj curpath maxvar : var) : Interm.stmt A nativeop :=
  let newobj := Psucc maxvar in
    let newpath := Psucc newobj in
      let maxvar' := Psucc newpath in
        block None (
          seq (
            seq
            (pathop _ _ (addbase class h b) (Some (compile_var (Newvar curpath))) (compile_var (Newvar newpath)))
            (casttobase _ _ (compile_var (Newvar curobj)) class h b (compile_var (Newvar newobj)))
          )
          (
            compile' (Context maxvar' (Some ((newobj, newpath, false), None)) nil O false)
            match init with
              | None => Sconstructor b nil
              | Some s => s
            end
          )
        )
          .

Definition compile_constrarray tinit b sz newobj index newobj' newpath' maxvar' :=
  compile_constrarray_aux b sz newobj index newobj' newpath' (
    fun j => block None (compile' (Context maxvar' (Some ((newobj', newpath', true), None)) nil O false) (tinit j))
  ) (exit _ _ 1%nat).


Definition compile_field_initializer class tinit init f curobj curpath maxvar :=
  let newobj := Psucc maxvar in
    let index := Psucc newobj in
      let newobj' := Psucc index in
        let newpath' := Psucc newobj' in
        let maxvar' := Psucc newpath' in
  match FieldSignature.type f with
    | FieldSignature.Scalar ty =>
      match assoc (@Constructor.initializer_key_eq_dec _) (existT _ Constructor.field (tt, f)) init with
        | None => skip _ _
        | Some st => block None (
          compile' (Context maxvar (Some ((curobj, curpath, false ), (Some (class, f)))) nil O false) st
        )
      end
    | FieldSignature.Struct b psz =>
      seq (
        getfield _ class f (compile_var (Newvar curobj)) (compile_var (Newvar newobj))
      ) (
        block None (
          compile_constrarray (
            match assoc (@FieldSignature.eq_dec _) f tinit with
              | Some init'' => init''
              | _ => (fun _ => Sconstructor b nil)
            end
          ) b (Zpos psz) newobj index newobj' newpath' maxvar' 0
        )
      )
  end.


Definition compile_constr_fields fields class tinit init body curobj curpath maxvar :=
  fold_right (fun f s => seq (
    compile_field_initializer class tinit init f curobj curpath maxvar
  ) s)
  ((compile' (Context xH None nil O false) body))
  fields.

Lemma vborder_list_ex : forall class, {vb | exists c, (Program.hierarchy prog) ! class = Some c /\ vborder_list (Program.hierarchy prog) (Class.super c) vb} + {(Program.hierarchy prog) ! class = None}.

Definition compile_constr_all_fields (ismostderived : bool) class tinit init body curobj curpath maxvar :=
    match (Program.hierarchy prog) ! class with
      | None => GARBAGE
      | Some cl => seq (
        setdyntype _ _ (
          if ismostderived then true else
            match vborder_list_ex class with
              | inleft (exist (_ :: _) _) => false
              | _ => true
            end
        ) class
        (compile_var (Newvar curobj)) (compile_var (Newvar curpath))
      )
      (compile_constr_fields (Class.fields cl) class tinit init body curobj curpath maxvar)
    end
    .

Definition compile_constr_direct_non_virtual_bases ismostderived vb class tinit init body curobj curpath maxvar :=
  fold_right (fun (b : ident) (s : Interm.stmt A nativeop) => seq (
    compile_base_initializer class (assoc (@Constructor.initializer_key_eq_dec _) (existT _ Constructor.base (Constructor.direct_non_virtual, b)) init) Class.Inheritance.Repeated b curobj curpath maxvar
  )
  s
  )
  (compile_constr_all_fields ismostderived class tinit init body curobj curpath maxvar)
  vb
.
 
Definition compile_constr_non_virtual_part ismostderived class tinit init body curobj curpath maxvar :=
  match (Program.hierarchy prog) ! class with
    | None => GARBAGE
    | Some cl => compile_constr_direct_non_virtual_bases ismostderived (map (fun hb : Class.Inheritance.t * ident => let (_, b) := hb in b) (filter (fun hb : _ * ident =>
        match hb with
          | (Class.Inheritance.Shared, _) => false
          | _ => true
        end
      ) (Class.super cl)))
 class tinit init body
      curobj curpath maxvar
  end.

Definition compile_constr_virtual_bases vb class tinit init body curobj curpath maxvar :=
  fold_right (fun (b : ident) (s : Interm.stmt A nativeop) => seq (
    compile_base_initializer class (assoc (@Constructor.initializer_key_eq_dec A) (existT _ Constructor.base (Constructor.virtual, b)) init) Class.Inheritance.Shared b curobj curpath maxvar
  )
  s
  )
  (seq (skip _ _) (compile_constr_non_virtual_part true class tinit init body curobj curpath maxvar))
  vb
.

Definition compile_constr ismostderived (k : Constructor.init_key_primary) (k2 : Constructor.init_key_secondary k) (vb : list (Constructor.init_key_item A k)) class tinit init body curobj curpath maxvar :=
  match k as k' return Constructor.init_key_secondary k' -> list (Constructor.init_key_item A k') -> _ with
    | Constructor.base => fun k2' vb' =>
      match k2' with
        | Constructor.direct_non_virtual => compile_constr_direct_non_virtual_bases ismostderived vb' class tinit init body curobj curpath maxvar
        | Constructor.virtual => compile_constr_virtual_bases vb' class tinit init body curobj curpath maxvar
      end
    | Constructor.field => fun _ vb' =>
      compile_constr_fields vb' class tinit init body curobj curpath maxvar
  end k2 vb.

Definition compile_constructor (class : ident) (c : Constructor.t A nativeop) (ismostderived : bool) : Interm.static_fun A nativeop :=
  let curobj := Psucc xH in
    let curpath := Psucc curobj in
      let is_most_derived := Psucc curpath in
        let maxvar := Psucc is_most_derived in
          Interm.Static_fun
          (compile_var (Oldvar (Constructor.this c)) :: compile_var (Newvar curpath) :: map (fun v => compile_var (Oldvar v)) (Constructor.args c))
          (
            seq
            (Interm.move _ _ (compile_var (Oldvar (Constructor.this c))) (compile_var (Newvar curobj)))
            (
              let nv :=seq
                (skip _ _)
                (compile_constr_non_virtual_part false class (Constructor.struct_field_initializers c) (Constructor.initializers c) (Constructor.body c) curobj curpath maxvar)
                in
                if ismostderived
                  then
                    match vborder_list_ex class with
                      | inright _ => nv
                      | inleft (exist vb _) => compile_constr_virtual_bases vb class (Constructor.struct_field_initializers c) (Constructor.initializers c) (Constructor.body c) curobj curpath maxvar
                    end
                  else
                    nv
            )
          )
          .

Lemma compile_constructor_eq_with_no_virtual_bases : forall class,
  (forall b, is_virtual_base_of (Program.hierarchy prog) b class -> False) ->
  forall c,
    compile_constructor class c true = compile_constructor class c false.

Definition compile_base_finalizer (class : ident) (h : Class.Inheritance.t) (b : ident) (curobj curpath maxvar : var) : Interm.stmt A nativeop :=
  let newobj := Psucc maxvar in
    let newpath := Psucc newobj in
      let maxvar' := Psucc newpath in
        seq (
          seq
          (pathop _ _ (addbase class h b) (Some (compile_var (Newvar curpath))) (compile_var (Newvar newpath)))
          (casttobase _ _ (compile_var (Newvar curobj)) class h b (compile_var (Newvar newobj)))
        )
        (call _ (Static _ (compile_static (Newstatic (compile_constrdestr b (StaticDestructor ) false)))) (compile_var (Newvar newobj) :: compile_var (Newvar newpath) :: nil) None)
        .

Definition compile_destr_virtual_bases vb class curobj curpath maxvar :=
  fold_right (fun (b : ident) (s : Interm.stmt A nativeop) => seq (
    compile_base_finalizer class Class.Inheritance.Shared b curobj curpath maxvar
  )
  s
  )
  (ret _ _ None)
  vb
.

Definition compile_destr_all_virtual_bases (ismostderived : bool) class curobj curpath maxvar :=
  seq (skip _ _)
  (if ismostderived
    then match vborder_list_ex class with
           | inright _ => GARBAGE
           | inleft (exist vb _) => (compile_destr_virtual_bases (rev vb) class curobj curpath maxvar)
         end
    else
      ret _ _ None)
      .

Definition compile_destr_direct_non_virtual_bases (ismostderived : bool) vb class curobj curpath maxvar :=
    fold_right (fun (b : ident) (s : Interm.stmt A nativeop) => seq (
      compile_base_finalizer class Class.Inheritance.Repeated b curobj curpath maxvar
    )
    s
    )
    (compile_destr_all_virtual_bases ismostderived class curobj curpath maxvar)
    vb
.

Definition compile_destr_field f class curobj maxvar :=
  let newobj := Psucc maxvar in
    let index := Psucc newobj in
      let newobj' := Psucc index in
        let newpath' := Psucc newobj' in
          let maxvar' := Psucc newpath' in
            match FieldSignature.type f with
              | FieldSignature.Scalar ty => skip _ _
              | FieldSignature.Struct b psz =>
                seq (
                  getfield _ class f (compile_var (Newvar curobj)) (compile_var (Newvar newobj))
                ) (
                  block None (
                    compile_destrarray_aux b newobj index newobj' newpath' (exit _ _ 1%nat) (Zpos psz - 1)
                  )
                )
            end.

Definition compile_destr_all_direct_non_virtual_bases ismostderived class curobj curpath maxvar :=
  match (Program.hierarchy prog) ! class with
    | None => GARBAGE
    | Some cl => compile_destr_direct_non_virtual_bases ismostderived (rev (
      (map (fun hb : Class.Inheritance.t * ident => let (_, b) := hb in b) (filter (fun hb : _ * ident =>
        match hb with
          | (Class.Inheritance.Shared, _) => false
          | _ => true
        end
      ) (Class.super cl)))
    )
    ) class curobj curpath maxvar
  end.

Definition compile_destr_fields ismostderived l class curobj curpath maxvar :=
  fold_right (fun f (s : Interm.stmt A nativeop) => seq (
    compile_destr_field f class curobj maxvar
  )
  s
  )
  (seq (skip _ _ ) (compile_destr_all_direct_non_virtual_bases ismostderived class curobj curpath maxvar))
  l
.

Definition compile_destr_all_fields ismostderived class curobj curpath maxvar :=
  match (Program.hierarchy prog) ! class with
    | None => GARBAGE
    | Some cl => compile_destr_fields ismostderived (rev (Class.fields cl)) class curobj curpath maxvar
  end.

Definition compile_destr (ismostderived : bool) (k : Constructor.init_key_primary) (k2 : Constructor.init_key_secondary k) (vb : list (Constructor.init_key_item A k)) :=
  match k as k' return Constructor.init_key_secondary k' -> list (Constructor.init_key_item A k') -> _ with
    | Constructor.base => fun k2' vb' =>
      match k2' with
        | Constructor.direct_non_virtual => compile_destr_direct_non_virtual_bases ismostderived vb'
        | Constructor.virtual => compile_destr_virtual_bases vb'
      end
    | Constructor.field => fun _ vb' =>
      compile_destr_fields ismostderived vb'
  end k2 vb.

Definition compile_destructor (class : ident) (ismostderived : bool) : Interm.static_fun A nativeop :=
  let curobj := Psucc xH in
    let curpath := Psucc curobj in
      let maxvar := Psucc curpath in
        Interm.Static_fun
        (compile_var (Newvar curobj) :: compile_var (Newvar curpath) :: nil)
        (
          (
            if ismostderived
              then (fun s => s)
              else
                seq
                (setdyntype _ _ false class
                  (compile_var (Newvar curobj)) (compile_var (Newvar curpath)))
          )(
            seq
            match (Program.hierarchy prog) ! class with
              | None => GARBAGE
              | Some cl =>
                match Method.find (Program.destructor_sig prog) (Class.methods cl) with
                  | None => GARBAGE
                  | Some m =>
                    match Method.kind m with
                      | Method.concrete mi =>
                        match (Program.methods prog) ! mi with
                          | None => GARBAGE
                          | Some code =>
                            block None
                              (seq
                                (move _ _ (compile_var (Newvar curobj)) (compile_var (Oldvar (Method_body.this code))))
                                (compile' (Context maxvar None nil O true ) (Method_body.code code))
                              )
                        end
                      | _ => GARBAGE
                    end
                end
            end
            (
              compile_destr_all_fields ismostderived class curobj curpath maxvar
            )
          )
        ).

Definition vars_invariant vars vars' :=
  forall var v, vars ! var = Some v -> vars' ! (compile_var (Oldvar var)) = Some (Val (A := A) v).

Lemma vars_invariant_newvar : forall vars vars',
  vars_invariant vars vars' ->
  forall var val, vars_invariant vars (PTree.set (compile_var (Newvar var)) val vars').

Lemma vars_invariant_newvar_recip : forall vars vars' var val,
  vars_invariant vars (PTree.set (compile_var (Newvar var)) val vars') ->
  vars_invariant vars vars'.

Lemma vars_invariant_oldvar : forall vars vars',
  vars_invariant vars vars' ->
  forall var val,
    vars_invariant (PTree.set var val vars) (PTree.set (compile_var (Oldvar var)) (Val val) vars').

Section Block_invariant.

  Variable heap : PTree.t Object.t.
  Variable vars : PTree.t (value A).
  Variable curobjpathfield : option ((ident * ident * bool) * option (ident * FieldSignature.t A)).
  Variable destrbody : bool.
  Variable minvar : positive.

Inductive block_invariant : ident -> list (BlockPoint.t A nativeop) -> list (option (var * var * (ident * Z))) -> list (frame A nativeop) -> Prop :=
| block_invariant_nil :
  match curobjpathfield with
    | Some ((curobj, curpath, _), _) => Plt curobj curpath /\ Plt curpath minvar
    | _ => True
  end ->
  block_invariant minvar nil nil nil

| block_invariant_cons_none : forall maxvar bl cbl fbl,
  block_invariant maxvar bl cbl fbl ->
  forall stl stl', stl' = map (compile (Context maxvar curobjpathfield cbl O destrbody)) stl ++
    (compile_discard 1%nat (cbl) (maxvar ) (Interm.exit _ _ 1%nat)) :: nil
    ->
    block_invariant maxvar (BlockPoint.make stl None :: bl) (None :: cbl) (Interm.Block None stl' :: fbl)

| block_invariant_cons_some : forall maxvar bl cbl fbl,
  block_invariant maxvar bl cbl fbl ->
  forall var, Plt maxvar var ->
    forall maxvar', Plt var maxvar' ->
      forall obj o, heap ! obj = Some o ->
        forall cn, cn = Object.class o ->
          forall sz, sz = Object.arraysize o ->
            forall hp,
              vars ! (compile_var (Newvar var)) = Some (Val (Value.ptr (Value.subobject obj nil 0 Class.Inheritance.Repeated (cn :: nil) hp))) ->
            forall stl stl', stl' = map (compile (Context maxvar curobjpathfield cbl O destrbody)) stl ++
              (compile_discard 1%nat (cbl) (maxvar ) (Interm.exit _ _ 1%nat)) :: nil
 ->
              block_invariant maxvar' (BlockPoint.make stl (Some obj) :: bl) (Some (var, maxvar, (cn, sz)) :: cbl) (Interm.Block (Some obj) stl' :: fbl).

End Block_invariant.

Lemma block_invariant_heap_new : forall heap vars curobjpathfield destrbody minvar maxvar bl cbl fbl,
  block_invariant heap vars curobjpathfield destrbody minvar maxvar bl cbl fbl ->
  forall obj, heap ! obj = None -> forall o,
    block_invariant (PTree.set obj o heap) vars curobjpathfield destrbody minvar maxvar bl cbl fbl.

Lemma block_invariant_oldvar : forall heap vars curobjpathfield destrbody minvar maxvar bl cbl fbl,
  block_invariant heap vars curobjpathfield destrbody minvar maxvar bl cbl fbl ->
  forall var val,
    block_invariant heap (PTree.set (compile_var (Oldvar var)) val vars) curobjpathfield destrbody minvar maxvar bl cbl fbl.

Lemma block_invariant_newvar_gt : forall heap vars curobjpathfield destrbody minvar maxvar bl cbl fbl,
  block_invariant heap vars curobjpathfield destrbody minvar maxvar bl cbl fbl ->
  forall var, Plt maxvar var ->
    forall val,
      block_invariant heap (PTree.set (compile_var (Newvar var)) val vars) curobjpathfield destrbody minvar maxvar bl cbl fbl.
 
Lemma block_invariant_curobj_lt_curpath : forall heap vars curobj curpath ismostderived curfield destrbody minvar maxvar bl cbl fbl,
  block_invariant heap vars (Some ((curobj, curpath, ismostderived), curfield)) destrbody minvar maxvar bl cbl fbl ->
  Plt curobj curpath.

Lemma block_invariant_curpath_lt_minvar : forall heap vars curobj curpath ismostderived curfield minvar maxvar destrbody bl cbl fbl,
  block_invariant heap vars (Some ((curobj, curpath, ismostderived), curfield)) destrbody minvar maxvar bl cbl fbl ->
  Plt curpath minvar.

Lemma block_invariant_minvar_le_maxvar : forall heap vars curobjpathfield minvar maxvar destrbody bl cbl fbl,
  block_invariant heap vars curobjpathfield destrbody minvar maxvar bl cbl fbl ->
  Ple minvar maxvar.

Fixpoint retrieve_list_stmt (U V : Type) (ls : U) (p : list (V * U)) {struct p} : U :=
  match p with
    | nil => ls
    | (_, ls') :: p' => retrieve_list_stmt ls' p'
  end.

Lemma retrieve_list_stmt_app : forall (U V : Type) p1 ls p2, retrieve_list_stmt (U := U) (V := V) ls (p1 ++ p2) = retrieve_list_stmt (retrieve_list_stmt ls p1) p2.


Section Stack_invariant.

  Variable heap : PTree.t (Object.t).
  Variable deallocated_objects : list positive.

Inductive stack_invariant : forall called_by_destr_body : bool, list (StackFrame.t A nativeop) ->
  option (option (PTree.t (Value.t A)) * positive * PTree.t (value A) * option ((positive * positive * bool) * option (ident * FieldSignature.t A))) ->
list (Interm.frame A nativeop) -> Prop :=
| stack_invariant_Kconstr : forall fr obj ar i h p tinit init body k k2 b bases,
  fr = StackFrame.Kconstr obj ar i (h, p) tinit init body k k2 b bases ->
  forall o, heap ! obj = Some o ->
    forall X class, valid_relative_pointer (Program.hierarchy prog) (Object.class o) (Object.arraysize o) ar X i h p class ->
      forall vars vars', vars_invariant vars vars' ->
        forall curobj hp, vars' ! (compile_var (Newvar curobj)) = Some (Val (Value.ptr (Value.subobject obj ar i h p hp))) ->
          forall curpath, Plt curobj curpath -> vars' ! (compile_var (Newvar curpath)) = Some (Path _ X h p) ->
            forall midvar,
              Plt curpath midvar ->
            forall fr' be,
              fr' = Block None (compile_constr (if path_eq_dec (h, p) (Class.Inheritance.Repeated, class :: nil) then true else false) k2 bases class tinit init body curobj curpath midvar :: be) ->
              forall newobj newpath newfield maxvar,
                match k as k' return Constructor.init_key_item _ k' -> Constructor.init_key_secondary k' -> _ with
                  | Constructor.field => fun f _ => newobj = curobj /\ newpath = curpath /\ midvar = maxvar /\ be = nil /\ exists cn, last p = Some cn /\ newfield = Some (cn, f)
                  | Constructor.base => fun ba k2' =>
                    newfield = None /\ Plt midvar newobj /\ Plt newobj newpath /\ Plt newpath maxvar /\
                    let h' := match k2' with Constructor.direct_non_virtual => h | _ => Class.Inheritance.Shared end in
                      let p' := match k2' with
                                  | Constructor.direct_non_virtual => p ++ ba :: nil
                                  | Constructor.virtual => ba :: nil
                                end in
                      vars' ! (compile_var (Newvar newpath)) = Some (Path _ X h' p') /\
                      be = nil /\
                      exists hp',
                        vars' ! (compile_var (Newvar newobj)) = Some (Val (Value.ptr (Value.subobject obj ar i h' p' hp')))
                end b k2 ->
              forall stk stk',
                stack_invariant false stk None stk' ->
                stack_invariant false (fr :: stk) (Some (Some vars, maxvar, vars', Some ((newobj, newpath, false), newfield))) (fr' :: stk')

| stack_invariant_Kconstrarray : forall fr obj ar n i cn tinit vars,
  fr = StackFrame.Kconstrarray obj ar n i cn tinit ->
  forall o, heap ! obj = Some o ->
    valid_array_path (Program.hierarchy prog) cn n (Object.class o) (Object.arraysize o) ar ->
      0 <= i < n ->
      forall vars', vars_invariant vars vars' ->
        forall blockvar hp, vars' ! (compile_var (Newvar blockvar)) = Some (Val (Value.ptr (Value.subobject obj ar 0 Class.Inheritance.Repeated (cn :: nil) hp))) ->
          forall minvar, Plt minvar blockvar ->
            forall index, Plt blockvar index ->
                forall newobj, Plt index newobj ->
              forall hp'', vars' ! (compile_var (Newvar newobj)) = Some (Val (Value.ptr (Value.subobject obj ar i Class.Inheritance.Repeated (cn :: nil) hp''))) ->
                forall newpath, Plt newobj newpath ->
                  vars' ! (compile_var (Newvar newpath)) = Some (Path _ cn Class.Inheritance.Repeated (cn :: nil)) ->
                  forall maxvar, Plt newpath maxvar ->
                    forall fr',
                      fr' = Block None (compile_constrarray tinit cn n blockvar index newobj newpath maxvar (i+1) :: nil) ->
                      forall bo stk stk' so,
                        stack_invariant bo stk (Some (Some vars, minvar, vars', so)) stk' ->
                        stack_invariant false (fr :: stk) (Some (Some vars, maxvar, vars', Some ((newobj, newpath, true), None))) (fr' :: stk')

| stack_invariant_Kconstrother : forall fr obj ar i h p tinit init body vars1 k k2 b bases,
  fr = StackFrame.Kconstrother obj ar i (h, p) tinit init body vars1 k k2 b bases ->
  forall o, heap ! obj = Some o ->
    forall X class, valid_relative_pointer (Program.hierarchy prog) (Object.class o) (Object.arraysize o) ar X i h p class ->
      forall vars0 vars', vars_invariant vars0 vars' ->
        forall curobj hp, vars' ! (compile_var (Newvar curobj)) = Some (Val (Value.ptr (Value.subobject obj ar i h p hp))) ->
          forall curpath, Plt curobj curpath -> vars' ! (compile_var (Newvar curpath)) = Some (Path _ X h p) ->
            forall maxvar, Plt curpath maxvar ->
              forall fr1, match k with
                            | Constructor.field => fr1 = nil
                            | Constructor.base => exists stl, fr1 = Callframe (exit _ _ 1%nat :: stl) vars' None :: nil
                          end ->
            forall fr' stk' be,
              fr' = fr1 ++ Block None (compile_constr (if path_eq_dec (h, p) (Class.Inheritance.Repeated, class :: nil) then true else false) k2 bases class tinit init body curobj curpath maxvar :: be) :: stk' ->
              be = nil ->
              forall so,
                match k with
                  | Constructor.base => vars0 = vars1
                  | Constructor.field => so = Some (Some vars0, maxvar, vars', None)
                end ->
                forall stk,
                  stack_invariant false stk None stk' ->
                  stack_invariant false (fr :: stk) so fr'

| stack_invariant_Kconstrothercells : forall fr obj ar n i cn tinit vars,
  fr = StackFrame.Kconstrothercells obj ar n i cn tinit vars ->
      forall vars', vars_invariant vars vars' ->
        forall blockvar hp, vars' ! (compile_var (Newvar blockvar)) = Some (Val (Value.ptr (Value.subobject obj ar 0 Class.Inheritance.Repeated (cn :: nil) hp))) ->
          forall minvar, Plt minvar blockvar ->
            forall index, Plt blockvar index ->
              forall newobj, Plt index newobj ->
                forall newpath, Plt newobj newpath ->
                  forall maxvar, Plt newpath maxvar ->
                    forall fr' stl stk',
                      fr' = Callframe (exit _ _ 1%nat :: stl) vars' None :: Block None (compile_constrarray tinit cn n blockvar index newobj newpath maxvar (i+1) :: nil) :: stk' ->
                      forall bo stk so',
                        stack_invariant bo stk (Some (Some vars, minvar, vars', so')) stk' ->
                        forall so,
                        stack_invariant false (fr :: stk) so fr'

| stack_invariant_Kreturnfromcall : forall fr ores vars further blocks,
  fr = StackFrame.Kreturnfromcall ores vars further blocks ->
  forall bo q q' curobjpathfield minvar maxvar vars',
    block_invariant heap vars' curobjpathfield bo minvar maxvar blocks q' q ->
    vars_invariant vars vars' ->
    forall ores', ores' = match ores with
                            | None => None
                            | Some res => Some (compile_var (Oldvar res))
                          end ->
    forall fr' stk',
      fr' = Callframe (map (compile (Context maxvar curobjpathfield q' O bo)) further ++ (compile_discard 1%nat q' maxvar (Interm.exit _ _ 1%nat)) :: nil) vars' ores' :: q ++ stk' ->
      forall stk ,
        stack_invariant bo stk (Some (Some vars, minvar, vars', curobjpathfield)) stk' ->
        forall so,
        stack_invariant false (fr :: stk) so (fr')

| stack_invariant_Kdestr :
forall fr obj ar i h p,
  fr = StackFrame.Kdestr obj ar i (h, p) ->
  forall o, heap ! obj = Some o ->
    forall X class, valid_relative_pointer (Program.hierarchy prog) (Object.class o) (Object.arraysize o) ar X i h p class ->
      forall vars vars',
        vars_invariant vars vars' ->
        forall curobj hp, vars' ! (compile_var (Newvar curobj)) = Some (Val (Value.ptr (Value.subobject obj ar i h p hp))) ->
          forall curpath, Plt curobj curpath -> vars' ! (compile_var (Newvar curpath)) = Some (Path _ X h p) ->
            forall maxvar,
              Plt curpath maxvar ->
              forall fr',
                fr' = Block None (compile_destr_all_fields (if path_eq_dec (h, p) (Class.Inheritance.Repeated, class :: nil) then true else false) class curobj curpath maxvar :: nil) ->
                forall stk stk',
                  stack_invariant false stk None stk' ->
                  stack_invariant true (fr :: stk) (Some (Some vars, maxvar, vars', None)) (fr' :: stk')

| stack_invariant_Kdestrcell : forall fr obj ar i cn,
  fr = StackFrame.Kdestrcell obj ar i cn ->
  forall vars',
    forall blockvar hp, vars' ! (compile_var (Newvar blockvar)) = Some (Val (Value.ptr (Value.subobject obj ar 0 Class.Inheritance.Repeated (cn :: nil) hp))) ->
      forall minvar, Plt minvar blockvar ->
        forall index, Plt blockvar index ->
          forall newobj, Plt index newobj ->
            forall newpath, Plt newobj newpath ->
              forall fr' stl,
                fr' = Callframe (compile_destrarray_aux cn blockvar index newobj newpath (exit _ _ 1%nat) (i-1) :: stl) vars' None ->
                forall bo stk stk' oo,
                  stack_invariant bo stk (Some (None, minvar, vars', oo)) stk' ->
                  stack_invariant false (fr :: stk) None (fr' :: stk')

| stack_invariant_Kdestrother : forall fr obj ar i h p k k2 base other,
  fr = StackFrame.Kdestrother obj ar i (h, p) k k2 base other ->
  forall o, heap ! obj = Some o ->
    forall X class, valid_relative_pointer (Program.hierarchy prog) (Object.class o) (Object.arraysize o) ar X i h p class ->
      forall vars',
        forall curobj hp, vars' ! (compile_var (Newvar curobj)) = Some (Val (Value.ptr (Value.subobject obj ar i h p hp))) ->
          forall curpath, Plt curobj curpath -> vars' ! (compile_var (Newvar curpath)) = Some (Path _ X h p) ->
            forall maxvar, Plt curpath maxvar ->
              forall fr' so,
                match k with
                  | Constructor.base => fr' = Callframe (compile_destr (if path_eq_dec (h, p) (Class.Inheritance.Repeated, class :: nil) then true else false) k2 other class curobj curpath maxvar :: nil) vars' None /\ so = None
                  | Constructor.field => fr' = Block None (compile_destr (if path_eq_dec (h, p) (Class.Inheritance.Repeated, class :: nil) then true else false) k2 other class curobj curpath maxvar :: nil) /\ so = Some (None, maxvar, vars', None)
                end ->
                forall s1,
                s1 = match k as k' return Constructor.init_key_secondary k' -> _ with
                       | Constructor.base => fun k'2 => match k'2 with Constructor.virtual => StackFrame.Kdestrcell obj ar (i) X :: nil | _ => nil
                                                        end
                       | _ => fun _ => nil
                     end k2 ->
                forall stk stk',
                  stack_invariant false (s1 ++ stk) None stk' ->
                  stack_invariant false (fr :: stk) so (fr' :: stk')

| stack_invariant_Kcontinue : forall fr k stm obj stl blocks,
  fr = StackFrame.Kcontinue k stm obj stl blocks ->
  forall o, heap ! obj = Some o ->
    forall vars vars',
      vars_invariant vars vars' ->
      forall p
        q' midvar maxvar curobjpathfield bo so,
        match k with
          | StackFrame.continue_constr =>
            so = Some vars /\
            exists blockvar,
              Plt midvar blockvar /\
              Plt blockvar maxvar /\
              exists hp,
                vars' ! (compile_var (Newvar blockvar)) = Some (Val (Value.ptr (Value.subobject obj nil 0 Class.Inheritance.Repeated (Object.class o :: nil) hp))) /\
                p = Interm.Block None (compile' (Context maxvar curobjpathfield (Some (blockvar, midvar, (Object.class o, Object.arraysize o)) :: q') O bo) stm :: nil)
                :: Interm.Block (Some obj) (map (compile (Context midvar curobjpathfield q' O bo)) stl ++ (compile_discard 1%nat q' midvar (Interm.exit _ _ 1%nat)) :: nil)
                :: nil
          | StackFrame.continue_destr varsd =>
            midvar = maxvar /\
            varsd = vars /\
            so = None /\
            exists stm', Cppsem.exit_succ stm = Some stm' /\
            exists p', exists fur',
              p = Block None (compile (Context maxvar curobjpathfield q' (S (length p')) bo) stm' :: fur')
              :: map (fun ob : _ * _ => let (o, b) := ob in Block o b) p'
              ++
              Block (Some obj) (map (compile (Context midvar curobjpathfield q' O bo)) stl ++ (compile_discard 1%nat q' midvar (Interm.exit _ _ 1%nat)) :: nil
) :: nil /\ forall o b, In (Some o, b) p' -> In o deallocated_objects
        end ->
        forall q minvar,
          block_invariant heap vars' curobjpathfield bo minvar midvar blocks q' q ->
          forall stk' stk'',
            stk'' = p ++ q ++ stk' ->
            forall stk,
              stack_invariant bo stk (Some (Some vars, minvar, vars', curobjpathfield)) stk' ->
              stack_invariant false (fr :: stk) (Some (so, maxvar, vars', None)) stk''

| stack_invariant_nil :
  forall so,
    stack_invariant false nil so nil
.

Lemma stack_invariant_oldvar : forall bo stk so stk',
  stack_invariant bo stk so stk' ->
  forall vars minvar vars' curobjpathfield, so = Some (Some vars, minvar, vars', curobjpathfield) ->
    forall var val, stack_invariant bo stk (Some (Some (PTree.set var val vars), minvar, PTree.set (compile_var (Oldvar var)) (Val val) vars', curobjpathfield)) stk'.


Ltac differt :=
  match goal with
    |- (PTree.set (compile_var (Newvar ?var)) _ _) ! _ = _ =>
      rewrite PTree.gso; [ eassumption |
        apply compile_var_other; intro Habs; injection Habs; intro; subst; destruct (Plt_irrefl var); repeat (eassumption || eapply Plt_trans)
      ]
  end.

Lemma stack_invariant_newvar_lt : forall bo stk so stk',
  stack_invariant bo stk so stk' ->
  forall ovars minvar vars' oo, so = Some (ovars, minvar, vars', oo) ->
    forall var, Plt minvar var -> forall val, stack_invariant bo stk (Some (ovars, minvar, PTree.set (compile_var (Newvar var)) (val) vars', oo)) stk'.

End Stack_invariant.


Lemma stack_invariant_heap_new : forall heap deallo bo stk so stk',
  stack_invariant heap deallo bo stk so stk' ->
  forall obj, heap ! obj = None -> forall o,
    stack_invariant (PTree.set obj o heap) deallo bo stk so stk'.

Lemma stack_invariant_dealloc_cons : forall heap dealloc bo stk so stk',
  stack_invariant heap dealloc bo stk so stk' ->
  forall obj,
    stack_invariant heap (obj :: dealloc) bo stk so stk'.

Inductive state_invariant : State.t A nativeop -> Interm.state A nativeop -> Prop :=

| state_invariant_constr : forall s obj ar i h p tinit init body vars k k2 bases,
  State.kind s = State.constr obj ar i (h, p) tinit init body vars k k2 bases ->
  forall o, (Globals.heap (State.global s)) ! obj = Some o ->
    forall X class, valid_relative_pointer (Program.hierarchy prog) (Object.class o) (Object.arraysize o) ar X i h p class ->
      forall vars', vars_invariant vars vars' ->
        forall curobj hp, vars' ! (compile_var (Newvar curobj)) = Some (Val (Value.ptr (Value.subobject obj ar i h p hp))) ->
          forall curpath, Plt curobj curpath -> vars' ! (compile_var (Newvar curpath)) = Some (Path _ X h p) ->
            forall maxvar, Plt curpath maxvar ->
            forall s',
              Interm.current s' = compile_constr (if path_eq_dec (h, p) (Class.Inheritance.Repeated, class :: nil) then true else false) k2 bases class tinit init body curobj curpath maxvar ->
              Interm.further s' = nil
              ->
              Interm.vars s' = vars' ->
              stack_invariant (Globals.heap (State.global s)) (State.deallocated_objects s) false (State.stack s) None (Interm.stack s') ->
              state_invariant s s'

| state_invariant_constr_array : forall s obj ar n i cn tinit vars,
  State.kind s = State.constr_array obj ar n i cn tinit vars ->
  forall o, (Globals.heap (State.global s)) ! obj = Some o ->
    valid_array_path (Program.hierarchy prog) cn n (Object.class o) (Object.arraysize o) ar ->
      0 <= i <= n ->
      forall vars', vars_invariant vars vars' ->
        forall blockvar hp, vars' ! (compile_var (Newvar blockvar)) = Some (Val (Value.ptr (Value.subobject obj ar 0 Class.Inheritance.Repeated (cn :: nil) hp))) ->
          forall minvar, Plt minvar blockvar ->
            forall index, Plt blockvar index ->
              forall newobj', Plt index newobj' ->
                forall newpath', Plt newobj' newpath' ->
                  forall maxvar', Plt newpath' maxvar' ->
                    forall s',
                      Interm.current s' = compile_constrarray tinit cn n blockvar index newobj' newpath' maxvar' i ->
                      Interm.further s' = nil ->
                      Interm.vars s' = vars' ->
                      forall bo curobjpathfield,
                        stack_invariant (Globals.heap (State.global s)) (State.deallocated_objects s) bo (State.stack s) (Some (Some vars, minvar, vars', curobjpathfield)) (Interm.stack s') ->
                        state_invariant s s'

| state_invariant_codepoint : forall s vars cur fur blocks,
  State.kind s = State.codepoint vars cur fur blocks ->
  forall q q' curobjpathfield minvar maxvar vars' bo,
    block_invariant (Globals.heap (State.global s)) vars' curobjpathfield bo minvar maxvar blocks q' q ->
      forall p
        (Hp_dealloc : forall o b, In (Some o, b) p -> In o (State.deallocated_objects s))
        s',
        ((if requires_destruct cur then True else cur = Sexit O) \/ p = nil) ->
        Interm.current s' = compile (Context maxvar curobjpathfield q' (length p) bo) cur ->
        ((requires_destruct cur) = (true) \/ retrieve_list_stmt (Interm.further s') p = map (compile (Context maxvar curobjpathfield q' O bo)) fur ++ (compile_discard 1%nat q' maxvar (Interm.exit _ _ 1%nat)) :: nil) ->
        vars_invariant vars vars' ->
        Interm.vars s' = vars' ->
        forall r,
        Interm.stack s' = map (fun ob : _ * _ => let (o, b) := ob in Block o b) p ++ q ++ r ->
        stack_invariant (Globals.heap (State.global s)) (State.deallocated_objects s) bo (State.stack s) (Some (Some vars, minvar, vars', curobjpathfield)) r ->
        state_invariant s s'

| state_invariant_destr : forall s obj ar i h p k k2 bases,
  State.kind s = State.destr obj ar i (h, p) k k2 bases ->
  forall o, (Globals.heap (State.global s)) ! obj = Some o ->
    forall X class, valid_relative_pointer (Program.hierarchy prog) (Object.class o) (Object.arraysize o) ar X i h p class ->
      forall vars' curobj hp, vars' ! (compile_var (Newvar curobj)) = Some (Val (Value.ptr (Value.subobject obj ar i h p hp))) ->
          forall curpath, Plt curobj curpath -> vars' ! (compile_var (Newvar curpath)) = Some (Path _ X h p) ->
            forall maxvar, Plt curpath maxvar ->
            forall s',
              Interm.current s' = compile_destr (if path_eq_dec (h, p) (Class.Inheritance.Repeated, class :: nil) then true else false) k2 bases class curobj curpath maxvar ->
              Interm.further s' = nil ->
              Interm.vars s' = vars' ->
              forall s1,
                s1 = match k as k' return Constructor.init_key_secondary k' -> _ with
                       | Constructor.base => fun k'2 => match k'2 with Constructor.virtual => StackFrame.Kdestrcell obj ar (i) X :: nil | _ => nil
                                                        end
                       | _ => fun _ => nil
                     end k2 ->
                stack_invariant (Globals.heap (State.global s)) (State.deallocated_objects s) false (s1 ++ State.stack s) None (Interm.stack s') ->
                state_invariant s s'

| state_invariant_destrarray : forall s obj ar i cn,
  State.kind s = State.destr_array obj ar i cn ->
  forall o, (Globals.heap (State.global s)) ! obj = Some o ->
    forall n,
    valid_array_path (Program.hierarchy prog) cn n (Object.class o) (Object.arraysize o) ar ->
      forall vars' blockvar hp, vars' ! (compile_var (Newvar blockvar)) = Some (Val (Value.ptr (Value.subobject obj ar 0 Class.Inheritance.Repeated (cn :: nil) hp))) ->
          forall minvar, Plt minvar blockvar ->
          forall index, Plt blockvar index ->
            forall newobj', Plt index newobj' ->
              forall newpath', Plt newobj' newpath' ->
                  forall s',
                    Interm.current s' = (compile_destrarray_aux cn blockvar index newobj' newpath' (exit _ _ 1%nat) (i)) ->
                    Interm.vars s' = vars' ->
                    forall bo curobjpathfield,
                      stack_invariant (Globals.heap (State.global s)) (State.deallocated_objects s) bo (State.stack s) (Some (None, minvar, vars', curobjpathfield)) (Interm.stack s') ->
                      state_invariant s s'

.

Function exitable (s : stmt A nativeop) (n : nat) {struct s} : option (stmt A nativeop) :=
  match s with
    | exit n' => if le_lt_dec n n' then Some (exit _ _ (n' - n)) else None
    | ret ovar => Some (ret _ _ ovar)
    | _ => None
  end.

Lemma exitable_O : forall s s', exitable s O = Some s' -> s = s'.

Lemma exitable_S : forall n stm stm', exitable stm (S n) = Some stm' ->
  exists stm1, exit_succ stm = Some stm1 /\ exitable stm (S n) = exitable stm1 n.

Variable is_primary_path : list ident -> bool.

Variable prog' : Interm.program A nativeop.

Lemma exit_further : forall p stm stm',
  exitable stm (length p) = Some stm' ->
  forall next_object dyntype field_values heap further vars1 stk,
    exists heap',
      star (evtr sem) (step (sem:=sem) prog' is_primary_path)
      (State stm further vars1
        (map
          (fun ob : option positive * list (stmt A nativeop) =>
            let (o, b) := ob in Block o b) p ++ stk) (Global (Globals.make heap next_object field_values) dyntype)) E0
    (State stm' (retrieve_list_stmt further p) vars1 stk (Global (Globals.make heap' next_object field_values) dyntype)) /\
    forall obj, (exists stl, In (Some obj, stl) p) \/ heap' ! obj = heap ! obj
.
                    
Lemma map_atom' : forall la,
  map
  (fun a : (sigT (ATOM.val (t := A))) => let (ty, va) := a in Some (Val (Value.atom ty va))) la =
  map (@Some _) (map (@Val _) (map (fun a : sigT (ATOM.val (t := A)) => let (ty, va) := a in Value.atom ty va) la)).

Lemma map_atom : forall la,
  map
  (fun x : sigT (ATOM.val (t := A)) =>
    let (ty, va) := x in Some (Value.atom ty va)) la =
  map (@Some _) (map (fun a : (sigT (ATOM.val (t := A))) => let (ty, va) := a in Value.atom ty va) la).

Lemma vars_invariant_map : forall v v', vars_invariant v v' ->
  forall lv args, map (@Some _) args = map (fun var => v ! var) lv ->
    map (@Some _) (map (@Val _) args) = map (fun var => v' ! var) (map (fun var => compile_var (Oldvar var)) lv).

Lemma constructed_field_not_deallocated : forall s, Invariant.invariant prog s ->
  forall obj ar i h p hp,
    valid_pointer (Program.hierarchy prog) (Globals.heap (State.global s)) (Value.subobject obj ar i h p hp) ->
    forall cn, last p = Some cn ->
      forall c, (Program.hierarchy prog) ! cn = Some c ->
        forall fs, In fs (Class.fields c) ->
          assoc (@aux_constr_state_key_eq_dec _) (obj, ar, i, (h, p), fs) (State.field_construction_states s) = Some Constructed ->
          In obj (State.deallocated_objects s) -> False.

Corollary get_field_scalar_some_not_deallocated_object :
  forall s, scalar_fields_some_constructed prog s -> invariant prog s ->
    forall obj ar i h p hp, valid_pointer (Program.hierarchy prog) (Globals.heap (State.global s)) (Value.subobject obj ar i h p hp) -> forall cn, last p = Some cn ->
      forall c, (Program.hierarchy prog) ! cn = Some c ->
        forall fs, In fs (Class.fields c) ->
          forall ty, FieldSignature.type fs = FieldSignature.Scalar ty ->
            forall v, Globals.get_field (Globals.field_values (State.global s)) (obj, ar, i, (h, p), fs) = Some v ->
              In obj (State.deallocated_objects s) -> False.

Lemma vars_invariant_set_params : forall args vargs',
  vars_invariant
  (Cppsem.set_params args vargs')
  (Interm.set_params (map (@Val _) args) (map (fun v => compile_var (Oldvar v)) vargs')).

Record invariant (s : State.t A nativeop) (s' : Interm.state A nativeop) : Prop := invariant_intro {
  invariant_state : state_invariant s s';
  invariant_heap : forall obj, In obj (State.deallocated_objects s) \/ (Globals.heap (globals (global s'))) ! obj = (Globals.heap (State.global s)) ! obj
    ;
  invariant_next_object : Globals.next_object (globals (global s')) = Globals.next_object (State.global s)
    ;
  invariant_field_values : forall f v, Globals.get_field (Globals.field_values (State.global s)) f = Some v -> Globals.get_field (Globals.field_values (globals (global s'))) f = Some v
    ;
  invariant_dynamic_type : forall obj ar i sh sp ch cp dh dp,
    Cppsem.dynamic_type (Program.hierarchy prog) (Globals.heap (State.global s)) (State.construction_states s) obj ar i sh sp ch cp dh dp ->
    assoc (@pointer_eq_dec _) (obj, (ar, i, (sh, sp))) (dynamic_type (global s')) = Some ((ch, cp), (dh, dp))
    ;
  invariant_allow_static_cast : forall obj ar i h p hp,
    valid_pointer (Program.hierarchy prog) (Globals.heap (State.global s)) (Value.subobject obj ar i h p hp) ->

    assoc (@pointer_eq_dec _) (obj, (ar, i, (h, p))) (State.construction_states s) = Some Constructed ->
    assoc (@pointer_eq_dec _) (obj, (ar, i, (h, p))) (dynamic_type (global s')) <> None
    ;
  invariant_inheritance : Invariant.invariant prog s
    ;
  invariant_scalar_fields : scalar_fields_some_constructed prog s
}.

Lemma invariant_allow_static_cast_strong : forall s s', invariant s s' ->
  forall obj ar i h p hp,
    valid_pointer (Program.hierarchy prog) (Globals.heap (State.global s)) (Value.subobject obj ar i h p hp) ->
    (Some BasesConstructed =< assoc (@pointer_eq_dec _) (obj, (ar, i, (h, p))) (State.construction_states s)) ->
    (assoc (@pointer_eq_dec _) (obj, (ar, i, (h, p))) (State.construction_states s) =< Some StartedDestructing) ->
    assoc (@pointer_eq_dec _) (obj, (ar, i, (h, p))) (dynamic_type (global s')) <> None
.
  

Lemma true_uniq : forall h1 h2 : True, h1 = h2.

Hypothesis prog'_hierarchy : Program.hierarchy prog = Interm.hierarchy prog'.

Hypothesis prog'_constructors : forall cn c, (Program.constructors prog) ! cn = Some c -> forall ty co, assoc (@Program.constructor_key_eq_dec _) ty c = Some co -> forall b,
  (Interm.statics prog') ! (compile_static (Newstatic (compile_constrdestr cn (StaticConstructor ty) b))) = Some (compile_constructor cn co b).

Hypothesis prog'_destructors : forall cn, (Program.hierarchy prog) ! cn <> None -> forall b, (Interm.statics prog') ! (compile_static (Newstatic (compile_constrdestr cn (StaticDestructor) b))) = Some (compile_destructor cn b).

Hypothesis prog'_statics : forall i m, (Program.static_methods prog) ! i = Some m -> (Interm.statics prog') ! (compile_static (Oldstatic i)) = Some (
  Static_fun (map (fun v => compile_var (Oldvar v)) (Static_method.args m)) (compile' (Context xH None nil O false) (Static_method.code m))
).

Hypothesis prog'_methods : forall i m, (Program.methods prog) ! i = Some m -> (Interm.methods prog') ! i = Some (
  Interm.Method_body
  (compile_var (Oldvar (Method_body.this m)))
  (map (fun v => compile_var (Oldvar v)) (Cppsem.Method_body.args m)) (compile' (Context xH None nil O false) (Cppsem.Method_body.code m))
).

Hypothesis prog'_main :
  Interm.main prog' = compile' (Context xH None nil O false) (Program.main prog).

Theorem init : forall st1, Cppsem.initial_state prog st1 ->
  exists st2, Interm.initial_state prog' st2 /\
    exists st2', star _ (Interm.step (sem := sem) prog' is_primary_path) st2 E0 st2' /\
      invariant st1 st2'.

Theorem fin : forall st1 st2 (r : outcome (evtr sem)),
  invariant st1 st2 ->
  Cppsem.final_state st1 r ->
  exists st2', star _ (Interm.step (sem := sem) prog' is_primary_path) st2 E0 st2' /\
    Interm.final_state st2' r.


Variable s1 : State.t A nativeop.
Variable t : trace (evtr sem).
Variable s2 : State.t A nativeop.

Variable cppsem : cppsemparam.

Hypothesis Hstep : Cppsem.step prog cppsem s1 t s2.

Variable s1' : state A nativeop.

Variable Hinv : invariant s1 s1'.

Notation goal := (exists s2',
  plus (evtr sem) (Interm.step prog' (sem := sem) is_primary_path) s1' t s2' /\
    invariant s2 s2')
  (only parsing).


Remark kind_inj : forall s18 s42 : State.t A nativeop, s18 = s42 ->
  State.kind s18 = State.kind s42.


Remark stack_inj : forall s18 s42 : State.t A nativeop,
  s18 = s42 ->
  State.stack s18 = State.stack s42.



Ltac abs t := t.

Lemma preservation_requires_destruct : forall vars sdestruct stl0
  stl obj bl stk gl cs auxcs f
  (Hs1 : State.make
         (State.codepoint vars sdestruct stl0
            (BlockPoint.make stl (Some obj) :: bl)) stk gl cs auxcs f = s1)
(Hdestruct : requires_destruct sdestruct = true),
goal.



Lemma preservation_exit_O : forall vars stl0 bl stk gl cs auxcs f
  (Hs1 : State.make (State.codepoint vars (Sexit 0) stl0 bl) stk gl cs auxcs f = s1),
  goal.



Transparent compile_discard.

Lemma preservation_exit_S_none : forall vars n stl0 stl bl stk gl cs auxcs f
  (Hs1 : State.make
    (State.codepoint vars (Sexit (S n)) stl0
      (BlockPoint.make stl None :: bl)) stk gl cs auxcs f = s1),
  goal.


Lemma preservation_skip_nil : forall vars bl stk gl cs auxcs f
  (Hs1: State.make (State.codepoint vars Sskip nil bl) stk gl cs auxcs f = s1),
  goal.


Lemma preservation_requires_exit_none : forall vars sexit stl0 stl bl stk gl cs auxcs f
(Hs1 : State.make
  (State.codepoint vars sexit stl0 (BlockPoint.make stl None :: bl))
  stk gl cs auxcs f = s1
)
(Hrequires_exit : requires_exit sexit = true)
, goal.


Lemma preservation_Sreturn_Kconstrother_base : forall vars stl obj ar i h p tinit init0 body vars' k2 b q stk gl cs auxcs f
(Hs1 :
  State.make (State.codepoint vars (Sreturn None) stl nil)
  (StackFrame.Kconstrother obj ar i (h, p) tinit init0 body vars'
    Constructor.base k2 b q :: stk) gl cs auxcs f = s1),
goal.


Lemma preservation_Sreturn_Kdestr : forall vars stl obj ar i h p stk gl cs auxcs f
  (Hs1 :
    State.make (State.codepoint vars (Sreturn None) stl nil)
    (StackFrame.Kdestr obj ar i (h, p) :: stk) gl cs auxcs f = s1),
  goal.


Lemma preservation_Sreturn_Kconstrothercells : forall vars stl obj ar n i cn init0 vars' stk gl cs auxcs f
  (Hs1 :
    State.make (State.codepoint vars (Sreturn None) stl nil)
    (StackFrame.Kconstrothercells obj ar n i cn init0 vars' :: stk) gl
    cs auxcs f = s1
  ),
  goal.



Lemma preservation_return_nil : forall vars vres stl vres' vars' stl' bl' stk gl cs auxcs f
  (Hs1 : State.make (State.codepoint vars (Sreturn vres) stl nil)
    (StackFrame.Kreturnfromcall vres' vars' stl' bl' :: stk) gl cs auxcs f = s1),
  goal.





Lemma preservation_destr_array_nil_Kcontinue : forall obj i cn vars stm obj' ostl bl stk gl cs auxcs f
  (Hs1 : State.make (State.destr_array obj nil i cn)
    (StackFrame.Kcontinue (StackFrame.continue_destr (A:=A) vars) stm
      obj' ostl bl :: stk) gl cs auxcs f = s1)
  (Hnil : i = -1),
  goal.



Lemma preservation_block_some : forall vars vlocstruct cn num init0 stm stl bl stk gl cs auxcs f
  (Hs1 : State.make
    (State.codepoint vars
      (Sblock (Some (vlocstruct, cn, num)) init0 stm) stl bl) stk gl cs
    auxcs f = s1),
  goal.


Lemma preservation_constr_array_nil_Kcontinue : forall obj ar n cn init0 vars stm obj' obk bl stk gl cs auxcs f
  (Hs1 :
    State.make (State.constr_array obj ar n n cn init0 vars)
    (StackFrame.Kcontinue (StackFrame.continue_constr A) stm obj' obk bl
      :: stk) gl cs auxcs f = s1),
  goal.


Lemma preservation_skip_cons : forall vars stm stl bl stk gl cs auxcs f
  (Hs1 : s1 = (State.make (State.codepoint vars Sskip (stm :: stl) bl) stk gl cs auxcs f)),
  goal.



Lemma preservation_if : forall vars test iftrue iffalse stl bl stk gl cs auxcs f
  (Hs1 : State.make (State.codepoint vars (Sif test iftrue iffalse) stl bl) stk gl cs auxcs f = s1),
  goal.

  
Lemma preservation_loop : forall vars stm stl bl stk gl cs auxcs f
(Hs1 : State.make (State.codepoint vars (Sloop stm) stl bl) stk gl cs auxcs f = s1),
goal.


Lemma preservation_seq : forall vars stm1 stm2 stl bl stk gl cs auxcs f
  (Hs1 : State.make (State.codepoint vars (Sseq stm1 stm2) stl bl) stk gl cs auxcs f = s1),
  goal.


Lemma preservation_block_none : forall vars i stm stl bl stk gl cs auxcs f (Hs1 : State.make (State.codepoint vars (Sblock None i stm) stl bl) stk gl cs auxcs f = s1), goal.


Lemma preservation_native : forall vars op vargs vres stl bl stk gl cs auxcs f
  (Hs1 : State.make (State.codepoint vars (Snative op vargs vres) stl bl) stk gl cs auxcs f = s1),
  goal.


Lemma preservation_move : forall vars src tgt stl bl stk gl cs auxcs f (Hs1 : State.make (State.codepoint vars (Smove src tgt) stl bl) stk gl cs auxcs f = s1), goal.


Lemma preservation_getfield : forall vars vobj ty fs tgt stl bl stk gl constate auxcs f
  (Hs1 : State.make (State.codepoint vars (Sgetfield vobj ty fs tgt) stl bl)
         stk gl constate auxcs f = s1),
  goal.


Lemma preservation_putfield : forall vars vobj ty fs tgt stl bl stk gl constate auxcs f
  (Hs1 : State.make (State.codepoint vars (Sputfield vobj ty fs tgt) stl bl) stk gl constate auxcs f = s1),
  goal.


Lemma preservation_index : forall vars vobj cn vindex tgt stl bl stk gl constate auxcs f
  (Hs1 : State.make (State.codepoint vars (Sindex vobj cn vindex tgt) stl bl) stk gl constate auxcs f = s1),
  goal.


Lemma preservation_ptreq : forall vars vptr1 vptr2 tgt stl bl stk gl constate auxcs f
  (Hs1 : State.make (State.codepoint vars (Sptreq vptr1 vptr2 tgt) stl bl) stk gl constate auxcs f = s1),
  goal.


Lemma preservation_call : forall vars ckind vargs oret stl blocks0 stack global constate auxcs f
  (Hs1 : State.make
    (State.codepoint vars (Scall nativeop ckind vargs oret) stl
      blocks0) stack global constate auxcs f = s1),
  goal.


Lemma preservation_invoke : forall vars vobj cn ms vargs vres stl bl stk gl constate auxcs f
  (Hs1 : State.make
    (State.codepoint vars (Sinvoke vobj cn ms vargs vres) stl bl) stk
    gl constate auxcs f = s1),
  goal.


Lemma preservation_dyncast : forall
  vars vobj cfrom cto vres stl bl stk gl constate auxcs f
  (Hs1 :
State.make
         (State.codepoint vars (Sdyncast vobj cfrom cto vres) stl bl) stk gl
         constate auxcs f = s1
  ), goal.


Lemma preservation_statcast : forall vars vobj cfrom cto vres stl bl stk gl constate auxcs f
  (Hs1 : State.make
    (State.codepoint vars (Sstatcast vobj cfrom cto vres) stl bl) stk gl
    constate auxcs f = s1),
  goal.



Lemma preservation_constr_array_cons : forall obj ar n i cn init0 vars stk gl cs auxcs f
  (Hs1 :
    State.make (State.constr_array obj ar n i cn init0 vars) stk gl cs
    auxcs f = s1)
  (Hcons : i < n),
  goal.


Lemma preservation_constr_cons_base_direct_non_virtual : forall obj ar i hp tinit init0 body vars b q stk gl cs auxcs f
  (Hs1 : State.make
    (State.constr obj ar i hp tinit init0 body vars Constructor.base
      Constructor.direct_non_virtual (b :: q)) stk gl cs auxcs f = s1),
  goal.


Lemma preservation_constr_cons_field_scalar_some : forall obj ar i hp tinit init0 body vars b q stk gl cs auxcs f
  (Hs1 :
    State.make
    (State.constr obj ar i hp tinit init0 body vars Constructor.field tt
      (b :: q)) stk gl cs auxcs f = s1
  )
  (Hscalar : match FieldSignature.type b with
               | FieldSignature.Scalar _ => True
               | FieldSignature.Struct _ _ => False
             end)
  code
  (Hinit :
    assoc (Constructor.initializer_key_eq_dec (A:=A))
    (existT (Constructor.init_subkey A) Constructor.field (tt, b)) init0 =
    Some code),
  goal.


Lemma preservation_constr_cons_field_struct : forall obj ar i hp tinit init0 body vars fs q stk gl cs auxcs f
  (Hs1 : State.make
    (State.constr obj ar i hp tinit init0 body vars Constructor.field tt
      (fs :: q)) stk gl cs auxcs f = s1)
  b n
  (Hstruct : FieldSignature.type fs = FieldSignature.Struct b n),
  goal.


Lemma preservation_constr_base_direct_non_virtual_nil : forall obj ar i h p tinit init0 body vars stk gl cs auxcs f
  (Hs1 :
    State.make
    (State.constr obj ar i (h, p) tinit init0 body vars Constructor.base
      Constructor.direct_non_virtual nil) stk gl cs auxcs f = s1),
  goal.

    
Lemma preservation_constr_cons_field_scalar_none : forall
  obj ar i h p tinit init0 body vars fs q stk gl cs auxcs f
  (Hs1: State.make
    (State.constr obj ar i (h, p) tinit init0 body vars
      Constructor.field tt (fs :: q)) stk gl cs auxcs f = s1)
  ty (Hscalar : FieldSignature.type fs = FieldSignature.Scalar ty)
  (Hnone : assoc (Constructor.initializer_key_eq_dec (A:=A))
    (existT (Constructor.init_subkey A) Constructor.field (tt, fs)) init0 =
    None),
  goal.


Lemma preservation_Sinitscalar : forall vars varg stl obj ar i h p tinit init0 body fs q stk gl cs auxcs f
  (Hs1 :
    State.make (State.codepoint vars (Sinitscalar varg) stl nil)
    (StackFrame.Kconstr obj ar i (h, p) tinit init0 body
      Constructor.field tt fs q :: stk) gl cs auxcs f = s1),
  goal.

    
Lemma preservation_constr_array_nil_Kconstrother_field : forall obj ar n b init0 vars obj' ar' i' h p tinit' init' body' vars' fs q stk gl cs auxcs f
  (Hs1 :
    State.make (State.constr_array obj ar n n b init0 vars)
    (StackFrame.Kconstrother obj' ar' i' (h, p) tinit' init' body' vars'
      Constructor.field tt fs q :: stk) gl cs auxcs f = s1
  ), goal.


Lemma preservation_constr_fields_nil : forall obj ar i h p tinit init0 body vars stk gl cs auxcs f
  (Hs1 :
    State.make
    (State.constr obj ar i (h, p) tinit init0 body vars Constructor.field
      tt nil) stk gl cs auxcs f = s1),
  goal.


  
Lemma preservation_destr_array_cons : forall
  obj ar j cn stk gl cs auxcs f
  (Hs1 : State.make (State.destr_array obj ar j cn) stk gl cs auxcs f = s1)
  (Hnonnegative : 0 <= j),
  goal.

  
Lemma preservation_destr_field_cons_scalar : forall obj ar i h p fs l stk gl cs auxcs f
  (Hs1 :
    State.make
    (State.destr obj ar i (h, p) Constructor.field tt (fs :: l)) stk gl
    cs auxcs f = s1)
  ty (Hscalar : FieldSignature.type fs = FieldSignature.Scalar ty),
  goal.


Lemma preservation_destr_field_cons_struct : forall obj ar i h p fs l stk gl cs auxcs f
  (Hs1 : State.make
    (State.destr obj ar i (h, p) Constructor.field tt (fs :: l)) stk gl
    cs auxcs f = s1)
 b n
 (Hstruct : FieldSignature.type fs = FieldSignature.Struct b n),
 goal.


Lemma preservation_destr_array_nil_Kdestrother_field : forall obj ar j cn obj' ar' i' hp' fs l stk gl cs auxcs f
  (Hs1 :
    State.make (State.destr_array obj ar j cn)
    (StackFrame.Kdestrother obj' ar' i' hp' Constructor.field tt fs l
      :: stk) gl cs auxcs f = s1)
  (Hnil : j = -1),
  goal.

  
Lemma preservation_destr_field_nil : forall obj ar i h p stk gl cs auxcs f
  (Hs1 : State.make (State.destr obj ar i (h, p) Constructor.field tt nil) stk gl cs auxcs f = s1),
  goal.

  
Lemma preservation_destr_base_cons_direct_non_virtual : forall obj ar i h p b bases stk gl cs auxcs f
    (Hs1 :
      State.make
      (State.destr obj ar i (h, p) Constructor.base Constructor.direct_non_virtual (b :: bases)) stk
      gl cs auxcs f = s1),
    goal.


Lemma preservation_destr_base_cons_virtual : forall obj ar i h p b bases stk gl cs auxcs f
  (Hs1 :
    State.make
    (State.destr obj ar i (h, p) Constructor.base Constructor.virtual
      (b :: bases)) stk gl cs auxcs f = s1),
  goal.


 Lemma preservation_destr_base_direct_non_virtual_nil_Kdestrother_base : forall obj ar i hp obj' ar' i' hp' beta b bases' stk gl cs auxcs f
   (Hs1 :
     State.make
     (State.destr obj ar i hp Constructor.base
       Constructor.direct_non_virtual nil)
     (StackFrame.Kdestrother obj' ar' i' hp' Constructor.base beta b
       bases' :: stk) gl cs auxcs f = s1),
   goal.


Lemma preservation_destr_base_direct_non_virtual_nil_Kdestrcell : forall obj ar i hp obj' ar' i' cn' stk gl cs auxcs f
  (Hs1 : State.make
         (State.destr obj ar i hp Constructor.base
            Constructor.direct_non_virtual nil)
         (StackFrame.Kdestrcell obj' ar' i' cn' :: stk) gl cs auxcs f = s1),
         goal.


Lemma preservation_destr_base_virtual_nil : forall obj ar i h p stk gl cs auxcs f
  (Hs1 :
  State.make
           (State.destr obj ar i (h, p) Constructor.base Constructor.virtual
              nil) stk gl cs auxcs f = s1),
goal.

 

Lemma preservation_Sconstructor_Kconstrarray : forall vars b tvargs stl obj ar n i cn init0 stk gl cs auxcs f
  (Hs1 : State.make (State.codepoint vars (Sconstructor b tvargs) stl nil)
    (StackFrame.Kconstrarray obj ar n i cn init0 :: stk) gl cs auxcs f = s1),
  goal.


Lemma preservation_constr_cons_base_virtual : forall obj ar i hp tinit init0 body vars b q stk gl cs auxcs f
  (Hs1 : State.make
    (State.constr obj ar i hp tinit init0 body vars Constructor.base
      Constructor.virtual (b :: q)) stk gl cs auxcs f = s1),
  goal.



Lemma preservation_Sconstructor_Kconstr_base : forall vars b tvargs stl obj ar i h p tinit init0 body k2 q stk gl cs auxcs f
(Hs1 : State.make (State.codepoint vars (Sconstructor b tvargs) stl nil)
  (StackFrame.Kconstr obj ar i (h, p) tinit init0 body
    Constructor.base k2 b q :: stk) gl cs auxcs f = s1),
goal.


  

Lemma preservation_constr_base_virtual_nil : forall obj ar i h p tinit init0 body vars stk gl cs auxcs f
  (Hs1 :
    State.make
    (State.constr obj ar i (h, p) tinit init0 body vars Constructor.base
      Constructor.virtual nil) stk gl cs auxcs f = s1),
  goal.



Theorem preservation : goal.


End Compiler.