Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import PrimTMSemantics.
Require Import LAsm.
Require Import XOmega.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.

Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.

Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import INVLemmaProc.

Require Import AbstractDataType.

Require Import LoadStoreSem3high.
Require Import IntelPrimSemantics.
Require Export TTrap.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Section WITHMEM.

  Local Open Scope Z_scope.

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

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

  Section Prim.


    Global Instance sys_dispatch_c_inv: TrapProcCreateINV sys_dispatch_c_spec.
    Proof.
      destruct trap_proc_create_inv.
      split; unfold sys_dispatch_c_spec; intros.
      -
        subdestruct; try (eapply uctx_set_errno_high_inv; eauto; fail).
        + eapply trap_proc_create_high_inv; eauto.
        + functional inversion H; inv H1; subst.
          × inv H0; constructor; auto.
          × inv H0; constructor; auto.
        + eapply trap_get_tsc_offset_high_inv; eauto.
        + eapply trap_set_tsc_offset_high_inv; eauto.
        + eapply trap_get_exitinfo_high_inv; eauto.
        + eapply trap_mmap_high_inv; eauto.
        + eapply trap_set_reg_high_inv; eauto.
        + eapply trap_get_reg_high_inv; eauto.
        + eapply trap_set_seg1_high_inv; eauto.
        + eapply trap_set_seg2_high_inv; eauto.
        + eapply trap_get_next_eip_high_inv; eauto.
        + eapply trap_inject_event_high_inv; eauto.
        + eapply trap_check_pending_event_high_inv; eauto.
        + eapply trap_check_int_shadow_high_inv; eauto.
        + eapply trap_intercept_int_window_high_inv; eauto.
        + eapply trap_handle_rdmsr_high_inv; eauto.
        + eapply trap_handle_wrmsr_high_inv; eauto.
        + eapply trap_get_quota_high_inv; eauto.
        + eapply trap_receivechan_high_inv; eauto.
        + eapply trap_sendtochan_high_inv; eauto.
        + eapply sys_getc_inv; eauto.
          econstructor.
          assumption.
        + eapply sys_putc_inv; eauto.
          econstructor.
          assumption.

      -
        subdestruct; try (eapply uctx_set_errno_low_inv; eauto; fail).
        + eapply trap_proc_create_low_inv; eauto.
        + functional inversion H; inv H1; subst.
          × constructor; auto.
          × constructor; auto.
        + eapply trap_get_tsc_offset_low_inv; eauto.
        + eapply trap_set_tsc_offset_low_inv; eauto.
        + eapply trap_get_exitinfo_low_inv; eauto.
        + eapply trap_mmap_low_inv; eauto.
        + eapply trap_set_reg_low_inv; eauto.
        + eapply trap_get_reg_low_inv; eauto.
        + eapply trap_set_seg1_low_inv; eauto.
        + eapply trap_set_seg2_low_inv; eauto.
        + eapply trap_get_next_eip_low_inv; eauto.
        + eapply trap_inject_event_low_inv; eauto.
        + eapply trap_check_pending_event_low_inv; eauto.
        + eapply trap_check_int_shadow_low_inv; eauto.
        + eapply trap_intercept_int_window_low_inv; eauto.
        + eapply trap_handle_rdmsr_low_inv; eauto.
        + eapply trap_handle_wrmsr_low_inv; eauto.
        + eapply trap_get_quota_low_inv; eauto.
        + eapply trap_receivechan_low_inv; eauto.
        + eapply trap_sendtochan_low_inv; eauto.
        + eapply sys_getc_inv; eauto.
          econstructor.
          assumption.
        + eapply sys_putc_inv; eauto.
          econstructor.
          assumption.

      -
        subdestruct; try (eapply uctx_set_errno_kernel_mode; eauto; fail).
        + eapply trap_proc_create_kernel_mode; eauto.
        + functional inversion H; inv H1; subst.
          × constructor; auto.
          × constructor; auto.
        + eapply trap_get_tsc_offset_kernel_mode; eauto.
        + eapply trap_set_tsc_offset_kernel_mode; eauto.
        + eapply trap_get_exitinfo_kernel_mode; eauto.
        + eapply trap_mmap_kernel_mode; eauto.
        + eapply trap_set_reg_kernel_mode; eauto.
        + eapply trap_get_reg_kernel_mode; eauto.
        + eapply trap_set_seg1_kernel_mode; eauto.
        + eapply trap_set_seg2_kernel_mode; eauto.
        + eapply trap_get_next_eip_kernel_mode; eauto.
        + eapply trap_inject_event_kernel_mode; eauto.
        + eapply trap_check_pending_event_kernel_mode; eauto.
        + eapply trap_check_int_shadow_kernel_mode; eauto.
        + eapply trap_intercept_int_window_kernel_mode; eauto.
        + eapply trap_handle_rdmsr_kernel_mode; eauto.
        + eapply trap_handle_wrmsr_kernel_mode; eauto.
        + eapply trap_get_quota_kernel_mode; eauto.
        + eapply trap_receivechan_kernel_mode; eauto.
        + eapply trap_sendtochan_kernel_mode; eauto.
        + eapply sys_getc_inv; eauto.
          econstructor.
          assumption.
        + eapply sys_putc_inv; eauto.
          econstructor.
          assumption.

      -
        subdestruct; eauto.
      -
        subdestruct; eauto.
    Qed.

  End Prim.

  Definition tdispatch_fresh : compatlayer (cdata RData) :=
    syscall_dispatch_C ↦ trap_proccreate_compatsem sys_dispatch_c_spec
                        .

  Definition tdispatch_passthrough : compatlayer (cdata RData) :=

    vmxinfo_get ↦ gensem thread_vmxinfo_get_spec
          ⊕ palloc ↦ gensem big2_palloc_spec
          
          ⊕ pt_read ↦ gensem thread_ptRead_spec
          ⊕ pt_resv ↦ gensem big2_ptResv_spec
          

          ⊕ uctx_get ↦ gensem thread_uctx_get_spec
          ⊕ uctx_set ↦ gensem thread_uctx_set_spec

          ⊕ get_CPU_ID ↦ gensem thread_get_CPU_ID_spec
          ⊕ get_curid ↦ gensem thread_get_curid_spec

          ⊕ vmx_run_vm ↦ primcall_vmx_enter_compatsem thread_vm_run_spec vmx_run_vm
          ⊕ vmx_return_from_guest ↦ primcall_vmx_return_compatsem thread_vmx_return_from_guest_spec
          ⊕ vmx_init ↦ vmcs_set_defaults_compatsem thread_vmx_init_spec

          ⊕ uctx_arg1 ↦ gensem uctx_arg1_spec
          ⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
          ⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
          ⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
          ⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
          ⊕ ptfault_resv ↦ gensem ptfault_resv_spec


          ⊕ cli ↦ gensem thread_cli_spec
          ⊕ sti ↦ gensem thread_sti_spec

          ⊕ trap_get ↦ primcall_trap_info_get_compatsem thread_trap_info_get_spec
          ⊕ trap_set ↦ primcall_trap_info_ret_compatsem thread_trap_info_ret_spec
          ⊕ proc_start_user ↦ primcall_start_user_tm_compatsem thread_proc_start_user_spec
          ⊕ proc_exit_user ↦ primcall_exit_user_tm_compatsem thread_proc_exit_user_spec
          ⊕ proc_start_user2 ↦ primcall_start_user_tm_compatsem2 thread_proc_start_user_spec
          ⊕ proc_exit_user2 ↦ primcall_exit_user_tm_compatsem2 thread_proc_exit_user_spec
          ⊕ accessors ↦ {| exec_load := (@exec_loadex _ _ _ _ _ _ _ _ Hmwd);
                           exec_store := (@exec_storeex _ _ _ _ _ _ _ _ Hmwd) |}.

  Definition tdispatch : compatlayer (cdata RData) := tdispatch_fresh ⊕ tdispatch_passthrough.

End WITHMEM.