theory ArchArch_AI

lemma set_cap_idx_up_aligned_area:
  "\<lbrace>K (\<exists>idx. pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at ((=) pcap) slot
      and valid_objs\<rbrace> set_cap (max_free_index_update pcap) slot
  \<lbrace>\<lambda>rv s. (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr pageBits \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s)\<rbrace>" apply (rule hoare_pre) apply (wp hoare_vcg_ex_lift set_cap_cte_wp_at) apply (rule_tac x = slot in exI) apply clarsimp apply (frule(1) cte_wp_valid_cap) apply (clarsimp simp: cte_wp_at_caps_of_state p_assoc_help valid_cap_def valid_untyped_def cap_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (\<exists>idx. pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at ((=) pcap) slot and valid_objs\<rbrace> set_cap (max_free_index_update pcap) slot \<lbrace>\<lambda>rv s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr pageBits \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap (max_free_index_update pcap) slot \<lbrace>\<lambda>rv s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr pageBits \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s\<rbrace>
 2. \<And>s. (K (\<exists>idx. pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at ((=) pcap) slot and valid_objs) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (K (\<exists>idx. pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at ((=) pcap) slot and valid_objs) s \<Longrightarrow> \<exists>x. ((\<lambda>s. if x = slot then up_aligned_area ptr pageBits \<subseteq> cap_range (max_free_index_update pcap) \<and> cap_is_device (max_free_index_update pcap) = dev else cte_wp_at (\<lambda>c. up_aligned_area ptr pageBits \<subseteq> cap_range c \<and> cap_is_device c = dev) x s) and cte_wp_at (\<lambda>_. True) slot) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (K (\<exists>idx. pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at ((=) pcap) slot and valid_objs) s \<Longrightarrow> ((\<lambda>s. if slot = slot then up_aligned_area ptr pageBits \<subseteq> cap_range (max_free_index_update pcap) \<and> cap_is_device (max_free_index_update pcap) = dev else cte_wp_at (\<lambda>c. up_aligned_area ptr pageBits \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) and cte_wp_at (\<lambda>_. True) slot) s proof (prove)
goal (1 subgoal):
 1. \<And>s idx. \<lbrakk>pcap = UntypedCap dev ptr pageBits idx; cte_wp_at ((=) (UntypedCap dev ptr pageBits idx)) slot s; valid_objs s\<rbrakk> \<Longrightarrow> (ptr \<le> (ptr && ~~ mask pageBits) + (2 ^ pageBits - 1) \<longrightarrow> (ptr && ~~ mask pageBits) + (2 ^ pageBits - 1) \<le> ptr + 2 ^ pageBits - 1) \<and> cte_wp_at (\<lambda>_. True) slot s proof (prove)
goal (1 subgoal):
 1. \<And>s idx. \<lbrakk>pcap = UntypedCap dev ptr pageBits idx; cte_wp_at ((=) (UntypedCap dev ptr pageBits idx)) slot s; valid_objs s; s \<turnstile> UntypedCap dev ptr pageBits idx\<rbrakk> \<Longrightarrow> (ptr \<le> (ptr && ~~ mask pageBits) + (2 ^ pageBits - 1) \<longrightarrow> (ptr && ~~ mask pageBits) + (2 ^ pageBits - 1) \<le> ptr + 2 ^ pageBits - 1) \<and> cte_wp_at (\<lambda>_. True) slot s proof (prove)
goal:
No subgoals!