theory Delete_C

lemma cteDelete_invs'':
  "\<lbrace>invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_to' ptr s)\<rbrace> cteDelete ptr ex \<lbrace>\<lambda>rv. invs'\<rbrace>" 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 valid_validE_R, rule finaliseSlot_invs) 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 clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)\<rbrace> cteDelete ptr ex \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)\<rbrace> doE p <- finaliseSlot ptr ex;
if ex \<or> fst p then liftE (emptySlot ptr (snd p)) else returnOk ()
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'10\<rbrace> finaliseSlot ptr ex \<lbrace>\<lambda>p s. (ex \<or> fst p \<longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s \<and> (\<forall>sl'. snd p \<noteq> capability.NullCap \<longrightarrow> sl' \<noteq> ptr \<longrightarrow> cteCaps_of s sl' \<noteq> Some (snd p))) \<and> (\<not> (ex \<or> fst p) \<longrightarrow> invs' s)\<rbrace>, -
 2. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'10 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'10\<rbrace> finaliseSlot ptr ex \<lbrace>?Q'13\<rbrace>, -
 2. \<And>rv s. ?Q'13 rv s \<Longrightarrow> (ex \<or> fst rv \<longrightarrow> invs' s \<and> 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> (\<not> (ex \<or> fst rv) \<longrightarrow> invs' s)
 3. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'10 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'10\<rbrace> finaliseSlot ptr ex \<lbrace>?Q'13\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. ?Q'13 rv s \<Longrightarrow> (ex \<or> fst rv \<longrightarrow> invs' s \<and> 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> (\<not> (ex \<or> fst rv) \<longrightarrow> invs' s)
 3. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'10 s proof (prove)
goal (3 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>?P'10\<rbrace> finaliseSlot ptr ex \<lbrace>?Q'13\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. ?Q'13 rv s \<Longrightarrow> (ex \<or> fst rv \<longrightarrow> invs' s \<and> 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> (\<not> (ex \<or> fst rv) \<longrightarrow> invs' s)
 3. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'10 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrace>?P19\<rbrace> finaliseSlot ptr ex \<lbrace>?Q21\<rbrace>, -
 2. \<And>s. s \<turnstile> \<lbrace>?P'20\<rbrace> finaliseSlot ptr ex \<lbrace>?Q'22\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s. ?Q21 rv s \<and> ?Q'22 rv s \<Longrightarrow> (ex \<or> fst rv \<longrightarrow> invs' s \<and> 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> (\<not> (ex \<or> fst rv) \<longrightarrow> invs' s)
 4. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P19 s \<and> ?P'20 s proof (prove)
goal (3 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>?P'20\<rbrace> finaliseSlot ptr ex \<lbrace>?Q'22\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. invs' s \<and> ?Q'22 rv s \<Longrightarrow> (ex \<or> fst rv \<longrightarrow> invs' s \<and> 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> (\<not> (ex \<or> fst rv) \<longrightarrow> invs' s)
 3. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'20 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrace>?P32\<rbrace> finaliseSlot ptr ex \<lbrace>?Q34\<rbrace>, -
 2. \<And>s. s \<turnstile> \<lbrace>?P'33\<rbrace> finaliseSlot ptr ex \<lbrace>?Q'35\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s. invs' s \<and> ?Q34 rv s \<and> ?Q'35 rv s \<Longrightarrow> (ex \<or> fst rv \<longrightarrow> invs' s \<and> 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> (\<not> (ex \<or> fst rv) \<longrightarrow> invs' s)
 4. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P32 s \<and> ?P'33 s proof (prove)
goal (3 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>?P'33\<rbrace> finaliseSlot ptr ex \<lbrace>?Q'35\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. invs' s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s) \<and> ?Q'35 rv s \<Longrightarrow> (ex \<or> fst rv \<longrightarrow> invs' s \<and> 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> (\<not> (ex \<or> fst rv) \<longrightarrow> invs' s)
 3. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'33 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrace>?P42\<rbrace> finaliseSlot ptr ex \<lbrace>?Q44\<rbrace>, -
 2. \<And>s. s \<turnstile> \<lbrace>?P'43\<rbrace> finaliseSlot ptr ex \<lbrace>?Q'45\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv s. invs' s \<and> (fst rv \<longrightarrow> cte_wp_at' (\<lambda>cte. removeable' ptr s (cteCap cte)) ptr s) \<and> ?Q44 rv s \<and> ?Q'45 rv s \<Longrightarrow> (ex \<or> fst rv \<longrightarrow> invs' s \<and> 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> (\<not> (ex \<or> fst rv) \<longrightarrow> invs' s)
 4. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P42 s \<and> ?P'43 s proof (prove)
goal (3 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>?P'43\<rbrace> finaliseSlot ptr ex \<lbrace>?Q'45\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. invs' s \<and> (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'45 rv s \<Longrightarrow> (ex \<or> fst rv \<longrightarrow> invs' s \<and> 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> (\<not> (ex \<or> fst rv) \<longrightarrow> invs' s)
 3. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> ?P'43 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. invs' s \<and> (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> ex \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr) ptr s) \<Longrightarrow> (ex \<or> fst rv \<longrightarrow> invs' s \<and> 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> (\<not> (ex \<or> fst rv) \<longrightarrow> invs' s)
 2. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and sch_act_simple and (\<lambda>s. ex \<or> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) s \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> (invs' s \<and> sch_act_simple s \<and> (\<not> ex \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) \<and> True proof (prove)
goal:
No subgoals!