diff --git a/proof/crefine/AARCH64/Fastpath_C.thy b/proof/crefine/AARCH64/Fastpath_C.thy index 11c8f146e9..8db6b9da93 100644 --- a/proof/crefine/AARCH64/Fastpath_C.thy +++ b/proof/crefine/AARCH64/Fastpath_C.thy @@ -2922,25 +2922,9 @@ proof - cong: if_cong call_ignore_cong) apply (rule ccorres_abstract_ksCurThread, ceqv) apply (rule_tac P="ct = curThread" in ccorres_gen_asm, simp only:, thin_tac "ct = curThread") - -(* FIXME AARCH64 reply_recv mess here *) - - apply (rule ccorres_move_const_guard - ccorres_move_c_guard_tcb_ctes2 - ccorres_move_array_assertion_tcb_ctes)+ -(* - apply (rule ccorres_abstract_ksCurThread, ceqv) - apply (rename_tac ksCurThread_y) apply (rule ccorres_move_const_guard ccorres_move_c_guard_tcb_ctes2 ccorres_move_array_assertion_tcb_ctes)+ - apply (rule_tac xf'="ksCurThread_' \ globals" - and val="tcb_ptr_to_ctcb_ptr curThread" - in ccorres_abstract_known) - apply (rule Seq_weak_ceqv, rule Basic_ceqv) - apply (rule rewrite_xfI) - apply (rule refl) -*) apply csymbr (* get caller cap *) apply (rule ccorres_move_c_guard_cte) @@ -2990,9 +2974,7 @@ proof - apply (vcg exspec=slowpath_noreturn_spec) apply (simp cong: call_ignore_cong) - (* FIXME AARCH64 start of block needing re-indent *) - - (* get vspace root *) + (* get vspace root *) apply (simp add: getThreadVSpaceRoot_def locateSlot_conv cong: call_ignore_cong) apply (rule ccorres_move_c_guard_tcb_ctes3 ccorres_move_array_assertion_tcb_ctes @@ -3002,14 +2984,14 @@ proof - apply simp apply ceqv apply (rename_tac vs_cap vs_cap') - (* get capVSBasePtr from the vspace cap on C side (we don't know it's vspace cap yet) *) - apply (rule ccorres_symb_exec_r) (* can't use csymbr, we need use alternative spec rule *) + (* get capVSBasePtr from the vspace cap on C side (we don't know it's vspace cap yet) *) + apply (rule ccorres_symb_exec_r) (* can't use csymbr, we need to use alternative spec rule *) apply (rule_tac xf'=ret__unsigned_longlong_' in ccorres_abstract, ceqv) apply (rename_tac vspace_cap_c_ptr_maybe) apply csymbr+ apply (simp add: isValidVTableRoot_conv cong: call_ignore_cong) apply (rule ccorres_Cond_rhs_Seq) - (* \ isValidVTableRoot (cteCap vs_cap) *) + (* \ isValidVTableRoot (cteCap vs_cap) *) apply simp apply (rule ccorres_split_throws) apply (rule ccorres_call_hSkip) @@ -3023,7 +3005,6 @@ proof - apply (rule_tac P="vspace_cap_c_ptr_maybe = capUntypedPtr (cteCap vs_cap)" in ccorres_gen_asm2) apply (simp cong: call_ignore_cong) - (* C: get the asid *) apply (rule ccorres_rhs_assoc2) apply (rule_tac xf'=asid___unsigned_long_' @@ -3048,7 +3029,6 @@ proof - apply (rule slowpath_ccorres, simp+) apply (vcg exspec=slowpath_noreturn_spec) apply (simp cong: call_ignore_cong) - apply (rule_tac xf'=ret__int_' and val="from_bool (apVSpace (the asid_map_entry_opt) \ capPTBasePtr (capCap (cteCap vs_cap)))" @@ -3059,7 +3039,6 @@ proof - casid_map_relation_Some_c_lift_eqs) apply ceqv apply (simp cong: call_ignore_cong) - (* C does two checks/aborts, but Haskell only one, so direct If-condition equivalence doesn't match. Step over C side, resolve Haskell check using resulting non-abort conditions. *) @@ -3299,124 +3278,91 @@ the one ccorres rule it affects? *) apply wp apply (rule_tac P=\ in hoare_triv, simp) apply simp - -(* FIXME AARCH64 this guard_is_UNIV proof is cobbled together and probably doesn't need half these - theorems *) apply (simp add: imp_conjL rf_sr_ksCurThread del: all_imp_to_ex) apply (clarsimp simp: ccap_relation_ep_helpers guard_is_UNIV_def - mi_from_H_def) - apply (clarsimp simp: signed_n_msgRegisters_to_H + mi_from_H_def signed_n_msgRegisters_to_H messageInfoFromWord_def Let_def - mi_from_H_def seL4_MessageInfo_lift_def msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def shiftL_nat - mask_def msgLabelBits_def - guard_is_UNIV_def) + mask_def msgLabelBits_def) apply (force simp: size_msgRegisters_def msgMaxLength_def - ccap_relation_ep_helpers split: if_splits) - - apply (wp sts_valid_objs' asid_has_vmid_lift) + apply (wp sts_valid_objs' asid_has_vmid_lift) + apply simp + apply (vcg exspec=thread_state_ptr_set_tsType_np_modifies) + apply (simp add: pred_conj_def) + apply (rule mapM_x_wp'[OF hoare_weaken_pre]) + apply (wp asid_has_vmid_lift) + apply clarsimp apply simp - apply (vcg exspec=thread_state_ptr_set_tsType_np_modifies) - apply (simp add: pred_conj_def) - apply (rule mapM_x_wp'[OF hoare_weaken_pre]) - apply (wp asid_has_vmid_lift) - apply clarsimp + apply (vcg exspec=fastpath_copy_mrs_modifies) + apply simp + apply wp + apply (wp setCTE_cte_wp_at_other asid_has_vmid_lift) apply simp - apply (vcg exspec=fastpath_copy_mrs_modifies) - - + apply vcg + apply simp + apply (wp | simp + | wp (once) updateMDB_weak_cte_wp_at + | wp (once) updateMDB_cte_wp_at_other asid_has_vmid_lift)+ + apply (vcg exspec=mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_modifies) + apply simp + apply (wp getCTE_wp') + apply simp + apply vcg + apply (simp add: shiftl_t2n) + apply (wp hoare_drop_imps setEndpoint_valid_mdb' set_ep_valid_objs' + setObject_no_0_obj'[where 'a=endpoint, folded setEndpoint_def] + asid_has_vmid_lift) + apply simp + apply (vcg exspec=endpoint_ptr_mset_epQueue_tail_state_modifies + exspec=endpoint_ptr_set_epQueue_head_np_modifies + exspec=endpoint_ptr_get_epQueue_tail_modifies) + apply (simp add: valid_pspace'_def pred_conj_def conj_comms + valid_mdb'_def) + apply (wp threadSet_cur threadSet_tcbState_valid_objs + threadSet_state_refs_of' threadSet_ctes_of + valid_ep_typ_at_lift' threadSet_cte_wp_at' asid_has_vmid_lift + | simp)+ + apply (vcg exspec=thread_state_ptr_mset_blockingObject_tsType_modifies) apply simp - apply wp - apply (wp setCTE_cte_wp_at_other asid_has_vmid_lift) - -apply simp -apply vcg - + (* throw away results of isHighestPrio and the fastfail shortcut *) + apply (wp (once) hoare_drop_imp, wp) + apply (wp (once) hoare_drop_imp, wp) + apply simp + apply (vcg exspec=isHighestPrio_modifies) apply simp - apply (wp | simp - | wp (once) updateMDB_weak_cte_wp_at - | wp (once) updateMDB_cte_wp_at_other asid_has_vmid_lift)+ - apply (vcg exspec=mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_modifies) - + apply (rule cd_wp) + apply simp + apply vcg apply simp - apply (wp getCTE_wp') - + apply vcg apply simp apply vcg - - apply (simp add: shiftl_t2n) - apply (wp hoare_drop_imps setEndpoint_valid_mdb' set_ep_valid_objs' - setObject_no_0_obj'[where 'a=endpoint, folded setEndpoint_def] - asid_has_vmid_lift) - + apply simp + apply (rule getASIDPoolEntry_wp) apply simp - apply (vcg exspec=endpoint_ptr_mset_epQueue_tail_state_modifies - exspec=endpoint_ptr_set_epQueue_head_np_modifies - exspec=endpoint_ptr_get_epQueue_tail_modifies) - - apply (simp add: valid_pspace'_def pred_conj_def conj_comms - valid_mdb'_def) -supply HOL.simp_thms(19)[simp del] - - - apply (wp threadSet_cur threadSet_tcbState_valid_objs - threadSet_state_refs_of' threadSet_ctes_of - valid_ep_typ_at_lift' threadSet_cte_wp_at' asid_has_vmid_lift - | simp)+ - apply (vcg exspec=thread_state_ptr_mset_blockingObject_tsType_modifies) - + apply (vcg exspec=findMapForASID_modifies) apply simp - (* throw away results of isHighestPrio and the fastfail shortcut *) - apply (wp (once) hoare_drop_imp, wp) - apply (wp (once) hoare_drop_imp, wp) - - apply simp - apply (vcg exspec=isHighestPrio_modifies) - -apply simp - apply (rule cd_wp) - -apply simp -apply vcg -apply simp -apply vcg -apply simp -apply vcg - apply simp - apply (rule getASIDPoolEntry_wp) + apply (vcg exspec=cap_vspace_cap_get_capVSMappedASID_modifies) + apply simp + (* accessing VSBasePtr without knowing it's a VSpace, can't use default spec *) + apply (rule conseqPre, vcg exspec=cap_vspace_cap_get_capVSBasePtr_spec2) + apply (rule subset_refl) + apply (rule conseqPre, vcg exspec=cap_vspace_cap_get_capVSBasePtr_spec2) + apply clarsimp + apply simp + apply (rule threadGet_wp) + apply (simp add: syscall_from_H_def ccap_relation_reply_helper) + apply (vcg exspec=seL4_Fault_get_seL4_FaultType_modifies) apply simp - apply (vcg exspec=findMapForASID_modifies) + apply (simp add: ccap_relation_reply_helper) + apply (rule return_wp) apply simp - apply (vcg exspec=cap_vspace_cap_get_capVSMappedASID_modifies) - + apply (vcg exspec=fastpath_reply_cap_check_modifies) apply simp - (* accessing VSBasePtr without knowing it's a VSpace, can't use default spec *) - apply (rule conseqPre, vcg exspec=cap_vspace_cap_get_capVSBasePtr_spec2) - apply (rule subset_refl) - apply (rule conseqPre, vcg exspec=cap_vspace_cap_get_capVSBasePtr_spec2) -apply clarsimp - -(* FIXME AARCH64 apply (simp add: ccap_relation_reply_helper) *) - apply simp - apply (rule threadGet_wp) (* FIXME AARCH64 something strange happening with Char *) - - apply (simp add: syscall_from_H_def ccap_relation_reply_helper) - apply (vcg exspec=seL4_Fault_get_seL4_FaultType_modifies) - -find_theorems valid return -apply simp -apply (simp add: ccap_relation_reply_helper) -apply (rule return_wp) - - apply simp - apply (vcg exspec=fastpath_reply_cap_check_modifies) - - apply simp apply (rule getEndpoint_wp) - apply (simp add: syscall_from_H_def ccap_relation_reply_helper) apply (vcg exspec=endpoint_ptr_get_state_modifies) apply simp @@ -3438,18 +3384,15 @@ apply (rule return_wp) apply (rule user_getreg_wp) apply simp apply (rule user_getreg_wp) - apply (rule conjI) - (* Haskell precondition *) -apply (prop_tac "SCAST(32 signed \ 64) (SCAST(64 \ 32 signed) tcbCallerSlot) = tcbCallerSlot") - apply (simp add: tcbCallerSlot_def) - - apply (clarsimp simp: ct_in_state'_def obj_at_tcbs_of word_sle_def) + apply (prop_tac "scast (scast tcbCallerSlot :: int_word) = tcbCallerSlot") + apply (simp add: tcbCallerSlot_def) + apply (clarsimp simp: ct_in_state'_def invs_cur' invs_arch_state' obj_at_tcbs_of word_sle_def) apply (clarsimp simp: invs_ksCurDomain_maxDomain') - apply (rule conjI, fastforce) (* cur_tcb' *) - apply (frule invs_queues) + apply (rename_tac cur_tcb cte) apply (frule invs_valid_objs') + apply (frule invs_queues) apply (clarsimp simp: valid_queues_def) apply (frule tcbs_of_aligned') apply (simp add: invs_pspace_aligned') @@ -3459,81 +3402,39 @@ apply (prop_tac "SCAST(32 signed \ 64) (SCAST(64 \ 32 si apply (frule st_tcb_at_state_refs_ofD') apply (frule ctes_of_valid', fastforce) apply (clarsimp simp: obj_at_tcbs_of ct_in_state'_def st_tcb_at_tcbs_of - invs_cur' invs_valid_objs' ctes_of_valid' + invs_valid_objs' ctes_of_valid' fun_upd_def[symmetric] fun_upd_idem pred_tcb_at'_def invs_no_0_obj' cong: conj_cong) - -apply (rule conjI) - apply (clarsimp simp: isCap_simps valid_cap'_def[split_simps capability.split] - maskCapRights_def cte_wp_at_ctes_of cte_level_bits_def) - apply (frule_tac p = a in ctes_of_valid', clarsimp) - apply (simp add: valid_cap_simps') - -apply clarsimp - - + apply (rule conjI) (* obj_at' of ep ptr *) + apply (fastforce dest: ctes_of_valid' simp: valid_cap_simps' isCap_simps cte_wp_at_ctes_of) + apply clarsimp apply (frule_tac p="p + tcbCallerSlot * cte_size" for p cte_size in ctes_of_valid', clarsimp) apply (clarsimp simp: valid_capAligned) - - apply (rule conjI, fastforce) (* valid_arch_state' *) - - apply (clarsimp simp: obj_at_tcbs_of ct_in_state'_def st_tcb_at_tcbs_of - invs_cur' invs_valid_objs' ctes_of_valid' - fun_upd_def[symmetric] fun_upd_idem pred_tcb_at'_def invs_no_0_obj') apply (frule_tac p="p + tcbVTableSlot * cte_size" for p cte_size in ctes_of_valid', clarsimp) - apply (rule conjI) (* asid_wf *) - apply (clarsimp simp: isCap_simps valid_cap'_def - dest!: isValidVTableRootD) + apply (clarsimp simp: isCap_simps valid_cap'_def dest!: isValidVTableRootD) apply (solves \clarsimp simp: wellformed_mapdata'_def\) - -apply clarsimp - -apply (rule conjI; clarsimp?) - prefer 2 (* tcbDomain maxDomain *) - apply (frule_tac tcb=tcba in tcbs_of_valid_tcb'[OF invs_valid_objs', rotated]) - apply simp - apply (simp add: valid_tcb'_def) - -apply (rule conjI; clarsimp?) (* canonical_address (capEPPtr (cteCap ctea)) *) - apply (clarsimp simp add: obj_at'_is_canonical dest!: invs_pspace_canonical') - + apply (frule_tac tcb=tcb in tcbs_of_valid_tcb'[OF invs_valid_objs', rotated], simp) + apply (clarsimp simp add: valid_tcb'_def) + apply (rule conjI; clarsimp?) (* canonical_address (capEPPtr (cteCap ctea)) *) + apply (clarsimp simp: obj_at'_is_canonical dest!: invs_pspace_canonical') apply (clarsimp simp: isCap_simps valid_cap'_def[split_simps capability.split] maskCapRights_def cte_wp_at_ctes_of cte_level_bits_def) - apply (frule_tac p = a in ctes_of_valid', clarsimp) + apply (frule_tac p=a in ctes_of_valid', clarsimp) apply (simp add: valid_cap_simps') - - apply (rule conjI, solves clarsimp)+ (* a bunch of consequences of invs' *) - apply (frule invs_mdb') - - apply (clarsimp simp: cte_wp_at_ctes_of tcbSlots cte_level_bits_def + apply (rule conjI, solves clarsimp)+ (* a bunch of consequences of invs' *) + apply (clarsimp simp: cte_wp_at_ctes_of cte_level_bits_def makeObject_cte isValidVTableRoot_def - (* ARM_HYP_H.isValidVTableRoot_def *) to_bool_def - valid_mdb'_def valid_tcb_state'_def - word_le_nat_alt[symmetric] (*length_msgRegisters*)) - -apply (rule conjI; clarsimp?) (* msglength *) - apply (simp add: word_le_nat_alt) - apply (simp add: size_msgRegisters_def n_msgRegisters_def length_msgRegisters) - - -apply (rule conjI; clarsimp?) (* asid_has_vmid *) - apply (prop_tac "capPTBasePtr (capCap (cteCap ctec)) = global.capUntypedPtr (cteCap ctec)") + valid_mdb'_def valid_tcb_state'_def) + apply (rule conjI; clarsimp?) (* msglength *) + apply (simp add: word_le_nat_alt size_msgRegisters_def n_msgRegisters_def length_msgRegisters) + apply (prop_tac "capPTBasePtr (capCap (cteCap ctec)) = capUntypedPtr (cteCap ctec)") apply (solves \clarsimp simp add: isVTableRoot_ex\) - apply simp - apply (clarsimp simp: asid_has_vmid_def asid_has_entry_def split: option.splits) - apply (rule_tac x=pool in exI) - apply clarsimp - apply (case_tac asid_entry, clarsimp) - - apply (rule_tac x=pool in exI) - apply clarsimp - apply (case_tac asid_entry, clarsimp) -(* FIXME AARCH64 WTF *) - - + apply (rule conjI) (* asid_has_vmid *) + apply (clarsimp simp: asid_has_vmid_def asid_has_entry_def) + apply (case_tac asid_entry, fastforce) apply (frule ko_at_valid_ep', fastforce) apply (frule invs_mdb') apply (safe del: notI disjE)[1] @@ -3544,63 +3445,32 @@ apply (rule conjI; clarsimp?) (* asid_has_vmid *) clarsimp+) apply (simp add: obj_at_tcbs_of st_tcb_at_tcbs_of) apply (drule invs_sym') - apply (erule_tac P=sym_refs in subst[rotated]) + apply (erule_tac P=sym_refs in subst[rotated]) apply (rule fun_upd_idem[symmetric]) apply (clarsimp simp: tcb_bound_refs'_def) apply (case_tac ntfnptr, simp_all)[1] apply (clarsimp simp: set_eq_subset) - apply (clarsimp simp: capAligned_def isVTableRoot_def field_simps) - - - apply (frule_tac ptr2=v0a in tcbs_of_cte_wp_at_vtable) - apply (frule_tac ptr2=v0a in tcbs_of_aligned') - apply (clarsimp simp: field_simps) - apply (clarsimp simp: capAligned_def) - apply (clarsimp simp: field_simps) - apply (solves \clarsimp simp add: isVTableRoot_ex\) + apply (solves \clarsimp simp: capAligned_def isVTableRoot_def field_simps\) (* C precondition *) - -(* FIXME AARCH64 RAF cleanup *) - apply (clarsimp simp: syscall_from_H_def[split_simps syscall.split] word_sle_def word_sless_def rf_sr_ksCurThread size_of_def cte_level_bits_def tcb_cnode_index_defs tcbCTableSlot_def tcbVTableSlot_def tcbReplySlot_def tcbCallerSlot_def from_bool_eq_if' of_bl_from_bool) - apply (frule obj_at_bound_tcb_grandD, clarsimp, clarsimp, simp) + apply (frule obj_at_bound_tcb_grandD, clarsimp, clarsimp, assumption) apply (clarsimp simp: typ_heap_simps' ccap_relation_ep_helpers) - apply (clarsimp simp: ccte_relation_eq_ccap_relation - ccap_relation_case_sum_Null_endpoint - isRight_case_sum typ_heap_simps' - cap_get_tag_isCap mi_from_H_def) - apply (intro conjI impI allI - ; clarsimp simp: isCap_simps capAligned_def objBits_simps' - (*cap_get_tag_isCap_ArchObject2*) typ_heap_simps isRight_def -casid_map_relation_Some_get_tag - dest!: ptr_val_tcb_ptr_mask2[unfolded objBits_def mask_def, simplified] - (*isValidVTableRootD'*) - split: sum.splits - ; (solves \clarsimp simp: ctcb_relation_def\)?) - - - (* cap_get_tag_isCap hides info obtained from isValidVTableRootD' *) - apply (frule (1) capVSBasePtr_CL_capUntypedPtr_helper) - apply (clarsimp simp: cap_get_tag_isCap dest!: isValidVTableRootD') -apply (clarsimp simp: isCap_simps capAligned_def objBits_simps' - (*cap_get_tag_isCap_ArchObject2*) typ_heap_simps isRight_def -casid_map_relation_Some_get_tag - dest!: ptr_val_tcb_ptr_mask2[unfolded objBits_def mask_def, simplified] - (*isValidVTableRootD'*) - split: sum.splits) - apply (frule (1) capVSBasePtr_CL_capUntypedPtr_helper) - apply (clarsimp simp: cap_get_tag_isCap dest!: isValidVTableRootD') -apply (clarsimp simp: isCap_simps capAligned_def objBits_simps' - (*cap_get_tag_isCap_ArchObject2*) typ_heap_simps isRight_def -casid_map_relation_Some_get_tag - dest!: ptr_val_tcb_ptr_mask2[unfolded objBits_def mask_def, simplified] - (*isValidVTableRootD'*) - split: sum.splits) + apply (clarsimp simp: ccte_relation_eq_ccap_relation ccap_relation_case_sum_Null_endpoint + typ_heap_simps' cap_get_tag_isCap mi_from_H_def) + apply (intro conjI impI allI; + clarsimp simp: isCap_simps capAligned_def objBits_simps' + typ_heap_simps + casid_map_relation_Some_get_tag + dest!: ptr_val_tcb_ptr_mask2[unfolded objBits_def mask_def, simplified]; + (solves \clarsimp simp: ctcb_relation_def\)?) + (* cap_get_tag_isCap hides info obtained from isValidVTableRootD' *) + apply (frule (1) capVSBasePtr_CL_capUntypedPtr_helper, + clarsimp simp: cap_get_tag_isCap isCap_simps dest!: isValidVTableRootD')+ done qed