theory ADT_C

lemma map_to_ctes_tcb_ctes:
  notes if_cong[cong]
  shows
  "ctes_of s' = ctes_of s \<Longrightarrow>
   ko_at' tcb p s \<Longrightarrow> ko_at' tcb' p s' \<Longrightarrow>
   \<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb" apply (clarsimp simp add: ran_tcb_cte_cases) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKO_opt_tcb
                 split: kernel_object.splits) apply (case_tac ko, simp_all, clarsimp) apply (clarsimp simp: objBits_type[of "KOTCB tcb" "KOTCB undefined"]
                        objBits_type[of "KOTCB tcb'" "KOTCB undefined"]) apply (rule conjI) apply (drule ps_clear_def3[THEN iffD1,rotated 2],
          assumption, simp add: objBits_simps')+ apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff) apply (drule_tac x=p in spec, simp) apply (rule conjI) apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff) apply (drule_tac x="p+0x10" in spec, simp add: objBitsKO_def) apply (frule_tac s1=s in ps_clear_def3[THEN iffD1,rotated 2],
          assumption, simp add: objBits_simps') apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
          assumption, simp add: objBits_simps') apply (drule (1) ps_clear_16)+ apply (simp add: is_aligned_add_helper[of _ 9 "0x10", simplified]
                    split_def objBits_simps') apply (rule conjI) apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff) apply (drule_tac x="p+0x20" in spec, simp add: objBitsKO_def) apply (frule_tac s1=s in ps_clear_def3[THEN iffD1,rotated 2],
          assumption, simp add: objBits_simps') apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
          assumption, simp add: objBits_simps') apply (drule (1) ps_clear_is_aligned_ctes_None(1))+ apply (simp add: is_aligned_add_helper[of _ 9 "0x20", simplified]
                    split_def objBits_simps') apply (rule conjI) apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff) apply (drule_tac x="p+0x30" in spec, simp add: objBitsKO_def) apply (frule_tac s1=s in ps_clear_def3[THEN iffD1,rotated 2],
          assumption, simp add: objBits_simps') apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
          assumption, simp add: objBits_simps') apply (drule (1) ps_clear_is_aligned_ctes_None(2))+ apply (simp add: is_aligned_add_helper[of _ 9 "0x30", simplified]
                    split_def objBits_simps') apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff) apply (drule_tac x="p+0x40" in spec, simp add: objBitsKO_def) apply (frule_tac s1=s in ps_clear_def3[THEN iffD1,rotated 2],
         assumption, simp add: objBits_simps') apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2],
         assumption, simp add: objBits_simps') apply (drule (1) ps_clear_is_aligned_ctes_None(3))+ apply (simp add: is_aligned_add_helper[of _ 9 "0x40", simplified]
                   split_def objBits_simps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s' = ctes_of s; ko_at' tcb p s; ko_at' tcb' p s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s' = ctes_of s; ko_at' tcb p s; ko_at' tcb' p s'\<rbrakk> \<Longrightarrow> tcb.tcbCTable tcb' = tcb.tcbCTable tcb \<and> tcb.tcbVTable tcb' = tcb.tcbVTable tcb \<and> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>ps_clear p (objBitsKO (KOTCB tcb')) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB tcb')); \<forall>x1. ko \<noteq> KOEndpoint x1; \<forall>x2. ko \<noteq> KONotification x2; ko \<noteq> KOKernelData; ko \<noteq> KOUserData; ko \<noteq> KOUserDataDevice; \<forall>x6. ko = KOTCB x6 \<longrightarrow> x6 = tcb \<and> is_aligned p (objBitsKO (KOTCB x6)) \<and> ksPSpace s p = Some (KOTCB x6) \<and> ps_clear p (objBitsKO (KOTCB x6)) s; \<forall>x7. ko \<noteq> KOCTE x7; \<forall>x8. ko \<noteq> KOArch x8\<rbrakk> \<Longrightarrow> tcb.tcbCTable tcb' = tcb.tcbCTable tcb \<and> tcb.tcbVTable tcb' = tcb.tcbVTable tcb \<and> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB tcb')) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB tcb')); is_aligned p (objBitsKO (KOTCB tcb)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB tcb)) s\<rbrakk> \<Longrightarrow> tcb.tcbCTable tcb' = tcb.tcbCTable tcb \<and> tcb.tcbVTable tcb' = tcb.tcbVTable tcb \<and> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCTable tcb' = tcb.tcbCTable tcb \<and> tcb.tcbVTable tcb' = tcb.tcbVTable tcb \<and> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCTable tcb' = tcb.tcbCTable tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbVTable tcb' = tcb.tcbVTable tcb \<and> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); {p + 1..p + (1 << objBitsKO (KOTCB undefined)) - 1} \<inter> dom (ksPSpace s') = {}; {p + 1..p + (1 << objBitsKO (KOTCB undefined)) - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> tcb.tcbCTable tcb' = tcb.tcbCTable tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbVTable tcb' = tcb.tcbVTable tcb \<and> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x. (if (\<exists>cte. ksPSpace s' x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' x of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None); ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); {p + 1..p + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s') = {}; {p + 1..p + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> tcb.tcbCTable tcb' = tcb.tcbCTable tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbVTable tcb' = tcb.tcbVTable tcb \<and> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbVTable tcb' = tcb.tcbVTable tcb \<and> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbVTable tcb' = tcb.tcbVTable tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; \<forall>x. (if (\<exists>cte. ksPSpace s' x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' x of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None); ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbVTable tcb' = tcb.tcbVTable tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x10) = Some (KOCTE cte)) \<and> is_aligned (p + 0x10) cteSizeBits \<and> {0x11 + p..0xF + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x10) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x10 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x10 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x10 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x10 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x10 - (p + 0x10 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x10) = Some (KOCTE cte)) \<and> is_aligned (p + 0x10) cteSizeBits \<and> {0x11 + p..0xF + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x10) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x10 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x10 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x10 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x10 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x10 - (p + 0x10 && ~~ mask (objBitsKO (KOTCB undefined))))) else None)\<rbrakk> \<Longrightarrow> tcb.tcbVTable tcb' = tcb.tcbVTable tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x10) = Some (KOCTE cte)) \<and> is_aligned (p + 0x10) cteSizeBits \<and> {0x11 + p..0xF + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x10) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x10 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x10 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x10 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x10 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x10 - (p + 0x10 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x10) = Some (KOCTE cte)) \<and> is_aligned (p + 0x10) cteSizeBits \<and> {0x11 + p..0xF + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x10) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x10 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x10 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x10 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x10 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x10 - (p + 0x10 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> tcb.tcbVTable tcb' = tcb.tcbVTable tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x10) = Some (KOCTE cte)) \<and> is_aligned (p + 0x10) cteSizeBits \<and> {0x11 + p..0xF + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x10) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x10 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x10 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x10 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x10 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x10 - (p + 0x10 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x10) = Some (KOCTE cte)) \<and> is_aligned (p + 0x10) cteSizeBits \<and> {0x11 + p..0xF + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x10) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x10 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x10 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x10 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x10 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x10 - (p + 0x10 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}; {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s') = {}\<rbrakk> \<Longrightarrow> tcb.tcbVTable tcb' = tcb.tcbVTable tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); (if (\<exists>cte. ksPSpace s' (p + 0x10) = Some (KOCTE cte)) \<and> is_aligned (p + 0x10) cteSizeBits \<and> {0x11 + p..0xF + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x10) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x10 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x10 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x10 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x10 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x10 - (p + 0x10 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x10) = Some (KOCTE cte)) \<and> is_aligned (p + 0x10) cteSizeBits \<and> {0x11 + p..0xF + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x10) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x10 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x10 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x10 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x10 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x10 - (p + 0x10 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}; {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s') = {}; ksPSpace s' (p + 2 ^ cteSizeBits) = None; ksPSpace s (p + 2 ^ cteSizeBits) = None\<rbrakk> \<Longrightarrow> tcb.tcbVTable tcb' = tcb.tcbVTable tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb \<and> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; \<forall>x. (if (\<exists>cte. ksPSpace s' x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' x of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None); ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x20) = Some (KOCTE cte)) \<and> is_aligned (p + 0x20) cteSizeBits \<and> {0x21 + p..0x1F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x20) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x20 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x20 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x20 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x20 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x20 - (p + 0x20 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x20) = Some (KOCTE cte)) \<and> is_aligned (p + 0x20) cteSizeBits \<and> {0x21 + p..0x1F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x20) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x20 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x20 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x20 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x20 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x20 - (p + 0x20 && ~~ mask (objBitsKO (KOTCB undefined))))) else None)\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x20) = Some (KOCTE cte)) \<and> is_aligned (p + 0x20) cteSizeBits \<and> {0x21 + p..0x1F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x20) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x20 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x20 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x20 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x20 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x20 - (p + 0x20 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x20) = Some (KOCTE cte)) \<and> is_aligned (p + 0x20) cteSizeBits \<and> {0x21 + p..0x1F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x20) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x20 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x20 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x20 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x20 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x20 - (p + 0x20 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x20) = Some (KOCTE cte)) \<and> is_aligned (p + 0x20) cteSizeBits \<and> {0x21 + p..0x1F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x20) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x20 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x20 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x20 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x20 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x20 - (p + 0x20 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x20) = Some (KOCTE cte)) \<and> is_aligned (p + 0x20) cteSizeBits \<and> {0x21 + p..0x1F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x20) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x20 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x20 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x20 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x20 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x20 - (p + 0x20 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}; {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s') = {}\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); (if (\<exists>cte. ksPSpace s' (p + 0x20) = Some (KOCTE cte)) \<and> is_aligned (p + 0x20) cteSizeBits \<and> {0x21 + p..0x1F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x20) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x20 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x20 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x20 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x20 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x20 - (p + 0x20 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x20) = Some (KOCTE cte)) \<and> is_aligned (p + 0x20) cteSizeBits \<and> {0x21 + p..0x1F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x20) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x20 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x20 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x20 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x20 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x20 - (p + 0x20 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}; {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s') = {}; ksPSpace s' (p + 2 * 2 ^ cteSizeBits) = None; ksPSpace s (p + 2 * 2 ^ cteSizeBits) = None\<rbrakk> \<Longrightarrow> tcb.tcbReply tcb' = tcb.tcbReply tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb \<and> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; \<forall>x. (if (\<exists>cte. ksPSpace s' x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' x of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None); ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x30) = Some (KOCTE cte)) \<and> is_aligned (p + 0x30) cteSizeBits \<and> {0x31 + p..0x2F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x30) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x30 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x30 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x30 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x30 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x30 - (p + 0x30 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x30) = Some (KOCTE cte)) \<and> is_aligned (p + 0x30) cteSizeBits \<and> {0x31 + p..0x2F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x30) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x30 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x30 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x30 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x30 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x30 - (p + 0x30 && ~~ mask (objBitsKO (KOTCB undefined))))) else None)\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x30) = Some (KOCTE cte)) \<and> is_aligned (p + 0x30) cteSizeBits \<and> {0x31 + p..0x2F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x30) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x30 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x30 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x30 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x30 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x30 - (p + 0x30 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x30) = Some (KOCTE cte)) \<and> is_aligned (p + 0x30) cteSizeBits \<and> {0x31 + p..0x2F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x30) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x30 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x30 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x30 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x30 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x30 - (p + 0x30 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x30) = Some (KOCTE cte)) \<and> is_aligned (p + 0x30) cteSizeBits \<and> {0x31 + p..0x2F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x30) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x30 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x30 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x30 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x30 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x30 - (p + 0x30 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x30) = Some (KOCTE cte)) \<and> is_aligned (p + 0x30) cteSizeBits \<and> {0x31 + p..0x2F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x30) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x30 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x30 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x30 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x30 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x30 - (p + 0x30 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}; {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s') = {}\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); (if (\<exists>cte. ksPSpace s' (p + 0x30) = Some (KOCTE cte)) \<and> is_aligned (p + 0x30) cteSizeBits \<and> {0x31 + p..0x2F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x30) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x30 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x30 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x30 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x30 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x30 - (p + 0x30 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x30) = Some (KOCTE cte)) \<and> is_aligned (p + 0x30) cteSizeBits \<and> {0x31 + p..0x2F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x30) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x30 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x30 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x30 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x30 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x30 - (p + 0x30 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}; {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s') = {}; ksPSpace s' (p + 3 * 2 ^ cteSizeBits) = None; ksPSpace s (p + 3 * 2 ^ cteSizeBits) = None\<rbrakk> \<Longrightarrow> tcb.tcbCaller tcb' = tcb.tcbCaller tcb
 2. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; ctes_of s' = ctes_of s; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p (objBitsKO (KOTCB undefined)) s'; \<forall>x. (if (\<exists>cte. ksPSpace s' x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' x of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s x = Some (KOCTE cte)) \<and> is_aligned x (objBitsKO (KOCTE undefined)) \<and> {x + 1..x + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s x of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb)) \<and> {(x && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(x && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (x && ~~ mask (objBitsKO (KOTCB undefined))) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - (x && ~~ mask (objBitsKO (KOTCB undefined))))) else None); ksPSpace s' p = Some (KOTCB tcb'); is_aligned p (objBitsKO (KOTCB undefined)); ksPSpace s p = Some (KOTCB tcb); ps_clear p (objBitsKO (KOTCB undefined)) s\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x40) = Some (KOCTE cte)) \<and> is_aligned (p + 0x40) cteSizeBits \<and> {0x41 + p..0x3F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x40) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x40 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x40 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x40 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x40 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x40 - (p + 0x40 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x40) = Some (KOCTE cte)) \<and> is_aligned (p + 0x40) cteSizeBits \<and> {0x41 + p..0x3F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x40) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x40 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x40 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x40 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x40 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x40 - (p + 0x40 && ~~ mask (objBitsKO (KOTCB undefined))))) else None)\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x40) = Some (KOCTE cte)) \<and> is_aligned (p + 0x40) cteSizeBits \<and> {0x41 + p..0x3F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x40) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x40 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x40 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x40 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x40 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x40 - (p + 0x40 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x40) = Some (KOCTE cte)) \<and> is_aligned (p + 0x40) cteSizeBits \<and> {0x41 + p..0x3F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x40) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x40 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x40 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x40 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x40 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x40 - (p + 0x40 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s'; ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); ps_clear p tcbBlockSizeBits s; (if (\<exists>cte. ksPSpace s' (p + 0x40) = Some (KOCTE cte)) \<and> is_aligned (p + 0x40) cteSizeBits \<and> {0x41 + p..0x3F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x40) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x40 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x40 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x40 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x40 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x40 - (p + 0x40 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x40) = Some (KOCTE cte)) \<and> is_aligned (p + 0x40) cteSizeBits \<and> {0x41 + p..0x3F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x40) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x40 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x40 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x40 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x40 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x40 - (p + 0x40 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}; {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s') = {}\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s' p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ksPSpace s p = Some (KOTCB tcb); (if (\<exists>cte. ksPSpace s' (p + 0x40) = Some (KOCTE cte)) \<and> is_aligned (p + 0x40) cteSizeBits \<and> {0x41 + p..0x3F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x40) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s' (p + 0x40 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x40 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x40 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s') = {} then case ksPSpace s' (p + 0x40 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x40 - (p + 0x40 && ~~ mask (objBitsKO (KOTCB undefined))))) else None) = (if (\<exists>cte. ksPSpace s (p + 0x40) = Some (KOCTE cte)) \<and> is_aligned (p + 0x40) cteSizeBits \<and> {0x41 + p..0x3F + (p + 2 ^ cteSizeBits)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x40) of Some (KOCTE xa) \<Rightarrow> Some xa else if (\<exists>tcb. ksPSpace s (p + 0x40 && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb)) \<and> {(p + 0x40 && ~~ mask tcbBlockSizeBits) + 1..(p + 0x40 && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p + 0x40 && ~~ mask tcbBlockSizeBits) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p + 0x40 - (p + 0x40 && ~~ mask (objBitsKO (KOTCB undefined))))) else None); {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s) = {}; {p + 1..p + (1 << tcbBlockSizeBits) - 1} \<inter> dom (ksPSpace s') = {}; ksPSpace s' (p + 4 * 2 ^ cteSizeBits) = None; ksPSpace s (p + 4 * 2 ^ cteSizeBits) = None\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb' = tcbIPCBufferFrame tcb proof (prove)
goal:
No subgoals!