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

AInvs: cleaner way to express ARM page table alignment

This commit is contained in:
Japheth Lim 2019-01-31 17:46:19 +11:00
parent 016a5d33ac
commit 3fc4166e7e
4 changed files with 5 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/infoflow/Example_Valid_State.thy
View File

@ -1268,7 +1268,7 @@ lemma valid_obj_s0[simp]:
Low_pt_ptr_def High_pt_ptr_def
shared_page_ptr_def
valid_vm_rights_def vm_kernel_only_def
kernel_base_def pageBits_def vmsz_aligned_def
kernel_base_def pageBits_def pt_bits_def vmsz_aligned_def
is_aligned_def[THEN meta_eq_to_obj_eq, THEN iffD2]
is_aligned_addrFromPPtr_n)+
apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def

3
proof/invariant-abstract/ARM/ArchArch_AI.thy
View File

@ -1507,7 +1507,8 @@ lemma arch_decode_inv_wf[wp]:
apply (clarsimp simp: neq_Nil_conv)
apply (thin_tac "Ball S P" for S P)
apply (rule conjI)
apply (clarsimp simp: valid_cap_def cap_aligned_def is_aligned_addrFromPPtr_n)
apply (clarsimp simp: valid_cap_def cap_aligned_def
pt_bits_def pageBits_def is_aligned_addrFromPPtr_n)
apply (rule conjI)
apply (clarsimp simp: valid_cap_def cap_aligned_def)
apply (rule conjI)

4
proof/invariant-abstract/ARM/ArchInvariants_AI.thy
View File

@ -308,9 +308,7 @@ definition
where
"wellformed_pde pde \<equiv> case pde of
pde.PageTablePDE p attr mw \<Rightarrow>
attr \<subseteq> {ParityEnabled}
\<comment> \<open>We don't have a variant of this alignment check that takes an @{const APageTable}. Yuck.\<close>
\<and> is_aligned p (arch_obj_size (PageTableCap undefined undefined))
attr \<subseteq> {ParityEnabled} \<and> is_aligned p pt_bits
| pde.SectionPDE p attr mw r \<Rightarrow>
r \<in> valid_vm_rights \<and> vmsz_aligned p ARMSection
| pde.SuperSectionPDE p attr r \<Rightarrow>

3
proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
View File

@ -324,8 +324,7 @@ definition
where
"wellformed_pde pde \<equiv> case pde of
pde.PageTablePDE p \<Rightarrow>
\<comment> \<open>We don't have a variant of this alignment check that takes an @{const APageTable}. Yuck.\<close>
is_aligned p (arch_obj_size (PageTableCap undefined undefined))
is_aligned p pt_bits
| pde.SectionPDE p attr r \<Rightarrow>
r \<in> valid_vm_rights \<and> vmsz_aligned p ARMSection
| pde.SuperSectionPDE p attr r \<Rightarrow>