diff --git a/proof/capDL-api/Arch_DP.thy b/proof/capDL-api/Arch_DP.thy index 10b0d039c..2f6f08c0f 100644 --- a/proof/capDL-api/Arch_DP.thy +++ b/proof/capDL-api/Arch_DP.thy @@ -63,16 +63,13 @@ lemma decode_page_map_intent_rv_20_24: [(PageDirectoryCap ptr real' asid',pdref)] (PageIntent (PageMapIntent vaddr perms vmattr)) \\r s. R r\, -" - apply (simp add:decode_invocation_def get_index_def - get_page_intent_def throw_opt_def cap_rights_def - decode_page_invocation_def throw_on_none_def get_mapped_asid_def) + apply (simp add: decode_invocation_def get_index_def get_page_intent_def throw_opt_def + cap_rights_def decode_page_invocation_def throw_on_none_def get_mapped_asid_def) apply (wp alternativeE_wp select_wp | wpc)+ - apply (rule validE_validE_R) - apply (wp alternativeE_wp) - apply (simp add:cdl_page_mapping_entries_def - split del:if_splits | wp | wpc)+ - - apply auto + apply (rule validE_validE_R) + apply (wp alternativeE_wp) + apply (simp add:cdl_page_mapping_entries_def split del:if_split | wp | wpc)+ + apply auto done lemma decode_page_map_intent_rv_16_12: @@ -92,7 +89,7 @@ lemma decode_page_map_intent_rv_16_12: apply (wp alternativeE_wp select_wp) apply (rule validE_validE_R) apply (wp alternativeE_wp) - apply (simp add:cdl_page_mapping_entries_def split del:if_splits) + apply (simp add:cdl_page_mapping_entries_def) apply (wp cdl_lookup_pt_slot_rv | wpc | simp)+ apply auto done diff --git a/proof/capDL-api/IRQ_DP.thy b/proof/capDL-api/IRQ_DP.thy index a515b0d66..9066484c5 100644 --- a/proof/capDL-api/IRQ_DP.thy +++ b/proof/capDL-api/IRQ_DP.thy @@ -394,11 +394,6 @@ shows "\\root_tcb_id \f root_tcb \* (root_t apply (clarsimp dest!: reset_cap_asid_simps2) done - -lemma obj_tcb_simps [simp]: - "is_tcb tcb \ Tcb (obj_tcb tcb) = tcb" - by (clarsimp simp: is_tcb_def obj_tcb_def split: cdl_object.splits) - lemma seL4_IRQHandler_SetEndpoint_wp: "\\root_tcb_id \f root_tcb \* (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* diff --git a/proof/capDL-api/Invocation_DP.thy b/proof/capDL-api/Invocation_DP.thy index 557bda82a..dd9459c77 100644 --- a/proof/capDL-api/Invocation_DP.thy +++ b/proof/capDL-api/Invocation_DP.thy @@ -202,7 +202,7 @@ lemma syscall_valid_helper: arg_decode_fn arg_error_handler_fn perform_syscall_fn \Q\,\\r. Inv\" - apply (simp add:syscall_def del:split_paired_all) + apply (simp add:syscall_def) apply (rule hoare_vcg_handle_elseE) apply simp apply simp @@ -455,9 +455,6 @@ lemma corrupt_ipc_buffer_active_tcbs[wp]: apply wp done -crunch cdl_current_thread [wp]: update_thread "\s. P (cdl_current_thread s)" -(wp: crunch_wps) - lemma update_thread_wp: "\tcb_at' (\tcb. P (f tcb)) thread\ update_thread thread f \\rv. tcb_at' P thread \" @@ -508,8 +505,7 @@ lemma handle_pending_interrupts_no_ntf_cap: apply (rule hoare_pre) apply (wp send_signal_no_pending | wpc - | simp add: option_select_def handle_interrupt_def - split del: if_splits)+ + | simp add: option_select_def handle_interrupt_def split del: if_split)+ apply (wp alternative_wp select_wp hoare_drop_imps hoare_vcg_all_lift) apply simp done @@ -696,14 +692,6 @@ crunch cdl_current_thread[wp]: invoke_untyped "\s. P (cdl_current_thread helper simp:cdl_cur_thread_detype crunch_simps) -crunch cdl_current_thread[wp]: insert_cap_sibling "\s. P (cdl_current_thread s)" -(wp:select_wp mapM_x_wp' crunch_wps hoare_unless_wp - simp: crunch_simps) - -crunch cdl_current_thread[wp]: insert_cap_child "\s. P (cdl_current_thread s)" -(wp:select_wp mapM_x_wp' crunch_wps hoare_unless_wp - simp:crunch_simps) - crunch cdl_current_thread[wp]: move_cap "\s. P (cdl_current_thread s)" (wp:select_wp mapM_x_wp' crunch_wps hoare_unless_wp simp:crunch_simps) @@ -855,7 +843,7 @@ lemma syscall_valid_helper_allow_error: perform_syscall_fn \\r s. (\ tcb_has_error thread_ptr s \ Q s) \ (tcb_has_error thread_ptr s \ P s)\,\\r. Inv\" - apply (simp add:syscall_def del:split_paired_all) + apply (simp add:syscall_def) apply (rule hoare_vcg_handle_elseE) apply (erule hoare_pre) apply simp diff --git a/proof/capDL-api/KHeap_DP.thy b/proof/capDL-api/KHeap_DP.thy index 7147132a9..d7755622a 100644 --- a/proof/capDL-api/KHeap_DP.thy +++ b/proof/capDL-api/KHeap_DP.thy @@ -679,15 +679,13 @@ lemma reset_cap_asid_ep_cap: lemma reset_cap_asid_ntfn_cap: "reset_cap_asid cap = reset_cap_asid cap' \ is_ntfn_cap cap = is_ntfn_cap cap'" - apply (case_tac cap; case_tac cap'; simp add: reset_cap_asid_def) - done + by (case_tac cap; case_tac cap'; simp add: reset_cap_asid_def) lemma cap_rights_reset_cap_asid: "reset_cap_asid cap = reset_cap_asid cap' \ cap_rights cap = cap_rights cap'" apply (clarsimp simp: cap_rights_def reset_cap_asid_def) - apply (case_tac cap; (case_tac cap'; simp)) - done + by (case_tac cap; (case_tac cap'; simp)) (* Lemmas about valid_src_cap *) lemma reset_cap_asid_cnode_cap: @@ -789,9 +787,6 @@ lemma fast_finalise_cap_non_ep_wp: "\

and K (\ ep_related_cap cap') \ fast_finalise cap' final \\y.

\" by (case_tac cap',simp_all add:ep_related_cap_def) -crunch inv [wp]: is_final_cap "\s. P" -(wp:crunch_wps select_wp simp:split_def unless_def) - lemma delete_cap_simple_wp: "\\s. c cap \* R> s \ \ ep_related_cap cap\ delete_cap_simple ptr @@ -1042,10 +1037,10 @@ lemma decode_cnode_mint_rvu: apply (metis reset_cap_asid_cap_type) apply (frule (1) reset_cap_asid_ep_cap[THEN iffD1]) apply simp - apply (metis reset_cap_asid_cap_badge ep_related_capI) + apply (metis reset_cap_asid_cap_badge ep_related_capI(1)) apply (frule (1) reset_cap_asid_ntfn_cap[THEN iffD1]) apply simp - apply (metis reset_cap_asid_cap_badge ep_related_capI) + apply (metis reset_cap_asid_cap_badge ep_related_capI(2)) apply (metis option.inject reset_cap_asid_cnode_cap) apply (metis cap_rights_reset_cap_asid) apply sep_solve @@ -1103,15 +1098,10 @@ lemma decode_cnode_mutate_rvu: apply (clarsimp dest!: mapu_dest_opt_cap simp: conj_comms update_cap_data_non cong:non_cap_cong) apply (subst (asm) reset_cap_asid_ep_related_cap[OF sym], assumption) - apply (metis reset_cap_asid_cap_type reset_cap_asid_ep_related_cap valid_src_cap_asid_cong - ep_related_capI) + apply (metis reset_cap_asid_cap_type valid_src_cap_asid_cong ep_related_capI(1-2)) apply sep_solve done -crunch preserve [wp]: decode_cnode_invocation "P" -(wp: derive_cap_wpE unlessE_wp hoare_whenE_wp select_wp hoare_drop_imps - simp: hoare_if_simpE if_apply_def2 throw_on_none_def) - lemma do_kernel_op_pull_back: "\\s. P s\ oper \\r. Q r\ \ \\s. P (kernel_state s)\ do_kernel_op oper \\r s. Q r (kernel_state s)\" diff --git a/proof/capDL-api/Retype_DP.thy b/proof/capDL-api/Retype_DP.thy index ab280b6f1..f2dbf47a9 100644 --- a/proof/capDL-api/Retype_DP.thy +++ b/proof/capDL-api/Retype_DP.thy @@ -491,7 +491,7 @@ lemma invoke_untyped_exception: apply (simp add: whenE_def) apply wp+ apply clarsimp - apply (cut_tac p = "(a,b)" in opt_cap_sep_imp) + apply (cut_tac p = "uref" in opt_cap_sep_imp) apply sep_solve apply (clarsimp dest!: reset_cap_asid_simps2) done @@ -561,12 +561,6 @@ lemma update_thread_intent_has_children[wp]: \\rv s. P (has_children ptr s)\" by (simp add:has_children_def is_cdt_parent_def | wp )+ -crunch cdt[wp]: set_cap "\s. P (cdl_cdt s)" -(wp:select_wp simp:crunch_simps corrupt_intents_def) - -crunch has_children[wp]: set_cap "has_children slot" -(wp:select_wp simp:crunch_simps corrupt_intents_def simp:has_children_def is_cdt_parent_def) - lemma seL4_Untyped_Retype_sep: "\cap_object root_cnode_cap = root_cnode; @@ -711,13 +705,6 @@ lemma seL4_Untyped_Retype_sep: * become parents, and never lose their children * **********************************************************************) - -crunch cdt_inc[wp]: set_cap "\s. cdl_cdt s child = parent" -(wp:select_wp simp:crunch_simps) - -crunch cdt_inc[wp]: has_restart_cap "\s. cdl_cdt s child = parent" -(wp:select_wp simp:crunch_simps) - crunch cdt_inc[wp]: schedule "\s. cdl_cdt s child = parent" (wp:select_wp alternative_wp crunch_wps simp:crunch_simps) @@ -857,12 +844,6 @@ lemma lookup_cap_rvu': crunch cdl_current_thread [wp]: handle_pending_interrupts "\s. P (cdl_current_thread s)" (wp: alternative_wp select_wp) -crunch cdl_current_thread [wp]: lookup_slot_for_cnode_op "\s. P (cdl_current_thread s)" -(wp: alternative_wp select_wp) - -crunch cdl_current_thread [wp]: lookup_slot "\s. P (cdl_current_thread s)" -(wp: alternative_wp select_wp) - crunch cdl_current_thread [wp]: lookup_cap "\s. P (cdl_current_thread s)" (wp: alternative_wp select_wp hoare_drop_imps) @@ -1049,10 +1030,6 @@ lemma transfer_caps_loop_cdl_parent: lemmas reset_untyped_cap_cdl2[wp] = reset_untyped_cap_cdl_parent[THEN valid_validE_E] -crunch cdl_parent[wp]: invoke_untyped "\s. cdl_cdt s slot = Some parent" - (wp: assert_inv crunch_wps select_wp mapME_x_inv_wp alternative_wp - simp: crunch_simps detype_def) - crunch cdt_parent: inject_reply_cap "\s. cdl_cdt s slot = Some parent" (simp: crunch_simps unless_def wp: crunch_wps) diff --git a/proof/capDL-api/TCB_DP.thy b/proof/capDL-api/TCB_DP.thy index 1920f5247..49202dc48 100644 --- a/proof/capDL-api/TCB_DP.thy +++ b/proof/capDL-api/TCB_DP.thy @@ -705,8 +705,7 @@ lemma call_kernel_with_intent_no_fault_helper': done lemma is_tcb_cap_is_object: "is_tcb_cap tcb_cap \ TcbCap (cap_object tcb_cap) = tcb_cap" - apply (clarsimp simp: cap_type_def cap_object_simps split: cdl_cap.splits) -done + by (clarsimp simp: cap_type_def split: cdl_cap.splits) lemma reset_cap_asid_mem_mapping: @@ -1033,6 +1032,7 @@ shows reset_cap_asid buffer_frame_cap = reset_cap_asid (buffer_frame_cap') " in hoare_gen_asmEx) apply (simp) apply (elim exE) + supply [[simproc del: defined_all]] apply simp apply (rule false_e_explode) apply (rule no_exception_conj') @@ -1056,7 +1056,7 @@ shows apply (rule conjI) prefer 2 apply (simp add: sep_conj_assoc update_tcb_fault_endpoint_def) - apply (clarsimp simp:unify cap_object_simps dest!:cap_typeD) + apply (clarsimp simp:unify dest!:cap_typeD) apply (rule sep_map_c_any[where cap = RestartCap]) apply (sep_schem) apply sep_solve @@ -1158,12 +1158,6 @@ shows apply (sep_solve) done -crunch idle_thread[wp]: set_cap "\s. P (cdl_current_thread s)" - (wp: crunch_wps) - -crunch current_domain[wp]: set_cap "\s. P (cdl_current_domain s)" - (wp: crunch_wps) - lemma reset_cap_asid_pending: "reset_cap_asid cap' = reset_cap_asid cap \ is_pending_cap cap' = is_pending_cap cap"