theory FinalCaps

lemma rec_del_silc_inv_CTEDelete_transferable':
  "\<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot
                    and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)
                    and cdt_change_allowed' aag slot\<rbrace>
   rec_del (CTEDeleteCall slot exposed)
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (cases "is_subject aag (fst slot)") apply (wp rec_del_silc_inv_not_transferable) apply simp apply (subst rec_del.simps[abs_def]) apply (wp add: hoare_K_bind without_preemption_wp empty_slot_silc_inv hoare_weak_lift_imp wp_transferable
                 rec_del_Finalise_transferable
            del: wp_not_transferable
         | wpc)+ apply (rule hoare_post_impErr,rule rec_del_Finalise_transferable) apply force apply force apply (clarsimp) apply (frule(3) cca_to_transferable_or_subject[OF invs_valid_objs invs_mdb]) apply (frule(4) cdt_change_allowed_not_silc[OF invs_valid_objs invs_mdb]) by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall slot exposed) and emptyable (slot_rdcall (CTEDeleteCall slot exposed)) and pas_refined aag and K (case CTEDeleteCall slot exposed of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))) s
 2. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot\<rbrace> rec_del (CTEDeleteCall slot exposed) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot\<rbrace> doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot exposed);
without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info;
returnOk undefined
odE \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> True \<and> (if exposed \<or> xa then \<lambda>s. (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s else (\<lambda>s. silc_inv aag st s \<and> silc_inv aag st s)) s\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; (K (rv = (True, NullCap)) and ?E48) s\<rbrakk> \<Longrightarrow> \<forall>x xa. rv = (x, xa) \<longrightarrow> True \<and> (if exposed \<or> x then \<lambda>s. (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> (silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s else (\<lambda>s. silc_inv aag st s \<and> silc_inv aag st s)) s
 2. \<And>e s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; ?E48 s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 3. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot) s\<rbrakk> \<Longrightarrow> (is_transferable_in slot and ?E48) s proof (prove)
goal (2 subgoals):
 1. \<And>e s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> silc_inv aag st s
 2. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot) s\<rbrakk> \<Longrightarrow> (is_transferable_in slot and (\<lambda>s. silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and emptyable slot and (\<lambda>s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and cdt_change_allowed' aag slot) s\<rbrakk> \<Longrightarrow> (is_transferable_in slot and (\<lambda>s. silc_inv aag st s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; silc_inv aag st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; emptyable slot s; \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s; cdt_change_allowed' aag slot s\<rbrakk> \<Longrightarrow> is_transferable_in slot s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; silc_inv aag st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; emptyable slot s; \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s; cdt_change_allowed' aag slot s; is_subject aag (fst slot) \<or> is_transferable_in slot s\<rbrakk> \<Longrightarrow> is_transferable_in slot s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; silc_inv aag st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; emptyable slot s; \<not> exposed \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s; cdt_change_allowed' aag slot s; is_subject aag (fst slot) \<or> is_transferable_in slot s; pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> is_transferable_in slot s \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel