Library mcertikos.proc.ProcGenLink

Require Import LinkTemplate.
Require Import PProc.
Require Import ProcGen.
Require Import ProcGenLinkSource.
Require Import PUCtxtIntro.
Require Import PUCtxtIntroCSource.
Require Import PUCtxtIntroCode.
Require Import ProcGenAsm.
Require Import ProcGenAsm1.
Require Import ProcGenAsm2.
Require Import ProcGenAsm3.
Require Import ProcGenAsmSource.

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 PProc_module puctxtintro pproc.
  Proof.
    init_correct.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type PProc_module puctxtintro pproc.
  Proof.
    link_correct_aux.
    - link_cfunction biglow_proc_create_spec_ref PUCTXTINTROCODE.proc_create_code_correct.
    - link_asmfunction proc_start_user_spec_ref proc_start_user_code_correct.
    - link_asmfunction proc_exit_user_spec_ref proc_exit_user_code_correct.
    - link_asmfunction proc_start_user_spec_ref2 proc_start_user_code_correct2.
    - link_asmfunction proc_exit_user_spec_ref2 proc_exit_user_code_correct2.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type PProc_module puctxtintro pproc.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type PProc_module puctxtintro pproc.
  Proof.
    make_program_exists link_correct_aux.
  Qed.

End WITHCOMPCERTIKOS.