From fe7cf9c5efc254d18fddb846cf13c2eb222f6769 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 17 Dec 2024 19:50:07 +1100 Subject: [PATCH] x64 refine: arch-split up to InvariantUpdates_H Updates the rest of X64 Refine to conform to the generic arch-split invariant interface. When things broke and when possible, we took the proof or chunks of proof from AARCH64. Otherwise: - projectKOs is not in the simpset - ioport_control/valid_arch_mdb_ctes hasn't been renamed in all cases, only made to work for now - the power-of-two vs mask situation is still a mess, requiring changing proofs to go one way or the other - unfolding tcb_cte_cases_def would benefit from tcb_cte_cases_neqs being in the simpset so that people avoid unfolding cteSizeBits when not necessary, but that can be done via a separate pass later Signed-off-by: Rafal Kolanski --- proof/refine/X64/ArchMove_R.thy | 2 +- proof/refine/X64/Arch_R.thy | 28 ++-- proof/refine/X64/Bits_R.thy | 2 +- proof/refine/X64/CNodeInv_R.thy | 63 +++---- proof/refine/X64/CSpace1_R.thy | 45 +++-- proof/refine/X64/CSpace_I.thy | 19 ++- proof/refine/X64/CSpace_R.thy | 46 +++--- proof/refine/X64/Detype_R.thy | 137 ++++++++-------- proof/refine/X64/Finalise_R.thy | 37 +++-- proof/refine/X64/InterruptAcc_R.thy | 2 +- proof/refine/X64/Interrupt_R.thy | 6 +- proof/refine/X64/InvariantUpdates_H.thy | 176 +++++++++++++++++--- proof/refine/X64/IpcCancel_R.thy | 40 +++-- proof/refine/X64/Ipc_R.thy | 30 ++-- proof/refine/X64/KHeap_R.thy | 42 ++++- proof/refine/X64/LevityCatch.thy | 1 + proof/refine/X64/RAB_FN.thy | 4 + proof/refine/X64/Refine.thy | 2 +- proof/refine/X64/Retype_R.thy | 103 +++++++----- proof/refine/X64/Schedule_R.thy | 10 +- proof/refine/X64/Syscall_R.thy | 4 +- proof/refine/X64/TcbAcc_R.thy | 49 +++--- proof/refine/X64/Tcb_R.thy | 23 +-- proof/refine/X64/Untyped_R.thy | 209 ++++++++++++------------ proof/refine/X64/VSpace_R.thy | 11 +- 25 files changed, 678 insertions(+), 413 deletions(-) diff --git a/proof/refine/X64/ArchMove_R.thy b/proof/refine/X64/ArchMove_R.thy index 90251d4748..1ffde19822 100644 --- a/proof/refine/X64/ArchMove_R.thy +++ b/proof/refine/X64/ArchMove_R.thy @@ -17,7 +17,7 @@ lemmas cte_index_repair_sym = cte_index_repair[symmetric] lemmas of_nat_inj64 = of_nat_inj[where 'a=machine_word_len, folded word_bits_def] -context begin interpretation Arch . +context Arch begin arch_global_naming lemma no_fail_in8[wp]: "no_fail \ (in8 a)" diff --git a/proof/refine/X64/Arch_R.thy b/proof/refine/X64/Arch_R.thy index 50965f4992..7531980d00 100644 --- a/proof/refine/X64/Arch_R.thy +++ b/proof/refine/X64/Arch_R.thy @@ -86,10 +86,10 @@ lemma createObject_typ_at': apply (unfold pspace_no_overlap'_def) apply (erule allE)+ apply (erule(1) impE) - apply (subgoal_tac "x \ {x..x + 2 ^ objBitsKO y - 1}") - apply (fastforce simp:is_aligned_neg_mask_eq p_assoc_help) + apply (subgoal_tac "x \ mask_range x (objBitsKO y)") + apply (fastforce simp: is_aligned_neg_mask_eq) apply (drule(1) pspace_alignedD') - apply (clarsimp simp: is_aligned_no_wrap' p_assoc_help) + apply (clarsimp simp: is_aligned_no_overflow_mask) done lemma retype_region2_ext_retype_region_ArchObject: @@ -210,6 +210,7 @@ lemma performASIDControlInvocation_corres: apply (simp add:objBits_simps archObjSize_def range_cover_full valid_cap'_def)+ apply (fastforce elim!: canonical_address_neq_mask) apply (rule in_kernel_mappings_neq_mask, (simp add: valid_cap'_def bit_simps)+)[1] + apply (simp add: valid_cap'_def bit_simps) apply (clarsimp simp:valid_cap'_def) apply (wp createObject_typ_at' createObjects_orig_cte_wp_at'[where sz = pageBits]) @@ -334,13 +335,15 @@ lemma performASIDControlInvocation_corres: simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2 null_filter_descendants_of'[OF null_filter_simp'] capAligned_def asid_low_bits_def) - apply (erule descendants_range_caps_no_overlapI') - apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) - apply (simp add:empty_descendants_range_in') - apply (simp add:word_bits_def bit_simps) - apply (rule is_aligned_weaken) - apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) - apply (simp add:pageBits_def) + apply (erule descendants_range_caps_no_overlapI') + apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq) + apply (simp add:empty_descendants_range_in') + apply (simp add:word_bits_def bit_simps) + apply (rule is_aligned_weaken) + apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) + apply (simp add: pageBits_def) + apply (simp add: pageBits_def) + apply (simp add: pageBits_def) apply clarsimp apply (drule(1) cte_cap_in_untyped_range) apply (fastforce simp: cte_wp_at_ctes_of) @@ -2035,7 +2038,7 @@ lemma performASIDControlInvocation_invs' [wp]: apply (wp createObjects'_wp_subst[OF createObjects_no_cte_invs[where sz = pageBits and ty="Inl (KOArch (KOASIDPool pool))" for pool]] createObjects_orig_cte_wp_at'[where sz = pageBits] hoare_vcg_const_imp_lift - |simp add: makeObjectKO_def projectKOs asid_pool_typ_at_ext' valid_cap'_def cong: rev_conj_cong + |simp add: makeObjectKO_def projectKOs asid_pool_typ_at_ext' valid_cap'_def valid_arch_cap'_def cong: rev_conj_cong |strengthen safe_parent_strg'[where idx= "2^ pageBits"])+ apply (rule hoare_vcg_conj_lift) apply (rule descendants_of'_helper) @@ -2107,8 +2110,9 @@ lemma performASIDControlInvocation_invs' [wp]: apply (simp add: pageBits_def untypedBits_defs) apply (frule_tac cte="CTE (capability.UntypedCap False a b c) m" for a b c m in valid_global_refsD', clarsimp) apply (simp add: Int_commute) + apply (prop_tac "w1 \ kernel_mappings") by (auto simp:empty_descendants_range_in' objBits_simps max_free_index_def - archObjSize_def asid_low_bits_def word_bits_def + archObjSize_def asid_low_bits_def word_bits_def live'_def hyp_live'_def range_cover_full descendants_range'_def2 is_aligned_mask null_filter_descendants_of'[OF null_filter_simp'] bit_simps valid_cap_simps' mask_def)+ diff --git a/proof/refine/X64/Bits_R.thy b/proof/refine/X64/Bits_R.thy index c997541ad9..ad70aecd35 100644 --- a/proof/refine/X64/Bits_R.thy +++ b/proof/refine/X64/Bits_R.thy @@ -457,7 +457,7 @@ lemma ko_at_cte_ipcbuffer: "ko_at' tcb p s \ cte_wp_at' (\x. x = tcbIPCBufferFrame tcb) (p + tcbIPCBufferSlot * 0x20) s" apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (erule (2) cte_wp_at_tcbI') - apply (fastforce simp add: tcb_cte_cases_def tcbIPCBufferSlot_def) + apply (fastforce simp: tcb_cte_cases_def tcbIPCBufferSlot_def cteSizeBits_def) apply simp done diff --git a/proof/refine/X64/CNodeInv_R.thy b/proof/refine/X64/CNodeInv_R.thy index 6af4db67ef..9a886cd6d9 100644 --- a/proof/refine/X64/CNodeInv_R.thy +++ b/proof/refine/X64/CNodeInv_R.thy @@ -4781,6 +4781,8 @@ 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) @@ -4788,44 +4790,46 @@ lemma ioport_control_n: "ioport_control n" apply (drule n_cap) apply (clarsimp split: if_split_asm) apply (clarsimp simp: weak_derived'_def) - apply (frule ioport_revocable, rule ioport_control) + 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 ioport_control) + apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) apply simp - apply (drule (1) ioport_controlD, rule ioport_control) + apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) apply simp apply (clarsimp simp: weak_derived'_def) - apply (frule ioport_revocable, rule ioport_control) + 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 ioport_control) + 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 ioport_control) + apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) apply simp apply (clarsimp simp: weak_derived'_def) - apply (frule ioport_revocable, rule ioport_control) + 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 ioport_control) + apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) apply simp - apply (drule (1) ioport_controlD, rule ioport_control) + apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) apply clarsimp - apply (drule (1) ioport_controlD, rule ioport_control) + 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 @@ -4872,7 +4876,7 @@ lemma cteSwap_valid_mdb_helper: cteSwap_chunked caps_contained untyped_mdb_n untyped_inc_n nullcaps_n ut_rev_n class_links_n irq_control_n ioport_control_n distinct_zombies_n reply_masters_rvk_fb_n - by (auto simp:untyped_eq) + by (auto simp: untyped_eq X64.valid_arch_mdb_ctes_def) end @@ -5317,16 +5321,16 @@ lemma Final_notUntyped_capRange_disjoint: apply (clarsimp simp: cteCaps_of_def) apply (drule(1) ctes_of_valid') apply (elim disjE isCapDs[elim_format]) - apply (clarsimp simp: valid_cap'_def bit_simps + apply (clarsimp simp: valid_cap'_def bit_simps valid_arch_cap'_def obj_at'_def projectKOs objBits_simps' - typ_at'_def ko_wp_at'_def + typ_at'_def ko_wp_at'_def live'_def split: capability.split_asm zombie_type.split_asm arch_capability.split_asm dest!: spec[where x=0]) apply (clarsimp simp: sameObjectAs_def3 isCap_simps) apply (simp add: isCap_simps) apply (simp add: isCap_simps) - apply (clarsimp simp: valid_cap'_def bit_simps + apply (clarsimp simp: valid_cap'_def bit_simps valid_arch_cap'_def obj_at'_def projectKOs objBits_simps typ_at'_def ko_wp_at'_def pd_pointer_table_at'_def page_table_at'_def page_directory_at'_def @@ -5644,7 +5648,7 @@ lemma make_zombie_invs': \ bound_tcb_at' ((=) None) p' s \ obj_at' (\tcb. tcbSchedNext tcb = None \ tcbSchedPrev tcb = None) p' s") - apply (clarsimp simp: pred_tcb_at'_def obj_at'_def ko_wp_at'_def projectKOs) + apply (clarsimp simp: pred_tcb_at'_def obj_at'_def ko_wp_at'_def projectKOs live'_def hyp_live'_def) apply (auto dest!: isCapDs)[1] apply (clarsimp simp: cte_wp_at_ctes_of disj_ac dest!: isCapDs) @@ -5759,7 +5763,7 @@ lemma shrink_zombie_invs': apply clarsimp apply (rule ccontr, erule notE, rule imageI) apply (drule word_le_minus_one_leq) - apply (rule ccontr, simp add: linorder_not_less mult.commute mult.left_commute) + apply (rule ccontr, simp add: linorder_not_less mult.commute mult.left_commute shiftl_t2n) done lemma setQueue_cte_wp_at': @@ -5809,6 +5813,7 @@ crunch doMachineOp lemma valid_Zombie_cte_at': "\ s \' Zombie p zt m; n < zombieCTEs zt \ \ cte_at' (p + (of_nat n * 2^cteSizeBits)) s" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (clarsimp simp: valid_cap'_def split: zombie_type.split_asm) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (subgoal_tac "tcb_cte_cases (of_nat n * 2^cteSizeBits) \ None") @@ -6070,7 +6075,7 @@ lemma ex_Zombie_to2: apply (intro exI, rule conjI, assumption) apply (simp add: image_def) apply (rule bexI[where x="of_nat n - 1"]) - apply (fastforce simp: objBits_defs) + apply (fastforce simp: objBits_defs shiftl_t2n) apply (subgoal_tac "n \ unats (len_of TYPE(machine_word_len))") apply (simp add: word_less_nat_alt) apply (subst unat_minus_one) @@ -6270,7 +6275,8 @@ proof (induct arbitrary: P p rule: finalise_spec_induct2) \ (\zb n cp. cteCap cte = Zombie q zb n \ Q cp \ (isZombie cp \ capZombiePtr cp \ q))" note hyps = "1.hyps"[folded reduceZombie_def[unfolded cteDelete_def finaliseSlot_def]] - have Q: "\x y n. {x :: machine_word} = (\x. y + x * 2^cteSizeBits) ` {0 ..< n} \ n = 1" + have Q: "\x y n. {x :: machine_word} = (\x. y + (x << cteSizeBits)) ` {0 ..< n} \ n = 1" + apply (simp only: shiftl_t2n mult_ac) apply (drule sym) apply (case_tac "1 < n") apply (frule_tac x = "y + 0 * 2^cteSizeBits" in eqset_imp_iff) @@ -6373,14 +6379,15 @@ proof (induct arbitrary: P p rule: finalise_spec_induct2) simp_all add: isCap_simps removeable'_def fun_eq_iff[where f="cte_refs' cap" for cap] fun_eq_iff[where f=tcb_cte_cases] - tcb_cte_cases_def)[1] - apply (frule Q) + tcb_cte_cases_def cteSizeBits_def)[1] + apply (frule Q[unfolded cteSizeBits_def, simplified]) apply clarsimp + apply (simp add: mask_def) apply (subst(asm) R) apply (drule valid_capAligned [OF ctes_of_valid']) apply fastforce apply (simp add: capAligned_def word_bits_def) - apply (frule Q) + apply (frule Q[unfolded cteSizeBits_def, simplified]) apply clarsimp apply (clarsimp simp: cte_wp_at_ctes_of capRemovable_def) apply (subgoal_tac "final_matters' (cteCap rv) \ \ isUntypedCap (cteCap rv)") @@ -7449,7 +7456,7 @@ next apply (rule_tac x="cte_map slot" in exI) apply (clarsimp simp: image_def) apply (rule_tac x="of_nat n" in bexI) - apply (fastforce simp: cte_level_bits_def objBits_defs mult.commute mult.left_commute) + apply (fastforce simp: cte_level_bits_def shiftl_t2n objBits_defs mult.commute mult.left_commute) apply simp apply (subst field_simps, rule plus_one_helper2) apply simp @@ -8486,26 +8493,26 @@ proof apply (erule (1) irq_controlD, rule irq_control) done - show "ioport_control m'" using src dest parency + 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 ioport_control) + 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 ioport_control) + apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) apply simp - apply (frule ioport_revocable, rule ioport_control) + 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 ioport_control) + apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) apply simp - apply (erule (1) ioport_controlD, rule ioport_control) + apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) done have distz: "distinct_zombies m" diff --git a/proof/refine/X64/CSpace1_R.thy b/proof/refine/X64/CSpace1_R.thy index 717408df1e..116366ac8a 100644 --- a/proof/refine/X64/CSpace1_R.thy +++ b/proof/refine/X64/CSpace1_R.thy @@ -212,6 +212,7 @@ lemma tcb_cases_related: "tcb_cap_cases ref = Some (getF, setF, restr) \ \getF' setF'. (\x. tcb_cte_cases (cte_map (x, ref) - x) = Some (getF', setF')) \ (\tcb tcb'. tcb_relation tcb tcb' \ cap_relation (getF tcb) (cteCap (getF' tcb')))" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) by (simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1 cte_map_def' tcb_relation_def split: if_split_asm) @@ -336,10 +337,12 @@ lemma maskCapRights [simp]: lemma maskCap_valid [simp]: "s \' RetypeDecls_H.maskCapRights R cap = s \' cap" - by (simp add: valid_cap'_def maskCapRights_def isCap_simps + apply (simp add: valid_cap'_def maskCapRights_def isCap_simps capAligned_def X64_H.maskCapRights_def split: capability.split arch_capability.split split del: if_split) + apply clarsimp (* FIXME arch-split: unclear why *) + done lemma getSlotCap_valid_cap: "\valid_objs'\ getSlotCap t \\r. valid_cap' r and cte_at' t\" @@ -1496,7 +1499,7 @@ lemma ps_clear_32: \ ksPSpace s (p + 2^cteSizeBits) = None" apply (simp add: ps_clear_def) apply (drule equals0D[where a="p + 2^cteSizeBits"]) - apply (simp add: dom_def add.commute objBits_defs take_bit_Suc) + apply (simp add: dom_def add.commute objBits_defs take_bit_Suc mask_def) apply (drule mp) apply (rule word_plus_mono_right) apply simp @@ -1619,7 +1622,7 @@ lemma tcb_cases_related2: \ (\tcb tcb'. tcb_relation tcb tcb' \ cap_relation (getF' tcb) (cteCap (getF tcb'))) \ (\tcb tcb' cap cte. tcb_relation tcb tcb' \ cap_relation cap (cteCap cte) \ tcb_relation (setF' (\x. cap) tcb) (setF (\x. cte) tcb'))" - apply (clarsimp simp: tcb_cte_cases_def tcb_relation_def cte_level_bits_def + apply (clarsimp simp: tcb_cte_cases_def tcb_relation_def cte_level_bits_def cteSizeBits_def tcb_cap_cases_simps[simplified] split: if_split_asm) apply (simp_all add: tcb_cnode_index_def cte_level_bits_def cte_map_def field_simps to_bl_1) @@ -3752,7 +3755,7 @@ lemma derived_sameRegionAs: apply (clarsimp simp: isCap_simps valid_cap'_def capAligned_def is_aligned_no_overflow capRange_def split: capability.splits arch_capability.splits option.splits) - apply (clarsimp simp: isCap_simps valid_cap'_def + apply (clarsimp simp: isCap_simps valid_cap'_def valid_arch_cap'_def is_aligned_no_overflow capRange_def split: capability.splits arch_capability.splits option.splits) done @@ -4980,6 +4983,8 @@ 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 @@ -4996,6 +5001,21 @@ lemma updateCapFreeIndex_ioport_control: 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 @@ -5048,19 +5068,6 @@ setUntypedCapAsFull (cteCap srcCTE) cap src apply clarsimp 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 - lemma setUntypedCapAsFull_valid_badges: assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" shows @@ -5220,6 +5227,8 @@ lemma mdb_inv_preserve_refl[simp]: "mdb_inv_preserve m m" by (simp add:mdb_inv_preserve_def) +context begin interpretation Arch . (* FIXME arch-split *) + lemma setUntypedCapAsFull_mdb[wp]: "\\s. valid_mdb' s \ cte_wp_at' (\c. c = srcCTE) slot s \ setUntypedCapAsFull (cteCap srcCTE) cap slot @@ -5238,6 +5247,8 @@ lemma setUntypedCapAsFull_mdb[wp]: apply (erule(1) mdb_inv_preserve_updateCap) done +end + lemma (in mdb_insert_abs_sib) next_slot_no_parent': "\valid_list_2 t m; finite_depth m; no_mloop m; m src = None\ \ next_slot p t (m(dest := None)) = next_slot p t m" diff --git a/proof/refine/X64/CSpace_I.thy b/proof/refine/X64/CSpace_I.thy index 511a6e758d..da26dd48aa 100644 --- a/proof/refine/X64/CSpace_I.thy +++ b/proof/refine/X64/CSpace_I.thy @@ -1200,7 +1200,7 @@ lemma cte_refs_capRange: apply simp defer \ \CNodeCap\ - apply (clarsimp simp: objBits_simps capAligned_def dest!: valid_capAligned) + apply (clarsimp simp: objBits_simps capAligned_def shiftl_t2n' mask_def dest!: valid_capAligned) apply (rename_tac word1 nat1 word2 nat2 x) apply (subgoal_tac "x * 2^cteSizeBits < 2 ^ (cteSizeBits + nat1)") apply (intro conjI) @@ -1219,7 +1219,7 @@ lemma cte_refs_capRange: apply (simp add: word_bits_def) \ \Zombie\ apply (rename_tac word zombie_type nat) - apply (clarsimp simp: capAligned_def valid_cap'_def objBits_simps) + apply (clarsimp simp: capAligned_def valid_cap'_def objBits_simps shiftl_t2n' mask_def ) apply (subgoal_tac "xa * 2^cteSizeBits < 2 ^ zBits zombie_type") apply (intro conjI) apply (erule(1) is_aligned_no_wrap') @@ -1419,8 +1419,9 @@ lemma untyped_inc: "untyped_inc' m" and class_links: "class_links m" and irq_control: "irq_control m" and - ioport_control: "ioport_control m" - using valid by (simp add: valid_mdb_ctes_def)+ + arch_mdb_ctes: "valid_arch_mdb_ctes m" (* FIXME arch-split: this should be valid_arch_mdb_ctes *) + using valid + by (simp_all add: valid_mdb_ctes_def) end (* of context vmdb *) @@ -1696,7 +1697,7 @@ lemma untypedRange_not_emptyD: "untypedRange c' \ {} \ is lemma usableRange_subseteq: "\capAligned c';isUntypedCap c'\ \ usableUntypedRange c' \ untypedRange c'" - apply (clarsimp simp:isCap_simps capAligned_def split:if_splits) + apply (clarsimp simp:isCap_simps capAligned_def shiftl_t2n' mask_def field_simps split:if_splits) apply (erule order_trans[OF is_aligned_no_wrap']) apply (erule of_nat_power) apply (simp add:word_bits_def)+ @@ -1796,6 +1797,10 @@ lemma class_links_init: apply (clarsimp simp: mdb_next_unfold) done +(* FIXME arch-split: compatibility shim, can be removed by arch-wide rename *) +abbreviation (input) + "isArchPageCap \ isArchFrameCap" + lemma distinct_zombies_copyE: "\ distinct_zombies m; m x = Some cte; capClass (cteCap cte') = PhysicalClass @@ -2056,7 +2061,7 @@ lemma setCTE_valid_objs'[wp]: apply (clarsimp simp: prod_eq_iff lookupAround2_char1 updateObject_cte in_monad typeError_def valid_obj'_def valid_tcb'_def valid_cte'_def - tcb_cte_cases_def + tcb_cte_cases_def tcb_cte_cases_neqs split: kernel_object.split_asm if_split_asm) done @@ -2093,6 +2098,8 @@ lemma getCTE_ctes_wp: lemma updateMDB_valid_objs'[wp]: "\valid_objs'\ updateMDB m p \\rv. valid_objs'\" apply (clarsimp simp add: updateMDB_def) +apply (wp setCTE_valid_objs') + apply (wp | simp)+ done diff --git a/proof/refine/X64/CSpace_R.thy b/proof/refine/X64/CSpace_R.thy index f6a4384519..a61db81a45 100644 --- a/proof/refine/X64/CSpace_R.thy +++ b/proof/refine/X64/CSpace_R.thy @@ -1405,21 +1405,22 @@ 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: - "ioport_control n" + "X64.ioport_control n" using src dest partial_is_derived' - apply (clarsimp simp: ioport_control_def) + 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 ioport_revocable, rule ioport_control) + 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) ioport_controlD, rule ioport_control) + apply (erule (1) X64.ioport_controlD, rule arch_mdb_ctes[simplified X64.valid_arch_mdb_ctes_def]) done context mdb_insert_child @@ -2613,10 +2614,10 @@ lemma setCTE_ko_wp_at_live[wp]: elim!: rsubst[where P=P]) apply (drule(1) updateObject_cte_is_tcb_or_cte [OF _ refl, rotated]) apply (elim exE conjE disjE) - apply (clarsimp simp: ps_clear_upd objBits_simps + apply (clarsimp simp: ps_clear_upd objBits_simps live'_def hyp_live'_def lookupAround2_char1) apply (simp add: tcb_cte_cases_def split: if_split_asm) - apply (clarsimp simp: ps_clear_upd objBits_simps) + apply (clarsimp simp: ps_clear_upd objBits_simps live'_def) done lemma setCTE_iflive': @@ -2674,10 +2675,10 @@ lemma setCTE_ko_wp_at_not_live[wp]: elim!: rsubst[where P=P]) apply (drule(1) updateObject_cte_is_tcb_or_cte [OF _ refl, rotated]) apply (elim exE conjE disjE) - apply (clarsimp simp: ps_clear_upd objBits_simps + apply (clarsimp simp: ps_clear_upd objBits_simps live'_def hyp_live'_def lookupAround2_char1) apply (simp add: tcb_cte_cases_def split: if_split_asm) - apply (clarsimp simp: ps_clear_upd objBits_simps) + apply (clarsimp simp: ps_clear_upd objBits_simps live'_def) done lemma setUntypedCapAsFull_ko_wp_not_at'[wp]: @@ -3304,7 +3305,7 @@ lemma usableUntypedRange_empty: apply (rule_tac x="2 ^ capBlockSize cp - 1" in word_of_nat_le) apply (simp add: unat_2p_sub_1 untypedBits_defs) apply (simp add: field_simps is_aligned_no_overflow) - apply (simp add: field_simps) + apply (simp add: field_simps mask_def) done lemma restrict_map_is_map_comp: @@ -3318,7 +3319,7 @@ lemma untypedZeroRange_to_usableCapRange: apply (clarsimp simp: untypedZeroRange_def split: if_split_asm) apply (frule(1) usableUntypedRange_empty) apply (clarsimp simp: isCap_simps valid_cap_simps' max_free_index_def) - apply (simp add: getFreeRef_def) + apply (simp add: getFreeRef_def mask_def add_diff_eq) done lemma untyped_ranges_zero_delta: @@ -4349,6 +4350,7 @@ lemma setupReplyMaster_invs'[wp]: "\invs' and tcb_at' t and ex_nonz_cap_to' t\ setupReplyMaster t \\rv. invs'\" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (simp add: invs'_def valid_state'_def) apply (rule hoare_pre) apply (wp setupReplyMaster_valid_pspace' sch_act_wf_lift tcb_in_cur_domain'_lift ct_idle_or_in_cur_domain'_lift @@ -4709,7 +4711,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 ioport_control) + apply (erule ioport_revocable, rule arch_mdb_ctes[simplified]) done lemma new_child [simp]: @@ -5738,7 +5740,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 ioport_control) + apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) apply simp done @@ -5953,6 +5955,8 @@ 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) @@ -5960,15 +5964,17 @@ lemma ioport' [simp]: apply (drule n'_rev) apply (clarsimp split: if_split_asm) apply (simp add: is_simple_cap'_def isCap_simps) - apply (frule ioport_revocable, rule ioport_control) + 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 ioport_control) + 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) @@ -6006,7 +6012,7 @@ lemma updateCapFreeIndex_no_0: apply (simp add:cte_wp_at_ctes_of)+ apply (rule mdb_inv_preserve_updateCap) apply (clarsimp simp:cte_wp_at_ctes_of)+ -done + done context begin interpretation Arch . (*FIXME: arch-split*) @@ -6124,16 +6130,14 @@ lemma locateSlot_cap_to'[wp]: "\\s. isCNodeCap cap \ (\r \ cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\ locateSlotCNode (capCNodePtr cap) n (v && mask (capCNodeBits cap)) \ex_cte_cap_wp_to' P\" - apply (simp add: locateSlot_conv) + apply (simp add: locateSlot_conv shiftl_t2n') apply wp apply (clarsimp dest!: isCapDs valid_capAligned - simp: objBits_simps' mult.commute capAligned_def cte_level_bits_def) + simp: objBits_simps' mult.commute capAligned_def cte_level_bits_def shiftl_t2n') apply (erule bspec) apply (case_tac "bits < word_bits") - apply simp - apply (rule and_mask_less_size) - apply (simp add: word_bits_def word_size) - apply (simp add: power_overflow word_bits_def) + apply (simp add: word_and_le1) + apply (simp add: power_overflow word_bits_def word_and_le1) done lemma rab_cap_to'': diff --git a/proof/refine/X64/Detype_R.thy b/proof/refine/X64/Detype_R.thy index 74a6c24d25..62401110d4 100644 --- a/proof/refine/X64/Detype_R.thy +++ b/proof/refine/X64/Detype_R.thy @@ -405,13 +405,13 @@ lemma cte_wp_at_delete': apply (drule(1) aligned_ranges_subset_or_disjoint) apply (subgoal_tac "{p, p - n} \ obj_range' (p - n) (KOTCB obj)") apply (clarsimp simp del: atLeastAtMost_iff - simp: field_simps objBits_simps obj_range'_def) + simp: field_simps objBits_simps obj_range'_def mask_def) apply fastforce - apply (simp add: obj_range'_def mask_in_range[symmetric] + apply (simp add: obj_range'_def neg_mask_in_mask_range[symmetric] del: atLeastAtMost_iff) apply (simp add: objBits_simps) apply (frule(1) tcb_cte_cases_aligned_helpers) - apply (simp add: is_aligned_neg_mask_eq) + apply simp done lemma map_to_ctes_delete: @@ -911,7 +911,7 @@ lemma detype_tcbSchedNexts_of: apply (clarsimp simp: opt_map_def) apply (rule ext) apply (rename_tac s) - apply (clarsimp simp: ko_wp_at'_def split: option.splits) + apply (clarsimp simp: ko_wp_at'_def live'_def split: option.splits) apply (drule_tac x=s in spec) apply force done @@ -925,7 +925,7 @@ lemma detype_tcbSchedPrevs_of: apply (clarsimp simp: opt_map_def) apply (rule ext) apply (rename_tac s) - apply (clarsimp simp: ko_wp_at'_def split: option.splits) + apply (clarsimp simp: ko_wp_at'_def live'_def split: option.splits) apply (drule_tac x=s in spec) apply force done @@ -939,7 +939,7 @@ lemma detype_inQ: apply (clarsimp simp: opt_map_def) apply (rule ext) apply (rename_tac s) - apply (clarsimp simp: inQ_def opt_pred_def ko_wp_at'_def split: option.splits) + apply (clarsimp simp: inQ_def opt_pred_def ko_wp_at'_def live'_def split: option.splits) apply (drule_tac x=s in spec) apply force done @@ -1121,22 +1121,23 @@ lemma valid_obj': apply fastforce apply simp apply (intro conjI) + apply (rename_tac tcb) + apply (case_tac "tcbState tcb"; clarsimp simp: valid_tcb_state'_def dest!: refs_notRange) apply (rename_tac tcb) - apply (case_tac "tcbState tcb"; clarsimp simp: valid_tcb_state'_def dest!: refs_notRange) - apply (rename_tac tcb) - apply (case_tac "tcbState tcb"; - clarsimp simp: valid_tcb_state'_def valid_bound_ntfn'_def - dest!: refs_notRange split: option.splits) + apply (case_tac "tcbState tcb"; + clarsimp simp: valid_tcb_state'_def valid_bound_ntfn'_def + dest!: refs_notRange split: option.splits) + apply (clarsimp simp: none_top_bool_cases) + apply (rename_tac prev) + apply (cut_tac P=live' and p=prev in live_notRange; fastforce?) + apply (fastforce dest: sym_heapD2[where p'=p] + simp: opt_map_def ko_wp_at'_def obj_at'_def live'_def projectKOs) apply (clarsimp simp: none_top_bool_cases) - apply (rename_tac prev) - apply (cut_tac P=live' and p=prev in live_notRange; fastforce?) - apply (fastforce dest: sym_heapD2[where p'=p] - simp: opt_map_def ko_wp_at'_def obj_at'_def projectKOs) - apply (clarsimp simp: none_top_bool_cases) - apply (rename_tac "next") - apply (cut_tac P=live' and p="next" in live_notRange; fastforce?) - apply (fastforce dest!: sym_heapD1[where p=p] - simp: opt_map_def ko_wp_at'_def obj_at'_def projectKOs) + apply (rename_tac "next") + apply (cut_tac P=live' and p="next" in live_notRange; fastforce?) + apply (fastforce dest!: sym_heapD1[where p=p] + simp: opt_map_def ko_wp_at'_def obj_at'_def live'_def projectKOs) + apply (clarsimp simp: valid_arch_tcb'_def) apply (clarsimp simp: valid_cte'_def) apply (rule_tac p=p in valid_cap2) apply (clarsimp simp: ko_wp_at'_def objBits_simps' cte_level_bits_def[symmetric]) @@ -1168,7 +1169,7 @@ lemma tcbSchedNexts_of_pspace': apply (case_tac "ksPSpace s' p"; clarsimp) apply (rename_tac obj) apply (case_tac "tcb_of' obj"; clarsimp) - apply (clarsimp simp: ko_wp_at'_def obj_at'_def) + apply (clarsimp simp: ko_wp_at'_def obj_at'_def live'_def) apply (fastforce simp: pspace_alignedD' pspace_distinctD') apply (clarsimp simp: opt_map_def split: option.splits) done @@ -1185,14 +1186,15 @@ lemma tcbSchedPrevs_of_pspace': apply (case_tac "ksPSpace s' p"; clarsimp) apply (rename_tac obj) apply (case_tac "tcb_of' obj"; clarsimp) - apply (clarsimp simp: ko_wp_at'_def obj_at'_def) + apply (clarsimp simp: ko_wp_at'_def obj_at'_def live'_def) apply (fastforce simp: pspace_alignedD' pspace_distinctD') apply (clarsimp simp: opt_map_def split: option.splits) done lemma st_tcb: "\P p. \ st_tcb_at' P p s'; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" - by (fastforce simp: pred_tcb_at'_def obj_at'_real_def projectKOs dest: live_notRange) + by (fastforce simp: pred_tcb_at'_def obj_at'_real_def projectKOs live'_def hyp_live'_def + dest: live_notRange) lemma irq_nodes_global: "\irq :: 8 word. irq_node' s + (ucast irq) * 32 \ global_refs' s" (*2^cte_level_bits *) @@ -1233,7 +1235,7 @@ proof - apply (frule valid_capAligned) apply (case_tac "\irq. cteCap c = IRQHandlerCap irq") apply (insert irq_nodes_range)[1] - apply clarsimp + apply (clarsimp simp: cteSizeBits_def shiftl_t2n') apply (frule subsetD [OF cte_refs_capRange]) apply simp apply assumption @@ -1569,7 +1571,9 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def show "valid_irq_node' (irq_node' s') ?s" using virq irq_nodes_range - by (simp add: valid_irq_node'_def mult.commute mult.left_commute ucast_ucast_mask_8) + (* FIXME arch-split: where is the mismatch between cteSizeBits/shifts and actual numbers? *) + by (simp add: valid_irq_node'_def mult.commute mult.left_commute ucast_ucast_mask_8 + cteSizeBits_def shiftl_t2n') show "valid_irq_handlers' ?s" using virqh apply (simp add: valid_irq_handlers'_def irq_issued'_def @@ -1583,7 +1587,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def by (clarsimp simp: irq_control_def) from ioport_ctrl - show "ioport_control ?ctes'" + show "valid_arch_mdb_ctes ?ctes'" by (clarsimp simp: ioport_control_def) from dist_z @@ -1657,7 +1661,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def apply (frule if_live_then_nonz_capE'[OF iflive, OF ko_wp_at'_weakenE]) apply (clarsimp simp: projectKOs) apply (case_tac "tcbState obj") - apply (clarsimp simp: projectKOs)+ + apply (clarsimp simp: projectKOs live'_def)+ apply (clarsimp dest!: ex_nonz_cap_notRange) done @@ -1675,7 +1679,7 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def apply (frule if_live_then_nonz_capE'[OF iflive, OF ko_wp_at'_weakenE]) apply (clarsimp simp: projectKOs) apply (case_tac "tcbState obj") - apply (clarsimp simp: projectKOs)+ + apply (clarsimp simp: projectKOs live'_def)+ apply (clarsimp dest!: ex_nonz_cap_notRange elim!: ko_wp_at'_weakenE) done @@ -1834,7 +1838,7 @@ lemma deleteObjects_st_tcb_at': apply (rule conjI) apply (fastforce elim: ko_wp_at'_weakenE) apply (erule if_live_then_nonz_capD' [rotated]) - apply (clarsimp simp: projectKOs) + apply (clarsimp simp: projectKOs live'_def) apply (clarsimp simp: invs'_def valid_state'_def) apply (clarsimp simp: pred_tcb_at'_def obj_at'_real_def field_simps ko_wp_at'_def ps_clear_def @@ -1869,11 +1873,12 @@ lemma deleteObjects_cap_to': apply (simp add: delete_locale_def) done +(* FIXME arch-split: consider "- mask_range ptr bits" in conclusion *) lemma valid_untyped_no_overlap: "\ valid_untyped' d ptr bits idx s; is_aligned ptr bits; valid_pspace' s \ \ pspace_no_overlap' ptr bits (s\ksPSpace := ksPSpace s |` (- {ptr .. ptr + 2 ^ bits - 1})\)" apply (clarsimp simp del: atLeastAtMost_iff - simp: pspace_no_overlap'_def valid_cap'_def valid_untyped'_def is_aligned_neg_mask_eq) + simp: pspace_no_overlap'_def valid_cap'_def valid_untyped'_def) apply (drule_tac x=x in spec) apply (drule restrict_map_Some_iff[THEN iffD1]) apply clarsimp @@ -1885,10 +1890,10 @@ lemma valid_untyped_no_overlap: apply (drule (1) aligned_ranges_subset_or_disjoint) apply (clarsimp simp del: Int_atLeastAtMost atLeastAtMost_iff atLeastatMost_subset_iff) apply (elim disjE) - apply (subgoal_tac "ptr \ {x..x + 2 ^ objBitsKO ko - 1}") - apply (clarsimp simp:p_assoc_help) - apply (clarsimp simp:p_assoc_help) - apply fastforce+ + apply (subgoal_tac "ptr \ mask_range x (objBitsKO ko)") + apply (clarsimp simp:p_assoc_help mask_def) + apply (clarsimp simp:p_assoc_help mask_def) + apply (fastforce simp: mask_def add_diff_eq)+ done lemma deleteObject_no_overlap[wp]: @@ -2619,11 +2624,11 @@ lemma placeNewObject_modify_commute: apply (case_tac "x = ptr'") apply (subgoal_tac "objBitsKO koa = objBitsKO ko") apply (drule(1) pspace_no_overlapD') - apply (clarsimp simp:field_simps) + apply (clarsimp simp:field_simps mask_def) apply (clarsimp) apply (drule_tac x = x and s = s in pspace_no_overlapD'[rotated]) apply (simp) - apply (clarsimp simp:field_simps) + apply (clarsimp simp:field_simps mask_def) apply (subgoal_tac "pspace_aligned' (ksPSpace_update (\ps. ps(ptr' \ f (ps ptr'))) s)") prefer 2 @@ -2769,10 +2774,10 @@ lemma getPDE_det: apply (rule conjI) apply (subst add.commute) apply (rule word_diff_ls') - apply (clarsimp simp: not_le plus_one_helper) + apply (clarsimp simp: not_le plus_one_helper mask_def) apply (subst add.commute) - apply (simp add: is_aligned_no_wrap' is_aligned_mask) - apply auto + apply (subst is_aligned_no_wrap'[simplified is_aligned_mask], assumption; simp add: mask_def) + apply auto done lemma in_dom_eq: @@ -2915,9 +2920,9 @@ lemma modify_pde_psp_no_overlap': apply (intro allI impI) apply (clarsimp split:if_splits) apply (drule(1) pspace_no_overlapD') - apply (simp add:objBits_simps archObjSize_def field_simps) + apply (simp add:objBits_simps archObjSize_def field_simps mask_def) apply (drule(1) pspace_no_overlapD')+ - apply (simp add:field_simps) + apply (simp add:field_simps mask_def) done qed @@ -3054,11 +3059,10 @@ lemma getPML4E_det: apply (rule conjI) apply (subst add.commute) apply (rule word_diff_ls') - apply (clarsimp simp:field_simps not_le plus_one_helper) + apply (clarsimp simp:field_simps not_le plus_one_helper mask_def) apply (subst add.commute) - apply (simp add: is_aligned_no_wrap' is_aligned_mask) - apply simp - apply auto + apply (subst is_aligned_no_wrap'[simplified is_aligned_mask], assumption; simp add: mask_def) + apply auto done lemma setCTE_pml4e_at': @@ -3257,9 +3261,9 @@ lemma modify_pml4e_psp_no_overlap': apply (intro allI impI) apply (clarsimp split:if_splits) apply (drule(1) pspace_no_overlapD') - apply (simp add:objBits_simps archObjSize_def field_simps) + apply (simp add:objBits_simps archObjSize_def field_simps mask_def) apply (drule(1) pspace_no_overlapD')+ - apply (simp add:field_simps) + apply (simp add:field_simps mask_def) done qed @@ -3570,8 +3574,8 @@ lemma getTCB_det: apply (rule conjI) apply (subst add.commute) apply (rule word_diff_ls') - apply (clarsimp simp:field_simps not_le plus_one_helper) - apply (simp add:field_simps is_aligned_no_wrap' is_aligned_mask) + apply (clarsimp simp:field_simps not_le plus_one_helper mask_def) + apply (simp add:field_simps is_aligned_no_overflow_mask flip: is_aligned_mask) apply simp apply auto done @@ -3704,7 +3708,7 @@ lemma placeNewObject_tcb_at': apply (wp unless_wp |wpc | simp add:alignError_def)+ by (auto simp: obj_at'_def is_aligned_mask lookupAround2_None1 lookupAround2_char1 field_simps objBits_simps - projectKO_opt_tcb projectKO_def return_def ps_clear_def + projectKO_opt_tcb projectKO_def return_def ps_clear_def add_mask_fold split: if_splits dest!: pspace_no_overlap_disjoint') @@ -3828,8 +3832,7 @@ lemma ctes_of_ko_at: (\ptr ko. (ksPSpace s ptr = Some ko \ p \ obj_range' ptr ko))" apply (clarsimp simp: map_to_ctes_def Let_def split: if_split_asm) apply (intro exI conjI, assumption) - apply (simp add: obj_range'_def objBits_simps' add.commute) - apply (simp add: is_aligned_no_wrap') + apply (simp add: obj_range'_def objBits_simps' is_aligned_no_overflow_mask) apply (intro exI conjI, assumption) apply (clarsimp simp: objBits_simps' obj_range'_def word_and_le2) apply (thin_tac "P" for P)+ @@ -3845,7 +3848,7 @@ lemma pspace_no_overlapD2': apply clarsimp apply (drule(1) pspace_no_overlapD') apply (erule in_empty_interE) - apply (simp add:obj_range'_def) + apply (simp add:obj_range'_def add_mask_fold) apply clarsimp apply (subst is_aligned_neg_mask_eq[symmetric]) apply simp @@ -4204,7 +4207,7 @@ proof - apply (rule is_aligned_shiftl_self) apply (simp add:range_cover_def) apply simp - apply (simp add:word_le_sub1 shiftl_t2n field_simps) + apply (simp add:word_le_sub1 shiftl_t2n field_simps mask_def) done qed @@ -4283,29 +4286,27 @@ lemma pspace_no_overlap'_le: assumes b: "sz < word_bits" shows "pspace_no_overlap' ptr sz' s" proof - - note blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff - Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex + note no_simps [simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff + atLeastatMost_subset_iff atLeastLessThan_iff + Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex have diff_cancel: "\a b c. (a::machine_word) + b - c = b + (a - c)" by simp - have bound :"(ptr && ~~ mask sz') - (ptr && ~~ mask sz) \ 2 ^ sz - 2 ^ sz'" - by (rule neg_mask_diff_bound[OF psp(2)]) + have bound: "(ptr && ~~ mask sz') - (ptr && ~~ mask sz) \ mask sz - mask sz'" + using neg_mask_diff_bound[OF psp(2)] + by (simp add: mask_def) show ?thesis - using psp + using psp apply (clarsimp simp:pspace_no_overlap'_def) apply (drule_tac x = x in spec) apply clarsimp apply (erule disjoint_subset2[rotated]) - apply (clarsimp simp:blah) - apply (rule word_plus_mcs[OF _ is_aligned_no_overflow']) + apply (clarsimp simp: no_simps) + apply (rule word_plus_mcs[OF _ is_aligned_no_overflow_mask]) apply (simp add:diff_cancel p_assoc_help) apply (rule le_plus) - apply (simp add:field_simps) apply (rule bound) - apply (rule word_le_minus_mono_left) - apply (erule two_power_increasing[OF _ b[unfolded word_bits_def]]) - apply (rule word_1_le_power) - using b[unfolded word_bits_def] apply simp - apply (simp add:is_aligned_neg_mask) + apply (erule mask_mono) + apply simp done qed @@ -5028,7 +5029,7 @@ proof - apply (drule(1) pspace_no_overlapD') apply (subst (asm) range_cover_tail_mask) apply simp+ - apply (simp add:word_le_sub1 shiftl_t2n field_simps) + apply (simp add:word_le_sub1 shiftl_t2n field_simps mask_def) apply auto done qed diff --git a/proof/refine/X64/Finalise_R.thy b/proof/refine/X64/Finalise_R.thy index 7a86169c7b..8774905fa1 100644 --- a/proof/refine/X64/Finalise_R.thy +++ b/proof/refine/X64/Finalise_R.thy @@ -1066,11 +1066,11 @@ lemma ioport_control_n [simp]: "ioport_control n" apply (frule n_revokable) apply (drule n_cap) apply (clarsimp split: if_split_asm) - apply (frule ioport_revocable, rule ioport_control) + 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 ioport_control) + apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) done lemma reply_masters_rvk_fb_m: "reply_masters_rvk_fb m" @@ -2090,9 +2090,10 @@ lemma isFinal_no_descendants: apply (simp add: valid_mdb'_def) done +(* FIXME arch-split: locale+Arch combination *) lemma (in vmdb) isFinal_untypedParent: assumes x: "m slot = Some cte" "isFinal (cteCap cte) slot (option_map cteCap o m)" - "final_matters' (cteCap cte) \ \ isIRQHandlerCap (cteCap cte) \ \ isArchIOPortCap (cteCap cte)" + "final_matters' (cteCap cte) \ \ isIRQHandlerCap (cteCap cte) \ \ X64.isArchIOPortCap (cteCap cte)" shows "m \ x \ slot \ (\cte'. m x = Some cte' \ isUntypedCap (cteCap cte') \ RetypeDecls_H.sameRegionAs (cteCap cte') (cteCap cte))" @@ -2414,10 +2415,10 @@ lemma unbindNotification_invs[wp]: apply (auto split: if_split_asm)[1] apply (auto simp: tcb_st_not_Bound ntfn_q_refs_of'_mult split: if_split_asm)[1] apply (frule obj_at_valid_objs', clarsimp+) - apply (simp add: valid_ntfn'_def valid_obj'_def projectKOs + apply (simp add: valid_ntfn'_def valid_obj'_def projectKOs live'_def split: ntfn.splits) apply (erule if_live_then_nonz_capE') - apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs) + apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs live'_def) done lemma ntfn_bound_tcb_at': @@ -2449,7 +2450,7 @@ lemma unbindMaybeNotification_invs[wp]: defer 7 apply (fold_subgoals (prefix))[8] subgoal premises prems using prems by (auto simp: pred_tcb_at' valid_pspace'_def projectKOs valid_obj'_def valid_ntfn'_def - ko_wp_at'_def + ko_wp_at'_def live'_def elim!: obj_atE' valid_objsE' if_live_then_nonz_capE' split: option.splits ntfn.splits) apply (rule delta_sym_refs, assumption) @@ -2527,7 +2528,7 @@ lemma deleteASID_invs'[wp]: apply clarsimp apply (auto dest!: ran_del_subset)[1] apply (wp getObject_valid_obj getObject_inv loadObject_default_inv - | simp add: objBits_simps archObjSize_def pageBits_def)+ + | simp add: X64.objBits_simps archObjSize_def pageBits_def)+ apply clarsimp done @@ -2662,7 +2663,8 @@ lemma deletingIRQHandler_removeable': apply (subst tree_cte_cteCap_eq[unfolded o_def])+ apply (wp hoare_use_eq_irq_node' [OF cteDeleteOne_irq_node' cteDeleteOne_cteCaps_of] getCTE_wp') - apply (clarsimp simp: cte_level_bits_def ucast_nat_def split: option.split_asm) + apply (clarsimp simp: cte_level_bits_def ucast_nat_def shiftl_t2n mult_ac cteSizeBits_def + split: option.split_asm) done lemma finaliseCap_cte_refs: @@ -2680,7 +2682,7 @@ lemma finaliseCap_cte_refs: apply clarsimp apply (rule ext, simp) apply (rule image_cong [OF _ refl]) - apply (fastforce simp: capAligned_def objBits_simps shiftL_nat) + apply (fastforce simp: capAligned_def objBits_simps shiftL_nat mask_def) done lemma deletingIRQHandler_final: @@ -2698,7 +2700,7 @@ declare suspend_unqueued [wp] lemma unbindNotification_valid_objs'_helper: "valid_tcb' tcb s \ valid_tcb' (tcbBoundNotification_update (\_. None) tcb) s " - by (clarsimp simp: valid_bound_ntfn'_def valid_tcb'_def tcb_cte_cases_def + by (clarsimp simp: valid_bound_ntfn'_def valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs split: option.splits ntfn.splits) lemma unbindNotification_valid_objs'_helper': @@ -2895,7 +2897,7 @@ lemma tcbQueueRemove_tcbSchedNext_tcbSchedPrev_None_obj_at': apply (wpsimp wp: threadSet_wp getTCB_wp) by (fastforce dest!: heap_ls_last_None simp: list_queue_relation_def prev_queue_head_def queue_end_valid_def - obj_at'_def opt_map_def ps_clear_def objBits_simps + obj_at'_def opt_map_def ps_clear_def X64.objBits_simps split: if_splits) lemma tcbSchedDequeue_tcbSchedNext_tcbSchedPrev_None_obj_at': @@ -2962,7 +2964,7 @@ lemma (in delete_one_conc_pre) finaliseCap_replaceable: apply (frule cte_wp_at_valid_objs_valid_cap', clarsimp+) apply (case_tac "cteCap cte", simp_all add: isCap_simps capRange_def cap_has_cleanup'_def - final_matters'_def objBits_simps + final_matters'_def X64.objBits_simps not_Final_removeable finaliseCap_def, simp_all add: removeable'_def) (* thread *) @@ -3245,6 +3247,8 @@ end global_interpretation delete_one_conc_pre by (unfold_locales, wp) (wp cteDeleteOne_tcbDomain_obj_at' cteDeleteOne_typ_at' cteDeleteOne_reply_pred_tcb_at | simp)+ +context begin interpretation Arch . (*FIXME: arch-split*) + lemma cteDeleteOne_invs[wp]: "\invs'\ cteDeleteOne ptr \\rv. invs'\" apply (simp add: cteDeleteOne_def unless_def @@ -3268,12 +3272,14 @@ lemma cteDeleteOne_invs[wp]: apply (rule conjI) subgoal by auto subgoal by (auto dest!: isCapDs simp: pred_tcb_at'_def obj_at'_def projectKOs - ko_wp_at'_def) + live'_def hyp_live'_def ko_wp_at'_def) apply (wp isFinalCapability_inv getCTE_wp' hoare_weak_lift_imp | wp (once) isFinal[where x=ptr])+ apply (fastforce simp: cte_wp_at_ctes_of) done +end + global_interpretation delete_one_conc_fr: delete_one_conc by unfold_locales wp @@ -3361,7 +3367,7 @@ lemma finaliseCap_valid_cap[wp]: apply simp apply (intro conjI impI) apply (clarsimp simp: valid_cap'_def isCap_simps capAligned_def - objBits_simps shiftL_nat)+ + X64.objBits_simps shiftL_nat)+ done @@ -3513,6 +3519,7 @@ lemma unbindMaybeNotification_corres: apply (rule corres_option_split) apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) apply (rule corres_return_trivial) + apply simp apply (rule corres_split[OF setNotification_corres]) apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) apply (rule setBoundNotification_corres) @@ -3622,7 +3629,7 @@ lemma finaliseCap_corres: apply (rule corres_guard_imp) apply (rule corres_split[OF unbindMaybeNotification_corres]) apply (rule cancelAllSignals_corres) - apply (wp abs_typ_at_lifts unbind_maybe_notification_invs typ_at_lifts hoare_drop_imps hoare_vcg_all_lift | wpc)+ + apply (wp abs_typ_at_lifts unbind_maybe_notification_invs gen_typ_at_lifts hoare_drop_imps hoare_vcg_all_lift | wpc)+ apply (clarsimp simp: valid_cap_def) apply (clarsimp simp: valid_cap'_def) apply (fastforce simp: final_matters'_def shiftL_nat zbits_map_def) diff --git a/proof/refine/X64/InterruptAcc_R.thy b/proof/refine/X64/InterruptAcc_R.thy index 87442c03e2..29a039db26 100644 --- a/proof/refine/X64/InterruptAcc_R.thy +++ b/proof/refine/X64/InterruptAcc_R.thy @@ -68,7 +68,7 @@ lemma getIRQSlot_real_cte[wp]: apply (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv) apply wp apply (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def - cte_level_bits_def ucast_nat_def) + cte_level_bits_def ucast_nat_def cteSizeBits_def shiftl_t2n) done lemma getIRQSlot_cte_at[wp]: diff --git a/proof/refine/X64/Interrupt_R.thy b/proof/refine/X64/Interrupt_R.thy index f9937b0c73..755fdc12ee 100644 --- a/proof/refine/X64/Interrupt_R.thy +++ b/proof/refine/X64/Interrupt_R.thy @@ -461,7 +461,7 @@ lemma invoke_irq_handler_invs'[wp]: apply clarsimp+ apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_to'_def isCap_simps untyped_derived_eq_def) - apply (fastforce simp: cte_level_bits_def badge_derived'_def)+ + apply (fastforce simp: cte_level_bits_def badge_derived'_def cteSizeBits_def shiftl_t2n) done lemma IRQHandler_valid': @@ -835,13 +835,13 @@ lemma updateTimeSlice_valid_pspace[wp]: "\valid_pspace'\ threadSet (tcbTimeSlice_update (\_. ts')) thread \\r. valid_pspace'\" apply (wp threadSet_valid_pspace'T) - apply (auto simp:tcb_cte_cases_def) + apply (auto simp: tcb_cte_cases_def tcb_cte_cases_neqs) done (* catch up tcbSchedAppend to tcbSchedEnqueue, which has these from crunches on possibleSwitchTo *) crunch tcbSchedAppend for irq_handlers'[wp]: valid_irq_handlers' - (simp: unless_def tcb_cte_cases_def wp: crunch_wps) + (simp: unless_def tcb_cte_cases_def tcb_cte_cases_neqs wp: crunch_wps) crunch tcbSchedAppend for irqs_masked'[wp]: irqs_masked' (simp: unless_def wp: crunch_wps) diff --git a/proof/refine/X64/InvariantUpdates_H.thy b/proof/refine/X64/InvariantUpdates_H.thy index b24ab1932d..96e3b1f4da 100644 --- a/proof/refine/X64/InvariantUpdates_H.thy +++ b/proof/refine/X64/InvariantUpdates_H.thy @@ -5,11 +5,122 @@ *) theory InvariantUpdates_H -imports Invariants_H +imports ArchInvsLemmas_H begin +(* generic consequences which require arch-specific proofs from ArchInvsLemmas_H *) +arch_requalify_facts + cte_wp_atE' + cte_wp_at_cteI' + tcb_at_cte_at' + typ_at_lift_valid_cap' + valid_arch_tcb_lift' + tcb_at_cte_at' + gen_objBitsT_simps + objBitsT_koTypeOf (* FIXME arch-split: consider declaring [simp] here rather than Schedule_R *) + +(* arch-specific typ_at_lifts in Arch *) (* FIXME arch-split: currently unused *) +lemmas gen_typ_at_lifts = + typ_at_lift_tcb' typ_at_lift_ep' typ_at_lift_ntfn' typ_at_lift_cte' typ_at_lift_cte_at' + typ_at_lift_valid_untyped' typ_at_lift_valid_cap' valid_bound_tcb_lift + valid_arch_tcb_lift' + +(* these depend on interpretations in ArchInvLemmas_H *) +context pspace_update_eq' +begin + +lemma valid_space_update [iff]: + "valid_pspace' (f s) = valid_pspace' s" + by (fastforce simp: valid_pspace' pspace) + +lemma cte_wp_at_update [iff]: + "cte_wp_at' P p (f s) = cte_wp_at' P p s" + by (fastforce intro: cte_wp_at'_pspaceI simp: pspace) + +lemma ex_nonz_cap_to_eq'[iff]: + "ex_nonz_cap_to' p (f s) = ex_nonz_cap_to' p s" + by (simp add: ex_nonz_cap_to'_def) + +lemma iflive_update [iff]: + "if_live_then_nonz_cap' (f s) = if_live_then_nonz_cap' s" + by (simp add: if_live_then_nonz_cap'_def ex_nonz_cap_to'_def) + +lemma valid_objs_update [iff]: + "valid_objs' (f s) = valid_objs' s" + apply (simp add: valid_objs'_def pspace) + apply (fastforce intro: valid_obj'_pspaceI simp: pspace) + done + +lemma valid_cap_update [iff]: + "(f s) \' c = s \' c" + by (auto intro: valid_cap'_pspaceI simp: pspace) + +(* exports from Arch locale version (safe for generic use) *) +interpretation Arch_pspace_update_eq' .. + +lemmas pspace_in_kernel_mappings_update'[iff] = pspace_in_kernel_mappings_update' + +end + +context Arch_p_arch_idle_update_eq' +begin + +lemma valid_arch_state_update' [iff]: + "valid_arch_state' (f s) = valid_arch_state' s" + by (simp add: valid_arch_state'_def arch cong: option.case_cong) + +end + +context p_arch_idle_update_eq' +begin + +lemma ifunsafe_update [iff]: + "if_unsafe_then_cap' (f s) = if_unsafe_then_cap' s" + by (simp add: if_unsafe_then_cap'_def ex_cte_cap_to'_def int_nd) + +(* exports from Arch locale version (safe for generic use) *) +interpretation Arch_p_arch_idle_update_eq' .. + +lemmas valid_arch_state_update'[iff] = valid_arch_state_update' + +end + + (* FIXME: use locales to shorten this work *) +(* FIXME arch-split: MOVE, or try make generic *) +context Arch begin arch_global_naming + +lemma invs'_gsCNodes_update[simp]: + "invs' (gsCNodes_update f s') = invs' s'" + apply (clarsimp simp: invs'_def valid_state'_def valid_bitmaps_def bitmapQ_defs + valid_irq_node'_def valid_irq_handlers'_def irq_issued'_def irqs_masked'_def + valid_machine_state'_def cur_tcb'_def) + apply (cases "ksSchedulerAction s'"; + simp add: ct_in_state'_def tcb_in_cur_domain'_def ct_idle_or_in_cur_domain'_def + ct_not_inQ_def) + done + +lemma invs'_gsUserPages_update[simp]: + "invs' (gsUserPages_update f s') = invs' s'" + apply (clarsimp simp: invs'_def valid_state'_def valid_bitmaps_def bitmapQ_defs + valid_irq_node'_def valid_irq_handlers'_def irq_issued'_def irqs_masked'_def + valid_machine_state'_def cur_tcb'_def) + apply (cases "ksSchedulerAction s'"; + simp add: ct_in_state'_def tcb_in_cur_domain'_def ct_idle_or_in_cur_domain'_def + ct_not_inQ_def) + done + +end + +(* FIXME arch-split: locale interface? *) +arch_requalify_facts + invs'_gsCNodes_update + invs'_gsUserPages_update + +lemmas [simp] = invs'_gsCNodes_update invs'_gsUserPages_update + + lemma ps_clear_domE[elim?]: "\ ps_clear x n s; dom (ksPSpace s) = dom (ksPSpace s') \ \ ps_clear x n s'" by (simp add: ps_clear_def) @@ -90,15 +201,43 @@ lemma inQ_context[simp]: lemma valid_tcb'_tcbQueued[simp]: "valid_tcb' (tcbQueued_update f tcb) = valid_tcb' tcb" - by (cases tcb, rule ext, simp add: valid_tcb'_def tcb_cte_cases_def cteSizeBits_def) + by (cases tcb, rule ext, simp add: valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs) lemma valid_tcb'_tcbFault_update[simp]: "valid_tcb' tcb s \ valid_tcb' (tcbFault_update f tcb) s" - by (clarsimp simp: valid_tcb'_def tcb_cte_cases_def cteSizeBits_def) + by (clarsimp simp: valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs) lemma valid_tcb'_tcbTimeSlice_update[simp]: "valid_tcb' (tcbTimeSlice_update f tcb) s = valid_tcb' tcb s" - by (simp add:valid_tcb'_def tcb_cte_cases_def cteSizeBits_def) + by (simp add:valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs) + +lemma invs'_wu[simp]: + "invs' (ksWorkUnitsCompleted_update f s) = invs' s" + apply (simp add: invs'_def cur_tcb'_def valid_state'_def valid_bitmaps_def + valid_irq_node'_def valid_machine_state'_def + ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def + bitmapQ_defs) + done + +(* FIXME arch-split: MOVE *) +context Arch begin arch_global_naming + +lemma valid_arch_state'_interrupt[simp]: + "valid_arch_state' (ksInterruptState_update f s) = valid_arch_state' s" + by (simp add: valid_arch_state'_def) + +end + +(* FIXME arch-split: locales? *) +arch_requalify_facts + valid_arch_state'_interrupt (* FIXME arch-split: safe to export? any arch where this wouldn't be true *) + +lemmas [simp] = + valid_arch_state'_interrupt + +lemma if_unsafe_then_cap_arch'[simp]: + "if_unsafe_then_cap' (ksArchState_update f s) = if_unsafe_then_cap' s" + by (simp add: if_unsafe_then_cap'_def ex_cte_cap_to'_def) lemma valid_bitmaps_ksSchedulerAction_update[simp]: "valid_bitmaps (ksSchedulerAction_update f s) = valid_bitmaps s" @@ -182,8 +321,17 @@ lemma ex_cte_cap_wp_to_work_units[simp]: = ex_cte_cap_wp_to' P slot s" by (simp add: ex_cte_cap_wp_to'_def) +(* add_upd_simps does not play nice with itself, so we need to give one instance a name prefix *) +context begin global_naming add_upd_invs'_gsUntypedZeroRanges + +add_upd_simps "invs' (gsUntypedZeroRanges_update f s)" + (obj_at'_real_def) + +end +lemmas [simp] = add_upd_invs'_gsUntypedZeroRanges.upd_simps + add_upd_simps "ct_in_state' P (gsUntypedZeroRanges_update f s)" -declare upd_simps[simp] +lemmas [simp] = upd_simps lemma ct_not_inQ_ksArchState_update[simp]: "ct_not_inQ (ksArchState_update f s) = ct_not_inQ s" @@ -258,22 +406,6 @@ lemma ct_in_state_ksSched[simp]: apply auto done -lemma invs'_wu [simp]: - "invs' (ksWorkUnitsCompleted_update f s) = invs' s" - apply (simp add: invs'_def cur_tcb'_def valid_state'_def valid_bitmaps_def - valid_irq_node'_def valid_machine_state'_def - ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def - bitmapQ_defs) - done - -lemma valid_arch_state'_interrupt[simp]: - "valid_arch_state' (ksInterruptState_update f s) = valid_arch_state' s" - by (simp add: valid_arch_state'_def cong: option.case_cong) - -context begin interpretation Arch . (*FIXME: arch-split*) - -end - lemma valid_bitmapQ_ksSchedulerAction_upd[simp]: "valid_bitmapQ (ksSchedulerAction_update f s) = valid_bitmapQ s" unfolding bitmapQ_defs by simp @@ -351,4 +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) -end \ No newline at end of file +end diff --git a/proof/refine/X64/IpcCancel_R.thy b/proof/refine/X64/IpcCancel_R.thy index 9944c416b7..1cbbb181ea 100644 --- a/proof/refine/X64/IpcCancel_R.thy +++ b/proof/refine/X64/IpcCancel_R.thy @@ -128,7 +128,7 @@ crunch cancelSignal context delete_one_conc_pre begin -lemmas delete_one_typ_ats[wp] = typ_at_lifts [OF delete_one_typ_at] +lemmas delete_one_typ_ats[wp] = X64.typ_at_lifts [OF delete_one_typ_at] lemma cancelIPC_tcb_at'[wp]: "\tcb_at' t\ cancelIPC t' \\_. tcb_at' t\" @@ -728,7 +728,6 @@ lemma cancelSignal_invs': apply (rule conjI) apply (case_tac "ntfnBoundTCB rv") apply (clarsimp elim!: if_live_state_refsE)+ - apply (rule conjI, clarsimp split: option.splits) apply (clarsimp dest!: idle'_no_refs) done qed @@ -800,6 +799,12 @@ crunch setEndpoint and valid_bitmaps[wp]: valid_bitmaps (wp: valid_bitmaps_lift simp: updateObject_default_def) +(* FIXME arch-split: non-hyp arches only, this is a duplicate (locales?) *) +lemma sym_refs_empty[simp]: + "sym_refs (\p. {}) = True" + unfolding sym_refs_def + by simp + lemma (in delete_one_conc) cancelIPC_invs[wp]: shows "\tcb_at' t and invs'\ cancelIPC t \\rv. invs'\" proof - @@ -827,7 +832,7 @@ proof - od \\rv. invs'\" apply (simp add: invs'_def valid_state'_def) apply (subst P) - apply (wp valid_irq_node_lift valid_global_refs_lift' valid_arch_state_lift' + apply (wp valid_irq_node_lift valid_global_refs_lift' irqs_masked_lift sts_sch_act' hoare_vcg_all_lift [OF setEndpoint_ksQ] setThreadState_ct_not_inQ EPSCHN @@ -864,7 +869,7 @@ proof - apply (rule conjI) apply (clarsimp elim!: if_live_state_refsE split: Structures_H.endpoint.split_asm) apply (drule st_tcb_at_state_refs_ofD') - apply (clarsimp simp: ep_redux_simps3 valid_ep'_def + apply (clarsimp simp: ep_redux_simps3 valid_ep'_def sym_refs_empty split: Structures_H.endpoint.split_asm cong: list.case_cong) apply (frule_tac x=t in distinct_remove1) @@ -1227,9 +1232,9 @@ crunch arch_post_cap_deletion end crunch cancel_ipc - for pspace_aligned[wp]: pspace_aligned - and pspace_distinct[wp]: pspace_distinct - (wp: crunch_wps simp: crunch_simps) + for pspace_aligned[wp]: "pspace_aligned :: det_state \ _" + and pspace_distinct[wp]: "pspace_distinct :: det_state \ _" + (simp: crunch_simps wp: crunch_wps) lemma (in delete_one) suspend_corres: "corres dc (einvs and tcb_at t) (invs' and tcb_at' t) @@ -1790,8 +1795,14 @@ lemma ct_not_in_ntfnQueue: crunch rescheduleRequired for valid_pspace'[wp]: "valid_pspace'" + +context begin interpretation Arch . (*FIXME: arch-split*) + crunch rescheduleRequired for valid_global_refs'[wp]: "valid_global_refs'" + +end + crunch rescheduleRequired for valid_machine_state'[wp]: "valid_machine_state'" @@ -1951,7 +1962,7 @@ lemma threadSet_not_tcb[wp]: by (clarsimp simp: threadSet_def valid_def getObject_def setObject_def in_monad loadObject_default_def ko_wp_at'_def projectKOs split_def in_magnitude_check - objBits_simps' updateObject_default_def + X64.objBits_simps' updateObject_default_def ps_clear_upd projectKO_opt_tcb) lemma setThreadState_not_tcb[wp]: @@ -2027,6 +2038,7 @@ lemma tcbSchedEnqueue_unlive_other: apply (drule_tac x=p in spec) apply (fastforce dest!: inQ_implies_tcbQueueds_of simp: tcbQueueEmpty_def ko_wp_at'_def opt_pred_def opt_map_def projectKOs + live'_def split: option.splits) done @@ -2056,7 +2068,7 @@ lemma cancelAllIPC_unlive: apply (clarsimp simp: projectKO_opt_tcb) apply (frule(1) obj_at_valid_objs') apply (intro conjI impI) - apply (clarsimp simp: valid_obj'_def valid_ep'_def projectKOs + apply (clarsimp simp: valid_obj'_def valid_ep'_def projectKOs live'_def obj_at'_def pred_tcb_at'_def ko_wp_at'_def split: endpoint.split_asm)+ done @@ -2070,11 +2082,11 @@ lemma cancelAllSignals_unlive: apply (rule bind_wp [OF _ get_ntfn_sp']) apply (case_tac "ntfnObj ntfn", simp_all add: setNotification_def) apply wp - apply (fastforce simp: obj_at'_real_def projectKOs + apply (fastforce simp: obj_at'_real_def projectKOs live'_def dest: obj_at_conj' elim: ko_wp_at'_weakenE) apply wp - apply (fastforce simp: obj_at'_real_def projectKOs + apply (fastforce simp: obj_at'_real_def projectKOs live'_def dest: obj_at_conj' elim: ko_wp_at'_weakenE) apply (wp rescheduleRequired_unlive) @@ -2086,7 +2098,7 @@ lemma cancelAllSignals_unlive: apply (clarsimp simp: pred_tcb_at'_def obj_at'_def projectKOs) apply (simp add: projectKOs projectKO_opt_tcb) apply (fastforce simp: ko_wp_at'_def valid_obj'_def valid_ntfn'_def - obj_at'_def projectKOs)+ + obj_at'_def projectKOs live'_def)+ done crunch tcbSchedEnqueue @@ -2146,7 +2158,7 @@ lemma cancelBadgedSends_filterM_helper': apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def) apply (erule delta_sym_refs) by (fastforce elim!: obj_atE' - simp: state_refs_of'_def projectKOs tcb_bound_refs'_def + simp: state_refs_of'_def projectKOs tcb_bound_refs'_def live'_def subsetD symreftype_inverse' split: if_split_asm)+ @@ -2181,7 +2193,7 @@ lemma cancelBadgedSends_invs[wp]: apply (frule obj_at_valid_objs', clarsimp) apply (clarsimp simp: valid_obj'_def valid_ep'_def projectKOs) apply (frule if_live_then_nonz_capD', simp add: obj_at'_real_def) - apply (clarsimp simp: projectKOs) + apply (clarsimp simp: projectKOs live'_def) apply (frule(1) sym_refs_ko_atD') apply (clarsimp simp add: fun_upd_idem st_tcb_at_refs_of_rev') diff --git a/proof/refine/X64/Ipc_R.thy b/proof/refine/X64/Ipc_R.thy index bfc4d23ae6..b598d115d6 100644 --- a/proof/refine/X64/Ipc_R.thy +++ b/proof/refine/X64/Ipc_R.thy @@ -353,7 +353,7 @@ lemma cteInsert_cte_wp_at: apply simp+ apply (rule word_of_nat_less) apply simp - apply (simp add:p_assoc_help) + apply (simp add:p_assoc_help mask_def) apply (simp add: max_free_index_def) apply (clarsimp simp: maskedAsFull_def is_derived'_def badge_derived'_def isCap_simps capMasterCap_def cte_wp_at_ctes_of @@ -1686,6 +1686,7 @@ lemma doFaultTransfer_invs[wp]: "\invs' and tcb_at' receiver\ doFaultTransfer badge sender receiver recv_buf \\rv. invs'\" +supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) by (simp add: doFaultTransfer_def split_def | wp | clarsimp split: option.split)+ @@ -1706,7 +1707,7 @@ lemma lookupIPCBuffer_valid_ipc_buffer [wp]: apply (clarsimp simp: projectKO_opts_defs split: kernel_object.split_asm) apply (clarsimp simp add: valid_obj'_def valid_tcb'_def isCap_simps cte_level_bits_def field_simps) - apply (drule bspec [OF _ ranI [where a = "0x80"]]) + apply (drule bspec [OF _ ranI [where a = "4 << cteSizeBits"]]) apply simp apply (clarsimp simp add: valid_cap'_def) apply (rule conjI) @@ -2067,7 +2068,8 @@ lemma reply_cap_end_mdb_chain: lemma unbindNotification_valid_objs'_strengthen: "valid_tcb' tcb s \ valid_tcb' (tcbBoundNotification_update Map.empty tcb) s" "valid_ntfn' ntfn s \ valid_ntfn' (ntfnBoundTCB_update Map.empty ntfn) s" - by (simp_all add: valid_tcb'_def valid_ntfn'_def valid_bound_tcb'_def valid_tcb_state'_def tcb_cte_cases_def split: ntfn.splits) + by (simp_all add: valid_tcb'_def valid_ntfn'_def valid_bound_tcb'_def valid_tcb_state'_def + tcb_cte_cases_def tcb_cte_cases_neqs split: ntfn.splits) crunch cteDeleteOne for valid_objs'[wp]: "valid_objs'" @@ -2236,7 +2238,8 @@ lemma doReplyTransfer_corres: apply (rule corres_split) apply (rule threadset_corresT; clarsimp simp add: tcb_relation_def fault_rel_optionation_def - tcb_cap_cases_def tcb_cte_cases_def exst_same_def) + tcb_cap_cases_def tcb_cte_cases_def tcb_cte_cases_neqs + exst_same_def) apply (rule_tac P="valid_sched and cur_tcb and tcb_at receiver and pspace_aligned and pspace_distinct" and P'="tcb_at' receiver and cur_tcb' @@ -2822,7 +2825,8 @@ crunch possibleSwitchTo and typ_at'[wp]: "\s. P (typ_at' T p s)" and irq_handlers'[wp]: valid_irq_handlers' and irq_states'[wp]: valid_irq_states' - (simp: unless_def tcb_cte_cases_def wp: crunch_wps) + (simp: unless_def tcb_cte_cases_def cteSizeBits_def wp: crunch_wps) + crunch sendSignal for ct'[wp]: "\s. P (ksCurThread s)" and it'[wp]: "\s. P (ksIdleThread s)" @@ -3309,6 +3313,7 @@ lemma receiveIPC_corres: dest!: invs_valid_objs elim!: obj_at_valid_objsE split: option.splits) + apply clarsimp apply (auto simp: valid_cap'_def invs_valid_pspace' valid_obj'_def valid_tcb'_def valid_bound_ntfn'_def obj_at'_def projectKOs pred_tcb_at'_def dest!: invs_valid_objs' obj_at_valid_objs' @@ -3555,6 +3560,7 @@ lemma setupCallerCap_ifunsafe[wp]: \\rv. if_unsafe_then_cap'\" unfolding setupCallerCap_def getThreadCallerSlot_def getThreadReplySlot_def locateSlot_conv + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (wp getSlotCap_cte_wp_at | simp add: unique_master_reply_cap' | strengthen eq_imp_strg | wp (once) hoare_drop_imp[where f="getCTE rs" for rs])+ @@ -3718,6 +3724,7 @@ lemma completeSignal_invs: "\invs' and tcb_at' tcb\ completeSignal ntfnptr tcb \\_. invs'\" + supply projectKOs[simp] apply (simp add: completeSignal_def) apply (rule bind_wp[OF _ get_ntfn_sp']) apply (rule hoare_pre) @@ -3729,12 +3736,13 @@ lemma completeSignal_invs: \ ntfnptr \ ksIdleThread s" in hoare_strengthen_post) apply ((wp hoare_vcg_ex_lift hoare_weak_lift_imp | wpc | simp add: valid_ntfn'_def)+)[1] - apply (clarsimp simp: obj_at'_def state_refs_of'_def typ_at'_def ko_wp_at'_def projectKOs split: option.splits) + apply (clarsimp simp: obj_at'_def state_refs_of'_def typ_at'_def ko_wp_at'_def projectKOs live'_def + split: option.splits) apply (blast dest: ntfn_q_refs_no_bound_refs') apply wp apply (subgoal_tac "valid_ntfn' ntfn s") apply (subgoal_tac "ntfnptr \ ksIdleThread s") - apply (fastforce simp: valid_ntfn'_def valid_bound_tcb'_def projectKOs ko_at_state_refs_ofD' + apply (fastforce simp: valid_ntfn'_def valid_bound_tcb'_def ko_at_state_refs_ofD' live'_def elim: obj_at'_weakenE if_live_then_nonz_capD'[OF invs_iflive' obj_at'_real_def[THEN meta_eq_to_obj_eq, @@ -3933,7 +3941,7 @@ lemma rai_invs'[wp]: apply (wp valid_irq_node_lift sts_sch_act' typ_at_lifts setThreadState_ct_not_inQ asUser_urz - | simp add: valid_ntfn'_def doNBRecvFailedTransfer_def | wpc)+ + | simp add: valid_ntfn'_def doNBRecvFailedTransfer_def live'_def | wpc)+ apply (clarsimp simp: pred_tcb_at' valid_tcb_state'_def) apply (rule conjI, clarsimp elim!: obj_at'_weakenE) apply (subgoal_tac "capNtfnPtr cap \ t") @@ -3971,7 +3979,7 @@ lemma rai_invs'[wp]: apply (wp hoare_vcg_const_Ball_lift valid_irq_node_lift sts_sch_act' setThreadState_ct_not_inQ typ_at_lifts asUser_urz - | simp add: valid_ntfn'_def doNBRecvFailedTransfer_def | wpc)+ + | simp add: valid_ntfn'_def doNBRecvFailedTransfer_def live'_def | wpc)+ apply (clarsimp simp: valid_tcb_state'_def) apply (frule_tac t=t in not_in_ntfnQueue) apply (simp) @@ -4207,8 +4215,8 @@ lemma sfi_invs_plus': done crunch send_fault_ipc - for pspace_aligned[wp]: pspace_aligned - and psapce_distinct[wp]: pspace_distinct + for pspace_aligned[wp]: "pspace_aligned :: det_ext state \ _" + and pspace_distinct[wp]: "pspace_distinct :: det_ext state \ _" (simp: crunch_simps wp: crunch_wps) lemma handleFault_corres: diff --git a/proof/refine/X64/KHeap_R.thy b/proof/refine/X64/KHeap_R.thy index 4b2418dd90..2b971e6f5a 100644 --- a/proof/refine/X64/KHeap_R.thy +++ b/proof/refine/X64/KHeap_R.thy @@ -261,7 +261,6 @@ lemma obj_relation_cuts_obj_bits: apply (erule (1) obj_relation_cutsE; clarsimp simp: objBits_simps objBits_defs bit_simps cte_level_bits_def pbfs_atleast_pageBits[simplified bit_simps]) - prefer 5 apply (cases ko; simp add: other_obj_relation_def objBits_defs split: kernel_object.splits) apply (rename_tac ako, case_tac ako; clarsimp simp: archObjSize_def)+ done @@ -410,6 +409,7 @@ lemma updateObject_cte_is_tcb_or_cte: \ ko' = KOTCB (setF (\x. cte) tcb) \ is_aligned q tcbBlockSizeBits \ ps_clear q tcbBlockSizeBits s) \ (\cte'. ko = KOCTE cte' \ ko' = KOCTE cte \ s' = s \ p = q \ is_aligned p cte_level_bits \ ps_clear p cte_level_bits s)" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (clarsimp simp: updateObject_cte typeError_def alignError_def tcbVTableSlot_def tcbCTableSlot_def to_bl_1 rev_take objBits_simps' in_monad map_bits_to_bl cte_level_bits_def in_magnitude_check @@ -910,6 +910,7 @@ declare diff_neg_mask[simp del] lemma cte_wp_at_ctes_of: "cte_wp_at' P p s = (\cte. ctes_of s p = Some cte \ P cte)" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (simp add: cte_wp_at_cases' map_to_ctes_def Let_def cte_level_bits_def objBits_simps' split del: if_split) @@ -918,7 +919,7 @@ lemma cte_wp_at_ctes_of: apply (clarsimp simp: ps_clear_def3 field_simps split del: if_split) apply (frule is_aligned_sub_helper) - apply (clarsimp simp: tcb_cte_cases_def split: if_split_asm) + apply (clarsimp simp: tcb_cte_cases_def cteSizeBits_def split: if_split_asm) apply (case_tac "n = 0") apply (clarsimp simp: field_simps) apply (subgoal_tac "ksPSpace s p = None") @@ -1400,6 +1401,7 @@ lemma typ_at'_valid_obj'_lift: assumes P: "\P T p. \\s. P (typ_at' T p s)\ f \\rv s. P (typ_at' T p s)\" notes [wp] = hoare_vcg_all_lift hoare_vcg_imp_lift hoare_vcg_const_Ball_lift typ_at_lifts [OF P] shows "\\s. valid_obj' obj s\ f \\rv s. valid_obj' obj s\" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (cases obj; simp add: valid_obj'_def hoare_TrueI) apply (rename_tac endpoint) apply (case_tac endpoint; simp add: valid_ep'_def, wp) @@ -1411,7 +1413,7 @@ lemma typ_at'_valid_obj'_lift: apply (case_tac "tcbState tcb"; simp add: valid_tcb'_def valid_tcb_state'_def split_def none_top_def valid_bound_ntfn'_def; - wpsimp wp: hoare_case_option_wp hoare_case_option_wp2; + wpsimp wp: hoare_case_option_wp hoare_case_option_wp2 valid_arch_tcb_lift' P; (clarsimp split: option.splits)?) apply (wpsimp simp: valid_cte'_def) apply (rename_tac arch_kernel_object) @@ -1903,6 +1905,38 @@ lemma set_ntfn_state_refs_of'[wp]: by (wp setObject_state_refs_of', simp_all add: objBits_simps' fun_upd_def) +(* FIXME arch-split: temporary fix for this arch *) +lemma non_hyp_state_hyp_refs_of'[simp]: + "state_hyp_refs_of' s = (\p. {})" + unfolding state_hyp_refs_of'_def + apply (rule ext) + by (clarsimp split: option.splits kernel_object.split + simp: hyp_refs_of'_def tcb_hyp_refs'_def) + +(* FIXME arch-split: temporary fix for this arch *) +lemma non_hyp_hyp_refs_of'[simp]: + "hyp_refs_of' p = {}" + unfolding state_hyp_refs_of'_def + by (clarsimp split: option.splits kernel_object.split + simp: hyp_refs_of'_def tcb_hyp_refs'_def) + +lemma setObject_state_hyp_refs_of': + assumes x: "updateObject val = updateObject_default val" + assumes y: "(1 :: machine_word) < 2 ^ objBits val" + shows + "\\s. P ((state_hyp_refs_of' s) (ptr := hyp_refs_of' (injectKO val)))\ + setObject ptr val + \\rv s. P (state_hyp_refs_of' s)\" + apply (clarsimp simp: setObject_def valid_def in_monad split_def + updateObject_default_def x in_magnitude_check y + elim!: rsubst[where P=P] intro!: ext + split del: if_split cong: option.case_cong if_cong) + done + +lemma set_ntfn_state_hyp_refs_of'[wp]: + "setNotification epptr ntfn \\s. P (state_hyp_refs_of' s)\" + by wpsimp + lemma setNotification_pred_tcb_at'[wp]: "\pred_tcb_at' proj P t\ setNotification ptr val \\rv. pred_tcb_at' proj P t\" apply (simp add: pred_tcb_at'_def setNotification_def) @@ -1987,7 +2021,7 @@ lemma setEndpoint_iflive'[wp]: apply (clarsimp simp: updateObject_default_def in_monad projectKOs) apply (clarsimp simp: updateObject_default_def in_monad projectKOs bind_def) - apply clarsimp + apply (clarsimp simp: live'_def) done declare setEndpoint_cte_wp_at'[wp] diff --git a/proof/refine/X64/LevityCatch.thy b/proof/refine/X64/LevityCatch.thy index 10d81455d0..afd20dc75f 100644 --- a/proof/refine/X64/LevityCatch.thy +++ b/proof/refine/X64/LevityCatch.thy @@ -9,6 +9,7 @@ imports "BaseRefine.Include" "Lib.LemmaBucket" "Lib.Corres_Method" + "Lib.AddUpdSimps" begin (* Try again, clagged from Include *) diff --git a/proof/refine/X64/RAB_FN.thy b/proof/refine/X64/RAB_FN.thy index cbe2a89c2f..6cf70d7597 100644 --- a/proof/refine/X64/RAB_FN.thy +++ b/proof/refine/X64/RAB_FN.thy @@ -80,6 +80,8 @@ lemma isCNodeCap_capUntypedPtr_capCNodePtr: "isCNodeCap c \ capUntypedPtr c = capCNodePtr c" by (clarsimp simp: isCap_simps) +context begin interpretation Arch . (*FIXME: arch-split*) + lemma resolveAddressBitsFn_eq: "monadic_rewrite F E (\s. (isCNodeCap cap \ (\slot. cte_wp_at' (\cte. cteCap cte = cap) slot s)) \ valid_objs' s \ cnode_caps_gsCNodes' s) @@ -145,3 +147,5 @@ proof (induct cap capptr bits rule: resolveAddressBits.induct) qed end + +end diff --git a/proof/refine/X64/Refine.thy b/proof/refine/X64/Refine.thy index e092230ae0..9e5e86ffac 100644 --- a/proof/refine/X64/Refine.thy +++ b/proof/refine/X64/Refine.thy @@ -639,7 +639,7 @@ lemma entry_corres: apply (simp add: tcb_relation_def arch_tcb_relation_def arch_tcb_context_set_def atcbContextSet_def) apply (clarsimp simp: tcb_cap_cases_def) - apply (clarsimp simp: tcb_cte_cases_def) + apply (clarsimp simp: tcb_cte_cases_def tcb_cte_cases_neqs) apply (simp add: exst_same_def) apply (rule corres_split[OF kernel_corres]) apply (rule corres_split_eqr[OF getCurThread_corres]) diff --git a/proof/refine/X64/Retype_R.thy b/proof/refine/X64/Retype_R.thy index a5ed6542e0..24fd400795 100644 --- a/proof/refine/X64/Retype_R.thy +++ b/proof/refine/X64/Retype_R.thy @@ -109,7 +109,8 @@ lemma valid_obj_makeObject_cte [simp]: lemma valid_obj_makeObject_tcb [simp]: "valid_obj' (KOTCB makeObject) s" unfolding valid_obj'_def valid_tcb'_def valid_tcb_state'_def - by (clarsimp simp: makeObject_tcb makeObject_cte tcb_cte_cases_def minBound_word) + by (clarsimp simp: makeObject_tcb makeObject_cte tcb_cte_cases_def minBound_word newArchTCB_def + cteSizeBits_def valid_arch_tcb'_def) lemma valid_obj_makeObject_endpoint [simp]: "valid_obj' (KOEndpoint makeObject) s" @@ -396,7 +397,7 @@ lemma pspace_no_overlap_disjoint': unfolding pspace_no_overlap'_def apply (rule disjointI) apply (rule ccontr) - apply clarsimp + apply (clarsimp simp: mask_def add_diff_eq) apply (elim allE impE notE) apply (simp add:field_simps)+ apply (erule(2) order_trans[OF _ is_aligned_no_overflow,OF _ pspace_alignedD']) @@ -497,7 +498,7 @@ lemma ps_clearD: "\ ps_clear x n s; ksPSpace s y = Some v; x < y; y \ x + 2 ^ n - 1 \ \ False" apply (clarsimp simp: ps_clear_def) apply (drule_tac a=y in equals0D) - apply (simp add: dom_def) + apply (simp add: dom_def mask_def add_diff_eq) apply fastforce done @@ -1024,12 +1025,9 @@ qed lemma pspace_no_overlapD': "\ ksPSpace s x = Some ko; pspace_no_overlap' p bits s \ \ {x .. x + 2 ^ objBitsKO ko - 1} \ {p .. (p && ~~ mask bits) + 2 ^ bits - 1} = {}" - apply (simp add:pspace_no_overlap'_def) - apply (intro impI) - apply (elim allE impE) - apply (simp add:field_simps)+ -done + by (simp add: pspace_no_overlap'_def mask_def add_diff_eq) +(* FIXME arch-split: AARCH64 uses mask_range here *) lemma new_range_subset: assumes cover: "range_cover ptr sz (objBitsKO ko) n" @@ -1126,14 +1124,14 @@ proof - apply (subst foldr_upd_app_if[folded data_map_insert_def]) apply (simp add: pspace_distinct'_def dom_if_Some ball_Un) apply (intro conjI ballI impI) - apply (simp add: ps_clear_def dom_if_Some Int_Un_distrib + apply (simp add: ps_clear_def dom_if_Some Int_Un_distrib mask_def add_diff_eq objBits_def[symmetric]) apply (rule conjI) apply (erule new_range_disjoint) apply (rule disjoint_subset[OF Diff_subset]) apply (erule disjoint_subset[OF new_range_sub]) apply (rule pspace_no_overlap_disjoint'[OF vs'(1) pn']) - apply (clarsimp simp add: ps_clear_def dom_if_Some Int_Un_distrib) + apply (clarsimp simp add: ps_clear_def dom_if_Some Int_Un_distrib mask_def add_diff_eq) apply (rule conjI) apply (erule new_range_disjoint) apply (rule disjoint_subset[OF Diff_subset]) @@ -1145,7 +1143,8 @@ proof - apply (subst Int_commute) apply (simp add:ptr_add_def field_simps) apply (rule disjoint_subset[OF Diff_subset]) - apply (erule pspace_no_overlapD' [OF _ pn']) + apply (drule pspace_no_overlapD' [OF _ pn']) + apply (simp add: mask_def add_diff_eq) done qed @@ -1172,8 +1171,8 @@ lemma ksPSpace_update_gs_eq[simp]: end -global_interpretation update_gs: PSpace_update_eq "update_gs ty us ptrs" - by (simp add: PSpace_update_eq_def) +global_interpretation update_gs: pspace_update_eq' "update_gs ty us ptrs" + by (simp add: pspace_update_eq'_def) context begin interpretation Arch . (*FIXME: arch-split*) @@ -2480,11 +2479,13 @@ proof - apply (drule(1) pspace_no_overlapD'[rotated]) apply (frule(1) range_cover_cell_subset) apply (erule disjE) + apply (simp add: mask_def add_diff_eq) apply (drule psubset_imp_subset) apply (drule(1) disjoint_subset2[rotated]) apply (drule(1) disjoint_subset) apply (drule(1) range_cover_subset_not_empty) apply clarsimp+ + apply (simp add: mask_def add_diff_eq) apply blast apply (drule(1) range_cover_no_0[OF ptr _ unat_less_helper]) apply simp @@ -3032,9 +3033,9 @@ 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 ioport_control) + apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) apply clarsimp - apply (erule (1) ioport_controlD, rule ioport_control) + apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) done lemma dist_z_m: "distinct_zombies m" @@ -3079,8 +3080,11 @@ where lemma obj_range'_subset: "\range_cover ptr sz (objBitsKO val) n; ptr' \ set (new_cap_addrs n ptr val)\ \ obj_range' ptr' val \ {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}" - unfolding obj_range'_def - by (rule new_range_subset, auto) + unfolding obj_range'_def mask_2pm1 + (* FIXME arch-split: this is struggling with the formulation of new_range_subset vs mask_range *) + apply (drule (1) new_range_subset) + apply (simp only: shiftl_t2n mult_1_right mask_2pm1 add_diff_eq) + done lemma obj_range'_subset_strong: assumes "range_cover ptr sz (objBitsKO val) n" @@ -3140,7 +3144,7 @@ proof - apply - apply (frule(1) obj_range'_subset) apply (simp add: obj_range'_def) - apply (cases "n = 0"; clarsimp simp:new_cap_addrs_def) + apply (cases "n = 0"; clarsimp simp:new_cap_addrs_def mask_def field_simps) done qed @@ -3199,9 +3203,10 @@ lemma valid_untyped'_helper: apply (drule Int_absorb1[OF psubset_imp_subset]) apply (drule aligned_untypedRange_non_empty) apply (simp add:isCap_simps) - apply (simp add:Int_ac) + apply (simp add:isCap_simps) + apply (simp add:Int_ac add_mask_fold) apply (drule(1) subset_trans) - apply blast + apply (simp only: add_mask_fold) apply (frule(1) obj_range'_subset_strong) apply (drule(1) non_disjoing_subset) apply blast @@ -3211,8 +3216,9 @@ lemma valid_untyped'_helper: apply (frule(1) obj_range'_subset) apply (drule(1) subset_trans) apply (erule impE) - apply clarsimp + apply (clarsimp simp: add_mask_fold) apply blast + apply (simp only: add_mask_fold) apply blast done qed @@ -3400,7 +3406,8 @@ proof (intro conjI impI) apply (rename_tac thread_state mcp priority bool option nat cptr vptr bound tcbprev tcbnext user_context) apply (case_tac thread_state, simp_all add: valid_tcb_state'_def valid_bound_tcb'_def valid_bound_ntfn'_def obj_at_disj' none_top_def - split: option.splits)[4] + valid_arch_tcb'_def + split: option.splits)[5] apply (simp add: valid_cte'_def) apply (frule pspace_alignedD' [OF _ ad(1)]) apply (frule pspace_distinctD' [OF _ ad(2)]) @@ -3692,7 +3699,7 @@ lemma createObjects_orig_cte_wp_at2': apply (simp add: cte_wp_at'_obj_at') apply (rule handy_prop_divs) apply (wp createObjects_orig_obj_at2'[where sz = sz], simp) - apply (simp add: tcb_cte_cases_def) + apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs) including classic_wp_pre apply (wp handy_prop_divs createObjects_orig_obj_at2'[where sz = sz] | simp add: o_def cong: option.case_cong)+ @@ -3726,12 +3733,12 @@ lemma createNewCaps_cte_wp_at2: mapM_x_wp' threadSet_cte_wp_at2')+ | assumption | clarsimp simp: APIType_capBits_def projectKO_opts_defs - makeObject_tcb tcb_cte_cases_def + makeObject_tcb tcb_cte_cases_def cteSizeBits_def archObjSize_def bit_simps createObjects_def curDomain_def objBits_if_dev split del: if_split - | simp add: objBits_simps)+ + | simp add: objBits_simps field_simps mult_2_right)+ done lemma createObjects_orig_obj_at': @@ -3787,7 +3794,7 @@ lemma createObjects_orig_cte_wp_at': \ cte_wp_at' P p s \ pspace_no_overlap' ptr sz s\ createObjects' ptr n val gbits \\r s. cte_wp_at' P p s\" - apply (simp add: cte_wp_at'_obj_at' tcb_cte_cases_def) + apply (simp add: cte_wp_at'_obj_at' tcb_cte_cases_def tcb_cte_cases_neqs) apply (rule hoare_pre, wp hoare_vcg_disj_lift createObjects_orig_obj_at'[where sz = sz]) apply clarsimp done @@ -3811,7 +3818,7 @@ lemma createNewCaps_cte_wp_at': | clarsimp simp: objBits_simps APIType_capBits_def createObjects_def curDomain_def archObjSize_def bit_simps | intro conjI impI - | force simp: tcb_cte_cases_def)+ + | force simp: tcb_cte_cases_def tcb_cte_cases_neqs)+ done lemma createObjects_obj_at_other: @@ -3853,7 +3860,7 @@ lemma valid_cap'_range_no_overlap: apply (erule disjE) apply (drule(2) disjoint_subset2 [OF obj_range'_subset]) apply (drule(1) disjoint_subset2[OF psubset_imp_subset]) - apply (simp add: Int_absorb ptr_add_def p_assoc_help + apply (simp add: Int_absorb ptr_add_def p_assoc_help mask_def del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff) apply (drule(1) obj_range'_subset) @@ -3864,6 +3871,7 @@ lemma valid_cap'_range_no_overlap: apply (erule of_nat_less_pow_64) apply (simp add:capAligned_def) apply (drule(1) disjoint_subset2) + apply (simp add: add_mask_fold) apply blast apply (intro allI) apply (drule_tac x = ptr' in spec) @@ -3872,7 +3880,7 @@ lemma valid_cap'_range_no_overlap: Int_atLeastAtMost atLeastatMost_empty_iff) apply (drule(2) disjoint_subset2 [OF obj_range'_subset]) apply (drule(1) disjoint_subset2) - apply (simp add: Int_absorb ptr_add_def p_assoc_help + apply (simp add: Int_absorb ptr_add_def p_assoc_help mask_def del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff) done @@ -4069,7 +4077,7 @@ lemma createNewCaps_iflive'[wp]: apply (case_tac apiobject_type, simp_all split del: if_split)[1] apply (rule hoare_pre, wp, simp) apply (wp mapM_x_wp' createObjects_iflive' threadSet_iflive' - | simp add: not_0 pspace_no_overlap'_def createObjects_def + | simp add: not_0 pspace_no_overlap'_def createObjects_def live'_def hyp_live'_def valid_pspace'_def makeObject_tcb makeObject_endpoint makeObject_notification objBitsKO_def APIType_capBits_def objBits_def @@ -4401,7 +4409,7 @@ lemma createNewCaps_idle'[wp]: | simp add: projectKO_opt_tcb projectKO_opt_cte makeObject_cte makeObject_tcb archObjSize_def tcb_cte_cases_def objBitsKO_def APIType_capBits_def - objBits_def createObjects_def bit_simps + objBits_def createObjects_def bit_simps tcb_cte_cases_neqs | intro conjI impI | clarsimp simp: curDomain_def)+ done @@ -4746,6 +4754,18 @@ lemma createNewCaps_vms: toAPIType_def object_type.splits bit_simps) done +(* FIXME arch-split: move, use as alternative when mask_range comes up *) +lemma new_range_subset': + assumes + cover: "range_cover ptr sz (objBitsKO ko) n" + and addr: "x \ set (new_cap_addrs n ptr ko)" + shows "mask_range x (objBitsKO ko) \ {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}" + using assms + apply - + apply (drule (1) new_range_subset) + apply (simp add: mask_def add_diff_eq) + done + lemma createObjects_pspace_domain_valid': "\\s. range_cover ptr sz (objBitsKO val + gbits) n \ n \ 0 \ {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \ kernel_data_refs = {} @@ -4760,13 +4780,12 @@ lemma createObjects_pspace_domain_valid': caps_overlap_reserved'_def) apply (simp add: pspace_domain_valid_def foldr_upd_app_if fun_upd_def[symmetric]) - apply (subgoal_tac " \x \ set (new_cap_addrs (unat (of_nat n << gbits)) ptr - val). {x..x + 2 ^ objBitsKO val - 1} - \ {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}") + apply (subgoal_tac " \x \ set (new_cap_addrs (unat (of_nat n << gbits)) ptr val). + mask_range x (objBitsKO val) \ {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}") apply blast apply (rule ballI) - apply (rule new_range_subset) + apply (rule new_range_subset') apply (erule range_cover_rel, simp+) apply (simp add: range_cover.unat_of_nat_n_shift field_simps) done @@ -5348,11 +5367,17 @@ lemma createObjects_untyped_ranges_zero': split: sum.split_asm kernel_object.split_asm arch_kernel_object.split_asm object_type.split_asm apiobject_type.split_asm) - apply (simp add: makeObject_tcb tcb_cte_cases_def makeObject_cte + apply (simp add: makeObject_tcb tcb_cte_cases_def makeObject_cte tcb_cte_cases_neqs untypedZeroRange_def) apply (simp add: makeObject_cte untypedZeroRange_def) done +(* FIXME arch-split: non-hyp arches only *) +lemma sym_refs_empty[simp]: + "sym_refs (\p. {}) = True" + unfolding sym_refs_def + by simp + lemma createObjects_no_cte_invs: assumes moKO: "makeObjectKO dev ty = Some val" assumes no_cte: "\c. projectKO_opt val \ Some (c::cte)" @@ -5429,10 +5454,12 @@ proof - createObjects_sched_queues | simp)+ apply clarsimp - apply ((intro conjI; assumption?); simp add: valid_pspace'_def objBits_def) + apply ((intro conjI; assumption?); simp add: valid_pspace'_def objBits_def projectKOs) apply (fastforce simp add: no_cte no_tcb split_def split: option.splits) - apply (auto simp: invs'_def no_tcb valid_state'_def no_cte + apply (fastforce simp: invs'_def no_tcb valid_state'_def no_cte split: option.splits kernel_object.splits) + apply (clarsimp simp: live'_def split: kernel_object.splits) + apply (clarsimp simp: live'_def split: kernel_object.splits) done qed diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy index 00134c2c98..ec6b780664 100644 --- a/proof/refine/X64/Schedule_R.thy +++ b/proof/refine/X64/Schedule_R.thy @@ -328,14 +328,14 @@ lemma tcbSchedAppend_iflive'[wp]: supply projectKOs[simp] apply (wpsimp wp: tcbQueueAppend_if_live_then_nonz_cap' threadGet_wp simp: bitmap_fun_defs) apply (frule_tac p=tcbPtr in if_live_then_nonz_capE') - apply (fastforce simp: ko_wp_at'_def st_tcb_at'_def obj_at'_def runnable_eq_active') + apply (fastforce simp: ko_wp_at'_def st_tcb_at'_def obj_at'_def runnable_eq_active' live'_def) apply (clarsimp simp: tcbQueueEmpty_def) apply (erule if_live_then_nonz_capE') apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def) apply (drule_tac x="tcbDomain tcb" in spec) apply (drule_tac x="tcbPriority tcb" in spec) apply (fastforce dest!: obj_at'_tcbQueueEnd_ksReadyQueues - simp: ko_wp_at'_def inQ_def obj_at'_def tcbQueueEmpty_def) + simp: ko_wp_at'_def inQ_def obj_at'_def tcbQueueEmpty_def live'_def) done lemma tcbSchedDequeue_iflive'[wp]: @@ -344,7 +344,7 @@ lemma tcbSchedDequeue_iflive'[wp]: \\_. if_live_then_nonz_cap'\" apply (simp add: tcbSchedDequeue_def) apply (wpsimp wp: tcbQueueRemove_if_live_then_nonz_cap' threadGet_wp) - apply (fastforce elim: if_live_then_nonz_capE' simp: obj_at'_def ko_wp_at'_def projectKOs) + apply (fastforce elim: if_live_then_nonz_capE' simp: obj_at'_def ko_wp_at'_def projectKOs live'_def) done crunch tcbSchedAppend @@ -1079,7 +1079,7 @@ lemma no_longer_inQ[simp]: lemma iflive_inQ_nonz_cap_strg: "if_live_then_nonz_cap' s \ obj_at' (inQ d prio) t s \ ex_nonz_cap_to' t s" - by (clarsimp simp: obj_at'_real_def projectKOs inQ_def + by (clarsimp simp: obj_at'_real_def projectKOs inQ_def live'_def elim!: if_live_then_nonz_capE' ko_wp_at'_weakenE) lemmas iflive_inQ_nonz_cap[elim] @@ -1796,7 +1796,7 @@ crunch set_scheduler_action crunch reschedule_required for in_correct_ready_q[wp]: in_correct_ready_q and ready_qs_distinct[wp]: ready_qs_distinct - (wp: crunch_wps ignore_del: reschedule_required) + (ignore: tcb_sched_action wp: crunch_wps) lemma tcbSchedEnqueue_valid_pspace'[wp]: "tcbSchedEnqueue tcbPtr \valid_pspace'\" diff --git a/proof/refine/X64/Syscall_R.thy b/proof/refine/X64/Syscall_R.thy index 411a93b7d4..3da2037dbb 100644 --- a/proof/refine/X64/Syscall_R.thy +++ b/proof/refine/X64/Syscall_R.thy @@ -906,7 +906,7 @@ lemma threadSet_all_invs_but_sch_extra: \\rv. all_invs_but_sch_extra \" apply (rule hoare_gen_asm) apply (wp threadSet_valid_pspace'T_P[where P = False and Q = \ and Q' = \]) - apply (simp add:tcb_cte_cases_def)+ + apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs)+ apply (wp threadSet_valid_pspace'T_P threadSet_state_refs_of'T_P[where f'=id and P'=False and Q=\ and g'=id and Q'=\] @@ -923,7 +923,7 @@ lemma threadSet_all_invs_but_sch_extra: threadSet_iflive'T threadSet_ifunsafe'T untyped_ranges_zero_lift threadSet_sched_pointers threadSet_valid_sched_pointers - | simp add:tcb_cte_cases_def cteCaps_of_def o_def)+ + | simp add:tcb_cte_cases_def tcb_cte_cases_neqs cteCaps_of_def o_def)+ apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift threadSet_pred_tcb_no_state | simp)+ apply (fastforce simp: sch_act_simple_def o_def cteCaps_of_def) done diff --git a/proof/refine/X64/TcbAcc_R.thy b/proof/refine/X64/TcbAcc_R.thy index 4d57f179c1..41306902cc 100644 --- a/proof/refine/X64/TcbAcc_R.thy +++ b/proof/refine/X64/TcbAcc_R.thy @@ -292,6 +292,7 @@ lemma update_valid_tcb'[simp]: "\f. valid_tcb' tcb (ksSchedulerAction_update f s) = valid_tcb' tcb s" "\f. valid_tcb' tcb (ksDomainTime_update f s) = valid_tcb' tcb s" by (auto simp: valid_tcb'_def valid_tcb_state'_def valid_bound_tcb'_def valid_bound_ntfn'_def + opt_tcb_at'_def valid_arch_tcb'_def split: option.splits thread_state.splits) lemma update_valid_tcbs'[simp]: @@ -441,7 +442,7 @@ lemma ball_tcb_cte_casesI: P (tcbCaller, tcbCaller_update); P (tcbIPCBufferFrame, tcbIPCBufferFrame_update) \ \ \x \ ran tcb_cte_cases. P x" - by (simp add: tcb_cte_cases_def) + by (simp add: tcb_cte_cases_def cteSizeBits_def) lemma all_tcbI: "\ \a b c d e f g h i j k l m n p q r s. P (Thread a b c d e f g h i j k l m n p q r s) \ @@ -805,6 +806,7 @@ lemma threadSet_valid_pspace'T_P: apply (clarsimp simp add: valid_obj'_def valid_tcb'_def bspec_split [OF spec [OF x]] z split_paired_Ball y u w v w' p n) + apply (simp add: valid_arch_tcb'_def) (* FIXME arch-split: non-hyp only *) done lemmas threadSet_valid_pspace'T = @@ -888,12 +890,12 @@ lemma threadSet_iflive'T: \\rv. if_live_then_nonz_cap'\" apply (simp add: threadSet_def) apply (wp setObject_tcb_iflive' getObject_tcb_wp) - apply (clarsimp simp: obj_at'_def projectKOs) + apply (clarsimp simp: obj_at'_def live'_def hyp_live'_def) apply (subst conj_assoc[symmetric], subst imp_disjL[symmetric])+ apply (rule conjI) apply (rule impI, clarsimp) apply (erule if_live_then_nonz_capE') - apply (clarsimp simp: ko_wp_at'_def) + apply (clarsimp simp: ko_wp_at'_def live'_def hyp_live'_def projectKOs) apply (clarsimp simp: bspec_split [OF spec [OF x]]) done @@ -1471,7 +1473,7 @@ lemma asUser_valid_tcbs'[wp]: "asUser t f \valid_tcbs'\" apply (simp add: asUser_def split_def) apply (wpsimp wp: threadSet_valid_tcbs' hoare_drop_imps - simp: valid_tcb'_def tcb_cte_cases_def objBits_simps') + simp: valid_tcb'_def valid_arch_tcb'_def tcb_cte_cases_def objBits_simps') done lemma asUser_corres': @@ -1503,7 +1505,7 @@ lemma asUser_corres': (set_object add (TCB (tcb \ tcb_arch := arch_tcb_context_set con (tcb_arch tcb) \))) (setObject add (tcb' \ tcbArch := atcbContextSet con' (tcbArch tcb') \))" by (rule setObject_update_TCB_corres [OF L2], - (simp add: tcb_cte_cases_def tcb_cap_cases_def exst_same_def)+) + (simp add: tcb_cte_cases_def tcb_cap_cases_def cteSizeBits_def exst_same_def)+) have L4: "\con con'. con = con' \ corres (\(irv, nc) (irv', nc'). r irv irv' \ nc = nc') \ \ (select_f (f con)) (select_f (g con'))" @@ -1601,10 +1603,10 @@ crunch asUser lemma asUser_valid_objs [wp]: "\valid_objs'\ asUser t f \\rv. valid_objs'\" - apply (simp add: asUser_def split_def) - apply (wp threadSet_valid_objs' hoare_drop_imps - | simp add: valid_tcb'_def tcb_cte_cases_def)+ - done + by (simp add: asUser_def split_def) + (wpsimp wp: threadSet_valid_objs' hoare_drop_imps + simp: valid_tcb'_def tcb_cte_cases_def valid_arch_tcb'_def cteSizeBits_def + atcbContextSet_def)+ lemma asUser_valid_pspace'[wp]: "\valid_pspace'\ asUser t m \\rv. valid_pspace'\" @@ -3283,7 +3285,7 @@ lemma sbn_valid_objs': \\rv. valid_objs'\" apply (simp add: setBoundNotification_def) apply (wp threadSet_valid_objs') - apply (simp add: valid_tcb'_def tcb_cte_cases_def) + apply (simp add: valid_tcb'_def tcb_cte_cases_def cteSizeBits_def) done lemma ssa_wp[wp]: @@ -3314,7 +3316,7 @@ lemma sts'_valid_pspace'_inv[wp]: apply (drule obj_at_ko_at') apply clarsimp apply (erule obj_at'_weakenE) - apply (simp add: tcb_cte_cases_def) + apply (simp add: tcb_cte_cases_def cteSizeBits_def) done lemma setQueue_tcb_in_cur_domain'[wp]: @@ -3337,7 +3339,7 @@ lemma sbn'_valid_pspace'_inv[wp]: apply (drule obj_at_ko_at') apply clarsimp apply (erule obj_at'_weakenE) - apply (simp add: tcb_cte_cases_def) + apply (simp add: tcb_cte_cases_def cteSizeBits_def) done crunch setQueue @@ -3980,6 +3982,8 @@ lemma isRunnable_const: "\st_tcb_at' runnable' t\ isRunnable t \\runnable _. runnable \" by (rule isRunnable_wp) +context begin interpretation Arch . (*FIXME: arch-split*) + lemma valid_ipc_buffer_ptr'D: assumes yv: "y < unat max_ipc_words" and buf: "valid_ipc_buffer_ptr' a s" @@ -4069,6 +4073,8 @@ lemma storeWordUser_corres: apply (simp add: valid_ipc_buffer_ptr'_def) done +end + lemma load_word_corres: "corres (=) \ (typ_at' UserDataT (a && ~~ mask pageBits) and (\s. is_aligned a word_size_bits)) @@ -4366,6 +4372,7 @@ qed lemma cte_at_tcb_at_32': "tcb_at' t s \ cte_at' (t + 32) s" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (simp add: cte_at'_obj_at') apply (rule disjI2, rule bexI[where x=32]) apply simp @@ -4794,7 +4801,7 @@ lemma tcbQueueRemove_if_live_then_nonz_cap': apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') apply (force dest: sym_heapD2[where p'=tcbPtr] sym_heapD1[where p=tcbPtr] elim: if_live_then_nonz_capE' - simp: valid_tcb'_def opt_map_def obj_at'_def ko_wp_at'_def projectKOs) + simp: valid_tcb'_def opt_map_def obj_at'_def ko_wp_at'_def projectKOs live'_def) done lemma tcbQueueRemove_ex_nonz_cap_to'[wp]: @@ -4830,12 +4837,12 @@ lemma tcbQueueInsert_if_live_then_nonz_cap': apply (wpsimp wp: tcbSchedPrev_update_iflive' tcbSchedNext_update_iflive' getTCB_wp) apply (intro conjI) apply (erule if_live_then_nonz_capE') - apply (clarsimp simp: ko_wp_at'_def obj_at'_def) + apply (clarsimp simp: ko_wp_at'_def obj_at'_def live'_def) apply (erule if_live_then_nonz_capE') apply (frule_tac p'=afterPtr in sym_heapD2) apply (fastforce simp: opt_map_def obj_at'_def) apply (frule (1) tcb_ko_at_valid_objs_valid_tcb') - apply (clarsimp simp: valid_tcb'_def ko_wp_at'_def obj_at'_def opt_map_def) + apply (clarsimp simp: valid_tcb'_def ko_wp_at'_def obj_at'_def opt_map_def live'_def) done lemma tcbSchedEnqueue_iflive'[wp]: @@ -4848,14 +4855,14 @@ lemma tcbSchedEnqueue_iflive'[wp]: apply normalise_obj_at' apply (rename_tac tcb) apply (frule_tac p=tcbPtr in if_live_then_nonz_capE') - apply (fastforce simp: ko_wp_at'_def obj_at'_def) + apply (fastforce simp: ko_wp_at'_def obj_at'_def live'_def) apply clarsimp apply (erule if_live_then_nonz_capE') apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def) apply (drule_tac x="tcbDomain tcb" in spec) apply (drule_tac x="tcbPriority tcb" in spec) apply (fastforce dest!: obj_at'_tcbQueueHead_ksReadyQueues - simp: ko_wp_at'_def inQ_def opt_pred_def opt_map_def obj_at'_def + simp: ko_wp_at'_def inQ_def opt_pred_def opt_map_def obj_at'_def live'_def split: option.splits) done @@ -4894,14 +4901,14 @@ crunch setThreadState, setBoundNotification lemma st_tcb_ex_cap'': "\ st_tcb_at' P t s; if_live_then_nonz_cap' s; \st. P st \ st \ Inactive \ \ idle' st \ \ ex_nonz_cap_to' t s" - by (clarsimp simp: pred_tcb_at'_def obj_at'_real_def projectKOs + by (clarsimp simp: pred_tcb_at'_def obj_at'_real_def projectKOs live'_def elim!: ko_wp_at'_weakenE if_live_then_nonz_capE') lemma bound_tcb_ex_cap'': "\ bound_tcb_at' P t s; if_live_then_nonz_cap' s; \ntfn. P ntfn \ bound ntfn \ \ ex_nonz_cap_to' t s" - by (clarsimp simp: pred_tcb_at'_def obj_at'_real_def projectKOs + by (clarsimp simp: pred_tcb_at'_def obj_at'_real_def projectKOs live'_def elim!: ko_wp_at'_weakenE if_live_then_nonz_capE') @@ -4916,13 +4923,13 @@ crunch removeFromBitmap lemma sts_ctes_of [wp]: "\\s. P (ctes_of s)\ setThreadState st t \\rv s. P (ctes_of s)\" apply (simp add: setThreadState_def) - apply (wp threadSet_ctes_ofT | simp add: tcb_cte_cases_def)+ + apply (wp threadSet_ctes_ofT | simp add: tcb_cte_cases_def tcb_cte_cases_neqs)+ done lemma sbn_ctes_of [wp]: "\\s. P (ctes_of s)\ setBoundNotification ntfn t \\rv s. P (ctes_of s)\" apply (simp add: setBoundNotification_def) - apply (wp threadSet_ctes_ofT | simp add: tcb_cte_cases_def)+ + apply (wp threadSet_ctes_ofT | simp add: tcb_cte_cases_def tcb_cte_cases_neqs)+ done crunch setThreadState, setBoundNotification diff --git a/proof/refine/X64/Tcb_R.thy b/proof/refine/X64/Tcb_R.thy index 6169ba5fcf..218b5d059b 100644 --- a/proof/refine/X64/Tcb_R.thy +++ b/proof/refine/X64/Tcb_R.thy @@ -320,8 +320,8 @@ lemma asUser_postModifyRegisters_corres: done crunch Tcb_A.restart, IpcCancel_A.suspend - for pspace_aligned[wp]: pspace_aligned - and pspace_distinct[wp]: pspace_distinct + for pspace_aligned[wp]: "pspace_aligned :: det_state \ _" + and pspace_distinct[wp]: "pspace_distinct :: det_state \ _" crunch restart for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers @@ -569,7 +569,7 @@ lemma threadSet_ct_in_state': done lemma valid_tcb'_tcbPriority_update: "\valid_tcb' tcb s; f (tcbPriority tcb) \ maxPriority \ \ valid_tcb' (tcbPriority_update f tcb) s" - apply (simp add: valid_tcb'_def tcb_cte_cases_def) + apply (simp add: valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs) done lemma threadSet_valid_objs_tcbPriority_update: @@ -654,7 +654,7 @@ lemma setMCPriority_corres: apply (clarsimp simp: setMCPriority_def set_mcpriority_def) apply (rule threadset_corresT) by (clarsimp simp: tcb_relation_def tcb_cap_cases_tcb_mcpriority - tcb_cte_cases_def exst_same_def)+ + tcb_cte_cases_def tcb_cte_cases_neqs exst_same_def)+ definition "out_rel fn fn' v v' \ @@ -969,8 +969,7 @@ lemma setMCPriority_invs': lemma valid_tcb'_tcbMCP_update: "\valid_tcb' tcb s \ f (tcbMCP tcb) \ maxPriority\ \ valid_tcb' (tcbMCP_update f tcb) s" - apply (simp add: valid_tcb'_def tcb_cte_cases_def) - done + by (simp add: valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs) lemma setMCPriority_valid_objs'[wp]: "\valid_objs' and K (prio \ maxPriority)\ setMCPriority t prio \\rv. valid_objs'\" @@ -1040,6 +1039,7 @@ lemma threadcontrol_corres_helper4: (assertDerived (cte_map (ab, ba)) ac (cteInsert ac (cte_map (ab, ba)) (cte_map (a, tcb_cnode_index 4))))) \\_ s. sym_heap_sched_pointers s \ valid_sched_pointers s \ valid_tcbs' s \ pspace_aligned' s \ pspace_distinct' s\" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (wpsimp wp: | strengthen invs_sym_heap_sched_pointers invs_valid_sched_pointers invs_valid_objs' valid_objs'_valid_tcbs' invs_pspace_aligned' @@ -1092,7 +1092,7 @@ lemma threadSet_invs_trivialT2: lemma getThreadBufferSlot_dom_tcb_cte_cases: "\\\ getThreadBufferSlot a \\rv s. rv \ (+) a ` dom tcb_cte_cases\" by (wpsimp simp: tcb_cte_cases_def getThreadBufferSlot_def locateSlot_conv cte_level_bits_def - tcbIPCBufferSlot_def) + tcbIPCBufferSlot_def cteSizeBits_def) lemma tcb_at'_cteInsert[wp]: "\\s. tcb_at' (ksCurThread s) s\ cteInsert t x y \\_ s. tcb_at' (ksCurThread s) s\" @@ -1120,7 +1120,7 @@ lemmas threadSet_invs_trivial2 = lemma valid_tcb_ipc_buffer_update: "\buf s. is_aligned buf msg_align_bits \ (\tcb. valid_tcb' tcb s \ valid_tcb' (tcbIPCBuffer_update (\_. buf) tcb) s)" - by (simp add: valid_tcb'_def tcb_cte_cases_def) + by (simp add: valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs) lemma checkCap_wp: assumes x: "\P\ f \\rv. Q\" @@ -1161,8 +1161,8 @@ crunch cap_insert (wp: crunch_wps ready_qs_distinct_lift) crunch cap_delete - for pspace_aligned[wp]: pspace_aligned - and pspace_distinct[wp]: pspace_distinct + for pspace_aligned[wp]: "pspace_aligned :: det_state \ _" + and pspace_distinct[wp]: "pspace_distinct :: det_state \ _" (ignore_del: preemption_point wp: crunch_wps simp: crunch_simps OR_choiceE_def @@ -1351,6 +1351,7 @@ proof - od odE od) g')" (is "corres _ ?T2_pre ?T2_pre' _ _") using z u + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply - apply (rule corres_guard_imp[where P=P and P'=P' and Q="P and cte_at (a, tcb_cnode_index 4)" @@ -1781,7 +1782,7 @@ lemma invokeTCB_corres: lemma tcbBoundNotification_caps_safe[simp]: "\(getF, setF)\ran tcb_cte_cases. getF (tcbBoundNotification_update (\_. Some ntfnptr) tcb) = getF tcb" - by (case_tac tcb, simp add: tcb_cte_cases_def) + by (case_tac tcb, simp add: tcb_cte_cases_def tcb_cte_cases_neqs) lemma valid_bound_ntfn_lift: assumes P: "\P T p. \\s. P (typ_at' T p s)\ f \\rv s. P (typ_at' T p s)\" diff --git a/proof/refine/X64/Untyped_R.thy b/proof/refine/X64/Untyped_R.thy index e9e314e61d..90cad18eef 100644 --- a/proof/refine/X64/Untyped_R.thy +++ b/proof/refine/X64/Untyped_R.thy @@ -449,38 +449,35 @@ lemma ctes_of_ko: isUntypedCap cap \ (\ptr\capRange cap. \optr ko. ksPSpace s optr = Some ko \ ptr \ obj_range' optr ko)" - apply (case_tac cap) + supply projectKOs[simp] + apply (case_tac cap; simp add: isCap_simps capRange_def) \ \TCB case\ - apply (simp_all add: isCap_simps capRange_def) - apply (clarsimp simp: valid_cap'_def obj_at'_def) - apply (intro exI conjI, assumption) - apply (clarsimp simp: projectKO_eq objBits_def obj_range'_def - dest!: projectKO_opt_tcbD simp: objBitsKO_def) + apply (clarsimp simp: valid_cap'_def obj_at'_def) + apply (intro exI conjI, assumption) + apply (clarsimp simp: objBits_def obj_range'_def mask_def add_diff_eq + dest!: projectKO_opt_tcbD simp: objBitsKO_def) \ \NTFN case\ apply (clarsimp simp: valid_cap'_def obj_at'_def) apply (intro exI conjI, assumption) - apply (clarsimp simp: projectKO_eq objBits_def - obj_range'_def projectKO_ntfn objBitsKO_def) + apply (clarsimp simp: objBits_def mask_def add_diff_eq obj_range'_def objBitsKO_def) \ \EP case\ apply (clarsimp simp: valid_cap'_def obj_at'_def) apply (intro exI conjI, assumption) - apply (clarsimp simp: projectKO_eq objBits_def - obj_range'_def projectKO_ep objBitsKO_def) + apply (clarsimp simp: objBits_def mask_def add_diff_eq obj_range'_def objBitsKO_def) \ \Zombie case\ apply (rename_tac word zombie_type nat) apply (case_tac zombie_type) apply (clarsimp simp: valid_cap'_def obj_at'_def) apply (intro exI conjI, assumption) - apply (clarsimp simp: projectKO_eq objBits_simps' obj_range'_def dest!: projectKO_opt_tcbD) - apply (clarsimp simp: valid_cap'_def obj_at'_def capAligned_def - objBits_simps' projectKOs) + apply (clarsimp simp: mask_def add_ac objBits_simps' obj_range'_def dest!: projectKO_opt_tcbD) + apply (clarsimp simp: valid_cap'_def obj_at'_def capAligned_def objBits_simps') apply (frule_tac ptr=ptr and sz=cte_level_bits in nasty_range [where 'a=machine_word_len, folded word_bits_def]) apply (simp add: cte_level_bits_def)+ apply clarsimp apply (drule_tac x=idx in spec) apply (clarsimp simp: less_mask_eq) - apply (fastforce simp: obj_range'_def projectKOs objBits_simps' field_simps)[1] + apply (fastforce simp: obj_range'_def objBits_simps' mask_def field_simps) \ \Arch cases\ apply (rename_tac arch_capability) apply (case_tac arch_capability) @@ -491,7 +488,7 @@ lemma ctes_of_ko: apply (case_tac ko, simp+)[1] apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; - simp add: archObjSize_def asid_low_bits_def pageBits_def bit_simps) + simp add: archObjSize_def asid_low_bits_def mask_def add_ac bit_simps) apply simp \ \IOPort case\ apply clarsimp @@ -507,7 +504,7 @@ lemma ctes_of_ko: apply (intro exI conjI,assumption) apply (clarsimp simp: obj_range'_def) apply (case_tac ko, simp_all split: if_splits, - (simp add: objBitsKO_def archObjSize_def field_simps shiftl_t2n)+)[1] + (simp add: objBitsKO_def archObjSize_def field_simps mask_def shiftl_t2n)+)[1] \ \PT case\ apply (rename_tac word option) apply (clarsimp simp: valid_cap'_def obj_at'_def pageBits_def bit_simps @@ -525,7 +522,7 @@ lemma ctes_of_ko: apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; simp) - apply (simp add: objBitsKO_def archObjSize_def field_simps shiftl_t2n) + apply (simp add: objBitsKO_def archObjSize_def field_simps mask_def shiftl_t2n) \ \PD case\ apply (clarsimp simp: valid_cap'_def obj_at'_def pageBits_def pdBits_def bit_simps page_directory_at'_def typ_at'_def ko_wp_at'_def) @@ -542,7 +539,7 @@ lemma ctes_of_ko: apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; simp) - apply (simp add: field_simps archObjSize_def shiftl_t2n) + apply (simp add: field_simps archObjSize_def shiftl_t2n mask_def) \ \PDPT case\ apply (clarsimp simp: valid_cap'_def obj_at'_def pageBits_def pdptBits_def bit_simps pd_pointer_table_at'_def typ_at'_def ko_wp_at'_def) @@ -559,7 +556,7 @@ lemma ctes_of_ko: apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; simp) - apply (simp add: field_simps archObjSize_def shiftl_t2n) + apply (simp add: field_simps archObjSize_def shiftl_t2n mask_def) \ \PML4 case\ apply (clarsimp simp: valid_cap'_def obj_at'_def pageBits_def pml4Bits_def bit_simps page_map_l4_at'_def typ_at'_def ko_wp_at'_def) @@ -576,17 +573,16 @@ lemma ctes_of_ko: apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; simp) - apply (simp add: field_simps archObjSize_def shiftl_t2n) + apply (simp add: field_simps archObjSize_def shiftl_t2n mask_def) \ \CNode case\ - apply (clarsimp simp: valid_cap'_def obj_at'_def capAligned_def - objBits_simps projectKOs) + apply (clarsimp simp: valid_cap'_def obj_at'_def capAligned_def objBits_simps) apply (frule_tac ptr=ptr and sz=cte_level_bits in nasty_range [where 'a=machine_word_len, folded word_bits_def]) apply (simp add: cte_level_bits_def objBits_defs)+ apply clarsimp apply (drule_tac x=idx in spec) apply (clarsimp simp: less_mask_eq) - apply (fastforce simp: obj_range'_def projectKOs objBits_simps' field_simps)[1] + apply (fastforce simp: obj_range'_def objBits_simps' field_simps mask_def)[1] done lemma untypedCap_descendants_range': @@ -669,7 +665,7 @@ lemma cte_wp_at_caps_descendants_range_inI': apply (drule untypedCap_descendants_range'[rotated]) apply (simp add: isCap_simps)+ apply (simp add: invs_valid_pspace') - apply (clarsimp simp: cte_wp_at_ctes_of) + apply (clarsimp simp: cte_wp_at_ctes_of add_mask_fold) apply (erule disjoint_subset2[rotated]) apply clarsimp apply (rule le_plus'[OF word_and_le2]) @@ -731,8 +727,8 @@ lemma map_ensure_empty': done lemma irq_nodes_global: - "irq_node' s + (ucast (irq :: 8 word)) * 32 \ global_refs' s" - by (simp add: global_refs'_def mult.commute mult.left_commute) + "irq_node' s + (ucast (irq :: irq) << cteSizeBits) \ global_refs' s" + by (simp add: global_refs'_def cteSizeBits_def shiftl_t2n) lemma valid_global_refsD2': "\ctes_of s p = Some cte; valid_global_refs' s\ \ @@ -743,17 +739,17 @@ lemma cte_cap_in_untyped_range: "\ ptr \ x; x \ ptr + 2 ^ bits - 1; cte_wp_at' (\cte. cteCap cte = UntypedCap d ptr bits idx) cref s; descendants_of' cref (ctes_of s) = {}; invs' s; ex_cte_cap_to' x s; valid_global_refs' s \ \ False" - apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of) + apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of add_mask_fold) apply (case_tac ctea, simp) apply (rename_tac cap node) apply (frule ctes_of_valid_cap', clarsimp) apply (case_tac "\irq. cap = IRQHandlerCap irq") apply (drule (1) equals0D[where a=x, OF valid_global_refsD2'[where p=cref]]) - apply (clarsimp simp: irq_nodes_global) + apply (clarsimp simp: irq_nodes_global add_mask_fold) apply (frule_tac p=crefa and p'=cref in caps_containedD', assumption) apply (clarsimp dest!: isCapDs) apply (rule_tac x=x in notemptyI) - apply (simp add: subsetD [OF cte_refs_capRange]) + apply (simp add: subsetD [OF cte_refs_capRange] add_mask_fold) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) apply (frule_tac p=cref and p'=crefa in untyped_mdbD', assumption) apply (simp_all add: isUntypedCap_def) @@ -885,9 +881,9 @@ lemma decodeUntyped_wf[wp]: apply clarsimp apply (erule disjE) apply (erule bspec) - apply (clarsimp simp:isCap_simps image_def) + apply (clarsimp simp:isCap_simps image_def shiftl_t2n mult_ac) apply (rule_tac x = x in bexI,simp) - apply simp + apply (simp add: mask_def) apply (erule order_trans) apply (frule(1) le_plus) apply (rule word_l_diffs,simp+) @@ -898,9 +894,10 @@ lemma decodeUntyped_wf[wp]: apply (clarsimp simp:ex_cte_cap_wp_to'_def) apply (rule_tac x = nodeSlot in exI) apply (case_tac cte) - apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps image_def) + apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps image_def + shiftl_t2n) apply (rule_tac x = x in bexI,simp) - apply simp + apply (simp add: mask_def) apply (erule order_trans) apply (frule(1) le_plus) apply (rule word_l_diffs,simp+) @@ -2697,7 +2694,7 @@ lemma irq_control_n' [simp]: lemma ioport_control_n' [simp]: "ioport_control n'" - using ioport_control phys + 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) @@ -3642,9 +3639,9 @@ lemma pspace_no_overlap_valid_untyped': \ valid_untyped' d ptr bits idx s" apply (clarsimp simp: valid_untyped'_def ko_wp_at'_def split del: if_split) apply (frule(1) pspace_no_overlapD') - apply (simp add: obj_range'_def[symmetric] Int_commute) + apply (simp add: obj_range'_def[symmetric] Int_commute add_mask_fold) apply (erule disjE) - apply (drule base_member_set[simplified field_simps]) + apply (drule base_member_set[simplified field_simps add_mask_fold]) apply (simp add: word_bits_def) apply blast apply (simp split: if_split_asm) @@ -3824,52 +3821,51 @@ lemma cte_wp_at_caps_no_overlapI': apply (intro ballI impI) apply (erule ranE) apply (subgoal_tac "isUntypedCap (cteCap ctea)") - prefer 2 + prefer 2 apply (rule untypedRange_not_emptyD) apply blast apply (case_tac ctea) apply simp apply (drule untyped_incD') - apply (simp add:isCap_simps)+ + apply (simp add:isCap_simps)+ apply (elim conjE) apply (erule subset_splitE) - apply (erule subset_trans[OF _ psubset_imp_subset,rotated]) - apply (clarsimp simp: word_and_le2) - apply simp - apply (thin_tac "P\Q" for P Q)+ - apply (elim conjE) - apply (drule disjoint_subset2[rotated, - where B' = "{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}"]) - apply clarsimp - apply (rule le_plus'[OF word_and_le2]) - apply simp - apply (erule word_of_nat_le) - apply simp + apply (erule subset_trans[OF _ psubset_imp_subset,rotated]) + apply (clarsimp simp: word_and_le2) apply simp + apply (thin_tac "P\Q" for P Q)+ + apply (elim conjE) + apply (drule disjoint_subset2[rotated, where B' = "{ptr..(ptr && ~~ mask sz) + mask sz}"]) + apply clarsimp + apply (rule le_plus'[OF word_and_le2]) + apply simp + apply (erule word_of_nat_le) + apply (simp add: add_mask_fold) + apply simp apply (erule subset_trans[OF _ equalityD1,rotated]) apply (clarsimp simp:word_and_le2) apply (thin_tac "P\Q" for P Q)+ apply (drule disjoint_subset[rotated, where A' = "{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}"]) - apply (clarsimp simp:word_and_le2 Int_ac)+ + apply (clarsimp simp:word_and_le2 Int_ac)+ done lemma descendants_range_ex_cte': "\descendants_range_in' S p (ctes_of s');ex_cte_cap_wp_to' P q s'; S \ capRange (cteCap cte); invs' s';ctes_of s' p = Some cte;isUntypedCap (cteCap cte)\ \ q \ S" - apply (frule invs_valid_objs') - apply (frule invs_mdb') - apply (clarsimp simp:invs'_def valid_state'_def) - apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of) - apply (frule_tac cte = "cte" in valid_global_refsD') - apply simp - apply (case_tac "\irq. cteCap ctea = IRQHandlerCap irq") - apply clarsimp + apply (frule invs_valid_objs') + apply (frule invs_mdb') + apply (clarsimp simp:invs'_def valid_state'_def) + apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of) + apply (frule_tac cte = "cte" in valid_global_refsD') + apply simp + apply (case_tac "\irq. cteCap ctea = IRQHandlerCap irq") + apply clarsimp apply (erule(1) in_empty_interE[OF _ _ subsetD,rotated -1]) - apply (clarsimp simp:global_refs'_def) - apply (erule_tac A = "range P" for P in subsetD) - apply (simp add:range_eqI field_simps) + apply (clarsimp simp:global_refs'_def) + apply (erule_tac A = "range P" for P in subsetD) + apply (simp add:range_eqI field_simps cteSizeBits_def shiftl_t2n) apply (case_tac ctea) apply clarsimp apply (case_tac ctea) @@ -3882,8 +3878,8 @@ lemma descendants_range_ex_cte': apply (drule_tac x = " (irq_node' s')" in cte_refs_capRange[rotated]) apply (erule(1) ctes_of_valid_cap') apply blast - apply (clarsimp simp:isCap_simps) - apply (simp add:valid_mdb'_def valid_mdb_ctes_def) + apply (clarsimp simp:isCap_simps) + apply (simp add:valid_mdb'_def valid_mdb_ctes_def) apply (drule(2) descendants_range_inD') apply clarsimp apply (drule_tac x = " (irq_node' s')" in cte_refs_capRange[rotated]) @@ -3996,49 +3992,49 @@ abbreviation(input) abbreviation(input) "usable_range == {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}" - lemma not_0_ptr[simp]: "ptr\ 0" - using misc cte_wp_at' - apply (clarsimp simp: cte_wp_at_ctes_of) - apply (case_tac cte) - apply clarsimp - apply (drule(1) ctes_of_valid_cap'[OF _ invs_valid_objs']) - apply (simp add: valid_cap'_def) - done +lemma not_0_ptr[simp]: "ptr\ 0" + using misc cte_wp_at' + apply (clarsimp simp: cte_wp_at_ctes_of) + apply (case_tac cte) + apply clarsimp + apply (drule(1) ctes_of_valid_cap'[OF _ invs_valid_objs']) + apply (simp add: valid_cap'_def) + done - lemma subset_stuff[simp]: - "retype_range \ usable_range" - apply (rule range_cover_subset'[OF cover]) - apply (simp add:misc2) - done +lemma subset_stuff[simp]: + "retype_range \ usable_range" + apply (rule range_cover_subset'[OF cover]) + apply (simp add:misc2) + done - lemma descendants_range[simp]: - "descendants_range_in' usable_range cref (ctes_of s)" - "descendants_range_in' retype_range cref (ctes_of s)" - proof - - have "descendants_range_in' usable_range cref (ctes_of s)" - using misc idx_cases cte_wp_at' cover - apply - - apply (erule disjE) - apply (erule cte_wp_at_caps_descendants_range_inI' - [OF _ _ _ range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]]) - apply simp+ - using desc_range - apply simp - done - thus "descendants_range_in' usable_range cref (ctes_of s)" - by simp - thus "descendants_range_in' retype_range cref (ctes_of s)" - by (rule descendants_range_in_subseteq'[OF _ subset_stuff]) - qed - - lemma vc'[simp] : "s \' capability.UntypedCap dev (ptr && ~~ mask sz) sz idx" - using misc cte_wp_at' - apply (clarsimp simp: cte_wp_at_ctes_of) - apply (case_tac cte) - apply clarsimp - apply (erule ctes_of_valid_cap') - apply (simp add: invs_valid_objs') - done +lemma descendants_range[simp]: + "descendants_range_in' usable_range cref (ctes_of s)" + "descendants_range_in' retype_range cref (ctes_of s)" +proof - + have "descendants_range_in' usable_range cref (ctes_of s)" + using misc idx_cases cte_wp_at' cover + apply - + apply (erule disjE) + apply (erule cte_wp_at_caps_descendants_range_inI' + [OF _ _ _ range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]]) + apply simp+ + using desc_range + apply simp + done + thus "descendants_range_in' usable_range cref (ctes_of s)" + by simp + thus "descendants_range_in' retype_range cref (ctes_of s)" + by (rule descendants_range_in_subseteq'[OF _ subset_stuff]) +qed + +lemma vc'[simp] : "s \' capability.UntypedCap dev (ptr && ~~ mask sz) sz idx" + using misc cte_wp_at' + apply (clarsimp simp: cte_wp_at_ctes_of) + apply (case_tac cte) + apply clarsimp + apply (erule ctes_of_valid_cap') + apply (simp add: invs_valid_objs') + done lemma ptr_cn[simp]: "canonical_address (ptr && ~~ mask sz)" @@ -4046,7 +4042,8 @@ lemma ptr_cn[simp]: lemma ptr_km[simp]: "ptr && ~~ mask sz \ kernel_mappings" - using vc' unfolding valid_cap'_def by clarsimp + using vc' unfolding valid_cap'_def + by clarsimp lemma sz_limit[simp]: "sz \ maxUntypedSizeBits" diff --git a/proof/refine/X64/VSpace_R.thy b/proof/refine/X64/VSpace_R.thy index d73bd1be77..5ed8038088 100644 --- a/proof/refine/X64/VSpace_R.thy +++ b/proof/refine/X64/VSpace_R.thy @@ -1753,7 +1753,7 @@ lemma storePDE_iflive [wp]: apply (rule hoare_pre) apply (rule setObject_iflive' [where P=\], simp) apply (simp add: objBits_simps archObjSize_def) - apply (auto simp: updateObject_default_def in_monad projectKOs) + apply (auto simp: updateObject_default_def in_monad projectKOs live'_def hyp_live'_def) done lemma setObject_pde_ksInt [wp]: @@ -1777,7 +1777,7 @@ lemma storePDPTE_iflive [wp]: apply (rule hoare_pre) apply (rule setObject_iflive' [where P=\], simp) apply (simp add: objBits_simps archObjSize_def) - apply (auto simp: updateObject_default_def in_monad projectKOs) + apply (auto simp: updateObject_default_def in_monad projectKOs live'_def hyp_live'_def) done lemma setObject_pdpte_ksInt [wp]: @@ -1801,7 +1801,7 @@ lemma storePML4E_iflive [wp]: apply (rule hoare_pre) apply (rule setObject_iflive' [where P=\], simp) apply (simp add: objBits_simps archObjSize_def) - apply (auto simp: updateObject_default_def in_monad projectKOs) + apply (auto simp: updateObject_default_def in_monad projectKOs live'_def hyp_live'_def) done lemma setObject_pml4e_ksInt [wp]: @@ -2170,7 +2170,7 @@ lemma storePTE_iflive [wp]: apply (rule hoare_pre) apply (rule setObject_iflive' [where P=\], simp) apply (simp add: objBits_simps archObjSize_def) - apply (auto simp: updateObject_default_def in_monad projectKOs) + apply (auto simp: updateObject_default_def in_monad projectKOs live'_def hyp_live'_def) done lemma setObject_pte_ksInt [wp]: @@ -2343,7 +2343,8 @@ lemma setASIDPool_iflive [wp]: apply (rule hoare_pre) apply (rule setObject_iflive' [where P=\], simp) apply (simp add: objBits_simps archObjSize_def) - apply (auto simp: updateObject_default_def in_monad projectKOs pageBits_def) + apply (auto simp: updateObject_default_def in_monad projectKOs pageBits_def + live'_def hyp_live'_def) done lemma setASIDPool_ksInt [wp]: