theory FinalCaps

lemma transfer_caps_silc_inv:
  "\<lbrace>silc_inv aag st and valid_objs and valid_mdb and pas_refined aag
                    and (\<lambda>s. (\<forall>x \<in> set caps. s \<turnstile> fst x) \<and>
                             (\<forall>x \<in> set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s
                                           \<and> real_cte_at (snd x) s))
                    and K (is_subject aag receiver \<and> (\<forall>cap \<in> set caps. is_subject aag (fst (snd cap))))\<rbrace>
  transfer_caps mi caps endpoint receiver receive_buffer
  \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: transfer_caps_def) apply (wpc | wp)+ apply (rule_tac P = "\<forall>x \<in> set dest_slots. is_subject aag (fst x)" in hoare_gen_asm) apply (wp transfer_caps_loop_pres_dest cap_insert_silc_inv) apply (fastforce simp: silc_inv_def) apply (wp get_receive_slots_authorised hoare_vcg_all_lift hoare_vcg_imp_lift | simp)+ apply (fastforce elim: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) and K (is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))))\<rbrace> transfer_caps mi caps endpoint receiver receive_buffer \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<Longrightarrow> \<lbrace>silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))\<rbrace> transfer_caps mi caps endpoint receiver receive_buffer \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<Longrightarrow> \<lbrace>silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))\<rbrace> do dest_slots <- get_receive_slots receiver receive_buffer;
case receive_buffer of None \<Rightarrow> return (MI (mi_length mi) 0 0 (mi_label mi)) | Some receive_buffer \<Rightarrow> transfer_caps_loop endpoint receive_buffer 0 caps dest_slots (MI (mi_length mi) 0 0 (mi_label mi))
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>dest_slots x2. \<lbrakk>is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))); receive_buffer = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R13 dest_slots x2\<rbrace> transfer_caps_loop endpoint x2 0 caps dest_slots (MI (mi_length mi) 0 0 (mi_label mi)) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<Longrightarrow> \<lbrace>?Q2\<rbrace> get_receive_slots receiver receive_buffer \<lbrace>\<lambda>dest_slots s. (receive_buffer = None \<longrightarrow> silc_inv aag st s) \<and> (\<forall>x. receive_buffer = Some x \<longrightarrow> ?R13 dest_slots x s)\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))); (silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>dest_slots x2. \<lbrakk>is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))); receive_buffer = Some x2; \<forall>x\<in>set dest_slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> \<lbrace>?P'18 dest_slots x2\<rbrace> transfer_caps_loop endpoint x2 0 caps dest_slots (MI (mi_length mi) 0 0 (mi_label mi)) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<Longrightarrow> \<lbrace>?Q2\<rbrace> get_receive_slots receiver receive_buffer \<lbrace>\<lambda>dest_slots s. (receive_buffer = None \<longrightarrow> silc_inv aag st s) \<and> (\<forall>x. receive_buffer = Some x \<longrightarrow> (?P'18 dest_slots x and K (\<forall>x\<in>set dest_slots. is_subject aag (fst x))) s)\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))); (silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>dest_slots x2 cap src dest s. \<lbrakk>is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))); receive_buffer = Some x2; \<forall>x\<in>set dest_slots. is_subject aag (fst x); silc_inv aag st s \<and> dest \<in> set dest_slots \<and> src \<in> snd ` set caps \<and> valid_objs s \<and> real_cte_at dest s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> real_cte_at src s \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (pasObjectAbs aag (fst src) = pasObjectAbs aag (fst dest) \<and> pasObjectAbs aag (fst dest) \<noteq> SilcLabel)) s
 2. \<And>dest_slots x2 b n'. \<lbrakk>is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))); receive_buffer = Some x2; \<forall>x\<in>set dest_slots. is_subject aag (fst x); n' \<le> 0 + length caps\<rbrakk> \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> set_extra_badge x2 b n' \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<Longrightarrow> \<lbrace>?Q2\<rbrace> get_receive_slots receiver receive_buffer \<lbrace>\<lambda>dest_slots s. (receive_buffer = None \<longrightarrow> silc_inv aag st s) \<and> (\<forall>x. receive_buffer = Some x \<longrightarrow> ((\<lambda>s. silc_inv aag st s \<and> valid_objs s \<and> valid_mdb s \<and> distinct dest_slots \<and> (\<forall>x\<in>set dest_slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) and K (\<forall>x\<in>set dest_slots. is_subject aag (fst x))) s)\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))); (silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>dest_slots x2 b n'. \<lbrakk>is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))); receive_buffer = Some x2; \<forall>x\<in>set dest_slots. is_subject aag (fst x); n' \<le> 0 + length caps\<rbrakk> \<Longrightarrow> \<lbrace>silc_inv aag st\<rbrace> set_extra_badge x2 b n' \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<Longrightarrow> \<lbrace>?Q2\<rbrace> get_receive_slots receiver receive_buffer \<lbrace>\<lambda>dest_slots s. (receive_buffer = None \<longrightarrow> silc_inv aag st s) \<and> (\<forall>x. receive_buffer = Some x \<longrightarrow> ((\<lambda>s. silc_inv aag st s \<and> valid_objs s \<and> valid_mdb s \<and> distinct dest_slots \<and> (\<forall>x\<in>set dest_slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)) and K (\<forall>x\<in>set dest_slots. is_subject aag (fst x))) s)\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))); (silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag receiver \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))); silc_inv aag st s \<and> valid_objs s \<and> valid_mdb s \<and> pas_refined aag s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)\<rbrakk> \<Longrightarrow> (\<exists>x. receive_buffer = Some x) \<longrightarrow> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s) proof (prove)
goal:
No subgoals!