theory SR_lemmas_C

lemma fst_setCTE0:
  notes option.case_cong_weak [cong]
  assumes ct: "cte_at' dest s"
  shows   "\<exists>(v, s') \<in> fst (setCTE dest cte s).
           (s' = s \<lparr> ksPSpace := ksPSpace s' \<rparr>)
           \<and> (dom (ksPSpace s) = dom (ksPSpace s'))
           \<and> (\<forall>x \<in> dom (ksPSpace s).
                case (the (ksPSpace s x)) of
                      KOCTE _ \<Rightarrow> (\<exists>cte. ksPSpace s' x = Some (KOCTE cte))
                    | KOTCB t \<Rightarrow> (\<exists>t'. ksPSpace s' x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t')
                    | _       \<Rightarrow> ksPSpace s' x = ksPSpace s x)" using ct apply - apply (clarsimp simp: setCTE_def setObject_def
    bind_def return_def assert_opt_def gets_def split_beta get_def
    modify_def put_def) apply (erule cte_wp_atE') apply (rule ps_clear_lookupAround2, assumption+) apply simp apply (erule is_aligned_no_overflow) apply (simp (no_asm_simp) del: fun_upd_apply cong: option.case_cong) apply (simp add: return_def updateObject_cte
     bind_def assert_opt_def gets_def split_beta get_def
     modify_def put_def unless_def when_def
     objBits_simps
     cong: bex_cong) apply (rule bexI [where x = "((), s)"]) apply (frule_tac s' = s in in_magnitude_check [where v = "()"]) apply (simp add: cte_level_bits_def) apply assumption apply (simp add: objBits_defs cte_level_bits_def) apply (erule bexI [rotated]) apply (simp  cong: if_cong) apply rule apply (simp split: kernel_object.splits) apply (fastforce simp: tcb_no_ctes_proj_def) apply (simp add: cte_level_bits_def objBits_defs) 
  (* clag *)
   apply (rule ps_clear_lookupAround2, assumption+) apply (erule (1) tcb_cte_cases_in_range1) apply (erule (1) tcb_cte_cases_in_range2) apply (simp add: return_def del: fun_upd_apply cong: bex_cong option.case_cong) apply (subst updateObject_cte_tcb) apply assumption apply (simp add: bind_def return_def assert_opt_def gets_def split_beta get_def when_def
    modify_def put_def unless_def when_def in_alignCheck') apply (simp add: objBits_simps) apply (simp add: magnitudeCheck_def return_def split: option.splits
    cong: bex_cong if_cong) apply (simp split: kernel_object.splits) apply (fastforce simp: tcb_no_ctes_proj_def) apply (simp add: magnitudeCheck_def when_def return_def fail_def
    linorder_not_less
    split: option.splits
    cong: bex_cong if_cong) apply rule apply (simp split: kernel_object.splits) apply (fastforce simp: tcb_no_ctes_proj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>(v, s')\<in>fst (setCTE dest cte s). s' = s\<lparr>ksPSpace := ksPSpace s'\<rparr> \<and> dom (ksPSpace s) = dom (ksPSpace s') \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace s' x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace s' x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace s' x = ksPSpace s x) proof (prove)
using this:
cte_wp_at' (\<lambda>_. True) dest s

goal (1 subgoal):
 1. \<exists>(v, s')\<in>fst (setCTE dest cte s). s' = s\<lparr>ksPSpace := ksPSpace s'\<rparr> \<and> dom (ksPSpace s) = dom (ksPSpace s') \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace s' x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace s' x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace s' x = ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>_. True) dest s \<Longrightarrow> \<exists>(v, s')\<in>fst (setCTE dest cte s). s' = s\<lparr>ksPSpace := ksPSpace s'\<rparr> \<and> dom (ksPSpace s) = dom (ksPSpace s') \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace s' x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace s' x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace s' x = ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>_. True) dest s \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x)
 2. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (4 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; True\<rbrakk> \<Longrightarrow> dest \<le> dest
 2. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; True\<rbrakk> \<Longrightarrow> dest \<le> dest + 2 ^ cte_level_bits - 1
 3. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; True; fst (lookupAround2 dest (ksPSpace s)) = Some (dest, KOCTE ctea); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some a \<Rightarrow> return a) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x)
 4. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; True\<rbrakk> \<Longrightarrow> dest \<le> dest + 2 ^ cte_level_bits - 1
 2. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; True; fst (lookupAround2 dest (ksPSpace s)) = Some (dest, KOCTE ctea); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some a \<Rightarrow> return a) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x)
 3. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; True; fst (lookupAround2 dest (ksPSpace s)) = Some (dest, KOCTE ctea); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some a \<Rightarrow> return a) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x)
 2. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; fst (lookupAround2 dest (ksPSpace s)) = Some (dest, KOCTE ctea); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (return (dest, KOCTE ctea) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x)
 2. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (alignCheck dest cteSizeBits s). \<exists>y\<in>fst (magnitudeCheck dest (snd (lookupAround2 dest (ksPSpace s))) cteSizeBits (snd y)). snd y\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cteb. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOCTE cteb) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = ksPSpace s x)
 2. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (3 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (magnitudeCheck dest (snd (lookupAround2 dest (ksPSpace s))) cteSizeBits (snd ((), s))). snd y\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cteb. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOCTE cteb) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = ksPSpace s x)
 2. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (alignCheck dest cteSizeBits s)
 3. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (5 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> 1 < 2 ^ cte_level_bits
 2. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ksPSpace (?s66 cte) dest = Some (?y66 cte)
 3. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest; (((), s) \<in> fst (magnitudeCheck dest (snd (lookupAround2 dest (ksPSpace (?s66 ctea)))) cte_level_bits (?s66 ctea))) = (s = ?s66 ctea \<and> ps_clear dest cte_level_bits (?s66 ctea))\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (magnitudeCheck dest (snd (lookupAround2 dest (ksPSpace s))) cteSizeBits (snd ((), s))). snd y\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cteb. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOCTE cteb) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = ksPSpace s x)
 4. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (alignCheck dest cteSizeBits s)
 5. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (4 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ksPSpace (?s66 cte) dest = Some (?y66 cte)
 2. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest; (((), s) \<in> fst (magnitudeCheck dest (snd (lookupAround2 dest (ksPSpace (?s66 ctea)))) cte_level_bits (?s66 ctea))) = (s = ?s66 ctea \<and> ps_clear dest cte_level_bits (?s66 ctea))\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (magnitudeCheck dest (snd (lookupAround2 dest (ksPSpace s))) cteSizeBits (snd ((), s))). snd y\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cteb. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOCTE cteb) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = ksPSpace s x)
 3. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (alignCheck dest cteSizeBits s)
 4. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (3 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest; (((), s) \<in> fst (magnitudeCheck dest (snd (lookupAround2 dest (ksPSpace s))) cte_level_bits s)) = (s = s \<and> ps_clear dest cte_level_bits s)\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (magnitudeCheck dest (snd (lookupAround2 dest (ksPSpace s))) cteSizeBits (snd ((), s))). snd y\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cteb. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOCTE cteb) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = ksPSpace s x)
 2. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (alignCheck dest cteSizeBits s)
 3. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (3 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest 4 s; is_aligned dest 4; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest; ((), s) \<in> fst (magnitudeCheck dest (snd (lookupAround2 dest (ksPSpace s))) 4 s)\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (magnitudeCheck dest (snd (lookupAround2 dest (ksPSpace s))) 4 s). snd y\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cteb. ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = Some (KOCTE cteb) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOCTE cte, snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd y))\<rparr>)) x = ksPSpace s x)
 2. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (alignCheck dest cteSizeBits s)
 3. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (3 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest 4 s; is_aligned dest 4; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> snd ((), s)\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(dest \<mapsto> KOCTE cte)\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOCTE cte, snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd ((), s)))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cteb. ksPSpace (snd ((), snd (KOCTE cte, snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd ((), s)))\<rparr>)) x = Some (KOCTE cteb) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOCTE cte, snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd ((), s)))\<rparr>)) x = ksPSpace s x)
 2. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (alignCheck dest cteSizeBits s)
 3. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (3 subgoals):
 1. \<And>ctea. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest 4 s; is_aligned dest 4; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOCTE cte, snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd ((), s)))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cteb. ksPSpace (snd ((), snd (KOCTE cte, snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd ((), s)))\<rparr>)) x = Some (KOCTE cteb) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOCTE cte, snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd ((), s)))\<rparr>)) x = ksPSpace s x
 2. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (alignCheck dest cteSizeBits s)
 3. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (3 subgoals):
 1. \<And>ctea x. \<lbrakk>ksPSpace s dest = Some (KOCTE ctea); ps_clear dest 4 s; is_aligned dest 4; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest; x \<in> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOCTE cte, snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd ((), s)))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cteb. ksPSpace (snd ((), snd (KOCTE cte, snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd ((), s)))\<rparr>)) x = Some (KOCTE cteb) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOCTE cte, snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((dest, KOCTE ctea), s)) \<mapsto> fst (KOCTE cte, snd ((), s)))\<rparr>)) x = ksPSpace s x
 2. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (alignCheck dest cteSizeBits s)
 3. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (3 subgoals):
 1. \<And>cte x. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest 4 s; is_aligned dest 4; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest; x \<in> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> x \<noteq> dest \<longrightarrow> (\<forall>x6. the (ksPSpace s x) = KOTCB x6 \<longrightarrow> (\<exists>t'. ksPSpace s x = Some (KOTCB t') \<and> tcb_no_ctes_proj x6 = tcb_no_ctes_proj t')) \<and> ((\<exists>x7. the (ksPSpace s x) = KOCTE x7) \<longrightarrow> (\<exists>cte. ksPSpace s x = Some (KOCTE cte)))
 2. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (alignCheck dest cteSizeBits s)
 3. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s dest = Some (KOCTE cte); ps_clear dest cte_level_bits s; is_aligned dest cte_level_bits; case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ cte_level_bits \<le> x - dest\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (alignCheck dest cteSizeBits s)
 2. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (3 subgoals):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> ptr' \<le> dest
 2. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> dest \<le> ptr' + 2 ^ tcbBlockSizeBits - 1
 3. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True; fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - ptr'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some a \<Rightarrow> return a) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True\<rbrakk> \<Longrightarrow> dest \<le> ptr' + 2 ^ tcbBlockSizeBits - 1
 2. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True; fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - ptr'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some a \<Rightarrow> return a) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); True; fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - ptr'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((case fst (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> fail | Some a \<Rightarrow> return a) s). \<exists>ya\<in>fst (updateObject cte (snd (fst y)) dest (fst (fst y)) (snd (lookupAround2 dest (ksPSpace s))) (snd y)). snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr> \<and> dom (ksPSpace s) = insert (fst (fst y)) (dom (ksPSpace s)) \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd ya\<lparr>ksPSpace := (ksPSpace s)(fst (fst y) \<mapsto> fst ya)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - ptr'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (updateObject cte (KOTCB tcb) dest ptr' (snd (lookupAround2 dest (ksPSpace s))) s). snd y\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> fst y)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> fst y)\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd y\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst y)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd y\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst y)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd y\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst y)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - ptr'\<rbrakk> \<Longrightarrow> tcb_cte_cases (dest - ptr') = Some (?accF101 tcb ptr' getF setF, ?updF101 tcb ptr' getF setF)
 2. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - ptr'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' (snd (lookupAround2 dest (ksPSpace s))) (objBits tcb);
return (KOTCB (?updF101 tcb ptr' getF setF (\<lambda>_. cte) tcb))
od) s). snd y\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> fst y)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> fst y)\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd y\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst y)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd y\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst y)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd y\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst y)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - ptr'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst ((do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' (snd (lookupAround2 dest (ksPSpace s))) (objBits tcb);
return (KOTCB (setF (\<lambda>_. cte) tcb))
od) s). snd y\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> fst y)\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> fst y)\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd y\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst y)\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>cte. ksPSpace (snd ((), snd y\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst y)\<rparr>)) x = Some (KOCTE cte) | _ \<Rightarrow> ksPSpace (snd ((), snd y\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst y)\<rparr>)) x = ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - ptr'\<rbrakk> \<Longrightarrow> is_aligned ptr' (objBits tcb) \<and> (is_aligned ptr' (objBits tcb) \<longrightarrow> (\<exists>y\<in>fst (magnitudeCheck ptr' (snd (lookupAround2 dest (ksPSpace s))) (objBits tcb) s). snd y\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOTCB (setF (\<lambda>_. cte) tcb))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOTCB (setF (\<lambda>_. cte) tcb))\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>ctea. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = Some (KOCTE ctea) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = ksPSpace s x))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); case snd (lookupAround2 dest (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - ptr'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (magnitudeCheck ptr' (snd (lookupAround2 dest (ksPSpace s))) tcbBlockSizeBits s). snd y\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOTCB (setF (\<lambda>_. cte) tcb))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOTCB (setF (\<lambda>_. cte) tcb))\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>ctea. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = Some (KOCTE ctea) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); snd (lookupAround2 dest (ksPSpace s)) = None\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s)))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>ctea. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s)))\<rparr>)) x = Some (KOCTE ctea) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s)))\<rparr>)) x = ksPSpace s x
 2. \<And>tcb ptr' getF setF x2. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); snd (lookupAround2 dest (ksPSpace s)) = Some x2; 2 ^ tcbBlockSizeBits \<le> x2 - ptr'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (when (x2 - ptr' < 2 ^ tcbBlockSizeBits) fail s). snd y\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOTCB (setF (\<lambda>_. cte) tcb))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOTCB (setF (\<lambda>_. cte) tcb))\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>ctea. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = Some (KOCTE ctea) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>tcb ptr' getF setF. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); snd (lookupAround2 dest (ksPSpace s)) = None\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (ksPSpace s). x \<noteq> ptr' \<longrightarrow> (\<forall>x6. the (ksPSpace s x) = KOTCB x6 \<longrightarrow> (\<exists>t'. ksPSpace s x = Some (KOTCB t') \<and> tcb_no_ctes_proj x6 = tcb_no_ctes_proj t')) \<and> ((\<exists>x7. the (ksPSpace s x) = KOCTE x7) \<longrightarrow> (\<exists>cte. ksPSpace s x = Some (KOCTE cte)))
 2. \<And>tcb ptr' getF setF x2. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); snd (lookupAround2 dest (ksPSpace s)) = Some x2; 2 ^ tcbBlockSizeBits \<le> x2 - ptr'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (when (x2 - ptr' < 2 ^ tcbBlockSizeBits) fail s). snd y\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOTCB (setF (\<lambda>_. cte) tcb))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOTCB (setF (\<lambda>_. cte) tcb))\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>ctea. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = Some (KOCTE ctea) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF x2. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); snd (lookupAround2 dest (ksPSpace s)) = Some x2; 2 ^ tcbBlockSizeBits \<le> x2 - ptr'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (when (x2 - ptr' < 2 ^ tcbBlockSizeBits) fail s). snd y\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOTCB (setF (\<lambda>_. cte) tcb))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOTCB (setF (\<lambda>_. cte) tcb))\<rparr> \<and> (\<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>ctea. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = Some (KOCTE ctea) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd y)\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd y))\<rparr>)) x = ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF x2. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); snd (lookupAround2 dest (ksPSpace s)) = Some x2; 2 ^ tcbBlockSizeBits \<le> x2 - ptr'\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (ksPSpace s). case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s)))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>ctea. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s)))\<rparr>)) x = Some (KOCTE ctea) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s)))\<rparr>)) x = ksPSpace s x proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF x2 x. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); snd (lookupAround2 dest (ksPSpace s)) = Some x2; 2 ^ tcbBlockSizeBits \<le> x2 - ptr'; x \<in> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> case the (ksPSpace s x) of KOTCB t \<Rightarrow> \<exists>t'. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s)))\<rparr>)) x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t' | KOCTE xa \<Rightarrow> \<exists>ctea. ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s)))\<rparr>)) x = Some (KOCTE ctea) | _ \<Rightarrow> ksPSpace (snd ((), snd (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s))\<lparr>ksPSpace := (ksPSpace s)(fst (fst ((ptr', KOTCB tcb), s)) \<mapsto> fst (KOTCB (setF (\<lambda>_. cte) tcb), snd ((), s)))\<rparr>)) x = ksPSpace s x proof (prove)
goal (1 subgoal):
 1. \<And>tcb ptr' getF setF x2 x. \<lbrakk>ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; tcb_cte_cases (dest - ptr') = Some (getF, setF); fst (lookupAround2 dest (ksPSpace s)) = Some (ptr', KOTCB tcb); snd (lookupAround2 dest (ksPSpace s)) = Some x2; 2 ^ tcbBlockSizeBits \<le> x2 - ptr'; x \<in> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> x \<noteq> ptr' \<longrightarrow> (\<forall>x6. the (ksPSpace s x) = KOTCB x6 \<longrightarrow> (\<exists>t'. ksPSpace s x = Some (KOTCB t') \<and> tcb_no_ctes_proj x6 = tcb_no_ctes_proj t')) \<and> ((\<exists>x7. the (ksPSpace s x) = KOCTE x7) \<longrightarrow> (\<exists>cte. ksPSpace s x = Some (KOCTE cte))) proof (prove)
goal:
No subgoals!