Require Export IPCIntroGenDef.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Section Refinement.

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

  Section WITHMEM.

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

    Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
    Proof.
      accessor_prop_tac.
      - eapply flatmem_store_exists; eauto.
    Qed.

    Lemma passthrough_correct:
      sim (crel HDATA LDATA) pipcintro_passthrough phthread.
    Proof.
      sim_oplus.
      - apply thread_vmxinfo_get_sim.
      - apply big2_palloc_sim.
      - apply thread_setPT_sim.
      - apply thread_ptRead_sim.
      - apply big2_ptResv_sim.
      - apply big2_thread_yield_sim.
      - apply big2_sched_init_sim.

      - apply thread_uctx_get_sim.
      - apply thread_uctx_set_sim.
      - apply big2_proc_create_sim.

      - apply thread_container_get_nchildren_sim.
      - apply thread_container_get_quota_sim.
      - apply thread_container_get_usage_sim.
      - apply thread_container_can_consume_sim.

      - apply thread_get_CPU_ID_sim.
      - apply thread_get_curid_sim.

      - apply big2_acquire_lock_SC_sim.
      - apply big2_release_lock_SC_sim.
      - apply thread_ipc_send_body_sim.

      - apply thread_rdmsr_sim.
      - apply thread_wrmsr_sim.

      - apply thread_vmx_set_intercept_intwin_sim.
      - apply thread_vmx_set_desc1_sim.
      - apply thread_vmx_set_desc2_sim.
      - apply thread_vmx_inject_event_sim.
      - apply thread_vmx_set_tsc_offset_sim.
      - apply thread_vmx_get_tsc_offset_sim.
      - apply thread_vmx_get_exit_reason_sim.
      - apply thread_vmx_get_exit_fault_addr_sim.
      - apply thread_vmx_get_exit_qualification_sim.
      - apply thread_vmx_check_pending_event_sim.
      - apply thread_vmx_check_int_shadow_sim.
      - apply thread_vmx_get_reg_sim.
      - apply thread_vmx_set_reg_sim.

      - apply thread_vmx_get_next_eip_sim.
      - apply thread_vmx_get_io_width_sim.
      - apply thread_vmx_get_io_write_sim.
      - apply thread_vmx_get_exit_io_rep_sim.
      - apply thread_vmx_get_exit_io_str_sim.
      - apply thread_vmx_get_exit_io_port_sim.
      - apply thread_vmx_set_mmap_sim.
      - apply thread_vm_run_sim, VMX_INJECT.
      - apply thread_vmx_return_from_guest_sim.
      - apply thread_vmx_init_sim.

      - apply thread_cli_sim.
      - apply thread_sti_sim.
      - apply thread_serial_intr_disable_sim.
      - apply thread_serial_intr_enable_sim.
      - apply thread_serial_putc_sim.
      - apply thread_cons_buf_read_sim.

      - apply thread_hostin_sim.
      - apply thread_hostout_sim.
      - apply thread_proc_create_postinit_sim.
      - apply thread_trap_info_get_sim.
      - apply thread_trap_info_ret_sim.
      - apply thread_proc_start_user_sim.
        intros; inv H; auto.
      - apply thread_proc_exit_user_sim.
      - apply thread_proc_start_user_sim2.
        intros; inv H; auto.
      - apply thread_proc_exit_user_sim2.
      - layer_sim_simpl.
        + eapply load_correct3high.
        + eapply store_correct3high.
    Qed.

  End WITHMEM.

End Refinement.