X64: some progress on ArchUntyped_AI.thy
This commit is contained in:
Xin,Gao
parent
6a549daec0
commit
9d555f5197
|
|
@ -21,6 +21,10 @@ requalify_consts
|
|||
region_in_kernel_window
|
||||
arch_default_cap
|
||||
second_level_tables
|
||||
|
||||
requalify_facts
|
||||
set_cap_valid_arch_caps_simple
|
||||
set_cap_kernel_window_simple
|
||||
end
|
||||
|
||||
primrec
|
||||
|
|
@ -57,8 +61,8 @@ lemma valid_untyped_inv_wcap:
|
|||
|
||||
locale Untyped_AI_of_bl_nat_to_cref =
|
||||
assumes of_bl_nat_to_cref:
|
||||
"\<lbrakk> x < 2 ^ bits; bits < 32 \<rbrakk>
|
||||
\<Longrightarrow> (of_bl (nat_to_cref bits x) :: word32) = of_nat x"
|
||||
"\<lbrakk> x < 2 ^ bits; bits < word_bits \<rbrakk>
|
||||
\<Longrightarrow> (of_bl (nat_to_cref bits x) :: machine_word) = of_nat x"
|
||||
|
||||
lemma cnode_cap_bits_range:
|
||||
"\<lbrakk> cte_wp_at P p s; invs s \<rbrakk> \<Longrightarrow>
|
||||
|
|
@ -295,7 +299,7 @@ locale Untyped_AI_arch =
|
|||
init_arch_objects ty ptr n us y
|
||||
\<lbrace>\<lambda>rv s. caps_overlap_reserved S s\<rbrace>"
|
||||
assumes delete_objects_rewrite:
|
||||
"\<And>sz ptr.\<lbrakk>2\<le> sz; sz\<le> word_bits;ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> delete_objects ptr sz =
|
||||
"\<And>sz ptr.\<lbrakk>word_size_bits \<le> sz; sz\<le> word_bits;ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> delete_objects ptr sz =
|
||||
do y \<leftarrow> modify (clear_um {ptr + of_nat k |k. k < 2 ^ sz});
|
||||
modify ((detype {ptr && ~~ mask sz..ptr + 2 ^ sz - 1})::'state_ext state \<Rightarrow> 'state_ext state)
|
||||
od"
|
||||
|
|
@ -2779,6 +2783,9 @@ lemma ct_in_state_trans_state[simp]:
|
|||
"ct_in_state P (trans_state a s) = ct_in_state P s"
|
||||
by (simp add: ct_in_state_def)
|
||||
|
||||
(* FIXME: XIN move to Word_Lemmas 64 *)
|
||||
lemmas unat_of_nat_word_bits = unat_of_nat_eq[where 'a = 64,unfolded word_bits_len_of, simplified]
|
||||
|
||||
lemma caps_of_state_pspace_no_overlapD:
|
||||
"\<lbrakk> caps_of_state s cref = Some (cap.UntypedCap dev ptr sz idx); invs s;
|
||||
idx < 2 ^ sz \<rbrakk>
|
||||
|
|
@ -2790,8 +2797,7 @@ lemma caps_of_state_pspace_no_overlapD:
|
|||
apply (simp add: cte_wp_at_caps_of_state is_aligned_neg_mask_eq)
|
||||
apply (simp add: is_aligned_neg_mask_eq)
|
||||
apply (simp add: mask_out_sub_mask)
|
||||
apply (subst unat_of_nat_eq[where 'a=machine_word_len, unfolded word_bits_len_of],
|
||||
erule order_less_le_trans, simp_all)
|
||||
apply (subst unat_of_nat_word_bits, erule order_less_le_trans, simp_all)
|
||||
apply (rule word_of_nat_less)
|
||||
apply (erule order_less_le_trans)
|
||||
apply simp
|
||||
|
|
@ -2897,6 +2903,7 @@ lemma reset_untyped_cap_invs_etc:
|
|||
apply (frule caps_of_state_valid_cap, clarsimp+)
|
||||
apply (simp add: valid_cap_def)
|
||||
apply simp
|
||||
sorry (*
|
||||
apply (clarsimp simp: bits_of_def free_index_of_def)
|
||||
apply (rule hoare_pre, rule hoare_post_impErr,
|
||||
rule_tac P="\<lambda>i. invs and ?psp and ct_active and valid_untyped_inv_wcap ?ui
|
||||
|
|
@ -2926,7 +2933,7 @@ lemma reset_untyped_cap_invs_etc:
|
|||
apply simp
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state)
|
||||
done
|
||||
|
||||
*)
|
||||
lemma get_cap_prop_known:
|
||||
"\<lbrace>cte_wp_at (\<lambda>cp. f cp = v) slot and Q v\<rbrace> get_cap slot \<lbrace>\<lambda>rv. Q (f rv)\<rbrace>"
|
||||
apply (wp get_cap_wp)
|
||||
|
|
|
|||
|
|
@ -589,6 +589,16 @@ lemma cap_insert_simple_invs:
|
|||
done
|
||||
|
||||
lemmas is_derived_def = is_derived_def[simplified is_derived_arch_def]
|
||||
lemma set_cap_kernel_window_simple:
|
||||
"\<lbrace>\<lambda>s. cap_refs_in_kernel_window s
|
||||
\<and> cte_wp_at (\<lambda>cap'. cap_range cap' = cap_range cap) ptr s\<rbrace>
|
||||
set_cap cap ptr
|
||||
\<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>"
|
||||
apply (wp X64.set_cap_cap_refs_in_kernel_window)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state
|
||||
X64.cap_refs_in_kernel_windowD)
|
||||
done
|
||||
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -1175,6 +1175,62 @@ lemma clearMemory_um_eq_0:
|
|||
apply (fastforce simp: ignore_failure_def split: if_split_asm)
|
||||
done
|
||||
|
||||
end
|
||||
lemma invs_irq_state_independent:
|
||||
"invs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>)
|
||||
= invs s"
|
||||
by (clarsimp simp: irq_state_independent_A_def invs_def
|
||||
valid_state_def valid_pspace_def valid_mdb_def valid_ioc_def valid_idle_def
|
||||
only_idle_def if_unsafe_then_cap_def valid_reply_caps_def
|
||||
valid_reply_masters_def valid_global_refs_def valid_arch_state_def
|
||||
valid_irq_node_def valid_irq_handlers_def valid_machine_state_def
|
||||
valid_arch_objs_def valid_arch_caps_def valid_global_objs_def
|
||||
valid_kernel_mappings_def equal_kernel_mappings_def
|
||||
valid_asid_map_def vspace_at_asid_def
|
||||
pspace_in_kernel_window_def cap_refs_in_kernel_window_def
|
||||
cur_tcb_def sym_refs_def state_refs_of_def
|
||||
swp_def valid_irq_states_def)
|
||||
|
||||
lemma caps_region_kernel_window_imp:
|
||||
"caps_of_state s p = Some cap
|
||||
\<Longrightarrow> cap_refs_in_kernel_window s
|
||||
\<Longrightarrow> S \<subseteq> cap_range cap
|
||||
\<Longrightarrow> region_in_kernel_window S s"
|
||||
apply (simp add: region_in_kernel_window_def)
|
||||
apply (drule(1) cap_refs_in_kernel_windowD)
|
||||
apply blast
|
||||
done
|
||||
|
||||
(* make these available in the generic theory? *)
|
||||
crunch irq_node[wp]: init_arch_objects "\<lambda>s. P (interrupt_irq_node s)"
|
||||
(wp: crunch_wps)
|
||||
|
||||
lemma init_arch_objects_excap[wp]:
|
||||
"\<lbrace>ex_cte_cap_wp_to P p\<rbrace> init_arch_objects tp ptr bits us refs \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>"
|
||||
by (wp ex_cte_cap_to_pres )
|
||||
|
||||
crunch st_tcb_at[wp]: init_arch_objects "st_tcb_at P t"
|
||||
(wp: crunch_wps ignore: update_object set_pml4)
|
||||
|
||||
|
||||
end
|
||||
|
||||
|
||||
lemmas invs_irq_state_independent[intro!, simp]
|
||||
= X64.invs_irq_state_independent
|
||||
|
||||
lemmas caps_region_kernel_window_imp
|
||||
= X64.caps_region_kernel_window_imp
|
||||
|
||||
|
||||
lemmas init_arch_objects_invs_from_restricted
|
||||
= X64.init_arch_objects_invs_from_restricted
|
||||
|
||||
|
||||
|
||||
lemmas init_arch_objects_wps
|
||||
= X64.init_arch_objects_cte_wp_at
|
||||
X64.init_arch_objects_valid_cap
|
||||
X64.init_arch_objects_cap_table
|
||||
X64.init_arch_objects_excap
|
||||
X64.init_arch_objects_st_tcb_at
|
||||
end
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -3554,5 +3554,32 @@ lemma invs_aligned_pml4D:
|
|||
apply (simp add: pml4_bits_def pageBits_def)
|
||||
done
|
||||
|
||||
(* is this the right way? we need this fact globally but it's proven with
|
||||
ARM defns. *)
|
||||
lemma set_cap_valid_arch_caps_simple:
|
||||
"\<lbrace>\<lambda>s. valid_arch_caps s
|
||||
\<and> valid_objs s
|
||||
\<and> cte_wp_at (Not o is_arch_cap) ptr s
|
||||
\<and> (obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap)
|
||||
\<and> \<not> (is_arch_cap cap)\<rbrace>
|
||||
set_cap cap ptr
|
||||
\<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>"
|
||||
apply (wp set_cap_valid_arch_caps)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state)
|
||||
apply (frule(1) caps_of_state_valid_cap)
|
||||
apply (rename_tac cap')
|
||||
apply (subgoal_tac "\<forall>x \<in> {cap, cap'}. \<not> is_pt_cap x \<and> \<not> X64.is_pd_cap x")
|
||||
apply simp
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: vs_cap_ref_def is_cap_simps split: cap.splits)
|
||||
apply (erule impCE)
|
||||
apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
|
||||
cte_wp_at_caps_of_state is_cap_simps
|
||||
obj_ref_none_no_asid)
|
||||
apply (clarsimp simp: is_cap_simps)
|
||||
apply (rule no_cap_to_obj_with_diff_ref_triv, simp_all)
|
||||
apply (rule ccontr, clarsimp simp: table_cap_ref_def is_cap_simps)
|
||||
apply (auto simp: is_cap_simps table_cap_ref_def split: cap.splits)
|
||||
done
|
||||
end
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue