theory Retype_AC

lemma set_free_index_invs':
  "\<lbrace>(\<lambda>s. invs s \<and> cte_wp_at ((=) cap) slot s \<and>
         (free_index_of cap \<le> idx' \<or>
          (descendants_range_in {word1..word1 + 2 ^ (bits_of cap) - 1} slot s \<and>
          pspace_no_overlap_range_cover word1 (bits_of cap) s)) \<and>
         idx' \<le> 2 ^ cap_bits cap \<and> is_untyped_cap cap) and
    K (word1 = obj_ref_of cap \<and> dev = (cap_is_device cap))\<rbrace>
   set_cap (UntypedCap dev word1 (bits_of cap) idx') slot
   \<lbrace>\<lambda>_. invs \<rbrace>" apply (rule hoare_gen_asm) apply (case_tac cap, simp_all add: bits_of_def) apply (case_tac "free_index_of cap \<le> idx'") apply simp apply (cut_tac cap=cap and cref=slot and idx="idx'" in set_free_index_invs) apply (simp add: free_index_of_def) apply (rule hoare_weaken_pre, assumption, fastforce elim: cte_wp_at_weakenE) apply simp apply (wp set_untyped_cap_invs_simple | simp)+ apply (fastforce simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. invs s \<and> cte_wp_at ((=) cap) slot s \<and> (free_index_of cap \<le> idx' \<or> descendants_range_in {word1..word1 + 2 ^ bits_of cap - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 (bits_of cap)) s) \<and> idx' \<le> 2 ^ cap_bits cap \<and> is_untyped_cap cap) and K (word1 = obj_ref_of cap \<and> dev = cap_is_device cap)\<rbrace> set_cap (UntypedCap dev word1 (bits_of cap) idx') slot \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. word1 = obj_ref_of cap \<and> dev = cap_is_device cap \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) cap) slot s \<and> (free_index_of cap \<le> idx' \<or> descendants_range_in {word1..word1 + 2 ^ bits_of cap - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 (bits_of cap)) s) \<and> idx' \<le> 2 ^ cap_bits cap \<and> is_untyped_cap cap\<rbrace> set_cap (UntypedCap dev word1 (bits_of cap) idx') slot \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> (free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx' \<or> descendants_range_in {word1..word1 + 2 ^ x23 - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 x23) s) \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; free_index_of cap \<le> idx'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> (free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx' \<or> descendants_range_in {word1..word1 + 2 ^ x23 - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 x23) s) \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; \<not> free_index_of cap \<le> idx'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> (free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx' \<or> descendants_range_in {word1..word1 + 2 ^ x23 - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 x23) s) \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; \<not> free_index_of cap \<le> idx'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> (free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx' \<or> descendants_range_in {word1..word1 + 2 ^ x23 - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 x23) s) \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx'; \<lbrace>\<lambda>s. (free_index_of cap \<le> idx' \<and> is_untyped_cap cap \<and> idx' \<le> 2 ^ cap_bits cap) \<and> invs s \<and> cte_wp_at (\<lambda>cp. \<exists>ptr sz dev idx'a idx''. idx'a \<le> idx' \<and> cp = UntypedCap dev ptr sz idx'a \<and> cap = UntypedCap dev ptr sz idx'') slot s\<rbrace> set_cap (free_index_update (\<lambda>_. idx') cap) slot \<lbrace>\<lambda>rv. invs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; \<not> free_index_of cap \<le> idx'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> (free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx' \<or> descendants_range_in {word1..word1 + 2 ^ x23 - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 x23) s) \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; x24 \<le> idx'; \<lbrace>\<lambda>s. idx' \<le> 2 ^ x23 \<and> invs s \<and> cte_wp_at (\<lambda>cp. \<exists>idx'a\<le>idx'. cp = UntypedCap x21 word1 x23 idx'a) slot s\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>rv. invs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; \<not> free_index_of cap \<le> idx'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> (free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx' \<or> descendants_range_in {word1..word1 + 2 ^ x23 - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 x23) s) \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; \<not> free_index_of cap \<le> idx'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> (free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx' \<or> descendants_range_in {word1..word1 + 2 ^ x23 - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 x23) s) \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x21 x23 x24. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; \<not> free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> descendants_range_in {word1..word1 + 2 ^ x23 - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 x23) s \<and> idx' \<le> 2 ^ x23\<rbrace> set_cap (UntypedCap x21 word1 x23 idx') slot \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x21 x23 x24 s. \<lbrakk>dev = x21; cap = UntypedCap x21 word1 x23 x24; \<not> free_index_of (UntypedCap x21 word1 x23 x24) \<le> idx'; invs s \<and> cte_wp_at ((=) (UntypedCap x21 word1 x23 x24)) slot s \<and> descendants_range_in {word1..word1 + 2 ^ x23 - 1} slot s \<and> pspace_no_overlap (up_aligned_area word1 x23) s \<and> idx' \<le> 2 ^ x23\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = x23 \<and> cap_is_device c = x21 \<and> obj_ref_of c = word1) slot s proof (prove)
goal:
No subgoals!