Library mcertikos.objects.ObjVMX
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import CalRealIntelModule.
Require Import CalTicketLock.
Require Import liblayers.compat.CompatGenSem.
Require Import ObjEPT.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Section OBJ_VMX.
Context `{real_params: RealParams}.
Function vmx_readz_spec (i: Z) (adt: RData): option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
if zle_lt 0 i VMX_Size´ then
match ZMap.get i (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v ⇒ Some (Int.unsigned v)
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function vmx_writez_spec (i value: Z) (adt: RData): option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
if zle_lt 0 i VMX_Size´ then
Some adt {vmx: ZMap.set (CPU_ID adt) (ZMap.set i (Vint (Int.repr value))
(ZMap.get (CPU_ID adt) (vmx adt))) (vmx adt)}
else None
else None
| _ ⇒ None
end.
Inductive reg_type:=
| TVMCS (z: Z)
| TVMX (z: Z).
Function Z2reg_type (reg: Z) :=
match reg with
| C_GUEST_EAX ⇒ Some (TVMX VMX_G_RAX´)
| C_GUEST_EBX ⇒ Some (TVMX VMX_G_RBX´)
| C_GUEST_ECX ⇒ Some (TVMX VMX_G_RCX´)
| C_GUEST_EDX ⇒ Some (TVMX VMX_G_RDX´)
| C_GUEST_ESI ⇒ Some (TVMX VMX_G_RSI´)
| C_GUEST_EDI ⇒ Some (TVMX VMX_G_RDI´)
| C_GUEST_CR2 ⇒ Some (TVMX VMX_G_CR2´)
| C_GUEST_EBP ⇒ Some (TVMX VMX_G_RBP´)
| C_GUEST_EIP ⇒ Some (TVMX VMX_G_RIP´)
| C_GUEST_ESP ⇒ Some (TVMCS C_VMCS_GUEST_RSP)
| C_GUEST_EFLAGS ⇒ Some (TVMCS C_VMCS_GUEST_RFLAGS)
| C_GUEST_CR0 ⇒ Some (TVMCS C_VMCS_GUEST_CR0)
| C_GUEST_CR3 ⇒ Some (TVMCS C_VMCS_GUEST_CR3)
| C_GUEST_CR4 ⇒ Some (TVMCS C_VMCS_GUEST_CR4)
| _ ⇒ None
end.
Function vmx_get_reg_spec (reg: Z) (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match Z2reg_type reg with
| Some (TVMX z) ⇒
match ZMap.get z (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v ⇒ Some (Int.unsigned v)
| _ ⇒ None
end
| Some (TVMCS z) ⇒
match ZMap.get (CPU_ID adt) (vmcs adt) with
| VMCSValid revid abrtid d ⇒
match ZMap.get z d with
| Vint v ⇒ Some (Int.unsigned v)
| _ ⇒ None
end
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function vmx_set_reg_spec (reg v: Z) (adt: RData): option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match Z2reg_type reg with
| Some (TVMX z) ⇒ Some adt {vmx: ZMap.set (CPU_ID adt) (ZMap.set z (Vint (Int.repr v))
(ZMap.get (CPU_ID adt) (vmx adt))) (vmx adt)}
| Some (TVMCS z) ⇒
match ZMap.get (CPU_ID adt) (vmcs adt) with
| VMCSValid revid abrtid d ⇒
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid (ZMap.set z (Vint (Int.repr v)) d)) (vmcs adt)}
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function vmx_get_next_eip_spec (adt: RData) : option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get (CPU_ID adt) (vmcs adt) with
| VMCSValid revid abrtid d ⇒
match ZMap.get VMX_G_RIP´ (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v1 ⇒
match ZMap.get C_VMCS_EXIT_INSTRUCTION_LENGTH d with
| Vint v2 ⇒ Some (Int.unsigned v1 + Int.unsigned v2)
| _ ⇒ None
end
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmx_get_exit_qualification_spec (adt: RData): option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get VMX_EXIT_QUALIFICATION´ (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v ⇒
Some (Int.unsigned v)
|_ ⇒ None
end
else None
| _ ⇒ None
end.
Function vmx_get_io_width_spec (adt: RData): option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get VMX_EXIT_QUALIFICATION´ (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v ⇒
let qsize := Z.land (Int.unsigned v) EXIT_QUAL_IO_SIZE in
if zeq qsize EXIT_QUAL_IO_ONE_BYTE then Some SZ8
else if zeq qsize EXIT_QUAL_IO_TWO_BYTE then Some SZ16
else Some SZ32
|_ ⇒ None
end
else None
| _ ⇒ None
end.
Function vmx_get_io_write_spec (adt: RData): option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get VMX_EXIT_QUALIFICATION´ (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v ⇒
let qdir := (Z.land (Z.shiftr (Int.unsigned v) EXIT_QUAL_IO_DIR) 1) in
if zeq qdir EXIT_QUAL_IO_IN then Some 0
else Some 1
|_ ⇒ None
end
else None
| _ ⇒ None
end.
Function vmx_get_exit_io_rep_spec (adt: RData): option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get VMX_EXIT_QUALIFICATION´ (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v ⇒
let qrep := Z.land (Z.shiftr (Int.unsigned v) EXIT_QUAL_IO_REP) 1 in
Some qrep
|_ ⇒ None
end
else None
| _ ⇒ None
end.
Function vmx_get_exit_io_str_spec (adt: RData): option Z :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get VMX_EXIT_QUALIFICATION´ (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v ⇒
let qrep := Z.land (Z.shiftr (Int.unsigned v) EXIT_QUAL_IO_STR) 1 in
Some qrep
|_ ⇒ None
end
else None
| _ ⇒ None
end.
Function vmx_get_exit_io_port_spec (adt: RData) :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get VMX_EXIT_QUALIFICATION´ (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v ⇒
Some ((Int.unsigned v) / C_EXIT_QUAL_IO_PORT)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function vmx_set_mmap_spec (gpa : Z) (hpa : Z) (mem_type: Z) (adt: RData) :=
match ept_add_mapping_spec gpa hpa mem_type adt with
| Some (adt´, res) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
if zle_le 0 res Int.max_unsigned then
if zle_lt 0 mem_type 4096 then
if zeq res 0 then
match ept_invalidate_mappings_spec adt´ with
| Some z ⇒ Some (adt´, z)
| _ ⇒ None
end
else Some (adt´, res)
else None
else None
else None
| _ ⇒ None
end.
Definition vmx_enter_spec (rs: regset) (adt: RData) : option (RData × regset) :=
match (ikern adt, ihost adt, pg adt, init adt) with
| (true, true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
let vvmx := ZMap.get (CPU_ID adt) (vmx adt) in
let rs´ := (Pregmap.init Vundef)
# EAX <- (ZMap.get VMX_G_RAX´ vvmx) # EBX <- (ZMap.get VMX_G_RBX´ vvmx)
# EDX <- (ZMap.get VMX_G_RDX´ vvmx) # ESI <- (ZMap.get VMX_G_RSI´ vvmx)
# EDI <- (ZMap.get VMX_G_RDI´ vvmx) # EBP <- (ZMap.get VMX_G_RBP´ vvmx)
# RA <- (ZMap.get VMX_G_RIP´ vvmx) in
let vvmx1 := ZMap.set VMX_HOST_EBP´ (rs EBP) vvmx in
let vvmx2 := ZMap.set VMX_HOST_EDI´ (rs EDI) vvmx1 in
Some (adt {vmx: ZMap.set (CPU_ID adt) vvmx2 (vmx adt)}{ihost: false}, rs´)
else None
| _ ⇒ None
end.
Function vmx_enter_pre_spec (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt, init adt) with
| (true, true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get (CPU_ID adt) (vmcs adt) with
| VMCSValid revid abrtid d ⇒
match ZMap.get VMX_G_RIP´ (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v ⇒
let d´ := ZMap.set C_VMCS_GUEST_RIP (Vint v) d in
Some (adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid d´) (vmcs adt)})
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Definition vm_run_spec (rs: regset) (adt: RData) : option (RData × regset) :=
match (ikern adt, pg adt, ihost adt, init adt) with
| (true, true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get (CPU_ID adt) (vmcs adt) with
| VMCSValid revid abrtid d ⇒
match ZMap.get VMX_G_RIP´ (ZMap.get (CPU_ID adt) (vmx adt)) with
| Vint v ⇒
let d´ := ZMap.set C_VMCS_GUEST_RIP (Vint v) d in
let vvmx := ZMap.get (CPU_ID adt) (vmx adt) in
let rs´ := (Pregmap.init Vundef)
# EAX <- (ZMap.get VMX_G_RAX´ vvmx) # EBX <- (ZMap.get VMX_G_RBX´ vvmx)
# EDX <- (ZMap.get VMX_G_RDX´ vvmx) # ESI <- (ZMap.get VMX_G_RSI´ vvmx)
# EDI <- (ZMap.get VMX_G_RDI´ vvmx) # EBP <- (ZMap.get VMX_G_RBP´ vvmx)
# RA <- (ZMap.get VMX_G_RIP´ vvmx) in
let vvmx1 := ZMap.set VMX_HOST_EBP´ (rs EBP) vvmx in
let vvmx2 := ZMap.set VMX_HOST_EDI´ (rs EDI) vvmx1 in
Some (adt {vmx: ZMap.set (CPU_ID adt) vvmx2 (vmx adt)}
{vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid d´) (vmcs adt)} {ihost: false}, rs´)
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Definition vmx_exit_spec (rs: regset) (adt: RData) : option (RData × regset) :=
match (ikern adt, ihost adt, pg adt, init adt) with
| (true, true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
let vvmx := ZMap.get (CPU_ID adt) (vmx adt) in
let vvmx1 := ZMap.set VMX_G_RDI´ (rs EDI) vvmx in
let vvmx2 := ZMap.set VMX_G_RAX´ (rs EAX) vvmx1 in
let vvmx3 := ZMap.set VMX_G_RBX´ (rs EBX) vvmx2 in
let vvmx5 := ZMap.set VMX_G_RDX´ (rs EDX) vvmx3 in
let vvmx6 := ZMap.set VMX_G_RSI´ (rs ESI) vvmx5 in
let vvmx7 := ZMap.set VMX_G_RBP´ (rs EBP) vvmx6 in
let rs´ := (Pregmap.init Vundef)
# EDI <- (ZMap.get VMX_HOST_EDI´ vvmx) # EBP <- (ZMap.get VMX_HOST_EBP´ vvmx) in
Some (adt {vmx: ZMap.set (CPU_ID adt) vvmx7 (vmx adt)}, rs´)
else None
| _ ⇒ None
end.
Function vmx_exit_post_spec (adt: RData) : option RData :=
match (ikern adt, pg adt, ihost adt) with
| (true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get (CPU_ID adt) (vmcs adt) with
| VMCSValid revid abrtid d ⇒
let vvmx := ZMap.get (CPU_ID adt) (vmx adt) in
match ZMap.get C_VMCS_GUEST_RIP d, ZMap.get C_VMCS_EXIT_REASON d,
ZMap.get C_VMCS_EXIT_QUALIFICATION d with
| Vint v1, Vint v2, Vint v3 ⇒
let vvmx1 := ZMap.set VMX_G_RIP´ (Vint v1) vvmx in
let vvmx2 := ZMap.set VMX_EXIT_REASON´ (Vint v2) vvmx1 in
let vvmx3 := ZMap.set VMX_EXIT_QUALIFICATION´ (Vint v3) vvmx2 in
let vvmx4 := ZMap.set VMX_LAUNCHED´ Vone vvmx3 in
Some (adt {vmx: ZMap.set (CPU_ID adt) vvmx4 (vmx adt)})
| _,_,_ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmx_return_from_guest_spec (adt: RData) : option RData :=
match (init adt, ikern adt, pg adt, ihost adt) with
| (true, true, true, false) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
match ZMap.get (CPU_ID adt) (vmcs adt) with
| VMCSValid revid abrtid d ⇒
let vvmx := ZMap.get (CPU_ID adt) (vmx adt) in
match ZMap.get C_VMCS_GUEST_RIP d, ZMap.get C_VMCS_EXIT_REASON d,
ZMap.get C_VMCS_EXIT_QUALIFICATION d with
| Vint v1, Vint v2, Vint v3 ⇒
let vvmx1 := ZMap.set VMX_G_RIP´ (Vint v1) vvmx in
let vvmx2 := ZMap.set VMX_EXIT_REASON´ (Vint v2) vvmx1 in
let vvmx3 := ZMap.set VMX_EXIT_QUALIFICATION´ (Vint v3) vvmx2 in
let vvmx4 := ZMap.set VMX_LAUNCHED´ Vone vvmx3 in
Some (adt {ihost: true} {vmx: ZMap.set (CPU_ID adt) vvmx4 (vmx adt)})
| _,_,_ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmx_init_spec
(pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b: block)
(adt: RData) : option RData :=
match (init adt, pg adt, in_intr adt, ikern adt, ihost adt, ipt adt) with
| (true, true, true, true, true, true) ⇒
if zle_lt 0 (CPU_ID adt) NUM_VMS then
if zle_lt 0 (ZMap.get (CPU_ID adt) (cid adt)) num_proc then
Some (((adt {ept: ZMap.set (CPU_ID adt)
(Calculate_EPDPTE 3 (ZMap.set 0 (EPML4EValid (ZMap.init EPDPTEUndef))
(ZMap.get (CPU_ID adt) (ept adt)))) (ept adt)})
{vmcs: ZMap.set (CPU_ID adt)
(Calculate_VMCS_at_i (CPU_ID adt) (ZMap.get (CPU_ID adt) (cid adt)) (ZMap.get (CPU_ID adt) (vmcs adt))
real_vmxinfo pml4ept_b stack_b idt_b
msr_bitmap_b io_bitmap_b host_rip_b) (vmcs adt)})
{vmx: ZMap.set (CPU_ID adt) (Calculate_VMX_at_i (ZMap.get (CPU_ID adt) (vmx adt))) (vmx adt)})
else None
else None
| _ ⇒ None
end.
End OBJ_VMX.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import IntelPrimSemantics.
Require Import AuxLemma.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Lemma val_inject_vint_eq:
∀ f n v v´ i,
val_inject f (ZMap.get n v) (ZMap.get n v´)
→ ZMap.get n v = Vint i
→ ZMap.get n v´ = Vint i.
Proof.
intros.
rewrite H0 in H; inversion H; reflexivity.
Qed.
Section VMX_GET_REG_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re3: relate_impl_vmcs}.
Context {re4: relate_impl_CPU_ID}.
Lemma vmx_get_reg_exist:
∀ s habd labd reg v f,
vmx_get_reg_spec reg habd = Some v
→ relate_AbData s f habd labd
→ vmx_get_reg_spec reg labd = Some v.
Proof.
unfold vmx_get_reg_spec in ×. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
revert H. subrewrite;
subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
exploit relate_impl_vmcs_eq; eauto; inversion 1; subst;
erewrite val_inject_vint_eq; subrewrite´; eauto.
Qed.
Lemma vmx_get_reg_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_reg_spec)
(id ↦ gensem vmx_get_reg_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
eapply vmx_get_reg_exist in H2; eauto.
rewrite H2; reflexivity.
Qed.
End VMX_GET_REG_SIM.
Section VMX_SET_REG_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re3: relate_impl_vmcs}.
Context {re4: relate_impl_CPU_ID}.
Lemma vmx_set_reg_exist:
∀ s habd habd´ labd reg v f,
vmx_set_reg_spec reg v habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, vmx_set_reg_spec reg v labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmx_set_reg_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
exploit relate_impl_vmcs_eq; eauto; inversion 1; subst;
inv HQ; refine_split´; trivial.
- apply relate_impl_vmcs_update; try assumption.
unfold VMCSPool_inj. intros.
assert(idcase: vmid = (CPU_ID labd) ∨ vmid ≠ (CPU_ID labd)) by omega.
case_eq idcase; intros.
subst.
repeat rewrite ZMap.gss.
repeat apply VMCS_inj_set_int.
econstructor; eauto.
rewrite ZMap.gso in H7 by assumption.
rewrite ZMap.gso in H9 by assumption.
exploit relate_impl_vmcs_eq; eauto.
- apply relate_impl_vmx_update; try assumption.
unfold VMXPool_inj. intros.
assert(idcase: vmid = (CPU_ID labd) ∨ vmid ≠ (CPU_ID labd)) by omega.
case_eq idcase; intros.
subst.
repeat rewrite ZMap.gss.
repeat apply VMX_inj_set_int.
econstructor; eauto.
rewrite ZMap.gso in H10 by assumption.
rewrite ZMap.gso in H11 by assumption.
exploit relate_impl_vmx_eq; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmx}.
Context {mt3: match_impl_vmcs}.
Lemma vmx_set_reg_match:
∀ s d d´ m reg v f,
vmx_set_reg_spec reg v d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmx_set_reg_spec; intros. subdestruct; inv H; trivial;
[ eapply match_impl_vmcs_update
| eapply match_impl_vmx_update ];
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) vmx_set_reg_spec}.
Context {inv0: PreservesInvariants (HD:= data0) vmx_set_reg_spec}.
Lemma vmx_set_reg_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_set_reg_spec)
(id ↦ gensem vmx_set_reg_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmx_set_reg_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmx_set_reg_match; eauto.
Qed.
End VMX_SET_REG_SIM.
Section VMX_GET_NEXT_EIP_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re3: relate_impl_vmcs}.
Context {re4: relate_impl_CPU_ID}.
Lemma vmx_get_next_eip_exist:
∀ s habd labd v f,
vmx_get_next_eip_spec habd = Some v
→ relate_AbData s f habd labd
→ vmx_get_next_eip_spec labd = Some v.
Proof.
unfold vmx_get_next_eip_spec in ×. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
revert H. subrewrite. subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
exploit relate_impl_vmcs_eq; eauto; inversion 1; subst;
erewrite 2 val_inject_vint_eq; eauto.
Qed.
Lemma vmx_get_next_eip_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_next_eip_spec)
(id ↦ gensem vmx_get_next_eip_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
eapply vmx_get_next_eip_exist in H2; eauto.
rewrite H2; reflexivity.
Qed.
End VMX_GET_NEXT_EIP_SIM.
Section VMX_GET_EXIT_QUALIFICATION_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re3: relate_impl_CPU_ID}.
Lemma vmx_get_exit_qualification_exist:
∀ s habd labd v f,
vmx_get_exit_qualification_spec habd = Some v
→ relate_AbData s f habd labd
→ vmx_get_exit_qualification_spec labd = Some v.
Proof.
Local Opaque Z.land.
unfold vmx_get_exit_qualification_spec in ×. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
erewrite val_inject_vint_eq; eauto; subrewrite´; eauto.
Qed.
Lemma vmx_get_exit_qualification_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_exit_qualification_spec)
(id ↦ gensem vmx_get_exit_qualification_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
eapply vmx_get_exit_qualification_exist in H2; eauto.
rewrite H2; reflexivity.
Qed.
End VMX_GET_EXIT_QUALIFICATION_SIM.
Section VMX_GET_IO_WIDTH_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re3: relate_impl_CPU_ID}.
Lemma vmx_get_io_width_exist:
∀ s habd labd v f,
vmx_get_io_width_spec habd = Some v
→ relate_AbData s f habd labd
→ vmx_get_io_width_spec labd = Some v.
Proof.
Local Opaque Z.land.
unfold vmx_get_io_width_spec in ×. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
erewrite val_inject_vint_eq; eauto; subrewrite´; eauto.
Qed.
Lemma vmx_get_io_width_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_io_width_spec)
(id ↦ gensem vmx_get_io_width_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
eapply vmx_get_io_width_exist in H2; eauto.
rewrite H2; reflexivity.
Qed.
End VMX_GET_IO_WIDTH_SIM.
Section VMX_GET_IO_WRITE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re4: relate_impl_CPU_ID}.
Lemma vmx_get_io_write_exist:
∀ s habd labd v f,
vmx_get_io_write_spec habd = Some v
→ relate_AbData s f habd labd
→ vmx_get_io_write_spec labd = Some v.
Proof.
Local Opaque Z.shiftr.
unfold vmx_get_io_write_spec in ×. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
erewrite val_inject_vint_eq; eauto; subrewrite´; eauto.
Qed.
Lemma vmx_get_io_write_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_io_write_spec)
(id ↦ gensem vmx_get_io_write_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
eapply vmx_get_io_write_exist in H2; eauto.
rewrite H2; reflexivity.
Qed.
End VMX_GET_IO_WRITE_SIM.
Section VMX_GET_EXIT_IO_REP_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re4: relate_impl_CPU_ID}.
Lemma vmx_get_exit_io_rep_exist:
∀ s habd labd v f,
vmx_get_exit_io_rep_spec habd = Some v
→ relate_AbData s f habd labd
→ vmx_get_exit_io_rep_spec labd = Some v.
Proof.
Local Opaque Z.land Z.shiftr.
unfold vmx_get_exit_io_rep_spec in ×. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
erewrite val_inject_vint_eq; eauto; subrewrite´; eauto.
Qed.
Lemma vmx_get_exit_io_rep_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_exit_io_rep_spec)
(id ↦ gensem vmx_get_exit_io_rep_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
eapply vmx_get_exit_io_rep_exist in H2; eauto.
rewrite H2; reflexivity.
Qed.
End VMX_GET_EXIT_IO_REP_SIM.
Section VMX_GET_EXIT_IO_STR_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re4: relate_impl_CPU_ID}.
Lemma vmx_get_exit_io_str_exist:
∀ s habd labd v f,
vmx_get_exit_io_str_spec habd = Some v
→ relate_AbData s f habd labd
→ vmx_get_exit_io_str_spec labd = Some v.
Proof.
Local Opaque Z.land Z.shiftr.
unfold vmx_get_exit_io_str_spec in ×. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
erewrite val_inject_vint_eq; eauto; subrewrite´; eauto.
Qed.
Lemma vmx_get_exit_io_str_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_exit_io_str_spec)
(id ↦ gensem vmx_get_exit_io_str_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
eapply vmx_get_exit_io_str_exist in H2; eauto.
rewrite H2; reflexivity.
Qed.
End VMX_GET_EXIT_IO_STR_SIM.
Section VMX_GET_EXIT_IO_PORT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re4: relate_impl_CPU_ID}.
Lemma vmx_get_exit_io_port_exist:
∀ s habd labd v f,
vmx_get_exit_io_port_spec habd = Some v
→ relate_AbData s f habd labd
→ vmx_get_exit_io_port_spec labd = Some v.
Proof.
unfold vmx_get_exit_io_port_spec in ×. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
erewrite val_inject_vint_eq; eauto; subrewrite´; eauto.
Qed.
Lemma vmx_get_exit_io_port_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_exit_io_port_spec)
(id ↦ gensem vmx_get_exit_io_port_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
eapply vmx_get_exit_io_port_exist in H2; eauto.
rewrite H2; reflexivity.
Qed.
End VMX_GET_EXIT_IO_PORT_SIM.
Section VMX_SET_MMAP_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ept}.
Context {re4: relate_impl_CPU_ID}.
Lemma vmx_set_mmap_exist:
∀ s habd habd´ labd gpa hpa mem_type i f,
vmx_set_mmap_spec gpa hpa mem_type habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, vmx_set_mmap_spec gpa hpa mem_type labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmx_set_mmap_spec; intros.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
destruct (ept_add_mapping_spec gpa hpa mem_type habd) as [ [] |] eqn:Hdestruct; contra_inv.
exploit ept_add_mapping_exist; eauto; intros [labd´ [HP HM]].
revert H. subrewrite.
subdestruct; inv HQ.
erewrite ept_invalidate_mappings_exists; eauto.
refine_split´; trivial.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_ept}.
Lemma vmx_set_mmap_match:
∀ s d d´ m gpa hpa mem_type i f,
vmx_set_mmap_spec gpa hpa mem_type d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmx_set_mmap_spec; intros.
subdestruct; inv H;
eapply ept_add_mapping_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) vmx_set_mmap_spec}.
Context {inv0: PreservesInvariants (HD:= data0) vmx_set_mmap_spec}.
Lemma vmx_set_mmap_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_set_mmap_spec)
(id ↦ gensem vmx_set_mmap_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmx_set_mmap_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmx_set_mmap_match; eauto.
Qed.
End VMX_SET_MMAP_SIM.
Section VM_RUN_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re3: relate_impl_vmcs}.
Context {re4: relate_impl_init}.
Context {re49: relate_impl_CPU_ID}.
Lemma vm_run_exist:
∀ s n habd habd´ labd rs0 rs1 r´0 f,
vm_run_spec rs0 habd = Some (habd´, rs1)
→ relate_AbData s f habd labd
→ (∀ r, val_inject f (Pregmap.get r rs0) (Pregmap.get r r´0))
→ (∀ r, Val.has_type (r´0#r) AST.Tint)
→ (∀ r, val_inject (Mem.flat_inj n) (r´0 r) (r´0 r))
→ VMXPool_inject_neutral (vmx labd) n
→ ∃ labd´ r´1, vm_run_spec r´0 labd = Some (labd´, r´1)
∧ relate_AbData s f habd´ labd´
∧ (∀ r, val_inject f (Pregmap.get r rs1) (Pregmap.get r r´1))
∧ (∀ r, Val.has_type (r´1#r) AST.Tint)
∧ (∀ r, val_inject (Mem.flat_inj n) (r´1 r) (r´1 r)).
Proof.
unfold vm_run_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1; subst.
exploit relate_impl_init_eq; eauto. intros.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
exploit relate_impl_vmcs_eq; eauto; inversion 1; subst.
pose proof (H9 14%Z) as HINJ.
inv HINJ;
try rewrite Hdestruct5 in H12; inv H12.
inv HQ. refine_split´; trivial.
- apply relate_impl_ihost_update, relate_impl_vmcs_update.
+ apply relate_impl_vmx_update; try assumption.
unfold VMXPool_inj. intros.
assert(idcase: vmid = (CPU_ID labd) ∨ vmid ≠ (CPU_ID labd)) by omega.
case_eq idcase; intros.
subst.
repeat rewrite ZMap.gss.
repeat apply VMX_inj_set_int.
econstructor; eauto.
intros.
Local Open Scope Z_scope.
unfold ZIndexed.t in i0.
assert(icase: i0 = 34 ∨ i0 ≠ 34) by omega.
case_eq icase; intros; subst.
repeat rewrite ZMap.gss. eauto.
assert(icase2: i0 = 33 ∨ i0 ≠ 33) by omega.
case_eq icase2; intros; subst.
repeat rewrite ZMap.gss. eauto.
repeat rewrite ZMap.gso by assumption.
repeat rewrite ZMap.gss. eauto.
repeat rewrite ZMap.gso by assumption.
repeat rewrite ZMap.gss. eauto.
repeat rewrite ZMap.gso by assumption.
eauto.
rewrite ZMap.gso in H12 by assumption.
rewrite ZMap.gso in H15 by assumption.
exploit relate_impl_vmx_eq; eauto.
+ unfold VMCSPool_inj. intros.
assert(idcase: vmid = (CPU_ID labd) ∨ vmid ≠ (CPU_ID labd)) by omega.
case_eq idcase; intros.
subst.
repeat rewrite ZMap.gss.
repeat apply VMX_inj_set_int.
econstructor; eauto.
intros.
Local Open Scope Z_scope.
unfold ZIndexed.t in i0.
assert(icase: i0 = 26654 ∨ i0 ≠ 26654) by omega.
case_eq icase; intros; subst.
repeat rewrite ZMap.gss. eauto.
repeat rewrite ZMap.gso by assumption.
eauto.
rewrite ZMap.gso in H12 by assumption.
rewrite ZMap.gso in H15 by assumption.
exploit relate_impl_vmcs_eq; eauto.
- intros.
repeat apply AsmX.set_reg_inject; auto.
- specialize (H4 (CPU_ID labd) (ZMap.get (CPU_ID labd) (vmx labd)) a eq_refl).
inv H4. intros.
destruct r as [| [] | [] | | [] |]; try apply H11; try constructor.
- specialize (H4 (CPU_ID labd) (ZMap.get (CPU_ID labd) (vmx labd)) a eq_refl).
inv H4.
destruct r as [| [] | [] | | [] |];
try apply H3; try apply H11;
constructor.
- rewrite Hdestruct5 in H11; inv H11.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmx}.
Context {mt3: match_impl_vmcs}.
Lemma vm_run_match:
∀ s d d´ m rs0 rs1 f,
vm_run_spec rs0 d = Some (d´, rs1)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vm_run_spec; intros.
subdestruct; inv H; trivial.
apply match_impl_ihost_update.
apply match_impl_vmcs_update.
apply match_impl_vmx_update. assumption.
Qed.
Context {inv: VMXEnterInvariants (data_ops := data_ops) vm_run_spec}.
Context {inv0: VMXEnterInvariants (data_ops:= data_ops0) vm_run_spec}.
Lemma vm_run_sim :
∀ id,
(∀ n d, low_level_invariant n d → VMXPool_inject_neutral (vmx d) n) →
sim (crel RData RData) (id ↦ primcall_vmx_enter_compatsem vm_run_spec id)
(id ↦ primcall_vmx_enter_compatsem vm_run_spec id).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. intros.
inv H1. inv H0. inv match_extcall_states.
set (rs02 := (Pregmap.init Vundef) # EDI <- (rs2 EDI) # EBP <- (rs2 EBP)).
assert (HR: ∀ reg,
val_inject f (Pregmap.get reg rs01) (Pregmap.get reg rs02)).
{
intros. subst rs01 rs02.
val_inject_simpl.
}
exploit vm_run_exist; eauto 2.
intros r; destruct r as [| [] | [] | | [] |]; try constructor;
try apply ASM_INV.
intros r; destruct r as [| [] | [] | | [] |]; try constructor;
try apply ASM_INV.
intros (labd´ & r´1 & HP & HM & Hrinj´ & Hrwt´ & Hrinj_flat´).
refine_split; eauto 1.
econstructor; eauto 1.
- eapply reg_symbol_inject; eassumption.
- eapply reg_val_inject_defined; eauto 1.
- intros.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv match_reg; try congruence.
specialize (HESP_STACK _ _ (eq_sym H1)).
replace b1 with b2 by congruence.
split.
× apply Ple_trans with b0;
[ apply HESP_STACK | apply (match_inject_forward _ _ _ H3) ].
× apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H3 match_inject).
- econstructor; eauto. econstructor; eauto.
eapply vm_run_match; eassumption.
subst rs0.
val_inject_simpl.
Qed.
End VM_RUN_SIM.
Local Open Scope Z_scope.
Section VMX_RETURN_FROM_GUEST_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re3: relate_impl_vmcs}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_ipt}.
Context {re6: relate_impl_cid}.
Context {re7: relate_impl_PT}.
Context {re8: relate_impl_uctxt}.
Context {re9: relate_impl_CPU_ID}.
Lemma vmx_return_from_guest_exist:
∀ s habd habd´ labd f,
vmx_return_from_guest_spec habd = Some habd´
→ relate_AbData s f habd labd
→ True
→ ∃ labd´, vmx_return_from_guest_spec labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmx_return_from_guest_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros Hipt.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
exploit relate_impl_cid_eq; eauto. intros Hcid.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmx_eq; eauto; inversion 1; subst;
exploit relate_impl_vmcs_eq; eauto; inversion 1; subst.
pose proof (H10 26654%Z) as Hi1.
pose proof (H10 17410%Z) as Hi2.
pose proof (H10 25600%Z) as Hi3.
inv HQ. inv Hi1. inv Hi2. inv Hi3.
refine_split´; trivial.
- apply relate_impl_vmx_update.
apply relate_impl_ihost_update; try assumption.
unfold VMXPool_inj. intros.
assert(idcase: vmid = (CPU_ID labd) ∨ vmid ≠ (CPU_ID labd)) by omega.
case_eq idcase; intros.
subst.
repeat rewrite ZMap.gss.
rewrite Hdestruct5 in H9; inv H9.
rewrite Hdestruct6 in H12; inv H12.
rewrite Hdestruct7 in H15; inv H15.
repeat (apply VMX_inj_set_int || apply VMX_inj_set);
try apply H; try apply H1.
rewrite ZMap.gso in H17, H18 by assumption.
exploit relate_impl_vmx_eq; eauto.
- rewrite Hdestruct7 in H15; inv H15.
- rewrite Hdestruct7 in H15; inv H15.
- rewrite Hdestruct7 in H8; inv H8.
- rewrite Hdestruct7 in H15; inv H15.
- rewrite Hdestruct6 in H12; inv H12.
- rewrite Hdestruct6 in H12; inv H12.
- rewrite Hdestruct6 in H8; inv H8.
- rewrite Hdestruct6 in H12; inv H12.
- rewrite Hdestruct5 in H9; inv H9.
- rewrite Hdestruct5 in H9; inv H9.
- rewrite Hdestruct5 in H8; inv H8.
- rewrite Hdestruct5 in H9; inv H9.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmx}.
Context {mt4: match_impl_ipt}.
Lemma vmx_return_from_guest_match:
∀ s d d´ m f,
vmx_return_from_guest_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmx_return_from_guest_spec; intros.
subdestruct; inv H; trivial.
apply match_impl_vmx_update.
apply match_impl_ihost_update.
assumption.
Qed.
Context {inv: VMXReturnInvariants (data_ops := data_ops) vmx_return_from_guest_spec}.
Context {inv0: VMXReturnInvariants (data_ops:= data_ops0) vmx_return_from_guest_spec}.
Context {low1: low_level_invariant_impl}.
Lemma vmx_return_from_guest_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_vmx_return_compatsem vmx_return_from_guest_spec)
(id ↦ primcall_vmx_return_compatsem vmx_return_from_guest_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl´. intros.
inv H. inv H0. inv match_extcall_states.
exploit vmx_return_from_guest_exist; eauto 2.
intros (labd´ & HP & HM).
exploit low_level_invariant_impl_eq; eauto. inversion 1.
refine_split; eauto 1.
econstructor; eauto 1.
- eapply reg_symbol_inject; eassumption.
- eapply reg_val_inject_defined; eauto 1.
- intros.
specialize (match_reg ESP); unfold Pregmap.get in match_reg.
inv match_reg; try congruence.
specialize (HESP_STACK _ _ (eq_sym H1)).
replace b1 with b2 by congruence.
split.
× apply Ple_trans with b0;
[ apply HESP_STACK | apply (match_inject_forward _ _ _ H3) ].
× apply (Mem.valid_block_inject_2 _ _ _ _ _ _ H3 match_inject).
- econstructor; eauto. econstructor; eauto.
eapply vmx_return_from_guest_match; eassumption.
subst rs0.
val_inject_simpl;
try (eapply Hrinj´; omega).
specialize (match_reg PC).
unfold Pregmap.get in match_reg.
rewrite HPC in match_reg.
inv match_reg.
inv ASM_INV.
inv inv_inject_neutral.
specialize (inv_reg_inject_neutral PC).
rewrite <- H2 in inv_reg_inject_neutral.
inv inv_reg_inject_neutral.
generalize H3; intro tmp.
eapply inject_forward_equal´ in tmp; eauto.
inv tmp.
econstructor; eauto.
Qed.
End VMX_RETURN_FROM_GUEST_SIM.
Section VMX_INIT_SIM.
Context `{real_params: RealParams}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmx}.
Context {re3: relate_impl_vmcs}.
Context {re7: relate_impl_init}.
Context {re15: relate_impl_cid}.
Context {re18: relate_impl_ept}.
Context {re23: relate_impl_CPU_ID}.
Context {re24: relate_impl_vmcs}.
Context {re25: relate_impl_vmx}.
Context {re26: relate_impl_ipt}.
Context {re27: relate_impl_in_intr}.
Let block_inject_neutral f b :=
∀ ofs, val_inject f (Vptr b ofs) (Vptr b ofs).
Lemma vmx_init_exist:
∀ s habd habd´ labd pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b f,
vmx_init_spec pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b habd = Some habd´
→ relate_AbData s f habd labd
→ block_inject_neutral f pm4ept_b
→ block_inject_neutral f stack_b
→ block_inject_neutral f idt_b
→ block_inject_neutral f msr_bitmap_b
→ block_inject_neutral f io_bitmap_b
→ block_inject_neutral f host_rip_b
→ ∃ labd´, vmx_init_spec pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmx_init_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_ipt_eq; eauto; inversion 1.
exploit relate_impl_init_eq; eauto; inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
exploit relate_impl_cid_eq; eauto; inversion 1.
exploit relate_impl_ept_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
subdestruct.
exploit relate_impl_vmcs_eq; eauto; intros.
exploit relate_impl_vmx_eq; eauto; intros.
rewrite <- ikern_eq, <- ihost_eq, <- pg_eq.
inv H. refine_split´; trivial.
apply relate_impl_vmx_update.
- apply relate_impl_vmcs_update.
+ apply relate_impl_ept_update.
assumption.
+ unfold VMCSPool_inj; intros.
case_eq (zeq vmid (CPU_ID habd)); intros; subst.
× repeat rewrite ZMap.gss.
inv H19; subst.
repeat (apply VMCS_inj_set_int || apply VMCS_inj_set);
try rewrite H26; auto.
econstructor; assumption.
× exploit relate_impl_vmcs_eq; eauto; intros.
repeat rewrite ZMap.gso; auto.
- unfold VMXPool_inj; intros.
case_eq (zeq vmid (CPU_ID habd)); intros; subst.
+ repeat rewrite ZMap.gss.
repeat apply VMX_inj_set_int; auto.
+ exploit relate_impl_vmx_eq; eauto; intros.
repeat rewrite ZMap.gso; auto.
Qed.
Context {mt2: match_impl_vmx}.
Context {mt3: match_impl_vmcs}.
Context {mt18: match_impl_ept}.
Lemma vmx_init_match:
∀ s d d´ m pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b f,
vmx_init_spec pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmx_init_spec; intros.
subdestruct; inv H; trivial.
apply match_impl_vmx_update.
apply match_impl_vmcs_update.
apply match_impl_ept_update.
assumption.
Qed.
Context {inv: VMCSSetDefaultsInvariants (data_ops := data_ops) vmx_init_spec}.
Context {inv0: VMCSSetDefaultsInvariants (data_ops := data_ops0) vmx_init_spec}.
Lemma inject_incr_block_inject_neutral s f i b :
find_symbol s i = Some b
→ inject_incr (Mem.flat_inj (genv_next s)) f
→ block_inject_neutral f b.
Proof.
unfold block_inject_neutral; intros symbol_exists incr ?.
apply val_inject_ptr with 0%Z.
- apply incr.
unfold Mem.flat_inj.
destruct (plt b (genv_next s)); try reflexivity.
contradict n.
eapply genv_symb_range; eassumption.
- symmetry; apply Int.add_zero.
Qed.
Lemma vmx_init_sim :
∀ id,
sim (crel RData RData) (id ↦ vmcs_set_defaults_compatsem vmx_init_spec)
(id ↦ vmcs_set_defaults_compatsem vmx_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmx_init_exist; eauto 2 using inject_incr_block_inject_neutral.
intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmx_init_match; eauto.
Qed.
End VMX_INIT_SIM.
End OBJ_SIM.