theory Untyped_AI

lemma set_free_index_invs_UntypedCap:
  "\<lbrace>\<lambda>s. invs s \<and> (\<exists>cap. free_index_of cap \<le> idx
        \<and> is_untyped_cap cap \<and> idx \<le> 2^cap_bits cap
        \<and> free_index_update (\<lambda>_. idx) cap = UntypedCap dev ptr sz idx
        \<and> cte_wp_at ((=) cap) cref s)\<rbrace>
   set_cap (UntypedCap dev ptr sz idx) cref
   \<lbrace>\<lambda>rv s'. invs s'\<rbrace>" apply (rule hoare_name_pre_state) apply clarsimp apply (cut_tac cap=cap and idx=idx in set_free_index_invs) apply clarsimp apply (erule hoare_pre) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (case_tac cap, simp_all add: free_index_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> (\<exists>cap. free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap \<and> free_index_update (\<lambda>_. idx) cap = UntypedCap dev ptr sz idx \<and> cte_wp_at ((=) cap) cref s)\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> (\<exists>cap. free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap \<and> free_index_update (\<lambda>_. idx) cap = UntypedCap dev ptr sz idx \<and> cte_wp_at ((=) cap) cref s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>invs s; free_index_of cap \<le> idx; is_untyped_cap cap; idx \<le> 2 ^ cap_bits cap; free_index_update (\<lambda>_. idx) cap = UntypedCap dev ptr sz idx; cte_wp_at ((=) cap) cref s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>invs s; free_index_of cap \<le> idx; is_untyped_cap cap; idx \<le> 2 ^ cap_bits cap; free_index_update (\<lambda>_. idx) cap = UntypedCap dev ptr sz idx; cte_wp_at ((=) cap) cref s; \<lbrace>\<lambda>sa. (free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap) \<and> invs sa \<and> cte_wp_at (\<lambda>cp. \<exists>ptr sz dev idx' idx''. idx' \<le> idx \<and> cp = UntypedCap dev ptr sz idx' \<and> cap = UntypedCap dev ptr sz idx'') (?cref8 s cap) sa\<rbrace> set_cap (free_index_update (\<lambda>_. idx) cap) (?cref8 s cap) \<lbrace>\<lambda>rv. invs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>invs s; free_index_of cap \<le> idx; is_untyped_cap cap; idx \<le> 2 ^ cap_bits cap; free_index_update (\<lambda>_. idx) cap = UntypedCap dev ptr sz idx; cte_wp_at ((=) cap) cref s; \<lbrace>\<lambda>sa. invs sa \<and> cte_wp_at (\<lambda>cp. \<exists>ptr sz dev idx'. idx' \<le> idx \<and> cp = UntypedCap dev ptr sz idx' \<and> (\<exists>idx''. cap = UntypedCap dev ptr sz idx'')) (?cref8 s cap) sa\<rbrace> set_cap (UntypedCap dev ptr sz idx) (?cref8 s cap) \<lbrace>\<lambda>rv. invs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cap sa. \<lbrakk>invs s; free_index_of cap \<le> idx; is_untyped_cap cap; idx \<le> 2 ^ cap_bits cap; free_index_update (\<lambda>_. idx) cap = UntypedCap dev ptr sz idx; cte_wp_at ((=) cap) cref s; s = sa\<rbrakk> \<Longrightarrow> invs sa \<and> cte_wp_at (\<lambda>cp. \<exists>ptr sz dev idx'. idx' \<le> idx \<and> cp = UntypedCap dev ptr sz idx' \<and> (\<exists>idx''. cap = UntypedCap dev ptr sz idx'')) cref sa proof (prove)
goal (1 subgoal):
 1. \<And>cap sa. \<lbrakk>invs sa; free_index_of cap \<le> idx; is_untyped_cap cap; idx \<le> 2 ^ cap_bits cap; free_index_update (\<lambda>_. idx) cap = UntypedCap dev ptr sz idx; caps_of_state sa cref = Some cap\<rbrakk> \<Longrightarrow> \<exists>ptr sz dev idx'. idx' \<le> idx \<and> cap = UntypedCap dev ptr sz idx' \<and> (\<exists>idx''. cap = UntypedCap dev ptr sz idx'') proof (prove)
goal:
No subgoals!