theory Finalise_IF

lemma cap_delete_one_reads_respects_f:
  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 (is_subject aag (fst 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
            reads_respects_f[OF empty_slot_reads_respects, where st=st]
            reads_respects_f[OF fast_finalise_reads_respects, where st=st]
            empty_slot_silc_inv
        | 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_subject aag (fst slot) \<and>
                                 pasObjectAbs aag (fst slot) \<noteq> SilcLabel"
                   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 split: cap.splits) apply force apply (wp reads_respects_f[OF get_cap_rev] get_cap_auth_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 (is_subject aag (fst 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 (is_subject aag (fst 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 (is_subject aag (fst 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 (is_subject aag (fst 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 (is_subject aag (fst 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_subject 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_subject 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 (is_subject aag (fst 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_subject 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_subject 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 (is_subject aag (fst 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_subject 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_subject 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_subject 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 (is_subject aag (fst 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_subject aag (fst slot); pasSubject aag \<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_subject 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_subject 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 (is_subject aag (fst 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_subject aag (fst slot); pasSubject aag \<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_subject 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_subject 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 (is_subject aag (fst 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_subject aag (fst slot); pasSubject aag \<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_subject 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_subject 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 (is_subject aag (fst 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_subject aag (fst slot); pasSubject aag \<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_subject 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_subject 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 (is_subject aag (fst 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_subject aag (fst slot); pasSubject aag \<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_subject 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_subject 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 (is_subject aag (fst 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_subject 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_subject 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 (is_subject aag (fst slot))) s \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<not> rv \<noteq> NullCap \<Longrightarrow> reads_respects_f aag l (?Q5 rv) (return ())
 2. reads_respects_f aag l ?P'4 (get_cap slot)
 3. \<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_subject aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel) \<and> (\<not> rv \<noteq> NullCap \<longrightarrow> ?Q5 rv s)\<rbrace>
 4. \<And>s. (silc_inv aag st and invs and pas_refined aag and K (is_subject aag (fst 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; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> silc_inv aag ?st76 s \<and> pas_refined ?aag79 s \<and> is_subject ?aag79 (fst slot) \<and> ((\<exists>cap. caps_of_state s slot = Some cap \<and> pas_cap_cur_auth ?aag79 cap) \<longrightarrow> silc_inv aag ?st76 s) \<and> pas_refined ?aag85 s \<and> is_subject ?aag85 (fst slot) \<and> (\<forall>cap. caps_of_state s slot = Some cap \<and> pas_cap_cur_auth ?aag85 cap \<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 \<and> cte_wp_at ((=) cap) slot s \<and> pasSubject aag \<noteq> SilcLabel)