From 2048660d39ab412b0da46794a06b31457b2e340d Mon Sep 17 00:00:00 2001 From: Ryan Barry Date: Thu, 12 Dec 2024 13:06:24 +1100 Subject: [PATCH] aarch64 aspec+ainvs+access: access control modulo sorries Signed-off-by: Ryan Barry --- proof/access-control/AARCH64/ArchADT_AC.thy | 67 +- proof/access-control/AARCH64/ArchAccess.thy | 135 +- .../access-control/AARCH64/ArchAccess_AC.thy | 94 +- proof/access-control/AARCH64/ArchArch_AC.thy | 1674 +++++++++++------ proof/access-control/AARCH64/ArchCNode_AC.thy | 45 +- .../AARCH64/ArchDomainSepInv.thy | 87 +- .../AARCH64/ArchFinalise_AC.thy | 373 ++-- .../AARCH64/ArchInterrupt_AC.thy | 13 +- proof/access-control/AARCH64/ArchIpc_AC.thy | 11 +- .../access-control/AARCH64/ArchRetype_AC.thy | 22 +- .../access-control/AARCH64/ArchSyscall_AC.thy | 250 ++- proof/access-control/AARCH64/ArchTcb_AC.thy | 6 +- .../AARCH64/ArchSchedule_AI.thy | 7 +- .../AARCH64/ArchVCPU_AI.thy | 6 +- .../AARCH64/ArchVSpace_AI.thy | 3 +- spec/abstract/AARCH64/VCPUAcc_A.thy | 12 +- 16 files changed, 1923 insertions(+), 882 deletions(-) diff --git a/proof/access-control/AARCH64/ArchADT_AC.thy b/proof/access-control/AARCH64/ArchADT_AC.thy index d49d34b5b4..ca23b3c3e4 100644 --- a/proof/access-control/AARCH64/ArchADT_AC.thy +++ b/proof/access-control/AARCH64/ArchADT_AC.thy @@ -8,40 +8,37 @@ theory ArchADT_AC imports ADT_AC begin -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 named_theorems ADT_AC_assms -lemma mask_ptTranslationBits_ucast_ucast: - "(asid && mask ptTranslationBits) = ucast (ucast asid :: 9 word)" - by (word_eqI_solve simp: ptTranslationBits_def) - lemma ptr_offset_in_ptr_range: - "\ invs s; x \ kernel_mappings; - get_vspace_of_thread (kheap s) (arch_state s) tcb \ global_pt s; + "\ invs s; get_vspace_of_thread (kheap s) (arch_state s) tcb \ global_pt s; get_page_info (aobjs_of s) - (get_vspace_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r) \ + (get_vspace_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r) \ \ ptrFromPAddr base + (x && mask sz) \ ptr_range (ptrFromPAddr base) sz" apply (simp add: ptr_range_def mask_def) apply (rule conjI) apply (rule_tac b="2 ^ sz - 1" in word_plus_mono_right2) apply (frule some_get_page_info_umapsD) - apply (fastforce dest: get_vspace_of_thread_reachable - simp: canonical_not_kernel_is_user get_page_info_def)+ + apply (fastforce dest: get_vspace_of_thread_reachable + simp: get_page_info_def)+ apply clarsimp apply (drule is_aligned_ptrFromPAddr_n) - apply (simp add: pageBitsForSize_def pageBits_def canonical_bit_def ptTranslationBits_def + apply (simp add: pageBitsForSize_def pageBits_def canonical_bit_def + ptTranslationBits_def pptrBaseOffset_alignment_def split: vmpage_size.splits) apply (clarsimp simp: is_aligned_no_overflow' word_and_le1)+ apply (subst p_assoc_help) apply (rule word_plus_mono_right) apply (rule word_and_le1) apply (frule some_get_page_info_umapsD) - apply (fastforce dest: get_vspace_of_thread_reachable - simp: canonical_not_kernel_is_user get_page_info_def)+ + apply (fastforce dest: get_vspace_of_thread_reachable + simp: get_page_info_def)+ apply clarsimp apply (drule is_aligned_ptrFromPAddr_n) - apply (simp add: pageBitsForSize_def pageBits_def canonical_bit_def ptTranslationBits_def + apply (simp add: pageBitsForSize_def pageBits_def canonical_bit_def + ptTranslationBits_def pptrBaseOffset_alignment_def split: vmpage_size.splits) apply (clarsimp simp: is_aligned_no_overflow') done @@ -50,24 +47,19 @@ lemma user_op_access[ADT_AC_assms]: "\ invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \ vspace_cap_rights_to_auth (ptable_rights tcb s x) \ \ abs_has_auth_to aag auth tcb (ptrFromPAddr ptr)" - apply (case_tac "x \ kernel_mappings") - using get_vspace_of_thread_asid_or_global_pt - apply (fastforce simp: ptable_rights_def vspace_cap_rights_to_auth_def invs_def - valid_state_def valid_arch_state_def kernel_mappings_canonical - dest: some_get_page_info_kmapsD split: option.splits) apply (clarsimp simp: ptable_lift_def split: option.splits) apply (insert get_vspace_of_thread_asid_or_global_pt) apply (erule_tac x=s in meta_allE) apply (erule_tac x=tcb in meta_allE) apply (cases "get_vspace_of_thread (kheap s) (arch_state s) tcb = global_pt s"; clarsimp) - apply (frule get_page_info_gpd_kmaps[rotated 2]; fastforce simp: get_page_info_def) - apply (frule (3) ptr_offset_in_ptr_range) + apply (frule get_page_info_gpd_kmaps[rotated 3]; fastforce simp: get_page_info_def) + apply (frule (2) ptr_offset_in_ptr_range) apply (frule get_vspace_of_thread_reachable; clarsimp) apply (frule vs_lookup_table_vspace) apply fastforce+ + apply (clarsimp simp: vspace_for_asid_def entry_for_asid_def pool_for_asid_def entry_for_pool_def) apply (clarsimp simp: get_vspace_of_thread_def get_page_info_def ptable_rights_def pt_lookup_slot_def - split: if_splits option.splits kernel_object.splits cap.splits arch_cap.splits) - apply (frule (1) canonical_not_kernel_is_user) + split: if_splits option.splits kernel_object.splits cap.splits arch_cap.splits pt_type.splits) apply (frule pt_lookup_slot_from_level_is_subject) apply (fastforce elim: vs_lookup_table_vref_independent)+ apply (rule aag_Control_into_owns) @@ -86,24 +78,21 @@ lemma user_op_access[ADT_AC_assms]: apply (drule (1) vs_lookup_table_extend, rule order_refl) apply (rename_tac level vref) apply (case_tac "level = asid_pool_level", simp add: pt_walk_top) - apply (frule vs_lookup_table_is_aligned; clarsimp simp: canonical_not_kernel_is_user) + apply (frule vs_lookup_table_is_aligned; clarsimp) apply (clarsimp simp: pas_refined_def pte_info_def split: pte.splits) apply (erule subsetD) - apply (clarsimp simp: auth_graph_map_def state_objs_to_policy_def) - apply (intro exI conjI sbta_vref | erule sym | rule refl)+ - apply (clarsimp simp: state_vrefs_def ptes_of_Some pts_of_Some) - apply (intro exI conjI) - apply (simp add: canonical_not_kernel_is_user)+ - apply (clarsimp simp: vs_refs_aux_def) - apply (rule conjI; clarsimp) - apply (clarsimp simp: graph_of_def pte_ref2_def Bex_def ptes_of_Some pts_of_Some aobjs_of_Some) - apply (rule_tac x="table_index (pt_slot_offset max_pt_level vref x)" in exI) - apply (fastforce simp: table_index_max_level_slots canonical_not_kernel_is_user - image_iff ptrFromPAddr_def mult_is_add.mult_ac) - apply (clarsimp simp: graph_of_def pte_ref2_def ptes_of_Some pts_of_Some aobjs_of_Some) - apply (rule_tac x="table_index (pt_slot_offset level vref x)" in exI) - apply (fastforce simp: image_iff table_index_offset_pt_bits_left - ptrFromPAddr_def mult_is_add.mult_ac) + apply (clarsimp simp: auth_graph_map_def state_objs_to_policy_def vspace_for_asid_def) + apply (drule_tac s="pasObjectAbs aag vref" in sym) + apply (clarsimp simp: ptes_of_Some pts_of_Some) + apply (clarsimp simp: pt_apply_def split: pt.splits) + apply (intro exI conjI sbta_vref | simp add: state_vrefs_def vspace_objs_of_Some)+ + apply (clarsimp simp: vs_refs_aux_def graph_of_def pte_ref2_def) + apply (rule_tac x="UCAST(64 \ vs_index_len) (pt_index max_pt_level x)" in exI) + apply (fastforce simp: image_iff ptrFromPAddr_def mult_is_add.mult_ac split: pte.splits) + apply (intro exI conjI sbta_vref | simp add: state_vrefs_def vspace_objs_of_Some)+ + apply (clarsimp simp: vs_refs_aux_def graph_of_def pte_ref2_def) + apply (rule_tac x="UCAST(64 \ 9) (pt_index level x)" in exI) + apply (fastforce simp: image_iff ptrFromPAddr_def mult_is_add.mult_ac split: pte.splits) done lemma write_in_vspace_cap_rights[ADT_AC_assms]: diff --git a/proof/access-control/AARCH64/ArchAccess.thy b/proof/access-control/AARCH64/ArchAccess.thy index 8c48f69eb3..0aff83ea09 100644 --- a/proof/access-control/AARCH64/ArchAccess.thy +++ b/proof/access-control/AARCH64/ArchAccess.thy @@ -8,7 +8,7 @@ theory ArchAccess imports Types begin -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 subsection \Arch-specific transformation of caps into authorities\ @@ -25,37 +25,39 @@ subsection \Generating a policy from the current ASID distribution\ definition pte_ref2 where "pte_ref2 level pte \ case pte of - PagePTE ppn atts rights - \ Some (ptrFromPAddr (addr_from_ppn ppn), - pageBitsForSize (vmpage_size_of_level level), + PagePTE paddr _ _ rights + \ Some (ptrFromPAddr paddr, + pt_bits_left level, vspace_cap_rights_to_auth rights) - | PageTablePTE ppn atts - \ Some (ptrFromPAddr (addr_from_ppn ppn), 0, {Control}) + | PageTablePTE ppn + \ Some (ptrFromPAddr (paddr_from_ppn ppn), 0, {Control}) | _ \ None" definition vs_refs_aux :: "vm_level \ arch_kernel_obj \ (obj_ref \ obj_ref \ aa_type \ auth) set" where "vs_refs_aux level \ \ko. case ko of - ASIDPool pool \ (\(r,p). (p, ucast r, AASIDPool, Control)) ` graph_of pool - | PageTable pt \ - \(r,(p, sz, auth)) \ graph_of (pte_ref2 level o pt) - {(x,y). x \ kernel_mapping_slots \ level = max_pt_level}. - (\(p, a). (p, ucast r, APageTable, a)) ` (ptr_range p sz \ auth) + ASIDPool pool \ (\(r,p). (p, ucast r, AASIDPool, Control)) ` graph_of (option_map ap_vspace o pool) + | PageTable pt \ (case pt of + VSRootPT pt \ \(r,(p, sz, auth)) \ graph_of (pte_ref2 level o pt). + (\(p, a). (p, ucast r, APageTable VSRootPT_T, a)) ` (ptr_range p sz \ auth) + | NormalPT pt \ \(r,(p, sz, auth)) \ graph_of (pte_ref2 level o pt). + (\(p, a). (p, ucast r, APageTable NormalPT_T, a)) ` (ptr_range p sz \ auth)) | _ \ {}" definition state_vrefs where "state_vrefs s \ \p. \{vs_refs_aux lvl ao | lvl ao bot asid vref. vs_lookup_table bot asid vref s = Some (lvl, p) - \ aobjs_of s p = Some ao \ vref \ user_region}" + \ vspace_objs_of s p = Some ao \ vref \ user_region}" lemma state_vrefsD: "\ vs_lookup_table level asid vref s = Some (lvl, p); - aobjs_of s p = Some ao; vref \ user_region; x \ vs_refs_aux lvl ao \ + vspace_objs_of s p = Some ao; vref \ user_region; x \ vs_refs_aux lvl ao \ \ x \ state_vrefs s p" unfolding state_vrefs_def by fastforce end -context Arch_p_arch_update_eq begin global_naming RISCV64 +context Arch_p_arch_update_eq begin global_naming AARCH64 interpretation Arch . @@ -64,7 +66,7 @@ lemma state_vrefs[iff]: "state_vrefs (f s) = state_vrefs s" end -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 lemmas state_vrefs_upd = cur_thread_update.state_vrefs @@ -80,17 +82,18 @@ end context Arch begin primrec aobj_ref' where - "aobj_ref' (ASIDPoolCap p as) = {p}" + "aobj_ref' (ASIDPoolCap ref _) = {ref}" | "aobj_ref' ASIDControlCap = {}" -| "aobj_ref' (FrameCap ref cR sz dev as) = ptr_range ref (pageBitsForSize sz)" -| "aobj_ref' (PageTableCap x as3) = {x}" +| "aobj_ref' (FrameCap ref _ sz _ _) = ptr_range ref (pageBitsForSize sz)" +| "aobj_ref' (PageTableCap ref _ _) = {ref}" +| "aobj_ref' (VCPUCap ref) = {ref}" fun acap_asid' :: "arch_cap \ asid set" where "acap_asid' (FrameCap _ _ _ _ mapping) = fst ` set_option mapping" -| "acap_asid' (PageTableCap _ mapping) = fst ` set_option mapping" -| "acap_asid' (ASIDPoolCap _ asid) - = {x. asid_high_bits_of x = asid_high_bits_of asid \ x \ 0}" +| "acap_asid' (PageTableCap _ _ mapping) = fst ` set_option mapping" +| "acap_asid' (ASIDPoolCap _ asid) = {x. asid_high_bits_of x = asid_high_bits_of asid \ x \ 0}" | "acap_asid' ASIDControlCap = UNIV" +| "acap_asid' (VCPUCap _) = {}" inductive_set state_asids_to_policy_aux for aag caps asid_tab vrefs where sata_asid: @@ -109,7 +112,7 @@ inductive_set state_asids_to_policy_aux for aag caps asid_tab vrefs where definition "state_asids_to_policy_arch aag caps astate vrefs \ - state_asids_to_policy_aux aag caps (riscv_asid_table astate) + state_asids_to_policy_aux aag caps (arm_asid_table astate) (vrefs :: 64 word \ (64 word \ 64 word \ aa_type \ auth) set)" declare state_asids_to_policy_arch_def[simp] @@ -201,21 +204,21 @@ lemma integrity_asids_kh_update: subsection \Misc definitions\ fun ctxt_IP_update where - "ctxt_IP_update (UserContext ctxt) = UserContext (ctxt(NextIP := ctxt FaultIP))" + "ctxt_IP_update (UserContext fpu ctxt) = UserContext fpu (ctxt(NextIP := ctxt FaultIP))" lemma ctxt_IP_update_def: "ctxt_IP_update ctxt = - (case ctxt of (UserContext ctxt') \ UserContext (ctxt'(NextIP := ctxt' FaultIP)))" + (case ctxt of (UserContext fpu ctxt') \ UserContext fpu (ctxt'(NextIP := ctxt' FaultIP)))" by (cases ctxt; clarsimp) abbreviation arch_IP_update where "arch_IP_update arch \ arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get arch)) arch" definition asid_pool_integrity :: - "'a set \ 'a PAS \ (asid_low_index \ obj_ref) \ (asid_low_index \ obj_ref) \ bool" where + "'a set \ 'a PAS \ (asid_low_index \ asid_pool_entry) \ (asid_low_index \ asid_pool_entry) \ bool" where "asid_pool_integrity subjects aag pool pool' \ \x. pool' x \ pool x - \ pool' x = None \ aag_subjects_have_auth_to subjects aag Control (the (pool x))" + \ pool' x = None \ aag_subjects_have_auth_to subjects aag Control (ap_vspace (the (pool x)))" inductive arch_integrity_obj_atomic :: "'a PAS \ 'a set \ 'a \ arch_kernel_obj \ arch_kernel_obj \ bool" @@ -275,4 +278,86 @@ end declare state_vrefs_upd[simp] declare integrity_asids_updates[simp] + +context Arch begin global_naming AARCH64 + +(* FIXME AARCH64: update the access control spec + -Parameterise arch object updates with machine state and arch state + -Model virtualised machine state more explicitly + -Specify when virtualised machine state can change (i.e. restoring from current VCPU) + -Specify when arm_current_vcpu can change (i.e. once current VCPU has been saved) + -Specify integrity constraints for FPUs +*) + +\ \Anyone can save virtualised registers to the current VCPU\ +lemma arch_troa_vcpu_save_reg: + "\ aobjs_of s vptr = Some (VCPU vcpu); ao' = VCPU vcpu'; + option_map fst (arm_current_vcpu (arch_state s)) = Some vptr; + vcpu' = vcpu\vcpu_regs := (vcpu_regs vcpu)(reg := vcpuHardwareReg_val reg (machine_state s))\ \ + \ arch_integrity_obj_atomic aag subjects l ao ao'" + sorry + +(* FIXME AARCH64: assert a connection to the current (or soon-to-be-switched-to) thread? *) +\ \Anyone can update the virtual count offset in the current VCPU\ +lemma arch_troa_vcpu_restore_vtimer: + "\ aobjs_of s vptr = Some (VCPU vcpu); ao' = VCPU vcpu'; + option_map fst (arm_current_vcpu (arch_state s)) = Some vptr; + vcpu' = vcpu\vcpu_regs := (vcpu_regs vcpu) + (VCPURegCNTVOFF := vcpu_regs vcpu VCPURegCNTVOFF + + (read_cntpct_val (machine_state s) + - vtimerLastPCount (vcpu_vtimer vcpu)))\ \ + \ arch_integrity_obj_atomic aag subjects l ao ao'" + sorry + +\ \Anyone can save the physical count register to the current VCPU\ +lemma arch_troa_vcpu_save_virt_timer: + "\ aobjs_of s vptr = Some (VCPU vcpu); ao' = VCPU vcpu'; + option_map fst (arm_current_vcpu (arch_state s)) = Some vptr; + vcpu' = vcpu\vcpu_vtimer := VirtTimer (read_cntpct_val (machine_state s))\ \ + \ arch_integrity_obj_atomic aag subjects l ao ao'" + sorry + +\ \Anyone can save virtualised GIC registers to the current VCPU\ +lemma arch_troa_vcpu_save_vgic: + "\ aobjs_of s vptr = Some (VCPU vcpu); ao' = VCPU vcpu'; + option_map fst (arm_current_vcpu (arch_state s)) = Some vptr; + vcpu' = vcpu \vcpu_vgic := vgic\; + vgic = vcpu_vgic vcpu\vgic_hcr := gic_vcpu_ctrl_hcr_val (machine_state s)\ \ + vgic = vcpu_vgic vcpu\vgic_vmcr := gic_vcpu_ctrl_vmcr_val (machine_state s)\ \ + vgic = vcpu_vgic vcpu\vgic_apr := gic_vcpu_ctrl_apr_val (machine_state s)\ \ + vgic = vcpu_vgic vcpu\vgic_lr := (vgic_lr (vcpu_vgic vcpu)) + (vreg := gic_vcpu_ctrl_lr_val (of_nat vreg) (machine_state s))\ \ + \ arch_integrity_obj_atomic aag subjects l ao ao'" + sorry + +\ \Update the vmid of a pool\ +lemma + arch_troa_asidpool_vmid: + "\ ao = ASIDPool pool; ao' = ASIDPool pool'; + \x. (pool x = None) = (pool' x = None); + \x e e'. pool x = Some e \ pool' x = Some e' + \ (ap_vspace e = ap_vspace e' \ + (ap_vmid e = ap_vmid e' \ ap_vmid e = None \ ap_vmid e' = None)) \ + \ arch_integrity_obj_atomic aag subjects l ao ao'" + sorry + +\ \If a VCPU belongs to the current agent, then so does its associated TCB\ +lemma associated_tcb_is_subject: + "\ vcpus_of s v = Some vcpu; vcpu_tcb vcpu = Some t; is_subject aag v \ + \ is_subject aag t" + sorry + +\ \If a TCB belongs to the current agent, then so does its associated VCPU\ +lemma associated_vcpu_is_subject: + "\ get_tcb t s = Some tcb; tcb_vcpu (tcb_arch tcb) = Some v; is_subject aag t \ + \ is_subject aag v" + sorry + +(* FIXME AARCH64: clarify when we can assume this *) +lemma invs_valid_cur_vcpu: + "invs s \ valid_cur_vcpu s" + sorry + +end + end diff --git a/proof/access-control/AARCH64/ArchAccess_AC.thy b/proof/access-control/AARCH64/ArchAccess_AC.thy index 0d5405dbed..4e3376a928 100644 --- a/proof/access-control/AARCH64/ArchAccess_AC.thy +++ b/proof/access-control/AARCH64/ArchAccess_AC.thy @@ -10,7 +10,7 @@ begin section\Arch-specific AC proofs\ -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 named_theorems Access_AC_assms @@ -59,7 +59,7 @@ proof goal_cases qed -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 lemma auth_ipc_buffers_tro[Access_AC_assms]: "\ integrity_obj_state aag activate subjects s s'; @@ -96,7 +96,7 @@ proof goal_cases qed -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 lemma ipcframe_subset_page: "\ valid_objs s; get_tcb p s = Some tcb; @@ -163,13 +163,99 @@ proof goal_cases qed -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 lemma pas_refined_irq_state_independent[intro!, simp]: "pas_refined x (s\machine_state := machine_state s\irq_state := f (irq_state (machine_state s))\\) = pas_refined x s" by (simp add: pas_refined_def) +(* FIXME AARCH64: try to use in_opt_map_eq where possible *) +lemma vspace_objs_of_Some: + "(vspace_objs_of s p = Some ao) = (aobjs_of s p = Some ao \ \is_VCPU ao)" + by (clarsimp simp: in_opt_map_eq vspace_obj_of_Some) + +lemma state_irqs_to_policy_eq_caps: + "\ x \ state_irqs_to_policy_aux aag caps; caps = caps' \ + \ x \ state_irqs_to_policy_aux aag caps'" + by (erule subst) + +lemma vs_lookup_table_eqI': + "\ asid_table s' (asid_high_bits_of asid) = asid_table s (asid_high_bits_of asid); + \pool_ptr. asid_table s' (asid_high_bits_of asid) = Some pool_ptr + \ bot_level \ max_pt_level + \ vspace_for_pool pool_ptr asid (asid_pools_of s') = + vspace_for_pool pool_ptr asid (asid_pools_of s); + bot_level < max_pt_level \ pts_of s' = pts_of s \ + \ vs_lookup_table bot_level asid vref s' = vs_lookup_table bot_level asid vref s" + by (auto simp: obind_def vs_lookup_table_def asid_pool_level_eq[symmetric] + pool_for_asid_def entry_for_pool_def vspace_for_pool_def + split: option.splits) + +lemma vs_refs_aux_eqI: + assumes "pts_of s' = pts_of s" + and "\p sz. data_at sz p s' = data_at sz p s" + and "\pool_ptr asid. (asid_pools_of s' |> oapply asid |> ogets ap_vspace) pool_ptr + = (asid_pools_of s |> oapply asid |> ogets ap_vspace) pool_ptr" + and "aobjs_of s p = Some ao" + and "aobjs_of s' p = Some ao'" + shows "vs_refs_aux level ao = vs_refs_aux level ao'" + apply (insert assms) + apply (clarsimp simp: fun_eq_iff) + apply (erule_tac x=p in allE)+ + apply (fastforce simp: vs_refs_aux_def graph_of_def image_iff opt_map_def ogets_def + split: option.splits arch_kernel_obj.splits) + done + +lemma state_vrefs_eqI': + assumes "asid_table s' = asid_table s" + and "pts_of s' = pts_of s" + and "\p sz. data_at sz p s' = data_at sz p s" + and "\pool_ptr asid. (asid_pools_of s' |> oapply asid |> ogets ap_vspace) pool_ptr + = (asid_pools_of s |> oapply asid |> ogets ap_vspace) pool_ptr" + shows "state_vrefs s' = state_vrefs s" + apply (insert assms) + apply (prop_tac "\level asid vref. vs_lookup_table level asid vref s' = vs_lookup_table level asid vref s") + apply (rule vs_lookup_table_eqI') + apply (auto simp: fun_eq_iff vspace_for_pool_def entry_for_pool_def obind_def ogets_def opt_map_def)[3] + apply (rule ext)+ + apply (intro equalityI subsetI; subst (asm) state_vrefs_def; clarsimp) + + apply (clarsimp simp: vspace_objs_of_Some) + apply (case_tac "vspace_objs_of s x"; clarsimp?) + apply (clarsimp simp: fun_eq_iff) + apply (erule_tac x=x in allE)+ + apply (fastforce simp: vspace_obj_of_def vs_refs_aux_def graph_of_def + image_iff opt_map_def ogets_def is_VCPU_def + split: option.splits arch_kernel_obj.splits if_splits )[1] + apply (prop_tac "\level. vs_refs_aux level ao = vs_refs_aux level ac") + apply (intro allI vs_refs_aux_eqI; fastforce simp: vspace_objs_of_Some) + apply (fastforce intro: state_vrefsD) + + apply (clarsimp simp: vspace_objs_of_Some) + apply (case_tac "vspace_objs_of s' x"; clarsimp?) + apply (clarsimp simp: fun_eq_iff) + apply (erule_tac x=x in allE)+ + apply (fastforce simp: vspace_obj_of_def vs_refs_aux_def graph_of_def + image_iff opt_map_def ogets_def is_VCPU_def + split: option.splits arch_kernel_obj.splits if_splits )[1] + apply (prop_tac "\level. vs_refs_aux level ac = vs_refs_aux level ao") + apply (intro allI vs_refs_aux_eqI; fastforce simp: vspace_objs_of_Some) + apply (fastforce intro!: state_vrefsD) + done + +lemma state_vrefs_eqI: + assumes "asid_table s' = asid_table s" + and "vspace_objs_of s' = vspace_objs_of s" + shows "state_vrefs s' = state_vrefs s" + apply (prop_tac "\level asid vref. vs_lookup_table level asid vref s = vs_lookup_table level asid vref s'") + apply (intro allI vs_lookup_table_eqI') + using assms apply (fastforce simp: obj_at_def) + using vspace_objs_of_aps_eq assms apply fastforce + using vspace_objs_of_pts_eq assms apply fastforce + using assms apply (fastforce simp: state_vrefs_def) + done + end end diff --git a/proof/access-control/AARCH64/ArchArch_AC.thy b/proof/access-control/AARCH64/ArchArch_AC.thy index 4519236a7b..f2954fd9dc 100644 --- a/proof/access-control/AARCH64/ArchArch_AC.thy +++ b/proof/access-control/AARCH64/ArchArch_AC.thy @@ -14,25 +14,20 @@ Arch-specific access control. \ -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 named_theorems Arch_AC_assms lemma set_mrs_state_vrefs[Arch_AC_assms, wp]: - "\pspace_aligned and valid_vspace_objs and valid_arch_state and (\s. P (state_vrefs s))\ + "\(\s. P (state_vrefs s))\ set_mrs thread buf msgs \\_ s. P (state_vrefs s)\" apply (simp add: set_mrs_def split_def set_object_def get_object_def split del: if_split) apply (wpsimp wp: gets_the_wp get_wp put_wp mapM_x_wp' simp: zipWithM_x_mapM_x split_def store_word_offs_def split_del: if_split) - apply (subst state_vrefs_eqI) - prefer 7 - apply assumption - apply (clarsimp simp: opt_map_def) - apply (fastforce simp: opt_map_def aobj_of_def) - apply clarsimp - apply (auto simp: valid_arch_state_def) + apply (subst (asm) state_vrefs_tcb_upd[symmetric]) + apply (auto simp: fun_upd_def get_tcb_def tcb_at_def) done lemma mul_add_word_size_lt_msg_align_bits_ofnat[Arch_AC_assms]: @@ -59,7 +54,7 @@ proof goal_cases qed -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 definition level_of_table :: "obj_ref \ 'z :: state_ext state \ vm_level" where @@ -68,7 +63,7 @@ definition level_of_table :: "obj_ref \ 'z :: state_ext state \ vs_lookup_table level asid vref s = Some (level, p); - ptes_of s p = Some pte; level \ max_pt_level; vref \ user_region; invs s \ + ptes_of s pt_t p = Some pte; level \ max_pt_level; vref \ user_region; invs s \ \ level_of_table p s = level" apply (subst level_of_table_def) apply (rule Greatest_equality, fastforce) @@ -79,7 +74,7 @@ lemma level_of_table_vs_lookup_table: lemma vs_lookup_slot_level_of_slot: "\ vs_lookup_slot level asid vref s = Some (level, p); - ptes_of s p = Some pte; level \ max_pt_level; vref \ user_region; invs s \ + ptes_of s pt_t p = Some pte; level \ max_pt_level; vref \ user_region; invs s \ \ level_of_slot asid vref p s = level" apply (subst level_of_slot_def) apply (rule Greatest_equality) @@ -101,18 +96,15 @@ lemma vs_lookup_table_vref_independent: lemma state_vrefs_store_NonPageTablePTE: "\ invs s; is_aligned p pte_bits; vs_lookup_slot level asid vref s = Some (level, p); - vref \ user_region; \ is_PageTablePTE pte; - kheap s (table_base p) = Some (ArchObj (PageTable pt)) \ - \ state_vrefs (s\kheap := \a. if a = table_base p - then Some (ArchObj (PageTable (\a. if a = table_index p - then pte - else pt a))) - else kheap s a\) = + vref \ user_region; \ is_PageTablePTE pte; pts_of s (table_base (pt_type pt) p) = Some pt \ + \ state_vrefs (s\kheap := (kheap s)(table_base (pt_type pt) p \ + ArchObj (PageTable (pt_upd pt (table_index (pt_type pt) p) pte)) + )\) = (\x. if \level' vref'. vref_for_level vref' (level + 1) = vref_for_level vref (level + 1) \ - vref' \ user_region \ p = pt_slot_offset level (table_base p) vref' \ - pt_walk level level' (table_base p) vref' (ptes_of s) = Some (level',x) - then (if x = table_base p - then vs_refs_aux level (PageTable (\a. if a = table_index p then pte else pt a)) + vref' \ user_region \ p = pt_slot_offset level (table_base (pt_type pt) p) vref' \ + pt_walk level level' (table_base (pt_type pt) p) vref' (ptes_of s) = Some (level',x) + then (if x = table_base (pt_type pt) p + then vs_refs_aux level (PageTable (pt_upd pt (table_index (pt_type pt) p) pte)) else {}) else state_vrefs s x)" apply (rule all_ext) @@ -120,20 +112,26 @@ lemma state_vrefs_store_NonPageTablePTE: apply (fastforce simp: vs_lookup_slot_def vs_lookup_table_def ptes_of_Some pts_of_Some aobjs_of_Some dest: pool_for_asid_no_pte) - apply (prop_tac "ptes_of s p \ None") - apply (drule valid_vspace_objs_strong_slotD; clarsimp split del: if_split) + apply (frule vs_lookup_slot_level_type) + apply (fastforce simp: ptes_of_Some pts_of_Some aobjs_of_Some)+ + apply (prop_tac "ptes_of s (pt_type pt) p \ None") + apply (drule valid_vspace_objs_strong_slotD; clarsimp simp: ptes_of_Some pts_of_Some aobjs_of_Some) apply (frule vs_lookup_slot_table_base; clarsimp split del: if_split) + apply (subst (asm) ptes_of_Some) apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp split del: if_split) apply safe - apply (subst (asm) state_vrefs_def opt_map_def)+ + apply (subst (asm) state_vrefs_def)+ apply (clarsimp split: option.splits split del: if_split) apply (subst (asm) vs_lookup_non_PageTablePTE[where s=s and s'="kheap_update _ s" and p=p]) - apply (fastforce simp: ptes_of_Some pts_of_Some aobjs_of_Some - opt_map_def pte_of_def obind_def - dest: pte_ptr_eq)+ - apply (case_tac "x = table_base p"; clarsimp) + apply ((fastforce simp: ptes_of_pts_of_upd ptes_of_Some pts_of_Some aobjs_of_Some + intro: ptes_of_pts_of_upd + dest: pte_ptr_eq split: if_splits + | clarsimp simp: opt_map_def fun_upd_def split: option.splits)+; fail)+ + + apply (frule pts_of_ptes_of; clarsimp) + apply (case_tac "x = table_base (pt_type pt) p"; clarsimp) apply (case_tac "lvl = asid_pool_level") - apply (fastforce dest: vs_lookup_table_no_asid[OF vs_lookup_level] + apply (fastforce dest: vs_lookup_table_no_asid[OF vs_lookup_level, where pt_t="pt_type pt"] simp: ptes_of_Some pts_of_Some aobjs_of_Some split: if_splits) apply (fastforce dest: vs_lookup_table_unique_level[OF vs_lookup_level] elim: allE[where x=level] split: if_splits) @@ -143,7 +141,10 @@ lemma state_vrefs_store_NonPageTablePTE: apply (frule vs_lookup_slot_level_of_slot) apply (fastforce simp: ptes_of_Some pts_of_Some aobjs_of_Some split: option.splits) apply fastforce+ - apply (subst (asm) vs_lookup_slot_table_unfold; fastforce) + apply (subst (asm) vs_lookup_slot_table_unfold) + apply fastforce+ + apply clarsimp + apply (metis (no_types, lifting) vs_lookup_slot_table_unfold vs_lookup_slot_unique_level) apply (rule conjI; clarsimp) apply (case_tac "level' < level") apply (subst (asm) vs_lookup_vref_for_level_eq1, rule sym, assumption) @@ -154,7 +155,7 @@ lemma state_vrefs_store_NonPageTablePTE: apply (frule_tac level=lvl in vs_lookup_level) apply (drule (1) vs_lookup_table_unique_level, rule refl) apply fastforce+ - apply (frule bit0.plus_one_leq) + apply (frule bit1.plus_one_leq) apply (erule_tac x=level in allE) apply (subst (asm) vs_lookup_slot_vref_for_level[symmetric], assumption) apply (frule_tac bot_level=bot in vs_lookup_min_level) @@ -162,31 +163,36 @@ lemma state_vrefs_store_NonPageTablePTE: apply (subst (asm) pt_walk.simps, clarsimp) apply (fastforce simp: state_vrefs_def opt_map_def) apply (prop_tac "level_of_slot asid vref p s = level") - apply (fastforce simp: vs_lookup_slot_table_unfold vs_lookup_slot_level_of_slot) + apply (fastforce simp: vs_lookup_slot_table_unfold ptes_of_Some intro: vs_lookup_slot_level_of_slot) apply (clarsimp split: if_splits) apply (rule state_vrefsD) apply (subst vs_lookup_non_PageTablePTE[where s=s and p=p and pte=pte]) - apply (fastforce dest: pte_ptr_eq - simp: ptes_of_Some pts_of_Some aobjs_of_Some - opt_map_def pte_of_def obind_def)+ - apply (case_tac "x = table_base p") + apply ((fastforce simp: ptes_of_pts_of_upd ptes_of_Some pts_of_Some aobjs_of_Some + intro: ptes_of_pts_of_upd + dest: pte_ptr_eq split: if_splits + | clarsimp simp: opt_map_def fun_upd_def split: option.splits)+; fail)+ + apply (case_tac "x = table_base (pt_type pt) p") apply (fastforce elim: allE[where x=level]) apply (subst (asm) state_vrefs_def, clarsimp) apply (rule_tac level=lvl and asid=asida and vref=vrefa in state_vrefsD) apply (subst vs_lookup_non_PageTablePTE[where s=s and p=p and pte=pte]) - apply (fastforce dest: pte_ptr_eq - simp: ptes_of_Some pts_of_Some aobjs_of_Some - opt_map_def pte_of_def obind_def)+ + apply ((fastforce simp: ptes_of_pts_of_upd ptes_of_Some pts_of_Some aobjs_of_Some + intro: ptes_of_pts_of_upd + dest: pte_ptr_eq split: if_splits + | clarsimp simp: opt_map_def fun_upd_def split: option.splits)+; fail)+ apply (clarsimp split: if_splits) apply (intro conjI; clarsimp) apply (case_tac "level' = asid_pool_level") apply (fastforce dest: vs_lookup_slot_no_asid simp: ptes_of_Some pts_of_Some aobjs_of_Some) - apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp) apply (case_tac "lvl < level") apply (drule_tac bot_level=bot in vs_lookup_level) apply (subst (asm) vs_lookup_split_Some, erule dual_order.strict_implies_order) apply fastforce + apply (frule vs_lookup_slot_level_type) + apply (fastforce simp: ptes_of_Some pts_of_Some aobjs_of_Some)+ + apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp) apply (drule (1) vs_lookup_table_unique_level; fastforce) + apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp) apply (metis vs_lookup_slot_table vs_lookup_slot_unique_level) apply (fastforce dest: vs_lookup_level) apply (fastforce simp: aobjs_of_Some opt_map_def) @@ -194,100 +200,102 @@ lemma state_vrefs_store_NonPageTablePTE: apply clarsimp done + lemma state_vrefs_store_NonPageTablePTE': "\ invs s; is_aligned p pte_bits; \ is_PageTablePTE pte; - kheap s (table_base p) = Some (ArchObj (PageTable pt)); + pts_of s (table_base (pt_type pt) p) = Some pt; \level asid vref. vref \ user_region \ vs_lookup_slot level asid vref s \ Some (level, p) \ - \ state_vrefs (s\kheap := \a. if a = table_base p - then Some (ArchObj (PageTable (\a. if a = table_index p - then pte - else pt a))) - else kheap s a\) = - (\x. if x = table_base p \ (\level. \\ (level, table_base p) s) - then vs_refs_aux (level_of_table (table_base p) s) (PageTable (\a. if a = table_index p - then pte - else pt a)) + \ state_vrefs (s\kheap := (kheap s)(table_base (pt_type pt) p \ + ArchObj (PageTable (pt_upd pt (table_index (pt_type pt) p) pte)) + )\) = + (\x. if x = table_base (pt_type pt) p \ (\level. \\ (level, table_base (pt_type pt) p) s) + then vs_refs_aux (level_of_table (table_base (pt_type pt) p) s) + (PageTable (pt_upd pt (table_index (pt_type pt) p) pte)) else state_vrefs s x)" apply (rule all_ext) + apply safe - apply (subst (asm) state_vrefs_def opt_map_def)+ + apply (frule pts_of_ptes_of; clarsimp) + apply (subst (asm) state_vrefs_def)+ apply (clarsimp split: option.splits split del: if_split) apply (clarsimp split: if_split_asm option.splits split del: if_split) apply (subst (asm) vs_lookup_non_PageTablePTE[where s=s and p=p and pte=pte]) - apply (fastforce dest: pte_ptr_eq - simp: ptes_of_Some pts_of_Some aobjs_of_Some - opt_map_def pte_of_def obind_def)+ + apply ((fastforce simp: ptes_of_pts_of_upd ptes_of_Some pts_of_Some aobjs_of_Some + intro: ptes_of_pts_of_upd + dest: pte_ptr_eq split: if_splits + | clarsimp simp: opt_map_def fun_upd_def split: option.splits)+; fail)+ apply (clarsimp split: if_splits) apply (drule vs_lookup_level) apply (rule conjI; clarsimp) apply (case_tac "level = asid_pool_level") - apply (fastforce dest: vs_lookup_table_no_asid simp: ptes_of_Some pts_of_Some aobjs_of_Some) + apply (clarsimp simp: ptes_of_Some pts_of_Some) + apply (fastforce dest: vs_lookup_table_pt_at vs_lookup_asid_pool + simp: asid_pools_of_ko_at obj_at_def opt_map_def) apply (case_tac "lvl = asid_pool_level") - apply (fastforce dest: vs_lookup_table_no_asid simp: ptes_of_Some pts_of_Some aobjs_of_Some) - apply (subst level_of_table_vs_lookup_table; fastforce simp: ptes_of_Some pts_of_Some aobjs_of_Some) + apply (fastforce dest: vs_lookup_table_pt_at vs_lookup_asid_pool + simp: asid_pools_of_ko_at obj_at_def) + apply (subst level_of_table_vs_lookup_table[where pt_t="pt_type pt"]; fastforce) apply (subst (asm) vs_lookup_non_PageTablePTE[where s=s and p=p and pte=pte]) - apply (fastforce dest: pte_ptr_eq - simp: ptes_of_Some pts_of_Some aobjs_of_Some - opt_map_def pte_of_def obind_def)+ + apply ((fastforce simp: ptes_of_pts_of_upd ptes_of_Some pts_of_Some aobjs_of_Some + intro: ptes_of_pts_of_upd + dest: pte_ptr_eq split: if_splits + | clarsimp simp: opt_map_def fun_upd_def split: option.splits)+; fail)+ apply (fastforce simp: state_vrefs_def aobjs_of_Some) apply (clarsimp split: if_splits) apply (case_tac "level = asid_pool_level") - apply (fastforce dest: vs_lookup_table_no_asid simp: ptes_of_Some pts_of_Some aobjs_of_Some) - apply (subst (asm) level_of_table_vs_lookup_table) + apply (clarsimp simp: ptes_of_Some pts_of_Some) + apply (fastforce dest: vs_lookup_table_pt_at vs_lookup_asid_pool + simp: asid_pools_of_ko_at obj_at_def opt_map_def) + apply (subst (asm) level_of_table_vs_lookup_table[where pt_t="pt_type pt"]) apply (fastforce simp: ptes_of_Some pts_of_Some aobjs_of_Some)+ apply (rule state_vrefsD) apply (subst vs_lookup_non_PageTablePTE[where s=s and p=p and pte=pte ]) - apply ((fastforce dest: pte_ptr_eq - simp: ptes_of_Some pts_of_Some aobjs_of_Some - opt_map_def pte_of_def obind_def)+)[7] - apply auto[1] - apply (fastforce simp: aobjs_of_Some opt_map_def) - apply clarsimp - apply clarsimp - apply (case_tac "x = table_base p") + apply ((fastforce simp: ptes_of_pts_of_upd ptes_of_Some pts_of_Some aobjs_of_Some + intro: ptes_of_pts_of_upd + dest: pte_ptr_eq split: if_splits + | clarsimp simp: opt_map_def fun_upd_def split: option.splits)+; fail)+ + apply (case_tac "x = table_base (pt_type pt) p") apply (fastforce dest: vs_lookup_level simp: state_vrefs_def) apply (subst (asm) state_vrefs_def, clarsimp) apply (rule state_vrefsD) apply (subst vs_lookup_non_PageTablePTE[where s=s and p=p and pte=pte ]) - apply ((fastforce dest: pte_ptr_eq - simp: ptes_of_Some pts_of_Some aobjs_of_Some - opt_map_def pte_of_def obind_def)+)[7] - apply auto[1] - apply (fastforce simp: aobjs_of_Some opt_map_def split: option.splits) - apply clarsimp - apply clarsimp + apply ((fastforce simp: ptes_of_pts_of_upd ptes_of_Some pts_of_Some aobjs_of_Some + intro: ptes_of_pts_of_upd + dest: pte_ptr_eq split: if_splits + | clarsimp simp: opt_map_def fun_upd_def split: option.splits)+; fail)+ done (* FIXME AC: make this less ugly *) lemma state_vrefs_store_NonPageTablePTE_wp: "\\s. invs s \ \ is_PageTablePTE pte \ - (\pt. ako_at (PageTable pt) (table_base p) s \ is_aligned p pte_bits \ + (\pt. pts_of s (table_base pt_t p) = Some pt \ pt_t = pt_type pt \ is_aligned p pte_bits \ (if \level asid vref. vs_lookup_slot level asid vref s = Some (level, p) \ vref \ user_region then (\level asid vref. vs_lookup_slot level asid vref s = Some (level, p) \ vref \ user_region \ P (\x. (if \level' vref'. vref_for_level vref' (level + 1) = vref_for_level vref (level + 1) \ - vref' \ user_region \ p = pt_slot_offset level (table_base p) vref' \ - pt_walk level level' (table_base p) vref' (ptes_of s) = Some (level', x) - then (if x = table_base p - then vs_refs_aux level (PageTable (\a. if a = table_index p then pte else pt a)) + vref' \ user_region \ p = pt_slot_offset level (table_base pt_t p) vref' \ + pt_walk level level' (table_base pt_t p) vref' (ptes_of s) = Some (level', x) + then (if x = table_base pt_t p + then vs_refs_aux level (PageTable (pt_upd pt (table_index pt_t p) pte)) else {}) else state_vrefs s x))) - else P (\x. (if x = table_base p \ (\level. \\ (level, table_base p) s) - then vs_refs_aux (level_of_table (table_base p) s) (PageTable (\a. if a = table_index p then pte else pt a)) + else P (\x. (if x = table_base pt_t p \ (\level. \\ (level, table_base pt_t p) s) + then vs_refs_aux (level_of_table (table_base pt_t p) s) (PageTable (pt_upd pt (table_index pt_t p) pte)) else state_vrefs s x))))\ - store_pte p pte + store_pte pt_t p pte \\_ s. P (state_vrefs s)\" unfolding store_pte_def set_pt_def apply (wpsimp wp: set_object_wp) apply (case_tac "\level asid vref. vs_lookup_slot level asid vref s = Some (level, p) \ vref \ user_region") + apply clarsimp apply (erule_tac x=pt in allE) - apply (clarsimp simp: fun_upd_def) apply (subst state_vrefs_store_NonPageTablePTE) apply fastforce+ - apply (clarsimp simp: obj_at_def) + apply (clarsimp simp: obj_at_def pts_of_Some aobjs_of_Some) apply (case_tac "level = asid_pool_level") apply (fastforce dest: vs_lookup_slot_no_asid simp: ptes_of_Some pts_of_Some aobjs_of_Some obj_at_def) + apply (clarsimp simp: pts_of_Some aobjs_of_Some obj_at_def) apply (case_tac "levela = asid_pool_level") apply (fastforce dest: vs_lookup_slot_no_asid simp: ptes_of_Some pts_of_Some aobjs_of_Some obj_at_def) @@ -298,12 +306,11 @@ lemma state_vrefs_store_NonPageTablePTE_wp: apply (fastforce intro: vm_level_less_le_1) apply clarsimp apply (erule_tac x=pt in allE) - apply (clarsimp simp: fun_upd_def) - apply (subst state_vrefs_store_NonPageTablePTE'; fastforce simp: obj_at_def) + apply (subst state_vrefs_store_NonPageTablePTE'; fastforce simp: obj_at_def aobjs_of_Some pts_of_Some) done lemma store_pte_thread_st_auth[wp]: - "store_pte p pte \\s. P (thread_st_auth s)\" + "store_pte pt_t p pte \\s. P (thread_st_auth s)\" unfolding store_pte_def set_pt_def apply (wpsimp wp: set_object_wp) apply (clarsimp simp: get_tcb_def thread_st_auth_def tcb_states_of_state_def obj_at_def @@ -311,7 +318,7 @@ lemma store_pte_thread_st_auth[wp]: done lemma store_pte_thread_bound_ntfns[wp]: - "store_pte p pte \\s. P (thread_bound_ntfns s)\" + "store_pte pt_t p pte \\s. P (thread_bound_ntfns s)\" unfolding store_pte_def set_pt_def apply (wpsimp wp: set_object_wp) apply (clarsimp simp: get_tcb_def thread_bound_ntfns_def obj_at_def @@ -319,11 +326,11 @@ lemma store_pte_thread_bound_ntfns[wp]: done lemma store_pte_domains_of_state[wp]: - "store_pte p pte \\s. P (domains_of_state s)\" + "store_pte pt_t p pte \\s. P (domains_of_state s)\" unfolding store_pte_def set_pt_def by (wpsimp wp: set_object_wp) lemma mapM_x_store_pte_caps_of_state[wp]: - "mapM_x (swp store_pte InvalidPTE) slots \\s. P (asid_table s)\" + "mapM_x (swp (store_pte pt_t) InvalidPTE) slots \\s. P (asid_table s)\" by (wpsimp wp: mapM_x_wp') lemma state_bits_to_policy_vrefs_subseteq: @@ -342,15 +349,88 @@ lemma state_asids_to_policy_vrefs_subseteq: apply (erule state_asids_to_policy_aux.cases; fastforce intro: state_asids_to_policy_aux.intros) done +lemma vs_lookup_table_subseteq: + "\ vs_lookup_table bot_level asid vref s' = Some (lvl,ptr); + \pptr. pool_for_asid asid s' = Some pptr \ pool_for_asid asid s = Some pptr; + \pptr vref. vspace_for_pool pptr asid (asid_pools_of s') = Some vref + \ vspace_for_pool pptr asid (asid_pools_of s) = Some vref; + ptes_of s' = ptes_of s \ + \ vs_lookup_table bot_level asid vref s = Some (lvl,ptr)" + by (auto simp: vs_lookup_table_def in_obind_eq split: if_splits) + +lemma vs_refs_aux_subseteq: + assumes "\asid vref. vspace_for_pool 0 asid (K (asid_pool_of ao')) = Some vref + \ vspace_for_pool 0 asid (K (asid_pool_of ao)) = Some vref" + and "\idx vref. option_map (swp pt_apply idx) (pt_of ao') = Some vref + \ option_map (swp pt_apply idx) (pt_of ao) = Some vref" + and "aa_type ao' = aa_type ao" + shows "vs_refs_aux lvl ao' \ vs_refs_aux lvl ao" + apply (insert assms) + apply (case_tac ao'; case_tac ao; + clarsimp simp: vs_refs_aux_def graph_of_def image_iff pt_type_def + split: pt.splits if_splits) + apply (erule_tac x="ucast ac" in allE) + apply (fastforce simp: asid_low_bits_of_def vspace_for_pool_def + entry_for_pool_def in_obind_eq ucast_ucast_id) + apply (erule_tac x="ucast ac" in allE) + apply (intro exI conjI; fastforce simp: ucast_ucast_id vs_index_bits_def) + apply (erule_tac x="ucast ac" in allE) + apply (intro exI conjI; fastforce simp: ucast_ucast_id vs_index_bits_def) + done + +lemma state_vrefs_subseteq: + assumes "typs_of s' x = typs_of s x" + and "pts_of s' = pts_of s" + and "\pptr asid. pool_for_asid asid s' = Some pptr \ pool_for_asid asid s = Some pptr" + and "\pptr asid vref. vspace_for_pool pptr asid (asid_pools_of s') = Some vref + \ vspace_for_pool pptr asid (asid_pools_of s) = Some vref" + shows "state_vrefs s' x \ state_vrefs s x" + apply (subst state_vrefs_def) + using assms(1) apply clarsimp + apply (case_tac "vspace_objs_of s x") + apply (fastforce simp: opt_map_def a_type_def + split: option.splits arch_kernel_obj.splits kernel_object.splits if_splits)[1] + apply (prop_tac "vs_refs_aux lvl ao \ vs_refs_aux lvl ac") + apply (rule vs_refs_aux_subseteq) + using assms(4) + apply (fastforce simp: opt_map_def aa_type_def vspace_for_pool_def entry_for_pool_def obind_def + split: option.splits arch_kernel_obj.splits) + using assms(2) + apply (clarsimp simp: in_opt_map_eq fun_eq_iff) + apply (erule_tac x=x in allE) + apply (fastforce simp: opt_map_def aa_type_def split: if_splits arch_kernel_obj.splits) + apply (fastforce simp: opt_map_def aa_type_def + split: option.splits arch_kernel_obj.splits) + apply (rule_tac state_vrefsD) + apply (erule vs_lookup_table_subseteq) + using assms by fastforce+ + +lemma pas_refined_subseteq: + "\ pas_refined aag s; caps_of_state s' = caps_of_state s; + \x y. asid_table s' x = Some y \ asid_table s x = Some y; + \x. state_vrefs s' x \ state_vrefs s x; interrupt_irq_node s' = interrupt_irq_node s; + domains_of_state s' = domains_of_state s; thread_st_auth s' = thread_st_auth s; + thread_bound_ntfns s' = thread_bound_ntfns s; cdt s' = cdt s \ + \ pas_refined aag s'" + apply (auto simp: pas_refined_def) + apply (clarsimp simp: state_objs_to_policy_def) + apply (erule subsetD) + apply (clarsimp simp: auth_graph_map_def) + apply (rule exI, rule conjI, rule refl)+ + apply (erule state_bits_to_policy_vrefs_subseteq; clarsimp) + apply (erule subsetD, rule state_asids_to_policy_vrefs_subseteq, auto) + done + lemma store_InvalidPTE_state_objs_in_policy: - "\\s. state_objs_in_policy aag s \ invs s \ table_base p \ global_refs s \ - ((\a. vspace_for_asid a s = Some (table_base p)) \ table_index p \ kernel_mapping_slots)\ - store_pte p InvalidPTE + "\\s. state_objs_in_policy aag s \ invs s\ + store_pte pt_t p InvalidPTE \\_ s. state_objs_in_policy aag s\" apply (rule hoare_weaken_pre) apply (clarsimp simp: state_objs_to_policy_def pred_conj_def) apply wps apply (rule state_vrefs_store_NonPageTablePTE_wp) + apply (intro conjI; fastforce?) + apply (intro allI impI) apply clarsimp apply (rule conjI; clarsimp) apply (intro exI conjI) @@ -364,32 +444,35 @@ lemma store_InvalidPTE_state_objs_in_policy: apply (case_tac "level = asid_pool_level") apply (fastforce dest: vs_lookup_slot_no_asid simp: ptes_of_Some pts_of_Some aobjs_of_Some obj_at_def) + apply (frule vs_lookup_slot_level_type) + apply (fastforce simp: ptes_of_Some)+ apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp) apply (erule state_vrefsD) - apply (fastforce simp: aobjs_of_Some obj_at_def) + apply (fastforce simp: pts_of_Some vspace_objs_of_Some obj_at_def) apply clarsimp - apply (fastforce simp: vs_refs_aux_def graph_of_def pte_ref2_def split: if_splits) + apply (fastforce simp: vs_refs_aux_def graph_of_def pte_ref2_def split: if_splits pt.splits) apply (clarsimp simp: state_objs_to_policy_def) apply (erule subsetD) apply (clarsimp simp: auth_graph_map_def) apply (rule exI, rule conjI, rule refl)+ apply (erule state_bits_to_policy_vrefs_subseteq; clarsimp) apply (case_tac "level = asid_pool_level") - apply (fastforce dest: vs_lookup_table_no_asid + apply (fastforce dest: vs_lookup_table_no_asid[where pt_t=pt_t] simp: ptes_of_Some pts_of_Some aobjs_of_Some obj_at_def) - apply (frule level_of_table_vs_lookup_table) - apply (fastforce dest: vs_lookup_slot_no_asid + apply (frule level_of_table_vs_lookup_table[where pt_t=pt_t]) + apply (fastforce dest: vs_lookup_slot_no_asid[where pt_t=pt_t] simp: ptes_of_Some pts_of_Some aobjs_of_Some obj_at_def)+ apply (erule state_vrefsD) - apply (fastforce simp: aobjs_of_Some obj_at_def) + apply (fastforce simp: pts_of_Some vspace_objs_of_Some obj_at_def) apply clarsimp - apply (fastforce simp: vs_refs_aux_def graph_of_def pte_ref2_def split: if_splits) + apply (auto simp: vs_refs_aux_def graph_of_def pte_ref2_def split: if_splits pt.splits) + apply fastforce + apply fastforce done lemma store_InvalidPTE_state_asids_to_policy: - "\\s. state_asids_to_policy aag s \ pasPolicy aag \ invs s \ table_base p \ global_refs s \ - ((\a. vspace_for_asid a s = Some (table_base p)) \ table_index p \ kernel_mapping_slots)\ - store_pte p InvalidPTE + "\\s. state_asids_to_policy aag s \ pasPolicy aag \ invs s\ + store_pte pt_t p InvalidPTE \\_ s. state_asids_to_policy aag s \ pasPolicy aag\" apply (rule hoare_weaken_pre) apply (clarsimp simp: state_objs_to_policy_def pred_conj_def) @@ -406,30 +489,34 @@ lemma store_InvalidPTE_state_asids_to_policy: apply (case_tac "level = asid_pool_level") apply (fastforce dest: vs_lookup_slot_no_asid simp: ptes_of_Some pts_of_Some aobjs_of_Some obj_at_def) + apply (frule vs_lookup_slot_level_type) + apply (fastforce simp: ptes_of_Some)+ apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp) apply (erule state_vrefsD) - apply (fastforce simp: aobjs_of_Some obj_at_def) + apply (fastforce simp: pts_of_Some vspace_objs_of_Some obj_at_def) apply clarsimp - apply (fastforce simp: vs_refs_aux_def graph_of_def pte_ref2_def split: if_splits) + apply (fastforce simp: vs_refs_aux_def graph_of_def pte_ref2_def split: if_splits pt.splits) apply (erule subsetD) apply (erule state_asids_to_policy_vrefs_subseteq; clarsimp) apply (case_tac "level = asid_pool_level") - apply (fastforce dest: vs_lookup_table_no_asid + apply (fastforce dest: vs_lookup_table_no_asid[where pt_t=pt_t] simp: ptes_of_Some pts_of_Some aobjs_of_Some obj_at_def) - apply (frule level_of_table_vs_lookup_table) + apply (frule level_of_table_vs_lookup_table[where pt_t=pt_t]) apply (fastforce dest: vs_lookup_slot_no_asid simp: ptes_of_Some pts_of_Some aobjs_of_Some obj_at_def)+ apply (erule state_vrefsD) - apply (fastforce simp: aobjs_of_Some obj_at_def) + apply (fastforce simp: pts_of_Some vspace_objs_of_Some obj_at_def) apply clarsimp - apply (fastforce simp: vs_refs_aux_def graph_of_def pte_ref2_def split: if_splits) + apply (auto simp: vs_refs_aux_def graph_of_def pte_ref2_def split: if_splits pt.splits) + apply fastforce + apply fastforce done lemma mapM_x_swp_store_InvalidPTE_pas_refined: "\pas_refined aag and invs and - (\s. \x \ set slots. table_base x \ global_refs s \ - (\asid. vspace_for_asid asid s \ Some (table_base x)))\ - mapM_x (swp store_pte InvalidPTE) slots + (\s. \x \ set slots. table_base pt_t x \ global_refs s \ + (\asid. vspace_for_asid asid s \ Some (table_base pt_t x)))\ + mapM_x (swp (store_pte pt_t) InvalidPTE) slots \\_ s. pas_refined aag s\" supply state_asids_to_policy_arch_def[simp del] apply (rule hoare_strengthen_post) @@ -441,23 +528,25 @@ lemma mapM_x_swp_store_InvalidPTE_pas_refined: done lemma mapM_swp_store_pte_invs_unmap: - "\\s. invs s \ pte = InvalidPTE \ table_base p \ global_refs s - \ (\asid. vspace_for_asid asid s \ Some (table_base p))\ - store_pte p pte + "\\s. invs s \ pte = InvalidPTE \ table_base pt_t p \ global_refs s + \ (\asid. vspace_for_asid asid s \ Some (table_base pt_t p))\ + store_pte pt_t p pte \\_. invs\" by (wpsimp wp: store_pte_invs simp: wellformed_pte_def) lemma store_pte_pas_refined: - "\\s. pas_refined aag s \ invs s \ table_base p \ global_refs s \ - (\slot ref. caps_of_state s slot = Some (ArchObjectCap (PageTableCap (table_base p) ref))) \ - ((\asid. vspace_for_asid asid s = Some (table_base p)) \ table_index p \ kernel_mapping_slots)\ - store_pte p InvalidPTE + "\\s. pas_refined aag s \ invs s \ table_base pt_t p \ global_refs s \ + (\slot pt_t ref. caps_of_state s slot = Some (ArchObjectCap (PageTableCap (table_base pt_t p) pt_t ref)))\ + store_pte pt_t p InvalidPTE \\_. pas_refined aag\" supply state_asids_to_policy_arch_def[simp del] apply (clarsimp simp: pas_refined_def) apply (wpsimp wp: store_InvalidPTE_state_objs_in_policy store_InvalidPTE_state_asids_to_policy) done +crunch invalidate_tlb_by_asid + for pas_refined[wp]: "pas_refined aag" + lemma unmap_page_table_pas_refined: "\pas_refined aag and invs and K (vaddr \ user_region)\ unmap_page_table asid vaddr pt @@ -477,7 +566,6 @@ lemma unmap_page_table_pas_refined: apply (drule vs_lookup_table_valid_cap; clarsimp?) apply (fastforce simp: valid_cap_def valid_arch_cap_def valid_arch_cap_ref_def obj_at_def dest: caps_of_state_valid split: cap.splits arch_cap.splits) - apply (metis vs_lookup_table_vspace user_region_slots is_aligned_neg_mask2 pt_slot_offset_offset) done crunch unmap_page_table @@ -485,16 +573,16 @@ crunch unmap_page_table definition authorised_page_table_inv :: "'a PAS \ page_table_invocation \ bool" where "authorised_page_table_inv aag pti \ - case pti of PageTableMap cap cslot_ptr pde obj_ref \ - is_subject aag (fst cslot_ptr) \ is_subject aag (obj_ref && ~~ mask pt_bits) \ + case pti of PageTableMap cap cslot pte slot level \ + is_subject aag (fst cslot) \ is_subject aag (table_base (level_type level) slot) \ pas_cap_cur_auth aag (ArchObjectCap cap) - | PageTableUnmap cap cslot_ptr \ - is_subject aag (fst cslot_ptr) \ + | PageTableUnmap cap cslot \ + is_subject aag (fst cslot) \ aag_cap_auth aag (pasSubject aag) (ArchObjectCap cap) \ - (\p asid vspace_ref. cap = PageTableCap p (Some (asid, vspace_ref)) + (\p pt_t asid vspace_ref. cap = PageTableCap p pt_t (Some (asid, vspace_ref)) \ is_subject_asid aag asid \ - (\x \ set [p, p + 2 ^ pte_bits .e. p + 2 ^ pt_bits - 1]. - is_subject aag (x && ~~ mask pt_bits)))" + (\x \ set [p, p + 2 ^ pte_bits .e. p + 2 ^ (pt_bits pt_t) - 1]. + is_subject aag (table_base pt_t x)))" lemma perform_pt_inv_unmap_pas_refined: "\pas_refined aag and invs and valid_pti (PageTableUnmap cap ct_slot) @@ -503,11 +591,10 @@ lemma perform_pt_inv_unmap_pas_refined: \\_. pas_refined aag\" unfolding perform_pt_inv_unmap_def apply (wpsimp wp: set_cap_pas_refined get_cap_wp) - apply (strengthen invs_psp_aligned invs_vspace_objs invs_arch_state) + apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift) apply wps apply (rule hoare_vcg_all_lift[OF hoare_vcg_imp_lift'[OF mapM_x_wp_inv]], wpsimp wp: mapM_x_wp_inv) apply (rule hoare_vcg_conj_lift[OF hoare_strengthen_post[OF mapM_x_swp_store_InvalidPTE_pas_refined]], assumption) - apply (rule hoare_vcg_conj_lift[OF hoare_strengthen_post[OF mapM_x_swp_store_pte_invs_unmap]], assumption) apply (wpsimp wp: pt_lookup_from_level_wrp store_pte_invs_unmap store_pte_pas_refined mapM_x_wp_inv unmap_page_table_pas_refined hoare_vcg_imp_lift' hoare_vcg_ball_lift hoare_vcg_all_lift)+ @@ -518,13 +605,13 @@ lemma perform_pt_inv_unmap_pas_refined: valid_pti_def cte_wp_at_caps_of_state update_map_data_def aag_cap_auth_def cap_auth_conferred_def arch_cap_auth_conferred_def wellformed_mapdata_def cap_links_asid_slot_def cap_links_irq_def is_transferable.simps) - apply (prop_tac "table_base x = acap_obj cap") + apply (prop_tac "table_base NormalPT_T x = acap_obj cap") apply (drule (1) caps_of_state_aligned_page_table) apply (simp only: is_aligned_neg_mask_eq') apply (clarsimp simp: add_mask_fold) apply (drule subsetD[OF upto_enum_step_subset], clarsimp) - apply (drule neg_mask_mono_le[where n=pt_bits]) - apply (drule neg_mask_mono_le[where n=pt_bits]) + apply (drule neg_mask_mono_le[where n="pt_bits NormalPT_T"]) + apply (drule neg_mask_mono_le[where n="pt_bits NormalPT_T"]) apply (fastforce dest: plus_mask_AND_NOT_mask_eq) apply (rule conjI; clarsimp) apply (fastforce simp: cte_wp_at_caps_of_state cap_range_def @@ -532,21 +619,27 @@ lemma perform_pt_inv_unmap_pas_refined: apply (frule vspace_for_asid_target) apply (drule valid_vs_lookupD; clarsimp) apply (drule (1) unique_table_refsD[rotated]; clarsimp) - apply (drule (1) cap_to_pt_is_pt_cap) - apply (clarsimp simp: in_omonad obj_at_def) + apply (clarsimp simp: obj_at_def) + apply (drule (1) cap_to_pt_is_pt_cap_and_type) + apply (fastforce simp: in_omonad obj_at_def) apply (fastforce intro: valid_objs_caps) apply (clarsimp simp: is_cap_simps) done +(* FIXME AARCH64: move *) +lemma fun_upd2_apply: + "(f (x, y := z)) a b = (if a = x \ b = y then z else f a b)" + by (clarsimp simp: fun_upd2_def) + lemma vs_lookup_PageTablePTE: "\ vs_lookup_table level asid vref s' = Some (lvl', pt); pspace_aligned s; valid_vspace_objs s; valid_asid_table s; - invalid_pte_at p s; ptes_of s' = (ptes_of s)(p \ pte); is_PageTablePTE pte; + invalid_pte_at pt_t p s; ptes_of s' = (ptes_of s)(pt_t,p \ pte); is_PageTablePTE pte; asid_pools_of s' = asid_pools_of s; asid_table s' = asid_table s; vref \ user_region; - pts_of s (the (pte_ref pte)) = Some empty_pt; pt \ pptr_from_pte pte \ + pts_of s (the (pte_ref pte)) = Some (empty_pt NormalPT_T); pt \ pptr_from_pte pte \ \ \level' \ level. vs_lookup_table level' asid vref s = Some (lvl', pt)" - apply (induct level arbitrary: lvl' pt rule: bit0.from_top_full_induct[where y=max_pt_level]) + apply (induct level arbitrary: lvl' pt rule: bit1.from_top_full_induct[where y=max_pt_level]) apply (fastforce simp: geq_max_pt_level vs_lookup_table_def pool_for_asid_def obind_def) apply (rule_tac x=lvl' in exI) apply (frule vs_lookup_min_level, clarsimp) @@ -558,9 +651,18 @@ lemma vs_lookup_PageTablePTE: apply (fastforce elim: le_less_trans dest: vm_level_less_plus_1_mono) apply (erule_tac x="lvl'+1" in allE) apply clarsimp - apply (frule subst[where s="ptes_of s'" and P="\ptes. ptes _ = _"]) - apply assumption - apply (drule mp, fastforce simp: pte_ref_def2 ptes_of_Some split: if_splits) + apply (frule (1) subst[where P="\ptes. _ ptes = (_ :: pte option)"]) + apply (clarsimp simp: fun_upd2_apply split: if_splits) + apply (cases pte; clarsimp) + apply (drule mp) + apply clarsimp + apply (case_tac "(lvl' + 1) + 1 \ max_pt_level") + apply (fastforce simp: add_ac ptes_of_Some dest!: pptr_from_pte_aligned_pt_bits[where pte=pte]) + apply (prop_tac "is_aligned (pptr_from_pte pte) (pt_bits (level_type (lvl' + 1)))") + apply (fastforce simp: geq_max_pt_level plus_one_eq_asid_pool max_pt_level_plus_one[symmetric] + vs_lookup_max_pt_level_eq[where s=s and s'=s'] less_imp_neq not_le add_ac + dest: vs_lookup_table_is_aligned[where pt_ptr="pptr_from_pte (PageTablePTE _)"]) + apply (clarsimp simp: ptes_of_Some) apply (cases pte; clarsimp) apply (drule_tac bot_level=level' in vs_lookup_level) apply (subst vs_lookup_split_Some) @@ -574,7 +676,7 @@ lemma vs_lookup_PageTablePTE: apply (subst (asm) pt_walk.simps) apply (clarsimp simp: obind_def) apply (subst pt_walk.simps) - apply (clarsimp split: if_splits simp: obind_def) + apply (clarsimp split: if_splits option.splits simp: obind_def) apply (fastforce dest: vm_level_less_le_1) apply (fastforce dest: vm_level_less_max_pt_level vm_level_less_plus_1_mono) apply (case_tac "lvl' = asid_pool_level") @@ -584,10 +686,10 @@ lemma vs_lookup_PageTablePTE: lemma vs_lookup_PageTablePTE': "\ vs_lookup_table level asid vref s = Some (lvl', pt); pspace_aligned s; valid_vspace_objs s; valid_asid_table s; - invalid_pte_at p s; ptes_of s' = (ptes_of s)(p \ pte); is_PageTablePTE pte; + invalid_pte_at pt_t p s; ptes_of s' = (ptes_of s)(pt_t, p \ pte); is_PageTablePTE pte; asid_pools_of s' = asid_pools_of s; asid_table s' = asid_table s; vref \ user_region \ \ \level' \ level. vs_lookup_table level' asid vref s' = Some (lvl', pt)" - apply (induct level arbitrary: lvl' pt rule: bit0.from_top_full_induct[where y=max_pt_level]) + apply (induct level arbitrary: lvl' pt rule: bit1.from_top_full_induct[where y=max_pt_level]) apply (fastforce simp: geq_max_pt_level vs_lookup_table_def pool_for_asid_def obind_def) apply (rule_tac x=lvl' in exI) apply (frule vs_lookup_min_level, clarsimp) @@ -615,6 +717,11 @@ lemma vs_lookup_PageTablePTE': apply (cases pte; clarsimp) apply (frule is_aligned_pt[rotated]) apply (erule vs_lookup_table_pt_at; fastforce) + apply (clarsimp split: option.splits) + apply (rule context_conjI) + apply (clarsimp simp: fun_upd2_def) + apply clarsimp + apply (clarsimp simp: fun_upd2_def split: if_splits) apply (clarsimp simp: invalid_pte_at_def ptes_of_Some pts_of_Some aobjs_of_Some) apply (fastforce dest: vm_level_less_le_1) apply (fastforce dest: vm_level_less_max_pt_level vm_level_less_plus_1_mono) @@ -628,17 +735,14 @@ lemma state_vrefs_store_PageTablePTE: and "vs_lookup_slot level asid vref s = Some (level, p)" and "vref \ user_region" and "is_PageTablePTE pte" - and "invalid_pte_at p s" - and "pts_of s (the (pte_ref pte)) = Some empty_pt" - and "the (pte_ref pte) \ table_base p" - and "kheap s (table_base p) = Some (ArchObj (PageTable pt))" - shows "state_vrefs (s\kheap := \a. if a = table_base p - then Some (ArchObj (PageTable (\a. if a = table_index p - then pte - else pt a))) - else kheap s a\) = - (\x. if x = table_base p - then vs_refs_aux level (PageTable (\a. if a = table_index p then pte else pt a)) + and "invalid_pte_at (pt_type pt) p s" + and "pts_of s (the (pte_ref pte)) = Some (empty_pt NormalPT_T)" + and "the (pte_ref pte) \ table_base (pt_type pt) p" + and "(kheap s)(table_base (pt_type pt) p) = Some (ArchObj (PageTable pt))" + shows "state_vrefs (s\kheap := (kheap s)(table_base (pt_type pt) p \ + ArchObj (PageTable (pt_upd pt (table_index (pt_type pt) p) pte)))\) = + (\x. if x = table_base (pt_type pt) p + then vs_refs_aux level (PageTable (pt_upd pt (table_index (pt_type pt) p) pte)) else state_vrefs s x)" (is "state_vrefs ?s' = _") using assms @@ -652,47 +756,100 @@ lemma state_vrefs_store_PageTablePTE: apply (clarsimp simp: state_vrefs_def opt_map_def split: option.splits) apply (case_tac "x = pptr_from_pte pte") apply (clarsimp simp: pte_ref_def2 split: if_splits) - apply (fastforce simp: vs_refs_aux_def graph_of_def pte_ref2_def) + apply (fastforce simp: empty_pt_def vs_refs_aux_def graph_of_def pte_ref2_def split: if_splits pt.splits) apply (drule_tac s=s and pte=pte and p=p in vs_lookup_PageTablePTE) - apply (fastforce simp: pts_of_Some aobjs_of_Some opt_map_def pte_of_def obind_def - dest: pte_ptr_eq)+ + apply ((fastforce simp: ptes_of_pts_of_upd ptes_of_Some pts_of_Some aobjs_of_Some + intro: ptes_of_pts_of_upd + dest: pte_ptr_eq split: if_splits + | clarsimp simp: opt_map_def fun_upd_def split: option.splits)+; fail)+ apply clarsimp apply (drule vs_lookup_level) apply (case_tac "lvl = asid_pool_level") - apply (fastforce dest: vs_lookup_asid_pool simp: asid_pools_of_ko_at obj_at_def) + apply (fastforce dest: vs_lookup_asid_pool simp: asid_pools_of_ko_at obj_at_def) + apply (frule vs_lookup_slot_level_type) + apply (fastforce simp: ptes_of_Some pts_of_Some aobjs_of_Some)+ apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp) apply (fastforce dest: vs_lookup_table_unique_level split: if_splits) apply (clarsimp simp: state_vrefs_def opt_map_def) + apply (case_tac "level = asid_pool_level") + apply (fastforce dest: vs_lookup_asid_pool simp: asid_pools_of_ko_at obj_at_def) + apply (frule vs_lookup_slot_level_type) + apply ((fastforce simp: ptes_of_Some pts_of_Some aobjs_of_Some)+)[7] apply (frule vs_lookup_slot_table_base) apply clarsimp+ - apply (case_tac "x = table_base p"; clarsimp) - apply (drule_tac pte=pte and s'="?s'" in vs_lookup_PageTablePTE'; - fastforce dest: pte_ptr_eq simp: pts_of_Some aobjs_of_Some opt_map_def pte_of_def obind_def) - apply (drule_tac level=bot and pte=pte and s'="?s'" in vs_lookup_PageTablePTE'; - fastforce dest: pte_ptr_eq simp: pts_of_Some aobjs_of_Some opt_map_def pte_of_def obind_def) + apply (case_tac "x = table_base (pt_type pt) p"; clarsimp) + apply (drule_tac pte=pte and s'="?s'" in vs_lookup_PageTablePTE') + apply (((fastforce simp: ptes_of_pts_of_upd ptes_of_Some pts_of_Some aobjs_of_Some + intro: ptes_of_pts_of_upd + dest: pte_ptr_eq split: if_splits + | clarsimp simp: opt_map_def fun_upd_def fun_upd2_def split: if_splits option.splits)+; fail)+)[10] + apply (drule_tac level=bot and pte=pte and s'="?s'" in vs_lookup_PageTablePTE') + apply (((fastforce simp: ptes_of_pts_of_upd ptes_of_Some pts_of_Some aobjs_of_Some + intro: ptes_of_pts_of_upd + dest: pte_ptr_eq split: if_splits + | clarsimp simp: opt_map_def fun_upd_def fun_upd2_def split: if_splits option.splits)+; fail)+)[10] done lemma state_vrefs_store_PageTablePTE_wp: - "\\s. invs s \ is_PageTablePTE pte \ invalid_pte_at p s \ - pts_of s (the (pte_ref pte)) = Some empty_pt \ the (pte_ref pte) \ table_base p \ + "\\s. invs s \ is_PageTablePTE pte \ invalid_pte_at pt_t p s \ + pts_of s (the (pte_ref pte)) = Some (empty_pt NormalPT_T) \ the (pte_ref pte) \ table_base pt_t p \ (\level asid vref. vs_lookup_slot level asid vref s = Some (level, p) \ vref \ user_region \ - (\pt. ako_at (PageTable pt) (table_base p) s \ - P (\x. if x = table_base p - then vs_refs_aux level (PageTable (\a. if a = table_index p - then pte - else pt a)) + (\pt. pts_of s (table_base pt_t p) = Some pt \ pt_t = pt_type pt \ is_aligned p pte_bits \ + P (\x. if x = table_base (pt_type pt) p + then vs_refs_aux level (PageTable (pt_upd pt (table_index (pt_type pt) p) pte)) else state_vrefs s x)))\ - store_pte p pte + store_pte pt_t p pte \\_ s. P (state_vrefs s)\" unfolding store_pte_def set_pt_def apply (wpsimp wp: set_object_wp) - apply (fastforce simp: fun_upd_def obj_at_def state_vrefs_store_PageTablePTE) + apply (subst state_vrefs_store_PageTablePTE; simp?) + apply (fastforce simp: fun_upd_def fun_upd2_def obj_at_def state_vrefs_store_PageTablePTE split: if_splits) + apply (clarsimp simp: pts_of_Some aobjs_of_Some obj_at_def) + done + +lemma pt_apply_def2: + "pt_apply pt = (\idx. case pt of NormalPT npt \ npt (ucast idx) | VSRootPT vs \ vs (ucast idx))" + by (fastforce simp: pt_apply_def) + +lemma pt_apply_upd_eq': + "pt_apply (pt_upd pt idx pte) idx' = + (if idx && mask (ptTranslationBits (pt_type pt)) = idx' && mask (ptTranslationBits (pt_type pt)) + then pte else pt_apply pt idx')" + by (fastforce simp: pt_apply_def pt_upd_def ucast_ucast_mask vs_index_bits_def ptTranslationBits_def + dest: arg_cong[where f="UCAST(vs_index_len \ 64)"] arg_cong[where f="UCAST(9 \ 64)"] + intro: ucast_up_inj[where 'b=64] + split: pt.splits) + +(* FIXME AARCH64: replace vs_refs_aux with this definition *) +lemma vs_refs_aux_def2: + "vs_refs_aux level = (\ko. case ko of + ASIDPool pool \ (\(r,p). (p, ucast r, AASIDPool, Control)) ` graph_of (option_map ap_vspace o pool) + | PageTable pt \ \(r,(p, sz, auth)) \ graph_of (pte_ref2 level o pt_apply pt). + (\(p, a). (p, r && mask (ptTranslationBits (pt_type pt)), APageTable (pt_type pt), a)) + ` (ptr_range p sz \ auth) + | _ \ {})" + apply (rule ext)+ + apply (rule equalityI) + apply (clarsimp simp: vs_refs_aux_def ) + apply (case_tac ko; clarsimp) + apply (case_tac x2; clarsimp simp: pt_apply_def2) + apply (clarsimp simp: graph_of_def image_iff) + apply (rule_tac x="UCAST(vs_index_len \ 64) ac" in exI) + apply (fastforce simp: ucast_and_mask_drop ucast_ucast_id vs_index_bits_def ptTranslationBits_def) + apply (clarsimp simp: graph_of_def image_iff) + apply (rule_tac x="UCAST(9 \ 64) ac" in exI) + apply (fastforce simp: ucast_and_mask_drop ucast_ucast_id vs_index_bits_def ptTranslationBits_def) + apply (clarsimp simp: vs_refs_aux_def) + apply (case_tac ko; clarsimp) + apply (case_tac x2; clarsimp simp: pt_apply_def2) + apply (fastforce simp: graph_of_def image_iff ucast_ucast_mask vs_index_bits_def ptTranslationBits_def) + apply (fastforce simp: graph_of_def image_iff ucast_ucast_mask vs_index_bits_def ptTranslationBits_def) done lemma perform_pt_inv_map_pas_refined[wp]: - "\pas_refined aag and invs and valid_pti (PageTableMap acap (a, b) pte p) - and K (authorised_page_table_inv aag (PageTableMap acap (a, b) pte p))\ - perform_pt_inv_map acap (a,b) pte p + "\pas_refined aag and invs and valid_pti (PageTableMap acap (a, b) pte p level) + and K (authorised_page_table_inv aag (PageTableMap acap (a, b) pte p level))\ + perform_pt_inv_map acap (a,b) pte p level \\_. pas_refined aag\" unfolding perform_pt_inv_map_def apply (rule hoare_gen_asm) @@ -717,7 +874,7 @@ lemma perform_pt_inv_map_pas_refined[wp]: apply (frule (2) vs_lookup_table_is_aligned; clarsimp) apply (drule (1) vs_lookup_table_target) apply (drule valid_vs_lookupD, erule vref_for_level_user_region; clarsimp) - apply (frule (1) cap_to_pt_is_pt_cap, simp, fastforce intro: valid_objs_caps) + apply (frule (1) cap_to_pt_is_pt_cap_and_type, simp, fastforce intro: valid_objs_caps) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (clarsimp simp: is_cap_simps is_arch_update_def cap_master_cap_def split: cap.splits arch_cap.splits) @@ -733,17 +890,19 @@ lemma perform_pt_inv_map_pas_refined[wp]: apply (fastforce dest: sbta_ts simp: state_objs_to_policy_def) apply (fastforce dest: sbta_bounds simp: state_objs_to_policy_def) apply (clarsimp simp: state_objs_to_policy_def is_arch_update_def cap_master_cap_def) - apply (drule_tac caps="caps_of_state s" in sbta_cdt; fastforce elim: is_transferable.cases - split: if_splits) + apply (drule_tac caps="caps_of_state s" in sbta_cdt; + fastforce elim: is_transferable.cases split: if_splits) apply (fastforce dest: sbta_cdt_transferable simp: state_objs_to_policy_def) apply (clarsimp split: if_splits) - apply (clarsimp simp: authorised_page_table_inv_def vs_refs_aux_def split: arch_kernel_obj.splits) - apply (erule swap) - apply (clarsimp simp: graph_of_def pte_ref2_def split: if_split_asm) - apply (cases pte; clarsimp simp: aag_cap_auth_def cap_auth_conferred_def arch_cap_auth_conferred_def) + apply (clarsimp simp: authorised_page_table_inv_def split: arch_kernel_obj.splits) + apply (clarsimp simp: aag_cap_auth_def cap_auth_conferred_def arch_cap_auth_conferred_def) + apply (cases pte; clarsimp) + apply (clarsimp simp: vs_refs_aux_def2 graph_of_def) + apply (clarsimp simp: pt_apply_upd_eq' split: if_splits) + apply (clarsimp simp: pte_ref2_def pptr_from_pte_def) apply (erule subsetD) apply (clarsimp simp: auth_graph_map_def state_objs_to_policy_def) - apply (rule_tac x="table_base p" in exI, rule conjI, erule sym) + apply (rule_tac x="table_base (pt_type pt) p" in exI, rule conjI, erule sym) apply (rule exI, rule conjI, rule refl) apply (rule sbta_vref) apply (case_tac "level = asid_pool_level") @@ -751,9 +910,10 @@ lemma perform_pt_inv_map_pas_refined[wp]: simp: vs_lookup_slot_def vs_lookup_table_def invalid_pte_at_def) apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp) apply (erule state_vrefsD) - apply (fastforce simp: aobjs_of_Some obj_at_def) + apply (fastforce simp: pts_of_Some vspace_objs_of_Some obj_at_def) apply clarsimp - apply (fastforce simp: vs_refs_aux_def graph_of_def pte_ref2_def) + apply (fastforce simp: vs_refs_aux_def2 graph_of_def) + (* slow ~60s *) apply (clarsimp simp: is_arch_update_def cap_master_cap_def split: cap.splits arch_cap.splits option.splits) apply (fastforce dest: sbta_vref simp: pas_refined_def auth_graph_map_def state_objs_to_policy_def) @@ -765,7 +925,7 @@ lemma perform_pt_inv_map_pas_refined[wp]: cap_links_asid_slot_def label_owns_asid_slot_def) apply (fastforce dest: sata_asid) apply (clarsimp split: if_splits) - apply (fastforce dest!: state_asids_to_policy_aux.intros simp: vs_refs_aux_def) + apply (fastforce dest!: state_asids_to_policy_aux.intros simp: vs_refs_aux_def split: pt.splits) apply (fastforce dest!: sata_asid_lookup) apply (fastforce dest!: sata_asidpool) apply (clarsimp simp: pas_refined_def) @@ -786,7 +946,7 @@ lemma perform_page_table_invocation_pas_refined: (* FIXME move to AInvs *) lemma store_pte_ekheap[wp]: - "store_pte p pte \\s. P (ekheap s)\" + "store_pte pt_t p pte \\s. P (ekheap s)\" apply (simp add: store_pte_def set_pt_def) apply (wp get_object_wp) apply simp @@ -810,20 +970,13 @@ lemma set_asid_pool_thread_bound_ntfns[wp]: split: kernel_object.split_asm option.split) done -(* FIXME move to AInvs *) -lemma set_asid_pool_ekheap[wp]: - "set_asid_pool p pool \\s. P (ekheap s)\" - apply (simp add: set_asid_pool_def) - apply (wp get_object_wp | simp)+ - done - crunch set_asid_pool for integrity_autarch: "integrity aag X st" (wp: crunch_wps) lemma store_pte_respects: - "\integrity aag X st and K (is_subject aag (table_base p))\ - store_pte p pte + "\integrity aag X st and K (is_subject aag (table_base pt_t p))\ + store_pte pt_t p pte \\_. integrity aag X st\" apply (simp add: store_pte_def set_pt_def) apply (wp get_object_wp set_object_integrity_autarch) @@ -831,17 +984,12 @@ lemma store_pte_respects: done lemma integrity_arch_state[iff]: - "riscv_asid_table v = riscv_asid_table (arch_state s) + "arm_asid_table v = arm_asid_table (arch_state s) \ integrity aag X st (s\arch_state := v\) = integrity aag X st s" unfolding integrity_def by simp -lemma integrity_riscv_global_pts[iff]: - "integrity aag X st (s\arch_state := ((arch_state s)\riscv_global_pts := v\)\) = - integrity aag X st s" - unfolding integrity_def by simp - lemma integrity_riscv_kernel_vspace[iff]: - "integrity aag X st (s\arch_state := ((arch_state s)\riscv_kernel_vspace := v\)\) = + "integrity aag X st (s\arch_state := ((arch_state s)\arm_kernel_vspace := v\)\) = integrity aag X st s" unfolding integrity_def by simp @@ -864,7 +1012,8 @@ lemma pt_walk_is_subject: level \ max_pt_level; vptr \ user_region; is_subject aag pt_ptr \ \ is_subject aag pt" apply (induct level arbitrary: pt_ptr; clarsimp) - apply (erule_tac x="pptr_from_pte (the (ptes_of s (pt_slot_offset level pt_ptr vptr)))" in meta_allE) + apply (erule_tac x="pptr_from_pte (the (ptes_of s (level_type level) (pt_slot_offset level pt_ptr vptr)))" + in meta_allE) apply (subst (asm) pt_walk.simps) apply (clarsimp simp: obind_def split: if_splits option.splits) apply (drule meta_mp) @@ -872,22 +1021,18 @@ lemma pt_walk_is_subject: apply (subst pt_walk.simps, clarsimp simp: obind_def) apply clarsimp apply (erule meta_mp) - apply (frule vs_lookup_table_pt_at; clarsimp simp: pt_at_eq) + apply (subst (asm) ptes_of_Some) + apply (frule vs_lookup_table_is_aligned; clarsimp) apply (erule (1) is_subject_trans) apply (clarsimp simp: pas_refined_def auth_graph_map_def) apply (erule subsetD, clarsimp) apply (rule exI conjI refl sta_vref)+ apply (erule state_vrefsD) - apply (fastforce simp: pts_of_Some) + apply (fastforce simp: vspace_objs_of_Some pts_of_Some) apply clarsimp - apply (frule_tac pt_ptr=pt_ptr in pspace_aligned_pts_ofD, simp) - apply (clarsimp simp: ptes_of_def obind_def is_PageTablePTE_def vs_refs_aux_def split: option.splits) - apply (drule_tac g=y and f="pte_ref2 level" in graph_of_comp) - apply (fastforce simp: pte_ref2_def) - apply (fastforce simp: aobjs_of_Some pts_of_Some pptr_from_pte_def - dest: table_index_max_level_slots - elim: rev_bexI bexI_minus[rotated] - intro!: pts_of_Some_alignedD) + apply (clarsimp simp: vs_refs_aux_def2 graph_of_def) + apply (rule_tac x="pt_index level vptr" in exI) + apply (fastforce simp: pptr_from_pte_def pte_ref2_def split: pte.splits) done lemma pt_lookup_slot_from_level_is_subject: @@ -895,16 +1040,19 @@ lemma pt_lookup_slot_from_level_is_subject: pt_lookup_slot_from_level level bot_level pt_ptr vptr (ptes_of s) = Some (level', pt); (\asid. vs_lookup_table level asid vptr s = Some (level, pt_ptr)); level \ max_pt_level; vptr \ user_region; is_subject aag pt_ptr \ - \ is_subject aag (table_base pt)" - by (fastforce dest: pt_walk_is_aligned vs_lookup_table_is_aligned pt_walk_is_subject - simp: pt_lookup_slot_from_level_def obind_def split: option.splits) + \ is_subject aag (table_base (level_type level') pt)" + apply (clarsimp simp: pt_lookup_slot_from_level_def) + apply (frule vs_lookup_table_is_aligned, fastforce+) + apply (frule pt_walk_is_aligned, fastforce+) + apply (frule pt_walk_is_subject, fastforce+) + done lemma pt_lookup_from_level_is_subject: "\\s. pas_refined aag s \ pspace_aligned s \ valid_vspace_objs s \ valid_asid_table s \ is_subject aag pt_ptr \ level \ max_pt_level \ vref \ user_region \ (\asid. vs_lookup_table level asid vref s = Some (level, pt_ptr))\ pt_lookup_from_level level pt_ptr vref pt - \\rv _. is_subject aag (table_base rv)\, -" + \\(rv,lvl) _. is_subject aag (table_base (level_type lvl) rv)\, -" apply (wpsimp wp: pt_lookup_from_level_wp) apply (erule_tac level=level and bot_level=levela and pt_ptr=pt_ptr and vptr=vref in pt_lookup_slot_from_level_is_subject) @@ -915,23 +1063,24 @@ lemma unmap_page_table_respects: and K (is_subject_asid aag asid \ vaddr \ user_region)\ unmap_page_table asid vaddr pt \\_. integrity aag X st\" - apply (simp add: unmap_page_table_def sfence_def) - apply (wpsimp wp: pt_lookup_from_level_is_subject dmo_mol_respects hoare_vcg_conj_liftE_weaker - store_pte_respects pt_lookup_from_level_wrp[where Q="\_. integrity aag X st"] - | wp (once) hoare_drop_imps hoare_vcg_conj_elimE)+ - apply (intro conjI; clarsimp) - apply fastforce + unfolding unmap_page_table_def invalidate_tlb_by_asid_def + apply (wpsimp wp: dmo_no_mem_respects store_pte_respects Nondet_VCG.hoare_vcg_all_liftE + simp: imp_conjR + | rule hoare_strengthen_postE_R[OF pt_lookup_from_level_is_subject], fastforce + | rule hoare_vcg_conj_elimE hoare_vcg_conj_liftE_R hoare_drop_imps)+ + apply (intro conjI; clarsimp?) apply (rule aag_Control_into_owns[rotated], assumption) apply (drule sym) - apply (clarsimp simp: vspace_for_asid_def obj_at_def pas_refined_def) + apply (clarsimp simp: vspace_for_asid_def entry_for_asid_def obj_at_def pas_refined_def) apply (erule_tac A="state_asids_to_policy_aux _ _ _ _" in subsetD) apply (rule sata_asid_lookup) - apply (simp add: vspace_for_pool_def pool_for_asid_def) - apply (clarsimp simp: vspace_for_pool_def) + apply (simp add: vspace_for_pool_def pool_for_asid_def) + apply (clarsimp simp: entry_for_pool_def vspace_for_pool_def) apply (drule pool_for_asid_vs_lookupD) apply (erule state_vrefsD) - apply (fastforce simp: aobjs_of_Some asid_pools_of_ko_at obj_at_def) + apply (fastforce simp: vspace_objs_of_Some aobjs_of_Some asid_pools_of_ko_at obj_at_def) apply assumption + apply (clarsimp simp: vs_refs_aux_def) apply (fastforce simp: vs_refs_aux_def graph_of_def asid_low_bits_of_mask_eq[symmetric] word_size ucast_ucast_b is_up_def source_size_def target_size_def) apply (fastforce dest: vs_lookup_table_vref_independent[OF vspace_for_asid_vs_lookup]) @@ -948,15 +1097,16 @@ lemma perform_page_table_invocation_respects: cap.case_cong arch_cap.case_cong) apply (cases page_table_invocation; clarsimp) apply (wpsimp wp: set_cap_integrity_autarch store_pte_respects - simp: authorised_page_table_inv_def sfence_def) + simp: authorised_page_table_inv_def cleanByVA_PoU_def) apply (rename_tac cap fst_cslot_ptr snd_cslot_ptr) - apply (wpsimp wp: set_cap_integrity_autarch) + apply (wpsimp wp: set_cap_integrity_autarch simp:cleanCacheRange_PoU_def) apply (rule_tac I="\s. integrity aag X st s \ is_subject aag fst_cslot_ptr \ is_PageTableCap cap" in mapM_x_inv_wp; clarsimp) apply (rule_tac P="\s. integrity aag X st s \ is_PageTableCap cap" in hoare_vcg_conj_lift) apply (wpsimp wp: store_pte_respects) apply (clarsimp simp: authorised_page_table_inv_def) apply (case_tac cap; clarsimp) + apply (metis add_mask_fold) apply (wpsimp wp: unmap_page_table_respects)+ apply (clarsimp simp: authorised_page_table_inv_def valid_pti_def valid_arch_cap_def wellformed_acap_def wellformed_mapdata_def @@ -968,13 +1118,21 @@ lemma perform_pg_inv_get_addr_pas_refined [wp]: perform_pg_inv_get_addr ptr \\_. pas_refined aag\" unfolding perform_pg_inv_get_addr_def - by wpsimp + by wp auto + +lemma store_pte_vmid_for_asid[wp]: + " store_pte pt_t p pte + \\s. P (vmid_for_asid s asid)\" + apply (simp add: store_pte_def set_pt_def) + apply (wp get_object_wp set_object_wp) + by (auto simp: obj_at_def opt_map_def vmid_for_asid_def obind_def entry_for_pool_def + split: if_splits option.splits) lemma unmap_page_pas_refined: "\pas_refined aag and invs and K (vptr \ user_region)\ unmap_page pgsz asid vptr pptr \\_. pas_refined aag\" - unfolding unmap_page_def + unfolding unmap_page_def invalidate_tlb_by_asid_va_def cleanByVA_PoU_def apply (clarsimp simp: conj_ac | wpsimp wp: set_cap_pas_refined_not_transferable hoare_vcg_all_lift hoare_vcg_imp_lift' get_cap_wp store_pte_pas_refined store_pte_valid_arch_state_unreachable)+ @@ -989,25 +1147,24 @@ lemma unmap_page_pas_refined: apply (drule vs_lookup_table_valid_cap; clarsimp?) apply (fastforce simp: valid_cap_def valid_arch_cap_def valid_arch_cap_ref_def obj_at_def dest: caps_of_state_valid split: cap.splits arch_cap.splits) - apply (metis vs_lookup_table_vspace user_region_slots is_aligned_neg_mask2 pt_slot_offset_offset) done -definition authorised_slots :: "'a PAS \ pte \ obj_ref \ 's :: state_ext state \ bool" where - "authorised_slots aag m s \ case m of (pte, slot) \ +definition authorised_slots :: "'a PAS \ pte \ obj_ref \ vm_level \ 's :: state_ext state \ bool" where + "authorised_slots aag m s \ case m of (pte, slot, lvl) \ (\level asid vref x. vs_lookup_slot level asid vref s = Some (level, slot) \ vref \ user_region \ level \ max_pt_level \ pte_ref2 level pte = Some x \ (\a \ snd (snd x). \p \ ptr_range (fst x) (fst (snd x)). aag_has_auth_to aag a p)) \ - is_subject aag (table_base slot)" + is_subject aag (table_base (level_type lvl) slot)" definition authorised_page_inv :: "'a PAS \ page_invocation \ 's :: state_ext state \ bool" where "authorised_page_inv aag pgi s \ case pgi of PageMap cap ptr slots \ pas_cap_cur_auth aag (ArchObjectCap cap) \ is_subject aag (fst ptr) \ authorised_slots aag slots s | PageUnmap cap ptr \ pas_cap_cur_auth aag (ArchObjectCap cap) \ is_subject aag (fst ptr) - | PageGetAddr ptr \ True" + | _ \ True" lemma perform_pg_inv_unmap_pas_refined: "\pas_refined aag and invs and valid_page_inv (PageUnmap cap ct_slot) @@ -1059,65 +1216,86 @@ lemma set_cap_same_ref[wp]: done lemma perform_pg_inv_map_pas_refined: - "\pas_refined aag and invs and valid_page_inv (PageMap cap ct_slot (pte,slot)) - and authorised_page_inv aag (PageMap cap ct_slot (pte,slot))\ - perform_pg_inv_map cap ct_slot pte slot + "\pas_refined aag and invs and valid_page_inv (PageMap cap ct_slot (pte,slot,level)) + and authorised_page_inv aag (PageMap cap ct_slot (pte,slot,level))\ + perform_pg_inv_map cap ct_slot pte slot level \\_. pas_refined aag\" - unfolding perform_pg_inv_map_def - apply (wpsimp simp: simp: pas_refined_def state_objs_to_policy_def) - apply (subst conj_commute, subst conj_commute) - apply clarsimp - apply (rule hoare_vcg_conj_lift, wpsimp) - apply wps - apply (rule state_vrefs_store_NonPageTablePTE_wp) - apply (rule_tac Q'="\_. invs and pas_refined aag and K (\ is_PageTablePTE pte) - and authorised_page_inv aag (PageMap cap ct_slot (pte,slot)) - and same_ref (pte,slot) (ArchObjectCap cap)" - in hoare_strengthen_post[rotated]) - apply (clarsimp simp: pas_refined_def) - apply (rule conjI) - apply clarsimp - apply (intro exI, rule conjI, assumption) - apply clarsimp + unfolding perform_pg_inv_map_def invalidate_tlb_by_asid_va_def cleanCacheRange_PoU_def cleanByVA_PoU_def + apply wp + apply wpsimp + apply wp + apply (wpsimp wp: hoare_vcg_if_lift hoare_vcg_imp_lift) + apply (rule_tac Q'="\_. pas_refined aag" in hoare_strengthen_post) + apply (simp add: pas_refined_def state_objs_to_policy_def) + apply wp + apply wps + apply (rule state_vrefs_store_NonPageTablePTE_wp) + apply (clarsimp simp: pas_refined_def) + apply (rule_tac Q'="\_. invs and pas_refined aag and K (\ is_PageTablePTE pte) + and authorised_page_inv aag (PageMap cap ct_slot (pte,slot,level)) + and same_ref (pte,slot,level) (ArchObjectCap cap)" + in hoare_strengthen_post[rotated]) + apply (clarsimp simp: pas_refined_def) apply (rule conjI) apply clarsimp - apply (erule_tac A="state_asids_to_policy_aux _ _ _ _" in subsetD) - apply (erule state_asids_to_policy_aux.cases) - apply (fastforce dest: sata_asid) - apply (clarsimp simp: cte_wp_at_caps_of_state) - apply (clarsimp simp only: split: if_splits) - apply (clarsimp simp: vs_refs_aux_def) - apply (erule sata_asid_lookup) - apply assumption - apply (fastforce dest: sata_asidpool) - apply (clarsimp simp: auth_graph_map_def authorised_page_inv_def) - apply (erule state_bits_to_policy.cases) - apply (fastforce dest: sbta_caps simp: state_objs_to_policy_def) - apply (fastforce dest: sbta_untyped simp: state_objs_to_policy_def) - apply (fastforce dest: sbta_ts simp: state_objs_to_policy_def) - apply (fastforce dest: sbta_bounds simp: state_objs_to_policy_def) - apply (fastforce dest: sbta_cdt simp: state_objs_to_policy_def) - apply (fastforce dest: sbta_cdt_transferable simp: state_objs_to_policy_def) - apply (clarsimp split: if_split_asm) - apply (clarsimp simp: vs_refs_aux_def graph_of_def) - apply (erule_tac P="_ \ _" in swap) - apply (case_tac "level = asid_pool_level") - apply (fastforce dest!: vs_lookup_slot_no_asid - simp: ptes_of_Some pts_of_Some aobjs_of_Some obj_at_def) + apply (intro exI, rule conjI, assumption) + apply clarsimp + apply (rule conjI) + prefer 2 + apply clarsimp + apply (erule_tac A="state_asids_to_policy_aux _ _ _ _" in subsetD) + apply (erule state_asids_to_policy_aux.cases) + apply (fastforce dest: sata_asid) + apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (clarsimp simp only: split: if_splits) + apply (clarsimp simp: vs_refs_aux_def split: pt.splits) + apply (erule sata_asid_lookup) + apply assumption + apply (fastforce dest: sata_asidpool) + apply (clarsimp simp: auth_graph_map_def authorised_page_inv_def) + apply (erule state_bits_to_policy.cases) + apply (fastforce dest: sbta_caps simp: state_objs_to_policy_def) + apply (fastforce dest: sbta_untyped simp: state_objs_to_policy_def) + apply (fastforce dest: sbta_ts simp: state_objs_to_policy_def) + apply (fastforce dest: sbta_bounds simp: state_objs_to_policy_def) + apply (fastforce dest: sbta_cdt simp: state_objs_to_policy_def) + apply (fastforce dest: sbta_cdt_transferable simp: state_objs_to_policy_def) apply (clarsimp split: if_split_asm) - apply (case_tac pte; clarsimp simp: authorised_slots_def) - apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp) - apply (erule subsetD) - apply (clarsimp simp: state_objs_to_policy_def) - apply (rule exI, rule conjI, rule refl)+ - apply (rule sbta_vref) - apply (erule state_vrefsD) - apply (fastforce simp: aobjs_of_Some obj_at_def) - apply fastforce - apply (fastforce simp: vs_refs_aux_def graph_of_def) - apply (fastforce dest: sbta_vref simp: state_objs_to_policy_def) - apply (clarsimp simp: same_ref_def) - apply (wpsimp wp: arch_update_cap_invs_map set_cap_pas_refined_not_transferable) + apply (clarsimp simp: vs_refs_aux_def) + apply (case_tac "levela = asid_pool_level") + apply (fastforce dest!: vs_lookup_slot_no_asid + simp: ptes_of_Some pts_of_Some aobjs_of_Some obj_at_def) + apply (clarsimp simp: pt_upd_def split: pt.splits) + apply (clarsimp simp: graph_of_def split: if_split_asm) + apply (case_tac pte; clarsimp simp: authorised_slots_def) + apply (clarsimp simp: same_ref_def) + apply (drule (1) vs_lookup_slot_unique_level; clarsimp) + apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp) + apply (erule subsetD) + apply (clarsimp simp: state_objs_to_policy_def) + apply (rule exI, rule conjI, rule refl)+ + apply (rule sbta_vref) + apply (erule state_vrefsD) + apply (fastforce simp: ptes_of_Some pts_of_Some vspace_objs_of_Some obj_at_def) + apply fastforce + apply (fastforce simp: vs_refs_aux_def graph_of_def) + apply (clarsimp simp: graph_of_def split: if_split_asm) + apply (case_tac pte; clarsimp simp: authorised_slots_def level_type_def) + apply (clarsimp simp: same_ref_def) + apply (drule (1) vs_lookup_slot_unique_level; clarsimp) + apply (subst (asm) vs_lookup_slot_table_unfold; clarsimp) + apply (erule subsetD) + apply (clarsimp simp: state_objs_to_policy_def level_type_def) + apply (rule exI, rule conjI, rule refl)+ + apply (rule sbta_vref) + apply (erule state_vrefsD) + apply (fastforce simp: ptes_of_Some pts_of_Some vspace_objs_of_Some obj_at_def) + apply fastforce + apply (fastforce simp: vs_refs_aux_def graph_of_def) + apply (fastforce dest: sbta_vref simp: state_objs_to_policy_def) + apply (clarsimp simp: same_ref_def) + apply (wpsimp wp: arch_update_cap_invs_map set_cap_pas_refined_not_transferable) + apply wp apply (clarsimp simp: valid_page_inv_def authorised_page_inv_def cte_wp_at_caps_of_state is_frame_cap_def is_arch_update_def cap_master_cap_def split: arch_cap.splits) @@ -1131,7 +1309,7 @@ lemma perform_page_invocation_pas_refined: "\pas_refined aag and invs and authorised_page_inv aag pgi and valid_page_inv pgi\ perform_page_invocation pgi \\_. pas_refined aag\" - apply (simp add: perform_page_invocation_def) + unfolding perform_page_invocation_def perform_flush_def apply (wpsimp wp: perform_pg_inv_map_pas_refined perform_pg_inv_unmap_pas_refined) apply auto done @@ -1147,18 +1325,16 @@ lemma unmap_page_respects: apply (rule hoare_pre) apply (wpsimp wp: store_pte_respects hoare_drop_imps[where Q="\rv. integrity aag X st"] - simp: sfence_def is_aligned_mask[symmetric] + simp: is_aligned_mask[symmetric] cleanByVA_PoU_def + invalidate_tlb_by_asid_va_def invalidateTranslationSingle_def | wp (once) hoare_drop_imps - mapM_set''[where f="(\a. store_pte a InvalidPTE)" - and I="\x s. is_subject aag (x && ~~ mask pt_bits)" - and Q="integrity aag X st"] | wp (once) hoare_drop_imps[where Q'="\rv s. rv"])+ apply (clarsimp simp: pt_lookup_slot_def) apply (frule pt_lookup_slot_from_level_is_subject) apply (fastforce simp: valid_arch_state_asid_table dest: vs_lookup_table_vref_independent[OF vspace_for_asid_vs_lookup])+ apply (erule (1) is_subject_asid_trans) - apply (clarsimp simp: pas_refined_def vspace_for_asid_def vspace_for_pool_def) + apply (clarsimp simp: pas_refined_def entry_for_asid_def entry_for_pool_def vspace_for_asid_def) apply (erule subsetD[where A="state_asids_to_policy_aux _ _ _ _"]) apply (rule sata_asid_lookup) apply (fastforce simp: pool_for_asid_def) @@ -1171,6 +1347,14 @@ lemma unmap_page_respects: apply simp done +lemma set_cap_vmid_for_asid[wp]: + "set_cap cap cslot + \\s. P (vmid_for_asid s asid)\" + apply (simp add: set_cap_def) + apply (wpsimp wp: get_object_wp set_object_wp) + by (auto simp: obj_at_def opt_map_def vmid_for_asid_def obind_def entry_for_pool_def + split: if_splits option.splits) + lemma perform_page_invocation_respects: "\integrity aag X st and pas_refined aag and authorised_page_inv aag pgi and valid_page_inv pgi and valid_vspace_objs @@ -1184,44 +1368,39 @@ proof - apply (unfold authorised_page_inv_def) apply (simp add: perform_page_invocation_def mapM_discarded swp_def valid_page_inv_def valid_unmap_def authorised_page_inv_def authorised_slots_def - perform_pg_inv_map_def perform_pg_inv_unmap_def sfence_def + perform_pg_inv_map_def perform_pg_inv_unmap_def + invalidate_tlb_by_asid_va_def invalidateTranslationSingle_def + cleanByVA_PoU_def perform_flush_def do_flush_def split: page_invocation.split sum.split arch_cap.split option.split, safe) - apply ((wp set_cap_integrity_autarch unmap_page_respects - mapM_x_and_const_wp[OF store_pte_respects] store_pte_respects - | elim conjE - | clarsimp dest!: set_tl_subset_mp - | wpc)+) - apply (rule conjI) - apply (case_tac m; clarsimp) - apply (clarsimp simp: aag_cap_auth_def cte_wp_at_caps_of_state) - apply (prop_tac "a \ acap_asid' (FrameCap r R sz dev (Some (a,b)))", clarsimp) - apply (drule (1) sata_asid[where aag=aag]) - apply (clarsimp simp: pas_refined_def) - apply (drule (1) subsetD) - apply (fastforce dest: aag_wellformed_Control) - apply (fastforce simp: valid_arch_cap_def wellformed_mapdata_def split: if_splits) - apply (wpsimp wp: set_mrs_integrity_autarch set_message_info_integrity_autarch - simp: ipc_buffer_has_auth_def perform_pg_inv_get_addr_def) + apply ((wp set_cap_integrity_autarch unmap_page_respects + mapM_x_and_const_wp[OF store_pte_respects] store_pte_respects + hoare_vcg_if_lift hoare_vcg_imp_lift hoare_vcg_ex_lift hoare_vcg_disj_lift + | elim conjE + | clarsimp dest!: set_tl_subset_mp split del: if_split + | wpc)+) + apply (rule conjI) + apply (case_tac m; clarsimp) + apply (clarsimp simp: aag_cap_auth_def cte_wp_at_caps_of_state) + apply (prop_tac "a \ acap_asid' (FrameCap r R sz dev (Some (a,b)))", clarsimp) + apply (drule (1) sata_asid[where aag=aag]) + apply (clarsimp simp: pas_refined_def) + apply (drule (1) subsetD) + apply (fastforce dest: aag_wellformed_Control) + apply (fastforce simp: valid_arch_cap_def wellformed_mapdata_def split: if_splits) + apply (wpsimp wp: set_mrs_integrity_autarch set_message_info_integrity_autarch dmo_no_mem_respects + simp: ipc_buffer_has_auth_def perform_pg_inv_get_addr_def)+ done qed -lemma integrity_asid_table_entry_update': - "\ integrity aag X st s; atable = riscv_asid_table (arch_state s); is_subject aag v; - (\asid'. asid' \ 0 \ asid_high_bits_of asid' = asid_high_bits_of asid \ is_subject_asid aag asid') \ - \ integrity aag X st (s\arch_state := - arch_state s\riscv_asid_table := \a. if a = asid_high_bits_of asid - then (Some v) - else atable a\\)" - by (clarsimp simp: integrity_def) - lemma asid_table_entry_update_integrity: - "\integrity aag X st and (\s. atable = riscv_asid_table (arch_state s)) and K (is_subject aag v) - and K (\asid'. asid' \ 0 \ asid_high_bits_of asid' = asid_high_bits_of asid - \ is_subject_asid aag asid')\ - modify (\s. s\arch_state := arch_state s\riscv_asid_table := atable(asid_high_bits_of asid := Some v)\\) + "\\s. integrity aag X st s \ atable = arm_asid_table (arch_state s) + \ (\v. vopt = Some v \ is_subject aag v) + \ (\asid'. asid' \ 0 \ asid_high_bits_of asid' = asid_high_bits_of asid + \ is_subject_asid aag asid')\ + modify (\s. s\arch_state := arch_state s\arm_asid_table := atable(asid_high_bits_of asid := vopt)\\) \\_. integrity aag X st\" - by wpsimp (blast intro: integrity_asid_table_entry_update') + by (wpsimp simp: integrity_def) definition authorised_asid_control_inv :: "'a PAS \ asid_control_invocation \ bool" where "authorised_asid_control_inv aag aci \ @@ -1236,9 +1415,9 @@ lemma perform_asid_control_invocation_respects: \\_. integrity aag X st\" apply (simp add: perform_asid_control_invocation_def) apply (wpc, simp) - apply (wpsimp wp: set_cap_integrity_autarch cap_insert_integrity_autarch - asid_table_entry_update_integrity retype_region_integrity[where sz=12] - hoare_weak_lift_imp delete_objects_valid_vspace_objs delete_objects_valid_arch_state) + apply (wpsimp wp: hoare_weak_lift_imp set_cap_integrity_autarch asid_table_entry_update_integrity + cap_insert_integrity_autarch retype_region_integrity[where sz=12] + delete_objects_valid_vspace_objs delete_objects_valid_arch_state) apply (clarsimp simp: authorised_asid_control_inv_def ptr_range_def add.commute range_cover_def obj_bits_api_def default_arch_object_def pageBits_def word_bits_def) apply (subst is_aligned_neg_mask_eq[THEN sym], assumption) @@ -1249,7 +1428,7 @@ lemma perform_asid_control_invocation_respects: lemma state_vrefs_asid_pool_map: "\ ako_at (ASIDPool Map.empty) frame s; asid_table s (asid_high_bits_of base) = None \ - \ state_vrefs (s\arch_state := arch_state s\riscv_asid_table := \a. if a = asid_high_bits_of base + \ state_vrefs (s\arch_state := arch_state s\arm_asid_table := \a. if a = asid_high_bits_of base then Some frame else asid_table s a\\) = state_vrefs s" @@ -1258,8 +1437,8 @@ lemma state_vrefs_asid_pool_map: apply safe apply (subst (asm) state_vrefs_def, clarsimp) apply (case_tac "asid_high_bits_of asid = asid_high_bits_of base") - apply (clarsimp simp: vs_lookup_table_def pool_for_asid_def vspace_for_pool_def graph_of_def - asid_pools_of_ko_at obj_at_def vs_refs_aux_def aobjs_of_Some + apply (clarsimp simp: vs_lookup_table_def pool_for_asid_def vspace_for_pool_def entry_for_pool_def + graph_of_def obj_at_def vs_refs_aux_def aobjs_of_Some vspace_objs_of_Some split: if_splits) apply (subst (asm) asid_update.vs_lookup_table[simplified fun_upd_def]) apply (clarsimp simp: asid_update_def asid_pools_of_ko_at) @@ -1281,9 +1460,9 @@ lemma pas_refined_asid_control_helper: "authorised_asid_control_inv aag (MakePool frame slot parent base) \ \\s. pas_refined aag s \ ko_at (ArchObj (ASIDPool Map.empty)) frame s \ asid_table s (asid_high_bits_of base) = None\ - do asid_table <- gets (riscv_asid_table \ arch_state); + do asid_table <- gets asid_table; asid_table' <- return (asid_table(asid_high_bits_of base \ frame)); - modify (\s. s\arch_state := arch_state s\riscv_asid_table := asid_table'\\) + modify (\s. s\arch_state := arch_state s\arm_asid_table := asid_table'\\) od \\_. pas_refined aag\" unfolding pas_refined_def @@ -1303,7 +1482,7 @@ lemma pas_refined_asid_control_helper: apply (fastforce dest: sata_asid) apply (subst (asm) state_vrefs_asid_pool_map; clarsimp) apply (case_tac "asid_high_bits_of asid = asid_high_bits_of base") - apply (clarsimp simp: state_vrefs_def aobjs_of_Some obj_at_def vs_refs_aux_def graph_of_def) + apply (clarsimp simp: state_vrefs_def aobjs_of_Some vspace_objs_of_Some obj_at_def vs_refs_aux_def graph_of_def) apply (drule sata_asid_lookup[rotated]; fastforce) apply (clarsimp split: if_splits) apply (fastforce simp: authorised_asid_control_inv_def is_aligned_no_overflow aag_wellformed_refl) @@ -1348,12 +1527,11 @@ lemma perform_asid_control_invocation_pas_refined: pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \ (\x. asid_high_bits_of x = asid_high_bits_of base \ is_subject_asid aag x)" in hoare_strengthen_post) - apply (simp add: page_bits_def) apply (wp add: delete_objects_pspace_no_overlap hoare_vcg_ex_lift delete_objects_descendants_range_in delete_objects_invs_ex delete_objects_pas_refined del: Untyped_AI.delete_objects_pspace_no_overlap - | simp add: page_bits_def)+ + | simp add: )+ apply clarsimp apply (rename_tac s idx) apply (frule untyped_cap_aligned, simp add: invs_valid_objs) @@ -1379,11 +1557,11 @@ lemma perform_asid_control_invocation_pas_refined: apply simp apply simp apply (rule subset_refl) - apply (simp add: page_bits_def) + apply simp apply (frule_tac x=x in bspec) apply (simp add: is_aligned_no_overflow) apply (clarsimp simp: ptr_range_def invs_psp_aligned invs_valid_objs aag_cap_auth_def - descendants_range_def2 empty_descendants_range_in page_bits_def + descendants_range_def2 empty_descendants_range_in pas_refined_refl cap_links_asid_slot_def label_owns_asid_slot_def cap_links_irq_def range_cover_def obj_bits_api_def pageBits_def default_arch_object_def and_mask_eq_iff_shiftr_0 mask_zero) @@ -1391,23 +1569,6 @@ lemma perform_asid_control_invocation_pas_refined: apply (intro conjI; fastforce intro: empty_descendants_range_in) done -lemma copy_global_mappings_integrity: - "\integrity aag X st and K (is_aligned x pt_bits \ is_subject aag x)\ - copy_global_mappings x - \\_. integrity aag X st\" - apply (rule hoare_gen_asm) - apply (simp add: copy_global_mappings_def) - apply (wp mapM_x_wp[OF _ subset_refl] store_pte_respects) - apply (simp only: pt_index_def) - apply (subst table_base_offset_id) - apply simp - apply (clarsimp simp: pte_bits_def word_size_bits_def pt_bits_def - table_size_def ptTranslationBits_def mask_def) - apply (word_bitwise, fastforce) - apply clarsimp - apply wpsimp+ - done - definition authorised_asid_pool_inv :: "'a PAS \ asid_pool_invocation \ bool" where "authorised_asid_pool_inv aag api \ case api of Assign asid pool_ptr ct_slot \ @@ -1419,22 +1580,15 @@ lemma perform_asid_pool_invocation_respects: perform_asid_pool_invocation api \\_. integrity aag X st\" apply (unfold perform_asid_pool_invocation_def store_asid_pool_entry_def) - apply (wpsimp wp: set_asid_pool_integrity_autarch get_cap_wp set_cap_integrity_autarch - copy_global_mappings_integrity hoare_drop_imps) - apply (clarsimp simp: authorised_asid_pool_inv_def valid_apinv_def cte_wp_at_caps_of_state is_cap_simps) - apply (rule conjI) - apply (rule is_aligned_pt; fastforce simp: valid_cap_def dest: caps_of_state_valid) - apply (frule_tac ptr="(a,b)" in sbta_caps) - apply simp - apply (simp add: cap_auth_conferred_def arch_cap_auth_conferred_def) - apply (erule_tac x=a in is_subject_trans, assumption) - apply (fastforce simp: pas_refined_def auth_graph_map_def state_objs_to_policy_def) + apply (wpsimp wp: set_asid_pool_integrity_autarch get_cap_wp + set_cap_integrity_autarch hoare_drop_imps) + apply (clarsimp simp: authorised_asid_pool_inv_def) done lemma store_pte_state_vrefs_unreachable: "\\s. P (state_vrefs s) \ pspace_aligned s \ valid_vspace_objs s \ - valid_asid_table s \ (\level. \ \\ (level, table_base p) s)\ - store_pte p pte + valid_asid_table s \ (\level. \ \\ (level, table_base pt_t p) s)\ + store_pte pt_t p pte \\_ s. P (state_vrefs s)\" supply fun_upd_apply[simp del] apply (wpsimp simp: store_pte_def set_pt_def wp: set_object_wp) @@ -1446,87 +1600,41 @@ lemma store_pte_state_vrefs_unreachable: apply (rule state_vrefsD) apply (subst vs_lookup_table_unreachable_upd_idem; fastforce) apply (drule vs_lookup_level) - apply (prop_tac "x \ table_base p", clarsimp) + apply (prop_tac "x \ table_base pt_t p", clarsimp) apply (fastforce simp: fun_upd_def aobjs_of_Some opt_map_def) apply clarsimp apply fastforce apply (subst (asm) state_vrefs_def, clarsimp) apply (rule state_vrefsD) apply (subst (asm) vs_lookup_table_unreachable_upd_idem; fastforce) - apply (prop_tac "x \ table_base p") + apply (prop_tac "x \ table_base pt_t p") apply (subst (asm) vs_lookup_table_unreachable_upd_idem; fastforce dest: vs_lookup_level) apply (fastforce simp: fun_upd_def aobjs_of_Some) apply clarsimp apply clarsimp done -lemma copy_global_mappings_state_vrefs: - "\\s. P (state_vrefs s) \ invs s \ is_aligned pt_ptr pt_bits \ (\level. \ \\ (level, pt_ptr) s)\ - copy_global_mappings pt_ptr - \\_ s. P (state_vrefs s)\" - unfolding copy_global_mappings_def - apply clarsimp - apply wp - apply (rule_tac Q'="\_ s. P (state_vrefs s) \ pspace_aligned s \ valid_vspace_objs s \ - valid_asid_table s \ unique_table_refs s \ valid_vs_lookup s \ - valid_objs s \ is_aligned pt_ptr pt_bits \ is_aligned global_pt pt_bits \ - (\level. \ \\ (level, table_base (pt_ptr)) s) \ - (\level. \ \\ (level, table_base (global_pt)) s)" - in hoare_strengthen_post[rotated], clarsimp) - apply (wpsimp wp: store_pte_state_vrefs_unreachable store_pte_valid_vs_lookup_unreachable - store_pte_vs_lookup_table_unreachable store_pte_valid_vspace_objs - hoare_vcg_all_lift hoare_vcg_imp_lift' mapM_x_wp') - apply (prop_tac "table_base (pt_ptr + (x << pte_bits)) = pt_ptr \ - table_base (global_pt + (x << pte_bits)) = global_pt") - apply (metis mask_2pm1 table_base_plus) - apply (fastforce simp: valid_objs_caps ptes_of_wellformed_pte) - apply wpsimp+ - apply (simp add: invs_valid_global_vspace_mappings) - apply (intro conjI; clarsimp) - apply (frule invs_valid_global_arch_objs) - apply (frule valid_global_arch_objs_pt_at) - using not_in_global_refs_vs_lookup apply fastforce - done - -crunch copy_global_mappings - for tcb_domain_map_wellformed[wp]: "\s. P (tcb_domain_map_wellformed aag s)" - and asid_table[wp]: "\s. P (asid_table s)" - and cdt[wp]: "\s. P (cdt s)" - and thread_st_auth[wp]: "\s. P (thread_st_auth s)" - and thread_bound_ntfns[wp]: "\s. P (thread_bound_ntfns s)" - (wp: crunch_wps) - -lemma copy_global_mappings_pas_refined: - "\\s. pas_refined aag s \ invs s \ is_aligned pt_ptr pt_bits \ (\level. \ \\ (level, pt_ptr) s)\ - copy_global_mappings pt_ptr - \\_. pas_refined aag\" - apply (clarsimp simp: pas_refined_def state_objs_to_policy_def) - apply (rule hoare_pre) - apply (wps) - apply (wpsimp wp: copy_global_mappings_state_vrefs)+ - done - lemma store_asid_pool_entry_state_vrefs: "\\s. P (\x. if x = pool_ptr then vs_refs_aux asid_pool_level (ASIDPool (\a. if a = asid_low_bits_of asid - then Some pt_base + then Some (ASIDPoolVSpace None pt_base) else the (asid_pools_of s pool_ptr) a)) else if x = pt_base - then vs_refs_aux max_pt_level (the (aobjs_of s x)) + then vs_refs_aux max_pt_level (the (vspace_objs_of s x)) else state_vrefs s x) \ pspace_aligned s \ valid_vspace_objs s \ valid_asid_table s \ pool_for_asid asid s = Some pool_ptr \ (\pool. ako_at (ASIDPool pool) pool_ptr s \ pool (asid_low_bits_of asid) = None) \ (\level. \\\ (level, pt_base) s) \ - (\pt. pts_of s pt_base = Some pt \ kernel_mappings_only pt s)\ - store_asid_pool_entry pool_ptr asid (Some pt_base) + (\pt. pts_of s pt_base = Some (empty_pt VSRootPT_T))\ + store_asid_pool_entry pool_ptr asid (Some (ASIDPoolVSpace None pt_base)) \\_ s. P (state_vrefs s)\" unfolding store_asid_pool_entry_def set_asid_pool_def apply (wpsimp wp: set_object_wp get_cap_wp) apply (erule rsubst[where P=P]) apply (rule all_ext) apply (clarsimp split del: if_split) - apply (prop_tac "is_aligned pt_base pt_bits") + apply (prop_tac "is_aligned pt_base (pt_bits (pt_type (empty_pt VSRootPT_T)))") apply (fastforce elim: pspace_aligned_pts_ofD dest: invs_psp_aligned) apply safe apply (clarsimp split: if_splits) @@ -1535,7 +1643,7 @@ lemma store_asid_pool_entry_state_vrefs: apply (simp only: fun_upd_def) apply (subst asid_pool_map.vs_lookup_table[simplified fun_upd_def]) apply (fastforce simp: asid_pool_map_def asid_pools_of_ko_at - valid_apinv_def asid_low_bits_of_def aobjs_of_Some) + valid_apinv_def asid_low_bits_of_def ) apply fastforce apply fastforce apply fastforce @@ -1548,9 +1656,9 @@ lemma store_asid_pool_entry_state_vrefs: valid_apinv_def asid_low_bits_of_def aobjs_of_Some) apply clarsimp apply fastforce - apply (fastforce simp: pts_of_Some) + apply (fastforce simp: vspace_objs_of_Some pts_of_Some) apply (fastforce simp: pts_of_Some) - apply (fastforce simp: pts_of_Some) + apply (clarsimp simp: vspace_obj_of_def opt_map_def split: option.splits) apply (clarsimp simp: obj_at_def) apply (subst (asm) state_vrefs_def, clarsimp) apply (rename_tac asida vref) @@ -1561,7 +1669,8 @@ lemma store_asid_pool_entry_state_vrefs: valid_apinv_def asid_low_bits_of_def aobjs_of_Some) apply fastforce apply (prop_tac "asid \ asida") - apply (fastforce simp: vs_lookup_table_def vspace_for_pool_def asid_pools_of_ko_at obj_at_def + apply (fastforce simp: vs_lookup_table_def entry_for_pool_def vspace_for_pool_def + asid_pools_of_ko_at obj_at_def split: if_splits) apply fastforce apply fastforce @@ -1574,13 +1683,15 @@ lemma store_asid_pool_entry_state_vrefs: valid_apinv_def asid_low_bits_of_def aobjs_of_Some) apply clarsimp apply (case_tac "x = pool_ptr") - apply (prop_tac "asid_pools_of s pool_ptr = Some pool") + apply (prop_tac "asid_pools_of s pool_ptr = Some rv") apply (clarsimp simp: asid_pools_of_ko_at obj_at_def) apply (clarsimp simp: vs_refs_aux_def) apply (case_tac "asida = asid \ bot \ max_pt_level"; clarsimp) + apply (clarsimp simp: vspace_obj_of_def opt_map_def split: option.splits) apply (case_tac "x = pt_base") apply (fastforce dest: vs_lookup_level) - apply (fastforce simp: state_vrefs_def) + apply clarsimp + apply (fastforce simp: state_vrefs_def vspace_obj_of_def opt_map_def split: option.splits) done crunch store_asid_pool_entry @@ -1599,8 +1710,8 @@ lemma store_asid_pool_entry_pas_refined: is_subject aag pt_base \ is_subject_asid aag asid \ (\level. \\\ (level, pt_base) s) \ (\pool. ako_at (ASIDPool pool) pool_ptr s \ pool (asid_low_bits_of asid) = None) \ - (\pt. pts_of s pt_base = Some pt \ kernel_mappings_only pt s)\ - store_asid_pool_entry pool_ptr asid (Some pt_base) + (\pt. pts_of s pt_base = Some (empty_pt VSRootPT_T))\ + store_asid_pool_entry pool_ptr asid (Some (ASIDPoolVSpace None pt_base)) \\_ s. pas_refined aag s\" apply (clarsimp simp: pas_refined_def state_objs_to_policy_def) apply (rule hoare_pre) @@ -1626,12 +1737,12 @@ lemma store_asid_pool_entry_pas_refined: apply (rule sbta_vref) apply (drule pool_for_asid_vs_lookupD) apply (erule_tac vref=0 in state_vrefsD) - apply (simp add: asid_pools_of_ko_at aobjs_of_ako_at_Some) + apply (fastforce simp: asid_pools_of_ko_at aobjs_of_ako_at_Some vspace_objs_of_Some) apply clarsimp apply (fastforce simp: vs_refs_aux_def graph_of_def) - apply (fastforce simp: vs_refs_aux_def kernel_mappings_only_def + apply (fastforce simp: vs_refs_aux_def empty_pt_def vspace_obj_of_def opt_map_def graph_of_def pts_of_Some pte_ref2_def - dest: sbta_vref split: if_splits) + dest: sbta_vref split: if_splits option.splits) apply (erule state_asids_to_policy_aux.cases) apply (erule subsetD[where A="state_asids_to_policy_aux _ _ _ _"]) apply (fastforce dest: sata_asid) @@ -1641,7 +1752,7 @@ lemma store_asid_pool_entry_pas_refined: apply (drule_tac x="asid_high_bits_of asid" in bspec, clarsimp) apply (drule_tac x="asid_high_bits_of asida" in bspec, clarsimp) apply clarsimp - apply (drule asid_high_low) + apply (drule asid_high_low_inj[rotated]) apply (simp add: asid_low_bits_of_mask_eq[symmetric]) apply (prop_tac "is_up UCAST(9 \ 16) \ is_up UCAST(9 \ 64)") apply (clarsimp simp: is_up_def source_size_def target_size_def word_size) @@ -1652,39 +1763,18 @@ lemma store_asid_pool_entry_pas_refined: apply (rule sata_asid_lookup, fastforce) apply (frule pool_for_asid_vs_lookupD) apply (erule_tac vref=0 in state_vrefsD) - apply (simp add: asid_pools_of_ko_at aobjs_of_ako_at_Some) + apply (fastforce simp: asid_pools_of_ko_at aobjs_of_ako_at_Some vspace_objs_of_Some) apply simp apply (fastforce simp: vs_refs_aux_def graph_of_def) apply (case_tac "poolptr = pt_base") - apply (clarsimp simp: vs_refs_aux_def pts_of_Some) + apply (fastforce simp: vs_refs_aux_def pts_of_Some empty_pt_def vspace_obj_of_def opt_map_def + split: option.splits) apply (erule subsetD[where A="state_asids_to_policy_aux _ _ _ _"]) apply (fastforce simp: sata_asid_lookup) apply (erule subsetD[where A="state_asids_to_policy_aux _ _ _ _"]) apply (fastforce simp: sata_asidpool) done - -lemma copy_global_mappings_vs_lookup_table_noteq: - "\\s. vs_lookup_table level asid vref s \ Some (level, pt_ptr) \ invs s \ - is_aligned pt_ptr pt_bits \ vref \ user_region \ (\level. \ \\ (level, pt_ptr) s)\ - copy_global_mappings pt_ptr - \\_ s. vs_lookup_table level asid vref s \ Some (level, pt_ptr)\" - unfolding copy_global_mappings_def - apply clarsimp - apply wp - apply (rule_tac Q'="\_. pspace_aligned and valid_vspace_objs and valid_asid_table and - unique_table_refs and valid_vs_lookup and valid_objs and - (\s. vs_lookup_table level asid vref s \ Some (level, pt_ptr) \ - vref \ user_region \ is_aligned pt_ptr pt_bits \ - (\level. \ \\ (level, table_base pt_ptr) s))" - in hoare_strengthen_post[rotated], clarsimp) - apply (wpsimp wp: mapM_x_wp' store_pte_valid_vspace_objs store_pte_vs_lookup_table_unreachable - store_pte_valid_vs_lookup_unreachable hoare_vcg_all_lift hoare_vcg_imp_lift') - apply (metis valid_objs_caps ptes_of_wellformed_pte mask_2pm1 table_base_plus) - apply wpsimp - apply fastforce - done - lemma perform_asid_pool_invocation_pas_refined [wp]: "\pas_refined aag and invs and valid_apinv api and K (authorised_asid_pool_inv aag api)\ perform_asid_pool_invocation api @@ -1692,55 +1782,476 @@ lemma perform_asid_pool_invocation_pas_refined [wp]: apply (simp add: perform_asid_pool_invocation_def) apply (strengthen invs_psp_aligned invs_vspace_objs valid_arch_state_asid_table invs_arch_state | wpsimp simp: ako_asid_pools_of - wp: copy_global_mappings_invs copy_global_mappings_pas_refined - copy_global_mappings_copies copy_global_mappings_vs_lookup_table_noteq - store_asid_pool_entry_pas_refined set_cap_pas_refined get_cap_wp + wp: store_asid_pool_entry_pas_refined set_cap_pas_refined get_cap_wp arch_update_cap_invs_map hoare_vcg_all_lift hoare_vcg_imp_lift')+ apply (clarsimp simp: cte_wp_at_caps_of_state valid_apinv_def cong: conj_cong) apply (clarsimp simp: is_PageTableCap_def is_ArchObjectCap_def) - apply (clarsimp split: option.splits) - apply (clarsimp simp: authorised_asid_pool_inv_def) - apply (prop_tac "(\x xa xb. vs_lookup_table x xa xb s = Some (x, x41) \ xb \ user_region)") + apply (clarsimp simp: authorised_asid_pool_inv_def is_arch_update_def update_map_data_def + is_cap_simps cap_master_cap_def asid_bits_of_defs + split: option.splits) + apply (intro conjI) + apply (fastforce dest: cap_cur_auth_caps_of_state pas_refined_refl + simp: aag_cap_auth_def cap_auth_conferred_def arch_cap_auth_conferred_def + cap_links_asid_slot_def label_owns_asid_slot_def cap_links_irq_def) + apply (fastforce dest: caps_of_state_valid + simp: update_map_data_def valid_cap_def cap_aligned_def wellformed_mapdata_def) + apply (fastforce dest: cap_cur_auth_caps_of_state pas_refined_Control + simp: aag_cap_auth_def cap_auth_conferred_def arch_cap_auth_conferred_def) apply (frule (1) caps_of_state_valid) apply (clarsimp simp: valid_cap_def) apply (clarsimp simp: obj_at_def) apply (rename_tac asid' pool_ptr a b acap_obj level asid vref pt) apply (drule (1) vs_lookup_table_valid_cap; clarsimp) - apply (frule (1) cap_to_pt_is_pt_cap, simp add: pts_of_Some aobjs_of_Some, fastforce intro: valid_objs_caps) - apply (drule (1) unique_table_refsD[rotated]; clarsimp) - apply (clarsimp simp: is_cap_simps) - apply (clarsimp simp: is_arch_update_def update_map_data_def is_cap_simps cap_master_cap_def asid_bits_of_defs) - apply (intro conjI) - apply (fastforce dest: cap_cur_auth_caps_of_state pas_refined_refl - simp: update_map_data_def aag_cap_auth_def cap_auth_conferred_def arch_cap_auth_conferred_def - cap_links_asid_slot_def label_owns_asid_slot_def cap_links_irq_def) - apply (fastforce dest: caps_of_state_valid - simp: update_map_data_def valid_cap_def cap_aligned_def wellformed_mapdata_def) - apply (fastforce dest: caps_of_state_aligned_page_table) - apply (fastforce dest: unique_table_capsD[rotated]) - apply (fastforce dest: cap_not_in_valid_global_refs) - apply (fastforce dest: cap_cur_auth_caps_of_state pas_refined_Control - simp: aag_cap_auth_def cap_auth_conferred_def arch_cap_auth_conferred_def) - apply fastforce - apply (fastforce dest: invs_valid_table_caps simp: valid_table_caps_def) + apply (frule (1) cap_to_pt_is_pt_cap_and_type) + apply (simp add: pts_of_Some aobjs_of_Some) + apply (fastforce intro: valid_objs_caps) + apply (drule (1) unique_table_refsD[rotated]; clarsimp simp: is_cap_simps) + apply (fastforce dest: invs_valid_table_caps simp: valid_table_caps_def is_vsroot_cap_def ) + done + +lemma perform_vspace_invocation_respects[wp]: + "perform_vspace_invocation iv \integrity aag X st\" + unfolding perform_vspace_invocation_def perform_flush_def + by (wpsimp wp: dmo_no_mem_respects) + +crunch perform_vspace_invocation + for pas_refined[wp]: "pas_refined aag" + +(* FIXME AARCH64: move these *) +lemma tcb_states_of_state_fun_upd: + "map_option tcb_state (get_tcb p s) = (case val of TCB tcb \ Some (tcb_state tcb) | _ \ None) + \ tcb_states_of_state (s\kheap := (kheap s)(p \ val)\) = tcb_states_of_state s" + by (fastforce simp: tcb_states_of_state_def get_tcb_def split: kernel_object.splits) + +lemma thread_st_auth_fun_upd: + "map_option tcb_state (get_tcb p s) = (case val of TCB tcb \ Some (tcb_state tcb) | _ \ None) + \ thread_st_auth (s\kheap := (kheap s)(p \ val)\) = thread_st_auth s" + by (auto simp: tcb_states_of_state_fun_upd thread_st_auth_def) + +lemma thread_bound_ntfns_fun_upd: + "map_option tcb_bound_notification (get_tcb p s) = + (case val of TCB tcb \ Some (tcb_bound_notification tcb) | _ \ None) + \ thread_bound_ntfns (s\kheap := (kheap s)(p \ val)\) = thread_bound_ntfns s" + by (fastforce simp: thread_bound_ntfns_def get_tcb_def split: kernel_object.splits) + +lemma vcpu_save_reg_respects: + "\\s. integrity aag X st s \ option_map fst (arm_current_vcpu (arch_state s)) = Some vr\ + vcpu_save_reg vr reg + \\_. integrity aag X st\" + unfolding vcpu_save_reg_def vcpu_update_def + apply (wpsimp wp: set_vcpu_wp get_vcpu_wp hoare_vcg_all_lift hoare_vcg_imp_lift dmo_wp + simp: readVCPUHardwareReg_def) + apply (clarsimp simp: integrity_def) + apply (subst tcb_states_of_state_fun_upd, fastforce simp: get_tcb_def obj_at_def)+ + apply (rule conjI) + apply (erule_tac x=vr in allE)+ + apply (auto elim!: tro_trans_spec simp: in_opt_map_eq + intro!: tro_arch arch_troa_vcpu_save_reg)[1] + apply (rule ccontr) + apply (auto simp: in_opt_map_eq) + done + +lemma save_virt_timer_respects: + "\\s. integrity aag X st s \ option_map fst (arm_current_vcpu (arch_state s)) = Some vr\ + save_virt_timer vr + \\_. integrity aag X st\" + (is "valid ?P _ _") + unfolding save_virt_timer_def vcpu_update_def + apply (wpsimp wp: set_vcpu_wp get_vcpu_wp hoare_vcg_all_lift hoare_vcg_imp_lift + simp: readVCPUHardwareReg_def read_cntpct_def)+ + apply (wp dmo_wp) + apply (rule_tac Q'="K ?P" in hoare_strengthen_post[rotated]) + apply (clarsimp simp: integrity_def simp del: fun_upd_apply) + apply (subst tcb_states_of_state_fun_upd; clarsimp simp: get_tcb_def obj_at_def)+ + apply (rule conjI) + apply (erule_tac x=vr in allE)+ + apply (auto elim!: tro_trans_spec simp: in_opt_map_eq + intro!: tro_arch arch_troa_vcpu_save_virt_timer)[1] + apply (rule ccontr) + apply (auto simp: in_opt_map_eq)[1] + by (wpsimp wp: dmo_no_mem_respects vcpu_save_reg_respects)+ + +lemma vgic_update_respects: + "\\s. integrity aag X st s \ option_map fst (arm_current_vcpu (arch_state s)) = Some vr + \ v = getf (machine_state s) + \ (setf = vgic_hcr_update \ getf = gic_vcpu_ctrl_hcr_val \ + setf = vgic_vmcr_update \ getf = gic_vcpu_ctrl_vmcr_val \ + setf = vgic_apr_update \ getf = gic_vcpu_ctrl_apr_val)\ + vgic_update vr (setf (\_. v)) + \\_. integrity aag X st\" + unfolding vgic_update_def vcpu_update_def + apply (wpsimp wp: set_vcpu_wp get_vcpu_wp dmo_wp) + apply (clarsimp simp: integrity_def) + apply (subst tcb_states_of_state_fun_upd, fastforce simp: get_tcb_def obj_at_def)+ + apply (rule conjI) + apply (erule_tac x=vr in allE)+ + apply (auto elim!: tro_trans_spec simp: in_opt_map_eq + intro!: tro_arch arch_troa_vcpu_save_vgic)[1] + apply (rule ccontr) + apply (auto simp: in_opt_map_eq) + done + +lemmas vgic_updates_respect = + vgic_update_respects[where setf=vgic_hcr_update and getf=gic_vcpu_ctrl_hcr_val, simplified] + vgic_update_respects[where setf=vgic_vmcr_update and getf=gic_vcpu_ctrl_vmcr_val, simplified] + vgic_update_respects[where setf=vgic_apr_update and getf=gic_vcpu_ctrl_apr_val, simplified] + +lemma get_gic_vcpu_ctrl_rvs: + "\\_. True\ do_machine_op get_gic_vcpu_ctrl_hcr \\rv s. rv = gic_vcpu_ctrl_hcr_val (machine_state s)\" + "\\_. True\ do_machine_op get_gic_vcpu_ctrl_vmcr \\rv s. rv = gic_vcpu_ctrl_vmcr_val (machine_state s)\" + "\\_. True\ do_machine_op get_gic_vcpu_ctrl_apr \\rv s. rv = gic_vcpu_ctrl_apr_val (machine_state s)\" + unfolding get_gic_vcpu_ctrl_hcr_def get_gic_vcpu_ctrl_vmcr_def get_gic_vcpu_ctrl_apr_def + by (wpsimp wp: dmo_wp)+ + +lemma vcpu_disable_None_respects[wp]: + "vcpu_disable None \integrity aag X st\" + unfolding vcpu_disable_def + by (wpsimp wp: dmo_no_mem_respects) + +lemma vcpu_disable_Some_respects: + "\\s. integrity aag X st s \ option_map fst (arm_current_vcpu (arch_state s)) = Some vcpu\ + vcpu_disable (Some vcpu) + \\_. integrity aag X st\" + unfolding vcpu_disable_def + by (wpsimp wp: dmo_no_mem_respects vcpu_save_reg_respects + save_virt_timer_respects vgic_updates_respect get_gic_vcpu_ctrl_rvs) + +lemma vgic_update_lr_respects: + "\\s. integrity aag X st s \ option_map fst (arm_current_vcpu (arch_state s)) = Some vr + \ lr = gic_vcpu_ctrl_lr_val (word_of_nat vreg) (machine_state s)\ + vgic_update_lr vr vreg lr + \\_. integrity aag X st\" + unfolding vgic_update_lr_def vgic_update_def vcpu_update_def + apply (wpsimp wp: set_vcpu_wp get_vcpu_wp dmo_wp hoare_vcg_all_lift hoare_vcg_imp_lift)+ + apply (clarsimp simp: integrity_def) + apply (subst tcb_states_of_state_fun_upd, fastforce simp: get_tcb_def obj_at_def)+ + apply (rule conjI) + apply (erule_tac x=vr in allE)+ + apply (auto elim!: tro_trans_spec simp: in_opt_map_eq + intro!: tro_arch arch_troa_vcpu_save_vgic)[1] + apply (rule ccontr) + apply (auto simp: in_opt_map_eq) + done + +lemma vcpu_save_reg_range_respects: + "\\s. integrity aag X st s \ map_option fst (arm_current_vcpu (arch_state s)) = Some vr\ + vcpu_save_reg_range vr from to + \\_. integrity aag X st\" + unfolding vcpu_save_reg_range_def + apply (rule_tac Q'="\_. P" and P=P for P in hoare_strengthen_post) + by (wpsimp wp: mapM_x_wp' vcpu_save_reg_respects)+ + +lemma vcpu_save_respects: + "\\s. integrity aag X st s \ arm_current_vcpu (arch_state s) = vb\ + vcpu_save vb + \\_. integrity aag X st\" + by (wpsimp wp: vcpu_save_reg_range_respects mapM_wp' vgic_update_lr_respects + vgic_updates_respect dmo_no_mem_respects get_gic_vcpu_ctrl_rvs + save_virt_timer_respects vcpu_save_reg_respects + simp: vcpu_save_def get_gic_vcpu_ctrl_lr_def + | wp dmo_wp)+ + +crunch vcpu_enable, vcpu_restore + for integrity_autarch: "integrity aag X st" + (wp: dmo_no_mem_respects mapM_wp' mapM_x_wp') + +lemma vcpu_switch_integrity: + "\\s. integrity aag X st s \ (\v. vcpu = Some v \ is_subject aag v)\ + vcpu_switch vcpu + \\_. integrity aag X st\" + unfolding vcpu_switch_def + by (wpsimp wp: vcpu_restore_integrity_autarch vcpu_save_respects vcpu_enable_integrity_autarch + vcpu_disable_Some_respects dmo_no_mem_respects)+ + +lemma vcpu_restore_reg_respects: + "\\s. integrity aag X st s \ (\v a. arm_current_vcpu (arch_state s) = Some (v,a) \ v = vcpu)\ + vcpu_restore_reg vcpu reg + \\_. integrity aag X st\" + unfolding vcpu_restore_reg_def + by (wpsimp wp: dmo_no_mem_respects) + +lemma restore_virt_timer_respects: + "\\s. integrity aag X st s \ option_map fst (arm_current_vcpu (arch_state s)) = Some vr\ + restore_virt_timer vr + \\_. integrity aag X st\" + (is "valid ?P _ _") + unfolding restore_virt_timer_def vcpu_write_reg_def vcpu_update_def vcpu_read_reg_def read_cntpct_def + apply (wpsimp wp: vcpu_restore_reg_respects set_vcpu_wp get_vcpu_wp + dmo_no_mem_respects dmo_wp hoare_vcg_imp_lift + simp_del: fun_upd_apply) + apply (rule_tac Q'="K ?P" in hoare_strengthen_post[rotated]) + apply (clarsimp simp: integrity_def) + apply (subst tcb_states_of_state_fun_upd, fastforce simp: get_tcb_def obj_at_def)+ + apply (rule conjI) + apply (erule_tac x=vr in allE)+ + apply (auto elim!: tro_trans_spec simp: in_opt_map_eq + intro!: tro_arch arch_troa_vcpu_restore_vtimer)[1] + apply (rule ccontr) + apply (auto simp: in_opt_map_eq)[1] + apply (wpsimp wp: vcpu_restore_reg_respects)+ + done + +lemma vcpu_enable_respects: + "\\s. integrity aag X st s \ option_map fst (arm_current_vcpu (arch_state s)) = Some vr\ + vcpu_enable vr + \\_. integrity aag X st\" + unfolding vcpu_enable_def + by (wpsimp wp: restore_virt_timer_respects vcpu_restore_reg_respects dmo_no_mem_respects) + +lemma vcpu_restore_respects: + "\\s. integrity aag X st s \ option_map fst (arm_current_vcpu (arch_state s)) = Some vr\ + vcpu_restore vr + \\_. integrity aag X st\" + unfolding vcpu_restore_def vcpu_restore_reg_range_def + by (wpsimp wp: vcpu_enable_respects vcpu_restore_reg_respects dmo_no_mem_respects mapM_x_wp' mapM_wp') + +lemma vcpu_switch_respects: + "vcpu_switch vcpu \integrity aag X st\" + unfolding vcpu_switch_def + by (wpsimp wp: vcpu_restore_respects vcpu_disable_Some_respects + vcpu_save_respects vcpu_enable_respects dmo_no_mem_respects) + +lemma arch_thread_set_integrity_autarch: + "\integrity aag X st and K (is_subject aag ptr)\ + arch_thread_set f ptr + \\_. integrity aag X st\" + unfolding arch_thread_set_def + by (wpsimp wp: set_object_integrity_autarch) + +lemma vcpu_invalidate_active_respects[wp]: + "vcpu_invalidate_active + \integrity aag X st\" + unfolding vcpu_invalidate_active_def + by wpsimp + +lemma dissociate_vcpu_tcb_respects: + "\integrity aag X st and K (is_subject aag vcpu \ is_subject aag tcb)\ + dissociate_vcpu_tcb vcpu tcb + \\_. integrity aag X st\" + unfolding dissociate_vcpu_tcb_def set_vcpu_def get_vcpu_def arch_thread_get_def + by (wpsimp wp: as_user_integrity_autarch set_object_integrity_autarch + arch_thread_set_integrity_autarch) + +crunch vcpu_invalidate_active + for vcpus_of[wp]: "\s. P (vcpus_of s)" + (simp: vcpu_invalidate_active_def vcpu_disable_def) + +lemma thread_set_vcpus_of[wp]: + "thread_set f tptr \\s. P (vcpus_of s)\" + unfolding thread_set_def + apply (wpsimp wp: set_object_wp) + apply (erule_tac P=P in rsubst) + apply (fastforce simp: get_tcb_def opt_map_def split: option.splits kernel_object.splits) + done + +lemma dissociate_vcpu_tcb_vcpus_of: + "\\s. P ((vcpus_of s)(v := Some ((the (vcpus_of s v))\vcpu_tcb := None\)))\ + dissociate_vcpu_tcb v tcb + \\_ s. P (vcpus_of s)\" + unfolding dissociate_vcpu_tcb_def + by (wpsimp wp: as_user_wp_thread_set_helper hoare_drop_imps get_vcpu_wp simp: fun_upd_def) + +lemma associate_vcpu_tcb_respects: + "\integrity aag X st and K (is_subject aag vcpu) and K (is_subject aag tcb)\ + associate_vcpu_tcb vcpu tcb + \\_. integrity aag X st\" + unfolding associate_vcpu_tcb_def + apply (wpsimp wp: vcpu_switch_integrity set_vcpu_integrity_autarch hoare_drop_imps + arch_thread_set_integrity_autarch dissociate_vcpu_tcb_respects get_vcpu_wp) + apply (rule_tac Q'="\a b. integrity aag X st b \ is_subject aag vcpu \ is_subject aag tcb \ + (\v x. vcpus_of b vcpu = Some v \ vcpu_tcb v = Some x \ is_subject aag x)" + in hoare_strengthen_post) + apply (wpsimp wp: dissociate_vcpu_tcb_respects dissociate_vcpu_tcb_vcpus_of arch_thread_get_wp)+ + apply (fastforce intro: associated_vcpu_is_subject associated_tcb_is_subject + simp: get_tcb_def obj_at_def opt_map_def + split: option.splits) + done + +lemma invoke_vcpu_inject_irq_respects: + "\integrity aag X st and K (is_subject aag vcpu)\ + invoke_vcpu_inject_irq vcpu index vir + \\_. integrity aag X st\" + unfolding invoke_vcpu_inject_irq_def set_gic_vcpu_ctrl_lr_def vgic_update_lr_def vgic_update_def + by (wpsimp wp: vcpu_update_integrity_autarch) + +lemma invoke_vcpu_read_register_respects: + "invoke_vcpu_read_register vcpu reg \integrity aag X st\" + unfolding invoke_vcpu_read_register_def read_vcpu_register_def readVCPUHardwareReg_def + by wpsimp + +lemma invoke_vcpu_write_register_respects: + "\integrity aag X st and K (is_subject aag vcpu)\ + invoke_vcpu_write_register vcpu reg val + \\_. integrity aag X st\" + unfolding invoke_vcpu_write_register_def write_vcpu_register_def + vcpu_write_reg_def writeVCPUHardwareReg_def + by (wpsimp wp: vcpu_update_integrity_autarch) + +lemma invoke_vcpu_ack_vppi_respects: + "\integrity aag X st and K (is_subject aag vcpu)\ + invoke_vcpu_ack_vppi vcpu vppi + \\_. integrity aag X st\" + unfolding invoke_vcpu_ack_vppi_def + by (wpsimp wp: vcpu_update_integrity_autarch) + + +definition authorised_vcpu_inv where + "authorised_vcpu_inv aag iv \ + case iv of VCPUSetTCB vcpu tcb \ is_subject aag vcpu \ is_subject aag tcb + | VCPUInjectIRQ vcpu index vir \ is_subject aag vcpu + | VCPUReadRegister vcpu reg \ is_subject aag vcpu + | VCPUWriteRegister vcpu reg val \ is_subject aag vcpu + | VCPUAckVPPI vcpu vppi \ is_subject aag vcpu" + +lemma perform_vcpu_invocation_respects[wp]: + "\integrity aag X st and K (authorised_vcpu_inv aag iv) and pas_refined aag + and invs and valid_vcpu_invocation iv and is_subject aag \ cur_thread\ + perform_vcpu_invocation iv + \\_. integrity aag X st\" + unfolding perform_vcpu_invocation_def + apply (wpsimp wp: associate_vcpu_tcb_respects invoke_vcpu_ack_vppi_respects invoke_vcpu_inject_irq_respects + invoke_vcpu_read_register_respects invoke_vcpu_write_register_respects) + apply (auto simp: authorised_vcpu_inv_def) + done + +lemma set_vcpu_thread_bound_ntfns[wp]: + "set_vcpu ptr vcpu \\s. P (thread_bound_ntfns s)\" + apply (wpsimp wp: set_vcpu_wp) + apply (erule_tac P=P in rsubst) + apply (rule ext) + apply (clarsimp simp: thread_bound_ntfns_def get_tcb_def obj_at_def) + done + +lemma arch_thread_set_thread_bound_ntfns[wp]: + "arch_thread_set f tptr \\s. P (thread_bound_ntfns s)\" + apply (wpsimp wp: arch_thread_set_wp) + apply (erule_tac P=P in rsubst) + apply (rule ext) + apply (clarsimp simp: thread_bound_ntfns_def get_tcb_def obj_at_def) + done + +lemma set_vcpu_thread_st_auth[wp]: + "set_vcpu ptr vcpu \\s. P (thread_st_auth s)\" + apply (wpsimp wp: set_vcpu_wp) + apply (erule_tac P=P in rsubst) + apply (rule ext) + apply (clarsimp simp: thread_st_auth_def tcb_states_of_state_def get_tcb_def obj_at_def) + done + +lemma arch_thread_thread_st_auth[wp]: + "arch_thread_set f tptr \\s. P (thread_st_auth s)\" + apply (wpsimp wp: arch_thread_set_wp) + apply (erule_tac P=P in rsubst) + apply (rule ext) + apply (clarsimp simp: thread_st_auth_def tcb_states_of_state_def get_tcb_def obj_at_def) + done + +crunch perform_vcpu_invocation + for irq_map_wellformed[wp]: "irq_map_wellformed aag" + and state_irqs_to_policy[wp]: "\s. P (state_irqs_to_policy aag s)" + and caps_of_state[wp]: "\s. P (caps_of_state s)" + and interrupt_irq_node[wp]: "\s. P (interrupt_irq_node s)" + and domains_of_state[wp]: "\s. P (domains_of_state s)" + and asid_table[wp]: "\s. P (asid_table s)" + and cdt[wp]: "\s. P (cdt s)" + and tcb_bound_notification[wp]: "\s. P (thread_bound_ntfns s)" + and thread_st_auth[wp]: "\s. P (thread_st_auth s)" + (wp: crunch_wps simp: crunch_simps) + +lemma set_vcpu_valid_asid_table[wp]: + "set_vcpu p v \valid_asid_table\" + apply (wpsimp wp: set_vcpu_wp) + apply (clarsimp simp: obj_at_def opt_map_def) done +lemma arch_thread_set_valid_asid_table[wp]: + "arch_thread_set f t \valid_asid_table\" + apply (wpsimp wp: arch_thread_set_wp) + apply (clarsimp simp: get_tcb_def obj_at_def opt_map_def + split: option.splits kernel_object.splits) + done + +lemma as_user_asid_pools_of[wp]: + "as_user t f \\s. P (asid_pools_of s)\" + unfolding as_user_def + apply (wpsimp wp: set_object_wp) + apply (erule_tac P=P in rsubst) + apply (fastforce simp: get_tcb_def opt_map_def split: option.splits) + done + +lemma as_user_valid_asid_table[wp]: + "as_user t f \valid_asid_table\" + apply (rule hoare_lift_Pf[where f=asid_table]) + apply (rule hoare_lift_Pf[where f=asid_pools_of]) + apply wpsimp+ + done + +lemma set_vcpu_vspace_objs_of[wp]: + "set_vcpu p vcpu \\s. P (vspace_objs_of s)\" + apply (wpsimp wp: set_vcpu_wp) + apply (clarsimp simp: opt_map_def typ_at_eq_kheap_obj) + done + +lemma thread_set_vspace_objs_of[wp]: + "thread_set f tptr \\s. P (vspace_objs_of s)\" + unfolding thread_set_def + apply (wpsimp wp: set_object_wp) + apply (erule_tac P=P in rsubst) + apply (fastforce simp: get_tcb_def opt_map_def split: option.splits kernel_object.splits) + done + +lemma arch_thread_set_vspace_objs_of[wp]: + "arch_thread_set f tptr \\s. P (vspace_objs_of s)\" + apply (wpsimp wp: arch_thread_set_wp) + apply (fastforce simp: get_tcb_def opt_map_def split: option.splits kernel_object.splits) + done + +(* FIXME AARCH64: weaken in ArchKHeap_AI *) +lemma vs_lookup_vspace_objs_lift: + assumes "\P. f \\s. P (vspace_objs_of s)\" + assumes "\P. f \\s. P (asid_table s)\" + shows "f \\s. P (vs_lookup s)\" + by (intro vs_lookup_lift vspace_objs_of_pts_lift vspace_objs_of_aps_lift assms) + +crunch dissociate_vcpu_tcb + for valid_asid_table[wp]: "valid_asid_table" + (wp: crunch_wps) + +crunch perform_vcpu_invocation + for vspace_objs_of[wp]: "\s. P (vspace_objs_of s)" + (wp: crunch_wps as_user_wp_thread_set_helper) + +lemma perform_vcpu_invocation_state_vrefs[wp]: + "perform_vcpu_invocation iv \\s. P (state_vrefs s)\" + unfolding state_vrefs_def + apply (rule hoare_lift_Pf[where f=vspace_objs_of] ) + apply (rule vs_lookup_vspace_objs_lift) + apply wpsimp+ + done + +crunch perform_vcpu_invocation + for pas_refined[wp]: "pas_refined aag" + (simp: pas_refined_def state_objs_to_policy_def ignore: perform_vcpu_invocation) + definition authorised_arch_inv :: "'a PAS \ arch_invocation \ 's :: state_ext state \ bool" where "authorised_arch_inv aag ai s \ case ai of InvokePageTable pti \ authorised_page_table_inv aag pti | InvokePage pgi \ authorised_page_inv aag pgi s | InvokeASIDControl aci \ authorised_asid_control_inv aag aci - | InvokeASIDPool api \ authorised_asid_pool_inv aag api" + | InvokeASIDPool api \ authorised_asid_pool_inv aag api + | InvokeVCPU vi \ authorised_vcpu_inv aag vi + | InvokeVSpace vi \ True" lemma invoke_arch_respects: - "\integrity aag X st and authorised_arch_inv aag ai and - pas_refined aag and invs and valid_arch_inv ai and is_subject aag \ cur_thread\ + "\integrity aag X st and authorised_arch_inv aag ai and pas_refined aag and invs + and valid_arch_inv ai and is_subject aag \ cur_thread\ arch_perform_invocation ai \\_. integrity aag X st\" apply (simp add: arch_perform_invocation_def) apply (wpsimp wp: perform_page_table_invocation_respects perform_page_invocation_respects - perform_asid_control_invocation_respects perform_asid_pool_invocation_respects) + perform_asid_control_invocation_respects perform_asid_pool_invocation_respects + perform_vspace_invocation_respects) apply (auto simp: authorised_arch_inv_def valid_arch_inv_def) done @@ -1759,15 +2270,16 @@ lemma vspace_for_asid_is_subject: "\ vspace_for_asid a s = Some xaa; pas_refined aag s; valid_asid_table s; is_subject_asid aag a \ \ is_subject aag xaa" apply (frule vspace_for_asid_vs_lookup) - apply (clarsimp simp: vspace_for_asid_def) + apply (clarsimp simp: vspace_for_asid_def entry_for_asid_def) apply (frule pool_for_asid_vs_lookupD) - apply (frule (1) pool_for_asid_validD) - apply (clarsimp simp: vspace_for_pool_def pool_for_asid_def asid_pools_of_ko_at obj_at_def) - apply (frule_tac vrefs="state_vrefs s" in sata_asid_lookup) - apply (rule_tac level=asid_pool_level and asid=a and vref=0 in state_vrefsD) - by (fastforce simp: aobjs_of_Some vs_refs_aux_def graph_of_def asid_low_bits_of_mask_eq[symmetric] - ucast_ucast_b is_up_def source_size_def target_size_def word_size pas_refined_def - dest: aag_wellformed_Control)+ + apply (clarsimp simp: vspace_for_pool_def entry_for_pool_def pool_for_asid_def asid_pools_of_ko_at ) + apply (frule_tac pdptr = "(ap_vspace v'a)" and vrefs="state_vrefs s" and a=Control in sata_asid_lookup) + apply (fastforce simp: vs_refs_aux_def graph_of_def asid_low_bits_of_mask_eq[symmetric] + ucast_ucast_b is_up_def opt_map_def source_size_def target_size_def + word_size pas_refined_def obj_at_def + dest: aag_wellformed_Control + intro!: state_vrefsD)+ + done lemma decode_page_table_invocation_authorised: "\invs and pas_refined aag and cte_wp_at ((=) (ArchObjectCap cap)) slot @@ -1784,12 +2296,13 @@ lemma decode_page_table_invocation_authorised: apply (unfold decode_page_table_invocation_def decode_pt_inv_map_def authorised_arch_inv_def) apply (wpsimp simp: Let_def is_final_cap_def if_fun_split) apply (clarsimp simp: cte_wp_at_caps_of_state) - apply (prop_tac "\y \ set [x, x + 2 ^ pte_bits .e. x + 2 ^ pt_bits - 1]. table_base y = x") + apply (rename_tac x t m s) + apply (prop_tac "\y \ set [x, x + 2 ^ pte_bits .e. x + 2 ^ pt_bits t - 1]. table_base t y = x") apply (drule (1) caps_of_state_aligned_page_table) apply (clarsimp simp only: is_aligned_neg_mask_eq' add_mask_fold) apply (drule subsetD[OF upto_enum_step_subset], clarsimp) - apply (drule neg_mask_mono_le[where n=pt_bits]) - apply (drule neg_mask_mono_le[where n=pt_bits]) + apply (drule_tac n="pt_bits t" in neg_mask_mono_le) + apply (drule_tac n="pt_bits t" in neg_mask_mono_le) apply (fastforce dest: plus_mask_AND_NOT_mask_eq) apply (intro conjI; clarsimp) apply (clarsimp simp: authorised_page_table_inv_def) @@ -1801,7 +2314,7 @@ lemma decode_page_table_invocation_authorised: dest: caps_of_state_aligned_page_table pt_walk_is_aligned) apply (frule vs_lookup_table_vref_independent[OF vspace_for_asid_vs_lookup, simplified]) apply (erule pt_walk_is_subject[rotated 4]; fastforce intro: vspace_for_asid_is_subject - simp: user_vtop_canonical_user + simp: user_vtop_leq_canonical_user user_region_def) apply (clarsimp simp: aag_cap_auth_def cap_auth_conferred_def arch_cap_auth_conferred_def cap_links_asid_slot_def label_owns_asid_slot_def cap_links_irq_def) @@ -1809,42 +2322,17 @@ lemma decode_page_table_invocation_authorised: cap_auth_conferred_def arch_cap_auth_conferred_def) done -lemma decode_frame_invocation_authorised: +lemma decode_fr_inv_flush_authorised: "\invs and pas_refined aag and cte_wp_at ((=) (ArchObjectCap cap)) slot and (\s. \(cap, slot) \ set excaps. cte_wp_at ((=) cap) slot s) and K (is_FrameCap cap \ (\(cap, slot) \ {(ArchObjectCap cap, slot)} \ set excaps. aag_cap_auth aag (pasObjectAbs aag (fst slot)) cap \ is_subject aag (fst slot) \ (\v \ cap_asid' cap. is_subject_asid aag v)))\ - decode_frame_invocation label msg slot cap excaps + decode_fr_inv_flush label msg slot cap excaps \\rv. authorised_arch_inv aag rv\,-" - unfolding decode_frame_invocation_def authorised_arch_inv_def decode_fr_inv_map_def - apply (wpsimp wp: check_vp_wpR simp: Let_def authorised_page_inv_def) - apply (rule conj_imp_strg) - apply (cases excaps; clarsimp) - apply (clarsimp simp: aag_cap_auth_def cap_auth_conferred_def arch_cap_auth_conferred_def - cap_links_asid_slot_def cap_links_irq_def authorised_slots_def) - apply (prop_tac "msg ! 0 \ user_region") - apply (fastforce dest: not_le_imp_less user_vtop_canonical_user - elim: dual_order.trans is_aligned_no_overflow_mask - simp: user_region_def vmsz_aligned_def) - apply (rule conjI) - apply (frule (1) pt_lookup_slot_vs_lookup_slotI, clarsimp) - apply (drule (1) vs_lookup_slot_unique_level; clarsimp) - apply (clarsimp simp: cte_wp_at_caps_of_state make_user_pte_def pte_ref2_def split: if_splits) - apply (subst (asm) ptrFromPAddr_addr_from_ppn[OF is_aligned_pageBitsForSize_table_size]) - apply (fastforce dest: caps_of_state_valid - simp: valid_cap_def cap_aligned_def pageBitsForSize_pt_bits_left) - apply (fastforce simp: vspace_cap_rights_to_auth_def mask_vm_rights_def validate_vm_rights_def - vm_kernel_only_def vm_read_only_def - split: if_splits) - apply (clarsimp simp: pt_lookup_slot_def pt_lookup_slot_from_level_def) - apply (subst table_base_pt_slot_offset) - apply (fastforce simp: cte_wp_at_caps_of_state - dest: caps_of_state_aligned_page_table pt_walk_is_aligned) - apply (frule vs_lookup_table_vref_independent[OF vspace_for_asid_vs_lookup, simplified]) - apply (erule pt_walk_is_subject[rotated 4]; fastforce intro: vspace_for_asid_is_subject) - done + unfolding authorised_arch_inv_def authorised_page_inv_def decode_fr_inv_flush_def Let_def + by wpsimp lemma decode_asid_control_invocation_authorised: "\invs and pas_refined aag and cte_wp_at ((=) (ArchObjectCap cap)) slot @@ -1857,13 +2345,9 @@ lemma decode_asid_control_invocation_authorised: \authorised_arch_inv aag\, -" unfolding decode_asid_control_invocation_def authorised_arch_inv_def authorised_asid_control_inv_def apply wpsimp - apply (cases excaps; clarsimp) - apply (rename_tac excaps_tail) - apply (case_tac excaps_tail; clarsimp) - apply (clarsimp simp: aag_cap_auth_def cte_wp_at_caps_of_state) - apply (drule (1) caps_of_state_valid[where cap="UntypedCap _ _ _ _"]) - apply (fastforce simp: valid_cap_def cap_aligned_def is_cap_simps cap_auth_conferred_def - dest: pas_refined_Control) + apply (cases excaps; cases "tl excaps"; clarsimp simp: aag_cap_auth_def cte_wp_at_caps_of_state) + apply (fastforce dest: caps_of_state_valid[where cap="UntypedCap _ _ _ _"] pas_refined_Control + simp: valid_cap_def cap_aligned_def is_cap_simps cap_auth_conferred_def) done lemma decode_asid_pool_invocation_authorised: @@ -1879,9 +2363,9 @@ lemma decode_asid_pool_invocation_authorised: apply wpsimp apply (erule swap[where P="authorised_asid_pool_inv _ _"]) apply (cases excaps; clarsimp) - apply (clarsimp simp: authorised_asid_pool_inv_def is_ASIDPoolCap_def) + apply (clarsimp simp: authorised_asid_pool_inv_def is_ASIDPoolCap_def + pas_refined_def state_objs_to_policy_def auth_graph_map_def) apply (rule conjI) - apply (clarsimp simp: pas_refined_def state_objs_to_policy_def auth_graph_map_def) apply (drule subsetD) apply (fastforce dest!: sbta_caps simp: obj_refs_def cte_wp_at_caps_of_state @@ -1892,6 +2376,90 @@ lemma decode_asid_pool_invocation_authorised: simp: cte_wp_at_caps_of_state valid_cap_def) done +lemma decode_fr_inv_map_authorised: + "\invs and pas_refined aag and cte_wp_at ((=) (ArchObjectCap cap)) slot + and (\s. \(cap, slot) \ set excaps. cte_wp_at ((=) cap) slot s) + and K (is_FrameCap cap \ (\(cap, slot) \ {(ArchObjectCap cap, slot)} \ set excaps. + aag_cap_auth aag (pasObjectAbs aag (fst slot)) cap \ + is_subject aag (fst slot) \ + (\v \ cap_asid' cap. is_subject_asid aag v)))\ + decode_fr_inv_map label msg slot cap excaps + \\rv. authorised_arch_inv aag rv\,-" + unfolding decode_fr_inv_map_def Let_def fun_app_def + apply (wpsimp wp: check_vp_wpR whenE_throwError_wp)+ + apply (subst imp_conjL[symmetric]) + apply (subst imp_disjL[symmetric]) + apply (rule impI) + apply clarsimp + apply (prop_tac "msg ! 0 \ user_region") + apply (prop_tac "\ user_vtop < msg ! 0 + mask (pageBitsForSize xb) \ msg!0 \ user_region") + apply (fastforce intro: dual_order.trans user_vtop_leq_canonical_user is_aligned_no_overflow_mask + simp: user_region_def vmsz_aligned_def not_less) + apply (fastforce dest: cte_wp_valid_cap simp: valid_cap_def wellformed_mapdata_def) + apply (cases excaps, clarsimp) + apply (drule_tac x="excaps ! 0" in bspec, clarsimp)+ + apply (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def + aag_cap_auth_def cap_links_asid_slot_def cap_links_irq_def pte_ref2_def + make_user_pte_def cap_auth_conferred_def arch_cap_auth_conferred_def) + apply (rule conjI) + apply (frule (1) pt_lookup_slot_vs_lookup_slotI, clarsimp) + apply (drule (1) vs_lookup_slot_unique_level; clarsimp) + apply (fastforce simp: cte_wp_at_caps_of_state make_user_pte_def pte_ref2_def + vspace_cap_rights_to_auth_def validate_vm_rights_def + mask_vm_rights_def vm_read_only_def vm_kernel_only_def + split: if_splits) + apply (fastforce elim: pt_lookup_slot_from_level_is_subject[rotated 4] + intro: vs_lookup_table_vref_independent[OF vspace_for_asid_vs_lookup] + pas_refined_Control[symmetric] + simp: pt_lookup_slot_def) + done + +lemma decode_frame_invocation_authorised: + "\invs and pas_refined aag and cte_wp_at ((=) (ArchObjectCap cap)) slot + and (\s. \(cap, slot) \ set excaps. cte_wp_at ((=) cap) slot s) + and K (is_FrameCap cap \ (\(cap, slot) \ {(ArchObjectCap cap, slot)} \ set excaps. + aag_cap_auth aag (pasObjectAbs aag (fst slot)) cap \ + is_subject aag (fst slot) \ + (\v \ cap_asid' cap. is_subject_asid aag v)))\ + decode_frame_invocation label msg slot cap excaps + \\rv. authorised_arch_inv aag rv\,-" + unfolding decode_frame_invocation_def + by (wpsimp wp: decode_fr_inv_flush_authorised decode_fr_inv_map_authorised + simp: authorised_arch_inv_def authorised_page_inv_def) + +lemma decode_vspace_invocation_authorised: + "\invs and pas_refined aag and cte_wp_at ((=) (ArchObjectCap cap)) slot + and (\s. \(cap, slot) \ set excaps. cte_wp_at ((=) cap) slot s) + and K (is_PageTableCap cap \ (\(cap, slot) \ {(ArchObjectCap cap, slot)} \ set excaps. + aag_cap_auth aag (pasObjectAbs aag (fst slot)) cap \ + is_subject aag (fst slot) \ + (\v \ cap_asid' cap. is_subject_asid aag v)))\ + decode_vspace_invocation label msg slot cap excaps + \\rv. authorised_arch_inv aag rv\, -" + unfolding decode_vspace_invocation_def decode_vs_inv_flush_def authorised_arch_inv_def Let_def + by wpsimp + +lemma decode_vcpu_invocation_authorised: + "\invs and pas_refined aag and cte_wp_at ((=) (ArchObjectCap cap)) slot + and (\s. \(cap, slot) \ set excaps. cte_wp_at ((=) cap) slot s) + and K (is_VCPUCap cap \ (\(cap, slot) \ {(ArchObjectCap cap, slot)} \ set excaps. + aag_cap_auth aag (pasObjectAbs aag (fst slot)) cap \ + is_subject aag (fst slot) \ + (\v \ cap_asid' cap. is_subject_asid aag v)))\ + decode_vcpu_invocation label msg cap excaps + \\rv. authorised_arch_inv aag rv\, -" + unfolding decode_vcpu_invocation_def decode_vcpu_set_tcb_def + decode_vcpu_inject_irq_def decode_vcpu_read_register_def + decode_vcpu_write_register_def decode_vcpu_ack_vppi_def authorised_arch_inv_def + apply (rule hoare_gen_asmE) + apply (rule_tac Q'="\rv s. \x. rv = InvokeVCPU x \ authorised_vcpu_inv aag x" + in hoare_strengthen_postE_R[rotated], clarsimp) + apply wpsimp + apply (fastforce elim: caps_of_state_pasObjectAbs_eq + simp: authorised_vcpu_inv_def cte_wp_at_caps_of_state + cap_auth_conferred_def arch_cap_auth_conferred_def) + done + lemma decode_arch_invocation_authorised: "\invs and pas_refined aag and cte_wp_at ((=) (ArchObjectCap cap)) slot and (\s. \(cap, slot) \ set excaps. cte_wp_at ((=) cap) slot s) @@ -1903,7 +2471,8 @@ lemma decode_arch_invocation_authorised: \authorised_arch_inv aag\, -" unfolding arch_decode_invocation_def apply (wpsimp wp: decode_page_table_invocation_authorised decode_asid_pool_invocation_authorised - decode_asid_control_invocation_authorised decode_frame_invocation_authorised) + decode_asid_control_invocation_authorised decode_frame_invocation_authorised + decode_vcpu_invocation_authorised decode_vspace_invocation_authorised) apply auto done @@ -1920,15 +2489,16 @@ lemma set_thread_state_authorised_arch_inv[wp]: apply (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def split: arch_invocation.splits page_invocation.splits) apply (wpsimp wp: set_object_wp)+ - apply (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def - authorised_slots_def vs_lookup_slot_def obind_def - split: arch_invocation.splits page_invocation.splits if_splits option.splits) - apply (clarsimp simp: vs_lookup_table_def obind_def vspace_for_pool_def - split: option.splits if_splits) - apply (subgoal_tac "(\p. pte_of p ((pts_of s)(ref := None))) = ptes_of s") - apply fastforce - apply (fastforce simp: pte_of_def obind_def pts_of_Some aobjs_of_Some get_tcb_def - split: option.splits) + apply (clarsimp simp: authorised_arch_inv_def) + apply (case_tac i; clarsimp) + apply (clarsimp simp: authorised_page_inv_def authorised_slots_def split: page_invocation.splits) + apply (erule_tac x=level in allE) + apply (erule_tac x=asid in allE) + apply (erule_tac x=vref in allE) + apply (drule mp) + apply (fastforce elim: subst[OF vs_lookup_table_eq_lift, rotated -1] + simp: vs_lookup_slot_table get_tcb_def opt_map_def + split: option.splits kernel_object.splits if_splits)+ done end diff --git a/proof/access-control/AARCH64/ArchCNode_AC.thy b/proof/access-control/AARCH64/ArchCNode_AC.thy index 39053ab651..3bab3f2231 100644 --- a/proof/access-control/AARCH64/ArchCNode_AC.thy +++ b/proof/access-control/AARCH64/ArchCNode_AC.thy @@ -10,7 +10,7 @@ begin section\Arch-specific CNode AC.\ -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 declare arch_post_modify_registers_def[simp] declare arch_post_cap_deletion_def[simp] @@ -56,29 +56,8 @@ lemma sata_update2[CNode_AC_assms]: simp: cap_links_asid_slot_def label_owns_asid_slot_def split: if_split_asm) -lemma state_vrefs_eqI: - "\ \bot_level asid vref level p. - bot_level < level \ vs_lookup_table level asid vref s = Some (level, p) - \ (if level \ max_pt_level - then pts_of s' p = pts_of s p - else asid_pools_of s' p = asid_pools_of s p); - aobjs_of s' = aobjs_of s; asid_table s' = asid_table s; - pspace_aligned s; valid_vspace_objs s; valid_asid_table s \ - \ state_vrefs (s' :: 'a :: state_ext state) = state_vrefs (s :: 'a :: state_ext state)" - apply (rule ext) - apply safe - apply (subst (asm) state_vrefs_def, clarsimp) - apply (fastforce intro: state_vrefsD elim: subst[OF vs_lookup_table_eqI,rotated -1]) - apply (subst (asm) state_vrefs_def, clarsimp) - apply (rule state_vrefsD) - apply (subst vs_lookup_table_eqI; fastforce) - apply fastforce+ - done - lemma set_cap_state_vrefs[CNode_AC_assms, wp]: - "\pspace_aligned and valid_vspace_objs and valid_arch_state and (\s. P (state_vrefs s))\ - set_cap cap slot - \\_ s :: det_ext state. P (state_vrefs s)\" + "set_cap cap slot \\s :: det_ext state. P (state_vrefs s)\" apply (simp add: set_cap_def set_object_def) apply (wpsimp wp: get_object_wp) apply safe @@ -86,10 +65,8 @@ lemma set_cap_state_vrefs[CNode_AC_assms, wp]: by (fastforce simp: valid_arch_state_def obj_at_def opt_map_def split: option.splits kernel_object.splits)+ -crunch maskInterrupt - for underlying_memory[CNode_AC_assms, wp]: "\s. P (underlying_memory s)" - and device_state[CNode_AC_assms, wp]: "\s. P (device_state s)" - (simp: maskInterrupt_def) +declare maskInterrupt_underlying_memory_inv[CNode_AC_assms, wp] + maskInterrupt_device_state_inv[CNode_AC_assms, wp] crunch set_cdt for state_vrefs[CNode_AC_assms, wp]: "\s. P (state_vrefs s)" @@ -100,14 +77,12 @@ crunch prepare_thread_delete, arch_finalise_cap (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def) lemma state_vrefs_tcb_upd[CNode_AC_assms]: - "\ pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tcb_at t s \ - \ state_vrefs (s\kheap := (kheap s)(t \ TCB tcb)\) = state_vrefs s" + "tcb_at t s \ state_vrefs (s\kheap := (kheap s)(t \ TCB tcb)\) = state_vrefs s" apply (rule state_vrefs_eqI) by (fastforce simp: opt_map_def obj_at_def is_obj_defs valid_arch_state_def)+ lemma state_vrefs_simple_type_upd[CNode_AC_assms]: - "\ pspace_aligned s; valid_vspace_objs s; valid_arch_state s; - ko_at ko ptr s; is_simple_type ko; a_type ko = a_type (f val) \ + "\ ko_at ko ptr s; is_simple_type ko; a_type ko = a_type (f val) \ \ state_vrefs (s\kheap := (kheap s)(ptr \ f val)\) = state_vrefs s" apply (case_tac ko; case_tac "f val"; clarsimp) by (fastforce intro!: state_vrefs_eqI simp: opt_map_def obj_at_def is_obj_defs valid_arch_state_def)+ @@ -158,7 +133,7 @@ proof goal_cases qed -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 lemma integrity_asids_set_cap_Nullcap[CNode_AC_assms]: "\(=) s\ set_cap NullCap slot \\_. integrity_asids aag subjects x a s\" @@ -185,7 +160,7 @@ proof goal_cases qed -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 lemma arch_post_cap_deletion_pas_refined[CNode_AC_assms, wp]: "arch_post_cap_deletion irqopt \pas_refined aag\" @@ -223,7 +198,7 @@ proof goal_cases qed -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 lemma arch_derive_cap_auth_derived[CNode_AC_assms]: "\\s. cte_wp_at (auth_derived (ArchObjectCap cap)) src_slot s\ @@ -327,7 +302,7 @@ global_interpretation CNode_AC_4?: CNode_AC_4 proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; (fact CNode_AC_assms)?) + by (unfold_locales; fact CNode_AC_assms) qed diff --git a/proof/access-control/AARCH64/ArchDomainSepInv.thy b/proof/access-control/AARCH64/ArchDomainSepInv.thy index 6d295b84e4..75be93b3ce 100644 --- a/proof/access-control/AARCH64/ArchDomainSepInv.thy +++ b/proof/access-control/AARCH64/ArchDomainSepInv.thy @@ -9,14 +9,26 @@ imports "DomainSepInv" begin -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 named_theorems DomainSepInv_assms -crunch arch_post_cap_deletion, set_pt, set_asid_pool, prepare_thread_delete, init_arch_objects +crunch arch_post_cap_deletion, set_pt, set_asid_pool, init_arch_objects for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st" (wp: domain_sep_inv_triv crunch_wps set_asid_pool_cte_wp_at set_pt_cte_wp_at) +crunch vcpu_update + for domain_sep_inv[wp]: "domain_sep_inv irqs st" + (wp: domain_sep_inv_triv crunch_wps set_asid_pool_cte_wp_at set_pt_cte_wp_at) + +crunch vcpu_save_reg, vcpu_invalidate_active, dissociate_vcpu_tcb, fpu_thread_delete + for interrupt_states[wp]: "\s. P (interrupt_states s)" + (wp: crunch_wps) + +crunch prepare_thread_delete + for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st" + (wp: domain_sep_inv_triv crunch_wps) + crunch arch_finalise_cap for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st" (wp: crunch_wps simp: crunch_simps) @@ -25,6 +37,22 @@ lemma arch_finalise_cap_rv[DomainSepInv_assms]: "\\_. P (NullCap,NullCap)\ arch_finalise_cap c x \\rv _. P rv\" unfolding arch_finalise_cap_def by wpsimp +lemma arch_derive_cap_domain_sep_inv[DomainSepInv_assms, wp]: + "\\\ arch_derive_cap acap \\rv _. domain_sep_inv_cap irqs rv\,-" + unfolding arch_derive_cap_def + by wpsimp + +lemma arch_post_modify_registers_domain_sep_inv[DomainSepInv_assms, wp]: + "arch_post_modify_registers cur t \domain_sep_inv irqs st\" + unfolding arch_post_modify_registers_def by wpsimp + +crunch handle_vm_fault, handle_vm_fault, perform_pg_inv_unmap, + perform_pg_inv_get_addr, perform_pt_inv_map, perform_pt_inv_unmap, + handle_arch_fault_reply, arch_mask_irq_signal, arch_switch_to_thread, + arch_switch_to_idle_thread, arch_activate_idle_thread, store_asid_pool_entry + for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st" + (wp: crunch_wps) + end @@ -32,28 +60,22 @@ global_interpretation DomainSepInv_1?: DomainSepInv_1 proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; (fact DomainSepInv_assms | wp init_arch_objects_inv)) + by (unfold_locales; (fact DomainSepInv_assms)?) qed +context Arch begin global_naming AARCH64 -context Arch begin global_naming RISCV64 - -crunch - handle_reserved_irq, handle_vm_fault, perform_pg_inv_map, perform_pg_inv_unmap, - perform_pg_inv_get_addr, perform_pt_inv_map, perform_pt_inv_unmap, - handle_hypervisor_fault, handle_arch_fault_reply, arch_mask_irq_signal, - arch_switch_to_thread, arch_switch_to_idle_thread, arch_activate_idle_thread, - store_asid_pool_entry, copy_global_mappings - for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st" - (wp: crunch_wps) +crunch perform_pg_inv_map, perform_flush + for domain_sep_inv[wp]: "domain_sep_inv irqs st" + (wp: crunch_wps simp: crunch_simps) lemma perform_page_invocation_domain_sep_inv: "\domain_sep_inv irqs st and valid_page_inv pgi\ perform_page_invocation pgi - \\_. domain_sep_inv irqs st\" + \\_ (s :: det_ext state). domain_sep_inv irqs st s\" apply (rule hoare_pre) apply (wp mapM_wp[OF _ subset_refl] set_cap_domain_sep_inv mapM_x_wp[OF _ subset_refl] - perform_page_invocation_domain_sep_inv_get_cap_helper hoare_weak_lift_imp + perform_page_invocation_domain_sep_inv_get_cap_helper | simp add: perform_page_invocation_def o_def | wpc)+ done @@ -73,7 +95,7 @@ lemma perform_asid_control_invocation_domain_sep_inv: unfolding perform_asid_control_invocation_def apply (rule hoare_pre) apply (wp modify_wp cap_insert_domain_sep_inv' set_cap_domain_sep_inv - get_cap_domain_sep_inv_cap[where st=st] hoare_weak_lift_imp + get_cap_domain_sep_inv_cap[where st=st] hoare_vcg_imp_lift | wpc | simp )+ done @@ -84,10 +106,27 @@ lemma perform_asid_pool_invocation_domain_sep_inv: apply (wp set_cap_domain_sep_inv get_cap_wp | wpc | simp)+ done +lemma perform_vspace_invocation_domain_sep_inv[wp]: + "perform_vspace_invocation iv \domain_sep_inv irqs st\" + by (wpsimp simp: perform_vspace_invocation_def) + +crunch invoke_vcpu_inject_irq, invoke_vcpu_read_register, invoke_vcpu_write_register, invoke_vcpu_ack_vppi + for domain_sep_inv[wp]: "domain_sep_inv irqs st" + +lemma associate_vcpu_tcb_domain_sep_inv[wp]: + "associate_vcpu_tcb a b \domain_sep_inv irqs st\" + unfolding associate_vcpu_tcb_def + by (wpsimp | wp domain_sep_inv_triv)+ + +lemma perform_vcpu_invocation_domain_sep_inv[wp]: + "perform_vcpu_invocation vcpu \domain_sep_inv irqs st\" + unfolding perform_vcpu_invocation_def + by wpsimp + lemma arch_perform_invocation_domain_sep_inv[DomainSepInv_assms]: "\domain_sep_inv irqs st and valid_arch_inv ai\ arch_perform_invocation ai - \\_. domain_sep_inv irqs st\" + \\_ (s :: det_ext state). domain_sep_inv irqs st s\" unfolding arch_perform_invocation_def apply (wpsimp wp: perform_page_table_invocation_domain_sep_inv perform_page_invocation_domain_sep_inv @@ -112,14 +151,14 @@ lemma arch_invoke_irq_control_domain_sep_inv[DomainSepInv_assms]: apply (wpsimp wp: do_machine_op_domain_sep_inv simp: arch_irq_control_inv_valid_def)+ done -lemma arch_derive_cap_domain_sep_inv[DomainSepInv_assms, wp]: - "\\\ arch_derive_cap acap \\rv _. domain_sep_inv_cap irqs rv\,-" - unfolding arch_derive_cap_def - by wpsimp +crunch handle_reserved_irq, handle_hypervisor_fault + for domain_sep_inv[wp]: + "\s :: det_ext state. domain_sep_inv irqs (st :: 's :: state_ext state) s" + (wp: crunch_wps simp: crunch_simps vcpu_update_def valid_vcpu_def valid_fault_def) -lemma arch_post_modify_registers_domain_sep_inv[DomainSepInv_assms, wp]: - "arch_post_modify_registers cur t \domain_sep_inv irqs st\" - unfolding arch_post_modify_registers_def by wpsimp +\ \Remove the parentheses\ +declare handle_reserved_irq_domain_sep_inv[simplified and_assoc, DomainSepInv_assms] +declare handle_hypervisor_fault_domain_sep_inv[simplified and_assoc, DomainSepInv_assms] end diff --git a/proof/access-control/AARCH64/ArchFinalise_AC.thy b/proof/access-control/AARCH64/ArchFinalise_AC.thy index c523ccf513..b852399327 100644 --- a/proof/access-control/AARCH64/ArchFinalise_AC.thy +++ b/proof/access-control/AARCH64/ArchFinalise_AC.thy @@ -8,12 +8,12 @@ theory ArchFinalise_AC imports Finalise_AC begin -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 named_theorems Finalise_AC_assms lemma state_vrefs_clear_asid_table: - "state_vrefs (s\arch_state := arch_state s\riscv_asid_table := \a. if a = asid_high_bits_of base + "state_vrefs (s\arch_state := arch_state s\arm_asid_table := \a. if a = asid_high_bits_of base then None else asid_table s a\\) x \ state_vrefs s x" @@ -22,82 +22,160 @@ lemma state_vrefs_clear_asid_table: lemma state_vrefs_clear_asid_pool: assumes "asid_table s (asid_high_bits_of asid) = Some pool_ptr" and "ako_at (ASIDPool pool) pool_ptr s" - shows "state_vrefs (s\kheap := \a. if a = pool_ptr - then Some (ArchObj (ASIDPool (\a. if a = asid_low_bits_of asid - then None - else pool a))) - else kheap s a\) x - \ state_vrefs s x" + shows "state_vrefs (s\kheap := (kheap s)(pool_ptr \ ArchObj + (ASIDPool (\a. if a = asid_low_bits_of asid then None else pool a)))\) x + \ state_vrefs s x" + apply (rule state_vrefs_subseteq) + using assms + by (auto simp: vspace_for_pool_def entry_for_pool_def opt_map_def obind_def obj_at_def) + +lemma pas_refined_arm_next_vmid[simp]: + "pas_refined aag (s\arch_state := arch_state s\arm_next_vmid := v\\) = pas_refined aag s" + by (auto simp: pas_refined_def state_objs_to_policy_def state_vrefs_def) + +lemma pas_refined_arm_vmid_table[simp]: + "pas_refined aag (s\arch_state := arch_state s\arm_vmid_table := v\\) = pas_refined aag s" + by (auto simp: pas_refined_def state_objs_to_policy_def state_vrefs_def) + +crunch invalidate_vmid_entry + for pas_refined[wp]: "pas_refined aag" + +lemma set_vcpu_state_vrefs[wp]: + "set_vcpu ptr vcpu \\s. P (state_vrefs s)\" + apply (wpsimp wp: set_vcpu_wp) + apply (erule_tac P=P in rsubst) + apply (fastforce intro: state_vrefs_eqI simp: opt_map_def typ_at_eq_kheap_obj) + done + +lemma state_vrefs_set_asid_pool_vmid: + assumes "pool_for_asid asid s = Some pool_ptr" + and "asid_pools_of s pool_ptr = Some pool" + and "pool (asid_low_bits_of asid) = Some entry" + shows "state_vrefs + (s\kheap := (kheap s) + (pool_ptr \ + ArchObj + (ASIDPool + (\a. if a = asid_low_bits_of asid + then Some (ASIDPoolVSpace vmid (ap_vspace entry)) else pool a)))\) + x + \ state_vrefs s x" (is "state_vrefs ?s' _ \ state_vrefs _ _") + apply (rule state_vrefs_subseteq) using assms - apply - - apply (clarsimp simp: state_vrefs_def) - apply (rule exI, rule conjI) - apply (rule_tac x=lvl in exI) - apply (rule_tac x="if x = pool_ptr then ASIDPool pool else ao" in exI) - apply (rule conjI, rule refl) - apply (rule_tac x=bot in exI) - apply (rule_tac x=asida in exI) - apply (rule_tac x=vref in exI) - apply (prop_tac "ptes_of ?s' = ptes_of s") - apply (fastforce simp: obj_at_def all_ext ptes_of_def obind_def opt_map_def) - apply (fastforce simp: vs_lookup_table_def vspace_for_pool_def obj_at_def obind_def opt_map_def - split: option.split_asm if_split_asm) - apply (fastforce simp: vs_refs_aux_def graph_of_def opt_map_def split: if_splits) + by (auto simp: vspace_for_pool_def entry_for_pool_def opt_map_def obind_def obj_at_def + split: option.splits) + +lemma update_asid_pool_entry_vmid_pas_refined[wp]: + "update_asid_pool_entry (\entry. Some (ASIDPoolVSpace vmid (ap_vspace entry))) asid \pas_refined aag\" + unfolding update_asid_pool_entry_def set_asid_pool_def + apply (wpsimp wp: set_object_wp)+ + apply (erule pas_refined_subseteq; clarsimp?) + apply (rule caps_of_state_fun_upd) + apply (clarsimp simp: obj_at_def opt_map_def split: option.splits) + apply (erule rev_subsetD, rule state_vrefs_subseteq) + apply (auto simp: vspace_for_pool_def entry_for_pool_def opt_map_def obind_def + split: option.splits kernel_object.splits)[4] + apply (rule thread_st_auth_fun_upd) + apply (clarsimp simp: obj_at_def asid_pools_of_ko_at get_tcb_def) + apply (rule thread_bound_ntfns_fun_upd) + apply (clarsimp simp: asid_pools_of_ko_at get_tcb_def obj_at_def) + done + +lemma tcb_vcpu_update_pas_refined[wp]: + "arch_thread_set v t \pas_refined aag\" + apply (wpsimp wp: arch_thread_set_wp) + apply (erule pas_refined_subseteq; clarsimp?) + apply (rule caps_of_state_fun_upd) + apply (clarsimp simp: obj_at_def get_tcb_def tcb_cap_cases_def + split: option.splits kernel_object.splits) + apply (erule rev_subsetD, rule state_vrefs_subseteq) + apply (auto simp: vspace_for_pool_def entry_for_pool_def opt_map_def obind_def get_tcb_def + split: option.splits kernel_object.splits)[4] + apply (rule thread_st_auth_fun_upd) + apply (clarsimp simp: obj_at_def asid_pools_of_ko_at get_tcb_def) + apply (rule thread_bound_ntfns_fun_upd) + apply (clarsimp simp: obj_at_def asid_pools_of_ko_at get_tcb_def) done -crunch set_vm_root for pas_refined[wp]: "pas_refined aag" +lemma set_vcpu_pas_refined[wp]: + "set_vcpu ptr vcpu \\s. pas_refined aag s\" + apply (wpsimp wp: set_vcpu_wp) + apply (erule pas_refined_subseteq; clarsimp?) + apply (fastforce simp: caps_of_state_fun_upd obj_at_def) + apply (erule rev_subsetD, rule state_vrefs_subseteq) + apply (auto simp: vspace_for_pool_def entry_for_pool_def opt_map_def obind_def obj_at_def)[4] + apply (fastforce simp: thread_st_auth_fun_upd obj_at_def asid_pools_of_ko_at get_tcb_def) + apply (fastforce simp: thread_bound_ntfns_fun_upd obj_at_def asid_pools_of_ko_at get_tcb_def) + done + +lemma vcpu_update_pas_refined: + "vcpu_update vr f \\s. pas_refined aag s\" + unfolding vcpu_update_def + by (wpsimp wp: get_vcpu_wp) + +crunch set_vm_root, invalidate_asid_entry + for pas_refined[wp]: "pas_refined aag" + (wp: crunch_wps ignore: update_asid_pool_entry) lemma delete_asid_pool_pas_refined[wp]: "delete_asid_pool base ptr \pas_refined aag\" - unfolding delete_asid_pool_def - apply wpsimp - apply (clarsimp simp: pas_refined_def state_objs_to_policy_def) - apply (rule conjI; clarsimp) - apply (erule subsetD) - apply (clarsimp simp: auth_graph_map_def) - apply (rule exI, rule conjI, rule refl)+ - apply (erule state_bits_to_policy_vrefs_subseteq; fastforce?) - apply (clarsimp simp: allI state_vrefs_clear_asid_table) - apply (erule subsetD, erule state_asids_to_policy_vrefs_subseteq) - apply clarsimp - apply (clarsimp simp: allI state_vrefs_clear_asid_table) - apply clarsimp + apply (wpsimp simp: delete_asid_pool_def) + apply (rule_tac Q'="\_ s. pas_refined aag s \ asid_low_bits_of base = 0 \ + arm_asid_table (arch_state s) = asid_table \ asid_pool_at ptr s" + in hoare_strengthen_post[rotated], clarsimp) + apply (erule pas_refined_subseteq; clarsimp?) + apply (erule rev_subsetD, rule state_vrefs_subseteq) + apply (auto simp: pool_for_asid_def)[4] + apply (wpsimp wp: mapM_wp')+ + apply (clarsimp simp: asid_pools_at_eq) done lemma delete_asid_pas_refined[wp]: "delete_asid asid pt \pas_refined aag\" - unfolding delete_asid_def - apply (rule bind_wp) - apply (wpsimp simp: set_asid_pool_def wp: set_object_wp hoare_vcg_imp_lift' hoare_vcg_all_lift) - apply (rule_tac Q'="\_ s. riscv_asid_table (arch_state s) = asid_table \ - ako_at (ASIDPool pool) x2 s \ pas_refined aag s" - in hoare_strengthen_post[rotated]) - defer - apply wpsimp+ - apply (clarsimp simp: pas_refined_def) - apply (intro conjI) - apply (clarsimp simp: state_objs_to_policy_def) - apply (subst (asm) caps_of_state_fun_upd[simplified fun_upd_def]) - apply (clarsimp simp: obj_at_def) - apply (erule subsetD) - apply (clarsimp simp: auth_graph_map_def) - apply (rule exI, rule conjI, rule refl)+ - apply (erule state_bits_to_policy_vrefs_subseteq) - apply clarsimp - apply (clarsimp simp: all_ext thread_st_auth_def tcb_states_of_state_def get_tcb_def obj_at_def) - apply (clarsimp simp: all_ext thread_bound_ntfns_def get_tcb_def obj_at_def) - apply clarsimp - apply (rule allI[OF state_vrefs_clear_asid_pool]; simp) - apply clarsimp - apply (erule subsetD, erule state_asids_to_policy_vrefs_subseteq) - apply (fastforce simp: obj_at_def caps_of_state_fun_upd[simplified fun_upd_def]) - apply (rule allI[OF state_vrefs_clear_asid_pool]; fastforce) - apply fastforce - apply (fastforce simp: obj_at_def caps_of_state_fun_upd[simplified fun_upd_def]) + apply (wpsimp wp: set_object_wp simp: delete_asid_def set_asid_pool_def simp_del: fun_upd_apply) + apply (rule_tac Q'="\_ s. pas_refined aag s \ pool_for_asid asid s = Some x2 \ asid_pool_at x2 s" + in hoare_strengthen_post[rotated]) + apply (clarsimp simp: asid_pools_at_eq) + apply (erule pas_refined_subseteq; clarsimp?) + apply (rule caps_of_state_fun_upd) + apply (clarsimp simp: obj_at_def opt_map_def split: option.splits) + apply (erule rev_subsetD, rule state_vrefs_subseteq) + apply (auto simp: vspace_for_pool_def entry_for_pool_def opt_map_def obind_def + split: option.splits)[4] + apply (rule thread_st_auth_fun_upd) + apply (clarsimp simp: obj_at_def get_tcb_def opt_map_def split: option.splits) + apply (rule thread_bound_ntfns_fun_upd) + apply (clarsimp simp: obj_at_def get_tcb_def opt_map_def split: option.splits) + apply wpsimp+ + apply (clarsimp simp: asid_pools_at_eq) done -lemma arch_finalise_cap_pas_refined[wp]: +lemma state_vrefs_set_current_vcpu[simp]: + "state_vrefs (s\arch_state := arch_state s\arm_current_vcpu := vcpu\\) + = state_vrefs s" + by (fastforce simp: state_vrefs_def dest: vs_lookup_clear_asid_table[simplified fun_upd_def]) + +lemma pas_refined_arm_current_vcpu_upd[simp]: + "pas_refined aag (s\arch_state := arch_state s\arm_current_vcpu := v\\) + = pas_refined aag s" + by (fastforce elim: pas_refined_by_subsets simp: state_objs_to_policy_def) + +crunch vcpu_invalidate_active + for pas_refined[wp]: "pas_refined aag" + (wp: crunch_wps simp: crunch_simps) + +lemma dissociate_vcpu_tcb_pas_refined[wp]: + "dissociate_vcpu_tcb vr t \pas_refined aag\" + unfolding dissociate_vcpu_tcb_def + by (wpsimp wp: get_vcpu_wp arch_thread_get_wp) + +lemma vcpu_finalise_cap_pas_refined[wp]: + "vcpu_finalise vr \pas_refined aag\" + unfolding vcpu_finalise_def + by (wpsimp wp: get_vcpu_wp) + +lemma arch_finalise_cap_pas_refined[Finalise_AC_assms, wp]: "\pas_refined aag and invs and valid_arch_cap c\ arch_finalise_cap c x \\_. pas_refined aag\" unfolding arch_finalise_cap_def apply (wpsimp wp: unmap_page_pas_refined unmap_page_table_pas_refined) @@ -105,19 +183,22 @@ lemma arch_finalise_cap_pas_refined[wp]: done crunch prepare_thread_delete - for pas_refined[wp]: "pas_refined aag" + for pas_refined[Finalise_AC_assms, wp]: "pas_refined aag" -crunch prepare_thread_delete - for respects[Finalise_AC_assms, wp]: "integrity aag X st" +lemma prepare_thread_delete_integrity[Finalise_AC_assms, wp]: + "\integrity aag X st and K (is_subject aag t)\ prepare_thread_delete t \\_. integrity aag X st\" + unfolding prepare_thread_delete_def + apply (wpsimp wp: dissociate_vcpu_tcb_respects arch_thread_get_wp + dmo_no_mem_respects hoare_vcg_all_lift hoare_vcg_imp_lift + simp: fpu_thread_delete_def) + using associated_vcpu_is_subject get_tcb_Some_ko_at by blast lemma sbn_st_vrefs[Finalise_AC_assms]: - "\(\s. P (state_vrefs s)) and pspace_aligned and valid_vspace_objs and valid_arch_state\ - set_bound_notification t st - \\_ s. P (state_vrefs s)\" + "set_bound_notification t st \\s. P (state_vrefs s)\" apply (simp add: set_bound_notification_def) apply (wpsimp wp: set_object_wp dxo_wp_weak) apply (subst state_vrefs_tcb_upd) - apply (auto simp: tcb_at_def) + apply (auto simp: tcb_at_def valid_arch_state_def) done lemma arch_finalise_cap_auth'[Finalise_AC_assms]: @@ -141,10 +222,43 @@ lemma arch_cap_cleanup_wf[Finalise_AC_assms]: \ (\irq. arch_cap_cleanup_opt acap = IRQHandlerCap irq \ is_subject_irq aag irq)" by simp -lemma set_vm_root_integrity[wp]: - "set_vm_root param_a \integrity aag X st\ " - unfolding set_vm_root_def - by (wpsimp wp: dmo_wp mol_respects get_cap_wp simp: setVSpaceRoot_def) +lemma update_asid_pool_entry_vmid_integrity: + "\\s. integrity aag X st s \ (vmid = None \ vmid_for_asid s asid = None)\ + update_asid_pool_entry (\entry. Some (ASIDPoolVSpace vmid (ap_vspace entry))) asid + \\_. integrity aag X st\" + unfolding update_asid_pool_entry_def set_asid_pool_def + apply (wpsimp wp: set_object_wp simp_del: fun_upd_apply) + apply (clarsimp simp: integrity_def) + apply (subst tcb_states_of_state_fun_upd, fastforce simp: get_tcb_def asid_pools_of_ko_at obj_at_def)+ + apply (intro conjI; clarsimp?) + apply (erule_tac allE, erule tro_trans_spec) + apply (force intro!: tro_arch arch_troa_asidpool_vmid + simp: asid_pools_of_ko_at vmid_for_asid_def entry_for_pool_def pool_for_asid_def + obj_at_def obind_def opt_map_def + split: option.splits if_splits) + apply (erule_tac x=asid in allE, auto simp: pool_for_asid_def) + done + +lemma store_vmid_Some_integrity: + "\\s. integrity aag X st s \ vmid_for_asid s asid = None\ + store_vmid asid vmid + \\_. integrity aag X st\" + unfolding store_vmid_def + by (wpsimp wp: update_asid_pool_entry_vmid_integrity) + +crunch find_free_vmid + for respects[wp]: "integrity aag X st" + (wp: update_asid_pool_entry_vmid_integrity dmo_no_mem_respects ignore: update_asid_pool_entry) + +lemma get_vmid_respects[wp]: + "get_vmid asid \integrity aag X st\" + unfolding get_vmid_def + by (wpsimp wp: store_vmid_Some_integrity) + +crunch arm_context_switch, set_global_user_vspace, set_vm_root, + invalidate_vmid_entry, invalidate_asid_entry, invalidate_tlb_by_asid + for respects[wp]: "integrity aag X st" + (wp: dmo_no_mem_respects ignore: update_asid_pool_entry) lemma delete_asid_pool_respects[wp]: "\integrity aag X st and @@ -152,87 +266,88 @@ lemma delete_asid_pool_respects[wp]: \ is_subject_asid aag asid')\ delete_asid_pool x y \\_. integrity aag X st\" - unfolding delete_asid_pool_def - by (wpsimp wp: mapM_wp[OF _ subset_refl] simp: integrity_asid_table_entry_update' integrity_def) - -crunch set_vm_root - for integrity_obj[wp]: "integrity_obj_state aag activate subjects st" - and cdt[wp]: "\s. P (cdt s)" - and is_original_cap[wp]: "\s. P (is_original_cap s x)" - and interrupt_irq_node[wp]: "\s. P (interrupt_states s x)" - and underlying_memory[wp]: "\s. P (underlying_memory (machine_state s) x)" - and device_state[wp]: "\s. P (device_state (machine_state s) x)" - and tcb_states_of_state[wp]: "\s. P (tcb_states_of_state s)" - (wp: dmo_wp) + by (wpsimp simp: delete_asid_pool_def wp: asid_table_entry_update_integrity mapM_wp') crunch set_asid_pool for is_original_cap[wp]: "\s. P (is_original_cap s x)" - and cdt_list[wp]: "\s. P (cdt_list s x)" - and ready_queues[wp]: "\s. P (ready_queues s x y)" - and machine_state[wp]: "\s. P (machine_state s)" lemma set_asid_pool_tcb_states_of_state[wp]: "set_asid_pool p pool \\s. P (tcb_states_of_state s)\" - apply (wpsimp wp: set_object_wp_strong simp: obj_at_def set_asid_pool_def) - apply (prop_tac "\x. get_tcb x (s\kheap := (kheap s)(p \ ArchObj (ASIDPool pool))\) = get_tcb x s") - apply (auto simp: tcb_states_of_state_def get_tcb_def) - done - -lemma delete_asid_integrity_asids: - "\\s. pas_refined aag s \ invs s \ is_subject aag pt \ - (\x a. integrity_asids aag {pasSubject aag} x a st s)\ - delete_asid asid pt - \\_ s. integrity_asids aag {pasSubject aag} x a st s\" - unfolding integrity_def - apply (wpsimp wp: dmo_wp mol_respects set_object_wp hoare_vcg_all_lift hoare_vcg_imp_lift - simp: delete_asid_def hwASIDFlush_def set_asid_pool_def) - apply (intro conjI impI allI; clarsimp) - apply fastforce - apply (clarsimp simp: opt_map_def) - apply (erule_tac x=asid in allE, fastforce) + apply (wpsimp wp: set_object_wp_strong simp: obj_at_def set_asid_pool_def) + apply (erule_tac P=P in rsubst) + apply (fastforce simp: tcb_states_of_state_def get_tcb_def split: kernel_object.splits) done -lemma set_asid_pool_respects_clear: +lemma set_asid_pool_integrity_objs: "\integrity_obj_state aag activate subjects st and (\s. \pool'. ako_at (ASIDPool pool') ptr s \ asid_pool_integrity subjects aag pool' pool)\ set_asid_pool ptr pool \\_. integrity_obj_state aag activate subjects st\" apply (wpsimp wp: set_object_wp_strong simp: obj_at_def set_asid_pool_def) - using arch_troa_asidpool_clear tro_arch tro_trans_spec by fastforce + by (fastforce elim: tro_trans_spec + intro: tro_arch arch_troa_asidpool_clear + simp: a_type_def aa_type_def + split: if_splits kernel_object.splits arch_kernel_obj.splits) + +lemma set_asid_pool_integrity_autarch: + "\\s. integrity aag X st s \ pas_refined aag s \ invs s \ + (\asid pool. pool_for_asid asid s = Some pool_ptr \ asid_pools_of s pool_ptr = Some pool \ + pool' = pool (asid_low_bits_of asid := None) \ + (\entry. pool (asid_low_bits_of asid) = Some entry + \ is_subject aag (ap_vspace entry)))\ + set_asid_pool pool_ptr pool' + \\_. integrity aag X st\" + unfolding integrity_def conj_assoc[symmetric] + apply (wp set_object_wp_strong set_asid_pool_integrity_objs dmo_wp hoare_vcg_all_lift + | wps | simp add: obj_at_def set_asid_pool_def)+ + apply (intro conjI impI; clarsimp) + apply (fastforce simp: opt_map_def asid_pool_integrity_def aag_has_Control_iff_owns) + apply (erule_tac x=pool_ptr in allE)+ + apply (erule_tac x=asid in allE)+ + apply (fastforce simp: asid_pools_of_ko_at obj_at_def pool_for_asid_def) + done lemma delete_asid_respects: - "\integrity aag X st and pas_refined aag and invs and K (is_subject aag pd)\ + "\integrity aag X st and pas_refined aag and invs and K (0 < asid \ is_subject aag pd)\ delete_asid asid pd \\_. integrity aag X st\" - unfolding integrity_def - supply integrity_asids_def[simp del] - apply (rule hoare_pre) - apply (simp only: conj_assoc[symmetric]) - apply (rule hoare_vcg_conj_lift) - apply (simp add: delete_asid_def) - apply (wp | wpc | wps)+ - apply (wpsimp wp: set_asid_pool_respects_clear dmo_wp - delete_asid_integrity_asids hoare_vcg_all_lift)+ - apply (clarsimp simp: pas_refined_refl obj_at_def asid_pool_integrity_def) + apply (simp add: delete_asid_def) + apply (wpsimp wp: set_asid_pool_integrity_autarch) + apply (rule_tac Q'="\_ s. integrity aag X st s \ pas_refined aag s \ invs s \ + is_subject aag pd \ pool_for_asid asid s = Some x2 \ + vspace_for_asid asid s = Some pd" in hoare_strengthen_post[rotated]) + apply (fastforce simp: vspace_for_asid_def obind_def entry_for_asid_def entry_for_pool_def + split: if_splits) + apply (wpsimp wp: set_asid_pool_integrity_autarch invalidate_tlb_by_asid_invs)+ + apply (clarsimp simp: vspace_for_asid_def entry_for_asid_def entry_for_pool_def in_obind_eq) done -lemma arch_finalise_cap_respects[wp]: +lemma vcpu_finalise_integrity_autarch: + "\integrity aag X st and K (is_subject aag vr)\ + vcpu_finalise vr + \\_. integrity aag X st\" + unfolding vcpu_finalise_def + apply (wpsimp wp: dissociate_vcpu_tcb_respects get_vcpu_wp) + apply (erule (2) associated_tcb_is_subject) + done + +lemma arch_finalise_cap_respects[Finalise_AC_assms, wp]: "\integrity aag X st and invs and pas_refined aag and valid_cap (ArchObjectCap cap) and K (pas_cap_cur_auth aag (ArchObjectCap cap))\ arch_finalise_cap cap final \\_. integrity aag X st\" apply (simp add: arch_finalise_cap_def) - apply (wpsimp wp: unmap_page_respects unmap_page_table_respects delete_asid_respects) + apply (wpsimp wp: unmap_page_respects unmap_page_table_respects + delete_asid_respects delete_asid_pool_respects vcpu_finalise_integrity_autarch) apply (auto simp: cap_auth_conferred_def arch_cap_auth_conferred_def wellformed_mapdata_def aag_cap_auth_def pas_refined_all_auth_is_owns valid_cap_simps cap_links_asid_slot_def label_owns_asid_slot_def intro: pas_refined_Control_into_is_subject_asid) done -crunch arch_post_cap_deletion - for pspace_aligned[Finalise_AC_assms, wp]: "\s :: det_ext state. pspace_aligned s" - and valid_vspace_objs[Finalise_AC_assms, wp]: "\s :: det_ext state. valid_vspace_objs s" - and valid_arch_state[Finalise_AC_assms, wp]: "\s :: det_ext state. valid_arch_state s" +declare prepare_thread_delete_st_tcb_at_halted[Finalise_AC_assms] +declare finalise_cap_valid_list[Finalise_AC_assms] +declare finalise_cap_replaceable[Finalise_AC_assms] end @@ -241,11 +356,11 @@ global_interpretation Finalise_AC_1?: Finalise_AC_1 proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; (fact Finalise_AC_assms | wp finalise_cap_replaceable)) + by (unfold_locales; fact Finalise_AC_assms) qed -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 lemma cap_revoke_respects'[Finalise_AC_assms]: "s \ \(\s. trp \ integrity aag X st s) and K (is_subject aag (fst slot)) diff --git a/proof/access-control/AARCH64/ArchInterrupt_AC.thy b/proof/access-control/AARCH64/ArchInterrupt_AC.thy index 09ff7a783c..6adcccd797 100644 --- a/proof/access-control/AARCH64/ArchInterrupt_AC.thy +++ b/proof/access-control/AARCH64/ArchInterrupt_AC.thy @@ -9,20 +9,19 @@ imports Interrupt_AC begin -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 named_theorems Interrupt_AC_assms definition arch_authorised_irq_ctl_inv :: "'a PAS \ Invocations_A.arch_irq_control_invocation \ bool" where "arch_authorised_irq_ctl_inv aag cinv \ - case cinv of (RISCVIRQControlInvocation irq x1 x2 trigger) \ + case cinv of (ARMIRQControlInvocation irq x1 x2 trigger) \ is_subject aag (fst x1) \ is_subject aag (fst x2) \ (pasSubject aag, Control, pasIRQAbs aag irq) \ pasPolicy aag" lemma arch_invoke_irq_control_pas_refined[Interrupt_AC_assms]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv + "\pas_refined aag and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv and K (arch_authorised_irq_ctl_inv aag irq_ctl_inv)\ arch_invoke_irq_control irq_ctl_inv \\_. pas_refined aag\" @@ -75,11 +74,11 @@ global_interpretation Interrupt_AC_1?: Interrupt_AC_1 "arch_authorised_irq_ctl_i proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; (fact Interrupt_AC_assms)?) + by (unfold_locales; (fact Interrupt_AC_assms | wp)?) qed -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 lemma arch_decode_irq_control_invocation_authorised[Interrupt_AC_assms]: "\pas_refined aag and @@ -105,7 +104,7 @@ global_interpretation Interrupt_AC_2?: Interrupt_AC_2 "arch_authorised_irq_ctl_i proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; (fact Interrupt_AC_assms)?) + by (unfold_locales; fact Interrupt_AC_assms) qed diff --git a/proof/access-control/AARCH64/ArchIpc_AC.thy b/proof/access-control/AARCH64/ArchIpc_AC.thy index 7be518e246..575161da53 100644 --- a/proof/access-control/AARCH64/ArchIpc_AC.thy +++ b/proof/access-control/AARCH64/ArchIpc_AC.thy @@ -8,7 +8,7 @@ theory ArchIpc_AC imports Ipc_AC begin -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 named_theorems Ipc_AC_assms @@ -77,7 +77,7 @@ proof goal_cases qed -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 lemma store_word_offs_respects_in_ipc[Ipc_AC_assms]: "\integrity_tcb_in_ipc aag X receiver epptr TRContext st and @@ -184,11 +184,6 @@ lemma auth_ipc_buffers_machine_state_update[Ipc_AC_assms, simp]: "auth_ipc_buffers (machine_state_update f s) = auth_ipc_buffers s" by (clarsimp simp: auth_ipc_buffers_def get_tcb_def) -crunch handle_arch_fault_reply - for pspace_aligned[Ipc_AC_assms, wp]: "\s :: det_ext state. pspace_aligned s" - and valid_vspace_objs[Ipc_AC_assms, wp]: "\s :: det_ext state. valid_vspace_objs s" - and valid_arch_state[Ipc_AC_assms, wp]: "\s :: det_ext state. valid_arch_state s" - lemma cap_insert_ext_integrity_asids_in_ipc[Ipc_AC_assms, wp]: "cap_insert_ext src_parent src_slot dest_slot src_p dest_p \\s. integrity_asids aag subjects x asid st @@ -232,7 +227,7 @@ global_interpretation Ipc_AC_2?: Ipc_AC_2 proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; (fact Ipc_AC_assms)?) + by (unfold_locales; fact Ipc_AC_assms) qed end diff --git a/proof/access-control/AARCH64/ArchRetype_AC.thy b/proof/access-control/AARCH64/ArchRetype_AC.thy index 93b34a9022..c0845be336 100644 --- a/proof/access-control/AARCH64/ArchRetype_AC.thy +++ b/proof/access-control/AARCH64/ArchRetype_AC.thy @@ -82,7 +82,7 @@ lemma pas_refined: end -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 named_theorems Retype_AC_assms @@ -97,7 +97,7 @@ lemma pts_of_detype[simp]: by (simp add: in_omonad detype_def) lemma ptes_of_detype_Some[simp]: - "(ptes_of (detype S s) p = Some pte) = (table_base p \ S \ ptes_of s p = Some pte)" + "(ptes_of (detype S s) pt_t p = Some pte) = (table_base pt_t p \ S \ ptes_of s pt_t p = Some pte)" by (simp add: in_omonad ptes_of_def detype_def) lemma asid_pools_of_detype: @@ -115,14 +115,14 @@ lemma pool_for_asid_detype_Some[simp]: lemma vspace_for_pool_detype_Some[simp]: "(vspace_for_pool ap asid (\p. if p \ S then None else pools p) = Some p) = (ap \ S \ vspace_for_pool ap asid pools = Some p)" - by (simp add: vspace_for_pool_def obind_def split: option.splits) + by (simp add: entry_for_pool_def vspace_for_pool_def obind_def split: option.splits) lemma vspace_for_asid_detype_Some[simp]: "(vspace_for_asid asid (detype S s) = Some p) = ((\ap. pool_for_asid asid s = Some ap \ ap \ S) \ vspace_for_asid asid s = Some p)" - apply (simp add: vspace_for_asid_def obind_def asid_pools_of_detype split: option.splits) - apply (auto simp: pool_for_asid_def) - done + by (auto simp: entry_for_asid_def entry_for_pool_def pool_for_asid_def + vspace_for_asid_def obind_def asid_pools_of_detype + split: option.splits) lemma pt_walk_detype: "pt_walk level bot_level pt_ptr vref (ptes_of (detype S s)) = Some (bot_level, p) \ @@ -154,7 +154,7 @@ lemma state_vrefs_detype[Retype_AC_assms, dest]: apply (clarsimp simp: state_vrefs_def) apply (frule vs_lookup_level) apply (drule vs_lookup_table) - apply fastforce + apply (fastforce simp: vspace_objs_of_Some) done lemma sata_detype[Retype_AC_assms]: @@ -190,7 +190,9 @@ lemma aobj_refs'_default'[Retype_AC_assms]: by (cases tp; simp add: arch_default_cap_def ptr_range_memI obj_bits_api_def default_arch_object_def) crunch init_arch_objects - for inv[wp]: P + for pas_refined[wp]: "pas_refined aag" + and integrity_autarch[wp]: "integrity aag X st" + (wp: crunch_wps dmo_no_mem_respects) lemma region_in_kernel_window_preserved: assumes "\P. f \\s. P (arch_state s)\" @@ -375,9 +377,9 @@ global_interpretation Retype_AC_1?: Retype_AC_1 proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; (fact Retype_AC_assms | wpsimp wp: init_arch_objects_inv)?) + by (unfold_locales; (fact Retype_AC_assms | wpsimp)) qed -requalify_facts RISCV64.storeWord_respects +requalify_facts AARCH64.storeWord_respects end diff --git a/proof/access-control/AARCH64/ArchSyscall_AC.thy b/proof/access-control/AARCH64/ArchSyscall_AC.thy index e9c7f0ee17..92a64193db 100644 --- a/proof/access-control/AARCH64/ArchSyscall_AC.thy +++ b/proof/access-control/AARCH64/ArchSyscall_AC.thy @@ -8,7 +8,7 @@ theory ArchSyscall_AC imports Syscall_AC begin -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 named_theorems Syscall_AC_assms @@ -18,6 +18,7 @@ crunch set_original crunch prepare_thread_delete for idle_thread[Syscall_AC_assms, wp]: "\s. P (idle_thread s)" + (wp: crunch_wps simp: crunch_simps) lemma cap_move_idle_thread[Syscall_AC_assms, wp]: "cap_move new_cap src_slot dest_slot \\s. P (idle_thread s)\" @@ -34,10 +35,13 @@ declare arch_finalise_cap_idle_thread[Syscall_AC_assms] lemma invs_irq_state_update[Syscall_AC_assms, simp]: "invs (s\machine_state := irq_state_update f sa\) = invs (s\machine_state := sa\)" apply (rule iffI) - apply (subst invs_irq_state_independent[symmetric]) - apply (subst RISCV64.fold_congs(2); fastforce) - apply (subst (asm) invs_irq_state_independent[symmetric]) - apply (subst RISCV64.fold_congs(2); fastforce) + apply (subst invs_irq_state_independent[where f=f, symmetric]) + apply (erule back_subst[where P=invs]) + apply clarsimp + apply (subst (asm) invs_irq_state_independent[where f=f, symmetric]) + apply clarsimp + apply (erule back_subst[where P=invs]) + apply clarsimp done crunch prepare_thread_delete, arch_finalise_cap @@ -54,13 +58,9 @@ lemma cancel_badged_sends_cur_thread[Syscall_AC_assms, wp]: unfolding cancel_badged_sends_def by (wpsimp wp: dxo_wp_weak filterM_preserved crunch_wps) -crunch arch_mask_irq_signal, handle_reserved_irq - for pas_refined[Syscall_AC_assms, wp]: "pas_refined aag" - -crunch handle_hypervisor_fault +crunch arch_mask_irq_signal for pas_refined[Syscall_AC_assms, wp]: "pas_refined aag" - and cur_thread[Syscall_AC_assms, wp]: "\s. P (cur_thread s)" - and integrity[Syscall_AC_assms, wp]: "integrity aag X st" + (wp: crunch_wps simp: crunch_simps) crunch handle_vm_fault for pas_refined[Syscall_AC_assms, wp]: "pas_refined aag" @@ -71,14 +71,14 @@ lemma handle_vm_fault_integrity[Syscall_AC_assms]: "\integrity aag X st and K (is_subject aag thread)\ handle_vm_fault thread vmfault_type \\rv. integrity aag X st\" - unfolding handle_vm_fault_def - by (cases vmfault_type; wpsimp wp: as_user_integrity_autarch dmo_wp) + unfolding handle_vm_fault_def addressTranslateS1_def + by (cases vmfault_type; wpsimp wp: dmo_no_mem_respects as_user_integrity_autarch ) crunch ackInterrupt, resetTimer for underlying_memory_inv[Syscall_AC_assms, wp]: "\s. P (underlying_memory s)" (simp: maskInterrupt_def) -crunch arch_mask_irq_signal, handle_reserved_irq +crunch arch_mask_irq_signal for integrity[Syscall_AC_assms, wp]: "integrity aag X st" (wp: dmo_no_mem_respects) @@ -120,25 +120,10 @@ lemma arch_activate_idle_thread_pas_refined[Syscall_AC_assms, wp]: "arch_activate_idle_thread t \pas_refined aag\" unfolding arch_activate_idle_thread_def by wpsimp -lemma arch_switch_to_thread_respects[Syscall_AC_assms, wp]: - "arch_switch_to_thread t \integrity aag X st\" - unfolding arch_switch_to_thread_def by wpsimp - -lemma arch_switch_to_thread_pas_refined[Syscall_AC_assms, wp]: - "arch_switch_to_thread t \pas_refined aag\" - unfolding arch_switch_to_thread_def by wpsimp - -lemma arch_switch_to_idle_thread_respects[Syscall_AC_assms, wp]: - "arch_switch_to_idle_thread \integrity aag X st\" - unfolding arch_switch_to_idle_thread_def by wpsimp - -lemma arch_switch_to_idle_thread_pas_refined[Syscall_AC_assms, wp]: - "arch_switch_to_idle_thread \pas_refined aag\" - unfolding arch_switch_to_idle_thread_def by wpsimp - -lemma arch_mask_irq_signal_arch_state[Syscall_AC_assms, wp]: - "arch_mask_irq_signal irq \\s :: det_ext state. P (arch_state s)\" - by wpsimp +crunch arch_switch_to_thread, arch_switch_to_idle_thread + for integrity[Syscall_AC_assms, wp]: "integrity aag X st" + and pas_refined[Syscall_AC_assms, wp]: "pas_refined aag" + (wp: crunch_wps vcpu_switch_respects simp: crunch_simps) lemma handle_reserved_irq_arch_state[Syscall_AC_assms, wp]: "handle_reserved_irq irq \\s :: det_ext state. P (arch_state s)\" @@ -151,15 +136,208 @@ crunch arch_post_cap_deletion crunch arch_post_modify_registers, arch_invoke_irq_control, arch_invoke_irq_handler, arch_perform_invocation, arch_mask_irq_signal, - handle_reserved_irq, handle_vm_fault, handle_hypervisor_fault, handle_arch_fault_reply + handle_vm_fault, handle_arch_fault_reply for cur_thread[Syscall_AC_assms, wp]: "\s. P (cur_thread s)" and idle_thread[Syscall_AC_assms, wp]: "\s. P (idle_thread s)" and cur_domain[Syscall_AC_assms, wp]: "\s. P (cur_domain s)" (wp: crunch_wps simp: crunch_simps) +crunch handle_hypervisor_fault + for idle_thread[Syscall_AC_assms, wp]: "\s :: det_ext state. P (idle_thread s)" + (wp: crunch_wps simp: crunch_simps) + +crunch handle_reserved_irq + for idle_thread[Syscall_AC_assms, wp]: "\s :: det_ext state. P (idle_thread s)" + (wp: crunch_wps simp: crunch_simps) + +crunch set_extra_badge + for cur_domain[Syscall_AC_assms, wp]: "\s :: det_ext state. P (cur_domain s)" + (wp: crunch_wps simp: crunch_simps) + +lemma transfer_caps_loop_cur_domain[wp]: + "transfer_caps_loop ep rcv_buffer n caps slots mi \\s :: det_ext state. P (cur_domain s)\" + supply if_split[split del] + apply (induct caps arbitrary: slots n mi) + apply (wpsimp | assumption)+ + done + +crunch handle_hypervisor_fault + for cur_domain[Syscall_AC_assms, wp]: "\s :: det_ext state. P (cur_domain s)" + (wp: crunch_wps simp: crunch_simps ignore_del: possible_switch_to) + +crunch handle_reserved_irq + for cur_domain[Syscall_AC_assms, wp]: "\s :: det_ext state. P (cur_domain s)" + (wp: crunch_wps simp: crunch_simps) + +crunch vgic_update_lr, vgic_update + for integrity_autarch[Syscall_AC_assms, wp]: "integrity aag X st" + +lemma vgic_maintenance_integrity_autarch: + "\\s. integrity aag X st s \ pas_refined aag s \ is_subject aag (cur_thread s) \ invs s\ + vgic_maintenance + \\rv. integrity aag X st\" + (is "\?P\ _ \_\") + unfolding vgic_maintenance_def vgic_update_lr_def get_gic_vcpu_ctrl_misr_def + get_gic_vcpu_ctrl_eisr0_def get_gic_vcpu_ctrl_eisr1_def + apply (wpsimp wp: handle_fault_integrity_autarch gts_wp dmo_no_mem_respects split_del: if_split + | wpsimp wp: hoare_vcg_all_lift hoare_drop_imps)+ + apply (frule invs_cur) + apply (frule invs_valid_cur_vcpu) + apply (clarsimp simp: valid_fault_def cur_tcb_def tcb_at_def) + apply (fastforce intro: associated_vcpu_is_subject + simp: valid_cur_vcpu_def pred_tcb_at_def obj_at_def active_cur_vcpu_of_def get_tcb_def) + done + +lemma vppi_event_integrity_autarch: + "\\s. integrity aag X st s \ pas_refined aag s \ (is_subject aag (cur_thread s)) \ invs s\ + vppi_event irq + \\_ s. integrity aag X st s\" + unfolding vppi_event_def + apply (wpsimp wp: handle_fault_integrity_autarch maskInterrupt_invs dmo_no_mem_respects + vcpu_update_integrity_autarch vcpu_update_pas_refined vcpu_update_trivial_invs + simp: if_fun_split + | wpsimp wp: hoare_vcg_all_lift hoare_drop_imps)+ + apply (frule invs_cur) + apply (frule invs_valid_cur_vcpu) + apply (clarsimp simp: valid_fault_def cur_tcb_def tcb_at_def) + apply (fastforce intro: associated_vcpu_is_subject + simp: valid_cur_vcpu_def pred_tcb_at_def obj_at_def active_cur_vcpu_of_def get_tcb_def) + done + +lemma handle_reserved_irq_integrity_autarch[Syscall_AC_assms]: + "\integrity aag X st and pas_refined aag and invs and (\s. is_subject aag (cur_thread s))\ + handle_reserved_irq irq + \\_. integrity aag X st\" + unfolding handle_reserved_irq_def + by (wpsimp wp: vppi_event_integrity_autarch vgic_maintenance_integrity_autarch) + +lemma vppi_event_pas_refined: + "\\s. pas_refined aag s \ (ct_active s \ is_subject aag (cur_thread s)) \ invs s\ + vppi_event irq + \\_ s. pas_refined aag s\" + unfolding vppi_event_def + apply (wpsimp wp: handle_fault_pas_refined gts_wp vcpu_update_pas_refined) + apply (rule hoare_lift_Pf2[where f="cur_thread", rotated]) + apply wpsimp + apply (wpsimp wp: vcpu_update_pas_refined vcpu_update_trivial_invs + hoare_vcg_all_lift hoare_vcg_imp_lift) + apply (rule_tac Q'="\rv s. pas_refined aag s \ (ct_active s \ is_subject aag (cur_thread s)) \ invs s" + in hoare_strengthen_post[rotated]) + apply (clarsimp simp: valid_fault_def ct_in_state_def pred_tcb_at_def obj_at_def runnable_eq) + apply (wpsimp wp: maskInterrupt_invs hoare_vcg_imp_lift)+ + done + +lemma vgic_maintenance_pas_refined: + "\\s. pas_refined aag s \ (ct_active s \ is_subject aag (cur_thread s)) \ invs s\ + vgic_maintenance + \\_ s. pas_refined aag s\" + unfolding vgic_maintenance_def vgic_update_lr_def vgic_update_def + get_gic_vcpu_ctrl_misr_def get_gic_vcpu_ctrl_eisr1_def get_gic_vcpu_ctrl_eisr0_def + apply (wpsimp wp: handle_fault_pas_refined gts_wp vcpu_update_pas_refined) + apply (rule hoare_lift_Pf2[where f="cur_thread", rotated]) + apply wpsimp + apply (wpsimp wp: vcpu_update_pas_refined vcpu_update_trivial_invs + hoare_vcg_all_lift hoare_vcg_imp_lift) + apply (rule_tac Q'="\rv s. pas_refined aag s \ (ct_active s \ is_subject aag (cur_thread s)) \ invs s" + in hoare_strengthen_post[rotated]) + apply (clarsimp simp: valid_fault_def ct_in_state_def pred_tcb_at_def obj_at_def runnable_eq) + apply ((wpsimp wp: hoare_vcg_imp_lift)+)[4] + apply (rule_tac Q'="\rv s. pas_refined aag s \ (ct_active s \ is_subject aag (cur_thread s)) \ invs s" + in hoare_strengthen_post[rotated]) + apply (auto simp: valid_fault_def ct_in_state_def pred_tcb_at_def obj_at_def runnable_eq)[1] + apply wpsimp+ + done + +lemma handle_reserved_irq_pas_refined[Syscall_AC_assms]: + "\\s. pas_refined aag s \ invs s \ (ct_active s \ is_subject aag (cur_thread s))\ + handle_reserved_irq irq + \\_ s. pas_refined aag s\" + unfolding handle_reserved_irq_def + by (wpsimp wp: vppi_event_pas_refined vgic_maintenance_pas_refined) + +lemma vgic_maintenance_idle: + "\integrity aag X st and invs and ct_idle\ + vgic_maintenance + \\_. integrity aag X st\" + unfolding vgic_maintenance_def + apply (rule bind_wp) + apply (rule_tac P'="\s. integrity aag X st s \ (\v. rv \ Some (v,True))" in hoare_weaken_pre) + apply (case_tac rv; clarsimp) + apply (case_tac b; clarsimp) + apply assumption + apply (wpsimp) + apply (prop_tac "only_idle s") + apply (clarsimp simp: invs_def valid_state_def) + apply (prop_tac "arch_tcb_at (\itcb. itcb_vcpu itcb = None) (idle_thread s) s") + apply (frule invs_valid_idle) + apply (clarsimp simp: valid_idle_def pred_tcb_at_def valid_arch_idle_def obj_at_def) + apply (frule invs_valid_cur_vcpu) + apply (clarsimp simp: valid_cur_vcpu_def only_idle_def pred_tcb_at_def + ct_in_state_def obj_at_def active_cur_vcpu_of_def) + done + +lemma vppi_event_idle: + "\integrity aag X st and invs and ct_idle\ + vppi_event irq + \\_. integrity aag X st\" + unfolding vppi_event_def + apply (rule bind_wp) + apply (rule_tac P'="\s. integrity aag X st s \ (\v. rv \ Some (v,True))" in hoare_weaken_pre) + apply (case_tac rv; clarsimp) + apply (case_tac b; clarsimp) + apply assumption + apply (wpsimp) + apply (prop_tac "only_idle s") + apply (clarsimp simp: invs_def valid_state_def) + apply (prop_tac "arch_tcb_at (\itcb. itcb_vcpu itcb = None) (idle_thread s) s") + apply (frule invs_valid_idle) + apply (clarsimp simp: valid_idle_def pred_tcb_at_def valid_arch_idle_def obj_at_def) + apply (frule invs_valid_cur_vcpu) + apply (clarsimp simp: valid_cur_vcpu_def only_idle_def pred_tcb_at_def + ct_in_state_def obj_at_def active_cur_vcpu_of_def) + done + +lemma handle_reserved_irq_idle[Syscall_AC_assms]: + "\integrity aag X st and invs and ct_idle\ + handle_reserved_irq irq + \\_. integrity aag X st\" + unfolding handle_reserved_irq_def + by (wpsimp wp: vppi_event_idle vgic_maintenance_idle) + +lemma handle_hypervisor_fault_pas_refined[Syscall_AC_assms, wp]: + "\\s. pas_refined aag s \ is_subject aag (cur_thread s) \ is_subject aag thread \ invs s\ + handle_hypervisor_fault thread fault + \\_ s. pas_refined aag s\" + apply (case_tac fault) + apply clarify + apply (subst handle_hypervisor_fault.simps) + apply (wpsimp wp: handle_fault_pas_refined simp: getESR_def isFpuEnable_def valid_fault_def) + done + +lemma handle_hypervisor_fault_integrity_autarch[Syscall_AC_assms, wp]: + "\\s. integrity aag X st s \ pas_refined aag s \ invs s \ is_subject aag thread + \ (ct_active s \ is_subject aag (cur_thread s))\ + handle_hypervisor_fault thread fault + \\_ s. integrity aag X st s\" + apply (case_tac fault) + apply clarify + apply (subst handle_hypervisor_fault.simps) + apply (wpsimp wp: handle_fault_integrity_autarch simp: getESR_def isFpuEnable_def valid_fault_def) + done + \ \These aren't proved in the previous crunch, and hence need to be declared\ -declare handle_arch_fault_reply_cur_thread[Syscall_AC_assms] declare handle_arch_fault_reply_it[Syscall_AC_assms] +declare handle_arch_fault_reply_cur_thread[Syscall_AC_assms] +declare arch_invoke_irq_control_cur_thread[Syscall_AC_assms] +declare arch_invoke_irq_handler_cur_thread[Syscall_AC_assms] +declare arch_mask_irq_signal_cur_thread[Syscall_AC_assms] +declare handle_reserved_irq_cur_thread[Syscall_AC_assms] +declare handle_hypervisor_fault_cur_thread[Syscall_AC_assms] +declare handle_vm_fault_cur_thread[Syscall_AC_assms] +declare ackInterrupt_underlying_memory_inv[Syscall_AC_assms] +declare resetTimer_underlying_memory_inv[Syscall_AC_assms] +declare arch_mask_irq_signal_arch_state[Syscall_AC_assms] +declare init_arch_objects_arch_state[Syscall_AC_assms] end @@ -168,7 +346,7 @@ global_interpretation Syscall_AC_1?: Syscall_AC_1 proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; (fact Syscall_AC_assms | wp init_arch_objects_inv)) + by (unfold_locales; fact Syscall_AC_assms) qed end diff --git a/proof/access-control/AARCH64/ArchTcb_AC.thy b/proof/access-control/AARCH64/ArchTcb_AC.thy index 800f889a7e..39c1a4a2e8 100644 --- a/proof/access-control/AARCH64/ArchTcb_AC.thy +++ b/proof/access-control/AARCH64/ArchTcb_AC.thy @@ -8,7 +8,7 @@ theory ArchTcb_AC imports Tcb_AC begin -context Arch begin global_naming RISCV64 +context Arch begin global_naming AARCH64 named_theorems Tcb_AC_assms @@ -92,9 +92,9 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]: emptyable_def | rule conjI | erule pas_refined_refl)+ apply (thin_tac "case_option _ _ _")+ - apply (fastforce split: cap.split_asm option.split_asm) + apply (fastforce split: cap.split_asm option.split_asm pt_type.split_asm) apply (thin_tac "case_option _ _ _")+ - apply (fastforce split: cap.split_asm option.split_asm) + apply (fastforce split: cap.split_asm option.split_asm pt_type.split_asm) done end diff --git a/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy b/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy index 01d12ad001..ef1627b0d8 100644 --- a/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy @@ -31,7 +31,12 @@ lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_assms]: lemma arch_stt_invs [wp,Schedule_AI_assms]: "arch_switch_to_thread t' \invs\" apply (wpsimp simp: arch_switch_to_thread_def) - by (rule sym_refs_VCPU_hyp_live; fastforce) + apply (clarsimp simp: obj_at_vcpu_hyp_live_of_s[symmetric] obj_at_conj_distrib) + apply (rule conjI) + apply (fastforce dest!: valid_tcb_objs[OF invs_valid_objs] + simp: valid_tcb_def valid_arch_tcb_def obj_at_def is_vcpu_def) + apply (rule sym_refs_VCPU_hyp_live; fastforce) + done lemma arch_stt_tcb [wp,Schedule_AI_assms]: "arch_switch_to_thread t' \tcb_at t'\" diff --git a/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy b/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy index 35dc4a38bc..e8d2ec6c0c 100644 --- a/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy @@ -120,8 +120,10 @@ lemma switch_vcpu_valid_cur_vcpu_cur_thread_update[wp]: vcpu_switch v \\_ s. valid_cur_vcpu (s\cur_thread := t\)\" unfolding vcpu_switch_def - apply (wpsimp simp: valid_cur_vcpu_def active_cur_vcpu_of_def) - by fastforce + apply (wpsimp simp: valid_cur_vcpu_def active_cur_vcpu_of_def + | rule hoare_lift_Pf[where f=arch_state])+ + apply fastforce + done lemma switch_vcpu_valid_cur_vcpu[wp]: "\\s. arch_tcb_at (\itcb. itcb_vcpu itcb = v) (cur_thread s) s\ diff --git a/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy b/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy index 48bb3f688a..77163ae0fa 100644 --- a/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy @@ -3063,13 +3063,14 @@ crunch vcpu_disable, vcpu_restore, vcpu_save (wp: crunch_wps) lemma vcpu_switch_invs[wp]: - "\invs and (\s. v \ None \ obj_at hyp_live (the v) s)\ vcpu_switch v \ \_ . invs \" + "\invs and (\s. v \ None \ vcpu_hyp_live_of s (the v))\ vcpu_switch v \ \_ . invs \" unfolding vcpu_switch_def apply (cases v; clarsimp) apply (wpsimp simp: cur_vcpu_at_def | strengthen invs_current_vcpu_update')+ apply (clarsimp simp: invs_def valid_state_def valid_arch_state_def cur_vcpu_def in_omonad obj_at_def hyp_live_def arch_live_def) apply (wpsimp simp: cur_vcpu_at_def | strengthen invs_current_vcpu_update')+ + apply (clarsimp simp: in_omonad obj_at_def hyp_live_def arch_live_def) done crunch diff --git a/spec/abstract/AARCH64/VCPUAcc_A.thy b/spec/abstract/AARCH64/VCPUAcc_A.thy index 26b69800fa..7304ee1c94 100644 --- a/spec/abstract/AARCH64/VCPUAcc_A.thy +++ b/spec/abstract/AARCH64/VCPUAcc_A.thy @@ -244,21 +244,21 @@ definition vcpu_switch :: "obj_ref option \ (unit,'z::state_ext) s_m cur_v \ gets (arm_current_vcpu \ arch_state); (case cur_v of None \ do \ \switch to the new vcpu with no current one\ - vcpu_restore new; - modify (\s. s\ arch_state := (arch_state s)\ arm_current_vcpu := Some (new, True) \\) + modify (\s. s\ arch_state := (arch_state s)\ arm_current_vcpu := Some (new, True) \\); + vcpu_restore new od | Some (vr, active) \ \ \switch from an existing vcpu\ (if vr \ new then do \ \different vcpu\ vcpu_save cur_v; - vcpu_restore new; - modify (\s. s\ arch_state := (arch_state s)\ arm_current_vcpu := Some (new, True) \\) + modify (\s. s\ arch_state := (arch_state s)\ arm_current_vcpu := Some (new, True) \\); + vcpu_restore new od else \ \same vcpu\ when (\ active) $ do do_machine_op isb; - vcpu_enable new; - modify (\s. s\ arch_state := (arch_state s)\ arm_current_vcpu := Some (new, True) \\) + modify (\s. s\ arch_state := (arch_state s)\ arm_current_vcpu := Some (new, True) \\); + vcpu_enable new od)) od"