theory CNodeInv_R

lemma cteDelete_invs':
  "\<lbrace>invs' and sch_act_simple and K ex\<rbrace> cteDelete ptr ex \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: cteDelete_def whenE_def split_def) apply (rule hoare_pre, wp finaliseSlot_invs) apply (rule hoare_post_imp_R) apply (unfold validE_R_def) apply (rule use_spec) apply (rule spec_valid_conj_liftE1) apply (rule finaliseSlot_removeable) apply (rule spec_valid_conj_liftE1) apply (rule finaliseSlot_irqs) apply (rule finaliseSlot_abort_cases'[folded finaliseSlot_def]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and K ex\<rbrace> cteDelete ptr ex \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. ex \<Longrightarrow> \<lbrace>invs' and sch_act_simple\<rbrace> cteDelete ptr ex \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. ex \<Longrightarrow> \<lbrace>invs' and sch_act_simple\<rbrace> doE p <- finaliseSlot ptr True;
liftE (emptySlot ptr (snd p))
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. ex \<Longrightarrow> \<lbrace>?P'12\<rbrace> finaliseSlot ptr True \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))\<rbrace>, -
 2. \<And>s. \<lbrakk>ex; (invs' and sch_act_simple) s\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'12 s proof (prove)
goal (3 subgoals):
 1. ex \<Longrightarrow> \<lbrace>?P'12\<rbrace> finaliseSlot ptr True \<lbrace>?Q'15\<rbrace>, -
 2. \<And>rv s. \<lbrakk>ex; ?Q'15 rv s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))
 3. \<And>s. \<lbrakk>ex; (invs' and sch_act_simple) s\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'12 s proof (prove)
goal (3 subgoals):
 1. ex \<Longrightarrow> \<lbrace>?P'12\<rbrace> finaliseSlot ptr True \<lbrace>?Q'15\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. \<lbrakk>ex; ?Q'15 rv s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))
 3. \<And>s. \<lbrakk>ex; (invs' and sch_act_simple) s\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'12 s proof (prove)
goal (3 subgoals):
 1. \<And>s. ex \<Longrightarrow> s \<turnstile> \<lbrace>?P'12\<rbrace> finaliseSlot ptr True \<lbrace>?Q'15\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. \<lbrakk>ex; ?Q'15 rv s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))
 3. \<And>s. \<lbrakk>ex; (invs' and sch_act_simple) s\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'12 s proof (prove)
goal (4 subgoals):
 1. \<And>s. ex \<Longrightarrow> \<lbrace>?P21\<rbrace> finaliseSlot ptr True \<lbrace>?Q23\<rbrace>, -
 2. \<And>s. ex \<Longrightarrow> s \<turnstile> \<lbrace>?P'22\<rbrace> finaliseSlot ptr True \<lbrace>?Q'24\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s. \<lbrakk>ex; ?Q23 rv s \<and> ?Q'24 rv s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))
 4. \<And>s. \<lbrakk>ex; (invs' and sch_act_simple) s\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P21 s \<and> ?P'22 s proof (prove)
goal (3 subgoals):
 1. \<And>s. ex \<Longrightarrow> s \<turnstile> \<lbrace>?P'22\<rbrace> finaliseSlot ptr True \<lbrace>?Q'24\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. \<lbrakk>ex; (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s) \<and> ?Q'24 rv s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))
 3. \<And>s. \<lbrakk>ex; (invs' and sch_act_simple) s\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'22 s proof (prove)
goal (4 subgoals):
 1. \<And>s. ex \<Longrightarrow> \<lbrace>?P31\<rbrace> finaliseSlot ptr True \<lbrace>?Q33\<rbrace>, -
 2. \<And>s. ex \<Longrightarrow> s \<turnstile> \<lbrace>?P'32\<rbrace> finaliseSlot ptr True \<lbrace>?Q'34\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s. \<lbrakk>ex; (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s) \<and> ?Q33 rv s \<and> ?Q'34 rv s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))
 4. \<And>s. \<lbrakk>ex; (invs' and sch_act_simple) s\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P31 s \<and> ?P'32 s proof (prove)
goal (3 subgoals):
 1. \<And>s. ex \<Longrightarrow> s \<turnstile> \<lbrace>?P'32\<rbrace> finaliseSlot ptr True \<lbrace>?Q'34\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. \<lbrakk>ex; (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s) \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)) \<and> ?Q'34 rv s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))
 3. \<And>s. \<lbrakk>ex; (invs' and sch_act_simple) s\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'32 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>ex; (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s) \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv)) \<and> (fst rv \<or> \<not> True \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr) ptr s)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. snd rv \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd rv))
 2. \<And>s. \<lbrakk>ex; (invs' and sch_act_simple) s\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ex; (invs' and sch_act_simple) s\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> True proof (prove)
goal:
No subgoals!