-
Notifications
You must be signed in to change notification settings - Fork 108
/
Copy pathCSpacePre_AI.thy
211 lines (184 loc) · 8.41 KB
/
CSpacePre_AI.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
(*
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
(*
CSpace invariants preamble
*)
theory CSpacePre_AI
imports ArchCSpaceInv_AI
begin
arch_requalify_consts
cap_asid
is_simple_cap_arch
is_derived_arch
safe_parent_for_arch
cap_asid_base
cap_vptr
arch_requalify_facts
replace_cap_invs
lemma fun_upd_Some:
"ms p = Some k \<Longrightarrow> (ms(a \<mapsto> b)) p = Some (if a = p then b else k)"
by auto
lemma fun_upd_Some_rev:
"\<lbrakk>ms a = Some k; (ms(a \<mapsto> b)) p = Some cap\<rbrakk>
\<Longrightarrow> ms p = Some (if a = p then k else cap)"
by auto
lemma P_bool_lift':
"\<lbrakk>\<lbrace>Q and Q'\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>(\<lambda>s. \<not> Q s) and Q'\<rbrace> f \<lbrace>\<lambda>r s. \<not> Q s\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s. P (Q s) \<and> Q' s\<rbrace> f \<lbrace>\<lambda>r s. P (Q s)\<rbrace>"
apply (clarsimp simp:valid_def)
apply (elim allE)
apply (case_tac "Q s")
apply fastforce+
done
lemma free_index_update_simps[simp]:
"free_index_update g (cap.UntypedCap dev ref sz f) = cap.UntypedCap dev ref sz (g f)"
by (simp add:free_index_update_def)
(* FIXME: MOVE*)
lemma is_cap_free_index_update[simp]:
"is_zombie (src_cap\<lparr>free_index := f \<rparr>) = is_zombie src_cap"
"is_cnode_cap (src_cap\<lparr>free_index := f \<rparr>) = is_cnode_cap src_cap"
"is_thread_cap (src_cap\<lparr>free_index := f \<rparr>) = is_thread_cap src_cap"
"is_domain_cap (src_cap\<lparr>free_index := f \<rparr>) = is_domain_cap src_cap"
"is_ep_cap (src_cap\<lparr>free_index := f \<rparr>) = is_ep_cap src_cap"
"is_untyped_cap (src_cap\<lparr>free_index := f \<rparr>) = is_untyped_cap src_cap"
"is_arch_cap (src_cap\<lparr>free_index := f \<rparr>) = is_arch_cap src_cap"
"is_zombie (src_cap\<lparr>free_index := f \<rparr>) = is_zombie src_cap"
"is_ntfn_cap (src_cap\<lparr>free_index := f \<rparr>) = is_ntfn_cap src_cap"
"is_reply_cap (src_cap\<lparr>free_index := f \<rparr>) = is_reply_cap src_cap"
"is_master_reply_cap (src_cap\<lparr>free_index := f \<rparr>) = is_master_reply_cap src_cap"
by (simp add:is_cap_simps free_index_update_def split:cap.splits)+
lemma masked_as_full_simps[simp]:
"masked_as_full (cap.EndpointCap r badge a) cap = (cap.EndpointCap r badge a)"
"masked_as_full (cap.Zombie r bits n) cap = (cap.Zombie r bits n)"
"masked_as_full (cap.ArchObjectCap x) cap = (cap.ArchObjectCap x)"
"masked_as_full (cap.CNodeCap r n g) cap = (cap.CNodeCap r n g)"
"masked_as_full (cap.ReplyCap r m a) cap = (cap.ReplyCap r m a)"
"masked_as_full cap.NullCap cap = cap.NullCap"
"masked_as_full cap.DomainCap cap = cap.DomainCap"
"masked_as_full (cap.ThreadCap r) cap = cap.ThreadCap r"
"masked_as_full cap (cap.EndpointCap r badge a) = cap"
"masked_as_full cap (cap.Zombie r bits n) = cap"
"masked_as_full cap (cap.ArchObjectCap x) = cap"
"masked_as_full cap (cap.CNodeCap r n g) = cap"
"masked_as_full cap (cap.ReplyCap r m a) = cap"
"masked_as_full cap cap.NullCap = cap"
"masked_as_full cap cap.DomainCap = cap"
"masked_as_full cap (cap.ThreadCap r) = cap"
by (simp add:masked_as_full_def)+
lemma maksed_as_full_test_function_stuff[simp]:
"gen_obj_refs (masked_as_full a cap) = gen_obj_refs a"
"cap_asid (masked_as_full a cap ) = cap_asid a"
"obj_refs (masked_as_full a cap ) = obj_refs a"
"is_zombie (masked_as_full a cap ) = is_zombie a"
"is_cnode_cap (masked_as_full a cap ) = is_cnode_cap a"
"is_thread_cap (masked_as_full a cap ) = is_thread_cap a"
"is_domain_cap (masked_as_full a cap ) = is_domain_cap a"
"is_ep_cap (masked_as_full a cap ) = is_ep_cap a"
"is_untyped_cap (masked_as_full a cap ) = is_untyped_cap a"
"is_arch_cap (masked_as_full a cap ) = is_arch_cap a"
"is_zombie (masked_as_full a cap ) = is_zombie a"
"is_ntfn_cap (masked_as_full a cap ) = is_ntfn_cap a"
"is_reply_cap (masked_as_full a cap ) = is_reply_cap a"
"is_master_reply_cap (masked_as_full a cap ) = is_master_reply_cap a"
by (auto simp:masked_as_full_def)
lemma set_untyped_cap_as_full_cte_wp_at_neg:
"\<lbrace>\<lambda>s. (dest \<noteq> src \<and> \<not> (cte_wp_at P dest s) \<or>
dest = src \<and> \<not> cte_wp_at (\<lambda>a. P (masked_as_full a cap)) src s) \<and>
cte_wp_at ((=) src_cap) src s\<rbrace>
set_untyped_cap_as_full src_cap cap src
\<lbrace>\<lambda>ya s. \<not> cte_wp_at P dest s\<rbrace>"
apply (clarsimp simp:set_untyped_cap_as_full_def | rule conjI |wp set_cap_cte_wp_at_neg)+
apply (clarsimp simp:cte_wp_at_caps_of_state masked_as_full_def)+
apply wp
apply clarsimp
done
lemma set_untyped_cap_as_full_is_final_cap'_neg:
"\<lbrace>\<lambda>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s\<rbrace>
set_untyped_cap_as_full src_cap cap src
\<lbrace>\<lambda>rv s. \<not> is_final_cap' cap' s\<rbrace>"
apply (rule hoare_pre)
apply (simp add:is_final_cap'_def2)
apply (wp hoare_vcg_all_lift hoare_vcg_ex_lift)
apply (rule_tac Q = "cte_wp_at Q slot"
and Q'="cte_wp_at ((=) src_cap) src" for Q slot in P_bool_lift' )
apply (wp set_untyped_cap_as_full_cte_wp_at)
apply clarsimp
apply (wp set_untyped_cap_as_full_cte_wp_at_neg)
apply (clarsimp simp:cte_wp_at_caps_of_state masked_as_full_def)
apply (clarsimp simp:is_final_cap'_def2)
done
lemma set_cap_def2:
"set_cap cap = (\<lambda>(oref, cref). do
obj \<leftarrow> get_object oref;
obj' \<leftarrow> (case (obj, tcb_cap_cases cref) of
(CNode sz cs, _) \<Rightarrow> if cref \<in> dom cs \<and> well_formed_cnode_n sz cs
then return $ CNode sz $ cs(cref \<mapsto> cap)
else fail
| (TCB tcb, Some (getF, setF, restr)) \<Rightarrow> return $ TCB (setF (\<lambda>x. cap) tcb)
| _ \<Rightarrow> fail);
set_object oref obj'
od)"
apply (rule ext, simp add: set_cap_def split_def)
apply (intro bind_cong bind_apply_cong refl)
apply (simp split: Structures_A.kernel_object.split)
apply (simp add: tcb_cap_cases_def)
done
lemmas cap_insert_typ_ats [wp] = abs_typ_at_lifts [OF cap_insert_typ_at]
definition
"is_simple_cap cap \<equiv>
cap \<noteq> cap.NullCap \<and> cap \<noteq> cap.IRQControlCap \<and> \<not>is_untyped_cap cap \<and>
\<not>is_master_reply_cap cap \<and> \<not>is_reply_cap cap \<and>
\<not>is_ep_cap cap \<and> \<not>is_ntfn_cap cap \<and>
\<not>is_thread_cap cap \<and> \<not>is_cnode_cap cap \<and> \<not>is_zombie cap \<and>
is_simple_cap_arch cap"
definition
"safe_parent_for m p cap parent \<equiv>
cap_is_device cap = cap_is_device parent \<and>
same_region_as parent cap \<and>
((\<exists>irq. cap = cap.IRQHandlerCap irq) \<and> parent = cap.IRQControlCap \<or>
is_untyped_cap parent \<and> descendants_of p m = {} \<or> safe_parent_for_arch cap parent)"
definition
capBadge_ordering :: "bool \<Rightarrow> (badge option \<times> badge option) set"
where
"capBadge_ordering firstBadged \<equiv>
(if firstBadged then {(None, None)} else Id) \<union> ({None, Some 0} \<times> range Some)"
(* True if cap' is derived from cap. *)
definition
is_derived :: "cdt \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
where
"is_derived m p cap' cap \<equiv>
cap' \<noteq> cap.NullCap \<and>
\<not> is_zombie cap \<and>
cap' \<noteq> cap.IRQControlCap \<and>
(if is_untyped_cap cap
then
cap_master_cap cap = cap_master_cap cap' \<and> descendants_of p m = {}
else
(cap_master_cap cap = cap_master_cap cap') \<and>
(cap_badge cap, cap_badge cap') \<in> capBadge_ordering False) \<and>
(is_master_reply_cap cap = is_reply_cap cap') \<and>
is_derived_arch cap' cap \<and>
\<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap'"
(* FIXME: remove copy_of and use cap_master_cap with weak_derived directly *)
definition
copy_of :: "cap \<Rightarrow> cap \<Rightarrow> bool"
where
"copy_of cap' cap \<equiv>
if (is_untyped_cap cap)
then cap = cap'
else same_object_as cap cap' \<and>
is_reply_cap cap = is_reply_cap cap' \<and>
is_master_reply_cap cap = is_master_reply_cap cap'"
(* cap' can be the result of a modification from cap made by the user
using Copy, Mint, Move, Mutate,... Actually, that relation should be symmetric*)
definition
"weak_derived cap cap' \<equiv>
(copy_of cap cap' \<and>
cap_asid cap = cap_asid cap' \<and>
cap_asid_base cap = cap_asid_base cap' \<and>
cap_vptr cap = cap_vptr cap') \<or>
cap' = cap"
end