theory Ipc_AC

lemma derive_cap_is_derived_foo':
  "\<lbrace>\<lambda>s :: det_ext state.
    \<forall>cap'. (valid_objs s \<and> cap' \<noteq> NullCap \<and>
            cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and>
                              (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and>
                              cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s
            \<longrightarrow> cte_at slot s) \<and>
           (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap') \<and>
           (cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and>
                                \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap)
           \<longrightarrow> Q cap' s\<rbrace>
   derive_cap slot cap
   \<lbrace>Q\<rbrace>, -" apply (clarsimp simp: validE_R_def validE_def valid_def split: sum.splits) apply (frule in_inv_by_hoareD[OF derive_cap_inv], clarsimp) apply (erule allE) apply (erule impEM) apply (frule use_validE_R[OF _ cap_derive_not_null_helper, OF _ _ imp_refl]) apply (rule derive_cap_inv[THEN valid_validE_R]) apply (intro conjI) apply (clarsimp simp: cte_wp_at_caps_of_state)+ apply (erule(1) use_validE_R[OF _ derive_cap_valid_cap]) apply simp apply (erule use_validE_R[OF _ derive_cap_auth_derived],simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cap'. (valid_objs s \<and> cap' \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> Q cap' s\<rbrace> derive_cap slot cap \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s b r. \<lbrakk>\<forall>cap'. (valid_objs s \<and> cap' \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> Q cap' s; (Inr r, b) \<in> fst (derive_cap slot cap s)\<rbrakk> \<Longrightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<lbrakk>\<forall>cap'. (valid_objs s \<and> cap' \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> Q cap' s; (Inr r, s) \<in> fst (derive_cap slot cap s)\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); (valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> ?cap'15 s r) \<and> (?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) \<longrightarrow> Q (?cap'15 s r) s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>s r. (Inr r, s) \<in> fst (derive_cap slot cap s) \<Longrightarrow> (valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> ?cap'15 s r) \<and> (?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap)
 2. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); (valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> ?cap'15 s r) \<and> (?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap); Q (?cap'15 s r) s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>s r. (Inr r, s) \<in> fst (derive_cap slot cap s) \<Longrightarrow> \<lbrace>\<lambda>a. cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap\<rbrace> derive_cap slot cap \<lbrace>?Q20 s r\<rbrace>, -
 2. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); r \<noteq> NullCap \<longrightarrow> ?Q20 s r r s\<rbrakk> \<Longrightarrow> (valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> ?cap'15 s r) \<and> (?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap)
 3. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); (valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> ?cap'15 s r) \<and> (?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap); Q (?cap'15 s r) s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); r \<noteq> NullCap \<longrightarrow> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> (valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> ?cap'15 s r) \<and> (?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap)
 2. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); (valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> ?cap'15 s r) \<and> (?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap); Q (?cap'15 s r) s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (4 subgoals):
 1. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); r \<noteq> NullCap \<longrightarrow> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 2. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); r \<noteq> NullCap \<longrightarrow> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> s \<turnstile> cap \<longrightarrow> s \<turnstile> ?cap'15 s r
 3. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); r \<noteq> NullCap \<longrightarrow> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> ?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap
 4. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); (valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> ?cap'15 s r) \<and> (?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap); Q (?cap'15 s r) s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); r \<noteq> NullCap \<longrightarrow> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap; s \<turnstile> cap\<rbrakk> \<Longrightarrow> s \<turnstile> ?cap'15 s r
 2. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); r \<noteq> NullCap \<longrightarrow> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> ?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap
 3. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); (valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> ?cap'15 s r) \<and> (?cap'15 s r \<noteq> NullCap \<longrightarrow> auth_derived (?cap'15 s r) cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap); Q (?cap'15 s r) s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); r \<noteq> NullCap \<longrightarrow> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> r \<noteq> NullCap \<longrightarrow> auth_derived r cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap
 2. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); (valid_objs s \<and> r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> r) \<and> (r \<noteq> NullCap \<longrightarrow> auth_derived r cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap); Q r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); r \<noteq> NullCap \<longrightarrow> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap\<rbrakk> \<Longrightarrow> r \<noteq> NullCap \<longrightarrow> auth_derived r cap
 2. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); (valid_objs s \<and> r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> r) \<and> (r \<noteq> NullCap \<longrightarrow> auth_derived r cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap); Q r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<lbrakk>(Inr r, s) \<in> fst (derive_cap slot cap s); (valid_objs s \<and> r \<noteq> NullCap \<and> cte_wp_at (\<lambda>capa. cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) slot s \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> r) \<and> (r \<noteq> NullCap \<longrightarrow> auth_derived r cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap); Q r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal:
No subgoals!