Library mcertikos.proc.CVIntroGenLink

Require Import LinkTemplate.
Require Import PCVIntro.
Require Import CVIntroGen.
Require Import CVIntroGenLinkSource.
Require Import CVIntroGenAsm.
Require Import PAbQueueAtomic.
Require Import PAbQueueAtomicCSource.
Require Import PAbQueueAtomicCode.

Section WITHCOMPCERTIKOS.
  Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{multi_oracle_link: !MultiOracleLink}.

  Lemma init_correct:
    init_correct_type PCVIntro_module pabqueue_atomic pcvintro.
  Proof.
    init_correct.
    - eapply relatesc.     - constructor.
      + reflexivity.
      + intros.
        rewrite !ZMap.gi.
        constructor.
    - edestruct (init_mem_characterization´ p b1) as (Hp & _ & _ & Hz); eauto.
      destruct Hz as [Hz _]; eauto.
      simpl in ×.
      econstructor; eauto.
      intros ofs Hofs.
      ∃ Vzero, Vzero, Vzero, Vzero.
      repeat apply conj.
      + apply load_four_bytes_zero.
        × ∃ (ofs × 4)%Z; omega.
        × intros i Hi.
          eapply Hz.
          xomega.
      + intros i Hi.
        eapply Hp.
        simpl in Hi.
        xomega.
      + simpl.
        ∃ (ofs × 4); omega.
      + apply load_four_bytes_zero.
        × ∃ (ofs × 4 + 1)%Z; omega.
        × intros i Hi.
          eapply Hz.
          omega.
      + intros i Hi.
        eapply Hp.
        simpl in Hi.
        xomega.
      + simpl.
        ∃ (ofs × 4 + 1); omega.
      + apply load_four_bytes_zero.
        × ∃ (ofs × 4 + 2)%Z; omega.
        × intros i Hi.
          eapply Hz.
          omega.
      + intros i Hi.
        eapply Hp.
        simpl in Hi.
        xomega.
      + simpl.
        ∃ (ofs × 4 + 2); omega.
      + apply load_four_bytes_zero.
        × ∃ (ofs × 4 + 3)%Z; omega.
        × intros i Hi.
          eapply Hz.
          omega.
      + intros i Hi.
        eapply Hp.
        simpl in Hi.
        xomega.
      + simpl.
        ∃ (ofs × 4 + 3); omega.
      + rewrite !ZMap.gi.
        constructor.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type PCVIntro_module pabqueue_atomic pcvintro.
  Proof.
    link_correct_aux.
    - link_cfunction get_sync_chan_to_ref PAbQueueAtomicCode.get_sync_chan_to_code_correct.
    - link_cfunction get_sync_chan_paddr_ref PAbQueueAtomicCode.get_sync_chan_paddr_code_correct.
    - link_cfunction get_sync_chan_count_ref PAbQueueAtomicCode.get_sync_chan_count_code_correct.
    - link_cfunction get_sync_chan_busy_ref PAbQueueAtomicCode.get_sync_chan_busy_code_correct.
    - link_cfunction set_sync_chan_to_ref PAbQueueAtomicCode.set_sync_chan_to_code_correct.
    - link_cfunction set_sync_chan_paddr_ref PAbQueueAtomicCode.set_sync_chan_paddr_code_correct.
    - link_cfunction set_sync_chan_count_ref PAbQueueAtomicCode.set_sync_chan_count_code_correct.
    - link_cfunction set_sync_chan_busy_ref PAbQueueAtomicCode.set_sync_chan_busy_code_correct.
    - link_cfunction init_sync_chan_ref PAbQueueAtomicCode.init_sync_chan_code_correct.
    - link_cfunction get_kernel_pa_ref PAbQueueAtomicCode.get_kernel_pa_code_correct.
    - link_asmfunction acquire_lock_Chan_spec_ref acquire_lock_SC_code_correct.
    - link_asmfunction release_lock_SC_spec_ref release_lock_SC_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type PCVIntro_module pabqueue_atomic pcvintro.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type PCVIntro_module pabqueue_atomic pcvintro.
  Proof.
    make_program_exists link_correct_aux.
  Qed.

End WITHCOMPCERTIKOS.