Library mcertikos.trap.SysCallGenLink

Require Import HAsmLinkTemplate.
Require Import TSysCall.
Require Import SysCallGen.
Require Import SysCallGenLinkSource.
Require Import TDispatch.
Require Import SysCallGenAsm.
Require Import SysCallGenAsm2.

Require Import GlobalOracleProp.
Require Import SingleOracle.
Require Import SingleAbstractDataType.

Section WITHCOMPCERTIKOS.

  Context `{single_oracle_prop: SingleOracleProp}.
  Context `{real_params : RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{compcertkos: CompCertiKOS}.
  Context `{multi_oracle_link: !MultiOracleLink}.

  Lemma init_correct:
    init_correct_type TSysCall_module tdispatch tsyscall.
  Proof.
    init_correct.
    - destruct (init_data_low_level_invariant (genv_next s)); eauto.
    - destruct (init_data_low_level_invariant (genv_next s)); eauto.
      repeat intro.
      edestruct kctxt_INJECT; eauto.
    - destruct (init_data_low_level_invariant (genv_next s)); eauto.
      repeat intro.
      edestruct uctxt_INJECT; eauto.
    - destruct (init_data_low_level_invariant (genv_next s)); eauto.
      repeat intro.
      assert (vmcs2 = vmcs1) as Hvmcs by congruence.
      rewrite Hvmcs.
      specialize (VMCS_INJECT vmid vmcs1 H0 H1).
      destruct VMCS_INJECT; eauto.
      constructor.
      intro.
      edestruct H3; eauto.
    - destruct (init_data_low_level_invariant (genv_next s)); eauto.
      repeat intro.
      assert (vmx2 = vmx1) as Hvmx by congruence.
      rewrite Hvmx.
      specialize (VMX_INJECT vmid vmx1 H0 H1).
      destruct VMX_INJECT; eauto.
      constructor.
      intro.
      edestruct H3; eauto.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type TSysCall_module tdispatch tsyscall.
  Proof.
    link_correct_aux.
    - match goal with |- cl_sim _ _ ?R ?x ?y ⇒ change (sim R x y) end.
      apply lower_bound.
    - link_asmfunction syscall_dispatch_spec_ref sys_dispatch_code_correct.
    - link_asmfunction pagefault_handler_spec_ref pgf_handler_code_correct.
    - link_asmfunction sys_run_vm_spec_ref sys_run_vm_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type TSysCall_module tdispatch tsyscall.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type TSysCall_module tdispatch tsyscall.
  Proof.
    make_program_exists link_correct_aux.
  Qed.

End WITHCOMPCERTIKOS.