Library mcertikos.trap.TrapArgGenLink

Require Import HAsmLinkTemplate.
Require Import TTrapArg.
Require Import TrapArgGen.
Require Import TrapArgGenLinkSource.
Require Import PIPC.
Require Import PIPCCSource.
Require Import PIPCCode.
Require Import LAsmModuleSemSpec.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Section WITHCOMPCERTIKOS.

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


  Notation HDATA := AbstractDataType.RData.
  Notation LDATA := AbstractDataType.RData.

  Notation HDATAOps := (cdata (cdata_ops := pipcintro_data_ops) HDATA).
  Notation LDATAOps := (cdata (cdata_ops := pipcintro_data_ops) LDATA).

  Definition oplus_monotonic := PseudoJoin.oplus_monotonic
    (A := compatlayer (cdata _ (cdata_ops := pipcintro_data_ops))).
  Definition oplus_sim_monotonic := PseudoJoin.oplus_sim_monotonic.
  Definition right_upper_bound := Structures.right_upper_bound
    (A := compatlayer (cdata _ (cdata_ops := pipcintro_data_ops))).
  Definition left_upper_bound := Structures.left_upper_bound
    (A := compatlayer (cdata _ (cdata_ops := pipcintro_data_ops))).

  Lemma init_correct:
    init_correct_type TTrapArg_module pipc ttraparg.
  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 TTrapArg_module pipc ttraparg.
  Proof.
    link_correct_aux.
    - link_cfunction
         uctx_arg1_spec_ref
         PIPCCODE.uctx_arg1_code_correct.
    - link_cfunction
         uctx_arg2_spec_ref
         PIPCCODE.uctx_arg2_code_correct.
    - link_cfunction
         uctx_arg3_spec_ref
         PIPCCODE.uctx_arg3_code_correct.
    - link_cfunction
         uctx_arg4_spec_ref
         PIPCCODE.uctx_arg4_code_correct.
    - link_cfunction
         uctx_set_errno_spec_ref
         PIPCCODE.uctx_set_errno_code_correct.
    - link_cfunction
         uctx_set_retval1_spec_ref
         PIPCCODE.uctx_set_retval1_code_correct.
    - link_cfunction
         uctx_set_retval2_spec_ref
         PIPCCODE.uctx_set_retval2_code_correct.
    - link_cfunction
         uctx_set_retval3_spec_ref
         PIPCCODE.uctx_set_retval3_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type TTrapArg_module pipc ttraparg.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type TTrapArg_module pipc ttraparg.
  Proof.
    make_program_exists link_correct_aux.
  Qed.


End WITHCOMPCERTIKOS.