theory ArchIpc_AI

lemma transfer_caps_tcb_caps:
  fixes P t ref mi caps ep receiver recv_buf
  assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c"
  shows
  "\<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace>
     transfer_caps mi caps ep receiver recv_buf
   \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace>" apply (simp add: transfer_caps_def) apply (wp hoare_vcg_const_Ball_lift hoare_vcg_const_imp_lift
            transfer_caps_loop_cte_wp_at
         | wpc | simp)+ apply (erule imp) apply (wp hoare_vcg_conj_lift hoare_vcg_const_imp_lift hoare_vcg_all_lift
            ) apply (rule_tac Q = "\<lambda>rv s.  ( \<forall>x\<in>set rv. real_cte_at x s )
      \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s"
       in hoare_strengthen_post) apply (wp get_rs_real_cte_at) apply clarsimp apply (drule(1) bspec) apply (clarsimp simp:obj_at_def is_tcb is_cap_table) apply (rule hoare_post_imp) apply (rule_tac Q="\<lambda>x. real_cte_at x s" in ballEI, assumption) apply (erule real_cte_at_cte) apply (rule get_rs_real_cte_at) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace> transfer_caps mi caps ep receiver recv_buf \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace> do dest_slots <- get_receive_slots receiver recv_buf;
case recv_buf of None \<Rightarrow> return (MI (mi_length mi) 0 0 (mi_label mi)) | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length mi) 0 0 (mi_label mi))
od \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x2 cap. \<lbrakk>recv_buf = Some x2; P cap\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap cap
 2. \<lbrace>?Q\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>dest_slots s. (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) and K ((t, ref) \<notin> set dest_slots) and (\<lambda>s. \<forall>x\<in>set dest_slots. cte_wp_at (\<lambda>_. True) x s)) s)\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>dest_slots s. (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) and K ((t, ref) \<notin> set dest_slots) and (\<lambda>s. \<forall>x\<in>set dest_slots. cte_wp_at (\<lambda>_. True) x s)) s)\<rbrace>
 2. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'29 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv. K ((t, ref) \<notin> set rv)\<rbrace>
 2. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'27 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) s \<and> ?P'29 x s) \<and> ?P'27 x s) proof (prove)
goal (4 subgoals):
 1. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'29 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. real_cte_at x s) \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s\<rbrace>
 2. \<And>x rv s. \<lbrakk>recv_buf = Some x; (\<forall>x\<in>set rv. real_cte_at x s) \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s\<rbrakk> \<Longrightarrow> K ((t, ref) \<notin> set rv) s
 3. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'27 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s\<rbrace>
 4. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) s \<and> ?P'29 x s) \<and> ?P'27 x s) proof (prove)
goal (3 subgoals):
 1. \<And>x rv s. \<lbrakk>recv_buf = Some x; (\<forall>x\<in>set rv. real_cte_at x s) \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s\<rbrakk> \<Longrightarrow> K ((t, ref) \<notin> set rv) s
 2. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'27 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) s \<and> valid_objs s \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s) \<and> ?P'27 x s) proof (prove)
goal (3 subgoals):
 1. \<And>x rv s. \<lbrakk>recv_buf = Some x; \<forall>x\<in>set rv. real_cte_at x s; cte_wp_at P (t, ref) s; tcb_at t s; (t, ref) \<in> set rv\<rbrakk> \<Longrightarrow> False
 2. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'27 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) s \<and> valid_objs s \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s) \<and> ?P'27 x s) proof (prove)
goal (3 subgoals):
 1. \<And>x rv s. \<lbrakk>recv_buf = Some x; cte_wp_at P (t, ref) s; tcb_at t s; (t, ref) \<in> set rv; real_cte_at (t, ref) s\<rbrakk> \<Longrightarrow> False
 2. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'27 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) s \<and> valid_objs s \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s) \<and> ?P'27 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'27 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s\<rbrace>
 2. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) s \<and> valid_objs s \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s) \<and> ?P'27 x s) proof (prove)
goal (3 subgoals):
 1. \<And>x rv s. \<lbrakk>recv_buf = Some x; ?Q58 x rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s
 2. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'27 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>?Q58 x\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) s \<and> valid_objs s \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s) \<and> ?P'27 x s) proof (prove)
goal (3 subgoals):
 1. \<And>x rv s xa. \<lbrakk>recv_buf = Some x; \<forall>x\<in>set rv. real_cte_at x s; xa \<in> set rv; real_cte_at xa s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) xa s
 2. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'27 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. real_cte_at x s\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) s \<and> valid_objs s \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s) \<and> ?P'27 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x. recv_buf = Some x \<Longrightarrow> \<lbrace>?P'27 x\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. real_cte_at x s\<rbrace>
 2. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) s \<and> valid_objs s \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s) \<and> ?P'27 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at P (t, ref) s) \<and> (\<forall>x. recv_buf = Some x \<longrightarrow> (cte_wp_at P (t, ref) s \<and> valid_objs s \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s) \<and> valid_objs s) proof (prove)
goal:
No subgoals!