theory KHeap_R

lemma setObject_cte_wp_at2':
  assumes x: "\<And>x n tcb s t. \<lbrakk> t \<in> fst (updateObject v (KOTCB tcb) ptr x n s); Q s;
                               lookupAround2 ptr (ksPSpace s) = (Some (x, KOTCB tcb), n) \<rbrakk>
                  \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF) \<in> ran tcb_cte_cases. getF tcb' = getF tcb)"
  assumes y: "\<And>x n cte s. fst (updateObject v (KOCTE cte) ptr x n s) = {}"
  shows      "\<lbrace>\<lambda>s. P' (cte_wp_at' P p s) \<and> Q s\<rbrace> setObject ptr v \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s)\<rbrace>" apply (clarsimp simp add: setObject_def valid_def in_monad split_def) apply (simp add: cte_wp_at_cases' split del: if_split) apply (erule rsubst[where P=P']) apply (rule iffI) apply (erule disjEI) apply (clarsimp simp: ps_clear_upd lookupAround2_char1 y) apply (erule exEI [where 'a=word32]) apply (clarsimp simp: ps_clear_upd lookupAround2_char1) apply (drule(1) x) apply (clarsimp simp: lookupAround2_char1 prod_eqI) apply (fastforce dest: bspec [OF _ ranI]) apply (erule disjEI) apply (clarsimp simp: ps_clear_upd lookupAround2_char1
                  split: if_split_asm) apply (frule updateObject_type) apply (case_tac ba, simp_all add: y)[1] apply (erule exEI) apply (clarsimp simp: ps_clear_upd lookupAround2_char1
                 split: if_split_asm) apply (frule updateObject_type) apply (case_tac ba, simp_all) apply (drule(1) x) apply (clarsimp simp: prod_eqI lookupAround2_char1) apply (fastforce dest: bspec [OF _ ranI]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (cte_wp_at' P p s) \<and> Q s\<rbrace> setObject ptr v \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>P' (cte_wp_at' P p s); Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> P' (cte_wp_at' P p (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>P' ((\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s))); Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> P' ((\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> ((\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s))) = ((\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s))\<rbrakk> \<Longrightarrow> (\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))
 2. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); (\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s\<rbrakk> \<Longrightarrow> \<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)
 2. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)\<rbrakk> \<Longrightarrow> \<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))
 3. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); (\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)\<rbrakk> \<Longrightarrow> \<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))
 2. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); (\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba s'' obj' x. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<exists>tcb. ksPSpace s (p - x) = Some (KOTCB tcb) \<and> is_aligned (p - x) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases x = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - x) tcbBlockSizeBits s)\<rbrakk> \<Longrightarrow> \<exists>tcb. (if p - x = a then Some obj' else ksPSpace s (p - x)) = Some (KOTCB tcb) \<and> is_aligned (p - x) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases x = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - x) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))
 2. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); (\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) proof (prove)
goal (2 subgoals):
 1. \<And>s s'' obj' x tcb getF setF. \<lbrakk>Q s; (obj', s'') \<in> fst (updateObject v (KOTCB tcb) ptr (p - x) (snd (lookupAround2 ptr (ksPSpace s))) s); p - x \<le> ptr; ksPSpace s (p - x) = Some (KOTCB tcb); \<forall>z. p - x < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned (p - x) tcbBlockSizeBits; tcb_cte_cases x = Some (getF, setF); P (getF tcb); ps_clear (p - x) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> \<exists>tcb. obj' = KOTCB tcb \<and> P (getF tcb)
 2. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); (\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) proof (prove)
goal (3 subgoals):
 1. \<And>s s'' obj' x tcb getF setF. \<lbrakk>Q s; p - x \<le> ptr; ksPSpace s (p - x) = Some (KOTCB tcb); \<forall>z. p - x < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned (p - x) tcbBlockSizeBits; tcb_cte_cases x = Some (getF, setF); P (getF tcb); ps_clear (p - x) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> lookupAround2 ptr (ksPSpace s) = (Some (p - x, KOTCB tcb), snd (lookupAround2 ptr (ksPSpace s)))
 2. \<And>s s'' obj' x tcb getF setF. \<lbrakk>Q s; p - x \<le> ptr; ksPSpace s (p - x) = Some (KOTCB tcb); \<forall>z. p - x < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned (p - x) tcbBlockSizeBits; tcb_cte_cases x = Some (getF, setF); P (getF tcb); ps_clear (p - x) tcbBlockSizeBits s; \<exists>tcb'. (obj', s'') = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)\<rbrakk> \<Longrightarrow> \<exists>tcb. obj' = KOTCB tcb \<and> P (getF tcb)
 3. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); (\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) proof (prove)
goal (2 subgoals):
 1. \<And>s s'' obj' x tcb getF setF. \<lbrakk>Q s; p - x \<le> ptr; ksPSpace s (p - x) = Some (KOTCB tcb); \<forall>z. p - x < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned (p - x) tcbBlockSizeBits; tcb_cte_cases x = Some (getF, setF); P (getF tcb); ps_clear (p - x) tcbBlockSizeBits s; \<exists>tcb'. (obj', s'') = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)\<rbrakk> \<Longrightarrow> \<exists>tcb. obj' = KOTCB tcb \<and> P (getF tcb)
 2. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); (\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); (\<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<or> (\<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)))\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<exists>cte. (if p = a then Some obj' else ksPSpace s p) = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s
 2. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s) proof (prove)
goal (2 subgoals):
 1. \<And>s ba s'' cte. \<lbrakk>Q s; (KOCTE cte, s'') \<in> fst (updateObject v ba ptr p (snd (lookupAround2 ptr (ksPSpace s))) s); p \<le> ptr; ksPSpace s p = Some ba; \<forall>z. p < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned p cte_level_bits; P cte; ps_clear p cteSizeBits s\<rbrakk> \<Longrightarrow> \<exists>cte. ba = KOCTE cte \<and> P cte
 2. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s) proof (prove)
goal (2 subgoals):
 1. \<And>s ba s'' cte. \<lbrakk>Q s; (KOCTE cte, s'') \<in> fst (updateObject v ba ptr p (snd (lookupAround2 ptr (ksPSpace s))) s); p \<le> ptr; ksPSpace s p = Some ba; \<forall>z. p < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned p cte_level_bits; P cte; ps_clear p cteSizeBits s; koTypeOf (KOCTE cte) = koTypeOf ba\<rbrakk> \<Longrightarrow> \<exists>cte. ba = KOCTE cte \<and> P cte
 2. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<exists>n tcb. (if p - n = a then Some obj' else ksPSpace s (p - n)) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj' x. \<lbrakk>Q s; fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<exists>tcb. (if p - x = a then Some obj' else ksPSpace s (p - x)) = Some (KOTCB tcb) \<and> is_aligned (p - x) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases x = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - x) tcbBlockSizeBits (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>tcb. ksPSpace s (p - x) = Some (KOTCB tcb) \<and> is_aligned (p - x) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases x = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - x) tcbBlockSizeBits s) proof (prove)
goal (1 subgoal):
 1. \<And>s ba s'' x tcb getF setF. \<lbrakk>Q s; (KOTCB tcb, s'') \<in> fst (updateObject v ba ptr (p - x) (snd (lookupAround2 ptr (ksPSpace s))) s); p - x \<le> ptr; ksPSpace s (p - x) = Some ba; \<forall>z. p - x < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned (p - x) tcbBlockSizeBits; tcb_cte_cases x = Some (getF, setF); P (getF tcb); ps_clear (p - x) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> \<exists>tcb. ba = KOTCB tcb \<and> P (getF tcb) proof (prove)
goal (1 subgoal):
 1. \<And>s ba s'' x tcb getF setF. \<lbrakk>Q s; (KOTCB tcb, s'') \<in> fst (updateObject v ba ptr (p - x) (snd (lookupAround2 ptr (ksPSpace s))) s); p - x \<le> ptr; ksPSpace s (p - x) = Some ba; \<forall>z. p - x < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned (p - x) tcbBlockSizeBits; tcb_cte_cases x = Some (getF, setF); P (getF tcb); ps_clear (p - x) tcbBlockSizeBits s; koTypeOf (KOTCB tcb) = koTypeOf ba\<rbrakk> \<Longrightarrow> \<exists>tcb. ba = KOTCB tcb \<and> P (getF tcb) proof (prove)
goal (1 subgoal):
 1. \<And>s ba s'' x tcb getF setF x6. \<lbrakk>Q s; (KOTCB tcb, s'') \<in> fst (updateObject v (KOTCB x6) ptr (p - x) (snd (lookupAround2 ptr (ksPSpace s))) s); p - x \<le> ptr; ksPSpace s (p - x) = Some (KOTCB x6); \<forall>z. p - x < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned (p - x) tcbBlockSizeBits; tcb_cte_cases x = Some (getF, setF); P (getF tcb); ps_clear (p - x) tcbBlockSizeBits s; ba = KOTCB x6\<rbrakk> \<Longrightarrow> P (getF x6) proof (prove)
goal (2 subgoals):
 1. \<And>s ba s'' x tcb getF setF x6. \<lbrakk>Q s; p - x \<le> ptr; ksPSpace s (p - x) = Some (KOTCB x6); \<forall>z. p - x < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned (p - x) tcbBlockSizeBits; tcb_cte_cases x = Some (getF, setF); P (getF tcb); ps_clear (p - x) tcbBlockSizeBits s; ba = KOTCB x6\<rbrakk> \<Longrightarrow> lookupAround2 ptr (ksPSpace s) = (Some (p - x, KOTCB x6), snd (lookupAround2 ptr (ksPSpace s)))
 2. \<And>s ba s'' x tcb getF setF x6. \<lbrakk>Q s; p - x \<le> ptr; ksPSpace s (p - x) = Some (KOTCB x6); \<forall>z. p - x < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned (p - x) tcbBlockSizeBits; tcb_cte_cases x = Some (getF, setF); P (getF tcb); ps_clear (p - x) tcbBlockSizeBits s; ba = KOTCB x6; \<exists>tcb'. (KOTCB tcb, s'') = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF x6)\<rbrakk> \<Longrightarrow> P (getF x6) proof (prove)
goal (1 subgoal):
 1. \<And>s ba s'' x tcb getF setF x6. \<lbrakk>Q s; p - x \<le> ptr; ksPSpace s (p - x) = Some (KOTCB x6); \<forall>z. p - x < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; is_aligned (p - x) tcbBlockSizeBits; tcb_cte_cases x = Some (getF, setF); P (getF tcb); ps_clear (p - x) tcbBlockSizeBits s; ba = KOTCB x6; \<exists>tcb'. (KOTCB tcb, s'') = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF x6)\<rbrakk> \<Longrightarrow> P (getF x6) proof (prove)
goal:
No subgoals!