Module FlatAsmgenproof

Require Import Coqlib Integers Values Maps AST.
Require Import Memtype Memory.
Require Import Smallstep.
Require Import Asm RealAsm.
Require Import FlatAsm FlatAsmBuiltin FlatAsmgen FlatAsmProgram.
Require Import Segment.
Require Import Events.
Require Import StackADT.
Require Import Linking Errors.
Require Import Globalenvs FlatAsmGlobenv.
Require Import AsmFacts.
Require Import Num.

Open Scope Z_scope.

Ltac monadInvX1 H :=
  let monadInvX H :=
      monadInvX1 H ||
                 match type of H with
                 | (?F _ _ _ _ _ _ _ _ = OK _) =>
                   ((progress simpl in H) || unfold F in H); monadInvX1 H
                 | (?F _ _ _ _ _ _ _ = OK _) =>
                   ((progress simpl in H) || unfold F in H); monadInvX1 H
                 | (?F _ _ _ _ _ _ = OK _) =>
                   ((progress simpl in H) || unfold F in H); monadInvX1 H
                 | (?F _ _ _ _ _ = OK _) =>
                   ((progress simpl in H) || unfold F in H); monadInvX1 H
                 | (?F _ _ _ _ = OK _) =>
                   ((progress simpl in H) || unfold F in H); monadInvX1 H
                 | (?F _ _ _ = OK _) =>
                   ((progress simpl in H) || unfold F in H); monadInvX1 H
                 | (?F _ _ = OK _) =>
                   ((progress simpl in H) || unfold F in H); monadInvX1 H
                 | (?F _ = OK _) =>
                   ((progress simpl in H) || unfold F in H); monadInvX1 H
                 end
  in

  match type of H with
  | (OK _ = OK _) =>
      inversion H; clear H; try subst
  | (Error _ = OK _) =>
      discriminate
  | (bind ?F ?G = OK ?X) =>
      let x := fresh "x" in (
      let EQ1 := fresh "EQ" in (
      let EQ2 := fresh "EQ" in (
      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
      clear H;
      try (monadInvX EQ1);
      try (monadInvX1 EQ2))))
  | (bind2 ?F ?G = OK ?X) =>
      let x1 := fresh "x" in (
      let x2 := fresh "x" in (
      let EQ1 := fresh "EQ" in (
      let EQ2 := fresh "EQ" in (
      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
      clear H;
      try (monadInvX EQ1);
      try (monadInvX1 EQ2)))))
  | (match ?X with left _ => _ | right _ => assertion_failed end = OK _) =>
      destruct X eqn:?; [try (monadInvX1 H) | discriminate]
  | (match (negb ?X) with true => _ | false => assertion_failed end = OK _) =>
      destruct X as [] eqn:?; [discriminate | try (monadInvX1 H)]
  | (match ?X with true => _ | false => assertion_failed end = OK _) =>
      destruct X as [] eqn:?; [try (monadInvX1 H) | discriminate]
  | (mmap ?F ?L = OK ?M) =>
      generalize (mmap_inversion F L H); intro
  | (match ?X with Some _ => _ | None => _ end = _) =>
      let EQ := fresh "EQ" in (
      destruct X eqn:EQ; try (monadInvX1 H))
  | (match ?X with pair _ _ => _ end = OK _) =>
      let EQ := fresh "EQ" in (
      destruct X eqn:EQ; try (monadInvX1 H))
  end.

Ltac monadInvX H :=
  monadInvX1 H ||
  match type of H with
  | (?F _ _ _ _ _ _ _ _ = OK _) =>
      ((progress simpl in H) || unfold F in H); monadInvX1 H
  | (?F _ _ _ _ _ _ _ = OK _) =>
      ((progress simpl in H) || unfold F in H); monadInvX1 H
  | (?F _ _ _ _ _ _ = OK _) =>
      ((progress simpl in H) || unfold F in H); monadInvX1 H
  | (?F _ _ _ _ _ = OK _) =>
      ((progress simpl in H) || unfold F in H); monadInvX1 H
  | (?F _ _ _ _ = OK _) =>
      ((progress simpl in H) || unfold F in H); monadInvX1 H
  | (?F _ _ _ = OK _) =>
      ((progress simpl in H) || unfold F in H); monadInvX1 H
  | (?F _ _ = OK _) =>
      ((progress simpl in H) || unfold F in H); monadInvX1 H
  | (?F _ = OK _) =>
      ((progress simpl in H) || unfold F in H); monadInvX1 H
  end.


Lemma alignw_le : forall x, x <= align x alignw.


Lemma divides_align : forall y x,
    y > 0 -> (y | x) -> align x y = x.

Lemma align_idempotent : forall v x,
    x > 0 -> align (align v x) x = align v x.

Lemma alignw_divides:
  forall z,
    (alignw | align z alignw).



Lemma transl_fun_exists : forall gmap defs gdefs f id,
    transl_globdefs gmap defs = OK gdefs ->
    In (id, Some (Gfun (Internal f))) defs ->
    exists f', transl_fun gmap id f = OK f'
          /\ forall i, In i (fn_code f') -> In i (get_defs_code gdefs).

Definition size_gvar (def: option (AST.globdef Asm.fundef unit)) : Z :=
  match def with
  | Some (Gvar gv) => init_data_list_size (gvar_init gv)
  | _ => 0
  end.


Definition size_fun (def: option (AST.globdef Asm.fundef unit)) : Z :=
  match def with
  | Some (Gfun (Internal f)) => code_size (Asm.fn_code f)
  | _ => 0
  end.

Lemma align0: align 0 alignw = 0.

Lemma update_instrs_code_size:
  forall i c lmap csize lmap' csize'
    (UI : update_instrs lmap csize i c = (lmap', csize')),
    csize' = csize + code_size c.

Lemma update_instrs_other:
  forall i i' l (n: i <> i') c lmap csize lmap' csize'
    (UI : update_instrs lmap csize i c = (lmap', csize')),
    lmap' i' l = lmap i' l.

Lemma align_plus:
  forall a b z,
    (z | a) -> z <> 0 ->
    align (a + b) z = a + align b z.

Section UPDATE_MAPS.

  Variable gmap: GID_MAP_TYPE.
  Variable lmap: LABEL_MAP_TYPE.
  Variables dsize csize: Z.

  Variable i: ident.
  Variable def: option (globdef Asm.fundef unit).

  Variable gmap': GID_MAP_TYPE.
  Variable lmap': LABEL_MAP_TYPE.
  Variables dsize' csize': Z.

  Hypothesis UPDATE: update_maps_def gmap lmap dsize csize i def = (gmap', lmap', dsize', csize').

  Lemma update_gmap:
    forall i',
      gmap' i' = if ident_eq i i'
                 then match def with
                      | None => gmap i
                      | Some (Gfun (External ef)) => gmap i
                      | Some (Gfun (Internal f)) => Some (code_label csize)
                      | Some (Gvar gvar) => Some (data_label dsize)
                      end
                 else gmap i'.

  Lemma update_lmap:
    forall i' l,
      lmap' i' l = if ident_eq i i'
                   then match def with
                        | Some (Gfun (Internal f)) =>
                          fst (update_instrs lmap csize i (Asm.fn_code f)) i l
                        | _ => lmap i' l
                        end
                   else lmap i' l.

  Lemma update_dsize:
    dsize' = dsize + align (size_gvar def) alignw.

  Lemma update_dsize_mono:
    dsize <= dsize'.




  Lemma update_csize_mono:
    csize <= csize'.

  Hypothesis csize_div: (alignw | csize).

  Lemma update_csize:
    csize' = csize + align (size_fun def) alignw.


  Hypothesis dsize_div: (alignw | dsize).

  Lemma update_dsize_div:
    (alignw | dsize').

  Lemma update_csize_div:
    (alignw | csize').


End UPDATE_MAPS.

Definition sum {A: Type} (f: A -> Z) (l: list A) :=
  fold_left (fun acc e => acc + f e) l 0.

Lemma fold_left_plus:
  forall {A} f (l: list A) d,
    fold_left (fun acc e => acc + f e) l d = d + sum f l.

Definition sizes_gvars (defs: list (ident * option (AST.globdef Asm.fundef unit))) : Z :=
  sum (fun d => align (size_gvar (snd d)) alignw) defs.


Definition sizes_funs (defs: list (ident * option (AST.globdef Asm.fundef unit))) : Z :=
  sum (fun d => align (size_fun (snd d)) alignw) defs.

Lemma sum_pos:
  forall {A: Type} f (fpos: forall x, 0 <= f x) (l: list A), 0 <= sum f l.

Lemma sizes_gvars_pos:
  forall d, 0 <= sizes_gvars d.


Lemma sizes_funs_pos:
  forall d, 0 <= sizes_funs d.

Section UPDATE_MAPS2.

  Variable defs: list (ident * option (globdef Asm.fundef unit)).

  Variable gmap: GID_MAP_TYPE.
  Variable lmap: LABEL_MAP_TYPE.
  Variables dsize csize : Z.

  Variable gmap': GID_MAP_TYPE.
  Variable lmap': LABEL_MAP_TYPE.
  Variables dsize' csize' : Z.

  Hypothesis UPDATE: update_maps gmap lmap dsize csize defs = (gmap', lmap', dsize', csize').

  Lemma umind:
    forall (P : GID_MAP_TYPE -> LABEL_MAP_TYPE -> Z -> Z -> Prop)
      (Pstart: P gmap lmap dsize csize)
      (Pstep: forall g l s c g' l' s' c' i d,
          update_maps_def g l s c i d = (g', l', s', c') ->
          P g l s c ->
          In (i,d) defs ->
          P g' l' s' c'),
      P gmap' lmap' dsize' csize'.
  

  Lemma update_gmap_not_in:
    forall i,
      ~ In i (map fst defs) ->
      gmap' i = gmap i.

  Lemma update_lmap_not_in:
    forall i l,
      ~ In i (map fst defs) ->
      lmap' i l = lmap i l.

  Definition maps := (GID_MAP_TYPE * LABEL_MAP_TYPE * Z * Z )%type.

  Lemma umind_rel_inv:
    forall (inv: maps -> Prop)
      (INVstart: inv (gmap,lmap,dsize,csize))
      (INV: forall g l s c g' l' s' c' i d,
          update_maps_def g l s c i d = (g', l', s', c') ->
          inv (g,l,s,c) -> inv (g',l',s',c'))
      {A: Type} (f: maps -> A) (t: _ -> A -> A)
      (Pstep: forall g l s c g' l' s' c' i d,
          update_maps_def g l s c i d = (g', l', s', c') ->
          In (i,d) defs ->
          inv (g,l,s,c) ->
          f (g',l',s',c') = t d (f (g,l,s,c))),
      fold_left (fun (acc : A) (id : ident * option (globdef Asm.fundef unit)) =>
                   t (snd id) acc) defs (f (gmap,lmap,dsize,csize))
      = f (gmap',lmap',dsize',csize').

  Lemma umind_rel:
    forall {A: Type} (f: maps -> A) (t: _ -> A -> A)
      (Pstep: forall g l s c g' l' s' c' i d,
          update_maps_def g l s c i d = (g', l', s', c') ->
          In (i,d) defs ->
          f (g',l',s',c') = t d (f (g,l,s,c))),
      fold_left (fun (acc : A) (id : ident * option (globdef Asm.fundef unit)) =>
                   t (snd id) acc) defs (f (gmap,lmap,dsize,csize))
      = f (gmap',lmap',dsize',csize').


  Lemma umind_inv:
    forall (inv: maps -> Prop)
      (INVstart: inv (gmap,lmap,dsize,csize))
      (INV: forall g l s c g' l' s' c' i d,
          update_maps_def g l s c i d = (g', l', s', c') ->
          inv (g,l,s,c) -> inv (g',l',s',c')),
      inv (gmap',lmap',dsize',csize').

  Lemma updates_gmap_in:
    forall i s,
      gmap' i = Some s ->
      In i (map fst defs) \/ gmap i = Some s.


  Lemma updates_dsize:
    dsize' = dsize + sizes_gvars defs.


  Hypothesis csize_div: (alignw | csize).

  Lemma updates_csize:
    csize' = csize + sizes_funs defs.

  Hypothesis dsize_div: (alignw | dsize).

  Lemma updates_dsize_div:
    (alignw | dsize').

  Lemma updates_csize_div:
    (alignw | csize').


  Lemma csize_mono:
    csize <= csize'.


  Lemma dsize_mono:
    dsize <= dsize'.



End UPDATE_MAPS2.

Lemma update_maps_app:
  forall a b gmap lmap dsize csize,
    update_maps gmap lmap dsize csize (a ++ b) =
    let '(gmap', lmap', dsize', csize') := update_maps gmap lmap dsize csize a in
    update_maps gmap' lmap' dsize' csize' b.

Theorem update_map_gmap_range : forall p gmap lmap dsize csize,
    make_maps p = (gmap, lmap, dsize, csize) ->
    forall id slbl, gmap id = Some slbl -> In (fst slbl) (code_segid :: data_segid :: nil).








Lemma tprog_id_in_seg_lists : forall gmap lmap p dsize csize tp id,
  transl_prog_with_map gmap lmap p dsize csize = OK tp ->
  id = code_segid \/ id = data_segid ->
  In id (map segid (list_of_segments tp)).


Lemma update_maps_cons:
  forall defs i def g l d c,
    update_maps g l d c ((i,def)::defs) =
    let '(g1,l1,d1,c1) := update_maps_def g l d c i def in
    update_maps g1 l1 d1 c1 defs.

Theorem update_map_gmap_range1 : forall p gmap lmap dsize csize tp,
    make_maps p = (gmap, lmap, dsize, csize) ->
    transl_prog_with_map gmap lmap p dsize csize = OK tp ->
    forall id slbl, gmap id = Some slbl -> In (fst slbl) (map segid (list_of_segments tp)).





Lemma transl_instr_inv : forall ofs fid sid i x,
  transl_instr ofs fid sid i = OK x ->
  exists sblk, x = (i, sblk, fid) /\ sblk = mkSegBlock sid (Ptrofs.repr ofs) (Ptrofs.repr (instr_size i)).

Lemma transl_instrs_gen_valid_code_labels : forall instrs (gmap: GID_MAP_TYPE) i (tp:FlatAsm.program) sid ofs1 ofs2 ofs' instrs',
  (forall id b, gmap id = Some b -> In (fst b) (map segid (list_of_segments tp))) ->
  gmap i = Some (sid, ofs1) ->
  transl_instrs i sid ofs2 instrs = OK (ofs', instrs') ->
  code_labels_are_valid init_block (length (list_of_segments tp)) (gen_segblocks tp) instrs'.

Lemma transl_fun_gen_valid_code_labels : forall gmap i f f' (tp:FlatAsm.program),
  (forall id b, gmap id = Some b -> In (fst b) (map segid (list_of_segments tp))) ->
  transl_fun gmap i f = OK f' ->
  code_labels_are_valid init_block (length (list_of_segments tp)) (gen_segblocks tp) (fn_code f').

Lemma transl_globdefs_gen_valid_code_labels : forall defs gmap tdefs (tp:FlatAsm.program),
  (forall id b, gmap id = Some b -> In (fst b) (map segid (list_of_segments tp))) ->
  transl_globdefs gmap defs = OK tdefs ->
  code_labels_are_valid init_block (length (list_of_segments tp)) (gen_segblocks tp) (get_defs_code tdefs).



   
Section WITHTRANSF.

Variable prog: Asm.program.
Variable tprog: FlatAsm.program.
Hypothesis TRANSF: transf_program prog = OK tprog.

Let ge := Genv.globalenv prog.
Let tge := globalenv tprog.

   

 

   
Lemma target_code_labels_are_valid :
  code_labels_are_valid
    init_block (length (list_of_segments tprog))
    (gen_segblocks tprog)
    (get_program_code tprog).

Lemma find_instr_self : forall i,
    code_labels_are_distinct (get_program_code tprog) ->
    In i (get_program_code tprog) ->
    Genv.find_instr tge
                    (Vptr (gen_segblocks tprog (segblock_id (snd (fst i)))) (segblock_start (snd (fst i)))) = Some i.

Lemma transl_instr_segblock : forall ofs' id i i' sid,
      transl_instr (Ptrofs.unsigned ofs') id sid i = OK i' ->
      segblock_to_label (snd (fst i')) = (sid, ofs').

Lemma find_instr_ofs_non_negative : forall code ofs i,
    find_instr ofs code = Some i -> ofs >= 0.

Lemma transl_instrs_ofs_bound: forall code code' id sid ofs fofs,
  transl_instrs id sid ofs code = OK (fofs, code') -> ofs <= fofs.

Lemma find_instr_transl_instrs : forall code id sid i ofs ofs' fofs code',
    find_instr (Ptrofs.unsigned ofs) code = Some i ->
    transl_instrs id sid (Ptrofs.unsigned ofs') code = OK (fofs, code') ->
    fofs <= Ptrofs.max_unsigned ->
    exists i' ofs1, transl_instr ofs1 id sid i = OK i'
               /\ segblock_to_label (snd (fst i')) = (sid, Ptrofs.add ofs ofs')
               /\ In i' code'.

Lemma find_instr_transl_fun : forall id f f' ofs i gmap s,
    find_instr (Ptrofs.unsigned ofs) (Asm.fn_code f) = Some i ->
    transl_fun gmap id f = OK f' ->
    gmap id = Some s ->
    exists i' ofs1, transl_instr ofs1 id (fst s) i = OK i'
               /\ segblock_to_label (snd (fst i')) = (fst s, Ptrofs.add ofs (snd s))
               /\ In i' (fn_code f').









Lemma lnr_transf: list_norepet (map fst (AST.prog_defs prog)).

Lemma update_map_gmap_domain : forall gmap lmap dsize csize id slbl,
    make_maps prog = (gmap, lmap, dsize, csize) ->
    gmap id = Some slbl ->
    In id (prog_defs_names prog).



Lemma defs_nodup_labels : forall defs f id,
    defs_no_duplicated_labels defs ->
    In (id, Some (Gfun (Internal f))) defs ->
    list_norepet (labels (Asm.fn_code f)).

Ltac solve_label_pos_inv :=
  match goal with
  | [ |- _ <> Asm.Plabel _ /\ label_pos _ _ _ = Some _] =>
    split; solve_label_pos_inv
  | [ |- _ <> Asm.Plabel _ ] =>
    unfold not; inversion 1
  | [ |- label_pos _ _ _ = Some _ ] => auto
  | _ => idtac
  end.

Lemma label_pos_inv : forall l ofs a instrs z,
    label_pos l ofs (a :: instrs) = Some z ->
    (a = Asm.Plabel l /\ z = ofs + instr_size a)
    \/ (a <> Asm.Plabel l /\ label_pos l (ofs + instr_size a) instrs = Some z).

Lemma update_instrs_map_pres_lmap_2 : forall instrs l id lmap lmap' csize csize',
    ~ In (Asm.Plabel l) instrs ->
    update_instrs lmap csize id instrs = (lmap',csize') ->
    lmap' id l = lmap id l.

Lemma update_instrs_cons:
  forall lmap csize id ins insns,
    update_instrs lmap csize id (ins::insns) =
    let (lmap',csize') := update_instr lmap csize id ins in
    update_instrs lmap' csize' id insns.

Lemma update_instrs_other_label:
  forall l id ins lmap csize lmap' csize',
    ~ In l (labels ins) ->
    update_instrs lmap csize id ins = (lmap',csize') ->
    lmap' id l = lmap id l.

Lemma update_instrs_map_lmap_inversion : forall instrs csize l z ofs id csize' lmap lmap' l'
    (MAXSIZE: csize' <= Ptrofs.max_unsigned)
    (MINSIZE: csize >= 0)
    (LNR: list_norepet (labels instrs))
    (LPOS: label_pos l ofs instrs = Some z)
    (UI: update_instrs lmap csize id instrs = (lmap', csize'))
    (LM: lmap' id l = Some l'),
    l' = (code_segid , Ptrofs.repr (csize + z - ofs)) /\ 0 <= (csize + z - ofs) <= Ptrofs.max_unsigned.

Lemma label_pos_min_size : forall instrs l ofs ofs',
    label_pos l ofs instrs = Some ofs' -> ofs <= ofs'.

Lemma size_fun_pos:
  forall o,
    0 <= size_fun o.

Lemma update_funs_map_lpos_inversion: forall defs id l f z gmap lmap csize dsize csize' dsize' gmap' lmap' l'
    (DDISTINCT : list_norepet (map fst defs))
    (LDISTINCT : list_norepet (labels (Asm.fn_code f)))
    (MAXSIZE : csize' <= Ptrofs.max_unsigned)
    (MINSIZE : csize >= 0)
    (AL: (alignw | csize)),
    In (id, Some (Gfun (Internal f))) defs ->
    label_pos l 0 (Asm.fn_code f) = Some z ->
    update_maps gmap lmap dsize csize defs = (gmap', lmap', dsize', csize') ->
    lmap' id l = Some l' ->
    (exists slbl : seglabel, gmap' id = Some slbl
                        /\ fst slbl = fst l'
                        /\ Ptrofs.add (snd slbl) (Ptrofs.repr z) = snd l').




Lemma update_map_lmap_inversion : forall id f gmap lmap dsize csize l z l',
    (dsize + csize) <= Ptrofs.max_unsigned ->
    list_norepet (map fst (AST.prog_defs prog)) ->
    list_norepet (labels (Asm.fn_code f)) ->
    In (id, Some (Gfun (Internal f))) (AST.prog_defs prog) ->
    make_maps prog = (gmap, lmap, dsize, csize) ->
    label_pos l 0 (Asm.fn_code f) = Some z ->
    lmap id l = Some l' ->
    exists slbl, gmap id = Some slbl /\
            fst slbl = fst l' /\
            Ptrofs.add (snd slbl) (Ptrofs.repr z) = snd l'.

End WITHTRANSF.




Section WITHMEMORYMODEL.
  
Context `{memory_model: Mem.MemoryModel }.
Existing Instance inject_perm_all.


Definition match_prog (p: Asm.program) (tp: FlatAsm.program) :=
  transf_program p = OK tp.

Section PRESERVATION.

Variable prog: Asm.program.
Variable tprog: FlatAsm.program.
Hypothesis TRANSF: match_prog prog tprog.

Let ge := Genv.globalenv prog.
Let tge := globalenv tprog.

Definition regset_inject (j:meminj) (rs rs' : regset) : Prop :=
  forall r, Val.inject j (rs r) (rs' r).

Record match_inj (mj: meminj) : Type :=
  mk_match_inj {

      agree_inj_instr : forall b b' f ofs ofs' i,
        Globalenvs.Genv.find_funct_ptr ge b = Some (Internal f) ->
        Asm.find_instr (Ptrofs.unsigned ofs) (Asm.fn_code f) = Some i ->
        mj b = Some (b', ofs') ->
        exists id i' sid ofs1,
          Genv.find_instr tge (Vptr b' (Ptrofs.add ofs (Ptrofs.repr ofs'))) = Some i' /\
          Globalenvs.Genv.find_symbol ge id = Some b /\
          transl_instr ofs1 id sid i = OK i';


      agree_inj_glob : forall id b,
          Globalenvs.Genv.find_symbol ge id = Some b ->
          exists b' ofs', Genv.find_symbol tge id = Some (b', ofs') /\
          mj b = Some (b', Ptrofs.unsigned ofs');

      agree_inj_lbl : forall id b f l z,
          Globalenvs.Genv.find_symbol ge id = Some b ->
          Globalenvs.Genv.find_funct_ptr ge b = Some (Internal f) ->
          label_pos l 0 (Asm.fn_code f) = Some z ->
          Val.inject mj (Vptr b (Ptrofs.repr z)) (Genv.label_address tge id l);
    }.



Definition valid_instr_offset_is_internal (mj:meminj) :=
  forall b b' f ofs i ofs',
    Globalenvs.Genv.find_funct_ptr ge b = Some (Internal f) ->
    find_instr (Ptrofs.unsigned ofs) (Asm.fn_code f) = Some i ->
    mj b = Some (b', ofs') ->
    Genv.genv_internal_codeblock tge b' = true.


Definition extfun_entry_is_external (mj:meminj) :=
  forall b b' f ofs,
    Globalenvs.Genv.find_funct_ptr ge b = Some (External f) ->
    mj b = Some (b', ofs) ->
    Genv.genv_internal_codeblock tge b' = false.


Definition def_frame_inj m := (flat_frameinj (length (Mem.stack m))).

Lemma store_pres_def_frame_inj : forall chunk m1 b ofs v m1',
    Mem.store chunk m1 b ofs v = Some m1' ->
    def_frame_inj m1 = def_frame_inj m1'.

Lemma storev_pres_def_frame_inj : forall chunk m1 v1 v2 m1',
    Mem.storev chunk m1 v1 v2 = Some m1' ->
    def_frame_inj m1= def_frame_inj m1'.


Lemma store_mapped_inject' :
  forall (f : meminj) (chunk : memory_chunk)
    (m1 : mem) (b1 : block) (ofs : Z) (v1 : val)
    (n1 m2 : mem) (b2 : block) (delta : Z) (v2 : val),
    Mem.inject f (def_frame_inj m1) m1 m2 ->
    Mem.store chunk m1 b1 ofs v1 = Some n1 ->
    f b1 = Some (b2, delta) ->
    Val.inject f v1 v2 ->
    exists n2 : mem,
      Mem.store chunk m2 b2 (ofs + delta) v2 = Some n2 /\
      Mem.inject f (def_frame_inj n1) n1 n2.

Theorem storev_mapped_inject':
  forall f chunk m1 a1 v1 n1 m2 a2 v2,
  Mem.inject f (def_frame_inj m1) m1 m2 ->
  Mem.storev chunk m1 a1 v1 = Some n1 ->
  Val.inject f a1 a2 ->
  Val.inject f v1 v2 ->
  exists n2,
    Mem.storev chunk m2 a2 v2 = Some n2 /\ Mem.inject f (def_frame_inj n1) n1 n2.

Definition match_find_funct (j:meminj) :=
  forall b f ofs b',
  Globalenvs.Genv.find_funct_ptr ge b = Some (External f) ->
  j b = Some (b', ofs) ->
  Genv.find_funct tge (Vptr b' (Ptrofs.repr ofs)) = Some (External f).

Definition glob_block_valid (m:mem) :=
  forall b g, Globalenvs.Genv.find_def ge b = Some g -> Mem.valid_block m b.

Inductive match_states: state -> state -> Prop :=
| match_states_intro: forall (j:meminj) (rs: regset) (m: mem) (rs': regset) (m':mem)
                        (MINJ: Mem.inject j (def_frame_inj m) m m')
                        (MATCHSMINJ: match_inj j)
                        (INSTRINTERNAL: valid_instr_offset_is_internal j)
                        (EXTEXTERNAL: extfun_entry_is_external j)
                        (MATCHFINDFUNCT: match_find_funct j)
                        (RSINJ: regset_inject j rs rs')
                        (GBVALID: glob_block_valid m),
    match_states (State rs m) (State rs' m').


Definition init_meminj : meminj :=
  let ge := Genv.globalenv prog in
  let tge := globalenv tprog in
  fun b =>
    if eq_block b (Globalenvs.Genv.genv_next ge)
    then Some (Genv.genv_next tge, 0)
    else
      match (Genv.invert_symbol ge b) with
      | None => None
      | Some id =>
        match Genv.find_symbol tge id with
        | None => None
        | Some (b,ofs) => Some (b, Ptrofs.unsigned ofs)
        end

      end.


Lemma in_transl_instrs:
  forall i si c o o' sz x1
    (RNG: 0 <= sz <= Ptrofs.max_unsigned)
    (POS: 0 <= o')
    (TI: transl_instrs i si o' c = OK (sz, x1))
    si'
    (IN: In (si', o) (map (fun i1 => (segblock_id (snd (fst i1)), segblock_start (snd (fst i1)))) x1)),
    si' = si /\ o' <= Ptrofs.unsigned o < o' + code_size c.


Lemma transl_instrs_diff_labels:
  forall i si c
    sz ofs c'
    (RNG: 0 <= sz <= Ptrofs.max_unsigned)
    (POS: 0 <= ofs)
    (TI : transl_instrs i si ofs c = OK (sz, c')),
    list_norepet (map (fun i1 => segblock_to_label (snd (fst i1))) c').

Lemma transl_globdef_distinct_code_labels:
  forall gmap i o p
    (TG : transl_globdef gmap i o = OK p),
    list_norepet (map (fun i0 => segblock_to_label (snd (fst i0))) (get_def_code p)).




Lemma in_transl_globdef:
  forall gmap i o p0
    (EQ : transl_globdef gmap i o = OK p0)
    x
    (IN: In x (map (fun i0 => segblock_to_label (snd (fst i0))) (get_def_code p0))),
    exists s,
      gmap i = Some s /\
      fst x = fst s /\ Ptrofs.unsigned (snd s) <= Ptrofs.unsigned (snd x) < Ptrofs.unsigned (snd s) + odef_size o.

Lemma in_transl_globdefs:
  forall gmap l gdefs
    (EQ : transl_globdefs gmap l = OK gdefs)
    x
    (IN: In x (map (fun i0 => segblock_to_label (snd (fst i0))) (get_defs_code gdefs))),
          exists i def s,
            In (i, def) l /\
            gmap i = Some s /\
            fst x = fst s /\ Ptrofs.unsigned (snd s) <= Ptrofs.unsigned (snd x) < Ptrofs.unsigned (snd s) + odef_size def.

Definition gmap_inj (gmap: GID_MAP_TYPE) (l: list (ident * option _)): Prop :=
  forall i1 i2 d1 d2 s1 s2 o1 o2,
    In (i1, d1) l ->
    In (i2, d2) l ->
    i1 <> i2 ->
    gmap i1 = Some (s1, o1) ->
    gmap i2 = Some (s2, o2) ->
    s1 <> s2 \/ Ptrofs.unsigned o1 + odef_size d1 <= Ptrofs.unsigned o2 \/ Ptrofs.unsigned o2 + odef_size d2 <= Ptrofs.unsigned o1.

Lemma gmap_inj_inv:
  forall gmap a b,
    gmap_inj gmap (a::b) ->
    gmap_inj gmap b.

Ltac ereplace t :=
  match type of t with
  | ?ty => let x := fresh in evar (x : ty); replace t with x; unfold x
  end.

Lemma transl_globdef_distinct_code_labels'
     : forall (gmap : GID_MAP_TYPE) (i : ident) (o : option (globdef Asm.fundef unit)) (p : ident * option gdef * segblock),
       transl_globdef gmap i o = OK p ->
       list_norepet (map (fun '(_,blk,_) => segblock_to_label blk) (get_def_code p)).

Lemma in_segblock_eq : forall a (c: list (instruction * segblock * ident)),
 In a (map (fun '(_, blk, _) => segblock_to_label blk) c) <->
 In a (map (fun i => segblock_to_label (snd (fst i))) c).

Lemma transl_globdefs_distinct_code_labels:
  forall gmap prog (GINJ: gmap_inj gmap (AST.prog_defs prog)) tgdefs,
    transl_globdefs gmap (AST.prog_defs prog) = OK tgdefs ->
    wf_prog prog ->
    code_labels_are_distinct (get_defs_code tgdefs).

Lemma update_maps_code_lt:
  forall defs g l d c g' l' d' c' i s
    (RNG: 0 <= c <= Ptrofs.max_unsigned)
    (RNG: 0 <= c' <= Ptrofs.max_unsigned)
    (UPDATE: update_maps g l d c defs = (g', l', d', c'))
    (AL: (alignw | c))
    (LNR: list_norepet (map fst defs))
    f
    (IN: In (i, Some (Gfun (Internal f))) defs)
    (BEFORE: g i = None)
    (AFTER: g' i = Some s),
    c <= Ptrofs.unsigned (snd s) /\ Ptrofs.unsigned (snd s) + code_size (Asm.fn_code f) <= c'.

Lemma update_maps_code_lt':
  forall defs g l d c g' l' d' c' i s
    (RNG: 0 <= c <= Ptrofs.max_unsigned)
    (RNG: 0 <= c' <= Ptrofs.max_unsigned)
    (UPDATE: update_maps g l d c defs = (g', l', d', c'))
    (AL: (alignw | c))
    (LNR: list_norepet (map fst defs))
    def
    (IN: In (i, def) defs)
    (BEFORE: g i = None)
    (GMAP: g' i = Some (code_segid, s)),
    c <= Ptrofs.unsigned s /\ Ptrofs.unsigned s + odef_size def <= c'.

Lemma update_maps_data_lt:
  forall defs g l d c g' l' d' c' i s
    (RNG: 0 <= d <= Ptrofs.max_unsigned)
    (RNG: 0 <= d' <= Ptrofs.max_unsigned)
    (UPDATE: update_maps g l d c defs = (g', l', d', c'))
    (LNR: list_norepet (map fst defs))
    gv
    (IN: In (i, Some (Gvar gv)) defs)
    (BEFORE: g i = None)
    (AFTER: g' i = Some s),
    d <= Ptrofs.unsigned (snd s) /\ Ptrofs.unsigned (snd s) + init_data_list_size (gvar_init gv) <= d'.

Lemma update_maps_data_lt':
  forall defs g l d c g' l' d' c' i s
    (RNG: 0 <= d <= Ptrofs.max_unsigned)
    (RNG: 0 <= d' <= Ptrofs.max_unsigned)
    (UPDATE: update_maps g l d c defs = (g', l', d', c'))
    (LNR: list_norepet (map fst defs))
    def
    (IN: In (i, def) defs)
    (BEFORE: g i = None)
    (GMAP: g' i = Some (data_segid, s)),
    d <= Ptrofs.unsigned s /\ Ptrofs.unsigned s + odef_size def <= d'.



Lemma norepet_unique:
  forall {A B} (f: A -> B) (l: list A)
    (LNR: list_norepet (map f l)) a b
    (INA: In a l) (INB: In b l) (EQ: f a = f b),
    a = b.

Definition sdef_is_var_or_internal_fun {F V: Type} (def: option (AST.globdef (AST.fundef F) V)) :=
  match def with
  | Some (Gvar _) => True
  | Some (Gfun (Internal f)) => True
  | _ => False
  end.

Lemma vit_dec : forall F V (def: option (AST.globdef (AST.fundef F) V)),
    {sdef_is_var_or_internal_fun def} + {~ (sdef_is_var_or_internal_fun def)}.

Lemma vit_false_inv: forall F V (def: option (AST.globdef (AST.fundef F) V)),
  ~ sdef_is_var_or_internal_fun def ->
  def = None \/ exists f, def = Some (Gfun (External f)).

Lemma update_map_gmap_some :
  forall (prog : Asm.program) (gmap : GID_MAP_TYPE) (lmap : LABEL_MAP_TYPE) (dsize csize : Z) (id : ident)
    defs gdefs def
    (VIT: sdef_is_var_or_internal_fun def)
    (UPDATE: make_maps prog = (gmap, lmap, dsize, csize))
    (BOUND: dsize + csize <= Ptrofs.max_unsigned)
    (LNR: list_norepet (map fst (AST.prog_defs prog)))
    (DEFS: (defs ++ (id, def) :: gdefs) = AST.prog_defs prog),
    exists slbl, gmap id = Some slbl
           /\ (forall id' def' slbl', In (id', def') defs -> (gmap id' = Some slbl') ->
                                 fst slbl' = fst slbl -> Ptrofs.unsigned (snd slbl') + odef_size def' <= Ptrofs.unsigned (snd slbl))
           /\ (forall id' def' slbl', In (id', def') gdefs -> (gmap id' = Some slbl') ->
                           fst slbl' = fst slbl -> Ptrofs.unsigned (snd slbl) + odef_size def <= Ptrofs.unsigned (snd slbl')).

Lemma make_maps_gmap_inj':
  forall prog0 g' l' d' c'
    (lnr : list_norepet (map fst (AST.prog_defs prog0)))
    (mm : make_maps prog0 = (g', l', d', c'))
    (bound: d' + c' <= Ptrofs.max_unsigned)
    l1 l2 l3 i1 i2 d1 d2 s1 s2 o1 o2
    (EQ: AST.prog_defs prog0 = l1 ++ (i1, d1) :: l2 ++ (i2, d2) :: l3)
    (G1 : g' i1 = Some (s1, o1))
    (G2 : g' i2 = Some (s2, o2)),
    s1 <> s2 \/ Ptrofs.unsigned o1 + odef_size d1 <= Ptrofs.unsigned o2 \/ Ptrofs.unsigned o2 + odef_size d2 <= Ptrofs.unsigned o1.

Lemma app_cons_assoc:
  forall {A} (l1: list A) a l2 b l3,
    (l1 ++ a :: l2) ++ b :: l3 = l1 ++ a :: l2 ++ b :: l3.


Lemma update_maps_gmap_inj:
  forall prog g' l' d' c'
    (lnr: list_norepet (map fst (AST.prog_defs prog)))
    (mm: make_maps prog = (g', l', d', c'))
    (bound: d' + c' <= Ptrofs.max_unsigned),
    gmap_inj g' (AST.prog_defs prog).


Lemma transl_prog_seg_code:
  forall gmap lmap dsize csize,
    transl_prog_with_map gmap lmap prog dsize csize = OK tprog ->
    segid (code_seg tprog) = code_segid.

Lemma transl_prog_seg_data:
  forall gmap lmap dsize csize,
    transl_prog_with_map gmap lmap prog dsize csize = OK tprog ->
    segid (data_seg tprog) = data_segid.


Lemma transl_fun_pres_stacksize : forall g i f f',
    transl_fun g i f = OK f' ->
    Asm.fn_stacksize f = fn_stacksize f'.

Lemma transl_prog_gmap : forall g l p p' dz sz,
  transl_prog_with_map g l p dz sz = OK p' -> glob_map p' = g.

Lemma transl_prog_lmap : forall g l p p' dz sz,
  transl_prog_with_map g l p dz sz = OK p' -> lbl_map p' = l.


Lemma transl_globdef_pres_index : forall gmap i o o' s i',
  transl_globdef gmap i o = OK (i', o', s) -> i' = i.

Lemma transl_globdefs_pres_index: forall defs gmap defs'
  (TL: transl_globdefs gmap defs = OK defs')
  (NPT: list_norepet (map fst (defs))),
  map fst defs = map (fun '(i,_,_) => i) defs'.

Lemma transl_globdefs_list_norepet: forall defs gmap defs'
  (TL: transl_globdefs gmap defs = OK defs')
  (NPT: list_norepet (map fst (defs))),
  list_norepet (map (fun '(i,_,_) => i) (defs')).

Lemma transl_prog_list_norepet : forall gmap lmap dsize csize
  (TL: transl_prog_with_map gmap lmap prog dsize csize = OK tprog)
  (NPT: list_norepet (map fst (AST.prog_defs prog))),
  list_norepet (map (fun '(i,_,_) => i) (prog_defs tprog)).


Lemma transl_globdefs_pres_def : forall defs g defs' i def
  (TL: transl_globdefs g defs = OK defs')
  (IN: In (i,def) defs),
  exists def' sb, In (i, def', sb) defs' /\ transl_globdef g i def = OK (i, def', sb).

Lemma transl_prog_pres_def : forall g l p dz cz p' i def
  (TL: transl_prog_with_map g l p dz cz = OK p')
  (IN: In (i,def) (AST.prog_defs p)),
  exists def' sb, In (i, def', sb) (prog_defs p') /\ transl_globdef g i def = OK (i, def', sb).

Lemma transl_globdefs_pres_def' : forall defs sdefs tdefs g i def gdefs
  (DEFSTAIL : defs ++ (i, def) :: gdefs = sdefs)
  (TL: transl_globdefs g sdefs = OK tdefs),
  exists defs' gdefs' def' sb,
    tdefs = defs' ++ (i, def', sb) :: gdefs'
    /\ transl_globdefs g defs = OK defs'
    /\ transl_globdef g i def = OK (i, def', sb)
    /\ transl_globdefs g gdefs = OK gdefs'.

Lemma transl_prog_pres_def' : forall defs gdefs g l p dz cz p' i def
  (DEFSTAIL : defs ++ (i, def) :: gdefs = (AST.prog_defs p))
  (TL: transl_prog_with_map g l p dz cz = OK p'),
  exists defs' gdefs' def' sb,
    (prog_defs p') = defs' ++ (i, def', sb) :: gdefs'
    /\ transl_globdefs g defs = OK defs'
    /\ transl_globdef g i def = OK (i, def', sb)
    /\ transl_globdefs g gdefs = OK gdefs'.

Lemma transl_globdefs_pres_non_def : forall defs g defs' i
  (TL: transl_globdefs g defs = OK defs')
  (IN: ~ In i (map fst defs)),
  ~ exists def sb, In (i, def, sb) defs'.

Lemma transl_prog_pres_non_def : forall g l p dz cz p' i
  (TL: transl_prog_with_map g l p dz cz = OK p')
  (IN: ~ In i (prog_defs_names p)),
  ~ exists def sb, In (i, def, sb) (prog_defs p').


Lemma update_maps_gmap_in : forall defs x def g l dz cz g' l' dz' cz'
                              (VIT: sdef_is_var_or_internal_fun def)
                              (NPT: list_norepet (map fst defs))
                              (IN: In (x, def) defs)
                              (UPD: update_maps g l dz cz defs = (g', l', dz', cz')),
    exists sid ofs, g' x = Some (sid, ofs).

Lemma find_symbol_exists : forall (x : ident) def
    (IN: In (x, def) (AST.prog_defs prog)),
    exists b ofs, Genv.find_symbol (globalenv tprog) x = Some (b, ofs).

Lemma find_symbol_to_gmap :
  forall (x : ident) def gmap lmap dz cz b ofs
    (IN: In (x, def) (AST.prog_defs prog))
    (FSYM: Genv.find_symbol (globalenv tprog) x = Some (b, ofs))
    (VI: sdef_is_var_or_internal_fun def)
    (MKMAP: make_maps prog = (gmap, lmap, dz, cz)),
  exists slbl, gmap x = Some slbl
          /\ b = gen_segblocks tprog (fst slbl)
          /\ ofs = snd slbl.

Lemma gmap_to_find_symbol:
  forall (x : ident) def gmap lmap dz cz slbl
    (IN: In (x, def) (AST.prog_defs prog))
    (VI: sdef_is_var_or_internal_fun def)
    (MKMAP: make_maps prog = (gmap, lmap, dz, cz))
    (GMAP: gmap x = Some slbl),
    Genv.find_symbol (globalenv tprog) x = Some (gen_segblocks tprog (fst slbl), snd slbl).
  

Lemma update_instrs_in_lbl : forall code p l cz id l' cz'
                               (IN: In p (labels code))
                               (UPI: update_instrs l cz id code = (l', cz')),
    exists sid ofs, l' id p = Some (sid, ofs).

Lemma update_maps_lmap_in : forall defs id f p g l dz cz g' l' dz' cz'
                              (NPT: list_norepet (map fst defs))
                              (IN: In (id, Some (Gfun (Internal f))) defs)
                              (INL: In p (labels (Asm.fn_code f)))
                              (UPD: update_maps g l dz cz defs = (g', l', dz', cz')),
    exists sid ofs, l' id p = Some (sid, ofs).

Lemma label_pos_in_fun : forall c l s z
  (LPOS: label_pos l s c = Some z),
  In l (labels c).

Theorem init_meminj_match_sminj :
    match_inj init_meminj.

Lemma find_symbol_some_pres: forall id b,
  Globalenvs.Genv.find_symbol ge id = Some b ->
  exists b' ofs', Genv.find_symbol tge id = Some (b', ofs')
             /\ init_meminj b = Some (b', Ptrofs.unsigned ofs').

  
Lemma alloc_pres_def_frame_inj : forall m1 lo hi m1' b,
    Mem.alloc m1 lo hi = (m1', b) ->
    def_frame_inj m1 = def_frame_inj m1'.


Definition partial_genv defs : Globalenvs.Genv.t Asm.fundef unit :=
  let emptyge := (Globalenvs.Genv.empty_genv Asm.fundef unit prog.(AST.prog_public)) in
  Globalenvs.Genv.add_globals emptyge defs.

Definition globs_meminj : meminj :=
  let ge := Genv.globalenv prog in
  let tge := globalenv tprog in
  fun b =>
      match (Genv.invert_symbol ge b) with
      | None => None
      | Some id =>
        match Genv.find_symbol tge id with
        | None => None
        | Some (b, ofs) => Some (b, Ptrofs.unsigned ofs)
        end
      end.



Lemma invert_add_global_genv_next : forall (F V: Type) (ge:Globalenvs.Genv.t F V) id def,
    Genv.invert_symbol (Genv.add_global ge (id, def)) (Globalenvs.Genv.genv_next ge) = Some id.

Lemma partial_genv_invert_symbol : forall defs id def,
    Genv.invert_symbol (partial_genv (defs ++ (id, def) :: nil)) (Globalenvs.Genv.genv_next (partial_genv defs)) = Some id.

Lemma partial_genv_find_symbol_eq : forall defs id def,
    Globalenvs.Genv.find_symbol (partial_genv (defs ++ (id, def) :: nil)) id = Some (Globalenvs.Genv.genv_next (partial_genv defs)).

Lemma partial_genv_find_symbol_neq : forall defs id id' def,
    id <> id' ->
    Globalenvs.Genv.find_symbol (partial_genv (defs ++ (id, def) :: nil)) id' = Globalenvs.Genv.find_symbol (partial_genv defs) id'.


Lemma partial_genv_find_symbol_inversion : forall defs x b,
  Globalenvs.Genv.find_symbol (partial_genv defs) x = Some b ->
  In x (map fst defs).

Lemma invert_symbol_add_global_none : forall defs id def b,
    ~In id (map fst defs) ->
    Genv.invert_symbol (Genv.add_global (partial_genv defs) (id, def)) b = None ->
    Genv.invert_symbol (partial_genv defs) b = None.

Lemma update_map_gmap_none :
  forall (prog : Asm.program) (gmap : GID_MAP_TYPE) (lmap : LABEL_MAP_TYPE) (dsize csize : Z) (id : ident) def
    (DEFSNAMES: list_norepet (map fst (AST.prog_defs prog)))
    (UPDATE: make_maps prog = (gmap, lmap, dsize, csize))
    (NVI: ~sdef_is_var_or_internal_fun def)
    (IN: In (id, def) (AST.prog_defs prog)),
    gmap id = None.




Definition fun_non_empty (def: AST.globdef Asm.fundef unit) : Prop :=
  match def with
  | Gfun (Internal f) =>
    (0 < length (Asm.fn_code f))%nat
  | _ => True
  end.

Definition defs_funs_non_empty (defs: list (ident * option (AST.globdef Asm.fundef unit))) : Prop :=
  Forall (fun '(id, def) =>
            match def with
            | None => True
            | Some def' => fun_non_empty def'
            end
         ) defs.

Lemma defs_funs_non_empty_cons_inv : forall a l,
  defs_funs_non_empty (a::l) -> defs_funs_non_empty l.

Lemma drop_perm_pres_def_frame_inj : forall m1 lo hi m1' b p,
    Mem.drop_perm m1 b lo hi p = Some m1' ->
    def_frame_inj m1 = def_frame_inj m1'.

Lemma transl_fun_inversion : forall gmap id f f',
    transl_fun gmap id f = OK f' ->
    exists slbl, gmap id = Some slbl /\ fn_range f' = mkSegBlock (fst slbl) (snd slbl) (Ptrofs.repr (Asm.code_size (Asm.fn_code f))).

Lemma partial_genv_invert_symbol_pres : forall defs id def b,
    ~ In id (map fst defs) ->
    b <> Globalenvs.Genv.genv_next (partial_genv defs) ->
    Genv.invert_symbol (partial_genv (defs ++ (id, def) :: nil)) b = Genv.invert_symbol (partial_genv defs) b.


Lemma advance_next_succ : forall {F V: Type} (defs: list (ident * option (globdef F V))) p,
  Genv.advance_next defs (Pos.succ p) = Pos.succ (Genv.advance_next defs p).

Lemma partial_genv_next : forall defs,
    Globalenvs.Genv.genv_next (partial_genv defs) = Pos.of_succ_nat (length defs).


Lemma partial_genv_next_succ : forall defs def,
    Globalenvs.Genv.genv_next (partial_genv (defs ++ def :: nil)) =
    Pos.succ (Globalenvs.Genv.genv_next (partial_genv defs)).

Lemma defs_names_distinct_not_in : forall(F V:Type) (defs:list (ident * option (AST.globdef F V))) id def gdefs,
    list_norepet (map fst (defs ++ (id, def) :: gdefs)) -> ~In id (map fst defs).

Lemma defs_names_distinct_prefix_neq : forall (F V:Type) (defs1: list (ident * option (AST.globdef F V)))
                                         id def defs2 id' def',
    list_norepet (map fst (defs1 ++ (id, def) :: defs2)) ->
    In (id', def') defs1 -> id <> id'.


Lemma find_symbol_add_globals_inversion :
  forall (F V:Type) (defs: list (ident * option (AST.globdef F V))) id r ge,
    Globalenvs.Genv.find_symbol (Globalenvs.Genv.add_globals ge defs) id = r ->
    (exists def, In (id, def) defs) \/ Globalenvs.Genv.find_symbol ge id = r.

Lemma find_symbol_inversion_1 : forall defs (x : ident) (b : block),
    Globalenvs.Genv.find_symbol (partial_genv defs) x = Some b -> exists def, In (x, def) defs.

Lemma find_symbol_inversion_2 : forall {F V} (prog:AST.program F V) (x : ident) (b : block),
    Globalenvs.Genv.find_symbol (Globalenvs.Genv.globalenv prog) x = Some b ->
    exists def, In (x, def) (AST.prog_defs prog).


Lemma store_zeros_mapped_inject:
  forall (f : meminj) (g : frameinj) (m1 : mem) (b1 : block) (ofs n : Z)
    (n1 m2 : mem) (b2 : block) (delta : Z),
    Mem.weak_inject f g m1 m2 ->
    store_zeros m1 b1 ofs n = Some n1 ->
    f b1 = Some (b2, delta) ->
    exists n2 : mem, store_zeros m2 b2 (ofs+delta) n = Some n2 /\ Mem.weak_inject f g n1 n2.

Lemma store_zeros_pres_def_frame_inj : forall m1 b lo hi m1',
    store_zeros m1 b lo hi = Some m1' ->
    def_frame_inj m1 = def_frame_inj m1'.

Lemma globs_meminj_pres_find_symbol:
  forall id b,
    Globalenvs.Genv.find_symbol ge id = Some b ->
    exists b' ofs', Genv.find_symbol tge id = Some (b', ofs') /\
               globs_meminj b = Some (b', Ptrofs.unsigned ofs').

Lemma store_init_data_list_mapped_inject_aux : forall v g m1 m1' m2 b1 b2 delta ofs,
    Mem.weak_inject globs_meminj g m1 m1' ->
    globs_meminj b1 = Some (b2, delta) ->
    Genv.store_init_data_list ge m1 b1 ofs v = Some m2 ->
    exists m2', store_init_data_list tge m1' b2 (ofs+delta) v = Some m2'
           /\ Mem.weak_inject globs_meminj g m2 m2'.

Lemma store_init_data_list_mapped_inject : forall g m1 m1' m2 (v:globvar unit) b1 b2 delta ofs,
    Mem.weak_inject globs_meminj g m1 m1' ->
    globs_meminj b1 = Some (b2, delta) ->
    Genv.store_init_data_list ge m1 b1 ofs (gvar_init v) = Some m2 ->
    exists m2', store_init_data_list tge m1' b2 (ofs+delta) (gvar_init v) = Some m2'
           /\ Mem.weak_inject globs_meminj g m2 m2'.

Lemma store_init_data_pres_def_frame_inj : forall m1 b1 ofs v m1',
    Genv.store_init_data ge m1 b1 ofs v = Some m1' ->
    def_frame_inj m1 = def_frame_inj m1'.

Lemma store_init_data_list_pres_def_frame_inj : forall gv m1 b1 ofs m1',
    Genv.store_init_data_list ge m1 b1 ofs gv = Some m1' ->
    def_frame_inj m1 = def_frame_inj m1'.


Lemma defs_names_distinct_not_in_tail : forall(F V:Type) (defs:list (ident * option (AST.globdef F V))) id def gdefs,
    list_norepet (map fst (defs ++ (id, def) :: gdefs)) -> ~In id (map fst gdefs).

Lemma genv_find_symbol_next : forall defs id def gdefs,
    list_norepet (map fst (AST.prog_defs prog)) ->
    AST.prog_defs prog = (defs ++ (id, def) :: gdefs) ->
    Globalenvs.Genv.find_symbol (Globalenvs.Genv.globalenv prog) id = Some (Globalenvs.Genv.genv_next (partial_genv defs)).


Lemma genv_invert_symbol_next : forall defs id def gdefs,
    list_norepet (map fst (AST.prog_defs prog)) ->
    AST.prog_defs prog = (defs ++ (id, def) :: gdefs) ->
    Genv.invert_symbol (Genv.globalenv prog) (Globalenvs.Genv.genv_next (partial_genv defs)) = Some id.

Definition aligned (ofs:Z) := forall chunk, (align_chunk chunk | ofs).

Lemma chunk_divides_alignw: forall chunk,
  (align_chunk chunk | alignw).

Lemma alignw_aligned : forall i,
  (alignw | i) -> aligned i.


Lemma update_map_gmap_aligned :
  forall defs gmap lmap dsize csize
    gmap1 lmap1 dsize1 csize1 slbl i
    (UPDATE: (gmap,lmap,dsize, csize) = update_maps gmap1 lmap1 dsize1 csize1 defs)
    (CSZALN: (alignw | csize1))
    (CSZBOUND: csize <= Ptrofs.max_unsigned)
    (CSZPOS: 0 <= csize1)
    (DSZALN: (alignw | dsize1))
    (DSZBOUND: dsize <= Ptrofs.max_unsigned)
    (DSZPOS: 0 <= dsize1)
    (GMAPALN: forall i' slbl', gmap1 i' = Some slbl' -> aligned (Ptrofs.unsigned (snd slbl')))
    (GMAP: gmap i = Some slbl),
    aligned (Ptrofs.unsigned (snd slbl)).

Lemma make_maps_sizes_pos :
  forall prog gmap lmap dsize csize,
    make_maps prog = (gmap, lmap, dsize, csize) ->
    dsize >= 0 /\ csize >= 0.

Lemma prog_odef_size_pos : forall defs id odef gdefs,
    defs ++ (id, odef) :: gdefs = AST.prog_defs prog ->
    def_not_empty odef.

Lemma make_maps_ofs_ordering :
  forall prog defs1 defs2 i1 i2 def1 def2 slbl1 slbl2
    gmap lmap dsize csize
    (SZMAX: dsize + csize <= Ptrofs.max_unsigned)
    (NORPT: list_norepet (map fst (AST.prog_defs prog)))
    (DEFS: AST.prog_defs prog = defs1 ++ defs2)
    (UPDATE: (gmap, lmap, dsize, csize) = make_maps prog)
    (IN1: In (i1, def1) defs1)
    (IN2: In (i2, def2) defs2)
    (GMAP1: gmap i1 = Some slbl1)
    (GMAP2: gmap i2 = Some slbl2)
    (SAMESEG: fst slbl1 = fst slbl2),
    odef_size def1 + Ptrofs.unsigned (snd slbl1) <= Ptrofs.unsigned (snd slbl2).

Lemma code_size_upper_bound':
  forall defs gmap lmap dsize csize id f
    gmap1 lmap1 dsize1 csize1
    (CZPOS: 0 <= csize1)
    (UPDATE: update_maps gmap1 lmap1 dsize1 csize1 defs = (gmap, lmap, dsize, csize))
    (IN: In (id, Some (Gfun (Internal f))) defs),
    code_size (Asm.fn_code f) <= csize.

Lemma code_size_upper_bound:
  forall defs prog gmap lmap dsize csize id f gdefs
    (MAKEMAPS: make_maps prog = (gmap, lmap, dsize, csize))
    (PROG: defs ++ (id, Some (Gfun (Internal f))) :: gdefs = AST.prog_defs prog),
    code_size (Asm.fn_code f) <= csize.

Lemma transf_prog_code_size_pos: forall prog tprog id f
    (TRANSF: transf_program prog = OK tprog)
    (IN: In (id, Some (Gfun (Internal f))) (AST.prog_defs prog)),
    0 < Asm.code_size (Asm.fn_code f).


Lemma globs_meminj_domain_valid : forall gmap lmap dsize csize m2 b p
    (UPDATE: make_maps prog = (gmap, lmap, dsize, csize))
    (ALLOCG: Genv.alloc_globals ge Mem.empty (AST.prog_defs prog) = Some m2)
    (TRANSPROG: transl_prog_with_map gmap lmap prog dsize csize = OK tprog)
    (INJ: globs_meminj b = Some p),
    Mem.valid_block m2 b.

Lemma Nth_len : forall {A:Type} l1 (x:A) l2, Nth (length l1) (l1 ++ x :: l2) x.

Lemma transl_prog_pres_nvi :
  forall def i
    (NVI: ~sdef_is_var_or_internal_fun def)
    (IN: In (i, def) (AST.prog_defs prog)),
  exists n def' sb, def_is_none_or_external_fun (i, def', sb) /\ Nth n (prog_defs tprog) (i, def', sb).

Lemma find_symbol_nvi_lower_bound :
  forall def i b ofs
    (NVI: ~sdef_is_var_or_internal_fun def)
    (IN: In (i, def) (AST.prog_defs prog))
    (FSYM: Genv.find_symbol (globalenv tprog) i = Some (b, ofs)),
    Ple (pos_advance_N init_block (length (list_of_segments tprog))) b.
  
Lemma transl_globdefs_pres_len : forall g defs defs'
    (TL: transl_globdefs g defs = OK defs'),
    length defs = length defs'.

Lemma transl_prog_pres_len : forall g l p p' dz cz
    (TL: transl_prog_with_map g l p dz cz = OK p'),
    length (prog_defs p') = length (AST.prog_defs p).


Lemma transl_prog_pres_nvi' :
  forall defs def gdefs i
    (DEFSTAIL : defs ++ (i, def) :: gdefs = AST.prog_defs prog)
    (NVI: ~sdef_is_var_or_internal_fun def),
  exists def' sb, def_is_none_or_external_fun (i, def', sb) /\ Nth (length defs) (prog_defs tprog) (i, def', sb).

Lemma find_symbol_nvi_eq:
  forall defs i def gdefs
    (DEFSTAIL : defs ++ (i, def) :: gdefs = AST.prog_defs prog)
    (NVIT: ~sdef_is_var_or_internal_fun def)
    (NPT: list_norepet (map (fun '(i, _) => i) (AST.prog_defs prog))),
            Genv.find_symbol (globalenv tprog) i = Some (pos_advance_N (Pos.of_succ_nat num_segments) (length defs), Ptrofs.zero).

Lemma pos_advance_N_succ_base : forall n,
    pos_advance_N 1 n = Pos.of_succ_nat n.

Lemma pos_advance_N_succ_commut:
  forall n1 n2,
    pos_advance_N (Pos.of_succ_nat n1) n2 = pos_advance_N (Pos.of_succ_nat n2) n1.

Lemma pos_advance_N_plt : forall p n,
  (0 < n)%nat -> Plt p (pos_advance_N p n).

Lemma pos_advande_N_plt_mono: forall n1 n2 b,
  (n1 < n2)%nat -> Plt (pos_advance_N b n1) (pos_advance_N b n2).

Lemma pos_advance_N_plt_add:
  forall b n1 n2, Plt (pos_advance_N b n1) (pos_advance_N b (n1+(Datatypes.S n2))).

Lemma pos_advande_N_ple_mono: forall n1 n2 b,
  (n1 <= n2)%nat -> Ple (pos_advance_N b n1) (pos_advance_N b n2).


Lemma pos_advance_N_ple_add:
  forall b n1 n2, Ple (pos_advance_N b n1) (pos_advance_N b (n1+n2)).


Lemma partial_genv_genv_next_bound:
  forall defs def gdefs prog i
    (DEFSTAIL: defs ++ (i, def) :: gdefs = AST.prog_defs prog),
    Plt (pos_advance_N (Globalenvs.Genv.genv_next (partial_genv defs)) num_segments)
        (pos_advance_N init_block (length (list_of_segments tprog) + length (AST.prog_defs prog))).

Lemma find_symbol_sb_vit : forall i odef sid ofs
    (IN: In (i, odef) (AST.prog_defs prog))
    (FSYM: Genv.find_symbol (globalenv tprog) i = Some (gen_segblocks tprog sid, ofs)),
    (sdef_is_var_or_internal_fun odef).



Lemma app_same_len_prefix : forall {A:Type} (l1:list A) l2 x l1' l2' x',
    length l1 = length l1' ->
    l1 ++ x :: l2 = l1' ++ x':: l2' ->
    x = x'.

Lemma zero_le_ptrofs_max: (0 <= Ptrofs.max_unsigned).

Lemma four_le_suc_len :
  forall {A:Type} (defs: list A),
    (4 <= Pos.succ (Pos.succ (Pos.succ (Pos.of_succ_nat (length defs)))))%positive.

Lemma store_globals_inject :
  forall gdefs tgdefs defs m1 m2 m1' gmap lmap dsize csize
    (DEFNAMES: list_norepet (map fst (AST.prog_defs prog)))
    (DEFSTAIL: defs ++ gdefs = AST.prog_defs prog)
    (UPDATE: make_maps prog = (gmap, lmap, dsize, csize))
    (BOUND: dsize + csize <= Ptrofs.max_unsigned)
    (TRANSPROG: transl_prog_with_map gmap lmap prog dsize csize = OK tprog)
    (TRANSG: transl_globdefs gmap gdefs = OK tgdefs)
    (MINJ: Mem.weak_inject globs_meminj (def_frame_inj m1) m1 m1')
    (ALLOCG: Genv.alloc_globals ge m1 gdefs = Some m2)
    (BLOCKEQ : Mem.nextblock m1 = Globalenvs.Genv.genv_next (partial_genv defs))
    (BLOCKEQ' : Mem.nextblock m1' = (pos_advance_N init_block (length (list_of_segments tprog) + length (AST.prog_defs prog))))
    (STK' : Mem.stack m1' = nil)
    (PERMOFS : forall b ofs k p, Mem.perm m1' b ofs k p -> 0 <= ofs < Ptrofs.max_unsigned)
    (OFSBOUND: forall id b def ofs k p,
        Globalenvs.Genv.find_symbol (partial_genv defs) id = Some b ->
        In (id, def) defs -> Mem.perm m1 b ofs k p ->
        ofs < odef_size def)
    (FINDVALIDSYM: forall id b ofs k p,
       Globalenvs.Genv.find_symbol ge id = Some b ->
       Mem.perm m1 b ofs k p ->
       Globalenvs.Genv.find_symbol (partial_genv defs) id = Some b)
    (DEFSPERM: forall id odef b' delta,
       In (id, odef) gdefs ->
       Genv.find_symbol tge id = Some (b', delta) ->
       (forall ofs k p, 0 <= ofs < odef_size odef -> Mem.perm m1' b' (Ptrofs.unsigned delta+ofs) k p)),
    exists m2', store_globals_iter tge (length defs) (gen_segblocks tprog) m1' tgdefs = Some m2'
           /\ Mem.weak_inject globs_meminj (def_frame_inj m2) m2 m2'.



Lemma store_all_globals_inject :
  forall tgdefs m2 m1' gmap lmap dsize csize
    (DEFNAMES: list_norepet (map fst (AST.prog_defs prog)))
    (UPDATE: make_maps prog = (gmap, lmap, dsize, csize))
    (TRANSPROG: transl_prog_with_map gmap lmap prog dsize csize = OK tprog)
    (TRANSG: transl_globdefs gmap (AST.prog_defs prog) = OK tgdefs)
    (BOUND: dsize + csize <= Ptrofs.max_unsigned)
    (MINJ: Mem.weak_inject globs_meminj (def_frame_inj Mem.empty) Mem.empty m1')
    (BLOCKEQ: Mem.nextblock m1' = (pos_advance_N init_block (length (list_of_segments tprog) + length (AST.prog_defs prog))))
    (STK: Mem.stack m1' = nil)
    (PERMOFS : forall b ofs k p, Mem.perm m1' b ofs k p -> 0 <= ofs < Ptrofs.max_unsigned)
    (DEFSPERM: forall id odef b' delta,
       In (id, odef) (AST.prog_defs prog) ->
       Genv.find_symbol tge id = Some (b', delta) ->
       (forall ofs k p, 0 <= ofs < odef_size odef -> Mem.perm m1' b' ((Ptrofs.unsigned delta)+ofs) k p))
    (ALLOCG: Genv.alloc_globals ge Mem.empty (AST.prog_defs prog) = Some m2),
    exists m2',store_globals tge (gen_segblocks tprog) m1' tgdefs = Some m2'
           /\ Mem.inject globs_meminj (def_frame_inj m2) m2 m2'.

Lemma globs_meminj_ofs_pos : forall b b' delta,
    globs_meminj b = Some (b', delta) -> delta >= 0.

Lemma alloc_global_exists: forall I (def: (ident * option (@gdef I) * segblock)) m,
    exists m', alloc_global m def = Some m'.

Lemma alloc_globals_exists: forall I (defs: list (ident * option (@gdef I) * segblock)) m,
    exists m', alloc_globals m defs = Some m'.


Lemma alloc_globals_segments_weak_inject: forall gmap lmap dsize csize m
    (UPDATE: make_maps prog = (gmap, lmap, dsize, csize))
    (TRANSPROG: transl_prog_with_map gmap lmap prog dsize csize = OK tprog)
    (NEXTBLOCK: Mem.nextblock m = init_block)
    (STACK: Mem.stack m = nil),
    exists m',
      alloc_globals (alloc_segments m (list_of_segments tprog)) (prog_defs tprog) = Some m'
      /\ Mem.weak_inject globs_meminj (def_frame_inj Mem.empty) Mem.empty m'.


Definition find_segsize (segs: list segment) id : option ptrofs :=
  match (List.find (fun s => ident_eq (segid s) id) segs) with
  | None => None
  | Some s => Some (segsize s)
  end.

Definition gen_segs dsize csize : list segment :=
  (mkSegment data_segid (Ptrofs.repr dsize))
    :: (mkSegment code_segid (Ptrofs.repr csize))
    :: nil.

Lemma update_maps_gmap_ofs_le_segsize :
  forall defs (gmap : GID_MAP_TYPE) (lmap : LABEL_MAP_TYPE) (dsize csize : Z) (id : ident)
    def slbl
    gmap1 lmap1 dsize1 csize1
    (DZLBND: dsize1 >= 0)
    (DZUBND: dsize <= Ptrofs.max_unsigned)
    (CZALNG: (alignw | csize1))
    (CZLBND: csize1 >= 0)
    (CZUBND: csize <= Ptrofs.max_unsigned)
    (UPDATE: update_maps gmap1 lmap1 dsize1 csize1 defs = (gmap, lmap, dsize, csize))
    (NORPT: list_norepet (map fst defs))
    (VI: sdef_is_var_or_internal_fun (Some def))
    (IN: In (id, Some def) defs)
    (GMAP: gmap id = Some slbl),
    exists sz, find_segsize (gen_segs dsize csize) (fst slbl) = Some sz /\
          (Ptrofs.unsigned (snd slbl)) + (def_size def) <= Ptrofs.unsigned sz.

Lemma transl_prog_segs : forall gmap lmap prog dsize csize tprog,
    transl_prog_with_map gmap lmap prog dsize csize = OK tprog ->
    list_of_segments tprog = gen_segs dsize csize.
 
Lemma make_maps_gmap_ofs_le_segsize :
  forall (gmap : GID_MAP_TYPE) (lmap : LABEL_MAP_TYPE) (dsize csize : Z) (id : ident)
    def slbl
    (UPDATE: make_maps prog = (gmap, lmap, dsize, csize))
    (VI: sdef_is_var_or_internal_fun (Some def))
    (IN: In (id, Some def) (AST.prog_defs prog))
    (GMAP: gmap id = Some slbl),
    exists sz, find_segsize (list_of_segments tprog) (fst slbl) = Some sz /\
          (Ptrofs.unsigned (snd slbl)) + (def_size def) <= Ptrofs.unsigned sz.

Lemma alloc_segments_pres_perm: forall segs m b m' ofs k p
  (ALLOCSEGS: m' = alloc_segments m segs)
  (PERM: Mem.perm m b ofs k p),
  Mem.perm m' b ofs k p.
      
Lemma alloc_segments_acc_segblocks_perm : forall segs m m' sid sz k p ofs smap
    (ALLOCSEGS: m' = alloc_segments m segs)
    (FINDSZ: find_segsize segs sid = Some sz)
    (SMAP: smap = acc_segblocks (Mem.nextblock m) (map segid segs) (fun id => undef_seg_block))
    (OFSBND: 0 <= ofs < Ptrofs.unsigned sz),
    Mem.perm m' (smap sid) ofs k p.

Lemma alloc_segments_init_perm :
  forall id odef b' delta ofs k p m
    (IN: In (id, odef) (AST.prog_defs prog))
    (VI: sdef_is_var_or_internal_fun odef)
    (FSYM: Genv.find_symbol tge id = Some (b', delta))
    (NB: Mem.nextblock m = init_block)
    (OFS: 0 <= ofs < odef_size odef),
    Mem.perm (alloc_segments m (list_of_segments tprog)) b' ((Ptrofs.unsigned delta)+ofs) k p.

Definition odef_size' {I:Type} (def: (ident * option (@gdef I) * segblock)) : Z :=
  let '(id, def', sb) := def in
  match def' with
  | None => 0
  | Some (Gfun (External f)) => 1
  | Some _ => Ptrofs.unsigned (segblock_size sb)
  end.

Lemma alloc_globals_ne_perm :
  forall (I:Type) defs def' n m m' ofs k p
    (NE: def_is_none_or_external_fun def')
    (NTH: Nth n defs def')
    (ALLOC: alloc_globals m defs = Some m')
    (OFS: 0 <= ofs < @odef_size' I def'),
    Mem.perm m' (pos_advance_N (Mem.nextblock m) n) ofs k p.


Lemma transl_prog_pres_odef_size :
  forall odef g id odef'
    (TL: transl_globdef g id odef = OK odef')
    (BND: odef_size odef <= Ptrofs.max_unsigned),
    odef_size odef = odef_size' odef'.
    

Lemma transl_prog_pres_nvi'' :
  forall odef g id def' sb
    (NVI: ~sdef_is_var_or_internal_fun odef)
    (TL: transl_globdef g id odef = OK (id, def', sb)),
    def_is_none_or_external_fun (id, def', sb).

Lemma size_gvar_pos:
  forall v, 0 <= size_gvar v.

Lemma size_gvar_bound :
  forall defs id v
    (IN: In (id, Some (Gvar v)) defs),
    size_gvar (Some (Gvar v)) <= sizes_gvars (defs).

Lemma odef_size_bound :
  forall g l dz cz id odef
    (MP: make_maps prog = (g, l, dz, cz))
    (BND: dz + cz <= Ptrofs.max_unsigned)
    (IN: In (id, odef) (AST.prog_defs prog)),
    odef_size odef <= Ptrofs.max_unsigned.

Lemma alloc_globals_init_perm :
  forall id odef b' delta ofs k p m m'
    (IN: In (id, odef) (AST.prog_defs prog))
    (NVI: ~ sdef_is_var_or_internal_fun odef)
    (FSYM: Genv.find_symbol tge id = Some (b', delta))
    (OFS: 0 <= ofs < odef_size odef)
    (NB: Mem.nextblock m = Pos.of_succ_nat num_segments)
    (GALLOC: alloc_globals m (prog_defs tprog) = Some m'),
    Mem.perm m' b' ((Ptrofs.unsigned delta)+ofs) k p.
    

Lemma init_mem_pres_inject : forall m gmap lmap dsize csize
    (UPDATE: make_maps prog = (gmap, lmap, dsize, csize))
    (TRANSPROG: transl_prog_with_map gmap lmap prog dsize csize = OK tprog)
    (INITMEM: Genv.init_mem prog = Some m),
    exists m', init_mem tprog = Some m' /\ Mem.inject globs_meminj (def_frame_inj m) m m'.


Lemma push_new_stage_def_frame_inj : forall m,
    def_frame_inj (Mem.push_new_stage m) = (1%nat :: def_frame_inj m).

Definition find_symbol_block_bound (ge:FlatAsm.genv) :=
  forall id b ofs, Genv.find_symbol ge id = Some (b, ofs) -> Pos.lt b (Genv.genv_next ge).

Lemma add_global_pres_find_symbol_block_bound: forall ge def,
  find_symbol_block_bound ge -> find_symbol_block_bound (add_global ge def).

Lemma add_globals_pres_find_symbol_block_bound: forall defs ge,
  find_symbol_block_bound ge -> find_symbol_block_bound (add_globals ge defs).


Lemma find_symbol_globenv_block_bound :
  forall (id : ident) b ofs, Genv.find_symbol (globalenv tprog) id = Some (b, ofs)
                        -> Pos.lt b (Genv.genv_next (globalenv tprog)).

Lemma init_meminj_genv_next_inv : forall b delta
    (MINJ: init_meminj b = Some (Genv.genv_next tge, delta)),
    b = Globalenvs.Genv.genv_next ge.





Lemma update_map_funct':
  forall gmap lmap dsize csize f i s,
    make_maps prog = (gmap, lmap, dsize, csize) ->
    list_norepet (map fst (AST.prog_defs prog)) ->
    In (i, Some (Gfun (Internal f))) (AST.prog_defs prog) ->
    gmap i = Some s ->
    fst s = code_segid.

Lemma update_map_funct:
  forall gmap lmap dsize csize b f i s,
    make_maps prog = (gmap, lmap, dsize, csize) ->
    list_norepet (map fst (AST.prog_defs prog)) ->
    Globalenvs.Genv.find_funct_ptr ge b = Some (Internal f) ->
    Genv.invert_symbol ge b = Some i ->
    gmap i = Some s ->
    fst s = code_segid.


Lemma gen_segblocks_code_map : forall g l p dz cz p'
                                 (TL: transl_prog_with_map g l p dz cz = OK p'),
    gen_segblocks p' code_segid = code_block.

Lemma gidmap_symbmap_internal_block:
  forall gmap lmap dsize csize b b' f i ofs,
    make_maps prog = (gmap, lmap, dsize, csize) ->
    transl_prog_with_map gmap lmap prog dsize csize = OK tprog ->
    list_norepet (map fst (AST.prog_defs prog)) ->
    Globalenvs.Genv.find_funct_ptr ge b = Some (Internal f) ->
    Genv.invert_symbol ge b = Some i ->
    gidmap_to_symbmap (gen_segblocks tprog) (glob_map tprog) i = Some (b',ofs) ->
    b' = code_block.


Lemma find_symbol_internal_block:
  forall gmap lmap dsize csize b b' f i ofs
    (MK: make_maps prog = (gmap, lmap, dsize, csize))
    (TL: transl_prog_with_map gmap lmap prog dsize csize = OK tprog)
    (NPT: list_norepet (map fst (AST.prog_defs prog)))
    (FPTR: Globalenvs.Genv.find_funct_ptr ge b = Some (Internal f))
    (INVS: Globalenvs.Genv.invert_symbol ge b = Some i)
    (FSYM: Genv.find_symbol tge i = Some (b',ofs)),
    b' = code_block.

Lemma valid_instr_offset_is_internal_init:
  list_norepet (map fst (AST.prog_defs prog)) ->
  valid_instr_offset_is_internal init_meminj.

Fixpoint filter_map {A B: Type} (f: A -> option B) (l: list A): list B :=
  match l with
    nil => nil
  | a::r => match f a with
             Some b => b :: filter_map f r
           | None => filter_map f r
           end
  end.

Lemma in_filter_map_iff {A B} (f: A -> option B) : forall l x,
    In x (filter_map f l) <-> (exists y, f y = Some x /\ In y l).

Lemma filter_map_ext:
  forall {A B} (f g: A -> option B) (EXT: forall x, f x = g x) l,
    filter_map f l = filter_map g l.

Lemma list_norepet_filter_map:
  forall {A B} (f: A -> option B) a l,
    list_norepet (filter_map f (a::l)) ->
    list_norepet (filter_map f l).


Lemma external_in_defs_inversion : forall defs f sb i (ge:FlatAsm.genv)
  (NPT: list_norepet (map (fun '(i, _, _) => i) defs))
  (IN: In (i, Some (Gfun (External f)), sb) defs),
  exists b o,
    Genv.find_symbol (add_globals ge defs) i = Some (b, o) /\
    Genv.find_def (add_globals ge defs) b o = Some (Gfun (External f)).
      

Lemma external_in_prog_defs_inversion : forall f sb i
  (NPT: list_norepet (map (fun '(i, _, _) => i) (prog_defs tprog)))
  (IN: In (i, Some (Gfun (External f)), sb) (prog_defs tprog)),
  exists b o,
    Genv.find_symbol (globalenv tprog) i = Some (b, o) /\
    Genv.find_def (globalenv tprog) b o = Some (Gfun (External f)).
  

Lemma external_find_symbol_det : forall defs (ge:FlatAsm.genv) i b1 b2 o1 o2 f sb
  (IN: In (i, Some (Gfun (External f)), sb) defs)
  (NPT: list_norepet (map (fun '(i, _, _) => i) defs))
  (FINSYM1: Genv.find_symbol (add_globals ge defs) i = Some (b1, o1))
  (FINSYM2: Genv.find_symbol (add_globals ge defs) i = Some (b2, o2)),
  b1 = b2 /\ o1 = o2.


Lemma external_find_symbol_det' : forall i b1 b2 o1 o2 f sb
  (IN: In (i, Some (Gfun (External f)), sb) (prog_defs tprog))
  (NPT: list_norepet (map (fun '(i, _, _) => i) (prog_defs tprog)))
  (FINSYM1: Genv.find_symbol (globalenv tprog) i = Some (b1, o1))
  (FINSYM2: Genv.find_symbol (globalenv tprog) i = Some (b2, o2)),
  b1 = b2 /\ o1 = o2.

Lemma extfun_transf:
  forall gmap lmap dsize csize
    (TL: transl_prog_with_map gmap lmap prog dsize csize = OK tprog)
    (NPT: list_norepet (map fst (AST.prog_defs prog))),
    forall b b' f ofs
      (FFP : Globalenvs.Genv.find_funct_ptr ge b = Some (External f))
      (JB: init_meminj b = Some (b', ofs)),
      Genv.find_funct tge (Vptr b' (Ptrofs.repr ofs)) = Some (External f).


Lemma add_globals_find_symbol_external: forall defs i f sb b ofs (ge:FlatAsm.genv)
     (NPT: list_norepet (map (fun '(i, _, _) => i) defs))
     (IN: In (i, Some (Gfun (External f)), sb) defs)
     (GNXT: Pos.lt (Pos.of_nat num_segments) (Genv.genv_next ge))
     (FSYM: Genv.find_symbol (add_globals ge defs) i = Some (b, ofs)),
     Pos.lt (Pos.of_nat num_segments) b.

Lemma find_symbol_external_block:
  forall gmap lmap dsize csize b b' f i ofs
    (MK: make_maps prog = (gmap, lmap, dsize, csize))
    (TL: transl_prog_with_map gmap lmap prog dsize csize = OK tprog)
    (NPT: list_norepet (map fst (AST.prog_defs prog)))
    (FPTR: Globalenvs.Genv.find_funct_ptr ge b = Some (External f))
    (INVS: Globalenvs.Genv.invert_symbol ge b = Some i)
    (FSYM: Genv.find_symbol tge i = Some (b',ofs)),
    b' <> code_block.
  
Lemma extfun_entry_is_external_init:
  list_norepet (map fst (AST.prog_defs prog)) ->
  extfun_entry_is_external init_meminj.


  

Lemma transl_prog_pres_main_id : forall gmap lmap prog dsize csize tprog,
    transl_prog_with_map gmap lmap prog dsize csize = OK tprog ->
    AST.prog_main prog = prog_main tprog.


Lemma symbol_address_inject : forall j id ofs
                                (MATCHINJ: match_inj j),
    Val.inject j (Senv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs).

Lemma main_ptr_inject:
  forall gmap lmap dsize csize
    (MATCH_INJ: match_inj init_meminj)
    (MAKEMAPS: make_maps prog = (gmap, lmap, dsize, csize))
    (TRANSL: transl_prog_with_map gmap lmap prog dsize csize = OK tprog),
    Val.inject init_meminj
               (Globalenvs.Genv.symbol_address
                  (Globalenvs.Genv.globalenv prog)
                  (AST.prog_main prog) Ptrofs.zero)
               (Genv.symbol_address
                  (globalenv tprog)
                  (prog_main tprog) Ptrofs.zero).



Lemma transf_initial_states : forall rs (SELF: forall j, forall r : PregEq.t, Val.inject j (rs r) (rs r)) st1,
    RealAsm.initial_state prog rs st1 ->
    exists st2, FlatAsm.initial_state tprog rs st2 /\ match_states st1 st2.


Context `{external_calls_ops : !ExternalCallsOps mem }.
Context `{!EnableBuiltins mem}.
Existing Instance Asm.mem_accessors_default.
Existing Instance FlatAsm.mem_accessors_default.

Lemma eval_builtin_arg_inject : forall j m m' rs rs' sp sp' arg varg
    (MATCHINJ: match_inj j)
    (MINJ: Mem.inject j (def_frame_inj m) m m')
    (RSINJ: regset_inject j rs rs')
    (VINJ: Val.inject j sp sp')
    (EVALBI: eval_builtin_arg ge rs sp m arg varg),
    exists varg', FlatAsmBuiltin.eval_builtin_arg _ _ _ _ tge rs' sp' m' arg varg' /\
             Val.inject j varg varg'.
   

Lemma eval_builtin_args_inject : forall j m m' rs rs' sp sp' args vargs
    (MATCHINJ: match_inj j)
    (MINJ: Mem.inject j (def_frame_inj m) m m')
    (RSINJ: regset_inject j rs rs')
    (VINJ: Val.inject j sp sp')
    (EVALBI: eval_builtin_args ge rs sp m args vargs),
    exists vargs', FlatAsmBuiltin.eval_builtin_args _ _ _ _ tge rs' sp' m' args vargs' /\
             Val.inject_list j vargs vargs'.

Lemma extcall_arg_inject : forall rs1 rs2 m1 m2 l arg1 j,
    extcall_arg rs1 m1 l arg1 ->
    Mem.inject j (def_frame_inj m1) m1 m2 ->
    regset_inject j rs1 rs2 ->
    exists arg2,
      Val.inject j arg1 arg2 /\
      extcall_arg rs2 m2 l arg2.

Lemma extcall_arg_pair_inject : forall rs1 rs2 m1 m2 lp arg1 j,
    extcall_arg_pair rs1 m1 lp arg1 ->
    Mem.inject j (def_frame_inj m1) m1 m2 ->
    regset_inject j rs1 rs2 ->
    exists arg2,
      Val.inject j arg1 arg2 /\
      extcall_arg_pair rs2 m2 lp arg2.

Lemma extcall_arguments_inject_aux : forall rs1 rs2 m1 m2 locs args1 j,
   list_forall2 (extcall_arg_pair rs1 m1) locs args1 ->
    Mem.inject j (def_frame_inj m1) m1 m2 ->
    regset_inject j rs1 rs2 ->
    exists args2,
      Val.inject_list j args1 args2 /\
      list_forall2 (extcall_arg_pair rs2 m2) locs args2.

Lemma extcall_arguments_inject : forall rs1 rs2 m1 m2 ef args1 j,
    Asm.extcall_arguments rs1 m1 (ef_sig ef) args1 ->
    Mem.inject j (def_frame_inj m1) m1 m2 ->
    regset_inject j rs1 rs2 ->
    exists args2,
      Val.inject_list j args1 args2 /\
      Asm.extcall_arguments rs2 m2 (ef_sig ef) args2.

Axiom external_call_inject : forall ge j vargs1 vargs2 m1 m2 m1' vres1 t ef,
    Val.inject_list j vargs1 vargs2 ->
    Mem.inject j (def_frame_inj m1) m1 m2 ->
    external_call ef ge vargs1 m1 t vres1 m1' ->
    exists j' vres2 m2',
      external_call ef ge vargs2 m2 t vres2 m2' /\
      Val.inject j' vres1 vres2 /\ Mem.inject j' (def_frame_inj m1') m1' m2' /\
      inject_incr j j' /\
      inject_separated j j' m1 m2.

Axiom external_call_valid_block: forall ef ge vargs m1 t vres m2 b,
    external_call ef ge vargs m1 t vres m2 -> Mem.valid_block m1 b -> Mem.valid_block m2 b.

Lemma extcall_pres_glob_block_valid : forall ef ge vargs m1 t vres m2,
  external_call ef ge vargs m1 t vres m2 -> glob_block_valid m1 -> glob_block_valid m2.

Lemma regset_inject_incr : forall j j' rs rs',
    regset_inject j rs rs' ->
    inject_incr j j' ->
    regset_inject j' rs rs'.

Lemma undef_regs_pres_inject : forall j rs rs' regs,
  regset_inject j rs rs' ->
  regset_inject j (Asm.undef_regs regs rs) (Asm.undef_regs regs rs').
  
Lemma Pregmap_gsspec_alt : forall (A : Type) (i j : Pregmap.elt) (x : A) (m : Pregmap.t A),
    (m # j <- x) i = (if Pregmap.elt_eq i j then x else m i).

Lemma regset_inject_expand : forall j rs1 rs2 v1 v2 r,
  regset_inject j rs1 rs2 ->
  Val.inject j v1 v2 ->
  regset_inject j (rs1 # r <- v1) (rs2 # r <- v2).

Lemma regset_inject_expand_vundef_left : forall j rs1 rs2 r,
  regset_inject j rs1 rs2 ->
  regset_inject j (rs1 # r <- Vundef) rs2.

Lemma set_res_pres_inject : forall res j rs1 rs2,
    regset_inject j rs1 rs2 ->
    forall vres1 vres2,
    Val.inject j vres1 vres2 ->
    regset_inject j (set_res res vres1 rs1) (set_res res vres2 rs2).


Lemma nextinstr_pres_inject : forall j rs1 rs2 sz,
    regset_inject j rs1 rs2 ->
    regset_inject j (nextinstr rs1 sz) (nextinstr rs2 sz).

Lemma nextinstr_nf_pres_inject : forall j rs1 rs2 sz,
    regset_inject j rs1 rs2 ->
    regset_inject j (nextinstr_nf rs1 sz) (nextinstr_nf rs2 sz).


Lemma set_pair_pres_inject : forall j rs1 rs2 v1 v2 loc,
    regset_inject j rs1 rs2 ->
    Val.inject j v1 v2 ->
    regset_inject j (set_pair loc v1 rs1) (set_pair loc v2 rs2).

Lemma vinject_pres_not_vundef : forall j v1 v2,
  Val.inject j v1 v2 -> v1 <> Vundef -> v2 <> Vundef.

Lemma vinject_pres_has_type : forall j v1 v2 t,
    Val.inject j v1 v2 -> v1 <> Vundef ->
    Val.has_type v1 t -> Val.has_type v2 t.

Lemma inject_decr : forall b j j' m1 m2 b' ofs,
  Mem.valid_block m1 b -> inject_incr j j' -> inject_separated j j' m1 m2 ->
  j' b = Some (b', ofs) -> j b = Some (b', ofs).

Lemma inject_pres_match_sminj :
  forall j j' m1 m2 (ms: match_inj j),
    glob_block_valid m1 -> inject_incr j j' -> inject_separated j j' m1 m2 ->
    match_inj j'.


Lemma inject_pres_valid_instr_offset_is_internal : forall j j' m1 m2,
    glob_block_valid m1 -> inject_incr j j' -> inject_separated j j' m1 m2 ->
    valid_instr_offset_is_internal j -> valid_instr_offset_is_internal j'.

Lemma inject_pres_extfun_entry_is_external : forall j j' m1 m2,
    glob_block_valid m1 -> inject_incr j j' -> inject_separated j j' m1 m2 ->
    extfun_entry_is_external j -> extfun_entry_is_external j'.

Lemma inject_pres_match_find_funct : forall j j' m1 m2,
    glob_block_valid m1 -> inject_incr j j' -> inject_separated j j' m1 m2 ->
    match_find_funct j -> match_find_funct j'.



Lemma inject_symbol_address : forall j id ofs,
    match_inj j ->
    Val.inject j (Globalenvs.Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs).


Ltac simpl_goal :=
  repeat match goal with
         | [ |- context [ Int.add Int.zero _ ] ] =>
           rewrite Int.add_zero_l
         | [ |- context [ Int64.add Int64.zero _ ] ] =>
           rewrite Int64.add_zero_l
         | [ |- context [Ptrofs.add _ (Ptrofs.of_int Int.zero)] ] =>
           rewrite Ptrofs.add_zero
         | [ |- context [Ptrofs.add _ (Ptrofs.of_int64 Int64.zero)] ] =>
           rewrite Ptrofs.add_zero
         | [ |- context [Ptrofs.add Ptrofs.zero _] ] =>
           rewrite Ptrofs.add_zero_l
         | [ |- context [Ptrofs.repr (Ptrofs.unsigned _)] ] =>
           rewrite Ptrofs.repr_unsigned
         end.


Ltac destr_pair_if :=
  repeat match goal with
         | [ |- context [match ?a with pair _ _ => _ end] ] =>
           destruct a eqn:?
         | [ |- context [if ?h then _ else _] ] =>
           destruct h eqn:?
         end.

Ltac inject_match :=
  match goal with
  | [ |- Val.inject ?j (match ?a with _ => _ end) (match ?b with _ => _ end) ] =>
    assert (Val.inject j a b)
  end.

Ltac inv_valinj :=
  match goal with
         | [ H : Val.inject _ (Vint _) _ |- _ ] =>
           inversion H; subst
         | [ H : Val.inject _ (Vlong _) _ |- _ ] =>
           inversion H; subst
         | [ H : Val.inject _ (Vptr _ _) _ |- _ ] =>
           inversion H; subst
         end.

Ltac destr_valinj_right H :=
  match type of H with
  | Val.inject _ _ ?a =>
    destruct a eqn:?
  end.

Ltac destr_valinj_left H :=
  match type of H with
  | Val.inject _ ?a ?b =>
    destruct a eqn:?
  end.

Lemma eval_addrmode32_inject: forall j a rs1 rs2,
    match_inj j ->
    regset_inject j rs1 rs2 ->
    Val.inject j (Asm.eval_addrmode32 ge a rs1) (FlatAsm.eval_addrmode32 tge a rs2).

Lemma eval_addrmode64_inject: forall j a rs1 rs2,
    match_inj j ->
    regset_inject j rs1 rs2 ->
    Val.inject j (Asm.eval_addrmode64 ge a rs1) (FlatAsm.eval_addrmode64 tge a rs2).

Lemma eval_addrmode_inject: forall j a rs1 rs2,
    match_inj j ->
    regset_inject j rs1 rs2 ->
    Val.inject j (Asm.eval_addrmode ge a rs1) (FlatAsm.eval_addrmode tge a rs2).

Lemma exec_load_step: forall j rs1 rs2 m1 m2 rs1' m1' sz chunk rd a
                          (MINJ: Mem.inject j (def_frame_inj m1) m1 m2)
                          (MATCHINJ: match_inj j)
                          (INSTRINTERNAL: valid_instr_offset_is_internal j)
                          (EXTEXTERNAL: extfun_entry_is_external j)
                          (MATCHFINDFUNCT: match_find_funct j)
                          (RSINJ: regset_inject j rs1 rs2)
                          (GBVALID: glob_block_valid m1),
    Asm.exec_load ge chunk m1 a rs1 rd sz = Next rs1' m1' ->
    exists rs2' m2',
      FlatAsm.exec_load tge chunk m2 a rs2 rd sz = Next rs2' m2' /\
      match_states (State rs1' m1') (State rs2' m2').

Lemma store_pres_glob_block_valid : forall m1 chunk b v ofs m2,
  Mem.store chunk m1 b ofs v = Some m2 -> glob_block_valid m1 -> glob_block_valid m2.

Lemma storev_pres_glob_block_valid : forall m1 chunk ptr v m2,
  Mem.storev chunk m1 ptr v = Some m2 -> glob_block_valid m1 -> glob_block_valid m2.

Lemma exec_store_step: forall j rs1 rs2 m1 m2 rs1' m1' sz chunk r a dregs
                         (MINJ: Mem.inject j (def_frame_inj m1) m1 m2)
                         (MATCHINJ: match_inj j)
                         (INSTRINTERNAL: valid_instr_offset_is_internal j)
                         (EXTEXTERNAL: extfun_entry_is_external j)
                         (MATCHFINDFUNCT: match_find_funct j)
                         (RSINJ: regset_inject j rs1 rs2)
                         (GBVALID: glob_block_valid m1),
    Asm.exec_store ge chunk m1 a rs1 r dregs sz = Next rs1' m1' ->
    exists rs2' m2',
      FlatAsm.exec_store tge chunk m2 a rs2 r dregs sz = Next rs2' m2' /\
      match_states (State rs1' m1') (State rs2' m2').


Lemma valid_ptr_inj : forall j m m',
    Mem.inject j (def_frame_inj m) m m' ->
    forall b i b' delta,
      j b = Some (b', delta) ->
      Mem.valid_pointer m b (Ptrofs.unsigned i) = true ->
      Mem.valid_pointer m' b' (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr delta))) = true.


Lemma weak_valid_ptr_inj: forall j m m',
  Mem.inject j (def_frame_inj m) m m' ->
  forall b1 ofs b2 delta,
  j b1 = Some(b2, delta) ->
  Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs) = true ->
  Mem.weak_valid_pointer m' b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.

Lemma weak_valid_ptr_no_overflow: forall j m m',
  Mem.inject j (def_frame_inj m) m m' ->
  forall b1 ofs b2 delta,
  j b1 = Some(b2, delta) ->
  Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs) = true ->
  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.

Lemma valid_different_ptrs_inj: forall j m m',
  Mem.inject j (def_frame_inj m) m m' ->
  forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
  b1 <> b2 ->
  Mem.valid_pointer m b1 (Ptrofs.unsigned ofs1) = true ->
  Mem.valid_pointer m b2 (Ptrofs.unsigned ofs2) = true ->
  j b1 = Some (b1', delta1) ->
  j b2 = Some (b2', delta2) ->
  b1' <> b2' \/
  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).

Definition cmpu_bool_inject := fun j m m' (MINJ: Mem.inject j (def_frame_inj m) m m') =>
                     Val.cmpu_bool_inject j (Mem.valid_pointer m) (Mem.valid_pointer m')
                                          (valid_ptr_inj j m m' MINJ)
                                          (weak_valid_ptr_inj j m m' MINJ)
                                          (weak_valid_ptr_no_overflow j m m' MINJ)
                                          (valid_different_ptrs_inj j m m' MINJ).

Lemma cmpu_bool_lessdef : forall j v1 v2 v1' v2' m m' c,
    Val.inject j v1 v1' -> Val.inject j v2 v2' ->
    Mem.inject j (def_frame_inj m) m m' ->
    Val.opt_lessdef (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2)
                (Val.cmpu_bool (Mem.valid_pointer m') c v1' v2').

Definition cmplu_bool_inject := fun j m m' (MINJ: Mem.inject j (def_frame_inj m) m m') =>
                     Val.cmplu_bool_inject j (Mem.valid_pointer m) (Mem.valid_pointer m')
                                           (valid_ptr_inj j m m' MINJ)
                                           (weak_valid_ptr_inj j m m' MINJ)
                                           (weak_valid_ptr_no_overflow j m m' MINJ)
                                           (valid_different_ptrs_inj j m m' MINJ).


Lemma cmplu_bool_lessdef : forall j v1 v2 v1' v2' m m' c,
    Val.inject j v1 v1' -> Val.inject j v2 v2' ->
    Mem.inject j (def_frame_inj m) m m' ->
    Val.opt_lessdef (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2)
                (Val.cmplu_bool (Mem.valid_pointer m') c v1' v2').

Lemma val_of_optbool_lessdef : forall j v1 v2,
    Val.opt_lessdef v1 v2 -> Val.inject j (Val.of_optbool v1) (Val.of_optbool v2).

Lemma cmpu_inject : forall j v1 v2 v1' v2' m m' c,
    Val.inject j v1 v1' -> Val.inject j v2 v2' ->
    Mem.inject j (def_frame_inj m) m m' ->
    Val.inject j (Val.cmpu (Mem.valid_pointer m) c v1 v2)
               (Val.cmpu (Mem.valid_pointer m') c v1' v2').

Lemma val_negative_inject: forall j v1 v2,
  Val.inject j v1 v2 -> Val.inject j (Val.negative v1) (Val.negative v2).

Lemma val_negativel_inject: forall j v1 v2,
  Val.inject j v1 v2 -> Val.inject j (Val.negativel v1) (Val.negativel v2).

Lemma sub_overflow_inject : forall v1 v2 v1' v2' j,
    Val.inject j v1 v2 -> Val.inject j v1' v2' ->
    Val.inject j (Val.sub_overflow v1 v1') (Val.sub_overflow v2 v2').

Lemma subl_overflow_inject : forall v1 v2 v1' v2' j,
    Val.inject j v1 v2 -> Val.inject j v1' v2' ->
    Val.inject j (Val.subl_overflow v1 v1') (Val.subl_overflow v2 v2').

Lemma compare_ints_inject: forall j v1 v2 v1' v2' rs rs' m m',
    Val.inject j v1 v1' -> Val.inject j v2 v2' ->
    Mem.inject j (def_frame_inj m) m m' ->
    regset_inject j rs rs' ->
    regset_inject j (compare_ints v1 v2 rs m) (compare_ints v1' v2' rs' m').

Lemma cmplu_lessdef : forall j v1 v2 v1' v2' m m' c,
    Val.inject j v1 v1' -> Val.inject j v2 v2' ->
    Mem.inject j (def_frame_inj m) m m' ->
    Val.opt_val_inject j (Val.cmplu (Mem.valid_pointer m) c v1 v2)
                     (Val.cmplu (Mem.valid_pointer m') c v1' v2').

Lemma compare_longs_inject: forall j v1 v2 v1' v2' rs rs' m m',
    Val.inject j v1 v1' -> Val.inject j v2 v2' ->
    Mem.inject j (def_frame_inj m) m m' ->
    regset_inject j rs rs' ->
    regset_inject j (compare_longs v1 v2 rs m) (compare_longs v1' v2' rs' m').

Ltac solve_val_inject :=
  match goal with
  | [ H : Val.inject _ (Vfloat _) Vundef |- _] => inversion H
  | [ H : Val.inject _ (Vfloat _) (Vint _) |- _] => inversion H
  | [ H : Val.inject _ (Vfloat _) (Vlong _) |- _] => inversion H
  | [ H : Val.inject _ (Vfloat _) (Vsingle _) |- _] => inversion H
  | [ H : Val.inject _ (Vfloat _) (Vptr _ _) |- _] => inversion H
  | [ H : Val.inject _ (Vfloat _) (Vfloat _) |- _] => inv H; solve_val_inject
  | [ H : Val.inject _ (Vsingle _) Vundef |- _] => inversion H
  | [ H : Val.inject _ (Vsingle _) (Vint _) |- _] => inversion H
  | [ H : Val.inject _ (Vsingle _) (Vlong _) |- _] => inversion H
  | [ H : Val.inject _ (Vsingle _) (Vsingle _) |- _] => inv H; solve_val_inject
  | [ H : Val.inject _ (Vsingle _) (Vptr _ _) |- _] => inversion H
  | [ H : Val.inject _ (Vsingle _) (Vfloat _) |- _] => inversion H
  | [ |- Val.inject _ (Val.of_bool ?v) (Val.of_bool ?v) ] => apply Val.vofbool_inject
  | [ |- Val.inject _ Vundef _ ] => auto
  end.

Ltac solve_regset_inject :=
  match goal with
  | [ H: regset_inject ?j ?rs1 ?rs2 |- regset_inject ?j (Asm.undef_regs ?uregs ?rs1) (Asm.undef_regs ?uregs ?rs2)] =>
    apply undef_regs_pres_inject; auto
  | [ |- regset_inject _ (Asm.undef_regs _ _) _ ] =>
    unfold Asm.undef_regs; solve_regset_inject
  | [ |- regset_inject _ _ (Asm.undef_regs _ _) ] =>
    unfold Asm.undef_regs; simpl; solve_regset_inject
  | [ |- regset_inject _ (?rs1 # ?r <- ?v1) (?rs2 # ?r <- ?v2) ] =>
    apply regset_inject_expand; [solve_regset_inject | solve_val_inject]
  | [ H: regset_inject ?j ?rs1 ?rs2 |- regset_inject ?j ?rs1 ?rs2 ] =>
    auto
  end.

Lemma compare_floats_inject: forall j v1 v2 v1' v2' rs rs',
    Val.inject j v1 v1' -> Val.inject j v2 v2' ->
    regset_inject j rs rs' ->
    regset_inject j (compare_floats v1 v2 rs) (compare_floats v1' v2' rs').

Lemma compare_floats32_inject: forall j v1 v2 v1' v2' rs rs',
    Val.inject j v1 v1' -> Val.inject j v2 v2' ->
    regset_inject j rs rs' ->
    regset_inject j (compare_floats32 v1 v2 rs) (compare_floats32 v1' v2' rs').

  
Ltac solve_store_load :=
  match goal with
  | [ H : Asm.exec_instr _ _ _ _ _ _ = Next _ _ |- _ ] =>
    unfold Asm.exec_instr in H; simpl in H; solve_store_load
  | [ H : Asm.exec_store _ _ _ _ _ _ _ _ = Next _ _ |- _ ] =>
    exploit exec_store_step; eauto
  | [ H : Asm.exec_load _ _ _ _ _ _ _ = Next _ _ |- _ ] =>
    exploit exec_load_step; eauto
  end.

Ltac solve_opt_lessdef :=
  match goal with
  | [ |- Val.opt_lessdef (match ?rs1 ?r with
                     | _ => _
                     end) _ ] =>
    let EQ := fresh "EQ" in (destruct (rs1 r) eqn:EQ; solve_opt_lessdef)
  | [ |- Val.opt_lessdef None _ ] => constructor
  | [ |- Val.opt_lessdef (Some _) (match ?rs2 ?r with
                              | _ => _
                              end) ] =>
    let EQ := fresh "EQ" in (destruct (rs2 r) eqn:EQ; solve_opt_lessdef)
  | [ H1: regset_inject _ ?rs1 ?rs2, H2: ?rs1 ?r = _, H3: ?rs2 ?r = _ |- _ ] =>
    generalize (H1 r); rewrite H2, H3; clear H2 H3; inversion 1; subst; solve_opt_lessdef
  | [ |- Val.opt_lessdef (Some ?v) (Some ?v) ] => constructor
  end.

Lemma eval_testcond_inject: forall j c rs1 rs2,
    regset_inject j rs1 rs2 ->
    Val.opt_lessdef (Asm.eval_testcond c rs1) (Asm.eval_testcond c rs2).

Hint Resolve nextinstr_nf_pres_inject nextinstr_pres_inject regset_inject_expand
  regset_inject_expand_vundef_left undef_regs_pres_inject
  Val.zero_ext_inject Val.sign_ext_inject Val.longofintu_inject Val.longofint_inject
  Val.singleoffloat_inject Val.loword_inject Val.floatofsingle_inject Val.intoffloat_inject Val.maketotal_inject
  Val.intoffloat_inject Val.floatofint_inject Val.intofsingle_inject Val.singleofint_inject
  Val.longoffloat_inject Val.floatoflong_inject Val.longofsingle_inject Val.singleoflong_inject
  eval_addrmode32_inject eval_addrmode64_inject eval_addrmode_inject
  Val.neg_inject Val.negl_inject Val.add_inject Val.addl_inject
  Val.sub_inject Val.subl_inject Val.mul_inject Val.mull_inject Val.mulhs_inject Val.mulhu_inject
  Val.mullhs_inject Val.mullhu_inject Val.shr_inject Val.shrl_inject Val.or_inject Val.orl_inject
  Val.xor_inject Val.xorl_inject Val.and_inject Val.andl_inject Val.notl_inject
  Val.shl_inject Val.shll_inject Val.vzero_inject Val.notint_inject
  Val.shru_inject Val.shrlu_inject Val.ror_inject Val.rorl_inject
  compare_ints_inject compare_longs_inject compare_floats_inject compare_floats32_inject
  Val.addf_inject Val.subf_inject Val.mulf_inject Val.divf_inject Val.negf_inject Val.absf_inject
  Val.addfs_inject Val.subfs_inject Val.mulfs_inject Val.divfs_inject Val.negfs_inject Val.absfs_inject
  val_of_optbool_lessdef eval_testcond_inject Val.offset_ptr_inject: inject_db.

Ltac solve_exec_instr :=
  match goal with
  | [ |- Next _ _ = Next _ _ ] =>
    reflexivity
  | [ |- context [eval_testcond _ _] ]=>
    unfold eval_testcond; solve_exec_instr
  | [ H: Asm.eval_testcond ?c ?r = _ |- context [Asm.eval_testcond ?c ?r] ] =>
    rewrite H; solve_exec_instr
  | [ H: _ = Asm.eval_testcond ?c ?r |- context [Asm.eval_testcond ?c ?r] ] =>
    rewrite <- H; solve_exec_instr
  end.

Ltac solve_match_states :=
  match goal with
  | [ H: Asm.Stuck = Next _ _ |- _ ] => inv H
  | [ |- exists _, _ ] => eexists; solve_match_states
  | [ |- (FlatAsm.exec_instr _ _ _ _ = Next _ _) /\ match_states _ _ ] =>
    split; [simpl; solve_exec_instr | econstructor; eauto; solve_match_states]
  | [ |- regset_inject _ _ _ ] =>
    eauto 10 with inject_db
  end.

Ltac destr_eval_testcond :=
  match goal with
  | [ H : match Asm.eval_testcond ?c ?rs with | _ => _ end = Next _ _ |- _ ] =>
    let ETEQ := fresh "ETEQ" in (
      destruct (Asm.eval_testcond c rs) eqn:ETEQ); destr_eval_testcond
  | [ H : Some ?b = Asm.eval_testcond _ _ |- _ ] =>
    match b with
    | true => fail 1
    | false => fail 1
    | _ => destruct b; destr_eval_testcond
    end
  | [ H : Asm.eval_testcond _ _ = Some ?b |- _] =>
    match b with
    | true => fail 1
    | false => fail 1
    | _ => destruct b; destr_eval_testcond
    end
  | [ H : Asm.Next _ _ = Next _ _ |- _ ] =>
    inv H; destr_eval_testcond
  | [ H: Val.opt_lessdef (Some true) (Asm.eval_testcond _ _) |- _ ] =>
    inv H; destr_eval_testcond
  | [ H: Val.opt_lessdef (Some false) (Asm.eval_testcond _ _) |- _ ] =>
    inv H; destr_eval_testcond
  | _ => idtac
  end.

Ltac destr_match_outcome :=
  match goal with
  | [ H: Asm.Stuck = Next _ _ |- _ ] => inv H
  | [ H: Asm.Next _ _ = Next _ _ |- _ ] => inv H; destr_match_outcome
  | [ H: match ?a with _ => _ end = Next _ _ |- _] =>
    let EQ := fresh "EQ" in (destruct a eqn:EQ; destr_match_outcome)
  | _ => idtac
  end.


Lemma goto_label_pres_mem : forall f l rs1 m1 rs1' m1',
    Asm.goto_label ge f l rs1 m1 = Next rs1' m1' -> m1 = m1'.

Lemma goto_label_inject : forall rs1 rs2 id b f l j m1 m2 rs1' m1' ofs
                            (MATCHSMINJ: match_inj j)
                            (RINJ: regset_inject j rs1 rs2)
                            (MINJ:Mem.inject j (def_frame_inj m1) m1 m2),
    rs1 PC = Vptr b ofs ->
    Globalenvs.Genv.find_symbol ge id = Some b ->
    Globalenvs.Genv.find_funct_ptr ge b = Some (Internal f) ->
    Asm.goto_label ge f l rs1 m1 = Next rs1' m1' ->
    exists rs2', goto_label tge id l rs2 m2 = Next rs2' m2 /\
            regset_inject j rs1' rs2' /\ Mem.inject j (def_frame_inj m1') m1' m2.

Lemma goto_tbl_label_inject : forall id tbl l b f j rs1 rs2 m1 m2 rs1' m1' i ofs
                                (MATCHSMINJ: match_inj j)
                                (RINJ: regset_inject j rs1 rs2)
                                (MINJ:Mem.inject j (def_frame_inj m1) m1 m2),
    rs1 PC = Vptr b ofs ->
    Globalenvs.Genv.find_symbol ge id = Some b ->
    Globalenvs.Genv.find_funct_ptr ge b = Some (Internal f) ->
    list_nth_z tbl i = Some l ->
    Asm.goto_label ge f l ((rs1 # RAX <- Vundef) # RDX <- Vundef) m1 = Next rs1' m1' ->
    exists rs2',
      FlatAsm.goto_label tge id l ((rs2 # RAX <- Vundef) # RDX <- Vundef) m2 = Next rs2' m2 /\
      regset_inject j rs1' rs2' /\ Mem.inject j (def_frame_inj m1') m1' m2.

Lemma add_globals_pres_senv :
  forall (defs : list (ident * option gdef * segblock)) (ge : FlatAsm.genv),
  Genv.genv_senv (add_globals ge defs) = Genv.genv_senv ge.

Lemma transl_prog_pres_senv : forall gmap lmap dsize csize tprog prog,
    transl_prog_with_map gmap lmap prog dsize csize = OK tprog ->
    (Genv.genv_senv (globalenv tprog)) = (Globalenvs.Genv.globalenv prog).



Lemma exec_instr_step : forall j rs1 rs2 m1 m2 rs1' m1' i i' id sid ofs ofs' f b
                        (MINJ: Mem.inject j (def_frame_inj m1) m1 m2)
                        (MATCHSMINJ: match_inj j)
                        (INSTRINTERNAL: valid_instr_offset_is_internal j)
                        (EXTEXTERNAL: extfun_entry_is_external j)
                        (MATCHFINDFUNCT: match_find_funct j)
                        (RSINJ: regset_inject j rs1 rs2)
                        (GBVALID: glob_block_valid m1),
    rs1 PC = Vptr b ofs ->
    Globalenvs.Genv.find_symbol ge id = Some b ->
    Globalenvs.Genv.find_funct_ptr ge b = Some (Internal f) ->
    Asm.find_instr (Ptrofs.unsigned ofs) (Asm.fn_code f) = Some i ->
    RealAsm.exec_instr ge f i rs1 m1 = Next rs1' m1' ->
    transl_instr ofs' id sid i = OK i' ->
    exists rs2' m2',
      FlatAsm.exec_instr tge i' rs2 m2 = Next rs2' m2' /\
      match_states (State rs1' m1') (State rs2' m2').

Theorem step_simulation:
  forall S1 t S2,
    RealAsm.step ge S1 t S2 ->
    forall S1' (MS: match_states S1 S1'),
    exists S2',
      FlatAsm.step tge S1' t S2' /\
      match_states S2 S2'.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> Asm.final_state st1 r -> FlatAsm.final_state st2 r.
  
Theorem transf_program_correct:
  forward_simulation (RealAsm.semantics prog (Pregmap.init Vundef)) (FlatAsm.semantics tprog (Pregmap.init Vundef)).

Require Import MCgen.
Arguments is_valid_label_dec: simpl nomatch.

Lemma transl_instrs_id_code:
  forall c i ii sbb id s i0 x x0,
    FlatAsmgen.transl_instrs i s i0 c = OK (x, x0) ->
    In (ii, sbb, id) x0 ->
    segblock_id sbb = s /\ i = id.


Lemma in_transl_globdefs_code:
  forall defs g tdefs i tdef sb,
    FlatAsmgen.transl_globdefs g defs = OK tdefs ->
    In (i, Some tdef, sb) tdefs ->
    exists def,
      In (i, def) defs /\ FlatAsmgen.transl_globdef g i def = OK (i, Some tdef, sb).

Lemma transl_fun_id_code:
  forall g i f1 f2 ii sbb id,
    FlatAsmgen.transl_fun g i f1 = OK f2 ->
    In (ii, sbb, id) (fn_code f2) ->
    exists s i0,
      g i = Some (s, i0) /\
      segblock_id sbb = s /\ i = id.

Lemma transl_instrs_back:
  forall c i ii sbb id s i0 x x0,
    FlatAsmgen.transl_instrs i s i0 c = OK (x, x0) ->
    In (ii, sbb, id) x0 ->
    exists ofs ii1,
      FlatAsmgen.transl_instr ofs i s ii1 = OK (ii, sbb,id) /\
      In ii1 c.

Lemma transf_check_faprog:
  wf_prog prog -> check_faprog tprog = true.

End PRESERVATION.


End WITHMEMORYMODEL.