adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

aarch64 ainvs: adapt hyp lemmas/consts from ARM_HYP 

This is a rough pass over all the vcpu|vppi|vgic items found in ARM_HYP
abstract invariants. Broken items and issues tagged with FIXMEs,
lemmas sorried when possible.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2022-05-26 00:46:34 +10:00 committed by Gerwin Klein
parent 3f85320012
commit 997883e364
18 changed files with 3198 additions and 64 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
proof/invariant-abstract/AARCH64/ArchAcc_AI.thy
View File

@ -947,6 +947,12 @@ lemma set_pt_valid_global:
\<lbrace>\<lambda>_ s. valid_global_refs s\<rbrace>"
by (wp valid_global_refs_cte_lift)
(* FIXME AARCH64: use vcpus_of instead *)
lemma set_pt_no_vcpu[wp]:
"\<lbrace>obj_at (is_vcpu and P) p'\<rbrace> set_pt p pt \<lbrace>\<lambda>_. obj_at (is_vcpu and P) p'\<rbrace>"
unfolding set_pt_def
by (wpsimp wp: set_object_wp_strong simp: obj_at_def is_vcpu_def a_type_def)
lemma set_pt_cur:
"\<lbrace>\<lambda>s. cur_tcb s\<rbrace>
set_pt p pt

467
proof/invariant-abstract/AARCH64/ArchArch_AI.thy
View File

@ -23,6 +23,16 @@ definition
is_aligned base asid_low_bits \<and>
asid_table s (asid_high_bits_of base) = None"
definition
"valid_vcpu_invocation vi \<equiv> case vi of
VCPUSetTCB vcpu_ptr tcb_ptr \<Rightarrow> vcpu_at vcpu_ptr and tcb_at tcb_ptr and
ex_nonz_cap_to vcpu_ptr and ex_nonz_cap_to tcb_ptr
and (\<lambda>s. tcb_ptr \<noteq> idle_thread s)
| VCPUInjectIRQ vcpu_ptr index virq \<Rightarrow> vcpu_at vcpu_ptr
| VCPUReadRegister vcpu_ptr reg \<Rightarrow> vcpu_at vcpu_ptr
| VCPUWriteRegister vcpu_ptr reg val \<Rightarrow> vcpu_at vcpu_ptr
| VCPUAckVPPI vcpu_ptr vppi \<Rightarrow> vcpu_at vcpu_ptr"
lemma safe_parent_strg:
"cte_wp_at (\<lambda>cap. cap = UntypedCap False frame pageBits idx) p s \<and>
descendants_of p (cdt s) = {} \<and>
@ -49,7 +59,8 @@ where
InvokePageTable pti \<Rightarrow> valid_pti pti
| InvokePage pgi \<Rightarrow> valid_page_inv pgi
| InvokeASIDControl aci \<Rightarrow> valid_aci aci
| InvokeASIDPool api \<Rightarrow> valid_apinv api"
| InvokeASIDPool api \<Rightarrow> valid_apinv api
| InvokeVCPU vi \<Rightarrow> valid_vcpu_invocation vi"
lemma check_vp_wpR [wp]:
"\<lbrace>\<lambda>s. vmsz_aligned w sz \<longrightarrow> P () s\<rbrace>
@ -214,6 +225,9 @@ crunch typ_at [wp]:
"\<lambda>s. P (typ_at T p s)"
(wp: crunch_wps simp: crunch_simps ignore: store_pte)
crunch typ_at [wp]: perform_vcpu_invocation "\<lambda>s. P (typ_at T p s)"
(wp: crunch_wps)
lemmas perform_page_table_invocation_typ_ats [wp] =
abs_typ_at_lifts [OF perform_page_table_invocation_typ_at]
@ -223,6 +237,9 @@ lemmas perform_page_invocation_typ_ats [wp] =
lemmas perform_asid_pool_invocation_typ_ats [wp] =
abs_typ_at_lifts [OF perform_asid_pool_invocation_typ_at]
lemmas perform_vcpu_invocation_typ_ats [wp] =
abs_typ_at_lifts [OF perform_vcpu_invocation_typ_at]
lemma perform_asid_control_invocation_tcb_at:
"\<lbrace>invs and valid_aci aci and st_tcb_at active p and
K (\<forall>w a b c. aci = asid_control_invocation.MakePool w a b c \<longrightarrow> w \<noteq> p)\<rbrace>
@ -926,12 +943,355 @@ qed
lemmas aci_invs[wp] =
aci_invs'[where Q=\<top>,simplified hoare_post_taut, OF refl refl refl TrueI TrueI TrueI,simplified]
lemma obj_at_upd2:
"obj_at P t' (s\<lparr>kheap := kheap s(t \<mapsto> v, x \<mapsto> v')\<rparr>) = (if t' = x then P v' else obj_at P t' (s\<lparr>kheap := kheap s(t \<mapsto> v)\<rparr>))"
by (simp add: obj_at_update obj_at_def)
lemma vcpu_invalidate_active_hyp_refs_empty[wp]:
"\<lbrace>obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace> vcpu_invalidate_active \<lbrace>\<lambda>r. obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace>"
unfolding vcpu_invalidate_active_def vcpu_disable_def by wpsimp
lemma as_user_hyp_refs_empty[wp]:
"\<lbrace>obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace> as_user t f \<lbrace>\<lambda>r. obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace>"
unfolding as_user_def
apply (wpsimp wp: set_object_wp)
by (clarsimp simp: get_tcb_Some_ko_at obj_at_def arch_tcb_context_set_def)
lemma dissociate_vcpu_tcb_obj_at_hyp_refs[wp]:
"\<lbrace>\<lambda>s. p \<notin> {t, vr} \<longrightarrow> obj_at (\<lambda>ko. hyp_refs_of ko = {}) p s \<rbrace>
dissociate_vcpu_tcb t vr
\<lbrace>\<lambda>rv s. obj_at (\<lambda>ko. hyp_refs_of ko = {}) p s\<rbrace>"
unfolding dissociate_vcpu_tcb_def
apply (cases "p \<notin> {t, vr}"; clarsimp)
apply (wp arch_thread_set_wp set_vcpu_wp)
apply (clarsimp simp: obj_at_upd2 obj_at_update)
sorry (* FIXME AARCH64 VCPU
apply (wp hoare_drop_imp get_vcpu_wp)+
apply (clarsimp simp: obj_at_upd2 obj_at_update)
apply (erule disjE;
(wp arch_thread_set_wp set_vcpu_wp
| clarsimp simp: obj_at_upd2 obj_at_update)+)
done *)
lemma associate_vcpu_tcb_sym_refs_hyp[wp]:
"\<lbrace>\<lambda>s. sym_refs (state_hyp_refs_of s)\<rbrace> associate_vcpu_tcb vr t \<lbrace>\<lambda>rv s. sym_refs (state_hyp_refs_of s)\<rbrace>"
apply (simp add: associate_vcpu_tcb_def)
apply (wp arch_thread_set_wp set_vcpu_wp | clarsimp)+
apply (rule_tac P="\<lambda>s. ko_at (ArchObj (VCPU v)) vr s \<and>
obj_at (\<lambda>ko. hyp_refs_of ko = {} ) t s \<and>
sym_refs (state_hyp_refs_of s)"
in hoare_triv)
apply (rule_tac Q="\<lambda>rv s. obj_at (\<lambda>ko. hyp_refs_of ko = {} ) vr s \<and>
obj_at (\<lambda>ko. hyp_refs_of ko = {} ) t s \<and>
sym_refs (state_hyp_refs_of s)"
in hoare_post_imp)
apply (clarsimp dest!: get_tcb_SomeD simp: obj_at_def)
apply (clarsimp simp add: sym_refs_def)
apply (case_tac "x = t"; case_tac "x = vr"; clarsimp simp add: state_hyp_refs_of_def obj_at_def
dest!: get_tcb_SomeD)
apply fastforce
apply (rule hoare_pre)
apply (wp | wpc | clarsimp)+
apply (simp add: obj_at_def)
sorry (* FIXME AARCH64 VCPU
apply (wp get_vcpu_ko | wpc | clarsimp)+
apply (rule_tac Q="\<lambda>rv s. (\<exists>t'. obj_at (\<lambda>tcb. tcb = TCB t' \<and> rv = tcb_vcpu (tcb_arch t')) t s) \<and>
sym_refs (state_hyp_refs_of s)"
in hoare_post_imp)
apply (clarsimp simp: obj_at_def)
apply (wp arch_thread_get_tcb)
apply simp
done *)
lemma arch_thread_set_inv_neq:
"\<lbrace>obj_at P p and K (t \<noteq> p)\<rbrace> arch_thread_set f t \<lbrace>\<lambda>rv. obj_at P p\<rbrace>"
unfolding arch_thread_set_def by (wpsimp wp: set_object_wp) (simp add: obj_at_def)
lemma live_vcpu [simp]:
"live (ArchObj (VCPU (v\<lparr>vcpu_tcb := Some tcb\<rparr>)))"
by (simp add: live_def hyp_live_def arch_live_def)
lemma ex_nonz_cap_to_vcpu_udpate[simp]:
"ex_nonz_cap_to t (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>) = ex_nonz_cap_to t s"
by (simp add: ex_nonz_cap_to_def)
lemma caps_of_state_VCPU_update:
"vcpu_at a s \<Longrightarrow> caps_of_state (s\<lparr>kheap := kheap s(a \<mapsto> ArchObj (VCPU b))\<rparr>) = caps_of_state s"
by (rule ext) (auto simp: caps_of_state_cte_wp_at cte_wp_at_cases obj_at_def)
lemma set_vcpu_ex_nonz_cap_to[wp]:
"\<lbrace>ex_nonz_cap_to t\<rbrace> set_vcpu a b \<lbrace>\<lambda>_. ex_nonz_cap_to t\<rbrace>"
apply (wp set_vcpu_wp)
apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state caps_of_state_VCPU_update)
done
lemma caps_of_state_tcb_arch_update:
"ko_at (TCB y) t' s \<Longrightarrow> caps_of_state (s\<lparr>kheap := kheap s(t' \<mapsto> TCB (y\<lparr>tcb_arch := f (tcb_arch y)\<rparr>))\<rparr>) = caps_of_state s"
by (rule ext) (auto simp: caps_of_state_cte_wp_at cte_wp_at_cases obj_at_def tcb_cap_cases_def)
lemma arch_thread_set_ex_nonz_cap_to[wp]:
"\<lbrace>ex_nonz_cap_to t\<rbrace> arch_thread_set f t' \<lbrace>\<lambda>_. ex_nonz_cap_to t\<rbrace>"
apply (wp arch_thread_set_wp)
apply clarsimp
apply (clarsimp simp: ex_nonz_cap_to_def get_tcb_Some_ko_at cte_wp_at_caps_of_state
caps_of_state_tcb_arch_update)
done
crunch ex_nonz_cap_to[wp]: dissociate_vcpu_tcb "ex_nonz_cap_to t"
(wp: crunch_wps)
crunches vcpu_switch
for if_live_then_nonz_cap[wp]: if_live_then_nonz_cap
(wp: crunch_wps)
lemma associate_vcpu_tcb_if_live_then_nonz_cap[wp]:
"\<lbrace>if_live_then_nonz_cap and ex_nonz_cap_to vcpu and ex_nonz_cap_to tcb\<rbrace>
associate_vcpu_tcb vcpu tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>"
unfolding associate_vcpu_tcb_def
by (wpsimp wp: arch_thread_set_inv_neq hoare_disjI1 get_vcpu_wp hoare_vcg_all_lift hoare_drop_imps)
lemma set_vcpu_valid_arch_Some[wp]:
"\<lbrace>valid_arch_state\<rbrace> set_vcpu vcpu (v\<lparr>vcpu_tcb := Some tcb\<rparr>) \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
apply (wp set_vcpu_wp)
apply (clarsimp simp: valid_arch_state_def)
apply (rule conjI)
sorry (* FIXME AARCH64 VCPU
apply (fastforce simp: valid_asid_table_def obj_at_def)
apply (clarsimp simp: obj_at_def is_vcpu_def hyp_live_def arch_live_def split: option.splits)
done *)
lemma valid_global_objs_vcpu_update_str:
"valid_global_objs s \<Longrightarrow> valid_global_objs (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>)"
by (simp add: valid_global_objs_def)
lemma valid_global_vspace_mappings_vcpu_update_str:
"valid_global_vspace_mappings s \<Longrightarrow> valid_global_vspace_mappings (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>)"
by (simp add: valid_global_vspace_mappings_def)
lemma arm_current_vcpu_update_valid_global_vspace_mappings[simp]:
"valid_global_vspace_mappings (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>)
= valid_global_vspace_mappings s"
by (clarsimp simp: valid_global_vspace_mappings_def global_refs_def
split: kernel_object.splits option.splits)
(* FIXME AARCH64 hyp machine ops
crunches associate_vcpu_tcb
for pspace_aligned[wp]: pspace_aligned
and pspace_distinct[wp]: pspace_distinct
and zombies_final[wp]: zombies_final
and sym_refs_state_refs_of[wp]: "\<lambda>s. sym_refs (state_refs_of s)"
and valid_mdb[wp]: valid_mdb
and valid_ioc[wp]: valid_ioc
and only_idle[wp]: only_idle
and if_unsafe_then_cap[wp]: if_unsafe_then_cap
and valid_reply_caps[wp]: valid_reply_caps
and valid_reply_masters[wp]: valid_reply_masters
and valid_irq_node[wp]: valid_irq_node
and valid_irq_handlers[wp]: valid_irq_handlers
and cap_refs_in_kernel_window[wp]: cap_refs_in_kernel_window
and pspace_respects_device_region[wp]: pspace_respects_device_region
and cur_tcb[wp]: cur_tcb
and valid_vspace_objs[wp]: valid_vspace_objs
and valid_arch_caps[wp]: valid_arch_caps
and valid_kernel_mappings[wp]: valid_kernel_mappings
and equal_kernel_mappings[wp]: equal_kernel_mappings
and valid_asid_map[wp]: valid_asid_map
and valid_global_vspace_mappings[wp]: valid_global_vspace_mappings
and pspace_in_kernel_window[wp]: pspace_in_kernel_window
(wp: crunch_wps dmo_valid_irq_states device_region_dmos simp: crunch_simps) *)
crunches vcpu_switch
for valid_idle[wp]: valid_idle
(wp: crunch_wps)
lemma associate_vcpu_tcb_valid_idle[wp]:
"\<lbrace>valid_idle and (\<lambda>s. tcb \<noteq> idle_thread s)\<rbrace> associate_vcpu_tcb vcpu tcb \<lbrace>\<lambda>_. valid_idle\<rbrace>"
apply (clarsimp simp: associate_vcpu_tcb_def)
by (wp hoare_vcg_all_lift
| wp (once) hoare_drop_imps
| wpc
| simp add: dissociate_vcpu_tcb_def vcpu_invalidate_active_def)+
lemma arm_current_vcpu_update_valid_global_refs[simp]:
"valid_global_refs (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>) = valid_global_refs s"
by (clarsimp simp: valid_global_refs_def global_refs_def
split: kernel_object.splits option.splits)
crunches associate_vcpu_tcb
for valid_global_refs[wp]: valid_global_refs
(wp: crunch_wps)
(* FIXME AARCH64 hyp machine ops
crunches vcpu_restore_reg
for valid_irq_states[wp]: valid_irq_states
(wp: crunch_wps dmo_valid_irq_states simp: writeVCPUHardwareReg_def) *)
lemma is_irq_active_sp:
"\<lbrace>P\<rbrace> get_irq_state irq \<lbrace>\<lambda>rv s. P s \<and> (rv = interrupt_states s irq)\<rbrace>"
by (wpsimp simp: get_irq_state_def)
lemma restore_virt_timer_valid_irq_states[wp]:
"restore_virt_timer vcpu_ptr \<lbrace>valid_irq_states\<rbrace>"
apply (clarsimp simp: restore_virt_timer_def is_irq_active_def liftM_def)
sorry (* FIXME AARCH64 VCPU
apply (repeat_unless \<open>rule hoare_seq_ext[OF _ is_irq_active_sp]\<close>
\<open>rule hoare_seq_ext_skip,
wpsimp wp: dmo_valid_irq_states
simp: isb_def setHCR_def set_cntv_cval_64_def read_cntpct_def
set_cntv_off_64_def\<close>)
apply (wpsimp simp: do_machine_op_def is_irq_active_def get_irq_state_def)
apply (clarsimp simp: valid_irq_states_def valid_irq_masks_def maskInterrupt_def in_monad)
done *)
(* FIXME AARCH64 irq_masks are down due to no_irq naming issue due to using crunch
crunches vcpu_switch
for valid_irq_states[wp]: valid_irq_states
(wp: crunch_wps dmo_valid_irq_states set_gic_vcpu_ctrl_hcr_irq_masks
set_gic_vcpu_ctrl_vmcr_irq_masks set_gic_vcpu_ctrl_lr_irq_masks
set_gic_vcpu_ctrl_apr_irq_masks
simp: get_gic_vcpu_ctrl_lr_def get_gic_vcpu_ctrl_apr_def get_gic_vcpu_ctrl_vmcr_def
get_gic_vcpu_ctrl_hcr_def maskInterrupt_def isb_def setHCR_def) *)
lemma associate_vcpu_tcb_valid_irq_states[wp]:
"associate_vcpu_tcb vcpu tcb \<lbrace>valid_irq_states\<rbrace>"
apply (clarsimp simp: associate_vcpu_tcb_def)
sorry (* FIXME AARCH64 VCPU
by (wp hoare_vcg_all_lift
| wp (once) hoare_drop_imps
| wpc
| simp add: dissociate_vcpu_tcb_def vcpu_invalidate_active_def)+ *)
crunches associate_vcpu_tcb
for cap_refs_respects_device_region[wp]: cap_refs_respects_device_region
(wp: crunch_wps cap_refs_respects_device_region_dmo
simp: read_cntpct_def get_irq_state_def maskInterrupt_def)
lemma arm_current_vcpu_update_valid_global_objs[simp]:
"valid_global_objs (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>) = valid_global_objs s"
by (clarsimp simp: valid_global_objs_def)
crunches associate_vcpu_tcb
for valid_global_objs[wp]: valid_global_objs
(wp: crunch_wps device_region_dmos)
lemma set_vcpu_tcb_Some_hyp_live[wp]:
"\<lbrace>\<top>\<rbrace> set_vcpu vcpu (v\<lparr>vcpu_tcb := Some tcb\<rparr>) \<lbrace>\<lambda>_. obj_at hyp_live vcpu\<rbrace>"
apply (wpsimp wp: set_vcpu_wp)
apply (clarsimp simp: obj_at_def hyp_live_def arch_live_def)
done
lemma associate_vcpu_tcb_valid_arch_state[wp]:
"associate_vcpu_tcb vcpu tcb \<lbrace>valid_arch_state\<rbrace>"
apply (clarsimp simp: associate_vcpu_tcb_def)
apply (wpsimp wp: vcpu_switch_valid_arch)
done (* FIXME AARCH64 VCPU this seems too easy, but remove if nothing changes
apply (rule_tac Q="\<lambda>_. valid_arch_state and obj_at hyp_live vcpu" in hoare_post_imp)
apply fastforce
apply wpsimp
apply (wpsimp wp: arch_thread_set.valid_arch_state)
apply (wpsimp wp: arch_thread_set_wp)+
done *)
lemma dmo_valid_machine_state[wp]:
"do_machine_op (set_cntv_cval_64 w) \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op read_cntpct \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op (set_cntv_off_64 w') \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op (maskInterrupt m irq) \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op (setHCR word) \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op isb \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op dsb \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op (set_gic_vcpu_ctrl_hcr f) \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op (set_gic_vcpu_ctrl_lr n w'') \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op (set_gic_vcpu_ctrl_apr w''') \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op (set_gic_vcpu_ctrl_vmcr w''') \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op (get_gic_vcpu_ctrl_lr w'''') \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op get_gic_vcpu_ctrl_apr \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op get_gic_vcpu_ctrl_vmcr \<lbrace>valid_machine_state\<rbrace>"
"do_machine_op get_gic_vcpu_ctrl_hcr \<lbrace>valid_machine_state\<rbrace>"
unfolding valid_machine_state_def read_cntpct_def
maskInterrupt_def setHCR_def set_gic_vcpu_ctrl_hcr_def set_gic_vcpu_ctrl_lr_def
set_gic_vcpu_ctrl_apr_def set_gic_vcpu_ctrl_vmcr_def get_gic_vcpu_ctrl_lr_def
get_gic_vcpu_ctrl_apr_def get_gic_vcpu_ctrl_vmcr_def get_gic_vcpu_ctrl_hcr_def
sorry (* FIXME AARCH64 VCPU
by (wpsimp wp: hoare_vcg_all_lift hoare_vcg_disj_lift dmo_machine_state_lift)+ *)
(* FIXME AARCH64 VCPU machine ops
crunches restore_virt_timer, vcpu_restore_reg_range, vcpu_save_reg_range, vgic_update_lr
for valid_machine_state[wp]: valid_machine_state
(wp: crunch_wps ignore: do_machine_op) *)
lemma vcpu_enable_valid_machine_state[wp]:
"vcpu_enable vcpu \<lbrace>valid_machine_state\<rbrace>"
apply (simp add: vcpu_enable_def)
sorry (* FIXME AARCH64 VCPU
by (wpsimp | subst do_machine_op_bind | simp add: isb_def)+ *)
(* FIXME AARCH64 VCPU
crunches vcpu_restore, vcpu_save
for valid_machine_state[wp]: valid_machine_state
(wp: mapM_wp_inv simp: do_machine_op_bind dom_mapM ignore: do_machine_op) *)
crunches associate_vcpu_tcb
for valid_machine_state[wp]: valid_machine_state
(wp: crunch_wps ignore: do_machine_op simp: get_gic_vcpu_ctrl_lr_def do_machine_op_bind)
lemma associate_vcpu_tcb_valid_objs[wp]:
"\<lbrace>valid_objs and vcpu_at vcpu\<rbrace>
associate_vcpu_tcb vcpu tcb
\<lbrace>\<lambda>_. valid_objs\<rbrace>"
sorry (* FIXME AARCH64 VCPU broken crunches?
by (wp arch_thread_get_wp
| wp (once) hoare_drop_imps
| wpc
| clarsimp simp: associate_vcpu_tcb_def valid_obj_def[abs_def] valid_vcpu_def
| simp add: obj_at_def)+ *)
lemma associate_vcpu_tcb_invs[wp]:
"\<lbrace>invs and ex_nonz_cap_to vcpu and ex_nonz_cap_to tcb and vcpu_at vcpu and (\<lambda>s. tcb \<noteq> idle_thread s)\<rbrace>
associate_vcpu_tcb vcpu tcb
\<lbrace>\<lambda>_. invs\<rbrace>"
sorry (* FIXME AARCH64 VCPU
by (wpsimp simp: invs_def valid_state_def valid_pspace_def) *)
lemma set_vcpu_regs_update[wp]:
"\<lbrace>invs and valid_obj p (ArchObj (VCPU vcpu)) and
obj_at (\<lambda>ko'. hyp_refs_of ko' = vcpu_tcb_refs (vcpu_tcb vcpu)) p\<rbrace>
set_vcpu p (vcpu_regs_update f vcpu) \<lbrace>\<lambda>_. invs\<rbrace>"
unfolding invs_def valid_state_def
by (wpsimp wp: set_vcpu_valid_pspace set_vcpu_valid_arch_eq_hyp)
lemma write_vcpu_register_invs[wp]:
"\<lbrace>invs\<rbrace> write_vcpu_register vcpu reg val \<lbrace>\<lambda>_. invs\<rbrace>"
unfolding write_vcpu_register_def
by wpsimp
lemma vgic_update_valid_pspace[wp]:
"\<lbrace>valid_pspace\<rbrace> vgic_update vcpuptr f \<lbrace>\<lambda>_. valid_pspace\<rbrace>"
unfolding vgic_update_def vcpu_update_def
apply (wpsimp wp: set_vcpu_valid_pspace get_vcpu_wp simp: valid_vcpu_def)
apply (fastforce simp: obj_at_def dest!: valid_pspace_vo)
done
crunches invoke_vcpu_inject_irq, vcpu_read_reg
for invs[wp]: invs (ignore: do_machine_op)
lemma invoke_vcpu_ack_vppi_invs[wp]:
"invoke_vcpu_ack_vppi vcpu_ptr vppi \<lbrace>invs\<rbrace>"
unfolding invoke_vcpu_ack_vppi_def by (wpsimp cong: vcpu.fold_congs)
lemma perform_vcpu_invs[wp]:
"\<lbrace>invs and valid_vcpu_invocation vi\<rbrace> perform_vcpu_invocation vi \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: perform_vcpu_invocation_def valid_vcpu_invocation_def)
apply (wpsimp simp: invoke_vcpu_read_register_def read_vcpu_register_def
invoke_vcpu_write_register_def)
done
lemma invoke_arch_invs[wp]:
"\<lbrace>invs and ct_active and valid_arch_inv ai\<rbrace>
arch_perform_invocation ai
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (cases ai, simp_all add: valid_arch_inv_def arch_perform_invocation_def)
apply (wp|simp)+
apply (wp perform_vcpu_invs|simp)+
sorry (* FIXME AARCH64
done *)
@ -990,22 +1350,32 @@ lemma sts_valid_vspace_table_inv[wp]:
by (cases i; wpsimp wp: sts_typ_ats hoare_vcg_ex_lift hoare_vcg_all_lift
simp: invalid_pte_at_def aobjs_of_ako_at_Some[symmetric])
lemma sts_valid_vcpu_invocation_inv:
"\<lbrace>valid_vcpu_invocation vcpu_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_vcpu_invocation vcpu_invocation\<rbrace>"
unfolding valid_vcpu_invocation_def by (cases vcpu_invocation; wpsimp)
lemma sts_valid_arch_inv:
"set_thread_state t st \<lbrace>valid_arch_inv ai\<rbrace>"
apply (cases ai; simp add: valid_arch_inv_def; wp?)
"\<lbrace>valid_arch_inv ai\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_arch_inv ai\<rbrace>"
apply (cases ai, simp_all add: valid_arch_inv_def)
apply (rename_tac page_table_invocation)
apply (case_tac page_table_invocation, simp_all add: valid_pti_def)[1]
sorry (* FIXME AARCH64 VCPU: valid_arch_inv is missing cases (VCPU and InvokeVSpace)
apply ((wp valid_pde_lift set_thread_state_valid_cap
hoare_vcg_all_lift hoare_vcg_const_imp_lift
hoare_vcg_ex_lift set_thread_state_ko
sts_typ_ats set_thread_state_cte_wp_at
| clarsimp simp: is_tcb_def)+)[4]
apply (rename_tac asid_control_invocation)
apply (case_tac asid_control_invocation)
apply (clarsimp simp: valid_aci_def cte_wp_at_caps_of_state)
sorry (* FIXME AARCH64 VCPU: valid_arch_inv is missing cases (VCPU and InvokeVSpace)
apply (rule hoare_pre, wp hoare_vcg_ex_lift cap_table_at_typ_at)
apply clarsimp
apply (clarsimp simp: valid_apinv_def split: asid_pool_invocation.splits)
apply (rule hoare_pre)
apply (wp hoare_vcg_ex_lift set_thread_state_ko)
apply (clarsimp simp: is_tcb_def)
apply (clarsimp simp: is_tcb_def, wp sts_valid_vcpu_invocation_inv)
done *)
crunch_ignore (add: select_ext find_vspace_for_asid)
@ -1299,6 +1669,43 @@ lemma decode_asid_control_invocation_wf[wp]:
apply (clarsimp simp add: cte_wp_at_caps_of_state)
done
lemma arch_decode_vcpu_invocation_wf[wp]:
"arch_cap = VCPUCap vcpu_ptr \<Longrightarrow>
\<lbrace>invs and valid_cap (ArchObjectCap arch_cap) and cte_wp_at ((=) (ArchObjectCap arch_cap)) slot
and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)\<rbrace>
decode_vcpu_invocation label args arch_cap excaps
\<lbrace>valid_arch_inv\<rbrace>, -"
apply (clarsimp simp: arch_decode_invocation_def decode_vcpu_invocation_def)
apply (cases "invocation_type label"; (simp, wp?))
apply (rename_tac arch_iv)
apply (case_tac "arch_iv"; (simp, wp?))
apply (simp add: decode_vcpu_set_tcb_def)
apply (rule hoare_pre, wpsimp)
apply (clarsimp simp: valid_arch_inv_def valid_vcpu_invocation_def)
apply (rename_tac tcb_ptr)
apply (frule_tac c="ThreadCap tcb_ptr" in cte_wp_valid_cap, fastforce)
apply (simp add: valid_cap_def)
apply (cases slot)
apply (clarsimp simp: ex_nonz_cap_to_def)
apply (rule conjI, fastforce elim: cte_wp_at_weakenE)
apply (rule conjI, fastforce elim: cte_wp_at_weakenE)
apply (clarsimp dest!: invs_valid_global_refs simp: cte_wp_at_caps_of_state)
apply (drule_tac ?cap="ThreadCap (idle_thread s)" in valid_global_refsD2, assumption)
apply (simp add:global_refs_def cap_range_def)
apply (simp add: decode_vcpu_inject_irq_def)
apply (rule hoare_pre, wpsimp simp: whenE_def wp: get_vcpu_wp)
apply (clarsimp simp: valid_arch_inv_def valid_vcpu_invocation_def obj_at_def)
apply (simp add: decode_vcpu_read_register_def)
apply (rule hoare_pre, wpsimp)
apply (clarsimp simp: valid_arch_inv_def valid_cap_def valid_vcpu_invocation_def)
apply (simp add: decode_vcpu_write_register_def)
apply (rule hoare_pre, wpsimp)
apply (clarsimp simp: valid_arch_inv_def valid_cap_def valid_vcpu_invocation_def)
apply (simp add: decode_vcpu_ack_vppi_def arch_check_irq_def)
apply (rule hoare_pre, wpsimp)
apply (clarsimp simp: valid_arch_inv_def valid_cap_def valid_vcpu_invocation_def)
done
lemma arch_decode_inv_wf[wp]:
"\<lbrace>invs and valid_cap (ArchObjectCap arch_cap) and
cte_wp_at ((=) (ArchObjectCap arch_cap)) slot and real_cte_at slot and
@ -1306,11 +1713,39 @@ lemma arch_decode_inv_wf[wp]:
(\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile> (fst x))\<rbrace>
arch_decode_invocation label args x_slot slot arch_cap excaps
\<lbrace>valid_arch_inv\<rbrace>,-"
sorry (* FIXME AARCH64 PTs
unfolding arch_decode_invocation_def
apply wpsimp
subgoal sorry (* VSRootPT *)
subgoal sorry (* NormalPT *)
apply wpsimp+
apply fastforce
done (* FIXME AARCH64 PTs
(note: ARM_HYP has this as one big proof, this factored-out style is nicer)
unfolding arch_decode_invocation_def by wpsimp fastforce *)
declare word_less_sub_le [simp]
crunches associate_vcpu_tcb
for pred_tcb_at[wp_unsafe]: "pred_tcb_at proj P t"
(wp: crunch_wps simp: crunch_simps)
crunches vcpu_read_reg, vcpu_write_reg, invoke_vcpu_inject_irq
for pred_tcb_at[wp]: "pred_tcb_at proj P t"
lemma perform_vcpu_invocation_pred_tcb_at[wp_unsafe]:
"\<lbrace>pred_tcb_at proj P t and K (proj_not_field proj tcb_arch_update)\<rbrace>
perform_vcpu_invocation iv
\<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>"
apply (simp add: perform_vcpu_invocation_def)
apply (rule hoare_pre)
apply (wp associate_vcpu_tcb_pred_tcb_at | wpc
| clarsimp simp: invoke_vcpu_read_register_def
read_vcpu_register_def
invoke_vcpu_write_register_def
write_vcpu_register_def
invoke_vcpu_ack_vppi_def)+
done
crunch pred_tcb_at [wp]:
perform_page_table_invocation, perform_page_invocation, perform_asid_pool_invocation
"pred_tcb_at proj P t"
@ -1324,7 +1759,21 @@ lemma arch_pinv_st_tcb_at:
apply (cases ai; simp add: arch_perform_invocation_def valid_arch_inv_def)
sorry (* FIXME AARCH64 enter MATCH (probably a free var somewhere)
apply (wp perform_asid_control_invocation_st_tcb_at; fastforce elim!: pred_tcb_weakenE)+
done *)
done
NOTE: ARM_HYP proof was:
apply (cases ai, simp_all add: arch_perform_invocation_def valid_arch_inv_def)
apply (wp perform_page_table_invocation_pred_tcb_at,
fastforce elim!: pred_tcb_weakenE)
apply (wp perform_page_directory_invocation_pred_tcb_at, fastforce elim: pred_tcb_weakenE)
apply (wp perform_page_invocation_pred_tcb_at, fastforce elim!: pred_tcb_weakenE)
apply (wp perform_asid_control_invocation_st_tcb_at,
fastforce elim!: pred_tcb_weakenE)
apply (wp perform_asid_pool_invocation_pred_tcb_at,
fastforce elim!: pred_tcb_weakenE)
apply (wp perform_vcpu_invocation_pred_tcb_at,
fastforce elim!: pred_tcb_weakenE)
done
*)
end

20
proof/invariant-abstract/AARCH64/ArchBCorres2_AI.thy
View File

@ -1,4 +1,5 @@
(*
* Copyright 2022, Proofcraft Pty Ltd
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
@ -127,17 +128,28 @@ crunch (bcorres)bcorres[wp]: receive_ipc,receive_signal,delete_caller_cap trunca
lemma handle_vm_fault_bcorres[wp]: "bcorres (handle_vm_fault a b) (handle_vm_fault a b)"
unfolding handle_vm_fault_def by (cases b; wpsimp)
lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b)"
by (cases b) wpsimp
lemma vgic_maintenance_bcorres[wp]:
"bcorres vgic_maintenance vgic_maintenance"
unfolding vgic_maintenance_def
by (wpsimp simp: vgic_update_lr_bcorres)
lemma vppi_event_bcorres[wp]:
"bcorres (vppi_event irq) (vppi_event irq)"
unfolding vppi_event_def
by wpsimp
lemma handle_reserved_irq_bcorres[wp]: "bcorres (handle_reserved_irq a) (handle_reserved_irq a)"
unfolding handle_reserved_irq_def by wpsimp
lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b)"
by (cases b; wpsimp)
lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
apply (cases e)
apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def
handle_interrupt_def Let_def handle_reserved_irq_def arch_mask_irq_signal_def
| intro impI conjI allI | wp | wpc)+
sorry (* FIXME AARCH64 VCPU vppi_event
done *)
done
crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord)

4
proof/invariant-abstract/AARCH64/ArchCNodeInv_AI.thy
View File

@ -473,8 +473,8 @@ lemma zombie_is_cap_toE_pre[CNodeInv_AI_assms]:
apply (simp add: nat_to_cref_def word_bits_conv)
done
(* FIXME AARCH64 FPU/VCPU
crunch st_tcb_at_halted[wp]: prepare_thread_delete "st_tcb_at halted t" *)
crunch st_tcb_at_halted[wp]: prepare_thread_delete "st_tcb_at halted t"
(wp: dissociate_vcpu_tcb_pred_tcb_at)
lemma finalise_cap_makes_halted_proof[CNodeInv_AI_assms]:
"\<lbrace>invs and valid_cap cap and (\<lambda>s. ex = is_final_cap' cap s)

14
proof/invariant-abstract/AARCH64/ArchCSpacePre_AI.thy
View File

@ -1,4 +1,5 @@
(*
* Copyright 2022, Proofcraft Pty Ltd
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
@ -41,11 +42,11 @@ lemma aobj_ref_cases:
ASIDPoolCap w _ \<Rightarrow> Some w
| ASIDControlCap \<Rightarrow> None
| FrameCap w _ _ _ _ \<Rightarrow> Some w
| PageTableCap w _ _ \<Rightarrow> Some w)"
| PageTableCap w _ _ \<Rightarrow> Some w
| VCPUCap v \<Rightarrow> Some v)"
apply (subst aobj_ref_cases')
sorry (* FIXME AARCH64 VCPU
apply (clarsimp cong: arch_cap.case_cong)
done *)
done
definition
"ups_of_heap h \<equiv> \<lambda>p.
@ -150,6 +151,13 @@ lemma arch_derived_is_device:
split: if_split_asm cap.splits arch_cap.splits)+
done
(* FIXME AARCH64: use vcpus_of instead *)
lemma set_cap_no_vcpu[wp]:
"\<lbrace>obj_at (is_vcpu and P) p\<rbrace> set_cap cap cref \<lbrace>\<lambda>_. obj_at (is_vcpu and P) p\<rbrace>"
unfolding set_cap_def2 split_def
by (wpsimp wp: set_object_wp get_object_wp get_cap_wp)
(auto simp: obj_at_def is_vcpu_def)
lemma valid_arch_mdb_simple:
"\<lbrakk> valid_arch_mdb (is_original_cap s) (caps_of_state s);
is_simple_cap cap; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow>

5
proof/invariant-abstract/AARCH64/ArchDetSchedAux_AI.thy
View File

@ -1,4 +1,5 @@
(*
* Copyright 2022, Proofcraft Pty Ltd
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
@ -135,6 +136,10 @@ crunch valid_sched_action[wp]: init_arch_objects valid_sched_action (wp: valid_s
crunch valid_sched[wp]: init_arch_objects valid_sched (wp: valid_sched_lift)
(* FIXME AARCH64 issue with crunch ordering, ArchVCPU_AI gets there first rather than some crunch
that does this declaration *)
declare invoke_untyped_cur_thread[DetSchedAux_AI_assms]
end
lemmas tcb_sched_action_valid_idle_etcb

26
proof/invariant-abstract/AARCH64/ArchDetSchedDomainTime_AI.thy
View File

@ -84,6 +84,32 @@ crunch domain_time_inv [wp, DetSchedDomainTime_AI_assms]: arch_perform_invocatio
crunch domain_list_inv [wp, DetSchedDomainTime_AI_assms]: arch_perform_invocation "\<lambda>s. P (domain_list s)"
(wp: crunch_wps check_cap_inv simp: if_apply_def2)
lemma vgic_maintenance_valid_domain_time:
"\<lbrace>\<lambda>s. 0 < domain_time s\<rbrace>
vgic_maintenance \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>"
unfolding vgic_maintenance_def
apply (rule hoare_strengthen_post [where Q="\<lambda>_ s. 0 < domain_time s"])
apply (wpsimp wp: handle_fault_domain_time_inv hoare_drop_imps)
apply clarsimp
done
lemma vppi_event_valid_domain_time:
"\<lbrace>\<lambda>s :: det_ext state. 0 < domain_time s\<rbrace>
vppi_event irq \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>"
unfolding vppi_event_def
apply (rule hoare_strengthen_post [where Q="\<lambda>_ s. 0 < domain_time s"])
apply (wpsimp wp: handle_fault_domain_time_inv hoare_drop_imps)
apply clarsimp
done
lemma handle_reserved_irq_valid_domain_time:
"\<lbrace>\<lambda>s :: det_ext state. 0 < domain_time s\<rbrace>
handle_reserved_irq i \<lbrace>\<lambda>y s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>"
unfolding handle_reserved_irq_def when_def
supply if_split[split del]
by (wpsimp wp: vppi_event_valid_domain_time vgic_maintenance_valid_domain_time
hoare_drop_imp[where R="\<lambda>_ _. irq_vppi_event_index _ = _"])
lemma timer_tick_valid_domain_time:
"\<lbrace> \<lambda>s :: det_ext state. 0 < domain_time s \<rbrace>
timer_tick

172
proof/invariant-abstract/AARCH64/ArchDetSchedSchedule_AI.thy
View File

@ -13,9 +13,64 @@ context Arch begin global_naming AARCH64
named_theorems DetSchedSchedule_AI_assms
(* FIXME AARCH64 VCPU
crunch prepare_thread_delete_idle_thread[wp, DetSchedSchedule_AI_assms]:
crunch prepare_thread_delete_idle_thread[wp, DetSchedSchedule_AI_assms]:
prepare_thread_delete "\<lambda>(s:: det_ext state). P (idle_thread s)"
(wp: crunch_wps)
crunch exst[wp]: set_vcpu "\<lambda>s. P (exst s)" (wp: crunch_wps)
crunch exst[wp]: vcpu_disable,vcpu_restore,vcpu_save "\<lambda>s. P (exst s)"
(wp: crunch_wps)
(* FIXME AARCH64: check if crunchable, also below *)
lemma vcpu_switch_exst[wp]:
"\<lbrace>\<lambda>s. P (exst s)\<rbrace> vcpu_switch param_a \<lbrace>\<lambda>_ s. P (exst s)\<rbrace>"
unfolding vcpu_switch_def by (rule hoare_pre) wpsimp+
lemma set_vcpu_etcbs [wp]:
"\<lbrace>valid_etcbs\<rbrace> set_vcpu a b \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
by (rule valid_etcbs_lift; wp)
(* FIXME AARCH64: param_a, also further below *)
lemma vcpu_switch_valid_etcbs[wp]:
"\<lbrace>valid_etcbs\<rbrace> vcpu_switch param_a \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
by (rule valid_etcbs_lift; wp)
lemma pred_tcb_atP[wp]:
"\<lbrace>\<lambda>s. P (pred_tcb_at proj Q t s)\<rbrace> set_vcpu prt vcpu \<lbrace>\<lambda>_ s. P (pred_tcb_at proj Q t s)\<rbrace>"
unfolding set_vcpu_def set_object_def
apply (wp get_object_wp)
apply (clarsimp simp: pred_tcb_at_def obj_at_def split: kernel_object.splits)
done
crunch pred_tcb_atP[wp]: vcpu_disable, vcpu_enable, vcpu_restore, vcpu_save
"\<lambda>s. P (pred_tcb_at proj Q t s)"
(wp: crunch_wps simp: crunch_simps)
lemma vcpu_switch_pred_tcb_at[wp]:
"\<lbrace>\<lambda>s. P (pred_tcb_at proj Q t s)\<rbrace> vcpu_switch vcpu \<lbrace>\<lambda>_ s. P (pred_tcb_at proj Q t s)\<rbrace>"
unfolding vcpu_switch_def by (rule hoare_pre) wpsimp+
lemma set_vcpu_valid_queues [wp]:
"\<lbrace>valid_queues\<rbrace> set_vcpu ptr vcpu \<lbrace>\<lambda>_. valid_queues\<rbrace>"
by (rule valid_queues_lift; wp)
lemma vcpu_switch_valid_queues[wp]:
"\<lbrace>valid_queues\<rbrace> vcpu_switch v \<lbrace>\<lambda>_. valid_queues\<rbrace>"
by (rule valid_queues_lift; wp)
lemma set_vcpu_weak_valid_sched_action[wp]:
"\<lbrace>weak_valid_sched_action\<rbrace> set_vcpu ptr vcpu \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>"
by (rule weak_valid_sched_action_lift; wp)
lemma vcpu_switch_weak_valid_sched_action[wp]:
"\<lbrace>weak_valid_sched_action\<rbrace> vcpu_switch v \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>"
by (rule weak_valid_sched_action_lift; wp)
(* FIXME AARCH64 VCPU
is this one and other pred_tcb_atP used?
crunch pred_tcb_atP[wp]: set_vm_root "\<lambda>s. P (pred_tcb_at proj Q t s)"
(wp: crunch_wps simp: crunch_simps)
crunch valid_etcbs [wp, DetSchedSchedule_AI_assms]:
arch_switch_to_idle_thread, arch_switch_to_thread, arch_get_sanitise_register_info, arch_post_modify_registers valid_etcbs
@ -36,6 +91,11 @@ crunch ct_not_in_q[wp]: set_vm_root "ct_not_in_q"
crunch ct_not_in_q'[wp]: set_vm_root "\<lambda>s. ct_not_in_q_2 (ready_queues s) (scheduler_action s) t"
(wp: crunch_wps simp: crunch_simps)
lemma vcpu_switch_valid_sched_action[wp]:
"\<lbrace>valid_sched_action\<rbrace> vcpu_switch v \<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
unfolding valid_sched_action_def is_activatable_def st_tcb_at_kh_simp
by (rule hoare_lift_Pf[where f=cur_thread]; wpsimp wp: hoare_vcg_imp_lift)
lemma switch_to_idle_thread_ct_not_in_q [wp, DetSchedSchedule_AI_assms]:
"\<lbrace>valid_queues and valid_idle\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>"
apply (simp add: switch_to_idle_thread_def)
@ -80,7 +140,23 @@ lemma switch_to_idle_thread_ct_in_cur_domain [wp, DetSchedSchedule_AI_assms]:
crunch ct_not_in_q [wp, DetSchedSchedule_AI_assms]: arch_switch_to_thread, arch_get_sanitise_register_info, arch_post_modify_registers ct_not_in_q
(simp: crunch_simps wp: crunch_wps)
lemma do_machine_op_activatable[wp]:
"\<lbrace>is_activatable t\<rbrace> do_machine_op oper \<lbrace>\<lambda>_. is_activatable t\<rbrace>"
unfolding do_machine_op_def by wpsimp
lemma set_vcpu_is_activatable[wp]:
"\<lbrace>is_activatable t\<rbrace> set_vcpu ptr vcpu \<lbrace>\<lambda>_. is_activatable t\<rbrace>"
unfolding is_activatable_def set_vcpu_def set_object_def
apply (wp get_object_wp)
apply (clarsimp simp: st_tcb_at_kh_def obj_at_kh_def obj_at_def)
done
(* FIXME AARCH64 VCPU
crunches vcpu_disable, vcpu_restore, vcpu_save, vcpu_switch, set_vm_root
for is_activatable[wp]: "is_activatable t"
and valid_sched[wp, DetSchedSchedule_AI_assms]: valid_sched
(wp: crunch_wps valid_sched_lift simp: crunch_simps)
crunch is_activatable [wp, DetSchedSchedule_AI_assms]: arch_switch_to_thread, arch_get_sanitise_register_info, arch_post_modify_registers "is_activatable t"
(simp: crunch_simps)
@ -119,6 +195,20 @@ crunch scheduler_action [wp, DetSchedSchedule_AI_assms]:
(simp: Let_def)
*)
lemma vcpu_switch_ct_in_q[wp]:
"\<lbrace>ct_in_q\<rbrace> vcpu_switch vcpu \<lbrace>\<lambda>_. ct_in_q\<rbrace>"
unfolding ct_in_q_def
apply (rule hoare_lift_Pf[where f="\<lambda>s. cur_thread s", rotated], wp)
apply (rule hoare_lift_Pf[where f="\<lambda>s. ready_queues s", rotated], wp)
apply wp
done
(* FIXME AARCH64 VCPU
crunches do_machine_op, set_vm_root, vcpu_switch
for valid_blocked[wp]: valid_blocked
and ct_in_q[wp]: ct_in_q
(wp: valid_blocked_lift simp: crunch_simps) *)
lemma set_vm_root_valid_blocked_ct_in_q [wp]:
"\<lbrace>valid_blocked and ct_in_q\<rbrace> set_vm_root p \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>"
sorry (* FIXME AARCH64 vm root
@ -198,6 +288,10 @@ lemma set_pt_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> set_pt ptr pt \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (wp hoare_drop_imps valid_sched_lift | simp add: set_pt_def)+
lemma set_vcpu_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> set_vcpu t vr \<lbrace>\<lambda>_. valid_sched\<rbrace>"
by (rule valid_sched_lift; wp)
lemma set_asid_pool_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (wp hoare_drop_imps valid_sched_lift | simp add: set_asid_pool_def)+
@ -237,6 +331,28 @@ crunch valid_sched[wp]:
valid_sched
(wp: mapM_x_wp' mapM_wp' crunch_wps) *)
(* FIXME AARCH64 VCPU
crunches
vcpu_read_reg,vcpu_write_reg,read_vcpu_register,write_vcpu_register,set_message_info,as_user
for cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
and valid_sched[wp]: valid_sched
and ct_in_state[wp]: "ct_in_state st"
(simp: crunch_simps wp: ct_in_state_thread_state_lift ignore: get_object) *)
lemma invoke_vcpu_read_register_valid_sched[wp]:
"\<lbrace>valid_sched and ct_active\<rbrace> invoke_vcpu_read_register v reg \<lbrace>\<lambda>_. valid_sched\<rbrace>"
sorry (* FIXME AARCH64: missing crunch on read_vcpu_register
unfolding invoke_vcpu_read_register_def by (wpsimp wp: set_thread_state_Running_valid_sched) *)
lemma invoke_vcpu_write_register_valid_sched[wp]:
"\<lbrace>valid_sched and ct_active\<rbrace> invoke_vcpu_write_register v reg val \<lbrace>\<lambda>_. valid_sched\<rbrace>"
sorry (* FIXME AARCH64 VCPU
unfolding invoke_vcpu_write_register_def by (wpsimp wp: set_thread_state_Restart_valid_sched) *)
(* FIXME AARCH64 VCPU
crunch valid_sched[wp]: perform_vcpu_invocation valid_sched
(wp: crunch_wps simp: crunch_simps ignore: set_thread_state) *)
lemma arch_perform_invocation_valid_sched [wp, DetSchedSchedule_AI_assms]:
"\<lbrace>invs and valid_sched and ct_active and valid_arch_inv a\<rbrace>
arch_perform_invocation a
@ -325,6 +441,55 @@ global_interpretation DetSchedSchedule_AI?: DetSchedSchedule_AI
context Arch begin global_naming AARCH64
lemma dmo_scheduler_act_sane[wp]:
"\<lbrace>scheduler_act_sane\<rbrace> do_machine_op f \<lbrace>\<lambda>rv. scheduler_act_sane\<rbrace>"
unfolding scheduler_act_sane_def
by (rule hoare_lift_Pf[where f=cur_thread]; wp)
lemma vgic_maintenance_irq_valid_sched[wp]:
"\<lbrace>valid_sched and invs and scheduler_act_sane and ct_not_queued\<rbrace>
vgic_maintenance
\<lbrace>\<lambda>rv. valid_sched\<rbrace>"
unfolding vgic_maintenance_def
supply if_split[split del] valid_fault_def[simp]
apply (wpsimp simp: get_gic_vcpu_ctrl_misr_def get_gic_vcpu_ctrl_eisr1_def
get_gic_vcpu_ctrl_eisr0_def if_apply_def2
wp: thread_get_wp'
ct_in_state_thread_state_lift ct_not_queued_lift sch_act_sane_lift
hoare_vcg_imp_lift' gts_wp hoare_vcg_all_lift
handle_fault_valid_sched hoare_vcg_disj_lift
| wp (once) hoare_drop_imp[where f="do_machine_op m" for m]
hoare_drop_imp[where f="return $ m" for m]
| wps
| strengthen not_pred_tcb_at_strengthen)+
sorry (* FIXME AARCH64 vgic_update_lr
apply (frule tcb_at_invs)
apply (clarsimp simp: runnable_eq halted_eq not_pred_tcb)
apply (fastforce intro!: st_tcb_ex_cap[where P=active]
simp: st_tcb_at_def ct_in_state_def obj_at_def)
done *)
lemma vppi_event_irq_valid_sched[wp]:
"\<lbrace>valid_sched and invs and scheduler_act_sane and ct_not_queued\<rbrace>
vppi_event irq
\<lbrace>\<lambda>rv. valid_sched\<rbrace>"
unfolding vppi_event_def
supply if_split[split del] valid_fault_def[simp]
apply (wpsimp simp: if_apply_def2
wp: hoare_vcg_imp_lift' gts_wp hoare_vcg_all_lift maskInterrupt_invs
hoare_vcg_disj_lift
handle_fault_valid_sched
ct_in_state_thread_state_lift ct_not_queued_lift sch_act_sane_lift
cong: vcpu.fold_congs
| wps
| strengthen not_pred_tcb_at_strengthen)+
sorry (* FIXME AARCH64 vcpu_update
apply (frule tcb_at_invs)
apply (clarsimp simp: runnable_eq halted_eq not_pred_tcb)
apply (fastforce intro!: st_tcb_ex_cap[where P=active]
simp: not_pred_tcb st_tcb_at_def obj_at_def ct_in_state_def)
done *)
lemma handle_hyp_fault_valid_sched[wp]:
"\<lbrace>valid_sched and invs and st_tcb_at active t and not_queued t and scheduler_act_not t
and (ct_active or ct_idle)\<rbrace>
@ -334,7 +499,8 @@ lemma handle_hyp_fault_valid_sched[wp]:
lemma handle_reserved_irq_valid_sched:
"\<lbrace>valid_sched and invs and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> scheduler_act_sane s \<and> ct_not_queued s)\<rbrace>
handle_reserved_irq irq \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
sorry (* FIXME AARCH64 VCPU vppi
unfolding handle_reserved_irq_def irq_vppi_event_index_def when_def
sorry (* FIXME AARCH64 double-when causing problems
unfolding handle_reserved_irq_def by (wpsimp simp: non_kernel_IRQs_def) *)
end

26
proof/invariant-abstract/AARCH64/ArchDeterministic_AI.thy
View File

@ -1,17 +1,32 @@
(*
* Copyright 2022, Proofcraft Pty Ltd
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory ArchDeterministic_AI
imports Deterministic_AI
imports Deterministic_AI ArchVCPU_AI
begin
declare dxo_wp_weak[wp del]
context Arch begin global_naming AARCH64
named_theorems Deterministic_AI_assms
crunch valid_list[wp, Deterministic_AI_assms]:
vcpu_save, vcpu_enable, vcpu_disable, vcpu_restore, arch_get_sanitise_register_info, arch_post_modify_registers valid_list
(wp: crunch_wps simp: unless_def crunch_simps)
(* FIXME AARCH64: crunchable? If not, rename param_a *)
lemma vcpu_switch_valid_list[wp, Deterministic_AI_assms]:
"\<lbrace>valid_list\<rbrace> vcpu_switch param_a \<lbrace>\<lambda>_. valid_list\<rbrace>"
apply (simp add: vcpu_switch_def)
apply (rule hoare_pre)
apply(wpsimp)+
done
crunch valid_list[wp, Deterministic_AI_assms]:
cap_swap_for_delete,set_cap,finalise_cap,arch_get_sanitise_register_info,
arch_post_modify_registers valid_list
@ -52,7 +67,7 @@ lemma perform_page_invocation_valid_list[wp]:
done *)
crunch valid_list[wp]: perform_invocation valid_list
(wp: crunch_wps simp: crunch_simps ignore: without_preemption)
(wp: crunch_wps simp: crunch_simps ignore: without_preemption as_user)
crunch valid_list[wp, Deterministic_AI_assms]: handle_invocation valid_list
(wp: crunch_wps syscall_valid simp: crunch_simps
@ -65,14 +80,17 @@ lemma handle_vm_fault_valid_list[wp, Deterministic_AI_assms]:
"handle_vm_fault thread fault \<lbrace>valid_list\<rbrace>"
unfolding handle_vm_fault_def by (cases fault; wpsimp)
crunches vgic_maintenance, vppi_event
for valid_list[wp]: valid_list
(wp: hoare_drop_imps)
lemma handle_interrupt_valid_list[wp, Deterministic_AI_assms]:
"\<lbrace>valid_list\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_.valid_list\<rbrace>"
unfolding handle_interrupt_def ackInterrupt_def
apply (rule hoare_pre)
sorry (* FIXME AARCH64 vvpi_event
by (wp get_cap_wp do_machine_op_valid_list
| wpc | simp add: get_irq_slot_def handle_reserved_irq_def arch_mask_irq_signal_def
| wp (once) hoare_drop_imps)+ *)
| wp (once) hoare_drop_imps)+
crunch valid_list[wp, Deterministic_AI_assms]: handle_send,handle_reply valid_list

36
proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy
View File

@ -48,6 +48,9 @@ crunch (empty_fail) empty_fail[wp]:
decode_set_tls_base
(simp: cap.splits arch_cap.splits split_def)
crunch (empty_fail) empty_fail[wp]: decode_vcpu_invocation
(simp: cap.splits arch_cap.splits split_def)
lemma decode_tcb_invocation_empty_fail[wp]:
"empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)"
by (simp add: decode_tcb_invocation_def split: gen_invocation_labels.splits invocation_label.splits
@ -58,6 +61,7 @@ crunch (empty_fail) empty_fail[wp]: find_vspace_for_asid, check_vp_alignment (*
lemma arch_decode_ARMASIDControlMakePool_empty_fail:
"invocation_type label = ArchInvocationLabel ARMASIDControlMakePool
\<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)"
apply (simp add: arch_decode_invocation_def Let_def)
apply (wpsimp simp: arch_decode_invocation_def decode_asid_pool_invocation_def)
apply (simp add: decode_asid_control_invocation_def)
apply (intro impI conjI allI)
@ -66,13 +70,16 @@ lemma arch_decode_ARMASIDControlMakePool_empty_fail:
apply simp
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def fail_def
gets_def get_def assert_def select_def
split: if_split_asm)
apply wpsimp
apply (wpsimp simp: decode_frame_invocation_def)
sorry (* FIXME AARCH64 VCPU and PageFlush invocations
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def fail_def
gets_def get_def assert_def select_def
split: if_split_asm)
apply wpsimp
apply (wpsimp simp: decode_frame_invocation_def)
subgoal sorry (* missing wp rule *)
subgoal sorry (* PTs *)
apply wpsimp
done (* FIXME AARCH64 VCPU and PageFlush invocations
apply (wpsimp simp: decode_page_table_invocation_def)
done *)
@ -134,6 +141,15 @@ lemma empty_fail_pt_lookup_from_level[wp]:
apply wpsimp
done
crunch (empty_fail) empty_fail[wp]: vcpu_update, vcpu_save_reg_range, vgic_update_lr, save_virt_timer
(ignore: set_object get_object)
lemma vcpu_save_empty_fail[wp,EmptyFail_AI_assms]: "empty_fail (vcpu_save a)"
apply (simp add: vcpu_save_def)
sorry (* FIXME AARCH64 missing empty_fail_dsb
apply (wpsimp wp: empty_fail_dsb empty_fail_isb simp: vgic_update_def)
done *)
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slot,
finalise_cap, preemption_point,
cap_swap_for_delete, decode_invocation
@ -180,6 +196,12 @@ lemma plic_complete_claim_empty_fail[wp, EmptyFail_AI_assms]:
"empty_fail (plic_complete_claim irq)"
by (clarsimp simp: plic_complete_claim_def)
lemma vgic_maintenance_empty_fail[wp]: "empty_fail vgic_maintenance"
by (wpsimp simp: get_gic_vcpu_ctrl_eisr0_def
get_gic_vcpu_ctrl_eisr1_def
get_gic_vcpu_ctrl_misr_def
vgic_maintenance_def)
crunches possible_switch_to, handle_event, activate_thread
for (empty_fail) empty_fail[wp, EmptyFail_AI_assms]
(simp: cap.splits arch_cap.splits split_def invocation_label.splits Let_def

635
proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy
View File

@ -144,6 +144,16 @@ lemma set_pt_tcb_at:
"\<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pt a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>"
by (wpsimp simp: set_pt_def obj_at_def wp: set_object_wp)
lemma set_vcpu_tcb_at_arch: (* generalise? this holds except when the ko is a vcpu *)
"\<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace>
set_vcpu p v
\<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>"
by (wp set_vcpu_nonvcpu_at; auto)
crunch tcb_at_arch: vcpu_switch "\<lambda>s. P (ko_at (TCB tcb) t s)"
(simp: crunch_simps when_def
wp: crunch_wps set_vcpu_tcb_at_arch)
crunch tcb_at_arch: unmap_page "\<lambda>s. P (ko_at (TCB tcb) t s)"
(simp: crunch_simps wp: crunch_wps set_pt_tcb_at ignore: set_object)
@ -301,6 +311,11 @@ lemma arch_thread_get_final_cap[wp]:
apply auto
done
lemma dissociate_vcpu_tcb_final_cap[wp]:
"\<lbrace>is_final_cap' cap\<rbrace> dissociate_vcpu_tcb v t \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>"
sorry (* FIXME AARCH64 FPU/VCPU
by (wpsimp simp: is_final_cap'_def2 cte_wp_at_caps_of_state) *)
lemma prepare_thread_delete_final[wp]:
"\<lbrace>is_final_cap' cap\<rbrace> prepare_thread_delete t \<lbrace> \<lambda>rv. is_final_cap' cap\<rbrace>"
sorry (* FIXME AARCH64 FPU/VCPU
@ -342,6 +357,10 @@ lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]:
crunch typ_at_arch [wp]: arch_thread_set "\<lambda>s. P (typ_at T p s)"
(wp: crunch_wps set_object_typ_at)
crunch typ_at[wp]: dissociate_vcpu_tcb "\<lambda>s. P (typ_at T p s)"
(wp: crunch_wps simp: crunch_simps unless_def assertE_def
ignore: do_machine_op set_object)
crunch typ_at[wp,Finalise_AI_asms]: arch_finalise_cap "\<lambda>s. P (typ_at T p s)"
(wp: crunch_wps simp: crunch_simps unless_def assertE_def
ignore: maskInterrupt set_object)
@ -353,6 +372,12 @@ crunch tcb_at[wp]: arch_thread_set "\<lambda>s. tcb_at p s"
crunch tcb_at[wp]: arch_thread_get "\<lambda>s. tcb_at p s"
lemma vcpu_set_tcb_at[wp]: "\<lbrace>\<lambda>s. tcb_at p s\<rbrace> set_vcpu t vcpu \<lbrace>\<lambda>_ s. tcb_at p s\<rbrace>"
by (wpsimp simp: tcb_at_typ)
crunch tcb_at[wp]: dissociate_vcpu_tcb "\<lambda>s. tcb_at p s"
(wp: crunch_wps)
(* FIXME AARCH64 FPU/VCPU
crunch tcb_at[wp]: prepare_thread_delete "\<lambda>s. tcb_at p s" *)
@ -491,10 +516,11 @@ lemma arch_thread_set_only_idle[wp]:
arch_thread_set_pred_tcb_at)
lemma arch_thread_set_valid_idle[wp]:
"arch_thread_set f t \<lbrace>valid_idle\<rbrace>"
sorry (* FIXME AARCH64 VCPU
"\<lbrace>valid_idle and (\<lambda> s. t \<noteq> idle_thread s \<or> (\<forall>atcb. tcb_vcpu atcb = None \<longrightarrow> tcb_vcpu (f atcb) = None))\<rbrace>
arch_thread_set f t
\<lbrace>\<lambda>rv. valid_idle\<rbrace>"
by (wpsimp simp: arch_thread_set_def set_object_def get_object_def valid_idle_def
valid_arch_idle_def get_tcb_def pred_tcb_at_def obj_at_def pred_neg_def) *)
valid_arch_idle_def get_tcb_def pred_tcb_at_def obj_at_def pred_neg_def)
lemma arch_thread_set_valid_ioc[wp]:
"\<lbrace>valid_ioc\<rbrace> arch_thread_set p v \<lbrace>\<lambda>rv. valid_ioc\<rbrace>"
@ -525,6 +551,17 @@ lemma arch_thread_set_zombies_final[wp]: "\<lbrace>zombies_final\<rbrace> arch_t
apply (clarsimp simp: obj_at_def tcb_cap_cases_def)
done
lemma arch_thread_set_if_live_then_nonz_cap_Some[wp]:
"\<lbrace> (ex_nonz_cap_to t or obj_at live t) and if_live_then_nonz_cap\<rbrace>
arch_thread_set (tcb_vcpu_update (\<lambda>_. Some vcp)) t \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>"
apply (simp add: arch_thread_set_def)
apply (wp set_object_iflive)
apply (clarsimp simp: ex_nonz_cap_to_def if_live_then_nonz_cap_def
dest!: get_tcb_SomeD)
apply (subst get_tcb_rev, assumption, subst option.sel)+
apply (clarsimp simp: obj_at_def tcb_cap_cases_def)
done
lemma arch_thread_set_pspace_in_kernel_window[wp]:
"\<lbrace>pspace_in_kernel_window\<rbrace> arch_thread_set f v \<lbrace>\<lambda>_.pspace_in_kernel_window\<rbrace>"
by (rule pspace_in_kernel_window_atyp_lift, wp+)
@ -555,6 +592,27 @@ lemma arch_thread_set_valid_objs_context[wp]:
apply (clarsimp simp:valid_obj_def valid_tcb_def tcb_cap_cases_def)
done
lemma arch_thread_set_valid_objs_vcpu_None[wp]:
"arch_thread_set (tcb_vcpu_update Map.empty) v \<lbrace>valid_objs\<rbrace>"
apply (simp add: arch_thread_set_def)
apply (wp set_object_valid_objs)
apply (clarsimp simp: Ball_def obj_at_def valid_objs_def dest!: get_tcb_SomeD)
apply (erule_tac x=v in allE)
apply (clarsimp simp: dom_def)
apply (subst get_tcb_rev, assumption, subst option.sel)+
apply (clarsimp simp:valid_obj_def valid_tcb_def tcb_cap_cases_def valid_arch_tcb_def)
done
lemma arch_thread_set_valid_objs_vcpu_Some[wp]:
"\<lbrace>valid_objs and vcpu_at vcpu\<rbrace> arch_thread_set (tcb_vcpu_update (\<lambda>_. Some vcpu)) v \<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (simp add: arch_thread_set_def)
apply (wpsimp wp: set_object_valid_objs)
apply (clarsimp simp: Ball_def obj_at_def valid_objs_def dest!: get_tcb_SomeD)
apply (erule_tac x=v in allE)
apply (clarsimp simp: dom_def)
apply (clarsimp simp:valid_obj_def valid_tcb_def tcb_cap_cases_def valid_arch_tcb_def obj_at_def)
done
lemma sym_refs_update_some_tcb:
"\<lbrakk>kheap s v = Some (TCB tcb) ; refs_of (TCB tcb) = refs_of (TCB (f tcb))\<rbrakk>
\<Longrightarrow> sym_refs (state_refs_of (s\<lparr>kheap := kheap s (v \<mapsto> TCB (f tcb))\<rparr>)) = sym_refs (state_refs_of s)"
@ -576,6 +634,128 @@ lemma arch_thread_sym_refs[wp]:
apply assumption
done
lemma arch_thread_get_tcb:
"\<lbrace> \<top> \<rbrace> arch_thread_get tcb_vcpu p \<lbrace>\<lambda>rv s. \<exists>t. obj_at (\<lambda>tcb. tcb = (TCB t) \<and> rv = tcb_vcpu (tcb_arch t)) p s\<rbrace>"
apply (simp add: arch_thread_get_def)
apply wp
apply (clarsimp simp: obj_at_def dest!: get_tcb_SomeD)
apply (subst get_tcb_rev, assumption, subst option.sel)+
apply simp
done
lemma get_vcpu_ko: "\<lbrace>Q\<rbrace> get_vcpu p \<lbrace>\<lambda>rv s. ko_at (ArchObj (VCPU rv)) p s \<and> Q s\<rbrace>"
unfolding get_vcpu_def
apply wpsimp
sorry (* FIXME AARCH64
apply (rule hoare_allI)
apply (subst eq_commute)
apply (subst (2) eq_commute)
apply clarsimp
apply (rule hoare_drop_imp)+
apply (subst conj_commute)
apply (wp get_object_sp[simplified pred_conj_def], simp)
done *)
lemma vcpu_invalidate_tcbs_inv[wp]:
"\<lbrace>obj_at (\<lambda>tcb. \<exists>t'. tcb = TCB t' \<and> P t') t\<rbrace>
vcpu_invalidate_active \<lbrace>\<lambda>rv. obj_at (\<lambda>tcb. \<exists>t'. tcb = TCB t' \<and> P t') t\<rbrace>"
unfolding vcpu_invalidate_active_def vcpu_disable_def by wpsimp
lemma sym_refs_vcpu_None:
assumes sym_refs: "sym_refs (state_hyp_refs_of s)"
assumes tcb: "ko_at (TCB tcb) t s" "tcb_vcpu (tcb_arch tcb) = Some vr"
shows "sym_refs (state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_arch := tcb_vcpu_update Map.empty (tcb_arch tcb)\<rparr>),
vr \<mapsto> ArchObj (VCPU (vcpu_tcb_update Map.empty v)))\<rparr>))"
(is "sym_refs (state_hyp_refs_of ?s')")
proof -
from tcb
have t: "state_hyp_refs_of s t = {(vr,TCBHypRef)}"
by (simp add: state_hyp_refs_of_def obj_at_def)
moreover
from t
have "(t,HypTCBRef) \<in> state_hyp_refs_of s vr"
using sym_refsD [of vr _ _ t, OF _ sym_refs] by auto
hence vr: "state_hyp_refs_of s vr = {(t,HypTCBRef)}"
sorry (* FIXME AARCH64 hyp
by (auto simp: state_hyp_refs_of_def hyp_refs_of_def tcb_vcpu_refs_def vcpu_tcb_refs_def
refs_of_def refs_of_a_def
split: option.splits kernel_object.splits arch_kernel_obj.splits) *)
moreover
from sym_refs vr
have "\<And>x r rt. \<lbrakk> (r, rt) \<in> state_hyp_refs_of s x; x \<noteq> t \<rbrakk> \<Longrightarrow> r \<noteq> vr"
by (auto dest: sym_refsD)
moreover
from sym_refs t
have "\<And>x r rt. \<lbrakk> (r, rt) \<in> state_hyp_refs_of s x; x \<noteq> vr \<rbrakk> \<Longrightarrow> r \<noteq> t"
by (auto dest: sym_refsD)
ultimately
have "sym_refs ((state_hyp_refs_of s) (vr := {}, t := {}))"
using sym_refs unfolding sym_refs_def by (clarsimp simp: split_def)
moreover
have "state_hyp_refs_of ?s' = (state_hyp_refs_of s) (vr := {}, t := {})"
unfolding state_hyp_refs_of_def sorry (* FIXME AARCH64 hyp by (rule ext) simp *)
ultimately
show ?thesis by simp
qed
lemma arch_thread_set_wp:
"\<lbrace>\<lambda>s. get_tcb p s \<noteq> None \<longrightarrow> Q (s\<lparr>kheap := kheap s(p \<mapsto> TCB (the (get_tcb p s)\<lparr>tcb_arch := f (tcb_arch (the (get_tcb p s)))\<rparr>))\<rparr>) \<rbrace>
arch_thread_set f p
\<lbrace>\<lambda>_. Q\<rbrace>"
apply (simp add: arch_thread_set_def)
apply (wp set_object_wp)
apply simp
done
lemma arch_thread_get_wp:
"\<lbrace>\<lambda>s. \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> Q (f (tcb_arch tcb)) s\<rbrace> arch_thread_get f t \<lbrace>Q\<rbrace>"
apply (wpsimp simp: arch_thread_get_def)
apply (auto dest!: get_tcb_ko_atD)
done
(* FIXME: move *)
lemma get_tcb_None_tcb_at:
"(get_tcb p s = None) = (\<not>tcb_at p s)"
by (auto simp: get_tcb_def obj_at_def is_tcb_def split: kernel_object.splits option.splits)
(* FIXME: move *)
lemma get_tcb_Some_ko_at:
"(get_tcb p s = Some t) = ko_at (TCB t) p s"
by (auto simp: get_tcb_def obj_at_def is_tcb_def split: kernel_object.splits option.splits)
lemma dissociate_vcpu_tcb_sym_refs_hyp[wp]:
"\<lbrace>\<lambda>s. sym_refs (state_hyp_refs_of s)\<rbrace> dissociate_vcpu_tcb vr t \<lbrace>\<lambda>rv s. sym_refs (state_hyp_refs_of s)\<rbrace>"
apply (simp add: dissociate_vcpu_tcb_def arch_get_sanitise_register_info_def)
apply (wp arch_thread_set_wp set_vcpu_wp)
apply (rule_tac Q="\<lambda>_ s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_vcpu (tcb_arch tcb) = Some vr) t s
\<and> sym_refs (state_hyp_refs_of s)" in hoare_post_imp)
apply clarsimp
apply (clarsimp simp: get_tcb_Some_ko_at obj_at_def sym_refs_vcpu_None split: if_splits)
apply (wp get_vcpu_wp arch_thread_get_wp)+
apply clarsimp
apply (rule conjI, clarsimp simp: obj_at_def)
apply clarsimp
apply (clarsimp simp: get_tcb_Some_ko_at obj_at_def sym_refs_vcpu_None split: if_splits)
done
(* FIXME AARCH64 VCPU
crunch valid_objs[wp]: dissociate_vcpu_tcb "valid_objs"
(wp: crunch_wps simp: crunch_simps valid_obj_def valid_vcpu_def ignore: arch_thread_set) *)
lemma set_vcpu_unlive_hyp[wp]:
"\<lbrace>\<lambda>s. vr \<noteq> t \<longrightarrow> obj_at (Not \<circ> hyp_live) t s\<rbrace>
set_vcpu vr (vcpu_tcb_update Map.empty v) \<lbrace>\<lambda>rv. obj_at (Not \<circ> hyp_live) t\<rbrace>"
apply (wpsimp wp: set_vcpu_wp)
apply (clarsimp simp: obj_at_def hyp_live_def arch_live_def)
done
lemma arch_thread_set_unlive_hyp[wp]:
"\<lbrace>\<lambda>s. vr \<noteq> t \<longrightarrow> obj_at (Not \<circ> hyp_live) vr s\<rbrace>
arch_thread_set (tcb_vcpu_update Map.empty) t \<lbrace>\<lambda>_. obj_at (Not \<circ> hyp_live) vr\<rbrace>"
apply (wpsimp simp: arch_thread_set_def wp: set_object_wp)
apply (clarsimp simp: obj_at_def hyp_live_def)
done
lemma as_user_unlive_hyp[wp]:
"\<lbrace>obj_at (Not \<circ> hyp_live) vr\<rbrace> as_user t f \<lbrace>\<lambda>_. obj_at (Not \<circ> hyp_live) vr\<rbrace>"
unfolding as_user_def
@ -583,6 +763,26 @@ lemma as_user_unlive_hyp[wp]:
sorry (* FIXME AARCH64 VCPU
by (clarsimp simp: obj_at_def hyp_live_def arch_tcb_context_set_def) *)
lemma dissociate_vcpu_tcb_unlive_hyp_vr[wp]:
"\<lbrace>\<top>\<rbrace> dissociate_vcpu_tcb vr t \<lbrace> \<lambda>_. obj_at (Not \<circ> hyp_live) vr\<rbrace>"
unfolding dissociate_vcpu_tcb_def arch_get_sanitise_register_info_def
by (wpsimp wp: get_vcpu_wp hoare_vcg_const_imp_lift hoare_drop_imps)
lemma dissociate_vcpu_tcb_unlive_hyp_t[wp]:
"\<lbrace>\<top>\<rbrace> dissociate_vcpu_tcb vr t \<lbrace> \<lambda>_. obj_at (Not \<circ> hyp_live) t\<rbrace>"
unfolding dissociate_vcpu_tcb_def arch_get_sanitise_register_info_def
by (wpsimp wp: hoare_vcg_const_imp_lift hoare_drop_imps get_vcpu_wp)
lemma arch_thread_set_unlive0[wp]:
"\<lbrace>obj_at (Not \<circ> live0) vr\<rbrace> arch_thread_set (tcb_vcpu_update Map.empty) t \<lbrace>\<lambda>_. obj_at (Not \<circ> live0) vr\<rbrace>"
apply (wpsimp simp: arch_thread_set_def wp: set_object_wp)
apply (clarsimp simp: obj_at_def get_tcb_def split: kernel_object.splits)
done
lemma set_vcpu_unlive0[wp]:
"\<lbrace>obj_at (Not \<circ> live0) t\<rbrace> set_vcpu vr v \<lbrace>\<lambda>rv. obj_at (Not \<circ> live0) t\<rbrace>"
by (wpsimp wp: set_vcpu_wp simp: obj_at_def)
lemma as_user_unlive0[wp]:
"\<lbrace>obj_at (Not \<circ> live0) vr\<rbrace> as_user t f \<lbrace>\<lambda>_. obj_at (Not \<circ> live0) vr\<rbrace>"
unfolding as_user_def
@ -592,6 +792,9 @@ lemma as_user_unlive0[wp]:
lemma o_def_not: "obj_at (\<lambda>a. \<not> P a) t s = obj_at (Not o P) t s"
by (simp add: obj_at_def)
crunch unlive0: dissociate_vcpu_tcb "obj_at (Not \<circ> live0) t"
(wp: crunch_wps simp: o_def_not ignore: arch_thread_set)
lemma arch_thread_set_if_live_then_nonz_cap':
"\<forall>y. hyp_live (TCB (y\<lparr>tcb_arch := p (tcb_arch y)\<rparr>)) \<longrightarrow> hyp_live (TCB y) \<Longrightarrow>
\<lbrace>if_live_then_nonz_cap\<rbrace> arch_thread_set p v \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>"
@ -605,10 +808,118 @@ lemma arch_thread_set_if_live_then_nonz_cap':
apply (clarsimp simp: live_def)
done
lemma arch_thread_set_if_live_then_nonz_cap_None[wp]:
"\<lbrace>if_live_then_nonz_cap\<rbrace> arch_thread_set (tcb_vcpu_update Map.empty) t \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>"
apply (wp arch_thread_set_if_live_then_nonz_cap')
apply (clarsimp simp: hyp_live_def)
apply assumption
done
lemma set_vcpu_if_live_then_nonz_cap_same_refs:
"\<lbrace>if_live_then_nonz_cap and obj_at (\<lambda>ko'. hyp_refs_of ko' = hyp_refs_of (ArchObj (VCPU v))) p\<rbrace>
set_vcpu p v \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>"
apply (simp add: set_vcpu_def)
including unfold_objects
apply (wpsimp wp: set_object_iflive[THEN hoare_set_object_weaken_pre]
simp: a_type_def live_def hyp_live_def arch_live_def)
apply (rule if_live_then_nonz_capD; simp)
sorry (* FIXME AARCH64 VCPU
apply (clarsimp simp: live_def hyp_live_def arch_live_def,
clarsimp simp: vcpu_tcb_refs_def split: option.splits)
done *)
lemma vgic_update_if_live_then_nonz_cap[wp]:
"\<lbrace>if_live_then_nonz_cap\<rbrace> vgic_update vcpuptr f \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>"
unfolding vgic_update_def vcpu_update_def
apply (wp set_vcpu_if_live_then_nonz_cap_same_refs get_vcpu_wp)
apply (clarsimp simp: obj_at_def)
done
lemma vcpu_save_reg_if_live_then_nonz_cap[wp]:
"\<lbrace>if_live_then_nonz_cap\<rbrace> vcpu_save_reg vcpuptr r \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>"
unfolding vcpu_save_reg_def vcpu_update_def
apply (wpsimp wp: set_vcpu_if_live_then_nonz_cap_same_refs get_vcpu_wp
hoare_vcg_imp_lift hoare_vcg_all_lift)
apply (simp add: obj_at_def)
done
lemma vcpu_update_regs_if_live_then_nonz_cap[wp]:
"vcpu_update vcpu_ptr (vcpu_regs_update f) \<lbrace>if_live_then_nonz_cap\<rbrace>"
unfolding vcpu_update_def
by (wpsimp wp: set_vcpu_if_live_then_nonz_cap_same_refs get_vcpu_wp)
(simp add: obj_at_def)
lemma vcpu_write_if_live_then_nonz_cap[wp]:
"vcpu_write_reg vcpu_ptr reg val \<lbrace>if_live_then_nonz_cap\<rbrace>"
unfolding vcpu_write_reg_def by (wpsimp cong: vcpu.fold_congs)
lemma vcpu_update_vtimer_if_live_then_nonz_cap[wp]:
"vcpu_update vcpu_ptr (vcpu_vtimer_update f) \<lbrace>if_live_then_nonz_cap\<rbrace>"
unfolding vcpu_update_def
by (wpsimp wp: set_vcpu_if_live_then_nonz_cap_same_refs get_vcpu_wp)
(simp add: obj_at_def)
crunches vcpu_disable, vcpu_invalidate_active
for if_live_then_nonz_cap[wp]: if_live_then_nonz_cap
(ignore: vcpu_update)
lemma dissociate_vcpu_tcb_if_live_then_nonz_cap[wp]:
"\<lbrace>if_live_then_nonz_cap\<rbrace> dissociate_vcpu_tcb vr t \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>"
unfolding dissociate_vcpu_tcb_def arch_get_sanitise_register_info_def
by (wpsimp wp: get_vcpu_wp arch_thread_get_wp hoare_drop_imps)
lemma vcpu_invalidate_active_ivs[wp]: "\<lbrace>invs\<rbrace> vcpu_invalidate_active \<lbrace>\<lambda>_. invs\<rbrace>"
unfolding vcpu_invalidate_active_def
by (wpsimp simp: cur_vcpu_at_def | strengthen invs_current_vcpu_update')+
crunch cur_tcb[wp]: dissociate_vcpu_tcb "cur_tcb"
(wp: crunch_wps)
crunches dissociate_vcpu_tcb
for cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
(wp: crunch_wps)
lemma same_caps_tcb_arch_update[simp]:
"same_caps (TCB (tcb_arch_update f tcb)) = same_caps (TCB tcb)"
by (rule ext) (clarsimp simp: tcb_cap_cases_def)
crunches dissociate_vcpu_tcb
for cap_refs_respects_device_region[wp]: "cap_refs_respects_device_region"
(wp: crunch_wps cap_refs_respects_device_region_dmo
simp: crunch_simps read_cntpct_def maskInterrupt_def
(* FIXME AARCH64 these should not be needed *)
enableFpuEL01_def check_export_arch_timer_def isb_def dsb_def
ignore: do_machine_op)
(* FIXME AARCH64 VCPU
crunch pspace_respects_device_region[wp]: dissociate_vcpu_tcb "pspace_respects_device_region"
(wp: crunch_wps) *)
crunch cap_refs_in_kernel_window[wp]: dissociate_vcpu_tcb "cap_refs_in_kernel_window"
(wp: crunch_wps simp: crunch_simps)
crunch pspace_in_kernel_window[wp]: dissociate_vcpu_tcb "pspace_in_kernel_window"
(wp: crunch_wps)
lemma valid_asid_map_arm_current_vcpu_update[simp]:
"valid_asid_map (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>) = valid_asid_map s"
by (simp add: valid_asid_map_def vspace_at_asid_def)
crunch valid_asid_map[wp]: dissociate_vcpu_tcb "valid_asid_map"
(wp: crunch_wps)
crunch valid_kernel_mappings[wp]: dissociate_vcpu_tcb "valid_kernel_mappings"
(wp: crunch_wps)
crunch valid_arch_caps[wp]: dissociate_vcpu_tcb "valid_arch_caps"
(wp: crunch_wps)
crunch valid_vspace_objs[wp]: dissociate_vcpu_tcb "valid_vspace_objs"
(wp: crunch_wps)
crunch valid_irq_handlers[wp]: dissociate_vcpu_tcb "valid_irq_handlers"
(wp: crunch_wps ignore: do_machine_op)
lemma as_user_valid_irq_node[wp]:
"\<lbrace>valid_irq_node\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_irq_node\<rbrace>"
unfolding as_user_def
@ -616,10 +927,89 @@ lemma as_user_valid_irq_node[wp]:
apply (clarsimp simp: valid_irq_node_def obj_at_def is_cap_table dest!: get_tcb_SomeD)
by (metis kernel_object.distinct(1) option.inject)
crunch valid_irq_node[wp]: dissociate_vcpu_tcb "valid_irq_node"
(wp: crunch_wps)
lemma dmo_valid_irq_states:
"(\<And>P. \<lbrace>\<lambda>s. P (irq_masks s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_masks s)\<rbrace>) \<Longrightarrow>
\<lbrace>valid_irq_states\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_irq_states\<rbrace>"
unfolding valid_irq_states_def do_machine_op_def
apply (rule hoare_lift_Pf [where f="\<lambda>s. irq_masks (machine_state s)"])
apply wpsimp+
apply (erule use_valid; assumption)
done
lemma dmo_machine_state_lift:
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P (machine_state s)\<rbrace> do_machine_op f \<lbrace>\<lambda>rv s. Q rv (machine_state s)\<rbrace>"
unfolding do_machine_op_def by wpsimp (erule use_valid; assumption)
lemma dmo_maskInterrupt_True_valid_irq_states[wp]:
"do_machine_op (maskInterrupt True irq) \<lbrace>valid_irq_states\<rbrace>"
unfolding valid_irq_states_def do_machine_op_def maskInterrupt_def
apply wpsimp
apply (erule use_valid)
apply (wpsimp simp: valid_irq_masks_def)+
done
(* FIXME AARCH64
crunches vcpu_save_reg, vgic_update, vcpu_disable
for valid_irq_states[wp]: valid_irq_states
and in_user_frame[wp]: "in_user_frame p"
(wp: dmo_maskInterrupt_True_valid_irq_states dmo_valid_irq_states
simp: isb_def setHCR_def setSCTLR_def set_gic_vcpu_ctrl_hcr_def getSCTLR_def
get_gic_vcpu_ctrl_hcr_def dsb_def readVCPUHardwareReg_def writeVCPUHardwareReg_def
read_cntpct_def maskInterrupt_def check_export_arch_timer_def) *)
lemma dmo_writeVCPUHardwareReg_valid_machine_state[wp]:
"do_machine_op (writeVCPUHardwareReg r v) \<lbrace>valid_machine_state\<rbrace>"
unfolding valid_machine_state_def
by (wpsimp wp: hoare_vcg_all_lift hoare_vcg_disj_lift writeVCPUHardwareReg_underlying_memory
dmo_machine_state_lift)
(* FIXME AARCH64
crunches vgic_update, vcpu_update, vcpu_write_reg, vcpu_save_reg, save_virt_timer
for in_user_frame[wp]: "in_user_frame p"
and valid_machine_state[wp]: valid_machine_state
and underlying_memory[wp]: "\<lambda>s. P (underlying_memory (machine_state s))"
(simp: readVCPUHardwareReg_def read_cntpct_def
wp: writeVCPUHardwareReg_underlying_memory_pred dmo_machine_state_lift
ignore: do_machine_op) *)
lemma vcpu_disable_valid_machine_state[wp]:
"\<lbrace>valid_machine_state\<rbrace> vcpu_disable vcpu_opt \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
unfolding vcpu_disable_def valid_machine_state_def
sorry (* FIXME AARCH64 broken crunches
by (wpsimp wp: dmo_machine_state_lift hoare_vcg_all_lift hoare_vcg_disj_lift
simp: isb_def setHCR_def setSCTLR_def set_gic_vcpu_ctrl_hcr_def getSCTLR_def
get_gic_vcpu_ctrl_hcr_def dsb_def writeVCPUHardwareReg_def maskInterrupt_def) *)
lemma valid_arch_state_vcpu_update_str:
"valid_arch_state s \<Longrightarrow> valid_arch_state (s\<lparr>arch_state := arm_current_vcpu_update Map.empty (arch_state s)\<rparr>)"
sorry (* FIXME AARCH64 VCPU
by (simp add: valid_arch_state_def) *)
lemma valid_global_refs_vcpu_update_str:
"valid_global_refs s \<Longrightarrow> valid_global_refs (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>)"
by (simp add: valid_global_refs_def global_refs_def)
lemma set_vcpu_None_valid_arch[wp]:
"\<lbrace>valid_arch_state and (\<lambda>s. \<forall>a. arm_current_vcpu (arch_state s) \<noteq> Some (vr, a))\<rbrace>
set_vcpu vr (vcpu_tcb_update Map.empty v) \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
apply (wp set_vcpu_wp)
apply (clarsimp simp: valid_arch_state_def)
sorry (* FIXME AARCH64 VCPU
apply (rule conjI)
apply (fastforce simp: valid_asid_table_def obj_at_def)
apply (clarsimp simp: obj_at_def split: option.splits)
done *)
lemma dissociate_vcpu_valid_arch[wp]:
"\<lbrace>valid_arch_state\<rbrace> dissociate_vcpu_tcb vr t \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
unfolding dissociate_vcpu_tcb_def vcpu_invalidate_active_def arch_get_sanitise_register_info_def
sorry (* FIXME AARCH64 VCPU
by (wpsimp wp: get_vcpu_wp arch_thread_get_wp
| strengthen valid_arch_state_vcpu_update_str | wp (once) hoare_drop_imps)+ *)
lemma as_user_valid_irq_states[wp]:
"\<lbrace>valid_irq_states\<rbrace> as_user t f \<lbrace>\<lambda>rv. valid_irq_states\<rbrace>"
unfolding as_user_def
@ -633,6 +1023,21 @@ lemma as_user_valid_ioc[wp]:
"\<lbrace>valid_ioc\<rbrace> as_user t f \<lbrace>\<lambda>rv. valid_ioc\<rbrace>"
unfolding valid_ioc_def by (wpsimp wp: hoare_vcg_imp_lift hoare_vcg_all_lift)
lemma dissociate_vcpu_tcb_invs[wp]: "\<lbrace>invs\<rbrace> dissociate_vcpu_tcb vr t \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def)
apply (simp add: pred_conj_def)
apply (rule hoare_vcg_conj_lift[rotated])+
sorry (* FIXME AARCH64 VCPU
apply (wpsimp wp: weak_if_wp get_vcpu_wp arch_thread_get_wp as_user_only_idle arch_thread_set_valid_idle
| simp add: dissociate_vcpu_tcb_def vcpu_invalidate_active_def arch_get_sanitise_register_info_def
| strengthen valid_arch_state_vcpu_update_str valid_global_refs_vcpu_update_str
| simp add: vcpu_disable_def valid_global_vspace_mappings_def valid_global_objs_def
| wp (once) hoare_drop_imps)+
done *)
crunch invs[wp]: vcpu_finalise invs
(ignore: dissociate_vcpu_tcb)
lemma arch_finalise_cap_invs' [wp,Finalise_AI_asms]:
"\<lbrace>invs and valid_cap (ArchObjectCap cap)\<rbrace>
arch_finalise_cap cap final
@ -645,20 +1050,116 @@ lemma arch_finalise_cap_invs' [wp,Finalise_AI_asms]:
sorry (* FIXME AARCH64 FPU/VCPU
done *)
lemma arch_thread_set_unlive_other:
"\<lbrace>\<lambda>s. vr \<noteq> t \<and> obj_at (Not \<circ> live) vr s\<rbrace> arch_thread_set (tcb_vcpu_update Map.empty) t \<lbrace>\<lambda>_. obj_at (Not \<circ> live) vr\<rbrace>"
apply (wpsimp simp: arch_thread_set_def wp: set_object_wp)
apply (clarsimp simp: obj_at_def)
done
lemma set_vcpu_unlive[wp]:
"\<lbrace>\<top>\<rbrace> set_vcpu vr (vcpu_tcb_update Map.empty v) \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) vr\<rbrace>"
apply (wp set_vcpu_wp)
apply (clarsimp simp: obj_at_def live_def hyp_live_def arch_live_def)
done
lemma as_user_unlive[wp]:
"\<lbrace>obj_at (Not \<circ> live) vr\<rbrace> as_user t f \<lbrace>\<lambda>_. obj_at (Not \<circ> live) vr\<rbrace>"
unfolding as_user_def
apply (wpsimp wp: set_object_wp)
by (clarsimp simp: obj_at_def live_def hyp_live_def arch_tcb_context_set_def dest!: get_tcb_SomeD)
lemma dissociate_vcpu_tcb_unlive_v:
"\<lbrace>\<top>\<rbrace> dissociate_vcpu_tcb vr t \<lbrace> \<lambda>_. obj_at (Not \<circ> live) vr\<rbrace>"
unfolding dissociate_vcpu_tcb_def
by (wpsimp wp: arch_thread_set_unlive_other get_vcpu_wp arch_thread_get_wp hoare_drop_imps
simp: bind_assoc)
lemma vcpu_finalise_unlive:
"\<lbrace>\<top>\<rbrace> vcpu_finalise r \<lbrace> \<lambda>_. obj_at (Not \<circ> live) r \<rbrace>"
apply (wpsimp simp: vcpu_finalise_def wp: dissociate_vcpu_tcb_unlive_v get_vcpu_wp)
apply (auto simp: obj_at_def live_def hyp_live_def arch_live_def)
done
lemma arch_finalise_cap_vcpu:
notes strg = tcb_cap_valid_imp_NullCap
vcpu_finalise_unlive[simplified o_def]
notes simps = replaceable_def
is_cap_simps vs_cap_ref_def
no_cap_to_obj_with_diff_ref_Null o_def
notes wps = hoare_drop_imp[where R="%_. is_final_cap' cap" for cap]
valid_cap_typ
shows
"cap = VCPUCap r \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> cap.ArchObjectCap cap \<and>
x = is_final_cap' (cap.ArchObjectCap cap) s \<and>
pspace_aligned s \<and> valid_vspace_objs s \<and> valid_objs s \<and>
valid_asid_table s\<rbrace>
arch_finalise_cap cap x
\<lbrace>\<lambda>rv s. replaceable s sl (fst rv) (cap.ArchObjectCap cap)\<rbrace>"
apply (simp add: arch_finalise_cap_def)
apply (rule hoare_pre)
sorry (* FIXME AARCH64
apply (wp wps | simp add: simps reachable_pg_cap_def| wpc | strengthen strg)+
done *)
lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_asms]:
"(s \<turnstile> ArchObjectCap cap \<and> aobj_ref cap = Some r)
"(s \<turnstile> ArchObjectCap cap \<and> aobj_ref cap = Some r \<and> \<not> typ_at (AArch AVCPU) r s)
\<longrightarrow> obj_at (\<lambda>ko. \<not> live ko) r s"
sorry (* FIXME AARCH64 FPU/VCPU
by (clarsimp simp: valid_cap_def obj_at_def valid_arch_cap_ref_def
a_type_arch_live live_def hyp_live_def
by (clarsimp simp: live_def valid_cap_def obj_at_def a_type_arch_live valid_cap_simps
hyp_live_def arch_live_def
split: arch_cap.split_asm if_splits) *)
lemma obj_at_not_live_valid_arch_cap_strg' [Finalise_AI_asms]:
"(s \<turnstile> ArchObjectCap cap \<and> aobj_ref cap = Some r \<and> cap \<noteq> VCPUCap r)
\<longrightarrow> obj_at (\<lambda>ko. \<not> live ko) r s"
sorry (* FIXME AARCH64 FPU/VCPU
by (clarsimp simp: live_def valid_cap_def obj_at_def
hyp_live_def arch_live_def
split: arch_cap.split_asm if_splits) *)
lemma arch_finalise_cap_replaceable1:
notes strg = tcb_cap_valid_imp_NullCap
obj_at_not_live_valid_arch_cap_strg[where cap=cap]
notes simps = replaceable_def and_not_not_or_imp
(* FIXME AARCH64 vs_lookup_pages_eq_at[THEN fun_cong, symmetric] *)
(* FIXME AARCH64 vs_lookup_pages_eq_ap[THEN fun_cong, symmetric] *)
is_cap_simps vs_cap_ref_def
no_cap_to_obj_with_diff_ref_Null o_def
notes wps = hoare_drop_imp[where R="%_. is_final_cap' cap" for cap]
(* FIXME AARCH64 unmap_page_table_unmapped3 *) valid_cap_typ
assumes X: "\<forall>r. cap \<noteq> VCPUCap r"
shows
"\<lbrace>\<lambda>s. s \<turnstile> cap.ArchObjectCap cap \<and>
x = is_final_cap' (cap.ArchObjectCap cap) s \<and>
pspace_aligned s \<and> valid_vspace_objs s \<and> valid_objs s \<and>
valid_asid_table s\<rbrace>
arch_finalise_cap cap x
\<lbrace>\<lambda>rv s. replaceable s sl (fst rv) (cap.ArchObjectCap cap)\<rbrace>"
sorry (* FIXME AARCH64
apply (simp add: arch_finalise_cap_def)
apply (rule hoare_pre)
apply (simp add: simps split: option.splits vmpage_size.splits)
apply (wp wps
| strengthen strg
| simp add: simps reachable_pg_cap_def live_def
| wpc)+
(* unmap_page case is a bit unpleasant *)
apply (strengthen cases_conj_strg[where P="\<not> is_final_cap' cap s" for cap s, simplified])
apply (rule hoare_post_imp, clarsimp split: vmpage_size.split, assumption)
apply (simp add: vspace_bits_defs)
apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift hoare_vcg_const_imp_lift
unmap_page_tcb_cap_valid unmap_page_page_unmapped
unmap_page_section_unmapped)[1]
apply (wp wps
| strengthen strg imp_and_strg tcb_cap_valid_imp_NullCap
| simp add: simps is_master_reply_cap_def reachable_pg_cap_def
| wpc)+
apply (intro conjI; clarsimp split: cap.splits arch_cap.splits vmpage_size.splits)
by (auto simp: valid_cap_def obj_at_def simps is_master_reply_cap_def
a_type_def data_at_def vspace_bits_defs X
elim!: tcb_cap_valid_imp_NullCap[rule_format, rotated]
split: cap.splits arch_cap.splits vmpage_size.splits) *)
crunches set_vm_root
for ptes_of[wp]: "\<lambda>s. P (ptes_of s)"
(* FIXME AARCH64 and asid_pools_of[wp]: "\<lambda>s. P (asid_pools_of s)" *)
@ -830,6 +1331,60 @@ lemma arch_finalise_cap_replaceable:
apply (clarsimp simp: valid_cap_def wellformed_mapdata_def cap_aligned_def)
done *)
(* FIXME AARCH64 this is the ARM_HYP formulation of arch_finalise_cap_replaceable
lemma arch_finalise_cap_replaceable1:
notes strg = tcb_cap_valid_imp_NullCap
obj_at_not_live_valid_arch_cap_strg[where cap=cap]
notes simps = replaceable_def and_not_not_or_imp
vs_lookup_pages_eq_at[THEN fun_cong, symmetric]
vs_lookup_pages_eq_ap[THEN fun_cong, symmetric]
is_cap_simps vs_cap_ref_def
no_cap_to_obj_with_diff_ref_Null o_def
notes wps = hoare_drop_imp[where R="%_. is_final_cap' cap" for cap]
unmap_page_table_unmapped3 valid_cap_typ
assumes X: "\<forall>r. cap \<noteq> VCPUCap r"
shows
"\<lbrace>\<lambda>s. s \<turnstile> cap.ArchObjectCap cap \<and>
x = is_final_cap' (cap.ArchObjectCap cap) s \<and>
pspace_aligned s \<and> valid_vspace_objs s \<and> valid_objs s \<and>
valid_asid_table (arm_asid_table (arch_state s)) s\<rbrace>
arch_finalise_cap cap x
\<lbrace>\<lambda>rv s. replaceable s sl (fst rv) (cap.ArchObjectCap cap)\<rbrace>"
apply (simp add: arch_finalise_cap_def)
apply (rule hoare_pre)
apply (simp add: simps split: option.splits vmpage_size.splits)
apply (wp wps
| strengthen strg
| simp add: simps reachable_pg_cap_def live_def
| wpc)+
(* unmap_page case is a bit unpleasant *)
apply (strengthen cases_conj_strg[where P="\<not> is_final_cap' cap s" for cap s, simplified])
apply (rule hoare_post_imp, clarsimp split: vmpage_size.split, assumption)
apply (simp add: vspace_bits_defs)
apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift hoare_vcg_const_imp_lift
unmap_page_tcb_cap_valid unmap_page_page_unmapped
unmap_page_section_unmapped)[1]
apply (wp wps
| strengthen strg imp_and_strg tcb_cap_valid_imp_NullCap
| simp add: simps is_master_reply_cap_def reachable_pg_cap_def
| wpc)+
apply (intro conjI; clarsimp split: cap.splits arch_cap.splits vmpage_size.splits)
by (auto simp: valid_cap_def obj_at_def simps is_master_reply_cap_def
a_type_def data_at_def vspace_bits_defs X
elim!: tcb_cap_valid_imp_NullCap[rule_format, rotated]
split: cap.splits arch_cap.splits vmpage_size.splits)
lemma arch_finalise_cap_replaceable:
shows
"\<lbrace>\<lambda>s. s \<turnstile> cap.ArchObjectCap cap \<and>
x = is_final_cap' (cap.ArchObjectCap cap) s \<and>
pspace_aligned s \<and> valid_vspace_objs s \<and> valid_objs s \<and>
valid_asid_table (arm_asid_table (arch_state s)) s\<rbrace>
arch_finalise_cap cap x
\<lbrace>\<lambda>rv s. replaceable s sl (fst rv) (cap.ArchObjectCap cap)\<rbrace>"
by (cases cap; simp add: arch_finalise_cap_vcpu arch_finalise_cap_replaceable1)
*)
global_naming Arch
lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]:
@ -885,6 +1440,13 @@ lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]:
apply (clarsimp dest!: obj_ref_none_no_asid[rule_format])
done
lemma dissociate_vcpu_tcb_no_cap_to_obj_ref[wp]:
"\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
dissociate_vcpu_tcb v t
\<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>"
sorry (* FIXME AARCH64 VCPU
by (wpsimp simp: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state) *)
lemma prepare_thread_delete_no_cap_to_obj_ref[wp]:
"\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
prepare_thread_delete t
@ -895,7 +1457,8 @@ lemma prepare_thread_delete_no_cap_to_obj_ref[wp]:
lemma prepare_thread_delete_unlive_hyp:
"\<lbrace>obj_at \<top> ptr\<rbrace> prepare_thread_delete ptr \<lbrace>\<lambda>rv. obj_at (Not \<circ> hyp_live) ptr\<rbrace>"
apply (simp add: prepare_thread_delete_def)
apply (wpsimp simp: obj_at_def is_tcb_def hyp_live_def)
apply (wpsimp wp: hoare_vcg_imp_lift arch_thread_get_wp)
apply (clarsimp simp: obj_at_def is_tcb_def hyp_live_def)
sorry (* FIXME AARCH64 VCPU
done *)
@ -982,13 +1545,15 @@ lemma arch_thread_set_cte_wp_at[wp]:
apply (clarsimp simp: tcb_cnode_map_def)+
done
(* FIXME AARCH64 VCPU/FPU
crunch cte_wp_at[wp,Finalise_AI_asms]: prepare_thread_delete "\<lambda>s. P (cte_wp_at P' p s)" *)
crunch cte_wp_at[wp,Finalise_AI_asms]: dissociate_vcpu_tcb "\<lambda>s. P (cte_wp_at P' p s)"
(simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set)
crunch cte_wp_at[wp,Finalise_AI_asms]: prepare_thread_delete "\<lambda>s. P (cte_wp_at P' p s)"
(simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set)
(* FIXME AARCH64 VCPU/FPU
crunch cte_wp_at[wp,Finalise_AI_asms]: arch_finalise_cap "\<lambda>s. P (cte_wp_at P' p s)"
(simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at
ignore: arch_thread_set) *)
(simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set)
end
interpretation Finalise_AI_1?: Finalise_AI_1
@ -1039,20 +1604,42 @@ interpretation Finalise_AI_2?: Finalise_AI_2
context Arch begin global_naming AARCH64
(* FIXME AARCH64 VCPU/FPU
crunch irq_node[Finalise_AI_asms,wp]: prepare_thread_delete "\<lambda>s. P (interrupt_irq_node s)" *)
crunches
vcpu_update, vgic_update, vcpu_disable, vcpu_restore, vcpu_save_reg_range, vgic_update_lr,
vcpu_save, vcpu_switch
for irq_node[wp]: "\<lambda>s. P (interrupt_irq_node s)"
(wp: crunch_wps subset_refl)
crunch irq_node[Finalise_AI_asms,wp]: prepare_thread_delete "\<lambda>s. P (interrupt_irq_node s)"
(wp: crunch_wps select_wp simp: crunch_simps)
crunch irq_node[wp]: arch_finalise_cap "\<lambda>s. P (interrupt_irq_node s)"
(simp: crunch_simps wp: crunch_wps)
crunch pred_tcb_at[wp]:
delete_asid_pool, delete_asid, unmap_page_table, unmap_page
delete_asid_pool, delete_asid, unmap_page_table, unmap_page, vcpu_invalidate_active
"pred_tcb_at proj P t"
(simp: crunch_simps wp: crunch_wps test)
(* FIXME AARCH64 VCPU
crunch pred_tcb_at[wp_unsafe]: arch_finalise_cap "pred_tcb_at proj P t"
(simp: crunch_simps wp: crunch_wps) *)
(simp: crunch_simps wp: crunch_wps)
(* FIXME AARCH64
crunch empty[wp]: find_free_hw_asid, store_hw_asid, load_hw_asid, set_vm_root_for_flush, page_table_mapped, invalidate_tlb_by_asid
"\<lambda>s. P (obj_at (empty_table {}) word s)" *)
lemma set_vcpu_empty[wp]:
"\<lbrace>\<lambda>s. P (obj_at (empty_table {}) word s)\<rbrace> set_vcpu p v \<lbrace>\<lambda>_ s. P (obj_at (empty_table {}) word s)\<rbrace>"
apply (rule set_vcpu.vsobj_at)
apply (clarsimp simp: vspace_obj_pred_def empty_table_def
split: kernel_object.splits arch_kernel_obj.splits)
done
crunches
vcpu_update, vgic_update, vcpu_disable, vcpu_restore, vcpu_save_reg_range, vgic_update_lr,
vcpu_save, vcpu_switch
for empty[wp]: "\<lambda>s. P (obj_at (empty_table {}) word s)"
(wp: crunch_wps subset_refl)
definition
replaceable_or_arch_update :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool" where
@ -1109,15 +1696,19 @@ lemma is_arch_update_reset_page:
apply (simp add: is_arch_update_def is_arch_cap_def cap_master_cap_def)
done
(* FIXME AARCH64 VCPU
crunch caps_of_state [wp]: vcpu_finalise "\<lambda>s. P (caps_of_state s)"
(wp: crunch_wps)
crunch caps_of_state [wp]: arch_finalise_cap "\<lambda>s. P (caps_of_state s)"
(wp: crunch_wps simp: crunch_simps) *)
(wp: crunch_wps simp: crunch_simps)
lemma set_vm_root_empty[wp]:
"\<lbrace>\<lambda>s. P (obj_at (empty_table S) p s)\<rbrace> set_vm_root v \<lbrace>\<lambda>_ s. P (obj_at (empty_table S) p s) \<rbrace>"
apply (simp add: set_vm_root_def)
apply (wpsimp wp: get_cap_wp)
sorry (* FIXME AARCH64
apply wpsimp+
apply (clarsimp simp: if_apply_def2)
apply (wpsimp+ | rule hoare_conjI[rotated] hoare_drop_imp hoare_allI)+
done *)
lemma set_asid_pool_empty[wp]:
@ -1178,9 +1769,8 @@ lemma replaceable_or_arch_update_pg:
global_naming Arch
(* FIXME AARCH64 FPU
crunch invs[wp]: prepare_thread_delete invs
(ignore: set_object) *)
(ignore: set_object)
lemma (* finalise_cap_invs *)[Finalise_AI_asms]:
shows "\<lbrace>invs and cte_wp_at ((=) cap) slot\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv. invs\<rbrace>"
@ -1363,6 +1953,7 @@ crunches unmap_page_table, store_pte, delete_asid_pool
for valid_cap[wp]: "valid_cap c"
(wp: mapM_wp_inv mapM_x_wp' simp: crunch_simps)
lemmas vcpu_finalise_typ_ats [wp] = abs_typ_at_lifts [OF vcpu_finalise_typ_at]
lemmas delete_asid_typ_ats[wp] = abs_typ_at_lifts [OF delete_asid_typ_at]
lemma arch_finalise_cap_valid_cap[wp]:

40
proof/invariant-abstract/AARCH64/ArchInterrupt_AI.thy
View File

@ -1,4 +1,5 @@
(*
* Copyright 2022, Proofcraft Pty Ltd
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
@ -231,10 +232,45 @@ lemma halted_eq:
"halted st = (st = Inactive \<or> st = IdleThreadState)"
by (cases st; simp)
crunches vgic_update, vgic_update_lr, vcpu_update for ex_nonz_cap_to[wp]: "ex_nonz_cap_to p"
(wp: ex_nonz_cap_to_pres)
lemma vgic_maintenance_invs[wp]:
"\<lbrace>invs\<rbrace> vgic_maintenance \<lbrace>\<lambda>_. invs\<rbrace>"
unfolding vgic_maintenance_def
supply if_split[split del] valid_fault_def[simp]
apply (wpsimp simp: get_gic_vcpu_ctrl_misr_def get_gic_vcpu_ctrl_eisr1_def
get_gic_vcpu_ctrl_eisr0_def if_apply_def2
wp: thread_get_wp' hoare_vcg_imp_lift' gts_wp hoare_vcg_all_lift
| wps
| wp (once) hoare_drop_imp[where f="do_machine_op m" for m]
hoare_drop_imp[where f="return $ m" for m]
| strengthen not_pred_tcb_at_strengthen
| wp (once) hoare_vcg_imp_lift' gts_wp)+
apply (frule tcb_at_invs)
apply (clarsimp simp: runnable_eq halted_eq not_pred_tcb)
apply (fastforce intro!: st_tcb_ex_cap[where P=active]
simp: not_pred_tcb st_tcb_at_def obj_at_def halted_eq)
done
lemma vppi_event_invs[wp]:
"\<lbrace>invs\<rbrace> vppi_event irq \<lbrace>\<lambda>_. invs\<rbrace>"
unfolding vppi_event_def
supply if_split[split del] valid_fault_def[simp]
apply (wpsimp simp: if_apply_def2
wp: hoare_vcg_imp_lift' gts_wp hoare_vcg_all_lift maskInterrupt_invs
cong: vcpu.fold_congs
| wps
| strengthen not_pred_tcb_at_strengthen)+
apply (frule tcb_at_invs)
apply (clarsimp simp: runnable_eq halted_eq not_pred_tcb)
apply (fastforce intro!: st_tcb_ex_cap[where P=active]
simp: not_pred_tcb st_tcb_at_def obj_at_def halted_eq)
done
lemma handle_reserved_irq_invs[wp]:
"\<lbrace>invs\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>_. invs\<rbrace>"
sorry (* FIXME AARCH64 VCPU vppi_event
unfolding handle_reserved_irq_def by (wpsimp simp: non_kernel_IRQs_def) *)
unfolding handle_reserved_irq_def by (wpsimp simp: non_kernel_IRQs_def)
lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]:
"\<lbrace>invs\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. invs\<rbrace>"

11
proof/invariant-abstract/AARCH64/ArchRetype_AI.thy
View File

@ -472,8 +472,15 @@ lemma hyp_refs_eq:
"state_hyp_refs_of s' = state_hyp_refs_of s"
unfolding s'_def ps_def
sorry (* FIXME AARCH64 VCPU
by (rule ext) (clarsimp simp: state_hyp_refs_of_def split: option.splits) *)
apply (rule ext)
apply (clarsimp simp: state_hyp_refs_of_def orthr split: option.splits)
apply (cases ty; simp add: tyunt default_object_def default_tcb_def hyp_refs_of_def tcb_hyp_refs_def
default_arch_tcb_def)
apply (rename_tac ao)
apply (clarsimp simp: refs_of_a_def ARM_HYP.vcpu_tcb_refs_def default_arch_object_def
ARM_A.default_vcpu_def
split: aobject_type.splits)
done *)
lemma obj_at_valid_pte:
"\<lbrakk>valid_pte level pte s; \<And>P p. obj_at P p s \<Longrightarrow> obj_at P p s'\<rbrakk>

17
proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy
View File

@ -32,10 +32,8 @@ global_naming Arch
lemma arch_stt_invs [wp,Schedule_AI_asms]:
"\<lbrace>invs\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: arch_switch_to_thread_def)
apply wp
sorry (* FIXME AARCH64 VCPU
done *)
apply (wpsimp simp: arch_switch_to_thread_def)
by (rule sym_refs_VCPU_hyp_live; fastforce)
lemma arch_stt_tcb [wp,Schedule_AI_asms]:
"\<lbrace>tcb_at t'\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. tcb_at t'\<rbrace>"
@ -56,6 +54,17 @@ lemma idle_strg:
by (clarsimp simp: invs_def valid_state_def valid_idle_def cur_tcb_def
pred_tcb_at_def valid_machine_state_def obj_at_def is_tcb_def)
lemma set_vcpu_ct[wp]:
"\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> set_vcpu v v' \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>"
by (wpsimp simp: set_vcpu_def wp: get_object_wp)
crunches
vcpu_update, vgic_update, vgic_update_lr, vcpu_restore_reg_range, vcpu_save_reg_range,
vcpu_enable, vcpu_disable, vcpu_save, vcpu_restore, vcpu_switch, vcpu_save
for it[wp]: "\<lambda>s. P (idle_thread s)"
and ct[wp]: "\<lambda>s. P (cur_thread s)"
(wp: mapM_x_wp mapM_wp subset_refl)
lemma arch_stit_invs[wp, Schedule_AI_asms]:
"\<lbrace>invs\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. invs\<rbrace>"
sorry (* FIXME AARCH64 VSpace & VCPU

674
proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy Normal file
View File

@ -0,0 +1,674 @@
(*
* Copyright 2022, Proofcraft Pty Ltd
* Copyright 2022, UNSW (ABN 57 195 873 197)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory ArchVCPU_AI
imports AInvs
begin
context Arch begin global_naming ARM_HYP (*FIXME: arch_split*)
(* FIXME AARCH64: move to ArchInvariants_AI and use there *)
definition active_cur_vcpu_of :: "'z state \<Rightarrow> obj_ref option" where
"active_cur_vcpu_of s \<equiv> case arm_current_vcpu (arch_state s) of Some (vr, True) \<Rightarrow> Some vr
| _ \<Rightarrow> None"
definition valid_cur_vcpu :: "'z::state_ext state \<Rightarrow> bool" where
"valid_cur_vcpu s \<equiv> arch_tcb_at (\<lambda>itcb. itcb_vcpu itcb = active_cur_vcpu_of s) (cur_thread s) s"
lemma valid_cur_vcpu_lift_ct_Q:
assumes arch_tcb_of_cur_thread: "\<And>P. \<lbrace>\<lambda>s. arch_tcb_at P (cur_thread s) s \<and> Q s\<rbrace>
f \<lbrace>\<lambda>_ s. arch_tcb_at P (cur_thread s) s\<rbrace>"
and active_cur_vcpu_of: "\<And>P. \<lbrace>\<lambda>s. P (active_cur_vcpu_of s) \<and> Q s\<rbrace>
f \<lbrace>\<lambda>_ s. P (active_cur_vcpu_of s)\<rbrace>"
shows "\<lbrace>\<lambda>s. valid_cur_vcpu s \<and> Q s\<rbrace> f \<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
unfolding valid_cur_vcpu_def valid_def
using use_valid[OF _ active_cur_vcpu_of] use_valid[OF _ arch_tcb_of_cur_thread]
by (fastforce simp: active_cur_vcpu_of_def)
lemmas valid_cur_vcpu_lift_ct = valid_cur_vcpu_lift_ct_Q[where Q=\<top>, simplified]
lemma valid_cur_vcpu_lift:
"\<lbrakk>\<And>P. f \<lbrace>\<lambda>s. P (active_cur_vcpu_of s)\<rbrace>; \<And>P t. f \<lbrace>\<lambda>s. arch_tcb_at P t s\<rbrace>;
\<And>P. f \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace>\<rbrakk> \<Longrightarrow>
f \<lbrace>valid_cur_vcpu\<rbrace>"
apply (rule valid_cur_vcpu_lift_ct)
apply (rule_tac f=cur_thread in hoare_lift_Pf3)
apply fastforce+
done
lemma valid_cur_vcpu_lift_weak:
"\<lbrakk>\<And>P. f \<lbrace>\<lambda>s. P (arch_state s)\<rbrace>; \<And>P t. f \<lbrace>\<lambda>s. arch_tcb_at P t s\<rbrace>;
\<And>P. f \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace>\<rbrakk> \<Longrightarrow>
f \<lbrace>valid_cur_vcpu\<rbrace>"
apply (rule valid_cur_vcpu_lift_ct)
apply (rule_tac f=cur_thread in hoare_lift_Pf3)
apply fastforce+
apply (clarsimp simp: valid_cur_vcpu_def valid_def)
by (fastforce simp: active_cur_vcpu_of_def)
lemma valid_cur_vcpu_lift_cur_thread_update:
assumes arch_tcb_at: "\<And>P. f \<lbrace>arch_tcb_at P t\<rbrace>"
and active_cur_vcpu_of: "\<And>P. f \<lbrace>\<lambda>s. P (active_cur_vcpu_of s)\<rbrace>"
shows "f \<lbrace>\<lambda>s. valid_cur_vcpu (s\<lparr>cur_thread := t\<rparr>)\<rbrace>"
unfolding valid_cur_vcpu_def valid_def
using use_valid[OF _ active_cur_vcpu_of] use_valid[OF _ arch_tcb_at]
by (fastforce simp: active_cur_vcpu_of_def)
crunches as_user
for active_cur_vcpu_of[wp]: "\<lambda>s. P (active_cur_vcpu_of s)"
(wp: crunch_wps simp: active_cur_vcpu_of_def)
lemma as_user_valid_cur_vcpu[wp]:
"as_user tptr f \<lbrace>valid_cur_vcpu\<rbrace>"
by (rule valid_cur_vcpu_lift; wpsimp wp: as_user_pred_tcb_at)
lemma machine_state_update_active_cur_vcpu_of[simp]:
"P (active_cur_vcpu_of (s\<lparr>machine_state := ms\<rparr>)) = P (active_cur_vcpu_of s)"
by (fastforce simp: active_cur_vcpu_of_def)
crunches do_machine_op
for valid_cur_vcpu[wp]: valid_cur_vcpu
and valid_cur_vcpu_cur_thread_update[wp]: "\<lambda>s. valid_cur_vcpu (s\<lparr>cur_thread := t\<rparr>)"
(wp: valid_cur_vcpu_lift_cur_thread_update valid_cur_vcpu_lift crunch_wps)
lemma valid_cur_vcpu_vcpu_update[simp]:
"vcpu_at v s \<Longrightarrow> valid_cur_vcpu (s\<lparr>kheap := kheap s(v \<mapsto> ArchObj (VCPU vcpu))\<rparr>) = valid_cur_vcpu s"
by (clarsimp simp: valid_cur_vcpu_def active_cur_vcpu_of_def pred_tcb_at_def obj_at_def)
crunches vcpu_save_reg, vcpu_write_reg, save_virt_timer, vgic_update, vcpu_disable
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: set_vcpu_wp)
lemma set_vcpu_arch_tcb_at_cur_thread[wp]:
"set_vcpu ptr vcpu \<lbrace>\<lambda>s. arch_tcb_at P (cur_thread s) s\<rbrace>"
apply (wpsimp wp: set_vcpu_wp get_vcpu_wp)
apply (clarsimp simp: pred_tcb_at_def obj_at_def)
done
crunches vcpu_disable, vcpu_restore, vcpu_save, set_vm_root
for arch_tcb_at_cur_thread[wp]: "\<lambda>s. arch_tcb_at P (cur_thread s) s"
(wp: crunch_wps ignore: set_object) (* FIXME AARCH64: set_object shouldn't be here *)
lemma invalidate_asid_active_cur_vcpu_of[wp]:
"\<lbrace>\<lambda>s. P (active_cur_vcpu_of s)\<rbrace> invalidate_asid param_a \<lbrace>\<lambda>_ s. P (active_cur_vcpu_of s)\<rbrace>"
sorry (* FIXME AARCH64: crunch was able to deal with this on ARM_HYP with old defs *)
crunches vcpu_update, do_machine_op, invalidate_asid
for active_cur_vcpu_of[wp]: "\<lambda>s. P (active_cur_vcpu_of s)"
(simp: active_cur_vcpu_of_def)
lemma vcpu_save_reg_active_cur_vcpu_of[wp]:
"vcpu_save_reg vr reg \<lbrace>\<lambda>s. P (active_cur_vcpu_of s)\<rbrace>"
by (wpsimp simp: vcpu_save_reg_def)
crunches vcpu_restore, do_machine_op, vcpu_save_reg, vgic_update, save_virt_timer,
vcpu_save_reg_range, vgic_update_lr, vcpu_enable, vcpu_save, set_vcpu
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift crunch_wps simp: active_cur_vcpu_of_def)
lemma switch_vcpu_valid_cur_vcpu_cur_thread_update[wp]:
"\<lbrace>arch_tcb_at (\<lambda>itcb. itcb_vcpu itcb = v) t\<rbrace>
vcpu_switch v
\<lbrace>\<lambda>_ s. valid_cur_vcpu (s\<lparr>cur_thread := t\<rparr>)\<rbrace>"
unfolding vcpu_switch_def
apply (wpsimp simp: valid_cur_vcpu_def active_cur_vcpu_of_def)
by fastforce
lemma switch_vcpu_valid_cur_vcpu[wp]:
"\<lbrace>\<lambda>s. arch_tcb_at (\<lambda>itcb. itcb_vcpu itcb = v) (cur_thread s) s\<rbrace>
vcpu_switch v
\<lbrace>\<lambda>_ s. valid_cur_vcpu s\<rbrace>"
unfolding vcpu_switch_def
apply (wpsimp simp: valid_cur_vcpu_def active_cur_vcpu_of_def)
by (clarsimp simp: pred_tcb_at_def obj_at_def)
lemma active_cur_vcpu_of_arm_vmid_table_upd[simp]:
"active_cur_vcpu_of (s\<lparr>arch_state := arch_state s \<lparr>arm_vmid_table := x \<rparr>\<rparr>) = active_cur_vcpu_of s"
by (clarsimp simp: active_cur_vcpu_of_def pred_tcb_at_def obj_at_def valid_cur_vcpu_def)
lemma valid_cur_vcpu_arm_vmid_table_upd[simp]:
"valid_cur_vcpu (s\<lparr>arch_state := arch_state s \<lparr>arm_vmid_table := x \<rparr>\<rparr>) = valid_cur_vcpu s"
by (clarsimp simp: valid_cur_vcpu_def)
lemma get_vmid_active_cur_vcpu_of[wp]:
"get_vmid asid \<lbrace>\<lambda>s. P (active_cur_vcpu_of s)\<rbrace>"
unfolding get_vmid_def
sorry (* FIXME AARCH64 crunches/vmid? *)
lemma store_vmid_active_cur_vcpu_of[wp]:
"store_vmid asid p \<lbrace>\<lambda>s. P (active_cur_vcpu_of s)\<rbrace>"
unfolding store_vmid_def
sorry (* FIXME AARCH64 crunches/vmid? *)
lemma arm_context_switch_active_cur_vcpu_of[wp]:
"arm_context_switch pd asid \<lbrace>\<lambda>s. P (active_cur_vcpu_of s)\<rbrace>"
unfolding arm_context_switch_def get_vmid_def
apply (wpsimp wp: load_vmid_wp)
sorry (* FIXME AARCH64 crunches/vmid? *)
lemma set_vm_root_active_cur_vcpu_of[wp]:
"set_vm_root tcb \<lbrace>\<lambda>s. P (active_cur_vcpu_of s)\<rbrace>"
sorry (* FIXME AARCH64 missing crunches
by (wpsimp simp: set_vm_root_def wp: get_cap_wp) *)
crunches set_vm_root
for valid_cur_vcpu_cur_thread_update[wp]: "\<lambda>s. valid_cur_vcpu (s\<lparr>cur_thread := t\<rparr>)"
(wp: valid_cur_vcpu_lift_cur_thread_update)
lemma arch_switch_to_thread_valid_cur_vcpu_cur_thread_update[wp]:
"\<lbrace>valid_cur_vcpu\<rbrace>
arch_switch_to_thread t
\<lbrace>\<lambda>_ s. valid_cur_vcpu (s\<lparr>cur_thread := t\<rparr>)\<rbrace>"
unfolding arch_switch_to_thread_def
apply wpsimp
by (fastforce simp: active_cur_vcpu_of_def pred_tcb_at_def obj_at_def get_tcb_def
split: option.splits kernel_object.splits)
lemma switch_to_thread_valid_cur_vcpu[wp]:
"switch_to_thread t \<lbrace>valid_cur_vcpu\<rbrace>"
unfolding switch_to_thread_def
by (wpsimp simp: valid_cur_vcpu_def active_cur_vcpu_of_def)
lemma arch_switch_to_idle_thread_valid_cur_vcpu_cur_thread_update[wp]:
"\<lbrace>\<lambda>s. valid_cur_vcpu s \<and> valid_idle s \<and> t = idle_thread s\<rbrace>
arch_switch_to_idle_thread
\<lbrace>\<lambda>_ s. valid_cur_vcpu (s\<lparr>cur_thread := t\<rparr>)\<rbrace>"
unfolding arch_switch_to_idle_thread_def
apply wpsimp
sorry (* FIXME AARCH64
by (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def valid_arch_idle_def) *)
lemma switch_to_idle_thread_valid_cur_vcpu[wp]:
"\<lbrace>valid_cur_vcpu and valid_idle\<rbrace>
switch_to_idle_thread
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
sorry (* FIXME AARCH64 arch_switch_to_idle_thread
by (wpsimp simp: switch_to_idle_thread_def) *)
lemma tcb_vcpu_update_empty_valid_cur_vcpu[wp]:
"\<lbrace>\<lambda>s. if t = cur_thread s
then arm_current_vcpu (arch_state s) = None
else valid_cur_vcpu s\<rbrace>
arch_thread_set (tcb_vcpu_update Map.empty) t
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
apply (wpsimp wp: arch_thread_set_wp)
by (clarsimp simp: valid_cur_vcpu_def pred_tcb_at_def active_cur_vcpu_of_def obj_at_def)
lemma vcpu_invalidate_active_valid_cur_vcpu[wp]:
"\<lbrace>\<lambda>s. arm_current_vcpu (arch_state s) \<noteq> None
\<and> arch_tcb_at (\<lambda>itcb. itcb_vcpu itcb = None) (cur_thread s) s\<rbrace>
vcpu_invalidate_active
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
unfolding vcpu_invalidate_active_def
by (wpsimp simp: valid_cur_vcpu_def active_cur_vcpu_of_def)
lemma vcpu_invalid_active_arm_current_vcpu_None[wp]:
"\<lbrace>\<top>\<rbrace> vcpu_invalidate_active \<lbrace>\<lambda>_ s. arm_current_vcpu (arch_state s) = None\<rbrace>"
unfolding vcpu_invalidate_active_def
by wpsimp
lemma dissociate_vcpu_tcb_valid_cur_vcpu[wp]:
"\<lbrace>\<lambda>s. valid_cur_vcpu s \<and> sym_refs (state_hyp_refs_of s)\<rbrace>
dissociate_vcpu_tcb vr t
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
unfolding dissociate_vcpu_tcb_def
apply (wpsimp wp: hoare_vcg_imp_lift' arch_thread_get_wp get_vcpu_wp)
by (fastforce simp: valid_cur_vcpu_def pred_tcb_at_def obj_at_def active_cur_vcpu_of_def
sym_refs_def state_hyp_refs_of_def
split: bool.splits option.splits)
lemma associate_vcpu_tcb_valid_cur_vcpu:
"\<lbrace>\<lambda>s. valid_cur_vcpu s \<and> sym_refs (state_hyp_refs_of s)\<rbrace>
associate_vcpu_tcb vr t
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
unfolding associate_vcpu_tcb_def
sorry (* FIXME AARCH64 something going on with _2 rephrase of valid_cur_vcpu
apply (wpsimp wp: hoare_vcg_imp_lift')
apply (wpsimp wp: arch_thread_set_wp)
apply (wpsimp wp: arch_thread_set_wp)
apply (rule_tac Q="\<lambda>_ s. valid_cur_vcpu s \<and> sym_refs (state_hyp_refs_of s)" in hoare_post_imp)
apply (clarsimp simp: pred_tcb_at_def obj_at_def valid_cur_vcpu_def active_cur_vcpu_of_def)
by (wpsimp wp: get_vcpu_wp hoare_drop_imps)+ *)
lemma set_thread_state_arch_tcb_at[wp]:
"set_thread_state ts ref \<lbrace>arch_tcb_at P t\<rbrace>"
unfolding set_thread_state_def
apply (wpsimp wp: set_object_wp)
by (clarsimp simp: pred_tcb_at_def obj_at_def get_tcb_def)
crunches set_thread_state
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift_weak)
crunches activate_thread
for valid_cur_vcpu[wp]: valid_cur_vcpu
crunches tcb_sched_action
for arch_tcb_at[wp]: "arch_tcb_at P t"
(simp: tcb_sched_action_def set_tcb_queue_def get_tcb_queue_def)
crunches tcb_sched_action
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift_weak)
crunches schedule_choose_new_thread
for valid_cur_vcpu[wp]: valid_cur_vcpu
(simp: crunch_simps valid_cur_vcpu_def active_cur_vcpu_of_def wp: crunch_wps)
lemma schedule_valid_cur_vcpu_det_ext[wp]:
"\<lbrace>valid_cur_vcpu and valid_idle\<rbrace>
(schedule :: (unit, det_ext) s_monad)
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
unfolding schedule_def schedule_switch_thread_fastfail_def ethread_get_when_def ethread_get_def
by (wpsimp wp: hoare_drop_imps gts_wp)
lemma schedule_valid_cur_vcpu[wp]:
"\<lbrace>valid_cur_vcpu and valid_idle\<rbrace>
(schedule :: (unit, unit) s_monad)
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
unfolding schedule_def allActiveTCBs_def
by (wpsimp wp: alternative_wp select_wp)
crunches cancel_all_ipc, blocked_cancel_ipc, unbind_maybe_notification, cancel_all_signals,
bind_notification, fast_finalise, deleted_irq_handler, post_cap_deletion, cap_delete_one,
reply_cancel_ipc, cancel_ipc, update_waiting_ntfn, send_signal, send_ipc, send_fault_ipc,
receive_ipc, handle_fault, handle_interrupt, handle_vm_fault, handle_hypervisor_fault,
send_signal, do_reply_transfer, unbind_notification, suspend, cap_swap, bind_notification,
restart, reschedule_required, possible_switch_to, thread_set_priority, reply_from_kernel
for arch_state[wp]: "\<lambda>s. P (arch_state s)"
and cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
(wp: mapM_x_wp_inv thread_set.arch_state select_wp crunch_wps
simp: crunch_simps possible_switch_to_def reschedule_required_def)
lemma do_unbind_notification_arch_tcb_at[wp]:
"do_unbind_notification ntfnptr ntfn tcbptr \<lbrace>arch_tcb_at P t\<rbrace>"
unfolding set_bound_notification_def set_simple_ko_def
apply (wpsimp wp: set_object_wp get_object_wp get_simple_ko_wp thread_get_wp)
by (fastforce simp: pred_tcb_at_def obj_at_def get_tcb_def)
lemma unbind_notification_arch_tcb_at[wp]:
"unbind_notification tcb \<lbrace>arch_tcb_at P t\<rbrace>"
unfolding unbind_notification_def
by wpsimp
lemma bind_notification_arch_tcb_at[wp]:
"bind_notification tcbptr ntfnptr \<lbrace>arch_tcb_at P t\<rbrace>"
unfolding bind_notification_def set_bound_notification_def set_simple_ko_def
apply (wpsimp wp: set_object_wp get_object_wp get_simple_ko_wp)
by (fastforce simp: pred_tcb_at_def obj_at_def get_tcb_def)
lemma unbind_maybe_notification_arch_tcb_at[wp]:
"unbind_maybe_notification ntfnptr \<lbrace>arch_tcb_at P t\<rbrace>"
unfolding unbind_maybe_notification_def
by wpsimp
crunches blocked_cancel_ipc, cap_delete_one, cancel_signal
for arch_tcb_at[wp]: "arch_tcb_at P t"
(wp: crunch_wps simp: crunch_simps)
lemma reply_cancel_ipc_arch_tcb_at[wp]:
"reply_cancel_ipc ntfnptr \<lbrace>arch_tcb_at P t\<rbrace>"
unfolding reply_cancel_ipc_def thread_set_def
apply (wpsimp wp: set_object_wp select_wp)
by (clarsimp simp: pred_tcb_at_def obj_at_def get_tcb_def)
crunches cancel_ipc, send_ipc, receive_ipc
for arch_tcb_at[wp]: "arch_tcb_at P t"
(wp: crunch_wps simp: crunch_simps)
lemma send_fault_ipc_arch_tcb_at[wp]:
"send_fault_ipc tptr fault \<lbrace>arch_tcb_at P t\<rbrace>"
unfolding send_fault_ipc_def thread_set_def Let_def
by (wpsimp wp: set_object_wp hoare_drop_imps hoare_vcg_all_lift_R
simp: pred_tcb_at_def obj_at_def get_tcb_def)
crunches handle_fault, handle_interrupt, handle_vm_fault, handle_hypervisor_fault, send_signal
for arch_tcb_at[wp]: "arch_tcb_at P t"
(wp: mapM_x_wp_inv crunch_wps)
crunches reschedule_required, set_scheduler_action, tcb_sched_action
for arch_tcb_at[wp]: "arch_tcb_at P t"
(simp: reschedule_required_def set_scheduler_action_def tcb_sched_action_def set_tcb_queue_def
get_tcb_queue_def)
lemma thread_set_fault_arch_tcb_at[wp]:
"thread_set (tcb_fault_update f) r \<lbrace>arch_tcb_at P t\<rbrace>"
unfolding thread_set_def
by (wpsimp wp: set_object_wp simp: pred_tcb_at_def obj_at_def get_tcb_def)
lemma do_reply_transfer_arch_tcb_at[wp]:
"do_reply_transfer sender receiver slot grant \<lbrace>arch_tcb_at P t\<rbrace>"
unfolding do_reply_transfer_def
by (wpsimp wp: gts_wp split_del: if_split)
crunches send_ipc, send_fault_ipc, receive_ipc, handle_fault, handle_interrupt, handle_vm_fault,
handle_hypervisor_fault, send_signal, do_reply_transfer, cancel_all_ipc,
cancel_all_signals, unbind_maybe_notification, suspend, deleting_irq_handler,
unbind_notification
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift_weak crunch_wps)
crunches init_arch_objects, reset_untyped_cap
for arch_state[wp]: "\<lambda>s. P (arch_state s)"
(wp: crunch_wps preemption_point_inv hoare_unless_wp mapME_x_wp'
simp: crunch_simps)
crunches invoke_untyped
for cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
and active_cur_vcpu_of[wp]: "\<lambda>s. P (active_cur_vcpu_of s)"
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv
simp: crunch_simps mapM_x_def[symmetric] active_cur_vcpu_of_def)
lemma invoke_untyped_valid_cur_vcpu:
"\<lbrace>valid_cur_vcpu and invs and valid_untyped_inv ui and ct_active\<rbrace>
invoke_untyped ui
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
apply (rule hoare_weaken_pre)
apply (rule valid_cur_vcpu_lift_ct_Q)
apply (rule_tac f=cur_thread in hoare_lift_Pf2)
apply (rule invoke_untyped_pred_tcb_at)
apply clarsimp
apply wpsimp
apply wpsimp
apply (fastforce simp: pred_tcb_at_def obj_at_def ct_in_state_def)
done
lemma valid_cur_vcpu_is_original_cap_update[simp]:
"valid_cur_vcpu (is_original_cap_update f s) = valid_cur_vcpu s"
by (clarsimp simp: valid_cur_vcpu_def pred_tcb_at_def obj_at_def active_cur_vcpu_of_def)
lemma active_cur_vcpu_of_arm_asid_table_update[simp]:
"P (active_cur_vcpu_of (s\<lparr>arch_state := arm_asid_table_update f (arch_state s)\<rparr>))
= P (active_cur_vcpu_of s)"
by (clarsimp simp: active_cur_vcpu_of_def)
crunches cap_insert, cap_move
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift_weak)
crunches suspend, unbind_notification, cap_swap_for_delete
for state_hyp_refs_of[wp]: "\<lambda>s. P (state_hyp_refs_of s)"
(wp: crunch_wps thread_set_hyp_refs_trivial select_wp simp: crunch_simps)
lemma prepare_thread_delete_valid_cur_vcpu[wp]:
"\<lbrace>\<lambda>s. valid_cur_vcpu s \<and> sym_refs (state_hyp_refs_of s)\<rbrace>
prepare_thread_delete p
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
unfolding prepare_thread_delete_def arch_thread_get_def
sorry (* FIXME AARCH64 FPU
by (wpsimp wp: dissociate_vcpu_tcb_valid_cur_vcpu) *)
crunches delete_asid_pool
for active_cur_vcpu_of[wp]: "\<lambda>s. P (active_cur_vcpu_of s)"
and cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
(wp: crunch_wps simp: crunch_simps)
crunches store_pte, set_asid_pool
for active_cur_vcpu_of[wp]: "\<lambda>s. P (active_cur_vcpu_of s)"
and cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
(wp: crunch_wps simp: crunch_simps active_cur_vcpu_of_def)
(* FIXME AARCH64 PTs
crunches unmap_page, unmap_page_table, delete_asid
for active_cur_vcpu_of[wp]: "\<lambda>s. P (active_cur_vcpu_of s)"
and cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
(wp: crunch_wps valid_cur_vcpu_lift) *)
(* FIXME AARCH64 invalidate_tlb_by_asid_va
crunches delete_asid_pool, unmap_page, unmap_page_table, delete_asid
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift) *)
(* FIXME AARCH64
crunches vcpu_finalise, arch_finalise_cap, finalise_cap
for valid_cur_vcpu[wp]: valid_cur_vcpu
(simp: crunch_simps) *)
crunches prepare_thread_delete, deleting_irq_handler, delete_asid_pool
for sym_refs_state_hyp_refs_of[wp]: "\<lambda>s. sym_refs (state_hyp_refs_of s)"
(wp: crunch_wps simp: crunch_simps)
lemmas store_pte_state_hyp_refs_of[wp] = store_pte_state_hyp_refs_of
lemma unmap_page_state_hyp_refs_of[wp]:
"unmap_page pgsz asid vptr pptr \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>"
unfolding unmap_page_def sorry (* FIXME AARCH64 lookup_pt_slot_def find_pd_for_asid_def
by (wpsimp wp: hoare_drop_imps mapM_wp_inv get_pde_wp store_pde_state_hyp_refs_of) *)
crunches delete_asid, vcpu_finalise, unmap_page_table, finalise_cap
for state_hyp_refs_of[wp]: "\<lambda>s. sym_refs (state_hyp_refs_of s)"
lemma preemption_point_state_hyp_refs_of[wp]:
"preemption_point \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>"
by (wpsimp wp: preemption_point_inv)
lemma preemption_point_valid_cur_vcpu[wp]:
"preemption_point \<lbrace>valid_cur_vcpu\<rbrace>"
apply (wpsimp wp: preemption_point_inv)
by (clarsimp simp: valid_cur_vcpu_def pred_tcb_at_def obj_at_def active_cur_vcpu_of_def)+
crunches cap_swap_for_delete, empty_slot
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift_weak)
lemma rec_del_sym_refs_state_hyp_refs_of[wp]:
"rec_del call \<lbrace>\<lambda>s. sym_refs (state_hyp_refs_of s)\<rbrace>"
by (rule rec_del_preservation; wpsimp)
crunches cap_delete
for state_hyp_refs_of[wp]: "\<lambda>s. sym_refs (state_hyp_refs_of s)"
lemma rec_del_valid_cur_vcpu[wp]:
"\<lbrace>\<lambda>s. valid_cur_vcpu s \<and> sym_refs (state_hyp_refs_of s)\<rbrace>
rec_del call
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
(is "\<lbrace>?pre\<rbrace> _ \<lbrace>_\<rbrace>")
apply (rule_tac Q="\<lambda>_. ?pre" in hoare_post_imp, fastforce)
sorry (* FIXME AARCH64
by (rule rec_del_preservation; wpsimp) *)
crunches cap_delete
for valid_cur_vcpu[wp]: valid_cur_vcpu
lemma cap_revoke_valid_cur_vcpu[wp]:
"\<lbrace>\<lambda>s. valid_cur_vcpu s \<and> sym_refs (state_hyp_refs_of s)\<rbrace>
cap_revoke slot
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
(is "\<lbrace>?pre\<rbrace> _ \<lbrace>_\<rbrace>")
apply (rule_tac Q="\<lambda>_. ?pre" in hoare_post_imp, fastforce)
by (wpsimp wp: cap_revoke_preservation)
crunches cancel_badged_sends, invoke_irq_control, invoke_irq_handler
for arch_tcb_at[wp]: "arch_tcb_at P t"
and cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
and arch_state[wp]: "\<lambda>s. P (arch_state s)"
(wp: filterM_preserved)
crunches store_pte, set_cap, set_mrs
for active_cur_vcpu_of[wp]: "\<lambda>s. P (active_cur_vcpu_of s)"
(simp: active_cur_vcpu_of_def)
crunches perform_page_table_invocation, perform_page_invocation,
perform_asid_pool_invocation, invoke_vcpu_inject_irq, invoke_vcpu_read_register,
invoke_vcpu_write_register, invoke_vcpu_ack_vppi
for arch_tcb_at[wp]: "arch_tcb_at P t"
and cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
and active_cur_vcpu_of[wp]: "\<lambda>s. P (active_cur_vcpu_of s)"
(wp: crunch_wps simp: crunch_simps)
crunches cancel_badged_sends, invoke_irq_control, invoke_irq_handler, invoke_vcpu_inject_irq,
bind_notification
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift_weak)
crunches perform_asid_pool_invocation, perform_page_table_invocation,
perform_page_invocation, invoke_vcpu_read_register,
invoke_vcpu_write_register, invoke_vcpu_ack_vppi
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift)
lemma invoke_cnode_valid_cur_vcpu[wp]:
"\<lbrace>\<lambda>s. valid_cur_vcpu s \<and> sym_refs (state_hyp_refs_of s)\<rbrace>
invoke_cnode i
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
unfolding invoke_cnode_def
by (wpc | wpsimp wp: hoare_drop_imps hoare_vcg_all_lift)+
lemma valid_cur_vcpu_trans_state[simp]:
"valid_cur_vcpu (trans_state f s) = valid_cur_vcpu s"
by (clarsimp simp: valid_cur_vcpu_def pred_tcb_at_def obj_at_def active_cur_vcpu_of_def)
crunches restart, reschedule_required, possible_switch_to, thread_set_priority
for arch_tcb_at[wp]: "arch_tcb_at P t"
(simp: possible_switch_to_def set_tcb_queue_def get_tcb_queue_def)
crunches restart, reschedule_required, possible_switch_to, thread_set_priority
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift_weak)
crunches restart, arch_post_modify_registers, arch_get_sanitise_register_info
for valid_cur_vcpu[wp]: valid_cur_vcpu
lemma thread_set_valid_cur_vcpu:
"(\<And>tcb. tcb_arch (f tcb) = tcb_arch tcb) \<Longrightarrow> thread_set f tptr \<lbrace>valid_cur_vcpu\<rbrace>"
apply (rule valid_cur_vcpu_lift_weak; (solves wpsimp)?)
unfolding thread_set_def
apply (wpsimp wp: set_object_wp)
apply (fastforce simp: pred_tcb_at_def obj_at_def get_tcb_def)
done
lemma fault_handler_update_valid_cur_vcpu[wp]:
"option_update_thread thread (tcb_fault_handler_update \<circ> f) opt \<lbrace>valid_cur_vcpu\<rbrace>"
unfolding option_update_thread_def
by (wpsimp wp: thread_set_valid_cur_vcpu)
lemma fault_handler_update_state_hyp_refs_of[wp]:
"option_update_thread thread (tcb_fault_handler_update \<circ> f) opt \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>"
unfolding option_update_thread_def
by (fastforce intro: thread_set_hyp_refs_trivial split: option.splits)
crunches set_mcpriority, set_priority
for valid_cur_vcpu[wp]: valid_cur_vcpu
(simp: set_priority_def)
lemma ethread_set_state_hyp_refs_of[wp]:
"ethread_set f t \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>"
unfolding ethread_set_def set_eobject_def
apply wp
apply (clarsimp dest!: get_tcb_SomeD)
done
crunches tcb_sched_action, possible_switch_to, set_scheduler_action, reschedule_required
for state_hyp_refs_of[wp]: "\<lambda>s. P (state_hyp_refs_of s)"
(simp: tcb_sched_action_def set_tcb_queue_def get_tcb_queue_def possible_switch_to_def
reschedule_required_def set_scheduler_action_def)
crunches set_mcpriority, set_priority
for state_hyp_refs_of[wp]: "\<lambda>s. P (state_hyp_refs_of s)"
(wp: thread_set_hyp_refs_trivial simp: set_priority_def thread_set_priority_def)
lemma invoke_tcb_valid_cur_vcpu[wp]:
"\<lbrace>\<lambda>s. valid_cur_vcpu s \<and> sym_refs (state_hyp_refs_of s)\<rbrace>
invoke_tcb iv
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
apply (cases iv; clarsimp; (solves \<open>wpsimp wp: mapM_x_wp_inv\<close>)?)
defer
subgoal for tcb_ptr ntfn_ptr_opt
by (case_tac ntfn_ptr_opt; wpsimp)
\<comment> \<open>ThreadControl\<close>
apply (forward_inv_step wp: check_cap_inv)+
by (wpsimp wp: check_cap_inv hoare_drop_imps thread_set_hyp_refs_trivial thread_set_valid_cur_vcpu)
crunches invoke_domain
for arch_state[wp]: "\<lambda>s. P (arch_state s)"
and arch_tcb_at[wp]: "arch_tcb_at P t"
and cur_thread[wp]: "\<lambda>s. P (cur_thread s)"
and valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift_weak)
crunches perform_asid_control_invocation
for cur_thread[wp]: "\<lambda>s. P (cur_thread s )"
and active_cur_vcpu_of[wp]: "\<lambda>s. P (active_cur_vcpu_of s)"
(simp: active_cur_vcpu_of_def)
lemma perform_asid_control_invocation_valid_cur_vcpu:
"\<lbrace>valid_cur_vcpu and invs and valid_aci iv and ct_active\<rbrace>
perform_asid_control_invocation iv
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
apply (rule hoare_weaken_pre)
apply (rule valid_cur_vcpu_lift_ct_Q)
apply (rule_tac f=cur_thread in hoare_lift_Pf2)
apply (rule perform_asid_control_invocation_pred_tcb_at)
apply wpsimp
apply wpsimp
apply (fastforce simp: pred_tcb_at_def obj_at_def ct_in_state_def)
done
lemma perform_vcpu_invocation_valid_cur_vcpu:
"\<lbrace>valid_cur_vcpu and invs\<rbrace> perform_vcpu_invocation iv \<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
unfolding perform_vcpu_invocation_def
by (wpsimp wp: associate_vcpu_tcb_valid_cur_vcpu)
lemma perform_invocation_valid_cur_vcpu[wp]:
"\<lbrace>valid_cur_vcpu and invs and valid_invocation iv and ct_active\<rbrace>
perform_invocation blocking call iv
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
apply (case_tac iv, simp_all; (solves wpsimp)?)
apply (wpsimp wp: invoke_untyped_valid_cur_vcpu)
unfolding arch_perform_invocation_def
apply (wpsimp wp: perform_vcpu_invocation_valid_cur_vcpu
perform_asid_control_invocation_valid_cur_vcpu)
sorry (* FIXME AARCH64 not all invocations go through, likely missing crunches
apply (fastforce simp: valid_arch_inv_def)
done *)
crunches reply_from_kernel, receive_signal
for valid_cur_vcpu[wp]: valid_cur_vcpu
(wp: valid_cur_vcpu_lift_weak)
lemma handle_invocation_valid_cur_vcpu[wp]:
"\<lbrace>valid_cur_vcpu and invs and ct_active\<rbrace> handle_invocation calling blocking \<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
unfolding handle_invocation_def
by (wp syscall_valid set_thread_state_ct_st
| simp add: split_def | wpc
| wp (once) hoare_drop_imps)+
(auto simp: ct_in_state_def elim: st_tcb_ex_cap)
lemma handle_recv_valid_cur_vcpu[wp]:
"handle_recv is_blocking \<lbrace>valid_cur_vcpu\<rbrace>"
unfolding handle_recv_def Let_def ep_ntfn_cap_case_helper delete_caller_cap_def
by (wpsimp wp: hoare_drop_imps)
lemma handle_event_valid_cur_vcpu:
"\<lbrace>valid_cur_vcpu and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
handle_event e
\<lbrace>\<lambda>_. valid_cur_vcpu\<rbrace>"
apply (cases e; clarsimp; (solves wpsimp)?)
unfolding handle_call_def handle_send_def handle_reply_def handle_yield_def
by (wpsimp wp: get_cap_wp)+
lemma call_kernel_valid_cur_vcpu:
"\<lbrace>valid_cur_vcpu and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
(call_kernel e) :: (unit, unit) s_monad
\<lbrace>\<lambda>_ . valid_cur_vcpu\<rbrace>"
unfolding call_kernel_def
apply (simp flip: bind_assoc)
by (wpsimp wp: handle_event_valid_cur_vcpu hoare_vcg_if_lift2 hoare_drop_imps
| strengthen invs_valid_idle)+
lemma call_kernel_valid_cur_vcpu_det_ext:
"\<lbrace>valid_cur_vcpu and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
(call_kernel e) :: (unit, det_ext) s_monad
\<lbrace>\<lambda>_ . valid_cur_vcpu\<rbrace>"
unfolding call_kernel_def
apply (simp flip: bind_assoc)
by (wpsimp wp: handle_event_valid_cur_vcpu hoare_vcg_if_lift2 hoare_drop_imps
| strengthen invs_valid_idle)+
end
end

21
proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy
View File

@ -47,6 +47,17 @@ lemma set_object_valid_vspace_objs'[wp]:
crunch valid_vspace_objs'[wp]: cap_insert, cap_swap_for_delete,empty_slot "valid_vspace_objs'"
(wp: crunch_wps simp: crunch_simps ignore:set_object)
crunches
vcpu_save, vcpu_restore, vcpu_enable, get_vcpu, set_vcpu, vcpu_disable, vcpu_read_reg,
read_vcpu_register,write_vcpu_register
for valid_vspace_objs'[wp]: "valid_vspace_objs'"
(wp: crunch_wps simp: crunch_simps ignore: set_object do_machine_op)
lemma vcpu_switch_valid_vspace_objs'[wp]:
"vcpu_switch v \<lbrace> valid_vspace_objs'\<rbrace>"
unfolding vcpu_switch_def
by wpsimp
lemma valid_pt_entries_invalid[simp]:
"valid_pt_entries (\<lambda>x. InvalidPTE)"
by (simp add:valid_entries_def)
@ -196,6 +207,16 @@ lemma invoke_untyped_valid_vspace_objs'[wp]:
crunches store_asid_pool_entry
for valid_vspace_objs'[wp]: "valid_vspace_objs'"
crunch valid_vspace_objs'[wp]: perform_vcpu_invocation "valid_vspace_objs'"
(ignore: delete_objects wp: hoare_drop_imps)
lemma decode_vcpu_invocation_valid_vspace_objs'[wp]:
"\<lbrace> valid_vspace_objs' \<rbrace>
decode_vcpu_invocation label args vcap excaps
\<lbrace>\<lambda>_. valid_vspace_objs' \<rbrace>, -"
unfolding decode_vcpu_invocation_def
by (wpsimp wp: get_cap_wp)
lemma perform_asid_pool_invocation_valid_vspace_objs'[wp]:
"\<lbrace> valid_vspace_objs' and valid_arch_state and pspace_aligned and
(\<lambda>s. valid_caps (caps_of_state s) s) \<rbrace>

1077
proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy
View File

File diff suppressed because it is too large Load Diff

11
proof/invariant-abstract/AARCH64/Machine_AI.thy
View File

@ -1,4 +1,5 @@
(*
* Copyright 2022, Proofcraft Pty Ltd
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
@ -236,17 +237,23 @@ lemma no_irq_resetTimer: "no_irq resetTimer"
lemma no_irq_debugPrint: "no_irq (debugPrint $ xs)"
by (simp add: no_irq_def)
crunch_ignore (add: dsb_impl)
(* hyp-related machine op no_irq/no_fail/empty_fail rules
FIXME: names are not in legacy no_irq_* form, so relying on adding them to relevant sets *)
crunch_ignore (empty_fail)
(add: writeVCPUHardwareReg_impl set_gic_vcpu_ctrl_vmcr_impl set_gic_vcpu_ctrl_apr_impl
set_gic_vcpu_ctrl_lr_impl get_gic_vcpu_ctrl_lr_impl set_gic_vcpu_ctrl_hcr_impl
setSCTLR_impl addressTranslateS1_impl)
setSCTLR_impl setHCR_impl addressTranslateS1_impl)
crunch_ignore (no_fail)
(add: writeVCPUHardwareReg_impl set_gic_vcpu_ctrl_vmcr_impl set_gic_vcpu_ctrl_apr_impl
set_gic_vcpu_ctrl_lr_impl get_gic_vcpu_ctrl_lr_impl set_gic_vcpu_ctrl_hcr_impl
setSCTLR_impl addressTranslateS1_impl)
setSCTLR_impl setHCR_impl addressTranslateS1_impl)
crunch_ignore
(add: writeVCPUHardwareReg_impl set_gic_vcpu_ctrl_vmcr_impl set_gic_vcpu_ctrl_apr_impl
set_gic_vcpu_ctrl_lr_impl get_gic_vcpu_ctrl_lr_impl set_gic_vcpu_ctrl_hcr_impl
setSCTLR_impl setHCR_impl addressTranslateS1_impl)
crunches getSCTLR, setSCTLR, addressTranslateS1,
readVCPUHardwareReg, writeVCPUHardwareReg,