Module AsmLocalize

Require Import Coqlib Maps Integers Values Memdata AST Globalenvs.
Require Import Blockset Footprint FMemOpFP GMemory FMemory FMemPerm MemAux CUAST
        Asm AsmLang ASM_local LDSimDefs Localize ValRels MemInterpolant val_casted.

Lemma init_genv_iff: forall cu ge G,
    AsmLang.init_genv cu ge G <->
    G = ge /\ ge_related ge (Genv.globalenv (mkprogram (cu_defs cu) (cu_public cu) 1%positive)).

Lemma Loclocalize_univ:
  forall j, Loclocalize j Locs.univ Locs.univ.

Lemma Loclocalize_emp:
  forall j, Loclocalize j Locs.emp Locs.emp.

Lemma FPlocalize_cmp_undef:
  forall j, FPlocalize j
                  {| FP.cmps := Locs.univ; FP.reads := Locs.emp; FP.writes := Locs.emp; FP.frees := Locs.emp |}
                  {| FP.cmps := Locs.univ; FP.reads := Locs.emp; FP.writes := Locs.emp; FP.frees := Locs.emp |}.


Lemma invert_symbol_from_string_eq:
  forall F V (ge ge_local: Genv.t (AST.fundef F) V) (NOREPEF: norep_ef_name ge_local),
    (forall b gd, (Genv.genv_defs ge_local) ! b = Some gd -> exists id, (Genv.genv_symb ge_local) ! id = Some b) ->
    ge_related ge ge_local ->
    forall name, invert_symbol_from_string ge name = invert_symbol_from_string ge_local name.

Program Definition empmem (BOUND: block) : Memory.Mem.mem :=
  Memory.Mem.mkmem (PMap.init (ZMap.init Undef))
                   (PMap.init (fun (_ : Z) (_ : Memtype.perm_kind) => None))
                   (BOUND) _ _ _.

Lemma strip_valid_block: forall fm, (GMem.valid_block (strip fm) = Mem.valid_block fm).

Lemma strip_mem_access: forall fm, GMem.mem_access (strip fm) = Mem.mem_access fm.

Lemma strip_mem_contents: forall fm, GMem.mem_contents (strip fm) = Mem.mem_contents fm.
Lemma list_forall2_split:
  forall A B (P: A -> B -> Prop) (al' bl': list B) (l: list A),
    list_forall2 P l (al' ++ bl') ->
    exists al bl, l = al ++ bl /\ list_forall2 P al al' /\ list_forall2 P bl bl'.
Lemma lmem_construction:
  forall F V (ge ge_local: Genv.t F V) j m fl,
    Bset.inject j (fun b => Plt b (Genv.genv_next ge_local)) (fun b => Plt b (Genv.genv_next ge)) ->
    ge_match_strict j ge ge_local ->
    init_gmem_generic ge m ->
    norep fl ->
    no_overlap fl (valid_block_bset m) ->
    exists lm, init_mem_generic ge_local lm /\
          mem_related j (Genv.genv_next ge) fl m lm.

Lemma init_mem_valid_block:
  forall ge m,
    AsmLang.init_mem ge m ->
    (forall b, Bset.belongsto (valid_block_bset m) b <-> Plt b (Genv.genv_next ge)).
  

Definition bj_constr (ge ge_local: Senv.t) : Bset.inj :=
  fun b => match Senv.invert_symbol ge_local b with
        | Some id => Senv.find_symbol ge b
        | None => None
        end.



Definition regset_related (j: Bset.inj) (rs_local rs: regset): Prop := forall r, val_related j (rs_local#r) (rs#r).

Definition loadframe_related (j: Bset.inj) (lf_local lf: load_frame) : Prop :=
  match lf_local, lf with
  | mk_load_frame b oty, mk_load_frame b' oty' => j b = Some b' /\ oty = oty'
  end.

Lemma set_regset_related:
  forall j rs rs' r v v',
    regset_related j rs rs' ->
    val_related j v v' ->
    regset_related j (rs # r <- v) (rs' # r <- v').

Lemma undef_regs_regset_related:
  forall rl j rs rs',
    regset_related j rs rs' ->
    regset_related j (undef_regs rl rs) (undef_regs rl rs').

Lemma set_res_regset_related:
  forall j br rs rs' v v',
    regset_related j rs rs' ->
    val_related j v v' ->
    regset_related j (set_res br v rs) (set_res br v' rs').
  
Lemma regset_related_val_related:
  forall j rs rs' r, regset_related j rs rs' -> val_related j (rs # r) (rs' # r).

Local Hint Resolve set_regset_related undef_regs_regset_related set_res_regset_related regset_related_val_related.

Inductive outcome_related (j: Bset.inj) (bound: block) (fl: freelist) : Asm.outcome -> AsmLang.outcome -> Prop :=
| Stuck_related: outcome_related j bound fl Asm.Stuck AsmLang.Stuck
| Next_related: forall rs rs' m m',
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    outcome_related j bound fl (Asm.Next rs m) (Next rs' m').

Lemma symbol_address_related:
  forall j (ge ge': genv) id ofs,
    (forall id, option_rel (fun b b' => j b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    val_related j (Genv.symbol_address ge id ofs) (Genv.symbol_address ge' id ofs).

Lemma eval_addrmode32_related:
  forall j ge ge' rs rs' a,
    Bset.inj_inject j ->
    (forall id, option_rel (fun b b' => j b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related j rs rs' ->
    val_related j (eval_addrmode32 ge a rs) (eval_addrmode32 ge' a rs').

Lemma eval_addrmode64_related:
  forall j ge ge' rs rs' a,
    Bset.inj_inject j ->
    (forall id, option_rel (fun b b' => j b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related j rs rs' ->
    val_related j (eval_addrmode64 ge a rs) (eval_addrmode64 ge' a rs').

Lemma eval_addrmode_related:
  forall j ge ge' rs rs' a,
    Bset.inj_inject j ->
    (forall id, option_rel (fun b b' => j b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related j rs rs' ->
    val_related j (eval_addrmode ge a rs) (eval_addrmode ge' a rs').

Lemma exec_load_related:
  forall j ge ge' rs rs' m m' bound fl chunk a rd (NOREP: norep fl),
    Bset.inj_inject (construct_inj j bound fl) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    outcome_related j bound fl (exec_load ge chunk m a rs rd) (AsmLang.exec_load ge' chunk m' a rs' rd).

Lemma exec_store_related:
  forall j ge ge' rs rs' m m' bound fl chunk a r1 destroyed (NOREP: norep fl),
    Bset.inj_inject (construct_inj j bound fl) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    outcome_related j bound fl (exec_store ge chunk m a rs r1 destroyed) (AsmLang.exec_store ge' chunk m' a rs' r1 destroyed).

Lemma compare_ints_related:
  forall j bound fl rs rs' m m' x x' y y',
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    val_related (construct_inj j bound fl) x x' ->
    val_related (construct_inj j bound fl) y y' ->
    Bset.inj_inject (construct_inj j bound fl) ->
    regset_related (construct_inj j bound fl) (Asm.compare_ints x y rs m) (compare_ints x' y' rs' m').

Lemma check_compare_ints_related:
  forall j bound fl m m' x x' y y',
    mem_related j bound fl (strip m') m ->
    val_related (construct_inj j bound fl) x x' ->
    val_related (construct_inj j bound fl) y y' ->
    Bset.inj_inject (construct_inj j bound fl) ->
    Asm.check_compare_ints x y m = check_compare_ints x' y' m'.
  
Lemma compare_longs_related:
    forall j bound fl rs rs' m m' x x' y y',
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    val_related (construct_inj j bound fl) x x' ->
    val_related (construct_inj j bound fl) y y' ->
    regset_related (construct_inj j bound fl) (Asm.compare_longs x y rs m) (compare_longs x' y' rs' m').

Lemma compare_floats_related:
  forall j rs rs' x x' y y',
    regset_related j rs rs' ->
    val_related j x x' ->
    val_related j y y' ->
    regset_related j (Asm.compare_floats x y rs) (compare_floats x' y' rs').

Lemma compare_floats32_related:
  forall j rs rs' x x' y y',
    regset_related j rs rs' ->
    val_related j x x' ->
    val_related j y y' ->
    regset_related j (Asm.compare_floats32 x y rs) (compare_floats32 x' y' rs').

Lemma eval_testcond_related:
  forall j c rs rs',
    regset_related j rs rs' ->
    option_rel eq (eval_testcond c rs) (eval_testcond c rs').

Local Hint Resolve symbol_address_related eval_addrmode64_related eval_addrmode32_related
      exec_load_related exec_store_related check_compare_ints_related compare_ints_related compare_longs_related
      compare_floats_related compare_floats32_related
      eval_testcond_related.

Lemma range_locset_localize:
  forall j b b' base size,
    j b = Some b' ->
    Bset.inj_inject j ->
    Loclocalize j (range_locset b' base size) (range_locset b base size).

Lemma weak_valid_pointer_fp_localize:
  forall j bound fl m m' b b' ofs,
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    Bset.inject j (fun b : block => Plt b bound) (fun b : block => Plt b bound) ->
    mem_related j bound fl (strip m') m ->
    construct_inj j bound fl b = Some b' ->
    FPlocalize (construct_inj j bound fl)
               (weak_valid_pointer_fp m' b' ofs) (MemOpFP.weak_valid_pointer_fp m b ofs).

Lemma loadv_fp_localize:
  forall j addr addr' chunk,
    Bset.inj_inject j ->
    val_related j addr addr' ->
    FPlocalize j (FMemOpFP.loadv_fp chunk addr') (FMemOpFP.loadv_fp chunk addr).

Lemma storev_fp_localize:
  forall j addr addr' chunk,
    Bset.inj_inject j ->
    val_related j addr addr' ->
    FPlocalize j (FMemOpFP.storev_fp chunk addr') (FMemOpFP.storev_fp chunk addr).

Lemma cmpu_fp_localize:
  forall j bound fl m m' v1 v1' v2 v2' c,
    norep fl ->
    no_overlap fl (fun b0 : block => Plt b0 bound) ->
    Bset.inject j (fun b0 : block => Plt b0 bound) (fun b0 : block => Plt b0 bound) ->
    mem_related j bound fl (strip m') m ->
    val_related (construct_inj j bound fl) v1 v1' ->
    val_related (construct_inj j bound fl) v2 v2' ->
    FPlocalize (construct_inj j bound fl)
               (of_optfp (Cop_fp.cmpu_bool_fp m' c v1' v2'))
               (ValFP.cmpu_bool_fp_total m c v1 v2).

Lemma exec_load_fp_localize:
  forall j ge ge' rs rs' bound fl chunk a ,
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    Bset.inject j (fun b : block => Plt b bound) (fun b : block => Plt b bound) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    FPlocalize (construct_inj j bound fl) (AsmLang.exec_load_fp ge' chunk a rs') (exec_load_fp ge chunk a rs).

Lemma exec_store_fp_localize:
  forall j ge ge' rs rs' bound fl chunk a ,
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    Bset.inject j (fun b : block => Plt b bound) (fun b : block => Plt b bound) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    FPlocalize (construct_inj j bound fl) (AsmLang.exec_store_fp ge' chunk a rs') (exec_store_fp ge chunk a rs).

Lemma locs_union_same:
  forall ls, Locs.union ls ls = ls.
Lemma fp_union_same:
  forall fp, FP.union fp fp = fp.
  
Lemma compare_ints_fp_localize:
  forall j bound fl m m' x x' y y',
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    Bset.inject j (fun b : block => Plt b bound) (fun b : block => Plt b bound) ->
    mem_related j bound fl (strip m') m ->
    val_related (construct_inj j bound fl) x x' ->
    val_related (construct_inj j bound fl) y y' ->
    FPlocalize (construct_inj j bound fl) (AsmLang.compare_ints_fp x' y' m') (ASM_local.compare_ints_fp x y m).

Lemma compare_longs_fp_localize:
  forall j bound fl m m' x x' y y',
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    Bset.inject j (fun b : block => Plt b bound) (fun b : block => Plt b bound) ->
    mem_related j bound fl (strip m') m ->
    val_related (construct_inj j bound fl) x x' ->
    val_related (construct_inj j bound fl) y y' ->
    FPlocalize (construct_inj j bound fl) (AsmLang.compare_longs_fp x' y' m') (ASM_local.compare_longs_fp x y m).

Lemma construct_inj_block_G:
  forall j bound fl b b',
    Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound) ->
    construct_inj j bound fl b = Some b' ->
    Bset.belongsto (fun b => Plt b bound) b' \/ (exists n, get_block fl n = b').

Ltac red_blocks0 :=
  repeat match goal with
           | |- context[match ?x with _ => _ end] => destruct x; subst
           | |- context[FP.union _ _] => apply fpG_union
         end.
Ltac red_blocks :=
  red_blocks0;
    simpl; try apply fpG_emp; intros ?b BLOCKS;
      unfold Bset.belongsto, FP.blocks, FP.locs, store_fp, Locs.blocks in *; simpl in *;
        repeat rewrite Locs.locs_union_emp in BLOCKS; repeat rewrite Locs.emp_union_locs in BLOCKS;
          destruct BLOCKS as (? & BLOCKS); apply range_locset_loc in BLOCKS; destruct BLOCKS as [BLOCKS _]; subst;
            eapply construct_inj_block_G; eauto.

Lemma exec_load_fp_fpG:
  forall j fl bound (ge ge': genv) rs rs' chunk a,
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    fpG fl (fun b => Plt b bound) (AsmLang.exec_load_fp ge' chunk a rs').

Lemma exec_store_fp_fpG:
  forall j fl bound (ge ge': genv) rs rs' chunk a,
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    fpG fl (fun b => Plt b bound) (AsmLang.exec_store_fp ge' chunk a rs').

Lemma compare_ints_fp_fpG:
  forall j fl bound m m' v1 v2 v1' v2',
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    mem_related j bound fl (strip m') m ->
    val_related (construct_inj j bound fl) v1 v1' ->
    val_related (construct_inj j bound fl) v2 v2' ->
    fpG fl (fun b => Plt b bound) (AsmLang.compare_ints_fp v1' v2' m').

Lemma compare_longs_fp_fpG:
   forall j fl bound m m' v1 v2 v1' v2',
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    mem_related j bound fl (strip m') m ->
    val_related (construct_inj j bound fl) v1 v1' ->
    val_related (construct_inj j bound fl) v2 v2' ->
    fpG fl (fun b => Plt b bound) (AsmLang.compare_longs_fp v1' v2' m').

Ltac solv_rel :=
  match goal with
  | H: regset_related ?j ?rs ?rs' |- context[eval_testcond ?c ?rs] =>
    destruct (eval_testcond_related j c rs rs' H); solv_rel
  | H: regset_related _ ?rs _ |- context[match ?rs ?r with _ => _ end] => destruct (H r); solv_rel
  | |- context[match ?x with _ => _ end] => destruct x; solv_rel
  | |- outcome_related _ _ _ (exec_load _ _ _ _ _ _) _ =>
    eapply exec_load_related; eauto; solv_rel
  | |- outcome_related _ _ _ (exec_store _ _ _ _ _ _ _) _ =>
    eapply exec_store_related; eauto; solv_rel
  | |- outcome_related _ _ _ _ _ =>
    constructor; auto; unfold nextinstr_nf, nextinstr; solv_rel
  | |- regset_related _ (_ # _ <- _) (_ # _ <- _) =>
    apply set_regset_related; auto; solv_rel
  | |- regset_related _ (undef_regs _ _) (undef_regs _ _) =>
    apply undef_regs_regset_related; eauto; solv_rel
  | |- val_related _ (Val.offset_ptr _ _) (Val.offset_ptr _ _) =>
    apply offset_ptr_val_related; eauto; solv_rel
  | |- val_related _ (eval_addrmode32 _ _ _) (eval_addrmode32 _ _ _) =>
    apply eval_addrmode_related; eauto; solv_rel
  | |- val_related _ (_ # _) (_ # _) =>
    apply regset_related_val_related; auto; solv_rel
  | |- val_related _ (Val.zero_ext _ _) _ =>
    apply zero_ext_related; eauto; solv_rel
  | |- val_related _ (Val.sign_ext _ _) _ =>
    apply sign_ext_related; eauto; solv_rel
  | |- val_related _ (Val.maketotal _) _ =>
    apply maketotal_related; eauto; solv_rel
  | b: bool |- _ => destruct b; solv_rel
  | _ => subst; try (constructor; fail); try (congruence; fail)
  end; subst.

Lemma val_related_check_undef:
  forall j x1 x2 y1 y2,
    val_related j x1 y1 ->
    val_related j x2 y2 ->
    check_vundef x1 x2 = check_vundef y1 y2.

Lemma exec_instr_related:
  forall j ge ge' f i rs rs' m m' fl bound,
    fl = FMemory.Mem.freelist m' ->
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    outcome_related j bound fl (ASM_local.exec_instr ge f i rs m) (AsmLang.exec_instr ge' f i rs' m') /\
    FPlocalize (construct_inj j bound fl) (AsmLang.exec_instr_fp ge' f i rs' m') (ASM_local.exec_instr_fp ge f i rs m) /\
    fpG fl (fun b => Plt b bound) (AsmLang.exec_instr_fp ge' f i rs' m').

Lemma exec_instr_fl_unchanged:
  forall ge fn i rs m rs' m',
    AsmLang.exec_instr ge fn i rs m = Next rs' m' ->
    FMemory.Mem.freelist m' = FMemory.Mem.freelist m.

Lemma eval_builtin_arg_related:
  forall j bound fl arg ge ge' rs rs' vsp vsp' m m' varg,
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Senv.find_symbol ge id) (Senv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    val_related (construct_inj j bound fl) vsp vsp' ->
    mem_related j bound fl (strip m') m ->
    Events.eval_builtin_arg ge rs vsp m arg varg ->
    exists varg', AsmLang.eval_builtin_arg ge' rs' vsp' m' arg varg' /\
             val_related (construct_inj j bound fl) varg varg'.

Lemma eval_builtin_arg_related':
  forall j bound fl arg ge ge' rs rs' vsp vsp' m m' varg',
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Senv.find_symbol ge id) (Senv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    val_related (construct_inj j bound fl) vsp vsp' ->
    mem_related j bound fl (strip m') m ->
    AsmLang.eval_builtin_arg ge' rs' vsp' m' arg varg' ->
    exists varg, Events.eval_builtin_arg ge rs vsp m arg varg /\
             val_related (construct_inj j bound fl) varg varg'.

Lemma eval_builtin_arg_fp_localize':
  forall j arg ge ge' rs rs' vsp vsp' fp',
    Bset.inj_inject j ->
    (forall id, option_rel (fun b b' => j b = Some b') (Senv.find_symbol ge id) (Senv.find_symbol ge' id)) ->
    regset_related j rs rs' ->
    val_related j vsp vsp' ->
    MemOpFP.eval_builtin_arg_fp ge' rs' vsp' arg fp' ->
    exists fp, MemOpFP.eval_builtin_arg_fp ge rs vsp arg fp /\
          FPlocalize j fp' fp.

Lemma eval_builtin_arg_fp_localize:
  forall j bound fl ge ge' rs rs' vsp vsp' arg fp,
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Senv.find_symbol ge id) (Senv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    val_related (construct_inj j bound fl) vsp vsp' ->
    MemOpFP.eval_builtin_arg_fp ge rs vsp arg fp ->
    exists fp', MemOpFP.eval_builtin_arg_fp ge' rs' vsp' arg fp' /\
           FPlocalize (construct_inj j bound fl) fp' fp /\ fpG fl (fun b => Plt b bound) fp'.

Lemma eval_builtin_args_related:
  forall j bound fl args ge ge' rs rs' vsp vsp' m m' vargs,
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Senv.find_symbol ge id) (Senv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    val_related (construct_inj j bound fl) vsp vsp' ->
    mem_related j bound fl (strip m') m ->
    Events.eval_builtin_args ge rs vsp m args vargs ->
    exists vargs', AsmLang.eval_builtin_args ge' rs' vsp' m' args vargs' /\
              list_forall2 (val_related (construct_inj j bound fl)) vargs vargs'.

Lemma eval_builtin_args_related':
  forall j bound fl args ge ge' rs rs' vsp vsp' m m' vargs',
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Senv.find_symbol ge id) (Senv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    val_related (construct_inj j bound fl) vsp vsp' ->
    mem_related j bound fl (strip m') m ->
    AsmLang.eval_builtin_args ge' rs' vsp' m' args vargs' ->
    exists vargs, Events.eval_builtin_args ge rs vsp m args vargs /\
             list_forall2 (val_related (construct_inj j bound fl)) vargs vargs'.

Lemma eval_builtin_args_fp_localize':
  forall j args ge ge' rs rs' vsp vsp' fp',
    Bset.inj_inject j ->
    (forall id, option_rel (fun b b' => j b = Some b') (Senv.find_symbol ge id) (Senv.find_symbol ge' id)) ->
    regset_related j rs rs' ->
    val_related j vsp vsp' ->
    MemOpFP.eval_builtin_args_fp ge' rs' vsp' args fp' ->
    exists fp, MemOpFP.eval_builtin_args_fp ge rs vsp args fp /\
          FPlocalize j fp' fp.

Lemma eval_builtin_args_fp_localize:
  forall j bound fl ge ge' rs rs' vsp vsp' args fp,
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Senv.find_symbol ge id) (Senv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    val_related (construct_inj j bound fl) vsp vsp' ->
    MemOpFP.eval_builtin_args_fp ge rs vsp args fp ->
    exists fp', MemOpFP.eval_builtin_args_fp ge' rs' vsp' args fp' /\
           FPlocalize (construct_inj j bound fl) fp' fp /\ fpG fl (fun b => Plt b bound) fp'.

Lemma extcall_arg_related:
  forall j bound fl rs rs' m m' l varg (NOREP: norep fl),
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    Asm.extcall_arg rs m l varg ->
    exists varg', AsmLang.extcall_arg rs' m' l varg' /\ val_related (construct_inj j bound fl) varg varg'.

Lemma extcall_arg_related':
  forall j bound fl rs rs' m m' l varg' (NOREP: norep fl),
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    AsmLang.extcall_arg rs' m' l varg' ->
    exists varg, Asm.extcall_arg rs m l varg /\ val_related (construct_inj j bound fl) varg varg'.

Lemma extcall_arg_fp_localize:
  forall j bound fl rs rs' l fp,
    Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound) ->
    Bset.inj_inject (construct_inj j bound fl)->
    regset_related (construct_inj j bound fl) rs rs' ->
    extcall_arg_fp rs l fp ->
    exists fp', (extcall_arg_fp rs' l fp') /\ (FPlocalize (construct_inj j bound fl) fp' fp) /\
           fpG fl (fun b => Plt b bound) fp'.

Lemma extcall_arg_fp_localize':
  forall j rs rs' l fp',
    Bset.inj_inject j ->
    regset_related j rs rs' ->
    extcall_arg_fp rs' l fp' ->
    exists fp, (extcall_arg_fp rs l fp) /\ (FPlocalize j fp' fp).

Lemma extcall_arguments_related:
  forall j bound fl rs rs' m m' sig vargs (NOREP: norep fl),
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    Asm.extcall_arguments rs m sig vargs ->
    exists vargs', AsmLang.extcall_arguments rs' m' sig vargs' /\
              list_forall2 (val_related (construct_inj j bound fl)) vargs vargs'.

Lemma extcall_arguments_related':
  forall j bound fl rs rs' m m' sig vargs' (NOREP: norep fl),
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    AsmLang.extcall_arguments rs' m' sig vargs' ->
    exists vargs, Asm.extcall_arguments rs m sig vargs /\
             list_forall2 (val_related (construct_inj j bound fl)) vargs vargs'.

Lemma extcall_args_fp_localize:
  forall j bound fl rs rs' sig fp,
    Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound) ->
    Bset.inj_inject (construct_inj j bound fl)->
    regset_related (construct_inj j bound fl) rs rs' ->
    extcall_arguments_fp rs sig fp ->
    exists fp', (extcall_arguments_fp rs' sig fp') /\ (FPlocalize (construct_inj j bound fl) fp' fp) /\
           fpG fl (fun b => Plt b bound) fp'.

Lemma extcall_args_fp_localize':
  forall j rs rs' sig fp',
    Bset.inj_inject j ->
    regset_related j rs rs' ->
    extcall_arguments_fp rs' sig fp' ->
    exists fp, (extcall_arguments_fp rs sig fp) /\ (FPlocalize j fp' fp).

Lemma store_args_related:
  forall j bound fl stk stk' args args' tys m m' (NOREP: norep fl),
    mem_related j bound fl (strip m') m ->
    construct_inj j bound fl stk = Some stk' ->
    list_forall2 (val_related (construct_inj j bound fl)) args args' ->
    option_rel (fun m fm => mem_related j bound fl (strip fm) m)
               (loadframe.store_args m stk args tys)
               (loadframe.store_args_fmem m' stk' args' tys).

Lemma store_args_freelist_unchg:
  forall m stk args tys m',
    loadframe.store_args_fmem m stk args tys = Some m' ->
    FMemory.Mem.freelist m' = FMemory.Mem.freelist m /\
    FMemory.Mem.validblocks m' = FMemory.Mem.validblocks m.


Lemma store_args_fp_localize:
  forall j bound fl stk stk' tyl,
    Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound) ->
    Bset.inj_inject (construct_inj j bound fl) ->
    construct_inj j bound fl stk = Some stk' ->
    FPlocalize (construct_inj j bound fl) (loadframe.store_args_fp stk' tyl) (loadframe.store_args_fp stk tyl) /\
    fpG fl (fun b => Plt b bound) (loadframe.store_args_fp stk' tyl).

Lemma exec_locked_instr_related:
  forall j ge ge' i rs rs' m m' fl bound,
    fl = FMemory.Mem.freelist m' ->
    norep fl ->
    no_overlap fl (fun b : block => Plt b bound) ->
    (Bset.inject j (fun b => Plt b bound) (fun b => Plt b bound)) ->
    (forall id, option_rel (fun b b' => (construct_inj j bound fl) b = Some b') (Genv.find_symbol ge id) (Genv.find_symbol ge' id)) ->
    regset_related (construct_inj j bound fl) rs rs' ->
    mem_related j bound fl (strip m') m ->
    outcome_related j bound fl (ASM_local.exec_locked_instr ge i rs m) (AsmLang.exec_locked_instr ge' i rs' m') /\
    FPlocalize (construct_inj j bound fl) (AsmLang.exec_locked_instr_fp ge' i rs' m')
               (ASM_local.exec_locked_instr_fp ge i rs m) /\
    fpG fl (fun b => Plt b bound) (AsmLang.exec_locked_instr_fp ge' i rs' m').

Lemma exec_locked_instr_freelist_unchg:
  forall ge i rs rs' m m',
    AsmLang.exec_locked_instr ge i rs m = AsmLang.Next rs' m' ->
    Mem.freelist m' = Mem.freelist m.

Inductive match_core (j: Bset.inj) : core -> core -> Prop :=
| match_state_intro:
    forall rs_local rs lf_local lf,
      regset_related j rs_local rs ->
      loadframe_related j lf_local lf ->
      match_core j (Core_State rs_local lf_local) (Core_State rs lf)
| match_state_callin:
    forall b b' args args' tys oty,
      j b = Some b' ->
      list_forall2 (val_related j) args args' ->
      match_core j (Core_CallstateIn b args tys oty) (Core_CallstateIn b' args' tys oty)
| match_state_callout:
    forall ef args rs lf args' rs' lf',
      list_forall2 (val_related j) args args' ->
      regset_related j rs rs' ->
      loadframe_related j lf lf' ->
      match_core j (Core_CallstateOut ef args rs lf) (Core_CallstateOut ef args' rs' lf')
| match_state_lockstate:
    forall rs rs' signal lf lf',
      regset_related j rs rs' ->
      loadframe_related j lf lf' ->
      match_core j (Core_LockState rs signal lf) (Core_LockState rs' signal lf').


Definition wdcu (cu: Asm_comp_unit) : Prop :=
  nodup_ef (cu_defs cu) = true /\ nodup_gd_ident (cu_defs cu) = true.

Theorem asm_lift: LangLift Asm_comp_unit wdcu AsmLang Asm_IS.


Lemma embed_eq:
  forall fm m,
    embed (strip fm) (Mem.freelist fm) m ->
    m = fm.

Theorem asm_localize: LangLocalize Asm_comp_unit wdcu AsmLang Asm_IS.