theory CSpace_R

lemma locateSlot_cap_to'[wp]:
  "\<lbrace>\<lambda>s. isCNodeCap cap \<and> (\<forall>r \<in> cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace>
     locateSlotCNode (capCNodePtr cap) n (v && mask (capCNodeBits cap))
   \<lbrace>ex_cte_cap_wp_to' P\<rbrace>" apply (simp add: locateSlot_conv) apply wp apply (clarsimp dest!: isCapDs valid_capAligned
                   simp: objBits_simps' mult.commute capAligned_def cte_level_bits_def) apply (erule bspec) apply (case_tac "bits < word_bits") apply simp apply (rule and_mask_less_size) apply (simp add: word_bits_def word_size) apply (simp add: power_overflow word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. isCNodeCap cap \<and> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> locateSlotCNode (capCNodePtr cap) n (v && mask (capCNodeBits cap)) \<lbrace>ex_cte_cap_wp_to' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. isCNodeCap cap \<and> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> do x <- stateAssert (\<lambda>s. case gsCNodes s (capCNodePtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask (capCNodeBits cap) < 2 ^ na) [];
return (capCNodePtr cap + 2 ^ cte_level_bits * (v && mask (capCNodeBits cap)))
od \<lbrace>ex_cte_cap_wp_to' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. isCNodeCap cap \<and> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s) \<Longrightarrow> (case gsCNodes s (capCNodePtr cap) of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask (capCNodeBits cap) < 2 ^ na) \<longrightarrow> ex_cte_cap_wp_to' P (capCNodePtr cap + 2 ^ cte_level_bits * (v && mask (capCNodeBits cap))) s proof (prove)
goal (1 subgoal):
 1. \<And>s ptr bits grd gsize. \<lbrakk>\<forall>r\<in>{0..2 ^ bits - 1}. ex_cte_cap_wp_to' P (ptr + r * 0x10) s; cap = capability.CNodeCap ptr bits grd gsize; case gsCNodes s ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask bits < 2 ^ na\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' P (ptr + (v && mask bits) * 0x10) s proof (prove)
goal (1 subgoal):
 1. \<And>s ptr bits grd gsize. \<lbrakk>cap = capability.CNodeCap ptr bits grd gsize; case gsCNodes s ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask bits < 2 ^ na\<rbrakk> \<Longrightarrow> v && mask bits \<in> {0..2 ^ bits - 1} proof (prove)
goal (2 subgoals):
 1. \<And>s ptr bits grd gsize. \<lbrakk>cap = capability.CNodeCap ptr bits grd gsize; case gsCNodes s ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask bits < 2 ^ na; bits < word_bits\<rbrakk> \<Longrightarrow> v && mask bits \<in> {0..2 ^ bits - 1}
 2. \<And>s ptr bits grd gsize. \<lbrakk>cap = capability.CNodeCap ptr bits grd gsize; case gsCNodes s ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask bits < 2 ^ na; \<not> bits < word_bits\<rbrakk> \<Longrightarrow> v && mask bits \<in> {0..2 ^ bits - 1} proof (prove)
goal (2 subgoals):
 1. \<And>s ptr bits grd gsize. \<lbrakk>cap = capability.CNodeCap ptr bits grd gsize; case gsCNodes s ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask bits < 2 ^ na; bits < word_bits\<rbrakk> \<Longrightarrow> v && mask bits < 2 ^ bits
 2. \<And>s ptr bits grd gsize. \<lbrakk>cap = capability.CNodeCap ptr bits grd gsize; case gsCNodes s ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask bits < 2 ^ na; \<not> bits < word_bits\<rbrakk> \<Longrightarrow> v && mask bits \<in> {0..2 ^ bits - 1} proof (prove)
goal (2 subgoals):
 1. \<And>s ptr bits grd gsize. \<lbrakk>cap = capability.CNodeCap ptr bits grd gsize; case gsCNodes s ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask bits < 2 ^ na; bits < word_bits\<rbrakk> \<Longrightarrow> bits < size v
 2. \<And>s ptr bits grd gsize. \<lbrakk>cap = capability.CNodeCap ptr bits grd gsize; case gsCNodes s ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask bits < 2 ^ na; \<not> bits < word_bits\<rbrakk> \<Longrightarrow> v && mask bits \<in> {0..2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s ptr bits grd gsize. \<lbrakk>cap = capability.CNodeCap ptr bits grd gsize; case gsCNodes s ptr of None \<Rightarrow> False | Some na \<Rightarrow> na = n \<and> v && mask bits < 2 ^ na; \<not> bits < word_bits\<rbrakk> \<Longrightarrow> v && mask bits \<in> {0..2 ^ bits - 1} proof (prove)
goal:
No subgoals!