Library mcertikos.trap.TrapGen

Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.

Require Import LayerCalculusLemma.
Require Import AbstractDataType.

Require Import LoadStoreSem3high.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Require Import TTrap.
Require Export TrapArgGen.
Require Import TrapGenSpec.

Definition of the refinement relation

Section Refinement.

  Local Open Scope string_scope.
  Local Open Scope error_monad_scope.
  Local Open Scope Z_scope.

  Context `{single_oracle_prop: SingleOracleProp}.
  Context `{real_params : RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.

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

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

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

Proofs the one-step forward simulations for the low level specifications

    Section OneStep_Forward_Relation.

      Section FRESH_PIM.

        Lemma sys_getc_kernel_mode:
          ∀ d2 d2´,
            sys_getc_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          unfold sys_getc_spec. intros.
          subdestruct.
          functional inversion Hdestruct.
          functional inversion H0; eauto.
        Qed.

        Lemma sys_getc_spec_ref:
          compatsim (crel HDATA LDATA) (gensem sys_getc_spec) sys_getc_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit sys_getc_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply sys_getc_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma sys_putc_kernel_mode:
          ∀ d2 d2´,
            sys_putc_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          unfold sys_putc_spec. intros.
          subdestruct.
          functional inversion Hdestruct; eauto.
        Qed.

        Lemma sys_putc_spec_ref:
          compatsim (crel HDATA LDATA) (gensem sys_putc_spec) sys_putc_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit sys_putc_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply sys_putc_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_get_quota_kernel_mode:
          ∀ d2 d2´,
            trap_get_quota_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          unfold trap_get_quota_spec. intros.
          destruct (thread_get_curid_spec d2) eqn:Hdestruct; try discriminate.
          subdestruct.
          functional inversion Hdestruct; subst; simpl; auto.
          functional inversion Hdestruct0.
          unfold c, cpu, curid in ×.
          clear c cpu curid.
          subst; auto.
        Qed.

        Lemma trap_get_quota_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_get_quota_spec) trap_get_quota_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_get_quota_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_get_quota_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_mmap_kernel_mode:
          ∀ d2 d2´,
            trap_mmap_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H;
          functional inversion H1; subst; simpl; auto.
        Qed.

        Lemma trap_mmap_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_mmap_spec) trap_mmap_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_mmap_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_mmap_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_sendtochan_kernel_mode:
          ∀ d2 d2´,
            trap_sendtochan_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H1; subst; simpl; auto.
        Qed.

        Lemma trap_sendtochan_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_sendtochan_spec) trap_sendtochan_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_sendtochan_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_sendtochan_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_receivechan_kernel_mode:
          ∀ d2 d2´,
            trap_receivechan_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H1; subst; simpl; auto.
        Qed.

        Lemma trap_receivechan_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_receivechan_spec) trap_receivechan_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_receivechan_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_receivechan_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_intercept_int_window_kernel_mode:
          ∀ d2 d2´,
            trap_intercept_int_window_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H1; subst; simpl; auto.
        Qed.

        Lemma trap_intercept_int_window_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_intercept_int_window_spec) trap_intercept_int_window_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_intercept_int_window_exist; try apply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_intercept_int_window_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_inject_event_kernel_mode:
          ∀ d2 d2´,
            trap_inject_event_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H2; subst; simpl; auto.
        Qed.

        Lemma trap_inject_event_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_inject_event_spec) trap_inject_event_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_inject_event_exist; try apply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_inject_event_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_check_int_shadow_kernel_mode:
          ∀ d2 d2´,
            trap_check_int_shadow_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H2; subst; simpl; auto.
        Qed.

        Lemma trap_check_int_shadow_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_check_int_shadow_spec) trap_check_int_shadow_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_check_int_shadow_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_check_int_shadow_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_check_pending_event_kernel_mode:
          ∀ d2 d2´,
            trap_check_pending_event_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H2; subst; simpl; auto.
        Qed.

        Lemma trap_check_pending_event_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_check_pending_event_spec) trap_check_pending_event_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_check_pending_event_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_check_pending_event_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_get_next_eip_kernel_mode:
          ∀ d2 d2´,
            trap_get_next_eip_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H1; subst; simpl; auto.
          functional inversion H4; subst; simpl; auto.
        Qed.

        Lemma trap_get_next_eip_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_get_next_eip_spec) trap_get_next_eip_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_get_next_eip_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_get_next_eip_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_get_reg_kernel_mode:
          ∀ d2 d2´,
            trap_get_reg_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H;
          functional inversion H1; subst; simpl; auto.
        Qed.

        Lemma trap_get_reg_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_get_reg_spec) trap_get_reg_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_get_reg_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_get_reg_kernel_mode; eauto.
          - constructor.
        Qed.

        Lemma trap_set_reg_kernel_mode:
          ∀ d2 d2´,
            trap_set_reg_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H;
          functional inversion H1; subst; simpl; auto.
        Qed.

        Lemma trap_set_reg_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_set_reg_spec) trap_set_reg_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_set_reg_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_set_reg_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_set_seg1_kernel_mode:
          ∀ d2 d2´,
            trap_set_seg1_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H;
          functional inversion H1; subst; simpl; auto.
        Qed.

        Lemma trap_set_seg1_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_set_seg1_spec) trap_set_seg1_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_set_seg1_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_set_seg1_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_set_seg2_kernel_mode:
          ∀ d2 d2´,
            trap_set_seg2_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H;
          functional inversion H1; subst; simpl; auto.
        Qed.

        Lemma trap_set_seg2_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_set_seg2_spec) trap_set_seg2_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_set_seg2_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_set_seg2_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_get_tsc_offset_kernel_mode:
          ∀ d2 d2´,
            trap_get_tsc_offset_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H2; subst; simpl; auto.
        Qed.

        Lemma trap_get_tsc_offset_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_get_tsc_offset_spec) trap_get_tsc_offset_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_get_tsc_offset_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_get_tsc_offset_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_set_tsc_offset_kernel_mode:
          ∀ d2 d2´,
            trap_set_tsc_offset_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          clear dependent ofs.
          functional inversion H1; subst; simpl; auto.
        Qed.

        Lemma trap_set_tsc_offset_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_set_tsc_offset_spec) trap_set_tsc_offset_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_set_tsc_offset_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_set_tsc_offset_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_get_exitinfo_kernel_mode:
          ∀ d2 d2´,
            trap_get_exitinfo_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H;
          functional inversion H1; subst; simpl; auto;
          functional inversion H13; subst; simpl; auto.
          functional inversion H14; subst; simpl; auto.
        Qed.

        Lemma trap_get_exitinfo_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_get_exitinfo_spec) trap_get_exitinfo_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_get_exitinfo_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_get_exitinfo_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_handle_rdmsr_kernel_mode:
          ∀ d2 d2´,
            trap_handle_rdmsr_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H1; subst; simpl; auto.
          functional inversion H8; subst; simpl; auto.
        Qed.

        Lemma trap_handle_rdmsr_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_handle_rdmsr_spec) trap_handle_rdmsr_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_handle_rdmsr_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_handle_rdmsr_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_handle_wrmsr_kernel_mode:
          ∀ d2 d2´,
            trap_handle_wrmsr_spec d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H1; subst; simpl; auto.
          functional inversion H8; subst; simpl; auto.
        Qed.

        Lemma trap_handle_wrmsr_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_handle_wrmsr_spec) trap_handle_wrmsr_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_handle_wrmsr_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_handle_wrmsr_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma ptfault_resv_kernel_mode:
          ∀ d2 d2´ v,
            ptfault_resv_spec v d2 = Some d2´
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H1.
          - unfold big2_palloc_spec in H5; subdestruct; eauto.
          - unfold big2_palloc_spec in H4; subdestruct; eauto.
        Qed.

        Lemma ptf_resv_spec_ref:
          compatsim (crel HDATA LDATA) (gensem ptfault_resv_spec) ptf_resv_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit ptfault_resv_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply ptfault_resv_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_proc_create_kernel_mode:
          ∀ d2 d2´ v1 v2,
            trap_proc_create_spec v1 v2 d2 = Some d2´
            → kernel_mode d2.
        Proof.
          unfold trap_proc_create_spec. intros.
          destruct (uctx_arg2_spec d2) eqn:Hdestruct; try discriminate.
          functional inversion Hdestruct; subst; simpl; auto.
          unfold uctx_set_errno_spec in H; subdestruct; auto.
        Qed.

        Lemma trap_proc_create_spec_ref:
          compatsim (crel HDATA LDATA) (trap_proccreate_compatsem trap_proc_create_spec) trap_proc_create_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_proc_create_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_proc_create_kernel_mode; eassumption.
          - constructor.
        Qed.

      End FRESH_PIM.

      Lemma passthrough_correct:
        sim (crel HDATA LDATA) ttrap_passthrough ttraparg.
      Proof.
        sim_oplus.         - apply thread_vmxinfo_get_sim.
        - apply big2_palloc_sim.
        - apply thread_ptRead_sim.
        - apply big2_ptResv_sim.         - apply big2_thread_yield_sim.

        - apply thread_get_CPU_ID_sim.
        - apply thread_get_curid_sim.

        - apply thread_uctx_get_sim.
        - apply thread_uctx_set_sim.

        - apply thread_vm_run_sim, VMX_INJECT.
        - apply thread_vmx_return_from_guest_sim.
        - apply thread_vmx_init_sim.

        - apply uctx_arg1_sim.
          intros. eapply valid_curid; eauto.
        - apply uctx_arg2_sim.
          intros. eapply valid_curid; eauto.
        - apply uctx_arg3_sim.
          intros. eapply valid_curid; eauto.
        - apply uctx_arg4_sim.
          intros. eapply valid_curid; eauto.
        - apply uctx_set_errno_sim.
          intros. eapply valid_curid; eauto.
        - apply uctx_set_retval1_sim.
          intros. eapply valid_curid; eauto.

        - apply thread_cli_sim.
        - apply thread_sti_sim.

        - apply thread_trap_info_get_sim.
        - apply thread_trap_info_ret_sim.
        - apply thread_proc_start_user_sim.
          intros. eapply valid_curid; eauto.
        - apply thread_proc_exit_user_sim.
        - apply thread_proc_start_user_sim2.
          intros. eapply valid_curid; eauto.
        - apply thread_proc_exit_user_sim2.

        - layer_sim_simpl.
          + eapply load_correct3high.
          + eapply store_correct3high.
      Qed.

    End OneStep_Forward_Relation.

  End WITHMEM.

End Refinement.