From 10ce1a623951a2959e4594cb9c0c42b5edea397c Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Thu, 21 Mar 2024 12:05:50 +1030 Subject: [PATCH] haskell+design+proof: add assert to deleteObjects An assert is added in order to provide extra information regarding liveness for objects in the region to be detyped, in preparation for forthcoming work that will add fields to the TCB object and modify the definition of liveness. The assert is added separately from the current assert in deleteObjects since these asserts are shown to hold via lemmas which occur in different locales. Greater use of the definition schact_is_rct is made in general, and in particular, in some top-level theorems, but note that the guards and preconditions of top-level theorems have not been strengthened. Signed-off-by: Michael McInerney --- proof/crefine/AARCH64/Detype_C.thy | 3 +- proof/crefine/AARCH64/Refine_C.thy | 2 +- proof/crefine/ARM/Detype_C.thy | 2 +- proof/crefine/ARM/Refine_C.thy | 2 +- proof/crefine/ARM_HYP/Detype_C.thy | 2 +- proof/crefine/ARM_HYP/Refine_C.thy | 2 +- proof/crefine/RISCV64/Detype_C.thy | 2 +- proof/crefine/RISCV64/Refine_C.thy | 2 +- proof/crefine/X64/Detype_C.thy | 2 +- proof/crefine/X64/Refine_C.thy | 2 +- proof/infoflow/refine/ADT_IF_Refine.thy | 11 +- proof/infoflow/refine/ADT_IF_Refine_C.thy | 4 +- .../infoflow/refine/ARM/ArchADT_IF_Refine.thy | 3 +- .../refine/RISCV64/ArchADT_IF_Refine.thy | 3 +- proof/refine/AARCH64/Arch_R.thy | 36 +- proof/refine/AARCH64/Detype_R.thy | 635 +++++++++--------- proof/refine/AARCH64/EmptyFail_H.thy | 2 +- proof/refine/AARCH64/Refine.thy | 3 +- proof/refine/AARCH64/Syscall_R.thy | 20 +- proof/refine/AARCH64/Untyped_R.thy | 8 +- proof/refine/ARM/Arch_R.thy | 41 +- proof/refine/ARM/Detype_R.thy | 625 +++++++++-------- proof/refine/ARM/EmptyFail_H.thy | 2 +- proof/refine/ARM/Refine.thy | 3 +- proof/refine/ARM/Syscall_R.thy | 22 +- proof/refine/ARM/Untyped_R.thy | 7 +- proof/refine/ARM_HYP/Arch_R.thy | 41 +- proof/refine/ARM_HYP/Detype_R.thy | 621 +++++++++-------- proof/refine/ARM_HYP/EmptyFail_H.thy | 2 +- proof/refine/ARM_HYP/Refine.thy | 4 +- proof/refine/ARM_HYP/Syscall_R.thy | 22 +- proof/refine/ARM_HYP/Untyped_R.thy | 7 +- proof/refine/RISCV64/Arch_R.thy | 42 +- proof/refine/RISCV64/Detype_R.thy | 524 ++++++++------- proof/refine/RISCV64/EmptyFail_H.thy | 2 +- proof/refine/RISCV64/Refine.thy | 3 +- proof/refine/RISCV64/Syscall_R.thy | 22 +- proof/refine/RISCV64/Untyped_R.thy | 8 +- proof/refine/X64/Arch_R.thy | 41 +- proof/refine/X64/Detype_R.thy | 529 ++++++++------- proof/refine/X64/EmptyFail_H.thy | 2 +- proof/refine/X64/Refine.thy | 3 +- proof/refine/X64/Syscall_R.thy | 22 +- proof/refine/X64/Untyped_R.thy | 7 +- spec/design/skel/PSpaceFuns_H.thy | 2 +- spec/haskell/src/SEL4/Model/PSpace.lhs | 7 +- 46 files changed, 1770 insertions(+), 1587 deletions(-) diff --git a/proof/crefine/AARCH64/Detype_C.thy b/proof/crefine/AARCH64/Detype_C.thy index c6fbac801d..d63899c3f7 100644 --- a/proof/crefine/AARCH64/Detype_C.thy +++ b/proof/crefine/AARCH64/Detype_C.thy @@ -1553,8 +1553,7 @@ lemma deleteObjects_ccorres': doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm bind_assoc modify_machinestate_assert_cnodes_swap modify_machinestate_assert_ptables_swap modify_modify_bind) - apply (rule ccorres_stateAssert_fwd) - apply (rule ccorres_stateAssert_fwd) + apply (rule ccorres_stateAssert_fwd)+ apply (rule ccorres_stateAssert_after) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) diff --git a/proof/crefine/AARCH64/Refine_C.thy b/proof/crefine/AARCH64/Refine_C.thy index eb460f7ec0..a02f75905c 100644 --- a/proof/crefine/AARCH64/Refine_C.thy +++ b/proof/crefine/AARCH64/Refine_C.thy @@ -522,7 +522,7 @@ lemma no_fail_callKernel: apply (rule corres_nofail) apply (rule corres_guard_imp) apply (rule kernel_corres) - apply (force simp: word_neq_0_conv) + apply (force simp: word_neq_0_conv schact_is_rct_def) apply (simp add: sch_act_simple_def) apply metis done diff --git a/proof/crefine/ARM/Detype_C.thy b/proof/crefine/ARM/Detype_C.thy index 97b3c51563..78acb233ef 100644 --- a/proof/crefine/ARM/Detype_C.thy +++ b/proof/crefine/ARM/Detype_C.thy @@ -1428,7 +1428,7 @@ lemma deleteObjects_ccorres': doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm bind_assoc modify_machinestate_assert_cnodes_swap modify_modify_bind) - apply (rule ccorres_stateAssert_fwd) + apply (rule ccorres_stateAssert_fwd)+ apply (rule ccorres_stateAssert_after) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy index 450647c6ca..45cf87e663 100644 --- a/proof/crefine/ARM/Refine_C.thy +++ b/proof/crefine/ARM/Refine_C.thy @@ -516,7 +516,7 @@ lemma no_fail_callKernel: apply (rule corres_nofail) apply (rule corres_guard_imp) apply (rule kernel_corres) - apply force + apply (force simp: schact_is_rct_def) apply (simp add: sch_act_simple_def) apply metis done diff --git a/proof/crefine/ARM_HYP/Detype_C.thy b/proof/crefine/ARM_HYP/Detype_C.thy index 697df03bf8..1d6349e303 100644 --- a/proof/crefine/ARM_HYP/Detype_C.thy +++ b/proof/crefine/ARM_HYP/Detype_C.thy @@ -1535,7 +1535,7 @@ lemma deleteObjects_ccorres': doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm bind_assoc modify_machinestate_assert_cnodes_swap modify_modify_bind) - apply (rule ccorres_stateAssert_fwd) + apply (rule ccorres_stateAssert_fwd)+ apply (rule ccorres_stateAssert_after) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index 6af0762b14..d14d078ac3 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -509,7 +509,7 @@ lemma no_fail_callKernel: apply (rule corres_nofail) apply (rule corres_guard_imp) apply (rule kernel_corres) - apply force + apply (force simp: schact_is_rct_def) apply (simp add: sch_act_simple_def) apply metis done diff --git a/proof/crefine/RISCV64/Detype_C.thy b/proof/crefine/RISCV64/Detype_C.thy index 6b4080632b..d53327927c 100644 --- a/proof/crefine/RISCV64/Detype_C.thy +++ b/proof/crefine/RISCV64/Detype_C.thy @@ -1544,7 +1544,7 @@ lemma deleteObjects_ccorres': doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm bind_assoc modify_machinestate_assert_cnodes_swap modify_modify_bind) - apply (rule ccorres_stateAssert_fwd) + apply (rule ccorres_stateAssert_fwd)+ apply (rule ccorres_stateAssert_after) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) diff --git a/proof/crefine/RISCV64/Refine_C.thy b/proof/crefine/RISCV64/Refine_C.thy index df0296cc2e..5653b9c881 100644 --- a/proof/crefine/RISCV64/Refine_C.thy +++ b/proof/crefine/RISCV64/Refine_C.thy @@ -493,7 +493,7 @@ lemma no_fail_callKernel: apply (rule corres_nofail) apply (rule corres_guard_imp) apply (rule kernel_corres) - apply (force simp: word_neq_0_conv) + apply (force simp: word_neq_0_conv schact_is_rct_def) apply (simp add: sch_act_simple_def) apply metis done diff --git a/proof/crefine/X64/Detype_C.thy b/proof/crefine/X64/Detype_C.thy index bd677c7ffa..9d042490be 100644 --- a/proof/crefine/X64/Detype_C.thy +++ b/proof/crefine/X64/Detype_C.thy @@ -1542,7 +1542,7 @@ lemma deleteObjects_ccorres': doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm bind_assoc modify_machinestate_assert_cnodes_swap modify_modify_bind) - apply (rule ccorres_stateAssert_fwd) + apply (rule ccorres_stateAssert_fwd)+ apply (rule ccorres_stateAssert_after) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) diff --git a/proof/crefine/X64/Refine_C.thy b/proof/crefine/X64/Refine_C.thy index 517362d961..dc9c04e2aa 100644 --- a/proof/crefine/X64/Refine_C.thy +++ b/proof/crefine/X64/Refine_C.thy @@ -495,7 +495,7 @@ lemma no_fail_callKernel: apply (rule corres_nofail) apply (rule corres_guard_imp) apply (rule kernel_corres) - apply (force simp: word_neq_0_conv) + apply (force simp: word_neq_0_conv schact_is_rct_def) apply (simp add: sch_act_simple_def) apply metis done diff --git a/proof/infoflow/refine/ADT_IF_Refine.thy b/proof/infoflow/refine/ADT_IF_Refine.thy index cfeaaa4cb6..f8f1ac5008 100644 --- a/proof/infoflow/refine/ADT_IF_Refine.thy +++ b/proof/infoflow/refine/ADT_IF_Refine.thy @@ -282,8 +282,7 @@ locale ADT_IF_Refine_1 = "\K (uop_sane uop)\ doUserOp_if uop tc \\r s. (fst r) \ Some Interrupt\" and handleEvent_corres_arch_extras: "corres (dc \ dc) - (einvs and (\s. event \ Interrupt \ ct_running s) - and (\s. scheduler_action s = resume_cur_thread)) + (einvs and (\s. event \ Interrupt \ ct_running s) and schact_is_rct) (invs' and (\s. event \ Interrupt \ ct_running' s) and (\s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras) @@ -293,7 +292,7 @@ begin lemma kernel_entry_if_corres: "corres (prod_lift (dc \ dc)) (einvs and (\s. event \ Interrupt \ ct_running s) - and (\s. scheduler_action s = resume_cur_thread) + and schact_is_rct and (\s. 0 < domain_time s) and valid_domain_list) (invs' and (\s. event \ Interrupt \ ct_running' s) and arch_extras @@ -320,7 +319,7 @@ lemma kernel_entry_if_corres: apply (wp hoare_TrueI threadSet_invs_trivial thread_set_invs_trivial thread_set_ct_running threadSet_ct_running' thread_set_not_state_valid_sched hoare_vcg_const_imp_lift handle_event_domain_time_inv handle_interrupt_valid_domain_time - | simp add: tcb_cap_cases_def | wpc | wp (once) hoare_drop_imps)+ + | simp add: tcb_cap_cases_def schact_is_rct_def | wpc | wp (once) hoare_drop_imps)+ apply (fastforce simp: invs_def cur_tcb_def) apply force done @@ -340,7 +339,7 @@ lemma kernelEntry_ex_abs[wp]: apply (rule_tac x=sa in exI) apply (clarsimp simp: domain_time_rel_eq domain_list_rel_eq) by (fastforce simp: ct_running_related ct_idle_related schedaction_related - active_from_running' active_from_running) + active_from_running' active_from_running schact_is_rct_def) lemma doUserOp_if_ct_in_state[wp]: "doUserOp_if f tc \ct_in_state' st\" @@ -1272,7 +1271,7 @@ lemma haskell_to_abs: apply (rule corres_guard_imp) apply (rule kernel_entry_if_corres) apply clarsimp - apply ((clarsimp simp: full_invs_if_def full_invs_if'_def)+)[2] + apply ((clarsimp simp: full_invs_if_def full_invs_if'_def schact_is_rct_def)+)[2] apply (fastforce simp: prod_lift_def) apply (rule kernelEntry_if_empty_fail) apply (simp add: kernel_handle_preemption_if_def handlePreemption_H_if_def) diff --git a/proof/infoflow/refine/ADT_IF_Refine_C.thy b/proof/infoflow/refine/ADT_IF_Refine_C.thy index 60d409bff2..6f4e5e95f9 100644 --- a/proof/infoflow/refine/ADT_IF_Refine_C.thy +++ b/proof/infoflow/refine/ADT_IF_Refine_C.thy @@ -384,7 +384,7 @@ lemma kernelEntry_corres_C: apply (erule no_fail_pre) apply (clarsimp simp: all_invs'_def) apply (rule exI, rule conjI, assumption) - apply clarsimp + apply (clarsimp simp: schact_is_rct_def) apply (simp only: bind_assoc) apply (simp add: getCurThread_def) apply (rule corres_guard_imp) @@ -413,7 +413,7 @@ lemma kernelEntry_corres_C: apply (rule threadSet_all_invs_triv'[where e=e]) apply (clarsimp simp: all_invs'_def) apply (rule exI, (rule conjI, assumption)+) - subgoal by force + subgoal by (force simp: schact_is_rct_def) apply simp apply (rule hoare_post_taut[where P=\]) apply wp+ diff --git a/proof/infoflow/refine/ARM/ArchADT_IF_Refine.thy b/proof/infoflow/refine/ARM/ArchADT_IF_Refine.thy index 09a27e4a9c..92def05969 100644 --- a/proof/infoflow/refine/ARM/ArchADT_IF_Refine.thy +++ b/proof/infoflow/refine/ARM/ArchADT_IF_Refine.thy @@ -427,8 +427,7 @@ lemma doUserOp_if_no_interrupt[ADT_IF_Refine_assms]: lemma handleEvent_corres_arch_extras[ADT_IF_Refine_assms]: "corres (dc \ dc) - (einvs and (\s. event \ Interrupt \ ct_running s) - and (\s. scheduler_action s = resume_cur_thread)) + (einvs and (\s. event \ Interrupt \ ct_running s) and schact_is_rct) (invs' and (\s. event \ Interrupt \ ct_running' s) and (\s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras) diff --git a/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine.thy b/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine.thy index 56b80b2ac3..4c96dfc7d4 100644 --- a/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine.thy +++ b/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine.thy @@ -374,8 +374,7 @@ lemma doUserOp_if_no_interrupt[ADT_IF_Refine_assms]: lemma handleEvent_corres_arch_extras[ADT_IF_Refine_assms]: "corres (dc \ dc) - (einvs and (\s. event \ Interrupt \ ct_running s) - and (\s. scheduler_action s = resume_cur_thread)) + (einvs and (\s. event \ Interrupt \ ct_running s) and schact_is_rct) (invs' and (\s. event \ Interrupt \ ct_running' s) and (\s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras) diff --git a/proof/refine/AARCH64/Arch_R.thy b/proof/refine/AARCH64/Arch_R.thy index 3d8c68783a..bd6f5e5d1e 100644 --- a/proof/refine/AARCH64/Arch_R.thy +++ b/proof/refine/AARCH64/Arch_R.thy @@ -133,7 +133,7 @@ lemma set_cap_device_and_range_aligned: lemma performASIDControlInvocation_corres: "asid_ci_map i = i' \ corres dc - (einvs and ct_active and valid_aci i) + (einvs and ct_active and valid_aci i and schact_is_rct) (invs' and ct_active' and valid_aci' i') (perform_asid_control_invocation i) (performASIDControlInvocation i')" @@ -274,6 +274,7 @@ lemma performASIDControlInvocation_corres: subgoal by (fastforce simp:cte_wp_at_caps_of_state descendants_range_def2 empty_descendants_range_in) apply (fold_subgoals (prefix))[2] subgoal premises prems using prems by (clarsimp simp:invs_def valid_state_def)+ + apply (clarsimp simp: schact_is_rct_def) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule detype_locale.non_null_present) apply (fastforce simp:cte_wp_at_caps_of_state) @@ -332,26 +333,27 @@ lemma performASIDControlInvocation_corres: simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2 null_filter_descendants_of'[OF null_filter_simp'] capAligned_def asid_low_bits_def) - apply (erule descendants_range_caps_no_overlapI') - apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) - apply (simp add:empty_descendants_range_in') - apply (simp add:word_bits_def bit_simps) - apply (rule is_aligned_weaken) - apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) - apply (simp add:pageBits_def) + apply (erule descendants_range_caps_no_overlapI') + apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) + apply (simp add:empty_descendants_range_in') + apply (simp add:word_bits_def bit_simps) + apply (rule is_aligned_weaken) + apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) + apply (simp add:pageBits_def) + apply clarsimp + apply (drule(1) cte_cap_in_untyped_range) + apply (fastforce simp:cte_wp_at_ctes_of) + apply assumption+ + apply fastforce + apply simp apply clarsimp - apply (drule(1) cte_cap_in_untyped_range) - apply (fastforce simp:cte_wp_at_ctes_of) + apply (drule (1) cte_cap_in_untyped_range) + apply (fastforce simp add: cte_wp_at_ctes_of) apply assumption+ + apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) apply fastforce apply simp apply clarsimp - apply (drule (1) cte_cap_in_untyped_range) - apply (fastforce simp add: cte_wp_at_ctes_of) - apply assumption+ - apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) - apply fastforce - apply simp done definition vcpu_invocation_map :: "vcpu_invocation \ vcpuinvocation" where @@ -1378,7 +1380,7 @@ lemma performARMVCPUInvocation_corres: lemma arch_performInvocation_corres: "archinv_relation ai ai' \ corres (dc \ (=)) - (einvs and ct_active and valid_arch_inv ai) + (einvs and ct_active and valid_arch_inv ai and schact_is_rct) (invs' and ct_active' and valid_arch_inv' ai') (arch_perform_invocation ai) (Arch.performInvocation ai')" apply (clarsimp simp: arch_perform_invocation_def diff --git a/proof/refine/AARCH64/Detype_R.thy b/proof/refine/AARCH64/Detype_R.thy index 4a867acf4f..b3e6358b3c 100644 --- a/proof/refine/AARCH64/Detype_R.thy +++ b/proof/refine/AARCH64/Detype_R.thy @@ -100,6 +100,9 @@ defs deletionIsSafe_def: t \ mask_range ptr bits) \ (\ko. ksPSpace s p = Some (KOArch ko) \ p \ mask_range ptr bits \ 6 \ bits)" +defs deletionIsSafe_delete_locale_def: + "deletionIsSafe_delete_locale \ \ptr bits s. \p. ko_wp_at' live' p s \ p \ mask_range ptr bits" + defs ksASIDMapSafe_def: "ksASIDMapSafe \ \s. True" @@ -123,6 +126,7 @@ lemma deleteObjects_def2: "is_aligned ptr bits \ deleteObjects ptr bits = do stateAssert (deletionIsSafe ptr bits) []; + stateAssert (deletionIsSafe_delete_locale ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ mask_range ptr bits)) []; stateAssert (\s. \ pTablePartialOverlap (gsPTTypes (ksArchState s)) (\x. x \ mask_range ptr bits)) []; @@ -141,6 +145,7 @@ lemma deleteObjects_def2: apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def deleteGhost_def o_def) apply (rule bind_eqI, rule ext) apply (rule bind_eqI, rule ext) + apply (rule bind_eqI, rule ext) apply (simp add: bind_assoc[symmetric]) apply (rule bind_cong[rotated], rule refl) apply (simp add: bind_assoc modify_modify deleteRange_def gets_modify_def) @@ -167,6 +172,7 @@ lemma deleteObjects_def3: do assert (is_aligned ptr bits); stateAssert (deletionIsSafe ptr bits) []; + stateAssert (deletionIsSafe_delete_locale ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ mask_range ptr bits)) []; stateAssert (\s. \ pTablePartialOverlap (gsPTTypes (ksArchState s)) (\x. x \ mask_range ptr bits)) []; @@ -448,6 +454,7 @@ next qed end + locale detype_locale' = detype_locale + constrains s::"det_state" lemma (in detype_locale') deletionIsSafe: @@ -544,199 +551,6 @@ qed context begin interpretation Arch . (*FIXME: arch_split*) -(* FIXME: generalizes lemma SubMonadLib.corres_submonad *) -(* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) -(* FIXME: move *) -lemma corres_machine_op: - assumes P: "corres_underlying Id False True r P Q x x'" - shows "corres r (P \ machine_state) (Q \ ksMachineState) - (do_machine_op x) (doMachineOp x')" - apply (rule corres_submonad3 - [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) - apply (simp_all add: state_relation_def swp_def) - done - -lemma ekheap_relation_detype: - "ekheap_relation ekh kh \ - ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" - by (fastforce simp add: ekheap_relation_def split: if_split_asm) - -lemma cap_table_at_gsCNodes_eq: - "(s, s') \ state_relation - \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" - apply (clarsimp simp: state_relation_def ghost_relation_def - obj_at_def is_cap_table) - apply (drule_tac x = ptr in spec)+ - apply (drule_tac x = bits in spec)+ - apply fastforce - done - -lemma cNodeNoPartialOverlap: - "corres dc (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s - \ valid_objs s \ pspace_aligned s) - \ - (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) - (\x. base \ x \ x \ base + mask magnitude)) [])" - apply (simp add: stateAssert_def assert_def) - apply (rule corres_symb_exec_r[OF _ get_sp]) - apply (rule corres_req[rotated], subst if_P, assumption) - apply simp - apply (clarsimp simp: cNodePartialOverlap_def) - apply (drule(1) cte_wp_valid_cap) - apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq - obj_at_def is_cap_table) - apply (frule(1) pspace_alignedD) - apply (simp add: add_mask_fold) - apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) - apply (erule is_aligned_get_word_bits[where 'a=machine_word_len, folded word_bits_def]) - apply (clarsimp simp: is_aligned_no_overflow_mask add_mask_fold) - apply (blast intro: order_trans) - apply (simp add: is_aligned_no_overflow_mask power_overflow word_bits_def) - apply wp+ - done - -lemma state_rel_ghost: - "(s,s') \ state_relation \ - ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') (gsPTTypes (ksArchState s'))" - by (erule state_relationE) - -lemma ghost_PTTypes: - "\ ghost_relation kh gsu gsc pt_Ts; pt_Ts p = Some pt_t \ \ - (\pt. kh p = Some (ArchObj (PageTable pt)) \ pt_t = pt_type pt)" - by (clarsimp simp: ghost_relation_def) - -lemma pTableNoPartialOverlap: - "corres dc - (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ - valid_objs s \ pspace_aligned s) - \ - (return x) - (stateAssert (\s. \ pTablePartialOverlap (gsPTTypes (ksArchState s)) - (\x. base \ x \ x \ base + mask magnitude)) [])" - apply (simp add: stateAssert_def assert_def) - apply (rule corres_symb_exec_r[OF _ get_sp]) - apply (rule corres_req[rotated], subst if_P, assumption) - apply simp - apply (clarsimp simp: pTablePartialOverlap_def) - apply (frule state_rel_ghost) - apply (drule (1) ghost_PTTypes) - apply clarsimp - apply (drule(1) cte_wp_valid_cap) - apply (clarsimp simp: valid_cap_def valid_untyped_def) - apply (frule(1) pspace_alignedD) - apply (simp add: add_mask_fold) - apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) - apply (clarsimp simp: pt_bits_def) - apply (erule is_aligned_get_word_bits[where 'a=machine_word_len, folded word_bits_def]) - apply (clarsimp simp: is_aligned_no_overflow_mask add_mask_fold) - apply (blast intro: order_trans) - apply (simp add: is_aligned_no_overflow_mask power_overflow word_bits_def) - apply wp+ - done - -lemma corres_return_bind: (* FIXME AARCH64: move to Corres_UL *) - "corres_underlying sr nf nf' r P P' (do return (); f od) g \ corres_underlying sr nf nf' r P P' f g" - by simp - -lemma corres_return_bind2: (* FIXME AARCH64: move to Corres_UL *) - "corres_underlying sr nf nf' r P P' f (do return (); g od) \ corres_underlying sr nf nf' r P P' f g" - by simp - -crunches doMachineOp - for gsCNodes[wp]: "\s. P (gsCNodes s)" - -lemma deleteObjects_corres: - "is_aligned base magnitude \ magnitude \ 3 \ - corres dc - (\s. einvs s - \ s \ (cap.UntypedCap d base magnitude idx) - \ (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s - \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) - \ untyped_children_in_mdb s \ if_unsafe_then_cap s - \ valid_mdb s \ valid_global_refs s \ ct_active s) - (\s. s \' (UntypedCap d base magnitude idx) - \ valid_pspace' s) - (delete_objects base magnitude) (deleteObjects base magnitude)" - apply (simp add: deleteObjects_def2) - apply (rule corres_stateAssert_implied[where P'=\, simplified]) - prefer 2 - apply clarsimp - apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and - s=s in detype_locale'.deletionIsSafe, - simp_all add: detype_locale'_def detype_locale_def p_assoc_help invs_valid_pspace)[1] - apply (simp add:valid_cap_simps) - apply (simp add: ksASIDMapSafe_def) - apply (simp add: delete_objects_def) - apply (rule corres_underlying_split[where r'=dc]) - apply (rule corres_guard_imp[where r=dc]) - apply (rule corres_machine_op[OF corres_Id]; simp) - apply (rule no_fail_freeMemory; simp) - apply simp - apply (auto elim: is_aligned_weaken)[1] - apply (rule corres_return_bind) - apply (rule corres_split[OF cNodeNoPartialOverlap]) - apply (rule corres_return_bind) - apply (rule corres_split[OF pTableNoPartialOverlap]) - apply simp - apply (rule_tac P="\s. valid_objs s \ valid_list s \ - (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ - descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ - s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ - valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ - zombies_final s \ sym_refs (state_refs_of s) \ sym_refs (state_hyp_refs_of s) \ - untyped_children_in_mdb s \ if_unsafe_then_cap s \ - valid_global_refs s" and - P'="\s. s \' capability.UntypedCap d base magnitude idx \ - valid_pspace' s" in corres_modify) - apply (simp add: valid_pspace'_def) - apply (rule state_relation_null_filterE, assumption, - simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] - apply (simp add: detype_def, rule state.equality; - simp add: detype_ext_def wrap_ext_det_ext_ext_def) - apply (intro exI, fastforce) - apply (rule ext, clarsimp simp add: null_filter_def) - apply (rule sym, rule ccontr, clarsimp) - apply (drule(4) cte_map_not_null_outside') - apply (fastforce simp add: cte_wp_at_caps_of_state) - apply simp - apply (rule ext, clarsimp simp: null_filter'_def map_to_ctes_delete) - apply (rule sym, rule ccontr, clarsimp) - apply (frule(2) pspace_relation_cte_wp_atI - [OF state_relation_pspace_relation]) - apply (elim exE) - apply (frule(4) cte_map_not_null_outside') - apply (rule cte_wp_at_weakenE, erule conjunct1) - apply (case_tac y, clarsimp) - apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def - valid_nullcaps_def) - apply clarsimp - apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, - erule cte_wp_at_weakenE[OF _ TrueI], assumption+) - apply (simp add: add_mask_fold) - apply (simp add: add_mask_fold) - apply (rule detype_pspace_relation[simplified], - simp_all add: state_relation_pspace_relation valid_pspace_def)[1] - apply (simp add: valid_cap'_def capAligned_def) - apply (clarsimp simp: valid_cap_def, assumption) - apply (fastforce simp: detype_def detype_ext_def add_mask_fold wrap_ext_det_ext_ext_def - intro!: ekheap_relation_detype) - apply (clarsimp simp: state_relation_def ghost_relation_of_heap - detype_def) - apply (drule_tac t="gsUserPages s'" in sym) - apply (drule_tac t="gsCNodes s'" in sym) - apply (drule_tac t="gsPTTypes (ksArchState s')" in sym) - apply (auto simp: ups_of_heap_def cns_of_heap_def ext pt_types_of_heap_def add_mask_fold - opt_map_def - split: option.splits kernel_object.splits)[1] - apply (simp add: valid_mdb_def) - apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | - simp add: invs_def valid_state_def valid_pspace_def - descendants_range_def | wp (once) hoare_drop_imps)+ - apply fastforce - apply (wpsimp wp: hoare_vcg_op_lift) - done - - text \Invariant preservation across concrete deletion\ lemma caps_containedD': @@ -799,88 +613,89 @@ lemma zobj_refs_capRange: end locale delete_locale = - fixes s and base and bits and ptr and idx and d - assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s" - and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s)" - and invs: "invs' s" - and ct_act: "ct_active' s" - and sa_simp: "sch_act_simple s" - and bwb: "bits < word_bits" + fixes s' and base and bits and ptr and idx and d + assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s'" + and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s')" + and invs: "invs' s'" + and ct_act: "ct_active' s'" + and sa_simp: "sch_act_simple s'" and al: "is_aligned base bits" - and safe: "deletionIsSafe base bits s" + and safe: "deletionIsSafe base bits s'" context delete_locale begin interpretation Arch . (*FIXME: arch_split*) -lemma valid_objs: "valid_objs' s" - and pa: "pspace_aligned' s" - and pc: "pspace_canonical' s" - and pd: "pspace_distinct' s" - and vq: "valid_queues s" - and vq': "valid_queues' s" - and sym_refs: "sym_refs (state_refs_of' s)" - and sym_hyp_refs: "sym_refs (state_hyp_refs_of' s)" - and iflive: "if_live_then_nonz_cap' s" - and ifunsafe: "if_unsafe_then_cap' s" - and dlist: "valid_dlist (ctes_of s)" - and no_0: "no_0 (ctes_of s)" - and chain_0: "mdb_chain_0 (ctes_of s)" - and badges: "valid_badges (ctes_of s)" - and contained: "caps_contained' (ctes_of s)" - and chunked: "mdb_chunked (ctes_of s)" - and umdb: "untyped_mdb' (ctes_of s)" - and uinc: "untyped_inc' (ctes_of s)" - and nullcaps: "valid_nullcaps (ctes_of s)" - and ut_rev: "ut_revocable' (ctes_of s)" - and dist_z: "distinct_zombies (ctes_of s)" - and irq_ctrl: "irq_control (ctes_of s)" - and clinks: "class_links (ctes_of s)" - and rep_r_fb: "reply_masters_rvk_fb (ctes_of s)" - and idle: "valid_idle' s" - and refs: "valid_global_refs' s" - and arch: "valid_arch_state' s" - and virq: "valid_irq_node' (irq_node' s) s" - and virqh: "valid_irq_handlers' s" - and virqs: "valid_irq_states' s" - and no_0_objs: "no_0_obj' s" - and ctnotinQ: "ct_not_inQ s" - and irqs_masked: "irqs_masked' s" - and ctcd: "ct_idle_or_in_cur_domain' s" - and cdm: "ksCurDomain s \ maxDomain" - and vds: "valid_dom_schedule' s" +lemma valid_objs: "valid_objs' s'" + and pa: "pspace_aligned' s'" + and pc: "pspace_canonical' s'" + and pd: "pspace_distinct' s'" + and vq: "valid_queues s'" + and vq': "valid_queues' s'" + and sym_refs: "sym_refs (state_refs_of' s')" + and sym_hyp_refs: "sym_refs (state_hyp_refs_of' s')" + and iflive: "if_live_then_nonz_cap' s'" + and ifunsafe: "if_unsafe_then_cap' s'" + and dlist: "valid_dlist (ctes_of s')" + and no_0: "no_0 (ctes_of s')" + and chain_0: "mdb_chain_0 (ctes_of s')" + and badges: "valid_badges (ctes_of s')" + and contained: "caps_contained' (ctes_of s')" + and chunked: "mdb_chunked (ctes_of s')" + and umdb: "untyped_mdb' (ctes_of s')" + and uinc: "untyped_inc' (ctes_of s')" + and nullcaps: "valid_nullcaps (ctes_of s')" + and ut_rev: "ut_revocable' (ctes_of s')" + and dist_z: "distinct_zombies (ctes_of s')" + and irq_ctrl: "irq_control (ctes_of s')" + and clinks: "class_links (ctes_of s')" + and rep_r_fb: "reply_masters_rvk_fb (ctes_of s')" + and idle: "valid_idle' s'" + and refs: "valid_global_refs' s'" + and arch: "valid_arch_state' s'" + and virq: "valid_irq_node' (irq_node' s') s'" + and virqh: "valid_irq_handlers' s'" + and virqs: "valid_irq_states' s'" + and no_0_objs: "no_0_obj' s'" + and ctnotinQ: "ct_not_inQ s'" + and irqs_masked: "irqs_masked' s'" + and ctcd: "ct_idle_or_in_cur_domain' s'" + and cdm: "ksCurDomain s' \ maxDomain" + and vds: "valid_dom_schedule' s'" using invs - by (auto simp add: invs'_def valid_state'_def valid_pspace'_def - valid_mdb'_def valid_mdb_ctes_def) + by (auto simp: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) abbreviation "base_bits \ mask_range base bits" -abbreviation - "state' \ (s \ ksPSpace := \x. if base \ x \ x \ base + mask bits then None else ksPSpace s x \)" +abbreviation pspace' :: pspace where + "pspace' \ \x. if base \ x \ x \ base + mask bits then None else ksPSpace s' x" + +abbreviation state' :: kernel_state where + "state' \ (s' \ ksPSpace := pspace' \)" lemma ko_wp_at'[simp]: - "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s \ p \ base_bits)" + "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s' \ p \ base_bits)" by (fastforce simp add: ko_wp_at_delete'[OF pd]) lemma obj_at'[simp]: - "\P p. (obj_at' P p state') = (obj_at' P p s \ p \ base_bits)" + "\P p. (obj_at' P p state') = (obj_at' P p s' \ p \ base_bits)" by (fastforce simp add: obj_at'_real_def) lemma typ_at'[simp]: - "typ_at' P p state' = (typ_at' P p s \ p \ base_bits)" + "typ_at' P p state' = (typ_at' P p s' \ p \ base_bits)" by (simp add: typ_at'_def) lemma valid_untyped[simp]: - "s \' UntypedCap d base bits idx" + "s' \' UntypedCap d base bits idx" using cte_wp_at_valid_objs_valid_cap' [OF cap valid_objs] by clarsimp lemma cte_wp_at'[simp]: - "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s \ p \ base_bits)" + "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s' \ p \ base_bits)" by (fastforce simp:cte_wp_at_delete'[where idx = idx,OF valid_untyped pd ]) (* the bits of caps they need for validity argument are within their capRanges *) lemma valid_cap_ctes_pre: - "\c. s \' c \ case c of CNodeCap ref bits g gs \ + "\c. s' \' c \ case c of CNodeCap ref bits g gs \ \x. ref + (x && mask bits) * 2^cteSizeBits \ capRange c | Zombie ref (ZombieCNode bits) n \ \x. ref + (x && mask bits) * 2^cteSizeBits \ capRange c @@ -911,13 +726,13 @@ lemma valid_cap_ctes_pre: done lemma replycap_argument: - "\p t m r. cte_wp_at' (\cte. cteCap cte = ReplyCap t m r) p s + "\p t m r. cte_wp_at' (\cte. cteCap cte = ReplyCap t m r) p s' \ t \ mask_range base bits" using safe by (force simp: deletionIsSafe_def cte_wp_at_ctes_of) lemma valid_cap': - "\p c. \ s \' c; cte_wp_at' (\cte. cteCap cte = c) p s; + "\p c. \ s' \' c; cte_wp_at' (\cte. cteCap cte = c) p s'; capRange c \ mask_range base bits = {} \ \ state' \' c" apply (subgoal_tac "capClass c = PhysicalClass \ capUntypedPtr c \ capRange c") apply (subgoal_tac "capClass c = PhysicalClass \ @@ -941,11 +756,11 @@ lemma valid_cap': done lemma objRefs_notrange: - assumes asms: "ctes_of s p = Some c" "\ isUntypedCap (cteCap c)" + assumes asms: "ctes_of s' p = Some c" "\ isUntypedCap (cteCap c)" shows "capRange (cteCap c) \ base_bits = {}" proof - from cap obtain node - where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" + where ctes_of: "ctes_of s' ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done @@ -966,11 +781,11 @@ proof - qed lemma ctes_of_valid [elim!]: - "ctes_of s p = Some cte \ s \' cteCap cte" + "ctes_of s' p = Some cte \ s' \' cteCap cte" by (case_tac cte, simp add: ctes_of_valid_cap' [OF _ valid_objs]) lemma valid_cap2: - "\ cte_wp_at' (\cte. cteCap cte = c) p s \ \ state' \' c" + "\ cte_wp_at' (\cte. cteCap cte = c) p s' \ \ state' \' c" apply (case_tac "isUntypedCap c") apply (drule cte_wp_at_valid_objs_valid_cap' [OF _ valid_objs]) apply (clarsimp simp: valid_cap'_def isCap_simps valid_untyped'_def) @@ -980,7 +795,7 @@ lemma valid_cap2: done lemma ex_nonz_cap_notRange: - "ex_nonz_cap_to' p s \ p \ base_bits" + "ex_nonz_cap_to' p s' \ p \ base_bits" apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (case_tac "isUntypedCap (cteCap cte)") apply (clarsimp simp: isCap_simps) @@ -992,14 +807,18 @@ lemma ex_nonz_cap_notRange: done lemma live_notRange: - "\ ko_wp_at' P p s; \ko. P ko \ live' ko \ \ p \ base_bits" + "\ ko_wp_at' P p s'; \ko. P ko \ live' ko \ \ p \ base_bits" apply (drule if_live_then_nonz_capE' [OF iflive ko_wp_at'_weakenE]) apply simp apply (erule ex_nonz_cap_notRange) done +lemma deletionIsSafe_delete_locale_holds: + "deletionIsSafe_delete_locale base bits s'" + by (fastforce dest: live_notRange simp: deletionIsSafe_delete_locale_def) + lemma refs_notRange: - "(x, tp) \ state_refs_of' s y \ y \ base_bits" + "(x, tp) \ state_refs_of' s' y \ y \ base_bits" apply (drule state_refs_of'_elemD) apply (erule live_notRange) apply (rule refs_of_live') @@ -1007,7 +826,7 @@ lemma refs_notRange: done lemma hyp_refs_notRange: - "(x, tp) \ state_hyp_refs_of' s y \ y \ base_bits" + "(x, tp) \ state_hyp_refs_of' s' y \ y \ base_bits" apply (drule state_hyp_refs_of'_elemD) apply (erule live_notRange) apply (rule hyp_refs_of_live') @@ -1015,8 +834,8 @@ lemma hyp_refs_notRange: done lemma sym_refs_VCPU_hyp_live': - "\ko_wp_at' ((=) (KOArch (KOVCPU v))) p s; sym_refs (state_hyp_refs_of' s); vcpuTCBPtr v = Some t\ - \ ko_wp_at' (\ko. koTypeOf ko = TCBT \ hyp_live' ko) t s" + "\ko_wp_at' ((=) (KOArch (KOVCPU v))) p s'; sym_refs (state_hyp_refs_of' s'); vcpuTCBPtr v = Some t\ + \ ko_wp_at' (\ko. koTypeOf ko = TCBT \ hyp_live' ko) t s'" apply (drule (1) sym_hyp_refs_ko_wp_atD) apply (clarsimp) apply (drule state_hyp_refs_of'_elemD) @@ -1025,8 +844,8 @@ lemma sym_refs_VCPU_hyp_live': done lemma sym_refs_TCB_hyp_live': - "\ko_wp_at' ((=) (KOTCB t)) p s; sym_refs (state_hyp_refs_of' s); atcbVCPUPtr (tcbArch t) = Some v\ - \ ko_wp_at' (\ko. koTypeOf ko = ArchT VCPUT \ hyp_live' ko) v s" + "\ko_wp_at' ((=) (KOTCB t)) p s'; sym_refs (state_hyp_refs_of' s'); atcbVCPUPtr (tcbArch t) = Some v\ + \ ko_wp_at' (\ko. koTypeOf ko = ArchT VCPUT \ hyp_live' ko) v s'" apply (drule (1) sym_hyp_refs_ko_wp_atD) apply (clarsimp) apply (drule state_hyp_refs_of'_elemD) @@ -1034,8 +853,223 @@ lemma sym_refs_TCB_hyp_live': apply (clarsimp simp: hyp_refs_of_rev' hyp_live'_def arch_live'_def) done +end + +context begin interpretation Arch . (*FIXME: arch_split*) + +(* FIXME: generalizes lemma SubMonadLib.corres_submonad *) +(* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) +(* FIXME: move *) +lemma corres_machine_op: + assumes P: "corres_underlying Id False True r P Q x x'" + shows "corres r (P \ machine_state) (Q \ ksMachineState) + (do_machine_op x) (doMachineOp x')" + apply (rule corres_submonad3 + [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) + apply (simp_all add: state_relation_def swp_def) + done + +lemma ekheap_relation_detype: + "ekheap_relation ekh kh \ + ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" + by (fastforce simp add: ekheap_relation_def split: if_split_asm) + +lemma cap_table_at_gsCNodes_eq: + "(s, s') \ state_relation + \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" + apply (clarsimp simp: state_relation_def ghost_relation_def + obj_at_def is_cap_table) + apply (drule_tac x = ptr in spec)+ + apply (drule_tac x = bits in spec)+ + apply fastforce + done + +lemma cNodeNoPartialOverlap: + "corres dc (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s + \ valid_objs s \ pspace_aligned s) + \ + (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) + (\x. base \ x \ x \ base + mask magnitude)) [])" + apply (simp add: stateAssert_def assert_def) + apply (rule corres_symb_exec_r[OF _ get_sp]) + apply (rule corres_req[rotated], subst if_P, assumption) + apply simp + apply (clarsimp simp: cNodePartialOverlap_def) + apply (drule(1) cte_wp_valid_cap) + apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq + obj_at_def is_cap_table) + apply (frule(1) pspace_alignedD) + apply (simp add: add_mask_fold) + apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) + apply (erule is_aligned_get_word_bits[where 'a=machine_word_len, folded word_bits_def]) + apply (clarsimp simp: is_aligned_no_overflow_mask add_mask_fold) + apply (blast intro: order_trans) + apply (simp add: is_aligned_no_overflow_mask power_overflow word_bits_def) + apply wp+ + done + +lemma state_rel_ghost: + "(s,s') \ state_relation \ + ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') (gsPTTypes (ksArchState s'))" + by (erule state_relationE) + +lemma ghost_PTTypes: + "\ ghost_relation kh gsu gsc pt_Ts; pt_Ts p = Some pt_t \ \ + (\pt. kh p = Some (ArchObj (PageTable pt)) \ pt_t = pt_type pt)" + by (clarsimp simp: ghost_relation_def) + +lemma pTableNoPartialOverlap: + "corres dc + (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ + valid_objs s \ pspace_aligned s) + \ + (return x) + (stateAssert (\s. \ pTablePartialOverlap (gsPTTypes (ksArchState s)) + (\x. base \ x \ x \ base + mask magnitude)) [])" + apply (simp add: stateAssert_def assert_def) + apply (rule corres_symb_exec_r[OF _ get_sp]) + apply (rule corres_req[rotated], subst if_P, assumption) + apply simp + apply (clarsimp simp: pTablePartialOverlap_def) + apply (frule state_rel_ghost) + apply (drule (1) ghost_PTTypes) + apply clarsimp + apply (drule(1) cte_wp_valid_cap) + apply (clarsimp simp: valid_cap_def valid_untyped_def) + apply (frule(1) pspace_alignedD) + apply (simp add: add_mask_fold) + apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) + apply (clarsimp simp: pt_bits_def) + apply (erule is_aligned_get_word_bits[where 'a=machine_word_len, folded word_bits_def]) + apply (clarsimp simp: is_aligned_no_overflow_mask add_mask_fold) + apply (blast intro: order_trans) + apply (simp add: is_aligned_no_overflow_mask power_overflow word_bits_def) + apply wp+ + done + +lemma corres_return_bind: (* FIXME AARCH64: move to Corres_UL *) + "corres_underlying sr nf nf' r P P' (do return (); f od) g \ corres_underlying sr nf nf' r P P' f g" + by simp + +lemma corres_return_bind2: (* FIXME AARCH64: move to Corres_UL *) + "corres_underlying sr nf nf' r P P' f (do return (); g od) \ corres_underlying sr nf nf' r P P' f g" + by simp + +crunches doMachineOp + for gsCNodes[wp]: "\s. P (gsCNodes s)" + and deletionIsSafe_delete_locale[wp]: "deletionIsSafe_delete_locale base magnitude" + (simp: deletionIsSafe_delete_locale_def) + +lemma deleteObjects_corres: + "is_aligned base magnitude \ magnitude \ 3 \ + corres dc + (\s. einvs s + \ s \ (cap.UntypedCap d base magnitude idx) + \ (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s + \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) + \ untyped_children_in_mdb s \ if_unsafe_then_cap s + \ valid_mdb s \ valid_global_refs s \ ct_active s + \ schact_is_rct s) + (\s'. invs' s' + \ cte_wp_at' (\cte. cteCap cte = UntypedCap d base magnitude idx) ptr s' + \ descendants_range' (UntypedCap d base magnitude idx) ptr (ctes_of s') + \ ct_active' s' + \ s' \' (UntypedCap d base magnitude idx)) + (delete_objects base magnitude) (deleteObjects base magnitude)" + apply (simp add: deleteObjects_def2) + apply (rule corres_stateAssert_implied[where P'=\, simplified]) + prefer 2 + apply clarsimp + apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and + s=s in detype_locale'.deletionIsSafe, + simp_all add: detype_locale'_def detype_locale_def p_assoc_help invs_valid_pspace)[1] + apply (simp add:valid_cap_simps) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe_delete_locale_holds) + apply (clarsimp simp: delete_locale_def) + apply (intro conjI) + apply (fastforce simp: sch_act_simple_def state_relation_def schact_is_rct_def) + apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and s=s + in detype_locale'.deletionIsSafe, + simp_all add: detype_locale'_def detype_locale_def invs_valid_pspace)[1] + apply (simp add:valid_cap_simps) + apply (simp add: ksASIDMapSafe_def) + apply (simp add: delete_objects_def) + apply (rule corres_underlying_split[where r'=dc]) + apply (rule corres_guard_imp[where r=dc]) + apply (rule corres_machine_op[OF corres_Id]; simp) + apply (rule no_fail_freeMemory; simp) + apply simp + apply (auto elim: is_aligned_weaken)[1] + apply (rule corres_return_bind) + apply (rule corres_split[OF cNodeNoPartialOverlap]) + apply (rule corres_return_bind) + apply (rule corres_split[OF pTableNoPartialOverlap]) + apply simp + apply (rule_tac P="\s. valid_objs s \ valid_list s \ + (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ + descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ + s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ + valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ + zombies_final s \ sym_refs (state_refs_of s) \ sym_refs (state_hyp_refs_of s) \ + untyped_children_in_mdb s \ if_unsafe_then_cap s \ + valid_global_refs s" and + P'="\s. s \' capability.UntypedCap d base magnitude idx \ + valid_pspace' s" in corres_modify) + apply (simp add: valid_pspace'_def) + apply (rule state_relation_null_filterE, assumption, + simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] + apply (simp add: detype_def, rule state.equality; + simp add: detype_ext_def wrap_ext_det_ext_ext_def) + apply (intro exI, fastforce) + apply (rule ext, clarsimp simp add: null_filter_def) + apply (rule sym, rule ccontr, clarsimp) + apply (drule(4) cte_map_not_null_outside') + apply (fastforce simp add: cte_wp_at_caps_of_state) + apply simp + apply (rule ext, clarsimp simp: null_filter'_def map_to_ctes_delete) + apply (rule sym, rule ccontr, clarsimp) + apply (frule(2) pspace_relation_cte_wp_atI + [OF state_relation_pspace_relation]) + apply (elim exE) + apply (frule(4) cte_map_not_null_outside') + apply (rule cte_wp_at_weakenE, erule conjunct1) + apply (case_tac y, clarsimp) + apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def + valid_nullcaps_def) + apply clarsimp + apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, + erule cte_wp_at_weakenE[OF _ TrueI], assumption+) + apply (simp add: add_mask_fold) + apply (simp add: add_mask_fold) + apply (rule detype_pspace_relation[simplified], + simp_all add: state_relation_pspace_relation valid_pspace_def)[1] + apply (simp add: valid_cap'_def capAligned_def) + apply (clarsimp simp: valid_cap_def, assumption) + apply (fastforce simp: detype_def detype_ext_def add_mask_fold wrap_ext_det_ext_ext_def + intro!: ekheap_relation_detype) + apply (clarsimp simp: state_relation_def ghost_relation_of_heap + detype_def) + apply (drule_tac t="gsUserPages s'" in sym) + apply (drule_tac t="gsCNodes s'" in sym) + apply (drule_tac t="gsPTTypes (ksArchState s')" in sym) + apply (auto simp: ups_of_heap_def cns_of_heap_def ext pt_types_of_heap_def add_mask_fold + opt_map_def + split: option.splits kernel_object.splits)[1] + apply (simp add: valid_mdb_def) + apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | + simp add: invs_def valid_state_def valid_pspace_def + descendants_range_def | wp (once) hoare_drop_imps)+ + apply fastforce + apply (wpsimp wp: hoare_vcg_op_lift) + done + +end + +context delete_locale begin interpretation Arch . (*FIXME: arch_split*) + lemma valid_obj': - "\ valid_obj' obj s; ko_wp_at' ((=) obj) p s \ \ valid_obj' obj state'" + "\ valid_obj' obj s'; ko_wp_at' ((=) obj) p s' \ \ valid_obj' obj state'" apply (case_tac obj, simp_all add: valid_obj'_def) apply (rename_tac endpoint) apply (case_tac endpoint, simp_all add: valid_ep'_def)[1] @@ -1082,16 +1116,15 @@ lemma valid_obj': done lemma st_tcb: - "\P p. \ st_tcb_at' P p s; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" - by (fastforce simp: pred_tcb_at'_def obj_at'_real_def live'_def hyp_live'_def - dest: live_notRange) + "\P p. \ st_tcb_at' P p s'; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" + by (fastforce simp: pred_tcb_at'_def obj_at'_real_def live'_def hyp_live'_def dest: live_notRange) lemma irq_nodes_global: - "\irq :: irq. irq_node' s + (ucast irq << cteSizeBits) \ global_refs' s" - by (simp add: global_refs'_def) + "\irq :: irq. irq_node' s' + (ucast irq << cteSizeBits) \ global_refs' s'" + by (simp add: global_refs'_def) lemma global_refs: - "global_refs' s \ base_bits = {}" + "global_refs' s' \ base_bits = {}" using cap apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule valid_global_refsD' [OF _ refs]) @@ -1099,20 +1132,20 @@ lemma global_refs: done lemma global_refs2: - "global_refs' s \ (- base_bits)" + "global_refs' s' \ (- base_bits)" using global_refs by blast lemma irq_nodes_range: - "\irq :: irq. irq_node' s + (ucast irq << cteSizeBits) \ base_bits" + "\irq :: irq. irq_node' s' + (ucast irq << cteSizeBits) \ base_bits" using irq_nodes_global global_refs by blast lemma cte_refs_notRange: - assumes asms: "ctes_of s p = Some c" - shows "cte_refs' (cteCap c) (irq_node' s) \ base_bits = {}" + assumes asms: "ctes_of s' p = Some c" + shows "cte_refs' (cteCap c) (irq_node' s') \ base_bits = {}" proof - from cap obtain node - where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" + where ctes_of: "ctes_of s' ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done @@ -1141,7 +1174,7 @@ proof - qed lemma non_null_present: - "cte_wp_at' (\c. cteCap c \ NullCap) p s \ p \ base_bits" + "cte_wp_at' (\c. cteCap c \ NullCap) p s' \ p \ base_bits" apply (drule (1) if_unsafe_then_capD' [OF _ ifunsafe]) apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of dest!: cte_refs_notRange simp del: atLeastAtMost_iff) @@ -1149,7 +1182,7 @@ lemma non_null_present: done lemma cte_cap: - "ex_cte_cap_to' p s \ ex_cte_cap_to' p state'" + "ex_cte_cap_to' p s' \ ex_cte_cap_to' p state'" apply (clarsimp simp: ex_cte_cap_to'_def) apply (frule non_null_present [OF cte_wp_at_weakenE']) apply clarsimp @@ -1157,37 +1190,37 @@ lemma cte_cap: done lemma idle_notRange: - "\cref. \ cte_wp_at' (\c. ksIdleThread s \ capRange (cteCap c)) cref s - \ ksIdleThread s \ base_bits" + "\cref. \ cte_wp_at' (\c. ksIdleThread s' \ capRange (cteCap c)) cref s' + \ ksIdleThread s' \ base_bits" apply (insert cap) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule_tac x=ptr in allE, clarsimp simp: field_simps mask_def) done abbreviation - "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + mask bits then None else ksPSpace s x)" + "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + mask bits then None else ksPSpace s' x)" lemmas tree_to_ctes = map_to_ctes_delete [OF valid_untyped pd] lemma map_to_ctesE[elim!]: - "\ ctes' x = Some cte; \ ctes_of s x = Some cte; x \ base_bits \ \ P \ \ P" + "\ ctes' x = Some cte; \ ctes_of s' x = Some cte; x \ base_bits \ \ P \ \ P" by (clarsimp simp: tree_to_ctes split: if_split_asm) lemma not_nullMDBNode: - "\ ctes_of s x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" + "\ ctes_of s' x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" using nullcaps apply (cases cte) apply (simp add: valid_nullcaps_def) done -lemma mdb_src: "\ ctes_of s \ x \ y; y \ 0 \ \ x \ base_bits" +lemma mdb_src: "\ ctes_of s' \ x \ y; y \ 0 \ \ x \ base_bits" apply (rule non_null_present) apply (clarsimp simp: next_unfold' cte_wp_at_ctes_of) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def) done -lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ \ y \ base_bits" +lemma mdb_dest: "\ ctes_of s' \ x \ y; y \ 0 \ \ y \ base_bits" apply (case_tac "x = 0") apply (insert no_0, simp add: next_unfold')[1] apply (drule(1) vdlist_nextD0 [OF _ _ dlist]) @@ -1198,7 +1231,7 @@ lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ done lemma trancl_next[elim]: - "\ ctes_of s \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" + "\ ctes_of s' \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" apply (erule rev_mp, erule converse_trancl_induct) apply clarsimp apply (rule r_into_trancl) @@ -1216,14 +1249,14 @@ lemma trancl_next[elim]: done lemma mdb_parent_notrange: - "ctes_of s \ x \ y \ x \ base_bits \ y \ base_bits" + "ctes_of s' \ x \ y \ x \ base_bits \ y \ base_bits" apply (erule subtree.induct) apply (frule(1) mdb_src, drule(1) mdb_dest, simp) apply (drule(1) mdb_dest, simp) done lemma mdb_parent: - "ctes_of s \ x \ y \ ctes' \ x \ y" + "ctes_of s' \ x \ y \ ctes' \ x \ y" apply (erule subtree.induct) apply (frule(1) mdb_src, frule(1) mdb_dest) apply (rule subtree.direct_parent) @@ -1239,7 +1272,7 @@ lemma mdb_parent: done lemma trancl_next_rev: - "ctes' \ x \\<^sup>+ y \ ctes_of s \ x \\<^sup>+ y" + "ctes' \ x \\<^sup>+ y \ ctes_of s' \ x \\<^sup>+ y" apply (erule converse_trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp: next_unfold') @@ -1249,7 +1282,7 @@ lemma trancl_next_rev: done lemma is_chunk[elim!]: - "is_chunk (ctes_of s) cap x y \ is_chunk ctes' cap x y" + "is_chunk (ctes_of s') cap x y \ is_chunk ctes' cap x y" apply (simp add: is_chunk_def) apply (erule allEI) apply (clarsimp dest!: trancl_next_rev) @@ -1350,7 +1383,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def intro!: cte_cap) from idle_notRange refs - have "ksIdleThread s \ ?ran" + have "ksIdleThread s' \ ?ran" apply (simp add: cte_wp_at_ctes_of valid_global_refs'_def valid_refs'_def) apply blast done @@ -1452,11 +1485,11 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def show "valid_arch_state' ?s" using arch global_refs2 apply (simp add: valid_arch_state'_def global_refs'_def) - apply (case_tac "armHSCurVCPU (ksArchState s)"; clarsimp simp add: split_def) + apply (case_tac "armHSCurVCPU (ksArchState s')"; clarsimp simp add: split_def) apply (drule live_notRange, clarsimp, case_tac ko; simp add: is_vcpu'_def live'_def) done - show "valid_irq_node' (irq_node' s) ?s" + show "valid_irq_node' (irq_node' s') ?s" using virq irq_nodes_range by (simp add: valid_irq_node'_def mult.commute mult.left_commute ucast_ucast_mask_8) @@ -1486,7 +1519,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def ball_ran_eq) from virqs - show "valid_irq_states' s" . + show "valid_irq_states' s'" . from no_0_objs show "no_0_obj' state'" @@ -1497,19 +1530,19 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def by (simp add: irqs_masked'_def) from sa_simp ct_act - show "sch_act_wf (ksSchedulerAction s) state'" + show "sch_act_wf (ksSchedulerAction s') state'" apply (simp add: sch_act_simple_def) - apply (case_tac "ksSchedulerAction s", simp_all add: ct_in_state'_def) + apply (case_tac "ksSchedulerAction s'", simp_all add: ct_in_state'_def) apply (fastforce dest!: st_tcb elim!: pred_tcb'_weakenE) done from invs - have "pspace_domain_valid s" by (simp add: invs'_def valid_state'_def) + have "pspace_domain_valid s'" by (simp add: invs'_def valid_state'_def) thus "pspace_domain_valid state'" by (simp add: pspace_domain_valid_def) from invs - have "valid_machine_state' s" by (simp add: invs'_def valid_state'_def) + have "valid_machine_state' s'" by (simp add: invs'_def valid_state'_def) thus "valid_machine_state' ?state''" apply (clarsimp simp: valid_machine_state'_def) apply (drule_tac x=p in spec) @@ -1562,11 +1595,11 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def apply (clarsimp dest!: ex_nonz_cap_notRange elim!: ko_wp_at'_weakenE) done - from cdm show "ksCurDomain s \ maxDomain" . + from cdm show "ksCurDomain s' \ maxDomain" . from invs - have urz: "untyped_ranges_zero' s" by (simp add: invs'_def valid_state'_def) - show "untyped_ranges_zero_inv (cteCaps_of state') (gsUntypedZeroRanges s)" + have urz: "untyped_ranges_zero' s'" by (simp add: invs'_def valid_state'_def) + show "untyped_ranges_zero_inv (cteCaps_of state') (gsUntypedZeroRanges s')" apply (simp add: untyped_zero_ranges_cte_def urz[unfolded untyped_zero_ranges_cte_def, rule_format, symmetric]) apply (clarsimp simp: fun_eq_iff intro!: arg_cong[where f=Ex]) @@ -1579,14 +1612,14 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def qed (clarsimp) lemma (in delete_locale) delete_ko_wp_at': - assumes objs: "ko_wp_at' P p s \ ex_nonz_cap_to' p s" + assumes objs: "ko_wp_at' P p s' \ ex_nonz_cap_to' p s'" shows "ko_wp_at' P p state'" using objs by (clarsimp simp: ko_wp_at'_def ps_clear_def dom_if_None Diff_Int_distrib dest!: ex_nonz_cap_notRange) lemma (in delete_locale) null_filter': - assumes descs: "Q (null_filter' (ctes_of s))" + assumes descs: "Q (null_filter' (ctes_of s'))" shows "Q (null_filter' (ctes_of state'))" using descs ifunsafe apply (clarsimp elim!: rsubst[where P=Q]) @@ -1604,7 +1637,7 @@ lemma (in delete_locale) null_filter': done lemma (in delete_locale) delete_ex_cte_cap_to': - assumes exc: "ex_cte_cap_to' p s" + assumes exc: "ex_cte_cap_to' p s'" shows "ex_cte_cap_to' p state'" using exc by (clarsimp elim!: cte_cap) diff --git a/proof/refine/AARCH64/EmptyFail_H.thy b/proof/refine/AARCH64/EmptyFail_H.thy index 7a33f6cda1..9eebd65456 100644 --- a/proof/refine/AARCH64/EmptyFail_H.thy +++ b/proof/refine/AARCH64/EmptyFail_H.thy @@ -307,7 +307,7 @@ crunch (empty_fail) empty_fail: callKernel theorem call_kernel_serial: "\ (einvs and (\s. event \ Interrupt \ ct_running s) and (ct_running or ct_idle) and - (\s. scheduler_action s = resume_cur_thread) and + schact_is_rct and (\s. 0 < domain_time s \ valid_domain_list s)) s; \s'. (s, s') \ state_relation \ (invs' and (\s. event \ Interrupt \ ct_running' s) and (ct_running' or ct_idle') and diff --git a/proof/refine/AARCH64/Refine.thy b/proof/refine/AARCH64/Refine.thy index f8742d7394..3c6a30033a 100644 --- a/proof/refine/AARCH64/Refine.thy +++ b/proof/refine/AARCH64/Refine.thy @@ -612,7 +612,7 @@ lemma kernel_corres': apply (wp handle_event_valid_sched hoare_vcg_if_lift3 | simp | strengthen non_kernel_IRQs_strg[where Q=True, simplified], simp cong: conj_cong)+ - apply (clarsimp simp: active_from_running) + apply (clarsimp simp: active_from_running schact_is_rct_def) apply (clarsimp simp: active_from_running') done @@ -688,6 +688,7 @@ lemma entry_corres: thread_set_not_state_valid_sched hoare_weak_lift_imp hoare_vcg_disj_lift ct_in_state_thread_state_lift | simp add: tcb_cap_cases_def ct_in_state'_def thread_set_no_change_tcb_state + schact_is_rct_def | (wps, wp threadSet_st_tcb_at2) )+ apply (clarsimp simp: invs_def cur_tcb_def valid_state_def valid_pspace_def) apply (clarsimp simp: ct_in_state'_def) diff --git a/proof/refine/AARCH64/Syscall_R.thy b/proof/refine/AARCH64/Syscall_R.thy index d37f4c493d..f64f361d95 100644 --- a/proof/refine/AARCH64/Syscall_R.thy +++ b/proof/refine/AARCH64/Syscall_R.thy @@ -401,7 +401,7 @@ lemma performInvocation_corres: "\ inv_relation i i'; call \ block \ \ corres (dc \ (=)) (einvs and valid_invocation i - and simple_sched_action + and schact_is_rct and ct_active and (\s. (\w w2 b c. i = Invocations_A.InvokeEndpoint w w2 b c) \ st_tcb_at simple (cur_thread s) s)) (invs' and sch_act_simple and valid_invocation' i' and ct_active') @@ -450,7 +450,7 @@ lemma performInvocation_corres: apply (clarsimp simp: liftME_def) apply (rule corres_guard_imp) apply (erule invokeTCB_corres) - apply (simp)+ + apply ((clarsimp dest!: schact_is_rct_simple)+)[2] \ \domain cap\ apply (clarsimp simp: invoke_domain_def) apply (rule corres_guard_imp) @@ -465,7 +465,7 @@ lemma performInvocation_corres: apply assumption apply (rule corres_trivial, simp add: returnOk_def) apply wp+ - apply (clarsimp+)[2] + apply ((clarsimp dest!: schact_is_rct_simple)+)[2] apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric]) apply (rule corres_guard_imp, rule performIRQControl_corres, simp+) apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric]) @@ -1182,7 +1182,7 @@ crunches reply_from_kernel lemma handleInvocation_corres: "c \ b \ corres (dc \ dc) - (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + (einvs and schact_is_rct and ct_active) (invs' and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_invocation c b) @@ -1226,14 +1226,14 @@ lemma handleInvocation_corres: apply (wp reply_from_kernel_tcb_at) apply (rule impI, wp+) apply (wpsimp wp: hoare_drop_imps|strengthen invs_distinct invs_psp_aligned)+ - apply (rule_tac Q="\rv. einvs and simple_sched_action and valid_invocation rve + apply (rule_tac Q="\rv. einvs and schact_is_rct and valid_invocation rve and (\s. thread = cur_thread s) and st_tcb_at active thread" in hoare_post_imp) apply (clarsimp simp: simple_from_active ct_in_state_def elim!: st_tcb_weakenE) apply (wp sts_st_tcb_at' set_thread_state_simple_sched_action - set_thread_state_active_valid_sched) + set_thread_state_schact_is_rct set_thread_state_active_valid_sched) apply (rule_tac Q="\rv. invs' and valid_invocation' rve' and (\s. thread = ksCurThread s) and st_tcb_at' active' thread @@ -1338,7 +1338,7 @@ lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at'] lemma handleSend_corres: "corres (dc \ dc) - (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + (einvs and schact_is_rct and ct_active) (invs' and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_send blocking) (handleSend blocking)" @@ -1772,7 +1772,7 @@ lemma hr_ct_active'[wp]: done lemma handleCall_corres: - "corres (dc \ dc) (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + "corres (dc \ dc) (einvs and schact_is_rct and ct_active) (invs' and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') @@ -1976,7 +1976,7 @@ lemma hvmf_invs_etc: lemma handleEvent_corres: "corres (dc \ dc) (einvs and (\s. event \ Interrupt \ ct_running s) and - (\s. scheduler_action s = resume_cur_thread)) + schact_is_rct) (invs' and (\s. event \ Interrupt \ ct_running' s) and (\s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event)" @@ -2044,8 +2044,6 @@ proof - doMachineOp_getActiveIRQ_IRQ_active' | simp | simp add: imp_conjR | wp (once) hoare_drop_imps)+ - apply force - apply simp apply (clarsimp simp: invs'_def valid_state'_def ct_not_inQ_def valid_queues_def valid_queues_no_bitmap_def) apply (rule_tac corres_underlying_split) diff --git a/proof/refine/AARCH64/Untyped_R.thy b/proof/refine/AARCH64/Untyped_R.thy index 2f855762f5..a781e18568 100644 --- a/proof/refine/AARCH64/Untyped_R.thy +++ b/proof/refine/AARCH64/Untyped_R.thy @@ -4226,7 +4226,7 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemma resetUntypedCap_corres: "untypinv_relation ui ui' \ corres (dc \ dc) - (invs and valid_untyped_inv_wcap ui + (invs and schact_is_rct and valid_untyped_inv_wcap ui (Some (cap.UntypedCap dev ptr sz idx)) and ct_active and einvs and (\_. \ptr_base ptr' ty us slots dev'. ui = Invocations_A.Retype slot True @@ -4377,7 +4377,8 @@ lemma resetUntypedCap_corres: apply (frule if_unsafe_then_capD'[OF ctes_of_cte_wpD], clarsimp+) apply (frule(1) descendants_range_ex_cte'[OF empty_descendants_range_in' _ order_refl], (simp add: isCap_simps add_mask_fold)+) - by (intro conjI impI; clarsimp) + apply (auto simp: descendants_range_in'_def valid_untyped'_def) + done end @@ -4654,7 +4655,7 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemma inv_untyped_corres': "\ untypinv_relation ui ui' \ \ corres (dc \ (=)) - (einvs and valid_untyped_inv ui and ct_active) + (einvs and valid_untyped_inv ui and ct_active and schact_is_rct) (invs' and valid_untyped_inv' ui' and ct_active') (invoke_untyped ui) (invokeUntyped ui')" apply (cases ui) @@ -4673,6 +4674,7 @@ lemma inv_untyped_corres': (cte_map cref) reset ptr_base ptr ao' us (map cte_map slots) dev" assume invs: "invs (s :: det_state)" "ct_active s" "valid_list s" "valid_sched s" + "schact_is_rct s" and invs': "invs' s'" "ct_active' s'" and sr: "(s, s') \ state_relation" and vui: "valid_untyped_inv_wcap ?ui (Some (cap.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s" diff --git a/proof/refine/ARM/Arch_R.thy b/proof/refine/ARM/Arch_R.thy index e3410084ae..75692b7624 100644 --- a/proof/refine/ARM/Arch_R.thy +++ b/proof/refine/ARM/Arch_R.thy @@ -128,7 +128,7 @@ lemma set_cap_device_and_range_aligned: lemma performASIDControlInvocation_corres: "asid_ci_map i = i' \ corres dc - (einvs and ct_active and valid_aci i) + (einvs and ct_active and valid_aci i and schact_is_rct) (invs' and ct_active' and valid_aci' i') (perform_asid_control_invocation i) (performASIDControlInvocation i')" @@ -327,29 +327,30 @@ lemma performASIDControlInvocation_corres: apply clarsimp apply (frule empty_descendants_range_in') apply (intro conjI, - simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2 - null_filter_descendants_of'[OF null_filter_simp'] - capAligned_def asid_low_bits_def) - apply (erule descendants_range_caps_no_overlapI') - apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) - apply (simp add:empty_descendants_range_in') - apply (simp add:word_bits_def pageBits_def) - apply (rule is_aligned_weaken) - apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) - apply (simp add:pageBits_def) + simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2 + null_filter_descendants_of'[OF null_filter_simp'] + capAligned_def asid_low_bits_def) + apply (erule descendants_range_caps_no_overlapI') + apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) + apply (simp add:empty_descendants_range_in') + apply (simp add:word_bits_def pageBits_def) + apply (rule is_aligned_weaken) + apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) + apply (simp add:pageBits_def) + apply clarsimp + apply (drule(1) cte_cap_in_untyped_range) + apply (fastforce simp:cte_wp_at_ctes_of) + apply assumption+ + apply fastforce + apply simp apply clarsimp - apply (drule(1) cte_cap_in_untyped_range) - apply (fastforce simp:cte_wp_at_ctes_of) + apply (drule (1) cte_cap_in_untyped_range) + apply (fastforce simp add: cte_wp_at_ctes_of) apply assumption+ + apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) apply fastforce apply simp apply clarsimp - apply (drule (1) cte_cap_in_untyped_range) - apply (fastforce simp add: cte_wp_at_ctes_of) - apply assumption+ - apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) - apply fastforce - apply simp done definition @@ -1126,7 +1127,7 @@ shows lemma arch_performInvocation_corres: "archinv_relation ai ai' \ corres (dc \ (=)) - (einvs and ct_active and valid_arch_inv ai) + (einvs and ct_active and valid_arch_inv ai and schact_is_rct) (invs' and ct_active' and valid_arch_inv' ai' and (\s. vs_valid_duplicates' (ksPSpace s))) (arch_perform_invocation ai) (Arch.performInvocation ai')" apply (clarsimp simp: arch_perform_invocation_def diff --git a/proof/refine/ARM/Detype_R.thy b/proof/refine/ARM/Detype_R.thy index e6e2289b0d..e9dbf8de1e 100644 --- a/proof/refine/ARM/Detype_R.thy +++ b/proof/refine/ARM/Detype_R.thy @@ -100,6 +100,9 @@ defs deletionIsSafe_def: (\ko. ksPSpace s p = Some (KOArch ko) \ p \ {ptr .. ptr + 2 ^ bits - 1} \ 6 \ bits)" +defs deletionIsSafe_delete_locale_def: + "deletionIsSafe_delete_locale \ \ptr bits s. \p. ko_wp_at' live' p s \ p \ {ptr .. ptr + 2 ^ bits - 1}" + defs ksASIDMapSafe_def: "ksASIDMapSafe \ \s. \asid hw_asid pd. armKSASIDMap (ksArchState s) asid = Some (hw_asid,pd) \ page_directory_at' pd s" @@ -116,6 +119,7 @@ lemma deleteObjects_def2: "is_aligned ptr bits \ deleteObjects ptr bits = do stateAssert (deletionIsSafe ptr bits) []; + stateAssert (deletionIsSafe_delete_locale ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ {ptr .. ptr + 2 ^ bits - 1})) []; modify (\s. s \ ksPSpace := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} @@ -129,6 +133,7 @@ lemma deleteObjects_def2: apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def deleteGhost_def) apply (rule bind_eqI, rule ext) apply (rule bind_eqI, rule ext) + apply (rule bind_eqI, rule ext) apply (simp add: bind_assoc[symmetric]) apply (rule bind_cong[rotated], rule refl) apply (simp add: bind_assoc modify_modify deleteRange_def gets_modify_def) @@ -149,6 +154,7 @@ lemma deleteObjects_def3: do assert (is_aligned ptr bits); stateAssert (deletionIsSafe ptr bits) []; + stateAssert (deletionIsSafe_delete_locale ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ {ptr .. ptr + 2 ^ bits - 1})) []; modify (\s. s \ ksPSpace := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} @@ -432,6 +438,7 @@ next qed end + locale detype_locale' = detype_locale + constrains s::"det_state" lemma (in detype_locale') deletionIsSafe: @@ -443,9 +450,8 @@ lemma (in detype_locale') deletionIsSafe: shows "deletionIsSafe base magnitude s'" proof - interpret Arch . (* FIXME: arch_split *) - note blah[simp del] = atLeastatMost_subset_iff atLeastLessThan_iff - Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex - atLeastAtMost_iff + note [simp del] = atLeastatMost_subset_iff atLeastLessThan_iff atLeastAtMost_iff + Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex have "\t m r. \ptr. cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s \ t \ {base .. base + 2 ^ magnitude - 1}" by (fastforce dest!: valid_cap2 simp: cap obj_reply_refs_def) @@ -521,194 +527,8 @@ proof - done thus ?thesis using cte by (auto simp: deletionIsSafe_def) qed -context begin interpretation Arch . (*FIXME: arch_split*) -lemma ksASIDMapSafeI: - "\ (s,s') \ state_relation; invs s; pspace_aligned' s' \ pspace_distinct' s' \ - \ ksASIDMapSafe s'" - apply (clarsimp simp: ksASIDMapSafe_def) - apply (subgoal_tac "valid_asid_map s") - prefer 2 - apply fastforce - apply (clarsimp simp: valid_asid_map_def graph_of_def) - apply (subgoal_tac "arm_asid_map (arch_state s) asid = Some (hw_asid, pd)") - prefer 2 - apply (clarsimp simp: state_relation_def arch_state_relation_def) - apply (erule allE)+ - apply (erule (1) impE) - apply clarsimp - apply (drule find_pd_for_asid_eq_helper) - apply fastforce - apply assumption - apply fastforce - apply clarsimp - apply (rule pspace_relation_pd) - apply (fastforce simp: state_relation_def) - apply fastforce - apply assumption - apply assumption - apply simp - done - -(* FIXME: generalizes lemma SubMonadLib.corres_submonad *) -(* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) -(* FIXME: move *) -lemma corres_machine_op: - assumes P: "corres_underlying Id False True r P Q x x'" - shows "corres r (P \ machine_state) (Q \ ksMachineState) - (do_machine_op x) (doMachineOp x')" - apply (rule corres_submonad3 - [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) - apply (simp_all add: state_relation_def swp_def) - done - -lemma ekheap_relation_detype: - "ekheap_relation ekh kh \ - ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" - by (fastforce simp add: ekheap_relation_def split: if_split_asm) - -lemma cap_table_at_gsCNodes_eq: - "(s, s') \ state_relation - \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" - apply (clarsimp simp: state_relation_def ghost_relation_def - obj_at_def is_cap_table) - apply (drule_tac x = ptr in spec)+ - apply (drule_tac x = bits in spec)+ - apply fastforce - done - -lemma cNodeNoPartialOverlap: - "corres dc (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s - \ valid_objs s \ pspace_aligned s) - \ - (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) - (\x. base \ x \ x \ base + 2 ^ magnitude - 1)) [])" - apply (simp add: stateAssert_def assert_def) - apply (rule corres_symb_exec_r[OF _ get_sp]) - apply (rule corres_req[rotated], subst if_P, assumption) - apply simp - apply (clarsimp simp: cNodePartialOverlap_def) - apply (drule(1) cte_wp_valid_cap) - apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq - obj_at_def is_cap_table) - apply (frule(1) pspace_alignedD) - apply simp - apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) - apply (erule is_aligned_get_word_bits[where 'a=32, folded word_bits_def]) - apply (clarsimp simp: is_aligned_no_overflow) - apply (blast intro: order_trans) - apply (simp add: is_aligned_no_overflow power_overflow word_bits_def) - apply wp+ - done - - -declare wrap_ext_det_ext_ext_def[simp] - -(* Just for ARM *) -lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s)" - apply (auto simp: state_hyp_refs_of_def sym_refs_def) - apply (case_tac "kheap s x"; simp add: hyp_refs_of_def) - apply (rename_tac ko) - apply (case_tac ko; clarsimp) - done - -lemma deleteObjects_corres: - "is_aligned base magnitude \ magnitude \ 2 \ - corres dc - (\s. einvs s - \ s \ (cap.UntypedCap d base magnitude idx) - \ (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s - \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) - \ untyped_children_in_mdb s \ if_unsafe_then_cap s - \ valid_mdb s \ valid_global_refs s \ ct_active s) - (\s. s \' (UntypedCap d base magnitude idx) - \ valid_pspace' s) - (delete_objects base magnitude) (deleteObjects base magnitude)" - apply (simp add: deleteObjects_def2) - apply (rule corres_stateAssert_implied[where P'=\, simplified]) - prefer 2 - apply clarsimp - apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and - s=s in detype_locale'.deletionIsSafe, - simp_all add: detype_locale'_def - detype_locale_def p_assoc_help invs_valid_pspace)[1] - apply (simp add:valid_cap_simps) - apply (simp add: bind_assoc[symmetric]) - apply (rule corres_stateAssert_implied2) - defer - apply (erule ksASIDMapSafeI, assumption, assumption) - apply (rule hoare_pre) - apply (rule delete_objects_invs) - apply fastforce - apply (simp add: doMachineOp_def split_def) - apply wp - apply (clarsimp simp: valid_pspace'_def pspace_distinct'_def - pspace_aligned'_def) - apply (rule conjI) - subgoal by fastforce - apply (clarsimp simp add: pspace_distinct'_def ps_clear_def - dom_if_None Diff_Int_distrib) - apply (simp add: delete_objects_def) - apply (rule_tac Q="\_ s. valid_objs s \ valid_list s \ - (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ - descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ - s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ - valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ - zombies_final s \ sym_refs (state_refs_of s) \ - untyped_children_in_mdb s \ if_unsafe_then_cap s \ - valid_global_refs s" and - Q'="\_ s. s \' capability.UntypedCap d base magnitude idx \ - valid_pspace' s" in corres_underlying_split) - apply (rule corres_bind_return) - apply (rule corres_guard_imp[where r=dc]) - apply (rule corres_split[OF _ cNodeNoPartialOverlap]) - apply (rule corres_machine_op[OF corres_Id], simp+) - apply (rule no_fail_freeMemory, simp+) - apply (wp hoare_vcg_ex_lift)+ - apply auto[1] - apply (auto elim: is_aligned_weaken) - apply (rule corres_modify) - apply (simp add: valid_pspace'_def) - apply (rule state_relation_null_filterE, assumption, - simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] - apply (simp add: detype_def, rule state.equality; simp add: detype_ext_def) - apply (intro exI, fastforce) - apply (rule ext, clarsimp simp add: null_filter_def) - apply (rule sym, rule ccontr, clarsimp) - apply (drule(4) cte_map_not_null_outside') - apply (fastforce simp add: cte_wp_at_caps_of_state) - apply simp - apply (rule ext, clarsimp simp add: null_filter'_def - map_to_ctes_delete[simplified field_simps]) - apply (rule sym, rule ccontr, clarsimp) - apply (frule(2) pspace_relation_cte_wp_atI - [OF state_relation_pspace_relation]) - apply (elim exE) - apply (frule(4) cte_map_not_null_outside') - apply (rule cte_wp_at_weakenE, erule conjunct1) - apply (case_tac y, clarsimp) - apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def - valid_nullcaps_def) - apply clarsimp - apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, - erule cte_wp_at_weakenE[OF _ TrueI], assumption+) - apply simp - apply (rule detype_pspace_relation[simplified], - simp_all add: state_relation_pspace_relation valid_pspace_def)[1] - apply (simp add: valid_cap'_def capAligned_def) - apply (clarsimp simp: valid_cap_def, assumption) - apply (fastforce simp add: detype_def detype_ext_def intro!: ekheap_relation_detype) - apply (clarsimp simp: state_relation_def ghost_relation_of_heap - detype_def) - apply (drule_tac t="gsUserPages s'" in sym) - apply (drule_tac t="gsCNodes s'" in sym) - apply (auto simp add: ups_of_heap_def cns_of_heap_def ext - split: option.splits kernel_object.splits)[1] - apply (simp add: valid_mdb_def) - apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | - simp add: invs_def valid_state_def valid_pspace_def - descendants_range_def | wp (once) hoare_drop_imps)+ - done +context begin interpretation Arch . (*FIXME: arch_split*) text \Invariant preservation across concrete deletion\ @@ -747,85 +567,87 @@ lemma sym_refs_ko_wp_atD: lemma zobj_refs_capRange: "capAligned c \ zobj_refs' c \ capRange c" by (cases c, simp_all add: capRange_def capAligned_def is_aligned_no_overflow) + end + locale delete_locale = - fixes s and base and bits and ptr and idx and d - assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s" - and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s)" - and invs: "invs' s" - and ct_act: "ct_active' s" - and sa_simp: "sch_act_simple s" - and bwb: "bits < word_bits" + fixes s' and base and bits and ptr and idx and d + assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s'" + and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s')" + and invs: "invs' s'" + and ct_act: "ct_active' s'" + and sa_simp: "sch_act_simple s'" and al: "is_aligned base bits" - and safe: "deletionIsSafe base bits s" - -context delete_locale -begin -interpretation Arch . (*FIXME: arch_split*) -lemma valid_objs: "valid_objs' s" - and pa: "pspace_aligned' s" - and pd: "pspace_distinct' s" - and vq: "valid_queues s" - and vq': "valid_queues' s" - and sym_refs: "sym_refs (state_refs_of' s)" - and iflive: "if_live_then_nonz_cap' s" - and ifunsafe: "if_unsafe_then_cap' s" - and dlist: "valid_dlist (ctes_of s)" - and no_0: "no_0 (ctes_of s)" - and chain_0: "mdb_chain_0 (ctes_of s)" - and badges: "valid_badges (ctes_of s)" - and contained: "caps_contained' (ctes_of s)" - and chunked: "mdb_chunked (ctes_of s)" - and umdb: "untyped_mdb' (ctes_of s)" - and uinc: "untyped_inc' (ctes_of s)" - and nullcaps: "valid_nullcaps (ctes_of s)" - and ut_rev: "ut_revocable' (ctes_of s)" - and dist_z: "distinct_zombies (ctes_of s)" - and irq_ctrl: "irq_control (ctes_of s)" - and clinks: "class_links (ctes_of s)" - and rep_r_fb: "reply_masters_rvk_fb (ctes_of s)" - and idle: "valid_idle' s" - and refs: "valid_global_refs' s" - and arch: "valid_arch_state' s" - and virq: "valid_irq_node' (irq_node' s) s" - and virqh: "valid_irq_handlers' s" - and virqs: "valid_irq_states' s" - and no_0_objs: "no_0_obj' s" - and ctnotinQ: "ct_not_inQ s" - and pde_maps: "valid_pde_mappings' s" - and irqs_masked: "irqs_masked' s" - and ctcd: "ct_idle_or_in_cur_domain' s" - and cdm: "ksCurDomain s \ maxDomain" - and vds: "valid_dom_schedule' s" + and safe: "deletionIsSafe base bits s'" + +context delete_locale begin interpretation Arch . (*FIXME: arch_split*) + +lemma valid_objs: "valid_objs' s'" + and pa: "pspace_aligned' s'" + and pd: "pspace_distinct' s'" + and vq: "valid_queues s'" + and vq': "valid_queues' s'" + and sym_refs: "sym_refs (state_refs_of' s')" + and iflive: "if_live_then_nonz_cap' s'" + and ifunsafe: "if_unsafe_then_cap' s'" + and dlist: "valid_dlist (ctes_of s')" + and no_0: "no_0 (ctes_of s')" + and chain_0: "mdb_chain_0 (ctes_of s')" + and badges: "valid_badges (ctes_of s')" + and contained: "caps_contained' (ctes_of s')" + and chunked: "mdb_chunked (ctes_of s')" + and umdb: "untyped_mdb' (ctes_of s')" + and uinc: "untyped_inc' (ctes_of s')" + and nullcaps: "valid_nullcaps (ctes_of s')" + and ut_rev: "ut_revocable' (ctes_of s')" + and dist_z: "distinct_zombies (ctes_of s')" + and irq_ctrl: "irq_control (ctes_of s')" + and clinks: "class_links (ctes_of s')" + and rep_r_fb: "reply_masters_rvk_fb (ctes_of s')" + and idle: "valid_idle' s'" + and refs: "valid_global_refs' s'" + and arch: "valid_arch_state' s'" + and virq: "valid_irq_node' (irq_node' s') s'" + and virqh: "valid_irq_handlers' s'" + and virqs: "valid_irq_states' s'" + and no_0_objs: "no_0_obj' s'" + and ctnotinQ: "ct_not_inQ s'" + and pde_maps: "valid_pde_mappings' s'" + and irqs_masked: "irqs_masked' s'" + and ctcd: "ct_idle_or_in_cur_domain' s'" + and cdm: "ksCurDomain s' \ maxDomain" + and vds: "valid_dom_schedule' s'" using invs - by (auto simp add: invs'_def valid_state'_def valid_pspace'_def - valid_mdb'_def valid_mdb_ctes_def) + by (auto simp: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) abbreviation "base_bits \ {base .. base + (2 ^ bits - 1)}" -abbreviation - "state' \ (s \ ksPSpace := \x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s x \)" +abbreviation pspace' :: pspace where + "pspace' \ \x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s' x" + +abbreviation state' :: kernel_state where + "state' \ (s' \ ksPSpace := pspace' \)" lemma ko_wp_at'[simp]: - "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s \ p \ base_bits)" + "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s' \ p \ base_bits)" by (fastforce simp add: ko_wp_at_delete'[OF pd]) lemma obj_at'[simp]: - "\P p. (obj_at' P p state') = (obj_at' P p s \ p \ base_bits)" + "\P p. (obj_at' P p state') = (obj_at' P p s' \ p \ base_bits)" by (fastforce simp add: obj_at'_real_def) lemma typ_at'[simp]: - "\T p. (typ_at' P p state') = (typ_at' P p s \ p \ base_bits)" + "typ_at' P p state' = (typ_at' P p s' \ p \ base_bits)" by (simp add: typ_at'_def) lemma valid_untyped[simp]: - "s \' UntypedCap d base bits idx" + "s' \' UntypedCap d base bits idx" using cte_wp_at_valid_objs_valid_cap' [OF cap valid_objs] by clarsimp lemma cte_wp_at'[simp]: - "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s \ p \ base_bits)" + "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s' \ p \ base_bits)" by (fastforce simp:cte_wp_at_delete'[where idx = idx,OF valid_untyped pd ]) (* the bits of caps they need for validity argument are within their capRanges *) @@ -854,13 +676,13 @@ lemma valid_cap_ctes_pre: done lemma replycap_argument: - "\p t m r. cte_wp_at' (\cte. cteCap cte = ReplyCap t m r) p s + "\p t m r. cte_wp_at' (\cte. cteCap cte = ReplyCap t m r) p s' \ t \ {base .. base + (2 ^ bits - 1)}" using safe by (fastforce simp add: deletionIsSafe_def cte_wp_at_ctes_of field_simps) lemma valid_cap': - "\p c. \ s \' c; cte_wp_at' (\cte. cteCap cte = c) p s; + "\p c. \ s' \' c; cte_wp_at' (\cte. cteCap cte = c) p s'; capRange c \ {base .. base + (2 ^ bits - 1)} = {} \ \ state' \' c" apply (subgoal_tac "capClass c = PhysicalClass \ capUntypedPtr c \ capRange c") apply (subgoal_tac "capClass c = PhysicalClass \ @@ -902,11 +724,11 @@ lemma valid_cap': done lemma objRefs_notrange: - assumes asms: "ctes_of s p = Some c" "\ isUntypedCap (cteCap c)" + assumes asms: "ctes_of s' p = Some c" "\ isUntypedCap (cteCap c)" shows "capRange (cteCap c) \ base_bits = {}" proof - from cap obtain node - where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" + where ctes_of: "ctes_of s' ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done @@ -927,11 +749,11 @@ proof - qed lemma ctes_of_valid [elim!]: - "ctes_of s p = Some cte \ s \' cteCap cte" + "ctes_of s' p = Some cte \ s' \' cteCap cte" by (case_tac cte, simp add: ctes_of_valid_cap' [OF _ valid_objs]) lemma valid_cap2: - "\ cte_wp_at' (\cte. cteCap cte = c) p s \ \ state' \' c" + "\ cte_wp_at' (\cte. cteCap cte = c) p s' \ \ state' \' c" apply (case_tac "isUntypedCap c") apply (drule cte_wp_at_valid_objs_valid_cap' [OF _ valid_objs]) apply (clarsimp simp: valid_cap'_def isCap_simps valid_untyped'_def) @@ -941,7 +763,7 @@ lemma valid_cap2: done lemma ex_nonz_cap_notRange: - "ex_nonz_cap_to' p s \ p \ base_bits" + "ex_nonz_cap_to' p s' \ p \ base_bits" apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (case_tac "isUntypedCap (cteCap cte)") apply (clarsimp simp: isCap_simps) @@ -953,22 +775,237 @@ lemma ex_nonz_cap_notRange: done lemma live_notRange: - "\ ko_wp_at' P p s; \ko. P ko \ live' ko \ \ p \ base_bits" + "\ ko_wp_at' P p s'; \ko. P ko \ live' ko \ \ p \ base_bits" apply (drule if_live_then_nonz_capE' [OF iflive ko_wp_at'_weakenE]) apply simp apply (erule ex_nonz_cap_notRange) done +lemma deletionIsSafe_delete_locale_holds: + "deletionIsSafe_delete_locale base bits s'" + by (fastforce dest: live_notRange simp: deletionIsSafe_delete_locale_def field_simps) + lemma refs_notRange: - "(x, tp) \ state_refs_of' s y \ y \ base_bits" + "(x, tp) \ state_refs_of' s' y \ y \ base_bits" apply (drule state_refs_of'_elemD) apply (erule live_notRange) apply (rule refs_of_live') apply clarsimp done +end + +context begin interpretation Arch . (*FIXME: arch_split*) + +lemma ksASIDMapSafeI: + "\ (s,s') \ state_relation; invs s; pspace_aligned' s' \ pspace_distinct' s' \ + \ ksASIDMapSafe s'" + apply (clarsimp simp: ksASIDMapSafe_def) + apply (subgoal_tac "valid_asid_map s") + prefer 2 + apply fastforce + apply (clarsimp simp: valid_asid_map_def graph_of_def) + apply (subgoal_tac "arm_asid_map (arch_state s) asid = Some (hw_asid, pd)") + prefer 2 + apply (clarsimp simp: state_relation_def arch_state_relation_def) + apply (erule allE)+ + apply (erule (1) impE) + apply clarsimp + apply (drule find_pd_for_asid_eq_helper) + apply fastforce + apply assumption + apply fastforce + apply clarsimp + apply (rule pspace_relation_pd) + apply (fastforce simp: state_relation_def) + apply fastforce + apply assumption + apply assumption + apply simp + done + +(* FIXME: generalizes lemma SubMonadLib.corres_submonad *) +(* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) +(* FIXME: move *) +lemma corres_machine_op: + assumes P: "corres_underlying Id False True r P Q x x'" + shows "corres r (P \ machine_state) (Q \ ksMachineState) + (do_machine_op x) (doMachineOp x')" + apply (rule corres_submonad3 + [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) + apply (simp_all add: state_relation_def swp_def) + done + +lemma ekheap_relation_detype: + "ekheap_relation ekh kh \ + ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" + by (fastforce simp add: ekheap_relation_def split: if_split_asm) + +lemma cap_table_at_gsCNodes_eq: + "(s, s') \ state_relation + \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" + apply (clarsimp simp: state_relation_def ghost_relation_def + obj_at_def is_cap_table) + apply (drule_tac x = ptr in spec)+ + apply (drule_tac x = bits in spec)+ + apply fastforce + done + +lemma cNodeNoPartialOverlap: + "corres dc (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s + \ valid_objs s \ pspace_aligned s) + \ + (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) + (\x. base \ x \ x \ base + 2 ^ magnitude - 1)) [])" + apply (simp add: stateAssert_def assert_def) + apply (rule corres_symb_exec_r[OF _ get_sp]) + apply (rule corres_req[rotated], subst if_P, assumption) + apply simp + apply (clarsimp simp: cNodePartialOverlap_def) + apply (drule(1) cte_wp_valid_cap) + apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq + obj_at_def is_cap_table) + apply (frule(1) pspace_alignedD) + apply simp + apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) + apply (erule is_aligned_get_word_bits[where 'a=32, folded word_bits_def]) + apply (clarsimp simp: is_aligned_no_overflow) + apply (blast intro: order_trans) + apply (simp add: is_aligned_no_overflow power_overflow word_bits_def) + apply wp+ + done + +declare wrap_ext_det_ext_ext_def[simp] + +lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s)" + apply (auto simp: state_hyp_refs_of_def sym_refs_def) + apply (case_tac "kheap s x"; simp add: hyp_refs_of_def) + apply (rename_tac ko) + apply (case_tac ko; clarsimp) + done + +crunches doMachineOp + for deletionIsSafe_delete_locale[wp]: "deletionIsSafe_delete_locale base magnitude" + (simp: deletionIsSafe_delete_locale_def) + +lemma deleteObjects_corres: + "is_aligned base magnitude \ magnitude \ 2 \ + corres dc + (\s. einvs s + \ s \ (cap.UntypedCap d base magnitude idx) + \ (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s + \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) + \ untyped_children_in_mdb s \ if_unsafe_then_cap s + \ valid_mdb s \ valid_global_refs s \ ct_active s + \ schact_is_rct s) + (\s'. invs' s' + \ cte_wp_at' (\cte. cteCap cte = UntypedCap d base magnitude idx) ptr s' + \ descendants_range' (UntypedCap d base magnitude idx) ptr (ctes_of s') + \ ct_active' s' + \ s' \' (UntypedCap d base magnitude idx)) + (delete_objects base magnitude) (deleteObjects base magnitude)" + apply (simp add: deleteObjects_def2) + apply (rule corres_stateAssert_implied[where P'=\, simplified]) + prefer 2 + apply clarsimp + apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and + s=s in detype_locale'.deletionIsSafe, + simp_all add: detype_locale'_def + detype_locale_def p_assoc_help invs_valid_pspace)[1] + apply (simp add:valid_cap_simps) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe_delete_locale_holds) + apply (clarsimp simp: delete_locale_def) + apply (intro conjI) + apply (fastforce simp: sch_act_simple_def state_relation_def schact_is_rct_def) + apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and s=s + in detype_locale'.deletionIsSafe, + simp_all add: detype_locale'_def detype_locale_def invs_valid_pspace)[1] + apply (simp add:valid_cap_simps) + apply (simp add: bind_assoc[symmetric]) + apply (rule corres_stateAssert_implied2) + defer + apply (erule ksASIDMapSafeI, assumption, assumption) + apply (rule hoare_pre) + apply (rule delete_objects_invs) + apply fastforce + apply (simp add: doMachineOp_def split_def) + apply wp + apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def pspace_distinct'_def + pspace_aligned'_def) + apply (rule conjI) + subgoal by fastforce + apply (clarsimp simp add: pspace_distinct'_def ps_clear_def + dom_if_None Diff_Int_distrib) + apply (simp add: delete_objects_def) + apply (rule_tac Q="\_ s. valid_objs s \ valid_list s \ + (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ + descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ + s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ + valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ + zombies_final s \ sym_refs (state_refs_of s) \ + untyped_children_in_mdb s \ if_unsafe_then_cap s \ + valid_global_refs s" and + Q'="\_ s. s \' capability.UntypedCap d base magnitude idx \ + valid_pspace' s" in corres_underlying_split) + apply (rule corres_bind_return) + apply (rule corres_guard_imp[where r=dc]) + apply (rule corres_split[OF _ cNodeNoPartialOverlap]) + apply (rule corres_machine_op[OF corres_Id], simp+) + apply (rule no_fail_freeMemory, simp+) + apply (wp hoare_vcg_ex_lift)+ + apply auto[1] + apply (auto elim: is_aligned_weaken) + apply (rule corres_modify) + apply (simp add: valid_pspace'_def) + apply (rule state_relation_null_filterE, assumption, + simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] + apply (simp add: detype_def, rule state.equality; simp add: detype_ext_def) + apply (intro exI, fastforce) + apply (rule ext, clarsimp simp add: null_filter_def) + apply (rule sym, rule ccontr, clarsimp) + apply (drule(4) cte_map_not_null_outside') + apply (fastforce simp add: cte_wp_at_caps_of_state) + apply simp + apply (rule ext, clarsimp simp add: null_filter'_def + map_to_ctes_delete[simplified field_simps]) + apply (rule sym, rule ccontr, clarsimp) + apply (frule(2) pspace_relation_cte_wp_atI + [OF state_relation_pspace_relation]) + apply (elim exE) + apply (frule(4) cte_map_not_null_outside') + apply (rule cte_wp_at_weakenE, erule conjunct1) + apply (case_tac y, clarsimp) + apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def + valid_nullcaps_def) + apply clarsimp + apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, + erule cte_wp_at_weakenE[OF _ TrueI], assumption+) + apply simp + apply (rule detype_pspace_relation[simplified], + simp_all add: state_relation_pspace_relation valid_pspace_def)[1] + apply (simp add: valid_cap'_def capAligned_def) + apply (clarsimp simp: valid_cap_def, assumption) + apply (fastforce simp add: detype_def detype_ext_def intro!: ekheap_relation_detype) + apply (clarsimp simp: state_relation_def ghost_relation_of_heap + detype_def) + apply (drule_tac t="gsUserPages s'" in sym) + apply (drule_tac t="gsCNodes s'" in sym) + apply (auto simp add: ups_of_heap_def cns_of_heap_def ext + split: option.splits kernel_object.splits)[1] + apply (simp add: valid_mdb_def) + apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | + simp add: invs_def valid_state_def valid_pspace_def + descendants_range_def | wp (once) hoare_drop_imps)+ + apply fastforce + done + +end + +context delete_locale begin interpretation Arch . (*FIXME: arch_split*) + lemma valid_obj': - "\ valid_obj' obj s; ko_wp_at' ((=) obj) p s \ \ valid_obj' obj state'" + "\ valid_obj' obj s'; ko_wp_at' ((=) obj) p s' \ \ valid_obj' obj state'" apply (case_tac obj, simp_all add: valid_obj'_def) apply (rename_tac endpoint) apply (case_tac endpoint, simp_all add: valid_ep'_def)[1] @@ -1015,17 +1052,15 @@ lemma valid_obj': done lemma st_tcb: - "\P p. \ st_tcb_at' P p s; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" - by (fastforce simp: pred_tcb_at'_def obj_at'_real_def - projectKOs - dest: live_notRange) + "\P p. \ st_tcb_at' P p s'; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" + by (fastforce simp: pred_tcb_at'_def obj_at'_real_def projectKOs dest: live_notRange) lemma irq_nodes_global: - "\irq :: 10 word. irq_node' s + (ucast irq) * 16 \ global_refs' s" - by (simp add: global_refs'_def mult.commute mult.left_commute cteSizeBits_def shiftl_t2n) + "\irq :: 10 word. irq_node' s' + (ucast irq) * 16 \ global_refs' s'" + by (simp add: global_refs'_def mult.commute mult.left_commute cteSizeBits_def shiftl_t2n) lemma global_refs: - "global_refs' s \ base_bits = {}" + "global_refs' s' \ base_bits = {}" using cap apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule valid_global_refsD' [OF _ refs]) @@ -1033,20 +1068,20 @@ lemma global_refs: done lemma global_refs2: - "global_refs' s \ (- base_bits)" + "global_refs' s' \ (- base_bits)" using global_refs by blast lemma irq_nodes_range: - "\irq :: 10 word. irq_node' s + (ucast irq) * 16 \ base_bits" + "\irq :: 10 word. irq_node' s' + (ucast irq) * 16 \ base_bits" using irq_nodes_global global_refs by blast lemma cte_refs_notRange: - assumes asms: "ctes_of s p = Some c" - shows "cte_refs' (cteCap c) (irq_node' s) \ base_bits = {}" + assumes asms: "ctes_of s' p = Some c" + shows "cte_refs' (cteCap c) (irq_node' s') \ base_bits = {}" proof - from cap obtain node - where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" + where ctes_of: "ctes_of s' ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done @@ -1075,7 +1110,7 @@ proof - qed lemma non_null_present: - "cte_wp_at' (\c. cteCap c \ NullCap) p s \ p \ base_bits" + "cte_wp_at' (\c. cteCap c \ NullCap) p s' \ p \ base_bits" apply (drule (1) if_unsafe_then_capD' [OF _ ifunsafe]) apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of dest!: cte_refs_notRange simp del: atLeastAtMost_iff) @@ -1083,7 +1118,7 @@ lemma non_null_present: done lemma cte_cap: - "ex_cte_cap_to' p s \ ex_cte_cap_to' p state'" + "ex_cte_cap_to' p s' \ ex_cte_cap_to' p state'" apply (clarsimp simp: ex_cte_cap_to'_def) apply (frule non_null_present [OF cte_wp_at_weakenE']) apply clarsimp @@ -1091,37 +1126,37 @@ lemma cte_cap: done lemma idle_notRange: - "\cref. \ cte_wp_at' (\c. ksIdleThread s \ capRange (cteCap c)) cref s - \ ksIdleThread s \ base_bits" + "\cref. \ cte_wp_at' (\c. ksIdleThread s' \ capRange (cteCap c)) cref s' + \ ksIdleThread s' \ base_bits" apply (insert cap) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule_tac x=ptr in allE, clarsimp simp: field_simps) done abbreviation - "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s x)" + "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s' x)" lemmas tree_to_ctes = map_to_ctes_delete [OF valid_untyped pd] lemma map_to_ctesE[elim!]: - "\ ctes' x = Some cte; \ ctes_of s x = Some cte; x \ base_bits \ \ P \ \ P" + "\ ctes' x = Some cte; \ ctes_of s' x = Some cte; x \ base_bits \ \ P \ \ P" by (clarsimp simp: tree_to_ctes split: if_split_asm) lemma not_nullMDBNode: - "\ ctes_of s x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" + "\ ctes_of s' x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" using nullcaps apply (cases cte) apply (simp add: valid_nullcaps_def) done -lemma mdb_src: "\ ctes_of s \ x \ y; y \ 0 \ \ x \ base_bits" +lemma mdb_src: "\ ctes_of s' \ x \ y; y \ 0 \ \ x \ base_bits" apply (rule non_null_present) apply (clarsimp simp: next_unfold' cte_wp_at_ctes_of) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def) done -lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ \ y \ base_bits" +lemma mdb_dest: "\ ctes_of s' \ x \ y; y \ 0 \ \ y \ base_bits" apply (case_tac "x = 0") apply (insert no_0, simp add: next_unfold')[1] apply (drule(1) vdlist_nextD0 [OF _ _ dlist]) @@ -1132,7 +1167,7 @@ lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ done lemma trancl_next[elim]: - "\ ctes_of s \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" + "\ ctes_of s' \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" apply (erule rev_mp, erule converse_trancl_induct) apply clarsimp apply (rule r_into_trancl) @@ -1150,14 +1185,14 @@ lemma trancl_next[elim]: done lemma mdb_parent_notrange: - "ctes_of s \ x \ y \ x \ base_bits \ y \ base_bits" + "ctes_of s' \ x \ y \ x \ base_bits \ y \ base_bits" apply (erule subtree.induct) apply (frule(1) mdb_src, drule(1) mdb_dest, simp) apply (drule(1) mdb_dest, simp) done lemma mdb_parent: - "ctes_of s \ x \ y \ ctes' \ x \ y" + "ctes_of s' \ x \ y \ ctes' \ x \ y" apply (erule subtree.induct) apply (frule(1) mdb_src, frule(1) mdb_dest) apply (rule subtree.direct_parent) @@ -1173,7 +1208,7 @@ lemma mdb_parent: done lemma trancl_next_rev: - "ctes' \ x \\<^sup>+ y \ ctes_of s \ x \\<^sup>+ y" + "ctes' \ x \\<^sup>+ y \ ctes_of s' \ x \\<^sup>+ y" apply (erule converse_trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp: next_unfold') @@ -1183,7 +1218,7 @@ lemma trancl_next_rev: done lemma is_chunk[elim!]: - "is_chunk (ctes_of s) cap x y \ is_chunk ctes' cap x y" + "is_chunk (ctes_of s') cap x y \ is_chunk ctes' cap x y" apply (simp add: is_chunk_def) apply (erule allEI) apply (clarsimp dest!: trancl_next_rev) @@ -1272,7 +1307,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def intro!: cte_cap) from idle_notRange refs - have "ksIdleThread s \ ?ran" + have "ksIdleThread s' \ ?ran" apply (simp add: cte_wp_at_ctes_of valid_global_refs'_def valid_refs'_def) apply blast done @@ -1387,7 +1422,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def page_directory_at'_def) by fastforce - show "valid_irq_node' (irq_node' s) ?s" + show "valid_irq_node' (irq_node' s') ?s" using virq irq_nodes_range by (simp add: valid_irq_node'_def mult.commute mult.left_commute ucast_ucast_mask_8 cteSizeBits_def shiftl_t2n) @@ -1418,7 +1453,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def ball_ran_eq) from virqs - show "valid_irq_states' s" . + show "valid_irq_states' s'" . from no_0_objs show "no_0_obj' state'" @@ -1433,19 +1468,19 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def by (simp add: irqs_masked'_def) from sa_simp ct_act - show "sch_act_wf (ksSchedulerAction s) state'" + show "sch_act_wf (ksSchedulerAction s') state'" apply (simp add: sch_act_simple_def) - apply (case_tac "ksSchedulerAction s", simp_all add: ct_in_state'_def) + apply (case_tac "ksSchedulerAction s'", simp_all add: ct_in_state'_def) apply (fastforce dest!: st_tcb elim!: pred_tcb'_weakenE) done from invs - have "pspace_domain_valid s" by (simp add: invs'_def valid_state'_def) + have "pspace_domain_valid s'" by (simp add: invs'_def valid_state'_def) thus "pspace_domain_valid state'" by (simp add: pspace_domain_valid_def) from invs - have "valid_machine_state' s" by (simp add: invs'_def valid_state'_def) + have "valid_machine_state' s'" by (simp add: invs'_def valid_state'_def) thus "valid_machine_state' ?state''" apply (clarsimp simp: valid_machine_state'_def) apply (drule_tac x=p in spec) @@ -1500,12 +1535,12 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def apply (clarsimp dest!: ex_nonz_cap_notRange elim!: ko_wp_at'_weakenE) done - from cdm show "ksCurDomain s \ maxDomain" . + from cdm show "ksCurDomain s' \ maxDomain" . from invs - have urz: "untyped_ranges_zero' s" by (simp add: invs'_def valid_state'_def) + have urz: "untyped_ranges_zero' s'" by (simp add: invs'_def valid_state'_def) show "untyped_ranges_zero_inv (cteCaps_of state') - (gsUntypedZeroRanges s)" + (gsUntypedZeroRanges s')" apply (simp add: untyped_zero_ranges_cte_def urz[unfolded untyped_zero_ranges_cte_def, rule_format, symmetric]) apply (clarsimp simp: fun_eq_iff intro!: arg_cong[where f=Ex]) @@ -1518,14 +1553,14 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def qed (clarsimp) lemma (in delete_locale) delete_ko_wp_at': - assumes objs: "ko_wp_at' P p s \ ex_nonz_cap_to' p s" + assumes objs: "ko_wp_at' P p s' \ ex_nonz_cap_to' p s'" shows "ko_wp_at' P p state'" using objs by (clarsimp simp: ko_wp_at'_def ps_clear_def dom_if_None Diff_Int_distrib dest!: ex_nonz_cap_notRange) lemma (in delete_locale) null_filter': - assumes descs: "Q (null_filter' (ctes_of s))" + assumes descs: "Q (null_filter' (ctes_of s'))" shows "Q (null_filter' (ctes_of state'))" using descs ifunsafe apply (clarsimp elim!: rsubst[where P=Q]) @@ -1543,7 +1578,7 @@ lemma (in delete_locale) null_filter': done lemma (in delete_locale) delete_ex_cte_cap_to': - assumes exc: "ex_cte_cap_to' p s" + assumes exc: "ex_cte_cap_to' p s'" shows "ex_cte_cap_to' p state'" using exc by (clarsimp elim!: cte_cap) diff --git a/proof/refine/ARM/EmptyFail_H.thy b/proof/refine/ARM/EmptyFail_H.thy index 19a71ee079..8b00db6c5a 100644 --- a/proof/refine/ARM/EmptyFail_H.thy +++ b/proof/refine/ARM/EmptyFail_H.thy @@ -264,7 +264,7 @@ crunch (empty_fail) empty_fail: callKernel theorem call_kernel_serial: "\ (einvs and (\s. event \ Interrupt \ ct_running s) and (ct_running or ct_idle) and - (\s. scheduler_action s = resume_cur_thread) and + schact_is_rct and (\s. 0 < domain_time s \ valid_domain_list s)) s; \s'. (s, s') \ state_relation \ (invs' and (\s. event \ Interrupt \ ct_running' s) and (ct_running' or ct_idle') and diff --git a/proof/refine/ARM/Refine.thy b/proof/refine/ARM/Refine.thy index 1869430383..07192b70f0 100644 --- a/proof/refine/ARM/Refine.thy +++ b/proof/refine/ARM/Refine.thy @@ -585,7 +585,7 @@ lemma kernel_corres': E="\_. valid_sched and invs and valid_list" in hoare_post_impErr) apply (wp handle_event_valid_sched hoare_vcg_imp_lift' |simp)+ - apply (clarsimp simp: active_from_running) + apply (clarsimp simp: active_from_running schact_is_rct_def) apply (clarsimp simp: active_from_running') done @@ -662,6 +662,7 @@ lemma entry_corres: thread_set_not_state_valid_sched hoare_weak_lift_imp hoare_vcg_disj_lift ct_in_state_thread_state_lift | simp add: tcb_cap_cases_def ct_in_state'_def thread_set_no_change_tcb_state + schact_is_rct_def | (wps, wp threadSet_st_tcb_at2) )+ apply (clarsimp simp: invs_def cur_tcb_def) apply (clarsimp simp: ct_in_state'_def) diff --git a/proof/refine/ARM/Syscall_R.thy b/proof/refine/ARM/Syscall_R.thy index 81515e8b1d..6f8a7b6e96 100644 --- a/proof/refine/ARM/Syscall_R.thy +++ b/proof/refine/ARM/Syscall_R.thy @@ -390,7 +390,7 @@ lemma performInvocation_corres: "\ inv_relation i i'; call \ block \ \ corres (dc \ (=)) (einvs and valid_invocation i - and simple_sched_action + and schact_is_rct and ct_active and (\s. (\w w2 b c. i = Invocations_A.InvokeEndpoint w w2 b c) \ st_tcb_at simple (cur_thread s) s)) (invs' and sch_act_simple and valid_invocation' i' and ct_active' and (\s. vs_valid_duplicates' (ksPSpace s))) @@ -440,7 +440,7 @@ lemma performInvocation_corres: apply (clarsimp simp: liftME_def) apply (rule corres_guard_imp) apply (erule invokeTCB_corres) - apply (simp)+ + apply ((clarsimp dest!: schact_is_rct_simple)+)[2] \ \domain cap\ apply (clarsimp simp: invoke_domain_def) apply (rule corres_guard_imp) @@ -455,7 +455,7 @@ lemma performInvocation_corres: apply assumption apply (rule corres_trivial, simp add: returnOk_def) apply wp+ - apply (clarsimp+)[2] + apply ((clarsimp dest!: schact_is_rct_simple)+)[2] apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric]) apply (rule corres_guard_imp, rule performIRQControl_corres, simp+) apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric]) @@ -1205,7 +1205,7 @@ crunch valid_duplicates'[wp]: setThreadState "\s. vs_valid_duplicates' ( lemma handleInvocation_corres: "c \ b \ corres (dc \ dc) - (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + (einvs and schact_is_rct and ct_active) (invs' and (\s. vs_valid_duplicates' (ksPSpace s)) and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_invocation c b) @@ -1255,14 +1255,14 @@ lemma handleInvocation_corres: apply simp apply wp apply simp - apply (rule_tac Q="\rv. einvs and simple_sched_action and valid_invocation rve + apply (rule_tac Q="\rv. einvs and schact_is_rct and valid_invocation rve and (\s. thread = cur_thread s) and st_tcb_at active thread" in hoare_post_imp) apply (clarsimp simp: simple_from_active ct_in_state_def elim!: st_tcb_weakenE) - apply (wp sts_st_tcb_at' set_thread_state_simple_sched_action - set_thread_state_active_valid_sched) + apply (wp sts_st_tcb_at' set_thread_state_schact_is_rct + set_thread_state_active_valid_sched) apply (rule_tac Q="\rv. invs' and valid_invocation' rve' and (\s. thread = ksCurThread s) and st_tcb_at' active' thread @@ -1368,7 +1368,7 @@ lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at'] lemma handleSend_corres: "corres (dc \ dc) - (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + (einvs and schact_is_rct and ct_active) (invs' and (\s. vs_valid_duplicates' (ksPSpace s)) and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_send blocking) (handleSend blocking)" @@ -1804,7 +1804,7 @@ lemma hr_ct_active'[wp]: done lemma handleCall_corres: - "corres (dc \ dc) (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + "corres (dc \ dc) (einvs and schact_is_rct and ct_active) (invs' and (\s. vs_valid_duplicates' (ksPSpace s)) and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') @@ -1985,7 +1985,7 @@ lemma handleHypervisorFault_corres: (* FIXME: move *) lemma handleEvent_corres: "corres (dc \ dc) (einvs and (\s. event \ Interrupt \ ct_running s) and - (\s. scheduler_action s = resume_cur_thread)) + schact_is_rct) (invs' and (\s. event \ Interrupt \ ct_running' s) and (\s. vs_valid_duplicates' (ksPSpace s)) and (\s. ksSchedulerAction s = ResumeCurrentThread)) @@ -2056,8 +2056,6 @@ proof - doMachineOp_getActiveIRQ_IRQ_active' | simp | simp add: imp_conjR | wp (once) hoare_drop_imps)+ - apply force - apply simp apply (simp add: invs'_def valid_state'_def) apply (rule_tac corres_underlying_split) apply (rule corres_guard_imp, rule getCurThread_corres, simp+) diff --git a/proof/refine/ARM/Untyped_R.thy b/proof/refine/ARM/Untyped_R.thy index a1216e7438..a0e2af4f1b 100644 --- a/proof/refine/ARM/Untyped_R.thy +++ b/proof/refine/ARM/Untyped_R.thy @@ -4173,7 +4173,7 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemma resetUntypedCap_corres: "untypinv_relation ui ui' \ corres (dc \ dc) - (invs and valid_untyped_inv_wcap ui + (invs and schact_is_rct and valid_untyped_inv_wcap ui (Some (cap.UntypedCap dev ptr sz idx)) and ct_active and einvs and (\_. \ptr_base ptr' ty us slots dev'. ui = Invocations_A.Retype slot True @@ -4331,7 +4331,7 @@ lemma resetUntypedCap_corres: apply (frule if_unsafe_then_capD'[OF ctes_of_cte_wpD], clarsimp+) apply (frule(1) descendants_range_ex_cte'[OF empty_descendants_range_in' _ order_refl], (simp add: isCap_simps)+) - apply (intro conjI impI; clarsimp) + apply (auto simp: descendants_range_in'_def valid_untyped'_def) done end @@ -4609,7 +4609,7 @@ defs archOverlap_def: lemma inv_untyped_corres': "\ untypinv_relation ui ui' \ \ corres (dc \ (=)) - (einvs and valid_untyped_inv ui and ct_active) + (einvs and valid_untyped_inv ui and ct_active and schact_is_rct) (invs' and valid_untyped_inv' ui' and ct_active') (invoke_untyped ui) (invokeUntyped ui')" apply (cases ui) @@ -4628,6 +4628,7 @@ lemma inv_untyped_corres': (cte_map cref) reset ptr_base ptr ao' us (map cte_map slots) dev" assume invs: "invs (s :: det_state)" "ct_active s" "valid_list s" "valid_sched s" + "schact_is_rct s" and invs': "invs' s'" "ct_active' s'" and sr: "(s, s') \ state_relation" and vui: "valid_untyped_inv_wcap ?ui (Some (cap.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s" diff --git a/proof/refine/ARM_HYP/Arch_R.thy b/proof/refine/ARM_HYP/Arch_R.thy index 342ea2cffb..d0a22a7ab3 100644 --- a/proof/refine/ARM_HYP/Arch_R.thy +++ b/proof/refine/ARM_HYP/Arch_R.thy @@ -127,7 +127,7 @@ lemma set_cap_device_and_range_aligned: lemma performASIDControlInvocation_corres: "asid_ci_map i = i' \ corres dc - (einvs and ct_active and valid_aci i) + (einvs and ct_active and valid_aci i and schact_is_rct) (invs' and ct_active' and valid_aci' i') (perform_asid_control_invocation i) (performASIDControlInvocation i')" @@ -326,29 +326,30 @@ lemma performASIDControlInvocation_corres: apply clarsimp apply (frule empty_descendants_range_in') apply (intro conjI, - simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2 - null_filter_descendants_of'[OF null_filter_simp'] - capAligned_def asid_low_bits_def) - apply (erule descendants_range_caps_no_overlapI') - apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) - apply (simp add:empty_descendants_range_in') - apply (simp add:word_bits_def pageBits_def) - apply (rule is_aligned_weaken) - apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) - apply (simp add:pageBits_def) + simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2 + null_filter_descendants_of'[OF null_filter_simp'] + capAligned_def asid_low_bits_def) + apply (erule descendants_range_caps_no_overlapI') + apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) + apply (simp add:empty_descendants_range_in') + apply (simp add:word_bits_def pageBits_def) + apply (rule is_aligned_weaken) + apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) + apply (simp add:pageBits_def) + apply clarsimp + apply (drule(1) cte_cap_in_untyped_range) + apply (fastforce simp:cte_wp_at_ctes_of) + apply assumption+ + apply fastforce + apply simp apply clarsimp - apply (drule(1) cte_cap_in_untyped_range) - apply (fastforce simp:cte_wp_at_ctes_of) + apply (drule (1) cte_cap_in_untyped_range) + apply (fastforce simp add: cte_wp_at_ctes_of) apply assumption+ + apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) apply fastforce apply simp apply clarsimp - apply (drule (1) cte_cap_in_untyped_range) - apply (fastforce simp add: cte_wp_at_ctes_of) - apply assumption+ - apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) - apply fastforce - apply simp done definition @@ -1379,7 +1380,7 @@ lemma performARMVCPUInvocation_corres: lemma arch_performInvocation_corres: assumes "archinv_relation ai ai'" shows "corres (dc \ (=)) - (einvs and ct_active and valid_arch_inv ai) + (einvs and ct_active and valid_arch_inv ai and schact_is_rct) (invs' and ct_active' and valid_arch_inv' ai' and (\s. vs_valid_duplicates' (ksPSpace s))) (arch_perform_invocation ai) (Arch.performInvocation ai')" proof - diff --git a/proof/refine/ARM_HYP/Detype_R.thy b/proof/refine/ARM_HYP/Detype_R.thy index 680aabb2e3..3e7c738bc2 100644 --- a/proof/refine/ARM_HYP/Detype_R.thy +++ b/proof/refine/ARM_HYP/Detype_R.thy @@ -100,6 +100,9 @@ defs deletionIsSafe_def: (\ko. ksPSpace s p = Some (KOArch ko) \ p \ {ptr .. ptr + 2 ^ bits - 1} \ 7 \ bits)" +defs deletionIsSafe_delete_locale_def: + "deletionIsSafe_delete_locale \ \ptr bits s. \p. ko_wp_at' live' p s \ p \ {ptr .. ptr + 2 ^ bits - 1}" + defs ksASIDMapSafe_def: "ksASIDMapSafe \ \s. \asid hw_asid pd. armKSASIDMap (ksArchState s) asid = Some (hw_asid,pd) \ page_directory_at' pd s" @@ -116,6 +119,7 @@ lemma deleteObjects_def2: "is_aligned ptr bits \ deleteObjects ptr bits = do stateAssert (deletionIsSafe ptr bits) []; + stateAssert (deletionIsSafe_delete_locale ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ {ptr .. ptr + 2 ^ bits - 1})) []; modify (\s. s \ ksPSpace := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} @@ -129,6 +133,7 @@ lemma deleteObjects_def2: apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def deleteGhost_def) apply (rule bind_eqI, rule ext) apply (rule bind_eqI, rule ext) + apply (rule bind_eqI, rule ext) apply (simp add: bind_assoc[symmetric]) apply (rule bind_cong[rotated], rule refl) apply (simp add: bind_assoc modify_modify deleteRange_def gets_modify_def) @@ -149,6 +154,7 @@ lemma deleteObjects_def3: do assert (is_aligned ptr bits); stateAssert (deletionIsSafe ptr bits) []; + stateAssert (deletionIsSafe_delete_locale ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ {ptr .. ptr + 2 ^ bits - 1})) []; modify (\s. s \ ksPSpace := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} @@ -432,6 +438,7 @@ next qed end + locale detype_locale' = detype_locale + constrains s::"det_state" lemma (in detype_locale') deletionIsSafe: @@ -522,187 +529,8 @@ proof - done thus ?thesis using cte by (auto simp: deletionIsSafe_def) qed -context begin interpretation Arch . (*FIXME: arch_split*) -lemma ksASIDMapSafeI: - "\ (s,s') \ state_relation; invs s; pspace_aligned' s' \ pspace_distinct' s' \ - \ ksASIDMapSafe s'" - apply (clarsimp simp: ksASIDMapSafe_def) - apply (subgoal_tac "valid_asid_map s") - prefer 2 - apply fastforce - apply (clarsimp simp: valid_asid_map_def graph_of_def) - apply (subgoal_tac "arm_asid_map (arch_state s) asid = Some (hw_asid, pd)") - prefer 2 - apply (clarsimp simp: state_relation_def arch_state_relation_def) - apply (erule allE)+ - apply (erule (1) impE) - apply clarsimp - apply (drule find_pd_for_asid_eq_helper) - apply fastforce - apply assumption - apply fastforce - apply clarsimp - apply (rule pspace_relation_pd) - apply (fastforce simp: state_relation_def) - apply fastforce - apply assumption - apply assumption - apply simp - done - -(* FIXME: generalizes lemma SubMonadLib.corres_submonad *) -(* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) -(* FIXME: move *) -lemma corres_machine_op: - assumes P: "corres_underlying Id False True r P Q x x'" - shows "corres r (P \ machine_state) (Q \ ksMachineState) - (do_machine_op x) (doMachineOp x')" - apply (rule corres_submonad3 - [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) - apply (simp_all add: state_relation_def swp_def) - done - -lemma ekheap_relation_detype: - "ekheap_relation ekh kh \ - ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" - by (fastforce simp add: ekheap_relation_def split: if_split_asm) - -lemma cap_table_at_gsCNodes_eq: - "(s, s') \ state_relation - \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" - apply (clarsimp simp: state_relation_def ghost_relation_def - obj_at_def is_cap_table) - apply (drule_tac x = ptr in spec)+ - apply (drule_tac x = bits in spec)+ - apply fastforce - done - -lemma cNodeNoPartialOverlap: - "corres dc (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s - \ valid_objs s \ pspace_aligned s) - \ - (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) - (\x. base \ x \ x \ base + 2 ^ magnitude - 1)) [])" - apply (simp add: stateAssert_def assert_def) - apply (rule corres_symb_exec_r[OF _ get_sp]) - apply (rule corres_req[rotated], subst if_P, assumption) - apply simp - apply (clarsimp simp: cNodePartialOverlap_def) - apply (drule(1) cte_wp_valid_cap) - apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq - obj_at_def is_cap_table) - apply (frule(1) pspace_alignedD) - apply simp - apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) - apply (erule is_aligned_get_word_bits[where 'a=32, folded word_bits_def]) - apply (clarsimp simp: is_aligned_no_overflow) - apply (blast intro: order_trans) - apply (simp add: is_aligned_no_overflow power_overflow word_bits_def) - apply wp+ - done - - -declare wrap_ext_det_ext_ext_def[simp] - - -lemma deleteObjects_corres: - "is_aligned base magnitude \ magnitude \ 2 \ - corres dc - (\s. einvs s - \ s \ (cap.UntypedCap d base magnitude idx) - \ (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s - \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) - \ untyped_children_in_mdb s \ if_unsafe_then_cap s - \ valid_mdb s \ valid_global_refs s \ ct_active s) - (\s. s \' (UntypedCap d base magnitude idx) - \ valid_pspace' s) - (delete_objects base magnitude) (deleteObjects base magnitude)" - apply (simp add: deleteObjects_def2) - apply (rule corres_stateAssert_implied[where P'=\, simplified]) - prefer 2 - apply clarsimp - apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and - s=s in detype_locale'.deletionIsSafe, - simp_all add: detype_locale'_def - detype_locale_def p_assoc_help invs_valid_pspace)[1] - apply (simp add:valid_cap_simps) - apply (simp add: bind_assoc[symmetric]) - apply (rule corres_stateAssert_implied2) - defer - apply (erule ksASIDMapSafeI, assumption, assumption) - apply (rule hoare_pre) - apply (rule delete_objects_invs) - apply fastforce - apply (simp add: doMachineOp_def split_def) - apply wp - apply (clarsimp simp: valid_pspace'_def pspace_distinct'_def - pspace_aligned'_def) - apply (rule conjI) - subgoal by fastforce - apply (clarsimp simp add: pspace_distinct'_def ps_clear_def - dom_if_None Diff_Int_distrib) - apply (simp add: delete_objects_def) - apply (rule_tac Q="\_ s. valid_objs s \ valid_list s \ - (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ - descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ - s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ - valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ - zombies_final s \ sym_refs (state_refs_of s) \ sym_refs (state_hyp_refs_of s) \ - untyped_children_in_mdb s \ if_unsafe_then_cap s \ - valid_global_refs s" and - Q'="\_ s. s \' capability.UntypedCap d base magnitude idx \ - valid_pspace' s" in corres_underlying_split) - apply (rule corres_bind_return) - apply (rule corres_guard_imp[where r=dc]) - apply (rule corres_split[OF _ cNodeNoPartialOverlap]) - apply (rule corres_machine_op[OF corres_Id], simp+) - apply (rule no_fail_freeMemory, simp+) - apply (wp hoare_vcg_ex_lift)+ - apply auto[1] - apply (auto elim: is_aligned_weaken) - apply (rule corres_modify) - apply (simp add: valid_pspace'_def) - apply (rule state_relation_null_filterE, assumption, - simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] - apply (simp add: detype_def, rule state.equality; simp add: detype_ext_def) - apply (intro exI, fastforce) - apply (rule ext, clarsimp simp add: null_filter_def) - apply (rule sym, rule ccontr, clarsimp) - apply (drule(4) cte_map_not_null_outside') - apply (fastforce simp add: cte_wp_at_caps_of_state) - apply simp - apply (rule ext, clarsimp simp add: null_filter'_def - map_to_ctes_delete[simplified field_simps]) - apply (rule sym, rule ccontr, clarsimp) - apply (frule(2) pspace_relation_cte_wp_atI - [OF state_relation_pspace_relation]) - apply (elim exE) - apply (frule(4) cte_map_not_null_outside') - apply (rule cte_wp_at_weakenE, erule conjunct1) - apply (case_tac y, clarsimp) - apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def - valid_nullcaps_def) - apply clarsimp - apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, - erule cte_wp_at_weakenE[OF _ TrueI], assumption+) - apply simp - apply (rule detype_pspace_relation[simplified], - simp_all add: state_relation_pspace_relation valid_pspace_def)[1] - apply (simp add: valid_cap'_def capAligned_def) - apply (clarsimp simp: valid_cap_def, assumption) - apply (fastforce simp add: detype_def detype_ext_def intro!: ekheap_relation_detype) - apply (clarsimp simp: state_relation_def ghost_relation_of_heap - detype_def) - apply (drule_tac t="gsUserPages s'" in sym) - apply (drule_tac t="gsCNodes s'" in sym) - apply (auto simp add: ups_of_heap_def cns_of_heap_def ext - split: option.splits kernel_object.splits)[1] - apply (simp add: valid_mdb_def) - apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | - simp add: invs_def valid_state_def valid_pspace_def - descendants_range_def | wp (once) hoare_drop_imps)+ - done +context begin interpretation Arch . (*FIXME: arch_split*) text \Invariant preservation across concrete deletion\ @@ -762,92 +590,93 @@ lemma zobj_refs_capRange: apply (drule is_aligned_no_overflow) apply simp done + end locale delete_locale = - fixes s and base and bits and ptr and idx and d - assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s" - and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s)" - and invs: "invs' s" - and ct_act: "ct_active' s" - and sa_simp: "sch_act_simple s" - and bwb: "bits < word_bits" + fixes s' and base and bits and ptr and idx and d + assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s'" + and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s')" + and invs: "invs' s'" + and ct_act: "ct_active' s'" + and sa_simp: "sch_act_simple s'" and al: "is_aligned base bits" - and safe: "deletionIsSafe base bits s" - -context delete_locale -begin -interpretation Arch . (*FIXME: arch_split*) -lemma valid_objs: "valid_objs' s" - and pa: "pspace_aligned' s" - and pd: "pspace_distinct' s" - and vq: "valid_queues s" - and vq': "valid_queues' s" - and sym_refs: "sym_refs (state_refs_of' s)" - and sym_hyp_refs: "sym_refs (state_hyp_refs_of' s)" - and iflive: "if_live_then_nonz_cap' s" - and ifunsafe: "if_unsafe_then_cap' s" - and dlist: "valid_dlist (ctes_of s)" - and no_0: "no_0 (ctes_of s)" - and chain_0: "mdb_chain_0 (ctes_of s)" - and badges: "valid_badges (ctes_of s)" - and contained: "caps_contained' (ctes_of s)" - and chunked: "mdb_chunked (ctes_of s)" - and umdb: "untyped_mdb' (ctes_of s)" - and uinc: "untyped_inc' (ctes_of s)" - and nullcaps: "valid_nullcaps (ctes_of s)" - and ut_rev: "ut_revocable' (ctes_of s)" - and dist_z: "distinct_zombies (ctes_of s)" - and irq_ctrl: "irq_control (ctes_of s)" - and clinks: "class_links (ctes_of s)" - and rep_r_fb: "reply_masters_rvk_fb (ctes_of s)" - and idle: "valid_idle' s" - and refs: "valid_global_refs' s" - and arch: "valid_arch_state' s" - and virq: "valid_irq_node' (irq_node' s) s" - and virqh: "valid_irq_handlers' s" - and virqs: "valid_irq_states' s" - and no_0_objs: "no_0_obj' s" - and ctnotinQ: "ct_not_inQ s" - and pde_maps: "valid_pde_mappings' s" - and irqs_masked: "irqs_masked' s" - and ctcd: "ct_idle_or_in_cur_domain' s" - and cdm: "ksCurDomain s \ maxDomain" - and vds: "valid_dom_schedule' s" + and safe: "deletionIsSafe base bits s'" + +context delete_locale begin interpretation Arch . (*FIXME: arch_split*) + +lemma valid_objs: "valid_objs' s'" + and pa: "pspace_aligned' s'" + and pd: "pspace_distinct' s'" + and vq: "valid_queues s'" + and vq': "valid_queues' s'" + and sym_refs: "sym_refs (state_refs_of' s')" + and sym_hyp_refs: "sym_refs (state_hyp_refs_of' s')" + and iflive: "if_live_then_nonz_cap' s'" + and ifunsafe: "if_unsafe_then_cap' s'" + and dlist: "valid_dlist (ctes_of s')" + and no_0: "no_0 (ctes_of s')" + and chain_0: "mdb_chain_0 (ctes_of s')" + and badges: "valid_badges (ctes_of s')" + and contained: "caps_contained' (ctes_of s')" + and chunked: "mdb_chunked (ctes_of s')" + and umdb: "untyped_mdb' (ctes_of s')" + and uinc: "untyped_inc' (ctes_of s')" + and nullcaps: "valid_nullcaps (ctes_of s')" + and ut_rev: "ut_revocable' (ctes_of s')" + and dist_z: "distinct_zombies (ctes_of s')" + and irq_ctrl: "irq_control (ctes_of s')" + and clinks: "class_links (ctes_of s')" + and rep_r_fb: "reply_masters_rvk_fb (ctes_of s')" + and idle: "valid_idle' s'" + and refs: "valid_global_refs' s'" + and arch: "valid_arch_state' s'" + and virq: "valid_irq_node' (irq_node' s') s'" + and virqh: "valid_irq_handlers' s'" + and virqs: "valid_irq_states' s'" + and no_0_objs: "no_0_obj' s'" + and ctnotinQ: "ct_not_inQ s'" + and pde_maps: "valid_pde_mappings' s'" + and irqs_masked: "irqs_masked' s'" + and ctcd: "ct_idle_or_in_cur_domain' s'" + and cdm: "ksCurDomain s' \ maxDomain" + and vds: "valid_dom_schedule' s'" using invs - by (auto simp add: invs'_def valid_state'_def valid_pspace'_def - valid_mdb'_def valid_mdb_ctes_def) + by (auto simp: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) abbreviation "base_bits \ {base .. base + (2 ^ bits - 1)}" -abbreviation - "state' \ (s \ ksPSpace := \x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s x \)" +abbreviation pspace' :: pspace where + "pspace' \ \x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s' x" + +abbreviation state' :: kernel_state where + "state' \ (s' \ ksPSpace := pspace' \)" lemma ko_wp_at'[simp]: - "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s \ p \ base_bits)" + "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s' \ p \ base_bits)" by (fastforce simp add: ko_wp_at_delete'[OF pd]) lemma obj_at'[simp]: - "\P p. (obj_at' P p state') = (obj_at' P p s \ p \ base_bits)" + "\P p. (obj_at' P p state') = (obj_at' P p s' \ p \ base_bits)" by (fastforce simp add: obj_at'_real_def) lemma typ_at'[simp]: - "\T p. (typ_at' P p state') = (typ_at' P p s \ p \ base_bits)" + "typ_at' P p state' = (typ_at' P p s' \ p \ base_bits)" by (simp add: typ_at'_def) lemma valid_untyped[simp]: - "s \' UntypedCap d base bits idx" + "s' \' UntypedCap d base bits idx" using cte_wp_at_valid_objs_valid_cap' [OF cap valid_objs] by clarsimp lemma cte_wp_at'[simp]: - "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s \ p \ base_bits)" + "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s' \ p \ base_bits)" by (fastforce simp:cte_wp_at_delete'[where idx = idx,OF valid_untyped pd ]) (* the bits of caps they need for validity argument are within their capRanges *) lemma valid_cap_ctes_pre: - "\c. s \' c \ case c of CNodeCap ref bits g gs + "\c. s' \' c \ case c of CNodeCap ref bits g gs \ \x. ref + (x && mask bits) * 2^cteSizeBits \ capRange c | Zombie ref (ZombieCNode bits) n \ \x. ref + (x && mask bits) * 2^cteSizeBits \ capRange c @@ -871,13 +700,13 @@ lemma valid_cap_ctes_pre: done lemma replycap_argument: - "\p t m r. cte_wp_at' (\cte. cteCap cte = ReplyCap t m r) p s + "\p t m r. cte_wp_at' (\cte. cteCap cte = ReplyCap t m r) p s' \ t \ {base .. base + (2 ^ bits - 1)}" using safe by (fastforce simp add: deletionIsSafe_def cte_wp_at_ctes_of field_simps) lemma valid_cap': - "\p c. \ s \' c; cte_wp_at' (\cte. cteCap cte = c) p s; + "\p c. \ s' \' c; cte_wp_at' (\cte. cteCap cte = c) p s'; capRange c \ {base .. base + (2 ^ bits - 1)} = {} \ \ state' \' c" apply (subgoal_tac "capClass c = PhysicalClass \ capUntypedPtr c \ capRange c") apply (subgoal_tac "capClass c = PhysicalClass \ @@ -919,11 +748,11 @@ lemma valid_cap': done lemma objRefs_notrange: - assumes asms: "ctes_of s p = Some c" "\ isUntypedCap (cteCap c)" + assumes asms: "ctes_of s' p = Some c" "\ isUntypedCap (cteCap c)" shows "capRange (cteCap c) \ base_bits = {}" proof - from cap obtain node - where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" + where ctes_of: "ctes_of s' ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done @@ -944,11 +773,11 @@ proof - qed lemma ctes_of_valid [elim!]: - "ctes_of s p = Some cte \ s \' cteCap cte" + "ctes_of s' p = Some cte \ s' \' cteCap cte" by (case_tac cte, simp add: ctes_of_valid_cap' [OF _ valid_objs]) lemma valid_cap2: - "\ cte_wp_at' (\cte. cteCap cte = c) p s \ \ state' \' c" + "\ cte_wp_at' (\cte. cteCap cte = c) p s' \ \ state' \' c" apply (case_tac "isUntypedCap c") apply (drule cte_wp_at_valid_objs_valid_cap' [OF _ valid_objs]) apply (clarsimp simp: valid_cap'_def isCap_simps valid_untyped'_def) @@ -958,7 +787,7 @@ lemma valid_cap2: done lemma ex_nonz_cap_notRange: - "ex_nonz_cap_to' p s \ p \ base_bits" + "ex_nonz_cap_to' p s' \ p \ base_bits" apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (case_tac "isUntypedCap (cteCap cte)") apply (clarsimp simp: isCap_simps) @@ -970,14 +799,18 @@ lemma ex_nonz_cap_notRange: done lemma live_notRange: - "\ ko_wp_at' P p s; \ko. P ko \ live' ko \ \ p \ base_bits" + "\ ko_wp_at' P p s'; \ko. P ko \ live' ko \ \ p \ base_bits" apply (drule if_live_then_nonz_capE' [OF iflive ko_wp_at'_weakenE]) apply simp apply (erule ex_nonz_cap_notRange) done +lemma deletionIsSafe_delete_locale_holds: + "deletionIsSafe_delete_locale base bits s'" + by (fastforce dest: live_notRange simp: deletionIsSafe_delete_locale_def field_simps) + lemma refs_notRange: - "(x, tp) \ state_refs_of' s y \ y \ base_bits" + "(x, tp) \ state_refs_of' s' y \ y \ base_bits" apply (drule state_refs_of'_elemD) apply (erule live_notRange) apply (rule refs_of_live') @@ -985,7 +818,7 @@ lemma refs_notRange: done lemma hyp_refs_notRange: - "(x, tp) \ state_hyp_refs_of' s y \ y \ base_bits" + "(x, tp) \ state_hyp_refs_of' s' y \ y \ base_bits" apply (drule state_hyp_refs_of'_elemD) apply (erule live_notRange) apply (rule hyp_refs_of_live') @@ -993,8 +826,8 @@ lemma hyp_refs_notRange: done lemma sym_refs_VCPU_hyp_live': - "\ko_wp_at' ((=) (KOArch (KOVCPU v))) p s; sym_refs (state_hyp_refs_of' s); vcpuTCBPtr v = Some t\ - \ ko_wp_at' (\ko. koTypeOf ko = TCBT \ hyp_live' ko) t s" + "\ko_wp_at' ((=) (KOArch (KOVCPU v))) p s'; sym_refs (state_hyp_refs_of' s'); vcpuTCBPtr v = Some t\ + \ ko_wp_at' (\ko. koTypeOf ko = TCBT \ hyp_live' ko) t s'" apply (drule (1) sym_hyp_refs_ko_wp_atD) apply (clarsimp) apply (drule state_hyp_refs_of'_elemD) @@ -1003,8 +836,8 @@ lemma sym_refs_VCPU_hyp_live': done lemma sym_refs_TCB_hyp_live': - "\ko_wp_at' ((=) (KOTCB t)) p s; sym_refs (state_hyp_refs_of' s); atcbVCPUPtr (tcbArch t) = Some v\ - \ ko_wp_at' (\ko. koTypeOf ko = ArchT VCPUT \ hyp_live' ko) v s" + "\ko_wp_at' ((=) (KOTCB t)) p s'; sym_refs (state_hyp_refs_of' s'); atcbVCPUPtr (tcbArch t) = Some v\ + \ ko_wp_at' (\ko. koTypeOf ko = ArchT VCPUT \ hyp_live' ko) v s'" apply (drule (1) sym_hyp_refs_ko_wp_atD) apply (clarsimp) apply (drule state_hyp_refs_of'_elemD) @@ -1012,8 +845,212 @@ lemma sym_refs_TCB_hyp_live': apply (clarsimp simp: hyp_refs_of_rev' hyp_live'_def arch_live'_def) done +end + +context begin interpretation Arch . (*FIXME: arch_split*) + +lemma ksASIDMapSafeI: + "\ (s,s') \ state_relation; invs s; pspace_aligned' s' \ pspace_distinct' s' \ + \ ksASIDMapSafe s'" + apply (clarsimp simp: ksASIDMapSafe_def) + apply (subgoal_tac "valid_asid_map s") + prefer 2 + apply fastforce + apply (clarsimp simp: valid_asid_map_def graph_of_def) + apply (subgoal_tac "arm_asid_map (arch_state s) asid = Some (hw_asid, pd)") + prefer 2 + apply (clarsimp simp: state_relation_def arch_state_relation_def) + apply (erule allE)+ + apply (erule (1) impE) + apply clarsimp + apply (drule find_pd_for_asid_eq_helper) + apply fastforce + apply assumption + apply fastforce + apply clarsimp + apply (rule pspace_relation_pd) + apply (fastforce simp: state_relation_def) + apply fastforce + apply assumption + apply assumption + apply simp + done + +(* FIXME: generalizes lemma SubMonadLib.corres_submonad *) +(* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) +(* FIXME: move *) +lemma corres_machine_op: + assumes P: "corres_underlying Id False True r P Q x x'" + shows "corres r (P \ machine_state) (Q \ ksMachineState) + (do_machine_op x) (doMachineOp x')" + apply (rule corres_submonad3 + [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) + apply (simp_all add: state_relation_def swp_def) + done + +lemma ekheap_relation_detype: + "ekheap_relation ekh kh \ + ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" + by (fastforce simp add: ekheap_relation_def split: if_split_asm) + +lemma cap_table_at_gsCNodes_eq: + "(s, s') \ state_relation + \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" + apply (clarsimp simp: state_relation_def ghost_relation_def + obj_at_def is_cap_table) + apply (drule_tac x = ptr in spec)+ + apply (drule_tac x = bits in spec)+ + apply fastforce + done + +lemma cNodeNoPartialOverlap: + "corres dc (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s + \ valid_objs s \ pspace_aligned s) + \ + (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) + (\x. base \ x \ x \ base + 2 ^ magnitude - 1)) [])" + apply (simp add: stateAssert_def assert_def) + apply (rule corres_symb_exec_r[OF _ get_sp]) + apply (rule corres_req[rotated], subst if_P, assumption) + apply simp + apply (clarsimp simp: cNodePartialOverlap_def) + apply (drule(1) cte_wp_valid_cap) + apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq + obj_at_def is_cap_table) + apply (frule(1) pspace_alignedD) + apply simp + apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) + apply (erule is_aligned_get_word_bits[where 'a=32, folded word_bits_def]) + apply (clarsimp simp: is_aligned_no_overflow) + apply (blast intro: order_trans) + apply (simp add: is_aligned_no_overflow power_overflow word_bits_def) + apply wp+ + done + +declare wrap_ext_det_ext_ext_def[simp] + +crunches doMachineOp + for deletionIsSafe_delete_locale[wp]: "deletionIsSafe_delete_locale base magnitude" + (simp: deletionIsSafe_delete_locale_def) + +lemma deleteObjects_corres: + "is_aligned base magnitude \ magnitude \ 2 \ + corres dc + (\s. einvs s + \ s \ (cap.UntypedCap d base magnitude idx) + \ (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s + \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) + \ untyped_children_in_mdb s \ if_unsafe_then_cap s + \ valid_mdb s \ valid_global_refs s \ ct_active s + \ schact_is_rct s) + (\s'. invs' s' + \ cte_wp_at' (\cte. cteCap cte = UntypedCap d base magnitude idx) ptr s' + \ descendants_range' (UntypedCap d base magnitude idx) ptr (ctes_of s') + \ ct_active' s' + \ s' \' (UntypedCap d base magnitude idx)) + (delete_objects base magnitude) (deleteObjects base magnitude)" + apply (simp add: deleteObjects_def2) + apply (rule corres_stateAssert_implied[where P'=\, simplified]) + prefer 2 + apply clarsimp + apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and + s=s in detype_locale'.deletionIsSafe, + simp_all add: detype_locale'_def + detype_locale_def p_assoc_help invs_valid_pspace)[1] + apply (simp add:valid_cap_simps) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe_delete_locale_holds) + apply (clarsimp simp: delete_locale_def) + apply (intro conjI) + apply (fastforce simp: sch_act_simple_def state_relation_def schact_is_rct_def) + apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and s=s + in detype_locale'.deletionIsSafe, + simp_all add: detype_locale'_def detype_locale_def invs_valid_pspace)[1] + apply (simp add:valid_cap_simps) + apply (simp add: bind_assoc[symmetric]) + apply (rule corres_stateAssert_implied2) + defer + apply (erule ksASIDMapSafeI, assumption, assumption) + apply (rule hoare_pre) + apply (rule delete_objects_invs) + apply fastforce + apply (simp add: doMachineOp_def split_def) + apply wp + apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def pspace_distinct'_def + pspace_aligned'_def) + apply (rule conjI) + subgoal by fastforce + apply (clarsimp simp add: pspace_distinct'_def ps_clear_def + dom_if_None Diff_Int_distrib) + apply (simp add: delete_objects_def) + apply (rule_tac Q="\_ s. valid_objs s \ valid_list s \ + (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ + descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ + s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ + valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ + zombies_final s \ sym_refs (state_refs_of s) \ sym_refs (state_hyp_refs_of s) \ + untyped_children_in_mdb s \ if_unsafe_then_cap s \ + valid_global_refs s" and + Q'="\_ s. s \' capability.UntypedCap d base magnitude idx \ + valid_pspace' s" in corres_underlying_split) + apply (rule corres_bind_return) + apply (rule corres_guard_imp[where r=dc]) + apply (rule corres_split[OF _ cNodeNoPartialOverlap]) + apply (rule corres_machine_op[OF corres_Id], simp+) + apply (rule no_fail_freeMemory, simp+) + apply (wp hoare_vcg_ex_lift)+ + apply auto[1] + apply (auto elim: is_aligned_weaken) + apply (rule corres_modify) + apply (simp add: valid_pspace'_def) + apply (rule state_relation_null_filterE, assumption, + simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] + apply (simp add: detype_def, rule state.equality; simp add: detype_ext_def) + apply (intro exI, fastforce) + apply (rule ext, clarsimp simp add: null_filter_def) + apply (rule sym, rule ccontr, clarsimp) + apply (drule(4) cte_map_not_null_outside') + apply (fastforce simp add: cte_wp_at_caps_of_state) + apply simp + apply (rule ext, clarsimp simp add: null_filter'_def + map_to_ctes_delete[simplified field_simps]) + apply (rule sym, rule ccontr, clarsimp) + apply (frule(2) pspace_relation_cte_wp_atI + [OF state_relation_pspace_relation]) + apply (elim exE) + apply (frule(4) cte_map_not_null_outside') + apply (rule cte_wp_at_weakenE, erule conjunct1) + apply (case_tac y, clarsimp) + apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def + valid_nullcaps_def) + apply clarsimp + apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, + erule cte_wp_at_weakenE[OF _ TrueI], assumption+) + apply simp + apply (rule detype_pspace_relation[simplified], + simp_all add: state_relation_pspace_relation valid_pspace_def)[1] + apply (simp add: valid_cap'_def capAligned_def) + apply (clarsimp simp: valid_cap_def, assumption) + apply (fastforce simp add: detype_def detype_ext_def intro!: ekheap_relation_detype) + apply (clarsimp simp: state_relation_def ghost_relation_of_heap + detype_def) + apply (drule_tac t="gsUserPages s'" in sym) + apply (drule_tac t="gsCNodes s'" in sym) + apply (auto simp add: ups_of_heap_def cns_of_heap_def ext + split: option.splits kernel_object.splits)[1] + apply (simp add: valid_mdb_def) + apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | + simp add: invs_def valid_state_def valid_pspace_def + descendants_range_def | wp (once) hoare_drop_imps)+ + apply fastforce + done + +end + +context delete_locale begin interpretation Arch . (*FIXME: arch_split*) + lemma valid_obj': - "\ valid_obj' obj s; ko_wp_at' ((=) obj) p s \ \ valid_obj' obj state'" + "\ valid_obj' obj s'; ko_wp_at' ((=) obj) p s' \ \ valid_obj' obj state'" apply (case_tac obj, simp_all add: valid_obj'_def) apply (rename_tac endpoint) apply (case_tac endpoint, simp_all add: valid_ep'_def)[1] @@ -1075,17 +1112,16 @@ lemma valid_obj': done lemma st_tcb: - "\P p. \ st_tcb_at' P p s; \ P Inactive; \ P IdleThreadState \ \ - st_tcb_at' P p state'" + "\P p. \ st_tcb_at' P p s'; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" by (fastforce simp: pred_tcb_at'_def obj_at'_real_def projectKOs live'_def hyp_live'_def - dest: live_notRange) + dest: live_notRange) lemma irq_nodes_global: - "\irq :: 10 word. irq_node' s + (ucast irq) * 16 \ global_refs' s" - by (simp add: global_refs'_def mult.commute mult.left_commute) + "\irq :: 10 word. irq_node' s' + (ucast irq) * 16 \ global_refs' s'" + by (simp add: global_refs'_def mult.commute mult.left_commute) lemma global_refs: - "global_refs' s \ base_bits = {}" + "global_refs' s' \ base_bits = {}" using cap apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule valid_global_refsD' [OF _ refs]) @@ -1093,20 +1129,20 @@ lemma global_refs: done lemma global_refs2: - "global_refs' s \ (- base_bits)" + "global_refs' s' \ (- base_bits)" using global_refs by blast lemma irq_nodes_range: - "\irq :: 10 word. irq_node' s + (ucast irq) * 16 \ base_bits" + "\irq :: 10 word. irq_node' s' + (ucast irq) * 16 \ base_bits" using irq_nodes_global global_refs by blast lemma cte_refs_notRange: - assumes asms: "ctes_of s p = Some c" - shows "cte_refs' (cteCap c) (irq_node' s) \ base_bits = {}" + assumes asms: "ctes_of s' p = Some c" + shows "cte_refs' (cteCap c) (irq_node' s') \ base_bits = {}" proof - from cap obtain node - where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" + where ctes_of: "ctes_of s' ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done @@ -1135,7 +1171,7 @@ proof - qed lemma non_null_present: - "cte_wp_at' (\c. cteCap c \ NullCap) p s \ p \ base_bits" + "cte_wp_at' (\c. cteCap c \ NullCap) p s' \ p \ base_bits" apply (drule (1) if_unsafe_then_capD' [OF _ ifunsafe]) apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of dest!: cte_refs_notRange simp del: atLeastAtMost_iff) @@ -1143,7 +1179,7 @@ lemma non_null_present: done lemma cte_cap: - "ex_cte_cap_to' p s \ ex_cte_cap_to' p state'" + "ex_cte_cap_to' p s' \ ex_cte_cap_to' p state'" apply (clarsimp simp: ex_cte_cap_to'_def) apply (frule non_null_present [OF cte_wp_at_weakenE']) apply clarsimp @@ -1151,37 +1187,37 @@ lemma cte_cap: done lemma idle_notRange: - "\cref. \ cte_wp_at' (\c. ksIdleThread s \ capRange (cteCap c)) cref s - \ ksIdleThread s \ base_bits" + "\cref. \ cte_wp_at' (\c. ksIdleThread s' \ capRange (cteCap c)) cref s' + \ ksIdleThread s' \ base_bits" apply (insert cap) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule_tac x=ptr in allE, clarsimp simp: field_simps) done abbreviation - "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s x)" + "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s' x)" lemmas tree_to_ctes = map_to_ctes_delete [OF valid_untyped pd] lemma map_to_ctesE[elim!]: - "\ ctes' x = Some cte; \ ctes_of s x = Some cte; x \ base_bits \ \ P \ \ P" + "\ ctes' x = Some cte; \ ctes_of s' x = Some cte; x \ base_bits \ \ P \ \ P" by (clarsimp simp: tree_to_ctes split: if_split_asm) lemma not_nullMDBNode: - "\ ctes_of s x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" + "\ ctes_of s' x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" using nullcaps apply (cases cte) apply (simp add: valid_nullcaps_def) done -lemma mdb_src: "\ ctes_of s \ x \ y; y \ 0 \ \ x \ base_bits" +lemma mdb_src: "\ ctes_of s' \ x \ y; y \ 0 \ \ x \ base_bits" apply (rule non_null_present) apply (clarsimp simp: next_unfold' cte_wp_at_ctes_of) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def) done -lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ \ y \ base_bits" +lemma mdb_dest: "\ ctes_of s' \ x \ y; y \ 0 \ \ y \ base_bits" apply (case_tac "x = 0") apply (insert no_0, simp add: next_unfold')[1] apply (drule(1) vdlist_nextD0 [OF _ _ dlist]) @@ -1192,7 +1228,7 @@ lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ done lemma trancl_next[elim]: - "\ ctes_of s \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" + "\ ctes_of s' \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" apply (erule rev_mp, erule converse_trancl_induct) apply clarsimp apply (rule r_into_trancl) @@ -1210,14 +1246,14 @@ lemma trancl_next[elim]: done lemma mdb_parent_notrange: - "ctes_of s \ x \ y \ x \ base_bits \ y \ base_bits" + "ctes_of s' \ x \ y \ x \ base_bits \ y \ base_bits" apply (erule subtree.induct) apply (frule(1) mdb_src, drule(1) mdb_dest, simp) apply (drule(1) mdb_dest, simp) done lemma mdb_parent: - "ctes_of s \ x \ y \ ctes' \ x \ y" + "ctes_of s' \ x \ y \ ctes' \ x \ y" apply (erule subtree.induct) apply (frule(1) mdb_src, frule(1) mdb_dest) apply (rule subtree.direct_parent) @@ -1233,7 +1269,7 @@ lemma mdb_parent: done lemma trancl_next_rev: - "ctes' \ x \\<^sup>+ y \ ctes_of s \ x \\<^sup>+ y" + "ctes' \ x \\<^sup>+ y \ ctes_of s' \ x \\<^sup>+ y" apply (erule converse_trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp: next_unfold') @@ -1243,7 +1279,7 @@ lemma trancl_next_rev: done lemma is_chunk[elim!]: - "is_chunk (ctes_of s) cap x y \ is_chunk ctes' cap x y" + "is_chunk (ctes_of s') cap x y \ is_chunk ctes' cap x y" apply (simp add: is_chunk_def) apply (erule allEI) apply (clarsimp dest!: trancl_next_rev) @@ -1341,7 +1377,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def intro!: cte_cap) from idle_notRange refs - have "ksIdleThread s \ ?ran" + have "ksIdleThread s' \ ?ran" apply (simp add: cte_wp_at_ctes_of valid_global_refs'_def valid_refs'_def) apply blast done @@ -1446,11 +1482,11 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def global_refs'_def) apply (intro conjI) apply (simp add: valid_asid_table'_def) - apply (case_tac "armHSCurVCPU (ksArchState s)"; clarsimp simp add: split_def) + apply (case_tac "armHSCurVCPU (ksArchState s')"; clarsimp simp add: split_def) apply (drule live_notRange, clarsimp, case_tac ko; simp add: is_vcpu'_def live'_def) done - show "valid_irq_node' (irq_node' s) ?s" + show "valid_irq_node' (irq_node' s') ?s" using virq irq_nodes_range by (simp add: valid_irq_node'_def mult.commute mult.left_commute ucast_ucast_mask_8) @@ -1480,7 +1516,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def ball_ran_eq) from virqs - show "valid_irq_states' s" . + show "valid_irq_states' s'" . from no_0_objs show "no_0_obj' state'" @@ -1495,19 +1531,19 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def by (simp add: irqs_masked'_def) from sa_simp ct_act - show "sch_act_wf (ksSchedulerAction s) state'" + show "sch_act_wf (ksSchedulerAction s') state'" apply (simp add: sch_act_simple_def) - apply (case_tac "ksSchedulerAction s", simp_all add: ct_in_state'_def) + apply (case_tac "ksSchedulerAction s'", simp_all add: ct_in_state'_def) apply (fastforce dest!: st_tcb elim!: pred_tcb'_weakenE) done from invs - have "pspace_domain_valid s" by (simp add: invs'_def valid_state'_def) + have "pspace_domain_valid s'" by (simp add: invs'_def valid_state'_def) thus "pspace_domain_valid state'" by (simp add: pspace_domain_valid_def) from invs - have "valid_machine_state' s" by (simp add: invs'_def valid_state'_def) + have "valid_machine_state' s'" by (simp add: invs'_def valid_state'_def) thus "valid_machine_state' ?state''" apply (clarsimp simp: valid_machine_state'_def) apply (drule_tac x=p in spec) @@ -1562,12 +1598,11 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def apply (clarsimp dest!: ex_nonz_cap_notRange elim!: ko_wp_at'_weakenE) done - from cdm show "ksCurDomain s \ maxDomain" . + from cdm show "ksCurDomain s' \ maxDomain" . from invs - have urz: "untyped_ranges_zero' s" by (simp add: invs'_def valid_state'_def) - show "untyped_ranges_zero_inv (cteCaps_of state') - (gsUntypedZeroRanges s)" + have urz: "untyped_ranges_zero' s'" by (simp add: invs'_def valid_state'_def) + show "untyped_ranges_zero_inv (cteCaps_of state') (gsUntypedZeroRanges s')" apply (simp add: untyped_zero_ranges_cte_def urz[unfolded untyped_zero_ranges_cte_def, rule_format, symmetric]) apply (clarsimp simp: fun_eq_iff intro!: arg_cong[where f=Ex]) @@ -1580,14 +1615,14 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def qed (clarsimp) lemma (in delete_locale) delete_ko_wp_at': - assumes objs: "ko_wp_at' P p s \ ex_nonz_cap_to' p s" + assumes objs: "ko_wp_at' P p s' \ ex_nonz_cap_to' p s'" shows "ko_wp_at' P p state'" using objs by (clarsimp simp: ko_wp_at'_def ps_clear_def dom_if_None Diff_Int_distrib dest!: ex_nonz_cap_notRange) lemma (in delete_locale) null_filter': - assumes descs: "Q (null_filter' (ctes_of s))" + assumes descs: "Q (null_filter' (ctes_of s'))" shows "Q (null_filter' (ctes_of state'))" using descs ifunsafe apply (clarsimp elim!: rsubst[where P=Q]) @@ -1605,7 +1640,7 @@ lemma (in delete_locale) null_filter': done lemma (in delete_locale) delete_ex_cte_cap_to': - assumes exc: "ex_cte_cap_to' p s" + assumes exc: "ex_cte_cap_to' p s'" shows "ex_cte_cap_to' p state'" using exc by (clarsimp elim!: cte_cap) diff --git a/proof/refine/ARM_HYP/EmptyFail_H.thy b/proof/refine/ARM_HYP/EmptyFail_H.thy index 129f720fd4..937d0c6891 100644 --- a/proof/refine/ARM_HYP/EmptyFail_H.thy +++ b/proof/refine/ARM_HYP/EmptyFail_H.thy @@ -277,7 +277,7 @@ crunch (empty_fail) empty_fail: callKernel theorem call_kernel_serial: "\ (einvs and (\s. event \ Interrupt \ ct_running s) and (ct_running or ct_idle) and - (\s. scheduler_action s = resume_cur_thread) and + schact_is_rct and (\s. 0 < domain_time s \ valid_domain_list s)) s; \s'. (s, s') \ state_relation \ (invs' and (\s. event \ Interrupt \ ct_running' s) and (ct_running' or ct_idle') and diff --git a/proof/refine/ARM_HYP/Refine.thy b/proof/refine/ARM_HYP/Refine.thy index 6a71497b4a..01918758a6 100644 --- a/proof/refine/ARM_HYP/Refine.thy +++ b/proof/refine/ARM_HYP/Refine.thy @@ -598,7 +598,7 @@ lemma kernel_corres': apply (wp handle_event_valid_sched hoare_vcg_if_lift3 | simp | strengthen non_kernel_IRQs_strg[where Q=True, simplified], simp cong: conj_cong)+ - apply (clarsimp simp: active_from_running) + apply (clarsimp simp: active_from_running schact_is_rct_def) apply (clarsimp simp: active_from_running') done @@ -673,7 +673,7 @@ lemma entry_corres: apply ((wp thread_set_invs_trivial thread_set_ct_running thread_set_not_state_valid_sched hoare_weak_lift_imp hoare_vcg_disj_lift ct_in_state_thread_state_lift - | simp add: tcb_cap_cases_def thread_set_no_change_tcb_state)+)[1] + | simp add: tcb_cap_cases_def thread_set_no_change_tcb_state schact_is_rct_def)+)[1] apply (simp add: pred_conj_def cong: conj_cong) apply (wp threadSet_invs_trivial threadSet_ct_running' hoare_weak_lift_imp hoare_vcg_disj_lift diff --git a/proof/refine/ARM_HYP/Syscall_R.thy b/proof/refine/ARM_HYP/Syscall_R.thy index 4d504c9b84..d9cdbe89ee 100644 --- a/proof/refine/ARM_HYP/Syscall_R.thy +++ b/proof/refine/ARM_HYP/Syscall_R.thy @@ -400,7 +400,7 @@ lemma performInvocation_corres: "\ inv_relation i i'; call \ block \ \ corres (dc \ (=)) (einvs and valid_invocation i - and simple_sched_action + and schact_is_rct and ct_active and (\s. (\w w2 b c. i = Invocations_A.InvokeEndpoint w w2 b c) \ st_tcb_at simple (cur_thread s) s)) (invs' and sch_act_simple and valid_invocation' i' and ct_active' and (\s. vs_valid_duplicates' (ksPSpace s))) @@ -450,7 +450,7 @@ lemma performInvocation_corres: apply (clarsimp simp: liftME_def) apply (rule corres_guard_imp) apply (erule invokeTCB_corres) - apply (simp)+ + apply ((clarsimp dest!: schact_is_rct_simple)+)[2] \ \domain cap\ apply (clarsimp simp: invoke_domain_def) apply (rule corres_guard_imp) @@ -465,7 +465,7 @@ lemma performInvocation_corres: apply assumption apply (rule corres_trivial, simp add: returnOk_def) apply wp+ - apply (clarsimp+)[2] + apply ((clarsimp dest!: schact_is_rct_simple)+)[2] apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric]) apply (rule corres_guard_imp, rule performIRQControl_corres, simp+) apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric]) @@ -1222,7 +1222,7 @@ crunch valid_duplicates'[wp]: setThreadState "\s. vs_valid_duplicates' ( lemma handleInvocation_corres: "c \ b \ corres (dc \ dc) - (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + (einvs and schact_is_rct and ct_active) (invs' and (\s. vs_valid_duplicates' (ksPSpace s)) and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_invocation c b) @@ -1272,14 +1272,14 @@ lemma handleInvocation_corres: apply simp apply wp apply simp - apply (rule_tac Q="\rv. einvs and simple_sched_action and valid_invocation rve + apply (rule_tac Q="\rv. einvs and schact_is_rct and valid_invocation rve and (\s. thread = cur_thread s) and st_tcb_at active thread" in hoare_post_imp) apply (clarsimp simp: simple_from_active ct_in_state_def elim!: st_tcb_weakenE) - apply (wp sts_st_tcb_at' set_thread_state_simple_sched_action - set_thread_state_active_valid_sched) + apply (wp sts_st_tcb_at' set_thread_state_schact_is_rct + set_thread_state_active_valid_sched) apply (rule_tac Q="\rv. invs' and valid_invocation' rve' and (\s. thread = ksCurThread s) and st_tcb_at' active' thread @@ -1380,7 +1380,7 @@ lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at'] lemma handleSend_corres: "corres (dc \ dc) - (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + (einvs and schact_is_rct and ct_active) (invs' and (\s. vs_valid_duplicates' (ksPSpace s)) and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_send blocking) (handleSend blocking)" @@ -1804,7 +1804,7 @@ lemma hr_ct_active'[wp]: done lemma handleCall_corres: - "corres (dc \ dc) (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + "corres (dc \ dc) (einvs and schact_is_rct and ct_active) (invs' and (\s. vs_valid_duplicates' (ksPSpace s)) and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') @@ -2012,7 +2012,7 @@ lemma hvmf_invs_etc: lemma handleEvent_corres: "corres (dc \ dc) (einvs and (\s. event \ Interrupt \ ct_running s) and - (\s. scheduler_action s = resume_cur_thread)) + schact_is_rct) (invs' and (\s. event \ Interrupt \ ct_running' s) and (\s. vs_valid_duplicates' (ksPSpace s)) and (\s. ksSchedulerAction s = ResumeCurrentThread)) @@ -2082,8 +2082,6 @@ proof - doMachineOp_getActiveIRQ_IRQ_active' | simp | simp add: imp_conjR | wp (once) hoare_drop_imps)+ - apply force - apply simp apply (clarsimp simp: invs'_def valid_state'_def ct_not_inQ_def valid_queues_def valid_queues_no_bitmap_def) apply (erule allE)+ diff --git a/proof/refine/ARM_HYP/Untyped_R.thy b/proof/refine/ARM_HYP/Untyped_R.thy index 5e327ebb5e..ce364fdf23 100644 --- a/proof/refine/ARM_HYP/Untyped_R.thy +++ b/proof/refine/ARM_HYP/Untyped_R.thy @@ -4222,7 +4222,7 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemma resetUntypedCap_corres: "untypinv_relation ui ui' \ corres (dc \ dc) - (invs and valid_untyped_inv_wcap ui + (invs and schact_is_rct and valid_untyped_inv_wcap ui (Some (cap.UntypedCap dev ptr sz idx)) and ct_active and einvs and (\_. \ptr_base ptr' ty us slots dev'. ui = Invocations_A.Retype slot True @@ -4380,7 +4380,7 @@ lemma resetUntypedCap_corres: apply (frule if_unsafe_then_capD'[OF ctes_of_cte_wpD], clarsimp+) apply (frule(1) descendants_range_ex_cte'[OF empty_descendants_range_in' _ order_refl], (simp add: isCap_simps)+) - apply (intro conjI impI; clarsimp) + apply (auto simp: descendants_range_in'_def valid_untyped'_def) done end @@ -4658,7 +4658,7 @@ defs archOverlap_def: lemma inv_untyped_corres': "\ untypinv_relation ui ui' \ \ corres (dc \ (=)) - (einvs and valid_untyped_inv ui and ct_active) + (einvs and valid_untyped_inv ui and ct_active and schact_is_rct) (invs' and valid_untyped_inv' ui' and ct_active') (invoke_untyped ui) (invokeUntyped ui')" apply (cases ui) @@ -4677,6 +4677,7 @@ lemma inv_untyped_corres': (cte_map cref) reset ptr_base ptr ao' us (map cte_map slots) dev" assume invs: "invs (s :: det_state)" "ct_active s" "valid_list s" "valid_sched s" + "schact_is_rct s" and invs': "invs' s'" "ct_active' s'" and sr: "(s, s') \ state_relation" and vui: "valid_untyped_inv_wcap ?ui (Some (cap.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s" diff --git a/proof/refine/RISCV64/Arch_R.thy b/proof/refine/RISCV64/Arch_R.thy index 0a0d28d318..a209ca58c0 100644 --- a/proof/refine/RISCV64/Arch_R.thy +++ b/proof/refine/RISCV64/Arch_R.thy @@ -132,7 +132,7 @@ lemma set_cap_device_and_range_aligned: lemma performASIDControlInvocation_corres: "asid_ci_map i = i' \ corres dc - (einvs and ct_active and valid_aci i) + (einvs and ct_active and valid_aci i and schact_is_rct) (invs' and ct_active' and valid_aci' i') (perform_asid_control_invocation i) (performASIDControlInvocation i')" @@ -273,6 +273,7 @@ lemma performASIDControlInvocation_corres: subgoal by (fastforce simp:cte_wp_at_caps_of_state descendants_range_def2 empty_descendants_range_in) apply (fold_subgoals (prefix))[2] subgoal premises prems using prems by (clarsimp simp:invs_def valid_state_def)+ + apply (clarsimp simp: schact_is_rct_def) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule detype_locale.non_null_present) apply (fastforce simp:cte_wp_at_caps_of_state) @@ -327,29 +328,30 @@ lemma performASIDControlInvocation_corres: apply clarsimp apply (frule empty_descendants_range_in') apply (intro conjI, - simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2 - null_filter_descendants_of'[OF null_filter_simp'] - capAligned_def asid_low_bits_def) - apply (erule descendants_range_caps_no_overlapI') - apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) - apply (simp add:empty_descendants_range_in') - apply (simp add:word_bits_def bit_simps) - apply (rule is_aligned_weaken) - apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) - apply (simp add:pageBits_def) + simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2 + null_filter_descendants_of'[OF null_filter_simp'] + capAligned_def asid_low_bits_def) + apply (erule descendants_range_caps_no_overlapI') + apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) + apply (simp add:empty_descendants_range_in') + apply (simp add:word_bits_def bit_simps) + apply (rule is_aligned_weaken) + apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) + apply (simp add:pageBits_def) + apply clarsimp + apply (drule(1) cte_cap_in_untyped_range) + apply (fastforce simp:cte_wp_at_ctes_of) + apply assumption+ + apply fastforce + apply simp apply clarsimp - apply (drule(1) cte_cap_in_untyped_range) - apply (fastforce simp:cte_wp_at_ctes_of) + apply (drule (1) cte_cap_in_untyped_range) + apply (fastforce simp add: cte_wp_at_ctes_of) apply assumption+ + apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) apply fastforce apply simp apply clarsimp - apply (drule (1) cte_cap_in_untyped_range) - apply (fastforce simp add: cte_wp_at_ctes_of) - apply assumption+ - apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) - apply fastforce - apply simp done definition @@ -916,7 +918,7 @@ shows lemma arch_performInvocation_corres: "archinv_relation ai ai' \ corres (dc \ (=)) - (einvs and ct_active and valid_arch_inv ai) + (einvs and ct_active and valid_arch_inv ai and schact_is_rct) (invs' and ct_active' and valid_arch_inv' ai') (arch_perform_invocation ai) (Arch.performInvocation ai')" apply (clarsimp simp: arch_perform_invocation_def diff --git a/proof/refine/RISCV64/Detype_R.thy b/proof/refine/RISCV64/Detype_R.thy index 8c9ff5c687..6c6fb9cc16 100644 --- a/proof/refine/RISCV64/Detype_R.thy +++ b/proof/refine/RISCV64/Detype_R.thy @@ -99,6 +99,9 @@ defs deletionIsSafe_def: t \ mask_range ptr bits) \ (\ko. ksPSpace s p = Some (KOArch ko) \ p \ mask_range ptr bits \ 6 \ bits)" +defs deletionIsSafe_delete_locale_def: + "deletionIsSafe_delete_locale \ \ptr bits s. \p. ko_wp_at' live' p s \ p \ mask_range ptr bits" + defs ksASIDMapSafe_def: "ksASIDMapSafe \ \s. True" @@ -115,6 +118,7 @@ lemma deleteObjects_def2: "is_aligned ptr bits \ deleteObjects ptr bits = do stateAssert (deletionIsSafe ptr bits) []; + stateAssert (deletionIsSafe_delete_locale ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ mask_range ptr bits)) []; modify (\s. s \ ksPSpace := \x. if x \ mask_range ptr bits @@ -128,6 +132,7 @@ lemma deleteObjects_def2: apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def deleteGhost_def) apply (rule bind_eqI, rule ext) apply (rule bind_eqI, rule ext) + apply (rule bind_eqI, rule ext) apply (simp add: bind_assoc[symmetric]) apply (rule bind_cong[rotated], rule refl) apply (simp add: bind_assoc modify_modify deleteRange_def gets_modify_def) @@ -148,6 +153,7 @@ lemma deleteObjects_def3: do assert (is_aligned ptr bits); stateAssert (deletionIsSafe ptr bits) []; + stateAssert (deletionIsSafe_delete_locale ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ mask_range ptr bits)) []; modify (\s. s \ ksPSpace := \x. if x \ mask_range ptr bits @@ -418,6 +424,7 @@ next qed end + locale detype_locale' = detype_locale + constrains s::"det_state" lemma (in detype_locale') deletionIsSafe: @@ -514,150 +521,6 @@ qed context begin interpretation Arch . (*FIXME: arch_split*) -(* FIXME: generalizes lemma SubMonadLib.corres_submonad *) -(* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) -(* FIXME: move *) -lemma corres_machine_op: - assumes P: "corres_underlying Id False True r P Q x x'" - shows "corres r (P \ machine_state) (Q \ ksMachineState) - (do_machine_op x) (doMachineOp x')" - apply (rule corres_submonad3 - [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) - apply (simp_all add: state_relation_def swp_def) - done - -lemma ekheap_relation_detype: - "ekheap_relation ekh kh \ - ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" - by (fastforce simp add: ekheap_relation_def split: if_split_asm) - -lemma cap_table_at_gsCNodes_eq: - "(s, s') \ state_relation - \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" - apply (clarsimp simp: state_relation_def ghost_relation_def - obj_at_def is_cap_table) - apply (drule_tac x = ptr in spec)+ - apply (drule_tac x = bits in spec)+ - apply fastforce - done - -lemma cNodeNoPartialOverlap: - "corres dc (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s - \ valid_objs s \ pspace_aligned s) - \ - (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) - (\x. base \ x \ x \ base + mask magnitude)) [])" - apply (simp add: stateAssert_def assert_def) - apply (rule corres_symb_exec_r[OF _ get_sp]) - apply (rule corres_req[rotated], subst if_P, assumption) - apply simp - apply (clarsimp simp: cNodePartialOverlap_def) - apply (drule(1) cte_wp_valid_cap) - apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq - obj_at_def is_cap_table) - apply (frule(1) pspace_alignedD) - apply (simp add: add_mask_fold) - apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) - apply (erule is_aligned_get_word_bits[where 'a=machine_word_len, folded word_bits_def]) - apply (clarsimp simp: is_aligned_no_overflow_mask add_mask_fold) - apply (blast intro: order_trans) - apply (simp add: is_aligned_no_overflow_mask power_overflow word_bits_def) - apply wp+ - done - -declare wrap_ext_det_ext_ext_def[simp] - - -lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s)" - apply (clarsimp simp: state_hyp_refs_of_def sym_refs_def) - by (case_tac "kheap s x"; simp) - -lemma deleteObjects_corres: - "is_aligned base magnitude \ magnitude \ 3 \ - corres dc - (\s. einvs s - \ s \ (cap.UntypedCap d base magnitude idx) - \ (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s - \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) - \ untyped_children_in_mdb s \ if_unsafe_then_cap s - \ valid_mdb s \ valid_global_refs s \ ct_active s) - (\s. s \' (UntypedCap d base magnitude idx) - \ valid_pspace' s) - (delete_objects base magnitude) (deleteObjects base magnitude)" - apply (simp add: deleteObjects_def2) - apply (rule corres_stateAssert_implied[where P'=\, simplified]) - prefer 2 - apply clarsimp - apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and - s=s in detype_locale'.deletionIsSafe, - simp_all add: detype_locale'_def - detype_locale_def p_assoc_help invs_valid_pspace)[1] - apply (simp add:valid_cap_simps) - apply (simp add: bind_assoc[symmetric] ksASIDMapSafe_def) - apply (simp add: delete_objects_def) - apply (rule_tac Q="\_ s. valid_objs s \ valid_list s \ - (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ - descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ - s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ - valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ - zombies_final s \ sym_refs (state_refs_of s) \ - untyped_children_in_mdb s \ if_unsafe_then_cap s \ - valid_global_refs s" and - Q'="\_ s. s \' capability.UntypedCap d base magnitude idx \ - valid_pspace' s" in corres_underlying_split) - apply (rule corres_bind_return) - apply (rule corres_guard_imp[where r=dc]) - apply (rule corres_split[OF _ cNodeNoPartialOverlap]) - apply (rule corres_machine_op[OF corres_Id], simp+) - apply (rule no_fail_freeMemory, simp+) - apply (wp hoare_vcg_ex_lift)+ - apply auto[1] - apply (auto elim: is_aligned_weaken)[1] - apply (rule corres_modify) - apply (simp add: valid_pspace'_def) - apply (rule state_relation_null_filterE, assumption, - simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] - apply (simp add: detype_def, rule state.equality; simp add: detype_ext_def) - apply (intro exI, fastforce) - apply (rule ext, clarsimp simp add: null_filter_def) - apply (rule sym, rule ccontr, clarsimp) - apply (drule(4) cte_map_not_null_outside') - apply (fastforce simp add: cte_wp_at_caps_of_state) - apply simp - apply (rule ext, clarsimp simp add: null_filter'_def - map_to_ctes_delete[simplified field_simps]) - apply (rule sym, rule ccontr, clarsimp) - apply (frule(2) pspace_relation_cte_wp_atI - [OF state_relation_pspace_relation]) - apply (elim exE) - apply (frule(4) cte_map_not_null_outside') - apply (rule cte_wp_at_weakenE, erule conjunct1) - apply (case_tac y, clarsimp) - apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def - valid_nullcaps_def) - apply clarsimp - apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, - erule cte_wp_at_weakenE[OF _ TrueI], assumption+) - apply (simp add: add_mask_fold) - apply (simp add: add_mask_fold) - apply (rule detype_pspace_relation[simplified], - simp_all add: state_relation_pspace_relation valid_pspace_def)[1] - apply (simp add: valid_cap'_def capAligned_def) - apply (clarsimp simp: valid_cap_def, assumption) - apply (fastforce simp add: detype_def detype_ext_def add_mask_fold intro!: ekheap_relation_detype) - apply (clarsimp simp: state_relation_def ghost_relation_of_heap - detype_def) - apply (drule_tac t="gsUserPages s'" in sym) - apply (drule_tac t="gsCNodes s'" in sym) - apply (auto simp add: ups_of_heap_def cns_of_heap_def ext add_mask_fold - split: option.splits kernel_object.splits)[1] - apply (simp add: valid_mdb_def) - apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | - simp add: invs_def valid_state_def valid_pspace_def - descendants_range_def | wp (once) hoare_drop_imps)+ - done - - text \Invariant preservation across concrete deletion\ lemma caps_containedD': @@ -695,90 +558,93 @@ lemma sym_refs_ko_wp_atD: lemma zobj_refs_capRange: "capAligned c \ zobj_refs' c \ capRange c" by (cases c, simp_all add: capRange_def capAligned_def is_aligned_no_overflow) + end + locale delete_locale = - fixes s and base and bits and ptr and idx and d - assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s" - and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s)" - and invs: "invs' s" - and ct_act: "ct_active' s" - and sa_simp: "sch_act_simple s" - and bwb: "bits < word_bits" + fixes s' and base and bits and ptr and idx and d + assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s'" + and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s')" + and invs: "invs' s'" + and ct_act: "ct_active' s'" + and sa_simp: "sch_act_simple s'" and al: "is_aligned base bits" - and safe: "deletionIsSafe base bits s" + and safe: "deletionIsSafe base bits s'" context delete_locale begin interpretation Arch . (*FIXME: arch_split*) -lemma valid_objs: "valid_objs' s" - and pa: "pspace_aligned' s" - and pc: "pspace_canonical' s" - and pkm: "pspace_in_kernel_mappings' s" - and pd: "pspace_distinct' s" - and vq: "valid_queues s" - and vq': "valid_queues' s" - and sym_refs: "sym_refs (state_refs_of' s)" - and iflive: "if_live_then_nonz_cap' s" - and ifunsafe: "if_unsafe_then_cap' s" - and dlist: "valid_dlist (ctes_of s)" - and no_0: "no_0 (ctes_of s)" - and chain_0: "mdb_chain_0 (ctes_of s)" - and badges: "valid_badges (ctes_of s)" - and contained: "caps_contained' (ctes_of s)" - and chunked: "mdb_chunked (ctes_of s)" - and umdb: "untyped_mdb' (ctes_of s)" - and uinc: "untyped_inc' (ctes_of s)" - and nullcaps: "valid_nullcaps (ctes_of s)" - and ut_rev: "ut_revocable' (ctes_of s)" - and dist_z: "distinct_zombies (ctes_of s)" - and irq_ctrl: "irq_control (ctes_of s)" - and clinks: "class_links (ctes_of s)" - and rep_r_fb: "reply_masters_rvk_fb (ctes_of s)" - and idle: "valid_idle' s" - and refs: "valid_global_refs' s" - and arch: "valid_arch_state' s" - and virq: "valid_irq_node' (irq_node' s) s" - and virqh: "valid_irq_handlers' s" - and virqs: "valid_irq_states' s" - and no_0_objs: "no_0_obj' s" - and ctnotinQ: "ct_not_inQ s" - and irqs_masked: "irqs_masked' s" - and ctcd: "ct_idle_or_in_cur_domain' s" - and cdm: "ksCurDomain s \ maxDomain" - and vds: "valid_dom_schedule' s" +lemma valid_objs: "valid_objs' s'" + and pa: "pspace_aligned' s'" + and pc: "pspace_canonical' s'" + and pkm: "pspace_in_kernel_mappings' s'" + and pd: "pspace_distinct' s'" + and vq: "valid_queues s'" + and vq': "valid_queues' s'" + and sym_refs: "sym_refs (state_refs_of' s')" + and iflive: "if_live_then_nonz_cap' s'" + and ifunsafe: "if_unsafe_then_cap' s'" + and dlist: "valid_dlist (ctes_of s')" + and no_0: "no_0 (ctes_of s')" + and chain_0: "mdb_chain_0 (ctes_of s')" + and badges: "valid_badges (ctes_of s')" + and contained: "caps_contained' (ctes_of s')" + and chunked: "mdb_chunked (ctes_of s')" + and umdb: "untyped_mdb' (ctes_of s')" + and uinc: "untyped_inc' (ctes_of s')" + and nullcaps: "valid_nullcaps (ctes_of s')" + and ut_rev: "ut_revocable' (ctes_of s')" + and dist_z: "distinct_zombies (ctes_of s')" + and irq_ctrl: "irq_control (ctes_of s')" + and clinks: "class_links (ctes_of s')" + and rep_r_fb: "reply_masters_rvk_fb (ctes_of s')" + and idle: "valid_idle' s'" + and refs: "valid_global_refs' s'" + and arch: "valid_arch_state' s'" + and virq: "valid_irq_node' (irq_node' s') s'" + and virqh: "valid_irq_handlers' s'" + and virqs: "valid_irq_states' s'" + and no_0_objs: "no_0_obj' s'" + and ctnotinQ: "ct_not_inQ s'" + and irqs_masked: "irqs_masked' s'" + and ctcd: "ct_idle_or_in_cur_domain' s'" + and cdm: "ksCurDomain s' \ maxDomain" + and vds: "valid_dom_schedule' s'" using invs - by (auto simp add: invs'_def valid_state'_def valid_pspace'_def - valid_mdb'_def valid_mdb_ctes_def) + by (auto simp add: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) abbreviation "base_bits \ mask_range base bits" -abbreviation - "state' \ (s \ ksPSpace := \x. if base \ x \ x \ base + mask bits then None else ksPSpace s x \)" +abbreviation pspace' :: pspace where + "pspace' \ \x. if base \ x \ x \ base + mask bits then None else ksPSpace s' x" + +abbreviation state' :: kernel_state where + "state' \ (s' \ ksPSpace := pspace' \)" lemma ko_wp_at'[simp]: - "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s \ p \ base_bits)" + "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s' \ p \ base_bits)" by (fastforce simp add: ko_wp_at_delete'[OF pd]) lemma obj_at'[simp]: - "\P p. (obj_at' P p state') = (obj_at' P p s \ p \ base_bits)" + "\P p. (obj_at' P p state') = (obj_at' P p s' \ p \ base_bits)" by (fastforce simp add: obj_at'_real_def) lemma typ_at'[simp]: - "typ_at' P p state' = (typ_at' P p s \ p \ base_bits)" + "typ_at' P p state' = (typ_at' P p s' \ p \ base_bits)" by (simp add: typ_at'_def) lemma valid_untyped[simp]: - "s \' UntypedCap d base bits idx" + "s' \' UntypedCap d base bits idx" using cte_wp_at_valid_objs_valid_cap' [OF cap valid_objs] by clarsimp lemma cte_wp_at'[simp]: - "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s \ p \ base_bits)" + "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s' \ p \ base_bits)" by (fastforce simp:cte_wp_at_delete'[where idx = idx,OF valid_untyped pd ]) (* the bits of caps they need for validity argument are within their capRanges *) lemma valid_cap_ctes_pre: - "\c. s \' c \ case c of CNodeCap ref bits g gs \ + "\c. s' \' c \ case c of CNodeCap ref bits g gs \ \x. ref + (x && mask bits) * 2^cteSizeBits \ capRange c | Zombie ref (ZombieCNode bits) n \ \x. ref + (x && mask bits) * 2^cteSizeBits \ capRange c @@ -806,13 +672,13 @@ lemma valid_cap_ctes_pre: done lemma replycap_argument: - "\p t m r. cte_wp_at' (\cte. cteCap cte = ReplyCap t m r) p s + "\p t m r. cte_wp_at' (\cte. cteCap cte = ReplyCap t m r) p s' \ t \ mask_range base bits" using safe by (force simp: deletionIsSafe_def cte_wp_at_ctes_of) lemma valid_cap': - "\p c. \ s \' c; cte_wp_at' (\cte. cteCap cte = c) p s; + "\p c. \ s' \' c; cte_wp_at' (\cte. cteCap cte = c) p s'; capRange c \ mask_range base bits = {} \ \ state' \' c" apply (subgoal_tac "capClass c = PhysicalClass \ capUntypedPtr c \ capRange c") apply (subgoal_tac "capClass c = PhysicalClass \ @@ -836,11 +702,11 @@ lemma valid_cap': done lemma objRefs_notrange: - assumes asms: "ctes_of s p = Some c" "\ isUntypedCap (cteCap c)" + assumes asms: "ctes_of s' p = Some c" "\ isUntypedCap (cteCap c)" shows "capRange (cteCap c) \ base_bits = {}" proof - from cap obtain node - where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" + where ctes_of: "ctes_of s' ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done @@ -861,11 +727,11 @@ proof - qed lemma ctes_of_valid [elim!]: - "ctes_of s p = Some cte \ s \' cteCap cte" + "ctes_of s' p = Some cte \ s' \' cteCap cte" by (case_tac cte, simp add: ctes_of_valid_cap' [OF _ valid_objs]) lemma valid_cap2: - "\ cte_wp_at' (\cte. cteCap cte = c) p s \ \ state' \' c" + "\ cte_wp_at' (\cte. cteCap cte = c) p s' \ \ state' \' c" apply (case_tac "isUntypedCap c") apply (drule cte_wp_at_valid_objs_valid_cap' [OF _ valid_objs]) apply (clarsimp simp: valid_cap'_def isCap_simps valid_untyped'_def) @@ -875,7 +741,7 @@ lemma valid_cap2: done lemma ex_nonz_cap_notRange: - "ex_nonz_cap_to' p s \ p \ base_bits" + "ex_nonz_cap_to' p s' \ p \ base_bits" apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (case_tac "isUntypedCap (cteCap cte)") apply (clarsimp simp: isCap_simps) @@ -887,22 +753,192 @@ lemma ex_nonz_cap_notRange: done lemma live_notRange: - "\ ko_wp_at' P p s; \ko. P ko \ live' ko \ \ p \ base_bits" + "\ ko_wp_at' P p s'; \ko. P ko \ live' ko \ \ p \ base_bits" apply (drule if_live_then_nonz_capE' [OF iflive ko_wp_at'_weakenE]) apply simp apply (erule ex_nonz_cap_notRange) done +lemma deletionIsSafe_delete_locale_holds: + "deletionIsSafe_delete_locale base bits s'" + by (fastforce dest: live_notRange simp: deletionIsSafe_delete_locale_def) + lemma refs_notRange: - "(x, tp) \ state_refs_of' s y \ y \ base_bits" + "(x, tp) \ state_refs_of' s' y \ y \ base_bits" apply (drule state_refs_of'_elemD) apply (erule live_notRange) apply (rule refs_of_live') apply clarsimp done +end + +context begin interpretation Arch . (*FIXME: arch_split*) + +(* FIXME: generalizes lemma SubMonadLib.corres_submonad *) +(* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) +(* FIXME: move *) +lemma corres_machine_op: + assumes P: "corres_underlying Id False True r P Q x x'" + shows "corres r (P \ machine_state) (Q \ ksMachineState) + (do_machine_op x) (doMachineOp x')" + apply (rule corres_submonad3 + [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) + apply (simp_all add: state_relation_def swp_def) + done + +lemma ekheap_relation_detype: + "ekheap_relation ekh kh \ + ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" + by (fastforce simp add: ekheap_relation_def split: if_split_asm) + +lemma cap_table_at_gsCNodes_eq: + "(s, s') \ state_relation + \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" + apply (clarsimp simp: state_relation_def ghost_relation_def + obj_at_def is_cap_table) + apply (drule_tac x = ptr in spec)+ + apply (drule_tac x = bits in spec)+ + apply fastforce + done + +lemma cNodeNoPartialOverlap: + "corres dc (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s + \ valid_objs s \ pspace_aligned s) + \ + (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) + (\x. base \ x \ x \ base + mask magnitude)) [])" + apply (simp add: stateAssert_def assert_def) + apply (rule corres_symb_exec_r[OF _ get_sp]) + apply (rule corres_req[rotated], subst if_P, assumption) + apply simp + apply (clarsimp simp: cNodePartialOverlap_def) + apply (drule(1) cte_wp_valid_cap) + apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq + obj_at_def is_cap_table) + apply (frule(1) pspace_alignedD) + apply (simp add: add_mask_fold) + apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) + apply (erule is_aligned_get_word_bits[where 'a=machine_word_len, folded word_bits_def]) + apply (clarsimp simp: is_aligned_no_overflow_mask add_mask_fold) + apply (blast intro: order_trans) + apply (simp add: is_aligned_no_overflow_mask power_overflow word_bits_def) + apply wp+ + done + +declare wrap_ext_det_ext_ext_def[simp] + +lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s')" + apply (clarsimp simp: state_hyp_refs_of_def sym_refs_def) + by (case_tac "kheap s' x"; simp) + +crunches doMachineOp + for deletionIsSafe_delete_locale[wp]: "deletionIsSafe_delete_locale base magnitude" + (simp: deletionIsSafe_delete_locale_def) + +lemma deleteObjects_corres: + "is_aligned base magnitude \ magnitude \ 3 \ + corres dc + (\s. einvs s + \ s \ (cap.UntypedCap d base magnitude idx) + \ (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s + \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) + \ untyped_children_in_mdb s \ if_unsafe_then_cap s + \ valid_mdb s \ valid_global_refs s \ ct_active s + \ schact_is_rct s) + (\s'. invs' s' + \ cte_wp_at' (\cte. cteCap cte = UntypedCap d base magnitude idx) ptr s' + \ descendants_range' (UntypedCap d base magnitude idx) ptr (ctes_of s') + \ ct_active' s' + \ s' \' (UntypedCap d base magnitude idx)) + (delete_objects base magnitude) (deleteObjects base magnitude)" + apply (simp add: deleteObjects_def2) + apply (rule corres_stateAssert_implied[where P'=\, simplified]) + prefer 2 + apply clarsimp + apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and + s=s in detype_locale'.deletionIsSafe, + simp_all add: detype_locale'_def + detype_locale_def p_assoc_help invs_valid_pspace)[1] + apply (simp add:valid_cap_simps) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe_delete_locale_holds) + apply (clarsimp simp: delete_locale_def) + apply (intro conjI) + apply (fastforce simp: sch_act_simple_def state_relation_def schact_is_rct_def) + apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and s=s + in detype_locale'.deletionIsSafe, + simp_all add: detype_locale'_def detype_locale_def invs_valid_pspace)[1] + apply (simp add:valid_cap_simps) + apply (simp add: bind_assoc[symmetric] ksASIDMapSafe_def) + apply (simp add: delete_objects_def) + apply (rule_tac Q="\_ s. valid_objs s \ valid_list s \ + (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ + descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ + s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ + valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ + zombies_final s \ sym_refs (state_refs_of s) \ + untyped_children_in_mdb s \ if_unsafe_then_cap s \ + valid_global_refs s" + and Q'="\_ s. s \' capability.UntypedCap d base magnitude idx \ + valid_pspace' s \ deletionIsSafe_delete_locale base magnitude s" + in corres_underlying_split) + apply (rule corres_bind_return) + apply (rule corres_guard_imp[where r=dc]) + apply (rule corres_split[OF _ cNodeNoPartialOverlap]) + apply (rule corres_machine_op[OF corres_Id], simp+) + apply (rule no_fail_freeMemory, simp+) + apply (wp hoare_vcg_ex_lift)+ + apply auto[1] + apply (auto elim: is_aligned_weaken)[1] + apply (rule corres_modify) + apply (simp add: valid_pspace'_def) + apply (rule state_relation_null_filterE, assumption, + simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] + apply (simp add: detype_def, rule state.equality; simp add: detype_ext_def) + apply (intro exI, fastforce) + apply (rule ext, clarsimp simp add: null_filter_def) + apply (rule sym, rule ccontr, clarsimp) + apply (drule(4) cte_map_not_null_outside') + apply (fastforce simp add: cte_wp_at_caps_of_state) + apply simp + apply (rule ext, clarsimp simp: null_filter'_def map_to_ctes_delete) + apply (rule sym, rule ccontr, clarsimp) + apply (frule(2) pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (elim exE) + apply (frule (4) cte_map_not_null_outside') + apply (rule cte_wp_at_weakenE, erule conjunct1) + apply (case_tac y, clarsimp) + apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) + apply clarsimp + apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, + erule cte_wp_at_weakenE[OF _ TrueI], assumption+) + apply (simp add: add_mask_fold) + apply (simp add: add_mask_fold) + apply (rule detype_pspace_relation[simplified], + simp_all add: state_relation_pspace_relation valid_pspace_def)[1] + apply (simp add: valid_cap'_def capAligned_def) + apply (clarsimp simp: valid_cap_def, assumption) + apply (fastforce simp: detype_def detype_ext_def add_mask_fold intro!: ekheap_relation_detype) + apply (simp add: add_mask_fold) + apply (clarsimp simp: state_relation_def ghost_relation_of_heap detype_def) + apply (drule_tac t="gsUserPages s'" in sym) + apply (drule_tac t="gsCNodes s'" in sym) + apply (auto simp: ups_of_heap_def cns_of_heap_def ext add_mask_fold + split: option.splits kernel_object.splits)[1] + apply (simp add: valid_mdb_def) + apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | + simp add: invs_def valid_state_def valid_pspace_def + descendants_range_def | wp (once) hoare_drop_imps)+ + apply fastforce + done + +end + +context delete_locale begin interpretation Arch . (*FIXME: arch_split*) + lemma valid_obj': - "\ valid_obj' obj s; ko_wp_at' ((=) obj) p s \ \ valid_obj' obj state'" + "\ valid_obj' obj s'; ko_wp_at' ((=) obj) p s' \ \ valid_obj' obj state'" apply (case_tac obj, simp_all add: valid_obj'_def) apply (rename_tac endpoint) apply (case_tac endpoint, simp_all add: valid_ep'_def)[1] @@ -941,16 +977,16 @@ lemma valid_obj': done lemma st_tcb: - "\P p. \ st_tcb_at' P p s; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" + "\P p. \ st_tcb_at' P p s'; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" by (fastforce simp: pred_tcb_at'_def obj_at'_real_def dest: live_notRange) lemma irq_nodes_global: - "\irq :: irq. irq_node' s + (ucast irq << cteSizeBits) \ global_refs' s" - by (simp add: global_refs'_def) + "\irq :: irq. irq_node' s' + (ucast irq << cteSizeBits) \ global_refs' s'" + by (simp add: global_refs'_def) lemma global_refs: - "global_refs' s \ base_bits = {}" + "global_refs' s' \ base_bits = {}" using cap apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule valid_global_refsD' [OF _ refs]) @@ -958,20 +994,20 @@ lemma global_refs: done lemma global_refs2: - "global_refs' s \ (- base_bits)" + "global_refs' s' \ (- base_bits)" using global_refs by blast lemma irq_nodes_range: - "\irq :: irq. irq_node' s + (ucast irq << cteSizeBits) \ base_bits" + "\irq :: irq. irq_node' s' + (ucast irq << cteSizeBits) \ base_bits" using irq_nodes_global global_refs by blast lemma cte_refs_notRange: - assumes asms: "ctes_of s p = Some c" - shows "cte_refs' (cteCap c) (irq_node' s) \ base_bits = {}" + assumes asms: "ctes_of s' p = Some c" + shows "cte_refs' (cteCap c) (irq_node' s') \ base_bits = {}" proof - from cap obtain node - where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" + where ctes_of: "ctes_of s' ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done @@ -1000,7 +1036,7 @@ proof - qed lemma non_null_present: - "cte_wp_at' (\c. cteCap c \ NullCap) p s \ p \ base_bits" + "cte_wp_at' (\c. cteCap c \ NullCap) p s' \ p \ base_bits" apply (drule (1) if_unsafe_then_capD' [OF _ ifunsafe]) apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of dest!: cte_refs_notRange simp del: atLeastAtMost_iff) @@ -1008,7 +1044,7 @@ lemma non_null_present: done lemma cte_cap: - "ex_cte_cap_to' p s \ ex_cte_cap_to' p state'" + "ex_cte_cap_to' p s' \ ex_cte_cap_to' p state'" apply (clarsimp simp: ex_cte_cap_to'_def) apply (frule non_null_present [OF cte_wp_at_weakenE']) apply clarsimp @@ -1016,37 +1052,37 @@ lemma cte_cap: done lemma idle_notRange: - "\cref. \ cte_wp_at' (\c. ksIdleThread s \ capRange (cteCap c)) cref s - \ ksIdleThread s \ base_bits" + "\cref. \ cte_wp_at' (\c. ksIdleThread s' \ capRange (cteCap c)) cref s' + \ ksIdleThread s' \ base_bits" apply (insert cap) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule_tac x=ptr in allE, clarsimp simp: field_simps mask_def) done abbreviation - "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + mask bits then None else ksPSpace s x)" + "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + mask bits then None else ksPSpace s' x)" lemmas tree_to_ctes = map_to_ctes_delete [OF valid_untyped pd] lemma map_to_ctesE[elim!]: - "\ ctes' x = Some cte; \ ctes_of s x = Some cte; x \ base_bits \ \ P \ \ P" + "\ ctes' x = Some cte; \ ctes_of s' x = Some cte; x \ base_bits \ \ P \ \ P" by (clarsimp simp: tree_to_ctes split: if_split_asm) lemma not_nullMDBNode: - "\ ctes_of s x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" + "\ ctes_of s' x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" using nullcaps apply (cases cte) apply (simp add: valid_nullcaps_def) done -lemma mdb_src: "\ ctes_of s \ x \ y; y \ 0 \ \ x \ base_bits" +lemma mdb_src: "\ ctes_of s' \ x \ y; y \ 0 \ \ x \ base_bits" apply (rule non_null_present) apply (clarsimp simp: next_unfold' cte_wp_at_ctes_of) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def) done -lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ \ y \ base_bits" +lemma mdb_dest: "\ ctes_of s' \ x \ y; y \ 0 \ \ y \ base_bits" apply (case_tac "x = 0") apply (insert no_0, simp add: next_unfold')[1] apply (drule(1) vdlist_nextD0 [OF _ _ dlist]) @@ -1057,7 +1093,7 @@ lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ done lemma trancl_next[elim]: - "\ ctes_of s \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" + "\ ctes_of s' \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" apply (erule rev_mp, erule converse_trancl_induct) apply clarsimp apply (rule r_into_trancl) @@ -1075,14 +1111,14 @@ lemma trancl_next[elim]: done lemma mdb_parent_notrange: - "ctes_of s \ x \ y \ x \ base_bits \ y \ base_bits" + "ctes_of s' \ x \ y \ x \ base_bits \ y \ base_bits" apply (erule subtree.induct) apply (frule(1) mdb_src, drule(1) mdb_dest, simp) apply (drule(1) mdb_dest, simp) done lemma mdb_parent: - "ctes_of s \ x \ y \ ctes' \ x \ y" + "ctes_of s' \ x \ y \ ctes' \ x \ y" apply (erule subtree.induct) apply (frule(1) mdb_src, frule(1) mdb_dest) apply (rule subtree.direct_parent) @@ -1098,7 +1134,7 @@ lemma mdb_parent: done lemma trancl_next_rev: - "ctes' \ x \\<^sup>+ y \ ctes_of s \ x \\<^sup>+ y" + "ctes' \ x \\<^sup>+ y \ ctes_of s' \ x \\<^sup>+ y" apply (erule converse_trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp: next_unfold') @@ -1108,7 +1144,7 @@ lemma trancl_next_rev: done lemma is_chunk[elim!]: - "is_chunk (ctes_of s) cap x y \ is_chunk ctes' cap x y" + "is_chunk (ctes_of s') cap x y \ is_chunk ctes' cap x y" apply (simp add: is_chunk_def) apply (erule allEI) apply (clarsimp dest!: trancl_next_rev) @@ -1203,7 +1239,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def intro!: cte_cap) from idle_notRange refs - have "ksIdleThread s \ ?ran" + have "ksIdleThread s' \ ?ran" apply (simp add: cte_wp_at_ctes_of valid_global_refs'_def valid_refs'_def) apply blast done @@ -1315,7 +1351,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def apply simp done - show "valid_irq_node' (irq_node' s) ?s" + show "valid_irq_node' (irq_node' s') ?s" using virq irq_nodes_range by (simp add: valid_irq_node'_def mult.commute mult.left_commute ucast_ucast_mask_8) @@ -1345,7 +1381,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def ball_ran_eq) from virqs - show "valid_irq_states' s" . + show "valid_irq_states' s'" . from no_0_objs show "no_0_obj' state'" @@ -1356,19 +1392,19 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def by (simp add: irqs_masked'_def) from sa_simp ct_act - show "sch_act_wf (ksSchedulerAction s) state'" + show "sch_act_wf (ksSchedulerAction s') state'" apply (simp add: sch_act_simple_def) - apply (case_tac "ksSchedulerAction s", simp_all add: ct_in_state'_def) + apply (case_tac "ksSchedulerAction s'", simp_all add: ct_in_state'_def) apply (fastforce dest!: st_tcb elim!: pred_tcb'_weakenE) done from invs - have "pspace_domain_valid s" by (simp add: invs'_def valid_state'_def) + have "pspace_domain_valid s'" by (simp add: invs'_def valid_state'_def) thus "pspace_domain_valid state'" by (simp add: pspace_domain_valid_def) from invs - have "valid_machine_state' s" by (simp add: invs'_def valid_state'_def) + have "valid_machine_state' s'" by (simp add: invs'_def valid_state'_def) thus "valid_machine_state' ?state''" apply (clarsimp simp: valid_machine_state'_def) apply (drule_tac x=p in spec) @@ -1421,11 +1457,11 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def apply (clarsimp dest!: ex_nonz_cap_notRange elim!: ko_wp_at'_weakenE) done - from cdm show "ksCurDomain s \ maxDomain" . + from cdm show "ksCurDomain s' \ maxDomain" . from invs - have urz: "untyped_ranges_zero' s" by (simp add: invs'_def valid_state'_def) - show "untyped_ranges_zero_inv (cteCaps_of state') (gsUntypedZeroRanges s)" + have urz: "untyped_ranges_zero' s'" by (simp add: invs'_def valid_state'_def) + show "untyped_ranges_zero_inv (cteCaps_of state') (gsUntypedZeroRanges s')" apply (simp add: untyped_zero_ranges_cte_def urz[unfolded untyped_zero_ranges_cte_def, rule_format, symmetric]) apply (clarsimp simp: fun_eq_iff intro!: arg_cong[where f=Ex]) @@ -1438,14 +1474,14 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def qed (clarsimp) lemma (in delete_locale) delete_ko_wp_at': - assumes objs: "ko_wp_at' P p s \ ex_nonz_cap_to' p s" + assumes objs: "ko_wp_at' P p s' \ ex_nonz_cap_to' p s'" shows "ko_wp_at' P p state'" using objs by (clarsimp simp: ko_wp_at'_def ps_clear_def dom_if_None Diff_Int_distrib dest!: ex_nonz_cap_notRange) lemma (in delete_locale) null_filter': - assumes descs: "Q (null_filter' (ctes_of s))" + assumes descs: "Q (null_filter' (ctes_of s'))" shows "Q (null_filter' (ctes_of state'))" using descs ifunsafe apply (clarsimp elim!: rsubst[where P=Q]) @@ -1463,7 +1499,7 @@ lemma (in delete_locale) null_filter': done lemma (in delete_locale) delete_ex_cte_cap_to': - assumes exc: "ex_cte_cap_to' p s" + assumes exc: "ex_cte_cap_to' p s'" shows "ex_cte_cap_to' p state'" using exc by (clarsimp elim!: cte_cap) diff --git a/proof/refine/RISCV64/EmptyFail_H.thy b/proof/refine/RISCV64/EmptyFail_H.thy index 50293f474e..068729f1a3 100644 --- a/proof/refine/RISCV64/EmptyFail_H.thy +++ b/proof/refine/RISCV64/EmptyFail_H.thy @@ -271,7 +271,7 @@ crunch (empty_fail) empty_fail: callKernel theorem call_kernel_serial: "\ (einvs and (\s. event \ Interrupt \ ct_running s) and (ct_running or ct_idle) and - (\s. scheduler_action s = resume_cur_thread) and + schact_is_rct and (\s. 0 < domain_time s \ valid_domain_list s)) s; \s'. (s, s') \ state_relation \ (invs' and (\s. event \ Interrupt \ ct_running' s) and (ct_running' or ct_idle') and diff --git a/proof/refine/RISCV64/Refine.thy b/proof/refine/RISCV64/Refine.thy index 4433ac92b7..55317f076d 100644 --- a/proof/refine/RISCV64/Refine.thy +++ b/proof/refine/RISCV64/Refine.thy @@ -579,7 +579,7 @@ lemma kernel_corres': E="\_. valid_sched and invs and valid_list" in hoare_post_impErr) apply (wp handle_event_valid_sched hoare_vcg_imp_lift' |simp)+ - apply (clarsimp simp: active_from_running) + apply (clarsimp simp: active_from_running schact_is_rct_def) apply (clarsimp simp: active_from_running') done @@ -655,6 +655,7 @@ lemma entry_corres: thread_set_not_state_valid_sched hoare_weak_lift_imp hoare_vcg_disj_lift ct_in_state_thread_state_lift | simp add: tcb_cap_cases_def ct_in_state'_def thread_set_no_change_tcb_state + schact_is_rct_def | (wps, wp threadSet_st_tcb_at2) )+ apply (clarsimp simp: invs_def cur_tcb_def valid_state_def valid_pspace_def) apply (clarsimp simp: ct_in_state'_def) diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index b5688aa2f6..b4efb3eac8 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -400,7 +400,7 @@ lemma performInvocation_corres: "\ inv_relation i i'; call \ block \ \ corres (dc \ (=)) (einvs and valid_invocation i - and simple_sched_action + and schact_is_rct and ct_active and (\s. (\w w2 b c. i = Invocations_A.InvokeEndpoint w w2 b c) \ st_tcb_at simple (cur_thread s) s)) (invs' and sch_act_simple and valid_invocation' i' and ct_active') @@ -449,7 +449,7 @@ lemma performInvocation_corres: apply (clarsimp simp: liftME_def) apply (rule corres_guard_imp) apply (erule invokeTCB_corres) - apply (simp)+ + apply ((clarsimp dest!: schact_is_rct_simple)+)[2] \ \domain cap\ apply (clarsimp simp: invoke_domain_def) apply (rule corres_guard_imp) @@ -464,7 +464,7 @@ lemma performInvocation_corres: apply assumption apply (rule corres_trivial, simp add: returnOk_def) apply wp+ - apply (clarsimp+)[2] + apply ((clarsimp dest!: schact_is_rct_simple)+)[2] apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric]) apply (rule corres_guard_imp, rule performIRQControl_corres, simp+) apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric]) @@ -1182,7 +1182,7 @@ crunches reply_from_kernel lemma handleInvocation_corres: "c \ b \ corres (dc \ dc) - (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + (einvs and schact_is_rct and ct_active) (invs' and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_invocation c b) @@ -1226,14 +1226,14 @@ lemma handleInvocation_corres: apply (wp reply_from_kernel_tcb_at) apply (rule impI, wp+) apply (wpsimp wp: hoare_drop_imps|strengthen invs_distinct invs_psp_aligned)+ - apply (rule_tac Q="\rv. einvs and simple_sched_action and valid_invocation rve + apply (rule_tac Q="\rv. einvs and schact_is_rct and valid_invocation rve and (\s. thread = cur_thread s) and st_tcb_at active thread" in hoare_post_imp) apply (clarsimp simp: simple_from_active ct_in_state_def elim!: st_tcb_weakenE) - apply (wp sts_st_tcb_at' set_thread_state_simple_sched_action - set_thread_state_active_valid_sched) + apply (wp sts_st_tcb_at' set_thread_state_schact_is_rct + set_thread_state_active_valid_sched) apply (rule_tac Q="\rv. invs' and valid_invocation' rve' and (\s. thread = ksCurThread s) and st_tcb_at' active' thread @@ -1338,7 +1338,7 @@ lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at'] lemma handleSend_corres: "corres (dc \ dc) - (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + (einvs and schact_is_rct and ct_active) (invs' and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_send blocking) (handleSend blocking)" @@ -1766,7 +1766,7 @@ lemma hr_ct_active'[wp]: done lemma handleCall_corres: - "corres (dc \ dc) (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + "corres (dc \ dc) (einvs and schact_is_rct and ct_active) (invs' and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') @@ -1945,7 +1945,7 @@ lemma handleHypervisorFault_corres: (* FIXME: move *) lemma handleEvent_corres: "corres (dc \ dc) (einvs and (\s. event \ Interrupt \ ct_running s) and - (\s. scheduler_action s = resume_cur_thread)) + schact_is_rct) (invs' and (\s. event \ Interrupt \ ct_running' s) and (\s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event)" @@ -2015,8 +2015,6 @@ proof - doMachineOp_getActiveIRQ_IRQ_active' | simp | simp add: imp_conjR | wp (once) hoare_drop_imps)+ - apply force - apply simp apply (simp add: invs'_def valid_state'_def) apply (rule_tac corres_underlying_split) apply (rule corres_guard_imp, rule getCurThread_corres, simp+) diff --git a/proof/refine/RISCV64/Untyped_R.thy b/proof/refine/RISCV64/Untyped_R.thy index f65dff97ee..2f1d77bac5 100644 --- a/proof/refine/RISCV64/Untyped_R.thy +++ b/proof/refine/RISCV64/Untyped_R.thy @@ -4203,7 +4203,7 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemma resetUntypedCap_corres: "untypinv_relation ui ui' \ corres (dc \ dc) - (invs and valid_untyped_inv_wcap ui + (invs and schact_is_rct and valid_untyped_inv_wcap ui (Some (cap.UntypedCap dev ptr sz idx)) and ct_active and einvs and (\_. \ptr_base ptr' ty us slots dev'. ui = Invocations_A.Retype slot True @@ -4354,7 +4354,8 @@ lemma resetUntypedCap_corres: apply (frule if_unsafe_then_capD'[OF ctes_of_cte_wpD], clarsimp+) apply (frule(1) descendants_range_ex_cte'[OF empty_descendants_range_in' _ order_refl], (simp add: isCap_simps add_mask_fold)+) - by (intro conjI impI; clarsimp) + apply (auto simp: descendants_range_in'_def valid_untyped'_def) + done end @@ -4634,7 +4635,7 @@ defs archOverlap_def: lemma inv_untyped_corres': "\ untypinv_relation ui ui' \ \ corres (dc \ (=)) - (einvs and valid_untyped_inv ui and ct_active) + (einvs and valid_untyped_inv ui and ct_active and schact_is_rct) (invs' and valid_untyped_inv' ui' and ct_active') (invoke_untyped ui) (invokeUntyped ui')" apply (cases ui) @@ -4653,6 +4654,7 @@ lemma inv_untyped_corres': (cte_map cref) reset ptr_base ptr ao' us (map cte_map slots) dev" assume invs: "invs (s :: det_state)" "ct_active s" "valid_list s" "valid_sched s" + "schact_is_rct s" and invs': "invs' s'" "ct_active' s'" and sr: "(s, s') \ state_relation" and vui: "valid_untyped_inv_wcap ?ui (Some (cap.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s" diff --git a/proof/refine/X64/Arch_R.thy b/proof/refine/X64/Arch_R.thy index 395b554113..2693eef7a4 100644 --- a/proof/refine/X64/Arch_R.thy +++ b/proof/refine/X64/Arch_R.thy @@ -129,7 +129,7 @@ lemma set_cap_device_and_range_aligned: lemma performASIDControlInvocation_corres: "asid_ci_map i = i' \ corres dc - (einvs and ct_active and valid_aci i) + (einvs and ct_active and valid_aci i and schact_is_rct) (invs' and ct_active' and valid_aci' i') (perform_asid_control_invocation i) (performASIDControlInvocation i')" @@ -332,29 +332,30 @@ lemma performASIDControlInvocation_corres: apply clarsimp apply (frule empty_descendants_range_in') apply (intro conjI, - simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2 - null_filter_descendants_of'[OF null_filter_simp'] - capAligned_def asid_low_bits_def) - apply (erule descendants_range_caps_no_overlapI') - apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) - apply (simp add:empty_descendants_range_in') - apply (simp add:word_bits_def bit_simps) - apply (rule is_aligned_weaken) - apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) - apply (simp add:pageBits_def) + simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2 + null_filter_descendants_of'[OF null_filter_simp'] + capAligned_def asid_low_bits_def) + apply (erule descendants_range_caps_no_overlapI') + apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) + apply (simp add:empty_descendants_range_in') + apply (simp add:word_bits_def bit_simps) + apply (rule is_aligned_weaken) + apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) + apply (simp add:pageBits_def) + apply clarsimp + apply (drule(1) cte_cap_in_untyped_range) + apply (fastforce simp:cte_wp_at_ctes_of) + apply assumption+ + apply fastforce + apply simp apply clarsimp - apply (drule(1) cte_cap_in_untyped_range) - apply (fastforce simp:cte_wp_at_ctes_of) + apply (drule (1) cte_cap_in_untyped_range) + apply (fastforce simp add: cte_wp_at_ctes_of) apply assumption+ + apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) apply fastforce apply simp apply clarsimp - apply (drule (1) cte_cap_in_untyped_range) - apply (fastforce simp add: cte_wp_at_ctes_of) - apply assumption+ - apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) - apply fastforce - apply simp done (* FIXME x64: move *) @@ -1400,7 +1401,7 @@ lemma arch_ioport_inv_case_simp: lemma arch_performInvocation_corres: "archinv_relation ai ai' \ corres (dc \ (=)) - (einvs and ct_active and valid_arch_inv ai) + (einvs and ct_active and valid_arch_inv ai and schact_is_rct) (invs' and ct_active' and valid_arch_inv' ai') (arch_perform_invocation ai) (Arch.performInvocation ai')" apply (clarsimp simp: arch_perform_invocation_def diff --git a/proof/refine/X64/Detype_R.thy b/proof/refine/X64/Detype_R.thy index 61d12ae49b..dd12d81d99 100644 --- a/proof/refine/X64/Detype_R.thy +++ b/proof/refine/X64/Detype_R.thy @@ -100,6 +100,9 @@ defs deletionIsSafe_def: (\ko. ksPSpace s p = Some (KOArch ko) \ p \ {ptr .. ptr + 2 ^ bits - 1} \ 6 \ bits)" +defs deletionIsSafe_delete_locale_def: + "deletionIsSafe_delete_locale \ \ptr bits s. \p. ko_wp_at' live' p s \ p \ {ptr .. ptr + 2 ^ bits - 1}" + defs ksASIDMapSafe_def: "ksASIDMapSafe \ \s. True" @@ -115,6 +118,7 @@ lemma deleteObjects_def2: "is_aligned ptr bits \ deleteObjects ptr bits = do stateAssert (deletionIsSafe ptr bits) []; + stateAssert (deletionIsSafe_delete_locale ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ {ptr .. ptr + 2 ^ bits - 1})) []; modify (\s. s \ ksPSpace := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} @@ -128,6 +132,7 @@ lemma deleteObjects_def2: apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def deleteGhost_def) apply (rule bind_eqI, rule ext) apply (rule bind_eqI, rule ext) + apply (rule bind_eqI, rule ext) apply (simp add: bind_assoc[symmetric]) apply (rule bind_cong[rotated], rule refl) apply (simp add: bind_assoc modify_modify deleteRange_def gets_modify_def) @@ -148,6 +153,7 @@ lemma deleteObjects_def3: do assert (is_aligned ptr bits); stateAssert (deletionIsSafe ptr bits) []; + stateAssert (deletionIsSafe_delete_locale ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ {ptr .. ptr + 2 ^ bits - 1})) []; modify (\s. s \ ksPSpace := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} @@ -454,6 +460,7 @@ next qed end + locale detype_locale' = detype_locale + constrains s::"det_state" lemma (in detype_locale') deletionIsSafe: @@ -547,149 +554,6 @@ qed context begin interpretation Arch . (*FIXME: arch_split*) -(* FIXME: generalizes lemma SubMonadLib.corres_submonad *) -(* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) -(* FIXME: move *) -lemma corres_machine_op: - assumes P: "corres_underlying Id False True r P Q x x'" - shows "corres r (P \ machine_state) (Q \ ksMachineState) - (do_machine_op x) (doMachineOp x')" - apply (rule corres_submonad3 - [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) - apply (simp_all add: state_relation_def swp_def) - done - -lemma ekheap_relation_detype: - "ekheap_relation ekh kh \ - ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" - by (fastforce simp add: ekheap_relation_def split: if_split_asm) - -lemma cap_table_at_gsCNodes_eq: - "(s, s') \ state_relation - \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" - apply (clarsimp simp: state_relation_def ghost_relation_def - obj_at_def is_cap_table) - apply (drule_tac x = ptr in spec)+ - apply (drule_tac x = bits in spec)+ - apply fastforce - done - -lemma cNodeNoPartialOverlap: - "corres dc (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s - \ valid_objs s \ pspace_aligned s) - \ - (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) - (\x. base \ x \ x \ base + 2 ^ magnitude - 1)) [])" - apply (simp add: stateAssert_def assert_def) - apply (rule corres_symb_exec_r[OF _ get_sp]) - apply (rule corres_req[rotated], subst if_P, assumption) - apply simp - apply (clarsimp simp: cNodePartialOverlap_def) - apply (drule(1) cte_wp_valid_cap) - apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq - obj_at_def is_cap_table) - apply (frule(1) pspace_alignedD) - apply simp - apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) - apply (erule is_aligned_get_word_bits[where 'a=machine_word_len, folded word_bits_def]) - apply (clarsimp simp: is_aligned_no_overflow) - apply (blast intro: order_trans) - apply (simp add: is_aligned_no_overflow power_overflow word_bits_def) - apply wp+ - done - -declare wrap_ext_det_ext_ext_def[simp] - - -lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s)" - apply (clarsimp simp: state_hyp_refs_of_def sym_refs_def) - by (case_tac "kheap s x"; simp) - -lemma deleteObjects_corres: - "is_aligned base magnitude \ magnitude \ 3 \ - corres dc - (\s. einvs s - \ s \ (cap.UntypedCap d base magnitude idx) - \ (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s - \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) - \ untyped_children_in_mdb s \ if_unsafe_then_cap s - \ valid_mdb s \ valid_global_refs s \ ct_active s) - (\s. s \' (UntypedCap d base magnitude idx) - \ valid_pspace' s) - (delete_objects base magnitude) (deleteObjects base magnitude)" - apply (simp add: deleteObjects_def2) - apply (rule corres_stateAssert_implied[where P'=\, simplified]) - prefer 2 - apply clarsimp - apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and - s=s in detype_locale'.deletionIsSafe, - simp_all add: detype_locale'_def - detype_locale_def p_assoc_help invs_valid_pspace)[1] - apply (simp add:valid_cap_simps) - apply (simp add: bind_assoc[symmetric] ksASIDMapSafe_def) - apply (simp add: delete_objects_def) - apply (rule_tac Q="\_ s. valid_objs s \ valid_list s \ - (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ - descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ - s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ - valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ - zombies_final s \ sym_refs (state_refs_of s) \ - untyped_children_in_mdb s \ if_unsafe_then_cap s \ - valid_global_refs s" and - Q'="\_ s. s \' capability.UntypedCap d base magnitude idx \ - valid_pspace' s" in corres_underlying_split) - apply (rule corres_bind_return) - apply (rule corres_guard_imp[where r=dc]) - apply (rule corres_split[OF _ cNodeNoPartialOverlap]) - apply (rule corres_machine_op[OF corres_Id], simp+) - apply (rule no_fail_freeMemory, simp+) - apply (wp hoare_vcg_ex_lift)+ - apply auto[1] - apply (auto elim: is_aligned_weaken)[1] - apply (rule corres_modify) - apply (simp add: valid_pspace'_def) - apply (rule state_relation_null_filterE, assumption, - simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] - apply (simp add: detype_def, rule state.equality; simp add: detype_ext_def) - apply (intro exI, fastforce) - apply (rule ext, clarsimp simp add: null_filter_def) - apply (rule sym, rule ccontr, clarsimp) - apply (drule(4) cte_map_not_null_outside') - apply (fastforce simp add: cte_wp_at_caps_of_state) - apply simp - apply (rule ext, clarsimp simp add: null_filter'_def - map_to_ctes_delete[simplified field_simps]) - apply (rule sym, rule ccontr, clarsimp) - apply (frule(2) pspace_relation_cte_wp_atI - [OF state_relation_pspace_relation]) - apply (elim exE) - apply (frule(4) cte_map_not_null_outside') - apply (rule cte_wp_at_weakenE, erule conjunct1) - apply (case_tac y, clarsimp) - apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def - valid_nullcaps_def) - apply clarsimp - apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, - erule cte_wp_at_weakenE[OF _ TrueI], assumption+) - apply simp - apply (rule detype_pspace_relation[simplified], - simp_all add: state_relation_pspace_relation valid_pspace_def)[1] - apply (simp add: valid_cap'_def capAligned_def) - apply (clarsimp simp: valid_cap_def, assumption) - apply (fastforce simp add: detype_def detype_ext_def intro!: ekheap_relation_detype) - apply (clarsimp simp: state_relation_def ghost_relation_of_heap - detype_def) - apply (drule_tac t="gsUserPages s'" in sym) - apply (drule_tac t="gsCNodes s'" in sym) - apply (auto simp add: ups_of_heap_def cns_of_heap_def ext - split: option.splits kernel_object.splits)[1] - apply (simp add: valid_mdb_def) - apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | - simp add: invs_def valid_state_def valid_pspace_def - descendants_range_def | wp (once) hoare_drop_imps)+ - done - - text \Invariant preservation across concrete deletion\ lemma caps_containedD': @@ -727,92 +591,95 @@ lemma sym_refs_ko_wp_atD: lemma zobj_refs_capRange: "capAligned c \ zobj_refs' c \ capRange c" by (cases c, simp_all add: capRange_def capAligned_def is_aligned_no_overflow) + end + locale delete_locale = - fixes s and base and bits and ptr and idx and d - assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s" - and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s)" - and invs: "invs' s" - and ct_act: "ct_active' s" - and sa_simp: "sch_act_simple s" - and bwb: "bits < word_bits" + fixes s' and base and bits and ptr and idx and d + assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s'" + and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s')" + and invs: "invs' s'" + and ct_act: "ct_active' s'" + and sa_simp: "sch_act_simple s'" and al: "is_aligned base bits" - and safe: "deletionIsSafe base bits s" + and safe: "deletionIsSafe base bits s'" context delete_locale begin interpretation Arch . (*FIXME: arch_split*) -lemma valid_objs: "valid_objs' s" - and pa: "pspace_aligned' s" - and pc: "pspace_canonical' s" - and pkm: "pspace_in_kernel_mappings' s" - and pd: "pspace_distinct' s" - and vq: "valid_queues s" - and vq': "valid_queues' s" - and sym_refs: "sym_refs (state_refs_of' s)" - and iflive: "if_live_then_nonz_cap' s" - and ifunsafe: "if_unsafe_then_cap' s" - and dlist: "valid_dlist (ctes_of s)" - and no_0: "no_0 (ctes_of s)" - and chain_0: "mdb_chain_0 (ctes_of s)" - and badges: "valid_badges (ctes_of s)" - and contained: "caps_contained' (ctes_of s)" - and chunked: "mdb_chunked (ctes_of s)" - and umdb: "untyped_mdb' (ctes_of s)" - and uinc: "untyped_inc' (ctes_of s)" - and nullcaps: "valid_nullcaps (ctes_of s)" - and ut_rev: "ut_revocable' (ctes_of s)" - and dist_z: "distinct_zombies (ctes_of s)" - and irq_ctrl: "irq_control (ctes_of s)" - and ioport_ctrl: "ioport_control (ctes_of s)" - and clinks: "class_links (ctes_of s)" - and rep_r_fb: "reply_masters_rvk_fb (ctes_of s)" - and idle: "valid_idle' s" - and refs: "valid_global_refs' s" - and arch: "valid_arch_state' s" - and virq: "valid_irq_node' (irq_node' s) s" - and virqh: "valid_irq_handlers' s" - and vioports: "valid_ioports' s" - and virqs: "valid_irq_states' s" - and no_0_objs: "no_0_obj' s" - and ctnotinQ: "ct_not_inQ s" - and irqs_masked: "irqs_masked' s" - and ctcd: "ct_idle_or_in_cur_domain' s" - and cdm: "ksCurDomain s \ maxDomain" - and vds: "valid_dom_schedule' s" +lemma valid_objs: "valid_objs' s'" + and pa: "pspace_aligned' s'" + and pc: "pspace_canonical' s'" + and pkm: "pspace_in_kernel_mappings' s'" + and pd: "pspace_distinct' s'" + and vq: "valid_queues s'" + and vq': "valid_queues' s'" + and sym_refs: "sym_refs (state_refs_of' s')" + and iflive: "if_live_then_nonz_cap' s'" + and ifunsafe: "if_unsafe_then_cap' s'" + and dlist: "valid_dlist (ctes_of s')" + and no_0: "no_0 (ctes_of s')" + and chain_0: "mdb_chain_0 (ctes_of s')" + and badges: "valid_badges (ctes_of s')" + and contained: "caps_contained' (ctes_of s')" + and chunked: "mdb_chunked (ctes_of s')" + and umdb: "untyped_mdb' (ctes_of s')" + and uinc: "untyped_inc' (ctes_of s')" + and nullcaps: "valid_nullcaps (ctes_of s')" + and ut_rev: "ut_revocable' (ctes_of s')" + and dist_z: "distinct_zombies (ctes_of s')" + and irq_ctrl: "irq_control (ctes_of s')" + and ioport_ctrl: "ioport_control (ctes_of s')" + and clinks: "class_links (ctes_of s')" + and rep_r_fb: "reply_masters_rvk_fb (ctes_of s')" + and idle: "valid_idle' s'" + and refs: "valid_global_refs' s'" + and arch: "valid_arch_state' s'" + and virq: "valid_irq_node' (irq_node' s') s'" + and virqh: "valid_irq_handlers' s'" + and vioports: "valid_ioports' s'" + and virqs: "valid_irq_states' s'" + and no_0_objs: "no_0_obj' s'" + and ctnotinQ: "ct_not_inQ s'" + and irqs_masked: "irqs_masked' s'" + and ctcd: "ct_idle_or_in_cur_domain' s'" + and cdm: "ksCurDomain s' \ maxDomain" + and vds: "valid_dom_schedule' s'" using invs - by (auto simp add: invs'_def valid_state'_def valid_pspace'_def - valid_mdb'_def valid_mdb_ctes_def) + by (auto simp: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) abbreviation "base_bits \ {base .. base + (2 ^ bits - 1)}" -abbreviation - "state' \ (s \ ksPSpace := \x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s x \)" +abbreviation pspace' :: pspace where + "pspace' \ \x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s' x" + +abbreviation state' :: kernel_state where + "state' \ (s' \ ksPSpace := pspace' \)" lemma ko_wp_at'[simp]: - "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s \ p \ base_bits)" + "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s' \ p \ base_bits)" by (fastforce simp add: ko_wp_at_delete'[OF pd]) lemma obj_at'[simp]: - "\P p. (obj_at' P p state') = (obj_at' P p s \ p \ base_bits)" + "\P p. (obj_at' P p state') = (obj_at' P p s' \ p \ base_bits)" by (fastforce simp add: obj_at'_real_def) lemma typ_at'[simp]: - "\T p. (typ_at' P p state') = (typ_at' P p s \ p \ base_bits)" + "typ_at' P p state' = (typ_at' P p s' \ p \ base_bits)" by (simp add: typ_at'_def) lemma valid_untyped[simp]: - "s \' UntypedCap d base bits idx" + "s' \' UntypedCap d base bits idx" using cte_wp_at_valid_objs_valid_cap' [OF cap valid_objs] by clarsimp lemma cte_wp_at'[simp]: - "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s \ p \ base_bits)" + "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s' \ p \ base_bits)" by (fastforce simp:cte_wp_at_delete'[where idx = idx,OF valid_untyped pd ]) (* the bits of caps they need for validity argument are within their capRanges *) lemma valid_cap_ctes_pre: - "\c. s \' c \ case c of CNodeCap ref bits g gs + "\c. s' \' c \ case c of CNodeCap ref bits g gs \ \x. ref + (x && mask bits) * 2^cteSizeBits \ capRange c | Zombie ref (ZombieCNode bits) n \ \x. ref + (x && mask bits) * 2^cteSizeBits \ capRange c @@ -850,13 +717,13 @@ lemma valid_cap_ctes_pre: done lemma replycap_argument: - "\p t m r. cte_wp_at' (\cte. cteCap cte = ReplyCap t m r) p s + "\p t m r. cte_wp_at' (\cte. cteCap cte = ReplyCap t m r) p s' \ t \ {base .. base + (2 ^ bits - 1)}" using safe by (fastforce simp add: deletionIsSafe_def cte_wp_at_ctes_of field_simps) lemma valid_cap': - "\p c. \ s \' c; cte_wp_at' (\cte. cteCap cte = c) p s; + "\p c. \ s' \' c; cte_wp_at' (\cte. cteCap cte = c) p s'; capRange c \ {base .. base + (2 ^ bits - 1)} = {} \ \ state' \' c" apply (subgoal_tac "capClass c = PhysicalClass \ capUntypedPtr c \ capRange c") apply (subgoal_tac "capClass c = PhysicalClass \ @@ -903,11 +770,11 @@ lemma valid_cap': done lemma objRefs_notrange: - assumes asms: "ctes_of s p = Some c" "\ isUntypedCap (cteCap c)" + assumes asms: "ctes_of s' p = Some c" "\ isUntypedCap (cteCap c)" shows "capRange (cteCap c) \ base_bits = {}" proof - from cap obtain node - where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" + where ctes_of: "ctes_of s' ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done @@ -928,11 +795,11 @@ proof - qed lemma ctes_of_valid [elim!]: - "ctes_of s p = Some cte \ s \' cteCap cte" + "ctes_of s' p = Some cte \ s' \' cteCap cte" by (case_tac cte, simp add: ctes_of_valid_cap' [OF _ valid_objs]) lemma valid_cap2: - "\ cte_wp_at' (\cte. cteCap cte = c) p s \ \ state' \' c" + "\ cte_wp_at' (\cte. cteCap cte = c) p s' \ \ state' \' c" apply (case_tac "isUntypedCap c") apply (drule cte_wp_at_valid_objs_valid_cap' [OF _ valid_objs]) apply (clarsimp simp: valid_cap'_def isCap_simps valid_untyped'_def) @@ -942,7 +809,7 @@ lemma valid_cap2: done lemma ex_nonz_cap_notRange: - "ex_nonz_cap_to' p s \ p \ base_bits" + "ex_nonz_cap_to' p s' \ p \ base_bits" apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (case_tac "isUntypedCap (cteCap cte)") apply (clarsimp simp: isCap_simps) @@ -954,22 +821,193 @@ lemma ex_nonz_cap_notRange: done lemma live_notRange: - "\ ko_wp_at' P p s; \ko. P ko \ live' ko \ \ p \ base_bits" + "\ ko_wp_at' P p s'; \ko. P ko \ live' ko \ \ p \ base_bits" apply (drule if_live_then_nonz_capE' [OF iflive ko_wp_at'_weakenE]) apply simp apply (erule ex_nonz_cap_notRange) done +lemma deletionIsSafe_delete_locale_holds: + "deletionIsSafe_delete_locale base bits s'" + by (fastforce dest: live_notRange simp: deletionIsSafe_delete_locale_def field_simps) + lemma refs_notRange: - "(x, tp) \ state_refs_of' s y \ y \ base_bits" + "(x, tp) \ state_refs_of' s' y \ y \ base_bits" apply (drule state_refs_of'_elemD) apply (erule live_notRange) apply (rule refs_of_live') apply clarsimp done +end + +context begin interpretation Arch . (*FIXME: arch_split*) + +(* FIXME: generalizes lemma SubMonadLib.corres_submonad *) +(* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) +(* FIXME: move *) +lemma corres_machine_op: + assumes P: "corres_underlying Id False True r P Q x x'" + shows "corres r (P \ machine_state) (Q \ ksMachineState) + (do_machine_op x) (doMachineOp x')" + apply (rule corres_submonad3 + [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) + apply (simp_all add: state_relation_def swp_def) + done + +lemma ekheap_relation_detype: + "ekheap_relation ekh kh \ + ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" + by (fastforce simp add: ekheap_relation_def split: if_split_asm) + +lemma cap_table_at_gsCNodes_eq: + "(s, s') \ state_relation + \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" + apply (clarsimp simp: state_relation_def ghost_relation_def + obj_at_def is_cap_table) + apply (drule_tac x = ptr in spec)+ + apply (drule_tac x = bits in spec)+ + apply fastforce + done + +lemma cNodeNoPartialOverlap: + "corres dc (\s. \cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s + \ valid_objs s \ pspace_aligned s) + \ + (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) + (\x. base \ x \ x \ base + 2 ^ magnitude - 1)) [])" + apply (simp add: stateAssert_def assert_def) + apply (rule corres_symb_exec_r[OF _ get_sp]) + apply (rule corres_req[rotated], subst if_P, assumption) + apply simp + apply (clarsimp simp: cNodePartialOverlap_def) + apply (drule(1) cte_wp_valid_cap) + apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq + obj_at_def is_cap_table) + apply (frule(1) pspace_alignedD) + apply simp + apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) + apply (erule is_aligned_get_word_bits[where 'a=machine_word_len, folded word_bits_def]) + apply (clarsimp simp: is_aligned_no_overflow) + apply (blast intro: order_trans) + apply (simp add: is_aligned_no_overflow power_overflow word_bits_def) + apply wp+ + done + +declare wrap_ext_det_ext_ext_def[simp] + +lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s)" + apply (clarsimp simp: state_hyp_refs_of_def sym_refs_def) + by (case_tac "kheap s x"; simp) + +crunches doMachineOp + for deletionIsSafe_delete_locale[wp]: "deletionIsSafe_delete_locale base magnitude" + (simp: deletionIsSafe_delete_locale_def) + +lemma deleteObjects_corres: + "is_aligned base magnitude \ magnitude \ 3 \ + corres dc + (\s. einvs s + \ s \ (cap.UntypedCap d base magnitude idx) + \ (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s + \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) + \ untyped_children_in_mdb s \ if_unsafe_then_cap s + \ valid_mdb s \ valid_global_refs s \ ct_active s + \ schact_is_rct s) + (\s'. invs' s' + \ cte_wp_at' (\cte. cteCap cte = UntypedCap d base magnitude idx) ptr s' + \ descendants_range' (UntypedCap d base magnitude idx) ptr (ctes_of s') + \ ct_active' s' + \ s' \' (UntypedCap d base magnitude idx)) + (delete_objects base magnitude) (deleteObjects base magnitude)" + apply (simp add: deleteObjects_def2) + apply (rule corres_stateAssert_implied[where P'=\, simplified]) + prefer 2 + apply clarsimp + apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and + s=s in detype_locale'.deletionIsSafe, + simp_all add: detype_locale'_def + detype_locale_def p_assoc_help invs_valid_pspace)[1] + apply (simp add:valid_cap_simps) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe_delete_locale_holds) + apply (clarsimp simp: delete_locale_def) + apply (intro conjI) + apply (fastforce simp: sch_act_simple_def state_relation_def schact_is_rct_def) + apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and s=s + in detype_locale'.deletionIsSafe, + simp_all add: detype_locale'_def detype_locale_def invs_valid_pspace)[1] + apply (simp add:valid_cap_simps) + apply (simp add: bind_assoc[symmetric] ksASIDMapSafe_def) + apply (simp add: delete_objects_def) + apply (rule_tac Q="\_ s. valid_objs s \ valid_list s \ + (\cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \ + descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ + s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ + valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ + zombies_final s \ sym_refs (state_refs_of s) \ + untyped_children_in_mdb s \ if_unsafe_then_cap s \ + valid_global_refs s" and + Q'="\_ s. s \' capability.UntypedCap d base magnitude idx \ + valid_pspace' s" in corres_underlying_split) + apply (rule corres_bind_return) + apply (rule corres_guard_imp[where r=dc]) + apply (rule corres_split[OF _ cNodeNoPartialOverlap]) + apply (rule corres_machine_op[OF corres_Id], simp+) + apply (rule no_fail_freeMemory, simp+) + apply (wp hoare_vcg_ex_lift)+ + apply auto[1] + apply (auto elim: is_aligned_weaken)[1] + apply (rule corres_modify) + apply (simp add: valid_pspace'_def) + apply (rule state_relation_null_filterE, assumption, + simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] + apply (simp add: detype_def, rule state.equality; simp add: detype_ext_def) + apply (intro exI, fastforce) + apply (rule ext, clarsimp simp add: null_filter_def) + apply (rule sym, rule ccontr, clarsimp) + apply (drule(4) cte_map_not_null_outside') + apply (fastforce simp add: cte_wp_at_caps_of_state) + apply simp + apply (rule ext, clarsimp simp add: null_filter'_def + map_to_ctes_delete[simplified field_simps]) + apply (rule sym, rule ccontr, clarsimp) + apply (frule(2) pspace_relation_cte_wp_atI + [OF state_relation_pspace_relation]) + apply (elim exE) + apply (frule(4) cte_map_not_null_outside') + apply (rule cte_wp_at_weakenE, erule conjunct1) + apply (case_tac y, clarsimp) + apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def + valid_nullcaps_def) + apply clarsimp + apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, + erule cte_wp_at_weakenE[OF _ TrueI], assumption+) + apply simp + apply (rule detype_pspace_relation[simplified], + simp_all add: state_relation_pspace_relation valid_pspace_def)[1] + apply (simp add: valid_cap'_def capAligned_def) + apply (clarsimp simp: valid_cap_def, assumption) + apply (fastforce simp add: detype_def detype_ext_def intro!: ekheap_relation_detype) + apply (clarsimp simp: state_relation_def ghost_relation_of_heap + detype_def) + apply (drule_tac t="gsUserPages s'" in sym) + apply (drule_tac t="gsCNodes s'" in sym) + apply (auto simp add: ups_of_heap_def cns_of_heap_def ext + split: option.splits kernel_object.splits)[1] + apply (simp add: valid_mdb_def) + apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | + simp add: invs_def valid_state_def valid_pspace_def + descendants_range_def | wp (once) hoare_drop_imps)+ + apply fastforce + done + +end + +context delete_locale begin interpretation Arch . (*FIXME: arch_split*) + lemma valid_obj': - "\ valid_obj' obj s; ko_wp_at' ((=) obj) p s \ \ valid_obj' obj state'" + "\ valid_obj' obj s'; ko_wp_at' ((=) obj) p s' \ \ valid_obj' obj state'" apply (case_tac obj, simp_all add: valid_obj'_def) apply (rename_tac endpoint) apply (case_tac endpoint, simp_all add: valid_ep'_def)[1] @@ -1020,17 +1058,15 @@ lemma valid_obj': done lemma st_tcb: - "\P p. \ st_tcb_at' P p s; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" - by (fastforce simp: pred_tcb_at'_def obj_at'_real_def - projectKOs - dest: live_notRange) + "\P p. \ st_tcb_at' P p s'; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" + by (fastforce simp: pred_tcb_at'_def obj_at'_real_def projectKOs dest: live_notRange) lemma irq_nodes_global: "\irq :: 8 word. irq_node' s + (ucast irq) * 32 \ global_refs' s" (*2^cte_level_bits *) by (simp add: global_refs'_def mult.commute mult.left_commute) lemma global_refs: - "global_refs' s \ base_bits = {}" + "global_refs' s' \ base_bits = {}" using cap apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule valid_global_refsD' [OF _ refs]) @@ -1038,20 +1074,20 @@ lemma global_refs: done lemma global_refs2: - "global_refs' s \ (- base_bits)" + "global_refs' s' \ (- base_bits)" using global_refs by blast lemma irq_nodes_range: - "\irq :: 8 word. irq_node' s + (ucast irq) * 32 \ base_bits" + "\irq :: 8 word. irq_node' s' + (ucast irq) * 32 \ base_bits" using irq_nodes_global global_refs by blast lemma cte_refs_notRange: - assumes asms: "ctes_of s p = Some c" - shows "cte_refs' (cteCap c) (irq_node' s) \ base_bits = {}" + assumes asms: "ctes_of s' p = Some c" + shows "cte_refs' (cteCap c) (irq_node' s') \ base_bits = {}" proof - from cap obtain node - where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" + where ctes_of: "ctes_of s' ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done @@ -1080,7 +1116,7 @@ proof - qed lemma non_null_present: - "cte_wp_at' (\c. cteCap c \ NullCap) p s \ p \ base_bits" + "cte_wp_at' (\c. cteCap c \ NullCap) p s' \ p \ base_bits" apply (drule (1) if_unsafe_then_capD' [OF _ ifunsafe]) apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of dest!: cte_refs_notRange simp del: atLeastAtMost_iff) @@ -1088,7 +1124,7 @@ lemma non_null_present: done lemma cte_cap: - "ex_cte_cap_to' p s \ ex_cte_cap_to' p state'" + "ex_cte_cap_to' p s' \ ex_cte_cap_to' p state'" apply (clarsimp simp: ex_cte_cap_to'_def) apply (frule non_null_present [OF cte_wp_at_weakenE']) apply clarsimp @@ -1096,37 +1132,37 @@ lemma cte_cap: done lemma idle_notRange: - "\cref. \ cte_wp_at' (\c. ksIdleThread s \ capRange (cteCap c)) cref s - \ ksIdleThread s \ base_bits" + "\cref. \ cte_wp_at' (\c. ksIdleThread s' \ capRange (cteCap c)) cref s' + \ ksIdleThread s' \ base_bits" apply (insert cap) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule_tac x=ptr in allE, clarsimp simp: field_simps) done abbreviation - "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s x)" + "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s' x)" lemmas tree_to_ctes = map_to_ctes_delete [OF valid_untyped pd] lemma map_to_ctesE[elim!]: - "\ ctes' x = Some cte; \ ctes_of s x = Some cte; x \ base_bits \ \ P \ \ P" + "\ ctes' x = Some cte; \ ctes_of s' x = Some cte; x \ base_bits \ \ P \ \ P" by (clarsimp simp: tree_to_ctes split: if_split_asm) lemma not_nullMDBNode: - "\ ctes_of s x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" + "\ ctes_of s' x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" using nullcaps apply (cases cte) apply (simp add: valid_nullcaps_def) done -lemma mdb_src: "\ ctes_of s \ x \ y; y \ 0 \ \ x \ base_bits" +lemma mdb_src: "\ ctes_of s' \ x \ y; y \ 0 \ \ x \ base_bits" apply (rule non_null_present) apply (clarsimp simp: next_unfold' cte_wp_at_ctes_of) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def) done -lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ \ y \ base_bits" +lemma mdb_dest: "\ ctes_of s' \ x \ y; y \ 0 \ \ y \ base_bits" apply (case_tac "x = 0") apply (insert no_0, simp add: next_unfold')[1] apply (drule(1) vdlist_nextD0 [OF _ _ dlist]) @@ -1137,7 +1173,7 @@ lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ done lemma trancl_next[elim]: - "\ ctes_of s \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" + "\ ctes_of s' \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" apply (erule rev_mp, erule converse_trancl_induct) apply clarsimp apply (rule r_into_trancl) @@ -1155,14 +1191,14 @@ lemma trancl_next[elim]: done lemma mdb_parent_notrange: - "ctes_of s \ x \ y \ x \ base_bits \ y \ base_bits" + "ctes_of s' \ x \ y \ x \ base_bits \ y \ base_bits" apply (erule subtree.induct) apply (frule(1) mdb_src, drule(1) mdb_dest, simp) apply (drule(1) mdb_dest, simp) done lemma mdb_parent: - "ctes_of s \ x \ y \ ctes' \ x \ y" + "ctes_of s' \ x \ y \ ctes' \ x \ y" apply (erule subtree.induct) apply (frule(1) mdb_src, frule(1) mdb_dest) apply (rule subtree.direct_parent) @@ -1178,7 +1214,7 @@ lemma mdb_parent: done lemma trancl_next_rev: - "ctes' \ x \\<^sup>+ y \ ctes_of s \ x \\<^sup>+ y" + "ctes' \ x \\<^sup>+ y \ ctes_of s' \ x \\<^sup>+ y" apply (erule converse_trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp: next_unfold') @@ -1188,7 +1224,7 @@ lemma trancl_next_rev: done lemma is_chunk[elim!]: - "is_chunk (ctes_of s) cap x y \ is_chunk ctes' cap x y" + "is_chunk (ctes_of s') cap x y \ is_chunk ctes' cap x y" apply (simp add: is_chunk_def) apply (erule allEI) apply (clarsimp dest!: trancl_next_rev) @@ -1283,7 +1319,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def intro!: cte_cap) from idle_notRange refs - have "ksIdleThread s \ ?ran" + have "ksIdleThread s' \ ?ran" apply (simp add: cte_wp_at_ctes_of valid_global_refs'_def valid_refs'_def) apply blast done @@ -1410,7 +1446,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def page_map_l4_at'_def) by fastforce - show "valid_irq_node' (irq_node' s) ?s" + show "valid_irq_node' (irq_node' s') ?s" using virq irq_nodes_range by (simp add: valid_irq_node'_def mult.commute mult.left_commute ucast_ucast_mask_8) @@ -1451,7 +1487,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def ball_ran_eq) from virqs - show "valid_irq_states' s" . + show "valid_irq_states' s'" . from no_0_objs show "no_0_obj' state'" @@ -1462,19 +1498,19 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def by (simp add: irqs_masked'_def) from sa_simp ct_act - show "sch_act_wf (ksSchedulerAction s) state'" + show "sch_act_wf (ksSchedulerAction s') state'" apply (simp add: sch_act_simple_def) - apply (case_tac "ksSchedulerAction s", simp_all add: ct_in_state'_def) + apply (case_tac "ksSchedulerAction s'", simp_all add: ct_in_state'_def) apply (fastforce dest!: st_tcb elim!: pred_tcb'_weakenE) done from invs - have "pspace_domain_valid s" by (simp add: invs'_def valid_state'_def) + have "pspace_domain_valid s'" by (simp add: invs'_def valid_state'_def) thus "pspace_domain_valid state'" by (simp add: pspace_domain_valid_def) from invs - have "valid_machine_state' s" by (simp add: invs'_def valid_state'_def) + have "valid_machine_state' s'" by (simp add: invs'_def valid_state'_def) thus "valid_machine_state' ?state''" apply (clarsimp simp: valid_machine_state'_def) apply (drule_tac x=p in spec) @@ -1529,12 +1565,11 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def apply (clarsimp dest!: ex_nonz_cap_notRange elim!: ko_wp_at'_weakenE) done - from cdm show "ksCurDomain s \ maxDomain" . + from cdm show "ksCurDomain s' \ maxDomain" . from invs - have urz: "untyped_ranges_zero' s" by (simp add: invs'_def valid_state'_def) - show "untyped_ranges_zero_inv (cteCaps_of state') - (gsUntypedZeroRanges s)" + have urz: "untyped_ranges_zero' s'" by (simp add: invs'_def valid_state'_def) + show "untyped_ranges_zero_inv (cteCaps_of state') (gsUntypedZeroRanges s')" apply (simp add: untyped_zero_ranges_cte_def urz[unfolded untyped_zero_ranges_cte_def, rule_format, symmetric]) apply (clarsimp simp: fun_eq_iff intro!: arg_cong[where f=Ex]) @@ -1547,14 +1582,14 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def qed (clarsimp) lemma (in delete_locale) delete_ko_wp_at': - assumes objs: "ko_wp_at' P p s \ ex_nonz_cap_to' p s" + assumes objs: "ko_wp_at' P p s' \ ex_nonz_cap_to' p s'" shows "ko_wp_at' P p state'" using objs by (clarsimp simp: ko_wp_at'_def ps_clear_def dom_if_None Diff_Int_distrib dest!: ex_nonz_cap_notRange) lemma (in delete_locale) null_filter': - assumes descs: "Q (null_filter' (ctes_of s))" + assumes descs: "Q (null_filter' (ctes_of s'))" shows "Q (null_filter' (ctes_of state'))" using descs ifunsafe apply (clarsimp elim!: rsubst[where P=Q]) @@ -1572,7 +1607,7 @@ lemma (in delete_locale) null_filter': done lemma (in delete_locale) delete_ex_cte_cap_to': - assumes exc: "ex_cte_cap_to' p s" + assumes exc: "ex_cte_cap_to' p s'" shows "ex_cte_cap_to' p state'" using exc by (clarsimp elim!: cte_cap) diff --git a/proof/refine/X64/EmptyFail_H.thy b/proof/refine/X64/EmptyFail_H.thy index 274d1cc81b..eddb896616 100644 --- a/proof/refine/X64/EmptyFail_H.thy +++ b/proof/refine/X64/EmptyFail_H.thy @@ -279,7 +279,7 @@ crunch (empty_fail) empty_fail: callKernel theorem call_kernel_serial: "\ (einvs and (\s. event \ Interrupt \ ct_running s) and (ct_running or ct_idle) and - (\s. scheduler_action s = resume_cur_thread) and + schact_is_rct and (\s. 0 < domain_time s \ valid_domain_list s)) s; \s'. (s, s') \ state_relation \ (invs' and (\s. event \ Interrupt \ ct_running' s) and (ct_running' or ct_idle') and diff --git a/proof/refine/X64/Refine.thy b/proof/refine/X64/Refine.thy index 3e3fe21f74..530bbac778 100644 --- a/proof/refine/X64/Refine.thy +++ b/proof/refine/X64/Refine.thy @@ -577,7 +577,7 @@ lemma kernel_corres': apply (rule_tac Q="\_. valid_sched and invs and valid_list" and E="\_. valid_sched and invs and valid_list" in hoare_post_impErr) apply (wp handle_event_valid_sched |simp)+ - apply (clarsimp simp: active_from_running) + apply (clarsimp simp: active_from_running schact_is_rct_def) apply (clarsimp simp: active_from_running') done @@ -654,6 +654,7 @@ lemma entry_corres: thread_set_not_state_valid_sched hoare_weak_lift_imp hoare_vcg_disj_lift ct_in_state_thread_state_lift | simp add: tcb_cap_cases_def ct_in_state'_def thread_set_no_change_tcb_state + schact_is_rct_def | (wps, wp threadSet_st_tcb_at2) )+ apply (clarsimp simp: invs_def cur_tcb_def) apply (clarsimp simp: ct_in_state'_def) diff --git a/proof/refine/X64/Syscall_R.thy b/proof/refine/X64/Syscall_R.thy index 130d526020..98ef62652a 100644 --- a/proof/refine/X64/Syscall_R.thy +++ b/proof/refine/X64/Syscall_R.thy @@ -400,7 +400,7 @@ lemma performInvocation_corres: "\ inv_relation i i'; call \ block \ \ corres (dc \ (=)) (einvs and valid_invocation i - and simple_sched_action + and schact_is_rct and ct_active and (\s. (\w w2 b c. i = Invocations_A.InvokeEndpoint w w2 b c) \ st_tcb_at simple (cur_thread s) s)) (invs' and sch_act_simple and valid_invocation' i' and ct_active') @@ -450,7 +450,7 @@ lemma performInvocation_corres: apply (clarsimp simp: liftME_def) apply (rule corres_guard_imp) apply (erule invokeTCB_corres) - apply (simp)+ + apply ((clarsimp dest!: schact_is_rct_simple)+)[2] \ \domain cap\ apply (clarsimp simp: invoke_domain_def) apply (rule corres_guard_imp) @@ -465,7 +465,7 @@ lemma performInvocation_corres: apply assumption apply (rule corres_trivial, simp add: returnOk_def) apply wp+ - apply (clarsimp+)[2] + apply ((clarsimp dest!: schact_is_rct_simple)+)[2] apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric]) apply (rule corres_guard_imp, rule performIRQControl_corres, simp+) apply (clarsimp simp: liftME_def[symmetric] o_def dc_def[symmetric]) @@ -1186,7 +1186,7 @@ lemmas set_thread_state_active_valid_sched = lemma handleInvocation_corres: "c \ b \ corres (dc \ dc) - (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + (einvs and schact_is_rct and ct_active) (invs' and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_invocation c b) @@ -1236,14 +1236,14 @@ lemma handleInvocation_corres: apply simp apply wp apply simp - apply (rule_tac Q="\rv. einvs and simple_sched_action and valid_invocation rve + apply (rule_tac Q="\rv. einvs and schact_is_rct and valid_invocation rve and (\s. thread = cur_thread s) and st_tcb_at active thread" in hoare_post_imp) apply (clarsimp simp: simple_from_active ct_in_state_def elim!: st_tcb_weakenE) - apply (wp sts_st_tcb_at' set_thread_state_simple_sched_action - set_thread_state_active_valid_sched) + apply (wp sts_st_tcb_at' set_thread_state_schact_is_rct + set_thread_state_active_valid_sched) apply (rule_tac Q="\rv. invs' and valid_invocation' rve' and (\s. thread = ksCurThread s) and st_tcb_at' active' thread @@ -1347,7 +1347,7 @@ lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at'] lemma handleSend_corres: "corres (dc \ dc) - (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + (einvs and schact_is_rct and ct_active) (invs' and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_send blocking) (handleSend blocking)" @@ -1774,7 +1774,7 @@ lemma hr_ct_active'[wp]: done lemma handleCall_corres: - "corres (dc \ dc) (einvs and (\s. scheduler_action s = resume_cur_thread) and ct_active) + "corres (dc \ dc) (einvs and schact_is_rct and ct_active) (invs' and (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') @@ -1954,7 +1954,7 @@ lemma handleHypervisorFault_corres: (* FIXME: move *) lemma handleEvent_corres: "corres (dc \ dc) (einvs and (\s. event \ Interrupt \ ct_running s) and - (\s. scheduler_action s = resume_cur_thread)) + schact_is_rct) (invs' and (\s. event \ Interrupt \ ct_running' s) and (\s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event)" @@ -2024,8 +2024,6 @@ proof - doMachineOp_getActiveIRQ_IRQ_active' | simp | simp add: imp_conjR | wp (once) hoare_drop_imps)+ - apply force - apply simp apply (simp add: invs'_def valid_state'_def) apply (rule_tac corres_underlying_split) apply (rule corres_guard_imp, rule getCurThread_corres, simp+) diff --git a/proof/refine/X64/Untyped_R.thy b/proof/refine/X64/Untyped_R.thy index 373064874a..551b5e7c2b 100644 --- a/proof/refine/X64/Untyped_R.thy +++ b/proof/refine/X64/Untyped_R.thy @@ -4305,7 +4305,7 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemma resetUntypedCap_corres: "untypinv_relation ui ui' \ corres (dc \ dc) - (invs and valid_untyped_inv_wcap ui + (invs and schact_is_rct and valid_untyped_inv_wcap ui (Some (cap.UntypedCap dev ptr sz idx)) and ct_active and einvs and (\_. \ptr_base ptr' ty us slots dev'. ui = Invocations_A.Retype slot True @@ -4461,7 +4461,7 @@ lemma resetUntypedCap_corres: apply (frule if_unsafe_then_capD'[OF ctes_of_cte_wpD], clarsimp+) apply (frule(1) descendants_range_ex_cte'[OF empty_descendants_range_in' _ order_refl], (simp add: isCap_simps)+) - apply (intro conjI impI; clarsimp) + apply (auto simp: descendants_range_in'_def valid_untyped'_def) done end @@ -4739,7 +4739,7 @@ defs archOverlap_def: lemma inv_untyped_corres': "\ untypinv_relation ui ui' \ \ corres (dc \ (=)) - (einvs and valid_untyped_inv ui and ct_active) + (einvs and valid_untyped_inv ui and ct_active and schact_is_rct) (invs' and valid_untyped_inv' ui' and ct_active') (invoke_untyped ui) (invokeUntyped ui')" apply (cases ui) @@ -4758,6 +4758,7 @@ lemma inv_untyped_corres': (cte_map cref) reset ptr_base ptr ao' us (map cte_map slots) dev" assume invs: "invs (s :: det_state)" "ct_active s" "valid_list s" "valid_sched s" + "schact_is_rct s" and invs': "invs' s'" "ct_active' s'" and sr: "(s, s') \ state_relation" and vui: "valid_untyped_inv_wcap ?ui (Some (cap.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s" diff --git a/spec/design/skel/PSpaceFuns_H.thy b/spec/design/skel/PSpaceFuns_H.thy index cb9a95cee5..fcc0abdb39 100644 --- a/spec/design/skel/PSpaceFuns_H.thy +++ b/spec/design/skel/PSpaceFuns_H.thy @@ -36,6 +36,6 @@ where "deleteRange m ptr bits \ consts lookupAround2 :: "('k :: {linorder,finite}) \ ( 'k , 'a ) DataMap.map \ (('k * 'a) option * 'k option)" -#INCLUDE_HASKELL SEL4/Model/PSpace.lhs bodies_only Data.Map=DataMap NOT PSpace ptrBits ptrBitsForSize lookupAround maybeToMonad typeError alignError alignCheck sizeCheck objBits deletionIsSafe cNodePartialOverlap pointerInUserData ksASIDMapSafe deleteRange +#INCLUDE_HASKELL SEL4/Model/PSpace.lhs bodies_only Data.Map=DataMap NOT PSpace ptrBits ptrBitsForSize lookupAround maybeToMonad typeError alignError alignCheck sizeCheck objBits deletionIsSafe deletionIsSafe_delete_locale cNodePartialOverlap pointerInUserData ksASIDMapSafe deleteRange end diff --git a/spec/haskell/src/SEL4/Model/PSpace.lhs b/spec/haskell/src/SEL4/Model/PSpace.lhs index 0e7478bdd3..1f8fc6d5f9 100644 --- a/spec/haskell/src/SEL4/Model/PSpace.lhs +++ b/spec/haskell/src/SEL4/Model/PSpace.lhs @@ -244,6 +244,8 @@ No type checks are performed when deleting objects; "deleteObjects" simply delet > alignError bits > stateAssert (deletionIsSafe ptr bits) > "Object deletion would leave dangling pointers" +> stateAssert (deletionIsSafe_delete_locale ptr bits) +> "Object deletion would leave dangling pointers" > doMachineOp $ freeMemory (PPtr (fromPPtr ptr)) bits > ps <- gets ksPSpace > let inRange = (\x -> x .&. ((- mask bits) - 1) == fromPPtr ptr) @@ -262,11 +264,14 @@ Clear the ghost state for user pages, cnodes, and arch-specific objects within t > Arch.deleteGhost ptr bits > stateAssert ksASIDMapSafe "Object deletion would leave dangling PD pointers" -In "deleteObjects" above, we assert "deletionIsSafe"; that is, that there are no pointers to these objects remaining elsewhere in the kernel state. Since we cannot easily check this in the Haskell model, we assume that it is always true; the assertion is strengthened during translation into Isabelle. +In "deleteObjects" above, we make two assertions, which, when taken together, say that there are no pointers to these objects remaining elsewhere in the kernel state. Since we cannot easily check this in the Haskell model, we assume that it is always true; the assertion is strengthened during translation into Isabelle. We separate these properties into two assertions, since they are shown to be true by different means. > deletionIsSafe :: PPtr a -> Int -> KernelState -> Bool > deletionIsSafe _ _ _ = True +> deletionIsSafe_delete_locale :: PPtr a -> Int -> KernelState -> Bool +> deletionIsSafe_delete_locale _ _ _ = True + We also assert that the ghost CNodes are all either completely deleted or unchanged; no CNode should be partially in the range and partially deleted. Again, this assertion requires logical quantifiers, and is inserted in translation. > cNodePartialOverlap :: (Word -> Maybe Int) -> (Word -> Bool) -> Bool