Lemmas for simplifying masking and thread states

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)

proof/crefine/AARCH64/Wellformed_C.thy

@@ -703,9 +703,26 @@ where
   "prioInvalid == seL4_InvalidPrio"
 
 (* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
-lemma ThreadState_Restart_mask[simp]:
-  "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
-  by (simp add: ThreadState_Restart_def mask_def)
+lemma
+  shows ThreadState_Restart_mask[simp]:
+  "(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"
+  and ThreadState_Running_mask[simp]:
+  "(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"
+  and ThreadState_BlockedOnSend_mask[simp]:
+  "(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"
+  and ThreadState_BlockedOnNotification_mask[simp]:
+  "(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:
   assumes "is_aligned p tcbBlockSizeBits"

proof/crefine/ARM/Recycle_C.thy

@@ -799,7 +799,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)

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)

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

proof/crefine/ARM/Wellformed_C.thy

@@ -632,6 +632,28 @@ abbreviation(input)
 where
   "prioInvalid == seL4_InvalidPrio"
 
+(* 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"
+  and ThreadState_Inactive_mask[simp]:
+  "(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"
+  and ThreadState_BlockedOnReceive_mask[simp]:
+  "(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"
+  and ThreadState_BlockedOnReply_mask[simp]:
+  "(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"
+  and ThreadState_IdleThreadState_mask[simp]:
+  "(scast ThreadState_IdleThreadState :: machine_word) && mask 4 = scast ThreadState_IdleThreadState"
+  by (simp add: ThreadState_defs mask_def)+
+
 end
 
 end

proof/crefine/ARM_HYP/Arch_C.thy

@@ -5230,7 +5230,6 @@ proof -
                           rf_sr_ksCurThread msgRegisters_unfold
                           valid_tcb_state'_def ThreadState_defs Kernel_C_maxIRQ
                           and_mask_eq_iff_le_mask capVCPUPtr_eq)
-    apply (clarsimp simp:  mask_def)
     done
 qed
 

proof/crefine/ARM_HYP/Recycle_C.thy

@@ -1126,7 +1126,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)

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)

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

proof/crefine/ARM_HYP/Wellformed_C.thy

@@ -707,6 +707,28 @@ abbreviation(input)
 where
   "prioInvalid == seL4_InvalidPrio"
 
+(* 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"
+  and ThreadState_Inactive_mask[simp]:
+  "(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"
+  and ThreadState_BlockedOnReceive_mask[simp]:
+  "(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"
+  and ThreadState_BlockedOnReply_mask[simp]:
+  "(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"
+  and ThreadState_IdleThreadState_mask[simp]:
+  "(scast ThreadState_IdleThreadState :: machine_word) && mask 4 = scast ThreadState_IdleThreadState"
+  by (simp add: ThreadState_defs mask_def)+
+
 end
 
 end

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)

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)

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

proof/crefine/RISCV64/Wellformed_C.thy

@@ -556,6 +556,28 @@ abbreviation(input)
 where
   "prioInvalid == seL4_InvalidPrio"
 
+(* 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"
+  and ThreadState_Inactive_mask[simp]:
+  "(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"
+  and ThreadState_BlockedOnReceive_mask[simp]:
+  "(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"
+  and ThreadState_BlockedOnReply_mask[simp]:
+  "(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"
+  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 *)
 
 schematic_goal size_gpRegisters: