Library mcertikos.trap.TTrap
*********************************************************************** * * * 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 defines the abstract data and the primitives for the VVMCBInit layer,
which will introduce the primtives of thread
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 LAsm.
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 CalRealPTB.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import INVLemmaProc.
Require Import INVLemmaIntel.
Require Import AbstractDataType.
Require Import LoadStoreSem3.
Require Export TTrapArg.
Require Export ObjTrap.
Require Export TrapPrimSemantics.
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 LAsm.
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 CalRealPTB.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import INVLemmaProc.
Require Import INVLemmaIntel.
Require Import AbstractDataType.
Require Import LoadStoreSem3.
Require Export TTrapArg.
Require Export ObjTrap.
Require Export TrapPrimSemantics.
Section WITHMEM.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Require Import FutureTactic.
Require Import INVLemmaInterrupt.
Require Import CLemmas.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Require Import FutureTactic.
Require Import INVLemmaInterrupt.
Require Import CLemmas.
Section Prim.
Global Instance sys_putc_inv: PreservesInvariants sys_putc_spec.
Proof.
Opaque serial_intr_disable_aux.
constructor; simpl; intros; inv_generic_sem H; inversion H0.
- functional inversion H2; subst.
eapply uctx_set_errno_low_inv; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_low_level_invariant _ _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (serial_putc_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_low_level_invariant0 _ _ d1); eauto.
econstructor.
econstructor.
instantiate (1:= Int.repr c).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_low_level_invariant1; eauto.
econstructor.
eassumption.
- functional inversion H2; subst.
eapply uctx_set_errno_high_inv; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_high_level_invariant _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (serial_putc_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_high_level_invariant0 _ d1); eauto.
econstructor.
econstructor.
instantiate (1:= Int.repr c).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_high_level_invariant1; eauto.
econstructor.
eassumption.
- functional inversion H2; subst.
eapply uctx_set_errno_kernel_mode; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_kernel_mode _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (serial_putc_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_kernel_mode0 _ d1); eauto.
econstructor.
econstructor.
instantiate (1:= Int.repr c).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_kernel_mode1; eauto.
econstructor.
eassumption.
Qed.
Global Instance sys_getc_inv: PreservesInvariants sys_getc_spec.
Proof.
constructor; simpl; intros; inv_generic_sem H; inversion H0.
- functional inversion H2; subst.
eapply uctx_set_errno_low_inv; try eassumption.
eapply uctx_set_retval1_low_inv; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_low_level_invariant _ _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (cons_buf_read_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_low_level_invariant0 _ _ d1); eauto.
econstructor.
instantiate (1:= Int.repr x).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_low_level_invariant1; eauto.
econstructor.
eassumption.
- functional inversion H2; subst.
eapply uctx_set_errno_high_inv; try eassumption.
eapply uctx_set_retval1_high_inv; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_high_level_invariant _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (cons_buf_read_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_high_level_invariant0 _ d1); eauto.
econstructor.
instantiate (1:= Int.repr x).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_high_level_invariant1; eauto.
econstructor.
eassumption.
- functional inversion H2; subst.
eapply uctx_set_errno_kernel_mode; try eassumption.
eapply uctx_set_retval1_kernel_mode; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_kernel_mode _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (cons_buf_read_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_kernel_mode0 _ d1); eauto.
econstructor.
instantiate (1:= Int.repr x).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_kernel_mode1; eauto.
econstructor.
eassumption.
Qed.
Section TRAP_GET_QUOTA.
Lemma trap_get_quota_high_inv:
∀ d d´,
trap_get_quota_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H.
eapply uctx_set_errno_high_inv; try eassumption.
eapply uctx_set_retval1_high_inv; eassumption.
Qed.
Lemma trap_get_quota_low_inv:
∀ d d´ n,
trap_get_quota_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H.
eapply uctx_set_errno_low_inv; try eassumption.
eapply uctx_set_retval1_low_inv; eassumption.
Qed.
Lemma trap_get_quota_kernel_mode:
∀ d d´,
trap_get_quota_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H.
eapply uctx_set_errno_kernel_mode; try eassumption.
eapply uctx_set_retval1_kernel_mode; eassumption.
Qed.
Global Instance trap_get_quota_inv: PreservesInvariants trap_get_quota_spec.
Proof.
preserves_invariants_simpl´;
[ eapply trap_get_quota_low_inv
| eapply trap_get_quota_high_inv
| eapply trap_get_quota_kernel_mode ];
eassumption.
Qed.
End TRAP_GET_QUOTA.
Section TRAP_HANDLE_RDMSR.
Lemma trap_handle_rdmsr_high_inv:
∀ d d´,
trap_handle_rdmsr_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_reg_high_inv; eauto.
eapply vmx_set_reg_high_inv; eauto.
eapply vmx_set_reg_high_inv; eauto.
Qed.
Lemma trap_handle_rdmsr_low_inv:
∀ d d´ n,
trap_handle_rdmsr_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_reg_low_inv; eauto.
eapply vmx_set_reg_low_inv; eauto.
eapply vmx_set_reg_low_inv; eauto.
Qed.
Lemma trap_handle_rdmsr_kernel_mode:
∀ d d´,
trap_handle_rdmsr_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_reg_kernel_mode; eauto.
eapply vmx_set_reg_kernel_mode; eauto.
eapply vmx_set_reg_kernel_mode; eauto.
Qed.
Global Instance trap_handle_rdmsr_inv: PreservesInvariants trap_handle_rdmsr_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_handle_rdmsr_low_inv; eauto.
- eapply trap_handle_rdmsr_high_inv; eauto.
- eapply trap_handle_rdmsr_kernel_mode; eauto.
Qed.
End TRAP_HANDLE_RDMSR.
Section TRAP_HANDLE_WRMSR.
Lemma trap_handle_wrmsr_high_inv:
∀ d d´,
trap_handle_wrmsr_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_reg_high_inv; eauto.
Qed.
Lemma trap_handle_wrmsr_low_inv:
∀ d d´ n,
trap_handle_wrmsr_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_reg_low_inv; eauto.
Qed.
Lemma trap_handle_wrmsr_kernel_mode:
∀ d d´,
trap_handle_wrmsr_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_reg_kernel_mode; eauto.
Qed.
Global Instance trap_handle_wrmsr_inv: PreservesInvariants trap_handle_wrmsr_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_handle_wrmsr_low_inv; eauto.
- eapply trap_handle_wrmsr_high_inv; eauto.
- eapply trap_handle_wrmsr_kernel_mode; eauto.
Qed.
End TRAP_HANDLE_WRMSR.
Section TRAP_CHAN_RECEIVE.
Lemma trap_receivechan_high_inv:
∀ d d´,
trap_receivechan_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
eapply syncreceive_chan_high_level_inv; eauto.
Qed.
Lemma trap_receivechan_low_inv:
∀ d d´ n,
trap_receivechan_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
eapply syncreceive_chan_low_level_inv; eauto.
Qed.
Lemma trap_receivechan_kernel_mode:
∀ d d´,
trap_receivechan_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst.
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
eapply syncreceive_chan_kernel_mode; eauto.
Qed.
Global Instance trap_receivechan_inv: PreservesInvariants trap_receivechan_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_receivechan_low_inv; eauto.
- eapply trap_receivechan_high_inv; eauto.
- eapply trap_receivechan_kernel_mode; eauto.
Qed.
End TRAP_CHAN_RECEIVE.
Section TRAP_INTERCEPT_INT_WINDOW.
Lemma trap_intercept_int_window_high_inv:
∀ d d´,
trap_intercept_int_window_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_intercept_intwin_high_inv; eauto.
Qed.
Lemma trap_intercept_int_window_low_inv:
∀ d d´ n,
trap_intercept_int_window_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_intercept_intwin_low_inv; eauto.
Qed.
Lemma trap_intercept_int_window_kernel_mode:
∀ d d´,
trap_intercept_int_window_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst.
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_intercept_intwin_kernel_mode; eauto.
Qed.
Global Instance trap_intercept_int_window_inv: PreservesInvariants trap_intercept_int_window_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_intercept_int_window_low_inv; eauto.
- eapply trap_intercept_int_window_high_inv; eauto.
- eapply trap_intercept_int_window_kernel_mode; eauto.
Qed.
End TRAP_INTERCEPT_INT_WINDOW.
Section TRAP_CHECK_PENDING_EVENT.
Lemma trap_check_pending_event_high_inv:
∀ d d´,
trap_check_pending_event_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_check_pending_event_low_inv:
∀ d d´ n,
trap_check_pending_event_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_check_pending_event_kernel_mode:
∀ d d´,
trap_check_pending_event_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst.
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_check_pending_event_inv: PreservesInvariants trap_check_pending_event_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_check_pending_event_low_inv; eauto.
- eapply trap_check_pending_event_high_inv; eauto.
- eapply trap_check_pending_event_kernel_mode; eauto.
Qed.
End TRAP_CHECK_PENDING_EVENT.
Section TRAP_CHECK_INT_SHADOW.
Lemma trap_check_int_shadow_high_inv:
∀ d d´,
trap_check_int_shadow_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_check_int_shadow_low_inv:
∀ d d´ n,
trap_check_int_shadow_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_check_int_shadow_kernel_mode:
∀ d d´,
trap_check_int_shadow_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst.
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_check_int_shadow_inv: PreservesInvariants trap_check_int_shadow_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_check_int_shadow_low_inv; eauto.
- eapply trap_check_int_shadow_high_inv; eauto.
- eapply trap_check_int_shadow_kernel_mode; eauto.
Qed.
End TRAP_CHECK_INT_SHADOW.
Section TRAP_INJECT_EVENT.
Lemma trap_inject_event_high_inv:
∀ d d´,
trap_inject_event_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_inject_event_high_inv; eauto.
Qed.
Lemma trap_inject_event_low_inv:
∀ d d´ n,
trap_inject_event_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_inject_event_low_inv; eauto.
Qed.
Lemma trap_inject_event_kernel_mode:
∀ d d´,
trap_inject_event_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_inject_event_kernel_mode; eauto.
Qed.
Global Instance trap_inject_event_inv: PreservesInvariants trap_inject_event_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_inject_event_low_inv; eauto.
- eapply trap_inject_event_high_inv; eauto.
- eapply trap_inject_event_kernel_mode; eauto.
Qed.
End TRAP_INJECT_EVENT.
Section TRAP_GET_NEXT_EIP.
Lemma trap_get_next_eip_high_inv:
∀ d d´,
trap_get_next_eip_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_get_next_eip_low_inv:
∀ d d´ n,
trap_get_next_eip_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_get_next_eip_kernel_mode:
∀ d d´,
trap_get_next_eip_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst.
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_get_next_eip_inv: PreservesInvariants trap_get_next_eip_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_get_next_eip_low_inv; eauto.
- eapply trap_get_next_eip_high_inv; eauto.
- eapply trap_get_next_eip_kernel_mode; eauto.
Qed.
End TRAP_GET_NEXT_EIP.
Section TRAP_GET_REG.
Lemma trap_get_reg_high_inv:
∀ d d´,
trap_get_reg_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_get_reg_low_inv:
∀ d d´ n,
trap_get_reg_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_get_reg_kernel_mode:
∀ d d´,
trap_get_reg_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_get_reg_inv: PreservesInvariants trap_get_reg_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_get_reg_low_inv; eauto.
- eapply trap_get_reg_high_inv; eauto.
- eapply trap_get_reg_kernel_mode; eauto.
Qed.
End TRAP_GET_REG.
Section TRAP_SET_REG.
Lemma trap_set_reg_high_inv:
∀ d d´,
trap_set_reg_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_reg_high_inv; eauto.
Qed.
Lemma trap_set_reg_low_inv:
∀ d d´ n,
trap_set_reg_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_reg_low_inv; eauto.
Qed.
Lemma trap_set_reg_kernel_mode:
∀ d d´,
trap_set_reg_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_reg_kernel_mode; eauto.
Qed.
Global Instance trap_set_reg_inv: PreservesInvariants trap_set_reg_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_set_reg_low_inv; eauto.
- eapply trap_set_reg_high_inv; eauto.
- eapply trap_set_reg_kernel_mode; eauto.
Qed.
End TRAP_SET_REG.
Section TRAP_SET_SEG.
Lemma trap_set_seg_high_inv:
∀ d d´,
trap_set_seg_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_desc_high_inv; eauto.
Qed.
Lemma trap_set_seg_low_inv:
∀ d d´ n,
trap_set_seg_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_desc_low_inv; eauto.
Qed.
Lemma trap_set_seg_kernel_mode:
∀ d d´,
trap_set_seg_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_desc_kernel_mode; eauto.
Qed.
Global Instance trap_set_seg_inv: PreservesInvariants trap_set_seg_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_set_seg_low_inv; eauto.
- eapply trap_set_seg_high_inv; eauto.
- eapply trap_set_seg_kernel_mode; eauto.
Qed.
End TRAP_SET_SEG.
Section TRAP_GET_TSC_OFFSET.
Lemma trap_get_tsc_offset_high_inv:
∀ d d´,
trap_get_tsc_offset_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval2_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_get_tsc_offset_low_inv:
∀ d d´ n,
trap_get_tsc_offset_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval2_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_get_tsc_offset_kernel_mode:
∀ d d´,
trap_get_tsc_offset_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval2_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_get_tsc_offset_inv: PreservesInvariants trap_get_tsc_offset_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_get_tsc_offset_low_inv; eauto.
- eapply trap_get_tsc_offset_high_inv; eauto.
- eapply trap_get_tsc_offset_kernel_mode; eauto.
Qed.
End TRAP_GET_TSC_OFFSET.
Section TRAP_SET_TSC_OFFSET.
Lemma trap_set_tsc_offset_high_inv:
∀ d d´,
trap_set_tsc_offset_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_tsc_offset_high_inv; eauto.
Qed.
Lemma trap_set_tsc_offset_low_inv:
∀ d d´ n,
trap_set_tsc_offset_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_tsc_offset_low_inv; eauto.
Qed.
Lemma trap_set_tsc_offset_kernel_mode:
∀ d d´,
trap_set_tsc_offset_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_tsc_offset_kernel_mode; eauto.
Qed.
Global Instance trap_set_tsc_offset_inv: PreservesInvariants trap_set_tsc_offset_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_set_tsc_offset_low_inv; eauto.
- eapply trap_set_tsc_offset_high_inv; eauto.
- eapply trap_set_tsc_offset_kernel_mode; eauto.
Qed.
End TRAP_SET_TSC_OFFSET.
Section TRAP_GET_EXITINFO.
Lemma trap_get_exitinfo_high_inv:
∀ d d´,
trap_get_exitinfo_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
- eapply uctx_set_retval4_high_inv; eauto.
eapply uctx_set_retval3_high_inv; eauto.
eapply uctx_set_retval2_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
- eapply uctx_set_retval2_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
- eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_get_exitinfo_low_inv:
∀ d d´ n,
trap_get_exitinfo_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
- eapply uctx_set_retval4_low_inv; eauto.
eapply uctx_set_retval3_low_inv; eauto.
eapply uctx_set_retval2_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
- eapply uctx_set_retval2_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
- eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_get_exitinfo_kernel_mode:
∀ d d´,
trap_get_exitinfo_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
- eapply uctx_set_retval4_kernel_mode; eauto.
eapply uctx_set_retval3_kernel_mode; eauto.
eapply uctx_set_retval2_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
- eapply uctx_set_retval2_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
- eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_get_exitinfo_inv: PreservesInvariants trap_get_exitinfo_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_get_exitinfo_low_inv; eauto.
- eapply trap_get_exitinfo_high_inv; eauto.
- eapply trap_get_exitinfo_kernel_mode; eauto.
Qed.
End TRAP_GET_EXITINFO.
Section TRAP_MMAP.
Lemma trap_mmap_high_inv:
∀ d d´,
trap_mmap_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros; functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto;
eapply vmx_set_mmap_high_inv; eauto.
eapply ptResv_high_level_inv; eauto.
Qed.
Lemma trap_mmap_low_inv:
∀ d d´ n,
trap_mmap_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros; functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto;
eapply vmx_set_mmap_low_inv; eauto.
eapply ptResv_low_level_inv; eauto.
Qed.
Lemma trap_mmap_kernel_mode:
∀ d d´,
trap_mmap_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros; functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto;
eapply vmx_set_mmap_kernel_mode; eauto.
eapply ptResv_kernel_mode; eauto.
Qed.
Global Instance trap_mmap_inv: PreservesInvariants trap_mmap_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_mmap_low_inv; eauto.
- eapply trap_mmap_high_inv; eauto.
- eapply trap_mmap_kernel_mode; eauto.
Qed.
End TRAP_MMAP.
Section PTFault_RESV_INV.
Lemma ptfault_resv_high_inv:
∀ d d´ i,
ptfault_resv_spec i d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros; functional inversion H; subst; simpl.
eapply ptResv_high_level_inv; eauto.
Qed.
Lemma ptfault_resv_low_inv:
∀ d d´ i n,
ptfault_resv_spec i d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros; functional inversion H; subst; simpl.
eapply ptResv_low_level_inv; eauto.
Qed.
Lemma ptfault_resv_kernel_mode:
∀ d d´ i,
ptfault_resv_spec i d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros; functional inversion H; subst;
eapply ptResv_kernel_mode; eauto.
Qed.
Global Instance ptfault_resv_inv: PreservesInvariants ptfault_resv_spec.
Proof.
preserves_invariants_simpl´.
- eapply ptfault_resv_low_inv; eauto.
- eapply ptfault_resv_high_inv; eauto.
- eapply ptfault_resv_kernel_mode; eauto.
Qed.
End PTFault_RESV_INV.
Global Instance trap_proc_create_inv: TrapProcCreateINV trap_proc_create_spec.
Proof.
destruct proc_create_inv.
split; unfold trap_proc_create_spec; intros;
destruct (uctx_arg3_spec d); try discriminate H;
destruct (zle_le 0 z
(cquota (ZMap.get (cid d) (AC d)) -
cusage (ZMap.get (cid d) (AC d)))) eqn:Hquota; subdestruct; auto.
- eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
eapply pcreate_high_level_invariant; eauto.
- eapply uctx_set_errno_high_inv; eauto.
- eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
eapply pcreate_low_level_invariant; eauto;
eapply stencil_find_symbol_inject´; eauto;
eapply flat_inj_inject_incr; assumption.
- eapply uctx_set_errno_low_inv; eauto.
- eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
- eapply uctx_set_errno_kernel_mode; eauto.
- eapply Mem.load_extends in Hdestruct9; eauto.
destruct Hdestruct9 as [v2[HLD HV]].
eapply Mem.load_extends in Hdestruct13; eauto.
destruct Hdestruct13 as [v3[HLD´ HV´]].
inv HV. inv HV´. subrewrite´.
- pose proof H1 as Hsymbol. apply H1 in Hdestruct7.
eapply Mem.load_inject in Hdestruct9; eauto.
destruct Hdestruct9 as [v2[HLD HV]].
rewrite Z.add_0_r in HLD. subst.
rewrite HLD. inv HV; eauto.
rewrite H4 in Hdestruct7.
inv Hdestruct7. rewrite Int.add_zero.
apply H1 in Hdestruct8.
eapply Mem.load_inject in Hdestruct13; eauto.
destruct Hdestruct13 as [v3[HLD´ HV´]].
rewrite Z.add_0_r in HLD´. subst.
rewrite HLD´. inv HV´; eauto.
rewrite H5 in Hdestruct8.
inv Hdestruct8. rewrite Int.add_zero.
subrewrite´.
Qed.
End Prim.
Global Instance sys_putc_inv: PreservesInvariants sys_putc_spec.
Proof.
Opaque serial_intr_disable_aux.
constructor; simpl; intros; inv_generic_sem H; inversion H0.
- functional inversion H2; subst.
eapply uctx_set_errno_low_inv; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_low_level_invariant _ _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (serial_putc_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_low_level_invariant0 _ _ d1); eauto.
econstructor.
econstructor.
instantiate (1:= Int.repr c).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_low_level_invariant1; eauto.
econstructor.
eassumption.
- functional inversion H2; subst.
eapply uctx_set_errno_high_inv; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_high_level_invariant _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (serial_putc_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_high_level_invariant0 _ d1); eauto.
econstructor.
econstructor.
instantiate (1:= Int.repr c).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_high_level_invariant1; eauto.
econstructor.
eassumption.
- functional inversion H2; subst.
eapply uctx_set_errno_kernel_mode; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_kernel_mode _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (serial_putc_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_kernel_mode0 _ d1); eauto.
econstructor.
econstructor.
instantiate (1:= Int.repr c).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_kernel_mode1; eauto.
econstructor.
eassumption.
Qed.
Global Instance sys_getc_inv: PreservesInvariants sys_getc_spec.
Proof.
constructor; simpl; intros; inv_generic_sem H; inversion H0.
- functional inversion H2; subst.
eapply uctx_set_errno_low_inv; try eassumption.
eapply uctx_set_retval1_low_inv; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_low_level_invariant _ _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (cons_buf_read_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_low_level_invariant0 _ _ d1); eauto.
econstructor.
instantiate (1:= Int.repr x).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_low_level_invariant1; eauto.
econstructor.
eassumption.
- functional inversion H2; subst.
eapply uctx_set_errno_high_inv; try eassumption.
eapply uctx_set_retval1_high_inv; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_high_level_invariant _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (cons_buf_read_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_high_level_invariant0 _ d1); eauto.
econstructor.
instantiate (1:= Int.repr x).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_high_level_invariant1; eauto.
econstructor.
eassumption.
- functional inversion H2; subst.
eapply uctx_set_errno_kernel_mode; try eassumption.
eapply uctx_set_retval1_kernel_mode; try eassumption.
generalize (serial_intr_enable_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_kernel_mode _ d2 _ d3); eauto.
econstructor.
eassumption.
generalize (cons_buf_read_inv); intro tmp; inv tmp; simpl in ×.
eapply (semprops_kernel_mode0 _ d1); eauto.
econstructor.
instantiate (1:= Int.repr x).
rewrite Int.unsigned_repr by (generalize max_unsigned_val; omega).
eassumption.
generalize (serial_intr_disable_inv); intro tmp; inv tmp; simpl in ×.
eapply semprops_kernel_mode1; eauto.
econstructor.
eassumption.
Qed.
Section TRAP_GET_QUOTA.
Lemma trap_get_quota_high_inv:
∀ d d´,
trap_get_quota_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H.
eapply uctx_set_errno_high_inv; try eassumption.
eapply uctx_set_retval1_high_inv; eassumption.
Qed.
Lemma trap_get_quota_low_inv:
∀ d d´ n,
trap_get_quota_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H.
eapply uctx_set_errno_low_inv; try eassumption.
eapply uctx_set_retval1_low_inv; eassumption.
Qed.
Lemma trap_get_quota_kernel_mode:
∀ d d´,
trap_get_quota_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H.
eapply uctx_set_errno_kernel_mode; try eassumption.
eapply uctx_set_retval1_kernel_mode; eassumption.
Qed.
Global Instance trap_get_quota_inv: PreservesInvariants trap_get_quota_spec.
Proof.
preserves_invariants_simpl´;
[ eapply trap_get_quota_low_inv
| eapply trap_get_quota_high_inv
| eapply trap_get_quota_kernel_mode ];
eassumption.
Qed.
End TRAP_GET_QUOTA.
Section TRAP_HANDLE_RDMSR.
Lemma trap_handle_rdmsr_high_inv:
∀ d d´,
trap_handle_rdmsr_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_reg_high_inv; eauto.
eapply vmx_set_reg_high_inv; eauto.
eapply vmx_set_reg_high_inv; eauto.
Qed.
Lemma trap_handle_rdmsr_low_inv:
∀ d d´ n,
trap_handle_rdmsr_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_reg_low_inv; eauto.
eapply vmx_set_reg_low_inv; eauto.
eapply vmx_set_reg_low_inv; eauto.
Qed.
Lemma trap_handle_rdmsr_kernel_mode:
∀ d d´,
trap_handle_rdmsr_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_reg_kernel_mode; eauto.
eapply vmx_set_reg_kernel_mode; eauto.
eapply vmx_set_reg_kernel_mode; eauto.
Qed.
Global Instance trap_handle_rdmsr_inv: PreservesInvariants trap_handle_rdmsr_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_handle_rdmsr_low_inv; eauto.
- eapply trap_handle_rdmsr_high_inv; eauto.
- eapply trap_handle_rdmsr_kernel_mode; eauto.
Qed.
End TRAP_HANDLE_RDMSR.
Section TRAP_HANDLE_WRMSR.
Lemma trap_handle_wrmsr_high_inv:
∀ d d´,
trap_handle_wrmsr_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_reg_high_inv; eauto.
Qed.
Lemma trap_handle_wrmsr_low_inv:
∀ d d´ n,
trap_handle_wrmsr_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_reg_low_inv; eauto.
Qed.
Lemma trap_handle_wrmsr_kernel_mode:
∀ d d´,
trap_handle_wrmsr_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_reg_kernel_mode; eauto.
Qed.
Global Instance trap_handle_wrmsr_inv: PreservesInvariants trap_handle_wrmsr_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_handle_wrmsr_low_inv; eauto.
- eapply trap_handle_wrmsr_high_inv; eauto.
- eapply trap_handle_wrmsr_kernel_mode; eauto.
Qed.
End TRAP_HANDLE_WRMSR.
Section TRAP_CHAN_RECEIVE.
Lemma trap_receivechan_high_inv:
∀ d d´,
trap_receivechan_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
eapply syncreceive_chan_high_level_inv; eauto.
Qed.
Lemma trap_receivechan_low_inv:
∀ d d´ n,
trap_receivechan_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
eapply syncreceive_chan_low_level_inv; eauto.
Qed.
Lemma trap_receivechan_kernel_mode:
∀ d d´,
trap_receivechan_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst.
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
eapply syncreceive_chan_kernel_mode; eauto.
Qed.
Global Instance trap_receivechan_inv: PreservesInvariants trap_receivechan_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_receivechan_low_inv; eauto.
- eapply trap_receivechan_high_inv; eauto.
- eapply trap_receivechan_kernel_mode; eauto.
Qed.
End TRAP_CHAN_RECEIVE.
Section TRAP_INTERCEPT_INT_WINDOW.
Lemma trap_intercept_int_window_high_inv:
∀ d d´,
trap_intercept_int_window_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_intercept_intwin_high_inv; eauto.
Qed.
Lemma trap_intercept_int_window_low_inv:
∀ d d´ n,
trap_intercept_int_window_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_intercept_intwin_low_inv; eauto.
Qed.
Lemma trap_intercept_int_window_kernel_mode:
∀ d d´,
trap_intercept_int_window_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst.
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_intercept_intwin_kernel_mode; eauto.
Qed.
Global Instance trap_intercept_int_window_inv: PreservesInvariants trap_intercept_int_window_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_intercept_int_window_low_inv; eauto.
- eapply trap_intercept_int_window_high_inv; eauto.
- eapply trap_intercept_int_window_kernel_mode; eauto.
Qed.
End TRAP_INTERCEPT_INT_WINDOW.
Section TRAP_CHECK_PENDING_EVENT.
Lemma trap_check_pending_event_high_inv:
∀ d d´,
trap_check_pending_event_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_check_pending_event_low_inv:
∀ d d´ n,
trap_check_pending_event_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_check_pending_event_kernel_mode:
∀ d d´,
trap_check_pending_event_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst.
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_check_pending_event_inv: PreservesInvariants trap_check_pending_event_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_check_pending_event_low_inv; eauto.
- eapply trap_check_pending_event_high_inv; eauto.
- eapply trap_check_pending_event_kernel_mode; eauto.
Qed.
End TRAP_CHECK_PENDING_EVENT.
Section TRAP_CHECK_INT_SHADOW.
Lemma trap_check_int_shadow_high_inv:
∀ d d´,
trap_check_int_shadow_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_check_int_shadow_low_inv:
∀ d d´ n,
trap_check_int_shadow_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_check_int_shadow_kernel_mode:
∀ d d´,
trap_check_int_shadow_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst.
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_check_int_shadow_inv: PreservesInvariants trap_check_int_shadow_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_check_int_shadow_low_inv; eauto.
- eapply trap_check_int_shadow_high_inv; eauto.
- eapply trap_check_int_shadow_kernel_mode; eauto.
Qed.
End TRAP_CHECK_INT_SHADOW.
Section TRAP_INJECT_EVENT.
Lemma trap_inject_event_high_inv:
∀ d d´,
trap_inject_event_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_inject_event_high_inv; eauto.
Qed.
Lemma trap_inject_event_low_inv:
∀ d d´ n,
trap_inject_event_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_inject_event_low_inv; eauto.
Qed.
Lemma trap_inject_event_kernel_mode:
∀ d d´,
trap_inject_event_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_inject_event_kernel_mode; eauto.
Qed.
Global Instance trap_inject_event_inv: PreservesInvariants trap_inject_event_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_inject_event_low_inv; eauto.
- eapply trap_inject_event_high_inv; eauto.
- eapply trap_inject_event_kernel_mode; eauto.
Qed.
End TRAP_INJECT_EVENT.
Section TRAP_GET_NEXT_EIP.
Lemma trap_get_next_eip_high_inv:
∀ d d´,
trap_get_next_eip_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_get_next_eip_low_inv:
∀ d d´ n,
trap_get_next_eip_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl.
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_get_next_eip_kernel_mode:
∀ d d´,
trap_get_next_eip_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst.
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_get_next_eip_inv: PreservesInvariants trap_get_next_eip_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_get_next_eip_low_inv; eauto.
- eapply trap_get_next_eip_high_inv; eauto.
- eapply trap_get_next_eip_kernel_mode; eauto.
Qed.
End TRAP_GET_NEXT_EIP.
Section TRAP_GET_REG.
Lemma trap_get_reg_high_inv:
∀ d d´,
trap_get_reg_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_get_reg_low_inv:
∀ d d´ n,
trap_get_reg_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_get_reg_kernel_mode:
∀ d d´,
trap_get_reg_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_get_reg_inv: PreservesInvariants trap_get_reg_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_get_reg_low_inv; eauto.
- eapply trap_get_reg_high_inv; eauto.
- eapply trap_get_reg_kernel_mode; eauto.
Qed.
End TRAP_GET_REG.
Section TRAP_SET_REG.
Lemma trap_set_reg_high_inv:
∀ d d´,
trap_set_reg_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_reg_high_inv; eauto.
Qed.
Lemma trap_set_reg_low_inv:
∀ d d´ n,
trap_set_reg_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_reg_low_inv; eauto.
Qed.
Lemma trap_set_reg_kernel_mode:
∀ d d´,
trap_set_reg_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_reg_kernel_mode; eauto.
Qed.
Global Instance trap_set_reg_inv: PreservesInvariants trap_set_reg_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_set_reg_low_inv; eauto.
- eapply trap_set_reg_high_inv; eauto.
- eapply trap_set_reg_kernel_mode; eauto.
Qed.
End TRAP_SET_REG.
Section TRAP_SET_SEG.
Lemma trap_set_seg_high_inv:
∀ d d´,
trap_set_seg_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_desc_high_inv; eauto.
Qed.
Lemma trap_set_seg_low_inv:
∀ d d´ n,
trap_set_seg_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_desc_low_inv; eauto.
Qed.
Lemma trap_set_seg_kernel_mode:
∀ d d´,
trap_set_seg_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_desc_kernel_mode; eauto.
Qed.
Global Instance trap_set_seg_inv: PreservesInvariants trap_set_seg_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_set_seg_low_inv; eauto.
- eapply trap_set_seg_high_inv; eauto.
- eapply trap_set_seg_kernel_mode; eauto.
Qed.
End TRAP_SET_SEG.
Section TRAP_GET_TSC_OFFSET.
Lemma trap_get_tsc_offset_high_inv:
∀ d d´,
trap_get_tsc_offset_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval2_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_get_tsc_offset_low_inv:
∀ d d´ n,
trap_get_tsc_offset_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval2_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_get_tsc_offset_kernel_mode:
∀ d d´,
trap_get_tsc_offset_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval2_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_get_tsc_offset_inv: PreservesInvariants trap_get_tsc_offset_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_get_tsc_offset_low_inv; eauto.
- eapply trap_get_tsc_offset_high_inv; eauto.
- eapply trap_get_tsc_offset_kernel_mode; eauto.
Qed.
End TRAP_GET_TSC_OFFSET.
Section TRAP_SET_TSC_OFFSET.
Lemma trap_set_tsc_offset_high_inv:
∀ d d´,
trap_set_tsc_offset_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
eapply vmx_set_tsc_offset_high_inv; eauto.
Qed.
Lemma trap_set_tsc_offset_low_inv:
∀ d d´ n,
trap_set_tsc_offset_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
eapply vmx_set_tsc_offset_low_inv; eauto.
Qed.
Lemma trap_set_tsc_offset_kernel_mode:
∀ d d´,
trap_set_tsc_offset_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
eapply vmx_set_tsc_offset_kernel_mode; eauto.
Qed.
Global Instance trap_set_tsc_offset_inv: PreservesInvariants trap_set_tsc_offset_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_set_tsc_offset_low_inv; eauto.
- eapply trap_set_tsc_offset_high_inv; eauto.
- eapply trap_set_tsc_offset_kernel_mode; eauto.
Qed.
End TRAP_SET_TSC_OFFSET.
Section TRAP_GET_EXITINFO.
Lemma trap_get_exitinfo_high_inv:
∀ d d´,
trap_get_exitinfo_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto.
- eapply uctx_set_retval4_high_inv; eauto.
eapply uctx_set_retval3_high_inv; eauto.
eapply uctx_set_retval2_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
- eapply uctx_set_retval2_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
- eapply uctx_set_retval1_high_inv; eauto.
Qed.
Lemma trap_get_exitinfo_low_inv:
∀ d d´ n,
trap_get_exitinfo_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto.
- eapply uctx_set_retval4_low_inv; eauto.
eapply uctx_set_retval3_low_inv; eauto.
eapply uctx_set_retval2_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
- eapply uctx_set_retval2_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
- eapply uctx_set_retval1_low_inv; eauto.
Qed.
Lemma trap_get_exitinfo_kernel_mode:
∀ d d´,
trap_get_exitinfo_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto.
- eapply uctx_set_retval4_kernel_mode; eauto.
eapply uctx_set_retval3_kernel_mode; eauto.
eapply uctx_set_retval2_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
- eapply uctx_set_retval2_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
- eapply uctx_set_retval1_kernel_mode; eauto.
Qed.
Global Instance trap_get_exitinfo_inv: PreservesInvariants trap_get_exitinfo_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_get_exitinfo_low_inv; eauto.
- eapply trap_get_exitinfo_high_inv; eauto.
- eapply trap_get_exitinfo_kernel_mode; eauto.
Qed.
End TRAP_GET_EXITINFO.
Section TRAP_MMAP.
Lemma trap_mmap_high_inv:
∀ d d´,
trap_mmap_spec d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros; functional inversion H; subst; simpl;
eapply uctx_set_errno_high_inv; eauto;
eapply vmx_set_mmap_high_inv; eauto.
eapply ptResv_high_level_inv; eauto.
Qed.
Lemma trap_mmap_low_inv:
∀ d d´ n,
trap_mmap_spec d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros; functional inversion H; subst; simpl;
eapply uctx_set_errno_low_inv; eauto;
eapply vmx_set_mmap_low_inv; eauto.
eapply ptResv_low_level_inv; eauto.
Qed.
Lemma trap_mmap_kernel_mode:
∀ d d´,
trap_mmap_spec d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros; functional inversion H; subst;
eapply uctx_set_errno_kernel_mode; eauto;
eapply vmx_set_mmap_kernel_mode; eauto.
eapply ptResv_kernel_mode; eauto.
Qed.
Global Instance trap_mmap_inv: PreservesInvariants trap_mmap_spec.
Proof.
preserves_invariants_simpl´.
- eapply trap_mmap_low_inv; eauto.
- eapply trap_mmap_high_inv; eauto.
- eapply trap_mmap_kernel_mode; eauto.
Qed.
End TRAP_MMAP.
Section PTFault_RESV_INV.
Lemma ptfault_resv_high_inv:
∀ d d´ i,
ptfault_resv_spec i d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros; functional inversion H; subst; simpl.
eapply ptResv_high_level_inv; eauto.
Qed.
Lemma ptfault_resv_low_inv:
∀ d d´ i n,
ptfault_resv_spec i d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros; functional inversion H; subst; simpl.
eapply ptResv_low_level_inv; eauto.
Qed.
Lemma ptfault_resv_kernel_mode:
∀ d d´ i,
ptfault_resv_spec i d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros; functional inversion H; subst;
eapply ptResv_kernel_mode; eauto.
Qed.
Global Instance ptfault_resv_inv: PreservesInvariants ptfault_resv_spec.
Proof.
preserves_invariants_simpl´.
- eapply ptfault_resv_low_inv; eauto.
- eapply ptfault_resv_high_inv; eauto.
- eapply ptfault_resv_kernel_mode; eauto.
Qed.
End PTFault_RESV_INV.
Global Instance trap_proc_create_inv: TrapProcCreateINV trap_proc_create_spec.
Proof.
destruct proc_create_inv.
split; unfold trap_proc_create_spec; intros;
destruct (uctx_arg3_spec d); try discriminate H;
destruct (zle_le 0 z
(cquota (ZMap.get (cid d) (AC d)) -
cusage (ZMap.get (cid d) (AC d)))) eqn:Hquota; subdestruct; auto.
- eapply uctx_set_errno_high_inv; eauto.
eapply uctx_set_retval1_high_inv; eauto.
eapply pcreate_high_level_invariant; eauto.
- eapply uctx_set_errno_high_inv; eauto.
- eapply uctx_set_errno_low_inv; eauto.
eapply uctx_set_retval1_low_inv; eauto.
eapply pcreate_low_level_invariant; eauto;
eapply stencil_find_symbol_inject´; eauto;
eapply flat_inj_inject_incr; assumption.
- eapply uctx_set_errno_low_inv; eauto.
- eapply uctx_set_errno_kernel_mode; eauto.
eapply uctx_set_retval1_kernel_mode; eauto.
- eapply uctx_set_errno_kernel_mode; eauto.
- eapply Mem.load_extends in Hdestruct9; eauto.
destruct Hdestruct9 as [v2[HLD HV]].
eapply Mem.load_extends in Hdestruct13; eauto.
destruct Hdestruct13 as [v3[HLD´ HV´]].
inv HV. inv HV´. subrewrite´.
- pose proof H1 as Hsymbol. apply H1 in Hdestruct7.
eapply Mem.load_inject in Hdestruct9; eauto.
destruct Hdestruct9 as [v2[HLD HV]].
rewrite Z.add_0_r in HLD. subst.
rewrite HLD. inv HV; eauto.
rewrite H4 in Hdestruct7.
inv Hdestruct7. rewrite Int.add_zero.
apply H1 in Hdestruct8.
eapply Mem.load_inject in Hdestruct13; eauto.
destruct Hdestruct13 as [v3[HLD´ HV´]].
rewrite Z.add_0_r in HLD´. subst.
rewrite HLD´. inv HV´; eauto.
rewrite H5 in Hdestruct8.
inv Hdestruct8. rewrite Int.add_zero.
subrewrite´.
Qed.
End Prim.
Definition ttrap_fresh : compatlayer (cdata RData) :=
ptfault_resv ↦ gensem ptfault_resv_spec
⊕ sys_proc_create ↦ trap_proccreate_compatsem trap_proc_create_spec
⊕ sys_get_quota ↦ gensem trap_get_quota_spec
⊕ sys_receive_chan ↦ gensem trap_receivechan_spec
⊕ sys_inject_event ↦ gensem trap_inject_event_spec
⊕ sys_check_int_shadow ↦ gensem trap_check_int_shadow_spec
⊕ sys_check_pending_event ↦ gensem trap_check_pending_event_spec
⊕ sys_intercept_int_window ↦ gensem trap_intercept_int_window_spec
⊕ sys_get_next_eip ↦ gensem trap_get_next_eip_spec
⊕ sys_get_reg ↦ gensem trap_get_reg_spec
⊕ sys_set_reg ↦ gensem trap_set_reg_spec
⊕ sys_set_seg ↦ gensem trap_set_seg_spec
⊕ sys_get_tsc_offset ↦ gensem trap_get_tsc_offset_spec
⊕ sys_set_tsc_offset ↦ gensem trap_set_tsc_offset_spec
⊕ sys_get_exitinfo ↦ gensem trap_get_exitinfo_spec
⊕ sys_handle_rdmsr ↦ gensem trap_handle_rdmsr_spec
⊕ sys_handle_wrmsr ↦ gensem trap_handle_wrmsr_spec
⊕ sys_mmap ↦ gensem trap_mmap_spec
⊕ sys_getc ↦ gensem sys_getc_spec
⊕ sys_putc ↦ gensem sys_putc_spec.
ptfault_resv ↦ gensem ptfault_resv_spec
⊕ sys_proc_create ↦ trap_proccreate_compatsem trap_proc_create_spec
⊕ sys_get_quota ↦ gensem trap_get_quota_spec
⊕ sys_receive_chan ↦ gensem trap_receivechan_spec
⊕ sys_inject_event ↦ gensem trap_inject_event_spec
⊕ sys_check_int_shadow ↦ gensem trap_check_int_shadow_spec
⊕ sys_check_pending_event ↦ gensem trap_check_pending_event_spec
⊕ sys_intercept_int_window ↦ gensem trap_intercept_int_window_spec
⊕ sys_get_next_eip ↦ gensem trap_get_next_eip_spec
⊕ sys_get_reg ↦ gensem trap_get_reg_spec
⊕ sys_set_reg ↦ gensem trap_set_reg_spec
⊕ sys_set_seg ↦ gensem trap_set_seg_spec
⊕ sys_get_tsc_offset ↦ gensem trap_get_tsc_offset_spec
⊕ sys_set_tsc_offset ↦ gensem trap_set_tsc_offset_spec
⊕ sys_get_exitinfo ↦ gensem trap_get_exitinfo_spec
⊕ sys_handle_rdmsr ↦ gensem trap_handle_rdmsr_spec
⊕ sys_handle_wrmsr ↦ gensem trap_handle_wrmsr_spec
⊕ sys_mmap ↦ gensem trap_mmap_spec
⊕ sys_getc ↦ gensem sys_getc_spec
⊕ sys_putc ↦ gensem sys_putc_spec.
Definition ttrap_passthrough : compatlayer (cdata RData) :=
fload ↦ gensem fload_spec
⊕ fstore ↦ gensem fstore_spec
⊕ palloc ↦ gensem palloc_spec
⊕ pt_read ↦ gensem ptRead_spec
⊕ shared_mem_status ↦ gensem shared_mem_status_spec
⊕ offer_shared_mem ↦ gensem offer_shared_mem_spec
⊕ get_curid ↦ gensem get_curid_spec
⊕ thread_wakeup ↦ gensem thread_wakeup_spec
⊕ syncsendto_chan_pre ↦ gensem syncsendto_chan_pre_spec
⊕ syncsendto_chan_post ↦ gensem syncsendto_chan_post_spec
⊕ uctx_get ↦ gensem uctx_get_spec
⊕ uctx_set ↦ gensem uctx_set_spec
⊕ vmx_run_vm ↦ primcall_vmx_enter_compatsem vm_run_spec vmx_run_vm
⊕ vmx_return_from_guest ↦ primcall_vmx_return_compatsem vmx_return_from_guest_spec
⊕ vmx_init ↦ vmcs_set_defaults_compatsem vmx_init_spec
⊕ uctx_arg1 ↦ gensem uctx_arg1_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
⊕ uctx_arg5 ↦ gensem uctx_arg5_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ cli ↦ gensem cli_spec
⊕ sti ↦ gensem sti_spec
⊕ trap_get ↦ primcall_trap_info_get_compatsem trap_info_get_spec
⊕ trap_set ↦ primcall_trap_info_ret_compatsem trap_info_ret_spec
⊕ thread_yield ↦ primcall_thread_schedule_compatsem thread_yield_spec (prim_ident:= thread_yield)
⊕ thread_sleep ↦ primcall_thread_transfer_compatsem thread_sleep_spec
⊕ proc_start_user ↦ primcall_start_user_compatsem proc_start_user_spec
⊕ proc_exit_user ↦ primcall_exit_user_compatsem proc_exit_user_spec
⊕ accessors ↦ {| exec_load := (@exec_loadex _ _ Hmwd);
exec_store := (@exec_storeex _ _ Hmwd) |}.
fload ↦ gensem fload_spec
⊕ fstore ↦ gensem fstore_spec
⊕ palloc ↦ gensem palloc_spec
⊕ pt_read ↦ gensem ptRead_spec
⊕ shared_mem_status ↦ gensem shared_mem_status_spec
⊕ offer_shared_mem ↦ gensem offer_shared_mem_spec
⊕ get_curid ↦ gensem get_curid_spec
⊕ thread_wakeup ↦ gensem thread_wakeup_spec
⊕ syncsendto_chan_pre ↦ gensem syncsendto_chan_pre_spec
⊕ syncsendto_chan_post ↦ gensem syncsendto_chan_post_spec
⊕ uctx_get ↦ gensem uctx_get_spec
⊕ uctx_set ↦ gensem uctx_set_spec
⊕ vmx_run_vm ↦ primcall_vmx_enter_compatsem vm_run_spec vmx_run_vm
⊕ vmx_return_from_guest ↦ primcall_vmx_return_compatsem vmx_return_from_guest_spec
⊕ vmx_init ↦ vmcs_set_defaults_compatsem vmx_init_spec
⊕ uctx_arg1 ↦ gensem uctx_arg1_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
⊕ uctx_arg5 ↦ gensem uctx_arg5_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ cli ↦ gensem cli_spec
⊕ sti ↦ gensem sti_spec
⊕ trap_get ↦ primcall_trap_info_get_compatsem trap_info_get_spec
⊕ trap_set ↦ primcall_trap_info_ret_compatsem trap_info_ret_spec
⊕ thread_yield ↦ primcall_thread_schedule_compatsem thread_yield_spec (prim_ident:= thread_yield)
⊕ thread_sleep ↦ primcall_thread_transfer_compatsem thread_sleep_spec
⊕ proc_start_user ↦ primcall_start_user_compatsem proc_start_user_spec
⊕ proc_exit_user ↦ primcall_exit_user_compatsem proc_exit_user_spec
⊕ accessors ↦ {| exec_load := (@exec_loadex _ _ Hmwd);
exec_store := (@exec_storeex _ _ Hmwd) |}.