From 0ac198fab5f9f172b00df67dfda7c076554146e1 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 24 Jul 2019 15:46:41 +1000 Subject: [PATCH] riscv refine: Arch_R sorry-free --- proof/refine/RISCV64/Arch_R.thy | 319 ++++++++++++++++---------------- 1 file changed, 162 insertions(+), 157 deletions(-) diff --git a/proof/refine/RISCV64/Arch_R.thy b/proof/refine/RISCV64/Arch_R.thy index 5f2067a0b..81cc557b7 100644 --- a/proof/refine/RISCV64/Arch_R.thy +++ b/proof/refine/RISCV64/Arch_R.thy @@ -16,8 +16,25 @@ theory Arch_R imports Untyped_R Finalise_R begin +(* FIXME RISCV: move to Corres, replace option_corres *) +lemma option_corres: + assumes None: "\ x = None; x' = None \ \ corres_underlying sr nf nf' r P P' (A None) (C None)" + assumes Some: "\z z'. \ x = Some z; x' = Some z' \ \ + corres_underlying sr nf nf' r (Q z) (Q' z') (A (Some z)) (C (Some z'))" + assumes None_eq: "(x = None) = (x' = None)" + shows "corres_underlying sr nf nf' r (\s. (x = None \ P s) \ (\z. x = Some z \ Q z s)) + (\s. (x' = None \ P' s) \ (\z. x' = Some z \ Q' z s)) + (A x) (C x')" + apply (cases x; cases x'; simp add: assms) + apply (simp add: None flip: None_eq) + apply (simp flip: None_eq) + done + +lemmas [datatype_schematic] = cap.sel list.sel(1) list.sel(3) + context begin interpretation Arch . (*FIXME: arch_split*) +declare arch_cap.sel [datatype_schematic] declare is_aligned_shiftl [intro!] declare is_aligned_shiftr [intro!] @@ -416,11 +433,6 @@ lemma asidHighBits [simp]: declare word_unat_power [symmetric, simp del] -(* FIXME RISCV: decodeMMU: undefined -> fail -crunch inv [wp]: "RISCV64_H.decodeInvocation" "P" - (wp: crunch_wps mapME_x_inv_wp getASID_wp - simp: forME_x_def crunch_simps - ignore: forME_x getObject) *) lemma case_option_corresE: assumes nonec: "corres r Pn Qn (nc >>=E f) (nc' >>=E g)" @@ -452,26 +464,66 @@ lemma select_ext_fap: = return (free_asid_pool_select p b)" by (simp add: select_ext_def get_def gets_def bind_def assert_def return_def) -(* FIXME RISCV -lemma find_vspace_for_asid_lookup_slot [wp]: - "\pspace_aligned and valid_vspace_objs\ - find_vspace_for_asid asid - \\rv. \\ (lookup_pml4_slot rv vptr && ~~ mask pml4_bits)\, -" - apply (rule hoare_pre) - apply (rule hoare_post_imp_R) - apply (rule hoare_vcg_R_conj) - apply (rule hoare_vcg_R_conj) - apply (rule find_vspace_for_asid_inv [where P="\", THEN valid_validE_R]) - apply (rule find_vspace_for_asid_lookup) - apply (rule find_vspace_for_asid_aligned_pm) - apply clarsimp - apply (subst lookup_pml4_slot_eq) - apply (auto simp: bit_simps) - done *) - lemmas vmsz_aligned_imp_aligned = vmsz_aligned_def[THEN meta_eq_to_obj_eq, THEN iffD1, THEN is_aligned_weaken] +lemma check_slot_corres: + "(\pte pte'. pte_relation' pte pte' \ test' pte' = test pte) \ + corres (ser \ dc) + (pte_at p and pspace_aligned and pspace_distinct) \ + (check_slot p test) + (checkSlot p test')" + apply (simp add: check_slot_def checkSlot_def unlessE_whenE liftE_bindE) + apply (rule corres_guard_imp) + apply (rule corres_split[OF _ get_pte_corres]) + apply (rule corres_whenE, simp) + apply (rule corres_trivial, simp) + apply simp + apply wpsimp+ + done + +lemma vmrights_map_vm_kernel_only[simp]: + "vmrights_map vm_kernel_only = VMKernelOnly" + by (simp add: vmrights_map_def vm_kernel_only_def) + +lemma not_in_vm_kernel_only[simp]: + "x \ vm_kernel_only" + by (simp add: vm_kernel_only_def) + +lemma vmrights_map_VMKernelOnly: + "vmrights_map (mask_vm_rights R r) = VMKernelOnly \ mask_vm_rights R r = vm_kernel_only" + by (auto simp: vmrights_map_def mask_vm_rights_def validate_vm_rights_def vm_read_write_def + vm_read_only_def split: if_splits) + +lemma machine_word_len_pageBits_shift[simp]: (* 52 = machine_word_len - pageBits *) + "UCAST(52 \ machine_word_len) (UCAST(machine_word_len \ 52) (p >> pageBits)) = p >> pageBits" + apply (simp add: ucast_ucast_mask pageBits_def) + apply word_bitwise + apply (simp add: word_size) + done + +lemma pte_relation_make_user[simp]: + "pte_relation' + (make_user_pte p (attribs_from_word a) (mask_vm_rights R (data_to_rights r))) + (makeUserPTE p (\attribsFromWord a) (maskVMRights (vmrights_map R) (rightsFromWord r)))" + by (auto simp: make_user_pte_def makeUserPTE_def attribs_from_word_def user_attr_def + attribsFromWord_def mask_vmrights_corres vmrights_map_VMKernelOnly) + +lemma below_user_vtop_in_user_region: + "p < user_vtop \ p \ user_region" + apply (simp add: user_region_def canonical_user_def user_vtop_def pptrUserTop_def RISCV64.pptrUserTop_def) + apply (simp add: bit_simps is_aligned_mask canonical_bit_def) + by (word_bitwise, clarsimp simp: word_size) + +lemma vmsz_aligned_user_region: + "\ vmsz_aligned p sz; p + (2 ^ pageBitsForSize sz - 1) < RISCV64_H.pptrUserTop \ + \ p \ user_region" + using pbfs_atleast_pageBits[of sz] + apply (simp flip: mask_2pm1 add: vmsz_aligned_def) + apply (simp add: user_region_def canonical_user_def pptrUserTop_def RISCV64.pptrUserTop_def) + apply (simp add: bit_simps is_aligned_mask canonical_bit_def word_plus_and_or_coroll) + by (word_bitwise, clarsimp simp: word_size) + lemma decode_page_inv_corres: "\cap = arch_cap.FrameCap p R sz d opt; acap_relation cap cap'; list_all2 cap_relation (map fst excaps) (map fst excaps'); @@ -493,162 +545,138 @@ lemma decode_page_inv_corres: apply (elim exE conjE) apply (simp split: list.split, intro conjI impI allI, simp_all)[1] apply (simp add: decodeRISCVFrameInvocationMap_def) + apply (rule whenE_throwError_corres_initial) + apply simp + apply (fastforce simp: mdata_map_def) + apply (simp split: cap.split, intro conjI impI allI, simp_all)[1] + apply (rename_tac arch_capa) + apply (case_tac arch_capa, simp_all)[1] + apply (rename_tac wd opt') + apply (case_tac opt'; simp add: mdata_map_def) + apply (rename_tac av, case_tac av, simp) + apply (rename_tac a v) apply (rule corres_guard_imp) - apply (rule whenE_throwError_corres) - apply simp - apply (fastforce simp: mdata_map_def) - apply (simp split: cap.split, intro conjI impI allI, simp_all)[1] - apply (rename_tac arch_capa) - apply (case_tac arch_capa, simp_all)[1] - apply (rename_tac wd opt') - apply (case_tac opt'; clarsimp simp: mdata_map_def) - apply (rename_tac optv) apply (rule corres_splitEE) prefer 2 - apply (rule corres_lookup_error) sorry (* FIXME RISCV - apply (rule_tac P="valid_arch_state and valid_vspace_objs and - pspace_aligned and equal_kernel_mappings and valid_global_objs and - valid_cap (cap.ArchObjectCap - (arch_cap.PageTableCap wd (Some optv)))" - in corres_guard_imp) - apply (rule find_vspace_for_asid_corres[OF refl]) - apply (clarsimp simp: valid_cap_def) - apply simp + apply (rule corres_lookup_error) + apply (rule find_vspace_for_asid_corres[OF refl]) apply (rule whenE_throwError_corres, simp, simp) - apply (rule_tac R="\_ s. valid_vspace_objs s \ pspace_aligned s - \ hd args + (2 ^ pageBitsForSize sz) \ user_vtop \ hd args \ user_vtop \ - valid_arch_state s \ equal_kernel_mappings s \ valid_global_objs s \ - s \ (fst (hd excaps)) \ (\\ (lookup_pml4_slot (obj_ref_of (fst (hd excaps))) (hd args) && ~~ mask pml4_bits)) s \ - (\\ rv') s \ page_map_l4_at rv' s" - and R'="\_ s. s \' (fst (hd excaps')) \ valid_objs' s \ - pspace_aligned' s \ pspace_distinct' s \ - valid_arch_state' s" - in corres_splitEE) + apply (rule corres_splitEE[where r'=dc]) prefer 2 apply (rule corres_whenE) - apply (simp add: pptr_base_def RISCV64.pptrBase_def pptrBase_def shiftl_t2n mask_def) + apply (simp add: pptr_base_def user_vtop_def pptrUserTop_def shiftl_t2n mask_def) apply (rule corres_trivial, simp) apply simp - apply (rule corres_guard_imp) + apply (rule corres_splitEE[where r'=dc]) + prefer 2 + apply (rule check_vp_corres) apply (rule corres_splitEE) prefer 2 - apply (rule check_vp_corres) - apply (rule corres_splitEE) + apply (simp only: corres_liftE_rel_sum) + apply (rule lookup_pt_slot_corres) + apply (clarsimp simp: unlessE_whenE) + apply (rule corres_splitEE[where r'=dc]) prefer 2 - apply (simp only: addrFromPPtr_def) - apply (rule create_mapping_entries_corres) - apply (simp add: mask_vmrights_corres) - apply (simp add: vm_attributes_corres) - apply (rule corres_splitEE) + apply datatype_schem + apply (rule corres_whenE, simp) + apply (rule corres_trivial, clarsimp simp: lookup_failure_map_def) + apply simp + apply (rule corres_splitEE[where r'=dc]) prefer 2 - apply (erule ensure_safe_mapping_corres) - apply (rule corres_trivial) - apply (rule corres_returnOk) - apply (clarsimp simp: archinv_relation_def page_invocation_map_def) - apply (wpsimp wp: hoare_whenE_wp check_vp_wpR createMappingEntries_wf)+ - apply (clarsimp simp: valid_cap_def) - apply (frule_tac vptr="hd args && user_vtop" in page_map_l4_pml4e_at_lookupI, assumption) - apply (clarsimp simp: vmsz_aligned_def pageBitsForSize_def is_aligned_pml4 - split: vmpage_size.splits) - apply (clarsimp simp: valid_cap'_def) - apply (simp add: mask_def) - apply (rule whenE_throwError_wp[unfolded validE_R_def]) - apply (wp hoare_whenE_wp)+ - apply (rule hoare_drop_imps)+ - apply (simp add:mask_def not_less) - apply (wp hoare_drop_imps find_vspace_for_asid_lookup_slot[unfolded mask_def, simplified])+ - apply (clarsimp simp: invs_def valid_state_def valid_pspace_def) + apply (rule check_slot_corres) + apply auto[1] + apply (rule corres_trivial, rule corres_returnOk) + apply (clarsimp simp: archinv_relation_def page_invocation_map_def mapping_map_def) + apply (wpsimp simp: if_apply_def2 + wp: validE_validE_R[OF find_vspace_for_asid_wp, simplified])+ + apply (clarsimp simp: invs_psp_aligned invs_distinct invs_vspace_objs invs_valid_asid_table + cte_wp_at_caps_of_state is_arch_diminished_def is_cap_simps) + apply (rule conjI; clarsimp?) + apply (clarsimp simp: valid_cap_def wellformed_mapdata_def) + apply (rule conjI) + apply (rule exI)+ + apply (rule conjI, erule vspace_for_asid_vs_lookup, simp) + apply (rule conjI) + apply (simp add: not_le vmsz_aligned_user_region[unfolded pptrUserTop_def] mask_def user_vtop_def) + apply clarsimp + apply (drule (1) pt_lookup_slot_vs_lookup_slotI, clarsimp) + apply (erule vs_lookup_slot_pte_at; assumption?) + apply (simp add: not_le vmsz_aligned_user_region[unfolded pptrUserTop_def] mask_def user_vtop_def) apply fastforce - \ \PageRemap\ - apply (cases "invocation_type l = ArchInvocationLabel RISCV64PageRemap") + \ \PageRemap\ + apply (cases "invocation_type l = ArchInvocationLabel RISCVPageRemap") apply (case_tac "\(1 < length args \ excaps \ [])") - subgoal by (auto split: list.split) + subgoal by (auto simp: decode_fr_inv_remap_def split: list.split) apply (simp add: Let_def split: list.split) apply (case_tac args, simp) apply (clarsimp simp: split_def) apply (rename_tac w1 w2 w3) apply (case_tac excaps', simp) + apply (clarsimp simp: decode_fr_inv_remap_def decodeRISCVFrameInvocationRemap_def) + apply (clarsimp simp: list_all2_Cons2) + apply (case_tac "fst (hd excaps)"; simp) apply clarsimp + apply (rename_tac arch_capa arch_capb) + apply (case_tac arch_capa; simp) + apply (rename_tac opt') + apply (case_tac opt'; simp) + apply (rename_tac av, case_tac av, simp) + apply (cases opt; clarsimp simp: mdata_map_def) apply (rule corres_guard_imp) - apply (rule whenE_throwError_corres, simp, simp) - apply (rule corres_splitEE [where r' = "(=)"]) + apply (rule corres_splitEE) prefer 2 - apply (clarsimp simp: list_all2_Cons2) - apply (case_tac "fst (hd excaps)", simp_all)[1] - apply clarsimp - apply (rename_tac arch_capa arch_capb) - apply (case_tac arch_capa, simp_all)[1] - apply (rename_tac opt') - apply (case_tac opt', simp_all)[1] - apply (rule corres_returnOkTT) - apply simp - apply (simp add: Let_def split: list.split) - apply (rule case_option_corresE) - apply (rule corres_trivial) - apply simp - apply simp + apply (rule corres_lookup_error) + apply (rule find_vspace_for_asid_corres[OF refl]) + apply (rule whenE_throwError_corres, clarsimp) + apply (clarsimp simp: up_ucast_inj_eq) apply (rule corres_splitEE) prefer 2 - apply (rule corres_lookup_error, simp) - apply (rule find_vspace_for_asid_corres[OF refl]) - apply (rule whenE_throwError_corres) - apply simp - apply simp - apply simp + apply (rule check_vp_corres) apply (rule corres_splitEE) prefer 2 - apply (rule check_vp_corres) + apply simp + apply (rule lookup_pt_slot_corres) + apply (clarsimp simp: unlessE_whenE) + apply datatype_schem + apply (rule whenE_throwError_corres, simp add: lookup_failure_map_def) + apply simp apply (rule corres_splitEE) prefer 2 - apply (simp only: addrFromPPtr_def) - apply (rule create_mapping_entries_corres) - apply (simp add: mask_vmrights_corres) - apply (simp add: vm_attributes_corres) - 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'="\rv s. valid_vspace_objs s \ pspace_aligned s \ - (snd v') < pptr_base \ canonical_address (snd v') \ - equal_kernel_mappings s \ valid_global_objs s \ valid_arch_state s \ - \ \(\\ (lookup_pml4_slot (fst pa) (snd v') && ~~ mask pml4_bits)) s \\ - page_map_l4_at rv s \ (\\ rv) s" - in hoare_post_imp_R, wp) - apply (clarsimp simp: page_directory_at_aligned_pd_bits valid_global_objs_def) - apply (auto intro!: page_directory_pde_at_lookupI elim!: is_aligned_pml4)[1] - apply wp - apply (wpc | wp throwE_R | wp (once) hoare_drop_imps)+ + apply (rule check_slot_corres) + apply (case_tac pte; simp add: is_PageTablePTE_def RISCV64_H.isPageTablePTE_def) + apply (rule corres_trivial, rule corres_returnOk, simp) + apply (clarsimp simp: archinv_relation_def page_invocation_map_def mapping_map_def) + apply wpsimp+ + apply (clarsimp simp: invs_psp_aligned invs_distinct invs_vspace_objs invs_valid_asid_table + cte_wp_at_caps_of_state is_arch_diminished_def is_cap_simps) + apply (rule conjI; clarsimp?) + apply (clarsimp simp: valid_cap_def wellformed_mapdata_def) + apply (rule conjI) + apply (rule exI)+ + apply (rule conjI, erule vspace_for_asid_vs_lookup, simp) + apply (rule conjI) + apply (clarsimp simp: valid_cap_def wellformed_mapdata_def) apply clarsimp - apply (drule bspec [where x = "excaps ! 0"]) - apply simp - apply (clarsimp simp: valid_cap_def wellformed_mapdata_def split: option.split) - apply (fastforce simp: invs_def valid_state_def valid_pspace_def mask_def) - apply (clarsimp split: option.split) + apply (drule (1) pt_lookup_slot_vs_lookup_slotI, clarsimp) + apply (erule vs_lookup_slot_pte_at; assumption?) + apply (simp add: valid_cap_def wellformed_mapdata_def) apply fastforce \ \PageUnmap\ apply (simp split del: if_split) - apply (cases "invocation_type l = ArchInvocationLabel RISCV64PageUnmap") + apply (cases "invocation_type l = ArchInvocationLabel RISCVPageUnmap") apply simp apply (rule corres_returnOk) apply (clarsimp simp: archinv_relation_def page_invocation_map_def) \ \PageGetAddress\ - apply (cases "invocation_type l = ArchInvocationLabel RISCV64PageGetAddress") + apply (cases "invocation_type l = ArchInvocationLabel RISCVPageGetAddress") apply simp apply (rule corres_returnOk) apply (clarsimp simp: archinv_relation_def page_invocation_map_def) by (clarsimp split: invocation_label.splits arch_invocation_label.splits split del: if_split) -*) lemma VMReadWrite_vmrights_map[simp]: "vmrights_map vm_read_write = VMReadWrite" by (simp add: vmrights_map_def vm_read_write_def) -lemma below_user_vtop_in_user_region: - "p < user_vtop \ p \ user_region" - apply (simp add: user_region_def canonical_user_def user_vtop_def pptrUserTop_def RISCV64.pptrUserTop_def) - apply (simp add: bit_simps is_aligned_mask canonical_bit_def) - by (word_bitwise, clarsimp simp: word_size) - lemma gets_vspace_for_asid_is_catch: "gets (vspace_for_asid a) = ((liftME Some (find_vspace_for_asid a)) const (return None))" apply (simp add: find_vspace_for_asid_def liftME_def liftE_bindE catch_def) @@ -678,20 +706,6 @@ crunches isFinalCapability for no_0_obj'[wp]: no_0_obj' (simp: crunch_simps wp: crunch_wps) -(* FIXME RISCV: move to Corres, replace option_corres *) -lemma option_corres: - assumes None: "\ x = None; x' = None \ \ corres_underlying sr nf nf' r P P' (A None) (C None)" - assumes Some: "\z z'. \ x = Some z; x' = Some z' \ \ - corres_underlying sr nf nf' r (Q z) (Q' z') (A (Some z)) (C (Some z'))" - assumes None_eq: "(x = None) = (x' = None)" - shows "corres_underlying sr nf nf' r (\s. (x = None \ P s) \ (\z. x = Some z \ Q z s)) - (\s. (x' = None \ P' s) \ (\z. x' = Some z \ Q' z s)) - (A x) (C x')" - apply (cases x; cases x'; simp add: assms) - apply (simp add: None flip: None_eq) - apply (simp flip: None_eq) - done - lemma decode_page_table_inv_corres: "\cap = arch_cap.PageTableCap p opt; acap_relation cap cap'; list_all2 cap_relation (map fst excaps) (map fst excaps'); @@ -1298,15 +1312,6 @@ lemma diminished_arch_update': by (clarsimp simp: is_arch_update'_def isCap_simps diminished'_def) -lemma vmsz_aligned_user_region: - "\ vmsz_aligned p sz; p + (2 ^ pageBitsForSize sz - 1) < RISCV64_H.pptrUserTop \ - \ p \ user_region" - using pbfs_atleast_pageBits[of sz] - apply (simp flip: mask_2pm1 add: vmsz_aligned_def) - apply (simp add: user_region_def canonical_user_def pptrUserTop_def RISCV64.pptrUserTop_def) - apply (simp add: bit_simps is_aligned_mask canonical_bit_def word_plus_and_or_coroll) - by (word_bitwise, clarsimp simp: word_size) - lemma decode_page_inv_wf[wp]: "cap = (arch_capability.FrameCap word vmrights vmpage_size d option) \ \invs' and valid_cap' (capability.ArchObjectCap cap ) and