theory Retype_AC

lemma create_cap_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and
    K (tp \<noteq> ArchObject ASIDPoolObj \<and> is_subject aag (fst p) \<and> is_subject aag (fst (fst ref)) \<and>
       (\<forall>x \<in> ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x) \<and>
       is_aligned (snd ref) (obj_bits_api tp sz))\<rbrace>
   create_cap tp sz p dev ref
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: create_cap_def split_def) apply (wps | wp set_cdt_pas_refined set_cap_pas_refined set_original_wp | clarsimp)+ apply (rule conjI) apply (cases "fst ref", clarsimp simp: pas_refined_refl) apply (cases "tp = Untyped") apply (simp add: cap_links_asid_slot_def pas_refined_refl cap_links_irq_def
                    aag_cap_auth_def ptr_range_def obj_bits_api_def) apply (clarsimp simp: clas_default_cap pas_refined_refl cli_default_cap aag_cap_auth_def) apply (drule obj_refs_default') apply (case_tac tp, simp_all) apply (auto intro: pas_refined_refl dest!: subsetD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (tp \<noteq> ArchObject ASIDPoolObj \<and> is_subject aag (fst p) \<and> is_subject aag (fst (fst ref)) \<and> (\<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x) \<and> is_aligned (snd ref) (obj_bits_api tp sz))\<rbrace> create_cap tp sz p dev ref \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>y. tp \<noteq> ArchObject ASIDPoolObj \<and> is_subject aag (fst p) \<and> is_subject aag (fst (fst ref)) \<and> (\<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x) \<and> is_aligned (snd ref) (obj_bits_api tp sz))\<rbrace> do dest_p <- gets (\<lambda>s. cdt s (fst ref));
cdt <- gets cdt;
y <- set_cdt (cdt(fst ref \<mapsto> p));
y <- create_cap_ext p (fst ref) dest_p;
y <- set_original (fst ref) True;
set_cap (default_cap tp (snd ref) sz dev) (fst ref)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tp \<noteq> ArchObject ASIDPoolObj; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x; is_aligned (snd ref) (obj_bits_api tp sz)\<rbrakk> \<Longrightarrow> (\<forall>a. (\<exists>b. (a, b) = fst ref) \<longrightarrow> (\<forall>aa. (\<exists>b. p = (aa, b) \<and> cdt s (fst ref) \<noteq> Some (aa, b)) \<longrightarrow> (is_transferable_in (fst ref) s \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag)) \<and> (is_transferable_in (fst ref) s \<longrightarrow> is_transferable_cap (default_cap tp (snd ref) sz dev) \<or> (pasSubject aag, Control, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag (default_cap tp (snd ref) sz dev) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tp \<noteq> ArchObject ASIDPoolObj; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x; is_aligned (snd ref) (obj_bits_api tp sz)\<rbrakk> \<Longrightarrow> \<forall>a. (\<exists>b. (a, b) = fst ref) \<longrightarrow> (\<forall>aa. (\<exists>b. p = (aa, b) \<and> cdt s (fst ref) \<noteq> Some (aa, b)) \<longrightarrow> (is_transferable_in (fst ref) s \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag)
 2. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tp \<noteq> ArchObject ASIDPoolObj; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x; is_aligned (snd ref) (obj_bits_api tp sz)\<rbrakk> \<Longrightarrow> (is_transferable_in (fst ref) s \<longrightarrow> is_transferable_cap (default_cap tp (snd ref) sz dev) \<or> (pasSubject aag, Control, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag (default_cap tp (snd ref) sz dev) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tp \<noteq> ArchObject ASIDPoolObj; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x; is_aligned (snd ref) (obj_bits_api tp sz)\<rbrakk> \<Longrightarrow> (is_transferable_in (fst ref) s \<longrightarrow> is_transferable_cap (default_cap tp (snd ref) sz dev) \<or> (pasSubject aag, Control, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag (default_cap tp (snd ref) sz dev) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tp \<noteq> ArchObject ASIDPoolObj; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x; is_aligned (snd ref) (obj_bits_api tp sz); tp = Untyped\<rbrakk> \<Longrightarrow> (is_transferable_in (fst ref) s \<longrightarrow> is_transferable_cap (default_cap tp (snd ref) sz dev) \<or> (pasSubject aag, Control, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag (default_cap tp (snd ref) sz dev)
 2. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tp \<noteq> ArchObject ASIDPoolObj; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x; is_aligned (snd ref) (obj_bits_api tp sz); tp \<noteq> Untyped\<rbrakk> \<Longrightarrow> (is_transferable_in (fst ref) s \<longrightarrow> is_transferable_cap (default_cap tp (snd ref) sz dev) \<or> (pasSubject aag, Control, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag (default_cap tp (snd ref) sz dev) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tp \<noteq> ArchObject ASIDPoolObj; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x; is_aligned (snd ref) (obj_bits_api tp sz); tp \<noteq> Untyped\<rbrakk> \<Longrightarrow> (is_transferable_in (fst ref) s \<longrightarrow> is_transferable_cap (default_cap tp (snd ref) sz dev) \<or> (pasSubject aag, Control, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag (default_cap tp (snd ref) sz dev) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tp \<noteq> ArchObject ASIDPoolObj; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x; is_aligned (snd ref) (obj_bits_api tp sz); tp \<noteq> Untyped\<rbrakk> \<Longrightarrow> (\<forall>x\<in>obj_refs_ac (default_cap tp (snd ref) sz dev). \<forall>auth\<in>cap_auth_conferred (default_cap tp (snd ref) sz dev). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (default_cap tp (snd ref) sz dev). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tp \<noteq> ArchObject ASIDPoolObj; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x; tp \<noteq> Untyped; obj_refs_ac (default_cap tp (snd ref) sz (?dev112 s)) \<subseteq> ptr_range (snd ref) (obj_bits_api tp sz)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>obj_refs_ac (default_cap tp (snd ref) sz dev). \<forall>auth\<in>cap_auth_conferred (default_cap tp (snd ref) sz dev). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (default_cap tp (snd ref) sz dev). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api TCBObject sz). is_subject aag x; snd ref \<in> ptr_range (snd ref) (obj_bits_api TCBObject sz); tp = TCBObject\<rbrakk> \<Longrightarrow> \<forall>auth\<in>cap_auth_conferred (ThreadCap (snd ref)). (pasSubject aag, auth, pasSubject aag) \<in> pasPolicy aag
 2. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api EndpointObject sz). is_subject aag x; snd ref \<in> ptr_range (snd ref) (obj_bits_api EndpointObject sz); tp = EndpointObject\<rbrakk> \<Longrightarrow> \<forall>auth\<in>cap_auth_conferred (EndpointCap (snd ref) 0 UNIV). (pasSubject aag, auth, pasSubject aag) \<in> pasPolicy aag
 3. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api NotificationObject sz). is_subject aag x; snd ref \<in> ptr_range (snd ref) (obj_bits_api NotificationObject sz); tp = NotificationObject\<rbrakk> \<Longrightarrow> \<forall>auth\<in>cap_auth_conferred (NotificationCap (snd ref) 0 {AllowRead, AllowWrite}). (pasSubject aag, auth, pasSubject aag) \<in> pasPolicy aag
 4. \<And>s. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api CapTableObject sz). is_subject aag x; snd ref \<in> ptr_range (snd ref) (obj_bits_api CapTableObject sz); tp = CapTableObject\<rbrakk> \<Longrightarrow> \<forall>auth\<in>cap_auth_conferred (CNodeCap (snd ref) sz []). (pasSubject aag, auth, pasSubject aag) \<in> pasPolicy aag
 5. \<And>s x6. \<lbrakk>pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; x6 \<noteq> ASIDPoolObj; is_subject aag (fst p); is_subject aag (fst (fst ref)); \<forall>x\<in>ptr_range (snd ref) (obj_bits_api (ArchObject x6) sz). is_subject aag x; aobj_ref' (arch_default_cap x6 (snd ref) sz (?dev112 s)) \<subseteq> ptr_range (snd ref) (obj_bits_api (ArchObject x6) sz); tp = ArchObject x6\<rbrakk> \<Longrightarrow> \<forall>x\<in>aobj_ref' (arch_default_cap x6 (snd ref) sz dev). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (arch_default_cap x6 (snd ref) sz dev)). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!