Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Arch-split overhaul for design spec #809

Merged
merged 4 commits into from
Aug 19, 2024
Merged

Arch-split overhaul for design spec #809

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d8ef271
machine: requalify more machine op consts and types
Xaphiosis Jul 31, 2024
1fc58ab
design m-skel: use arch_global_naming and arch_requalify
Xaphiosis Jul 30, 2024
7e538e4
design: deploy arch_requalify infrastructure
Xaphiosis Jul 30, 2024
e152c9e
refine+crefine: update for arch_requalify design spec updates
Xaphiosis Jul 31, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions proof/crefine/AARCH64/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2812,10 +2812,10 @@ lemma ctes_of_ex_cte_cap_to':


lemma Arch_isFrameType_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
Call Arch_isFrameType_'proc
\<lbrace> \<acute>ret__unsigned_long =
from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
apply vcg
apply (simp add: toEnum_object_type_to_H)
apply (frule object_type_from_to_H)
Expand Down
6 changes: 3 additions & 3 deletions proof/crefine/AARCH64/Retype_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5047,7 +5047,7 @@ lemma placeNewObject_user_data:
done

definition
createObject_hs_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
createObject_hs_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"createObject_hs_preconds regionBase newType userSize d \<equiv>
(invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
Expand All @@ -5070,14 +5070,14 @@ abbreviation

(* these preconds actually used throughout the proof *)
abbreviation(input)
createObject_c_preconds1 :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
createObject_c_preconds1 :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
where
"createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
{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 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
createObject_c_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
where
"createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
(createObject_c_preconds1 regionBase newType userSize deviceMemory
Expand Down
4 changes: 2 additions & 2 deletions proof/crefine/ARM/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2623,10 +2623,10 @@ lemma ctes_of_ex_cte_cap_to':


lemma Arch_isFrameType_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
Call Arch_isFrameType_'proc
\<lbrace> \<acute>ret__unsigned_long =
from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
apply vcg
apply (simp add: toEnum_object_type_to_H)
apply (frule object_type_from_to_H)
Expand Down
6 changes: 3 additions & 3 deletions proof/crefine/ARM/Retype_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4350,7 +4350,7 @@ lemma placeNewObject_user_data:


definition
createObject_hs_preconds :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
createObject_hs_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"createObject_hs_preconds regionBase newType userSize d \<equiv>
(invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
Expand All @@ -4373,14 +4373,14 @@ abbreviation

(* these preconds actually used throughout the proof *)
abbreviation(input)
createObject_c_preconds1 :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
createObject_c_preconds1 :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
where
"createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
{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 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
createObject_c_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
where
"createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
(createObject_c_preconds1 regionBase newType userSize deviceMemory
Expand Down
4 changes: 2 additions & 2 deletions proof/crefine/ARM_HYP/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2828,10 +2828,10 @@ lemma ctes_of_ex_cte_cap_to':


lemma Arch_isFrameType_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
Call Arch_isFrameType_'proc
\<lbrace> \<acute>ret__unsigned_long =
from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
apply vcg
apply (simp add: toEnum_object_type_to_H)
apply (frule object_type_from_to_H)
Expand Down
6 changes: 3 additions & 3 deletions proof/crefine/ARM_HYP/Retype_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4919,7 +4919,7 @@ lemma placeNewObject_user_data:


definition
createObject_hs_preconds :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
createObject_hs_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"createObject_hs_preconds regionBase newType userSize d \<equiv>
(invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
Expand All @@ -4942,14 +4942,14 @@ abbreviation

(* these preconds actually used throughout the proof *)
abbreviation(input)
createObject_c_preconds1 :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
createObject_c_preconds1 :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
where
"createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
{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 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
createObject_c_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
where
"createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
(createObject_c_preconds1 regionBase newType userSize deviceMemory
Expand Down
4 changes: 2 additions & 2 deletions proof/crefine/RISCV64/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2774,10 +2774,10 @@ lemma ctes_of_ex_cte_cap_to':


lemma Arch_isFrameType_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
Call Arch_isFrameType_'proc
\<lbrace> \<acute>ret__unsigned_long =
from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
apply vcg
apply (simp add: toEnum_object_type_to_H)
apply (frule object_type_from_to_H)
Expand Down
6 changes: 3 additions & 3 deletions proof/crefine/RISCV64/Retype_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4796,7 +4796,7 @@ lemma placeNewObject_user_data:
done

definition
createObject_hs_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
createObject_hs_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"createObject_hs_preconds regionBase newType userSize d \<equiv>
(invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
Expand All @@ -4819,14 +4819,14 @@ abbreviation

(* these preconds actually used throughout the proof *)
abbreviation(input)
createObject_c_preconds1 :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
createObject_c_preconds1 :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
where
"createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
{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 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
createObject_c_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
where
"createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
(createObject_c_preconds1 regionBase newType userSize deviceMemory
Expand Down
4 changes: 2 additions & 2 deletions proof/crefine/X64/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2800,10 +2800,10 @@ lemma ctes_of_ex_cte_cap_to':


lemma Arch_isFrameType_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
Call Arch_isFrameType_'proc
\<lbrace> \<acute>ret__unsigned_long =
from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
apply vcg
apply (simp add: toEnum_object_type_to_H)
apply (frule object_type_from_to_H)
Expand Down
6 changes: 3 additions & 3 deletions proof/crefine/X64/Retype_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5628,7 +5628,7 @@ lemma placeNewObject_user_data:
done

definition
createObject_hs_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
createObject_hs_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"createObject_hs_preconds regionBase newType userSize d \<equiv>
(invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
Expand All @@ -5651,14 +5651,14 @@ abbreviation

(* these preconds actually used throughout the proof *)
abbreviation(input)
createObject_c_preconds1 :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
createObject_c_preconds1 :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
where
"createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
{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 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
createObject_c_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
where
"createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
(createObject_c_preconds1 regionBase newType userSize deviceMemory
Expand Down
2 changes: 1 addition & 1 deletion proof/refine/AARCH64/Syscall_R.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -535,7 +535,7 @@ crunch InterruptDecls_H.invokeIRQHandler
for typ_at'[wp]: "\<lambda>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"
Expand Down
2 changes: 1 addition & 1 deletion proof/refine/ARM/Syscall_R.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -526,7 +526,7 @@ crunch InterruptDecls_H.invokeIRQHandler
for typ_at'[wp]: "\<lambda>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"
Expand Down
8 changes: 4 additions & 4 deletions proof/refine/ARM/orphanage/Orphanage.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1797,11 +1797,11 @@ lemma invokeIRQControl_no_orphans [wp]:
apply (wp | clarsimp)+
done

lemma invokeIRQHandler_no_orphans [wp]:
lemma arch_invokeIRQHandler_no_orphans[wp]:
"\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
invokeIRQHandler i
ARM_H.invokeIRQHandler i
\<lbrace> \<lambda>reply s. no_orphans s \<rbrace>"
apply (cases i, simp_all add: invokeIRQHandler_def)
apply (cases i, simp_all add: ARM_H.invokeIRQHandler_def)
apply (wp | clarsimp | fastforce)+
done

Expand Down Expand Up @@ -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]:
Expand Down
2 changes: 1 addition & 1 deletion proof/refine/ARM_HYP/Syscall_R.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -536,7 +536,7 @@ crunch InterruptDecls_H.invokeIRQHandler
for typ_at'[wp]: "\<lambda>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"
Expand Down
2 changes: 1 addition & 1 deletion proof/refine/RISCV64/Syscall_R.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -534,7 +534,7 @@ crunch InterruptDecls_H.invokeIRQHandler
for typ_at'[wp]: "\<lambda>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"
Expand Down
2 changes: 1 addition & 1 deletion proof/refine/X64/Syscall_R.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -535,7 +535,7 @@ crunch InterruptDecls_H.invokeIRQHandler
for typ_at'[wp]: "\<lambda>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"
Expand Down
18 changes: 7 additions & 11 deletions spec/design/m-skel/AARCH64/MachineTypes.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ imports
Platform
begin

context Arch begin global_naming AARCH64
context Arch begin arch_global_naming

#INCLUDE_SETTINGS keep_constructor=hyp_fault_type
#INCLUDE_SETTINGS keep_constructor=virt_timer
Expand All @@ -33,11 +33,9 @@ section "Types"

end

context begin interpretation Arch .
requalify_types register vcpureg vppievent_irq virt_timer
end
arch_requalify_types register vcpureg vppievent_irq virt_timer

context Arch begin global_naming AARCH64
context Arch begin arch_global_naming

#INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 instanceproofs
#INCLUDE_HASKELL SEL4/Object/Structures/AARCH64.hs CONTEXT AARCH64 instanceproofs ONLY VPPIEventIRQ VirtTimer
Expand Down Expand Up @@ -73,7 +71,7 @@ where

end_qualify

context Arch begin global_naming AARCH64
context Arch begin arch_global_naming

text \<open>
The machine monad is used for operations on the state defined above.
Expand All @@ -85,7 +83,7 @@ end
translations
(type) "'c AARCH64.machine_monad" <= (type) "(AARCH64.machine_state, 'c) nondet_monad"

context Arch begin global_naming AARCH64
context Arch begin arch_global_naming

text \<open>
After kernel initialisation all IRQs are masked.
Expand Down Expand Up @@ -122,11 +120,9 @@ definition

end

context begin interpretation Arch .
requalify_types vmpage_size
end
arch_requalify_types vmpage_size

context Arch begin global_naming AARCH64
context Arch begin arch_global_naming

#INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs CONTEXT AARCH64 instanceproofs ONLY VMFaultType HypFaultType VMPageSize

Expand Down
18 changes: 7 additions & 11 deletions spec/design/m-skel/ARM/MachineTypes.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ imports
Platform
begin

context Arch begin global_naming ARM
context Arch begin arch_global_naming

text \<open>
An implementation of the machine's types, defining register set
Expand All @@ -29,11 +29,9 @@ section "Types"

end

context begin interpretation Arch .
requalify_types register
end
arch_requalify_types register

context Arch begin global_naming ARM
context Arch begin arch_global_naming

#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM instanceproofs
(*>*)
Expand Down Expand Up @@ -83,7 +81,7 @@ where

end_qualify

context Arch begin global_naming ARM
context Arch begin arch_global_naming

text \<open>
The machine monad is used for operations on the state defined above.
Expand All @@ -95,7 +93,7 @@ end
translations
(type) "'c ARM.machine_monad" <= (type) "(ARM.machine_state, 'c) nondet_monad"

context Arch begin global_naming ARM
context Arch begin arch_global_naming

text \<open>
After kernel initialisation all IRQs are masked.
Expand Down Expand Up @@ -137,11 +135,9 @@ definition

end

context begin interpretation Arch .
requalify_types vmpage_size
end
arch_requalify_types vmpage_size

context Arch begin global_naming ARM
context Arch begin arch_global_naming

#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs CONTEXT ARM instanceproofs ONLY HardwareASID VMFaultType VMPageSize HypFaultType

Expand Down
Loading
Loading