From 57d03332046fd9ed59b43ee95db132232ff1f416 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 18 Jan 2022 11:20:54 +1100 Subject: [PATCH] cleanup ainvs: reduce warnings Signed-off-by: Gerwin Klein --- proof/invariant-abstract/CNodeInv_AI.thy | 14 +----- proof/invariant-abstract/CSpaceInv_AI.thy | 3 -- proof/invariant-abstract/CSpace_AI.thy | 50 ++++++++----------- .../DetSchedDomainTime_AI.thy | 14 ------ proof/invariant-abstract/DetSchedInvs_AI.thy | 3 +- .../DetSchedSchedule_AI.thy | 33 +----------- proof/invariant-abstract/Deterministic_AI.thy | 4 +- proof/invariant-abstract/Detype_AI.thy | 9 ++-- proof/invariant-abstract/Finalise_AI.thy | 4 -- proof/invariant-abstract/IpcCancel_AI.thy | 17 +++---- proof/invariant-abstract/Ipc_AI.thy | 49 +++--------------- proof/invariant-abstract/KHeap_AI.thy | 14 ------ proof/invariant-abstract/Retype_AI.thy | 11 ++-- proof/invariant-abstract/Syscall_AI.thy | 9 +--- proof/invariant-abstract/TcbAcc_AI.thy | 8 --- proof/invariant-abstract/Tcb_AI.thy | 14 +----- proof/invariant-abstract/Untyped_AI.thy | 39 ++++----------- 17 files changed, 62 insertions(+), 233 deletions(-) diff --git a/proof/invariant-abstract/CNodeInv_AI.thy b/proof/invariant-abstract/CNodeInv_AI.thy index 781473f24..9ea1ca732 100644 --- a/proof/invariant-abstract/CNodeInv_AI.thy +++ b/proof/invariant-abstract/CNodeInv_AI.thy @@ -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 "\s. revoke_progress_ord m (\x. opti wp: hoare_drop_imps empty_slot_rvk_prog' select_wp thread_set_caps_of_state_trivial) -crunch rvk_prog: cancel_all_ipc "\s. revoke_progress_ord m (\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 "\s. revoke_progress_ord m (\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 "\s. revoke_progress_ord m (\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) diff --git a/proof/invariant-abstract/CSpaceInv_AI.thy b/proof/invariant-abstract/CSpaceInv_AI.thy index 3bd69dc5f..b15a6e475 100644 --- a/proof/invariant-abstract/CSpaceInv_AI.thy +++ b/proof/invariant-abstract/CSpaceInv_AI.thy @@ -102,9 +102,6 @@ crunch inv[wp]: get_cap "P" (simp: crunch_simps) -declare resolve_address_bits'.simps [simp del] - - lemma rab_inv[wp]: "\P\ resolve_address_bits slot \\rv. P\" unfolding resolve_address_bits_def diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy index adbd61728..904ca7a76 100644 --- a/proof/invariant-abstract/CSpace_AI.thy +++ b/proof/invariant-abstract/CSpace_AI.thy @@ -57,7 +57,7 @@ lemma capBadge_ordefield_simps[simp]: "((y, y) \ capBadge_ordering fb) = (fb \ (y = None \ y = Some 0))" "((Some x, Some z) \ capBadge_ordering fb) = (x = 0 \ (\ fb \ x = z))" "(y, Some 0) \ capBadge_ordering fb = (y = None \ 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]: "\ valid_objs \ get_cap addr \ valid_cap \" 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: \\s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \ cte_wp_at ((=) src_cap) src s\ set_untyped_cap_as_full src_cap cap src \\rv s'. mdb_cte_at (swp (cte_wp_at P) s') (cdt s') \" - 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]: "\\s. P (is_original_cap s)\ set_untyped_cap_as_full src_cap cap src \\rv s'. P (is_original_cap s') \" - 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 \ cap, src \ 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 "\s. P (global_refs s)" - - lemma set_untyped_cap_as_full_valid_global_refs[wp]: "\valid_global_refs and cte_wp_at ((=) src_cap) src\ 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]: diff --git a/proof/invariant-abstract/DetSchedDomainTime_AI.thy b/proof/invariant-abstract/DetSchedDomainTime_AI.thy index adf0ddca3..f4e235930 100644 --- a/proof/invariant-abstract/DetSchedDomainTime_AI.thy +++ b/proof/invariant-abstract/DetSchedDomainTime_AI.thy @@ -151,8 +151,6 @@ context DetSchedDomainTime_AI begin crunch domain_list_inv[wp]: do_ipc_transfer "\s. P (domain_list s)" (wp: crunch_wps simp: zipWithM_x_mapM rule: transfer_caps_loop_pres) -crunch domain_list_inv[wp]: copy_mrs "\s. P (domain_list s)" - crunch domain_list_inv[wp]: handle_fault "\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 "\s. P (domain_list s)" - (wp: crunch_wps check_cap_inv) - -crunch (in DetSchedDomainTime_AI_2) domain_list_inv[wp]: handle_interrupt "\s. P (domain_list s)" - crunch domain_list_inv[wp]: cap_move "\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 "\s. P (domain_time s)" (wp: crunch_wps simp: zipWithM_x_mapM rule: transfer_caps_loop_pres) -crunch domain_time_inv[wp]: copy_mrs "\s. P (domain_time s)" - crunch domain_time_inv[wp]: handle_fault "\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 "\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: diff --git a/proof/invariant-abstract/DetSchedInvs_AI.thy b/proof/invariant-abstract/DetSchedInvs_AI.thy index caa43d9f6..e80655d12 100644 --- a/proof/invariant-abstract/DetSchedInvs_AI.thy +++ b/proof/invariant-abstract/DetSchedInvs_AI.thy @@ -407,7 +407,8 @@ lemma valid_etcbs_tcb_etcb: lemma valid_etcbs_get_tcb_get_etcb: "\ valid_etcbs s; get_tcb ptr s = Some tcb \ \ \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 diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 775e164c6..076c14dee 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -196,8 +196,6 @@ abbreviation valid_sched_except_blocked_2 where abbreviation valid_sched_except_blocked :: "det_ext state \ bool" where "valid_sched_except_blocked s \ 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: "\valid_sched\ set_bound_notification ref ntfn \\_. valid_sched\" apply (simp add: valid_sched_def | wp set_bound_notification_valid_queues @@ -1108,8 +1104,6 @@ lemma tcb_sched_action_lift: \ \P\ tcb_sched_action a b \\_. P\" 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 \ (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: "\valid_sched and ct_not_queued and (\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]: "\valid_sched\ cancel_all_signals ntfnptr \\rv. valid_sched\" 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 "\s :: det_ext state. P (scheduler_action s)" crunch scheduler_act[wp]: set_extra_badge,cap_insert "\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 "\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 "\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 "\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="\_. valid_sched and scheduler_act_not thread and not_queued thread and (\s. recvr \ 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 \ \invs\ thread_set (tcb_fault_update (\_. 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: "\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 \ (\y. get_tcb thread s = Some y) \ s \ 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 "\s. etcb_at P t s" - (wp: crunch_wps simp: cap_insert_ext_def) - lemma set_thread_state_active_valid_sched: "active st \ \valid_sched and ct_active and (\s. cur_thread s = ct)\ @@ -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: "\invs and valid_sched and ct_active and diff --git a/proof/invariant-abstract/Deterministic_AI.thy b/proof/invariant-abstract/Deterministic_AI.thy index e426bfbed..f127c88ad 100644 --- a/proof/invariant-abstract/Deterministic_AI.thy +++ b/proof/invariant-abstract/Deterministic_AI.thy @@ -4167,8 +4167,8 @@ lemma next_slot_setD: (\p q. (slot \ descendants_of p m \ p = slot) \ q \ next_sib_set p t m \ next \ descendants_of q m \ {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) diff --git a/proof/invariant-abstract/Detype_AI.thy b/proof/invariant-abstract/Detype_AI.thy index 7d8d451e1..d133d9ec3 100644 --- a/proof/invariant-abstract/Detype_AI.thy +++ b/proof/invariant-abstract/Detype_AI.thy @@ -76,8 +76,7 @@ lemma cdt_detype[simp]: lemma caps_of_state_detype[simp]: "caps_of_state (detype S s) = (\p. if fst p \ 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'="\x y. (x, y) \ ssr", OF _ _ gets_sp gets_sp]) - apply (clarsimp simp: corres_gets) + apply clarsimp apply (rule corres_split' [where r'="\(x, x') (y, y'). rvr x y \ (x', y') \ 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'="\x y. (x, y) \ ssr", OF _ _ gets_sp gets_sp]) - apply (clarsimp simp: corres_gets) + apply clarsimp apply (rule corres_split' [where r'="\(x, x') (y, y'). rvr x y \ (x', y') \ ssr", OF _ _ hoare_post_taut hoare_post_taut]) defer diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index 23afa912d..bef35e561 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -961,8 +961,6 @@ lemma get_irq_slot_emptyable[wp]: crunch (in Finalise_AI_2) invs[wp]: deleting_irq_handler "invs :: 'a state \ 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: "\st_tcb_at P t and K (\st. active st \ P st)\ cap_delete_one ptr diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index 2e3fc099e..9261e1ab2 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -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]: "\\\ cancel_ipc t \\rv. st_tcb_at simple t\" @@ -772,7 +772,7 @@ lemma suspend_unlive: \\rv. obj_at (Not \ live0) t\" 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="\_. 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: \ 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: diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy index e0d2336ce..f5299fac1 100644 --- a/proof/invariant-abstract/Ipc_AI.thy +++ b/proof/invariant-abstract/Ipc_AI.thy @@ -72,7 +72,7 @@ lemma get_recv_slot_inv[wp]: lemma cte_wp_at_eq_simp: "cte_wp_at ((=) cap) = cte_wp_at (\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]: \\rv. cur_tcb\" by (wp transfer_caps_loop_pres) -crunch it[wp]: cap_insert "\s. P (idle_thread s)" - (wp: crunch_wps simp: crunch_simps) - lemma (in Ipc_AI) tcl_it[wp]: "\P ep buffer n caps slots mi. \\s::'state_ext state. P (idle_thread s)\ @@ -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 \ 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 "\s. P (caps_of_state s)" - (wp: crunch_wps simp: crunch_simps) - - crunch mdb_P [wp]: set_mrs "\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 \ 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 \ 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 "\s. P (idle_thread s)" - (wp: crunch_wps select_wp simp: crunch_simps unless_def) - - lemma sai_invs[wp]: "\invs and ex_nonz_cap_to ntfn\ send_signal ntfn bdg \\rv. invs\" 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 \ cap_refs_respects_device_region s \ 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]: - "\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') diff --git a/proof/invariant-abstract/KHeap_AI.thy b/proof/invariant-abstract/KHeap_AI.thy index 3a3fac1df..8b71a71ff 100644 --- a/proof/invariant-abstract/KHeap_AI.thy +++ b/proof/invariant-abstract/KHeap_AI.thy @@ -669,9 +669,6 @@ lemma set_object_cap_refs_respects_device_region: done -crunch no_revokable[wp]: set_simple_ko "\s. P (is_original_cap s)" - (wp: crunch_wps) - lemma get_object_ret: "\obj_at P addr\ get_object addr \\r s. P r\" 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 "\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 "\s. P (interrupt_states s)" - (wp: crunch_wps) - lemma set_simple_ko_only_idle [wp]: "set_simple_ko f p ntfn \only_idle\" 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]: "\P\ mop \\rv s. Q rv\ \ \\s. P (machine_state s)\ do_machine_op mop \\rv s. Q rv\" diff --git a/proof/invariant-abstract/Retype_AI.thy b/proof/invariant-abstract/Retype_AI.thy index d08e3573a..c559d3fe4 100644 --- a/proof/invariant-abstract/Retype_AI.thy +++ b/proof/invariant-abstract/Retype_AI.thy @@ -478,7 +478,7 @@ proof - show "x \ {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="(\)"]) 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="(\)"]) - 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])+ diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index 93093b8b7..9e9f1fcee 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -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]: "\st_tcb_at active t and invs and ex_nonz_cap_to t\ 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: "\cap. P cap \ cap \ 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 \ _" - crunch (in Syscall_AI) vo[wp]: handle_fault_reply "valid_objs :: 'state_ext state \ _" 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) diff --git a/proof/invariant-abstract/TcbAcc_AI.thy b/proof/invariant-abstract/TcbAcc_AI.thy index 7fcf42425..5bf505502 100644 --- a/proof/invariant-abstract/TcbAcc_AI.thy +++ b/proof/invariant-abstract/TcbAcc_AI.thy @@ -307,8 +307,6 @@ lemma thread_set_valid_idle_trivial: crunch it [wp]: thread_set "\s. P (idle_thread s)" -crunch arch [wp]: thread_set "\s. P (arch_state s)" - lemma thread_set_caps_of_state_trivial: assumes x: "\tcb. \(getF, v) \ ran tcb_cap_cases. @@ -852,8 +850,6 @@ lemma fold_fun_upd: apply clarsimp done -crunch obj_at[wp]: store_word_offs "\s. P (obj_at Q p s)" - lemma load_word_offs_P[wp]: "\P\ load_word_offs a x \\_. P\" 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 "\s. P (arch_state s)" - lemma st_tcb_ex_cap: "\ st_tcb_at P t s; if_live_then_nonz_cap s; @@ -1624,8 +1618,6 @@ lemma set_thread_state_cte_at: "\cte_at p\ set_thread_state x st \\rv. cte_at p\" by (rule set_thread_state_cte_wp_at) -crunch cte_at: set_bound_notification "cte_at p" - lemma as_user_mdb [wp]: "\valid_mdb\ as_user f t \\_. valid_mdb\" diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index b0f015089..d40c12b1a 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -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 "\s. P (typ_at T p s)" - lemma restart_typ_at[wp]: "\\s. P (typ_at T p s)\ Tcb_A.restart t \\rv s. P (typ_at T p s)\" 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: "\tcb. tcb_state (fn tcb) = tcb_state tcb" - shows "\emptyable sl\ thread_set fn p \\rv. emptyable sl\" - by (wp emptyable_lift x thread_set_no_change_tcb_state) - - -crunch not_cte_wp_at[wp]: unbind_maybe_notification "\s. \cp\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: \ no_cap_to_obj_dr_emp (fst x) s)\ decode_tcb_invocation label args (cap.ThreadCap t) slot extras \tcb_inv_wf\,-" - 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 diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index eb9187f0c..539fea24f 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -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: \ 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 "\s. P (interrupt_irq_node s)" -crunch irq_states[wp]: update_cdt "\s. P (interrupt_states s)" crunch ups[wp]: set_cdt "\s. P (ups_of_heap (kheap s))" crunch cns[wp]: set_cdt "\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 "\s. P (interrupt_states s)" - -crunch ups[wp]: set_cdt "\s. P (ups_of_heap (kheap s))" - -crunch cns[wp]: set_cdt "\s. P (cns_of_heap (kheap s))" - - lemma set_cdt_tcb_valid[wp]: "\tcb_cap_valid cap ptr\ set_cdt m \\rv. tcb_cap_valid cap ptr\" 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 "\s. P (cdt s)" -crunch cte_wp_at[wp]: do_machine_op "\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 \ 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 \ 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 \ 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 \ 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 \ cap_aligned cap" - by (simp add: valid_cap_def) - -crunch irq_node[wp]: do_machine_op "\s. P (interrupt_irq_node s)" - (* FIXME: move *) lemma ge_mask_eq: "len_of TYPE('a) \ n \ (x::'a::len word) && mask n = x" by (simp add: mask_def p2_eq_0[THEN iffD2])