Library mcertikos.trap.TrapGenLink

Require Import HAsmLinkTemplate.
Require Import TTrap.
Require Import TrapGen.
Require Import TrapGenLinkSource.
Require Import TTrapArg.
Require Import TTrapArgCSource.
Require Import TTrapArgCSource2.
Require Import TTrapArgCode.
Require Import TTrapArgCode1.
Require Import TTrapArgCode2.
Require Import TTrapArgCode3.
Require Import TTrapArgCode4.
Require Import TTrapArgCode5.

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 TTrap_module ttraparg ttrap.
  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 TTrap_module ttraparg ttrap.
  Proof.
    link_correct_aux.
    - link_cfunction
        ptf_resv_spec_ref
        TTRAPARGCODE2.ptfault_resv_code_correct.
    - link_cfunction
        trap_proc_create_spec_ref
        TTRAPARGCODE2.sys_proc_create_code_correct.
    - link_cfunction
        trap_get_quota_spec_ref
        TTRAPARGCODE.sys_get_quota_code_correct.
    - link_cfunction
        trap_receivechan_spec_ref
        TTRAPARGCODE.sys_receive_chan_code_correct.
    - link_cfunction
        trap_sendtochan_spec_ref
        TTRAPARGCODE.sys_sendto_chan_code_correct.
    - link_cfunction
        trap_inject_event_spec_ref
        TTRAPARGCODE.sys_inject_event_code_correct.
    - link_cfunction
        trap_check_int_shadow_spec_ref
        TTRAPARGCODE.sys_check_int_shadow_code_correct.
    - link_cfunction
        trap_check_pending_event_spec_ref
        TTRAPARGCODE.sys_check_pending_event_code_correct.
    - link_cfunction
        trap_intercept_int_window_spec_ref
        TTRAPARGCODE.sys_intercept_int_window_code_correct.
    - link_cfunction
        trap_get_next_eip_spec_ref
        TTRAPARGCODE.sys_get_next_eip_code_correct.
    - link_cfunction
        trap_get_reg_spec_ref
        TTRAPARGCODE.sys_get_reg_body_code_correct.
    - link_cfunction
        trap_set_reg_spec_ref
        TTRAPARGCODE.sys_set_reg_body_code_correct.
    - link_cfunction
        trap_set_seg1_spec_ref
        TTRAPARGCODE.sys_set_seg1_body_code_correct.
    - link_cfunction
        trap_set_seg2_spec_ref
        TTRAPARGCODE.sys_set_seg2_body_code_correct.
    - link_cfunction
        trap_get_tsc_offset_spec_ref
        TTRAPARGCODE.sys_get_tsc_offset_body_code_correct.
    - link_cfunction
        trap_set_tsc_offset_spec_ref
        TTRAPARGCODE.sys_set_tsc_offset_body_code_correct.
    - link_cfunction
        trap_get_exitinfo_spec_ref
        TTRAPARGCODE.sys_get_exitinfo_body_code_correct.
    - link_cfunction
        trap_handle_rdmsr_spec_ref
        TTRAPARGCODE.sys_handle_rdmsr_body_code_correct.
    - link_cfunction
        trap_handle_wrmsr_spec_ref
        TTRAPARGCODE.sys_handle_wrmsr_body_code_correct.
    - link_cfunction
        trap_mmap_spec_ref
        TTRAPARGCODE2.sys_mmap_code_correct.
    - link_cfunction
        sys_getc_spec_ref
        TTRAPARGCODE3.sys_getc_code_correct.
    - link_cfunction
        sys_putc_spec_ref
        TTRAPARGCODE3.sys_putc_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type TTrap_module ttraparg ttrap.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type TTrap_module ttraparg ttrap.
  Proof.
    make_program_exists link_correct_aux.
  Qed.

End WITHCOMPCERTIKOS.