theory Untyped_AI

lemma lookup_cap_ex:
  "\<lbrace>valid_objs\<rbrace> lookup_cap t x \<lbrace>\<lambda>rv s. valid_objs s \<and>
                                (\<exists>p1 p2 m c'. rv = mask_cap m c' \<and>
                                  cte_wp_at (\<lambda>c. c = c') (p1, p2) s)\<rbrace>,-" apply (simp add: lookup_cap_def split_def) apply wp apply (rule_tac P1=wellformed_cap in hoare_strengthen_post[OF get_cap_cte_wp_at_P]) apply clarsimp apply (rule exI)+ apply (subst cap_mask_UNIV, simp) apply fastforce apply (wpsimp|strengthen cte_wp_at_wellformed_strengthen)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_cap t x \<lbrace>\<lambda>rv s. valid_objs s \<and> (\<exists>p1 p2 m c'. rv = mask_cap m c' \<and> cte_wp_at (\<lambda>c. c = c') (p1, p2) s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> doE p <- lookup_slot_for_thread t x;
liftE (get_cap (fst p))
odE \<lbrace>\<lambda>rv s. valid_objs s \<and> (\<exists>p1 p2 m c'. rv = mask_cap m c' \<and> cte_wp_at (\<lambda>c. c = c') (p1, p2) s)\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrace>?P'4 p\<rbrace> get_cap (fst p) \<lbrace>\<lambda>rv s. \<exists>p1 p2 m c'. rv = mask_cap m c' \<and> cte_wp_at (\<lambda>c. c = c') (p1, p2) s\<rbrace>
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t x \<lbrace>\<lambda>p s. valid_objs s \<and> ?P'4 p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>p rv s. cte_wp_at (\<lambda>c. c = rv) (fst p) s \<and> wellformed_cap rv \<Longrightarrow> \<exists>p1 p2 m c'. rv = mask_cap m c' \<and> cte_wp_at (\<lambda>c. c = c') (p1, p2) s
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t x \<lbrace>\<lambda>p s. valid_objs s \<and> cte_wp_at wellformed_cap (fst p) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>a b rv s. \<lbrakk>cte_wp_at (\<lambda>c. c = rv) (a, b) s; wellformed_cap rv\<rbrakk> \<Longrightarrow> \<exists>p1 p2 m c'. rv = mask_cap m c' \<and> cte_wp_at (\<lambda>c. c = c') (p1, p2) s
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t x \<lbrace>\<lambda>p s. valid_objs s \<and> cte_wp_at wellformed_cap (fst p) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>a b rv s. \<lbrakk>cte_wp_at (\<lambda>c. c = rv) (a, b) s; wellformed_cap rv\<rbrakk> \<Longrightarrow> rv = mask_cap (?m15 a b rv s) (?c'17 a b rv s) \<and> cte_wp_at (\<lambda>c. c = ?c'17 a b rv s) (?p1.11 a b rv s, ?p2.13 a b rv s) s
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t x \<lbrace>\<lambda>p s. valid_objs s \<and> cte_wp_at wellformed_cap (fst p) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>a b rv s. \<lbrakk>cte_wp_at (\<lambda>c. c = rv) (a, b) s; wellformed_cap rv\<rbrakk> \<Longrightarrow> rv = rv \<and> cte_wp_at (\<lambda>c. c = rv) (?p1.20 a b rv s (?a20 a b rv s) (?b20 a b rv s) rv s, ?p2.20 a b rv s (?a20 a b rv s) (?b20 a b rv s) rv s) s
 2. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t x \<lbrace>\<lambda>p s. valid_objs s \<and> cte_wp_at wellformed_cap (fst p) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> lookup_slot_for_thread t x \<lbrace>\<lambda>p s. valid_objs s \<and> cte_wp_at wellformed_cap (fst p) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!