1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11theory ArchLevityCatch_AI 12imports 13 "ArchBCorres_AI" 14 "Lib.LemmaBucket" 15 "Lib.SplitRule" 16begin 17 18context Arch begin global_naming ARM 19 20lemma asid_high_bits_of_shift : 21 "asid_high_bits_of (ucast x << asid_low_bits) = x" 22 apply (simp add: asid_high_bits_of_def) 23 apply (rule word_eqI) 24 apply (simp add: word_size nth_ucast nth_shiftr nth_shiftl asid_low_bits_def) 25 done 26 27lemma ptrFormPAddr_addFromPPtr : 28 "ptrFromPAddr (Platform.ARM.addrFromPPtr x) = x" 29 by (simp add: ptrFromPAddr_def Platform.ARM.addrFromPPtr_def) 30 31(****** From GeneralLib *******) 32 33lemma asid_high_bits_of_add_ucast: 34 "is_aligned w asid_low_bits \<Longrightarrow> 35 asid_high_bits_of (ucast (x::10 word) + w) = asid_high_bits_of w" 36 apply (rule word_eqI) 37 apply (simp add: word_size asid_high_bits_of_def nth_ucast nth_shiftr is_aligned_nth) 38 apply (subst word_plus_and_or_coroll) 39 apply (rule word_eqI) 40 apply (clarsimp simp: nth_ucast) 41 apply (drule test_bit_size) 42 apply (simp add: word_size asid_low_bits_def) 43 apply (auto dest: test_bit_size simp: word_size asid_low_bits_def nth_ucast) 44 done 45 46lemma asid_high_bits_of_add: 47 "\<lbrakk>is_aligned w asid_low_bits; x \<le> 2 ^ asid_low_bits - 1\<rbrakk> 48 \<Longrightarrow> asid_high_bits_of (w + x) = asid_high_bits_of w" 49 apply (rule word_eqI) 50 apply (simp add: word_size asid_high_bits_of_def nth_ucast nth_shiftr 51 is_aligned_nth) 52 apply (drule le2p_bits_unset_32, simp add: asid_low_bits_def) 53 apply (subst word_plus_and_or_coroll) 54 apply (rule word_eqI) 55 apply (clarsimp simp: word_size) 56 apply (case_tac "na < asid_low_bits") 57 apply (simp add: asid_low_bits_def linorder_not_less word_bits_def) 58 apply (auto dest: test_bit_size 59 simp: asid_low_bits_def word_bits_def nth_ucast) 60 done 61 62lemma preemption_point_success [simp,intro]: 63 "((Inr (), s') \<in> fst (preemption_point s)) \<Longrightarrow> 64 \<exists>f es. s' = s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>, exst := es \<rparr>" 65 apply (auto simp: in_monad preemption_point_def do_machine_op_def 66 select_f_def select_def getActiveIRQ_def alternative_def 67 do_extended_op_def OR_choiceE_def mk_ef_def 68 split: option.splits if_splits 69 intro: exI[where x=id]) 70 apply (rule_tac x=Suc in exI, rule_tac x="exst bb" in exI, force)+ 71 apply (rule_tac x=id in exI, rule_tac x="exst b" in exI, force)+ 72 done 73 74lemma pageBits_less_word_bits [simp]: 75 "pageBits < word_bits" by (simp add: pageBits_def word_bits_conv) 76 77lemma aobj_ref_arch_cap[simp]: 78 "aobj_ref (arch_default_cap aty ptr us dev) = Some ptr" 79 apply (case_tac aty) 80 apply (simp_all add: aobj_ref_def arch_default_cap_def p_assoc_help) 81 done 82 83 84end 85end 86