From d24eaabbc54e3fbfa47d33c965dcc870980861ef Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Thu, 6 Jul 2023 10:19:14 +1000 Subject: [PATCH] rt proof: rename whileLoop_wp' Signed-off-by: Corey Lewis --- .../ARM/ArchVSpaceEntries_AI.thy | 6 +- proof/invariant-abstract/Bits_AI.thy | 2 +- .../DetSchedDomainTime_AI.thy | 4 +- .../DetSchedSchedule_AI.thy | 64 +++++++++---------- proof/invariant-abstract/Deterministic_AI.thy | 6 +- proof/invariant-abstract/IpcCancel_AI.thy | 2 +- .../invariant-abstract/SchedContextInv_AI.thy | 4 +- proof/invariant-abstract/SchedContext_AI.thy | 26 ++++---- proof/refine/ARM/IpcCancel_R.thy | 6 +- proof/refine/ARM/Ipc_R.thy | 4 +- proof/refine/ARM/Schedule_R.thy | 12 ++-- proof/refine/RISCV64/IpcCancel_R.thy | 6 +- proof/refine/RISCV64/Ipc_R.thy | 4 +- proof/refine/RISCV64/Schedule_R.thy | 12 ++-- proof/refine/RISCV64/Syscall_R.thy | 2 +- 15 files changed, 80 insertions(+), 80 deletions(-) diff --git a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy index 0bb8663a0e..5000e4b9ed 100644 --- a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy @@ -430,14 +430,14 @@ lemma as_user_valid_pdpt_objs[wp]: crunch valid_pdpt_objs[wp]: send_signal, send_ipc "valid_pdpt_objs" (wp: get_sched_context_wp mapM_wp' maybeM_inv hoare_vcg_if_lift2 hoare_drop_imps - transfer_caps_loop_pres whileLoop_wp' + transfer_caps_loop_pres whileLoop_valid_inv simp: zipWithM_x_mapM ignore: set_thread_state_act set_object test_reschedule) crunch valid_pdpt_objs[wp]: cancel_all_ipc, cancel_all_signals, unbind_maybe_notification, sched_context_maybe_unbind_ntfn, reply_unlink_tcb, sched_context_unbind_all_tcbs, sched_context_unbind_ntfn "valid_pdpt_objs" - (wp: maybeM_inv hoare_drop_imp mapM_x_wp' whileLoop_wp' ignore: tcb_release_remove + (wp: maybeM_inv hoare_drop_imp mapM_x_wp' whileLoop_valid_inv ignore: tcb_release_remove simp: crunch_simps is_round_robin_def) crunch valid_pdpt_objs[wp]: @@ -1150,7 +1150,7 @@ crunch valid_pdpt_objs[wp]: end_timeslice "valid_pdpt_objs::det_state \ _" - (wp: hoare_drop_imps hoare_vcg_if_lift2 whileLoop_wp' hoare_vcg_all_lift + (wp: hoare_drop_imps hoare_vcg_if_lift2 whileLoop_valid_inv hoare_vcg_all_lift simp: Let_def ignore: tcb_release_remove) lemma perform_invocation_valid_pdpt[wp]: diff --git a/proof/invariant-abstract/Bits_AI.thy b/proof/invariant-abstract/Bits_AI.thy index 8cd6b31c59..f95be2e021 100644 --- a/proof/invariant-abstract/Bits_AI.thy +++ b/proof/invariant-abstract/Bits_AI.thy @@ -8,7 +8,7 @@ theory Bits_AI imports ArchBits_AI begin -lemmas crunch_wps = hoare_drop_imps mapM_wp' mapM_x_wp' whileLoop_wp' +lemmas crunch_wps = hoare_drop_imps mapM_wp' mapM_x_wp' whileLoop_valid_inv lemmas crunch_simps = split_def whenE_def unlessE_def Let_def if_fun_split assertE_def zipWithM_mapM zipWithM_x_mapM diff --git a/proof/invariant-abstract/DetSchedDomainTime_AI.thy b/proof/invariant-abstract/DetSchedDomainTime_AI.thy index 20ea64709f..34f046d77c 100644 --- a/proof/invariant-abstract/DetSchedDomainTime_AI.thy +++ b/proof/invariant-abstract/DetSchedDomainTime_AI.thy @@ -106,7 +106,7 @@ crunches reply_remove, sched_context_unbind_tcb, sched_context_zero_refill_max (wp: hoare_drop_imps get_simple_ko_wp) crunch domain_list_inv[wp]: cancel_all_ipc, cancel_all_signals "\s. P (domain_list s)" - (wp: hoare_drop_imps mapM_x_wp' whileLoop_wp') + (wp: hoare_drop_imps mapM_x_wp' whileLoop_valid_inv) crunch domain_list_inv[wp]: finalise_cap "\s::det_state. P (domain_list s)" (wp: crunch_wps maybeM_inv dxo_wp_weak select_inv simp: crunch_simps) @@ -204,7 +204,7 @@ crunches set_priority, restart, sched_context_bind_tcb,sched_context_bind_ntfn, sched_context_unbind_reply, sched_context_yield_to for domain_list_inv[wp]: "\s. P (domain_list s)" - (wp: hoare_drop_imps mapM_wp' maybeM_inv whileLoop_wp' simp: crunch_simps) + (wp: hoare_drop_imps mapM_wp' maybeM_inv whileLoop_valid_inv simp: crunch_simps) context DetSchedDomainTime_AI begin diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 24bd7bb9a0..191f706a1c 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -3668,7 +3668,7 @@ lemma refill_unblock_check_valid_sched_misc[wp]: (ready_queues s) (release_queue s) (scheduler_action s) (etcbs_of s) (tcb_sts_of s) (tcb_scps_of s) (tcb_faults_of s) (sc_replies_of s)\" unfolding refill_unblock_check_defs - apply (wpsimp wp: hoare_drop_imp whileLoop_wp') + apply (wpsimp wp: hoare_drop_imp whileLoop_valid_inv) done lemma refill_unblock_check_valid_blocked_except_set[wp]: @@ -3676,7 +3676,7 @@ lemma refill_unblock_check_valid_blocked_except_set[wp]: refill_unblock_check sc_ptr \\rv. valid_blocked_except_set S\" unfolding refill_unblock_check_defs update_sched_context_set_refills_rewrite - apply (wpsimp wp: set_refills_wp get_refills_wp is_round_robin_wp whileLoop_wp' + apply (wpsimp wp: set_refills_wp get_refills_wp is_round_robin_wp whileLoop_valid_inv | fastforce simp: vs_all_heap_simps valid_blocked_except_set_2_def valid_blocked_thread_def obj_at_def)+ done @@ -3720,7 +3720,7 @@ method merge_refills_simple method refill_head_overlapping_loop_simple = ((clarsimp simp: refill_head_overlapping_loop_def)? - , wpsimp wp: whileLoop_wp' set_refills_wp get_refills_wp + , wpsimp wp: whileLoop_valid_inv set_refills_wp get_refills_wp simp: merge_refills_def round_robin_def refill_pop_head_def sc_valid_refills_def update_sched_context_set_refills_rewrite update_refill_hd_rewrite vs_all_heap_simps obj_at_def) @@ -3816,7 +3816,7 @@ lemma refill_unblock_check_is_refill_sufficient[wp]: \rule hoare_seq_ext_skip, solves wpsimp, clarsimp?\) apply (cases "sc_ptr' \ sc_ptr") - apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: merge_refills_def refill_pop_head_def head_insufficient_loop_def refill_head_overlapping_loop_def non_overlapping_merge_refills_def vs_all_heap_simps update_refill_hd_rewrite update_sched_context_set_refills_rewrite) @@ -3864,7 +3864,7 @@ lemma merge_refills_is_refill_ready: lemma refill_head_overlapping_is_refill_ready: "refill_head_overlapping_loop sc_ptr' \is_refill_ready sc_ptr\" apply (clarsimp simp: refill_head_overlapping_loop_def) - apply (wpsimp wp: whileLoop_wp'; fastforce?) + apply (wpsimp wp: whileLoop_valid_inv; fastforce?) apply (wpsimp wp: merge_refills_is_refill_ready) done @@ -3985,7 +3985,7 @@ lemma refill_unblock_check_bounded_release_time: lemma refill_unblock_check_is_active_sc_at[wp]: "refill_unblock_check sc_ptr \\s. Q (is_active_sc scp s)\" apply (clarsimp simp: refill_unblock_check_defs) - apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: update_sched_context_set_refills_rewrite | clarsimp simp: vs_all_heap_simps active_sc_def obj_at_kh_kheap_simps pred_map_simps)+ done @@ -4037,7 +4037,7 @@ lemma refill_head_overlapping_loop_refills_sum: apply (clarsimp simp: refill_head_overlapping_loop_def) apply (cases "sc_ptr'\sc_ptr") apply refill_head_overlapping_loop_simple - apply (wpsimp wp: whileLoop_wp'; fastforce?) + apply (wpsimp wp: whileLoop_valid_inv; fastforce?) apply (wpsimp wp: merge_refills_refills_sum) apply (fastforce intro!: refill_head_overlapping_true_imp_length_at_least_two simp: vs_all_heap_simps) @@ -4223,7 +4223,7 @@ lemma refill_head_overlapping_loop_length: "refill_head_overlapping_loop sc_ptr' \\s. pred_map (\cfg. length (scrc_refills cfg) \ scrc_refill_max cfg) (sc_refill_cfgs_of s) sc_ptr\" apply (clarsimp simp: refill_head_overlapping_loop_def) - apply (wpsimp wp: whileLoop_wp'; fastforce?) + apply (wpsimp wp: whileLoop_valid_inv; fastforce?) apply merge_refills_simple apply (frule refill_head_overlapping_true_imp_length_at_least_two) apply (clarsimp simp: vs_all_heap_simps) @@ -4318,7 +4318,7 @@ lemma refill_head_overlapping_loop_window: refill_head_overlapping_loop sc_ptr' \\_ s. pred_map (\cfg. window (scrc_refills cfg) (scrc_period cfg)) (sc_refill_cfgs_of s) sc_ptr\" apply (clarsimp simp: refill_head_overlapping_loop_def) - apply (wpsimp wp: whileLoop_wp'; fastforce?) + apply (wpsimp wp: whileLoop_valid_inv; fastforce?) apply merge_refills_simple apply (clarsimp simp: window_def last_tl tl_Nil) done @@ -4336,7 +4336,7 @@ lemma refill_unblock_check_valid_refills[wp]: apply (rule hoare_seq_ext[OF _ gets_sp]) apply (case_tac "sc_ptr \ p") - apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: merge_refills_def refill_pop_head_def head_insufficient_loop_def refill_head_overlapping_loop_def non_overlapping_merge_refills_def vs_all_heap_simps update_refill_hd_rewrite update_sched_context_set_refills_rewrite) @@ -4531,21 +4531,21 @@ lemma refill_budget_check_round_robin_cur_sc_active[wp]: method handle_overrun_loop_body_simple = ((clarsimp simp: handle_overrun_loop_body_def)? - , wpsimp wp: whileLoop_wp' set_refills_wp get_refills_wp + , wpsimp wp: whileLoop_valid_inv set_refills_wp get_refills_wp simp: refill_pop_head_def vs_all_heap_simps obj_at_def refill_single_def refill_size_def update_sched_context_set_refills_rewrite update_refill_hd_rewrite schedule_used_defs) method handle_overrun_loop_simple = ((clarsimp simp: handle_overrun_loop_def)? - , wpsimp wp: whileLoop_wp' set_refills_wp get_refills_wp + , wpsimp wp: whileLoop_valid_inv set_refills_wp get_refills_wp simp: handle_overrun_loop_body_def merge_refills_def round_robin_def refill_pop_head_def sc_valid_refills_def vs_all_heap_simps obj_at_def refill_budget_check_defs update_sched_context_set_refills_rewrite schedule_used_defs) method head_insufficient_loop_simple = ((clarsimp simp: head_insufficient_loop_def)? - , wpsimp wp: whileLoop_wp' set_refills_wp get_refills_wp + , wpsimp wp: whileLoop_valid_inv set_refills_wp get_refills_wp simp: non_overlapping_merge_refills_def refill_pop_head_def schedule_used_defs update_sched_context_set_refills_rewrite update_refill_hd_rewrite , clarsimp simp: vs_all_heap_simps obj_at_def sc_valid_refills_def round_robin_def @@ -4586,7 +4586,7 @@ lemma refill_budget_check_valid_sched_misc[wp]: (etcbs_of s) (tcb_sts_of s) (tcb_scps_of s) (tcb_faults_of s) (sc_replies_of s) (ep_send_qs_of s) (ep_recv_qs_of s)\" unfolding refill_budget_check_defs schedule_used_defs - apply (wpsimp wp: hoare_drop_imp whileLoop_wp') + apply (wpsimp wp: hoare_drop_imp whileLoop_valid_inv) done lemma commit_time_is_active_sc[wp]: @@ -9553,7 +9553,7 @@ lemma handle_overrun_loop_nonzero_refills: "handle_overrun_loop usage \\s. pred_map (\cfg. scrc_refills cfg \ []) (sc_refill_cfgs_of s) sc_ptr\" apply (clarsimp simp: handle_overrun_loop_def) - apply (wpsimp wp: whileLoop_wp' handle_overrun_loop_body_nonzero_refills) + apply (wpsimp wp: whileLoop_valid_inv handle_overrun_loop_body_nonzero_refills) done lemma handle_overrun_loop_body_refills_unat_sum_equals_budget: @@ -10512,11 +10512,11 @@ lemma refill_budget_check_valid_refills[wp]: apply (rule_tac B="\_ s. valid_refills sc_ptr s \ robin = round_robin csc_ptr s \ cur_sc s = csc_ptr" in hoare_seq_ext[rotated]) - apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: refill_budget_check_defs update_sched_context_set_refills_rewrite schedule_used_defs | fastforce simp: obj_at_def vs_all_heap_simps )+)[1] - apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: refill_budget_check_defs update_sched_context_set_refills_rewrite schedule_used_defs | fastforce simp: obj_at_def vs_all_heap_simps)+)[1] @@ -11151,11 +11151,11 @@ lemma refill_budget_check_refill_ready_offset_ready_and_sufficient: \ robin = round_robin csc_ptr s \ cur_sc s = csc_ptr" in hoare_seq_ext[rotated]) - apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: refill_budget_check_defs update_sched_context_set_refills_rewrite schedule_used_defs | fastforce simp: obj_at_def vs_all_heap_simps )+)[1] - apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: refill_budget_check_defs update_sched_context_set_refills_rewrite schedule_used_defs | fastforce simp: obj_at_def vs_all_heap_simps)+)[1] @@ -11265,11 +11265,11 @@ lemma refill_budget_check_is_refill_sufficient: apply (rule_tac B="\_ s. is_refill_sufficient 0 sc_ptr s \ robin = round_robin csc_ptr s \ cur_sc s = csc_ptr" in hoare_seq_ext[rotated]) - apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: refill_budget_check_defs update_sched_context_set_refills_rewrite schedule_used_defs | fastforce simp: obj_at_def vs_all_heap_simps )+)[1] - apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: refill_budget_check_defs update_sched_context_set_refills_rewrite schedule_used_defs | fastforce simp: obj_at_def vs_all_heap_simps)+)[1] @@ -11493,7 +11493,7 @@ lemma valid_state_sym_refs[dest]: "valid_state s \ sym_refs (sta lemma refill_budget_check_active_sc_tcb_at[wp]: "refill_budget_check usage \\s. P (active_sc_tcb_at t s)\" unfolding refill_budget_check_defs schedule_used_defs - apply (wpsimp wp: hoare_drop_imp whileLoop_wp') + apply (wpsimp wp: hoare_drop_imp whileLoop_valid_inv) done lemma refill_budget_check_active_sc_tcb_at': @@ -11720,7 +11720,7 @@ lemma refill_budget_check_not_active_sc[wp]: apply handle_overrun_loop_simple apply (rule hoare_seq_ext_skip, solves wpsimp, clarsimp?)+ apply (rule hoare_seq_ext_skip) - apply (wpsimp wp: hoare_drop_imp whileLoop_wp' set_refills_wp get_refills_wp + apply (wpsimp wp: hoare_drop_imp whileLoop_valid_inv set_refills_wp get_refills_wp update_sched_context_wp simp: obj_at_def vs_all_heap_simps schedule_used_defs) apply head_insufficient_loop_simple @@ -11798,11 +11798,11 @@ lemma refill_budget_check_bounded_release_time: apply (rule_tac B="\_ s. bounded_release_time sc_ptr s \ robin = round_robin csc_ptr s \ cur_sc s = csc_ptr" in hoare_seq_ext[rotated]) - apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: refill_budget_check_defs update_sched_context_set_refills_rewrite schedule_used_defs | fastforce simp: obj_at_def vs_all_heap_simps )+)[1] - apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply ((wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: refill_budget_check_defs update_sched_context_set_refills_rewrite schedule_used_defs | fastforce simp: obj_at_def vs_all_heap_simps)+)[1] @@ -12061,7 +12061,7 @@ lemma refill_unblock_check_refill_ready_no_overflow_sc: refill_unblock_check sc_ptr \\_ s. pred_map (refill_ready_no_overflow_sc usage curtime) (sc_refill_cfgs_of s) sc_ptr'\" unfolding refill_unblock_check_defs refill_ready_no_overflow_def merge_refill_def - apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' is_round_robin_wp + apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv is_round_robin_wp simp: vs_all_heap_simps obj_at_def update_sched_context_set_refills_rewrite) done @@ -14492,7 +14492,7 @@ lemma valid_sched_active_reply_scs[simp,elim!]: lemma refill_unblock_check_active_if_bound_sc_tcb_at[wp]: "refill_unblock_check scp \active_if_bound_sc_tcb_at t\" unfolding refill_unblock_check_def refill_head_overlapping_loop_def - apply (wpsimp wp: whileLoop_wp' set_refills_wp get_refills_wp + apply (wpsimp wp: whileLoop_valid_inv set_refills_wp get_refills_wp simp: merge_refills_def update_refill_hd_rewrite refill_pop_head_def update_sched_context_set_refills_rewrite) apply (erule disjE) @@ -15279,7 +15279,7 @@ lemma complete_signal_valid_sched: lemma refill_unblock_check_ko_at_endoint[wp]: "refill_unblock_check sc_ptr \\s. ko_at (Endpoint ep) ep_ptr s\" apply (clarsimp simp: refill_unblock_check_def refill_head_overlapping_loop_def) - by (wpsimp wp: get_refills_wp set_refills_wp is_round_robin_wp whileLoop_wp' + by (wpsimp wp: get_refills_wp set_refills_wp is_round_robin_wp whileLoop_valid_inv simp: merge_refills_def update_refill_hd_rewrite refill_pop_head_def update_sched_context_set_refills_rewrite obj_at_def) @@ -16800,7 +16800,7 @@ lemma check_budget_sc_tcb_sc_at[wp]: handle_timeout_def refill_budget_check_defs refill_reset_rr_def update_refill_tl_def update_sched_context_set_refills_rewrite schedule_used_defs apply clarsimp - apply (wpsimp wp: hoare_drop_imps send_fault_ipc_sc_tcb_sc_at hoare_vcg_if_lift2 whileLoop_wp' + apply (wpsimp wp: hoare_drop_imps send_fault_ipc_sc_tcb_sc_at hoare_vcg_if_lift2 whileLoop_valid_inv simp: Let_def) done @@ -18184,7 +18184,7 @@ lemma refill_budget_check_sc_refill_max_sc_at: ; clarsimp simp: sc_at_pred_n_def obj_at_def) apply (rule hoare_seq_ext_skip, solves wpsimp)+ apply (rule hoare_seq_ext_skip) - apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: obj_at_def merge_refills_def refill_pop_head_def sc_at_pred_n_def update_sched_context_set_refills_rewrite update_refill_hd_rewrite) apply (head_insufficient_loop_simple @@ -21964,7 +21964,7 @@ lemma refill_unblock_check_cur_sc_offset_ready[wp]: refill_unblock_check scp \\_ s. cur_sc_active s \ cur_sc_offset_ready (consumed_time s) s\" unfolding refill_unblock_check_defs merge_refill_def - apply (wpsimp wp: whileLoop_wp' update_sched_context_wp get_refills_wp) + apply (wpsimp wp: whileLoop_valid_inv update_sched_context_wp get_refills_wp) apply (clarsimp simp: vs_all_heap_simps obj_at_def refill_ready_no_overflow_def split: if_split_asm) apply (wpsimp wp: update_sched_context_wp get_refills_wp)+ @@ -21978,7 +21978,7 @@ lemma refill_unblock_check_cur_sc_offset_sufficient[wp]: unfolding refill_unblock_check_defs apply (rule_tac Q="\_ s. scp \ cur_sc s \ (cur_sc_active s \ cur_sc_offset_sufficient (consumed_time s) s)" in hoare_strengthen_post) - apply (wpsimp wp: whileLoop_wp' update_sched_context_wp get_refills_wp) + apply (wpsimp wp: whileLoop_valid_inv update_sched_context_wp get_refills_wp) apply (clarsimp simp: vs_all_heap_simps split: if_split_asm) apply (wpsimp wp: update_sched_context_wp get_refills_wp)+ apply (clarsimp simp: vs_all_heap_simps obj_at_def)+ diff --git a/proof/invariant-abstract/Deterministic_AI.thy b/proof/invariant-abstract/Deterministic_AI.thy index 0d584be7cf..5b0d0833e5 100644 --- a/proof/invariant-abstract/Deterministic_AI.thy +++ b/proof/invariant-abstract/Deterministic_AI.thy @@ -3956,7 +3956,7 @@ crunches sched_context_unbind_ntfn, sched_context_maybe_unbind_ntfn, sched_context_unbind_yield_from, cancel_all_ipc, thread_set, reply_remove_tcb for valid_list[wp]: valid_list - (wp: mapM_x_wp' hoare_drop_imp whileLoop_wp' simp: is_round_robin_def crunch_simps) + (wp: mapM_x_wp' hoare_drop_imp whileLoop_valid_inv simp: is_round_robin_def crunch_simps) crunch all_but_exst[wp]: update_work_units "all_but_exst P" @@ -4063,7 +4063,7 @@ crunch valid_list[wp]: do_fault_transfer valid_list (wp: mapM_wp hoare_drop_imp ignore: make_fault_msg) crunch valid_list[wp]: transfer_caps,do_normal_transfer,do_ipc_transfer,refill_unblock_check valid_list - (wp: mapM_wp hoare_drop_imp whileLoop_wp') + (wp: mapM_wp hoare_drop_imp whileLoop_valid_inv) lemma send_ipc_valid_list[wp]: "send_ipc block call badge can_grant can_reply_grant can_donate thread epptr \valid_list\" @@ -4089,7 +4089,7 @@ crunches set_refills,refill_size, schedule_used lemma refill_budget_check_valid_list[wp]: "refill_budget_check usage \valid_list\" unfolding refill_budget_check_defs - apply (wpsimp wp: whileLoop_wp' hoare_drop_imps) + apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps) done lemma refill_budget_check_round_robin_valid_list[wp]: diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index 4169903b15..7d8f2dde33 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -2400,7 +2400,7 @@ lemma refill_unblock_check_obj_at_impossible': refill_unblock_check sc_opt \\s. P (obj_at P' p s)\" unfolding refill_unblock_check_def - by (wpsimp wp: whileLoop_wp' update_sched_context_wp get_refills_wp + by (wpsimp wp: whileLoop_valid_inv update_sched_context_wp get_refills_wp simp: refill_head_overlapping_loop_def merge_refills_def update_refill_hd_def refill_pop_head_def is_round_robin_def | clarsimp elim!: rsubst[where P=P] simp: obj_at_def)+ diff --git a/proof/invariant-abstract/SchedContextInv_AI.thy b/proof/invariant-abstract/SchedContextInv_AI.thy index 49d942d786..21fb8ac576 100644 --- a/proof/invariant-abstract/SchedContextInv_AI.thy +++ b/proof/invariant-abstract/SchedContextInv_AI.thy @@ -1486,7 +1486,7 @@ lemma set_refills_active_sc_at[wp]: lemma refill_unblock_check_active_sc_at[wp]: "refill_unblock_check sc_ptr \\s. Q (active_sc_at sc_ptr s)\" apply (clarsimp simp: refill_unblock_check_defs simp del: update_refill_hd_def) - apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp' + apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv simp: update_refill_hd_rewrite update_sched_context_set_refills_rewrite active_sc_at_def) done @@ -1580,7 +1580,7 @@ lemma set_sc_obj_ref_active: crunches commit_time for sc_active: "active_sc_at sc_ptr" - (wp: set_sc_obj_ref_active whileLoop_wp' crunch_wps simp: crunch_simps) + (wp: set_sc_obj_ref_active whileLoop_valid_inv crunch_wps simp: crunch_simps) lemma sc_badge_update_active[wp]: "set_sc_obj_ref sc_badge_update sc_ptr x \active_sc_at p'\" diff --git a/proof/invariant-abstract/SchedContext_AI.thy b/proof/invariant-abstract/SchedContext_AI.thy index f45bbf9817..b016fa1880 100644 --- a/proof/invariant-abstract/SchedContext_AI.thy +++ b/proof/invariant-abstract/SchedContext_AI.thy @@ -177,7 +177,7 @@ lemma update_refill_tl_valid_objs[wp]: lemma refill_unblock_check_valid_objs[wp]: "refill_unblock_check sc_ptr \valid_objs\" - by (wpsimp wp: set_refills_valid_objs whileLoop_wp' get_refills_wp + by (wpsimp wp: set_refills_valid_objs whileLoop_valid_inv get_refills_wp hoare_drop_imps simp: refill_unblock_check_defs) @@ -208,7 +208,7 @@ lemma refill_pop_head_valid_objs[wp]: lemma head_insufficient_loop_valid_objs[wp]: "head_insufficient_loop usage \valid_objs\" unfolding head_insufficient_loop_def - by (wpsimp wp: whileLoop_wp' simp: non_overlapping_merge_refills_def update_refill_hd_def) + by (wpsimp wp: whileLoop_valid_inv simp: non_overlapping_merge_refills_def update_refill_hd_def) lemma schedule_used_valid_objs[wp]: "schedule_used sc_ptr new \valid_objs\" @@ -221,7 +221,7 @@ lemma handle_overrun_loop_valid_objs[wp]: "handle_overrun_loop usage \valid_objs\" unfolding handle_overrun_loop_def handle_overrun_loop_body_def refill_single_def refill_size_def update_refill_hd_def - apply (wpsimp wp: whileLoop_wp' + apply (wpsimp wp: whileLoop_valid_inv simp: valid_sched_context_def) done @@ -527,7 +527,7 @@ crunches head_insufficient_loop, handle_overrun_loop lemma refill_budget_check_if_live_then_nonz_cap[wp]: "refill_budget_check usage \if_live_then_nonz_cap\" - apply (wpsimp wp: whileLoop_wp' get_refills_wp hoare_drop_imps + apply (wpsimp wp: whileLoop_valid_inv get_refills_wp hoare_drop_imps hoare_vcg_all_lift hoare_vcg_if_lift2 simp: refill_budget_check_def update_refill_hd_def) done @@ -535,7 +535,7 @@ lemma refill_budget_check_if_live_then_nonz_cap[wp]: lemma refill_unblock_check_refs_of[wp]: "refill_unblock_check sc_ptr \\s. P (state_refs_of s)\" apply (wpsimp simp: refill_unblock_check_defs - wp: hoare_drop_imp whileLoop_wp') + wp: hoare_drop_imp whileLoop_valid_inv) apply (clarsimp simp: state_refs_of_def) done @@ -613,7 +613,7 @@ lemma refill_budget_check_invs[wp]: "refill_budget_check usage \invs\" unfolding refill_budget_check_def apply (wpsimp simp: refill_budget_check_defs - wp: hoare_drop_imp whileLoop_wp' hoare_vcg_if_lift2) + wp: hoare_drop_imp whileLoop_valid_inv hoare_vcg_if_lift2) done lemma update_sched_context_valid_irq_node [wp]: @@ -776,7 +776,7 @@ crunches head_insufficient_loop, handle_overrun_loop lemma refill_budget_check_valid_replies_pred[wp]: "refill_budget_check usage \ valid_replies_pred P \" apply (wpsimp simp: refill_budget_check_def - wp: get_refills_wp whileLoop_wp' hoare_drop_imps + wp: get_refills_wp whileLoop_valid_inv hoare_drop_imps hoare_vcg_all_lift hoare_vcg_if_lift2) done @@ -882,7 +882,7 @@ crunches handle_overrun_loop, head_insufficient_loop lemma refill_budget_check_bound_sc_tcb_at_ct[wp]: "refill_budget_check usage \\s. bound_sc_tcb_at P (cur_thread s) s\" unfolding refill_budget_check_def - apply (wpsimp wp: whileLoop_wp' get_refills_wp hoare_drop_imps hoare_vcg_all_lift + apply (wpsimp wp: whileLoop_valid_inv get_refills_wp hoare_drop_imps hoare_vcg_all_lift hoare_vcg_if_lift2) done @@ -897,7 +897,7 @@ lemma commit_time_bound_sc_tcb_at [wp]: lemma refill_unblock_check_bound_sc_tcb_at [wp]: "refill_unblock_check sc_ptr \\s. bound_sc_tcb_at ((=) (Some sc)) (cur_thread s) s\" unfolding refill_unblock_check_defs - apply (wpsimp wp: whileLoop_wp' get_refills_wp hoare_drop_imps) + apply (wpsimp wp: whileLoop_valid_inv get_refills_wp hoare_drop_imps) done crunches if_cond_refill_unblock_check @@ -996,7 +996,7 @@ crunches head_insufficient_loop, handle_overrun_loop lemma refill_budget_check_ct_in_state[wp]: "refill_budget_check usage \ ct_in_state t \" unfolding refill_budget_check_def - apply (wpsimp wp: whileLoop_wp' get_refills_wp hoare_drop_imps hoare_vcg_all_lift + apply (wpsimp wp: whileLoop_valid_inv get_refills_wp hoare_drop_imps hoare_vcg_all_lift hoare_vcg_if_lift2) done @@ -1011,7 +1011,7 @@ crunch ct_in_state[wp]: commit_time "ct_in_state t" lemma refill_unblock_check_ct_in_state[wp]: "refill_unblock_check csc \ ct_in_state t \" unfolding refill_unblock_check_defs - apply (wpsimp wp: whileLoop_wp' get_refills_wp hoare_drop_imps) + apply (wpsimp wp: whileLoop_valid_inv get_refills_wp hoare_drop_imps) done lemma switch_sched_context_ct_in_state[wp]: @@ -1714,7 +1714,7 @@ lemma refill_unblock_check_state_refs_of_ct[wp]: apply (clarsimp simp: state_refs_of_def obj_at_def intro!: ext elim!: rsubst[where P="\x. P x (cur_thread s)" for s])+ apply (wpsimp simp: set_refills_def - wp: update_sched_context_wp get_refills_wp whileLoop_wp') + wp: update_sched_context_wp get_refills_wp whileLoop_valid_inv) apply (clarsimp simp: state_refs_of_def obj_at_def intro!: ext elim!: rsubst[where P="\x. P x (cur_thread s)" for s])+ done @@ -1723,7 +1723,7 @@ lemma refill_unblock_check_it_ct[wp]: "refill_unblock_check scp \\s. P (idle_thread s) (cur_thread s)\" apply (wpsimp simp: refill_unblock_check_defs set_refills_def update_sched_context_def set_object_def - wp: get_refills_wp get_object_wp whileLoop_wp') + wp: get_refills_wp get_object_wp whileLoop_valid_inv) done lemma get_sc_refill_capacity_sp: diff --git a/proof/refine/ARM/IpcCancel_R.thy b/proof/refine/ARM/IpcCancel_R.thy index 31da846d47..e41df2d79d 100644 --- a/proof/refine/ARM/IpcCancel_R.thy +++ b/proof/refine/ARM/IpcCancel_R.thy @@ -3185,7 +3185,7 @@ lemma refillPopHead_valid_pspace'[wp]: refillPopHead scp \\_. valid_pspace'\" unfolding refillPopHead_def updateSchedContext_def - apply (wpsimp wp: whileLoop_wp') + apply (wpsimp wp: whileLoop_valid_inv) by (fastforce simp: obj_at'_def projectKOs valid_obj'_def refillNextIndex_def MIN_REFILLS_def valid_sched_context'_def valid_sched_context_size'_def scBits_simps objBits_simps dest!: opt_predD @@ -3194,7 +3194,7 @@ lemma refillPopHead_valid_pspace'[wp]: lemma refillUnblockCheck_ko_wp_at_not_live[wp]: "refillUnblockCheck scp \\s. P (ko_wp_at' (Not \ live') p' s)\" unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def - apply (wpsimp wp: whileLoop_wp' updateSchedContext_wp hoare_drop_imps + apply (wpsimp wp: whileLoop_valid_inv updateSchedContext_wp hoare_drop_imps simp: updateRefillHd_def refillPopHead_def) apply (clarsimp simp: ko_wp_at'_def obj_at'_def projectKOs runReaderT_def opt_map_red refillNextIndex_def @@ -3220,7 +3220,7 @@ lemma refillUnblockCheck_refs_of'[wp]: "refillUnblockCheck sc_ptr \\s. P (state_refs_of' s)\" unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def apply (wpsimp simp: updateRefillHd_def refillPopHead_def - wp: hoare_drop_imp whileLoop_wp' isRoundRobin_wp updateSchedContext_wp) + wp: hoare_drop_imp whileLoop_valid_inv isRoundRobin_wp updateSchedContext_wp) apply (clarsimp simp: runReaderT_def elim!: rsubst[where P=P]) apply (clarsimp simp: obj_at'_def projectKOs opt_map_red refillNextIndex_def) apply (fastforce simp: state_refs_of'_def get_refs_def2 ps_clear_upd objBits_simps option.case_eq_if diff --git a/proof/refine/ARM/Ipc_R.thy b/proof/refine/ARM/Ipc_R.thy index 94812d0393..1828e88c1e 100644 --- a/proof/refine/ARM/Ipc_R.thy +++ b/proof/refine/ARM/Ipc_R.thy @@ -5722,7 +5722,7 @@ lemma refillUnblockCheck_sym_heap_tcbSCs[wp]: \\_. sym_heap_tcbSCs\" supply opt_mapE [rule del] unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def - apply (wpsimp wp: whileLoop_wp' updateSchedContext_wp wp_del: use_corresK + apply (wpsimp wp: whileLoop_valid_inv updateSchedContext_wp wp_del: use_corresK simp: refillPopHead_def) apply (clarsimp simp: sym_heap_def obj_at'_def projectKOs ps_clear_upd opt_map_red projectKO_opt_tcb) apply (wpsimp wp: updateSchedContext_wp getCurTime_wp refillReady_wp isRoundRobin_wp @@ -5746,7 +5746,7 @@ lemma refillUnblockCheck_sym_heap_scReplies[wp]: \\_. sym_heap_scReplies\" supply opt_mapE [rule del] unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def - apply (wpsimp wp: whileLoop_wp' updateSchedContext_wp wp_del: use_corresK + apply (wpsimp wp: whileLoop_valid_inv updateSchedContext_wp wp_del: use_corresK simp: refillPopHead_def) apply (clarsimp simp: sym_heap_def obj_at'_def projectKOs ps_clear_upd opt_map_red projectKO_opt_reply) apply (drule_tac x=scp and y=p' in spec2) diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy index 3987044c8b..3815bdf64a 100644 --- a/proof/refine/ARM/Schedule_R.thy +++ b/proof/refine/ARM/Schedule_R.thy @@ -2402,7 +2402,7 @@ lemma refillUnblockCheck_valid_machine_state'[wp]: refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def refillPopHead_def updateSchedContext_def setReprogramTimer_def valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) - apply (wpsimp wp: whileLoop_wp' hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp + apply (wpsimp wp: whileLoop_valid_inv hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp hoare_drop_imps getRefillNext_wp) apply fastforce done @@ -2412,7 +2412,7 @@ lemma refillUnblockCheck_list_refs_of_replies'[wp]: apply (clarsimp simp: refillUnblockCheck_def valid_mdb'_def refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def refillPopHead_def updateSchedContext_def setReprogramTimer_def refillReady_def isRoundRobin_def) - apply (wpsimp wp: whileLoop_wp' hoare_drop_imps scActive_wp getRefillNext_wp + apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps scActive_wp getRefillNext_wp simp: o_def) done @@ -2596,7 +2596,7 @@ lemma refillBudgetCheck_valid_mdb'[wp]: lemma handleOverrunLoop_list_refs_of_replies'[wp]: "handleOverrunLoop usage \\s. sym_refs (list_refs_of_replies' s)\" apply (clarsimp simp: handleOverrunLoop_def) - apply (wpsimp wp: whileLoop_wp' hoare_drop_imps getRefillNext_wp + apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps getRefillNext_wp getRefillSize_wp refillFull_wp refillEmpty_wp simp: o_def handleOverrunLoopBody_def refillPopHead_def updateSchedContext_def scheduleUsed_def refillAddTail_def updateRefillHd_def setRefillTl_def @@ -2609,7 +2609,7 @@ lemma refillBudgetCheck_list_refs_of_replies'[wp]: setReprogramTimer_def refillReady_def isRoundRobin_def headInsufficientLoop_def nonOverlappingMergeRefills_def) apply (rule hoare_seq_ext_skip, solves wpsimp)+ - apply (wpsimp wp: whileLoop_wp' hoare_drop_imps refillFull_wp refillEmpty_wp getRefillNext_wp + apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps refillFull_wp refillEmpty_wp getRefillNext_wp getRefillSize_wp hoare_vcg_all_lift hoare_vcg_if_lift2 simp: o_def scheduleUsed_def refillAddTail_def setRefillHd_def updateRefillHd_def setRefillTl_def updateRefillTl_def updateSchedContext_def) @@ -2633,7 +2633,7 @@ lemma refillBudgetCheck_valid_idle'[wp]: lemma handleOverrunLoop_valid_machine_state'[wp]: "handleOverrunLoop usage \valid_machine_state'\" apply (clarsimp simp: handleOverrunLoop_def) - apply (wpsimp wp: whileLoop_wp' hoare_drop_imps getRefillNext_wp + apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps getRefillNext_wp getRefillSize_wp refillFull_wp refillEmpty_wp simp: handleOverrunLoopBody_def refillPopHead_def updateSchedContext_def scheduleUsed_def refillAddTail_def updateRefillHd_def setRefillTl_def @@ -2646,7 +2646,7 @@ lemma refillBudgetCheck_valid_machine_state'[wp]: setReprogramTimer_def refillReady_def isRoundRobin_def headInsufficientLoop_def nonOverlappingMergeRefills_def) apply (rule hoare_seq_ext_skip, solves wpsimp)+ - apply (wpsimp wp: whileLoop_wp' hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp hoare_drop_imps + apply (wpsimp wp: whileLoop_valid_inv hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp hoare_drop_imps refillFull_wp refillEmpty_wp getRefillNext_wp getRefillSize_wp simp: scheduleUsed_def refillAddTail_def setRefillTl_def updateRefillTl_def setRefillHd_def updateRefillHd_def updateSchedContext_def) diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy index 410829c891..1cb102e9cd 100644 --- a/proof/refine/RISCV64/IpcCancel_R.thy +++ b/proof/refine/RISCV64/IpcCancel_R.thy @@ -3146,7 +3146,7 @@ lemma refillPopHead_valid_pspace'[wp]: refillPopHead scp \\_. valid_pspace'\" unfolding refillPopHead_def updateSchedContext_def - apply (wpsimp wp: whileLoop_wp') + apply (wpsimp wp: whileLoop_valid_inv) by (fastforce simp: obj_at'_def valid_obj'_def refillNextIndex_def MIN_REFILLS_def valid_sched_context'_def valid_sched_context_size'_def scBits_simps objBits_simps dest!: opt_predD @@ -3155,7 +3155,7 @@ lemma refillPopHead_valid_pspace'[wp]: lemma refillUnblockCheck_ko_wp_at_not_live[wp]: "refillUnblockCheck scp \\s. P (ko_wp_at' (Not \ live') p' s)\" unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def - apply (wpsimp wp: whileLoop_wp' updateSchedContext_wp hoare_drop_imps + apply (wpsimp wp: whileLoop_valid_inv updateSchedContext_wp hoare_drop_imps simp: updateRefillHd_def refillPopHead_def) apply (clarsimp simp: ko_wp_at'_def obj_at'_def runReaderT_def opt_map_red refillNextIndex_def @@ -3181,7 +3181,7 @@ lemma refillUnblockCheck_refs_of'[wp]: "refillUnblockCheck sc_ptr \\s. P (state_refs_of' s)\" unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def apply (wpsimp simp: updateRefillHd_def refillPopHead_def - wp: hoare_drop_imp whileLoop_wp' isRoundRobin_wp updateSchedContext_wp) + wp: hoare_drop_imp whileLoop_valid_inv isRoundRobin_wp updateSchedContext_wp) apply (clarsimp simp: runReaderT_def elim!: rsubst[where P=P]) apply (clarsimp simp: obj_at'_def opt_map_red refillNextIndex_def) apply (fastforce simp: state_refs_of'_def get_refs_def2 ps_clear_upd objBits_simps option.case_eq_if diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 2f6a43aa88..018b43e740 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -5733,7 +5733,7 @@ lemma refillUnblockCheck_sym_heap_tcbSCs[wp]: refillUnblockCheck scp \\_. sym_heap_tcbSCs\" unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def - apply (wpsimp wp: whileLoop_wp' updateSchedContext_wp wp_del: use_corresK + apply (wpsimp wp: whileLoop_valid_inv updateSchedContext_wp wp_del: use_corresK simp: refillPopHead_def) apply (clarsimp simp: sym_heap_def obj_at'_def ps_clear_upd opt_map_red projectKO_opt_tcb) apply (wpsimp wp: updateSchedContext_wp getCurTime_wp refillReady_wp isRoundRobin_wp @@ -5756,7 +5756,7 @@ lemma refillUnblockCheck_sym_heap_scReplies[wp]: refillUnblockCheck scp \\_. sym_heap_scReplies\" unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def - apply (wpsimp wp: whileLoop_wp' updateSchedContext_wp wp_del: use_corresK + apply (wpsimp wp: whileLoop_valid_inv updateSchedContext_wp wp_del: use_corresK simp: refillPopHead_def) apply (clarsimp simp: sym_heap_def obj_at'_def ps_clear_upd opt_map_red projectKO_opt_reply) apply (drule_tac x=scp and y=p' in spec2) diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index b853dc42d9..b706c1475f 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -2360,7 +2360,7 @@ lemma refillUnblockCheck_valid_machine_state'[wp]: refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def refillPopHead_def updateSchedContext_def setReprogramTimer_def valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) - apply (wpsimp wp: whileLoop_wp' hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp + apply (wpsimp wp: whileLoop_valid_inv hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp hoare_drop_imps getRefillNext_wp) apply fastforce done @@ -2370,7 +2370,7 @@ lemma refillUnblockCheck_list_refs_of_replies'[wp]: apply (clarsimp simp: refillUnblockCheck_def valid_mdb'_def refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def refillPopHead_def updateSchedContext_def setReprogramTimer_def refillReady_def isRoundRobin_def) - apply (wpsimp wp: whileLoop_wp' hoare_drop_imps scActive_wp getRefillNext_wp + apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps scActive_wp getRefillNext_wp simp: o_def) done @@ -2553,7 +2553,7 @@ lemma refillBudgetCheck_valid_mdb'[wp]: lemma handleOverrunLoop_list_refs_of_replies'[wp]: "handleOverrunLoop usage \\s. sym_refs (list_refs_of_replies' s)\" apply (clarsimp simp: handleOverrunLoop_def) - apply (wpsimp wp: whileLoop_wp' hoare_drop_imps getRefillNext_wp + apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps getRefillNext_wp getRefillSize_wp refillFull_wp refillEmpty_wp simp: o_def handleOverrunLoopBody_def refillPopHead_def updateSchedContext_def scheduleUsed_def refillAddTail_def updateRefillHd_def setRefillTl_def @@ -2566,7 +2566,7 @@ lemma refillBudgetCheck_list_refs_of_replies'[wp]: setReprogramTimer_def refillReady_def isRoundRobin_def headInsufficientLoop_def nonOverlappingMergeRefills_def) apply (rule hoare_seq_ext_skip, solves wpsimp)+ - apply (wpsimp wp: whileLoop_wp' hoare_drop_imps refillFull_wp refillEmpty_wp getRefillNext_wp + apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps refillFull_wp refillEmpty_wp getRefillNext_wp getRefillSize_wp hoare_vcg_all_lift hoare_vcg_if_lift2 simp: o_def scheduleUsed_def refillAddTail_def setRefillHd_def updateRefillHd_def setRefillTl_def updateRefillTl_def updateSchedContext_def) @@ -2588,7 +2588,7 @@ lemma refillBudgetCheck_valid_idle'[wp]: lemma handleOverrunLoop_valid_machine_state'[wp]: "handleOverrunLoop usage \valid_machine_state'\" apply (clarsimp simp: handleOverrunLoop_def) - apply (wpsimp wp: whileLoop_wp' hoare_drop_imps getRefillNext_wp + apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps getRefillNext_wp getRefillSize_wp refillFull_wp refillEmpty_wp simp: handleOverrunLoopBody_def refillPopHead_def updateSchedContext_def scheduleUsed_def refillAddTail_def updateRefillHd_def setRefillTl_def @@ -2601,7 +2601,7 @@ lemma refillBudgetCheck_valid_machine_state'[wp]: setReprogramTimer_def refillReady_def isRoundRobin_def headInsufficientLoop_def nonOverlappingMergeRefills_def) apply (rule hoare_seq_ext_skip, solves wpsimp)+ - by (wpsimp wp: whileLoop_wp' hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp hoare_drop_imps + by (wpsimp wp: whileLoop_valid_inv hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp hoare_drop_imps refillFull_wp refillEmpty_wp getRefillNext_wp getRefillSize_wp simp: scheduleUsed_def refillAddTail_def setRefillTl_def updateRefillTl_def setRefillHd_def updateRefillHd_def updateSchedContext_def) diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 9b11f66236..cd8f329426 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -774,7 +774,7 @@ lemma ifConfRefillUnblockCheck_ko_at'_tcb[wp]: "ifCondRefillUnblockCheck scOpt act ast \\s. P (ko_at' (ko :: tcb) tcbPtr s)\" unfolding ifCondRefillUnblockCheck_def refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def updateSchedContext_def refillPopHead_def - by (wpsimp wp: whileLoop_wp' hoare_drop_imps) + by (wpsimp wp: whileLoop_valid_inv hoare_drop_imps) lemma doReplyTransfer_invs'[wp]: "\invs' and tcb_at' sender and reply_at' replyPtr and sch_act_simple\