Library mcertikos.proc.VMCSInitGenLink

Require Import LinkTemplate.
Require Import VVMCSInit.
Require Import VMCSInitGen.
Require Import VMCSInitGenLinkSource.
Require Import VVMCSIntro.
Require Import VVMCSIntroCSource.
Require Import VVMCSIntroCode.
Require Import VVMCSIntroCodeSetDesc.
Require Import VVMCSIntroCodeSetDefaults.

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 VVMCSInit_module vmcsintro vmcsinit.
  Proof.
    init_correct.
    - repeat intro.
      rewrite <- H1, <- H2.
      rewrite ZMap.gi.
      econstructor; eauto.
      intro; rewrite ZMap.gi; eauto.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type VVMCSInit_module vmcsintro vmcsinit.
  Proof.
    link_correct_aux.
    - link_cfunction
        vmx_set_intercept_intwin_spec_ref
        VMCSINTROCODE.vmx_set_intercept_intwin__code_correct.
    - link_cfunction
        vmx_set_desc1_spec_ref
        VMCSINTROCODESETDESC.vmx_set_desc1_body__code_correct.
    - link_cfunction
        vmx_set_desc2_spec_ref
        VMCSINTROCODESETDESC.vmx_set_desc2_body__code_correct.
    - link_cfunction
        vmx_inject_event_spec_ref
        VMCSINTROCODE.vmx_inject_event__code_correct.
    - link_cfunction
        vmx_set_tsc_offset_spec_ref
        VMCSINTROCODE.vmx_set_tsc_offset__code_correct.
    - link_cfunction
        vmx_get_tsc_offset_spec_ref
        VMCSINTROCODE.vmx_get_tsc_offset__code_correct.
    - link_cfunction
        vmx_get_exit_reason_spec_ref
        VMCSINTROCODE.vmx_get_exit_reason__code_correct.
    - link_cfunction
        vmx_get_exit_fault_addr_spec_ref
        VMCSINTROCODE.vmx_get_exit_fault_addr__code_correct.
    - link_cfunction
        vmx_check_pending_event_spec_ref
        VMCSINTROCODE.vmx_check_pending_event__code_correct.
    - link_cfunction
        vmx_check_int_shadow_spec_ref
        VMCSINTROCODE.vmx_check_int_shadow__code_correct.
    - link_cfunction
        vmcs_set_defaults_spec_ref
        VMCSINTROCODE.vmcs_set_defaults__code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type VVMCSInit_module vmcsintro vmcsinit.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type VVMCSInit_module vmcsintro vmcsinit.
  Proof.
    make_program_exists link_correct_aux.
  Qed.

End WITHCOMPCERTIKOS.