From 9659431b5b74427747bd20fb69421843f74e4e78 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 4 Aug 2026 13:15:15 +1000 Subject: [PATCH 1/5] lib: add sorted addresses of non-overlapping objects Useful for reducing proof effort in showing pspace_distinct' and other distinctness properties for concrete states. The auxiliary concept of aligned_offsets (an array of smaller objects making up a larger object) could be useful in the definitions of CNodes, page tables, etc in the design spec. Signed-off-by: Gerwin Klein --- lib/Lib.thy | 1 + lib/ROOT | 1 + lib/Sorted_Addrs.thy | 253 ++++++++++++++++++++++++++ lib/Word_Lib/Word_Lemmas_Internal.thy | 52 ++++++ 4 files changed, 307 insertions(+) create mode 100644 lib/Sorted_Addrs.thy 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 From 02fcaa2a665a37e5bfd16126ca5f4013f1f75336 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 2 Jun 2026 10:05:39 +1000 Subject: [PATCH 2/5] riscv machine+m-skel: maxIRQ declaration + lemmas - add machine declarations for maxIRQ - remove old manual maxIRQ definition - add interface lemmas for maxIRQ Signed-off-by: Gerwin Klein --- spec/design/m-skel/RISCV64/MachineTypes.thy | 2 +- .../RISCV64/Arch_Kernel_Config_Lemmas.thy | 123 ++++++++++++++++++ spec/machine/RISCV64/Platform.thy | 6 +- 3 files changed, 127 insertions(+), 4 deletions(-) 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/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" From 61010777238028e390cdffdb21c72cfc59e78ef6 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 30 Jun 2026 10:25:47 +1000 Subject: [PATCH 3/5] riscv machine: remove incorrect 0xFF in getActiveIRQ Change the definition of getActiveIRQ in RISCV64 to not suppress 0xFF, which was an invalid IRQ of some previous platform. Instead check for symbolic irqInvalid. From the proof perspective, even this check is not necessary, but it models actual hardware behaviour where irqInvalid (= irq 0) is reserved to mean "no IRQ". Signed-off-by: Gerwin Klein --- spec/machine/RISCV64/MachineOps.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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" From 4d530e01d910baba28576481f0a47684ef0538d6 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 2 Jun 2026 10:09:51 +1000 Subject: [PATCH 4/5] riscv aspec: adjustments for generic maxIRQ Increase alignment of IRQ node in example init state and add alignment check lemma (also used later in AInvs). We need to increase alignment, because some platforms have a much larger number of IRQs (>512). Signed-off-by: Gerwin Klein --- spec/abstract/RISCV64/Init_A.thy | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) 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. From a65df3fb012b877afdafb7f584e64c09aba02b73 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 2 Jun 2026 10:11:39 +1000 Subject: [PATCH 5/5] riscv proofs: update for generic maxIRQ Use properties from Arch_Kernel_Config_Lemmas instead of unfolding, which also simplifies most proofs that used these Kernel_Config constants. Improve the pspace_distinct' proof in the infoflow refine state example by making use of the new Sorted_Addresses library. Signed-off-by: Gerwin Klein --- proof/crefine/RISCV64/ADT_C.thy | 16 +- proof/crefine/RISCV64/ArchMove_C.thy | 12 - proof/crefine/RISCV64/CSpace_C.thy | 13 +- proof/crefine/RISCV64/Ctac_lemmas_C.thy | 4 +- proof/crefine/RISCV64/Delete_C.thy | 4 +- proof/crefine/RISCV64/Finalise_C.thy | 38 +- proof/crefine/RISCV64/Interrupt_C.thy | 147 +-- proof/crefine/RISCV64/Syscall_C.thy | 64 +- proof/crefine/RISCV64/Wellformed_C.thy | 9 +- proof/infoflow/RISCV64/ArchCNode_IF.thy | 2 +- .../infoflow/RISCV64/Example_Valid_State.thy | 222 ++-- proof/infoflow/Retype_IF.thy | 6 +- .../refine/RISCV64/Example_Valid_StateH.thy | 1137 ++++++++--------- .../RISCV64/ArchInterrupt_AI.thy | 9 +- .../RISCV64/ArchKernelInit_AI.thy | 73 +- proof/refine/RISCV64/ArchInterrupt_R.thy | 11 +- 16 files changed, 802 insertions(+), 965 deletions(-) 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