From ae7b48bd07c42e63a17a540f8b5165015b2d1acf Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Wed, 11 Dec 2024 16:30:05 +1100 Subject: [PATCH] arm ainvs: proof update for det_ext refactor Signed-off-by: Corey Lewis --- .../ARM/ArchBCorres2_AI.thy | 37 +---- .../ARM/ArchDetSchedAux_AI.thy | 142 +++++------------- .../ARM/ArchDetSchedDomainTime_AI.thy | 19 ++- .../ARM/ArchDetSchedSchedule_AI.thy | 55 +++---- .../invariant-abstract/ARM/ArchDetype_AI.thy | 9 +- .../ARM/ArchEmptyFail_AI.thy | 26 +--- .../ARM/ArchInterrupt_AI.thy | 4 + .../ARM/ArchInvariants_AI.thy | 101 ++++--------- proof/invariant-abstract/ARM/ArchKHeap_AI.thy | 30 +++- .../invariant-abstract/ARM/ArchRetype_AI.thy | 67 ++++----- .../ARM/ArchSchedule_AI.thy | 53 +++---- .../invariant-abstract/ARM/ArchUntyped_AI.thy | 11 +- .../ARM/ArchVSpaceEntries_AI.thy | 27 ++-- .../invariant-abstract/ARM/ArchVSpace_AI.thy | 2 +- 14 files changed, 209 insertions(+), 374 deletions(-) diff --git a/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy b/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy index 5cb4a812c4..13c88bbec0 100644 --- a/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy +++ b/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy @@ -15,11 +15,11 @@ named_theorems BCorres2_AI_assms crunch invoke_cnode for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state - (simp: swp_def ignore: clearMemory without_preemption filterM ethread_set ) + (simp: swp_def ignore: clearMemory without_preemption filterM) crunch create_cap,init_arch_objects,retype_region,delete_objects for (bcorres) bcorres[wp]: truncate_state - (ignore: freeMemory clearMemory retype_region_ext) + (ignore: freeMemory clearMemory) crunch set_extra_badge,derive_cap for (bcorres) bcorres[wp]: truncate_state (ignore: storeWord) @@ -28,7 +28,7 @@ crunch invoke_untyped for (bcorres) bcorres[wp]: truncate_state (ignore: sequence_x) -crunch set_mcpriority, +crunch set_mcpriority, set_priority, arch_get_sanitise_register_info, arch_post_modify_registers for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state @@ -74,10 +74,6 @@ lemma handle_arch_fault_reply_bcorres[wp,BCorres2_AI_assms]: "bcorres ( handle_arch_fault_reply a b c d) (handle_arch_fault_reply a b c d)" by (cases a; simp add: handle_arch_fault_reply_def; wp) -crunch - arch_switch_to_thread,arch_switch_to_idle_thread - for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state - end interpretation BCorres2_AI?: BCorres2_AI @@ -86,11 +82,9 @@ interpretation BCorres2_AI?: BCorres2_AI case 1 show ?case by (unfold_locales; (fact BCorres2_AI_assms)?) qed -lemmas schedule_bcorres[wp] = schedule_bcorres1[OF BCorres2_AI_axioms] - context Arch begin arch_global_naming -crunch send_ipc,send_signal,do_reply_transfer,arch_perform_invocation +crunch send_ipc,send_signal,do_reply_transfer,arch_perform_invocation,invoke_domain for (bcorres) bcorres[wp]: truncate_state (simp: gets_the_def swp_def ignore: freeMemory clearMemory loadWord cap_fault_on_failure storeWord lookup_error_on_failure getRestartPC getRegister mapME) @@ -148,10 +142,8 @@ lemma handle_vm_fault_bcorres[wp]: "bcorres (handle_vm_fault a b) (handle_vm_fau lemma handle_reserved_irq_bcorres[wp]: "bcorres (handle_reserved_irq a) (handle_reserved_irq a)" by (simp add: handle_reserved_irq_def; wp) -lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b)" - apply (cases b) - apply (simp | wp)+ - done +crunch handle_hypervisor_fault, timer_tick + for (bcorres) bcorres[wp]: truncate_state lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)" apply (cases e) @@ -160,23 +152,6 @@ lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)" | intro impI conjI allI | wp | wpc)+ done -crunch guarded_switch_to,switch_to_idle_thread - for (bcorres) bcorres[wp]: truncate_state (ignore: storeWord clearExMonitor) - -lemma choose_switch_or_idle: - "((), s') \ fst (choose_thread s) \ - (\word. ((),s') \ fst (guarded_switch_to word s)) \ - ((),s') \ fst (switch_to_idle_thread s)" - apply (simp add: choose_thread_def) - apply (clarsimp simp add: switch_to_idle_thread_def bind_def gets_def - arch_switch_to_idle_thread_def in_monad - return_def get_def modify_def put_def - get_thread_state_def - thread_get_def - split: if_split_asm) - apply force - done - end end diff --git a/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy index 553776135f..a18d03da96 100644 --- a/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy @@ -12,118 +12,59 @@ context Arch begin arch_global_naming named_theorems DetSchedAux_AI_assms +lemma set_pd_etcbs[wp]: + "set_pd p pd \\s. P (etcbs_of s)\" + unfolding set_pd_def + apply (wpsimp wp: set_object_wp_strong) + by (auto elim!: rsubst[where P=P] simp: etcbs_of'_def obj_at_def a_type_def + split: kernel_object.splits) + crunch init_arch_objects for exst[wp]: "\s. P (exst s)" - and ct[wp]: "\s. P (cur_thread s)" - and valid_etcbs[wp, DetSchedAux_AI_assms]: valid_etcbs - (wp: crunch_wps unless_wp valid_etcbs_lift) - -crunch invoke_untyped - for ct[wp, DetSchedAux_AI_assms]: "\s. P (cur_thread s)" - (wp: crunch_wps dxo_wp_weak preemption_point_inv mapME_x_inv_wp - simp: crunch_simps do_machine_op_def detype_def mapM_x_defsym unless_def - ignore: freeMemory retype_region_ext) -crunch invoke_untyped - for ready_queues[wp, DetSchedAux_AI_assms]: "\s. P (ready_queues s)" - (wp: crunch_wps mapME_x_inv_wp preemption_point_inv' - simp: detype_def detype_ext_def crunch_simps - wrap_ext_det_ext_ext_def mapM_x_defsym - ignore: freeMemory) -crunch invoke_untyped - for scheduler_action[wp, DetSchedAux_AI_assms]: "\s. P (scheduler_action s)" - (wp: crunch_wps mapME_x_inv_wp preemption_point_inv' - simp: detype_def detype_ext_def crunch_simps - wrap_ext_det_ext_ext_def mapM_x_defsym - ignore: freeMemory) -crunch invoke_untyped - for cur_domain[wp, DetSchedAux_AI_assms]: "\s. P (cur_domain s)" - (wp: crunch_wps mapME_x_inv_wp preemption_point_inv' - simp: detype_def detype_ext_def crunch_simps - wrap_ext_det_ext_ext_def mapM_x_defsym - ignore: freeMemory) -crunch invoke_untyped - for idle_thread[wp, DetSchedAux_AI_assms]: "\s. P (idle_thread s)" - (wp: crunch_wps mapME_x_inv_wp preemption_point_inv dxo_wp_weak - simp: detype_def detype_ext_def crunch_simps - wrap_ext_det_ext_ext_def mapM_x_defsym - ignore: freeMemory retype_region_ext) + and etcbs_of[wp, DetSchedAux_AI_assms]: "\s. P (etcbs_of s)" + and ready_queues[wp, DetSchedAux_AI_assms]: "\s. P (ready_queues s)" + and idle_thread[wp, DetSchedAux_AI_assms]: "\s. P (idle_thread s)" + and schedact[wp, DetSchedAux_AI_assms]: "\s. P (scheduler_action s)" + and cur_domain[wp, DetSchedAux_AI_assms]: "\s. P (cur_domain s)" + (wp: crunch_wps) -lemma tcb_sched_action_valid_idle_etcb: - "\valid_idle_etcb\ - tcb_sched_action foo thread - \\_. valid_idle_etcb\" - apply (rule valid_idle_etcb_lift) - apply (simp add: tcb_sched_action_def set_tcb_queue_def) - apply (wp | simp)+ - done - -lemma delete_objects_etcb_at[wp, DetSchedAux_AI_assms]: - "\\s::det_ext state. etcb_at P t s\ delete_objects a b \\r s. etcb_at P t s\" - apply (simp add: delete_objects_def) - apply (wp) - apply (simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def etcb_at_def|wp)+ - done - -crunch reset_untyped_cap - for etcb_at[wp]: "etcb_at P t" - (wp: preemption_point_inv' mapME_x_inv_wp crunch_wps - simp: unless_def) - -crunch reset_untyped_cap - for valid_etcbs[wp]: "valid_etcbs" - (wp: preemption_point_inv' mapME_x_inv_wp crunch_wps - simp: unless_def) - -lemma invoke_untyped_etcb_at [DetSchedAux_AI_assms]: - "\(\s :: det_ext state. etcb_at P t s) and valid_etcbs\ invoke_untyped ui \\r s. st_tcb_at (Not o inactive) t s \ etcb_at P t s\" - apply (cases ui) - apply (simp add: mapM_x_def[symmetric] invoke_untyped_def whenE_def - split del: if_split) - apply (wp retype_region_etcb_at mapM_x_wp' - create_cap_no_pred_tcb_at typ_at_pred_tcb_at_lift - hoare_convert_imp[OF create_cap_no_pred_tcb_at] - hoare_convert_imp[OF _ init_arch_objects_exst] - | simp - | (wp (once) hoare_drop_impE_E))+ - done +crunch init_arch_objects + for valid_queues[wp]: valid_queues + and valid_sched_action[wp]: valid_sched_action + and valid_sched[wp]: valid_sched + (wp: valid_queues_lift valid_sched_action_lift valid_sched_lift) +lemma tcb_sched_action_valid_idle_etcb: + "tcb_sched_action foo thread \valid_idle_etcb\" + by (rule valid_idle_etcb_lift) + (wpsimp simp: tcb_sched_action_def set_tcb_queue_def) crunch init_arch_objects for valid_blocked[wp, DetSchedAux_AI_assms]: valid_blocked - (wp: valid_blocked_lift set_cap_typ_at) + (wp: valid_blocked_lift crunch_wps) -lemma perform_asid_control_etcb_at:"\(\s. etcb_at P t s) and valid_etcbs\ - perform_asid_control_invocation aci - \\r s. st_tcb_at (Not \ inactive) t s \ etcb_at P t s\" +lemma perform_asid_control_etcb_at: + "\etcb_at P t\ + perform_asid_control_invocation aci + \\r s. st_tcb_at (Not \ inactive) t s \ etcb_at P t s\" apply (simp add: perform_asid_control_invocation_def) - apply (rule hoare_pre) - apply (wp | wpc | simp)+ + apply wpsimp apply (wp hoare_imp_lift_something typ_at_pred_tcb_at_lift)[1] apply (rule hoare_drop_imps) apply (wp retype_region_etcb_at)+ apply simp done -crunch perform_asid_control_invocation - for ct[wp]: "\s. P (cur_thread s)" - crunch perform_asid_control_invocation for idle_thread[wp]: "\s. P (idle_thread s)" + and valid_blocked[wp]: valid_blocked + and schedact[wp]: "\s. P (scheduler_action s)" + and ready_queues[wp]: "\s. P (ready_queues s)" + and cur_domain[wp]: "\s. P (cur_domain s)" + (wp: hoare_weak_lift_imp simp: detype_def) crunch perform_asid_control_invocation - for valid_etcbs[wp]: valid_etcbs (wp: hoare_weak_lift_imp) - -crunch perform_asid_control_invocation - for valid_blocked[wp]: valid_blocked (wp: hoare_weak_lift_imp) - -crunch perform_asid_control_invocation - for schedact[wp]: "\s :: det_ext state. P (scheduler_action s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory) - -crunch perform_asid_control_invocation - for rqueues[wp]: "\s :: det_ext state. P (ready_queues s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory) - -crunch perform_asid_control_invocation - for cur_domain[wp]: "\s :: det_ext state. P (cur_domain s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory) + for ct[wp]: "\s. P (cur_thread s)" lemma perform_asid_control_invocation_valid_sched: "\ct_active and invs and valid_aci aci and valid_sched and valid_idle\ @@ -143,26 +84,11 @@ lemma perform_asid_control_invocation_valid_sched: apply simp done -crunch init_arch_objects - for valid_queues[wp]: valid_queues (wp: valid_queues_lift) - -crunch init_arch_objects - for valid_sched_action[wp]: valid_sched_action (wp: valid_sched_action_lift) - -crunch init_arch_objects - for valid_sched[wp]: valid_sched (wp: valid_sched_lift) - end lemmas tcb_sched_action_valid_idle_etcb = ARM.tcb_sched_action_valid_idle_etcb -global_interpretation DetSchedAux_AI_det_ext?: DetSchedAux_AI_det_ext - proof goal_cases - interpret Arch . - case 1 show ?case by (unfold_locales; (fact DetSchedAux_AI_assms)?) - qed - global_interpretation DetSchedAux_AI?: DetSchedAux_AI proof goal_cases interpret Arch . diff --git a/proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy index f190452d13..8783d0a64b 100644 --- a/proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy @@ -20,9 +20,10 @@ crunch arch_activate_idle_thread, arch_switch_to_thread, arch_switch_to_idle_thread, handle_arch_fault_reply, arch_invoke_irq_control, handle_vm_fault, arch_get_sanitise_register_info, - prepare_thread_delete, handle_hypervisor_fault, make_arch_fault_msg, + prepare_thread_delete, handle_hypervisor_fault, make_arch_fault_msg, init_arch_objects, arch_post_modify_registers, arch_post_cap_deletion, arch_invoke_irq_handler - for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\s. P (domain_list s)" + for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\s::det_state. P (domain_list s)" + (wp: crunch_wps) crunch arch_finalise_cap for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\s. P (domain_time s)" @@ -34,7 +35,8 @@ crunch arch_invoke_irq_control, handle_vm_fault, arch_get_sanitise_register_info, prepare_thread_delete, handle_hypervisor_fault, arch_post_modify_registers, arch_post_cap_deletion, arch_invoke_irq_handler - for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\s. P (domain_time s)" + for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\s::det_state. P (domain_time s)" + (wp: crunch_wps) declare init_arch_objects_exst[DetSchedDomainTime_AI_assms] make_arch_fault_msg_inv[DetSchedDomainTime_AI_assms] @@ -55,11 +57,11 @@ crunch arch_mask_irq_signal for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\s. P (domain_list s)" crunch arch_perform_invocation - for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\s. P (domain_time s)" + for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\s::det_state. P (domain_time s)" (wp: crunch_wps check_cap_inv) crunch arch_perform_invocation - for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\s. P (domain_list s)" + for domain_list_inv[wp, DetSchedDomainTime_AI_assms]: "\s::det_state. P (domain_list s)" (wp: crunch_wps check_cap_inv) lemma timer_tick_valid_domain_time: @@ -68,7 +70,7 @@ lemma timer_tick_valid_domain_time: \\x s. domain_time s = 0 \ scheduler_action s = choose_new_thread\" (is "\ ?dtnot0 \ _ \ _ \") unfolding timer_tick_def supply if_split[split del] - supply ethread_get_wp[wp del] + supply thread_get_wp[wp del] supply if_apply_def2[simp] apply (wpsimp wp: reschedule_required_valid_domain_time hoare_vcg_const_imp_lift gts_wp @@ -76,10 +78,13 @@ lemma timer_tick_valid_domain_time: postcondition once we hit thread_set_time_slice *) hoare_post_imp[where Q'="\_. ?dtnot0" and Q="\_ s. domain_time s = 0 \ X s" and f="thread_set_time_slice t ts" for X t ts] - hoare_drop_imp[where f="ethread_get t f" for t f]) + hoare_drop_imp[where f="thread_get t f" for t f]) apply fastforce done +crunch do_machine_op + for domain_time_sched[wp]: "\s. P (domain_time s) (scheduler_action s)" + lemma handle_interrupt_valid_domain_time [DetSchedDomainTime_AI_assms]: "\\s :: det_ext state. 0 < domain_time s \ handle_interrupt i diff --git a/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy index 35a913be19..7a67f72df4 100644 --- a/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy @@ -19,11 +19,6 @@ crunch prepare_thread_delete for prepare_thread_delete_idle_thread[wp, DetSchedSchedule_AI_assms]: "\(s:: det_ext state). P (idle_thread s)" -crunch - arch_switch_to_idle_thread, arch_switch_to_thread, arch_get_sanitise_register_info, arch_post_modify_registers - for valid_etcbs[wp, DetSchedSchedule_AI_assms]: valid_etcbs - (simp: crunch_simps ignore: clearExMonitor) - crunch switch_to_idle_thread, switch_to_thread, set_vm_root, arch_get_sanitise_register_info, arch_post_modify_registers for valid_queues[wp, DetSchedSchedule_AI_assms]: valid_queues @@ -35,11 +30,9 @@ crunch (simp: crunch_simps ignore: clearExMonitor) crunch set_vm_root - for ct_not_in_q[wp]: "ct_not_in_q" - (wp: crunch_wps simp: crunch_simps) - -crunch set_vm_root - for ct_not_in_q'[wp]: "\s. ct_not_in_q_2 (ready_queues s) (scheduler_action s) t" + for ready_queues[wp]: "\s. P (ready_queues s)" + and ct_not_in_q[wp]: "ct_not_in_q" + and ct_not_in_q'[wp]: "\s. ct_not_in_q_2 (ready_queues s) (scheduler_action s) t" (wp: crunch_wps simp: crunch_simps) lemma switch_to_idle_thread_ct_not_in_q [wp, DetSchedSchedule_AI_assms]: @@ -54,7 +47,7 @@ lemma switch_to_idle_thread_ct_not_in_q [wp, DetSchedSchedule_AI_assms]: crunch set_vm_root for valid_sched_action'[wp]: "\s. valid_sched_action_2 (scheduler_action s) - (ekheap s) (kheap s) thread (cur_domain s)" + (etcbs_of s) (kheap s) thread (cur_domain s)" (wp: crunch_wps simp: crunch_simps) lemma switch_to_idle_thread_valid_sched_action [wp, DetSchedSchedule_AI_assms]: @@ -71,7 +64,7 @@ lemma switch_to_idle_thread_valid_sched_action [wp, DetSchedSchedule_AI_assms]: crunch set_vm_root for ct_in_cur_domain'[wp]: "\s. ct_in_cur_domain_2 t (idle_thread s) - (scheduler_action s) (cur_domain s) (ekheap s)" + (scheduler_action s) (cur_domain s) (etcbs_of s)" (wp: crunch_wps simp: crunch_simps) lemma switch_to_idle_thread_ct_in_cur_domain [wp, DetSchedSchedule_AI_assms]: @@ -102,7 +95,7 @@ crunch set_vm_root (wp: crunch_wps whenE_wp simp: crunch_simps) crunch arch_switch_to_thread - for ct_in_cur_domain_2[wp, DetSchedSchedule_AI_assms]: "\s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)" + for ct_in_cur_domain_2[wp, DetSchedSchedule_AI_assms]: "\s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (etcbs_of s)" (simp: crunch_simps) crunch set_vm_root @@ -142,7 +135,7 @@ lemma arch_switch_to_thread_valid_blocked [wp, DetSchedSchedule_AI_assms]: done lemma switch_to_idle_thread_ct_not_queued [wp, DetSchedSchedule_AI_assms]: - "\valid_queues and valid_etcbs and valid_idle\ + "\valid_queues and valid_idle\ switch_to_idle_thread \\rv s. not_queued (cur_thread s) s\" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def @@ -192,17 +185,19 @@ lemma switch_to_idle_thread_cur_thread_idle_thread [wp, DetSchedSchedule_AI_assm "\\\ switch_to_idle_thread \\_ s. cur_thread s = idle_thread s\" by (wp | simp add:switch_to_idle_thread_def arch_switch_to_idle_thread_def)+ -lemma set_pd_valid_etcbs[wp]: - "\valid_etcbs\ set_pd ptr pd \\rv. valid_etcbs\" - by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_pd_def)+ +lemma set_pt_etcbs[wp]: + "set_pt ptr pt \\s. P (etcbs_of s)\" + unfolding set_pt_def + apply (wpsimp wp: set_object_wp_strong) + by (auto elim!: rsubst[where P=P] simp: etcbs_of'_def obj_at_def a_type_def + split: kernel_object.splits) -lemma set_pt_valid_etcbs[wp]: - "\valid_etcbs\ set_pt ptr pt \\rv. valid_etcbs\" - by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_pt_def)+ - -lemma set_asid_pool_valid_etcbs[wp]: - "\valid_etcbs\ set_asid_pool ptr pool \\rv. valid_etcbs\" - by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_asid_pool_def)+ +lemma set_asid_pool_etcbs[wp]: + "set_asid_pool ptr pool \\s. P (etcbs_of s)\" + unfolding set_asid_pool_def + apply (wpsimp wp: set_object_wp_strong) + by (auto elim!: rsubst[where P=P] simp: etcbs_of'_def obj_at_def a_type_def + split: kernel_object.splits) lemma set_pt_valid_sched[wp]: "\valid_sched\ set_pt ptr pt \\rv. valid_sched\" @@ -222,12 +217,6 @@ crunch (wp: crunch_wps hoare_drop_imps unless_wp select_inv mapM_wp subset_refl if_fun_split simp: crunch_simps ignore: tcb_sched_action) -crunch - arch_finalise_cap, prepare_thread_delete - for valid_etcbs[wp, DetSchedSchedule_AI_assms]: valid_etcbs - (wp: hoare_drop_imps unless_wp select_inv mapM_x_wp mapM_wp subset_refl - if_fun_split simp: crunch_simps ignore: set_object thread_set) - crunch arch_finalise_cap, prepare_thread_delete for simple_sched_action[wp, DetSchedSchedule_AI_assms]: simple_sched_action @@ -311,11 +300,9 @@ lemma arch_post_modify_registers_not_idle_thread[DetSchedSchedule_AI_assms]: crunch arch_post_cap_deletion for valid_sched[wp, DetSchedSchedule_AI_assms]: valid_sched - and valid_etcbs[wp, DetSchedSchedule_AI_assms]: valid_etcbs and ct_not_in_q[wp, DetSchedSchedule_AI_assms]: ct_not_in_q and simple_sched_action[wp, DetSchedSchedule_AI_assms]: simple_sched_action and not_cur_thread[wp, DetSchedSchedule_AI_assms]: "not_cur_thread t" - and is_etcb_at[wp, DetSchedSchedule_AI_assms]: "is_etcb_at t" and not_queued[wp, DetSchedSchedule_AI_assms]: "not_queued t" and sched_act_not[wp, DetSchedSchedule_AI_assms]: "scheduler_act_not t" and weak_valid_sched_action[wp, DetSchedSchedule_AI_assms]: weak_valid_sched_action @@ -345,6 +332,10 @@ crunch cap_swap_for_delete, cap_move, cancel_badged_sends simp: crunch_simps check_cap_at_def filterM_mapM unless_def ignore: without_preemption filterM rec_del check_cap_at cap_revoke) +crunch arch_switch_to_thread + for etcbs_of[wp, DetSchedSchedule_AI_assms]: "\s. P (etcbs_of s)" + and cur_domain[wp, DetSchedSchedule_AI_assms]: "\s. P (cur_domain s)" + end global_interpretation DetSchedSchedule_AI?: DetSchedSchedule_AI diff --git a/proof/invariant-abstract/ARM/ArchDetype_AI.thy b/proof/invariant-abstract/ARM/ArchDetype_AI.thy index 6f98d49f50..3a68b13926 100644 --- a/proof/invariant-abstract/ARM/ArchDetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetype_AI.thy @@ -450,9 +450,8 @@ lemma in_user_frame_eq: Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex order_class.Icc_eq_Icc and [simp] = p2pm1_to_mask - shows "p \ untyped_range cap \ in_user_frame p - (trans_state (\_. detype_ext (untyped_range cap) (exst s)) s - \kheap := \x. if x \ untyped_range cap then None else kheap s x\) + shows "p \ untyped_range cap \ + in_user_frame p (s \kheap := \x. if x \ untyped_range cap then None else kheap s x\) = in_user_frame p s" using cap_is_valid untyped apply (cases cap; simp add: in_user_frame_def valid_untyped_def valid_cap_def obj_at_def) @@ -478,9 +477,7 @@ lemma in_device_frame_eq: order_class.Icc_eq_Icc and p2pm1[simp] = p2pm1_to_mask shows "p \ untyped_range cap - \ in_device_frame p - (trans_state (\_. detype_ext (untyped_range cap) (exst s)) s - \kheap := \x. if x \ untyped_range cap then None else kheap s x\) + \ in_device_frame p (s \kheap := \x. if x \ untyped_range cap then None else kheap s x\) = in_device_frame p s" using cap_is_valid untyped unfolding in_device_frame_def diff --git a/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy b/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy index e55c7e412b..c5f6d06e48 100644 --- a/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy @@ -142,18 +142,6 @@ crunch for (empty_fail) empty_fail[wp, EmptyFail_AI_assms] end -global_interpretation EmptyFail_AI_schedule_unit?: EmptyFail_AI_schedule_unit - proof goal_cases - interpret Arch . - case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) - qed - -global_interpretation EmptyFail_AI_schedule_det?: EmptyFail_AI_schedule_det - proof goal_cases - interpret Arch . - case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) - qed - global_interpretation EmptyFail_AI_schedule?: EmptyFail_AI_schedule proof goal_cases interpret Arch . @@ -171,21 +159,9 @@ crunch possible_switch_to, handle_event, activate_thread page_table_invocation.splits page_invocation.splits asid_control_invocation.splits asid_pool_invocation.splits arch_invocation.splits irq_state.splits syscall.splits flush_type.splits page_directory_invocation.splits - ignore: resetTimer_impl ackInterrupt_impl ignore_del: possible_switch_to) + ignore: resetTimer_impl ackInterrupt_impl) end -global_interpretation EmptyFail_AI_call_kernel_unit?: EmptyFail_AI_call_kernel_unit - proof goal_cases - interpret Arch . - case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) - qed - -global_interpretation EmptyFail_AI_call_kernel_det?: EmptyFail_AI_call_kernel_det - proof goal_cases - interpret Arch . - case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) - qed - global_interpretation EmptyFail_AI_call_kernel?: EmptyFail_AI_call_kernel proof goal_cases interpret Arch . diff --git a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy index c34b0956fd..dc491ab727 100644 --- a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy @@ -201,6 +201,10 @@ lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (maskInterrupt f irq)" by (wp | simp add: maskInterrupt_def)+ +crunch timer_tick + for invs[wp]: invs + (wp: thread_set_invs_trivial[OF ball_tcb_cap_casesI]) + lemma (* handle_interrupt_invs *) [Interrupt_AI_assms]: "\invs\ handle_interrupt irq \\_. invs\" apply (simp add: handle_interrupt_def) diff --git a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy index f2d42846c3..5521b6bc4a 100644 --- a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy @@ -2303,84 +2303,47 @@ lemma valid_arch_arch_tcb_context_set[simp]: "valid_arch_tcb (arch_tcb_context_set a t) = valid_arch_tcb t" by (simp add: arch_tcb_context_set_def) -lemma tcb_arch_ref_context_update: - "tcb_arch_ref (t\tcb_arch := (arch_tcb_context_set a (tcb_arch t))\) = tcb_arch_ref t" - by (simp add: tcb_arch_ref_def arch_tcb_context_set_def) - -lemma tcb_arch_ref_set_registers: - "tcb_arch_ref (tcb\tcb_arch := arch_tcb_set_registers regs (tcb_arch tcb)\) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - lemma valid_arch_arch_tcb_set_registers[simp]: "valid_arch_tcb (arch_tcb_set_registers a t) = valid_arch_tcb t" by (simp add: arch_tcb_set_registers_def) -lemma tcb_arch_ref_ipc_buffer_update: "\tcb. - tcb_arch_ref (tcb_ipc_buffer_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - -lemma tcb_arch_ref_mcpriority_update: "\tcb. - tcb_arch_ref (tcb_mcpriority_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - -lemma tcb_arch_ref_ctable_update: "\tcb. - tcb_arch_ref (tcb_ctable_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - -lemma tcb_arch_ref_vtable_update: "\tcb. - tcb_arch_ref (tcb_vtable_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - -lemma tcb_arch_ref_reply_update: "\tcb. - tcb_arch_ref (tcb_reply_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - -lemma tcb_arch_ref_caller_update: "\tcb. - tcb_arch_ref (tcb_caller_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - -lemma tcb_arch_ref_ipcframe_update: "\tcb. - tcb_arch_ref (tcb_ipcframe_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - -lemma tcb_arch_ref_state_update: "\tcb. - tcb_arch_ref (tcb_state_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - -lemma tcb_arch_ref_fault_handler_update: "\tcb. - tcb_arch_ref (tcb_fault_handler_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - -lemma tcb_arch_ref_fault_update: "\tcb. - tcb_arch_ref (tcb_fault_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - -lemma tcb_arch_ref_bound_notification_update: "\tcb. - tcb_arch_ref (tcb_bound_notification_update f tcb) = tcb_arch_ref tcb" - by (simp add: tcb_arch_ref_def) - - -lemmas tcb_arch_ref_simps[simp] = tcb_arch_ref_ipc_buffer_update tcb_arch_ref_mcpriority_update - tcb_arch_ref_ctable_update tcb_arch_ref_vtable_update tcb_arch_ref_reply_update - tcb_arch_ref_caller_update tcb_arch_ref_ipcframe_update tcb_arch_ref_state_update - tcb_arch_ref_fault_handler_update tcb_arch_ref_fault_update tcb_arch_ref_bound_notification_update - tcb_arch_ref_context_update tcb_arch_ref_set_registers +lemma tcb_arch_ref_simps[simp]: + "\f. tcb_arch_ref (tcb_ipc_buffer_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_mcpriority_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_ctable_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_vtable_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_reply_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_caller_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_ipcframe_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_state_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_fault_handler_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_fault_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_bound_notification_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_domain_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_priority_update f tcb) = tcb_arch_ref tcb" + "\f. tcb_arch_ref (tcb_time_slice_update f tcb) = tcb_arch_ref tcb" + "tcb_arch_ref (t\tcb_arch := (arch_tcb_context_set a (tcb_arch t))\) = tcb_arch_ref t" + "tcb_arch_ref (tcb\tcb_arch := arch_tcb_set_registers regs (tcb_arch tcb)\) = tcb_arch_ref tcb" + by (auto simp: tcb_arch_ref_def arch_tcb_set_registers_def arch_tcb_context_set_def) lemma hyp_live_tcb_def: "hyp_live (TCB tcb) = bound (tcb_arch_ref tcb)" by (clarsimp simp: hyp_live_def tcb_arch_ref_def) lemma hyp_live_tcb_simps[simp]: -"\tcb f. hyp_live (TCB (tcb_ipc_buffer_update f tcb)) = hyp_live (TCB tcb)" -"\tcb f. hyp_live (TCB (tcb_mcpriority_update f tcb)) = hyp_live (TCB tcb)" -"\tcb f. hyp_live (TCB (tcb_ctable_update f tcb)) = hyp_live (TCB tcb)" -"\tcb f. hyp_live (TCB (tcb_vtable_update f tcb)) = hyp_live (TCB tcb)" -"\tcb f. hyp_live (TCB (tcb_reply_update f tcb)) = hyp_live (TCB tcb)" -"\tcb f. hyp_live (TCB (tcb_caller_update f tcb)) = hyp_live (TCB tcb)" -"\tcb f. hyp_live (TCB (tcb_ipcframe_update f tcb)) = hyp_live (TCB tcb)" -"\tcb f. hyp_live (TCB (tcb_state_update f tcb)) = hyp_live (TCB tcb)" -"\tcb f. hyp_live (TCB (tcb_fault_handler_update f tcb)) = hyp_live (TCB tcb)" -"\tcb f. hyp_live (TCB (tcb_fault_update f tcb)) = hyp_live (TCB tcb)" -"\tcb f. hyp_live (TCB (tcb_bound_notification_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_ipc_buffer_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_mcpriority_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_ctable_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_vtable_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_reply_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_caller_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_ipcframe_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_state_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_fault_handler_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_fault_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_bound_notification_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_domain_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_priority_update f tcb)) = hyp_live (TCB tcb)" + "\f. hyp_live (TCB (tcb_time_slice_update f tcb)) = hyp_live (TCB tcb)" by (simp_all add: hyp_live_tcb_def) diff --git a/proof/invariant-abstract/ARM/ArchKHeap_AI.thy b/proof/invariant-abstract/ARM/ArchKHeap_AI.thy index f5a3c2e01f..8adec8e661 100644 --- a/proof/invariant-abstract/ARM/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/ARM/ArchKHeap_AI.thy @@ -796,7 +796,7 @@ lemma pspace_respects_region_cong[cong]: definition "obj_is_device tp dev \ case tp of Untyped \ dev - | _ \(case (default_object tp dev 0) of (ArchObj (DataPage dev _)) \ dev + | _ \(case default_object tp dev 0 0 of (ArchObj (DataPage dev _)) \ dev | _ \ False)" lemma cap_is_device_obj_is_device[simp]: @@ -839,6 +839,30 @@ lemma state_hyp_refs_of_tcb_state_update: apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits) done +lemma state_hyp_refs_of_tcb_domain_update: + "kheap s t = Some (TCB tcb) \ + state_hyp_refs_of (s\kheap := (kheap s)(t \ TCB (tcb\tcb_domain := d\))\) + = state_hyp_refs_of s" + apply (rule all_ext) + apply (clarsimp simp add: state_hyp_refs_of_def obj_at_def split: option.splits) + done + +lemma state_hyp_refs_of_tcb_priority_update: + "kheap s t = Some (TCB tcb) \ + state_hyp_refs_of (s\kheap := (kheap s)(t \ TCB (tcb\tcb_priority := p\))\) + = state_hyp_refs_of s" + apply (rule all_ext) + apply (clarsimp simp add: state_hyp_refs_of_def obj_at_def split: option.splits) + done + +lemma state_hyp_refs_of_tcb_time_slice_update: + "kheap s t = Some (TCB tcb) \ + state_hyp_refs_of (s\kheap := (kheap s)(t \ TCB (tcb\tcb_time_slice := ts\))\) + = state_hyp_refs_of s" + apply (rule all_ext) + apply (clarsimp simp add: state_hyp_refs_of_def obj_at_def split: option.splits) + done + lemma arch_valid_obj_same_type: "\ arch_valid_obj ao s; kheap s p = Some ko; a_type k = a_type ko \ \ arch_valid_obj ao (s\kheap := (kheap s)(p \ k)\)" @@ -846,11 +870,11 @@ lemma arch_valid_obj_same_type: clarsimp simp: typ_at_same_type) -lemma default_arch_object_not_live: "\ live (ArchObj (default_arch_object aty dev us))" +lemma default_arch_object_not_live[simp]: "\ live (ArchObj (default_arch_object aty dev us))" by (clarsimp simp: default_arch_object_def live_def hyp_live_def arch_live_def split: aobject_type.splits) -lemma default_tcb_not_live: "\ live (TCB default_tcb)" +lemma default_tcb_not_live[simp]: "\ live (TCB (default_tcb d))" by (clarsimp simp: default_tcb_def default_arch_tcb_def live_def hyp_live_def) lemma valid_arch_tcb_same_type: diff --git a/proof/invariant-abstract/ARM/ArchRetype_AI.thy b/proof/invariant-abstract/ARM/ArchRetype_AI.thy index 0e191d2b36..9cd07e358c 100644 --- a/proof/invariant-abstract/ARM/ArchRetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchRetype_AI.thy @@ -58,23 +58,14 @@ declare store_pde_state_hyp_refs_of [wp] (* These also prove facts about copy_global_mappings *) crunch init_arch_objects - for pspace_aligned[wp]: "pspace_aligned" - (ignore: clearMemory wp: crunch_wps unless_wp) -crunch init_arch_objects - for pspace_distinct[wp]: "pspace_distinct" - (ignore: clearMemory wp: crunch_wps unless_wp) -crunch init_arch_objects - for mdb_inv[wp]: "\s. P (cdt s)" - (ignore: clearMemory wp: crunch_wps unless_wp) -crunch init_arch_objects - for valid_mdb[wp]: "valid_mdb" - (ignore: clearMemory wp: crunch_wps unless_wp) -crunch init_arch_objects - for cte_wp_at[wp]: "\s. P (cte_wp_at P' p s)" - (ignore: clearMemory wp: crunch_wps unless_wp) -crunch init_arch_objects - for typ_at[wp]: "\s. P (typ_at T p s)" - (ignore: clearMemory wp: crunch_wps unless_wp) + for pspace_aligned[wp]: "pspace_aligned" + and pspace_distinct[wp]: "pspace_distinct" + and mdb_inv[wp]: "\s. P (cdt s)" + and valid_mdb[wp]: "valid_mdb" + and cte_wp_at[wp]: "\s. P (cte_wp_at P' p s)" + and typ_at[wp]: "\s. P (typ_at T p s)" + and cur_thread[wp]: "\s. P (cur_thread s)" + (ignore: clearMemory wp: crunch_wps) lemma mdb_cte_at_store_pde[wp]: "\\s. mdb_cte_at (swp (cte_wp_at ((\) cap.NullCap)) s) (cdt s)\ @@ -667,7 +658,7 @@ lemma valid_untyped_helper [Retype_AI_assms]: and cn : "caps_no_overlap ptr sz s" and vp : "valid_pspace s" shows "valid_cap c - (s\kheap := \x. if x \ set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\)" + (s\kheap := \x. if x \ set (retype_addrs ptr ty n us) then Some (default_object ty dev us (cur_domain s)) else kheap s x\)" (is "valid_cap c ?ns") proof - have obj_at_pres: "\P x. obj_at P x s \ obj_at P x ?ns" @@ -675,7 +666,7 @@ lemma valid_untyped_helper [Retype_AI_assms]: (erule pspace_no_overlapC [OF pn _ _ cover vp]) note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff - have cover':"range_cover ptr sz (obj_bits (default_object ty dev us)) n" + have cover':"range_cover ptr sz (obj_bits (default_object ty dev us (cur_domain s))) n" using cover tyunt by (clarsimp simp: obj_bits_dev_irr) @@ -762,30 +753,28 @@ lemma valid_cap: proof - note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff - have cover':"range_cover ptr sz (obj_bits (default_object ty dev us)) n" + have cover':"range_cover ptr sz (obj_bits (default_object ty dev us (cur_domain s))) n" using cover tyunt by (clarsimp simp: obj_bits_dev_irr) show ?thesis using cap apply (case_tac cap) unfolding valid_cap_def - apply (simp_all add: valid_cap_def obj_at_pres cte_at_pres - split: option.split_asm arch_cap.split_asm - option.splits) + apply (simp_all add: valid_cap_def obj_at_pres cte_at_pres + split: option.split_asm arch_cap.split_asm option.splits) apply (clarsimp simp add: valid_untyped_def ps_def s'_def) apply (intro conjI) - apply clarsimp - apply (drule disjoint_subset [OF retype_addrs_obj_range_subset [OF _ cover' tyunt]]) - apply (simp add: Int_ac p_assoc_help[symmetric]) - apply simp apply clarsimp + apply (drule disjoint_subset [OF retype_addrs_obj_range_subset [OF _ cover' tyunt]]) + apply (simp add: Int_ac p_assoc_help[symmetric]) + apply fastforce + apply clarsimp apply (drule disjoint_subset [OF retype_addrs_obj_range_subset [OF _ cover' tyunt]]) apply (simp add: Int_ac p_assoc_help[symmetric]) - apply simp - using cover tyunt - apply (simp add: obj_bits_api_def2 split: Structures_A.apiobject_type.splits) - apply clarsimp+ - apply (fastforce elim!: obj_at_pres)+ + apply fastforce + using cover tyunt + apply (simp add: obj_bits_api_def2 split: Structures_A.apiobject_type.splits) + apply (fastforce elim!: obj_at_pres)+ done qed @@ -802,13 +791,13 @@ lemma valid_arch_state: valid_asid_table_def valid_global_pts_def) lemma vs_refs_default [simp]: - "vs_refs (default_object ty dev us) = {}" + "vs_refs (default_object ty dev us d) = {}" by (simp add: default_object_def default_arch_object_def tyunt vs_refs_def o_def pde_ref_def graph_of_def split: Structures_A.apiobject_type.splits aobject_type.splits) lemma vs_refs_pages_default [simp]: - "vs_refs_pages (default_object ty dev us) = {}" + "vs_refs_pages (default_object ty dev us d) = {}" by (simp add: default_object_def default_arch_object_def tyunt vs_refs_pages_def o_def pde_ref_pages_def pte_ref_pages_def graph_of_def split: Structures_A.apiobject_type.splits aobject_type.splits) @@ -869,10 +858,10 @@ proof fix p ao assume p: "(\\ p) s'" assume "ko_at (ArchObj ao) p s'" - hence "ko_at (ArchObj ao) p s \ ArchObj ao = default_object ty dev us" + hence "ko_at (ArchObj ao) p s \ ArchObj ao = default_object ty dev us (cur_domain s)" by (simp add: ps_def obj_at_def s'_def split: if_split_asm) moreover - { assume "ArchObj ao = default_object ty dev us" with tyunt + { assume "ArchObj ao = default_object ty dev us (cur_domain s)" with tyunt have "valid_vspace_obj ao s'" by (rule valid_vspace_obj_default) } moreover @@ -1001,7 +990,7 @@ lemma pspace_respects_device_regionD: lemma default_obj_dev: - "\ty \ Untyped;default_object ty dev us = ArchObj (DataPage dev' sz)\ \ dev = dev'" + "\ty \ Untyped;default_object ty dev us d = ArchObj (DataPage dev' sz)\ \ dev = dev'" by (clarsimp simp: default_object_def default_arch_object_def split: apiobject_type.split_asm aobject_type.split_asm) @@ -1137,7 +1126,7 @@ lemma pspace_respects_device_region: apply (rule pspace_respects_device_regionI) apply (clarsimp simp add: pspace_respects_device_region_def s'_def ps_def split: if_split_asm ) - apply (drule retype_addrs_obj_range_subset[OF _ _ tyunt]) + apply (drule retype_addrs_obj_range_subset[OF _ _ tyunt, where d'="cur_domain s"]) using cover tyunt apply (simp add: obj_bits_api_def3 split: if_splits) apply (frule default_obj_dev[OF tyunt],simp) @@ -1151,7 +1140,7 @@ lemma pspace_respects_device_region: apply fastforce apply (clarsimp simp add: pspace_respects_device_region_def s'_def ps_def split: if_split_asm ) - apply (drule retype_addrs_obj_range_subset[OF _ _ tyunt]) + apply (drule retype_addrs_obj_range_subset[OF _ _ tyunt, where d'="cur_domain s"]) using cover tyunt apply (simp add: obj_bits_api_def4 split: if_splits) apply (frule default_obj_dev[OF tyunt],simp) diff --git a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy index cab261b35e..7ac02733f3 100644 --- a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy @@ -50,11 +50,9 @@ lemma arch_stt_tcb [wp,Schedule_AI_assms]: apply (wp) done -lemma arch_stt_runnable[Schedule_AI_assms]: - "\st_tcb_at runnable t\ arch_switch_to_thread t \\r . st_tcb_at runnable t\" - apply (simp add: arch_switch_to_thread_def) - apply wp - done +lemma arch_stt_st_tcb_at[Schedule_AI_assms]: + "arch_switch_to_thread t \st_tcb_at Q t\" + by (wpsimp simp: arch_switch_to_thread_def) lemma arch_stit_invs[wp, Schedule_AI_assms]: "\invs\ arch_switch_to_idle_thread \\r. invs\" @@ -66,8 +64,15 @@ lemma arch_stit_tcb_at[wp]: apply wp done +lemma idle_strg: + "thread = idle_thread s \ invs s \ invs (s\cur_thread := thread\)" + by (clarsimp simp: invs_def valid_state_def valid_idle_def cur_tcb_def + pred_tcb_at_def valid_machine_state_def obj_at_def is_tcb_def) + crunch set_vm_root for ct[wp]: "\s. P (cur_thread s)" + and it[wp]: "\s. P (idle_thread s)" + and scheduler_action[wp]: "\s. P (scheduler_action s)" (wp: crunch_wps simp: crunch_simps) lemma arch_stit_activatable[wp, Schedule_AI_assms]: @@ -77,11 +82,10 @@ lemma arch_stit_activatable[wp, Schedule_AI_assms]: done lemma stit_invs [wp,Schedule_AI_assms]: - "\invs\ switch_to_idle_thread \\rv. invs\" - apply (simp add: switch_to_idle_thread_def) - apply (wp sct_invs) - by (clarsimp simp: invs_def valid_state_def valid_idle_def cur_tcb_def - pred_tcb_at_def valid_machine_state_def obj_at_def is_tcb_def) + "switch_to_idle_thread \invs\" + apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) + apply (wpsimp|strengthen idle_strg)+ + done lemma stit_activatable[Schedule_AI_assms]: "\invs\ switch_to_idle_thread \\rv . ct_in_state activatable\" @@ -91,28 +95,15 @@ lemma stit_activatable[Schedule_AI_assms]: elim!: pred_tcb_weaken_strongerE) done -lemma stt_invs [wp,Schedule_AI_assms]: - "\invs\ switch_to_thread t' \\_. invs\" - apply (simp add: switch_to_thread_def) - apply wp - apply (simp add: trans_state_update[symmetric] del: trans_state_update) - apply (rule_tac Q'="\_. invs and tcb_at t'" in hoare_strengthen_post, wp) - apply (clarsimp simp: invs_def valid_state_def valid_idle_def - valid_irq_node_def valid_machine_state_def) - apply (fastforce simp: cur_tcb_def obj_at_def - elim: valid_pspace_eqI ifunsafe_pspaceI) - apply wp+ - apply clarsimp - apply (simp add: is_tcb_def) - done -end +lemma arch_stt_scheduler_action [wp, Schedule_AI_assms]: + "\\s. P (scheduler_action s)\ arch_switch_to_thread t' \\_ s. P (scheduler_action s)\" + by (wpsimp simp: arch_switch_to_thread_def) -interpretation Schedule_AI_U?: Schedule_AI_U - proof goal_cases - interpret Arch . - case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) - qed +lemma arch_stit_scheduler_action [wp, Schedule_AI_assms]: + "\\s. P (scheduler_action s)\ arch_switch_to_idle_thread \\_ s. P (scheduler_action s)\" + by (wpsimp simp: arch_switch_to_idle_thread_def) + +end interpretation Schedule_AI?: Schedule_AI proof goal_cases diff --git a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy index f3dd14be84..c193451253 100644 --- a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy @@ -155,7 +155,7 @@ lemma retype_ret_valid_caps_captable[Untyped_AI_assms]: \ range_cover ptr sz (obj_bits_api CapTableObject us) n \ ptr \ 0 \ \ \y\{0..kheap := foldr (\p kh. kh(p \ default_object CapTableObject dev us)) (map (\p. ptr_add ptr (p * 2 ^ obj_bits_api CapTableObject us)) [0..kheap := foldr (\p kh. kh(p \ default_object CapTableObject dev us (cur_domain s))) (map (\p. ptr_add ptr (p * 2 ^ obj_bits_api CapTableObject us)) [0.. \ CNodeCap (ptr_add ptr (y * 2 ^ obj_bits_api CapTableObject us)) us []" by ((clarsimp simp:valid_cap_def default_object_def cap_aligned_def cte_level_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def @@ -168,8 +168,8 @@ lemma retype_ret_valid_caps_aobj[Untyped_AI_assms]: \pspace_no_overlap_range_cover ptr sz s \ x6 \ ASIDPoolObj \ range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \ ptr \ 0\ \ \y\{0..kheap := foldr (\p kh. kh(p \ default_object (ArchObject x6) dev us)) (map (\p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0.. \ ArchObjectCap (ARM_A.arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)" + \kheap := foldr (\p kh. kh(p \ default_object (ArchObject x6) dev us (cur_domain s))) (map (\p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0.. \ ArchObjectCap (arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)" apply (rename_tac aobject_type us n) apply (case_tac aobject_type) by (clarsimp simp: valid_cap_def default_object_def cap_aligned_def @@ -521,9 +521,8 @@ lemma nonempty_table_caps_of[Untyped_AI_assms]: lemma nonempty_default[simp, Untyped_AI_assms]: - "tp \ Untyped \ \ nonempty_table S (default_object tp dev us)" - apply (case_tac tp, simp_all add: default_object_def nonempty_table_def - a_type_def) + "tp \ Untyped \ \ nonempty_table S (default_object tp dev us d)" + apply (case_tac tp, simp_all add: default_object_def nonempty_table_def a_type_def) apply (rename_tac aobject_type) apply (case_tac aobject_type, simp_all add: default_arch_object_def) apply (simp_all add: empty_table_def pde_ref_def valid_pde_mappings_def) diff --git a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy index f8c735edaa..d9bd9887e6 100644 --- a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy @@ -621,15 +621,11 @@ lemma invoke_cnode_valid_pdpt_objs[wp]: apply (wp get_cap_wp | wpc | simp split del: if_split)+ done -crunch invoke_tcb +crunch invoke_tcb, invoke_domain for valid_pdpt_objs[wp]: "valid_pdpt_objs" (wp: check_cap_inv crunch_wps simp: crunch_simps ignore: check_cap_at) -lemma invoke_domain_valid_pdpt_objs[wp]: - "\valid_pdpt_objs\ invoke_domain t d \\rv. valid_pdpt_objs\" - by (simp add: invoke_domain_def | wp)+ - crunch set_extra_badge, transfer_caps_loop for valid_pdpt_objs[wp]: "valid_pdpt_objs" (rule: transfer_caps_loop_pres) @@ -1498,11 +1494,11 @@ lemma invocation_duplicates_valid_exst_update[simp]: apply (clarsimp simp add: invocation_duplicates_valid_def pti_duplicates_valid_def page_inv_duplicates_valid_def page_inv_entries_safe_def split: sum.splits invocation.splits arch_invocation.splits kernel_object.splits page_table_invocation.splits page_invocation.splits)+ done - lemma set_thread_state_duplicates_valid[wp]: "\invocation_duplicates_valid i\ set_thread_state t st \\rv. invocation_duplicates_valid i\" - apply (simp add: set_thread_state_def set_object_def get_object_def) - apply (wp|simp)+ + apply (simp add: set_thread_state_def set_thread_state_act_def set_scheduler_action_def + get_thread_state_def thread_get_def set_object_def get_object_def) + apply wpsimp apply (clarsimp simp: invocation_duplicates_valid_def pti_duplicates_valid_def page_inv_duplicates_valid_def page_inv_entries_safe_def Let_def @@ -1511,7 +1507,7 @@ lemma set_thread_state_duplicates_valid[wp]: page_table_invocation.split page_invocation.split sum.split ) - apply (auto simp add: obj_at_def page_inv_entries_safe_def) + apply (auto simp add: obj_at_def page_inv_entries_safe_def) done lemma handle_invocation_valid_pdpt[wp]: @@ -1525,22 +1521,21 @@ lemma handle_invocation_valid_pdpt[wp]: (auto simp: ct_in_state_def elim: st_tcb_ex_cap) -crunch handle_event, activate_thread,switch_to_thread, - switch_to_idle_thread +crunch handle_event, activate_thread, switch_to_thread, + switch_to_idle_thread, schedule_choose_new_thread for valid_pdpt[wp]: "valid_pdpt_objs" (simp: crunch_simps wp: crunch_wps OR_choice_weak_wp select_ext_weak_wp ignore: without_preemption getActiveIRQ resetTimer ackInterrupt getFAR getDFSR getIFSR OR_choice set_scheduler_action clearExMonitor) -lemma schedule_valid_pdpt[wp]: "\valid_pdpt_objs\ schedule :: (unit,unit) s_monad \\_. valid_pdpt_objs\" - apply (simp add: schedule_def allActiveTCBs_def) - apply wpsimp - done +lemma schedule_valid_pdpt[wp]: + "schedule \valid_pdpt_objs\" + unfolding schedule_def by (wpsimp wp: hoare_drop_imps) lemma call_kernel_valid_pdpt[wp]: "\invs and (\s. e \ Interrupt \ ct_running s) and valid_pdpt_objs\ - (call_kernel e) :: (unit,unit) s_monad + call_kernel e \\_. valid_pdpt_objs\" apply (cases e, simp_all add: call_kernel_def) apply (rule hoare_pre) diff --git a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy index 00ae764be0..009c6024bf 100644 --- a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy @@ -4952,7 +4952,7 @@ lemma invs_aligned_pdD: lemma valid_vspace_obj_default: assumes tyunt: "ty \ Structures_A.apiobject_type.Untyped" - shows "ArchObj ao = default_object ty dev us \ valid_vspace_obj ao s'" + shows "ArchObj ao = default_object ty dev us d \ valid_vspace_obj ao s'" apply (cases ty, simp_all add: default_object_def tyunt) apply (simp add: valid_vspace_obj_default') done