Module Cshmannotgenproof

Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import AST.
Require Import Values.
Require Import Events.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Csharpminor.
Require Import Csharpminorannot.
Require Import Cshmannotgen.

Section CORRECTNESS.

Variable prog: Csharpminor.program.
Variable tprog: Csharpminorannot.program.

Hypothesis TRANSL: transl_program prog = OK tprog.
Definition ge := Genv.globalenv prog.
Definition tge := Genv.globalenv tprog.

Inductive tr_fundef: Csharpminor.fundef -> fundef -> Prop :=
| tr_internal: forall f tf n1 n2,
                 transl_function f n1 = OK (n2, tf) ->
                 tr_fundef (Internal f) (Internal tf)
| tr_external: forall ef,
                 tr_fundef (External ef) (External ef).

Lemma transl_globdefs_spec:
  forall l n l',
    transl_globdefs l n = OK l' ->
    list_forall2 (match_globdef tr_fundef (fun v1 v2 => v1 = v2)) l l'.

Lemma transl_program_spec:
  forall p tp,
  transl_program p = OK tp ->
  match_program tr_fundef (fun v1 v2 => v1 = v2) nil p.(prog_main) p tp.

Lemma symbols_preserved:
  forall s, Genv.find_symbol tge s = Genv.find_symbol ge s.

Lemma function_ptr_translated:
  forall (b: block) (f: Csharpminor.fundef),
  Genv.find_funct_ptr ge b = Some f ->
  exists tf, Genv.find_funct_ptr tge b = Some tf /\ tr_fundef f tf.

Lemma functions_translated:
  forall (v: val) (f: Csharpminor.fundef),
  Genv.find_funct ge v = Some f ->
  exists tf, Genv.find_funct tge v = Some tf /\ tr_fundef f tf.

Lemma public_preserved:
  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.

Lemma varinfo_preserved:
  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.

Lemma init_mem_preserved:
  forall m,
    Genv.init_mem prog = Some m ->
    Genv.init_mem tprog = Some m.

Lemma sig_preserved:
  forall fd tfd,
    tr_fundef fd tfd ->
    Csharpminor.funsig fd = funsig tfd.

Lemma tr_fundef_transl_fundef:
  forall fd tfd,
    tr_fundef fd tfd ->
    exists n1 n2, transl_fundef fd n1 = OK (n2, tfd).

Section EVAL_EXPR.

  Lemma eval_var_addr_preserved:
    forall e id b,
      Csharpminor.eval_var_addr ge e id b ->
      eval_var_addr tge e id b.

  Lemma eval_expr_preserved:
    forall e le m a v,
      Csharpminor.eval_expr ge e le m a v ->
      forall ta n1 n2, transl_expr a n1 = OK (n2, ta) ->
                    eval_expr tge e le m (expr_erase ta) v.

  Lemma eval_exprlist_preserved:
    forall e le m al vl,
      Csharpminor.eval_exprlist ge e le m al vl ->
      forall tal n1 n2, transl_exprlist al n1 = OK (n2, tal) ->
                   eval_exprlist tge e le m (List.map expr_erase tal) vl.

End EVAL_EXPR.

Lemma transl_lstatement_select_switch_case:
  forall ls ls' ls1 n m m',
    transl_lstatement ls m = OK (m', ls') ->
    Csharpminor.select_switch_case n ls = Some ls1 ->
    exists m'' ls2,
      select_switch_case n ls' = Some ls2 /\
      transl_lstatement ls1 m'' = OK (m', ls2).

Lemma transl_lstatement_select_switch_case_none:
  forall ls ls' n m m',
    transl_lstatement ls m = OK (m', ls') ->
    Csharpminor.select_switch_case n ls = None ->
    select_switch_case n ls' = None.

Lemma transl_lstatement_select_switch:
  forall ls ls' n m m',
    transl_lstatement ls m = OK (m', ls') ->
    exists m'', transl_lstatement (Csharpminor.select_switch n ls) m'' = OK (m', select_switch n ls').

Lemma transl_statement_seq_of_lbl_stmt:
  forall ls ls' m m',
    transl_lstatement ls m = OK (m', ls') ->
    transl_statement (Csharpminor.seq_of_lbl_stmt ls) m = OK (m', seq_of_lbl_stmt ls').

Lemma transl_statement_seq_of_lbl_statements:
  forall ls ls' n m m',
    transl_lstatement ls m = OK (m', ls') ->
    exists m'', transl_statement (Csharpminor.seq_of_lbl_stmt (Csharpminor.select_switch n ls)) m'' = OK (m', seq_of_lbl_stmt (select_switch n ls')).

Inductive match_cont: Csharpminor.cont -> Csharpminorannot.cont -> list (ident * env) -> Prop :=
| match_stop:
    match_cont Csharpminor.Kstop Kstop nil
| match_seq:
    forall s ts k tk stk n m,
      transl_statement s n = OK (m, ts) ->
      match_cont k tk stk ->
      match_cont (Csharpminor.Kseq s k) (Kseq ts tk) stk
| match_block:
    forall k tk stk,
      match_cont k tk stk ->
      match_cont (Csharpminor.Kblock k) (Kblock tk) stk
| match_call:
    forall optid f tf e le k tk nm stk n m,
      transl_function f n = OK (m, tf) ->
      match_cont k tk stk ->
      match_cont (Csharpminor.Kcall optid f e le k) (Kcall optid tf e le tk) ((nm, e)::stk).

Inductive match_states: Csharpminor.state -> Csharpminorannot.state -> Prop :=
| match_regular_states:
    forall f tf s ts k tk e le m stk n1 n2 m1 m2
      (TF: transl_function f m1 = OK (m2, tf))
      (TS: transl_statement s n1 = OK (n2, ts))
      (MCONT: match_cont k tk stk),
      match_states (Csharpminor.State f s k e le m) (State tf ts tk e le m)
| match_call_states:
    forall fd tfd args k tk m stk n1 n2
      (TFD: transl_fundef fd n1 = OK (n2, tfd))
      (MCONT: match_cont k tk stk),
      match_states (Csharpminor.Callstate fd args k m) (Callstate tfd args tk m)
| match_return_states:
    forall v k tk m stk
      (MCONT: match_cont k tk stk),
      match_states (Csharpminor.Returnstate v k m) (Returnstate v tk m).

Lemma is_call_cont_preserved:
  forall k tk stk,
    Csharpminor.is_call_cont k ->
    match_cont k tk stk ->
    is_call_cont tk.

Lemma match_cont_call_cont:
  forall k tk stk,
    match_cont k tk stk ->
    match_cont (Csharpminor.call_cont k) (call_cont tk) stk.

Lemma find_label_none_transl_statement:
  forall lbl s ts k tk stk n1 n2,
    transl_statement s n1 = OK (n2, ts) ->
    Csharpminor.find_label lbl s k = None ->
    match_cont k tk stk ->
    find_label lbl ts tk = None
with find_label_ls_none_transl_lstatement:
           forall lbl s ts k tk stk n1 n2,
             transl_lstatement s n1 = OK (n2, ts) ->
             Csharpminor.find_label_ls lbl s k = None ->
             match_cont k tk stk ->
             find_label_ls lbl ts tk = None.

Lemma find_label_transl_statement:
  forall lbl s ts k tk s' k' stk n1 n2,
    transl_statement s n1 = OK (n2, ts) ->
    Csharpminor.find_label lbl s k = Some (s', k') ->
    match_cont k tk stk ->
    exists n3 n4 ts' tk', find_label lbl ts tk = Some (ts', tk') /\
                     transl_statement s' n3 = OK (n4, ts') /\
                     match_cont k' tk' stk
with find_label_ls_transl_statement:
  forall lbl s ts k tk s' k' stk n1 n2,
    transl_lstatement s n1 = OK (n2, ts) ->
    Csharpminor.find_label_ls lbl s k = Some (s', k') ->
    match_cont k tk stk ->
    exists n3 n4 ts' tk', find_label_ls lbl ts tk = Some (ts', tk') /\
                     transl_statement s' n3 = OK (n4, ts') /\
                     match_cont k' tk' stk.

Lemma add_globals_preserves:
  forall P gl (ge: Genv.t fundef unit),
    (forall ge id g, P ge -> In (id, g) gl -> PTree.get id ge.(Genv.genv_symb) = None -> P (Genv.add_global ge (id, g))) ->
    (forall id g, In (id, g) gl -> PTree.get id ge.(Genv.genv_symb) = None) ->
    list_norepet (List.map fst gl) ->
    P ge ->
    P (Genv.add_globals ge gl).

Lemma find_funct_ptr_inversion':
  forall b f,
  Genv.find_funct_ptr tge b = Some f ->
  exists id, Genv.find_symbol tge id = Some b.

Lemma initial_states_simulation:
  forall S, Csharpminor.initial_state prog S ->
       exists R, initial_state tprog R /\ match_states S R.

Lemma final_states_simulation:
  forall S R r,
    match_states S R ->
    Csharpminor.final_state S r ->
    final_state R r.

Lemma step_simulation:
  forall s1 t s1',
    Csharpminor.step ge s1 t s1' ->
    forall s2, match_states s1 s2 ->
          exists s2', step tge s2 t s2' /\ match_states s1' s2'.

Theorem transl_program_correct:
  forward_simulation (Csharpminor.semantics prog) (Csharpminorannot.semantics tprog).

End CORRECTNESS.