Library mcertikos.layerlib.AuxStateDataType
This file provide some data types that will be used in the layer definitions and refinement proofs
Require Import Coqlib.
Require Import Constant.
Require Import Maps.
Require Import Values.
Require Import Integers.
Require Import AST.
Require Import AsmX.
Require Export AuxFunctions.
Require Import Constant.
Require Import Maps.
Require Import Values.
Require Import Integers.
Require Import AST.
Require Import AsmX.
Require Export AuxFunctions.
*Data types for abstract data
Section MemoryManagement.
Definition PDX (i:Z) := i/(PgSize × one_k).
Definition PTX (i:Z) := (i/PgSize) mod one_k.
Definition PTADDR (i:Z) (ofs:Z) := (i × PgSize) + (ofs mod PgSize).
Definition PageI (i: Z) := i / PgSize.
Lemma size_chunk_range:
∀ chunk,
0≤ size_chunk chunk ≤ 8.
Proof.
induction chunk; simpl; omega.
Qed.
Lemma mod_chunk´:
∀ i,
0 ≤ i < 1024 →
i × 4 ≤ 4096 - size_chunk Mint32.
Proof.
simpl. intros.
omega.
Qed.
Lemma mod_chunk:
∀ i,
(i mod 1024) × 4 ≤ PgSize - size_chunk Mint32.
Proof.
intros.
exploit (Z.mod_pos_bound i 1024).
omega. intros Hrange.
eapply mod_chunk´.
assumption.
Qed.
Lemma HPS: PgSize > 0.
Proof. omega. Qed.
Physical memory intromation table
Inductive MMPerm:=
| MMUsable
| MMResv.
Inductive MMInfo:=
| MMValid (s l:Z) (p: MMPerm)
| MMUndef.
Definition MMTable := ZMap.t MMInfo.
Definition VMXInfo := ZMap.t Z.
Class RealParamsOps : Type :=
{
real_mm: MMTable;
real_size: Z;
real_vmxinfo: VMXInfo
}.
Section MMTable_Property.
| MMUsable
| MMResv.
Inductive MMInfo:=
| MMValid (s l:Z) (p: MMPerm)
| MMUndef.
Definition MMTable := ZMap.t MMInfo.
Definition VMXInfo := ZMap.t Z.
Class RealParamsOps : Type :=
{
real_mm: MMTable;
real_size: Z;
real_vmxinfo: VMXInfo
}.
Section MMTable_Property.
Remark MM_dec (mm: MMTable) (i:Z):
{ ∃ s l p, ZMap.get i mm = MMValid s l p ∧ s ≥ 0 ∧ l > 0 ∧ s + l < Int.max_unsigned}
+{¬∃ s l p, ZMap.get i mm = MMValid s l p ∧ s ≥ 0 ∧ l > 0 ∧ s + l < Int.max_unsigned}.
Proof.
induction (ZMap.get i mm); [|right; red; intros [s´[l´[p´ [HT _]]]]; discriminate].
destruct (zle 0 s); [|right; red; intros [s´[l´[p´ [HT [HF _]]]]]; inv HT; omega].
destruct (zlt 0 l); [|right; red; intros [s´[l´[p´ [HT [_[HF _]]]]]]; inv HT; omega].
destruct (zlt (s + l) Int.max_unsigned); [|right; red; intros [s´[l´[p´ [HT [_[_ HF]]]]]]; inv HT; omega].
left.
∃ s, l, p.
split; trivial.
split; omega.
Qed.
Definition MM_range (mm: MMTable) (lo high: Z) :=
∀ i , lo ≤ i < high → ∃ s l p, (ZMap.get i mm = MMValid s l p ∧ s ≥ 0 ∧ l > 0 ∧ s + l < Int.max_unsigned).
Lemma general_range_dec:
∀ P,
(∀ i, {P i} + {¬P i}) →
∀ lo hi, {∀ i, lo ≤ i < hi → P i} + {¬ ∀ i, lo ≤ i < hi → P i}.
Proof.
intros.
assert(HP: ∀ n, 0 ≤ n
→ {∀ i, lo ≤ i < (lo+n) → P i} + {¬ ∀ i, lo ≤ i < (lo+n) → P i}).
{
apply natlike_rec2.
- left; intros. omegaContradiction.
- destruct 2.
+ destruct (H (lo+z)).
× left; intros.
destruct (zeq i (lo + z)); subst; trivial.
apply p; omega.
× right; red; intro.
assert (lo ≤ (lo+z) < lo + Z.succ z) by omega.
elim n; auto.
+ right; red; intro; elim n; clear n. intros.
assert (lo ≤ i < lo + Z.succ z) by omega.
auto.
}
destruct (zlt lo hi).
replace hi with (lo + (hi - lo)) by omega. apply HP. omega.
left; intros. omegaContradiction.
Qed.
Remark MM_range_dec:
∀ mm lo high, {MM_range mm lo high} + {¬MM_range mm lo high}.
Proof.
intros. unfold MM_range.
eapply general_range_dec. intros.
apply MM_dec.
Qed.
Definition MM_valid (mm: MMTable) (size: Z) := MM_range mm 0 size.
Remark MM_valid_dec (mm: MMTable) (size: Z) :
{MM_valid mm size} +{¬MM_valid mm size}.
Proof.
unfold MM_valid.
apply (MM_range_dec mm 0 size).
Qed.
Definition perm_consist (s1 s2 l1 l2 :Z) (p1 p2: MMPerm):=
s1 < s2 + l2 → s2 < s1 + l1 → p1 = p2.
Remark perm_consist_dec (s1 s2 l1 l2 :Z) (p1 p2: MMPerm) :
{perm_consist s1 s2 l1 l2 p1 p2} + {¬perm_consist s1 s2 l1 l2 p1 p2}.
Proof.
unfold perm_consist.
destruct(Z_lt_dec s1 (s2+l2)).
destruct(Z_lt_dec s2 (s1+l1)).
assert(HP1: {p1 = p2} + {¬p1 = p2}) by decide equality.
destruct HP1; [left; auto| right; red; auto].
left; intros; omegaContradiction.
left; intros; omega.
Qed.
Remark MMPerm_dec (p1 p2: MMPerm) :
{ p1 = p2} + { p1 ≠ p2}.
Proof.
decide equality.
Qed.
Definition MM_correct_pos (mm: MMTable) (i j: Z) :=
∀ s1 s2 l1 l2 p1 p2,
ZMap.get i mm = MMValid s1 l1 p1
→ ZMap.get j mm = MMValid s2 l2 p2
→ perm_consist s1 s2 l1 l2 p1 p2.
Remark MM_correct_pos_dec (mm: MMTable) (i j:Z) :
{MM_correct_pos mm i j} + {¬ MM_correct_pos mm i j}.
Proof.
unfold MM_correct_pos.
destruct (ZMap.get i mm); [| left; intros; discriminate].
destruct (ZMap.get j mm); [| left; intros; discriminate].
unfold perm_consist.
destruct (MMPerm_dec p p0).
left; intros; inv H; inv H0; trivial.
destruct (zlt s (s0 + l0)).
destruct (zlt s0 (s + l)).
right; red; intros. elim n; eauto.
left; intros; inv H; inv H0; omega.
left; intros; inv H; inv H0; omega.
Qed.
Definition MM_correct1 (mm: MMTable) (i size: Z) :=
∀ j, 0≤ j < size → MM_correct_pos mm i j.
Remark MM_correct1_dec (mm: MMTable) (i size:Z) :
{MM_correct1 mm i size} + {¬ MM_correct1 mm i size}.
Proof.
unfold MM_correct1.
eapply general_range_dec. intros.
apply MM_correct_pos_dec.
Qed.
Definition MM_correct2 (mm: MMTable) (size size2: Z) :=
∀ i, 0≤ i < size → MM_correct1 mm i size2.
Remark MM_correct2_dec (mm: MMTable) (size size2:Z) :
{MM_correct2 mm size size2} + {¬ MM_correct2 mm size size2}.
Proof.
unfold MM_correct2.
eapply general_range_dec. intros.
apply MM_correct1_dec.
Qed.
Definition MM_correct (mm: MMTable) (size: Z) :=
∀ i j s1 s2 l1 l2 p1 p2,
0≤ i < size → 0≤ j < size
→ ZMap.get i mm = MMValid s1 l1 p1
→ ZMap.get j mm = MMValid s2 l2 p2
→ perm_consist s1 s2 l1 l2 p1 p2.
Remark MM_correct_dec (mm: MMTable) (size:Z) :
{MM_correct mm size} + {¬ MM_correct mm size}.
Proof.
destruct (MM_correct2_dec mm size size).
left; unfold MM_correct, MM_correct2, MM_correct1, MM_correct_pos in *; eauto.
right;red;intro; apply n.
unfold MM_correct2, MM_correct1, MM_correct_pos; eauto.
Qed.
Definition MM_kern_valid (mm: MMTable)(n size:Z):=
∃ i s l,
0≤ i < size ∧ ZMap.get i mm = MMValid s l MMUsable ∧ s≤ n × PgSize ∧ l + s ≥ ((n+1)* PgSize).
Remark MM_kern_valid_dec (mm:MMTable) (n size:Z) :
{MM_kern_valid mm n size} +{¬MM_kern_valid mm n size}.
Proof.
assert(HQ: ∀ k, 0≤ k → {MM_kern_valid mm n k} +{¬MM_kern_valid mm n k}).
unfold MM_kern_valid; apply natlike_rec2.
right; red; intros; destruct H as [i[_[_[HI _]]]]; omega.
destruct 2.
left.
destruct e as [i [s[l[HI[HM[HS HL]]]]]].
∃ i, s, l; repeat (split;trivial); omega.
Ltac right_simpl H0 H1 z n0:=
right; red; intros; destruct H1 as [i´[s´[l´ HM]]]; destruct (zeq i´ z);
[subst; destruct HM as [_ [HM [HM1 HF]]]; rewrite H0 in HM; inv HM; try omega
| elim n0; ∃ i´, s´, l´; destruct HM as [HM1 HM2]; split; trivial; omega].
caseEq (ZMap.get z mm); intros; [|right_simpl H0 H1 z n0].
destruct (MMPerm_dec p MMUsable); [|right_simpl H0 H1 z n0; elim n1; trivial].
destruct (zle s (n × PgSize)); [|right_simpl H0 H1 z n0].
destruct (zle ((n+1)*PgSize) (l + s)); [|right_simpl H0 H1 z n0].
left; ∃ z, s, l.
rewrite e in H0.
repeat(split;trivial);
omega.
destruct (Z_le_dec size 0).
right; red; unfold MM_kern_valid; intro.
destruct H as [i[_[_[HI _]]]]; omega.
apply HQ; omega.
Qed.
Definition MM_kern_range (mm:MMTable) (n size: Z):=
∀ i, 0≤ i < n → MM_kern_valid mm i size.
Definition MM_kern (mm:MMTable) (size: Z):=
MM_kern_range mm kern_low size.
End MMTable_Property.
Definition trapinfo := prod int val.
Definition init_trap_info : trapinfo := (Int.zero, Vzero).
Inductive globalpointer :=
| GLOBP (b: ident) (ofs: int)
| GLOBUndef.
Section CR3_Property.
Definition CR3_valid (pt: globalpointer) := ∃ b ofs, pt = GLOBP b ofs.
Remark CR3_valid_dec (pt: globalpointer) :
{CR3_valid pt } + { ¬ CR3_valid pt}.
Proof.
unfold CR3_valid.
destruct pt.
left.
eauto.
right.
red; intros.
destruct H as [b0 [ofs0 HG]].
inv HG.
Qed.
End CR3_Property.
Section CONTAINER.
{ ∃ s l p, ZMap.get i mm = MMValid s l p ∧ s ≥ 0 ∧ l > 0 ∧ s + l < Int.max_unsigned}
+{¬∃ s l p, ZMap.get i mm = MMValid s l p ∧ s ≥ 0 ∧ l > 0 ∧ s + l < Int.max_unsigned}.
Proof.
induction (ZMap.get i mm); [|right; red; intros [s´[l´[p´ [HT _]]]]; discriminate].
destruct (zle 0 s); [|right; red; intros [s´[l´[p´ [HT [HF _]]]]]; inv HT; omega].
destruct (zlt 0 l); [|right; red; intros [s´[l´[p´ [HT [_[HF _]]]]]]; inv HT; omega].
destruct (zlt (s + l) Int.max_unsigned); [|right; red; intros [s´[l´[p´ [HT [_[_ HF]]]]]]; inv HT; omega].
left.
∃ s, l, p.
split; trivial.
split; omega.
Qed.
Definition MM_range (mm: MMTable) (lo high: Z) :=
∀ i , lo ≤ i < high → ∃ s l p, (ZMap.get i mm = MMValid s l p ∧ s ≥ 0 ∧ l > 0 ∧ s + l < Int.max_unsigned).
Lemma general_range_dec:
∀ P,
(∀ i, {P i} + {¬P i}) →
∀ lo hi, {∀ i, lo ≤ i < hi → P i} + {¬ ∀ i, lo ≤ i < hi → P i}.
Proof.
intros.
assert(HP: ∀ n, 0 ≤ n
→ {∀ i, lo ≤ i < (lo+n) → P i} + {¬ ∀ i, lo ≤ i < (lo+n) → P i}).
{
apply natlike_rec2.
- left; intros. omegaContradiction.
- destruct 2.
+ destruct (H (lo+z)).
× left; intros.
destruct (zeq i (lo + z)); subst; trivial.
apply p; omega.
× right; red; intro.
assert (lo ≤ (lo+z) < lo + Z.succ z) by omega.
elim n; auto.
+ right; red; intro; elim n; clear n. intros.
assert (lo ≤ i < lo + Z.succ z) by omega.
auto.
}
destruct (zlt lo hi).
replace hi with (lo + (hi - lo)) by omega. apply HP. omega.
left; intros. omegaContradiction.
Qed.
Remark MM_range_dec:
∀ mm lo high, {MM_range mm lo high} + {¬MM_range mm lo high}.
Proof.
intros. unfold MM_range.
eapply general_range_dec. intros.
apply MM_dec.
Qed.
Definition MM_valid (mm: MMTable) (size: Z) := MM_range mm 0 size.
Remark MM_valid_dec (mm: MMTable) (size: Z) :
{MM_valid mm size} +{¬MM_valid mm size}.
Proof.
unfold MM_valid.
apply (MM_range_dec mm 0 size).
Qed.
Definition perm_consist (s1 s2 l1 l2 :Z) (p1 p2: MMPerm):=
s1 < s2 + l2 → s2 < s1 + l1 → p1 = p2.
Remark perm_consist_dec (s1 s2 l1 l2 :Z) (p1 p2: MMPerm) :
{perm_consist s1 s2 l1 l2 p1 p2} + {¬perm_consist s1 s2 l1 l2 p1 p2}.
Proof.
unfold perm_consist.
destruct(Z_lt_dec s1 (s2+l2)).
destruct(Z_lt_dec s2 (s1+l1)).
assert(HP1: {p1 = p2} + {¬p1 = p2}) by decide equality.
destruct HP1; [left; auto| right; red; auto].
left; intros; omegaContradiction.
left; intros; omega.
Qed.
Remark MMPerm_dec (p1 p2: MMPerm) :
{ p1 = p2} + { p1 ≠ p2}.
Proof.
decide equality.
Qed.
Definition MM_correct_pos (mm: MMTable) (i j: Z) :=
∀ s1 s2 l1 l2 p1 p2,
ZMap.get i mm = MMValid s1 l1 p1
→ ZMap.get j mm = MMValid s2 l2 p2
→ perm_consist s1 s2 l1 l2 p1 p2.
Remark MM_correct_pos_dec (mm: MMTable) (i j:Z) :
{MM_correct_pos mm i j} + {¬ MM_correct_pos mm i j}.
Proof.
unfold MM_correct_pos.
destruct (ZMap.get i mm); [| left; intros; discriminate].
destruct (ZMap.get j mm); [| left; intros; discriminate].
unfold perm_consist.
destruct (MMPerm_dec p p0).
left; intros; inv H; inv H0; trivial.
destruct (zlt s (s0 + l0)).
destruct (zlt s0 (s + l)).
right; red; intros. elim n; eauto.
left; intros; inv H; inv H0; omega.
left; intros; inv H; inv H0; omega.
Qed.
Definition MM_correct1 (mm: MMTable) (i size: Z) :=
∀ j, 0≤ j < size → MM_correct_pos mm i j.
Remark MM_correct1_dec (mm: MMTable) (i size:Z) :
{MM_correct1 mm i size} + {¬ MM_correct1 mm i size}.
Proof.
unfold MM_correct1.
eapply general_range_dec. intros.
apply MM_correct_pos_dec.
Qed.
Definition MM_correct2 (mm: MMTable) (size size2: Z) :=
∀ i, 0≤ i < size → MM_correct1 mm i size2.
Remark MM_correct2_dec (mm: MMTable) (size size2:Z) :
{MM_correct2 mm size size2} + {¬ MM_correct2 mm size size2}.
Proof.
unfold MM_correct2.
eapply general_range_dec. intros.
apply MM_correct1_dec.
Qed.
Definition MM_correct (mm: MMTable) (size: Z) :=
∀ i j s1 s2 l1 l2 p1 p2,
0≤ i < size → 0≤ j < size
→ ZMap.get i mm = MMValid s1 l1 p1
→ ZMap.get j mm = MMValid s2 l2 p2
→ perm_consist s1 s2 l1 l2 p1 p2.
Remark MM_correct_dec (mm: MMTable) (size:Z) :
{MM_correct mm size} + {¬ MM_correct mm size}.
Proof.
destruct (MM_correct2_dec mm size size).
left; unfold MM_correct, MM_correct2, MM_correct1, MM_correct_pos in *; eauto.
right;red;intro; apply n.
unfold MM_correct2, MM_correct1, MM_correct_pos; eauto.
Qed.
Definition MM_kern_valid (mm: MMTable)(n size:Z):=
∃ i s l,
0≤ i < size ∧ ZMap.get i mm = MMValid s l MMUsable ∧ s≤ n × PgSize ∧ l + s ≥ ((n+1)* PgSize).
Remark MM_kern_valid_dec (mm:MMTable) (n size:Z) :
{MM_kern_valid mm n size} +{¬MM_kern_valid mm n size}.
Proof.
assert(HQ: ∀ k, 0≤ k → {MM_kern_valid mm n k} +{¬MM_kern_valid mm n k}).
unfold MM_kern_valid; apply natlike_rec2.
right; red; intros; destruct H as [i[_[_[HI _]]]]; omega.
destruct 2.
left.
destruct e as [i [s[l[HI[HM[HS HL]]]]]].
∃ i, s, l; repeat (split;trivial); omega.
Ltac right_simpl H0 H1 z n0:=
right; red; intros; destruct H1 as [i´[s´[l´ HM]]]; destruct (zeq i´ z);
[subst; destruct HM as [_ [HM [HM1 HF]]]; rewrite H0 in HM; inv HM; try omega
| elim n0; ∃ i´, s´, l´; destruct HM as [HM1 HM2]; split; trivial; omega].
caseEq (ZMap.get z mm); intros; [|right_simpl H0 H1 z n0].
destruct (MMPerm_dec p MMUsable); [|right_simpl H0 H1 z n0; elim n1; trivial].
destruct (zle s (n × PgSize)); [|right_simpl H0 H1 z n0].
destruct (zle ((n+1)*PgSize) (l + s)); [|right_simpl H0 H1 z n0].
left; ∃ z, s, l.
rewrite e in H0.
repeat(split;trivial);
omega.
destruct (Z_le_dec size 0).
right; red; unfold MM_kern_valid; intro.
destruct H as [i[_[_[HI _]]]]; omega.
apply HQ; omega.
Qed.
Definition MM_kern_range (mm:MMTable) (n size: Z):=
∀ i, 0≤ i < n → MM_kern_valid mm i size.
Definition MM_kern (mm:MMTable) (size: Z):=
MM_kern_range mm kern_low size.
End MMTable_Property.
Definition trapinfo := prod int val.
Definition init_trap_info : trapinfo := (Int.zero, Vzero).
Inductive globalpointer :=
| GLOBP (b: ident) (ofs: int)
| GLOBUndef.
Section CR3_Property.
Definition CR3_valid (pt: globalpointer) := ∃ b ofs, pt = GLOBP b ofs.
Remark CR3_valid_dec (pt: globalpointer) :
{CR3_valid pt } + { ¬ CR3_valid pt}.
Proof.
unfold CR3_valid.
destruct pt.
left.
eauto.
right.
red; intros.
destruct H as [b0 [ofs0 HG]].
inv HG.
Qed.
End CR3_Property.
Section CONTAINER.
Agent Container
Inductive Container : Type :=
mkContainer {
cquota : Z;
cusage : Z;
cparent : Z;
cchildren : list Z;
cused : bool
}.
Definition ContainerPool : Type := ZMap.t Container.
Definition Container_unused := mkContainer 0 0 0 nil false.
Section Container_Property.
Inductive child_quotas_bounded : ContainerPool → list Z → Z → Prop :=
| cqb_nil : ∀ C n, 0 ≤ n → child_quotas_bounded C nil n
| cqb_cons : ∀ C c cs n m, 0 ≤ cquota (ZMap.get c C) ≤ m →
child_quotas_bounded C cs n →
child_quotas_bounded C (c::cs) (n+m).
Lemma cqb_nonneg : ∀ cs C n, child_quotas_bounded C cs n → 0 ≤ n.
Proof.
induction cs; simpl; intros.
inv H; auto.
inv H.
apply Z.add_nonneg_nonneg; try omega.
apply (IHcs C); auto.
Qed.
Lemma cqb_bound : ∀ cs C n1 n2, child_quotas_bounded C cs n1 →
n1 ≤ n2 → child_quotas_bounded C cs n2.
Proof.
induction cs; simpl; intros.
inv H; constructor; omega.
inv H.
apply (IHcs _ _ (n2-m)) in H6; try omega.
replace n2 with (n2 - m + m); try omega.
constructor; auto.
Qed.
Lemma cqb_notin : ∀ cs C c n con,
child_quotas_bounded C cs n → ¬ In c cs →
child_quotas_bounded (ZMap.set c con C) cs n.
Proof.
induction cs; simpl; intros.
inv H; constructor; auto.
inv H; constructor; auto.
rewrite ZMap.gso; auto.
Qed.
Lemma cqb_weaken : ∀ cs C c n con,
child_quotas_bounded C cs n → 0 ≤ cquota con ≤ cquota (ZMap.get c C) →
child_quotas_bounded (ZMap.set c con C) cs n.
Proof.
induction cs; simpl; intros.
inv H; constructor; auto.
inv H; constructor; auto.
destruct (zeq a c); subst.
rewrite ZMap.gss; omega.
rewrite ZMap.gso; auto.
Qed.
Fact remove_notin {A} : ∀ (l : list A) a eq, ¬ In a l → remove eq a l = l.
Proof.
induction l; simpl; intros; auto.
destruct (eq a0 a); subst.
contradict H; auto.
rewrite IHl; auto.
Qed.
Lemma cqb_remove : ∀ cs C c n,
child_quotas_bounded C cs n → In c cs →
child_quotas_bounded C (remove zeq c cs) (n - cquota (ZMap.get c C)).
Proof.
induction cs; simpl; intros.
inv H0.
inv H.
destruct (in_dec zeq c cs) as [Hin|Hnin].
destruct (zeq c a); subst.
apply (IHcs _ a) in H6; auto.
apply cqb_bound with (n1 := n0 - cquota (ZMap.get a C)); auto; try omega.
replace (n0 + m - cquota (ZMap.get c C)) with (n0 - cquota (ZMap.get c C) + m); try omega.
constructor; auto.
destruct H0; subst; try contradiction.
destruct (zeq c c).
apply cqb_bound with (n1 := n0); try omega.
rewrite remove_notin; auto.
contradict n; auto.
Qed.
Inductive Container_valid (C : ContainerPool) : Prop :=
mkContainer_valid {
cvalid_id : ∀ i, cused (ZMap.get i C) = true → 0 ≤ i < num_proc;
cvalid_root : ∀ i, cused (ZMap.get i C) = true →
(i = cparent (ZMap.get i C) ↔ i = 0);
cvalid_quota : ∀ i, cused (ZMap.get i C) = true →
cquota (ZMap.get i C) ≤ Int.max_unsigned;
cvalid_usage : ∀ i, cused (ZMap.get i C) = true →
0 ≤ cusage (ZMap.get i C) ≤ cquota (ZMap.get i C);
cvalid_parent_used : ∀ i, cused (ZMap.get i C) = true →
cused (ZMap.get (cparent (ZMap.get i C)) C) = true;
cvalid_children_used : ∀ i, cused (ZMap.get i C) = true →
Forall (fun j ⇒ cused (ZMap.get j C) = true) (cchildren (ZMap.get i C));
cvalid_parents_child : ∀ i, cused (ZMap.get i C) = true → (i ≠ 0)%Z →
In i (cchildren (ZMap.get (cparent (ZMap.get i C)) C));
cvalid_childrens_parent : ∀ i, cused (ZMap.get i C) = true →
Forall (fun j ⇒ cparent (ZMap.get j C) = i) (cchildren (ZMap.get i C));
cvalid_cqb : ∀ i, cused (ZMap.get i C) = true →
child_quotas_bounded C (cchildren (ZMap.get i C)) (cusage (ZMap.get i C));
cvalid_nodup : ∀ i, cused (ZMap.get i C) = true →
NoDup (cchildren (ZMap.get i C))
}.
End Container_Property.
Fixpoint init_container_children (i : nat) (lst : list Z) : list Z :=
match i with
| O ⇒ (1::nil)
| S k ⇒ let prev := init_container_children k nil in
(Z.of_nat (S k) + 1)::prev
end.
Definition init_container : Container := (mkContainer (root_quota/TOTAL_CPU) 0 0 nil true).
Fixpoint init_cal_container (i : nat) (ACPool : ContainerPool) : ContainerPool :=
match i with
| O ⇒ ZMap.set 1 init_container ACPool
| S k ⇒ ZMap.set (Z.of_nat (S k) + 1) init_container (init_cal_container k ACPool)
end.
Definition init_real_container : ContainerPool :=
init_cal_container (Z.to_nat (TOTAL_CPU - 1))
(ZMap.set 0 (mkContainer root_quota root_quota 0
(init_container_children (Z.to_nat (TOTAL_CPU - 1)) nil)
true) (ZMap.init Container_unused)).
Definition AC_init := init_real_container.
End CONTAINER.
mkContainer {
cquota : Z;
cusage : Z;
cparent : Z;
cchildren : list Z;
cused : bool
}.
Definition ContainerPool : Type := ZMap.t Container.
Definition Container_unused := mkContainer 0 0 0 nil false.
Section Container_Property.
Inductive child_quotas_bounded : ContainerPool → list Z → Z → Prop :=
| cqb_nil : ∀ C n, 0 ≤ n → child_quotas_bounded C nil n
| cqb_cons : ∀ C c cs n m, 0 ≤ cquota (ZMap.get c C) ≤ m →
child_quotas_bounded C cs n →
child_quotas_bounded C (c::cs) (n+m).
Lemma cqb_nonneg : ∀ cs C n, child_quotas_bounded C cs n → 0 ≤ n.
Proof.
induction cs; simpl; intros.
inv H; auto.
inv H.
apply Z.add_nonneg_nonneg; try omega.
apply (IHcs C); auto.
Qed.
Lemma cqb_bound : ∀ cs C n1 n2, child_quotas_bounded C cs n1 →
n1 ≤ n2 → child_quotas_bounded C cs n2.
Proof.
induction cs; simpl; intros.
inv H; constructor; omega.
inv H.
apply (IHcs _ _ (n2-m)) in H6; try omega.
replace n2 with (n2 - m + m); try omega.
constructor; auto.
Qed.
Lemma cqb_notin : ∀ cs C c n con,
child_quotas_bounded C cs n → ¬ In c cs →
child_quotas_bounded (ZMap.set c con C) cs n.
Proof.
induction cs; simpl; intros.
inv H; constructor; auto.
inv H; constructor; auto.
rewrite ZMap.gso; auto.
Qed.
Lemma cqb_weaken : ∀ cs C c n con,
child_quotas_bounded C cs n → 0 ≤ cquota con ≤ cquota (ZMap.get c C) →
child_quotas_bounded (ZMap.set c con C) cs n.
Proof.
induction cs; simpl; intros.
inv H; constructor; auto.
inv H; constructor; auto.
destruct (zeq a c); subst.
rewrite ZMap.gss; omega.
rewrite ZMap.gso; auto.
Qed.
Fact remove_notin {A} : ∀ (l : list A) a eq, ¬ In a l → remove eq a l = l.
Proof.
induction l; simpl; intros; auto.
destruct (eq a0 a); subst.
contradict H; auto.
rewrite IHl; auto.
Qed.
Lemma cqb_remove : ∀ cs C c n,
child_quotas_bounded C cs n → In c cs →
child_quotas_bounded C (remove zeq c cs) (n - cquota (ZMap.get c C)).
Proof.
induction cs; simpl; intros.
inv H0.
inv H.
destruct (in_dec zeq c cs) as [Hin|Hnin].
destruct (zeq c a); subst.
apply (IHcs _ a) in H6; auto.
apply cqb_bound with (n1 := n0 - cquota (ZMap.get a C)); auto; try omega.
replace (n0 + m - cquota (ZMap.get c C)) with (n0 - cquota (ZMap.get c C) + m); try omega.
constructor; auto.
destruct H0; subst; try contradiction.
destruct (zeq c c).
apply cqb_bound with (n1 := n0); try omega.
rewrite remove_notin; auto.
contradict n; auto.
Qed.
Inductive Container_valid (C : ContainerPool) : Prop :=
mkContainer_valid {
cvalid_id : ∀ i, cused (ZMap.get i C) = true → 0 ≤ i < num_proc;
cvalid_root : ∀ i, cused (ZMap.get i C) = true →
(i = cparent (ZMap.get i C) ↔ i = 0);
cvalid_quota : ∀ i, cused (ZMap.get i C) = true →
cquota (ZMap.get i C) ≤ Int.max_unsigned;
cvalid_usage : ∀ i, cused (ZMap.get i C) = true →
0 ≤ cusage (ZMap.get i C) ≤ cquota (ZMap.get i C);
cvalid_parent_used : ∀ i, cused (ZMap.get i C) = true →
cused (ZMap.get (cparent (ZMap.get i C)) C) = true;
cvalid_children_used : ∀ i, cused (ZMap.get i C) = true →
Forall (fun j ⇒ cused (ZMap.get j C) = true) (cchildren (ZMap.get i C));
cvalid_parents_child : ∀ i, cused (ZMap.get i C) = true → (i ≠ 0)%Z →
In i (cchildren (ZMap.get (cparent (ZMap.get i C)) C));
cvalid_childrens_parent : ∀ i, cused (ZMap.get i C) = true →
Forall (fun j ⇒ cparent (ZMap.get j C) = i) (cchildren (ZMap.get i C));
cvalid_cqb : ∀ i, cused (ZMap.get i C) = true →
child_quotas_bounded C (cchildren (ZMap.get i C)) (cusage (ZMap.get i C));
cvalid_nodup : ∀ i, cused (ZMap.get i C) = true →
NoDup (cchildren (ZMap.get i C))
}.
End Container_Property.
Fixpoint init_container_children (i : nat) (lst : list Z) : list Z :=
match i with
| O ⇒ (1::nil)
| S k ⇒ let prev := init_container_children k nil in
(Z.of_nat (S k) + 1)::prev
end.
Definition init_container : Container := (mkContainer (root_quota/TOTAL_CPU) 0 0 nil true).
Fixpoint init_cal_container (i : nat) (ACPool : ContainerPool) : ContainerPool :=
match i with
| O ⇒ ZMap.set 1 init_container ACPool
| S k ⇒ ZMap.set (Z.of_nat (S k) + 1) init_container (init_cal_container k ACPool)
end.
Definition init_real_container : ContainerPool :=
init_cal_container (Z.to_nat (TOTAL_CPU - 1))
(ZMap.set 0 (mkContainer root_quota root_quota 0
(init_container_children (Z.to_nat (TOTAL_CPU - 1)) nil)
true) (ZMap.init Container_unused)).
Definition AC_init := init_real_container.
End CONTAINER.
Allocation table
Inductive ATType: Type :=
| ATKern
| ATResv
| ATNorm.
Remark ATType_dec:
∀ x y: ATType,
{x = y} + {x ≠ y}.
Proof.
intros. repeat progress (decide equality).
Qed.
Inductive ATInfo :=
| ATValid (b: bool) (t: ATType)
| ATUndef.
Definition ATable := ZMap.t ATInfo.
Inductive ATCInfo :=
| ATCValid (n: Z)
| ATCUndef.
Definition ATCTable := ZMap.t ATCInfo.
Function ZtoATType (i: Z) : option ATType :=
match i with
| 0 ⇒ Some ATResv
| 1 ⇒ Some ATKern
| 2 ⇒ Some ATNorm
| _ ⇒ None
end.
Definition IntToBoolZ (n: int) : Z :=
if Int.eq n Int.zero then 0
else 1.
Definition ZToATTypeZ (n: Z) : Z :=
if zeq n 0 then 0
else if zeq n 1 then 0
else 1.
Section AT_Property.
Definition AT_kern (AT: ATable) (nps: Z) :=
∀ i, 0≤ i < kern_low ∨ kern_high ≤ i < nps
→ ZMap.get i AT = ATValid false ATKern.
Definition AT_usr (AT: ATable) (nps: Z):=
∀ i, kern_low ≤ i < Z.min kern_high nps
→ ∃ b, (ZMap.get i AT = ATValid b ATNorm)
∨ ZMap.get i AT = ATValid b ATResv.
Remark AT_dec (info: ATInfo) (b: bool) (t: ATType):
{info = ATValid b t} + {¬info = ATValid b t}.
Proof.
repeat progress (decide equality).
Qed.
Lemma min_ex: ∀ (P: Z → Prop) lo hi,
(∀ n, {P n} + {¬ P n}) →
{n : Z | lo < n < hi ∧ P n ∧ ∀ n´, lo < n´ < n → ¬ P n´} +
{∀ n, lo < n < hi → ¬ P n}.
Proof.
intros.
assert(HP: ∀ k,
0 ≤ k → {n : Z | lo < n < lo + k + 1 ∧ P n ∧ (∀ n´ : Z, lo < n´ < n → ¬ P n´)} +
{(∀ n : Z, lo < n < lo + k + 1 → ¬ P n)}).
{
apply natlike_rec2.
- right; intros; omega.
- intros z HR HT.
destruct HT.
+ left; destruct s as [n[HT HM]].
∃ n; split; trivial; omega.
+ specialize (H (lo + z + 1)).
destruct H.
× left; ∃ (lo + z + 1); split; auto; omega.
× right; intros; destruct (zeq n1 (lo + z + 1)); subst; trivial; apply n; omega.
}
destruct (zlt lo hi).
- replace hi with (lo + (hi - lo - 1) + 1) by omega. apply HP. omega.
- right; intros. omegaContradiction.
Qed.
| ATKern
| ATResv
| ATNorm.
Remark ATType_dec:
∀ x y: ATType,
{x = y} + {x ≠ y}.
Proof.
intros. repeat progress (decide equality).
Qed.
Inductive ATInfo :=
| ATValid (b: bool) (t: ATType)
| ATUndef.
Definition ATable := ZMap.t ATInfo.
Inductive ATCInfo :=
| ATCValid (n: Z)
| ATCUndef.
Definition ATCTable := ZMap.t ATCInfo.
Function ZtoATType (i: Z) : option ATType :=
match i with
| 0 ⇒ Some ATResv
| 1 ⇒ Some ATKern
| 2 ⇒ Some ATNorm
| _ ⇒ None
end.
Definition IntToBoolZ (n: int) : Z :=
if Int.eq n Int.zero then 0
else 1.
Definition ZToATTypeZ (n: Z) : Z :=
if zeq n 0 then 0
else if zeq n 1 then 0
else 1.
Section AT_Property.
Definition AT_kern (AT: ATable) (nps: Z) :=
∀ i, 0≤ i < kern_low ∨ kern_high ≤ i < nps
→ ZMap.get i AT = ATValid false ATKern.
Definition AT_usr (AT: ATable) (nps: Z):=
∀ i, kern_low ≤ i < Z.min kern_high nps
→ ∃ b, (ZMap.get i AT = ATValid b ATNorm)
∨ ZMap.get i AT = ATValid b ATResv.
Remark AT_dec (info: ATInfo) (b: bool) (t: ATType):
{info = ATValid b t} + {¬info = ATValid b t}.
Proof.
repeat progress (decide equality).
Qed.
Lemma min_ex: ∀ (P: Z → Prop) lo hi,
(∀ n, {P n} + {¬ P n}) →
{n : Z | lo < n < hi ∧ P n ∧ ∀ n´, lo < n´ < n → ¬ P n´} +
{∀ n, lo < n < hi → ¬ P n}.
Proof.
intros.
assert(HP: ∀ k,
0 ≤ k → {n : Z | lo < n < lo + k + 1 ∧ P n ∧ (∀ n´ : Z, lo < n´ < n → ¬ P n´)} +
{(∀ n : Z, lo < n < lo + k + 1 → ¬ P n)}).
{
apply natlike_rec2.
- right; intros; omega.
- intros z HR HT.
destruct HT.
+ left; destruct s as [n[HT HM]].
∃ n; split; trivial; omega.
+ specialize (H (lo + z + 1)).
destruct H.
× left; ∃ (lo + z + 1); split; auto; omega.
× right; intros; destruct (zeq n1 (lo + z + 1)); subst; trivial; apply n; omega.
}
destruct (zlt lo hi).
- replace hi with (lo + (hi - lo - 1) + 1) by omega. apply HP. omega.
- right; intros. omegaContradiction.
Qed.
Definition first_free (At: ATable) (size: Z) :
{n| 0 < n < size ∧ ZMap.get n At = ATValid false ATNorm ∧
(∀ x, 0 < x < n → ¬ ZMap.get x At = ATValid false ATNorm)}
+ {∀ x, 0 < x < size → ¬ ZMap.get x At = ATValid false ATNorm}.
Proof.
eapply min_ex. intros.
destruct (ZMap.get n At).
- destruct b.
+ right. red; intros. inv H.
+ destruct t.
× right. red; intros. inv H.
× right. red; intros. inv H.
× left. eauto.
- right. red; intros. inv H.
Defined.
End AT_Property.
Inductive LATOwner :=
| LATO (n pdi pti: Z).
Inductive LATCInfo :=
| LATCValid (l: list LATOwner)
| LATCUndef.
Remark LATOwner_dec:
∀ x y: LATOwner,
{x = y} + {x ≠ y}.
Proof.
intros. repeat progress (decide equality).
Qed.
Definition LATCTable := ZMap.t LATCInfo.
Section LAT_Property.
Inductive relate_LATCInfo : ATCInfo → LATCInfo → Prop :=
| RELATE_Undef: relate_LATCInfo ATCUndef LATCUndef
| RELATE_VALID:
∀ n l,
n = Z_of_nat (length l) →
relate_LATCInfo (ATCValid n) (LATCValid l).
Definition relate_LATCTable (a1 : ATCTable) (a2 : LATCTable) :=
∀ i, relate_LATCInfo (ZMap.get i a1) (ZMap.get i a2).
Lemma relate_LATable_gss:
∀ a1 a2,
relate_LATCTable a1 a2 →
∀ s1 s2,
relate_LATCInfo s1 s2 →
∀ i,
relate_LATCTable (ZMap.set i s1 a1) (ZMap.set i s2 a2).
Proof.
unfold relate_LATCTable; intros.
destruct (zeq i i0); subst.
- repeat rewrite ZMap.gss. trivial.
- repeat rewrite ZMap.gso; auto.
Qed.
Definition LATCTable_nil (lat: LATCTable) (a: ATable):=
∀ i l, ZMap.get i a = ATValid false ATNorm →
ZMap.get i lat = LATCValid l →
l = nil.
Section LATABLE_NIL.
Lemma LATCTable_nil_int:
LATCTable_nil (ZMap.init LATCUndef) (ZMap.init ATUndef).
Proof.
intros i. intros.
repeat rewrite ZMap.gi in ×. inv H.
Qed.
Lemma LATCTable_nil_gss_nil:
∀ la n a,
LATCTable_nil la a→
LATCTable_nil (ZMap.set n (LATCValid nil) la) a.
Proof.
unfold LATCTable_nil; intros.
destruct (zeq i n); subst.
- rewrite ZMap.gss in H1. inv H1. trivial.
- rewrite ZMap.gso in H1; eauto.
Qed.
Lemma LATCTable_nil_gso_true:
∀ la n l a t,
LATCTable_nil la a →
LATCTable_nil (ZMap.set n (LATCValid l) la) (ZMap.set n (ATValid true t) a).
Proof.
unfold LATCTable_nil; intros.
destruct (zeq i n); subst.
- rewrite ZMap.gss in ×. inv H0.
- rewrite ZMap.gso in *; eauto.
Qed.
End LATABLE_NIL.
End LAT_Property.
{n| 0 < n < size ∧ ZMap.get n At = ATValid false ATNorm ∧
(∀ x, 0 < x < n → ¬ ZMap.get x At = ATValid false ATNorm)}
+ {∀ x, 0 < x < size → ¬ ZMap.get x At = ATValid false ATNorm}.
Proof.
eapply min_ex. intros.
destruct (ZMap.get n At).
- destruct b.
+ right. red; intros. inv H.
+ destruct t.
× right. red; intros. inv H.
× right. red; intros. inv H.
× left. eauto.
- right. red; intros. inv H.
Defined.
End AT_Property.
Inductive LATOwner :=
| LATO (n pdi pti: Z).
Inductive LATCInfo :=
| LATCValid (l: list LATOwner)
| LATCUndef.
Remark LATOwner_dec:
∀ x y: LATOwner,
{x = y} + {x ≠ y}.
Proof.
intros. repeat progress (decide equality).
Qed.
Definition LATCTable := ZMap.t LATCInfo.
Section LAT_Property.
Inductive relate_LATCInfo : ATCInfo → LATCInfo → Prop :=
| RELATE_Undef: relate_LATCInfo ATCUndef LATCUndef
| RELATE_VALID:
∀ n l,
n = Z_of_nat (length l) →
relate_LATCInfo (ATCValid n) (LATCValid l).
Definition relate_LATCTable (a1 : ATCTable) (a2 : LATCTable) :=
∀ i, relate_LATCInfo (ZMap.get i a1) (ZMap.get i a2).
Lemma relate_LATable_gss:
∀ a1 a2,
relate_LATCTable a1 a2 →
∀ s1 s2,
relate_LATCInfo s1 s2 →
∀ i,
relate_LATCTable (ZMap.set i s1 a1) (ZMap.set i s2 a2).
Proof.
unfold relate_LATCTable; intros.
destruct (zeq i i0); subst.
- repeat rewrite ZMap.gss. trivial.
- repeat rewrite ZMap.gso; auto.
Qed.
Definition LATCTable_nil (lat: LATCTable) (a: ATable):=
∀ i l, ZMap.get i a = ATValid false ATNorm →
ZMap.get i lat = LATCValid l →
l = nil.
Section LATABLE_NIL.
Lemma LATCTable_nil_int:
LATCTable_nil (ZMap.init LATCUndef) (ZMap.init ATUndef).
Proof.
intros i. intros.
repeat rewrite ZMap.gi in ×. inv H.
Qed.
Lemma LATCTable_nil_gss_nil:
∀ la n a,
LATCTable_nil la a→
LATCTable_nil (ZMap.set n (LATCValid nil) la) a.
Proof.
unfold LATCTable_nil; intros.
destruct (zeq i n); subst.
- rewrite ZMap.gss in H1. inv H1. trivial.
- rewrite ZMap.gso in H1; eauto.
Qed.
Lemma LATCTable_nil_gso_true:
∀ la n l a t,
LATCTable_nil la a →
LATCTable_nil (ZMap.set n (LATCValid l) la) (ZMap.set n (ATValid true t) a).
Proof.
unfold LATCTable_nil; intros.
destruct (zeq i n); subst.
- rewrite ZMap.gss in ×. inv H0.
- rewrite ZMap.gso in *; eauto.
Qed.
End LATABLE_NIL.
End LAT_Property.
Physical Page Info
Pg Onwership
Inductive PPgOnwer :=
| PGPMap (n i: Z).
Inductive PPgInfo :=
| PGUndef
| PGAlloc
| PGHide (o: PPgOnwer).
Definition PPermT := ZMap.t PPgInfo.
Section PPgInfo_Property.
Inductive PPgInfo_leq: PPgInfo → PPgInfo → Prop :=
| PGLE_REFL: ∀ i, PPgInfo_leq i i
| PGLE_ALLOC_BUSY: ∀ o, PPgInfo_leq (PGHide o) (PGAlloc )
.
Definition PPermT_les (c1 c2: PPermT) :=
∀ i, PPgInfo_leq (ZMap.get i c1) (ZMap.get i c2).
Definition consistent_ppage (att: ATable) (ppt: PPermT) (nps: Z): Prop :=
∀ i,
0≤ i < nps →
(¬ (ZMap.get i ppt = PGUndef)
→
ZMap.get i att = ATValid true ATNorm)
∧ (ZMap.get i att = ATValid true ATNorm
→ ¬ (ZMap.get i ppt = PGUndef)).
Lemma consistent_ppage_init:
∀ nps,
consistent_ppage (ZMap.init ATUndef) (ZMap.init PGUndef) nps.
Proof.
split; repeat rewrite ZMap.gi; intros.
- elim H0. reflexivity.
- discriminate.
Qed.
Remark PPgOwner_dec (o o1: PPgOnwer):
{ o = o1 } + {¬ o = o1 }.
Proof.
decide equality; apply zeq.
Qed.
Remark PPgInfo_dec (pperm pperm1: PPgInfo):
{pperm = pperm1} + {¬ pperm = pperm1}.
Proof.
decide equality.
eapply PPgOwner_dec.
Qed.
End PPgInfo_Property.
Inductive PTPerm: Type :=
| PTP
| PTU
| PTK (b: bool).
Function ZtoPerm (i:Z): option PTPerm:=
match i with
| PT_PERM_P ⇒ Some PTP
| PT_PERM_PTKF ⇒ Some (PTK false)
| PT_PERM_PTKT ⇒ Some (PTK true)
| PT_PERM_PTU ⇒ Some PTU
| _ ⇒ None
end.
Function PermtoZ (p: PTPerm): Z :=
match p with
| PTP ⇒ PT_PERM_P
| PTU ⇒ PT_PERM_PTU
| PTK false ⇒ PT_PERM_PTKF
| PTK true ⇒ PT_PERM_PTKT
end.
Lemma PermZ_eq:
∀ v p, ZtoPerm v = Some p → v = PermtoZ p.
Proof.
functional inversion 1; trivial.
Qed.
Lemma PermZ_eq_r: ∀ p, ZtoPerm (PermtoZ p) = Some p.
Proof.
intros.
destruct p; trivial.
destruct b; trivial.
Qed.
Lemma ZtoPerm_range: ∀ i p, ZtoPerm (i) = Some p → 0≤ i < 260.
Proof.
functional inversion 1; omega.
Qed.
| PGPMap (n i: Z).
Inductive PPgInfo :=
| PGUndef
| PGAlloc
| PGHide (o: PPgOnwer).
Definition PPermT := ZMap.t PPgInfo.
Section PPgInfo_Property.
Inductive PPgInfo_leq: PPgInfo → PPgInfo → Prop :=
| PGLE_REFL: ∀ i, PPgInfo_leq i i
| PGLE_ALLOC_BUSY: ∀ o, PPgInfo_leq (PGHide o) (PGAlloc )
.
Definition PPermT_les (c1 c2: PPermT) :=
∀ i, PPgInfo_leq (ZMap.get i c1) (ZMap.get i c2).
Definition consistent_ppage (att: ATable) (ppt: PPermT) (nps: Z): Prop :=
∀ i,
0≤ i < nps →
(¬ (ZMap.get i ppt = PGUndef)
→
ZMap.get i att = ATValid true ATNorm)
∧ (ZMap.get i att = ATValid true ATNorm
→ ¬ (ZMap.get i ppt = PGUndef)).
Lemma consistent_ppage_init:
∀ nps,
consistent_ppage (ZMap.init ATUndef) (ZMap.init PGUndef) nps.
Proof.
split; repeat rewrite ZMap.gi; intros.
- elim H0. reflexivity.
- discriminate.
Qed.
Remark PPgOwner_dec (o o1: PPgOnwer):
{ o = o1 } + {¬ o = o1 }.
Proof.
decide equality; apply zeq.
Qed.
Remark PPgInfo_dec (pperm pperm1: PPgInfo):
{pperm = pperm1} + {¬ pperm = pperm1}.
Proof.
decide equality.
eapply PPgOwner_dec.
Qed.
End PPgInfo_Property.
Inductive PTPerm: Type :=
| PTP
| PTU
| PTK (b: bool).
Function ZtoPerm (i:Z): option PTPerm:=
match i with
| PT_PERM_P ⇒ Some PTP
| PT_PERM_PTKF ⇒ Some (PTK false)
| PT_PERM_PTKT ⇒ Some (PTK true)
| PT_PERM_PTU ⇒ Some PTU
| _ ⇒ None
end.
Function PermtoZ (p: PTPerm): Z :=
match p with
| PTP ⇒ PT_PERM_P
| PTU ⇒ PT_PERM_PTU
| PTK false ⇒ PT_PERM_PTKF
| PTK true ⇒ PT_PERM_PTKT
end.
Lemma PermZ_eq:
∀ v p, ZtoPerm v = Some p → v = PermtoZ p.
Proof.
functional inversion 1; trivial.
Qed.
Lemma PermZ_eq_r: ∀ p, ZtoPerm (PermtoZ p) = Some p.
Proof.
intros.
destruct p; trivial.
destruct b; trivial.
Qed.
Lemma ZtoPerm_range: ∀ i p, ZtoPerm (i) = Some p → 0≤ i < 260.
Proof.
functional inversion 1; omega.
Qed.
Page Table
Inductive PTEInfo:=
| PTEValid (v: Z) (p: PTPerm)
| PTEUnPresent
| PTEUndef.
Definition PTE := ZMap.t PTEInfo.
Inductive PDE :=
| PDEValid (pi: Z) (pte: PTE)
| PDEID
| PDEUnPresent
| PDEUndef.
Inductive IDPTEInfo:=
| IDPTEValid (p: PTPerm)
| IDPTEUndef.
Definition IDPTE := ZMap.t IDPTEInfo.
Definition IDPDE := ZMap.t IDPTE.
Definition PMap := ZMap.t PDE.
Section PT_Property.
Definition PDE_kern (pmap: PMap) (i: Z):=
ZMap.get (PDX (i × PgSize)) pmap = PDEID.
Definition PDE_kern_range (pmap: PMap) (lo high: Z) :=
∀ i , lo ≤ i < high → PDE_kern pmap i.
Definition PMap_common (pmap: PMap) :=
∀ i, 0≤ i < kern_low ∨ kern_high ≤ i < maxpage
→ PDE_kern pmap i.
Definition PMap_kern (pmap: PMap) :=
∀ i, kern_low ≤ i < kern_high
→ PDE_kern pmap i.
Remark PDE_kern_dec:
∀ pt i, {PDE_kern pt i} + {¬ PDE_kern pt i}.
Proof.
intros; unfold PDE_kern.
destruct (ZMap.get (PDX (i × PgSize)) pt) eqn: HPDX.
+ right; red; intros. discriminate.
+ left; trivial.
+ right; red; intros. discriminate.
+ right; red; intros. discriminate.
Qed.
Remark PDE_kern_range_dec:
∀ pt lo high, {PDE_kern_range pt lo high} + {¬PDE_kern_range pt lo high}.
Proof.
intros. unfold PDE_kern_range.
eapply general_range_dec. intros.
apply PDE_kern_dec.
Qed.
Remark PMap_common_dec:
∀ pt, {PMap_common pt } + { ¬ PMap_common pt}.
Proof.
intros; unfold PMap_common.
destruct (PDE_kern_range_dec pt 0 kern_low).
+ destruct (PDE_kern_range_dec pt kern_high maxpage).
× left; unfold PDE_kern_range in *; intros.
destruct H; auto.
× right; red; intros.
unfold PDE_kern_range in *; auto.
+ right; red; intros.
apply n; unfold PDE_kern_range; auto.
Qed.
Remark PMap_kern_dec:
∀ pt, {PMap_kern pt } + { ¬ PMap_kern pt}.
Proof.
intros. apply (PDE_kern_range_dec pt kern_low kern_high).
Qed.
Definition PDE_usr (pmap: PMap) (i: Z):=
ZMap.get (PDX (i × PgSize)) pmap = PDEUnPresent
∨ ZMap.get (PDX (i × PgSize)) pmap = PDEID
∨ (∃ pte pi, ZMap.get (PDX (i × PgSize)) pmap = PDEValid pi pte
∧ ¬ (ZMap.get (PTX (i × PgSize)) pte = PTEUndef)).
Definition PDE_usr_range (pmap: PMap) (lo high: Z) :=
∀ i , lo ≤ i < high → PDE_usr pmap i.
Definition PMap_usr (pmap: PMap) :=
∀ i, kern_low ≤ i < kern_high
→ PDE_usr pmap i.
Remark PDE_usr_dec:
∀ pt i, {PDE_usr pt i} + {¬ PDE_usr pt i}.
Proof.
intros; unfold PDE_usr.
destruct (ZMap.get (PDX (i × PgSize)) pt) eqn: HPDX.
- destruct (ZMap.get (PTX (i × 4096)) pte) eqn: HPTX.
+ left; intros. right. right.
esplit; esplit. split; trivial.
rewrite HPTX. red; intros HF; inv HF.
+ left; intros. right. right.
esplit; esplit. split; trivial.
rewrite HPTX. red; intros HF; inv HF.
+ right; red; intros. destruct H.
× discriminate.
× destruct H; try discriminate.
destruct H as (? & ? & HW & HF).
inv HW. elim HF; assumption.
- left. right. left. reflexivity.
- left. left. reflexivity.
- right; red; intros. destruct H.
+ discriminate.
+ destruct H; try discriminate.
destruct H as (? & ? & HW & HF). inv HW.
Qed.
Remark PDE_usr_range_dec:
∀ pt lo high, {PDE_usr_range pt lo high} + {¬PDE_usr_range pt lo high}.
Proof.
intros. unfold PDE_usr_range.
eapply general_range_dec. intros.
apply PDE_usr_dec.
Qed.
Remark PMap_usr_dec:
∀ pt, {PMap_usr pt } + { ¬ PMap_usr pt}.
Proof.
intros; unfold PMap_usr.
destruct (PDE_usr_range_dec pt kern_low kern_high ).
- left; unfold PDE_usr_range in *; intros. eauto.
- right; red; intros.
apply n; unfold PDE_usr_range; auto.
Qed.
Definition PMap_valid (pmap: PMap) :=
PMap_common pmap ∧ PMap_usr pmap.
Remark PMap_valid_dec:
∀ pt, {PMap_valid pt } + { ¬ PMap_valid pt}.
Proof.
intros; unfold PMap_valid.
destruct (PMap_common_dec pt).
destruct (PMap_usr_dec pt).
- left. eauto.
- right; red; intros.
apply n. apply H.
- right; red; intros.
apply n. apply H.
Qed.
End PT_Property.
Function pt_Arg´ (n vadr: Z) : bool :=
if zlt_lt 0 n num_proc then
if zle_lt adr_low vadr adr_high then
true
else false
else false.
Function pt_Arg (n vadr padr np: Z) : bool :=
if pt_Arg´ n vadr then
if zlt_lt 0 padr np then
true
else false
else false.
Section IDPMap_Property.
Definition IDPTE_valid (pte: IDPTE) (i: Z) (b: bool):=
ZMap.get i pte = IDPTEValid (PTK b).
Definition IDPTE_valid_range (pte: IDPTE) (lo high: Z) (b: bool):=
∀ i , lo ≤ i < high → IDPTE_valid pte i b.
Definition IDPTE_valid_page (pte: IDPTE) (b: bool):=
∀ i , 0 ≤ i < one_k → IDPTE_valid pte i b.
Definition IDPDE_range (pde: IDPDE) (lo high: Z) (b: bool):=
∀ i , lo ≤ i < high → IDPTE_valid_page (ZMap.get (PDX (i × PgSize)) pde) b.
Definition IDPDE_common (pde: IDPDE) :=
∀ i, 0≤ i < kern_low ∨ kern_high ≤ i < maxpage
→ IDPTE_valid_page (ZMap.get (PDX (i × PgSize)) pde) true.
Definition IDPDE_kern (pde: IDPDE) :=
∀ i, kern_low ≤ i < kern_high
→ IDPTE_valid_page (ZMap.get (PDX (i × PgSize)) pde) false.
Definition IDPDE_init (pde: IDPDE) :=
IDPDE_common pde ∧ IDPDE_kern pde.
Remark IDPTE_valid_dec:
∀ pte i b, {IDPTE_valid pte i b} + {¬ IDPTE_valid pte i b}.
Proof.
intros; unfold IDPTE_valid.
repeat (decide equality).
Qed.
Remark IDPTE_valid_range_dec:
∀ pte lo high b, {IDPTE_valid_range pte lo high b} + {¬ IDPTE_valid_range pte lo high b}.
Proof.
intros. unfold IDPTE_valid_range.
eapply general_range_dec. intros.
apply IDPTE_valid_dec.
Qed.
Remark IDPTE_valid_page_dec:
∀ pte b, {IDPTE_valid_page pte b} + {¬ IDPTE_valid_page pte b}.
Proof.
intros. eapply IDPTE_valid_range_dec.
Qed.
Remark IDPDE_range_dec:
∀ pde lo high b, {IDPDE_range pde lo high b} + {¬ IDPDE_range pde lo high b}.
Proof.
intros. unfold IDPDE_range.
eapply general_range_dec. intros.
apply IDPTE_valid_page_dec.
Qed.
Remark IDPDE_common_dec:
∀ pde, {IDPDE_common pde } + { ¬ IDPDE_common pde}.
Proof.
intros; unfold IDPDE_common.
destruct (IDPDE_range_dec pde 0 kern_low true).
destruct (IDPDE_range_dec pde kern_high maxpage true).
- left; unfold IDPDE_range in *; intros.
destruct H; auto.
- right; red; intros.
unfold IDPDE_range in *; auto.
- right; red; intros.
apply n; unfold IDPDE_range; auto.
Qed.
Remark IDPDE_kern_dec:
∀ pde, {IDPDE_kern pde } + { ¬ IDPDE_kern pde}.
Proof.
intros. apply IDPDE_range_dec.
Qed.
Remark IDPDE_init_dec:
∀ pde, {IDPDE_init pde } + { ¬ IDPDE_init pde}.
Proof.
intros.
destruct (IDPDE_common_dec pde).
destruct (IDPDE_kern_dec pde).
- left; split; assumption.
- right; red; intros; elim n. apply H.
- right; red; intros; elim n. apply H.
Qed.
End IDPMap_Property.
Definition PMapPool := ZMap.t PMap.
Section PTP_Property.
Definition consistent_pmap (ptp: PMapPool) (ppt: PPermT) (At: ATable) (lat: LATCTable) (nps: Z): Prop :=
∀ i,
0 ≤ i < num_proc →
∀ j,
0≤ j < adr_max →
∀ pte pi,
ZMap.get (PDX j) (ZMap.get i ptp) = PDEValid pi pte →
0 < pi < nps
∧ ZMap.get pi ppt = PGHide (PGPMap i (PDX j))
∧ ZMap.get pi At = ATValid true ATNorm
∧ ZMap.get pi lat = LATCValid nil.
Lemma consistent_pmap_init:
∀ pg a la nps,
consistent_pmap (ZMap.init (ZMap.init PDEUndef)) pg a la nps.
Proof.
unfold consistent_pmap.
intros. repeat rewrite ZMap.gi in H1. inv H1.
Qed.
Definition consistent_pmap_domain (ptp: PMapPool) (ppt: PPermT) (lat: LATCTable) (nps: Z): Prop :=
∀ i,
0 ≤ i < num_proc →
∀ j,
0≤ j < adr_max →
∀ pte pi,
ZMap.get (PDX j) (ZMap.get i ptp) = PDEValid pi pte →
∀ v p,
ZMap.get (PTX j) pte = PTEValid v p →
0 < v < nps
∧ ZMap.get v ppt = PGAlloc
∧ ∃ l, ZMap.get v lat = LATCValid l
∧ count_occ LATOwner_dec l (LATO i (PDX j) (PTX j)) = 1%nat.
Lemma consistent_pmap_domain_init:
∀ pg la nps,
consistent_pmap_domain (ZMap.init (ZMap.init PDEUndef)) pg la nps.
Proof.
unfold consistent_pmap_domain.
intros. repeat rewrite ZMap.gi in H1. inv H1.
Qed.
Definition consistent_at_lat (At: ATable) (lat: LATCTable) (nps: Z): Prop :=
∀ v,
0 < v < nps →
∀ l,
ZMap.get v lat = LATCValid l →
l ≠ nil →
ZMap.get v At = ATValid true ATNorm.
Lemma consistent_at_lat_init:
∀ a nps,
consistent_at_lat a (ZMap.init LATCUndef) nps.
Proof.
unfold consistent_at_lat.
intros. repeat rewrite ZMap.gi in H0. inv H0.
Qed.
Definition consistent_lat_domain (ptp: PMapPool) (lat: LATCTable) (nps: Z): Prop :=
∀ v,
0 < v < nps →
∀ l,
ZMap.get v lat = LATCValid l →
∀ n pdi pti,
In (LATO n pdi pti) l →
0 ≤ pti ≤ PTX (Int.max_unsigned)
∧ ∃ pi pte,
ZMap.get pdi (ZMap.get n ptp) = PDEValid pi pte
∧ ∃ p,
ZMap.get pti pte = PTEValid v p.
Lemma consistent_lat_domain_init:
∀ ptp nps,
consistent_lat_domain ptp (ZMap.init LATCUndef) nps.
Proof.
unfold consistent_lat_domain.
intros. repeat rewrite ZMap.gi in H0. inv H0.
Qed.
Definition PDE_unp (pmap: PMap) (i: Z) :=
ZMap.get (PDX (i × PgSize)) pmap = PDEUnPresent.
Definition PDE_unp_range (pmap: PMap) (lo high: Z) :=
∀ i , lo ≤ i < high → PDE_unp pmap i.
Definition PMap_init (pmap: PMap) :=
PMap_common pmap
∧ PDE_unp_range pmap kern_low kern_high.
Lemma PMap_init_common_usr:
∀ pmap,
PMap_init pmap → PMap_valid pmap.
Proof.
unfold PMap_valid, PMap_init, PMap_usr, PDE_unp_range. intros.
destruct H as [HT1 HT2].
split; [assumption|].
intros. exploit HT2; eauto.
unfold PDE_unp, PDE_usr.
left; assumption.
Qed.
End PTP_Property.
| PTEValid (v: Z) (p: PTPerm)
| PTEUnPresent
| PTEUndef.
Definition PTE := ZMap.t PTEInfo.
Inductive PDE :=
| PDEValid (pi: Z) (pte: PTE)
| PDEID
| PDEUnPresent
| PDEUndef.
Inductive IDPTEInfo:=
| IDPTEValid (p: PTPerm)
| IDPTEUndef.
Definition IDPTE := ZMap.t IDPTEInfo.
Definition IDPDE := ZMap.t IDPTE.
Definition PMap := ZMap.t PDE.
Section PT_Property.
Definition PDE_kern (pmap: PMap) (i: Z):=
ZMap.get (PDX (i × PgSize)) pmap = PDEID.
Definition PDE_kern_range (pmap: PMap) (lo high: Z) :=
∀ i , lo ≤ i < high → PDE_kern pmap i.
Definition PMap_common (pmap: PMap) :=
∀ i, 0≤ i < kern_low ∨ kern_high ≤ i < maxpage
→ PDE_kern pmap i.
Definition PMap_kern (pmap: PMap) :=
∀ i, kern_low ≤ i < kern_high
→ PDE_kern pmap i.
Remark PDE_kern_dec:
∀ pt i, {PDE_kern pt i} + {¬ PDE_kern pt i}.
Proof.
intros; unfold PDE_kern.
destruct (ZMap.get (PDX (i × PgSize)) pt) eqn: HPDX.
+ right; red; intros. discriminate.
+ left; trivial.
+ right; red; intros. discriminate.
+ right; red; intros. discriminate.
Qed.
Remark PDE_kern_range_dec:
∀ pt lo high, {PDE_kern_range pt lo high} + {¬PDE_kern_range pt lo high}.
Proof.
intros. unfold PDE_kern_range.
eapply general_range_dec. intros.
apply PDE_kern_dec.
Qed.
Remark PMap_common_dec:
∀ pt, {PMap_common pt } + { ¬ PMap_common pt}.
Proof.
intros; unfold PMap_common.
destruct (PDE_kern_range_dec pt 0 kern_low).
+ destruct (PDE_kern_range_dec pt kern_high maxpage).
× left; unfold PDE_kern_range in *; intros.
destruct H; auto.
× right; red; intros.
unfold PDE_kern_range in *; auto.
+ right; red; intros.
apply n; unfold PDE_kern_range; auto.
Qed.
Remark PMap_kern_dec:
∀ pt, {PMap_kern pt } + { ¬ PMap_kern pt}.
Proof.
intros. apply (PDE_kern_range_dec pt kern_low kern_high).
Qed.
Definition PDE_usr (pmap: PMap) (i: Z):=
ZMap.get (PDX (i × PgSize)) pmap = PDEUnPresent
∨ ZMap.get (PDX (i × PgSize)) pmap = PDEID
∨ (∃ pte pi, ZMap.get (PDX (i × PgSize)) pmap = PDEValid pi pte
∧ ¬ (ZMap.get (PTX (i × PgSize)) pte = PTEUndef)).
Definition PDE_usr_range (pmap: PMap) (lo high: Z) :=
∀ i , lo ≤ i < high → PDE_usr pmap i.
Definition PMap_usr (pmap: PMap) :=
∀ i, kern_low ≤ i < kern_high
→ PDE_usr pmap i.
Remark PDE_usr_dec:
∀ pt i, {PDE_usr pt i} + {¬ PDE_usr pt i}.
Proof.
intros; unfold PDE_usr.
destruct (ZMap.get (PDX (i × PgSize)) pt) eqn: HPDX.
- destruct (ZMap.get (PTX (i × 4096)) pte) eqn: HPTX.
+ left; intros. right. right.
esplit; esplit. split; trivial.
rewrite HPTX. red; intros HF; inv HF.
+ left; intros. right. right.
esplit; esplit. split; trivial.
rewrite HPTX. red; intros HF; inv HF.
+ right; red; intros. destruct H.
× discriminate.
× destruct H; try discriminate.
destruct H as (? & ? & HW & HF).
inv HW. elim HF; assumption.
- left. right. left. reflexivity.
- left. left. reflexivity.
- right; red; intros. destruct H.
+ discriminate.
+ destruct H; try discriminate.
destruct H as (? & ? & HW & HF). inv HW.
Qed.
Remark PDE_usr_range_dec:
∀ pt lo high, {PDE_usr_range pt lo high} + {¬PDE_usr_range pt lo high}.
Proof.
intros. unfold PDE_usr_range.
eapply general_range_dec. intros.
apply PDE_usr_dec.
Qed.
Remark PMap_usr_dec:
∀ pt, {PMap_usr pt } + { ¬ PMap_usr pt}.
Proof.
intros; unfold PMap_usr.
destruct (PDE_usr_range_dec pt kern_low kern_high ).
- left; unfold PDE_usr_range in *; intros. eauto.
- right; red; intros.
apply n; unfold PDE_usr_range; auto.
Qed.
Definition PMap_valid (pmap: PMap) :=
PMap_common pmap ∧ PMap_usr pmap.
Remark PMap_valid_dec:
∀ pt, {PMap_valid pt } + { ¬ PMap_valid pt}.
Proof.
intros; unfold PMap_valid.
destruct (PMap_common_dec pt).
destruct (PMap_usr_dec pt).
- left. eauto.
- right; red; intros.
apply n. apply H.
- right; red; intros.
apply n. apply H.
Qed.
End PT_Property.
Function pt_Arg´ (n vadr: Z) : bool :=
if zlt_lt 0 n num_proc then
if zle_lt adr_low vadr adr_high then
true
else false
else false.
Function pt_Arg (n vadr padr np: Z) : bool :=
if pt_Arg´ n vadr then
if zlt_lt 0 padr np then
true
else false
else false.
Section IDPMap_Property.
Definition IDPTE_valid (pte: IDPTE) (i: Z) (b: bool):=
ZMap.get i pte = IDPTEValid (PTK b).
Definition IDPTE_valid_range (pte: IDPTE) (lo high: Z) (b: bool):=
∀ i , lo ≤ i < high → IDPTE_valid pte i b.
Definition IDPTE_valid_page (pte: IDPTE) (b: bool):=
∀ i , 0 ≤ i < one_k → IDPTE_valid pte i b.
Definition IDPDE_range (pde: IDPDE) (lo high: Z) (b: bool):=
∀ i , lo ≤ i < high → IDPTE_valid_page (ZMap.get (PDX (i × PgSize)) pde) b.
Definition IDPDE_common (pde: IDPDE) :=
∀ i, 0≤ i < kern_low ∨ kern_high ≤ i < maxpage
→ IDPTE_valid_page (ZMap.get (PDX (i × PgSize)) pde) true.
Definition IDPDE_kern (pde: IDPDE) :=
∀ i, kern_low ≤ i < kern_high
→ IDPTE_valid_page (ZMap.get (PDX (i × PgSize)) pde) false.
Definition IDPDE_init (pde: IDPDE) :=
IDPDE_common pde ∧ IDPDE_kern pde.
Remark IDPTE_valid_dec:
∀ pte i b, {IDPTE_valid pte i b} + {¬ IDPTE_valid pte i b}.
Proof.
intros; unfold IDPTE_valid.
repeat (decide equality).
Qed.
Remark IDPTE_valid_range_dec:
∀ pte lo high b, {IDPTE_valid_range pte lo high b} + {¬ IDPTE_valid_range pte lo high b}.
Proof.
intros. unfold IDPTE_valid_range.
eapply general_range_dec. intros.
apply IDPTE_valid_dec.
Qed.
Remark IDPTE_valid_page_dec:
∀ pte b, {IDPTE_valid_page pte b} + {¬ IDPTE_valid_page pte b}.
Proof.
intros. eapply IDPTE_valid_range_dec.
Qed.
Remark IDPDE_range_dec:
∀ pde lo high b, {IDPDE_range pde lo high b} + {¬ IDPDE_range pde lo high b}.
Proof.
intros. unfold IDPDE_range.
eapply general_range_dec. intros.
apply IDPTE_valid_page_dec.
Qed.
Remark IDPDE_common_dec:
∀ pde, {IDPDE_common pde } + { ¬ IDPDE_common pde}.
Proof.
intros; unfold IDPDE_common.
destruct (IDPDE_range_dec pde 0 kern_low true).
destruct (IDPDE_range_dec pde kern_high maxpage true).
- left; unfold IDPDE_range in *; intros.
destruct H; auto.
- right; red; intros.
unfold IDPDE_range in *; auto.
- right; red; intros.
apply n; unfold IDPDE_range; auto.
Qed.
Remark IDPDE_kern_dec:
∀ pde, {IDPDE_kern pde } + { ¬ IDPDE_kern pde}.
Proof.
intros. apply IDPDE_range_dec.
Qed.
Remark IDPDE_init_dec:
∀ pde, {IDPDE_init pde } + { ¬ IDPDE_init pde}.
Proof.
intros.
destruct (IDPDE_common_dec pde).
destruct (IDPDE_kern_dec pde).
- left; split; assumption.
- right; red; intros; elim n. apply H.
- right; red; intros; elim n. apply H.
Qed.
End IDPMap_Property.
Definition PMapPool := ZMap.t PMap.
Section PTP_Property.
Definition consistent_pmap (ptp: PMapPool) (ppt: PPermT) (At: ATable) (lat: LATCTable) (nps: Z): Prop :=
∀ i,
0 ≤ i < num_proc →
∀ j,
0≤ j < adr_max →
∀ pte pi,
ZMap.get (PDX j) (ZMap.get i ptp) = PDEValid pi pte →
0 < pi < nps
∧ ZMap.get pi ppt = PGHide (PGPMap i (PDX j))
∧ ZMap.get pi At = ATValid true ATNorm
∧ ZMap.get pi lat = LATCValid nil.
Lemma consistent_pmap_init:
∀ pg a la nps,
consistent_pmap (ZMap.init (ZMap.init PDEUndef)) pg a la nps.
Proof.
unfold consistent_pmap.
intros. repeat rewrite ZMap.gi in H1. inv H1.
Qed.
Definition consistent_pmap_domain (ptp: PMapPool) (ppt: PPermT) (lat: LATCTable) (nps: Z): Prop :=
∀ i,
0 ≤ i < num_proc →
∀ j,
0≤ j < adr_max →
∀ pte pi,
ZMap.get (PDX j) (ZMap.get i ptp) = PDEValid pi pte →
∀ v p,
ZMap.get (PTX j) pte = PTEValid v p →
0 < v < nps
∧ ZMap.get v ppt = PGAlloc
∧ ∃ l, ZMap.get v lat = LATCValid l
∧ count_occ LATOwner_dec l (LATO i (PDX j) (PTX j)) = 1%nat.
Lemma consistent_pmap_domain_init:
∀ pg la nps,
consistent_pmap_domain (ZMap.init (ZMap.init PDEUndef)) pg la nps.
Proof.
unfold consistent_pmap_domain.
intros. repeat rewrite ZMap.gi in H1. inv H1.
Qed.
Definition consistent_at_lat (At: ATable) (lat: LATCTable) (nps: Z): Prop :=
∀ v,
0 < v < nps →
∀ l,
ZMap.get v lat = LATCValid l →
l ≠ nil →
ZMap.get v At = ATValid true ATNorm.
Lemma consistent_at_lat_init:
∀ a nps,
consistent_at_lat a (ZMap.init LATCUndef) nps.
Proof.
unfold consistent_at_lat.
intros. repeat rewrite ZMap.gi in H0. inv H0.
Qed.
Definition consistent_lat_domain (ptp: PMapPool) (lat: LATCTable) (nps: Z): Prop :=
∀ v,
0 < v < nps →
∀ l,
ZMap.get v lat = LATCValid l →
∀ n pdi pti,
In (LATO n pdi pti) l →
0 ≤ pti ≤ PTX (Int.max_unsigned)
∧ ∃ pi pte,
ZMap.get pdi (ZMap.get n ptp) = PDEValid pi pte
∧ ∃ p,
ZMap.get pti pte = PTEValid v p.
Lemma consistent_lat_domain_init:
∀ ptp nps,
consistent_lat_domain ptp (ZMap.init LATCUndef) nps.
Proof.
unfold consistent_lat_domain.
intros. repeat rewrite ZMap.gi in H0. inv H0.
Qed.
Definition PDE_unp (pmap: PMap) (i: Z) :=
ZMap.get (PDX (i × PgSize)) pmap = PDEUnPresent.
Definition PDE_unp_range (pmap: PMap) (lo high: Z) :=
∀ i , lo ≤ i < high → PDE_unp pmap i.
Definition PMap_init (pmap: PMap) :=
PMap_common pmap
∧ PDE_unp_range pmap kern_low kern_high.
Lemma PMap_init_common_usr:
∀ pmap,
PMap_init pmap → PMap_valid pmap.
Proof.
unfold PMap_valid, PMap_init, PMap_usr, PDE_unp_range. intros.
destruct H as [HT1 HT2].
split; [assumption|].
intros. exploit HT2; eauto.
unfold PDE_unp, PDE_usr.
left; assumption.
Qed.
End PTP_Property.
page table bit map
Function ZtoBool (i:Z): option bool :=
match i with
| 0 ⇒ Some false
| 1 ⇒ Some true
| _ ⇒ None
end.
Function BooltoZ (b:bool): Z :=
match b with
| true ⇒ 1
| _ ⇒ 0
end.
End MemoryManagement.
Section ProcessManagement.
Definition KContext := regset.
Definition KContextPool := ZMap.t KContext.
Lemma register_type_load:
∀ (rs: regset) r v f,
Val.has_type (rs r) Tint
→ val_inject f (Val.load_result Mint32 (rs r)) v
→ val_inject f (rs r) v.
Proof.
intros.
unfold Val.has_type in ×.
destruct (rs r); inv H; inv H0; try econstructor; eauto.
Qed.
Definition PregtoZ (r: preg) : option Z :=
match r with
| ESP ⇒ Some 0
| EDI ⇒ Some 1
| ESI ⇒ Some 2
| EBX ⇒ Some 3
| EBP ⇒ Some 4
| RA ⇒ Some 5
| _ ⇒ None
end.
Function ZtoPreg (i: Z) : option preg :=
match i with
| 0 ⇒ Some (IR ESP)
| 1 ⇒ Some (IR EDI)
| 2 ⇒ Some (IR ESI)
| 3 ⇒ Some (IR EBX)
| 4 ⇒ Some (IR EBP)
| 5 ⇒ Some RA
| _ ⇒ None
end.
Definition kctxt_inj (f:meminj) (range:Z) (kctxtp kctxtp´: KContextPool) :=
∀ i n r,
0≤ n < range
→ ZtoPreg i = Some r
→ val_inject f (Pregmap.get r (ZMap.get n kctxtp)) (Pregmap.get r (ZMap.get n kctxtp´)).
Definition kctxt_inject_neutral (kp: KContextPool) (n: block) :=
∀ ofs,
0 ≤ ofs < num_proc →
let rs := ZMap.get ofs kp in
∀ v r, ZtoPreg v = Some r →
Val.has_type (rs r) Tint
∧ val_inject (Mem.flat_inj n) (rs r) (rs r).
Lemma PregToZ_correct:
∀ r i, PregtoZ r = Some i → ZtoPreg i = Some r.
Proof.
intros.
induction r; inv H; auto.
induction i0; inv H1; auto.
Qed.
Lemma ZtoPreg_correct:
∀ r i, ZtoPreg i = Some r → PregtoZ r = Some i.
Proof.
functional inversion 1; trivial.
Qed.
Lemma ZtoPreg_range:
∀ n r,
ZtoPreg n = Some r → 0≤ n ≤ 5.
Proof.
functional inversion 1; omega.
Qed.
Lemma ZtoPreg_range_correct:
∀ n,
0≤ n ≤ 5 → ∃ r, ZtoPreg n = Some r.
Proof.
intros.
destruct (zeq n 0). subst; simpl; eauto.
destruct (zeq n 1). subst; simpl; eauto.
destruct (zeq n 2). subst; simpl; eauto.
destruct (zeq n 3). subst; simpl; eauto.
destruct (zeq n 4). subst; simpl; eauto.
destruct (zeq n 5). subst; simpl; eauto.
omega.
Qed.
Lemma ZtoPreg_type:
∀ v r,
ZtoPreg v = Some r → Tint = typ_of_preg r.
Proof.
functional inversion 1; trivial.
Qed.
Definition is_valid_context_reg (v: val) :=
match v with
| Vfloat _ ⇒ false
| _ ⇒ true
end.
Inductive ThreadState :=
| READY
| RUN
| SLEEP
| DEAD
| PENDING.
Remark ThreadState_dec: ∀ ts ts´: ThreadState, {ts = ts´} + {¬ ts = ts´}.
Proof.
intros; decide equality.
Qed.
Function ZtoThreadState (i:Z) :=
match i with
| 0 ⇒ Some READY
| 1 ⇒ Some RUN
| 2 ⇒ Some SLEEP
| 3 ⇒ Some DEAD
| 4 ⇒ Some PENDING
| _ ⇒ None
end.
Definition ThreadStatetoZ (tds: ThreadState) :=
match tds with
| READY ⇒ 0
| RUN ⇒ 1
| SLEEP ⇒ 2
| DEAD ⇒ 3
| PENDING ⇒ 4
end.
Lemma ZtoThreadState_correct:
∀ i tds, ZtoThreadState i = Some tds → ThreadStatetoZ tds = i.
Proof.
functional inversion 1; trivial.
Qed.
Lemma ThreadStatetoZ_correct:
∀ tds, ZtoThreadState (ThreadStatetoZ tds) = Some tds.
Proof.
destruct tds; trivial.
Qed.
Lemma ZtoThreadState_range:
∀ i tds, ZtoThreadState i = Some tds → 0 ≤ i ≤ 4.
Proof.
functional inversion 1; omega.
Qed.
Lemma ZtoThreadState_range_correct:
∀ i, 0≤ i ≤ 4 → ∃ tds, ZtoThreadState i = Some tds.
Proof.
intros.
destruct (zeq i 0). subst; simpl; eauto.
destruct (zeq i 1). subst; simpl; eauto.
destruct (zeq i 2). subst; simpl; eauto.
destruct (zeq i 3). subst; simpl; eauto.
destruct (zeq i 4). subst; simpl; eauto.
omega.
Qed.
Inductive TCB :=
| TCBUndef
| TCBValid (tds: ThreadState) (cpu_id: Z) (prev: Z) (next: Z).
Remark TCB_dec: ∀ tcb tcb´: TCB, {tcb = tcb´} + {¬ tcb = tcb´}.
Proof.
intros.
decide equality; try apply Z_eq_dec.
apply ThreadState_dec.
Qed.
Definition TCBPool := ZMap.t TCB.
Definition TCBCorrect (tcb: TCB) (high:Z) :=
∃ s cpid prev next, tcb = TCBValid s cpid prev next ∧ 0≤ prev ≤ high ∧ 0≤ next ≤ high.
Definition TCBCorrect_range´ (tcb: TCBPool) (lo high num_proc: Z) :=
∀ i , lo ≤ i < high → TCBCorrect (ZMap.get i tcb) num_proc.
Definition TCBCorrect_range (tcb: TCBPool) :=
∀ i , 0 ≤ i < num_proc → TCBCorrect (ZMap.get i tcb) num_proc.
Definition TCBInit´ (tcb: TCBPool) (lo high num_proc: Z) :=
∀ i , lo ≤ i < high → ZMap.get i tcb = TCBValid DEAD 0 num_proc num_proc.
Definition TCBInit (tcb: TCBPool) :=
∀ i , 0 ≤ i < num_proc → ZMap.get i tcb = TCBValid DEAD 0 num_proc num_proc.
Inductive TDQueue :=
| TDQUndef
| TDQValid (head tail: Z).
Definition TDQueuePool := ZMap.t TDQueue.
Definition TDQCorrect (tdq: TDQueue) (high:Z) :=
∃ head tail, tdq = TDQValid head tail ∧ 0≤ head ≤ high ∧ 0≤ tail ≤ high.
Definition TDQCorrect_range (tdq: TDQueuePool) :=
∀ i , 0 ≤ i < num_chan → TDQCorrect (ZMap.get i tdq) num_proc.
Definition TDQInit (tdq: TDQueuePool) :=
∀ i , 0 ≤ i < num_chan → ZMap.get i tdq = TDQValid num_proc num_proc.
Inductive AbQueue :=
| AbQUndef
| AbQValid (l: list Z).
Definition AbQueuePool := ZMap.t AbQueue.
Inductive AbTCB :=
| AbTCBUndef
| AbTCBValid (tds: ThreadState) (cpuid: Z) (inQ: Z).
Definition AbTCBPool := ZMap.t AbTCB.
Function rdy_q_id (cpu: Z): Z := READ_Q_START + cpu.
Function msg_q_id (cpu: Z): Z := MSG_Q_START + cpu.
Function slp_q_id (cv: Z) (curid: Z) : Z := SLEEP_Q_START + cv.
Definition AbTCBCorrect (tcb: AbTCB):=
∃ s c b, tcb = AbTCBValid s c b ∧ (-1 ≤ b < TDQ_SIZE).
Definition AbTCBStrong (tcb: AbTCB):=
∃ s c b, tcb = AbTCBValid s c b ∧ ((s = RUN ∨ s = DEAD) → b = -1)
∧ (s = SLEEP ∨ s = PENDING → 0 ≤ b < num_proc)
∧ (s = READY → b = num_proc).
Definition AbQCorrect (tdq: AbQueue) :=
∃ l, tdq = AbQValid l ∧ (∀ x, In x l → 0 ≤ x < num_proc).
Definition AbTCBInit (tcb: AbTCBPool) :=
∀ i , 0 ≤ i < num_proc → ZMap.get i tcb = AbTCBValid DEAD 0 (-1).
Definition AbQInit (tdq: AbQueuePool) :=
∀ i , 0 ≤ i < num_chan → ZMap.get i tdq = AbQValid nil.
Definition AbTCBCorrect_range t :=
∀ i, 0 ≤ i < num_proc → AbTCBCorrect (ZMap.get i t).
Definition AbTCBStrong_range t:=
∀ i, 0 ≤ i < num_proc →
AbTCBStrong (ZMap.get i t).
Definition AbQCorrect_range q :=
∀ i, 0 ≤ i < num_chan → AbQCorrect (ZMap.get i q).
Definition NotInQ c t :=
∀ i s j b,
0 ≤ i < num_proc
→ cused (ZMap.get i c) = false
→ ZMap.get i t = AbTCBValid s j b
→ b = -1.
Definition QCount t q :=
∀ i s c b,
0 ≤ i < num_proc
→ ZMap.get i t = AbTCBValid s c b
→ 0 ≤ b < num_chan
→ ∃ l,
ZMap.get b q = AbQValid l
∧ count_occ zeq l i = 1%nat.
Definition InQ t q :=
∀ i j l,
0 ≤ i < num_proc
→ 0 ≤ j < num_chan
→ ZMap.get j q = AbQValid l
→ In i l
→ ∃ s c, ZMap.get i t = AbTCBValid s c j.
Definition CurIDValid j i c t :=
cused (ZMap.get i c) = true
∧ (ZMap.get i t = AbTCBValid RUN j (-1)).
Function Queue_arg (n i: Z) :=
if zle_lt 0 n num_chan then
if zle_lt 0 i num_proc then
true
else false
else false.
Section AbTCB_TDQ_Property.
Lemma AbTCBInit_valid:
∀ tcbp,
AbTCBInit tcbp
→ (∀ i, 0 ≤ i < num_proc →
AbTCBCorrect (ZMap.get i tcbp)).
Proof.
unfold AbTCBInit, AbTCBCorrect; intros.
esplit; esplit; esplit. split.
eapply H; eauto. omega.
Qed.
Lemma AbTCBInit_notInQ:
∀ tcbp,
AbTCBInit tcbp →
(∀ i s c b, 0 ≤ i < num_proc →
ZMap.get i tcbp = AbTCBValid s c b →
b = -1).
Proof.
unfold AbTCBInit; intros.
specialize (H _ H0). rewrite H1 in H; inv H. trivial.
Qed.
Lemma AbTDQInit_valid:
∀ tdqp,
AbQInit tdqp
→ (∀ i, 0 ≤ i < num_chan →
AbQCorrect (ZMap.get i tdqp)).
Proof.
unfold AbQInit, AbQCorrect; intros.
esplit. split.
eapply H; eauto. intros. inv H1.
Qed.
End AbTCB_TDQ_Property.
Definition UContext := ZMap.t val.
Definition UContextPool := ZMap.t UContext.
Definition uctxt_inj (f:meminj) (uctxtp uctxtp´: UContextPool) :=
∀ i j,
0≤ i < num_proc →
0≤ j < UCTXT_SIZE →
val_inject f (ZMap.get j (ZMap.get i uctxtp))
(ZMap.get j (ZMap.get i uctxtp´)).
Definition uctxt_inject_neutral (up: UContextPool) (n: block) :=
∀ ii ii´,
0≤ ii < num_proc →
0≤ ii´ < UCTXT_SIZE →
let v:= (ZMap.get ii´ (ZMap.get ii up)) in
Val.has_type v AST.Tint
∧ val_inject (Mem.flat_inj n) v v.
Function is_UCTXT_ptr (ofs : Z): bool :=
match ofs with
| U_EDI ⇒ false
| U_ESI ⇒ false
| U_EBX ⇒ false
| U_EDX ⇒ false
| U_ECX ⇒ false
| U_EAX ⇒ false
| U_ES ⇒ false
| U_DS ⇒ false
| U_ERR ⇒ false
| U_TRAPNO ⇒ false
| U_CS ⇒ false
| U_EFLAGS ⇒ false
| U_ESP ⇒ false
| U_SS ⇒ false
| _ ⇒ true
end.
Lemma is_UCTXT_ptr_range:
∀ i, is_UCTXT_ptr i = false → 0≤ i < UCTXT_SIZE.
Proof.
intros.
functional inversion H; omega.
Qed.
Function UCtxt_Reg (r: preg) : bool :=
match r with
| IR _ ⇒ true
| RA ⇒ true
| _ ⇒ false
end.
Inductive SyncChannel :=
| SyncChanUndef
| SyncChanValid (to senderpaddr count busy: int).
Definition SyncChanPool := ZMap.t SyncChannel.
Definition SyncChannel_Valid (ch: SyncChannel) :=
∃ t p c b, ch = SyncChanValid t p c b.
Definition SyncChanPool_Valid (chp: SyncChanPool) :=
∀ i, 0 ≤ i < num_chan → SyncChannel_Valid (ZMap.get i chp).
Definition SyncChannel_Init (ch: SyncChannel) :=
ch = SyncChanValid (Int.repr num_chan) Int.zero Int.zero Int.zero.
Definition SyncChanPool_Init (chp: SyncChanPool) :=
∀ i, 0 ≤ i < num_chan → SyncChannel_Init (ZMap.get i chp).
Lemma SyncChannel_Init_Correct:
∀ chp,
SyncChanPool_Init chp → SyncChanPool_Valid chp.
Proof.
unfold SyncChanPool_Init, SyncChanPool_Valid.
unfold SyncChannel_Init, SyncChannel_Valid.
intros. erewrite H; eauto.
Qed.
Inductive SharedMemInfo :=
| SHRDREADY | SHRDPEND | SHRDDEAD.
Remark SharedMemInfo_dec:
∀ x y: SharedMemInfo,
{x = y} + {x ≠ y}.
Proof.
intros. repeat progress (decide equality).
Qed.
Inductive SharedMemState :=
| SHRDValid (info: SharedMemInfo) (seen: bool) (vadr: Z)
| SHRDUndef.
Definition SharedMemSTPool :=
ZMap.t (ZMap.t SharedMemState).
Function SharedMemInfo2Z (i: SharedMemInfo) :=
match i with
| SHRDREADY ⇒ SHARED_MEM_READY
| SHRDPEND ⇒ SHARED_MEM_PEND
| SHRDDEAD ⇒ SHARED_MEM_DEAD
end.
Function Z2SharedMemInfo (i: Z) :=
match i with
| SHARED_MEM_READY ⇒ Some SHRDREADY
| SHARED_MEM_PEND ⇒ Some SHRDPEND
| SHARED_MEM_DEAD ⇒ Some SHRDDEAD
| _ ⇒ None
end.
Lemma Z2SharedMemInfo_correct:
∀ st i,
Z2SharedMemInfo st = Some i →
SharedMemInfo2Z i = st.
Proof.
functional inversion 1; reflexivity.
Qed.
Lemma SharedMemInfo2Z_correct:
∀ st i,
SharedMemInfo2Z i = st →
Z2SharedMemInfo st = Some i.
Proof.
functional inversion 1; reflexivity.
Qed.
Lemma SharedMemInfo2Z_range:
∀ st i,
SharedMemInfo2Z i = st →
SHARED_MEM_READY ≤ st ≤ SHARED_MEM_DEAD.
Proof.
functional inversion 1; omega.
Qed.
Definition SharedMemST_Valid (st: SharedMemState) :=
∃ i s vadr, st = SHRDValid i s vadr.
Definition SharedMemSTPool_Init (smsp: SharedMemSTPool) :=
∀ i,
0 ≤ i < num_proc →
∀ j, 0 ≤ j < num_proc →
SharedMemST_Valid (ZMap.get j (ZMap.get i smsp)).
End ProcessManagement.
Section VirtManagement.
Inductive NPTPerm :=
| ALL_PERM.
Definition NPTPerm2Z (perm : NPTPerm) : Z :=
match perm with
| ALL_PERM ⇒ 39
end.
Inductive NPTE:=
| NPTEValid (hpa: Z)
| NPTEUndef.
Definition NPTab := ZMap.t NPTE.
Inductive NPDE :=
| NPDEValid (nptab : NPTab)
| NPDEUndef.
Definition NPT := ZMap.t NPDE.
Definition NPDE_valid (npt: NPT) (i:Z) :=
∃ npte, ZMap.get (PDX i) npt = NPDEValid npte.
Definition NPT_valid (npt: NPT) (lo high: Z):=
∀ i , lo ≤ i < high → NPDE_valid npt i.
Definition PregtoZ_Host (r: preg) : option Z :=
match r with
| ECX ⇒ Some 0
| EDI ⇒ Some 1
| ESI ⇒ Some 2
| EBX ⇒ Some 3
| EBP ⇒ Some 4
| EDX ⇒ Some 5
| ESP ⇒ Some 6
| RA ⇒ Some 7
| _ ⇒ None
end.
Function ZtoPreg_Host (i: Z) : option preg :=
match i with
| 0 ⇒ Some (IR ECX)
| 1 ⇒ Some (IR EDI)
| 2 ⇒ Some (IR ESI)
| 3 ⇒ Some (IR EBX)
| 4 ⇒ Some (IR EBP)
| 5 ⇒ Some (IR EDX)
| 6 ⇒ Some (IR ESP)
| 7 ⇒ Some RA
| _ ⇒ None
end.
Lemma PregToZ_Host_correct:
∀ r i, PregtoZ_Host r = Some i → ZtoPreg_Host i = Some r.
Proof.
intros. destruct r; inv H.
destruct i0; inv H1; reflexivity.
reflexivity.
Qed.
Lemma ZtoPreg_Host_correct:
∀ r i, ZtoPreg_Host i = Some r → PregtoZ_Host r = Some i.
Proof.
intros. functional inversion H; reflexivity.
Qed.
Lemma ZtoPreg_Host_range:
∀ n r,
ZtoPreg_Host n = Some r → 0≤ n ≤ 7.
Proof.
intros. functional inversion H; omega.
Qed.
Lemma ZtoPreg_range_Host_correct:
∀ n,
0≤ n ≤ 7 → ∃ r, ZtoPreg_Host n = Some r.
Proof.
intros.
destruct (zeq n 0); subst. simpl; eauto.
destruct (zeq n 1); subst. simpl; eauto.
destruct (zeq n 2); subst. simpl; eauto.
destruct (zeq n 3); subst. simpl; eauto.
destruct (zeq n 4); subst. simpl; eauto.
destruct (zeq n 5); subst. simpl; eauto.
destruct (zeq n 6); subst. simpl; eauto.
destruct (zeq n 7); subst. simpl; eauto.
omega.
Qed.
Lemma ZtoPreg_Host_type:
∀ n r,
ZtoPreg_Host n = Some r →
typ_of_preg r = Tint.
Proof.
intros. functional inversion H; reflexivity.
Qed.
Definition hctx_inj (f:meminj)(hctxt hctxt´: regset) :=
∀ i r,
ZtoPreg_Host i = Some r
→ val_inject f (Pregmap.get r hctxt) (Pregmap.get r hctxt´).
Definition addr_valid (addr : Z) :=
if zle_le 0 addr (Int.max_unsigned + 1 - PgSize) then
if Zdivide_dec PgSize addr HPS then
true
else
false
else
false.
Function is_VMCB_Z_ofs (v:Z) : bool :=
if zle_lt 0 v 16 then
true
else
if zle_lt 18 v 44 then
true
else
if zle_lt 46 v 338 then
true
else
if zle_lt 344 v 348 then
true
else
if zle_lt 352 v 374 then
true
else
if zle_lt 376 v 382 then
true
else
if zle_lt 384 v 400 then
true
else
if zle_lt 402 v 1024 then
true
else
false.
Lemma VMCB_Z_ofs_range:
∀ v, is_VMCB_Z_ofs v = true → 0 ≤ v ≤ 1023.
Proof.
intros.
functional inversion H; omega.
Qed.
Function is_VMCB_V_ofs (v:Z) : bool :=
match v with
| VMCB_V_CR4_LO_OFFSET ⇒ true
| VMCB_V_CR3_LO_OFFSET ⇒ true
| VMCB_V_CR0_LO_OFFSET ⇒ true
| VMCB_V_RFLAGS_LO_OFFSET ⇒ true
| VMCB_V_RIP_LO_OFFSET ⇒ true
| VMCB_V_RSP_LO_OFFSET ⇒ true
| VMCB_V_RAX_LO_OFFSET ⇒ true
| VMCB_V_CR2_LO_OFFSET ⇒ true
| _ ⇒ false
end.
Lemma VMCB_V_ofs_range:
∀ v, is_VMCB_V_ofs v = true → VMCB_V_CR4_LO_OFFSET ≤ v ≤ VMCB_V_CR2_LO_OFFSET.
Proof.
intros.
functional inversion H; omega.
Qed.
Lemma VMCB_V_ofs_correct:
∀ v, is_VMCB_V_ofs v = true → is_VMCB_Z_ofs v = false.
Proof.
intros.
functional inversion H; trivial.
Qed.
Lemma VMCB_Z_ofs_correct:
∀ v, is_VMCB_Z_ofs v = true → is_VMCB_V_ofs v = false.
Proof.
intros.
functional induction (is_VMCB_V_ofs v); trivial; inv H.
Qed.
Inductive valid_val: val → Prop :=
| valid_val_int: ∀ n, valid_val (Vint n)
| valid_val_vptr: ∀ b ofs, valid_val (Vptr b ofs)
| valid_val_undef: valid_val Vundef.
Definition VMCB_Val := ZMap.t val.
Inductive VMCB_Entry_Z :=
| VMCBEntryZValid (v : Z)
| VMCBEntryZUndef.
Definition VMCB_Z := ZMap.t VMCB_Entry_Z.
Definition VMCB_Entry_Z_Valid (vmcb_z : VMCB_Z) (ofs : Z) : Prop :=
∃ v, ZMap.get ofs vmcb_z = VMCBEntryZValid v ∧ 0 ≤ v ≤ Int.max_unsigned.
Definition VMCB_Z_Range_Valid (vmcb_z : VMCB_Z) (lo high: Z):=
∀ i , lo ≤ i < high → VMCB_Entry_Z_Valid vmcb_z i.
Definition VMCB_Z_Valid (vmcb_z : VMCB_Z) :=
∀ ofs, is_VMCB_Z_ofs ofs = true → VMCB_Entry_Z_Valid vmcb_z ofs.
Ltac simpl_if :=
repeat match goal with
| [ |- context [if ?a then _ else _]] ⇒ destruct a
end; trivial; try omega.
Definition XVMState := ZMap.t val.
Definition bit_not (n : Z) : Z := Z.lxor n (Int.unsigned Int.mone).
Lemma Z_lxor_range :
∀ x y,
0 ≤ x ≤ Int.max_unsigned → 0 ≤ y ≤ Int.max_unsigned →
0 ≤ Z.lxor x y ≤ Int.max_unsigned.
Proof.
unfold Int.max_unsigned. simpl.
intros.
split.
rewrite Z.lxor_nonneg.
split; omega.
assert(Z.lxor x y < 4294967296).
apply Z.log2_lt_cancel.
assert(Z.log2 (Z.lxor x y) ≤ Z.max (Z.log2 x) (Z.log2 y)).
apply Z.log2_lxor.
omega.
omega.
apply Z.le_lt_trans with (m := Z.max (Z.log2 x) (Z.log2 y)); auto.
rewrite Zmax_spec in ×.
destruct (zlt (Z.log2 y) (Z.log2 x)).
assert(Z.log2 x ≤ Z.log2 4294967295).
apply Z.log2_le_mono.
omega.
simpl in ×.
omega.
assert(Z.log2 y ≤ Z.log2 4294967295).
apply Z.log2_le_mono.
omega.
simpl in ×.
omega.
omega.
Qed.
Lemma bit_not_range :
∀ n,
0 ≤ n ≤ Int.max_unsigned →
0 ≤ bit_not n ≤ Int.max_unsigned.
Proof.
unfold bit_not. intros.
apply Z_lxor_range; auto.
unfold Int.mone.
destruct (Int.repr (-1)).
simpl.
unfold Int.max_unsigned in ×.
omega.
Qed.
Primitives: get the information of VMEXIT
idx = 0 : get the lower 32-bit of EXITCODE;
idx = 1 : get the lower 32-bit of EXITINFO1;
idx = 2 : get the lower 32-bit of EXITINFO2;
idx = 3 : get the lower 32-bit of EXITINTINFO;
idx = 4 : get the higher 32-bit of EXITINTINFO.
Function id2exitcode (idx: Z) :=
match idx with
| 0 ⇒ Some VMCB_Z_EXITCODE_LO_OFFSET
| 1 ⇒ Some VMCB_Z_EXITINFO1_LO_OFFSET
| 2 ⇒ Some VMCB_Z_EXITINFO2_LO_OFFSET
| 3 ⇒ Some VMCB_Z_EXITINTINFO_LO_OFFSET
| 4 ⇒ Some VMCB_Z_EXITINTINFO_HI_OFFSET
| _ ⇒ None
end.
Function seg2offset (seg : Z) : Z :=
match seg with
| G_CS ⇒ VMCB_Z_CS_OFFSET
| G_DS ⇒ VMCB_Z_DS_OFFSET
| G_ES ⇒ VMCB_Z_ES_OFFSET
| G_FS ⇒ VMCB_Z_FS_OFFSET
| G_GS ⇒ VMCB_Z_GS_OFFSET
| G_SS ⇒ VMCB_Z_SS_OFFSET
| G_LDTR ⇒ VMCB_Z_LDTR_OFFSET
| G_TR ⇒ VMCB_Z_TR_OFFSET
| G_GDTR ⇒ VMCB_Z_GDTR_OFFSET
| _ ⇒ VMCB_Z_IDTR_OFFSET
end.
Function reg2offset (reg : Z) : option Z :=
match reg with
| G_EAX ⇒ Some VMCB_V_RAX_LO_OFFSET
| G_ESP ⇒ Some VMCB_V_RSP_LO_OFFSET
| G_EIP ⇒ Some VMCB_V_RIP_LO_OFFSET
| G_EFLAGS ⇒ Some VMCB_V_RFLAGS_LO_OFFSET
| G_CR0 ⇒ Some VMCB_V_CR0_LO_OFFSET
| G_CR2 ⇒ Some VMCB_V_CR2_LO_OFFSET
| G_CR3 ⇒ Some VMCB_V_CR3_LO_OFFSET
| G_CR4 ⇒ Some VMCB_V_CR4_LO_OFFSET
| _ ⇒ None
end.
Lemma reg2offset_correct:
∀ r n, reg2offset r = Some n → is_VMCB_V_ofs n = true.
Proof.
intros.
functional inversion H;
trivial.
Qed.
Function xreg2offset (reg : Z) : option Z :=
match reg with
| G_EBX ⇒ Some XVMST_EBX_OFFSET
| G_ECX ⇒ Some XVMST_ECX_OFFSET
| G_EDX ⇒ Some XVMST_EDX_OFFSET
| G_ESI ⇒ Some XVMST_ESI_OFFSET
| G_EDI ⇒ Some XVMST_EDI_OFFSET
| G_EBP ⇒ Some XVMST_EBP_OFFSET
| _ ⇒ None
end.
Lemma xreg2offset_correct:
∀ r n, xreg2offset r = Some n → 0≤ n < XVMST_SIZE.
Proof.
intros.
functional inversion H;
omega.
Qed.
Function hreg2offset (reg : Z) : Z :=
match reg with
| G_EAX ⇒ VMCB_V_RAX_LO_OFFSET
| G_EBX ⇒ XVMST_EBX_OFFSET
| G_ECX ⇒ XVMST_ECX_OFFSET
| G_EDX ⇒ XVMST_EDX_OFFSET
| G_ESI ⇒ XVMST_ESI_OFFSET
| G_EDI ⇒ XVMST_EDI_OFFSET
| G_EBP ⇒ XVMST_EBP_OFFSET
| G_ESP ⇒ VMCB_V_RSP_LO_OFFSET
| _ ⇒ VMCB_V_RIP_LO_OFFSET
end.
End VirtManagement.
Ltac inv_uctx_primitive HVV:=
repeat match goal with
| [ |- context[Pregmap.elt_eq ?a ?b]]
⇒ destruct (Pregmap.elt_eq a b);
[try (eapply HVV; eauto; try omega; try (apply PregToZ_correct; compute;trivial))|]
end.
Ltac inv_hctx_primitive HVV:=
repeat match goal with
| [ |- context[Pregmap.elt_eq ?a ?b]]
⇒ destruct (Pregmap.elt_eq a b);
[try (eapply HVV; eauto; try omega; try (apply PregToZ_Host_correct; compute;trivial))|]
end.
Notation Lremove := (remove LATOwner_dec).
Section IntelVirtManagement.
Section EPTDEF.
Definition EPT_PTAB_INDEX (i:Z) := (i/PgSize) mod five_one_two.
Definition EPT_PDIR_INDEX (i:Z) := (i/ (PgSize × five_one_two)) mod five_one_two.
Definition EPT_PDPT_INDEX (i:Z) := (i/ (PgSize × five_one_two × five_one_two))
mod five_one_two.
Definition EPT_PML4_INDEX (i:Z) := (i/ (PgSize × five_one_two × five_one_two ×
five_one_two)) mod five_one_two.
Definition EPTADDR (i:Z) (ofs:Z) := (i × PgSize) + (ofs mod PgSize).
Inductive EPTPerm :=
| ALL_EPERM.
Definition EPTPerm2Z (perm : EPTPerm) : Z := 7.
Inductive EPTE:=
| EPTEValid (hpa: Z)
| EPTEUndef.
Definition EPTAB := ZMap.t EPTE.
Inductive EPDTE :=
| EPDTEValid (eptab : EPTAB)
| EPDTEUndef.
Definition EPDT := ZMap.t EPDTE.
Inductive EPDPTE :=
| EPDPTEValid (epdt: EPDT)
| EPDPTEUndef.
Definition EPDPT := ZMap.t EPDPTE.
Inductive EPML4E :=
| EPML4EValid (epdpt: EPDPT)
| EPML4EUndef.
Definition EPT := ZMap.t EPML4E.
Definition EPT_valid (ept: EPT) :=
∃ epdpt, ((ZMap.get 0 ept = EPML4EValid epdpt) ∧
(∀ i2, 0 ≤ i2 < 4 →
∃ epdt, ((ZMap.get i2 epdpt = EPDPTEValid epdt) ∧
(∀ i3, 0 ≤ i3 < 512 → ∃ eptab, (ZMap.get i3 epdt = EPDTEValid eptab))))).
Definition EPTPool := ZMap.t EPT.
End EPTDEF.
Section VMCSDEF.
Inductive VMCS_Encoding : Type :=
| VMCS_VPID
| VMCS_GUEST_ES_SELECTOR
| VMCS_GUEST_CS_SELECTOR
| VMCS_GUEST_SS_SELECTOR
| VMCS_GUEST_DS_SELECTOR
| VMCS_GUEST_FS_SELECTOR
| VMCS_GUEST_GS_SELECTOR
| VMCS_GUEST_LDTR_SELECTOR
| VMCS_GUEST_TR_SELECTOR
| VMCS_HOST_ES_SELECTOR
| VMCS_HOST_CS_SELECTOR
| VMCS_HOST_SS_SELECTOR
| VMCS_HOST_DS_SELECTOR
| VMCS_HOST_FS_SELECTOR
| VMCS_HOST_GS_SELECTOR
| VMCS_HOST_TR_SELECTOR
| VMCS_IO_BITMAP_A
| VMCS_IO_BITMAP_A_HI
| VMCS_IO_BITMAP_B
| VMCS_IO_BITMAP_B_HI
| VMCS_MSR_BITMAP
| VMCS_MSR_BITMAP_HI
| VMCS_EXIT_MSR_STORE
| VMCS_EXIT_MSR_LOAD
| VMCS_ENTRY_MSR_LOAD
| VMCS_EXECUTIVE_VMCS
| VMCS_TSC_OFFSET
| VMCS_VIRTUAL_APIC
| VMCS_APIC_ACCESS
| VMCS_EPTP
| VMCS_EPTP_HI
| VMCS_GUEST_PHYSICAL_ADDRESS
| VMCS_LINK_POINTER
| VMCS_GUEST_IA32_DEBUGCTL
| VMCS_GUEST_IA32_PAT
| VMCS_GUEST_IA32_EFER
| VMCS_GUEST_IA32_PERF_GLOBAL_CTRL
| VMCS_GUEST_PDPTE0
| VMCS_GUEST_PDPTE1
| VMCS_GUEST_PDPTE2
| VMCS_GUEST_PDPTE3
| VMCS_HOST_IA32_PAT
| VMCS_HOST_IA32_EFER
| VMCS_HOST_IA32_PERF_GLOBAL_CTRL
| VMCS_PIN_BASED_CTLS
| VMCS_PRI_PROC_BASED_CTLS
| VMCS_EXCEPTION_BITMAP
| VMCS_PF_ERROR_MASK
| VMCS_PF_ERROR_MATCH
| VMCS_CR3_TARGET_COUNT
| VMCS_EXIT_CTLS
| VMCS_EXIT_MSR_STORE_COUNT
| VMCS_EXIT_MSR_LOAD_COUNT
| VMCS_ENTRY_CTLS
| VMCS_ENTRY_MSR_LOAD_COUNT
| VMCS_ENTRY_INTR_INFO
| VMCS_ENTRY_EXCEPTION_ERROR
| VMCS_ENTRY_INST_LENGTH
| VMCS_TPR_THRESHOLD
| VMCS_SEC_PROC_BASED_CTLS
| VMCS_PLE_GAP
| VMCS_PLE_WINDOW
| VMCS_INSTRUCTION_ERROR
| VMCS_EXIT_REASON
| VMCS_EXIT_INTERRUPTION_INFO
| VMCS_EXIT_INTERRUPTION_ERROR
| VMCS_IDT_VECTORING_INFO
| VMCS_IDT_VECTORING_ERROR
| VMCS_EXIT_INSTRUCTION_LENGTH
| VMCS_EXIT_INSTRUCTION_INFO
| VMCS_GUEST_ES_LIMIT
| VMCS_GUEST_CS_LIMIT
| VMCS_GUEST_SS_LIMIT
| VMCS_GUEST_DS_LIMIT
| VMCS_GUEST_FS_LIMIT
| VMCS_GUEST_GS_LIMIT
| VMCS_GUEST_LDTR_LIMIT
| VMCS_GUEST_TR_LIMIT
| VMCS_GUEST_GDTR_LIMIT
| VMCS_GUEST_IDTR_LIMIT
| VMCS_GUEST_ES_ACCESS_RIGHTS
| VMCS_GUEST_CS_ACCESS_RIGHTS
| VMCS_GUEST_SS_ACCESS_RIGHTS
| VMCS_GUEST_DS_ACCESS_RIGHTS
| VMCS_GUEST_FS_ACCESS_RIGHTS
| VMCS_GUEST_GS_ACCESS_RIGHTS
| VMCS_GUEST_LDTR_ACCESS_RIGHTS
| VMCS_GUEST_TR_ACCESS_RIGHTS
| VMCS_GUEST_INTERRUPTIBILITY
| VMCS_GUEST_ACTIVITY
| VMCS_GUEST_SMBASE
| VMCS_GUEST_IA32_SYSENTER_CS
| VMCS_PREEMPTION_TIMER_VALUE
| VMCS_HOST_IA32_SYSENTER_CS
| VMCS_CR0_MASK
| VMCS_CR4_MASK
| VMCS_CR0_SHADOW
| VMCS_CR4_SHADOW
| VMCS_CR3_TARGET0
| VMCS_CR3_TARGET1
| VMCS_CR3_TARGET2
| VMCS_CR3_TARGET3
| VMCS_EXIT_QUALIFICATION
| VMCS_IO_RCX
| VMCS_IO_RSI
| VMCS_IO_RDI
| VMCS_IO_RIP
| VMCS_GUEST_LINEAR_ADDRESS
| VMCS_GUEST_CR0
| VMCS_GUEST_CR3
| VMCS_GUEST_CR4
| VMCS_GUEST_ES_BASE
| VMCS_GUEST_CS_BASE
| VMCS_GUEST_SS_BASE
| VMCS_GUEST_DS_BASE
| VMCS_GUEST_FS_BASE
| VMCS_GUEST_GS_BASE
| VMCS_GUEST_LDTR_BASE
| VMCS_GUEST_TR_BASE
| VMCS_GUEST_GDTR_BASE
| VMCS_GUEST_IDTR_BASE
| VMCS_GUEST_DR7
| VMCS_GUEST_RSP
| VMCS_GUEST_RIP
| VMCS_GUEST_RFLAGS
| VMCS_GUEST_PENDING_DBG_EXCEPTIONS
| VMCS_GUEST_IA32_SYSENTER_ESP
| VMCS_GUEST_IA32_SYSENTER_EIP
| VMCS_HOST_CR0
| VMCS_HOST_CR3
| VMCS_HOST_CR4
| VMCS_HOST_FS_BASE
| VMCS_HOST_GS_BASE
| VMCS_HOST_TR_BASE
| VMCS_HOST_GDTR_BASE
| VMCS_HOST_IDTR_BASE
| VMCS_HOST_IA32_SYSENTER_ESP
| VMCS_HOST_IA32_SYSENTER_EIP
| VMCS_HOST_RSP
| VMCS_HOST_RIP.
Function vmcs_ZtoEncoding (z:Z) : option VMCS_Encoding :=
match z with
| C_VMCS_VPID ⇒ Some VMCS_VPID
| C_VMCS_GUEST_ES_SELECTOR ⇒ Some VMCS_GUEST_ES_SELECTOR
| C_VMCS_GUEST_CS_SELECTOR ⇒ Some VMCS_GUEST_CS_SELECTOR
| C_VMCS_GUEST_SS_SELECTOR ⇒ Some VMCS_GUEST_SS_SELECTOR
| C_VMCS_GUEST_DS_SELECTOR ⇒ Some VMCS_GUEST_DS_SELECTOR
| C_VMCS_GUEST_FS_SELECTOR ⇒ Some VMCS_GUEST_FS_SELECTOR
| C_VMCS_GUEST_GS_SELECTOR ⇒ Some VMCS_GUEST_GS_SELECTOR
| C_VMCS_GUEST_LDTR_SELECTOR ⇒ Some VMCS_GUEST_LDTR_SELECTOR
| C_VMCS_GUEST_TR_SELECTOR ⇒ Some VMCS_GUEST_TR_SELECTOR
| C_VMCS_HOST_ES_SELECTOR ⇒ Some VMCS_HOST_ES_SELECTOR
| C_VMCS_HOST_CS_SELECTOR ⇒ Some VMCS_HOST_CS_SELECTOR
| C_VMCS_HOST_SS_SELECTOR ⇒ Some VMCS_HOST_SS_SELECTOR
| C_VMCS_HOST_DS_SELECTOR ⇒ Some VMCS_HOST_DS_SELECTOR
| C_VMCS_HOST_FS_SELECTOR ⇒ Some VMCS_HOST_FS_SELECTOR
| C_VMCS_HOST_GS_SELECTOR ⇒ Some VMCS_HOST_GS_SELECTOR
| C_VMCS_HOST_TR_SELECTOR ⇒ Some VMCS_HOST_TR_SELECTOR
| C_VMCS_IO_BITMAP_A ⇒ Some VMCS_IO_BITMAP_A
| C_VMCS_IO_BITMAP_A_HI ⇒ Some VMCS_IO_BITMAP_A_HI
| C_VMCS_IO_BITMAP_B ⇒ Some VMCS_IO_BITMAP_B
| C_VMCS_IO_BITMAP_B_HI ⇒ Some VMCS_IO_BITMAP_B_HI
| C_VMCS_MSR_BITMAP ⇒ Some VMCS_MSR_BITMAP
| C_VMCS_MSR_BITMAP_HI ⇒ Some VMCS_MSR_BITMAP_HI
| C_VMCS_EXIT_MSR_STORE ⇒ Some VMCS_EXIT_MSR_STORE
| C_VMCS_EXIT_MSR_LOAD ⇒ Some VMCS_EXIT_MSR_LOAD
| C_VMCS_ENTRY_MSR_LOAD ⇒ Some VMCS_ENTRY_MSR_LOAD
| C_VMCS_EXECUTIVE_VMCS ⇒ Some VMCS_EXECUTIVE_VMCS
| C_VMCS_TSC_OFFSET ⇒ Some VMCS_TSC_OFFSET
| C_VMCS_VIRTUAL_APIC ⇒ Some VMCS_VIRTUAL_APIC
| C_VMCS_APIC_ACCESS ⇒ Some VMCS_APIC_ACCESS
| C_VMCS_EPTP ⇒ Some VMCS_EPTP
| C_VMCS_EPTP_HI ⇒ Some VMCS_EPTP_HI
| C_VMCS_GUEST_PHYSICAL_ADDRESS ⇒ Some VMCS_GUEST_PHYSICAL_ADDRESS
| C_VMCS_LINK_POINTER ⇒ Some VMCS_LINK_POINTER
| C_VMCS_GUEST_IA32_DEBUGCTL ⇒ Some VMCS_GUEST_IA32_DEBUGCTL
| C_VMCS_GUEST_IA32_PAT ⇒ Some VMCS_GUEST_IA32_PAT
| C_VMCS_GUEST_IA32_EFER ⇒ Some VMCS_GUEST_IA32_EFER
| C_VMCS_GUEST_IA32_PERF_GLOBAL_CTRL ⇒ Some VMCS_GUEST_IA32_PERF_GLOBAL_CTRL
| C_VMCS_GUEST_PDPTE0 ⇒ Some VMCS_GUEST_PDPTE0
| C_VMCS_GUEST_PDPTE1 ⇒ Some VMCS_GUEST_PDPTE1
| C_VMCS_GUEST_PDPTE2 ⇒ Some VMCS_GUEST_PDPTE2
| C_VMCS_GUEST_PDPTE3 ⇒ Some VMCS_GUEST_PDPTE3
| C_VMCS_HOST_IA32_PAT ⇒ Some VMCS_HOST_IA32_PAT
| C_VMCS_HOST_IA32_EFER ⇒ Some VMCS_HOST_IA32_EFER
| C_VMCS_HOST_IA32_PERF_GLOBAL_CTRL ⇒ Some VMCS_HOST_IA32_PERF_GLOBAL_CTRL
| C_VMCS_PIN_BASED_CTLS ⇒ Some VMCS_PIN_BASED_CTLS
| C_VMCS_PRI_PROC_BASED_CTLS ⇒ Some VMCS_PRI_PROC_BASED_CTLS
| C_VMCS_EXCEPTION_BITMAP ⇒ Some VMCS_EXCEPTION_BITMAP
| C_VMCS_PF_ERROR_MASK ⇒ Some VMCS_PF_ERROR_MASK
| C_VMCS_PF_ERROR_MATCH ⇒ Some VMCS_PF_ERROR_MATCH
| C_VMCS_CR3_TARGET_COUNT ⇒ Some VMCS_CR3_TARGET_COUNT
| C_VMCS_EXIT_CTLS ⇒ Some VMCS_EXIT_CTLS
| C_VMCS_EXIT_MSR_STORE_COUNT ⇒ Some VMCS_EXIT_MSR_STORE_COUNT
| C_VMCS_EXIT_MSR_LOAD_COUNT ⇒ Some VMCS_EXIT_MSR_LOAD_COUNT
| C_VMCS_ENTRY_CTLS ⇒ Some VMCS_ENTRY_CTLS
| C_VMCS_ENTRY_MSR_LOAD_COUNT ⇒ Some VMCS_ENTRY_MSR_LOAD_COUNT
| C_VMCS_ENTRY_INTR_INFO ⇒ Some VMCS_ENTRY_INTR_INFO
| C_VMCS_ENTRY_EXCEPTION_ERROR ⇒ Some VMCS_ENTRY_EXCEPTION_ERROR
| C_VMCS_ENTRY_INST_LENGTH ⇒ Some VMCS_ENTRY_INST_LENGTH
| C_VMCS_TPR_THRESHOLD ⇒ Some VMCS_TPR_THRESHOLD
| C_VMCS_SEC_PROC_BASED_CTLS ⇒ Some VMCS_SEC_PROC_BASED_CTLS
| C_VMCS_PLE_GAP ⇒ Some VMCS_PLE_GAP
| C_VMCS_PLE_WINDOW ⇒ Some VMCS_PLE_WINDOW
| C_VMCS_INSTRUCTION_ERROR ⇒ Some VMCS_INSTRUCTION_ERROR
| C_VMCS_EXIT_REASON ⇒ Some VMCS_EXIT_REASON
| C_VMCS_EXIT_INTERRUPTION_INFO ⇒ Some VMCS_EXIT_INTERRUPTION_INFO
| C_VMCS_EXIT_INTERRUPTION_ERROR ⇒ Some VMCS_EXIT_INTERRUPTION_ERROR
| C_VMCS_IDT_VECTORING_INFO ⇒ Some VMCS_IDT_VECTORING_INFO
| C_VMCS_IDT_VECTORING_ERROR ⇒ Some VMCS_IDT_VECTORING_ERROR
| C_VMCS_EXIT_INSTRUCTION_LENGTH ⇒ Some VMCS_EXIT_INSTRUCTION_LENGTH
| C_VMCS_EXIT_INSTRUCTION_INFO ⇒ Some VMCS_EXIT_INSTRUCTION_INFO
| C_VMCS_GUEST_ES_LIMIT ⇒ Some VMCS_GUEST_ES_LIMIT
| C_VMCS_GUEST_CS_LIMIT ⇒ Some VMCS_GUEST_CS_LIMIT
| C_VMCS_GUEST_SS_LIMIT ⇒ Some VMCS_GUEST_SS_LIMIT
| C_VMCS_GUEST_DS_LIMIT ⇒ Some VMCS_GUEST_DS_LIMIT
| C_VMCS_GUEST_FS_LIMIT ⇒ Some VMCS_GUEST_FS_LIMIT
| C_VMCS_GUEST_GS_LIMIT ⇒ Some VMCS_GUEST_GS_LIMIT
| C_VMCS_GUEST_LDTR_LIMIT ⇒ Some VMCS_GUEST_LDTR_LIMIT
| C_VMCS_GUEST_TR_LIMIT ⇒ Some VMCS_GUEST_TR_LIMIT
| C_VMCS_GUEST_GDTR_LIMIT ⇒ Some VMCS_GUEST_GDTR_LIMIT
| C_VMCS_GUEST_IDTR_LIMIT ⇒ Some VMCS_GUEST_IDTR_LIMIT
| C_VMCS_GUEST_ES_ACCESS_RIGHTS ⇒ Some VMCS_GUEST_ES_ACCESS_RIGHTS
| C_VMCS_GUEST_CS_ACCESS_RIGHTS ⇒ Some VMCS_GUEST_CS_ACCESS_RIGHTS
| C_VMCS_GUEST_SS_ACCESS_RIGHTS ⇒ Some VMCS_GUEST_SS_ACCESS_RIGHTS
| C_VMCS_GUEST_DS_ACCESS_RIGHTS ⇒ Some VMCS_GUEST_DS_ACCESS_RIGHTS
| C_VMCS_GUEST_FS_ACCESS_RIGHTS ⇒ Some VMCS_GUEST_FS_ACCESS_RIGHTS
| C_VMCS_GUEST_GS_ACCESS_RIGHTS ⇒ Some VMCS_GUEST_GS_ACCESS_RIGHTS
| C_VMCS_GUEST_LDTR_ACCESS_RIGHTS ⇒ Some VMCS_GUEST_LDTR_ACCESS_RIGHTS
| C_VMCS_GUEST_TR_ACCESS_RIGHTS ⇒ Some VMCS_GUEST_TR_ACCESS_RIGHTS
| C_VMCS_GUEST_INTERRUPTIBILITY ⇒ Some VMCS_GUEST_INTERRUPTIBILITY
| C_VMCS_GUEST_ACTIVITY ⇒ Some VMCS_GUEST_ACTIVITY
| C_VMCS_GUEST_SMBASE ⇒ Some VMCS_GUEST_SMBASE
| C_VMCS_GUEST_IA32_SYSENTER_CS ⇒ Some VMCS_GUEST_IA32_SYSENTER_CS
| C_VMCS_PREEMPTION_TIMER_VALUE ⇒ Some VMCS_PREEMPTION_TIMER_VALUE
| C_VMCS_HOST_IA32_SYSENTER_CS ⇒ Some VMCS_HOST_IA32_SYSENTER_CS
| C_VMCS_CR0_MASK ⇒ Some VMCS_CR0_MASK
| C_VMCS_CR4_MASK ⇒ Some VMCS_CR4_MASK
| C_VMCS_CR0_SHADOW ⇒ Some VMCS_CR0_SHADOW
| C_VMCS_CR4_SHADOW ⇒ Some VMCS_CR4_SHADOW
| C_VMCS_CR3_TARGET0 ⇒ Some VMCS_CR3_TARGET0
| C_VMCS_CR3_TARGET1 ⇒ Some VMCS_CR3_TARGET1
| C_VMCS_CR3_TARGET2 ⇒ Some VMCS_CR3_TARGET2
| C_VMCS_CR3_TARGET3 ⇒ Some VMCS_CR3_TARGET3
| C_VMCS_EXIT_QUALIFICATION ⇒ Some VMCS_EXIT_QUALIFICATION
| C_VMCS_IO_RCX ⇒ Some VMCS_IO_RCX
| C_VMCS_IO_RSI ⇒ Some VMCS_IO_RSI
| C_VMCS_IO_RDI ⇒ Some VMCS_IO_RDI
| C_VMCS_IO_RIP ⇒ Some VMCS_IO_RIP
| C_VMCS_GUEST_LINEAR_ADDRESS ⇒ Some VMCS_GUEST_LINEAR_ADDRESS
| C_VMCS_GUEST_CR0 ⇒ Some VMCS_GUEST_CR0
| C_VMCS_GUEST_CR3 ⇒ Some VMCS_GUEST_CR3
| C_VMCS_GUEST_CR4 ⇒ Some VMCS_GUEST_CR4
| C_VMCS_GUEST_ES_BASE ⇒ Some VMCS_GUEST_ES_BASE
| C_VMCS_GUEST_CS_BASE ⇒ Some VMCS_GUEST_CS_BASE
| C_VMCS_GUEST_SS_BASE ⇒ Some VMCS_GUEST_SS_BASE
| C_VMCS_GUEST_DS_BASE ⇒ Some VMCS_GUEST_DS_BASE
| C_VMCS_GUEST_FS_BASE ⇒ Some VMCS_GUEST_FS_BASE
| C_VMCS_GUEST_GS_BASE ⇒ Some VMCS_GUEST_GS_BASE
| C_VMCS_GUEST_LDTR_BASE ⇒ Some VMCS_GUEST_LDTR_BASE
| C_VMCS_GUEST_TR_BASE ⇒ Some VMCS_GUEST_TR_BASE
| C_VMCS_GUEST_GDTR_BASE ⇒ Some VMCS_GUEST_GDTR_BASE
| C_VMCS_GUEST_IDTR_BASE ⇒ Some VMCS_GUEST_IDTR_BASE
| C_VMCS_GUEST_DR7 ⇒ Some VMCS_GUEST_DR7
| C_VMCS_GUEST_RSP ⇒ Some VMCS_GUEST_RSP
| C_VMCS_GUEST_RIP ⇒ Some VMCS_GUEST_RIP
| C_VMCS_GUEST_RFLAGS ⇒ Some VMCS_GUEST_RFLAGS
| C_VMCS_GUEST_PENDING_DBG_EXCEPTIONS ⇒ Some VMCS_GUEST_PENDING_DBG_EXCEPTIONS
| C_VMCS_GUEST_IA32_SYSENTER_ESP ⇒ Some VMCS_GUEST_IA32_SYSENTER_ESP
| C_VMCS_GUEST_IA32_SYSENTER_EIP ⇒ Some VMCS_GUEST_IA32_SYSENTER_EIP
| C_VMCS_HOST_CR0 ⇒ Some VMCS_HOST_CR0
| C_VMCS_HOST_CR3 ⇒ Some VMCS_HOST_CR3
| C_VMCS_HOST_CR4 ⇒ Some VMCS_HOST_CR4
| C_VMCS_HOST_FS_BASE ⇒ Some VMCS_HOST_FS_BASE
| C_VMCS_HOST_GS_BASE ⇒ Some VMCS_HOST_GS_BASE
| C_VMCS_HOST_TR_BASE ⇒ Some VMCS_HOST_TR_BASE
| C_VMCS_HOST_GDTR_BASE ⇒ Some VMCS_HOST_GDTR_BASE
| C_VMCS_HOST_IDTR_BASE ⇒ Some VMCS_HOST_IDTR_BASE
| C_VMCS_HOST_IA32_SYSENTER_ESP ⇒ Some VMCS_HOST_IA32_SYSENTER_ESP
| C_VMCS_HOST_IA32_SYSENTER_EIP ⇒ Some VMCS_HOST_IA32_SYSENTER_EIP
| C_VMCS_HOST_RSP ⇒ Some VMCS_HOST_RSP
| C_VMCS_HOST_RIP ⇒ Some VMCS_HOST_RIP
| _ ⇒ None
end.
Definition vmcs_EncodingtoZ (e: VMCS_Encoding) : Z :=
match e with
| VMCS_VPID ⇒ C_VMCS_VPID
| VMCS_GUEST_ES_SELECTOR ⇒ C_VMCS_GUEST_ES_SELECTOR
| VMCS_GUEST_CS_SELECTOR ⇒ C_VMCS_GUEST_CS_SELECTOR
| VMCS_GUEST_SS_SELECTOR ⇒ C_VMCS_GUEST_SS_SELECTOR
| VMCS_GUEST_DS_SELECTOR ⇒ C_VMCS_GUEST_DS_SELECTOR
| VMCS_GUEST_FS_SELECTOR ⇒ C_VMCS_GUEST_FS_SELECTOR
| VMCS_GUEST_GS_SELECTOR ⇒ C_VMCS_GUEST_GS_SELECTOR
| VMCS_GUEST_LDTR_SELECTOR ⇒ C_VMCS_GUEST_LDTR_SELECTOR
| VMCS_GUEST_TR_SELECTOR ⇒ C_VMCS_GUEST_TR_SELECTOR
| VMCS_HOST_ES_SELECTOR ⇒ C_VMCS_HOST_ES_SELECTOR
| VMCS_HOST_CS_SELECTOR ⇒ C_VMCS_HOST_CS_SELECTOR
| VMCS_HOST_SS_SELECTOR ⇒ C_VMCS_HOST_SS_SELECTOR
| VMCS_HOST_DS_SELECTOR ⇒ C_VMCS_HOST_DS_SELECTOR
| VMCS_HOST_FS_SELECTOR ⇒ C_VMCS_HOST_FS_SELECTOR
| VMCS_HOST_GS_SELECTOR ⇒ C_VMCS_HOST_GS_SELECTOR
| VMCS_HOST_TR_SELECTOR ⇒ C_VMCS_HOST_TR_SELECTOR
| VMCS_IO_BITMAP_A ⇒ C_VMCS_IO_BITMAP_A
| VMCS_IO_BITMAP_A_HI ⇒ C_VMCS_IO_BITMAP_A_HI
| VMCS_IO_BITMAP_B ⇒ C_VMCS_IO_BITMAP_B
| VMCS_IO_BITMAP_B_HI ⇒ C_VMCS_IO_BITMAP_B_HI
| VMCS_MSR_BITMAP ⇒ C_VMCS_MSR_BITMAP
| VMCS_MSR_BITMAP_HI ⇒ C_VMCS_MSR_BITMAP_HI
| VMCS_EXIT_MSR_STORE ⇒ C_VMCS_EXIT_MSR_STORE
| VMCS_EXIT_MSR_LOAD ⇒ C_VMCS_EXIT_MSR_LOAD
| VMCS_ENTRY_MSR_LOAD ⇒ C_VMCS_ENTRY_MSR_LOAD
| VMCS_EXECUTIVE_VMCS ⇒ C_VMCS_EXECUTIVE_VMCS
| VMCS_TSC_OFFSET ⇒ C_VMCS_TSC_OFFSET
| VMCS_VIRTUAL_APIC ⇒ C_VMCS_VIRTUAL_APIC
| VMCS_APIC_ACCESS ⇒ C_VMCS_APIC_ACCESS
| VMCS_EPTP ⇒ C_VMCS_EPTP
| VMCS_EPTP_HI ⇒ C_VMCS_EPTP_HI
| VMCS_GUEST_PHYSICAL_ADDRESS ⇒ C_VMCS_GUEST_PHYSICAL_ADDRESS
| VMCS_LINK_POINTER ⇒ C_VMCS_LINK_POINTER
| VMCS_GUEST_IA32_DEBUGCTL ⇒ C_VMCS_GUEST_IA32_DEBUGCTL
| VMCS_GUEST_IA32_PAT ⇒ C_VMCS_GUEST_IA32_PAT
| VMCS_GUEST_IA32_EFER ⇒ C_VMCS_GUEST_IA32_EFER
| VMCS_GUEST_IA32_PERF_GLOBAL_CTRL ⇒ C_VMCS_GUEST_IA32_PERF_GLOBAL_CTRL
| VMCS_GUEST_PDPTE0 ⇒ C_VMCS_GUEST_PDPTE0
| VMCS_GUEST_PDPTE1 ⇒ C_VMCS_GUEST_PDPTE1
| VMCS_GUEST_PDPTE2 ⇒ C_VMCS_GUEST_PDPTE2
| VMCS_GUEST_PDPTE3 ⇒ C_VMCS_GUEST_PDPTE3
| VMCS_HOST_IA32_PAT ⇒ C_VMCS_HOST_IA32_PAT
| VMCS_HOST_IA32_EFER ⇒ C_VMCS_HOST_IA32_EFER
| VMCS_HOST_IA32_PERF_GLOBAL_CTRL ⇒ C_VMCS_HOST_IA32_PERF_GLOBAL_CTRL
| VMCS_PIN_BASED_CTLS ⇒ C_VMCS_PIN_BASED_CTLS
| VMCS_PRI_PROC_BASED_CTLS ⇒ C_VMCS_PRI_PROC_BASED_CTLS
| VMCS_EXCEPTION_BITMAP ⇒ C_VMCS_EXCEPTION_BITMAP
| VMCS_PF_ERROR_MASK ⇒ C_VMCS_PF_ERROR_MASK
| VMCS_PF_ERROR_MATCH ⇒ C_VMCS_PF_ERROR_MATCH
| VMCS_CR3_TARGET_COUNT ⇒ C_VMCS_CR3_TARGET_COUNT
| VMCS_EXIT_CTLS ⇒ C_VMCS_EXIT_CTLS
| VMCS_EXIT_MSR_STORE_COUNT ⇒ C_VMCS_EXIT_MSR_STORE_COUNT
| VMCS_EXIT_MSR_LOAD_COUNT ⇒ C_VMCS_EXIT_MSR_LOAD_COUNT
| VMCS_ENTRY_CTLS ⇒ C_VMCS_ENTRY_CTLS
| VMCS_ENTRY_MSR_LOAD_COUNT ⇒ C_VMCS_ENTRY_MSR_LOAD_COUNT
| VMCS_ENTRY_INTR_INFO ⇒ C_VMCS_ENTRY_INTR_INFO
| VMCS_ENTRY_EXCEPTION_ERROR ⇒ C_VMCS_ENTRY_EXCEPTION_ERROR
| VMCS_ENTRY_INST_LENGTH ⇒ C_VMCS_ENTRY_INST_LENGTH
| VMCS_TPR_THRESHOLD ⇒ C_VMCS_TPR_THRESHOLD
| VMCS_SEC_PROC_BASED_CTLS ⇒ C_VMCS_SEC_PROC_BASED_CTLS
| VMCS_PLE_GAP ⇒ C_VMCS_PLE_GAP
| VMCS_PLE_WINDOW ⇒ C_VMCS_PLE_WINDOW
| VMCS_INSTRUCTION_ERROR ⇒ C_VMCS_INSTRUCTION_ERROR
| VMCS_EXIT_REASON ⇒ C_VMCS_EXIT_REASON
| VMCS_EXIT_INTERRUPTION_INFO ⇒ C_VMCS_EXIT_INTERRUPTION_INFO
| VMCS_EXIT_INTERRUPTION_ERROR ⇒ C_VMCS_EXIT_INTERRUPTION_ERROR
| VMCS_IDT_VECTORING_INFO ⇒ C_VMCS_IDT_VECTORING_INFO
| VMCS_IDT_VECTORING_ERROR ⇒ C_VMCS_IDT_VECTORING_ERROR
| VMCS_EXIT_INSTRUCTION_LENGTH ⇒ C_VMCS_EXIT_INSTRUCTION_LENGTH
| VMCS_EXIT_INSTRUCTION_INFO ⇒ C_VMCS_EXIT_INSTRUCTION_INFO
| VMCS_GUEST_ES_LIMIT ⇒ C_VMCS_GUEST_ES_LIMIT
| VMCS_GUEST_CS_LIMIT ⇒ C_VMCS_GUEST_CS_LIMIT
| VMCS_GUEST_SS_LIMIT ⇒ C_VMCS_GUEST_SS_LIMIT
| VMCS_GUEST_DS_LIMIT ⇒ C_VMCS_GUEST_DS_LIMIT
| VMCS_GUEST_FS_LIMIT ⇒ C_VMCS_GUEST_FS_LIMIT
| VMCS_GUEST_GS_LIMIT ⇒ C_VMCS_GUEST_GS_LIMIT
| VMCS_GUEST_LDTR_LIMIT ⇒ C_VMCS_GUEST_LDTR_LIMIT
| VMCS_GUEST_TR_LIMIT ⇒ C_VMCS_GUEST_TR_LIMIT
| VMCS_GUEST_GDTR_LIMIT ⇒ C_VMCS_GUEST_GDTR_LIMIT
| VMCS_GUEST_IDTR_LIMIT ⇒ C_VMCS_GUEST_IDTR_LIMIT
| VMCS_GUEST_ES_ACCESS_RIGHTS ⇒ C_VMCS_GUEST_ES_ACCESS_RIGHTS
| VMCS_GUEST_CS_ACCESS_RIGHTS ⇒ C_VMCS_GUEST_CS_ACCESS_RIGHTS
| VMCS_GUEST_SS_ACCESS_RIGHTS ⇒ C_VMCS_GUEST_SS_ACCESS_RIGHTS
| VMCS_GUEST_DS_ACCESS_RIGHTS ⇒ C_VMCS_GUEST_DS_ACCESS_RIGHTS
| VMCS_GUEST_FS_ACCESS_RIGHTS ⇒ C_VMCS_GUEST_FS_ACCESS_RIGHTS
| VMCS_GUEST_GS_ACCESS_RIGHTS ⇒ C_VMCS_GUEST_GS_ACCESS_RIGHTS
| VMCS_GUEST_LDTR_ACCESS_RIGHTS ⇒ C_VMCS_GUEST_LDTR_ACCESS_RIGHTS
| VMCS_GUEST_TR_ACCESS_RIGHTS ⇒ C_VMCS_GUEST_TR_ACCESS_RIGHTS
| VMCS_GUEST_INTERRUPTIBILITY ⇒ C_VMCS_GUEST_INTERRUPTIBILITY
| VMCS_GUEST_ACTIVITY ⇒ C_VMCS_GUEST_ACTIVITY
| VMCS_GUEST_SMBASE ⇒ C_VMCS_GUEST_SMBASE
| VMCS_GUEST_IA32_SYSENTER_CS ⇒ C_VMCS_GUEST_IA32_SYSENTER_CS
| VMCS_PREEMPTION_TIMER_VALUE ⇒ C_VMCS_PREEMPTION_TIMER_VALUE
| VMCS_HOST_IA32_SYSENTER_CS ⇒ C_VMCS_HOST_IA32_SYSENTER_CS
| VMCS_CR0_MASK ⇒ C_VMCS_CR0_MASK
| VMCS_CR4_MASK ⇒ C_VMCS_CR4_MASK
| VMCS_CR0_SHADOW ⇒ C_VMCS_CR0_SHADOW
| VMCS_CR4_SHADOW ⇒ C_VMCS_CR4_SHADOW
| VMCS_CR3_TARGET0 ⇒ C_VMCS_CR3_TARGET0
| VMCS_CR3_TARGET1 ⇒ C_VMCS_CR3_TARGET1
| VMCS_CR3_TARGET2 ⇒ C_VMCS_CR3_TARGET2
| VMCS_CR3_TARGET3 ⇒ C_VMCS_CR3_TARGET3
| VMCS_EXIT_QUALIFICATION ⇒ C_VMCS_EXIT_QUALIFICATION
| VMCS_IO_RCX ⇒ C_VMCS_IO_RCX
| VMCS_IO_RSI ⇒ C_VMCS_IO_RSI
| VMCS_IO_RDI ⇒ C_VMCS_IO_RDI
| VMCS_IO_RIP ⇒ C_VMCS_IO_RIP
| VMCS_GUEST_LINEAR_ADDRESS ⇒ C_VMCS_GUEST_LINEAR_ADDRESS
| VMCS_GUEST_CR0 ⇒ C_VMCS_GUEST_CR0
| VMCS_GUEST_CR3 ⇒ C_VMCS_GUEST_CR3
| VMCS_GUEST_CR4 ⇒ C_VMCS_GUEST_CR4
| VMCS_GUEST_ES_BASE ⇒ C_VMCS_GUEST_ES_BASE
| VMCS_GUEST_CS_BASE ⇒ C_VMCS_GUEST_CS_BASE
| VMCS_GUEST_SS_BASE ⇒ C_VMCS_GUEST_SS_BASE
| VMCS_GUEST_DS_BASE ⇒ C_VMCS_GUEST_DS_BASE
| VMCS_GUEST_FS_BASE ⇒ C_VMCS_GUEST_FS_BASE
| VMCS_GUEST_GS_BASE ⇒ C_VMCS_GUEST_GS_BASE
| VMCS_GUEST_LDTR_BASE ⇒ C_VMCS_GUEST_LDTR_BASE
| VMCS_GUEST_TR_BASE ⇒ C_VMCS_GUEST_TR_BASE
| VMCS_GUEST_GDTR_BASE ⇒ C_VMCS_GUEST_GDTR_BASE
| VMCS_GUEST_IDTR_BASE ⇒ C_VMCS_GUEST_IDTR_BASE
| VMCS_GUEST_DR7 ⇒ C_VMCS_GUEST_DR7
| VMCS_GUEST_RSP ⇒ C_VMCS_GUEST_RSP
| VMCS_GUEST_RIP ⇒ C_VMCS_GUEST_RIP
| VMCS_GUEST_RFLAGS ⇒ C_VMCS_GUEST_RFLAGS
| VMCS_GUEST_PENDING_DBG_EXCEPTIONS ⇒ C_VMCS_GUEST_PENDING_DBG_EXCEPTIONS
| VMCS_GUEST_IA32_SYSENTER_ESP ⇒ C_VMCS_GUEST_IA32_SYSENTER_ESP
| VMCS_GUEST_IA32_SYSENTER_EIP ⇒ C_VMCS_GUEST_IA32_SYSENTER_EIP
| VMCS_HOST_CR0 ⇒ C_VMCS_HOST_CR0
| VMCS_HOST_CR3 ⇒ C_VMCS_HOST_CR3
| VMCS_HOST_CR4 ⇒ C_VMCS_HOST_CR4
| VMCS_HOST_FS_BASE ⇒ C_VMCS_HOST_FS_BASE
| VMCS_HOST_GS_BASE ⇒ C_VMCS_HOST_GS_BASE
| VMCS_HOST_TR_BASE ⇒ C_VMCS_HOST_TR_BASE
| VMCS_HOST_GDTR_BASE ⇒ C_VMCS_HOST_GDTR_BASE
| VMCS_HOST_IDTR_BASE ⇒ C_VMCS_HOST_IDTR_BASE
| VMCS_HOST_IA32_SYSENTER_ESP ⇒ C_VMCS_HOST_IA32_SYSENTER_ESP
| VMCS_HOST_IA32_SYSENTER_EIP ⇒ C_VMCS_HOST_IA32_SYSENTER_EIP
| VMCS_HOST_RSP ⇒ C_VMCS_HOST_RSP
| VMCS_HOST_RIP ⇒ C_VMCS_HOST_RIP
end.
Definition vmcs_encoding_beq (a b: VMCS_Encoding): bool :=
match (a, b) with
| (VMCS_VPID, VMCS_VPID) ⇒ true
| (VMCS_GUEST_ES_SELECTOR, VMCS_GUEST_ES_SELECTOR) ⇒ true
| (VMCS_GUEST_CS_SELECTOR, VMCS_GUEST_CS_SELECTOR) ⇒ true
| (VMCS_GUEST_SS_SELECTOR, VMCS_GUEST_SS_SELECTOR) ⇒ true
| (VMCS_GUEST_DS_SELECTOR, VMCS_GUEST_DS_SELECTOR) ⇒ true
| (VMCS_GUEST_FS_SELECTOR, VMCS_GUEST_FS_SELECTOR) ⇒ true
| (VMCS_GUEST_GS_SELECTOR, VMCS_GUEST_GS_SELECTOR) ⇒ true
| (VMCS_GUEST_LDTR_SELECTOR, VMCS_GUEST_LDTR_SELECTOR) ⇒ true
| (VMCS_GUEST_TR_SELECTOR, VMCS_GUEST_TR_SELECTOR) ⇒ true
| (VMCS_HOST_ES_SELECTOR, VMCS_HOST_ES_SELECTOR) ⇒ true
| (VMCS_HOST_CS_SELECTOR, VMCS_HOST_CS_SELECTOR) ⇒ true
| (VMCS_HOST_SS_SELECTOR, VMCS_HOST_SS_SELECTOR) ⇒ true
| (VMCS_HOST_DS_SELECTOR, VMCS_HOST_DS_SELECTOR) ⇒ true
| (VMCS_HOST_FS_SELECTOR, VMCS_HOST_FS_SELECTOR) ⇒ true
| (VMCS_HOST_GS_SELECTOR, VMCS_HOST_GS_SELECTOR) ⇒ true
| (VMCS_HOST_TR_SELECTOR, VMCS_HOST_TR_SELECTOR) ⇒ true
| (VMCS_IO_BITMAP_A, VMCS_IO_BITMAP_A) ⇒ true
| (VMCS_IO_BITMAP_A_HI, VMCS_IO_BITMAP_A_HI) ⇒ true
| (VMCS_IO_BITMAP_B, VMCS_IO_BITMAP_B) ⇒ true
| (VMCS_IO_BITMAP_B_HI, VMCS_IO_BITMAP_B_HI) ⇒ true
| (VMCS_MSR_BITMAP, VMCS_MSR_BITMAP) ⇒ true
| (VMCS_MSR_BITMAP_HI, VMCS_MSR_BITMAP_HI) ⇒ true
| (VMCS_EXIT_MSR_STORE, VMCS_EXIT_MSR_STORE) ⇒ true
| (VMCS_EXIT_MSR_LOAD, VMCS_EXIT_MSR_LOAD) ⇒ true
| (VMCS_ENTRY_MSR_LOAD, VMCS_ENTRY_MSR_LOAD) ⇒ true
| (VMCS_EXECUTIVE_VMCS, VMCS_EXECUTIVE_VMCS) ⇒ true
| (VMCS_TSC_OFFSET, VMCS_TSC_OFFSET) ⇒ true
| (VMCS_VIRTUAL_APIC, VMCS_VIRTUAL_APIC) ⇒ true
| (VMCS_APIC_ACCESS, VMCS_APIC_ACCESS) ⇒ true
| (VMCS_EPTP, VMCS_EPTP) ⇒ true
| (VMCS_EPTP_HI, VMCS_EPTP_HI) ⇒ true
| (VMCS_GUEST_PHYSICAL_ADDRESS, VMCS_GUEST_PHYSICAL_ADDRESS) ⇒ true
| (VMCS_LINK_POINTER, VMCS_LINK_POINTER) ⇒ true
| (VMCS_GUEST_IA32_DEBUGCTL, VMCS_GUEST_IA32_DEBUGCTL) ⇒ true
| (VMCS_GUEST_IA32_PAT, VMCS_GUEST_IA32_PAT) ⇒ true
| (VMCS_GUEST_IA32_EFER, VMCS_GUEST_IA32_EFER) ⇒ true
| (VMCS_GUEST_IA32_PERF_GLOBAL_CTRL , VMCS_GUEST_IA32_PERF_GLOBAL_CTRL ) ⇒ true
| (VMCS_GUEST_PDPTE0, VMCS_GUEST_PDPTE0) ⇒ true
| (VMCS_GUEST_PDPTE1, VMCS_GUEST_PDPTE1) ⇒ true
| (VMCS_GUEST_PDPTE2, VMCS_GUEST_PDPTE2) ⇒ true
| (VMCS_GUEST_PDPTE3, VMCS_GUEST_PDPTE3) ⇒ true
| (VMCS_HOST_IA32_PAT, VMCS_HOST_IA32_PAT) ⇒ true
| (VMCS_HOST_IA32_EFER, VMCS_HOST_IA32_EFER) ⇒ true
| (VMCS_HOST_IA32_PERF_GLOBAL_CTRL, VMCS_HOST_IA32_PERF_GLOBAL_CTRL) ⇒ true
| (VMCS_PIN_BASED_CTLS, VMCS_PIN_BASED_CTLS) ⇒ true
| (VMCS_PRI_PROC_BASED_CTLS, VMCS_PRI_PROC_BASED_CTLS) ⇒ true
| (VMCS_EXCEPTION_BITMAP, VMCS_EXCEPTION_BITMAP) ⇒ true
| (VMCS_PF_ERROR_MASK, VMCS_PF_ERROR_MASK) ⇒ true
| (VMCS_PF_ERROR_MATCH, VMCS_PF_ERROR_MATCH) ⇒ true
| (VMCS_CR3_TARGET_COUNT, VMCS_CR3_TARGET_COUNT) ⇒ true
| (VMCS_EXIT_CTLS, VMCS_EXIT_CTLS) ⇒ true
| (VMCS_EXIT_MSR_STORE_COUNT, VMCS_EXIT_MSR_STORE_COUNT) ⇒ true
| (VMCS_EXIT_MSR_LOAD_COUNT, VMCS_EXIT_MSR_LOAD_COUNT) ⇒ true
| (VMCS_ENTRY_CTLS, VMCS_ENTRY_CTLS) ⇒ true
| (VMCS_ENTRY_MSR_LOAD_COUNT, VMCS_ENTRY_MSR_LOAD_COUNT) ⇒ true
| (VMCS_ENTRY_INTR_INFO, VMCS_ENTRY_INTR_INFO) ⇒ true
| (VMCS_ENTRY_EXCEPTION_ERROR, VMCS_ENTRY_EXCEPTION_ERROR) ⇒ true
| (VMCS_ENTRY_INST_LENGTH, VMCS_ENTRY_INST_LENGTH) ⇒ true
| (VMCS_TPR_THRESHOLD, VMCS_TPR_THRESHOLD) ⇒ true
| (VMCS_SEC_PROC_BASED_CTLS, VMCS_SEC_PROC_BASED_CTLS) ⇒ true
| (VMCS_PLE_GAP, VMCS_PLE_GAP) ⇒ true
| (VMCS_PLE_WINDOW, VMCS_PLE_WINDOW) ⇒ true
| (VMCS_INSTRUCTION_ERROR, VMCS_INSTRUCTION_ERROR) ⇒ true
| (VMCS_EXIT_REASON, VMCS_EXIT_REASON) ⇒ true
| (VMCS_EXIT_INTERRUPTION_INFO, VMCS_EXIT_INTERRUPTION_INFO) ⇒ true
| (VMCS_EXIT_INTERRUPTION_ERROR, VMCS_EXIT_INTERRUPTION_ERROR) ⇒ true
| (VMCS_IDT_VECTORING_INFO, VMCS_IDT_VECTORING_INFO) ⇒ true
| (VMCS_IDT_VECTORING_ERROR, VMCS_IDT_VECTORING_ERROR) ⇒ true
| (VMCS_EXIT_INSTRUCTION_LENGTH, VMCS_EXIT_INSTRUCTION_LENGTH) ⇒ true
| (VMCS_EXIT_INSTRUCTION_INFO, VMCS_EXIT_INSTRUCTION_INFO) ⇒ true
| (VMCS_GUEST_ES_LIMIT, VMCS_GUEST_ES_LIMIT) ⇒ true
| (VMCS_GUEST_CS_LIMIT, VMCS_GUEST_CS_LIMIT) ⇒ true
| (VMCS_GUEST_SS_LIMIT, VMCS_GUEST_SS_LIMIT) ⇒ true
| (VMCS_GUEST_DS_LIMIT, VMCS_GUEST_DS_LIMIT) ⇒ true
| (VMCS_GUEST_FS_LIMIT, VMCS_GUEST_FS_LIMIT) ⇒ true
| (VMCS_GUEST_GS_LIMIT, VMCS_GUEST_GS_LIMIT) ⇒ true
| (VMCS_GUEST_LDTR_LIMIT, VMCS_GUEST_LDTR_LIMIT) ⇒ true
| (VMCS_GUEST_TR_LIMIT, VMCS_GUEST_TR_LIMIT) ⇒ true
| (VMCS_GUEST_GDTR_LIMIT, VMCS_GUEST_GDTR_LIMIT) ⇒ true
| (VMCS_GUEST_IDTR_LIMIT, VMCS_GUEST_IDTR_LIMIT) ⇒ true
| (VMCS_GUEST_ES_ACCESS_RIGHTS, VMCS_GUEST_ES_ACCESS_RIGHTS) ⇒ true
| (VMCS_GUEST_CS_ACCESS_RIGHTS, VMCS_GUEST_CS_ACCESS_RIGHTS) ⇒ true
| (VMCS_GUEST_SS_ACCESS_RIGHTS, VMCS_GUEST_SS_ACCESS_RIGHTS) ⇒ true
| (VMCS_GUEST_DS_ACCESS_RIGHTS, VMCS_GUEST_DS_ACCESS_RIGHTS) ⇒ true
| (VMCS_GUEST_FS_ACCESS_RIGHTS, VMCS_GUEST_FS_ACCESS_RIGHTS) ⇒ true
| (VMCS_GUEST_GS_ACCESS_RIGHTS, VMCS_GUEST_GS_ACCESS_RIGHTS) ⇒ true
| (VMCS_GUEST_LDTR_ACCESS_RIGHTS, VMCS_GUEST_LDTR_ACCESS_RIGHTS) ⇒ true
| (VMCS_GUEST_TR_ACCESS_RIGHTS, VMCS_GUEST_TR_ACCESS_RIGHTS) ⇒ true
| (VMCS_GUEST_INTERRUPTIBILITY, VMCS_GUEST_INTERRUPTIBILITY) ⇒ true
| (VMCS_GUEST_ACTIVITY, VMCS_GUEST_ACTIVITY) ⇒ true
| (VMCS_GUEST_SMBASE, VMCS_GUEST_SMBASE) ⇒ true
| (VMCS_GUEST_IA32_SYSENTER_CS, VMCS_GUEST_IA32_SYSENTER_CS) ⇒ true
| (VMCS_PREEMPTION_TIMER_VALUE, VMCS_PREEMPTION_TIMER_VALUE) ⇒ true
| (VMCS_HOST_IA32_SYSENTER_CS, VMCS_HOST_IA32_SYSENTER_CS) ⇒ true
| (VMCS_CR0_MASK, VMCS_CR0_MASK) ⇒ true
| (VMCS_CR4_MASK, VMCS_CR4_MASK) ⇒ true
| (VMCS_CR0_SHADOW, VMCS_CR0_SHADOW) ⇒ true
| (VMCS_CR4_SHADOW, VMCS_CR4_SHADOW) ⇒ true
| (VMCS_CR3_TARGET0, VMCS_CR3_TARGET0) ⇒ true
| (VMCS_CR3_TARGET1, VMCS_CR3_TARGET1) ⇒ true
| (VMCS_CR3_TARGET2, VMCS_CR3_TARGET2) ⇒ true
| (VMCS_CR3_TARGET3, VMCS_CR3_TARGET3) ⇒ true
| (VMCS_EXIT_QUALIFICATION, VMCS_EXIT_QUALIFICATION) ⇒ true
| (VMCS_IO_RCX, VMCS_IO_RCX) ⇒ true
| (VMCS_IO_RSI, VMCS_IO_RSI) ⇒ true
| (VMCS_IO_RDI, VMCS_IO_RDI) ⇒ true
| (VMCS_IO_RIP, VMCS_IO_RIP) ⇒ true
| (VMCS_GUEST_LINEAR_ADDRESS, VMCS_GUEST_LINEAR_ADDRESS) ⇒ true
| (VMCS_GUEST_CR0, VMCS_GUEST_CR0) ⇒ true
| (VMCS_GUEST_CR3, VMCS_GUEST_CR3) ⇒ true
| (VMCS_GUEST_CR4, VMCS_GUEST_CR4) ⇒ true
| (VMCS_GUEST_ES_BASE, VMCS_GUEST_ES_BASE) ⇒ true
| (VMCS_GUEST_CS_BASE, VMCS_GUEST_CS_BASE) ⇒ true
| (VMCS_GUEST_SS_BASE, VMCS_GUEST_SS_BASE) ⇒ true
| (VMCS_GUEST_DS_BASE, VMCS_GUEST_DS_BASE) ⇒ true
| (VMCS_GUEST_FS_BASE, VMCS_GUEST_FS_BASE) ⇒ true
| (VMCS_GUEST_GS_BASE, VMCS_GUEST_GS_BASE) ⇒ true
| (VMCS_GUEST_LDTR_BASE, VMCS_GUEST_LDTR_BASE) ⇒ true
| (VMCS_GUEST_TR_BASE, VMCS_GUEST_TR_BASE) ⇒ true
| (VMCS_GUEST_GDTR_BASE, VMCS_GUEST_GDTR_BASE) ⇒ true
| (VMCS_GUEST_IDTR_BASE, VMCS_GUEST_IDTR_BASE) ⇒ true
| (VMCS_GUEST_DR7, VMCS_GUEST_DR7) ⇒ true
| (VMCS_GUEST_RSP, VMCS_GUEST_RSP) ⇒ true
| (VMCS_GUEST_RIP, VMCS_GUEST_RIP) ⇒ true
| (VMCS_GUEST_RFLAGS, VMCS_GUEST_RFLAGS) ⇒ true
| (VMCS_GUEST_PENDING_DBG_EXCEPTIONS, VMCS_GUEST_PENDING_DBG_EXCEPTIONS) ⇒ true
| (VMCS_GUEST_IA32_SYSENTER_ESP, VMCS_GUEST_IA32_SYSENTER_ESP) ⇒ true
| (VMCS_GUEST_IA32_SYSENTER_EIP, VMCS_GUEST_IA32_SYSENTER_EIP) ⇒ true
| (VMCS_HOST_CR0, VMCS_HOST_CR0) ⇒ true
| (VMCS_HOST_CR3, VMCS_HOST_CR3) ⇒ true
| (VMCS_HOST_CR4, VMCS_HOST_CR4) ⇒ true
| (VMCS_HOST_FS_BASE, VMCS_HOST_FS_BASE) ⇒ true
| (VMCS_HOST_GS_BASE, VMCS_HOST_GS_BASE) ⇒ true
| (VMCS_HOST_TR_BASE, VMCS_HOST_TR_BASE) ⇒ true
| (VMCS_HOST_GDTR_BASE, VMCS_HOST_GDTR_BASE) ⇒ true
| (VMCS_HOST_IDTR_BASE, VMCS_HOST_IDTR_BASE) ⇒ true
| (VMCS_HOST_IA32_SYSENTER_ESP, VMCS_HOST_IA32_SYSENTER_ESP) ⇒ true
| (VMCS_HOST_IA32_SYSENTER_EIP, VMCS_HOST_IA32_SYSENTER_EIP) ⇒ true
| (VMCS_HOST_RSP, VMCS_HOST_RSP) ⇒ true
| (VMCS_HOST_RIP, VMCS_HOST_RIP) ⇒ true
|(_, _) ⇒ false
end.
Lemma vmcs_encoding_Z_eq:
∀ z e, vmcs_ZtoEncoding z = Some e ↔
z = vmcs_EncodingtoZ e.
Proof.
split.
- functional inversion 1; trivial.
- induction e; intros; subst; trivial.
Qed.
Lemma vmcs_encoding_Z_eq_r:
∀ e, vmcs_ZtoEncoding (vmcs_EncodingtoZ e) = Some e.
Proof.
intros. destruct e; trivial.
Qed.
Lemma vmcs_ZtoEncoding_range:
∀ z e, vmcs_ZtoEncoding z = Some e →
(0 ≤ z ≤ 27670)%Z.
Proof.
functional inversion 1; omega.
Qed.
Inductive VMCS :=
| VMCSValid (revid: val) (abrtid: val) (data: ZMap.t val).
Definition VMCSPool := ZMap.t VMCS.
Inductive VMCS_inj : meminj → VMCS → VMCS → Prop :=
| VMCS_INJ_INTRO:
∀ f r a v v´,
(∀ i,
val_inject f (ZMap.get i v) (ZMap.get i v´))
→ VMCS_inj f (VMCSValid r a v) (VMCSValid r a v´).
Definition VMCSPool_inj (f: meminj) (vmcspool1: VMCSPool) (vmcspool2: VMCSPool) :=
∀ vmid vmcs1 vmcs2,
0 ≤ vmid < NUM_VMS
→ ZMap.get vmid vmcspool1 = vmcs1
→ ZMap.get vmid vmcspool2 = vmcs2
→ VMCS_inj f vmcs1 vmcs2.
Inductive VMCS_inject_neutral :VMCS → block → Prop :=
| VMCS_inject_neutral_INTRO:
∀ r a d n,
(∀ ofs,
let v := ZMap.get ofs d in
Val.has_type v Tint
∧ val_inject (Mem.flat_inj n) v v)
→ VMCS_inject_neutral (VMCSValid r a d) n.
Definition VMCSPool_inject_neutral (vmcspool: VMCSPool) (n: block) :=
∀ vmid vmcs,
0 ≤ vmid < NUM_VMS
→ ZMap.get vmid vmcspool = vmcs
→ VMCS_inject_neutral vmcs n.
Inductive FieldWidth :=
W16 | W32 | W64.
Function field_width_beq (a b: FieldWidth) :=
match (a, b) with
| (W16, W16) ⇒ true
| (W32, W32) ⇒ true
| (W64, W64) ⇒ true
| (_, _) ⇒ false
end.
Definition vmcs_filed_width_by_encoding (encoding: VMCS_Encoding): FieldWidth :=
match encoding with
| VMCS_VPID ⇒ W16
| VMCS_GUEST_ES_SELECTOR ⇒ W16
| VMCS_GUEST_CS_SELECTOR ⇒ W16
| VMCS_GUEST_SS_SELECTOR ⇒ W16
| VMCS_GUEST_DS_SELECTOR ⇒ W16
| VMCS_GUEST_FS_SELECTOR ⇒ W16
| VMCS_GUEST_GS_SELECTOR ⇒ W16
| VMCS_GUEST_LDTR_SELECTOR ⇒ W16
| VMCS_GUEST_TR_SELECTOR ⇒ W16
| VMCS_HOST_ES_SELECTOR ⇒ W16
| VMCS_HOST_CS_SELECTOR ⇒ W16
| VMCS_HOST_SS_SELECTOR ⇒ W16
| VMCS_HOST_DS_SELECTOR ⇒ W16
| VMCS_HOST_FS_SELECTOR ⇒ W16
| VMCS_HOST_GS_SELECTOR ⇒ W16
| VMCS_HOST_TR_SELECTOR ⇒ W16
| VMCS_IO_BITMAP_A ⇒ W64
| VMCS_IO_BITMAP_A_HI ⇒ W64
| VMCS_IO_BITMAP_B ⇒ W64
| VMCS_IO_BITMAP_B_HI ⇒ W64
| VMCS_MSR_BITMAP ⇒ W64
| VMCS_MSR_BITMAP_HI ⇒ W64
| VMCS_EXIT_MSR_STORE ⇒ W16
| VMCS_EXIT_MSR_LOAD ⇒ W16
| VMCS_ENTRY_MSR_LOAD ⇒ W16
| VMCS_EXECUTIVE_VMCS ⇒ W16
| VMCS_TSC_OFFSET ⇒ W16
| VMCS_VIRTUAL_APIC ⇒ W16
| VMCS_APIC_ACCESS ⇒ W16
| VMCS_EPTP ⇒ W64
| VMCS_EPTP_HI ⇒ W64
| VMCS_GUEST_PHYSICAL_ADDRESS ⇒ W64
| VMCS_LINK_POINTER ⇒ W64
| VMCS_GUEST_IA32_DEBUGCTL ⇒ W64
| VMCS_GUEST_IA32_PAT ⇒ W64
| VMCS_GUEST_IA32_EFER ⇒ W64
| VMCS_GUEST_IA32_PERF_GLOBAL_CTRL ⇒ W64
| VMCS_GUEST_PDPTE0 ⇒ W64
| VMCS_GUEST_PDPTE1 ⇒ W64
| VMCS_GUEST_PDPTE2 ⇒ W64
| VMCS_GUEST_PDPTE3 ⇒ W64
| VMCS_HOST_IA32_PAT ⇒ W64
| VMCS_HOST_IA32_EFER ⇒ W64
| VMCS_HOST_IA32_PERF_GLOBAL_CTRL ⇒ W64
| VMCS_PIN_BASED_CTLS ⇒ W32
| VMCS_PRI_PROC_BASED_CTLS ⇒ W32
| VMCS_EXCEPTION_BITMAP ⇒ W32
| VMCS_PF_ERROR_MASK ⇒ W32
| VMCS_PF_ERROR_MATCH ⇒ W32
| VMCS_CR3_TARGET_COUNT ⇒ W32
| VMCS_EXIT_CTLS ⇒ W32
| VMCS_EXIT_MSR_STORE_COUNT ⇒ W32
| VMCS_EXIT_MSR_LOAD_COUNT ⇒ W32
| VMCS_ENTRY_CTLS ⇒ W32
| VMCS_ENTRY_MSR_LOAD_COUNT ⇒ W32
| VMCS_ENTRY_INTR_INFO ⇒ W32
| VMCS_ENTRY_EXCEPTION_ERROR ⇒ W32
| VMCS_ENTRY_INST_LENGTH ⇒ W32
| VMCS_TPR_THRESHOLD ⇒ W32
| VMCS_SEC_PROC_BASED_CTLS ⇒ W32
| VMCS_PLE_GAP ⇒ W32
| VMCS_PLE_WINDOW ⇒ W32
| VMCS_INSTRUCTION_ERROR ⇒ W32
| VMCS_EXIT_REASON ⇒ W32
| VMCS_EXIT_INTERRUPTION_INFO ⇒ W32
| VMCS_EXIT_INTERRUPTION_ERROR ⇒ W32
| VMCS_IDT_VECTORING_INFO ⇒ W32
| VMCS_IDT_VECTORING_ERROR ⇒ W32
| VMCS_EXIT_INSTRUCTION_LENGTH ⇒ W32
| VMCS_EXIT_INSTRUCTION_INFO ⇒ W32
| VMCS_GUEST_ES_LIMIT ⇒ W32
| VMCS_GUEST_CS_LIMIT ⇒ W32
| VMCS_GUEST_SS_LIMIT ⇒ W32
| VMCS_GUEST_DS_LIMIT ⇒ W32
| VMCS_GUEST_FS_LIMIT ⇒ W32
| VMCS_GUEST_GS_LIMIT ⇒ W32
| VMCS_GUEST_LDTR_LIMIT ⇒ W32
| VMCS_GUEST_TR_LIMIT ⇒ W32
| VMCS_GUEST_GDTR_LIMIT ⇒ W32
| VMCS_GUEST_IDTR_LIMIT ⇒ W32
| VMCS_GUEST_ES_ACCESS_RIGHTS ⇒ W32
| VMCS_GUEST_CS_ACCESS_RIGHTS ⇒ W32
| VMCS_GUEST_SS_ACCESS_RIGHTS ⇒ W32
| VMCS_GUEST_DS_ACCESS_RIGHTS ⇒ W32
| VMCS_GUEST_FS_ACCESS_RIGHTS ⇒ W32
| VMCS_GUEST_GS_ACCESS_RIGHTS ⇒ W32
| VMCS_GUEST_LDTR_ACCESS_RIGHTS ⇒ W32
| VMCS_GUEST_TR_ACCESS_RIGHTS ⇒ W32
| VMCS_GUEST_INTERRUPTIBILITY ⇒ W32
| VMCS_GUEST_ACTIVITY ⇒ W32
| VMCS_GUEST_SMBASE ⇒ W32
| VMCS_GUEST_IA32_SYSENTER_CS ⇒ W32
| VMCS_PREEMPTION_TIMER_VALUE ⇒ W32
| VMCS_HOST_IA32_SYSENTER_CS ⇒ W32
| VMCS_CR0_MASK ⇒ W32
| VMCS_CR4_MASK ⇒ W32
| VMCS_CR0_SHADOW ⇒ W32
| VMCS_CR4_SHADOW ⇒ W32
| VMCS_CR3_TARGET0 ⇒ W32
| VMCS_CR3_TARGET1 ⇒ W32
| VMCS_CR3_TARGET2 ⇒ W32
| VMCS_CR3_TARGET3 ⇒ W32
| VMCS_EXIT_QUALIFICATION ⇒ W32
| VMCS_IO_RCX ⇒ W32
| VMCS_IO_RSI ⇒ W32
| VMCS_IO_RDI ⇒ W32
| VMCS_IO_RIP ⇒ W32
| VMCS_GUEST_LINEAR_ADDRESS ⇒ W32
| VMCS_GUEST_CR0 ⇒ W32
| VMCS_GUEST_CR3 ⇒ W32
| VMCS_GUEST_CR4 ⇒ W32
| VMCS_GUEST_ES_BASE ⇒ W32
| VMCS_GUEST_CS_BASE ⇒ W32
| VMCS_GUEST_SS_BASE ⇒ W32
| VMCS_GUEST_DS_BASE ⇒ W32
| VMCS_GUEST_FS_BASE ⇒ W32
| VMCS_GUEST_GS_BASE ⇒ W32
| VMCS_GUEST_LDTR_BASE ⇒ W32
| VMCS_GUEST_TR_BASE ⇒ W32
| VMCS_GUEST_GDTR_BASE ⇒ W32
| VMCS_GUEST_IDTR_BASE ⇒ W32
| VMCS_GUEST_DR7 ⇒ W32
| VMCS_GUEST_RSP ⇒ W32
| VMCS_GUEST_RIP ⇒ W32
| VMCS_GUEST_RFLAGS ⇒ W32
| VMCS_GUEST_PENDING_DBG_EXCEPTIONS ⇒ W32
| VMCS_GUEST_IA32_SYSENTER_ESP ⇒ W32
| VMCS_GUEST_IA32_SYSENTER_EIP ⇒ W32
| VMCS_HOST_CR0 ⇒ W32
| VMCS_HOST_CR3 ⇒ W32
| VMCS_HOST_CR4 ⇒ W32
| VMCS_HOST_FS_BASE ⇒ W32
| VMCS_HOST_GS_BASE ⇒ W32
| VMCS_HOST_TR_BASE ⇒ W32
| VMCS_HOST_GDTR_BASE ⇒ W32
| VMCS_HOST_IDTR_BASE ⇒ W32
| VMCS_HOST_IA32_SYSENTER_ESP ⇒ W32
| VMCS_HOST_IA32_SYSENTER_EIP ⇒ W32
| VMCS_HOST_RSP ⇒ W32
| VMCS_HOST_RIP ⇒ W32
end.
Inductive FieldPerm :=
ReadOnly | WriteOnly | ReadWrite.
Definition vmcs_wr_permission_by_encoding (encoding: VMCS_Encoding): FieldPerm :=
match encoding with
| VMCS_VPID ⇒ ReadWrite
| VMCS_GUEST_ES_SELECTOR ⇒ ReadWrite
| VMCS_GUEST_CS_SELECTOR ⇒ ReadWrite
| VMCS_GUEST_SS_SELECTOR ⇒ ReadWrite
| VMCS_GUEST_DS_SELECTOR ⇒ ReadWrite
| VMCS_GUEST_FS_SELECTOR ⇒ ReadWrite
| VMCS_GUEST_GS_SELECTOR ⇒ ReadWrite
| VMCS_GUEST_LDTR_SELECTOR ⇒ ReadWrite
| VMCS_GUEST_TR_SELECTOR ⇒ ReadWrite
| VMCS_HOST_ES_SELECTOR ⇒ ReadWrite
| VMCS_HOST_CS_SELECTOR ⇒ ReadWrite
| VMCS_HOST_SS_SELECTOR ⇒ ReadWrite
| VMCS_HOST_DS_SELECTOR ⇒ ReadWrite
| VMCS_HOST_FS_SELECTOR ⇒ ReadWrite
| VMCS_HOST_GS_SELECTOR ⇒ ReadWrite
| VMCS_HOST_TR_SELECTOR ⇒ ReadWrite
| VMCS_IO_BITMAP_A ⇒ ReadWrite
| VMCS_IO_BITMAP_A_HI ⇒ ReadWrite
| VMCS_IO_BITMAP_B ⇒ ReadWrite
| VMCS_IO_BITMAP_B_HI ⇒ ReadWrite
| VMCS_MSR_BITMAP ⇒ ReadWrite
| VMCS_MSR_BITMAP_HI ⇒ ReadWrite
| VMCS_EXIT_MSR_STORE ⇒ ReadWrite
| VMCS_EXIT_MSR_LOAD ⇒ ReadWrite
| VMCS_ENTRY_MSR_LOAD ⇒ ReadWrite
| VMCS_EXECUTIVE_VMCS ⇒ ReadWrite
| VMCS_TSC_OFFSET ⇒ ReadWrite
| VMCS_VIRTUAL_APIC ⇒ ReadWrite
| VMCS_APIC_ACCESS ⇒ ReadWrite
| VMCS_EPTP ⇒ ReadWrite
| VMCS_EPTP_HI ⇒ ReadWrite
| VMCS_GUEST_PHYSICAL_ADDRESS ⇒ ReadOnly
| VMCS_LINK_POINTER ⇒ ReadWrite
| VMCS_GUEST_IA32_DEBUGCTL ⇒ ReadWrite
| VMCS_GUEST_IA32_PAT ⇒ ReadWrite
| VMCS_GUEST_IA32_EFER ⇒ ReadWrite
| VMCS_GUEST_IA32_PERF_GLOBAL_CTRL ⇒ ReadWrite
| VMCS_GUEST_PDPTE0 ⇒ ReadWrite
| VMCS_GUEST_PDPTE1 ⇒ ReadWrite
| VMCS_GUEST_PDPTE2 ⇒ ReadWrite
| VMCS_GUEST_PDPTE3 ⇒ ReadWrite
| VMCS_HOST_IA32_PAT ⇒ ReadWrite
| VMCS_HOST_IA32_EFER ⇒ ReadWrite
| VMCS_HOST_IA32_PERF_GLOBAL_CTRL ⇒ ReadWrite
| VMCS_PIN_BASED_CTLS ⇒ ReadWrite
| VMCS_PRI_PROC_BASED_CTLS ⇒ ReadWrite
| VMCS_EXCEPTION_BITMAP ⇒ ReadWrite
| VMCS_PF_ERROR_MASK ⇒ ReadWrite
| VMCS_PF_ERROR_MATCH ⇒ ReadWrite
| VMCS_CR3_TARGET_COUNT ⇒ ReadWrite
| VMCS_EXIT_CTLS ⇒ ReadWrite
| VMCS_EXIT_MSR_STORE_COUNT ⇒ ReadWrite
| VMCS_EXIT_MSR_LOAD_COUNT ⇒ ReadWrite
| VMCS_ENTRY_CTLS ⇒ ReadWrite
| VMCS_ENTRY_MSR_LOAD_COUNT ⇒ ReadWrite
| VMCS_ENTRY_INTR_INFO ⇒ ReadWrite
| VMCS_ENTRY_EXCEPTION_ERROR ⇒ ReadWrite
| VMCS_ENTRY_INST_LENGTH ⇒ ReadWrite
| VMCS_TPR_THRESHOLD ⇒ ReadWrite
| VMCS_SEC_PROC_BASED_CTLS ⇒ ReadWrite
| VMCS_PLE_GAP ⇒ ReadWrite
| VMCS_PLE_WINDOW ⇒ ReadWrite
| VMCS_INSTRUCTION_ERROR ⇒ ReadOnly
| VMCS_EXIT_REASON ⇒ ReadOnly
| VMCS_EXIT_INTERRUPTION_INFO ⇒ ReadOnly
| VMCS_EXIT_INTERRUPTION_ERROR ⇒ ReadOnly
| VMCS_IDT_VECTORING_INFO ⇒ ReadOnly
| VMCS_IDT_VECTORING_ERROR ⇒ ReadOnly
| VMCS_EXIT_INSTRUCTION_LENGTH ⇒ ReadOnly
| VMCS_EXIT_INSTRUCTION_INFO ⇒ ReadOnly
| VMCS_GUEST_ES_LIMIT ⇒ ReadWrite
| VMCS_GUEST_CS_LIMIT ⇒ ReadWrite
| VMCS_GUEST_SS_LIMIT ⇒ ReadWrite
| VMCS_GUEST_DS_LIMIT ⇒ ReadWrite
| VMCS_GUEST_FS_LIMIT ⇒ ReadWrite
| VMCS_GUEST_GS_LIMIT ⇒ ReadWrite
| VMCS_GUEST_LDTR_LIMIT ⇒ ReadWrite
| VMCS_GUEST_TR_LIMIT ⇒ ReadWrite
| VMCS_GUEST_GDTR_LIMIT ⇒ ReadWrite
| VMCS_GUEST_IDTR_LIMIT ⇒ ReadWrite
| VMCS_GUEST_ES_ACCESS_RIGHTS ⇒ ReadWrite
| VMCS_GUEST_CS_ACCESS_RIGHTS ⇒ ReadWrite
| VMCS_GUEST_SS_ACCESS_RIGHTS ⇒ ReadWrite
| VMCS_GUEST_DS_ACCESS_RIGHTS ⇒ ReadWrite
| VMCS_GUEST_FS_ACCESS_RIGHTS ⇒ ReadWrite
| VMCS_GUEST_GS_ACCESS_RIGHTS ⇒ ReadWrite
| VMCS_GUEST_LDTR_ACCESS_RIGHTS ⇒ ReadWrite
| VMCS_GUEST_TR_ACCESS_RIGHTS ⇒ ReadWrite
| VMCS_GUEST_INTERRUPTIBILITY ⇒ ReadWrite
| VMCS_GUEST_ACTIVITY ⇒ ReadWrite
| VMCS_GUEST_SMBASE ⇒ ReadWrite
| VMCS_GUEST_IA32_SYSENTER_CS ⇒ ReadWrite
| VMCS_PREEMPTION_TIMER_VALUE ⇒ ReadWrite
| VMCS_HOST_IA32_SYSENTER_CS ⇒ ReadWrite
| VMCS_CR0_MASK ⇒ ReadWrite
| VMCS_CR4_MASK ⇒ ReadWrite
| VMCS_CR0_SHADOW ⇒ ReadWrite
| VMCS_CR4_SHADOW ⇒ ReadWrite
| VMCS_CR3_TARGET0 ⇒ ReadWrite
| VMCS_CR3_TARGET1 ⇒ ReadWrite
| VMCS_CR3_TARGET2 ⇒ ReadWrite
| VMCS_CR3_TARGET3 ⇒ ReadWrite
| VMCS_EXIT_QUALIFICATION ⇒ ReadOnly
| VMCS_IO_RCX ⇒ ReadOnly
| VMCS_IO_RSI ⇒ ReadOnly
| VMCS_IO_RDI ⇒ ReadOnly
| VMCS_IO_RIP ⇒ ReadOnly
| VMCS_GUEST_LINEAR_ADDRESS ⇒ ReadOnly
| VMCS_GUEST_CR0 ⇒ ReadWrite
| VMCS_GUEST_CR3 ⇒ ReadWrite
| VMCS_GUEST_CR4 ⇒ ReadWrite
| VMCS_GUEST_ES_BASE ⇒ ReadWrite
| VMCS_GUEST_CS_BASE ⇒ ReadWrite
| VMCS_GUEST_SS_BASE ⇒ ReadWrite
| VMCS_GUEST_DS_BASE ⇒ ReadWrite
| VMCS_GUEST_FS_BASE ⇒ ReadWrite
| VMCS_GUEST_GS_BASE ⇒ ReadWrite
| VMCS_GUEST_LDTR_BASE ⇒ ReadWrite
| VMCS_GUEST_TR_BASE ⇒ ReadWrite
| VMCS_GUEST_GDTR_BASE ⇒ ReadWrite
| VMCS_GUEST_IDTR_BASE ⇒ ReadWrite
| VMCS_GUEST_DR7 ⇒ ReadWrite
| VMCS_GUEST_RSP ⇒ ReadWrite
| VMCS_GUEST_RIP ⇒ ReadWrite
| VMCS_GUEST_RFLAGS ⇒ ReadWrite
| VMCS_GUEST_PENDING_DBG_EXCEPTIONS ⇒ ReadWrite
| VMCS_GUEST_IA32_SYSENTER_ESP ⇒ ReadWrite
| VMCS_GUEST_IA32_SYSENTER_EIP ⇒ ReadWrite
| VMCS_HOST_CR0 ⇒ ReadWrite
| VMCS_HOST_CR3 ⇒ ReadWrite
| VMCS_HOST_CR4 ⇒ ReadWrite
| VMCS_HOST_FS_BASE ⇒ ReadWrite
| VMCS_HOST_GS_BASE ⇒ ReadWrite
| VMCS_HOST_TR_BASE ⇒ ReadWrite
| VMCS_HOST_GDTR_BASE ⇒ ReadWrite
| VMCS_HOST_IDTR_BASE ⇒ ReadWrite
| VMCS_HOST_IA32_SYSENTER_ESP ⇒ ReadWrite
| VMCS_HOST_IA32_SYSENTER_EIP ⇒ ReadWrite
| VMCS_HOST_RSP ⇒ ReadWrite
| VMCS_HOST_RIP ⇒ ReadWrite
end.
End VMCSDEF.
Section VMXDEF.
Definition VMX := ZMap.t val.
Definition VMXPool := ZMap.t VMX.
Inductive VMX_inj : meminj → VMX → VMX → Prop :=
| VMX_INJ_INTRO:
∀ f v v´,
(∀ i,
val_inject f (ZMap.get i v) (ZMap.get i v´))
→ VMX_inj f v v´.
Definition VMXPool_inj (f: meminj) (vmxpool1: VMXPool) (vmxpool2: VMXPool) :=
∀ vmid vmx1 vmx2,
0 ≤ vmid < NUM_VMS
→ ZMap.get vmid vmxpool1 = vmx1
→ ZMap.get vmid vmxpool2 = vmx2
→ VMX_inj f vmx1 vmx2.
Inductive VMX_inject_neutral :VMX → block → Prop :=
| VMX_inject_neutral_INTRO:
∀ d n,
(∀ ofs,
let v := ZMap.get ofs d in
Val.has_type v Tint
∧ val_inject (Mem.flat_inj n) v v)
→ VMX_inject_neutral d n.
Definition VMXPool_inject_neutral (vmxpool: VMXPool) (n: block) :=
∀ vmid vmx,
0 ≤ vmid < NUM_VMS
→ ZMap.get vmid vmxpool = vmx
→ VMX_inject_neutral vmx n.
End VMXDEF.
End IntelVirtManagement.
Section NEW_IPC.
Definition PageBuffer := list int.
Definition PageBufferPool := ZMap.t PageBuffer.
Definition page_buffer_init: PageBufferPool := ZMap.init nil.
End NEW_IPC.