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

arch_split x64 arm: make cte_level_bits an arch constant

This commit is contained in:
Matthew Brecknell 2017-03-27 11:39:17 +11:00
parent 03e25952e3
commit bb92e92f52
19 changed files with 134 additions and 114 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
proof/invariant-abstract/ARM/ArchCNodeInv_AI.thy
View File

@ -20,6 +20,20 @@ lemma set_cap_in_device_frame[wp]:
"\<lbrace>in_device_frame buffer\<rbrace> set_cap cap ref \<lbrace>\<lambda>_. in_device_frame buffer\<rbrace>"
by (simp add: in_device_frame_def) (wp hoare_vcg_ex_lift set_cap_typ_at)
lemma valid_cnode_capI:
"\<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; n > 0; length g \<le> 32\<rbrakk>
\<Longrightarrow> s \<turnstile> cap.CNodeCap w n g"
apply (simp add: valid_cap_def cap_aligned_def)
apply (rule conjI)
apply (clarsimp simp add: pspace_aligned_def obj_at_def)
apply (drule bspec, fastforce)
apply (clarsimp simp: is_obj_defs wf_obj_bits)
apply (clarsimp simp add: obj_at_def is_obj_defs valid_objs_def dom_def)
apply (erule allE, erule impE, blast)
apply (simp add: valid_obj_def valid_cs_def valid_cs_size_def)
apply (simp add: word_bits_def cte_level_bits_def)
done
(* unused *)
lemma derive_cap_objrefs [CNodeInv_AI_assms]:
"\<lbrace>\<lambda>s. P (obj_refs cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv)\<rbrace>,-"

13
proof/invariant-abstract/ARM/ArchCSpace_AI.thy
View File

@ -20,6 +20,19 @@ context Arch begin global_naming ARM
named_theorems CSpace_AI_assms
lemma cte_at_length_limit:
"\<lbrakk> cte_at p s; valid_objs s \<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits"
apply (simp add: cte_at_cases)
apply (erule disjE)
apply clarsimp
apply (erule(1) valid_objsE)
apply (clarsimp simp: valid_obj_def well_formed_cnode_n_def valid_cs_def valid_cs_size_def
length_set_helper)
apply (drule arg_cong[where f="\<lambda>S. snd p \<in> S"])
apply (simp add: domI)
apply (clarsimp simp add: tcb_cap_cases_length word_bits_conv cte_level_bits_def)
done
(* FIXME: move? *)
lemma getActiveIRQ_wp [CSpace_AI_assms]:
"irq_state_independent_A P \<Longrightarrow>

15
proof/invariant-abstract/ARM/ArchDetype_AI.thy
View File

@ -114,6 +114,20 @@ lemma region_in_kernel_window_delete_objects[wp]:
\<lbrace>\<lambda>_. region_in_kernel_window S\<rbrace>"
by (wp | simp add: delete_objects_def do_machine_op_def split_def)+
lemma of_bl_length2:
"length xs < word_bits - cte_level_bits \<Longrightarrow> of_bl xs * 16 < (2 :: machine_word) ^ (length xs + 4)"
apply (simp add: power_add cte_level_bits_def)
apply (rule word_mult_less_mono1)
apply (rule of_bl_length, simp add: word_bits_def)
apply simp
apply simp
apply (simp add: word_bits_def)
apply (rule order_less_le_trans)
apply (erule power_strict_increasing)
apply simp
apply simp
done
end
interpretation Detype_AI?: Detype_AI
@ -536,4 +550,5 @@ lemma delete_objects_invs[wp]:
apply (simp add: valid_cap_def cap_aligned_def word_size_bits_def)
done
end
end

25
proof/invariant-abstract/ARM/ArchKernelInit_AI.thy
View File

@ -127,7 +127,7 @@ proof -
apply (rule word_add_le_mono2)
apply (simp only: trans [OF shiftl_t2n mult.commute])
apply (rule nasty_split_lt[OF P])
apply (simp_all add: cte_level_bits_def
apply (simp_all add: cte_level_bits_def
word_bits_def kernel_base_def init_irq_node_ptr_def)
done
show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
@ -193,7 +193,7 @@ lemma in_kernel_base:
lemma pspace_aligned_init_A:
"pspace_aligned init_A_st"
apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
dom_if_Some cte_level_bits_def)
dom_if_Some cte_level_bits_def)
apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
simp_all add: is_aligned_def word_bits_def kernel_base_def)[1]
done
@ -202,22 +202,20 @@ lemma pspace_distinct_init_A:
"pspace_distinct init_A_st"
apply (clarsimp simp: pspace_distinct_def state_defs pageBits_def
empty_cnode_bits kernel_base_def
cte_level_bits_def linorder_not_le cong: if_cong)
linorder_not_le cte_level_bits_def
cong: if_cong)
apply (safe,
simp_all add: init_irq_ptrs_all_ineqs
[simplified kernel_base_def, simplified])[1]
apply (cut_tac x="init_irq_node_ptr + (ucast irq << cte_level_bits)"
and y="init_irq_node_ptr + (ucast irqa << cte_level_bits)"
and sz=cte_level_bits in aligned_neq_into_no_overlap)
apply (simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def)
and sz=cte_level_bits in aligned_neq_into_no_overlap;
simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def)
apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
apply (simp add: is_aligned_def cte_level_bits_def init_irq_node_ptr_def
kernel_base_def)
apply (simp add: is_aligned_def)
apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
apply (simp add: is_aligned_def cte_level_bits_def init_irq_node_ptr_def
kernel_base_def)
apply (simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def
linorder_not_le)
apply (simp add: is_aligned_def)
apply (simp add: linorder_not_le)
done
lemma caps_of_state_init_A_st_Null:
@ -330,7 +328,7 @@ lemma invs_A:
apply (rule inj_onI)
apply (simp add: init_irq_ptrs_eq[unfolded cte_level_bits_def])
apply clarsimp
defer
apply word_bitwise
apply (simp add: valid_irq_handlers_def caps_of_state_init_A_st_Null
ran_def cong: rev_conj_cong)
apply (rule conjI)
@ -380,7 +378,7 @@ lemma invs_A:
apply (rule in_kernel_base|simp)+
apply (erule exE,drule sym,simp add:field_simps)
apply (rule in_kernel_base[simplified add.commute])
apply (rule word_less_add_right,simp add:cte_level_bits_def)
apply (rule word_less_add_right, simp add: cte_level_bits_def)
apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
apply simp
apply (simp add:cte_level_bits_def field_simps)
@ -392,7 +390,6 @@ lemma invs_A:
apply (rule in_kernel_base|simp)+
apply (simp add: cap_refs_in_kernel_window_def caps_of_state_init_A_st_Null
valid_refs_def[unfolded cte_wp_at_caps_of_state])
apply word_bitwise
done
end

4
proof/invariant-abstract/ARM/ArchUntyped_AI.thy
View File

@ -168,7 +168,7 @@ lemma retype_ret_valid_caps_captable[Untyped_AI_assms]:
\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object CapTableObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api CapTableObject us)) [0..<n])
(kheap s)\<rparr> \<turnstile> CNodeCap (ptr_add ptr (y * 2 ^ obj_bits_api CapTableObject us)) us []"
by ((clarsimp simp:valid_cap_def default_object_def cap_aligned_def
cte_level_bits_def slot_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
cte_level_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
dom_def arch_default_cap_def ptr_add_def | rule conjI | intro conjI obj_at_foldr_intro imageI
| rule is_aligned_add_multI[OF _ le_refl],
(simp add:range_cover_def word_bits_def obj_bits_api_def slot_bits_def)+)+)[1]
@ -183,7 +183,7 @@ lemma retype_ret_valid_caps_aobj[Untyped_AI_assms]:
apply (rename_tac aobject_type us n)
apply (case_tac aobject_type)
by (clarsimp simp: valid_cap_def default_object_def cap_aligned_def
cte_level_bits_def slot_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
cte_level_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
dom_def arch_default_cap_def ptr_add_def
| intro conjI obj_at_foldr_intro
imageI valid_vm_rights_def

22
proof/invariant-abstract/CNodeInv_AI.thy
View File

@ -19,7 +19,8 @@ begin
context begin interpretation Arch .
requalify_facts set_cap_arch
requalify_facts
set_cap_arch cte_at_length_limit
end
declare set_cap_arch[wp]
@ -330,21 +331,6 @@ proof -
qed
lemma valid_cnode_capI:
"\<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; n > 0; length g \<le> 32\<rbrakk>
\<Longrightarrow> s \<turnstile> cap.CNodeCap w n g"
apply (simp add: valid_cap_def cap_aligned_def)
apply (rule conjI)
apply (clarsimp simp add: pspace_aligned_def obj_at_def)
apply (drule bspec, fastforce)
apply (clarsimp simp: is_obj_defs wf_obj_bits cte_level_bits_def)
apply (clarsimp simp add: obj_at_def is_obj_defs valid_objs_def dom_def)
apply (erule allE, erule impE, blast)
apply (simp add: valid_obj_def valid_cs_def valid_cs_size_def)
apply (simp add: cte_level_bits_def word_bits_def)
done
lemma Suc_length_not_empty:
"length xs = length xs' \<Longrightarrow> Suc 0 \<le> length xs' = (xs \<noteq> [])"
by (fastforce simp: le_simps)
@ -2268,10 +2254,6 @@ lemma of_bl_eq_0:
done
(* FIXME: eliminate *)
lemmas cte_at_length = cte_at_length_limit
context CNodeInv_AI begin
lemma zombie_is_cap_toE:

13
proof/invariant-abstract/CSpace_AI.thy
View File

@ -458,19 +458,6 @@ lemma tcb_cap_cases_length:
"x \<in> dom tcb_cap_cases \<Longrightarrow> length x = 3"
by (auto simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1)
lemma cte_at_length_limit:
"\<lbrakk> cte_at p s; valid_objs s \<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits"
apply (simp add: cte_at_cases)
apply (erule disjE)
apply clarsimp
apply (erule(1) valid_objsE)
apply (clarsimp simp: valid_obj_def well_formed_cnode_n_def valid_cs_def valid_cs_size_def
length_set_helper)
apply (drule arg_cong[where f="\<lambda>S. snd p \<in> S"])
apply (simp add: domI)
apply (clarsimp simp add: tcb_cap_cases_length word_bits_conv cte_level_bits_def)
done
lemma cte_at_cref_len:
"\<lbrakk>cte_at (p, c) s; cte_at (p, c') s\<rbrakk> \<Longrightarrow> length c = length c'"

19
proof/invariant-abstract/Detype_AI.thy
View File

@ -977,10 +977,6 @@ lemma valid_pspace_well_formed_cnode[intro?]:
by (erule (1) well_formed_cnode_valid_cs_size [OF valid_cs_sizeI])
lemma clb_is_32:
"2 ^ cte_level_bits = (32 :: word32)" by (simp add: cte_level_bits_def)
lemmas cte_wp_at_cte_at = cte_wp_at_weakenE [OF _ TrueI]
@ -997,21 +993,6 @@ lemma dom_known_length:
by (drule domI[where m=f], simp)
lemma of_bl_length2:
"length xs < word_bits - cte_level_bits \<Longrightarrow> of_bl xs * 16 < (2 :: machine_word) ^ (length xs + 4)"
apply (simp add: power_add)
apply (rule word_mult_less_mono1)
apply (rule of_bl_length, simp add: word_bits_def)
apply simp
apply simp
apply (simp add: word_bits_def cte_level_bits_def)
apply (rule order_less_le_trans)
apply (erule power_strict_increasing)
apply simp
apply simp
done
lemma (in Detype_AI) cte_map_not_null_outside: (*FIXME: arch_split*)
"\<lbrakk> cte_wp_at (op \<noteq> cap.NullCap) p (s :: 'a state);
cte_wp_at (op = cap) p' s;is_untyped_cap cap;

22
proof/invariant-abstract/Invariants_AI.thy
View File

@ -1830,8 +1830,7 @@ lemma wf_cs_insert:
lemma obj_bits_CNode:
"\<lbrakk> valid_cs_size sz ps; ps cref = Some cap \<rbrakk> \<Longrightarrow>
obj_bits (CNode sz ps) = cte_level_bits + length cref"
unfolding valid_cs_size_def
by (auto simp: well_formed_cnode_n_def cte_level_bits_def)
by (auto simp: valid_cs_size_def well_formed_cnode_n_def)
lemma obj_bits_CNode':
"\<lbrakk> valid_cs_size sz ps; cref \<in> dom ps \<rbrakk> \<Longrightarrow>
@ -1965,8 +1964,7 @@ lemma valid_CNodeCapE:
apply (clarsimp simp: valid_obj_def valid_cs_def well_formed_cnode_n_def)
apply (erule valid_cs_sizeE)
apply (clarsimp simp: cap_aligned_def)
apply (drule (3) R)
apply (auto simp: cte_level_bits_def)
apply (erule (5) R)
done
lemma cap_table_at_cte_at:
@ -2298,9 +2296,8 @@ lemma wf_unique:
by (clarsimp simp: well_formed_cnode_n_def length_set_helper)
lemma wf_obj_bits:
"well_formed_cnode_n bits f \<Longrightarrow>
obj_bits (CNode bits f) = cte_level_bits + bits"
by (auto simp: cte_level_bits_def)
"well_formed_cnode_n bits f \<Longrightarrow> obj_bits (CNode bits f) = cte_level_bits + bits"
by simp
lemma wf_cs_n_unique:
"\<lbrakk> well_formed_cnode_n n f; well_formed_cnode_n n' f \<rbrakk>
@ -2309,8 +2306,7 @@ lemma wf_cs_n_unique:
lemma typ_at_range:
"\<lbrakk> typ_at T p s; pspace_aligned s; valid_objs s \<rbrakk> \<Longrightarrow>
typ_range p T \<noteq> {}"
"\<lbrakk> typ_at T p s; pspace_aligned s; valid_objs s \<rbrakk> \<Longrightarrow> typ_range p T \<noteq> {}"
apply (erule (1) obj_at_valid_objsE)
apply (clarsimp simp: pspace_aligned_def)
apply (drule bspec)
@ -2318,7 +2314,7 @@ lemma typ_at_range:
apply clarsimp
apply (case_tac ko)
apply (clarsimp simp: a_type_def split: if_split_asm)
apply (clarsimp simp: typ_range_def obj_bits_type_def interval_empty cte_level_bits_def)
apply (clarsimp simp: typ_range_def obj_bits_type_def)
apply (erule notE)
apply (erule is_aligned_no_overflow)
apply (clarsimp simp: valid_obj_def valid_cs_def valid_cs_size_def)
@ -2382,14 +2378,14 @@ lemma valid_objs_caps_contained:
apply (simp add: cap_table_at_typ)
apply (erule allE, erule allE, erule (1) impE)
apply (drule (2) typ_at_range)
apply (clarsimp simp: typ_range_def obj_bits_type_def interval_empty cte_level_bits_def)
apply (clarsimp simp: typ_range_def obj_bits_type_def)
apply fastforce
apply (clarsimp simp: valid_cap_def is_cap_simps)
apply (clarsimp simp: valid_untyped_T)
apply (simp add: tcb_at_typ)
apply (erule allE, erule allE, erule (1) impE)
apply (drule (2) typ_at_range)
apply (clarsimp simp: typ_range_def obj_bits_type_def interval_empty)
apply (clarsimp simp: typ_range_def obj_bits_type_def)
apply fastforce
done
@ -3063,7 +3059,7 @@ lemma well_formed_cnode_valid_cs_size:
lemma empty_cnode_bits:
"obj_bits (CNode n (empty_cnode n)) = cte_level_bits + n"
by (simp add: wf_empty_bits cte_level_bits_def)
by (simp add: wf_empty_bits)
lemma irq_revocableD:
"\<lbrakk> cs p = Some IRQControlCap; irq_revocable (is_original_cap s) cs \<rbrakk> \<Longrightarrow> is_original_cap s p"

14
proof/invariant-abstract/Retype_AI.thy
View File

@ -225,15 +225,13 @@ lemma (in Retype_AI_slot_bits) obj_bits_api_default_object:
"\<lbrakk> ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> obj_bits_api ty us = obj_bits (default_object ty dev us)"
unfolding obj_bits_api_def default_object_def
by (cases ty)
(simp_all add: slot_bits_def2 arch_kobj_size_cong wf_empty_bits cte_level_bits_def)
(simp_all add: slot_bits_def2 arch_kobj_size_cong wf_empty_bits)
lemma obj_bits_api_default_CapTableObject:
"obj_bits (default_object Structures_A.apiobject_type.CapTableObject dev us)
= cte_level_bits + us"
unfolding default_object_def
by (simp add: cte_level_bits_def wf_empty_bits)
by (simp add: default_object_def wf_empty_bits)
lemma empty_cnode_dom:
@ -249,7 +247,7 @@ lemma obj_bits_api_def2:
| _ \<Rightarrow> obj_bits (default_object type False obj_size_bits))"
by (simp add: obj_bits_api_def default_object_def
wf_empty_bits dom_empty_cnode ex_with_length
slot_bits_def2 cte_level_bits_def
slot_bits_def2
split: apiobject_type.split)
lemma obj_bits_api_def3:
@ -258,7 +256,7 @@ lemma obj_bits_api_def3:
else obj_bits (default_object type False obj_size_bits))"
by (simp add: obj_bits_api_def default_object_def
wf_empty_bits dom_empty_cnode ex_with_length
slot_bits_def2 cte_level_bits_def
slot_bits_def2
split: apiobject_type.split)
lemma obj_bits_api_def4:
@ -267,7 +265,7 @@ lemma obj_bits_api_def4:
else obj_bits (default_object type True obj_size_bits))"
by (simp add: obj_bits_api_def default_object_def arch_kobj_size_cong
wf_empty_bits dom_empty_cnode ex_with_length
slot_bits_def2 cte_level_bits_def
slot_bits_def2
split: apiobject_type.split)
lemma obj_bits_dev_irr:
@ -2174,7 +2172,7 @@ lemma use_retype_region_proofs':
apply (rule retype_region_proofs.intro, simp_all)[1]
apply (fastforce simp add: range_cover_def obj_bits_api_def
slot_bits_def2 word_bits_def cte_level_bits_def)+
slot_bits_def2 word_bits_def)+
done
end

10
proof/invariant-abstract/Untyped_AI.thy
View File

@ -77,13 +77,11 @@ lemma cnode_cap_bits_range:
apply (case_tac ko, simp_all add: is_cap_table_def)[1]
apply (clarsimp simp: valid_obj_def valid_cs_def well_formed_cnode_n_def
valid_cs_size_def length_set_helper
word_bits_def cte_level_bits_def)
word_bits_def)
apply (drule invs_psp_aligned)
apply (unfold pspace_aligned_def)
apply (frule domI, drule (1) bspec)
apply (clarsimp simp: obj_bits.simps ex_with_length add.commute
cte_level_bits_def
split: if_split_asm)
apply (clarsimp simp: ex_with_length add.commute split: if_split_asm)
done
@ -1356,14 +1354,14 @@ lemma retype_ret_valid_caps:
apply (case_tac tp,simp_all)
defer
apply ((clarsimp simp:valid_cap_def default_object_def cap_aligned_def
cte_level_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
is_obj_defs well_formed_cnode_n_def empty_cnode_def
dom_def ptr_add_def | rule conjI | intro conjI obj_at_foldr_intro imageI
| rule is_aligned_add_multI[OF _ le_refl],
(simp add:range_cover_def word_bits_def obj_bits_api_def)+)+)[3]
apply (rule_tac ptr=ptr and sz=sz in retype_ret_valid_caps_captable; simp)
apply (rule_tac ptr=ptr and sz=sz in retype_ret_valid_caps_aobj; simp)
apply (clarsimp simp:valid_cap_def default_object_def cap_aligned_def
cte_level_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
is_obj_defs well_formed_cnode_n_def empty_cnode_def
dom_def ptr_add_def | intro conjI obj_at_foldr_intro
imageI
| rule is_aligned_add_multI[OF _ le_refl]

13
proof/invariant-abstract/X64/ArchCNodeInv_AI.thy
View File

@ -16,6 +16,19 @@ context Arch begin global_naming X64
named_theorems CNodeInv_AI_assms
lemma valid_cnode_capI:
"\<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; n > 0; length g \<le> 64\<rbrakk>
\<Longrightarrow> s \<turnstile> cap.CNodeCap w n g"
apply (simp add: valid_cap_def cap_aligned_def)
apply (rule conjI)
apply (clarsimp simp add: pspace_aligned_def obj_at_def)
apply (drule bspec, fastforce)
apply (clarsimp simp: is_obj_defs wf_obj_bits)
apply (clarsimp simp add: obj_at_def is_obj_defs valid_objs_def dom_def)
apply (erule allE, erule impE, blast)
apply (simp add: valid_obj_def valid_cs_def valid_cs_size_def)
apply (simp add: word_bits_def cte_level_bits_def)
done
(* unused *)
lemma derive_cap_objrefs [CNodeInv_AI_assms]:

13
proof/invariant-abstract/X64/ArchCSpace_AI.thy
View File

@ -20,6 +20,19 @@ context Arch begin global_naming X64
named_theorems CSpace_AI_assms
lemma cte_at_length_limit:
"\<lbrakk> cte_at p s; valid_objs s \<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits"
apply (simp add: cte_at_cases)
apply (erule disjE)
apply clarsimp
apply (erule(1) valid_objsE)
apply (clarsimp simp: valid_obj_def well_formed_cnode_n_def valid_cs_def valid_cs_size_def
length_set_helper)
apply (drule arg_cong[where f="\<lambda>S. snd p \<in> S"])
apply (simp add: domI)
apply (clarsimp simp add: tcb_cap_cases_length word_bits_conv cte_level_bits_def)
done
(* FIXME: move? *)
lemma getActiveIRQ_wp [CSpace_AI_assms]:
"irq_state_independent_A P \<Longrightarrow>

14
proof/invariant-abstract/X64/ArchDetype_AI.thy
View File

@ -107,6 +107,20 @@ lemma region_in_kernel_window_delete_objects[wp]:
\<lbrace>\<lambda>_. region_in_kernel_window S\<rbrace>"
by (wp | simp add: delete_objects_def do_machine_op_def split_def)+
lemma of_bl_length2:
"length xs < word_bits - cte_level_bits \<Longrightarrow> of_bl xs * 32 < (2 :: machine_word) ^ (length xs + 5)"
apply (simp add: power_add cte_level_bits_def)
apply (rule word_mult_less_mono1)
apply (rule of_bl_length, simp add: word_bits_def)
apply simp
apply simp
apply (simp add: word_bits_def)
apply (rule order_less_le_trans)
apply (erule power_strict_increasing)
apply simp
apply simp
done
end
interpretation Detype_AI?: Detype_AI

15
proof/invariant-abstract/X64/ArchKernelInit_AI.thy
View File

@ -178,16 +178,13 @@ lemma pspace_distinct_init_A: "pspace_distinct init_A_st"
apply (safe; simp add: init_irq_ptrs_all_ineqs[simplified kernel_base_def, simplified])
apply (cut_tac x="init_irq_node_ptr + (ucast irq << cte_level_bits)"
and y="init_irq_node_ptr + (ucast irqa << cte_level_bits)"
and sz=cte_level_bits in aligned_neq_into_no_overlap)
apply (simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def)
and sz=cte_level_bits in aligned_neq_into_no_overlap;
simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def)
apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
apply (simp add: is_aligned_def cte_level_bits_def init_irq_node_ptr_def
kernel_base_def)
apply (simp add: is_aligned_def)
apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
apply (simp add: is_aligned_def cte_level_bits_def init_irq_node_ptr_def
kernel_base_def)
apply (simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def
linorder_not_le)
apply (simp add: is_aligned_def)
apply (simp add: linorder_not_le)
done
lemma caps_of_state_init_A_st_Null:
@ -343,7 +340,7 @@ lemma invs_A:
apply (rule in_kernel_base_in_pptr_base | simp add: bit_simps)+
apply (erule exE, drule sym, simp add:field_simps)
apply (rule in_kernel_base_in_pptr_base[simplified add.commute])
apply (rule word_less_add_right,simp add:cte_level_bits_def)
apply (rule word_less_add_right, simp add: cte_level_bits_def)
apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
apply simp
apply (simp add:cte_level_bits_def field_simps)

4
proof/invariant-abstract/X64/ArchUntyped_AI.thy
View File

@ -168,7 +168,7 @@ lemma retype_ret_valid_caps_captable[Untyped_AI_assms]:
\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object CapTableObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api CapTableObject us)) [0..<n])
(kheap s)\<rparr> \<turnstile> CNodeCap (ptr_add ptr (y * 2 ^ obj_bits_api CapTableObject us)) us []"
by ((clarsimp simp:valid_cap_def default_object_def cap_aligned_def
cte_level_bits_def slot_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
cte_level_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
dom_def arch_default_cap_def ptr_add_def | rule conjI | intro conjI obj_at_foldr_intro imageI
| rule is_aligned_add_multI[OF _ le_refl],
(simp add:range_cover_def word_bits_def obj_bits_api_def slot_bits_def)+)+)[1]
@ -183,7 +183,7 @@ lemma retype_ret_valid_caps_aobj[Untyped_AI_assms]:
apply (rename_tac aobject_type us n)
apply (case_tac aobject_type)
by (clarsimp simp: valid_cap_def default_object_def cap_aligned_def
cte_level_bits_def slot_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
cte_level_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def
dom_def arch_default_cap_def ptr_add_def
| intro conjI obj_at_foldr_intro
imageI valid_vm_rights_def

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

@ -99,11 +99,15 @@ datatype arch_kernel_obj =
| DataPage bool vmpage_size
lemmas arch_kernel_obj_cases =
arch_kernel_obj.induct[where arch_kernel_obj=x and P="\<lambda>x'. x = x' \<longrightarrow> P x'" for x P, simplified, rule_format]
arch_kernel_obj.induct[where arch_kernel_obj=x and P="\<lambda>x'. x = x' \<longrightarrow> P x'" for x P,
simplified, rule_format]
lemmas arch_kernel_obj_cases_asm =
arch_kernel_obj.induct[where arch_kernel_obj=x and P="\<lambda>x'. x = x' \<longrightarrow> P x' \<longrightarrow> R" for P R x,
simplified, rule_format, rotated -1]
arch_kernel_obj.induct[where arch_kernel_obj=x and P="\<lambda>x'. x = x' \<longrightarrow> P x' \<longrightarrow> R" for P R x,
simplified, rule_format, rotated -1]
definition [simplified slot_bits_def]:
"cte_level_bits \<equiv> slot_bits"
primrec
arch_obj_size :: "arch_cap \<Rightarrow> nat"

5
spec/abstract/Structures_A.thy
View File

@ -45,6 +45,7 @@ requalify_consts
default_arch_tcb
arch_tcb_context_get
arch_tcb_context_set
cte_level_bits
end
@ -432,10 +433,6 @@ definition
well_formed_cnode_n :: "nat \<Rightarrow> cnode_contents \<Rightarrow> bool" where
"well_formed_cnode_n n \<equiv> \<lambda>cs. dom cs = {x. length x = n}"
definition
cte_level_bits :: nat where
"cte_level_bits \<equiv> 5"
primrec
obj_bits :: "kernel_object \<Rightarrow> nat"
where

3
spec/abstract/X64/Arch_Structs_A.thy
View File

@ -163,10 +163,11 @@ datatype arch_kernel_obj =
definition table_size :: nat where
"table_size = ptTranslationBits + word_size_bits"
definition iotable_size :: nat where
"iotable_size = ptTranslationBits + 2*word_size_bits"
definition [simplified slot_bits_def]:
"cte_level_bits \<equiv> slot_bits"
primrec
arch_obj_size :: "arch_cap \<Rightarrow> nat"