diff --git a/lib/Lib.thy b/lib/Lib.thy index e4ea9ffd5c..797cf4d354 100644 --- a/lib/Lib.thy +++ b/lib/Lib.thy @@ -22,6 +22,7 @@ imports Monads.Monad_Lib Basics.CLib NICTATools + Sorted_Addrs "Word_Lib.WordSetup" begin diff --git a/lib/ROOT b/lib/ROOT index ecd64a8054..4e2213b195 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -71,6 +71,7 @@ session Lib (lib) = Word_Lib + Rules_Tac Heap_List None_Top_Bot + Sorted_Addrs (* should move to Monads: *) NonDetMonadLemmaBucket diff --git a/lib/Sorted_Addrs.thy b/lib/Sorted_Addrs.thy new file mode 100644 index 0000000000..238389c6ef --- /dev/null +++ b/lib/Sorted_Addrs.thy @@ -0,0 +1,253 @@ +(* + * Copyright 2026, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory Sorted_Addrs +imports + Word_Lib.WordSetup + Eisbach_Tools.Eisbach_Methods +begin + +(* Proving pspace_distinct' produces quadratically many slow arithmetic proof obligations when + done directly. If we instead provide a sorted list of addresses of non-overlapping objects, + pspace_distinct' follows abstractly. Proving that a list of addresses is sorted and + non-overlapping produces only linearly many proof obligations. + + The local sorted_addrs below defines sorted lists of addresses for non-overlapping objects + and derives and unfolded version of pspace_distinct'. because pspace_distinct' itself is not + yet available. See lemma obj_spaced_distinct. + + The locale can be instantiated to the abstract and design levels by providing either obj_bits + or objBitsKO as a parameter at interpretation. + + In addition to a plain list of object addresses, there are also helper functions for defining + lists of aligned offsets within a larger region, for instance for CNodes or page tables, and + for appending these into the global sorted list of objects. + + See proof/infoflow/refine/RISCV64/Example_Valid_StateH.thy for an example of how this is used. +*) + + +(* Addresses of objects inside CNodes or page tables. p is the start of the encompassing object + region, sz its size in bits, and `align` the homogeneous alignment (and size) of the smaller + objects within. These will automatically be sorted and non-overlapping. *) +definition aligned_offsets :: "'a::len word \ nat \ nat \ 'a word list" where + "aligned_offsets p sz align = [p, p + 2^align .e. p + mask sz]" + +locale sorted_addrs = + fixes bits_of :: "'o \ nat" (* this is for obj_bits or objBitsKO *) +begin + +(* get alignment of an object at specific address *) +definition align_of :: "('a::len word \ 'o) \ 'a word \ nat" where + "align_of kh p \ case kh p of Some obj \ bits_of obj | None \ 0" + +(* the objects in the list are ordered by address and non-overlapping *) +fun obj_spaced :: "('a::len word \ 'o) \ 'a word list \ bool" where + "obj_spaced kh [] = True" +| "obj_spaced kh [p] = True" +| "obj_spaced kh (p#p'#ps) = (p + mask (align_of kh p) < p' \ obj_spaced kh (p'#ps))" + +(* pspace_aligned' in a more convenient form. The following is expected to hold when instantiated + to the design spec level: + "\ pspace_aligned' s; set addrs = dom (ksPSpace s) \ \ obj_aligned (ksPSpace s) addrs" *) +definition obj_aligned :: "('a::len word \ 'o) \ 'a word list \ bool" where + "obj_aligned kh addrs \ \p \ set addrs. is_aligned p (align_of kh p)" + +(* all objects in the set have the given alignment *) +definition offsets_align :: "('a::len word \ 'o) \ 'a word set \ nat \ bool" where + "offsets_align kh addrs n \ \p \ addrs. align_of kh p = n" + + +(* Lemmas *) + +lemma obj_spaced_nth: + "obj_spaced kh xs = (\i. Suc i < length xs \ + xs ! i + mask (align_of kh (xs ! i)) < xs ! Suc i)" + by (induct xs rule: obj_spaced.induct; fastforce simp: nth_Cons split: nat.split) + +lemma sorted_imp_obj_spaced: + "sorted_wrt (\p p'. p + mask (align_of kh p) < p') xs \ obj_spaced kh xs" + by (induct xs rule: obj_spaced.induct) auto + +lemma obj_spaced_imp_sorted: + "\ obj_aligned kh addrs; set xs \ set addrs; obj_spaced kh xs \ \ + sorted_wrt (\p p'. p + mask (align_of kh p) < p') xs" + apply (induct xs rule: obj_spaced.induct; clarsimp) + apply (meson aligned_add_mask_lessD basic_trans_rules(19) obj_aligned_def) + done + +lemma obj_spaced_sorted: + "obj_aligned kh ps \ obj_spaced kh ps = sorted_wrt (\p p'. p + mask (align_of kh p) < p') ps" + by (auto intro!: obj_spaced_imp_sorted sorted_imp_obj_spaced) + +lemma obj_spaced_append: + "obj_spaced kh (xs @ ys) = + (obj_spaced kh xs \ obj_spaced kh ys \ + (xs \ [] \ ys \ [] \ last xs + mask (align_of kh (last xs)) < hd ys))" + apply (induct xs rule: obj_spaced.induct; simp) + apply (case_tac ys, auto) + done + +lemma obj_spaced_distinct: + "\ obj_spaced kh addrs; obj_aligned kh addrs; dom kh = set addrs; kh p = Some ko \ \ + (mask_range p (bits_of ko) - {p}) \ dom kh = {}" + apply (simp add: obj_spaced_sorted sorted_wrt_iff_nth_less) + apply (clarsimp simp: obj_aligned_def) + apply (prop_tac "p \ set addrs", fastforce) + apply (frule (1) bspec) + apply (simp add: align_of_def) + apply (rule Int_emptyI) + apply (rename_tac p') + apply clarsimp + apply (drule_tac x=p' in bspec, assumption) + apply (prop_tac "\ko'. kh p' = Some ko'", fastforce) + apply (clarsimp simp: in_set_conv_nth) + apply (rename_tac i j ko') + apply (case_tac "i < j"; clarsimp) + apply (erule allE)+ + apply (erule (1) impE, erule (1) impE) + apply simp + apply (clarsimp simp: not_less le_less) + apply (prop_tac "i \ j", fastforce) + apply simp + apply (erule allE)+ + apply (erule (1) impE, erule (1) impE) + apply simp + apply (drule is_aligned_no_overflow_mask)+ + apply fastforce + done + + +(* Arrays of small objects: aligned_offsets *) + +lemma length_aligned_offsets: + "is_aligned p sz \ + length (aligned_offsets p sz align) = Suc (unat ((mask sz :: 'a word) div 2 ^ align))" + for p::"'a::len word" + unfolding aligned_offsets_def + apply (subst length_upto_enum_step) + apply (erule is_aligned_no_overflow_mask) + apply simp + done + +lemma aligned_offsets_nth: + "\ is_aligned p sz; n < length (aligned_offsets p sz align) \ \ + aligned_offsets p sz align ! n = p + of_nat n * 2^align" + apply (simp add: aligned_offsets_def) + apply (subst upto_enum_step_nth) + apply (erule is_aligned_no_overflow_mask) + apply simp + apply (subst (asm) length_upto_enum_step) + apply (erule is_aligned_no_overflow_mask) + apply simp + apply simp + done + +lemma aligned_offsets_obj_spaced: + "\ offsets_align kh (set (aligned_offsets p sz align)) align; is_aligned p sz \ \ + obj_spaced kh (aligned_offsets p sz align)" + apply (clarsimp simp: obj_spaced_nth offsets_align_def) + apply (simp add: aligned_offsets_nth length_aligned_offsets ring_distribs add_ac) + apply (erule (1) nth_aligned_offset_no_overflow) + done + +lemma set_aligned_offsets: + "is_aligned p n \ + set (aligned_offsets p sz n) = {p'. p \ p' \ p' \ p + mask sz} \ {p. is_aligned p n}" + apply (clarsimp simp: aligned_offsets_def upto_enum_step_def) + apply (rule conjI) + apply fastforce + apply (clarsimp simp: not_less) + apply (rule equalityI; clarsimp) + apply (rule conjI; clarsimp) + apply (meson div_to_mult_word_lt word_plus_mono_right word_plus_mono_right2) + apply (erule is_aligned_add) + apply (rule is_aligned_mult_triv2) + apply (clarsimp simp: image_iff) + apply (simp flip: shiftr_div_2n_w shiftl_eq_mult) + apply (rule_tac x="(x - p) >> n" in exI) + apply (rule conjI) + apply (simp add: add.commute le_shiftr word_diff_ls') + apply (prop_tac "is_aligned (x - p) n") + apply (erule (1) aligned_sub_aligned_simple) + apply (simp add: is_aligned_shiftr_shiftl) + done + +lemma aligned_offsets_neq_Nil: + "is_aligned p sz \ aligned_offsets p sz n \ []" + apply (prop_tac "length (aligned_offsets p sz n) \ 0") + apply (simp add: length_aligned_offsets) + apply clarsimp + done + +lemma hd_aligned_offsets: + "\ is_aligned p sz; sz < LENGTH('a) \ \ hd (aligned_offsets p sz n) = p" for p::"'a::len word" + apply (prop_tac "length (aligned_offsets p sz n) \ 0") + apply (simp add: length_aligned_offsets) + apply clarsimp + apply (frule is_aligned_no_overflow_mask) + apply (simp add: upto_enum_step_def not_less aligned_offsets_def split: if_splits) + apply (rule conjI, fastforce) + apply (simp add: hd_map) + apply (simp flip: shiftr_div_2n_w shiftl_eq_mult add: shiftr_mask2) + apply (clarsimp simp: upto_enum_def hd_append hd_map) + apply (simp add: unat_eq_zero) + done + +lemma hd_aligned_offsets_append: + "\ is_aligned p sz; sz < LENGTH('a) \ \ hd (aligned_offsets p sz n @ xs) = p" + for p::"'a::len word" + by (simp add: aligned_offsets_neq_Nil hd_aligned_offsets) + +lemma obj_spaced_cons_aligned_offsets: + "\ is_aligned p' sz; sz < LENGTH('a) \ \ + obj_spaced kh (p # aligned_offsets p' sz n @ xs) = + (p + mask (align_of kh p) < p' \ obj_spaced kh (aligned_offsets p' sz n @ xs))" + for p::"'a::len word" + apply (frule (1) hd_aligned_offsets[where n=n]) + apply (drule aligned_offsets_neq_Nil[where n=n]) + apply (clarsimp simp: neq_Nil_conv) + done + +lemma last_aligned_offsets: + "is_aligned p sz \ last (aligned_offsets p sz n) = p + (mask sz >> n << n)" + apply (frule aligned_offsets_neq_Nil[where n=n]) + apply (simp add: last_conv_nth aligned_offsets_nth length_aligned_offsets) + apply (simp flip: shiftr_div_2n_w shiftl_t2n') + done + +lemma last_aligned_offests_plus_mask: + "\ offsets_align kh (set (aligned_offsets p sz n)) n; is_aligned p sz; n \ sz \ \ + last (aligned_offsets p sz n) + mask (align_of kh (last (aligned_offsets p sz n))) = + p + mask sz" +proof - + assume sz: "n \ sz" + assume [simp]: "is_aligned p sz" + hence "aligned_offsets p sz n \ []" + by (rule aligned_offsets_neq_Nil) + moreover + assume "offsets_align kh (set (aligned_offsets p sz n)) n" + ultimately + have [simp]: "align_of kh (last (aligned_offsets p sz n)) = n" + by (simp add: offsets_align_def) + have "last (aligned_offsets p sz n) = p + (mask sz >> n << n)" + by (simp add: last_aligned_offsets) + also + have "... + mask n = p + (mask sz && ~~mask n) + mask n" + by (simp add: and_not_mask) + also + from mask_and_neg_mask_compose[OF sz] + have "... = p + mask sz" + by simp + finally + have "last (aligned_offsets p sz n) + mask n = p + mask sz" . + thus ?thesis + by simp +qed + +end (* locale sorted_addrs *) + +end \ No newline at end of file diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib/Word_Lemmas_Internal.thy index 73ae637e5d..d1d7248eda 100644 --- a/lib/Word_Lib/Word_Lemmas_Internal.thy +++ b/lib/Word_Lib/Word_Lemmas_Internal.thy @@ -1130,4 +1130,56 @@ lemma ucast_0_eq_right: lemmas ucast_0_eq = ucast_0_eq_left ucast_0_eq_right +lemma nth_aligned_offset_no_overflow: + fixes p :: "'a::len word" + assumes aligned: "is_aligned p sz" + assumes i: "i < unat (mask sz div 2 ^ n :: 'a word)" + shows "p + (mask n + word_of_nat i * 2 ^ n) < p + (2 ^ n + word_of_nat i * 2 ^ n)" +proof - + from i + have n: "n < LENGTH('a)" + by (metis div_by_0 gr_implies_not0 unat_2tp_if unsigned_eq_0_iff) + + from i + have i_len: "i < 2^LENGTH('a)" + by (auto intro: order_less_trans) + + let ?i = "word_of_nat i :: 'a::len word" + from i + have i_shift: "?i < mask sz >> n" + by (simp add: word_less_nat_alt shiftr_div_2n_w i_len unat_of_nat_eq) + + have Suc_i: "Suc i * 2 ^ n \ unat (mask sz :: 'a word)" + by (metis Suc_leI bot_nat_0.extremum_strict div_by_0 i th2 unat_2tp_if unat_div) + + from aligned + have p_mask: "p \ p + mask sz" + by (simp add: is_aligned_no_overflow_mask) + + have less_mask: "2 ^ n + (?i << n) \ mask sz" + by (metis Suc_i of_nat_Suc of_nat_shiftl shiftl_1 word_of_nat_le word_shiftl_add_distrib) + + have mask_less: "mask n < (2 ^n :: 'a word)" + by (simp add: mask_lt_2pn n) + hence "mask n + (?i << n) < 2 ^ n + (?i << n)" + by (smt (verit, ccfv_SIG) Suc_i add.commute add_right_cancel bot_nat_0.extremum_strict + is_aligned_and_not_zero is_aligned_shift le_unat_uoi mult_Suc + n_less_equal_power_2 of_nat_add of_nat_numeral of_nat_shiftl + olen_add_eqv order_less_le semiring_1_class.of_nat_power + trans_less_add1 unsigned_eq_0_iff word_plus_mono_right) + moreover + have "p \ p + (2 ^ n + (?i << n))" + using less_mask p_mask order_less_imp_le word_random + by blast + ultimately + have "p + (mask n + (?i << n)) < p + (2 ^ n + (?i << n))" + by (rule word_plus_strict_mono_right) + thus ?thesis + by (simp add: shiftl_t2n') +qed + +lemma mask_and_neg_mask_compose: + "n \ sz \ (mask sz && ~~mask n) + mask n = mask sz" + by (metis diff_add_cancel mask_sub) + end diff --git a/proof/crefine/RISCV64/ADT_C.thy b/proof/crefine/RISCV64/ADT_C.thy index a60194c26c..a3802da34d 100644 --- a/proof/crefine/RISCV64/ADT_C.thy +++ b/proof/crefine/RISCV64/ADT_C.thy @@ -294,11 +294,13 @@ lemma cirqstate_cancel: definition "cint_state_to_H cnode cirqs \ - InterruptState (ptr_val cnode) - (\i::6 word. if i \ maxIRQ then cirqstate_to_H (index cirqs (unat i)) - else irqstate.IRQInactive)" + InterruptState (ptr_val cnode) + (\i::irq. if i \ maxIRQ then cirqstate_to_H (index cirqs (unat i)) + else irqstate.IRQInactive)" -lemma cint_rel_to_H: +end + +lemma (in kernel_m) cint_rel_to_H: "irqs_masked' s \ cinterrupt_relation (ksInterruptState s) n t \ cint_state_to_H n t = (ksInterruptState s)" @@ -306,9 +308,9 @@ lemma cint_rel_to_H: apply (cases "ksInterruptState s") apply (rename_tac "fun") apply (clarsimp simp: cinterrupt_relation_def cint_state_to_H_def - maxIRQ_def Kernel_C.maxIRQ_def) + maxIRQ_def Kernel_C_maxIRQ) apply (rule ext) - apply clarsimp + apply (clarsimp split: if_split) apply (drule spec, erule impE, assumption) apply (drule_tac s="irqstate_to_C (fun i)" in sym, simp add: cirqstate_cancel[THEN fun_cong, simplified]) @@ -322,6 +324,8 @@ lemma projectKO_opt_UserData [simp]: "projectKO_opt KOUserData = Some UserData" by (simp add: projectKO_opts_defs) +context begin interpretation Arch . (*FIXME: arch-split*) + lemma ucast_ucast_mask_pageBits_shift: "ucast (ucast (p && mask pageBits >> 3) :: 9 word) = p && mask pageBits >> 3" apply (rule word_eqI) diff --git a/proof/crefine/RISCV64/ArchMove_C.thy b/proof/crefine/RISCV64/ArchMove_C.thy index 70425747a5..3f124ece1d 100644 --- a/proof/crefine/RISCV64/ArchMove_C.thy +++ b/proof/crefine/RISCV64/ArchMove_C.thy @@ -337,18 +337,6 @@ lemma asid_shiftr_low_bits_less[simplified]: apply simp done -lemma getActiveIRQ_neq_Some0x3FF': - "\\\ getActiveIRQ in_kernel \\rv s. rv \ Some 0x3FF\" - apply (simp add: getActiveIRQ_def) - apply wpsimp - done - -lemma getActiveIRQ_neq_Some0x3FF: - "\\\ doMachineOp (getActiveIRQ in_kernel) \\rv s. rv \ Some 0x3FF\" - apply (wpsimp simp: doMachineOp_def split_def) - apply (auto dest: use_valid intro: getActiveIRQ_neq_Some0x3FF') - done - (* We don't have access to n_msgRegisters from C here, but the number of msg registers in C should be equivalent to what we have in the abstract/design specs. We want a number for this definition that automatically updates if the number of registers changes, and we sanity check it later diff --git a/proof/crefine/RISCV64/CSpace_C.thy b/proof/crefine/RISCV64/CSpace_C.thy index c98792d471..4c27b3a65d 100644 --- a/proof/crefine/RISCV64/CSpace_C.thy +++ b/proof/crefine/RISCV64/CSpace_C.thy @@ -1930,7 +1930,7 @@ definition where "cleanup_info_wf' cap \ case cap of IRQHandlerCap irq \ - UCAST(6\machine_word_len) irq \ SCAST(32 signed\machine_word_len) Kernel_C.maxIRQ + UCAST(irq_len\machine_word_len) irq \ SCAST(32 signed\machine_word_len) Kernel_C.maxIRQ | ArchObjectCap acap \ arch_cleanup_info_wf' acap | _ \ True" @@ -2236,9 +2236,11 @@ lemma postCapDeletion_ccorres: apply (clarsimp simp: isCap_simps) apply (frule cap_get_tag_isCap_unfolded_H_cap(5)) apply (clarsimp simp: cap_irq_handler_cap_lift ccap_relation_def cap_to_H_def - cleanup_info_wf'_def c_valid_cap_def cl_valid_cap_def mask_def) - apply (rule mask_eq_ucast_eq[where 'a="6" and 'b="64" and 'c="64", symmetric, simplified]) - by (simp add: mask_def) + cleanup_info_wf'_def c_valid_cap_def cl_valid_cap_def) + apply (rule mask_eq_ucast_eq[where 'a="irq_len" and 'b="machine_word_len" and 'c="machine_word_len", + symmetric, simplified]) + apply (simp flip: LENGTH_irq_len_irqBits) + done lemma emptySlot_ccorres: "ccorres dc xfdc @@ -2829,7 +2831,8 @@ lemma sameRegionAs_spec: apply (simp add: cap_to_H_def) apply (clarsimp simp: up_ucast_inj_eq c_valid_cap_def ucast_eq_mask cl_valid_cap_def mask_twice from_bool_0 - split: if_split bool.split + simp flip: LENGTH_irq_len_irqBits + split: if_split bool.split | intro impI conjI | simp) apply (frule_tac cap'=cap_b in cap_get_tag_isArchCap_unfolded_H_cap) diff --git a/proof/crefine/RISCV64/Ctac_lemmas_C.thy b/proof/crefine/RISCV64/Ctac_lemmas_C.thy index f7875d0c76..c48013e21d 100644 --- a/proof/crefine/RISCV64/Ctac_lemmas_C.thy +++ b/proof/crefine/RISCV64/Ctac_lemmas_C.thy @@ -161,11 +161,11 @@ lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap] lemma array_assertion_abs_irq: "\s s'. (s, s') \ rf_sr \ True - \ (n s' \ 64 \ (x s' \ 0 \ n s' \ 0)) + \ (n s' \ 2 ^ irqBits \ (x s' \ 0 \ n s' \ 0)) \ (x s' = 0 \ array_assertion intStateIRQNode_Ptr (n s') (hrs_htd (t_hrs_' (globals s'))))" apply (intro allI impI disjCI2) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) - apply (clarsimp simp: h_t_valid_clift_Some_iff) + apply (clarsimp simp: h_t_valid_clift_Some_iff simp flip: LENGTH_irq_len_irqBits) apply (erule clift_array_assertion_imp, (simp add: exI[where x=0])+) done diff --git a/proof/crefine/RISCV64/Delete_C.thy b/proof/crefine/RISCV64/Delete_C.thy index b3bc638f85..9896e19203 100644 --- a/proof/crefine/RISCV64/Delete_C.thy +++ b/proof/crefine/RISCV64/Delete_C.thy @@ -897,8 +897,8 @@ lemma finaliseSlot_ccorres: arch_cap_has_cleanup'_def split: option.split capability.splits) apply (auto dest!: ctes_of_valid' - simp: valid_cap'_def Kernel_C.maxIRQ_def maxIRQ_def - unat_ucast word_le_nat_alt cleanup_info_wf'_def arch_cleanup_info_wf'_def)[1] + simp: valid_cap'_def maxIRQ_def Kernel_C_maxIRQ + cleanup_info_wf'_def arch_cleanup_info_wf'_def)[1] subgoal by (auto dest!: valid_capAligned ctes_of_valid' simp: isCap_simps final_matters'_def o_def) apply clarsimp diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy index 4a8800f169..4d7f8e25e8 100644 --- a/proof/crefine/RISCV64/Finalise_C.thy +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -978,11 +978,11 @@ lemma unbindMaybeNotification_ccorres: (* TODO: move *) definition irq_opt_relation_def: - "irq_opt_relation (airq :: (6 word) option) (cirq :: machine_word) \ + "irq_opt_relation (airq :: irq option) (cirq :: machine_word) \ case airq of Some irq \ (cirq = ucast irq \ irq \ ucast irqInvalid \ - ucast irq \ UCAST(32 signed \ 6) Kernel_C.maxIRQ) + ucast irq \ UCAST(32 signed \ irq_len) Kernel_C.maxIRQ) | None \ cirq = ucast irqInvalid" lemma finaliseCap_True_cases_ccorres: @@ -1684,8 +1684,8 @@ lemma cteDeleteOne_ccorres: lemma getIRQSlot_ccorres_stuff: "\ (s, s') \ rf_sr \ \ - CTypesDefs.ptr_add intStateIRQNode_Ptr (uint (irq :: 6 word)) - = Ptr (irq_node' s + 2 ^ cte_level_bits * ucast irq)" + CTypesDefs.ptr_add intStateIRQNode_Ptr (uint irq) + = Ptr (irq_node' s + 2 ^ cte_level_bits * ucast irq)" for irq :: irq apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def cinterrupt_relation_def) apply (simp add: objBits_simps cte_level_bits_def @@ -1723,10 +1723,9 @@ lemma deletingIRQHandler_ccorres: apply (clarsimp simp: cap_get_tag_isCap ghost_assertion_data_get_def ghost_assertion_data_set_def) apply (simp add: cap_tag_defs) - apply (clarsimp simp: cte_wp_at_ctes_of Collect_const_mem - irq_opt_relation_def Kernel_C.maxIRQ_def) - apply (drule word_le_nat_alt[THEN iffD1]) - apply (clarsimp simp: uint_0_iff unat_gt_0 uint_up_ucast is_up) + using maxIRQ_less_2p_irqBits + apply (clarsimp simp: cte_wp_at_ctes_of Collect_const_mem word_le_nat_alt word_less_nat_alt + irq_opt_relation_def Kernel_C_maxIRQ uint_0_iff unat_gt_0) done (* 6 = wordRadix, @@ -1747,21 +1746,16 @@ lemma Zombie_new_spec: done lemma irq_opt_relation_Some_ucast: - "\ x && mask 6 = x; ucast x \ irqInvalid; - ucast x \ (scast Kernel_C.maxIRQ :: 6 word) \ x \ (scast Kernel_C.maxIRQ :: machine_word) \ + "\ x && mask irqBits = x; ucast x \ irqInvalid; + ucast x \ (scast Kernel_C.maxIRQ :: irq) \ x \ (scast Kernel_C.maxIRQ :: machine_word) \ \ irq_opt_relation (Some (ucast x)) x" unfolding irq_opt_relation_def - apply simp - using ucast_ucast_mask[where x=x and 'a=6, symmetric] - apply (simp add: irq_opt_relation_def) - apply (clarsimp simp: irqInvalid_def Kernel_C.maxIRQ_def) - apply (simp only: unat_arith_simps ) - apply (clarsimp simp: word_le_nat_alt Kernel_C.maxIRQ_def) - done + using ucast_ucast_mask[where x=x and 'a=irq_len, unfolded LENGTH_irq_len_irqBits] + by (auto simp: Kernel_C_maxIRQ irq_machine_le_maxIRQ_irq) lemma ccap_relation_IRQHandler_mask: "\ ccap_relation acap ccap; isIRQHandlerCap acap \ - \ capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 6 + \ capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask irqBits = capIRQ_CL (cap_irq_handler_cap_lift ccap)" apply (simp only: cap_get_tag_isCap[symmetric]) apply (drule ccap_relation_c_valid_cap) @@ -2247,16 +2241,16 @@ lemma finaliseCap_ccorres: apply clarsimp apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) apply (frule(1) ccap_relation_IRQHandler_mask) - apply (clarsimp simp: isCap_simps irqInvalid_def valid_cap'_def) + apply (clarsimp simp: isCap_simps valid_cap'_def) apply (rule irq_opt_relation_Some_ucast) apply fastforce - apply (simp add: irqInvalid_def) - apply (simp add: Kernel_C.maxIRQ_def maxIRQ_def) + apply simp + apply (simp add: Kernel_C_maxIRQ maxIRQ_def) apply fastforce apply clarsimp apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) apply (frule(1) ccap_relation_IRQHandler_mask) - apply (clarsimp simp add:mask_eq_ucast_eq) + apply (clarsimp simp: ucast_ucast_mask simp flip: LENGTH_irq_len_irqBits) done end diff --git a/proof/crefine/RISCV64/Interrupt_C.thy b/proof/crefine/RISCV64/Interrupt_C.thy index 13c43a7186..0616ede9cb 100644 --- a/proof/crefine/RISCV64/Interrupt_C.thy +++ b/proof/crefine/RISCV64/Interrupt_C.thy @@ -51,7 +51,7 @@ lemma ptr_add_assertion_irq_guard: lemma cte_at_irq_node': "invs' s \ - cte_at' (irq_node' s + 2 ^ cte_level_bits * ucast (irq :: 6 word)) s" + cte_at' (irq_node' s + 2 ^ cte_level_bits * ucast (irq :: irq)) s" by (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def cte_level_bits_def real_cte_at' cteSizeBits_def shiftl_t2n) @@ -91,18 +91,17 @@ proof - apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def ghost_assertion_data_set_def) apply (clarsimp simp: cte_at_irq_node' ucast_nat_def) - apply (clarsimp simp: cte_wp_at_ctes_of badge_derived'_def - Collect_const_mem unat_gt_0 valid_cap_simps' maxIRQ_def) + apply (clarsimp simp: cte_wp_at_ctes_of badge_derived'_def maxIRQ_def + Collect_const_mem unat_gt_0 valid_cap_simps') apply (drule word_le_nat_alt[THEN iffD1]) - apply clarsimp - apply (drule valid_globals_ex_cte_cap_irq[where irq=irq]) - apply auto + using maxIRQ_less_2p_irqBits + apply (auto dest: valid_globals_ex_cte_cap_irq[where irq=irq]) done qed lemma invokeIRQHandler_ClearIRQHandler_ccorres: "ccorres dc xfdc - (invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and K(irq \ 0xFF)) + (invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) (UNIV \ {s. irq_' s = ucast irq}) [] (InterruptDecls_H.invokeIRQHandler (ClearIRQHandler irq)) (Call invokeIRQHandler_ClearIRQHandler_'proc)" @@ -120,12 +119,9 @@ lemma invokeIRQHandler_ClearIRQHandler_ccorres: apply wp apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def ghost_assertion_data_set_def) - apply (clarsimp simp: cte_at_irq_node' ucast_nat_def) - apply (drule word_le_nat_alt[THEN iffD1]) - apply (auto simp add:Word.uint_up_ucast) - apply (case_tac "of_int (uint irq) \ 0 \ 0 < unat irq") - by (auto simp: Collect_const_mem unat_eq_0) - + apply (clarsimp simp: cte_at_irq_node' split: if_split) + apply (auto simp: unat_eq_0 unat_le_2p_irqBits) + done lemma ntfn_case_can_send: "(case cap of NotificationCap x1 x2 x3 x4 \ f x3 @@ -269,30 +265,28 @@ lemma decodeIRQHandlerInvocation_ccorres: slotcap_in_mem_def valid_tcb_state'_def dest!: interpret_excaps_eq split: bool.splits) apply (intro conjI impI allI) - apply (clarsimp simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def - excaps_map_def excaps_in_mem_def word_less_nat_alt hd_conv_nth - slotcap_in_mem_def valid_tcb_state'_def - dest!: interpret_excaps_eq split: bool.splits)+ - apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')[6] - apply (drule ctes_of_valid') - apply fastforce - apply (clarsimp simp add:valid_cap_simps' maxIRQ_def) - apply (erule order.trans,simp) + apply (clarsimp simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def + excaps_map_def excaps_in_mem_def word_less_nat_alt hd_conv_nth + slotcap_in_mem_def valid_tcb_state'_def + dest!: interpret_excaps_eq split: bool.splits)+ + apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')[6] + apply (drule ctes_of_valid') + apply fastforce + apply (clarsimp simp: valid_cap_simps' maxIRQ_def) apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid') done declare mask_of_mask[simp] lemma ucast_maxIRQ_le_eq: - "UCAST(6 \ 64) irq \ SCAST(32 signed \ 64) Kernel_C.maxIRQ \ - irq \ SCAST(32 signed \ 6) Kernel_C.maxIRQ" - apply (subst ucast_le_ucast_6_64[symmetric]) - by (clarsimp simp: ucast_up_ucast is_up Kernel_C.maxIRQ_def) + "UCAST(irq_len \ machine_word_len) irq \ SCAST(32 signed \ machine_word_len) Kernel_C.maxIRQ \ + irq \ SCAST(32 signed \ irq_len) Kernel_C.maxIRQ" + by (simp add: Kernel_C_maxIRQ) lemma ucast_maxIRQ_le_eq': - "UCAST(6 \ 64) irq \ SCAST(32 signed \ 64) Kernel_C.maxIRQ \ irq \ maxIRQ" - apply (clarsimp simp: Kernel_C.maxIRQ_def maxIRQ_def) - by word_bitwise + "UCAST(irq_len \ machine_word_len) irq \ SCAST(32 signed \ machine_word_len) Kernel_C.maxIRQ \ + irq \ maxIRQ" + by (clarsimp simp: Kernel_C_maxIRQ maxIRQ_def) lemma invokeIRQControl_expanded_ccorres: "ccorres (K (K \) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') @@ -318,20 +312,15 @@ lemma invokeIRQControl_expanded_ccorres: apply (vcg exspec=cteInsert_modifies) apply wp apply (vcg exspec=setIRQState_modifies) - apply (clarsimp simp: is_simple_cap'_def isCap_simps valid_cap_simps' capAligned_def) + apply (clarsimp simp: is_simple_cap'_def isCap_simps valid_cap_simps' capAligned_def + Kernel_C_maxIRQ) apply (rule conjI, fastforce simp: word_bits_def)+ apply (rule conjI) - apply (clarsimp simp: word_le_nat_alt Kernel_C.maxIRQ_def maxIRQ_def) + apply (clarsimp simp: maxIRQ_def) apply (clarsimp simp: Collect_const_mem ccap_relation_def cap_irq_handler_cap_lift - cap_to_H_def c_valid_cap_def cl_valid_cap_def - word_bw_assocs mask_twice Kernel_C.maxIRQ_def ucast_ucast_a - is_up ucast_ucast_b is_down) - apply (subst less_mask_eq) - apply (rule le_m1_iff_lt[THEN iffD1,THEN iffD1]) - apply simp - apply (erule order.trans, simp) - apply (simp add: mask_def) - apply word_bitwise + cap_to_H_def c_valid_cap_def cl_valid_cap_def) + using irqBits_le_12 + apply (simp add: mask_twice ucast_and_mask_drop flip: LENGTH_irq_len_irqBits) done lemma invokeIRQControl_ccorres: @@ -352,7 +341,7 @@ lemma isIRQActive_ccorres: (isIRQActive irq) (Call isIRQActive_'proc)" apply (cinit lift: irq_') apply (simp add: getIRQState_def getInterruptState_def) - apply (rule_tac P="irq \ ucast Kernel_C.maxIRQ \ unat irq < (126::nat)" in ccorres_gen_asm) + apply (rule_tac P="irq \ ucast Kernel_C.maxIRQ \ unat irq < Kernel_Config.maxIRQ + 1" in ccorres_gen_asm) apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: simpler_gets_def word_sless_msb_less maxIRQ_def @@ -363,12 +352,13 @@ lemma isIRQActive_ccorres: Let_def cinterrupt_relation_def) apply (drule spec, drule(1) mp) apply (case_tac "intStateIRQTable (ksInterruptState \) irq") - apply (simp add: irq_state_defs Kernel_C.maxIRQ_def word_le_nat_alt)+ + apply (simp add: irq_state_defs)+ + apply (simp add: Kernel_C_maxIRQ word_le_nat_alt) done lemma Platform_maxIRQ: "maxIRQ = scast Kernel_C.maxIRQ" - by (simp add: maxIRQ_def Kernel_C.maxIRQ_def) + by (simp add: maxIRQ_def Kernel_C_maxIRQ) lemma Arch_invokeIRQControl_ccorres: "ccorres (K (K \) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') @@ -414,8 +404,8 @@ lemma liftME_invocationCatch: split: sum.split) done -lemma maxIRQ_ucast_scast [simp]: - "ucast (scast Kernel_C.maxIRQ :: 6 word) = scast Kernel_C.maxIRQ" +lemma maxIRQ_ucast_scast[simp]: + "ucast (scast Kernel_C.maxIRQ :: irq) = scast Kernel_C.maxIRQ" by (clarsimp simp: Kernel_C.maxIRQ_def) lemma decodeIRQ_arch_helper: "x \ IRQIssueIRQHandler \ @@ -427,7 +417,7 @@ lemma Arch_checkIRQ_ccorres: \ \ \irq = irq \ [] (checkIRQ irq) (Call Arch_checkIRQ_'proc)" apply (cinit lift: irq_' ) - apply (simp add: irqInvalid_def Kernel_C.irqInvalid_def Kernel_C.maxIRQ_def maxIRQ_def + apply (simp add: irqInvalid_def Kernel_C.irqInvalid_def Kernel_C_maxIRQ maxIRQ_def del: Collect_const) apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) @@ -443,33 +433,31 @@ lemma checkIRQ_wpE: lemma maxIRQ_ucast_toEnum_eq: "x \ ucast maxIRQ \ toEnum (unat x) = x" for x::machine_word - by (simp add: word_le_nat_alt maxIRQ_def) + using Kernel_Config_maxIRQ_ucast_toEnum_eq + by (simp add: maxIRQ_def) lemma toEnum_unat_irq_t_leq_scast: "x \ ucast maxIRQ \ (toEnum (unat x)::irq) \ scast Kernel_C.maxIRQ" for x::machine_word - by (simp add: word_le_nat_alt maxIRQ_def Kernel_C.maxIRQ_def ucast_nat_def unat_ucast) + unfolding maxIRQ_def + by (simp add: Kernel_C_maxIRQ maxIRQ_ucast_toEnum_eq_irq irq_machine_le_maxIRQ_irq) lemma ucast_toEnum_unat_irq_t_leq_ucast: "x \ ucast maxIRQ \ UCAST(_ \ machine_word_len) (toEnum (unat x)::irq) \ ucast Kernel_C.maxIRQ" for x::machine_word - by (simp add: word_le_nat_alt maxIRQ_def Kernel_C.maxIRQ_def ucast_nat_def unat_ucast) + unfolding maxIRQ_def + by (simp add: Kernel_C_maxIRQ maxIRQ_ucast_toEnum_eq_irq irq_machine_le_maxIRQ_irq) lemma ucast_toEnum_unat_irq_t_leq_scast: "x \ ucast maxIRQ \ UCAST(_ \ machine_word_len) (toEnum (unat x)::irq) \ scast Kernel_C.maxIRQ" for x::machine_word - by (simp add: word_le_nat_alt maxIRQ_def Kernel_C.maxIRQ_def ucast_nat_def unat_ucast) + unfolding maxIRQ_def + by (simp add: Kernel_C_maxIRQ maxIRQ_ucast_toEnum_eq_irq irq_machine_le_maxIRQ_irq) lemma maxIRQ_irqInvalid: "\ x \ ucast maxIRQ; x \ ucast irqInvalid \ \ toEnum (unat x) \ irqInvalid" for x :: machine_word - apply (simp add: word_le_nat_alt maxIRQ_def irqInvalid_def ucast_nat_def unat_ucast) - apply (rule notI, erule notE) - apply unat_arith - apply (clarsimp simp: unat_ucast_mask) - apply (subst (asm) and_mask_eq_iff_le_mask[THEN iffD2]) - apply (simp add: mask_def word_le_nat_alt) - apply assumption - done + unfolding maxIRQ_def + by (simp add: Kernel_C_maxIRQ maxIRQ_ucast_toEnum_eq_irq ucast_eq_irqInvalid_conv) lemmas maxIRQ_casts = maxIRQ_irqInvalid toEnum_unat_irq_t_leq_scast ucast_toEnum_unat_irq_t_leq_ucast maxIRQ_ucast_toEnum_eq ucast_toEnum_unat_irq_t_leq_scast @@ -603,13 +591,11 @@ lemma Arch_decodeIRQControlInvocation_ccorres: apply (rule_tac P'="\ \ksCurThread = tcb_ptr_to_ctcb_ptr thread\" in conseqPre) apply (prop_tac "\x::machine_word. \ scast Kernel_C.maxIRQ < x \ x = ucast (toEnum (unat x)::irq)") - apply (clarsimp simp: Kernel_C.maxIRQ_def not_less word_le_nat_alt ucast_nat_def - ucast_ucast_mask) - apply (rule sym) - apply (simp add: and_mask_eq_iff_le_mask) - apply (simp add: mask_def word_le_nat_alt) - apply (clarsimp simp: numeral_2_eq_2 numeral_3_eq_3 exception_defs - ThreadState_defs mask_def) + using leq_maxIRQ_leq_mask_irq_len + apply (clarsimp simp: Kernel_C_maxIRQ not_less + maxIRQ_ucast_toEnum_eq_irq ucast_ucast_mask + simp flip: and_mask_eq_iff_le_mask) + apply (simp only: numeral_2_eq_2 numeral_3_eq_3) apply (rule conseqPre, vcg) apply (fastforce simp: exception_defs split: if_split) apply (rule subset_refl) @@ -723,13 +709,13 @@ lemma decodeIRQControlInvocation_ccorres: apply (clarsimp simp: throwError_def return_def exception_defs syscall_error_rel_def syscall_error_to_H_def syscall_error_type_defs) - apply (ctac add: ccorres_injection_handler_csum1 - [OF lookupTargetSlot_ccorres, - unfolded lookupTargetSlot_def]) - prefer 2 - apply ccorres_rewrite - apply (ctac add: ccorres_return_C_errorE) - apply ccorres_rewrite + apply (ctac add: ccorres_injection_handler_csum1 + [OF lookupTargetSlot_ccorres, + unfolded lookupTargetSlot_def]) + prefer 2 + apply ccorres_rewrite + apply (ctac add: ccorres_return_C_errorE) + apply ccorres_rewrite apply csymbr apply (ctac add: ccorres_injection_handler_csum1[OF ensureEmptySlot_ccorres]) prefer 2 @@ -767,15 +753,14 @@ lemma decodeIRQControlInvocation_ccorres: apply simp apply (wp checkIRQ_wpE) apply (rule_tac P'="\ \ksCurThread = tcb_ptr_to_ctcb_ptr thread\" in conseqPre) - apply (prop_tac "\x::machine_word. \ scast Kernel_C.maxIRQ < x - \ x = ucast (toEnum (unat x)::irq)") - apply (clarsimp simp: Kernel_C.maxIRQ_def not_less word_le_nat_alt ucast_nat_def - ucast_ucast_mask) - apply (rule sym) - apply (simp add: and_mask_eq_iff_le_mask) - apply (simp add: mask_def word_le_nat_alt) - apply (clarsimp simp: numeral_2_eq_2 exception_defs ThreadState_defs mask_def) - apply (rule conseqPre, vcg) + apply (prop_tac "\x::machine_word. \ scast Kernel_C.maxIRQ < x + \ x = ucast (toEnum (unat x)::irq)") + using leq_maxIRQ_leq_mask_irq_len + apply (clarsimp simp: Kernel_C_maxIRQ not_less + maxIRQ_ucast_toEnum_eq_irq ucast_ucast_mask + simp flip: and_mask_eq_iff_le_mask) + apply (simp only: numeral_2_eq_2) + apply (rule conseqPre, vcg) apply (fastforce simp: exception_defs) apply (rule subset_refl) apply simp diff --git a/proof/crefine/RISCV64/Syscall_C.thy b/proof/crefine/RISCV64/Syscall_C.thy index c19e968f35..bf5053553e 100644 --- a/proof/crefine/RISCV64/Syscall_C.thy +++ b/proof/crefine/RISCV64/Syscall_C.thy @@ -329,7 +329,7 @@ lemma decodeInvocation_ccorres: apply (frule cap_get_tag_isCap_unfolded_H_cap, drule (1) cap_get_tag_to_H) apply fastforce apply (frule cap_get_tag_isCap_unfolded_H_cap, drule (1) cap_get_tag_to_H) - apply (fastforce simp: cap_endpoint_cap_lift_def mask_eq_ucast_eq) + apply (fastforce simp: cap_endpoint_cap_lift_def mask_eq_ucast_eq simp flip: LENGTH_irq_len_irqBits) apply (frule ccap_relation_ep_helpers) apply (clarsimp simp: cap_get_tag_isCap isEndpointCap_def) apply clarsimp @@ -1525,13 +1525,6 @@ lemma scast_maxIRQ_less_eq: lemmas scast_maxIRQ_is_less = scast_maxIRQ_less_eq [THEN iffD1] -lemma ucast_maxIRQ_is_less: - "SCAST(32 signed \ 64) Kernel_C.maxIRQ < UCAST(6 \ 64) irq \ scast Kernel_C.maxIRQ < irq" - apply (clarsimp simp: scast_def Kernel_C.maxIRQ_def) - apply (subgoal_tac "LENGTH(6) \ LENGTH(64)") - apply (drule less_ucast_ucast_less[where x= "0x36" and y="irq"]) - by (simp)+ - lemma validIRQcastingLess: "Kernel_C.maxIRQ maxIRQ < b" by (simp add: Platform_maxIRQ scast_maxIRQ_is_less is_up_def target_size source_size) @@ -1541,15 +1534,6 @@ lemma scast_maxIRQ_is_not_less: shows "\ Kernel_C.maxIRQ \ (scast Kernel_C.maxIRQ < b)" by (simp add: scast_maxIRQ_less_eq) -lemma ucast_maxIRQ_is_not_less: - "\ (SCAST(32 signed \ 64) Kernel_C.maxIRQ < UCAST(6 \ 64) irq) \ \ (scast Kernel_C.maxIRQ < irq)" - apply (clarsimp simp: scast_def Kernel_C.maxIRQ_def) - apply (subgoal_tac "LENGTH(6) \ LENGTH(64)") - prefer 2 - apply simp - apply (erule notE) - using ucast_up_mono by fastforce - lemma ccorres_return_void_C_Seq: "ccorres_underlying sr \ r rvxf arrel xf P P' hs X (return_void_C) \ ccorres_underlying sr \ r rvxf arrel xf P P' hs X (return_void_C ;; Z)" @@ -1583,9 +1567,7 @@ lemma handleInterrupt_ccorres: (Call handleInterrupt_'proc)" apply (cinit lift: irq_' cong: call_ignore_cong) apply (rule ccorres_Cond_rhs_Seq) - apply (simp add: Platform_maxIRQ del: Collect_const) - apply (drule ucast_maxIRQ_is_less[simplified]) - apply (simp del: Collect_const) + apply (simp add: Platform_maxIRQ Kernel_C_maxIRQ del: Collect_const) apply (rule ccorres_rhs_assoc)+ apply (subst doMachineOp_bind) apply (rule maskInterrupt_empty_fail) @@ -1600,7 +1582,7 @@ lemma handleInterrupt_ccorres: apply (vcg exspec=ackInterrupt_modifies) apply wp apply (vcg exspec=maskInterrupt_modifies) - apply (simp add: ucast_maxIRQ_is_not_less Platform_maxIRQ del: Collect_const) + apply (simp add: Kernel_C_maxIRQ Platform_maxIRQ del: Collect_const) apply (rule ccorres_pre_getIRQState) apply wpc apply simp @@ -1674,33 +1656,27 @@ lemma handleInterrupt_ccorres: apply (ctac (no_vcg) add: ackInterrupt_ccorres) apply wp apply (vcg exspec=handleReservedIRQ_modifies) - apply (simp add: sint_ucast_eq_uint is_down uint_up_ucast is_up ) - apply (clarsimp simp: word_sless_alt word_less_alt word_le_def Kernel_C.maxIRQ_def - uint_up_ucast is_up_def - source_size_def target_size_def word_size - sint_ucast_eq_uint is_down is_up word_0_sle_from_less) + apply (clarsimp simp: Kernel_C_maxIRQ not_less) apply (rule conjI) apply (clarsimp simp: cte_wp_at_ctes_of non_kernel_IRQs_def) - apply (clarsimp) - apply (clarsimp simp: Kernel_C.IRQTimer_def Kernel_C.IRQSignal_def - cte_wp_at_ctes_of ucast_ucast_b is_up) + (* array guard; numeral version of ucast irq < maxIRQ+1 *) + apply (solves \simp add: Kernel_Config.maxIRQ_def word_less_nat_alt word_le_nat_alt\) + apply (clarsimp simp: Kernel_C.IRQTimer_def Kernel_C.IRQSignal_def IRQReserved_def + cte_wp_at_ctes_of ucast_ucast_b is_up) apply (intro conjI impI) - apply clarsimp - apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) - apply (clarsimp simp: typ_heap_simps') - apply (simp add: cap_get_tag_isCap) - apply (clarsimp simp: isCap_simps) - apply (frule cap_get_tag_isCap_unfolded_H_cap) - apply (frule cap_get_tag_to_H, assumption) - apply (clarsimp simp: to_bool_def) - apply (cut_tac un_ui_le[where b = "54::machine_word" and a = irq, - simplified word_size]) - apply (simp add: ucast_eq_0 is_up_def source_size_def - target_size_def word_size unat_gt_0 not_less - | subst array_assertion_abs_irq[rule_format, OF conjI])+ - apply (clarsimp simp:nat_le_iff) - apply (clarsimp simp: IRQReserved_def)+ + apply clarsimp + apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) + apply (clarsimp simp: typ_heap_simps') + apply (simp add: cap_get_tag_isCap) + apply (clarsimp simp: isCap_simps) + apply (frule cap_get_tag_isCap_unfolded_H_cap) + apply (frule cap_get_tag_to_H, assumption) + apply (clarsimp simp: to_bool_def) + apply (simp add: unat_le_2p_irqBits) + apply (simp add: ucast_eq_0 is_up unat_gt_0) + apply (simp add: word_less_nat_alt unat_lt2p[where 'a=irq_len, simplified]) done + end end diff --git a/proof/crefine/RISCV64/Wellformed_C.thy b/proof/crefine/RISCV64/Wellformed_C.thy index 0eb738e21f..bbf38c3d0c 100644 --- a/proof/crefine/RISCV64/Wellformed_C.thy +++ b/proof/crefine/RISCV64/Wellformed_C.thy @@ -323,7 +323,7 @@ cl_valid_cap :: "cap_CL \ bool" where "cl_valid_cap c \ case c of - Cap_irq_handler_cap fc \ ((capIRQ_CL fc) && mask 6 = capIRQ_CL fc) + Cap_irq_handler_cap fc \ ((capIRQ_CL fc) && mask irqBits = capIRQ_CL fc) | Cap_frame_cap fc \ capFSize_CL fc < 3 \ capFVMRights_CL fc < 4 \ capFVMRights_CL fc \ 0 | x \ True" @@ -498,8 +498,11 @@ text \maxIRQ interface\ declare Kernel_C.maxIRQ_def[code] -(* FIXME: compute maxIRQ for kernel config instead *) -value_type irq_array_size = "Suc (unat Kernel_C.maxIRQ)" +lemma Kernel_C_maxIRQ: + "Kernel_C.maxIRQ = Kernel_Config.maxIRQ" + by (simp add: Kernel_C.maxIRQ_def Kernel_Config.maxIRQ_def) + +value_type irq_array_size = "Suc Kernel_Config.maxIRQ" text \TCBFlags interface\ diff --git a/proof/infoflow/RISCV64/ArchCNode_IF.thy b/proof/infoflow/RISCV64/ArchCNode_IF.thy index 374899d6b8..7e4206eb53 100644 --- a/proof/infoflow/RISCV64/ArchCNode_IF.thy +++ b/proof/infoflow/RISCV64/ArchCNode_IF.thy @@ -56,7 +56,7 @@ lemma set_cap_globals_equiv[CNode_IF_assms]: done definition irq_at :: "nat \ (irq \ bool) \ irq option" where - "irq_at pos masks \ let i = irq_oracle pos in (if i = 0x3F \ masks i then None else Some i)" + "irq_at pos masks \ let i = irq_oracle pos in (if i = irqInvalid \ masks i then None else Some i)" lemma dmo_getActiveIRQ_wp[CNode_IF_assms]: "\\s. P (irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s))) diff --git a/proof/infoflow/RISCV64/Example_Valid_State.thy b/proof/infoflow/RISCV64/Example_Valid_State.thy index 4eb727431d..16b616fc80 100644 --- a/proof/infoflow/RISCV64/Example_Valid_State.thy +++ b/proof/infoflow/RISCV64/Example_Valid_State.thy @@ -25,10 +25,17 @@ section \Example\ consts s0_context :: user_context -(* define the irqs to come regularly every 10 *) +definition timer_irq :: "'a::numeral" where + "timer_irq \ 1" (* not equal to irqInvalid and \ maxIRQ, otherwise arbitrary *) + +lemma timer_irq_le_maxIRQ: + "(timer_irq::irq) \ Kernel_Config.maxIRQ" + unfolding Kernel_Config.maxIRQ_def timer_irq_def + by simp +(* define the irqs to come regularly every 10 *) axiomatization where - irq_oracle_def: "RISCV64.irq_oracle \ \pos. if pos mod 10 = 0 then 10 else 0" + irq_oracle_def: "RISCV64.irq_oracle \ \pos. if pos mod 10 = 0 then timer_irq else 0" context begin interpretation Arch . (*FIXME: arch-split*) @@ -218,13 +225,10 @@ definition "High_pool_ptr = pptr_base + 0xA000" definition "Low_cnode_ptr = pptr_base + 0x10000" definition "High_cnode_ptr = pptr_base + 0x18000" definition "Silc_cnode_ptr = pptr_base + 0x20000" -definition "irq_cnode_ptr = pptr_base + 0x28000" definition "shared_page_ptr_virt = pptr_base + 0x200000" definition "shared_page_ptr_phys = addrFromPPtr shared_page_ptr_virt" -definition "timer_irq \ 10" (* not sure exactly how this fits in *) - definition "Low_mcp \ 5 :: priority" definition "Low_prio \ 5 :: priority" definition "High_mcp \ 5 :: priority" @@ -236,7 +240,7 @@ definition "High_domain \ 1 :: domain" lemmas s0_ptr_defs = Low_pool_ptr_def High_pool_ptr_def Low_cnode_ptr_def High_cnode_ptr_def Silc_cnode_ptr_def - ntfn_ptr_def irq_cnode_ptr_def Low_pd_ptr_def High_pd_ptr_def Low_pt_ptr_def High_pt_ptr_def + ntfn_ptr_def Low_pd_ptr_def High_pd_ptr_def Low_pt_ptr_def High_pt_ptr_def Low_tcb_ptr_def High_tcb_ptr_def idle_tcb_ptr_def timer_irq_def Low_prio_def High_prio_def Low_time_slice_def Low_domain_def High_domain_def init_irq_node_ptr_def riscv_global_pt_ptr_def pptr_base_def pptrBase_def canonical_bit_def shared_page_ptr_virt_def @@ -247,7 +251,7 @@ distinct ptrs_distinct[simp]: Low_tcb_ptr High_tcb_ptr idle_tcb_ptr ntfn_ptr Low_pt_ptr High_pt_ptr shared_page_ptr_virt Low_pd_ptr High_pd_ptr Low_cnode_ptr High_cnode_ptr Low_pool_ptr High_pool_ptr - Silc_cnode_ptr irq_cnode_ptr riscv_global_pt_ptr + Silc_cnode_ptr riscv_global_pt_ptr init_irq_node_ptr by (auto simp: s0_ptr_defs) @@ -612,9 +616,6 @@ definition idle_tcb :: kernel_object where tcb_flags = {}, tcb_arch = \tcb_context = empty_context\\" -definition - "irq_cnode \ CNode 0 (Map.empty([] \ cap.NullCap))" - abbreviation "Low_pool' \ \idx. if idx = asid_low_bits_of Low_asid then Some Low_pd_ptr else None" @@ -631,7 +632,7 @@ definition "shared_page \ ArchObj (DataPage False RISCVLargePage)" definition kh0 :: kheap where - "kh0 \ (\x. if \irq :: irq. init_irq_node_ptr + (ucast irq << 5) = x + "kh0 \ (\x. if \irq :: irq. init_irq_node_ptr + (ucast irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None) (Low_cnode_ptr \ Low_cnode, @@ -640,7 +641,6 @@ definition kh0 :: kheap where High_pool_ptr \ High_pool, Silc_cnode_ptr \ Silc_cnode, ntfn_ptr \ ntfn, - irq_cnode_ptr \ irq_cnode, Low_pd_ptr \ Low_pd, High_pd_ptr \ High_pd, Low_pt_ptr \ Low_pt, @@ -651,67 +651,68 @@ definition kh0 :: kheap where shared_page_ptr_virt \ shared_page, riscv_global_pt_ptr \ init_global_pt)" -lemma irq_node_offs_min: - "init_irq_node_ptr \ init_irq_node_ptr + (ucast (irq :: irq) << 5)" - apply (rule_tac sz=59 in machine_word_plus_mono_right_split) - apply (simp add: unat_word_ariths mask_def shiftl_t2n s0_ptr_defs) - apply (cut_tac x=irq and 'a=64 in ucast_less) - apply simp - apply (simp add: word_less_nat_alt) - apply (simp add: word_bits_def) - done +definition + "irq_node_size \ 2^(irq_len + cte_level_bits)" + +lemma init_irq_node_ptr_plus_size_neg_mask[simp]: + "init_irq_node_ptr + irq_node_size && ~~ mask (irq_len + cte_level_bits) = + init_irq_node_ptr + irq_node_size" + by (simp add: s0_ptr_defs irq_node_size_def irq_len_val cte_level_bits_def mask_def) lemma irq_node_offs_max: - "init_irq_node_ptr + (ucast (irq:: irq) << 5) < init_irq_node_ptr + 0x7E1" - apply (simp add: s0_ptr_defs shiftl_t2n) - apply (cut_tac x=irq and 'a=64 in ucast_less) + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) < init_irq_node_ptr + irq_node_size" + apply (simp add: s0_ptr_defs cte_level_bits_def shiftl_t2n) + apply (cut_tac x=irq and 'a=machine_word_len in ucast_less) apply simp - apply (simp add: word_less_nat_alt unat_word_ariths) + apply (simp add: word_less_nat_alt unat_word_ariths + irq_node_size_def cte_level_bits_def irq_len_val) done -definition irq_node_offs_range where - "irq_node_offs_range \ {x. init_irq_node_ptr \ x \ x < init_irq_node_ptr + 0x7E1} - \ {x. is_aligned x 5}" +definition irq_node_offs_range :: "obj_ref set" where + "irq_node_offs_range \ {x. init_irq_node_ptr \ x \ x < init_irq_node_ptr + irq_node_size} \ + {x. is_aligned x cte_level_bits}" + +declare is_aligned_init_irq_cte[simp] + +lemma is_aligned_init_irq_cte_level_bits[simp]: + "is_aligned init_irq_node_ptr cte_level_bits" + by (rule is_aligned_weaken, rule is_aligned_init_irq_cte, simp) lemma irq_node_offs_in_range: - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ irq_node_offs_range" - apply (clarsimp simp: irq_node_offs_min irq_node_offs_max irq_node_offs_range_def) + "init_irq_node_ptr + (ucast (irq:: irq) << cte_level_bits) \ irq_node_offs_range" + apply (clarsimp simp: irq_node_offs_max init_irq_ptrs_ineqs irq_node_offs_range_def) apply (rule is_aligned_add[OF _ is_aligned_shift]) - apply (simp add: is_aligned_def s0_ptr_defs) + apply simp done lemma irq_node_offs_range_correct: "x \ irq_node_offs_range - \ \irq. x = init_irq_node_ptr + (ucast (irq:: irq) << 5)" - apply (clarsimp simp: irq_node_offs_min irq_node_offs_max irq_node_offs_range_def s0_ptr_defs) - apply (rule_tac x="ucast ((x - 0xFFFFFFC000003000) >> 5)" in exI) - apply (clarsimp simp: ucast_ucast_mask) + \ \irq. x = init_irq_node_ptr + (ucast (irq:: irq) << cte_level_bits)" + unfolding irq_node_offs_range_def + apply clarsimp + apply (rule_tac x="ucast ((x - init_irq_node_ptr) >> cte_level_bits)" in exI) + apply (simp add: ucast_ucast_mask) apply (subst aligned_shiftr_mask_shiftl) apply (rule aligned_sub_aligned) apply assumption - apply (simp add: is_aligned_def) - apply simp - apply simp - apply (rule_tac n=11 in mask_eqI) + apply (simp add: is_aligned_def s0_ptr_defs cte_level_bits_def) + apply (simp add: cte_level_bits_def) + apply (rule_tac n="irq_len + cte_level_bits" in mask_eqI) apply (subst mask_add_aligned) - apply (simp add: is_aligned_def) - apply (simp add: mask_twice) + apply (simp add: is_aligned_def s0_ptr_defs cte_level_bits_def irq_len_val) + apply (simp add: mask_twice irq_len_val cte_level_bits_def) apply (simp add: diff_conv_add_uminus del: add_uminus_conv_diff) apply (subst add.commute[symmetric]) apply (subst mask_add_aligned) - apply (simp add: is_aligned_def) + apply (simp add: is_aligned_def s0_ptr_defs cte_level_bits_def irq_len_val) apply simp apply (simp add: diff_conv_add_uminus del: add_uminus_conv_diff) apply (subst add_mask_lower_bits) - apply (simp add: is_aligned_def) - apply clarsimp - apply (cut_tac x=x and y="0xFFFFFFC0000037E0" and n=14 in neg_mask_mono_le) - apply (force dest: word_less_sub_1) - apply (drule_tac n=11 in aligned_le_sharp) - apply (simp add: is_aligned_def) - apply (simp add: mask_def is_aligned_mask) - apply word_bitwise - apply fastforce + apply (simp add: is_aligned_def s0_ptr_defs cte_level_bits_def irq_len_val) + apply (clarsimp simp: cte_level_bits_def irq_len_val) + apply (erule (1) aligned_intvl_neg_mask_start) + apply (simp add: is_aligned_def s0_ptr_defs cte_level_bits_def irq_len_val) + apply (simp add: irq_node_size_def cte_level_bits_def irq_len_val) done lemma irq_node_offs_range_distinct[simp]: @@ -721,7 +722,6 @@ lemma irq_node_offs_range_distinct[simp]: "High_pool_ptr \ irq_node_offs_range" "Silc_cnode_ptr \ irq_node_offs_range" "ntfn_ptr \ irq_node_offs_range" - "irq_cnode_ptr \ irq_node_offs_range" "Low_pd_ptr \ irq_node_offs_range" "High_pd_ptr \ irq_node_offs_range" "Low_pt_ptr \ irq_node_offs_range" @@ -731,30 +731,30 @@ lemma irq_node_offs_range_distinct[simp]: "idle_tcb_ptr \ irq_node_offs_range" "riscv_global_pt_ptr \ irq_node_offs_range" "shared_page_ptr_virt \ irq_node_offs_range" - by(simp add:irq_node_offs_range_def s0_ptr_defs)+ + by (simp add: irq_node_offs_range_def irq_node_size_def irq_len_val cte_level_bits_def + s0_ptr_defs)+ lemma irq_node_offs_distinct[simp]: - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ Low_cnode_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ High_cnode_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ Low_pool_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ High_pool_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ Silc_cnode_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ ntfn_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ irq_cnode_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ Low_pd_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ High_pd_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ Low_pt_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ High_pt_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ Low_tcb_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ High_tcb_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ idle_tcb_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ riscv_global_pt_ptr" - "init_irq_node_ptr + (ucast (irq:: irq) << 5) \ shared_page_ptr_virt" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ Low_cnode_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ High_cnode_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ Low_pool_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ High_pool_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ Silc_cnode_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ ntfn_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ Low_pd_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ High_pd_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ Low_pt_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ High_pt_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ Low_tcb_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ High_tcb_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ idle_tcb_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ riscv_global_pt_ptr" + "init_irq_node_ptr + (ucast (irq::irq) << cte_level_bits) \ shared_page_ptr_virt" by (simp add:not_inD[symmetric, OF _ irq_node_offs_in_range])+ lemma kh0_dom: "dom kh0 = {shared_page_ptr_virt, riscv_global_pt_ptr, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, - High_pt_ptr, Low_pt_ptr, High_pd_ptr, Low_pd_ptr, irq_cnode_ptr, ntfn_ptr, + High_pt_ptr, Low_pt_ptr, High_pd_ptr, Low_pd_ptr, ntfn_ptr, Silc_cnode_ptr, High_pool_ptr, Low_pool_ptr, High_cnode_ptr, Low_cnode_ptr} \ irq_node_offs_range" apply (rule equalityI) @@ -778,7 +778,6 @@ lemma kh0_SomeD: x = Low_pt_ptr \ y = Low_pt \ x = High_pd_ptr \ y = High_pd \ x = Low_pd_ptr \ y = Low_pd \ - x = irq_cnode_ptr \ y = irq_cnode \ x = ntfn_ptr \ y = ntfn \ x = Silc_cnode_ptr \ y = Silc_cnode \ x = High_pool_ptr \ y = High_pool \ @@ -792,7 +791,7 @@ lemma kh0_SomeD: lemmas kh0_obj_def = Low_cnode_def High_cnode_def Silc_cnode_def Low_pool_def High_pool_def Low_pd_def High_pd_def - Low_pt_def High_pt_def Low_tcb_def High_tcb_def idle_tcb_def irq_cnode_def ntfn_def + Low_pt_def High_pt_def Low_tcb_def High_tcb_def idle_tcb_def ntfn_def init_global_pt_def global_pte_def vm_kernel_only_def shared_page_def @@ -831,7 +830,7 @@ definition s0_internal :: "det_ext state" where domain_time = 5, ready_queues = (const (const [])), machine_state = machine_state0, - interrupt_irq_node = (\irq. init_irq_node_ptr + (ucast irq << 5)), + interrupt_irq_node = (\irq. init_irq_node_ptr + (ucast irq << cte_level_bits)), interrupt_states = (\_. irq_state.IRQInactive) (timer_irq := irq_state.IRQTimer), arch_state = arch_state0, exst = exst0 @@ -848,7 +847,6 @@ lemma kh_s0_def: x = Low_pt_ptr \ y = Low_pt \ x = High_pd_ptr \ y = High_pd \ x = Low_pd_ptr \ y = Low_pd \ - x = irq_cnode_ptr \ y = irq_cnode \ x = ntfn_ptr \ y = ntfn \ x = Silc_cnode_ptr \ y = Silc_cnode \ x = High_pool_ptr \ y = High_pool \ @@ -874,7 +872,7 @@ definition Sys1AgentMap :: "(auth_graph_label subject_label) agent_map" where Low_pool_ptr := partition_label Low, High_pool_ptr := partition_label High, ntfn_ptr := partition_label High, - irq_cnode_ptr := partition_label IRQ0, + init_irq_node_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, @@ -890,7 +888,7 @@ lemma Sys1AgentMap_simps: "Sys1AgentMap Low_pool_ptr = partition_label Low" "Sys1AgentMap High_pool_ptr = partition_label High" "Sys1AgentMap ntfn_ptr = partition_label High" - "Sys1AgentMap irq_cnode_ptr = partition_label IRQ0" + "Sys1AgentMap init_irq_node_ptr = partition_label IRQ0" "Sys1AgentMap Silc_cnode_ptr = SilcLabel" "Sys1AgentMap Low_pd_ptr = partition_label Low" "Sys1AgentMap High_pd_ptr = partition_label High" @@ -1110,7 +1108,7 @@ lemma Sys1_pas_refined: apply (intro conjI) apply (simp add: Sys1_pas_wellformed) apply (clarsimp simp: irq_map_wellformed_aux_def s0_internal_def Sys1AgentMap_def Sys1PAS_def) - apply (clarsimp simp: s0_ptr_defs ptr_range_def) + apply (clarsimp simp: s0_ptr_defs ptr_range_def pageBits_def ptTranslationBits_def cte_level_bits_def) apply word_bitwise apply (clarsimp simp: tcb_domain_map_wellformed_aux_def minBound_word High_domain_def Low_domain_def Sys1PAS_def Sys1AgentMap_def default_domain_def) @@ -1204,27 +1202,29 @@ lemma silc_inv_s0: apply (simp add: cte_wp_at_cases s0_internal_def kh0_def kh0_obj_def) apply (case_tac a, clarsimp) apply (clarsimp split: if_splits) - apply ((clarsimp simp: intra_label_cap_def cte_wp_at_cases tcb_cap_cases_def - cap_points_to_label_def split: if_split_asm)+)[8] + apply ((clarsimp simp: intra_label_cap_def cte_wp_at_cases tcb_cap_cases_def + cap_points_to_label_def split: if_split_asm)+)[7] apply (clarsimp simp: intra_label_cap_def cap_points_to_label_def) apply (drule cte_wp_at_caps_of_state' s0_caps_of_state)+ - apply ((erule disjE | - clarsimp simp: Sys1PAS_def Sys1AgentMap_simps - the_nat_to_bl_def nat_to_bl_def ctes_wp_at_def cte_wp_at_cases - s0_internal_def kh0_def kh0_obj_def Silc_caps_well_formed obj_refs_def - | simp add: Silc_caps_def)+)[1] - apply (clarsimp simp: Sys1PAS_def Sys1AgentMap_def) + subgoal + by (erule disjE + | clarsimp simp: Sys1PAS_def Sys1AgentMap_simps + the_nat_to_bl_def nat_to_bl_def ctes_wp_at_def cte_wp_at_cases + s0_internal_def kh0_def kh0_obj_def Silc_caps_well_formed + | simp add: Silc_caps_def)+ + apply (clarsimp simp add: intra_label_cap_def) + apply (clarsimp simp: Sys1PAS_def Sys1AgentMap_def) apply (intro conjI) apply (clarsimp simp: all_children_def s0_internal_def silc_dom_equiv_def equiv_for_refl) apply (clarsimp simp: all_children_def s0_internal_def silc_dom_equiv_def equiv_for_refl) - apply (clarsimp simp: Invariants_AI.cte_wp_at_caps_of_state ) + apply (clarsimp simp: Invariants_AI.cte_wp_at_caps_of_state) by (auto simp:is_transferable.simps dest:s0_caps_of_state) - lemma only_timer_irq_s0: "only_timer_irq timer_irq s0_internal" apply (clarsimp simp: only_timer_irq_def s0_internal_def irq_is_recurring_def is_irq_at_def - irq_at_def Let_def irq_oracle_def machine_state0_def timer_irq_def) + irq_at_def Let_def irq_oracle_def machine_state0_def timer_irq_def + irqInvalid_def) apply presburger done @@ -1294,7 +1294,6 @@ lemma valid_obj_s0[simp]: "valid_obj Low_pool_ptr Low_pool s0_internal" "valid_obj Silc_cnode_ptr Silc_cnode s0_internal" "valid_obj ntfn_ptr ntfn s0_internal" - "valid_obj irq_cnode_ptr irq_cnode s0_internal" "valid_obj Low_pd_ptr Low_pd s0_internal" "valid_obj High_pd_ptr High_pd s0_internal" "valid_obj Low_pt_ptr Low_pt s0_internal" @@ -1304,12 +1303,10 @@ lemma valid_obj_s0[simp]: "valid_obj idle_tcb_ptr idle_tcb s0_internal" "valid_obj riscv_global_pt_ptr init_global_pt s0_internal" "valid_obj shared_page_ptr_virt shared_page s0_internal" - apply (simp_all add: valid_obj_def kh0_obj_def) - apply (simp add: valid_cs_def Low_caps_ran High_caps_ran Silc_caps_ran - valid_cs_size_def word_bits_def cte_level_bits_def)+ - apply (simp add: valid_ntfn_def obj_at_def s0_internal_def kh0_def High_tcb_def is_tcb_def) - apply (simp add: valid_cs_def valid_cs_size_def word_bits_def - cte_level_bits_def well_formed_cnode_n_def) + apply (simp_all add: valid_obj_def kh0_obj_def) + apply (simp add: valid_cs_def Low_caps_ran High_caps_ran Silc_caps_ran + valid_cs_size_def word_bits_def cte_level_bits_def)+ + apply (simp add: valid_ntfn_def obj_at_def s0_internal_def kh0_def High_tcb_def is_tcb_def) apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def valid_tcb_state_def valid_arch_tcb_def is_valid_vtable_root_def is_master_reply_cap_def is_ntfn_def obj_at_def wellformed_pte_def valid_vm_rights_def vm_kernel_only_def @@ -1344,15 +1341,12 @@ lemma pspace_distinct_s0: apply clarsimp apply (clarsimp simp: s0_ptr_defs cte_level_bits_def) apply word_bitwise - apply auto[1] - apply (elim disjE) - (* slow *) - by (simp | clarsimp simp: kh0_obj_def cte_level_bits_def s0_ptr_defs pte_bits_def bit_simps - | fastforce - | clarsimp simp: irq_node_offs_range_def s0_ptr_defs, - drule_tac x="0x1F" in word_plus_strict_mono_right, simp, simp add: add.commute, - drule(1) notE[rotated, OF less_trans, OF _ _ leD, rotated 2] - | drule(1) notE[rotated, OF le_less_trans, OF _ _ leD, rotated 2], simp, assumption)+ + subgoal by auto + (* slow, 289 subgoals after disjE *) + by (elim disjE, + simp_all add: kh0_obj_def cte_level_bits_def s0_ptr_defs pte_bits_def bit_simps; + (clarsimp simp: s0_ptr_defs irq_node_offs_range_def irq_node_size_def irq_len_val + cte_level_bits_def, unat_arith)) lemma valid_pspace_s0[simp]: "valid_pspace s0_internal" @@ -1500,20 +1494,16 @@ lemma valid_irq_node_s0[simp]: apply (rule injI) apply simp apply (rule ccontr) - apply (rule_tac bnd="0x40" and 'a=64 in shift_distinct_helper[rotated 3]) + apply (rule_tac bnd="2^irq_len" and 'a=machine_word_len in shift_distinct_helper[rotated 3]) apply assumption - apply simp - apply simp - apply (rule ucast_less[where 'b=6, simplified]) - apply simp - apply (rule ucast_less[where 'b=6, simplified]) - apply simp + apply (simp add: cte_level_bits_def) + (* safe when irq_len < word_size - cte_level_bits *) + apply (simp add: cte_level_bits_def irq_len_val) + apply (simp add: ucast_irq_bounded_machine_word) + apply (simp add: ucast_irq_bounded_machine_word) apply (rule notI) - apply (drule ucast_up_inj) - apply simp - apply simp - apply (clarsimp simp: obj_at_def s0_internal_def) - apply (force simp: kh0_def is_cap_table_def well_formed_cnode_n_def dom_empty_cnode) + apply (simp add: ucast_up_inj) + apply (force simp: obj_at_def s0_internal_def kh0_def is_cap_table_def well_formed_cnode_n_def) done lemma valid_irq_handlers_s0[simp]: diff --git a/proof/infoflow/Retype_IF.thy b/proof/infoflow/Retype_IF.thy index 3c7aadeeea..914b13a9a2 100644 --- a/proof/infoflow/Retype_IF.thy +++ b/proof/infoflow/Retype_IF.thy @@ -560,7 +560,11 @@ lemma invoke_untyped_reads_respects_g: apply (clarsimp simp: is_cap_simps) apply (rule equiv_valid_guard_imp, rule invoke_untyped_reads_respects_g_wcap) apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state valid_untyped_inv_wcap) - apply auto[1] + (* resolve schematics first, auto and fastforce on their own take forever *) + apply (rule conjI; clarsimp) + apply (rule conjI, (rule refl sym | assumption))+ + apply assumption+ + apply fastforce apply (rule equiv_valid_guard_imp, rule gen_asm_ev'[where Q=False]) apply simp apply (cases ui, clarsimp simp: valid_untyped_inv_wcap cte_wp_at_caps_of_state) diff --git a/proof/infoflow/refine/RISCV64/Example_Valid_StateH.thy b/proof/infoflow/refine/RISCV64/Example_Valid_StateH.thy index 798f038f5a..ece3b6427f 100644 --- a/proof/infoflow/refine/RISCV64/Example_Valid_StateH.thy +++ b/proof/infoflow/refine/RISCV64/Example_Valid_StateH.thy @@ -54,8 +54,8 @@ definition Low_cte' :: "10 word \ cte option" where definition Low_cte :: "obj_ref \ obj_ref \ kernel_object option" where "Low_cte \ \base offs. - if is_aligned offs 5 \ base \ offs \ offs \ base + 2 ^ 15 - 1 - then map_option (\cte. KOCTE cte) (Low_cte' (ucast (offs - base >> 5))) + if is_aligned offs cte_level_bits \ base \ offs \ offs \ base + 2 ^ 15 - 1 + then map_option (\cte. KOCTE cte) (Low_cte' (ucast (offs - base >> cte_level_bits))) else None" @@ -88,8 +88,8 @@ definition High_cte' :: "10 word \ cte option" where definition High_cte :: "obj_ref \ obj_ref \ kernel_object option" where "High_cte \ \base offs. - if is_aligned offs 5 \ base \ offs \ offs \ base + 2 ^ 15 - 1 - then map_option (\cte. KOCTE cte) (High_cte' (ucast (offs - base >> 5))) + if is_aligned offs cte_level_bits \ base \ offs \ offs \ base + 2 ^ 15 - 1 + then map_option (\cte. KOCTE cte) (High_cte' (ucast (offs - base >> cte_level_bits))) else None" @@ -113,8 +113,8 @@ definition Silc_cte' :: "10 word \ cte option" where definition Silc_cte :: "obj_ref \ obj_ref \ kernel_object option" where "Silc_cte \ \base offs. - if is_aligned offs 5 \ base \ offs \ offs \ base + 2 ^ 15 - 1 - then map_option (\cte. KOCTE cte) (Silc_cte' (ucast (offs - base >> 5))) + if is_aligned offs cte_level_bits \ base \ offs \ offs \ base + 2 ^ 15 - 1 + then map_option (\cte. KOCTE cte) (Silc_cte' (ucast (offs - base >> cte_level_bits))) else None" @@ -309,13 +309,12 @@ definition option_update_range :: "('a \ 'b option) \ (' "option_update_range f g \ \x. case f x of None \ g x | Some y \ Some y" definition kh0H :: "(obj_ref \ kernel_object)" where - "kh0H \ (option_update_range (\x. if \irq :: irq. init_irq_node_ptr + (ucast irq << 5) = x - then Some (KOCTE (CTE NullCap Null_mdb)) else None) \ + "kh0H \ (option_update_range (\x. if \irq :: irq. init_irq_node_ptr + (ucast irq << cte_level_bits) = x + then Some (KOCTE irq_cte) else None) \ option_update_range (Low_cte Low_cnode_ptr) \ option_update_range (High_cte High_cnode_ptr) \ option_update_range (Silc_cte Silc_cnode_ptr) \ option_update_range [ntfn_ptr \ KONotification ntfnH] \ - option_update_range [irq_cnode_ptr \ KOCTE irq_cte] \ option_update_range (Low_pdH Low_pd_ptr) \ option_update_range (High_pdH High_pd_ptr) \ option_update_range (Low_ptH Low_pt_ptr) \ @@ -344,10 +343,9 @@ lemma s0_ptrs_aligned: "is_aligned idle_tcb_ptr 10" "is_aligned ntfn_ptr 5" "is_aligned shared_page_ptr_virt 21" - "is_aligned irq_cnode_ptr 10" "is_aligned Low_pool_ptr 12" "is_aligned High_pool_ptr 12" - by (simp add: is_aligned_def s0_ptr_defs)+ + by (simp add: is_aligned_def s0_ptr_defs irq_len_val cte_level_bits_def)+ text \Page offset lemmas\ @@ -620,14 +618,15 @@ lemma cnode_offs_max: definition cnode_offs_range where "cnode_offs_range (ptr :: obj_ref) \ {x. ptr \ x \ x \ ptr + 2 ^ 15 - 1} - \ {x. is_aligned x 5}" + \ {x. is_aligned x cte_level_bits}" lemma cnode_offs_in_range': "\ is_aligned ptr 15; length x = 10 \ \ ptr + of_bl x * 0x20 \ cnode_offs_range ptr" apply (simp add: cnode_offs_min' cnode_offs_max' cnode_offs_range_def add.commute) apply (rule is_aligned_add) apply (erule is_aligned_weaken) - apply simp + apply (simp add: cte_level_bits_def) + apply (simp add: cte_level_bits_def) apply (rule_tac is_aligned_mult_triv2[where x="of_bl x" and n=5, simplified]) done @@ -637,15 +636,15 @@ lemma cnode_offs_in_range: "length x = 10 \ Silc_cnode_ptr + of_bl x * 0x20 \ cnode_offs_range Silc_cnode_ptr" by (simp_all add: cnode_offs_in_range' s0_ptrs_aligned) -lemma le_mask_eq: +lemma le_mask_eq: (* FIXME: move to WordLib or eliminate *) "x \ 2 ^ n - 1 \ x AND mask n = (x :: 'a :: len word)" apply (unfold word_less_alt word_numeral_alt) apply (simp add: word_of_int_power_hom mask_eq_exp_minus_1[symmetric]) apply (erule word_le_mask_eq) done -lemma word_div_mult': - fixes c :: obj_ref +lemma word_div_mult': (* FIXME: move to WordLib or eliminate *) + fixes c :: "'a :: len word" shows "\ 0 < c; a \ b * c \ \ a div c \ b" apply (simp add: word_le_nat_alt unat_div) apply (simp add: less_Suc_eq_le[symmetric]) @@ -671,7 +670,7 @@ lemma cnode_offs_range_correct': apply simp apply (rule word_diff_ls') apply (drule_tac a=x and n=5 in aligned_le_sharp) - apply simp + apply (simp add: cte_level_bits_def) apply (simp add: add.commute) apply (subst(asm) mask_out_add_aligned[symmetric]) apply (erule is_aligned_weaken) @@ -681,7 +680,7 @@ lemma cnode_offs_range_correct': apply (clarsimp simp: neg_mask_is_div[where n=5, simplified, symmetric]) apply (subst is_aligned_neg_mask_eq) apply (rule aligned_sub_aligned) - apply assumption + apply (simp add: cte_level_bits_def) apply (erule is_aligned_weaken) apply simp apply simp @@ -819,81 +818,81 @@ lemma kh0H_dom_distinct: "Low_tcb_ptr \ cnode_offs_range Silc_cnode_ptr" "High_pool_ptr \ cnode_offs_range Silc_cnode_ptr" "Low_pool_ptr \ cnode_offs_range Silc_cnode_ptr" - "irq_cnode_ptr \ cnode_offs_range Silc_cnode_ptr" + "init_irq_node_ptr \ cnode_offs_range Silc_cnode_ptr" "ntfn_ptr \ cnode_offs_range Silc_cnode_ptr" "idle_tcb_ptr \ cnode_offs_range Low_cnode_ptr" "High_tcb_ptr \ cnode_offs_range Low_cnode_ptr" "Low_tcb_ptr \ cnode_offs_range Low_cnode_ptr" "High_pool_ptr \ cnode_offs_range Low_cnode_ptr" "Low_pool_ptr \ cnode_offs_range Low_cnode_ptr" - "irq_cnode_ptr \ cnode_offs_range Low_cnode_ptr" + "init_irq_node_ptr \ cnode_offs_range Low_cnode_ptr" "ntfn_ptr \ cnode_offs_range Low_cnode_ptr" "idle_tcb_ptr \ cnode_offs_range High_cnode_ptr" "High_tcb_ptr \ cnode_offs_range High_cnode_ptr" "Low_tcb_ptr \ cnode_offs_range High_cnode_ptr" "High_pool_ptr \ cnode_offs_range High_cnode_ptr" "Low_pool_ptr \ cnode_offs_range High_cnode_ptr" - "irq_cnode_ptr \ cnode_offs_range High_cnode_ptr" + "init_irq_node_ptr \ cnode_offs_range High_cnode_ptr" "ntfn_ptr \ cnode_offs_range High_cnode_ptr" "idle_tcb_ptr \ pt_offs_range Low_pd_ptr" "High_tcb_ptr \ pt_offs_range Low_pd_ptr" "Low_tcb_ptr \ pt_offs_range Low_pd_ptr" "High_pool_ptr \ pt_offs_range Low_pd_ptr" "Low_pool_ptr \ pt_offs_range Low_pd_ptr" - "irq_cnode_ptr \ pt_offs_range Low_pd_ptr" + "init_irq_node_ptr \ pt_offs_range Low_pd_ptr" "ntfn_ptr \ pt_offs_range Low_pd_ptr" "idle_tcb_ptr \ pt_offs_range High_pd_ptr" "High_tcb_ptr \ pt_offs_range High_pd_ptr" "Low_tcb_ptr \ pt_offs_range High_pd_ptr" "High_pool_ptr \ pt_offs_range High_pd_ptr" "Low_pool_ptr \ pt_offs_range High_pd_ptr" - "irq_cnode_ptr \ pt_offs_range High_pd_ptr" + "init_irq_node_ptr \ pt_offs_range High_pd_ptr" "ntfn_ptr \ pt_offs_range High_pd_ptr" "idle_tcb_ptr \ pt_offs_range riscv_global_pt_ptr" "High_tcb_ptr \ pt_offs_range riscv_global_pt_ptr" "Low_tcb_ptr \ pt_offs_range riscv_global_pt_ptr" "High_pool_ptr \ pt_offs_range riscv_global_pt_ptr" "Low_pool_ptr \ pt_offs_range riscv_global_pt_ptr" - "irq_cnode_ptr \ pt_offs_range riscv_global_pt_ptr" + "init_irq_node_ptr \ pt_offs_range riscv_global_pt_ptr" "ntfn_ptr \ pt_offs_range riscv_global_pt_ptr" "idle_tcb_ptr \ pt_offs_range Low_pt_ptr" "High_tcb_ptr \ pt_offs_range Low_pt_ptr" "Low_tcb_ptr \ pt_offs_range Low_pt_ptr" "High_pool_ptr \ pt_offs_range Low_pt_ptr" "Low_pool_ptr \ pt_offs_range Low_pt_ptr" - "irq_cnode_ptr \ pt_offs_range Low_pt_ptr" + "init_irq_node_ptr \ pt_offs_range Low_pt_ptr" "ntfn_ptr \ pt_offs_range Low_pt_ptr" "idle_tcb_ptr \ pt_offs_range High_pt_ptr" "High_tcb_ptr \ pt_offs_range High_pt_ptr" "Low_tcb_ptr \ pt_offs_range High_pt_ptr" "High_pool_ptr \ pt_offs_range High_pt_ptr" "Low_pool_ptr \ pt_offs_range High_pt_ptr" - "irq_cnode_ptr \ pt_offs_range High_pt_ptr" + "init_irq_node_ptr \ pt_offs_range High_pt_ptr" "ntfn_ptr \ pt_offs_range High_pt_ptr" "idle_tcb_ptr \ tcb_offs_range Low_tcb_ptr" "High_tcb_ptr \ tcb_offs_range Low_tcb_ptr" "High_pool_ptr \ tcb_offs_range Low_tcb_ptr" "Low_pool_ptr \ tcb_offs_range Low_tcb_ptr" - "irq_cnode_ptr \ tcb_offs_range Low_tcb_ptr" + "init_irq_node_ptr \ tcb_offs_range Low_tcb_ptr" "ntfn_ptr \ tcb_offs_range Low_tcb_ptr" "idle_tcb_ptr \ tcb_offs_range High_tcb_ptr" "Low_tcb_ptr \ tcb_offs_range High_tcb_ptr" "High_pool_ptr \ tcb_offs_range High_tcb_ptr" "Low_pool_ptr \ tcb_offs_range High_tcb_ptr" - "irq_cnode_ptr \ tcb_offs_range High_tcb_ptr" + "init_irq_node_ptr \ tcb_offs_range High_tcb_ptr" "ntfn_ptr \ tcb_offs_range High_tcb_ptr" "High_tcb_ptr \ tcb_offs_range idle_tcb_ptr" "Low_tcb_ptr \ tcb_offs_range idle_tcb_ptr" "High_pool_ptr \ tcb_offs_range idle_tcb_ptr" "Low_pool_ptr \ tcb_offs_range idle_tcb_ptr" - "irq_cnode_ptr \ tcb_offs_range idle_tcb_ptr" + "init_irq_node_ptr \ tcb_offs_range idle_tcb_ptr" "ntfn_ptr \ tcb_offs_range idle_tcb_ptr" "idle_tcb_ptr \ page_offs_range shared_page_ptr_virt" "High_tcb_ptr \ page_offs_range shared_page_ptr_virt" "Low_tcb_ptr \ page_offs_range shared_page_ptr_virt" "High_pool_ptr \ page_offs_range shared_page_ptr_virt" "Low_pool_ptr \ page_offs_range shared_page_ptr_virt" - "irq_cnode_ptr \ page_offs_range shared_page_ptr_virt" + "init_irq_node_ptr \ page_offs_range shared_page_ptr_virt" "ntfn_ptr \ page_offs_range shared_page_ptr_virt" by (auto simp: tcb_offs_range_def pt_offs_range_def page_offs_range_def cnode_offs_range_def kh0H_obj_def s0_ptr_defs) @@ -977,9 +976,11 @@ lemma kh0H_dom_sets_distinct: "tcb_offs_range Low_tcb_ptr \ tcb_offs_range idle_tcb_ptr = {}" "tcb_offs_range Low_tcb_ptr \ page_offs_range shared_page_ptr_virt = {}" "page_offs_range shared_page_ptr_virt \ tcb_offs_range idle_tcb_ptr = {}" - by (rule disjointI, clarsimp simp: tcb_offs_range_def pt_offs_range_def page_offs_range_def - irq_node_offs_range_def cnode_offs_range_def s0_ptr_defs - , drule (1) order_trans le_less_trans, fastforce)+ + by (rule disjointI, + clarsimp simp: tcb_offs_range_def pt_offs_range_def page_offs_range_def + irq_node_offs_range_def cnode_offs_range_def s0_ptr_defs + irq_node_size_def irq_len_val cte_level_bits_def, + drule (1) order_trans le_less_trans, fastforce)+ lemmas offs_in_range = pt_offs_in_range page_offs_in_range tcb_offs_in_range cnode_offs_in_range irq_node_offs_in_range @@ -996,63 +997,63 @@ lemma kh0H_dom_distinct': "length x = 10 \ Silc_cnode_ptr + of_bl x * 0x20 \ Low_tcb_ptr" "length x = 10 \ Silc_cnode_ptr + of_bl x * 0x20 \ High_pool_ptr" "length x = 10 \ Silc_cnode_ptr + of_bl x * 0x20 \ Low_pool_ptr" - "length x = 10 \ Silc_cnode_ptr + of_bl x * 0x20 \ irq_cnode_ptr" + "length x = 10 \ Silc_cnode_ptr + of_bl x * 0x20 \ init_irq_node_ptr" "length x = 10 \ Silc_cnode_ptr + of_bl x * 0x20 \ ntfn_ptr" "length x = 10 \ Low_cnode_ptr + of_bl x * 0x20 \ idle_tcb_ptr" "length x = 10 \ Low_cnode_ptr + of_bl x * 0x20 \ High_tcb_ptr" "length x = 10 \ Low_cnode_ptr + of_bl x * 0x20 \ High_pool_ptr" "length x = 10 \ Low_cnode_ptr + of_bl x * 0x20 \ Low_pool_ptr" "length x = 10 \ Low_cnode_ptr + of_bl x * 0x20 \ Low_tcb_ptr" - "length x = 10 \ Low_cnode_ptr + of_bl x * 0x20 \ irq_cnode_ptr" + "length x = 10 \ Low_cnode_ptr + of_bl x * 0x20 \ init_irq_node_ptr" "length x = 10 \ Low_cnode_ptr + of_bl x * 0x20 \ ntfn_ptr" "length x = 10 \ High_cnode_ptr + of_bl x * 0x20 \ idle_tcb_ptr" "length x = 10 \ High_cnode_ptr + of_bl x * 0x20 \ High_tcb_ptr" "length x = 10 \ High_cnode_ptr + of_bl x * 0x20 \ Low_tcb_ptr" "length x = 10 \ High_cnode_ptr + of_bl x * 0x20 \ High_pool_ptr" "length x = 10 \ High_cnode_ptr + of_bl x * 0x20 \ Low_pool_ptr" - "length x = 10 \ High_cnode_ptr + of_bl x * 0x20 \ irq_cnode_ptr" + "length x = 10 \ High_cnode_ptr + of_bl x * 0x20 \ init_irq_node_ptr" "length x = 10 \ High_cnode_ptr + of_bl x * 0x20 \ ntfn_ptr" "Low_pd_ptr + (ucast y << 3) \ idle_tcb_ptr" "Low_pd_ptr + (ucast y << 3) \ High_tcb_ptr" "Low_pd_ptr + (ucast y << 3) \ Low_tcb_ptr" "Low_pd_ptr + (ucast y << 3) \ High_pool_ptr" "Low_pd_ptr + (ucast y << 3) \ Low_pool_ptr" - "Low_pd_ptr + (ucast y << 3) \ irq_cnode_ptr" + "Low_pd_ptr + (ucast y << 3) \ init_irq_node_ptr" "Low_pd_ptr + (ucast y << 3) \ ntfn_ptr" "High_pd_ptr + (ucast y << 3) \ idle_tcb_ptr" "High_pd_ptr + (ucast y << 3) \ High_tcb_ptr" "High_pd_ptr + (ucast y << 3) \ Low_tcb_ptr" "High_pd_ptr + (ucast y << 3) \ High_pool_ptr" "High_pd_ptr + (ucast y << 3) \ Low_pool_ptr" - "High_pd_ptr + (ucast y << 3) \ irq_cnode_ptr" + "High_pd_ptr + (ucast y << 3) \ init_irq_node_ptr" "High_pd_ptr + (ucast y << 3) \ ntfn_ptr" "Low_pt_ptr + (ucast y << 3) \ idle_tcb_ptr" "Low_pt_ptr + (ucast y << 3) \ High_tcb_ptr" "Low_pt_ptr + (ucast y << 3) \ Low_tcb_ptr" "Low_pt_ptr + (ucast y << 3) \ High_pool_ptr" "Low_pt_ptr + (ucast y << 3) \ Low_pool_ptr" - "Low_pt_ptr + (ucast y << 3) \ irq_cnode_ptr" + "Low_pt_ptr + (ucast y << 3) \ init_irq_node_ptr" "Low_pt_ptr + (ucast y << 3) \ ntfn_ptr" "High_pt_ptr + (ucast y << 3) \ idle_tcb_ptr" "High_pt_ptr + (ucast y << 3) \ High_tcb_ptr" "High_pt_ptr + (ucast y << 3) \ Low_tcb_ptr" "High_pt_ptr + (ucast y << 3) \ High_pool_ptr" "High_pt_ptr + (ucast y << 3) \ Low_pool_ptr" - "High_pt_ptr + (ucast y << 3) \ irq_cnode_ptr" + "High_pt_ptr + (ucast y << 3) \ init_irq_node_ptr" "High_pt_ptr + (ucast y << 3) \ ntfn_ptr" "riscv_global_pt_ptr + (ucast y << 3) \ idle_tcb_ptr" "riscv_global_pt_ptr + (ucast y << 3) \ High_tcb_ptr" "riscv_global_pt_ptr + (ucast y << 3) \ Low_tcb_ptr" "riscv_global_pt_ptr + (ucast y << 3) \ High_pool_ptr" "riscv_global_pt_ptr + (ucast y << 3) \ Low_pool_ptr" - "riscv_global_pt_ptr + (ucast y << 3) \ irq_cnode_ptr" + "riscv_global_pt_ptr + (ucast y << 3) \ init_irq_node_ptr" "riscv_global_pt_ptr + (ucast y << 3) \ ntfn_ptr" "shared_page_ptr_virt + (ucast y << 12) \ idle_tcb_ptr" "shared_page_ptr_virt + (ucast y << 12) \ High_tcb_ptr" "shared_page_ptr_virt + (ucast y << 12) \ Low_tcb_ptr" "shared_page_ptr_virt + (ucast y << 12) \ High_pool_ptr" "shared_page_ptr_virt + (ucast y << 12) \ Low_pool_ptr" - "shared_page_ptr_virt + (ucast y << 12) \ irq_cnode_ptr" + "shared_page_ptr_virt + (ucast y << 12) \ init_irq_node_ptr" "shared_page_ptr_virt + (ucast y << 12) \ ntfn_ptr" apply (drule offs_in_range, fastforce simp: kh0H_dom_distinct)+ apply (cut_tac x=y in offs_in_range(1), fastforce simp: kh0H_dom_distinct)+ @@ -1078,9 +1079,9 @@ lemma shared_pageH_KOUserData[simp]: lemma kh0H_simps[simp]: fixes y :: pt_index shows - "kh0H (init_irq_node_ptr + (ucast (irq :: irq) << 5)) = Some (KOCTE (CTE NullCap Null_mdb))" + "kh0H (init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)) = Some (KOCTE irq_cte)" "kh0H ntfn_ptr = Some (KONotification ntfnH)" - "kh0H irq_cnode_ptr = Some (KOCTE irq_cte)" + "kh0H init_irq_node_ptr = Some (KOCTE irq_cte)" "kh0H Low_pool_ptr = Some (KOArch Low_poolH)" "kh0H High_pool_ptr = Some (KOArch High_poolH)" "kh0H Low_tcb_ptr = Some (KOTCB Low_tcbH)" @@ -1096,9 +1097,12 @@ lemma kh0H_simps[simp]: "kh0H (riscv_global_pt_ptr + (ucast y << 3)) = global_ptH riscv_global_pt_ptr (riscv_global_pt_ptr + (ucast y << 3))" "kh0H (shared_page_ptr_virt + (ucast y << 12)) = Some KOUserData" supply option.case_cong[cong] - apply (fastforce simp: kh0H_def option_update_range_def) + apply (fastforce simp: kh0H_def option_update_range_def) + apply (clarsimp simp: kh0H_def kh0H_dom_distinct option_update_range_def not_in_range_None) + apply (clarsimp simp: kh0H_def kh0H_dom_distinct option_update_range_def not_in_range_None) + apply (rule_tac x=0 in exI, simp) by ((clarsimp simp: kh0H_def kh0H_dom_distinct kh0H_dom_distinct' - option_update_range_def not_in_range_None offs_in_range + option_update_range_def not_in_range_None offs_in_range | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_None | rule conjI | clarsimp split: option.splits)+, @@ -1109,7 +1113,7 @@ lemma kh0H_simps[simp]: lemma kh0H_dom: "dom kh0H = {idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, - High_pool_ptr, Low_pool_ptr, irq_cnode_ptr, ntfn_ptr} \ + High_pool_ptr, Low_pool_ptr, ntfn_ptr} \ irq_node_offs_range \ page_offs_range shared_page_ptr_virt \ cnode_offs_range Silc_cnode_ptr \ @@ -1122,17 +1126,20 @@ lemma kh0H_dom: pt_offs_range Low_pt_ptr" apply (rule equalityI) apply (simp add: kh0H_def dom_def) - apply (clarsimp simp: offs_in_range option_update_range_def not_in_range_None split: if_split_asm) + apply (clarsimp simp: offs_in_range option_update_range_def not_in_range_None + simp flip: cte_level_bits_def + split: if_split_asm) apply (clarsimp simp: dom_def) apply (rule conjI) apply (force simp: kh0H_def kh0H_dom_distinct option_update_range_def not_in_range_None + simp flip: cte_level_bits_def dest: irq_node_offs_range_correct split: option.splits) by (rule conjI | clarsimp simp: kh0H_def kh0H_dom_distinct option_update_range_def not_in_range_None - split: option.splits - , frule offs_range_correct - , clarsimp simp: kh0H_all_obj_def cnode_offs_range_def page_offs_range_def pt_offs_range_def - split: if_split_asm)+ + split: option.splits, + frule offs_range_correct, + clarsimp simp: kh0H_all_obj_def cnode_offs_range_def page_offs_range_def pt_offs_range_def + split: if_split_asm)+ lemmas kh0H_SomeD' = set_mp[OF equalityD1[OF kh0H_dom[simplified dom_def]], OF CollectI, simplified, OF exI] @@ -1144,7 +1151,7 @@ lemma kh0H_SomeD: x = idle_tcb_ptr \ y = KOTCB idle_tcbH \ x \ pt_offs_range riscv_global_pt_ptr \ global_ptH riscv_global_pt_ptr x \ None \ y = the (global_ptH riscv_global_pt_ptr x) \ - x \ irq_node_offs_range \ y = KOCTE (CTE NullCap Null_mdb) \ + x \ irq_node_offs_range \ y = KOCTE irq_cte \ x \ pt_offs_range Low_pt_ptr \ Low_ptH Low_pt_ptr x \ None \ y = the (Low_ptH Low_pt_ptr x) \ x \ pt_offs_range High_pt_ptr \ High_ptH High_pt_ptr x \ None \ y = the (High_ptH High_pt_ptr x) \ x \ pt_offs_range Low_pd_ptr \ Low_pdH Low_pd_ptr x \ None \ y = the (Low_pdH Low_pd_ptr x) \ @@ -1154,7 +1161,6 @@ lemma kh0H_SomeD: x \ cnode_offs_range Low_cnode_ptr \ Low_cte Low_cnode_ptr x \ None \ y = the (Low_cte Low_cnode_ptr x) \ x \ cnode_offs_range High_cnode_ptr \ High_cte High_cnode_ptr x \ None \ y = the (High_cte High_cnode_ptr x) \ x \ cnode_offs_range Silc_cnode_ptr \ Silc_cte Silc_cnode_ptr x \ None \ y = the (Silc_cte Silc_cnode_ptr x) \ - x = irq_cnode_ptr \ y = KOCTE irq_cte \ x \ page_offs_range shared_page_ptr_virt \ y = KOUserData" apply (frule kh0H_SomeD') apply (elim disjE) @@ -1172,12 +1178,12 @@ definition s0H_internal :: "kernel_state" where "s0H_internal \ \ ksPSpace = kh0H, gsUserPages = [shared_page_ptr_virt \ RISCVLargePage], - gsCNodes = (\x. if \irq :: irq. init_irq_node_ptr + (ucast irq << 5) = x + gsCNodes = (\x. if \irq :: irq. init_irq_node_ptr + (ucast irq << cte_level_bits) = x then Some 0 else None) (Low_cnode_ptr \ 10, High_cnode_ptr \ 10, Silc_cnode_ptr \ 10, - irq_cnode_ptr \ 0), + init_irq_node_ptr \ 0), gsUntypedZeroRanges = ran (map_comp untypedZeroRange (option_map cteCap o map_to_ctes kh0H)), gsMaxObjectSize = card (UNIV :: obj_ref set), ksDomScheduleIdx = 0, @@ -1198,16 +1204,16 @@ definition s0H_internal :: "kernel_state" where definition Low_cte_cte :: "obj_ref \ obj_ref \ cte option" where - "Low_cte_cte \ \base offs. if is_aligned offs 5 \ base \ offs \ offs \ base + 2 ^ 15 - 1 - then Low_cte' (ucast (offs - base >> 5)) else None" + "Low_cte_cte \ \base offs. if is_aligned offs cte_level_bits \ base \ offs \ offs \ base + 2 ^ 15 - 1 + then Low_cte' (ucast (offs - base >> cte_level_bits)) else None" definition High_cte_cte :: "obj_ref \ obj_ref \ cte option" where - "High_cte_cte \ \base offs. if is_aligned offs 5 \ base \ offs \ offs \ base + 2 ^ 15 - 1 - then High_cte' (ucast (offs - base >> 5)) else None" + "High_cte_cte \ \base offs. if is_aligned offs cte_level_bits \ base \ offs \ offs \ base + 2 ^ 15 - 1 + then High_cte' (ucast (offs - base >> cte_level_bits)) else None" definition Silc_cte_cte :: "obj_ref \ obj_ref \ cte option" where - "Silc_cte_cte \ \base offs. if is_aligned offs 5 \ base \ offs \ offs \ base + 2 ^ 15 - 1 - then Silc_cte' (ucast (offs - base >> 5)) else None" + "Silc_cte_cte \ \base offs. if is_aligned offs cte_level_bits \ base \ offs \ offs \ base + 2 ^ 15 - 1 + then Silc_cte' (ucast (offs - base >> cte_level_bits)) else None" definition Low_tcb_cte :: "obj_ref \ cte option" where "Low_tcb_cte \ [Low_tcb_ptr \ tcbCTable Low_tcbH, @@ -1252,7 +1258,7 @@ lemma set_mem_neq: "\ y \ S; x \ S \ \ x \ y" by fastforce -lemma neg_mask_decompose: +lemma neg_mask_decompose: (* FIXME: move to WordLib *) "x && ~~ mask n = ptr \ x = ptr + (x && mask n)" by (clarsimp simp: AND_NOT_mask_plus_AND_mask_eq) @@ -1260,6 +1266,131 @@ lemma opt_None_not_dom: "m a = None \ a \ dom m" by (simp add: dom_def) + +lemma kh_s0H[simp]: + "ksPSpace s0H_internal = kh0H" + by (simp add: s0H_internal_def) + +lemma s0H_pspace_aligned'[intro!]: + "pspace_aligned' s0H_internal" + supply [simp] = cte_level_bits_def pteBits_def objBits_defs + apply (clarsimp simp: pspace_aligned'_def) + apply (drule kh0H_SomeD) + by (elim disjE; clarsimp simp: s0_ptr_defs kh0H_all_obj_def objBitsKO_def archObjSize_def + cnode_offs_range_def page_offs_range_def pt_offs_range_def + irq_node_offs_range_def is_aligned_mask mask_def bit_simps + split: if_splits) + +interpretation sorted_addrs objBitsKO . + +lemma pspace_aligned'_obj_aligned: + "\ pspace_aligned' s; set addrs = dom (ksPSpace s) \ \ obj_aligned (ksPSpace s) addrs" + unfolding obj_aligned_def pspace_aligned'_def align_of_def + by force + +lemma init_irq_node_ptr_less_size_eq_le_mask: + "(x < init_irq_node_ptr + irq_node_size) = + (x \ init_irq_node_ptr + mask (irq_len + cte_level_bits))" + apply (simp add: init_irq_node_ptr_def irq_node_size_def irq_len_val cte_level_bits_def mask_def + pptr_base_def pptrBase_def canonical_bit_def) + apply unat_arith + done + +lemma aligned_offsets_irq_node_offs_range: + "set (aligned_offsets init_irq_node_ptr (irq_len + cte_level_bits) cte_level_bits) = + irq_node_offs_range" + by (simp add: set_aligned_offsets irq_node_offs_range_def init_irq_node_ptr_less_size_eq_le_mask) + +lemma aligned_offsets_page_offs_range: + "is_aligned p pageBits \ set (aligned_offsets p 21 pageBits) = page_offs_range p" + by (simp add: set_aligned_offsets page_offs_range_def mask_def add.commute pageBits_def) + +lemma aligned_offsets_cnode_offs_range: + "is_aligned p cte_level_bits \ set (aligned_offsets p 15 cte_level_bits) = cnode_offs_range p" + by (simp add: set_aligned_offsets cnode_offs_range_def mask_def add.commute) + +lemma aligned_offsets_pt_offs_range: + "is_aligned p pte_bits \ set (aligned_offsets p 12 pte_bits) = pt_offs_range p" + by (simp add: set_aligned_offsets pt_offs_range_def mask_def add.commute bit_simps) + +definition kh0H_addrs :: "obj_ref list" where + "kh0H_addrs = [ntfn_ptr, Low_tcb_ptr, High_tcb_ptr, idle_tcb_ptr] @ + aligned_offsets riscv_global_pt_ptr 12 pte_bits @ + aligned_offsets Low_pt_ptr 12 pte_bits @ + aligned_offsets High_pt_ptr 12 pte_bits @ + aligned_offsets Low_pd_ptr 12 pte_bits @ + aligned_offsets High_pd_ptr 12 pte_bits @ + [Low_pool_ptr, High_pool_ptr] @ + aligned_offsets Low_cnode_ptr 15 cte_level_bits @ + aligned_offsets High_cnode_ptr 15 cte_level_bits @ + aligned_offsets Silc_cnode_ptr 15 cte_level_bits @ + aligned_offsets init_irq_node_ptr (irq_len + cte_level_bits) cte_level_bits @ + aligned_offsets shared_page_ptr_virt 21 pageBits" + +lemma s0_pt_ptrs_aligned_pte_bits[simp]: + "is_aligned riscv_global_pt_ptr pte_bits" + "is_aligned Low_pt_ptr pte_bits" + "is_aligned High_pt_ptr pte_bits" + "is_aligned Low_pd_ptr pte_bits" + "is_aligned High_pd_ptr pte_bits" + "is_aligned Low_cnode_ptr cte_level_bits" + "is_aligned High_cnode_ptr cte_level_bits" + "is_aligned Silc_cnode_ptr cte_level_bits" + "is_aligned shared_page_ptr_virt pageBits" + by (rule is_aligned_weaken, rule s0_ptrs_aligned, simp add: bit_simps cte_level_bits_def)+ + +lemma offsets_align_s0_ptrs[simp, intro!]: + "offsets_align kh0H (set (aligned_offsets riscv_global_pt_ptr 12 pte_bits)) pte_bits" + "offsets_align kh0H (set (aligned_offsets Low_pt_ptr 12 pte_bits)) pte_bits" + "offsets_align kh0H (set (aligned_offsets High_pt_ptr 12 pte_bits)) pte_bits" + "offsets_align kh0H (set (aligned_offsets Low_pd_ptr 12 pte_bits)) pte_bits" + "offsets_align kh0H (set (aligned_offsets High_pd_ptr 12 pte_bits)) pte_bits" + "offsets_align kh0H (set (aligned_offsets shared_page_ptr_virt 21 pageBits)) pageBits" + "offsets_align kh0H (set (aligned_offsets Low_cnode_ptr 15 cte_level_bits)) cte_level_bits" + "offsets_align kh0H (set (aligned_offsets High_cnode_ptr 15 cte_level_bits)) cte_level_bits" + "offsets_align kh0H (set (aligned_offsets Silc_cnode_ptr 15 cte_level_bits)) cte_level_bits" + "offsets_align kh0H + (set (aligned_offsets init_irq_node_ptr (irq_len + cte_level_bits) cte_level_bits)) + cte_level_bits" + using aligned_offsets_pt_offs_range aligned_offsets_page_offs_range + aligned_offsets_cnode_offs_range aligned_offsets_irq_node_offs_range + cteSizeBits_cte_level_bits + by (clarsimp simp: offsets_align_def s0_ptrs_aligned align_of_def, + prop_tac "p \ dom kh0H", simp add: kh0H_dom, + clarsimp simp: kh0H_obj_def objBits_simps dest!: offs_range_correct split: if_splits)+ + +lemma cte_level_bits_le_cnode_size[simp]: + "cte_level_bits \ 15" + by (simp add: cte_level_bits_def) + +lemma pte_bits_le_pt_size[simp]: + "pte_bits \ 12" + by (simp add: pte_bits_def bit_simps) + +lemma obj_spaced_kh0H_addrs: + "obj_spaced kh0H kh0H_addrs" + supply [simp] = irq_cte_len_leq_word[simplified] s0_ptrs_aligned aligned_offsets_neq_Nil + apply (simp add: kh0H_addrs_def obj_spaced_cons_aligned_offsets obj_spaced_append) + apply (simp add: hd_aligned_offsets hd_aligned_offsets_append) + apply (simp add: aligned_offsets_obj_spaced last_aligned_offests_plus_mask) + apply (simp add: align_of_def objBitsKO_def objBits_defs kh0H_obj_def archObjSize_def bit_simps) + by (simp add: s0_ptr_defs mask_def irq_len_val cte_level_bits_def) (* arithmetic only *) + +lemma dom_eq_kh0H_addrs: + "dom kh0H = set kh0H_addrs" + by (auto simp: kh0H_dom kh0H_addrs_def aligned_offsets_irq_node_offs_range + aligned_offsets_cnode_offs_range aligned_offsets_pt_offs_range + aligned_offsets_page_offs_range) + +lemma s0H_pspace_distinct': + "pspace_distinct' s0H_internal" + apply (clarsimp simp: pspace_distinct'_def ps_clear_def) + apply (rule obj_spaced_distinct[where addrs=kh0H_addrs]; + clarsimp simp: dom_eq_kh0H_addrs obj_spaced_kh0H_addrs + pspace_aligned'_obj_aligned[where s=s0H_internal, simplified] + s0H_pspace_aligned') + done + lemma tcb_offs_range_mask_eq: "\ x \ tcb_offs_range ptr; is_aligned ptr 10 \ \ x && ~~ mask 10 = ptr" apply (drule(1) tcb_offs_range_correct') @@ -1330,18 +1461,54 @@ lemma kh0H_dom_tcb: \ x = Low_tcb_ptr \ x = High_tcb_ptr \ x = idle_tcb_ptr" apply (frule domI[where m="kh0H"]) apply (simp add: kh0H_dom) - apply (elim disjE) - by (auto dest: offs_range_correct simp: kh0H_all_obj_def s0_ptrs_aligned split: if_split_asm) + apply (auto dest: offs_range_correct simp: kh0H_all_obj_def s0_ptrs_aligned split: if_split_asm) + done + +lemma kh0H_ko_aligned: + "kh0H p = Some ko \ is_aligned p (objBitsKO ko)" + using s0H_pspace_aligned' + by (force simp: pspace_aligned'_def) + +lemma kh0H_ko_distinct: + "kh0H p = Some ko \ (mask_range p (objBitsKO ko) - {p}) \ dom kh0H = {}" + using s0H_pspace_distinct' + by (fastforce simp: pspace_distinct'_def ps_clear_def) + +lemma kh0H_cte_aligned: + "kh0H p = Some (KOCTE cte) \ is_aligned p cte_level_bits" + by (clarsimp dest!: kh0H_ko_aligned simp: objBitsKO_def cteSizeBits_cte_level_bits) + +lemma kh0H_cte_distinct: + "kh0H p = Some (KOCTE cte) \ (mask_range p cte_level_bits - {p}) \ dom kh0H = {}" + by (clarsimp dest!: kh0H_ko_distinct simp: objBitsKO_def cteSizeBits_cte_level_bits) + +lemma aligned_plus_1_eq_mask_range: + "\ is_aligned p n; 0 < n \ \ {p + 1..p + mask n} = mask_range p n - {p}" + apply (rule equalityI; clarsimp) + apply (metis aligned_less_plus_1 word_add_increasing word_le_less_eq word_not_le) + apply (metis plus_one_helper word_le_less_eq word_not_le) + done + +lemma kh0_cte_map_to_ctes: + "kh0H p = Some (KOCTE cte) \ map_to_ctes kh0H p = Some cte" + apply (frule kh0H_cte_aligned) + apply (frule kh0H_cte_distinct) + apply (clarsimp simp: map_to_ctes_def Let_def objBitsKO_def cteSizeBits_cte_level_bits + add_mask_fold aligned_plus_1_eq_mask_range) + done + +lemma subset_not_disjointD: + "\ A \ C = {}; B \ C \ {}; B \ A \ \ False" + by blast lemma map_to_ctes_kh0H: "map_to_ctes kh0H = (option_update_range - (\x. if \irq :: irq. init_irq_node_ptr + (ucast irq << 5) = x - then Some (CTE NullCap Null_mdb) else None) \ + (\x. if \irq :: irq. init_irq_node_ptr + (ucast irq << cte_level_bits) = x + then Some irq_cte else None) \ option_update_range (Low_cte_cte Low_cnode_ptr) \ option_update_range (High_cte_cte High_cnode_ptr) \ option_update_range (Silc_cte_cte Silc_cnode_ptr) \ - option_update_range [irq_cnode_ptr \ CTE NullCap Null_mdb] \ option_update_range Low_tcb_cte \ option_update_range High_tcb_cte \ option_update_range idle_tcb_cte @@ -1358,7 +1525,6 @@ lemma map_to_ctes_kh0H: apply (elim disjE) apply (clarsimp simp: option_update_range_def) apply (frule mask_in_tcb_offs_range) - apply (clarsimp simp: kh0H_dom_distinct[THEN set_mem_neq]) apply (simp add: kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None | simp add: kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None)+ apply (rule conjI, clarsimp) @@ -1369,7 +1535,6 @@ lemma map_to_ctes_kh0H: split: if_split_asm dest: neg_mask_decompose) apply (clarsimp simp: option_update_range_def) apply (frule mask_in_tcb_offs_range) - apply (clarsimp simp: kh0H_dom_distinct[THEN set_mem_neq]) apply (simp add: kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None | simp add: kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None)+ apply (rule conjI, clarsimp) @@ -1381,7 +1546,6 @@ lemma map_to_ctes_kh0H: split: if_split_asm dest: neg_mask_decompose) apply (clarsimp simp: option_update_range_def) apply (frule mask_in_tcb_offs_range) - apply (clarsimp simp: kh0H_dom_distinct[THEN set_mem_neq]) apply (simp add: kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None | simp add: kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None)+ apply (rule conjI, clarsimp) @@ -1440,42 +1604,40 @@ lemma map_to_ctes_kh0H: clarsimp simp: option_update_range_def kh0H_dom_distinct[THEN set_mem_neq] not_in_range_cte_None, ((clarsimp simp: kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None irq_node_offs_in_range | clarsimp simp: kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1])+)[5] - prefer 8 + prefer 7 apply ((clarsimp simp: map_to_ctes_def Let_def kh0H_obj_def split del: if_split, subst if_split_eq1, rule conjI, clarsimp, drule kh0H_dom_tcb, fastforce simp: s0_ptr_defs mask_def objBitsKO_def, fastforce simp: option_update_range_def kh0H_dom_distinct not_in_range_cte_None)+)[3] - apply ((clarsimp simp: map_to_ctes_def Let_def kh0H_obj_def objBitsKO_def - split: if_split_asm split del: if_split, - subst if_split_eq1, rule conjI, rule impI, - clarsimp simp: option_update_range_def kh0H_dom_distinct not_in_range_cte_None, - (clarsimp simp: option_update_range_def kh0H_dom_distinct[THEN set_mem_neq] - kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None - | simp add: kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+, - rule conjI, clarsimp, drule offs_range_correct, - fastforce simp: Low_cte_cte_def High_cte_cte_def Silc_cte_cte_def, - rule impI, rule FalseE, drule offs_range_correct, - clarsimp simp: Low_cte_def High_cte_def Silc_cte_def cnode_offs_min cnode_offs_max, - cut_tac x="of_bl y" and z="0x20::obj_ref" and y="2 ^ 15 - 1" in div_to_mult_word_lt, - frule_tac 'a=64 in of_bl_length_le, simp, simp, drule int_not_emptyD, - clarsimp simp: kh0H_dom s0_ptr_defs cnode_offs_range_def page_offs_range_def - pt_offs_range_def irq_node_offs_range_def, - (elim disjE, (clarsimp simp: s0_ptr_defs, - drule_tac b="x + y * 0x20" and n=5 for x y in aligned_le_sharp, - fastforce simp: is_aligned_def, clarsimp simp: add.commute, - subst (asm) mask_out_add_aligned[symmetric], - simp add: is_aligned_mult_triv2[where n=5, simplified], - simp add: mask_def, drule word_leq_le_minus_one, - subst add.commute, rule neq_0_no_wrap, - erule word_plus_mono_right2[rotated], - fastforce, fastforce, fastforce simp: add.commute | unat_arith)+)[1])+)[3] - apply (clarsimp simp: map_to_ctes_def Let_def kh0H_obj_def split del: if_split, - subst if_split_eq1, rule conjI, rule impI, - clarsimp simp: option_update_range_def kh0H_dom_distinct not_in_range_cte_None, rule impI, - clarsimp simp: kh0H_dom objBitsKO_def s0_ptr_defs is_aligned_def page_offs_range_def - cnode_offs_range_def pt_offs_range_def irq_node_offs_range_def, - rule FalseE, drule int_not_emptyD, clarsimp, - (elim disjE, (clarsimp | drule(1) order_trans le_less_trans, fastforce)+)[1]) + (* Low_cnode *) + apply (clarsimp simp: Low_cte_def split: if_split_asm) + apply (frule kh0_cte_map_to_ctes) + apply (clarsimp simp: option_update_range_def) + apply (fastforce simp: Low_cte_cte_def) + (* High_cnode *) + apply (clarsimp simp: High_cte_def split: if_split_asm) + apply (frule kh0_cte_map_to_ctes) + apply (clarsimp simp: option_update_range_def) + apply (rename_tac p cte) + apply (rule conjI; clarsimp) + apply (prop_tac "Low_cte_cte Low_cnode_ptr p = None") + apply (rule not_in_range_cte_None) + apply (erule kh0H_dom_sets_distinct[THEN orthD1]) + apply (clarsimp simp: High_cte_cte_def split: option.split) + (* Silc_cnode *) + apply (clarsimp simp: Silc_cte_def split: if_split_asm) + apply (frule kh0_cte_map_to_ctes) + apply (clarsimp simp: option_update_range_def) + apply (rename_tac p cte) + apply (rule conjI; clarsimp) + apply (prop_tac "Low_cte_cte Low_cnode_ptr p = None") + apply (rule not_in_range_cte_None) + apply (erule kh0H_dom_sets_distinct[THEN orthD1]) + apply (prop_tac "High_cte_cte High_cnode_ptr p = None") + apply (rule not_in_range_cte_None) + apply (erule kh0H_dom_sets_distinct[THEN orthD1]) + apply (clarsimp simp: Silc_cte_cte_def split: option.split) + (* shared_page_ptr_virt *) apply (clarsimp simp: map_to_ctes_def Let_def kh0H_obj_def split del: if_split) apply (subst if_split_eq1) apply (rule conjI, clarsimp) @@ -1483,53 +1645,26 @@ lemma map_to_ctes_kh0H: apply (clarsimp simp: option_update_range_def kh0H_dom_distinct not_in_range_cte_None) apply (rule conjI; clarsimp) apply (rule conjI; clarsimp) - apply (subst is_aligned_neg_mask_eq, clarsimp simp: objBitsKO_def page_offs_range_def is_aligned_weaken)+ - apply (clarsimp split: option.splits) - apply (intro conjI impI; drule kh0H_dom_sets_distinct[THEN orthD2] - kh0H_dom_sets_distinct[THEN orthD1], - drule not_in_range_cte_None, solves clarsimp) - apply (clarsimp simp: map_to_ctes_def Let_def kh0H_obj_def split del: if_split) - apply (frule irq_node_offs_range_correct) - apply (subst if_split_eq1) - apply (rule conjI) - apply (rule impI) - apply (clarsimp simp: option_update_range_def kh0H_dom_distinct not_in_range_cte_None) - apply fastforce - apply (rule impI) - apply clarsimp - apply (erule impE) - apply (rule is_aligned_add) - apply (simp add: is_aligned_def s0_ptr_defs objBitsKO_def) - apply (rule is_aligned_shiftl) - apply (clarsimp simp: objBitsKO_def) - apply (rule FalseE) - apply (clarsimp simp: s0_ptr_defs cnode_offs_range_def page_offs_range_def pt_offs_range_def - irq_node_offs_range_def objBitsKO_def kh0H_dom) - apply (cut_tac x=irq and 'a=64 in ucast_less) - apply simp - apply (drule shiftl_less_t2n'[where n=5]) - apply simp - apply simp - apply (drule plus_one_helper[where n="0x7FF", simplified]) - apply (elim disjE) - apply (unat_arith+)[7] - apply (drule int_not_emptyD) + apply (clarsimp split: option.split) + apply (intro conjI impI; drule kh0H_dom_sets_distinct[THEN orthD2] + kh0H_dom_sets_distinct[THEN orthD1], + drule not_in_range_cte_None, solves clarsimp) + apply (clarsimp simp: page_offs_range_def add_mask_fold) + apply (subst (asm) aligned_plus_1_eq_mask_range, simp) + apply (simp add: objBitsKO_def) + apply (frule kh0H_ko_aligned) + apply (frule kh0H_ko_distinct) + apply (simp add: objBitsKO_def pageBits_def) + apply (drule (1) subset_not_disjointD) + apply (rule Diff_mono; clarsimp) + apply (rule aligned_mask_step; clarsimp simp: is_aligned_weaken is_aligned_no_overflow_mask) + apply (erule FalseE) + (* init_irq_cnode *) apply clarsimp - apply (elim disjE, - ((clarsimp, - drule(1) aligned_le_sharp, - clarsimp simp: add.commute, - subst(asm) mask_out_add_aligned[symmetric], - simp add: is_aligned_shiftl, - simp add: mask_def, - drule word_leq_le_minus_one, - subst add.commute, - rule neq_0_no_wrap, - erule word_plus_mono_right2[rotated], - fastforce, - fastforce, - fastforce simp: add.commute) - | unat_arith)+)[1] + apply (frule kh0_cte_map_to_ctes) + apply (clarsimp simp: option_update_range_def) + apply (frule irq_node_offs_range_correct) + apply fastforce done lemma option_update_range_map_comp: @@ -1541,8 +1676,8 @@ lemma tcb_offs_in_rangeI: by (simp add: tcb_offs_range_def) lemma map_to_ctes_kh0H_simps[simp]: - "map_to_ctes kh0H (init_irq_node_ptr + (ucast (irq :: irq) << 5)) = Some (CTE NullCap Null_mdb)" - "map_to_ctes kh0H irq_cnode_ptr = Some (CTE NullCap Null_mdb)" + "map_to_ctes kh0H (init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)) = + Some irq_cte" "length x = 10 \ map_to_ctes kh0H (Low_cnode_ptr + of_bl x * 0x20) = Low_cte_cte Low_cnode_ptr (Low_cnode_ptr + of_bl x * 0x20)" "length x = 10 \ map_to_ctes kh0H (High_cnode_ptr + of_bl x * 0x20) = @@ -1564,10 +1699,9 @@ lemma map_to_ctes_kh0H_simps[simp]: "map_to_ctes kh0H (idle_tcb_ptr + 0x40) = idle_tcb_cte (idle_tcb_ptr + 0x40)" "map_to_ctes kh0H (idle_tcb_ptr + 0x60) = idle_tcb_cte (idle_tcb_ptr + 0x60)" "map_to_ctes kh0H (idle_tcb_ptr + 0x80) = idle_tcb_cte (idle_tcb_ptr + 0x80)" - supply option.case_cong[cong] if_cong[cong] - apply (clarsimp simp: map_to_ctes_kh0H option_update_range_def) - apply fastforce - apply (clarsimp simp: map_to_ctes_kh0H option_update_range_def kh0H_dom_distinct not_in_range_cte_None) + supply option.case_cong[cong] if_cong[cong] + apply (clarsimp simp: map_to_ctes_kh0H option_update_range_def) + apply fastforce apply ((clarsimp simp: option_update_range_def not_in_range_cte_None cnode_offs_in_range kh0H_dom_distinct kh0H_dom_distinct' map_to_ctes_kh0H s0_ptrs_aligned, ((clarsimp simp: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | @@ -1587,7 +1721,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1595,7 +1728,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1608,7 +1740,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1616,7 +1747,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1629,7 +1759,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1637,7 +1766,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1650,7 +1778,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1658,7 +1785,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1672,7 +1798,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1680,7 +1805,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1693,7 +1817,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1701,7 +1824,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1714,7 +1836,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1722,7 +1843,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1735,7 +1855,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1743,7 +1862,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1757,7 +1875,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1765,7 +1882,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1778,7 +1894,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1786,7 +1901,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1799,7 +1913,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1807,7 +1920,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1820,7 +1932,6 @@ lemma map_to_ctes_kh0H_simps[simp]: apply ((simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None | simp add: offs_in_range kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1] apply (intro conjI impI allI) - apply (simp add: s0_ptr_defs) apply clarsimp apply (drule not_disjointI, rule irq_node_offs_in_range, @@ -1828,7 +1939,6 @@ lemma map_to_ctes_kh0H_simps[simp]: erule notE, rule kh0H_dom_sets_distinct) apply (clarsimp simp: kh0H_dom_distinct) - apply clarsimp by (drule not_disjointI, rule irq_node_offs_in_range, assumption, @@ -1841,8 +1951,7 @@ lemma map_to_ctes_kh0H_dom: Low_tcb_ptr, Low_tcb_ptr + 0x20, Low_tcb_ptr + 0x40, Low_tcb_ptr + 0x60, Low_tcb_ptr + 0x80, High_tcb_ptr, High_tcb_ptr + 0x20, High_tcb_ptr + 0x40, - High_tcb_ptr + 0x60, High_tcb_ptr + 0x80, - irq_cnode_ptr} + High_tcb_ptr + 0x60, High_tcb_ptr + 0x80} \ irq_node_offs_range \ cnode_offs_range Silc_cnode_ptr \ cnode_offs_range High_cnode_ptr @@ -1897,8 +2006,7 @@ lemma map_to_ctes_kh0H_SomeD: x = High_tcb_ptr + 0x40 \ y = (CTE (ReplyCap High_tcb_ptr True True) (MDB 0 0 True True)) \ x = High_tcb_ptr + 0x60 \ y = (CTE NullCap Null_mdb) \ x = High_tcb_ptr + 0x80 \ y = (CTE NullCap Null_mdb) \ - x = irq_cnode_ptr \ y = (CTE NullCap Null_mdb) \ - x \ irq_node_offs_range \ y = (CTE NullCap Null_mdb) \ + x \ irq_node_offs_range \ y = irq_cte \ x \ cnode_offs_range Silc_cnode_ptr \ Silc_cte_cte Silc_cnode_ptr x \ None \ y = the (Silc_cte_cte Silc_cnode_ptr x) \ x \ cnode_offs_range High_cnode_ptr \ High_cte_cte High_cnode_ptr x \ None \ y = the (High_cte_cte High_cnode_ptr x) \ @@ -1921,303 +2029,6 @@ lemma mask_neg_add_aligned': "is_aligned q n \ q + p && ~~ mask n = (p && ~~ mask n) + q" by (simp add: mask_out_add_aligned[symmetric]) -lemma kh_s0H[simp]: - "ksPSpace s0H_internal = kh0H" - by (simp add: s0H_internal_def) - -lemma pspace_distinct'_split: - notes less_1_simp[simp del] shows - "(\(y, ko) \ graph_of (ksPSpace ks). (x \ y \ y + (1 << objBitsKO ko) - 1 < x) - \ y \ y + (1 << objBitsKO ko) - 1) - \ pspace_distinct' (ks \ksPSpace := restrict_map (ksPSpace ks) {..< x}\) - \ pspace_distinct' (ks \ksPSpace := restrict_map (ksPSpace ks) {x ..}\) - \ pspace_distinct' ks" - apply (clarsimp simp: pspace_distinct'_def) - apply (drule bspec, erule graph_ofI, clarsimp) - apply (simp add: Ball_def) - apply (drule_tac x=xa in spec)+ - apply (erule disjE) - apply (simp add: domI) - apply (thin_tac "P \ Q" for P Q) - apply (simp add: ps_clear_def) - apply (erule trans[rotated]) - apply auto[1] - apply (clarsimp simp add: domI) - apply (drule mp, erule(1) order_le_less_trans) - apply (thin_tac "P \ Q" for P Q) - apply (simp add: ps_clear_def) - apply (erule trans[rotated]) - apply (fastforce simp: mask_eq_exp_minus_1 add_diff_eq) - done - -lemma irq_node_offs_range_def2: - "irq_node_offs_range = {x. init_irq_node_ptr \ x \ x \ init_irq_node_ptr + 0x7E0} \ - {x. is_aligned x 5}" - apply (safe, simp_all add: irq_node_offs_range_def add.commute) - by (auto dest: word_less_sub_1 simp: s0_ptr_defs elim: dual_order.strict_trans2[rotated]) - -(* FIXME IF: fix repetitiveness *) -lemma s0H_pspace_distinct': - notes pteBits_def[simp] objBits_defs[simp] - shows "pspace_distinct' s0H_internal" - supply option.case_cong[cong] if_cong[cong] - apply (clarsimp simp: pspace_distinct'_def ps_clear_def mask_eq_exp_minus_1) - apply (rule disjointI) - apply clarsimp - apply (drule kh0H_SomeD)+ - \ \ntfn_ptr\ - apply (erule_tac P="_ \ y = _" in disjE) - subgoal by ((elim disjE; clarsimp), - (thin_tac "_ \ _", clarsimp simp: pt_offs_range_def page_offs_range_def - cnode_offs_range_def irq_node_offs_range_def2 - , drule dual_order.trans, assumption - , clarsimp simp: s0_ptr_defs objBitsKO_def - | solves \clarsimp simp: s0_ptr_defs objBitsKO_def\)+) - \ \Low_tcb_ptr\ - apply (erule_tac P="_ \ y = _" in disjE) - subgoal by ((elim disjE; clarsimp), - (thin_tac "_ \ _", clarsimp simp: pt_offs_range_def page_offs_range_def - cnode_offs_range_def irq_node_offs_range_def2 - , drule dual_order.trans, assumption - , clarsimp simp: s0_ptr_defs objBitsKO_def - | solves \clarsimp simp: s0_ptr_defs objBitsKO_def\)+) - \ \High_tcb_ptr\ - apply (erule_tac P="_ \ y = _" in disjE) - subgoal by ((elim disjE; clarsimp), - (thin_tac "_ \ _", clarsimp simp: pt_offs_range_def page_offs_range_def - cnode_offs_range_def irq_node_offs_range_def2 - , drule dual_order.trans, assumption - , clarsimp simp: s0_ptr_defs objBitsKO_def - | solves \clarsimp simp: s0_ptr_defs objBitsKO_def\)+) - \ \Idle_tcb_ptr\ - apply (erule_tac P="_ \ y = _" in disjE) - subgoal by ((elim disjE; clarsimp), - (thin_tac "_ \ _", clarsimp simp: pt_offs_range_def page_offs_range_def - cnode_offs_range_def irq_node_offs_range_def2 - , drule dual_order.trans, assumption - , clarsimp simp: s0_ptr_defs objBitsKO_def - | solves \clarsimp simp: s0_ptr_defs objBitsKO_def\)+) - \ \riscv_global_pt_ptr\ - apply (erule_tac P="_ \ _ \ y = _" in disjE) - apply (elim disjE; clarsimp) - apply ((clarsimp simp: irq_node_offs_range_def2 pt_offs_range_def objBitsKO_def, - drule dual_order.trans, assumption, - (thin_tac "ya \ _", thin_tac "_ \ ya", - drule_tac b=ya and a="_ + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs)+)[4] - apply (clarsimp simp: pt_offs_range_def objBitsKO_def archObjSize_def kh0H_obj_def bit_simps - split: if_split_asm; - (drule (1) aligned_le_sharp, simp add: mask_neg_add_aligned', fastforce simp: mask_def)) - apply (thin_tac "_ \ _", - clarsimp simp: kh0H_obj_def objBitsKO_def archObjSize_def bit_simps pt_offs_range_def - irq_node_offs_range_def2 cnode_offs_range_def page_offs_range_def, - drule_tac a=x and b="_ + _" in aligned_le_sharp, assumption, - drule dual_order.trans[rotated], - erule word_plus_mono_left, simp add: s0_ptr_defs mask_def, - (drule_tac b=ya and a="(_ && ~~ mask _) + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs mask_def)+ - \ \irq_node_offs_range\ - apply (erule_tac P="_ \ y = _" in disjE) - apply (elim disjE; clarsimp) - apply ((clarsimp simp: irq_node_offs_range_def2 pt_offs_range_def objBitsKO_def, - drule dual_order.trans, assumption, - (thin_tac "ya \ _", thin_tac "_ \ ya", - drule_tac b=ya and a="_ + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs)+)[5] - apply (clarsimp simp: irq_node_offs_range_def objBitsKO_def archObjSize_def kh0H_obj_def - split: if_split_asm; - (drule(1) aligned_le_sharp, simp add: mask_neg_add_aligned', fastforce simp: mask_def)) - apply (thin_tac "_ \ _", - clarsimp simp: kh0H_obj_def objBitsKO_def archObjSize_def bit_simps pt_offs_range_def - irq_node_offs_range_def2 cnode_offs_range_def page_offs_range_def, - drule_tac a=x and b="_ + _" in aligned_le_sharp, assumption, - drule dual_order.trans[rotated], - erule word_plus_mono_left, simp add: s0_ptr_defs mask_def, - (drule_tac b=ya and a="(_ && ~~ mask _) + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs mask_def)+ - \ \Low_pt_ptr\ - apply (erule_tac P="_ \ _ \ y = _" in disjE) - apply (elim disjE; clarsimp) - apply ((clarsimp simp: irq_node_offs_range_def2 pt_offs_range_def objBitsKO_def, - drule dual_order.trans, assumption, - (thin_tac "ya \ _", thin_tac "_ \ ya", - drule_tac b=ya and a="_ + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs)+)[6] - apply (clarsimp simp: pt_offs_range_def objBitsKO_def archObjSize_def kh0H_obj_def bit_simps - split: if_split_asm; - (drule (1) aligned_le_sharp, simp add: mask_neg_add_aligned', fastforce simp: mask_def)) - apply (thin_tac "_ \ _", - clarsimp simp: kh0H_obj_def objBitsKO_def archObjSize_def bit_simps pt_offs_range_def - irq_node_offs_range_def2 cnode_offs_range_def page_offs_range_def, - drule_tac a=x and b="_ + _" in aligned_le_sharp, assumption, - drule dual_order.trans[rotated], - erule word_plus_mono_left, simp add: s0_ptr_defs mask_def, - (drule_tac b=ya and a="(_ && ~~ mask _) + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs mask_def)+ - \ \High_pt_ptr\ - apply (erule_tac P="_ \ _ \ y = _" in disjE) - apply (elim disjE; clarsimp) - apply ((clarsimp simp: irq_node_offs_range_def2 pt_offs_range_def objBitsKO_def, - drule dual_order.trans, assumption, - (thin_tac "ya \ _", thin_tac "_ \ ya", - drule_tac b=ya and a="_ + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs)+)[7] - apply (clarsimp simp: pt_offs_range_def objBitsKO_def archObjSize_def kh0H_obj_def bit_simps - split: if_split_asm; - (drule (1) aligned_le_sharp, simp add: mask_neg_add_aligned', fastforce simp: mask_def)) - apply (thin_tac "_ \ _", - clarsimp simp: kh0H_obj_def objBitsKO_def archObjSize_def bit_simps pt_offs_range_def - irq_node_offs_range_def2 cnode_offs_range_def page_offs_range_def, - drule_tac a=x and b="_ + _" in aligned_le_sharp, assumption, - drule dual_order.trans[rotated], - erule word_plus_mono_left, simp add: s0_ptr_defs mask_def, - (drule_tac b=ya and a="(_ && ~~ mask _) + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs mask_def)+ - \ \Low_pd_ptr\ - apply (erule_tac P="_ \ _ \ y = _" in disjE) - apply (elim disjE; clarsimp) - apply ((clarsimp simp: irq_node_offs_range_def2 pt_offs_range_def objBitsKO_def, - drule dual_order.trans, assumption, - (thin_tac "ya \ _", thin_tac "_ \ ya", - drule_tac b=ya and a="_ + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs)+)[8] - apply (clarsimp simp: pt_offs_range_def objBitsKO_def archObjSize_def kh0H_obj_def bit_simps - split: if_split_asm; - (drule (1) aligned_le_sharp, simp add: mask_neg_add_aligned', fastforce simp: mask_def)) - apply (thin_tac "_ \ _", - clarsimp simp: kh0H_obj_def objBitsKO_def archObjSize_def bit_simps pt_offs_range_def - irq_node_offs_range_def2 cnode_offs_range_def page_offs_range_def, - drule_tac a=x and b="_ + _" in aligned_le_sharp, assumption, - drule dual_order.trans[rotated], - erule word_plus_mono_left, simp add: s0_ptr_defs mask_def, - (drule_tac b=ya and a="(_ && ~~ mask _) + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs mask_def)+ - \ \High_pd_ptr\ - apply (erule_tac P="_ \ _ \ y = _" in disjE) - apply (elim disjE; clarsimp) - apply ((clarsimp simp: irq_node_offs_range_def2 pt_offs_range_def objBitsKO_def, - drule dual_order.trans, assumption, - (thin_tac "ya \ _", thin_tac "_ \ ya", - drule_tac b=ya and a="_ + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs)+)[9] - apply (clarsimp simp: pt_offs_range_def objBitsKO_def archObjSize_def kh0H_obj_def bit_simps - split: if_split_asm; - (drule (1) aligned_le_sharp, simp add: mask_neg_add_aligned', fastforce simp: mask_def)) - apply (thin_tac "_ \ _", - clarsimp simp: kh0H_obj_def objBitsKO_def archObjSize_def bit_simps pt_offs_range_def - irq_node_offs_range_def cnode_offs_range_def page_offs_range_def, - drule_tac a=x and b="_ + _" in aligned_le_sharp, assumption, - drule dual_order.trans[rotated], - erule word_plus_mono_left, simp add: s0_ptr_defs mask_def, - (drule_tac b=ya and a="(_ && ~~ mask _) + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs mask_def)+ - \ \Low_pool_ptr\ - apply (erule_tac P="_ \ y = _" in disjE) - subgoal for x y ya yb - by ((elim disjE; clarsimp), - ((clarsimp simp: irq_node_offs_range_def2 pt_offs_range_def cnode_offs_range_def - page_offs_range_def objBitsKO_def archObjSize_def kh0H_obj_def, - (thin_tac "ya \ _", drule dual_order.trans, assumption | - thin_tac "_ \ ya", drule dual_order.trans, assumption)?, - solves \clarsimp simp: s0_ptr_defs bit_simps\)+)) - \ \High_pool_ptr\ - apply (erule_tac P="_ \ y = _" in disjE) - subgoal for x y ya yb - by ((elim disjE; clarsimp), - ((clarsimp simp: irq_node_offs_range_def2 pt_offs_range_def cnode_offs_range_def - page_offs_range_def objBitsKO_def archObjSize_def kh0H_obj_def, - (thin_tac "ya \ _", drule dual_order.trans, assumption | - thin_tac "_ \ ya", drule dual_order.trans, assumption)?, - solves \clarsimp simp: s0_ptr_defs bit_simps\)+)) - \ \Low_cnode_ptr\ - apply (erule_tac P="_ \ _ \ y = _" in disjE) - apply (elim disjE; clarsimp) - apply ((clarsimp simp: cnode_offs_range_def irq_node_offs_range_def2 - pt_offs_range_def objBitsKO_def, - drule dual_order.trans, assumption, - (thin_tac "ya \ _", thin_tac "_ \ ya", - drule_tac b=ya and a="_ + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs)+)[12] - apply (clarsimp simp: objBitsKO_def kh0H_obj_def Low_cte'_def Low_capsH_def cnode_offs_range_def - split: if_split_asm; - (drule (1) aligned_le_sharp, simp add: mask_neg_add_aligned', fastforce simp: mask_def)) - apply (thin_tac "_ \ _", - clarsimp simp: kh0H_obj_def objBitsKO_def archObjSize_def bit_simps pt_offs_range_def - irq_node_offs_range_def cnode_offs_range_def page_offs_range_def, - drule_tac a=x and b="_ + _" in aligned_le_sharp, assumption, - drule dual_order.trans[rotated], - erule word_plus_mono_left, simp add: s0_ptr_defs mask_def, - (drule_tac b=ya and a="(_ && ~~ mask _) + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs mask_def)+ - \ \High_cnode_ptr\ - apply (erule_tac P="_ \ _ \ y = _" in disjE) - apply (elim disjE; clarsimp) - apply ((clarsimp simp: cnode_offs_range_def irq_node_offs_range_def2 - pt_offs_range_def objBitsKO_def, - drule dual_order.trans, assumption, - (thin_tac "ya \ _", thin_tac "_ \ ya", - drule_tac b=ya and a="_ + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs)+)[13] - apply (clarsimp simp: objBitsKO_def kh0H_obj_def High_cte'_def High_capsH_def cnode_offs_range_def - split: if_split_asm; - (drule (1) aligned_le_sharp, simp add: mask_neg_add_aligned', fastforce simp: mask_def)) - apply (thin_tac "_ \ _", - clarsimp simp: kh0H_obj_def objBitsKO_def archObjSize_def bit_simps pt_offs_range_def - irq_node_offs_range_def cnode_offs_range_def page_offs_range_def, - drule_tac a=x and b="_ + _" in aligned_le_sharp, assumption, - drule dual_order.trans[rotated], - erule word_plus_mono_left, simp add: s0_ptr_defs mask_def, - (drule_tac b=ya and a="(_ && ~~ mask _) + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs mask_def)+ - \ \Silc_cnode_ptr\ - apply (erule_tac P="_ \ _ \ y = _" in disjE) - apply (elim disjE; clarsimp) - apply ((clarsimp simp: cnode_offs_range_def irq_node_offs_range_def2 - pt_offs_range_def objBitsKO_def, - drule dual_order.trans, assumption, - (thin_tac "ya \ _", thin_tac "_ \ ya", - drule_tac b=ya and a="_ + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs)+)[14] - apply (clarsimp simp: objBitsKO_def kh0H_obj_def Silc_cte'_def Silc_capsH_def cnode_offs_range_def - split: if_split_asm; - (drule (1) aligned_le_sharp, simp add: mask_neg_add_aligned', fastforce simp: mask_def)) - apply (thin_tac "_ \ _", - clarsimp simp: kh0H_obj_def objBitsKO_def archObjSize_def bit_simps pt_offs_range_def - irq_node_offs_range_def cnode_offs_range_def page_offs_range_def, - drule_tac a=x and b="_ + _" in aligned_le_sharp, assumption, - drule dual_order.trans[rotated], - erule word_plus_mono_left, simp add: s0_ptr_defs mask_def, - (drule_tac b=ya and a="(_ && ~~ mask _) + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs mask_def)+ - \ \irq_cnode_ptr\ - apply (erule_tac P="_ \ y = _" in disjE) - subgoal for x y ya yb - by ((elim disjE; clarsimp), - ((clarsimp simp: irq_node_offs_range_def2 pt_offs_range_def cnode_offs_range_def - page_offs_range_def objBitsKO_def archObjSize_def kh0H_obj_def, - (thin_tac "ya \ _", drule dual_order.trans, assumption | - thin_tac "_ \ ya", drule dual_order.trans, assumption)?, - solves \clarsimp simp: s0_ptr_defs bit_simps\)+)) - \ \shared_page_ptr\ - apply (elim disjE; clarsimp) - apply ((clarsimp simp: cnode_offs_range_def irq_node_offs_range_def2 - page_offs_range_def pt_offs_range_def objBitsKO_def, - drule dual_order.trans, assumption, - (thin_tac "ya \ _", thin_tac "_ \ ya", - drule_tac b=ya and a="_ + _" in dual_order.trans, assumption)?, - simp add: s0_ptr_defs)+)[16] - apply (clarsimp simp: page_offs_range_def objBitsKO_def archObjSize_def bit_simps) - apply (drule (1) aligned_le_sharp, simp add: mask_neg_add_aligned', fastforce simp: mask_def) - done - -lemma pspace_distinctD'': - "\ \v. ksPSpace s x = Some v \ objBitsKO v = n; pspace_distinct' s \ - \ ps_clear x n s" - apply clarsimp - apply (drule(1) pspace_distinctD') - apply simp - done - lemma cnode_offs_min2': "is_aligned ptr 15 \ (ptr :: obj_ref) \ ptr + 0x20 * (x && mask 10)" apply (erule is_aligned_no_wrap') @@ -2258,7 +2069,8 @@ lemma cnode_offs_max2: lemma cnode_offs_in_range2': "is_aligned ptr 15 \ ptr + 0x20 * (x && mask 10) \ cnode_offs_range ptr" - apply (clarsimp simp: cnode_offs_min2' cnode_offs_max2' cnode_offs_range_def add.commute) + apply (clarsimp simp: cnode_offs_min2' cnode_offs_max2' cnode_offs_range_def cte_level_bits_def + add.commute) apply (rule is_aligned_add) apply (erule is_aligned_weaken) apply simp @@ -2277,21 +2089,21 @@ lemma kh0H_dom_distinct2: "Silc_cnode_ptr + 0x20 * (x && mask 10) \ Low_tcb_ptr" "Silc_cnode_ptr + 0x20 * (x && mask 10) \ High_pool_ptr" "Silc_cnode_ptr + 0x20 * (x && mask 10) \ Low_pool_ptr" - "Silc_cnode_ptr + 0x20 * (x && mask 10) \ irq_cnode_ptr" + "Silc_cnode_ptr + 0x20 * (x && mask 10) \ init_irq_node_ptr" "Silc_cnode_ptr + 0x20 * (x && mask 10) \ ntfn_ptr" "Low_cnode_ptr + 0x20 * (x && mask 10) \ idle_tcb_ptr" "Low_cnode_ptr + 0x20 * (x && mask 10) \ High_tcb_ptr" "Low_cnode_ptr + 0x20 * (x && mask 10) \ Low_tcb_ptr" "Low_cnode_ptr + 0x20 * (x && mask 10) \ High_pool_ptr" "Low_cnode_ptr + 0x20 * (x && mask 10) \ Low_pool_ptr" - "Low_cnode_ptr + 0x20 * (x && mask 10) \ irq_cnode_ptr" + "Low_cnode_ptr + 0x20 * (x && mask 10) \ init_irq_node_ptr" "Low_cnode_ptr + 0x20 * (x && mask 10) \ ntfn_ptr" "High_cnode_ptr + 0x20 * (x && mask 10) \ idle_tcb_ptr" "High_cnode_ptr + 0x20 * (x && mask 10) \ High_tcb_ptr" "High_cnode_ptr + 0x20 * (x && mask 10) \ Low_tcb_ptr" "High_cnode_ptr + 0x20 * (x && mask 10) \ High_pool_ptr" "High_cnode_ptr + 0x20 * (x && mask 10) \ Low_pool_ptr" - "High_cnode_ptr + 0x20 * (x && mask 10) \ irq_cnode_ptr" + "High_cnode_ptr + 0x20 * (x && mask 10) \ init_irq_node_ptr" "High_cnode_ptr + 0x20 * (x && mask 10) \ ntfn_ptr" by (cut_tac x=x in cnode_offs_in_range2(1), fastforce simp: kh0H_dom_distinct | cut_tac x=x in cnode_offs_in_range2(2), fastforce simp: kh0H_dom_distinct @@ -2339,6 +2151,14 @@ lemma less_0x200_exists_ucast: apply clarsimp done +lemma pspace_distinctD'': + "\ \v. ksPSpace s x = Some v \ objBitsKO v = n; pspace_distinct' s \ + \ ps_clear x n s" + apply clarsimp + apply (drule(1) pspace_distinctD') + apply simp + done + lemma valid_caps_s0H[simp]: notes pteBits_def[simp] objBits_defs[simp] shows @@ -2361,7 +2181,7 @@ lemma valid_caps_s0H[simp]: "valid_cap' (NotificationCap ntfn_ptr 0 False True) s0H_internal" "valid_cap' (ReplyCap Low_tcb_ptr True True) s0H_internal" "valid_cap' (ReplyCap High_tcb_ptr True True) s0H_internal" - supply option.case_cong[cong] if_cong[cong] + supply option.case_cong[cong] if_cong[cong] cte_level_bits_def[simp] apply (simp | simp add: valid_cap'_def s0H_internal_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def, intro conjI, simp add: objBitsKO_def s0_ptrs_aligned, simp add: objBitsKO_def, @@ -2369,6 +2189,20 @@ lemma valid_caps_s0H[simp]: rule pspace_distinctD'[OF _ s0H_pspace_distinct', simplified s0H_internal_def], simp)+ apply (simp add: valid_cap'_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def) + apply (intro conjI) + apply (simp add: objBitsKO_def s0_ptrs_aligned) + apply (simp add: objBitsKO_def) + apply (simp add: objBitsKO_def s0_ptrs_aligned mask_def) + apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct']) + apply clarsimp + apply (simp add: valid_cap'_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def) + apply (intro conjI) + apply (simp add: objBitsKO_def s0_ptrs_aligned) + apply (simp add: objBitsKO_def) + apply (simp add: objBitsKO_def s0_ptrs_aligned mask_def) + apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct']) + apply clarsimp + apply (simp add: valid_cap'_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def) apply (intro conjI) apply (simp add: objBitsKO_def s0_ptrs_aligned) apply (simp add: objBitsKO_def) @@ -2424,7 +2258,9 @@ lemma valid_caps_s0H[simp]: by (simp add: valid_cap'_def s0H_internal_def capAligned_def word_bits_def objBits_def obj_at'_def, intro conjI, simp add: objBitsKO_def s0_ptrs_aligned, simp add: objBitsKO_def, simp add: objBitsKO_def s0_ptrs_aligned mask_def, - rule pspace_distinctD'[OF _ s0H_pspace_distinct', simplified s0H_internal_def], simp)+ + rule pspace_distinctD'[OF _ s0H_pspace_distinct', + simplified s0H_internal_def cte_level_bits_def], + simp)+ text \We can only instantiate our example state (featuring high and low domains) if the number of configured domains is > 1, i.e. that maxDomain is 1 or greater. When seL4 is configured for a @@ -2674,39 +2510,40 @@ lemma map_to_ctes_kh0H_simps'[simp]: (MDB (Low_cnode_ptr + 0xA0) (High_cnode_ptr + 0xA0) False False))" "map_to_ctes kh0H (Silc_cnode_ptr + 0x27C0) = Some (CTE (NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 318 * 0x20) (Low_cnode_ptr + 318 * 0x20) False False))" - apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 1", simplified the_nat_to_bl_simps, simplified] + supply cte_level_bits_def[simp] + apply (clarsimp simp: map_to_ctes_kh0H_simps(2)[where x="the_nat_to_bl_10 1", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 2", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(2)[where x="the_nat_to_bl_10 2", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 3", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(2)[where x="the_nat_to_bl_10 3", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 4", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(2)[where x="the_nat_to_bl_10 4", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 5", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(2)[where x="the_nat_to_bl_10 5", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 6", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(2)[where x="the_nat_to_bl_10 6", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 318", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(2)[where x="the_nat_to_bl_10 318", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 1", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 1", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 2", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 2", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 3", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 3", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 4", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 4", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 5", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 5", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 6", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 6", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 318", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 318", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(5)[where x="the_nat_to_bl_10 2", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 2", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(5)[where x="the_nat_to_bl_10 5", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 5", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) - apply (clarsimp simp: map_to_ctes_kh0H_simps(5)[where x="the_nat_to_bl_10 318", simplified the_nat_to_bl_simps, simplified] + apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 318", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) done @@ -2726,17 +2563,20 @@ lemma mdb_next_s0H: apply (elim exE conjE) apply (frule map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all)[1] + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + ucast_shiftr_13E ucast_shiftr_5 s0_ptrs_aligned cte_level_bits_def + split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps - ucast_shiftr_13E ucast_shiftr_5 s0_ptrs_aligned + ucast_shiftr_13E ucast_shiftr_5 s0_ptrs_aligned cte_level_bits_def split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps - ucast_shiftr_5 s0_ptrs_aligned + ucast_shiftr_5 s0_ptrs_aligned cte_level_bits_def split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps - ucast_shiftr_13E ucast_shiftr_5 s0_ptrs_aligned + ucast_shiftr_13E ucast_shiftr_5 s0_ptrs_aligned cte_level_bits_def split: if_split_asm) apply (clarsimp simp: next_unfold' map_to_ctes_kh0H_dom) - apply (elim disjE, simp_all add: kh0H_all_obj_def') + apply (elim disjE, simp_all add: kh0H_all_obj_def')[1] done lemma mdb_prev_s0H: @@ -2755,16 +2595,20 @@ lemma mdb_prev_s0H: apply (elim exE conjE) apply (frule map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all)[1] + apply clarsimp + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + ucast_shiftr_13E ucast_shiftr_5 s0_ptrs_aligned cte_level_bits_def + split: if_split_asm) apply clarsimp apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps - ucast_shiftr_13E ucast_shiftr_5 s0_ptrs_aligned + ucast_shiftr_13E ucast_shiftr_5 s0_ptrs_aligned cte_level_bits_def split: if_split_asm) apply clarsimp - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def ucast_shiftr_13E ucast_shiftr_3 ucast_shiftr_2 s0_ptrs_aligned split: if_split_asm) apply clarsimp - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def ucast_shiftr_5 ucast_shiftr_3 ucast_shiftr_2 s0_ptrs_aligned split: if_split_asm) apply (clarsimp simp: mdb_prev_def map_to_ctes_kh0H_dom) @@ -2784,6 +2628,7 @@ lemma mdb_next_trancl_s0H: p = Low_tcb_ptr + 0x20 \ p' = Low_cnode_ptr + 0x60 \ p = High_tcb_ptr \ p' = High_cnode_ptr + 0x40 \ p = High_tcb_ptr + 0x20 \ p' = High_cnode_ptr + 0x60)" + supply cte_level_bits_def[simp] apply (rule iffI) apply (erule converse_trancl_induct) apply (clarsimp simp: mdb_next_s0H) @@ -2831,67 +2676,79 @@ lemma sameRegionAs_s0H: p = High_cnode_ptr + 0x40 \ p' = High_tcb_ptr \ p = High_tcb_ptr + 0x20 \ p' = High_cnode_ptr + 0x60 \ p = High_cnode_ptr + 0x60 \ p' = High_tcb_ptr + 0x20)" - supply option.case_cong[cong] if_cong[cong] s0_ptrs_aligned[simp] + supply [cong] = option.case_cong if_cong + supply [simp] = s0_ptrs_aligned apply (frule_tac x=p in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all) - apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) - apply (elim disjE, simp_all add: sameRegionAs_def isCap_simps)[1] - apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: if_split_asm) - apply (clarsimp simp: to_bl_use_of_bl the_nat_to_bl_simps kh0H_all_obj_def' ucast_shiftr_2 - split: if_split_asm) + (* p = Low_tcb_ptr (+ x) and p = High_tcb_ptr (+ x) cases *) apply ((frule_tac x=p' in map_to_ctes_kh0H_SomeD, - (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps)[1], - ((clarsimp simp: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps to_bl_use_of_bl + (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps)[1]; + (clarsimp simp: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps to_bl_use_of_bl the_nat_to_bl_simps kh0H_all_obj_def' ucast_shiftr_2 ucast_shiftr_3 - split: if_split_asm)+)[3])+)[5] + cte_level_bits_def + split: if_split_asm))+)[6] + (* init_irq_node *) + apply (clarsimp simp: kh0H_all_obj_def') + (* Silc_cnode_ptr *) apply (clarsimp simp: kh0H_all_obj_def' split: if_split_asm) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def isCap_simps)[1] - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + apply (clarsimp simp: kh0H_all_obj_def') + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_13E; clarsimp) apply (drule(2) ucast_shiftr_13E; clarsimp) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E cte_level_bits_def split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E cte_level_bits_def split: if_split_asm) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def') + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_5; clarsimp) apply (drule(2) ucast_shiftr_5; clarsimp) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_5; clarsimp) apply (drule(2) ucast_shiftr_5; clarsimp) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_5; clarsimp) apply (drule(2) ucast_shiftr_5; clarsimp) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def') + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_2; clarsimp) apply (drule(2) ucast_shiftr_2; clarsimp) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + (* High_cnode_ptr *) apply (clarsimp simp: kh0H_all_obj_def' split: if_split_asm) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def isCap_simps)[1] + apply (clarsimp simp: kh0H_all_obj_def') apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E + cte_level_bits_def + split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + cte_level_bits_def split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (drule(2) ucast_shiftr_13E; clarsimp) apply (drule(2) ucast_shiftr_13E; clarsimp) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E + cte_level_bits_def split: if_split_asm) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] + apply (clarsimp simp: kh0H_all_obj_def') apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 + cte_level_bits_def split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_6; clarsimp) apply (drule(2) ucast_shiftr_6; clarsimp) @@ -2899,128 +2756,164 @@ lemma sameRegionAs_s0H: apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] + apply (clarsimp simp: kh0H_all_obj_def') apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 + cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_5; clarsimp) apply (drule(2) ucast_shiftr_5; clarsimp) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_5; clarsimp) apply (drule(2) ucast_shiftr_5; clarsimp) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_5; clarsimp) apply (drule(2) ucast_shiftr_5; clarsimp) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] + apply (clarsimp simp: kh0H_all_obj_def') apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_4; clarsimp) apply (drule(2) ucast_shiftr_4; clarsimp) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 + cte_level_bits_def) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 + cte_level_bits_def split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_3; clarsimp) apply (drule(2) ucast_shiftr_3; clarsimp) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 - split: if_split_asm) - apply (drule(2) ucast_shiftr_2; clarsimp) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 + cte_level_bits_def + split: if_split_asm) + apply (drule(2) ucast_shiftr_2; clarsimp) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_2; clarsimp) apply (drule(2) ucast_shiftr_2; clarsimp) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] + apply (clarsimp simp: kh0H_all_obj_def') apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 + cte_level_bits_def + split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (drule(2) ucast_shiftr_1; clarsimp) apply (drule(2) ucast_shiftr_1; clarsimp) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + (* Low_cnode_ptr *) apply (clarsimp simp: kh0H_all_obj_def' split: if_split_asm) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def isCap_simps)[1] - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E - split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) - apply (drule(2) ucast_shiftr_13E; clarsimp) - apply (drule(2) ucast_shiftr_13E; clarsimp) + apply (clarsimp simp: kh0H_all_obj_def') + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def split: if_split_asm) + apply (drule(2) ucast_shiftr_13E; clarsimp) + apply (drule(2) ucast_shiftr_13E; clarsimp) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E + cte_level_bits_def + split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E + cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_13E; clarsimp) apply (drule(2) ucast_shiftr_13E; clarsimp) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] + apply (clarsimp simp: kh0H_all_obj_def') apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_6; clarsimp) apply (drule(2) ucast_shiftr_6; clarsimp) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] + apply (clarsimp simp: kh0H_all_obj_def') apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 + cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_5; clarsimp) apply (drule(2) ucast_shiftr_5; clarsimp) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_5; clarsimp) apply (drule(2) ucast_shiftr_5; clarsimp) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def split: if_split_asm) apply (drule(2) ucast_shiftr_5; clarsimp) apply (drule(2) ucast_shiftr_5; clarsimp) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] + apply (clarsimp simp: kh0H_all_obj_def') apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_4; clarsimp) apply (drule(2) ucast_shiftr_4; clarsimp) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 - split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 + cte_level_bits_def + split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_3; clarsimp) apply (drule(2) ucast_shiftr_3; clarsimp) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 - split: if_split_asm) - apply (drule(2) ucast_shiftr_2; clarsimp) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 + cte_level_bits_def + split: if_split_asm) + apply (drule(2) ucast_shiftr_2; clarsimp) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_2; clarsimp) apply (drule(2) ucast_shiftr_2; clarsimp) apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all add: sameRegionAs_def RISCV64_H.sameRegionAs_def isCap_simps split: if_split_asm)[1] - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 - split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 + split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) - apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_1; clarsimp) apply (drule(2) ucast_shiftr_1; clarsimp) done @@ -3039,7 +2932,7 @@ lemma s0H_valid_pspace': assumes "1 \ maxDomain" shows "valid_pspace' s0H_internal" using assms - supply option.case_cong[cong] if_cong[cong] + supply option.case_cong[cong] if_cong[cong] cte_level_bits_def[simp] apply (clarsimp simp: valid_pspace'_def s0H_pspace_distinct' s0H_valid_objs') apply (intro conjI) apply (clarsimp simp: pspace_aligned'_def) @@ -3091,7 +2984,8 @@ lemma s0H_valid_pspace': apply ((rule r_r_into_trancl[OF next_fold next_fold], simp+)+)[2] apply ((erule r_into_trancl[OF next_fold], clarsimp)+)[3] apply ((rule r_r_into_trancl[OF next_fold next_fold], simp+)+)[2] - apply ((erule r_into_trancl[OF next_fold], clarsimp)+)[5] + apply ((erule r_into_trancl[OF next_fold], clarsimp)+)[4] + apply (simp add: irq_cte_def) apply (clarsimp simp: kh0H_all_obj_def Silc_cte_cte_def cnode_offs_range_def split: if_split_asm) apply ((rule r_r_into_trancl[OF next_fold next_fold], simp+)+)[2] @@ -3135,7 +3029,7 @@ lemma s0H_valid_pspace': split: if_split_asm)+)[1] apply (clarsimp simp: caps_contained'_def) apply (drule_tac x=p in map_to_ctes_kh0H_SomeD) - apply (elim disjE, simp_all)[1] + apply (elim disjE, simp_all add: irq_cte_def)[1] apply (clarsimp simp: Silc_cte_cte_def kh0H_all_obj_def split: if_split_asm) apply (clarsimp simp: High_cte_cte_def kh0H_all_obj_def split: if_split_asm) apply (clarsimp simp: Low_cte_cte_def kh0H_all_obj_def split: if_split_asm) @@ -3310,7 +3204,9 @@ lemma s0H_invs: apply (rule_tac x="High_cnode_ptr + 0x20" in exI) apply (clarsimp simp: kh0H_all_obj_def' image_def) apply (rule_tac x="Silc_cnode_ptr + 0x40" in exI) - apply (clarsimp simp: kh0H_all_obj_def' image_def to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' image_def to_bl_use_of_bl the_nat_to_bl_simps + cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_13E, rule s0_ptrs_aligned, simp) apply (rule_tac x="(0x27C0 >> 5)" in bexI) apply simp @@ -3324,7 +3220,9 @@ lemma s0H_invs: apply simp apply (simp add: mask_def) apply (rule_tac x="High_cnode_ptr + 0x40" in exI) - apply (clarsimp simp: kh0H_all_obj_def' image_def to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' image_def to_bl_use_of_bl the_nat_to_bl_simps + cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_13E, rule s0_ptrs_aligned, simp) apply (rule_tac x="0x13E" in bexI) apply simp @@ -3354,7 +3252,9 @@ lemma s0H_invs: apply simp apply (simp add: mask_def) apply (rule_tac x="Low_cnode_ptr + 0x40" in exI) - apply (clarsimp simp: kh0H_all_obj_def' image_def to_bl_use_of_bl the_nat_to_bl_simps split: if_split_asm) + apply (clarsimp simp: kh0H_all_obj_def' image_def to_bl_use_of_bl the_nat_to_bl_simps + cte_level_bits_def + split: if_split_asm) apply (drule(2) ucast_shiftr_13E, rule s0_ptrs_aligned, simp) apply (rule_tac x="0x13E" in bexI) apply simp @@ -3399,13 +3299,14 @@ lemma s0H_invs: apply (rule conjI) apply (clarsimp simp: s0H_internal_def is_aligned_def s0_ptr_defs word_size) apply (clarsimp simp: obj_at'_def objBitsKO_def s0H_internal_def + kh0H_simps(1)[unfolded cte_level_bits_def] shiftl_t2n[where n=4, simplified, symmetric]) apply (rule conjI) apply (rule is_aligned_add) apply (simp add: is_aligned_def s0_ptr_defs) apply (rule is_aligned_shift) apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct', simplified s0H_internal_def]) - apply (simp add: objBitsKO_def) + apply (simp add: objBitsKO_def kh0H_simps(1)[unfolded cte_level_bits_def]) apply (rule conjI) apply (clarsimp simp: valid_irq_handlers'_def cteCaps_of_def ran_def) apply (drule_tac map_to_ctes_kh0H_SomeD) @@ -3416,13 +3317,14 @@ lemma s0H_invs: apply (rule conjI) apply (clarsimp simp: valid_machine_state'_def s0H_internal_def machine_state0_def) apply (rule conjI) - apply (clarsimp simp: irqs_masked'_def s0H_internal_def maxIRQ_def timer_irq_def irqInvalid_def) + using timer_irq_le_maxIRQ + apply (fastforce simp: irqs_masked'_def s0H_internal_def maxIRQ_def ) apply (rule conjI) - apply (clarsimp simp: sym_heap_def opt_map_def projectKOs split: option.splits) + apply (clarsimp simp: sym_heap_def opt_map_def split: option.splits) using kh0H_dom_tcb apply (fastforce simp: kh0H_obj_def) apply (rule conjI) - apply (clarsimp simp: valid_sched_pointers_def opt_map_def projectKOs split: option.splits) + apply (clarsimp simp: valid_sched_pointers_def opt_map_def split: option.splits) using kh0H_dom_tcb apply (fastforce simp: kh0H_obj_def) apply (rule conjI) @@ -3449,9 +3351,13 @@ lemma s0H_invs: apply (simp add: objBitsKO_def) done +lemma well_formed_cnode_n_0[simp]: + "well_formed_cnode_n 0 [[] \ cap]" + by (simp add: well_formed_cnode_n_def) + lemma kh0_pspace_dom: "pspace_dom kh0 = {idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, - High_pool_ptr, Low_pool_ptr, irq_cnode_ptr, ntfn_ptr} \ + High_pool_ptr, Low_pool_ptr, ntfn_ptr} \ irq_node_offs_range \ page_offs_range shared_page_ptr_virt \ cnode_offs_range Silc_cnode_ptr \ @@ -3485,9 +3391,6 @@ lemma kh0_pspace_dom: apply (rule conjI) apply (rule_tac x=Low_pool_ptr in exI) apply (clarsimp simp: kh0_def kh0_obj_def s0_ptr_defs image_def) - apply (rule conjI) - apply (rule_tac x=irq_cnode_ptr in exI) - apply (clarsimp simp: kh0_def kh0_obj_def s0_ptr_defs image_def cte_map_def) apply (rule conjI) apply (rule_tac x=ntfn_ptr in exI) apply (clarsimp simp: kh0_def kh0_obj_def s0_ptr_defs image_def) @@ -3598,50 +3501,48 @@ lemma s0_pspace_rel: apply clarsimp apply (drule kh0_SomeD) apply (elim disjE) - apply (clarsimp simp: kh0_obj_def bit_simps dest!: less_0x200_exists_ucast) - defer - apply ((clarsimp simp: kh0_obj_def kh0H_obj_def bit_simps word_bits_def - fault_rel_optionation_def tcb_relation_cut_def - tcb_relation_def arch_tcb_relation_def the_nat_to_bl_simps - split del: if_split)+)[3] - prefer 13 - apply ((clarsimp simp: kh0_obj_def kh0H_all_obj_def bit_simps add.commute - pt_offs_max pt_offs_min pte_relation_def - split del: if_split, - clarsimp simp: s0_ptr_defs shared_page_ptr_phys_def addrFromPPtr_def pptrBaseOffset_def paddrBase_def - vmrights_map_def vm_read_only_def vm_read_write_def - kh0_obj_def kh0H_all_obj_def elf_index_value, - (clarsimp simp: bit_simps mask_def)?)+)[5] - apply (clarsimp simp: kh0_obj_def kh0H_obj_def well_formed_cnode_n_def - cte_relation_def cte_map_def bit_simps) - apply (clarsimp simp: kh0H_obj_def bit_simps ntfn_def other_obj_relation_def ntfn_relation_def) - defer - apply ((clarsimp simp: kh0_obj_def kh0H_obj_def other_obj_relation_def - asid_pool_relation_def comp_def inv_into_def2 other_aobj_relation_def, - rule ext, - clarsimp simp: asid_low_bits_of_def asid_low_bits_def High_asid_def, - word_bitwise, fastforce)+)[2] + apply (clarsimp simp: kh0_obj_def bit_simps dest!: less_0x200_exists_ucast) + defer + apply ((clarsimp simp: kh0_obj_def kh0H_obj_def bit_simps word_bits_def + fault_rel_optionation_def tcb_relation_cut_def + tcb_relation_def arch_tcb_relation_def the_nat_to_bl_simps + split del: if_split)+)[3] + prefer 12 + apply ((clarsimp simp: kh0_obj_def kh0H_all_obj_def bit_simps add.commute + pt_offs_max pt_offs_min pte_relation_def + split del: if_split, + clarsimp simp: s0_ptr_defs shared_page_ptr_phys_def addrFromPPtr_def pptrBaseOffset_def paddrBase_def + vmrights_map_def vm_read_only_def vm_read_write_def + kh0_obj_def kh0H_all_obj_def elf_index_value, + (clarsimp simp: bit_simps mask_def)?)+)[5] + apply (clarsimp simp: kh0H_obj_def bit_simps ntfn_def other_obj_relation_def ntfn_relation_def) + defer + apply ((clarsimp simp: kh0_obj_def kh0H_obj_def other_obj_relation_def + asid_pool_relation_def comp_def inv_into_def2 other_aobj_relation_def, + rule ext, + clarsimp simp: asid_low_bits_of_def asid_low_bits_def High_asid_def, + word_bitwise, fastforce)+)[2] + apply (clarsimp simp: kh0H_obj_def kh0_obj_def cte_relation_def cte_map_def') + apply (cut_tac dom_caps(2))[1] + apply (frule_tac m=High_caps in domI) + apply (cut_tac x=y in cnode_offs_in_range(2), simp) + apply (clarsimp simp: cnode_offs_range_def kh0H_all_obj_def High_caps_def cte_level_bits_def + the_nat_to_bl_simps vmrights_map_def vm_read_only_def + split: if_split_asm) apply (clarsimp simp: kh0H_obj_def kh0_obj_def cte_relation_def cte_map_def') - apply (cut_tac dom_caps(2))[1] - apply (frule_tac m=High_caps in domI) - apply (cut_tac x=y in cnode_offs_in_range(2), simp) - apply (clarsimp simp: cnode_offs_range_def kh0H_all_obj_def High_caps_def - the_nat_to_bl_simps vmrights_map_def vm_read_only_def + apply (cut_tac dom_caps(3))[1] + apply (frule_tac m=Low_caps in domI) + apply (cut_tac x=y in cnode_offs_in_range(1), simp) + apply (clarsimp simp: cnode_offs_range_def kh0H_all_obj_def Low_caps_def cte_level_bits_def + the_nat_to_bl_simps vmrights_map_def vm_read_write_def split: if_split_asm) - apply (clarsimp simp: kh0H_obj_def kh0_obj_def cte_relation_def cte_map_def') - apply (cut_tac dom_caps(3))[1] - apply (frule_tac m=Low_caps in domI) - apply (cut_tac x=y in cnode_offs_in_range(1), simp) - apply (clarsimp simp: cnode_offs_range_def kh0H_all_obj_def Low_caps_def - the_nat_to_bl_simps vmrights_map_def vm_read_write_def - split: if_split_asm) apply (fastforce simp: kh0H_obj_def cte_map_def cte_relation_def well_formed_cnode_n_def dest: irq_node_offs_range_correct split: if_split_asm) apply (clarsimp simp: kh0H_obj_def kh0_obj_def cte_relation_def cte_map_def') apply (cut_tac dom_caps(1))[1] apply (frule_tac m=Silc_caps in domI) apply (cut_tac x=y in cnode_offs_in_range(3), simp) - apply (clarsimp simp: cnode_offs_range_def kh0H_all_obj_def Silc_caps_def + apply (clarsimp simp: cnode_offs_range_def kh0H_all_obj_def Silc_caps_def cte_level_bits_def the_nat_to_bl_simps vmrights_map_def vm_read_only_def split: if_split_asm) done @@ -3670,23 +3571,19 @@ lemma s0_srel: apply (fastforce simp: kh0_def kh0_obj_def dest: kh0_SomeD) apply clarsimp apply (rule conjI) - apply clarsimp - apply (rule iffI) - apply clarsimp - apply (drule kh0_SomeD) - apply (clarsimp simp: irq_node_offs_in_range) - apply (fastforce simp: kh0_def well_formed_cnode_n_def empty_cnode_def dom_def) + apply (fastforce simp: kh0_def well_formed_cnode_n_def empty_cnode_def dom_def + irq_node_offs_in_range + dest: kh0_SomeD) apply clarsimp apply (clarsimp simp: s0_ptr_defs) apply (subgoal_tac "a \ irq_node_offs_range") prefer 2 - apply (clarsimp simp: irq_node_offs_range_def s0_ptr_defs) - apply (erule_tac x="ucast (a - 0xFFFFFFC000003000 >> 5)" in allE) + apply (clarsimp simp: irq_node_offs_range_def s0_ptr_defs irq_node_size_def irq_len_val cte_level_bits_def) + apply (erule_tac x="ucast (a - 0xFFFFFFC000030000 >> 5)" in allE) apply (subst (asm) ucast_ucast_len) apply (rule shiftr_less_t2n) - apply (rule word_less_sub_right) - apply (erule dual_order.strict_trans[rotated], clarsimp) - apply clarsimp + apply (simp add: is_aligned_def) + apply unat_arith apply (simp add: shiftr_shiftl1) apply (subst(asm) is_aligned_neg_mask_eq) apply (rule aligned_sub_aligned[where n=5]) @@ -3721,8 +3618,8 @@ lemma s0_srel: apply clarsimp apply (drule kh0_SomeD) apply (clarsimp simp: s0_ptr_defs kh0_obj_def) - apply (fastforce simp: kh0_def kh0_obj_def dom_def s0_ptr_defs Silc_caps_def - well_formed_cnode_n_def empty_cnode_def) + apply (fastforce simp: s0_ptr_defs irq_node_offs_range_def cte_level_bits_def + is_aligned_def irq_node_size_def irq_len_val) apply clarsimp apply (drule kh0_SomeD) apply (clarsimp simp: s0_ptr_defs kh0_obj_def) diff --git a/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy b/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy index 68a3273c99..b4af67b425 100644 --- a/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy @@ -45,13 +45,10 @@ lemma decode_irq_control_valid [Interrupt_AI_assms]: split del: if_split cong: if_cong) apply (wpsimp wp: ensure_empty_stronger simp: cte_wp_at_eq_simp arch_irq_control_inv_valid_def | wp (once) hoare_drop_imps)+ - apply (clarsimp simp: linorder_not_less word_le_nat_alt unat_ucast maxIRQ_def) + apply (clarsimp simp: linorder_not_less irq_machine_le_maxIRQ_irq ucast_eq_irqInvalid_conv + maxIRQ_def) apply (cases caps; clarsimp simp: cte_wp_at_eq_simp) - apply (intro conjI impI; clarsimp) - apply (drule ucast_ucast_mask_eq) - apply (subst and_mask_eq_iff_le_mask) - apply (simp add: mask_def word_le_nat_alt) - apply fast + apply fastforce done lemma get_irq_slot_different_ARCH[Interrupt_AI_assms]: diff --git a/proof/invariant-abstract/RISCV64/ArchKernelInit_AI.thy b/proof/invariant-abstract/RISCV64/ArchKernelInit_AI.thy index 7df4fcd825..171b4ff89c 100644 --- a/proof/invariant-abstract/RISCV64/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchKernelInit_AI.thy @@ -59,42 +59,54 @@ lemma pptr_base_num: "pptr_base = 0xFFFFFFC000000000" by (simp add: pptr_base_def pptrBase_def canonical_bit_def) -(* IRQ nodes occupy 11 bits of address space in this RISCV example state: - 6 for irq number, 5 for cte_level_bits. *) +(* Depends on irq_len_val, but needs cte_level_bits. If irq_len is so large that this is not true, + other things will have broken before here, so using _val is safe at this point. *) +lemma irq_cte_len_leq_word: + "irq_len + cte_level_bits < LENGTH(machine_word_len)" + by (simp add: irq_len_val cte_level_bits_def) + +(* IRQ nodes occupy (irq_len + cte_level_bits) bits of address space in this RISCV example state. *) lemma init_irq_ptrs_ineqs: "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \ init_irq_node_ptr" "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + mask cte_level_bits - \ init_irq_node_ptr + mask 11" + \ init_irq_node_ptr + mask (irq_len + cte_level_bits)" "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) - \ init_irq_node_ptr + mask 11" + \ init_irq_node_ptr + mask (irq_len + cte_level_bits)" proof - - have P: "ucast irq < (2 ^ (11 - cte_level_bits) :: machine_word)" - apply (rule order_le_less_trans[OF - ucast_le_ucast[where 'a=6 and 'b=64, simplified, THEN iffD2, OF word_n1_ge]]) - apply (simp add: cte_level_bits_def minus_one_norm) + have [simplified, simp]: + "unat (mask (irq_len + cte_level_bits) :: machine_word) + unat init_irq_node_ptr + < 2 ^ LENGTH(machine_word_len)" + apply (simp only: add.commute) + apply (rule is_aligned_mask_offset_unat, rule is_aligned_init_irq_cte) + apply (simp add: mask_def add.commute) done - show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \ init_irq_node_ptr" - apply (rule is_aligned_no_wrap'[where sz=11]) - apply (simp add: is_aligned_def init_irq_node_ptr_def pptr_base_num) - apply (rule shiftl_less_t2n[OF P]) - apply simp + show "init_irq_node_ptr + (ucast irq << cte_level_bits) \ init_irq_node_ptr" + apply (rule is_aligned_no_wrap'[where sz="irq_len + cte_level_bits"]) + apply (rule is_aligned_init_irq_cte) + apply (rule shiftl_less_t2n) + apply (simp add: ucast_irq_bounded_machine_word) + apply (rule irq_cte_len_leq_word) done - show Q: "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + mask cte_level_bits - \ init_irq_node_ptr + mask 11" - apply (simp only: add_diff_eq[symmetric] add.assoc) + show Q: "init_irq_node_ptr + (ucast irq << cte_level_bits) + mask cte_level_bits + \ init_irq_node_ptr + mask (irq_len + cte_level_bits)" + apply (simp only: add.assoc) apply (rule word_add_le_mono2) apply (simp only: trans [OF shiftl_t2n mult.commute] mask_def mult_1) - apply (rule nasty_split_lt[OF P]) - apply (auto simp: cte_level_bits_def init_irq_node_ptr_def mask_def pptr_base_num) + apply (rule nasty_split_lt) + apply (simp add: ucast_irq_bounded_machine_word) + apply simp + apply (rule irq_cte_len_leq_word) + apply simp done - show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) - \ init_irq_node_ptr + mask 11" + show "init_irq_node_ptr + (ucast irq << cte_level_bits) + \ init_irq_node_ptr + mask (irq_len + cte_level_bits)" apply (simp only: add_diff_eq[symmetric] mask_def mult_1 shiftl_t2n mult.commute) apply (rule word_add_le_mono2) apply (rule word_le_minus_one_leq) - apply (rule shiftl_less_t2n[OF P, simplified shiftl_t2n mult.commute]) - apply simp - apply (simp add: cte_level_bits_def init_irq_node_ptr_def pptr_base_num) + apply (rule shiftl_less_t2n[simplified shiftl_t2n mult.commute]) + apply (simp add: ucast_irq_bounded_machine_word) + apply (rule irq_cte_len_leq_word) + apply (simp flip: mask_2pm1) done qed @@ -505,20 +517,7 @@ lemma irq_node_in_kernel_window_init_arch_state': m \ mask (size (irq::irq)) << cte_level_bits\ \ x \ kernel_window_2 (riscv_kernel_vspace init_arch_state)" apply (clarsimp simp: kernel_window_def init_vspace_uses_def init_arch_state_def) - apply (rule conjI) - apply (clarsimp simp: state_defs) - apply (rule ccontr, simp add:not_le) - apply (drule(1) le_less_trans) - apply (cut_tac is_aligned_no_wrap'[where ptr=pptr_base - and off="0x3000 + m" - and sz=canonical_bit, simplified]) - apply (simp add: add_ac) - apply (auto simp: pptr_base_kernel_elf_base irq_node_pptr_base_kernel_elf_base)[1] - apply (simp add: pptr_base_num canonical_bit_def is_aligned_def) - apply (simp add: pptr_base_num cte_level_bits_def canonical_bit_def mask_def word_size) - apply unat_arith - apply clarsimp - apply (thin_tac "kernel_elf_base \ x \ P" for x P) + apply (subgoal_tac "pptr_base \ x \ x < pptr_base + 2 ^ kernel_window_bits", simp) apply (simp add: cte_level_bits_def canonical_bit_def mask_def init_irq_node_ptr_def pptr_base_num word_size kernel_window_bits_def) apply unat_arith diff --git a/proof/refine/RISCV64/ArchInterrupt_R.thy b/proof/refine/RISCV64/ArchInterrupt_R.thy index fa5192f253..33cbcbdd18 100644 --- a/proof/refine/RISCV64/ArchInterrupt_R.thy +++ b/proof/refine/RISCV64/ArchInterrupt_R.thy @@ -17,7 +17,7 @@ named_theorems Interrupt_R_assms lemma maxIRQ_H_ucast_toEnum_eq_irq[Interrupt_R_assms]: "x \ ucast maxIRQ \ toEnum (unat x) = (ucast x :: irq)" for x::machine_word - by (simp add: word_le_nat_alt maxIRQ_def) + by (simp add: word_le_nat_alt maxIRQ_def maxIRQ_ucast_toEnum_eq_irq) lemma arch_valid_irq_le_maxIRQ[Interrupt_R_assms]: "arch_valid_irq irq \ irq \ maxIRQ" @@ -66,9 +66,7 @@ lemma checkIRQ_irq_valid[Interrupt_R_assms]: supply hoare_vcg_prop[wp del] apply (clarsimp simp: unlessE_def split del: if_split) apply (wpsimp simp: maxIRQ_H_ucast_toEnum_eq_irq) - apply (simp add: not_less word_le_nat_alt unat_ucast_upcast is_up unat_ucast_unat_id - maxIRQ_def irqInvalid_def - flip: word_unat.Rep_inject) + apply (clarsimp simp: maxIRQ_def ucast_eq_irqInvalid_conv irq_machine_le_maxIRQ_irq) done lemma arch_decodeIRQControlInvocation_corres[Interrupt_R_assms]: @@ -126,9 +124,8 @@ lemma arch_decode_irq_control_valid'[Interrupt_R_assms, wp]: | wp whenE_throwError_wp isIRQActive_wp ensureEmptySlot_stronger | wpc | wp (once) hoare_drop_imps)+ - apply (clarsimp simp: invs_valid_objs' not_less maxIRQ_H_ucast_toEnum_eq_irq word_le_nat_alt - unat_ucast_upcast is_up unat_ucast_unat_id maxIRQ_def - simp flip: word_unat.Rep_inject) + apply (clarsimp simp: invs_valid_objs' not_less maxIRQ_def maxIRQ_H_ucast_toEnum_eq_irq + ucast_eq_irqInvalid_conv irq_machine_le_maxIRQ_irq) done crunch Arch.decodeIRQControlInvocation diff --git a/spec/abstract/RISCV64/Init_A.thy b/spec/abstract/RISCV64/Init_A.thy index 464ecb457e..b0e9d83914 100644 --- a/spec/abstract/RISCV64/Init_A.thy +++ b/spec/abstract/RISCV64/Init_A.thy @@ -25,10 +25,17 @@ definition riscv_global_pt_ptr :: obj_ref where "riscv_global_pt_ptr = pptr_base + 0x2000" -(* Sufficiently aligned for irq type + cte_level_bits *) +(* Sufficiently aligned for irq type + cte_level_bits. irq_len can be up to 10, depending on + platform, so we need an alignment of at least 15 bits. *) definition init_irq_node_ptr :: obj_ref where - "init_irq_node_ptr = pptr_base + 0x3000" + "init_irq_node_ptr = pptr_base + 0x30000" + +(* Alignment check *) +lemma is_aligned_init_irq_cte: + "is_aligned init_irq_node_ptr (irq_len + cte_level_bits)" + by (simp add: cte_level_bits_def init_irq_node_ptr_def pptr_base_def pptrBase_def + canonical_bit_def irq_len_val is_aligned_def) (* The highest user-level virtual address that is still canonical. It can be larger than user_vtop, which is the highest address we allow to be mapped. diff --git a/spec/design/m-skel/RISCV64/MachineTypes.thy b/spec/design/m-skel/RISCV64/MachineTypes.thy index 49040d6d2d..ace3f7cbe0 100644 --- a/spec/design/m-skel/RISCV64/MachineTypes.thy +++ b/spec/design/m-skel/RISCV64/MachineTypes.thy @@ -62,7 +62,7 @@ record axiomatization irq_oracle :: "nat \ RISCV64.irq" where - irq_oracle_max_irq: "\n. irq_oracle n <= RISCV64.maxIRQ" + irq_oracle_max_irq: "\n. irq_oracle n <= maxIRQ" end_qualify diff --git a/spec/machine/RISCV64/Arch_Kernel_Config_Lemmas.thy b/spec/machine/RISCV64/Arch_Kernel_Config_Lemmas.thy index ae9fd4d637..89230e7b06 100644 --- a/spec/machine/RISCV64/Arch_Kernel_Config_Lemmas.thy +++ b/spec/machine/RISCV64/Arch_Kernel_Config_Lemmas.thy @@ -42,5 +42,128 @@ lemma kernelELFBase_no_overflow: unfolding kernelELFBase_def kernelELFPAddrBase_def pptrTop_def by (simp add: mask_def Kernel_Config.physBase_def) + +(* maxIRQ lemmas *) + +lemma maxIRQ_less_2p_irqBits: + "(Kernel_Config.maxIRQ::nat) < 2 ^ irqBits" + by (simp add: Kernel_Config.maxIRQ_def Kernel_Config.irqBits_def) + +lemma irqBits_le_12: (* global C bitfield struct limit on maxIRQ *) + "irqBits \ 12" + by (simp add: Kernel_Config.irqBits_def) + +lemma irq_machine_le_maxIRQ_irq: + "irq \ Kernel_Config.maxIRQ \ (ucast irq::irq) \ Kernel_Config.maxIRQ" for irq::machine_word + by (simp add: Kernel_Config.maxIRQ_def word_le_nat_alt unat_ucast) + +lemma maxIRQ_leq_mask_irq_len: + "(Kernel_Config.maxIRQ::machine_word) \ mask LENGTH(irq_len)" + by (simp add: Kernel_Config.maxIRQ_def mask_def) + +lemma unat_2p_irq_len_machine: + "unat (2 ^ irq_len :: machine_word) = 2 ^ irq_len" + by (simp add: irq_len_val) + +lemma unat_irq_bounded: + "unat irq < 2 ^ irq_len" for irq::irq + using unat_lt2p[where 'a=irq_len] + by (simp add: irq_len_val) + +lemma unat_le_2p_irqBits: + "unat irq \ 2 ^ irqBits" for irq :: irq + by (metis irq_len_def nless_le unat_irq_bounded) + +lemma unat_2p_irqBits_machine_word: + "unat (2 ^ irqBits :: machine_word) = 2 ^ irqBits" + using irq_len_def unat_2p_irq_len_machine + by simp + +(* follows from value_type definition of irq_len *) +lemma LENGTH_irq_len_irqBits[simp]: (* [simp] will fire only for simp del: len_of_numeral_defs *) + "LENGTH(irq_len) = irqBits" + using irq_len_def irq_len_val + by simp + +lemma maxIRQ_less_2p_irq_len: + "(Kernel_Config.maxIRQ::nat) < 2^LENGTH(irq_len)" + using maxIRQ_less_2p_irqBits + by (simp del: len_of_numeral_defs) + +(* maxIRQ as a generic numeral allows us to write rules about casts/unat/uint etc without + mentioning numbers: *) + +lemma of_nat_maxIRQ[simp]: + "of_nat Kernel_Config.maxIRQ = (Kernel_Config.maxIRQ::'a::len word)" + by (simp add: Kernel_Config.maxIRQ_def) + +lemma of_int_maxIRQ[simp]: + "of_int Kernel_Config.maxIRQ = (Kernel_Config.maxIRQ::'a::len word)" + by (simp add: Kernel_Config.maxIRQ_def) + +lemma scast_maxIRQ_32_signed_irq[simp]: + "scast (Kernel_Config.maxIRQ :: 32 signed word) = (Kernel_Config.maxIRQ :: irq)" + by (simp add: Kernel_Config.maxIRQ_def) + +lemma scast_maxIRQ_32_signed_machine_word[simp]: + "scast (Kernel_Config.maxIRQ :: 32 signed word) = (Kernel_Config.maxIRQ :: machine_word)" + by (simp add: Kernel_Config.maxIRQ_def) + +(* Safe for [simp] because we don't use maxIRQ at lower than irq_len *) +lemma unat_maxIRQ[simp]: + "LENGTH(irq_len) \ LENGTH('a::len) \ unat (Kernel_Config.maxIRQ::'a word) = Kernel_Config.maxIRQ" + by (metis maxIRQ_less_2p_irq_len Word.of_nat_unat of_nat_inverse of_nat_maxIRQ unat_ucast_up_simp) + +(* Safe for [simp] because we don't use maxIRQ at lower than irq_len *) +lemma uint_maxIRQ[simp]: + "LENGTH(irq_len) \ LENGTH('a::len) \ uint (Kernel_Config.maxIRQ::'a word) = Kernel_Config.maxIRQ" + apply ((solves \clarsimp simp: Kernel_Config.maxIRQ_def\)?) (* proof for maxIRQ = 1 *) + apply (metis Kernel_Config.maxIRQ_def of_nat_numeral uint_nat unat_maxIRQ)? + done + +(* Safe for [simp] because we don't use maxIRQ at lower than irq_len *) +lemma ucast_maxIRQ[simp]: + "\ LENGTH(irq_len) \ LENGTH('a::len); LENGTH(irq_len) \ LENGTH('b::len) \ \ + UCAST ('a \ 'b) Kernel_Config.maxIRQ = Kernel_Config.maxIRQ" + by (metis of_nat_maxIRQ ucast_nat_def unat_maxIRQ) + +(* Safe for [simp] because we don't cast down from irq type *) +lemma maxIRQ_less_upcast[simp]: + "LENGTH(irq_len) \ LENGTH('a::len) \ + (Kernel_Config.maxIRQ < (ucast irq :: 'a word)) = (Kernel_Config.maxIRQ < irq)" for irq::irq + by (simp add: word_less_nat_alt unat_ucast_up_simp) + +(* Safe for [simp] because we don't cast down from irq type *) +lemma maxIRQ_le_upcast[simp]: + "LENGTH(irq_len) \ LENGTH('a::len) \ + ((ucast irq :: 'a word) \ Kernel_Config.maxIRQ) = (irq \ Kernel_Config.maxIRQ)" for irq::irq + by (simp add: word_le_nat_alt unat_ucast_up_simp) + +lemma maxIRQ_ucast_toEnum_eq_irq: + "x \ Kernel_Config.maxIRQ \ toEnum (unat x) = (ucast x :: irq)" for x::machine_word + by (simp add: word_le_nat_alt Kernel_Config.maxIRQ_def) + +lemma Kernel_Config_maxIRQ_ucast_toEnum_eq: + "x \ Kernel_Config.maxIRQ \ toEnum (unat x) = x" for x::machine_word + by (simp add: word_le_nat_alt Kernel_Config.maxIRQ_def) + + +(* The following are derived and no longer need to unfold Kernel_Config constants, + but are small enough to include here *) + +lemma leq_maxIRQ_leq_mask_irq_len: + "x \ Kernel_Config.maxIRQ \ x \ mask LENGTH(irq_len)" for x :: machine_word + by (erule order_trans, rule maxIRQ_leq_mask_irq_len) + +lemma ucast_eq_irqInvalid_conv: + "x \ Kernel_Config.maxIRQ \ (ucast x = irqInvalid) = (x = ucast irqInvalid)" for x :: machine_word + unfolding irqInvalid_def + using leq_maxIRQ_leq_mask_irq_len + by (simp add: ucast_0_eq_left) + +lemma ucast_irq_bounded_machine_word: + "(ucast irq :: machine_word) < 2 ^ irq_len" for irq::irq + by (simp add: word_less_nat_alt unat_ucast_upcast is_up unat_2p_irq_len_machine unat_irq_bounded) + end end diff --git a/spec/machine/RISCV64/MachineOps.thy b/spec/machine/RISCV64/MachineOps.thy index a8d52be684..cd99eadf10 100644 --- a/spec/machine/RISCV64/MachineOps.thy +++ b/spec/machine/RISCV64/MachineOps.thy @@ -135,9 +135,9 @@ definition getActiveIRQ :: "bool \ (irq option) machine_monad" is_masked \ gets $ irq_masks; modify (\s. s \ irq_state := irq_state s + 1 \); active_irq \ gets $ irq_oracle \ irq_state; - if is_masked active_irq \ active_irq = 0xFF \ (in_kernel \ active_irq \ non_kernel_IRQs) + if is_masked active_irq \ active_irq = irqInvalid \ (in_kernel \ active_irq \ non_kernel_IRQs) then return None - else return ((Some active_irq) :: irq option) + else return (Some active_irq) od" definition maskInterrupt :: "bool \ irq \ unit machine_monad" diff --git a/spec/machine/RISCV64/Platform.thy b/spec/machine/RISCV64/Platform.thy index 5535baf670..3e763989f1 100644 --- a/spec/machine/RISCV64/Platform.thy +++ b/spec/machine/RISCV64/Platform.thy @@ -172,9 +172,9 @@ definition minIRQ :: "irq" where "minIRQ \ 0" -definition maxIRQ :: "'a::numeral" - where - "maxIRQ \ 54" +(* maxIRQ is defined via Kernel_Config on this architecture *) +definition maxIRQ :: "'a::numeral" where + "maxIRQ \ Kernel_Config.maxIRQ" (* Reserved by C to represent "not an IRQ" *) definition irqInvalid :: "irq"