From 0cba8a62cc42523419088b59a1e37096ab850cd9 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 9 Sep 2024 13:44:10 +0930 Subject: [PATCH] crefine: lemmas for simplifying masking and thread states Signed-off-by: Michael McInerney --- proof/crefine/AARCH64/Syscall_C.thy | 3 --- proof/crefine/AARCH64/Wellformed_C.thy | 23 +++++++++++++++--- proof/crefine/ARM/Recycle_C.thy | 1 - proof/crefine/ARM/Syscall_C.thy | 4 ---- proof/crefine/ARM/Tcb_C.thy | 4 ---- proof/crefine/ARM/Wellformed_C.thy | 22 ++++++++++++++++++ proof/crefine/ARM_HYP/Arch_C.thy | 1 - proof/crefine/ARM_HYP/Recycle_C.thy | 1 - proof/crefine/ARM_HYP/Syscall_C.thy | 4 ---- proof/crefine/ARM_HYP/Tcb_C.thy | 4 ---- proof/crefine/ARM_HYP/Wellformed_C.thy | 22 ++++++++++++++++++ proof/crefine/RISCV64/Recycle_C.thy | 1 - proof/crefine/RISCV64/Syscall_C.thy | 4 ---- proof/crefine/RISCV64/Tcb_C.thy | 4 ---- proof/crefine/RISCV64/Wellformed_C.thy | 22 ++++++++++++++++++ proof/crefine/X64/Arch_C.thy | 32 ++++++++++---------------- proof/crefine/X64/Recycle_C.thy | 1 - proof/crefine/X64/Syscall_C.thy | 4 ---- proof/crefine/X64/Tcb_C.thy | 4 ---- proof/crefine/X64/Wellformed_C.thy | 22 ++++++++++++++++++ 20 files changed, 120 insertions(+), 63 deletions(-) diff --git a/proof/crefine/AARCH64/Syscall_C.thy b/proof/crefine/AARCH64/Syscall_C.thy index 199592009c..7602befca1 100644 --- 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 index 9517cab4bf..8ec4988225 100644 --- a/proof/crefine/AARCH64/Wellformed_C.thy +++ b/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" diff --git a/proof/crefine/ARM/Recycle_C.thy b/proof/crefine/ARM/Recycle_C.thy index df3ff05be3..06fb11a675 100644 --- a/proof/crefine/ARM/Recycle_C.thy +++ b/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) diff --git a/proof/crefine/ARM/Syscall_C.thy b/proof/crefine/ARM/Syscall_C.thy index 1b7e214e52..5e88f977f6 100644 --- 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 index 82c5be1e8c..fc975b2a3f 100644 --- 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 index caa878d9bf..d097de76d5 100644 --- a/proof/crefine/ARM/Wellformed_C.thy +++ b/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 diff --git a/proof/crefine/ARM_HYP/Arch_C.thy b/proof/crefine/ARM_HYP/Arch_C.thy index 9cc8df1e92..9c06ceeb70 100644 --- a/proof/crefine/ARM_HYP/Arch_C.thy +++ b/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 diff --git a/proof/crefine/ARM_HYP/Recycle_C.thy b/proof/crefine/ARM_HYP/Recycle_C.thy index 2db441b729..1f0c282a89 100644 --- a/proof/crefine/ARM_HYP/Recycle_C.thy +++ b/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) diff --git a/proof/crefine/ARM_HYP/Syscall_C.thy b/proof/crefine/ARM_HYP/Syscall_C.thy index 8631445958..d10a172606 100644 --- 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 index 9f710990d7..112f0cafa0 100644 --- 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 index 7cc8b68842..36670658b3 100644 --- a/proof/crefine/ARM_HYP/Wellformed_C.thy +++ b/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 diff --git a/proof/crefine/RISCV64/Recycle_C.thy b/proof/crefine/RISCV64/Recycle_C.thy index b2d0451ad9..b2cee3882e 100644 --- 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 index 9e6e2b1ca8..7c6fa301a1 100644 --- 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 index 583dc114db..c911140f81 100644 --- 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 index ad1989b612..1e16122630 100644 --- a/proof/crefine/RISCV64/Wellformed_C.thy +++ b/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: diff --git a/proof/crefine/X64/Arch_C.thy b/proof/crefine/X64/Arch_C.thy index 6097839389..e72edffb94 100644 --- a/proof/crefine/X64/Arch_C.thy +++ b/proof/crefine/X64/Arch_C.thy @@ -1278,7 +1278,7 @@ lemma decodeX64PageTableInvocation_ccorres: apply (auto dest: ctes_of_valid')[1] (* X64PageTableUnmap *) apply (rule conjI) - apply (fastforce simp: rf_sr_ksCurThread ThreadState_defs + apply (fastforce simp: rf_sr_ksCurThread mask_eq_iff_w2p word_size ct_in_state'_def st_tcb_at'_def word_sle_def word_sless_def @@ -1312,7 +1312,6 @@ lemma decodeX64PageTableInvocation_ccorres: intro!: is_aligned_addrFromPPtr[simplified bit_simps, simplified] simp: vmsz_aligned_def cap_to_H_simps cap_page_table_cap_lift_def bit_simps capAligned_def) apply clarsimp - apply (rule conjI, clarsimp simp: ThreadState_defs mask_def) apply (rule conjI) (* ccap_relation *) apply (clarsimp simp: ccap_relation_def map_option_Some_eq2 cap_page_table_cap_lift[THEN iffD1] @@ -1338,7 +1337,6 @@ lemma decodeX64PageTableInvocation_ccorres: (* the below proof duplicates some of the sections above *) apply (clarsimp simp: pde_tag_defs pde_get_tag_def word_and_1) apply safe - apply (clarsimp simp: ThreadState_defs mask_def) (* ccap_relation *) apply (clarsimp simp: ccap_relation_def map_option_Some_eq2 cap_page_table_cap_lift[THEN iffD1] cap_to_H_simps asid_wf_def3[simplified asid_bits_def, simplified]) @@ -1845,7 +1843,7 @@ lemma performPageGetAddress_ccorres: apply (cases isCall) apply (auto simp: X64.badgeRegister_def X64_H.badgeRegister_def Kernel_C.badgeRegister_def X64.capRegister_def Kernel_C.RDI_def Kernel_C.RSI_def fromPAddr_def - ThreadState_defs pred_tcb_at'_def obj_at'_def ct_in_state'_def) + pred_tcb_at'_def obj_at'_def ct_in_state'_def) done lemma vmsz_aligned_addrFromPPtr': @@ -2209,7 +2207,7 @@ lemma decodeX86ModeMapPage_ccorres: apply (simp add: all_ex_eq_helper) apply (vcg exspec=createSafeMappingEntries_PDPTE_modifies) by (fastforce simp: invs_valid_objs' tcb_at_invs' vmsz_aligned_addrFromPPtr' - valid_tcb_state'_def invs_sch_act_wf' ThreadState_defs rf_sr_ksCurThread + valid_tcb_state'_def invs_sch_act_wf' rf_sr_ksCurThread arch_invocation_label_defs mask_def isCap_simps) lemma valid_cap'_PageCap_kernel_mappings: @@ -2662,8 +2660,7 @@ lemma decodeX64FrameInvocation_ccorres: (Some (y, a)))) cap}" and A' = "{}" in conseqPost) apply (vcg exspec=createSafeMappingEntries_PTE_modifies) - apply (clarsimp simp: ThreadState_defs mask_def rf_sr_ksCurThread - isCap_simps cap_pml4_cap_lift + apply (clarsimp simp: rf_sr_ksCurThread isCap_simps cap_pml4_cap_lift get_capPtr_CL_def ccap_relation_PML4Cap_BasePtr) apply clarsimp apply (rule ccorres_Cond_rhs) @@ -2697,8 +2694,7 @@ lemma decodeX64FrameInvocation_ccorres: (Some (y, a)))) cap}" and A' = "{}" in conseqPost) apply (vcg exspec=createSafeMappingEntries_PDE_modifies) - apply (clarsimp simp: ThreadState_defs mask_def rf_sr_ksCurThread - isCap_simps cap_pml4_cap_lift + apply (clarsimp simp: rf_sr_ksCurThread isCap_simps cap_pml4_cap_lift get_capPtr_CL_def ccap_relation_PML4Cap_BasePtr) apply clarsimp apply (rule ccorres_add_returnOk) @@ -2797,7 +2793,7 @@ lemma decodeX64FrameInvocation_ccorres: (* C side *) - apply (clarsimp simp: rf_sr_ksCurThread ThreadState_defs mask_eq_iff_w2p + apply (clarsimp simp: rf_sr_ksCurThread mask_eq_iff_w2p word_size word_less_nat_alt from_bool_0 excaps_map_def cte_wp_at_ctes_of n_msgRegisters_def) apply (frule(1) ctes_of_valid') @@ -3251,7 +3247,7 @@ lemma decodeX64PageDirectoryInvocation_ccorres: slotcap_in_mem_def) apply (auto dest: ctes_of_valid')[1] apply (rule conjI) - apply (clarsimp simp: rf_sr_ksCurThread ThreadState_defs + apply (clarsimp simp: rf_sr_ksCurThread mask_eq_iff_w2p word_size ct_in_state'_def st_tcb_at'_def word_sle_def word_sless_def @@ -3284,7 +3280,6 @@ lemma decodeX64PageDirectoryInvocation_ccorres: intro!: is_aligned_addrFromPPtr[simplified bit_simps, simplified] simp: vmsz_aligned_def cap_to_H_simps cap_page_directory_cap_lift_def bit_simps capAligned_def) apply clarsimp - apply (rule conjI, clarsimp simp: ThreadState_defs mask_def) (* ccap_relation *) apply (rule conjI) apply (clarsimp simp: ccap_relation_def map_option_Some_eq2 cap_page_directory_cap_lift[THEN iffD1] @@ -3314,7 +3309,6 @@ lemma decodeX64PageDirectoryInvocation_ccorres: context_conjI creates a mess, separate lemmas would be a bit unwieldy *) apply safe - apply (clarsimp simp: ThreadState_defs mask_def) (* ccap_relation *) apply (clarsimp simp: ccap_relation_def map_option_Some_eq2 cap_page_directory_cap_lift[THEN iffD1] cap_to_H_simps asid_wf_def3[simplified asid_bits_def, simplified]) @@ -3694,7 +3688,7 @@ lemma decodeX64PDPTInvocation_ccorres: elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')[1] apply (auto simp: neq_Nil_conv excaps_in_mem_def slotcap_in_mem_def)[1] apply (rule conjI) - apply (fastforce simp: rf_sr_ksCurThread ThreadState_defs + apply (fastforce simp: rf_sr_ksCurThread mask_eq_iff_w2p word_size ct_in_state'_def st_tcb_at'_def word_sle_def word_sless_def @@ -3727,7 +3721,6 @@ lemma decodeX64PDPTInvocation_ccorres: apply (clarsimp simp: get_capMappedASID_CL_def) apply (subst cap_lift_PML4Cap_Base[symmetric]; (assumption | rule sym, assumption)) apply (clarsimp simp: rf_sr_ksCurThread) - apply (rule conjI, fastforce simp: ThreadState_defs mask_def) (* ccap_relation *) apply (rule conjI) apply (erule ccap_relationE[where c="ArchObjectCap (PDPointerTableCap _ _)"]) @@ -4046,7 +4039,7 @@ lemma decodeX64MMUInvocation_ccorres: apply (rule_tac Q'=UNIV and A'="{}" in conseqPost) apply (vcg exspec=ensureEmptySlot_modifies) apply (frule length_ineq_not_Nil) - apply (clarsimp simp: null_def ThreadState_defs mask_def hd_conv_nth + apply (clarsimp simp: null_def hd_conv_nth isCap_simps rf_sr_ksCurThread cap_get_tag_UntypedCap word_le_make_less asid_high_bits_def split: list.split) @@ -4415,8 +4408,7 @@ lemma decodeX64MMUInvocation_ccorres: dest!: st_tcb_at_idle_thread' elim!: pred_tcb'_weakenE)[1] apply (clarsimp simp: cte_wp_at_ctes_of asidHighBits_handy_convs - word_sle_def word_sless_def asidLowBits_handy_convs - rf_sr_ksCurThread ThreadState_defs mask_def[where n=4] + word_sle_def word_sless_def asidLowBits_handy_convs rf_sr_ksCurThread cong: if_cong) apply (clarsimp simp: ccap_relation_isDeviceCap2 objBits_simps archObjSize_def pageBits_def case_bool_If) @@ -5376,7 +5368,7 @@ proof - apply (clarsimp simp: ct_in_state'_def) apply (rule_tac P="UNIV" in conseqPre) apply (simp add: all_ex_eq_helper, vcg exspec=getSyscallArg_modifies) - apply (clarsimp simp: interpret_excaps_eq rf_sr_ksCurThread ThreadState_defs mask_def) + apply (clarsimp simp: interpret_excaps_eq rf_sr_ksCurThread) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply clarsimp apply (rule conjI, clarsimp simp: sysargs_rel_to_n dest!: unat_length_4_helper) @@ -5718,7 +5710,7 @@ proof - invs_sch_act_wf' ct_active_st_tcb_at_minor' rf_sr_ksCurThread ucast_mask_drop[where n=16, simplified mask_def, simplified]) apply (safe, simp_all add: unat_eq_0 unat_eq_1) - apply (clarsimp dest!: unat_length_2_helper simp: ThreadState_defs mask_def syscall_error_rel_def + apply (clarsimp dest!: unat_length_2_helper simp: syscall_error_rel_def | (thin_tac "P" for P)+, word_bitwise)+ done qed diff --git a/proof/crefine/X64/Recycle_C.thy b/proof/crefine/X64/Recycle_C.thy index 7eb8d1c6aa..b8bc3f8e50 100644 --- 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) diff --git a/proof/crefine/X64/Syscall_C.thy b/proof/crefine/X64/Syscall_C.thy index adda71099e..0d366bf3f8 100644 --- a/proof/crefine/X64/Syscall_C.thy +++ b/proof/crefine/X64/Syscall_C.thy @@ -322,7 +322,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) @@ -518,8 +517,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 @@ -893,7 +890,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/X64/Tcb_C.thy b/proof/crefine/X64/Tcb_C.thy index 7c4f2dbae3..575c1403e5 100644 --- a/proof/crefine/X64/Tcb_C.thy +++ b/proof/crefine/X64/Tcb_C.thy @@ -3297,7 +3297,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) @@ -3430,7 +3429,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/X64/Wellformed_C.thy b/proof/crefine/X64/Wellformed_C.thy index 66d4ec6df8..07ce28b5c7 100644 --- a/proof/crefine/X64/Wellformed_C.thy +++ b/proof/crefine/X64/Wellformed_C.thy @@ -614,6 +614,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