theory Ipc_AI

lemma derive_cap_is_derived_foo:
  "\<lbrace>\<lambda>s. \<forall>cap'. (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 \<and> valid_objs s \<and> cap' \<noteq> NullCap
          \<longrightarrow> cte_at slot s )
            \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap')
            \<and> (cap' \<noteq> NullCap \<longrightarrow> 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 add: 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 simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cap'. (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 \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> 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'. (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 \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> 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'. (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 \<and> valid_objs s \<and> cap' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap') \<and> (cap' \<noteq> NullCap \<longrightarrow> 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); (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 \<and> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<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> 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> (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 \<and> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<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> 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); (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 \<and> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<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> 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> (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 \<and> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<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> 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); (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 \<and> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<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> 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> (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 \<and> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<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> 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); (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 \<and> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<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> 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> 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 \<and> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<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> 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); (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 \<and> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<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> 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> 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); (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 \<and> valid_objs s \<and> ?cap'15 s r \<noteq> NullCap \<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> 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> 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); (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 \<and> valid_objs s \<and> r \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> r) \<and> (r \<noteq> NullCap \<longrightarrow> 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); (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 \<and> valid_objs s \<and> r \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s) \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> r) \<and> (r \<noteq> NullCap \<longrightarrow> 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!