Library mcertikos.proc.VVMCSIntroCodeSetDesc
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import VMCSInitGenSpec.
Require Import ObjVMCS.
Require Import VVMCSIntroCSource.
Require Import VVMCSIntro.
Hint Resolve Int.unsigned_range_2.
Hint Resolve CLemmas.Z_lor_range_lo.
Hint Resolve Z_lor_range.
Function unsigned64 (x : int64) : Z64 :=
VZ64 (Int64.unsigned x).
Function unpack64 (x: Z64): Z :=
match x with
| VZ64 z ⇒ z
end.
Function repr64 (x : Z64) : int64 :=
Int64.repr (unpack64 x).
Lemma unsigned64_repr: ∀ x: Z64,
0 ≤ unpack64(x) ≤ Int64.max_unsigned →
unsigned64 (repr64 x) = x.
Proof.
unfold repr64, unpack64, unsigned64.
intros. destruct x. rewrite Int64.unsigned_repr; auto.
Qed.
Print Int64.repr_unsigned.
Lemma repr64_unsigned: ∀ x: int64,
repr64 (unsigned64 x) = x.
Proof.
unfold repr64, unpack64, unsigned64.
apply Int64.repr_unsigned.
Qed.
Module VMCSINTROCODESETDESC.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Section VMXSETDESC2.
Let L: compatlayer (cdata RData) :=
vmcs_writez ↦ gensem vmcs_writez_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXSetDesc2Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import VMCSInitGenSpec.
Require Import ObjVMCS.
Require Import VVMCSIntroCSource.
Require Import VVMCSIntro.
Hint Resolve Int.unsigned_range_2.
Hint Resolve CLemmas.Z_lor_range_lo.
Hint Resolve Z_lor_range.
Function unsigned64 (x : int64) : Z64 :=
VZ64 (Int64.unsigned x).
Function unpack64 (x: Z64): Z :=
match x with
| VZ64 z ⇒ z
end.
Function repr64 (x : Z64) : int64 :=
Int64.repr (unpack64 x).
Lemma unsigned64_repr: ∀ x: Z64,
0 ≤ unpack64(x) ≤ Int64.max_unsigned →
unsigned64 (repr64 x) = x.
Proof.
unfold repr64, unpack64, unsigned64.
intros. destruct x. rewrite Int64.unsigned_repr; auto.
Qed.
Print Int64.repr_unsigned.
Lemma repr64_unsigned: ∀ x: int64,
repr64 (unsigned64 x) = x.
Proof.
unfold repr64, unpack64, unsigned64.
apply Int64.repr_unsigned.
Qed.
Module VMCSINTROCODESETDESC.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Section VMXSETDESC2.
Let L: compatlayer (cdata RData) :=
vmcs_writez ↦ gensem vmcs_writez_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXSetDesc2Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmcs_writez
Variable bvmcs_writez: block.
Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez =
let arg_type := (Tcons tint (Tcons tint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
Some (External (EF_external vmcs_writez
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_set_desc2_body_correct:
∀ m d d´ env le seg lim ar,
env = PTree.empty _ →
PTree.get _seg le = Some (Vint seg) →
PTree.get _lim le = Some (Vint lim) →
PTree.get _ar le = Some (Vint ar) →
True →
True →
vmx_set_desc2_spec (Int.unsigned seg) (Int.unsigned lim)
(Int.unsigned ar) d = Some d´ →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_set_desc2_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
assert(evval: Int.unsigned seg = C_GUEST_CS ∨
Int.unsigned seg = C_GUEST_DS ∨
Int.unsigned seg = C_GUEST_ES ∨
Int.unsigned seg = C_GUEST_FS ∨
Int.unsigned seg = C_GUEST_GS ∨
Int.unsigned seg = C_GUEST_SS ∨
Int.unsigned seg = C_GUEST_LDTR ∨
Int.unsigned seg = C_GUEST_TR ∨
Int.unsigned seg = C_GUEST_GDTR ∨
Int.unsigned seg = C_GUEST_IDTR ∨
Int.unsigned seg > C_GUEST_IDTR).
{
generalize (Int.unsigned_range seg); intro.
repeat autounfold in H.
unfold two_power_nat in H.
unfold shift_nat in H.
simpl in H.
omega.
}
assert (
ihost d = true ∧ pg d = true ∧ ikern d = true
∧ ∃ revid, ∃ abrtid, ∃ m,
ZMap.get (CPU_ID d) (vmcs d)
= VMCSValid revid abrtid m).
{
functional inversion H5; subst.
split; (assumption || split; (assumption || split; (assumption || idtac))).
∃ revid, abrtid, d0; assumption.
}
assert (CPU_range: 0 ≤ (CPU_ID d) < 8).
{ inv H6; auto. }
assert (vmcs_double_update: ∀ vmcspool vmcspool´,
d {vmcs : vmcspool} {vmcs: vmcspool´} =
d {vmcs : vmcspool´}).
{ unfold update_vmcs.
simpl.
auto. }
destruct H as [Hh [Hp [Hk Hd]]].
destruct Hd.
destruct H.
destruct H.
destruct evval as [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | evval]]]]]]]]]].
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
reflexivity.
- functional inversion H5;
functional inversion H14;
functional inversion H16; omega.
Qed.
End VMXSetDesc2Body.
Theorem vmx_set_desc2_body__code_correct:
spec_le
(vmx_set_desc2 ↦ vmx_set_desc2_spec_low)
(〚vmx_set_desc2 ↦ f_vmx_set_desc2 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
Require Import TacticsForTesting.
fbigsteptest
(vmx_set_desc2_body_correct
s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_set_desc2)
(Vint seg :: Vint lim :: Vint ar :: nil)
(create_undef_temps (fn_temps f_vmx_set_desc2))
)
) H0; try discriminate.
intro tmpH; destruct tmpH as [le´ stmt].
repeat fbigstep_post.
Qed.
End VMXSETDESC2.
Section VMXSETDESC1.
Let L: compatlayer (cdata RData) :=
vmcs_writez ↦ gensem vmcs_writez_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXSetDesc1Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez =
let arg_type := (Tcons tint (Tcons tint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
Some (External (EF_external vmcs_writez
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_set_desc2_body_correct:
∀ m d d´ env le seg lim ar,
env = PTree.empty _ →
PTree.get _seg le = Some (Vint seg) →
PTree.get _lim le = Some (Vint lim) →
PTree.get _ar le = Some (Vint ar) →
True →
True →
vmx_set_desc2_spec (Int.unsigned seg) (Int.unsigned lim)
(Int.unsigned ar) d = Some d´ →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_set_desc2_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
assert(evval: Int.unsigned seg = C_GUEST_CS ∨
Int.unsigned seg = C_GUEST_DS ∨
Int.unsigned seg = C_GUEST_ES ∨
Int.unsigned seg = C_GUEST_FS ∨
Int.unsigned seg = C_GUEST_GS ∨
Int.unsigned seg = C_GUEST_SS ∨
Int.unsigned seg = C_GUEST_LDTR ∨
Int.unsigned seg = C_GUEST_TR ∨
Int.unsigned seg = C_GUEST_GDTR ∨
Int.unsigned seg = C_GUEST_IDTR ∨
Int.unsigned seg > C_GUEST_IDTR).
{
generalize (Int.unsigned_range seg); intro.
repeat autounfold in H.
unfold two_power_nat in H.
unfold shift_nat in H.
simpl in H.
omega.
}
assert (
ihost d = true ∧ pg d = true ∧ ikern d = true
∧ ∃ revid, ∃ abrtid, ∃ m,
ZMap.get (CPU_ID d) (vmcs d)
= VMCSValid revid abrtid m).
{
functional inversion H5; subst.
split; (assumption || split; (assumption || split; (assumption || idtac))).
∃ revid, abrtid, d0; assumption.
}
assert (CPU_range: 0 ≤ (CPU_ID d) < 8).
{ inv H6; auto. }
assert (vmcs_double_update: ∀ vmcspool vmcspool´,
d {vmcs : vmcspool} {vmcs: vmcspool´} =
d {vmcs : vmcspool´}).
{ unfold update_vmcs.
simpl.
auto. }
destruct H as [Hh [Hp [Hk Hd]]].
destruct Hd.
destruct H.
destruct H.
destruct evval as [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | evval]]]]]]]]]].
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc2_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
reflexivity.
- functional inversion H5;
functional inversion H14;
functional inversion H16; omega.
Qed.
End VMXSetDesc2Body.
Theorem vmx_set_desc2_body__code_correct:
spec_le
(vmx_set_desc2 ↦ vmx_set_desc2_spec_low)
(〚vmx_set_desc2 ↦ f_vmx_set_desc2 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
Require Import TacticsForTesting.
fbigsteptest
(vmx_set_desc2_body_correct
s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_set_desc2)
(Vint seg :: Vint lim :: Vint ar :: nil)
(create_undef_temps (fn_temps f_vmx_set_desc2))
)
) H0; try discriminate.
intro tmpH; destruct tmpH as [le´ stmt].
repeat fbigstep_post.
Qed.
End VMXSETDESC2.
Section VMXSETDESC1.
Let L: compatlayer (cdata RData) :=
vmcs_writez ↦ gensem vmcs_writez_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section VMXSetDesc1Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmcs_writez
Variable bvmcs_writez: block.
Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez =
let arg_type := (Tcons tint (Tcons tint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
Some (External (EF_external vmcs_writez
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_set_desc1_body_correct:
∀ m d d´ env le seg sel base,
env = PTree.empty _ →
PTree.get _seg le = Some (Vint seg) →
PTree.get _sel le = Some (Vint sel) →
PTree.get _base le = Some (Vint base) →
True →
True →
vmx_set_desc1_spec (Int.unsigned seg) (Int.unsigned sel)
(Int.unsigned base) d = Some d´ →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_set_desc1_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
assert(evval: Int.unsigned seg = C_GUEST_CS ∨
Int.unsigned seg = C_GUEST_DS ∨
Int.unsigned seg = C_GUEST_ES ∨
Int.unsigned seg = C_GUEST_FS ∨
Int.unsigned seg = C_GUEST_GS ∨
Int.unsigned seg = C_GUEST_SS ∨
Int.unsigned seg = C_GUEST_LDTR ∨
Int.unsigned seg = C_GUEST_TR ∨
Int.unsigned seg = C_GUEST_GDTR ∨
Int.unsigned seg = C_GUEST_IDTR ∨
Int.unsigned seg > C_GUEST_IDTR).
{
generalize (Int.unsigned_range seg); intro.
repeat autounfold in H.
unfold two_power_nat in H.
unfold shift_nat in H.
simpl in H.
omega.
}
assert (
ihost d = true ∧ pg d = true ∧ ikern d = true
∧ ∃ revid, ∃ abrtid, ∃ m,
ZMap.get (CPU_ID d) (vmcs d)
= VMCSValid revid abrtid m).
{
functional inversion H5; subst.
split; (assumption || split; (assumption || split; (assumption || idtac))).
∃ revid, abrtid, d0; assumption.
}
assert (CPU_range: 0 ≤ (CPU_ID d) < 8).
{ inv H6; auto. }
assert (vmcs_double_update: ∀ vmcspool vmcspool´,
d {vmcs : vmcspool} {vmcs: vmcspool´} =
d {vmcs : vmcspool´}).
{ unfold update_vmcs.
simpl.
auto. }
destruct H as [Hh [Hp [Hk Hd]]].
destruct Hd.
destruct H.
destruct H.
destruct evval as [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | evval]]]]]]]]]].
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
reflexivity.
- functional inversion H5;
functional inversion H14;
functional inversion H16; omega.
Qed.
End VMXSetDesc1Body.
Theorem vmx_set_desc1_body__code_correct:
spec_le
(vmx_set_desc1 ↦ vmx_set_desc1_spec_low)
(〚vmx_set_desc1 ↦ f_vmx_set_desc1 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
Require Import TacticsForTesting.
fbigsteptest
(vmx_set_desc1_body_correct
s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_set_desc1)
(Vint seg :: Vint sel :: Vint base :: nil)
(create_undef_temps (fn_temps f_vmx_set_desc1))
)
) H0; try discriminate.
intro tmpH; destruct tmpH as [le´ stmt].
repeat fbigstep_post.
Qed.
End VMXSETDESC1.
End WithPrimitives.
End VMCSINTROCODESETDESC.
Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez =
let arg_type := (Tcons tint (Tcons tint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
Some (External (EF_external vmcs_writez
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Lemma vmx_set_desc1_body_correct:
∀ m d d´ env le seg sel base,
env = PTree.empty _ →
PTree.get _seg le = Some (Vint seg) →
PTree.get _sel le = Some (Vint sel) →
PTree.get _base le = Some (Vint base) →
True →
True →
vmx_set_desc1_spec (Int.unsigned seg) (Int.unsigned sel)
(Int.unsigned base) d = Some d´ →
high_level_invariant d →
kernel_mode d →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_set_desc1_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
assert(evval: Int.unsigned seg = C_GUEST_CS ∨
Int.unsigned seg = C_GUEST_DS ∨
Int.unsigned seg = C_GUEST_ES ∨
Int.unsigned seg = C_GUEST_FS ∨
Int.unsigned seg = C_GUEST_GS ∨
Int.unsigned seg = C_GUEST_SS ∨
Int.unsigned seg = C_GUEST_LDTR ∨
Int.unsigned seg = C_GUEST_TR ∨
Int.unsigned seg = C_GUEST_GDTR ∨
Int.unsigned seg = C_GUEST_IDTR ∨
Int.unsigned seg > C_GUEST_IDTR).
{
generalize (Int.unsigned_range seg); intro.
repeat autounfold in H.
unfold two_power_nat in H.
unfold shift_nat in H.
simpl in H.
omega.
}
assert (
ihost d = true ∧ pg d = true ∧ ikern d = true
∧ ∃ revid, ∃ abrtid, ∃ m,
ZMap.get (CPU_ID d) (vmcs d)
= VMCSValid revid abrtid m).
{
functional inversion H5; subst.
split; (assumption || split; (assumption || split; (assumption || idtac))).
∃ revid, abrtid, d0; assumption.
}
assert (CPU_range: 0 ≤ (CPU_ID d) < 8).
{ inv H6; auto. }
assert (vmcs_double_update: ∀ vmcspool vmcspool´,
d {vmcs : vmcspool} {vmcs: vmcspool´} =
d {vmcs : vmcspool´}).
{ unfold update_vmcs.
simpl.
auto. }
destruct H as [Hh [Hp [Hk Hd]]].
destruct Hd.
destruct H.
destruct H.
destruct evval as [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | [evval | evval]]]]]]]]]].
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
reflexivity.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
rewrite vmcs_double_update.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
reflexivity.
- esplit.
repeat vcgen.
unfold vmcs_writez_spec.
simpl.
rewrite Hk, Hp, Hh.
rewrite zle_lt_true; try omega.
rewrite H.
rewrite evval in H5; simpl in H5.
unfold vmx_set_desc1_spec in H5; simpl in H5.
rewrite Hh, Hp, Hk in H5.
rewrite zle_lt_true in H5; try omega.
rewrite H in H5.
inversion H5.
unfold aux_zmap_4val_set, aux_zmap_2val_set.
repeat rewrite Int.repr_unsigned.
reflexivity.
- functional inversion H5;
functional inversion H14;
functional inversion H16; omega.
Qed.
End VMXSetDesc1Body.
Theorem vmx_set_desc1_body__code_correct:
spec_le
(vmx_set_desc1 ↦ vmx_set_desc1_spec_low)
(〚vmx_set_desc1 ↦ f_vmx_set_desc1 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
Require Import TacticsForTesting.
fbigsteptest
(vmx_set_desc1_body_correct
s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_vmx_set_desc1)
(Vint seg :: Vint sel :: Vint base :: nil)
(create_undef_temps (fn_temps f_vmx_set_desc1))
)
) H0; try discriminate.
intro tmpH; destruct tmpH as [le´ stmt].
repeat fbigstep_post.
Qed.
End VMXSETDESC1.
End WithPrimitives.
End VMCSINTROCODESETDESC.