theory Finalise_R

lemma cap_delete_one_corres:
  "corres dc (einvs and cte_wp_at can_fast_finalise ptr)
        (invs' and cte_at' (cte_map ptr))
        (cap_delete_one ptr) (cteDeleteOne (cte_map ptr))" apply (simp add: cap_delete_one_def cteDeleteOne_def'
                   unless_def when_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule_tac F="can_fast_finalise cap" in corres_gen_asm) apply (rule corres_if) apply fastforce apply (rule corres_split[OF isFinalCapability_corres[where ptr=ptr]]) apply (simp add: split_def bind_assoc [THEN sym]) apply (rule corres_split[OF fast_finaliseCap_corres[where sl=ptr]]) apply simp+ apply (rule emptySlot_corres, simp) apply (wp hoare_drop_imps)+ apply (wp isFinalCapability_inv | wp (once) isFinal[where x="cte_map ptr"])+ apply (rule corres_trivial, simp) apply (wp get_cap_wp getCTE_wp)+ apply (clarsimp simp: cte_wp_at_caps_of_state can_fast_finalise_Null
                  elim!: caps_of_state_valid_cap) apply (clarsimp simp: cte_wp_at_ctes_of) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and cte_wp_at can_fast_finalise ptr) (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) (cap_delete_one ptr) (cteDeleteOne (cte_map ptr)) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and cte_wp_at can_fast_finalise ptr) (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) (do cap <- get_cap ptr;
if cap \<noteq> cap.NullCap then do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot ptr cap.NullCap
od else return ()
od) (do cte <- getCTE (cte_map ptr);
if cteCap cte \<noteq> capability.NullCap then do final <- isFinalCapability cte;
(remainder, info) <- global.finaliseCap (cteCap cte) final True;
y <- assert (capRemovable remainder (cte_map ptr) \<and> info = capability.NullCap);
emptySlot (cte_map ptr) capability.NullCap
od else return ()
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do cap <- get_cap ptr;
if cap \<noteq> cap.NullCap then do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot ptr cap.NullCap
od else return ()
od) (do cte <- getCTE (cte_map ptr);
if cteCap cte \<noteq> capability.NullCap then do final <- isFinalCapability cte;
(remainder, info) <- global.finaliseCap (cteCap cte) final True;
y <- assert (capRemovable remainder (cte_map ptr) \<and> info = capability.NullCap);
emptySlot (cte_map ptr) capability.NullCap
od else return ()
od)
 2. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>cap cte. cap_relation cap (cteCap cte) \<Longrightarrow> corres dc (?R4 cap) (?R'4 cte) (if cap \<noteq> cap.NullCap then do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot ptr cap.NullCap
od else return ()) (if cteCap cte \<noteq> capability.NullCap then do final <- isFinalCapability cte;
(remainder, info) <- global.finaliseCap (cteCap cte) final True;
y <- assert (capRemovable remainder (cte_map ptr) \<and> info = capability.NullCap);
emptySlot (cte_map ptr) capability.NullCap
od else return ())
 2. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>?R'4\<rbrace>
 4. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 5. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?P10 cap) (?R'4 cte) (if cap \<noteq> cap.NullCap then do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot ptr cap.NullCap
od else return ()) (if cteCap cte \<noteq> capability.NullCap then do final <- isFinalCapability cte;
(remainder, info) <- global.finaliseCap (cteCap cte) final True;
y <- assert (capRemovable remainder (cte_map ptr) \<and> info = capability.NullCap);
emptySlot (cte_map ptr) capability.NullCap
od else return ())
 2. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. ?P10 cap and (\<lambda>s. can_fast_finalise cap)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>?R'4\<rbrace>
 4. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 5. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> (cap \<noteq> cap.NullCap) = (cteCap cte \<noteq> capability.NullCap)
 2. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?P13 cap) (?P'16 cte) (do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot ptr cap.NullCap
od) (do final <- isFinalCapability cte;
(remainder, info) <- global.finaliseCap (cteCap cte) final True;
y <- assert (capRemovable remainder (cte_map ptr) \<and> info = capability.NullCap);
emptySlot (cte_map ptr) capability.NullCap
od)
 3. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?Q14 cap) (?Q'17 cte) (return ()) (return ())
 4. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. (if cap \<noteq> cap.NullCap then ?P13 cap else ?Q14 cap) and (\<lambda>s. can_fast_finalise cap)\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?P'16 cte else ?Q'17 cte\<rbrace>
 6. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 7. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?P13 cap) (?P'16 cte) (do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot ptr cap.NullCap
od) (do final <- isFinalCapability cte;
(remainder, info) <- global.finaliseCap (cteCap cte) final True;
y <- assert (capRemovable remainder (cte_map ptr) \<and> info = capability.NullCap);
emptySlot (cte_map ptr) capability.NullCap
od)
 2. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?Q14 cap) (?Q'17 cte) (return ()) (return ())
 3. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. (if cap \<noteq> cap.NullCap then ?P13 cap else ?Q14 cap) and (\<lambda>s. can_fast_finalise cap)\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then ?P'16 cte else ?Q'17 cte\<rbrace>
 5. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 6. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> corres dc (?R27 cap cte final) (?R'27 cap cte finala) (do y <- fast_finalise cap final;
empty_slot ptr cap.NullCap
od) (do (remainder, info) <- global.finaliseCap (cteCap cte) finala True;
y <- assert (capRemovable remainder (cte_map ptr) \<and> info = capability.NullCap);
emptySlot (cte_map ptr) capability.NullCap
od)
 2. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 cap\<rbrace> is_final_cap cap \<lbrace>?R27 cap cte\<rbrace>
 3. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 cte\<rbrace> isFinalCapability cte \<lbrace>?R'27 cap cte\<rbrace>
 4. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?Q14 cap) (?Q'17 cte) (return ()) (return ())
 5. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. (if cap \<noteq> cap.NullCap then invs and cte_wp_at ((=) cap) ptr and ?Q30 cap else ?Q14 cap) and (\<lambda>s. can_fast_finalise cap)\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then invs' and cte_wp_at' ((=) cte) (cte_map ptr) and ?Q'32 cte else ?Q'17 cte\<rbrace>
 7. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 8. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> corres dc (?R27 cap cte final) (?R'27 cap cte finala) (do y <- fast_finalise cap final;
empty_slot ptr cap.NullCap
od) (do y <- do p <- global.finaliseCap (cteCap cte) finala True;
assert (capRemovable (fst p) (cte_map ptr) \<and> snd p = capability.NullCap)
od;
emptySlot (cte_map ptr) capability.NullCap
od)
 2. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 cap\<rbrace> is_final_cap cap \<lbrace>?R27 cap cte\<rbrace>
 3. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 cte\<rbrace> isFinalCapability cte \<lbrace>?R'27 cap cte\<rbrace>
 4. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?Q14 cap) (?Q'17 cte) (return ()) (return ())
 5. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. (if cap \<noteq> cap.NullCap then invs and cte_wp_at ((=) cap) ptr and ?Q30 cap else ?Q14 cap) and (\<lambda>s. can_fast_finalise cap)\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then invs' and cte_wp_at' ((=) cte) (cte_map ptr) and ?Q'32 cte else ?Q'17 cte\<rbrace>
 7. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 8. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (13 subgoals):
 1. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> final_matters' (cteCap cte) \<longrightarrow> final = finala
 2. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> cap_relation cap (cteCap cte)
 3. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> can_fast_finalise cap
 4. \<And>cap cte final finala y ya. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R36 cap cte final finala y) (?R'36 cap cte final finala ya) (empty_slot ptr cap.NullCap) (emptySlot (cte_map ptr) capability.NullCap)
 5. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q40 cap cte final\<rbrace> fast_finalise cap final \<lbrace>?R36 cap cte final finala\<rbrace>
 6. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 cap cte finala\<rbrace> do p <- global.finaliseCap (cteCap cte) finala True;
assert (capRemovable (fst p) (cte_map ptr) \<and> snd p = capability.NullCap)
od \<lbrace>?R'36 cap cte final finala\<rbrace>
 7. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 cap\<rbrace> is_final_cap cap \<lbrace>\<lambda>final. (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap \<and> cte_wp_at ((=) cap) ptr s) and ?Q40 cap cte final\<rbrace>
 8. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>finala. (\<lambda>s. invs' s \<and> valid_cap' (cteCap cte) s) and ?Q'42 cap cte finala\<rbrace>
 9. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?Q14 cap) (?Q'17 cte) (return ()) (return ())
 10. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. (if cap \<noteq> cap.NullCap then invs and cte_wp_at ((=) cap) ptr and ?Q30 cap else ?Q14 cap) and (\<lambda>s. can_fast_finalise cap)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> corres dc (?R36 cap cte final finala ()) (?R'36 cap cte final finala ()) (empty_slot ptr cap.NullCap) (emptySlot (cte_map ptr) capability.NullCap)
 2. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q40 cap cte final\<rbrace> fast_finalise cap final \<lbrace>?R36 cap cte final finala\<rbrace>
 3. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 cap cte finala\<rbrace> do p <- global.finaliseCap (cteCap cte) finala True;
assert (capRemovable (fst p) (cte_map ptr) \<and> snd p = capability.NullCap)
od \<lbrace>?R'36 cap cte final finala\<rbrace>
 4. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 cap\<rbrace> is_final_cap cap \<lbrace>\<lambda>final. (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap \<and> cte_wp_at ((=) cap) ptr s) and ?Q40 cap cte final\<rbrace>
 5. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>finala. (\<lambda>s. invs' s \<and> valid_cap' (cteCap cte) s) and ?Q'42 cap cte finala\<rbrace>
 6. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?Q14 cap) (?Q'17 cte) (return ()) (return ())
 7. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. (if cap \<noteq> cap.NullCap then invs and cte_wp_at ((=) cap) ptr and ?Q30 cap else ?Q14 cap) and (\<lambda>s. can_fast_finalise cap)\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then invs' and cte_wp_at' ((=) cte) (cte_map ptr) and ?Q'32 cte else ?Q'17 cte\<rbrace>
 9. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 10. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q40 cap cte final\<rbrace> fast_finalise cap final \<lbrace>\<lambda>a. einvs and cte_wp_at (\<lambda>_. True) ptr\<rbrace>
 2. \<And>cap cte final finala. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap; final_matters' (cteCap cte) \<longrightarrow> final = finala\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42 cap cte finala\<rbrace> do p <- global.finaliseCap (cteCap cte) finala True;
assert (capRemovable (fst p) (cte_map ptr) \<and> snd p = capability.NullCap)
od \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)\<rbrace>
 3. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q30 cap\<rbrace> is_final_cap cap \<lbrace>\<lambda>final. (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap \<and> cte_wp_at ((=) cap) ptr s) and ?Q40 cap cte final\<rbrace>
 4. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>finala. (\<lambda>s. invs' s \<and> valid_cap' (cteCap cte) s) and ?Q'42 cap cte finala\<rbrace>
 5. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?Q14 cap) (?Q'17 cte) (return ()) (return ())
 6. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. (if cap \<noteq> cap.NullCap then invs and cte_wp_at ((=) cap) ptr and ?Q30 cap else ?Q14 cap) and (\<lambda>s. can_fast_finalise cap)\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then invs' and cte_wp_at' ((=) cte) (cte_map ptr) and ?Q'32 cte else ?Q'17 cte\<rbrace>
 8. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 9. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'32 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>finala s. invs' s \<and> valid_cap' (cteCap cte) s \<and> invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map ptr) s\<rbrace>
 2. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?Q14 cap) (?Q'17 cte) (return ()) (return ())
 3. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. (if cap \<noteq> cap.NullCap then invs and cte_wp_at ((=) cap) ptr and ((\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap \<and> cte_wp_at ((=) cap) ptr s) and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> cte_wp_at (\<lambda>_. True) ptr s)) else ?Q14 cap) and (\<lambda>s. can_fast_finalise cap)\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then invs' and cte_wp_at' ((=) cte) (cte_map ptr) and ?Q'32 cte else ?Q'17 cte\<rbrace>
 5. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 6. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>cap cte. \<lbrakk>cap_relation cap (cteCap cte); can_fast_finalise cap\<rbrakk> \<Longrightarrow> corres dc (?Q14 cap) (?Q'17 cte) (return ()) (return ())
 2. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. (if cap \<noteq> cap.NullCap then invs and cte_wp_at ((=) cap) ptr and ((\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap \<and> cte_wp_at ((=) cap) ptr s) and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> cte_wp_at (\<lambda>_. True) ptr s)) else ?Q14 cap) and (\<lambda>s. can_fast_finalise cap)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then invs' and cte_wp_at' ((=) cte) (cte_map ptr) and (\<lambda>s. invs' s \<and> valid_cap' (cteCap cte) s \<and> invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map ptr) s) else ?Q'17 cte\<rbrace>
 4. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 5. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_cap ptr \<lbrace>\<lambda>cap. (if cap \<noteq> cap.NullCap then invs and cte_wp_at ((=) cap) ptr and ((\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap \<and> cte_wp_at ((=) cap) ptr s) and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> cte_wp_at (\<lambda>_. True) ptr s)) else (\<lambda>_. True)) and (\<lambda>s. can_fast_finalise cap)\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getCTE (cte_map ptr) \<lbrace>\<lambda>cte. if cteCap cte \<noteq> capability.NullCap then invs' and cte_wp_at' ((=) cte) (cte_map ptr) and (\<lambda>s. invs' s \<and> valid_cap' (cteCap cte) s \<and> invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map ptr) s) else (\<lambda>_. True)\<rbrace>
 3. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and ?Q4) s
 4. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and cte_wp_at can_fast_finalise ptr) s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) ptr and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) ptr s \<longrightarrow> ((if cap \<noteq> cap.NullCap then invs and cte_wp_at ((=) cap) ptr and ((\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap \<and> cte_wp_at ((=) cap) ptr s) and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> cte_wp_at (\<lambda>_. True) ptr s)) else (\<lambda>_. True)) and (\<lambda>s. can_fast_finalise cap)) s)) s
 2. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map ptr) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (cte_map ptr) s \<and> (if cteCap cte \<noteq> capability.NullCap then invs' and cte_wp_at' ((=) cte) (cte_map ptr) and (\<lambda>s. invs' s \<and> valid_cap' (cteCap cte) s \<and> invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map ptr) s) else (\<lambda>_. True)) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. cte_wp_at' (\<lambda>_. True) (cte_map ptr) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (cte_map ptr) s \<and> (if cteCap cte \<noteq> capability.NullCap then invs' and cte_wp_at' ((=) cte) (cte_map ptr) and (\<lambda>s. invs' s \<and> valid_cap' (cteCap cte) s \<and> invs' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map ptr) s) else (\<lambda>_. True)) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>invs' s; ctes_of s (cte_map ptr) = Some cte\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<exists>ctea. (cteCap ctea \<noteq> capability.NullCap \<longrightarrow> cte = ctea \<and> valid_cap' (cteCap ctea) s) \<and> (cteCap ctea = capability.NullCap \<longrightarrow> cte = ctea)) proof (prove)
goal:
No subgoals!