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

x64 refine: fix proofs after rebase and spec updates

This commit is contained in:
Matthew Brecknell 2017-04-24 22:11:02 +10:00
parent d4fc2de959
commit 2c742ed2c6
4 changed files with 21 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -624,7 +624,7 @@ lemma decode_page_inv_corres:
valid_cap (cap.ArchObjectCap
(arch_cap.PML4Cap wd (Some optv)))"
in corres_guard_imp)
apply (rule find_vspace_for_asid_corres)
apply (rule find_vspace_for_asid_corres[OF refl])
apply (clarsimp simp: valid_cap_def)
apply (simp add: mask_def)
apply assumption
@ -704,7 +704,7 @@ lemma decode_page_inv_corres:
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error, simp)
apply (rule find_vspace_for_asid_corres)
apply (rule find_vspace_for_asid_corres[OF refl])
apply (rule whenE_throwError_corres)
apply simp
apply simp
@ -785,7 +785,7 @@ lemma decode_page_table_inv_corres:
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error)
apply (rule find_vspace_for_asid_corres)
apply (rule find_vspace_for_asid_corres[OF refl])
apply (rule whenE_throwError_corres, simp, simp)
apply (rule corres_splitEE)
prefer 2
@ -887,7 +887,7 @@ lemma decode_page_directory_inv_corres:
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error)
apply (rule find_vspace_for_asid_corres)
apply (rule find_vspace_for_asid_corres[OF refl])
apply (rule whenE_throwError_corres, simp, simp)
apply (rule corres_splitEE)
prefer 2
@ -989,7 +989,7 @@ lemma decode_pdpt_inv_corres:
apply (rule corres_splitEE)
prefer 2
apply (rule corres_lookup_error)
apply (rule find_vspace_for_asid_corres)
apply (rule find_vspace_for_asid_corres[OF refl])
apply (rule whenE_throwError_corres, simp, simp)
apply (rule corres_splitEE)
prefer 2
@ -1195,7 +1195,7 @@ shows
apply (rule corres_splitEE)
prefer 2
apply simp
apply (rule get_asid_pool_corres_inv')
apply (rule get_asid_pool_corres_inv'[OF refl])
apply (simp add: bindE_assoc)
apply (rule corres_splitEE)
prefer 2

22
proof/refine/X64/Finalise_R.thy
View File

@ -3522,28 +3522,28 @@ lemma arch_finalise_cap_corres:
o_def dc_def[symmetric]
split: option.split,
safe)
apply (rule corres_guard_imp, rule delete_asid_pool_corres)
apply (rule corres_guard_imp, rule delete_asid_pool_corres[OF refl refl])
apply (clarsimp simp: valid_cap_def mask_def)
apply (clarsimp simp: valid_cap'_def)
apply auto[1]
apply (rule corres_guard_imp, rule unmap_page_corres)
apply (rule corres_guard_imp, rule unmap_page_corres[OF refl refl refl refl])
apply simp
apply (clarsimp simp: valid_cap_def valid_unmap_def)
apply (auto simp: vmsz_aligned_def pbfs_atleast_pageBits mask_def
elim: is_aligned_weaken invs_valid_asid_map)[2]
apply (rule corres_guard_imp, rule unmap_page_table_corres)
elim: is_aligned_weaken)[2]
apply (rule corres_guard_imp, rule unmap_page_table_corres[OF refl refl refl])
apply (auto simp: valid_cap_def valid_cap'_def mask_def bit_simps
elim!: is_aligned_weaken invs_valid_asid_map)[2]
apply (rule corres_guard_imp, rule unmap_pd_corres)
elim!: is_aligned_weaken)[2]
apply (rule corres_guard_imp, rule unmap_pd_corres[OF refl refl refl])
apply (auto simp: valid_cap_def valid_cap'_def mask_def bit_simps wellformed_mapdata_def
vmsz_aligned_def
elim!: is_aligned_weaken invs_valid_asid_map)[2]
apply (rule corres_guard_imp, rule unmap_pdpt_corres)
elim!: is_aligned_weaken)[2]
apply (rule corres_guard_imp, rule unmap_pdpt_corres[OF refl refl refl])
apply (auto simp: valid_cap_def valid_cap'_def mask_def bit_simps wellformed_mapdata_def
vmsz_aligned_def
elim!: is_aligned_weaken invs_valid_asid_map)[2]
apply (rule corres_guard_imp, rule delete_asid_corres)
apply (auto elim!: invs_valid_asid_map simp: mask_def valid_cap_def)[2]
elim!: is_aligned_weaken)[2]
apply (rule corres_guard_imp, rule delete_asid_corres[OF refl refl])
apply (auto simp: mask_def valid_cap_def)[2]
done

2
proof/refine/X64/Schedule_R.thy
View File

@ -226,7 +226,7 @@ lemma arch_switch_thread_corres:
(arch_switch_to_thread t) (Arch.switchToThread t)"
apply (simp add: arch_switch_to_thread_def X64_H.switchToThread_def)
apply (rule corres_guard_imp)
apply (rule set_vm_root_corres)
apply (rule set_vm_root_corres[OF refl])
apply (clarsimp simp: st_tcb_at_tcb_at)
apply (clarsimp simp: valid_pspace'_def)
done

25
proof/refine/X64/VSpace_R.thy
View File

@ -1806,11 +1806,7 @@ lemma unmap_pd_corres:
simp: lookup_failure_map_def pdpte_relation_def
split: X64_A.pdpte.splits)
apply simp
apply (rule corres_split_nor[OF _ flush_all_corres[OF _ refl]])
prefer 2
(* FIXME x64: change Haskell spec so that invalidateASID takes a word,
and unmapPageDirectory uses fromPPtr instead of addrFromPPtr *)
subgoal sorry
apply (rule corres_split_nor[OF _ flush_all_corres[OF refl refl]])
apply (rule corres_split[OF invalidate_local_page_structure_cache_asid_corres
store_pdpte_corres'])
apply ((wpsimp wp: get_pdpte_wp simp: pdpte_at_def)+)[8]
@ -1933,11 +1929,7 @@ lemma unmap_pdpt_corres:
simp: lookup_failure_map_def pml4e_relation_def
split: X64_A.pml4e.splits)
apply simp
apply (rule corres_split_nor[OF _ flush_all_corres[OF _ refl]])
prefer 2
(* FIXME x64: change Haskell spec so that invalidateASID takes a word,
and unmapPageDirectory uses fromPPtr instead of addrFromPPtr *)
subgoal sorry
apply (rule corres_split_nor[OF _ flush_all_corres[OF refl refl]])
apply (rule store_pml4e_corres'[OF refl], simp)
apply ((wpsimp wp: get_pml4e_wp simp: pml4e_at_def)+)[5]
apply (wpsimp wp: hoare_drop_imps)
@ -3122,16 +3114,6 @@ lemmas storePDE_Invalid_invs = storePDE_invs[where pde=InvalidPDE, simplified]
lemmas storePDPTE_Invalid_invs = storePDPTE_invs[where pde=InvalidPDPTE, simplified]
lemmas storePML4E_Invalid_invs = storePML4E_invs[where pde=InvalidPML4E, simplified]
lemma dmo_writeCR3_invs'[wp]:
"\<lbrace>invs'\<rbrace> doMachineOp (writeCR3 a b) \<lbrace>\<lambda>_. invs'\<rbrace>"
apply (wp dmo_invs' no_irq_writeCR3 no_irq)
apply clarsimp
apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = underlying_memory m p"
in use_valid[where P=P and Q="\<lambda>_. P" for P])
apply (simp add: writeCR3_def machine_op_lift_def
machine_rest_lift_def split_def | wp)+
done
(* FIXME x64: move*)
lemma no_irq_invalidateTranslationSingleASID[wp]:
"no_irq (invalidateTranslationSingleASID a b)"
@ -3299,8 +3281,7 @@ crunch valid_pde'[wp]: pteCheckIfMapped, pdeCheckIfMapped "valid_pde' pde"
lemma perform_pt_invs [wp]:
notes no_irq[wp]
shows
"\<lbrace>invs' and valid_page_inv' pt\<rbrace> performPageInvocation pt \<lbrace>\<lambda>_. invs'\<rbrace>"
shows "\<lbrace>invs' and valid_page_inv' pt\<rbrace> performPageInvocation pt \<lbrace>\<lambda>_. invs'\<rbrace>"
apply (simp add: performPageInvocation_def)
apply (cases pt)
apply clarsimp