Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import MemoryX.
Require Import Events.
Require Import EventsX.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import Locations.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import Errors.
Require Import Op.
Require Import Smallstep.
Require Import AuxLemma.
Require Import AuxStateDataType.
Require Import GenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import Clight.
Require Import CDataTypes.
Require Import CLemmas.
Require Import XOmega.
Require Import ZArith.
Require Import TacticsForTesting.
Require Import CommonTactic.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import Ctypes.
Require Import VMPower.Spec.
Require Import AbsMachine.Spec.
Require Import MemOps.Spec.
Require Import Ident.
Require Import SmmuOps.Layer.
Require Import VCPUOpsAux.Spec.
Require Import RData.
Require Import BootOps.Spec.
Require Import Constants.
Require Import HypsecCommLib.
Require Import VCPUOpsAux.Code.
Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.
Section VCPUOpsAuxProofLow.
Context `{real_params: RealParams}.
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}.
Section reset_gp_regs_proof.
Let L : compatlayer (cdata RData) :=
get_int_pc ↦ gensem get_int_pc_spec
⊕ search_load_info ↦ gensem search_load_info_spec
⊕ clear_shadow_gp_regs ↦ gensem clear_shadow_gp_regs_spec
⊕ get_int_pstate ↦ gensem get_int_pstate_spec
⊕ set_shadow_ctxt ↦ gensem set_shadow_ctxt_spec
⊕ reset_fp_regs ↦ gensem reset_fp_regs_spec
⊕ panic ↦ gensem panic_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_get_int_pc: block.
Hypothesis h_get_int_pc_s : Genv.find_symbol ge get_int_pc = Some b_get_int_pc.
Hypothesis h_get_int_pc_p : Genv.find_funct_ptr ge b_get_int_pc
= Some (External (EF_external get_int_pc
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tulong cc_default))
(Tcons tuint (Tcons tuint Tnil)) tulong cc_default).
Variable b_search_load_info: block.
Hypothesis h_search_load_info_s : Genv.find_symbol ge search_load_info = Some b_search_load_info.
Hypothesis h_search_load_info_p : Genv.find_funct_ptr ge b_search_load_info
= Some (External (EF_external search_load_info
(signature_of_type (Tcons tuint (Tcons tulong Tnil)) tulong cc_default))
(Tcons tuint (Tcons tulong Tnil)) tulong cc_default).
Variable b_clear_shadow_gp_regs: block.
Hypothesis h_clear_shadow_gp_regs_s : Genv.find_symbol ge clear_shadow_gp_regs = Some b_clear_shadow_gp_regs.
Hypothesis h_clear_shadow_gp_regs_p : Genv.find_funct_ptr ge b_clear_shadow_gp_regs
= Some (External (EF_external clear_shadow_gp_regs
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tvoid cc_default))
(Tcons tuint (Tcons tuint Tnil)) tvoid cc_default).
Variable b_get_int_pstate: block.
Hypothesis h_get_int_pstate_s : Genv.find_symbol ge get_int_pstate = Some b_get_int_pstate.
Hypothesis h_get_int_pstate_p : Genv.find_funct_ptr ge b_get_int_pstate
= Some (External (EF_external get_int_pstate
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tulong cc_default))
(Tcons tuint (Tcons tuint Tnil)) tulong cc_default).
Variable b_set_shadow_ctxt: block.
Hypothesis h_set_shadow_ctxt_s : Genv.find_symbol ge set_shadow_ctxt = Some b_set_shadow_ctxt.
Hypothesis h_set_shadow_ctxt_p : Genv.find_funct_ptr ge b_set_shadow_ctxt
= Some (External (EF_external set_shadow_ctxt
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default).
Variable b_reset_fp_regs: block.
Hypothesis h_reset_fp_regs_s : Genv.find_symbol ge reset_fp_regs = Some b_reset_fp_regs.
Hypothesis h_reset_fp_regs_p : Genv.find_funct_ptr ge b_reset_fp_regs
= Some (External (EF_external reset_fp_regs
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tvoid cc_default))
(Tcons tuint (Tcons tuint Tnil)) tvoid cc_default).
Variable b_panic: block.
Hypothesis h_panic_s : Genv.find_symbol ge panic = Some b_panic.
Hypothesis h_panic_p : Genv.find_funct_ptr ge b_panic
= Some (External (EF_external panic
(signature_of_type Tnil tvoid cc_default))
Tnil tvoid cc_default).
Lemma reset_gp_regs_body_correct:
forall m d d' env le vmid vcpuid
(Henv: env = PTree.empty _)
(HPTvmid: PTree.get _vmid le = Some (Vint vmid))
(HPTvcpuid: PTree.get _vcpuid le = Some (Vint vcpuid))
(Hinv: high_level_invariant d)
(Hspec: reset_gp_regs_spec0 (Int.unsigned vmid) (Int.unsigned vcpuid) d = Some d'),
exists le', (exec_stmt ge env le ((m, d): mem) reset_gp_regs_body E0 le' (m, d') Out_normal).
Proof.
solve_code_proof Hspec reset_gp_regs_body; eexists; solve_proof_low.
Qed.
End BodyProof.
Theorem reset_gp_regs_code_correct:
spec_le (reset_gp_regs ↦ reset_gp_regs_spec_low) (〚 reset_gp_regs ↦ f_reset_gp_regs 〛 L).
Proof.
set (L' := L) in *.
unfold L in *.
fbigstep_pre L'.
fbigstep (reset_gp_regs_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp b4 Hb4fs Hb4fp b5 Hb5fs Hb5fp b6 Hb6fs Hb6fp m'0 labd labd'
(PTree.empty _) (bind_parameter_temps' (fn_params f_reset_gp_regs ) (Vint vmid :: Vint vcpuid :: nil)
(create_undef_temps (fn_temps f_reset_gp_regs)))) hinv.
Qed.
End reset_gp_regs_proof.
Section reset_sys_regs_proof.
Let L : compatlayer (cdata RData) :=
get_sys_reg_desc_val ↦ gensem get_sys_reg_desc_val_spec
⊕ read_actlr_el1 ↦ gensem read_actlr_el1_spec
⊕ set_shadow_ctxt ↦ gensem set_shadow_ctxt_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_get_sys_reg_desc_val: block.
Hypothesis h_get_sys_reg_desc_val_s : Genv.find_symbol ge get_sys_reg_desc_val = Some b_get_sys_reg_desc_val.
Hypothesis h_get_sys_reg_desc_val_p : Genv.find_funct_ptr ge b_get_sys_reg_desc_val
= Some (External (EF_external get_sys_reg_desc_val
(signature_of_type (Tcons tuint Tnil) tulong cc_default))
(Tcons tuint Tnil) tulong cc_default).
Variable b_read_actlr_el1: block.
Hypothesis h_read_actlr_el1_s : Genv.find_symbol ge read_actlr_el1 = Some b_read_actlr_el1.
Hypothesis h_read_actlr_el1_p : Genv.find_funct_ptr ge b_read_actlr_el1
= Some (External (EF_external read_actlr_el1
(signature_of_type Tnil tulong cc_default))
Tnil tulong cc_default).
Variable b_set_shadow_ctxt: block.
Hypothesis h_set_shadow_ctxt_s : Genv.find_symbol ge set_shadow_ctxt = Some b_set_shadow_ctxt.
Hypothesis h_set_shadow_ctxt_p : Genv.find_funct_ptr ge b_set_shadow_ctxt
= Some (External (EF_external set_shadow_ctxt
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default).
Lemma reset_sys_regs_body_correct:
forall m d d' env le vmid vcpuid
(Henv: env = PTree.empty _)
(HPTvmid: PTree.get _vmid le = Some (Vint vmid))
(HPTvcpuid: PTree.get _vcpuid le = Some (Vint vcpuid))
(Hinv: high_level_invariant d)
(Hspec: reset_sys_regs_spec0 (Int.unsigned vmid) (Int.unsigned vcpuid) d = Some d'),
exists le', (exec_stmt ge env le ((m, d): mem) reset_sys_regs_body E0 le' (m, d') Out_normal).
Proof.
solve_code_proof Hspec reset_sys_regs_body; eexists; repeat sstep.
Local Opaque get_sys_reg_desc_val_spec set_shadow_ctxt_spec.
get_loop_body.
set (Hloop := C1).
remember
(PTree.set _i (Vint (Int.repr 60))
(PTree.set _num (Vint (Int.repr 63))) le)
as le_loop.
remember 63 as num.
set (P := fun le0 m0 => m0 = (m, d) /\ le0 = le_loop).
set (Q := fun le0 m0 => m0 = (m, d') /\ le0 ! _vmid = Some (Vint vmid)).
set (Inv := fun le0 m0 n => exists idx1 adt1,
reset_sys_regs_loop0 (Z.to_nat (num - n)) 60 (Int.unsigned vmid * 16 + Int.unsigned vcpuid)
(Int.unsigned vcpuid) d = Some (adt1, Int.unsigned idx1) /\
m0 = (m, adt1) /\ 0 <= n /\ n <= num /\ le0 ! _i = Some (Vint idx1) /\
le0 ! _vcpuid = Some (Vint vcpuid) /\ le0 ! _num = Some (Vint (Int.repr n)) /\
le0 ! _ctxtid = Some (Vint (Int.repr (Int.unsigned vmid * 16 + Int.unsigned vcpuid)))).
assert(loop_succ: forall N, Z.of_nat N <= num -> exists idx' adt',
reset_sys_regs_loop0 (Z.to_nat (num - Z.of_nat N)) 60 (Int.unsigned vmid * 16 + Int.unsigned vcpuid)
(Int.unsigned vcpuid) d = Some (adt', Int.unsigned idx')).
{ add_int Hloop z; try somega.
induction N. rewrite Z.sub_0_r. rewrite Hloop. intros. repeat eexists; reflexivity.
intro C. erewrite loop_ind_sub1 in IHN; try omega.
rewrite Nat2Z.inj_succ, succ_plus_1 in C.
assert(Hcc: Z.of_nat N <= num) by omega.
apply IHN in Hcc. destruct Hcc as (? & ? & Hnext).
Local Opaque Z.of_nat. simpl in Hnext. clear Heqle_loop.
simpl_func Hnext; try add_int' z0; repeat eexists; try somega. }
assert (T: LoopProofSimpleWhile.t (external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops L) cond body ge (PTree.empty _) P Q).
{ apply LoopProofSimpleWhile.make with (W:=Z) (lt:=fun z1 z2 => (0 <= z2 /\ z1 < z2)) (I:=Inv).
- apply Zwf_well_founded.
- unfold P, Inv. intros ? ? C. destruct C as [C1 C2].
rewrite C2 in *. exists num.
replace (num - num) with 0 by omega. simpl.
rewrite Heqle_loop in *. repeat eexists; first [reflexivity|assumption|repeat sstep].
add_int' 60; try somega. reflexivity.
- intros ? ? ? I. unfold Inv in I. destruct I as (? & ? & ? & ? & ? & ? & ? & ? & ? & ?).
set (Hnow := H2).
rewrite Heqbody, Heqcond in *.
destruct (n >? 0) eqn:Hn; bool_rel.
+ eexists. eexists. split_and.
* sstep.
* repeat sstep.
* intro C. inversion C.
* assert(Hlx: Z.of_nat (Z.to_nat (n-1)) <= num) by (rewrite Z2Nat.id; omega).
apply loop_succ in Hlx. rewrite Z2Nat.id in Hlx; try omega.
intro. destruct Hlx as (? & ? & Hnext). duplicate Hnext.
rewrite loop_nat_sub1 in Hnext; try somega.
simpl in Hnext. rewrite Hnow in Hnext.
autounfold in Hnext; repeat simpl_hyp Hnext; repeat destruct_con; bool_rel; contra; inversion Hnext.
assert((4294967295 / 65536)=65535) by reflexivity.
assert((4294967295 / 256)=16777215) by reflexivity.
assert((2147483647 / 65536)=32767) by reflexivity.
assert((2147483647 / 256)=8388607) by reflexivity.
assert((4294967295 / 2)=2147483647) by reflexivity.
assert((2147483647 / 2)=1073741823) by reflexivity.
rewrite H17, H18 in *; eexists; eexists; split; [repeat sstep|
exists (n-1); split; [split; sstep| repeat sstep; unfold Inv; repeat eexists; first[eassumption|repeat sstep]]].
rewrite H15.
rewrite H35, H36 in *; eexists; eexists; split; [repeat sstep|
exists (n-1); split; [split; sstep| repeat sstep; unfold Inv; repeat eexists; first[eassumption|repeat sstep]]].
+ eexists. eexists. split_and.
* sstep.
* repeat sstep.
* intro. unfold Q.
assert (n=0) by omega. clear Heqle_loop. subst.
sstep. rewrite Hloop in Hnow. inv Hnow.
split_and; first[reflexivity|repeat sstep].
* intro C. inversion C. }
assert (Pre: P le_loop (m, r)) by (split; reflexivity).
pose proof (LoopProofSimpleWhile.termination _ _ _ _ _ _ T _ (m, r) Pre) as LoopProof.
destruct LoopProof as (le' & m' & (exec & Post)).
unfold exec_stmt in exec. rewrite Heqle_loop in exec.
unfold Q in Post. destruct Post as (Hm' & ?). rewrite Hm' in exec.
rewrite Heqbody, Heqcond, Heqle_loop in *.
eexists. big_vcgen.
step_code_proof. step_code_proof.
somega. big_vcgen. step_code_proof.
step_code_proof. step_code_proof.
somega. repeat sstep.
big_vcgen. big_vcgen.
step_code_proof.
Qed.
End BodyProof.
Theorem reset_sys_regs_code_correct:
spec_le (reset_sys_regs ↦ reset_sys_regs_spec_low) (〚 reset_sys_regs ↦ f_reset_sys_regs 〛 L).
Proof.
set (L' := L) in *.
unfold L in *.
fbigstep_pre L'.
fbigstep (reset_sys_regs_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m'0 labd labd'
(PTree.empty _) (bind_parameter_temps' (fn_params f_reset_sys_regs ) (Vint vmid :: Vint vcpuid :: nil)
(create_undef_temps (fn_temps f_reset_sys_regs)))) hinv.
Qed.
End reset_sys_regs_proof.
Section sync_dirty_to_shadow_proof.
Let L : compatlayer (cdata RData) :=
get_shadow_dirty_bit ↦ gensem get_shadow_dirty_bit_spec
⊕ get_int_gpr ↦ gensem get_int_gpr_spec
⊕ set_shadow_ctxt ↦ gensem set_shadow_ctxt_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_get_shadow_dirty_bit: block.
Hypothesis h_get_shadow_dirty_bit_s : Genv.find_symbol ge get_shadow_dirty_bit = Some b_get_shadow_dirty_bit.
Hypothesis h_get_shadow_dirty_bit_p : Genv.find_funct_ptr ge b_get_shadow_dirty_bit
= Some (External (EF_external get_shadow_dirty_bit
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tulong cc_default))
(Tcons tuint (Tcons tuint Tnil)) tulong cc_default).
Variable b_get_int_gpr: block.
Hypothesis h_get_int_gpr_s : Genv.find_symbol ge get_int_gpr = Some b_get_int_gpr.
Hypothesis h_get_int_gpr_p : Genv.find_funct_ptr ge b_get_int_gpr
= Some (External (EF_external get_int_gpr
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tulong cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tulong cc_default).
Variable b_set_shadow_ctxt: block.
Hypothesis h_set_shadow_ctxt_s : Genv.find_symbol ge set_shadow_ctxt = Some b_set_shadow_ctxt.
Hypothesis h_set_shadow_ctxt_p : Genv.find_funct_ptr ge b_set_shadow_ctxt
= Some (External (EF_external set_shadow_ctxt
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default).
Lemma sync_dirty_to_shadow_body_correct:
forall m d d' env le vmid vcpuid
(Henv: env = PTree.empty _)
(HPTvmid: PTree.get _vmid le = Some (Vint vmid))
(HPTvcpuid: PTree.get _vcpuid le = Some (Vint vcpuid))
(Hinv: high_level_invariant d)
(Hspec: sync_dirty_to_shadow_spec0 (Int.unsigned vmid) (Int.unsigned vcpuid) d = Some d'),
exists le', (exec_stmt ge env le ((m, d): mem) sync_dirty_to_shadow_body E0 le' (m, d') Out_normal).
Proof.
solve_code_proof Hspec sync_dirty_to_shadow_body; eexists; solve_proof_low.
Qed.
End BodyProof.
Theorem sync_dirty_to_shadow_code_correct:
spec_le (sync_dirty_to_shadow ↦ sync_dirty_to_shadow_spec_low) (〚 sync_dirty_to_shadow ↦ f_sync_dirty_to_shadow 〛 L).
Proof.
set (L' := L) in *.
unfold L in *.
fbigstep_pre L'.
fbigstep (sync_dirty_to_shadow_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m'0 labd labd'
(PTree.empty _) (bind_parameter_temps' (fn_params f_sync_dirty_to_shadow ) (Vint vmid :: Vint vcpuid :: nil)
(create_undef_temps (fn_temps f_sync_dirty_to_shadow)))) hinv.
Qed.
End sync_dirty_to_shadow_proof.
Section prep_wfx_proof.
Let L : compatlayer (cdata RData) :=
set_shadow_dirty_bit ↦ gensem set_shadow_dirty_bit_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_set_shadow_dirty_bit: block.
Hypothesis h_set_shadow_dirty_bit_s : Genv.find_symbol ge set_shadow_dirty_bit = Some b_set_shadow_dirty_bit.
Hypothesis h_set_shadow_dirty_bit_p : Genv.find_funct_ptr ge b_set_shadow_dirty_bit
= Some (External (EF_external set_shadow_dirty_bit
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tulong Tnil))) tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tulong Tnil))) tvoid cc_default).
Lemma prep_wfx_body_correct:
forall m d d' env le vmid vcpuid
(Henv: env = PTree.empty _)
(HPTvmid: PTree.get _vmid le = Some (Vint vmid))
(HPTvcpuid: PTree.get _vcpuid le = Some (Vint vcpuid))
(Hinv: high_level_invariant d)
(Hspec: prep_wfx_spec0 (Int.unsigned vmid) (Int.unsigned vcpuid) d = Some d'),
exists le', (exec_stmt ge env le ((m, d): mem) prep_wfx_body E0 le' (m, d') Out_normal).
Proof.
solve_code_proof Hspec prep_wfx_body; eexists; solve_proof_low.
Qed.
End BodyProof.
Theorem prep_wfx_code_correct:
spec_le (prep_wfx ↦ prep_wfx_spec_low) (〚 prep_wfx ↦ f_prep_wfx 〛 L).
Proof.
set (L' := L) in *.
unfold L in *.
fbigstep_pre L'.
fbigstep (prep_wfx_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp m'0 labd labd'
(PTree.empty _) (bind_parameter_temps' (fn_params f_prep_wfx ) (Vint vmid :: Vint vcpuid :: nil)
(create_undef_temps (fn_temps f_prep_wfx)))) hinv.
Qed.
End prep_wfx_proof.
Section prep_hvc_proof.
Let L : compatlayer (cdata RData) :=
set_shadow_dirty_bit ↦ gensem set_shadow_dirty_bit_spec
⊕ set_int_gpr ↦ gensem set_int_gpr_spec
⊕ get_shadow_ctxt ↦ gensem get_shadow_ctxt_spec
⊕ set_vm_poweroff ↦ gensem set_vm_poweroff_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_set_shadow_dirty_bit: block.
Hypothesis h_set_shadow_dirty_bit_s : Genv.find_symbol ge set_shadow_dirty_bit = Some b_set_shadow_dirty_bit.
Hypothesis h_set_shadow_dirty_bit_p : Genv.find_funct_ptr ge b_set_shadow_dirty_bit
= Some (External (EF_external set_shadow_dirty_bit
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tulong Tnil))) tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tulong Tnil))) tvoid cc_default).
Variable b_set_int_gpr: block.
Hypothesis h_set_int_gpr_s : Genv.find_symbol ge set_int_gpr = Some b_set_int_gpr.
Hypothesis h_set_int_gpr_p : Genv.find_funct_ptr ge b_set_int_gpr
= Some (External (EF_external set_int_gpr
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default).
Variable b_get_shadow_ctxt: block.
Hypothesis h_get_shadow_ctxt_s : Genv.find_symbol ge get_shadow_ctxt = Some b_get_shadow_ctxt.
Hypothesis h_get_shadow_ctxt_p : Genv.find_funct_ptr ge b_get_shadow_ctxt
= Some (External (EF_external get_shadow_ctxt
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tulong cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tulong cc_default).
Variable b_set_vm_poweroff: block.
Hypothesis h_set_vm_poweroff_s : Genv.find_symbol ge set_vm_poweroff = Some b_set_vm_poweroff.
Hypothesis h_set_vm_poweroff_p : Genv.find_funct_ptr ge b_set_vm_poweroff
= Some (External (EF_external set_vm_poweroff
(signature_of_type (Tcons tuint Tnil) tvoid cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Lemma prep_hvc_body_correct:
forall m d d' env le vmid vcpuid
(Henv: env = PTree.empty _)
(HPTvmid: PTree.get _vmid le = Some (Vint vmid))
(HPTvcpuid: PTree.get _vcpuid le = Some (Vint vcpuid))
(Hinv: high_level_invariant d)
(Hspec: prep_hvc_spec0 (Int.unsigned vmid) (Int.unsigned vcpuid) d = Some d'),
exists le', (exec_stmt ge env le ((m, d): mem) prep_hvc_body E0 le' (m, d') Out_normal).
Proof.
solve_code_proof Hspec prep_hvc_body; eexists; solve_proof_low.
Qed.
End BodyProof.
Theorem prep_hvc_code_correct:
spec_le (prep_hvc ↦ prep_hvc_spec_low) (〚 prep_hvc ↦ f_prep_hvc 〛 L).
Proof.
set (L' := L) in *.
unfold L in *.
fbigstep_pre L'.
fbigstep (prep_hvc_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp m'0 labd labd'
(PTree.empty _) (bind_parameter_temps' (fn_params f_prep_hvc ) (Vint vmid :: Vint vcpuid :: nil)
(create_undef_temps (fn_temps f_prep_hvc)))) hinv.
Qed.
End prep_hvc_proof.
Section prep_abort_proof.
Let L : compatlayer (cdata RData) :=
get_int_esr ↦ gensem get_int_esr_spec
⊕ get_shadow_ctxt ↦ gensem get_shadow_ctxt_spec
⊕ set_shadow_dirty_bit ↦ gensem set_shadow_dirty_bit_spec
⊕ set_int_gpr ↦ gensem set_int_gpr_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_get_int_esr: block.
Hypothesis h_get_int_esr_s : Genv.find_symbol ge get_int_esr = Some b_get_int_esr.
Hypothesis h_get_int_esr_p : Genv.find_funct_ptr ge b_get_int_esr
= Some (External (EF_external get_int_esr
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tulong cc_default))
(Tcons tuint (Tcons tuint Tnil)) tulong cc_default).
Variable b_get_shadow_ctxt: block.
Hypothesis h_get_shadow_ctxt_s : Genv.find_symbol ge get_shadow_ctxt = Some b_get_shadow_ctxt.
Hypothesis h_get_shadow_ctxt_p : Genv.find_funct_ptr ge b_get_shadow_ctxt
= Some (External (EF_external get_shadow_ctxt
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tulong cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tulong cc_default).
Variable b_set_shadow_dirty_bit: block.
Hypothesis h_set_shadow_dirty_bit_s : Genv.find_symbol ge set_shadow_dirty_bit = Some b_set_shadow_dirty_bit.
Hypothesis h_set_shadow_dirty_bit_p : Genv.find_funct_ptr ge b_set_shadow_dirty_bit
= Some (External (EF_external set_shadow_dirty_bit
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tulong Tnil))) tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tulong Tnil))) tvoid cc_default).
Variable b_set_int_gpr: block.
Hypothesis h_set_int_gpr_s : Genv.find_symbol ge set_int_gpr = Some b_set_int_gpr.
Hypothesis h_set_int_gpr_p : Genv.find_funct_ptr ge b_set_int_gpr
= Some (External (EF_external set_int_gpr
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default).
Lemma prep_abort_body_correct:
forall m d d' env le vmid vcpuid
(Henv: env = PTree.empty _)
(HPTvmid: PTree.get _vmid le = Some (Vint vmid))
(HPTvcpuid: PTree.get _vcpuid le = Some (Vint vcpuid))
(Hinv: high_level_invariant d)
(Hspec: prep_abort_spec0 (Int.unsigned vmid) (Int.unsigned vcpuid) d = Some d'),
exists le', (exec_stmt ge env le ((m, d): mem) prep_abort_body E0 le' (m, d') Out_normal).
Proof.
solve_code_proof Hspec prep_abort_body; eexists; solve_proof_low.
Qed.
End BodyProof.
Theorem prep_abort_code_correct:
spec_le (prep_abort ↦ prep_abort_spec_low) (〚 prep_abort ↦ f_prep_abort 〛 L).
Proof.
set (L' := L) in *.
unfold L in *.
fbigstep_pre L'.
fbigstep (prep_abort_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp m'0 labd labd'
(PTree.empty _) (bind_parameter_temps' (fn_params f_prep_abort ) (Vint vmid :: Vint vcpuid :: nil)
(create_undef_temps (fn_temps f_prep_abort)))) hinv.
Qed.
End prep_abort_proof.
Section update_exception_gp_regs_proof.
Let L : compatlayer (cdata RData) :=
get_shadow_ctxt ↦ gensem get_shadow_ctxt_spec
⊕ get_exception_vector ↦ gensem get_exception_vector_spec
⊕ set_shadow_ctxt ↦ gensem set_shadow_ctxt_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_get_shadow_ctxt: block.
Hypothesis h_get_shadow_ctxt_s : Genv.find_symbol ge get_shadow_ctxt = Some b_get_shadow_ctxt.
Hypothesis h_get_shadow_ctxt_p : Genv.find_funct_ptr ge b_get_shadow_ctxt
= Some (External (EF_external get_shadow_ctxt
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tulong cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tulong cc_default).
Variable b_get_exception_vector: block.
Hypothesis h_get_exception_vector_s : Genv.find_symbol ge get_exception_vector = Some b_get_exception_vector.
Hypothesis h_get_exception_vector_p : Genv.find_funct_ptr ge b_get_exception_vector
= Some (External (EF_external get_exception_vector
(signature_of_type (Tcons tulong Tnil) tulong cc_default))
(Tcons tulong Tnil) tulong cc_default).
Variable b_set_shadow_ctxt: block.
Hypothesis h_set_shadow_ctxt_s : Genv.find_symbol ge set_shadow_ctxt = Some b_set_shadow_ctxt.
Hypothesis h_set_shadow_ctxt_p : Genv.find_funct_ptr ge b_set_shadow_ctxt
= Some (External (EF_external set_shadow_ctxt
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint (Tcons tulong Tnil)))) tvoid cc_default).
Lemma update_exception_gp_regs_body_correct:
forall m d d' env le vmid vcpuid
(Henv: env = PTree.empty _)
(HPTvmid: PTree.get _vmid le = Some (Vint vmid))
(HPTvcpuid: PTree.get _vcpuid le = Some (Vint vcpuid))
(Hinv: high_level_invariant d)
(Hspec: update_exception_gp_regs_spec0 (Int.unsigned vmid) (Int.unsigned vcpuid) d = Some d'),
exists le', (exec_stmt ge env le ((m, d): mem) update_exception_gp_regs_body E0 le' (m, d') Out_normal).
Proof.
solve_code_proof Hspec update_exception_gp_regs_body; eexists; solve_proof_low.
Qed.
End BodyProof.
Theorem update_exception_gp_regs_code_correct:
spec_le (update_exception_gp_regs ↦ update_exception_gp_regs_spec_low) (〚 update_exception_gp_regs ↦ f_update_exception_gp_regs 〛 L).
Proof.
set (L' := L) in *.
unfold L in *.
fbigstep_pre L'.
fbigstep (update_exception_gp_regs_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m'0 labd labd'
(PTree.empty _) (bind_parameter_temps' (fn_params f_update_exception_gp_regs ) (Vint vmid :: Vint vcpuid :: nil)
(create_undef_temps (fn_temps f_update_exception_gp_regs)))) hinv.
Qed.
End update_exception_gp_regs_proof.
Section post_handle_shadow_s2pt_fault_proof.
Let L : compatlayer (cdata RData) :=
get_int_new_pte ↦ gensem get_int_new_pte_spec
⊕ get_int_new_pte ↦ gensem get_int_new_pte_spec
⊕ prot_and_map_vm_s2pt ↦ gensem prot_and_map_vm_s2pt_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_get_int_new_pte: block.
Hypothesis h_get_int_new_pte_s : Genv.find_symbol ge get_int_new_pte = Some b_get_int_new_pte.
Hypothesis h_get_int_new_pte_p : Genv.find_funct_ptr ge b_get_int_new_pte
= Some (External (EF_external get_int_new_pte
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tulong cc_default))
(Tcons tuint (Tcons tuint Tnil)) tulong cc_default).
Variable b_get_int_new_pte: block.
Hypothesis h_get_int_new_pte_s : Genv.find_symbol ge get_int_new_pte = Some b_get_int_new_pte.
Hypothesis h_get_int_new_pte_p : Genv.find_funct_ptr ge b_get_int_new_pte
= Some (External (EF_external get_int_new_pte
(signature_of_type (Tcons tuint (Tcons tuint Tnil)) tulong cc_default))
(Tcons tuint (Tcons tuint Tnil)) tulong cc_default).
Variable b_prot_and_map_vm_s2pt: block.
Hypothesis h_prot_and_map_vm_s2pt_s : Genv.find_symbol ge prot_and_map_vm_s2pt = Some b_prot_and_map_vm_s2pt.
Hypothesis h_prot_and_map_vm_s2pt_p : Genv.find_funct_ptr ge b_prot_and_map_vm_s2pt
= Some (External (EF_external prot_and_map_vm_s2pt
(signature_of_type (Tcons tuint (Tcons tulong (Tcons tulong (Tcons tuint Tnil)))) tvoid cc_default))
(Tcons tuint (Tcons tulong (Tcons tulong (Tcons tuint Tnil)))) tvoid cc_default).
Lemma post_handle_shadow_s2pt_fault_body_correct:
forall m d d' env le vmid vcpuid addr
(Henv: env = PTree.empty _)
(HPTvmid: PTree.get _vmid le = Some (Vint vmid))
(HPTvcpuid: PTree.get _vcpuid le = Some (Vint vcpuid))
(HPTaddr: PTree.get _addr le = Some (Vlong addr))
(Hinv: high_level_invariant d)
(Hspec: post_handle_shadow_s2pt_fault_spec0 (Int.unsigned vmid) (Int.unsigned vcpuid) (VZ64 (Int64.unsigned addr)) d = Some d'),
exists le', (exec_stmt ge env le ((m, d): mem) post_handle_shadow_s2pt_fault_body E0 le' (m, d') Out_normal).
Proof.
solve_code_proof Hspec post_handle_shadow_s2pt_fault_body; eexists; solve_proof_low.
Qed.
End BodyProof.
Theorem post_handle_shadow_s2pt_fault_code_correct:
spec_le (post_handle_shadow_s2pt_fault ↦ post_handle_shadow_s2pt_fault_spec_low) (〚 post_handle_shadow_s2pt_fault ↦ f_post_handle_shadow_s2pt_fault 〛 L).
Proof.
set (L' := L) in *.
unfold L in *.
fbigstep_pre L'.
fbigstep (post_handle_shadow_s2pt_fault_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m'0 labd labd'
(PTree.empty _) (bind_parameter_temps' (fn_params f_post_handle_shadow_s2pt_fault ) (Vint vmid :: Vint vcpuid :: Vlong addr :: nil)
(create_undef_temps (fn_temps f_post_handle_shadow_s2pt_fault)))) hinv.
Qed.
End post_handle_shadow_s2pt_fault_proof.
End VCPUOpsAuxProofLow.