theory ArchIpc_AI

lemma transfer_caps_loop_cte_wp_at:
  assumes imp: "\<And>cap. P cap \<Longrightarrow> \<not> is_untyped_cap cap"
  shows "\<lbrace>cte_wp_at P sl and K (sl \<notin> set slots) and (\<lambda>s. \<forall>x \<in> set slots. cte_at x s)\<rbrace>
   transfer_caps_loop ep buffer n caps slots mi
   \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>" apply (induct caps arbitrary: slots n mi) apply (simp, wp, simp) apply (clarsimp simp: Let_def split_def whenE_def
                  cong: if_cong list.case_cong
             split del: if_split) apply (rule hoare_pre) apply (wp hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift
              derive_cap_is_derived_foo
             hoare_drop_imps
        | assumption | simp split del: if_split)+ apply (wp hoare_vcg_conj_lift cap_insert_weak_cte_wp_at2) apply (erule imp) apply (wp hoare_vcg_ball_lift
             | clarsimp simp: is_cap_simps split del:if_split
             | unfold derive_cap_def arch_derive_cap_def
             | wpc
             | rule conjI
             | case_tac slots)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P sl and K (sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slots n mi. \<lbrace>cte_wp_at P sl and K (sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n [] slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 2. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>cte_wp_at P sl and K (sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>) \<Longrightarrow> \<lbrace>cte_wp_at P sl and K (sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. \<lbrace>cte_wp_at P sl and K (sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>) \<Longrightarrow> \<lbrace>cte_wp_at P sl and K (sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n (a # caps) slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a aa b caps slots n mi. (\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>) \<Longrightarrow> \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (if is_ep_cap a \<and> ep = Some (obj_ref_of a) then doE y <- liftE (set_extra_badge buffer (cap_ep_badge a) n);
liftE (transfer_caps_loop (Some (obj_ref_of a)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE else if slots \<noteq> [] then doE cap' <- derive_cap (aa, b) a;
y <- if cap' = NullCap then throwError undefined else returnOk ();
y <- liftE (cap_insert cap' (aa, b) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) caps (tl slots) mi)
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))) \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a aa b caps slots n mi. (\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>) \<Longrightarrow> \<lbrace>?Q9 a aa b caps slots n mi\<rbrace> const_on_failure (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) (if is_ep_cap a \<and> ep = Some (obj_ref_of a) then doE y <- liftE (set_extra_badge buffer (cap_ep_badge a) n);
liftE (transfer_caps_loop (Some (obj_ref_of a)) buffer (Suc n) caps slots (MI (mi_length mi) (mi_extra_caps mi) (mi_caps_unwrapped mi || 2 ^ n) (mi_label mi)))
odE else if slots \<noteq> [] then doE cap' <- derive_cap (aa, b) a;
y <- if cap' = NullCap then throwError undefined else returnOk ();
y <- liftE (cap_insert cap' (aa, b) (hd slots));
liftE (transfer_caps_loop ep buffer (Suc n) caps (tl slots) mi)
odE else returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi))) \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 2. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; (cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)) s\<rbrakk> \<Longrightarrow> ?Q9 a aa b caps slots n mi s proof (prove)
goal (5 subgoals):
 1. \<And>a aa b caps slots n mi cap'. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B56 a aa b caps slots n mi cap' ()\<rbrace> cap_insert cap' (aa, b) (hd slots) \<lbrace>\<lambda>ya s. cte_wp_at P sl s \<and> sl \<notin> set (tl slots) \<and> (\<forall>x\<in>set (tl slots). cte_wp_at (\<lambda>_. True) x s)\<rbrace>
 2. \<And>a aa b caps slots n mi cap'. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B55 a aa b caps slots n mi cap'\<rbrace> if cap' = NullCap then throwError undefined else returnOk () \<lbrace>?B56 a aa b caps slots n mi cap'\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 3. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q54 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>?B55 a aa b caps slots n mi\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 4. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R54 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 5. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; (cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)) s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> cte_wp_at P sl s \<and> sl \<notin> set slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q54 a aa b caps slots n mi s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R54 a aa b caps slots n mi s)) proof (prove)
goal (6 subgoals):
 1. \<And>a aa b caps slots n mi cap' c. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []; P c\<rbrakk> \<Longrightarrow> \<not> is_untyped_cap c
 2. \<And>a aa b caps slots n mi cap'. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'133 a aa b caps slots n mi cap' ()\<rbrace> cap_insert cap' (aa, b) (hd slots) \<lbrace>\<lambda>rv s. sl \<notin> set (tl slots) \<and> (\<forall>x\<in>set (tl slots). cte_wp_at (\<lambda>_. True) x s)\<rbrace>
 3. \<And>a aa b caps slots n mi cap'. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B55 a aa b caps slots n mi cap'\<rbrace> if cap' = NullCap then throwError undefined else returnOk () \<lbrace>\<lambda>c d. (if sl = hd slots then P cap' else cte_wp_at P sl d) \<and> ?P'133 a aa b caps slots n mi cap' c d\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 4. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q54 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>?B55 a aa b caps slots n mi\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 5. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R54 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 6. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; (cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)) s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> cte_wp_at P sl s \<and> sl \<notin> set slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q54 a aa b caps slots n mi s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R54 a aa b caps slots n mi s)) proof (prove)
goal (5 subgoals):
 1. \<And>a aa b caps slots n mi cap'. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; is_ep_cap a \<longrightarrow> ep \<noteq> Some (obj_ref_of a); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'133 a aa b caps slots n mi cap' ()\<rbrace> cap_insert cap' (aa, b) (hd slots) \<lbrace>\<lambda>rv s. sl \<notin> set (tl slots) \<and> (\<forall>x\<in>set (tl slots). cte_wp_at (\<lambda>_. True) x s)\<rbrace>
 2. \<And>a aa b caps slots n mi cap'. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B55 a aa b caps slots n mi cap'\<rbrace> if cap' = NullCap then throwError undefined else returnOk () \<lbrace>\<lambda>c d. (if sl = hd slots then P cap' else cte_wp_at P sl d) \<and> ?P'133 a aa b caps slots n mi cap' c d\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 3. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q54 a aa b caps slots n mi\<rbrace> derive_cap (aa, b) a \<lbrace>?B55 a aa b caps slots n mi\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 4. \<And>a aa b caps slots n mi. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; \<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)); \<not> slots \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R54 a aa b caps slots n mi\<rbrace> returnOk (MI (mi_length mi) (word_of_nat n) (mi_caps_unwrapped mi) (mi_label mi)) \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>, \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>
 5. \<And>a aa b caps slots n mi s. \<lbrakk>\<And>slots n mi. \<lbrace>cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>; (cte_wp_at P sl and (\<lambda>y. sl \<notin> set slots) and (\<lambda>s. \<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)) s\<rbrakk> \<Longrightarrow> (is_ep_cap a \<and> ep = Some (obj_ref_of a) \<longrightarrow> cte_wp_at P sl s \<and> sl \<notin> set slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>_. True) x s)) \<and> (\<not> (is_ep_cap a \<and> ep = Some (obj_ref_of a)) \<longrightarrow> (slots \<noteq> [] \<longrightarrow> ?Q54 a aa b caps slots n mi s) \<and> (\<not> slots \<noteq> [] \<longrightarrow> ?R54 a aa b caps slots n mi s)) proof (prove)
goal:
No subgoals!