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 Export PIPC.
Require Export ObjArg.

Require Export ObjTMVMM.
Require Export ObjTMSCHED.
Require Export ObjTMINTELVIRT.
Require Export ObjTMIPCDEVPRIM.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Require Import INVLemmaIntel.
Require Import IntelPrimSemantics.
Require Import CalRealIntelModule.
Require Import INVLemmaThreadContainer.

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 INV.

    Lemma uctxt_inject_neutral_gss_arg:
      ∀ up n,
        uctxt_inject_neutral up n →
        ∀ i ii v,
          uctxt_inject_neutral (ZMap.set i (ZMap.set ii (Vint v) (ZMap.get i up)) up) n.
    Proof.
      unfold uctxt_inject_neutral. intros.
      destruct (zeq i ii0); subst.
      - rewrite ZMap.gss; eauto.
        destruct (zeq ii ii´); subst.
        + rewrite ZMap.gss. split; constructor.
        + rewrite ZMap.gso; eauto.
      - rewrite ZMap.gso; eauto.
    Qed.

    Section SET_ERRNO.

      Lemma uctx_set_errno_high_inv:
        ∀ d d´ i0,
          uctx_set_errno_spec i0 d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. inv H0; functional inversion H; subst; simpl.
        constructor; simpl; intros; try congruence; eauto 2.
      Qed.

      Lemma uctx_set_errno_low_inv:
        ∀ d d´ i0 n,
          uctx_set_errno_spec i0 d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. inv H0; functional inversion H; subst; simpl.
        constructor; simpl; intros; try congruence; eauto 2.
        eapply uctxt_inject_neutral_gss_arg; eauto.
      Qed.

      Lemma uctx_set_errno_kernel_mode:
        ∀ d d´ i0,
          uctx_set_errno_spec i0 d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst; constructor; trivial.
      Qed.

    Global Instance uctx_set_errno_inv: PreservesInvariants uctx_set_errno_spec.
    Proof.
      preserves_invariants_simpl´.
      - eapply uctx_set_errno_low_inv; eauto.
      - eapply uctx_set_errno_high_inv; eauto.
      - eapply uctx_set_errno_kernel_mode; eauto.
    Qed.

    End SET_ERRNO.

    Section SET_RETVAL1.

      Lemma uctx_set_retval1_high_inv:
        ∀ d d´ i0,
          uctx_set_retval1_spec i0 d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. inv H0; functional inversion H; subst; simpl.
        constructor; simpl; intros; try congruence; eauto 2.
      Qed.

      Lemma uctx_set_retval1_low_inv:
        ∀ d d´ i0 n,
          uctx_set_retval1_spec i0 d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. inv H0; functional inversion H; subst; simpl.
        constructor; simpl; intros; try congruence; eauto 2.
        eapply uctxt_inject_neutral_gss_arg; eauto.
      Qed.

      Lemma uctx_set_retval1_kernel_mode:
        ∀ d d´ i0,
          uctx_set_retval1_spec i0 d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst; constructor; trivial.
      Qed.

      Global Instance uctx_set_retval1_inv: PreservesInvariants uctx_set_retval1_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply uctx_set_retval1_low_inv; eauto.
        - eapply uctx_set_retval1_high_inv; eauto.
        - eapply uctx_set_retval1_kernel_mode; eauto.
      Qed.

    End SET_RETVAL1.

    Section SET_RETVAL2.

      Lemma uctx_set_retval2_high_inv:
        ∀ d d´ i0,
          uctx_set_retval2_spec i0 d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. inv H0; functional inversion H; subst; simpl.
        constructor; simpl; intros; try congruence; eauto 2.
      Qed.

      Lemma uctx_set_retval2_low_inv:
        ∀ d d´ i0 n,
          uctx_set_retval2_spec i0 d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. inv H0; functional inversion H; subst; simpl.
        constructor; simpl; intros; try congruence; eauto 2.
        eapply uctxt_inject_neutral_gss_arg; eauto.
      Qed.

      Lemma uctx_set_retval2_kernel_mode:
        ∀ d d´ i0,
          uctx_set_retval2_spec i0 d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst; constructor; trivial.
      Qed.

      Global Instance uctx_set_retval2_inv: PreservesInvariants uctx_set_retval2_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply uctx_set_retval2_low_inv; eauto.
        - eapply uctx_set_retval2_high_inv; eauto.
        - eapply uctx_set_retval2_kernel_mode; eauto.
      Qed.

    End SET_RETVAL2.

    Section SET_RETVAL3.

      Lemma uctx_set_retval3_high_inv:
        ∀ d d´ i0,
          uctx_set_retval3_spec i0 d = Some d´→
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. inv H0; functional inversion H; subst; simpl.
        constructor; simpl; intros; try congruence; eauto 2.
      Qed.

      Lemma uctx_set_retval3_low_inv:
        ∀ d d´ i0 n,
          uctx_set_retval3_spec i0 d = Some d´→
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. inv H0; functional inversion H; subst; simpl.
        constructor; simpl; intros; try congruence; eauto 2.
        eapply uctxt_inject_neutral_gss_arg; eauto.
      Qed.

      Lemma uctx_set_retval3_kernel_mode:
        ∀ d d´ i0,
          uctx_set_retval3_spec i0 d = Some d´→
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. functional inversion H; subst; constructor; trivial.
      Qed.

      Global Instance uctx_set_retval3_inv: PreservesInvariants uctx_set_retval3_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply uctx_set_retval3_low_inv; eauto.
        - eapply uctx_set_retval3_high_inv; eauto.
        - eapply uctx_set_retval3_kernel_mode; eauto.
      Qed.

    End SET_RETVAL3.

  End INV.

  Definition ttraparg_fresh : compatlayer (cdata RData) :=
    uctx_arg1 ↦ gensem uctx_arg1_spec
               ⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
               ⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
               ⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
               ⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
               ⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
               ⊕ uctx_set_retval2 ↦ gensem uctx_set_retval2_spec
               ⊕ uctx_set_retval3 ↦ gensem uctx_set_retval3_spec.

  Definition ttraparg_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
          ⊕ thread_yield ↦ gensem big2_thread_yield_spec

          ⊕ uctx_get ↦ gensem thread_uctx_get_spec
          ⊕ uctx_set ↦ gensem thread_uctx_set_spec
          ⊕ proc_create ↦ proc_create_compatsem big2_proc_create_spec

          ⊕ container_get_quota ↦ gensem thread_container_get_quota_spec
          ⊕ container_get_usage ↦ gensem thread_container_get_usage_spec
          ⊕ container_can_consume ↦ gensem thread_container_can_consume_spec

          ⊕ get_CPU_ID ↦ gensem thread_get_CPU_ID_spec
          ⊕ get_curid ↦ gensem thread_get_curid_spec

          ⊕ syncsendto_chan_post ↦ gensem thread_syncsendto_chan_spec
          ⊕ syncreceive_chan ↦ gensem thread_syncreceive_chan_spec

          ⊕ rdmsr ↦ gensem thread_rdmsr_spec
          ⊕ wrmsr ↦ gensem thread_wrmsr_spec

          ⊕ vmx_set_intercept_intwin ↦ gensem thread_vmx_set_intercept_intwin_spec
          ⊕ vmx_set_desc1 ↦ gensem thread_vmx_set_desc1_spec
          ⊕ vmx_set_desc2 ↦ gensem thread_vmx_set_desc2_spec
          ⊕ vmx_inject_event ↦ gensem thread_vmx_inject_event_spec
          ⊕ vmx_set_tsc_offset ↦ gensem thread_vmx_set_tsc_offset_spec
          ⊕ vmx_get_tsc_offset ↦ gensem thread_vmx_get_tsc_offset_spec
          ⊕ vmx_get_exit_reason ↦ gensem thread_vmx_get_exit_reason_spec
          ⊕ vmx_get_exit_fault_addr ↦ gensem thread_vmx_get_exit_fault_addr_spec
          ⊕ vmx_get_exit_qualification ↦ gensem thread_vmx_get_exit_qualification_spec
          ⊕ vmx_check_pending_event ↦ gensem thread_vmx_check_pending_event_spec
          ⊕ vmx_check_int_shadow ↦ gensem thread_vmx_check_int_shadow_spec
          ⊕ vmx_get_reg ↦ gensem thread_vmx_get_reg_spec
          ⊕ vmx_set_reg ↦ gensem thread_vmx_set_reg_spec

          ⊕ vmx_get_next_eip ↦ gensem thread_vmx_get_next_eip_spec
          ⊕ vmx_get_io_width ↦ gensem thread_vmx_get_io_width_spec
          ⊕ vmx_get_io_write ↦ gensem thread_vmx_get_io_write_spec
          ⊕ vmx_get_exit_io_rep ↦ gensem thread_vmx_get_exit_io_rep_spec
          ⊕ vmx_get_exit_io_str ↦ gensem thread_vmx_get_exit_io_str_spec
          ⊕ vmx_get_exit_io_port ↦ gensem thread_vmx_get_exit_io_port_spec
          ⊕ vmx_set_mmap ↦ gensem thread_vmx_set_mmap_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

          ⊕ cli ↦ gensem thread_cli_spec
          ⊕ sti ↦ gensem thread_sti_spec
          ⊕ serial_intr_disable ↦ gensem thread_serial_intr_disable_spec
          ⊕ serial_intr_enable ↦ gensem thread_serial_intr_enable_spec
          ⊕ serial_putc ↦ gensem thread_serial_putc_spec
          ⊕ cons_buf_read ↦ gensem thread_cons_buf_read_spec

          ⊕ proc_create_postinit ↦ gensem thread_proc_create_postinit_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 ttraparg : compatlayer (cdata RData) := ttraparg_fresh ⊕ ttraparg_passthrough.

End WITHMEM.