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

x64: progress in ArchAcc_R

This commit is contained in:
Joel Beeren 2017-03-22 18:06:21 +11:00
parent 28c13ef778
commit 72f6b33659
2 changed files with 726 additions and 470 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1183
proof/refine/X64/ArchAcc_R.thy
View File

File diff suppressed because it is too large Load Diff

13
proof/refine/X64/Bits_R.thy
View File

@ -128,6 +128,16 @@ lemma projectKO_PDE:
by (cases ko)
(auto simp: projectKO_opts_defs split: arch_kernel_object.splits)
lemma projectKO_PDPTE:
"(projectKO_opt ko = Some t) = (ko = KOArch (KOPDPTE t))"
by (cases ko)
(auto simp: projectKO_opts_defs split: arch_kernel_object.splits)
lemma projectKO_PML4E:
"(projectKO_opt ko = Some t) = (ko = KOArch (KOPML4E t))"
by (cases ko)
(auto simp: projectKO_opts_defs split: arch_kernel_object.splits)
lemma projectKO_user_data:
"(projectKO_opt ko = Some (t :: user_data)) = (ko = KOUserData)"
by (cases ko)
@ -141,7 +151,8 @@ lemma projectKO_user_data_device:
lemmas projectKOs =
projectKO_ntfn projectKO_ep projectKO_cte projectKO_tcb
projectKO_ASID projectKO_PTE projectKO_PDE projectKO_user_data projectKO_user_data_device
projectKO_ASID projectKO_PTE projectKO_PDE projectKO_PDPTE projectKO_PML4E
projectKO_user_data projectKO_user_data_device
projectKO_eq projectKO_eq2
lemma capAligned_epI: