From 357ccc987dee33b7b9780145e17f3205d462ceda Mon Sep 17 00:00:00 2001 From: Ryan Barry Date: Thu, 12 Dec 2024 13:04:18 +1100 Subject: [PATCH] access: relax conditions -Remove various instances of pspace_aligned, valid_vspace_objs, and valid_asid_table/valid_arch_state from preconditions -Relax the is_subject predicate in various Syscall_AC lemmas Signed-off-by: Ryan Barry --- proof/access-control/ARM/ArchDomainSepInv.thy | 32 +-- proof/access-control/ARM/ArchInterrupt_AC.thy | 5 +- proof/access-control/ARM/ArchSyscall_AC.thy | 2 +- proof/access-control/Arch_AC.thy | 16 +- proof/access-control/CNode_AC.thy | 60 ++--- proof/access-control/DomainSepInv.thy | 206 ++++++++--------- proof/access-control/Finalise_AC.thy | 71 ++---- proof/access-control/Interrupt_AC.thy | 6 +- proof/access-control/Ipc_AC.thy | 115 +++------- proof/access-control/RISCV64/ArchArch_AC.thy | 15 +- proof/access-control/RISCV64/ArchCNode_AC.thy | 45 ++-- .../RISCV64/ArchDomainSepInv.thy | 42 ++-- .../RISCV64/ArchFinalise_AC.thy | 17 +- .../RISCV64/ArchInterrupt_AC.thy | 3 +- proof/access-control/RISCV64/ArchIpc_AC.thy | 5 - .../access-control/RISCV64/ArchSyscall_AC.thy | 3 +- proof/access-control/Retype_AC.thy | 80 ++----- proof/access-control/Syscall_AC.thy | 207 ++++++++++-------- proof/access-control/Tcb_AC.thy | 27 +-- 19 files changed, 383 insertions(+), 574 deletions(-) diff --git a/proof/access-control/ARM/ArchDomainSepInv.thy b/proof/access-control/ARM/ArchDomainSepInv.thy index a71f853432..74d5be62f2 100644 --- a/proof/access-control/ARM/ArchDomainSepInv.thy +++ b/proof/access-control/ARM/ArchDomainSepInv.thy @@ -25,6 +25,21 @@ 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 +crunch + invalidate_tlb_by_asid, handle_reserved_irq, handle_vm_fault, + handle_hypervisor_fault, handle_arch_fault_reply, arch_mask_irq_signal, + arch_switch_to_thread, arch_switch_to_idle_thread, arch_activate_idle_thread + for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st" + +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 x31 \domain_sep_inv irqs st\" + unfolding arch_post_modify_registers_def by wpsimp + end @@ -38,12 +53,6 @@ qed context Arch begin global_naming ARM_A -crunch - invalidate_tlb_by_asid, handle_reserved_irq, handle_vm_fault, - handle_hypervisor_fault, handle_arch_fault_reply, arch_mask_irq_signal, - arch_switch_to_thread, arch_switch_to_idle_thread, arch_activate_idle_thread - for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st" - lemma perform_page_invocation_domain_sep_inv: "\domain_sep_inv irqs st and valid_page_inv pgi\ perform_page_invocation pgi @@ -120,15 +129,6 @@ 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 - -lemma arch_post_modify_registers_domain_sep_inv[DomainSepInv_assms, wp]: - "arch_post_modify_registers cur x31 \domain_sep_inv irqs st\" - unfolding arch_post_modify_registers_def by wpsimp - end @@ -136,7 +136,7 @@ global_interpretation DomainSepInv_2?: DomainSepInv_2 proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; fact DomainSepInv_assms) + by (unfold_locales; wpsimp wp: DomainSepInv_assms) qed end diff --git a/proof/access-control/ARM/ArchInterrupt_AC.thy b/proof/access-control/ARM/ArchInterrupt_AC.thy index 78abd12d2b..9ac28a213a 100644 --- a/proof/access-control/ARM/ArchInterrupt_AC.thy +++ b/proof/access-control/ARM/ArchInterrupt_AC.thy @@ -21,8 +21,7 @@ definition arch_authorised_irq_ctl_inv :: (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,7 +74,7 @@ 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) qed diff --git a/proof/access-control/ARM/ArchSyscall_AC.thy b/proof/access-control/ARM/ArchSyscall_AC.thy index 068449213b..c717a31f5e 100644 --- a/proof/access-control/ARM/ArchSyscall_AC.thy +++ b/proof/access-control/ARM/ArchSyscall_AC.thy @@ -179,7 +179,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)?) + by (unfold_locales; wpsimp wp: Syscall_AC_assms) qed end diff --git a/proof/access-control/Arch_AC.thy b/proof/access-control/Arch_AC.thy index 512058f6b9..195dc942d5 100644 --- a/proof/access-control/Arch_AC.thy +++ b/proof/access-control/Arch_AC.thy @@ -68,9 +68,7 @@ lemma mapM_set'': done lemma as_user_state_vrefs: - "\pspace_aligned and valid_vspace_objs and valid_arch_state and (\s. P (state_vrefs s))\ - as_user t f - \\_ s :: det_ext state. P (state_vrefs s)\" + "as_user t f \\s :: det_ext state. P (state_vrefs s)\" apply (simp add: as_user_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: state_vrefs_tcb_upd obj_at_def is_obj_defs @@ -79,9 +77,7 @@ lemma as_user_state_vrefs: done lemma as_user_pas_refined[wp]: - "\pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag\ - as_user t f - \\_. pas_refined aag\" + "as_user t f \pas_refined aag\" apply (simp add: pas_refined_def state_objs_to_policy_def) apply (rule hoare_pre) apply wps @@ -151,9 +147,7 @@ lemma is_subject_asid_into_loas: locale Arch_AC_1 = assumes set_mrs_state_vrefs[wp]: - "\pspace_aligned and valid_vspace_objs and valid_arch_state and (\s. P (state_vrefs s))\ - set_mrs thread buf msgs - \\_ s :: det_ext state. P (state_vrefs s)\" + "set_mrs thread buf msgs \\s :: det_ext state. P (state_vrefs s)\" and mul_add_word_size_lt_msg_align_bits_ofnat: "\ p < 2 ^ (msg_align_bits - word_size_bits); k < word_size \ \ of_nat p * of_nat word_size + k < (2 :: obj_ref) ^ msg_align_bits" @@ -196,9 +190,7 @@ lemma store_word_offs_integrity_autarch: done lemma set_mrs_pas_refined[wp]: - "\pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag\ - set_mrs thread buf msgs - \\_. pas_refined aag\" + "set_mrs thread buf msgs \pas_refined aag\" apply (simp add: pas_refined_def state_objs_to_policy_def) apply (rule hoare_pre) apply (wp | wps)+ diff --git a/proof/access-control/CNode_AC.thy b/proof/access-control/CNode_AC.thy index b79309883c..d45ce00054 100644 --- a/proof/access-control/CNode_AC.thy +++ b/proof/access-control/CNode_AC.thy @@ -67,18 +67,14 @@ locale CNode_AC_1 = state_asids_to_policy_arch aag caps (as :: arch_state) vrefs \ pasPolicy aag \ \ state_asids_to_policy_arch aag (caps(ptr \ cap, ptr' \ cap')) as vrefs \ pasPolicy aag" and state_vrefs_tcb_upd: - "\ pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tcb_at tptr s \ - \ state_vrefs (s\kheap := (kheap s)(tptr \ TCB tcb)\) = state_vrefs s" + "tcb_at tptr s \ state_vrefs (s\kheap := (kheap s)(tptr \ TCB tcb)\) = state_vrefs s" and state_vrefs_simple_type_upd: - "\ pspace_aligned s; valid_vspace_objs s; valid_arch_state s; - ko_at ko p s; is_simple_type ko; a_type ko = a_type (f (val :: 'b)) \ + "\ ko_at ko p s; is_simple_type ko; a_type ko = a_type (f (val :: 'b)) \ \ state_vrefs (s\kheap := (kheap s)(p \ f val)\) = state_vrefs s" and a_type_arch_object_not_tcb[simp]: "a_type (ArchObj arch_kernel_obj) \ ATCB" and set_cap_state_vrefs: - "\P. \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)\" + "\P. set_cap cap slot \\s :: det_ext state. P (state_vrefs s)\" and set_cdt_state_vrefs[wp]: "\P. set_cdt t \\s :: det_ext state. P (state_vrefs s)\" and set_cdt_state_asids_to_policy[wp]: @@ -308,7 +304,7 @@ lemma sita_caps_update2: context CNode_AC_1 begin lemma set_cap_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and + "\pas_refined aag and (\s. (is_transferable_in ptr s \ (\ Option.is_none (cdt s ptr))) \ is_transferable_cap cap \ abs_has_auth_to aag Control (fst $ the $ cdt s ptr) (fst ptr)) and @@ -330,8 +326,7 @@ lemma set_cap_pas_refined: done lemma set_cap_pas_refined_not_transferable: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and cte_wp_at (\c. \is_transferable (Some c)) ptr + "\pas_refined aag and cte_wp_at (\c. \is_transferable (Some c)) ptr and K (aag_cap_auth aag (pasObjectAbs aag (fst ptr)) cap)\ set_cap cap ptr \\_. pas_refined aag\" @@ -1025,7 +1020,7 @@ locale CNode_AC_3 = CNode_AC_2 + begin lemma cap_insert_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and + "\pas_refined aag and valid_mdb and (\s. (is_transferable_in src_slot s \ (\ Option.is_none (cdt s src_slot))) \ is_transferable_cap new_cap) and K (is_subject aag (fst dest_slot) \ is_subject aag (fst src_slot) @@ -1049,7 +1044,7 @@ lemma cap_insert_pas_refined: dest: aag_cdt_link_Control aag_cdt_link_DeleteDerived cap_auth_caps_of_state) lemma cap_insert_pas_refined': - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and + "\pas_refined aag and valid_mdb and (\s. cte_wp_at is_transferable_cap src_slot s \ is_transferable_cap new_cap) and K (is_subject aag (fst dest_slot) \ is_subject aag (fst src_slot) \ pas_cap_cur_auth aag new_cap) \ @@ -1060,7 +1055,7 @@ lemma cap_insert_pas_refined': simp: cte_wp_at_caps_of_state Option.is_none_def) lemma cap_insert_pas_refined_not_transferable: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb + "\pas_refined aag and valid_mdb and not cte_wp_at is_transferable_cap src_slot and K (is_subject aag (fst dest_slot) \ is_subject aag (fst src_slot) \ pas_cap_cur_auth aag new_cap) \ @@ -1069,7 +1064,7 @@ lemma cap_insert_pas_refined_not_transferable: by (wpsimp wp: cap_insert_pas_refined') lemma cap_insert_pas_refined_same_object_as: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb + "\pas_refined aag and valid_mdb and cte_wp_at (same_object_as new_cap) src_slot and K (is_subject aag (fst dest_slot) \ is_subject aag (fst src_slot) \ (\ is_master_reply_cap new_cap) \ pas_cap_cur_auth aag new_cap)\ @@ -1081,8 +1076,7 @@ lemma cap_insert_pas_refined_same_object_as: elim: is_transferable_capE split: cap.splits) lemma cap_move_pas_refined[wp]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and valid_mdb and cte_wp_at (weak_derived new_cap) src_slot + "\pas_refined aag and valid_mdb and cte_wp_at (weak_derived new_cap) src_slot and cte_wp_at ((=) NullCap) dest_slot and K (is_subject aag (fst dest_slot) \ is_subject aag (fst src_slot) \ pas_cap_cur_auth aag new_cap)\ @@ -1099,14 +1093,8 @@ lemma cap_move_pas_refined[wp]: dest: invs_mdb pas_refined_mem[OF sta_cdt] pas_refined_mem[OF sta_cdt_transferable]) -crunch set_original, set_cdt - for pspace_aligned[wp]: pspace_aligned - and valid_vspace_objs[wp]: valid_vspace_objs - and valid_arch_state[wp]: valid_arch_state - lemma empty_slot_pas_refined[wp, wp_not_transferable]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and valid_mdb and K (is_subject aag (fst slot))\ + "\pas_refined aag and valid_mdb and K (is_subject aag (fst slot))\ empty_slot slot irqopt \\_. pas_refined aag\" apply (simp add: empty_slot_def post_cap_deletion_def) @@ -1119,8 +1107,7 @@ lemma empty_slot_pas_refined[wp, wp_not_transferable]: lemma empty_slot_pas_refined_transferable[wp_transferable]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and valid_mdb and (\s. is_transferable (caps_of_state s slot))\ + "\pas_refined aag and valid_mdb and (\s. is_transferable (caps_of_state s slot))\ empty_slot slot irqopt \\_. pas_refined aag\" apply (simp add: empty_slot_def post_cap_deletion_def) @@ -1178,7 +1165,7 @@ lemma cap_swap_pas_refined[wp]: by (erule subsetD; force simp: is_transferable_weak_derived intro!: sbta_cdt_transferable auth_graph_map_memI)+ apply (blast intro: state_bits_to_policy.intros auth_graph_map_memI) - by fastforce+ + done lemma cap_swap_for_delete_pas_refined[wp]: "\pas_refined aag and invs and K (is_subject aag (fst slot) \ is_subject aag (fst slot'))\ @@ -1305,9 +1292,7 @@ lemma set_simple_ko_ekheap[wp]: context CNode_AC_3 begin lemma sts_st_vrefs[wp]: - "\pspace_aligned and valid_vspace_objs and valid_arch_state and (\s. P (state_vrefs s))\ - set_thread_state t st - \\_ s :: det_ext state. P (state_vrefs s)\" + "set_thread_state t st \\s :: det_ext state. P (state_vrefs s)\" apply (simp add: set_thread_state_def del: set_thread_state_ext_extended.dxo_eq) apply (wpsimp wp: set_object_wp dxo_wp_weak) apply (clarsimp simp: state_vrefs_tcb_upd obj_at_def is_obj_defs @@ -1316,8 +1301,7 @@ lemma sts_st_vrefs[wp]: done lemma set_thread_state_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and - K (\r \ tcb_st_to_auth st. abs_has_auth_to aag (snd r) t (fst r))\ + "\pas_refined aag and K (\r \ tcb_st_to_auth st. abs_has_auth_to aag (snd r) t (fst r))\ set_thread_state t st \\_. pas_refined aag\" apply (simp add: pas_refined_def state_objs_to_policy_def) @@ -1330,17 +1314,14 @@ lemma set_thread_state_pas_refined: done lemma set_simple_ko_vrefs[wp]: - "\pspace_aligned and valid_vspace_objs and valid_arch_state and (\s. P (state_vrefs s))\ - set_simple_ko f ptr (val :: 'b) - \\_ s :: det_ext state. P (state_vrefs s)\" + "set_simple_ko f ptr (val :: 'b) \\s :: det_ext state. P (state_vrefs s)\" apply (simp add: set_simple_ko_def set_object_def) apply (wp get_object_wp) apply (fastforce simp: state_vrefs_simple_type_upd obj_at_def elim!: rsubst[where P=P, OF _ ext]) done lemma set_simple_ko_pas_refined[wp]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ - set_simple_ko f ptr (ep :: 'b) \\_. pas_refined aag\" + "set_simple_ko f ptr (ep :: 'b) \pas_refined aag\" apply (simp add: pas_refined_def state_objs_to_policy_def) apply (rule hoare_pre) apply (wp tcb_domain_map_wellformed_lift | wps)+ @@ -1348,9 +1329,7 @@ lemma set_simple_ko_pas_refined[wp]: done lemma thread_set_state_vrefs: - "\pspace_aligned and valid_vspace_objs and valid_arch_state and (\s. P (state_vrefs s))\ - thread_set f t - \\_ s :: det_ext state. P (state_vrefs s)\" + "thread_set f t \\s :: det_ext state. P (state_vrefs s)\" apply (simp add: thread_set_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: state_vrefs_tcb_upd obj_at_def is_obj_defs @@ -1387,8 +1366,7 @@ lemma thread_set_pas_refined_triv: assumes cps: "\tcb. \(getF, v)\ran tcb_cap_cases. getF (f tcb) = getF tcb" and st: "\tcb. tcb_state (f tcb) = tcb_state tcb" and ntfn: "\tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb" - shows "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ - thread_set f t \\_. pas_refined aag\" + shows "thread_set f t \pas_refined aag\" by (wpsimp wp: tcb_domain_map_wellformed_lift thread_set_state_vrefs simp: pas_refined_def state_objs_to_policy_def | wps thread_set_caps_of_state_trivial[OF cps] diff --git a/proof/access-control/DomainSepInv.thy b/proof/access-control/DomainSepInv.thy index 7d2c2c6421..0650010cc8 100644 --- a/proof/access-control/DomainSepInv.thy +++ b/proof/access-control/DomainSepInv.thy @@ -320,6 +320,22 @@ locale DomainSepInv_1 = "prepare_thread_delete t \\s :: det_ext state. domain_sep_inv irqs st s\" and arch_finalise_cap_rv: "\\_. P (NullCap,NullCap)\ arch_finalise_cap c x \\rv s :: det_ext state. P rv\" + and arch_switch_to_thread_domain_sep_inv[wp]: + "arch_switch_to_thread t \\s :: det_ext state. domain_sep_inv irqs (st :: 'state_ext state) s\" + and arch_switch_to_idle_thread_domain_sep_inv[wp]: + "arch_switch_to_idle_thread \\s :: det_ext state. domain_sep_inv irqs st s\" + and arch_activate_idle_thread_domain_sep_inv[wp]: + "arch_activate_idle_thread t \\s :: det_ext state. domain_sep_inv irqs st s\" + and arch_mask_irq_signal_domain_sep_inv[wp]: + "arch_mask_irq_signal irq \\s :: det_ext state. domain_sep_inv irqs st s\" + and arch_derive_cap_domain_sep_inv[wp]: + "\\\ arch_derive_cap acap \\rv s :: det_ext state. domain_sep_inv_cap irqs rv\,-" + and arch_post_modify_registers_domain_sep_inv[wp]: + "arch_post_modify_registers cur t \\s :: det_ext state. domain_sep_inv irqs st s\" + and handle_arch_fault_reply_domain_sep_inv[wp]: + "handle_arch_fault_reply vmf thread d ds \\s :: det_ext state. domain_sep_inv irqs st s\" + and handle_vm_fault_domain_sep_inv[wp]: + "handle_vm_fault t vmf_t \\s :: det_ext state. domain_sep_inv irqs st s\" begin lemma deleted_irq_handler_domain_sep_inv: @@ -739,83 +755,6 @@ lemma domain_sep_inv_cap_ArchObjectCap[simp]: "domain_sep_inv_cap irqs (ArchObjectCap arch_cap)" by (simp add: domain_sep_inv_cap_def) - -locale DomainSepInv_2 = DomainSepInv_1 state_ext_t - for state_ext_t :: "'state_ext :: state_ext itself" + - assumes arch_switch_to_thread_domain_sep_inv[wp]: - "arch_switch_to_thread t \\s :: det_ext state. domain_sep_inv irqs (st :: 'state_ext state) s\" - and arch_switch_to_idle_thread_domain_sep_inv[wp]: - "arch_switch_to_idle_thread \\s :: det_ext state. domain_sep_inv irqs st s\" - and arch_activate_idle_thread_domain_sep_inv[wp]: - "arch_activate_idle_thread t \\s :: det_ext state. domain_sep_inv irqs st s\" - and arch_mask_irq_signal_domain_sep_inv[wp]: - "arch_mask_irq_signal irq \\s :: det_ext state. domain_sep_inv irqs st s\" - and arch_derive_cap_domain_sep_inv[wp]: - "\\\ arch_derive_cap acap \\rv s :: det_ext state. domain_sep_inv_cap irqs rv\,-" - and arch_post_modify_registers_domain_sep_inv[wp]: - "arch_post_modify_registers cur x31 \\s :: det_ext state. domain_sep_inv irqs st s\" - and arch_perform_invocation_domain_sep_inv[wp]: - "\domain_sep_inv irqs st and valid_arch_inv ai\ - arch_perform_invocation ai - \\_ s :: det_ext state. domain_sep_inv irqs st s\" - and arch_invoke_irq_handler_domain_sep_inv[wp]: - "arch_invoke_irq_handler ihi \\s :: det_ext state. domain_sep_inv irqs st s\" - and arch_invoke_irq_control_domain_sep_inv: - "\domain_sep_inv irqs st and arch_irq_control_inv_valid ivk\ - arch_invoke_irq_control ivk - \\_ s :: det_ext state. domain_sep_inv irqs st s\" - and handle_arch_fault_reply_domain_sep_inv[wp]: - "handle_arch_fault_reply vmf thread x y \\s :: det_ext state. domain_sep_inv irqs st s\" - and handle_hypervisor_fault_domain_sep_inv[wp]: - "handle_hypervisor_fault t hf_t \\s :: det_ext state. domain_sep_inv irqs st s\" - and handle_vm_fault_domain_sep_inv[wp]: - "handle_vm_fault t vmf_t \\s :: det_ext state. domain_sep_inv irqs st s\" - and handle_reserved_irq_domain_sep_inv[wp]: - "handle_reserved_irq irq \\s :: det_ext state. domain_sep_inv irqs st s\" -begin - -(* when i is AckIRQ the preconditions here contradict each other, which - is why this lemma is true *) -lemma invoke_irq_handler_domain_sep_inv: - "\domain_sep_inv irqs st and irq_handler_inv_valid i\ - invoke_irq_handler i - \\_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\" - apply (case_tac i) - apply (wp cap_insert_domain_sep_inv' | simp)+ - apply (rename_tac irq cap cslot_ptr s) - apply (case_tac cap, simp_all add: domain_sep_inv_cap_def)[1] - apply (wp | clarsimp)+ - done - -(* similarly, the preconditions here tend to contradict one another *) -lemma invoke_control_domain_sep_inv: - "\domain_sep_inv irqs st and irq_control_inv_valid i\ - invoke_irq_control i - \\_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\" - including classic_wp_pre - apply (case_tac i) - apply (case_tac irqs) - apply (wp cap_insert_domain_sep_inv' | simp )+ - apply (simp add: set_irq_state_def, wp, simp) - apply (fastforce simp: domain_sep_inv_def domain_sep_inv_cap_def) - apply (fastforce simp: valid_def domain_sep_inv_def) - apply simp - apply (wp arch_invoke_irq_control_domain_sep_inv) - done - -lemma derive_cap_domain_sep_inv_cap: - "\\s. domain_sep_inv_cap irqs cap\ - derive_cap slot cap - \\rv s :: det_ext state. domain_sep_inv_cap irqs rv\,-" - apply (simp add: derive_cap_def) - apply (rule hoare_pre) - apply (wp | wpc | simp add: )+ - apply auto - done - -end - - crunch receive_signal, complete_signal for domain_sep_inv[wp]: "domain_sep_inv irqs st" @@ -850,7 +789,7 @@ lemma transfer_caps_domain_sep_inv: done -context DomainSepInv_2 begin +context DomainSepInv_1 begin lemma do_normal_transfer_domain_sep_inv: "\domain_sep_inv irqs st and valid_objs and valid_mdb\ @@ -918,8 +857,9 @@ lemma receive_ipc_domain_sep_inv: done lemma send_fault_ipc_domain_sep_inv: - "\domain_sep_inv irqs st and valid_objs and sym_refs \ state_refs_of - and valid_mdb and K (valid_fault fault)\ + "\domain_sep_inv irqs st and valid_objs and valid_mdb + and sym_refs \ state_refs_of + and K (valid_fault fault)\ send_fault_ipc thread fault \\_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\" unfolding send_fault_ipc_def @@ -1035,7 +975,7 @@ lemma invoke_domain_domain_set_inv: done -context DomainSepInv_2 begin +context DomainSepInv_1 begin lemma invoke_tcb_domain_sep_inv: "\domain_sep_inv irqs st and tcb_inv_wf tinv\ @@ -1060,6 +1000,70 @@ lemma invoke_tcb_domain_sep_inv: del: set_priority_extended.dxo_eq)+ done +end + + +locale DomainSepInv_2 = DomainSepInv_1 state_ext_t + for state_ext_t :: "'state_ext :: state_ext itself" + + assumes arch_perform_invocation_domain_sep_inv[wp]: + "\domain_sep_inv irqs st and valid_arch_inv ai\ + arch_perform_invocation ai + \\_ s :: det_ext state. domain_sep_inv irqs st s\" + and arch_invoke_irq_handler_domain_sep_inv[wp]: + "arch_invoke_irq_handler ihi \\s :: det_ext state. domain_sep_inv irqs st s\" + and arch_invoke_irq_control_domain_sep_inv: + "\domain_sep_inv irqs st and arch_irq_control_inv_valid ivk\ + arch_invoke_irq_control ivk + \\_ s :: det_ext state. domain_sep_inv irqs st s\" + and handle_hypervisor_fault_domain_sep_inv[wp]: + "\domain_sep_inv irqs st and valid_objs and valid_mdb and sym_refs \ state_refs_of\ + handle_hypervisor_fault t hf_t + \\_ s :: det_ext state. domain_sep_inv irqs st s\" + and handle_reserved_irq_domain_sep_inv[wp]: + "\domain_sep_inv irqs st and valid_objs and valid_mdb and sym_refs \ state_refs_of\ + handle_reserved_irq irq + \\_ s :: det_ext state. domain_sep_inv irqs (st :: 'state_ext state) s\" +begin + +(* when i is AckIRQ the preconditions here contradict each other, which + is why this lemma is true *) +lemma invoke_irq_handler_domain_sep_inv: + "\domain_sep_inv irqs st and irq_handler_inv_valid i\ + invoke_irq_handler i + \\_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\" + apply (case_tac i) + apply (wp cap_insert_domain_sep_inv' | simp)+ + apply (rename_tac irq cap cslot_ptr s) + apply (case_tac cap, simp_all add: domain_sep_inv_cap_def)[1] + apply (wp | clarsimp)+ + done + +(* similarly, the preconditions here tend to contradict one another *) +lemma invoke_control_domain_sep_inv: + "\domain_sep_inv irqs st and irq_control_inv_valid i\ + invoke_irq_control i + \\_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\" + including classic_wp_pre + apply (case_tac i) + apply (case_tac irqs) + apply (wp cap_insert_domain_sep_inv' | simp )+ + apply (simp add: set_irq_state_def, wp, simp) + apply (fastforce simp: domain_sep_inv_def domain_sep_inv_cap_def) + apply (fastforce simp: valid_def domain_sep_inv_def) + apply simp + apply (wp arch_invoke_irq_control_domain_sep_inv) + done + +lemma derive_cap_domain_sep_inv_cap: + "\\s. domain_sep_inv_cap irqs cap\ + derive_cap slot cap + \\rv s :: det_ext state. domain_sep_inv_cap irqs rv\,-" + apply (simp add: derive_cap_def) + apply (rule hoare_pre) + apply (wp | wpc | simp add: )+ + apply auto + done + lemma perform_invocation_domain_sep_inv': "\domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \ state_refs_of\ @@ -1150,7 +1154,8 @@ lemma domain_sep_inv_cur_thread_update[simp]: lemma (in is_extended') domain_sep_inv[wp]: "I (domain_sep_inv irqs st)" by (rule lift_inv, simp) -context DomainSepInv_2 begin +context DomainSepInv_2 +begin lemma handle_recv_domain_sep_inv: "\domain_sep_inv irqs st and invs\ @@ -1181,35 +1186,30 @@ lemma handle_event_domain_sep_inv: "\domain_sep_inv irqs st and invs and (\s. ev \ Interrupt \ ct_active s)\ handle_event ev \\_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\" - apply (case_tac ev, simp_all) - apply (rule hoare_pre) - apply (wpsimp wp: handle_send_domain_sep_inv handle_call_domain_sep_inv - handle_recv_domain_sep_inv handle_reply_domain_sep_inv hy_inv - | simp add: invs_valid_objs invs_mdb invs_sym_refs valid_fault_def)+ - apply (rule_tac E'="\rv s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state) \ - invs s \ valid_fault rv" - and Q="Q" and Q'=Q for Q - in hoare_strengthen_postE) - apply (wp | simp add: invs_valid_objs invs_mdb invs_sym_refs valid_fault_def | auto)+ - done + apply (case_tac ev) + by (wpsimp wp: handle_send_domain_sep_inv handle_call_domain_sep_inv + handle_recv_domain_sep_inv handle_reply_domain_sep_inv hy_inv + | strengthen invs_valid_objs invs_mdb invs_sym_refs + | simp add: valid_fault_def + | wp hoare_drop_imps)+ lemma schedule_domain_sep_inv: "(schedule :: (unit,det_ext) s_monad) \domain_sep_inv irqs (st :: 'state_ext state)\" - apply (simp add: schedule_def allActiveTCBs_def) - apply (wp add: guarded_switch_to_lift hoare_drop_imps - del: ethread_get_wp - | wpc | clarsimp simp: get_thread_state_def thread_get_def trans_state_update'[symmetric] - schedule_choose_new_thread_def)+ - done + unfolding schedule_def allActiveTCBs_def + by (wp add: guarded_switch_to_lift hoare_drop_imps + del: ethread_get_wp + | wpc | clarsimp simp: get_thread_state_def thread_get_def trans_state_update'[symmetric] + schedule_choose_new_thread_def)+ lemma call_kernel_domain_sep_inv: "\domain_sep_inv irqs st and invs and (\s. ev \ Interrupt \ ct_active s)\ call_kernel ev :: (unit,det_ext) s_monad \\_ s. domain_sep_inv irqs (st :: 'state_ext state) s\" - apply (simp add: call_kernel_def) - apply (wp handle_interrupt_domain_sep_inv handle_event_domain_sep_inv schedule_domain_sep_inv - | simp)+ - done + unfolding call_kernel_def + by (wpsimp wp: handle_event_domain_sep_inv schedule_domain_sep_inv + simp: if_fun_split + | strengthen invs_valid_objs invs_mdb invs_sym_refs + | wp hoare_drop_imps)+ end diff --git a/proof/access-control/Finalise_AC.thy b/proof/access-control/Finalise_AC.thy index 36f064cfa3..488311bb13 100644 --- a/proof/access-control/Finalise_AC.thy +++ b/proof/access-control/Finalise_AC.thy @@ -23,9 +23,7 @@ NB: the @{term is_subject} assumption is not appropriate for some of locale Finalise_AC_1 = fixes aag :: "'a PAS" assumes sbn_st_vrefs: - "\P. \(\s. P (state_vrefs s)) and pspace_aligned and valid_vspace_objs and valid_arch_state\ - set_bound_notification ref ntfn - \\_ s :: det_ext state. P (state_vrefs s)\" + "\P. set_bound_notification ref ntfn \\s :: det_ext state. P (state_vrefs s)\" and arch_finalise_cap_auth': "\pas_refined aag\ arch_finalise_cap acap final \\rv _. pas_cap_cur_auth aag (fst rv)\" and arch_finalise_cap_obj_refs: @@ -48,12 +46,12 @@ locale Finalise_AC_1 = and prepare_thread_delete_pas_refined[wp]: "prepare_thread_delete p \pas_refined aag\" and prepare_thread_delete_respects[wp]: - "prepare_thread_delete p \integrity aag X st\" + "\integrity aag X st and K (is_subject aag p)\ prepare_thread_delete p \\_. integrity aag X st\" and finalise_cap_replaceable: "\\s :: det_ext state. s \ cap \ x = is_final_cap' cap s \ valid_mdb s \ cte_wp_at ((=) cap) sl s \ valid_objs s \ sym_refs (state_refs_of s) \ (cap_irqs cap \ {} \ if_unsafe_then_cap s \ valid_global_refs s) \ - (is_arch_cap cap \ pspace_aligned s \ valid_vspace_objs s \ + (is_arch_cap cap \ pspace_aligned s \ pspace_distinct s \ valid_vspace_objs s \ valid_arch_state s \ valid_arch_caps s)\ finalise_cap cap x \\rv s. replaceable s sl (fst rv) cap\" @@ -62,12 +60,6 @@ locale Finalise_AC_1 = and K (pas_cap_cur_auth aag (ArchObjectCap acap))\ arch_finalise_cap acap final \\_. integrity aag X st\" - and arch_post_cap_deletion[wp]: - "arch_post_cap_deletion acap \\s :: det_ext state. pspace_aligned s\" - and arch_post_cap_deletion_valid_vspace_objs[wp]: - "arch_post_cap_deletion acap \\s :: det_ext state. valid_vspace_objs s\" - and arch_post_cap_deletion_valid_arch_state[wp]: - "arch_post_cap_deletion acap \\s :: det_ext state. valid_arch_state s\" begin lemma tcb_sched_action_dequeue_integrity': @@ -250,7 +242,7 @@ crunch fast_finalise context Finalise_AC_1 begin lemma sbn_pas_refined[wp]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and + "\pas_refined aag and K (case ntfn of None \ True | Some ntfn' \ \auth \ {Receive, Reset}. abs_has_auth_to aag auth t ntfn')\ set_bound_notification t ntfn @@ -264,52 +256,29 @@ lemma sbn_pas_refined[wp]: split: if_split_asm) lemma unbind_notification_pas_refined[wp]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ - unbind_notification tptr - \\_. pas_refined aag\" + "unbind_notification tptr \pas_refined aag\" apply (clarsimp simp: unbind_notification_def) apply (wp set_simple_ko_pas_refined hoare_drop_imps | wpc | simp)+ done lemma unbind_maybe_notification_pas_refined[wp]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ - unbind_maybe_notification nptr \\_. pas_refined aag\" + "unbind_maybe_notification nptr \pas_refined aag\" apply (clarsimp simp: unbind_maybe_notification_def) apply (wp set_simple_ko_pas_refined hoare_drop_imps | wpc | simp)+ done lemma cancel_all_ipc_pas_refined[wp]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ - cancel_all_ipc epptr - \\_. pas_refined aag\" + "cancel_all_ipc epptr \pas_refined aag\" apply (clarsimp simp: cancel_all_ipc_def get_ep_queue_def cong: endpoint.case_cong) - apply (rule_tac Q'="\_. pas_refined aag and pspace_aligned - and valid_vspace_objs - and valid_arch_state" - in hoare_strengthen_post) - apply (wpsimp wp: mapM_x_wp_inv set_thread_state_pas_refined get_simple_ko_wp)+ + apply (wpsimp wp: mapM_x_wp_inv set_thread_state_pas_refined get_simple_ko_wp)+ done lemma cancel_all_signals_pas_refined[wp]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and - valid_arch_state\ - cancel_all_signals ntfnptr - \\_. pas_refined aag\" + "cancel_all_signals ntfnptr \pas_refined aag\" apply (clarsimp simp: cancel_all_signals_def cong: ntfn.case_cong) - apply (rule_tac Q'="\_. pas_refined aag and pspace_aligned - and valid_vspace_objs - and valid_arch_state" - in hoare_strengthen_post) - apply (wpsimp wp: mapM_x_wp_inv set_thread_state_pas_refined get_simple_ko_wp)+ + apply (wpsimp wp: mapM_x_wp_inv set_thread_state_pas_refined get_simple_ko_wp)+ done -crunch unbind_maybe_notification, cancel_all_ipc, cancel_all_signals, - fast_finalise, blocked_cancel_ipc, cap_move - for pspace_aligned[wp]: pspace_aligned - and valid_vspace_objs[wp]: valid_vspace_objs - and valid_arch_state[wp]: valid_arch_state - (ignore: cap_move_ext tcb_sched_action reschedule_required wp: dxo_wp_weak mapM_x_inv_wp) - crunch cap_delete_one for pas_refined_transferable[wp_transferable]: "pas_refined aag" and pas_refined[wp, wp_not_transferable]: "pas_refined aag" @@ -368,12 +337,6 @@ lemma deleting_irq_handler_pas_refined[wp]: apply (fastforce simp: pas_refined_def irq_map_wellformed_aux_def) done -crunch suspend - for pspace_aligned[wp]: "\s :: det_ext state. pspace_aligned s" - and valid_vspace_objs[wp]: "\s :: det_ext state. valid_vspace_objs s" - and valid_arch_state[wp]: "\s :: det_ext state. valid_arch_state s" - (wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps simp: tcb_cap_cases_def) - crunch suspend for pas_refined[wp]: "pas_refined aag" @@ -541,7 +504,6 @@ lemma reply_cancel_ipc_respects[wp]: thread_set_not_state_valid_sched hoare_weak_lift_imp thread_set_cte_wp_at_trivial thread_set_pas_refined simp: ran_tcb_cap_cases)+ - apply (strengthen invs_psp_aligned invs_vspace_objs invs_arch_state, clarsimp) apply (rule conjI) apply (fastforce simp: cte_wp_at_caps_of_state intro:is_transferable.intros dest!: reply_cap_descends_from_master0) @@ -594,7 +556,6 @@ lemma suspend_respects[wp]: apply (rule hoare_conjI) apply (wp hoare_drop_imps)+ apply wpsimp+ - apply fastforce done end @@ -997,9 +958,7 @@ lemma set_eobject_integrity_autarch: done lemma cancel_badged_sends_pas_refined[wp]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ - cancel_badged_sends epptr badge - \\_. pas_refined aag\" + "cancel_badged_sends epptr badge \pas_refined aag\" unfolding cancel_badged_sends_def by (wpsimp simp: filterM_mapM wp: mapM_wp_inv set_thread_state_pas_refined get_simple_ko_wp) @@ -1015,8 +974,7 @@ lemma thread_set_pas_refined_triv_idleT: and st: "\tcb. P (tcb_state tcb) \ tcb_state (f tcb) = tcb_state tcb" and ba: "\tcb. Q (tcb_bound_notification tcb) \ tcb_bound_notification (f tcb) = tcb_bound_notification tcb" - shows "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and idle_tcb_at (\(st, ntfn, arch). P st \ Q ntfn \ R arch) t\ + shows "\pas_refined aag and idle_tcb_at (\(st, ntfn, arch). P st \ Q ntfn \ R arch) t\ thread_set f t \\_. pas_refined aag\" apply (simp add: pas_refined_def state_objs_to_policy_def) @@ -1026,10 +984,7 @@ lemma thread_set_pas_refined_triv_idleT: apply (wpsimp wp: set_object_wp) apply (clarsimp simp: pred_tcb_def2 fun_upd_def[symmetric] del: subsetI) - apply (subst state_vrefs_tcb_upd, fastforce+) - apply (clarsimp simp: tcb_at_def) - apply (subst state_vrefs_tcb_upd, fastforce+) - apply (clarsimp simp: tcb_at_def) + apply (subst state_vrefs_tcb_upd, clarsimp simp: tcb_at_def)+ apply (rule conjI) apply (erule_tac P="\ ts ba. auth_graph_map a (state_bits_to_policy cps ts ba cd vr) \ ag" for a cps cd vr ag in rsubst') diff --git a/proof/access-control/Interrupt_AC.thy b/proof/access-control/Interrupt_AC.thy index 42dee66806..19e434a611 100644 --- a/proof/access-control/Interrupt_AC.thy +++ b/proof/access-control/Interrupt_AC.thy @@ -30,8 +30,7 @@ lemma pas_refined_is_subject_irqD: locale Interrupt_AC_1 = fixes arch_authorised_irq_ctl_inv :: "'a PAS \ arch_irq_control_invocation \ bool" assumes arch_invoke_irq_control_pas_refined: - "\pas_refined (aag :: 'a PAS) 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 :: 'a PAS) 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\" @@ -59,8 +58,7 @@ definition authorised_irq_ctl_inv :: "'a PAS \ Invocations_A.irq_con | ArchIRQControl acinv \ arch_authorised_irq_ctl_inv aag acinv" lemma invoke_irq_control_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and valid_mdb and irq_control_inv_valid irq_ctl_inv + "\pas_refined aag and valid_mdb and irq_control_inv_valid irq_ctl_inv and K (authorised_irq_ctl_inv aag irq_ctl_inv)\ invoke_irq_control irq_ctl_inv \\_. pas_refined aag\" diff --git a/proof/access-control/Ipc_AC.thy b/proof/access-control/Ipc_AC.thy index eb7a8cc056..4289021a27 100644 --- a/proof/access-control/Ipc_AC.thy +++ b/proof/access-control/Ipc_AC.thy @@ -67,15 +67,13 @@ crunch possible_switch_to for tcb_domain_map_wellformed[wp]: "tcb_domain_map_wellformed aag" lemma update_waiting_ntfn_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and ko_at (Notification ntfn) ntfnptr and K (ntfn_obj ntfn = WaitingNtfn queue)\ + "\pas_refined aag and ko_at (Notification ntfn) ntfnptr and K (ntfn_obj ntfn = WaitingNtfn queue)\ update_waiting_ntfn ntfnptr queue badge val \\_. pas_refined aag\" by (wpsimp wp: set_thread_state_pas_refined set_simple_ko_pas_refined simp: update_waiting_ntfn_def) lemma cancel_ipc_receive_blocked_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs - and valid_arch_state and st_tcb_at receive_blocked t\ + "\pas_refined aag and st_tcb_at receive_blocked t\ cancel_ipc t \\_. pas_refined aag\" apply (clarsimp simp: cancel_ipc_def) @@ -85,9 +83,7 @@ lemma cancel_ipc_receive_blocked_pas_refined: done lemma send_signal_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ - send_signal ntfnptr badge - \\_. pas_refined aag\" + "send_signal ntfnptr badge \pas_refined aag\" apply (simp add: send_signal_def) apply (rule bind_wp[OF _ get_simple_ko_sp]) apply (wpsimp wp: set_simple_ko_pas_refined update_waiting_ntfn_pas_refined gts_wp @@ -96,8 +92,7 @@ lemma send_signal_pas_refined: done lemma receive_signal_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and K (\ntfnptr \ obj_refs_ac cap. abs_has_auth_to aag Receive thread ntfnptr)\ + "\pas_refined aag and K (\ntfnptr \ obj_refs_ac cap. abs_has_auth_to aag Receive thread ntfnptr)\ receive_signal thread cap is_blocking \\_. pas_refined aag\" apply (simp add: receive_signal_def) @@ -172,9 +167,6 @@ locale Ipc_AC_1 = "\P. make_fault_msg ft t \\s :: det_ext state. P s\" and tcb_context_no_change: "\ctxt. (tcb :: tcb) = tcb\tcb_arch := arch_tcb_context_set ctxt (tcb_arch tcb)\" - (* This assumption excludes x64 (its valid_arch_state includes caps) *) - and transfer_caps_loop_valid_arch[wp]: - "transfer_caps_loop ep buffer n caps slots mi \valid_arch_state :: det_ext state \ _\" begin lemma send_upd_ctxintegrity: @@ -736,8 +728,7 @@ lemma derive_cap_is_derived_foo': lemma transfer_caps_loop_presM_extended: fixes P vo em ex buffer slots caps n mi assumes x: "\cap src dest. - \\s. P s \ (vo \ pspace_aligned s \ valid_vspace_objs s \ valid_arch_state s - \ valid_objs s \ valid_mdb s \ real_cte_at dest s + \\s. P s \ (vo \ valid_objs s \ valid_mdb s \ real_cte_at dest s \ s \ cap \ Psrc src \ Pdest dest \ Pcap cap \ tcb_cap_valid cap dest s \ real_cte_at src s \ cte_wp_at (is_derived (cdt s) src cap) src s @@ -748,8 +739,7 @@ lemma transfer_caps_loop_presM_extended: \\_ s :: det_ext state. P s\" assumes eb: "\b n. set_extra_badge buffer b n \P\" assumes pcap_auth_derived: "\cap cap'. \ auth_derived cap cap'; Pcap cap' \ \ Pcap cap" - shows "\\s. P s \ (vo \ pspace_aligned s \ valid_vspace_objs s \ valid_arch_state s - \ valid_objs s \ valid_mdb s \ distinct slots + shows "\\s. P s \ (vo \ valid_objs s \ valid_mdb s \ distinct slots \ (\x \ set slots. cte_wp_at (\cap. cap = NullCap) x s \ real_cte_at x s \ Pdest x) \ (\x \ set caps. valid_cap (fst x) s \ Psrc (snd x) \ Pcap (fst x) @@ -807,8 +797,7 @@ lemma transfer_caps_loop_presM_extended: by (clarsimp simp: masked_as_full_def is_cap_simps split: if_splits)+ lemma transfer_caps_loop_pas_refined: - "\\s. pas_refined aag s \ pspace_aligned s \ valid_vspace_objs s \ - valid_arch_state s \ valid_objs s \ valid_mdb s \ + "\\s. pas_refined aag s \ valid_objs s \ valid_mdb s \ (\x \ set caps. valid_cap (fst x) s \ real_cte_at (snd x) s \ cte_wp_at (\cp. fst x \ NullCap \ cp = fst x) (snd x) s) \ (\x\set slots. real_cte_at x s \ cte_wp_at (\cap. cap = NullCap) x s) \ @@ -831,8 +820,7 @@ lemma transfer_caps_loop_pas_refined: done lemma transfer_caps_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs - and valid_arch_state and valid_objs and valid_mdb + "\pas_refined aag and valid_objs and valid_mdb and (\s. (\x \ set caps. valid_cap (fst x) s \ cte_wp_at (\cp. fst x \ NullCap \ cp = fst x) (snd x) s \ real_cte_at (snd x) s)) @@ -849,16 +837,9 @@ lemma transfer_caps_pas_refined: end lemma copy_mrs_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ - copy_mrs sender sbuf receiver rbuf n - \\_. pas_refined aag\" + "copy_mrs sender sbuf receiver rbuf n \pas_refined aag\" unfolding copy_mrs_def - apply (rule_tac Q'="\_. pas_refined aag and pspace_aligned - and valid_vspace_objs - and valid_arch_state" - in hoare_strengthen_post[rotated], clarsimp) - apply (wpsimp wp: mapM_wp_inv) - done + by (wpsimp wp: mapM_wp_inv) lemma lookup_cap_and_slot_authorised: "\pas_refined aag and K (is_subject aag thread)\ @@ -916,13 +897,8 @@ context Ipc_AC_1 begin crunch do_fault_transfer for pas_refined[wp]: "\s :: det_ext state. pas_refined aag s" -crunch transfer_caps, copy_mrs - for valid_arch_state[wp]: "valid_arch_state :: det_ext state \ _" - (wp: crunch_wps) - lemma do_normal_transfer_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and valid_objs and valid_mdb + "\pas_refined aag and valid_objs and valid_mdb and K (grant \ is_subject aag sender) and K (grant \ is_subject aag receiver)\ do_normal_transfer sender sbuf endpoint badge grant receiver rbuf @@ -945,8 +921,7 @@ next qed lemma do_ipc_transfer_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and valid_objs and valid_mdb + "\pas_refined aag and valid_objs and valid_mdb and K (grant \ is_subject aag sender) and K (grant \ is_subject aag receiver)\ do_ipc_transfer sender ep badge grant receiver @@ -959,7 +934,7 @@ end (* FIXME MOVE*) lemma cap_insert_pas_refined_transferable: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and + "\pas_refined aag and valid_mdb and K (is_transferable_cap new_cap \ aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap \ abs_has_auth_to aag DeleteDerived (fst src_slot) (fst dest_slot))\ cap_insert new_cap src_slot dest_slot @@ -982,7 +957,7 @@ lemma cap_insert_pas_refined_transferable: intro: aag_wellformed_delete_derived_trans[OF _ _ pas_refined_wellformed]) lemma setup_caller_cap_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and + "\pas_refined aag and valid_mdb and K ((grant \ is_subject aag sender \ is_subject aag receiver) \ abs_has_auth_to aag Reply receiver sender)\ setup_caller_cap sender receiver grant @@ -1061,12 +1036,11 @@ lemma send_ipc_pas_refined: apply (wpc | wp set_thread_state_pas_refined)+ apply (simp add: hoare_if_r_and split del:if_split) apply (wp setup_caller_cap_pas_refined set_thread_state_pas_refined)+ - apply (simp split del:if_split) - apply (rule_tac Q'="\rv. pas_refined aag and pspace_aligned and valid_vspace_objs and - valid_arch_state and valid_mdb and - K (can_grant \ can_grant_reply - \ (reply_can_grant \ is_subject aag x21) \ - (pasObjectAbs aag x21, Reply, pasSubject aag) \ pasPolicy aag)" + apply (simp split del: if_split) + apply (rule_tac Q'="\rv. pas_refined aag and valid_mdb and + K (can_grant \ can_grant_reply + \ (reply_can_grant \ is_subject aag x21) \ + (pasObjectAbs aag x21, Reply, pasSubject aag) \ pasPolicy aag)" in hoare_strengthen_post[rotated]) apply simp apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined hoare_weak_lift_imp gts_wp @@ -1180,8 +1154,7 @@ lemma receive_ipc_sender_can_grant_helper: done lemma complete_signal_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and bound_tcb_at ((=) (Some ntfnptr)) thread\ + "\pas_refined aag and bound_tcb_at ((=) (Some ntfnptr)) thread\ complete_signal ntfnptr thread \\_. pas_refined aag\" apply (simp add: complete_signal_def) @@ -1207,8 +1180,7 @@ lemma receive_ipc_base_pas_refined: apply (wp set_thread_state_pas_refined get_simple_ko_wp setup_caller_cap_pas_refined | wpc | simp add: thread_get_def do_nbrecv_failed_transfer_def split del: if_split)+ apply (rename_tac list sss data) - apply (rule_tac Q'="\rv s. pas_refined aag s \ pspace_aligned s \ valid_vspace_objs s \ - valid_arch_state s \ valid_mdb s \ + apply (rule_tac Q'="\rv s. pas_refined aag s \ valid_mdb s \ (sender_can_grant data \ is_subject aag (hd list)) \ (sender_can_grant_reply data \ (AllowGrant \ rights \ is_subject aag (hd list)) \ @@ -1286,7 +1258,6 @@ lemma receive_ipc_pas_refined: apply (rule bind_wp[OF _ get_simple_ko_sp]) apply (case_tac "isActive ntfn", simp_all) apply (wp complete_signal_pas_refined, clarsimp) - apply fastforce (* regular case again *) apply (rule hoare_pre, wp receive_ipc_base_pas_refined) apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def) @@ -1365,8 +1336,7 @@ lemma transfer_caps_integrity_autarch: lemma do_normal_transfer_send_integrity_autarch: notes lec_valid_cap[wp del] shows - "\pas_refined aag and integrity aag X st and pspace_aligned and - valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and + "\pas_refined aag and integrity aag X st and valid_objs and valid_mdb and K (is_subject aag receiver \ ipc_buffer_has_auth aag receiver rbuf \ (grant \ is_subject aag sender))\ do_normal_transfer sender sbuf endpoint badge grant receiver rbuf @@ -1390,8 +1360,7 @@ lemma do_fault_transfer_integrity_autarch: set_mrs_integrity_autarch thread_get_wp') lemma do_ipc_transfer_integrity_autarch: - "\pas_refined aag and integrity aag X st and - pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and + "\pas_refined aag and integrity aag X st and valid_objs and valid_mdb and K (is_subject aag receiver \ (grant \ is_subject aag sender))\ do_ipc_transfer sender ep badge grant receiver \\_. integrity aag X st\" @@ -1768,12 +1737,6 @@ locale Ipc_AC_2 = Ipc_AC_1 + and handle_arch_fault_reply_integrity_tcb_in_fault_reply_TRFContext[wp]: "handle_arch_fault_reply vmf thread x y \integrity_tcb_in_fault_reply aag X thread TRFContext st\" - and handle_arch_fault_reply_pspace_aligned[wp]: - "handle_arch_fault_reply vmf thread x y \\s :: det_ext state. pspace_aligned s\" - and handle_arch_fault_reply_valid_vspace_objs[wp]: - "handle_arch_fault_reply vmf thread x y \\s :: det_ext state. valid_vspace_objs s\" - and handle_arch_fault_reply_valid_arch_state[wp]: - "handle_arch_fault_reply vmf thread x y \\s :: det_ext state. valid_arch_state s\" and cap_insert_ext_integrity_asids_in_ipc[wp]: "cap_insert_ext src_parent src_slot dest_slot src_p dest_p \\s. integrity_asids aag subjects x asid st @@ -2072,8 +2035,7 @@ lemma do_normal_transfer_respects_in_ipc: notes lec_valid_cap[wp del] shows "\integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and - pspace_aligned and valid_vspace_objs and valid_arch_state and -valid_objs and valid_mdb and st_tcb_at can_receive_ipc receiver and + valid_objs and valid_mdb and st_tcb_at can_receive_ipc receiver and (\s. grant \ is_subject aag sender \ is_subject aag receiver) and K ((\ is_subject aag receiver \ (case recv_buf of None \ True | Some buf' \ auth_ipc_buffers st receiver = @@ -2105,7 +2067,6 @@ lemma do_fault_transfer_respects_in_ipc: lemma do_ipc_transfer_respects_in_ipc: "\integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and - pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and st_tcb_at can_receive_ipc receiver and (\s. grant \ is_subject aag sender \ is_subject aag receiver)\ do_ipc_transfer sender epopt badge grant receiver @@ -2330,7 +2291,7 @@ lemma setup_caller_cap_respects_in_ipc_reply: by (wpsimp wp: cap_insert_reply_cap_respects_in_ipc set_thread_state_respects_in_ipc_autarch) lemma send_ipc_integrity_autarch: - "\integrity aag X st and pas_refined aag and invs and is_subject aag \ cur_thread and + "\integrity aag X st and pas_refined aag and invs and obj_at (\ep. can_grant \ (\r \ refs_of ep. snd r = EPRecv \ is_subject aag (fst r))) epptr and K (is_subject aag sender \ aag_has_auth_to aag SyncSend epptr \ (can_grant_reply \ aag_has_auth_to aag Call epptr))\ @@ -2409,15 +2370,13 @@ lemma valid_tcb_fault_update: context Ipc_AC_2 begin lemma thread_set_fault_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ + "\pas_refined aag\ thread_set (tcb_fault_update (\_. Some fault)) thread \\_. pas_refined aag\" - by (wpsimp wp: send_ipc_pas_refined thread_set_pas_refined - thread_set_refs_trivial thread_set_obj_at_impossible) + by (wpsimp wp: thread_set_pas_refined) lemma send_fault_ipc_pas_refined: - "\pas_refined aag and invs and is_subject aag \ cur_thread - and K (valid_fault fault) and K (is_subject aag thread)\ + "\pas_refined aag and invs and K (valid_fault fault) and K (is_subject aag thread)\ send_fault_ipc thread fault \\_. pas_refined aag\" apply (rule hoare_gen_asm)+ @@ -2426,8 +2385,7 @@ lemma send_fault_ipc_pas_refined: thread_set_refs_trivial thread_set_obj_at_impossible get_cap_wp thread_set_valid_objs'' hoare_vcg_conj_lift hoare_vcg_ex_lift hoare_vcg_all_lift simp: split_def) - apply (rule_tac Q'="\rv s. pas_refined aag s \ is_subject aag (cur_thread s) \ - invs s \ valid_fault fault \ is_subject aag (fst (fst rv))" + apply (rule_tac Q'="\rv s. pas_refined aag s \ invs s \ valid_fault fault \ is_subject aag (fst (fst rv))" in hoare_strengthen_postE_R[rotated]) apply (fastforce dest!: cap_auth_caps_of_state simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state aag_cap_auth_def @@ -2437,8 +2395,7 @@ lemma send_fault_ipc_pas_refined: done lemma handle_fault_pas_refined: - "\pas_refined aag and invs and is_subject aag \ cur_thread - and K (valid_fault fault) and K (is_subject aag thread)\ + "\pas_refined aag and invs and K (valid_fault fault) and K (is_subject aag thread)\ handle_fault thread fault \\_. pas_refined aag\" apply (wpsimp wp: set_thread_state_pas_refined simp: handle_fault_def handle_double_fault_def) @@ -2449,7 +2406,6 @@ lemma handle_fault_pas_refined: apply (rule hoare_strengthen_postE[where E'=E and E=E for E]) apply (rule valid_validE) apply (wpsimp wp: send_fault_ipc_pas_refined)+ - apply fastforce done end @@ -2471,7 +2427,7 @@ lemma obj_at_conj_distrib: context Ipc_AC_2 begin lemma send_fault_ipc_integrity_autarch: - "\pas_refined aag and invs and integrity aag X st and is_subject aag \ cur_thread + "\pas_refined aag and invs and integrity aag X st and K (valid_fault fault) and K (is_subject aag thread)\ send_fault_ipc thread fault \\_. integrity aag X st\" @@ -2492,7 +2448,6 @@ lemma send_fault_ipc_integrity_autarch: apply (rule_tac Q'="\rv s. integrity aag X st s \ pas_refined aag s \ invs s \ valid_fault fault - \ is_subject aag (cur_thread s) \ is_subject aag (fst (fst rv))" in hoare_strengthen_postE_R[rotated]) apply (clarsimp simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state obj_at_def) @@ -2512,7 +2467,7 @@ lemma send_fault_ipc_integrity_autarch: done lemma handle_fault_integrity_autarch: - "\pas_refined aag and integrity aag X st and is_subject aag \ cur_thread and invs + "\integrity aag X st and pas_refined aag and invs and K (valid_fault fault) and K (is_subject aag thread)\ handle_fault thread fault \\_. integrity aag X st\" @@ -2533,12 +2488,6 @@ lemma tcb_st_to_auth_Restart_Inactive [simp]: context Ipc_AC_2 begin -crunch handle_fault_reply - for pspace_aligned[wp]: "\s :: det_ext state. pspace_aligned s" - and valid_vspace_objs[wp]: "\s :: det_ext state. valid_vspace_objs s" - and valid_arch_state[wp]: "\s :: det_ext state. valid_arch_state s" - (wp: arch_get_sanitise_register_info_inv) - lemma do_reply_transfer_pas_refined: "\pas_refined aag and invs and K (is_subject aag sender) and K ((grant \ is_subject aag receiver) \ is_subject aag (fst slot))\ diff --git a/proof/access-control/RISCV64/ArchArch_AC.thy b/proof/access-control/RISCV64/ArchArch_AC.thy index 4519236a7b..90075ebf16 100644 --- a/proof/access-control/RISCV64/ArchArch_AC.thy +++ b/proof/access-control/RISCV64/ArchArch_AC.thy @@ -19,20 +19,13 @@ context Arch begin global_naming RISCV64 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))\ - set_mrs thread buf msgs - \\_ 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]: @@ -503,11 +496,9 @@ 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 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)+ diff --git a/proof/access-control/RISCV64/ArchCNode_AC.thy b/proof/access-control/RISCV64/ArchCNode_AC.thy index 39053ab651..38662c773e 100644 --- a/proof/access-control/RISCV64/ArchCNode_AC.thy +++ b/proof/access-control/RISCV64/ArchCNode_AC.thy @@ -56,29 +56,28 @@ lemma sata_update2[CNode_AC_assms]: simp: cap_links_asid_slot_def label_owns_asid_slot_def split: if_split_asm) +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 vspace_for_pool_def + split: option.splits) + 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 + assumes "asid_table s' = asid_table s" + and "aobjs_of s' = aobjs_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 by (auto simp: vspace_for_pool_def state_vrefs_def) 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 @@ -100,14 +99,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)+ diff --git a/proof/access-control/RISCV64/ArchDomainSepInv.thy b/proof/access-control/RISCV64/ArchDomainSepInv.thy index 6d295b84e4..f749c22af8 100644 --- a/proof/access-control/RISCV64/ArchDomainSepInv.thy +++ b/proof/access-control/RISCV64/ArchDomainSepInv.thy @@ -25,6 +25,26 @@ 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 +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) + +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 + +declare init_arch_objects_inv[DomainSepInv_assms] + end @@ -32,21 +52,12 @@ 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 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) - lemma perform_page_invocation_domain_sep_inv: "\domain_sep_inv irqs st and valid_page_inv pgi\ perform_page_invocation pgi @@ -112,15 +123,6 @@ 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 - -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 - end @@ -128,7 +130,7 @@ global_interpretation DomainSepInv_2?: DomainSepInv_2 proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; fact DomainSepInv_assms) + by (unfold_locales; wpsimp wp: DomainSepInv_assms) qed end diff --git a/proof/access-control/RISCV64/ArchFinalise_AC.thy b/proof/access-control/RISCV64/ArchFinalise_AC.thy index c523ccf513..7c769a04cd 100644 --- a/proof/access-control/RISCV64/ArchFinalise_AC.thy +++ b/proof/access-control/RISCV64/ArchFinalise_AC.thy @@ -111,9 +111,7 @@ crunch prepare_thread_delete for respects[Finalise_AC_assms, wp]: "integrity aag X st" 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) @@ -216,7 +214,7 @@ lemma delete_asid_respects: apply (clarsimp simp: pas_refined_refl obj_at_def asid_pool_integrity_def) done -lemma arch_finalise_cap_respects[wp]: +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 @@ -229,10 +227,11 @@ lemma arch_finalise_cap_respects[wp]: 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 arch_finalise_cap_pas_refined[Finalise_AC_assms] +declare prepare_thread_delete_pas_refined[Finalise_AC_assms] +declare finalise_cap_replaceable[Finalise_AC_assms] end @@ -241,7 +240,7 @@ 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; wpsimp wp: Finalise_AC_assms) qed diff --git a/proof/access-control/RISCV64/ArchInterrupt_AC.thy b/proof/access-control/RISCV64/ArchInterrupt_AC.thy index 09ff7a783c..938d3bc052 100644 --- a/proof/access-control/RISCV64/ArchInterrupt_AC.thy +++ b/proof/access-control/RISCV64/ArchInterrupt_AC.thy @@ -21,8 +21,7 @@ definition arch_authorised_irq_ctl_inv :: (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\" diff --git a/proof/access-control/RISCV64/ArchIpc_AC.thy b/proof/access-control/RISCV64/ArchIpc_AC.thy index 211262fde4..30a9994e71 100644 --- a/proof/access-control/RISCV64/ArchIpc_AC.thy +++ b/proof/access-control/RISCV64/ArchIpc_AC.thy @@ -188,11 +188,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 diff --git a/proof/access-control/RISCV64/ArchSyscall_AC.thy b/proof/access-control/RISCV64/ArchSyscall_AC.thy index e9c7f0ee17..e8db944cac 100644 --- a/proof/access-control/RISCV64/ArchSyscall_AC.thy +++ b/proof/access-control/RISCV64/ArchSyscall_AC.thy @@ -160,6 +160,7 @@ crunch \ \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 init_arch_objects_inv[Syscall_AC_assms] end @@ -168,7 +169,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; wpsimp wp: Syscall_AC_assms) qed end diff --git a/proof/access-control/Retype_AC.thy b/proof/access-control/Retype_AC.thy index b81ad611ab..c432e6910b 100644 --- a/proof/access-control/Retype_AC.thy +++ b/proof/access-control/Retype_AC.thy @@ -373,7 +373,7 @@ lemma obj_refs_default': by (cases tp; auto simp: ptr_range_memI obj_bits_api_def dest: rev_subsetD[OF _ aobj_refs'_default']) lemma create_cap_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and + "\pas_refined aag and K (tp \ ArchObject ASIDPoolObj \ is_subject aag (fst p) \ is_subject aag (fst (fst ref)) \ (\x \ ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x) \ is_aligned (snd ref) (obj_bits_api tp sz))\ @@ -787,28 +787,6 @@ lemma set_free_index_invs': apply (fastforce simp: cte_wp_at_def) done -lemma delete_objects_pspace_no_overlap: - "\pspace_aligned and valid_objs and cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\ - delete_objects ptr sz - \\_. pspace_no_overlap_range_cover ptr sz\" - unfolding delete_objects_def do_machine_op_def - apply (wp | simp add: split_def detype_machine_state_update_comm)+ - apply clarsimp - apply (rule pspace_no_overlap_detype) - apply (auto dest: cte_wp_at_valid_objs_valid_cap) - done - -lemma delete_objects_pspace_no_overlap': - "\pspace_aligned and valid_objs and cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\ - delete_objects ptr sz - \\_. pspace_no_overlap_range_cover (ptr && ~~ mask sz) sz\" - apply (clarsimp simp: valid_def) - apply (frule untyped_cap_aligned, simp) - apply (clarsimp) - apply (frule(1) cte_wp_at_valid_objs_valid_cap) - apply (erule use_valid, wp delete_objects_pspace_no_overlap, auto) - done - (* FIXME: move *) lemma valid_cap_range_untyped: "\ valid_objs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s \ @@ -924,22 +902,6 @@ lemma delete_objects_pas_refined: apply simp done -lemma delete_objects_pspace_aligned[wp]: - "delete_objects ptr sz \pspace_aligned\" - unfolding delete_objects_def do_machine_op_def - apply (wp | simp add: split_def detype_machine_state_update_comm)+ - apply clarsimp - apply (auto simp add: detype_def pspace_aligned_def) - done - -lemma reset_untyped_cap_pspace_aligned[wp]: - "reset_untyped_cap slot \pspace_aligned\" - apply (clarsimp simp: reset_untyped_cap_def) - apply (wpsimp wp: mapME_x_inv_wp ) - apply (rule valid_validE) - apply (wpsimp wp: preemption_point_inv dxo_wp_weak hoare_drop_imps)+ - done - lemma valid_vspace_objs_detype: assumes "invs s" assumes "cte_wp_at (\c. is_untyped_cap c \ descendants_range c ptr s @@ -1028,8 +990,7 @@ lemma reset_untyped_cap_pas_refined[wp]: apply (wps | wp set_cap_pas_refined_not_transferable | simp add: unless_def)+ apply (rule valid_validE) apply (rule_tac P="is_untyped_cap cap \ pas_cap_cur_auth aag cap" in hoare_gen_asm) - apply (rule_tac Q'="\_. cte_wp_at (\ c. \ is_transferable (Some c)) slot and pas_refined aag and - pspace_aligned and valid_vspace_objs and valid_arch_state" + apply (rule_tac Q'="\_. cte_wp_at (\ c. \ is_transferable (Some c)) slot and pas_refined aag" in hoare_strengthen_post) apply (rule validE_valid, rule mapME_x_inv_wp) apply (rule hoare_pre) @@ -1046,7 +1007,6 @@ lemma reset_untyped_cap_pas_refined[wp]: apply (fastforce simp: cte_wp_at_caps_of_state)+ apply (cases slot) apply (auto elim: caps_pas_cap_cur_auth_UntypedCap_idx_dev) - apply (fastforce simp: bits_of_def is_cap_simps)+ done lemma invoke_untyped_pas_refined: @@ -1056,9 +1016,8 @@ lemma invoke_untyped_pas_refined: \\_. pas_refined aag\" apply (rule hoare_gen_asm) apply (rule hoare_pre) - apply (rule_tac Q'="\_. pas_refined aag and pspace_aligned and valid_vspace_objs - and valid_arch_state and pas_cur_domain aag" in hoare_strengthen_post) - apply (rule invoke_untyped_Q) + apply (rule_tac Q'="\_. pas_refined aag and pas_cur_domain aag" in hoare_strengthen_post) + apply (rule invoke_untyped_Q) apply (rule hoare_pre, wp create_cap_pas_refined) apply (clarsimp simp: authorised_untyped_inv_def range_cover.aligned ptr_range_def[symmetric] @@ -1074,31 +1033,20 @@ lemma invoke_untyped_pas_refined: | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+ apply (clarsimp simp: retype_addrs_aligned_range_cover cte_wp_at_caps_of_state) - apply (rule context_conjI, clarsimp) - apply (drule valid_global_refsD[rotated 2]) - apply (clarsimp simp: post_retype_invs_def split: if_split_asm) - apply (erule caps_of_state_cteD) - apply (erule notE, erule subsetD[rotated]) - apply (rule order_trans, erule retype_addrs_subset_ptr_bits) - apply (simp add: field_simps word_and_le2) - apply blast + apply (drule valid_global_refsD[rotated 2]) + apply (clarsimp simp: post_retype_invs_def split: if_split_asm) + apply (erule caps_of_state_cteD) + apply (erule notE, erule subsetD[rotated]) + apply (rule order_trans, erule retype_addrs_subset_ptr_bits) + apply (simp add: field_simps word_and_le2) apply (rule hoare_name_pre_state, clarsimp) apply (rule hoare_pre, wp retype_region_pas_refined) - apply (rule_tac Q'="\rv. post_retype_invs tp rv and pas_cur_domain aag" in hoare_strengthen_post) - apply (wp retype_region_post_retype_invs_spec) - apply (clarsimp simp: post_retype_invs_def invs_def valid_state_def valid_pspace_def split: if_splits) apply (clarsimp simp: authorised_untyped_inv_def) apply (strengthen range_cover_le[mk_strg I E], simp) - apply (intro conjI) - apply (intro conjI exI; - (erule cte_wp_at_weakenE)?, - clarsimp simp: field_simps word_and_le2) - apply (clarsimp simp: cte_wp_at_caps_of_state) - apply (erule caps_region_kernel_window_imp) - apply clarsimp - apply clarsimp - apply (fastforce simp: word_and_le2) - apply (fastforce simp: cte_wp_at_caps_of_state) + apply (intro conjI exI; + (erule cte_wp_at_weakenE)?, + clarsimp simp: field_simps word_and_le2) + apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule hoare_pre, wp set_cap_pas_refined) apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) apply (cases ui, diff --git a/proof/access-control/Syscall_AC.thy b/proof/access-control/Syscall_AC.thy index ad13ff9fb8..82963b0fb8 100644 --- a/proof/access-control/Syscall_AC.thy +++ b/proof/access-control/Syscall_AC.thy @@ -371,7 +371,6 @@ lemma handle_recv_integrity: apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def valid_fault_def) apply wpsimp+ - apply fastforce done lemma handle_reply_pas_refined[wp]: @@ -469,30 +468,42 @@ locale Syscall_AC_1 = "Syscall_AC_wps (arch_activate_idle_thread t) aag" and arch_mask_irq_signal_integrity[simp]: "Syscall_AC_wps (arch_mask_irq_signal irq) aag" - and handle_reserved_irq_integrity[simp]: - "Syscall_AC_wps (handle_reserved_irq irq) aag" - and handle_hypervisor_fault_integrity[simp]: - "Syscall_AC_wps (handle_hypervisor_fault t hf_t) aag" and arch_switch_to_idle_thread_pas_refined[wp]: "arch_switch_to_idle_thread \pas_refined aag\" and arch_activate_idle_thread_pas_refined[wp]: "arch_activate_idle_thread t \pas_refined aag\" and arch_mask_irq_signal_pas_refined[wp]: "arch_mask_irq_signal irq \pas_refined aag\" - and handle_reserved_irq_pas_refined[wp]: - "handle_reserved_irq irq \pas_refined aag\" - and handle_hypervisor_fault_pas_refined[wp]: - "handle_hypervisor_fault t hf_t \pas_refined aag\" + and arch_mask_irq_signal_pas_cur_domain: + "arch_mask_irq_signal irq \pas_cur_domain aag\" + and handle_reserved_irq_integrity_autarch: + "\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\" + and handle_reserved_irq_integrity_idle: + "\integrity aag X st and invs and ct_idle\ + handle_reserved_irq irq + \\_. integrity aag X st\" + and handle_reserved_irq_pas_refined: + "\\s. pas_refined aag s \ invs s \ (ct_active s \ is_subject aag (cur_thread s))\ + handle_reserved_irq irq \\_. pas_refined aag\" + and handle_reserved_irq_pas_cur_domain: + "handle_reserved_irq irq \pas_cur_domain aag\" + and handle_hypervisor_fault_integrity_autarch: + "\\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\" + and handle_hypervisor_fault_pas_refined: + "\\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\" and handle_vm_fault_integrity: "\integrity aag X st and K (is_subject aag thread)\ handle_vm_fault thread vmfault_type \\rv. integrity aag X st\" and handle_vm_fault_pas_refined[wp]: "handle_vm_fault t vmf_t \pas_refined aag\" - and arch_mask_irq_signal_pas_cur_domain: - "arch_mask_irq_signal irq \pas_cur_domain aag\" - and handle_reserved_irq_pas_cur_domain: - "handle_reserved_irq irq \pas_cur_domain aag\" and ackInterrupt_underlying_memory_inv[wp]: "\P. ackInterrupt irq \\s. P (underlying_memory s)\" and resetTimer_underlying_memory_inv[wp]: @@ -555,20 +566,17 @@ sublocale Syscall_AC_1 \ arch_activate_idle_thread: Syscall_AC_wps "ar by simp sublocale Syscall_AC_1 \ arch_mask_irq_signal: Syscall_AC_wps "arch_mask_irq_signal irq" aag by simp -sublocale Syscall_AC_1 \ handle_reserved_irq: Syscall_AC_wps "handle_reserved_irq irq" aag - by simp -sublocale Syscall_AC_1 \ handle_hypervisor_fault: Syscall_AC_wps "handle_hypervisor_fault t hf_t" aag - by simp context Syscall_AC_1 begin lemma handle_interrupt_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ - handle_interrupt irq \\_. pas_refined aag\" + "\pas_refined aag and invs and (\s. ct_active s \ is_subject aag (cur_thread s))\ + handle_interrupt irq + \\_. pas_refined aag\" apply (simp add: handle_interrupt_def) apply (rule conjI; rule impI;rule hoare_pre) - apply (wp send_signal_pas_refined get_cap_wp + apply (wp send_signal_pas_refined get_cap_wp handle_reserved_irq_pas_refined | wpc | simp add: get_irq_slot_def get_irq_state_def )+ done @@ -589,23 +597,6 @@ lemma timer_tick_integrity[wp]: apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def) done -lemma handle_interrupt_integrity_autarch: - "\integrity aag X st and pas_refined aag and invs - and (\s. ct_active s \ is_subject aag (cur_thread s)) - and K (is_subject_irq aag irq)\ - handle_interrupt irq - \\_. integrity aag X st\" - apply (simp add: handle_interrupt_def cong: irq_state.case_cong) - apply (rule conjI; rule impI; rule hoare_pre) - apply (wp (once) send_signal_respects get_cap_auth_wp [where aag = aag] dmo_mol_respects - ackInterrupt_device_state_inv resetTimer_device_state_inv - | simp add: get_irq_slot_def get_irq_state_def - | wp dmo_no_mem_respects - | wpc)+ - apply (fastforce simp: is_cap_simps aag_cap_auth_def cap_auth_conferred_def - cap_rights_to_auth_def) - done - lemma hacky_ipc_Send: "\ abs_has_auth_to aag Notify (interrupt_irq_node s irq) p; pas_refined aag s; pasMaySendIrqs aag \ @@ -617,27 +608,50 @@ lemma hacky_ipc_Send: apply simp done +lemma handle_interrupt_integrity_autarch: + "\integrity aag X st and pas_refined aag and invs + and (\s. pasMaySendIrqs aag \ interrupt_states s irq \ IRQSignal) + and (\s. is_subject aag (cur_thread s))\ + handle_interrupt irq + \\_. integrity aag X st\" + apply (simp add: handle_interrupt_def cong: irq_state.case_cong bind_cong) + apply (rule conjI; rule impI; rule hoare_pre) + apply (wpsimp wp: send_signal_respects get_cap_wp dmo_mol_respects dmo_no_mem_respects + ackInterrupt_device_state_inv resetTimer_device_state_inv + handle_reserved_irq_integrity_autarch + simp: get_irq_slot_def get_irq_state_def)+ + apply (rule conjI, fastforce)+ \ \valid_objs etc.\ + apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (rule_tac s = s in hacky_ipc_Send [where irq = irq]) + apply (drule (1) cap_auth_caps_of_state) + apply (clarsimp simp: aag_cap_auth_def is_cap_simps cap_auth_conferred_def + cap_rights_to_auth_def split: if_split_asm) + apply assumption+ + done + lemma handle_interrupt_integrity: "\integrity aag X st and pas_refined aag and invs and (\s. pasMaySendIrqs aag \ interrupt_states s irq \ IRQSignal) - and (\s. ct_active s \ is_subject aag (cur_thread s))\ + and (\s. ct_active s \ is_subject aag (cur_thread s)) + and (ct_active or ct_idle)\ handle_interrupt irq \\_. integrity aag X st\" - apply (simp add: handle_interrupt_def - cong: irq_state.case_cong bind_cong) + apply (subst distrib(3)) + apply (rule hoare_pre_disj) + apply (wpsimp wp: handle_interrupt_integrity_autarch) + apply (simp add: handle_interrupt_def cong: irq_state.case_cong bind_cong) apply (rule conjI; rule impI; rule hoare_pre) - apply (wp (once) send_signal_respects get_cap_wp dmo_mol_respects dmo_no_mem_respects - ackInterrupt_device_state_inv resetTimer_device_state_inv - | wpc - | simp add: get_irq_slot_def get_irq_state_def)+ - apply clarsimp + apply (wpsimp wp: send_signal_respects get_cap_wp dmo_mol_respects dmo_no_mem_respects + ackInterrupt_device_state_inv resetTimer_device_state_inv + handle_reserved_irq_integrity_idle + simp: get_irq_slot_def get_irq_state_def)+ apply (rule conjI, fastforce)+ \ \valid_objs etc.\ apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule_tac s = s in hacky_ipc_Send [where irq = irq]) - apply (drule (1) cap_auth_caps_of_state) - apply (clarsimp simp: aag_cap_auth_def is_cap_simps cap_auth_conferred_def - cap_rights_to_auth_def split: if_split_asm) - apply assumption+ + apply (drule (1) cap_auth_caps_of_state) + apply (clarsimp simp: aag_cap_auth_def is_cap_simps cap_auth_conferred_def + cap_rights_to_auth_def split: if_split_asm) + apply assumption+ done lemma handle_yield_pas_refined[wp]: @@ -647,25 +661,22 @@ lemma handle_yield_pas_refined[wp]: lemma handle_event_pas_refined: "\pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct - and (\s. ev \ Interrupt \ is_subject aag (cur_thread s)) + and (\s. ct_active s \ is_subject aag (cur_thread s)) and (\s. ev \ Interrupt \ ct_active s) \ handle_event ev \\_. pas_refined aag\" apply (case_tac ev; simp) - apply (rename_tac syscall) - apply (case_tac syscall; simp add: handle_send_def handle_call_def) - apply ((wp handle_invocation_pas_refined handle_recv_pas_refined - handle_fault_pas_refined - | simp | clarsimp)+) + apply (rename_tac syscall) + apply (case_tac syscall; simp add: handle_send_def handle_call_def) + apply ((wp handle_invocation_pas_refined handle_recv_pas_refined + handle_fault_pas_refined + | simp | clarsimp)+) + apply (fastforce simp: valid_fault_def) + apply (wp handle_fault_pas_refined | simp)+ apply (fastforce simp: valid_fault_def) - apply (wp handle_fault_pas_refined | simp)+ - apply (fastforce simp: valid_fault_def) - apply (wp handle_interrupt_pas_refined handle_fault_pas_refined - hoare_vcg_conj_lift hoare_vcg_all_lift - | wpc - | rule hoare_drop_imps - | strengthen invs_vobjs_strgs invs_psp_aligned invs_vspace_objs invs_arch_state - | simp)+ + apply (wpsimp wp: handle_fault_pas_refined handle_hypervisor_fault_pas_refined hoare_drop_imps + handle_interrupt_pas_refined hoare_vcg_conj_lift hoare_vcg_all_lift + simp: ct_in_state_def)+ done lemma valid_fault_Unknown[simp]: @@ -692,7 +703,7 @@ lemma handle_event_integrity: "\integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct - and (\s. ct_active s \ is_subject aag (cur_thread s)) + and (\s. is_subject aag (cur_thread s)) and (\s. ev \ Interrupt \ ct_active s) and ((=) st)\ handle_event ev \\_. integrity aag X st\" @@ -700,9 +711,9 @@ lemma handle_event_integrity: apply (unfold handle_send_def handle_call_def) by (wpsimp wp: handle_recv_integrity handle_invocation_respects handle_reply_respects handle_fault_integrity_autarch - handle_interrupt_integrity handle_vm_fault_integrity + handle_interrupt_integrity_autarch handle_vm_fault_integrity handle_reply_pas_refined handle_vm_fault_valid_fault - handle_reply_valid_sched + handle_reply_valid_sched handle_hypervisor_fault_integrity_autarch hoare_vcg_conj_lift hoare_vcg_all_lift hoare_drop_imps simp: domain_sep_inv_def | rule dmo_wp hoare_vcg_conj_elimE @@ -730,12 +741,9 @@ lemma activate_thread_integrity: done lemma activate_thread_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\ - activate_thread - \\_. pas_refined aag\" + "activate_thread \pas_refined aag\" unfolding activate_thread_def get_thread_state_def thread_get_def - apply (wpsimp wp: set_thread_state_pas_refined hoare_drop_imps) - done + by (wpsimp wp: set_thread_state_pas_refined hoare_drop_imps) lemma integrity_cur_thread[iff]: "integrity aag X st (s\cur_thread := v\) = integrity aag X st s" @@ -1144,39 +1152,46 @@ lemma guarded_pas_domain_machine_state_update[simp]: by (simp add: guarded_pas_domain_def) lemma call_kernel_integrity': - "st \ \einvs and pas_refined aag and is_subject aag \ cur_thread and schact_is_rct and guarded_pas_domain aag + "st \ \einvs and pas_refined aag and (\s. ct_active s \ is_subject aag (cur_thread s)) + and schact_is_rct and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and (\s. ev \ Interrupt \ ct_active s) and (ct_active or ct_idle) and K (pasMayActivate aag \ pasMayEditReadyQueues aag)\ call_kernel ev \\_. integrity aag X st\" - apply (simp add: call_kernel_def) - apply (simp only: spec_valid_def) - apply (wpsimp wp: activate_thread_respects schedule_integrity_pasMayEditReadyQueues - handle_interrupt_integrity dmo_wp handle_interrupt_pas_refined) + apply (case_tac "ev = Interrupt"; clarsimp simp: call_kernel_def spec_valid_def) + apply (wpsimp wp: activate_thread_respects schedule_integrity_pasMayEditReadyQueues + handle_interrupt_integrity handle_interrupt_pas_refined) + apply (rule_tac Q="\rv s. (rv = None \ P s) \ (\x. rv = Some x \ Q x s)" + and Q'="\rv s. P s \ (\x. rv = Some x \ Q x s)" + for P Q in hoare_strengthen_post[rotated]; clarsimp cong: conj_cong) + apply (wpsimp wp: hoare_vcg_all_lift hoare_drop_imps) + apply (fastforce intro!: valid_sched_ct_not_queued + simp: schact_is_rct_def domain_sep_inv_def guarded_pas_domain_def) + apply (wpsimp wp: activate_thread_respects schedule_integrity_pasMayEditReadyQueues dmo_wp + handle_interrupt_integrity_autarch handle_interrupt_pas_refined ) apply (clarsimp simp: if_fun_split) apply (rule_tac Q'="\rv ms. (rv \ None \ the rv \ non_kernel_IRQs) \ Q True (domain_sep_inv (pasMaySendIrqs aag) st' s) rv ms" and Q="\rv ms. Q (the rv \ non_kernel_IRQs \ scheduler_act_sane s \ ct_not_queued s) (pasMaySendIrqs aag \ interrupt_states s (the rv) \ IRQSignal) rv ms" for Q in hoare_strengthen_post[rotated], fastforce simp: domain_sep_inv_def) - apply (wpsimp wp: getActiveIRQ_rv_None hoare_drop_imps getActiveIRQ_inv) + apply (wpsimp wp: getActiveIRQ_rv_None getActiveIRQ_inv hoare_drop_imps) apply (rule hoare_strengthen_postE, - rule_tac Q="integrity aag X st and pas_refined aag and einvs and guarded_pas_domain aag - and domain_sep_inv (pasMaySendIrqs aag) st' - and is_subject aag \ cur_thread - and K (pasMayActivate aag \ pasMayEditReadyQueues aag)" - in valid_validE) - apply (wpsimp wp: handle_event_integrity he_invs handle_event_pas_refined - handle_event_cur_thread handle_event_cur_domain + rule_tac Q="integrity aag X st and pas_refined aag and einvs and guarded_pas_domain aag + and domain_sep_inv (pasMaySendIrqs aag) st' + and is_subject aag \ cur_thread + and K (pasMayActivate aag \ pasMayEditReadyQueues aag)" + in valid_validE) + apply (wpsimp wp: handle_event_integrity handle_event_pas_refined handle_event_domain_sep_inv handle_event_valid_sched)+ - apply (fastforce simp: domain_sep_inv_def guarded_pas_domain_def)+ + apply (fastforce simp: domain_sep_inv_def guarded_pas_domain_def) done lemma call_kernel_integrity: "\pas_refined aag and einvs and (\s. ev \ Interrupt \ ct_active s) and (ct_active or ct_idle) and domain_sep_inv (pasMaySendIrqs aag) st' and schact_is_rct - and guarded_pas_domain aag and is_subject aag o cur_thread + and guarded_pas_domain aag and (\s. ct_active s \ is_subject aag (cur_thread s)) and K (pasMayActivate aag \ pasMayEditReadyQueues aag) and (\s. s = st)\ call_kernel ev \\_. integrity aag X st\" @@ -1188,18 +1203,22 @@ lemma call_kernel_integrity: done lemma call_kernel_pas_refined: - "\einvs and pas_refined aag and is_subject aag \ cur_thread and guarded_pas_domain aag + "\einvs and pas_refined aag and (\s. ct_active s \ is_subject aag (cur_thread s)) + and guarded_pas_domain aag and (\s. ev \ Interrupt \ ct_active s) and (ct_active or ct_idle) and schact_is_rct and pas_cur_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'\ call_kernel ev \\_. pas_refined aag\" - apply (simp add: call_kernel_def ) - apply (wp activate_thread_pas_refined schedule_pas_refined handle_interrupt_pas_refined - do_machine_op_pas_refined dmo_wp hoare_drop_imps getActiveIRQ_inv - | simp add: if_fun_split - | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+ - apply (wp he_invs handle_event_pas_refined) - apply auto + apply (case_tac "ev = Interrupt"; clarsimp simp: call_kernel_def) + apply (wpsimp wp: activate_thread_pas_refined schedule_pas_refined handle_interrupt_pas_refined + do_machine_op_pas_refined dmo_wp hoare_drop_imps getActiveIRQ_inv + | simp add: if_fun_split + | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+ + apply (rule hoare_strengthen_postE, + rule_tac Q="pas_refined aag and invs and is_subject aag \ cur_thread" + in valid_validE) + apply (wpsimp wp: he_invs handle_event_pas_refined) + apply auto done end diff --git a/proof/access-control/Tcb_AC.thy b/proof/access-control/Tcb_AC.thy index 9555729fdf..f1f7f54454 100644 --- a/proof/access-control/Tcb_AC.thy +++ b/proof/access-control/Tcb_AC.thy @@ -96,8 +96,7 @@ lemma cdt_NullCap: by (rule ccontr) (force dest: mdb_cte_atD simp: valid_mdb_def2) lemma setup_reply_master_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state - and valid_mdb and K (is_subject aag t)\ + "\pas_refined aag and valid_mdb and K (is_subject aag t)\ setup_reply_master t \\_. pas_refined aag\" apply (simp add: setup_reply_master_def) @@ -108,7 +107,7 @@ crunch possible_switch_to for tcb_domain_map_wellformed[wp]: "tcb_domain_map_wellformed aag" crunch setup_reply_master - for pspace_aligned[wp]: pspace_aligned + for pas_refined[wp]: "pas_refined aag" lemma restart_pas_refined: "\pas_refined aag and invs and tcb_at t and K (is_subject aag t)\ @@ -116,8 +115,8 @@ lemma restart_pas_refined: \\_. pas_refined aag\" apply (simp add: restart_def get_thread_state_def) apply (wp set_thread_state_pas_refined setup_reply_master_pas_refined thread_get_wp' - | strengthen invs_mdb - | fastforce)+ + | strengthen invs_mdb)+ + apply fastforce done lemma option_update_thread_set_safe_lift: @@ -177,7 +176,7 @@ lemma (in is_extended') cte_wp_at[wp]: "I (cte_wp_at P a)" by (rule lift_inv, simp) lemma checked_insert_pas_refined: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and + "\pas_refined aag and valid_mdb and K (\ is_master_reply_cap new_cap \ is_subject aag target \ is_subject aag (fst src_slot) \ pas_cap_cur_auth aag new_cap)\ check_cap_at new_cap src_slot @@ -340,8 +339,7 @@ lemma hoare_st_refl: done lemma bind_notification_pas_refined[wp]: - "\pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and - K (\auth \ {Receive, Reset}. abs_has_auth_to aag auth t ntfn)\ + "\pas_refined aag and K (\auth \ {Receive, Reset}. abs_has_auth_to aag auth t ntfn)\ bind_notification t ntfn \\_. pas_refined aag\" apply (clarsimp simp: bind_notification_def) @@ -358,13 +356,6 @@ lemma invoke_tcb_ntfn_control_pas_refined[wp]: apply (wp | fastforce simp: authorised_tcb_inv_def)+ done -crunch suspend, restart - for pspace_aligned[wp]: "\s :: det_ext state. pspace_aligned s" - and valid_vspace_objs[wp]: "\s :: det_ext state. valid_vspace_objs s" - and valid_arch_state[wp]: "\s :: det_ext state. valid_arch_state s" - (wp: dxo_wp_weak) - - context Tcb_AC_1 begin lemma invoke_tcb_pas_refined: @@ -382,11 +373,7 @@ lemma invoke_tcb_pas_refined: apply assumption apply (rule hoare_gen_asm) apply (cases ti, simp_all add: authorised_tcb_inv_def) - apply (wp ita_wps hoare_drop_imps - hoare_strengthen_post[where Q'="\_. pas_refined aag and pspace_aligned - and valid_vspace_objs - and valid_arch_state", - OF mapM_x_wp'] + apply (wp ita_wps hoare_drop_imps mapM_x_wp' | simp add: emptyable_def if_apply_def2 authorised_tcb_inv_def | rule ball_tcb_cap_casesI | wpc