theory CNodeInv_R

lemma cteSwap_ifunsafe'[wp]:
  "\<lbrace>if_unsafe_then_cap' and ex_cte_cap_to' c1 and ex_cte_cap_to' c2
        and cte_wp_at' (\<lambda>cte. cte_refs' (cteCap cte) = cte_refs' c) c1
        and cte_wp_at' (\<lambda>cte. cte_refs' (cteCap cte) = cte_refs' c') c2\<rbrace>
     cteSwap c c1 c' c2
  \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" apply (simp add: ifunsafe'_def3 cteSwap_def) apply (wp | simp add: o_def | rule 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 (c1 := c2, c2 := c1)) crefc" in exI) apply (clarsimp simp: modify_map_def) apply fastforce apply (clarsimp dest!: modify_map_K_D
                 split: if_split_asm) apply (drule_tac x=cref in spec) apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap' and ex_cte_cap_wp_to' (\<lambda>_. True) c1 and ex_cte_cap_wp_to' (\<lambda>_. True) c2 and cte_wp_at' (\<lambda>cte. cte_refs' (cteCap cte) = cte_refs' c) c1 and cte_wp_at' (\<lambda>cte. cte_refs' (cteCap cte) = cte_refs' c') c2\<rbrace> cteSwap c c1 c' c2 \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>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))) and ex_cte_cap_wp_to' (\<lambda>_. True) c1 and ex_cte_cap_wp_to' (\<lambda>_. True) c2 and cte_wp_at' (\<lambda>cte. cte_refs' (cteCap cte) = cte_refs' c) c1 and cte_wp_at' (\<lambda>cte. cte_refs' (cteCap cte) = cte_refs' c') c2\<rbrace> do cte1 <- getCTE c1;
y <- updateCap c1 c';
y <- updateCap c2 c;
y <- updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. c2));
y <- updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. c2));
cte2 <- getCTE c2;
y <- updateMDB c1 (const (cteMDBNode cte2));
y <- updateMDB c2 (const (cteMDBNode cte1));
y <- updateMDB (mdbPrev (cteMDBNode cte2)) (mdbNext_update (\<lambda>_. c1));
updateMDB (mdbNext (cteMDBNode cte2)) (mdbPrev_update (\<lambda>_. c1))
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> proof (prove)
goal (1 subgoal):
 1. \<And>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))) \<and> ex_cte_cap_wp_to' (\<lambda>_. True) c1 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) c2 s \<and> cte_wp_at' (\<lambda>cte. cte_refs' (cteCap cte) = cte_refs' c) c1 s \<and> cte_wp_at' (\<lambda>cte. cte_refs' (cteCap cte) = cte_refs' c') c2 s \<Longrightarrow> \<forall>cref. (\<exists>cap. modify_map (modify_map (cteCaps_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (modify_map (cteCaps_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cref cte ctea cap. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ex_cte_cap_wp_to' (\<lambda>_. True) c1 s; ex_cte_cap_wp_to' (\<lambda>_. True) c2 s; ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref = Some cap; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s) proof (prove)
goal (2 subgoals):
 1. \<And>s cref cte ctea cap. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ex_cte_cap_wp_to' (\<lambda>_. True) c1 s; ex_cte_cap_wp_to' (\<lambda>_. True) c2 s; ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref = Some cap; cap \<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) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s cref cte ctea cap. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ex_cte_cap_wp_to' (\<lambda>_. True) c1 s; ex_cte_cap_wp_to' (\<lambda>_. True) c2 s; ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref = Some cap; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s cref cte ctea cap crefa crefb crefc cteb ctec cted. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref = Some cap; cap \<noteq> capability.NullCap; ctes_of s crefa = Some cteb; c1 \<in> cte_refs' (cteCap cteb) (irq_node' s); ctes_of s crefb = Some ctec; c2 \<in> cte_refs' (cteCap ctec) (irq_node' s); ctes_of s crefc = Some cted; cref \<in> cte_refs' (cteCap cted) (irq_node' s)\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s cref cte ctea cap. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ex_cte_cap_wp_to' (\<lambda>_. True) c1 s; ex_cte_cap_wp_to' (\<lambda>_. True) c2 s; ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref = Some cap; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s cref cte ctea cap crefa crefb crefc cteb ctec cted. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref = Some cap; cap \<noteq> capability.NullCap; ctes_of s crefa = Some cteb; c1 \<in> cte_refs' (cteCap cteb) (irq_node' s); ctes_of s crefb = Some ctec; c2 \<in> cte_refs' (cteCap ctec) (irq_node' s); ctes_of s crefc = Some cted; cref \<in> cte_refs' (cteCap cted) (irq_node' s)\<rbrakk> \<Longrightarrow> \<exists>cap'. modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) ((id(c1 := c2, c2 := c1)) crefc) = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s cref cte ctea cap. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ex_cte_cap_wp_to' (\<lambda>_. True) c1 s; ex_cte_cap_wp_to' (\<lambda>_. True) c2 s; ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref = Some cap; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s cref cte ctea cap crefa crefb crefc cteb ctec cted. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; (if cref = c2 then map_option (\<lambda>a. c) (if c2 = c1 then Some c' else Some (cteCap ctea)) else if cref = c1 then Some c' else map_option cteCap (ctes_of s cref)) = Some cap; cap \<noteq> capability.NullCap; ctes_of s crefa = Some cteb; c1 \<in> cte_refs' (cteCap cteb) (irq_node' s); ctes_of s crefb = Some ctec; c2 \<in> cte_refs' (cteCap ctec) (irq_node' s); ctes_of s crefc = Some cted; cref \<in> cte_refs' (cteCap cted) (irq_node' s)\<rbrakk> \<Longrightarrow> (crefc = c1 \<longrightarrow> cref \<in> cte_refs' c (irq_node' s)) \<and> (crefc \<noteq> c1 \<longrightarrow> crefc = c2 \<longrightarrow> (c1 = c2 \<longrightarrow> cref \<in> cte_refs' c (irq_node' s)) \<and> (c1 \<noteq> c2 \<longrightarrow> cref \<in> cte_refs' c' (irq_node' s)))
 2. \<And>s cref cte ctea cap. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ex_cte_cap_wp_to' (\<lambda>_. True) c1 s; ex_cte_cap_wp_to' (\<lambda>_. True) c2 s; ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref = Some cap; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s cref cte ctea cap. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ex_cte_cap_wp_to' (\<lambda>_. True) c1 s; ex_cte_cap_wp_to' (\<lambda>_. True) c2 s; ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) cref = Some cap; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s cref cte ctea z. \<lbrakk>\<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ex_cte_cap_wp_to' (\<lambda>_. True) c1 s; ex_cte_cap_wp_to' (\<lambda>_. True) c2 s; ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; cteCap z \<noteq> capability.NullCap; cref \<noteq> c2; cref \<noteq> c1; ctes_of s cref = Some z\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s cref cte ctea z. \<lbrakk>ex_cte_cap_wp_to' (\<lambda>_. True) c1 s; ex_cte_cap_wp_to' (\<lambda>_. True) c2 s; ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; cteCap z \<noteq> capability.NullCap; cref \<noteq> c2; cref \<noteq> c1; ctes_of s cref = Some z; (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s cref cte ctea z crefa crefb cref' cteb ctec za. \<lbrakk>ctes_of s c1 = Some cte; cte_refs' (cteCap cte) = cte_refs' c; ctes_of s c2 = Some ctea; cte_refs' (cteCap ctea) = cte_refs' c'; cteCap z \<noteq> capability.NullCap; cref \<noteq> c2; cref \<noteq> c1; ctes_of s cref = Some z; ctes_of s crefa = Some cteb; c1 \<in> cte_refs' (cteCap cteb) (irq_node' s); ctes_of s crefb = Some ctec; c2 \<in> cte_refs' (cteCap ctec) (irq_node' s); cref \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> \<exists>crefa cte. ctes_of s crefa = Some cte \<and> cref \<in> cte_refs' (cteCap cte) (irq_node' s) proof (prove)
goal:
No subgoals!