theory ArchCSpace_AI

lemma setup_reply_master_arch_caps[wp, CSpace_AI_assms]:
  "\<lbrace>valid_arch_caps and tcb_at t and valid_objs and pspace_aligned\<rbrace>
     setup_reply_master t
   \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp set_cap_valid_arch_caps get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state is_pd_cap_def
                        is_pt_cap_def vs_cap_ref_def) apply (rule no_cap_to_obj_with_diff_ref_triv,
         simp_all add: is_cap_simps table_cap_ref_def) apply (simp add: valid_cap_def cap_aligned_def word_bits_def) apply (clarsimp simp: obj_at_def is_tcb dest!: pspace_alignedD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and tcb_at t and valid_objs and pspace_aligned\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and tcb_at t and valid_objs and pspace_aligned\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_arch_caps and tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. valid_arch_caps (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') (t, tcb_cnode_index 2) (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (ReplyCap t True {AllowGrant, AllowWrite}) = Some vref \<and> obj_refs (ReplyCap t True {AllowGrant, AllowWrite}) = obj_refs cap' \<or> \<not> is_final_cap' cap' (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) \<and> \<not> reachable_pg_cap cap' (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>))) \<and> no_cap_to_obj_with_diff_ref (ReplyCap t True {AllowGrant, AllowWrite}) {(t, tcb_cnode_index 2)} (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) \<and> (is_pt_cap (ReplyCap t True {AllowGrant, AllowWrite}) \<or> is_pd_cap (ReplyCap t True {AllowGrant, AllowWrite}) \<longrightarrow> cap_asid (ReplyCap t True {AllowGrant, AllowWrite}) = None \<longrightarrow> (\<forall>r\<in>obj_refs (ReplyCap t True {AllowGrant, AllowWrite}). obj_at (empty_table (set (second_level_tables (arch_state (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>))))) r (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>))) \<and> (is_pt_cap (ReplyCap t True {AllowGrant, AllowWrite}) \<or> is_pd_cap (ReplyCap t True {AllowGrant, AllowWrite}) \<longrightarrow> (\<forall>oldcap. caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) (t, tcb_cnode_index 2) = Some oldcap \<longrightarrow> is_pt_cap (ReplyCap t True {AllowGrant, AllowWrite}) \<and> is_pt_cap oldcap \<or> is_pd_cap (ReplyCap t True {AllowGrant, AllowWrite}) \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid (ReplyCap t True {AllowGrant, AllowWrite}) = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs (ReplyCap t True {AllowGrant, AllowWrite})) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs (ReplyCap t True {AllowGrant, AllowWrite}) \<and> (is_pd_cap (ReplyCap t True {AllowGrant, AllowWrite}) \<and> is_pd_cap cap' \<or> is_pt_cap (ReplyCap t True {AllowGrant, AllowWrite}) \<and> is_pt_cap cap') \<and> (cap_asid (ReplyCap t True {AllowGrant, AllowWrite}) = None \<or> cap_asid cap' = None)) ptr' (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) \<longrightarrow> ptr' = (t, tcb_cnode_index 2))) else valid_arch_caps) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_arch_caps s; tcb_at t s; valid_objs s; pspace_aligned s; caps_of_state s (t, tcb_cnode_index 2) = Some NullCap\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ReplyCap t True {AllowGrant, AllowWrite}) {(t, tcb_cnode_index 2)} (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_arch_caps s; tcb_at t s; valid_objs s; pspace_aligned s; caps_of_state s (t, tcb_cnode_index 2) = Some NullCap\<rbrakk> \<Longrightarrow> s \<turnstile> ReplyCap t True {AllowGrant, AllowWrite} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_arch_caps s; tcb_at t s; valid_objs s; pspace_aligned s; caps_of_state s (t, tcb_cnode_index 2) = Some NullCap\<rbrakk> \<Longrightarrow> is_aligned t 9 proof (prove)
goal:
No subgoals!