From 6133838e7f5fc72b013d6185dcbbd1adfbcf433b Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 8 May 2024 21:09:51 +0930 Subject: [PATCH] fix trailing whitespace errors squash Signed-off-by: Michael McInerney --- proof/crefine/AARCH64/IpcCancel_C.thy | 4 ++-- proof/crefine/AARCH64/Refine_C.thy | 2 +- proof/crefine/AARCH64/Schedule_C.thy | 2 +- proof/refine/X64/Interrupt_R.thy | 2 +- proof/refine/X64/Ipc_R.thy | 4 ++-- proof/refine/X64/Schedule_R.thy | 2 +- 6 files changed, 8 insertions(+), 8 deletions(-) diff --git a/proof/crefine/AARCH64/IpcCancel_C.thy b/proof/crefine/AARCH64/IpcCancel_C.thy index 63f53551dc..b711de1a09 100644 --- a/proof/crefine/AARCH64/IpcCancel_C.thy +++ b/proof/crefine/AARCH64/IpcCancel_C.thy @@ -30,7 +30,7 @@ qed lemmas cready_queues_index_to_C_in_range = cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val] - + lemma cready_queues_index_to_C_inj: "\ cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; prio \ maxPriority; prio' \ maxPriority \ \ prio = prio' \ qdom = qdom'" @@ -670,7 +670,7 @@ lemma tcb_queue_prepend_ccorres: (\ctcb_queue_relation queue \queue\ \ \\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\) hs (tcbQueuePrepend queue tcbPtr) (Call tcb_queue_prepend_'proc)" (is "ccorres _ _ ?abs _ _ _ _") - supply if_split[split del] + supply if_split[split del] apply (cinit lift: tcb_') \ \cinit is not able to lift queue_' because queue_' is later modified in the C program\ apply (rule_tac xf'=queue_' in ccorres_abstract, ceqv, rename_tac cqueue) diff --git a/proof/crefine/AARCH64/Refine_C.thy b/proof/crefine/AARCH64/Refine_C.thy index 47dbcc0406..22686e0565 100644 --- a/proof/crefine/AARCH64/Refine_C.thy +++ b/proof/crefine/AARCH64/Refine_C.thy @@ -433,7 +433,7 @@ lemma handleSyscall_ccorres: apply (wpsimp wp: hoare_drop_imps) apply (simp | wpc - | wp hoare_drop_imp handleReply_sane handleReply_nonz_cap_to_ct schedule_invs' + | wp hoare_drop_imp handleReply_sane handleReply_nonz_cap_to_ct schedule_invs' | strengthen ct_active_not_idle'_strengthen invs_valid_objs_strengthen)+ apply (rule_tac Q="\rv. invs' and ct_active'" in hoare_post_imp, simp) apply (wp hy_invs') diff --git a/proof/crefine/AARCH64/Schedule_C.thy b/proof/crefine/AARCH64/Schedule_C.thy index 1b73cd7462..c8160479d2 100644 --- a/proof/crefine/AARCH64/Schedule_C.thy +++ b/proof/crefine/AARCH64/Schedule_C.thy @@ -105,7 +105,7 @@ lemma Arch_switchToThread_ccorres: lemma all_invs_but_ct_idle_or_in_cur_domain'_pspace_aligned': "all_invs_but_ct_idle_or_in_cur_domain' s \ pspace_aligned' s" by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def) - + lemma all_invs_but_ct_idle_or_in_cur_domain'_pspace_distinct': "all_invs_but_ct_idle_or_in_cur_domain' s \ pspace_distinct' s" by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def) diff --git a/proof/refine/X64/Interrupt_R.thy b/proof/refine/X64/Interrupt_R.thy index bef4dd79e2..9c696b7625 100644 --- a/proof/refine/X64/Interrupt_R.thy +++ b/proof/refine/X64/Interrupt_R.thy @@ -759,7 +759,7 @@ lemmas corres_eq_trivial = corres_Id[where f = h and g = h for h, simplified] lemma handleInterrupt_corres: "corres dc - einvs + einvs (invs' and (\s. intStateIRQTable (ksInterruptState s) irq \ IRQInactive)) (handle_interrupt irq) (handleInterrupt irq)" (is "corres dc ?P ?P' ?f ?g") diff --git a/proof/refine/X64/Ipc_R.thy b/proof/refine/X64/Ipc_R.thy index f2db2e3ba8..e7a0cd3f5b 100644 --- a/proof/refine/X64/Ipc_R.thy +++ b/proof/refine/X64/Ipc_R.thy @@ -2201,14 +2201,14 @@ lemma doReplyTransfer_corres: in corres_inst) apply (case_tac rvb, simp_all)[1] apply (rule corres_guard_imp) - apply (rule corres_split[OF setThreadState_corres]) + apply (rule corres_split[OF setThreadState_corres]) apply simp apply (fold dc_def, rule possibleSwitchTo_corres) apply simp apply (wp hoare_weak_lift_imp hoare_weak_lift_imp_conj set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at' sts_st_tcb' sts_valid_objs' - | simp + | simp | force simp: valid_sched_def valid_sched_action_def valid_tcb_state'_def)+ apply (rule corres_guard_imp) diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy index c4a48071b5..3b1d441901 100644 --- a/proof/refine/X64/Schedule_R.thy +++ b/proof/refine/X64/Schedule_R.thy @@ -1383,7 +1383,7 @@ lemma guarded_switch_to_corres: apply (rule switchToThread_corres) apply (force simp: st_tcb_at_tcb_at) apply (wp gts_st_tcb_at) - apply (force simp: st_tcb_at_tcb_at)+ + apply (force simp: st_tcb_at_tcb_at)+ done abbreviation "enumPrio \ [0.e.maxPriority]"