From 668c4dd359dea32324345b58d977fd8850807541 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 9 Sep 2024 13:44:10 +0930 Subject: [PATCH 1/2] crefine: lemmas for simplifying masking and thread states Signed-off-by: Michael McInerney --- proof/crefine/AARCH64/Wellformed_C.thy | 18 ++++++++++++++++-- proof/crefine/ARM/Wellformed_C.thy | 19 +++++++++++++++++++ proof/crefine/ARM_HYP/Wellformed_C.thy | 19 +++++++++++++++++++ proof/crefine/RISCV64/Wellformed_C.thy | 19 +++++++++++++++++++ proof/crefine/X64/Wellformed_C.thy | 19 +++++++++++++++++++ 5 files changed, 92 insertions(+), 2 deletions(-) diff --git a/proof/crefine/AARCH64/Wellformed_C.thy b/proof/crefine/AARCH64/Wellformed_C.thy index 76e236b963..cf7f44bbda 100644 --- a/proof/crefine/AARCH64/Wellformed_C.thy +++ b/proof/crefine/AARCH64/Wellformed_C.thy @@ -666,9 +666,23 @@ lemma ptrFromPAddr_mask_cacheLineSize[simp]: by (simp add: ptrFromPAddr_def add_mask_ignore) (* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *) -lemma ThreadState_Restart_mask[simp]: +lemma + shows ThreadState_Restart_mask[simp]: "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart" - by (simp add: ThreadState_Restart_def mask_def) + 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" + by (simp add: ThreadState_defs mask_def)+ lemma aligned_tcb_ctcb_not_NULL: assumes "is_aligned p tcbBlockSizeBits" diff --git a/proof/crefine/ARM/Wellformed_C.thy b/proof/crefine/ARM/Wellformed_C.thy index e2c6c7805d..c10f19631c 100644 --- a/proof/crefine/ARM/Wellformed_C.thy +++ b/proof/crefine/ARM/Wellformed_C.thy @@ -575,6 +575,25 @@ 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" + by (simp add: ThreadState_defs mask_def)+ + end end diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy index c5dae8cd44..237d6e3dee 100644 --- a/proof/crefine/ARM_HYP/Wellformed_C.thy +++ b/proof/crefine/ARM_HYP/Wellformed_C.thy @@ -612,6 +612,25 @@ 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" + by (simp add: ThreadState_defs mask_def)+ + end end diff --git a/proof/crefine/RISCV64/Wellformed_C.thy b/proof/crefine/RISCV64/Wellformed_C.thy index ad1989b612..47470b7c1d 100644 --- a/proof/crefine/RISCV64/Wellformed_C.thy +++ b/proof/crefine/RISCV64/Wellformed_C.thy @@ -556,6 +556,25 @@ 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" + by (simp add: ThreadState_defs mask_def)+ + (* generic lemmas with arch-specific consequences *) schematic_goal size_gpRegisters: diff --git a/proof/crefine/X64/Wellformed_C.thy b/proof/crefine/X64/Wellformed_C.thy index 66d4ec6df8..e690ba9592 100644 --- a/proof/crefine/X64/Wellformed_C.thy +++ b/proof/crefine/X64/Wellformed_C.thy @@ -614,6 +614,25 @@ 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" + by (simp add: ThreadState_defs mask_def)+ + end end From ba8ac9868ab732563e6104d5bb8ab710cd0c3063 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 10 Sep 2024 12:25:40 +0930 Subject: [PATCH 2/2] crefine: address Raf's comment and hopefully fix errors squash Signed-off-by: Michael McInerney --- proof/crefine/AARCH64/Syscall_C.thy | 3 --- proof/crefine/AARCH64/Wellformed_C.thy | 17 ++++++++++------- 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 | 17 ++++++++++------- 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 | 17 ++++++++++------- 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 | 17 ++++++++++------- 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 | 17 ++++++++++------- 18 files changed, 50 insertions(+), 74 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 cf7f44bbda..d47712e4e7 100644 --- 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 index 79d6f27ec5..456a9d5c17 100644 --- 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 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 c10f19631c..62138f8e8f 100644 --- 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 index f6e39812f7..6629b11fd6 100644 --- 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 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 237d6e3dee..d698661f90 100644 --- 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 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 47470b7c1d..1e16122630 100644 --- 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 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 e690ba9592..07ce28b5c7 100644 --- a/proof/crefine/X64/Wellformed_C.thy +++ b/proof/crefine/X64/Wellformed_C.thy @@ -617,20 +617,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