diff --git a/proof/refine/AARCH64/ADT_H.thy b/proof/refine/AARCH64/ADT_H.thy index 5f0f9ed3c8..de24d21310 100644 --- a/proof/refine/AARCH64/ADT_H.thy +++ b/proof/refine/AARCH64/ADT_H.thy @@ -281,6 +281,9 @@ definition tcb_fault = map_option FaultMap (tcbFault tcb), tcb_bound_notification = tcbBoundNotification tcb, tcb_mcpriority = tcbMCP tcb, + tcb_priority = tcbPriority tcb, + tcb_time_slice = tcbTimeSlice tcb, + tcb_domain = tcbDomain tcb, tcb_arch = ArchTcbMap (tcbArch tcb)\" definition @@ -831,53 +834,6 @@ proof - done qed -definition - "EtcbMap tcb \ - \tcb_priority = tcbPriority tcb, - time_slice = tcbTimeSlice tcb, - tcb_domain = tcbDomain tcb\" - -definition absEkheap :: - "(machine_word \ Structures_H.kernel_object) \ obj_ref \ etcb option" where - "absEkheap h \ \x. - case h x of - Some (KOTCB tcb) \ Some (EtcbMap tcb) - | _ \ None" - -lemma absEkheap_correct: - assumes pspace_relation: "pspace_relation (kheap s) (ksPSpace s')" - assumes ekheap_relation: "ekheap_relation (ekheap s) (ksPSpace s')" - assumes vetcbs: "valid_etcbs s" - shows "absEkheap (ksPSpace s') = ekheap s" - apply (rule ext) - apply (clarsimp simp: absEkheap_def split: option.splits Structures_H.kernel_object.splits) - apply (subgoal_tac "\x. (\tcb. kheap s x = Some (TCB tcb)) = - (\tcb'. ksPSpace s' x = Some (KOTCB tcb'))") - using vetcbs ekheap_relation - apply (clarsimp simp: valid_etcbs_def is_etcb_at_def dom_def ekheap_relation_def st_tcb_at_def obj_at_def) - apply (erule_tac x=x in allE)+ - apply (rule conjI, force) - apply clarsimp - apply (rule conjI, clarsimp simp: EtcbMap_def etcb_relation_def)+ - apply clarsimp - using pspace_relation - apply (clarsimp simp add: pspace_relation_def pspace_dom_def UNION_eq - dom_def Collect_eq) - apply (rule iffI) - apply (erule_tac x=x in allE)+ - apply (case_tac "ksPSpace s' x", clarsimp) - apply (erule_tac x=x in allE, clarsimp) - apply clarsimp - apply (case_tac a, simp_all add: tcb_relation_cut_def other_obj_relation_def) - apply (insert pspace_relation) - apply (clarsimp simp: obj_at'_def) - apply (erule(1) pspace_dom_relatedE) - apply (erule(1) obj_relation_cutsE) - apply (clarsimp simp: other_obj_relation_def - split: Structures_A.kernel_object.split_asm if_split_asm - AARCH64_A.arch_kernel_obj.split_asm)+ - done - text \The following function can be used to reverse cte_map.\ definition "cteMap cns \ \p. @@ -1645,13 +1601,6 @@ lemma absSchedulerAction_correct: definition "absExst s \ \work_units_completed_internal = ksWorkUnitsCompleted s, - scheduler_action_internal = absSchedulerAction (ksSchedulerAction s), - ekheap_internal = absEkheap (ksPSpace s), - domain_list_internal = ksDomSchedule s, - domain_index_internal = ksDomScheduleIdx s, - cur_domain_internal = ksCurDomain s, - domain_time_internal = ksDomainTime s, - ready_queues_internal = (\d p. heap_walk (tcbSchedNexts_of s) (tcbQueueHead (ksReadyQueues s (d, p))) []), cdt_list_internal = absCDTList (cteMap (gsCNodes s)) (ctes_of s)\" lemma absExst_correct: @@ -1659,16 +1608,12 @@ lemma absExst_correct: assumes rel: "(s, s') \ state_relation" shows "absExst s' = exst s" apply (rule det_ext.equality) - using rel invs invs' - apply (simp_all add: absExst_def absSchedulerAction_correct absEkheap_correct - absCDTList_correct[THEN fun_cong] state_relation_def invs_def - valid_state_def ready_queues_relation_def ready_queue_relation_def - invs'_def valid_state'_def - valid_pspace_def valid_sched_def valid_pspace'_def curry_def - fun_eq_iff) - apply (fastforce simp: absEkheap_correct) - apply (fastforce simp: list_queue_relation_def Let_def dest: heap_ls_is_walk) - done + using rel invs invs' + apply (simp_all add: absExst_def absSchedulerAction_correct + absCDTList_correct[THEN fun_cong] state_relation_def invs_def valid_state_def + ready_queues_relation_def invs'_def valid_state'_def + valid_pspace_def valid_sched_def valid_pspace'_def curry_def fun_eq_iff) + done definition @@ -1677,6 +1622,12 @@ definition cdt = absCDT (cteMap (gsCNodes s)) (ctes_of s), is_original_cap = absIsOriginalCap (cteMap (gsCNodes s)) (ksPSpace s), cur_thread = ksCurThread s, idle_thread = ksIdleThread s, + scheduler_action = absSchedulerAction (ksSchedulerAction s), + domain_list = ksDomSchedule s, + domain_index = ksDomScheduleIdx s, + cur_domain = ksCurDomain s, + domain_time = ksDomainTime s, + ready_queues = (\d p. heap_walk (tcbSchedNexts_of s) (tcbQueueHead (ksReadyQueues s (d, p))) []), machine_state = observable_memory (ksMachineState s) (user_mem' s), interrupt_irq_node = absInterruptIRQNode (ksInterruptState s), interrupt_states = absInterruptStates (ksInterruptState s), diff --git a/proof/refine/AARCH64/ArchAcc_R.thy b/proof/refine/AARCH64/ArchAcc_R.thy index 8b574600a7..670605d67c 100644 --- a/proof/refine/AARCH64/ArchAcc_R.thy +++ b/proof/refine/AARCH64/ArchAcc_R.thy @@ -455,11 +455,6 @@ lemma setObject_PT_corres: apply ((simp split: if_split_asm)+)[2] apply (simp add: other_obj_relation_def split: Structures_A.kernel_object.splits arch_kernel_obj.splits) - apply (rule conjI) - apply (clarsimp simp: ekheap_relation_def pspace_relation_def) - apply (drule_tac x=p in bspec, erule domI) - apply (simp add: other_obj_relation_def - split: Structures_A.kernel_object.splits) apply (extract_conjunct \match conclusion in "ghost_relation _ _ _ _" \ -\) apply (clarsimp simp add: ghost_relation_def) apply (erule_tac x="p && ~~ mask (pt_bits (pt_type pt))" in allE)+ diff --git a/proof/refine/AARCH64/Arch_R.thy b/proof/refine/AARCH64/Arch_R.thy index ff4072cd66..7d16e54654 100644 --- a/proof/refine/AARCH64/Arch_R.thy +++ b/proof/refine/AARCH64/Arch_R.thy @@ -96,24 +96,6 @@ lemma createObject_typ_at': apply (clarsimp simp: is_aligned_no_overflow_mask) done -lemma retype_region2_ext_retype_region_ArchObject: - "retype_region ptr n us (ArchObject x)= - retype_region2 ptr n us (ArchObject x)" - apply (rule ext) - apply (simp add: retype_region_def retype_region2_def bind_assoc - retype_region2_ext_def retype_region_ext_def default_ext_def) - apply (rule ext) - apply (intro monad_eq_split_tail ext)+ - apply simp - apply simp - apply (simp add:gets_def get_def bind_def return_def simpler_modify_def ) - apply (rule_tac x = xc in fun_cong) - apply (rule_tac f = do_extended_op in arg_cong) - apply (rule ext) - apply simp - apply simp - done - lemma set_cap_device_and_range_aligned: "is_aligned ptr sz \ \\_. True\ set_cap @@ -165,7 +147,6 @@ lemma performASIDControlInvocation_corres: apply (clarsimp simp:is_cap_simps) apply (simp add: free_index_of_def) apply (rule corres_split) - apply (simp add: retype_region2_ext_retype_region_ArchObject ) apply (rule corres_retype [where ty="Inl (KOArch (KOASIDPool F))" for F, unfolded APIType_map2_def makeObjectKO_def, THEN createObjects_corres',simplified, @@ -315,9 +296,8 @@ lemma performASIDControlInvocation_corres: apply (rule conjI, rule pspace_no_overlap_subset, rule pspace_no_overlap_detype[OF caps_of_state_valid]) apply (simp add:invs_psp_aligned invs_valid_objs is_aligned_neg_mask_eq)+ - apply (clarsimp simp: detype_def clear_um_def detype_ext_def valid_sched_def valid_etcbs_def - st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def - wrap_ext_det_ext_ext_def) + apply (clarsimp simp: detype_def clear_um_def valid_sched_def + st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def) apply (simp add: detype_def clear_um_def) apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) apply (simp add:invs_valid_objs)+ diff --git a/proof/refine/AARCH64/CSpace1_R.thy b/proof/refine/AARCH64/CSpace1_R.thy index 8cff61483d..d10fe77238 100644 --- a/proof/refine/AARCH64/CSpace1_R.thy +++ b/proof/refine/AARCH64/CSpace1_R.thy @@ -1733,37 +1733,30 @@ proof - done qed -definition pspace_relations where - "pspace_relations ekh kh kh' \ pspace_relation kh kh' \ ekheap_relation ekh kh'" - lemma set_cap_not_quite_corres_prequel: assumes cr: - "pspace_relations (ekheap s) (kheap s) (ksPSpace s')" + "pspace_relation (kheap s) (ksPSpace s')" "(x,t') \ fst (setCTE p' c' s')" "valid_objs s" "pspace_aligned s" "pspace_distinct s" "cte_at p s" "pspace_aligned' s'" "pspace_distinct' s'" assumes c: "cap_relation c (cteCap c')" assumes p: "p' = cte_map p" shows "\t. ((),t) \ fst (set_cap c p s) \ - pspace_relations (ekheap t) (kheap t) (ksPSpace t')" + pspace_relation (kheap t) (ksPSpace t')" using cr apply (clarsimp simp: setCTE_def setObject_def in_monad split_def) apply (drule(1) updateObject_cte_is_tcb_or_cte[OF _ refl, rotated]) apply (elim disjE exE conjE) - apply (clarsimp simp: lookupAround2_char1 pspace_relations_def) + apply (clarsimp simp: lookupAround2_char1) apply (frule(5) cte_map_pulls_tcb_to_abstract[OF p]) apply (simp add: domI) apply (frule tcb_cases_related2) apply (clarsimp simp: set_cap_def2 split_def bind_def get_object_def simpler_gets_def assert_def fail_def return_def set_object_def get_def put_def) - apply (rule conjI) - apply (erule(2) pspace_relation_update_tcbs) - apply (simp add: c) - apply (clarsimp simp: ekheap_relation_def pspace_relation_def) - apply (drule bspec, erule domI) - apply (clarsimp simp: etcb_relation_def tcb_cte_cases_def split: if_split_asm) - apply (clarsimp simp: pspace_relations_def) + apply (erule(2) pspace_relation_update_tcbs) + apply (simp add: c) + apply clarsimp apply (frule(5) cte_map_pulls_cte_to_abstract[OF p]) apply (clarsimp simp: set_cap_def split_def bind_def get_object_def simpler_gets_def assert_def a_type_def fail_def return_def @@ -1771,24 +1764,20 @@ lemma set_cap_not_quite_corres_prequel: apply (erule(1) valid_objsE) apply (clarsimp simp: valid_obj_def valid_cs_def valid_cs_size_def exI) apply (rule conjI, clarsimp) - apply (rule conjI) - apply (erule(1) pspace_relation_update_ctes[where cap=c]) - apply clarsimp - apply (intro conjI impI) - apply (rule ext, clarsimp simp add: domI p) - apply (drule cte_map_inj_eq [OF _ _ cr(6) cr(3-5)]) - apply (simp add: cte_at_cases domI) - apply (simp add: prod_eq_iff) - apply (insert p)[1] - apply (clarsimp split: option.split Structures_A.kernel_object.split - intro!: ext) + apply (erule(1) pspace_relation_update_ctes[where cap=c]) + apply clarsimp + apply (intro conjI impI) + apply (rule ext, clarsimp simp add: domI p) apply (drule cte_map_inj_eq [OF _ _ cr(6) cr(3-5)]) - apply (simp add: cte_at_cases domI well_formed_cnode_invsI[OF cr(3)]) - apply clarsimp - apply (simp add: c) - apply (clarsimp simp: ekheap_relation_def pspace_relation_def) - apply (drule bspec, erule domI) - apply (clarsimp simp: etcb_relation_def tcb_cte_cases_def split: if_split_asm) + apply (simp add: cte_at_cases domI) + apply (simp add: prod_eq_iff) + apply (insert p)[1] + apply (clarsimp split: option.split Structures_A.kernel_object.split + intro!: ext) + apply (drule cte_map_inj_eq [OF _ _ cr(6) cr(3-5)]) + apply (simp add: cte_at_cases domI well_formed_cnode_invsI[OF cr(3)]) + apply clarsimp + apply (simp add: c) apply (simp add: wf_cs_insert) done @@ -1801,7 +1790,7 @@ lemma setCTE_pspace_only: lemma set_cap_not_quite_corres: assumes cr: - "pspace_relations (ekheap s) (kheap s) (ksPSpace s')" + "pspace_relation (kheap s) (ksPSpace s')" "cur_thread s = ksCurThread s'" "idle_thread s = ksIdleThread s'" "machine_state s = ksMachineState s'" @@ -1818,10 +1807,9 @@ lemma set_cap_not_quite_corres: assumes c: "cap_relation c c'" assumes p: "p' = cte_map p" shows "\t. ((),t) \ fst (set_cap c p s) \ - pspace_relations (ekheap t) (kheap t) (ksPSpace t') \ + pspace_relation (kheap t) (ksPSpace t') \ cdt t = cdt s \ cdt_list t = cdt_list s \ - ekheap t = ekheap s \ scheduler_action t = scheduler_action s \ ready_queues t = ready_queues s \ is_original_cap t = is_original_cap s \ @@ -2438,10 +2426,6 @@ lemma capClass_ztc_relation: cap_relation c c' \ \ capClass c' = PhysicalClass" by (auto simp: is_cap_simps) -lemma pspace_relationsD: - "\pspace_relation kh kh'; ekheap_relation ekh kh'\ \ pspace_relations ekh kh kh'" - by (simp add: pspace_relations_def) - lemma updateCap_corres: "\cap_relation cap cap'; is_zombie cap \ is_cnode_cap cap \ is_thread_cap cap \ @@ -2463,14 +2447,13 @@ lemma updateCap_corres: apply fastforce apply (clarsimp simp: cte_wp_at_ctes_of) apply (clarsimp simp add: state_relation_def) - apply (drule(1) pspace_relationsD) apply (frule (3) set_cap_not_quite_corres; fastforce?) apply (erule cte_wp_at_weakenE, rule TrueI) apply clarsimp apply (rule bexI) prefer 2 apply simp - apply (clarsimp simp: in_set_cap_cte_at_swp pspace_relations_def) + apply (clarsimp simp: in_set_cap_cte_at_swp) apply (drule updateCap_stuff) apply simp apply (extract_conjunct \match conclusion in "ghost_relation _ _ _ _" \ -\) @@ -2592,24 +2575,6 @@ lemma updateMDB_pspace_relation: apply fastforce done -lemma updateMDB_ekheap_relation: - assumes "(x, s'') \ fst (updateMDB p f s')" - assumes "ekheap_relation (ekheap s) (ksPSpace s')" - shows "ekheap_relation (ekheap s) (ksPSpace s'')" using assms - apply (clarsimp simp: updateMDB_def Let_def setCTE_def setObject_def in_monad ekheap_relation_def etcb_relation_def split_def split: if_split_asm) - apply (drule(1) updateObject_cte_is_tcb_or_cte[OF _ refl, rotated]) - apply (drule_tac P="(=) s'" in use_valid [OF _ getCTE_sp], rule refl) - apply (drule bspec, erule domI) - apply (clarsimp simp: tcb_cte_cases_def lookupAround2_char1 split: if_split_asm) - done - -lemma updateMDB_pspace_relations: - assumes "(x, s'') \ fst (updateMDB p f s')" - assumes "pspace_relations (ekheap s) (kheap s) (ksPSpace s')" - assumes "pspace_aligned' s'" "pspace_distinct' s'" - shows "pspace_relations (ekheap s) (kheap s) (ksPSpace s'')" using assms - by (simp add: pspace_relations_def updateMDB_pspace_relation updateMDB_ekheap_relation) - lemma updateMDB_ctes_of: assumes "(x, s') \ fst (updateMDB p f s)" assumes "no_0 (ctes_of s)" @@ -2654,7 +2619,7 @@ crunch updateMDB lemma updateMDB_the_lot: assumes "(x, s'') \ fst (updateMDB p f s')" - assumes "pspace_relations (ekheap s) (kheap s) (ksPSpace s')" + assumes "pspace_relation (kheap s) (ksPSpace s')" assumes "pspace_aligned' s'" "pspace_distinct' s'" "no_0 (ctes_of s')" shows "ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f) \ ksMachineState s'' = ksMachineState s' \ @@ -2667,7 +2632,7 @@ lemma updateMDB_the_lot: ksArchState s'' = ksArchState s' \ gsUserPages s'' = gsUserPages s' \ gsCNodes s'' = gsCNodes s' \ - pspace_relations (ekheap s) (kheap s) (ksPSpace s'') \ + pspace_relation (kheap s) (ksPSpace s'') \ pspace_aligned' s'' \ pspace_distinct' s'' \ no_0 (ctes_of s'') \ ksDomScheduleIdx s'' = ksDomScheduleIdx s' \ @@ -2679,7 +2644,7 @@ lemma updateMDB_the_lot: (\domain priority. (inQ domain priority |< tcbs_of' s'') = (inQ domain priority |< tcbs_of' s'))" using assms - apply (simp add: updateMDB_eqs updateMDB_pspace_relations split del: if_split) + apply (simp add: updateMDB_eqs updateMDB_pspace_relation split del: if_split) apply (frule (1) updateMDB_ctes_of) apply clarsimp apply (rule conjI) @@ -3869,7 +3834,6 @@ lemma setCTE_UntypedCap_corres: apply (clarsimp simp: cte_wp_at_ctes_of) apply clarsimp apply (clarsimp simp add: state_relation_def split_def) - apply (drule (1) pspace_relationsD) apply (frule_tac c = "cap.UntypedCap dev r bits idx" in set_cap_not_quite_corres_prequel) apply assumption+ @@ -3880,8 +3844,6 @@ lemma setCTE_UntypedCap_corres: apply (rule bexI) prefer 2 apply assumption - apply (clarsimp simp: pspace_relations_def) - apply (subst conj_assoc[symmetric]) apply clarsimp apply (rule conjI) apply (frule setCTE_pspace_only) @@ -3893,7 +3855,7 @@ lemma setCTE_UntypedCap_corres: apply (rule use_valid[OF _ setCTE_tcbSchedNexts_of], assumption) apply (rule use_valid[OF _ setCTE_ksReadyQueues], assumption) apply (rule use_valid[OF _ setCTE_inQ_opt_pred], assumption) - apply (rule use_valid[OF _ set_cap_exst], assumption) + apply (rule use_valid[OF _ set_cap_rqueues], assumption) apply clarsimp apply (rule conjI) apply (frule setCTE_pspace_only) @@ -5156,8 +5118,8 @@ crunch set_untyped_cap_as_full lemma updateMDB_the_lot': assumes "(x, s'') \ fst (updateMDB p f s')" - assumes "pspace_relations (ekheap sa) (kheap s) (ksPSpace s')" - assumes "pspace_aligned' s'" "pspace_distinct' s'" "no_0 (ctes_of s')" "ekheap s = ekheap sa" + assumes "pspace_relation (kheap s) (ksPSpace s')" + assumes "pspace_aligned' s'" "pspace_distinct' s'" "no_0 (ctes_of s')" shows "ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f) \ ksMachineState s'' = ksMachineState s' \ ksWorkUnitsCompleted s'' = ksWorkUnitsCompleted s' \ @@ -5169,7 +5131,7 @@ lemma updateMDB_the_lot': ksArchState s'' = ksArchState s' \ gsUserPages s'' = gsUserPages s' \ gsCNodes s'' = gsCNodes s' \ - pspace_relations (ekheap s) (kheap s) (ksPSpace s'') \ + pspace_relation (kheap s) (ksPSpace s'') \ pspace_aligned' s'' \ pspace_distinct' s'' \ no_0 (ctes_of s'') \ ksDomScheduleIdx s'' = ksDomScheduleIdx s' \ @@ -5182,7 +5144,7 @@ lemma updateMDB_the_lot': (inQ domain priority |< tcbs_of' s'') = (inQ domain priority |< tcbs_of' s'))" apply (rule updateMDB_the_lot) using assms - apply (fastforce simp: pspace_relations_def)+ + apply fastforce+ done lemma cte_map_inj_eq': @@ -5247,7 +5209,6 @@ lemma cteInsert_corres: apply (simp+)[3] apply (clarsimp simp: corres_underlying_def state_relation_def in_monad valid_mdb'_def valid_mdb_ctes_def) - apply (drule (1) pspace_relationsD) apply (drule (18) set_cap_not_quite_corres) apply (rule refl) apply (elim conjE exE) @@ -5286,7 +5247,6 @@ lemma cteInsert_corres: apply (thin_tac "ksCurThread t = p" for p t)+ apply (thin_tac "ksIdleThread t = p" for p t)+ apply (thin_tac "ksSchedulerAction t = p" for p t)+ - apply (clarsimp simp: pspace_relations_def) apply (rule conjI) apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) @@ -6724,7 +6684,6 @@ lemma cteSwap_corres: apply (clarsimp simp: corres_underlying_def in_monad state_relation_def) apply (clarsimp simp: valid_mdb'_def) - apply (drule(1) pspace_relationsD) apply (drule (12) set_cap_not_quite_corres) apply (erule cte_wp_at_weakenE, rule TrueI) apply assumption+ @@ -6760,20 +6719,19 @@ lemma cteSwap_corres: apply (simp cong: option.case_cong) apply (drule updateCap_stuff, elim conjE, erule(1) impE) apply (drule (2) updateMDB_the_lot') - apply (erule (1) impE, assumption) - apply (fastforce simp only: no_0_modify_map) - apply assumption + apply (erule (1) impE, assumption) + apply (fastforce simp only: no_0_modify_map) apply (elim conjE TrueE, simp only:) - apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map) apply (drule in_getCTE, elim conjE, simp only:) - apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map) apply (elim conjE TrueE, simp only:) - apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map) apply (elim conjE TrueE, simp only:) - apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map) apply (elim conjE TrueE, simp only:) - apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) - apply (simp only: pspace_relations_def refl) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map) + apply (simp only: refl) apply (rule conjI, rule TrueI)+ apply (thin_tac "ksMachineState t = p" for t p)+ apply (thin_tac "ksCurThread t = p" for t p)+ @@ -6822,7 +6780,6 @@ lemma cteSwap_corres: apply (thin_tac "domain_index t = p" for t p)+ apply (thin_tac "domain_list t = p" for t p)+ apply (thin_tac "domain_time t = p" for t p)+ - apply (thin_tac "ekheap t = p" for t p)+ apply (thin_tac "scheduler_action t = p" for t p)+ apply (thin_tac "ksArchState t = p" for t p)+ apply (thin_tac "gsCNodes t = p" for t p)+ @@ -6831,7 +6788,6 @@ lemma cteSwap_corres: apply (thin_tac "ksIdleThread t = p" for t p)+ apply (thin_tac "gsUserPages t = p" for t p)+ apply (thin_tac "pspace_relation s s'" for s s')+ - apply (thin_tac "ekheap_relation e p" for e p)+ apply (thin_tac "interrupt_state_relation n s s'" for n s s')+ apply (thin_tac "(s,s') \ arch_state_relation" for s s')+ apply (rule conjI) diff --git a/proof/refine/AARCH64/CSpace_R.thy b/proof/refine/AARCH64/CSpace_R.thy index acabae6d98..265010391f 100644 --- a/proof/refine/AARCH64/CSpace_R.thy +++ b/proof/refine/AARCH64/CSpace_R.thy @@ -694,8 +694,7 @@ lemma next_slot_eq2: lemma set_cap_not_quite_corres': assumes cr: - "pspace_relations (ekheap (a)) (kheap s) (ksPSpace s')" - "ekheap (s) = ekheap (a)" + "pspace_relation (kheap s) (ksPSpace s')" "cur_thread s = ksCurThread s'" "idle_thread s = ksIdleThread s'" "machine_state s = ksMachineState s'" @@ -712,10 +711,9 @@ lemma set_cap_not_quite_corres': assumes c: "cap_relation c c'" assumes p: "p' = cte_map p" shows "\t. ((),t) \ fst (set_cap c p s) \ - pspace_relations (ekheap t) (kheap t) (ksPSpace t') \ + pspace_relation (kheap t) (ksPSpace t') \ cdt t = cdt s \ cdt_list t = cdt_list (s) \ - ekheap t = ekheap (s) \ scheduler_action t = scheduler_action (s) \ ready_queues t = ready_queues (s) \ is_original_cap t = is_original_cap s \ @@ -732,7 +730,7 @@ lemma set_cap_not_quite_corres': domain_time t = ksDomainTime t'" apply (rule set_cap_not_quite_corres) using cr - apply (fastforce simp: c p pspace_relations_def)+ + apply (fastforce simp: c p)+ done context begin interpretation Arch . (*FIXME: arch-split*) @@ -804,7 +802,6 @@ lemma cteMove_corres: apply fastforce apply fastforce apply fastforce - apply (drule (1) pspace_relationsD) apply (drule_tac p=ptr' in set_cap_not_quite_corres, assumption+) apply fastforce apply fastforce @@ -864,7 +861,7 @@ lemma cteMove_corres: apply (frule(1) use_valid [OF _ updateCap_no_0]) apply (frule(2) use_valid [OF _ updateCap_no_0, OF _ use_valid [OF _ updateCap_no_0]]) apply (elim conjE) - apply (drule (5) updateMDB_the_lot', elim conjE) + apply (drule (4) updateMDB_the_lot', elim conjE) apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule (4) updateMDB_the_lot, elim conjE) @@ -892,7 +889,6 @@ lemma cteMove_corres: apply fastforce apply fastforce apply fastforce - apply (clarsimp simp: pspace_relations_def) apply (rule conjI) subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) apply (thin_tac "gsCNodes t = p" for t p)+ @@ -913,7 +909,6 @@ lemma cteMove_corres: apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ apply (thin_tac "ksDomainTime t = p" for t p)+ apply (thin_tac "ksDomSchedule t = p" for t p)+ - apply (thin_tac "ekheap_relation t p" for t p)+ apply (thin_tac "pspace_relation t p" for t p)+ apply (thin_tac "interrupt_state_relation s t p" for s t p)+ apply (thin_tac "ghost_relation s t p q" for s t p q)+ @@ -3538,7 +3533,7 @@ lemma deriveCap_untyped_derived: lemma setCTE_corres: "cap_relation cap (cteCap cte) \ - corres_underlying {(s, s'). pspace_relations (ekheap (s)) (kheap s) (ksPSpace s')} False True dc + corres_underlying {(s, s'). pspace_relation (kheap s) (ksPSpace s')} False True dc (pspace_distinct and pspace_aligned and valid_objs and cte_at p) (pspace_aligned' and pspace_distinct' and cte_at' (cte_map p)) (set_cap cap p) @@ -3604,7 +3599,7 @@ lemma ghost_relation_of_heap: done lemma corres_caps_decomposition: - assumes x: "corres_underlying {(s, s'). pspace_relations (ekheap (s)) (kheap s) (ksPSpace s')} False True r P P' f g" + assumes x: "corres_underlying {(s, s'). pspace_relation (kheap s) (ksPSpace s')} False True r P P' f g" assumes u: "\P. \\s. P (new_caps s)\ f \\rv s. P (caps_of_state s)\" "\P. \\s. P (new_mdb s)\ f \\rv s. P (cdt s)\" "\P. \\s. P (new_list s)\ f \\rv s. P (cdt_list (s))\" @@ -3717,13 +3712,11 @@ proof - note abs_irq_together = abs_irq_together'[simplified] show ?thesis unfolding state_relation_def swp_cte_at - apply (subst conj_assoc[symmetric]) - apply (subst pspace_relations_def[symmetric]) apply (rule corres_underlying_decomposition [OF x]) apply (simp add: ghost_relation_of_heap) apply (wpsimp wp: hoare_vcg_conj_lift mdb_wp rvk_wp list_wp u abs_irq_together simp: pt_types_of_heap_eq)+ - apply (intro z[simplified o_def] conjI | simp add: state_relation_def pspace_relations_def swp_cte_at - | (clarsimp, drule (1) z(6), simp add: state_relation_def pspace_relations_def swp_cte_at))+ + apply (intro z[simplified o_def] conjI | simp add: state_relation_def swp_cte_at + | (drule (1) z(6), simp add: state_relation_def swp_cte_at))+ done qed @@ -3735,7 +3728,7 @@ lemma getCTE_symb_exec_r: done lemma updateMDB_symb_exec_r: - "corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False nf' dc + "corres_underlying {(s, s'). pspace_relation (kheap s) (ksPSpace s')} False nf' dc \ (pspace_aligned' and pspace_distinct' and (no_0 \ ctes_of) and (\s. p \ 0 \ cte_at' p s)) (return ()) (updateMDB p m)" using no_fail_updateMDB [of p m] @@ -3782,9 +3775,13 @@ crunch setCTE (simp: setObject_def wp: updateObject_cte_inv) lemma set_original_symb_exec_l': - "corres_underlying {(s, s'). f (ekheap s) (kheap s) s'} False nf' dc P P' (set_original p b) (return x)" + "corres_underlying {(s, s'). f (kheap s) s'} False nf' dc P P' (set_original p b) (return x)" by (simp add: corres_underlying_def return_def set_original_def in_monad Bex_def) +crunch set_cap + for domain_index[wp]: "\s. P (domain_index s)" + (wp: set_object_wp) + lemma create_reply_master_corres: "\ sl' = cte_map sl ; AllowGrant \ rights \ \ corres dc @@ -4772,7 +4769,6 @@ lemma cteInsert_simple_corres: apply (simp+)[3] apply (clarsimp simp: corres_underlying_def state_relation_def in_monad valid_mdb'_def valid_mdb_ctes_def) - apply (drule (1) pspace_relationsD) apply (drule (18) set_cap_not_quite_corres) apply (rule refl) apply (elim conjE exE) @@ -4799,7 +4795,7 @@ lemma cteInsert_simple_corres: apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) - apply (clarsimp simp: pspace_relations_def) + apply clarsimp apply (rule conjI) subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) apply (thin_tac "gsCNodes t = p" for t p)+ @@ -4826,7 +4822,6 @@ lemma cteInsert_simple_corres: apply (thin_tac "ksDomainTime t = p" for t p)+ apply (thin_tac "ksDomSchedule t = p" for t p)+ apply (thin_tac "ctes_of t = p" for t p)+ - apply (thin_tac "ekheap_relation t p" for t p)+ apply (thin_tac "pspace_relation t p" for t p)+ apply (thin_tac "interrupt_state_relation s t p" for s t p)+ apply (thin_tac "sched_act_relation t p" for t p)+ @@ -5990,7 +5985,7 @@ lemma setCTE_set_cap_ready_queues_relation_valid_corres: shows "ready_queues_relation t t'" apply (clarsimp simp: ready_queues_relation_def) apply (insert pre) - apply (rule use_valid[OF step_abs set_cap_exst]) + apply (rule use_valid[OF step_abs set_cap_rqueues]) apply (rule use_valid[OF step_conc setCTE_ksReadyQueues]) apply (rule use_valid[OF step_conc setCTE_tcbSchedNexts_of]) apply (rule use_valid[OF step_conc setCTE_tcbSchedPrevs_of]) @@ -6016,7 +6011,6 @@ lemma updateCap_same_master: apply (clarsimp simp: cte_wp_at_ctes_of) apply clarsimp apply (clarsimp simp add: state_relation_def) - apply (drule (1) pspace_relationsD) apply (frule (4) set_cap_not_quite_corres_prequel) apply (erule cte_wp_at_weakenE, rule TrueI) apply assumption @@ -6027,7 +6021,7 @@ lemma updateCap_same_master: apply (rule bexI) prefer 2 apply assumption - apply (clarsimp simp: pspace_relations_def) + apply clarsimp apply (subst conj_assoc[symmetric]) apply (extract_conjunct \match conclusion in "ready_queues_relation a b" for a b \ -\) subgoal by (erule setCTE_set_cap_ready_queues_relation_valid_corres; assumption) diff --git a/proof/refine/AARCH64/Detype_R.thy b/proof/refine/AARCH64/Detype_R.thy index cecc4b5bd0..e968ffcb82 100644 --- a/proof/refine/AARCH64/Detype_R.thy +++ b/proof/refine/AARCH64/Detype_R.thy @@ -869,11 +869,6 @@ lemma corres_machine_op: apply (simp_all add: state_relation_def swp_def) done -lemma ekheap_relation_detype: - "ekheap_relation ekh kh \ - ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" - by (fastforce simp add: ekheap_relation_def split: if_split_asm) - lemma cap_table_at_gsCNodes_eq: "(s, s') \ state_relation \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" @@ -1017,11 +1012,11 @@ lemma detype_ready_queues_relation: tcb_of' |> tcbSchedPrev) (\d p. inQ d p |< ((\x. if lower \ x \ x \ upper then None else ksPSpace s' x) |> tcb_of'))" - apply (clarsimp simp: detype_ext_def ready_queues_relation_def Let_def) + apply (clarsimp simp: ready_queues_relation_def Let_def) apply (frule (1) detype_tcbSchedNexts_of[where S="{lower..upper}"]; simp) apply (frule (1) detype_tcbSchedPrevs_of[where S="{lower..upper}"]; simp) apply (frule (1) detype_inQ[where S="{lower..upper}"]; simp) - apply (fastforce simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def) + apply (fastforce simp add: detype_def wrap_ext_det_ext_ext_def) done lemma deleteObjects_corres: @@ -1084,35 +1079,31 @@ lemma deleteObjects_corres: apply (simp add: valid_pspace'_def) apply (rule state_relation_null_filterE, assumption, simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] - apply (simp add: detype_def, rule state.equality; - simp add: detype_ext_def wrap_ext_det_ext_ext_def) - apply (intro exI, fastforce) - apply (rule ext, clarsimp simp add: null_filter_def) - apply (rule sym, rule ccontr, clarsimp) - apply (drule(4) cte_map_not_null_outside') - apply (fastforce simp add: cte_wp_at_caps_of_state) - apply simp - apply (rule ext, clarsimp simp: null_filter'_def map_to_ctes_delete) + apply (simp add: detype_def) + apply (intro exI, fastforce) + apply (rule ext, clarsimp simp add: null_filter_def) apply (rule sym, rule ccontr, clarsimp) - apply (frule(2) pspace_relation_cte_wp_atI - [OF state_relation_pspace_relation]) - apply (elim exE) - apply (frule(4) cte_map_not_null_outside') - apply (rule cte_wp_at_weakenE, erule conjunct1) - apply (case_tac y, clarsimp) - apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def - valid_nullcaps_def) - apply clarsimp - apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, - erule cte_wp_at_weakenE[OF _ TrueI], assumption+) - apply (simp add: add_mask_fold) + apply (drule(4) cte_map_not_null_outside') + apply (fastforce simp add: cte_wp_at_caps_of_state) + apply simp + apply (rule ext, clarsimp simp: null_filter'_def map_to_ctes_delete) + apply (rule sym, rule ccontr, clarsimp) + apply (frule(2) pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (elim exE) + apply (frule(4) cte_map_not_null_outside') + apply (rule cte_wp_at_weakenE, erule conjunct1) + apply (case_tac y, clarsimp) + apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def + valid_nullcaps_def) + apply clarsimp + apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, + erule cte_wp_at_weakenE[OF _ TrueI], assumption+) apply (simp add: add_mask_fold) - apply (rule detype_pspace_relation[simplified], - simp_all add: state_relation_pspace_relation valid_pspace_def)[1] - apply (simp add: valid_cap'_def capAligned_def) - apply (clarsimp simp: valid_cap_def, assumption) - apply (fastforce simp: detype_def detype_ext_def add_mask_fold wrap_ext_det_ext_ext_def - intro!: ekheap_relation_detype) + apply (simp add: add_mask_fold) + apply (rule detype_pspace_relation[simplified], + simp_all add: state_relation_pspace_relation valid_pspace_def)[1] + apply (simp add: valid_cap'_def capAligned_def) + apply (clarsimp simp: valid_cap_def, assumption) apply (rule detype_ready_queues_relation; blast?) apply (clarsimp simp: deletionIsSafe_delete_locale_def) apply (erule state_relation_ready_queues_relation) @@ -3232,23 +3223,19 @@ lemma createObject_setCTE_commute: cteSizeBits_def) \ \Untyped\ apply (simp add: monad_commute_guard_imp[OF return_commute]) - \ \TCB, EP, NTFN\ + \ \TCB\ apply (rule monad_commute_guard_imp[OF commute_commute]) - apply (rule monad_commute_split[OF monad_commute_split]) - apply (rule monad_commute_split[OF commute_commute[OF return_commute]]) - apply (rule setCTE_modify_tcbDomain_commute) - apply wp - apply (rule curDomain_commute) - apply wp+ - apply (rule setCTE_placeNewObject_commute) - apply (wp placeNewObject_tcb_at' placeNewObject_cte_wp_at' - placeNewObject_pspace_distinct' - placeNewObject_pspace_aligned' - | clarsimp simp: objBits_simps')+ - apply (rule monad_commute_guard_imp[OF commute_commute] - ,rule monad_commute_split[OF commute_commute[OF return_commute]] - ,rule setCTE_placeNewObject_commute - ,(wp|clarsimp simp: objBits_simps')+)+ + apply (rule monad_commute_split[OF monad_commute_split[OF commute_commute]]) + apply (rule return_commute) + apply (rule setCTE_placeNewObject_commute) + apply wp + apply (rule curDomain_commute) + apply (wpsimp simp: objBits_simps')+ + \ \EP, NTFN\ + apply (rule monad_commute_guard_imp[OF commute_commute], + rule monad_commute_split[OF commute_commute[OF return_commute]], + rule setCTE_placeNewObject_commute, + (wpsimp simp: objBits_simps')+)+ \ \CNode\ apply (rule monad_commute_guard_imp[OF commute_commute]) apply (rule monad_commute_split)+ @@ -4487,6 +4474,34 @@ lemma createTCBs_tcb_at': apply (simp add: objBits_simps shiftl_t2n) done +lemma curDomain_createObjects'_comm: + "do x \ createObjects' ptr n obj us; + y \ curDomain; + m x y + od = + do y \ curDomain; + x \ createObjects' ptr n obj us; + m x y + od" + apply (rule ext) + apply (case_tac x) + by (auto simp: createObjects'_def split_def bind_assoc return_def unless_def + when_def simpler_gets_def alignError_def fail_def assert_def + bind_def curDomain_def modify_def get_def put_def + split: option.splits) + +lemma curDomain_twice_simp: + "do x \ curDomain; + y \ curDomain; + m x y + od = + do x \ curDomain; + m x x + od" + apply (rule ext) + apply (case_tac x) + by (auto simp: simpler_gets_def bind_def curDomain_def) + lemma createNewCaps_Cons: assumes cover:"range_cover ptr sz (Types_H.getObjectSize ty us) (Suc (Suc n))" and "valid_pspace' s" "valid_arch_state' s" @@ -4585,91 +4600,40 @@ proof - apiGetObjectSize_def shiftl_t2n field_simps shiftL_nat mapM_x_def sequence_x_def append fromIntegral_def integral_inv[unfolded Fun.comp_def]) - \ \TCB, EP, NTFN\ - apply (simp add: bind_assoc - AARCH64_H.getObjectSize_def - sequence_def Retype_H.createObject_def - AARCH64_H.toAPIType_def + \ \TCB\ + apply (simp add: bind_assoc AARCH64_H.getObjectSize_def + mapM_def sequence_def Retype_H.createObject_def + AARCH64_H.toAPIType_def objBitsKO_def createObjects_def AARCH64_H.createObject_def - Arch_createNewCaps_def comp_def + Arch_createNewCaps_def comp_def append apiGetObjectSize_def shiftl_t2n field_simps - shiftL_nat append mapM_x_append2 - fromIntegral_def integral_inv[unfolded Fun.comp_def])+ - apply (subst monad_eq) - apply (rule createObjects_Cons) - apply (simp add: field_simps shiftl_t2n bind_assoc pageBits_def - objBits_simps placeNewObject_def2)+ - apply (rule_tac Q = "\r s. pspace_aligned' s \ - pspace_distinct' s \ - pspace_no_overlap' (ptr + (2^tcbBlockSizeBits + of_nat n * 2^tcbBlockSizeBits)) (objBitsKO (KOTCB makeObject)) s \ - range_cover (ptr + 2^tcbBlockSizeBits) sz - (objBitsKO (KOTCB makeObject)) (Suc n) - \ (\x\set [0.e.of_nat n]. tcb_at' (ptr + x * 2^tcbBlockSizeBits) s)" - in monad_eq_split2) - apply simp - apply (subst monad_commute_simple[symmetric]) - apply (rule commute_commute[OF curDomain_commute]) - apply wpsimp+ - apply (rule_tac Q = "\r s. r = (ksCurDomain s) \ - pspace_aligned' s \ - pspace_distinct' s \ - pspace_no_overlap' (ptr + (2^tcbBlockSizeBits + of_nat n * 2^tcbBlockSizeBits)) (objBitsKO (KOTCB makeObject)) s \ - range_cover (ptr + 2^tcbBlockSizeBits) sz - (objBitsKO (KOTCB makeObject)) (Suc n) - \ (\x\set [0.e.of_nat n]. tcb_at' (ptr + x * 2^tcbBlockSizeBits) s) - " in monad_eq_split) - apply (subst monad_commute_simple[symmetric]) - apply (rule createObjects_setDomains_commute) - apply (clarsimp simp:objBits_simps) - apply (rule conj_impI) - apply (erule aligned_add_aligned) - apply (rule aligned_add_aligned[where n = tcbBlockSizeBits]) - apply (simp add:is_aligned_def objBits_defs) - apply (cut_tac is_aligned_shift[where m = tcbBlockSizeBits and k = "of_nat n", - unfolded shiftl_t2n,simplified]) - apply (simp add:field_simps)+ - apply (erule range_cover_full) - apply (simp add: word_bits_conv objBits_defs) - apply (rule_tac Q = "\x s. (ksCurDomain s) = r" in monad_eq_split2) - apply simp - apply (rule_tac Q = "\x s. (ksCurDomain s) = r" in monad_eq_split) - apply (subst rewrite_step[where f = curDomain and - P ="\s. ksCurDomain s = r" and f' = "return r"]) - apply (simp add:curDomain_def bind_def gets_def get_def) - apply simp - apply (simp add:mapM_x_singleton) - apply wp - apply simp - apply (wp mapM_x_wp') - apply simp - apply (simp add:curDomain_def,wp) - apply simp - apply (wp createObjects'_psp_aligned[where sz = sz] - createObjects'_psp_distinct[where sz = sz]) - apply (rule hoare_vcg_conj_lift) - apply (rule hoare_post_imp[OF _ - createObjects'_pspace_no_overlap[unfolded shiftl_t2n, - where gz = tcbBlockSizeBits and sz = sz, simplified]]) - apply (simp add:objBits_simps field_simps) - apply (simp add: objBits_simps) - apply (wp createTCBs_tcb_at'[where sz = sz]) - apply (clarsimp simp:objBits_simps word_bits_def field_simps) - apply (frule range_cover_le[where n = "Suc n"],simp+) - apply (drule range_cover_offset[where p = 1,rotated]) - apply simp - apply (simp add: objBits_defs) - apply (((simp add: bind_assoc - AARCH64_H.getObjectSize_def - mapM_def sequence_def Retype_H.createObject_def - AARCH64_H.toAPIType_def - createObjects_def AARCH64_H.createObject_def - Arch_createNewCaps_def comp_def - apiGetObjectSize_def shiftl_t2n field_simps - shiftL_nat mapM_x_def sequence_x_def append - fromIntegral_def integral_inv[unfolded Fun.comp_def])+ - , subst monad_eq, rule createObjects_Cons - , (simp add: field_simps shiftl_t2n bind_assoc pageBits_def - objBits_simps placeNewObject_def2)+)+)[2] + shiftL_nat fromIntegral_def integral_inv[unfolded Fun.comp_def]) + apply (subst curDomain_createObjects'_comm) + apply (subst curDomain_twice_simp) + apply (simp add: monad_eq_simp_state) + apply (intro conjI; clarsimp simp: in_monad) + apply ((fastforce simp: curDomain_def simpler_gets_def return_def placeNewObject_def2 + field_simps shiftl_t2n bind_assoc objBits_simps in_monad + createObjects_Cons[where + val="KOTCB (tcbDomain_update (\_. ksCurDomain s) makeObject)" + and s=s, simplified objBitsKO_def])+)[2] + apply ((clarsimp simp: curDomain_def simpler_gets_def return_def split_def bind_def + field_simps shiftl_t2n bind_assoc objBits_simps placeNewObject_def2 + createObjects_Cons[where + val="KOTCB (tcbDomain_update (\_. ksCurDomain s) makeObject)" + and s=s, simplified objBitsKO_def])+)[1] + \ \EP, NTFN\ + apply (((simp add: AARCH64_H.getObjectSize_def + mapM_def sequence_def Retype_H.createObject_def + AARCH64_H.toAPIType_def + createObjects_def AARCH64_H.createObject_def + Arch_createNewCaps_def comp_def + apiGetObjectSize_def shiftl_t2n field_simps + shiftL_nat mapM_x_def sequence_x_def append + fromIntegral_def integral_inv[unfolded Fun.comp_def])+, + subst monad_eq, rule createObjects_Cons, + (simp add: field_simps shiftl_t2n bind_assoc pageBits_def + objBits_simps' placeNewObject_def2)+)+)[2] apply (in_case "CapTableObject") apply (simp add: bind_assoc @@ -4693,6 +4657,7 @@ proof - apply (rule arg_cong2[where f=gsCNodes_update, OF ext refl]) apply (rule ext) apply simp + apply (in_case "HugePageObject") apply (simp add: Arch_createNewCaps_def Retype_H.createObject_def createObjects_def bind_assoc @@ -5128,35 +5093,19 @@ lemma createObject_pspace_no_overlap': apply wpc apply (wp ArchCreateObject_pspace_no_overlap') apply wpc - apply wp - apply (simp add:placeNewObject_def2) - apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 - | simp add: placeNewObject_def2 curDomain_def word_shiftl_add_distrib - field_simps)+ - apply (simp add:add.assoc[symmetric]) - apply (wp createObjects'_pspace_no_overlap2 - [where n =0 and sz = sz,simplified]) - apply (simp add:placeNewObject_def2) - apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 - | simp add: placeNewObject_def2 word_shiftl_add_distrib - field_simps)+ - apply (simp add:add.assoc[symmetric]) - apply (wp createObjects'_pspace_no_overlap2 - [where n =0 and sz = sz,simplified]) - apply (simp add:placeNewObject_def2) - apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 - | simp add: placeNewObject_def2 word_shiftl_add_distrib - field_simps)+ - apply (simp add:add.assoc[symmetric]) - apply (wp createObjects'_pspace_no_overlap2 - [where n =0 and sz = sz,simplified]) - apply (simp add:placeNewObject_def2) - apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 - | simp add: placeNewObject_def2 word_shiftl_add_distrib - field_simps)+ - apply (simp add:add.assoc[symmetric]) - apply (wp createObjects'_pspace_no_overlap2 - [where n =0 and sz = sz,simplified]) + apply wp + \ \TCB\ + apply (wp createObjects'_pspace_no_overlap2[where n =0 and sz = sz,simplified] + | simp add: curDomain_def placeNewObject_def2 word_shiftl_add_distrib field_simps)+ + apply (simp add:add.assoc[symmetric]) + apply (wp createObjects'_pspace_no_overlap2[where n =0 and sz = sz,simplified]) + apply (wpsimp simp: curDomain_def) + \ \other objects\ + apply ((wp createObjects'_pspace_no_overlap2 + | simp add: placeNewObject_def2 word_shiftl_add_distrib field_simps)+, + simp add:add.assoc[symmetric], + wp createObjects'_pspace_no_overlap2[where n =0 and sz = sz,simplified])+ + \ \Cleanup\ apply clarsimp apply (frule(1) range_cover_no_0[where p = n]) apply simp @@ -5174,10 +5123,9 @@ lemma createObject_pspace_no_overlap': apply (simp add:shiftl_t2n field_simps) apply (frule range_cover_offset[rotated,where p = n]) apply simp+ - apply (auto simp: word_shiftl_add_distrib field_simps shiftl_t2n elim: range_cover_le, - auto simp add: APIType_capBits_def fromAPIType_def objBits_def - dest!: to_from_apiTypeD) - done + by (auto simp: word_shiftl_add_distrib field_simps shiftl_t2n elim: range_cover_le) + (auto simp: APIType_capBits_def fromAPIType_def objBits_def objBits_simps + dest!: to_from_apiTypeD) crunch updatePTType for aligned'[wp]: pspace_aligned' diff --git a/proof/refine/AARCH64/Finalise_R.thy b/proof/refine/AARCH64/Finalise_R.thy index ed95bad7bb..c8db99da25 100644 --- a/proof/refine/AARCH64/Finalise_R.thy +++ b/proof/refine/AARCH64/Finalise_R.thy @@ -1624,7 +1624,7 @@ lemma emptySlot_corres: apply (simp add: put_def) apply (simp add: exec_gets exec_get exec_put del: fun_upd_apply | subst bind_def)+ apply (clarsimp simp: state_relation_def) - apply (drule updateMDB_the_lot, fastforce simp: pspace_relations_def, fastforce, fastforce) + apply (drule updateMDB_the_lot, fastforce simp: pspace_relation_def, fastforce, fastforce) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) apply (elim conjE) @@ -1653,7 +1653,7 @@ lemma emptySlot_corres: apply clarsimp apply (drule updateCap_stuff, elim conjE, erule (1) impE) apply clarsimp - apply (drule updateMDB_the_lot, force simp: pspace_relations_def, assumption+, simp) + apply (drule updateMDB_the_lot, force simp: pspace_relation_def, assumption+, simp) apply (rule bexI) prefer 2 apply (simp only: trans_state_update[symmetric]) @@ -1681,7 +1681,7 @@ lemma emptySlot_corres: apply (rule mdb_ptr_axioms.intro) subgoal by simp apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv) - apply (simp add: pspace_relations_def) + apply (simp add: pspace_relation_def) apply (rule conjI) apply (clarsimp simp: data_at_def ghost_relation_typ_at set_cap_a_type_inv) apply (rule conjI) @@ -3819,8 +3819,7 @@ lemma return_NullCap_pair_corres[corres]: lemma arch_finaliseCap_corres: "\ final_matters' (ArchObjectCap cap') \ final = final'; acap_relation cap cap' \ \ corres (\r r'. cap_relation (fst r) (fst r') \ cap_relation (snd r) (snd r')) - (\s. invs s \ valid_etcbs s - \ s \ cap.ArchObjectCap cap + (\s. invs s \ s \ cap.ArchObjectCap cap \ (final_matters (cap.ArchObjectCap cap) \ final = is_final_cap' (cap.ArchObjectCap cap) s) \ cte_wp_at ((=) (cap.ArchObjectCap cap)) sl s) diff --git a/proof/refine/AARCH64/Init_R.thy b/proof/refine/AARCH64/Init_R.thy index b75793a303..edaa9e4808 100644 --- a/proof/refine/AARCH64/Init_R.thy +++ b/proof/refine/AARCH64/Init_R.thy @@ -51,6 +51,12 @@ definition zeroed_main_abstract_state :: is_original_cap = \, cur_thread = 0, idle_thread = 0, + scheduler_action = resume_cur_thread, + domain_list = [], + domain_index = 0, + cur_domain = 0, + domain_time = 0, + ready_queues = (\_ _. []), machine_state = init_machine_state, interrupt_irq_node = (\irq. ucast irq << cte_level_bits), interrupt_states = (K irq_state.IRQInactive), @@ -62,13 +68,6 @@ definition zeroed_extended_state :: where "zeroed_extended_state \ \ work_units_completed_internal = 0, - scheduler_action_internal = resume_cur_thread, - ekheap_internal = Map.empty, - domain_list_internal = [], - domain_index_internal = 0, - cur_domain_internal = 0, - domain_time_internal = 0, - ready_queues_internal = (\_ _. []), cdt_list_internal = K [] \" @@ -119,8 +118,7 @@ lemma non_empty_refine_state_relation: "(zeroed_abstract_state, zeroed_intermediate_state) \ state_relation" apply (clarsimp simp: state_relation_def zeroed_state_defs state.defs) apply (intro conjI) - apply (clarsimp simp: pspace_relation_def pspace_dom_def) - apply (clarsimp simp: ekheap_relation_def) + apply (clarsimp simp: pspace_relation_def pspace_dom_def) apply (clarsimp simp: ready_queues_relation_def ready_queue_relation_def queue_end_valid_def opt_pred_def list_queue_relation_def tcbQueueEmpty_def prev_queue_head_def) diff --git a/proof/refine/AARCH64/Interrupt_R.thy b/proof/refine/AARCH64/Interrupt_R.thy index 407e022f64..46231249b9 100644 --- a/proof/refine/AARCH64/Interrupt_R.thy +++ b/proof/refine/AARCH64/Interrupt_R.thy @@ -600,7 +600,7 @@ lemma getIRQState_prop: lemma decDomainTime_corres: "corres dc \ \ dec_domain_time decDomainTime" apply (simp add:dec_domain_time_def corres_underlying_def decDomainTime_def simpler_modify_def) - apply (clarsimp simp:state_relation_def) + apply (clarsimp simp: state_relation_def cdt_relation_def) done lemma thread_state_case_if: @@ -634,24 +634,24 @@ lemma timerTick_corres: apply (rule corres_split[where r' = dc]) apply (rule corres_if[where Q = \ and Q' = \]) apply (case_tac state,simp_all)[1] - apply (rule_tac r'="(=)" in corres_split[OF ethreadget_corres]) - apply (simp add:etcb_relation_def) + apply (rule_tac r'="(=)" in corres_split[OF threadGet_corres]) + apply (simp add: tcb_relation_def) apply (rename_tac ts ts') apply (rule_tac R="1 < ts" in corres_cases) apply (simp) apply (unfold thread_set_time_slice_def) - apply (rule ethread_set_corres, simp+) - apply (clarsimp simp: etcb_relation_def) + apply (rule threadset_corres; simp add: tcb_relation_def inQ_def) apply simp - apply (rule corres_split[OF ethread_set_corres]) - apply (simp add: sch_act_wf_weak etcb_relation_def pred_conj_def)+ + apply (rule corres_split[OF threadset_corres]) + apply (simp add: sch_act_wf_weak tcb_relation_def pred_conj_def inQ_def)+ apply (rule corres_split[OF tcbSchedAppend_corres], simp) apply (rule rescheduleRequired_corres) apply wp apply ((wpsimp wp: tcbSchedAppend_sym_heap_sched_pointers tcbSchedAppend_valid_objs' | strengthen valid_objs'_valid_tcbs')+)[1] - apply ((wp thread_set_time_slice_valid_queues + apply ((wpsimp wp: thread_set_valid_queues thread_set_no_change_tcb_state + thread_set_weak_valid_sched_action | strengthen valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct)+)[1] apply ((wpsimp wp: threadSet_sched_pointers threadSet_valid_sched_pointers @@ -671,10 +671,10 @@ lemma timerTick_corres: threadSet_pred_tcb_at_state threadSet_weak_sch_act_wf rescheduleRequired_weak_sch_act_wf)+ apply (strengthen valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct) - apply (wpsimp wp: thread_set_time_slice_valid_queues) - apply ((wpsimp wp: thread_set_time_slice_valid_queues + apply (wpsimp wp: thread_set_valid_queues thread_set_weak_valid_sched_action) + apply ((wpsimp wp: thread_set_valid_queues | strengthen valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct)+)[1] - apply wpsimp + apply (wpsimp wp: thread_get_wp) apply wpsimp apply ((wpsimp wp: threadSet_sched_pointers threadSet_valid_sched_pointers threadSet_valid_objs' @@ -682,11 +682,8 @@ lemma timerTick_corres: | wp (once) hoare_drop_imp)+)[1] apply (wpsimp wp: gts_wp gts_wp')+ apply (clarsimp simp: cur_tcb_def) - apply (frule valid_sched_valid_etcbs) - apply (frule (1) tcb_at_is_etcb_at) apply (frule valid_sched_valid_queues) apply (fastforce simp: pred_tcb_at_def obj_at_def valid_sched_weak_strg) - apply (clarsimp simp: etcb_at_def split: option.splits) apply fastforce apply (fastforce simp: valid_state'_def ct_not_inQ_def) apply fastforce diff --git a/proof/refine/AARCH64/Invariants_H.thy b/proof/refine/AARCH64/Invariants_H.thy index c952717536..8293b29342 100644 --- a/proof/refine/AARCH64/Invariants_H.thy +++ b/proof/refine/AARCH64/Invariants_H.thy @@ -3314,9 +3314,6 @@ lemma invs'_invs_no_cicd: "invs' s \ all_invs_but_ct_idle_or_in_cur_domain' s" by (simp add: invs'_to_invs_no_cicd'_def) -lemma einvs_valid_etcbs: "einvs s \ valid_etcbs s" - by (clarsimp simp: valid_sched_def) - lemma invs'_bitmapQ_no_L1_orphans: "invs' s \ bitmapQ_no_L1_orphans s" by (simp add: invs'_def valid_state'_def valid_bitmaps_def) @@ -3576,4 +3573,24 @@ interpretation Arch . instance by intro_classes auto end +context Arch begin + +lemma objBits_less_word_bits: + "objBits v < word_bits" + unfolding objBits_simps' + apply (case_tac "injectKO v"; simp) + by (simp add: pageBits_def pteBits_def objBits_simps word_bits_def + split: arch_kernel_object.split)+ + +lemma objBits_pos_power2[simp]: + assumes "objBits v < word_bits" + shows "(1::machine_word) < (2::machine_word) ^ objBits v" + unfolding objBits_simps' + apply (insert assms) + apply (case_tac "injectKO v"; simp) + by (simp add: pageBits_def pteBits_def objBits_simps + split: arch_kernel_object.split)+ + +end + end diff --git a/proof/refine/AARCH64/IpcCancel_R.thy b/proof/refine/AARCH64/IpcCancel_R.thy index ae185783fc..58b4d61a5d 100644 --- a/proof/refine/AARCH64/IpcCancel_R.thy +++ b/proof/refine/AARCH64/IpcCancel_R.thy @@ -525,7 +525,7 @@ lemma (in delete_one) cancelIPC_ReplyCap_corres: apply (simp add: tcb_relation_def fault_rel_optionation_def) apply (simp add: tcb_cap_cases_def) apply (simp add: tcb_cte_cases_def cteSizeBits_def) - apply (simp add: exst_same_def) + apply (simp add: inQ_def) apply (fastforce simp: st_tcb_at_tcb_at) apply clarsimp defer @@ -1181,9 +1181,9 @@ crunch asUser crunch set_thread_state for in_correct_ready_q[wp]: in_correct_ready_q - (wp: crunch_wps) + (wp: set_object_wp) -crunch set_thread_state_ext +crunch set_thread_state_act for ready_qs_distinct[wp]: ready_qs_distinct (wp: crunch_wps) @@ -1193,6 +1193,10 @@ lemma set_thread_state_ready_qs_distinct[wp]: apply (wpsimp wp: set_object_wp) by (clarsimp simp: ready_qs_distinct_def) +crunch as_user + for in_correct_ready_q[wp]: in_correct_ready_q + (wp: set_object_wp) + lemma as_user_ready_qs_distinct[wp]: "as_user tptr f \ready_qs_distinct\" unfolding as_user_def @@ -1298,7 +1302,7 @@ proof - unfolding arch_thread_set_def archThreadSet_def by (corres' \(rotate_tac, erule tcb_rel) | (rule ball_tcb_cte_casesI; simp) | - simp add: exst_same_def tcb_cap_cases_def\ + simp add: tcb_cap_cases_def\ corres: getObject_TCB_corres setObject_update_TCB_corres') qed @@ -1496,7 +1500,7 @@ lemma sts_sch_act_not_ct[wp]: text \Cancelling all IPC in an endpoint or notification object\ lemma ep_cancel_corres_helper: - "corres dc ((\s. \t \ set list. tcb_at t s) and valid_etcbs and valid_queues + "corres dc ((\s. \t \ set list. tcb_at t s) and valid_queues and pspace_aligned and pspace_distinct) (valid_objs' and sym_heap_sched_pointers and valid_sched_pointers) (mapM_x (\t. do @@ -1533,7 +1537,7 @@ lemma ep_cancel_corres_helper: crunch set_simple_ko for ready_qs_distinct[wp]: ready_qs_distinct and in_correct_ready_q[wp]: in_correct_ready_q - (rule: ready_qs_distinct_lift wp: crunch_wps) + (wp: ready_qs_distinct_lift in_correct_ready_q_lift) lemma ep_cancel_corres: "corres dc (invs and valid_sched and ep_at ep) (invs' and ep_at' ep) @@ -1542,7 +1546,7 @@ proof - have P: "\list. corres dc (\s. (\t \ set list. tcb_at t s) \ valid_pspace s \ ep_at ep s - \ valid_etcbs s \ weak_valid_sched_action s \ valid_queues s) + \ weak_valid_sched_action s \ valid_queues s) (\s. (\t \ set list. tcb_at' t s) \ valid_pspace' s \ ep_at' ep s \ weak_sch_act_wf (ksSchedulerAction s) s \ valid_objs' s \ sym_heap_sched_pointers s \ valid_sched_pointers s) @@ -2261,7 +2265,7 @@ lemma cancelBadgedSends_corres: and pspace_distinct'"]]) apply (rule_tac S="(=)" and Q="\xs s. (\x \ set xs. (epptr, TCBBlockedSend) \ state_refs_of s x) \ - distinct xs \ valid_etcbs s \ + distinct xs \ in_correct_ready_q s \ ready_qs_distinct s \ pspace_aligned s \ pspace_distinct s" and Q'="\_ s. valid_objs' s \ sym_heap_sched_pointers s \ valid_sched_pointers s @@ -2285,7 +2289,7 @@ lemma cancelBadgedSends_corres: | strengthen valid_objs'_valid_tcbs')+ apply (clarsimp simp: valid_tcb_state_def tcb_at_def st_tcb_def2 st_tcb_at_refs_of_rev - dest!: state_refs_of_elemD elim!: tcb_at_is_etcb_at[rotated]) + dest!: state_refs_of_elemD) apply (simp add: valid_tcb_state'_def) apply (wp hoare_vcg_const_Ball_lift gts_wp | clarsimp)+ apply (wp hoare_vcg_imp_lift sts_st_tcb' sts_valid_objs' diff --git a/proof/refine/AARCH64/Ipc_R.thy b/proof/refine/AARCH64/Ipc_R.thy index 89fe5e8fbe..dd72894b4e 100644 --- a/proof/refine/AARCH64/Ipc_R.thy +++ b/proof/refine/AARCH64/Ipc_R.thy @@ -2192,7 +2192,7 @@ lemma doReplyTransfer_corres: apply (rule corres_split) apply (rule threadset_corresT; clarsimp simp add: tcb_relation_def fault_rel_optionation_def cteSizeBits_def - tcb_cap_cases_def tcb_cte_cases_def exst_same_def) + tcb_cap_cases_def tcb_cte_cases_def inQ_def) apply (rule_tac Q="valid_sched and cur_tcb and tcb_at receiver and pspace_aligned and pspace_distinct" and Q'="tcb_at' receiver and cur_tcb' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) @@ -3386,7 +3386,7 @@ lemma sendFaultIPC_corres: apply (rule corres_if2 [OF refl]) apply (simp add: dc_def[symmetric]) apply (rule corres_split[OF threadset_corres sendIPC_corres], simp_all)[1] - apply (simp add: tcb_relation_def fault_rel_optionation_def exst_same_def)+ + apply (simp add: tcb_relation_def fault_rel_optionation_def inQ_def)+ apply (wp thread_set_invs_trivial thread_set_no_change_tcb_state thread_set_typ_at ep_at_typ_at ex_nonz_cap_to_pres thread_set_cte_wp_at_trivial thread_set_not_state_valid_sched diff --git a/proof/refine/AARCH64/KHeap_R.thy b/proof/refine/AARCH64/KHeap_R.thy index cfc92c72d6..dc30e00899 100644 --- a/proof/refine/AARCH64/KHeap_R.thy +++ b/proof/refine/AARCH64/KHeap_R.thy @@ -1015,17 +1015,6 @@ lemma obj_relation_cut_same_type: arch_kernel_obj.split_asm arch_kernel_object.split_asm) done -definition exst_same :: "Structures_H.tcb \ Structures_H.tcb \ bool" -where - "exst_same tcb tcb' \ tcbPriority tcb = tcbPriority tcb' - \ tcbTimeSlice tcb = tcbTimeSlice tcb' - \ tcbDomain tcb = tcbDomain tcb'" - -fun exst_same' :: "Structures_H.kernel_object \ Structures_H.kernel_object \ bool" -where - "exst_same' (KOTCB tcb) (KOTCB tcb') = exst_same tcb tcb'" | - "exst_same' _ _ = True" - lemma tcbs_of'_non_tcb_update: "\typ_at' (koTypeOf ko) ptr s'; koTypeOf ko \ TCBT\ \ tcbs_of' (s'\ksPSpace := (ksPSpace s')(ptr \ ko)\) = tcbs_of' s'" @@ -1043,7 +1032,6 @@ lemma setObject_other_corres: \ map_to_ctes ((ksPSpace s) (ptr \ injectKO ob')) = map_to_ctes (ksPSpace s)" assumes t: "is_other_obj_relation_type (a_type ob)" assumes b: "\ko. P ko \ objBits ko = objBits ob'" - assumes e: "\ko. P ko \ exst_same' (injectKO ko) (injectKO ob')" assumes P: "\v::'a::pspace_storable. (1 :: machine_word) < 2 ^ objBits v" shows "other_obj_relation ob (injectKO (ob' :: 'a :: pspace_storable)) \ corres dc (obj_at (\ko. a_type ko = a_type ob) ptr and obj_at (same_caps ob) ptr) @@ -1094,21 +1082,6 @@ lemma setObject_other_corres: apply (insert t) apply ((erule disjE | clarsimp simp: is_other_obj_relation_type is_other_obj_relation_type_def a_type_def)+)[1] - apply (extract_conjunct \match conclusion in "ekheap_relation _ _" \ -\) - apply (simp only: ekheap_relation_def) - apply (rule ballI, drule(1) bspec) - apply (drule domD) - apply (insert e) - apply atomize - apply (clarsimp simp: obj_at'_def) - apply (erule_tac x=obj in allE) - apply (clarsimp simp: projectKO_eq project_inject) - apply (case_tac ob; - simp_all add: a_type_def other_obj_relation_def etcb_relation_def - is_other_obj_relation_type t exst_same_def)[1] - apply (clarsimp simp: is_other_obj_relation_type t exst_same_def - split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits - arch_kernel_obj.splits)+ \ \ready_queues_relation\ apply (prop_tac "koTypeOf (injectKO ob') \ TCBT") subgoal diff --git a/proof/refine/AARCH64/Refine.thy b/proof/refine/AARCH64/Refine.thy index fa4ebe573b..271fe40305 100644 --- a/proof/refine/AARCH64/Refine.thy +++ b/proof/refine/AARCH64/Refine.thy @@ -196,18 +196,27 @@ lemma absKState_correct: shows "absKState s' = abs_state s" using assms apply (intro state.equality, simp_all add: absKState_def abs_state_def) - apply (rule absHeap_correct, clarsimp+) - apply (clarsimp elim!: state_relationE) - apply (rule absCDT_correct, clarsimp+) - apply (rule absIsOriginalCap_correct, clarsimp+) + apply (rule absHeap_correct; clarsimp) + apply (clarsimp elim!: state_relationE) + apply (rule absCDT_correct; clarsimp) + apply (rule absIsOriginalCap_correct; clarsimp) + apply (simp add: state_relation_def) + apply (simp add: state_relation_def) + apply (clarsimp simp: state_relation_def) + apply (rule absSchedulerAction_correct, simp add: state_relation_def) + apply (simp add: state_relation_def) + apply (simp add: state_relation_def) + apply (simp add: state_relation_def) apply (simp add: state_relation_def) - apply (simp add: state_relation_def) + apply (simp add: state_relation_def ready_queues_relation_def ready_queue_relation_def Let_def + list_queue_relation_def) + apply (fastforce dest: heap_ls_is_walk) apply (clarsimp simp: user_mem_relation invs_def invs'_def) apply (simp add: state_relation_def) apply (rule absInterruptIRQNode_correct, simp add: state_relation_def) apply (rule absInterruptStates_correct, simp add: state_relation_def) apply (rule absArchState_correct, simp) - apply (rule absExst_correct, simp+) + apply (rule absExst_correct; simp) done text \The top-level invariance\ @@ -218,7 +227,7 @@ lemma set_thread_state_sched_act: \\rs s. P (scheduler_action (s::det_state))\" apply (simp add: set_thread_state_def) apply wp - apply (simp add: set_thread_state_ext_def) + apply (simp add: set_thread_state_act_def) apply wp apply (rule hoare_pre_cont) apply (rule_tac Q'="\rv. (\s. runnable ts) and (\s. P (scheduler_action s))" @@ -272,7 +281,7 @@ lemma kernel_entry_invs: apply clarsimp apply (simp add: kernel_entry_def) apply (wp akernel_invs_det_ext call_kernel_valid_sched thread_set_invs_trivial - thread_set_ct_running thread_set_not_state_valid_sched + thread_set_not_state_valid_sched hoare_vcg_disj_lift ct_in_state_thread_state_lift thread_set_no_change_tcb_state call_kernel_domain_time_inv_det_ext call_kernel_domain_list_inv_det_ext hoare_weak_lift_imp @@ -330,13 +339,13 @@ lemmas valid_list_inits[simp] = valid_list_init[simplified] lemma valid_sched_init[simp]: "valid_sched init_A_st" apply (simp add: valid_sched_def init_A_st_def ext_init_def) - apply (clarsimp simp: valid_etcbs_def init_kheap_def st_tcb_at_kh_def obj_at_kh_def - obj_at_def is_etcb_at_def idle_thread_ptr_def + apply (clarsimp simp: init_kheap_def st_tcb_at_kh_def obj_at_kh_def + obj_at_def idle_thread_ptr_def valid_queues_2_def ct_not_in_q_def not_queued_def valid_sched_action_def is_activatable_def init_irq_node_ptr_def arm_global_pt_ptr_def ct_in_cur_domain_2_def valid_blocked_2_def valid_idle_etcb_def - etcb_at'_def default_etcb_def) + etcb_at'_def etcbs_of'_def) done lemma valid_domain_list_init[simp]: @@ -465,27 +474,6 @@ lemma kernelEntry_invs': valid_domain_list'_def)+ done -lemma absKState_correct': - "\einvs s; invs' s'; (s,s') \ state_relation\ - \ absKState s' = abs_state s" - apply (intro state.equality, simp_all add: absKState_def abs_state_def) - apply (rule absHeap_correct) - apply (clarsimp simp: valid_state_def valid_pspace_def)+ - apply (clarsimp dest!: state_relationD) - apply (rule absCDT_correct) - apply (clarsimp simp: valid_state_def valid_pspace_def - valid_state'_def valid_pspace'_def)+ - apply (rule absIsOriginalCap_correct, clarsimp+) - apply (simp add: state_relation_def) - apply (simp add: state_relation_def) - apply (clarsimp simp: user_mem_relation invs_def invs'_def) - apply (simp add: state_relation_def) - apply (rule absInterruptIRQNode_correct, simp add: state_relation_def) - apply (rule absInterruptStates_correct, simp add: state_relation_def) - apply (erule absArchState_correct) - apply (rule absExst_correct, simp, assumption+) - done - lemma ptable_lift_abs_state[simp]: "ptable_lift t (abs_state s) = ptable_lift t s" by (simp add: ptable_lift_def abs_state_def) @@ -503,7 +491,7 @@ lemma ptable_rights_imp_UserData: shows "pointerInUserData y s' \ pointerInDeviceData y s'" proof - from invs invs' rel have [simp]: "absKState s' = abs_state s" - by - (rule absKState_correct', simp_all) + by - (rule absKState_correct, simp_all) from invs have valid: "valid_state s" by auto from invs' have valid': "valid_state' s'" by auto have "in_user_frame y s \ in_device_frame y s " @@ -669,11 +657,10 @@ lemma entry_corres: apply (rule corres_split) apply simp apply (rule threadset_corresT; simp?) - apply (simp add: tcb_relation_def arch_tcb_relation_def - arch_tcb_context_set_def atcbContextSet_def) - apply (clarsimp simp: tcb_cap_cases_def cteSizeBits_def) - apply (clarsimp simp: tcb_cte_cases_def cteSizeBits_def) - apply (simp add: exst_same_def) + apply (simp add: tcb_relation_def arch_tcb_relation_def + arch_tcb_context_set_def atcbContextSet_def) + apply (clarsimp simp: tcb_cap_cases_def cteSizeBits_def) + apply (clarsimp simp: tcb_cte_cases_def cteSizeBits_def) apply (rule corres_split[OF kernel_corres]) apply (rule corres_split_eqr[OF getCurThread_corres]) apply (rule threadGet_corres) @@ -683,7 +670,7 @@ lemma entry_corres: apply (rule hoare_strengthen_post, rule akernel_invs_det_ext, simp add: invs_def valid_state_def valid_pspace_def cur_tcb_def) apply (rule hoare_strengthen_post, rule ckernel_invs, simp add: invs'_def cur_tcb'_def) - apply (wp thread_set_invs_trivial thread_set_ct_running + apply (wp thread_set_invs_trivial threadSet_invs_trivial threadSet_ct_running' thread_set_not_state_valid_sched hoare_weak_lift_imp hoare_vcg_disj_lift ct_in_state_thread_state_lift diff --git a/proof/refine/AARCH64/Retype_R.thy b/proof/refine/AARCH64/Retype_R.thy index 6625f1857f..13c7c3faf9 100644 --- a/proof/refine/AARCH64/Retype_R.thy +++ b/proof/refine/AARCH64/Retype_R.thy @@ -77,14 +77,14 @@ where | VCPUObject \ vcpuBits" definition - makeObjectKO :: "bool \ (kernel_object + AARCH64_H.object_type) \ kernel_object" + makeObjectKO :: "bool \ domain \ (kernel_object + AARCH64_H.object_type) \ kernel_object" where - "makeObjectKO dev ty \ case ty of + "makeObjectKO dev d ty \ case ty of Inl KOUserData \ Some KOUserData | Inl (KOArch (KOASIDPool _)) \ Some (KOArch (KOASIDPool makeObject)) | Inl (KOArch (KOVCPU _)) \ Some (KOArch (KOVCPU makeObject)) | Inr VCPUObject \ Some (KOArch (KOVCPU makeObject)) - | Inr (APIObjectType ArchTypes_H.TCBObject) \ Some (KOTCB makeObject) + | Inr (APIObjectType ArchTypes_H.TCBObject) \ Some (KOTCB (tcbDomain_update (\_. d) makeObject)) | Inr (APIObjectType ArchTypes_H.EndpointObject) \ Some (KOEndpoint makeObject) | Inr (APIObjectType ArchTypes_H.NotificationObject) \ Some (KONotification makeObject) | Inr (APIObjectType ArchTypes_H.CapTableObject) \ Some (KOCTE makeObject) @@ -111,6 +111,12 @@ lemma valid_obj_makeObject_tcb [simp]: by (clarsimp simp: makeObject_tcb makeObject_cte tcb_cte_cases_def minBound_word newArchTCB_def cteSizeBits_def) +lemma valid_obj_makeObject_tcb_tcbDomain_update [simp]: + "d \ maxDomain \ valid_obj' (KOTCB (tcbDomain_update (\_. d) makeObject)) s" + unfolding valid_obj'_def valid_tcb'_def valid_tcb_state'_def valid_arch_tcb'_def + by (clarsimp simp: makeObject_tcb makeObject_cte objBits_simps' newArchTCB_def + tcb_cte_cases_def maxDomain_def maxPriority_def numPriorities_def minBound_word) + lemma valid_obj_makeObject_endpoint [simp]: "valid_obj' (KOEndpoint makeObject) s" unfolding valid_obj'_def valid_ep'_def @@ -301,15 +307,14 @@ lemma cte_at_next_slot'': lemma state_relation_null_filterE: - "\ (s, s') \ state_relation; t = kheap_update f (ekheap_update ef s); + "\ (s, s') \ state_relation; t = kheap_update f s; \f' g' h' pt_fn'. t' = s'\ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s'), ksArchState := (ksArchState s') \gsPTTypes := pt_fn' (gsPTTypes (ksArchState s'))\\; null_filter (caps_of_state t) = null_filter (caps_of_state s); null_filter' (ctes_of t') = null_filter' (ctes_of s'); - pspace_relation (kheap t) (ksPSpace t'); - ekheap_relation (ekheap t) (ksPSpace t'); ready_queues_relation t t'; + pspace_relation (kheap t) (ksPSpace t'); ready_queues_relation t t'; ghost_relation (kheap t) (gsUserPages t') (gsCNodes t') (gsPTTypes (ksArchState t')); valid_list s; pspace_aligned' s'; pspace_distinct' s'; valid_objs s; valid_mdb s; @@ -328,13 +333,12 @@ lemma state_relation_null_filterE: apply (case_tac "cdt s (a, b)") apply (subst mdb_cte_at_no_descendants, assumption) apply (simp add: cte_wp_at_caps_of_state swp_def) - apply (cut_tac s="kheap_update f (ekheap_update ef s)" and + apply (cut_tac s="kheap_update f s" and s'="s'\ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'), gsCNodes := h' (gsCNodes s'), ksArchState := ksArchState s' \gsPTTypes := pt_fn' (gsPTTypes (ksArchState s'))\\" in pspace_relation_ctes_ofI, simp_all)[1] - apply (simp add: trans_state_update[symmetric] del: trans_state_update) apply (erule caps_of_state_cteD) apply (clarsimp simp: descendants_of'_def) apply (case_tac cte) @@ -439,12 +443,12 @@ lemma foldr_update_obj_at': done lemma makeObjectKO_eq: - assumes x: "makeObjectKO dev tp = Some v" + assumes x: "makeObjectKO dev d tp = Some v" shows "(v = KOCTE cte) = (tp = Inr (APIObjectType ArchTypes_H.CapTableObject) \ cte = makeObject)" "(v = KOTCB tcb) = - (tp = Inr (APIObjectType ArchTypes_H.TCBObject) \ tcb = makeObject)" + (tp = Inr (APIObjectType ArchTypes_H.TCBObject) \ tcb = (tcbDomain_update (\_. d) makeObject))" using x by (simp add: makeObjectKO_def eq_commute split: apiobject_type.split_asm sum.split_asm kernel_object.split_asm @@ -499,7 +503,7 @@ lemma ps_clearD: done lemma cte_wp_at_retype': - assumes ko: "makeObjectKO dev tp = Some obj" + assumes ko: "makeObjectKO dev d tp = Some obj" and pv: "pspace_aligned' s" "pspace_distinct' s" and pv': "pspace_aligned' (ksPSpace_update (\x xa. if xa \ set addrs then Some obj else ksPSpace s xa) s)" "pspace_distinct' (ksPSpace_update (\x xa. if xa \ set addrs then Some obj else ksPSpace s xa) s)" @@ -518,13 +522,14 @@ lemma cte_wp_at_retype': apply (subgoal_tac "(\P :: cte \ bool. obj_at' P p ?s') \ (\ (\P :: tcb \ bool. obj_at' P (p && ~~ mask tcbBlockSizeBits) ?s'))") apply (simp only: cte_wp_at_obj_cases_mask foldr_update_obj_at'[OF pv pv' al]) - apply (simp add: the_ctes_makeObject makeObjectKO_eq [OF ko] makeObject_cte dom_def - split del: if_split - cong: if_cong) + apply (simp add: the_ctes_makeObject makeObjectKO_eq [OF ko] makeObject_cte + split del: if_split + cong: if_cong) apply (insert al ko) - apply (simp, safe, simp_all) - apply fastforce - apply fastforce + apply simp + apply (safe; simp) + apply ((fastforce simp: makeObjectKO_def makeObject_cte makeObject_tcb tcb_cte_cases_def + split: if_split_asm)+)[10] apply (clarsimp elim!: obj_atE' simp: objBits_simps) apply (drule ps_clearD[where y=p and n=tcbBlockSizeBits]) apply simp @@ -538,7 +543,7 @@ lemma cte_wp_at_retype': done lemma ctes_of_retype: - assumes ko: "makeObjectKO dev tp = Some obj" + assumes ko: "makeObjectKO dev d tp = Some obj" and pv: "pspace_aligned' s" "pspace_distinct' s" and pv': "pspace_aligned' (ksPSpace_update (\x xa. if xa \ set addrs then Some obj else ksPSpace s xa) s)" "pspace_distinct' (ksPSpace_update (\x xa. if xa \ set addrs then Some obj else ksPSpace s xa) s)" @@ -567,7 +572,7 @@ lemma None_ctes_of_cte_at: by (fastforce simp add: cte_wp_at_ctes_of) lemma null_filter_ctes_retype: - assumes ko: "makeObjectKO dev tp = Some obj" + assumes ko: "makeObjectKO dev d tp = Some obj" and pv: "pspace_aligned' s" "pspace_distinct' s" and pv': "pspace_aligned' (ksPSpace_update (\x xa. if xa \ set addrs then Some obj else ksPSpace s xa) s)" "pspace_distinct' (ksPSpace_update (\x xa. if xa \ set addrs then Some obj else ksPSpace s xa) s)" @@ -598,7 +603,8 @@ lemma null_filter_ctes_retype: apply (insert ko[symmetric], simp add: makeObjectKO_def objBits_simps) apply clarsimp apply (subst(asm) subtract_mask[symmetric], - erule_tac v="if x \ set addrs then KOTCB makeObject else KOCTE cte" + erule_tac v="if x \ set addrs then KOTCB (tcbDomain_update (\_. d) makeObject) + else KOCTE cte" in tcb_space_clear) apply (simp add: is_aligned_mask word_bw_assocs) apply assumption @@ -726,13 +732,13 @@ lemma obj_relation_retype_leD: by (simp add: obj_relation_retype_def) lemma obj_relation_retype_default_leD: - "\ obj_relation_retype (default_object (APIType_map2 ty) dev us) ko; + "\ obj_relation_retype (default_object (APIType_map2 ty) dev us d) ko; ty \ Inr (APIObjectType ArchTypes_H.Untyped) \ \ objBitsKO ko \ obj_bits_api (APIType_map2 ty) us" by (simp add: obj_relation_retype_def objBits_def obj_bits_dev_irr) lemma makeObjectKO_Untyped: - "makeObjectKO dev ty = Some v \ ty \ Inr (APIObjectType ArchTypes_H.Untyped)" + "makeObjectKO dev d ty = Some v \ ty \ Inr (APIObjectType ArchTypes_H.Untyped)" by (clarsimp simp: makeObjectKO_def) lemma obj_relation_cuts_trivial: @@ -754,10 +760,10 @@ lemma obj_relation_cuts_trivial: lemma obj_relation_retype_addrs_eq: assumes not_unt:"ty \ Inr (APIObjectType ArchTypes_H.Untyped)" assumes amp: "m = 2^ ((obj_bits_api (APIType_map2 ty) us) - (objBitsKO ko)) * n" - assumes orr: "obj_relation_retype (default_object (APIType_map2 ty) dev us) ko" + assumes orr: "obj_relation_retype (default_object (APIType_map2 ty) dev us d) ko" shows "\ range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n \ \ (\x \ set (retype_addrs ptr (APIType_map2 ty) n us). - fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) + fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us d) x) = set (new_cap_addrs m ptr ko)" apply (rule set_eqI, rule iffI) apply (clarsimp simp: retype_addrs_def) @@ -817,7 +823,7 @@ lemma obj_relation_retype_addrs_eq: done lemma objBits_le_obj_bits_api: - "makeObjectKO dev ty = Some ko \ + "makeObjectKO dev d ty = Some ko \ objBitsKO ko \ obj_bits_api (APIType_map2 ty) us" apply (case_tac ty) apply (auto simp: default_arch_object_def bit_simps @@ -846,12 +852,12 @@ lemma retype_pspace_relation: and vs': "pspace_aligned' s'" "pspace_distinct' s'" and pn: "pspace_no_overlap_range_cover ptr sz s" and pn': "pspace_no_overlap' ptr sz s'" - and ko: "makeObjectKO dev ty = Some ko" + and ko: "makeObjectKO dev d ty = Some ko" and cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" - and orr: "obj_relation_retype (default_object (APIType_map2 ty) dev us) ko" + and orr: "obj_relation_retype (default_object (APIType_map2 ty) dev us d) ko" and num_r: "m = 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n" shows - "pspace_relation (foldr (\p ps. ps(p \ default_object (APIType_map2 ty) dev us)) + "pspace_relation (foldr (\p ps. ps(p \ default_object (APIType_map2 ty) dev us d)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))" (is "pspace_relation ?ps ?ps'") @@ -870,7 +876,7 @@ proof "set (retype_addrs ptr (APIType_map2 ty) n us) \ dom (kheap s) = {}" by auto - note pdom = pspace_dom_upd [OF dom_Int_ra, where ko="default_object (APIType_map2 ty) dev us"] + note pdom = pspace_dom_upd [OF dom_Int_ra, where ko="default_object (APIType_map2 ty) dev us d"] have pdom': "dom ?ps' = dom (ksPSpace s') \ set (new_cap_addrs m ptr ko)" by (clarsimp simp add: foldr_upd_app_if[folded data_map_insert_def] @@ -942,79 +948,6 @@ lemma foldr_upd_app_if': "foldr (\p ps. ps(p := f p)) as g = (\x apply simp done -lemma etcb_rel_makeObject: "etcb_relation default_etcb makeObject" - apply (simp add: etcb_relation_def default_etcb_def) - apply (simp add: makeObject_tcb default_priority_def default_domain_def) - done - - -lemma ekh_at_tcb_at: "valid_etcbs_2 ekh kh \ ekh x = Some y \ \tcb. kh x = Some (TCB tcb)" - apply (simp add: valid_etcbs_2_def - st_tcb_at_kh_def obj_at_kh_def - is_etcb_at'_def obj_at_def) - apply force - done - -lemma default_etcb_default_domain_futz [simp]: - "default_etcb\tcb_domain := default_domain\ = default_etcb" -unfolding default_etcb_def by simp - -lemma retype_ekheap_relation: - assumes sr: "ekheap_relation (ekheap s) (ksPSpace s')" - and sr': "pspace_relation (kheap s) (ksPSpace s')" - and vs: "valid_pspace s" "valid_mdb s" - and et: "valid_etcbs s" - and vs': "pspace_aligned' s'" "pspace_distinct' s'" - and pn: "pspace_no_overlap_range_cover ptr sz s" - and pn': "pspace_no_overlap' ptr sz s'" - and ko: "makeObjectKO dev ty = Some ko" - and cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" - and orr: "obj_relation_retype (default_object (APIType_map2 ty) dev us) ko" - and num_r: "m = 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n" - shows - "ekheap_relation (foldr (\p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) - (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) - (foldr (\addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))" - (is "ekheap_relation ?ps ?ps'") - proof - - have not_unt: "ty \ Inr (APIObjectType ArchTypes_H.Untyped)" - by (rule makeObjectKO_Untyped[OF ko]) - show ?thesis - apply (case_tac "ty \ Inr (APIObjectType apiobject_type.TCBObject)") - apply (insert ko) - apply (cut_tac retype_pspace_relation[OF sr' vs vs' pn pn' ko cover orr num_r]) - apply (simp add: foldr_upd_app_if' foldr_upd_app_if[folded data_map_insert_def]) - apply (simp add: obj_relation_retype_addrs_eq[OF not_unt num_r orr cover,symmetric]) - apply (insert sr) - apply (clarsimp simp add: ekheap_relation_def - pspace_relation_def default_ext_def cong: if_cong - split: if_split_asm) - subgoal by (clarsimp simp add: makeObjectKO_def APIType_map2_def cong: if_cong - split: sum.splits Structures_H.kernel_object.splits - arch_kernel_object.splits AARCH64_H.object_type.splits apiobject_type.splits) - - apply (frule ekh_at_tcb_at[OF et]) - apply (intro impI conjI) - apply clarsimp - apply (drule_tac x=a in bspec,force) - apply (clarsimp simp: tcb_relation_cut_def split: if_split_asm) - apply (case_tac ko,simp_all) - apply (clarsimp simp add: makeObjectKO_def cong: if_cong split: sum.splits Structures_H.kernel_object.splits - arch_kernel_object.splits AARCH64_H.object_type.splits - apiobject_type.splits if_split_asm) - apply (drule_tac x=xa in bspec,simp) - subgoal by force - subgoal by force - apply (simp add: foldr_upd_app_if' foldr_upd_app_if[folded data_map_insert_def]) - apply (simp add: obj_relation_retype_addrs_eq[OF not_unt num_r orr cover,symmetric]) - apply (clarsimp simp add: APIType_map2_def default_ext_def ekheap_relation_def - default_object_def makeObjectKO_def etcb_rel_makeObject - cong: if_cong - split: if_split_asm) - apply force - done -qed - lemma pspace_no_overlapD': "\ ksPSpace s x = Some ko; pspace_no_overlap' p bits s \ \ {x .. x + 2 ^ objBitsKO ko - 1} \ {p .. (p && ~~ mask bits) + 2 ^ bits - 1} = {}" @@ -1214,7 +1147,7 @@ lemma retype_ksPSpace_dom_same: fixes x v assumes vs': "pspace_aligned' s'" "pspace_distinct' s'" assumes pn': "pspace_no_overlap' ptr sz s'" - assumes ko: "makeObjectKO dev ty = Some ko" + assumes ko: "makeObjectKO dev d ty = Some ko" assumes cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" assumes num_r: "m = 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n" shows @@ -1253,7 +1186,7 @@ qed lemma retype_tcbSchedPrevs_of: assumes vs': "pspace_aligned' s'" "pspace_distinct' s'" assumes pn': "pspace_no_overlap' ptr sz s'" - assumes ko: "makeObjectKO dev ty = Some ko" + assumes ko: "makeObjectKO dev d ty = Some ko" assumes cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" assumes num_r: "m = 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n" shows @@ -1279,7 +1212,7 @@ qed lemma retype_tcbSchedNexts_of: assumes vs': "pspace_aligned' s'" "pspace_distinct' s'" assumes pn': "pspace_no_overlap' ptr sz s'" - assumes ko: "makeObjectKO dev ty = Some ko" + assumes ko: "makeObjectKO dev d ty = Some ko" assumes cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" assumes num_r: "m = 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n" shows @@ -1305,7 +1238,7 @@ qed lemma retype_inQ: assumes vs': "pspace_aligned' s'" "pspace_distinct' s'" assumes pn': "pspace_no_overlap' ptr sz s'" - assumes ko: "makeObjectKO dev ty = Some ko" + assumes ko: "makeObjectKO dev d ty = Some ko" assumes cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" assumes num_r: "m = 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n" shows @@ -1334,12 +1267,12 @@ lemma retype_ready_queues_relation: assumes rlqr: "ready_queues_relation s s'" assumes vs': "pspace_aligned' s'" "pspace_distinct' s'" assumes pn': "pspace_no_overlap' ptr sz s'" - assumes ko: "makeObjectKO dev ty = Some ko" + assumes ko: "makeObjectKO dev d ty = Some ko" assumes cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" assumes num_r: "m = 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n" shows "ready_queues_relation - (s \kheap := foldr (\p. data_map_insert p (default_object (APIType_map2 ty) dev us)) + (s \kheap := foldr (\p. data_map_insert p (default_object (APIType_map2 ty) dev us d)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\) (s'\ksPSpace := foldr (\addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\)" using rlqr @@ -1352,31 +1285,28 @@ lemma retype_state_relation: notes data_map_insert_def[simp del] assumes sr: "(s, s') \ state_relation" and vs: "valid_pspace s" "valid_mdb s" - and et: "valid_etcbs s" "valid_list s" + and et: "valid_list s" and vs': "pspace_aligned' s'" "pspace_distinct' s'" and pn: "pspace_no_overlap_range_cover ptr sz s" and pn': "pspace_no_overlap' ptr sz s'" and cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" - and ko: "makeObjectKO dev ty = Some ko" + and ko: "makeObjectKO dev d ty = Some ko" and api: "obj_bits_api (APIType_map2 ty) us \ sz" - and orr: "obj_relation_retype (default_object (APIType_map2 ty) dev us) ko" + and orr: "obj_relation_retype (default_object (APIType_map2 ty) dev us d) ko" and num_r: "m = 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n" shows - "(ekheap_update - (\_. foldr (\p ekh a. if a = p then default_ext (APIType_map2 ty) default_domain else ekh a) - (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) - s - \kheap := - foldr (\p. data_map_insert p (default_object (APIType_map2 ty) dev us)) + "(s \kheap := + foldr (\p. data_map_insert p (default_object (APIType_map2 ty) dev us d)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)\, update_gs (APIType_map2 ty) us (set (retype_addrs ptr (APIType_map2 ty) n us)) (s'\ksPSpace := foldr (\addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')\)) \ state_relation" - (is "(ekheap_update (\_. ?eps) s\kheap := ?ps\, update_gs _ _ _ (s'\ksPSpace := ?ps'\)) + (is "(s\kheap := ?ps\, update_gs _ _ _ (s'\ksPSpace := ?ps'\)) \ state_relation") - proof (rule state_relation_null_filterE[OF sr refl _ _ _ _ _ _ _ _ vs'], simp_all add: trans_state_update[symmetric] del: trans_state_update) + proof (rule state_relation_null_filterE[OF sr refl _ _ _ _ _ _ _ vs'], + simp_all add: trans_state_update[symmetric] del: trans_state_update) have cover':"range_cover ptr sz (objBitsKO ko) m" by (rule range_cover_rel[OF cover objBits_le_obj_bits_api[OF ko] num_r]) @@ -1442,12 +1372,6 @@ lemma retype_state_relation: by (rule retype_pspace_relation [OF _ vs vs' pn pn' ko cover orr num_r, folded data_map_insert_def]) - have "ekheap_relation (ekheap (s)) (ksPSpace s')" - using sr by (simp add: state_relation_def) - - thus "ekheap_relation ?eps ?ps'" - by (fold fun_upd_apply) (rule retype_ekheap_relation[OF _ pspr vs et(1) vs' pn pn' ko cover orr num_r]) - have pn2: "\a\set ?al. kheap s a = None" by (rule ccontr) (clarsimp simp: pspace_no_overlapD1[OF pn _ cover vs(1)]) @@ -1642,208 +1566,6 @@ lemma objBitsKO_gt_0: "0 < objBitsKO ko" apply (simp_all add:archObjSize_def bit_simps) done -lemma kheap_ekheap_double_gets: - "(\rv erv rv'. \pspace_relation rv rv'; ekheap_relation erv rv'\ - \ corres r (R rv erv) (R' rv') (b rv erv) (d rv')) \ - corres r (\s. R (kheap s) (ekheap s) s) (\s. R' (ksPSpace s) s) - (do x \ gets kheap; xa \ gets ekheap; b x xa od) (gets ksPSpace >>= d)" - apply (rule corres_symb_exec_l) - apply (rule corres_guard_imp) - apply (rule_tac r'= "\erv rv'. ekheap_relation erv rv' \ pspace_relation x rv'" - in corres_split) - apply (subst corres_gets[where P="\s. x = kheap s" and P'=\]) - apply clarsimp - apply (simp add: state_relation_def) - apply clarsimp - apply assumption - apply (wp gets_exs_valid | simp)+ - done - -(* - -Split out the extended operation that sets the etcb domains. - -This allows the existing corres proofs in this file to more-or-less go -through as they stand. - -A more principled fix would be to change the abstract spec and -generalise init_arch_objects to initialise other object types. - -*) - -definition retype_region2_ext :: "obj_ref list \ Structures_A.apiobject_type \ unit det_ext_monad" where - "retype_region2_ext ptrs type \ modify (\s. ekheap_update (foldr (\p ekh. (ekh(p := default_ext type default_domain))) ptrs) s)" - -crunch retype_region2_ext - for all_but_exst[wp]: "all_but_exst P" -crunch retype_region2_ext - for (empty_fail) empty_fail[wp] - -end - -interpretation retype_region2_ext_extended: is_extended "retype_region2_ext ptrs type" - by (unfold_locales; wp) - -context begin interpretation Arch . (*FIXME: arch-split*) - -definition - "retype_region2_extra_ext ptrs type \ - when (type = Structures_A.TCBObject) (do - cdom \ gets cur_domain; - mapM_x (ethread_set (\tcb. tcb\tcb_domain := cdom\)) ptrs - od)" - -crunch retype_region2_extra_ext - for all_but_exst[wp]: "all_but_exst P" (wp: mapM_x_wp) -crunch retype_region2_extra_ext - for (empty_fail) empty_fail[wp] (wp: mapM_x_wp) - -end - -interpretation retype_region2_extra_ext_extended: is_extended "retype_region2_extra_ext ptrs type" - by (unfold_locales; wp) - -context begin interpretation Arch . (*FIXME: arch-split*) - -definition - retype_region2 :: "obj_ref \ nat \ nat \ Structures_A.apiobject_type \ bool \ (obj_ref list,'z::state_ext) s_monad" -where - "retype_region2 ptr numObjects o_bits type dev \ do - obj_size \ return $ 2 ^ obj_bits_api type o_bits; - ptrs \ return $ map (\p. ptr_add ptr (p * obj_size)) [0..< numObjects]; - when (type \ Structures_A.Untyped) (do - kh \ gets kheap; - kh' \ return $ foldr (\p kh. kh(p \ default_object type dev o_bits)) ptrs kh; - do_extended_op (retype_region2_ext ptrs type); - modify $ kheap_update (K kh') - od); - return $ ptrs - od" - -lemma retype_region_ext_modify_kheap_futz: - "(retype_region2_extra_ext ptrs type :: (unit, det_ext) s_monad) >>= (\_. modify (kheap_update f)) - = (modify (kheap_update f) >>= (\_. retype_region2_extra_ext ptrs type))" - apply (clarsimp simp: retype_region_ext_def retype_region2_ext_def retype_region2_extra_ext_def when_def bind_assoc) - apply (subst oblivious_modify_swap) - defer - apply (simp add: bind_assoc) - apply (rule oblivious_bind) - apply simp - apply (rule oblivious_mapM_x) - apply (clarsimp simp: ethread_set_def set_eobject_def) - apply (rule oblivious_bind) - apply (simp add: gets_the_def) - apply (rule oblivious_bind) - apply (clarsimp simp: get_etcb_def) - apply simp - apply (simp add: modify_def[symmetric]) -done - -lemmas retype_region_ext_modify_kheap_futz' = fun_cong[OF arg_cong[where f=Nondet_Monad.bind, OF retype_region_ext_modify_kheap_futz[symmetric]], simplified bind_assoc] - -lemma foldr_upd_app_if_eta_futz: - "foldr (\p ps. ps(p \ f p)) as = (\g x. if x \ set as then Some (f x) else g x)" -apply (rule ext) -apply (rule foldr_upd_app_if) -done - -lemma modify_ekheap_update_comp_futz: - "modify (ekheap_update (f \ g)) = modify (ekheap_update g) >>= (K (modify (ekheap_update f)))" -by (simp add: o_def modify_def bind_def gets_def get_def put_def) - -lemma mapM_x_modify_futz: - assumes "\ptr\set ptrs. ekheap s ptr \ None" - shows "mapM_x (ethread_set F) (rev ptrs) s - = modify (ekheap_update (foldr (\p ekh. ekh(p := Some (F (the (ekh p))))) ptrs)) s" (is "?lhs ptrs s = ?rhs ptrs s") -using assms -proof(induct ptrs arbitrary: s) - case Nil thus ?case by (simp add: mapM_x_Nil return_def simpler_modify_def) -next - case (Cons ptr ptrs s) - have "?rhs (ptr # ptrs) s - = (do modify (ekheap_update (foldr (\p ekh. ekh(p \ F (the (ekh p)))) ptrs)); - modify (ekheap_update (\ekh. ekh(ptr \ F (the (ekh ptr))))) - od) s" - by (simp only: foldr_Cons modify_ekheap_update_comp_futz) simp - also have "... = (do ?lhs ptrs; - modify (ekheap_update (\ekh. ekh(ptr \ F (the (ekh ptr))))) - od) s" - apply (rule monad_eq_split_tail) - apply simp - apply (rule Cons.hyps[symmetric]) - using Cons.prems - apply force - done - also have "... = ?lhs (ptr # ptrs) s" - apply (simp add: mapM_x_append mapM_x_singleton) - apply (rule monad_eq_split2[OF refl, where - P="\s. \ptr\set (ptr # ptrs). ekheap s ptr \ None" - and Q="\_ s. ekheap s ptr \ None"]) - apply (simp add: ethread_set_def - assert_opt_def get_etcb_def gets_the_def gets_def get_def modify_def put_def set_eobject_def - bind_def fail_def return_def split_def - split: option.splits) - apply ((wp mapM_x_wp[OF _ subset_refl] | simp add: ethread_set_def set_eobject_def)+)[1] - using Cons.prems - apply force - done - finally show ?case by (rule sym) -qed - -lemma awkward_fold_futz: - "fold (\p ekh. ekh(p \ the (ekh p)\tcb_domain := cur_domain s\)) ptrs ekh - = (\x. if x \ set ptrs then Some ((the (ekh x))\tcb_domain := cur_domain s\) else ekh x)" -by (induct ptrs arbitrary: ekh) (simp_all add: fun_eq_iff) - -lemma retype_region2_ext_retype_region_ext_futz: - "retype_region2_ext ptrs type >>= (\_. retype_region2_extra_ext ptrs type) - = retype_region_ext ptrs type" -proof(cases type) - case TCBObject - have complete_futz: - "\F x. modify (ekheap_update (\_. F (cur_domain x) (ekheap x))) x = modify (ekheap_update (\ekh. F (cur_domain x) ekh)) x" - by (simp add: modify_def get_def get_etcb_def put_def bind_def return_def) - have second_futz: - "\f G. - do modify (ekheap_update f); - cdom \ gets (\s. cur_domain s); - G cdom - od = - do cdom \ gets (\s. cur_domain s); - modify (ekheap_update f); - G cdom - od" - by (simp add: bind_def gets_def get_def return_def simpler_modify_def) - from TCBObject show ?thesis - apply (clarsimp simp: retype_region_ext_def retype_region2_ext_def retype_region2_extra_ext_def when_def bind_assoc) - apply (clarsimp simp: exec_gets fun_eq_iff) - apply (subst complete_futz) - apply (simp add: second_futz[simplified] exec_gets) - apply (simp add: default_ext_def exec_modify) - apply (subst mapM_x_modify_futz[where ptrs="rev ptrs", simplified]) - apply (simp add: foldr_upd_app_if_eta_futz) - apply (simp add: modify_def exec_get put_def o_def) - apply (simp add: foldr_upd_app_if_eta_futz foldr_conv_fold awkward_fold_futz) - apply (simp cong: if_cong) - done -qed (auto simp: fun_eq_iff retype_region_ext_def retype_region2_ext_def retype_region2_extra_ext_def - put_def gets_def get_def bind_def return_def mk_ef_def modify_def foldr_upd_app_if' when_def default_ext_def) - -lemma retype_region2_ext_retype_region: - "(retype_region ptr numObjects o_bits type dev :: (obj_ref list, det_ext) s_monad) - = (do ptrs \ retype_region2 ptr numObjects o_bits type dev; - retype_region2_extra_ext ptrs type; - return ptrs - od)" -apply (clarsimp simp: retype_region_def retype_region2_def when_def bind_assoc) - apply safe - defer - apply (simp add: retype_region2_extra_ext_def) -apply (subst retype_region_ext_modify_kheap_futz'[simplified bind_assoc]) -apply (subst retype_region2_ext_retype_region_ext_futz[symmetric]) -apply (simp add: bind_assoc) -done - lemma getObject_tcb_gets: "getObject addr >>= (\x::tcb. gets proj >>= (\y. G x y)) = gets proj >>= (\y. getObject addr >>= (\x. G x y))" @@ -1886,37 +1608,26 @@ next done qed -(* - -The existing proof continues below. - -*) - -lemma modify_ekheap_update_ekheap: - "modify (\s. ekheap_update f s) = do s \ gets ekheap; modify (\s'. s'\ekheap := f s\) od" -by (simp add: modify_def gets_def get_def put_def bind_def return_def split_def fun_eq_iff) - lemma corres_retype': assumes not_zero: "n \ 0" and aligned: "is_aligned ptr (objBitsKO ko + gbits)" - and obj_bits_api: "obj_bits_api (APIType_map2 ty) us = - objBitsKO ko + gbits" - and check: "(sz < obj_bits_api (APIType_map2 ty) us) - = (sz < objBitsKO ko + gbits)" + and obj_bits_api: "obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits" + and check: "(sz < obj_bits_api (APIType_map2 ty) us) = (sz < objBitsKO ko + gbits)" and usv: "APIType_map2 ty = Structures_A.CapTableObject \ 0 < us" - and ko: "makeObjectKO dev ty = Some ko" + and ko: "makeObjectKO dev d ty = Some ko" and orr: "obj_bits_api (APIType_map2 ty) us \ sz \ - obj_relation_retype - (default_object (APIType_map2 ty) dev us) ko" + obj_relation_retype (default_object (APIType_map2 ty) dev us d) ko" and cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" shows "corres (\rv rv'. rv' = g rv) - (\s. valid_pspace s \ pspace_no_overlap_range_cover ptr sz s - \ valid_mdb s \ valid_etcbs s \ valid_list s) - (\s. pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' ptr sz s) - (retype_region2 ptr n us (APIType_map2 ty) dev) - (do addrs \ createObjects ptr n ko gbits; - _ \ modify (update_gs (APIType_map2 ty) us (set addrs)); - return (g addrs) od)" + (\s. valid_pspace s \ pspace_no_overlap_range_cover ptr sz s + \ valid_mdb s \ valid_list s) + (\s. pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' ptr sz s + \ (ty = Inr (APIObjectType TCBObject) \ d = ksCurDomain s)) + (retype_region ptr n us (APIType_map2 ty) dev) + (do addrs \ createObjects ptr n ko gbits; + _ \ modify (update_gs (APIType_map2 ty) us (set addrs)); + return (g addrs) + od)" (is "corres ?r ?P ?P' ?C ?A") proof - note data_map_insert_def[simp del] @@ -1994,7 +1705,7 @@ proof - have al': "is_aligned ptr (obj_bits_api (APIType_map2 ty) us)" by (simp add: obj_bits_api ko) show ?thesis - apply (simp add: when_def retype_region2_def createObjects'_def + apply (simp add: when_def retype_region_def createObjects'_def createObjects_def aligned obj_bits_api[symmetric] ko[symmetric] al' shiftl_t2n data_map_insert_def[symmetric] is_aligned_mask[symmetric] split_def unless_def @@ -2002,79 +1713,90 @@ proof - split del: if_split) apply (subst retype_addrs_fold)+ apply (subst if_P) - using ko - apply (clarsimp simp: makeObjectKO_def) - apply (simp add: bind_assoc retype_region2_ext_def) - apply (rule corres_guard_imp) - apply (subst modify_ekheap_update_ekheap) - apply (simp only: bind_assoc) - apply (rule kheap_ekheap_double_gets) - apply (rule corres_symb_exec_r) - apply (simp add: not_less modify_modify bind_assoc[symmetric] - obj_bits_api[symmetric] shiftl_t2n upto_enum_red' + using ko + apply (clarsimp simp: makeObjectKO_def) + apply (simp add: bind_assoc) + apply (rule corres_guard_imp) + apply (rule_tac r'=pspace_relation in corres_underlying_split) + apply (clarsimp dest!: state_relation_pspace_relation) + apply (simp add: gets_def) + apply (rule corres_symb_exec_l[rotated]) + apply (rule exs_valid_get) + apply (rule get_sp) + apply (simp add: get_def no_fail_def) + apply (rule corres_symb_exec_r) + apply (simp add: not_less modify_modify bind_assoc[symmetric] + obj_bits_api[symmetric] shiftl_t2n upto_enum_red' range_cover.unat_of_nat_n[OF cover]) - apply (rule corres_split_nor[OF _ corres_trivial]) - apply (rename_tac x eps ps) - apply (rule_tac P="\s. x = kheap s \ eps = ekheap (s) \ ?P s" and - P'="\s. ps = ksPSpace s \ ?P' s" in corres_modify) - apply (simp add: set_retype_addrs_fold new_caps_adds_fold) - apply (erule retype_state_relation[OF _ _ _ _ _ _ _ _ _ cover _ _ orr], - simp_all add: ko not_zero obj_bits_api - bound[simplified obj_bits_api ko])[1] - apply (clarsimp simp: retype_addrs_fold[symmetric] ptr_add_def upto_enum_red' not_zero' - range_cover.unat_of_nat_n[OF cover] word_le_sub1) - apply (rule_tac f=g in arg_cong) - apply clarsimp - apply wp+ - apply (clarsimp split: option.splits) - apply (intro conjI impI) - apply (clarsimp|wp)+ - apply (clarsimp split: option.splits) - apply wpsimp - apply (clarsimp split: option.splits) - apply (intro conjI impI) - apply wp - apply (clarsimp simp:lookupAround2_char1) - apply wp - apply (clarsimp simp: obj_bits_api ko) - apply (drule(1) pspace_no_overlap_disjoint') - apply (rule_tac x1 = a in ccontr[OF in_empty_interE]) - apply simp - apply (clarsimp simp: not_less shiftL_nat) - apply (erule order_trans) - apply (subst p_assoc_help) - apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz"]) - apply (subst add.commute) - apply (subst add.assoc) - apply (rule word_plus_mono_right) - using cover - apply - - apply (rule iffD2[OF word_le_nat_alt]) - apply (subst word_of_nat_minus) - using not_zero - apply simp - apply (rule le_trans[OF unat_plus_gt]) - apply simp - apply (subst unat_minus_one) - apply (subst mult.commute) - apply (rule word_power_nonzero_64) - apply (rule of_nat_less_pow_64[OF n_estimate]) - apply (simp add:word_bits_def objBitsKO_gt_0 ko) - apply (simp add:range_cover_def obj_bits_api ko word_bits_def) - apply (cut_tac not_zero',clarsimp simp:ko) - apply(clarsimp simp:field_simps ko) - apply (subst unat_sub[OF word_1_le_power]) - apply (simp add:range_cover_def) - apply (subst diff_add_assoc[symmetric]) - apply (cut_tac unat_of_nat_n',simp add:ko) - apply (clarsimp simp: obj_bits_api ko) - apply (rule diff_le_mono) - apply (frule range_cover.range_cover_compare_bound) - apply (cut_tac obj_bits_api unat_of_nat_shift') - apply (clarsimp simp:add.commute range_cover_def ko) - apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask,OF le_refl ]) - apply (simp add:range_cover_def domI)+ - done + apply (rule corres_guard_imp) + apply (rule corres_split_nor[OF _ corres_trivial]) + apply (rename_tac ps ps' sa) + apply (rule_tac P="\s. ps = kheap s \ sa = s \ ?P s" and + P'="\s. ps' = ksPSpace s \ ?P' s" in corres_modify) + apply(frule curdomain_relation[THEN sym]) + apply (simp add: set_retype_addrs_fold new_caps_adds_fold) + apply (drule retype_state_relation[OF _ _ _ _ _ _ _ _ cover _ _ orr], + simp_all add: ko not_zero obj_bits_api + bound[simplified obj_bits_api ko])[1] + apply (cases ty; simp; rename_tac tp; case_tac tp; + clarsimp simp: default_object_def APIType_map2_def + split: arch_kernel_object.splits apiobject_type.splits) + apply (clarsimp simp: retype_addrs_fold[symmetric] ptr_add_def upto_enum_red' not_zero' + range_cover.unat_of_nat_n[OF cover] word_le_sub1) + apply (rule_tac f=g in arg_cong) + apply clarsimp + apply wpsimp+ + apply simp+ + apply (clarsimp split: option.splits) + apply (intro conjI impI) + apply (clarsimp|wp)+ + apply (clarsimp split: option.splits) + apply wpsimp + apply (clarsimp split: option.splits) + apply (intro conjI impI) + apply wp + apply (clarsimp simp:lookupAround2_char1) + apply wp + apply (clarsimp simp: obj_bits_api ko) + apply (drule(1) pspace_no_overlap_disjoint') + apply (rule_tac x1 = a in ccontr[OF in_empty_interE]) + apply simp + apply (clarsimp simp: not_less shiftL_nat) + apply (erule order_trans) + apply (subst p_assoc_help) + apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz"]) + apply (subst add.commute) + apply (subst add.assoc) + apply (rule word_plus_mono_right) + using cover + apply - + apply (rule iffD2[OF word_le_nat_alt]) + apply (subst word_of_nat_minus) + using not_zero + apply simp + apply (rule le_trans[OF unat_plus_gt]) + apply simp + apply (subst unat_minus_one) + apply (subst mult.commute) + apply (rule word_power_nonzero_64) + apply (rule of_nat_less_pow_64[OF n_estimate]) + apply (simp add:word_bits_def objBitsKO_gt_0 ko) + apply (simp add:range_cover_def obj_bits_api ko word_bits_def) + apply (cut_tac not_zero',clarsimp simp:ko) + apply(clarsimp simp:field_simps ko) + apply (subst unat_sub[OF word_1_le_power]) + apply (simp add:range_cover_def) + apply (subst diff_add_assoc[symmetric]) + apply (cut_tac unat_of_nat_n',simp add:ko) + apply (clarsimp simp: obj_bits_api ko) + apply (rule diff_le_mono) + apply (frule range_cover.range_cover_compare_bound) + apply (cut_tac obj_bits_api unat_of_nat_shift') + apply (clarsimp simp:add.commute range_cover_def ko) + apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask,OF le_refl ]) + apply (simp add:range_cover_def domI)+ + apply wpsimp+ + done qed lemma createObjects_corres': @@ -2566,15 +2288,16 @@ proof - fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def curDomain_def split: AARCH64_H.object_type.splits) apply (wp mapM_x_wp' hoare_vcg_const_Ball_lift)+ - apply (rule hoare_post_imp) - prefer 2 - apply (rule createObjects_obj_at [where 'a = "tcb",OF _ not_0]) - using cover - apply (clarsimp simp: AARCH64_H.toAPIType_def APIType_capBits_def objBits_simps - split: AARCH64_H.object_type.splits) - apply simp - apply (clarsimp simp: valid_cap'_def objBits_simps) - apply (fastforce intro: capAligned_tcbI) + apply (rule hoare_post_imp) + prefer 2 + apply (rule createObjects_obj_at [where 'a = "tcb",OF _ not_0]) + using cover + apply (clarsimp simp: AARCH64_H.toAPIType_def APIType_capBits_def objBits_simps + split: AARCH64_H.object_type.splits) + apply simp+ + apply (clarsimp simp: valid_cap'_def objBits_simps) + apply (fastforce intro: capAligned_tcbI) + apply wp done next case EndpointObject with Some cover ct show ?thesis @@ -2655,7 +2378,7 @@ lemma other_objs_default_relation: "\ case ty of Structures_A.EndpointObject \ ko = injectKO (makeObject :: endpoint) | Structures_A.NotificationObject \ ko = injectKO (makeObject :: Structures_H.notification) | _ \ False \ \ - obj_relation_retype (default_object ty dev n) ko" + obj_relation_retype (default_object ty dev n d) ko" apply (rule obj_relation_retype_other_obj) apply (clarsimp simp: default_object_def is_other_obj_relation_type_def @@ -2675,7 +2398,8 @@ lemma other_objs_default_relation: done lemma tcb_relation_retype: - "obj_relation_retype (default_object Structures_A.TCBObject dev n) (KOTCB makeObject)" + "obj_relation_retype (default_object Structures_A.TCBObject dev n d) + (KOTCB (tcbDomain_update (\_. d) makeObject))" by (clarsimp simp: tcb_relation_cut_def default_object_def obj_relation_retype_def tcb_relation_def default_tcb_def makeObject_tcb makeObject_cte new_context_def newContext_def newFPUState_def @@ -2684,7 +2408,7 @@ lemma tcb_relation_retype: lemma captable_relation_retype: "n < word_bits \ - obj_relation_retype (default_object Structures_A.CapTableObject dev n) (KOCTE makeObject)" + obj_relation_retype (default_object Structures_A.CapTableObject dev n d) (KOCTE makeObject)" apply (clarsimp simp: obj_relation_retype_def default_object_def wf_empty_bits objBits_simps' dom_empty_cnode ex_with_length cte_level_bits_def) @@ -2702,7 +2426,7 @@ lemma captable_relation_retype: done lemma pagetable_relation_retype: - "obj_relation_retype (default_object (ArchObject PageTableObj) dev n) + "obj_relation_retype (default_object (ArchObject PageTableObj) dev n d) (KOArch (KOPTE makeObject))" apply (simp add: default_object_def default_arch_object_def makeObject_pte obj_relation_retype_def @@ -2712,7 +2436,7 @@ lemma pagetable_relation_retype: done lemma vsroot_relation_retype: - "obj_relation_retype (default_object (ArchObject VSpaceObj) dev n) + "obj_relation_retype (default_object (ArchObject VSpaceObj) dev n d) (KOArch (KOPTE makeObject))" apply (simp add: default_object_def default_arch_object_def makeObject_pte obj_relation_retype_def @@ -2725,20 +2449,21 @@ lemmas makeObjectKO_simps = makeObjectKO_def[split_simps AARCH64_H.object_type.s apiobject_type.split sum.split kernel_object.split ] lemma corres_retype: - assumes not_zero: "n \ 0" + assumes not_zero: "n \ 0" and aligned: "is_aligned ptr (objBitsKO ko + gbits)" and obj_bits_api: "obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits" and tp: "APIType_map2 ty \ no_gs_types" - and ko: "makeObjectKO dev ty = Some ko" + and ko: "makeObjectKO dev d ty = Some ko" and orr: "obj_bits_api (APIType_map2 ty) us \ sz \ - obj_relation_retype (default_object (APIType_map2 ty) dev us) ko" + obj_relation_retype (default_object (APIType_map2 ty) dev us d) ko" and cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" shows "corres (=) (\s. valid_pspace s \ pspace_no_overlap_range_cover ptr sz s - \ valid_mdb s \ valid_etcbs s \ valid_list s) + \ valid_mdb s \ valid_list s) (\s. pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' ptr sz s - \ (\val. ko = injectKO val)) - (retype_region2 ptr n us (APIType_map2 ty) dev) (createObjects ptr n ko gbits)" + \ (\val. ko = injectKO val) + \ (ty = Inr (APIObjectType TCBObject) \ d = ksCurDomain s)) + (retype_region ptr n us (APIType_map2 ty) dev) (createObjects ptr n ko gbits)" apply (rule corres_guard_imp) apply (rule_tac F = "(\val. ko = injectKO val)" in corres_gen_asm2) apply (erule exE) @@ -3227,7 +2952,8 @@ proof - qed lemma createObjects_valid_pspace': - assumes mko: "makeObjectKO dev ty = Some val" + assumes mko: "makeObjectKO dev d ty = Some val" + and max_d: "ty = Inr (APIObjectType TCBObject) \ d \ maxDomain" and not_0: "n \ 0" and cover: "range_cover ptr sz (objBitsKO val + gbits) n" and sz_limit: "sz \ maxUntypedSizeBits" @@ -3331,7 +3057,7 @@ proof (intro conjI impI) elim!: ranE split: if_split_asm) apply (insert sym[OF mko])[1] - apply (clarsimp simp: makeObjectKO_def + apply (clarsimp simp: makeObjectKO_def max_d split: bool.split_asm sum.split_asm AARCH64_H.object_type.split_asm apiobject_type.split_asm @@ -3439,7 +3165,8 @@ abbreviation "injectKOS \ (injectKO :: ('a :: pspace_storable) \ kernel_object)" lemma createObjects_valid_pspace_untyped': - assumes mko: "makeObjectKO dev ty = Some val" + assumes mko: "makeObjectKO dev d ty = Some val" + and max_d: "ty = Inr (APIObjectType TCBObject) \ d \ maxDomain" and not_0: "n \ 0" and cover: "range_cover ptr sz (objBitsKO val + gbits) n" and sz_limit: "sz \ maxUntypedSizeBits" @@ -3447,7 +3174,7 @@ lemma createObjects_valid_pspace_untyped': shows "\\s. pspace_no_overlap' ptr sz s \ valid_pspace' s \ caps_no_overlap'' ptr sz s \ ptr \ 0 \ caps_overlap_reserved' {ptr .. ptr + of_nat (n * 2^gbits * 2 ^ objBitsKO val ) - 1} s \ createObjects' ptr n val gbits \\r. valid_pspace'\" - apply (wp createObjects_valid_pspace' [OF mko not_0 cover sz_limit ptr_cn]) + apply (wp createObjects_valid_pspace' [OF mko max_d not_0 cover sz_limit ptr_cn]) apply simp done @@ -3627,15 +3354,12 @@ lemma createNewCaps_cte_wp_at2: createNewCaps ty ptr n objsz dev \\rv s. P (cte_wp_at' P' p s)\" including classic_wp_pre - apply (simp add: createNewCaps_def createObjects_def AARCH64_H.toAPIType_def - split del: if_split) - apply (case_tac ty; simp add: createNewCaps_def createObjects_def Arch_createNewCaps_def - split del: if_split cong: if_cong) + unfolding createNewCaps_def Arch_createNewCaps_def createObjects_def AARCH64_H.toAPIType_def + apply (case_tac ty; simp split del: if_split cong: if_cong) apply (rename_tac apiobject_type) apply (case_tac apiobject_type; simp split del: if_split) - apply (wp, simp add:createObjects_def) - apply ((wp createObjects_orig_cte_wp_at2'[where sz = sz] - mapM_x_wp' threadSet_cte_wp_at2')+ + apply (rule hoare_pre, wp, simp add: createObjects_def) + apply ((wp createObjects_orig_cte_wp_at2'[where sz = sz] mapM_x_wp') | assumption | clarsimp simp: APIType_capBits_def projectKO_opts_defs makeObject_tcb tcb_cte_cases_def cteSizeBits_def @@ -4169,10 +3893,9 @@ lemma createNewCaps_ko_wp_atQ': \ pspace_no_overlap' ptr sz s) and K (\d (tcb_x :: tcb). \tcbQueued tcb_x \ tcbState tcb_x = Inactive \ P' (injectKO (tcb_x \ tcbDomain := d \)) = P' (injectKO tcb_x)) - and K (\v. makeObjectKO d (Inr ty) = Some v - \ P' v \ P True)\ - createNewCaps ty ptr n us d - \\rv s. P (ko_wp_at' P' p s)\" + and (\s. \v. makeObjectKO dev (ksCurDomain s) (Inr ty) = Some v \ P' v \ P True)\ + createNewCaps ty ptr n us dev + \\_ s. P (ko_wp_at' P' p s)\" apply (rule hoare_name_pre_state) apply (clarsimp simp: createNewCaps_def AARCH64_H.toAPIType_def split del: if_split) @@ -4309,14 +4032,14 @@ lemma createNewCaps_idle'[wp]: leads to a failed proof state. If this could be fixed then the inclusion of classic_wp_pre could also be removed. *) including classic_wp_pre - apply (wp mapM_x_wp' createObjects_idle' threadSet_idle' + apply (wp mapM_x_wp' createObjects_idle' + | clarsimp simp: curDomain_def | simp add: projectKO_opt_tcb projectKO_opt_cte mult_2 makeObject_cte makeObject_tcb archObjSize_def tcb_cte_cases_def objBitsKO_def APIType_capBits_def objBits_def createObjects_def cteSizeBits_def | simp add: field_simps - | intro conjI impI - | clarsimp simp: curDomain_def)+ + | intro conjI impI)+ done crunch createNewCaps @@ -4558,9 +4281,12 @@ lemma createNewCaps_valid_pspace: and cover: "range_cover ptr sz (APIType_capBits ty us) n" and sz_limit: "sz \ maxUntypedSizeBits" and ptr_cn: "canonical_address (ptr && ~~ mask sz)" - shows "\\s. pspace_no_overlap' ptr sz s \ valid_pspace' s - \ caps_no_overlap'' ptr sz s \ ptr \ 0 \ caps_overlap_reserved' {ptr..ptr + of_nat n * 2^(APIType_capBits ty us) - 1} s \ ksCurDomain s \ maxDomain\ - createNewCaps ty ptr n us dev \\r. valid_pspace'\" + shows + "\\s. pspace_no_overlap' ptr sz s \ valid_pspace' s + \ caps_no_overlap'' ptr sz s \ ptr \ 0 \ caps_overlap_reserved' {ptr..ptr + of_nat n * 2^(APIType_capBits ty us) - 1} s + \ ksCurDomain s \ maxDomain\ + createNewCaps ty ptr n us dev + \\r. valid_pspace'\" unfolding createNewCaps_def Arch_createNewCaps_def using valid_obj_makeObject_rules sz_limit ptr_cn apply (clarsimp simp: AARCH64_H.toAPIType_def @@ -4570,14 +4296,18 @@ lemma createNewCaps_valid_pspace: apply (case_tac apiobject_type, simp_all split del: if_split) apply (rule hoare_pre, wp, clarsimp) apply (insert cover) - apply (wp createObjects_valid_pspace_untyped' [OF _ not_0 , where ty="Inr ty" and sz = sz] - mapM_x_threadSet_valid_pspace mapM_x_wp' - | simp add: makeObjectKO_def APIType_capBits_def - objBits_simps not_0 createObjects_def curDomain_def - | intro conjI impI - | simp add: power_add field_simps mult_2_right - | simp add: bit_simps)+ - done + (* for TCBObject, we need to know a bit more about tcbDomain *) + apply (simp add: curDomain_def) + apply (rule bind_wp[OF _ gets_sp]) + apply (clarsimp simp: createObjects_def) + apply (rule hoare_assume_pre) + by (wp createObjects_valid_pspace_untyped' [OF _ _ not_0 , where ty="Inr ty" and sz = sz] + mapM_x_threadSet_valid_pspace mapM_x_wp' + | simp add: makeObjectKO_def APIType_capBits_def + objBits_simps not_0 createObjects_def curDomain_def + | intro conjI impI + | simp add: power_add field_simps mult_2_right + | simp add: bit_simps)+ lemma doMachineOp_return_foo: "doMachineOp (do x\a;return () od) = (do (doMachineOp a); return () od)" @@ -4765,7 +4495,7 @@ crunch createNewCaps (wp: mapM_x_wp' simp: crunch_simps) lemma createObjects_null_filter': - "\\s. P (null_filter' (ctes_of s)) \ makeObjectKO dev ty = Some val \ + "\\s. P (null_filter' (ctes_of s)) \ makeObjectKO dev d ty = Some val \ range_cover ptr sz (objBitsKO val + gbits) n \ n \ 0 \ pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' ptr sz s\ createObjects' ptr n val gbits @@ -5174,7 +4904,7 @@ lemma untyped_zero_ranges_cte_def: done lemma createObjects_untyped_ranges_zero': - assumes moKO: "makeObjectKO dev ty = Some val" + assumes moKO: "makeObjectKO dev d ty = Some val" shows "\ct_active' and valid_pspace' and pspace_no_overlap' ptr sz and untyped_ranges_zero' @@ -5200,9 +4930,10 @@ lemma createObjects_untyped_ranges_zero': done lemma createObjects_no_cte_invs: - assumes moKO: "makeObjectKO dev ty = Some val" + assumes moKO: "makeObjectKO dev d ty = Some val" assumes no_cte: "\c. projectKO_opt val \ Some (c::cte)" assumes no_tcb: "\t. projectKO_opt val \ Some (t::tcb)" + and mdom: "ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \ d \ maxDomain" shows "\\s. range_cover ptr sz ((objBitsKO val) + gbits) n \ n \ 0 \ sz \ maxUntypedSizeBits \ canonical_address (ptr && ~~ mask sz) @@ -5287,23 +5018,21 @@ qed lemma corres_retype_update_gsI: assumes not_zero: "n \ 0" and aligned: "is_aligned ptr (objBitsKO ko + gbits)" - and obj_bits_api: "obj_bits_api (APIType_map2 ty) us = - objBitsKO ko + gbits" - and check: "sz < obj_bits_api (APIType_map2 ty) us \ - sz < objBitsKO ko + gbits" + and obj_bits_api: "obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits" + and check: "sz < obj_bits_api (APIType_map2 ty) us \ sz < objBitsKO ko + gbits" and usv: "APIType_map2 ty = Structures_A.CapTableObject \ 0 < us" - and ko: "makeObjectKO dev ty = Some ko" + and ko: "makeObjectKO dev d ty = Some ko" and orr: "obj_bits_api (APIType_map2 ty) us \ sz \ - obj_relation_retype - (default_object (APIType_map2 ty) dev us) ko" + obj_relation_retype (default_object (APIType_map2 ty) dev us d) ko" and cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n" and f: "f = update_gs (APIType_map2 ty) us" shows "corres (\rv rv'. rv' = g rv) (\s. valid_pspace s \ pspace_no_overlap_range_cover ptr sz s - \ valid_mdb s \ valid_etcbs s \ valid_list s) + \ valid_mdb s \ valid_list s) (\s. pspace_aligned' s \ pspace_distinct' s \ - pspace_no_overlap' ptr sz s) - (retype_region2 ptr n us (APIType_map2 ty) dev) + pspace_no_overlap' ptr sz s \ + (ty = Inr (APIObjectType TCBObject) \ d = ksCurDomain s)) + (retype_region ptr n us (APIType_map2 ty) dev) (do addrs \ createObjects ptr n ko gbits; _ \ modify (f (set addrs)); return (g addrs) @@ -5314,69 +5043,11 @@ lemma corres_retype_update_gsI: lemma gcd_corres: "corres (=) \ \ (gets cur_domain) curDomain" by (simp add: curDomain_def state_relation_def) -lemma retype_region2_extra_ext_mapM_x_corres: - shows "corres dc - (valid_etcbs and (\s. \addr\set addrs. tcb_at addr s)) - (\s. \addr\set addrs. obj_at' (Not \ tcbQueued) addr s) - (retype_region2_extra_ext addrs Structures_A.apiobject_type.TCBObject) - (mapM_x (\addr. do cdom \ curDomain; - threadSet (tcbDomain_update (\_. cdom)) addr - od) - addrs)" - apply (rule corres_guard_imp) - apply (simp add: retype_region2_extra_ext_def curDomain_mapM_x_futz[symmetric] when_def) - apply (rule corres_split_eqr[OF gcd_corres]) - apply (rule_tac S="Id \ {(x, y). x \ set addrs}" - and P="\s. (\t \ set addrs. tcb_at t s) \ valid_etcbs s" - and P'="\s. \t \ set addrs. obj_at' (Not \ tcbQueued) t s" - in corres_mapM_x) - apply simp - apply (rule corres_guard_imp) - apply (rule ethread_set_corres, simp_all add: etcb_relation_def non_exst_same_def)[1] - apply (case_tac tcb') - apply simp - apply fastforce - apply (fastforce simp: obj_at'_def) - apply (wp hoare_vcg_ball_lift | simp)+ - apply (clarsimp simp: obj_at'_def) - apply fastforce - apply auto[1] - apply (wp | simp add: curDomain_def)+ - done - -lemma retype_region2_extra_ext_trivial: - "ty \ APIType_map2 (Inr (APIObjectType apiobject_type.TCBObject)) - \ retype_region2_extra_ext ptrs ty = return ()" -by (simp add: retype_region2_extra_ext_def when_def APIType_map2_def) - -lemma retype_region2_retype_region_PageTableObject: - "retype_region ptr n us (APIType_map2 (Inr PageTableObject)) dev = - (retype_region2 ptr n us (APIType_map2 (Inr PageTableObject)) dev :: obj_ref list det_ext_monad)" - by (simp add: retype_region2_ext_retype_region retype_region2_extra_ext_def when_def - APIType_map2_def) - -lemma retype_region2_valid_etcbs[wp]:"\valid_etcbs\ retype_region2 a b c d dev \\_. valid_etcbs\" - apply (simp add: retype_region2_def) - apply (simp add: retype_region2_ext_def bind_assoc) - apply wp - apply (clarsimp simp del: fun_upd_apply) - apply (blast intro: valid_etcb_fold_update) - done - -lemma retype_region2_obj_at: - assumes tytcb: "ty = Structures_A.apiobject_type.TCBObject" - shows "\\\ retype_region2 ptr n us ty dev \\rv s. \x \ set rv. tcb_at x s\" - using tytcb unfolding retype_region2_def - apply (simp only: return_bind bind_return foldr_upd_app_if fun_app_def K_bind_def) - apply (wp dxo_wp_weak | simp)+ - apply (auto simp: obj_at_def default_object_def is_tcb_def) - done - -lemma createObjects_Not_tcbQueued: +lemma createObjects_tcb_at': "\range_cover ptr sz (objBitsKO (injectKOS (makeObject::tcb))) n; n \ 0\ \ \\s. pspace_no_overlap' ptr sz s \ pspace_aligned' s \ pspace_distinct' s\ createObjects ptr n (KOTCB makeObject) 0 - \\ptrs s. \addr\set ptrs. obj_at' (Not \ tcbQueued) addr s\" + \\ptrs s. \addr\set ptrs. tcb_at' addr s\" apply (rule hoare_strengthen_post[OF createObjects_ko_at_strg[where val = "(makeObject :: tcb)"]]) apply (auto simp: obj_at'_def project_inject objBitsKO_def objBits_def makeObject_tcb) done @@ -5431,7 +5102,7 @@ lemma regroup_createObjects_dmo_gsPTTypes: lemma corres_retype_region_createNewCaps: "corres ((\r r'. length r = length r' \ list_all2 cap_relation r r') \ map (\ref. default_cap (APIType_map2 (Inr ty)) ref us dev)) - (\s. valid_pspace s \ valid_mdb s \ valid_etcbs s \ valid_list s \ valid_arch_state s + (\s. valid_pspace s \ valid_mdb s \ valid_list s \ valid_arch_state s \ caps_no_overlap y sz s \ pspace_no_overlap_range_cover y sz s \ caps_overlap_reserved {y..y + of_nat n * 2 ^ (obj_bits_api (APIType_map2 (Inr ty)) us) - 1} s \ (\slot. cte_wp_at (\c. up_aligned_area y sz \ cap_range c \ cap_is_device c = dev) slot s) @@ -5466,78 +5137,60 @@ lemma corres_retype_region_createNewCaps: apply simp apply (clarsimp simp: range_cover_def) apply (arith+)[4] - \ \TCB, EP, NTFN\ - apply (simp_all add: retype_region2_ext_retype_region - bind_cong[OF curDomain_mapM_x_futz refl, unfolded bind_assoc] - split del: if_split)[8] + \ \TCB\ + apply (simp_all add: curDomain_def split del: if_split) + apply (rule corres_underlying_gets_pre_rhs[rotated]) + apply (rule gets_sp) apply (rule corres_guard_imp) + apply (rule corres_bind_return) apply (rule corres_split_eqr) apply (rule corres_retype[where 'a = tcb], simp_all add: obj_bits_api_def objBits_simps' pageBits_def - APIType_map2_def makeObjectKO_def - tcb_relation_retype)[1] - apply (fastforce simp: range_cover_def) - apply (simp add: tcb_relation_retype) - apply (rule corres_split_nor) - apply (simp add: APIType_map2_def) - apply (rule retype_region2_extra_ext_mapM_x_corres) - apply (rule corres_trivial, simp) - apply (clarsimp simp: list_all2_same list_all2_map1 list_all2_map2 - objBits_simps APIType_map2_def) - apply wp - apply wp - apply ((wp retype_region2_obj_at | simp add: APIType_map2_def)+)[1] - apply ((wp createObjects_Not_tcbQueued[where sz=sz] - | simp add: APIType_map2_def objBits_simps' obj_bits_api_def)+)[1] - apply simp - apply simp - apply (subst retype_region2_extra_ext_trivial) - apply (simp add: APIType_map2_def) - apply (simp add: liftM_def[symmetric] split del: if_split) - apply (rule corres_rel_imp) - apply (rule corres_guard_imp) - apply (rule corres_retype[where 'a = endpoint], - simp_all add: obj_bits_api_def objBits_simps' pageBits_def APIType_map2_def - makeObjectKO_def other_objs_default_relation)[1] - apply (fastforce simp: range_cover_def) + APIType_map2_def makeObjectKO_def)[1] + apply (fastforce simp: range_cover_def) + apply (simp add: tcb_relation_retype) + apply (rule corres_returnTT, simp) + apply (clarsimp simp: list_all2_same list_all2_map1 list_all2_map2 + objBits_simps APIType_map2_def) + apply ((wp | simp add: APIType_map2_def)+)[1] + apply ((wp createObjects_tcb_at'[where sz=sz] | simp add: APIType_map2_def objBits_simps' obj_bits_api_def)+)[1] apply simp apply simp - apply (clarsimp simp: list_all2_same list_all2_map1 list_all2_map2 objBits_simps - APIType_map2_def) - apply (subst retype_region2_extra_ext_trivial) - apply (simp add: APIType_map2_def) + \ \EP, NTFN\ apply (simp add: liftM_def[symmetric] split del: if_split) apply (rule corres_rel_imp) apply (rule corres_guard_imp) - apply (rule corres_retype[where 'a = notification], - simp_all add: obj_bits_api_def objBits_simps' pageBits_def APIType_map2_def - makeObjectKO_def other_objs_default_relation)[1] - apply (fastforce simp: range_cover_def) - apply simp - apply simp - apply (clarsimp simp: list_all2_same list_all2_map1 list_all2_map2 objBits_simps - APIType_map2_def) - \ \CapTable\ - apply (subst retype_region2_extra_ext_trivial) - apply (simp add: APIType_map2_def) - apply (subst bind_assoc_return_reverse[of "createObjects y n (KOCTE makeObject) us"]) - apply (subst liftM_def[of "map (\addr. capability.CNodeCap addr us 0 0)", symmetric]) - apply simp + apply (rule corres_retype[where 'a = endpoint], + simp_all add: obj_bits_api_def objBits_simps' pageBits_def + APIType_map2_def makeObjectKO_def + other_objs_default_relation)[1] + apply ((simp add: range_cover_def APIType_map2_def + list_all2_same list_all2_map1 list_all2_map2)+)[4] + apply (simp add: liftM_def[symmetric] split del: if_split) apply (rule corres_rel_imp) apply (rule corres_guard_imp) - apply (rule corres_retype_update_gsI, - simp_all add: obj_bits_api_def objBits_simps' pageBits_def APIType_map2_def - makeObjectKO_def slot_bits_def field_simps ext)[1] - apply (simp add: range_cover_def) - apply (rule captable_relation_retype,simp add: range_cover_def word_bits_def) + apply (rule corres_retype[where 'a = notification], + simp_all add: obj_bits_api_def objBits_simps' pageBits_def + APIType_map2_def makeObjectKO_def + other_objs_default_relation)[1] + apply ((simp add: range_cover_def APIType_map2_def + list_all2_same list_all2_map1 list_all2_map2)+)[4] + \ \CapTable\ + apply (find_goal \match premises in "_ = ArchTypes_H.apiobject_type.CapTableObject" \ \-\\) + apply (subst bind_assoc_return_reverse[of "createObjects y n (KOCTE makeObject) us"]) + apply (subst liftM_def [of "map (\addr. capability.CNodeCap addr us 0 0)", symmetric]) apply simp - apply simp - apply (clarsimp simp: list_all2_same list_all2_map1 list_all2_map2 objBits_simps - allRights_def APIType_map2_def - split del: if_split) + apply (rule corres_rel_imp) + apply (rule corres_guard_imp) + apply (rule corres_retype_update_gsI, + simp_all add: obj_bits_api_def objBits_simps' pageBits_def + APIType_map2_def makeObjectKO_def slot_bits_def + field_simps ext)[1] + apply ((clarsimp simp : range_cover_def APIType_map2_def word_bits_def + list_all2_same list_all2_map1 list_all2_map2 + | rule captable_relation_retype)+)[5] + \ \HugePageObject\ apply (in_case \HugePageObject\) - apply (subst retype_region2_extra_ext_trivial) - apply (simp add: APIType_map2_def) apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split) apply (simp add: init_arch_objects_def split del: if_split) apply (subst regroup_createObjects_dmo_userPages) @@ -5561,9 +5214,8 @@ lemma corres_retype_region_createNewCaps: apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def list_all2_map1 list_all2_map2 list_all2_same) apply ((wpsimp split_del: if_split)+)[6] + \ \VSpaceObject\ apply (in_case \VSpaceObject\) - apply (subst retype_region2_extra_ext_trivial) - apply (simp add: APIType_map2_def) apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split) apply (simp add: init_arch_objects_def split del: if_split) apply (subst regroup_createObjects_dmo_gsPTTypes) @@ -5584,9 +5236,8 @@ lemma corres_retype_region_createNewCaps: apply (rule corres_returnTT) apply (simp add: arch_default_cap_def list_all2_map1 list_all2_map2 list_all2_same) apply ((wpsimp split_del: if_split)+)[6] + \ \SmallPageObject\ apply (in_case \SmallPageObject\) - apply (subst retype_region2_extra_ext_trivial) - apply (simp add: APIType_map2_def) apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split) apply (simp add: init_arch_objects_def split del: if_split) apply (subst regroup_createObjects_dmo_userPages) @@ -5610,9 +5261,8 @@ lemma corres_retype_region_createNewCaps: apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def list_all2_map1 list_all2_map2 list_all2_same) apply ((wpsimp split_del: if_split)+)[6] + \ \LargePageObject\ apply (in_case \LargePageObject\) - apply (subst retype_region2_extra_ext_trivial) - apply (simp add: APIType_map2_def) apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split) apply (simp add: init_arch_objects_def split del: if_split) apply (subst regroup_createObjects_dmo_userPages) @@ -5636,9 +5286,8 @@ lemma corres_retype_region_createNewCaps: apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def list_all2_map1 list_all2_map2 list_all2_same) apply ((wpsimp split_del: if_split)+)[6] + \ \PageTableObject\ apply (in_case \PageTableObject\) - apply (subst retype_region2_ext_retype_region) - apply (subst retype_region2_extra_ext_trivial, simp add: APIType_map2_def) apply (simp_all add: corres_liftM2_simp[unfolded liftM_def]) apply (simp add: init_arch_objects_def split del: if_split) apply (subst regroup_createObjects_dmo_gsPTTypes) @@ -5660,11 +5309,8 @@ lemma corres_retype_region_createNewCaps: apply (clarsimp simp: list_all2_map1 list_all2_map2 list_all2_same APIType_map2_def arch_default_cap_def) apply ((wpsimp split_del: if_split)+)[6] + \ \VCPUObject\ apply (in_case \VCPUObject\) - apply (subst retype_region2_ext_retype_region) - apply (subst retype_region2_extra_ext_trivial) - apply (simp add: APIType_map2_def) - apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split) apply (rule corres_rel_imp) apply (simp add: init_arch_objects_APIType_map2_VCPU_noop split del: if_split) apply (rule corres_guard_imp) diff --git a/proof/refine/AARCH64/Schedule_R.thy b/proof/refine/AARCH64/Schedule_R.thy index 091798dacf..39b341a24c 100644 --- a/proof/refine/AARCH64/Schedule_R.thy +++ b/proof/refine/AARCH64/Schedule_R.thy @@ -194,7 +194,7 @@ lemma schedule_choose_new_thread_sched_act_rct[wp]: lemma tcbSchedAppend_corres: "tcb_ptr = tcbPtr \ corres dc - (in_correct_ready_q and ready_qs_distinct and valid_etcbs and st_tcb_at runnable tcb_ptr + (in_correct_ready_q and ready_qs_distinct and st_tcb_at runnable tcb_ptr and pspace_aligned and pspace_distinct) (sym_heap_sched_pointers and valid_sched_pointers and valid_tcbs') (tcb_sched_action tcb_sched_append tcb_ptr) (tcbSchedAppend tcbPtr)" @@ -210,9 +210,9 @@ lemma tcbSchedAppend_corres: apply (fastforce dest: pspace_distinct_cross) apply (clarsimp simp: tcb_sched_action_def tcb_sched_append_def get_tcb_queue_def tcbSchedAppend_def getQueue_def unless_def when_def) - apply (rule corres_symb_exec_l[OF _ _ ethread_get_sp]; (solves wpsimp)?) + apply (rule corres_symb_exec_l[OF _ _ thread_get_sp]; (solves wpsimp)?) apply (rename_tac domain) - apply (rule corres_symb_exec_l[OF _ _ ethread_get_sp]; (solves wpsimp)?) + apply (rule corres_symb_exec_l[OF _ _ thread_get_sp]; (solves wpsimp)?) apply (rename_tac priority) apply (rule corres_symb_exec_l[OF _ _ gets_sp]; (solves wpsimp)?) apply (rule corres_stateAssert_ignore) @@ -224,12 +224,11 @@ lemma tcbSchedAppend_corres: apply (rule corres_symb_exec_r[OF _ threadGet_sp]; (solves wpsimp)?) apply (subst if_distrib[where f="set_tcb_queue domain prio" for domain prio]) apply (rule corres_if_strong') - apply (frule state_relation_ready_queues_relation) - apply (frule in_ready_q_tcbQueued_eq[where t=tcbPtr]) subgoal - by (fastforce dest: tcb_at_ekheap_dom pred_tcb_at_tcb_at - simp: obj_at'_def opt_pred_def opt_map_def obj_at_def is_tcb_def - in_correct_ready_q_def etcb_at_def is_etcb_at_def) + by (fastforce dest!: state_relation_ready_queues_relation + in_ready_q_tcbQueued_eq[where t=tcbPtr] + simp: obj_at'_def opt_pred_def opt_map_def in_correct_ready_q_def + obj_at_def etcb_at_def etcbs_of'_def) apply (find_goal \match conclusion in "corres _ _ _ _ (return ())" \ \-\\) apply (rule monadic_rewrite_corres_l[where P=P and Q=P for P, simplified]) apply (clarsimp simp: set_tcb_queue_def) @@ -277,16 +276,15 @@ lemma tcbSchedAppend_corres: apply (drule set_tcb_queue_new_state) apply (wpsimp wp: threadSet_wp simp: setQueue_def tcbQueueAppend_def) apply normalise_obj_at' - apply (frule (1) tcb_at_is_etcb_at) - apply (clarsimp simp: obj_at_def is_etcb_at_def etcb_at_def) - apply (rename_tac s d p s' tcb' tcb etcb) - apply (frule_tac t=tcbPtr in ekheap_relation_tcb_domain_priority) + apply (clarsimp simp: obj_at_def) + apply (rename_tac s d p s' tcb' tcb) + apply (frule_tac t=tcbPtr in pspace_relation_tcb_domain_priority) apply (force simp: obj_at_def) apply (force simp: obj_at'_def) apply (clarsimp split: if_splits) apply (cut_tac ts="ready_queues s d p" in list_queue_relation_nil) apply (force dest!: spec simp: list_queue_relation_def) - apply (cut_tac ts="ready_queues s (tcb_domain etcb) (tcb_priority etcb)" + apply (cut_tac ts="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" in obj_at'_tcbQueueEnd_ksReadyQueues) apply fast apply fast @@ -296,8 +294,8 @@ lemma tcbSchedAppend_corres: apply (force dest!: spec simp: list_queue_relation_def) apply (clarsimp simp: list_queue_relation_def) - apply (case_tac "d \ tcb_domain etcb \ p \ tcb_priority etcb") - apply (cut_tac d=d and d'="tcb_domain etcb" and p=p and p'="tcb_priority etcb" + apply (case_tac "d \ tcb_domain tcb \ p \ tcb_priority tcb") + apply (cut_tac d=d and d'="tcb_domain tcb" and p=p and p'="tcb_priority tcb" in ready_queues_disjoint) apply force apply fastforce @@ -321,14 +319,14 @@ lemma tcbSchedAppend_corres: apply (clarsimp simp: fun_upd_apply split: if_splits) \ \the ready queue was not originally empty\ - apply (clarsimp simp: etcb_at_def obj_at'_def) - apply (prop_tac "the (tcbQueueEnd (ksReadyQueues s' (tcb_domain etcb, tcb_priority etcb))) + apply (clarsimp simp: obj_at'_def) + apply (prop_tac "the (tcbQueueEnd (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb))) \ set (ready_queues s d p)") apply (erule orthD2) - apply (drule_tac x="tcb_domain etcb" in spec) - apply (drule_tac x="tcb_priority etcb" in spec) + apply (drule_tac x="tcb_domain tcb" in spec) + apply (drule_tac x="tcb_priority tcb" in spec) apply clarsimp - apply (drule_tac x="the (tcbQueueEnd (ksReadyQueues s' (tcb_domain etcb, tcb_priority etcb)))" + apply (drule_tac x="the (tcbQueueEnd (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb)))" in spec) subgoal by (auto simp: in_opt_pred opt_map_red) apply (intro conjI impI allI) @@ -345,7 +343,7 @@ lemma tcbSchedAppend_corres: apply (case_tac "ready_queues s d p"; force simp: tcbQueueEmpty_def) apply (case_tac "t = tcbPtr") apply (clarsimp simp: inQ_def fun_upd_apply split: if_splits) - apply (case_tac "t = the (tcbQueueEnd (ksReadyQueues s' (tcb_domain etcb, tcb_priority etcb)))") + apply (case_tac "t = the (tcbQueueEnd (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb)))") apply (clarsimp simp: inQ_def opt_pred_def fun_upd_apply) apply (clarsimp simp: inQ_def in_opt_pred opt_map_def fun_upd_apply) apply (clarsimp simp: fun_upd_apply split: if_splits) @@ -353,9 +351,9 @@ lemma tcbSchedAppend_corres: \ \d = tcb_domain tcb \ p = tcb_priority tcb\ apply clarsimp - apply (drule_tac x="tcb_domain etcb" in spec) - apply (drule_tac x="tcb_priority etcb" in spec) - apply (cut_tac ts="ready_queues s (tcb_domain etcb) (tcb_priority etcb)" + apply (drule_tac x="tcb_domain tcb" in spec) + apply (drule_tac x="tcb_priority tcb" in spec) + apply (cut_tac ts="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" in tcbQueueHead_iff_tcbQueueEnd) apply (force simp: list_queue_relation_def) apply (frule valid_tcbs'_maxDomain[where t=tcbPtr], simp add: obj_at'_def) @@ -797,7 +795,7 @@ defs idleThreadNotQueued_def: "idleThreadNotQueued s \ obj_at' (Not \ tcbQueued) (ksIdleThread s) s" lemma idle_thread_not_queued: - "\valid_idle s; valid_queues s; valid_etcbs s\ + "\valid_idle s; valid_queues s\ \ \ (\d p. idle_thread s \ set (ready_queues s d p))" apply (clarsimp simp: valid_queues_def) apply (drule_tac x=d in spec) @@ -805,7 +803,7 @@ lemma idle_thread_not_queued: apply clarsimp apply (drule_tac x="idle_thread s" in bspec) apply fastforce - apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def valid_etcbs_def) + apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) done lemma valid_idle_tcb_at: @@ -813,12 +811,12 @@ lemma valid_idle_tcb_at: by (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def is_tcb_def) lemma setCurThread_corres: - "corres dc (valid_idle and valid_queues and valid_etcbs and pspace_aligned and pspace_distinct) \ + "corres dc (valid_idle and valid_queues and pspace_aligned and pspace_distinct) \ (modify (cur_thread_update (\_. t))) (setCurThread t)" apply (clarsimp simp: setCurThread_def) apply (rule corres_stateAssert_add_assertion[rotated]) apply (clarsimp simp: idleThreadNotQueued_def) - apply (frule (2) idle_thread_not_queued) + apply (frule (1) idle_thread_not_queued) apply (frule state_relation_pspace_relation) apply (frule state_relation_ready_queues_relation) apply (frule state_relation_idle_thread) @@ -886,6 +884,7 @@ crunch arch_switch_to_thread, arch_switch_to_idle_thread and pspace_distinct[wp]: pspace_distinct and ready_qs_distinct[wp]: ready_qs_distinct and valid_idle[wp]: valid_idle + and ready_queues[wp]: "\s. P (ready_queues s)" (wp: ready_qs_distinct_lift simp: crunch_simps) lemma valid_queues_in_correct_ready_q[elim!]: @@ -901,7 +900,7 @@ lemma switchToThread_corres: and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and pspace_in_kernel_window and unique_table_refs - and st_tcb_at runnable t and valid_etcbs and (\s. sym_refs (state_hyp_refs_of s)) + and st_tcb_at runnable t and (\s. sym_refs (state_hyp_refs_of s)) and valid_queues and valid_idle) (no_0_obj' and sym_heap_sched_pointers and valid_objs') (switch_to_thread t) (switchToThread t)" @@ -922,7 +921,7 @@ lemma switchToThread_corres: apply (rule corres_guard_imp) apply (rule corres_split[OF arch_switchToThread_corres]) apply (rule corres_split[OF tcbSchedDequeue_corres setCurThread_corres]) - apply (wpsimp simp: is_tcb_def)+ + apply (wpsimp simp: is_tcb_def wp: in_correct_ready_q_lift)+ apply (fastforce intro!: st_tcb_at_tcb_at) apply wpsimp apply wpsimp @@ -974,7 +973,7 @@ lemma arch_switchToIdleThread_corres: lemma switchToIdleThread_corres: "corres dc - (invs and valid_queues and valid_etcbs) + (invs and valid_queues) invs_no_cicd' switch_to_idle_thread switchToIdleThread" apply (simp add: switch_to_idle_thread_def Thread_H.switchToIdleThread_def) @@ -1612,7 +1611,7 @@ lemma guarded_switch_to_corres: and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and pspace_in_kernel_window and unique_table_refs - and st_tcb_at runnable t and valid_etcbs and (\s. sym_refs (state_hyp_refs_of s)) + and st_tcb_at runnable t and (\s. sym_refs (state_hyp_refs_of s)) and valid_queues and valid_idle) (no_0_obj' and sym_heap_sched_pointers and valid_objs') (guarded_switch_to t) (switchToThread t)" @@ -1850,25 +1849,27 @@ lemma schact_bind_inside: "do x \ f; (case act of resume_cur_thread \ apply (case_tac act,simp_all) done -interpretation tcb_sched_action_extended: is_extended' "tcb_sched_action f a" - by (unfold_locales) - lemma getDomainTime_corres: "corres (=) \ \ (gets domain_time) getDomainTime" by (simp add: getDomainTime_def state_relation_def) +lemma reset_work_units_equiv: + "do_extended_op (modify (work_units_completed_update (\_. 0))) + = (modify (work_units_completed_update (\_. 0)))" + by (clarsimp simp: reset_work_units_def[symmetric]) + lemma nextDomain_corres: "corres dc \ \ next_domain nextDomain" - apply (simp add: next_domain_def nextDomain_def) + apply (clarsimp simp: next_domain_def nextDomain_def reset_work_units_equiv modify_modify) apply (rule corres_modify) - apply (simp add: state_relation_def Let_def dschLength_def dschDomain_def) + apply (simp add: state_relation_def Let_def dschLength_def dschDomain_def cdt_relation_def) done lemma next_domain_valid_sched[wp]: "\ valid_sched and (\s. scheduler_action s = choose_new_thread)\ next_domain \ \_. valid_sched \" apply (simp add: next_domain_def Let_def) - apply (wp, simp add: valid_sched_def valid_sched_action_2_def ct_not_in_q_2_def) - apply (simp add:valid_blocked_2_def) + apply (wpsimp wp: dxo_wp_weak) + apply (clarsimp simp: valid_sched_def) done lemma nextDomain_invs_no_cicd': @@ -1902,7 +1903,7 @@ lemma scheduleChooseNewThread_fragment_corres: lemma scheduleSwitchThreadFastfail_corres: "\ ct \ it \ (tp = tp' \ cp = cp') ; ct = ct' ; it = it' \ \ - corres ((=)) (is_etcb_at ct) (tcb_at' ct) + corres ((=)) (is_tcb_at ct) (tcb_at' ct) (schedule_switch_thread_fastfail ct it cp tp) (scheduleSwitchThreadFastfail ct' it' cp' tp')" by (clarsimp simp: schedule_switch_thread_fastfail_def scheduleSwitchThreadFastfail_def) @@ -1941,9 +1942,6 @@ lemma isHighestPrio_corres: apply (wpsimp simp: if_apply_def2 wp: hoare_drop_imps ksReadyQueuesL1Bitmap_return_wp)+ done -crunch set_scheduler_action - for valid_idle_etcb[wp]: valid_idle_etcb - crunch isHighestPrio for inv[wp]: P crunch curDomain @@ -1971,13 +1969,13 @@ lemma scheduleChooseNewThread_corres: apply auto done -lemma ethread_get_when_corres: - assumes x: "\etcb tcb'. etcb_relation etcb tcb' \ r (f etcb) (f' tcb')" - shows "corres (\rv rv'. b \ r rv rv') (is_etcb_at t) (tcb_at' t) - (ethread_get_when b f t) (threadGet f' t)" - apply (clarsimp simp: ethread_get_when_def) +lemma thread_get_when_corres: + assumes x: "\tcb tcb'. tcb_relation tcb tcb' \ r (f tcb) (f' tcb')" + shows "corres (\rv rv'. b \ r rv rv') (tcb_at t and pspace_aligned and pspace_distinct) (tcb_at' t) + ((if b then thread_get f t else return 0)) (threadGet f' t)" + apply clarsimp apply (rule conjI; clarsimp) - apply (rule corres_guard_imp, rule ethreadget_corres; simp add: x) + apply (rule corres_guard_imp, rule threadGet_corres; simp add: x) apply (clarsimp simp: threadGet_def) apply (rule corres_noop) apply wpsimp+ @@ -1986,31 +1984,29 @@ lemma ethread_get_when_corres: lemma tcb_sched_enqueue_in_correct_ready_q[wp]: "tcb_sched_action tcb_sched_enqueue t \in_correct_ready_q\ " unfolding tcb_sched_action_def tcb_sched_enqueue_def set_tcb_queue_def - apply wpsimp - apply (clarsimp simp: in_correct_ready_q_def obj_at_def etcb_at_def is_etcb_at_def - split: option.splits) + apply (wpsimp wp: thread_get_wp') + apply (clarsimp simp: in_correct_ready_q_def obj_at_def etcb_at_def is_etcb_at_def etcbs_of'_def) done lemma tcb_sched_append_in_correct_ready_q[wp]: "tcb_sched_action tcb_sched_append tcb_ptr \in_correct_ready_q\ " unfolding tcb_sched_action_def tcb_sched_append_def - apply wpsimp - apply (clarsimp simp: in_correct_ready_q_def obj_at_def etcb_at_def is_etcb_at_def - split: option.splits) + apply (wpsimp wp: thread_get_wp') + apply (clarsimp simp: in_correct_ready_q_def obj_at_def etcb_at_def is_etcb_at_def etcbs_of'_def) done lemma tcb_sched_enqueue_ready_qs_distinct[wp]: "tcb_sched_action tcb_sched_enqueue t \ready_qs_distinct\ " unfolding tcb_sched_action_def set_tcb_queue_def apply (wpsimp wp: thread_get_wp') - apply (clarsimp simp: ready_qs_distinct_def etcb_at_def is_etcb_at_def split: option.splits) + apply (clarsimp simp: ready_qs_distinct_def etcb_at_def is_etcb_at_def) done lemma tcb_sched_append_ready_qs_distinct[wp]: "tcb_sched_action tcb_sched_append t \ready_qs_distinct\ " unfolding tcb_sched_action_def tcb_sched_append_def set_tcb_queue_def apply (wpsimp wp: thread_get_wp') - apply (clarsimp simp: ready_qs_distinct_def etcb_at_def is_etcb_at_def split: option.splits) + apply (clarsimp simp: ready_qs_distinct_def etcb_at_def is_etcb_at_def) done crunch set_scheduler_action @@ -2023,9 +2019,11 @@ crunch reschedule_required and ready_qs_distinct[wp]: ready_qs_distinct (ignore: tcb_sched_action wp: crunch_wps) +crunch tcb_sched_action + for valid_vs_lookup[wp]: valid_vs_lookup + lemma schedule_corres: "corres dc (invs and valid_sched and valid_list) invs' (Schedule_A.schedule) ThreadDecls_H.schedule" - supply ethread_get_wp[wp del] supply ssa_wp[wp del] supply tcbSchedEnqueue_invs'[wp del] supply tcbSchedEnqueue_invs'_not_ResumeCurrentThread[wp del] @@ -2064,12 +2062,12 @@ lemma schedule_corres: apply (rule corres_split[OF getIdleThread_corres], rename_tac it it') apply (rule_tac F="was_running \ ct \ it" in corres_gen_asm) apply (rule corres_split) - apply (rule ethreadget_corres[where r="(=)"]) - apply (clarsimp simp: etcb_relation_def) + apply (rule threadGet_corres[where r="(=)"]) + apply (clarsimp simp: tcb_relation_def) apply (rename_tac tp tp') apply (rule corres_split) - apply (rule ethread_get_when_corres[where r="(=)"]) - apply (clarsimp simp: etcb_relation_def) + apply (rule thread_get_when_corres[where r="(=)"]) + apply (clarsimp simp: tcb_relation_def) apply (rename_tac cp cp') apply (rule corres_split) apply (rule scheduleSwitchThreadFastfail_corres; simp) @@ -2131,7 +2129,7 @@ lemma schedule_corres: apply clarsimp subgoal for s - apply (clarsimp split: Deterministic_A.scheduler_action.splits + apply (clarsimp split: Structures_A.scheduler_action.splits simp: invs_psp_aligned invs_distinct invs_valid_objs invs_arch_state invs_vspace_objs[simplified] tcb_at_invs) apply (rule conjI, clarsimp) @@ -2143,14 +2141,13 @@ lemma schedule_corres: subgoal for candidate apply (clarsimp simp: valid_sched_def invs_def valid_state_def cur_tcb_def valid_arch_caps_def valid_sched_action_def - weak_valid_sched_action_def tcb_at_is_etcb_at - tcb_at_is_etcb_at[OF st_tcb_at_tcb_at[rotated]] + weak_valid_sched_action_def valid_blocked_except_def valid_blocked_def invs_hyp_sym_refs) apply (fastforce simp add: pred_tcb_at_def obj_at_def is_tcb valid_idle_def) done (* choose new thread case *) apply (intro impI conjI allI tcb_at_invs - | fastforce simp: invs_def cur_tcb_def valid_etcbs_def + | fastforce simp: invs_def cur_tcb_def valid_sched_def st_tcb_at_def obj_at_def valid_state_def weak_valid_sched_action_def not_cur_thread_def)+ done @@ -2500,7 +2497,7 @@ lemma sbn_sch_act_sane: lemma possibleSwitchTo_corres: "corres dc - (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t + (weak_valid_sched_action and cur_tcb and st_tcb_at runnable t and in_correct_ready_q and ready_qs_distinct and pspace_aligned and pspace_distinct) ((\s. weak_sch_act_wf (ksSchedulerAction s) s) and sym_heap_sched_pointers and valid_sched_pointers and valid_objs') @@ -2509,7 +2506,6 @@ lemma possibleSwitchTo_corres: apply (fastforce dest: pspace_aligned_cross) apply (rule_tac Q'=pspace_distinct' in corres_cross_add_guard) apply (fastforce dest: pspace_distinct_cross) - supply ethread_get_wp[wp del] apply (rule corres_cross_over_guard[where P'=Q and Q="tcb_at' t and Q" for Q]) apply (clarsimp simp: state_relation_def) apply (rule tcb_at_cross, erule st_tcb_at_tcb_at; assumption) @@ -2517,8 +2513,8 @@ lemma possibleSwitchTo_corres: apply (rule corres_guard_imp) apply (rule corres_split[OF curDomain_corres], simp) apply (rule corres_split) - apply (rule ethreadget_corres[where r="(=)"]) - apply (clarsimp simp: etcb_relation_def) + apply (rule threadGet_corres[where r="(=)"]) + apply (clarsimp simp: tcb_relation_def) apply (rule corres_split[OF getSchedulerAction_corres]) apply (rule corres_if, simp) apply (rule tcbSchedEnqueue_corres, simp) @@ -2528,14 +2524,9 @@ lemma possibleSwitchTo_corres: apply (rule tcbSchedEnqueue_corres, simp) apply (wp reschedule_required_valid_queues | strengthen valid_objs'_valid_tcbs')+ apply (rule setSchedulerAction_corres, simp) - apply (wpsimp simp: if_apply_def2 - wp: hoare_drop_imp[where f="ethread_get a b" for a b])+ - apply (wp hoare_drop_imps)[1] - apply wp+ - apply (clarsimp simp: valid_sched_def invs_def valid_state_def cur_tcb_def st_tcb_at_tcb_at - valid_sched_action_def weak_valid_sched_action_def - tcb_at_is_etcb_at[OF st_tcb_at_tcb_at[rotated]]) - apply (fastforce simp: tcb_at_is_etcb_at) + apply (wpsimp wp: hoare_drop_imps)+ + apply (clarsimp simp: st_tcb_at_tcb_at) + apply fastforce done end diff --git a/proof/refine/AARCH64/StateRelation.thy b/proof/refine/AARCH64/StateRelation.thy index e8f13fae54..06b7d00e75 100644 --- a/proof/refine/AARCH64/StateRelation.thy +++ b/proof/refine/AARCH64/StateRelation.thy @@ -182,7 +182,10 @@ definition tcb_relation :: "Structures_A.tcb \ Structures_H.tcb \ cap_relation (tcb_caller tcb) (cteCap (tcbCaller tcb')) \ cap_relation (tcb_ipcframe tcb) (cteCap (tcbIPCBufferFrame tcb')) \ tcb_bound_notification tcb = tcbBoundNotification tcb' - \ tcb_mcpriority tcb = tcbMCP tcb'" + \ tcb_mcpriority tcb = tcbMCP tcb' + \ tcb_priority tcb = tcbPriority tcb' + \ tcb_time_slice tcb = tcbTimeSlice tcb' + \ tcb_domain tcb = tcbDomain tcb'" \ \ A pair of objects @{term "(obj, obj')"} should satisfy the following relation when, under further @@ -320,18 +323,7 @@ definition pspace_relation :: (pspace_dom ab = dom con) \ (\x \ dom ab. \(y, P) \ obj_relation_cuts (the (ab x)) x. P (the (ab x)) (the (con y)))" -definition etcb_relation :: "etcb \ Structures_H.tcb \ bool" where - "etcb_relation \ \etcb tcb'. - tcb_priority etcb = tcbPriority tcb' - \ tcb_time_slice etcb = tcbTimeSlice tcb' - \ tcb_domain etcb = tcbDomain tcb'" - -definition ekheap_relation :: - "(obj_ref \ etcb option) \ (machine_word \ Structures_H.kernel_object) \ bool" where - "ekheap_relation ab con \ - \x \ dom ab. \tcb'. con x = Some (KOTCB tcb') \ etcb_relation (the (ab x)) tcb'" - -primrec sched_act_relation :: "Deterministic_A.scheduler_action \ scheduler_action \ bool" +primrec sched_act_relation :: "Structures_A.scheduler_action \ scheduler_action \ bool" where "sched_act_relation resume_cur_thread a' = (a' = ResumeCurrentThread)" | "sched_act_relation choose_new_thread a' = (a' = ChooseNewThread)" | @@ -359,8 +351,8 @@ lemma list_queue_relation_nil: by (fastforce dest: heap_path_head simp: tcbQueueEmpty_def list_queue_relation_def) definition ready_queue_relation :: - "Deterministic_A.domain \ Structures_A.priority - \ Deterministic_A.ready_queue \ ready_queue + "Structures_A.domain \ Structures_A.priority + \ Structures_A.ready_queue \ ready_queue \ (obj_ref \ obj_ref) \ (obj_ref \ obj_ref) \ (obj_ref \ bool) \ bool" where @@ -370,7 +362,7 @@ definition ready_queue_relation :: \ (d > maxDomain \ p > maxPriority \ tcbQueueEmpty q')" definition ready_queues_relation_2 :: - "(Deterministic_A.domain \ Structures_A.priority \ Deterministic_A.ready_queue) + "(Structures_A.domain \ Structures_A.priority \ Structures_A.ready_queue) \ (domain \ priority \ ready_queue) \ (obj_ref \ obj_ref) \ (obj_ref \ obj_ref) \ (domain \ priority \ obj_ref \ bool) \ bool" @@ -525,7 +517,6 @@ definition APIType_map :: "Structures_A.apiobject_type \ AARCH64_H.o definition state_relation :: "(det_state \ kernel_state) set" where "state_relation \ {(s, s'). pspace_relation (kheap s) (ksPSpace s') - \ ekheap_relation (ekheap s) (ksPSpace s') \ sched_act_relation (scheduler_action s) (ksSchedulerAction s') \ ready_queues_relation s s' \ ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') (gsPTTypes (ksArchState s')) @@ -557,10 +548,6 @@ lemma state_relation_pspace_relation[elim!]: "(s,s') \ state_relation \ pspace_relation (kheap s) (ksPSpace s')" by (simp add: state_relation_def) -lemma state_relation_ekheap_relation[elim!]: - "(s,s') \ state_relation \ ekheap_relation (ekheap s) (ksPSpace s')" - by (simp add: state_relation_def) - lemma state_relation_sched_act_relation[elim!]: "(s,s') \ state_relation \ sched_act_relation (scheduler_action s) (ksSchedulerAction s')" by (clarsimp simp: state_relation_def) @@ -576,7 +563,6 @@ lemma state_relation_idle_thread[elim!]: lemma state_relationD: "(s, s') \ state_relation \ pspace_relation (kheap s) (ksPSpace s') \ - ekheap_relation (ekheap s) (ksPSpace s') \ sched_act_relation (scheduler_action s) (ksSchedulerAction s') \ ready_queues_relation s s' \ ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') (gsPTTypes (ksArchState s')) \ @@ -598,7 +584,6 @@ lemma state_relationD: lemma state_relationE [elim?]: assumes sr: "(s, s') \ state_relation" and rl: "\ pspace_relation (kheap s) (ksPSpace s'); - ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation s s'; ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') (gsPTTypes (ksArchState s')); @@ -647,11 +632,6 @@ lemma pspace_relation_absD: apply (fastforce simp: image_def intro: rev_bexI) done -lemma ekheap_relation_absD: - "\ ab x = Some y; ekheap_relation ab con \ \ - \tcb'. con x = Some (KOTCB tcb') \ etcb_relation y tcb'" - by (force simp add: ekheap_relation_def) - lemma in_related_pspace_dom: "\ s' x = Some y; pspace_relation s s' \ \ x \ pspace_dom s" by (clarsimp simp add: pspace_relation_def) diff --git a/proof/refine/AARCH64/Syscall_R.thy b/proof/refine/AARCH64/Syscall_R.thy index 8a5061f324..9bdb038f64 100644 --- a/proof/refine/AARCH64/Syscall_R.thy +++ b/proof/refine/AARCH64/Syscall_R.thy @@ -351,7 +351,7 @@ lemma threadSet_tcbDomain_update_sch_act_wf[wp]: lemma setDomain_corres: "corres dc - (valid_etcbs and valid_sched and tcb_at tptr and pspace_aligned and pspace_distinct) + (valid_sched and tcb_at tptr and pspace_aligned and pspace_distinct) (invs' and sch_act_simple and tcb_at' tptr and (\s. new_dom \ maxDomain)) (set_domain tptr new_dom) (setDomain tptr new_dom)" apply (rule corres_gen_asm2) @@ -360,8 +360,8 @@ lemma setDomain_corres: apply (rule corres_split[OF getCurThread_corres]) apply (rule corres_split[OF tcbSchedDequeue_corres], simp) apply (rule corres_split) - apply (rule ethread_set_corres; simp) - apply (clarsimp simp: etcb_relation_def) + apply (rule threadSet_not_queued_corres; + simp add: tcb_relation_def tcb_cap_cases_def tcb_cte_cases_def cteSizeBits_def) apply (rule corres_split[OF isRunnable_corres]) apply simp apply (rule corres_split) @@ -374,9 +374,9 @@ lemma setDomain_corres: apply ((wpsimp wp: hoare_drop_imps | strengthen valid_objs'_valid_tcbs')+)[1] apply (wpsimp wp: gts_wp) apply wpsimp - apply ((wpsimp wp: hoare_vcg_imp_lift' ethread_set_not_queued_valid_queues hoare_vcg_all_lift - | strengthen valid_objs'_valid_tcbs' valid_queues_in_correct_ready_q - valid_queues_ready_qs_distinct)+)[1] + apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_all_lift + thread_set_in_correct_ready_q_not_queued thread_set_no_change_tcb_state + thread_set_no_change_tcb_state_converse thread_set_weak_valid_sched_action) apply (rule_tac Q'="\_. valid_objs' and sym_heap_sched_pointers and valid_sched_pointers and pspace_aligned' and pspace_distinct' and (\s. sch_act_wf (ksSchedulerAction s) s) and tcb_at' tptr" @@ -385,7 +385,7 @@ lemma setDomain_corres: apply (wpsimp wp: threadSet_valid_objs' threadSet_sched_pointers threadSet_valid_sched_pointers)+ apply (rule_tac Q'="\_ s. valid_queues s \ not_queued tptr s - \ pspace_aligned s \ pspace_distinct s \ valid_etcbs s + \ pspace_aligned s \ pspace_distinct s \ weak_valid_sched_action s" in hoare_post_imp) apply (fastforce simp: pred_tcb_at_def obj_at_def) @@ -399,10 +399,7 @@ lemma setDomain_corres: apply (clarsimp simp: tcb_cte_cases_def cteSizeBits_def) apply fastforce apply (wp hoare_vcg_all_lift tcbSchedDequeue_not_queued)+ - apply clarsimp - apply (frule tcb_at_is_etcb_at) - apply simp+ - apply (auto elim: tcb_at_is_etcb_at valid_objs'_maxDomain valid_objs'_maxPriority pred_tcb'_weakenE + apply (auto elim: valid_objs'_maxDomain valid_objs'_maxPriority pred_tcb'_weakenE simp: valid_sched_def valid_sched_action_def) done @@ -1572,8 +1569,7 @@ lemma handleYield_corres: | strengthen valid_objs'_valid_tcbs' valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct)+ apply (simp add: invs_def valid_sched_def valid_sched_action_def cur_tcb_def - tcb_at_is_etcb_at valid_state_def valid_pspace_def ct_in_state_def - runnable_eq_active) + valid_state_def valid_pspace_def ct_in_state_def runnable_eq_active) apply (fastforce simp: invs'_def valid_state'_def ct_in_state'_def sch_act_wf_weak cur_tcb'_def valid_pspace_valid_objs' valid_objs'_maxDomain tcb_in_cur_domain'_def) done @@ -1821,10 +1817,6 @@ lemma handleReply_nonz_cap_to_ct: crunch handleFaultReply for ksQ[wp]: "\s. P (ksReadyQueues s p)" -crunch handle_recv - for valid_etcbs[wp]: "valid_etcbs" - (wp: crunch_wps simp: crunch_simps) - lemma handleReply_handleRecv_corres: "corres dc (einvs and ct_running) (invs' and ct_running' and (\s. ksSchedulerAction s = ResumeCurrentThread)) diff --git a/proof/refine/AARCH64/TcbAcc_R.thy b/proof/refine/AARCH64/TcbAcc_R.thy index 4520609f36..0f7ebb4d5e 100644 --- a/proof/refine/AARCH64/TcbAcc_R.thy +++ b/proof/refine/AARCH64/TcbAcc_R.thy @@ -341,29 +341,27 @@ lemma setObject_update_TCB_corres': assumes tables': "\(getF, v) \ ran tcb_cte_cases. getF new_tcb' = getF tcb'" assumes sched_pointers: "tcbSchedPrev new_tcb' = tcbSchedPrev tcb'" "tcbSchedNext new_tcb' = tcbSchedNext tcb'" - assumes flag: "tcbQueued new_tcb' = tcbQueued tcb'" + assumes flag: "\d p. inQ d p new_tcb' = inQ d p tcb'" assumes r: "r () ()" - assumes exst: "exst_same tcb' new_tcb'" shows "corres r (ko_at (TCB tcb) ptr) (ko_at' tcb' ptr) (set_object ptr (TCB new_tcb)) (setObject ptr new_tcb')" - apply (rule_tac F="tcb_relation tcb tcb' \ exst_same tcb' new_tcb'" in corres_req) + apply (rule_tac F="tcb_relation tcb tcb'" in corres_req) apply (clarsimp simp: state_relation_def obj_at_def obj_at'_def) apply (frule(1) pspace_relation_absD) - apply (clarsimp simp: tcb_relation_cut_def exst) + apply (clarsimp simp: tcb_relation_cut_def) apply (rule corres_no_failI) - apply (rule no_fail_pre) - apply wp + apply wp apply (clarsimp simp: obj_at'_def) apply (unfold set_object_def setObject_def) apply (clarsimp simp: in_monad split_def bind_def gets_def get_def Bex_def - put_def return_def modify_def get_object_def projectKOs obj_at_def - updateObject_default_def in_magnitude_check obj_at'_def) - apply (rename_tac s s' t') - apply (prop_tac "t' = s'") - apply (clarsimp simp: magnitudeCheck_def in_monad split: option.splits) - apply (drule singleton_in_magnitude_check) + put_def return_def modify_def get_object_def obj_at_def + updateObject_default_def in_magnitude_check objBits_less_word_bits) + apply (rename_tac s s' ko) + apply (prop_tac "ko = tcb'") + apply (clarsimp simp: obj_at'_def project_inject) + apply (clarsimp simp: state_relation_def) apply (prop_tac "map_to_ctes ((ksPSpace s') (ptr \ injectKO new_tcb')) = map_to_ctes (ksPSpace s')") apply (frule_tac tcb=new_tcb' and tcb=tcb' in map_to_ctes_upd_tcb) @@ -371,72 +369,57 @@ lemma setObject_update_TCB_corres': apply (clarsimp simp: objBits_simps ps_clear_def3 field_simps objBits_defs mask_def) apply (insert tables')[1] apply (rule ext) - apply (clarsimp split: if_splits) - apply blast + subgoal by auto apply (prop_tac "obj_at (same_caps (TCB new_tcb)) ptr s") using tables apply (fastforce simp: obj_at_def) - apply (clarsimp simp: caps_of_state_after_update cte_wp_at_after_update swp_def + apply (clarsimp simp: caps_of_state_after_update cte_wp_at_after_update swp_def fun_upd_def obj_at_def assms) - apply (clarsimp simp add: state_relation_def) apply (subst conj_assoc[symmetric]) apply (extract_conjunct \match conclusion in "ghost_relation _ _ _ _" \ -\) - apply (clarsimp simp add: ghost_relation_def) + apply (clarsimp simp: ghost_relation_def) apply (erule_tac x=ptr in allE)+ apply clarsimp - apply (simp only: pspace_relation_def pspace_dom_update dom_fun_upd2 simp_thms) - apply (elim conjE) - apply (frule bspec, erule domI) - apply clarsimp - apply (rule conjI) + apply (extract_conjunct \match conclusion in "pspace_relation _ _" \ -\) + apply (fold fun_upd_def) apply (simp only: pspace_relation_def simp_thms pspace_dom_update[where x="kernel_object.TCB _" and v="kernel_object.TCB _", simplified a_type_def, simplified]) - apply (rule conjI) using assms apply (simp only: dom_fun_upd2 simp_thms) + apply (elim conjE) apply (frule bspec, erule domI) apply (rule ballI, drule(1) bspec) apply (drule domD) - apply (clarsimp simp: tcb_relation_cut_def project_inject split: if_split_asm kernel_object.split_asm) + apply (clarsimp simp: project_inject tcb_relation_cut_def + split: if_split_asm kernel_object.split_asm) apply (rename_tac aa ba) apply (drule_tac x="(aa, ba)" in bspec, simp) apply clarsimp apply (frule_tac ko'="kernel_object.TCB tcb" and x'=ptr in obj_relation_cut_same_type) apply (simp add: tcb_relation_cut_def)+ apply clarsimp - apply (extract_conjunct \match conclusion in "ekheap_relation _ _" \ -\) - apply (simp only: ekheap_relation_def) - apply (rule ballI, drule (1) bspec) - apply (insert exst) - apply (clarsimp simp: etcb_relation_def exst_same_def) - apply (extract_conjunct \match conclusion in "ready_queues_relation_2 _ _ _ _ _" \ -\) - apply (insert sched_pointers flag exst) - apply (clarsimp simp: ready_queues_relation_def Let_def) - apply (prop_tac "(tcbSchedNexts_of s')(ptr := tcbSchedNext new_tcb') = tcbSchedNexts_of s'") - apply (fastforce simp: opt_map_def) - apply (prop_tac "(tcbSchedPrevs_of s')(ptr := tcbSchedPrev new_tcb') = tcbSchedPrevs_of s'") - apply (fastforce simp: opt_map_def) - apply (clarsimp simp: ready_queue_relation_def opt_pred_def opt_map_def exst_same_def inQ_def - split: option.splits) - apply (metis (mono_tags, opaque_lifting)) - apply (clarsimp simp: fun_upd_def caps_of_state_after_update cte_wp_at_after_update swp_def - obj_at_def) - done + apply (insert sched_pointers flag) + apply (clarsimp simp: ready_queues_relation_def Let_def) + apply (prop_tac "(tcbSchedNexts_of s')(ptr := tcbSchedNext new_tcb') = tcbSchedNexts_of s'") + apply (fastforce simp: opt_map_def) + apply (prop_tac "(tcbSchedPrevs_of s')(ptr := tcbSchedPrev new_tcb') = tcbSchedPrevs_of s'") + apply (fastforce simp: opt_map_def) + by (clarsimp simp: ready_queue_relation_def opt_pred_def opt_map_def split: option.splits) lemma setObject_update_TCB_corres: "\tcb_relation tcb tcb' \ tcb_relation new_tcb new_tcb'; \(getF, v) \ ran tcb_cap_cases. getF new_tcb = getF tcb; \(getF, v) \ ran tcb_cte_cases. getF new_tcb' = getF tcb'; tcbSchedPrev new_tcb' = tcbSchedPrev tcb'; tcbSchedNext new_tcb' = tcbSchedNext tcb'; - tcbQueued new_tcb' = tcbQueued tcb'; exst_same tcb' new_tcb'; + \d p. inQ d p new_tcb' = inQ d p tcb'; r () ()\ \ corres r (\s. get_tcb ptr s = Some tcb) (\s'. (tcb', s') \ fst (getObject ptr s')) (set_object ptr (TCB new_tcb)) (setObject ptr new_tcb')" apply (rule corres_guard_imp) - apply (erule (7) setObject_update_TCB_corres') + apply (erule (4) setObject_update_TCB_corres'; fastforce) apply (clarsimp simp: getObject_def in_monad split_def obj_at'_def loadObject_default_def objBits_simps' in_magnitude_check)+ done @@ -490,8 +473,7 @@ lemma threadset_corresT: getF (f' tcb) = getF tcb" assumes sched_pointers: "\tcb. tcbSchedPrev (f' tcb) = tcbSchedPrev tcb" "\tcb. tcbSchedNext (f' tcb) = tcbSchedNext tcb" - assumes flag: "\tcb. tcbQueued (f' tcb) = tcbQueued tcb" - assumes e: "\tcb'. exst_same tcb' (f' tcb')" + assumes flag: "\d p tcb'. inQ d p (f' tcb') = inQ d p tcb'" shows "corres dc (tcb_at t and pspace_aligned and pspace_distinct) \ (thread_set f t) (threadSet f' t)" @@ -499,15 +481,14 @@ lemma threadset_corresT: apply (rule corres_guard_imp) apply (rule corres_split[OF getObject_TCB_corres]) apply (rule setObject_update_TCB_corres') - apply (erule x) - apply (rule y) - apply (clarsimp simp: bspec_split [OF spec [OF z]]) - apply fastforce - apply (rule sched_pointers) + apply (erule x) + apply (rule y) + apply (clarsimp simp: bspec_split [OF spec [OF z]]) + apply fastforce apply (rule sched_pointers) - apply (rule flag) - apply simp - apply (rule e) + apply (rule sched_pointers) + apply (rule flag) + apply simp apply wp+ apply (clarsimp simp add: tcb_at_def obj_at_def) apply (drule get_tcb_SomeD) @@ -537,8 +518,7 @@ lemma threadSet_corres_noopT: getF (fn tcb) = getF tcb" assumes s: "\tcb'. tcbSchedPrev (fn tcb') = tcbSchedPrev tcb'" "\tcb'. tcbSchedNext (fn tcb') = tcbSchedNext tcb'" - assumes f: "\tcb'. tcbQueued (fn tcb') = tcbQueued tcb'" - assumes e: "\tcb'. exst_same tcb' (fn tcb')" + assumes f: "\d p tcb'. inQ d p (fn tcb') = inQ d p tcb'" shows "corres dc (tcb_at t and pspace_aligned and pspace_distinct) \ (return v) (threadSet fn t)" proof - @@ -556,13 +536,12 @@ proof - defer apply (subst bind_return [symmetric], rule corres_underlying_split [OF threadset_corresT]) - apply (simp add: x) - apply simp - apply (rule y) - apply (fastforce simp: s) + apply (simp add: x) + apply simp + apply (rule y) apply (fastforce simp: s) - apply (fastforce simp: f) - apply (rule e) + apply (fastforce simp: s) + apply (fastforce simp: f) apply (rule corres_noop [where P=\ and P'=\]) apply simp apply (rule no_fail_pre, wpsimp+)[1] @@ -582,19 +561,17 @@ lemma threadSet_corres_noop_splitT: assumes w: "\P'\ threadSet fn t \\x. Q'\" assumes s: "\tcb'. tcbSchedPrev (fn tcb') = tcbSchedPrev tcb'" "\tcb'. tcbSchedNext (fn tcb') = tcbSchedNext tcb'" - assumes f: "\tcb'. tcbQueued (fn tcb') = tcbQueued tcb'" - assumes e: "\tcb'. exst_same tcb' (fn tcb')" + assumes f: "\d p tcb'. inQ d p (fn tcb') = inQ d p tcb'" shows "corres r (tcb_at t and pspace_aligned and pspace_distinct and P) P' m (threadSet fn t >>= (\rv. m'))" apply (rule corres_guard_imp) apply (subst return_bind[symmetric]) apply (rule corres_split_nor[OF threadSet_corres_noopT]) - apply (simp add: x) - apply (rule y) - apply (fastforce simp: s) + apply (simp add: x) + apply (rule y) apply (fastforce simp: s) - apply (fastforce simp: f) - apply (rule e) + apply (fastforce simp: s) + apply (fastforce simp: f) apply (rule z) apply (wp w)+ apply simp @@ -1563,7 +1540,7 @@ proof - (set_object add (TCB (tcb \ tcb_arch := arch_tcb_context_set con (tcb_arch tcb) \))) (setObject add (tcb' \ tcbArch := atcbContextSet con' (tcbArch tcb') \))" by (rule setObject_update_TCB_corres [OF L2], - (simp add: tcb_cte_cases_def tcb_cap_cases_def cteSizeBits_def exst_same_def)+) + (simp add: tcb_cte_cases_def tcb_cap_cases_def cteSizeBits_def)+) have L4: "\con con'. con = con' \ corres (\(irv, nc) (irv', nc'). r irv irv' \ nc = nc') \ \ (select_f (f con)) (select_f (g con'))" @@ -1922,41 +1899,6 @@ lemma fun_if_triv[simp]: "(\x. if x = y then f y else f x) = f" by (force) -lemma corres_get_etcb: - "corres (etcb_relation) (is_etcb_at t) (tcb_at' t) - (gets_the (get_etcb t)) (getObject t)" - apply (rule corres_no_failI) - apply wp - apply (clarsimp simp add: get_etcb_def gets_the_def gets_def - get_def assert_opt_def bind_def - return_def fail_def - split: option.splits - ) - apply (frule in_inv_by_hoareD [OF getObject_inv_tcb]) - apply (clarsimp simp add: is_etcb_at_def obj_at'_def projectKO_def - projectKO_opt_tcb split_def - getObject_def loadObject_default_def in_monad) - apply (case_tac bb) - apply (simp_all add: fail_def return_def) - apply (clarsimp simp add: state_relation_def ekheap_relation_def) - apply (drule bspec) - apply clarsimp - apply blast - apply (clarsimp simp add: other_obj_relation_def lookupAround2_known1) - done - - -lemma ethreadget_corres: - assumes x: "\etcb tcb'. etcb_relation etcb tcb' \ r (f etcb) (f' tcb')" - shows "corres r (is_etcb_at t) (tcb_at' t) (ethread_get f t) (threadGet f' t)" - apply (simp add: ethread_get_def threadGet_def) - apply (fold liftM_def) - apply simp - apply (rule corres_rel_imp) - apply (rule corres_get_etcb) - apply (simp add: x) - done - lemma getQueue_corres: "corres (\ls q. (ls = [] \ tcbQueueEmpty q) \ (ls \ [] \ tcbQueueHead q = Some (hd ls)) \ queue_end_valid ls q) @@ -2007,13 +1949,14 @@ crunch removeFromBitmap lemmas addToBitmap_typ_ats [wp] = typ_at_lifts [OF addToBitmap_typ_at'] lemmas removeFromBitmap_typ_ats [wp] = typ_at_lifts [OF removeFromBitmap_typ_at'] -lemma ekheap_relation_tcb_domain_priority: - "\ekheap_relation (ekheap s) (ksPSpace s'); ekheap s t = Some (tcb); +lemma pspace_relation_tcb_domain_priority: + "\pspace_relation (kheap s) (ksPSpace s'); kheap s t = Some (TCB tcb); ksPSpace s' t = Some (KOTCB tcb')\ \ tcbDomain tcb' = tcb_domain tcb \ tcbPriority tcb' = tcb_priority tcb" - apply (clarsimp simp: ekheap_relation_def) - apply (drule_tac x=t in bspec, blast) - apply (clarsimp simp: other_obj_relation_def etcb_relation_def) + apply (clarsimp simp: pspace_relation_def) + apply (drule_tac x=t in bspec) + apply (fastforce simp: obj_at_def) + apply (clarsimp simp: obj_at_def obj_at'_def tcb_relation_cut_def tcb_relation_def) done lemma no_fail_thread_get[wp]: @@ -2060,86 +2003,17 @@ lemma threadSet_pspace_relation: apply (fastforce dest!: tcb_rel) done -lemma ekheap_relation_update_tcbs: - "\ ekheap_relation (ekheap s) (ksPSpace s'); ekheap s x = Some oetcb; - ksPSpace s' x = Some (KOTCB otcb'); etcb_relation etcb tcb' \ - \ ekheap_relation ((ekheap s)(x \ etcb)) ((ksPSpace s')(x \ KOTCB tcb'))" - by (simp add: ekheap_relation_def) - -lemma ekheap_relation_update_concrete_tcb: - "\ekheap_relation (ekheap s) (ksPSpace s'); ekheap s ptr = Some etcb; - ksPSpace s' ptr = Some (KOTCB otcb'); - etcb_relation etcb tcb'\ - \ ekheap_relation (ekheap s) ((ksPSpace s')(ptr \ KOTCB tcb'))" - by (fastforce dest: ekheap_relation_update_tcbs simp: map_upd_triv) - -lemma ekheap_relation_etcb_relation: - "\ekheap_relation (ekheap s) (ksPSpace s'); ekheap s ptr = Some etcb; - ksPSpace s' ptr = Some (KOTCB tcb')\ - \ etcb_relation etcb tcb'" - apply (clarsimp simp: ekheap_relation_def) - apply (drule_tac x=ptr in bspec) - apply (fastforce simp: obj_at_def) - apply (clarsimp simp: obj_at_def obj_at'_def) - done - -lemma threadSet_ekheap_relation: - fixes s :: det_state - assumes etcb_rel: "(\etcb tcb'. etcb_relation etcb tcb' \ etcb_relation etcb (F tcb'))" - shows - "\\s'. ekheap_relation (ekheap s) (ksPSpace s') \ pspace_relation (kheap s) (ksPSpace s') - \ valid_etcbs s\ - threadSet F tcbPtr - \\_ s'. ekheap_relation (ekheap s) (ksPSpace s')\" - supply fun_upd_apply[simp del] - unfolding threadSet_def setObject_def updateObject_default_def - apply (wpsimp wp: getObject_tcb_wp simp: updateObject_default_def) - apply (frule tcb_at'_cross) - apply (fastforce simp: obj_at'_def) - apply normalise_obj_at' - apply (frule (1) tcb_at_is_etcb_at) - apply (clarsimp simp: obj_at_def is_tcb_def is_etcb_at_def) - apply (rename_tac ko, case_tac ko; clarsimp) - apply (rule ekheap_relation_update_concrete_tcb) - apply fastforce - apply fastforce - apply (fastforce simp: obj_at'_def) - apply (frule (1) ekheap_relation_etcb_relation) - apply (fastforce simp: obj_at'_def) - apply (fastforce dest!: etcb_rel) - done - lemma tcbQueued_update_pspace_relation[wp]: fixes s :: det_state shows "threadSet (tcbQueued_update f) tcbPtr \\s'. pspace_relation (kheap s) (ksPSpace s')\" by (wpsimp wp: threadSet_pspace_relation simp: tcb_relation_def) -lemma tcbQueued_update_ekheap_relation[wp]: - fixes s :: det_state - shows - "\\s'. ekheap_relation (ekheap s) (ksPSpace s') \ pspace_relation (kheap s) (ksPSpace s') - \ valid_etcbs s\ - threadSet (tcbQueued_update f) tcbPtr - \\_ s'. ekheap_relation (ekheap s) (ksPSpace s')\" - by (wpsimp wp: threadSet_ekheap_relation simp: etcb_relation_def) - lemma tcbQueueRemove_pspace_relation[wp]: fixes s :: det_state shows "tcbQueueRemove queue tcbPtr \\s'. pspace_relation (kheap s) (ksPSpace s')\" unfolding tcbQueueRemove_def by (wpsimp wp: threadSet_pspace_relation hoare_drop_imps simp: tcb_relation_def) -lemma tcbQueueRemove_ekheap_relation[wp]: - fixes s :: det_state - shows - "\\s'. ekheap_relation (ekheap s) (ksPSpace s') \ pspace_relation (kheap s) (ksPSpace s') - \ valid_etcbs s\ - tcbQueueRemove queue tcbPtr - \\_ s'. ekheap_relation (ekheap s) (ksPSpace s')\" - unfolding tcbQueueRemove_def - by (wpsimp wp: threadSet_ekheap_relation threadSet_pspace_relation hoare_drop_imps - simp: tcb_relation_def etcb_relation_def) - lemma threadSet_ghost_relation[wp]: "threadSet f tcbPtr \\s'. ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') (gsPTTypes (ksArchState s'))\" unfolding threadSet_def setObject_def updateObject_default_def @@ -2178,7 +2052,7 @@ lemma set_tcb_queue_projs: \\s. P (kheap s) (cdt s) (is_original_cap s) (cur_thread s) (idle_thread s) (scheduler_action s) (domain_list s) (domain_index s) (cur_domain s) (domain_time s) (machine_state s) (interrupt_irq_node s) (interrupt_states s) (arch_state s) (caps_of_state s) - (work_units_completed s) (cdt_list s) (ekheap s)\" + (work_units_completed s) (cdt_list s)\" by (wpsimp simp: set_tcb_queue_def) lemma set_tcb_queue_cte_at: @@ -2191,7 +2065,6 @@ lemma set_tcb_queue_cte_at: lemma set_tcb_queue_projs_inv: "fst (set_tcb_queue d p queue s) = {(r, s')} \ kheap s = kheap s' - \ ekheap s = ekheap s' \ cdt s = cdt s' \ is_original_cap s = is_original_cap s' \ cur_thread s = cur_thread s' @@ -2224,51 +2097,18 @@ lemma tcbQueuePrepend_pspace_relation[wp]: unfolding tcbQueuePrepend_def by (wpsimp wp: threadSet_pspace_relation simp: tcb_relation_def) -lemma tcbQueuePrepend_ekheap_relation[wp]: - fixes s :: det_state - shows - "\\s'. ekheap_relation (ekheap s) (ksPSpace s') \ pspace_relation (kheap s) (ksPSpace s') - \ valid_etcbs s\ - tcbQueuePrepend queue tcbPtr - \\_ s'. ekheap_relation (ekheap s) (ksPSpace s')\" - unfolding tcbQueuePrepend_def - by (wpsimp wp: threadSet_pspace_relation threadSet_ekheap_relation - simp: tcb_relation_def etcb_relation_def) - lemma tcbQueueAppend_pspace_relation[wp]: fixes s :: det_state shows "tcbQueueAppend queue tcbPtr \\s'. pspace_relation (kheap s) (ksPSpace s')\" unfolding tcbQueueAppend_def by (wpsimp wp: threadSet_pspace_relation simp: tcb_relation_def) -lemma tcbQueueAppend_ekheap_relation[wp]: - fixes s :: det_state - shows - "\\s'. ekheap_relation (ekheap s) (ksPSpace s') \ pspace_relation (kheap s) (ksPSpace s') - \ valid_etcbs s\ - tcbQueueAppend queue tcbPtr - \\_ s'. ekheap_relation (ekheap s) (ksPSpace s')\" - unfolding tcbQueueAppend_def - by (wpsimp wp: threadSet_pspace_relation threadSet_ekheap_relation - simp: tcb_relation_def etcb_relation_def) - lemma tcbQueueInsert_pspace_relation[wp]: fixes s :: det_state shows "tcbQueueInsert tcbPtr afterPtr \\s'. pspace_relation (kheap s) (ksPSpace s')\" unfolding tcbQueueInsert_def by (wpsimp wp: threadSet_pspace_relation hoare_drop_imps simp: tcb_relation_def) -lemma tcbQueueInsert_ekheap_relation[wp]: - fixes s :: det_state - shows - "\\s'. ekheap_relation (ekheap s) (ksPSpace s') \ pspace_relation (kheap s) (ksPSpace s') - \ valid_etcbs s\ - tcbQueueInsert tcbPtr afterPtr - \\_ s'. ekheap_relation (ekheap s) (ksPSpace s')\" - unfolding tcbQueueInsert_def - by (wpsimp wp: threadSet_pspace_relation threadSet_ekheap_relation hoare_drop_imps - simp: tcb_relation_def etcb_relation_def) - lemma removeFromBitmap_pspace_relation[wp]: fixes s :: det_state shows "removeFromBitmap tdom prio \\s'. pspace_relation (kheap s) (ksPSpace s')\" @@ -2349,22 +2189,22 @@ lemma threadSet_ready_queues_relation: definition in_correct_ready_q_2 where "in_correct_ready_q_2 queues ekh \ \d p. \t \ set (queues d p). is_etcb_at' t ekh - \ etcb_at' (\t. tcb_priority t = p \ tcb_domain t = d) t ekh" + \ etcb_at' (\t. etcb_priority t = p \ etcb_domain t = d) t ekh" -abbreviation in_correct_ready_q :: "det_ext state \ bool" where - "in_correct_ready_q s \ in_correct_ready_q_2 (ready_queues s) (ekheap s)" +abbreviation in_correct_ready_q :: "'z state \ bool" where + "in_correct_ready_q s \ in_correct_ready_q_2 (ready_queues s) (etcbs_of s)" lemmas in_correct_ready_q_def = in_correct_ready_q_2_def lemma in_correct_ready_q_lift: - assumes c: "\P. \\s. P (ekheap s)\ f \\rv s. P (ekheap s)\" + assumes c: "\P. f \\s. P (etcbs_of s)\" assumes r: "\P. f \\s. P (ready_queues s)\" shows "f \in_correct_ready_q\" apply (rule hoare_pre) apply (wps assms | wpsimp)+ done -definition ready_qs_distinct :: "det_ext state \ bool" where +definition ready_qs_distinct :: "'z state \ bool" where "ready_qs_distinct s \ \d p. distinct (ready_queues s d p)" lemma ready_qs_distinct_lift: @@ -2461,28 +2301,6 @@ lemma thread_get_exs_valid[wp]: by (clarsimp simp: thread_get_def get_tcb_def gets_the_def gets_def return_def get_def exs_valid_def tcb_at_def bind_def) -lemma ethread_get_sp: - "\P\ ethread_get f ptr - \\rv. etcb_at (\tcb. f tcb = rv) ptr and P\" - apply wpsimp - apply (clarsimp simp: etcb_at_def split: option.splits) - done - -lemma ethread_get_exs_valid[wp]: - "\tcb_at tcb_ptr s; valid_etcbs s\ \ \(=) s\ ethread_get f tcb_ptr \\\_. (=) s\" - apply (frule (1) tcb_at_is_etcb_at) - apply (clarsimp simp: ethread_get_def get_etcb_def gets_the_def gets_def return_def get_def - is_etcb_at_def exs_valid_def bind_def) - done - -lemma no_fail_ethread_get[wp]: - "no_fail (tcb_at tcb_ptr and valid_etcbs) (ethread_get f tcb_ptr)" - unfolding ethread_get_def - apply wpsimp - apply (frule (1) tcb_at_is_etcb_at) - apply (clarsimp simp: is_etcb_at_def get_etcb_def) - done - lemma threadGet_sp: "\P\ threadGet f ptr \\rv s. \tcb :: tcb. ko_at' tcb ptr s \ f tcb = rv \ P s\" unfolding threadGet_def setObject_def @@ -2509,7 +2327,7 @@ lemma in_ready_q_tcbQueued_eq: lemma tcbSchedEnqueue_corres: "tcb_ptr = tcbPtr \ corres dc - (in_correct_ready_q and ready_qs_distinct and valid_etcbs and st_tcb_at runnable tcb_ptr + (in_correct_ready_q and ready_qs_distinct and st_tcb_at runnable tcb_ptr and pspace_aligned and pspace_distinct) (sym_heap_sched_pointers and valid_sched_pointers and valid_tcbs') (tcb_sched_action tcb_sched_enqueue tcb_ptr) (tcbSchedEnqueue tcbPtr)" @@ -2525,9 +2343,9 @@ lemma tcbSchedEnqueue_corres: apply (fastforce dest: pspace_distinct_cross) apply (clarsimp simp: tcb_sched_action_def tcb_sched_enqueue_def get_tcb_queue_def tcbSchedEnqueue_def getQueue_def unless_def when_def) - apply (rule corres_symb_exec_l[OF _ _ ethread_get_sp]; (solves wpsimp)?) + apply (rule corres_symb_exec_l[OF _ _ thread_get_sp]; (solves wpsimp)?) apply (rename_tac domain) - apply (rule corres_symb_exec_l[OF _ _ ethread_get_sp]; (solves wpsimp)?) + apply (rule corres_symb_exec_l[OF _ _ thread_get_sp]; (solves wpsimp)?) apply (rename_tac priority) apply (rule corres_symb_exec_l[OF _ _ gets_sp]; (solves wpsimp)?) apply (rule corres_stateAssert_ignore) @@ -2539,12 +2357,11 @@ lemma tcbSchedEnqueue_corres: apply (rule corres_symb_exec_r[OF _ threadGet_sp]; (solves wpsimp)?) apply (subst if_distrib[where f="set_tcb_queue domain prio" for domain prio]) apply (rule corres_if_strong') - apply (frule state_relation_ready_queues_relation) - apply (frule in_ready_q_tcbQueued_eq[where t=tcbPtr]) subgoal - by (fastforce dest: tcb_at_ekheap_dom pred_tcb_at_tcb_at - simp: obj_at'_def opt_pred_def opt_map_def obj_at_def is_tcb_def - in_correct_ready_q_def etcb_at_def is_etcb_at_def) + by (fastforce dest!: state_relation_ready_queues_relation + in_ready_q_tcbQueued_eq[where t=tcbPtr] + simp: obj_at'_def opt_pred_def opt_map_def in_correct_ready_q_def + obj_at_def etcb_at_def etcbs_of'_def) apply (find_goal \match conclusion in "corres _ _ _ _ (return ())" \ \-\\) apply (rule monadic_rewrite_corres_l[where P=P and Q=P for P, simplified]) apply (clarsimp simp: set_tcb_queue_def) @@ -2591,19 +2408,18 @@ lemma tcbSchedEnqueue_corres: apply (drule set_tcb_queue_new_state) apply (wpsimp wp: threadSet_wp getObject_tcb_wp simp: setQueue_def tcbQueuePrepend_def) apply normalise_obj_at' - apply (frule (1) tcb_at_is_etcb_at) - apply (clarsimp simp: obj_at_def is_etcb_at_def etcb_at_def) - apply (rename_tac s d p s' tcb' tcb etcb) - apply (frule_tac t=tcbPtr in ekheap_relation_tcb_domain_priority) + apply (clarsimp simp: obj_at_def) + apply (rename_tac s d p s' tcb' tcb) + apply (frule_tac t=tcbPtr in pspace_relation_tcb_domain_priority) apply (force simp: obj_at_def) apply (force simp: obj_at'_def) apply (clarsimp split: if_splits) apply (cut_tac ts="ready_queues s d p" in list_queue_relation_nil) apply (force dest!: spec simp: list_queue_relation_def) - apply (cut_tac ts="ready_queues s (tcb_domain etcb) (tcb_priority etcb)" + apply (cut_tac ts="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" in list_queue_relation_nil) apply (force dest!: spec simp: list_queue_relation_def) - apply (cut_tac ts="ready_queues s (tcb_domain etcb) (tcb_priority etcb)" and s'=s' + apply (cut_tac ts="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" and s'=s' in obj_at'_tcbQueueEnd_ksReadyQueues) apply fast apply auto[1] @@ -2612,14 +2428,14 @@ lemma tcbSchedEnqueue_corres: apply (cut_tac xs="ready_queues s d p" and st="tcbQueueHead (ksReadyQueues s' (d, p))" in heap_path_head') apply (auto dest: spec simp: list_queue_relation_def tcbQueueEmpty_def)[1] - apply (cut_tac xs="ready_queues s (tcb_domain etcb) (tcb_priority etcb)" - and st="tcbQueueHead (ksReadyQueues s' (tcb_domain etcb, tcb_priority etcb))" + apply (cut_tac xs="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" + and st="tcbQueueHead (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb))" in heap_path_head') apply (auto dest: spec simp: list_queue_relation_def tcbQueueEmpty_def)[1] apply (clarsimp simp: list_queue_relation_def) - apply (case_tac "\ (d = tcb_domain etcb \ p = tcb_priority etcb)") - apply (cut_tac d=d and d'="tcb_domain etcb" and p=p and p'="tcb_priority etcb" + apply (case_tac "\ (d = tcb_domain tcb \ p = tcb_priority tcb)") + apply (cut_tac d=d and d'="tcb_domain tcb" and p=p and p'="tcb_priority tcb" in ready_queues_disjoint) apply force apply fastforce @@ -2643,8 +2459,8 @@ lemma tcbSchedEnqueue_corres: apply (clarsimp simp: fun_upd_apply split: if_splits) \ \the ready queue was not originally empty\ - apply (clarsimp simp: etcb_at_def obj_at'_def) - apply (prop_tac "the (tcbQueueHead (ksReadyQueues s' (tcb_domain etcb, tcb_priority etcb))) + apply (clarsimp simp: obj_at'_def) + apply (prop_tac "the (tcbQueueHead (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb))) \ set (ready_queues s d p)") apply (erule orthD2) apply (clarsimp simp: tcbQueueEmpty_def) @@ -2662,7 +2478,7 @@ lemma tcbSchedEnqueue_corres: apply (case_tac "ready_queues s d p"; force simp: tcbQueueEmpty_def) apply (case_tac "t = tcbPtr") apply (clarsimp simp: inQ_def fun_upd_apply obj_at'_def split: if_splits) - apply (case_tac "t = the (tcbQueueHead (ksReadyQueues s' (tcb_domain etcb, tcb_priority etcb)))") + apply (case_tac "t = the (tcbQueueHead (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb)))") apply (clarsimp simp: inQ_def opt_pred_def opt_map_def obj_at'_def fun_upd_apply split: option.splits) apply metis @@ -2670,11 +2486,11 @@ lemma tcbSchedEnqueue_corres: apply (clarsimp simp: fun_upd_apply split: if_splits) apply (clarsimp simp: fun_upd_apply split: if_splits) - \ \d = tcb_domain etcb \ p = tcb_priority etcb\ + \ \d = tcb_domain tcb \ p = tcb_priority tcb\ apply clarsimp - apply (drule_tac x="tcb_domain etcb" in spec) - apply (drule_tac x="tcb_priority etcb" in spec) - apply (cut_tac ts="ready_queues s (tcb_domain etcb) (tcb_priority etcb)" + apply (drule_tac x="tcb_domain tcb" in spec) + apply (drule_tac x="tcb_priority tcb" in spec) + apply (cut_tac ts="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" in tcbQueueHead_iff_tcbQueueEnd) apply (force simp: list_queue_relation_def) apply (frule valid_tcbs'_maxDomain[where t=tcbPtr], simp add: obj_at'_def) @@ -2719,7 +2535,7 @@ lemma setSchedulerAction_corres: apply (simp add: setSchedulerAction_def set_scheduler_action_def) apply (rule corres_no_failI) apply wp - apply (clarsimp simp: in_monad simpler_modify_def state_relation_def) + apply (clarsimp simp: in_monad simpler_modify_def state_relation_def swp_def) done lemma getSchedulerAction_corres: @@ -2730,7 +2546,7 @@ lemma getSchedulerAction_corres: lemma rescheduleRequired_corres: "corres dc - (weak_valid_sched_action and in_correct_ready_q and ready_qs_distinct and valid_etcbs + (weak_valid_sched_action and in_correct_ready_q and ready_qs_distinct and pspace_aligned and pspace_distinct) (sym_heap_sched_pointers and valid_sched_pointers and valid_tcbs') (reschedule_required) rescheduleRequired" @@ -2748,8 +2564,8 @@ lemma rescheduleRequired_corres: apply (rule setSchedulerAction_corres) apply simp apply (wp | wpc | simp)+ - apply (force dest: st_tcb_weakenE simp: in_monad weak_valid_sched_action_def valid_etcbs_def st_tcb_at_def obj_at_def is_tcb - split: Deterministic_A.scheduler_action.split) + apply (force dest: st_tcb_weakenE simp: in_monad weak_valid_sched_action_def st_tcb_at_def obj_at_def is_tcb + split: Structures_A.scheduler_action.split) apply (clarsimp split: scheduler_action.splits) done @@ -2922,8 +2738,8 @@ definition tcb_queue_remove :: "'a \ 'a list \ 'a list" definition tcb_sched_dequeue' :: "obj_ref \ unit det_ext_monad" where "tcb_sched_dequeue' tcb_ptr \ do - d \ ethread_get tcb_domain tcb_ptr; - prio \ ethread_get tcb_priority tcb_ptr; + d \ thread_get tcb_domain tcb_ptr; + prio \ thread_get tcb_priority tcb_ptr; queue \ get_tcb_queue d prio; when (tcb_ptr \ set queue) $ set_tcb_queue d prio (tcb_queue_remove tcb_ptr queue) od" @@ -2941,7 +2757,7 @@ lemma filter_tcb_queue_remove: done lemma tcb_sched_dequeue_monadic_rewrite: - "monadic_rewrite False True (is_etcb_at t and (\s. \d p. distinct (ready_queues s d p))) + "monadic_rewrite False True (tcb_at t and (\s. \d p. distinct (ready_queues s d p))) (tcb_sched_action tcb_sched_dequeue t) (tcb_sched_dequeue' t)" supply if_split[split del] apply (clarsimp simp: tcb_sched_dequeue'_def tcb_sched_dequeue_def tcb_sched_action_def @@ -2954,9 +2770,9 @@ lemma tcb_sched_dequeue_monadic_rewrite: apply (metis (mono_tags, lifting) filter_cong) apply (rule monadic_rewrite_modify_noop) apply (wpsimp wp: thread_get_wp)+ - apply (clarsimp simp: etcb_at_def split: option.splits) - apply (prop_tac "(\d' p. if d' = tcb_domain x2 \ p = tcb_priority x2 - then filter (\x. x \ t) (ready_queues s (tcb_domain x2) (tcb_priority x2)) + apply (clarsimp simp: tcb_at_def) + apply (prop_tac "(\d' p. if d' = tcb_domain tcb \ p = tcb_priority tcb + then filter ((\) t) (ready_queues s (tcb_domain tcb) (tcb_priority tcb)) else ready_queues s d' p) = ready_queues s") apply (subst filter_True) @@ -2989,7 +2805,7 @@ lemma in_queue_not_head_or_not_tail_length_gt_1: lemma tcbSchedDequeue_corres: "tcb_ptr = tcbPtr \ corres dc - (in_correct_ready_q and ready_qs_distinct and valid_etcbs and tcb_at tcb_ptr + (in_correct_ready_q and ready_qs_distinct and tcb_at tcb_ptr and pspace_aligned and pspace_distinct) (sym_heap_sched_pointers and valid_objs') (tcb_sched_action tcb_sched_dequeue tcb_ptr) (tcbSchedDequeue tcbPtr)" @@ -3003,22 +2819,22 @@ lemma tcbSchedDequeue_corres: apply (fastforce dest: pspace_distinct_cross) apply (rule monadic_rewrite_corres_l[where P=P and Q=P for P, simplified]) apply (rule monadic_rewrite_guard_imp[OF tcb_sched_dequeue_monadic_rewrite]) - apply (fastforce dest: tcb_at_is_etcb_at simp: in_correct_ready_q_def ready_qs_distinct_def) + apply (fastforce simp: in_correct_ready_q_def ready_qs_distinct_def) apply (clarsimp simp: tcb_sched_dequeue'_def get_tcb_queue_def tcbSchedDequeue_def getQueue_def unless_def when_def) - apply (rule corres_symb_exec_l[OF _ _ ethread_get_sp]; wpsimp?) + apply (rule corres_symb_exec_l[OF _ _ thread_get_sp]; wpsimp?) apply (rename_tac dom) - apply (rule corres_symb_exec_l[OF _ _ ethread_get_sp]; wpsimp?) + apply (rule corres_symb_exec_l[OF _ _ thread_get_sp]; wpsimp?) apply (rename_tac prio) apply (rule corres_symb_exec_l[OF _ _ gets_sp]; (solves wpsimp)?) apply (rule corres_stateAssert_ignore) apply (fastforce intro: ksReadyQueues_asrt_cross) apply (rule corres_symb_exec_r[OF _ threadGet_sp]; (solves wpsimp)?) apply (rule corres_if_strong'; fastforce?) - apply (frule state_relation_ready_queues_relation) - apply (frule in_ready_q_tcbQueued_eq[where t=tcbPtr]) - apply (fastforce simp: obj_at'_def opt_pred_def opt_map_def obj_at_def is_tcb_def - in_correct_ready_q_def etcb_at_def is_etcb_at_def) + apply (fastforce dest!: state_relation_ready_queues_relation + in_ready_q_tcbQueued_eq[where t=tcbPtr] + simp: obj_at'_def opt_pred_def opt_map_def in_correct_ready_q_def + obj_at_def etcb_at_def etcbs_of'_def) apply (rule corres_symb_exec_r[OF _ threadGet_sp]; wpsimp?) apply (rule corres_symb_exec_r[OF _ threadGet_sp]; wpsimp?) apply (rule corres_symb_exec_r[OF _ gets_sp]; wpsimp?) @@ -3040,24 +2856,23 @@ lemma tcbSchedDequeue_corres: apply (wpsimp wp: threadSet_wp getObject_tcb_wp simp: setQueue_def tcbQueueRemove_def split_del: if_split) - apply (frule (1) tcb_at_is_etcb_at) - apply (clarsimp simp: obj_at_def is_etcb_at_def etcb_at_def) + apply (clarsimp simp: obj_at_def) apply normalise_obj_at' - apply (rename_tac s d p s' tcb' tcb etcb) - apply (frule_tac t=tcbPtr in ekheap_relation_tcb_domain_priority) + apply (rename_tac s d p s' tcb' tcb) + apply (frule_tac t=tcbPtr in pspace_relation_tcb_domain_priority) apply (force simp: obj_at_def) apply (force simp: obj_at'_def) - apply (case_tac "d \ tcb_domain etcb \ p \ tcb_priority etcb") + apply (case_tac "d \ tcb_domain tcb \ p \ tcb_priority tcb") apply clarsimp - apply (cut_tac p=tcbPtr and ls="ready_queues s (tcb_domain etcb) (tcb_priority etcb)" + apply (cut_tac p=tcbPtr and ls="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" in list_queue_relation_neighbour_in_set) apply (fastforce dest!: spec) apply fastforce apply fastforce apply (cut_tac xs="ready_queues s d p" in heap_path_head') apply (force dest!: spec simp: ready_queues_relation_def Let_def list_queue_relation_def) - apply (cut_tac d=d and d'="tcb_domain etcb" and p=p and p'="tcb_priority etcb" + apply (cut_tac d=d and d'="tcb_domain tcb" and p=p and p'="tcb_priority tcb" in ready_queues_disjoint) apply force apply fastforce @@ -3081,7 +2896,7 @@ lemma tcbSchedDequeue_corres: apply (clarsimp simp: fun_upd_apply) apply (clarsimp simp: fun_upd_apply) - apply (clarsimp simp: etcb_at_def obj_at'_def) + apply (clarsimp simp: obj_at'_def) apply (intro conjI; clarsimp) \ \tcbPtr is the head of the ready queue\ @@ -3127,8 +2942,8 @@ lemma tcbSchedDequeue_corres: \ \d = tcb_domain tcb \ p = tcb_priority tcb\ apply clarsimp - apply (drule_tac x="tcb_domain etcb" in spec) - apply (drule_tac x="tcb_priority etcb" in spec) + apply (drule_tac x="tcb_domain tcb" in spec) + apply (drule_tac x="tcb_priority tcb" in spec) apply (clarsimp simp: list_queue_relation_def) apply (frule heap_path_head') apply (frule heap_ls_distinct) @@ -3141,7 +2956,7 @@ lemma tcbSchedDequeue_corres: apply (simp add: fun_upd_apply tcb_queue_remove_def queue_end_valid_def heap_ls_unique heap_path_last_end) apply (simp add: fun_upd_apply prev_queue_head_def) - apply (case_tac "ready_queues s (tcb_domain etcb) (tcb_priority etcb)"; + apply (case_tac "ready_queues s (tcb_domain tcb) (tcb_priority tcb)"; clarsimp simp: tcb_queue_remove_def inQ_def opt_pred_def fun_upd_apply) apply (intro conjI; clarsimp) @@ -3160,7 +2975,7 @@ lemma tcbSchedDequeue_corres: apply (clarsimp simp: opt_map_red opt_map_upd_triv fun_upd_apply) apply (clarsimp simp: queue_end_valid_def fun_upd_apply last_tl) apply (clarsimp simp: prev_queue_head_def fun_upd_apply) - apply (case_tac "ready_queues s (tcb_domain etcb) (tcb_priority etcb)"; + apply (case_tac "ready_queues s (tcb_domain tcb) (tcb_priority tcb)"; clarsimp simp: inQ_def opt_pred_def opt_map_def fun_upd_apply split: option.splits) apply (intro conjI; clarsimp) @@ -3239,11 +3054,11 @@ lemma setThreadState_corres: (set_thread_state t ts) (setThreadState ts' t)" (is "?tsr \ corres dc ?Pre ?Pre' ?sts ?sts'") apply (simp add: set_thread_state_def setThreadState_def) - apply (simp add: set_thread_state_ext_def[abs_def]) + apply (simp add: set_thread_state_act_def[abs_def]) apply (subst bind_assoc[symmetric], subst thread_set_def[simplified, symmetric]) apply (rule corres_guard_imp) apply (rule corres_split[where r'=dc]) - apply (rule threadset_corres, (simp add: tcb_relation_def exst_same_def)+) + apply (rule threadset_corres, (simp add: tcb_relation_def inQ_def)+) apply (subst thread_get_test[where test="runnable"]) apply (rule corres_split[OF thread_get_isRunnable_corres]) apply (rule corres_split[OF getCurThread_corres]) @@ -3264,7 +3079,7 @@ lemma setBoundNotification_corres: (set_bound_notification t ntfn) (setBoundNotification ntfn t)" apply (simp add: set_bound_notification_def setBoundNotification_def) apply (subst thread_set_def[simplified, symmetric]) - apply (rule threadset_corres, simp_all add:tcb_relation_def exst_same_def) + apply (rule threadset_corres, simp_all add:tcb_relation_def inQ_def) done crunch rescheduleRequired, tcbSchedDequeue, setThreadState, setBoundNotification @@ -5972,154 +5787,6 @@ lemma asUser_irq_handlers': apply (wpsimp wp: threadSet_irq_handlers' [OF all_tcbI, OF ball_tcb_cte_casesI] select_f_inv) done -(* the brave can try to move this up to near setObject_update_TCB_corres' *) - -definition non_exst_same :: "Structures_H.tcb \ Structures_H.tcb \ bool" -where - "non_exst_same tcb tcb' \ \d p ts. tcb' = tcb\tcbDomain := d, tcbPriority := p, tcbTimeSlice := ts\" - -fun non_exst_same' :: "Structures_H.kernel_object \ Structures_H.kernel_object \ bool" -where - "non_exst_same' (KOTCB tcb) (KOTCB tcb') = non_exst_same tcb tcb'" | - "non_exst_same' _ _ = True" - -lemma non_exst_same_prio_upd[simp]: - "non_exst_same tcb (tcbPriority_update f tcb)" - by (cases tcb, simp add: non_exst_same_def) - -lemma non_exst_same_timeSlice_upd[simp]: - "non_exst_same tcb (tcbTimeSlice_update f tcb)" - by (cases tcb, simp add: non_exst_same_def) - -lemma non_exst_same_domain_upd[simp]: - "non_exst_same tcb (tcbDomain_update f tcb)" - by (cases tcb, simp add: non_exst_same_def) - -lemma set_eobject_corres': - assumes e: "etcb_relation etcb tcb'" - assumes z: "\s. obj_at' P ptr s - \ map_to_ctes ((ksPSpace s) (ptr \ KOTCB tcb')) = map_to_ctes (ksPSpace s)" - shows - "corres dc - (tcb_at ptr and is_etcb_at ptr) - (obj_at' (\ko. non_exst_same ko tcb') ptr and obj_at' P ptr - and obj_at' (\tcb. (tcbDomain tcb \ tcbDomain tcb' \ tcbPriority tcb \ tcbPriority tcb') - \ \ tcbQueued tcb) ptr) - (set_eobject ptr etcb) (setObject ptr tcb')" - apply (rule corres_no_failI) - apply (rule no_fail_pre) - apply wp - apply (clarsimp simp: obj_at'_def) - apply (unfold set_eobject_def setObject_def) - apply (clarsimp simp: in_monad split_def bind_def gets_def get_def Bex_def - put_def return_def modify_def get_object_def - updateObject_default_def in_magnitude_check objBits_simps') - apply (clarsimp simp add: state_relation_def z) - apply (clarsimp simp add: obj_at_def is_etcb_at_def) - apply (simp only: pspace_relation_def dom_fun_upd2 simp_thms) - apply (elim conjE) - apply (frule bspec, erule domI) - apply (rule conjI) - apply (rule ballI, drule(1) bspec) - apply (drule domD) - apply (clarsimp simp: is_other_obj_relation_type) - apply (drule(1) bspec) - apply (clarsimp simp: non_exst_same_def) - apply (case_tac bb; simp) - apply (clarsimp simp: obj_at'_def other_obj_relation_def tcb_relation_cut_def - cte_relation_def tcb_relation_def - split: if_split_asm)+ - apply (clarsimp simp: aobj_relation_cuts_def split: AARCH64_A.arch_kernel_obj.splits) - apply (rename_tac arch_kernel_obj obj d p ts) - apply (case_tac arch_kernel_obj; simp) - apply (clarsimp simp: pte_relation_def is_tcb_def - split: if_split_asm)+ - apply (extract_conjunct \match conclusion in "ekheap_relation _ _" \ -\) - apply (simp only: ekheap_relation_def dom_fun_upd2 simp_thms) - apply (frule bspec, erule domI) - apply (rule ballI, drule(1) bspec) - apply (drule domD) - apply (clarsimp simp: obj_at'_def) - apply (insert e) - apply (clarsimp simp: other_obj_relation_def etcb_relation_def is_other_obj_relation_type - split: Structures_A.kernel_object.splits kernel_object.splits arch_kernel_obj.splits) - apply (frule in_ready_q_tcbQueued_eq[where t=ptr]) - apply (rename_tac s' conctcb' abstcb exttcb) - apply (clarsimp simp: ready_queues_relation_def Let_def) - apply (prop_tac "(tcbSchedNexts_of s')(ptr := tcbSchedNext tcb') = tcbSchedNexts_of s'") - apply (fastforce simp: opt_map_def obj_at'_def non_exst_same_def split: option.splits) - apply (prop_tac "(tcbSchedPrevs_of s')(ptr := tcbSchedPrev tcb') = tcbSchedPrevs_of s'") - apply (fastforce simp: opt_map_def obj_at'_def non_exst_same_def split: option.splits) - apply (clarsimp simp: ready_queue_relation_def opt_map_def opt_pred_def obj_at'_def inQ_def - non_exst_same_def - split: option.splits) - apply metis - done - -lemma set_eobject_corres: - assumes tcbs: "non_exst_same tcb' tcbu'" - assumes e: "etcb_relation etcb tcb' \ etcb_relation etcbu tcbu'" - assumes tables': "\(getF, v) \ ran tcb_cte_cases. getF tcbu' = getF tcb'" - assumes r: "r () ()" - shows - "corres r - (tcb_at add and (\s. ekheap s add = Some etcb)) - (ko_at' tcb' add - and obj_at' (\tcb. (tcbDomain tcb \ tcbDomain tcbu' \ tcbPriority tcb \ tcbPriority tcbu') - \ \ tcbQueued tcb) add) - (set_eobject add etcbu) (setObject add tcbu')" - apply (rule_tac F="non_exst_same tcb' tcbu' \ etcb_relation etcbu tcbu'" in corres_req) - apply (clarsimp simp: state_relation_def obj_at_def obj_at'_def) - apply (frule(1) pspace_relation_absD) - apply (clarsimp simp: other_obj_relation_def ekheap_relation_def e tcbs) - apply (drule bspec, erule domI) - apply (clarsimp simp: e) - apply (erule conjE) - apply (rule corres_guard_imp) - apply (rule corres_rel_imp) - apply (rule set_eobject_corres'[where P="(=) tcb'"]) - apply simp - defer - apply (simp add: r) - apply (fastforce simp: is_etcb_at_def elim!: obj_at_weakenE) - apply (subst(asm) eq_commute) - apply (clarsimp simp: obj_at'_def) - apply (clarsimp simp: obj_at'_def objBits_simps) - apply (subst map_to_ctes_upd_tcb, assumption+) - apply (simp add: ps_clear_def3 field_simps objBits_defs mask_def) - apply (subst if_not_P) - apply (fastforce dest: bspec [OF tables', OF ranI]) - apply simp - done - -lemma ethread_set_corresT: - assumes x: "\tcb'. non_exst_same tcb' (f' tcb')" - assumes z: "\tcb. \(getF, setF) \ ran tcb_cte_cases. getF (f' tcb) = getF tcb" - assumes e: "\etcb tcb'. etcb_relation etcb tcb' \ etcb_relation (f etcb) (f' tcb')" - shows - "corres dc - (tcb_at t and valid_etcbs) - (tcb_at' t - and obj_at' (\tcb. (tcbDomain tcb \ tcbDomain (f' tcb) - \ tcbPriority tcb \ tcbPriority (f' tcb)) - \ \ tcbQueued tcb) t) - (ethread_set f t) (threadSet f' t)" - apply (simp add: ethread_set_def threadSet_def bind_assoc) - apply (rule corres_guard_imp) - apply (rule corres_split[OF corres_get_etcb set_eobject_corres]) - apply (rule x) - apply (erule e) - apply (simp add: z)+ - apply (wp getObject_tcb_wp)+ - apply clarsimp - apply (simp add: valid_etcbs_def tcb_at_st_tcb_at[symmetric]) - apply (force simp: tcb_at_def get_etcb_def obj_at_def) - apply (clarsimp simp: obj_at'_def) - done - -lemmas ethread_set_corres = - ethread_set_corresT [OF _ all_tcbI, OF _ ball_tcb_cte_casesI] - lemma archTcbUpdate_aux2: "(\tcb. tcb\ tcbArch := f (tcbArch tcb)\) = tcbArch_update f" by (rule ext, case_tac tcb, simp) diff --git a/proof/refine/AARCH64/Tcb_R.thy b/proof/refine/AARCH64/Tcb_R.thy index d303b7c184..6d6d4411ba 100644 --- a/proof/refine/AARCH64/Tcb_R.thy +++ b/proof/refine/AARCH64/Tcb_R.thy @@ -220,7 +220,7 @@ lemma restart_corres: apply (clarsimp simp: invs'_def valid_state'_def sch_act_wf_weak valid_pspace'_def valid_tcb_state'_def) apply wp+ - apply (simp add: valid_sched_def invs_def tcb_at_is_etcb_at invs_psp_aligned invs_distinct) + apply (simp add: valid_sched_def invs_def invs_psp_aligned invs_distinct) apply clarsimp done @@ -341,7 +341,7 @@ lemma invokeTCB_WriteRegisters_corres: apply simp apply (wp+)[2] apply ((wp hoare_weak_lift_imp restart_invs' - | strengthen valid_sched_weak_strg einvs_valid_etcbs + | strengthen valid_sched_weak_strg invs_weak_sch_act_wf valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct valid_sched_valid_queues valid_objs'_valid_tcbs' invs_valid_objs' @@ -583,9 +583,63 @@ crunch tcbSchedDequeue crunch tcbSchedDequeue for st_tcb_at'[wp]: "\s. P (st_tcb_at' st tcbPtr s)" +lemma thread_set_ready_qs_distinct[wp]: + "thread_set f tcb_ptr \ready_qs_distinct\" + apply (wpsimp wp: thread_set_wp) + by (clarsimp simp: ready_qs_distinct_def) + +lemma thread_set_in_correct_ready_q_not_queued: + "\in_correct_ready_q and not_queued t\ + thread_set f t + \\_. in_correct_ready_q\" + unfolding thread_set_priority_def + apply (wpsimp wp: thread_set_wp) + apply (clarsimp simp: in_correct_ready_q_def not_queued_def is_etcb_at'_def etcb_at_def etcbs_of'_def) + done + +lemma tcb_sched_dequeue_in_correct_ready_q[wp]: + "tcb_sched_action tcb_sched_dequeue t \in_correct_ready_q\ " + unfolding tcb_sched_action_def set_tcb_queue_def + apply (wpsimp wp: thread_get_wp') + apply (clarsimp simp: in_correct_ready_q_def tcb_sched_dequeue_def) + done + +lemma tcb_sched_dequeue_ready_qs_distinct[wp]: + "tcb_sched_action tcb_sched_dequeue t \ready_qs_distinct\ " + unfolding tcb_sched_action_def set_tcb_queue_def + apply (wpsimp wp: thread_get_wp') + apply (clarsimp simp: ready_qs_distinct_def tcb_sched_dequeue_def) + done + +\ \For updating the domain and the priority fields of a TCB that is not in a ready queue\ +lemma threadSet_not_queued_corres: + "\\tcb tcb'. tcb_relation tcb tcb' \ tcb_relation (f tcb) (F tcb'); + \tcb'. tcbSchedNext (F tcb') = tcbSchedNext tcb'; + \tcb'. tcbSchedPrev (F tcb') = tcbSchedPrev tcb'; + \tcb'. tcbQueued (F tcb') = tcbQueued tcb'; + \tcb. \(getF, v) \ ran tcb_cap_cases. getF (f tcb) = getF tcb; + \tcb'. \(getF, v)\ran tcb_cte_cases. getF (F tcb') = getF tcb'\ + \ corres dc (tcb_at t and not_queued t and pspace_aligned and pspace_distinct) \ + (thread_set f t) (threadSet F t)" + apply (rule_tac Q'="tcb_at' t" in corres_cross_add_guard) + apply (fastforce dest!: state_relationD elim!: tcb_at_cross) + apply (simp add: thread_set_def threadSet_def) + apply (rule corres_symb_exec_l[OF _ _ gets_the_sp]; wpsimp simp: tcb_at_def) + apply (rule corres_symb_exec_r[OF _ getObject_tcb_sp]; wpsimp?) + apply (rename_tac tcb tcb') + apply (rule stronger_corres_guard_imp) + apply (rule_tac F="\ tcbQueued tcb'" in corres_gen_asm) + apply (rule_tac tcb=tcb and tcb'=tcb' in setObject_update_TCB_corres'; + fastforce simp: inQ_def) + apply (frule state_relation_ready_queues_relation) + apply (frule in_ready_q_tcbQueued_eq[where t=t]) + apply (clarsimp simp: opt_pred_def opt_map_def obj_at'_def not_queued_def) + apply clarsimp + done + lemma sp_corres2: "corres dc - (valid_etcbs and weak_valid_sched_action and cur_tcb and tcb_at t + (weak_valid_sched_action and cur_tcb and tcb_at t and valid_queues and pspace_aligned and pspace_distinct) (tcb_at' t and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\_. x \ maxPriority) and sym_heap_sched_pointers and valid_sched_pointers) @@ -593,8 +647,9 @@ lemma sp_corres2: apply (simp add: setPriority_def set_priority_def thread_set_priority_def) apply (rule stronger_corres_guard_imp) apply (rule corres_split[OF tcbSchedDequeue_corres], simp) - apply (rule corres_split[OF ethread_set_corres], simp_all)[1] - apply (simp add: etcb_relation_def) + apply (rule corres_split[OF threadSet_not_queued_corres]; + simp add: tcb_relation_def tcb_cap_cases_def tcb_cte_cases_def + cteSizeBits_def) apply (rule corres_split[OF isRunnable_corres]) apply (erule corres_when) apply(rule corres_split[OF getCurThread_corres]) @@ -604,19 +659,19 @@ lemma sp_corres2: apply ((clarsimp | wp hoare_weak_lift_imp hoare_vcg_if_lift hoare_wp_combs gts_wp isRunnable_wp)+)[4] - apply (wp hoare_vcg_imp_lift' hoare_vcg_if_lift hoare_vcg_all_lift - ethread_set_not_queued_valid_queues - | strengthen valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct)+ + apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_if_lift hoare_vcg_all_lift + thread_set_in_correct_ready_q_not_queued thread_set_no_change_tcb_state + thread_set_no_change_tcb_state_converse thread_set_weak_valid_sched_action)+ apply ((wp hoare_vcg_imp_lift' hoare_vcg_all_lift isRunnable_wp threadSet_pred_tcb_no_state threadSet_valid_objs_tcbPriority_update threadSet_sched_pointers threadSet_valid_sched_pointers tcb_dequeue_not_queued tcbSchedDequeue_not_queued threadSet_weak_sch_act_wf - | simp add: etcb_relation_def + | simp add: tcb_relation_def | strengthen valid_objs'_valid_tcbs' obj_at'_weakenE[where P="Not \ tcbQueued"] | wps)+) - apply (force simp: valid_etcbs_def tcb_at_st_tcb_at[symmetric] state_relation_def + apply (force simp: tcb_at_st_tcb_at[symmetric] state_relation_def dest: pspace_relation_tcb_at intro: st_tcb_at_opeqI) apply clarsimp done @@ -639,7 +694,7 @@ lemma setMCPriority_corres: apply (clarsimp simp: setMCPriority_def set_mcpriority_def) apply (rule threadset_corresT) by (clarsimp simp: tcb_relation_def tcb_cap_cases_tcb_mcpriority - tcb_cte_cases_def cteSizeBits_def exst_same_def)+ + tcb_cte_cases_def cteSizeBits_def inQ_def)+ definition "out_rel fn fn' v v' \ @@ -653,8 +708,7 @@ lemma out_corresT: assumes y: "\v. \tcb. \(getF, setF)\ran tcb_cte_cases. getF (fn' v tcb) = getF tcb" assumes sched_pointers: "\tcb v. tcbSchedPrev (fn' v tcb) = tcbSchedPrev tcb" "\tcb v. tcbSchedNext (fn' v tcb) = tcbSchedNext tcb" - assumes flag: "\tcb v. tcbQueued (fn' v tcb) = tcbQueued tcb" - assumes e: "\tcb v. exst_same tcb (fn' v tcb)" + assumes flag: "\d p tcb' v. inQ d p (fn' v tcb') = inQ d p tcb'" shows "out_rel fn fn' v v' \ corres dc (tcb_at t and pspace_aligned and pspace_distinct) @@ -662,7 +716,7 @@ lemma out_corresT: (option_update_thread t fn v) (case_option (return ()) (\x. threadSet (fn' x) t) v')" apply (case_tac v, simp_all add: out_rel_def option_update_thread_def) - apply (clarsimp simp: threadset_corresT [OF _ x y sched_pointers flag e]) + apply (clarsimp simp: threadset_corresT [OF _ x y sched_pointers flag]) done lemmas out_corres = out_corresT [OF _ all_tcbI, OF ball_tcb_cap_casesI ball_tcb_cte_casesI] @@ -990,14 +1044,14 @@ lemma thread_set_ipc_weak_valid_sched_action: apply (simp | intro impI | elim exE conjE)+ apply (frule get_tcb_SomeD) apply (erule ssubst) - apply (clarsimp simp add: weak_valid_sched_action_def valid_etcbs_2_def st_tcb_at_kh_def - get_tcb_def obj_at_kh_def obj_at_def is_etcb_at'_def valid_sched_def valid_sched_action_def) + apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_kh_def obj_at_kh_def valid_sched_def + valid_sched_action_def) done lemma threadcontrol_corres_helper3: "\einvs and simple_sched_action\ check_cap_at cap p (check_cap_at (cap.ThreadCap cap') slot (cap_insert cap p (t, tcb_cnode_index 4))) - \\_ s. weak_valid_sched_action s \ in_correct_ready_q s \ ready_qs_distinct s \ valid_etcbs s + \\_ s. weak_valid_sched_action s \ in_correct_ready_q s \ ready_qs_distinct s \ pspace_aligned s \ pspace_distinct s\" apply (wpsimp | strengthen valid_sched_valid_queues valid_queues_in_correct_ready_q @@ -1177,7 +1231,7 @@ proof - (option_map to_bl v)) (case v of None \ return () | Some x \ threadSet (tcbFaultHandler_update (%_. x)) t)" - apply (rule out_corres, simp_all add: exst_same_def) + apply (rule out_corres, simp_all add: inQ_def) apply (case_tac v, simp_all add: out_rel_def) apply (safe, case_tac tcb', simp add: tcb_relation_def split: option.split) done @@ -1187,7 +1241,7 @@ proof - (option_update_thread t (tcb_ipc_buffer_update o (%x _. x)) v) (case v of None \ return () | Some x \ threadSet (tcbIPCBuffer_update (%_. x)) t)" - apply (rule out_corres, simp_all add: exst_same_def) + apply (rule out_corres, simp_all ) apply (case_tac v, simp_all add: out_rel_def) apply (safe, case_tac tcb', simp add: tcb_relation_def) done @@ -1316,20 +1370,19 @@ proof - apply (rule cteDelete_corres) apply (rule_tac F="is_aligned aa msg_align_bits" in corres_gen_asm2) apply (rule corres_split_nor) - apply (rule threadset_corres, - (simp add: tcb_relation_def), (simp add: exst_same_def)+)[1] + apply (rule threadset_corres; simp add: tcb_relation_def) apply (rule corres_split[OF getCurThread_corres], clarsimp) apply (rule corres_when[OF refl rescheduleRequired_corres]) apply (wpsimp wp: gct_wp)+ apply (strengthen valid_queues_ready_qs_distinct) apply (wpsimp wp: thread_set_ipc_weak_valid_sched_action thread_set_valid_queues - hoare_drop_imp) + hoare_drop_imp in_correct_ready_q_lift thread_set_etcbs) apply clarsimp apply (strengthen valid_objs'_valid_tcbs' invs_valid_objs')+ apply (wpsimp wp: threadSet_sched_pointers threadSet_valid_sched_pointers hoare_drop_imp threadSet_invs_tcbIPCBuffer_update) apply (clarsimp simp: pred_conj_def) - apply (strengthen einvs_valid_etcbs valid_queues_in_correct_ready_q + apply (strengthen valid_queues_in_correct_ready_q valid_sched_valid_queues)+ apply wp apply (clarsimp simp: pred_conj_def) @@ -1345,8 +1398,7 @@ proof - in corres_gen_asm) apply (rule_tac F="isArchObjectCap ac" in corres_gen_asm2) apply (rule corres_split_nor) - apply (rule threadset_corres, - simp add: tcb_relation_def, (simp add: exst_same_def)+) + apply (rule threadset_corres; simp add: tcb_relation_def) apply (rule corres_split) apply (erule checkCapAt_cteInsert_corres) apply (rule corres_split[OF getCurThread_corres], clarsimp) @@ -1724,7 +1776,7 @@ lemma invokeTCB_corres: apply (rule TcbAcc_R.rescheduleRequired_corres) apply (rule corres_trivial, simp) apply (wpsimp wp: hoare_drop_imp)+ - apply (fastforce dest: valid_sched_valid_queues simp: valid_sched_weak_strg einvs_valid_etcbs) + apply (fastforce dest: valid_sched_valid_queues simp: valid_sched_weak_strg) apply fastforce done @@ -1950,7 +2002,7 @@ lemma decodeSetPriority_corres: "\ cap_relation cap cap'; is_thread_cap cap; list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras' \ \ corres (ser \ tcbinv_relation) - (cur_tcb and valid_etcbs and (pspace_aligned and pspace_distinct and (\s. \x \ set extras. s \ (fst x)))) + (cur_tcb and (pspace_aligned and pspace_distinct and (\s. \x \ set extras. s \ (fst x)))) (invs' and (\s. \x \ set extras'. s \' (fst x))) (decode_set_priority args cap slot extras) (decodeSetPriority args cap' extras')" @@ -1968,7 +2020,7 @@ lemma decodeSetMCPriority_corres: "\ cap_relation cap cap'; is_thread_cap cap; list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras' \ \ corres (ser \ tcbinv_relation) - (cur_tcb and valid_etcbs and (pspace_aligned and pspace_distinct and (\s. \x \ set extras. s \ (fst x)))) + (cur_tcb and (pspace_aligned and pspace_distinct and (\s. \x \ set extras. s \ (fst x)))) (invs' and (\s. \x \ set extras'. s \' (fst x))) (decode_set_mcpriority args cap slot extras) (decodeSetMCPriority args cap' extras')" @@ -2074,7 +2126,7 @@ lemma decodeSetSchedParams_corres: "\ cap_relation cap cap'; is_thread_cap cap; list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras' \ \ corres (ser \ tcbinv_relation) - (cur_tcb and valid_etcbs and + (cur_tcb and (pspace_aligned and pspace_distinct and (\s. \x \ set extras. s \ (fst x)))) (invs' and (\s. \x \ set extras'. s \' (fst x))) (decode_set_sched_params args cap slot extras) diff --git a/proof/refine/AARCH64/Untyped_R.thy b/proof/refine/AARCH64/Untyped_R.thy index d9966e08cf..157a14ec38 100644 --- a/proof/refine/AARCH64/Untyped_R.thy +++ b/proof/refine/AARCH64/Untyped_R.thy @@ -1316,7 +1316,7 @@ lemma in_getCTE2: declare wrap_ext_op_det_ext_ext_def[simp] lemma do_ext_op_update_cdt_list_symb_exec_l': - "corres_underlying {(s::det_state, s'). f (kheap s) (ekheap s) s'} nf nf' dc P P' (create_cap_ext p z a) (return x)" + "corres_underlying {(s::det_state, s'). f (kheap s) s'} nf nf' dc P P' (create_cap_ext p z a) (return x)" apply (simp add: corres_underlying_def create_cap_ext_def update_cdt_list_def set_cdt_list_def bind_def put_def get_def gets_def return_def) done @@ -1357,15 +1357,14 @@ lemma set_cdt_symb_exec_l: "corres_underlying {(s, s'). f (kheap s) (exst s) s'} nf nf' dc P P' (set_cdt g) (return x)" by (simp add: corres_underlying_def return_def set_cdt_def in_monad Bex_def) -crunch create_cap_ext - for domain_index[wp]: "\s. P (domain_index s)" crunch create_cap_ext for work_units_completed[wp]: "\s. P (work_units_completed s)" + (ignore_del: create_cap_ext) context begin interpretation Arch . (*FIXME: arch-split*) lemma updateNewFreeIndex_noop_psp_corres: - "corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False True + "corres_underlying {(s, s'). pspace_relation (kheap s) (ksPSpace s')} False True dc \ (cte_at' slot) (return ()) (updateNewFreeIndex slot)" apply (simp add: updateNewFreeIndex_def) @@ -1377,6 +1376,10 @@ lemma updateNewFreeIndex_noop_psp_corres: | simp add: updateTrackedFreeIndex_def getSlotCap_def)+ done +crunch set_cap, set_cdt + for domain_index[wp]: "\s. P (domain_index s)" + (wp: crunch_wps) + crunch updateMDB, updateNewFreeIndex, setCTE for rdyq_projs[wp]: "\s. P (ksReadyQueues s) (tcbSchedNexts_of s) (tcbSchedPrevs_of s) (\d p. inQ d p |< tcbs_of' s)" @@ -2981,35 +2984,31 @@ lemma createNewCaps_range_helper: apply (frule range_cover.range_cover_n_less) apply (frule range_cover.unat_of_nat_n) apply (cases tp, simp_all split del: if_split) - apply (rename_tac apiobject_type) - apply (case_tac apiobject_type, simp_all split del: if_split) - apply (rule hoare_pre, wp) - apply (frule range_cover_not_zero[rotated -1],simp) - apply (clarsimp simp: APIType_capBits_def objBits_simps ptr_add_def o_def) - apply (subst upto_enum_red') - apply unat_arith - apply (clarsimp simp: o_def fromIntegral_def toInteger_nat fromInteger_nat) - apply fastforce - apply (rule hoare_pre,wp createObjects_ret2) - apply (clarsimp simp: APIType_capBits_def word_bits_def bit_simps - objBits_simps ptr_add_def o_def) - apply (fastforce simp: objBitsKO_def objBits_def) - apply (rule hoare_pre,wp createObjects_ret2) - apply (clarsimp simp: APIType_capBits_def word_bits_def - objBits_simps ptr_add_def o_def) - apply (fastforce simp: objBitsKO_def objBits_def) - apply (rule hoare_pre,wp createObjects_ret2) - apply (clarsimp simp: APIType_capBits_def word_bits_def objBits_simps ptr_add_def o_def) - apply (fastforce simp: objBitsKO_def objBits_def) - apply (rule hoare_pre,wp createObjects_ret2) - apply (clarsimp simp: APIType_capBits_def word_bits_def objBits_simps ptr_add_def o_def) - apply (fastforce simp: objBitsKO_def objBits_def) - apply (wp createObjects_ret2 - | clarsimp simp: APIType_capBits_def objBits_if_dev archObjSize_def word_bits_def - split del: if_split - | simp add: objBits_simps - | (rule exI, (fastforce simp: bit_simps)))+ - done + apply (rename_tac apiobject_type) + apply (case_tac apiobject_type, simp_all split del: if_split) + \\Untyped\ + apply (rule hoare_pre, wp) + apply (frule range_cover_not_zero[rotated -1],simp) + apply (clarsimp simp: APIType_capBits_def objBits_simps ptr_add_def o_def) + apply (subst upto_enum_red') + apply unat_arith + apply (clarsimp simp: o_def fromIntegral_def toInteger_nat fromInteger_nat) + apply fastforce + \\TCB\ + apply (rule hoare_pre, wp createObjects_ret2) + apply (wpsimp simp: curDomain_def) + apply (clarsimp simp: APIType_capBits_def word_bits_def objBits_simps ptr_add_def o_def) + apply (fastforce simp: objBitsKO_def objBits_def) + \\other APIObjectType\ + apply ((rule hoare_pre, wp createObjects_ret2, + clarsimp simp: APIType_capBits_def word_bits_def objBits_simps ptr_add_def o_def, + fastforce simp: objBitsKO_def objBits_def)+)[3] + \\Arch objects\ + by (wp createObjects_ret2 + | clarsimp simp: APIType_capBits_def objBits_if_dev word_bits_def + split del: if_split + | simp add: objBits_simps + | (rule exI, (fastforce simp: bit_simps)))+ lemma createNewCaps_range_helper2: "\\s. range_cover ptr sz (APIType_capBits tp us) n \ 0 < n\ @@ -4037,9 +4036,6 @@ end context begin interpretation Arch . (*FIXME: arch-split*) -lemma valid_sched_etcbs[elim!]: "valid_sched_2 queues ekh sa cdom kh ct it \ valid_etcbs_2 ekh kh" - by (simp add: valid_sched_def) - crunch deleteObjects for ksIdleThread[wp]: "\s. P (ksIdleThread s)" (simp: crunch_simps wp: hoare_drop_imps unless_wp) @@ -4996,7 +4992,7 @@ lemma inv_untyped_corres': invs_distinct) apply (clarsimp simp:conj_comms ball_conj_distrib ex_in_conv) apply ((rule validE_R_validE)?, - rule_tac Q'="\_ s. valid_etcbs s \ valid_list s \ invs s \ ct_active s + rule_tac Q'="\_ s. valid_list s \ invs s \ ct_active s \ valid_untyped_inv_wcap ui (Some (cap.UntypedCap dev (ptr && ~~ mask sz) sz (if reset then 0 else idx))) s \ (reset \ pspace_no_overlap {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} s) @@ -5084,7 +5080,7 @@ lemma inv_untyped_corres': apply (clarsimp simp only: pred_conj_def invs ui) apply (strengthen vui) apply (cut_tac vui invs invs') - apply (clarsimp simp: cte_wp_at_caps_of_state valid_sched_etcbs schact_is_rct_def) + apply (clarsimp simp: cte_wp_at_caps_of_state schact_is_rct_def) apply (cut_tac vui' invs') apply (clarsimp simp: ui cte_wp_at_ctes_of if_apply_def2 ui') done diff --git a/proof/refine/AARCH64/VSpace_R.thy b/proof/refine/AARCH64/VSpace_R.thy index 5d955a122c..08130a0f10 100644 --- a/proof/refine/AARCH64/VSpace_R.thy +++ b/proof/refine/AARCH64/VSpace_R.thy @@ -350,11 +350,10 @@ lemma setObject_VCPU_corres: apply (simp add: set_vcpu_def) apply (rule corres_guard_imp) apply (rule setObject_other_corres [where P="\ko::vcpu. True"], simp) - apply (clarsimp simp: obj_at'_def) - apply (erule map_to_ctes_upd_other, simp, simp) - apply (simp add: a_type_def is_other_obj_relation_type_def) - apply (simp add: objBits_simps) - apply simp + apply (clarsimp simp: obj_at'_def) + apply (erule map_to_ctes_upd_other, simp, simp) + apply (simp add: a_type_def is_other_obj_relation_type_def) + apply (simp add: objBits_simps) apply (simp add: objBits_simps vcpuBits_def pageBits_def) apply (simp add: other_obj_relation_def asid_pool_relation_def) apply (clarsimp simp: typ_at_to_obj_at'[symmetric] obj_at_def exs_valid_def diff --git a/proof/refine/Move_R.thy b/proof/refine/Move_R.thy index 5fe79b1b0a..543c1392ed 100644 --- a/proof/refine/Move_R.thy +++ b/proof/refine/Move_R.thy @@ -250,10 +250,4 @@ lemma check_active_irq_invs_just_idle: and (\s. 0 < domain_time s) and valid_domain_list \" by (wpsimp simp: check_active_irq_def ct_in_state_def) -lemma caps_of_state_kheap_ekheap[simp]: - "caps_of_state (kheap_update f (ekheap_update ef s)) - = caps_of_state (kheap_update f s)" - apply (simp add: trans_state_update[symmetric] del: trans_state_update) - done - end