theory ArchIpc_AI

lemma transfer_caps_non_null_cte_wp_at:
  assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c"
  shows  "\<lbrace>valid_objs and cte_wp_at (P and ((\<noteq>) cap.NullCap)) ptr\<rbrace>
     transfer_caps mi caps ep receiver recv_buf
   \<lbrace>\<lambda>_. cte_wp_at (P and ((\<noteq>) cap.NullCap)) ptr\<rbrace>" unfolding transfer_caps_def apply simp apply (rule hoare_pre) apply (wp hoare_vcg_ball_lift transfer_caps_loop_cte_wp_at hoare_weak_lift_imp
     | wpc | clarsimp simp:imp)+ apply (rule hoare_strengthen_post
            [where Q="\<lambda>rv s'. (cte_wp_at ((\<noteq>) cap.NullCap) ptr) s'
                      \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) cap.NullCap) x s')",
             rotated]) apply (clarsimp) apply  (rule conjI) apply (erule contrapos_pn) apply (drule_tac x=ptr in bspec, assumption) apply (clarsimp elim!: cte_wp_at_orth) apply (rule ballI) apply (drule(1) bspec) apply (erule cte_wp_cte_at) apply (wp) apply (auto simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace> transfer_caps mi caps ep receiver recv_buf \<lbrace>\<lambda>_. cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace> do dest_slots <- get_receive_slots receiver recv_buf;
mi' <- return $ MI (mi_length mi) 0 0 (mi_label mi);
case recv_buf of None \<Rightarrow> return mi' | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots mi'
od \<lbrace>\<lambda>_. cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr\<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>_. cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<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>_. cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace>
 2. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'34\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s. ptr \<notin> set rv \<and> (\<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s)\<rbrace>
 2. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> ?P'34 s) proof (prove)
goal (3 subgoals):
 1. \<And>rv s. cte_wp_at ((\<noteq>) NullCap) ptr s \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s) \<Longrightarrow> ptr \<notin> set rv \<and> (\<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s)
 2. \<lbrace>?P'34\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s'. cte_wp_at ((\<noteq>) NullCap) ptr s' \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s')\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> ?P'34 s) proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) ptr s; \<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s\<rbrakk> \<Longrightarrow> ptr \<notin> set rv \<and> (\<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s)
 2. \<lbrace>?P'34\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s'. cte_wp_at ((\<noteq>) NullCap) ptr s' \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s')\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> ?P'34 s) proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) ptr s; \<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s\<rbrakk> \<Longrightarrow> ptr \<notin> set rv
 2. \<And>rv s. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) ptr s; \<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s
 3. \<lbrace>?P'34\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s'. cte_wp_at ((\<noteq>) NullCap) ptr s' \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s')\<rbrace>
 4. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> ?P'34 s) proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s; ptr \<in> set rv\<rbrakk> \<Longrightarrow> \<not> cte_wp_at ((\<noteq>) NullCap) ptr s
 2. \<And>rv s. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) ptr s; \<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s
 3. \<lbrace>?P'34\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s'. cte_wp_at ((\<noteq>) NullCap) ptr s' \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s')\<rbrace>
 4. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> ?P'34 s) proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>ptr \<in> set rv; cte_wp_at ((=) NullCap) ptr s\<rbrakk> \<Longrightarrow> \<not> cte_wp_at ((\<noteq>) NullCap) ptr s
 2. \<And>rv s. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) ptr s; \<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s
 3. \<lbrace>?P'34\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s'. cte_wp_at ((\<noteq>) NullCap) ptr s' \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s')\<rbrace>
 4. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> ?P'34 s) proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) ptr s; \<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. cte_wp_at (\<lambda>_. True) x s
 2. \<lbrace>?P'34\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s'. cte_wp_at ((\<noteq>) NullCap) ptr s' \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s')\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> ?P'34 s) proof (prove)
goal (3 subgoals):
 1. \<And>rv s x. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) ptr s; \<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s; x \<in> set rv\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s
 2. \<lbrace>?P'34\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s'. cte_wp_at ((\<noteq>) NullCap) ptr s' \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s')\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> ?P'34 s) proof (prove)
goal (3 subgoals):
 1. \<And>rv s x. \<lbrakk>cte_wp_at ((\<noteq>) NullCap) ptr s; x \<in> set rv; cte_wp_at ((=) NullCap) x s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s
 2. \<lbrace>?P'34\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s'. cte_wp_at ((\<noteq>) NullCap) ptr s' \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s')\<rbrace>
 3. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> ?P'34 s) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'34\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv s'. cte_wp_at ((\<noteq>) NullCap) ptr s' \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) NullCap) x s')\<rbrace>
 2. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> ?P'34 s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr) s \<Longrightarrow> (recv_buf = None \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s) \<and> ((\<exists>x. recv_buf = Some x) \<longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ptr s \<and> cte_wp_at ((\<noteq>) NullCap) ptr s \<and> True) proof (prove)
goal:
No subgoals!