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

aarch64 ainvs: update lemmas for cur_vcpu and vmid 

These are required as interface for Invariants_AI (and generally useful)

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-04-14 10:25:25 +10:00 committed by Gerwin Klein
parent f49386bb09
commit 9a0c45a7ea
1 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy
View File

@ -2687,6 +2687,10 @@ lemma vspace_for_asid_update[iff]:
"vspace_for_asid asid (f s) = vspace_for_asid asid s"
by (simp add: vspace_for_asid_def obind_def split: option.splits)
lemma vmid_for_asid_update[iff]:
"vmid_for_asid asid (f s) = vmid_for_asid asid s"
by (simp add: vmid_for_asid_def obind_def)
lemma vs_lookup_update [iff]:
"vs_lookup_table bot_level asid vptr (f s) = vs_lookup_table bot_level asid vptr s"
by (auto simp: vs_lookup_table_def pspace arch obind_def split: option.splits)
@ -2719,6 +2723,14 @@ lemma equal_kernel_mappings_update [iff]:
"equal_kernel_mappings (f s) = equal_kernel_mappings s"
by (simp add: equal_kernel_mappings_def pspace)
lemma cur_vcpu_update [iff]:
"cur_vcpu (f s) = cur_vcpu s"
by (simp add: cur_vcpu_def arch split: option.splits)
lemma vmid_inv_update [iff]:
"vmid_inv (f s) = vmid_inv s"
by (simp add: vmid_inv_def arch is_inv_def swp_def)
end
declare AARCH64.arch_tcb_context_absorbs[simp]