theory Finalise_AC

lemma rec_del_Finalise_transferable:
  "\<lbrace>(\<lambda>s. is_transferable (caps_of_state s slot)) and P\<rbrace>
   rec_del (FinaliseSlotCall slot exposed)
   \<lbrace>\<lambda>rv. K (rv = (True,NullCap)) and P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>" apply (subst rec_del.simps[abs_def]) apply (wp hoare_K_bind | wpc )+ apply ((simp only: validE_R_def validE_E_def)?, rule hoare_FalseE) apply ((simp only: validE_R_def validE_E_def)?, rule hoare_FalseE) apply ((simp only: validE_R_def validE_E_def)?, rule hoare_FalseE) apply (wp without_preemption_wp) apply (rule hoare_post_imp[of "\<lambda>rv s. rv = (NullCap,NullCap) \<and> P s" for P]) apply (clarsimp; assumption) apply (wp finalise_cap_transferable without_preemption_wp get_cap_wp)+ by (fastforce simp:cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_transferable_in slot and P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>rv. K (rv = (True, NullCap)) and P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_transferable_in slot and P\<rbrace> doE cap <- without_preemption $ get_cap slot;
if cap = NullCap then returnOk (True, NullCap) else doE is_final <- without_preemption $ is_final_cap cap;
(remainder, cleanup_info) <- without_preemption $ finalise_cap cap is_final;
if cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> exposed then doE without_preemption $ set_cap remainder slot;
returnOk (False, NullCap)
odE else doE without_preemption $ set_cap remainder slot;
rec_del (ReduceZombieCall remainder slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE
odE
odE \<lbrace>\<lambda>rv. K (rv = (True, NullCap)) and P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cap is_final x x1 x2 xa. \<lbrakk>cap \<noteq> NullCap; x = (x1, x2); \<not> cap_removeable x1 slot; cap_cyclic_zombie x1 slot \<and> \<not> exposed\<rbrakk> \<Longrightarrow> \<lbrace>?P'20 cap is_final x x1 x2 xa\<rbrace> K_bind (returnOk (False, NullCap)) xa \<lbrace>\<lambda>rv s. K (rv = (True, NullCap)) s \<and> P s\<rbrace>, -
 2. \<And>cap is_final x x1 x2. \<lbrakk>cap \<noteq> NullCap; x = (x1, x2); \<not> cap_removeable x1 slot; cap_cyclic_zombie x1 slot \<and> \<not> exposed\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 cap is_final x x1 x2\<rbrace> without_preemption $ set_cap x1 slot \<lbrace>\<lambda>xa s. P s \<and> ?P'20 cap is_final x x1 x2 xa s\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>cap is_final x x1 x2. \<lbrakk>cap \<noteq> NullCap; x = (x1, x2); \<not> cap_removeable x1 slot; \<not> (cap_cyclic_zombie x1 slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> \<lbrace>?R18 cap is_final x x1 x2\<rbrace> doE without_preemption $ set_cap x1 slot;
rec_del (ReduceZombieCall x1 slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE \<lbrace>\<lambda>rv s. K (rv = (True, NullCap)) s \<and> P s\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>cap is_final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B5 cap is_final\<rbrace> without_preemption $ finalise_cap cap is_final \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> (cap_removeable xa slot \<longrightarrow> K ((True, xb) = (True, NullCap)) s \<and> P s) \<and> (\<not> cap_removeable xa slot \<longrightarrow> (cap_cyclic_zombie xa slot \<and> \<not> exposed \<longrightarrow> ?Q18 cap is_final x xa xb s) \<and> (\<not> (cap_cyclic_zombie xa slot \<and> \<not> exposed) \<longrightarrow> ?R18 cap is_final x xa xb s))\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R3 cap\<rbrace> without_preemption $ is_final_cap cap \<lbrace>?B5 cap\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<lbrace>?Q\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> K ((True, NullCap) = (True, NullCap)) s \<and> P s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R3 cap s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cap is_final x x1 x2. \<lbrakk>cap \<noteq> NullCap; x = (x1, x2); \<not> cap_removeable x1 slot; cap_cyclic_zombie x1 slot \<and> \<not> exposed\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 cap is_final x x1 x2\<rbrace> without_preemption $ set_cap x1 slot \<lbrace>\<lambda>xa s. P s \<and> False\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>cap is_final x x1 x2. \<lbrakk>cap \<noteq> NullCap; x = (x1, x2); \<not> cap_removeable x1 slot; \<not> (cap_cyclic_zombie x1 slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> \<lbrace>?R18 cap is_final x x1 x2\<rbrace> doE without_preemption $ set_cap x1 slot;
rec_del (ReduceZombieCall x1 slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE \<lbrace>\<lambda>rv s. K (rv = (True, NullCap)) s \<and> P s\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>cap is_final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B5 cap is_final\<rbrace> without_preemption $ finalise_cap cap is_final \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> (cap_removeable xa slot \<longrightarrow> K ((True, xb) = (True, NullCap)) s \<and> P s) \<and> (\<not> cap_removeable xa slot \<longrightarrow> (cap_cyclic_zombie xa slot \<and> \<not> exposed \<longrightarrow> ?Q18 cap is_final x xa xb s) \<and> (\<not> (cap_cyclic_zombie xa slot \<and> \<not> exposed) \<longrightarrow> ?R18 cap is_final x xa xb s))\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R3 cap\<rbrace> without_preemption $ is_final_cap cap \<lbrace>?B5 cap\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<lbrace>?Q\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> K ((True, NullCap) = (True, NullCap)) s \<and> P s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R3 cap s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap is_final x x1 x2. \<lbrakk>cap \<noteq> NullCap; x = (x1, x2); \<not> cap_removeable x1 slot; \<not> (cap_cyclic_zombie x1 slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> \<lbrace>?R18 cap is_final x x1 x2\<rbrace> doE without_preemption $ set_cap x1 slot;
rec_del (ReduceZombieCall x1 slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE \<lbrace>\<lambda>rv s. K (rv = (True, NullCap)) s \<and> P s\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>cap is_final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B5 cap is_final\<rbrace> without_preemption $ finalise_cap cap is_final \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> (cap_removeable xa slot \<longrightarrow> K ((True, xb) = (True, NullCap)) s \<and> P s) \<and> (\<not> cap_removeable xa slot \<longrightarrow> (cap_cyclic_zombie xa slot \<and> \<not> exposed \<longrightarrow> False) \<and> (\<not> (cap_cyclic_zombie xa slot \<and> \<not> exposed) \<longrightarrow> ?R18 cap is_final x xa xb s))\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R3 cap\<rbrace> without_preemption $ is_final_cap cap \<lbrace>?B5 cap\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<lbrace>?Q\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> K ((True, NullCap) = (True, NullCap)) s \<and> P s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R3 cap s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cap is_final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B5 cap is_final\<rbrace> without_preemption $ finalise_cap cap is_final \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> (cap_removeable xa slot \<longrightarrow> K ((True, xb) = (True, NullCap)) s \<and> P s) \<and> (\<not> cap_removeable xa slot \<longrightarrow> (cap_cyclic_zombie xa slot \<and> \<not> exposed \<longrightarrow> False) \<and> (\<not> (cap_cyclic_zombie xa slot \<and> \<not> exposed) \<longrightarrow> False))\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R3 cap\<rbrace> without_preemption $ is_final_cap cap \<lbrace>?B5 cap\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<lbrace>?Q\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> K ((True, NullCap) = (True, NullCap)) s \<and> P s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R3 cap s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cap is_final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?P'29 cap is_final\<rbrace> finalise_cap cap is_final \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> (cap_removeable xa slot \<longrightarrow> K ((True, xb) = (True, NullCap)) s \<and> P s) \<and> (\<not> cap_removeable xa slot \<longrightarrow> (cap_cyclic_zombie xa slot \<and> \<not> exposed \<longrightarrow> False) \<and> (\<not> (cap_cyclic_zombie xa slot \<and> \<not> exposed) \<longrightarrow> False))\<rbrace>
 2. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R3 cap\<rbrace> without_preemption $ is_final_cap cap \<lbrace>\<lambda>is_final s. True \<and> ?P'29 cap is_final s\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<lbrace>?Q\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> K ((True, NullCap) = (True, NullCap)) s \<and> P s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R3 cap s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap is_final rv s. \<lbrakk>cap \<noteq> NullCap; rv = (NullCap, NullCap) \<and> ?Pa42 cap is_final s\<rbrakk> \<Longrightarrow> \<forall>x xa. rv = (x, xa) \<longrightarrow> (cap_removeable x slot \<longrightarrow> K ((True, xa) = (True, NullCap)) s \<and> P s) \<and> (\<not> cap_removeable x slot \<longrightarrow> (cap_cyclic_zombie x slot \<and> \<not> exposed \<longrightarrow> False) \<and> (\<not> (cap_cyclic_zombie x slot \<and> \<not> exposed) \<longrightarrow> False))
 2. \<And>cap is_final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?P'29 cap is_final\<rbrace> finalise_cap cap is_final \<lbrace>\<lambda>rv s. rv = (NullCap, NullCap) \<and> ?Pa42 cap is_final s\<rbrace>
 3. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R3 cap\<rbrace> without_preemption $ is_final_cap cap \<lbrace>\<lambda>is_final s. True \<and> ?P'29 cap is_final s\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<lbrace>?Q\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> K ((True, NullCap) = (True, NullCap)) s \<and> P s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R3 cap s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 5. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cap is_final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?P'29 cap is_final\<rbrace> finalise_cap cap is_final \<lbrace>\<lambda>rv s. rv = (NullCap, NullCap) \<and> P s\<rbrace>
 2. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R3 cap\<rbrace> without_preemption $ is_final_cap cap \<lbrace>\<lambda>is_final s. True \<and> ?P'29 cap is_final s\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 3. \<lbrace>?Q\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> K ((True, NullCap) = (True, NullCap)) s \<and> P s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R3 cap s)\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> True) \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (cap = NullCap \<longrightarrow> K ((True, NullCap) = (True, NullCap)) s \<and> P s) \<and> (cap \<noteq> NullCap \<longrightarrow> True \<and> True \<and> (P and K (is_transferable_cap cap)) s))