theory Finalise_IF

lemma rec_del_Finalise_transferable_read_respects_f:
  "reads_respects_f aag l
     (silc_inv aag st and is_transferable_in slot and K(aag_can_read_not_silc aag (fst slot)))
     (rec_del (FinaliseSlotCall slot exposed))" apply (subst rec_del.simps[abs_def]) apply (wp | wpc | simp)+ apply ((wp ev_pre_cont hoare_pre_cont)+)[3] apply simp apply (wp liftE_ev finalise_cap_transferable_ev | simp)+ apply (rule hoare_post_imp[OF _ finalise_cap_transferable[where P=\<top>]], fastforce) apply (wpsimp wp: is_final_cap_reads_respects hoare_drop_imp get_cap_wp
                        reads_respects_f[OF get_cap_rev, where st=st and Q="\<top>"])+ by (fastforce simp: cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and is_transferable_in slot and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) (rec_del (FinaliseSlotCall slot exposed)) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and is_transferable_in slot and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) (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) proof (prove)
goal (10 subgoals):
 1. \<And>rv rva rvb x1 x2. \<lbrakk>rv \<noteq> NullCap; rvb = (x1, x2); \<not> cap_removeable x1 slot; cap_cyclic_zombie x1 slot \<and> \<not> exposed\<rbrakk> \<Longrightarrow> reads_respects_f aag l (?P'17 rv rva (x1, x2) x1 x2) (set_cap x1 slot)
 2. \<And>rv rva rvb x1 x2. \<lbrakk>rv \<noteq> NullCap; rvb = (x1, x2); \<not> cap_removeable x1 slot; cap_cyclic_zombie x1 slot \<and> \<not> exposed\<rbrakk> \<Longrightarrow> \<lbrace>?P''17 rv rva rvb x1 x2\<rbrace> without_preemption $ set_cap x1 slot \<lbrace>\<lambda>rvc _. True\<rbrace>, -
 3. \<And>rv rva rvb x1 x2. \<lbrakk>rv \<noteq> NullCap; rvb = (x1, x2); \<not> cap_removeable x1 slot; \<not> (cap_cyclic_zombie x1 slot \<and> \<not> exposed)\<rbrakk> \<Longrightarrow> reads_respects_f aag l (?Q16 rv rva rvb x1 x2) (doE without_preemption $ set_cap x1 slot;
rec_del (ReduceZombieCall x1 slot exposed);
preemption_point;
rec_del (FinaliseSlotCall slot exposed)
odE)
 4. \<And>rv rva. rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?P'4 rv rva) (without_preemption $ finalise_cap rv rva)
 5. \<And>rv rva. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. \<forall>x xa. rvb = (x, xa) \<longrightarrow> (cap_removeable x slot \<longrightarrow> True) \<and> (\<not> cap_removeable x slot \<longrightarrow> (cap_cyclic_zombie x slot \<and> \<not> exposed \<longrightarrow> ?P'17 rv rva rvb x xa s \<and> ?P''17 rv rva rvb x xa s) \<and> (\<not> (cap_cyclic_zombie x slot \<and> \<not> exposed) \<longrightarrow> ?Q16 rv rva rvb x xa s))\<rbrace>, -
 6. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?P'3 rv) (without_preemption $ is_final_cap rv)
 7. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>, -
 8. reads_respects_f aag l ?P' (without_preemption $ get_cap slot)
 9. \<lbrace>?P''\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'3 rv s \<and> ?P''3 rv s)\<rbrace>, -
 10. \<And>s. (silc_inv aag st and is_transferable_in slot and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (7 subgoals):
 1. \<And>rv rva. rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?P'4 rv rva) (without_preemption $ finalise_cap rv rva)
 2. \<And>rv rva. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. \<forall>x xa. rvb = (x, xa) \<longrightarrow> (cap_removeable x slot \<longrightarrow> True) \<and> (\<not> cap_removeable x slot \<longrightarrow> (cap_cyclic_zombie x slot \<and> \<not> exposed \<longrightarrow> False \<and> False) \<and> (\<not> (cap_cyclic_zombie x slot \<and> \<not> exposed) \<longrightarrow> False))\<rbrace>, -
 3. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?P'3 rv) (without_preemption $ is_final_cap rv)
 4. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>, -
 5. reads_respects_f aag l ?P' (without_preemption $ get_cap slot)
 6. \<lbrace>?P''\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'3 rv s \<and> ?P''3 rv s)\<rbrace>, -
 7. \<And>s. (silc_inv aag st and is_transferable_in slot and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (7 subgoals):
 1. \<And>rv rva. rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?P'4 rv rva) (liftE (finalise_cap rv rva))
 2. \<And>rv rva. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> without_preemption $ finalise_cap rv rva \<lbrace>\<lambda>rvb s. \<forall>x xa. rvb = (x, xa) \<longrightarrow> (cap_removeable x slot \<longrightarrow> True) \<and> (\<not> cap_removeable x slot \<longrightarrow> (cap_cyclic_zombie x slot \<and> \<not> exposed \<longrightarrow> False \<and> False) \<and> (\<not> (cap_cyclic_zombie x slot \<and> \<not> exposed) \<longrightarrow> False))\<rbrace>, -
 3. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?P'3 rv) (without_preemption $ is_final_cap rv)
 4. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>, -
 5. reads_respects_f aag l ?P' (without_preemption $ get_cap slot)
 6. \<lbrace>?P''\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'3 rv s \<and> ?P''3 rv s)\<rbrace>, -
 7. \<And>s. (silc_inv aag st and is_transferable_in slot and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rvb s. \<forall>x. (\<exists>xa. rvb = (x, xa)) \<longrightarrow> \<not> cap_removeable x slot \<longrightarrow> (cap_cyclic_zombie x slot \<longrightarrow> exposed) \<and> cap_cyclic_zombie x slot \<and> \<not> exposed\<rbrace>
 2. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?P'3 rv) (without_preemption $ is_final_cap rv)
 3. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. K (is_transferable_cap rv) s \<and> ?P''4 rv rva s\<rbrace>, -
 4. reads_respects_f aag l ?P' (without_preemption $ get_cap slot)
 5. \<lbrace>?P''\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'3 rv s \<and> ?P''3 rv s)\<rbrace>, -
 6. \<And>s. (silc_inv aag st and is_transferable_in slot and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (5 subgoals):
 1. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?P'3 rv) (without_preemption $ is_final_cap rv)
 2. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> without_preemption $ is_final_cap rv \<lbrace>\<lambda>rva s. K (is_transferable_cap rv) s \<and> ((\<lambda>_. True) and K (is_transferable_cap rv)) s\<rbrace>, -
 3. reads_respects_f aag l ?P' (without_preemption $ get_cap slot)
 4. \<lbrace>?P''\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (rv \<noteq> NullCap \<longrightarrow> ?P'3 rv s \<and> ?P''3 rv s)\<rbrace>, -
 5. \<And>s. (silc_inv aag st and is_transferable_in slot and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>silc_inv aag st s; is_transferable_in slot s; aag_can_read aag (fst slot); pasObjectAbs aag (fst slot) \<noteq> SilcLabel; cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow> silc_inv aag (?st77 cap) s \<and> cte_wp_at ((=) cap) (?slot77 cap) s \<and> aag_can_read aag (fst (?slot77 cap)) \<and> pasObjectAbs aag (fst (?slot77 cap)) \<noteq> SilcLabel \<and> is_transferable_cap cap