From e152c9e364a34c7aee07d00423e034643c7fcc82 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Wed, 31 Jul 2024 16:53:29 +1000 Subject: [PATCH] refine+crefine: update for arch_requalify design spec updates Signed-off-by: Rafal Kolanski --- proof/crefine/AARCH64/Invoke_C.thy | 4 ++-- proof/crefine/AARCH64/Retype_C.thy | 6 +++--- proof/crefine/ARM/Invoke_C.thy | 4 ++-- proof/crefine/ARM/Retype_C.thy | 6 +++--- proof/crefine/ARM_HYP/Invoke_C.thy | 4 ++-- proof/crefine/ARM_HYP/Retype_C.thy | 6 +++--- proof/crefine/RISCV64/Invoke_C.thy | 4 ++-- proof/crefine/RISCV64/Retype_C.thy | 6 +++--- proof/crefine/X64/Invoke_C.thy | 4 ++-- proof/crefine/X64/Retype_C.thy | 6 +++--- proof/refine/AARCH64/Syscall_R.thy | 2 +- proof/refine/ARM/Syscall_R.thy | 2 +- proof/refine/ARM/orphanage/Orphanage.thy | 8 ++++---- proof/refine/ARM_HYP/Syscall_R.thy | 2 +- proof/refine/RISCV64/Syscall_R.thy | 2 +- proof/refine/X64/Syscall_R.thy | 2 +- 16 files changed, 34 insertions(+), 34 deletions(-) diff --git a/proof/crefine/AARCH64/Invoke_C.thy b/proof/crefine/AARCH64/Invoke_C.thy index 15b994746a..e74e29273c 100644 --- a/proof/crefine/AARCH64/Invoke_C.thy +++ b/proof/crefine/AARCH64/Invoke_C.thy @@ -2812,10 +2812,10 @@ lemma ctes_of_ex_cte_cap_to': lemma Arch_isFrameType_spec: - "\s. \ \ \s. unat \type \ fromEnum (maxBound::ArchTypes_H.object_type)\ + "\s. \ \ \s. unat \type \ fromEnum (maxBound::object_type)\ Call Arch_isFrameType_'proc \ \ret__unsigned_long = - from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\" + from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\" apply vcg apply (simp add: toEnum_object_type_to_H) apply (frule object_type_from_to_H) diff --git a/proof/crefine/AARCH64/Retype_C.thy b/proof/crefine/AARCH64/Retype_C.thy index 20481e5bd0..ba8b9a0df9 100644 --- a/proof/crefine/AARCH64/Retype_C.thy +++ b/proof/crefine/AARCH64/Retype_C.thy @@ -5047,7 +5047,7 @@ lemma placeNewObject_user_data: done definition - createObject_hs_preconds :: "machine_word \ ArchTypes_H.object_type \ nat \ bool \ kernel_state \ bool" + createObject_hs_preconds :: "machine_word \ object_type \ nat \ bool \ kernel_state \ bool" where "createObject_hs_preconds regionBase newType userSize d \ (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize) @@ -5070,14 +5070,14 @@ abbreviation (* these preconds actually used throughout the proof *) abbreviation(input) - createObject_c_preconds1 :: "machine_word \ ArchTypes_H.object_type \ nat \ bool \ (globals myvars) set" + createObject_c_preconds1 :: "machine_word \ object_type \ nat \ bool \ (globals myvars) set" where "createObject_c_preconds1 regionBase newType userSize deviceMemory \ {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}" (* these preconds used at start of proof *) definition - createObject_c_preconds :: "machine_word \ ArchTypes_H.object_type \ nat \ bool \ (globals myvars) set" + createObject_c_preconds :: "machine_word \ object_type \ nat \ bool \ (globals myvars) set" where "createObject_c_preconds regionBase newType userSize deviceMemory \ (createObject_c_preconds1 regionBase newType userSize deviceMemory diff --git a/proof/crefine/ARM/Invoke_C.thy b/proof/crefine/ARM/Invoke_C.thy index 9cccf1178e..524f811aeb 100644 --- a/proof/crefine/ARM/Invoke_C.thy +++ b/proof/crefine/ARM/Invoke_C.thy @@ -2623,10 +2623,10 @@ lemma ctes_of_ex_cte_cap_to': lemma Arch_isFrameType_spec: - "\s. \ \ \s. unat \type \ fromEnum (maxBound::ArchTypes_H.object_type)\ + "\s. \ \ \s. unat \type \ fromEnum (maxBound::object_type)\ Call Arch_isFrameType_'proc \ \ret__unsigned_long = - from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\" + from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\" apply vcg apply (simp add: toEnum_object_type_to_H) apply (frule object_type_from_to_H) diff --git a/proof/crefine/ARM/Retype_C.thy b/proof/crefine/ARM/Retype_C.thy index f72ef05c28..b0b5fd33ec 100644 --- a/proof/crefine/ARM/Retype_C.thy +++ b/proof/crefine/ARM/Retype_C.thy @@ -4350,7 +4350,7 @@ lemma placeNewObject_user_data: definition - createObject_hs_preconds :: "word32 \ ArchTypes_H.object_type \ nat \ bool \ kernel_state \ bool" + createObject_hs_preconds :: "word32 \ object_type \ nat \ bool \ kernel_state \ bool" where "createObject_hs_preconds regionBase newType userSize d \ (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize) @@ -4373,14 +4373,14 @@ abbreviation (* these preconds actually used throughout the proof *) abbreviation(input) - createObject_c_preconds1 :: "word32 \ ArchTypes_H.object_type \ nat \ bool \ (globals myvars) set" + createObject_c_preconds1 :: "word32 \ object_type \ nat \ bool \ (globals myvars) set" where "createObject_c_preconds1 regionBase newType userSize deviceMemory \ {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}" (* these preconds used at start of proof *) definition - createObject_c_preconds :: "word32 \ ArchTypes_H.object_type \ nat \ bool \ (globals myvars) set" + createObject_c_preconds :: "word32 \ object_type \ nat \ bool \ (globals myvars) set" where "createObject_c_preconds regionBase newType userSize deviceMemory \ (createObject_c_preconds1 regionBase newType userSize deviceMemory diff --git a/proof/crefine/ARM_HYP/Invoke_C.thy b/proof/crefine/ARM_HYP/Invoke_C.thy index 103d13b238..84432c6231 100644 --- a/proof/crefine/ARM_HYP/Invoke_C.thy +++ b/proof/crefine/ARM_HYP/Invoke_C.thy @@ -2828,10 +2828,10 @@ lemma ctes_of_ex_cte_cap_to': lemma Arch_isFrameType_spec: - "\s. \ \ \s. unat \type \ fromEnum (maxBound::ArchTypes_H.object_type)\ + "\s. \ \ \s. unat \type \ fromEnum (maxBound::object_type)\ Call Arch_isFrameType_'proc \ \ret__unsigned_long = - from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\" + from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\" apply vcg apply (simp add: toEnum_object_type_to_H) apply (frule object_type_from_to_H) diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy index be5ff3990e..a6762ccc4e 100644 --- a/proof/crefine/ARM_HYP/Retype_C.thy +++ b/proof/crefine/ARM_HYP/Retype_C.thy @@ -4919,7 +4919,7 @@ lemma placeNewObject_user_data: definition - createObject_hs_preconds :: "word32 \ ArchTypes_H.object_type \ nat \ bool \ kernel_state \ bool" + createObject_hs_preconds :: "word32 \ object_type \ nat \ bool \ kernel_state \ bool" where "createObject_hs_preconds regionBase newType userSize d \ (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize) @@ -4942,14 +4942,14 @@ abbreviation (* these preconds actually used throughout the proof *) abbreviation(input) - createObject_c_preconds1 :: "word32 \ ArchTypes_H.object_type \ nat \ bool \ (globals myvars) set" + createObject_c_preconds1 :: "word32 \ object_type \ nat \ bool \ (globals myvars) set" where "createObject_c_preconds1 regionBase newType userSize deviceMemory \ {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}" (* these preconds used at start of proof *) definition - createObject_c_preconds :: "word32 \ ArchTypes_H.object_type \ nat \ bool \ (globals myvars) set" + createObject_c_preconds :: "word32 \ object_type \ nat \ bool \ (globals myvars) set" where "createObject_c_preconds regionBase newType userSize deviceMemory \ (createObject_c_preconds1 regionBase newType userSize deviceMemory diff --git a/proof/crefine/RISCV64/Invoke_C.thy b/proof/crefine/RISCV64/Invoke_C.thy index f74814a574..b521bd42b2 100644 --- a/proof/crefine/RISCV64/Invoke_C.thy +++ b/proof/crefine/RISCV64/Invoke_C.thy @@ -2774,10 +2774,10 @@ lemma ctes_of_ex_cte_cap_to': lemma Arch_isFrameType_spec: - "\s. \ \ \s. unat \type \ fromEnum (maxBound::ArchTypes_H.object_type)\ + "\s. \ \ \s. unat \type \ fromEnum (maxBound::object_type)\ Call Arch_isFrameType_'proc \ \ret__unsigned_long = - from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\" + from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\" apply vcg apply (simp add: toEnum_object_type_to_H) apply (frule object_type_from_to_H) diff --git a/proof/crefine/RISCV64/Retype_C.thy b/proof/crefine/RISCV64/Retype_C.thy index 77d931c5e0..539221b01c 100644 --- a/proof/crefine/RISCV64/Retype_C.thy +++ b/proof/crefine/RISCV64/Retype_C.thy @@ -4796,7 +4796,7 @@ lemma placeNewObject_user_data: done definition - createObject_hs_preconds :: "machine_word \ ArchTypes_H.object_type \ nat \ bool \ kernel_state \ bool" + createObject_hs_preconds :: "machine_word \ object_type \ nat \ bool \ kernel_state \ bool" where "createObject_hs_preconds regionBase newType userSize d \ (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize) @@ -4819,14 +4819,14 @@ abbreviation (* these preconds actually used throughout the proof *) abbreviation(input) - createObject_c_preconds1 :: "machine_word \ ArchTypes_H.object_type \ nat \ bool \ (globals myvars) set" + createObject_c_preconds1 :: "machine_word \ object_type \ nat \ bool \ (globals myvars) set" where "createObject_c_preconds1 regionBase newType userSize deviceMemory \ {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}" (* these preconds used at start of proof *) definition - createObject_c_preconds :: "machine_word \ ArchTypes_H.object_type \ nat \ bool \ (globals myvars) set" + createObject_c_preconds :: "machine_word \ object_type \ nat \ bool \ (globals myvars) set" where "createObject_c_preconds regionBase newType userSize deviceMemory \ (createObject_c_preconds1 regionBase newType userSize deviceMemory diff --git a/proof/crefine/X64/Invoke_C.thy b/proof/crefine/X64/Invoke_C.thy index 3c24ca6970..9b94f45d7a 100644 --- a/proof/crefine/X64/Invoke_C.thy +++ b/proof/crefine/X64/Invoke_C.thy @@ -2800,10 +2800,10 @@ lemma ctes_of_ex_cte_cap_to': lemma Arch_isFrameType_spec: - "\s. \ \ \s. unat \type \ fromEnum (maxBound::ArchTypes_H.object_type)\ + "\s. \ \ \s. unat \type \ fromEnum (maxBound::object_type)\ Call Arch_isFrameType_'proc \ \ret__unsigned_long = - from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\" + from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\" apply vcg apply (simp add: toEnum_object_type_to_H) apply (frule object_type_from_to_H) diff --git a/proof/crefine/X64/Retype_C.thy b/proof/crefine/X64/Retype_C.thy index f2963a8ff8..122be6b735 100644 --- a/proof/crefine/X64/Retype_C.thy +++ b/proof/crefine/X64/Retype_C.thy @@ -5628,7 +5628,7 @@ lemma placeNewObject_user_data: done definition - createObject_hs_preconds :: "machine_word \ ArchTypes_H.object_type \ nat \ bool \ kernel_state \ bool" + createObject_hs_preconds :: "machine_word \ object_type \ nat \ bool \ kernel_state \ bool" where "createObject_hs_preconds regionBase newType userSize d \ (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize) @@ -5651,14 +5651,14 @@ abbreviation (* these preconds actually used throughout the proof *) abbreviation(input) - createObject_c_preconds1 :: "machine_word \ ArchTypes_H.object_type \ nat \ bool \ (globals myvars) set" + createObject_c_preconds1 :: "machine_word \ object_type \ nat \ bool \ (globals myvars) set" where "createObject_c_preconds1 regionBase newType userSize deviceMemory \ {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}" (* these preconds used at start of proof *) definition - createObject_c_preconds :: "machine_word \ ArchTypes_H.object_type \ nat \ bool \ (globals myvars) set" + createObject_c_preconds :: "machine_word \ object_type \ nat \ bool \ (globals myvars) set" where "createObject_c_preconds regionBase newType userSize deviceMemory \ (createObject_c_preconds1 regionBase newType userSize deviceMemory diff --git a/proof/refine/AARCH64/Syscall_R.thy b/proof/refine/AARCH64/Syscall_R.thy index 79466cd0cc..8a5061f324 100644 --- a/proof/refine/AARCH64/Syscall_R.thy +++ b/proof/refine/AARCH64/Syscall_R.thy @@ -535,7 +535,7 @@ crunch InterruptDecls_H.invokeIRQHandler for typ_at'[wp]: "\s. P (typ_at' T p s)" lemmas invokeIRQHandler_typ_ats[wp] = - typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at'] + typ_at_lifts [OF invokeIRQHandler_typ_at'] crunch setDomain for tcb_at'[wp]: "tcb_at' tptr" diff --git a/proof/refine/ARM/Syscall_R.thy b/proof/refine/ARM/Syscall_R.thy index 422530076f..1b6188b32e 100644 --- a/proof/refine/ARM/Syscall_R.thy +++ b/proof/refine/ARM/Syscall_R.thy @@ -526,7 +526,7 @@ crunch InterruptDecls_H.invokeIRQHandler for typ_at'[wp]: "\s. P (typ_at' T p s)" lemmas invokeIRQHandler_typ_ats[wp] = - typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at'] + typ_at_lifts [OF invokeIRQHandler_typ_at'] crunch setDomain for tcb_at'[wp]: "tcb_at' tptr" diff --git a/proof/refine/ARM/orphanage/Orphanage.thy b/proof/refine/ARM/orphanage/Orphanage.thy index 60d9e6ba12..efe187dda3 100644 --- a/proof/refine/ARM/orphanage/Orphanage.thy +++ b/proof/refine/ARM/orphanage/Orphanage.thy @@ -1797,11 +1797,11 @@ lemma invokeIRQControl_no_orphans [wp]: apply (wp | clarsimp)+ done -lemma invokeIRQHandler_no_orphans [wp]: +lemma arch_invokeIRQHandler_no_orphans[wp]: "\ \s. no_orphans s \ invs' s \ - invokeIRQHandler i + ARM_H.invokeIRQHandler i \ \reply s. no_orphans s \" - apply (cases i, simp_all add: invokeIRQHandler_def) + apply (cases i, simp_all add: ARM_H.invokeIRQHandler_def) apply (wp | clarsimp | fastforce)+ done @@ -1939,7 +1939,7 @@ lemma setDomain_no_orphans [wp]: apply (fastforce simp: tcb_at_typ_at' is_active_tcb_ptr_runnable') done -crunch InterruptDecls_H.invokeIRQHandler +crunch invokeIRQHandler for no_orphans[wp]: no_orphans lemma performInvocation_no_orphans [wp]: diff --git a/proof/refine/ARM_HYP/Syscall_R.thy b/proof/refine/ARM_HYP/Syscall_R.thy index 52873b90a3..80a53138fd 100644 --- a/proof/refine/ARM_HYP/Syscall_R.thy +++ b/proof/refine/ARM_HYP/Syscall_R.thy @@ -536,7 +536,7 @@ crunch InterruptDecls_H.invokeIRQHandler for typ_at'[wp]: "\s. P (typ_at' T p s)" lemmas invokeIRQHandler_typ_ats[wp] = - typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at'] + typ_at_lifts [OF invokeIRQHandler_typ_at'] crunch setDomain for tcb_at'[wp]: "tcb_at' tptr" diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 63b7ff5d2f..892fc1034d 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -534,7 +534,7 @@ crunch InterruptDecls_H.invokeIRQHandler for typ_at'[wp]: "\s. P (typ_at' T p s)" lemmas invokeIRQHandler_typ_ats[wp] = - typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at'] + typ_at_lifts [OF invokeIRQHandler_typ_at'] crunch setDomain for tcb_at'[wp]: "tcb_at' tptr" diff --git a/proof/refine/X64/Syscall_R.thy b/proof/refine/X64/Syscall_R.thy index cd9575f6a9..4db9157811 100644 --- a/proof/refine/X64/Syscall_R.thy +++ b/proof/refine/X64/Syscall_R.thy @@ -535,7 +535,7 @@ crunch InterruptDecls_H.invokeIRQHandler for typ_at'[wp]: "\s. P (typ_at' T p s)" lemmas invokeIRQHandler_typ_ats[wp] = - typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at'] + typ_at_lifts [OF invokeIRQHandler_typ_at'] crunch setDomain for tcb_at'[wp]: "tcb_at' tptr"