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

cleanup ainvs: reduce warnings 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-01-18 11:20:54 +11:00 committed by Gerwin Klein
parent bf58cb2a19
commit 57d0333204
17 changed files with 62 additions and 233 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -735,10 +735,6 @@ lemma cte_wp_and:
by (auto simp: cte_wp_at_def)
crunch cte_wp_at[wp]: get_mrs "cte_wp_at P c"
(wp: crunch_wps simp: crunch_simps)
lemmas cte_wp_and' = cte_wp_and [unfolded pred_conj_def]
@ -1513,7 +1509,7 @@ lemma cap_swap_fd_caps_of_state[wp]:
apply (simp add: fun_upd_def id_def[symmetric] cong: if_cong)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (erule rsubst[where P=P])
apply (clarsimp intro!: ext)
apply fastforce
done
@ -2718,14 +2714,6 @@ crunch rvk_prog: cancel_ipc "\<lambda>s. revoke_progress_ord m (\<lambda>x. opti
wp: hoare_drop_imps empty_slot_rvk_prog' select_wp
thread_set_caps_of_state_trivial)
crunch rvk_prog: cancel_all_ipc "\<lambda>s. revoke_progress_ord m (\<lambda>x. option_map cap_to_rpo (caps_of_state s x))"
(simp: crunch_simps o_def unless_def is_final_cap_def
wp: crunch_wps empty_slot_rvk_prog' select_wp)
crunch rvk_prog: cancel_all_signals "\<lambda>s. revoke_progress_ord m (\<lambda>x. option_map cap_to_rpo (caps_of_state s x))"
(simp: crunch_simps o_def unless_def is_final_cap_def
wp: crunch_wps empty_slot_rvk_prog' select_wp)
crunch rvk_prog: suspend "\<lambda>s. revoke_progress_ord m (\<lambda>x. option_map cap_to_rpo (caps_of_state s x))"
(simp: crunch_simps o_def unless_def is_final_cap_def
wp: crunch_wps empty_slot_rvk_prog' select_wp)

3
proof/invariant-abstract/CSpaceInv_AI.thy
View File

@ -102,9 +102,6 @@ crunch inv[wp]: get_cap "P"
(simp: crunch_simps)
declare resolve_address_bits'.simps [simp del]
lemma rab_inv[wp]:
"\<lbrace>P\<rbrace> resolve_address_bits slot \<lbrace>\<lambda>rv. P\<rbrace>"
unfolding resolve_address_bits_def

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

@ -57,7 +57,7 @@ lemma capBadge_ordefield_simps[simp]:
"((y, y) \<in> capBadge_ordering fb) = (fb \<longrightarrow> (y = None \<or> y = Some 0))"
"((Some x, Some z) \<in> capBadge_ordering fb) = (x = 0 \<or> (\<not> fb \<and> x = z))"
"(y, Some 0) \<in> capBadge_ordering fb = (y = None \<or> y = Some 0)"
by (simp add: capBadge_ordering_def disj_ac
by (simp add: capBadge_ordering_def disj.commute
| simp add: eq_commute image_def
| fastforce)+
@ -121,9 +121,6 @@ lemma preemption_point_inv:
end
lemmas valid_cap_machine_state [iff]
= machine_state_update.valid_cap_update
lemma get_cap_valid [wp]:
"\<lbrace> valid_objs \<rbrace> get_cap addr \<lbrace> valid_cap \<rbrace>"
apply (wp get_cap_wp)
@ -1405,22 +1402,22 @@ proof -
apply (erule_tac x=src in allE)
apply (erule_tac x=p' in allE)
apply (cut_tac p = src and c' = c in no_usage)
apply (clarsimp simp del:split_paired_All split del:if_splits simp: descendants_child)
apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child)
apply (erule_tac x=src in allE)
apply (erule_tac x=p' in allE)
apply (clarsimp simp del:split_paired_All split del:if_splits simp: descendants_child)
apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child)
apply (erule_tac x=p in allE)
apply (case_tac "p'=dest")
apply (case_tac "p'=src")
apply (erule_tac x=src in allE)
apply (clarsimp simp del:split_paired_All split del:if_splits simp: descendants_child)
apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child)
apply (erule_tac x=src in allE)
apply (clarsimp simp del:split_paired_All split del:if_splits simp: descendants_child)
apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child)
apply (cut_tac p = "(a,b)" and c' = ca in no_usage)
apply (clarsimp simp del:split_paired_All split del:if_splits simp: descendants_child)
apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child)
apply (case_tac "p' = src")
apply (erule_tac x = src in allE)
apply (clarsimp simp del:split_paired_All split del:if_splits simp: descendants_child)
apply (clarsimp simp del:split_paired_All split del:if_split simp: descendants_child)
apply (erule_tac x = p' in allE)
apply (clarsimp simp del:split_paired_All simp: descendants_child)
done
@ -1725,7 +1722,7 @@ lemma mdb_cte_at_set_untyped_cap_as_full:
\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace>
set_untyped_cap_as_full src_cap cap src
\<lbrace>\<lambda>rv s'. mdb_cte_at (swp (cte_wp_at P) s') (cdt s') \<rbrace>"
apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_splits)
apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_split)
apply (rule hoare_pre)
apply (wp set_cap_mdb_cte_at)
apply clarsimp
@ -1741,7 +1738,7 @@ lemma set_untyped_cap_as_full_is_original[wp]:
"\<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace>
set_untyped_cap_as_full src_cap cap src
\<lbrace>\<lambda>rv s'. P (is_original_cap s') \<rbrace>"
apply (simp add:set_untyped_cap_as_full_def split del:if_splits)
apply (simp add:set_untyped_cap_as_full_def split del:if_split)
apply (rule hoare_pre)
apply wp
apply auto
@ -1827,7 +1824,7 @@ lemma cap_insert_mdb_cte_at:
set_cap_cte_wp_at get_cap_wp)+
apply (clarsimp simp:free_index_update_def split:cap.splits)
apply (wp)+
apply (clarsimp simp:if_True conj_comms split del:if_splits cong:prod.case_cong_weak)
apply (clarsimp simp:conj_comms split del:if_split cong:prod.case_cong_weak)
apply (wps)
apply (wp valid_case_option_post_wp get_cap_wp hoare_vcg_if_lift
hoare_impI set_untyped_cap_as_full_cte_wp_at )+
@ -2997,7 +2994,7 @@ lemma descendants_inc:
assumes c: "weak_derived cap src_cap"
shows "descendants_inc m' (cs (dest \<mapsto> cap, src \<mapsto> cap.NullCap))"
using dc s d c
apply (simp add: descendants_inc_def descendants split)
apply (simp add: descendants_inc_def descendants)
apply (intro allI conjI)
apply (intro impI allI)
apply (drule spec)+
@ -3026,33 +3023,33 @@ proof -
split: if_split_asm cap.splits)
with ut s d
show ?thesis
apply (simp add: untyped_inc_def descendants del: split_paired_All split del: if_splits)
apply (simp add: untyped_inc_def descendants del: split_paired_All split del: if_split)
apply (intro allI)
apply (case_tac "p = src")
apply (simp del: split_paired_All split del: if_splits)
apply (simp del: split_paired_All split del: if_splits)
apply (simp del: split_paired_All split del: if_split)
apply (simp del: split_paired_All split del: if_split)
apply (case_tac "p = dest")
apply (simp del: split_paired_All split del: if_splits)
apply (simp del: split_paired_All split del: if_split)
apply (case_tac "p' = src")
apply (simp del: split_paired_All split del: if_splits)+
apply (simp del: split_paired_All split del: if_split)+
apply (case_tac "p' = dest")
apply (simp del:split_paired_All split del:if_splits)+
apply (simp del:split_paired_All split del:if_split)+
apply (intro impI allI conjI)
apply ((erule_tac x=src in allE,erule_tac x=p' in allE,simp)+)[5]
apply (erule_tac x=src in allE)
apply (erule_tac x=p' in allE)
apply simp
apply (intro conjI impI)
apply (simp del:split_paired_All split del:if_splits)+
apply (simp del:split_paired_All split del:if_split)+
apply (case_tac "p' = src")
apply (simp del: split_paired_All split del: if_splits)+
apply (simp del: split_paired_All split del: if_split)+
apply (case_tac "p' = dest")
apply (simp del:split_paired_All split del:if_splits)+
apply (simp del:split_paired_All split del:if_split)+
apply (intro impI allI conjI)
apply (erule_tac x=p in allE,erule_tac x=src in allE)
apply simp
apply (intro conjI impI)
apply (simp del:split_paired_All split del:if_splits)+
apply (simp del:split_paired_All split del:if_split)+
apply (intro conjI impI allI)
apply (erule_tac x=p in allE,erule_tac x=p' in allE)
apply simp
@ -3574,9 +3571,6 @@ lemma set_untyped_cap_as_full_valid_reply_masters:
done
crunch global_refs[wp]: set_untyped_cap_as_full "\<lambda>s. P (global_refs s)"
lemma set_untyped_cap_as_full_valid_global_refs[wp]:
"\<lbrace>valid_global_refs and cte_wp_at ((=) src_cap) src\<rbrace>
set_untyped_cap_as_full src_cap cap src
@ -3822,8 +3816,6 @@ lemma set_cdt_valid_ioc[wp]:
crunch valid_ioc[wp]: update_cdt valid_ioc
crunch cte_wp_at[wp]: update_cdt "cte_wp_at P slot"
(* FIXME: we could weaken this. *)
lemma set_original_valid_ioc[wp]:

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

@ -151,8 +151,6 @@ context DetSchedDomainTime_AI begin
crunch domain_list_inv[wp]: do_ipc_transfer "\<lambda>s. P (domain_list s)"
(wp: crunch_wps simp: zipWithM_x_mapM rule: transfer_caps_loop_pres)
crunch domain_list_inv[wp]: copy_mrs "\<lambda>s. P (domain_list s)"
crunch domain_list_inv[wp]: handle_fault "\<lambda>s. P (domain_list s)"
(wp: mapM_wp hoare_drop_imps simp: crunch_simps ignore:copy_mrs)
@ -189,11 +187,6 @@ crunch domain_list_inv[wp]:
(wp: crunch_wps check_cap_inv)
end
crunch (in DetSchedDomainTime_AI_2) domain_list_inv[wp]: arch_perform_invocation "\<lambda>s. P (domain_list s)"
(wp: crunch_wps check_cap_inv)
crunch (in DetSchedDomainTime_AI_2) domain_list_inv[wp]: handle_interrupt "\<lambda>s. P (domain_list s)"
crunch domain_list_inv[wp]: cap_move "\<lambda>s. P (domain_list s)"
context DetSchedDomainTime_AI begin
@ -299,8 +292,6 @@ context DetSchedDomainTime_AI begin
crunch domain_time_inv[wp]: do_ipc_transfer "\<lambda>s. P (domain_time s)"
(wp: crunch_wps simp: zipWithM_x_mapM rule: transfer_caps_loop_pres)
crunch domain_time_inv[wp]: copy_mrs "\<lambda>s. P (domain_time s)"
crunch domain_time_inv[wp]: handle_fault "\<lambda>s. P (domain_time s)"
(wp: mapM_wp hoare_drop_imps simp: crunch_simps ignore:copy_mrs)
@ -383,9 +374,6 @@ lemma handle_event_domain_time_inv:
apply (wp|simp|wpc)+
done
crunch domain_time_inv[wp]: send_fault_ipc, handle_call "\<lambda>s. P (domain_time s)"
(wp: hoare_drop_imps mapM_x_wp_inv select_wp without_preemption_wp simp: crunch_simps unless_def)
end
lemma next_domain_domain_time_left[wp]:
@ -408,8 +396,6 @@ lemma schedule_choose_new_thread_domain_time_left[wp]:
unfolding schedule_choose_new_thread_def
by (wpsimp simp: word_gt_0)
crunch valid_domain_list: schedule_choose_new_thread valid_domain_list
crunch etcb_at[wp]: tcb_sched_action "etcb_at P t"
lemma schedule_domain_time_left:

3
proof/invariant-abstract/DetSchedInvs_AI.thy
View File

@ -407,7 +407,8 @@ lemma valid_etcbs_tcb_etcb:
lemma valid_etcbs_get_tcb_get_etcb:
"\<lbrakk> valid_etcbs s; get_tcb ptr s = Some tcb \<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb ptr s = Some etcb"
apply (clarsimp simp: valid_etcbs_def valid_etcbs_def st_tcb_at_def obj_at_def is_etcb_at_def get_etcb_def get_tcb_def split: option.splits if_split)
apply (clarsimp simp: valid_etcbs_def st_tcb_at_def obj_at_def is_etcb_at_def get_etcb_def get_tcb_def
split: option.splits if_split)
apply (erule_tac x=ptr in allE)
apply (clarsimp simp: get_etcb_def split: option.splits kernel_object.splits)+
done

33
proof/invariant-abstract/DetSchedSchedule_AI.thy
View File

@ -196,8 +196,6 @@ abbreviation valid_sched_except_blocked_2 where
abbreviation valid_sched_except_blocked :: "det_ext state \<Rightarrow> bool" where
"valid_sched_except_blocked s \<equiv> valid_sched_except_blocked_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)"
crunch etcb_at[wp]: tcb_sched_action "etcb_at P t"
declare valid_idle_etcb_lift[wp]
lemma tcb_sched_action_enqueue_valid_sched[wp]:
@ -608,8 +606,6 @@ lemma set_bound_notification_valid_blocked[wp]:
apply (simp add: st_tcb_def2 split: if_split_asm)
done
crunch valid_blocked[wp]: get_bound_notification "valid_blocked"
lemma set_bound_notification_valid_sched:
"\<lbrace>valid_sched\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_sched\<rbrace>"
apply (simp add: valid_sched_def | wp set_bound_notification_valid_queues
@ -1108,8 +1104,6 @@ lemma tcb_sched_action_lift:
\<Longrightarrow> \<lbrace>P\<rbrace> tcb_sched_action a b \<lbrace>\<lambda>_. P\<rbrace>"
by (wp | simp add: tcb_sched_action_def etcb_at_def)+
crunch valid_idle[wp]: next_domain valid_idle
definition next_thread where
"next_thread queues \<equiv> (hd (max_non_empty_queue queues))"
@ -1253,8 +1247,6 @@ lemma set_scheduler_action_rct_switch_thread_valid_blocked:
apply clarsimp
done
crunch etcb_at[wp]: set_scheduler_action "etcb_at P t"
lemma set_scheduler_action_rct_switch_thread_valid_sched:
"\<lbrace>valid_sched and ct_not_queued
and (\<lambda>s. st_tcb_at activatable (cur_thread s) s)
@ -1473,9 +1465,6 @@ lemma cancel_all_ipc_valid_sched[wp]:
apply (simp_all add: valid_sched_def valid_sched_action_def)
done
crunch etcb_at[wp]: set_notification "etcb_at P t"
(wp: crunch_wps simp: crunch_simps)
lemma cancel_all_signals_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> cancel_all_signals ntfnptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
apply (simp add: cancel_all_signals_def)
@ -2611,7 +2600,6 @@ lemma set_thread_state_ready_queues[wp]:
apply (wp | wpc | simp add: tcb_sched_action_def)+
done
crunch scheduler_act[wp]: cap_insert_ext "\<lambda>s :: det_ext state. P (scheduler_action s)"
crunch scheduler_act[wp]: set_extra_badge,cap_insert "\<lambda>s :: det_state. P (scheduler_action s)" (wp: crunch_wps)
context DetSchedSchedule_AI begin
@ -2619,8 +2607,6 @@ context DetSchedSchedule_AI begin
crunch scheduler_act[wp]: do_ipc_transfer "\<lambda>s :: det_state. P (scheduler_action s)"
(wp: crunch_wps ignore: const_on_failure rule: transfer_caps_loop_pres)
crunch ready_queues[wp]: cap_insert_ext "\<lambda>s :: det_ext state. P (ready_queues s)"
crunch ready_queues[wp]: cap_insert,set_extra_badge,do_ipc_transfer, set_simple_ko, thread_set, setup_caller_cap "\<lambda>s :: det_state. P (ready_queues s)"
(wp: crunch_wps ignore: const_on_failure rule: transfer_caps_loop_pres)
@ -2648,7 +2634,7 @@ lemma send_ipc_valid_sched:
apply (wp set_thread_state_runnable_valid_queues
set_thread_state_runnable_valid_sched_action
set_thread_state_valid_blocked_except sts_st_tcb_at')
apply (clarsimp simp: conj_ac eq_commute)
apply (clarsimp simp: conj.commute eq_commute)
apply (rename_tac recvr q recv_state)
apply (rule_tac Q="\<lambda>_. valid_sched and scheduler_act_not thread and not_queued thread
and (\<lambda>s. recvr \<noteq> cur_thread s)
@ -2679,10 +2665,6 @@ lemma send_ipc_valid_sched:
done
end
crunch not_queued[wp]: thread_set "not_queued t"
crunch sched_act_not[wp]: thread_set "scheduler_act_not t"
lemma thread_set_tcb_fault_set_invs:
"valid_fault f \<Longrightarrow> \<lbrace>invs\<rbrace>
thread_set (tcb_fault_update (\<lambda>_. Some f)) t
@ -2903,10 +2885,6 @@ lemma reschedule_required_not_queued:
split: option.splits)
done
crunch sched_act_not[wp]: tcb_sched_action "scheduler_act_not t"
crunch not_queued[wp]: set_thread_state "not_queued t"
context DetSchedSchedule_AI begin
lemma cancel_all_ipc_not_queued:
"\<lbrace>st_tcb_at active t and valid_objs and not_queued t and scheduler_act_not t
@ -3037,7 +3015,7 @@ crunch is_etcb_at[wp]: setup_reply_master, cancel_ipc "is_etcb_at t"
(wp: hoare_drop_imps crunch_wps select_inv simp: crunch_simps unless_def)
end
crunch valid_etcbs[wp]: setup_reply_master "valid_etcbs"
crunch weak_valid_sched_action[wp]: setup_reply_master "weak_valid_sched_action"
crunch is_etcb_at_ext[wp]: set_thread_state_ext, tcb_sched_action,
@ -3084,8 +3062,6 @@ lemma opt_update_thread_simple_sched_action[wp]:
crunch ct_active[wp]: delete_caller_cap ct_active (wp: ct_in_state_thread_state_lift)
crunch valid_sched[wp]: lookup_cap valid_sched
lemma test:
"invs s \<longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> s \<turnstile> tcb_ctable (the (get_tcb thread s))"
apply (simp add: invs_valid_tcb_ctable_strengthen)
@ -3122,9 +3098,6 @@ end
crunch valid_sched[wp]: reply_from_kernel valid_sched
crunch etcb_at[wp]: cap_insert "\<lambda>s. etcb_at P t s"
(wp: crunch_wps simp: cap_insert_ext_def)
lemma set_thread_state_active_valid_sched:
"active st \<Longrightarrow>
\<lbrace>valid_sched and ct_active and (\<lambda>s. cur_thread s = ct)\<rbrace>
@ -3267,8 +3240,6 @@ crunch not_queued[wp]: set_thread_state_ext "not_queued t"
crunch ct_not_queued[wp]: set_thread_state ct_not_queued (wp: ct_not_queued_lift)
crunch valid_sched[wp]: lookup_cap_and_slot valid_sched
context DetSchedSchedule_AI begin
lemma handle_invocation_valid_sched:
"\<lbrace>invs and valid_sched and ct_active and

4
proof/invariant-abstract/Deterministic_AI.thy
View File

@ -4167,8 +4167,8 @@ lemma next_slot_setD:
(\<exists>p q. (slot \<in> descendants_of p m \<or> p = slot) \<and> q \<in> next_sib_set p t m \<and> next \<in> descendants_of q m \<union> {q})"
apply(subst(asm) next_slot_set_def)
apply(simp)
apply(induct_tac "next" slot rule: trancl.induct)
apply(assumption)
apply(induct "next" slot rule: trancl.induct)
apply simp
apply(simp add: next_slot_def split: if_split_asm)
apply(simp add: next_child_def valid_list_2_def descendants_of_def cdt_parent_defs)
apply(case_tac "t b", simp, fastforce)

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

@ -76,8 +76,7 @@ lemma cdt_detype[simp]:
lemma caps_of_state_detype[simp]:
"caps_of_state (detype S s) =
(\<lambda>p. if fst p \<in> S then None else caps_of_state s p)"
by (clarsimp simp add: caps_of_state_cte_wp_at
intro!: ext)
by (fastforce simp add: caps_of_state_cte_wp_at)
lemma state_refs_of_detype:
@ -829,7 +828,7 @@ lemma invariants:
(detype (untyped_range cap) (clear_um (untyped_range cap) s))"
using detype_invs_lemmas detype_invs_assms ct_act
by (simp add: invs_def valid_state_def valid_pspace_def
detype_clear_um_independent clear_um.state_refs_update clear_um.state_hyp_refs_update)
detype_clear_um_independent clear_um.state_refs_update)
end
@ -1065,7 +1064,7 @@ lemma corres_submonad2:
assert_def return_def bind_def)
apply (rule corres_split' [where r'="\<lambda>x y. (x, y) \<in> ssr",
OF _ _ gets_sp gets_sp])
apply (clarsimp simp: corres_gets)
apply clarsimp
apply (rule corres_split' [where r'="\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr",
OF _ _ hoare_post_taut hoare_post_taut])
defer
@ -1093,7 +1092,7 @@ lemma corres_submonad3:
assert_def return_def bind_def)
apply (rule corres_split' [where r'="\<lambda>x y. (x, y) \<in> ssr",
OF _ _ gets_sp gets_sp])
apply (clarsimp simp: corres_gets)
apply clarsimp
apply (rule corres_split' [where r'="\<lambda>(x, x') (y, y'). rvr x y \<and> (x', y') \<in> ssr",
OF _ _ hoare_post_taut hoare_post_taut])
defer

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

@ -961,8 +961,6 @@ lemma get_irq_slot_emptyable[wp]:
crunch (in Finalise_AI_2) invs[wp]: deleting_irq_handler "invs :: 'a state \<Rightarrow> bool"
crunch tcb_at[wp]: unbind_notification "tcb_at t"
locale Finalise_AI_3 = Finalise_AI_2 a b
for a :: "('a :: state_ext) itself"
@ -1086,8 +1084,6 @@ lemma fast_finalise_st_tcb_at:
apply (cases cap; wpsimp wp: cancel_all_ipc_st_tcb_at cancel_all_signals_st_tcb_at)
done
crunch st_tcb_at[wp]: empty_slot "st_tcb_at P t"
lemma cap_delete_one_st_tcb_at:
"\<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st)\<rbrace>
cap_delete_one ptr

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

@ -197,7 +197,7 @@ lemma update_restart_pc_has_reply_cap[wp]:
crunch st_tcb_at_simple[wp]: reply_cancel_ipc "st_tcb_at simple t"
(wp: crunch_wps select_wp sts_st_tcb_at_cases thread_set_no_change_tcb_state
simp: crunch_simps unless_def fast_finalise.simps)
simp: crunch_simps unless_def)
lemma cancel_ipc_simple [wp]:
"\<lbrace>\<top>\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>"
@ -772,7 +772,7 @@ lemma suspend_unlive:
\<lbrace>\<lambda>rv. obj_at (Not \<circ> live0) t\<rbrace>"
apply (simp add: suspend_def set_thread_state_def set_object_def get_object_def)
(* avoid creating two copies of obj_at *)
supply hoare_vcg_if_split[wp_split del] if_splits[split del]
supply hoare_vcg_if_split[wp_split del] if_split[split del]
apply (wp | simp only: obj_at_exst_update)+
apply (simp add: obj_at_def)
apply (rule_tac Q="\<lambda>_. bound_tcb_at ((=) None) t" in hoare_strengthen_post)
@ -816,8 +816,7 @@ lemma cancel_all_invs_helper:
apply (rule sts_st_tcb_at_cases, simp)
apply (strengthen reply_cap_doesnt_exist_strg)
apply (auto simp: valid_tcb_state_def idle_no_ex_cap o_def if_split_asm
elim!: rsubst[where P=sym_refs] st_tcb_weakenE
intro!: ext)
elim!: rsubst[where P=sym_refs] st_tcb_weakenE)
done
@ -950,10 +949,9 @@ lemma ntfn_bound_tcb_at:
\<Longrightarrow> bound_tcb_at P tcbptr s"
apply (drule_tac x=ntfnptr in sym_refsD[rotated])
apply (fastforce simp: state_refs_of_def)
apply (auto simp: pred_tcb_at_def obj_at_def valid_obj_def valid_ntfn_def is_tcb
state_refs_of_def refs_of_rev
simp del: refs_of_simps
elim!: valid_objsE)
apply (fastforce simp: pred_tcb_at_def obj_at_def valid_obj_def valid_ntfn_def is_tcb
state_refs_of_def refs_of_rev
simp del: refs_of_simps)
done
lemma bound_tcb_bound_notification_at:
@ -964,8 +962,7 @@ lemma bound_tcb_bound_notification_at:
apply (fastforce simp: state_refs_of_def pred_tcb_at_def obj_at_def)
apply (auto simp: pred_tcb_at_def obj_at_def valid_obj_def valid_ntfn_def is_tcb
state_refs_of_def refs_of_rev
simp del: refs_of_simps
elim!: valid_objsE)
simp del: refs_of_simps)
done
lemma unbind_notification_invs:

49
proof/invariant-abstract/Ipc_AI.thy
View File

@ -72,7 +72,7 @@ lemma get_recv_slot_inv[wp]:
lemma cte_wp_at_eq_simp:
"cte_wp_at ((=) cap) = cte_wp_at (\<lambda>c. c = cap)"
apply (rule arg_cong [where f=cte_wp_at])
apply (safe intro!: ext)
apply fastforce
done
lemma get_rs_cte_at[wp]:
@ -478,12 +478,12 @@ lemma cap_insert_cte_wp_at:
apply (clarsimp split:if_split_asm)
apply (clarsimp simp:cap_insert_def)
apply (wp set_cap_cte_wp_at | simp split del: if_split)+
apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_splits)
apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_split)
apply (wp get_cap_wp)+
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (clarsimp simp:cap_insert_def)
apply (wp set_cap_cte_wp_at | simp split del: if_split)+
apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_splits)
apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_split)
apply (wp set_cap_cte_wp_at get_cap_wp)+
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (frule(1) caps_of_state_valid)
@ -784,9 +784,6 @@ lemma (in Ipc_AI) tcl_ct[wp]:
\<lbrace>\<lambda>rv. cur_tcb\<rbrace>"
by (wp transfer_caps_loop_pres)
crunch it[wp]: cap_insert "\<lambda>s. P (idle_thread s)"
(wp: crunch_wps simp: crunch_simps)
lemma (in Ipc_AI) tcl_it[wp]:
"\<And>P ep buffer n caps slots mi.
\<lbrace>\<lambda>s::'state_ext state. P (idle_thread s)\<rbrace>
@ -1192,12 +1189,6 @@ end
(* FIXME: move *)
crunch valid_vspace_objs [wp]: set_extra_badge valid_vspace_objs
crunch vspace_objs [wp]: set_untyped_cap_as_full "valid_vspace_objs"
(wp: crunch_wps simp: crunch_simps ignore: set_object set_cap)
crunch vspace_objs [wp]: cap_insert "valid_vspace_objs"
(wp: crunch_wps simp: crunch_simps ignore: set_object set_cap)
lemma zipWith_append2:
"length ys + 1 < n \<Longrightarrow>
zipWith f [0 ..< n] (ys @ [y]) = zipWith f [0 ..< n] ys @ [f (length ys) y]"
@ -1457,13 +1448,6 @@ crunch "distinct" [wp]: copy_mrs pspace_distinct
(wp: mapM_wp' simp: copy_mrs_redux)
crunch mdb [wp]: store_word_offs valid_mdb (wp: crunch_wps simp: crunch_simps)
crunch caps_of_state [wp]: store_word_offs "\<lambda>s. P (caps_of_state s)"
(wp: crunch_wps simp: crunch_simps)
crunch mdb_P [wp]: set_mrs "\<lambda>s. P (cdt s)"
(wp: crunch_wps simp: crunch_simps zipWithM_x_mapM)
@ -1788,8 +1772,6 @@ context Ipc_AI begin
crunch only_idle [wp]: do_ipc_transfer "only_idle :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: crunch_simps)
crunch valid_global_vspace_mappings [wp]: set_extra_badge valid_global_vspace_mappings
crunch pspace_in_kernel_window[wp]: do_ipc_transfer "pspace_in_kernel_window :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: crunch_simps)
@ -2070,8 +2052,7 @@ lemma update_waiting_invs:
apply (frule ko_at_state_refs_ofD)
apply (frule st_tcb_at_state_refs_ofD)
apply (erule(1) obj_at_valid_objsE)
apply (clarsimp simp: valid_obj_def valid_ntfn_def obj_at_def is_ntfn_def
split del: if_split)
apply (clarsimp simp: valid_obj_def valid_ntfn_def obj_at_def is_ntfn_def)
apply (rule conjI, clarsimp simp: obj_at_def split: option.splits list.splits)
apply (rule conjI, clarsimp elim!: pred_tcb_weakenE)
apply (rule conjI, clarsimp dest!: idle_no_ex_cap)
@ -2080,8 +2061,8 @@ lemma update_waiting_invs:
split: if_split_asm if_split)
apply (simp only: tcb_bound_refs_eq_restr, simp)
apply (fastforce dest!: refs_in_ntfn_bound_refs symreftype_inverse'
elim!: valid_objsE simp: valid_obj_def valid_ntfn_def obj_at_def is_tcb
split: if_split_asm if_split)
simp: valid_obj_def valid_ntfn_def obj_at_def is_tcb
split: if_split_asm)
apply (clarsimp elim!: pred_tcb_weakenE)
done
@ -2144,10 +2125,6 @@ lemma cancel_ipc_cte_wp_at_not_reply_state:
done
crunch idle[wp]: cancel_ipc "\<lambda>s. P (idle_thread s)"
(wp: crunch_wps select_wp simp: crunch_simps unless_def)
lemma sai_invs[wp]:
"\<lbrace>invs and ex_nonz_cap_to ntfn\<rbrace> send_signal ntfn bdg \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: send_signal_def)
@ -2615,12 +2592,6 @@ crunch cap_refs_respects_device_region[wp]: copy_mrs "cap_refs_respects_device_r
VSpace_AI.cap_refs_respects_device_region_dmo ball_tcb_cap_casesI
const_on_failure_wp simp: crunch_simps zipWithM_x_mapM ball_conj_distrib)
crunch cap_refs_respects_device_region[wp]: get_receive_slots "cap_refs_respects_device_region"
(wp: crunch_wps hoare_vcg_const_Ball_lift
VSpace_AI.cap_refs_respects_device_region_dmo ball_tcb_cap_casesI
const_on_failure_wp simp: crunch_simps zipWithM_x_mapM )
lemma invs_respects_device_region:
"invs s \<Longrightarrow> cap_refs_respects_device_region s \<and> pspace_respects_device_region s"
@ -2985,14 +2956,6 @@ end
crunch cap_to[wp]: receive_signal "ex_nonz_cap_to p"
(wp: crunch_wps)
crunch ex_nonz_cap_to[wp]: set_message_info "ex_nonz_cap_to p"
lemma is_derived_not_Null [simp]:
"\<not>is_derived m p c NullCap"
by (auto simp add: is_derived_def cap_master_cap_simps dest: cap_master_cap_eqDs)
crunch mdb[wp]: set_message_info valid_mdb
(wp: select_wp crunch_wps mapM_wp')

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

@ -669,9 +669,6 @@ lemma set_object_cap_refs_respects_device_region:
done
crunch no_revokable[wp]: set_simple_ko "\<lambda>s. P (is_original_cap s)"
(wp: crunch_wps)
lemma get_object_ret:
"\<lbrace>obj_at P addr\<rbrace> get_object addr \<lbrace>\<lambda>r s. P r\<rbrace>"
unfolding get_object_def
@ -1162,8 +1159,6 @@ lemmas set_simple_ko_valid_irq_handlers[wp]
= valid_irq_handlers_lift [OF set_simple_ko_caps_of_state set_simple_ko_interrupt_states]
crunch irq_node[wp]: set_simple_ko "\<lambda>s. P (interrupt_irq_node s)"
lemmas hoare_use_eq_irq_node = hoare_use_eq[where f=interrupt_irq_node]
@ -1177,9 +1172,6 @@ lemmas cap_table_at_lift_irq =
hoare_use_eq_irq_node [OF _ cap_table_at_lift_valid]
crunch interrupt_states[wp]: set_notification "\<lambda>s. P (interrupt_states s)"
(wp: crunch_wps)
lemma set_simple_ko_only_idle [wp]:
"set_simple_ko f p ntfn \<lbrace>only_idle\<rbrace>"
by (wp only_idle_lift)
@ -1199,10 +1191,6 @@ lemma set_simple_ko_cap_refs_respects_device_region[wp]:
simp_thm: is_ep_def is_ntfn_def)
crunch v_ker_map[wp]: set_simple_ko "valid_kernel_mappings"
(ignore: set_object wp: set_object_v_ker_map crunch_wps simp: set_simple_ko_def)
(* There are two wp rules for preserving valid_ioc over set_object.
First, the more involved rule for CNodes and TCBs *)
lemma set_object_valid_ioc_caps:
@ -1298,8 +1286,6 @@ lemma set_ntfn_minor_invs:
dest!: obj_at_state_refs_ofD)
done
crunch asid_map[wp]: set_bound_notification "valid_asid_map"
lemma do_machine_op_result[wp]:
"\<lbrace>P\<rbrace> mop \<lbrace>\<lambda>rv s. Q rv\<rbrace> \<Longrightarrow>
\<lbrace>\<lambda>s. P (machine_state s)\<rbrace> do_machine_op mop \<lbrace>\<lambda>rv s. Q rv\<rbrace>"

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

@ -478,7 +478,7 @@ proof -
show "x \<in> {x .. x + (2 ^ obj_bits ko - 1)}"
proof (rule base_member_set)
from vp show "is_aligned x (obj_bits ko)" using ps'
by (auto elim!: valid_pspaceE pspace_alignedE)
by (auto elim!: valid_pspaceE)
show "obj_bits ko < len_of TYPE(machine_word_len)"
by (rule valid_pspace_obj_sizes [OF _ ranI, unfolded word_bits_def]) fact+
qed
@ -918,8 +918,6 @@ locale Retype_AI_dmo_eq_kernel_restricted =
crunch only_idle[wp]: do_machine_op "only_idle"
crunch valid_global_refs[wp]: do_machine_op "valid_global_refs"
crunch global_mappings[wp]: do_machine_op "valid_global_vspace_mappings"
crunch valid_kernel_mappings[wp]: do_machine_op "valid_kernel_mappings"
crunch cap_refs_in_kernel_window[wp]: do_machine_op "cap_refs_in_kernel_window"
@ -1032,8 +1030,7 @@ lemma unsafe_rep2:
apply (subst P_null_filter_caps_of_cte_wp_at, simp)+
apply (simp add: null_filter_same [where cps="caps_of_state s" for s, OF cte_wp_at_not_Null])
apply (fastforce simp: if_unsafe_then_cap2_def cte_wp_at_caps_of_state
if_unsafe_then_cap_def ex_cte_cap_wp_to_def
intro!: ext)
if_unsafe_then_cap_def ex_cte_cap_wp_to_def)
done
@ -1114,10 +1111,10 @@ lemma valid_mdb_rep2:
apply (rule arg_cong2 [where f="(\<and>)"])
apply (simp add: reply_caps_mdb_def
del: split_paired_Ex split_paired_All)
apply (fastforce intro!: iffI elim!: allEI exEI
apply (fastforce elim!: allEI exEI
simp del: split_paired_Ex split_paired_All)
apply (rule arg_cong2 [where f="(\<and>)"])
apply (fastforce simp: reply_masters_mdb_def intro!: iffI elim!: allEI
apply (fastforce simp: reply_masters_mdb_def elim!: allEI
simp del: split_paired_All split: if_split_asm)
apply (fastforce simp: valid_arch_mdb_null_filter[simplified null_filter_def])
apply (rule arg_cong[where f=All, OF ext])+

9
proof/invariant-abstract/Syscall_AI.thy
View File

@ -130,8 +130,6 @@ where
| "valid_invocation (InvokeArchObject i) = valid_arch_inv i"
crunch inv [wp]: lookup_cap_and_slot P
lemma sts_Restart_invs[wp]:
"\<lbrace>st_tcb_at active t and invs and ex_nonz_cap_to t\<rbrace>
set_thread_state t Structures_A.Restart
@ -274,9 +272,6 @@ lemma do_ipc_transfer_emptyable[wp]:
apply (wp hoare_convert_imp | clarsimp)+
done
crunch emptyable[wp]: do_ipc_transfer "emptyable sl"
lemma do_ipc_transfer_non_null_cte_wp_at2:
fixes P
assumes PNN: "\<And>cap. P cap \<Longrightarrow> cap \<noteq> cap.NullCap"
@ -1207,8 +1202,6 @@ lemmas (in Syscall_AI) hr_ct_in_state_simple[wp]
= ct_in_state_thread_state_lift [OF handle_reply_cur_thread
handle_reply_st_tcb_at_simple]
crunch (in Syscall_AI) nonz_cap_to[wp]: handle_fault_reply "ex_nonz_cap_to p :: 'state_ext state \<Rightarrow> _"
crunch (in Syscall_AI) vo[wp]: handle_fault_reply "valid_objs :: 'state_ext state \<Rightarrow> _"
lemmas handle_fault_reply_typ_ats[wp] =
@ -1391,7 +1384,7 @@ lemma send_ipc_st_tcb_at_runnable:
apply (rule conjI)
apply (wpc
| wp sts_st_tcb_at_other dxo_wp_weak hoare_drop_imps
| clarsimp simp: if_cancel if_fun_split)+
| clarsimp simp: if_fun_split)+
apply (wp get_simple_ko_wp)
apply clarsimp
apply (drule st_tcb_at_state_refs_ofD)

8
proof/invariant-abstract/TcbAcc_AI.thy
View File

@ -307,8 +307,6 @@ lemma thread_set_valid_idle_trivial:
crunch it [wp]: thread_set "\<lambda>s. P (idle_thread s)"
crunch arch [wp]: thread_set "\<lambda>s. P (arch_state s)"
lemma thread_set_caps_of_state_trivial:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
@ -852,8 +850,6 @@ lemma fold_fun_upd:
apply clarsimp
done
crunch obj_at[wp]: store_word_offs "\<lambda>s. P (obj_at Q p s)"
lemma load_word_offs_P[wp]:
"\<lbrace>P\<rbrace> load_word_offs a x \<lbrace>\<lambda>_. P\<rbrace>"
unfolding load_word_offs_def
@ -1313,8 +1309,6 @@ lemma set_bound_notification_global_refs [wp]:
apply (wp thread_set_global_refs_triv|clarsimp simp: tcb_cap_cases_def)+
done
crunch arch [wp]: set_thread_state, set_bound_notification "\<lambda>s. P (arch_state s)"
lemma st_tcb_ex_cap:
"\<lbrakk> st_tcb_at P t s; if_live_then_nonz_cap s;
@ -1624,8 +1618,6 @@ lemma set_thread_state_cte_at:
"\<lbrace>cte_at p\<rbrace> set_thread_state x st \<lbrace>\<lambda>rv. cte_at p\<rbrace>"
by (rule set_thread_state_cte_wp_at)
crunch cte_at: set_bound_notification "cte_at p"
lemma as_user_mdb [wp]:
"\<lbrace>valid_mdb\<rbrace> as_user f t \<lbrace>\<lambda>_. valid_mdb\<rbrace>"

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

@ -137,8 +137,6 @@ lemma restart_invs[wp]:
apply (auto dest!: idle_no_ex_cap simp: invs_def valid_state_def valid_pspace_def)
done
crunch typ_at[wp]: setup_reply_master "\<lambda>s. P (typ_at T p s)"
lemma restart_typ_at[wp]:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> Tcb_A.restart t \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
by (wpsimp simp: Tcb_A.restart_def wp: cancel_ipc_typ_at)
@ -403,15 +401,7 @@ lemma tcb_cap_always_valid_strg:
by (clarsimp simp: tcb_cap_valid_def st_tcb_def2 tcb_at_def
split: option.split_asm)
lemma thread_set_emptyable[wp]:
assumes x: "\<And>tcb. tcb_state (fn tcb) = tcb_state tcb"
shows "\<lbrace>emptyable sl\<rbrace> thread_set fn p \<lbrace>\<lambda>rv. emptyable sl\<rbrace>"
by (wp emptyable_lift x thread_set_no_change_tcb_state)
crunch not_cte_wp_at[wp]: unbind_maybe_notification "\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp"
(wp: thread_set_caps_of_state_trivial simp: tcb_cap_cases_def)
declare thread_set_emptyable[wp]
lemma (in Tcb_AI_1) rec_del_all_caps_in_range:
assumes x: "P cap.NullCap"
@ -1262,7 +1252,7 @@ lemma decode_tcb_inv_wf:
\<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace>
decode_tcb_invocation label args (cap.ThreadCap t) slot extras
\<lbrace>tcb_inv_wf\<rbrace>,-"
apply (simp add: decode_tcb_invocation_def Let_def del: tcb_inv_wf_def
apply (simp add: decode_tcb_invocation_def Let_def
cong: if_cong split del: if_split)
apply (rule hoare_vcg_precond_impE_R)
apply wpc

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

@ -576,7 +576,7 @@ lemma cte_wp_at_caps_descendants_range_inI:
apply (drule untyped_cap_descendants_range[rotated])
apply simp+
apply (simp add: invs_valid_pspace)
apply (clarsimp simp: cte_wp_at_caps_of_state usable_untyped_range.simps)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (erule disjoint_subset2[rotated])
apply clarsimp
apply (rule le_plus'[OF word_and_le2])
@ -744,7 +744,7 @@ lemma pspace_no_overlap_detype:
\<Longrightarrow> pspace_no_overlap_range_cover ptr bits (detype {ptr .. ptr + 2 ^ bits - 1} s)"
apply (drule(2) pspace_no_overlap_detype'[rotated])
apply (drule valid_cap_aligned)
apply (clarsimp simp: cap_aligned_def is_aligned_neg_mask_eq field_simps)
apply (clarsimp simp: cap_aligned_def field_simps)
done
lemma zip_take_length[simp]:
@ -810,8 +810,6 @@ lemma not_waiting_reply_slot_no_descendants:
done
crunch irq_node[wp]: set_thread_state "\<lambda>s. P (interrupt_irq_node s)"
crunch irq_states[wp]: update_cdt "\<lambda>s. P (interrupt_states s)"
crunch ups[wp]: set_cdt "\<lambda>s. P (ups_of_heap (kheap s))"
crunch cns[wp]: set_cdt "\<lambda>s. P (cns_of_heap (kheap s))"
@ -828,14 +826,6 @@ lemma list_all2_zip_split:
apply (case_tac ds; simp)
done
crunch irq_states[wp]: update_cdt "\<lambda>s. P (interrupt_states s)"
crunch ups[wp]: set_cdt "\<lambda>s. P (ups_of_heap (kheap s))"
crunch cns[wp]: set_cdt "\<lambda>s. P (cns_of_heap (kheap s))"
lemma set_cdt_tcb_valid[wp]:
"\<lbrace>tcb_cap_valid cap ptr\<rbrace> set_cdt m \<lbrace>\<lambda>rv. tcb_cap_valid cap ptr\<rbrace>"
by (simp add: set_cdt_def, wp, simp add: tcb_cap_valid_def)
@ -1588,7 +1578,6 @@ 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)"
lemmas dmo_valid_cap[wp] = valid_cap_typ [OF do_machine_op_obj_at]
@ -1784,7 +1773,7 @@ lemma set_cap_valid_mdb_simple:
assume "reply_caps_mdb (cdt s) (caps_of_state s)"
thus "reply_caps_mdb (cdt s) (caps_of_state s(cref \<mapsto> cap.UntypedCap dev r bits idx))"
using cstate
apply (simp add: reply_caps_mdb_def del: split_paired_All split_paired_Ex)
apply (simp add: reply_caps_mdb_def del: split_paired_All)
apply (intro allI impI conjI)
apply (drule spec)+
apply (erule(1) impE)
@ -1794,7 +1783,7 @@ lemma set_cap_valid_mdb_simple:
done
assume "reply_masters_mdb (cdt s) (caps_of_state s)"
thus "reply_masters_mdb (cdt s) (caps_of_state s(cref \<mapsto> cap.UntypedCap dev r bits idx))"
apply (simp add: reply_masters_mdb_def del: split_paired_All split_paired_Ex)
apply (simp add: reply_masters_mdb_def del: split_paired_All)
apply (intro allI impI ballI)
apply (erule exE)
apply (elim allE impE)
@ -1834,7 +1823,7 @@ lemma set_free_index_valid_pspace_simple:
apply (elim allE allE impE)
apply simp+
apply (drule(1) pspace_no_overlap_obj_range)
apply (simp add: is_aligned_neg_mask_eq field_simps)
apply (simp add: field_simps)
apply (clarsimp simp add: pred_tcb_at_def tcb_cap_valid_def obj_at_def is_tcb
valid_ipc_buffer_cap_def split: option.split)
apply (drule(2) tcb_cap_slot_regular)
@ -1929,7 +1918,7 @@ lemma set_cap_caps_no_overlap:
lemma caps_overlap_reserved_detype:
"caps_overlap_reserved S s \<Longrightarrow> caps_overlap_reserved S (detype H s)"
apply (clarsimp simp: caps_of_state_detype caps_overlap_reserved_def )
apply (clarsimp simp: caps_overlap_reserved_def )
apply (erule ranE)
apply (clarsimp split: if_splits)
apply (drule bspec)
@ -1940,7 +1929,7 @@ lemma caps_overlap_reserved_detype:
lemma caps_no_overlap_detype:
"caps_no_overlap ptr sz s \<Longrightarrow> caps_no_overlap ptr sz (detype H s)"
apply (clarsimp simp: caps_of_state_detype caps_no_overlap_def)
apply (clarsimp simp: caps_no_overlap_def)
apply (erule ranE)
apply (clarsimp split: if_splits)
apply (drule bspec,fastforce)
@ -2420,8 +2409,7 @@ lemma valid_untyped_cap_inc:
apply (rule word_of_nat_le)
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=machine_word_len, folded word_bits_def])
apply (simp add: word_less_nat_alt)
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)
@ -2611,7 +2599,7 @@ proof -
apply (simp add: exI[where x=0])
apply (rule exI[where x="?al"])
apply (strengthen filter_upt_eq)
apply (simp add: linorder_not_less conj_ac)
apply (simp add: linorder_not_less conj.commute)
apply (simp add: alignUp_ge_nat[simplified] sub1[simplified]
sub1[THEN order_less_imp_le, simplified]
power_minus_is_div[OF b] le1 le2)
@ -2820,8 +2808,7 @@ lemma reset_untyped_cap_invs_etc:
| wp (once) ct_in_state_thread_state_lift
| (rule irq_state_independent_A_def[THEN meta_eq_to_obj_eq, THEN iffD2],
simp add: ex_cte_cap_wp_to_def ct_in_state_def))+
apply (clarsimp simp: is_aligned_neg_mask_eq bits_of_def field_simps
cte_wp_at_caps_of_state nth_rev)
apply (clarsimp simp: bits_of_def field_simps cte_wp_at_caps_of_state nth_rev)
apply (strengthen order_trans[where z="2 ^ sz", rotated, mk_strg I E])
apply (clarsimp split: if_split_asm)
apply auto[1]
@ -3412,12 +3399,6 @@ lemma cap_to_protected:
apply auto
done
lemma valid_cap_aligned:
"valid_cap cap s \<Longrightarrow> cap_aligned cap"
by (simp add: valid_cap_def)
crunch irq_node[wp]: do_machine_op "\<lambda>s. P (interrupt_irq_node s)"
(* FIXME: move *)
lemma ge_mask_eq: "len_of TYPE('a) \<le> n \<Longrightarrow> (x::'a::len word) && mask n = x"
by (simp add: mask_def p2_eq_0[THEN iffD2])