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

aarch64 ainvs: convert 2 FIXMEs into longer term issues (#601) 

Both of these affect other architectures and need more discussion.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-03-08 17:04:37 +11:00 committed by GitHub
parent a454a093c0
commit 9d5c8be3dc
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 1 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -771,7 +771,7 @@ lemmas simple_bit_simps =
lemmas table_bits_simps =
pt_bits_def[simplified] pte_bits_def[unfolded word_size_bits_def] vs_index_bits_def
named_theorems bit_simps (* FIXME AARCH64: shadows Word_Lib bit_simps *)
named_theorems bit_simps
lemmas [bit_simps] = table_bits_simps simple_bit_simps ipa_size_def valid_vs_slot_bits_def

1
proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy
View File

@ -543,7 +543,6 @@ crunches get_vmid, invalidate_asid_entry, invalidate_tlb_by_asid, invalidate_tlb
and cur[wp]: cur_tcb
and valid_objs[wp]: valid_objs
(* FIXME AARCH64: typ_at_lifts should include arch things *)
lemmas find_free_vmid_typ_ats[wp] = abs_typ_at_lifts [OF find_free_vmid_typ_at]
lemmas invalidate_asid_typ_ats[wp] = abs_typ_at_lifts [OF invalidate_asid_typ_at]
lemmas update_asid_pool_entry_typ_ats[wp] = abs_typ_at_lifts [OF update_asid_pool_entry_typ_at]