Module SimProg

Require Import Events.
Require Import Values.
Require Import AST.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import CoqlibC.
Require Import Skeleton.
Require Import ModSem.
Require Import SimSymb.
Require Import Integers.
Require Import ASTC.
Require Import Maps.
Require Import LinkingC.

Require Import Syntax Sem Mod ModSem.
Require Import SimMem SimModSem SimMod.
Require Import Sound SemProps.

Set Implicit Arguments.





Module ProgPair.
Section PROGPAIR.
Context `{SM: SimMem.class} {SS: SimSymb.class SM} {SU: Sound.class}.

  Definition t := list ModPair.t.

  Definition sim (pp: t) := List.Forall ModPair.sim pp.

  Definition src (pp: t): program := List.map ModPair.src pp.
  Definition tgt (pp: t): program := List.map ModPair.tgt pp.


End PROGPAIR.
End ProgPair.

Hint Unfold ProgPair.sim ProgPair.src ProgPair.tgt.






Section SIM.
Context `{SM: SimMem.class} {SS: SimSymb.class SM} {SU: Sound.class}.

  Variable pp: ProgPair.t.
  Hypothesis SIMPROG: ProgPair.sim pp.
  Let p_src := pp.(ProgPair.src).
  Let p_tgt := pp.(ProgPair.tgt).



  Theorem sim_link_sk
          sk_link_src
          (LOADSRC: p_src.(link_sk) = Some sk_link_src)
          (WF: forall md, In md p_src -> <<WF: Sk.wf md>>):
      exists ss_link sk_link_tgt,
        <<LOADTGT: p_tgt.(link_sk) = Some sk_link_tgt>>
        /\ <<SIMSK: SimSymb.sim_sk ss_link sk_link_src sk_link_tgt>>
        /\ <<LE: Forall (fun mp => (SimSymb.le mp.(ModPair.ss) mp.(ModPair.src) mp.(ModPair.tgt) ss_link)) pp>>.
Proof.
    u. subst_locals. ginduction pp; ii; ss. destruct a; ss.
    unfold ProgPair.src in *. unfold link_sk in *. ss. destruct (classic (t = [])).
    { clarify; ss. cbn in *. clarify. clear IHt. inv SIMPROG. inv H2. inv H1. ss.
      esplits; eauto. econs; eauto. ss. apply SimSymb.le_refl.
    }
    rename H into NNIL. eapply link_list_cons_inv in LOADSRC; cycle 1.
    { destruct t; ss. }
    des. rename sk_link_src into sk_link_link_src. rename restl into sk_link_src.
    inv SIMPROG. exploit IHt; eauto. intro IH; des.
    inv H1. ss. exploit (SimSymb.sim_sk_link); try eapply HD; eauto.
    { eapply WF; et. }
    { eapply link_list_preserves_wf_sk; eauto. }
    { eapply SimSymb.sim_sk_preserves_wf; et. eapply WF; et. }
    { eapply SimSymb.sim_sk_preserves_wf; et. eapply link_list_preserves_wf_sk; eauto. }
    i; des. esplits; eauto.
    - eapply link_list_cons; eauto.
    - econs; eauto. rewrite Forall_forall in *. ii.
      all ltac:(fun H => apply link_list_linkorder in H). des.
      rewrite Forall_forall in *. eapply SimSymb.le_trans; eauto.
      + eapply TL; eauto. destruct x; ss. do 2 (apply in_map_iff; esplits; ss; eauto). ss.
      + eapply IH; eauto. destruct x; ss. do 2 (apply in_map_iff; esplits; ss; eauto). ss.
  Qed.

End SIM.