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 LoadStoreSem3high.
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 CalRealProcModule.
Require Import INVLemmaMemory.
Require Import INVLemmaThread.

Require Import AbstractDataType.

Require Import CalTicketLock.
Require Import INVLemmaInterrupt.
Require Import INVLemmaDriver.
Require Import DeviceStateDataType.
Require Import FutureTactic.
Require Export PIPCIntro.

Require Export ObjSyncIPC.

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

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.

    Section SEND.

      Lemma syncsendto_chan_high_level_inv:
        ∀ chid vaddr scount n d d´,
          thread_syncsendto_chan_spec chid vaddr scount d = Some (d´, n) →
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. unfold thread_syncsendto_chan_spec in ×. subdestruct; inv H.
        eapply release_lock_SC_high_level_inv; eauto.
        unfold thread_ipc_send_body_spec in Hdestruct0.
        subdestruct.
        eapply ipc_send_body_high_level_inv; eauto.
        eapply syncsendto_chan_pre_high_level_inv; eauto.
      Qed.

      Lemma syncsendto_chan_low_level_inv:
        ∀ chid vaddr scount d d´ n r,
          thread_syncsendto_chan_spec chid vaddr scount d = Some (d´, r) →
          low_level_invariant n d →
          low_level_invariant n d´.
      Proof.
        intros. unfold thread_syncsendto_chan_spec in ×. subdestruct; inv H.
        eapply release_lock_SC_low_level_inv; eauto.
        unfold thread_ipc_send_body_spec in Hdestruct0.
        subdestruct.
        eapply ipc_send_body_low_level_inv; eauto.
        eapply syncsendto_chan_pre_low_level_inv; eauto.
      Qed.

      Lemma syncsendto_chan_kernel_mode:
        ∀ chid vaddr scount d d´ r,
          thread_syncsendto_chan_spec chid vaddr scount d = Some (d´, r) →
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. unfold thread_syncsendto_chan_spec in ×. subdestruct; inv H.
        eapply release_lock_SC_kernel_mode; eauto.
        unfold thread_ipc_send_body_spec in Hdestruct0.
        subdestruct.
        eapply ipc_send_body_kernel_mode; eauto.
        eapply syncsendto_chan_pre_kernel_mode; eauto.
      Qed.

      Global Instance syncsendto_chan_inv: PreservesInvariants thread_syncsendto_chan_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply syncsendto_chan_low_level_inv; eassumption.
        - eapply syncsendto_chan_high_level_inv; eassumption.
        - eapply syncsendto_chan_kernel_mode; eassumption.
      Qed.

    End SEND.

    Section RECEIVE.

      Lemma syncreceive_chan_high_level_inv:
        ∀ chanid vaddr count d d´ n,
          thread_syncreceive_chan_spec chanid vaddr count d = Some (d´, n) →
          high_level_invariant d →
          high_level_invariant d´.
      Proof.
        intros. unfold thread_syncreceive_chan_spec in ×. subdestruct; inv H.
        eapply release_lock_SC_high_level_inv; eauto.
        eapply tryreceive_chan_high_level_inv; eauto.
        eapply acquire_lock_SC_high_level_inv; eauto.
      Qed.

      Lemma syncreceive_chan_low_level_inv:
        ∀ chanid vaddr count d d´ n n´,
          thread_syncreceive_chan_spec chanid vaddr count d = Some (d´, n) →
          low_level_invariant n´ d →
          low_level_invariant n´ d´.
      Proof.
        intros. unfold thread_syncreceive_chan_spec in ×. subdestruct; inv H.
        eapply release_lock_SC_low_level_inv; eauto.
        eapply tryreceive_chan_low_level_inv; eauto.
        eapply acquire_lock_SC_low_level_inv; eauto.
      Qed.

      Lemma syncreceive_chan_kernel_mode:
        ∀ chanid vaddr count d d´ n,
          thread_syncreceive_chan_spec chanid vaddr count d = Some (d´, n) →
          kernel_mode d →
          kernel_mode d´.
      Proof.
        intros. unfold thread_syncreceive_chan_spec in ×. subdestruct; inv H.
        eapply release_lock_SC_kernel_mode; eauto.
        eapply tryreceive_chan_kernel_mode; eauto.
        eapply acquire_lock_SC_kernel_mode; eauto.
      Qed.

      Global Instance syncreceive_chan_inv: PreservesInvariants thread_syncreceive_chan_spec.
      Proof.
        preserves_invariants_simpl´.
        - eapply syncreceive_chan_low_level_inv; eassumption.
        - eapply syncreceive_chan_high_level_inv; eassumption.
        - eapply syncreceive_chan_kernel_mode; eassumption.
      Qed.

    End RECEIVE.

  End INV.

  Definition pipc_fresh : compatlayer (cdata RData) :=
    syncsendto_chan_post ↦ gensem thread_syncsendto_chan_spec
                  ⊕ syncreceive_chan ↦ gensem thread_syncreceive_chan_spec.

  Definition pipc_passthrough : compatlayer (cdata RData) :=

    vmxinfo_get ↦ gensem thread_vmxinfo_get_spec
          ⊕ palloc ↦ gensem big2_palloc_spec
          
          ⊕ set_pt ↦ gensem thread_setPT_spec
          ⊕ pt_read ↦ gensem thread_ptRead_spec
          ⊕ pt_resv ↦ gensem big2_ptResv_spec
          
          
          
          ⊕ thread_yield ↦ gensem big2_thread_yield_spec
          ⊕ sched_init ↦ gensem big2_sched_init_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_nchildren ↦ gensem thread_container_get_nchildren_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
          

          ⊕ 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

          ⊕ host_in ↦ primcall_general_compatsem thread_hostin_spec
          ⊕ host_out ↦ primcall_general_compatsem thread_hostout_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 pipc : compatlayer (cdata RData) := pipc_fresh ⊕ pipc_passthrough.

End WITHMEM.