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

merge x64-split into local branch

This commit is contained in:
Matthew Brecknell 2017-01-11 15:43:58 +11:00
parent 5bdcbe537e 47f78b30a6
commit a1b5f16ed6
28 changed files with 455 additions and 287 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -373,6 +373,8 @@ definition
where
"vs_lookup \<equiv> \<lambda>s. vs_lookup_trans s `` vs_asid_refs (arm_asid_table (arch_state s))"
definition "second_level_tables \<equiv> arch_state.arm_global_pts"
end
context begin interpretation Arch .

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

@ -46,11 +46,11 @@ lemma update_cap_data_closedform:
simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True
is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size
cap_ep_badge.simps badge_update_def o_def cap_rights_update_def
simp_thms cap_rights.simps Let_def split_def
simp_thms cap_rights.simps Let_def split_def badge_bits_def
the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def
arch_update_cap_data_def
cong: if_cong)
apply auto
apply (auto simp: word_bits_def cnode_padding_bits_def cnode_guard_size_bits_def)
done
lemma cap_asid_PageCap_None [simp]:

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

@ -581,7 +581,7 @@ requalify_consts post_retype_invs_check
end
definition
post_retype_invs :: "apiobject_type \<Rightarrow> word32 list \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
post_retype_invs :: "apiobject_type \<Rightarrow> machine_word list \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"post_retype_invs tp refs \<equiv>
if post_retype_invs_check tp

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

@ -326,7 +326,7 @@ declare store_pde_pred_tcb_at [wp]
(* nonempty_table *)
definition
nonempty_table :: "word32 set \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
nonempty_table :: "machine_word set \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
where
"nonempty_table S ko \<equiv>
(a_type ko = AArch APageTable \<or> a_type ko = AArch APageDirectory)
@ -342,7 +342,7 @@ lemma create_cap_valid_arch_caps[wp, Untyped_AI_assms]:
and valid_cap (default_cap tp oref sz dev)
and (\<lambda>(s::'state_ext::state_ext state). \<forall>r\<in>obj_refs (default_cap tp oref sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
and cte_wp_at (op = cap.NullCap) cref
and K (tp \<noteq> ArchObject ASIDPoolObj)\<rbrace>
create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>"
@ -361,7 +361,7 @@ lemma create_cap_valid_arch_caps[wp, Untyped_AI_assms]:
apply (case_tac cref, fastforce)
apply (simp add: obj_ref_none_no_asid)
apply (rule conjI)
apply (auto simp: is_cap_simps valid_cap_def
apply (auto simp: is_cap_simps valid_cap_def second_level_tables_def
obj_at_def nonempty_table_def a_type_simps)[1]
apply (clarsimp simp del: imp_disjL)
apply (case_tac "\<exists>x. x \<in> obj_refs cap")
@ -549,15 +549,15 @@ lemma mapM_copy_global_mappings_nonempty_table[wp]:
done
lemma init_arch_objects_nonempty_table[Untyped_AI_assms, wp]:
"\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s)
"\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
\<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and
K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us))\<rbrace>
init_arch_objects tp ptr bits us refs
\<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s)\<rbrace>"
\<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: init_arch_objects_def split del: split_if)
apply (rule hoare_pre)
apply (wp hoare_unless_wp | wpc | simp add: reserve_region_def)+
apply (wp hoare_unless_wp | wpc | simp add: reserve_region_def second_level_tables_def)+
apply (clarsimp simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def)
done

2
proof/invariant-abstract/Finalise_AI.thy
View File

@ -983,7 +983,7 @@ crunch tcb_at[wp]: unbind_notification "tcb_at t"
locale Finalise_AI_3 = Finalise_AI_2 a b
for a :: "('a :: state_ext) itself"
and b :: "('b :: state_ext) itself" +
fixes replaceable_or_arch_update :: "'a state \<Rightarrow> 32 word \<times> bool list \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
fixes replaceable_or_arch_update :: "'a state \<Rightarrow> machine_word \<times> bool list \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
fixes c :: "'c itself"
assumes finalise_cap_invs:
"\<And> cap slot x.

2
proof/invariant-abstract/IpcCancel_AI.thy
View File

@ -820,7 +820,7 @@ lemma suspend_unlive:
done
definition bound_refs_of_tcb :: "'a state \<Rightarrow> 32 word \<Rightarrow> (32 word \<times> reftype) set"
definition bound_refs_of_tcb :: "'a state \<Rightarrow> machine_word \<Rightarrow> (machine_word \<times> reftype) set"
where
"bound_refs_of_tcb s t \<equiv> case kheap s t of
Some (TCB tcb) \<Rightarrow> tcb_bound_refs (tcb_bound_notification tcb)

2
proof/invariant-abstract/Tcb_AI.thy
View File

@ -1040,7 +1040,7 @@ where
primrec
thread_control_target :: "tcb_invocation \<Rightarrow> word32"
thread_control_target :: "tcb_invocation \<Rightarrow> machine_word"
where
"thread_control_target (tcb_invocation.ThreadControl a b c d e f g h) = a"

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

@ -19,6 +19,8 @@ context begin interpretation Arch .
requalify_consts
region_in_kernel_window
arch_default_cap
second_level_tables
end
primrec
@ -61,7 +63,7 @@ locale Untyped_AI_of_bl_nat_to_cref =
lemma cnode_cap_bits_range:
"\<lbrakk> cte_wp_at P p s; invs s \<rbrakk> \<Longrightarrow>
(\<exists>c. P c \<and> (is_cnode_cap c \<longrightarrow>
(\<lambda>n. n > 0 \<and> n < 28 \<and> is_aligned (obj_ref_of c) (n + 4)) (bits_of c)))"
(\<lambda>n. n > 0 \<and> n < (word_bits - 4) \<and> is_aligned (obj_ref_of c) (n + 4)) (bits_of c)))"
apply (frule invs_valid_objs)
apply (drule(1) cte_wp_at_valid_objs_valid_cap)
apply clarsimp
@ -298,7 +300,7 @@ locale Untyped_AI_arch =
"\<And>ptr sz s x6 us n dev. \<lbrakk>pspace_no_overlap_range_cover ptr sz (s::'state_ext state) \<and> x6 \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \<and> ptr \<noteq> 0(*; tp = ArchObject x6*)\<rbrakk>
\<Longrightarrow> \<forall>y\<in>{0..<n}. s
\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x6) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0..<n])
(kheap s)\<rparr> \<turnstile> ArchObjectCap (ARM_A.arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)"
(kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)"
assumes init_arch_objects_descendants_range[wp]:
"\<And>x cref ty ptr n us y. \<lbrace>\<lambda>(s::'state_ext state). descendants_range x cref s \<rbrace> init_arch_objects ty ptr n us y
@ -388,20 +390,23 @@ qed
lemma range_cover_stuff:
"\<lbrakk>0 < n;n \<le> unat ((2::word32) ^ sz - of_nat rv >> bits);
notes unat_power_lower_machine = unat_power_lower[where 'a=machine_word_len]
notes unat_of_nat_machine = unat_of_nat_eq[where 'a=machine_word_len]
shows
"\<lbrakk>0 < n;n \<le> unat ((2::machine_word) ^ sz - of_nat rv >> bits);
rv \<le> 2^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow>
rv \<le> unat (alignUp (w + of_nat rv) bits - w) \<and>
(alignUp (w + of_nat rv) bits) && ~~ mask sz = w \<and>
range_cover (alignUp (w + ((of_nat rv)::word32)) bits) sz bits n"
range_cover (alignUp (w + ((of_nat rv)::machine_word)) bits) sz bits n"
apply (clarsimp simp: range_cover_def)
proof (intro conjI)
assume not_0 : "0<n"
assume bound : "n \<le> unat ((2::word32) ^ sz - of_nat rv >> bits)" "rv\<le> 2^sz"
assume bound : "n \<le> unat ((2::machine_word) ^ sz - of_nat rv >> bits)" "rv\<le> 2^sz"
"sz < word_bits"
assume al: "is_aligned w sz"
have space: "(2::word32) ^ sz - of_nat rv \<le> 2^ sz"
have space: "(2::machine_word) ^ sz - of_nat rv \<le> 2^ sz"
apply (rule word_sub_le[OF word_of_nat_le])
apply (clarsimp simp: bound unat_power_lower32)
apply (clarsimp simp: bound unat_power_lower_machine)
done
show cmp: "bits \<le> sz"
using not_0 bound
@ -411,7 +416,7 @@ lemma range_cover_stuff:
apply (drule le_trans)
apply (rule word_le_nat_alt[THEN iffD1])
apply (rule le_shiftr[OF space])
apply (subgoal_tac "(2::word32)^sz >> bits = 0")
apply (subgoal_tac "(2::machine_word)^sz >> bits = 0")
apply simp
apply (rule and_mask_eq_iff_shiftr_0[THEN iffD1])
apply (simp add: and_mask_eq_iff_le_mask)
@ -419,18 +424,18 @@ lemma range_cover_stuff:
apply (simp add: word_bits_def mask_def power_overflow)
apply (subst le_mask_iff_lt_2n[THEN iffD1])
apply (simp add: word_bits_def)
apply (simp add: word_less_nat_alt[THEN iffD2] unat_power_lower32)
apply (simp add: word_less_nat_alt[THEN iffD2] unat_power_lower_machine)
done
have shiftr_t2n[simp]:"(2::word32)^sz >> bits = 2^ (sz - bits)"
have shiftr_t2n[simp]:"(2::machine_word)^sz >> bits = 2^ (sz - bits)"
using bound cmp
apply (case_tac "sz = 0",simp)
apply (subgoal_tac "(1::word32) << sz >> bits = 2^ (sz -bits)")
apply (subgoal_tac "(1::machine_word) << sz >> bits = 2^ (sz -bits)")
apply simp
apply (subst shiftl_shiftr1)
apply (simp add: word_size word_bits_def shiftl_t2n word_1_and_bl)+
done
have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: word32) ^ sz"
have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: machine_word) ^ sz"
using bound cmp not_0
apply -
apply (case_tac "rv = 0")
@ -438,7 +443,7 @@ lemma range_cover_stuff:
apply (clarsimp simp: alignUp_def2)
apply (subst mask_eq_x_eq_0[THEN iffD1])
apply (simp add: and_mask_eq_iff_le_mask mask_def)
apply (simp add: p2_gt_0[where 'a=32, folded word_bits_def])
apply (simp add: p2_gt_0[where 'a=machine_word_len, folded word_bits_def])
apply (simp add: alignUp_def3)
apply (subgoal_tac "1 \<le> unat (2 ^ sz - of_nat rv >> bits)")
prefer 2
@ -448,11 +453,11 @@ lemma range_cover_stuff:
apply (simp add: shiftr_div_2n')
apply (simp add: td_gal[symmetric])
apply (subst (asm) unat_sub)
apply (simp add: word_of_nat_le unat_power_lower32)
apply (simp add: word_of_nat_le unat_power_lower_machine)
apply (simp add: le_diff_conv2 word_of_nat_le unat_le_helper word_less_nat_alt)
apply (rule le_less_trans[OF unat_plus_gt])
apply (rule less_le_trans[where y = "2^bits + unat (of_nat rv)"])
apply (simp add: unat_power_lower32)
apply (simp add: unat_power_lower_machine)
apply (rule le_less_trans[OF _ measure_unat])
apply (rule word_le_nat_alt[THEN iffD1])
apply (rule word_and_le2)
@ -460,10 +465,10 @@ lemma range_cover_stuff:
apply (subst word_bits_def[symmetric])
apply (erule le_less_trans)
apply simp
apply (simp add: unat_power_lower32)
apply (simp add: unat_power_lower_machine)
done
show "n + unat (alignUp (w + ((of_nat rv)::word32)) bits && mask sz >> bits) \<le> 2 ^ (sz - bits)"
show "n + unat (alignUp (w + ((of_nat rv)::machine_word)) bits && mask sz >> bits) \<le> 2 ^ (sz - bits)"
using not_0 bound cmp
apply -
apply (erule le_trans[OF add_le_mono])
@ -508,37 +513,42 @@ lemma range_cover_stuff:
apply (case_tac "rv = 0")
apply simp
apply (rule le_trans[OF _ word_le_nat_alt[THEN iffD1,OF alignUp_ge]])
apply (subst unat_of_nat32)
apply (erule le_less_trans)
apply simp
apply (simp_all add: word_bits_def)[2]
apply (subst unat_of_nat_machine)
apply (erule le_less_trans)
apply (rule power_strict_increasing)
apply (simp_all add: word_bits_def)[4]
apply (rule alignUp_is_aligned_nz[where x = "2^sz"])
apply (rule is_aligned_weaken[OF is_aligned_triv2])
apply (simp_all add: word_bits_def)[2]
apply (subst word_of_nat_le)
apply (subst unat_power_lower32)
apply simp+
apply (erule of_nat_neq_0)
apply (erule le_less_trans)
apply (subst word_bits_def[symmetric])
apply simp
done
apply (rule is_aligned_weaken[OF is_aligned_triv2])
apply (simp_all add: word_bits_def)[2]
apply (subst word_of_nat_le)
apply (subst unat_power_lower_machine)
apply (simp add: word_bits_def)+
apply (erule of_nat_neq_0)
apply (erule le_less_trans)
apply (rule power_strict_increasing)
apply (simp add: word_bits_def)+
done
show "alignUp (w + of_nat rv) bits && ~~ mask sz = w"
using bound not_0 cmp al
apply (clarsimp simp: alignUp_plus[OF is_aligned_weaken]
mask_out_add_aligned[symmetric])
apply (clarsimp simp: and_not_mask)
apply (subgoal_tac "alignUp ((of_nat rv)::word32) bits >> sz = 0")
apply (subgoal_tac "alignUp ((of_nat rv)::machine_word) bits >> sz = 0")
apply simp
apply (simp add: le_mask_iff[symmetric] mask_def)
done
show "sz < 32" by (simp add: bound(3)[unfolded word_bits_def, simplified])
qed
qed (simp add: word_bits_def)
context Arch begin
(*FIXME: generify proof that uses this *)
lemmas range_cover_stuff_arch = range_cover_stuff[unfolded word_bits_def, simplified]
end
lemma cte_wp_at_range_cover:
"\<lbrakk>bits < word_bits; rv\<le> 2^ sz; invs s;
cte_wp_at (op = (cap.UntypedCap dev w sz idx)) p s;
0 < n; n \<le> unat ((2::word32) ^ sz - of_nat rv >> bits)\<rbrakk>
0 < n; n \<le> unat ((2::machine_word) ^ sz - of_nat rv >> bits)\<rbrakk>
\<Longrightarrow> range_cover (alignUp (w + of_nat rv) bits) sz bits n"
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (frule(1) caps_of_state_valid)
@ -550,7 +560,7 @@ lemma cte_wp_at_range_cover:
lemma le_mask_le_2p:
"\<lbrakk>idx \<le> unat ((ptr::word32) && mask sz);sz < word_bits\<rbrakk> \<Longrightarrow> idx < 2^ sz"
"\<lbrakk>idx \<le> unat ((ptr::machine_word) && mask sz);sz < word_bits\<rbrakk> \<Longrightarrow> idx < 2^ sz"
apply (erule le_less_trans)
apply (rule unat_less_helper)
apply simp
@ -680,18 +690,18 @@ lemma cases_imp_eq:
by blast
lemma inj_16:
"\<lbrakk> of_nat x * 16 = of_nat y * (16 :: word32);
"\<lbrakk> of_nat x * 16 = of_nat y * (16 :: machine_word);
x < bnd; y < bnd; bnd \<le> 2 ^ (word_bits - 4) \<rbrakk>
\<Longrightarrow> of_nat x = (of_nat y :: word32)"
\<Longrightarrow> of_nat x = (of_nat y :: machine_word)"
apply (fold shiftl_t2n [where n=4, simplified, simplified mult.commute])
apply (simp only: word_bl.Rep_inject[symmetric]
bl_shiftl)
apply (drule(1) order_less_le_trans)+
apply (drule of_nat_mono_maybe[rotated, where 'a=32])
apply (drule of_nat_mono_maybe[rotated, where 'a=machine_word_len])
apply (rule power_strict_increasing)
apply (simp add: word_bits_def)
apply simp
apply (drule of_nat_mono_maybe[rotated, where 'a=32])
apply (drule of_nat_mono_maybe[rotated, where 'a=machine_word_len])
apply (rule power_strict_increasing)
apply (simp add: word_bits_def)
apply simp
@ -703,12 +713,15 @@ lemma inj_16:
lemma of_nat_shiftR:
"a < 2 ^ word_bits \<Longrightarrow>
unat (of_nat (shiftR a b)::word32) = unat ((of_nat a :: word32) >> b)"
unat (of_nat (shiftR a b)::machine_word) = unat ((of_nat a :: machine_word) >> b)"
apply (subst shiftr_div_2n')
apply (clarsimp simp: shiftR_nat)
apply (subst unat_of_nat32)
apply (subst unat_of_nat_eq[where 'a=machine_word_len])
apply (simp only: word_bits_def)
apply (erule le_less_trans[OF div_le_dividend])
apply (simp add: unat_of_nat32)
apply (subst unat_of_nat_eq[where 'a=machine_word_len])
apply (simp only: word_bits_def)
apply simp
done
@ -1466,17 +1479,17 @@ lemma of_nat_shift_distinct_helper:
done
lemmas of_nat_shift_distinct_helper32 = of_nat_shift_distinct_helper[where 'a=32, folded word_bits_def]
lemmas of_nat_shift_distinct_helper_machine = of_nat_shift_distinct_helper[where 'a=machine_word_len, folded word_bits_def]
lemma ptr_add_distinct_helper:
"\<lbrakk> ptr_add (p :: word32) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \<noteq> y;
"\<lbrakk> ptr_add (p :: machine_word) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \<noteq> y;
x < bnd; y < bnd; n < word_bits;
bnd \<le> 2 ^ (word_bits - n) \<rbrakk>
\<Longrightarrow> P"
apply (clarsimp simp: ptr_add_def word_unat_power[symmetric]
shiftl_t2n[symmetric, simplified mult.commute])
apply (erule(5) of_nat_shift_distinct_helper32)
apply (erule(5) of_nat_shift_distinct_helper_machine)
done
@ -1637,12 +1650,12 @@ lemma retype_region_distinct_sets:
apply (clarsimp simp: retype_addrs_def distinct_prop_map)
apply (rule distinct_prop_distinct)
apply simp
apply (subgoal_tac "of_nat y * (2::word32) ^ obj_bits_api tp us \<noteq> of_nat x * 2 ^ obj_bits_api tp us")
apply (subgoal_tac "of_nat y * (2::machine_word) ^ obj_bits_api tp us \<noteq> of_nat x * 2 ^ obj_bits_api tp us")
apply (case_tac tp) defer
apply (simp add:cap_range_def ptr_add_def)+
apply (clarsimp simp: ptr_add_def word_unat_power[symmetric]
shiftl_t2n[simplified mult.commute, symmetric])
apply (erule(2) of_nat_shift_distinct_helper[where 'a=32 and n = "obj_bits_api tp us"])
apply (erule(2) of_nat_shift_distinct_helper[where 'a=machine_word_len and n = "obj_bits_api tp us"])
apply simp
apply (simp add:range_cover_def)
apply (erule range_cover.range_cover_n_le)
@ -2064,10 +2077,10 @@ lemma op_equal: "(\<lambda>x. x = c) = (op = c)" by (rule ext) auto
lemma mask_out_eq_0:
"\<lbrakk>idx < 2^ sz;sz<word_bits\<rbrakk> \<Longrightarrow> ((of_nat idx)::word32) && ~~ mask sz = 0"
"\<lbrakk>idx < 2^ sz;sz<word_bits\<rbrakk> \<Longrightarrow> ((of_nat idx)::machine_word) && ~~ mask sz = 0"
apply (clarsimp simp: mask_out_sub_mask)
apply (subst less_mask_eq[symmetric])
apply (erule(1) of_nat_less_pow_32)
apply (erule(1) of_nat_power[where 'a=machine_word_len, folded word_bits_def])
apply simp
done
@ -2090,7 +2103,7 @@ lemma is_aligned_neg_mask_eq':
lemma neg_mask_mask_unat:
"sz < word_bits \<Longrightarrow>
unat ((ptr::word32) && ~~ mask sz) + unat (ptr && mask sz) = unat ptr"
unat ((ptr::machine_word) && ~~ mask sz) + unat (ptr && mask sz) = unat ptr"
apply (subst unat_plus_simple[THEN iffD1,symmetric])
apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask[OF le_refl]])
apply (rule and_mask_less')
@ -2320,7 +2333,7 @@ proof -
apply -
apply (erule disjE)
apply (erule cte_wp_at_caps_descendants_range_inI[OF _ _ _ range_cover.sz(1)
[where 'a=32, folded word_bits_def]])
[where 'a=machine_word_len, folded word_bits_def]])
apply (simp add:cte_wp_at_caps_of_state desc_range)+
done
thus "descendants_range_in usable_range cref s"
@ -2340,7 +2353,7 @@ lemma ps_no_overlap[simp]: "\<not> reset \<longrightarrow> pspace_no_overlap_ran
using misc cte_wp_at cover idx_cases
apply clarsimp
apply (erule cte_wp_at_pspace_no_overlapI[OF _ _ _
range_cover.sz(1)[where 'a=32, folded word_bits_def]])
range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]])
apply (simp add: cte_wp_at_caps_of_state)
apply simp+
done
@ -2350,7 +2363,7 @@ lemma caps_no_overlap[simp]: "caps_no_overlap ptr sz s"
apply -
apply (erule disjE)
apply (erule cte_wp_at_caps_no_overlapI[OF _ _ _ range_cover.sz(1)
[where 'a=32, folded word_bits_def]])
[where 'a=machine_word_len, folded word_bits_def]])
apply (simp add:cte_wp_at_caps_of_state)+
apply (erule descendants_range_caps_no_overlapI)
apply (simp add:cte_wp_at_caps_of_state desc_range)+
@ -2415,14 +2428,14 @@ lemma usable_range_disjoint:
{ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {}"
proof -
have idx_compare''[simp]:
"unat ((ptr && mask sz) + (of_nat (length slots) * (2::word32) ^ obj_bits_api tp us)) < 2 ^ sz
"unat ((ptr && mask sz) + (of_nat (length slots) * (2::machine_word) ^ obj_bits_api tp us)) < 2 ^ sz
\<Longrightarrow> ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1
< ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us"
apply (rule minus_one_helper,simp)
apply (rule neq_0_no_wrap)
apply (rule machine_word_plus_mono_right_split)
apply (simp add:shiftl_t2n range_cover_unat[OF cover] field_simps)
apply (simp add:range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+
apply (simp add:range_cover.sz[where 'a=machine_word_len, folded word_bits_def, OF cover])+
done
show ?thesis
apply (clarsimp simp:mask_out_sub_mask blah)
@ -2526,14 +2539,14 @@ lemma valid_untyped_cap_inc:
apply simp
apply (erule disjoint_subset[rotated])
apply (frule(1) le_mask_le_2p[OF _
range_cover.sz(1)[where 'a=32, folded word_bits_def]])
range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]])
apply clarsimp
apply (rule word_plus_mono_right)
apply (rule word_of_nat_le)
apply (simp add: unat_of_nat32 range_cover_unat field_simps)
apply (simp add: unat_of_nat_eq[where 'a=machine_word_len] range_cover_unat field_simps)
apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask[OF le_refl]])
apply (simp add: word_less_nat_alt
unat_power_lower[where 'a=32, folded word_bits_def])
unat_power_lower[where 'a=machine_word_len, folded word_bits_def])
apply (simp add: range_cover_unat range_cover.unat_of_nat_shift shiftl_t2n field_simps)
apply (subst add.commute)
apply (simp add: range_cover.range_cover_compare_bound)
@ -3116,16 +3129,15 @@ lemma create_cap_irq_handlers[wp]:
crunch valid_arch_objs[wp]: create_cap "valid_arch_objs"
(simp: crunch_simps)
locale Untyped_AI_nonempty_table =
fixes state_ext_t :: "('state_ext::state_ext) itself"
fixes nonempty_table :: "word32 set \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
fixes nonempty_table :: "machine_word set \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
assumes create_cap_valid_arch_caps[wp]:
"\<And>tp oref sz dev cref p.\<lbrace>valid_arch_caps
and valid_cap (default_cap tp oref sz dev)
and (\<lambda>(s::'state_ext state). \<forall>r\<in>obj_refs (default_cap tp oref sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
and cte_wp_at (op = cap.NullCap) cref
and K (tp \<noteq> ArchObject ASIDPoolObj)\<rbrace>
create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>"
@ -3223,7 +3235,7 @@ lemma (in Untyped_AI_nonempty_table) create_cap_invs[wp]:
and real_cte_at cref
and (\<lambda>(s::'state_ext state). \<forall>r\<in>obj_refs (default_cap tp oref sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
and K (p \<noteq> cref \<and> tp \<noteq> ArchObject ASIDPoolObj)\<rbrace>
create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (rule hoare_pre)
@ -3256,9 +3268,9 @@ lemma create_cap_no_cap[wp]:
done
lemma (in Untyped_AI_nonempty_table) create_cap_nonempty_tables[wp]:
"\<lbrace>\<lambda>s. P (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) p s)\<rbrace>
"\<lbrace>\<lambda>s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>
create_cap tp sz p' dev (cref, oref)
\<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) p s)\<rbrace>"
\<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>"
apply (rule hoare_pre)
apply (rule hoare_use_eq [where f=arch_state, OF create_cap_arch_state])
apply (simp add: create_cap_def set_cdt_def)
@ -3308,7 +3320,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs_inv:
real_cte_at (fst tup) s)
\<and> (\<forall>tup \<in> set ((cref,oref)#list). \<forall>r \<in> obj_refs (default_cap tp (snd tup) sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> Structures_A.obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
\<and> distinct (p # (map fst ((cref,oref)#list)))
\<and> tp \<noteq> ArchObject ASIDPoolObj) \<rbrace>
create_cap tp sz p dev (cref,oref)
@ -3333,7 +3345,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs_inv:
real_cte_at (fst tup) s)
\<and> (\<forall>tup \<in> set list. \<forall>r \<in> obj_refs (default_cap tp (snd tup) sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> Structures_A.obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
\<and> distinct (p # (map fst list))
\<and> tp \<noteq> ArchObject ASIDPoolObj) \<rbrace>"
apply (rule hoare_pre)
@ -3385,7 +3397,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs:
real_cte_at (fst tup) s)
\<and> (\<forall>tup \<in> set (zip crefs orefs). \<forall>r \<in> obj_refs (default_cap tp (snd tup) sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> Structures_A.obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
\<and> distinct (p # (map fst (zip crefs orefs)))
\<and> tp \<noteq> ArchObject ASIDPoolObj)
and K (set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us))\<rbrace>
@ -3488,7 +3500,7 @@ lemma retype_region_refs_distinct[wp]:
| drule subsetD [OF obj_refs_default_cap]
less_two_pow_divD)+
apply (simp add: range_cover_def word_bits_def)
apply (erule range_cover.range_cover_n_le[where 'a=32, folded word_bits_def])
apply (erule range_cover.range_cover_n_le[where 'a=machine_word_len, folded word_bits_def])
done
@ -3543,9 +3555,9 @@ lemma do_machine_op_obj_at_arch_state[wp]:
by (clarsimp simp: do_machine_op_def split_def | wp)+
lemma (in Untyped_AI_nonempty_table) retype_nonempty_table[wp]:
"\<lbrace>\<lambda>(s::('state_ext::state_ext) state). \<not> (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\<rbrace>
"\<lbrace>\<lambda>(s::('state_ext::state_ext) state). \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>
retype_region ptr sz us tp dev
\<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\<rbrace>"
\<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>"
apply (simp add: retype_region_def split del: split_if)
apply (rule hoare_pre)
apply (wp|simp del: fun_upd_apply)+
@ -3575,9 +3587,9 @@ lemma invs_cap_refs_in_kernel_window[elim!]:
by (simp add: invs_def valid_state_def)
lemma (in Untyped_AI_nonempty_table) set_cap_nonempty_tables[wp]:
"\<lbrace>\<lambda>s. P (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) p s)\<rbrace>
"\<lbrace>\<lambda>s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>
set_cap cap cref
\<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) p s)\<rbrace>"
\<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>"
apply (rule hoare_pre)
apply (rule hoare_use_eq [where f=arch_state, OF set_cap_arch])
apply (wp set_cap_obj_at_impossible)

8
proof/invariant-abstract/X64/ArchBCorres2_AI.thy
View File

@ -34,7 +34,7 @@ lemma invoke_tcb_bcorres[wp]:
fixes a
shows "bcorres (invoke_tcb a) (invoke_tcb a)"
apply (cases a)
apply (wp | wpc | simp)+
apply (wp | wpc | simp add: set_mcpriority_def)+
apply (rename_tac option)
apply (case_tac option)
apply (wp | wpc | simp)+
@ -53,7 +53,7 @@ lemma transfer_caps_loop_bcorres[wp]:
lemma invoke_irq_control_bcorres[wp]: "bcorres (invoke_irq_control a) (invoke_irq_control a)"
apply (cases a)
apply (wp | simp add: arch_invoke_irq_control_def)+
apply (wp | simp add: arch_invoke_irq_control_def | wpc)+
done
lemma invoke_irq_handler_bcorres[wp]: "bcorres (invoke_irq_handler a) (invoke_irq_handler a)"
@ -75,7 +75,7 @@ lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (d
apply (wp | wpc | simp add: split_def | intro impI conjI)+
done
crunch (bcorres)bcorres[wp]: decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_bind_notification,decode_unbind_notification truncate_state
crunch (bcorres)bcorres[wp]: decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_set_mcpriority,decode_bind_notification,decode_unbind_notification truncate_state
lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
(decode_tcb_configure b (cap.ThreadCap c) d e)"
@ -111,7 +111,7 @@ lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def handle_interrupt_def Let_def | intro impI conjI allI | wp | wpc)+
done
crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord clearExMonitor)
crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord)
lemma choose_switch_or_idle:
"((), s') \<in> fst (choose_thread s) \<Longrightarrow>

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

@ -112,7 +112,7 @@ lemma same_object_as_def2:
\<and> \<not> cp = NullCap \<and> \<not> is_untyped_cap cp
\<and> \<not> is_zombie cp
\<and> (is_arch_cap cp \<longrightarrow>
(case the_arch_cap cp of PageCap x rs sz v
(case the_arch_cap cp of PageCap d x rs tp sz v
\<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1
| _ \<Rightarrow> True)))"
apply (simp add: same_object_as_def is_cap_simps split: cap.split)

72
proof/invariant-abstract/X64/ArchEmptyFail_AI.thy
View File

@ -17,13 +17,9 @@ context Arch begin global_naming X64
named_theorems EmptyFail_AI_assms
crunch_ignore (empty_fail)
(add: invalidateTLB_ASID_impl invalidateTLB_VAASID_impl cleanByVA_impl
cleanByVA_PoU_impl invalidateByVA_impl invalidateByVA_I_impl
invalidate_I_PoU_impl cleanInvalByVA_impl branchFlush_impl
clean_D_PoU_impl cleanInvalidate_D_PoC_impl cleanInvalidateL2Range_impl
invalidateL2Range_impl cleanL2Range_impl flushBTAC_impl
writeContextID_impl isb_impl dsb_impl dmb_impl setHardwareASID_impl
writeTTBR0_impl cacheRangeOp)
(add: setCurrentVSpaceRoot_impl invalidateTLBEntry_impl invalidatePageStructureCache_impl
resetCR3_impl hwASIDInvalidate_impl ioapicMapPinToVector_impl updateIRQState_impl
in8_impl in16_impl in32_impl out8_impl out16_impl out32_impl)
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]:
loadWord, load_word_offs, storeWord, getRestartPC, get_mrs
@ -42,6 +38,18 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
(simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits
bool.splits list.splits thread_state.splits split_def catch_def sum.splits
Let_def wp: zipWithM_x_empty_fail)
lemma port_out_empty_fail[simp, intro!]:
assumes ef: "\<And>a. empty_fail (oper a)"
shows "empty_fail (port_out oper w)"
apply (simp add: port_out_def)
by (wp | simp add: ef)+
lemma port_in_empty_fail[simp, intro!]:
assumes ef: "empty_fail oper"
shows "empty_fail (port_in oper)"
apply (simp add: port_in_def)
by (wp | simp add: ef)+
crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification
(simp: cap.splits arch_cap.splits split_def)
@ -49,31 +57,43 @@ crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notificati
lemma decode_tcb_invocation_empty_fail[wp]:
"empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)"
by (simp add: decode_tcb_invocation_def split: invocation_label.splits | wp | intro conjI impI)+
crunch (empty_fail) empty_fail[wp]: find_vspace_for_asid, check_vp_alignment,
ensure_safe_mapping, get_asid_pool, lookup_pt_slot,
decode_port_invocation
(simp: kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits
pdpte.splits pml4e.splits vmpage_size.splits)
crunch (empty_fail) empty_fail[wp]: find_pd_for_asid, get_master_pde, check_vp_alignment,
create_mapping_entries, ensure_safe_mapping, get_asid_pool, resolve_vaddr
(simp: kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits)
lemma create_mapping_entries_empty_fail[wp]:
"empty_fail (create_mapping_entries a b c d e f)"
by (case_tac c; simp add: create_mapping_entries_def; wp)
lemma arch_decode_X64ASIDControlMakePool_empty_fail:
"invocation_type label = ArchInvocationLabel X64ASIDControlMakePool
\<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)"
apply (simp add: arch_decode_invocation_def Let_def)
apply (intro impI conjI allI)
apply (simp add: isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits)+
apply (rule impI)
apply (simp split: arch_cap.splits)
apply (intro conjI impI)
apply (simp add: split_def)
apply wp
apply simp
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: split_if_asm)
by (simp add: Let_def split: cap.splits arch_cap.splits option.splits | wp | intro conjI impI allI)+
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def
returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: split_if_asm)
apply (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+
by (clarsimp simp add: decode_page_invocation_def split: arch_cap.splits | wp)+
lemma arch_decode_X64ASIDPoolAssign_empty_fail:
"invocation_type label = ArchInvocationLabel X64ASIDPoolAssign
\<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)"
apply (simp add: arch_decode_invocation_def split_def Let_def isPageFlushLabel_def isPDFlushLabel_def
apply (simp add: arch_decode_invocation_def Let_def split: arch_cap.splits)
apply (intro impI allI conjI)
apply (simp add: arch_decode_invocation_def split_def Let_def
split: arch_cap.splits cap.splits option.splits | intro impI allI)+
apply clarsimp
apply (rule empty_fail_bindE)
apply simp
apply (rule empty_fail_bindE)
@ -87,7 +107,7 @@ lemma arch_decode_X64ASIDPoolAssign_empty_fail:
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
gets_def get_def assert_def fail_def)
apply wp
apply (clarsimp simp: decode_page_invocation_def | wp)+
done
lemma arch_decode_invocation_empty_fail[wp]:
@ -99,7 +119,8 @@ lemma arch_decode_invocation_empty_fail[wp]:
apply (find_goal \<open>succeeds \<open>erule arch_decode_X64ASIDControlMakePool_empty_fail\<close>\<close>)
apply (find_goal \<open>succeeds \<open>erule arch_decode_X64ASIDPoolAssign_empty_fail\<close>\<close>)
apply ((simp add: arch_decode_X64ASIDControlMakePool_empty_fail arch_decode_X64ASIDPoolAssign_empty_fail)+)[2]
by ((simp add: arch_decode_invocation_def Let_def split: arch_cap.splits cap.splits option.splits | wp | intro conjI impI allI)+)
by ((simp add: arch_decode_invocation_def decode_page_invocation_def Let_def
split: arch_cap.splits cap.splits option.splits | wp | intro conjI impI allI)+)
end
@ -111,12 +132,19 @@ global_interpretation EmptyFail_AI_derive_cap?: EmptyFail_AI_derive_cap
context Arch begin global_naming X64
lemma flush_table_empty_fail[simp, wp]: "empty_fail (flush_table a b c)"
unfolding flush_table_def
apply simp
apply (wp | wpc)+
done
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slot,
setHardwareASID, setCurrentPD, finalise_cap, preemption_point,
finalise_cap, preemption_point,
cap_swap_for_delete, decode_invocation
(simp: Let_def catch_def split_def OR_choiceE_def mk_ef_def option.splits endpoint.splits
notification.splits thread_state.splits sum.splits cap.splits arch_cap.splits
kernel_object.splits vmpage_size.splits pde.splits bool.splits list.splits)
kernel_object.splits vmpage_size.splits pde.splits bool.splits list.splits
forM_x_def empty_fail_mapM_x)
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: setRegister, setNextPC
@ -159,8 +187,8 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_event, activate_t
thread_state.splits endpoint.splits catch_def sum.splits cnode_invocation.splits
page_table_invocation.splits page_invocation.splits asid_control_invocation.splits
asid_pool_invocation.splits arch_invocation.splits irq_state.splits syscall.splits
flush_type.splits page_directory_invocation.splits
ignore: resetTimer_impl ackInterrupt_impl)
page_directory_invocation.splits
ignore: resetTimer_impl)
end
global_interpretation EmptyFail_AI_call_kernel_unit?: EmptyFail_AI_call_kernel_unit

86
proof/invariant-abstract/X64/ArchFinalise_AI.thy
View File

@ -21,12 +21,12 @@ lemma (* obj_at_not_live_valid_arch_cap_strg *) [Finalise_AI_asms]:
\<longrightarrow> obj_at (\<lambda>ko. \<not> live ko) r s"
by (clarsimp simp: valid_cap_def obj_at_def
a_type_arch_live
split: arch_cap.split_asm)
split: arch_cap.split_asm split_if_asm)
global_naming X64
lemma valid_global_refs_asid_table_udapte [iff]:
"valid_global_refs (s\<lparr>arch_state := arm_asid_table_update f (arch_state s)\<rparr>) =
"valid_global_refs (s\<lparr>arch_state := x64_asid_table_update f (arch_state s)\<rparr>) =
valid_global_refs s"
by (simp add: valid_global_refs_def global_refs_def)
@ -43,8 +43,10 @@ lemma reachable_pg_cap_update[simp]:
by (simp add:reachable_pg_cap_def vs_lookup_pages_def
vs_lookup_pages1_def obj_at_def)
(* FIXME x64: this needs stuff about equality between vs_lookup and vs_lookup_pages
for PageMapL4, PDPTs *)
lemma vs_lookup_pages_eq:
"\<lbrakk>valid_arch_objs s; valid_asid_table (arm_asid_table (arch_state s)) s;
"\<lbrakk>valid_arch_objs s; valid_asid_table (x64_asid_table (arch_state s)) s;
valid_cap cap s; table_cap_ref cap = Some vref; oref \<in> obj_refs cap\<rbrakk>
\<Longrightarrow> (vref \<unrhd> oref) s = (vref \<rhd> oref) s"
apply (clarsimp simp: table_cap_ref_def
@ -54,10 +56,10 @@ lemma vs_lookup_pages_eq:
apply (rule iffI[rotated, OF vs_lookup_pages_vs_lookupI], assumption)
apply (simp add: valid_cap_def)
apply (erule vs_lookup_vs_lookup_pagesI', clarsimp+)
done
sorry
lemma nat_to_cref_unat_of_bl':
"\<lbrakk> length xs < 32; n = length xs \<rbrakk> \<Longrightarrow>
"\<lbrakk> length xs < word_bits; n = length xs \<rbrakk> \<Longrightarrow>
nat_to_cref n (unat (of_bl xs :: machine_word)) = xs"
apply (simp add: nat_to_cref_def word_bits_def)
apply (rule nth_equalityI)
@ -72,11 +74,13 @@ lemma nat_to_cref_unat_of_bl':
lemmas nat_to_cref_unat_of_bl = nat_to_cref_unat_of_bl' [OF _ refl]
lemma invs_arm_asid_table_unmap:
(* FIXME x64: this needs reevaluation - do we need the "asid_map" premise?
note delete_asid_pool for arm and x64 differ a lot *)
lemma invs_x64_asid_table_unmap:
"invs s \<and> is_aligned base asid_low_bits \<and> base \<le> mask asid_bits
\<and> (\<forall>x\<in>set [0.e.2 ^ asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None)
\<and> tab = arm_asid_table (arch_state s)
\<longrightarrow> invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)"
\<and> (\<forall>x\<in>set [0.e.2 ^ asid_low_bits - 1]. x64_asid_map (arch_state s) (base + x) = None)
\<and> tab = x64_asid_table (arch_state s)
\<longrightarrow> invs (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)"
apply (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)
apply (strengthen valid_asid_map_unmap valid_arch_objs_unmap_strg
valid_vs_lookup_unmap_strg valid_arch_state_unmap_strg)
@ -90,33 +94,25 @@ lemma delete_asid_pool_invs[wp]:
delete_asid_pool base pptr
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: delete_asid_pool_def)
apply wp
apply (strengthen invs_arm_asid_table_unmap)
apply simp
apply (rule hoare_vcg_conj_lift,
(rule mapM_invalidate[where ptr=pptr])?,
((wp mapM_wp' | simp add: if_apply_def2)+)[1])+
apply wp
apply (clarsimp simp: is_aligned_mask[symmetric])
apply (rule conjI)
apply (rule vs_lookupI)
apply (erule vs_asid_refsI)
apply simp
apply_trace wp
apply (clarsimp simp: if_apply_def2 invs_x64_asid_table_unmap[rule_format])
thm invs_x64_asid_table_unmap[rule_format, simplified]
apply (rule invs_x64_asid_table_unmap[rule_format])
apply clarsimp
done
sorry
lemma delete_asid_invs[wp]:
"\<lbrace>invs and K (asid \<le> mask asid_bits)\<rbrace>
delete_asid asid pd
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: delete_asid_def cong: option.case_cong)
apply (wp set_asid_pool_invs_unmap | wpc)+
apply (simp add: invalidate_asid_entry_def invalidate_asid_def invalidate_hw_asid_entry_def)
apply_trace (wp set_asid_pool_invs_unmap hoare_vcg_all_lift dmo_wp | wpc | simp | wp_once )+
apply (simp add:)
apply (wp load_hw_asid_wp)
apply (simp add: flush_space_def)
apply (wp load_hw_asid_wp|wpc)+
apply (clarsimp simp del: fun_upd_apply)
apply (subgoal_tac "valid_asid_table (arm_asid_table (arch_state s)) s")
apply (subgoal_tac "valid_asid_table (x64_asid_table (arch_state s)) s")
prefer 2
apply fastforce
apply (clarsimp simp: valid_asid_table_def)
@ -433,7 +429,7 @@ lemma arch_finalise_cap_replaceable[wp]:
"\<lbrace>\<lambda>s. s \<turnstile> cap.ArchObjectCap cap \<and>
x = is_final_cap' (cap.ArchObjectCap cap) s \<and>
pspace_aligned s \<and> valid_arch_objs s \<and> valid_objs s \<and>
valid_asid_table (arm_asid_table (arch_state s)) s\<rbrace>
valid_asid_table (x64_asid_table (arch_state s)) s\<rbrace>
arch_finalise_cap cap x
\<lbrace>\<lambda>rv s. replaceable s sl rv (cap.ArchObjectCap cap)\<rbrace>"
apply (simp add: arch_finalise_cap_def)
@ -589,7 +585,7 @@ context Arch begin global_naming X64
lemma fast_finalise_replaceable[wp]:
"\<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s
\<and> cte_wp_at (op = cap) sl s \<and> valid_asid_table (arm_asid_table (arch_state s)) s
\<and> cte_wp_at (op = cap) sl s \<and> valid_asid_table (x64_asid_table (arch_state s)) s
\<and> valid_mdb s \<and> valid_objs s \<and> sym_refs (state_refs_of s)\<rbrace>
fast_finalise cap x
\<lbrace>\<lambda>rv s. cte_wp_at (replaceable s sl cap.NullCap) sl s\<rbrace>"
@ -1200,7 +1196,7 @@ lemma replaceable_reset_pd_strg:
lemma arch_finalise_case_no_lookup:
"\<lbrace>pspace_aligned and valid_arch_objs and valid_objs and
valid_cap (cap.ArchObjectCap acap) and (\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s)
valid_cap (cap.ArchObjectCap acap) and (\<lambda>s. valid_asid_table (x64_asid_table (arch_state s)) s)
and K (aobj_ref acap = Some w \<and> is_final)\<rbrace>
arch_finalise_cap acap is_final
\<lbrace>\<lambda>rv s. (\<forall>vs. vs_cap_ref (cap.ArchObjectCap acap) = Some vs \<longrightarrow> \<not> (vs \<unrhd> w) s)\<rbrace>"
@ -1274,7 +1270,7 @@ crunch valid_cap: invalidate_tlb_by_asid "valid_cap cap"
crunch inv: page_table_mapped "P"
crunch valid_objs[wp]: invalidate_tlb_by_asid "valid_objs"
crunch valid_asid_table[wp]: do_machine_op
"\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s"
"\<lambda>s. valid_asid_table (x64_asid_table (arch_state s)) s"
lemma mapM_x_swp_store_invalid_pte_invs:
"\<lbrace>invs and (\<lambda>s. \<exists>slot. cte_wp_at
@ -1639,8 +1635,8 @@ lemma set_asid_pool_obj_at_ptr:
lemma valid_arch_state_table_strg:
"valid_arch_state s \<and> asid_pool_at p s \<and>
Some p \<notin> arm_asid_table (arch_state s) ` (dom (arm_asid_table (arch_state s)) - {x}) \<longrightarrow>
valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>)"
Some p \<notin> x64_asid_table (arch_state s) ` (dom (x64_asid_table (arch_state s)) - {x}) \<longrightarrow>
valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>)"
apply (clarsimp simp: valid_arch_state_def valid_asid_table_def ran_def)
apply (rule conjI, fastforce)
apply (erule inj_on_fun_upd_strongerI)
@ -1648,15 +1644,15 @@ lemma valid_arch_state_table_strg:
done
lemma valid_table_caps_table [simp]:
"valid_table_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table'\<rparr>\<rparr>) = valid_table_caps s"
"valid_table_caps (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table'\<rparr>\<rparr>) = valid_table_caps s"
by (simp add: valid_table_caps_def)
lemma valid_global_objs_table [simp]:
"valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table'\<rparr>\<rparr>) = valid_global_objs s"
"valid_global_objs (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table'\<rparr>\<rparr>) = valid_global_objs s"
by (simp add: valid_global_objs_def)
lemma valid_kernel_mappings [iff]:
"valid_kernel_mappings (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table'\<rparr>\<rparr>) = valid_kernel_mappings s"
"valid_kernel_mappings (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table'\<rparr>\<rparr>) = valid_kernel_mappings s"
by (simp add: valid_kernel_mappings_def)
lemma vs_asid_refs_updateD:
@ -1674,7 +1670,7 @@ lemma vs_lookup1_arch [simp]:
lemma vs_lookup_empty_table:
"(rs \<rhd> q)
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool empty)),
arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
(rs \<rhd> q) s \<or> (rs = [VSRef (ucast x) None] \<and> q = p)"
apply (erule vs_lookupE)
apply clarsimp
@ -1707,7 +1703,7 @@ lemma vs_lookup_empty_table:
lemma vs_lookup_pages_empty_table:
"(rs \<unrhd> q)
(s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (ASIDPool empty)),
arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
arch_state := arch_state s\<lparr>x64_asid_table := x64_asid_table (arch_state s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
(rs \<unrhd> q) s \<or> (rs = [VSRef (ucast x) None] \<and> q = p)"
apply (subst (asm) vs_lookup_pages_def)
apply (clarsimp simp: Image_def)
@ -1741,8 +1737,8 @@ lemma set_asid_pool_empty_table_objs:
"\<lbrace>valid_arch_objs and asid_pool_at p\<rbrace>
set_asid_pool p empty
\<lbrace>\<lambda>rv s. valid_arch_objs
(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of word2 \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
(s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of word2 \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def valid_arch_objs_def
@ -1766,8 +1762,8 @@ lemma set_asid_pool_empty_table_lookup:
(\<lambda>s. \<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))\<rbrace>
set_asid_pool p empty
\<lbrace>\<lambda>rv s. valid_vs_lookup
(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
(s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def valid_vs_lookup_def
@ -1788,8 +1784,8 @@ lemma set_asid_pool_empty_valid_asid_map:
\<and> (\<forall>asid'. \<not> ([VSRef asid' None] \<rhd> p) s)
\<and> (\<forall>p'. \<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p') s)\<rbrace>
set_asid_pool p empty
\<lbrace>\<lambda>rv s. valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
\<lbrace>\<lambda>rv s. valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: valid_asid_map_def vspace_at_asid_def
@ -1820,8 +1816,8 @@ lemma set_asid_pool_invs_table:
\<and> (\<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p) s)
\<and> (\<forall>p'. \<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p') s)\<rbrace>
set_asid_pool p empty
\<lbrace>\<lambda>x s. invs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table :=
arm_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
\<lbrace>\<lambda>x s. invs (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def)
apply (rule hoare_pre)
apply (wp valid_irq_node_typ set_asid_pool_typ_at
@ -1857,7 +1853,7 @@ lemma delete_asid_pool_unmapped2:
apply (wp delete_asid_pool_unmapped)
apply (simp add: delete_asid_pool_def)
apply wp
apply (rule_tac Q="\<lambda>rv s. ?Q s \<and> asid_table = arm_asid_table (arch_state s)"
apply (rule_tac Q="\<lambda>rv s. ?Q s \<and> asid_table = x64_asid_table (arch_state s)"
in hoare_post_imp)
apply (clarsimp simp: fun_upd_def[symmetric])
apply (drule vs_lookup_clear_asid_table[rule_format])

7
proof/invariant-abstract/X64/ArchInterrupt_AI.thy
View File

@ -19,8 +19,9 @@ named_theorems Interrupt_AI_asms
lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_asms]:
"\<lbrace>P\<rbrace> decode_irq_control_invocation label args slot caps \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: decode_irq_control_invocation_def Let_def arch_check_irq_def
arch_decode_irq_control_invocation_def whenE_def, safe)
apply (wp | simp)+
arch_decode_irq_control_invocation_def whenE_def split del: split_if)
apply (rule hoare_pre)
apply (wp | simp split del: split_if)+
done
lemma (* decode_irq_control_valid *)[Interrupt_AI_asms]:
@ -78,6 +79,8 @@ lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_asms]:
by (rule ext, simp add: no_cap_to_obj_with_diff_ref_def
cte_wp_at_caps_of_state
obj_ref_none_no_asid)
crunch valid_cap: do_machine_op "valid_cap cap"
lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]:
"\<lbrace>valid_cap cap\<rbrace> set_irq_state IRQSignal irq \<lbrace>\<lambda>rv. valid_cap cap\<rbrace>"

2
proof/invariant-abstract/X64/ArchInvariants_AI.thy
View File

@ -498,6 +498,8 @@ definition
where
"vs_lookup \<equiv> \<lambda>s. vs_lookup_trans s `` vs_asid_refs (x64_asid_table (arch_state s))"
definition "second_level_tables \<equiv> arch_state.x64_global_pdpts"
end
context begin interpretation Arch .

80
proof/invariant-abstract/X64/ArchIpc_AI.thy
View File

@ -20,35 +20,42 @@ lemma update_cap_data_closedform:
"update_cap_data pres w cap =
(case cap of
EndpointCap r badge rights \<Rightarrow>
if badge = 0 \<and> \<not> pres then (EndpointCap r (w && mask 28) rights) else NullCap
if badge = 0 \<and> \<not> pres then (EndpointCap r (w && mask badge_bits) rights) else NullCap
| NotificationCap r badge rights \<Rightarrow>
if badge = 0 \<and> \<not> pres then (NotificationCap r (w && mask 28) rights) else NullCap
if badge = 0 \<and> \<not> pres then (NotificationCap r (w && mask badge_bits) rights) else NullCap
| CNodeCap r bits guard \<Rightarrow>
if word_bits < unat ((w >> 3) && mask 5) + bits
if word_bits < unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits) + bits
then NullCap
else CNodeCap r bits ((\<lambda>g''. drop (size g'' - unat ((w >> 3) && mask 5)) (to_bl g'')) ((w >> 8) && mask 18))
else CNodeCap r bits ((\<lambda>g''. drop (size g'' - unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits)) (to_bl g'')) ((w >> 8) && mask 18))
| ThreadCap r \<Rightarrow> ThreadCap r
| DomainCap \<Rightarrow> DomainCap
| UntypedCap p n idx \<Rightarrow> UntypedCap p n idx
| UntypedCap d p n idx \<Rightarrow> UntypedCap d p n idx
| NullCap \<Rightarrow> NullCap
| ReplyCap t m \<Rightarrow> ReplyCap t m
| IRQControlCap \<Rightarrow> IRQControlCap
| IRQHandlerCap irq \<Rightarrow> IRQHandlerCap irq
| Zombie r b n \<Rightarrow> Zombie r b n
| ArchObjectCap cap \<Rightarrow> ArchObjectCap cap)"
| ArchObjectCap cap \<Rightarrow>
let fst = ucast w;
lst = ucast (w >> 16)
in case cap of IOPortCap old_fst old_lst \<Rightarrow>
if (fst \<le> lst \<and> fst \<ge> old_fst \<and> lst \<le> old_lst)
then ArchObjectCap (IOPortCap fst lst)
else NullCap
| _ \<Rightarrow> ArchObjectCap cap)"
apply (cases cap,
simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True
is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size
cap_ep_badge.simps badge_update_def o_def cap_rights_update_def
simp_thms cap_rights.simps Let_def split_def
the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def
arch_update_cap_data_def
arch_update_cap_data_def cnode_padding_bits_def cnode_guard_size_bits_def
cong: if_cong)
apply auto
apply (auto simp: cnode_padding_bits_def cnode_guard_size_bits_def)
done
lemma cap_asid_PageCap_None [simp]:
"cap_asid (ArchObjectCap (PageCap r R pgsz None)) = None"
"cap_asid (ArchObjectCap (PageCap d r R typ pgsz None)) = None"
by (simp add: cap_asid_def)
lemma arch_derive_cap_is_derived:
@ -190,7 +197,7 @@ lemma obj_refs_remove_rights[simp, Ipc_AI_assms]:
lemma storeWord_um_inv:
"\<lbrace>\<lambda>s. underlying_memory s = um\<rbrace>
storeWord a v
\<lbrace>\<lambda>_ s. is_aligned a 2 \<and> x \<in> {a,a+1,a+2,a+3} \<or> underlying_memory s x = um x\<rbrace>"
\<lbrace>\<lambda>_ s. is_aligned a 3 \<and> x \<in> {a,a+1,a+2,a+3,a+4,a+5,a+6,a+7} \<or> underlying_memory s x = um x\<rbrace>"
apply (simp add: storeWord_def is_aligned_mask)
apply wp
apply simp
@ -200,17 +207,17 @@ lemma store_word_offs_vms[wp, Ipc_AI_assms]:
"\<lbrace>valid_machine_state\<rbrace> store_word_offs ptr offs v \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
proof -
have aligned_offset_ignore:
"\<And>(l::word32) (p::word32) sz. l<4 \<Longrightarrow> p && mask 2 = 0 \<Longrightarrow>
"\<And>(l::machine_word) (p::machine_word) sz. l<word_size \<Longrightarrow> p && mask word_size_bits = 0 \<Longrightarrow>
p+l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)"
proof -
fix l p sz
assume al: "(p::word32) && mask 2 = 0"
assume "(l::word32) < 4" hence less: "l<2^2" by simp
have le: "2 \<le> pageBitsForSize sz" by (case_tac sz, simp_all)
assume al: "(p::machine_word) && mask word_size_bits = 0"
assume "(l::machine_word) < word_size" hence less: "l<2^word_size_bits" by (simp add: word_size_bits_def word_size_def)
have le: "word_size_bits \<le> pageBitsForSize sz" by (case_tac sz, simp_all add: bit_simps)
show "?thesis l p sz"
by (rule is_aligned_add_helper[simplified is_aligned_mask,
THEN conjunct2, THEN mask_out_first_mask_some,
where n=2, OF al less le])
where n=word_size_bits, OF al less le])
qed
show ?thesis
@ -227,23 +234,23 @@ proof -
apply (erule disjE, simp)
apply (simp add: in_user_frame_def word_size_def)
apply (erule exEI)
apply (subgoal_tac "(ptr + of_nat offs * 4) && ~~ mask (pageBitsForSize x) =
p && ~~ mask (pageBitsForSize x)", simp)
apply (simp only: is_aligned_mask[of _ 2])
apply (elim disjE, simp_all)
apply (rule aligned_offset_ignore[symmetric], simp+)+
apply (subgoal_tac "(ptr + of_nat offs * word_size) && ~~ mask (pageBitsForSize x) =
p && ~~ mask (pageBitsForSize x)", simp add: word_size_def)
apply (simp only: is_aligned_mask[of _ word_size_bits, simplified word_size_bits_def])
apply (elim disjE, simp_all add: word_size_def)
apply (rule aligned_offset_ignore[symmetric, simplified word_size_bits_def word_size_def], simp+)+
done
qed
lemma is_zombie_update_cap_data[simp, Ipc_AI_assms]:
"is_zombie (update_cap_data P data cap) = is_zombie cap"
by (simp add: update_cap_data_closedform is_zombie_def
split: cap.splits)
by (clarsimp simp: update_cap_data_closedform is_zombie_def Let_def
split: cap.splits arch_cap.splits)
lemma valid_msg_length_strengthen [Ipc_AI_assms]:
"valid_message_info mi \<longrightarrow> unat (mi_length mi) \<le> msg_max_length"
apply (clarsimp simp: valid_message_info_def)
apply (subgoal_tac "unat (mi_length mi) \<le> unat (of_nat msg_max_length :: word32)")
apply (subgoal_tac "unat (mi_length mi) \<le> unat (of_nat msg_max_length :: machine_word)")
apply (clarsimp simp: unat_of_nat msg_max_length_def)
apply (clarsimp simp: un_ui_le word_le_def)
done
@ -271,18 +278,22 @@ lemma lookup_ipc_buffer_in_user_frame[wp, Ipc_AI_assms]:
\<lbrace>case_option (\<lambda>_. True) in_user_frame\<rbrace>"
apply (simp add: lookup_ipc_buffer_def)
apply (wp get_cap_wp thread_get_wp | wpc | simp)+
apply (clarsimp simp add: obj_at_def is_tcb)
apply (subgoal_tac "in_user_frame (xa + (tcb_ipc_buffer tcb &&
mask (pageBitsForSize xc))) s", simp)
apply (drule (1) cte_wp_valid_cap)
apply (clarsimp simp add: obj_at_def is_tcb split: split_if_asm)
apply (rename_tac dev p R tp sz m)
apply (subgoal_tac "in_user_frame (p + (tcb_ipc_buffer tcb &&
mask (pageBitsForSize sz))) s", simp)
apply (frule (1) cte_wp_valid_cap)
apply (clarsimp simp add: valid_cap_def cap_aligned_def in_user_frame_def)
apply (thin_tac "case_option a b c" for a b c)
apply (rule_tac x=xc in exI)
apply (subgoal_tac "(xa + (tcb_ipc_buffer tcb && mask (pageBitsForSize xc)) &&
~~ mask (pageBitsForSize xc)) = xa", simp)
apply (rule is_aligned_add_helper[THEN conjunct2], assumption)
apply (rule and_mask_less')
apply (case_tac xc, simp_all)
apply (rule_tac x=sz in exI)
apply (subst is_aligned_add_helper[THEN conjunct2])
apply simp
apply (simp add: and_mask_less' word_bits_def)
apply (clarsimp simp: caps_of_state_cteD'[where P="\<lambda>x. True", simplified, symmetric])
apply (drule (1) CSpace_AI.tcb_cap_slot_regular)
apply simp
apply (simp add: is_nondevice_page_cap_def case_bool_If
split: if_splits)
done
lemma transfer_caps_loop_cte_wp_at:
@ -302,13 +313,12 @@ lemma transfer_caps_loop_cte_wp_at:
| assumption | simp split del: split_if)+
apply (wp hoare_vcg_conj_lift cap_insert_weak_cte_wp_at2)
apply (erule imp)
apply (wp hoare_vcg_ball_lift
by (wp hoare_vcg_ball_lift
| clarsimp simp: is_cap_simps split del:split_if
| unfold derive_cap_def arch_derive_cap_def
| wpc
| rule conjI
| case_tac slots)+
done
lemma transfer_caps_tcb_caps:
fixes P t ref mi caps ep receiver recv_buf

6
proof/invariant-abstract/X64/ArchRetype_AI.thy
View File

@ -583,7 +583,7 @@ requalify_consts post_retype_invs_check
end
definition
post_retype_invs :: "apiobject_type \<Rightarrow> word32 list \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
post_retype_invs :: "apiobject_type \<Rightarrow> machine_word list \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"post_retype_invs tp refs \<equiv>
if post_retype_invs_check tp
@ -952,10 +952,10 @@ lemma unique_table_refs_null:
definition
region_in_kernel_window :: "word32 set \<Rightarrow> 'z state \<Rightarrow> bool"
region_in_kernel_window :: "machine_word set \<Rightarrow> 'z state \<Rightarrow> bool"
where
"region_in_kernel_window S \<equiv>
\<lambda>s. \<forall>x \<in> S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow"
\<lambda>s. \<forall>x \<in> S. x64_kernel_vspace (arch_state s) x = X64VSpaceKernelWindow"
end

64
proof/invariant-abstract/X64/ArchTcb_AI.thy
View File

@ -57,23 +57,27 @@ where
is_cnode_cap cap
\<or> (is_arch_cap cap
\<and> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None))"
\<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pdpt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pml4_cap cap \<longrightarrow> cap_asid cap \<noteq> None))"
definition (* arch specific *)
"pt_pd_asid cap \<equiv> case cap of
"vspace_asid cap \<equiv> case cap of
ArchObjectCap (PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
| ArchObjectCap (PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid
| ArchObjectCap (PageDirectoryCap _ (Some (asid, _))) \<Rightarrow> Some asid
| ArchObjectCap (PDPointerTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
| ArchObjectCap (PML4Cap _ (Some asid)) \<Rightarrow> Some asid
| _ \<Rightarrow> None"
lemmas pt_pd_asid_simps [simp] = (* arch specific *)
pt_pd_asid_def [split_simps cap.split arch_cap.split option.split prod.split]
lemmas vspace_asid_simps [simp] = (* arch specific *)
vspace_asid_def [split_simps cap.split arch_cap.split option.split prod.split]
lemma checked_insert_is_derived: (* arch specific *)
"\<lbrakk> same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap;
obj_refs new_cap = obj_refs old_cap
\<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap
\<and> pt_pd_asid old_cap = pt_pd_asid new_cap\<rbrakk>
\<and> vspace_asid old_cap = vspace_asid new_cap\<rbrakk>
\<Longrightarrow> is_derived m slot new_cap old_cap"
apply (cases slot)
apply (frule same_object_as_cap_master)
@ -82,17 +86,18 @@ lemma checked_insert_is_derived: (* arch specific *)
apply (frule same_master_cap_same_types)
apply (simp add: is_derived_def)
apply clarsimp
apply (auto simp: is_cap_simps cap_master_cap_def
by (auto simp: is_cap_simps cap_master_cap_def
is_cnode_or_valid_arch_def vs_cap_ref_def
table_cap_ref_def pt_pd_asid_def up_ucast_inj_eq
table_cap_ref_def vspace_asid_def up_ucast_inj_eq
split: cap.split_asm arch_cap.split_asm
option.split_asm)[1]
done
lemma is_cnode_or_valid_arch_cap_asid: (* arch specific *)
"is_cnode_or_valid_arch cap
\<Longrightarrow> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None)"
\<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pdpt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pml4_cap cap \<longrightarrow> cap_asid cap \<noteq> None)"
by (auto simp add: is_cnode_or_valid_arch_def
is_cap_simps)
@ -100,11 +105,11 @@ lemma checked_insert_tcb_invs[wp]: (* arch specific *)
"\<lbrace>invs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref)
and K (is_cnode_or_valid_arch new_cap) and valid_cap new_cap
and tcb_cap_valid new_cap (target, ref)
and K (is_pt_cap new_cap \<or> is_pd_cap new_cap
and K (is_pt_cap new_cap \<or> is_pd_cap new_cap \<or> is_pdpt_cap new_cap \<or> is_pml4_cap new_cap
\<longrightarrow> cap_asid new_cap \<noteq> None)
and (cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap
\<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and>
pt_pd_asid c = pt_pd_asid new_cap) src_slot)\<rbrace>
vspace_asid c = vspace_asid new_cap) src_slot)\<rbrace>
check_cap_at new_cap src_slot
(check_cap_at (cap.ThreadCap target) slot
(cap_insert new_cap src_slot (target, ref))) \<lbrace>\<lambda>rv. invs\<rbrace>"
@ -170,15 +175,15 @@ by (unfold_locales; fact Tcb_AI_asms)
lemma use_no_cap_to_obj_asid_strg: (* arch specific *)
"(cte_at p s \<and> no_cap_to_obj_dr_emp cap s \<and> valid_cap cap s \<and> invs s)
\<longrightarrow> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap
\<longrightarrow> table_cap_ref c = table_cap_ref cap \<and> pt_pd_asid c = pt_pd_asid cap) p s"
\<longrightarrow> table_cap_ref c = table_cap_ref cap \<and> vspace_asid c = vspace_asid cap) p s"
apply (clarsimp simp: cte_wp_at_caps_of_state
no_cap_to_obj_with_diff_ref_def
simp del: split_paired_All)
apply (frule caps_of_state_valid_cap, fastforce)
apply (erule allE)+
apply (erule (1) impE)+
apply (simp add: table_cap_ref_def pt_pd_asid_def split: cap.splits arch_cap.splits option.splits prod.splits)
apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+
apply (simp add: table_cap_ref_def vspace_asid_def split: cap.splits arch_cap.splits option.splits prod.splits)
apply (fastforce simp: table_cap_ref_def valid_cap_simps wellformed_mapdata_def elim!: asid_low_high_bits)+
done
lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
@ -195,7 +200,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
| rule obj_ref_none_no_asid)+
done
lemma tc_invs[Tcb_AI_asms]:
"\<lbrace>invs and tcb_at a
and (case_option \<top> (valid_cap o fst) e)
@ -207,6 +211,10 @@ lemma tc_invs[Tcb_AI_asms]:
and (case_option \<top> (no_cap_to_obj_dr_emp o fst) e)
and (case_option \<top> (no_cap_to_obj_dr_emp o fst) f)
and (case_option \<top> (case_option \<top> (no_cap_to_obj_dr_emp o fst) o snd) g)
(* only set prio \<le> mcp *)
and (\<lambda>s. case_option True (\<lambda>pr. mcpriority_tcb_at (\<lambda>mcp. pr \<le> mcp) (cur_thread s) s) pr)
(* only set mcp \<le> prev_mcp *)
and (\<lambda>s. case_option True (\<lambda>mcp. mcpriority_tcb_at (\<lambda>m. mcp \<le> m) (cur_thread s) s) mcp)
and K (case_option True (is_cnode_cap o fst) e)
and K (case_option True (is_valid_vtable_root o fst) f)
and K (case_option True (\<lambda>v. case_option True
@ -214,10 +222,10 @@ lemma tc_invs[Tcb_AI_asms]:
and is_arch_cap and is_cnode_or_valid_arch)
o fst) (snd v)) g)
and K (case_option True (\<lambda>bl. length bl = word_bits) b)\<rbrace>
invoke_tcb (ThreadControl a sl b pr e f g)
invoke_tcb (ThreadControl a sl b mcp pr e f g)
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (rule hoare_gen_asm)+
apply (simp add: split_def cong: option.case_cong)
apply (simp add: split_def set_mcpriority_def cong: option.case_cong)
apply (rule hoare_vcg_precond_imp)
apply wp
apply ((simp only: simp_thms
@ -250,12 +258,14 @@ lemma tc_invs[Tcb_AI_asms]:
| strengthen use_no_cap_to_obj_asid_strg
tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"]
tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"])+)
apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified]
is_cap_simps is_valid_vtable_root_def
apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] is_nondevice_page_cap_arch_def
is_cap_simps is_valid_vtable_root_def is_nondevice_page_cap_simps
is_cnode_or_valid_arch_def tcb_cap_valid_def
invs_valid_objs cap_asid_def vs_cap_ref_def
split: option.split_asm
| rule conjI)+
split: option.split_asm )+
apply (simp add: case_bool_If valid_ipc_buffer_cap_def is_nondevice_page_cap_simps
is_nondevice_page_cap_arch_def
split: arch_cap.splits if_splits)+
done
@ -265,7 +275,7 @@ lemma check_valid_ipc_buffer_inv: (* arch_specific *)
cong: cap.case_cong arch_cap.case_cong
split del: split_if)
apply (rule hoare_pre)
apply (wp | simp split del: split_if | wpcw)+
apply (wp | simp add: whenE_def split del: split_if | wpcw)+
done
lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]:
@ -279,7 +289,7 @@ lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]:
cong: cap.case_cong arch_cap.case_cong
split del: split_if)
apply (rule hoare_pre)
apply (wp | simp split del: split_if | wpc)+
apply (wp | simp add: whenE_def split del: split_if | wpc)+
apply (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def
valid_ipc_buffer_cap_def)
done
@ -317,9 +327,9 @@ lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]:
apply (simp add: no_cap_to_obj_with_diff_ref_def
update_cap_objrefs)
apply (clarsimp simp: update_cap_data_closedform
table_cap_ref_def
table_cap_ref_def Let_def
arch_update_cap_data_def
split: cap.split)
split: cap.split arch_cap.splits)
apply simp
done
@ -342,7 +352,7 @@ lemma update_cap_valid[Tcb_AI_asms]:
apply (simp add: word_bits_def)
apply (rename_tac arch_cap)
using valid_validate_vm_rights[simplified valid_vm_rights_def]
apply (case_tac arch_cap, simp_all add: acap_rights_update_def
apply (case_tac arch_cap, simp_all add: acap_rights_update_def Let_def
split: option.splits prod.splits)
done

55
proof/invariant-abstract/X64/Machine_AI.thy
View File

@ -367,6 +367,61 @@ lemma empty_fail_clearMemory [simp, intro!]:
"\<And>a b. empty_fail (clearMemory a b)"
by (simp add: clearMemory_def mapM_x_mapM ef_storeWord)
(* FIXME x64: move *)
lemma setCurrentVSpaceRoot_ef[simp,wp]: "empty_fail (setCurrentVSpaceRoot a b)"
by (simp add: setCurrentVSpaceRoot_def)
lemma getFaultAddress_ef[simp,wp]: "empty_fail getFaultAddress"
by (simp add: getFaultAddress_def)
(* FIXME x64: move *)
lemma ioapicMapPinToVector_ef[simp,wp]: "empty_fail (ioapicMapPinToVector a b c d e)"
by (simp add: ioapicMapPinToVector_def)
(* FIXME x64: move *)
lemma invalidateTLBEntry_ef[simp,wp]: "empty_fail (invalidateTLBEntry b)"
by (simp add: invalidateTLBEntry_def)
(* FIXME x64: move *)
lemma hwASIDInvalidate_ef[simp,wp]: "empty_fail (hwASIDInvalidate b)"
by (simp add: hwASIDInvalidate_def)
(* FIXME x64: move *)
lemma updateIRQState_ef[simp,wp]: "empty_fail (updateIRQState b c)"
by (simp add: updateIRQState_def)
(* FIXME x64: move *)
lemma invalidatePageStructureCache_ef[simp,wp]: "empty_fail (invalidatePageStructureCache)"
by (simp add: invalidatePageStructureCache_def)
(* FIXME x64: move *)
lemma resetCR3_ef[simp,wp]: "empty_fail (resetCR3)"
by (simp add: resetCR3_def)
(* FIXME x64: move *)
lemma in8_ef[simp,wp]: "empty_fail (in8 port)"
by (simp add: in8_def)
(* FIXME x64: move *)
lemma in16_ef[simp,wp]: "empty_fail (in16 port)"
by (simp add: in16_def)
(* FIXME x64: move *)
lemma in32_ef[simp,wp]: "empty_fail (in32 port)"
by (simp add: in32_def)
(* FIXME x64: move *)
lemma out8_ef[simp,wp]: "empty_fail (out8 port dat)"
by (simp add: out8_def)
(* FIXME x64: move *)
lemma out16_ef[simp,wp]: "empty_fail (out16 port dat)"
by (simp add: out16_def)
(* FIXME x64: move *)
lemma out32_ef[simp,wp]: "empty_fail (out32 port dat)"
by (simp add: out32_def)
end
end

14
spec/abstract/ARM/ArchCSpace_A.thy
View File

@ -21,16 +21,22 @@ begin
context Arch begin global_naming ARM_A
definition cnode_guard_size_bits :: "nat"
where
"cnode_guard_size_bits \<equiv> 5"
definition cnode_padding_bits :: "nat"
where
"cnode_padding_bits \<equiv> 3"
text {* On a user request to modify a cnode capability, extract new guard bits and guard. *}
definition
update_cnode_cap_data :: "data \<Rightarrow> nat \<times> data" where
"update_cnode_cap_data w \<equiv>
let
pad_bits = 3;
guard_bits = 18;
guard_size_bits = 5;
guard_size' = unat ((w >> pad_bits) && mask guard_size_bits);
guard'' = (w >> (pad_bits + guard_size_bits)) && mask guard_bits
guard_size' = unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits);
guard'' = (w >> (cnode_padding_bits + cnode_guard_size_bits)) && mask guard_bits
in (guard_size', guard'')"
text {* For some purposes capabilities to physical objects are treated

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

@ -260,6 +260,11 @@ where
| DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz
| ASIDPool f \<Rightarrow> AASIDPool)"
text {* For implementation reasons the badge word has differing amounts of bits *}
definition
badge_bits :: nat where
"badge_bits \<equiv> 28"
end
section "Arch-specific tcb"

2
spec/abstract/CSpace_A.thy
View File

@ -37,6 +37,8 @@ requalify_consts
msg_max_extra_caps
msg_align_bits
update_cnode_cap_data
cnode_padding_bits
cnode_guard_size_bits
end

8
spec/abstract/Structures_A.thy
View File

@ -41,6 +41,7 @@ requalify_consts
asid_high_bits
asid_low_bits
arch_is_frame_type
badge_bits
default_arch_tcb
arch_tcb_context_get
arch_tcb_context_set
@ -227,13 +228,6 @@ definition
| ArchObjectCap acap \<Rightarrow> ArchObjectCap (acap_rights_update cr' acap)
| _ \<Rightarrow> cap"
text {* For implementation reasons not all bits of the badge word can be used. *}
definition
badge_bits :: nat where
"badge_bits \<equiv> 28"
declare badge_bits_def [simp]
definition
badge_update :: "badge \<Rightarrow> cap \<Rightarrow> cap" where
"badge_update data cap \<equiv>

14
spec/abstract/X64/ArchCSpace_A.thy
View File

@ -21,16 +21,22 @@ begin
context Arch begin global_naming X64_A
definition cnode_guard_size_bits :: "nat"
where
"cnode_guard_size_bits \<equiv> 6"
definition cnode_padding_bits :: "nat"
where
"cnode_padding_bits \<equiv> 2"
text {* On a user request to modify a cnode capability, extract new guard bits and guard. *}
definition
update_cnode_cap_data :: "data \<Rightarrow> nat \<times> data" where
"update_cnode_cap_data w \<equiv>
let
pad_bits = 2;
guard_bits = 18;
guard_size_bits = 6;
guard_size' = unat ((w >> pad_bits) && mask guard_size_bits);
guard'' = (w >> (pad_bits + guard_size_bits)) && mask guard_bits
guard_size' = unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits);
guard'' = (w >> (cnode_padding_bits + cnode_guard_size_bits)) && mask guard_bits
in (guard_size', guard'')"
text {* For some purposes capabilities to physical objects are treated

16
spec/abstract/X64/ArchDecode_A.thy
View File

@ -171,7 +171,8 @@ where
ensure_port_operation_allowed cap port 1;
output_data \<leftarrow> returnOk $ ucast $ args ! 1;
returnOk $ InvokeIOPort $ IOPortInvocation port $ IOPortOut32 output_data
odE"
odE
| _ \<Rightarrow> throwError IllegalOperation"
(*X64STUB*)
definition
decode_io_unmap_invocation :: "data \<Rightarrow> data list \<Rightarrow> cslot_ptr \<Rightarrow> arch_cap \<Rightarrow>
@ -350,9 +351,9 @@ where
odE
else throwError TruncatedMessage
else if invocation_type label = ArchInvocationLabel X64PageUnmap then
case map_type of
(*case map_type of
VMIOSpaceMap \<Rightarrow> decode_io_unmap_invocation label args cte cap extra_caps
| _ \<Rightarrow> returnOk $ InvokePage $ PageUnmap cap cte
| _ \<Rightarrow>*) returnOk $ InvokePage $ PageUnmap cap cte
(* FIXME x64-vtd:
else if invocation_type label = ArchInvocationLabel X64PageMapIO
then decode_io_map_invocation label args cte cap extra_caps
@ -360,7 +361,7 @@ where
else if invocation_type label = ArchInvocationLabel X64PageGetAddress
then returnOk $ InvokePage $ PageGetAddr p
else throwError IllegalOperation
| _ \<Rightarrow> undefined)"
| _ \<Rightarrow> fail)"
definition filter_frame_attrs :: "frame_attrs \<Rightarrow> table_attrs"
where
@ -475,7 +476,7 @@ where
else throwError IllegalOperation
| ASIDControlCap \<Rightarrow>
if invocation_type label = ArchInvocationLabel X64ASIDPoolAssign then
if invocation_type label = ArchInvocationLabel X64ASIDControlMakePool then
if length args > 1 \<and> length extra_caps > 1
then let index = args ! 0;
depth = args ! 1;
@ -497,7 +498,7 @@ where
else throwError $ InvalidCapability 1);
dest_slot \<leftarrow> lookup_target_slot root (to_bl index) (unat depth);
ensure_empty dest_slot;
returnOk $ InvokeASIDControl $ MakePool undefined undefined parent_slot base
returnOk $ InvokeASIDControl $ MakePool frame dest_slot parent_slot base
odE
else throwError TruncatedMessage
else throwError IllegalOperation
@ -517,8 +518,9 @@ where
(- dom pool \<inter> {x. x \<le> 2 ^ asid_low_bits - 1 \<and> ucast x + base \<noteq> 0});
whenE (free_set = {}) $ throwError DeleteFirst;
offset \<leftarrow> liftE $ select_ext (\<lambda>_. free_asid_pool_select pool base) free_set;
returnOk $ InvokeASIDPool $ Assign undefined undefined pd_cap_slot
returnOk $ InvokeASIDPool $ Assign (ucast offset + base) p pd_cap_slot
odE
| _ \<Rightarrow> throwError $ InvalidCapability 1
else throwError TruncatedMessage
else throwError IllegalOperation

6
spec/abstract/X64/ArchVSpace_A.thy
View File

@ -378,15 +378,15 @@ where
*)
| IOPortCap _ _ \<Rightarrow> returnOk c"
(* FIXME: update when IOSpace comes through *)
(* FIXME: update when IOSpace comes through, first/last ports may be wrong order *)
text {* No user-modifiable data is stored in x64-specific capabilities. *}
definition
arch_update_cap_data :: "data \<Rightarrow> arch_cap \<Rightarrow> cap"
where
"arch_update_cap_data data c \<equiv> case c of
IOPortCap first_port_old last_port_old \<Rightarrow>
let first_port = undefined data; (* ioPortGetFirstPort *)
last_port = undefined data (* ioPortGetLastPort *) in
let first_port = (ucast data ); (* ioPortGetFirstPort *)
last_port = (ucast (data >> 16)) (* ioPortGetLastPort *) in
if (first_port \<le> last_port \<and> first_port \<ge> first_port_old \<and> last_port \<le> last_port_old)
then ArchObjectCap $ IOPortCap first_port last_port
else NullCap

15
spec/abstract/X64/Arch_A.thy
View File

@ -27,14 +27,13 @@ definition
"arch_invoke_irq_control aic \<equiv> (case aic of
IssueIRQHandlerIOAPIC irq dest src ioapic pin level polarity vector \<Rightarrow> without_preemption (do
do_machine_op $ ioapicMapPinToVector ioapic pin level polarity vector;
irq_state \<leftarrow> do_machine_op $ irqStateIRQIOAPICNew ioapic pin level polarity
(1::machine_word) (0::machine_word);
irq_state \<leftarrow> return $ IRQIOAPIC ioapic pin level polarity True;
do_machine_op $ updateIRQState irq irq_state;
set_irq_state IRQSignal (IRQ irq);
cap_insert (IRQHandlerCap (IRQ irq)) dest src
od) |
IssueIRQHandlerMSI irq dest src bus dev func handle \<Rightarrow> without_preemption (do
irq_state \<leftarrow> do_machine_op $ irqStateIRQMSINew bus dev func handle;
irq_state \<leftarrow> return $ IRQMSI bus dev func handle;
do_machine_op $ updateIRQState irq irq_state;
set_irq_state IRQSignal (IRQ irq);
cap_insert (IRQHandlerCap (IRQ irq)) dest src
@ -122,13 +121,6 @@ where
return (pd \<noteq> InvalidPDE)
od"
definition
set_message_info :: "obj_ref \<Rightarrow> message_info \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"set_message_info thread info \<equiv>
as_user thread $ set_register msg_info_register $
message_info_to_data info"
text {* The Page capability confers the authority to map, unmap and flush the
memory page. The remap system call is a convenience operation that ensures the
page is mapped in the same location as this cap was previously used to map it
@ -272,7 +264,8 @@ definition
| InvokePage oper \<Rightarrow> perform_page_invocation oper
| InvokeASIDControl oper \<Rightarrow> perform_asid_control_invocation oper
| InvokeASIDPool oper \<Rightarrow> perform_asid_pool_invocation oper
| InvokeIOPort oper \<Rightarrow> perform_io_port_invocation oper;
| InvokeIOPort oper \<Rightarrow> perform_io_port_invocation oper
| _ \<Rightarrow> fail;
return $ []
od"

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

@ -362,6 +362,11 @@ where
| PDPointerTable pdpt \<Rightarrow> APDPointerTable
| PageMapL4 pm \<Rightarrow> APageMapL4)"
text {* For implementation reasons the badge word has differing amounts of bits *}
definition
badge_bits :: nat where
"badge_bits \<equiv> 64"
end
section "Arch-specific TCB"

91
spec/machine/X64/MachineOps.thy
View File

@ -250,10 +250,12 @@ definition setCurrentCR3 :: "Platform.X64.cr3 \<Rightarrow> unit machine_monad"
where
"setCurrentCR3 \<equiv> undefined"
consts'
mfence_impl :: "unit machine_rest_monad"
definition
mfence :: "unit machine_monad"
where
"mfence \<equiv> undefined"
"mfence \<equiv> machine_op_lift mfence_impl"
consts'
invalidateTLBEntry_impl :: "word64 \<Rightarrow> unit machine_rest_monad"
@ -277,6 +279,7 @@ definition
resetCR3 :: "unit machine_monad" where
"resetCR3 \<equiv> machine_op_lift resetCR3_impl "
(* FIXME x64: VT-d
definition
firstValidIODomain :: "word16"
where
@ -286,36 +289,44 @@ definition
numIODomainIDBits :: "nat"
where
"numIODomainIDBits \<equiv> undefined"
*)
consts'
hwASIDInvalidate_impl :: "word64 \<Rightarrow> unit machine_rest_monad"
definition
hwASIDInvalidate :: "word64 \<Rightarrow> unit machine_monad"
where
"hwASIDInvalidate asid \<equiv> undefined"
"hwASIDInvalidate asid \<equiv> machine_op_lift (hwASIDInvalidate_impl asid)"
consts'
getFaultAddress_val :: "machine_state \<Rightarrow> machine_word"
definition
getFaultAddress :: "word64 machine_monad"
where
"getFaultAddress \<equiv> undefined"
"getFaultAddress \<equiv> gets getFaultAddress_val"
consts'
irqIntOffset_val :: "machine_state \<Rightarrow> machine_word"
definition
irqIntOffset :: "machine_word"
where
"irqIntOffset \<equiv> undefined"
"irqIntOffset \<equiv> 0x20"
definition
maxPCIBus :: "machine_word"
where
"maxPCIBus \<equiv> undefined"
"maxPCIBus \<equiv> 0xFF"
definition
maxPCIDev :: "machine_word"
where
"maxPCIDev \<equiv> undefined"
"maxPCIDev \<equiv> 31"
definition
maxPCIFunc :: "machine_word"
where
"maxPCIFunc \<equiv> undefined"
"maxPCIFunc \<equiv> 7"
definition
numIOAPICs :: "machine_word"
@ -325,26 +336,38 @@ where
definition
ioapicIRQLines :: "machine_word"
where
"ioapicIRQLines \<equiv> undefined"
"ioapicIRQLines \<equiv> error []"
(* FIXME x64: technically this is defined in c and should be here *)
consts'
ioapicMapPinToVector_impl :: "machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_rest_monad"
definition
ioapicMapPinToVector :: "machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
where
"ioapicMapPinToVector ioapic pin level polarity vector \<equiv> undefined"
"ioapicMapPinToVector ioapic pin level polarity vector \<equiv> machine_op_lift (ioapicMapPinToVector_impl ioapic pin level polarity vector)"
datatype X64IRQState =
IRQFree
| IRQReserved
| IRQMSI
(MSIBus : machine_word)
(MSIDev : machine_word)
(MSIFunc : machine_word)
(MSIHandle : machine_word)
| IRQIOAPIC
(IRQioapic : machine_word)
(IRQPin : machine_word)
(IRQLevel : machine_word)
(IRQPolarity : machine_word)
(IRQMasked : bool)
consts'
updateIRQState_impl :: "irq \<Rightarrow> X64IRQState \<Rightarrow> unit machine_rest_monad"
definition
"irqStateIRQIOAPICNew \<equiv> error []"
definition
"irqStateIRQMSINew \<equiv> error []"
datatype x64irqstate =
X64IRQState
definition
updateIRQState :: "irq \<Rightarrow> x64irqstate \<Rightarrow> unit machine_monad"
updateIRQState :: "irq \<Rightarrow> X64IRQState \<Rightarrow> unit machine_monad"
where
"updateIRQState arg1 arg2 \<equiv> error []"
"updateIRQState arg1 arg2 \<equiv> machine_op_lift (updateIRQState_impl arg1 arg2)"
(*FIXME: How to deal with this directly? *)
definition
@ -353,36 +376,50 @@ where
"IRQ \<equiv> id"
(* FIXME x64: More underspecified operations *)
consts'
in8_impl :: "word16 \<Rightarrow> unit machine_rest_monad"
in8_val :: "machine_state \<Rightarrow> machine_word"
definition
in8 :: "word16 \<Rightarrow> machine_word machine_monad"
where
"in8 \<equiv> error []"
"in8 port \<equiv> do machine_op_lift $ in8_impl port; gets in8_val od"
consts'
in16_impl :: "word16 \<Rightarrow> unit machine_rest_monad"
in16_val :: "machine_state \<Rightarrow> machine_word"
definition
in16 :: "word16 \<Rightarrow> machine_word machine_monad"
where
"in16 \<equiv> error []"
"in16 port \<equiv> do machine_op_lift $ in16_impl port; gets in16_val od"
consts'
in32_impl :: "word16 \<Rightarrow> unit machine_rest_monad"
in32_val :: "machine_state \<Rightarrow> machine_word"
definition
in32 :: "word16 \<Rightarrow> machine_word machine_monad"
where
"in32 \<equiv> error []"
"in32 port \<equiv> do machine_op_lift $ in32_impl port; gets in32_val od"
consts'
out8_impl :: "word16 \<Rightarrow> word8 \<Rightarrow> unit machine_rest_monad"
definition
out8 :: "word16 \<Rightarrow> word8 \<Rightarrow> unit machine_monad"
where
"out8 \<equiv> error []"
"out8 port dat \<equiv> machine_op_lift $ out8_impl port dat"
consts'
out16_impl :: "word16 \<Rightarrow> word16 \<Rightarrow> unit machine_rest_monad"
definition
out16 :: "word16 \<Rightarrow> word16 \<Rightarrow> unit machine_monad"
where
"out16 \<equiv> error []"
"out16 port dat \<equiv> machine_op_lift $ out16_impl port dat"
consts'
out32_impl :: "word16 \<Rightarrow> word32 \<Rightarrow> unit machine_rest_monad"
definition
out32 :: "word16 \<Rightarrow> word32 \<Rightarrow> unit machine_monad"
where
"out32 \<equiv> error []"
"out32 port dat \<equiv> machine_op_lift $ out32_impl port dat"
end