theory Untyped_AI

lemma delete_objects_ex_cte_cap_wp_to:
  notes untyped_range.simps[simp del]
  shows
  "\<lbrace>ex_cte_cap_wp_to P slot and invs and
      cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> {ptr_base .. ptr_base + 2 ^ sz - 1} \<subseteq> untyped_range cp)
          src_slot and (\<lambda>s. descendants_of src_slot (cdt s) = {})\<rbrace>
    delete_objects ptr_base sz
   \<lbrace>\<lambda>rv s. ex_cte_cap_wp_to P slot s\<rbrace>" apply (simp add: delete_objects_def ex_cte_cap_wp_to_def) apply (rule hoare_pre) apply (rule hoare_lift_Pf2 [where f="interrupt_irq_node"]) apply (wp hoare_vcg_ex_lift | simp)+ apply (clarsimp simp: cte_wp_at_caps_of_state) apply (intro exI conjI, assumption+) apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+) apply (case_tac "the (caps_of_state s src_slot)", simp_all) apply (frule ex_cte_cap_protects, simp add: cte_wp_at_caps_of_state,
    rule empty_descendants_range_in, (assumption | clarsimp)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P slot and invs and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> {ptr_base..ptr_base + 2 ^ sz - 1} \<subseteq> untyped_range cp) src_slot and (\<lambda>s. descendants_of src_slot (cdt s) = {})\<rbrace> delete_objects ptr_base sz \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> slot \<in> cte_refs c (interrupt_irq_node s)) (a, b) s) and invs and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> {ptr_base..ptr_base + 2 ^ sz - 1} \<subseteq> untyped_range cp) src_slot and (\<lambda>s. descendants_of src_slot (cdt s) = {})\<rbrace> do y <- do_machine_op (freeMemory ptr_base sz);
modify (detype {ptr_base..ptr_base + 2 ^ sz - 1})
od \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> slot \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- do_machine_op (freeMemory ptr_base sz);
modify (detype {ptr_base..ptr_base + 2 ^ sz - 1})
od \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> slot \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> slot \<in> cte_refs c (interrupt_irq_node s)) (a, b) s) and invs and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> {ptr_base..ptr_base + 2 ^ sz - 1} \<subseteq> untyped_range cp) src_slot and (\<lambda>s. descendants_of src_slot (cdt s) = {})) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?Q3 x\<rbrace> do y <- do_machine_op (freeMemory ptr_base sz);
modify (detype {ptr_base..ptr_base + 2 ^ sz - 1})
od \<lbrace>\<lambda>_ a. \<exists>aa b. cte_wp_at (\<lambda>c. P c \<and> slot \<in> cte_refs c x) (aa, b) a\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> do y <- do_machine_op (freeMemory ptr_base sz);
modify (detype {ptr_base..ptr_base + 2 ^ sz - 1})
od \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace>
 3. \<And>s. ((\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> slot \<in> cte_refs c (interrupt_irq_node s)) (a, b) s) and invs and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> {ptr_base..ptr_base + 2 ^ sz - 1} \<subseteq> untyped_range cp) src_slot and (\<lambda>s. descendants_of src_slot (cdt s) = {})) s \<Longrightarrow> ?Q3 (interrupt_irq_node s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>a b. cte_wp_at (\<lambda>c. P c \<and> slot \<in> cte_refs c (interrupt_irq_node s)) (a, b) s) \<and> invs s \<and> cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> {ptr_base..ptr_base + 2 ^ sz - 1} \<subseteq> untyped_range cp) src_slot s \<and> descendants_of src_slot (cdt s) = {} \<Longrightarrow> \<exists>x. (\<exists>xa. cte_wp_at (\<lambda>a. P a \<and> slot \<in> cte_refs a (interrupt_irq_node s)) (x, xa) s) \<and> (ptr_base \<le> x \<longrightarrow> \<not> x \<le> ptr_base + 2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap capa. \<lbrakk>invs s; caps_of_state s (a, b) = Some cap; descendants_of src_slot (cdt s) = {}; P cap; slot \<in> cte_refs cap (interrupt_irq_node s); caps_of_state s src_slot = Some capa; is_untyped_cap capa; {ptr_base..ptr_base + 2 ^ sz - 1} \<subseteq> untyped_range capa\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>xa cap. caps_of_state s (x, xa) = Some cap \<and> P cap \<and> slot \<in> cte_refs cap (interrupt_irq_node s)) \<and> (ptr_base \<le> x \<longrightarrow> \<not> x \<le> ptr_base + 2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap capa. \<lbrakk>invs s; caps_of_state s (a, b) = Some cap; descendants_of src_slot (cdt s) = {}; P cap; slot \<in> cte_refs cap (interrupt_irq_node s); caps_of_state s src_slot = Some capa; is_untyped_cap capa; {ptr_base..ptr_base + 2 ^ sz - 1} \<subseteq> untyped_range capa\<rbrakk> \<Longrightarrow> ptr_base \<le> a \<longrightarrow> \<not> a \<le> ptr_base + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap capa. \<lbrakk>invs s; caps_of_state s (a, b) = Some cap; descendants_of src_slot (cdt s) = {}; P cap; slot \<in> cte_refs cap (interrupt_irq_node s); caps_of_state s src_slot = Some capa; is_untyped_cap capa; {ptr_base..ptr_base + 2 ^ sz - 1} \<subseteq> untyped_range capa; ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s; ptr_base \<le> a; a \<le> ptr_base + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap capa x21 x22 x23 x24. \<lbrakk>invs s; caps_of_state s (a, b) = Some cap; descendants_of src_slot (cdt s) = {}; P cap; slot \<in> cte_refs cap (interrupt_irq_node s); caps_of_state s src_slot = Some (UntypedCap x21 x22 x23 x24); {ptr_base..ptr_base + 2 ^ sz - 1} \<subseteq> untyped_range (UntypedCap x21 x22 x23 x24); ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s; ptr_base \<le> a; a \<le> ptr_base + 2 ^ sz - 1; capa = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!