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

isabelle-2021: x64 ainvs update 

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2021-09-17 10:21:22 +10:00 committed by Gerwin Klein
parent a3dbee3e72
commit 11fac22447
14 changed files with 167 additions and 212 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -214,7 +214,7 @@ bundle pagebits =
pml4_bits_def[simp] pml4_shift_bits_def[simp]
table_size_def[simp] ptTranslationBits_def[simp]
pageBits_def[simp] mask_lower_twice[simp]
word_bool_alg.conj_assoc[symmetric,simp] obj_at_def[simp]
and.assoc[where ?'a = \<open>'a::len word\<close>,symmetric,simp] obj_at_def[simp]
pde.splits[split] pdpte.splits[split] pml4e.splits[split]
pte.splits[split]
@ -2468,10 +2468,6 @@ lemma set_asid_pool_cur_tcb [wp]:
by (rule hoare_lift_Pf [where f=cur_thread]; wp)
crunch arch [wp]: set_asid_pool "\<lambda>s. P (arch_state s)"
(wp: get_object_wp)
lemma set_asid_pool_valid_arch [wp]:
"\<lbrace>valid_arch_state\<rbrace> set_asid_pool p a \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
by (rule valid_arch_state_lift) (wp set_asid_pool_typ_at)+

211
proof/invariant-abstract/X64/ArchArch_AI.thy
View File

@ -84,7 +84,7 @@ lemma check_vp_inv: "\<lbrace>P\<rbrace> check_vp_alignment sz w \<lbrace>\<lamb
lemma p2_low_bits_max:
"(2 ^ asid_low_bits - 1) = (max_word :: 9 word)"
by (simp add: asid_low_bits_def max_word_def)
by (simp add: asid_low_bits_def)
lemma dom_ucast_eq:
@ -123,7 +123,7 @@ lemma dom_ucast_eq:
lemma asid_high_bits_max_word:
"(2 ^ asid_high_bits - 1) = (max_word :: 3 word)"
by (simp add: asid_high_bits_def max_word_def)
by (simp add: asid_high_bits_def)
lemma dom_ucast_eq_8:
@ -732,9 +732,8 @@ lemma aci_invs':
\<lbrace>\<lambda>_.Q\<rbrace>"
assumes retype_region_Q[wp]:"\<And>a b c d e. \<lbrace>Q\<rbrace> retype_region a b c d e \<lbrace>\<lambda>_.Q\<rbrace>"
assumes set_cap_Q[wp]: "\<And>a b. \<lbrace>Q\<rbrace> set_cap a b \<lbrace>\<lambda>_.Q\<rbrace>"
shows
"\<lbrace>invs and Q and ct_active and valid_aci aci\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>y s. invs s \<and> Q s\<rbrace>"
proof -
shows "\<lbrace>invs and Q and ct_active and valid_aci aci\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>y s. invs s \<and> Q s\<rbrace>"
proof -
have cap_insert_invsQ:
"\<And>cap src dest ap asid.
\<lbrace>Q and (invs and valid_cap cap and tcb_cap_valid cap dest and
@ -757,117 +756,115 @@ lemma aci_invs':
(s\<lparr>arch_state := arch_state s
\<lparr>x64_asid_table := (x64_asid_table \<circ> arch_state) s
(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<rbrace>"
apply (wp cap_insert_ap_invs)
apply simp
apply (rule hoare_pre)
apply (rule cap_insert_Q)
apply (auto simp: cte_wp_at_caps_of_state)
done
apply (wp cap_insert_ap_invs)
apply simp
apply (rule hoare_pre)
apply (rule cap_insert_Q, assumption)
apply (auto simp: cte_wp_at_caps_of_state)
done
show ?thesis
apply (clarsimp simp: perform_asid_control_invocation_def valid_aci_def
split: asid_control_invocation.splits)
apply (rename_tac word1 a b aa ba word2)
apply (rule hoare_pre)
apply (wp hoare_vcg_const_imp_lift)
apply (wp cap_insert_invsQ hoare_vcg_ex_lift
| simp)+
apply (simp add: valid_cap_def |
strengthen real_cte_tcb_valid safe_parent_strg
invs_vobjs_strgs
ex_cte_cap_to_cnode_always_appropriate_strg)+
apply (wp hoare_vcg_const_imp_lift set_free_index_invs
retype_region_plain_invs[where sz = pageBits]
retype_cte_wp_at[where sz = pageBits] hoare_vcg_ex_lift
retype_region_obj_at_other3[where P="is_cap_table n" and sz = pageBits for n]
retype_region_ex_cte_cap_to[where sz = pageBits]
retype_region_ap[simplified]
retype_region_ap'[simplified]
retype_region_no_cap_to_obj[where sz = pageBits,simplified]
| simp del: split_paired_Ex)+
apply (strengthen invs_valid_objs invs_psp_aligned
invs_mdb invs_valid_pspace
exI[where x="case aci of MakePool frame slot parent base \<Rightarrow> parent"]
exI[where x="case aci of MakePool frame slot parent base \<Rightarrow> parent",
simplified]
caps_region_kernel_window_imp[where
p = "case aci of MakePool frame slot parent base \<Rightarrow> parent"]
invs_cap_refs_in_kernel_window)+
apply (wp set_cap_caps_no_overlap set_cap_no_overlap get_cap_wp
max_index_upd_caps_overlap_reserved max_index_upd_invs_simple
set_cap_cte_cap_wp_to set_cap_cte_wp_at max_index_upd_no_cap_to
| simp split del: if_split | wp (once) hoare_vcg_ex_lift)+
apply (rule_tac P = "is_aligned word1 page_bits" in hoare_gen_asm)
apply (subst delete_objects_rewrite)
apply (simp add:page_bits_def pageBits_def word_size_bits_def)
apply (simp add:page_bits_def pageBits_def word_bits_def)
apply (simp)
apply wp
apply (clarsimp simp: cte_wp_at_caps_of_state if_option_Some
Misc_Arithmetic.if_bool_simps
split del: if_split)
apply (frule_tac cap = "(cap.UntypedCap False word1 pageBits idx)"
in detype_invariants[rotated 3],clarsimp+)
apply (simp add:cte_wp_at_caps_of_state)+
apply (simp add:descendants_range_def2 empty_descendants_range_in)
apply (simp add:invs_mdb invs_valid_pspace invs_psp_aligned invs_valid_objs)
apply (clarsimp dest!:caps_of_state_cteD)
apply (frule(1) unsafe_protected[where p=t and p'=t for t])
apply (simp add:empty_descendants_range_in)+
apply fastforce
apply clarsimp
apply (frule_tac p = "(aa,ba)" in cte_wp_valid_cap)
apply fastforce
apply (clarsimp simp: detype_clear_um_independent obj_bits_api_def arch_kobj_size_def
default_arch_object_def conj_comms)
apply (rule conjI, clarsimp simp:valid_cap_simps cap_aligned_def page_bits_def not_le)+
apply clarsimp
apply (simp add:empty_descendants_range_in)
apply (frule valid_cap_aligned)
apply (clarsimp simp: cap_aligned_def)
apply (subst caps_no_overlap_detype[OF descendants_range_caps_no_overlapI],
assumption, simp,
simp add: empty_descendants_range_in)
apply (frule pspace_no_overlap_detype, clarify+)
apply (frule intvl_range_conv[where bits = pageBits])
apply (simp add:pageBits_def word_bits_def)
apply (simp)
apply (clarsimp simp: page_bits_def)
apply (frule(1) ex_cte_cap_protects)
apply (simp add:empty_descendants_range_in)
apply (clarsimp simp: perform_asid_control_invocation_def valid_aci_def
split: asid_control_invocation.splits)
apply (rename_tac word1 a b aa ba word2)
apply (rule hoare_pre)
apply (wp hoare_vcg_const_imp_lift)
apply (wp cap_insert_invsQ hoare_vcg_ex_lift | simp)+
apply (simp add: valid_cap_def |
strengthen real_cte_tcb_valid safe_parent_strg
invs_vobjs_strgs
ex_cte_cap_to_cnode_always_appropriate_strg)+
apply (wp hoare_vcg_const_imp_lift set_free_index_invs
retype_region_plain_invs[where sz = pageBits]
retype_cte_wp_at[where sz = pageBits] hoare_vcg_ex_lift
retype_region_obj_at_other3[where P="is_cap_table n" and sz = pageBits for n]
retype_region_ex_cte_cap_to[where sz = pageBits]
retype_region_ap[simplified]
retype_region_ap'[simplified]
retype_region_no_cap_to_obj[where sz = pageBits,simplified]
| simp del: split_paired_Ex)+
apply (strengthen invs_valid_objs invs_psp_aligned
invs_mdb invs_valid_pspace
exI[where x="case aci of MakePool frame slot parent base \<Rightarrow> parent"]
exI[where x="case aci of MakePool frame slot parent base \<Rightarrow> parent",
simplified]
caps_region_kernel_window_imp[where
p = "case aci of MakePool frame slot parent base \<Rightarrow> parent"]
invs_cap_refs_in_kernel_window)+
apply (wp set_cap_caps_no_overlap set_cap_no_overlap get_cap_wp
max_index_upd_caps_overlap_reserved max_index_upd_invs_simple
set_cap_cte_cap_wp_to set_cap_cte_wp_at max_index_upd_no_cap_to
| simp split del: if_split | wp (once) hoare_vcg_ex_lift)+
apply (rule_tac P = "is_aligned word1 page_bits" in hoare_gen_asm)
apply (subst delete_objects_rewrite)
apply (simp add:page_bits_def pageBits_def word_size_bits_def)
apply (simp add:page_bits_def pageBits_def word_bits_def)
apply (simp)
apply wp
apply (clarsimp simp: cte_wp_at_caps_of_state if_option_Some
if_bool_simps
split del: if_split)
apply (frule_tac cap = "(cap.UntypedCap False word1 pageBits idx)"
in detype_invariants[rotated 3],clarsimp+)
apply (simp add:cte_wp_at_caps_of_state)+
apply (simp add:descendants_range_def2 empty_descendants_range_in)
apply (simp add:invs_mdb invs_valid_pspace invs_psp_aligned invs_valid_objs)
apply (clarsimp dest!:caps_of_state_cteD)
apply (frule(1) unsafe_protected[where p=t and p'=t for t])
apply (simp add:empty_descendants_range_in)+
apply fastforce
apply clarsimp
apply (frule_tac p = "(aa,ba)" in cte_wp_valid_cap)
apply fastforce
apply (rule subset_refl)
apply fastforce
apply (clarsimp simp: field_simps)
apply (intro conjI impI,
simp_all add:free_index_of_def valid_cap_simps valid_untyped_def
empty_descendants_range_in range_cover_full clear_um_def max_free_index_def,
(clarsimp simp:valid_untyped_def valid_cap_simps)+)[1]
apply (clarsimp simp: detype_clear_um_independent obj_bits_api_def arch_kobj_size_def
default_arch_object_def conj_comms)
apply (rule conjI, clarsimp simp:valid_cap_simps cap_aligned_def page_bits_def not_le)+
apply clarsimp
apply (simp add:empty_descendants_range_in)
apply (frule valid_cap_aligned)
apply (clarsimp simp: cap_aligned_def)
apply (subst caps_no_overlap_detype[OF descendants_range_caps_no_overlapI],
assumption, simp, simp add: empty_descendants_range_in)
apply (frule pspace_no_overlap_detype, clarify+)
apply (frule intvl_range_conv[where bits = pageBits])
apply (simp add:pageBits_def word_bits_def)
apply (simp)
apply (clarsimp simp: page_bits_def)
apply (frule(1) ex_cte_cap_protects)
apply (simp add:empty_descendants_range_in)
apply fastforce
apply (rule subset_refl)
apply fastforce
apply (clarsimp simp: field_simps)
apply (intro conjI impI,
simp_all add: free_index_of_def valid_cap_simps valid_untyped_def empty_descendants_range_in
range_cover_full clear_um_def max_free_index_def,
(clarsimp simp:valid_untyped_def valid_cap_simps)+)[1]
apply (simp add: cte_wp_at_def)
apply (simp add: cte_wp_at_def)
apply (erule(1) cap_to_protected)
apply (simp add:empty_descendants_range_in descendants_range_def2)+
apply (erule(1) cap_to_protected)
apply (simp add:empty_descendants_range_in descendants_range_def2)+
apply clarsimp
apply (drule invs_arch_state)+
apply (clarsimp simp: valid_arch_state_def valid_asid_table_def)
apply (drule (1) bspec)+
apply clarsimp
apply (erule notE, erule is_aligned_no_overflow)
apply clarsimp
apply (drule invs_arch_state)+
apply (clarsimp simp: valid_arch_state_def valid_asid_table_def)
apply (drule (1) bspec)+
apply clarsimp
apply (erule notE, erule is_aligned_no_overflow)
apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def)
apply (thin_tac "cte_wp_at ((=) cap.NullCap) p s" for p s)
apply (subst(asm) eq_commute,
erule(1) untyped_children_in_mdbE[where cap="cap.UntypedCap dev p bits idx" for dev p bits idx,
simplified, rotated])
apply (simp add: is_aligned_no_overflow)
apply simp
apply clarsimp
done
apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def)
apply (thin_tac "cte_wp_at ((=) cap.NullCap) p s" for p s)
apply (subst(asm) eq_commute,
erule(1) untyped_children_in_mdbE[where cap="cap.UntypedCap dev p bits idx" for dev p bits idx,
simplified, rotated])
apply (simp add: is_aligned_no_overflow)
apply simp
apply clarsimp
done
qed
lemmas aci_invs[wp] = aci_invs'[where Q=\<top>,simplified hoare_post_taut, OF refl refl refl TrueI TrueI TrueI,simplified]
lemma set_ioport_mask_tcb_cap_valid[wp]:

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

@ -676,13 +676,14 @@ next
apply (erule disjE)
apply (simp only: zobj_refs.simps mem_simps)
apply clarsimp+
apply (drule sym, simp)
apply (drule sym, simp)
apply clarsimp
apply (simp add: unat_eq_0)
apply (drule of_bl_eq_0)
apply (drule zombie_cte_bits_less, simp add: word_bits_def)
apply (clarsimp simp: cte_wp_at_caps_of_state)
subgoal
apply (drule sym, simp)
apply (drule sym, simp)
apply clarsimp
apply (simp add: unat_eq_0)
apply (drule of_bl_eq_0)
apply (drule zombie_cte_bits_less, simp add: word_bits_def)
by (clarsimp simp: cte_wp_at_caps_of_state)
apply (drule_tac s="appropriate_cte_cap c" for c in sym)
apply (clarsimp simp: is_cap_simps appropriate_Zombie gen_obj_refs_eq)
apply (simp add: is_final_cap_def)

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

@ -179,8 +179,6 @@ lemma set_cap_valid_vs_lookup:
apply (auto simp: cte_wp_at_caps_of_state)[1]
done
crunch arch[wp]: set_cap "\<lambda>s. P (arch_state s)" (simp: split_def)
lemma set_cap_valid_table_caps:
"\<lbrace>\<lambda>s. valid_table_caps s
\<and> ((is_vspace_table_cap cap) \<longrightarrow> cap_asid cap = None
@ -338,15 +336,11 @@ lemma set_cap_hyp_refs_of [wp]:
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
apply (simp add: set_cap_def set_object_def split_def)
apply (wp get_object_wp | wpc)+
apply (auto elim!: rsubst[where P=P]
simp: state_hyp_refs_of_def obj_at_def
intro!: ext
split: if_split_asm)
done
by (fastforce elim!: rsubst[where P=P]
simp: state_hyp_refs_of_def obj_at_def
split: if_split_asm)
lemma state_hyp_refs_of_revokable[simp]:
"state_hyp_refs_of (s \<lparr> is_original_cap := m \<rparr>) = state_hyp_refs_of s"
by (rule revokable_update.state_hyp_refs_update)
lemmas state_hyp_refs_of_revokable = state_hyp_refs_update
lemma is_valid_vtable_root_is_arch_cap:
"is_valid_vtable_root cap \<Longrightarrow> is_arch_cap cap"

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

@ -266,7 +266,7 @@ lemma safe_parent_for_arch_not_arch:
by (clarsimp simp: safe_parent_for_arch_def is_cap_simps)
lemma safe_parent_cap_range_arch:
"\<And>cap pcap. safe_parent_for_arch cap pcap \<Longrightarrow> cap_range cap \<subseteq> cap_range pcap"
"safe_parent_for_arch cap pcap \<Longrightarrow> cap_range cap \<subseteq> cap_range pcap"
by (clarsimp simp: safe_parent_for_arch_def cap_range_def)
definition

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

@ -516,7 +516,7 @@ lemma tcb_cnode_index_def2 [CSpace_AI_assms]:
apply (clarsimp simp: to_bl_nth word_size word_bits_def)
apply (subst of_nat_ucast[where 'a=machine_word_len and 'b=3])
apply (simp add: is_down_def target_size_def source_size_def word_size)
apply (simp add: nth_ucast)
apply (simp add: nth_ucast del: unsigned_of_nat)
apply fastforce
done

28
proof/invariant-abstract/X64/ArchDetSchedAux_AI.thy
View File

@ -14,7 +14,6 @@ named_theorems DetSchedAux_AI_assms
crunch exst[wp]: set_object, init_arch_objects "\<lambda>s. P (exst s)" (wp: crunch_wps hoare_unless_wp)
crunch ct[wp]: init_arch_objects "\<lambda>s. P (cur_thread s)" (wp: crunch_wps hoare_unless_wp)
crunch st_tcb_at[wp]: init_arch_objects "st_tcb_at Q t" (wp: mapM_x_wp' hoare_unless_wp)
crunch valid_etcbs[wp, DetSchedAux_AI_assms]: init_arch_objects valid_etcbs (wp: valid_etcbs_lift)
crunch ct[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (cur_thread s)"
@ -56,7 +55,6 @@ crunch ekheap[wp]: do_machine_op "\<lambda>s. P (ekheap s)"
lemma delete_objects_etcb_at[wp, DetSchedAux_AI_assms]:
"\<lbrace>\<lambda>s::det_ext state. etcb_at P t s\<rbrace> delete_objects a b \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>"
apply (simp add: delete_objects_def)
apply (wp)
apply (simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def etcb_at_def|wp)+
done
@ -85,32 +83,6 @@ lemma invoke_untyped_etcb_at [DetSchedAux_AI_assms]:
crunch valid_blocked[wp, DetSchedAux_AI_assms]: init_arch_objects valid_blocked
(wp: valid_blocked_lift set_cap_typ_at)
crunch ct[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (cur_thread s)"
(wp: crunch_wps dxo_wp_weak simp: crunch_simps do_machine_op_def detype_def mapM_x_defsym
ignore: freeMemory ignore: retype_region_ext)
crunch ready_queues[wp, DetSchedAux_AI_assms]:
invoke_untyped "\<lambda>s :: det_ext state. P (ready_queues s)"
(wp: crunch_wps
simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym
ignore: freeMemory)
crunch scheduler_action[wp, DetSchedAux_AI_assms]:
invoke_untyped "\<lambda>s :: det_ext state. P (scheduler_action s)"
(wp: crunch_wps
simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym
ignore: freeMemory)
crunch cur_domain[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s :: det_ext state. P (cur_domain s)"
(wp: crunch_wps
simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym
ignore: freeMemory)
crunch idle_thread[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (idle_thread s)"
(wp: crunch_wps dxo_wp_weak hoare_unless_wp
simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym
ignore: freeMemory retype_region_ext)
lemma perform_asid_control_etcb_at:"\<lbrace>(\<lambda>s. etcb_at P t s) and valid_etcbs\<rbrace>
perform_asid_control_invocation aci
\<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"

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

@ -521,7 +521,7 @@ lemma cap_refs_respects_device_region_detype[detype_invs_proofs]:
have "cap_refs_respects_device_region s"
using invs by (simp add: invs_def valid_state_def)
thus ?thesis
apply (clarsimp simp: clear_um_def cap_refs_respects_device_region_def cte_wp_at_detype
apply (clarsimp simp: clear_um_def cap_refs_respects_device_region_def
simp del: split_paired_All split_paired_Ex)
apply (drule_tac x = "(a,b)" in spec)
apply (clarsimp simp: cte_wp_at_caps_of_state cap_range_respects_device_region_def detype_def)

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

@ -123,7 +123,7 @@ lemma arch_decode_irq_control_valid[wp]:
| wp hoare_vcg_imp_lift_R[where P="\<lambda>rv s. x64_num_ioapics (arch_state s) \<noteq> 0"]
| wp (once) hoare_drop_imps)+
apply ( safe; auto simp: word_le_not_less[symmetric] word_leq_minus_one_le
ucast_id irq_plus_min_ge_min irq_plus_min_le_max ioapicIRQLines_def
irq_plus_min_ge_min irq_plus_min_le_max ioapicIRQLines_def
minUserIRQ_def maxUserIRQ_def word_add_le_mono1 word_add_le_mono2
word_le_plus irq_ineq_one irq_ineq_two irq_ineq_three irq_ineq_four
| cap_hammer | word_hammer)+
@ -266,7 +266,7 @@ lemma updateIRQState_invs[wp]:
vs_lookup_pages1_def valid_table_caps_def empty_table_def second_level_tables_def
valid_global_objs_def valid_kernel_mappings_def valid_asid_map_def
valid_x64_irq_state_def valid_ioports_def all_ioports_issued_def
issued_ioports_def Word_Lemmas.word_not_le[symmetric])
issued_ioports_def word_not_le[symmetric])
done
lemma no_irq_ioapicMapPinToVector: "no_irq (ioapicMapPinToVector a b c d e)"

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

@ -12,10 +12,38 @@ context Arch begin global_naming X64
named_theorems Ipc_AI_assms
crunch pspace_respects_device_region[wp]: set_extra_badge "pspace_respects_device_region"
crunch cap_refs_respects_device_region[wp]: set_extra_badge "cap_refs_respects_device_region"
(wp: crunch_wps cap_refs_respects_device_region_dmo)
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 badge_bits) rights) else NullCap
| NotificationCap r badge rights \<Rightarrow>
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 >> cnode_padding_bits) && mask cnode_guard_size_bits) + bits
then NullCap
else CNodeCap r bits ((\<lambda>g''. drop (size g'' - unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits))
(to_bl g''))
((w >> 6) && mask 58))
| ThreadCap r \<Rightarrow> ThreadCap r
| DomainCap \<Rightarrow> DomainCap
| UntypedCap d p n idx \<Rightarrow> UntypedCap d p n idx
| NullCap \<Rightarrow> NullCap
| ReplyCap t m rights \<Rightarrow> ReplyCap t m rights
| IRQControlCap \<Rightarrow> IRQControlCap
| IRQHandlerCap irq \<Rightarrow> IRQHandlerCap irq
| Zombie r b n \<Rightarrow> Zombie r b n
| ArchObjectCap cap \<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 cnode_padding_bits_def cnode_guard_size_bits_def
cong: if_cong)
apply (auto simp: cnode_padding_bits_def cnode_guard_size_bits_def)
done
lemma cap_asid_PageCap_None [simp]:
"cap_asid (ArchObjectCap (PageCap d r R typ pgsz None)) = None"
@ -210,6 +238,7 @@ lemma valid_msg_length_strengthen [Ipc_AI_assms]:
apply (clarsimp simp: valid_message_info_def)
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)
including no_take_bit
apply (clarsimp simp: un_ui_le word_le_def)
done
@ -416,10 +445,10 @@ crunch typ_at[Ipc_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register
end
interpretation Ipc_AI?: Ipc_AI
proof goal_cases
proof goal_cases
interpret Arch .
case 1 show ?case by (unfold_locales; (fact Ipc_AI_assms)?)
qed
qed
context Arch begin global_naming X64

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

@ -256,7 +256,8 @@ lemma set_object_pt_not_vs_lookup_pages:
apply (clarsimp simp: obj_at_def split:if_split_asm)
apply (case_tac "pa=p")
apply (clarsimp simp: vs_refs_pages_def graph_of_def)
apply (erule_tac x=ab in allE)
apply (rename_tac slot pte)
apply (erule_tac x=slot in allE)
apply (drule_tac R="vs_lookup_pages1 s" in rtranclD)
apply clarsimp
apply (drule tranclD)
@ -277,7 +278,8 @@ lemma set_object_pt_not_vs_lookup_pages:
apply (clarsimp simp: obj_at_def split:if_split_asm)
apply (case_tac "pa=p")
apply (clarsimp simp: vs_refs_pages_def graph_of_def)
apply (erule_tac x=rs in allE)
apply (rename_tac vs slot pte)
apply (erule_tac x=vs in allE)
apply (clarsimp simp: vs_lookup_pages_def)
apply (drule(1) ImageI, erule (1) notE)
apply clarsimp
@ -891,7 +893,7 @@ lemma valid_arch_mdb_lift:
assumes c: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (caps_of_state s)\<rbrace>"
assumes r: "\<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> f \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace>"
shows "\<lbrace>\<lambda>s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>"
apply (clarsimp simp: valid_arch_mdb_def valid_def)
apply (clarsimp simp: valid_def)
apply (frule_tac P1="(=) (caps_of_state s)" in use_valid [OF _ c], rule refl)
apply (frule_tac P1="(=) (is_original_cap s)" in use_valid [OF _ r], rule refl)
apply clarsimp

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

@ -58,7 +58,7 @@ lemma descendants_empty [simp]:
"descendants_of x Map.empty = {}"
by (clarsimp simp: descendants_of_def)
lemma [simp]: "\<not>is_reply_cap Structures_A.NullCap"
lemma reply_Null [simp]: "\<not>is_reply_cap NullCap"
by (simp add: is_reply_cap_def)
declare cap_range_NullCap [simp]
@ -122,9 +122,8 @@ lemma init_irq_ptrs_eq:
apply (erule_tac bnd="ucast (max_word :: irq) + 1"
in shift_distinct_helper[rotated 3],
safe intro!: plus_one_helper2,
simp_all add: ucast_le_ucast[where 'a=8 and 'b=64,simplified] up_ucast_inj_eq,
simp_all add: cte_level_bits_def word_bits_def up_ucast_inj_eq
max_word_def)
simp_all add: ucast_le_ucast[where 'a=8 and 'b=64,simplified] up_ucast_inj_eq ucast_leq_mask,
simp_all add: cte_level_bits_def word_bits_def up_ucast_inj_eq mask_eq_exp_minus_1)
done
lemma in_kernel_base:
@ -238,7 +237,7 @@ done
lemma invs_A:
"invs init_A_st" (is "invs ?st")
supply is_aligned_def[THEN meta_eq_to_obj_eq, THEN iffD2, simp]
supply is_aligned_def[THEN iffD2, simp]
supply image_cong_simp [cong del]
apply (simp add: invs_def)
apply (rule conjI)

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

@ -18,9 +18,7 @@ lemma of_bl_nat_to_cref[Untyped_AI_assms]:
apply (clarsimp intro!: less_mask_eq
simp: nat_to_cref_def of_drop_to_bl
word_size word_less_nat_alt word_bits_def)
apply (subst unat_of_nat)
apply (erule order_le_less_trans [OF mod_less_eq_dividend])
done
by (simp add: take_bit_nat_def)
lemma cnode_cap_ex_cte[Untyped_AI_assms]:
@ -208,11 +206,6 @@ proof -
done
qed
crunch pdistinct[wp]: do_machine_op "pspace_distinct"
crunch vmdb[wp]: do_machine_op "valid_mdb"
crunch mdb[wp]: do_machine_op "\<lambda>s. P (cdt s)"
crunch cte_wp_at[wp]: do_machine_op "\<lambda>s. P (cte_wp_at P' p s)"
lemma cap_refs_in_kernel_windowD2:
"\<lbrakk> cte_wp_at P p (s::'state_ext::state_ext state); cap_refs_in_kernel_window s \<rbrakk>
\<Longrightarrow> \<exists>cap. P cap \<and> region_in_kernel_window (cap_range cap) s"
@ -393,21 +386,6 @@ lemma create_cap_ioports[wp, Untyped_AI_assms]:
by (wpsimp wp: set_cap_ioports' set_cdt_cte_wp_at
simp: safe_ioport_insert_not_ioport[OF default_cap_not_ioport] create_cap_def)
crunch irq_node[wp]: store_pde "\<lambda>s. P (interrupt_irq_node s)"
(wp: crunch_wps)
(* make these available in the generic theory? *)
lemma init_arch_objects_irq_node[wp]:
"\<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> init_arch_objects tp ptr bits us refs \<lbrace>\<lambda>rv s. P (interrupt_irq_node s)\<rbrace>"
by (wp init_arch_objects_hoare_lift | simp)+
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 init_arch_objects_irq_node init_arch_objects_cte_wp_at)
crunch nonempty_table[wp]: do_machine_op
"\<lambda>s. P' (obj_at (nonempty_table (set (x64_global_pts (arch_state s)))) r s)"
(* FIXME: move *)
lemma simpler_store_pml4e_def:
"store_pml4e p pde s =

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

@ -166,10 +166,6 @@ lemma dmo_vspace_at_asid [wp]:
apply (simp add: vspace_at_asid_def)
done
crunch inv: find_vspace_for_asid "P"
(simp: assertE_def crunch_simps wp: crunch_wps)
lemma find_vspace_for_asid_vspace_at_asid [wp]:
"\<lbrace>\<top>\<rbrace> find_vspace_for_asid asid \<lbrace>\<lambda>pd. vspace_at_asid asid pd\<rbrace>, -"
apply (simp add: find_vspace_for_asid_def assertE_def split del: if_split)
@ -384,10 +380,6 @@ lemma valid_global_objs_arch_update:
by (simp add: valid_global_objs_def second_level_tables_def)
crunch pred_tcb_at [wp]: find_vspace_for_asid "\<lambda>s. P (pred_tcb_at proj Q p s)"
(simp: crunch_simps)
lemma find_vspace_for_asid_assert_wp:
"\<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<and> asid \<noteq> 0 \<longrightarrow> P pd s\<rbrace> find_vspace_for_asid_assert asid \<lbrace>P\<rbrace>"
apply (simp add: find_vspace_for_asid_assert_def
@ -2841,9 +2833,6 @@ lemma update_aobj_zombies[wp]:
crunch is_final_cap' [wp]: store_pde "is_final_cap' cap"
(wp: crunch_wps simp: crunch_simps set_arch_obj_simps ignore: set_object set_pd)
crunch is_final_cap' [wp]: store_pte "is_final_cap' cap"
(wp: crunch_wps simp: crunch_simps ignore: set_object set_pt)
crunch is_final_cap' [wp]: store_pdpte "is_final_cap' cap"
(wp: crunch_wps simp: crunch_simps set_arch_obj_simps ignore: set_object set_pdpt)
@ -3311,8 +3300,6 @@ lemma vs_lookup_invs_ref_is_unique: "\<lbrakk> (ref \<rhd> p) s; (ref' \<rhd> p)
apply (erule reachable_pd_not_global)
by (auto elim: invs_valid_kernel_mappings intro!: valid_objs_caps)
crunch global_refs: store_pde "\<lambda>s. P (global_refs s)"
crunch invs[wp]: pte_check_if_mapped, pde_check_if_mapped "invs"
crunch vs_lookup[wp]: pte_check_if_mapped, pde_check_if_mapped "\<lambda>s. P (vs_lookup s)"