theory CSpace_AI

lemma setup_reply_master_pspace[wp]:
  "\<lbrace>valid_pspace and tcb_at t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_pspace\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp get_cap_wp set_cap_valid_pspace) apply clarsimp apply (rule conjI, clarsimp elim!: cte_wp_at_weakenE) apply (rule conjI, simp add: valid_cap_def cap_aligned_def word_bits_def) apply (clarsimp simp: tcb_at_def valid_pspace_def pspace_aligned_def) apply (fastforce dest: get_tcb_SomeD elim: my_BallE [where y=t]) apply (clarsimp simp: tcb_cap_valid_def is_cap_simps tcb_at_st_tcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace and tcb_at t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace and tcb_at t\<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_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_pspace and tcb_at t) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. cte_wp_at (\<lambda>cap'. (\<forall>p'\<in>zobj_refs cap' - zobj_refs (ReplyCap t True {AllowGrant, AllowWrite}). obj_at (Not \<circ> live) p' (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>)) \<and> (\<forall>r\<in>ex_zombie_refs (ReplyCap t True {AllowGrant, AllowWrite}, cap'). \<forall>p'. (t, tcb_cnode_index 2) \<noteq> p' \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') p' (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) \<and> \<not> is_zombie (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> s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr> \<turnstile> ReplyCap t True {AllowGrant, AllowWrite} \<and> tcb_cap_valid (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> valid_pspace (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) else valid_pspace) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace s; tcb_at t s; cte_wp_at ((=) NullCap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. \<forall>p'\<in>zobj_refs cap'. obj_at (Not \<circ> live) p' s) (t, tcb_cnode_index 2) s \<and> s \<turnstile> ReplyCap t True {AllowGrant, AllowWrite} \<and> tcb_cap_valid (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_pspace s; tcb_at t s; cte_wp_at ((=) NullCap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> s \<turnstile> ReplyCap t True {AllowGrant, AllowWrite} \<and> tcb_cap_valid (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 (2 subgoals):
 1. \<And>s. \<lbrakk>valid_pspace s; tcb_at t s; cte_wp_at ((=) NullCap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_aligned t 9
 2. \<And>s. \<lbrakk>valid_pspace s; tcb_at t s; cte_wp_at ((=) NullCap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> tcb_cap_valid (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 (2 subgoals):
 1. \<And>s tcb. \<lbrakk>cte_wp_at ((=) NullCap) (t, tcb_cnode_index 2) s; get_tcb t s = Some tcb; valid_objs s; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> is_aligned t 9
 2. \<And>s. \<lbrakk>valid_pspace s; tcb_at t s; cte_wp_at ((=) NullCap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> tcb_cap_valid (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_pspace s; tcb_at t s; cte_wp_at ((=) NullCap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> tcb_cap_valid (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:
No subgoals!