From 24000f9eb73c37ff0ebeed756f7afbf8e37fb259 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 9 Jan 2025 16:53:48 +1100 Subject: [PATCH 1/3] x64 ainvs: prove uniqueness of IOPortControlCaps This invariant is currently proved on the Haskell level only. This commit is in preparation of removing the invariant from the Haskell level, crossing it over via assertions. Signed-off-by: Gerwin Klein --- proof/invariant-abstract/X64/ArchArch_AI.thy | 12 ++++++- .../X64/ArchCNodeInv_AI.thy | 34 +++++++++++++++++++ .../X64/ArchCSpaceInv_AI.thy | 23 +++++++++++-- .../invariant-abstract/X64/ArchCSpace_AI.thy | 33 ++++++++++++++++-- .../invariant-abstract/X64/ArchDetype_AI.thy | 16 +++++---- .../X64/ArchInvariants_AI.thy | 34 +++++++++++++------ proof/invariant-abstract/X64/ArchIpc_AI.thy | 31 +++++++++++++++-- proof/invariant-abstract/X64/ArchKHeap_AI.thy | 12 +++---- .../X64/ArchKernelInit_AI.thy | 2 ++ .../invariant-abstract/X64/ArchRetype_AI.thy | 15 +++++++- .../invariant-abstract/X64/ArchTcbAcc_AI.thy | 1 + .../invariant-abstract/X64/ArchUntyped_AI.thy | 11 ++++++ .../invariant-abstract/X64/ArchVSpace_AI.thy | 5 +++ 13 files changed, 197 insertions(+), 32 deletions(-) diff --git a/proof/invariant-abstract/X64/ArchArch_AI.thy b/proof/invariant-abstract/X64/ArchArch_AI.thy index 94c32186b4..0dfde242dd 100644 --- a/proof/invariant-abstract/X64/ArchArch_AI.thy +++ b/proof/invariant-abstract/X64/ArchArch_AI.thy @@ -591,12 +591,22 @@ lemma cap_insert_ioports_ap: | wpc | simp split del: if_split)+ done +lemma cap_insert_ioport_control_ap: + "\ioport_control_unique and K (is_ap_cap cap)\ + cap_insert cap src dest + \\_. ioport_control_unique\" + unfolding cap_insert_def set_untyped_cap_as_full_def + apply (wpsimp wp: get_cap_wp set_cap_ioport_control_safe hoare_vcg_const_imp_lift) + apply (auto simp: cte_wp_at_caps_of_state is_cap_simps) + done + lemma cap_insert_valid_arch_state_ap: "\valid_arch_state and (\s. cte_wp_at (\cap'. safe_ioport_insert cap cap' s) dest s) and K (is_ap_cap cap)\ cap_insert cap src dest \\rv. valid_arch_state\" - by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_ioports_ap)+ + by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_ioports_ap + cap_insert_ioport_control_ap)+ (simp add: valid_arch_state_def) lemma cap_insert_ap_invs: diff --git a/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy b/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy index be426f12bb..9048fbba4b 100644 --- a/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy +++ b/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy @@ -444,6 +444,30 @@ lemma cap_swap_ioports[wp]: dest!: weak_derived_cap_ioports) by (fastforce elim!: ranE split: if_split_asm) +lemma same_object_as_IOPortControlCap_eq: + "same_object_as cap (ArchObjectCap IOPortControlCap) = (cap = ArchObjectCap IOPortControlCap)" + unfolding same_object_as_def + by (simp split: cap.splits arch_cap.splits) + +lemma copy_of_IOPortControlCap_eq: + "(copy_of (ArchObjectCap IOPortControlCap) cap) = (cap = ArchObjectCap IOPortControlCap)" + unfolding copy_of_def + by (auto simp: is_cap_simps same_object_as_IOPortControlCap_eq) + +lemma weak_derived_IOPortControlCap_eq[simp]: + "weak_derived (ArchObjectCap IOPortControlCap) cap = (cap = ArchObjectCap IOPortControlCap)" + unfolding weak_derived_def + by (auto simp: copy_of_IOPortControlCap_eq) + +lemma cap_swap_ioport_control[wp]: + "\ioport_control_unique and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\ + cap_swap c a c' b + \\_. ioport_control_unique\" + apply (wpsimp wp: cap_swap_caps_of_state simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: ioport_control_unique_def) + apply (cases a, cases b) + by (rule conjI; clarsimp)+ + lemma cap_swap_valid_arch_state[wp, CNodeInv_AI_assms]: "\valid_arch_state and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\ cap_swap c a c' b @@ -989,6 +1013,16 @@ lemma cap_move_ioports: dest!: weak_derived_cap_ioports) by (fastforce elim!: ranE split: if_split_asm) +lemma cap_move_ioport_control[wp]: + "\ioport_control_unique and cte_wp_at (weak_derived cap) ptr\ + cap_move cap ptr ptr' + \\_. ioport_control_unique\" + apply (wpsimp wp: cap_move_caps_of_state simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: ioport_control_unique_def) + apply (cases ptr) + apply (rule conjI; clarsimp) + done + lemma cap_move_valid_arch: "\valid_arch_state and cte_wp_at ((=) cap.NullCap) ptr' and cte_wp_at (weak_derived cap) ptr diff --git a/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy b/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy index 36defd6de2..539a44f595 100644 --- a/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy +++ b/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy @@ -49,13 +49,22 @@ lemma set_cap_ioports_safe: apply blast+ done +lemma set_cap_ioport_control_safe: + "\\s. ioport_control_unique s \ + (cap = ArchObjectCap IOPortControlCap \ cte_wp_at ((=) (ArchObjectCap IOPortControlCap)) ptr s) \ + set_cap cap ptr + \\rv. ioport_control_unique \" + apply wp + apply (auto simp: ioport_control_unique_def cte_wp_at_caps_of_state) + done + lemma set_cap_non_arch_valid_arch_state: "\\s. valid_arch_state s \ cte_wp_at (\_. \is_arch_cap cap) ptr s\ set_cap cap ptr \\rv. valid_arch_state \" unfolding valid_arch_state_def by (wp set_cap.aobj_at valid_asid_table_lift valid_global_pts_lift valid_global_pds_lift - valid_global_pdpts_lift typ_at_lift set_cap_ioports_safe)+ + valid_global_pdpts_lift typ_at_lift set_cap_ioports_safe set_cap_ioport_control_safe)+ (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps valid_pspace_def safe_ioport_insert_triv) lemma set_cap_ioports_no_new_ioports: @@ -80,12 +89,15 @@ lemma set_cap_ioports_no_new_ioports: lemma set_cap_no_new_ioports_arch_valid_arch_state: "\\s. valid_arch_state s - \ cte_wp_at (\cap'. cap_ioports cap = {} \ cap_ioports cap = cap_ioports cap') ptr s\ + \ cte_wp_at (\cap'. cap_ioports cap = {} \ cap_ioports cap = cap_ioports cap') ptr s + \ (cap = ArchObjectCap IOPortControlCap \ + cte_wp_at ((=) (ArchObjectCap IOPortControlCap)) ptr s) \ set_cap cap ptr \\rv. valid_arch_state \" unfolding valid_arch_state_def by (wp set_cap.aobj_at valid_asid_table_lift valid_global_pts_lift valid_global_pds_lift - valid_global_pdpts_lift typ_at_lift set_cap_ioports_no_new_ioports)+ + valid_global_pdpts_lift typ_at_lift set_cap_ioports_no_new_ioports + set_cap_ioport_control_safe)+ (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps valid_pspace_def) lemma valid_ioportsD: @@ -111,6 +123,10 @@ lemma unique_table_refs_no_cap_asidE: lemmas unique_table_refs_no_cap_asidD = unique_table_refs_no_cap_asidE[where S="{}"] +lemma is_ioport_control_cap_simp[simp]: + "is_ioport_control_cap (ArchObjectCap IOPortControlCap)" + by (simp add: is_ioport_control_cap_def) + lemma replace_cap_invs: "\\s. invs s \ cte_wp_at (replaceable s p cap) p s \ cap \ cap.NullCap @@ -214,6 +230,7 @@ lemma replace_cap_invs: valid_arch_caps_def unique_table_refs_no_cap_asidE) apply clarsimp apply (rule conjI, solves clarsimp) + apply (rule conjI, solves clarsimp) apply (rule Ball_emptyI, simp add: gen_obj_refs_subset) done diff --git a/proof/invariant-abstract/X64/ArchCSpace_AI.thy b/proof/invariant-abstract/X64/ArchCSpace_AI.thy index 5ab4847157..7aae58f40d 100644 --- a/proof/invariant-abstract/X64/ArchCSpace_AI.thy +++ b/proof/invariant-abstract/X64/ArchCSpace_AI.thy @@ -419,11 +419,26 @@ lemma cap_insert_derived_ioports: apply (drule_tac cap=cap in valid_ioports_issuedD, simp+) done +lemma is_derived_not_ioport_control: + "is_derived (cdt s) src cap cap' \ cap \ ArchObjectCap IOPortControlCap" + by (clarsimp simp add: is_derived_def is_derived_arch_def split: if_splits) + +lemma cap_insert_derived_ioport_control: + "\ioport_control_unique and (\s. cte_wp_at (is_derived (cdt s) src cap) src s)\ + cap_insert cap src dest + \\rv. ioport_control_unique\" + unfolding cap_insert_def set_untyped_cap_as_full_def + apply (wpsimp wp: get_cap_wp) + apply (auto dest!: is_derived_not_ioport_control + simp: cte_wp_at_caps_of_state ioport_control_unique_def is_cap_simps) + done + lemma cap_insert_derived_valid_arch_state[CSpace_AI_assms]: "\valid_arch_state and (\s. cte_wp_at (is_derived (cdt s) src cap) src s)\ cap_insert cap src dest \\rv. valid_arch_state \" - by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_derived_ioports)+ + by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_derived_ioports + cap_insert_derived_ioport_control)+ (simp add: cap_insert_aobj_at valid_arch_state_def) lemma cap_insert_simple_ioports: @@ -437,12 +452,21 @@ lemma cap_insert_simple_ioports: | wpc | simp split del: if_splits)+ done +lemma cap_insert_simple_ioport_control: + "\ioport_control_unique and K (is_simple_cap cap)\ + cap_insert cap src dest + \\rv. ioport_control_unique\" + unfolding cap_insert_def set_untyped_cap_as_full_def + by (wpsimp wp: get_cap_wp) + (auto simp: cte_wp_at_caps_of_state is_simple_cap_def ioport_control_unique_def) + lemma cap_insert_simple_valid_arch_state: "\valid_arch_state and (\s. cte_wp_at (\cap'. safe_ioport_insert cap cap' s) dest s) and K (is_simple_cap cap \ \is_ap_cap cap)\ cap_insert cap src dest \\rv. valid_arch_state\" - by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_simple_ioports)+ + by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_simple_ioports + cap_insert_simple_ioport_control)+ (simp add: valid_arch_state_def) end @@ -629,6 +653,11 @@ lemma setup_reply_master_ioports[wp]: apply (wpsimp simp: setup_reply_master_def wp: set_cap_ioports_no_new_ioports get_cap_wp) by (clarsimp simp: cte_wp_at_caps_of_state) +lemma setup_reply_master_arch_ioport_control[wp]: + "setup_reply_master t \ioport_control_unique\" + unfolding setup_reply_master_def + by (wpsimp wp: get_cap_wp simp: ioport_control_unique_def) + lemma setup_reply_master_arch[CSpace_AI_assms]: "setup_reply_master t \ valid_arch_state \" by (wp valid_arch_state_lift_ioports_typ_at setup_reply_master_ioports)+ diff --git a/proof/invariant-abstract/X64/ArchDetype_AI.thy b/proof/invariant-abstract/X64/ArchDetype_AI.thy index 2cd93f1bb6..54b138c07f 100644 --- a/proof/invariant-abstract/X64/ArchDetype_AI.thy +++ b/proof/invariant-abstract/X64/ArchDetype_AI.thy @@ -181,11 +181,15 @@ lemma tcb_arch_detype[detype_invs_proofs]: lemma valid_ioports_detype: "valid_ioports s \ valid_ioports (detype (untyped_range cap) s)" - apply (clarsimp simp: valid_ioports_def all_ioports_issued_def ioports_no_overlap_def issued_ioports_def more_update.caps_of_state_update) - apply (clarsimp simp: detype_def cap_ioports_def ran_def elim!: ranE split: if_splits cap.splits arch_cap.splits) - apply (rule conjI) - apply (force simp: ran_def) - by (metis (full_types) ranI) + apply (clarsimp simp: valid_ioports_def all_ioports_issued_def ioports_no_overlap_def + issued_ioports_def) + apply (clarsimp simp: detype_def cap_ioports_def ran_def) + by blast + +lemma ioport_control_detype: + "ioport_control_unique_2 caps \ + ioport_control_unique_2 (\p. if fst p \ S then None else caps p)" + by (auto simp: ioport_control_unique_2_def) lemma valid_arch_state_detype[detype_invs_proofs]: "valid_arch_state (detype (untyped_range cap) s)" @@ -194,7 +198,7 @@ lemma valid_arch_state_detype[detype_invs_proofs]: apply (strengthen valid_ioports_detype, simp add: valid_arch_state_def valid_asid_table_def valid_global_pdpts_def valid_global_pds_def valid_global_pts_def - global_refs_def cap_range_def) + global_refs_def cap_range_def ioport_control_detype) apply (clarsimp simp: ran_def arch_state_det) apply (drule vs_lookup_atI) apply (drule (1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI]) diff --git a/proof/invariant-abstract/X64/ArchInvariants_AI.thy b/proof/invariant-abstract/X64/ArchInvariants_AI.thy index 61ab34ef58..e5b6889437 100644 --- a/proof/invariant-abstract/X64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/X64/ArchInvariants_AI.thy @@ -1051,6 +1051,17 @@ definition where "valid_x64_irq_state irqState \ \irq > maxIRQ. irqState irq = IRQFree" +definition ioport_control_unique_2 :: "(cslot_ptr \ cap option) \ bool" where + "ioport_control_unique_2 caps \ + \p p'. caps p = Some (ArchObjectCap IOPortControlCap) \ + caps p' = Some (ArchObjectCap IOPortControlCap) \ + p' = p" + +locale_abbrev ioport_control_unique where + "ioport_control_unique s \ ioport_control_unique_2 (caps_of_state s)" + +lemmas ioport_control_unique_def = ioport_control_unique_2_def + definition valid_arch_state :: "'z::state_ext state \ bool" where @@ -1062,6 +1073,7 @@ where \ valid_global_pdpts s \ valid_cr3 (x64_current_cr3 (arch_state s)) \ valid_x64_irq_state (x64_irq_state (arch_state s)) + \ ioport_control_unique s \ valid_ioports s" definition @@ -1778,23 +1790,23 @@ lemma valid_arch_state_lift: apply (wp arch typs caps hoare_vcg_conj_lift hoare_vcg_const_Ball_lift)+ done -(* we usually have a rule for valid_ioports, but it often comes with side-conditions *) +(* we usually have a rule for valid_ioports and ioport_control_unique, but they often come with + side-conditions *) lemma valid_arch_state_lift_ioports_typ_at: - fixes Q assumes typs: "\T p. \typ_at (AArch T) p\ f \\_. typ_at (AArch T) p\" assumes arch: "\P. \\s. P (arch_state s)\ f \\_ s. P (arch_state s)\" assumes ports: "\ Q \ f \\_. valid_ioports \" - shows "\valid_arch_state and Q\ f \\_. valid_arch_state\" - apply (simp add: valid_arch_state_def pred_conj_def) + assumes control: "\ P \ f \\_. ioport_control_unique\" + shows "\valid_arch_state and Q and P\ f \\_. valid_arch_state\" apply (simp add: valid_arch_state_def valid_asid_table_def valid_global_pts_def valid_global_pds_def valid_global_pdpts_def) - (* we need to do this piece-wise so we can grab - `valid_ioports_2 (caps_of_state x) (arch_state x) \ Q x` at the end *) - apply (rule hoare_vcg_conj_lift[rotated])+ - apply (solves \wpsimp wp: ports\) - (* the rest are trivial once arch_state is lifted out *) - apply (rule hoare_lift_Pf2[where f="\s. arch_state s", OF _ arch], - solves \wp typs hoare_vcg_conj_lift hoare_vcg_const_Ball_lift\)+ + apply wp_pre + (* isolate the `valid_ioports_2 (caps_of_state s) (arch_state s)` at the end, + because we don't want wps to act on (arch_state s) there. *) + apply (rule hoare_vcg_conj_lift[rotated])+ + apply (rule ports) + apply (wps arch | wp control typs hoare_vcg_op_lift)+ + apply simp done lemma aobj_at_default_arch_cap_valid: diff --git a/proof/invariant-abstract/X64/ArchIpc_AI.thy b/proof/invariant-abstract/X64/ArchIpc_AI.thy index d99816f59d..226b0b83bb 100644 --- a/proof/invariant-abstract/X64/ArchIpc_AI.thy +++ b/proof/invariant-abstract/X64/ArchIpc_AI.thy @@ -442,6 +442,25 @@ lemma transfer_caps_loop_ioports: apply clarsimp done +lemma transfer_caps_loop_ioport_control: + "\ioport_control_unique and valid_objs and valid_mdb and K (distinct slots) + and (\s. \x \ set slots. real_cte_at x s \ cte_wp_at (\cap. cap = cap.NullCap) x s) + and transfer_caps_srcs caps\ + transfer_caps_loop ep buffer n caps slots mi + \\rv. ioport_control_unique\" + apply (rule hoare_pre) + apply (rule transfer_caps_loop_presM[where vo=True and em=False and ex=False]) + apply (wp cap_insert_derived_ioport_control) + apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (wp valid_ioports_lift) + apply (clarsimp simp:cte_wp_at_caps_of_state|intro conjI ballI)+ + apply (drule(1) bspec,clarsimp) + apply (frule(1) caps_of_state_valid) + apply (fastforce simp:valid_cap_def) + apply (drule(1) bspec) + apply clarsimp + done + lemma transfer_caps_loop_valid_arch[Ipc_AI_2_assms]: "\slots caps ep buffer n mi. \valid_arch_state and valid_objs and valid_mdb and K (distinct slots) @@ -450,7 +469,7 @@ lemma transfer_caps_loop_valid_arch[Ipc_AI_2_assms]: transfer_caps_loop ep buffer n caps slots mi \\_. valid_arch_state\" by (wpsimp wp: valid_arch_state_lift_ioports_aobj_at transfer_caps_loop_ioports - transfer_caps_loop_aobj_at) + transfer_caps_loop_ioport_control transfer_caps_loop_aobj_at) (simp add: valid_arch_state_def) lemma setup_caller_cap_aobj_at: @@ -459,14 +478,22 @@ lemma setup_caller_cap_aobj_at: unfolding setup_caller_cap_def by (wpsimp wp: cap_insert_aobj_at sts.aobj_at) +lemma setup_caller_cap_ioport_control[wp]: + "setup_caller_cap st rt grant \ioport_control_unique\" + unfolding setup_caller_cap_def cap_insert_def set_untyped_cap_as_full_def + apply (wpsimp wp: get_cap_wp split_del: if_split simp: cte_wp_at_caps_of_state) + apply (auto simp: ioport_control_unique_def) + done + lemma setup_caller_cap_valid_arch[Ipc_AI_2_assms, wp]: "setup_caller_cap st rt grant \valid_arch_state\" by (wp valid_arch_state_lift_ioports_aobj_at[rotated -1] setup_caller_cap_ioports - setup_caller_cap_aobj_at) + setup_caller_cap_aobj_at)+ (simp add: valid_arch_state_def) crunch do_ipc_transfer for ioports[wp]: "valid_ioports" + and ioport_control[wp]: "ioport_control_unique" (wp: crunch_wps hoare_vcg_const_Ball_lift transfer_caps_loop_ioports simp: zipWithM_x_mapM crunch_simps ball_conj_distrib ) diff --git a/proof/invariant-abstract/X64/ArchKHeap_AI.thy b/proof/invariant-abstract/X64/ArchKHeap_AI.thy index b2551e9b08..0be4430dae 100644 --- a/proof/invariant-abstract/X64/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/X64/ArchKHeap_AI.thy @@ -541,17 +541,17 @@ lemma typ_at_lift: (wpsimp wp: aobj_at) lemma valid_arch_state_lift_ioports_aobj_at: - fixes P assumes ioports: "\ P \ f \\_. valid_ioports \" - shows "\valid_arch_state and P\ f \\rv. valid_arch_state\" + assumes control: "\ Q \ f \\_. ioport_control_unique \" + shows "\valid_arch_state and P and Q\ f \\rv. valid_arch_state\" apply (simp add: valid_arch_state_def) apply (rule hoare_vcg_conj_lift | wp valid_asid_table_lift typ_at_lift valid_global_pts_lift valid_global_pds_lift valid_global_pdpts_lift)+ - apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp) - apply (rule hoare_vcg_conj_lift) - apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp) - apply (wp ioports) + apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp) + apply (rule hoare_vcg_conj_lift) + apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp) + apply (wp control ioports) apply simp done diff --git a/proof/invariant-abstract/X64/ArchKernelInit_AI.thy b/proof/invariant-abstract/X64/ArchKernelInit_AI.thy index a60898c122..1917227bab 100644 --- a/proof/invariant-abstract/X64/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/X64/ArchKernelInit_AI.thy @@ -305,6 +305,8 @@ lemma invs_A: apply (clarsimp simp: valid_arch_state_def) apply (rule conjI) apply (clarsimp simp: valid_asid_table_def state_defs) + apply (prop_tac "ioport_control_unique init_A_st") + apply (simp add: caps_of_state_init_A_st_Null ioport_control_unique_def) apply (subgoal_tac "valid_ioports init_A_st") apply (simp add: valid_global_pts_def valid_global_pds_def valid_global_pdpts_def valid_arch_state_def state_defs obj_at_def a_type_def diff --git a/proof/invariant-abstract/X64/ArchRetype_AI.thy b/proof/invariant-abstract/X64/ArchRetype_AI.thy index 4fda34a834..36e0e30b11 100644 --- a/proof/invariant-abstract/X64/ArchRetype_AI.thy +++ b/proof/invariant-abstract/X64/ArchRetype_AI.thy @@ -885,6 +885,15 @@ lemma ioports_no_overlap_null: apply (case_tac cap'; clarsimp) by (case_tac cap; clarsimp simp: ran_null_filter) +lemma null_filter_IOPortControlCap_eq[simp]: + "(null_filter caps p = Some (ArchObjectCap IOPortControlCap)) = + (caps p = Some (ArchObjectCap IOPortControlCap))" + by (auto simp add: null_filter_def) + +lemma ioport_control_null: + "ioport_control_unique_2 (null_filter caps) = ioport_control_unique_2 caps" + by (clarsimp simp: ioport_control_unique_def) + lemma pspace_respects_device_regionI: assumes uat: "\ptr sz. kheap s ptr = Some (ArchObj (DataPage False sz)) \ obj_range ptr (ArchObj $ DataPage False sz) \ - device_region s" @@ -1010,12 +1019,16 @@ lemma valid_ioports: "valid_ioports s \ valid_ioports s'" by (clarsimp simp: valid_ioports_def ioports_no_overlap_eq all_ioports_issued_eq) +lemmas ioport_control_eq + = arg_cong[where f=ioport_control_unique_2, OF null_filter, + simplified ioport_control_null] + lemma valid_arch_state: "valid_arch_state s \ valid_arch_state s'" unfolding valid_arch_state_def by (strengthen valid_ioports, clarsimp simp: valid_arch_state_def obj_at_pres valid_asid_table_def valid_global_pts_def - valid_global_pds_def valid_global_pdpts_def) + valid_global_pds_def valid_global_pdpts_def ioport_control_eq) lemma valid_global_objs: "valid_global_objs s \ valid_global_objs s'" diff --git a/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy b/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy index a635a890db..b3ebd49a0b 100644 --- a/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy +++ b/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy @@ -188,6 +188,7 @@ lemma thread_set_valid_arch_state[TcbAcc_AI_assms]: "(\tcb. \(getF, v) \ ran tcb_cap_cases. getF (f tcb) = getF tcb) \ thread_set f t \ valid_arch_state \" by (wp valid_arch_state_lift_ioports_aobj_at thread_set_ioports thread_set.aobj_at + thread_set_caps_of_state_trivial | simp add: valid_arch_state_def)+ end diff --git a/proof/invariant-abstract/X64/ArchUntyped_AI.thy b/proof/invariant-abstract/X64/ArchUntyped_AI.thy index 65a303877f..50fd2001c6 100644 --- a/proof/invariant-abstract/X64/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/X64/ArchUntyped_AI.thy @@ -386,6 +386,17 @@ lemma create_cap_ioports[wp]: by (wpsimp wp: set_cap_ioports_safe set_cdt_cte_wp_at simp: safe_ioport_insert_not_ioport[OF default_cap_not_ioport] create_cap_def) +lemma default_cap_neq_IOPortControlCap[simp]: + "default_cap tp oref sz dev \ ArchObjectCap IOPortControlCap" + apply (cases tp; simp) + apply (simp add: arch_default_cap_def split: aobject_type.split) + done + +lemma create_cap_ioport_control[wp]: + "create_cap tp sz p dev (cref,oref) \ioport_control_unique\" + unfolding create_cap_def + by (wpsimp simp: ioport_control_unique_def) + lemma create_cap_valid_arch_state[wp, Untyped_AI_assms]: "\valid_arch_state and cte_wp_at (\_. True) cref\ create_cap tp sz p dev (cref,oref) diff --git a/proof/invariant-abstract/X64/ArchVSpace_AI.thy b/proof/invariant-abstract/X64/ArchVSpace_AI.thy index d8cae2e16f..787b97a428 100644 --- a/proof/invariant-abstract/X64/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpace_AI.thy @@ -1334,6 +1334,10 @@ lemma master_cap_eq_is_device_cap_eq: lemmas vs_cap_ref_eq_imp_table_cap_ref_eq' = vs_cap_ref_eq_imp_table_cap_ref_eq[OF master_cap_eq_is_pg_cap_eq] +lemma IOPortControlCap_cap_master_cap_eq[simp]: + "(ArchObjectCap IOPortControlCap = cap_master_cap cap) = (cap = ArchObjectCap IOPortControlCap)" + by (simp add: cap_master_cap_def split: cap.splits arch_cap.splits) + lemma arch_update_cap_invs_map: "\cte_wp_at (is_arch_update cap and (\c. \r. vs_cap_ref c = Some r \ vs_cap_ref cap = Some r)) p @@ -1372,6 +1376,7 @@ lemma arch_update_cap_invs_map: apply (rule conjI) apply (frule master_cap_obj_refs) apply (clarsimp simp: cap_ioports_def cap_master_cap_def split: arch_cap.splits cap.splits) + apply (rule conjI, solves \clarsimp simp: cap_master_cap_simps\) apply (rule conjI, frule master_cap_obj_refs, simp) apply (rule conjI) apply (frule master_cap_obj_refs) From 1c5ebd9e38d44872f0be876d3f0f628ef3beaf9e Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 23 Jan 2025 16:02:05 +1100 Subject: [PATCH 2/3] haskell+design: archMDBAssertions in cteInsert Introduce the name and assertion "archMDBAssertions" in cteInsert so that specific architectures can make additional MDB assumptions (e.g. IOControlPortCap uniqueness in X64). Signed-off-by: Gerwin Klein --- spec/design/skel/CNode_H.thy | 3 ++- spec/haskell/src/SEL4/Object/CNode.lhs | 15 +++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/spec/design/skel/CNode_H.thy b/spec/design/skel/CNode_H.thy index d1ff1fdec4..dd3f82d9c5 100644 --- a/spec/design/skel/CNode_H.thy +++ b/spec/design/skel/CNode_H.thy @@ -31,6 +31,7 @@ where p s" by auto -#INCLUDE_HASKELL SEL4/Object/CNode.lhs bodies_only NOT finaliseSlot cteRevoke cteDeleteOne noReplyCapsFor +#INCLUDE_HASKELL SEL4/Object/CNode.lhs bodies_only NOT finaliseSlot cteRevoke \ + cteDeleteOne noReplyCapsFor archMDBAssertions end diff --git a/spec/haskell/src/SEL4/Object/CNode.lhs b/spec/haskell/src/SEL4/Object/CNode.lhs index 5040dc03ac..14ef389082 100644 --- a/spec/haskell/src/SEL4/Object/CNode.lhs +++ b/spec/haskell/src/SEL4/Object/CNode.lhs @@ -231,6 +231,15 @@ The following functions define the operations that can be performed by a CNode i \subsubsection{Inserting New Capabilities} +\begin{impdetails} + +Arch assertions for the refinement proof. Content is defined in Isabelle. + +> archMDBAssertions :: KernelState -> Bool +> archMDBAssertions _ = error "defined in Isabelle" + +\end{impdetails} + > setUntypedCapAsFull :: Capability -> Capability -> PPtr CTE -> Kernel () > setUntypedCapAsFull srcCap newCap srcSlot = do > if (isUntypedCap srcCap && isUntypedCap newCap && @@ -242,6 +251,12 @@ Insertion of new capabilities copied from existing capabilities is performed by > cteInsert :: Capability -> PPtr CTE -> PPtr CTE -> Kernel () > cteInsert newCap srcSlot destSlot = do +\begin{impdetails} + +> stateAssert archMDBAssertions "architecture dependent MDB assertions must hold" + +\end{impdetails} + First, fetch the capability table entry for the source. > srcCTE <- getCTE srcSlot From 708927ea5dcc439c2a944af68f9104711c317c13 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 21 Jan 2025 17:23:00 +1100 Subject: [PATCH 3/3] refine+crefine: remove valid_arch_mdb_ctes - replace the ioport_control invariant with archMDBAssertions - remove lemmas needed only for the invariant - add corresponding crossing lemmas for caps_of_state based on existing older cte_wp_at lemmas Signed-off-by: Gerwin Klein --- proof/crefine/AARCH64/CSpace_C.thy | 5 +- proof/crefine/AARCH64/Fastpath_C.thy | 2 + .../crefine/AARCH64/IsolatedThreadAction.thy | 17 +- proof/crefine/ARM/CSpace_C.thy | 3 +- proof/crefine/ARM/Fastpath_C.thy | 2 + proof/crefine/ARM/IsolatedThreadAction.thy | 17 +- proof/crefine/ARM_HYP/CSpace_C.thy | 3 +- proof/crefine/ARM_HYP/Fastpath_C.thy | 2 + .../crefine/ARM_HYP/IsolatedThreadAction.thy | 17 +- proof/crefine/X64/CSpace_C.thy | 5 +- proof/crefine/X64/IsolatedThreadAction.thy | 17 +- proof/refine/AARCH64/ArchInvsDefs_H.thy | 3 - proof/refine/AARCH64/Arch_R.thy | 9 +- proof/refine/AARCH64/CNodeInv_R.thy | 3 - proof/refine/AARCH64/CSpace1_R.thy | 94 +++++--- proof/refine/AARCH64/CSpace_R.thy | 36 +-- proof/refine/AARCH64/Interrupt_R.thy | 3 + proof/refine/AARCH64/InvariantUpdates_H.thy | 6 - proof/refine/AARCH64/Ipc_R.thy | 50 +++-- proof/refine/AARCH64/Tcb_R.thy | 2 +- proof/refine/ARM/ArchInvsDefs_H.thy | 3 - proof/refine/ARM/Arch_R.thy | 9 +- proof/refine/ARM/CNodeInv_R.thy | 3 - proof/refine/ARM/CSpace1_R.thy | 94 +++++--- proof/refine/ARM/CSpace_R.thy | 37 +-- proof/refine/ARM/Interrupt_R.thy | 3 + proof/refine/ARM/InvariantUpdates_H.thy | 6 - proof/refine/ARM/Ipc_R.thy | 50 +++-- proof/refine/ARM/Tcb_R.thy | 2 +- proof/refine/ARM_HYP/ArchInvsDefs_H.thy | 3 - proof/refine/ARM_HYP/Arch_R.thy | 9 +- proof/refine/ARM_HYP/CNodeInv_R.thy | 3 - proof/refine/ARM_HYP/CSpace1_R.thy | 94 +++++--- proof/refine/ARM_HYP/CSpace_R.thy | 37 +-- proof/refine/ARM_HYP/Interrupt_R.thy | 3 + proof/refine/ARM_HYP/InvariantUpdates_H.thy | 6 - proof/refine/ARM_HYP/Ipc_R.thy | 50 +++-- proof/refine/ARM_HYP/Tcb_R.thy | 2 +- proof/refine/Invariants_H.thy | 8 +- proof/refine/X64/ArchInvsDefs_H.thy | 12 - proof/refine/X64/ArchInvsLemmas_H.thy | 9 - proof/refine/X64/Arch_R.thy | 17 +- proof/refine/X64/CNodeInv_R.thy | 80 +------ proof/refine/X64/CSpace1_R.thy | 211 +++++++++--------- proof/refine/X64/CSpace_I.thy | 38 +--- proof/refine/X64/CSpace_R.thy | 164 +++----------- proof/refine/X64/Detype_R.thy | 5 - proof/refine/X64/Finalise_R.thy | 13 -- proof/refine/X64/Interrupt_R.thy | 19 +- proof/refine/X64/Ipc_R.thy | 50 +++-- proof/refine/X64/Retype_R.thy | 11 +- proof/refine/X64/Tcb_R.thy | 2 +- proof/refine/X64/Untyped_R.thy | 8 - 53 files changed, 668 insertions(+), 689 deletions(-) diff --git a/proof/crefine/AARCH64/CSpace_C.thy b/proof/crefine/AARCH64/CSpace_C.thy index f3cc296f8e..2d4ecb29b8 100644 --- a/proof/crefine/AARCH64/CSpace_C.thy +++ b/proof/crefine/AARCH64/CSpace_C.thy @@ -985,8 +985,9 @@ lemma cteInsert_ccorres: (Call cteInsert_'proc)" supply ctes_of_aligned_bits[simp] apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_' - simp del: return_bind simp add: Collect_const) + simp del: return_bind simp add: Collect_const) apply (rule ccorres_move_c_guard_cte) + apply (rule ccorres_stateAssert) apply (ctac pre: ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) @@ -1040,7 +1041,7 @@ lemma cteInsert_ccorres: apply (frule valid_cap_untyped_inv) apply clarsimp apply (rule conjI) - apply (case_tac ctea) + apply (case_tac cte) apply (clarsimp simp: isUntypedCap_def split: capability.splits) apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) apply fastforce diff --git a/proof/crefine/AARCH64/Fastpath_C.thy b/proof/crefine/AARCH64/Fastpath_C.thy index 18fe506b69..a8dacac7fa 100644 --- a/proof/crefine/AARCH64/Fastpath_C.thy +++ b/proof/crefine/AARCH64/Fastpath_C.thy @@ -2279,6 +2279,7 @@ proof - apply (rule ccorres_assert2) apply (rule ccorres_pre_threadGet, rename_tac destState) apply (rule_tac P="isReceive destState" in ccorres_gen_asm) + apply (rule ccorres_stateAssert) apply (rule ccorres_pre_getCTE2, rename_tac curThreadReplyCTE2) apply (rule ccorres_pre_getCTE2, rename_tac destCallerCTE) apply (rule ccorres_assert2)+ @@ -2449,6 +2450,7 @@ proof - apply (rule conseqPre, vcg, clarsimp) apply (simp add: cte_level_bits_def field_simps shiftl_t2n ctes_of_Some_cte_wp_at + archMDBAssertions_def del: all_imp_to_ex cong: imp_cong conj_cong) apply (wp hoare_vcg_all_lift threadSet_ctes_of hoare_vcg_imp_lift' threadSet_valid_objs' diff --git a/proof/crefine/AARCH64/IsolatedThreadAction.thy b/proof/crefine/AARCH64/IsolatedThreadAction.thy index ea26491a83..82b47cc01f 100644 --- a/proof/crefine/AARCH64/IsolatedThreadAction.thy +++ b/proof/crefine/AARCH64/IsolatedThreadAction.thy @@ -1528,6 +1528,20 @@ lemma setCTE_isolatable: apply (clarsimp simp: obj_at'_def projectKOs) done +lemma archMDBAssertions_isolatable: + "thread_actions_isolatable idx (stateAssert archMDBAssertions [])" + unfolding stateAssert_def archMDBAssertions_def + apply (clarsimp simp: thread_actions_isolatable_def) + apply (simp add: isolate_thread_actions_def bind_assoc split_def) + apply (simp add: bind_select_f_bind[symmetric] select_f_returns) + apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def + map_to_ctes_partial_overwrite) + apply (simp add: select_f_asserts) + apply (clarsimp simp: exec_modify o_def return_def) + apply (simp add: ksPSpace_update_partial_id) + apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def) + done + lemma cteInsert_isolatable: "thread_actions_isolatable idx (cteInsert cap src dest)" supply if_split[split del] if_cong[cong] @@ -1536,7 +1550,8 @@ lemma cteInsert_isolatable: apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre] thread_actions_isolatable_if thread_actions_isolatable_returns - getCTE_isolatable setCTE_isolatable) + getCTE_isolatable setCTE_isolatable + archMDBAssertions_isolatable) apply (wp | simp)+ done diff --git a/proof/crefine/ARM/CSpace_C.thy b/proof/crefine/ARM/CSpace_C.thy index 84d0b1f044..792d3a2e0c 100644 --- a/proof/crefine/ARM/CSpace_C.thy +++ b/proof/crefine/ARM/CSpace_C.thy @@ -1010,6 +1010,7 @@ lemma cteInsert_ccorres: simp del: return_bind simp add: Collect_const) apply (rule ccorres_move_c_guard_cte) + apply (rule ccorres_stateAssert) apply (ctac pre: ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) @@ -1063,7 +1064,7 @@ lemma cteInsert_ccorres: apply (frule valid_cap_untyped_inv) apply clarsimp apply (rule conjI) - apply (case_tac ctea) + apply (case_tac cte) apply (clarsimp simp: isUntypedCap_def split: capability.splits) apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) apply fastforce diff --git a/proof/crefine/ARM/Fastpath_C.thy b/proof/crefine/ARM/Fastpath_C.thy index 6e14968108..48ecb62ebc 100644 --- a/proof/crefine/ARM/Fastpath_C.thy +++ b/proof/crefine/ARM/Fastpath_C.thy @@ -2083,6 +2083,7 @@ proof - apply (rule ccorres_assert2) apply (rule ccorres_pre_threadGet, rename_tac destState) apply (rule_tac P="isReceive destState" in ccorres_gen_asm) + apply (rule ccorres_stateAssert) apply (rule ccorres_pre_getCTE2, rename_tac curThreadReplyCTE2) apply (rule ccorres_pre_getCTE2, rename_tac destCallerCTE) apply (rule ccorres_assert2)+ @@ -2246,6 +2247,7 @@ proof - apply (rule conseqPre, vcg, clarsimp) apply (simp add: cte_level_bits_def field_simps shiftl_t2n ctes_of_Some_cte_wp_at + archMDBAssertions_def del: all_imp_to_ex cong: imp_cong conj_cong) apply (wp hoare_vcg_all_lift threadSet_ctes_of hoare_vcg_imp_lift' threadSet_valid_objs' diff --git a/proof/crefine/ARM/IsolatedThreadAction.thy b/proof/crefine/ARM/IsolatedThreadAction.thy index 4f54066de2..61b7d713fb 100644 --- a/proof/crefine/ARM/IsolatedThreadAction.thy +++ b/proof/crefine/ARM/IsolatedThreadAction.thy @@ -1141,6 +1141,20 @@ lemma assert_isolatable: thread_actions_isolatable_returns thread_actions_isolatable_fail) +lemma archMDBAssertions_isolatable: + "thread_actions_isolatable idx (stateAssert archMDBAssertions [])" + unfolding stateAssert_def archMDBAssertions_def + apply (clarsimp simp: thread_actions_isolatable_def) + apply (simp add: isolate_thread_actions_def bind_assoc split_def) + apply (simp add: bind_select_f_bind[symmetric] select_f_returns) + apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def + map_to_ctes_partial_overwrite) + apply (simp add: select_f_asserts) + apply (clarsimp simp: exec_modify o_def return_def) + apply (simp add: ksPSpace_update_partial_id) + apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def) + done + lemma cteInsert_isolatable: "thread_actions_isolatable idx (cteInsert cap src dest)" supply if_split[split del] if_cong[cong] @@ -1149,7 +1163,8 @@ lemma cteInsert_isolatable: apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre] thread_actions_isolatable_if thread_actions_isolatable_returns assert_isolatable - getCTE_isolatable setCTE_isolatable) + getCTE_isolatable setCTE_isolatable + archMDBAssertions_isolatable) apply (wp | simp)+ done diff --git a/proof/crefine/ARM_HYP/CSpace_C.thy b/proof/crefine/ARM_HYP/CSpace_C.thy index b7029f9449..e7abb000ef 100644 --- a/proof/crefine/ARM_HYP/CSpace_C.thy +++ b/proof/crefine/ARM_HYP/CSpace_C.thy @@ -1050,6 +1050,7 @@ lemma cteInsert_ccorres: simp del: return_bind simp add: Collect_const) apply (rule ccorres_move_c_guard_cte) + apply (rule ccorres_stateAssert) apply (ctac pre: ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) @@ -1103,7 +1104,7 @@ lemma cteInsert_ccorres: apply (frule valid_cap_untyped_inv) apply clarsimp apply (rule conjI) - apply (case_tac ctea) + apply (case_tac cte) apply (clarsimp simp: isUntypedCap_def split: capability.splits) apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) apply fastforce diff --git a/proof/crefine/ARM_HYP/Fastpath_C.thy b/proof/crefine/ARM_HYP/Fastpath_C.thy index 5ba460dc59..e7c9912ba5 100644 --- a/proof/crefine/ARM_HYP/Fastpath_C.thy +++ b/proof/crefine/ARM_HYP/Fastpath_C.thy @@ -2129,6 +2129,7 @@ proof - apply (rule ccorres_assert2) apply (rule ccorres_pre_threadGet, rename_tac destState) apply (rule_tac P="isReceive destState" in ccorres_gen_asm) + apply (rule ccorres_stateAssert) apply (rule ccorres_pre_getCTE2, rename_tac curThreadReplyCTE2) apply (rule ccorres_pre_getCTE2, rename_tac destCallerCTE) apply (rule ccorres_assert2)+ @@ -2290,6 +2291,7 @@ proof - apply (rule conseqPre, vcg, clarsimp) apply (simp add: cte_level_bits_def field_simps shiftl_t2n ctes_of_Some_cte_wp_at + archMDBAssertions_def del: all_imp_to_ex cong: imp_cong conj_cong) apply (wp hoare_vcg_all_lift threadSet_ctes_of hoare_vcg_imp_lift' threadSet_valid_objs' diff --git a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy index 9b2c5fd10e..e71ebcaebf 100644 --- a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy +++ b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy @@ -1416,6 +1416,20 @@ lemma assert_isolatable: thread_actions_isolatable_returns thread_actions_isolatable_fail) +lemma archMDBAssertions_isolatable: + "thread_actions_isolatable idx (stateAssert archMDBAssertions [])" + unfolding stateAssert_def archMDBAssertions_def + apply (clarsimp simp: thread_actions_isolatable_def) + apply (simp add: isolate_thread_actions_def bind_assoc split_def) + apply (simp add: bind_select_f_bind[symmetric] select_f_returns) + apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def + map_to_ctes_partial_overwrite) + apply (simp add: select_f_asserts) + apply (clarsimp simp: exec_modify o_def return_def) + apply (simp add: ksPSpace_update_partial_id) + apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def) + done + lemma cteInsert_isolatable: "thread_actions_isolatable idx (cteInsert cap src dest)" supply if_split[split del] if_cong[cong] @@ -1424,7 +1438,8 @@ lemma cteInsert_isolatable: apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre] thread_actions_isolatable_if thread_actions_isolatable_returns assert_isolatable - getCTE_isolatable setCTE_isolatable) + getCTE_isolatable setCTE_isolatable + archMDBAssertions_isolatable) apply (wp | simp)+ done diff --git a/proof/crefine/X64/CSpace_C.thy b/proof/crefine/X64/CSpace_C.thy index e8b39a5233..f7b50972dc 100644 --- a/proof/crefine/X64/CSpace_C.thy +++ b/proof/crefine/X64/CSpace_C.thy @@ -1020,8 +1020,9 @@ lemma cteInsert_ccorres: (Call cteInsert_'proc)" supply ctes_of_aligned_bits[simp] apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_' - simp del: return_bind simp add: Collect_const) + simp del: return_bind simp add: Collect_const) apply (rule ccorres_move_c_guard_cte) + apply (rule ccorres_stateAssert) apply (ctac pre: ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) @@ -1075,7 +1076,7 @@ lemma cteInsert_ccorres: apply (frule valid_cap_untyped_inv) apply clarsimp apply (rule conjI) - apply (case_tac ctea) + apply (case_tac cte) apply (clarsimp simp: isUntypedCap_def split: capability.splits) apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) apply fastforce diff --git a/proof/crefine/X64/IsolatedThreadAction.thy b/proof/crefine/X64/IsolatedThreadAction.thy index 53b98565d6..f2a11252e8 100644 --- a/proof/crefine/X64/IsolatedThreadAction.thy +++ b/proof/crefine/X64/IsolatedThreadAction.thy @@ -1167,6 +1167,20 @@ lemma assert_isolatable: thread_actions_isolatable_returns thread_actions_isolatable_fail) +lemma archMDBAssertions_isolatable: + "thread_actions_isolatable idx (stateAssert archMDBAssertions [])" + unfolding stateAssert_def archMDBAssertions_def + apply (clarsimp simp: thread_actions_isolatable_def) + apply (simp add: isolate_thread_actions_def bind_assoc split_def) + apply (simp add: bind_select_f_bind[symmetric] select_f_returns) + apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def + map_to_ctes_partial_overwrite) + apply (simp add: select_f_asserts) + apply (clarsimp simp: exec_modify o_def return_def) + apply (simp add: ksPSpace_update_partial_id) + apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def) + done + lemma cteInsert_isolatable: "thread_actions_isolatable idx (cteInsert cap src dest)" supply if_split[split del] if_cong[cong] @@ -1175,7 +1189,8 @@ lemma cteInsert_isolatable: apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre] thread_actions_isolatable_if thread_actions_isolatable_returns assert_isolatable - getCTE_isolatable setCTE_isolatable) + getCTE_isolatable setCTE_isolatable + archMDBAssertions_isolatable) apply (wp | simp)+ done diff --git a/proof/refine/AARCH64/ArchInvsDefs_H.thy b/proof/refine/AARCH64/ArchInvsDefs_H.thy index 3818e78c9e..cf0a534a92 100644 --- a/proof/refine/AARCH64/ArchInvsDefs_H.thy +++ b/proof/refine/AARCH64/ArchInvsDefs_H.thy @@ -194,9 +194,6 @@ definition where "isArchFrameCap cap \ case cap of ArchObjectCap (FrameCap _ _ _ _ _) \ True | _ \ False" -definition valid_arch_mdb_ctes :: "cte_heap \ bool" where - "valid_arch_mdb_ctes \ \" - (* Addresses of all PTEs in a VSRoot table at p *) definition table_refs' :: "machine_word \ machine_word set" where "table_refs' p \ (\i. p + (i << pte_bits)) ` mask_range 0 (ptTranslationBits VSRootPT_T)" diff --git a/proof/refine/AARCH64/Arch_R.thy b/proof/refine/AARCH64/Arch_R.thy index ff4072cd66..30cb21d78e 100644 --- a/proof/refine/AARCH64/Arch_R.thy +++ b/proof/refine/AARCH64/Arch_R.thy @@ -143,6 +143,7 @@ lemma performASIDControlInvocation_corres: apply (cases i) apply (rename_tac word1 prod1 prod2 word2) apply (clarsimp simp: asid_ci_map_def) + apply (rename_tac p slot p' slot' word2) apply (simp add: perform_asid_control_invocation_def placeNewObject_def2 performASIDControlInvocation_def) apply (rule corres_name_pre) @@ -195,7 +196,7 @@ lemma performASIDControlInvocation_corres: apply wp+ apply (strengthen safe_parent_strg[where idx = "2^pageBits"]) apply (strengthen invs_valid_objs invs_distinct - invs_psp_aligned invs_mdb + invs_psp_aligned invs_mdb invs_arch_state | simp cong:conj_cong)+ apply (wp retype_region_plain_invs[where sz = pageBits] retype_cte_wp_at[where sz = pageBits])+ @@ -279,7 +280,7 @@ lemma performASIDControlInvocation_corres: apply (drule detype_locale.non_null_present) apply (fastforce simp: cte_wp_at_caps_of_state) apply simp - apply (frule_tac ptr = "(aa,ba)" in detype_invariants [rotated 3]) + apply (frule_tac ptr = "(p', slot')" in detype_invariants [rotated 3]) apply fastforce apply simp apply (simp add: cte_wp_at_caps_of_state) @@ -304,7 +305,7 @@ lemma performASIDControlInvocation_corres: apply (simp add:detype_clear_um_independent) apply (rule conjI) apply clarsimp - apply (drule_tac p = "(aa,ba)" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) + apply (drule_tac p = "(p', slot')" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) apply fastforce apply (clarsimp simp: region_in_kernel_window_def valid_cap_def cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def) @@ -319,7 +320,7 @@ lemma performASIDControlInvocation_corres: st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def wrap_ext_det_ext_ext_def) apply (simp add: detype_def clear_um_def) - apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (drule_tac x = "cte_map (p', slot')" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) apply (simp add:invs_valid_objs)+ apply clarsimp apply (drule cte_map_inj_eq) diff --git a/proof/refine/AARCH64/CNodeInv_R.thy b/proof/refine/AARCH64/CNodeInv_R.thy index 7be1e991d8..aead729009 100644 --- a/proof/refine/AARCH64/CNodeInv_R.thy +++ b/proof/refine/AARCH64/CNodeInv_R.thy @@ -8398,9 +8398,6 @@ proof apply (erule (1) irq_controlD, rule irq_control) done - show "valid_arch_mdb_ctes m'" - by simp - have distz: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def) diff --git a/proof/refine/AARCH64/CSpace1_R.thy b/proof/refine/AARCH64/CSpace1_R.thy index 322e8b604c..0305fcbacf 100644 --- a/proof/refine/AARCH64/CSpace1_R.thy +++ b/proof/refine/AARCH64/CSpace1_R.thy @@ -14,6 +14,20 @@ imports CSpace_I begin +context Arch begin arch_global_naming + +(* No assertion necessary for this architecture. *) +definition arch_mdb_assert :: "cte_heap \ bool" where + "arch_mdb_assert m \ True" + +end + +arch_requalify_consts + arch_mdb_assert + +defs archMDBAssertions_def: + "archMDBAssertions s \ arch_mdb_assert (ctes_of s)" + context Arch begin global_naming AARCH64_A (*FIXME: arch-split*) lemmas final_matters_def = final_matters_def[simplified final_matters_arch_def] @@ -248,7 +262,7 @@ lemma pspace_relation_cte_wp_at: lemma pspace_relation_ctes_ofI: "\ pspace_relation (kheap s) (ksPSpace s'); - cte_wp_at ((=) c) slot s; pspace_aligned' s'; + cte_wp_at ((=) c) slot s; pspace_aligned' s'; pspace_distinct' s' \ \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" apply (cases slot, clarsimp) @@ -256,6 +270,22 @@ lemma pspace_relation_ctes_ofI: apply (simp add: cte_wp_at_ctes_of) done +lemma pspace_relation_caps_of_state_cross: + "\ pspace_relation (kheap s) (ksPSpace s'); + caps_of_state s slot = Some c; pspace_aligned s; pspace_distinct s \ + \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" + for s' :: kernel_state + by (auto simp: cte_wp_at_caps_of_state + intro!: pspace_relation_ctes_ofI pspace_aligned_cross pspace_distinct_cross) + +lemma caps_of_state_cross: + "\ caps_of_state s slot = Some cap; pspace_aligned s; pspace_distinct s; (s,s') \ state_relation \ + \ \cap'. cteCaps_of s' (cte_map slot) = Some cap' \ cap_relation cap cap'" + apply (erule state_relationE) + apply (drule (3) pspace_relation_caps_of_state_cross) + apply (fastforce simp: cteCaps_of_def) + done + lemma get_cap_corres_P: "corres (\x y. cap_relation x (cteCap y) \ P x) (cte_wp_at P cslot_ptr) @@ -912,21 +942,13 @@ lemma ctes_of_valid_cap'': done lemma cap_insert_objs' [wp]: - "\valid_objs' - and valid_cap' cap\ - cteInsert cap src dest \\rv. valid_objs'\" - including no_pre - apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: if_split) - apply (wp setCTE_valid_objs) - apply simp - apply wp+ - apply (clarsimp simp: updateCap_def) - apply (wp|simp)+ - apply (rule hoare_drop_imp)+ - apply wp+ - apply (rule hoare_strengthen_post[OF getCTE_sp]) + "\valid_objs' and valid_cap' cap\ + cteInsert cap src dest + \\_. valid_objs'\" + apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: setCTE_valid_objs | wp getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps - dest!: ctes_of_valid_cap'') + dest!: ctes_of_valid_cap'') done lemma cteInsert_weak_cte_wp_at: @@ -1964,6 +1986,14 @@ lemma pspace_relation_cte_wp_atI: apply assumption done +lemma caps_of_state_rev_cross: + "\ ctes_of s' p = Some cte; valid_objs s; (s,s') \ state_relation \ + \ \cap slot. caps_of_state s slot = Some cap \ p = cte_map slot \ cap_relation cap (cteCap cte)" + apply (erule state_relationE) + apply (drule (2) pspace_relation_cte_wp_atI) + apply (fastforce simp: cte_wp_at_caps_of_state) + done + lemma sameRegion_corres: "\ sameRegionAs c' d'; cap_relation c c'; cap_relation d d' \ \ same_region_as c d" @@ -5195,6 +5225,15 @@ lemma cte_map_inj_eq': done context begin interpretation Arch . (*FIXME: arch-split*) + +(* interface lemma: generic statement, arch-specific proof *) +lemma archMDBAssertions_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_arch_state s; valid_objs s; + (s, s') \ state_relation \ + \ archMDBAssertions s'" + unfolding archMDBAssertions_def + by (simp add: arch_mdb_assert_def) + lemma cteInsert_corres: notes split_paired_All[simp del] split_paired_Ex[simp del] trans_state_update'[symmetric,simp] @@ -5203,30 +5242,33 @@ lemma cteInsert_corres: (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=Structures_A.NullCap) dest and - (\s. cte_wp_at (is_derived (cdt s) src c) src s)) + (\s. cte_wp_at (is_derived (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and cte_wp_at' (\c. cteCap c=NullCap) dest') (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _) _ _") using assms unfolding cap_insert_def cteInsert_def apply simp + (* this lemma doesn't use the assertion, but does need to establish it *) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (is_derived (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src)" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -5235,7 +5277,7 @@ lemma cteInsert_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. (is_derived (cdt s) src c) src_cap) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) and + R'="\r. ?P' and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src)" in corres_split[where r'=dc]) @@ -5299,7 +5341,7 @@ lemma cteInsert_corres: apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") @@ -5587,7 +5629,7 @@ lemma cteInsert_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = isCapRevocable c' (cteCap srcCTE)") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply simp apply (rule is_cap_revocable_eq, assumption, assumption) @@ -5600,7 +5642,7 @@ lemma cteInsert_corres: split:if_splits dest!:cap_master_cap_eqDs) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5626,7 +5668,7 @@ lemma cteInsert_corres: apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) @@ -5636,7 +5678,7 @@ lemma cteInsert_corres: apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") diff --git a/proof/refine/AARCH64/CSpace_R.thy b/proof/refine/AARCH64/CSpace_R.thy index 6778d2349e..498fb85bd5 100644 --- a/proof/refine/AARCH64/CSpace_R.thy +++ b/proof/refine/AARCH64/CSpace_R.thy @@ -4519,6 +4519,7 @@ end locale mdb_insert_simple = mdb_insert + assumes safe_parent: "safe_parent_for' m src c'" assumes simple: "is_simple_cap' c'" + assumes arch_mdb_assert: "arch_mdb_assert m" begin interpretation Arch . (*FIXME: arch-split*) @@ -4717,6 +4718,12 @@ lemma maskedAsFull_revokable_safe_parent: context begin interpretation Arch . (*FIXME: arch-split*) +(* FIXME arch-split: generic statement, arch specific proof *) +lemma setUntypedCapAsFull_archMDBAssertions[wp]: + "setUntypedCapAsFull src_cap cap p \archMDBAssertions\" + unfolding archMDBAssertions_def arch_mdb_assert_def + by wp + lemma cteInsert_simple_corres: assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest" notes trans_state_update'[symmetric,simp] @@ -4725,34 +4732,36 @@ lemma cteInsert_simple_corres: valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=cap.NullCap) dest and K (is_simple_cap c) and - (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s)) + (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and K (is_simple_cap' c') and cte_wp_at' (\c. cteCap c=NullCap) dest' and (\s. safe_parent_for' (ctes_of s) src' c')) (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _ and _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _ and _) _ _") using assms unfolding cap_insert_def cteInsert_def supply subst_all [simp del] apply simp + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and - Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + Q="?P' and archMDBAssertions and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -4761,7 +4770,7 @@ lemma cteInsert_simple_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) + R'="\r. ?P' and archMDBAssertions and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_split[where r'=dc]) @@ -4856,7 +4865,7 @@ lemma cteInsert_simple_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = isCapRevocable c' (cteCap srcCTE)") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) apply (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply clarsimp apply (rule is_cap_revocable_eq, assumption, assumption) @@ -4869,7 +4878,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -4893,14 +4902,14 @@ lemma cteInsert_simple_corres: set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") @@ -4924,7 +4933,8 @@ lemma cteInsert_simple_corres: apply (simp (no_asm_simp) add: cdt_relation_def split: if_split) apply (intro impI allI) apply (frule mdb_insert_simple_axioms.intro) - apply(clarsimp simp:cte_wp_at_ctes_of) + apply(clarsimp simp:cte_wp_at_ctes_of) + apply (simp add: archMDBAssertions_def) apply (drule (1) mdb_insert_simple.intro) apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable_safe_parent[symmetric]) apply simp+ @@ -5820,7 +5830,7 @@ lemma cteInsert_simple_mdb': mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ - apply ((clarsimp simp:valid_mdb_ctes_def)+) + apply (clarsimp simp:valid_mdb_ctes_def archMDBAssertions_def)+ apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) done diff --git a/proof/refine/AARCH64/Interrupt_R.thy b/proof/refine/AARCH64/Interrupt_R.thy index b6985106fa..47d0f51a8d 100644 --- a/proof/refine/AARCH64/Interrupt_R.thy +++ b/proof/refine/AARCH64/Interrupt_R.thy @@ -477,6 +477,9 @@ lemma setIRQTrigger_corres: | simp add: dc_def)+ done +crunch set_irq_state + for valid_arch_state[wp]: valid_arch_state + lemma arch_performIRQControl_corres: "arch_irq_control_inv_relation x2 ivk' \ corres (dc \ dc) (einvs and arch_irq_control_inv_valid x2) diff --git a/proof/refine/AARCH64/InvariantUpdates_H.thy b/proof/refine/AARCH64/InvariantUpdates_H.thy index 156fbec100..c065290e69 100644 --- a/proof/refine/AARCH64/InvariantUpdates_H.thy +++ b/proof/refine/AARCH64/InvariantUpdates_H.thy @@ -516,10 +516,4 @@ lemma invs'_gsTypes_update: end -(* FIXME arch-split: valid_arch_mdb_ctes only exists to contain ioport_control on x64, and it is not - yet clear what the best way to arch-split it is, or whether it can be crossed from AInvs. - Therefore, for now, export the truth that it doesn't do anything on this arch beyond this point *) -arch_requalify_facts valid_arch_mdb_ctes_def -lemmas [simp] = valid_arch_mdb_ctes_def - end diff --git a/proof/refine/AARCH64/Ipc_R.thy b/proof/refine/AARCH64/Ipc_R.thy index ef18b656ec..56c206ddb7 100644 --- a/proof/refine/AARCH64/Ipc_R.thy +++ b/proof/refine/AARCH64/Ipc_R.thy @@ -392,6 +392,10 @@ lemma cte_refs'_maskedAsFull[simp]: apply (clarsimp simp:maskedAsFull_def isCap_simps)+ done +lemma set_extra_badge_valid_arch_state[wp]: + "set_extra_badge buffer badge n \ valid_arch_state \" + unfolding set_extra_badge_def + by wp lemma transferCapsToSlots_corres: "\ list_all2 (\(cap, slot) (cap', slot'). cap_relation cap cap' @@ -399,7 +403,7 @@ lemma transferCapsToSlots_corres: mi' = message_info_map mi \ \ corres ((=) \ message_info_map) (\s. valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_mdb s - \ valid_list s + \ valid_list s \ valid_arch_state s \ (case ep of Some x \ ep_at x s | _ \ True) \ (\x \ set slots. cte_wp_at (\cap. cap = cap.NullCap) x s \ real_cte_at x s) @@ -473,7 +477,8 @@ next apply (simp add: tl_map) apply (rule corres_rel_imp, rule Cons.hyps, simp_all)[1] apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift - hoare_vcg_const_Ball_lift cap_insert_weak_cte_wp_at) + hoare_vcg_const_Ball_lift cap_insert_derived_valid_arch_state + cap_insert_weak_cte_wp_at) apply (wp hoare_vcg_const_Ball_lift | simp add:split_def del: imp_disj1)+ apply (wp cap_insert_cte_wp_at) apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift @@ -614,6 +619,7 @@ lemma cteInsert_assume_Null: apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cteInsert_def) + apply (rule bind_wp[OF _ stateAssert_sp]) apply (rule bind_wp[OF _ getCTE_sp])+ apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) @@ -1041,7 +1047,7 @@ lemma transferCaps_corres: corres ((=) \ message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb - and valid_list + and valid_list and valid_arch_state and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame recv_buf and (\s. valid_message_info info) @@ -1414,10 +1420,14 @@ lemma copyMRs_valid_mdb[wp]: "\valid_mdb'\ copyMRs t buf t' buf' n \\rv. valid_mdb'\" by (simp add: valid_mdb'_def copyMRs_ctes_of) +crunch copy_mrs + for valid_arch_state[wp]: valid_arch_state + (wp: crunch_wps) + lemma doNormalTransfer_corres: "corres dc (tcb_at sender and tcb_at receiver and (pspace_aligned:: det_state \ bool) - and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct + and valid_objs and cur_tcb and valid_mdb and valid_list and valid_arch_state and pspace_distinct and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame send_buf and case_option \ in_user_frame recv_buf) @@ -1696,7 +1706,7 @@ lemma lookupIPCBuffer_valid_ipc_buffer [wp]: lemma doIPCTransfer_corres: "corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned - and valid_list + and valid_list and valid_arch_state and pspace_distinct and valid_mdb and cur_tcb and (\s. case ep of Some x \ ep_at x s | _ \ True)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' @@ -1704,9 +1714,9 @@ lemma doIPCTransfer_corres: (do_ipc_transfer s ep bg grt r) (doIPCTransfer s ep bg grt r)" apply (simp add: do_ipc_transfer_def doIPCTransfer_def) - apply (rule_tac Q="%receiveBuffer sa. tcb_at s sa \ valid_objs sa \ - pspace_aligned sa \ tcb_at r sa \ - cur_tcb sa \ valid_mdb sa \ valid_list sa \ pspace_distinct sa \ + apply (rule_tac Q="\receiveBuffer sa. tcb_at s sa \ valid_objs sa \ + pspace_aligned sa \ pspace_distinct sa \ tcb_at r sa \ + cur_tcb sa \ valid_mdb sa \ valid_list sa \ valid_arch_state sa \ (case ep of None \ True | Some x \ ep_at x sa) \ case_option (\_. True) in_user_frame receiveBuffer sa \ obj_at (\ko. \tcb. ko = TCB tcb @@ -2282,7 +2292,7 @@ lemma setupCallerCap_corres: (st_tcb_at (Not \ halted) sender and tcb_at receiver and st_tcb_at (Not \ awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb - and valid_list and + and valid_list and valid_arch_state and valid_reply_masters and cte_wp_at (\c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) @@ -2501,6 +2511,7 @@ proof - valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct valid_sched_valid_queues)+ apply ((wp hoare_drop_imps do_ipc_transfer_tcb_caps weak_valid_sched_action_lift + do_ipc_transfer_valid_arch | clarsimp simp: is_cap_simps)+)[1] apply (simp add: pred_conj_def) apply (strengthen sch_act_wf_weak) @@ -3216,7 +3227,7 @@ lemma receiveIPC_corres: apply (rule corres_split[OF doIPCTransfer_corres]) apply (simp split del: if_split cong: if_cong) apply (fold dc_def)[1] - apply (rule_tac P="valid_objs and valid_mdb and valid_list + apply (rule_tac P="valid_objs and valid_mdb and valid_list and valid_arch_state and valid_sched and cur_tcb and valid_reply_caps @@ -3246,7 +3257,7 @@ lemma receiveIPC_corres: apply (fastforce simp: st_tcb_at_tcb_at st_tcb_def2 valid_sched_def valid_sched_action_def) apply (clarsimp split: if_split_asm) - apply (clarsimp | wp do_ipc_transfer_tcb_caps)+ + apply (clarsimp | wp do_ipc_transfer_tcb_caps do_ipc_transfer_valid_arch)+ apply (rule_tac Q'="\_ s. sch_act_wf (ksSchedulerAction s) s \ sym_heap_sched_pointers s \ valid_sched_pointers s \ pspace_aligned' s \ pspace_distinct' s" @@ -3584,19 +3595,12 @@ lemma cteInsert_cap_to': "\ex_nonz_cap_to' p and cte_wp_at' (\c. cteCap c = NullCap) dest\ cteInsert cap src dest \\rv. ex_nonz_cap_to' p\" - apply (simp add: cteInsert_def ex_nonz_cap_to'_def - updateCap_def setUntypedCapAsFull_def - split del: if_split) - apply (rule hoare_pre, rule hoare_vcg_ex_lift) - apply (wp updateMDB_weak_cte_wp_at - setCTE_weak_cte_wp_at - | simp - | rule hoare_drop_imps)+ - apply (wp getCTE_wp) - apply clarsimp + apply (simp add: cteInsert_def ex_nonz_cap_to'_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: updateMDB_weak_cte_wp_at setCTE_weak_cte_wp_at hoare_vcg_ex_lift + | rule hoare_drop_imps + | wp getCTE_wp)+ (* getCTE_wp is separate to apply it only to the last one *) apply (rule_tac x=cref in exI) - apply (rule conjI) - apply (clarsimp simp: cte_wp_at_ctes_of)+ + apply (fastforce simp: cte_wp_at_ctes_of) done crunch setExtraBadge diff --git a/proof/refine/AARCH64/Tcb_R.thy b/proof/refine/AARCH64/Tcb_R.thy index 9e7b2892ad..6dc628c412 100644 --- a/proof/refine/AARCH64/Tcb_R.thy +++ b/proof/refine/AARCH64/Tcb_R.thy @@ -851,7 +851,7 @@ lemma checkCapAt_cteInsert_corres: apply clarsimp apply (rule conjI, fastforce)+ apply (cases src_slot) - apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: cte_wp_at_caps_of_state invs_arch_state) apply (rule conjI) apply (frule same_object_as_cap_master) apply (clarsimp simp: cap_master_cap_simps is_cnode_or_valid_arch_def diff --git a/proof/refine/ARM/ArchInvsDefs_H.thy b/proof/refine/ARM/ArchInvsDefs_H.thy index e6a572539a..3d6307213b 100644 --- a/proof/refine/ARM/ArchInvsDefs_H.thy +++ b/proof/refine/ARM/ArchInvsDefs_H.thy @@ -168,9 +168,6 @@ abbreviation (input) lemmas isArchPageCap_def = isArchFrameCap_def -definition valid_arch_mdb_ctes :: "cte_heap \ bool" where - "valid_arch_mdb_ctes \ \" - definition page_directory_refs' :: "word32 \ word32 set" where "page_directory_refs' x \ (\y. x + (y << 2)) ` {y. y < 2 ^ 12}" diff --git a/proof/refine/ARM/Arch_R.thy b/proof/refine/ARM/Arch_R.thy index 825a297896..4939f7cc10 100644 --- a/proof/refine/ARM/Arch_R.thy +++ b/proof/refine/ARM/Arch_R.thy @@ -137,6 +137,7 @@ lemma performASIDControlInvocation_corres: apply (cases i) apply (rename_tac word1 prod1 prod2 word2) apply (clarsimp simp: asid_ci_map_def) + apply (rename_tac p slot p' slot' word2) apply (simp add: perform_asid_control_invocation_def placeNewObject_def2 performASIDControlInvocation_def) apply (rule corres_name_pre) @@ -194,7 +195,7 @@ lemma performASIDControlInvocation_corres: apply wp+ apply (strengthen safe_parent_strg[where idx = "2^pageBits"]) apply (strengthen invs_valid_objs invs_distinct - invs_psp_aligned invs_mdb + invs_psp_aligned invs_mdb invs_arch_state | simp cong:conj_cong)+ apply (wp retype_region_plain_invs[where sz = pageBits] retype_cte_wp_at[where sz = pageBits])+ @@ -277,7 +278,7 @@ lemma performASIDControlInvocation_corres: apply (drule detype_locale.non_null_present) apply (fastforce simp:cte_wp_at_caps_of_state) apply simp - apply (frule_tac ptr = "(aa,ba)" in detype_invariants [rotated 3]) + apply (frule_tac ptr = "(p', slot')" in detype_invariants [rotated 3]) apply fastforce apply simp apply (simp add: cte_wp_at_caps_of_state) @@ -304,7 +305,7 @@ lemma performASIDControlInvocation_corres: apply (simp add:empty_descendants_range_in)+ apply (rule conjI) apply clarsimp - apply (drule_tac p = "(aa,ba)" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) + apply (drule_tac p = "(p', slot')" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) apply fastforce apply (clarsimp simp: region_in_kernel_window_def valid_cap_def cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def) @@ -314,7 +315,7 @@ lemma performASIDControlInvocation_corres: apply (clarsimp simp: detype_def clear_um_def detype_ext_def valid_sched_def valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def) apply (simp add: detype_def clear_um_def) - apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (drule_tac x = "cte_map (p', slot')" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) apply (simp add:invs_valid_objs)+ apply clarsimp apply (drule cte_map_inj_eq) diff --git a/proof/refine/ARM/CNodeInv_R.thy b/proof/refine/ARM/CNodeInv_R.thy index b4456a969b..a891af069e 100644 --- a/proof/refine/ARM/CNodeInv_R.thy +++ b/proof/refine/ARM/CNodeInv_R.thy @@ -8371,9 +8371,6 @@ proof apply (erule (1) irq_controlD, rule irq_control) done - show "valid_arch_mdb_ctes m'" - by simp - have distz: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def) diff --git a/proof/refine/ARM/CSpace1_R.thy b/proof/refine/ARM/CSpace1_R.thy index ca93a5334e..7b50f6cf0f 100644 --- a/proof/refine/ARM/CSpace1_R.thy +++ b/proof/refine/ARM/CSpace1_R.thy @@ -14,6 +14,20 @@ imports "AInvs.ArchDetSchedSchedule_AI" begin +context Arch begin arch_global_naming + +(* No assertion necessary for this architecture. *) +definition arch_mdb_assert :: "cte_heap \ bool" where + "arch_mdb_assert m \ True" + +end + +arch_requalify_consts + arch_mdb_assert + +defs archMDBAssertions_def: + "archMDBAssertions s \ arch_mdb_assert (ctes_of s)" + context Arch begin global_naming ARM_A (*FIXME: arch-split*) lemmas final_matters_def = final_matters_def[simplified final_matters_arch_def] @@ -250,7 +264,7 @@ lemma pspace_relation_cte_wp_at: lemma pspace_relation_ctes_ofI: "\ pspace_relation (kheap s) (ksPSpace s'); - cte_wp_at ((=) c) slot s; pspace_aligned' s'; + cte_wp_at ((=) c) slot s; pspace_aligned' s'; pspace_distinct' s' \ \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" apply (cases slot, clarsimp) @@ -258,6 +272,22 @@ lemma pspace_relation_ctes_ofI: apply (simp add: cte_wp_at_ctes_of) done +lemma pspace_relation_caps_of_state_cross: + "\ pspace_relation (kheap s) (ksPSpace s'); + caps_of_state s slot = Some c; pspace_aligned s; pspace_distinct s \ + \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" + for s' :: kernel_state + by (auto simp: cte_wp_at_caps_of_state + intro!: pspace_relation_ctes_ofI pspace_aligned_cross pspace_distinct_cross) + +lemma caps_of_state_cross: + "\ caps_of_state s slot = Some cap; pspace_aligned s; pspace_distinct s; (s,s') \ state_relation \ + \ \cap'. cteCaps_of s' (cte_map slot) = Some cap' \ cap_relation cap cap'" + apply (erule state_relationE) + apply (drule (3) pspace_relation_caps_of_state_cross) + apply (fastforce simp: cteCaps_of_def) + done + lemma get_cap_corres_P: "corres (\x y. cap_relation x (cteCap y) \ P x) (cte_wp_at P cslot_ptr) @@ -890,21 +920,13 @@ lemma ctes_of_valid_cap'': done lemma cap_insert_objs' [wp]: - "\valid_objs' - and valid_cap' cap\ - cteInsert cap src dest \\rv. valid_objs'\" - including no_pre - apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: if_split) - apply (wp setCTE_valid_objs) - apply simp - apply wp+ - apply (clarsimp simp: updateCap_def) - apply (wp|simp)+ - apply (rule hoare_drop_imp)+ - apply wp+ - apply (rule hoare_strengthen_post[OF getCTE_sp]) + "\valid_objs' and valid_cap' cap\ + cteInsert cap src dest + \\_. valid_objs'\" + apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: setCTE_valid_objs | wp getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps - dest!: ctes_of_valid_cap'') + dest!: ctes_of_valid_cap'') done lemma cteInsert_weak_cte_wp_at: @@ -1930,6 +1952,14 @@ lemma pspace_relation_cte_wp_atI: apply assumption done +lemma caps_of_state_rev_cross: + "\ ctes_of s' p = Some cte; valid_objs s; (s,s') \ state_relation \ + \ \cap slot. caps_of_state s slot = Some cap \ p = cte_map slot \ cap_relation cap (cteCap cte)" + apply (erule state_relationE) + apply (drule (2) pspace_relation_cte_wp_atI) + apply (fastforce simp: cte_wp_at_caps_of_state) + done + lemma sameRegion_corres: "\ sameRegionAs c' d'; cap_relation c c'; cap_relation d d' \ \ same_region_as c d" @@ -5064,6 +5094,15 @@ lemma cte_map_inj_eq': done context begin interpretation Arch . (*FIXME: arch-split*) + +(* interface lemma: generic statement, arch-specific proof *) +lemma archMDBAssertions_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_arch_state s; valid_objs s; + (s, s') \ state_relation \ + \ archMDBAssertions s'" + unfolding archMDBAssertions_def + by (simp add: arch_mdb_assert_def) + lemma cteInsert_corres: notes split_paired_All[simp del] split_paired_Ex[simp del] trans_state_update'[symmetric,simp] @@ -5072,30 +5111,33 @@ lemma cteInsert_corres: (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=Structures_A.NullCap) dest and - (\s. cte_wp_at (is_derived (cdt s) src c) src s)) + (\s. cte_wp_at (is_derived (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and cte_wp_at' (\c. cteCap c=NullCap) dest') (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _) _ _") using assms unfolding cap_insert_def cteInsert_def apply simp + (* this lemma doesn't use the assertion, but does need to establish it *) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (is_derived (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src)" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -5104,7 +5146,7 @@ lemma cteInsert_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. (is_derived (cdt s) src c) src_cap) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) and + R'="\r. ?P' and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src)" in corres_split[where r'=dc]) @@ -5168,7 +5210,7 @@ lemma cteInsert_corres: apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") @@ -5455,7 +5497,7 @@ lemma cteInsert_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply simp apply (rule revokable_eq, assumption, assumption) @@ -5468,7 +5510,7 @@ lemma cteInsert_corres: split:if_splits dest!:cap_master_cap_eqDs) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5494,7 +5536,7 @@ lemma cteInsert_corres: apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) @@ -5504,7 +5546,7 @@ lemma cteInsert_corres: apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") diff --git a/proof/refine/ARM/CSpace_R.thy b/proof/refine/ARM/CSpace_R.thy index 736bb403b8..41f5065f63 100644 --- a/proof/refine/ARM/CSpace_R.thy +++ b/proof/refine/ARM/CSpace_R.thy @@ -4531,6 +4531,7 @@ end locale mdb_insert_simple = mdb_insert + assumes safe_parent: "safe_parent_for' m src c'" assumes simple: "is_simple_cap' c'" + assumes arch_mdb_assert: "arch_mdb_assert m" begin interpretation Arch . (*FIXME: arch-split*) lemma dest_no_parent_n: @@ -4723,6 +4724,13 @@ lemma maskedAsFull_revokable_safe_parent: done context begin interpretation Arch . (*FIXME: arch-split*) + +(* FIXME arch-split: generic statement, arch specific proof *) +lemma setUntypedCapAsFull_archMDBAssertions[wp]: + "setUntypedCapAsFull src_cap cap p \archMDBAssertions\" + unfolding archMDBAssertions_def arch_mdb_assert_def + by wp + lemma cteInsert_simple_corres: assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest" notes trans_state_update'[symmetric,simp] @@ -4731,34 +4739,36 @@ lemma cteInsert_simple_corres: valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=cap.NullCap) dest and K (is_simple_cap c) and - (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s)) + (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and K (is_simple_cap' c') and cte_wp_at' (\c. cteCap c=NullCap) dest' and (\s. safe_parent_for' (ctes_of s) src' c')) (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _ and _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _ and _) _ _") using assms unfolding cap_insert_def cteInsert_def supply subst_all [simp del] apply simp + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and - Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + Q="?P' and archMDBAssertions and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -4767,7 +4777,7 @@ lemma cteInsert_simple_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) + R'="\r. ?P' and archMDBAssertions and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_split[where r'=dc]) @@ -4860,7 +4870,7 @@ lemma cteInsert_simple_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) apply (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply clarsimp apply (rule revokable_eq, assumption, assumption) @@ -4873,7 +4883,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -4898,14 +4908,14 @@ lemma cteInsert_simple_corres: setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") @@ -4929,7 +4939,8 @@ lemma cteInsert_simple_corres: apply (simp (no_asm_simp) add: cdt_relation_def split: if_split) apply (intro impI allI) apply (frule mdb_insert_simple_axioms.intro) - apply(clarsimp simp:cte_wp_at_ctes_of) + apply(clarsimp simp:cte_wp_at_ctes_of) + apply (simp add: archMDBAssertions_def) apply (drule (1) mdb_insert_simple.intro) apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable_safe_parent[symmetric]) apply simp+ @@ -5813,7 +5824,7 @@ lemma cteInsert_simple_mdb': mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ - apply ((clarsimp simp:valid_mdb_ctes_def)+) + apply (clarsimp simp:valid_mdb_ctes_def archMDBAssertions_def)+ apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) done diff --git a/proof/refine/ARM/Interrupt_R.thy b/proof/refine/ARM/Interrupt_R.thy index c4ab7d5eae..5f6460f598 100644 --- a/proof/refine/ARM/Interrupt_R.thy +++ b/proof/refine/ARM/Interrupt_R.thy @@ -489,6 +489,9 @@ lemma setIRQTrigger_corres: | simp add: dc_def)+ done +crunch set_irq_state + for valid_arch_state[wp]: valid_arch_state + lemma arch_performIRQControl_corres: "arch_irq_control_inv_relation x2 ivk' \ corres (dc \ dc) (einvs and arch_irq_control_inv_valid x2) diff --git a/proof/refine/ARM/InvariantUpdates_H.thy b/proof/refine/ARM/InvariantUpdates_H.thy index bd0cc3d0c8..96e3b1f4da 100644 --- a/proof/refine/ARM/InvariantUpdates_H.thy +++ b/proof/refine/ARM/InvariantUpdates_H.thy @@ -483,10 +483,4 @@ lemma invs'_update_cnt[elim!]: by (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def cur_tcb'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def bitmapQ_defs) -(* FIXME arch-split: valid_arch_mdb_ctes only exists to contain ioport_control on x64, and it is not - yet clear what the best way to arch-split it is, or whether it can be crossed from AInvs. - Therefore, for now, export the truth that it doesn't do anything on this arch beyond this point *) -arch_requalify_facts valid_arch_mdb_ctes_def -lemmas [simp] = valid_arch_mdb_ctes_def - end diff --git a/proof/refine/ARM/Ipc_R.thy b/proof/refine/ARM/Ipc_R.thy index 329096a33b..cc188baeaa 100644 --- a/proof/refine/ARM/Ipc_R.thy +++ b/proof/refine/ARM/Ipc_R.thy @@ -377,6 +377,10 @@ lemma cte_refs'_maskedAsFull[simp]: apply (clarsimp simp:maskedAsFull_def isCap_simps)+ done +lemma set_extra_badge_valid_arch_state[wp]: + "set_extra_badge buffer badge n \ valid_arch_state \" + unfolding set_extra_badge_def + by wp lemma transferCapsToSlots_corres: "\ list_all2 (\(cap, slot) (cap', slot'). cap_relation cap cap' @@ -384,7 +388,7 @@ lemma transferCapsToSlots_corres: mi' = message_info_map mi \ \ corres ((=) \ message_info_map) (\s. valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_mdb s - \ valid_list s + \ valid_list s \ valid_arch_state s \ (case ep of Some x \ ep_at x s | _ \ True) \ (\x \ set slots. cte_wp_at (\cap. cap = cap.NullCap) x s \ real_cte_at x s) @@ -458,7 +462,8 @@ next apply (simp add: tl_map) apply (rule corres_rel_imp, rule Cons.hyps, simp_all)[1] apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift - hoare_vcg_const_Ball_lift cap_insert_weak_cte_wp_at) + hoare_vcg_const_Ball_lift cap_insert_derived_valid_arch_state + cap_insert_weak_cte_wp_at) apply (wp hoare_vcg_const_Ball_lift | simp add:split_def del: imp_disj1)+ apply (wp cap_insert_cte_wp_at) apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift @@ -599,6 +604,7 @@ lemma cteInsert_assume_Null: apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cteInsert_def) + apply (rule bind_wp[OF _ stateAssert_sp]) apply (rule bind_wp[OF _ getCTE_sp])+ apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) @@ -1034,7 +1040,7 @@ lemma transferCaps_corres: corres ((=) \ message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb - and valid_list + and valid_list and valid_arch_state and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame recv_buf and (\s. valid_message_info info) @@ -1395,10 +1401,14 @@ lemma copyMRs_valid_mdb[wp]: "\valid_mdb'\ copyMRs t buf t' buf' n \\rv. valid_mdb'\" by (simp add: valid_mdb'_def copyMRs_ctes_of) +crunch copy_mrs + for valid_arch_state[wp]: valid_arch_state + (wp: crunch_wps) + lemma doNormalTransfer_corres: "corres dc (tcb_at sender and tcb_at receiver and (pspace_aligned:: det_state \ bool) - and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct + and valid_objs and cur_tcb and valid_mdb and valid_list and valid_arch_state and pspace_distinct and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame send_buf and case_option \ in_user_frame recv_buf) @@ -1670,7 +1680,7 @@ lemma lookupIPCBuffer_valid_ipc_buffer [wp]: lemma doIPCTransfer_corres: "corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned - and valid_list + and valid_list and valid_arch_state and pspace_distinct and valid_mdb and cur_tcb and (\s. case ep of Some x \ ep_at x s | _ \ True)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' @@ -1678,9 +1688,9 @@ lemma doIPCTransfer_corres: (do_ipc_transfer s ep bg grt r) (doIPCTransfer s ep bg grt r)" apply (simp add: do_ipc_transfer_def doIPCTransfer_def) - apply (rule_tac Q="%receiveBuffer sa. tcb_at s sa \ valid_objs sa \ - pspace_aligned sa \ tcb_at r sa \ - cur_tcb sa \ valid_mdb sa \ valid_list sa \ pspace_distinct sa \ + apply (rule_tac Q="\receiveBuffer sa. tcb_at s sa \ valid_objs sa \ + pspace_aligned sa \ pspace_distinct sa \ tcb_at r sa \ + cur_tcb sa \ valid_mdb sa \ valid_list sa \ valid_arch_state sa \ (case ep of None \ True | Some x \ ep_at x sa) \ case_option (\_. True) in_user_frame receiveBuffer sa \ obj_at (\ko. \tcb. ko = TCB tcb @@ -2255,7 +2265,7 @@ lemma setupCallerCap_corres: (st_tcb_at (Not \ halted) sender and tcb_at receiver and st_tcb_at (Not \ awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb - and valid_list and + and valid_list and valid_arch_state and valid_reply_masters and cte_wp_at (\c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) @@ -2469,6 +2479,7 @@ proof - valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct valid_sched_valid_queues)+ apply ((wp hoare_drop_imps do_ipc_transfer_tcb_caps weak_valid_sched_action_lift + do_ipc_transfer_valid_arch | clarsimp simp: is_cap_simps)+)[1] apply (simp add: pred_conj_def) apply (strengthen sch_act_wf_weak) @@ -3191,7 +3202,7 @@ lemma receiveIPC_corres: apply (rule corres_split[OF doIPCTransfer_corres]) apply (simp split del: if_split cong: if_cong) apply (fold dc_def)[1] - apply (rule_tac P="valid_objs and valid_mdb and valid_list + apply (rule_tac P="valid_objs and valid_mdb and valid_list and valid_arch_state and valid_sched and cur_tcb and valid_reply_caps @@ -3221,7 +3232,7 @@ lemma receiveIPC_corres: apply (fastforce simp: st_tcb_at_tcb_at st_tcb_def2 valid_sched_def valid_sched_action_def) apply (clarsimp split: if_split_asm) - apply (clarsimp | wp do_ipc_transfer_tcb_caps)+ + apply (clarsimp | wp do_ipc_transfer_tcb_caps do_ipc_transfer_valid_arch)+ apply (rule_tac Q'="\_ s. sch_act_wf (ksSchedulerAction s) s \ sym_heap_sched_pointers s \ valid_sched_pointers s \ pspace_aligned' s \ pspace_distinct' s" @@ -3563,19 +3574,12 @@ lemma cteInsert_cap_to': "\ex_nonz_cap_to' p and cte_wp_at' (\c. cteCap c = NullCap) dest\ cteInsert cap src dest \\rv. ex_nonz_cap_to' p\" - apply (simp add: cteInsert_def ex_nonz_cap_to'_def - updateCap_def setUntypedCapAsFull_def - split del: if_split) - apply (rule hoare_pre, rule hoare_vcg_ex_lift) - apply (wp updateMDB_weak_cte_wp_at - setCTE_weak_cte_wp_at - | simp - | rule hoare_drop_imps)+ - apply (wp getCTE_wp) - apply clarsimp + apply (simp add: cteInsert_def ex_nonz_cap_to'_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: updateMDB_weak_cte_wp_at setCTE_weak_cte_wp_at hoare_vcg_ex_lift + | rule hoare_drop_imps + | wp getCTE_wp)+ (* getCTE_wp is separate to apply it only to the last one *) apply (rule_tac x=cref in exI) - apply (rule conjI) - apply (clarsimp simp: cte_wp_at_ctes_of)+ + apply (fastforce simp: cte_wp_at_ctes_of) done crunch setExtraBadge diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy index d43abb7fad..3aa6eed474 100644 --- a/proof/refine/ARM/Tcb_R.thy +++ b/proof/refine/ARM/Tcb_R.thy @@ -869,7 +869,7 @@ lemma checkCapAt_cteInsert_corres: apply clarsimp apply (rule conjI, fastforce)+ apply (cases src_slot) - apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: cte_wp_at_caps_of_state invs_arch_state) apply (rule conjI) apply (frule same_object_as_cap_master) apply (clarsimp simp: cap_master_cap_simps is_cnode_or_valid_arch_def diff --git a/proof/refine/ARM_HYP/ArchInvsDefs_H.thy b/proof/refine/ARM_HYP/ArchInvsDefs_H.thy index e51e4f91bd..2d042df68a 100644 --- a/proof/refine/ARM_HYP/ArchInvsDefs_H.thy +++ b/proof/refine/ARM_HYP/ArchInvsDefs_H.thy @@ -206,9 +206,6 @@ abbreviation (input) lemmas isArchPageCap_def = isArchFrameCap_def -definition valid_arch_mdb_ctes :: "cte_heap \ bool" where - "valid_arch_mdb_ctes \ \" - definition page_directory_refs' :: "word32 \ word32 set" where "page_directory_refs' x \ (\y. x + (y << 3)) ` {y. y < 2 ^ 11}" diff --git a/proof/refine/ARM_HYP/Arch_R.thy b/proof/refine/ARM_HYP/Arch_R.thy index 57e588ebc8..77304f6673 100644 --- a/proof/refine/ARM_HYP/Arch_R.thy +++ b/proof/refine/ARM_HYP/Arch_R.thy @@ -137,6 +137,7 @@ lemma performASIDControlInvocation_corres: apply (cases i) apply (rename_tac word1 prod1 prod2 word2) apply (clarsimp simp: asid_ci_map_def) + apply (rename_tac p slot p' slot' word2) apply (simp add: perform_asid_control_invocation_def placeNewObject_def2 performASIDControlInvocation_def) apply (rule corres_name_pre) @@ -194,7 +195,7 @@ lemma performASIDControlInvocation_corres: apply wp+ apply (strengthen safe_parent_strg[where idx = "2^pageBits"]) apply (strengthen invs_valid_objs invs_distinct - invs_psp_aligned invs_mdb + invs_psp_aligned invs_mdb invs_arch_state | simp cong:conj_cong)+ apply (wp retype_region_plain_invs[where sz = pageBits] retype_cte_wp_at[where sz = pageBits])+ @@ -278,7 +279,7 @@ lemma performASIDControlInvocation_corres: apply (drule detype_locale.non_null_present) apply (fastforce simp:cte_wp_at_caps_of_state) apply simp - apply (frule_tac ptr = "(aa,ba)" in detype_invariants [rotated 3]) + apply (frule_tac ptr = "(p', slot')" in detype_invariants [rotated 3]) apply fastforce apply simp apply (simp add: cte_wp_at_caps_of_state) @@ -305,7 +306,7 @@ lemma performASIDControlInvocation_corres: apply (simp add:empty_descendants_range_in)+ apply (rule conjI) apply clarsimp - apply (drule_tac p = "(aa,ba)" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) + apply (drule_tac p = "(p', slot')" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) apply fastforce apply (clarsimp simp: region_in_kernel_window_def valid_cap_def cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def) @@ -315,7 +316,7 @@ lemma performASIDControlInvocation_corres: apply (clarsimp simp: detype_def clear_um_def detype_ext_def valid_sched_def valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def) apply (simp add: detype_def clear_um_def) - apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (drule_tac x = "cte_map (p', slot')" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) apply (simp add:invs_valid_objs)+ apply clarsimp apply (drule cte_map_inj_eq) diff --git a/proof/refine/ARM_HYP/CNodeInv_R.thy b/proof/refine/ARM_HYP/CNodeInv_R.thy index 43e571cf7a..5c4221469b 100644 --- a/proof/refine/ARM_HYP/CNodeInv_R.thy +++ b/proof/refine/ARM_HYP/CNodeInv_R.thy @@ -8466,9 +8466,6 @@ proof apply (erule (1) irq_controlD, rule irq_control) done - show "valid_arch_mdb_ctes m'" - by simp - have distz: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def) diff --git a/proof/refine/ARM_HYP/CSpace1_R.thy b/proof/refine/ARM_HYP/CSpace1_R.thy index fefddf70c1..7add6866a8 100644 --- a/proof/refine/ARM_HYP/CSpace1_R.thy +++ b/proof/refine/ARM_HYP/CSpace1_R.thy @@ -14,6 +14,20 @@ imports "AInvs.ArchDetSchedSchedule_AI" begin +context Arch begin arch_global_naming + +(* No assertion necessary for this architecture. *) +definition arch_mdb_assert :: "cte_heap \ bool" where + "arch_mdb_assert m \ True" + +end + +arch_requalify_consts + arch_mdb_assert + +defs archMDBAssertions_def: + "archMDBAssertions s \ arch_mdb_assert (ctes_of s)" + context Arch begin global_naming ARM_HYP_A (*FIXME: arch-split*) lemmas final_matters_def = final_matters_def[simplified final_matters_arch_def] @@ -250,7 +264,7 @@ lemma pspace_relation_cte_wp_at: lemma pspace_relation_ctes_ofI: "\ pspace_relation (kheap s) (ksPSpace s'); - cte_wp_at ((=) c) slot s; pspace_aligned' s'; + cte_wp_at ((=) c) slot s; pspace_aligned' s'; pspace_distinct' s' \ \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" apply (cases slot, clarsimp) @@ -258,6 +272,22 @@ lemma pspace_relation_ctes_ofI: apply (simp add: cte_wp_at_ctes_of) done +lemma pspace_relation_caps_of_state_cross: + "\ pspace_relation (kheap s) (ksPSpace s'); + caps_of_state s slot = Some c; pspace_aligned s; pspace_distinct s \ + \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" + for s' :: kernel_state + by (auto simp: cte_wp_at_caps_of_state + intro!: pspace_relation_ctes_ofI pspace_aligned_cross pspace_distinct_cross) + +lemma caps_of_state_cross: + "\ caps_of_state s slot = Some cap; pspace_aligned s; pspace_distinct s; (s,s') \ state_relation \ + \ \cap'. cteCaps_of s' (cte_map slot) = Some cap' \ cap_relation cap cap'" + apply (erule state_relationE) + apply (drule (3) pspace_relation_caps_of_state_cross) + apply (fastforce simp: cteCaps_of_def) + done + lemma get_cap_corres_P: "corres (\x y. cap_relation x (cteCap y) \ P x) (cte_wp_at P cslot_ptr) @@ -907,21 +937,13 @@ lemma ctes_of_valid_cap'': done lemma cap_insert_objs' [wp]: - "\valid_objs' - and valid_cap' cap\ - cteInsert cap src dest \\rv. valid_objs'\" - including no_pre - apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: if_split) - apply (wp setCTE_valid_objs) - apply simp - apply wp+ - apply (clarsimp simp: updateCap_def) - apply (wp|simp)+ - apply (rule hoare_drop_imp)+ - apply wp+ - apply (rule hoare_strengthen_post[OF getCTE_sp]) + "\valid_objs' and valid_cap' cap\ + cteInsert cap src dest + \\_. valid_objs'\" + apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: setCTE_valid_objs | wp getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps - dest!: ctes_of_valid_cap'') + dest!: ctes_of_valid_cap'') done lemma cteInsert_weak_cte_wp_at: @@ -1970,6 +1992,14 @@ lemma pspace_relation_cte_wp_atI: apply assumption done +lemma caps_of_state_rev_cross: + "\ ctes_of s' p = Some cte; valid_objs s; (s,s') \ state_relation \ + \ \cap slot. caps_of_state s slot = Some cap \ p = cte_map slot \ cap_relation cap (cteCap cte)" + apply (erule state_relationE) + apply (drule (2) pspace_relation_cte_wp_atI) + apply (fastforce simp: cte_wp_at_caps_of_state) + done + lemma sameRegion_corres: "\ sameRegionAs c' d'; cap_relation c c'; cap_relation d d' \ \ same_region_as c d" @@ -5229,6 +5259,15 @@ lemma cte_map_inj_eq': done context begin interpretation Arch . (*FIXME: arch-split*) + +(* interface lemma: generic statement, arch-specific proof *) +lemma archMDBAssertions_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_arch_state s; valid_objs s; + (s, s') \ state_relation \ + \ archMDBAssertions s'" + unfolding archMDBAssertions_def + by (simp add: arch_mdb_assert_def) + lemma cteInsert_corres: notes split_paired_All[simp del] split_paired_Ex[simp del] trans_state_update'[symmetric,simp] @@ -5237,30 +5276,33 @@ lemma cteInsert_corres: (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=Structures_A.NullCap) dest and - (\s. cte_wp_at (is_derived (cdt s) src c) src s)) + (\s. cte_wp_at (is_derived (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and cte_wp_at' (\c. cteCap c=NullCap) dest') (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _) _ _") using assms unfolding cap_insert_def cteInsert_def apply simp + (* this lemma doesn't use the assertion, but does need to establish it *) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (is_derived (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src)" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -5269,7 +5311,7 @@ lemma cteInsert_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. (is_derived (cdt s) src c) src_cap) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) and + R'="\r. ?P' and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src)" in corres_split[where r'=dc]) @@ -5353,7 +5395,7 @@ lemma cteInsert_corres: apply(rule conjI) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") @@ -5640,7 +5682,7 @@ lemma cteInsert_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply simp apply (rule revokable_eq, assumption, assumption) @@ -5653,7 +5695,7 @@ lemma cteInsert_corres: split:if_splits dest!:cap_master_cap_eqDs) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5680,14 +5722,14 @@ lemma cteInsert_corres: apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) apply (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") diff --git a/proof/refine/ARM_HYP/CSpace_R.thy b/proof/refine/ARM_HYP/CSpace_R.thy index b1af243a36..9854d4cfef 100644 --- a/proof/refine/ARM_HYP/CSpace_R.thy +++ b/proof/refine/ARM_HYP/CSpace_R.thy @@ -4582,6 +4582,7 @@ end locale mdb_insert_simple = mdb_insert + assumes safe_parent: "safe_parent_for' m src c'" assumes simple: "is_simple_cap' c'" + assumes arch_mdb_assert: "arch_mdb_assert m" begin interpretation Arch . (*FIXME: arch-split*) lemma dest_no_parent_n: @@ -4774,6 +4775,13 @@ lemma maskedAsFull_revokable_safe_parent: done context begin interpretation Arch . (*FIXME: arch-split*) + +(* FIXME arch-split: generic statement, arch specific proof *) +lemma setUntypedCapAsFull_archMDBAssertions[wp]: + "setUntypedCapAsFull src_cap cap p \archMDBAssertions\" + unfolding archMDBAssertions_def arch_mdb_assert_def + by wp + lemma cteInsert_simple_corres: assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest" notes trans_state_update'[symmetric,simp] @@ -4782,34 +4790,36 @@ lemma cteInsert_simple_corres: valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=cap.NullCap) dest and K (is_simple_cap c) and - (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s)) + (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and K (is_simple_cap' c') and cte_wp_at' (\c. cteCap c=NullCap) dest' and (\s. safe_parent_for' (ctes_of s) src' c')) (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _ and _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _ and _) _ _") using assms unfolding cap_insert_def cteInsert_def supply subst_all [simp del] apply simp + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and - Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + Q="?P' and archMDBAssertions and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -4818,7 +4828,7 @@ lemma cteInsert_simple_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) + R'="\r. ?P' and archMDBAssertions and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_split[where r'=dc]) @@ -4911,7 +4921,7 @@ lemma cteInsert_simple_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) apply (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply clarsimp apply (rule revokable_eq, assumption, assumption) @@ -4924,7 +4934,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -4949,14 +4959,14 @@ lemma cteInsert_simple_corres: setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") @@ -4980,7 +4990,8 @@ lemma cteInsert_simple_corres: apply (simp (no_asm_simp) add: cdt_relation_def split: if_split) apply (intro impI allI) apply (frule mdb_insert_simple_axioms.intro) - apply(clarsimp simp:cte_wp_at_ctes_of) + apply(clarsimp simp:cte_wp_at_ctes_of) + apply (simp add: archMDBAssertions_def) apply (drule (1) mdb_insert_simple.intro) apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable_safe_parent[symmetric]) apply simp+ @@ -5879,7 +5890,7 @@ lemma cteInsert_simple_mdb': mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ - apply ((clarsimp simp:valid_mdb_ctes_def)+) + apply (clarsimp simp:valid_mdb_ctes_def archMDBAssertions_def)+ apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) done diff --git a/proof/refine/ARM_HYP/Interrupt_R.thy b/proof/refine/ARM_HYP/Interrupt_R.thy index 3aa0268a7f..03c8ffb629 100644 --- a/proof/refine/ARM_HYP/Interrupt_R.thy +++ b/proof/refine/ARM_HYP/Interrupt_R.thy @@ -475,6 +475,9 @@ lemma setIRQTrigger_corres: | simp add: dc_def)+ done +crunch set_irq_state + for valid_arch_state[wp]: valid_arch_state + lemma arch_performIRQControl_corres: "arch_irq_control_inv_relation x2 ivk' \ corres (dc \ dc) (einvs and arch_irq_control_inv_valid x2) diff --git a/proof/refine/ARM_HYP/InvariantUpdates_H.thy b/proof/refine/ARM_HYP/InvariantUpdates_H.thy index 7edfa783a5..5ad53df77d 100644 --- a/proof/refine/ARM_HYP/InvariantUpdates_H.thy +++ b/proof/refine/ARM_HYP/InvariantUpdates_H.thy @@ -483,10 +483,4 @@ lemma invs'_update_cnt[elim!]: by (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def cur_tcb'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def bitmapQ_defs) -(* FIXME arch-split: valid_arch_mdb_ctes only exists to contain ioport_control on x64, and it is not - yet clear what the best way to arch-split it is, or whether it can be crossed from AInvs. - Therefore, for now, export the truth that it doesn't do anything on this arch beyond this point *) -arch_requalify_facts valid_arch_mdb_ctes_def -lemmas [simp] = valid_arch_mdb_ctes_def - end diff --git a/proof/refine/ARM_HYP/Ipc_R.thy b/proof/refine/ARM_HYP/Ipc_R.thy index 13d9da30da..c8914e1314 100644 --- a/proof/refine/ARM_HYP/Ipc_R.thy +++ b/proof/refine/ARM_HYP/Ipc_R.thy @@ -388,6 +388,10 @@ lemma cte_refs'_maskedAsFull[simp]: apply (clarsimp simp:maskedAsFull_def isCap_simps)+ done +lemma set_extra_badge_valid_arch_state[wp]: + "set_extra_badge buffer badge n \ valid_arch_state \" + unfolding set_extra_badge_def + by wp lemma transferCapsToSlots_corres: "\ list_all2 (\(cap, slot) (cap', slot'). cap_relation cap cap' @@ -395,7 +399,7 @@ lemma transferCapsToSlots_corres: mi' = message_info_map mi \ \ corres ((=) \ message_info_map) (\s. valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_mdb s - \ valid_list s + \ valid_list s \ valid_arch_state s \ (case ep of Some x \ ep_at x s | _ \ True) \ (\x \ set slots. cte_wp_at (\cap. cap = cap.NullCap) x s \ real_cte_at x s) @@ -469,7 +473,8 @@ next apply (simp add: tl_map) apply (rule corres_rel_imp, rule Cons.hyps, simp_all)[1] apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift - hoare_vcg_const_Ball_lift cap_insert_weak_cte_wp_at) + hoare_vcg_const_Ball_lift cap_insert_derived_valid_arch_state + cap_insert_weak_cte_wp_at) apply (wp hoare_vcg_const_Ball_lift | simp add:split_def del: imp_disj1)+ apply (wp cap_insert_cte_wp_at) apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift @@ -610,6 +615,7 @@ lemma cteInsert_assume_Null: apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cteInsert_def) + apply (rule bind_wp[OF _ stateAssert_sp]) apply (rule bind_wp[OF _ getCTE_sp])+ apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) @@ -1052,7 +1058,7 @@ lemma transferCaps_corres: corres ((=) \ message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb - and valid_list + and valid_list and valid_arch_state and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame recv_buf and (\s. valid_message_info info) @@ -1458,10 +1464,14 @@ lemma copyMRs_valid_mdb[wp]: "\valid_mdb'\ copyMRs t buf t' buf' n \\rv. valid_mdb'\" by (simp add: valid_mdb'_def copyMRs_ctes_of) +crunch copy_mrs + for valid_arch_state[wp]: valid_arch_state + (wp: crunch_wps) + lemma doNormalTransfer_corres: "corres dc (tcb_at sender and tcb_at receiver and (pspace_aligned:: det_state \ bool) - and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct + and valid_objs and cur_tcb and valid_mdb and valid_list and valid_arch_state and pspace_distinct and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame send_buf and case_option \ in_user_frame recv_buf) @@ -1768,7 +1778,7 @@ lemma lookupIPCBuffer_valid_ipc_buffer [wp]: lemma doIPCTransfer_corres: "corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned - and valid_list + and valid_list and valid_arch_state and pspace_distinct and valid_mdb and cur_tcb and (\s. case ep of Some x \ ep_at x s | _ \ True)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' @@ -1776,9 +1786,9 @@ lemma doIPCTransfer_corres: (do_ipc_transfer s ep bg grt r) (doIPCTransfer s ep bg grt r)" apply (simp add: do_ipc_transfer_def doIPCTransfer_def) - apply (rule_tac Q="%receiveBuffer sa. tcb_at s sa \ valid_objs sa \ - pspace_aligned sa \ tcb_at r sa \ - cur_tcb sa \ valid_mdb sa \ valid_list sa \ pspace_distinct sa \ + apply (rule_tac Q="\receiveBuffer sa. tcb_at s sa \ valid_objs sa \ + pspace_aligned sa \ pspace_distinct sa \ tcb_at r sa \ + cur_tcb sa \ valid_mdb sa \ valid_list sa \ valid_arch_state sa \ (case ep of None \ True | Some x \ ep_at x sa) \ case_option (\_. True) in_user_frame receiveBuffer sa \ obj_at (\ko. \tcb. ko = TCB tcb @@ -2386,7 +2396,7 @@ lemma setupCallerCap_corres: (st_tcb_at (Not \ halted) sender and tcb_at receiver and st_tcb_at (Not \ awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb - and valid_list and + and valid_list and valid_arch_state and valid_reply_masters and cte_wp_at (\c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) @@ -2603,6 +2613,7 @@ proof - valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct valid_sched_valid_queues)+ apply ((wp hoare_drop_imps do_ipc_transfer_tcb_caps weak_valid_sched_action_lift + do_ipc_transfer_valid_arch | clarsimp simp: is_cap_simps)+)[1] apply (simp add: pred_conj_def) apply (strengthen sch_act_wf_weak) @@ -3328,7 +3339,7 @@ lemma receiveIPC_corres: apply (rule corres_split[OF doIPCTransfer_corres]) apply (simp split del: if_split cong: if_cong) apply (fold dc_def)[1] - apply (rule_tac P="valid_objs and valid_mdb and valid_list + apply (rule_tac P="valid_objs and valid_mdb and valid_list and valid_arch_state and valid_sched and cur_tcb and valid_reply_caps @@ -3358,7 +3369,7 @@ lemma receiveIPC_corres: apply (fastforce simp: st_tcb_at_tcb_at st_tcb_def2 valid_sched_def valid_sched_action_def) apply (clarsimp split: if_split_asm) - apply (clarsimp | wp do_ipc_transfer_tcb_caps)+ + apply (clarsimp | wp do_ipc_transfer_tcb_caps do_ipc_transfer_valid_arch)+ apply (rule_tac Q'="\_ s. sch_act_wf (ksSchedulerAction s) s \ sym_heap_sched_pointers s \ valid_sched_pointers s \ pspace_aligned' s \ pspace_distinct' s" @@ -3713,19 +3724,12 @@ lemma cteInsert_cap_to': "\ex_nonz_cap_to' p and cte_wp_at' (\c. cteCap c = NullCap) dest\ cteInsert cap src dest \\rv. ex_nonz_cap_to' p\" - apply (simp add: cteInsert_def ex_nonz_cap_to'_def - updateCap_def setUntypedCapAsFull_def - split del: if_split) - apply (rule hoare_pre, rule hoare_vcg_ex_lift) - apply (wp updateMDB_weak_cte_wp_at - setCTE_weak_cte_wp_at - | simp - | rule hoare_drop_imps)+ - apply (wp getCTE_wp) - apply clarsimp + apply (simp add: cteInsert_def ex_nonz_cap_to'_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: updateMDB_weak_cte_wp_at setCTE_weak_cte_wp_at hoare_vcg_ex_lift + | rule hoare_drop_imps + | wp getCTE_wp)+ (* getCTE_wp is separate to apply it only to the last one *) apply (rule_tac x=cref in exI) - apply (rule conjI) - apply (clarsimp simp: cte_wp_at_ctes_of)+ + apply (fastforce simp: cte_wp_at_ctes_of) done crunch setExtraBadge diff --git a/proof/refine/ARM_HYP/Tcb_R.thy b/proof/refine/ARM_HYP/Tcb_R.thy index 849d926639..1fc409c811 100644 --- a/proof/refine/ARM_HYP/Tcb_R.thy +++ b/proof/refine/ARM_HYP/Tcb_R.thy @@ -875,7 +875,7 @@ lemma checkCapAt_cteInsert_corres: apply clarsimp apply (rule conjI, fastforce)+ apply (cases src_slot) - apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: cte_wp_at_caps_of_state invs_arch_state) apply (rule conjI) apply (frule same_object_as_cap_master) apply (clarsimp simp: cap_master_cap_simps is_cnode_or_valid_arch_def diff --git a/proof/refine/Invariants_H.thy b/proof/refine/Invariants_H.thy index 22d123c279..bbc83a7ed9 100644 --- a/proof/refine/Invariants_H.thy +++ b/proof/refine/Invariants_H.thy @@ -25,7 +25,6 @@ arch_requalify_consts global_refs' valid_arch_state' archMakeObjectT - valid_arch_mdb_ctes pspace_in_kernel_mappings' kernel_data_refs kernel_mappings @@ -412,8 +411,6 @@ where "valid_objs' s \ \obj \ ran (ksPSpace s). valid_obj' obj s" -type_synonym cte_heap = "machine_word \ cte option" - definition map_to_ctes :: "(machine_word \ kernel_object) \ cte_heap" where @@ -639,8 +636,7 @@ where mdb_chunked m \ untyped_mdb' m \ untyped_inc' m \ valid_nullcaps m \ ut_revocable' m \ class_links m \ distinct_zombies m - \ irq_control m \ reply_masters_rvk_fb m - \ valid_arch_mdb_ctes m" + \ irq_control m \ reply_masters_rvk_fb m" definition valid_mdb' :: "kernel_state \ bool" @@ -2214,7 +2210,7 @@ lemma valid_mdb_ctesI [intro]: caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; - reply_masters_rvk_fb m; valid_arch_mdb_ctes m \ + reply_masters_rvk_fb m \ \ valid_mdb_ctes m" unfolding valid_mdb_ctes_def by auto diff --git a/proof/refine/X64/ArchInvsDefs_H.thy b/proof/refine/X64/ArchInvsDefs_H.thy index 118cea10e8..dce0ce53a0 100644 --- a/proof/refine/X64/ArchInvsDefs_H.thy +++ b/proof/refine/X64/ArchInvsDefs_H.thy @@ -192,13 +192,6 @@ primrec acapClass :: "arch_capability \ capclass" where | "acapClass (IOPortCap x y) = IOPortClass" | "acapClass IOPortControlCap = IOPortClass" -(* IOPortControl caps are unique and always revocable *) -definition - "ioport_control m \ - \p n. m p = Some (CTE (ArchObjectCap IOPortControlCap) n) \ - mdbRevocable n \ - (\p' n'. m p' = Some (CTE (ArchObjectCap IOPortControlCap) n') \ p' = p)" - definition isArchFrameCap :: "capability \ bool" where @@ -215,11 +208,6 @@ definition where "isArchIOPortCap cap \ case cap of ArchObjectCap (IOPortCap f l) \ True | _ \ False" -definition valid_arch_mdb_ctes :: "cte_heap \ bool" where - "valid_arch_mdb_ctes \ ioport_control" - -lemmas [simp] = valid_arch_mdb_ctes_def - definition table_refs' :: "machine_word \ machine_word set" where "table_refs' x \ (\y. x + (y << word_size_bits)) ` {y. y < 2^ptTranslationBits}" diff --git a/proof/refine/X64/ArchInvsLemmas_H.thy b/proof/refine/X64/ArchInvsLemmas_H.thy index 11a32aab90..38ead17306 100644 --- a/proof/refine/X64/ArchInvsLemmas_H.thy +++ b/proof/refine/X64/ArchInvsLemmas_H.thy @@ -373,15 +373,6 @@ lemma page_map_l4_pml4e_atI': "\ page_map_l4_at' p s; x < 2^ptTranslationBits \ \ pml4e_at' (p + (x << word_size_bits)) s" by (simp add: page_map_l4_at'_def pageBits_def) -lemma ioport_controlD: - "\ m p = Some (CTE (ArchObjectCap IOPortControlCap) n); m p' = Some (CTE (ArchObjectCap IOPortControlCap) n'); - ioport_control m \ \ p' = p" - unfolding ioport_control_def by blast - -lemma ioport_revocable: - "\ m p = Some (CTE (ArchObjectCap IOPortControlCap) n); ioport_control m \ \ mdbRevocable n" - unfolding ioport_control_def by blast - lemma tcb_hyp_refs_of'_simps[simp]: "tcb_hyp_refs' atcb = {}" by (auto simp: tcb_hyp_refs'_def) diff --git a/proof/refine/X64/Arch_R.thy b/proof/refine/X64/Arch_R.thy index 7531980d00..a376268451 100644 --- a/proof/refine/X64/Arch_R.thy +++ b/proof/refine/X64/Arch_R.thy @@ -139,6 +139,7 @@ lemma performASIDControlInvocation_corres: apply (cases i) apply (rename_tac word1 prod1 prod2 word2) apply (clarsimp simp: asid_ci_map_def) + apply (rename_tac p slot p' slot' word2) apply (simp add: perform_asid_control_invocation_def placeNewObject_def2 performASIDControlInvocation_def) apply (rule corres_name_pre) @@ -197,7 +198,7 @@ lemma performASIDControlInvocation_corres: apply wp+ apply (strengthen safe_parent_strg[where idx = "2^pageBits"]) apply (strengthen invs_valid_objs invs_distinct - invs_psp_aligned invs_mdb + invs_psp_aligned invs_mdb invs_arch_state | simp cong:conj_cong)+ apply (wp retype_region_plain_invs[where sz = pageBits] retype_cte_wp_at[where sz = pageBits])+ @@ -269,9 +270,9 @@ lemma performASIDControlInvocation_corres: deleteObjects_null_filter[where p="makePoolParent i'"]) apply (clarsimp simp:invs_mdb max_free_index_def invs_untyped_children) apply (prop_tac "detype_locale x y sa" for x y) - apply (simp add: detype_locale_def) - apply (fastforce simp: cte_wp_at_caps_of_state descendants_range_def2 - empty_descendants_range_in invs_untyped_children) + apply (clarsimp simp: detype_locale_def cte_wp_at_caps_of_state) + apply (rule conjI, assumption, rule conjI, solves simp) (* force instantiation to Untyped cap *) + apply (fastforce simp: descendants_range_def2 empty_descendants_range_in invs_untyped_children) apply (intro conjI) apply (clarsimp) apply (erule(1) caps_of_state_valid) @@ -283,7 +284,7 @@ lemma performASIDControlInvocation_corres: apply (drule detype_locale.non_null_present) apply (fastforce simp:cte_wp_at_caps_of_state) apply simp - apply (frule_tac ptr = "(aa,ba)" in detype_invariants [rotated 3]) + apply (frule_tac ptr = "(p', slot')" in detype_invariants [rotated 3]) apply fastforce apply simp apply (simp add: cte_wp_at_caps_of_state) @@ -311,7 +312,7 @@ lemma performASIDControlInvocation_corres: apply (simp add:empty_descendants_range_in)+ apply (rule conjI) apply clarsimp - apply (drule_tac p = "(aa,ba)" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) + apply (drule_tac p = "(p', slot')" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) apply fastforce apply (clarsimp simp: region_in_kernel_window_def valid_cap_def cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def) @@ -321,7 +322,7 @@ lemma performASIDControlInvocation_corres: apply (clarsimp simp: detype_def clear_um_def detype_ext_def valid_sched_def valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def) apply (simp add: detype_def clear_um_def) - apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (drule_tac x = "cte_map (p', slot')" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) apply (simp add:invs_valid_objs)+ apply clarsimp apply (drule cte_map_inj_eq) @@ -1392,7 +1393,7 @@ lemma performX64PortInvocation_corres: apply wpsimp apply (clarsimp simp: is_simple_cap_def is_cap_simps) apply wpsimp - apply (strengthen invs_distinct[mk_strg] invs_psp_aligned_strg invs_strgs) + apply (strengthen invs_distinct[mk_strg] invs_psp_aligned_strg invs_strgs invs_arch_state) apply (wpsimp wp: set_ioport_mask_invs set_ioport_mask_safe_parent_for) apply (clarsimp simp: is_simple_cap'_def isCap_simps) apply wpsimp diff --git a/proof/refine/X64/CNodeInv_R.thy b/proof/refine/X64/CNodeInv_R.thy index 9a886cd6d9..4b8074e011 100644 --- a/proof/refine/X64/CNodeInv_R.thy +++ b/proof/refine/X64/CNodeInv_R.thy @@ -4781,55 +4781,6 @@ lemma irq_control_n: "irq_control n" apply clarsimp done -context begin interpretation Arch . (* FIXME arch-split *) - -lemma ioport_control_n: "ioport_control n" - using src dest dest_derived src_derived - apply (clarsimp simp: ioport_control_def) - apply (frule revokable) - apply (drule n_cap) - apply (clarsimp split: if_split_asm) - apply (clarsimp simp: weak_derived'_def) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule n_cap) - apply (split if_split_asm) - apply (thin_tac "capability.ArchObjectCap X64_H.IOPortControlCap = dcap") - apply clarsimp - apply (clarsimp split: if_split_asm) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (clarsimp simp: weak_derived'_def) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule n_cap) - apply (split if_split_asm) - apply clarsimp - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (split if_split_asm) - apply (thin_tac "capability.ArchObjectCap X64_H.IOPortControlCap = scap") - apply clarsimp - apply (clarsimp split: if_split_asm) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (clarsimp simp: weak_derived'_def) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule n_cap) - apply (clarsimp split: if_split_asm) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply clarsimp - done - -end - lemma distinct_zombies_m: "distinct_zombies m" using valid by auto @@ -4874,9 +4825,9 @@ lemma cteSwap_valid_mdb_helper: shows "valid_mdb_ctes n" using cteSwap_chain cteSwap_dlist_helper cteSwap_valid_badges cteSwap_chunked caps_contained untyped_mdb_n untyped_inc_n - nullcaps_n ut_rev_n class_links_n irq_control_n ioport_control_n + nullcaps_n ut_rev_n class_links_n irq_control_n distinct_zombies_n reply_masters_rvk_fb_n - by (auto simp: untyped_eq X64.valid_arch_mdb_ctes_def) + by (auto simp: untyped_eq) end @@ -5732,10 +5683,7 @@ lemma make_zombie_invs': apply (subgoal_tac "cap \ IRQControlCap") apply (clarsimp simp: irq_control_def) apply (clarsimp simp: isCap_simps) - apply (rule conjI[rotated]) - apply (subgoal_tac "cap \ ArchObjectCap IOPortControlCap") - apply (clarsimp simp: ioport_control_def) - apply (clarsimp simp: isCap_simps) + apply (clarsimp simp: isCap_simps) apply (simp add: reply_masters_rvk_fb_def, erule ball_ran_fun_updI) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: modify_map_apply) @@ -8493,28 +8441,6 @@ proof apply (erule (1) irq_controlD, rule irq_control) done - show "valid_arch_mdb_ctes m'" using src dest parency - apply (clarsimp simp: ioport_control_def) - apply (frule m'_revocable) - apply (drule m'_cap) - apply (clarsimp split: if_split_asm) - apply (clarsimp simp add: weak_derived'_def) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule m'_cap) - apply (clarsimp split: if_split_asm) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule m'_cap) - apply (clarsimp split: if_split_asm) - apply (clarsimp simp: weak_derived'_def) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - done - have distz: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def) diff --git a/proof/refine/X64/CSpace1_R.thy b/proof/refine/X64/CSpace1_R.thy index 116366ac8a..4151dd801d 100644 --- a/proof/refine/X64/CSpace1_R.thy +++ b/proof/refine/X64/CSpace1_R.thy @@ -14,6 +14,24 @@ imports "AInvs.ArchDetSchedSchedule_AI" begin +context Arch begin arch_global_naming + +(* IOPortControl caps are unique and always revocable. Defined separately from archMDBAssertions, + because locale mdb_insert_simple needs a form that only takes a cte_heap. *) +definition arch_mdb_assert :: "cte_heap \ bool" where + "arch_mdb_assert m \ + \p n. m p = Some (CTE (ArchObjectCap IOPortControlCap) n) \ + mdbRevocable n \ + (\p' n'. m p' = Some (CTE (ArchObjectCap IOPortControlCap) n') \ p' = p)" + +end + +arch_requalify_consts + arch_mdb_assert + +defs archMDBAssertions_def: + "archMDBAssertions s \ arch_mdb_assert (ctes_of s)" + context Arch begin global_naming X64_A (*FIXME: arch-split*) lemmas final_matters_def = final_matters_def[simplified final_matters_arch_def] @@ -248,7 +266,7 @@ lemma pspace_relation_cte_wp_at: lemma pspace_relation_ctes_ofI: "\ pspace_relation (kheap s) (ksPSpace s'); - cte_wp_at ((=) c) slot s; pspace_aligned' s'; + cte_wp_at ((=) c) slot s; pspace_aligned' s'; pspace_distinct' s' \ \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" apply (cases slot, clarsimp) @@ -256,6 +274,22 @@ lemma pspace_relation_ctes_ofI: apply (simp add: cte_wp_at_ctes_of) done +lemma pspace_relation_caps_of_state_cross: + "\ pspace_relation (kheap s) (ksPSpace s'); + caps_of_state s slot = Some c; pspace_aligned s; pspace_distinct s \ + \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" + for s' :: kernel_state + by (auto simp: cte_wp_at_caps_of_state + intro!: pspace_relation_ctes_ofI pspace_aligned_cross pspace_distinct_cross) + +lemma caps_of_state_cross: + "\ caps_of_state s slot = Some cap; pspace_aligned s; pspace_distinct s; (s,s') \ state_relation \ + \ \cap'. cteCaps_of s' (cte_map slot) = Some cap' \ cap_relation cap cap'" + apply (erule state_relationE) + apply (drule (3) pspace_relation_caps_of_state_cross) + apply (fastforce simp: cteCaps_of_def) + done + lemma get_cap_corres_P: "corres (\x y. cap_relation x (cteCap y) \ P x) (cte_wp_at P cslot_ptr) @@ -917,21 +951,13 @@ lemma ctes_of_valid_cap'': done lemma cap_insert_objs' [wp]: - "\valid_objs' - and valid_cap' cap\ - cteInsert cap src dest \\rv. valid_objs'\" - including no_pre - apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: if_split) - apply (wp setCTE_valid_objs) - apply simp - apply wp+ - apply (clarsimp simp: updateCap_def) - apply (wp|simp)+ - apply (rule hoare_drop_imp)+ - apply wp+ - apply (rule hoare_strengthen_post[OF getCTE_sp]) + "\valid_objs' and valid_cap' cap\ + cteInsert cap src dest + \\_. valid_objs'\" + apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: setCTE_valid_objs | wp getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps - dest!: ctes_of_valid_cap'') + dest!: ctes_of_valid_cap'') done lemma cteInsert_weak_cte_wp_at: @@ -1972,6 +1998,21 @@ lemma pspace_relation_cte_wp_atI: apply assumption done +lemma caps_of_state_rev_cross: + "\ ctes_of s' p = Some cte; valid_objs s; (s,s') \ state_relation \ + \ \cap slot. caps_of_state s slot = Some cap \ p = cte_map slot \ cap_relation cap (cteCap cte)" + apply (erule state_relationE) + apply (drule (2) pspace_relation_cte_wp_atI) + apply (fastforce simp: cte_wp_at_caps_of_state) + done + +lemma cap_relation_IOPortControlCap[simp]: + "cap_relation cap (ArchObjectCap IOPortControlCap) = + (cap = Structures_A.ArchObjectCap X64_A.IOPortControlCap)" + apply (cases cap; simp) + apply (rename_tac acap, case_tac acap; simp) + done + lemma sameRegion_corres: "\ sameRegionAs c' d'; cap_relation c c'; cap_relation d d' \ \ same_region_as c d" @@ -4550,43 +4591,6 @@ lemma irq_control_preserve: apply (simp add:dom misc)+ done -lemma ioport_control_preserve_oneway: - assumes dom: "\x. (x \ dom m) = (x \ dom m')" - assumes misc: - "\x cte cte'. \m x =Some cte;m' x = Some cte'\ \ - isIOPortControlCap' (cteCap cte) = isIOPortControlCap' (cteCap cte') \ - cteMDBNode cte = cteMDBNode cte'" - shows "ioport_control m \ ioport_control m'" - apply (clarsimp simp:ioport_control_def) - apply (frule iffD2[OF dom,OF domI]) - apply clarsimp - apply (frule(1) misc) - apply (clarsimp simp:isCap_simps) - apply (case_tac y) - apply (elim allE impE) - apply fastforce - apply clarsimp - apply (drule_tac x = p' in spec) - apply (erule impE) - apply (frule_tac x1 = p' in iffD2[OF dom,OF domI]) - apply clarsimp - apply (drule(1) misc)+ - apply (case_tac y) - apply (simp add:isCap_simps)+ - done - -lemma ioport_control_preserve: - assumes dom: "\x. (x \ dom m) = (x \ dom m')" - assumes misc: - "\x cte cte'. \m x =Some cte;m' x = Some cte'\ \ - isIOPortControlCap' (cteCap cte) = isIOPortControlCap' (cteCap cte') \ - cteMDBNode cte = cteMDBNode cte'" - shows "ioport_control m = ioport_control m'" - apply (rule iffI[OF ioport_control_preserve_oneway[OF dom misc]]) - apply (assumption)+ - apply (rule ioport_control_preserve_oneway) - apply (simp add:dom misc)+ - done end locale mdb_inv_preserve = fixes m m' @@ -4625,8 +4629,7 @@ lemma preserve_stuff: \ mdb_chunked m = mdb_chunked m' \ valid_badges m = valid_badges m' \ untyped_mdb' m = untyped_mdb' m' - \ irq_control m = irq_control m' - \ ioport_control m = ioport_control m'" + \ irq_control m = irq_control m'" apply (intro conjI) apply (rule valid_dlist_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ @@ -4646,8 +4649,6 @@ lemma preserve_stuff: apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ apply (rule irq_control_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ - apply (rule ioport_control_preserve) - apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ done lemma untyped_inc': @@ -4983,39 +4984,6 @@ lemma updateCapFreeIndex_irq_control: apply (clarsimp simp:cte_wp_at_ctes_of)+ done -context begin interpretation Arch . (* FIXME arch-split *) - -lemma updateCapFreeIndex_ioport_control: - assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" - shows - "\\s. P (ioport_control (Q (ctes_of s))) \ cte_wp_at' (\c. c = srcCTE \ isUntypedCap (cteCap c)) src s\ - updateCap src (capFreeIndex_update (\_. index) (cteCap srcCTE)) - \\r s. P (ioport_control (Q (ctes_of s)))\" - apply (wp updateCap_ctes_of_wp) - apply (subgoal_tac "mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src - (cteCap_update (\_. capFreeIndex_update (\_. index) (cteCap srcCTE)))))") - apply (drule mdb_inv_preserve.preserve_stuff) - apply simp - apply (rule preserve) - apply (rule mdb_inv_preserve_updateCap) - apply (clarsimp simp:cte_wp_at_ctes_of)+ - done - -lemma setUntypedCapAsFull_ioport_control: - assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" - shows - "\\s. P (ioport_control (Q (ctes_of s))) \ cte_wp_at' (\c. c = srcCTE) src s\ - setUntypedCapAsFull (cteCap srcCTE) cap src - \\r s. P (ioport_control (Q (ctes_of s)))\" - apply (clarsimp simp:setUntypedCapAsFull_def split:if_splits,intro conjI impI) - apply (wp updateCapFreeIndex_ioport_control) - apply (clarsimp simp:cte_wp_at_ctes_of preserve)+ - apply wp - apply clarsimp - done - -end - lemma setUntypedCapAsFull_mdb_chunked: assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" shows @@ -5315,6 +5283,46 @@ lemma cte_map_inj_eq': done context begin interpretation Arch . (*FIXME: arch-split*) + +lemma arch_mdb_assertD: + "\ m p = Some (CTE (ArchObjectCap IOPortControlCap) n); m p' = Some (CTE (ArchObjectCap IOPortControlCap) n'); + arch_mdb_assert m \ \ p' = p" + unfolding arch_mdb_assert_def by blast + +lemma ioport_revocable: + "\ m p = Some (CTE (ArchObjectCap IOPortControlCap) n); arch_mdb_assert m \ \ mdbRevocable n" + unfolding arch_mdb_assert_def by blast + +lemma arch_mdb_assert_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); ioport_control_unique s; valid_objs s; + (s,s') \ state_relation \ + \ arch_mdb_assert (ctes_of s')" + unfolding arch_mdb_assert_def valid_arch_mdb_def + apply clarsimp + apply (frule (2) caps_of_state_rev_cross) + apply clarsimp + apply (rule conjI) + (* revocable *) + apply (simp add: ioport_revocable_def) + apply (erule allE, erule allE, erule (1) impE) + apply (erule state_relationE) + apply (clarsimp simp: revokable_relation_def) + apply (force simp: null_filter_def) + (* ioport_control_unique *) + apply (thin_tac "ctes_of s' _ = _") + apply (clarsimp simp: ioport_control_unique_def) + apply (drule (2) caps_of_state_rev_cross) + apply fastforce + done + +(* interface lemma: generic statement, arch-specific proof *) +lemma archMDBAssertions_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_arch_state s; valid_objs s; + (s, s') \ state_relation \ + \ archMDBAssertions s'" + unfolding archMDBAssertions_def + by (drule arch_mdb_assert_cross; simp add: valid_arch_state_def) + lemma cteInsert_corres: notes split_paired_All[simp del] split_paired_Ex[simp del] trans_state_update'[symmetric,simp] @@ -5323,30 +5331,33 @@ lemma cteInsert_corres: (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=Structures_A.NullCap) dest and - (\s. cte_wp_at (is_derived (cdt s) src c) src s)) + (\s. cte_wp_at (is_derived (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and cte_wp_at' (\c. cteCap c=NullCap) dest') (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _) _ _") using assms unfolding cap_insert_def cteInsert_def apply simp + (* this lemma doesn't use the assertion, but does need to establish it *) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (is_derived (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src)" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -5355,7 +5366,7 @@ lemma cteInsert_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. (is_derived (cdt s) src c) src_cap) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) and + R'="\r. ?P' and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src)" in corres_split[where r'=dc]) @@ -5442,7 +5453,7 @@ lemma cteInsert_corres: apply(rule conjI) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") @@ -5712,7 +5723,7 @@ lemma cteInsert_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = isCapRevocable c' (cteCap srcCTE)") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply simp apply (rule is_cap_revocable_eq, assumption, assumption) @@ -5725,7 +5736,7 @@ lemma cteInsert_corres: split:if_splits dest!:cap_master_cap_eqDs) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5752,14 +5763,14 @@ lemma cteInsert_corres: apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE, clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) apply (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") diff --git a/proof/refine/X64/CSpace_I.thy b/proof/refine/X64/CSpace_I.thy index da26dd48aa..7905f2df9f 100644 --- a/proof/refine/X64/CSpace_I.thy +++ b/proof/refine/X64/CSpace_I.thy @@ -1418,8 +1418,7 @@ lemma untyped_mdb: "untyped_mdb' m" and untyped_inc: "untyped_inc' m" and class_links: "class_links m" and - irq_control: "irq_control m" and - arch_mdb_ctes: "valid_arch_mdb_ctes m" (* FIXME arch-split: this should be valid_arch_mdb_ctes *) + irq_control: "irq_control m" using valid by (simp_all add: valid_mdb_ctes_def) @@ -1956,35 +1955,6 @@ lemma irq_control_init: apply (erule (1) irq_controlD, rule ctrl) done -definition - "no_ioport' m \ \p cte. m p = Some cte \ cteCap cte \ (ArchObjectCap IOPortControlCap)" - -lemma no_ioportD': - "\ m p = Some (CTE (ArchObjectCap IOPortControlCap) n); no_ioport' m \ \ False" - unfolding no_ioport'_def - apply (erule allE, erule allE, erule (1) impE) - apply auto - done - -lemma ioport_control_init: - assumes no_ioport: "cap = (ArchObjectCap IOPortControlCap) \ no_ioport' m" - assumes ctrl: "ioport_control m" - shows "ioport_control (m(p \ CTE cap initMDBNode))" - using no_ioport - apply (clarsimp simp: ioport_control_def) - apply (rule conjI) - apply (clarsimp simp: initMDBNode_def) - apply (erule (1) no_ioportD') - apply clarsimp - apply (frule ioport_revocable, rule ctrl) - apply clarsimp - apply (rule conjI) - apply clarsimp - apply (erule (1) no_ioportD') - apply clarsimp - apply (erule (1) ioport_controlD, rule ctrl) - done - lemma valid_mdb_ctes_init: "\ valid_mdb_ctes m; m p = Some cte; no_mdb cte; caps_no_overlap' m (capRange cap); s \' cap; @@ -2019,10 +1989,8 @@ lemma valid_mdb_ctes_init: apply (rule valid_capAligned, erule(1) ctes_of_valid_cap') apply (rule conjI) apply (erule (1) irq_control_init) - apply (rule conjI) - apply (simp add: ran_def reply_masters_rvk_fb_def) - apply (auto simp: initMDBNode_def)[1] - apply (erule (1) ioport_control_init) + apply (simp add: ran_def reply_masters_rvk_fb_def) + apply (auto simp: initMDBNode_def)[1] done lemma setCTE_state_refs_of'[wp]: diff --git a/proof/refine/X64/CSpace_R.thy b/proof/refine/X64/CSpace_R.thy index a61db81a45..e97fda36d3 100644 --- a/proof/refine/X64/CSpace_R.thy +++ b/proof/refine/X64/CSpace_R.thy @@ -1405,24 +1405,6 @@ lemma (in mdb_insert_der) irq_control_n: apply (erule (1) irq_controlD, rule irq_control) done -(* FIXME arch-split: locale issues here, can't place in Arch, need to re-work hierarchy *) -lemma (in mdb_insert_der) ioport_control_n: - "X64.ioport_control n" - using src dest partial_is_derived' - apply (clarsimp simp: X64.ioport_control_def) - apply (frule n_cap) - apply (drule n_revocable) - apply (clarsimp split: if_split_asm) - apply (simp add: is_derived'_def isCap_simps) - apply (frule X64.ioport_revocable, rule arch_mdb_ctes[simplified X64.valid_arch_mdb_ctes_def]) - apply clarsimp - apply (drule n_cap) - apply (clarsimp split: if_split_asm) - apply (erule disjE) - apply (clarsimp simp: is_derived'_def isCap_simps) - apply (erule (1) X64.ioport_controlD, rule arch_mdb_ctes[simplified X64.valid_arch_mdb_ctes_def]) - done - context mdb_insert_child begin @@ -1998,73 +1980,6 @@ lemma cteInsert_irq_control: apply (clarsimp simp: modify_map_apply irq_control_prev_update fun_upd_def) done -lemma ioport_control_prev_update: - "ioport_control (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = ioport_control m" - apply (simp add: ioport_control_def) - apply (rule iffI) - apply clarsimp - apply (simp only: modify_map_if) - apply (erule_tac x=p in allE) - apply (simp (no_asm_use) split: if_split_asm) - apply (case_tac "x=p") - apply fastforce - apply clarsimp - apply (erule_tac x=p' in allE) - apply simp - apply (case_tac "x=p'") - apply simp - apply fastforce - apply clarsimp - apply (erule_tac x=p in allE) - apply (simp add: modify_map_if split: if_split_asm) - apply clarsimp - apply (case_tac "x=p'") - apply clarsimp - apply clarsimp - apply clarsimp - apply (case_tac "x=p'") - apply clarsimp - apply clarsimp - done - -lemma cteInsert_ioport_control: - "\valid_mdb' and pspace_distinct' and pspace_aligned' and (\s. src \ dest) and - (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ - cteInsert cap src dest - \\_ s. ioport_control (ctes_of s)\" - apply (unfold cteInsert_def updateCap_def) - apply (simp add: valid_mdb'_def split del: if_split) - apply (wp updateMDB_ctes_of_no_0 getCTE_wp') - apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) - apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of - setUntypedCapAsFull_ctes_of_no_0 setUntypedCapAsFull_ioport_control mdb_inv_preserve_fun_upd - mdb_inv_preserve_modify_map,simp) - apply (wp getCTE_wp)+ - apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) - apply (subgoal_tac "src \ 0") - prefer 2 - apply (fastforce simp: valid_mdb_ctes_def no_0_def) - apply (subgoal_tac "dest \ 0") - prefer 2 - apply (fastforce simp: valid_mdb_ctes_def no_0_def) - apply (rule conjI) - apply (fastforce simp: valid_mdb_ctes_def no_0_def) - apply (case_tac cte) - apply (rename_tac s_cap s_node) - apply (case_tac cteb) - apply (rename_tac d_cap d_node) - apply (simp add: nullPointer_def) - apply (subgoal_tac "mdb_insert_der (ctes_of s) src s_cap s_node dest NullCap d_node cap") - prefer 2 - apply unfold_locales[1] - apply (assumption|rule refl)+ - apply (simp add: valid_mdb_ctes_def) - apply (simp add: valid_mdb_ctes_def) - apply assumption+ - apply (drule mdb_insert_der.ioport_control_n) - apply (clarsimp simp: modify_map_apply ioport_control_prev_update fun_upd_def) - done - lemma capMaster_isUntyped: "capMasterCap c = capMasterCap c' \ isUntypedCap c = isUntypedCap c'" by (simp add: capMasterCap_def isCap_simps split: capability.splits) @@ -2241,7 +2156,7 @@ lemma cteInsert_mdb' [wp]: \\_. valid_mdb'\" apply (simp add:valid_mdb'_def valid_mdb_ctes_def) apply (rule_tac Q'="\r s. valid_dlist (ctes_of s) \ irq_control (ctes_of s) \ - no_0 (ctes_of s) \ mdb_chain_0 (ctes_of s) \ ioport_control (ctes_of s) \ + no_0 (ctes_of s) \ mdb_chain_0 (ctes_of s) \ mdb_chunked (ctes_of s) \ untyped_mdb' (ctes_of s) \ untyped_inc' (ctes_of s) \ Q s" for Q in hoare_strengthen_post) @@ -2250,7 +2165,7 @@ lemma cteInsert_mdb' [wp]: apply assumption apply (rule hoare_name_pre_state) apply (wp cteInsert_no_0 cteInsert_valid_dlist cteInsert_mdb_chain_0 cteInsert_untyped_inc' - cteInsert_mdb_chunked cteInsert_untyped_mdb cteInsert_irq_control cteInsert_ioport_control) + cteInsert_mdb_chunked cteInsert_untyped_mdb cteInsert_irq_control) apply (unfold cteInsert_def) apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: if_split) @@ -2308,7 +2223,6 @@ proof - and class_links: "class_links ?m" and distinct_zombies: "distinct_zombies ?m" and irq: "irq_control ?m" - and ioport: "ioport_control ?m" and reply_masters_rvk_fb: "reply_masters_rvk_fb ?m" and vn: "valid_nullcaps ?m" and ut_rev:"ut_revocable' ?m" @@ -4541,14 +4455,9 @@ lemma arch_update_setCTE_mdb: apply (clarsimp simp: is_arch_update'_def isCap_simps) apply (rule conjI) apply clarsimp - apply (rule conjI) - apply (simp add: reply_masters_rvk_fb_def) - apply (erule ball_ran_fun_updI) - apply (clarsimp simp add: is_arch_update'_def isCap_simps) - apply (clarsimp simp: is_arch_update'_def) - apply (case_tac cap; clarsimp simp: isCap_simps) - apply (case_tac x8; clarsimp simp: isCap_simps ioport_control_def) - apply auto + apply (simp add: reply_masters_rvk_fb_def) + apply (erule ball_ran_fun_updI) + apply (clarsimp simp add: is_arch_update'_def isCap_simps) done lemma capMaster_zobj_refs: @@ -4673,6 +4582,7 @@ end locale mdb_insert_simple = mdb_insert + assumes safe_parent: "safe_parent_for' m src c'" assumes simple: "is_simple_cap' c'" + assumes arch_mdb_assert: "arch_mdb_assert m" begin interpretation Arch . (*FIXME: arch-split*) lemma dest_no_parent_n: @@ -4711,7 +4621,7 @@ lemma src_node_revokable [simp]: apply (erule disjE) apply (clarsimp simp: ut_revocable'_def) apply (clarsimp simp: isCap_simps) - apply (erule ioport_revocable, rule arch_mdb_ctes[simplified]) + apply (erule ioport_revocable, rule arch_mdb_assert) done lemma new_child [simp]: @@ -4876,6 +4786,15 @@ lemma maskedAsFull_revokable_safe_parent: context begin interpretation Arch . (*FIXME: arch-split*) +(* FIXME arch-split: generic statement, arch specific proof *) +lemma setUntypedCapAsFull_archMDBAssertions[wp]: + "setUntypedCapAsFull src_cap cap p \archMDBAssertions\" + unfolding setUntypedCapAsFull_def archMDBAssertions_def updateCap_def + apply (wpsimp wp: getCTE_wp') + apply (rename_tac cte, case_tac cte, rename_tac cte_cap node) + apply (clarsimp simp: arch_mdb_assert_def cte_wp_at_ctes_of isCap_simps split: if_split_asm) + done + lemma cteInsert_simple_corres: assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest" notes trans_state_update'[symmetric,simp] @@ -4884,34 +4803,36 @@ lemma cteInsert_simple_corres: valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=cap.NullCap) dest and K (is_simple_cap c) and - (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s)) + (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and K (is_simple_cap' c') and cte_wp_at' (\c. cteCap c=NullCap) dest' and (\s. safe_parent_for' (ctes_of s) src' c')) (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _ and _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _ and _) _ _") using assms unfolding cap_insert_def cteInsert_def supply subst_all [simp del] apply simp + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and - Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + Q="?P' and archMDBAssertions and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -4920,7 +4841,7 @@ lemma cteInsert_simple_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) + R'="\r. ?P' and archMDBAssertions and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_split[where r'=dc]) @@ -5015,7 +4936,7 @@ lemma cteInsert_simple_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = isCapRevocable c' (cteCap srcCTE)") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) apply (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply clarsimp apply (rule is_cap_revocable_eq, assumption, assumption) @@ -5028,7 +4949,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5052,14 +4973,14 @@ lemma cteInsert_simple_corres: set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") @@ -5083,7 +5004,8 @@ lemma cteInsert_simple_corres: apply (simp (no_asm_simp) add: cdt_relation_def split: if_split) apply (intro impI allI) apply (frule mdb_insert_simple_axioms.intro) - apply(clarsimp simp:cte_wp_at_ctes_of) + apply(clarsimp simp:cte_wp_at_ctes_of) + apply (simp add: archMDBAssertions_def) apply (drule (1) mdb_insert_simple.intro) apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable_safe_parent[symmetric]) apply simp+ @@ -5740,7 +5662,7 @@ lemma ioport_control_src: apply (erule disjE, clarsimp simp: isCap_simps) apply (erule disjE, clarsimp simp: isCap_simps capRange_def) apply (clarsimp simp: isCap_simps split: if_split_asm) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) + apply (drule (1) arch_mdb_assertD, rule arch_mdb_assert) apply simp done @@ -5955,26 +5877,6 @@ lemma irq' [simp]: apply (erule (1) irq_controlD, rule irq_control) done -context begin interpretation Arch . (* FIXME arch-split *) - -lemma ioport' [simp]: - "ioport_control n'" using simple - apply (clarsimp simp: ioport_control_def) - apply (frule n'_cap) - apply (drule n'_rev) - apply (clarsimp split: if_split_asm) - apply (simp add: is_simple_cap'_def isCap_simps) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule n'_cap) - apply (clarsimp split: if_split_asm) - apply (erule disjE) - apply (clarsimp simp: is_simple_cap'_def isCap_simps) - apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - done - -end - lemma reply_masters_rvk_fb: "reply_masters_rvk_fb m" using valid by (simp add: valid_mdb_ctes_def) @@ -6047,7 +5949,7 @@ lemma cteInsert_simple_mdb': mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ - apply ((clarsimp simp:valid_mdb_ctes_def)+) + apply (clarsimp simp:valid_mdb_ctes_def archMDBAssertions_def)+ apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) done diff --git a/proof/refine/X64/Detype_R.thy b/proof/refine/X64/Detype_R.thy index 62401110d4..64ba5bb398 100644 --- a/proof/refine/X64/Detype_R.thy +++ b/proof/refine/X64/Detype_R.thy @@ -628,7 +628,6 @@ lemma valid_objs: "valid_objs' 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'" @@ -1586,10 +1585,6 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def show "irq_control ?ctes'" by (clarsimp simp: irq_control_def) - from ioport_ctrl - show "valid_arch_mdb_ctes ?ctes'" - by (clarsimp simp: ioport_control_def) - from dist_z show "distinct_zombies ?ctes'" apply (simp add: tree_to_ctes distinct_zombies_def diff --git a/proof/refine/X64/Finalise_R.thy b/proof/refine/X64/Finalise_R.thy index 8774905fa1..1c1a83cc29 100644 --- a/proof/refine/X64/Finalise_R.thy +++ b/proof/refine/X64/Finalise_R.thy @@ -1060,19 +1060,6 @@ lemma irq_control_n [simp]: "irq_control n" apply (erule (1) irq_controlD, rule irq_control) done -lemma ioport_control_n [simp]: "ioport_control n" - using slot - apply (clarsimp simp: ioport_control_def) - apply (frule n_revokable) - apply (drule n_cap) - apply (clarsimp split: if_split_asm) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule n_cap) - apply (clarsimp simp: if_split_asm) - apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - done - lemma reply_masters_rvk_fb_m: "reply_masters_rvk_fb m" using valid by auto diff --git a/proof/refine/X64/Interrupt_R.thy b/proof/refine/X64/Interrupt_R.thy index 755fdc12ee..6f234a3bde 100644 --- a/proof/refine/X64/Interrupt_R.thy +++ b/proof/refine/X64/Interrupt_R.thy @@ -500,6 +500,13 @@ crunch X64_H.updateIRQState and ex_cte_cap_wp_to'[wp]: "ex_cte_cap_wp_to' a b" (simp: ex_cte_cap_wp_to'_def valid_mdb'_def) +crunch set_irq_state + for valid_arch_state[wp]: valid_arch_state + +lemma maxUserIRQ_le_maxIRQ: + "X64.maxUserIRQ \ maxIRQ" + by (simp add: X64.maxUserIRQ_def maxIRQ_def) + lemma arch_performIRQControl_corres: "arch_irq_control_inv_relation x2 ivk' \ corres (dc \ dc) (einvs and arch_irq_control_inv_valid x2) @@ -516,10 +523,12 @@ lemma arch_performIRQControl_corres: apply (rule setIRQState_corres) apply (simp add: irq_state_relation_def) apply (rule cteInsert_simple_corres) - apply (wpsimp simp: IRQHandler_valid IRQHandler_valid' | wps)+ + apply (wpsimp simp: IRQHandler_valid IRQHandler_valid' + | strengthen invs_arch_state + | wps)+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def cte_wp_at_caps_of_state is_simple_cap_def is_cap_simps arch_irq_control_inv_valid_def - safe_parent_for_def) + safe_parent_for_def order_trans[OF _ maxUserIRQ_le_maxIRQ]) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def IRQHandler_valid IRQHandler_valid' is_simple_cap'_def isCap_simps IRQ_def) apply (clarsimp simp: safe_parent_for'_def cte_wp_at_ctes_of) @@ -533,10 +542,12 @@ lemma arch_performIRQControl_corres: apply (rule setIRQState_corres) apply (simp add: irq_state_relation_def) apply (rule cteInsert_simple_corres) - apply (wpsimp simp: IRQHandler_valid IRQHandler_valid' | wps)+ + apply (wpsimp simp: IRQHandler_valid IRQHandler_valid' + | strengthen invs_arch_state + | wps)+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def cte_wp_at_caps_of_state is_simple_cap_def is_cap_simps arch_irq_control_inv_valid_def - safe_parent_for_def) + safe_parent_for_def order_trans[OF _ maxUserIRQ_le_maxIRQ]) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def IRQHandler_valid IRQHandler_valid' is_simple_cap'_def isCap_simps IRQ_def) apply (clarsimp simp: safe_parent_for'_def cte_wp_at_ctes_of) diff --git a/proof/refine/X64/Ipc_R.thy b/proof/refine/X64/Ipc_R.thy index b598d115d6..d5e2c5e684 100644 --- a/proof/refine/X64/Ipc_R.thy +++ b/proof/refine/X64/Ipc_R.thy @@ -392,6 +392,10 @@ lemma cte_refs'_maskedAsFull[simp]: apply (clarsimp simp:maskedAsFull_def isCap_simps)+ done +lemma set_extra_badge_valid_arch_state[wp]: + "set_extra_badge buffer badge n \ valid_arch_state \" + unfolding set_extra_badge_def + by wp lemma transferCapsToSlots_corres: "\ list_all2 (\(cap, slot) (cap', slot'). cap_relation cap cap' @@ -399,7 +403,7 @@ lemma transferCapsToSlots_corres: mi' = message_info_map mi \ \ corres ((=) \ message_info_map) (\s. valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_mdb s - \ valid_list s + \ valid_list s \ valid_arch_state s \ (case ep of Some x \ ep_at x s | _ \ True) \ (\x \ set slots. cte_wp_at (\cap. cap = cap.NullCap) x s \ real_cte_at x s) @@ -473,7 +477,8 @@ next apply (simp add: tl_map) apply (rule corres_rel_imp, rule Cons.hyps, simp_all)[1] apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift - hoare_vcg_const_Ball_lift cap_insert_weak_cte_wp_at) + hoare_vcg_const_Ball_lift cap_insert_derived_valid_arch_state + cap_insert_weak_cte_wp_at) apply (wp hoare_vcg_const_Ball_lift | simp add:split_def del: imp_disj1)+ apply (wp cap_insert_cte_wp_at) apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift @@ -614,6 +619,7 @@ lemma cteInsert_assume_Null: apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cteInsert_def) + apply (rule bind_wp[OF _ stateAssert_sp]) apply (rule bind_wp[OF _ getCTE_sp])+ apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) @@ -1040,7 +1046,7 @@ lemma transferCaps_corres: corres ((=) \ message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb - and valid_list + and valid_list and valid_arch_state and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame recv_buf and (\s. valid_message_info info) @@ -1459,10 +1465,14 @@ lemma copyMRs_valid_mdb[wp]: "\valid_mdb'\ copyMRs t buf t' buf' n \\rv. valid_mdb'\" by (simp add: valid_mdb'_def copyMRs_ctes_of) +crunch copy_mrs + for valid_arch_state[wp]: valid_arch_state + (wp: crunch_wps) + lemma doNormalTransfer_corres: "corres dc (tcb_at sender and tcb_at receiver and (pspace_aligned:: det_state \ bool) - and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct + and valid_objs and cur_tcb and valid_mdb and valid_list and valid_arch_state and pspace_distinct and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame send_buf and case_option \ in_user_frame recv_buf) @@ -1733,7 +1743,7 @@ lemma lookupIPCBuffer_valid_ipc_buffer [wp]: lemma doIPCTransfer_corres: "corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned - and valid_list + and valid_list and valid_arch_state and pspace_distinct and valid_mdb and cur_tcb and (\s. case ep of Some x \ ep_at x s | _ \ True)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' @@ -1741,9 +1751,9 @@ lemma doIPCTransfer_corres: (do_ipc_transfer s ep bg grt r) (doIPCTransfer s ep bg grt r)" apply (simp add: do_ipc_transfer_def doIPCTransfer_def) - apply (rule_tac Q="%receiveBuffer sa. tcb_at s sa \ valid_objs sa \ - pspace_aligned sa \ tcb_at r sa \ - cur_tcb sa \ valid_mdb sa \ valid_list sa \ pspace_distinct sa \ + apply (rule_tac Q="\receiveBuffer sa. tcb_at s sa \ valid_objs sa \ + pspace_aligned sa \ pspace_distinct sa \ tcb_at r sa \ + cur_tcb sa \ valid_mdb sa \ valid_list sa \ valid_arch_state sa \ (case ep of None \ True | Some x \ ep_at x sa) \ case_option (\_. True) in_user_frame receiveBuffer sa \ obj_at (\ko. \tcb. ko = TCB tcb @@ -2329,7 +2339,7 @@ lemma setupCallerCap_corres: (st_tcb_at (Not \ halted) sender and tcb_at receiver and st_tcb_at (Not \ awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb - and valid_list and + and valid_list and valid_arch_state and valid_reply_masters and cte_wp_at (\c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) @@ -2546,6 +2556,7 @@ proof - valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct valid_sched_valid_queues)+ apply ((wp hoare_drop_imps do_ipc_transfer_tcb_caps weak_valid_sched_action_lift + do_ipc_transfer_valid_arch | clarsimp simp: is_cap_simps)+)[1] apply (simp add: pred_conj_def) apply (strengthen sch_act_wf_weak) @@ -3245,7 +3256,7 @@ lemma receiveIPC_corres: apply (rule corres_split[OF doIPCTransfer_corres]) apply (simp split del: if_split cong: if_cong) apply (fold dc_def)[1] - apply (rule_tac P="valid_objs and valid_mdb and valid_list + apply (rule_tac P="valid_objs and valid_mdb and valid_list and valid_arch_state and valid_sched and cur_tcb and valid_reply_caps @@ -3275,7 +3286,7 @@ lemma receiveIPC_corres: apply (fastforce simp: st_tcb_at_tcb_at st_tcb_def2 valid_sched_def valid_sched_action_def) apply (clarsimp split: if_split_asm) - apply (clarsimp | wp do_ipc_transfer_tcb_caps)+ + apply (clarsimp | wp do_ipc_transfer_tcb_caps do_ipc_transfer_valid_arch)+ apply (rule_tac Q'="\_ s. sch_act_wf (ksSchedulerAction s) s \ sym_heap_sched_pointers s \ valid_sched_pointers s \ pspace_aligned' s \ pspace_distinct' s" @@ -3607,19 +3618,12 @@ lemma cteInsert_cap_to': "\ex_nonz_cap_to' p and cte_wp_at' (\c. cteCap c = NullCap) dest\ cteInsert cap src dest \\rv. ex_nonz_cap_to' p\" - apply (simp add: cteInsert_def ex_nonz_cap_to'_def - updateCap_def setUntypedCapAsFull_def - split del: if_split) - apply (rule hoare_pre, rule hoare_vcg_ex_lift) - apply (wp updateMDB_weak_cte_wp_at - setCTE_weak_cte_wp_at - | simp - | rule hoare_drop_imps)+ - apply (wp getCTE_wp) - apply clarsimp + apply (simp add: cteInsert_def ex_nonz_cap_to'_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: updateMDB_weak_cte_wp_at setCTE_weak_cte_wp_at hoare_vcg_ex_lift + | rule hoare_drop_imps + | wp getCTE_wp)+ (* getCTE_wp is separate to apply it only to the last one *) apply (rule_tac x=cref in exI) - apply (rule conjI) - apply (clarsimp simp: cte_wp_at_ctes_of)+ + apply (fastforce simp: cte_wp_at_ctes_of) done crunch setExtraBadge diff --git a/proof/refine/X64/Retype_R.thy b/proof/refine/X64/Retype_R.thy index 24fd400795..e5e6bca43b 100644 --- a/proof/refine/X64/Retype_R.thy +++ b/proof/refine/X64/Retype_R.thy @@ -3029,15 +3029,6 @@ lemma irq_control_n: apply (erule (1) irq_controlD, rule irq_control) done -lemma ioport_control_n: - "ioport_control n" - apply (clarsimp simp add: ioport_control_def) - apply (simp add: n_Some_eq split: if_split_asm) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - done - lemma dist_z_m: "distinct_zombies m" using valid by auto @@ -3065,7 +3056,7 @@ lemma valid_n: by (simp add: valid_mdb_ctes_def dlist_n no_0_n mdb_chain_0_n valid_badges_n caps_contained_n untyped_mdb_n untyped_inc_n mdb_chunked_n valid_nullcaps_n ut_rev_n - class_links_n irq_control_n dist_z_n ioport_control_n + class_links_n irq_control_n dist_z_n reply_masters_rvk_fb_n) end diff --git a/proof/refine/X64/Tcb_R.thy b/proof/refine/X64/Tcb_R.thy index 218b5d059b..1891e4e47f 100644 --- a/proof/refine/X64/Tcb_R.thy +++ b/proof/refine/X64/Tcb_R.thy @@ -867,7 +867,7 @@ lemma checkCapAt_cteInsert_corres: apply clarsimp apply (rule conjI, fastforce)+ apply (cases src_slot) - apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: cte_wp_at_caps_of_state invs_arch_state) apply (rule conjI) apply (frule same_object_as_cap_master) apply (clarsimp simp: cap_master_cap_simps is_cnode_or_valid_arch_def diff --git a/proof/refine/X64/Untyped_R.thy b/proof/refine/X64/Untyped_R.thy index 90cad18eef..74903212f0 100644 --- a/proof/refine/X64/Untyped_R.thy +++ b/proof/refine/X64/Untyped_R.thy @@ -2692,14 +2692,6 @@ lemma irq_control_n' [simp]: apply (clarsimp simp: modify_map_if split: if_split_asm) done -lemma ioport_control_n' [simp]: - "ioport_control n'" - using arch_mdb_ctes[simplified] phys - apply (clarsimp simp: ioport_control_def) - apply (clarsimp simp: n'_def n_def) - apply (clarsimp simp: modify_map_if split: if_split_asm) - done - lemma dist_z_m: "distinct_zombies m" using valid by auto