Library mcertikos.trap.TrapArgGen
*********************************************************************** * * * 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. * * * ***********************************************************************
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import LoadStoreSem3.
Require Import TTrapArg.
Require Export VMXInitGen.
Require Import TrapArgGenSpec.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := pproc_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := pproc_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := pproc_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := pproc_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Section Exists.
Lemma uctx_argn_exist´:
∀ n s habd z labd f,
uctx_argn_spec n habd = Some z →
0 ≤ n < UCTXT_SIZE →
0 ≤ cid habd < num_proc →
relate_AbData s f habd labd →
uctx_argn_spec n labd = Some z
∧ kernel_mode labd.
Proof.
intros. split.
- eapply uctx_argn_exist; eauto.
- unfold uctx_argn_spec in ×.
inv H2. revert H; subrewrite.
simpl; subdestruct. eauto.
Qed.
Lemma uctx_set_regk_exist´:
∀ k s habd habd´ labd n f,
uctx_set_regk_spec k n habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ cid habd < num_proc
→ ∃ labd´, uctx_set_regk_spec k n labd = Some labd´
∧ relate_AbData s f habd´ labd´
∧ kernel_mode labd.
Proof.
intros. exploit uctx_set_regk_exist; eauto.
intros (labd´ & He & HR).
refine_split´; eauto.
unfold uctx_set_regk_spec in He.
simpl; subdestruct. eauto.
Qed.
End Exists.
Section FRESH_PRIM.
Lemma uctx_arg1_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg1_spec) uctx_arg1_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- omega.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_arg2_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg2_spec) uctx_arg2_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- omega.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_arg3_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg3_spec) uctx_arg3_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- omega.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_arg4_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg4_spec) uctx_arg4_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- omega.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_arg5_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg5_spec) uctx_arg5_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- omega.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_arg6_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg6_spec) uctx_arg6_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_set_errno_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_errno_spec) uctx_set_errno_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_set_regk_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [labd´ [HP [HM Hkern]]].
refine_split; try econstructor; eauto.
constructor.
Qed.
Lemma uctx_set_retval1_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_retval1_spec) uctx_set_retval1_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_set_regk_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [labd´ [HP [HM Hkern]]].
refine_split; try econstructor; eauto.
constructor.
Qed.
Lemma uctx_set_retval2_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_retval2_spec) uctx_set_retval2_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_set_regk_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [labd´ [HP [HM Hkern]]].
refine_split; try econstructor; eauto.
constructor.
Qed.
Lemma uctx_set_retval3_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_retval3_spec) uctx_set_retval3_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_set_regk_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [labd´ [HP [HM Hkern]]].
refine_split; try econstructor; eauto.
constructor.
Qed.
Lemma uctx_set_retval4_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_retval4_spec) uctx_set_retval4_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_set_regk_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [labd´ [HP [HM Hkern]]].
refine_split; try econstructor; eauto.
constructor.
Qed.
End FRESH_PRIM.
Lemma passthrough_correct:
sim (crel HDATA LDATA) ttraparg_passthrough vmxinit.
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 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 vmx_get_reg_sim.
- apply vmx_set_reg_sim.
- apply vmx_get_next_eip_sim.
- apply vmx_get_io_width_sim.
- apply vmx_get_io_write_sim.
- apply vmx_get_exit_io_rep_sim.
- apply vmx_get_exit_io_str_sim.
- apply vmx_get_exit_io_port_sim.
- apply vmx_set_mmap_sim.
- apply vm_run_sim, VMX_INJECT.
- apply vmx_return_from_guest_sim.
intros. eapply valid_curid; eauto.
- apply vmx_init_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 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 OneStep_Forward_Relation.
End WITHMEM.
End Refinement.
Lemma uctx_argn_exist´:
∀ n s habd z labd f,
uctx_argn_spec n habd = Some z →
0 ≤ n < UCTXT_SIZE →
0 ≤ cid habd < num_proc →
relate_AbData s f habd labd →
uctx_argn_spec n labd = Some z
∧ kernel_mode labd.
Proof.
intros. split.
- eapply uctx_argn_exist; eauto.
- unfold uctx_argn_spec in ×.
inv H2. revert H; subrewrite.
simpl; subdestruct. eauto.
Qed.
Lemma uctx_set_regk_exist´:
∀ k s habd habd´ labd n f,
uctx_set_regk_spec k n habd = Some habd´
→ relate_AbData s f habd labd
→ 0 ≤ cid habd < num_proc
→ ∃ labd´, uctx_set_regk_spec k n labd = Some labd´
∧ relate_AbData s f habd´ labd´
∧ kernel_mode labd.
Proof.
intros. exploit uctx_set_regk_exist; eauto.
intros (labd´ & He & HR).
refine_split´; eauto.
unfold uctx_set_regk_spec in He.
simpl; subdestruct. eauto.
Qed.
End Exists.
Section FRESH_PRIM.
Lemma uctx_arg1_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg1_spec) uctx_arg1_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- omega.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_arg2_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg2_spec) uctx_arg2_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- omega.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_arg3_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg3_spec) uctx_arg3_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- omega.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_arg4_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg4_spec) uctx_arg4_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- omega.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_arg5_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg5_spec) uctx_arg5_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- omega.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_arg6_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_arg6_spec) uctx_arg6_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_argn_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [HP Hkern].
refine_split; try econstructor; eauto.
Qed.
Lemma uctx_set_errno_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_errno_spec) uctx_set_errno_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_set_regk_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [labd´ [HP [HM Hkern]]].
refine_split; try econstructor; eauto.
constructor.
Qed.
Lemma uctx_set_retval1_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_retval1_spec) uctx_set_retval1_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_set_regk_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [labd´ [HP [HM Hkern]]].
refine_split; try econstructor; eauto.
constructor.
Qed.
Lemma uctx_set_retval2_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_retval2_spec) uctx_set_retval2_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_set_regk_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [labd´ [HP [HM Hkern]]].
refine_split; try econstructor; eauto.
constructor.
Qed.
Lemma uctx_set_retval3_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_retval3_spec) uctx_set_retval3_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_set_regk_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [labd´ [HP [HM Hkern]]].
refine_split; try econstructor; eauto.
constructor.
Qed.
Lemma uctx_set_retval4_spec_ref:
compatsim (crel HDATA LDATA) (gensem uctx_set_retval4_spec) uctx_set_retval4_spec_low.
Proof.
compatsim_simpl (@match_AbData).
exploit uctx_set_regk_exist´; eauto 1.
- eapply valid_curid; eauto.
- intros [labd´ [HP [HM Hkern]]].
refine_split; try econstructor; eauto.
constructor.
Qed.
End FRESH_PRIM.
Lemma passthrough_correct:
sim (crel HDATA LDATA) ttraparg_passthrough vmxinit.
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 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 vmx_get_reg_sim.
- apply vmx_set_reg_sim.
- apply vmx_get_next_eip_sim.
- apply vmx_get_io_width_sim.
- apply vmx_get_io_write_sim.
- apply vmx_get_exit_io_rep_sim.
- apply vmx_get_exit_io_str_sim.
- apply vmx_get_exit_io_port_sim.
- apply vmx_set_mmap_sim.
- apply vm_run_sim, VMX_INJECT.
- apply vmx_return_from_guest_sim.
intros. eapply valid_curid; eauto.
- apply vmx_init_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 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 OneStep_Forward_Relation.
End WITHMEM.
End Refinement.