Library mcertikos.virt.intel.VMXIntroGenPassthrough

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
***********************************************************************

This file provide the contextual refinement proof between MAL layer and MPTIntro layer

Require Export VMXIntroGenDef.

Definition of the refinement relation

Section Refinement.

  Context `{real_params: RealParams}.

  Section WITHMEM.

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

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

    Lemma passthrough_correct:
      sim (crel HDATA LDATA) vmxintro_passthrough vmcsinit.
    Proof.
      sim_oplus.
      - apply fload_sim.
      - apply fstore_sim.
      - apply palloc_sim.
      - apply ptRead_sim.
      - apply ptResv_sim.
      - apply shared_mem_status_sim.
      - apply offer_shared_mem_sim.
      - apply get_curid_sim.
      - apply thread_wakeup_sim.
      - apply syncreceive_chan_sim.
      - apply syncsendto_chan_pre_sim.
      - apply syncsendto_chan_post_sim.
      - apply uctx_get_sim.
      - apply uctx_set_sim.
      - apply proc_create_sim.
      - apply rdmsr_sim.
      - apply wrmsr_sim.
      - apply cli_sim.
      - apply sti_sim.
      - apply cons_buf_read_sim.
      - apply serial_putc_sim.
      - apply serial_intr_disable_sim.
      - apply serial_intr_enable_sim.
      - apply vmcs_readz_sim.
      - apply vmcs_writez_sim.
      - apply vmptrld_sim.
      - apply vmx_set_intercept_intwin_sim.
      - apply vmx_set_desc_sim.
      - apply vmx_inject_event_sim.
      - apply vmx_set_tsc_offset_sim.
      - apply vmx_get_tsc_offset_sim.
      - apply vmx_get_exit_reason_sim.
      - apply vmx_get_exit_fault_addr_sim.
      - apply vmx_check_pending_event_sim.
      - apply vmx_check_int_shadow_sim.
      - apply vmcs_set_defaults_sim.
      - apply ept_add_mapping_sim.
      - apply ept_invalidate_mappings_sim.
      - apply container_get_quota_sim.
      - apply container_get_usage_sim.
      - apply container_can_consume_sim.
      - apply hostin_sim.
      - apply trap_info_get_sim.
      - apply trap_info_ret_sim.
      - apply thread_yield_sim.
      - apply thread_sleep_sim.
      - apply proc_start_user_sim.
        intros. eapply valid_curid; eauto.
      - apply proc_exit_user_sim.
      - layer_sim_simpl.
        + eapply load_correct3.
        + eapply store_correct3.
    Qed.

  End WITHMEM.

End Refinement.