Library mcertikos.proc.QueueIntroGenLink

Require Import LinkTemplate.
Require Import PQueueIntro.
Require Import QueueIntroGen.
Require Import QueueIntroGenLinkSource.
Require Import QueueIntroGenAsm.
Require Import PSleeper.
Require Import PSleeperCSource.
Require Import PSleeperCode.

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 PQueueIntro_module psleeper pqueueintro.
  Proof.
    init_correct.
    - eapply relatetcb.     - constructor.
      + reflexivity.
      + intros i Hi.
        rewrite !ZMap.gi.
        constructor.
    - edestruct (init_mem_characterization´ p b1) as (Hp & _ & _ & Hz); eauto.
      destruct Hz as [Hz _]; eauto.
      simpl in ×.
      constructor.
      intros ofs Hofs.
      ∃ Vzero, Vzero.
      repeat apply conj.
      + apply load_four_bytes_zero.
        × ∃ (ofs × 2 + num_proc × 4)%Z; omega.
        × intros i Hi.
          eapply Hz.
          omega.
      + intros i Hi.
        eapply Hp.
        simpl in Hi.
        xomega.
      + simpl.
        ∃ (ofs × 2 + (num_proc × 4)); omega.
      + apply load_four_bytes_zero.
        × ∃ (ofs × 2 + 1 + num_proc × 4)%Z; omega.
        × intros i Hi.
          eapply Hz.
          omega.
      + intros i Hi.
        eapply Hp.
        simpl in Hi.
        xomega.
      + simpl.
        ∃ (ofs × 2 + 1 + (num_proc × 4)); omega.
      + rewrite ZMap.gi.
        constructor.
    - edestruct (init_mem_characterization´ p b1) as (Hp & _ & _ & Hz); eauto.
      destruct Hz as [Hz _]; eauto.
      simpl in ×.
      constructor.
      intros ofs Hofs.
      ∃ Vzero, Vzero, Vzero, Vzero.
      repeat apply conj.
      + apply load_four_bytes_zero.
        × ∃ (ofs × 4)%Z; omega.
        × intros i Hi.
          eapply Hz.
          omega.
      + 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 PQueueIntro_module psleeper pqueueintro.
  Proof.
    link_correct_aux.
    - link_cfunction get_state_spec_ref PSLEEPERCODE.get_state_code_correct.
    - link_cfunction get_prev_spec_ref PSLEEPERCODE.get_prev_code_correct.
    - link_cfunction get_next_spec_ref PSLEEPERCODE.get_next_code_correct.
    - link_cfunction tcb_get_CPU_ID_spec_ref PSLEEPERCODE.tcb_get_CPU_ID_code_correct.
    - link_cfunction set_state_spec_ref PSLEEPERCODE.set_state_code_correct.
    - link_cfunction set_prev_spec_ref PSLEEPERCODE.set_prev_code_correct.
    - link_cfunction set_next_spec_ref PSLEEPERCODE.set_next_code_correct.
    - link_cfunction tcb_set_CPU_ID_spec_ref PSLEEPERCODE.tcb_set_CPU_ID_code_correct.
    - link_cfunction tcb_init_spec_ref PSLEEPERCODE.tcb_init_code_correct.
    - link_cfunction get_head_spec_ref PSLEEPERCODE.get_head_code_correct.
    - link_cfunction get_tail_spec_ref PSLEEPERCODE.get_tail_code_correct.
    - link_cfunction set_head_spec_ref PSLEEPERCODE.set_head_code_correct.
    - link_cfunction set_tail_spec_ref PSLEEPERCODE.set_tail_code_correct.
    - link_cfunction tdq_init_spec_ref PSLEEPERCODE.tdq_init_code_correct.
    - link_asmfunction acquire_lock_TCB_spec_ref acquire_lock_TCB_code_correct.
    - link_asmfunction release_lock_TCB_spec_ref release_lock_TCB_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type PQueueIntro_module psleeper pqueueintro.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type PQueueIntro_module psleeper pqueueintro.
  Proof.
    make_program_exists link_correct_aux.
  Qed.
End WITHCOMPCERTIKOS.