secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

arm+arm-hyp: remove duplicated ASpec asid bit definitions 

MiscMachine_A already contains asid_high_bits, asid_low_bits and
asid_bits. Other architectures don't duplicate them in Arch_Structs_A,
so ARM and ARM_HYP shouldn't either.

For ARM, this also means fixing up DRefine+DPolicy+CamkesCdlRefine to
refer to the MiscMachine_A definitions when needed (CapDL duplicates
them again in Types_D, but as they don't import machine theories, those
can't be removed).

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2024-07-25 06:05:10 +10:00 committed by Rafal Kolanski
parent bdbfa7d554
commit fa9797948c
11 changed files with 38 additions and 55 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
camkes/cdl-refine/Eval_CAMKES_CDL.thy
View File

@ -169,7 +169,7 @@ lemma Collect_asid_high__eval_helper:
apply (subst arg_cong[where f="(<) _"])
prefer 2
apply (rule unat_lt2p)
apply (simp add: asid_high_bits_def)
apply (simp add: MiscMachine_A.asid_high_bits_def)
apply (simp add: transform_asid_def asid_high_bits_of_def[abs_def])
apply (rule set_eqI)
apply (rule iffI)
@ -177,34 +177,35 @@ lemma Collect_asid_high__eval_helper:
apply (clarsimp simp: Collect_conj_eq image_iff)
apply (rule_tac x="(of_nat asid_high << asid_low_bits) + 1" in bexI)
apply (subst add.commute, subst shiftr_irrelevant)
apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
apply (clarsimp simp: is_aligned_shift)
apply (subst shiftl_shiftr_id)
apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
apply (clarsimp simp: asid_low_bits_def asid_high_bits_def word_of_nat_less)
apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
apply (clarsimp simp: is_aligned_shift MiscMachine_A.asid_low_bits_def)
apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
apply (subst shiftl_shiftr_id, simp)
apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less)
apply (subst ucast_of_nat_small)
apply (clarsimp simp: asid_high_bits_def)
apply (clarsimp simp: MiscMachine_A.asid_high_bits_def)
apply simp
apply clarsimp
apply (rule conjI)
apply (clarsimp simp: unat_ucast_eq_unat_and_mask)
apply (subst add.commute, subst shiftr_irrelevant)
apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def)
apply (clarsimp simp: is_aligned_shift)
apply (subst shiftl_shiftr_id)
apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
apply (clarsimp simp: asid_low_bits_def asid_high_bits_def word_of_nat_less)
apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def
word_of_nat_less)
apply (fold asid_high_bits_def)
apply (subst less_mask_eq)
apply (clarsimp simp: asid_high_bits_def word_of_nat_less)
apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less)
apply (rule unat_of_nat_eq)
apply (clarsimp simp: asid_high_bits_def)
apply (clarsimp simp: MiscMachine_A.asid_high_bits_def)
apply (rule less_is_non_zero_p1[where k="2^asid_high_bits << asid_low_bits"])
apply (simp only: shiftl_t2n)
apply (simp add: shiftl_t2n)
apply (subst mult.commute, subst mult.commute, rule word_mult_less_mono1)
apply (clarsimp simp: asid_high_bits_def word_of_nat_less)
apply (clarsimp simp: asid_low_bits_def)
apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less)
apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def)
done

16
proof/dpolicy/Dpolicy.thy
View File

@ -217,26 +217,26 @@ lemmas cdl_state_objs_to_policy_cases
= cdl_state_bits_to_policy.cases[OF cdl_state_objs_to_policy_mem[THEN iffD1]]
lemma transform_asid_rev [simp]:
"asid \<le> 2 ^ ARM_A.asid_bits - 1 \<Longrightarrow> transform_asid_rev (transform_asid asid) = asid"
"asid \<le> 2 ^ MiscMachine_A.asid_bits - 1 \<Longrightarrow> transform_asid_rev (transform_asid asid) = asid"
apply (clarsimp simp:transform_asid_def transform_asid_rev_def
asid_high_bits_of_def ARM_A.asid_low_bits_def)
asid_high_bits_of_def asid_low_bits_def)
apply (subgoal_tac "asid >> 10 < 2 ^ asid_high_bits")
apply (simp add:ARM_A.asid_high_bits_def ARM_A.asid_bits_def)
apply (simp add: MiscMachine_A.asid_high_bits_def MiscMachine_A.asid_bits_def MiscMachine_A.asid_low_bits_def)
apply (subst ucast_ucast_len)
apply simp
apply (subst shiftr_shiftl1)
apply simp
apply (subst ucast_ucast_mask)
apply (simp add:mask_out_sub_mask)
apply (simp add:ARM_A.asid_high_bits_def)
apply (rule shiftr_less_t2n[where m=7, simplified])
apply (simp add:ARM_A.asid_bits_def)
apply (simp add: asid_high_bits_def)
apply (rule shiftr_less_t2n[where m=MiscMachine_A.asid_high_bits, simplified])
apply (simp add: MiscMachine_A.asid_bits_def MiscMachine_A.asid_high_bits_def)
done
abbreviation
"valid_asid_mapping mapping \<equiv> (case mapping of
None \<Rightarrow> True
| Some (asid, ref) \<Rightarrow> asid \<le> 2 ^ ARM_A.asid_bits - 1)"
| Some (asid, ref) \<Rightarrow> asid \<le> 2 ^ asid_bits - 1)"
lemma transform_asid_rev_transform_mapping [simp]:
"valid_asid_mapping mapping \<Longrightarrow>
@ -1073,7 +1073,7 @@ lemma state_vrefs_asid_pool_transform_rev:
"\<lbrakk> einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap;
\<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap;
opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap \<rbrakk> \<Longrightarrow>
(pdptr, asid && mask ARM_A.asid_low_bits, AASIDPool, Control)
(pdptr, asid && mask MiscMachine_A.asid_low_bits, AASIDPool, Control)
\<in> state_vrefs s (cap_object poolcap)"
apply (subgoal_tac "cap_object poolcap \<noteq> idle_thread s")
prefer 2

6
proof/drefine/Arch_DR.thy
View File

@ -730,7 +730,7 @@ next
apply (thin_tac "free_asid_select v \<notin> dom v")
apply clarsimp
apply (subgoal_tac "unat ((ucast (free_asid_select v) :: word32) << 10) mod 1024=0")
apply (simp add: asid_high_bits_of_shift[simplified asid_low_bits_def])
apply (simp add: asid_high_bits_of_shift[simplified asid_low_bits_def[simplified]])
apply (rule shiftl_mod[where n=10, simplified])
apply (cut_tac x="free_asid_select v" and 'a=32 in ucast_less)
apply simp
@ -1638,8 +1638,8 @@ proof -
"CSpaceAcc_A.descendants_of cref (cdt s') = {}"
"caps_of_state s' cref = Some cap"
"cap = cap.UntypedCap False frame pageBits idx"
"is_aligned (base::word32) ARM_A.asid_low_bits"
"base < 2 ^ ARM_A.asid_bits"
"is_aligned (base::word32) asid_low_bits"
"base < 2 ^ asid_bits"
assume relation:"arch_invocation_relation (InvokeAsidControl asid_inv)
(arch_invocation.InvokeASIDControl (asid_control_invocation.MakePool frame cnode_ref cref base))"
assume asid_para: "asid_inv' = asid_control_invocation.MakePool frame cnode_ref cref base"

10
proof/drefine/CNode_DR.thy
View File

@ -1159,7 +1159,7 @@ lemma set_asid_pool_empty':
done
lemma empty_pool:
"(\<lambda>x. if x \<le> 2 ^ ARM_A.asid_low_bits - 1 then None else (ap :: 10 word \<rightharpoonup> word32) x) = Map.empty"
"(\<lambda>x. if x \<le> 2 ^ asid_low_bits - 1 then None else (ap :: 10 word \<rightharpoonup> word32) x) = Map.empty"
apply (rule ext)
apply (cut_tac ptr=x and 'a=10 in word_up_bound)
apply (simp add:asid_low_bits_def)
@ -1180,8 +1180,8 @@ lemma get_set_asid_pool:
lemma set_asid_pool_empty:
"set_asid_pool a Map.empty \<equiv>
mapM_x (\<lambda>slot. get_asid_pool a >>= (\<lambda>pool. set_asid_pool a (pool(ucast slot:=None))))
[0 :: word32 .e. 2 ^ ARM_A.asid_low_bits - 1]"
using set_asid_pool_empty' [of "2 ^ ARM_A.asid_low_bits - 1" a]
[0 :: word32 .e. 2 ^ asid_low_bits - 1]"
using set_asid_pool_empty' [of "2 ^ asid_low_bits - 1" a]
apply -
apply (rule eq_reflection)
apply simp
@ -1243,7 +1243,7 @@ lemma dcorres_set_asid_pool_empty:
"dcorres dc \<top> (valid_idle and asid_pool_at a and
(\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)))
(mapM_x PageTableUnmap_D.empty_slot
(map (Pair a) [0 .e. 2 ^ ARM_A.asid_low_bits - 1]))
(map (Pair a) [0 .e. 2 ^ asid_low_bits - 1]))
(set_asid_pool a Map.empty)"
apply (unfold set_asid_pool_empty)
apply (rule dcorres_list_all2_mapM_[where F="\<lambda>x y. snd x = snd (transform_asid y)"])
@ -1269,7 +1269,7 @@ lemma dcorres_set_asid_pool_empty:
apply (wp | clarsimp)+
apply simp
apply (wp get_asid_pool_triv | clarsimp simp:typ_at_eq_kheap_obj obj_at_def swp_def)+
apply (subgoal_tac "(aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ ARM_A.asid_low_bits])")
apply (subgoal_tac "(aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ asid_low_bits])")
apply clarsimp
apply (clarsimp simp del:set_map simp: suffix_def)
apply (wp | clarsimp simp:swp_def)+

2
proof/invariant-abstract/ARM/ArchArch_AI.thy
View File

@ -1074,7 +1074,7 @@ lemma find_pd_for_asid_ref_offset_voodoo:
in hoare_strengthen_postE_R)
apply (simp add: ucast_ucast_mask
mask_asid_low_bits_ucast_ucast)
apply (fold asid_low_bits_def)
apply (fold asid_low_bits_def[simplified])
apply (rule hoare_pre, wp find_pd_for_asid_lookup_ref)
apply (simp add: )
apply (simp add: pd_shifting)

2
proof/invariant-abstract/ARM/ArchVSpace_AI.thy
View File

@ -4933,7 +4933,7 @@ lemma perform_asid_pool_invs [wp]:
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (clarsimp simp: vs_cap_ref_def mask_asid_low_bits_ucast_ucast)
apply (clarsimp simp: asid_low_bits_def[symmetric] ucast_ucast_mask
apply (clarsimp simp: asid_low_bits_def[simplified, symmetric] ucast_ucast_mask
word_neq_0_conv[symmetric])
apply (erule notE, rule asid_low_high_bits, simp_all)[1]
apply (simp add: asid_high_bits_of_def)

2
proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy
View File

@ -1416,7 +1416,7 @@ lemma find_pd_for_asid_ref_offset_voodoo:
in hoare_strengthen_postE_R)
apply (simp add: ucast_ucast_mask
mask_asid_low_bits_ucast_ucast)
apply (fold asid_low_bits_def)
apply (fold asid_low_bits_def[simplified])
apply (rule hoare_pre, wp find_pd_for_asid_lookup_ref)
apply (simp add: vspace_bits_defs)
apply (simp add: pd_shifting[simplified vspace_bits_defs, simplified] vspace_bits_defs)

2
proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy
View File

@ -5998,7 +5998,7 @@ lemma perform_asid_pool_invs [wp]:
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (clarsimp simp: vs_cap_ref_def mask_asid_low_bits_ucast_ucast)
apply (clarsimp simp: asid_low_bits_def[symmetric] ucast_ucast_mask
apply (clarsimp simp: asid_low_bits_def[simplified, symmetric] ucast_ucast_mask
word_neq_0_conv[symmetric])
apply (erule notE, rule asid_low_high_bits, simp_all)[1]
apply (simp add: asid_high_bits_of_def)

2
proof/refine/ARM/Arch_R.thy
View File

@ -888,7 +888,7 @@ shows
apply (drule dom_hd_assocsD)
apply (simp add: select_ext_fa[simplified free_asid_select_def]
free_asid_select_def o_def returnOk_liftE[symmetric]
split del: if_split)
split del: if_split)
apply (thin_tac "fst a \<notin> b \<and> P" for a b P)
apply (case_tac "isUntypedCap a \<and> capBlockSize a = objBits (makeObject::asidpool)
\<and> \<not> capIsDevice a")

9
spec/abstract/ARM/Arch_Structs_A.thy
View File

@ -56,15 +56,6 @@ definition
is_page_cap :: "arch_cap \<Rightarrow> bool" where
"is_page_cap c \<equiv> \<exists>x0 x1 x2 x3 x4. c = PageCap x0 x1 x2 x3 x4"
definition
asid_high_bits :: nat where
"asid_high_bits \<equiv> 7"
definition
asid_low_bits :: nat where
"asid_low_bits \<equiv> 10 :: nat"
definition
asid_bits :: nat where
"asid_bits \<equiv> 17 :: nat"
section \<open>Architecture-specific objects\<close>

9
spec/abstract/ARM_HYP/Arch_Structs_A.thy
View File

@ -57,15 +57,6 @@ definition
is_page_cap :: "arch_cap \<Rightarrow> bool" where
"is_page_cap c \<equiv> \<exists>x0 x1 x2 x3 x4. c = PageCap x0 x1 x2 x3 x4"
definition
asid_high_bits :: nat where
"asid_high_bits \<equiv> 7"
definition
asid_low_bits :: nat where
"asid_low_bits \<equiv> 10 :: nat"
definition
asid_bits :: nat where
"asid_bits \<equiv> 17 :: nat"
section \<open>Architecture-specific objects\<close>