adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

aarch64 aspec: adjust for Haskell-defined PT type 

This includes a new type for ptTranslationBits, which is also shared
from Haskell.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-05-05 15:38:44 +10:00 committed by Gerwin Klein
parent 8ff19483a8
commit d87cf0bed8
2 changed files with 6 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
spec/abstract/AARCH64/ArchVSpaceAcc_A.thy
View File

@ -125,13 +125,13 @@ section "Basic Operations"
definition pt_bits_left :: "vm_level \<Rightarrow> nat" where
"pt_bits_left level =
(if level = asid_pool_level
then ptTranslationBits True + ptTranslationBits False * size max_pt_level
else ptTranslationBits False * size level)
then ptTranslationBits VSRootPT_T + ptTranslationBits NormalPT_T * size max_pt_level
else ptTranslationBits NormalPT_T * size level)
+ pageBits"
definition pt_index :: "vm_level \<Rightarrow> vspace_ref \<Rightarrow> machine_word" where
"pt_index level vptr \<equiv>
(vptr >> pt_bits_left level) && mask (ptTranslationBits (level = max_pt_level))"
(vptr >> pt_bits_left level) && mask (ptTranslationBits (level_type level))"
locale_abbrev global_pt :: "'z state \<Rightarrow> obj_ref" where

8
spec/abstract/AARCH64/Arch_Structs_A.thy
View File

@ -29,8 +29,6 @@ text \<open>
along with capabilities for virtual memory mappings.
\<close>
datatype pt_type = VSRoot_T | Normal_T
datatype arch_cap =
ASIDPoolCap
(acap_obj : obj_ref)
@ -121,11 +119,11 @@ lemma length_vs_index_len[simp]:
by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])
lemma vs_index_ptTranslationBits:
"ptTranslationBits True = LENGTH(vs_index_len)"
"ptTranslationBits VSRootPT_T = LENGTH(vs_index_len)"
by (simp add: ptTranslationBits_def vs_index_bits_def)
lemma pt_index_ptTranslationBits:
"ptTranslationBits False = LENGTH(pt_index_len)"
"ptTranslationBits NormalPT_T = LENGTH(pt_index_len)"
by (simp add: ptTranslationBits_def)
(* This could also be a record, but we expect further alternatives to be added for SMMU *)
@ -205,7 +203,7 @@ definition pte_bits :: nat where
"pte_bits = word_size_bits"
definition table_size :: "pt_type \<Rightarrow> nat" where
"table_size pt_t = ptTranslationBits (pt_t = VSRoot_T) + pte_bits" (* FIXME AARCH64: introduce levels in Haskell, include from there *)
"table_size pt_t = ptTranslationBits pt_t + pte_bits"
definition pt_bits :: "pt_type \<Rightarrow> nat" where
"pt_bits pt_t \<equiv> table_size pt_t"