theory Finalise_AI

lemma cap_delete_one_deletes_reply:
  "\<lbrace>cte_wp_at (is_reply_cap_to t) slot and valid_reply_caps\<rbrace>
    cap_delete_one slot
   \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace>" apply (simp add: cap_delete_one_def unless_def is_final_cap_def) apply wp apply (rule_tac Q="\<lambda>rv s. \<forall>sl' R. if (sl' = slot)
                               then cte_wp_at (\<lambda>c. c = cap.NullCap) sl' s
                               else caps_of_state s sl' \<noteq> Some (cap.ReplyCap t False R)"
                  in hoare_post_imp) apply (clarsimp simp add: has_reply_cap_def is_reply_cap_to_def cte_wp_at_caps_of_state
                      simp del: split_paired_All split_paired_Ex
                         split: if_split_asm elim!: allEI) apply (rule hoare_vcg_all_lift) apply simp apply (wp hoare_weak_lift_imp empty_slot_deletes empty_slot_caps_of_state get_cap_wp)+ apply (fastforce simp: cte_wp_at_caps_of_state valid_reply_caps_def
                        is_cap_simps unique_reply_caps_def is_reply_cap_to_def
              simp del: split_paired_All) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (is_reply_cap_to t) slot and valid_reply_caps\<rbrace> cap_delete_one slot \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (is_reply_cap_to t) slot and valid_reply_caps\<rbrace> do cap <- get_cap slot;
when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot slot NullCap
od)
od \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap final y. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B4 cap final y\<rbrace> empty_slot slot NullCap \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace>
 2. \<And>cap final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 3. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> gets (is_final_cap' cap) \<lbrace>?B3 cap\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> NullCap then ?Q2 cap else (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 5. \<And>s. (cte_wp_at (is_reply_cap_to t) slot and valid_reply_caps) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cap final y rv s. \<lbrakk>cap \<noteq> NullCap; \<forall>sl' R. if sl' = slot then cte_wp_at (\<lambda>c. c = NullCap) sl' s else caps_of_state s sl' \<noteq> Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> \<not> has_reply_cap t s
 2. \<And>cap final y. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B4 cap final y\<rbrace> empty_slot slot NullCap \<lbrace>\<lambda>rv s. \<forall>sl' R. if sl' = slot then cte_wp_at (\<lambda>c. c = NullCap) sl' s else caps_of_state s sl' \<noteq> Some (ReplyCap t False R)\<rbrace>
 3. \<And>cap final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 4. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> gets (is_final_cap' cap) \<lbrace>?B3 cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> NullCap then ?Q2 cap else (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 6. \<And>s. (cte_wp_at (is_reply_cap_to t) slot and valid_reply_caps) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap final y. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B4 cap final y\<rbrace> empty_slot slot NullCap \<lbrace>\<lambda>rv s. \<forall>sl' R. if sl' = slot then cte_wp_at (\<lambda>c. c = NullCap) sl' s else caps_of_state s sl' \<noteq> Some (ReplyCap t False R)\<rbrace>
 2. \<And>cap final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> fast_finalise cap final \<lbrace>?B4 cap final\<rbrace>
 3. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> gets (is_final_cap' cap) \<lbrace>?B3 cap\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> NullCap then ?Q2 cap else (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 5. \<And>s. (cte_wp_at (is_reply_cap_to t) slot and valid_reply_caps) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap final y sl'. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?P28 cap final y sl'\<rbrace> empty_slot slot NullCap \<lbrace>\<lambda>rv s. \<forall>R. if sl' = slot then cte_wp_at (\<lambda>c. c = NullCap) sl' s else caps_of_state s sl' \<noteq> Some (ReplyCap t False R)\<rbrace>
 2. \<And>cap final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> fast_finalise cap final \<lbrace>\<lambda>y s. \<forall>x. ?P28 cap final y x s\<rbrace>
 3. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> gets (is_final_cap' cap) \<lbrace>?B3 cap\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> NullCap then ?Q2 cap else (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 5. \<And>s. (cte_wp_at (is_reply_cap_to t) slot and valid_reply_caps) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap final sl'. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?P28 cap final () sl'\<rbrace> empty_slot slot NullCap \<lbrace>\<lambda>rv s. (sl' = slot \<longrightarrow> cte_wp_at (\<lambda>c. c = NullCap) slot s) \<and> (sl' \<noteq> slot \<longrightarrow> (\<forall>R. caps_of_state s sl' \<noteq> Some (ReplyCap t False R)))\<rbrace>
 2. \<And>cap final. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B3 cap final\<rbrace> fast_finalise cap final \<lbrace>\<lambda>y s. \<forall>x. ?P28 cap final y x s\<rbrace>
 3. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> gets (is_final_cap' cap) \<lbrace>?B3 cap\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_cap slot \<lbrace>\<lambda>cap. if cap \<noteq> NullCap then ?Q2 cap else (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 5. \<And>s. (cte_wp_at (is_reply_cap_to t) slot and valid_reply_caps) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at (is_reply_cap_to t) slot and valid_reply_caps) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (if cap \<noteq> NullCap then \<lambda>s. \<forall>x. (x = slot \<longrightarrow> True) \<and> (x \<noteq> slot \<longrightarrow> (\<forall>R. ((caps_of_state s)(slot \<mapsto> NullCap)) x \<noteq> Some (ReplyCap t False R))) else (\<lambda>s. \<not> has_reply_cap t s)) s proof (prove)
goal:
No subgoals!