aarch64 machine+aspec+cspec: pt_type ghost+table array sizes
- add ghost state corresponding to gsPTTypes in Haskell and ASpec - add ghost type comments - style update for old definitions since we need to touch most of these - define vs/pt_array_len for use in C annotations - make NormalPT_T/VSRootPT_T names available for use in C annotations Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
parent
57f60084e8
commit
4add4bdbf2
|
|
@ -113,48 +113,7 @@ definition pte_base_addr :: "pte \<Rightarrow> paddr" where
|
|||
definition ppn_from_pptr :: "obj_ref \<Rightarrow> ppn" where
|
||||
"ppn_from_pptr p = ucast (addrFromPPtr p >> pageBits)"
|
||||
|
||||
definition vs_index_bits :: nat where
|
||||
"vs_index_bits \<equiv> if config_ARM_PA_SIZE_BITS_40 then 10 else (9::nat)"
|
||||
|
||||
lemma vs_index_bits_ge0[simp, intro!]: "0 < vs_index_bits"
|
||||
by (simp add: vs_index_bits_def)
|
||||
|
||||
(* A dependent-ish type in Isabelle. We use typedef here instead of value_type so that we can
|
||||
retain a symbolic value (vs_index_bits) for the size of the type instead of getting a plain
|
||||
number such as 9 or 10. *)
|
||||
typedef vs_index_len = "{n :: nat. n < vs_index_bits}" by auto
|
||||
|
||||
end
|
||||
|
||||
instantiation AARCH64_A.vs_index_len :: len0
|
||||
begin
|
||||
interpretation Arch .
|
||||
definition len_of_vs_index_len: "len_of (x::vs_index_len itself) \<equiv> CARD(vs_index_len)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation AARCH64_A.vs_index_len :: len
|
||||
begin
|
||||
interpretation Arch .
|
||||
instance
|
||||
proof
|
||||
show "0 < LENGTH(vs_index_len)"
|
||||
by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])
|
||||
qed
|
||||
end
|
||||
|
||||
context Arch begin global_naming AARCH64_A
|
||||
|
||||
type_synonym vs_index = "vs_index_len word"
|
||||
|
||||
type_synonym pt_index_len = 9
|
||||
type_synonym pt_index = "pt_index_len word"
|
||||
|
||||
text \<open>Sanity check:\<close>
|
||||
lemma length_vs_index_len[simp]:
|
||||
"LENGTH(vs_index_len) = vs_index_bits"
|
||||
by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])
|
||||
|
||||
(* Sanity check for page table type sizes -- ptTranslationBits not yet available at definition site *)
|
||||
lemma vs_index_ptTranslationBits:
|
||||
"ptTranslationBits VSRootPT_T = LENGTH(vs_index_len)"
|
||||
by (simp add: ptTranslationBits_def vs_index_bits_def)
|
||||
|
|
|
|||
|
|
@ -18,6 +18,8 @@ context begin interpretation Arch .
|
|||
|
||||
requalify_types
|
||||
machine_state
|
||||
pt_array_len
|
||||
vs_array_len
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -25,54 +27,73 @@ declare [[populate_globals=true]]
|
|||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
||||
type_synonym cghost_state = "(machine_word \<rightharpoonup> vmpage_size) * (machine_word \<rightharpoonup> nat)
|
||||
* ghost_assertions"
|
||||
(* Sanity checks for array sizes. ptTranslationBits not yet available at definition site. *)
|
||||
lemma ptTranslationBits_vs_index_bits:
|
||||
"ptTranslationBits VSRootPT_T = vs_index_bits"
|
||||
by (simp add: ptTranslationBits_def vs_index_bits_def)
|
||||
|
||||
definition
|
||||
gs_clear_region :: "addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
|
||||
(* FIXME AARCH64: this is guaranteed to always succeed even though config_ARM_PA_SIZE_BITS_40
|
||||
is unfolded. It'd be nicer if we could also get something symbolic out of value_type, though *)
|
||||
lemma ptTranslationBits_vs_array_len':
|
||||
"2 ^ ptTranslationBits VSRootPT_T = vs_array_len"
|
||||
by (simp add: vs_array_len_def ptTranslationBits_vs_index_bits vs_index_bits_def
|
||||
Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
|
||||
|
||||
lemmas ptTranslationBits_vs_array_len = ptTranslationBits_vs_array_len'[unfolded vs_array_len_def]
|
||||
|
||||
type_synonym cghost_state =
|
||||
"(machine_word \<rightharpoonup> vmpage_size) \<times> \<comment> \<open>Frame sizes\<close>
|
||||
(machine_word \<rightharpoonup> nat) \<times> \<comment> \<open>CNode sizes\<close>
|
||||
(machine_word \<rightharpoonup> pt_type) \<times> \<comment> \<open>PT types\<close>
|
||||
ghost_assertions" \<comment> \<open>ASMRefine assertions\<close>
|
||||
|
||||
definition gs_clear_region :: "addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
|
||||
"gs_clear_region ptr bits gs \<equiv>
|
||||
(%x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x,
|
||||
%x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x, snd (snd gs))"
|
||||
(\<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x,
|
||||
\<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x,
|
||||
\<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd (snd gs)) x,
|
||||
snd (snd (snd gs)))"
|
||||
|
||||
definition
|
||||
gs_new_frames:: "vmpage_size \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
|
||||
where
|
||||
definition gs_new_frames:: "vmpage_size \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
|
||||
"gs_new_frames sz ptr bits \<equiv> \<lambda>gs.
|
||||
if bits < pageBitsForSize sz then gs
|
||||
else (\<lambda>x. if \<exists>n\<le>mask (bits - pageBitsForSize sz).
|
||||
x = ptr + n * 2 ^ pageBitsForSize sz then Some sz
|
||||
else fst gs x, snd gs)"
|
||||
if bits < pageBitsForSize sz then gs
|
||||
else (\<lambda>x. if \<exists>n\<le>mask (bits - pageBitsForSize sz).
|
||||
x = ptr + n * 2 ^ pageBitsForSize sz then Some sz
|
||||
else fst gs x, snd gs)"
|
||||
|
||||
definition
|
||||
gs_new_cnodes:: "nat \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
|
||||
where
|
||||
definition gs_new_cnodes:: "nat \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
|
||||
"gs_new_cnodes sz ptr bits \<equiv> \<lambda>gs.
|
||||
if bits < sz + 4 then gs
|
||||
else (fst gs, \<lambda>x. if \<exists>n\<le>mask (bits - sz - 4). x = ptr + n * 2 ^ (sz + 4)
|
||||
then Some sz
|
||||
else fst (snd gs) x, snd (snd gs))"
|
||||
if bits < sz + 4 then gs
|
||||
else (fst gs, \<lambda>x. if \<exists>n\<le>mask (bits - sz - 4). x = ptr + n * 2 ^ (sz + 4)
|
||||
then Some sz
|
||||
else fst (snd gs) x, snd (snd gs))"
|
||||
|
||||
abbreviation
|
||||
gs_get_assn :: "int \<Rightarrow> cghost_state \<Rightarrow> machine_word"
|
||||
where
|
||||
"gs_get_assn k \<equiv> ghost_assertion_data_get k (snd o snd)"
|
||||
definition gs_new_pt_t:: "pt_type \<Rightarrow> addr \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
|
||||
"gs_new_pt_t pt_t ptr \<equiv>
|
||||
\<lambda>gs. (fst gs, fst (snd gs), (fst (snd (snd gs))) (ptr \<mapsto> pt_t), snd (snd (snd gs)))"
|
||||
|
||||
abbreviation
|
||||
gs_set_assn :: "int \<Rightarrow> machine_word \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
|
||||
where
|
||||
"gs_set_assn k v \<equiv> ghost_assertion_data_set k v (apsnd o apsnd)"
|
||||
abbreviation gs_get_assn :: "int \<Rightarrow> cghost_state \<Rightarrow> machine_word" where
|
||||
"gs_get_assn k \<equiv> ghost_assertion_data_get k (snd \<circ> snd \<circ> snd)"
|
||||
|
||||
abbreviation gs_set_assn :: "int \<Rightarrow> machine_word \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
|
||||
"gs_set_assn k v \<equiv> ghost_assertion_data_set k v (apsnd \<circ> apsnd \<circ> apsnd)"
|
||||
|
||||
declare [[record_codegen = false]]
|
||||
declare [[allow_underscore_idents = true]]
|
||||
|
||||
end
|
||||
|
||||
(* workaround for the fact that the C parser wants to know the vmpage sizes*)
|
||||
(* Workaround for the fact that the retype annotations need the vmpage sizes*)
|
||||
(* create appropriately qualified aliases *)
|
||||
context begin interpretation Arch . global_naming vmpage_size
|
||||
requalify_consts ARMSmallPage ARMLargePage ARMHugePage
|
||||
end
|
||||
|
||||
(* Also need pt_type constructors for retype annotations. We leave them available globally for C. *)
|
||||
context begin interpretation Arch .
|
||||
requalify_consts NormalPT_T VSRootPT_T
|
||||
end
|
||||
|
||||
definition
|
||||
ctcb_size_bits :: nat
|
||||
where
|
||||
|
|
|
|||
|
|
@ -101,5 +101,64 @@ definition irqVTimerEvent :: irq where
|
|||
definition pageColourBits :: nat where
|
||||
"pageColourBits \<equiv> undefined" \<comment> \<open>not implemented on this platform\<close>
|
||||
|
||||
|
||||
section \<open>Page table sizes\<close>
|
||||
|
||||
definition vs_index_bits :: nat where
|
||||
"vs_index_bits \<equiv> if config_ARM_PA_SIZE_BITS_40 then 10 else (9::nat)"
|
||||
|
||||
end
|
||||
|
||||
(* Need to declare code equation outside Arch locale *)
|
||||
declare AARCH64.vs_index_bits_def[code]
|
||||
|
||||
context Arch begin global_naming AARCH64
|
||||
|
||||
lemma vs_index_bits_ge0[simp, intro!]: "0 < vs_index_bits"
|
||||
by (simp add: vs_index_bits_def)
|
||||
|
||||
(* A dependent-ish type in Isabelle. We use typedef here instead of value_type so that we can
|
||||
retain a symbolic value (vs_index_bits) for the size of the type instead of getting a plain
|
||||
number such as 9 or 10. *)
|
||||
typedef vs_index_len = "{n :: nat. n < vs_index_bits}" by auto
|
||||
|
||||
end
|
||||
|
||||
instantiation AARCH64.vs_index_len :: len0
|
||||
begin
|
||||
interpretation Arch .
|
||||
definition len_of_vs_index_len: "len_of (x::vs_index_len itself) \<equiv> CARD(vs_index_len)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation AARCH64.vs_index_len :: len
|
||||
begin
|
||||
interpretation Arch .
|
||||
instance
|
||||
proof
|
||||
show "0 < LENGTH(vs_index_len)"
|
||||
by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])
|
||||
qed
|
||||
end
|
||||
|
||||
context Arch begin global_naming AARCH64
|
||||
|
||||
type_synonym vs_index = "vs_index_len word"
|
||||
|
||||
type_synonym pt_index_len = 9
|
||||
type_synonym pt_index = "pt_index_len word"
|
||||
|
||||
text \<open>Sanity check:\<close>
|
||||
lemma length_vs_index_len[simp]:
|
||||
"LENGTH(vs_index_len) = vs_index_bits"
|
||||
by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])
|
||||
|
||||
|
||||
section \<open>C array sizes corresponding to page table sizes\<close>
|
||||
|
||||
value_type pt_array_len = "(2::nat) ^ LENGTH(pt_index_len)"
|
||||
value_type vs_array_len = "(2::nat) ^ vs_index_bits"
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue