theory CSpace1_R

lemma cte_map_pulls_tcb_to_abstract:
  "\<lbrakk> y = cte_map z; pspace_relation (kheap s) (ksPSpace s');
     ksPSpace s' x = Some (KOTCB tcb);
     pspace_aligned s; pspace_distinct s; valid_objs s;
     cte_at z s; (y - x) \<in> dom tcb_cte_cases \<rbrakk>
     \<Longrightarrow> \<exists>tcb'. kheap s x = Some (TCB tcb') \<and> tcb_relation tcb' tcb
                  \<and> (z = (x, tcb_cnode_index (unat ((y - x) >> cte_level_bits))))" apply (rule pspace_dom_relatedE, assumption+) apply (erule(1) obj_relation_cutsE, simp_all split: if_split_asm) apply (clarsimp simp: other_obj_relation_def
                 split: Structures_A.kernel_object.split_asm
                        ARM_A.arch_kernel_obj.split_asm) apply (drule tcb_cases_related2) apply clarsimp apply (frule(1) cte_wp_at_tcbI [OF _ _ TrueI, where t="(a, b)" for a b, simplified]) apply (erule(5) cte_map_inj_eq [OF sym]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' x = Some (KOTCB tcb); pspace_aligned s; pspace_distinct s; valid_objs s; cte_wp_at (\<lambda>_. True) z s; y - x \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> \<exists>tcb'. kheap s x = Some (TCB tcb') \<and> tcb_relation tcb' tcb \<and> z = (x, tcb_cnode_index (unat (y - x >> cte_level_bits))) proof (prove)
goal (1 subgoal):
 1. \<And>ya ko P. \<lbrakk>y = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' x = Some (KOTCB tcb); pspace_aligned s; pspace_distinct s; valid_objs s; cte_wp_at (\<lambda>_. True) z s; y - x \<in> dom tcb_cte_cases; kheap s ya = Some ko; (x, P) \<in> obj_relation_cuts ko ya; P ko (KOTCB tcb)\<rbrakk> \<Longrightarrow> \<exists>tcb'. kheap s x = Some (TCB tcb') \<and> tcb_relation tcb' tcb \<and> z = (x, tcb_cnode_index (unat (y - x >> cte_level_bits))) proof (prove)
goal (1 subgoal):
 1. \<And>ya ko P. \<lbrakk>y = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' ya = Some (KOTCB tcb); pspace_aligned s; pspace_distinct s; valid_objs s; cte_wp_at (\<lambda>_. True) z s; cte_map z - ya \<in> dom tcb_cte_cases; kheap s ya = Some ko; P ko (KOTCB tcb); x = ya; other_obj_relation ko (KOTCB tcb); is_other_obj_relation_type (a_type ko)\<rbrakk> \<Longrightarrow> \<exists>tcb'. ko = TCB tcb' \<and> tcb_relation tcb' tcb \<and> z = (ya, tcb_cnode_index (unat (cte_map z - ya >> cte_level_bits))) proof (prove)
goal (1 subgoal):
 1. \<And>P x2 a b. \<lbrakk>is_other_obj_relation_type ATCB; y = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' x = Some (KOTCB tcb); pspace_aligned s; pspace_distinct s; valid_objs s; cte_wp_at (\<lambda>_. True) z s; kheap s x = Some (TCB x2); P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb; tcb_cte_cases (cte_map z - x) = Some (a, b)\<rbrakk> \<Longrightarrow> z = (x, tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) proof (prove)
goal (1 subgoal):
 1. \<And>P x2 a b. \<lbrakk>is_other_obj_relation_type ATCB; y = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' x = Some (KOTCB tcb); pspace_aligned s; pspace_distinct s; valid_objs s; cte_wp_at (\<lambda>_. True) z s; kheap s x = Some (TCB x2); P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb; \<exists>getF' setF' restr. tcb_cap_cases (tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) = Some (getF', setF', restr) \<and> cte_map (x, tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) = cte_map z \<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (a tcb'))) \<and> (\<forall>tcb tcb' cap cte. tcb_relation tcb tcb' \<longrightarrow> cap_relation cap (cteCap cte) \<longrightarrow> tcb_relation (setF' (\<lambda>x. cap) tcb) (b (\<lambda>x. cte) tcb'))\<rbrakk> \<Longrightarrow> z = (x, tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) proof (prove)
goal (1 subgoal):
 1. \<And>P x2 a b getF' setF' restr. \<lbrakk>is_other_obj_relation_type ATCB; y = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' x = Some (KOTCB tcb); pspace_aligned s; pspace_distinct s; valid_objs s; cte_wp_at (\<lambda>_. True) z s; kheap s x = Some (TCB x2); P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb; tcb_cap_cases (tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) = Some (getF', setF', restr); cte_map (x, tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) = cte_map z; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (a tcb')); \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> (\<forall>cap cte. cap_relation cap (cteCap cte) \<longrightarrow> tcb_relation (setF' (\<lambda>x. cap) tcb) (b (\<lambda>x. cte) tcb'))\<rbrakk> \<Longrightarrow> z = (x, tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) proof (prove)
goal (1 subgoal):
 1. \<And>P x2 a b getF' setF' restr. \<lbrakk>is_other_obj_relation_type ATCB; y = cte_map z; pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' x = Some (KOTCB tcb); pspace_aligned s; pspace_distinct s; valid_objs s; cte_wp_at (\<lambda>_. True) z s; kheap s x = Some (TCB x2); P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb; tcb_cap_cases (tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) = Some (getF', setF', restr); cte_map (x, tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) = cte_map z; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (a tcb')); \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> (\<forall>cap cte. cap_relation cap (cteCap cte) \<longrightarrow> tcb_relation (setF' (\<lambda>x. cap) tcb) (b (\<lambda>x. cte) tcb')); cte_wp_at (\<lambda>a. True) (x, tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) s\<rbrakk> \<Longrightarrow> z = (x, tcb_cnode_index (unat (cte_map z - x >> cte_level_bits))) proof (prove)
goal:
No subgoals!