Library mcertikos.proc.SleeperGenLink

Require Import LinkTemplate.
Require Import PSleeper.
Require Import SleeperGen.
Require Import SleeperGenLinkSource.
Require Import PKContextNew.
Require Import PKContextNewCSource.
Require Import PKContextNewCode.

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

  Lemma init_correct:
    init_correct_type PSleeper_module pkcontextnew psleeper.
  Proof.
    init_correct.
    - edestruct (init_mem_characterization´ p b) as (Hp & _ & _ & Hz); eauto.
      destruct Hz as [Hz _]; eauto.
      simpl in ×.
      pose proof current_CPU_ID_range.
      econstructor; eauto.
      + apply load_four_bytes_zero.
        × ∃ current_CPU_ID; omega.
        × intros i Hi.
          eapply Hz.
          omega.
      + split.
        × intros i Hi.
          eapply Hp.
          simpl in Hi.
          change (Z.max ?x _) with x.
          omega.
        × simpl.
          ∃ current_CPU_ID; omega.
      + unfold init_sleeper.
        rewrite ZMap.gi.
        reflexivity.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type PSleeper_module pkcontextnew psleeper.
  Proof.
    link_correct_aux.
    - link_cfunction sleeper_inc_spec_ref PKCONTEXTNEWCODE.sleeper_inc_code_correct.
    - link_cfunction sleeper_dec_spec_ref PKCONTEXTNEWCODE.sleeper_dec_code_correct.
    - link_cfunction sleeper_zzz_spec_ref PKCONTEXTNEWCODE.sleeper_zzz_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type PSleeper_module pkcontextnew psleeper.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type PSleeper_module pkcontextnew psleeper.
  Proof.
    make_program_exists link_correct_aux.
  Qed.
End WITHCOMPCERTIKOS.