theory FinalCaps

lemma get_thread_cap_ret_is_subject:
  "\<lbrace>(pas_refined aag) and K (is_subject aag (fst slot))\<rbrace>
   get_cap slot
   \<lbrace>\<lambda>rv s. is_thread_cap rv \<longrightarrow> (is_subject aag (obj_ref_of rv))\<rbrace>" apply (clarsimp simp: valid_def) apply (frule get_cap_det) apply (drule_tac f=fst in arg_cong) apply (subst (asm) fst_conv) apply (drule in_get_cap_cte_wp_at[THEN iffD1]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule caps_of_state_pasObjectAbs_eq) apply (blast intro: sym) apply (fastforce simp: cap_auth_conferred_def split: cap.split) apply assumption+ apply (case_tac a, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag (fst slot))\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. is_thread_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (get_cap slot s); pas_refined aag s; is_subject aag (fst slot); is_thread_cap a\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of a) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (get_cap slot s); pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; get_cap slot s = ({(a, s)}, False)\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of a) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (get_cap slot s); pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = fst ({(a, s)}, False)\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of a) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (get_cap slot s); pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of a) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; s = b \<and> cte_wp_at ((=) a) slot s\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of a) proof (prove)
goal (1 subgoal):
 1. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of a) proof (prove)
goal (5 subgoals):
 1. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> caps_of_state (?s19 s a) (?p19 s a) = Some (?cap19 s a)
 2. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred (?cap19 s a)
 3. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> is_subject aag (fst (?p19 s a))
 4. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> pas_refined aag (?s19 s a)
 5. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> obj_ref_of a \<in> obj_refs_ac (?cap19 s a) proof (prove)
goal (4 subgoals):
 1. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred a
 2. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> is_subject aag (fst slot)
 3. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> obj_ref_of a \<in> obj_refs_ac a proof (prove)
goal (3 subgoals):
 1. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> is_subject aag (fst slot)
 2. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> obj_ref_of a \<in> obj_refs_ac a proof (prove)
goal (1 subgoal):
 1. \<And>s a. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); is_thread_cap a; fst (get_cap slot s) = {(a, s)}; caps_of_state s slot = Some a\<rbrakk> \<Longrightarrow> obj_ref_of a \<in> obj_refs_ac a proof (prove)
goal:
No subgoals!