theory Finalise_IF

lemma cap_delete_one_reads_respects_f_transferable:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects_f aag l
     (silc_inv aag st and invs and pas_refined aag
                      and K (aag_can_read_not_silc aag (fst slot)) and is_transferable_in slot)
     (cap_delete_one slot)" unfolding cap_delete_one_def fun_app_def apply (unfold unless_def when_def) apply (rule equiv_valid_guard_imp) apply (wp is_final_cap_reads_respects empty_slot_silc_inv
             reads_respects_f[OF empty_slot_reads_respects, where st=st]
             reads_respects_f[OF fast_finalise_reads_respects, where st=st]
          | simp | elim conjE)+ apply (rule_tac Q="\<lambda>rva s. rva = is_final_cap' rv s \<and>
                                 cte_wp_at ((=) rv) slot s \<and>
                                 silc_inv aag st s \<and>
                                 is_transferable_in slot s \<and>
                                 aag_can_read_not_silc aag (fst slot)"
                   in hoare_strengthen_post) apply wp apply (rule conjI) apply clarsimp apply (drule silc_inv) apply (erule_tac x=rv in allE, erule_tac x=slot in allE) apply simp apply (drule(1) intra_label_capD) apply (clarsimp simp: cap_points_to_label_def' cte_wp_at_caps_of_state split: cap.splits) apply (force elim: is_transferable_capE) apply (wp reads_respects_f[OF get_cap_rev] get_cap_wp | simp | elim conjE)+ by (fastforce simp: cte_wp_at_caps_of_state silc_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) (cap_delete_one slot) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) (do cap <- get_cap slot;
unless (cap = NullCap) (do final <- is_final_cap cap;
fast_finalise cap final;
empty_slot slot NullCap
od)
od) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) (do cap <- get_cap slot;
if cap \<noteq> NullCap then do final <- is_final_cap cap;
fast_finalise cap final;
empty_slot slot NullCap
od else return ()
od) proof (prove)
goal (2 subgoals):
 1. reads_respects_f aag l ?Q (do cap <- get_cap slot;
if cap \<noteq> NullCap then do final <- is_final_cap cap;
fast_finalise cap final;
empty_slot slot NullCap
od else return ()
od)
 2. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P'36 rv\<rbrace> is_final_cap rv \<lbrace>\<lambda>rva s. (rva \<longrightarrow> (case rv of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True)) \<and> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrace>
 2. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 3. reads_respects_f aag l ?P'4 (get_cap slot)
 4. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> ?P'36 rv s) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 5. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (6 subgoals):
 1. \<And>rv. rv \<noteq> NullCap \<Longrightarrow> \<lbrace>?P'36 rv\<rbrace> is_final_cap rv \<lbrace>\<lambda>rva s. rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrace>
 2. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> (rva \<longrightarrow> (case rv of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True)) \<and> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
 3. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 4. reads_respects_f aag l ?P'4 (get_cap slot)
 5. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> ?P'36 rv s) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 6. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (5 subgoals):
 1. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> (rva \<longrightarrow> (case rv of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True)) \<and> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
 2. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 3. reads_respects_f aag l ?P'4 (get_cap slot)
 4. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> True \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 5. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> rva \<longrightarrow> (case rv of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True)
 2. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
 3. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 4. reads_respects_f aag l ?P'4 (get_cap slot)
 5. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> True \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 6. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>rv \<noteq> NullCap; cte_wp_at ((=) rv) slot s; silc_inv aag st s; is_transferable_in slot s; aag_can_read aag (fst slot); pasObjectAbs aag (fst slot) \<noteq> SilcLabel; is_final_cap' rv s\<rbrakk> \<Longrightarrow> case rv of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True
 2. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
 3. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 4. reads_respects_f aag l ?P'4 (get_cap slot)
 5. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> True \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 6. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>rv \<noteq> NullCap; cte_wp_at ((=) rv) slot s; is_transferable_in slot s; aag_can_read aag (fst slot); pasObjectAbs aag (fst slot) \<noteq> SilcLabel; is_final_cap' rv s; \<forall>cap slot. cte_wp_at ((=) cap) slot s \<and> is_final_cap' cap s \<longrightarrow> intra_label_cap aag slot s \<or> pasObjectAbs aag (fst slot) = SilcLabel\<rbrakk> \<Longrightarrow> case rv of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True
 2. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
 3. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 4. reads_respects_f aag l ?P'4 (get_cap slot)
 5. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> True \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 6. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>rv \<noteq> NullCap; cte_wp_at ((=) rv) slot s; is_transferable_in slot s; aag_can_read aag (fst slot); pasObjectAbs aag (fst slot) \<noteq> SilcLabel; is_final_cap' rv s; cte_wp_at ((=) rv) slot s \<and> is_final_cap' rv s \<longrightarrow> intra_label_cap aag slot s \<or> pasObjectAbs aag (fst slot) = SilcLabel\<rbrakk> \<Longrightarrow> case rv of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True
 2. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
 3. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 4. reads_respects_f aag l ?P'4 (get_cap slot)
 5. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> True \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 6. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>rv \<noteq> NullCap; cte_wp_at ((=) rv) slot s; is_transferable_in slot s; aag_can_read aag (fst slot); pasObjectAbs aag (fst slot) \<noteq> SilcLabel; is_final_cap' rv s; intra_label_cap aag slot s\<rbrakk> \<Longrightarrow> case rv of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True
 2. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
 3. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 4. reads_respects_f aag l ?P'4 (get_cap slot)
 5. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> True \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 6. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>rv \<noteq> NullCap; cte_wp_at ((=) rv) slot s; is_transferable_in slot s; aag_can_read aag (fst slot); pasObjectAbs aag (fst slot) \<noteq> SilcLabel; is_final_cap' rv s; cap_points_to_label aag rv (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> case rv of EndpointCap r badge rights \<Rightarrow> aag_can_read aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True
 2. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
 3. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 4. reads_respects_f aag l ?P'4 (get_cap slot)
 5. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> True \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 6. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>rv \<noteq> NullCap; caps_of_state s slot = Some rv; is_transferable_cap rv; aag_can_read aag (fst slot); pasObjectAbs aag (fst slot) \<noteq> SilcLabel; is_final_cap' rv s; \<forall>x\<in>gen_obj_refs rv. pasGenAbs aag x = pasObjectAbs aag (fst slot)\<rbrakk> \<Longrightarrow> (\<forall>x31. (\<exists>x32 x33. rv = EndpointCap x31 x32 x33) \<longrightarrow> aag_can_read aag x31) \<and> (\<forall>x41. (\<exists>x42 x43. rv = NotificationCap x41 x42 x43) \<longrightarrow> is_subject aag x41)
 2. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
 3. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 4. reads_respects_f aag l ?P'4 (get_cap slot)
 5. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> True \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 6. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (5 subgoals):
 1. \<And>rv rva s. \<lbrakk>rv \<noteq> NullCap; rva = is_final_cap' rv s \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> ?Q12 rv rva s \<and> silc_inv aag st s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel
 2. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 3. reads_respects_f aag l ?P'4 (get_cap slot)
 4. \<lbrace>?P''4\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv \<noteq> NullCap \<longrightarrow> (silc_inv aag (?st28 rv) and (\<lambda>s. cte_wp_at ((=) rv) (?slot28 rv) s \<and> aag_can_read aag (fst (?slot28 rv)) \<and> pasObjectAbs aag (fst (?slot28 rv)) \<noteq> SilcLabel)) s \<and> silc_inv aag st s \<and> (pas_refined aag and invs) s \<and> True \<and> cte_wp_at ((=) rv) slot s \<and> silc_inv aag st s \<and> is_transferable_in slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 5. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) and is_transferable_in slot) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; aag_can_read aag (fst slot); pasObjectAbs aag (fst slot) \<noteq> SilcLabel; is_transferable_in slot s\<rbrakk> \<Longrightarrow> silc_inv aag ?st85 s \<and> ((\<exists>cap. cte_wp_at ((=) cap) slot s) \<longrightarrow> silc_inv aag ?st85 s) \<and> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag (?st28 cap) s \<and> cte_wp_at ((=) cap) (?slot28 cap) s \<and> aag_can_read aag (fst (?slot28 cap)) \<and> pasObjectAbs aag (fst (?slot28 cap)) \<noteq> SilcLabel)