Library mcertikos.mcslock.MCSCurIDGenLink

Require Import LinkTemplate.
Require Import MCSMCurID.
Require Import MCSCurIDGen.
Require Import MCSCurIDGenLinkSource.
Require Import MCSMBoot.
Require Import MCSMBootCSource.
Require Import MCSMBootCode.

Require Import CDataTypes.
Require Import Globalenvs.
Require Import AST.

Section WITHCOMPCERTIKOS.
  Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
  Context `{mcs_oracle_prop: MCSOracleProp}.

  Lemma init_correct:
    init_correct_type MCSMCurID_module mboot mcurid.
  Proof.
    init_correct.
    - edestruct (init_mem_characterization´ p b) as (Hp & _ & _ & Hz); eauto.
      destruct Hz as [Hz _]; eauto.
      simpl in ×.
      econstructor; eauto.

      intros ofs Hofs.
      ∃ Int.zero.
      repeat apply conj.
      + apply load_four_bytes_zero.
        × ∃ ofs; omega.
        × intros i Hi.
          eapply Hz.
          omega.
      + intros i Hi.
        eapply Hp.
        simpl in Hi.
        change (Z.max ?x _) with x.
        omega.
      + simpl.
        ∃ ofs; omega.
      + rewrite ZMap.gi.
        reflexivity.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type MCSMCurID_module mboot mcurid.
  Proof.
    link_correct_aux.
    - link_cfunction get_curid_spec_ref MCSMBOOTCODE.get_curid_code_correct.
    - link_cfunction set_curid_spec_ref MCSMBOOTCODE.set_curid_code_correct.
    - link_cfunction set_curid_init_spec_ref MCSMBOOTCODE.set_curid_init_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type MCSMCurID_module mboot mcurid.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type MCSMCurID_module mboot mcurid.
  Proof.
    make_program_exists link_correct_aux.
  Qed.

End WITHCOMPCERTIKOS.