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

riscv ainvs+access: add proofs for Retype_AC 

Signed-off-by: Ryan Barry <ryan.barry@unsw.edu.au>
This commit is contained in:
Ryan Barry 2021-07-09 16:43:41 +10:00 committed by Ryan Barry
parent 9478264f19
commit cc5014240d
3 changed files with 519 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

366
proof/access-control/RISCV64/ArchRetype_AC.thy Normal file
View File

@ -0,0 +1,366 @@
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory ArchRetype_AC
imports Retype_AC
begin
lemma invs_mdb_cte':
"invs s \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)"
by (drule invs_mdb) (simp add: valid_mdb_def2)
context retype_region_proofs begin interpretation Arch .
lemma state_vrefs_eq:
"\<lbrakk> valid_vspace_objs s; valid_arch_state s \<rbrakk>
\<Longrightarrow> state_vrefs s' = state_vrefs s"
apply (insert dev vp)
apply (intro ext subset_antisym subsetI)
apply (clarsimp simp: state_vrefs_def)
apply (frule vs_lookup_level)
apply (simp add: vs_lookup_table')
apply (prop_tac "kheap s x = kheap s' x")
apply (clarsimp simp: s'_def ps_def split: if_splits)
apply (case_tac "lvl > max_pt_level")
apply (fastforce simp: valid_arch_state_def opt_map_def orthr
dest: vs_lookup_asid_pool
split: option.splits)
apply (fastforce simp: valid_arch_state_def valid_pspace_def obj_at_def orthr
dest!: vs_lookup_table_pt_at )
apply (fastforce simp: opt_map_def)
apply (clarsimp simp: state_vrefs_def)
apply (frule vs_lookup_level)
apply (prop_tac "kheap s x = kheap s' x")
apply (clarsimp simp: s'_def ps_def split: if_splits)
apply (case_tac "lvl > max_pt_level")
apply (fastforce simp: valid_arch_state_def opt_map_def orthr
dest: vs_lookup_asid_pool
split: option.splits)
apply (fastforce simp: valid_arch_state_def valid_pspace_def obj_at_def orthr
dest!: vs_lookup_table_pt_at )
apply (fastforce simp: opt_map_def vs_lookup_table'[symmetric])
done
end
context retype_region_proofs' begin interpretation Arch .
lemma pas_refined:
"\<lbrakk> invs s; pas_refined aag s \<rbrakk> \<Longrightarrow> pas_refined aag s'"
apply (erule pas_refined_state_objs_to_policy_subset)
apply (simp add: state_objs_to_policy_def refs_eq mdb_and_revokable)
apply (subst state_vrefs_eq; fastforce?)
apply (rule subsetI, rename_tac x, case_tac x, simp)
apply (erule state_bits_to_policy.cases)
apply (solves \<open>auto intro!: sbta_caps intro: caps_retype split: cap.split\<close>)
apply (solves \<open>auto intro!: sbta_untyped intro: caps_retype split: cap.split\<close>)
apply (blast intro: state_bits_to_policy.intros)
apply (blast intro: state_bits_to_policy.intros)
apply (force intro!: sbta_cdt
dest: caps_of_state_pres invs_mdb_cte'[THEN mdb_cte_atD[rotated]])
apply (force intro!: sbta_cdt_transferable
dest: caps_of_state_pres invs_mdb_cte'[THEN mdb_cte_atD[rotated]])
apply (blast intro: state_bits_to_policy.intros)
apply (subst state_vrefs_eq; fastforce?)
apply (force elim!: state_asids_to_policy_aux.cases
intro: state_asids_to_policy_aux.intros caps_retype
split: cap.split
dest: sata_asid[OF caps_retype, rotated])
apply clarsimp
apply (erule state_irqs_to_policy_aux.cases)
apply (solves\<open>auto intro!: sita_controlled intro: caps_retype split: cap.split\<close>)
apply (rule domains_of_state)
apply simp
done
end
context Arch begin
lemma aobjs_of_detype[simp]:
"(aobjs_of (detype S s) p = Some aobj) = (p \<notin> S \<and> aobjs_of s p = Some aobj)"
by (simp add: in_omonad detype_def)
lemma pts_of_detype[simp]:
"(pts_of (detype S s) p = Some pt) = (p \<notin> S \<and> pts_of s p = Some pt)"
by (simp add: in_omonad detype_def)
lemma ptes_of_detype_Some[simp]:
"(ptes_of (detype S s) p = Some pte) = (table_base p \<notin> S \<and> ptes_of s p = Some pte)"
by (simp add: in_omonad ptes_of_def detype_def)
lemma asid_pools_of_detype:
"asid_pools_of (detype S s) = (\<lambda>p. if p\<in>S then None else asid_pools_of s p)"
by (rule ext) (simp add: detype_def opt_map_def)
lemma asid_pools_of_detype_Some[simp]:
"(asid_pools_of (detype S s) p = Some ap) = (p \<notin> S \<and> asid_pools_of s p = Some ap)"
by (simp add: in_omonad detype_def)
lemma pool_for_asid_detype_Some[simp]:
"(pool_for_asid asid (detype S s) = Some p) = (pool_for_asid asid s = Some p)"
by (simp add: pool_for_asid_def)
lemma vspace_for_pool_detype_Some[simp]:
"(vspace_for_pool ap asid (\<lambda>p. if p \<in> S then None else pools p) = Some p) =
(ap \<notin> S \<and> vspace_for_pool ap asid pools = Some p)"
by (simp add: vspace_for_pool_def obind_def split: option.splits)
lemma vspace_for_asid_detype_Some[simp]:
"(vspace_for_asid asid (detype S s) = Some p) =
((\<exists>ap. pool_for_asid asid s = Some ap \<and> ap \<notin> S) \<and> vspace_for_asid asid s = Some p)"
apply (simp add: vspace_for_asid_def obind_def asid_pools_of_detype split: option.splits)
apply (auto simp: pool_for_asid_def)
done
lemma pt_walk_detype:
"pt_walk level bot_level pt_ptr vref (ptes_of (detype S s)) = Some (bot_level, p) \<Longrightarrow>
pt_walk level bot_level pt_ptr vref (ptes_of s) = Some (bot_level, p)"
apply (induct level arbitrary: pt_ptr)
apply (subst pt_walk.simps, simp)
apply (subst pt_walk.simps)
apply (subst (asm) (3) pt_walk.simps)
apply (clarsimp simp: in_omonad split: if_split_asm)
apply (erule disjE; clarsimp)
apply (drule meta_spec, drule (1) meta_mp)
apply fastforce
done
lemma vs_lookup_table:
"vs_lookup_table level asid vref (detype S s) = Some (level, p) \<Longrightarrow>
vs_lookup_table level asid vref s = Some (level, p)"
apply (clarsimp simp: vs_lookup_table_def in_omonad obind_def asid_pools_of_detype
split: if_split_asm option.split_asm)
apply (rule conjI)
apply clarsimp
apply (subst pt_walk_detype)
apply simp
apply simp
done
end
context Arch begin global_naming RISCV64
named_theorems Retype_AC_assms
declare retype_region_proofs'.pas_refined[Retype_AC_assms]
lemma state_vrefs_detype[Retype_AC_assms, dest]:
"x \<in> state_vrefs (detype R s) p \<Longrightarrow> x \<in> state_vrefs s p"
apply (clarsimp simp: state_vrefs_def)
apply (frule vs_lookup_level)
apply (drule vs_lookup_table)
apply fastforce
done
lemma sata_detype[Retype_AC_assms]:
"state_asids_to_policy aag (detype R s) \<subseteq> state_asids_to_policy aag s"
apply (clarsimp)
apply (erule state_asids_to_policy_aux.induct)
apply (auto intro: state_asids_to_policy_aux.intros split: if_split_asm)
done
lemma word_size_bits_untyped_min_bits[Retype_AC_assms]: "word_size_bits \<le> untyped_min_bits"
by (simp add: word_size_bits_def untyped_min_bits_def)
lemma clas_default_cap[Retype_AC_assms]:
"tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> cap_links_asid_slot aag p (default_cap tp p' sz dev)"
unfolding cap_links_asid_slot_def
apply (cases tp, simp_all)
apply (rename_tac aobject_type)
apply (case_tac aobject_type, simp_all add: arch_default_cap_def)
done
lemma cli_default_cap[Retype_AC_assms]:
"tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> cap_links_irq aag p (default_cap tp p' sz dev)"
unfolding cap_links_irq_def
apply (cases tp, simp_all)
done
lemma aobj_refs'_default'[Retype_AC_assms]:
"is_aligned oref (obj_bits_api (ArchObject tp) sz)
\<Longrightarrow> aobj_ref' (arch_default_cap tp oref sz dev) \<subseteq> ptr_range oref (obj_bits_api (ArchObject tp) sz)"
by (cases tp; simp add: arch_default_cap_def ptr_range_memI obj_bits_api_def default_arch_object_def)
crunches init_arch_objects
for inv[wp]: P
lemma region_in_kernel_window_preserved:
assumes "\<And>P. f \<lbrace>\<lambda>s. P (arch_state s)\<rbrace>"
shows "\<And>S. f \<lbrace>region_in_kernel_window S\<rbrace>"
apply (clarsimp simp: valid_def region_in_kernel_window_def)
apply (erule use_valid)
apply (rule assms)
apply fastforce
done
(* proof clagged from Retype_AI.clearMemory_vms *)
lemma freeMemory_vms:
"valid_machine_state s \<Longrightarrow>
\<forall>x\<in>fst (freeMemory ptr bits (machine_state s)). valid_machine_state (s\<lparr>machine_state := snd x\<rparr>)"
apply (clarsimp simp: valid_machine_state_def disj_commute[of "in_user_frame p s" for p s])
apply (drule_tac x=p in spec, simp)
apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = 0"
in use_valid[where P=P and Q="\<lambda>_. P" for P], simp_all)
apply (simp add: freeMemory_def machine_op_lift_def machine_rest_lift_def split_def)
apply (wp hoare_drop_imps | simp | wp mapM_x_wp_inv)+
apply (simp add: storeWord_def | wp)+
apply (simp add: word_rsplit_0 upto.simps)
apply simp
done
lemma dmo_freeMemory_vms:
"do_machine_op (freeMemory ptr bits) \<lbrace>valid_machine_state\<rbrace>"
apply (unfold do_machine_op_def)
apply (wp modify_wp freeMemory_vms | simp add: split_def)+
done
lemma freeMemory_valid_irq_states:
"freeMemory ptr bits \<lbrace>\<lambda>ms. valid_irq_states (s\<lparr>machine_state := ms\<rparr>)\<rbrace>"
unfolding freeMemory_def
by (wp mapM_x_wp[OF _ subset_refl] storeWord_valid_irq_states)
crunch pspace_respects_device_region[wp]: freeMemory "\<lambda>ms. P (device_state ms)"
(wp: crunch_wps)
lemma dmo_freeMemory_invs[Retype_AC_assms]:
"do_machine_op (freeMemory ptr bits) \<lbrace>invs\<rbrace>"
apply (simp add: do_machine_op_def invs_def valid_state_def cur_tcb_def | wp | wpc)+
apply (clarsimp)
apply (frule_tac P1="(=) (device_state (machine_state s))"
in use_valid[OF _ freeMemory_pspace_respects_device_region])
apply simp
apply simp
apply (rule conjI)
apply (erule use_valid[OF _ freeMemory_valid_irq_states], simp)
apply (drule freeMemory_vms)
apply auto
done
crunch global_refs[wp]: delete_objects "\<lambda>s. P (global_refs s)"
(ignore: do_machine_op freeMemory)
lemma init_arch_objects_pas_cur_domain[Retype_AC_assms, wp]:
"init_arch_objects tp ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>"
by wp
lemma retype_region_pas_cur_domain[Retype_AC_assms, wp]:
"retype_region ptr n us tp dev \<lbrace>pas_cur_domain aag\<rbrace>"
by wp
lemma reset_untyped_cap_pas_cur_domain[Retype_AC_assms, wp]:
"reset_untyped_cap src_slot \<lbrace>pas_cur_domain aag\<rbrace>"
by wp
lemma arch_data_to_obj_type_not_ASIDPoolObj[Retype_AC_assms, simp]:
"arch_data_to_obj_type v \<noteq> Some ASIDPoolObj"
by (clarsimp simp: arch_data_to_obj_type_def)
lemma data_to_nat_of_nat[Retype_AC_assms, simp]:
"of_nat (data_to_nat x) = x"
by simp
lemma nonzero_data_to_nat_simp[Retype_AC_assms]:
"0 < data_to_nat x \<Longrightarrow> 0 < x"
by (auto dest: word_of_nat_less)
lemma storeWord_integrity_autarch:
"\<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and>
(is_aligned p word_size_bits \<longrightarrow> (\<forall>p' \<in> ptr_range p word_size_bits. is_subject aag p'))\<rbrace>
storeWord p v
\<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>"
unfolding storeWord_def
apply wp
apply (auto simp: upto.simps integrity_def is_aligned_mask [symmetric] word_size_bits_def
intro!: trm_lrefl ptr_range_memI ptr_range_add_memI)
done
(* TODO: proof has mainly been copied from dmo_clearMemory_respects *)
lemma dmo_freeMemory_respects[Retype_AC_assms]:
"\<lbrace>integrity aag X st and K (is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and>
(\<forall>p \<in> ptr_range ptr bits. is_subject aag p))\<rbrace>
do_machine_op (freeMemory ptr bits)
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
unfolding do_machine_op_def freeMemory_def
apply (simp add: split_def)
apply wp
apply clarsimp
apply (erule use_valid)
apply (wp mol_respects mapM_x_wp' storeWord_integrity_autarch)
apply simp
apply (clarsimp simp: word_size_def word_size_bits_def word_bits_def
upto_enum_step_shift_red[where us=3, simplified])
apply (erule bspec)
apply (erule set_mp [rotated])
apply (rule ptr_range_subset)
apply simp
apply (simp add: is_aligned_mult_triv2 [where n = 3, simplified])
apply assumption
apply (erule word_less_power_trans_ofnat [where k = 3, simplified])
apply assumption
apply simp
apply simp
done
lemma storeWord_respects:
"\<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and>
(\<forall>p' \<in> ptr_range p word_size_bits. aag_has_auth_to aag Write p')\<rbrace>
storeWord p v
\<lbrace>\<lambda>_ ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace>"
unfolding storeWord_def word_size_bits_def
apply wp
apply (auto simp: upto.simps integrity_def is_aligned_mask [symmetric]
intro!: trm_write ptr_range_memI ptr_range_add_memI)
done
lemma dmo_clearMemory_respects'[Retype_AC_assms]:
"\<lbrace>integrity aag X st and
K (is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and>
(\<forall>p \<in> ptr_range ptr bits. aag_has_auth_to aag Write p))\<rbrace>
do_machine_op (clearMemory ptr (2 ^ bits))
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
unfolding do_machine_op_def clearMemory_def
apply (simp add: split_def )
apply wp
apply clarsimp
apply (erule use_valid)
apply (wp mol_respects mapM_x_wp' storeWord_respects)+
apply (simp add: word_size_bits_def)
apply (clarsimp simp: word_size_def word_bits_def upto_enum_step_shift_red[where us=3, simplified])
apply (erule bspec)
apply (erule set_mp [rotated])
apply (rule ptr_range_subset)
apply simp
apply (simp add: is_aligned_mult_triv2 [where n = 3, simplified])
apply assumption
apply (erule word_less_power_trans_ofnat [where k = 3, simplified])
apply assumption
apply simp
apply simp
done
end
global_interpretation Retype_AC_1?: Retype_AC_1
proof goal_cases
interpret Arch .
case 1 show ?case
by (unfold_locales; (fact Retype_AC_assms | wpsimp wp: init_arch_objects_inv)?)
qed
context begin interpretation Arch .
requalify_facts storeWord_respects
end
end

227
proof/access-control/Retype_AC.thy
View File

@ -169,11 +169,11 @@ locale retype_region_proofs' = retype_region_proofs +
locale Retype_AC_1 =
fixes aag :: "'a PAS"
assumes state_vrefs_detype[simp]:
"state_vrefs (detype R s) = (\<lambda>x. if x \<in> R then {} else state_vrefs s x)"
"x \<in> state_vrefs (detype R s) p \<Longrightarrow> x \<in> state_vrefs s p"
and sata_detype:
"state_asids_to_policy aag (detype R s) \<subseteq> state_asids_to_policy aag s"
and untyped_min_bits_ge_2:
"2 \<le> untyped_min_bits"
and word_size_bits_untyped_min_bits:
"word_size_bits \<le> untyped_min_bits"
and clas_default_cap:
"\<And>tp. tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> cap_links_asid_slot aag l (default_cap tp p sz dev)"
and cli_default_cap:
@ -201,25 +201,19 @@ locale Retype_AC_1 =
"\<And>x. of_nat (data_to_nat x) = x"
and nonzero_data_to_nat_simp:
"\<And>x. 0 < data_to_nat x \<Longrightarrow> 0 < x"
and retype_region_proofs_vrefs_eq:
"retype_region_proofs s ty us ptr sz n dev
\<Longrightarrow> state_vrefs (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us)
then Some (default_object ty dev us)
else kheap s x\<rparr>) =
state_vrefs s"
and retype_region_proofs'_pas_refined:
"\<lbrakk> retype_region_proofs' s ty us ptr sz n dev; invs s; pas_refined aag s \<rbrakk>
\<Longrightarrow> pas_refined aag (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us)
then Some (default_object ty dev us)
else kheap s x\<rparr>)"
and dmo_freeMemory_respects:
"\<lbrace>integrity aag X st and K (is_aligned ptr bits \<and> bits < word_bits \<and> 2 \<le> bits
assumes dmo_freeMemory_respects:
"\<lbrace>integrity aag X st and K (is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits
\<and> (\<forall>p \<in> ptr_range ptr bits. is_subject aag p))\<rbrace>
do_machine_op (freeMemory ptr bits)
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
and dmo_clearMemory_respects':
"\<lbrace>integrity aag X st and
K (is_aligned ptr bits \<and> bits < word_bits \<and> 2 \<le> bits \<and>
K (is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and>
(\<forall>p \<in> ptr_range ptr bits. aag_has_auth_to aag Write p))\<rbrace>
do_machine_op (clearMemory ptr (2 ^ bits))
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
@ -242,7 +236,8 @@ lemma sta_detype:
"state_objs_to_policy (detype R s) \<subseteq> state_objs_to_policy s"
apply (clarsimp simp add: state_objs_to_policy_def state_refs_of_detype)
apply (erule state_bits_to_policy.induct)
apply (auto intro: state_bits_to_policy.intros split: if_split_asm)
apply (auto intro: state_bits_to_policy.intros dest: state_vrefs_detype
simp: state_objs_to_policy_def split: if_splits)
done
lemma pas_refined_detype:
@ -252,15 +247,15 @@ lemma pas_refined_detype:
done
lemma delete_objects_respects[wp]:
"\<lbrace>integrity aag X st and K (is_aligned ptr bits \<and> bits < word_bits \<and> 2 \<le> bits \<and>
(\<forall>p\<in>ptr_range ptr bits. is_subject aag p))\<rbrace>
"\<lbrace>\<lambda>s. integrity aag X st s \<and> is_aligned ptr bits \<and> bits < word_bits \<and>
word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace>
delete_objects ptr bits
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: delete_objects_def)
apply (rule_tac seq_ext)
apply (simp add: delete_objects_def)
apply (rule_tac seq_ext)
apply (rule hoare_triv[of P _ "%_. P" for P])
apply (wp dmo_freeMemory_respects | simp)+
by (fastforce simp: ptr_range_def intro!: detype_integrity)
by (fastforce simp: ptr_range_def intro!: detype_integrity)
lemma integrity_work_units_completed_update[simp]:
"integrity aag X st (work_units_completed_update f s) = integrity aag X st s"
@ -272,6 +267,7 @@ lemma integrity_irq_state_independent[intro!, simp]:
integrity x y z s"
by (simp add: integrity_def)
(* FIXME AC: shouldn't use word-dependent definitions in a generic context *)
lemma reset_untyped_cap_integrity:
"\<lbrace>integrity aag X st and pas_refined aag and valid_objs
and cte_wp_at is_untyped_cap slot
@ -292,6 +288,7 @@ lemma reset_untyped_cap_integrity:
set_cap_integrity_autarch dmo_clearMemory_respects' | simp)+
apply (clarsimp simp: cap_aligned_def is_cap_simps bits_of_def)
apply (subst aligned_add_aligned, assumption, rule is_aligned_shiftl, simp+)
apply (simp add: word_size_bits_def reset_chunk_bits_def)
apply (clarsimp simp: arg_cong2[where f="(\<le>)", OF refl reset_chunk_bits_def])
apply (drule bspec, erule subsetD[rotated])
apply (simp only: ptr_range_def, rule new_range_subset',
@ -308,7 +305,7 @@ lemma reset_untyped_cap_integrity:
apply (clarsimp simp: cap_aligned_def is_cap_simps valid_cap_simps bits_of_def)
apply (frule(2) cap_cur_auth_caps_of_state)
apply (clarsimp simp: aag_cap_auth_def ptr_range_def aag_has_Control_iff_owns
pas_refined_refl le_trans[OF untyped_min_bits_ge_2])
pas_refined_refl le_trans[OF word_size_bits_untyped_min_bits])
done
lemma retype_region_integrity:
@ -364,7 +361,7 @@ lemma obj_refs_default':
by (cases tp; auto simp: ptr_range_memI obj_bits_api_def dest: rev_subsetD[OF _ aobj_refs'_default'])
lemma create_cap_pas_refined:
"\<lbrace>pas_refined aag and
"\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and
K (tp \<noteq> ArchObject ASIDPoolObj \<and> is_subject aag (fst p) \<and> is_subject aag (fst (fst ref)) \<and>
(\<forall>x \<in> ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x) \<and>
is_aligned (snd ref) (obj_bits_api tp sz))\<rbrace>
@ -461,7 +458,7 @@ lemma use_retype_region_proofs_ext':
apply (clarsimp simp: retype_addrs_fold
foldr_upd_app_if fun_upd_def[symmetric])
apply safe
apply (rule x)
apply (rule x)
apply (rule retype_region_proofs.intro, simp_all)[1]
apply (fastforce simp: range_cover_def obj_bits_api_def z slot_bits_def2 word_bits_def)+
done
@ -523,31 +520,6 @@ lemma retype_region_pas_refined:
apply auto
done
(* FIXME MOVE *)
lemma retype_region_aag_bits:
"\<lbrace>\<lambda>s :: det_ext state. P (null_filter (caps_of_state s)) (state_refs_of s) (cdt s) (state_vrefs s)
\<and> valid_pspace s \<and> valid_mdb s
\<and> caps_overlap_reserved {ptr..ptr + of_nat num_objects * 2 ^ obj_bits_api tp us - 1} s
\<and> caps_no_overlap ptr sz s \<and> pspace_no_overlap_range_cover ptr sz s
\<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s)
\<and> ((tp = CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr sz (obj_bits_api tp us) num_objects)\<rbrace>
retype_region ptr num_objects us tp dev
\<lbrace>\<lambda>_ s. P (null_filter (caps_of_state s)) (state_refs_of s) (cdt s) (state_vrefs s)\<rbrace>"
apply (subst conj_assoc [symmetric])+
apply (rule hoare_gen_asm [unfolded pred_conj_def K_def])+
apply (rule hoare_pre)
apply (rule use_retype_region_proofs)
apply (frule retype_region_proofs.null_filter, erule ssubst)
apply (frule retype_region_proofs.refs_eq, erule ssubst)
apply (frule retype_region_proofs_vrefs_eq, erule ssubst)
apply (frule retype_region_proofs.mdb_and_revokable, erule ssubst)
apply assumption
apply simp
apply simp
apply simp
apply blast
done
end
@ -939,9 +911,101 @@ lemma delete_objects_pas_refined:
apply simp
done
lemma delete_objects_pspace_aligned[wp]:
"delete_objects ptr sz \<lbrace>pspace_aligned\<rbrace>"
unfolding delete_objects_def do_machine_op_def
apply (wp | simp add: split_def detype_machine_state_update_comm)+
apply clarsimp
apply (auto simp add: detype_def pspace_aligned_def)
done
lemma reset_untyped_cap_pspace_aligned[wp]:
"reset_untyped_cap slot \<lbrace>pspace_aligned\<rbrace>"
apply (clarsimp simp: reset_untyped_cap_def)
apply (wpsimp wp: mapME_x_inv_wp )
apply (rule valid_validE)
apply (wpsimp wp: preemption_point_inv dxo_wp_weak hoare_drop_imps)+
done
lemma valid_vspace_objs_detype:
assumes "invs s"
assumes "cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s
\<and> untyped_range c = {p..p + 2 ^ sz - 1}) ptr s"
shows "valid_vspace_objs (detype {p..p + 2 ^ sz - 1} s)"
proof -
obtain c where c_def: "cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s
\<and> untyped_range c = {p..p + 2 ^ sz - 1}"
using assms by (fastforce dest: cte_wp_at_norm)
have detype: "detype_locale_arch c ptr s"
by unfold_locales (auto simp: assms c_def invs_untyped_children)
thus ?thesis
using detype_locale_arch.valid_vspace_obj_detype by (fastforce simp: c_def)
qed
lemma delete_objects_valid_vspace_objs:
"\<lbrace>\<lambda>s. invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and>
untyped_range c = {p..p + 2 ^ sz - 1}) ptr s)\<rbrace>
delete_objects p sz
\<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
unfolding delete_objects_def do_machine_op_def
apply (wp | simp add: split_def detype_machine_state_update_comm)+
apply (auto simp: valid_vspace_objs_detype)
done
lemma reset_untyped_cap_valid_vspace_objs:
"\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c src_slot s) src_slot s\<rbrace>
reset_untyped_cap src_slot
\<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
unfolding reset_untyped_cap_def
apply (wpsimp wp: mapME_x_inv_wp preemption_point_inv)
apply (wp static_imp_wp delete_objects_valid_vspace_objs)
apply (wpsimp wp: get_cap_wp)+
apply (cases src_slot)
apply (auto simp: cte_wp_at_caps_of_state)
apply (fastforce simp: bits_of_def is_cap_simps)+
done
lemma valid_arch_state_detype:
assumes "invs s"
assumes "cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s
\<and> untyped_range c = {p..p + 2 ^ sz - 1}) ptr s"
shows "valid_arch_state (detype {p..p + 2 ^ sz - 1} s)"
proof -
obtain c where c_def: "cte_wp_at ((=) c) ptr s \<and> is_untyped_cap c \<and> descendants_range c ptr s
\<and> untyped_range c = {p..p + 2 ^ sz - 1}"
using assms by (fastforce dest: cte_wp_at_norm)
have detype: "detype_locale_arch c ptr s"
by unfold_locales (auto simp: assms c_def invs_untyped_children)
thus ?thesis
using detype_locale_arch.valid_arch_state_detype by (fastforce simp: c_def)
qed
lemma delete_objects_valid_arch_state:
"\<lbrace>\<lambda>s. invs s \<and> (\<exists>ptr. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c ptr s \<and>
untyped_range c = {p..p + 2 ^ sz - 1}) ptr s)\<rbrace>
delete_objects p sz
\<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
unfolding delete_objects_def do_machine_op_def
apply (wp | simp add: split_def detype_machine_state_update_comm)+
apply (auto simp: valid_arch_state_detype)
done
lemma reset_untyped_cap_valid_arch_state:
"\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c src_slot s) src_slot s\<rbrace>
reset_untyped_cap src_slot
\<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
unfolding reset_untyped_cap_def
apply (wpsimp wp: mapME_x_inv_wp preemption_point_inv)
apply (wp static_imp_wp delete_objects_valid_arch_state)
apply (wpsimp wp: get_cap_wp)+
apply (cases src_slot)
apply (auto simp: cte_wp_at_caps_of_state)
apply (fastforce simp: bits_of_def is_cap_simps)+
done
lemma reset_untyped_cap_pas_refined[wp]:
"\<lbrace>pas_refined aag and cte_wp_at is_untyped_cap slot
and cte_wp_at (\<lambda>c. fst slot \<notin> untyped_range c) slot
"\<lbrace>pas_refined aag and invs and
(\<lambda>s. cte_wp_at (\<lambda>c. is_untyped_cap c \<and> descendants_range c slot s) slot s)
and K (is_subject aag (fst slot))\<rbrace>
reset_untyped_cap slot
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
@ -951,7 +1015,8 @@ lemma reset_untyped_cap_pas_refined[wp]:
apply (wps | wp set_cap_pas_refined_not_transferable | simp add: unless_def)+
apply (rule valid_validE)
apply (rule_tac P="is_untyped_cap cap \<and> pas_cap_cur_auth aag cap" in hoare_gen_asm)
apply (rule_tac Q="\<lambda>_.cte_wp_at (\<lambda> c. \<not> is_transferable (Some c)) slot and pas_refined aag"
apply (rule_tac Q="\<lambda>_. cte_wp_at (\<lambda> c. \<not> is_transferable (Some c)) slot and pas_refined aag and
pspace_aligned and valid_vspace_objs and valid_arch_state"
in hoare_strengthen_post)
apply (rule validE_valid, rule mapME_x_inv_wp)
apply (rule hoare_pre)
@ -960,11 +1025,15 @@ lemma reset_untyped_cap_pas_refined[wp]:
| simp)+
apply (fastforce simp: is_cap_simps aag_cap_auth_UntypedCap_idx_dev bits_of_def)
apply blast
apply (wps
| wp hoare_vcg_const_imp_lift get_cap_wp delete_objects_pas_refined hoare_drop_imp
| simp)+
apply (wps | wp hoare_vcg_const_imp_lift get_cap_wp delete_objects_pas_refined hoare_drop_imp
delete_objects_valid_vspace_objs delete_objects_valid_arch_state
| simp)+
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
apply (frule cte_map_not_null_outside'[rotated])
apply (fastforce simp: cte_wp_at_caps_of_state)+
apply (cases slot)
apply (auto elim: caps_pas_cap_cur_auth_UntypedCap_idx_dev)
apply (fastforce simp: bits_of_def is_cap_simps)+
done
lemma invoke_untyped_pas_refined:
@ -974,7 +1043,8 @@ lemma invoke_untyped_pas_refined:
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
apply (rule hoare_pre)
apply (rule_tac Q="\<lambda>_. pas_refined aag and pas_cur_domain aag" in hoare_strengthen_post)
apply (rule_tac Q="\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs
and valid_arch_state and pas_cur_domain aag" in hoare_strengthen_post)
apply (rule invoke_untyped_Q)
apply (rule hoare_pre, wp create_cap_pas_refined)
apply (clarsimp simp: authorised_untyped_inv_def
@ -987,40 +1057,43 @@ lemma invoke_untyped_pas_refined:
apply (clarsimp simp add: aag_cap_auth_def ptr_range_def[symmetric]
pas_refined_all_auth_is_owns)
apply blast
apply (wp init_arch_objects_pas_refined)
apply (wpsimp wp: init_arch_objects_pas_refined init_arch_objects_invs_from_restricted
| strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+
apply (clarsimp simp: retype_addrs_aligned_range_cover
cte_wp_at_caps_of_state)
apply (drule valid_global_refsD[rotated 2])
apply (clarsimp simp: post_retype_invs_def split: if_split_asm)
apply (erule caps_of_state_cteD)
apply (erule notE, erule subsetD[rotated])
apply (rule order_trans, erule retype_addrs_subset_ptr_bits)
apply (simp add: field_simps word_and_le2)
apply (rule context_conjI, clarsimp)
apply (drule valid_global_refsD[rotated 2])
apply (clarsimp simp: post_retype_invs_def split: if_split_asm)
apply (erule caps_of_state_cteD)
apply (erule notE, erule subsetD[rotated])
apply (rule order_trans, erule retype_addrs_subset_ptr_bits)
apply (simp add: field_simps word_and_le2)
apply blast
apply (rule hoare_name_pre_state, clarsimp)
apply (rule hoare_pre, wp retype_region_pas_refined)
apply (rule_tac Q="\<lambda>rv. post_retype_invs tp rv and pas_cur_domain aag" in hoare_strengthen_post)
apply (wp retype_region_post_retype_invs_spec)
apply (clarsimp simp: post_retype_invs_def invs_def valid_state_def valid_pspace_def split: if_splits)
apply (clarsimp simp: authorised_untyped_inv_def)
apply (strengthen range_cover_le[mk_strg I E], simp)
apply (intro conjI exI;
(erule cte_wp_at_weakenE)?,
clarsimp simp: field_simps word_and_le2)
apply (intro conjI)
apply (intro conjI exI;
(erule cte_wp_at_weakenE)?,
clarsimp simp: field_simps word_and_le2)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (erule caps_region_kernel_window_imp)
apply clarsimp
apply clarsimp
apply (fastforce simp: word_and_le2)
apply (fastforce simp: cte_wp_at_caps_of_state)
apply (rule hoare_pre, wp set_cap_pas_refined)
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps)
apply (cases ui,
clarsimp simp: authorised_untyped_inv_def caps_pas_cap_cur_auth_UntypedCap_idx_dev)
apply wp
apply (wp reset_untyped_cap_valid_vspace_objs reset_untyped_cap_valid_arch_state)
apply clarsimp
apply (cases ui, clarsimp)
(* FIXME CLEAN UP ? *)
apply (intro conjI)
prefer 2
apply (simp add: cte_wp_at_caps_of_state del: untyped_range.simps)
apply (rule cte_map_not_null_outside'
[where p="(a, b)" and p'="(a, b)" for a b,
simplified fst_conv, OF caps_of_state_cteD],
assumption)
apply (force simp: descendants_range_def
cte_wp_at_caps_of_state authorised_untyped_inv_def)+
apply (force simp: descendants_range_def cte_wp_at_caps_of_state authorised_untyped_inv_def)
done
end
@ -1104,7 +1177,7 @@ lemma decode_untyped_invocation_authorised:
"\<lambda>rv s. rv \<noteq> ArchObject ASIDPoolObj \<and>
(\<forall>cap. cte_wp_at ((=) cap) slot s
\<longrightarrow> (\<forall>ref \<in> ptr_range base (bits_of cap). is_subject aag ref)) \<and>
is_subject aag (fst slot) \<and> pas_refined aag s \<and> 2 \<le> sz \<and>
is_subject aag (fst slot) \<and> pas_refined aag s \<and> word_size_bits \<le> sz \<and>
sz < word_bits \<and> is_aligned base sz \<and>
(is_cnode_cap (excaps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs (excaps ! 0). is_subject aag x))"
in hoare_post_imp_R)
@ -1114,7 +1187,7 @@ lemma decode_untyped_invocation_authorised:
apply (auto dest!: bang_0_in_set dest: cte_wp_at_eqD2
simp: valid_cap_def cap_aligned_def obj_ref_of_def is_cap_simps
cap_auth_conferred_def pas_refined_all_auth_is_owns bits_of_UntypedCap
aag_cap_auth_def ptr_range_def le_trans[OF untyped_min_bits_ge_2])
aag_cap_auth_def ptr_range_def le_trans[OF word_size_bits_untyped_min_bits])
done
end

6
proof/invariant-abstract/RISCV64/ArchDetype_AI.thy
View File

@ -233,20 +233,20 @@ lemma pt_walk_detype:
done
lemma vs_lookup_table:
"vs_lookup_table level asid vref (detype (untyped_range cap) s) = Some (level, p) \<Longrightarrow>
"vs_lookup_table level asid vref (detype S s) = Some (level, p) \<Longrightarrow>
vs_lookup_table level asid vref s = Some (level, p)"
by (fastforce simp: vs_lookup_table_def in_omonad asid_pools_of_detype pt_walk_detype
split: if_split_asm)
lemma vs_lookup_slot:
"(vs_lookup_slot level asid vref (detype (untyped_range cap) s) = Some (level, p)) ==>
"(vs_lookup_slot level asid vref (detype S s) = Some (level, p)) \<Longrightarrow>
(vs_lookup_slot level asid vref s = Some (level, p))"
by (fastforce simp: vs_lookup_slot_def in_omonad asid_pools_of_detype
split: if_split_asm
dest!: vs_lookup_table)
lemma vs_lookup_target:
"(vs_lookup_target level asid vref (detype (untyped_range cap) s) = Some (level, p)) ==>
"(vs_lookup_target level asid vref (detype S s) = Some (level, p)) \<Longrightarrow>
(vs_lookup_target level asid vref s = Some (level, p))"
by (fastforce simp: vs_lookup_target_def in_omonad asid_pools_of_detype
split: if_split_asm