theory Finalise_R

lemma no_fail_isFinalCapability [wp]:
  "no_fail (valid_mdb' and cte_wp_at' ((=) cte) p) (isFinalCapability cte)" apply (simp add: isFinalCapability_def) apply (clarsimp simp: Let_def split del: if_split) apply (rule no_fail_pre, wp getCTE_wp') apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def cte_wp_at_ctes_of nullPointer_def) apply (rule conjI) apply clarsimp apply (erule (2) valid_dlistEp) apply simp apply clarsimp apply (rule conjI) apply (erule (2) valid_dlistEn) apply simp apply clarsimp apply (rule valid_dlistEn, assumption+) apply (erule (2) valid_dlistEp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (valid_mdb' and cte_wp_at' ((=) cte) p) (isFinalCapability cte) proof (prove)
goal (1 subgoal):
 1. no_fail (valid_mdb' and cte_wp_at' ((=) cte) p) (let mdb = cteMDBNode cte in do prevIsSameObject <- if mdbPrev mdb = nullPointer then return False else do prev <- getCTE (mdbPrev mdb);
return (global.sameObjectAs (cteCap prev) (cteCap cte))
od;
if prevIsSameObject then return False else if mdbNext mdb = nullPointer then return True else do next <- getCTE (mdbNext mdb);
return (\<not> global.sameObjectAs (cteCap cte) (cteCap next))
od
od) proof (prove)
goal (1 subgoal):
 1. no_fail (valid_mdb' and cte_wp_at' ((=) cte) p) (do prevIsSameObject <- if mdbPrev (cteMDBNode cte) = nullPointer then return False else do prev <- getCTE (mdbPrev (cteMDBNode cte));
return (global.sameObjectAs (cteCap prev) (cteCap cte))
od;
if prevIsSameObject then return False else if mdbNext (cteMDBNode cte) = nullPointer then return True else do next <- getCTE (mdbNext (cteMDBNode cte));
return (\<not> global.sameObjectAs (cteCap cte) (cteCap next))
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_mdb' and cte_wp_at' ((=) cte) p) s \<Longrightarrow> ((if mdbPrev (cteMDBNode cte) = nullPointer then \<lambda>_. True else cte_wp_at' (\<lambda>_. True) (mdbPrev (cteMDBNode cte)) and (\<lambda>s. \<forall>ctea. cte_wp_at' ((=) ctea) (mdbPrev (cteMDBNode cte)) s \<longrightarrow> True)) and (\<lambda>s. (mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> (if False then \<lambda>_. True else if mdbNext (cteMDBNode cte) = nullPointer then \<lambda>_. True else cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode cte)) and (\<lambda>s. \<forall>ctea. cte_wp_at' ((=) ctea) (mdbNext (cteMDBNode cte)) s \<longrightarrow> True)) s) \<and> (mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> (\<forall>ctea. cte_wp_at' ((=) ctea) (mdbPrev (cteMDBNode cte)) s \<longrightarrow> (if global.sameObjectAs (cteCap ctea) (cteCap cte) then \<lambda>_. True else if mdbNext (cteMDBNode cte) = nullPointer then \<lambda>_. True else cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode cte)) and (\<lambda>s. \<forall>ctea. cte_wp_at' ((=) ctea) (mdbNext (cteMDBNode cte)) s \<longrightarrow> True)) s)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode cte) = 0 \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (mdbPrev (cteMDBNode cte) = 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = 0 \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea)
 2. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (mdbPrev (cteMDBNode cte) = 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea
 2. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (mdbPrev (cteMDBNode cte) = 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte'. \<lbrakk>no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0; mdbPrev (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbPrev (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea
 2. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (mdbPrev (cteMDBNode cte) = 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (mdbPrev (cteMDBNode cte) = 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) = 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) \<and> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) = 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)
 2. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte'. \<lbrakk>no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) = 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)
 2. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte'. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte' cte'a. \<lbrakk>no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = p; ctes_of s (mdbPrev (cteMDBNode cte)) = Some cte'a; mdbNext (cteMDBNode cte'a) = p\<rbrakk> \<Longrightarrow> (\<exists>ctea. ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea) \<and> (\<forall>ctea. \<not> global.sameObjectAs (cteCap ctea) (cteCap cte) \<longrightarrow> ctes_of s (mdbPrev (cteMDBNode cte)) = Some ctea \<longrightarrow> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) proof (prove)
goal:
No subgoals!