Module UnreadglobproofC

Require Import FSets CoqlibC Maps Ordered Iteration Errors.
Require Import AST Linking.
Require Import IntegersC ValuesC Memory Globalenvs Events Smallstep.
Require Import Op Registers RTLC.
Require Import Unreadglob.
Require Import sflib.
Require SimMemInjInv.
newly added *
Require Export Unreadglobproof.
Require Import Simulation.
Require Import Skeleton Mod ModSem SimMod SimModSem SimSymb SimMem AsmregsC MatchSimModSem.
Require SimMemInjInvC.
Require SimSymbDropInv.
Require SoundTop.
Require Import CtypingC.
Require Import ModSemProps.
Require Import JunkBlock.

Set Implicit Arguments.



Local Existing Instance SimSymbDropInv.SimMemInvTop.
Local Existing Instance SimSymbDropInv.SimSymbDropInv.

Section SIMMODSEM.

Variable skenv_link_src skenv_link_tgt: SkEnv.t.
Variable sm_link: SimMem.t.
Variable prog: RTL.program.
Variable tprog: RTL.program.
Let md_src: Mod.t := (RTLC.module prog).
Let md_tgt: Mod.t := (RTLC.module tprog).
Hypothesis (INCLSRC: SkEnv.includes skenv_link_src md_src.(Mod.sk)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link_tgt md_tgt.(Mod.sk)).
Hypothesis (WFSRC: SkEnv.wf skenv_link_src).
Hypothesis (WFTGT: SkEnv.wf skenv_link_tgt).
Hypothesis TRANSL: match_prog prog tprog.
Let ge := (SkEnv.revive (SkEnv.project skenv_link_src md_src.(Mod.sk)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link_tgt md_tgt.(Mod.sk)) tprog).
Definition msp: ModSemPair.t :=
  ModSemPair.mk (md_src.(Mod.modsem) skenv_link_src) (md_tgt.(Mod.modsem) skenv_link_tgt)
                ((prog.(defs) -1 tprog.(defs) -1 (Pos.eq_dec tprog.(prog_main))): ident -> Prop)
                sm_link
.

Inductive match_states
          (sm_init: SimMem.t)
          (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
| match_states_intro
    (MATCHST: Unreadglobproof.match_states prog tprog (used_set tprog) skenv_link_src skenv_link_tgt ge tge st_src0 st_tgt0 sm0)
    (MCOMPATSRC: st_src0.(RTL.get_mem) = sm0.(SimMem.src))
    (MCOMPATTGT: st_tgt0.(RTL.get_mem) = sm0.(SimMem.tgt))
.

Lemma find_funct_inject
      invar used fptr tfptr fd j
      (SIMGE: meminj_preserves_globals prog tprog used ge tge invar j)
      (FINDSRC: Genv.find_funct ge fptr = Some fd)
      (INJ: Val.inject j fptr tfptr)
  :
    <<FINDTGT: Genv.find_funct tge tfptr = Some (transf_fundef (transf_function (fun _ i => filter_instr used i)) fd)>>
.
Proof.
  inv SIMGE.
  uge0. des_ifs_safe.
  inv INJ.
  exploit defs_inject; et. i; des. clarify. psimpl. des_ifs.
Qed.

Theorem sim_skenv_meminj_preserves_globals
        sm_arg
        (SIMSKENV:
           SimSymbDropInv.sim_skenv
             sm_arg ((prog.(defs) -1 tprog.(defs) -1 (Pos.eq_dec tprog.(prog_main))): ident -> Prop)
             (SkEnv.project skenv_link_src md_src.(Mod.sk)) (SkEnv.project skenv_link_tgt md_tgt.(Mod.sk)))
  :
    <<SIMGE: meminj_preserves_globals prog tprog (used_set tprog) ge tge (SimMemInjInv.mem_inv_src sm_arg) (SimMemInj.inj sm_arg.(SimMemInjInv.minj))>>
.
Proof.
  exploit SkEnv.project_revive_precise; et.
  { eapply SkEnv.project_impl_spec; et. eapply INCLSRC. }
  { ss. }
  intro GESRC.

  inv SIMSKENV. ss. bar.
  destruct TRANSL as [used0 TRANSL0]. desH TRANSL0. clarify.
  econs.
  - i. exploit SIMSYMB1; et. i; des. clarify. esplits; eauto.
    unfold used_set. des_sumbool. ss. apply not_and_or in KEPT. des; eauto.
    + apply not_and_or in KEPT. des; eauto.
      { exfalso. apply KEPT. inv GESRC. exploit SYMB2P; eauto. }
      { right. apply NNPP in KEPT. unfold defs in KEPT. des_sumbool. ss. }
    + left. apply NNPP in KEPT. des_sumbool. ss.
  - i. exploit SIMSYMB2; et.
    { ii. des. unfold used_set in *. ss. des_sumbool.
      align_bool; bsimpl. des_sumbool.
      des; clarify.
      unfold defs in *. des_sumbool. ss.
    }
  - eauto.
  - ii. dup H0. eapply Genv.find_invert_symbol in H0.
    inv TRANSL1. ss. inv TRANSL0. ss. specialize (match_prog_def id). des_ifs.
    hexploit (SSINV id); eauto. splits.
    + inv GESRC. ss. eapply SYMB2P; eauto.
    + ii. eapply defs_prog_defmap in H2. des. clarify.
    + unfold proj_sumbool in *. rewrite match_prog_main in *. des_ifs.
  - i. unfold ge in H0. exploit Genv_map_defs_def; et. i; des.
    exploit SIMDEF; et. i; des. clarify. psimpl.
    uo. des_ifs_safe.
    exploit Genv.invert_find_symbol; et. intro SYMBSRC; des.
    exploit SIMSYMB1; et. i; des. psimpl. clear_tac.
    exploit Genv.find_invert_symbol; et. intro SYMBTGT; des.

    destruct (classic (defs prog i)); cycle 1.
    { clear - Heq1 H1. contradict H1. unfold defs in *. des_sumbool. apply prog_defmap_spec; et. }
    assert(KEPT0: (defs tprog i \/ Pos.eq_dec (prog_main tprog) i)).
    { tauto. }
    clear KEPT.
    assert(IN: (used_set tprog) i).
    { clarify. unfold used_set. des_sumbool. ss. des; des_sumbool; eauto. right.
      unfold defs in KEPT0. des_sumbool. ss.
    }

    esplits; et.
    + unfold tge.
      unfold SkEnv.revive.
      erewrite Genv_map_defs_def_inv; et.
      uo. des_ifs_safe.
      erewrite match_prog_def; et. rewrite Heq1. ss. des_ifs_safe.
      (* exploit IS.mem_1; et. i; clarify. *)
    + i. eapply used_closed; et.
  - unfold tge. i.
    exploit Genv_map_defs_def; et. i; des.
    uo. des_ifs. bsimpl.
    exploit SIMDEFINV; et. i; des. clarify. psimpl. clear_tac.
    exploit Genv.invert_find_symbol; et. intro SYMBTGT; des.
    exploit SIMSYMB3; et. i; des.
    exploit Genv.find_invert_symbol; et. intro SYMBSRC.

    assert(used_set tprog i).
    { hexploit (match_prog_def _ _ _ TRANSL1 i); et. i. des_ifs. }

    exploit SIMSYMB2; et.
    { unfold used_set in *. clear - H1. des_sumbool.
      ii. des. align_bool; bsimpl. des_sumbool. ss. des; clarify.
      unfold defs in *. des_sumbool. ss.
    }
    i; des.
    clarify. clear_tac.

    assert(blk_src = b).
    { eapply DISJ; et. }
    clarify.

    unfold ge.
    unfold SkEnv.revive.
    erewrite Genv_map_defs_def_inv; et.
    uo.
    des_ifs_safe.

    hexploit (match_prog_def _ _ _ TRANSL1 i); et. intro DEFMAP. des_ifs_safe. unfold option_map in *.
    des_ifs_safe.
    esplits; et.
  - eauto.
Qed.


Let SEGESRC: senv_genv_compat skenv_link_src ge. Proof. eapply SkEnv.senv_genv_compat; et. Qed.
Let SEGETGT: senv_genv_compat skenv_link_tgt tge. Proof. eapply SkEnv.senv_genv_compat; et. Qed.
Theorem sim_modsem
  :
    ModSemPair.sim msp
.
Proof.
  (* rr in TRANSL. destruct TRANSL as [TRANSL0 TRANSL1]. *)
  destruct TRANSL as [used0 TRANSL0]. des.
  eapply match_states_sim with (match_states := match_states)
                               (match_states_at := fun _ _ => eq)
                               (sound_state := SoundTop.sound_state);
    eauto; ii; ss.
  - instantiate (1:= Nat.lt). apply lt_wf.
  - eapply SoundTop.sound_state_local_preservation.
  - (* init bsim *)
    (* destruct sm_arg; ss. clarify. *)
    inv INITTGT. des. inv SAFESRC. destruct args_src, args_tgt; ss.
    inv SIMARGS; ss. clarify.
    assert(SIMGE: meminj_preserves_globals prog tprog (used_set tprog) ge tge (SimMemInjInv.mem_inv_src sm_arg) (SimMemInj.inj sm_arg.(SimMemInjInv.minj))).
    { eapply sim_skenv_meminj_preserves_globals; et. apply SIMSKENV. }
    des.
    esplits; eauto; try refl; econs; eauto.
    + inv TYP. folder. ss. inv TYP0.
      exploit find_funct_inject; et. i; des. clarify.
      rpapply match_states_call; ss; eauto.
      { econs; ss; et.
        - inv SIMSKENV. ss. eapply SimSymbDropInv.sim_skenv_symbols_inject; et.
        - inv SIMSKENV. inv MWF. inv WF. inv SIMSKELINK. ss. etrans; eauto. etrans; eauto. rewrite NBSRC. refl.
        - inv SIMSKENV. inv MWF. inv WF. inv SIMSKELINK. ss. etrans; eauto. etrans; eauto. rewrite NBTGT. refl.
      }
      { eapply inject_list_typify_list; eauto. }
      { eapply MWF. }
  - des. inv SAFESRC.
    inv SIMARGS; ss.
    assert(SIMGE: meminj_preserves_globals prog tprog (used_set tprog) ge tge (SimMemInjInv.mem_inv_src sm_arg) (SimMemInj.inj sm_arg.(SimMemInjInv.minj))).
    { eapply sim_skenv_meminj_preserves_globals; et. apply SIMSKENV. }
    exploit find_funct_inject; et. i; des. clarify.
    inv TYP.
    esplits; eauto. econs; try eapply H; eauto.
    + econs; et.
      etrans; try apply LEN; et. symmetry. eapply inject_list_length; et.
    + etrans; try apply LEN; et. symmetry. eapply inject_list_length; et.
  - (* call wf *)
    inv MATCH; ss. inv MATCHST; ss.
  - (* call fsim *)
    des. clear_tac.
    assert(SIMGE: meminj_preserves_globals prog tprog (used_set tprog) ge tge (SimMemInjInv.mem_inv_src sm0) (SimMemInj.inj sm0.(SimMemInjInv.minj))).
    { eapply sim_skenv_meminj_preserves_globals; et. apply SIMSKENV. }
    inv MATCH; ss.
    inv CALLSRC. inv MATCHST; ss. clarify.
    folder.
    inv MCOMPAT; ss. clear_tac.
    inv FPTR; try (by des; ss).
    ss. destruct (Ptrofs.eq_dec ofs1 Ptrofs.zero); clarify; try (by des; ss).
    esplits; try refl; eauto.
    + econs; eauto.
      * folder.
        ss. des_ifs_safe.
        inv SIMGE. uge0. des_ifs_safe. exploit defs_rev_inject; eauto. i; des. clarify. des_ifs_safe. des_ifs.
      * clear EXTERNAL. des. ss. uge0. des_ifs_safe.
        psimpl.
        inv SIMSKENV. inv SIMSKELINK. ss.
        exploit SIMDEF; et. i; des. clarify. des_ifs. esplits; et.
    + econs; ss; et.
  - (* after fsim *)
    des. clear_tac.
    assert(SIMGE: meminj_preserves_globals prog tprog (used_set tprog) ge tge (SimMemInjInv.mem_inv_src sm0) (SimMemInj.inj sm0.(SimMemInjInv.minj))).
    { eapply sim_skenv_meminj_preserves_globals; et. apply SIMSKENV. }
    inv AFTERSRC.
    inv SIMRET; ss. exists (SimMemInjInvC.unlift' sm_arg sm_ret).
    inv MATCH; ss. inv MATCHST; ss.
    inv HISTORY. ss. clear_tac.
    esplits; try refl; eauto.
    + econs; eauto.
    + econs; ss; eauto.
      inv MLE0; ss. inv MLE1; ss.
      inv MCOMPAT. clear_tac.
      rpapply match_states_return; ss; eauto; ss.
      { eapply match_stacks_bound; et; cycle 1.
        { eauto with mem. }
        { eauto with mem. }
        eapply match_stacks_incr; et.
        { i. inv FROZEN. exploit NEW_IMPLIES_OUTSIDE; et. }
      }
      { eapply inject_typify; et. }
      { eapply MWF. }

  - (* final fsim *)
    inv MATCH. inv FINALSRC; inv MATCHST; ss.
    inv STACKS. inv MCOMPAT; ss.
    eexists sm0. esplits; ss; eauto; try refl. econs; ss; eauto.
  - (* step *)
    left; i.
    assert(SIMGE: meminj_preserves_globals prog tprog (used_set tprog) ge tge (SimMemInjInv.mem_inv_src sm0) (SimMemInj.inj sm0.(SimMemInjInv.minj))).
    { eapply sim_skenv_meminj_preserves_globals; et. apply SIMSKENV. }

    esplits; eauto.
    { apply modsem_receptive; et. }
    inv MATCH.
    ii. hexploit (@step_simulation prog tprog (used_set tprog) skenv_link_src skenv_link_tgt); eauto.
    i; des.
    esplits; eauto.
    + left. apply plus_one. econs; eauto. eapply modsem2_determinate; eauto.
    + econs; ss.
      * inv H0; ss; inv MCOMPAT; ss.
      * inv H0; ss; inv MCOMPAT; ss.
Unshelve.
  all: ss; try (by econs).
Qed.

End SIMMODSEM.


Section SIMMOD.

Variable prog: RTL.program.
Variable tprog: RTL.program.
Hypothesis TRANSL: match_prog prog tprog.

Definition mp: ModPair.t :=
  ModPair.mk (RTLC.module prog) (RTLC.module tprog) ((prog.(defs) -1 tprog.(defs) -1 (Pos.eq_dec tprog.(prog_main))): ident -> Prop)
.

Theorem sim_mod
  :
    ModPair.sim mp
.
Proof.
  econs; ss.
  - destruct TRANSL as [used0 TRANSL0]. desH TRANSL0. clarify.
    econs; ss.
    + i. ss. inv TRANSL1.
      specialize (match_prog_def id).
      generalize (Sk.of_program_prog_defmap prog fn_sig id). intro REL0.
      generalize (Sk.of_program_prog_defmap tprog fn_sig id). intro REL1.

      destruct (classic (defs prog id)); cycle 1.
      {
        rewrite <- (Sk.of_program_defs fn_sig) in H.
        inv REL0; align_opt; cycle 1.
        { exploit prog_defmap_image; et. i; des. unfold defs in *. align_bool; bsimpl. align_bool. des_sumbool. ss. }
        unfold fundef in *.
        rewrite H1 in *.
        inv REL1; align_opt; ss; clarify.
        des_ifs.
      }

      assert(KEPT0: defs tprog id \/ Pos.eq_dec (prog_main tprog) id).
      { tauto. }
      clear KEPT.

      assert(IN: used_set tprog id).
      { unfold used_set. des_sumbool. ss. des; et; bsimpl.
        - right. unfold defs in *. des_sumbool. ss.
        - des_sumbool. clarify. tauto.
      }

      des_ifs.
      unfold fundef in *. rewrite match_prog_def in *.
      unfold option_map in *. des_ifs; cycle 1.
      { unfold defs in *. des_sumbool. apply prog_defmap_spec in H. des; clarify. }
      inv REL1. inv REL0.
      destruct g; ss.
      * destruct f; ss.
        { inv H2; ss. des_ifs. inv H4; ss. des_ifs. }
        { inv H2; ss. des_ifs. inv H4; ss. des_ifs. des_sumbool. clarify. }
      * { inv H2; ss. des_ifs. inv H4; ss. des_ifs. inv H5; inv H2; ss. repeat f_equal. destruct i2, i3; ss. }

    + i. ss. inv TRANSL1.
      specialize (match_prog_def id).
      generalize (Sk.of_program_prog_defmap prog fn_sig id). intro REL0.
      generalize (Sk.of_program_prog_defmap tprog fn_sig id). intro REL1.

      des. align_bool; bsimpl. align_bool. des_sumbool.
      inv REL1; ss; align_opt.
      rewrite <- (Sk.of_program_defs fn_sig) in DROP1.
      exploit prog_defmap_image; et. i; des. unfold defs in *; ss. des_sumbool. ss.

    + ii. unfold privs. bsimpl. des. bsimpl. des_sumbool.
      rewrite (Sk.of_program_defs fn_sig). split; ss.
      unfold NW. align_bool; bsimpl. des_sumbool.
      ii.

      exploit used_public; et. intro IN. unfold used_set in IN. des_sumbool. ss. des; clarify; ss.
      unfold defs in *. des_sumbool. ss.

    + inv TRANSL1; ss.

    + inv TRANSL1; ss.
    + ii. des.
      inv TRANSL0.
      assert(PROG0: (prog_defmap tprog) ! id = Some (Gvar gv)).
      {
        (* TODO: make lemma!!!!!!!!!!!!!!!!!!! *)
        generalize (Sk.of_program_prog_defmap tprog fn_sig id). intro REL.
        inv REL; try congruence.
        rewrite PROG in *. clarify.
        inv H2. inv H4. ss. destruct i1, i2; ss.
      }
      inv TRANSL1.
      rewrite match_prog_def in *. des_ifs.
      unfold option_map in PROG0. des_ifs. unfold map_globdef in H1. des_ifs.
      exploit (used_closed id); et. ii.
      exploit used_defined; et. i; des.
      { exploit prog_defmap_dom; et. i; des. specialize (match_prog_def id_drop). des_ifs. rewrite H2 in *.
        unfold defs in DROP1. apply DROP1. des_sumbool. eapply prog_defmap_image; et.
      }
      { clarify. apply DROP0. des_sumbool. ss. }
    + inv TRANSL1. eapply NoDup_norepet; et. rewrite Sk.of_program_defs_names; ss.
    + ii. des. eapply H0. des_sumbool. inv TRANSL1. eauto.
  - ii. eapply sim_modsem; eauto.
Unshelve.
  all: ss.
Qed.

End SIMMOD.