theory CSpace1_R

lemma pspace_relation_cte_wp_atI':
  "\<lbrakk> pspace_relation (kheap s) (ksPSpace s');
     cte_wp_at' ((=) cte) x s'; valid_objs s \<rbrakk>
  \<Longrightarrow> \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> x = cte_map slot" apply (simp add: cte_wp_at_cases') apply (elim disjE conjE exE) apply (erule(1) pspace_dom_relatedE) apply (erule(1) obj_relation_cutsE, simp_all split: if_split_asm)[1] apply (intro exI, rule conjI[OF _ conjI [OF _ refl]]) apply (simp add: cte_wp_at_cases domI well_formed_cnode_invsI) apply (simp split: if_split_asm) apply (erule(1) pspace_dom_relatedE) apply (erule(1) obj_relation_cutsE, simp_all split: if_split_asm) apply (simp add: other_obj_relation_def
            split: Structures_A.kernel_object.split_asm
                   ARM_A.arch_kernel_obj.split_asm) apply (subgoal_tac "n = x - y", clarsimp) apply (drule tcb_cases_related2, clarsimp) apply (intro exI, rule conjI) apply (erule(1) cte_wp_at_tcbI[where t="(a, b)" for a b, simplified]) apply fastforce apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); cte_wp_at' ((=) cte) x s'; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> x = cte_map slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ksPSpace s' x = Some (KOCTE cte) \<and> is_aligned x cte_level_bits \<and> ps_clear x cteSizeBits s' \<or> (\<exists>n tcb. ksPSpace s' (x - n) = Some (KOTCB tcb) \<and> is_aligned (x - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> cte = getF tcb \<and> ps_clear (x - n) tcbBlockSizeBits s')); valid_objs s\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap cte) \<and> x = cte_map (a, b) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; ksPSpace s' x = Some (KOCTE cte); is_aligned x cte_level_bits; ps_clear x cteSizeBits s'\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap cte) \<and> x = cte_map (a, b)
 2. \<And>n tcb getF setF. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; ksPSpace s' (x - n) = Some (KOTCB tcb); is_aligned (x - n) tcbBlockSizeBits; cte = getF tcb; ps_clear (x - n) tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap cte) \<and> x = cte_map (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>y ko P. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned x cte_level_bits; ps_clear x cteSizeBits s'; kheap s y = Some ko; (x, P) \<in> obj_relation_cuts ko y; P ko (KOCTE cte)\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap cte) \<and> x = cte_map (a, b)
 2. \<And>n tcb getF setF. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; ksPSpace s' (x - n) = Some (KOTCB tcb); is_aligned (x - n) tcbBlockSizeBits; cte = getF tcb; ps_clear (x - n) tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap cte) \<and> x = cte_map (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>y ko P sz cs z cap ctea. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned (cte_map (y, z)) cte_level_bits; ps_clear (cte_map (y, z)) cteSizeBits s'; kheap s y = Some (CNode sz cs); P (CNode sz cs) (KOCTE ctea); ko = CNode sz cs; well_formed_cnode_n sz cs; x = cte_map (y, z); cte = ctea; cs z = Some cap; cap_relation cap (cteCap ctea)\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap ctea) \<and> cte_map (y, z) = cte_map (a, b)
 2. \<And>n tcb getF setF. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; ksPSpace s' (x - n) = Some (KOTCB tcb); is_aligned (x - n) tcbBlockSizeBits; cte = getF tcb; ps_clear (x - n) tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap cte) \<and> x = cte_map (a, b) proof (prove)
goal (3 subgoals):
 1. \<And>y ko P sz cs z cap ctea. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned (cte_map (y, z)) cte_level_bits; ps_clear (cte_map (y, z)) cteSizeBits s'; kheap s y = Some (CNode sz cs); P (CNode sz cs) (KOCTE ctea); ko = CNode sz cs; well_formed_cnode_n sz cs; x = cte_map (y, z); cte = ctea; cs z = Some cap; cap_relation cap (cteCap ctea)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?c23 y ko P sz cs z cap ctea)) (y, z) s
 2. \<And>y ko P sz cs z cap ctea. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned (cte_map (y, z)) cte_level_bits; ps_clear (cte_map (y, z)) cteSizeBits s'; kheap s y = Some (CNode sz cs); P (CNode sz cs) (KOCTE ctea); ko = CNode sz cs; well_formed_cnode_n sz cs; x = cte_map (y, z); cte = ctea; cs z = Some cap; cap_relation cap (cteCap ctea)\<rbrakk> \<Longrightarrow> cap_relation (?c23 y ko P sz cs z cap ctea) (cteCap ctea)
 3. \<And>n tcb getF setF. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; ksPSpace s' (x - n) = Some (KOTCB tcb); is_aligned (x - n) tcbBlockSizeBits; cte = getF tcb; ps_clear (x - n) tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap cte) \<and> x = cte_map (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>y ko P sz cs z cap ctea. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned (cte_map (y, z)) cte_level_bits; ps_clear (cte_map (y, z)) cteSizeBits s'; kheap s y = Some (CNode sz cs); P (CNode sz cs) (KOCTE ctea); ko = CNode sz cs; well_formed_cnode_n sz cs; x = cte_map (y, z); cte = ctea; cs z = Some cap; cap_relation cap (cteCap ctea)\<rbrakk> \<Longrightarrow> cap_relation cap (cteCap ctea)
 2. \<And>n tcb getF setF. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; ksPSpace s' (x - n) = Some (KOTCB tcb); is_aligned (x - n) tcbBlockSizeBits; cte = getF tcb; ps_clear (x - n) tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap cte) \<and> x = cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; ksPSpace s' (x - n) = Some (KOTCB tcb); is_aligned (x - n) tcbBlockSizeBits; cte = getF tcb; ps_clear (x - n) tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap cte) \<and> x = cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF y ko P. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned (x - n) tcbBlockSizeBits; cte = getF tcb; ps_clear (x - n) tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF); kheap s y = Some ko; (x - n, P) \<in> obj_relation_cuts ko y; P ko (KOTCB tcb)\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap cte) \<and> x = cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF y ko P. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF); kheap s y = Some ko; P ko (KOTCB tcb); x - n = y; other_obj_relation ko (KOTCB tcb); is_other_obj_relation_type (a_type ko)\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap (getF tcb)) \<and> x = cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF y ko P x2. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF); kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); x - n = y; ko = TCB x2; tcb_relation x2 tcb\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap (getF tcb)) \<and> x = cte_map (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>tcb getF setF y P x2. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; tcb_cte_cases (x - y) = Some (getF, setF); kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap (getF tcb)) \<and> x = cte_map (a, b)
 2. \<And>n tcb getF setF y ko P x2. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF); kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); x - n = y; ko = TCB x2; tcb_relation x2 tcb\<rbrakk> \<Longrightarrow> n = x - y proof (prove)
goal (2 subgoals):
 1. \<And>tcb getF setF y P x2 getF' setF' restr. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb; tcb_cap_cases (tcb_cnode_index (unat (x - y >> cte_level_bits))) = Some (getF', setF', restr); cte_map (y, tcb_cnode_index (unat (x - y >> cte_level_bits))) = x; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (getF 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) (setF (\<lambda>x. cte) tcb'))\<rbrakk> \<Longrightarrow> \<exists>c a b. cte_wp_at ((=) c) (a, b) s \<and> cap_relation c (cteCap (getF tcb)) \<and> x = cte_map (a, b)
 2. \<And>n tcb getF setF y ko P x2. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF); kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); x - n = y; ko = TCB x2; tcb_relation x2 tcb\<rbrakk> \<Longrightarrow> n = x - y proof (prove)
goal (3 subgoals):
 1. \<And>tcb getF setF y P x2 getF' setF' restr. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb; tcb_cap_cases (tcb_cnode_index (unat (x - y >> cte_level_bits))) = Some (getF', setF', restr); cte_map (y, tcb_cnode_index (unat (x - y >> cte_level_bits))) = x; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (getF 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) (setF (\<lambda>x. cte) tcb'))\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?c107 tcb getF setF y P x2 getF' setF' restr)) (?a108 tcb getF setF y P x2 getF' setF' restr, ?b109 tcb getF setF y P x2 getF' setF' restr) s
 2. \<And>tcb getF setF y P x2 getF' setF' restr. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb; tcb_cap_cases (tcb_cnode_index (unat (x - y >> cte_level_bits))) = Some (getF', setF', restr); cte_map (y, tcb_cnode_index (unat (x - y >> cte_level_bits))) = x; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (getF 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) (setF (\<lambda>x. cte) tcb'))\<rbrakk> \<Longrightarrow> cap_relation (?c107 tcb getF setF y P x2 getF' setF' restr) (cteCap (getF tcb)) \<and> x = cte_map (?a108 tcb getF setF y P x2 getF' setF' restr, ?b109 tcb getF setF y P x2 getF' setF' restr)
 3. \<And>n tcb getF setF y ko P x2. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF); kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); x - n = y; ko = TCB x2; tcb_relation x2 tcb\<rbrakk> \<Longrightarrow> n = x - y proof (prove)
goal (3 subgoals):
 1. \<And>tcb getF setF y P x2 getF' setF' restr. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb; tcb_cap_cases (tcb_cnode_index (unat (x - y >> cte_level_bits))) = Some (getF', setF', restr); cte_map (y, tcb_cnode_index (unat (x - y >> cte_level_bits))) = x; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (getF 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) (setF (\<lambda>x. cte) tcb'))\<rbrakk> \<Longrightarrow> ?c107 tcb getF setF y P x2 getF' setF' restr = getF' x2
 2. \<And>tcb getF setF y P x2 getF' setF' restr. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb; tcb_cap_cases (tcb_cnode_index (unat (x - y >> cte_level_bits))) = Some (getF', setF', restr); cte_map (y, tcb_cnode_index (unat (x - y >> cte_level_bits))) = x; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (getF 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) (setF (\<lambda>x. cte) tcb'))\<rbrakk> \<Longrightarrow> cap_relation (?c107 tcb getF setF y P x2 getF' setF' restr) (cteCap (getF tcb)) \<and> x = cte_map (y, tcb_cnode_index (unat (x - y >> cte_level_bits)))
 3. \<And>n tcb getF setF y ko P x2. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF); kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); x - n = y; ko = TCB x2; tcb_relation x2 tcb\<rbrakk> \<Longrightarrow> n = x - y proof (prove)
goal (2 subgoals):
 1. \<And>tcb getF setF y P x2 getF' setF' restr. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); tcb_relation x2 tcb; tcb_cap_cases (tcb_cnode_index (unat (x - y >> cte_level_bits))) = Some (getF', setF', restr); cte_map (y, tcb_cnode_index (unat (x - y >> cte_level_bits))) = x; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (getF 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) (setF (\<lambda>x. cte) tcb'))\<rbrakk> \<Longrightarrow> cap_relation (getF' x2) (cteCap (getF tcb)) \<and> x = cte_map (y, tcb_cnode_index (unat (x - y >> cte_level_bits)))
 2. \<And>n tcb getF setF y ko P x2. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF); kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); x - n = y; ko = TCB x2; tcb_relation x2 tcb\<rbrakk> \<Longrightarrow> n = x - y proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF y ko P x2. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap s) (ksPSpace s'); valid_objs s; is_aligned y tcbBlockSizeBits; cte = getF tcb; ps_clear y tcbBlockSizeBits s'; tcb_cte_cases n = Some (getF, setF); kheap s y = Some (TCB x2); P (TCB x2) (KOTCB tcb); x - n = y; ko = TCB x2; tcb_relation x2 tcb\<rbrakk> \<Longrightarrow> n = x - y proof (prove)
goal:
No subgoals!