Library mcertikos.ticketlog.CurIDGenLink

Require Import LinkTemplate.
Require Import MCurID.
Require Import CurIDGen.
Require Import CurIDGenLinkSource.
Require Import MBoot.
Require Import MBootCSource.
Require Import MBootCode.

Require Import Globalenvs.
Require Import AST.

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

  Lemma init_correct:
    init_correct_type MCurID_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 MCurID_module mboot mcurid.
  Proof.
    link_correct_aux.
    - link_cfunction get_curid_spec_ref MBOOTCODE.get_curid_code_correct.
    - link_cfunction set_curid_spec_ref MBOOTCODE.set_curid_code_correct.
    - link_cfunction set_curid_init_spec_ref MBOOTCODE.set_curid_init_code_correct.
    - apply passthrough_correct.
  Qed.

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

  Theorem make_program_exists:
    make_program_exist_type MCurID_module mboot mcurid.
  Proof.
    make_program_exists link_correct_aux.
  Qed.
End WITHCOMPCERTIKOS.