crefine: address Raf's comment and hopefully fix errors squash

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Sep 10, 2024 · ba8ac98 · ba8ac98
1 parent 668c4dd
commit ba8ac98
Show file tree

Hide file tree

Showing 18 changed files with 50 additions and 74 deletions.
diff --git a/proof/crefine/AARCH64/Syscall_C.thy b/proof/crefine/AARCH64/Syscall_C.thy
@@ -519,8 +519,6 @@ lemma handleDoubleFault_ccorres:
     apply (rule empty_fail_asUser)
     apply (simp add: getRestartPC_def)
    apply wp
-  apply clarsimp
-  apply (simp add: ThreadState_defs)
   apply (fastforce simp: valid_tcb_state'_def)
   done
 
@@ -895,7 +893,6 @@ lemma handleInvocation_ccorres:
                     apply auto[1]
                    apply clarsimp
                   apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)
-                  apply (simp add: ThreadState_defs mask_def)
                   apply (simp add: typ_heap_simps)
                   apply (case_tac ts, simp_all add: cthread_state_relation_def)[1]
                  apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)

diff --git a/proof/crefine/AARCH64/Wellformed_C.thy b/proof/crefine/AARCH64/Wellformed_C.thy
@@ -668,20 +668,23 @@ lemma ptrFromPAddr_mask_cacheLineSize[simp]:
 (* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
 lemma
   shows ThreadState_Restart_mask[simp]:
-  "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
+  "(scast ThreadState_Restart :: machine_word) && mask 4 = scast ThreadState_Restart"
   and ThreadState_Inactive_mask[simp]:
-  "(scast ThreadState_Inactive::machine_word) && mask 4 = scast ThreadState_Inactive"
+  "(scast ThreadState_Inactive :: machine_word) && mask 4 = scast ThreadState_Inactive"
   and ThreadState_Running_mask[simp]:
-  "(scast ThreadState_Running::machine_word) && mask 4 = scast ThreadState_Running"
+  "(scast ThreadState_Running :: machine_word) && mask 4 = scast ThreadState_Running"
   and ThreadState_BlockedOnReceive_mask[simp]:
-  "(scast ThreadState_BlockedOnReceive::machine_word) && mask 4 = scast ThreadState_BlockedOnReceive"
+  "(scast ThreadState_BlockedOnReceive :: machine_word) && mask 4
+   = scast ThreadState_BlockedOnReceive"
   and ThreadState_BlockedOnSend_mask[simp]:
-  "(scast ThreadState_BlockedOnSend::machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
+  "(scast ThreadState_BlockedOnSend :: machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
   and ThreadState_BlockedOnReply_mask[simp]:
-  "(scast ThreadState_BlockedOnReply::machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
+  "(scast ThreadState_BlockedOnReply :: machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
   and ThreadState_BlockedOnNotification_mask[simp]:
-  "(scast ThreadState_BlockedOnNotification::machine_word) && mask 4
+  "(scast ThreadState_BlockedOnNotification :: machine_word) && mask 4
    = scast ThreadState_BlockedOnNotification"
+  and ThreadState_IdleThreadState_mask[simp]:
+  "(scast ThreadState_IdleThreadState :: machine_word) && mask 4 = scast ThreadState_IdleThreadState"
   by (simp add: ThreadState_defs mask_def)+
 
 lemma aligned_tcb_ctcb_not_NULL:

diff --git a/proof/crefine/ARM/Recycle_C.thy b/proof/crefine/ARM/Recycle_C.thy
@@ -798,7 +798,6 @@ lemma cancelBadgedSends_ccorres:
           apply (clarsimp simp: typ_heap_simps st_tcb_at'_def)
           apply (drule(1) obj_at_cslift_tcb)
           apply (clarsimp simp: ctcb_relation_blocking_ipc_badge)
-          apply (rule conjI, simp add: ThreadState_defs mask_def)
           apply (rule conjI)
            apply clarsimp
            apply (frule rf_sr_cscheduler_relation)

diff --git a/proof/crefine/ARM/Syscall_C.thy b/proof/crefine/ARM/Syscall_C.thy
@@ -318,7 +318,6 @@ lemma decodeInvocation_ccorres:
    apply (clarsimp simp: isCap_simps cap_get_tag_to_H from_bool_neq_0)
   apply (insert ccap_relation_IRQHandler_mask, elim meta_allE, drule(1) meta_mp)
   apply (clarsimp simp: word_size)
-  apply (clarsimp simp: less_mask_eq)
   apply (clarsimp simp: cap_get_tag_isCap)
   apply (cases cp ; clarsimp simp: isCap_simps)
      apply (frule cap_get_tag_isCap_unfolded_H_cap, drule (1) cap_get_tag_to_H)
@@ -448,8 +447,6 @@ lemma handleDoubleFault_ccorres:
     apply (rule empty_fail_asUser)
     apply (simp add: getRestartPC_def)
    apply wp
-  apply clarsimp
-  apply (simp add: ThreadState_defs)
   apply (fastforce simp: valid_tcb_state'_def)
   done
 
@@ -858,7 +855,6 @@ lemma handleInvocation_ccorres:
                     apply auto[1]
                    apply clarsimp
                   apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)
-                  apply (simp add: ThreadState_defs mask_def)
                   apply (simp add: typ_heap_simps)
                   apply (case_tac ts, simp_all add: cthread_state_relation_def)[1]
                  apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)

diff --git a/proof/crefine/ARM/Tcb_C.thy b/proof/crefine/ARM/Tcb_C.thy
@@ -3244,7 +3244,6 @@ lemma decodeSetMCPriority_ccorres:
                 elim!: obj_at'_weakenE pred_tcb'_weakenE
                 dest!: st_tcb_at_idle_thread')[1]
    apply (clarsimp simp: interpret_excaps_eq excaps_map_def)
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size option_to_0_def)
   apply (frule rf_sr_ksCurThread)
   apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def)
@@ -3377,7 +3376,6 @@ lemma decodeSetPriority_ccorres:
                 elim!: obj_at'_weakenE pred_tcb'_weakenE
                 dest!: st_tcb_at_idle_thread')[1]
    apply (clarsimp simp: interpret_excaps_eq excaps_map_def)
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size option_to_0_def)
   apply (frule rf_sr_ksCurThread)
   apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def)
@@ -4404,7 +4402,6 @@ lemma decodeSetTLSBase_ccorres:
    apply (clarsimp simp: ct_in_state'_def sysargs_rel_n_def n_msgRegisters_def)
    apply (auto simp: valid_tcb_state'_def
               elim!: pred_tcb'_weakenE)[1]
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size)
   apply (frule rf_sr_ksCurThread)
   apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply (auto simp: unat_eq_0 le_max_word_ucast_id)+
@@ -4556,7 +4553,6 @@ lemma decodeTCBInvocation_ccorres:
               dest!: st_tcb_at_idle_thread')[1]
   apply (simp split: sum.split add: cintr_def intr_and_se_rel_def
                         exception_defs syscall_error_rel_def)
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size)
   apply (simp add: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply clarsimp
   done

diff --git a/proof/crefine/ARM/Wellformed_C.thy b/proof/crefine/ARM/Wellformed_C.thy
@@ -578,20 +578,23 @@ where
 (* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
 lemma
   shows ThreadState_Restart_mask[simp]:
-  "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
+  "(scast ThreadState_Restart :: machine_word) && mask 4 = scast ThreadState_Restart"
   and ThreadState_Inactive_mask[simp]:
-  "(scast ThreadState_Inactive::machine_word) && mask 4 = scast ThreadState_Inactive"
+  "(scast ThreadState_Inactive :: machine_word) && mask 4 = scast ThreadState_Inactive"
   and ThreadState_Running_mask[simp]:
-  "(scast ThreadState_Running::machine_word) && mask 4 = scast ThreadState_Running"
+  "(scast ThreadState_Running :: machine_word) && mask 4 = scast ThreadState_Running"
   and ThreadState_BlockedOnReceive_mask[simp]:
-  "(scast ThreadState_BlockedOnReceive::machine_word) && mask 4 = scast ThreadState_BlockedOnReceive"
+  "(scast ThreadState_BlockedOnReceive :: machine_word) && mask 4
+   = scast ThreadState_BlockedOnReceive"
   and ThreadState_BlockedOnSend_mask[simp]:
-  "(scast ThreadState_BlockedOnSend::machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
+  "(scast ThreadState_BlockedOnSend :: machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
   and ThreadState_BlockedOnReply_mask[simp]:
-  "(scast ThreadState_BlockedOnReply::machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
+  "(scast ThreadState_BlockedOnReply :: machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
   and ThreadState_BlockedOnNotification_mask[simp]:
-  "(scast ThreadState_BlockedOnNotification::machine_word) && mask 4
+  "(scast ThreadState_BlockedOnNotification :: machine_word) && mask 4
    = scast ThreadState_BlockedOnNotification"
+  and ThreadState_IdleThreadState_mask[simp]:
+  "(scast ThreadState_IdleThreadState :: machine_word) && mask 4 = scast ThreadState_IdleThreadState"
   by (simp add: ThreadState_defs mask_def)+
 
 end

diff --git a/proof/crefine/ARM_HYP/Recycle_C.thy b/proof/crefine/ARM_HYP/Recycle_C.thy
@@ -1138,7 +1138,6 @@ lemma cancelBadgedSends_ccorres:
           apply (clarsimp simp: typ_heap_simps st_tcb_at'_def)
           apply (drule(1) obj_at_cslift_tcb)
           apply (clarsimp simp: ctcb_relation_blocking_ipc_badge)
-          apply (rule conjI, simp add: ThreadState_defs mask_def)
           apply (rule conjI)
            apply clarsimp
            apply (frule rf_sr_cscheduler_relation)

diff --git a/proof/crefine/ARM_HYP/Syscall_C.thy b/proof/crefine/ARM_HYP/Syscall_C.thy
@@ -324,7 +324,6 @@ lemma decodeInvocation_ccorres:
    apply (clarsimp simp: isCap_simps cap_get_tag_to_H from_bool_neq_0)
   apply (insert ccap_relation_IRQHandler_mask, elim meta_allE, drule(1) meta_mp)
   apply (clarsimp simp: word_size)
-  apply (clarsimp simp: less_mask_eq)
   apply (clarsimp simp: cap_get_tag_isCap)
   apply (cases cp ; clarsimp simp: isCap_simps)
      apply (frule cap_get_tag_isCap_unfolded_H_cap, drule (1) cap_get_tag_to_H)
@@ -534,8 +533,6 @@ lemma handleDoubleFault_ccorres:
     apply (rule empty_fail_asUser)
     apply (simp add: getRestartPC_def)
    apply wp
-  apply clarsimp
-  apply (simp add: ThreadState_defs)
   apply (fastforce simp: valid_tcb_state'_def)
   done
 
@@ -955,7 +952,6 @@ lemma handleInvocation_ccorres:
                     apply auto[1]
                    apply clarsimp
                   apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)
-                  apply (simp add: ThreadState_defs mask_def)
                   apply (simp add: typ_heap_simps)
                   apply (case_tac ts, simp_all add: cthread_state_relation_def)[1]
                  apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)

diff --git a/proof/crefine/ARM_HYP/Tcb_C.thy b/proof/crefine/ARM_HYP/Tcb_C.thy
@@ -3338,7 +3338,6 @@ lemma decodeSetMCPriority_ccorres:
                 elim!: obj_at'_weakenE pred_tcb'_weakenE
                 dest!: st_tcb_at_idle_thread')[1]
    apply (clarsimp simp: interpret_excaps_eq excaps_map_def)
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size option_to_0_def)
   apply (frule rf_sr_ksCurThread)
   apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def)
@@ -3471,7 +3470,6 @@ lemma decodeSetPriority_ccorres:
                 elim!: obj_at'_weakenE pred_tcb'_weakenE
                 dest!: st_tcb_at_idle_thread')[1]
    apply (clarsimp simp: interpret_excaps_eq excaps_map_def)
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size option_to_0_def)
   apply (frule rf_sr_ksCurThread)
   apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def)
@@ -4495,7 +4493,6 @@ lemma decodeSetTLSBase_ccorres:
    apply (clarsimp simp: ct_in_state'_def sysargs_rel_n_def n_msgRegisters_def)
    apply (auto simp: valid_tcb_state'_def
               elim!: pred_tcb'_weakenE)[1]
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size)
   apply (frule rf_sr_ksCurThread)
   apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply (auto simp: unat_eq_0 le_max_word_ucast_id)+
@@ -4647,7 +4644,6 @@ lemma decodeTCBInvocation_ccorres:
               dest!: st_tcb_at_idle_thread')[1]
   apply (simp split: sum.split add: cintr_def intr_and_se_rel_def
                         exception_defs syscall_error_rel_def)
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size)
   apply (simp add: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply clarsimp
   done

diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy
@@ -615,20 +615,23 @@ where
 (* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
 lemma
   shows ThreadState_Restart_mask[simp]:
-  "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
+  "(scast ThreadState_Restart :: machine_word) && mask 4 = scast ThreadState_Restart"
   and ThreadState_Inactive_mask[simp]:
-  "(scast ThreadState_Inactive::machine_word) && mask 4 = scast ThreadState_Inactive"
+  "(scast ThreadState_Inactive :: machine_word) && mask 4 = scast ThreadState_Inactive"
   and ThreadState_Running_mask[simp]:
-  "(scast ThreadState_Running::machine_word) && mask 4 = scast ThreadState_Running"
+  "(scast ThreadState_Running :: machine_word) && mask 4 = scast ThreadState_Running"
   and ThreadState_BlockedOnReceive_mask[simp]:
-  "(scast ThreadState_BlockedOnReceive::machine_word) && mask 4 = scast ThreadState_BlockedOnReceive"
+  "(scast ThreadState_BlockedOnReceive :: machine_word) && mask 4
+   = scast ThreadState_BlockedOnReceive"
   and ThreadState_BlockedOnSend_mask[simp]:
-  "(scast ThreadState_BlockedOnSend::machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
+  "(scast ThreadState_BlockedOnSend :: machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
   and ThreadState_BlockedOnReply_mask[simp]:
-  "(scast ThreadState_BlockedOnReply::machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
+  "(scast ThreadState_BlockedOnReply :: machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
   and ThreadState_BlockedOnNotification_mask[simp]:
-  "(scast ThreadState_BlockedOnNotification::machine_word) && mask 4
+  "(scast ThreadState_BlockedOnNotification :: machine_word) && mask 4
    = scast ThreadState_BlockedOnNotification"
+  and ThreadState_IdleThreadState_mask[simp]:
+  "(scast ThreadState_IdleThreadState :: machine_word) && mask 4 = scast ThreadState_IdleThreadState"
   by (simp add: ThreadState_defs mask_def)+
 
 end

diff --git a/proof/crefine/RISCV64/Recycle_C.thy b/proof/crefine/RISCV64/Recycle_C.thy
@@ -1019,7 +1019,6 @@ lemma cancelBadgedSends_ccorres:
           apply (clarsimp simp: typ_heap_simps st_tcb_at'_def)
           apply (drule(1) obj_at_cslift_tcb)
           apply (clarsimp simp: ctcb_relation_blocking_ipc_badge)
-          apply (rule conjI, simp add: ThreadState_defs mask_def)
           apply (rule conjI)
            apply clarsimp
            apply (frule rf_sr_cscheduler_relation)

diff --git a/proof/crefine/RISCV64/Syscall_C.thy b/proof/crefine/RISCV64/Syscall_C.thy
@@ -324,7 +324,6 @@ lemma decodeInvocation_ccorres:
    apply (clarsimp simp: isCap_simps cap_get_tag_to_H from_bool_neq_0)
   apply (insert ccap_relation_IRQHandler_mask, elim meta_allE, drule(1) meta_mp)
   apply (clarsimp simp: word_size)
-  apply (clarsimp simp: less_mask_eq)
   apply (clarsimp simp: cap_get_tag_isCap)
   apply (cases cp ; clarsimp simp: isCap_simps)
      apply (frule cap_get_tag_isCap_unfolded_H_cap, drule (1) cap_get_tag_to_H)
@@ -520,8 +519,6 @@ lemma handleDoubleFault_ccorres:
     apply (rule empty_fail_asUser)
     apply (simp add: getRestartPC_def)
    apply wp
-  apply clarsimp
-  apply (simp add: ThreadState_defs)
   apply (fastforce simp: valid_tcb_state'_def)
   done
 
@@ -896,7 +893,6 @@ lemma handleInvocation_ccorres:
                     apply auto[1]
                    apply clarsimp
                   apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)
-                  apply (simp add: ThreadState_defs mask_def)
                   apply (simp add: typ_heap_simps)
                   apply (case_tac ts, simp_all add: cthread_state_relation_def)[1]
                  apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)

diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy
@@ -3308,7 +3308,6 @@ lemma decodeSetMCPriority_ccorres:
                 elim!: obj_at'_weakenE pred_tcb'_weakenE
                 dest!: st_tcb_at_idle_thread')[1]
    apply (clarsimp simp: interpret_excaps_eq excaps_map_def)
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size option_to_0_def)
   apply (frule rf_sr_ksCurThread)
   apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def)
@@ -3441,7 +3440,6 @@ lemma decodeSetPriority_ccorres:
                 elim!: obj_at'_weakenE pred_tcb'_weakenE
                 dest!: st_tcb_at_idle_thread')[1]
    apply (clarsimp simp: interpret_excaps_eq excaps_map_def)
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size option_to_0_def)
   apply (frule rf_sr_ksCurThread)
   apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def)
@@ -4505,7 +4503,6 @@ lemma decodeSetTLSBase_ccorres:
    apply (clarsimp simp: ct_in_state'_def sysargs_rel_n_def n_msgRegisters_def)
    apply (auto simp: valid_tcb_state'_def
               elim!: pred_tcb'_weakenE)[1]
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size)
   apply (frule rf_sr_ksCurThread)
   apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply (auto simp: unat_eq_0 le_max_word_ucast_id)+
@@ -4657,7 +4654,6 @@ lemma decodeTCBInvocation_ccorres:
               dest!: st_tcb_at_idle_thread')[1]
   apply (simp split: sum.split add: cintr_def intr_and_se_rel_def
                         exception_defs syscall_error_rel_def)
-  apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size)
   apply (simp add: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
   apply clarsimp
   done

diff --git a/proof/crefine/RISCV64/Wellformed_C.thy b/proof/crefine/RISCV64/Wellformed_C.thy
@@ -559,20 +559,23 @@ where
 (* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
 lemma
   shows ThreadState_Restart_mask[simp]:
-  "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
+  "(scast ThreadState_Restart :: machine_word) && mask 4 = scast ThreadState_Restart"
   and ThreadState_Inactive_mask[simp]:
-  "(scast ThreadState_Inactive::machine_word) && mask 4 = scast ThreadState_Inactive"
+  "(scast ThreadState_Inactive :: machine_word) && mask 4 = scast ThreadState_Inactive"
   and ThreadState_Running_mask[simp]:
-  "(scast ThreadState_Running::machine_word) && mask 4 = scast ThreadState_Running"
+  "(scast ThreadState_Running :: machine_word) && mask 4 = scast ThreadState_Running"
   and ThreadState_BlockedOnReceive_mask[simp]:
-  "(scast ThreadState_BlockedOnReceive::machine_word) && mask 4 = scast ThreadState_BlockedOnReceive"
+  "(scast ThreadState_BlockedOnReceive :: machine_word) && mask 4
+   = scast ThreadState_BlockedOnReceive"
   and ThreadState_BlockedOnSend_mask[simp]:
-  "(scast ThreadState_BlockedOnSend::machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
+  "(scast ThreadState_BlockedOnSend :: machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
   and ThreadState_BlockedOnReply_mask[simp]:
-  "(scast ThreadState_BlockedOnReply::machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
+  "(scast ThreadState_BlockedOnReply :: machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
   and ThreadState_BlockedOnNotification_mask[simp]:
-  "(scast ThreadState_BlockedOnNotification::machine_word) && mask 4
+  "(scast ThreadState_BlockedOnNotification :: machine_word) && mask 4
    = scast ThreadState_BlockedOnNotification"
+  and ThreadState_IdleThreadState_mask[simp]:
+  "(scast ThreadState_IdleThreadState :: machine_word) && mask 4 = scast ThreadState_IdleThreadState"
   by (simp add: ThreadState_defs mask_def)+
 
 (* generic lemmas with arch-specific consequences *)

diff --git a/proof/crefine/X64/Recycle_C.thy b/proof/crefine/X64/Recycle_C.thy
@@ -1119,7 +1119,6 @@ lemma cancelBadgedSends_ccorres:
           apply (clarsimp simp: typ_heap_simps st_tcb_at'_def)
           apply (drule(1) obj_at_cslift_tcb)
           apply (clarsimp simp: ctcb_relation_blocking_ipc_badge)
-          apply (rule conjI, simp add: ThreadState_defs mask_def)
           apply (rule conjI)
            apply clarsimp
            apply (frule rf_sr_cscheduler_relation)