diff --git a/proof/crefine/AARCH64/Finalise_C.thy b/proof/crefine/AARCH64/Finalise_C.thy index ce4a38f214..939f62ed25 100644 --- a/proof/crefine/AARCH64/Finalise_C.thy +++ b/proof/crefine/AARCH64/Finalise_C.thy @@ -965,7 +965,7 @@ lemma unbindMaybeNotification_ccorres: (* On ARM, irqInvalid is 2^16-1 (i.e. -1 in 16-bit), which, by type, is always greater than maxIRQ *) (* This means we could remove the cirq \ irqInvalid part in the Some clause. Currently left in for - proof convencience *) + proof convenience *) definition irq_opt_relation :: "irq option \ machine_word \ bool" where "irq_opt_relation airq cirq \ case airq of diff --git a/proof/crefine/ARM/Finalise_C.thy b/proof/crefine/ARM/Finalise_C.thy index 6756444dd3..63181b8ae0 100644 --- a/proof/crefine/ARM/Finalise_C.thy +++ b/proof/crefine/ARM/Finalise_C.thy @@ -929,7 +929,7 @@ lemma unbindMaybeNotification_ccorres: (* On ARM, irqInvalid is 2^16-1 (i.e. -1 in 16-bit), which, by type, is always greater than maxIRQ *) (* This means we could remove the cirq \ irqInvalid part in the Some clause. Currently left in for - proof convencience *) + proof convenience *) definition irq_opt_relation :: "irq option \ machine_word \ bool" where "irq_opt_relation airq cirq \ case airq of diff --git a/proof/crefine/ARM_HYP/Finalise_C.thy b/proof/crefine/ARM_HYP/Finalise_C.thy index 2172eadadf..e72c634003 100644 --- a/proof/crefine/ARM_HYP/Finalise_C.thy +++ b/proof/crefine/ARM_HYP/Finalise_C.thy @@ -963,7 +963,7 @@ lemma unbindMaybeNotification_ccorres: (* On ARM, irqInvalid is 2^16-1 (i.e. -1 in 16-bit), which, by type, is always greater than maxIRQ *) (* This means we could remove the cirq \ irqInvalid part in the Some clause. Currently left in for - proof convencience *) + proof convenience *) definition irq_opt_relation :: "irq option \ machine_word \ bool" where "irq_opt_relation airq cirq \ case airq of diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index d54fc1d452..1c73871530 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -274,7 +274,7 @@ lemma handleSyscall_ccorres: apply (subst ccorres_seq_skip'[symmetric]) apply (rule ccorres_split_nothrow_novcg) apply (rule_tac R=\ and xf=xfdc in ccorres_when) - apply (case_tac rv; clarsimp simp: irq_type_never_invalid) + apply (auto simp: irq_type_never_invalid split: option.splits)[1] apply (ctac (no_vcg) add: handleInterrupt_ccorres) apply ceqv apply (rule_tac r=dc and xf=xfdc in ccorres_returnOk_skip[unfolded returnOk_def,simplified]) @@ -303,7 +303,7 @@ lemma handleSyscall_ccorres: apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_Guard)? apply (rule_tac R=\ and xf=xfdc in ccorres_when) - apply (case_tac rv; clarsimp simp: irq_type_never_invalid) + apply (auto simp: irq_type_never_invalid split: option.splits)[1] apply (ctac (no_vcg) add: handleInterrupt_ccorres) apply ceqv apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified]) @@ -331,7 +331,7 @@ lemma handleSyscall_ccorres: apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_Guard)? apply (rule_tac R=\ and xf=xfdc in ccorres_when) - apply (case_tac rv; clarsimp simp: irq_type_never_invalid) + apply (auto simp: irq_type_never_invalid split: option.splits)[1] apply (ctac (no_vcg) add: handleInterrupt_ccorres) apply ceqv apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified]) diff --git a/spec/abstract/X64/ArchInterrupt_A.thy b/spec/abstract/X64/ArchInterrupt_A.thy index c0edee4eb5..a8bb69b689 100644 --- a/spec/abstract/X64/ArchInterrupt_A.thy +++ b/spec/abstract/X64/ArchInterrupt_A.thy @@ -32,7 +32,7 @@ end context begin interpretation Arch . -(* On Arm architectures, maxIRQ is defined in Kernel_Config. On RISCV64 it is defined manually. *) +(* On Arm architectures, maxIRQ is defined in Kernel_Config. On X64 it is defined manually. *) requalify_consts maxIRQ diff --git a/spec/design/skel/AARCH64/ArchInterrupt_H.thy b/spec/design/skel/AARCH64/ArchInterrupt_H.thy index 91bdcb12cb..e3adf88154 100644 --- a/spec/design/skel/AARCH64/ArchInterrupt_H.thy +++ b/spec/design/skel/AARCH64/ArchInterrupt_H.thy @@ -15,10 +15,6 @@ begin context Arch begin global_naming AARCH64_H -(* Kernel_Config provides a generic numeral, Haskell expects type irq *) -abbreviation (input) maxIRQ :: irq where - "maxIRQ == Kernel_Config.maxIRQ" - #INCLUDE_HASKELL SEL4/Object/Interrupt/AARCH64.hs CONTEXT AARCH64_H bodies_only ArchInv= Arch= NOT plic_complete_claim end diff --git a/spec/design/skel/ARM/ArchInterrupt_H.thy b/spec/design/skel/ARM/ArchInterrupt_H.thy index e4adda77f9..0c1a5ee861 100644 --- a/spec/design/skel/ARM/ArchInterrupt_H.thy +++ b/spec/design/skel/ARM/ArchInterrupt_H.thy @@ -15,10 +15,6 @@ begin context Arch begin global_naming ARM_H -(* Kernel_Config provides a generic numeral, Haskell expects type irq *) -abbreviation (input) maxIRQ :: irq where - "maxIRQ == Kernel_Config.maxIRQ" - #INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs Arch= CONTEXT ARM_H bodies_only ArchInv= end diff --git a/spec/design/skel/ARM_HYP/ArchInterrupt_H.thy b/spec/design/skel/ARM_HYP/ArchInterrupt_H.thy index 5d6b4fedc6..919733bdb6 100644 --- a/spec/design/skel/ARM_HYP/ArchInterrupt_H.thy +++ b/spec/design/skel/ARM_HYP/ArchInterrupt_H.thy @@ -15,10 +15,6 @@ begin context Arch begin global_naming ARM_HYP_H -(* Kernel_Config provides a generic numeral, Haskell expects type irq *) -abbreviation (input) maxIRQ :: irq where - "maxIRQ == Kernel_Config.maxIRQ" - #INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs Arch= CONTEXT ARM_HYP_H bodies_only ArchInv= NOT initInterruptController definition initInterruptController :: "unit kernel"