Module MCgenproof

Require Import Coqlib Integers Values Maps AST.
Require Import Memtype Memory.
Require Import Smallstep.
Require Import Asm MC MCgen.
Require Import FlatAsm FlatAsmBuiltin 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.


Section WITHMEMORYMODEL.

  Context `{external_calls_ops : ExternalCalls }.
  Existing Instance Asm.mem_accessors_default.
  Existing Instance FlatAsm.mem_accessors_default.
  Existing Instance inject_perm_all.

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

Section PRESERVATION.

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

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

  Inductive match_states : Asm.state -> Asm.state -> Prop :=
  | match_states_intro m rs:
      match_states (State m rs) (State m rs).


  Lemma alloc_global_transl:
    forall lmap d d' m m',
      transl_globdef lmap d = OK d' ->
      alloc_global m d = Some m' ->
      alloc_global m d' = Some m'.

  Lemma alloc_globals_transl:
    forall lmap d d' m m',
      transl_globdefs lmap d = OK d' ->
      alloc_globals m d = Some m' ->
      alloc_globals m d' = Some m'.

  Lemma add_global_symb:
    forall ge1 ge2
      (SSYMB : forall i : ident, Genv.genv_symb ge1 i = Genv.genv_symb ge2 i)
      (NB : Genv.genv_next ge1 = Genv.genv_next ge2)
      lmap a x (EQ : transl_globdef lmap a = OK x),
    forall i0 : ident, Genv.genv_symb (add_global ge1 a) i0 = Genv.genv_symb (add_global ge2 x) i0.

  Lemma add_global_next:
    forall ge1 ge2
      (NB : Genv.genv_next ge1 = Genv.genv_next ge2)
      lmap a x (EQ : transl_globdef lmap a = OK x),
      Genv.genv_next (add_global ge1 a) = Genv.genv_next (add_global ge2 x).

  Lemma add_globals_symb:
    forall lmap d d' (TG: transl_globdefs lmap d = OK d')
      ge1 ge2 (SSYMB: forall i, Genv.genv_symb ge1 i = Genv.genv_symb ge2 i)
      (NB: Genv.genv_next ge1 = Genv.genv_next ge2)
    ,
    forall i, Genv.genv_symb (add_globals ge1 d) i = Genv.genv_symb (add_globals ge2 d') i.

  Lemma symbol_address_same:
    forall i o,
      Genv.symbol_address ge i o = Genv.symbol_address tge i o.

  Lemma store_init_data_transl:
    forall ld m b o m',
      store_init_data ge m b o ld = Some m' ->
      store_init_data tge m b o ld = Some m'.

  Lemma store_init_data_list_transl:
    forall ld m b o m',
      store_init_data_list ge m b o ld = Some m' ->
      store_init_data_list tge m b o ld = Some m'.

  Lemma store_global_transl:
    forall lmap n sb d d' m m',
      transl_globdef lmap d = OK d' ->
      store_global ge n sb m d = Some m' ->
      store_global tge n sb m d' = Some m'.

  Lemma store_globals_iter_transl:
    forall lmap sb d d' n m m',
      transl_globdefs lmap d = OK d' ->
      store_globals_iter ge n sb m d = Some m' ->
      store_globals_iter tge n sb m d' = Some m'.

  Lemma store_globals_transl:
    forall lmap sb d d' m m',
      transl_globdefs lmap d = OK d' ->
      store_globals ge sb m d = Some m' ->
      store_globals tge sb m d' = Some m'.


Lemma transf_initial_states :
  forall rs st1,
    FlatAsm.initial_state prog rs st1 ->
    exists st2, MC.initial_state tprog rs st2 /\ match_states st1 st2.




Lemma eval_addrmode32_same:
  forall am rs,
    eval_addrmode32 ge am rs = eval_addrmode32 tge am rs.

Lemma eval_addrmode64_same:
  forall am rs,
    eval_addrmode64 ge am rs = eval_addrmode64 tge am rs.

Lemma eval_addrmode_same:
  forall am rs,
    eval_addrmode ge am rs = eval_addrmode tge am rs.

Lemma exec_load_step:
  forall ch m am rs pr o,
    exec_load ge ch m am rs pr o = exec_load tge ch m am rs pr o.

Lemma exec_store_step:
  forall ch m am rs pr lpr o,
    exec_store ge ch m am rs pr lpr o = exec_store tge ch m am rs pr lpr o.

Lemma acc_instrs_map_codeblock:
  forall I smap b ofs i sb id code acc
    (SMAP: smap code_segid = code_block)
    (INIT: forall i sb id, acc b ofs = Some (i, sb, id) -> b = code_block /\ segblock_id sb = code_segid /\ segblock_start sb = ofs)
    (CODE: Forall (fun '(i,sb,id) => segblock_id sb = code_segid) code)
    (AIM : @acc_instrs_map I smap code acc b ofs = Some (i, sb, id)),
    b = code_block /\ segblock_id sb = code_segid /\ segblock_start sb = ofs.

Lemma code_segid_segid_code_seg:
  code_segid = segid (code_seg prog).

Lemma code_segid_not_segid_data_seg:
  code_segid <> segid (data_seg prog).

Hypothesis lmap_code_seg:
  forall id l s0 i,
    lbl_map prog id l = Some (s0, i) -> s0 = code_segid.

Lemma check_faprog_true: check_faprog prog = true.

Lemma wf_faprog:
  Forall
    (fun '(i, d, _) =>
       forall f : function,
         d = Some (Gfun (Internal f)) ->
         Forall (fun '(ins, sb1, ii) => segblock_id sb1 = code_segid /\ i = ii /\ is_valid_label (lbl_map prog) (ins,sb1,ii)) (fn_code f) /\
         list_norepet (map (get_instr_ptr (gen_segblocks prog)) (fn_code f))
    )
    (prog_defs prog).

Lemma prog_in_code_block:
  Forall
    (fun '(_, d, _) =>
       forall f : function,
         d = Some (Gfun (Internal f)) ->
         Forall (fun '(_, sb1, _) => segblock_id sb1 = code_segid) (fn_code f))
    (prog_defs prog).

  
Lemma labels_valid:
  Forall (fun '(_,o,_) =>
            forall f,
              o = Some (Gfun (Internal f)) ->
              Forall (is_valid_label (lbl_map prog)) (fn_code f)
         ) (prog_defs prog).

Lemma code_lnr:
  Forall (fun '(_,o,_) =>
            forall f,
              o = Some (Gfun (Internal f)) ->
              list_norepet (map (get_instr_ptr (gen_segblocks prog)) (fn_code f))
         ) (prog_defs prog).

Lemma ident_fun_correct:
  Forall
    (fun '(i,o,sb) =>
       forall f,
         o = Some (Gfun (Internal f)) ->
         Forall
           (fun '(_,ii) => i = ii)
           (fn_code f)
    )
    (prog_defs prog).

Lemma Forall_app:
  forall {A} (P: A -> Prop) (l1 l2: list A),
    Forall P l1 ->
    Forall P l2 ->
    Forall P (l1 ++ l2).

Lemma genv_instrs_codeblock:
  forall b ofs i sb id,
    Forall (fun '(_,d,sb) => forall f,
                d = Some (Gfun (Internal f)) ->
                Forall (fun '(_,sb,_) => segblock_id sb = code_segid) (fn_code f)
           ) (prog_defs prog) ->
    Genv.genv_instrs ge b ofs = Some (i, sb, id) ->
    b = code_block /\ segblock_id sb = code_segid /\ segblock_start sb = ofs.

Lemma genv_lbl_map:
  forall b, Genv.genv_lbl ge b = lblmap_to_symbmap (gen_segblocks prog) (lbl_map prog) b.

Lemma label_correct:
  forall (rs2: regset) b ofs i sb id
    (RPC : rs2 PC = Vptr b ofs)
    (FI : Genv.genv_instrs ge b ofs = Some (i, sb, id))
    l p
    (Heqo1 : lbl_map prog id l = Some p),
    Val.offset_ptr (rs2 PC)
                   (Ptrofs.add (Ptrofs.sub (snd p) (Ptrofs.add (segblock_start sb) (segblock_size sb)))
                               (segblock_size sb)) = Genv.label_address ge id l.

Lemma get_lbl_list_offset_ok:
  forall lmap id tbl sb tbl' o l,
    get_lbl_list_offset lmap id tbl sb = OK tbl' ->
    list_nth_z tbl o = Some l ->
    exists ofs,
      list_nth_z tbl' o = Some ofs /\ get_lbl_offset lmap id l sb = OK ofs.

Lemma exec_instr_step : forall rs1 m1 rs2 m2
                          (MINJ: match_states (State rs1 m1) (State rs2 m2))
                          b ofs i i' rs1' m1',
    rs1 PC = Vptr b ofs ->
    Genv.find_instr ge (Vptr b ofs) = Some i ->
    FlatAsm.exec_instr ge i rs1 m1 = Next rs1' m1' ->
    transl_instr (lbl_map prog) (snd i) i = OK i' ->
    exists rs2' m2',
      MC.exec_instr tge i' rs2 m2 = Next rs2' m2' /\
      match_states (State rs1' m1') (State rs2' m2').

Lemma acc_instrs_map_app:
  forall {I} sbs l1 l2 acc b o,
    acc_instrs_map (I:=I) sbs (l1 ++ l2) acc b o =
    acc_instrs_map sbs l1 (acc_instrs_map sbs l2 acc) b o.

Lemma segblock_dec:
  forall s1 s2: segblock,
    { s1 = s2 } + { s1 <> s2 }.

Lemma instr_with_info_dec:
  forall {I} (Idec: forall i1 i2 : I, {i1 = i2} + {i1 <> i2}) (i1 i2 : instr_with_info (I:= I)),
    { i1 = i2 } + { i1 <> i2 }.


Axiom asm_instruction_dec:
  forall i1 i2: Asm.instruction, {i1 = i2} + {i1 <> i2}.

Lemma testcond_dec:
  forall t1 t2: testcond, {t1 = t2} + {t1 <> t2}.

Lemma instruction_dec:
  forall i1 i2: instruction, {i1 = i2} + {i1 <> i2}.

Lemma acc_instrs_map_not_in:
  forall {I} sbs l acc b o i,
    acc_instrs_map (I:=I) sbs l acc b o = Some i ->
    ~ In i l ->
    acc b o = Some i.

Lemma in_instrs_in_code:
  forall b o i,
    Genv.genv_instrs ge b o = Some i ->
    exists f id sb,
      In (id, Some (Gfun (Internal f)), sb) (prog_defs prog) /\ In i (fn_code f).

Lemma find_instr_has_transl:
  forall p i,
    Genv.find_instr ge p = Some i ->
    exists i',
      transl_instr (lbl_map prog) (snd i) i = OK i'.

Lemma gen_segblocks_same:
  gen_segblocks tprog = gen_segblocks prog.

Lemma code_segid_same:
  code_seg tprog = code_seg prog.


Lemma data_segid_same:
  data_seg tprog = data_seg prog.

Lemma acc_instrs_map_in:
  forall {I} (Idec: forall i1 i2: I, {i1 = i2} + {i1 <> i2}) (a: @instr_with_info I) sbs l acc b o,
    In a l ->
    (forall b o a, acc b o = Some a -> ~ In a l) ->
    acc_instrs_map sbs l acc b o = Some a ->
    get_instr_ptr sbs a = Vptr b o .

Lemma acc_instrs_map_in':
  forall {I} (Idec: forall i1 i2: I, {i1 = i2} + {i1 <> i2}) (a: @instr_with_info I) sbs l acc b o
    (IN: In a l)
    (LNR: list_norepet (map (get_instr_ptr sbs) l))
    (GIP: get_instr_ptr sbs a = Vptr b o),
    acc_instrs_map sbs l acc b o = Some a.


Lemma acc_instrs_map_not_in':
  forall {I} sbs l acc b o,
    ~ In (Vptr b o) (map (get_instr_ptr sbs) l) ->
    acc_instrs_map (I:=I) sbs l acc b o = acc b o.

Lemma acc_instrs_map_get_instr_ptr:
  forall {I} sbs b o (a: @instr_with_info I) l acc,
    (forall b o, acc b o = Some a -> get_instr_ptr sbs a = Vptr b o) ->
    acc_instrs_map sbs l acc b o = Some a ->
    get_instr_ptr sbs a = Vptr b o.

Lemma acc_instrs_map_in_list:
  forall {I} (Idec: forall i1 i2: I, {i1 = i2} + {i1 <> i2})
    sbs l acc b o (a x: @instr_with_info I)
    (LNRCODE: list_norepet (map (get_instr_ptr sbs) l))
    (AIM: acc_instrs_map sbs l acc b o = Some a)
    (IN: In x l)
    (GIP: get_instr_ptr sbs x = Vptr b o),
    a = x.

Lemma relate_instrs:
  forall {I1 I2} (Idec1: forall i1 i2: I1, {i1 = i2} + {i1 <> i2})
    (Idec1: forall i1 i2: I2, {i1 = i2} + {i1 <> i2}) sbs R d1 d2
    (LF: list_forall2 (fun '(_,o1,_) '(_,o2,_) =>
                         match o1 with
                         | Some (Gfun (Internal f1)) =>
                           match o2 with
                           | Some (Gfun (Internal f2)) =>
                             list_forall2 R (fn_code f1) (fn_code f2)
                           | _ => False
                           end
                         | _ => match o2 with
                           | Some (Gfun (Internal f2)) => False
                           | _ => True
                           end
                         end
                      ) d1 d2)
    (LNRCODE: Forall (fun '(_,o1,_) =>
                         match o1 with
                         | Some (Gfun (Internal f1)) =>
                           list_norepet (map (get_instr_ptr sbs) (fn_code f1))
                         | _ => True
                         end) d1)
     (LNRCODE': Forall (fun '(_,o1,_) =>
                         match o1 with
                         | Some (Gfun (Internal f1)) =>
                           list_norepet (map (get_instr_ptr sbs) (fn_code f1))
                         | _ => True
                         end) d2)
    a1 a2 acc1 acc2 b o
    (REC: forall a1 a2 b o, acc1 b o = Some a1 -> R a1 a2 -> acc2 b o = Some a2)
    (ACC_OK: forall a0 (b2 : block) (o2 : ptrofs), acc1 b2 o2 = Some a0 -> get_instr_ptr sbs a0 = Vptr b2 o2
)
    (DET: forall a b1 b2, R a b1 -> R a b2 -> b1 = b2)
    (RGIP: forall a b, R a b -> get_instr_ptr sbs a = get_instr_ptr sbs b)
    (REL: R a1 a2)
    (AIM: acc_instrs_map (I:= I1) sbs (get_defs_code d1) acc1 b o = Some a1),
    acc_instrs_map (I:= I2) sbs (get_defs_code d2) acc2 b o = Some a2.

Lemma same_instr_ptr_transl_instr:
  forall lmap sbs i c x,
    transl_instr lmap i c = OK x ->
    get_instr_ptr sbs c = get_instr_ptr sbs x.

Lemma same_instr_ptr_transl_instrs:
  forall lmap sbs i c x,
    transl_instrs lmap i c = OK x ->
    map (get_instr_ptr sbs) c = map (get_instr_ptr sbs) x.

Lemma lnr_transl_instrs:
  forall lmap sbs i c x,
    list_norepet (map (get_instr_ptr sbs) c) ->
    transl_instrs lmap i c = OK x ->
    list_norepet (map (get_instr_ptr sbs) x).

Lemma lnr_code_transl:
  forall lmap d x,
    Forall
      (fun '(_, o, _) =>
         forall f : function,
           o = Some (Gfun (Internal f)) ->
           list_norepet (map (get_instr_ptr (gen_segblocks prog)) (fn_code f)))
      d ->
    transl_globdefs lmap d = OK x ->
    Forall
      (fun '(_, o, _) =>
         forall f : function,
           o = Some (Gfun (Internal f)) ->
           list_norepet (map (get_instr_ptr (gen_segblocks prog)) (fn_code f)))
      x.


Lemma find_instr_transl_find_instr:
  forall p i i',
    Genv.find_instr ge p = Some i ->
    transl_instr (lbl_map prog) (snd i) i = OK i' ->
    Genv.find_instr tge p = Some i'.

Lemma codeblock_same:
  forall b,
    Genv.genv_internal_codeblock tge b = Genv.genv_internal_codeblock ge b.

Lemma add_global_genv_senv:
  forall {I} (ge: genv) l,
    Genv.genv_senv (add_global (I:=I) ge l) = Genv.genv_senv ge.

Lemma add_globals_genv_senv:
  forall {I} l (ge: genv),
    Genv.genv_senv (add_globals (I:=I) ge l) = Genv.genv_senv ge.

Lemma senv_equiv:
  Senv.equiv (Genv.genv_senv ge) (Genv.genv_senv tge).

Lemma eval_builtin_arg_preserved:
  forall {I1 I2 A} (ge : genv (I:= I1)) (tge: genv (I:=I2)) (e: A -> val) sp m al vl (EQ: forall i o, Genv.symbol_address tge i o = Genv.symbol_address ge i o),
    FlatAsmBuiltin.eval_builtin_arg _ _ _ _ ge e sp m al vl ->
    FlatAsmBuiltin.eval_builtin_arg _ _ _ _ tge e sp m al vl.

Lemma eval_builtin_args_preserved:
  forall {I1 I2 A} (ge : genv (I:= I1)) (tge: genv (I:=I2)) (e: A -> val) sp m al vl (EQ: forall i o, Genv.symbol_address tge i o = Genv.symbol_address ge i o),
    FlatAsmBuiltin.eval_builtin_args _ _ _ _ ge e sp m al vl ->
    FlatAsmBuiltin.eval_builtin_args _ _ _ _ tge e sp m al vl.


Lemma genv_defs_add_globals_rel:
  forall lmap f b o defs tdefs (ge: genv (I:= Asm.instruction)) (tge : genv (I := instruction))
    (REC: Genv.genv_defs ge b o = Some (Gfun (External f)) ->
          Genv.genv_defs tge b o = Some (Gfun (External f)))
    (NB: Genv.genv_next ge = Genv.genv_next tge),
    Genv.genv_defs (add_globals ge defs) b o = Some (Gfun (External f)) ->
    transl_globdefs lmap defs = OK tdefs ->
    Genv.genv_defs (add_globals tge tdefs) b o = Some (Gfun (External f)).

Lemma find_funct_ptr_transf:
  forall b ofs f,
    Genv.find_funct_ptr ge b ofs = Some (External f) ->
    Genv.find_funct_ptr tge b ofs = Some (External f).


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

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

End PRESERVATION.


End WITHMEMORYMODEL.