theory CNodeInv_R

lemma cteMove_ifunsafe':
  "\<lbrace>if_unsafe_then_cap'
      and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest
      and ex_cte_cap_to' dest
      and cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src\<rbrace>
     cteMove cap src dest
   \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" apply (rule hoare_pre) apply (simp add: ifunsafe'_def3 cteMove_def o_def) apply (wp getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def) apply (subgoal_tac "ex_cte_cap_to' cref s") apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of) apply (rule_tac x="(id (dest := src, src := dest)) crefb"
                in exI) apply (auto simp: modify_map_def dest!: weak_derived_cte_refs
              split: if_split_asm)[1] apply (case_tac "cref = dest") apply simp apply (rule if_unsafe_then_capD'[where P="\<lambda>cte. cteCap cte \<noteq> NullCap"]) apply (clarsimp simp add: cte_wp_at_ctes_of modify_map_def
                       split: if_split_asm) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest and ex_cte_cap_wp_to' (\<lambda>_. True) dest and cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src\<rbrace> cteMove cap src dest \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cteMove cap src dest \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>
 2. \<And>s. (if_unsafe_then_cap' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest and ex_cte_cap_wp_to' (\<lambda>_. True) dest and cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
cte <- getCTE src;
y <- updateCap dest cap;
y <- updateCap src capability.NullCap;
y <- updateMDB dest (const (cteMDBNode cte));
y <- updateMDB src (const nullMDBNode);
y <- updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))\<rbrace>
 2. \<And>s. (if_unsafe_then_cap' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest and ex_cte_cap_wp_to' (\<lambda>_. True) dest and cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (if_unsafe_then_cap' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest and ex_cte_cap_wp_to' (\<lambda>_. True) dest and cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src) s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) dest s \<longrightarrow> cteCap cte = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) src s \<longrightarrow> (\<forall>cref. (\<exists>capa. modify_map (modify_map (cteCaps_of s) dest (K cap)) src (K capability.NullCap) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (modify_map (cteCaps_of s) dest (K cap)) src (K capability.NullCap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s) proof (prove)
goal (2 subgoals):
 1. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; ex_cte_cap_wp_to' (\<lambda>_. True) cref s\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s ctea cteb cref capa crefa crefb cte ctec. \<lbrakk>if_unsafe_then_cap' s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; ctes_of s crefa = Some cte; dest \<in> cte_refs' (cteCap cte) (irq_node' s); ctes_of s crefb = Some ctec; cref \<in> cte_refs' (cteCap ctec) (irq_node' s)\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s ctea cteb cref capa crefa crefb cte ctec. \<lbrakk>if_unsafe_then_cap' s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; ctes_of s crefa = Some cte; dest \<in> cte_refs' (cteCap cte) (irq_node' s); ctes_of s crefb = Some ctec; cref \<in> cte_refs' (cteCap ctec) (irq_node' s)\<rbrakk> \<Longrightarrow> \<exists>cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) ((id(dest := src, src := dest)) crefb) = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; cref = dest\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s
 2. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; cref \<noteq> dest\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; cref \<noteq> dest\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (3 subgoals):
 1. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; cref \<noteq> dest\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte \<noteq> capability.NullCap) cref s
 2. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; cref \<noteq> dest\<rbrakk> \<Longrightarrow> if_unsafe_then_cap' s
 3. \<And>s ctea cteb cref capa cte. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; cref \<noteq> dest; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> cteCap cte \<noteq> capability.NullCap proof (prove)
goal (2 subgoals):
 1. \<And>s ctea cteb cref capa. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; cref \<noteq> dest\<rbrakk> \<Longrightarrow> if_unsafe_then_cap' s
 2. \<And>s ctea cteb cref capa cte. \<lbrakk>if_unsafe_then_cap' s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; cteCap ctea = capability.NullCap; weak_derived' (cteCap cteb) cap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; ctes_of s src = Some cteb; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) cref = Some capa; capa \<noteq> capability.NullCap; cref \<noteq> dest; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> cteCap cte \<noteq> capability.NullCap proof (prove)
goal:
No subgoals!