riscv access: add proofs for CNode_AC
Signed-off-by: Ryan Barry <ryan.barry@unsw.edu.au>
This commit is contained in:
Ryan Barry
Ryan Barry
parent
52abdf42de
commit
9478264f19
|
|
@ -55,14 +55,18 @@ locale CNode_AC_1 =
|
|||
state_asids_to_policy_arch aag caps (as :: arch_state) vrefs \<subseteq> pasPolicy aag \<rbrakk>
|
||||
\<Longrightarrow> state_asids_to_policy_arch aag (caps(ptr \<mapsto> cap, ptr' \<mapsto> cap')) as vrefs \<subseteq> pasPolicy aag"
|
||||
and state_vrefs_tcb_upd:
|
||||
"get_tcb tptr s = Some y \<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(tptr \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"
|
||||
"\<lbrakk> pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tcb_at tptr s \<rbrakk>
|
||||
\<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(tptr \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"
|
||||
and state_vrefs_simple_type_upd:
|
||||
"\<lbrakk> ko_at ko p s; is_simple_type ko; a_type ko = a_type (f (val :: 'b)) \<rbrakk>
|
||||
"\<lbrakk> pspace_aligned s; valid_vspace_objs s; valid_arch_state s;
|
||||
ko_at ko p s; is_simple_type ko; a_type ko = a_type (f (val :: 'b)) \<rbrakk>
|
||||
\<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(p \<mapsto> f val)\<rparr>) = state_vrefs s"
|
||||
and a_type_arch_object_not_tcb[simp]:
|
||||
"a_type (ArchObj arch_kernel_obj) \<noteq> ATCB"
|
||||
and set_cap_state_vrefs[wp]:
|
||||
"\<And>P. set_cap cap slot \<lbrace>\<lambda>s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||
and set_cap_state_vrefs:
|
||||
"\<And>P. \<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
|
||||
set_cap cap slot
|
||||
\<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||
and set_cdt_state_vrefs[wp]:
|
||||
"\<And>P. set_cdt t \<lbrace>\<lambda>s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||
and set_cdt_state_asids_to_policy[wp]:
|
||||
|
|
@ -293,7 +297,7 @@ lemma sita_caps_update2:
|
|||
context CNode_AC_1 begin
|
||||
|
||||
lemma set_cap_pas_refined:
|
||||
"\<lbrace>pas_refined aag and
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and
|
||||
(\<lambda>s. (is_transferable_in ptr s \<and> (\<not> Option.is_none (cdt s ptr)))
|
||||
\<longrightarrow> is_transferable_cap cap \<or>
|
||||
abs_has_auth_to aag Control (fst $ the $ cdt s ptr) (fst ptr)) and
|
||||
|
|
@ -302,7 +306,7 @@ lemma set_cap_pas_refined:
|
|||
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
|
||||
apply (simp add: pas_refined_def state_objs_to_policy_def aag_cap_auth_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp set_cap_caps_of_state | wps)+
|
||||
apply (wp set_cap_caps_of_state set_cap_state_vrefs | wps)+
|
||||
apply clarsimp
|
||||
apply (intro conjI) \<comment> \<open>auth_graph_map\<close>
|
||||
apply (clarsimp dest!: auth_graph_map_memD)
|
||||
|
|
@ -315,7 +319,8 @@ lemma set_cap_pas_refined:
|
|||
done
|
||||
|
||||
lemma set_cap_pas_refined_not_transferable:
|
||||
"\<lbrace>pas_refined aag and cte_wp_at (\<lambda>c. \<not>is_transferable (Some c)) ptr
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
|
||||
and cte_wp_at (\<lambda>c. \<not>is_transferable (Some c)) ptr
|
||||
and K (aag_cap_auth aag (pasObjectAbs aag (fst ptr)) cap)\<rbrace>
|
||||
set_cap cap ptr
|
||||
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
|
||||
|
|
@ -1017,10 +1022,12 @@ locale CNode_AC_3 = CNode_AC_2 +
|
|||
"arch_post_cap_deletion irqopt \<lbrace>pas_refined aag\<rbrace>"
|
||||
and aobj_ref'_same_aobject:
|
||||
"same_aobject_as ao' ao \<Longrightarrow> aobj_ref' ao = aobj_ref' ao'"
|
||||
and set_untyped_cap_as_full_valid_arch_state[wp]:
|
||||
"set_untyped_cap_as_full src_cap new_cap src_slot \<lbrace>\<lambda>s :: det_ext state. valid_arch_state s\<rbrace>"
|
||||
begin
|
||||
|
||||
lemma cap_insert_pas_refined:
|
||||
"\<lbrace>pas_refined aag and valid_mdb and
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and
|
||||
(\<lambda>s. (is_transferable_in src_slot s \<and> (\<not> Option.is_none (cdt s src_slot)))
|
||||
\<longrightarrow> is_transferable_cap new_cap) and
|
||||
K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot)
|
||||
|
|
@ -1044,7 +1051,7 @@ lemma cap_insert_pas_refined:
|
|||
dest: aag_cdt_link_Control aag_cdt_link_DeleteDerived cap_auth_caps_of_state)
|
||||
|
||||
lemma cap_insert_pas_refined':
|
||||
"\<lbrace>pas_refined aag and valid_mdb and
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and
|
||||
(\<lambda>s. cte_wp_at is_transferable_cap src_slot s \<longrightarrow> is_transferable_cap new_cap) and
|
||||
K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot)
|
||||
\<and> pas_cap_cur_auth aag new_cap) \<rbrace>
|
||||
|
|
@ -1055,7 +1062,8 @@ lemma cap_insert_pas_refined':
|
|||
simp: cte_wp_at_caps_of_state Option.is_none_def)
|
||||
|
||||
lemma cap_insert_pas_refined_not_transferable:
|
||||
"\<lbrace>pas_refined aag and valid_mdb and not cte_wp_at is_transferable_cap src_slot
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb
|
||||
and not cte_wp_at is_transferable_cap src_slot
|
||||
and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot)
|
||||
\<and> pas_cap_cur_auth aag new_cap) \<rbrace>
|
||||
cap_insert new_cap src_slot dest_slot
|
||||
|
|
@ -1063,9 +1071,10 @@ lemma cap_insert_pas_refined_not_transferable:
|
|||
by (wpsimp wp: cap_insert_pas_refined')
|
||||
|
||||
lemma cap_insert_pas_refined_same_object_as:
|
||||
"\<lbrace>pas_refined aag and valid_mdb and cte_wp_at (same_object_as new_cap) src_slot
|
||||
and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and>
|
||||
(\<not> is_master_reply_cap new_cap) \<and> pas_cap_cur_auth aag new_cap)\<rbrace>
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb
|
||||
and cte_wp_at (same_object_as new_cap) src_slot
|
||||
and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and>
|
||||
(\<not> is_master_reply_cap new_cap) \<and> pas_cap_cur_auth aag new_cap)\<rbrace>
|
||||
cap_insert new_cap src_slot dest_slot
|
||||
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
|
||||
apply (wp cap_insert_pas_refined)
|
||||
|
|
@ -1074,7 +1083,8 @@ lemma cap_insert_pas_refined_same_object_as:
|
|||
elim: is_transferable_capE split: cap.splits)
|
||||
|
||||
lemma cap_move_pas_refined[wp]:
|
||||
"\<lbrace>pas_refined aag and valid_mdb and cte_wp_at (weak_derived new_cap) src_slot
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
|
||||
and valid_mdb and cte_wp_at (weak_derived new_cap) src_slot
|
||||
and cte_wp_at ((=) NullCap) dest_slot
|
||||
and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot)
|
||||
\<and> pas_cap_cur_auth aag new_cap)\<rbrace>
|
||||
|
|
@ -1091,8 +1101,14 @@ lemma cap_move_pas_refined[wp]:
|
|||
dest: invs_mdb pas_refined_mem[OF sta_cdt]
|
||||
pas_refined_mem[OF sta_cdt_transferable])
|
||||
|
||||
crunches set_original, set_cdt
|
||||
for pspace_aligned[wp]: pspace_aligned
|
||||
and valid_vspace_objs[wp]: valid_vspace_objs
|
||||
and valid_arch_state[wp]: valid_arch_state
|
||||
|
||||
lemma empty_slot_pas_refined[wp, wp_not_transferable]:
|
||||
"\<lbrace>pas_refined aag and valid_mdb and K (is_subject aag (fst slot))\<rbrace>
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
|
||||
and valid_mdb and K (is_subject aag (fst slot))\<rbrace>
|
||||
empty_slot slot irqopt
|
||||
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
|
||||
apply (simp add: empty_slot_def post_cap_deletion_def)
|
||||
|
|
@ -1103,8 +1119,10 @@ lemma empty_slot_pas_refined[wp, wp_not_transferable]:
|
|||
pas_refined_mem[OF sta_cdt] pas_refined_mem[OF sta_cdt_transferable]
|
||||
pas_refined_Control)
|
||||
|
||||
|
||||
lemma empty_slot_pas_refined_transferable[wp_transferable]:
|
||||
"\<lbrace>pas_refined aag and valid_mdb and (\<lambda>s. is_transferable (caps_of_state s slot))\<rbrace>
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
|
||||
and valid_mdb and (\<lambda>s. is_transferable (caps_of_state s slot))\<rbrace>
|
||||
empty_slot slot irqopt
|
||||
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
|
||||
apply (simp add: empty_slot_def post_cap_deletion_def)
|
||||
|
|
@ -1131,7 +1149,7 @@ lemma cap_swap_pas_refined[wp]:
|
|||
apply (rule hoare_pre)
|
||||
apply (wp add: tcb_domain_map_wellformed_lift | simp split del: if_split)+
|
||||
apply (simp only:pas_refined_def state_objs_to_policy_def)
|
||||
apply (wps | wp set_cdt_cdt_ct_ms_rvk set_cap_caps_of_state)+
|
||||
apply (wps | wp set_cap_state_vrefs set_cdt_cdt_ct_ms_rvk set_cap_caps_of_state)+
|
||||
apply (clarsimp simp: pas_refined_def aag_cap_auth_def state_objs_to_policy_def
|
||||
cte_wp_at_caps_of_state
|
||||
split: if_split_asm split del: if_split)
|
||||
|
|
@ -1161,7 +1179,8 @@ lemma cap_swap_pas_refined[wp]:
|
|||
apply (simp split: if_splits add: aag_wellformed_refl)
|
||||
by (erule subsetD;
|
||||
force simp: is_transferable_weak_derived intro!: sbta_cdt_transferable auth_graph_map_memI)+
|
||||
by (blast intro: state_bits_to_policy.intros auth_graph_map_memI)
|
||||
apply (blast intro: state_bits_to_policy.intros auth_graph_map_memI)
|
||||
by fastforce+
|
||||
|
||||
lemma cap_swap_for_delete_pas_refined[wp]:
|
||||
"\<lbrace>pas_refined aag and invs and K (is_subject aag (fst slot) \<and> is_subject aag (fst slot'))\<rbrace>
|
||||
|
|
@ -1288,16 +1307,18 @@ lemma set_simple_ko_ekheap[wp]:
|
|||
context CNode_AC_3 begin
|
||||
|
||||
lemma sts_st_vrefs[wp]:
|
||||
"set_thread_state t st \<lbrace>\<lambda>s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
|
||||
set_thread_state t st
|
||||
\<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||
apply (simp add: set_thread_state_def del: set_thread_state_ext_extended.dxo_eq)
|
||||
apply (wpsimp wp: set_object_wp dxo_wp_weak)
|
||||
apply (clarsimp simp: state_vrefs_tcb_upd
|
||||
apply (clarsimp simp: state_vrefs_tcb_upd obj_at_def is_obj_defs
|
||||
elim!: rsubst[where P=P, OF _ ext]
|
||||
dest!: get_tcb_SomeD)
|
||||
done
|
||||
|
||||
lemma set_thread_state_pas_refined:
|
||||
"\<lbrace>pas_refined aag and
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and
|
||||
K (\<forall>r \<in> tcb_st_to_auth st. abs_has_auth_to aag (snd r) t (fst r))\<rbrace>
|
||||
set_thread_state t st
|
||||
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
|
||||
|
|
@ -1311,26 +1332,31 @@ lemma set_thread_state_pas_refined:
|
|||
done
|
||||
|
||||
lemma set_simple_ko_vrefs[wp]:
|
||||
"set_simple_ko f ptr (val :: 'b) \<lbrace>\<lambda>s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
|
||||
set_simple_ko f ptr (val :: 'b)
|
||||
\<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||
apply (simp add: set_simple_ko_def set_object_def)
|
||||
apply (wp get_object_wp)
|
||||
apply (fastforce simp: state_vrefs_simple_type_upd obj_at_def elim!: rsubst[where P=P, OF _ ext])
|
||||
done
|
||||
|
||||
lemma set_simple_ko_pas_refined[wp]:
|
||||
"set_simple_ko f ptr (ep :: 'b) \<lbrace>pas_refined aag\<rbrace>"
|
||||
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
|
||||
set_simple_ko f ptr (ep :: 'b) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
|
||||
apply (simp add: pas_refined_def state_objs_to_policy_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp tcb_domain_map_wellformed_lift | wps)+
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma thread_set_st_vrefs[wp]:
|
||||
"thread_set f t \<lbrace>\<lambda>s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||
lemma thread_set_state_vrefs:
|
||||
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
|
||||
thread_set f t
|
||||
\<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||
apply (simp add: thread_set_def)
|
||||
apply (wpsimp wp: set_object_wp)
|
||||
apply (clarsimp simp: state_vrefs_tcb_upd
|
||||
elim!: rsubst[where P=P, OF _ ext] dest!: get_tcb_SomeD)
|
||||
apply (clarsimp simp: state_vrefs_tcb_upd obj_at_def is_obj_defs
|
||||
dest!: get_tcb_SomeD)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
@ -1363,8 +1389,10 @@ lemma thread_set_pas_refined_triv:
|
|||
assumes cps: "\<And>tcb. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f tcb) = getF tcb"
|
||||
and st: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
|
||||
and ntfn: "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
|
||||
shows "thread_set f t \<lbrace>pas_refined aag\<rbrace>"
|
||||
by (wpsimp wp: tcb_domain_map_wellformed_lift simp: pas_refined_def state_objs_to_policy_def
|
||||
shows "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
|
||||
thread_set f t \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
|
||||
by (wpsimp wp: tcb_domain_map_wellformed_lift thread_set_state_vrefs
|
||||
simp: pas_refined_def state_objs_to_policy_def
|
||||
| wps thread_set_caps_of_state_trivial[OF cps]
|
||||
thread_set_thread_states_trivT[OF st]
|
||||
thread_set_thread_bound_ntfns_trivT[OF ntfn])+
|
||||
|
|
|
|||
|
|
@ -0,0 +1,334 @@
|
|||
(*
|
||||
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
||||
*
|
||||
* SPDX-License-Identifier: GPL-2.0-only
|
||||
*)
|
||||
|
||||
theory ArchCNode_AC
|
||||
imports CNode_AC
|
||||
begin
|
||||
|
||||
section\<open>Arch-specific CNode AC.\<close>
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
declare arch_post_modify_registers_def[simp]
|
||||
declare arch_post_cap_deletion_def[simp]
|
||||
declare arch_cap_cleanup_opt_def[simp]
|
||||
declare arch_mask_irq_signal_def[simp]
|
||||
|
||||
named_theorems CNode_AC_assms
|
||||
|
||||
lemma sata_cdt_update[CNode_AC_assms, simp]:
|
||||
"state_asids_to_policy aag (cdt_update f s) = state_asids_to_policy aag s"
|
||||
by simp
|
||||
|
||||
lemma sata_is_original_cap_update[CNode_AC_assms, simp]:
|
||||
"state_asids_to_policy aag (is_original_cap_update f s) = state_asids_to_policy aag s"
|
||||
by simp
|
||||
|
||||
lemma sata_interrupt_states_update[CNode_AC_assms, simp]:
|
||||
"state_asids_to_policy aag (interrupt_states_update f s) = state_asids_to_policy aag s"
|
||||
by simp
|
||||
|
||||
lemma sata_machine_state_update[CNode_AC_assms, simp]:
|
||||
"state_asids_to_policy aag (machine_state_update f s) = state_asids_to_policy aag s"
|
||||
by simp
|
||||
|
||||
lemma sata_update[CNode_AC_assms]:
|
||||
"\<lbrakk> pas_wellformed aag;
|
||||
cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap;
|
||||
state_asids_to_policy_arch aag caps as vrefs \<subseteq> pasPolicy aag \<rbrakk>
|
||||
\<Longrightarrow> state_asids_to_policy_arch aag (caps(ptr \<mapsto> cap)) as vrefs \<subseteq> pasPolicy aag"
|
||||
by (fastforce intro: state_asids_to_policy_aux.intros
|
||||
elim!: state_asids_to_policy_aux.cases
|
||||
simp: cap_links_asid_slot_def label_owns_asid_slot_def
|
||||
split: if_split_asm)
|
||||
|
||||
lemma sata_update2[CNode_AC_assms]:
|
||||
"\<lbrakk> pas_wellformed aag;
|
||||
cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap;
|
||||
cap_links_asid_slot aag (pasObjectAbs aag (fst ptr')) cap';
|
||||
state_asids_to_policy_arch aag caps as vrefs \<subseteq> pasPolicy aag \<rbrakk>
|
||||
\<Longrightarrow> state_asids_to_policy_arch aag (caps(ptr \<mapsto> cap, ptr' \<mapsto> cap')) as vrefs \<subseteq> pasPolicy aag"
|
||||
by (fastforce intro: state_asids_to_policy_aux.intros
|
||||
elim!: state_asids_to_policy_aux.cases
|
||||
simp: cap_links_asid_slot_def label_owns_asid_slot_def
|
||||
split: if_split_asm)
|
||||
|
||||
lemma state_vrefs_eqI:
|
||||
"\<lbrakk> \<forall>bot_level asid vref level p.
|
||||
bot_level < level \<and> vs_lookup_table level asid vref s = Some (level, p)
|
||||
\<longrightarrow> (if level \<le> max_pt_level
|
||||
then pts_of s' p = pts_of s p
|
||||
else asid_pools_of s' p = asid_pools_of s p);
|
||||
aobjs_of s' = aobjs_of s; asid_table s' = asid_table s;
|
||||
pspace_aligned s; valid_vspace_objs s; valid_asid_table s \<rbrakk>
|
||||
\<Longrightarrow> state_vrefs (s' :: 'a :: state_ext state) = state_vrefs (s :: 'a :: state_ext state)"
|
||||
apply (rule ext)
|
||||
apply safe
|
||||
apply (subst (asm) state_vrefs_def, clarsimp)
|
||||
apply (fastforce intro: state_vrefsD elim: subst[OF vs_lookup_table_eqI,rotated -1])
|
||||
apply (subst (asm) state_vrefs_def, clarsimp)
|
||||
apply (rule state_vrefsD)
|
||||
apply (subst vs_lookup_table_eqI; fastforce)
|
||||
apply fastforce+
|
||||
done
|
||||
|
||||
lemma set_cap_state_vrefs[CNode_AC_assms, wp]:
|
||||
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. P (state_vrefs s))\<rbrace>
|
||||
set_cap cap slot
|
||||
\<lbrace>\<lambda>_ s :: det_ext state. P (state_vrefs s)\<rbrace>"
|
||||
apply (simp add: set_cap_def set_object_def)
|
||||
apply (wpsimp wp: get_object_wp)
|
||||
apply safe
|
||||
apply (all \<open>subst state_vrefs_eqI\<close>)
|
||||
by (fastforce simp: valid_arch_state_def obj_at_def opt_map_def
|
||||
split: option.splits kernel_object.splits)+
|
||||
|
||||
crunches maskInterrupt
|
||||
for underlying_memory[CNode_AC_assms, wp]: "\<lambda>s. P (underlying_memory s)"
|
||||
and device_state[CNode_AC_assms, wp]: "\<lambda>s. P (device_state s)"
|
||||
(simp: maskInterrupt_def)
|
||||
|
||||
crunches set_cdt
|
||||
for state_vrefs[CNode_AC_assms, wp]: "\<lambda>s. P (state_vrefs s)"
|
||||
and state_asids_to_policy[CNode_AC_assms, wp]: "\<lambda>s. P (state_asids_to_policy aag s)"
|
||||
|
||||
crunches prepare_thread_delete, arch_finalise_cap
|
||||
for cur_domain[CNode_AC_assms, wp]:"\<lambda>s. P (cur_domain s)"
|
||||
(wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def)
|
||||
|
||||
lemma state_vrefs_tcb_upd[CNode_AC_assms]:
|
||||
"\<lbrakk> pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tcb_at t s \<rbrakk>
|
||||
\<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(t \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"
|
||||
apply (rule state_vrefs_eqI)
|
||||
by (fastforce simp: opt_map_def obj_at_def is_obj_defs valid_arch_state_def)+
|
||||
|
||||
lemma state_vrefs_simple_type_upd[CNode_AC_assms]:
|
||||
"\<lbrakk> pspace_aligned s; valid_vspace_objs s; valid_arch_state s;
|
||||
ko_at ko ptr s; is_simple_type ko; a_type ko = a_type (f val) \<rbrakk>
|
||||
\<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(ptr \<mapsto> f val)\<rparr>) = state_vrefs s"
|
||||
apply (case_tac ko; case_tac "f val"; clarsimp)
|
||||
by (fastforce intro!: state_vrefs_eqI simp: opt_map_def obj_at_def is_obj_defs valid_arch_state_def)+
|
||||
|
||||
lemma a_type_arch_object_not_tcb[CNode_AC_assms, simp]:
|
||||
"a_type (ArchObj arch_kernel_obj) \<noteq> ATCB"
|
||||
by auto
|
||||
|
||||
lemma arch_post_cap_deletion_cur_domain[CNode_AC_assms, wp]:
|
||||
"arch_post_cap_deletion acap \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace>"
|
||||
by wpsimp
|
||||
|
||||
lemma arch_post_cap_deletion_integrity[CNode_AC_assms]:
|
||||
"arch_post_cap_deletion acap \<lbrace>integrity aag X st\<rbrace>"
|
||||
by wpsimp
|
||||
|
||||
end
|
||||
|
||||
|
||||
context is_extended begin interpretation Arch .
|
||||
|
||||
lemma list_integ_lift[CNode_AC_assms]:
|
||||
assumes li:
|
||||
"\<lbrace>list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\<rbrace>
|
||||
f
|
||||
\<lbrace>\<lambda>_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\<rbrace>"
|
||||
assumes ekh: "\<And>P. f \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>"
|
||||
assumes rq: "\<And>P. f \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace>"
|
||||
shows "\<lbrace>integrity aag X st and Q\<rbrace> f \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
apply (unfold integrity_def[abs_def] integrity_asids_def)
|
||||
apply (simp only: integrity_cdt_list_as_list_integ)
|
||||
apply (rule hoare_lift_Pf2[where f="ekheap"])
|
||||
apply (simp add: tcb_states_of_state_def get_tcb_def)
|
||||
apply (wp li[simplified tcb_states_of_state_def get_tcb_def] ekh rq)+
|
||||
apply (simp only: integrity_cdt_list_as_list_integ)
|
||||
apply (simp add: tcb_states_of_state_def get_tcb_def)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
|
||||
global_interpretation CNode_AC_1?: CNode_AC_1
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case
|
||||
by (unfold_locales; fact CNode_AC_assms)
|
||||
qed
|
||||
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
lemma integrity_asids_set_cap_Nullcap[CNode_AC_assms]:
|
||||
"\<lbrace>(=) s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_. integrity_asids aag subjects x s\<rbrace>"
|
||||
unfolding integrity_asids_def by wpsimp
|
||||
|
||||
crunches set_original
|
||||
for state_asids_to_policy[CNode_AC_assms, wp]: "\<lambda>s. P (state_asids_to_policy aag s)"
|
||||
and state_objs_to_policy[CNode_AC_assms, wp]: "\<lambda>s. P (state_objs_to_policy s)"
|
||||
(simp: state_objs_to_policy_def)
|
||||
|
||||
crunches set_cdt_list, update_cdt_list
|
||||
for state_vrefs[CNode_AC_assms, wp]: "\<lambda>s. P (state_vrefs s)"
|
||||
and state_asids_to_policy[CNode_AC_assms, wp]: "\<lambda>s. P (state_asids_to_policy aag s)"
|
||||
(simp: set_cdt_list_def)
|
||||
|
||||
end
|
||||
|
||||
|
||||
global_interpretation CNode_AC_2?: CNode_AC_2
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case
|
||||
by (unfold_locales; fact CNode_AC_assms)
|
||||
qed
|
||||
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
lemma arch_post_cap_deletion_pas_refined[CNode_AC_assms, wp]:
|
||||
"arch_post_cap_deletion irqopt \<lbrace>pas_refined aag\<rbrace>"
|
||||
by (wpsimp simp: post_cap_deletion_def)
|
||||
|
||||
lemma aobj_ref'_same_aobject[CNode_AC_assms]:
|
||||
"same_aobject_as ao' ao \<Longrightarrow> aobj_ref' ao = aobj_ref' ao'"
|
||||
by (cases ao; clarsimp split: arch_cap.splits)
|
||||
|
||||
crunches set_untyped_cap_as_full
|
||||
for valid_arch_state[CNode_AC_assms, wp]: valid_arch_state
|
||||
|
||||
end
|
||||
|
||||
|
||||
context is_extended begin interpretation Arch .
|
||||
|
||||
lemma pas_refined_tcb_domain_map_wellformed[CNode_AC_assms, wp]:
|
||||
assumes tdmw: "f \<lbrace>tcb_domain_map_wellformed aag\<rbrace>"
|
||||
shows "f \<lbrace>pas_refined aag\<rbrace>"
|
||||
apply (simp add: pas_refined_def)
|
||||
apply (wp tdmw)
|
||||
apply (wp lift_inv)
|
||||
apply simp+
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
|
||||
global_interpretation CNode_AC_3?: CNode_AC_3
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case
|
||||
by (unfold_locales; fact CNode_AC_assms)
|
||||
qed
|
||||
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
lemma arch_derive_cap_auth_derived[CNode_AC_assms]:
|
||||
"\<lbrace>\<lambda>s. cte_wp_at (auth_derived (ArchObjectCap cap)) src_slot s\<rbrace>
|
||||
arch_derive_cap cap
|
||||
\<lbrace>\<lambda>rv s. cte_wp_at (auth_derived rv) src_slot s\<rbrace>, -"
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | wpc | simp add: arch_derive_cap_def)+
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state)
|
||||
apply (safe)
|
||||
apply (clarsimp simp: auth_derived_def arch_cap_auth_conferred_def cap_auth_conferred_def)
|
||||
done
|
||||
|
||||
lemma cap_asid'_cap_rights_update[CNode_AC_assms, simp]:
|
||||
"acap_asid' (acap_rights_update rights ao) = acap_asid' ao"
|
||||
by (cases ao; clarsimp simp: cap_rights_update_def acap_rights_update_def)
|
||||
|
||||
lemma untyped_range_cap_rights_update[CNode_AC_assms, simp]:
|
||||
"untyped_range (cap_rights_update rights (ArchObjectCap ao)) = untyped_range (ArchObjectCap ao)"
|
||||
by (cases ao; clarsimp simp: cap_rights_update_def)
|
||||
|
||||
lemma obj_refs_cap_rights_update[CNode_AC_assms, simp]:
|
||||
"aobj_ref' (acap_rights_update rights ao) = aobj_ref' ao"
|
||||
by (cases ao; clarsimp simp: cap_rights_update_def acap_rights_update_def)
|
||||
|
||||
lemma auth_derived_arch_update_cap_data[CNode_AC_assms]:
|
||||
"auth_derived (ArchObjectCap ao) cap' \<Longrightarrow> auth_derived (arch_update_cap_data pres w ao) cap'"
|
||||
by (simp add: update_cap_data_def is_cap_simps arch_update_cap_data_def
|
||||
split del: if_split cong: if_cong)
|
||||
|
||||
lemma acap_auth_conferred_acap_rights_update[CNode_AC_assms]:
|
||||
"arch_cap_auth_conferred (acap_rights_update (acap_rights acap \<inter> R) acap)
|
||||
\<subseteq> arch_cap_auth_conferred acap"
|
||||
by (auto simp: arch_cap_auth_conferred_def vspace_cap_rights_to_auth_def acap_rights_update_def
|
||||
validate_vm_rights_def vm_kernel_only_def vm_read_only_def
|
||||
split: arch_cap.splits)
|
||||
|
||||
lemma arch_derive_cap_clas[CNode_AC_assms]:
|
||||
"\<lbrace>\<lambda>s. cap_links_asid_slot aag p (ArchObjectCap acap)\<rbrace>
|
||||
arch_derive_cap acap
|
||||
\<lbrace>\<lambda>rv s. cap_links_asid_slot aag p rv\<rbrace>, -"
|
||||
apply (simp add: arch_derive_cap_def cong: cap.case_cong)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | wpc)+
|
||||
apply (auto simp: is_cap_simps cap_links_asid_slot_def)
|
||||
done
|
||||
|
||||
lemma arch_derive_cap_obj_refs_auth[CNode_AC_assms]:
|
||||
"\<lbrace>K (\<forall>r\<in>obj_refs (ArchObjectCap cap).
|
||||
\<forall>auth\<in>cap_auth_conferred (ArchObjectCap cap). aag_has_auth_to aag auth r)\<rbrace>
|
||||
arch_derive_cap cap
|
||||
\<lbrace>(\<lambda>x s. \<forall>r\<in>obj_refs x. \<forall>auth\<in>cap_auth_conferred x. aag_has_auth_to aag auth r)\<rbrace>, -"
|
||||
unfolding arch_derive_cap_def
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | wpc)+
|
||||
apply (clarsimp simp: cap_auth_conferred_def arch_cap_auth_conferred_def)
|
||||
done
|
||||
|
||||
(* FIXME: move *)
|
||||
lemma arch_derive_cap_obj_refs_subset[CNode_AC_assms]:
|
||||
"\<lbrace>\<lambda>s. (\<forall>x \<in> aobj_ref' acap. P x s)\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv s. \<forall>x \<in> obj_refs rv. P x s\<rbrace>, -"
|
||||
by (wpsimp simp: arch_derive_cap_def) fastforce
|
||||
|
||||
lemma arch_derive_cap_clip[CNode_AC_assms]:
|
||||
"\<lbrace>K (cap_links_irq aag l (ArchObjectCap ac))\<rbrace>
|
||||
arch_derive_cap ac
|
||||
\<lbrace>\<lambda>x s. cap_links_irq aag l x\<rbrace>, -"
|
||||
by (wpsimp simp: arch_derive_cap_def comp_def cli_no_irqs)
|
||||
|
||||
(* FIXME: move *)
|
||||
lemma arch_derive_cap_untyped_range_subset[CNode_AC_assms]:
|
||||
"\<lbrace>\<lambda>s. \<forall>x \<in> untyped_range (ArchObjectCap acap). P x s\<rbrace>
|
||||
arch_derive_cap acap
|
||||
\<lbrace>\<lambda>rv s. \<forall>x \<in> untyped_range rv. P x s\<rbrace>, -"
|
||||
by (wpsimp simp: arch_derive_cap_def)
|
||||
|
||||
lemma arch_update_cap_obj_refs_subset[CNode_AC_assms]:
|
||||
"\<lbrakk> x \<in> obj_refs (arch_update_cap_data pres data cap) \<rbrakk> \<Longrightarrow> x \<in> aobj_ref' cap"
|
||||
by (simp add: arch_update_cap_data_def)
|
||||
|
||||
lemma arch_update_cap_untyped_range_empty[CNode_AC_assms, simp]:
|
||||
"untyped_range (arch_update_cap_data pres data cap) = {}"
|
||||
by (simp add: arch_update_cap_data_def)
|
||||
|
||||
lemma arch_update_cap_irqs_controlled_empty[CNode_AC_assms, simp]:
|
||||
"cap_irqs_controlled (arch_update_cap_data pres data cap) = {}"
|
||||
by (simp add: arch_update_cap_data_def)
|
||||
|
||||
lemma arch_update_cap_links_asid_slot[CNode_AC_assms]:
|
||||
"cap_links_asid_slot aag p (arch_update_cap_data pres w acap) =
|
||||
cap_links_asid_slot aag p (ArchObjectCap acap)"
|
||||
by (simp add: arch_update_cap_data_def)
|
||||
|
||||
lemma arch_update_cap_cap_auth_conferred_subset[CNode_AC_assms]:
|
||||
"y \<in> cap_auth_conferred (arch_update_cap_data b w acap) \<Longrightarrow> y \<in> arch_cap_auth_conferred acap"
|
||||
by (simp add: arch_update_cap_data_def cap_auth_conferred_def)
|
||||
|
||||
end
|
||||
|
||||
|
||||
global_interpretation CNode_AC_4?: CNode_AC_4
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case
|
||||
by (unfold_locales; (fact CNode_AC_assms)?)
|
||||
qed
|
||||
|
||||
|
||||
end
|
||||
Loading…
Reference in New Issue