Library mcertikos.virt.intel.EPTIntroGenPassthrough
*********************************************************************** * * * 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
Section Refinement.
Context `{real_params: RealParams}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Lemma passthrough_correct:
sim (crel HDATA LDATA) eptintro_passthrough pproc.
Proof.
sim_oplus.
- apply fload_sim.
- apply fstore_sim.
- apply vmxinfo_get_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 proc_init_sim.
- apply uctx_get_sim.
- apply uctx_set_sim.
- apply proc_create_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 container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply hostin_sim.
- apply hostout_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_correct.
+ eapply store_correct.
Qed.
End WITHMEM.
End Refinement.
Context `{real_params: RealParams}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Lemma passthrough_correct:
sim (crel HDATA LDATA) eptintro_passthrough pproc.
Proof.
sim_oplus.
- apply fload_sim.
- apply fstore_sim.
- apply vmxinfo_get_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 proc_init_sim.
- apply uctx_get_sim.
- apply uctx_set_sim.
- apply proc_create_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 container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply hostin_sim.
- apply hostout_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_correct.
+ eapply store_correct.
Qed.
End WITHMEM.
End Refinement.