Library mcertikos.ipc.IPCGenLink

Require Import HAsmLinkTemplate.
Require Import PIPC.
Require Import IPCGen.
Require Import IPCGenLinkSource.
Require Import PIPCIntro.
Require Import PIPCIntroCSource.
Require Import PIPCIntroCode.
Require Import GlobalOracleProp.
Require Import SingleOracle.

Section WITHCOMPCERTIKOS.

  Context `{single_oracle_prop: SingleOracleProp}.
  Context `{real_params : RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{compcertkos: CompCertiKOS}.
  Context `{multi_oracle_link: !MultiOracleLink}.

  Lemma init_correct:
    init_correct_type PIPC_module pipcintro pipc.
  Proof.
    init_correct.
    - destruct (init_data_low_level_invariant (genv_next s)); eauto.
    - destruct (init_data_low_level_invariant (genv_next s)); eauto.
      repeat intro.
      edestruct kctxt_INJECT; eauto.
    - destruct (init_data_low_level_invariant (genv_next s)); eauto.
      repeat intro.
      edestruct uctxt_INJECT; eauto.
    - destruct (init_data_low_level_invariant (genv_next s)); eauto.
      repeat intro.
      assert (vmcs2 = vmcs1) as Hvmcs by congruence.
      rewrite Hvmcs.
      specialize (VMCS_INJECT vmid vmcs1 H0 H1).
      destruct VMCS_INJECT; eauto.
      constructor.
      intro.
      edestruct H3; eauto.
    - destruct (init_data_low_level_invariant (genv_next s)); eauto.
      repeat intro.
      assert (vmx2 = vmx1) as Hvmx by congruence.
      rewrite Hvmx.
      specialize (VMX_INJECT vmid vmx1 H0 H1).
      destruct VMX_INJECT; eauto.
      constructor.
      intro.
      edestruct H3; eauto.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type PIPC_module pipcintro pipc.
  Proof.
    link_correct_aux.
    - link_cfunction
        syncsendto_chan_spec_ref
        PIPCINTROCODE.syncsendto_chan_code_correct.
    - link_cfunction
        syncreceive_chan_spec_ref
        PIPCINTROCODE.syncreceive_chan_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type PIPC_module pipcintro pipc.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type PIPC_module pipcintro pipc.
  Proof.
    make_program_exists link_correct_aux.
  Qed.

End WITHCOMPCERTIKOS.