theory Untyped_AI

lemma create_cap_overlap_reserved [wp]:
 "\<lbrace>caps_overlap_reserved (untyped_range c) and
   K (cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}) and
   cte_wp_at ((\<noteq>) cap.NullCap) p and
   cte_wp_at ((=) cap.NullCap) cref and
   valid_mdb and K (cap_aligned (default_cap tp oref sz dev))\<rbrace>
  create_cap tp sz p dev (cref,oref)
  \<lbrace>\<lambda>rv s. caps_overlap_reserved (untyped_range c) s\<rbrace>" apply (simp add: create_cap_def caps_overlap_reserved_def cte_wp_at_caps_of_state set_cdt_def) apply (wp set_cap_caps_of_state2 | simp del: fun_upd_apply)+ apply (clarsimp simp: ran_def split: if_splits) apply (case_tac "cref = (a,b)") apply simp apply (erule(1) disjoint_subset[OF usable_range_subseteq]) apply (simp add:Int_ac cap_range_inter_emptyD) apply simp apply (erule(2) caps_overlap_reservedD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>caps_overlap_reserved (untyped_range c) and K (cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}) and cte_wp_at ((\<noteq>) NullCap) p and cte_wp_at ((=) NullCap) cref and valid_mdb and K (cap_aligned (default_cap tp oref sz dev))\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. caps_overlap_reserved (untyped_range c)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>caps_overlap_reserved (untyped_range c) and (\<lambda>y. cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}) and cte_wp_at ((\<noteq>) NullCap) p and cte_wp_at ((=) NullCap) cref and valid_mdb and (\<lambda>y. cap_aligned (default_cap tp oref sz dev))\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := cdt(cref \<mapsto> p)\<rparr>)
od;
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> untyped_range c = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. caps_overlap_reserved (untyped_range c) s \<and> cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {} \<and> cte_wp_at ((\<noteq>) NullCap) p s \<and> cte_wp_at ((=) NullCap) cref s \<and> valid_mdb s \<and> cap_aligned (default_cap tp oref sz dev) \<Longrightarrow> \<forall>cap\<in>ran ((caps_of_state s)(cref \<mapsto> default_cap tp oref sz dev)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> untyped_range c = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>caps_overlap_reserved (untyped_range c) s; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) NullCap) cref s; valid_mdb s; cap_aligned (default_cap tp oref sz dev); (a, b) = cref \<longrightarrow> default_cap tp oref sz dev = cap; (a, b) \<noteq> cref \<longrightarrow> caps_of_state s (a, b) = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> untyped_range c = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cap a b. \<lbrakk>caps_overlap_reserved (untyped_range c) s; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) NullCap) cref s; valid_mdb s; cap_aligned (default_cap tp oref sz dev); (a, b) = cref \<longrightarrow> default_cap tp oref sz dev = cap; (a, b) \<noteq> cref \<longrightarrow> caps_of_state s (a, b) = Some cap; is_untyped_cap cap; cref = (a, b)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> untyped_range c = {}
 2. \<And>s cap a b. \<lbrakk>caps_overlap_reserved (untyped_range c) s; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) NullCap) cref s; valid_mdb s; cap_aligned (default_cap tp oref sz dev); (a, b) = cref \<longrightarrow> default_cap tp oref sz dev = cap; (a, b) \<noteq> cref \<longrightarrow> caps_of_state s (a, b) = Some cap; is_untyped_cap cap; cref \<noteq> (a, b)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> untyped_range c = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cap a b. \<lbrakk>caps_overlap_reserved (untyped_range c) s; cap_range c \<inter> untyped_range cap = {}; cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) NullCap) (a, b) s; valid_mdb s; cap_aligned cap; default_cap tp oref sz dev = cap; is_untyped_cap cap; cref = (a, b)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> untyped_range c = {}
 2. \<And>s cap a b. \<lbrakk>caps_overlap_reserved (untyped_range c) s; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) NullCap) cref s; valid_mdb s; cap_aligned (default_cap tp oref sz dev); (a, b) = cref \<longrightarrow> default_cap tp oref sz dev = cap; (a, b) \<noteq> cref \<longrightarrow> caps_of_state s (a, b) = Some cap; is_untyped_cap cap; cref \<noteq> (a, b)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> untyped_range c = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cap a b. \<lbrakk>caps_overlap_reserved (untyped_range c) s; cap_range c \<inter> untyped_range cap = {}; cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) NullCap) (a, b) s; valid_mdb s; default_cap tp oref sz dev = cap; is_untyped_cap cap; cref = (a, b)\<rbrakk> \<Longrightarrow> untyped_range cap \<inter> untyped_range c = {}
 2. \<And>s cap a b. \<lbrakk>caps_overlap_reserved (untyped_range c) s; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) NullCap) cref s; valid_mdb s; cap_aligned (default_cap tp oref sz dev); (a, b) = cref \<longrightarrow> default_cap tp oref sz dev = cap; (a, b) \<noteq> cref \<longrightarrow> caps_of_state s (a, b) = Some cap; is_untyped_cap cap; cref \<noteq> (a, b)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> untyped_range c = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>caps_overlap_reserved (untyped_range c) s; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) NullCap) cref s; valid_mdb s; cap_aligned (default_cap tp oref sz dev); (a, b) = cref \<longrightarrow> default_cap tp oref sz dev = cap; (a, b) \<noteq> cref \<longrightarrow> caps_of_state s (a, b) = Some cap; is_untyped_cap cap; cref \<noteq> (a, b)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> untyped_range c = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>caps_overlap_reserved (untyped_range c) s; cap_range c \<inter> cap_range (default_cap tp oref sz dev) = {}; cte_wp_at ((\<noteq>) NullCap) p s; cte_wp_at ((=) NullCap) cref s; valid_mdb s; cap_aligned (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; is_untyped_cap cap; cref \<noteq> (a, b)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> untyped_range c = {} proof (prove)
goal:
No subgoals!