theory Fastpath_Equiv

lemma setEndpoint_setCTE_pivot[unfolded K_bind_def]:
  "do setEndpoint p val; setCTE slot cte; f od =
     do setCTE slot cte; setEndpoint p val; f od" supply if_split[split del] apply (rule monadic_rewrite_to_eq) apply simp apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_trans,
          rule_tac f="ep_at' p" in monadic_rewrite_add_gets) apply (rule monadic_rewrite_transverse, rule monadic_rewrite_add_gets,
          rule monadic_rewrite_bind_tail) apply (rename_tac epat) apply (rule monadic_rewrite_transverse) apply (rule monadic_rewrite_bind_tail) apply (simp add: setEndpoint_def setObject_modify_assert bind_assoc) apply (rule_tac rv=epat in monadic_rewrite_gets_known) apply (wp setCTE_typ_at'[where T="koType TYPE(endpoint)", unfolded typ_at_to_obj_at']
                  | simp)+ apply (simp add: setCTE_assert_modify bind_assoc) apply (rule monadic_rewrite_trans, rule monadic_rewrite_add_gets,
           rule monadic_rewrite_bind_tail)+ apply (rename_tac cteat tcbat) apply (rule monadic_rewrite_trans, rule monadic_rewrite_bind_tail) apply (rule monadic_rewrite_trans) apply (rule_tac rv=cteat in monadic_rewrite_gets_known) apply (rule_tac rv=tcbat in monadic_rewrite_gets_known) apply (wp setEndpoint_typ_at'[where T="koType TYPE(tcb)", unfolded typ_at_to_obj_at']
                 setEndpoint_typ_at'[where T="koType TYPE(cte)", unfolded typ_at_to_obj_at']
                     | simp)+ apply (rule_tac P="\<lambda>s. epat = ep_at' p s \<and> cteat = real_cte_at' slot s
                           \<and> tcbat = (tcb_at' (slot && ~~ mask 9) and (%y. slot && mask 9 : dom tcb_cte_cases)) s"
                   in monadic_rewrite_pre_imp_eq) apply (simp add: setEndpoint_def setObject_modify_assert bind_assoc
                       exec_gets assert_def exec_modify
                split: if_split) apply (auto split: if_split simp: obj_at'_def projectKOs objBits_defs
                    del: ext
                 intro!: arg_cong[where f=f] ext kernel_state.fold_congs)[1] apply wp+ apply (simp add: objBits_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do setEndpoint p val;
setCTE slot cte;
f
od = do setCTE slot cte;
setEndpoint p val;
f
od proof (prove)
goal (1 subgoal):
 1. do setEndpoint p val;
setCTE slot cte;
f
od = do setCTE slot cte;
setEndpoint p val;
f
od proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False True (\<lambda>_. True) (do setEndpoint p val;
setCTE slot cte;
f
od) (do setCTE slot cte;
setEndpoint p val;
f
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False True (\<lambda>_. True) (do y <- setEndpoint p val;
y <- setCTE slot cte;
f
od) (do y <- setCTE slot cte;
y <- setEndpoint p val;
f
od) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False True ?Q2 (do y <- setEndpoint p val;
y <- setCTE slot cte;
f
od) (do y <- setCTE slot cte;
y <- setEndpoint p val;
f
od)
 2. \<And>s. True \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False True ?Q5 (do _ <- gets (ep_at' p);
y <- setEndpoint p val;
y <- setCTE slot cte;
f
od) (do y <- setCTE slot cte;
y <- setEndpoint p val;
f
od)
 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 <- setEndpoint p val;
y <- setCTE slot cte;
f
od) (do y <- setCTE slot cte;
y <- setEndpoint p val;
f
od)
 2. \<lbrace>?P9\<rbrace> gets (ep_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>epat. monadic_rewrite False True (?Q13 epat) (do y <- setEndpoint p val;
y <- setCTE slot cte;
f
od) (do y <- setCTE slot cte;
y <- setEndpoint p val;
f
od)
 2. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>?Q13\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (4 subgoals):
 1. \<And>epat. monadic_rewrite False True (?Q16 epat) (do y <- setCTE slot cte;
y <- setEndpoint p val;
f
od) (?b16 epat)
 2. \<And>epat. monadic_rewrite False True (?P16 epat) (do y <- setEndpoint p val;
y <- setCTE slot cte;
f
od) (?b16 epat)
 3. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. ?P16 epat and ?Q16 epat\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (5 subgoals):
 1. \<And>epat y. monadic_rewrite False True (?Q19 epat y) (do y <- setEndpoint p val;
f
od) (?j19 epat y)
 2. \<And>epat. \<lbrace>?Q16 epat\<rbrace> setCTE slot cte \<lbrace>?Q19 epat\<rbrace>
 3. \<And>epat. monadic_rewrite False True (?P16 epat) (do y <- setEndpoint p val;
y <- setCTE slot cte;
f
od) (setCTE slot cte >>= ?j19 epat)
 4. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. ?P16 epat and ?Q16 epat\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (5 subgoals):
 1. \<And>epat. monadic_rewrite False True (?Q19 epat ()) (do fa <- gets (ep_at' p);
y <- assert fa;
y <- modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint val)));
f
od) (?j19 epat ())
 2. \<And>epat. \<lbrace>?Q16 epat\<rbrace> setCTE slot cte \<lbrace>?Q19 epat\<rbrace>
 3. \<And>epat. monadic_rewrite False True (?P16 epat) (do y <- setEndpoint p val;
y <- setCTE slot cte;
f
od) (setCTE slot cte >>= ?j19 epat)
 4. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. ?P16 epat and ?Q16 epat\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (4 subgoals):
 1. \<And>epat. \<lbrace>?Q16 epat\<rbrace> setCTE slot cte \<lbrace>\<lambda>a b. ep_at' p b = epat\<rbrace>
 2. \<And>epat. monadic_rewrite False True (?P16 epat) (do y <- setEndpoint p val;
y <- setCTE slot cte;
f
od) (do x <- setCTE slot cte;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint val)));
f
od)
 3. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. ?P16 epat and ?Q16 epat\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (3 subgoals):
 1. \<And>epat. monadic_rewrite False True (?P16 epat) (do y <- setEndpoint p val;
y <- setCTE slot cte;
f
od) (do x <- setCTE slot cte;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a));
f
od)
 2. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. ?P16 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (3 subgoals):
 1. \<And>epat. monadic_rewrite False True (?P16 epat) (do y <- setEndpoint p val;
c <- gets (real_cte_at' slot);
t <- gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
y <- if c then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
f
od) (do c <- gets (real_cte_at' slot);
t <- gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
x <- if c then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a));
f
od)
 2. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. ?P16 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (5 subgoals):
 1. \<And>epat uu_ uua_. monadic_rewrite False True (?Q39 epat uu_ uua_) (do y <- setEndpoint p val;
c <- gets (real_cte_at' slot);
t <- gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
y <- if c then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
f
od) (do x <- if uu_ then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if uua_ then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a));
f
od)
 2. \<And>epat uu_. \<lbrace>?Q35 epat uu_\<rbrace> gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>?Q39 epat uu_\<rbrace>
 3. \<And>epat. \<lbrace>?Q28 epat\<rbrace> gets (real_cte_at' slot) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q35 epat uu_\<rbrace>
 4. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. (\<lambda>_. True) and ?Q28 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (5 subgoals):
 1. \<And>epat cteat tcbat. monadic_rewrite False True (?Q39 epat cteat tcbat) (do y <- setEndpoint p val;
c <- gets (real_cte_at' slot);
t <- gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
y <- if c then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
f
od) (do x <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a));
f
od)
 2. \<And>epat uu_. \<lbrace>?Q35 epat uu_\<rbrace> gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>?Q39 epat uu_\<rbrace>
 3. \<And>epat. \<lbrace>?Q28 epat\<rbrace> gets (real_cte_at' slot) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q35 epat uu_\<rbrace>
 4. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. (\<lambda>_. True) and ?Q28 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (7 subgoals):
 1. \<And>epat cteat tcbat y. monadic_rewrite False True (?Q45 epat cteat tcbat y) (do c <- gets (real_cte_at' slot);
t <- gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
y <- if c then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
f
od) (?j45 epat cteat tcbat y)
 2. \<And>epat cteat tcbat. \<lbrace>?P42 epat cteat tcbat\<rbrace> setEndpoint p val \<lbrace>?Q45 epat cteat tcbat\<rbrace>
 3. \<And>epat cteat tcbat. monadic_rewrite False True (?Q42 epat cteat tcbat) (setEndpoint p val >>= ?j45 epat cteat tcbat) (do x <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a));
f
od)
 4. \<And>epat uu_. \<lbrace>?Q35 epat uu_\<rbrace> gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. ?P42 epat uu_ tcbat and ?Q42 epat uu_ tcbat\<rbrace>
 5. \<And>epat. \<lbrace>?Q28 epat\<rbrace> gets (real_cte_at' slot) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q35 epat uu_\<rbrace>
 6. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. (\<lambda>_. True) and ?Q28 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (8 subgoals):
 1. \<And>epat cteat tcbat y. monadic_rewrite False True (?P48 epat cteat tcbat y) (do c <- gets (real_cte_at' slot);
t <- gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
y <- if c then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
f
od) (?g48 epat cteat tcbat y)
 2. \<And>epat cteat tcbat y. monadic_rewrite False True (?Q48 epat cteat tcbat y) (?g48 epat cteat tcbat y) (?j45 epat cteat tcbat y)
 3. \<And>epat cteat tcbat. \<lbrace>?P42 epat cteat tcbat\<rbrace> setEndpoint p val \<lbrace>\<lambda>y. ?P48 epat cteat tcbat y and ?Q48 epat cteat tcbat y\<rbrace>
 4. \<And>epat cteat tcbat. monadic_rewrite False True (?Q42 epat cteat tcbat) (setEndpoint p val >>= ?j45 epat cteat tcbat) (do x <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a));
f
od)
 5. \<And>epat uu_. \<lbrace>?Q35 epat uu_\<rbrace> gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. ?P42 epat uu_ tcbat and ?Q42 epat uu_ tcbat\<rbrace>
 6. \<And>epat. \<lbrace>?Q28 epat\<rbrace> gets (real_cte_at' slot) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q35 epat uu_\<rbrace>
 7. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. (\<lambda>_. True) and ?Q28 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (7 subgoals):
 1. \<And>epat cteat tcbat y. monadic_rewrite False True (?Q48 epat cteat tcbat y) (do t <- gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
y <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
f
od) (?j45 epat cteat tcbat y)
 2. \<And>epat cteat tcbat. \<lbrace>?P42 epat cteat tcbat\<rbrace> setEndpoint p val \<lbrace>\<lambda>y. (\<lambda>s. real_cte_at' slot s = cteat) and ?Q48 epat cteat tcbat y\<rbrace>
 3. \<And>epat cteat tcbat. monadic_rewrite False True (?Q42 epat cteat tcbat) (setEndpoint p val >>= ?j45 epat cteat tcbat) (do x <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a));
f
od)
 4. \<And>epat uu_. \<lbrace>?Q35 epat uu_\<rbrace> gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. ?P42 epat uu_ tcbat and ?Q42 epat uu_ tcbat\<rbrace>
 5. \<And>epat. \<lbrace>?Q28 epat\<rbrace> gets (real_cte_at' slot) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q35 epat uu_\<rbrace>
 6. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. (\<lambda>_. True) and ?Q28 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (6 subgoals):
 1. \<And>epat cteat tcbat. \<lbrace>?P42 epat cteat tcbat\<rbrace> setEndpoint p val \<lbrace>\<lambda>y. (\<lambda>s. real_cte_at' slot s = cteat) and (\<lambda>s. (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) s = tcbat)\<rbrace>
 2. \<And>epat cteat tcbat. monadic_rewrite False True (?Q42 epat cteat tcbat) (do x <- setEndpoint p val;
y <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
f
od) (do x <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a));
f
od)
 3. \<And>epat uu_. \<lbrace>?Q35 epat uu_\<rbrace> gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. ?P42 epat uu_ tcbat and ?Q42 epat uu_ tcbat\<rbrace>
 4. \<And>epat. \<lbrace>?Q28 epat\<rbrace> gets (real_cte_at' slot) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q35 epat uu_\<rbrace>
 5. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. (\<lambda>_. True) and ?Q28 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (5 subgoals):
 1. \<And>epat cteat tcbat. monadic_rewrite False True (?Q42 epat cteat tcbat) (do x <- setEndpoint p val;
y <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
f
od) (do x <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a));
f
od)
 2. \<And>epat uu_. \<lbrace>?Q35 epat uu_\<rbrace> gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' slot s = uu_ \<and> (tcb_at' (slot && ~~ mask tcbBlockSizeBits) s \<and> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and ?Q42 epat uu_ tcbat\<rbrace>
 3. \<And>epat. \<lbrace>?Q28 epat\<rbrace> gets (real_cte_at' slot) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q35 epat uu_\<rbrace>
 4. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. (\<lambda>_. True) and ?Q28 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (5 subgoals):
 1. \<And>epat cteat tcbat s. epat = ep_at' p s \<and> cteat = real_cte_at' slot s \<and> tcbat = (tcb_at' (slot && ~~ mask 9) and (\<lambda>y. slot && mask 9 \<in> dom tcb_cte_cases)) s \<Longrightarrow> (do x <- setEndpoint p val;
y <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
f
od) s = (do x <- if cteat then modify (ksPSpace_update (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) else if tcbat then modify (ksPSpace_update (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) else fail;
y <- assert epat;
y <- modify (ksPSpace_update (\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a));
f
od) s
 2. \<And>epat uu_. \<lbrace>?Q35 epat uu_\<rbrace> gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' slot s = uu_ \<and> (tcb_at' (slot && ~~ mask tcbBlockSizeBits) s \<and> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and (\<lambda>s. epat = ep_at' p s \<and> uu_ = real_cte_at' slot s \<and> tcbat = (tcb_at' (slot && ~~ mask 9) and (\<lambda>y. slot && mask 9 \<in> dom tcb_cte_cases)) s)\<rbrace>
 3. \<And>epat. \<lbrace>?Q28 epat\<rbrace> gets (real_cte_at' slot) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q35 epat uu_\<rbrace>
 4. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. (\<lambda>_. True) and ?Q28 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (5 subgoals):
 1. \<And>epat s. epat = ep_at' p s \<Longrightarrow> ep_at' p s \<longrightarrow> (tcb_at' (slot && ~~ mask 9) s \<and> slot && mask 9 \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' slot s \<longrightarrow> f (ksPSpace_update ((\<lambda>ps. ps(slot \<mapsto> KOCTE cte)) \<circ> (\<lambda>ps. ps(p \<mapsto> KOEndpoint val))) s) = f (ksPSpace_update ((\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a) \<circ> (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) s)) \<and> (\<not> real_cte_at' slot s \<longrightarrow> f (ksPSpace_update ((\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits)))))))) \<circ> (\<lambda>ps. ps(p \<mapsto> KOEndpoint val))) s) = f (ksPSpace_update ((\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a) \<circ> (\<lambda>ps. ps(slot && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (slot && ~~ mask tcbBlockSizeBits))))))))) s))) \<and> ((tcb_at' (slot && ~~ mask 9) s \<longrightarrow> slot && mask 9 \<notin> dom tcb_cte_cases) \<longrightarrow> real_cte_at' slot s \<longrightarrow> f (ksPSpace_update ((\<lambda>ps. ps(slot \<mapsto> KOCTE cte)) \<circ> (\<lambda>ps. ps(p \<mapsto> KOEndpoint val))) s) = f (ksPSpace_update ((\<lambda>ps a. if a = p then Some (KOEndpoint val) else ps a) \<circ> (\<lambda>ps. ps(slot \<mapsto> KOCTE cte))) s))
 2. \<And>epat uu_. \<lbrace>?Q35 epat uu_\<rbrace> gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' slot s = uu_ \<and> (tcb_at' (slot && ~~ mask tcbBlockSizeBits) s \<and> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and (\<lambda>s. epat = ep_at' p s \<and> uu_ = real_cte_at' slot s \<and> tcbat = (tcb_at' (slot && ~~ mask 9) and (\<lambda>y. slot && mask 9 \<in> dom tcb_cte_cases)) s)\<rbrace>
 3. \<And>epat. \<lbrace>?Q28 epat\<rbrace> gets (real_cte_at' slot) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q35 epat uu_\<rbrace>
 4. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. (\<lambda>_. True) and ?Q28 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (?P9 and (\<lambda>_. True))) s proof (prove)
goal (4 subgoals):
 1. \<And>epat uu_. \<lbrace>?Q35 epat uu_\<rbrace> gets (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) \<lbrace>\<lambda>tcbat. (\<lambda>s. real_cte_at' slot s = uu_ \<and> (tcb_at' (slot && ~~ mask tcbBlockSizeBits) s \<and> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = tcbat) and (\<lambda>s. epat = ep_at' p s \<and> uu_ = real_cte_at' slot s \<and> tcbat = (tcb_at' (slot && ~~ mask 9) and (\<lambda>y. slot && mask 9 \<in> dom tcb_cte_cases)) s)\<rbrace>
 2. \<And>epat. \<lbrace>?Q28 epat\<rbrace> gets (real_cte_at' slot) \<lbrace>\<lambda>uu_. (\<lambda>_. True) and ?Q35 epat uu_\<rbrace>
 3. \<lbrace>?P9\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>epat. (\<lambda>_. True) and ?Q28 epat and (\<lambda>s. ep_at' p s = epat)\<rbrace>
 4. \<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>_. True) and (\<lambda>sb. ((\<lambda>s. real_cte_at' slot s = real_cte_at' slot sa \<and> (tcb_at' (slot && ~~ mask tcbBlockSizeBits) s \<and> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases) = (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) sb) and (\<lambda>sc. ep_at' p s = ep_at' p sc \<and> real_cte_at' slot sa = real_cte_at' slot sc \<and> (tcb_at' (slot && ~~ mask tcbBlockSizeBits) and (\<lambda>y. slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)) sb = (tcb_at' (slot && ~~ mask 9) and (\<lambda>y. slot && mask 9 \<in> dom tcb_cte_cases)) sc)) sb)) sa) and (\<lambda>sa. ep_at' p sa = ep_at' p s)) s) and (\<lambda>_. True))) s proof (prove)
goal:
No subgoals!