theory Fastpath_Equiv

lemma set_setCTE[unfolded K_bind_def]:
  "do setCTE p val; setCTE p val' od = setCTE p val'" supply if_split[split del] apply simp apply (rule monadic_rewrite_to_eq) apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_trans,
          rule_tac f="real_cte_at' p" in monadic_rewrite_add_gets) apply (rule monadic_rewrite_transverse, rule monadic_rewrite_add_gets,
          rule monadic_rewrite_bind_tail) apply (rule monadic_rewrite_trans,
           rule_tac f="tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)"
                  in monadic_rewrite_add_gets) apply (rule monadic_rewrite_transverse, rule monadic_rewrite_add_gets,
           rule monadic_rewrite_bind_tail) apply (rename_tac cteat tcbat) apply (rule monadic_rewrite_trans) apply (rule monadic_rewrite_bind_tail) apply (simp add: setCTE_assert_modify) apply (rule monadic_rewrite_trans, rule_tac rv=cteat in monadic_rewrite_gets_known) apply (rule_tac rv=tcbat in monadic_rewrite_gets_known) apply (wp setCTE_typ_at'[where T="koType TYPE(tcb)", unfolded typ_at_to_obj_at']
                setCTE_typ_at'[where T="koType TYPE(cte)", unfolded typ_at_to_obj_at']
                  | simp)+ apply (simp add: setCTE_assert_modify bind_assoc) apply (rule monadic_rewrite_bind_tail)+ apply (rule_tac P="c = cteat \<and> t = tcbat
                           \<and> (tcbat \<longrightarrow>
                                 (\<exists> getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF)
                                        \<and> (\<forall> f g tcb. setF f (setF g tcb) = setF (f o g) tcb)))"
                   in monadic_rewrite_gen_asm) apply (rule monadic_rewrite_is_refl[OF ext]) apply (simp add: exec_modify split: if_split) apply (auto simp: simpler_modify_def projectKO_opt_tcb objBits_defs
                    del: ext
                 intro!: kernel_state.fold_congs ext
                  split: if_split)[1] apply wp+ apply (clarsimp simp: objBits_defs intro!: all_tcbI) apply (auto simp: tcb_cte_cases_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do setCTE p val;
setCTE p val'
od = setCTE p val' proof (prove)
goal (1 subgoal):
 1. do setCTE p val;
setCTE p val'
od = setCTE p val' proof (prove)
goal (1 subgoal):
 1. do y <- setCTE p val;
setCTE p val'
od = setCTE p val' proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False True (\<lambda>_. True) (do y <- setCTE p val;
setCTE p val'
od) (setCTE p val') proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False True ?Q2 (do y <- setCTE p val;
setCTE p val'
od) (setCTE p val')
 2. \<And>s. True \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False True ?Q5 (do _ <- gets (real_cte_at' p);
y <- setCTE p val;
setCTE p val'
od) (setCTE p val')
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s proof (prove)
goal (3 subgoals):
 1. \<And>uu_. monadic_rewrite False True (?Q13 uu_) (do y <- setCTE p val;
setCTE p val'
od) (setCTE p val')
 2. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>?Q13\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (3 subgoals):
 1. \<And>uu_. monadic_rewrite False True (?Q16 uu_) (do _ <- gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases));
y <- setCTE p val;
setCTE p val'
od) (setCTE p val')
 2. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q16 uu_\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (4 subgoals):
 1. \<And>uu_ uua_. monadic_rewrite False True (?Q24 uu_ uua_) (do y <- setCTE p val;
setCTE p val'
od) (setCTE p val')
 2. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>?Q24 uu_\<rbrace>
 3. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (4 subgoals):
 1. \<And>cteat tcbat. monadic_rewrite False True (?Q24 cteat tcbat) (do y <- setCTE p val;
setCTE p val'
od) (setCTE p val')
 2. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>?Q24 uu_\<rbrace>
 3. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (5 subgoals):
 1. \<And>cteat tcbat. monadic_rewrite False True (?P27 cteat tcbat) (do y <- setCTE p val;
setCTE p val'
od) (?g27 cteat tcbat)
 2. \<And>cteat tcbat. monadic_rewrite False True (?Q27 cteat tcbat) (?g27 cteat tcbat) (setCTE p val')
 3. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. ?P27 uu_ tcbat and ?Q27 uu_ tcbat\<rbrace>
 4. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (6 subgoals):
 1. \<And>cteat tcbat y. monadic_rewrite False True (?Q30 cteat tcbat y) (setCTE p val') (?j30 cteat tcbat y)
 2. \<And>cteat tcbat. \<lbrace>?P27 cteat tcbat\<rbrace> setCTE p val \<lbrace>?Q30 cteat tcbat\<rbrace>
 3. \<And>cteat tcbat. monadic_rewrite False True (?Q27 cteat tcbat) (setCTE p val >>= ?j30 cteat tcbat) (setCTE p val')
 4. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. ?P27 uu_ tcbat and ?Q27 uu_ tcbat\<rbrace>
 5. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (6 subgoals):
 1. \<And>cteat tcbat. monadic_rewrite False True (?Q30 cteat tcbat ()) (do c <- gets (real_cte_at' p);
t <- gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val'))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail
od) (?j30 cteat tcbat ())
 2. \<And>cteat tcbat. \<lbrace>?P27 cteat tcbat\<rbrace> setCTE p val \<lbrace>?Q30 cteat tcbat\<rbrace>
 3. \<And>cteat tcbat. monadic_rewrite False True (?Q27 cteat tcbat) (setCTE p val >>= ?j30 cteat tcbat) (setCTE p val')
 4. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. ?P27 uu_ tcbat and ?Q27 uu_ tcbat\<rbrace>
 5. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (6 subgoals):
 1. \<And>cteat tcbat. monadic_rewrite False True (?Q40 cteat tcbat ()) (do t <- gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
if cteat then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val'))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail
od) (?j30 cteat tcbat ())
 2. \<And>cteat tcbat. \<lbrace>?P27 cteat tcbat\<rbrace> setCTE p val \<lbrace>\<lambda>a. (\<lambda>a. real_cte_at' p a = cteat) and ?Q40 cteat tcbat a\<rbrace>
 3. \<And>cteat tcbat. monadic_rewrite False True (?Q27 cteat tcbat) (setCTE p val >>= ?j30 cteat tcbat) (setCTE p val')
 4. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. ?P27 uu_ tcbat and ?Q27 uu_ tcbat\<rbrace>
 5. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (5 subgoals):
 1. \<And>cteat tcbat. \<lbrace>?P27 cteat tcbat\<rbrace> setCTE p val \<lbrace>\<lambda>a. (\<lambda>a. real_cte_at' p a = cteat) and (\<lambda>a. (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) a = tcbat)\<rbrace>
 2. \<And>cteat tcbat. monadic_rewrite False True (?Q27 cteat tcbat) (do x <- setCTE p val;
if cteat then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val'))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail
od) (setCTE p val')
 3. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. ?P27 uu_ tcbat and ?Q27 uu_ tcbat\<rbrace>
 4. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (4 subgoals):
 1. \<And>cteat tcbat. monadic_rewrite False True (?Q27 cteat tcbat) (do x <- setCTE p val;
if cteat then modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOCTE val') else ps a)) else if tcbat then modify (ksPSpace_update (\<lambda>ps a. if a = p && ~~ mask tcbBlockSizeBits then Some (KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))) else ps a)) else fail
od) (setCTE p val')
 2. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' p s = uu_ \<and> (tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and ?Q27 uu_ tcbat\<rbrace>
 3. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (4 subgoals):
 1. \<And>cteat tcbat. monadic_rewrite False True (?Q27 cteat tcbat) (do c <- gets (real_cte_at' p);
t <- gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
x <- if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail;
if cteat then modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOCTE val') else ps a)) else if tcbat then modify (ksPSpace_update (\<lambda>ps a. if a = p && ~~ mask tcbBlockSizeBits then Some (KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))) else ps a)) else fail
od) (do c <- gets (real_cte_at' p);
t <- gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val'))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail
od)
 2. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' p s = uu_ \<and> (tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and ?Q27 uu_ tcbat\<rbrace>
 3. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (6 subgoals):
 1. \<And>cteat tcbat c t. monadic_rewrite False True (?Q66 cteat tcbat c t) (do x <- if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail;
if cteat then modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOCTE val') else ps a)) else if tcbat then modify (ksPSpace_update (\<lambda>ps a. if a = p && ~~ mask tcbBlockSizeBits then Some (KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))) else ps a)) else fail
od) (if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val'))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail)
 2. \<And>cteat tcbat c. \<lbrace>?Q63 cteat tcbat c\<rbrace> gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>?Q66 cteat tcbat c\<rbrace>
 3. \<And>cteat tcbat. \<lbrace>?Q27 cteat tcbat\<rbrace> gets (real_cte_at' p) \<lbrace>?Q63 cteat tcbat\<rbrace>
 4. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' p s = uu_ \<and> (tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and ?Q27 uu_ tcbat\<rbrace>
 5. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (6 subgoals):
 1. \<And>cteat tcbat c t. c = cteat \<and> t = tcbat \<and> (tcbat \<longrightarrow> (\<exists>getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF) \<and> (\<forall>f g tcb. setF f (setF g tcb) = setF (f \<circ> g) tcb))) \<Longrightarrow> monadic_rewrite False True (?Q69 cteat tcbat c t) (do x <- if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail;
if cteat then modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOCTE val') else ps a)) else if tcbat then modify (ksPSpace_update (\<lambda>ps a. if a = p && ~~ mask tcbBlockSizeBits then Some (KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))) else ps a)) else fail
od) (if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val'))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail)
 2. \<And>cteat tcbat c. \<lbrace>?Q63 cteat tcbat c\<rbrace> gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>t. (\<lambda>_. c = cteat \<and> t = tcbat \<and> (tcbat \<longrightarrow> (\<exists>getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF) \<and> (\<forall>f g tcb. setF f (setF g tcb) = setF (f \<circ> g) tcb)))) and ?Q69 cteat tcbat c t\<rbrace>
 3. \<And>cteat tcbat. \<lbrace>?Q27 cteat tcbat\<rbrace> gets (real_cte_at' p) \<lbrace>?Q63 cteat tcbat\<rbrace>
 4. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' p s = uu_ \<and> (tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and ?Q27 uu_ tcbat\<rbrace>
 5. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (6 subgoals):
 1. \<And>cteat tcbat c t x. c = cteat \<and> t = tcbat \<and> (tcbat \<longrightarrow> (\<exists>getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF) \<and> (\<forall>f g tcb. setF f (setF g tcb) = setF (f \<circ> g) tcb))) \<Longrightarrow> (do x <- if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail;
if cteat then modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOCTE val') else ps a)) else if tcbat then modify (ksPSpace_update (\<lambda>ps a. if a = p && ~~ mask tcbBlockSizeBits then Some (KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))) else ps a)) else fail
od) x = (if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val'))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail) x
 2. \<And>cteat tcbat c. \<lbrace>?Q63 cteat tcbat c\<rbrace> gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>t. (\<lambda>_. c = cteat \<and> t = tcbat \<and> (tcbat \<longrightarrow> (\<exists>getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF) \<and> (\<forall>f g tcb. setF f (setF g tcb) = setF (f \<circ> g) tcb)))) and (\<lambda>_. True)\<rbrace>
 3. \<And>cteat tcbat. \<lbrace>?Q27 cteat tcbat\<rbrace> gets (real_cte_at' p) \<lbrace>?Q63 cteat tcbat\<rbrace>
 4. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' p s = uu_ \<and> (tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and ?Q27 uu_ tcbat\<rbrace>
 5. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (6 subgoals):
 1. \<And>cteat tcbat x. tcbat \<longrightarrow> (\<exists>getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF) \<and> (\<forall>f g tcb. setF f (setF g tcb) = setF (f \<circ> g) tcb)) \<Longrightarrow> (tcbat \<longrightarrow> (cteat \<longrightarrow> modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOCTE val') else ps a)) (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val)) x) = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val'))) x) \<and> (\<not> cteat \<longrightarrow> modify (ksPSpace_update (\<lambda>ps a. if a = p && ~~ mask tcbBlockSizeBits then Some (KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))) else ps a)) (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits)))))))) x) = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. val') (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x)) \<and> (\<not> tcbat \<longrightarrow> cteat \<longrightarrow> modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOCTE val') else ps a)) (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val)) x) = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE val'))) x)
 2. \<And>cteat tcbat c. \<lbrace>?Q63 cteat tcbat c\<rbrace> gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>t. (\<lambda>_. c = cteat \<and> t = tcbat \<and> (tcbat \<longrightarrow> (\<exists>getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF) \<and> (\<forall>f g tcb. setF f (setF g tcb) = setF (f \<circ> g) tcb)))) and (\<lambda>_. True)\<rbrace>
 3. \<And>cteat tcbat. \<lbrace>?Q27 cteat tcbat\<rbrace> gets (real_cte_at' p) \<lbrace>?Q63 cteat tcbat\<rbrace>
 4. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' p s = uu_ \<and> (tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and ?Q27 uu_ tcbat\<rbrace>
 5. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (5 subgoals):
 1. \<And>cteat tcbat c. \<lbrace>?Q63 cteat tcbat c\<rbrace> gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>t. (\<lambda>_. c = cteat \<and> t = tcbat \<and> (tcbat \<longrightarrow> (\<exists>getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF) \<and> (\<forall>f g tcb. setF f (setF g tcb) = setF (f \<circ> g) tcb)))) and (\<lambda>_. True)\<rbrace>
 2. \<And>cteat tcbat. \<lbrace>?Q27 cteat tcbat\<rbrace> gets (real_cte_at' p) \<lbrace>?Q63 cteat tcbat\<rbrace>
 3. \<And>uu_. \<lbrace>?P20 uu_\<rbrace> gets (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' p s = uu_ \<and> (tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and ?Q27 uu_ tcbat\<rbrace>
 4. \<lbrace>?P9\<rbrace> gets (real_cte_at' p) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and (?P20 uu_ and (\<lambda>_. True))\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>s. ((\<lambda>_. True) and ((\<lambda>sa. ((\<lambda>sb. real_cte_at' p sb = real_cte_at' p s \<and> (tcb_at' (p && ~~ mask tcbBlockSizeBits) sb \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) sa) and (\<lambda>sb. ((\<lambda>_. real_cte_at' p sb = real_cte_at' p s \<and> (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) sb = (tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) sa \<and> ((tcb_at' (p && ~~ mask 9) and K (p && mask 9 \<in> dom tcb_cte_cases)) sa \<longrightarrow> (\<exists>getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF) \<and> (\<forall>f g tcb. setF f (setF g tcb) = setF (f \<circ> g) tcb)))) and (\<lambda>_. True)) sb)) sa) and (\<lambda>_. True))) s) and (\<lambda>_. True))) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b f g aa ba c d e fa ga h i j k l m n pa q. \<lbrakk>tcb_at' (p && ~~ mask 9) s; tcb_cte_cases (p && mask 9) = Some (a, b)\<rbrakk> \<Longrightarrow> b f (b g (Thread aa ba c d e fa ga h i j k l m n pa q)) = b (f \<circ> g) (Thread aa ba c d e fa ga h i j k l m n pa q) proof (prove)
goal:
No subgoals!