Library mcertikos.proc.UCtxtIntroGenLink

Require Import LinkTemplate.
Require Import PUCtxtIntro.
Require Import UCtxtIntroGen.
Require Import UCtxtIntroGenLinkSource.
Require Import PQThread.
Require Import PQThreadCSource.
Require Import PQThreadCode.
Require Import UCtxtIntroGenAsmSource.
Require Import UCtxtIntroGenAsm.

Require Import PUCtxtIntroDef.
Require Import LAsmModuleSemSpec.
Require Import CDataTypes.
Require Import ObjProc.

Section WITHCOMPCERTIKOS.

  Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{multi_oracle_link: !MultiOracleLink}.

  Lemma make_program_find_symbol (CTXT md : module)(m : mem) s :
    (p <- make_program s (CTXT ⊕ (md
                                    ⊕ UCTX_LOC ↦ uctx_loc_type) ⊕ ∅) (pqthread ⊕ L64);
      ret (Genv.init_mem p) = OK (Some m))
    → ∃ b, find_symbol s UCTX_LOC = Some b ∧
                 ∀ i n,
                   0≤ i < num_proc
                   → 0≤ n < UCTXT_SIZE
                   → Mem.valid_access m Mint32 b (i × UCTXT_SIZE × 4 + n × 4) Writable.
  Proof.
    intros mkprog; inv_monad´ mkprog.
    assert (mkgenv := make_program_make_globalenv _ _ _ _ mkprog0).
    pose proof mkgenv as mkgenv´.
    eapply make_globalenv_stencil_matches in mkgenv´.
    inv_make_globalenv mkgenv. subst.
    rewrite (stencil_matches_symbols _ _ mkgenv´) in ×. inv mkgenv´.
    eexists; split; try eassumption.
    specialize (Genv.init_mem_characterization _ _ Hbvi H0); eauto.
    unfold Genv.perm_globvar; simpl; intros [Hperm _].
    change (Z.max 69632 0) with 69632 in Hperm.
    intros; repeat split.

    - unfold Mem.range_perm; intros; apply Hperm.
      simpl in H.
      unfold size_chunk in H2.
      omega.

    - replace (i × 17 × 4 + n × 4) with ((i × 17 + n) × 4) by ring.
      simpl.
      eexists.
      reflexivity.
  Qed.

  Lemma init_correct:
    init_correct_type PUCtxtIntro_module pqthread puctxtintro.
  Proof.
    init_correct.
    - exploit make_program_find_symbol; eauto.
      intros (b´ & find_symbol_UCTX_LOC & access).
      assert (b´ = b1) by congruence; subst.
      econstructor; try eassumption; intros.

      specialize (access _ _ H0 H1).
      assert (readable : Mem.valid_access m2 Mint32 b1 (i × 17 × 4 + n × 4) Readable).
      { eapply Mem.valid_access_implies; try eassumption; econstructor. }
      destruct (Mem.valid_access_load _ _ _ _ readable) as [v load].
      ∃ v.
      repeat (split; [ eassumption|]).
      split; auto.
      rewrite ZMap.gi.
      rewrite ZMap.gi.
      simpl.
      econstructor.
  Qed.


  Lemma uctx_get_correct :
    ∀ COMPILABLE: LayerCompilable ((UCTX_LOC ↦ uctx_loc_type ⊕ pqthread) ⊕ L64),
    ∀ MOK: ModuleOK (uctx_get ↦ f_uctx_get),
    ∀ M2: LAsm.module,
      CompCertiKOS.transf_module (uctx_get ↦ f_uctx_get) = OK M2 →
      cl_sim _ _
             (crel HDATA LDATA)
             (uctx_get ↦ gensem uctx_get_spec)
             (〚 M2 〛((UCTX_LOC ↦ uctx_loc_type ⊕ pqthread) ⊕ L64)).
  Proof.
    intros.
    eapply link_compiler; eauto.
    - eapply uctx_get_spec_ref.
    - link_nextblock.
    - link_kernel_mode.
    - eapply PQTHREADCODE.uctx_get_code_correct.
    - apply left_upper_bound.
  Qed.

  Lemma uctx_set_correct :
    ∀ COMPILABLE: LayerCompilable ((UCTX_LOC ↦ uctx_loc_type ⊕ pqthread) ⊕ L64),
    ∀ MOK: ModuleOK (uctx_set ↦ f_uctx_set),
    ∀ M2: LAsm.module,
      CompCertiKOS.transf_module (uctx_set ↦ f_uctx_set) = OK M2 →
      cl_sim _ _
             (crel HDATA LDATA)
             (uctx_set ↦ gensem uctx_set_spec)
             (〚 M2 〛((UCTX_LOC ↦ uctx_loc_type ⊕ pqthread) ⊕ L64)).
  Proof.
    intros.
    eapply link_compiler; eauto.
    - eapply uctx_set_spec_ref.
    - link_nextblock.
    - link_kernel_mode.
    - eapply PQTHREADCODE.uctx_set_code_correct.
    - apply left_upper_bound.
  Qed.

  Lemma uctx_set_eip_correct :
    ∀ COMPILABLE: LayerCompilable ((UCTX_LOC ↦ uctx_loc_type ⊕ pqthread) ⊕ L64),
    ∀ MOK: ModuleOK (uctx_set_eip ↦ f_uctx_set_eip),
    ∀ M2: LAsm.module,
      CompCertiKOS.transf_module (uctx_set_eip ↦ f_uctx_set_eip) = OK M2 →
      cl_sim _ _
             (crel HDATA LDATA)
             (uctx_set_eip ↦ (uctx_set_eip_compatsem _))
             (〚 M2 〛((UCTX_LOC ↦ uctx_loc_type ⊕ pqthread) ⊕ L64)).
  Proof.
    intros.
    eapply link_compiler; eauto.
    - eapply uctx_set_eip_spec_ref.
    - link_nextblock.
    - link_kernel_mode.
    - eapply PQTHREADCODE.uctx_set_eip_code_correct.
    - apply left_upper_bound.
  Qed.

  Lemma save_uctx_correct :
    ∀ COMPILABLE: LayerCompilable ((UCTX_LOC ↦ uctx_loc_type ⊕ pqthread) ⊕ L64),
    ∀ MOK: ModuleOK (save_uctx ↦ f_save_uctx),
    ∀ M2: LAsm.module,
      CompCertiKOS.transf_module (save_uctx ↦ f_save_uctx) = OK M2 →
      cl_sim _ _
             (crel HDATA LDATA)
             (save_uctx ↦ (save_uctx_compatsem _))
             (〚 M2 〛((UCTX_LOC ↦ uctx_loc_type ⊕ pqthread) ⊕ L64)).
  Proof.
    intros.
    eapply link_compiler; eauto.
    - eapply save_uctx_spec_ref.
    - link_nextblock.
    - link_kernel_mode.
    - eapply PQTHREADCODE.save_uctx_code_correct.
    - apply oplus_monotonic; [ reflexivity |].
      repeat (apply left_upper_bound || apply le_right).
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type PUCtxtIntro_module pqthread puctxtintro.
  Proof.
    link_correct_aux.
    - eapply uctx_get_correct; code_correct_tac.
    - eapply uctx_set_correct; code_correct_tac.
    - eapply uctx_set_eip_correct; code_correct_tac.
    - eapply save_uctx_correct; code_correct_tac.
    - link_asmfunction restore_uctx_spec_ref restore_uctx_code_correct.
    - link_asmfunction elf_load_spec_ref elf_load_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type PUCtxtIntro_module pqthread puctxtintro.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type PUCtxtIntro_module pqthread puctxtintro.
  Proof.
    make_program_exists link_correct_aux.
  Qed.

End WITHCOMPCERTIKOS.