theory Fastpath_Equiv

lemma setCTE_updateCapMDB:
  "p \<noteq> 0 \<Longrightarrow>
   setCTE p cte = do updateCap p (cteCap cte); updateMDB p (const (cteMDBNode cte)) od" supply if_split[split del] apply (simp add: updateCap_def updateMDB_def bind_assoc set_getCTE
                   cte_overwrite set_setCTE) apply (simp add: getCTE_assert_opt setCTE_assert_modify bind_assoc) apply (rule ext, simp add: exec_gets assert_opt_def exec_modify
                      split: if_split option.split) apply (cut_tac P=\<top> and p=p and s=x in cte_wp_at_ctes_of) apply (cases cte) apply (simp add: cte_wp_at_obj_cases') apply (auto simp: mask_out_sub_mask) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> setCTE p cte = do updateCap p (cteCap cte);
updateMDB p (const (cteMDBNode cte))
od proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> setCTE p cte = do updateCap p (cteCap cte);
updateMDB p (const (cteMDBNode cte))
od proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> setCTE p cte = do ctea <- getCTE p;
setCTE p cte
od proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> 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 cte))) 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. cte) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail
od = do x <- gets (\<lambda>s. ctes_of s p);
ctea <- assert_opt x;
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 cte))) 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. cte) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail
od proof (prove)
goal (1 subgoal):
 1. \<And>x. p \<noteq> 0 \<Longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> ctes_of x p = None \<longrightarrow> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE cte))) x = fail x) \<and> (\<not> real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x = fail x)) \<and> ((tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> ctes_of x p = None \<longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE cte))) x = fail x) \<and> (\<not> real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x = fail x)) \<and> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE cte))) x = fail x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>p \<noteq> 0; cte_wp_at' (\<lambda>_. True) p x = (\<exists>cte. ctes_of x p = Some cte \<and> True)\<rbrakk> \<Longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> ctes_of x p = None \<longrightarrow> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE cte))) x = fail x) \<and> (\<not> real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x = fail x)) \<and> ((tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> ctes_of x p = None \<longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE cte))) x = fail x) \<and> (\<not> real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x = fail x)) \<and> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE cte))) x = fail x)) proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2. \<lbrakk>p \<noteq> 0; cte_wp_at' (\<lambda>_. True) p x = (\<exists>cte. ctes_of x p = Some cte \<and> True); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> ctes_of x p = None \<longrightarrow> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE cte))) x = fail x) \<and> (\<not> real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x = fail x)) \<and> ((tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> ctes_of x p = None \<longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE cte))) x = fail x) \<and> (\<not> real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. cte) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x = fail x)) \<and> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE cte))) x = fail x)) proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2. \<lbrakk>p \<noteq> 0; (real_cte_at' p x \<or> (\<exists>n\<in>dom tcb_cte_cases. tcb_at' (p - n) x)) = (\<exists>cte. ctes_of x p = Some cte); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> ctes_of x p = None \<longrightarrow> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE (CTE x1 x2)))) x = fail x) \<and> (\<not> real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. CTE x1 x2) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x = fail x)) \<and> ((tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> ctes_of x p = None \<longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE (CTE x1 x2)))) x = fail x) \<and> (\<not> real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. CTE x1 x2) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x = fail x)) \<and> (real_cte_at' p x \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE (CTE x1 x2)))) x = fail x)) proof (prove)
goal:
No subgoals!