adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

sysinit: implement support for shared frames 

Co-authored-by: Michael Sproul <michael.sproul@data61.csiro.au>
This commit is contained in:
Callum Bannister 2019-01-25 16:38:20 +11:00
parent 02c19be141
commit 4c79675879
13 changed files with 1950 additions and 1253 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
proof/capDL-api/KHeap_DP.thy
View File

@ -545,7 +545,6 @@ lemma reset_cap_asid_cap_has_object:
lemma cap_object_reset_cap_asid:
"\<lbrakk>reset_cap_asid cap = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> cap_object cap = cap_object cap'"
apply (case_tac cap',simp_all add:reset_cap_asid_def split:cdl_cap.split_asm)
apply (simp add:cap_object_def cap_has_object_def)+
done
lemma cap_type_reset_cap_asid[simp]:

140
proof/sep-capDL/Helpers_SD.thy
View File

@ -455,6 +455,12 @@ lemma object_size_bits_empty_cnode [simp]:
"object_size_bits (CNode (empty_cnode sz)) = sz"
by (clarsimp simp: object_size_bits_def empty_cnode_def)
lemma is_pt_pt_size[simp]: "is_pt obj \<Longrightarrow> object_size_bits obj = pt_size"
by (clarsimp simp: object_size_bits_def pt_size_def is_pt_def split: cdl_object.splits)
lemma is_pd_pd_size[simp]: "is_pd obj \<Longrightarrow> object_size_bits obj = pd_size"
by (clarsimp simp: object_size_bits_def pt_size_def is_pd_def split: cdl_object.splits)
definition
object_at_pointer_size_bits :: "cdl_state \<Rightarrow> cdl_object_id \<Rightarrow> cdl_size_bits"
where
@ -550,7 +556,7 @@ definition
"real_object_at \<equiv> \<lambda> obj_id s. obj_id \<in> dom (cdl_objects s) \<and> obj_id \<notin> irq_nodes s"
(* Agregate object types. *)
(* Aggregate object types. *)
abbreviation
"table_at \<equiv> \<lambda>obj_id s. pt_at obj_id s \<or> pd_at obj_id s"
abbreviation
@ -609,6 +615,9 @@ lemma object_type_is_object:
is_cnode_def is_irq_node_def is_asidpool_def is_pt_def is_pd_def is_frame_def
split: cdl_object.splits)
lemma is_ptD[dest]: "is_pt obj \<Longrightarrow> \<exists>x. obj = PageTable x"
by (clarsimp simp: is_pt_def split: cdl_object.splits)
lemma object_at_object_type:
"\<lbrakk>cdl_objects spec obj_id = Some obj; untyped_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = UntypedType"
"\<lbrakk>cdl_objects spec obj_id = Some obj; ep_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = EndpointType"
@ -619,6 +628,7 @@ lemma object_at_object_type:
"\<lbrakk>cdl_objects spec obj_id = Some obj; asidpool_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = AsidPoolType"
"\<lbrakk>cdl_objects spec obj_id = Some obj; pt_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = PageTableType"
"\<lbrakk>cdl_objects spec obj_id = Some obj; pd_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = PageDirectoryType"
"\<lbrakk>cdl_objects spec obj_id = Some obj; frame_at obj_id spec\<rbrakk> \<Longrightarrow> \<exists>n. object_type obj = FrameType n"
by (simp_all add: object_at_def object_type_is_object)
lemma object_type_object_at:
@ -642,6 +652,15 @@ lemma set_object_type [simp]:
"{obj_id \<in> dom (cdl_objects spec). real_object_at obj_id spec} = {obj_id. real_object_at obj_id spec}"
by (auto simp: object_at_def real_object_at_def)
lemma pt_at_is_real[simp]: "pt_at pt_id spec \<Longrightarrow> pt_id \<in> {obj_id. real_object_at obj_id spec}"
apply (clarsimp simp: object_at_def is_pt_def real_object_at_def dom_def
irq_nodes_def is_irq_node_def)
by (clarsimp split: cdl_object.splits)
lemma pd_at_is_real[simp]: "pd_at pt_id spec \<Longrightarrow> pt_id \<in> {obj_id. real_object_at obj_id spec}"
apply (clarsimp simp: object_at_def is_pd_def real_object_at_def dom_def
irq_nodes_def is_irq_node_def)
by (clarsimp split: cdl_object.splits)
definition
real_objects :: "cdl_state \<Rightarrow> cdl_object_id set"
@ -666,6 +685,34 @@ where "is_fake_pt_cap cap \<equiv> case cap of
PageTableCap _ Fake _ \<Rightarrow> True
| _ \<Rightarrow> False"
definition is_real_vm_cap :: "cdl_cap \<Rightarrow> bool"
where
"is_real_vm_cap cap \<equiv>
(case cap of
FrameCap _ _ _ _ Real _ \<Rightarrow> True
| PageTableCap _ Real _ \<Rightarrow> True
| PageDirectoryCap _ Real _ \<Rightarrow> True
| _ \<Rightarrow> False)"
definition is_fake_vm_cap :: "cdl_cap \<Rightarrow> bool"
where
"is_fake_vm_cap cap \<equiv>
(case cap of
FrameCap _ _ _ _ Fake _ \<Rightarrow> True
| PageTableCap _ Fake _ \<Rightarrow> True
| PageDirectoryCap _ Fake _ \<Rightarrow> True
| _ \<Rightarrow> False)"
abbreviation
"fake_frame_cap dev ptr rights n \<equiv> FrameCap dev ptr rights n Fake None"
abbreviation
"is_fake_frame_cap cap \<equiv> (case cap of FrameCap _ _ _ _ Fake None \<Rightarrow> True | _ \<Rightarrow> False)"
definition dev_of :: "cdl_cap \<Rightarrow> bool option" where
"dev_of cap = (case cap of FrameCap dev ptr _ n _ _ \<Rightarrow> Some dev | _ \<Rightarrow> None)"
definition cap_size_bits :: "cdl_cap \<Rightarrow> nat" where
"cap_size_bits cap = (case cap of FrameCap _ _ _ n _ _ \<Rightarrow> n | _ \<Rightarrow> 0)"
lemma is_fake_pt_cap_is_pt_cap [elim!]:
"is_fake_pt_cap cap \<Longrightarrow> is_pt_cap cap"
by (clarsimp simp: is_fake_pt_cap_def split: cdl_cap.splits)
@ -824,6 +871,24 @@ lemma cap_object_default_cap_frame:
"is_frame_cap cap \<Longrightarrow> cap_object (default_cap (the (cap_type cap)) {obj_id} sz dev) = obj_id"
by clarsimp
lemma is_pd_default_cap[simp]:
"is_pd obj \<Longrightarrow>
cdl_objects spec ptr = Some obj \<Longrightarrow>
default_cap (object_type obj) {ptr'} n b = PageDirectoryCap ptr' Real None"
by (clarsimp simp: object_type_is_object default_cap_def)
lemma pd_at_default_cap[simp]:
"pd_at ptr spec \<Longrightarrow>
cdl_objects spec ptr = Some obj \<Longrightarrow>
default_cap (object_type obj) {ptr'} n b = PageDirectoryCap ptr' Real None"
by (fastforce simp: object_at_def)
lemma pt_at_default_cap[simp]:
"pt_at ptr spec \<Longrightarrow>
cdl_objects spec ptr = Some obj \<Longrightarrow>
default_cap (object_type obj) {ptr'} n b = PageTableCap ptr' Real None"
by (clarsimp simp: object_type_is_object default_cap_def object_at_def)
lemma default_cap_not_null [elim!]:
"default_cap type obj_ids sz dev = NullCap \<Longrightarrow> False"
"NullCap = default_cap type obj_ids sz dev\<Longrightarrow> False"
@ -835,7 +900,7 @@ lemma cap_objects_update_cap_object [simp]:
by (clarsimp simp: cap_has_object_def update_cap_object_def
split: cdl_cap.splits)
lemma cap_has_object_default_cap [simp]:
lemma cap_has_object_default_cap [simp]:
"type \<noteq> IRQNodeType \<Longrightarrow> cap_has_object (default_cap type ids sz dev)"
by (clarsimp simp: default_cap_def cap_has_object_def split: cdl_object_type.splits)
@ -1124,4 +1189,75 @@ lemma inter_empty_not_both:
"\<lbrakk>x \<in> A; A \<inter> B = {}\<rbrakk> \<Longrightarrow> x \<notin> B"
by fastforce
lemma object_at_predicate_lift:
"object_at P obj_id spec \<Longrightarrow> P (the (cdl_objects spec obj_id))"
by (fastforce simp: object_at_def)
lemma object_at_cdl_objects_elim[elim]:
"object_at P obj_id spec \<Longrightarrow> cdl_objects spec obj_id = Some (the (cdl_objects spec obj_id))"
by (fastforce simp: object_at_def)
lemma opt_cap_object_slot:
"cdl_objects spec obj_id = Some obj \<Longrightarrow>
P (object_slots obj slot) \<Longrightarrow>
P (opt_cap (obj_id, slot) spec)"
by (fastforce simp: object_at_def opt_cap_def slots_of_def opt_object_def)
lemma opt_cap_object_slotE:
"cdl_objects spec obj_id = Some obj \<Longrightarrow>
object_slots obj slot = Some cap \<Longrightarrow>
opt_cap (obj_id, slot) spec = Some cap"
by (rule opt_cap_object_slot)
lemma slots_of_object_slot:
"cdl_objects spec obj_id = Some obj \<Longrightarrow>
P (object_slots obj slot) \<Longrightarrow>
P (slots_of obj_id spec slot)"
by (fastforce simp: object_at_def opt_cap_def slots_of_def opt_object_def)
lemma slots_of_object_slotE:
"cdl_objects spec obj_id = Some obj \<Longrightarrow>
object_slots obj slot = Some cap \<Longrightarrow>
slots_of obj_id spec slot = Some cap"
by (fastforce simp: object_at_def opt_cap_def slots_of_def opt_object_def)
lemma object_at_cdl_objects:
"cdl_objects spec obj_id = Some obj \<Longrightarrow>
P obj \<Longrightarrow>
object_at P obj_id spec"
by (fastforce simp: object_at_def)
lemma opt_cap_object_slot_simp:
"cdl_objects spec obj_id = Some obj \<Longrightarrow>
opt_cap (obj_id, slot) spec = object_slots obj slot"
by (fastforce simp: object_at_def opt_cap_def slots_of_def opt_object_def)
lemma slots_of_object_slot_simp:
"cdl_objects spec obj_id = Some obj \<Longrightarrow>
slots_of obj_id spec slot = object_slots obj slot"
by (fastforce simp: object_at_def opt_cap_def slots_of_def opt_object_def)
lemma is_fake_pt_cap_cap_has_object:
"is_fake_pt_cap cap \<Longrightarrow> cap_has_object cap"
by (clarsimp simp: cap_has_object_def is_fake_pt_cap_def split: cdl_cap.splits)
lemma is_fake_pt_cap_pt_cap:
"is_fake_pt_cap (PageTableCap x R z) \<longleftrightarrow> R = Fake"
by (clarsimp simp: is_fake_pt_cap_def split: cdl_frame_cap_type.splits)
lemma fake_vm_cap_simp:
"is_fake_vm_cap (FrameCap x y z a R b) \<longleftrightarrow> R = Fake"
by (clarsimp simp: is_fake_vm_cap_def split: cdl_frame_cap_type.splits)
lemma frame_not_pt[intro!]: "\<not> (is_frame x \<and> is_pt x)"
by (cases x; clarsimp simp: is_frame_def is_pt_def)
lemma not_frame_and_pt: "is_frame x \<Longrightarrow> is_pt x \<Longrightarrow> False"
by (fastforce simp: frame_not_pt[simplified])
lemma not_cap_at_cap_not_at:
"(slot \<in> dom (slots_of obj_id spec) \<and> \<not> cap_at P (obj_id, slot) spec) \<longleftrightarrow>
(slot \<in> dom (slots_of obj_id spec) \<and> cap_at (\<lambda>x. \<not> P x) (obj_id, slot) spec)"
by (intro iffI; clarsimp simp: cap_at_def opt_cap_def)
end

2
spec/capDL/Types_D.thy
View File

@ -354,7 +354,7 @@ where
then (THE c. c \<in> cap_objects cap)
else undefined"
lemma cap_object_simps:
lemma cap_object_simps[simp]:
"cap_object (IOPageTableCap x) = x"
"cap_object (IOSpaceCap x) = x"
"cap_object (IOPortsCap x a) = x"

82
sys-init/DuplicateCaps_SI.thy
View File

@ -31,11 +31,6 @@ lemma sep_map_zip_snd_take:
apply simp
done
lemma sep_map_c_unat [simp]:
"(\<lambda>slot. (obj_id, slot) \<mapsto>c NullCap) \<circ> unat =
(\<lambda>cptr. (obj_id, unat cptr) \<mapsto>c NullCap)"
by fastforce
lemma wfdc_obj_not_untyped:
"well_formed_cap (default_cap t oid sz dev) \<Longrightarrow> t \<noteq> UntypedType"
by (clarsimp simp:default_cap_def well_formed_cap_def)
@ -48,13 +43,21 @@ lemma derived_cap_default:
lemma cnode_or_tcb_at_wfc:
"\<lbrakk>cnode_or_tcb_at obj_id spec; cdl_objects spec obj_id = Some obj; sz \<le> 32\<rbrakk>
\<Longrightarrow> well_formed_cap (default_cap (object_type obj) oid sz dev)"
\<Longrightarrow> well_formed_cap (default_cap (object_type obj) oid sz dev)"
apply (elim disjE)
apply (simp add: object_at_def is_tcb_def default_cap_def well_formed_cap_def
is_cnode_def object_type_def guard_bits_def
split: cdl_object.splits)+
done
lemma frame_at_wfc:
"\<lbrakk>frame_at obj_id spec; cdl_objects spec obj_id = Some obj; sz \<le> 32\<rbrakk>
\<Longrightarrow> well_formed_cap (default_cap (object_type obj) oid sz dev)"
apply (simp add: object_at_def is_frame_def default_cap_def well_formed_cap_def
is_cnode_def object_type_def guard_bits_def vm_read_write_def
split: cdl_object.splits)
done
lemma seL4_CNode_Copy_sep_helper:
"\<lbrakk>(free_cptr::32 word) < 2 ^ si_cnode_size;
(cap_ptr::32 word) < 2 ^ si_cnode_size;
@ -96,17 +99,54 @@ lemma seL4_CNode_Copy_sep_helper:
apply sep_solve
done
lemma duplicate_cap_sep_helper:
(* This definition is a bit of a hack for the duplicate_cap_sep_helper_general lemma below.
Originally it only supported CNodes and TCBs, but it has been extended with support for'
duplicating frames *)
definition well_formed_obj_filter ::
"(cdl_object_id \<Rightarrow> cdl_state \<Rightarrow> bool) \<Rightarrow> bool"
where
"well_formed_obj_filter obj_filter \<equiv>
\<forall>spec obj_id obj.
obj_filter obj_id spec \<and> cdl_objects spec obj_id = Some obj
\<longrightarrow> (\<forall>oid sz dev. sz \<le> 32 \<longrightarrow> well_formed_cap (default_cap (object_type obj) oid sz dev))
\<and> (well_formed spec \<longrightarrow> real_object_at obj_id spec)"
lemma wf_obj_filter_wfc:
"\<lbrakk>well_formed_obj_filter obj_filter;
obj_filter obj_id spec;
cdl_objects spec obj_id = Some obj;
sz \<le> 32\<rbrakk> \<Longrightarrow>
well_formed_cap (default_cap (object_type obj) oid sz dev)"
by (clarsimp simp: well_formed_obj_filter_def)
lemma wf_obj_filter_real_object_at:
"\<lbrakk>well_formed_obj_filter obj_filter;
well_formed spec;
obj_filter obj_id spec;
cdl_objects spec obj_id = Some obj\<rbrakk> \<Longrightarrow>
real_object_at obj_id spec"
by (clarsimp simp: well_formed_obj_filter_def)
lemma wf_obj_filter_cnode_or_tcb_at:
"well_formed_obj_filter cnode_or_tcb_at"
by (auto simp: well_formed_obj_filter_def object_at_real_object_at intro: cnode_or_tcb_at_wfc)
lemma wf_obj_filter_frame_at:
"well_formed_obj_filter frame_at"
by (auto simp: well_formed_obj_filter_def object_at_real_object_at intro: frame_at_wfc)
lemma duplicate_cap_sep_helper_general:
"\<lbrakk>well_formed spec; distinct obj_ids;
list_all (\<lambda>n. n < 2 ^ si_cnode_size) (map unat free_cptrs);
(obj_id, free_cptr) \<in> set (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] free_cptrs);
well_formed_obj_filter obj_filter;
(obj_id, free_cptr) \<in> set (zip [obj\<leftarrow>obj_ids. obj_filter obj spec] free_cptrs);
set obj_ids = dom (cdl_objects spec)\<rbrakk>
\<Longrightarrow>
\<lbrace>\<guillemotleft>(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
si_cap_at t orig_caps spec dev obj_id \<and>* si_objects \<and>* R\<guillemotright>\<rbrace>
duplicate_cap spec orig_caps (obj_id, free_cptr)
\<lbrace>\<lambda>_ s.
\<guillemotleft>si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] free_cptrs))
\<guillemotleft>si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. obj_filter obj spec] free_cptrs))
spec dev obj_id \<and>*
si_cap_at t orig_caps spec dev obj_id \<and>* si_objects \<and>* R\<guillemotright> s\<rbrace>"
apply (rule hoare_assume_pre)
@ -126,26 +166,27 @@ lemma duplicate_cap_sep_helper:
seL4_CNode_Copy_sep_helper)
apply (rule unat_less_2_si_cnode_size, simp)
apply simp
apply (erule(1) cnode_or_tcb_at_wfc)
apply (frule (1) well_formed_object_size_bits_word_bits, simp add: word_bits_def)
apply sep_solve
apply (erule (2) wf_obj_filter_wfc)
apply (frule (1) well_formed_object_size_bits_word_bits, simp add: word_bits_def)
apply sep_solve
apply sep_solve
apply (rule conjI)
apply (rule unat_less_2_si_cnode_size, simp)
apply sep_solve
apply clarsimp
done
lemma duplicate_cap_sep:
lemma duplicate_cap_sep_general:
"\<lbrace>\<guillemotleft>(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>* si_objects \<and>* R\<guillemotright> and K (
well_formed spec \<and> distinct obj_ids \<and>
list_all (\<lambda>n. n < 2 ^ si_cnode_size) (map unat free_cptrs) \<and>
(obj_id, free_cptr) \<in> set (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] free_cptrs) \<and>
well_formed_obj_filter obj_filter \<and>
(obj_id, free_cptr) \<in> set (zip [obj\<leftarrow>obj_ids. obj_filter obj spec] free_cptrs) \<and>
set obj_ids = dom (cdl_objects spec))\<rbrace>
duplicate_cap spec orig_caps (obj_id, free_cptr)
\<lbrace>\<lambda>_.
\<guillemotleft>si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] free_cptrs))
\<guillemotleft>si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. obj_filter obj spec] free_cptrs))
spec dev obj_id \<and>*
si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>* si_objects \<and>* R\<guillemotright>\<rbrace>"
apply (rule hoare_gen_asm)
@ -155,15 +196,14 @@ lemma duplicate_cap_sep:
apply (rule hoare_chain [where
P="\<guillemotleft>((si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>* si_objects) \<and>*
(\<And>* obj_id \<in> {obj_id. real_object_at obj_id spec}. si_cap_at t orig_caps spec dev obj_id) \<and>* R\<guillemotright>" and
Q="\<lambda>rv.\<guillemotleft>(si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec]
Q="\<lambda>rv.\<guillemotleft>(si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. obj_filter obj spec]
free_cptrs)) spec dev obj_id \<and>* si_objects) \<and>*
(\<And>* obj_id \<in> {obj_id. real_object_at obj_id spec}. si_cap_at t orig_caps spec dev obj_id) \<and>* R\<guillemotright>"])
apply (rule sep_set_conj_map_singleton_wp [where x=obj_id])
apply simp
apply (drule in_set_zip1)
apply (fastforce simp: object_at_real_object_at)
apply (fastforce dest: in_set_zip1 simp: wf_obj_filter_real_object_at)
apply (rule hoare_chain)
apply (rule_tac t=t and R=R in duplicate_cap_sep_helper, assumption+)
apply (rule_tac t=t and R=R in duplicate_cap_sep_helper_general, fastforce+)
apply sep_solve
apply sep_solve
apply sep_solve
@ -171,6 +211,8 @@ lemma duplicate_cap_sep:
apply sep_solve
done
lemmas duplicate_cap_sep = duplicate_cap_sep_general[where obj_filter=cnode_or_tcb_at]
lemma duplicate_caps_sep_helper:
"\<lbrace>\<guillemotleft>si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
(\<And>* (obj_id, free_cptr) \<in> set (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] free_cptrs).
@ -201,7 +243,7 @@ lemma duplicate_caps_sep_helper:
apply (clarsimp simp: sep_conj_assoc)
apply (rename_tac obj_id free_cptr)
apply (wp sep_wp: duplicate_cap_sep [where obj_ids=obj_ids and free_cptrs=free_cptrs and t=t])
apply clarsimp
apply (clarsimp simp: wf_obj_filter_cnode_or_tcb_at)
apply sep_solve
apply (clarsimp simp: sep_conj_assoc si_caps_at_def)
apply sep_solve

7
sys-init/InitCSpace_SI.thy
View File

@ -14,6 +14,7 @@ imports
ObjectInitialised_SI
RootTask_SI
SysInit_SI
Mapped_Separating_Conjunction
begin
(****************************
@ -1740,10 +1741,6 @@ lemma set_take_add:
set (take i zs) \<union> set (take j (drop i zs)) = set (take k zs)"
by (metis set_append take_add)
lemma sep_map_set_conj_set_cong:
"\<lbrakk>sep_map_set_conj f xs s; xs = ys\<rbrakk> \<Longrightarrow> sep_map_set_conj f ys s"
by simp
lemma wellformed_no_dev:
"well_formed spec \<Longrightarrow>(\<forall>obj_id. cnode_at obj_id spec \<longrightarrow>
(\<forall>slot\<in>dom (slots_of obj_id spec). cap_at (\<lambda>c. is_device_cap c = False) (obj_id, slot) spec))"
@ -1800,7 +1797,7 @@ lemma init_cspace_sep:
and irqs="used_irq_list spec"], simp+)
apply (subst (asm) sep.prod.union_disjoint [symmetric], simp+)
apply (metis (no_types) distinct_append distinct_take_strg inf_sup_aci(1) take_add)
apply (erule sep_map_set_conj_set_cong)
apply (erule sep_map_set_conj_set_cong[THEN fun_cong, THEN iffD1, rotated])
apply clarsimp
apply (subst Un_commute, subst set_take_add, (simp add: add.commute)+)
done

1
sys-init/InitTCB_SI.thy
View File

@ -432,7 +432,6 @@ lemma tcb_configure_post:
apply (clarsimp simp: si_objects_def)
apply (clarsimp simp: sep_conj_exists sep_conj_assoc)
apply (clarsimp simp: si_cap_at_def sep_conj_assoc sep_conj_exists)
apply (clarsimp simp: object_at_def)
apply (subst tcb_half_decomp' [where obj_id=obj_id and k_obj_id=k_obj_id],
(assumption|simp)+)
apply (subst (asm) sep_map_f_eq_tcb_fault_endpoint, assumption+)

1916
sys-init/InitVSpace_SI.thy
View File

File diff suppressed because it is too large Load Diff

216
sys-init/Mapped_Separating_Conjunction.thy Normal file
View File

@ -0,0 +1,216 @@
(*
* Copyright 2019, Data61
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(DATA61_GPL)
*)
(* Utility lemmas related to the mapping of separating conjunctions over sets and lists *)
theory Mapped_Separating_Conjunction
imports
Sep_Algebra.Sep_Algebra_L4v
"HOL-Library.Multiset"
begin
lemmas sep_map_set_conj_set_cong = arg_cong[where f="sep_map_set_conj P" for P]
lemma sep_map_set_conj_set_elim:
"sep_map_set_conj P xs s \<Longrightarrow> \<lbrakk> \<And>x s. x \<in> xs \<Longrightarrow> P x s = Q x s\<rbrakk> \<Longrightarrow> sep_map_set_conj Q xs s"
apply (induct xs arbitrary: s rule: infinite_finite_induct)
apply fastforce
apply fastforce
apply clarsimp
apply (erule sep_conj_impl; blast)
done
lemma split_filter_set: "xs = {x \<in> xs. P x} \<union> {x \<in> xs. \<not>P x}"
by blast
lemma set_minus_not_filter[simp]: "{x \<in> xs. P x} - {x \<in> xs. \<not>P x} = {x \<in> xs. P x}"
by blast
lemma set_minus_not_filter'[simp]: "{x \<in> xs. \<not>P x} - {x \<in> xs. P x} = {x \<in> xs. \<not>P x}"
by blast
lemma set_inter_not_filter[simp]: "{x \<in> xs. P x} \<inter> {x \<in> xs. \<not>P x} = {}"
by blast
declare sep_list_conj_map_add[simp]
lemma sep_map_list_conj_decomp[simp]:
"sep_map_list_conj (\<lambda>(x, y). P x y \<and>* Q x y) xs =
(sep_map_list_conj (\<lambda>(x, y). P x y) xs \<and>* sep_map_list_conj (\<lambda>(x , y). Q x y) xs)"
apply (intro ext iffI)
apply (induct xs; clarsimp)
apply sep_cancel+
apply fastforce
apply (induct xs; clarsimp)
apply sep_cancel+
apply fastforce
done
lemma image_insertD: "insert (P x) (P ` S) = Q ` S' \<Longrightarrow> \<exists>s\<in>S'. Q s = P x "
by (metis imageE insertI1)
lemma sep_map_set_inj_eqI:
"inj_on P xs \<Longrightarrow> inj_on Q ys \<Longrightarrow> P ` xs = Q ` ys \<Longrightarrow>
sep_map_set_conj P xs = sep_map_set_conj Q ys"
apply (induct xs arbitrary: ys rule: infinite_finite_induct)
apply clarsimp
defer
apply clarsimp+
apply (frule image_insertD)
apply clarsimp
apply atomize
apply (erule_tac x="ys - {s}" in allE)
apply (drule mp)
apply (simp add: inj_on_diff)
apply (drule mp)
apply (metis (no_types, hide_lams) image_insert inj_on_insert insert_Diff_single
insert_absorb insert_ident)
apply clarsimp
apply (subgoal_tac "finite ys")
apply (simp add: sep.prod.remove)
apply (metis finite.insertI finite_image_iff)
apply (subgoal_tac "infinite ys", clarsimp)
using finite_image_iff by fastforce
lemma add_mset_eq_mem:
"add_mset (P x) (image_mset P (mset_set F)) = image_mset Q (mset_set S')
\<Longrightarrow> \<exists>y. Q y = P x \<and> y \<in> S'"
apply (drule union_single_eq_member)
apply clarsimp
by (metis elem_mset_set empty_iff infinite_set_mset_mset_set)
lemma sep_map_set_conj_mset_eq:
"\<lbrakk>image_mset P (mset_set S) = image_mset Q (mset_set S');
finite S; finite S'\<rbrakk>
\<Longrightarrow> sep_map_set_conj P S = sep_map_set_conj Q S'"
apply (induction S arbitrary: S' rule: infinite_finite_induct; clarsimp)
apply (simp add: mset_set_empty_iff)
apply (subgoal_tac "\<exists>y. y \<in> S' \<and> Q y = P x")
apply (clarsimp simp: sep.prod.remove mset_set.remove)
by (fastforce dest: union_single_eq_member)
lemma sep_map_set_conj_multisetE:
"\<lbrakk>sep_map_set_conj P S s; finite S; finite S';
image_mset P (mset_set S) = image_mset Q (mset_set S')\<rbrakk>
\<Longrightarrow> sep_map_set_conj Q S' s"
by (subst sep_map_set_conj_mset_eq; fastforce)
lemma not_in_image_vimage: "x \<notin> P ` S \<Longrightarrow> P -` {x} \<inter> S = {}"
by blast
lemma bij_image_mset_eq:
"\<lbrakk>finite S; finite S'; P ` S = Q ` S';
(\<And>x. x \<in> P ` S \<Longrightarrow> \<exists>f. bij_betw f (P -` {x} \<inter> S) (Q -` {x} \<inter> S'))\<rbrakk>
\<Longrightarrow> image_mset P (mset_set S) = image_mset Q (mset_set S')"
apply (rule multiset_eqI)
apply (clarsimp simp: count_image_mset)
apply (case_tac "x \<in> Q ` S'"; clarsimp simp: bij_betw_iff_card not_in_image_vimage )
done
lemma sep_map_set_elim:
"\<lbrakk>sep_map_set_conj P xs s;
xs = ys;
(\<And>x s. x \<in> xs \<Longrightarrow> P x s \<Longrightarrow> Q x s)\<rbrakk>
\<Longrightarrow> sep_map_set_conj Q ys s"
apply clarsimp
apply (case_tac "finite xs")
apply clarsimp
apply (erule sep_map_set_conj_impl)
apply atomize
apply (erule_tac x=x in allE)
apply clarsimp
apply clarsimp
apply clarsimp
done
lemma sep_map_set_conj_Union:
"\<lbrakk>\<forall>s \<in> S. finite s;
\<forall>s s'. s \<in> S \<and> s' \<in> S \<longrightarrow> s \<noteq> s' \<longrightarrow> s \<inter> s' = {}\<rbrakk>
\<Longrightarrow> sep_map_set_conj (sep_map_set_conj P) S = sep_map_set_conj P (\<Union> S) "
apply (induct S rule: infinite_finite_induct; clarsimp)
apply (metis (no_types) finite_UnionD sep.prod.infinite)
apply (subst sep.prod.union_disjoint; clarsimp?)
by blast
lemma sep_map_set_quotient_split:
"\<lbrakk>finite xs; equiv xs R\<rbrakk>
\<Longrightarrow> sep_map_set_conj P xs = sep_map_set_conj (sep_map_set_conj P ) (xs//R) "
apply (subst sep_map_set_conj_Union; clarsimp)
apply (meson in_quotient_imp_subset infinite_super)
apply (fastforce dest: quotient_disj)
by (simp add: Union_quotient)
lemma sep_map_set_conj_congE:
"\<lbrakk>sep_map_set_conj (sep_map_set_conj P) xs s;
finite xs;
finite ys;
xs - {{}} = ys - {{}}\<rbrakk>
\<Longrightarrow> sep_map_set_conj (sep_map_set_conj P) ys s"
apply clarsimp
apply (induct xs arbitrary:ys s rule: infinite_finite_induct)
apply clarsimp+
apply (subgoal_tac "ys = {{}} \<or> ys = {}")
apply (erule disjE; clarsimp)
apply blast
apply clarsimp
apply (case_tac "x = {}")
apply (metis Diff_idemp Diff_insert_absorb Sep_Tactic_Helpers.sep_conj_empty sep.prod.empty)
apply (subgoal_tac "x \<in> ys")
apply (clarsimp simp: sep.prod.remove)
apply sep_cancel
apply (metis Diff_insert Diff_insert2 Diff_insert_absorb finite_Diff)
apply blast
done
lemma sep_map_set_conj_cong_empty_eq:
"\<lbrakk>finite xs;
finite ys;
xs - {{}} = ys - {{}}\<rbrakk>
\<Longrightarrow> sep_map_set_conj (sep_map_set_conj P) xs = sep_map_set_conj (sep_map_set_conj P) ys "
apply clarsimp
apply (intro ext iffI; erule sep_map_set_conj_congE)
by blast+
lemma sep_map_set_conj_match:
"sep_map_set_conj P S s \<Longrightarrow> (\<And>x s. x \<in> S \<Longrightarrow> P x s \<Longrightarrow> Q x s) \<Longrightarrow> sep_map_set_conj Q S s"
apply (induct rule: infinite_finite_induct; clarsimp)
apply (erule sep_conj_impl)
apply blast
by (metis sep_map_set_elim)
lemma sep_map_set_squash:
"\<lbrakk>\<forall>x y. x \<in> S \<longrightarrow> y \<in> S \<longrightarrow> x \<noteq> y \<longrightarrow> f x = f y \<longrightarrow> f x = {}; finite S\<rbrakk>
\<Longrightarrow> sep_map_set_conj (\<lambda>v. sep_map_set_conj P (f v)) S =
sep_map_set_conj (sep_map_set_conj P) (f ` S)"
apply (induction S rule: infinite_finite_induct; clarsimp)
apply (case_tac "f x \<in> f ` F"; clarsimp)
apply (subgoal_tac "f x = {}")
apply clarsimp
apply blast
done
lemma sep_map_set_conj_subst:
"(\<And>x. x \<in> S \<Longrightarrow> Q x = Q' x) \<Longrightarrow> sep_map_set_conj Q S = sep_map_set_conj Q' S"
by clarsimp
lemma sep_map_zip_fst:
"(\<And>* map (\<lambda>(a,b). f a) (zip xs ys)) s =
(\<And>* map (\<lambda>a. f (fst a)) (zip xs ys)) s"
by (simp add: case_prod_unfold)
lemma sep_map_zip_snd:
"(\<And>* map (\<lambda>(a, b). f b) (zip xs ys)) s =
(\<And>* map (\<lambda>a. f (snd a)) (zip xs ys)) s"
by (simp add: case_prod_unfold)
declare sep_map_zip_fst[THEN iffD1, sep_cancel] sep_map_zip_fst[THEN iffD2, sep_cancel]
sep_map_zip_snd[THEN iffD1, sep_cancel] sep_map_zip_snd[THEN iffD2, sep_cancel]
end

33
sys-init/ObjectInitialised_SI.thy
View File

@ -146,6 +146,23 @@ where
"object_empty_slots_empty spec t spec_object_id \<equiv>
object_initialised_general spec t object_default_state sep_map_E spec_object_id"
definition slots_in_object_empty ::
"(cdl_cap \<Rightarrow> bool) \<Rightarrow> cdl_object_id \<Rightarrow> cdl_state \<Rightarrow>
(cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> sep_pred" where
"slots_in_object_empty P obj_id spec t \<equiv>
sep_map_set_conj (object_empty spec t)
{obj. \<exists>slot. slot \<in> dom (slots_of obj_id spec)
\<and> cap_at P (obj_id, slot) spec
\<and> obj = cap_ref_object (obj_id, slot) spec}"
definition slots_in_object_init ::
"(cdl_cap \<Rightarrow> bool) \<Rightarrow> cdl_object_id \<Rightarrow> cdl_state \<Rightarrow>
(cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> sep_pred" where
"slots_in_object_init P obj_id spec t \<equiv>
sep_map_set_conj (object_initialised spec t)
{obj. \<exists>slot. slot \<in> dom (slots_of obj_id spec)
\<and> cap_at P (obj_id, slot) spec
\<and> obj = cap_ref_object (obj_id, slot) spec}"
(**********************************************
* Predicates about CNodes being initialised. *
@ -436,6 +453,16 @@ lemma cap_transform_nullcap [simp]:
by (clarsimp simp: cap_transform_def cap_has_object_def
update_cap_object_def)
lemma cap_transform_pt_simp [simp]:
"cap_transform t (PageTableCap x y z) = PageTableCap (the (t x)) y z"
by (clarsimp simp: option.the_def cap_transform_def update_cap_object_def cap_object_def
split: option.splits)
lemma cap_transform_frame [simp]:
"cap_transform t (FrameCap x ptr rights n y z) = FrameCap x (the (t ptr)) rights n y z"
by (clarsimp simp: option.the_def cap_transform_def update_cap_object_def cap_object_def
split: option.splits)
lemma cap_type_cap_transform [simp]:
"cap_type (cap_transform t cap) = cap_type cap"
by (clarsimp simp: cap_transform_def cap_has_object_def)
@ -1375,4 +1402,10 @@ lemma object_fields_empty_half_initialised:
\<Longrightarrow> cnode_fields_half_initialised spec t obj_id = object_fields_empty spec t obj_id"
by (clarsimp simp: cnode_fields_half_initialised_object_fields_initialised cnode_fields_empty_initialised)
lemma object_default_state_frame [simp]:
"is_frame object \<Longrightarrow> object_default_state object = object"
by (clarsimp simp: object_default_state_def default_object_def
object_type_is_object object_type_def
split: cdl_object.splits)
end

172
sys-init/Proof_SI.thy
View File

@ -47,24 +47,6 @@ lemma parse_bootinfo_sep:
apply (clarsimp simp: zip_map1 comp_def split_beta')
done
lemma parse_spec_inv:
"\<lbrace>\<lambda>s. \<guillemotleft>R\<guillemotright> s\<rbrace>
parse_spec spec obj_ids
\<lbrace>\<lambda>rv s. \<guillemotleft>R\<guillemotright> s\<rbrace>"
apply (clarsimp simp: parse_spec_def sep_state_projection2_def)
apply (wp)
apply clarsimp
done
lemma parse_spec_sep:
"\<lbrace>\<lambda>s. True\<rbrace>
parse_spec spec obj_ids
\<lbrace>\<lambda>_ s. set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids \<rbrace>"
apply (clarsimp simp: parse_spec_def)
apply (wp)
apply clarsimp
done
(* This isn't actually all the combinations, but enough of them for what I needed. *)
lemma object_types_distinct:
"tcb_at x s \<Longrightarrow> \<not> cnode_at x s"
@ -100,13 +82,6 @@ lemma real_objects_some_type:
split: cdl_object.splits)
by metis
lemma object_at_irq_node_irq_node_at:
"\<lbrakk>well_formed spec; object_at P obj_id spec; obj_id \<in> irq_nodes spec\<rbrakk> \<Longrightarrow> irq_node_at obj_id spec"
apply (clarsimp simp: object_at_def)
apply (frule (2) well_formed_irq_nodes_object_type)
apply (simp add: object_type_is_object)
done
lemma capdl_objects_by_parts:
"well_formed spec \<Longrightarrow>
(sep_map_set_conj P {obj_id. real_object_at obj_id spec}) =
@ -168,16 +143,12 @@ lemma valid_case_prod':
lemma le_list_all:
"\<lbrakk>unat start < 2 ^ si_cnode_size; unat (end - 1) < 2 ^ si_cnode_size\<rbrakk>
\<Longrightarrow> list_all (\<lambda>n. (n::32 word) < 2 ^ si_cnode_size) [start .e. end - 1]"
\<Longrightarrow> list_all (\<lambda>n. (n::32 word) < 2 ^ si_cnode_size) [start .e. end - 1]"
apply (clarsimp simp: list_all_iff)
apply (subst word_arith_power_alt)
apply simp
by (metis (no_types) dual_order.strict_trans2 unat_less_2_si_cnode_size word_of_int_numeral word_of_int_power_hom)
lemma sep_conj_pred_conj:
"(P \<and>* (P' and K Q)) s = ((P \<and>* P') and K Q) s"
by (case_tac "Q = False", simp_all)
lemma list_all_drop:
"list_all P xs \<Longrightarrow> list_all P (drop n xs)"
by (fastforce simp: list_all_iff dest: in_set_dropD)
@ -188,6 +159,23 @@ lemma dom_map_of_zip':
apply (subst dom_map_of_zip, simp+)
done
(* FIXME: MOVE (Lib) *)
lemma in_zip_map: "p \<in> set xs \<Longrightarrow> length xs \<le> length ys \<Longrightarrow> map_of (zip xs ys) p \<noteq> None"
using dom_map_of_zip' by blast
lemma map_of_list_allE:
"map_of (zip ys xs) p = Some v \<Longrightarrow> distinct ys \<Longrightarrow> list_all P xs \<Longrightarrow> P v"
apply (induct ys arbitrary: xs; clarsimp)
by (meson in_set_zipE list_all_spec map_of_SomeD)
lemma card_eq_lengthI:
"set xs = ys \<Longrightarrow> distinct xs \<Longrightarrow> length xs = card ys"
by (induct xs arbitrary: ys; fastforce)
lemma length_filter_card:
"\<lbrakk>s_list = sorted_list_of_set s; finite s\<rbrakk>
\<Longrightarrow> length (filter P s_list) = card {x \<in> s. P x}"
by (fastforce intro: card_eq_lengthI)
(* Dirty hack that is sadly needed to make the below proof work. *)
declare [[unify_search_bound = 1000]]
@ -196,7 +184,8 @@ lemma small_one:
"\<lbrakk>well_formed spec;
set obj_ids = dom (cdl_objects spec); distinct obj_ids;
real_ids = [obj_id \<leftarrow> obj_ids. real_object_at obj_id spec];
length obj_ids + length [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] \<le> unat fend - unat fstart;
length obj_ids + length [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] +
card (\<Union>(set ` get_frame_caps spec ` {obj. pd_at obj spec})) \<le> unat fend - unat fstart;
length untyped_caps = unat uend - unat ustart;
distinct_sets (map cap_free_ids untyped_caps);
list_all is_full_untyped_cap untyped_caps;
@ -216,7 +205,12 @@ lemma small_one:
\<lbrace>\<guillemotleft>(\<And>* (cptr, cap) \<in> set (zip untyped_cptrs untyped_caps). (si_cnode_id, unat cptr) \<mapsto>c cap) \<and>*
(\<And>* cptr \<in> set free_cptrs. (si_cnode_id, unat cptr) \<mapsto>c NullCap) \<and>*
(\<And>* obj_id\<in>(\<Union>cap\<in>set untyped_caps. cap_free_ids cap). obj_id \<mapsto>o Untyped) \<and>*
si_objects \<and>* si_irq_nodes spec \<and>* R\<guillemotright>\<rbrace>
si_objects \<and>*
si_irq_nodes spec \<and>*
(SETSEPCONJ pd_id | pd_at pd_id spec.
frame_duplicates_empty (make_frame_cap_map obj_ids (drop (length obj_ids) free_cptrs) spec)
pd_id spec) \<and>*
R\<guillemotright>\<rbrace>
init_system spec bootinfo obj_ids
\<lbrace>\<lambda>_ s. \<exists>t.
\<guillemotleft>objects_initialised spec t {obj_id. real_object_at obj_id spec} \<and>*
@ -226,8 +220,12 @@ lemma small_one:
si_objects \<and>*
si_objects_extra_caps (dom (cdl_objects spec))
(free_cptrs :: 32 word list)
(untyped_cptrs :: 32 word list) spec \<and>* R\<guillemotright> s \<and>
inj_on t (dom (cdl_objects spec)) \<and> dom t = set obj_ids\<rbrace>"
(untyped_cptrs :: 32 word list) spec \<and>*
(SETSEPCONJ pd_id | pd_at pd_id spec.
frame_duplicates_copied (make_frame_cap_map obj_ids (drop (length obj_ids) free_cptrs) spec)
pd_id spec t) \<and>*
R\<guillemotright> s \<and>
inj_on t (dom (cdl_objects spec)) \<and> dom t = set obj_ids\<rbrace>"
apply clarsimp
apply (frule (1) le_list_all [where start = ustart])
apply (frule (1) le_list_all [where start = fstart])
@ -235,73 +233,74 @@ lemma small_one:
apply (insert distinct_card [symmetric, where xs ="[obj\<leftarrow>obj_ids . cnode_or_tcb_at obj spec]"], simp)
apply (frule distinct_card [symmetric])
apply (clarsimp simp: init_system_def, wp valid_case_prod')
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in start_threads_sep [sep_wandise], simp)
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and
free_cptrs="[fstart .e. fend - 1]" in init_cspace_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_tcbs_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_vspace_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_pd_asids_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and dev=False in init_irqs_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and dev=False and
untyped_cptrs = "[ustart .e. uend - 1]" and
free_cptrs_orig = "[fstart .e. fend - 1]" in duplicate_caps_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in start_threads_sep [sep_wandise], simp)
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and
free_cptrs="[fstart .e. fend - 1]" in init_cspace_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_tcbs_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_vspace_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_pd_asids_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and dev=False in init_irqs_sep [sep_wandise])
apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and dev=False and
untyped_cptrs = "[ustart .e. uend - 1]" and
free_cptrs_orig = "[fstart .e. fend - 1]" in duplicate_caps_sep [sep_wandise])
apply (rule create_irq_caps_sep [where dev = False,sep_wandise,
where free_cptrs_orig = "[fstart .e. fend - 1]"
and untyped_cptrs = "[ustart .e. uend - 1]"
and orig_caps = "map_of (zip [obj\<leftarrow>obj_ids. real_object_at obj spec] [fstart .e. fend - 1])"
and orig_caps = "map_of (zip [obj\<leftarrow>obj_ids. real_object_at obj spec]
[fstart .e. fend - 1])"
and spec = spec])
apply (wp sep_wp: create_objects_sep [where untyped_caps = untyped_caps and dev = False])
apply (wp sep_wp: parse_bootinfo_sep [where fstart = fstart
and fend = fend
and ustart = ustart
and uend = uend
and untyped_caps = untyped_caps])
apply (wp sep_wp: parse_bootinfo_sep [where fstart = fstart
and fend = fend
and ustart = ustart
and uend = uend
and untyped_caps = untyped_caps])
apply (subst objects_initialised_by_parts, assumption)
apply (subst objects_empty_by_parts, assumption)+
apply (subst objects_empty_objects_initialised_capless)+
apply clarsimp
apply (sep_cancel+ | intro conjI allI impI | erule sep_curry[rotated, where P=R])+
apply simp
apply (intro conjI allI impI | sep_cancel+)+
apply (intro conjI pred_andI)
apply sep_cancel+
apply (intro conjI pred_andI allI impI)
apply (erule sep_curry[rotated, where P=R])
apply (intro conjI pred_andI allI impI)
apply sep_solve
apply (clarsimp simp: linorder_not_le)
apply (intro conjI allI impI pred_andI | sep_cancel+)+
apply fastforce
apply (clarsimp simp: less_diff_conv)
apply (rule list_all_drop, erule (1) le_list_all)
apply clarsimp
apply (subgoal_tac "map_of (zip (filter (\<lambda>obj. real_object_at obj spec) obj_ids) free_cptrs)
p \<noteq> None")
apply clarsimp
apply (erule map_of_list_allE)
apply (fastforce intro!: List.distinct_filter)
apply (fastforce intro!: le_list_all)
apply (rule in_zip_map)
apply clarsimp
apply (fastforce dest!: real_object_not_irq_node(3))
apply (insert length_filter_le[where xs = obj_ids and P="\<lambda>obj. real_object_at obj spec"],
fastforce)[1]
apply (erule (1) le_list_all)
apply (rule list_all_drop, erule (1) le_list_all)
apply simp
apply (subst dom_map_of_zip')
apply (insert length_filter_le [where xs = obj_ids and P="\<lambda>obj. real_object_at obj spec"], simp)
apply (insert length_filter_le [where xs = obj_ids and P="\<lambda>obj. real_object_at obj spec"],
fastforce)[1]
apply simp
apply (erule (1) le_list_all)
done
(* FIXME, make the acquiring of the object_ids part of sys_init, not a parameter. *)
lemma set_inter_rewrite:
" ({x. P x} \<inter> S) =
{x \<in> S. P x}"
by fast
(**************************************************
* The top level lemma for system initialisation. *
**************************************************)
(* FIXME, make the acquiring of the object_ids part of sys_init, not a parameter. *)
lemma sys_init:
"\<lbrakk>well_formed spec; set obj_ids = dom (cdl_objects spec); distinct obj_ids\<rbrakk> \<Longrightarrow>
"\<lbrakk>well_formed spec; obj_ids = sorted_list_of_set (dom (cdl_objects spec))\<rbrakk> \<Longrightarrow>
\<lbrace>\<guillemotleft>valid_boot_info bootinfo spec \<and>* R\<guillemotright>\<rbrace>
init_system spec bootinfo obj_ids
\<lbrace>\<lambda>_ s. \<exists>t.
init_system spec bootinfo obj_ids
\<lbrace>\<lambda>_ s. \<exists>t.
\<guillemotleft>objects_initialised spec t {obj_id. real_object_at obj_id spec} \<and>*
irqs_initialised spec t (used_irqs spec) \<and>*
si_final_objects spec t \<and>* R\<guillemotright> s \<and>
si_final_objects spec t \<and>*
(EXS map. (SETSEPCONJ pd_id | pd_at pd_id spec. frame_duplicates_copied map pd_id spec t)) \<and>*
R\<guillemotright> s \<and>
inj_on t (set obj_ids) \<and> dom t = set obj_ids\<rbrace>"
apply (frule distinct_card)
apply (insert distinct_card [where xs = "[obj\<leftarrow>obj_ids . cnode_or_tcb_at obj spec]"], simp)
apply (clarsimp simp: valid_boot_info_def si_final_objects_def
sep_conj_exists sep_conj_assoc)
@ -309,19 +308,22 @@ lemma sys_init:
apply (rule hoare_ex_pre)+
apply (rule hoare_grab_asm)+
apply (rule hoare_chain)
apply (rule small_one [where obj_ids=obj_ids and R=R],
(assumption|simp add: unat_less_2_si_cnode_size')+)
apply (rule small_one[where obj_ids="sorted_list_of_set (dom (cdl_objects spec))" and R=R],
(assumption|simp add: unat_less_2_si_cnode_size' length_filter_card)+)
apply sep_solve
apply clarsimp
apply (rule_tac x=t in exI)
apply (clarsimp)
apply (clarsimp simp: si_objects_extra_caps_def si_caps_at_def
sep_conj_exists sep_conj_assoc)
apply (rule_tac x="(map_of (zip [obj\<leftarrow>obj_ids . cnode_or_tcb_at obj spec] (drop (length obj_ids) [fstart .e. fend - 1])))" in exI)
apply (rule_tac x="(map_of (zip [obj \<leftarrow> obj_ids. cnode_or_tcb_at obj spec]
(drop (length obj_ids) [fstart .e. fend - 1])))" in exI)
apply (rule_tac x="[x .e. xa - 1]" in exI)
apply (rule_tac x="[fstart .e. fend - 1]" in exI)
apply (rule_tac x=untyped_capsa in exI)
apply (rule_tac x=all_available_ids in exI)
apply (rule_tac x="make_frame_cap_map obj_ids (drop (card (dom (cdl_objects spec)))
[fstart .e. fend - 1]) spec" in exI)
apply (clarsimp simp: sep_conj_ac)
done
@ -329,16 +331,18 @@ definition injective :: "('a \<Rightarrow> 'b option) \<Rightarrow> bool"
where "injective f \<equiv> inj_on f (dom f)"
lemma sys_init_paper:
"\<lbrakk>well_formed spec; set obj_ids = dom (cdl_objects spec); distinct obj_ids\<rbrakk> \<Longrightarrow>
"\<lbrakk>well_formed spec; obj_ids = sorted_list_of_set (dom (cdl_objects spec))\<rbrakk> \<Longrightarrow>
\<lbrace>\<guillemotleft>valid_boot_info bootinfo spec \<and>* R\<guillemotright>\<rbrace>
init_system spec bootinfo obj_ids
\<lbrace>\<lambda>_ s. \<exists>\<phi>.
\<lbrace>\<lambda>_ s. \<exists>\<phi>.
\<guillemotleft>objects_initialised spec \<phi> {obj_id. real_object_at obj_id spec} \<and>*
irqs_initialised spec \<phi> (used_irqs spec) \<and>*
si_final_objects spec \<phi> \<and>* R\<guillemotright> s \<and>
si_final_objects spec \<phi> \<and>*
(EXS map. (SETSEPCONJ pd_id | pd_at pd_id spec. frame_duplicates_copied map pd_id spec \<phi>)) \<and>*
R\<guillemotright> s \<and>
injective \<phi> \<and> dom \<phi> = set obj_ids\<rbrace>"
apply (rule hoare_strengthen_post)
apply (fact sys_init)
apply (fact sys_init)
apply (fastforce simp: injective_def)
done

69
sys-init/RootTask_SI.thy
View File

@ -12,7 +12,7 @@
* The layout of the capability space and other parts of the system-initialiser.
*)
theory RootTask_SI
imports WellFormed_SI
imports WellFormed_SI SysInit_SI
begin
(******************************************************************
@ -506,6 +506,60 @@ lemma valid_si_caps_at_si_cap_at:
apply (clarsimp simp: sep_conj_ac)+
done
(*******************************************************
* Frames have been duplicated. *
*******************************************************)
abbreviation (input)
"lookup_obj obj_id slot P s \<equiv> \<exists>cap. opt_cap (obj_id, slot) s = Some cap
\<and> cap \<noteq> NullCap
\<and> P (cap_object cap) s"
abbreviation "get_obj obj_id slot spec \<equiv> (cap_object o the) (opt_cap (obj_id, slot) spec)"
abbreviation "ref_obj spec obj_id slot \<equiv> cap_ref_object (obj_id, slot) spec"
abbreviation "real_frame_cap_of dev ptr rights n t \<equiv> FrameCap dev ((the o t) ptr) rights n Real None"
abbreviation (input) "the_cap spec pt_id pt_slot \<equiv> the (opt_cap (pt_id, pt_slot) spec)"
definition conjure_real_frame_cap ::
"cdl_cap \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> cdl_cap"
where
"conjure_real_frame_cap cap t \<equiv>
case cap of FrameCap _ ptr _ n _ _ \<Rightarrow> real_frame_cap_of False ptr vm_read_write n t | _ \<Rightarrow> cap"
definition frame_duplicates_empty ::
"(cdl_object_id \<times> nat \<Rightarrow> word32) \<Rightarrow> cdl_object_id \<Rightarrow> cdl_state \<Rightarrow> (sep_state \<Rightarrow> bool)"
where
"frame_duplicates_empty cptr_map pd_id spec \<equiv>
sep_map_set_conj
(\<lambda>x. let pt_id = get_obj pd_id x spec in
sep_map_set_conj (\<lambda>y. (si_cnode_id, unat $ cptr_map (pt_id, y)) \<mapsto>c NullCap)
{slot \<in> dom (slots_of pt_id spec). cap_at ((\<noteq>) NullCap) (pt_id, slot) spec})
{slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>cap. cap \<noteq> NullCap \<and> pt_at (cap_object cap) spec)
(pd_id, slot) spec} \<and>*
sep_map_set_conj
(\<lambda>x. let frame_id = get_obj pd_id x spec in
(si_cnode_id, unat $ cptr_map (pd_id, x)) \<mapsto>c NullCap)
{slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>cap. cap \<noteq> NullCap \<and> frame_at (cap_object cap) spec)
(pd_id, slot) spec}"
definition frame_duplicates_copied ::
"(cdl_object_id \<times> nat \<Rightarrow> word32) \<Rightarrow> cdl_object_id \<Rightarrow> cdl_state
\<Rightarrow> (cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> (sep_state \<Rightarrow> bool)"
where
"frame_duplicates_copied cptr_map pd_id spec t \<equiv>
sep_map_set_conj
(\<lambda>x. let pt_id = get_obj pd_id x spec in
sep_map_set_conj (\<lambda>y. (si_cnode_id, unat $ cptr_map (pt_id, y)) \<mapsto>c
conjure_real_frame_cap (the_cap spec pt_id y) t)
{slot \<in> dom (slots_of pt_id spec). cap_at ((\<noteq>) NullCap) (pt_id, slot) spec})
{slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>cap. cap \<noteq> NullCap \<and> pt_at (cap_object cap) spec)
(pd_id, slot) spec} \<and>*
sep_map_set_conj
(\<lambda>x. let frame_id = get_obj pd_id x spec in
(si_cnode_id, unat $ cptr_map (pd_id, x)) \<mapsto>c
conjure_real_frame_cap (the_cap spec pd_id x) t)
{slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>cap. cap \<noteq> NullCap \<and> frame_at (cap_object cap) spec)
(pd_id, slot) spec}"
(**********************************************************
* The pre and post conditions of the system initialiser. *
**********************************************************)
@ -515,13 +569,20 @@ definition
valid_boot_info
where
"valid_boot_info bootinfo spec \<equiv> \<lambda>s.
\<exists>untyped_caps fstart fend ustart uend.
\<exists>untyped_caps fstart fend ustart uend obj_ids.
((\<And>*(cptr, cap) \<in> set (zip [ustart .e. uend - 1] untyped_caps). (si_cnode_id, unat cptr) \<mapsto>c cap) \<and>*
(\<And>* cptr \<in> set [fstart .e. fend - 1]. (si_cnode_id, unat cptr) \<mapsto>c NullCap) \<and>*
(\<And>* obj_id\<in>(\<Union>cap\<in>set untyped_caps. cap_free_ids cap). obj_id \<mapsto>o Untyped) \<and>*
si_objects \<and>* si_irq_nodes spec) s \<and>
(SETSEPCONJ pd_id | pd_at pd_id spec.
frame_duplicates_empty (make_frame_cap_map obj_ids
(drop (card (dom (cdl_objects spec))) [fstart .e. fend - 1]) spec)
pd_id spec) \<and>*
si_objects \<and>*
si_irq_nodes spec) s \<and>
obj_ids = sorted_list_of_set (dom (cdl_objects spec)) \<and>
card (dom (cdl_objects spec)) +
card {obj_id. cnode_or_tcb_at obj_id spec} \<le> unat fend - unat fstart \<and>
card {obj_id. cnode_or_tcb_at obj_id spec} +
card (\<Union>(set ` get_frame_caps spec ` {obj. pd_at obj spec})) \<le> unat fend - unat fstart \<and>
length untyped_caps = unat uend - unat ustart \<and>
distinct_sets (map cap_free_ids untyped_caps) \<and>
list_all is_full_untyped_cap untyped_caps \<and>

182
sys-init/SysInit_SI.thy
View File

@ -27,15 +27,6 @@ where
return (untyped_list, free_slots)
od"
(* Currently, objects are created in any order.
Later versions could create untypes before their children and use the untyped_covers.
A refinement will create bigger ones first to remove internal fragmentation. *)
definition
parse_spec :: "cdl_state \<Rightarrow> cdl_object_id list \<Rightarrow> unit u_monad"
where
"parse_spec spec obj_ids \<equiv>
assert (set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids)"
(* Create a new object in the next free cnode slot using a given untyped.
Return whether or not the operation fails. *)
definition
@ -185,7 +176,7 @@ definition duplicate_caps :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarro
\<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) u_monad"
where
"duplicate_caps spec orig_caps obj_ids free_slots \<equiv> do
obj_ids' \<leftarrow> return [obj_id \<leftarrow> obj_ids. cnode_at obj_id spec \<or> tcb_at obj_id spec];
obj_ids' \<leftarrow> return [obj_id \<leftarrow> obj_ids. cnode_or_tcb_at obj_id spec];
assert (length obj_ids' \<le> length free_slots);
mapM_x (duplicate_cap spec orig_caps) (zip obj_ids' free_slots);
return $ map_of $ zip obj_ids' free_slots
@ -266,58 +257,44 @@ where
mapM_x (set_asid spec orig_caps) pd_ids
od"
(* Map the right cap into the slot of a page directory or page table. *)
definition map_page :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
\<Rightarrow> cdl_object_id \<Rightarrow> cdl_right set \<Rightarrow> word32 \<Rightarrow> unit u_monad"
where
"map_page spec orig_caps page_id pd_id rights vaddr \<equiv> do
(* Map a page into a page table or page directory *)
definition map_page ::
"cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
\<Rightarrow> cdl_object_id \<Rightarrow> cdl_right set \<Rightarrow> word32 \<Rightarrow> cdl_cptr \<Rightarrow> unit u_monad"
where
"map_page spec orig_caps page_id pd_id rights vaddr free_cptr \<equiv> do
cdl_page \<leftarrow> assert_opt $ opt_object page_id spec;
sel4_page \<leftarrow> assert_opt $ orig_caps page_id;
sel4_pd \<leftarrow> assert_opt $ orig_caps pd_id;
vmattribs \<leftarrow> assert_opt $ opt_vmattribs cdl_page;
if (pt_at page_id spec) then
seL4_PageTable_Map sel4_page sel4_pd vaddr vmattribs
else if (frame_at page_id spec) then
seL4_Page_Map sel4_page sel4_pd vaddr rights vmattribs
else
fail;
return ()
assert (frame_at page_id spec);
\<comment> \<open>Copy the frame cap into a new slot for mapping, this enables shared frames\<close>
duplicate_cap spec orig_caps (page_id, free_cptr);
seL4_Page_Map free_cptr sel4_pd vaddr rights vmattribs;
return ()
od"
(* Maps a page directory slot (and all its contents if it's a page table). *)
definition map_page_directory_slot :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option)
\<Rightarrow> cdl_object_id\<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad"
where
"map_page_directory_slot spec orig_caps pd_id pd_slot \<equiv> do
page_cap \<leftarrow> assert_opt $ opt_cap (pd_id, pd_slot) spec;
page_id \<leftarrow> return $ cap_object page_cap;
(* The page table's virtual address is given by the number of slots and how much memory each maps.
Each page directory slot maps 10+12 bits of memory (by the page table and page respectively). *)
page_vaddr \<leftarrow> return $ of_nat pd_slot << (pt_size + small_frame_size);
page_rights \<leftarrow> return (cap_rights page_cap);
when (page_cap \<noteq> NullCap)
(map_page spec orig_caps page_id pd_id page_rights page_vaddr)
(* Map a page table into a page directory *)
definition map_page_table ::
"cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
\<Rightarrow> cdl_object_id \<Rightarrow> cdl_right set \<Rightarrow> word32 \<Rightarrow> unit u_monad"
where
"map_page_table spec orig_caps page_id pd_id rights vaddr \<equiv> do
cdl_page \<leftarrow> assert_opt $ opt_object page_id spec;
sel4_page \<leftarrow> assert_opt $ orig_caps page_id;
sel4_pd \<leftarrow> assert_opt $ orig_caps pd_id;
vmattribs \<leftarrow> assert_opt $ opt_vmattribs cdl_page;
assert (pt_at page_id spec);
seL4_PageTable_Map sel4_page sel4_pd vaddr vmattribs;
return ()
od"
(* Maps a page directory and all its contents. *)
definition map_page_directory :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
\<Rightarrow> unit u_monad"
where
"map_page_directory spec orig_caps pd_id \<equiv> do
pd_slots \<leftarrow> return $ slots_of_list spec pd_id;
mapM_x (map_page_directory_slot spec orig_caps pd_id) pd_slots
od"
(* Maps a page directory slot. *)
definition map_page_table_slot :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
\<Rightarrow> cdl_object_id \<Rightarrow> word32 \<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad"
where
"map_page_table_slot spec orig_caps pd_id pt_id pt_vaddr pt_slot \<equiv> do
(* Map a page table slot *)
definition map_page_table_slot ::
"cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
\<Rightarrow> cdl_object_id \<Rightarrow> word32 \<Rightarrow> (cdl_cap_ref \<Rightarrow> cdl_cptr) \<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad"
where
"map_page_table_slot spec orig_caps pd_id pt_id pt_vaddr free_cptr pt_slot \<equiv> do
frame_cap \<leftarrow> assert_opt $ opt_cap (pt_id, pt_slot) spec;
page \<leftarrow> return $ cap_object frame_cap;
@ -326,43 +303,94 @@ where
Each page stores 12 bits of memory. *)
page_vaddr \<leftarrow> return $ pt_vaddr + (of_nat pt_slot << small_frame_size);
page_rights \<leftarrow> return (cap_rights frame_cap);
when (frame_cap \<noteq> NullCap)
(map_page spec orig_caps page pd_id page_rights page_vaddr)
if frame_cap \<noteq> NullCap then
do cptr \<leftarrow> return $ free_cptr (pt_id, pt_slot);
map_page spec orig_caps page pd_id page_rights page_vaddr cptr
od
else
return ()
od"
(* Maps a page table's slots. *)
definition map_page_table_slots :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
\<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad"
where
"map_page_table_slots spec orig_caps pd_id pd_slot \<equiv> do
(* Map a page directory slot (and all its contents if it points to a page table) *)
definition map_page_directory_slot ::
"cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option)
\<Rightarrow> cdl_object_id \<Rightarrow> (cdl_cap_ref \<Rightarrow> cdl_cptr) \<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad"
where
"map_page_directory_slot spec orig_caps pd_id free_cptrs pd_slot \<equiv> do
page_cap \<leftarrow> assert_opt $ opt_cap (pd_id, pd_slot) spec;
page \<leftarrow> return $ cap_object page_cap;
page_slots \<leftarrow> return $ slots_of_list spec page;
page_id \<leftarrow> return $ cap_object page_cap;
(* The page's virtual address is given by the number of slots and how much memory each maps.
(* The page table's virtual address is given by the number of slots and how much memory each maps.
Each page directory slot maps 10+12 bits of memory (by the page table and page respectively). *)
page_vaddr \<leftarrow> return $ of_nat pd_slot << (pt_size + small_frame_size);
page_rights \<leftarrow> return (cap_rights page_cap);
when (fake_pt_cap_at (pd_id, pd_slot) spec)
(mapM_x (map_page_table_slot spec orig_caps pd_id page page_vaddr) page_slots)
if pt_at page_id spec then
do
map_page_table spec orig_caps page_id pd_id page_rights page_vaddr;
page_slots \<leftarrow> return $ slots_of_list spec page_id;
mapM_x (map_page_table_slot spec orig_caps pd_id page_id page_vaddr free_cptrs)
[slot <- page_slots. cap_at ((\<noteq>) NullCap) (page_id, slot) spec]
od
else if frame_at page_id spec then
do
cptr \<leftarrow> return $ free_cptrs (pd_id, pd_slot);
map_page spec orig_caps page_id pd_id page_rights page_vaddr cptr
od
else
return ()
od"
(* Maps a page directory and all its contents. *)
definition map_page_directory_page_tables :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
\<Rightarrow> unit u_monad"
where
"map_page_directory_page_tables spec orig_caps pd_id \<equiv> do
(* Map a page directory and all its contents *)
definition map_page_directory ::
"cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option)
\<Rightarrow> (cdl_cap_ref \<Rightarrow> cdl_cptr) \<Rightarrow> cdl_object_id \<Rightarrow> unit u_monad"
where
"map_page_directory spec orig_caps free_cptrs pd_id \<equiv> do
pd_slots \<leftarrow> return $ slots_of_list spec pd_id;
mapM_x (map_page_table_slots spec orig_caps pd_id) pd_slots
mapM_x (map_page_directory_slot spec orig_caps pd_id free_cptrs)
[pd_slot <- pd_slots. cap_at (\<lambda>cap. cap \<noteq> NullCap
\<and> frame_at (cap_object cap) spec) (pd_id, pd_slot) spec];
mapM_x (map_page_directory_slot spec orig_caps pd_id free_cptrs)
[pd_slot <- pd_slots. cap_at (\<lambda>cap. cap \<noteq> NullCap
\<and> pt_at (cap_object cap) spec) (pd_id, pd_slot) spec]
od"
(* Get a list of all the (object_id, slot) pairs contained within a page directory
and its child page tables which contain frame caps *)
definition get_frame_caps :: "cdl_state \<Rightarrow> cdl_object_id \<Rightarrow> (cdl_object_id \<times> nat) list" where
"get_frame_caps spec pd_id \<equiv> do {
pd_slot <- slots_of_list spec pd_id;
obj_cap <- case_option [] (\<lambda>x. [x]) $ opt_cap (pd_id, pd_slot) spec;
let obj_id = cap_object obj_cap;
if frame_at obj_id spec then
[(pd_id, pd_slot)]
else
\<comment> \<open>If the slot contains a page table cap, collect all its slots that contain frames\<close>
map (Pair obj_id) o filter (\<lambda>slot. cap_at ((\<noteq>) NullCap) (obj_id, slot) spec) $
slots_of_list spec obj_id
}"
(* Construct a function to assign each frame cap a free cptr, mapping all other slots to 0 *)
definition make_frame_cap_map ::
"cdl_object_id list \<Rightarrow> word32 list \<Rightarrow> cdl_state \<Rightarrow> cdl_object_id \<times> nat \<Rightarrow> word32"
where
"make_frame_cap_map obj_ids free_cptrs spec ref \<equiv>
case_option 0 id
(map_of (zip ([obj_id \<leftarrow> obj_ids. pd_at obj_id spec] \<bind> get_frame_caps spec) free_cptrs) ref)"
(* Maps page directories and all their contents. *)
definition init_vspace :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id list \<Rightarrow> unit u_monad"
definition init_vspace ::
"cdl_state \<Rightarrow>
(cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow>
cdl_object_id list \<Rightarrow>
cdl_cptr list \<Rightarrow>
unit u_monad"
where
"init_vspace spec orig_caps obj_ids \<equiv> do
"init_vspace spec orig_caps obj_ids free_cptrs \<equiv> do
pd_ids \<leftarrow> return [obj_id \<leftarrow> obj_ids. pd_at obj_id spec];
mapM_x (map_page_directory spec orig_caps) pd_ids;
mapM_x (map_page_directory_page_tables spec orig_caps) pd_ids
cptr_map \<leftarrow> return $ make_frame_cap_map obj_ids free_cptrs spec;
mapM_x (map_page_directory spec orig_caps cptr_map) pd_ids
od"
(**************************
@ -480,7 +508,7 @@ where
init_irqs spec orig_caps irq_caps;
init_pd_asids spec orig_caps obj_ids;
init_vspace spec orig_caps obj_ids;
init_vspace spec orig_caps obj_ids free_cptrs;
init_tcbs spec orig_caps obj_ids;
init_cspace spec orig_caps dup_caps irq_caps obj_ids;
start_threads spec dup_caps obj_ids

382
sys-init/WellFormed_SI.thy
View File

@ -24,6 +24,7 @@ imports
"DSpecProofs.Kernel_DP"
"SepDSpec.Separation_SD"
"Lib.SimpStrategy"
"AInvs.Rights_AI"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
@ -136,24 +137,6 @@ where
| PageDirectoryCap _ _ ad \<Rightarrow> ad \<noteq> None
| _ \<Rightarrow> False)"
definition is_real_vm_cap :: "cdl_cap \<Rightarrow> bool"
where
"is_real_vm_cap cap \<equiv>
(case cap of
FrameCap _ _ _ _ Real _ \<Rightarrow> True
| PageTableCap _ Real _ \<Rightarrow> True
| PageDirectoryCap _ Real _ \<Rightarrow> True
| _ \<Rightarrow> False)"
definition is_fake_vm_cap :: "cdl_cap \<Rightarrow> bool"
where
"is_fake_vm_cap cap \<equiv>
(case cap of
FrameCap _ _ _ _ Fake _ \<Rightarrow> True
| PageTableCap _ Fake _ \<Rightarrow> True
| PageDirectoryCap _ Fake _ \<Rightarrow> True
| _ \<Rightarrow> False)"
(* Original caps must have default rights,
* and original endpoint + notification caps must not be badged.
*)
@ -385,7 +368,7 @@ lemma well_formed_cap_cap_has_object_eq:
lemma well_formed_cap_update_cap_objects [simp]:
"is_untyped_cap cap
\<Longrightarrow> well_formed_cap (update_cap_objects x cap) = well_formed_cap cap"
\<Longrightarrow> well_formed_cap (update_cap_objects x cap) = well_formed_cap cap"
apply (clarsimp simp: update_cap_object_def
update_cap_objects_def well_formed_cap_def)
apply (cases cap, simp_all)
@ -399,8 +382,7 @@ lemma well_formed_cap_update_cap_object [simp]:
lemma cap_rights_inter_default_cap_rights:
"\<lbrakk>well_formed_cap cap; cap_type cap = Some type\<rbrakk>
\<Longrightarrow> cap_rights (default_cap type ids sz dev) \<inter> cap_rights cap
= cap_rights cap"
\<Longrightarrow> cap_rights (default_cap type ids sz dev) \<inter> cap_rights cap = cap_rights cap"
by (fastforce simp: well_formed_cap_def default_cap_def cap_type_def cap_rights_def
validate_vm_rights_def vm_read_write_def
vm_kernel_only_def vm_read_only_def
@ -444,7 +426,7 @@ lemma well_formed_distinct_slots_of_list [elim!]:
lemma well_formed_object_size_bits:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
\<Longrightarrow> object_size_bits (object_default_state obj) = object_size_bits obj"
\<Longrightarrow> object_size_bits (object_default_state obj) = object_size_bits obj"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply (clarsimp)
@ -452,13 +434,13 @@ lemma well_formed_object_size_bits:
lemma well_formed_well_formed_caps:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
\<Longrightarrow> well_formed_caps spec obj_id obj"
\<Longrightarrow> well_formed_caps spec obj_id obj"
by (clarsimp simp: well_formed_def split: option.splits)
lemma well_formed_well_formed_cap:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj;
object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk>
\<Longrightarrow> well_formed_cap cap"
\<Longrightarrow> well_formed_cap cap"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply (clarsimp simp: well_formed_caps_def)
@ -475,13 +457,13 @@ lemma well_formed_well_formed_cap':
lemma well_formed_well_formed_cap_to_object:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
\<Longrightarrow> well_formed_cap_to_object spec obj_id obj"
\<Longrightarrow> well_formed_cap_to_object spec obj_id obj"
by (clarsimp simp: well_formed_def split: option.splits)
lemma well_formed_well_formed_cap_to_real_object:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj;
object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk>
\<Longrightarrow> well_formed_cap_to_real_object spec cap"
\<Longrightarrow> well_formed_cap_to_real_object spec cap"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply (clarsimp simp: well_formed_caps_def)
@ -499,7 +481,7 @@ lemma well_formed_well_formed_cap_to_real_object':
lemma well_formed_well_formed_cap_types_match:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj;
object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk>
\<Longrightarrow> well_formed_cap_types_match spec cap"
\<Longrightarrow> well_formed_cap_types_match spec cap"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply (clarsimp simp: well_formed_caps_def)
@ -516,7 +498,7 @@ lemma well_formed_well_formed_cap_types_match':
lemma well_formed_cap_object_is_real:
"\<lbrakk>well_formed spec; opt_cap slot spec = Some cap; cap_has_object cap\<rbrakk>
\<Longrightarrow> real_object_at (cap_object cap) spec"
\<Longrightarrow> real_object_at (cap_object cap) spec"
apply (drule (1) well_formed_well_formed_cap_to_real_object', simp)
apply (clarsimp simp: well_formed_cap_to_real_object_def)
done
@ -524,7 +506,7 @@ lemma well_formed_cap_object_is_real:
lemma well_formed_types_match:
"\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap;
cdl_objects spec (cap_object cap) = Some cap_obj; cap_has_object cap\<rbrakk>
\<Longrightarrow> Some (object_type cap_obj) = cap_type cap"
\<Longrightarrow> Some (object_type cap_obj) = cap_type cap"
apply (frule cap_has_object_not_NullCap)
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
@ -538,7 +520,7 @@ lemma well_formed_types_match:
lemma well_formed_object_slots:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
\<Longrightarrow> dom (object_slots obj) = dom (object_slots (object_default_state obj))"
\<Longrightarrow> dom (object_slots obj) = dom (object_slots (object_default_state obj))"
apply (clarsimp simp: well_formed_def)
apply (erule allE [where x=obj_id])
apply simp
@ -547,8 +529,7 @@ lemma well_formed_object_slots:
lemma well_formed_slot_object_size_bits:
"\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap;
cdl_objects spec obj_id = Some obj; cnode_at obj_id spec\<rbrakk>
\<Longrightarrow> slot < 2 ^ object_size_bits obj"
apply (frule opt_cap_cdl_objects)
\<Longrightarrow> slot < 2 ^ object_size_bits obj"
apply (clarsimp simp: well_formed_def object_at_def is_cnode_def)
apply (erule_tac x=obj_id in allE)
apply clarsimp
@ -564,9 +545,26 @@ lemma well_formed_slot_object_size_bits:
apply (clarsimp simp: object_slots_slots_of)
done
lemma well_formed_slot_object_size_bits_pt:
"\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap;
pt_at obj_id spec; cdl_objects spec obj_id = Some obj\<rbrakk>
\<Longrightarrow> slot < 2 ^ object_size_bits obj"
apply (clarsimp simp: well_formed_def object_at_def is_pt_def)
apply (erule_tac x=obj_id in allE)
apply clarsimp
apply (subgoal_tac "slot \<in> dom (object_slots (object_default_state obj))")
apply (thin_tac "dom P = dom Q" for P Q)
apply (clarsimp simp: well_formed_caps_def)
apply (erule_tac x=slot in allE)
apply (clarsimp simp: object_default_state_def2 object_type_def has_slots_def
default_tcb_def object_size_bits_def object_slots_def
empty_cnode_def empty_cap_map_def pt_size_def pd_size_def
split: cdl_object.splits if_split_asm)
by (fastforce intro: object_slots_opt_capI)
lemma well_formed_cnode_object_size_bits:
"\<lbrakk>well_formed spec; cnode_at obj_id spec; cdl_objects spec obj_id = Some obj\<rbrakk>
\<Longrightarrow> 0 < object_size_bits obj"
\<Longrightarrow> 0 < object_size_bits obj"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply (clarsimp simp: is_cnode_def object_at_def)
@ -575,7 +573,7 @@ lemma well_formed_cnode_object_size_bits:
lemma well_formed_cnode_object_size_bits_eq:
"\<lbrakk>well_formed spec; opt_cap slot spec = Some cap;
cdl_objects spec (cap_object cap) = Some obj; is_cnode_cap cap\<rbrakk>
\<Longrightarrow> object_size_bits obj = cnode_cap_size cap"
\<Longrightarrow> object_size_bits obj = cnode_cap_size cap"
apply (frule (1) well_formed_cap_object_is_real)
apply (clarsimp simp: cap_has_object_def cap_type_def split: cdl_cap.splits)
apply (clarsimp simp: well_formed_def split_def split:option.splits)
@ -603,7 +601,7 @@ lemma slots_of_set [simp]:
lemma well_formed_well_formed_tcb:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
\<Longrightarrow> well_formed_tcb spec obj_id obj"
\<Longrightarrow> well_formed_tcb spec obj_id obj"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply clarsimp
@ -611,7 +609,7 @@ lemma well_formed_well_formed_tcb:
lemma well_formed_well_formed_vspace:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
\<Longrightarrow> well_formed_vspace spec obj_id obj"
\<Longrightarrow> well_formed_vspace spec obj_id obj"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply clarsimp
@ -619,7 +617,7 @@ lemma well_formed_well_formed_vspace:
lemma well_formed_well_formed_irq_node:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
\<Longrightarrow> well_formed_irq_node spec obj_id obj"
\<Longrightarrow> well_formed_irq_node spec obj_id obj"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply clarsimp
@ -640,7 +638,7 @@ lemma well_formed_inj_cdl_irq_node:
lemma well_formed_vm_cap_has_asid:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj;
object_slots obj slot = Some cap\<rbrakk>
\<Longrightarrow> \<not>vm_cap_has_asid cap"
\<Longrightarrow> \<not>vm_cap_has_asid cap"
apply (case_tac "cap = NullCap")
apply (clarsimp simp: vm_cap_has_asid_def)
apply (drule (3) well_formed_well_formed_cap)
@ -655,27 +653,14 @@ lemma is_fake_vm_cap_cap_type:
by (clarsimp simp: is_fake_vm_cap_def cap_type_def
split: cdl_cap.splits)
lemma well_formed_irq_node_in_irq_nodes:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_irq_node obj\<rbrakk>
\<Longrightarrow> obj_id \<in> irq_nodes spec"
oops
term real_object_at
lemma well_formed_irq_node_cap_is_ntfn_cap:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_irq_node obj;
object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk>
\<Longrightarrow> is_ntfn_cap cap"
apply (frule (3) well_formed_well_formed_cap_types_match)
apply (clarsimp simp: well_formed_cap_types_match_def)
oops
lemma is_fake_vm_cap_cap_has_object[simp]:
"is_fake_vm_cap cap \<Longrightarrow> cap_has_object cap"
by (clarsimp simp: cap_has_object_def is_fake_vm_cap_def split: cdl_cap.splits)
lemma well_formed_is_fake_vm_cap:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_cnode obj \<or> is_tcb obj \<or> is_irq_node obj;
object_slots obj slot = Some cap\<rbrakk>
\<Longrightarrow> \<not>is_fake_vm_cap cap"
\<Longrightarrow> \<not>is_fake_vm_cap cap"
apply (case_tac "is_irq_node obj")
apply (frule (1) well_formed_well_formed_irq_node)
apply (clarsimp simp: well_formed_irq_node_def object_at_def irq_nodes_def)
@ -696,7 +681,7 @@ lemma vm_cap_has_asid_update_cap_object [simp]:
lemma well_formed_object_size_bits_word_bits [simp]:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some spec_obj\<rbrakk>
\<Longrightarrow> object_size_bits spec_obj < word_bits"
\<Longrightarrow> object_size_bits spec_obj < word_bits"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply clarsimp
@ -705,7 +690,7 @@ lemma well_formed_object_size_bits_word_bits [simp]:
lemma well_formed_is_untyped_cap:
"\<lbrakk>well_formed spec; cnode_at obj_id spec;
opt_cap (obj_id, slot) spec = Some cap\<rbrakk>
\<Longrightarrow> \<not> is_untyped_cap cap"
\<Longrightarrow> \<not> is_untyped_cap cap"
apply (frule opt_cap_cdl_objects)
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
@ -719,7 +704,7 @@ lemma well_formed_is_untyped_cap:
lemma well_formed_cap_has_object:
"\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some spec_cap;
spec_cap \<noteq> NullCap; \<not> is_untyped_cap spec_cap; \<not> is_irqhandler_cap spec_cap\<rbrakk>
\<Longrightarrow> cap_has_object spec_cap"
\<Longrightarrow> cap_has_object spec_cap"
apply (clarsimp simp: opt_cap_def opt_object_def slots_of_def)
apply (clarsimp simp: well_formed_def)
apply (clarsimp split: option.splits)
@ -736,7 +721,7 @@ lemma well_formed_cap_has_object:
lemma well_formed_cap_object:
"\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some spec_cap;
cap_has_object spec_cap\<rbrakk>
\<Longrightarrow> \<exists>obj. cdl_objects spec (cap_object spec_cap) = Some obj"
\<Longrightarrow> \<exists>obj. cdl_objects spec (cap_object spec_cap) = Some obj"
apply (frule (1) well_formed_well_formed_cap', clarsimp)
apply (frule (1) well_formed_cap_has_object)
apply clarsimp
@ -753,19 +738,19 @@ lemma well_formed_cap_object:
lemma well_formed_cap_object_in_dom:
"\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some spec_cap;
cap_has_object spec_cap\<rbrakk>
\<Longrightarrow> cap_object spec_cap \<in> dom (cdl_objects spec)"
\<Longrightarrow> cap_object spec_cap \<in> dom (cdl_objects spec)"
by (drule (2) well_formed_cap_object, clarsimp)
lemma well_formed_all_caps_cap_object:
"\<lbrakk>well_formed spec; cap \<in> all_caps spec; cap_has_object cap\<rbrakk>
\<Longrightarrow>\<exists>obj. cdl_objects spec (cap_object cap) = Some obj"
\<Longrightarrow>\<exists>obj. cdl_objects spec (cap_object cap) = Some obj"
apply (clarsimp simp: all_caps_def)
apply (erule (2) well_formed_cap_object)
done
lemma well_formed_all_caps_cap_irq:
"\<lbrakk>well_formed spec; cap \<in> all_caps spec; is_irqhandler_cap cap\<rbrakk>
\<Longrightarrow>\<exists>obj. cdl_objects spec (cdl_irq_node spec (cap_irq cap)) = Some obj"
\<Longrightarrow>\<exists>obj. cdl_objects spec (cdl_irq_node spec (cap_irq cap)) = Some obj"
apply (clarsimp simp: all_caps_def)
apply (frule (1) well_formed_well_formed_cap_types_match', simp)
apply (clarsimp simp: well_formed_cap_types_match_def)
@ -773,7 +758,7 @@ lemma well_formed_all_caps_cap_irq:
lemma well_formed_update_cap_rights_idem:
"\<lbrakk>well_formed_cap cap; rights = cap_rights cap\<rbrakk>
\<Longrightarrow> update_cap_rights rights cap = cap"
\<Longrightarrow> update_cap_rights rights cap = cap"
by (auto simp: update_cap_rights_def cap_rights_def well_formed_cap_def
validate_vm_rights_def vm_kernel_only_def vm_read_write_def
vm_read_only_def split: cdl_cap.splits)
@ -789,7 +774,7 @@ lemma default_ntfn_cap[simp]:
lemma default_cap_well_formed_cap:
"\<lbrakk>well_formed_cap cap; cap_type cap = Some type; cnode_cap_size cap = sz\<rbrakk>
\<Longrightarrow> well_formed_cap (default_cap type obj_ids sz dev)"
\<Longrightarrow> well_formed_cap (default_cap type obj_ids sz dev)"
by (auto simp: well_formed_cap_def default_cap_def cap_type_def
word_gt_a_gt_0 vm_read_write_def cnode_cap_size_def
split: cdl_cap.splits)
@ -797,7 +782,7 @@ lemma default_cap_well_formed_cap:
lemma default_cap_well_formed_cap2:
"\<lbrakk>is_default_cap cap; cap_type cap = Some type; sz \<le> 32;
\<not> is_untyped_cap cap; \<not> is_asidpool_cap cap\<rbrakk>
\<Longrightarrow> well_formed_cap (default_cap type obj_ids sz dev )"
\<Longrightarrow> well_formed_cap (default_cap type obj_ids sz dev )"
apply (clarsimp simp: is_default_cap_def)
apply (clarsimp simp: default_cap_def well_formed_cap_def
word_gt_a_gt_0 badge_bits_def guard_bits_def
@ -809,7 +794,7 @@ lemma well_formed_well_formed_orig_cap:
"\<lbrakk>well_formed spec;
opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap;
original_cap_at (obj_id, slot) spec\<rbrakk>
\<Longrightarrow> well_formed_orig_cap cap"
\<Longrightarrow> well_formed_orig_cap cap"
apply (frule opt_cap_dom_cdl_objects)
apply (clarsimp simp: dom_def, rename_tac obj)
apply (frule (1) object_slots_opt_cap, simp)
@ -828,7 +813,7 @@ lemma well_formed_orig_ep_cap_is_default:
"\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec;
opt_cap (obj_id, slot) spec = Some cap;
ep_related_cap cap; cap \<noteq> NullCap\<rbrakk>
\<Longrightarrow> is_default_cap cap"
\<Longrightarrow> is_default_cap cap"
apply (case_tac "\<exists>obj_id R. cap = ReplyCap obj_id R")
apply (frule (1) well_formed_well_formed_cap', simp)
apply (clarsimp simp: well_formed_cap_def)
@ -847,7 +832,7 @@ lemma cap_rights_default_cap_eq:
lemma well_formed_orig_caps:
"\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec;
slots_of obj_id spec slot = Some cap; cap \<noteq> NullCap; cap_type cap = Some type\<rbrakk>
\<Longrightarrow> cap_rights (default_cap type obj_ids sz dev) = cap_rights cap"
\<Longrightarrow> cap_rights (default_cap type obj_ids sz dev) = cap_rights cap"
apply (frule well_formed_well_formed_orig_cap, simp add: opt_cap_def, assumption+)
apply (clarsimp simp: well_formed_orig_cap_def)
apply (subst (asm) cap_rights_default_cap_eq, fast)
@ -872,7 +857,7 @@ lemma well_formed_cdt:
lemma well_formed_cap_to_real_object:
"\<lbrakk>well_formed spec; real_object_at obj_id spec\<rbrakk>
\<Longrightarrow> \<exists>cnode_id slot cap.
\<Longrightarrow> \<exists>cnode_id slot cap.
opt_cap (cnode_id, slot) spec = Some cap \<and>
original_cap_at (cnode_id, slot) spec \<and>
cnode_at cnode_id spec \<and>
@ -885,7 +870,7 @@ lemma well_formed_cap_to_real_object:
lemma well_formed_cap_to_irq_object:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; obj_id \<in> irq_nodes spec\<rbrakk>
\<Longrightarrow> \<exists>cnode_id slot cap.
\<Longrightarrow> \<exists>cnode_id slot cap.
opt_cap (cnode_id, slot) spec = Some cap \<and>
original_cap_at (cnode_id, slot) spec \<and>
cnode_at cnode_id spec \<and>
@ -898,7 +883,7 @@ lemma well_formed_cap_to_irq_object:
lemma well_formed_cap_to_non_empty_pt:
"\<lbrakk>well_formed spec; pt_at obj_id spec;
object_at (\<lambda>obj. object_default_state obj \<noteq> obj) obj_id spec\<rbrakk>
\<Longrightarrow> \<exists>pd_id slot cap.
\<Longrightarrow> \<exists>pd_id slot cap.
opt_cap (pd_id, slot) spec = Some cap \<and>
pd_at pd_id spec \<and>
cap_object cap = obj_id \<and>
@ -915,21 +900,21 @@ lemma dom_object_slots_default_tcb:
lemma well_formed_tcb_has_fault:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some (Tcb tcb)\<rbrakk>
\<Longrightarrow> \<not> cdl_tcb_has_fault tcb"
\<Longrightarrow> \<not> cdl_tcb_has_fault tcb"
apply (drule (1) well_formed_well_formed_tcb)
apply (clarsimp simp: well_formed_tcb_def tcb_has_fault_def)
done
lemma well_formed_tcb_domain:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some (Tcb tcb)\<rbrakk>
\<Longrightarrow> cdl_tcb_domain tcb = minBound"
\<Longrightarrow> cdl_tcb_domain tcb = minBound"
apply (drule (1) well_formed_well_formed_tcb)
apply (clarsimp simp: well_formed_tcb_def tcb_domain_def)
done
lemma well_formed_object_domain:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
\<Longrightarrow> object_domain obj = minBound"
\<Longrightarrow> object_domain obj = minBound"
apply (case_tac "\<exists>tcb. obj = Tcb tcb")
apply clarsimp
apply (drule (1) well_formed_tcb_domain)
@ -940,7 +925,7 @@ lemma well_formed_object_domain:
lemma well_formed_tcb_object_slots:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some tcb; is_tcb tcb\<rbrakk>
\<Longrightarrow> dom (object_slots tcb) = {0..tcb_boundntfn_slot}"
\<Longrightarrow> dom (object_slots tcb) = {0..tcb_boundntfn_slot}"
apply (frule (1) well_formed_object_slots)
apply (clarsimp simp: object_default_state_def2 is_tcb_def split: cdl_object.splits)
apply (rule dom_object_slots_default_tcb)
@ -949,7 +934,7 @@ lemma well_formed_tcb_object_slots:
lemma well_formed_tcb_cspace_cap:
"\<lbrakk>well_formed spec;
tcb_at obj_id spec\<rbrakk>
\<Longrightarrow> \<exists>cspace_cap. opt_cap (obj_id, tcb_cspace_slot) spec = Some cspace_cap \<and>
\<Longrightarrow> \<exists>cspace_cap. opt_cap (obj_id, tcb_cspace_slot) spec = Some cspace_cap \<and>
is_cnode_cap cspace_cap \<and> cap_guard_size cspace_cap \<noteq> 0 \<and>
real_object_at (cap_object cspace_cap) spec"
apply (clarsimp simp: object_at_def)
@ -973,7 +958,7 @@ lemma well_formed_tcb_cspace_cap:
lemma cap_data_cap_guard_size_0:
"\<lbrakk>well_formed_cap cap; is_cnode_cap cap; cap_data cap = 0\<rbrakk>
\<Longrightarrow> cap_guard_size cap = 0"
\<Longrightarrow> cap_guard_size cap = 0"
apply (clarsimp simp: cap_type_def cap_data_def guard_as_rawdata_def
well_formed_cap_def
split: cdl_cap.splits)
@ -993,7 +978,7 @@ lemma well_formed_tcb_cspace_cap_cap_data:
"\<lbrakk>well_formed spec; tcb_at obj_id spec;
cdl_objects spec obj_id = Some (Tcb tcb);
opt_cap (obj_id, tcb_cspace_slot) spec = Some spec_cspace_cap\<rbrakk>
\<Longrightarrow> cap_data spec_cspace_cap \<noteq> 0"
\<Longrightarrow> cap_data spec_cspace_cap \<noteq> 0"
apply (frule (1) well_formed_tcb_cspace_cap, clarsimp)
apply (frule (1) well_formed_well_formed_cap', clarsimp)
apply (drule (2) cap_data_cap_guard_size_0, simp)
@ -1001,7 +986,7 @@ lemma well_formed_tcb_cspace_cap_cap_data:
lemma well_formed_tcb_opt_cap:
"\<lbrakk>well_formed spec; tcb_at obj_id spec; slot \<in> {0..tcb_boundntfn_slot}\<rbrakk>
\<Longrightarrow> \<exists>cap. opt_cap (obj_id, slot) spec = Some cap"
\<Longrightarrow> \<exists>cap. opt_cap (obj_id, slot) spec = Some cap"
apply (clarsimp simp: object_at_def)
apply (drule (1) well_formed_object_slots)
apply (fastforce simp: object_default_state_def2 is_tcb_def
@ -1014,7 +999,7 @@ lemma well_formed_tcb_opt_cap:
lemma well_formed_tcb_vspace_cap:
"\<lbrakk>well_formed spec;
tcb_at obj_id spec\<rbrakk>
\<Longrightarrow> \<exists>vspace_cap.
\<Longrightarrow> \<exists>vspace_cap.
opt_cap (obj_id, tcb_vspace_slot) spec = Some vspace_cap \<and> is_pd_cap vspace_cap"
apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_vspace_slot], simp add: tcb_slot_defs)
apply (clarsimp simp: object_at_def)
@ -1025,7 +1010,7 @@ lemma well_formed_tcb_vspace_cap:
lemma well_formed_tcb_ipcbuffer_cap:
"\<lbrakk>well_formed spec;
tcb_at obj_id spec\<rbrakk>
\<Longrightarrow> \<exists>tcb_ipcbuffer_cap.
\<Longrightarrow> \<exists>tcb_ipcbuffer_cap.
opt_cap (obj_id, tcb_ipcbuffer_slot) spec = Some tcb_ipcbuffer_cap \<and>
is_default_cap tcb_ipcbuffer_cap \<and> is_frame_cap tcb_ipcbuffer_cap"
apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_ipcbuffer_slot], simp add: tcb_slot_defs)
@ -1036,7 +1021,7 @@ lemma well_formed_tcb_ipcbuffer_cap:
lemma well_formed_tcb_caller_cap:
"\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk>
\<Longrightarrow> opt_cap (obj_id, tcb_caller_slot) spec = Some NullCap"
\<Longrightarrow> opt_cap (obj_id, tcb_caller_slot) spec = Some NullCap"
apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_caller_slot], simp add: tcb_slot_defs)
apply (clarsimp simp: object_at_def)
apply (frule (1) well_formed_well_formed_tcb)
@ -1045,7 +1030,7 @@ lemma well_formed_tcb_caller_cap:
lemma well_formed_tcb_replycap_cap:
"\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk>
\<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) spec = Some NullCap \<or>
\<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) spec = Some NullCap \<or>
opt_cap (obj_id, tcb_replycap_slot) spec = Some (MasterReplyCap obj_id)"
apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_replycap_slot], simp add: tcb_slot_defs)
apply (clarsimp simp: object_at_def)
@ -1056,7 +1041,7 @@ lemma well_formed_tcb_replycap_cap:
lemma well_formed_tcb_pending_op_cap:
"\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk>
\<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) spec = Some NullCap \<or>
\<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) spec = Some NullCap \<or>
opt_cap (obj_id, tcb_pending_op_slot) spec = Some RestartCap"
apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_pending_op_slot], simp add: tcb_slot_defs)
apply (clarsimp simp: object_at_def)
@ -1066,7 +1051,7 @@ lemma well_formed_tcb_pending_op_cap:
lemma well_formed_tcb_pending_op_replycap:
"\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk>
\<Longrightarrow> (opt_cap (obj_id, tcb_replycap_slot) spec = Some (MasterReplyCap obj_id))
\<Longrightarrow> (opt_cap (obj_id, tcb_replycap_slot) spec = Some (MasterReplyCap obj_id))
= (opt_cap (obj_id, tcb_pending_op_slot) spec = Some RestartCap)"
apply (clarsimp simp: object_at_def)
apply (drule (1) well_formed_well_formed_tcb)
@ -1075,7 +1060,7 @@ lemma well_formed_tcb_pending_op_replycap:
lemma well_formed_tcb_boundntfn_cap:
"\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk>
\<Longrightarrow> opt_cap (obj_id, tcb_boundntfn_slot) spec = Some NullCap"
\<Longrightarrow> opt_cap (obj_id, tcb_boundntfn_slot) spec = Some NullCap"
apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_boundntfn_slot], simp add: tcb_slot_defs)
apply (elim exE)
apply (clarsimp simp: object_at_def)
@ -1087,7 +1072,7 @@ lemma well_formed_orig_caps_unique:
cnode_at obj_id spec; cnode_at obj_id' spec; cap_has_object cap; cap_has_object cap';
opt_cap (obj_id, slot) spec = Some cap; opt_cap (obj_id', slot') spec = Some cap';
cap_object cap = cap_object cap'\<rbrakk>
\<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
\<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
by (clarsimp simp: well_formed_def well_formed_orig_caps_unique_def)
lemma well_formed_orig_caps_unique':
@ -1096,19 +1081,19 @@ lemma well_formed_orig_caps_unique':
opt_cap (obj_id, slot) spec = Some cap; opt_cap (obj_id', slot') spec = Some cap';
cap_has_object cap; cap_has_object cap';
cap_object cap = cap_object cap'\<rbrakk>
\<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
\<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
by (clarsimp simp: well_formed_def well_formed_orig_caps_unique_def real_cap_ref_def)
lemma well_formed_irqhandler_caps_unique:
"\<lbrakk>well_formed s; is_irqhandler_cap cap; is_irqhandler_cap cap';
opt_cap (obj_id, slot) s = Some cap; opt_cap (obj_id', slot') s = Some cap';
cap_irq cap = cap_irq cap'\<rbrakk>
\<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
\<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
by (clarsimp simp: well_formed_def well_formed_irqhandler_caps_unique_def)
lemma object_cap_ref_cap_irq:
"\<lbrakk>object_cap_ref (obj_id, slot) spec; opt_cap (obj_id, slot) spec = Some cap\<rbrakk>
\<Longrightarrow> cap_irq cap = undefined"
\<Longrightarrow> cap_irq cap = undefined"
by (auto simp: object_cap_ref_def cap_has_object_def cap_irq_def
split: cdl_cap.splits)
@ -1122,7 +1107,7 @@ lemma well_formed_orig_caps_unique_object_cap:
opt_cap (obj_id, slot) spec = Some cap; opt_cap (obj_id', slot') spec = Some cap';
cap_has_object cap; cap_has_object cap';
cap_object cap = cap_object cap'\<rbrakk>
\<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
\<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
apply (frule object_cap_ref_real_cap_ref, drule (1) object_cap_ref_cap_irq)+
apply (erule (8) well_formed_orig_caps_unique', simp)
done
@ -1130,7 +1115,7 @@ lemma well_formed_orig_caps_unique_object_cap:
lemma well_formed_child_cap_not_copyable:
"\<lbrakk>well_formed spec; \<not> original_cap_at (obj_id, slot) spec;
opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap\<rbrakk>
\<Longrightarrow> is_copyable_cap cap"
\<Longrightarrow> is_copyable_cap cap"
apply (clarsimp simp: well_formed_def)
apply (erule_tac x=obj_id in allE)
apply (clarsimp simp: opt_cap_def opt_object_def slots_of_def)
@ -1142,13 +1127,13 @@ lemma well_formed_child_cap_not_copyable:
lemma well_formed_child_cap_not_copyable':
"\<lbrakk>well_formed spec;
opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap\<rbrakk>
\<Longrightarrow> \<not>original_cap_at (obj_id, slot) spec \<longrightarrow> is_copyable_cap cap"
\<Longrightarrow> \<not>original_cap_at (obj_id, slot) spec \<longrightarrow> is_copyable_cap cap"
by (rule impI, erule (3) well_formed_child_cap_not_copyable)
lemma well_formed_pd:
"\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap;
pd_at obj_id spec; cap \<noteq> NullCap\<rbrakk>
\<Longrightarrow> is_frame_cap cap \<or> is_fake_pt_cap cap"
\<Longrightarrow> is_frame_cap cap \<or> is_fake_pt_cap cap"
apply (clarsimp simp: object_at_def)
apply (frule (1) well_formed_well_formed_vspace)
apply (clarsimp simp: well_formed_vspace_def)
@ -1160,7 +1145,7 @@ lemma well_formed_pd:
lemma well_formed_pt:
"\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap;
pt_at obj_id spec; cap \<noteq> NullCap\<rbrakk>
\<Longrightarrow> is_frame_cap cap"
\<Longrightarrow> is_frame_cap cap"
apply (clarsimp simp: object_at_def)
apply (frule (1) well_formed_well_formed_vspace)
apply (clarsimp simp: well_formed_vspace_def)
@ -1175,6 +1160,26 @@ lemma well_formed_pt_cap_is_fake_pt_cap:
\<Longrightarrow> is_fake_pt_cap cap"
by (frule (2) well_formed_pd, clarsimp+)
lemma wf_cap_pt_cap[simp]: "well_formed_cap (PageTableCap pt_id ty addr) \<longleftrightarrow> addr = None"
by (clarsimp simp: well_formed_cap_def)
lemma wf_frame_cap_frame_size_bits:
"\<lbrakk>well_formed spec;
opt_cap (pt_ptr, slot) spec = Some (FrameCap dev frame_ptr rights n Fake None);
cdl_objects spec frame_ptr = Some (Frame frame)\<rbrakk>
\<Longrightarrow> cdl_frame_size_bits frame = n"
apply (clarsimp simp: opt_cap_def slots_of_def opt_object_def split: option.splits)
apply (frule (2) well_formed_well_formed_cap_types_match, fastforce)
apply (fastforce simp: well_formed_cap_types_match_def cap_object_def object_type_def)
done
lemma wf_pd_cap_has_object:
"\<lbrakk>well_formed spec;
pd_at spec_pd_ptr spec;
opt_cap (spec_pd_ptr, slot) spec = Some cap;
cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_has_object cap"
by (fastforce simp: cap_has_object_def cap_type_def is_fake_pt_cap_def
dest: well_formed_pd split: cdl_cap.splits)
(****************************************
@ -1237,7 +1242,7 @@ lemma well_formed_irq_nodes_cdl_irq_node:
lemma well_formed_cdl_irq_node_irq_nodes:
"\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
\<Longrightarrow> cdl_irq_node spec irq \<in> irq_nodes spec"
\<Longrightarrow> cdl_irq_node spec irq \<in> irq_nodes spec"
apply (drule well_formed_well_formed_irq_table)
apply (clarsimp simp: well_formed_irq_table_def)
apply (fastforce simp: object_at_def)
@ -1245,14 +1250,14 @@ lemma well_formed_cdl_irq_node_irq_nodes:
lemma well_formed_irq_is_irq_node:
"\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
\<Longrightarrow> is_irq_node irq_node"
\<Longrightarrow> is_irq_node irq_node"
apply (frule (1) well_formed_cdl_irq_node_irq_nodes)
apply (clarsimp simp: irq_nodes_def object_at_def)
done
lemma well_formed_object_slots_irq_node:
"\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
\<Longrightarrow> dom (object_slots irq_node) = {0}"
\<Longrightarrow> dom (object_slots irq_node) = {0}"
apply (frule (1) well_formed_cdl_irq_node_irq_nodes)
apply (frule (1) well_formed_well_formed_irq_node)
apply (clarsimp simp: well_formed_irq_node_def)
@ -1262,7 +1267,7 @@ lemma well_formed_irq_ntfn_cap:
"\<lbrakk>well_formed spec;
irq \<in> bound_irqs spec;
opt_cap (cdl_irq_node spec irq, 0) spec = Some ntfn_cap\<rbrakk>
\<Longrightarrow> ntfn_cap = NotificationCap (cap_object ntfn_cap) 0 {AllowRead, AllowWrite}"
\<Longrightarrow> ntfn_cap = NotificationCap (cap_object ntfn_cap) 0 {AllowRead, AllowWrite}"
apply (frule opt_cap_cdl_objects, clarsimp)
apply (frule (1) well_formed_object_slots_irq_node [where irq=irq])
apply (frule (1) well_formed_well_formed_irq_node)
@ -1284,7 +1289,7 @@ lemma well_formed_bound_irqs_are_used_irqs:
lemma well_formed_slots_of_used_irq_node:
"\<lbrakk>well_formed spec; irq \<in> used_irqs spec\<rbrakk>
\<Longrightarrow> dom (slots_of (cdl_irq_node spec irq) spec) = {0}"
\<Longrightarrow> dom (slots_of (cdl_irq_node spec irq) spec) = {0}"
apply (clarsimp simp: used_irqs_def slots_of_def opt_object_def split: option.splits)
apply (frule (2) well_formed_all_caps_cap_irq, clarsimp)
apply (erule (1) well_formed_object_slots_irq_node)
@ -1292,14 +1297,14 @@ lemma well_formed_slots_of_used_irq_node:
lemma well_formed_slot_0_of_used_irq_node:
"\<lbrakk>well_formed spec; irq \<in> used_irqs spec\<rbrakk>
\<Longrightarrow> \<exists>ntfn_cap. slots_of (cdl_irq_node spec irq) spec 0 = Some ntfn_cap"
\<Longrightarrow> \<exists>ntfn_cap. slots_of (cdl_irq_node spec irq) spec 0 = Some ntfn_cap"
apply (frule (1) well_formed_slots_of_used_irq_node)
apply (clarsimp simp: dom_eq_singleton_conv)
done
lemma well_formed_object_slots_default_irq_node:
"\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
\<Longrightarrow> dom (object_slots (object_default_state irq_node)) = {0}"
\<Longrightarrow> dom (object_slots (object_default_state irq_node)) = {0}"
by (metis well_formed_object_slots well_formed_object_slots_irq_node)
lemma object_slots_empty_cnode:
@ -1315,7 +1320,7 @@ lemma dom_empty_cap_map_singleton:
lemma well_formed_size_irq_node:
"\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
\<Longrightarrow> object_size_bits irq_node = 0"
\<Longrightarrow> object_size_bits irq_node = 0"
apply (frule (1) well_formed_irq_is_irq_node)
apply (frule (1) well_formed_object_slots)
apply (drule (1) well_formed_object_slots_default_irq_node)
@ -1326,14 +1331,14 @@ lemma well_formed_size_irq_node:
lemma well_formed_used_irqs_have_irq_node:
"\<lbrakk>well_formed spec; irq \<in> used_irqs spec\<rbrakk>
\<Longrightarrow> \<exists>irq_node. cdl_objects spec (cdl_irq_node spec irq) = Some irq_node"
\<Longrightarrow> \<exists>irq_node. cdl_objects spec (cdl_irq_node spec irq) = Some irq_node"
apply (clarsimp simp: used_irqs_def)
apply (erule (2) well_formed_all_caps_cap_irq)
done
lemma well_formed_bound_irqs_have_irq_node:
"\<lbrakk>well_formed spec; irq \<in> bound_irqs spec\<rbrakk>
\<Longrightarrow> \<exists>irq_node. cdl_objects spec (cdl_irq_node spec irq) = Some irq_node"
\<Longrightarrow> \<exists>irq_node. cdl_objects spec (cdl_irq_node spec irq) = Some irq_node"
apply (frule well_formed_well_formed_irqhandler_caps)
apply (clarsimp simp: well_formed_irqhandler_caps_def used_irqs_def bound_irqs_def all_caps_def)
done
@ -1341,7 +1346,7 @@ lemma well_formed_bound_irqs_have_irq_node:
lemma well_formed_irq_node_is_bound:
"\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node;
object_slots irq_node 0 \<noteq> Some NullCap\<rbrakk>
\<Longrightarrow> irq \<in> bound_irqs spec"
\<Longrightarrow> irq \<in> bound_irqs spec"
apply (frule well_formed_well_formed_irqhandler_caps)
apply (frule (1) well_formed_object_slots_default_irq_node)
apply (frule (1) well_formed_object_slots)
@ -1376,7 +1381,7 @@ lemma well_formed_cap_object_cdl_irq_node:
(* There are no untyped objects (as there are no untyped caps). *)
lemma well_formed_object_untyped:
"\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some object\<rbrakk>
\<Longrightarrow> object_type object \<noteq> UntypedType"
\<Longrightarrow> object_type object \<noteq> UntypedType"
apply (case_tac "real_object_at obj_id spec")
apply (frule (1) well_formed_cap_to_real_object)
apply clarsimp
@ -1411,7 +1416,7 @@ lemma well_formed_no_asidpools:
lemma well_formed_fake_pt_cap_in_pd:
"\<lbrakk>well_formed spec; slots_of obj_id spec slot = Some cap; is_fake_pt_cap cap\<rbrakk>
\<Longrightarrow> pd_at obj_id spec"
\<Longrightarrow> pd_at obj_id spec"
apply (clarsimp simp: slots_of_def opt_object_def split: option.splits)
apply (rename_tac obj)
apply (frule well_formed_asidpool_at [where obj_id=obj_id])
@ -1428,6 +1433,18 @@ lemma well_formed_fake_pt_cap_in_pd:
apply (clarsimp simp: is_fake_pt_cap_is_pt_cap object_slots_def)
done
lemma well_formed_pt_cap_pt_at:
"\<lbrakk>well_formed spec; opt_cap cap_ref spec = Some cap; is_fake_pt_cap cap\<rbrakk>
\<Longrightarrow> pt_at (cap_object cap) spec"
apply (case_tac cap_ref, clarsimp)
apply (frule (1) well_formed_cap_object)
apply (fastforce intro: is_fake_pt_cap_cap_has_object)
apply clarsimp
apply (frule (2) well_formed_types_match)
apply (fastforce intro: is_fake_pt_cap_cap_has_object)
apply (clarsimp simp: is_fake_pt_cap_is_pt_cap object_at_def object_type_is_object)
done
lemma cap_has_object_cap_irq [simp]:
"cap_has_object cap \<Longrightarrow> cap_irq cap = undefined"
by (auto simp: cap_has_object_def cap_irq_def split: cdl_cap.splits)
@ -1573,7 +1590,7 @@ lemma well_formed_objects_only_real_or_irq:
lemma well_formed_objects_card:
"\<lbrakk>well_formed spec \<rbrakk>
\<Longrightarrow> card (used_irqs spec) + card {x. real_object_at x spec} = card (dom (cdl_objects spec))"
\<Longrightarrow> card (used_irqs spec) + card {x. real_object_at x spec} = card (dom (cdl_objects spec))"
apply (frule well_formed_inj_cdl_irq_node)
apply (frule well_formed_objects_real_or_irq)
apply (frule well_formed_objects_only_real_or_irq)
@ -1673,6 +1690,153 @@ lemma update_cap_data:
apply simp
done
lemma well_formed_frame_in_pt:
"\<lbrakk>well_formed spec;
opt_cap (pt, pt_slot) spec = Some frame_cap;
frame_cap \<noteq> NullCap;
pt_at pt spec\<rbrakk>
\<Longrightarrow> \<exists>sz. cap_type frame_cap = Some (FrameType sz) \<and>
(sz = 12 \<or> sz = 16) \<and>
is_fake_vm_cap frame_cap"
apply (clarsimp simp: well_formed_def object_at_def)
apply (drule_tac x = pt in spec)
apply (clarsimp simp: well_formed_vspace_def opt_cap_def slots_of_def opt_object_def
split: option.split_asm)
done
lemma well_formed_frame_in_pd:
"\<lbrakk>well_formed spec;
opt_cap (pd, pt_slot) spec = Some frame_cap;
pd_at pd spec;
is_frame_cap frame_cap\<rbrakk>
\<Longrightarrow> (\<exists>sz. cap_type frame_cap = Some (FrameType sz) \<and> (sz = 20 \<or> sz = 24)) \<and>
is_fake_vm_cap frame_cap \<and>
\<not> is_device_cap frame_cap"
apply (clarsimp simp: well_formed_def object_at_def)
apply (drule_tac x = pd in spec)
apply (clarsimp simp: well_formed_vspace_def opt_cap_def slots_of_def opt_object_def
split: option.split_asm)
apply (drule_tac x = pt_slot in spec)
apply (drule_tac x = frame_cap in spec)
apply (clarsimp simp: is_fake_pt_cap_def cap_type_def
split: cdl_cap.splits)
apply (clarsimp simp: cap_at_def opt_cap_def slots_of_def opt_object_def
simp del: split_paired_All)
apply (drule_tac x = pd in spec)
apply (drule_tac x = pt_slot in spec)
apply fastforce
done
lemma well_formed_no_dev: "well_formed spec \<Longrightarrow> \<forall>slot. \<not> cap_at is_device_cap slot spec"
by (clarsimp simp: well_formed_def)
lemma well_formed_frame_cap[simp]:
"well_formed_cap (FrameCap x y rights a b R) \<longleftrightarrow>
R = None \<and> (rights = vm_read_write \<or> rights = vm_read_only)"
apply (clarsimp simp: well_formed_cap_def split: cdl_frame_cap_type.splits)
apply (rule iffI; clarsimp?)
done
lemma wf_cap_in_pt_is_frame:
"well_formed spec \<Longrightarrow>
page_cap \<noteq> NullCap \<Longrightarrow>
pt_at pt_id spec \<Longrightarrow>
opt_cap (pt_id, slot) spec = Some page_cap \<Longrightarrow>
page_cap = fake_frame_cap False (cap_object page_cap)
(validate_vm_rights (cap_rights page_cap))
(cap_size_bits page_cap) \<and>
(cap_size_bits page_cap = 12 \<or> cap_size_bits page_cap = 16)"
apply (frule well_formed_frame_in_pt, fastforce+)
apply (clarsimp simp: cap_type_def cap_rights_def cap_size_bits_def split: cdl_cap.splits)
apply (frule well_formed_well_formed_cap[where obj_id=pt_id])
apply (fastforce intro: object_slots_opt_capI)+
apply clarsimp
apply (drule well_formed_no_dev, clarsimp simp: cap_at_def)
apply (fastforce simp: fake_vm_cap_simp)
done
lemma wf_frame_cap_in_pd:
"well_formed spec \<Longrightarrow>
page_cap \<noteq> NullCap \<Longrightarrow>
pd_at pd_id spec \<Longrightarrow>
opt_cap (pd_id, slot) spec = Some page_cap \<Longrightarrow>
frame_at (cap_object page_cap) spec \<Longrightarrow>
page_cap = fake_frame_cap False (cap_object page_cap)
(validate_vm_rights (cap_rights page_cap))
(cap_size_bits page_cap) \<and>
(cap_size_bits page_cap = 20 \<or> cap_size_bits page_cap = 24)"
apply (frule well_formed_frame_in_pd, fastforce+)
apply (frule well_formed_types_match, fastforce+)
using object_type_is_object(9) object_type_object_at(9) wf_pd_cap_has_object apply blast
apply (frule object_at_object_type(10)[rotated], rule classical, fastforce)
apply (fastforce simp: cap_type_def split: cdl_cap.splits)
apply (clarsimp simp: cap_type_def cap_rights_def cap_size_bits_def split: cdl_cap.splits)
apply (frule well_formed_well_formed_cap[where obj_id=pd_id])
apply fastforce
apply (fastforce intro: object_slots_opt_capI)
apply (fastforce simp: fake_vm_cap_simp)+
done
lemma wf_pt_in_pd_fake_and_none:
"well_formed spec \<Longrightarrow>
page_cap \<noteq> NullCap \<Longrightarrow>
pd_at pd_id spec \<Longrightarrow>
opt_cap (pd_id, slot) spec = Some page_cap \<Longrightarrow>
pt_at (cap_object page_cap) spec \<Longrightarrow>
page_cap = PageTableCap (cap_object page_cap) Fake None"
apply (clarsimp simp: object_at_def)
apply (frule well_formed_types_match[where obj_id=pd_id and slot=slot])
apply fastforce+
using object_at_def wf_pd_cap_has_object
apply blast
apply (clarsimp simp: object_type_is_object)
apply (frule well_formed_pt_cap_is_fake_pt_cap[where obj_id=pd_id and slot=slot])
apply fastforce
apply (clarsimp simp: object_at_def)
apply (clarsimp simp: object_type_is_object)
apply (frule (1) well_formed_well_formed_cap[where obj_id=pd_id and slot=slot])
apply (clarsimp simp: opt_cap_def slots_of_def opt_object_def split: option.splits)
apply fastforce+
apply (clarsimp simp: cap_type_def is_fake_pt_cap_pt_cap split: cdl_cap.splits)
using well_formed_well_formed_cap' wf_cap_pt_cap by blast
lemma well_formed_pd_slots_have_objects:
"\<lbrakk>well_formed spec; pd_at pd_id spec; slot \<in> dom (slots_of pd_id spec);
slots_of pd_id spec slot = Some cap; cap \<noteq> NullCap\<rbrakk>
\<Longrightarrow> cap_has_object cap"
apply (drule (1) wf_pd_cap_has_object[where cap=cap and slot=slot])
apply (clarsimp simp: opt_cap_def)+
done
lemma well_formed_pd_slot_limited:
"\<lbrakk>well_formed spec; pd_at obj_id spec; slots_of obj_id spec slot = Some cap\<rbrakk>
\<Longrightarrow> slot < 4096"
apply (clarsimp simp:well_formed_def object_at_def)
apply (drule_tac x = obj_id in spec)
apply (clarsimp simp: is_pd_def object_type_simps object_default_state_def slots_of_def,
simp add: default_object_def object_type_simps opt_object_def object_slots_def empty_cap_map_def
split: cdl_object.split_asm option.split_asm)
apply fastforce
done
lemma well_formed_pd_frame_or_pt:
"well_formed spec \<Longrightarrow>
pd_at pd_ptr spec \<Longrightarrow>
opt_cap (pd_ptr,slot) spec = Some slot_cap \<Longrightarrow>
cap_object slot_cap = ptr \<Longrightarrow>
slot_cap \<noteq> NullCap \<Longrightarrow>
frame_at ptr spec \<noteq> pt_at ptr spec"
apply (frule (3) well_formed_pd[where obj_id=pd_ptr and slot=slot])
apply clarsimp
apply (frule (3) wf_pd_cap_has_object)
apply (frule (2) well_formed_cap_object)
apply clarsimp
apply (safe; (fastforce simp: object_at_def dest: not_frame_and_pt)?)
apply (frule well_formed_types_match[where obj_id=pd_ptr and slot=slot], fastforce+)
apply (fastforce simp: object_type_is_object(10) intro: object_at_cdl_objects)
apply (frule well_formed_types_match[where obj_id=pd_ptr and slot=slot], fastforce+)
using is_fake_pt_cap_is_pt_cap object_type_is_object(8) by (fastforce intro: object_at_cdl_objects)
end
end