Library mcertikos.mm.ALInitGenLink

Require Import LinkTemplate.
Require Import MALInit.
Require Import ALInitGen.
Require Import ALInitGenLinkSource.
Require Import ALInitGenAsm.
Require Import MContainer.
Require Import MContainerCSource.
Require Import MContainerCode.

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 MALInit_module mcontainer malinit.
  Proof.
    init_correct.
    - eapply relateat.
    - econstructor; eauto.
      rewrite !ZMap.gi.
      constructor.
    - econstructor; eauto.
      intros ofs Hofs.
      edestruct (init_mem_characterization´ p b2) as (Hp & _ & _ & Hz); eauto.
      ∃ Vzero.
      repeat apply conj; eauto.
      + simpl in Hz.
        destruct Hz as [Hz _]; eauto.
        eapply load_four_bytes_zero.
        × ∃ ofs.
          reflexivity.
        × intros i Hi.
          eapply Hz.
          omega.
      + intros i Hi.
        eapply Hp.
        unfold globvar_map.
        simpl in Hi |- ×.
        change (Z.max ?x _) with x.
        xomega.
      + ∃ ofs; reflexivity.
      + rewrite ZMap.gi.
        constructor.
    - econstructor; eauto.
      intros ofs Hofs.
      edestruct (init_mem_characterization´ p b1) as (Hp & _ & _ & Hz); eauto.
      simpl in Hz.
      destruct Hz as [Hz _]; eauto.
      ∃ Vzero, Vzero.
      repeat apply conj; eauto.
      + eapply load_four_bytes_zero.
        × ∃ (ofs × 2); omega.
        × intros i Hi.
          eapply Hz.
          omega.
      + eapply load_four_bytes_zero.
        × ∃ (ofs × 2 + 1); omega.
        × intros i Hi.
          eapply Hz.
          omega.
      + intros i Hi.
        eapply Hp.
        unfold globvar_map.
        simpl in Hi |- ×.
        change (Z.max ?x _) with x.
        omega.
      + ∃ (ofs × 2); simpl; omega.
      + intros i Hi.
        eapply Hp.
        unfold globvar_map.
        simpl in Hi |- ×.
        change (Z.max ?x _) with x.
        omega.
      + ∃ (ofs × 2 + 1); simpl; omega.
      + rewrite ZMap.gi.
        constructor.
    - edestruct (init_mem_characterization´ p b3) as (Hp & _ & Hz & _); eauto.
      destruct Hz as [Hz _]; eauto.
      repeat apply conj; eauto.
      ∃ 0; reflexivity.
    - reflexivity.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type MALInit_module mcontainer malinit.
  Proof.
    link_correct_aux.
    - link_cfunction getatu_spec_ref MCONTAINERCODE.at_get_code_correct.
    - link_cfunction getatnorm_spec_ref MCONTAINERCODE.is_norm_code_correct.
    - link_cfunction getatc_spec_ref MCONTAINERCODE.at_get_c_code_correct.
    - link_cfunction setatu_spec_ref MCONTAINERCODE.at_set_code_correct.
    - link_cfunction setatnorm_spec_ref MCONTAINERCODE.set_norm_correct.
    - link_cfunction setatc_spec_ref MCONTAINERCODE.at_set_c_code_correct.
    - link_cfunction setnps_spec_ref MCONTAINERCODE.set_nps_correct.
    - link_cfunction getnps_spec_ref MCONTAINERCODE.get_nps_code_correct.
    - link_asmfunction acquire_lock_AT_spec_ref acquire_lock_AT_code_correct.
    - link_asmfunction release_lock_AT_spec_ref release_lock_AT_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type MALInit_module mcontainer malinit.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type MALInit_module mcontainer malinit.
  Proof.
    make_program_exists link_correct_aux.
  Qed.
End WITHCOMPCERTIKOS.