Library mcertikos.objects.ObjVMCS
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 GlobIdent.
Require Import Z64Lemma.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Section OBJ_VMCS.
Context `{real_params: RealParams}.
Function vmcs_get_revid_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 _ _ ⇒
match revid with
| Vint v ⇒ Some (Int.unsigned v)
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmcs_set_revid_spec (revid: 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 (ZMap.get (CPU_ID adt) (vmcs adt)) with
| VMCSValid _ abrtid data ⇒
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid (Vint (Int.repr revid)) abrtid data) (vmcs adt)}
end
else None
| _ ⇒ None
end.
Function vmcs_get_abrtid_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 _ abrtid _ ⇒
match abrtid with
| Vint v ⇒ Some (Int.unsigned v)
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmcs_set_abrtid_spec (abrtid: 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 (ZMap.get (CPU_ID adt) (vmcs adt)) with
| VMCSValid revid _ data ⇒
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid (Vint (Int.repr abrtid)) data) (vmcs adt)}
end
else None
| _ ⇒ None
end.
Function vmcs_readz_spec (enc: 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 (ZMap.get (CPU_ID adt) (vmcs adt)) with
| VMCSValid _ _ data ⇒
match vmcs_ZtoEncoding enc with
| Some _ ⇒
match ZMap.get enc data with
| Vint v ⇒ Some (Int.unsigned v)
| _ ⇒ None
end
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmcs_writez_spec (enc 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
match (ZMap.get (CPU_ID adt) (vmcs adt)) with
| VMCSValid revid abrtid d ⇒
match vmcs_ZtoEncoding enc with
| Some _ ⇒
let d´ := ZMap.set enc (Vint (Int.repr value)) d in
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid d´) (vmcs adt)}
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmcs_readz64_spec (enc: Z) (adt: RData): option Z64 :=
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 _ _ data ⇒
match vmcs_ZtoEncoding enc with
| Some _ ⇒
match ZMap.get enc data, ZMap.get (enc + 1) data with
| Vint v1, Vint v2 ⇒
Some (VZ64 (Z64ofwords (Int.unsigned v2) (Int.unsigned v1)))
| _, _ ⇒ None
end
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmcs_writez64_spec (enc : Z) (value: Z64) (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 ⇒
match vmcs_ZtoEncoding enc with
| Some _ ⇒
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid (write64_aux enc value d)) (vmcs adt)}
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmcs_Z2ident (v: Z) :=
match v with
| 0 ⇒ Some EPT_LOC
| 1 ⇒ Some tss_LOC
| 2 ⇒ Some gdt_LOC
| 3 ⇒ Some idt_LOC
| 4 ⇒ Some msr_bitmap_LOC
| 5 ⇒ Some io_bitmap_LOC
| 6 ⇒ Some vmx_return_from_guest
| _ ⇒ None
end.
Function vmcs_write_ident_spec (enc: Z) (b: block) (ofs: int) (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 ⇒
match vmcs_ZtoEncoding enc with
| Some _ ⇒
let d´ := ZMap.set enc (Vptr b ofs) d in
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid d´) (vmcs adt)}
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Notation NOT_PROCBASED_INT_WINDOW_EXITING := 4294967291 % Z.
Function vmx_set_intercept_intwin_spec (enable: Z) (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 (CPU_ID adt) (vmcs adt)) with
| VMCSValid revid abrtid d ⇒
match ZMap.get C_VMCS_PRI_PROC_BASED_CTLS d with
| Vint ctrls ⇒
if zeq enable 1 then
let res := Z.lor (Int.unsigned ctrls) PROCBASED_INT_WINDOW_EXITING in
let d´ := ZMap.set C_VMCS_PRI_PROC_BASED_CTLS (Vint (Int.repr res)) d in
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid d´) (vmcs adt)}
else
let res := Z.land (Int.unsigned ctrls) NOT_PROCBASED_INT_WINDOW_EXITING in
let d´ := ZMap.set C_VMCS_PRI_PROC_BASED_CTLS (Vint (Int.repr res)) d in
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid d´) (vmcs adt)}
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Definition aux_zmap_2val_set (k1 v1 k2 v2: Z) (d: ZMap.t val): ZMap.t val :=
ZMap.set k2 (Vint (Int.repr v2)) (ZMap.set k1 (Vint (Int.repr v1)) d).
Definition aux_zmap_4val_set (k1 v1 k2 v2 k3 v3 k4 v4: Z) (d: ZMap.t val): ZMap.t val :=
let d1 := aux_zmap_2val_set k1 v1 k2 v2 d in
aux_zmap_2val_set k3 v3 k4 v4 d1.
Inductive SegDescType :=
| SegDesc4 (ebase elim ear esel: Z)
| SegDesc2 (ebase elim: Z)
| SegUndef.
Function get_seg_desc_paramter (seg: Z) :=
match seg with
| C_GUEST_CS ⇒ SegDesc4
C_VMCS_GUEST_CS_BASE
C_VMCS_GUEST_CS_LIMIT
C_VMCS_GUEST_CS_ACCESS_RIGHTS
C_VMCS_GUEST_CS_SELECTOR
| C_GUEST_SS ⇒ SegDesc4
C_VMCS_GUEST_SS_BASE
C_VMCS_GUEST_SS_LIMIT
C_VMCS_GUEST_SS_ACCESS_RIGHTS
C_VMCS_GUEST_SS_SELECTOR
| C_GUEST_DS ⇒ SegDesc4
C_VMCS_GUEST_DS_BASE
C_VMCS_GUEST_DS_LIMIT
C_VMCS_GUEST_DS_ACCESS_RIGHTS
C_VMCS_GUEST_DS_SELECTOR
| C_GUEST_ES ⇒ SegDesc4
C_VMCS_GUEST_ES_BASE
C_VMCS_GUEST_ES_LIMIT
C_VMCS_GUEST_ES_ACCESS_RIGHTS
C_VMCS_GUEST_ES_SELECTOR
| C_GUEST_FS ⇒ SegDesc4
C_VMCS_GUEST_FS_BASE
C_VMCS_GUEST_FS_LIMIT
C_VMCS_GUEST_FS_ACCESS_RIGHTS
C_VMCS_GUEST_FS_SELECTOR
| C_GUEST_GS ⇒ SegDesc4
C_VMCS_GUEST_GS_BASE
C_VMCS_GUEST_GS_LIMIT
C_VMCS_GUEST_GS_ACCESS_RIGHTS
C_VMCS_GUEST_GS_SELECTOR
| C_GUEST_LDTR ⇒ SegDesc4
C_VMCS_GUEST_LDTR_BASE
C_VMCS_GUEST_LDTR_LIMIT
C_VMCS_GUEST_LDTR_ACCESS_RIGHTS
C_VMCS_GUEST_LDTR_SELECTOR
| C_GUEST_TR ⇒ SegDesc4
C_VMCS_GUEST_TR_BASE
C_VMCS_GUEST_TR_LIMIT
C_VMCS_GUEST_TR_ACCESS_RIGHTS
C_VMCS_GUEST_TR_SELECTOR
| C_GUEST_GDTR ⇒ SegDesc2
C_VMCS_GUEST_GDTR_BASE
C_VMCS_GUEST_GDTR_LIMIT
| C_GUEST_IDTR ⇒ SegDesc2
C_VMCS_GUEST_IDTR_BASE
C_VMCS_GUEST_IDTR_LIMIT
| _ ⇒ SegUndef
end.
Function vmx_set_desc1_aux (seg sel base: Z) (d: ZMap.t val) :=
match get_seg_desc_paramter seg with
| SegDesc4 ebase elim ear esel ⇒ Some (aux_zmap_2val_set ebase base esel sel d)
| SegDesc2 ebase elim ⇒ Some (ZMap.set ebase (Vint (Int.repr base)) d)
| _ ⇒ None
end.
Function vmx_set_desc1_spec (seg sel base: 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 (ZMap.get (CPU_ID adt) (vmcs adt)) with
| VMCSValid revid abrtid d ⇒
match vmx_set_desc1_aux seg sel base d with
| Some d´ ⇒ Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid d´) (vmcs adt)}
| None ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmx_set_desc2_aux (seg lim ar: Z) (d: ZMap.t val) :=
match get_seg_desc_paramter seg with
| SegDesc4 ebase elim ear esel ⇒ Some (aux_zmap_2val_set elim lim ear ar d)
| SegDesc2 ebase elim ⇒ Some (ZMap.set elim (Vint (Int.repr lim)) d)
| _ ⇒ None
end.
Function vmx_set_desc2_spec (seg lim ar: 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 (ZMap.get (CPU_ID adt) (vmcs adt)) with
| VMCSValid revid abrtid d ⇒
match vmx_set_desc2_aux seg lim ar d with
| Some d´ ⇒ Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid d´) (vmcs adt)}
| None ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmx_inject_event_spec (type vector errcode ev : 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 (ZMap.get (CPU_ID adt) (vmcs adt)) with
| VMCSValid revid abrtid d ⇒
match ZMap.get C_VMCS_ENTRY_INTR_INFO d with
| Vint intr_info ⇒
let i := Int.unsigned intr_info in
let is_invalid := Z.land i VMCS_INTERRUPTION_INFO_VALID in
if zeq is_invalid 0 then
let i1 := Z.lor VMCS_INTERRUPTION_INFO_VALID type in
let i2 := Z.lor i1 vector in
if zeq ev 1 then
let i3 := Z.lor i2 VMCS_INTERRUPTION_INFO_EV in
let d1 := ZMap.set C_VMCS_ENTRY_INTR_INFO (Vint (Int.repr i3)) d in
let d2 := ZMap.set C_VMCS_ENTRY_EXCEPTION_ERROR (Vint (Int.repr errcode)) d1 in
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid d2) (vmcs adt)}
else
let d1 := ZMap.set C_VMCS_ENTRY_INTR_INFO (Vint (Int.repr i2)) d in
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid d1) (vmcs adt)}
else
Some adt
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmx_check_pending_event_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 (CPU_ID adt) (vmcs adt)) with
| VMCSValid revid abrtid d ⇒
match ZMap.get C_VMCS_ENTRY_INTR_INFO d with
| Vint ctrls ⇒
if zeq (Z.land (Int.unsigned ctrls) VMCS_INTERRUPTION_INFO_VALID) 0 then
Some 0
else Some 1
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmx_check_int_shadow_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 (CPU_ID adt) (vmcs adt)) with
| VMCSValid revid abrtid d ⇒
match ZMap.get C_VMCS_GUEST_INTERRUPTIBILITY d with
| Vint ctrls ⇒
if zeq (Z.land (Int.unsigned ctrls) VMCS_INTERRUPTIBILITY_STI_or_MOVSS_BLOCKING) 0 then
Some 0
else Some 1
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmx_get_exit_reason_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 C_VMCS_EXIT_REASON d with
| Vint r ⇒ Some (Z.land (Int.unsigned r) EXIT_REASON_MASK)
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmx_set_tsc_offset_spec (tsc_offset: Z64) (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 (CPU_ID adt) (vmcs adt)) with
| VMCSValid revid abrtid d ⇒
Some adt {vmcs: ZMap.set (CPU_ID adt) (VMCSValid revid abrtid (write64_aux C_VMCS_TSC_OFFSET tsc_offset d)) (vmcs adt)}
end
else None
| _ ⇒ None
end.
Function vmx_get_tsc_offset_spec (adt: RData): option Z64 :=
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 C_VMCS_TSC_OFFSET d, ZMap.get (C_VMCS_TSC_OFFSET + 1) d with
| Vint v1, Vint v2 ⇒ Some (VZ64 (Z64ofwords (Int.unsigned v2) (Int.unsigned v1)))
| _ , _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function vmx_get_exit_fault_addr_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 C_VMCS_GUEST_PHYSICAL_ADDRESS d with
| Vint v ⇒ Some (Int.unsigned v)
| _ ⇒ None
end
end
else None
| _ ⇒ None
end.
Function rdmsr_spec (r: Z) (adt: RData) : option Z64 :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some (VZ64 0)
| _ ⇒ None
end.
Function wrmsr_spec (r: Z) (v: Z64) (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some 0
| _ ⇒ None
end.
Function rcr0_spec (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some 0
| _ ⇒ None
end.
Function rcr3_spec (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some 0
| _ ⇒ None
end.
Function rcr4_spec (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some 0
| _ ⇒ None
end.
Function vmptrld_spec (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some adt
| _ ⇒ None
end.
Function vmx_enable_spec (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some adt
| _ ⇒ None
end.
Function vmcs_set_defaults_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)})
else None
else None
| _ ⇒ None
end.
End OBJ_VMCS.
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}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmcs}.
Context {re3: relate_impl_CPU_ID}.
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.
Lemma rdmsr_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem rdmsr_spec)
(id ↦ gensem rdmsr_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
unfold rdmsr_spec in ×.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H2; subrewrite. subdestruct.
inv HQ; trivial.
Qed.
Lemma wrmsr_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem wrmsr_spec)
(id ↦ gensem wrmsr_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
unfold wrmsr_spec in ×.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H2; subrewrite. subdestruct.
inv HQ; trivial.
Qed.
Lemma vmcs_readz_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmcs_readz_spec)
(id ↦ gensem vmcs_readz_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
unfold vmcs_readz_spec in ×.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H2; subrewrite. subdestruct.
exploit relate_impl_vmcs_eq; eauto.
intro.
inversion H1; subst.
erewrite val_inject_vint_eq; eauto.
inv HQ; trivial.
Qed.
Section VMCS_WRITEZ_SIM.
Lemma vmcs_writez_exist:
∀ s habd habd´ labd enc value f,
vmcs_writez_spec enc value habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, vmcs_writez_spec enc value labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmcs_writez_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct.
exploit relate_impl_vmcs_eq; eauto.
intro.
inversion H; 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.
apply VMCS_inj_set_int.
rewrite H9.
apply H.
rewrite ZMap.gso in H5 by assumption.
rewrite ZMap.gso in H7 by assumption.
exploit relate_impl_vmcs_eq; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmcs}.
Lemma vmcs_writez_match:
∀ s d d´ m enc value f,
vmcs_writez_spec enc value d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmcs_writez_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_vmcs_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) vmcs_writez_spec}.
Context {inv0: PreservesInvariants (HD:= data0) vmcs_writez_spec}.
Lemma vmcs_writez_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmcs_writez_spec)
(id ↦ gensem vmcs_writez_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmcs_writez_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmcs_writez_match; eauto.
Qed.
End VMCS_WRITEZ_SIM.
Lemma vmcs_readz64_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmcs_readz64_spec)
(id ↦ gensem vmcs_readz64_spec).
Proof.
Local Opaque Z.shiftl.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
unfold vmcs_readz64_spec in ×.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H2. subrewrite. subdestruct.
exploit relate_impl_vmcs_eq; eauto. intros.
inversion H1; subst.
erewrite 2 val_inject_vint_eq; eauto.
inv HQ; trivial.
Qed.
Section VMCS_WRITEZ64_SIM.
Lemma vmcs_writez64_exist:
∀ s habd habd´ labd enc value f,
vmcs_writez64_spec enc value habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, vmcs_writez64_spec enc value labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmcs_writez64_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct.
exploit relate_impl_vmcs_eq; eauto. intros.
inversion H; 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.
rewrite H9.
apply H.
rewrite ZMap.gso in H5 by assumption.
rewrite ZMap.gso in H7 by assumption.
exploit relate_impl_vmcs_eq; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmcs}.
Lemma vmcs_writez64_match:
∀ s d d´ m enc value f,
vmcs_writez64_spec enc value d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmcs_writez64_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_vmcs_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) vmcs_writez64_spec}.
Context {inv0: PreservesInvariants (HD:= data0) vmcs_writez64_spec}.
Lemma vmcs_writez64_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmcs_writez64_spec)
(id ↦ gensem vmcs_writez64_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmcs_writez64_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmcs_writez64_match; eauto.
Qed.
End VMCS_WRITEZ64_SIM.
Section VMX_SET_INTERCEPT_INTWIN_SIM.
Lemma vmx_set_intercept_intwin_exist:
∀ s habd habd´ labd enable f,
vmx_set_intercept_intwin_spec enable habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, vmx_set_intercept_intwin_spec enable labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmx_set_intercept_intwin_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct.
- exploit relate_impl_vmcs_eq; eauto.
intro tmp; inversion tmp; subst.
erewrite val_inject_vint_eq; eauto.
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.
rewrite H8.
apply tmp.
rewrite ZMap.gso in H3 by assumption.
rewrite ZMap.gso in H6 by assumption.
exploit relate_impl_vmcs_eq; eauto.
- exploit relate_impl_vmcs_eq; eauto.
intro tmp; inversion tmp; subst.
erewrite val_inject_vint_eq; eauto.
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.
rewrite H8.
apply tmp.
rewrite ZMap.gso in H3 by assumption.
rewrite ZMap.gso in H6 by assumption.
exploit relate_impl_vmcs_eq; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmcs}.
Lemma vmx_set_intercept_intwin_match:
∀ s d d´ m enable f,
vmx_set_intercept_intwin_spec enable d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmx_set_intercept_intwin_spec; intros.
subdestruct; inv H; trivial;
eapply match_impl_vmcs_update; assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) vmx_set_intercept_intwin_spec}.
Context {inv0: PreservesInvariants (HD:= data0) vmx_set_intercept_intwin_spec}.
Lemma vmx_set_intercept_intwin_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_set_intercept_intwin_spec)
(id ↦ gensem vmx_set_intercept_intwin_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmx_set_intercept_intwin_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmx_set_intercept_intwin_match; eauto.
Qed.
End VMX_SET_INTERCEPT_INTWIN_SIM.
Section VMX_SET_DESC1_SIM.
Lemma vmx_set_desc1_exist:
∀ s habd habd´ labd seg sel base f,
vmx_set_desc1_spec seg sel base habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, vmx_set_desc1_spec seg sel base labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmx_set_desc1_spec, vmx_set_desc1_aux; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmcs_eq; eauto; intros tmp; inv tmp;
inv HQ; refine_split´;
(trivial || apply relate_impl_vmcs_update;
try assumption; repeat apply VMCS_inj_set_int).
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 H3 by assumption.
rewrite ZMap.gso in H6 by assumption.
exploit relate_impl_vmcs_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 VMCS_inj_set_int.
econstructor; eauto.
rewrite ZMap.gso in H3 by assumption.
rewrite ZMap.gso in H6 by assumption.
exploit relate_impl_vmcs_eq; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmcs}.
Lemma vmx_set_desc1_match:
∀ s d d´ m seg sel base f,
vmx_set_desc1_spec seg sel base d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmx_set_desc1_spec, vmx_set_desc1_aux; intros.
subdestruct; inv H; trivial;
eapply match_impl_vmcs_update; assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) vmx_set_desc1_spec}.
Context {inv0: PreservesInvariants (HD:= data0) vmx_set_desc1_spec}.
Lemma vmx_set_desc1_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_set_desc1_spec)
(id ↦ gensem vmx_set_desc1_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmx_set_desc1_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmx_set_desc1_match; eauto.
Qed.
End VMX_SET_DESC1_SIM.
Section VMX_SET_DESC2_SIM.
Lemma vmx_set_desc2_exist:
∀ s habd habd´ labd seg lim ar f,
vmx_set_desc2_spec seg lim ar habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, vmx_set_desc2_spec seg lim ar labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmx_set_desc2_spec, vmx_set_desc2_aux; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite.
subdestruct;
exploit relate_impl_vmcs_eq; eauto; intros tmp; inv tmp;
inv HQ; refine_split´;
(trivial || apply relate_impl_vmcs_update;
try assumption; repeat apply VMCS_inj_set_int).
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 H3 by assumption.
rewrite ZMap.gso in H6 by assumption.
exploit relate_impl_vmcs_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 VMCS_inj_set_int.
econstructor; eauto.
rewrite ZMap.gso in H3 by assumption.
rewrite ZMap.gso in H6 by assumption.
exploit relate_impl_vmcs_eq; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmcs}.
Lemma vmx_set_desc2_match:
∀ s d d´ m seg lim ar f,
vmx_set_desc2_spec seg lim ar d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmx_set_desc2_spec, vmx_set_desc2_aux; intros.
subdestruct; inv H; trivial;
eapply match_impl_vmcs_update; assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) vmx_set_desc2_spec}.
Context {inv0: PreservesInvariants (HD:= data0) vmx_set_desc2_spec}.
Lemma vmx_set_desc2_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_set_desc2_spec)
(id ↦ gensem vmx_set_desc2_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmx_set_desc2_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmx_set_desc2_match; eauto.
Qed.
End VMX_SET_DESC2_SIM.
Section VMX_INJECT_EVENT_SIM.
Lemma vmx_inject_event_exist:
∀ s habd habd´ labd type vector errcode ev f,
vmx_inject_event_spec type vector errcode ev habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, vmx_inject_event_spec type vector errcode ev labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
Local Opaque Z.land Z.lor.
unfold vmx_inject_event_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct.
- exploit relate_impl_vmcs_eq; eauto. intros.
inv H.
erewrite val_inject_vint_eq; eauto.
subrewrite´.
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 H3 by assumption.
rewrite ZMap.gso in H5 by assumption.
exploit relate_impl_vmcs_eq; eauto.
- exploit relate_impl_vmcs_eq; eauto. intros.
inv H.
erewrite val_inject_vint_eq; eauto.
subrewrite´.
inv HQ; refine_split´; trivial.
- exploit relate_impl_vmcs_eq; eauto. intros.
inv H.
erewrite val_inject_vint_eq; eauto.
subrewrite´.
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 H3 by assumption.
rewrite ZMap.gso in H5 by assumption.
exploit relate_impl_vmcs_eq; eauto.
- exploit relate_impl_vmcs_eq; eauto. intros.
inv H.
erewrite val_inject_vint_eq; eauto.
subrewrite´.
inv HQ; refine_split´; trivial.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmcs}.
Lemma vmx_inject_event_match:
∀ s d d´ m type vecter errcode ev f,
vmx_inject_event_spec type vecter errcode ev d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmx_inject_event_spec; intros.
subdestruct; inv H; trivial;
eapply match_impl_vmcs_update; assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) vmx_inject_event_spec}.
Context {inv0: PreservesInvariants (HD:= data0) vmx_inject_event_spec}.
Lemma vmx_inject_event_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_inject_event_spec)
(id ↦ gensem vmx_inject_event_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmx_inject_event_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmx_inject_event_match; eauto.
Qed.
End VMX_INJECT_EVENT_SIM.
Section VMX_SET_TSC_OFFSET_SIM.
Lemma vmx_set_tsc_offset_exist:
∀ s habd habd´ labd tsc_offset f,
vmx_set_tsc_offset_spec tsc_offset habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, vmx_set_tsc_offset_spec tsc_offset labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmx_set_tsc_offset_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct.
exploit relate_impl_vmcs_eq; eauto. intro tmp; inv tmp.
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 H3 by assumption.
rewrite ZMap.gso in H6 by assumption.
exploit relate_impl_vmcs_eq; eauto.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmcs}.
Lemma vmx_set_tsc_offset_match:
∀ s d d´ m tsc_offset f,
vmx_set_tsc_offset_spec tsc_offset d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold vmx_set_tsc_offset_spec; intros.
subdestruct; inv H; trivial;
eapply match_impl_vmcs_update; assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) vmx_set_tsc_offset_spec}.
Context {inv0: PreservesInvariants (HD:= data0) vmx_set_tsc_offset_spec}.
Lemma vmx_set_tsc_offset_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_set_tsc_offset_spec)
(id ↦ gensem vmx_set_tsc_offset_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmx_set_tsc_offset_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmx_set_tsc_offset_match; eauto.
Qed.
End VMX_SET_TSC_OFFSET_SIM.
Section GET_TSC_SIM.
Lemma vmx_get_tsc_offset_exists:
∀ habd labd z s f,
vmx_get_tsc_offset_spec habd = Some z →
relate_AbData s f habd labd →
vmx_get_tsc_offset_spec labd = Some z.
Proof.
unfold vmx_get_tsc_offset_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct.
exploit relate_impl_vmcs_eq; eauto. intros.
inv H.
erewrite 2 val_inject_vint_eq; eauto.
Qed.
Lemma vmx_get_tsc_offset_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_tsc_offset_spec)
(id ↦ gensem vmx_get_tsc_offset_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite vmx_get_tsc_offset_exists; eauto.
reflexivity.
Qed.
End GET_TSC_SIM.
Section GET_REASON_SIM.
Lemma vmx_get_exit_reason_exists:
∀ habd labd z s f,
vmx_get_exit_reason_spec habd = Some z →
relate_AbData s f habd labd →
vmx_get_exit_reason_spec labd = Some z.
Proof.
unfold vmx_get_exit_reason_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct.
exploit relate_impl_vmcs_eq; eauto. intros.
inv H.
erewrite val_inject_vint_eq; eauto.
Qed.
Lemma vmx_get_exit_reason_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_exit_reason_spec)
(id ↦ gensem vmx_get_exit_reason_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite vmx_get_exit_reason_exists; eauto.
reflexivity.
Qed.
End GET_REASON_SIM.
Section GET_FAULT_SIM.
Lemma vmx_get_exit_fault_addr_exists:
∀ habd labd z s f,
vmx_get_exit_fault_addr_spec habd = Some z →
relate_AbData s f habd labd →
vmx_get_exit_fault_addr_spec labd = Some z.
Proof.
unfold vmx_get_exit_fault_addr_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct.
exploit relate_impl_vmcs_eq; eauto. intros.
inv H.
erewrite val_inject_vint_eq; eauto.
Qed.
Lemma vmx_get_exit_fault_addr_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_get_exit_fault_addr_spec)
(id ↦ gensem vmx_get_exit_fault_addr_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite vmx_get_exit_fault_addr_exists; eauto.
reflexivity.
Qed.
End GET_FAULT_SIM.
Section CHECK_PEND_SIM.
Lemma vmx_check_pending_event_exists:
∀ habd labd z s f,
vmx_check_pending_event_spec habd = Some z →
relate_AbData s f habd labd →
vmx_check_pending_event_spec labd = Some z.
Proof.
unfold vmx_check_pending_event_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct;
exploit relate_impl_vmcs_eq; eauto; intro tmp; inv tmp;
erewrite val_inject_vint_eq; eauto; subrewrite´.
Qed.
Lemma vmx_check_pending_event_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_check_pending_event_spec)
(id ↦ gensem vmx_check_pending_event_spec).
Proof.
Local Opaque Z.land.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite vmx_check_pending_event_exists; eauto.
reflexivity.
Qed.
End CHECK_PEND_SIM.
Section CHECK_INT_SIM.
Lemma vmx_check_int_shadow_exists:
∀ habd labd z s f,
vmx_check_int_shadow_spec habd = Some z →
relate_AbData s f habd labd →
vmx_check_int_shadow_spec labd = Some z.
Proof.
unfold vmx_check_int_shadow_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct;
exploit relate_impl_vmcs_eq; eauto; intro tmp; inv tmp;
erewrite val_inject_vint_eq; eauto; subrewrite´.
Qed.
Lemma vmx_check_int_shadow_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmx_check_int_shadow_spec)
(id ↦ gensem vmx_check_int_shadow_spec).
Proof.
Local Opaque Z.land.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite vmx_check_int_shadow_exists; eauto.
reflexivity.
Qed.
End CHECK_INT_SIM.
Section VMPTRLD_SIM.
Lemma vmptrld_exists:
∀ habd habd´ labd s f,
vmptrld_spec habd = Some habd´ →
relate_AbData s f habd labd →
∃ labd´, vmptrld_spec labd = Some labd´ ∧ relate_AbData s f habd´ labd´.
Proof.
unfold vmptrld_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
revert H. subrewrite. subdestruct.
inv HQ; refine_split´; trivial.
Qed.
Context {mt1: match_impl_iflags}.
Context {inv: PreservesInvariants (HD:= data) vmptrld_spec}.
Context {inv0: PreservesInvariants (HD:= data0) vmptrld_spec}.
Lemma vmptrld_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem vmptrld_spec)
(id ↦ gensem vmptrld_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmptrld_exists; eauto.
intro tmp; destruct tmp.
destruct H.
match_external_states_simpl.
unfold vmptrld_spec in H1.
subdestruct.
inversion H1; subst.
assumption.
Qed.
End VMPTRLD_SIM.
Section VMCS_SET_DEFAULTS_SIM.
Context `{real_params: RealParams}.
Context {re333: relate_impl_ept}.
Context {re4: relate_impl_ipt}.
Context {re5: relate_impl_LAT}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_init}.
Context {re8: relate_impl_PT}.
Context {re9: relate_impl_ptpool}.
Context {re10: relate_impl_idpde}.
Context {re12: relate_impl_smspool}.
Context {re13: relate_impl_abtcb}.
Context {re14: relate_impl_abq}.
Context {re15: relate_impl_cid}.
Context {re16: relate_impl_syncchpool}.
Context {re17: relate_impl_vmxinfo}.
Context {re18: relate_impl_AC}.
Context {re19: relate_impl_in_intr}.
Context {re20: relate_impl_ioapic}.
Context {re21: relate_impl_lapic}.
Context {re22: relate_impl_CPU_ID}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re300: relate_impl_big_log}.
Let block_inject_neutral f b :=
∀ ofs, val_inject f (Vptr b ofs) (Vptr b ofs).
Lemma vmcs_set_defaults_exist:
∀ s habd habd´ labd pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b f,
vmcs_set_defaults_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´, vmcs_set_defaults_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 vmcs_set_defaults_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_in_intr_eq; eauto. inversion 1.
exploit relate_impl_ept_eq; eauto. inversion 1.
revert H. intro. subdestruct.
exploit relate_impl_vmcs_eq; eauto.
intros.
rewrite <- pg_eq, <- ikern_eq, <- ihost_eq.
inv H.
refine_split´; trivial.
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.
inversion H19.
subst.
repeat (apply VMCS_inj_set_int || apply VMCS_inj_set);
try rewrite H; auto.
econstructor.
assumption.
+ intros; subst.
exploit relate_impl_vmcs_eq; eauto; intros.
repeat rewrite ZMap.gso; try auto.
Qed.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_vmcs}.
Context {mt3: match_impl_ept}.
Context {mt4: match_impl_ipt}.
Context {mt5: match_impl_LAT}.
Context {mt6: match_impl_nps}.
Context {mt7: match_impl_init}.
Context {mt8: match_impl_PT}.
Context {mt9: match_impl_ptpool}.
Context {mt10: match_impl_idpde}.
Context {mt12: match_impl_smspool}.
Context {mt13: match_impl_abtcb}.
Context {mt14: match_impl_abq}.
Context {mt15: match_impl_cid}.
Context {mt16: match_impl_syncchpool}.
Context {mt17: match_impl_vmxinfo}.
Context {mt18: match_impl_AC}.
Context {mt19: match_impl_ioapic}.
Context {mt20: match_impl_lapic}.
Context {mt50: match_impl_big_log}.
Context {mt30: match_impl_syncchpool}.
Lemma vmcs_set_defaults_match:
∀ s d d´ m pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b f,
vmcs_set_defaults_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 vmcs_set_defaults_spec; intros.
subdestruct; inv H; trivial.
apply match_impl_vmcs_update.
apply match_impl_ept_update.
assumption.
Qed.
Context {inv: VMCSSetDefaultsInvariants (data_ops := data_ops) vmcs_set_defaults_spec}.
Context {inv0: VMCSSetDefaultsInvariants (data_ops := data_ops0) vmcs_set_defaults_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 vmcs_set_defaults_sim :
∀ id,
sim (crel RData RData) (id ↦ vmcs_set_defaults_compatsem vmcs_set_defaults_spec)
(id ↦ vmcs_set_defaults_compatsem vmcs_set_defaults_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit vmcs_set_defaults_exist; eauto 2 using inject_incr_block_inject_neutral.
intros [labd´ [HP HM]].
match_external_states_simpl.
eapply vmcs_set_defaults_match; eauto.
Qed.
End VMCS_SET_DEFAULTS_SIM.
End OBJ_SIM.