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