theory CSpace_R

lemma cteInsert_no_0:
  "\<lbrace>valid_mdb' and pspace_aligned' and pspace_distinct' and
    (\<lambda>s. src \<noteq> dest) and K (capAligned cap) and valid_objs' and
    (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace>
   cteInsert cap src dest
   \<lbrace>\<lambda>_ s. no_0 (ctes_of s) \<rbrace>" apply (rule hoare_name_pre_state) apply clarsimp apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: if_split) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of
        setUntypedCapAsFull_ctes_of_no_0 mdb_inv_preserve_modify_map getCTE_wp
        setUntypedCapAsFull_valid_dlist mdb_inv_preserve_fun_upd | simp)+ apply (intro conjI impI) apply (clarsimp simp:cte_wp_at_ctes_of) apply (clarsimp simp:valid_mdb_ctes_def no_0_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and K (capAligned cap) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_ s. no_0 (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and K (capAligned cap) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_ s. no_0 (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_mdb' s; pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_ s. no_0 (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_mdb' s; pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do srcCTE <- getCTE src;
srcMDB <- return (cteMDBNode srcCTE);
srcCap <- return (cteCap srcCTE);
newCapIsRevocable <- return (revokable' srcCap cap);
newMDB <- return (mdbFirstBadged_update (\<lambda>_. newCapIsRevocable) (mdbRevocable_update (\<lambda>_. newCapIsRevocable) (mdbPrev_update (\<lambda>_. src) srcMDB)));
oldCTE <- getCTE dest;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
setUntypedCapAsFull srcCap cap src;
do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
updateMDB dest (const newMDB);
updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext newMDB) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>_ s. no_0 (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>_ s. no_0 (ctes_of s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s srcCTE x y ya. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B12 s srcCTE x y ya\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. \<forall>cte. cte_wp_at' ((=) cte) dest s \<longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) \<and> no_0 (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) \<and> no_0 (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) \<and> no_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode srcCTE)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))\<rbrace>
 2. \<And>s srcCTE x y. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B11 s srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B12 s srcCTE x y\<rbrace>
 3. \<And>s srcCTE x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B10 s srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B11 s srcCTE x\<rbrace>
 4. \<And>s srcCTE. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B9 s srcCTE\<rbrace> getCTE dest \<lbrace>?B10 s srcCTE\<rbrace>
 5. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s\<rbrace> getCTE src \<lbrace>?B9 s\<rbrace>
 6. \<And>s sa. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s; s = sa\<rbrakk> \<Longrightarrow> ?Q8 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s srcCTE x cte. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; ctes_of s src = Some cte; is_derived' (ctes_of s) src cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?B12 s srcCTE x () ()\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. \<forall>cte. ctes_of s dest = Some cte \<longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte))\<rbrace>
 2. \<And>s srcCTE x y. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B11 s srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B12 s srcCTE x y\<rbrace>
 3. \<And>s srcCTE x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B10 s srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B11 s srcCTE x\<rbrace>
 4. \<And>s srcCTE. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?B9 s srcCTE\<rbrace> getCTE dest \<lbrace>?B10 s srcCTE\<rbrace>
 5. \<And>s. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s\<rbrace> getCTE src \<lbrace>?B9 s\<rbrace>
 6. \<And>s sa. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; capAligned cap; valid_objs' s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s; s = sa\<rbrakk> \<Longrightarrow> ?Q8 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; cte_wp_at' (is_derived' (ctes_of sa) src cap \<circ> cteCap) src sa; s = sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) src sa \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src sa) \<and> \<not> cte_wp_at' (\<lambda>_. True) dest sa \<or> (\<forall>x. \<exists>cte. cte_wp_at' ((=) cte) src sa \<and> (\<exists>ctea. cte_wp_at' ((=) ctea) dest sa \<and> (cteCap ctea = capability.NullCap \<longrightarrow> ctes_of sa dest = Some x \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) \<and> cte_wp_at' ((=) cte) src sa))) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; cte_wp_at' (is_derived' (ctes_of sa) src cap \<circ> cteCap) src sa; s = sa; cte_wp_at' (\<lambda>_. True) src sa\<rbrakk> \<Longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src sa) \<and> \<not> cte_wp_at' (\<lambda>_. True) dest sa \<or> (\<forall>x. \<exists>cte. cte_wp_at' ((=) cte) src sa \<and> (\<exists>ctea. cte_wp_at' ((=) ctea) dest sa \<and> (cteCap ctea = capability.NullCap \<longrightarrow> ctes_of sa dest = Some x \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) \<and> cte_wp_at' ((=) cte) src sa))) proof (prove)
goal (1 subgoal):
 1. \<And>sa ctea x. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; valid_objs' sa; ctes_of sa src = Some ctea; is_derived' (ctes_of sa) src cap (cteCap ctea); ctes_of sa dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of sa a) proof (prove)
goal:
No subgoals!