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

x64: ainvs+refine: fix up proofs for decodeX64FrameInvocation changes

This commit is contained in:
Joel Beeren 2018-06-29 12:12:30 +10:00
parent e6ca6883ad
commit 7f52da6571
2 changed files with 8 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/invariant-abstract/X64/ArchEmptyFail_AI.thy
View File

@ -66,7 +66,7 @@ lemma decode_tcb_invocation_empty_fail[wp]:
by (simp add: decode_tcb_invocation_def split: invocation_label.splits | wp | intro conjI impI)+
crunch (empty_fail) empty_fail[wp]: find_vspace_for_asid, check_vp_alignment,
ensure_safe_mapping, get_asid_pool, lookup_pt_slot,
ensure_safe_mapping, get_asid_pool, lookup_pt_slot, get_pt,
decode_port_invocation, decode_ioport_control_invocation
(simp: kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits
pdpte.splits pml4e.splits vmpage_size.splits Let_def)

12
proof/refine/X64/Arch_R.thy
View File

@ -651,7 +651,7 @@ lemma decode_page_inv_corres:
apply simp
apply (rule whenE_throwError_corres, simp, simp)
apply (rule_tac R="\<lambda>_ s. valid_vspace_objs s \<and> pspace_aligned s
\<and> (hd args && user_vtop) + (2 ^ pageBitsForSize sz - 1) \<le> user_vtop \<and>
\<and> (hd args && user_vtop) + (2 ^ pageBitsForSize sz) \<le> user_vtop \<and>
valid_arch_state s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and>
s \<turnstile> (fst (hd excaps)) \<and> (\<exists>\<rhd> (lookup_pml4_slot (obj_ref_of (fst (hd excaps))) (hd args) && ~~ mask pml4_bits)) s \<and>
(\<exists>\<rhd> rv') s \<and> page_map_l4_at rv' s"
@ -705,6 +705,7 @@ lemma decode_page_inv_corres:
apply (case_tac excaps', simp)
apply clarsimp
apply (rule corres_guard_imp)
apply (rule whenE_throwError_corres, simp, simp)
apply (rule corres_splitEE [where r' = "op ="])
prefer 2
apply (clarsimp simp: list_all2_Cons2)
@ -738,10 +739,11 @@ lemma decode_page_inv_corres:
apply (rule create_mapping_entries_corres)
apply (simp add: mask_vmrights_corres)
apply (simp add: vm_attributes_corres)
apply (rule corres_trivial)
apply (rule corres_returnOk)
apply (clarsimp simp: archinv_relation_def page_invocation_map_def)
apply (wp | simp)+
apply (rule corres_splitEE[OF _ ensure_safe_mapping_corres])
apply (rule corres_trivial)
apply (rule corres_returnOk)
apply (clarsimp simp: archinv_relation_def page_invocation_map_def)
apply (wp createMappingEntries_wf | simp)+
apply (rule_tac Q'="\<lambda>rv s. valid_vspace_objs s \<and> pspace_aligned s \<and>
(snd v') < pptr_base \<and> canonical_address (snd v') \<and>
equal_kernel_mappings s \<and> valid_global_objs s \<and> valid_arch_state s \<and>