Module Theorems

Require Import CompAnnot.
Import Coqlib Errors Smallstep Behaviors CompAnnot Maps.
Import AST Globalenvs.
Require RTLdefgenproof.
Require CsharpminorAnalysisproof.
Require CSE2proof.
Require Renumber2proof.

Lemma rtl_of_cminor_correct:
  forall cse2 num p tp,
    rtl_of_cminor cse2 num p = OK tp ->
    forward_simulation (Cminor.semantics p) (RTL.semantics tp).
Proof.
  intros. unfold rtl_of_cminor, Compiler.time in H.
  repeat rewrite Compiler.compose_print_identity in H.
  simpl in H. case_eq (Selection.sel_program p); intros; rewrite H0 in H; simpl in H; try congruence.
  case_eq (RTLgen.transl_program p0); intros; rewrite H1 in H; simpl in H; try congruence.
  case_eq (Inlining.transf_program (Compiler.total_if Compopts.optim_tailcalls Tailcall.transf_program p1)); intros; rewrite H2 in H; simpl in H; try congruence.
  set (p3 := Compiler.total_if Compopts.optim_constprop Constprop.transf_program (Renumber.transf_program p2)) in *.
  set (p4 := Compiler.total_if Compopts.optim_constprop Renumber.transf_program p3) in *.
  case_eq (Compiler.partial_if Compopts.optim_CSE (if cse2 then CSE2.transf_program else CSE.transf_program) p4); intros; rewrite H3 in H; simpl in H; try congruence.
  case_eq (Compiler.partial_if Compopts.optim_redundancy Deadcode.transf_program p5); intros; rewrite H4 in H; simpl in H; try congruence.
  apply compose_forward_simulation with (CminorSel.semantics p0).
  { apply Selectionproof.transf_program_correct; easy. }
  apply compose_forward_simulation with (RTL.semantics p1).
  { apply RTLgenproof.transf_program_correct; easy. }
  apply compose_forward_simulation with (RTL.semantics p2).
  { apply compose_forward_simulation with (RTL.semantics (Compiler.total_if Compopts.optim_tailcalls Tailcall.transf_program p1)).
    - eapply Compiler.total_if_simulation.
      apply Tailcallproof.transf_program_correct.
    - eapply Inliningproof.transf_program_correct; auto. }
  apply compose_forward_simulation with (RTL.semantics p3).
  { apply compose_forward_simulation with (RTL.semantics (Renumber.transf_program p2)).
    - apply Renumberproof.transf_program_correct.
    - eapply Compiler.total_if_simulation.
      apply Constpropproof.transf_program_correct. }
  apply compose_forward_simulation with (RTL.semantics p4).
  { apply Compiler.total_if_simulation.
    apply Renumberproof.transf_program_correct. }
  apply compose_forward_simulation with (RTL.semantics p5).
  { eapply Compiler.partial_if_simulation; eauto.
    destruct cse2; try apply CSEproof.transf_program_correct; try apply CSE2proof.transf_program_correct. }
  apply compose_forward_simulation with (RTL.semantics p6).
  { eapply Compiler.partial_if_simulation; eauto.
    apply Deadcodeproof.transf_program_correct. }
  apply Unusedglobproof.transf_program_correct. easy.
Qed.

Lemma tp_safe:
  forall unload stack p tp def1 def2,
    doit' unload stack p = OK (tp, def1, def2) ->
    forall beh, program_behaves (RTL.semantics tp) beh -> not_wrong beh.
Proof.
  Local Opaque rtl_of_cminor.
  intros. unfold doit', Compiler.time in H.
  case_eq (cminorannot_of_csyntax unload stack p); intros; rewrite H1 in H; simpl in H; try monadInv H.
  case_eq (CsharpminorAnalysis.vanalysis (Compopts.num_dom tt) (Compopts.max_concretize tt) (Compopts.trace tt) (Compopts.verbose tt) (Compopts.unroll tt) p0); intros; rewrite H2 in H; simpl in H; try monadInv H.
  destruct p1. destruct l; try monadInv H. simpl in H.
  case_eq (cminor_of_cminorannot 0 p0); intros; rewrite H3 in H; simpl in H; try monadInv H.
  case_eq (rtl_of_cminor false id p1); intros; rewrite H4 in H; simpl in H; try monadInv H.
  unfold parallel in H. unfold Compiler.apply_partial in H; simpl in H. unfold Compiler.apply_total in H; simpl in H.
  case_eq (Cshmdefgen.transl_program (fun n : AST.ident => Coqlib.proj_sumbool (MoreRTL.mem n (MoreRTL.collect_annot p2))) p0); intros; rewrite H5 in H; try monadInv H.
  case_eq (CsharpminorAnalysis.vanalysis (Compopts.num_dom tt) (Compopts.max_concretize tt) (Compopts.trace tt) (Compopts.verbose tt) (Compopts.unroll tt) p3); intros; rewrite H6 in H; simpl in H; try monadInv H.
  destruct p4. destruct l; try monadInv H.
  case_eq (cminor_of_cminorannot 1 p3); intros; setoid_rewrite H7 in H; simpl in H; try monadInv H.
  case_eq (rtl_of_cminor true (BinInt.Z.add 10) p4); intros; rewrite H8 in H; simpl in H; try monadInv H.
  destruct (RTLperm.no_fancy_builtin (Compiler.print (Compiler.print_RTL 19) p5)); try monadInv H.
  case_eq (RTLdefgen.transf_program p2); intros; rewrite H9 in H; simpl in H; try monadInv H.
  case_eq (Renumber2.transf_program p6); intros; rewrite H10 in H; simpl in H; try monadInv H.
  destruct u. generalize (CsharpminorAnalysisproof.vanalysis_sound _ _ _ _ _ _ _ H2). intros HA.
  unfold cminor_of_cminorannot in H3; simpl in H3. unfold Compiler.time in H3.
  unfold Compiler.apply_total in H3; simpl in H3. unfold Compiler.print in H3.
  case_eq (Cminorgen.transl_program p0); intros; rewrite H in H3; inv H3.
  generalize (Cminorgenproof.transl_program_correct _ _ H). intros HB.
  generalize (rtl_of_cminor_correct _ _ _ _ H4). intros HC.
  generalize (compose_forward_simulation HB HC). intros HD.
  generalize (forward_to_backward_simulation HD (Csharpminorannot.semantics_receptive _) (RTL.semantics_determinate _)). intros HE.
  exploit backward_simulation_same_safe_behavior; eauto.
Qed.

Lemma def2_is_defgen_of_tp:
  forall unload stack p tp def1 def2,
    doit' unload stack p = OK (tp, def1, def2) ->
    exists tp', RTLdefgen.transf_program tp = OK tp' /\ Renumber2.transf_program tp' = OK def2.
Proof.
  Local Opaque rtl_of_cminor.
  intros. unfold doit', Compiler.time in H.
  case_eq (cminorannot_of_csyntax unload stack p); intros; rewrite H0 in H; simpl in H; try monadInv H.
  case_eq (CsharpminorAnalysis.vanalysis (Compopts.num_dom tt) (Compopts.max_concretize tt) (Compopts.trace tt) (Compopts.verbose tt) (Compopts.unroll tt) p0); intros; rewrite H1 in H; simpl in H; try monadInv H.
  destruct p1. destruct l; try monadInv H. simpl in H.
  case_eq (cminor_of_cminorannot 0 p0); intros; rewrite H2 in H; simpl in H; try monadInv H.
  case_eq (rtl_of_cminor false id p1); intros; rewrite H3 in H; simpl in H; try monadInv H.
  unfold parallel in H. unfold Compiler.apply_partial in H; simpl in H. unfold Compiler.apply_total in H; simpl in H.
  case_eq (Cshmdefgen.transl_program (fun n : AST.ident => Coqlib.proj_sumbool (MoreRTL.mem n (MoreRTL.collect_annot p2))) p0); intros; rewrite H4 in H; try monadInv H.
  case_eq (CsharpminorAnalysis.vanalysis (Compopts.num_dom tt) (Compopts.max_concretize tt) (Compopts.trace tt) (Compopts.verbose tt) (Compopts.unroll tt) p3); intros; rewrite H5 in H; simpl in H; try monadInv H.
  destruct p4. destruct l; try monadInv H.
  case_eq (cminor_of_cminorannot 1 p3); intros; setoid_rewrite H6 in H; simpl in H; try monadInv H.
  case_eq (rtl_of_cminor true (BinInt.Z.add 10) p4); intros; rewrite H7 in H; simpl in H; try monadInv H.
  destruct (RTLperm.no_fancy_builtin (Compiler.print (Compiler.print_RTL 19) p5)); try monadInv H.
  case_eq (RTLdefgen.transf_program p2); intros; rewrite H8 in H; simpl in H; try monadInv H.
  case_eq (Renumber2.transf_program p6); intros; rewrite H9 in H; simpl in H; try monadInv H.
  unfold Compiler.print; simpl. eauto.
Qed.

Lemma def1_safe:
  forall unload stack p tp def1 def2,
    doit' unload stack p = OK (tp, def1, def2) ->
    forall beh, program_behaves (RTL.semantics def1) beh -> not_wrong beh.
Proof.
  Local Opaque rtl_of_cminor.
  intros. unfold doit', Compiler.time in H.
  case_eq (cminorannot_of_csyntax unload stack p); intros; rewrite H1 in H; simpl in H; try monadInv H.
  case_eq (CsharpminorAnalysis.vanalysis (Compopts.num_dom tt) (Compopts.max_concretize tt) (Compopts.trace tt) (Compopts.verbose tt) (Compopts.unroll tt) p0); intros; rewrite H2 in H; simpl in H; try monadInv H.
  destruct p1. destruct l; try monadInv H. simpl in H.
  case_eq (cminor_of_cminorannot 0 p0); intros; rewrite H3 in H; simpl in H; try monadInv H.
  case_eq (rtl_of_cminor false id p1); intros; rewrite H4 in H; simpl in H; try monadInv H.
  unfold parallel in H. unfold Compiler.apply_partial in H; simpl in H. unfold Compiler.apply_total in H; simpl in H.
  case_eq (Cshmdefgen.transl_program (fun n : AST.ident => Coqlib.proj_sumbool (MoreRTL.mem n (MoreRTL.collect_annot p2))) p0); intros; rewrite H5 in H; try monadInv H.
  case_eq (CsharpminorAnalysis.vanalysis (Compopts.num_dom tt) (Compopts.max_concretize tt) (Compopts.trace tt) (Compopts.verbose tt) (Compopts.unroll tt) p3); intros; rewrite H6 in H; simpl in H; try monadInv H.
  destruct p4. destruct l; try monadInv H.
  case_eq (cminor_of_cminorannot 1 p3); intros; setoid_rewrite H7 in H; simpl in H; try monadInv H.
  case_eq (rtl_of_cminor true (BinInt.Z.add 10) p4); intros; rewrite H8 in H; simpl in H; try monadInv H.
  destruct (RTLperm.no_fancy_builtin (Compiler.print (Compiler.print_RTL 19) p5)); try monadInv H.
  case_eq (RTLdefgen.transf_program p2); intros; rewrite H9 in H; simpl in H; try monadInv H.
  case_eq (Renumber2.transf_program p6); intros; rewrite H10 in H; simpl in H; try monadInv H.
  destruct u0.
  generalize (CsharpminorAnalysisproof.vanalysis_sound _ _ _ _ _ _ _ H6). intros HA.
  unfold cminor_of_cminorannot in H7; simpl in H7. unfold Compiler.time in H7.
  unfold Compiler.apply_total in H7; simpl in H7. unfold Compiler.print in H7.
  case_eq (Cminorgen.transl_program p3); intros; rewrite H in H7; inv H7.
  generalize (Cminorgenproof.transl_program_correct _ _ H). intros HB.
  generalize (rtl_of_cminor_correct _ _ _ _ H8). intros HC.
  generalize (compose_forward_simulation HB HC). intros HD.
  generalize (forward_to_backward_simulation HD (Csharpminorannot.semantics_receptive p3) (RTL.semantics_determinate p5)). intros HE.
  exploit backward_simulation_same_safe_behavior; eauto.
Qed.

Lemma RTLdefgenproof_implies:
  forall unload stack p tp def1 def2,
    doit' unload stack p = OK (tp, def1, def2) ->
    (forall beh, program_behaves (RTL.semantics def2) beh -> not_wrong beh) ->
    (forall beh, program_behaves (RTL.semantics_safe tp) beh -> not_wrong beh).
Proof.
  intros. generalize (def2_is_defgen_of_tp _ _ _ _ _ _ H). intros [tp' [HA HB]].
  assert (HC: forall beh, program_behaves (RTL.semantics tp') beh -> not_wrong beh).
  { intros; exploit backward_simulation_same_safe_behavior; eauto.
    eapply Renumber2proof.transf_program_backward_simulation; eauto. }
  generalize (tp_safe _ _ _ _ _ _ H). intros HD.
  eapply RTLdefgenproof.def_program_safe_implies_annotations_correct; eauto.
Qed.

Lemma if_validated:
  forall unload stack p tp def1 def2,
    doit' unload stack p = OK (tp, def1, def2) ->
    forward_simulation (RTLperm.semantics def1) (RTL.semantics def2) ->
    MoreSemantics.safe (RTL.semantics_safe tp).
Proof.
  intros unload stack p tp def1 def2 H X beh Hsafe.
  eapply RTLdefgenproof_implies; eauto.
  generalize (def1_safe _ _ _ _ _ _ H). intros HA.
  assert (Hsim: forward_simulation (RTL.semantics def1) (RTL.semantics def2)).
  { eapply compose_forward_simulation; eauto.
    eapply RTLperm.simulation. }
  generalize (program_behaves_exists (RTL.semantics def1)). intros [beh' Hbeh].
  generalize (forward_to_backward_simulation Hsim (RTL.semantics_receptive def1) (RTL.semantics_determinate def2)). intros Hbsim.
  intros; exploit backward_simulation_same_safe_behavior; eauto.
Qed.

Theorem annotations_correct:
  forall unload stack printer fuel p tp def1 def2,
    doit' unload stack p = OK (tp, def1, def2) ->
    equivalence_check printer def2 def1 fuel = OK tt ->
    RTLperm.no_fancy_builtin def1 = true ->
    (forall name sig args m tr vres m',
        Events.external_functions_sem name sig (Genv.globalenv def1) args m tr vres m' ->
        RTLperm.eq3 (RTLperm.mem_perm m) (RTLperm.mem_perm m')) ->
    MoreSemantics.safe (RTL.semantics_safe tp).
Proof.
  intros unload stack printer fuel p tp def1 def2 H H0 H1 H2.
  eapply if_validated. exact H. clear H.
  set (ger x := match x with xI y => inl (inr y) | xO y => inl (inl y) | xH => inr tt end).
  refine (ProductSimulation.simulation _ _ _ _ ger _ _ _ _ Pos.max Pos.succ Pos.le
                                      Pos.le_refl Pos.le_trans Sexpr.pos_max_le Sexpr.pos_succ_le_ne
                                      _ _ fuel printer H0 _ H2
         ); try reflexivity.
  eapply RTLperm.consistent_permissions; eauto.
Qed.

Generated by coq2html