theory CSpace_R

lemma ensureNoChildren_wp:
  "\<lbrace>\<lambda>s. (descendants_of' p (ctes_of s) \<noteq> {} \<longrightarrow> Q s)
    \<and> (descendants_of' p (ctes_of s) = {} \<longrightarrow> P () s)\<rbrace>
      ensureNoChildren p
   \<lbrace>P\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>" apply (simp add: ensureNoChildren_def whenE_def) apply (wp getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def descendants_of'_def) apply (intro conjI impI allI) apply clarsimp apply (drule spec, erule notE, rule subtree.direct_parent) apply (simp add:mdb_next_rel_def mdb_next_def) apply simp apply (simp add: parentOf_def) apply clarsimp apply (erule (4) subtree_no_parent) apply clarsimp apply (erule (2) subtree_next_0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (descendants_of' p (ctes_of s) \<noteq> {} \<longrightarrow> Q s) \<and> (descendants_of' p (ctes_of s) = {} \<longrightarrow> P () s)\<rbrace> ensureNoChildren p \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (descendants_of' p (ctes_of s) \<noteq> {} \<longrightarrow> Q s) \<and> (descendants_of' p (ctes_of s) = {} \<longrightarrow> P () s)\<rbrace> doE cte <- liftE (getCTE p);
if mdbNext (cteMDBNode cte) \<noteq> nullPointer then doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
if isMDBParentOf cte next then throwError Fault_H.syscall_error.RevokeFirst else returnOk ()
odE else returnOk ()
odE \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (descendants_of' p (ctes_of s) \<noteq> {} \<longrightarrow> Q s) \<and> (descendants_of' p (ctes_of s) = {} \<longrightarrow> P () s) \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) p s \<longrightarrow> (mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> (\<forall>ctea. cte_wp_at' ((=) ctea) (mdbNext (cteMDBNode cte)) s \<longrightarrow> (isMDBParentOf cte ctea \<longrightarrow> Q s \<and> True) \<and> (\<not> isMDBParentOf cte ctea \<longrightarrow> P () s))) \<and> (\<not> mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> P () s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<forall>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea \<longrightarrow> (isMDBParentOf cte ctea \<longrightarrow> Q s) \<and> (\<not> isMDBParentOf cte ctea \<longrightarrow> P () s))) \<and> (mdbNext (cteMDBNode cte) = 0 \<longrightarrow> P () s) proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> Q s
 2. \<And>s cte ctea. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; \<not> isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> P () s
 3. \<And>s cte. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> P () s proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea. \<lbrakk>P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea; \<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x\<rbrakk> \<Longrightarrow> Q s
 2. \<And>s cte ctea. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; \<not> isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> P () s
 3. \<And>s cte. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> P () s proof (prove)
goal (5 subgoals):
 1. \<And>s cte ctea. \<lbrakk>P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> ctes_of s \<turnstile> p \<leadsto> ?x29 s cte ctea
 2. \<And>s cte ctea. \<lbrakk>P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> ?x29 s cte ctea \<noteq> 0
 3. \<And>s cte ctea. \<lbrakk>P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> ctes_of s \<turnstile> p parentOf ?x29 s cte ctea
 4. \<And>s cte ctea. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; \<not> isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> P () s
 5. \<And>s cte. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> P () s proof (prove)
goal (4 subgoals):
 1. \<And>s cte ctea. \<lbrakk>P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0
 2. \<And>s cte ctea. \<lbrakk>P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> ctes_of s \<turnstile> p parentOf mdbNext (cteMDBNode cte)
 3. \<And>s cte ctea. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; \<not> isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> P () s
 4. \<And>s cte. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> P () s proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea. \<lbrakk>P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> ctes_of s \<turnstile> p parentOf mdbNext (cteMDBNode cte)
 2. \<And>s cte ctea. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; \<not> isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> P () s
 3. \<And>s cte. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> P () s proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; \<not> isMDBParentOf cte ctea\<rbrakk> \<Longrightarrow> P () s
 2. \<And>s cte. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> P () s proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea x. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; \<not> isMDBParentOf cte ctea; \<not> P () s; ctes_of s \<turnstile> p \<rightarrow> x\<rbrakk> \<Longrightarrow> False
 2. \<And>s cte. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> P () s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; (\<forall>x. \<not> ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> P () s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> P () s proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>(\<exists>x. ctes_of s \<turnstile> p \<rightarrow> x) \<longrightarrow> Q s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) = 0; \<not> P () s; ctes_of s \<turnstile> p \<rightarrow> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!