Require Import IPCIntroGenDef.
Require Import IPCIntroGenSpec.
Require Import XOmega.
Require Import ObjSyncIPC.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Section Refinement.

  Context `{single_oracle_prop: SingleOracleProp}.
  Context `{real_params : RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

    Ltac pattern2_refinement_simpl:=
      pattern2_refinement_simpl´ (@relate_AbData).

    Lemma syncsendto_chan_pre_spec_ref:
      compatsim (crel HDATA LDATA) (gensem thread_syncsendto_chan_pre_spec) thread_syncsendto_chan_pre_spec_low.
    Proof.
      compatsim_simpl (@match_AbData).
      exploit thread_syncsendto_chan_pre_exist; eauto 1. intros (labd´ & HP & HM).
      refine_split; try econstructor; eauto.
      - unfold thread_syncsendto_chan_pre_spec in HP; subdestruct; now constructor.
      - eapply thread_syncsendto_chan_pre_match. eapply H1. eapply match_match.
    Qed.

    Lemma tryreceive_chan_spec_ref:
      compatsim (crel HDATA LDATA) (gensem thread_tryreceive_chan_spec) thread_tryreceive_chan_spec_low.
    Proof.
      compatsim_simpl (@match_AbData).
      exploit thread_tryreceive_chan_exist; eauto 1. intros (labd´ & HP & HM).
      refine_split; try econstructor; eauto.
      - functional inversion HP; now constructor.
      - eapply thread_tryreceive_chan_match; eauto.
    Qed.

  End WITHMEM.

End Refinement.