kings-crown/FVELER_Isabelle huggingface dataset:
theory CNode_AC

lemma empty_slot_integrity[wp,wp_not_transferable]:
  "\<lbrace>integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag
                       and K (is_subject aag (fst slot) \<and> cleanup_info_wf c aag)\<rbrace>
   empty_slot slot c
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (integrity_trans_start) apply (rule hoare_pre) apply (wp empty_slot_integrity_spec[simplified spec_valid_def]) by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and valid_list and valid_objs and valid_mdb and pas_refined aag and K (is_subject aag (fst slot) \<and> cleanup_info_wf c aag)\<rbrace> empty_slot slot c \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_list and (valid_objs and (valid_mdb and (pas_refined aag and K (is_subject aag (fst slot) \<and> cleanup_info_wf c aag))))) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> empty_slot slot c \<lbrace>\<lambda>_. integrity aag X s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_list and (valid_objs and (valid_mdb and (pas_refined aag and K (is_subject aag (fst slot) \<and> cleanup_info_wf c aag))))) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> empty_slot slot c \<lbrace>\<lambda>_. integrity aag X s\<rbrace>
 2. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and K (is_subject aag (fst slot) \<and> cleanup_info_wf c aag))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(valid_list and (valid_objs and (valid_mdb and (pas_refined aag and K (is_subject aag (fst slot) \<and> cleanup_info_wf c aag))))) s; s = sa\<rbrakk> \<Longrightarrow> sa = s \<and> (valid_list and valid_mdb and valid_objs and pas_refined aag and K (is_subject aag (fst slot) \<and> cleanup_info_wf c aag)) sa
theory CNode_AC

lemma reply_masters_mdbD1:
 "\<lbrakk> reply_masters_mdb m cs ; cs slot = Some (ReplyCap t True R) \<rbrakk>
    \<Longrightarrow> m slot = None" by (fastforce simp:reply_masters_mdb_def simp del:split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reply_masters_mdb m cs; cs slot = Some (ReplyCap t True R)\<rbrakk> \<Longrightarrow> m slot = None
theory CNode_AC

lemma reply_cap_no_grand_parent:
  "\<lbrakk> m \<Turnstile> pptr \<rightarrow>* slot ; reply_mdb m cs ; cs slot = Some (ReplyCap t False R) \<rbrakk>
     \<Longrightarrow> pptr = slot \<or> (m \<Turnstile> pptr \<leadsto> slot \<and> (\<exists> R'. cs pptr = Some (ReplyCap t True R')))" apply (clarsimp simp: reply_mdb_def del: disjCI) apply (erule(1) reply_caps_mdbE) apply (drule(1) reply_masters_mdbD1) apply (erule rtrancl.cases, blast) apply (erule rtrancl.cases, simp add: cdt_parent_of_def) apply (simp add: cdt_parent_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> pptr \<rightarrow>* slot; reply_mdb m cs; cs slot = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> pptr = slot \<or> m \<Turnstile> pptr \<leadsto> slot \<and> (\<exists>R'. cs pptr = Some (ReplyCap t True R')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> pptr \<rightarrow>* slot; cs slot = Some (ReplyCap t False R); reply_caps_mdb m cs; reply_masters_mdb m cs\<rbrakk> \<Longrightarrow> pptr = slot \<or> m \<Turnstile> pptr \<leadsto> slot \<and> (\<exists>R'. cs pptr = Some (ReplyCap t True R')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr R'. \<lbrakk>m \<Turnstile> pptr \<rightarrow>* slot; cs slot = Some (ReplyCap t False R); reply_masters_mdb m cs; m slot = Some ptr; cs ptr = Some (ReplyCap t True R')\<rbrakk> \<Longrightarrow> pptr = slot \<or> m \<Turnstile> pptr \<leadsto> slot \<and> (\<exists>R'. cs pptr = Some (ReplyCap t True R')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr R'. \<lbrakk>m \<Turnstile> pptr \<rightarrow>* slot; cs slot = Some (ReplyCap t False R); m slot = Some ptr; cs ptr = Some (ReplyCap t True R'); m ptr = None\<rbrakk> \<Longrightarrow> pptr = slot \<or> m \<Turnstile> pptr \<leadsto> slot \<and> (\<exists>R'. cs pptr = Some (ReplyCap t True R')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr R' a b c. \<lbrakk>cs slot = Some (ReplyCap t False R); m slot = Some ptr; cs ptr = Some (ReplyCap t True R'); m ptr = None; pptr = a; slot = c; m \<Turnstile> a \<rightarrow>* b; m \<Turnstile> b \<leadsto> c\<rbrakk> \<Longrightarrow> pptr = slot \<or> m \<Turnstile> pptr \<leadsto> slot \<and> (\<exists>R'. cs pptr = Some (ReplyCap t True R')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr R' a b c aa ba ca. \<lbrakk>cs slot = Some (ReplyCap t False R); m slot = Some ptr; cs ptr = Some (ReplyCap t True R'); m ptr = None; pptr = a; slot = c; m \<Turnstile> b \<leadsto> c; a = aa; b = ca; m \<Turnstile> aa \<rightarrow>* ba; m \<Turnstile> ba \<leadsto> ca\<rbrakk> \<Longrightarrow> pptr = slot \<or> m \<Turnstile> pptr \<leadsto> slot \<and> (\<exists>R'. cs pptr = Some (ReplyCap t True R')) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma set_cap_integrity_deletion[wp_transferable]:
  "\<lbrace>integrity aag X st and valid_mdb and valid_objs
                       and pas_refined aag and cdt_change_allowed' aag slot\<rbrace>
   set_cap NullCap slot
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (cases "is_subject aag (fst slot)") apply (wpsimp wp: set_cap_integrity_autarch) apply (wpsimp wp: set_cap_integrity_deletion_aux) by (fastforce dest: cca_to_transferable_or_subject simp: cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and valid_mdb and valid_objs and pas_refined aag and cdt_change_allowed' aag slot\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>integrity aag X st and valid_mdb and valid_objs and pas_refined aag and cdt_change_allowed' aag slot\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>integrity aag X st and valid_mdb and valid_objs and pas_refined aag and cdt_change_allowed' aag slot\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot) \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>integrity aag X st and valid_mdb and valid_objs and pas_refined aag and cdt_change_allowed' aag slot\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> pasSubject aag; integrity aag X st s; valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag slot s\<rbrakk> \<Longrightarrow> is_transferable_in slot s
theory CNode_AC

lemma update_cdt_list_pas_refined[wp]:
  "update_cdt_list f \<lbrace>pas_refined aag\<rbrace>" by (wpsimp simp: pas_refined_def state_objs_to_policy_def | wps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> update_cdt_list f \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory CNode_AC

lemma monad_commuteI2:
  "monad_commute P (f :: ('s, unit) nondet_monad) g \<Longrightarrow> (\<And>s. P s) \<Longrightarrow>
   (do f; g od) = (do g; f od)" by (monad_eq simp: monad_commute_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monad_commute P f g; \<And>s. P s\<rbrakk> \<Longrightarrow> do f;
g
od = do g;
f
od
theory CNode_AC

lemma modify_modify_commute:
  "monad_commute (\<lambda>s. f (g s) = g (f s)) (modify f) (modify g)" by (monad_eq simp: monad_commute_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>s. f (g s) = g (f s)) (modify f) (modify g)
theory CNode_AC

lemma modify_gets_commute:
  "monad_commute (\<lambda>s. g (f s) = g s) (modify f) (gets g)" by (monad_eq simp: monad_commute_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>s. g (f s) = g s) (modify f) (gets g)
theory CNode_AC

lemma set_eq_iff_imp:
  "(A = B) = ((\<forall>x. x \<in> A \<longrightarrow> x \<in> B) \<and> (\<forall>x. x \<in> B \<longrightarrow> x \<in> A))" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A = B) = ((\<forall>x. x \<in> A \<longrightarrow> x \<in> B) \<and> (\<forall>x. x \<in> B \<longrightarrow> x \<in> A))
theory CNode_AC

lemma put_as_modify:
  "put t = modify (\<lambda>_. t)" by monad_eq

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. put t = modify (\<lambda>_. t)
theory CNode_AC

lemma put_commuteI:
  "monad_commute P f (modify (\<lambda>_. t)) \<Longrightarrow> monad_commute P f (put t)" by (simp add: put_as_modify)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute P f (modify (\<lambda>_. t)) \<Longrightarrow> monad_commute P f (put t)
theory CNode_AC

lemma get_commuteI:
  "monad_commute P f (gets (\<lambda>s. s)) \<Longrightarrow> monad_commute P f get" by (simp add: gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute P f (gets (\<lambda>s. s)) \<Longrightarrow> monad_commute P f get
theory CNode_AC

lemma gets_gets_commute:
  "monad_commute \<top> (gets f) (gets g)" by (monad_eq simp: monad_commute_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (gets f) (gets g)
theory CNode_AC

lemma gets_get_commute:
  "(\<And>s0. \<lbrace>(=) s0\<rbrace> g \<lbrace>\<lambda>r t. s0 = t\<rbrace>) \<Longrightarrow>
   monad_commute \<top> (gets f) g" by (monad_eq simp: monad_commute_def valid_def) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s0. \<lbrace>(=) s0\<rbrace> g \<lbrace>\<lambda>r. (=) s0\<rbrace>) \<Longrightarrow> monad_commute (\<lambda>_. True) (gets f) g
theory CNode_AC

lemma assert_commute':
  "empty_fail f \<Longrightarrow> monad_commute \<top> (assert G) f" by (monad_eq simp: monad_commute_def empty_fail_def) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> monad_commute (\<lambda>_. True) (assert G) f
theory CNode_AC

lemma wpc_helper_monad_commute:
  "monad_commute P f g \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (monad_commute P f g)" by (clarsimp simp: wpc_helper_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute P f g \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (monad_commute P f g)
theory CNode_AC

lemma set_cdt_set_original_comm:
  "(do set_cdt c; set_original slot val od) =
   (do set_original slot val; set_cdt c od)" apply (clarsimp simp: set_cdt_def[folded modify_def]
                        set_original_def[folded gets_modify_def]
                        get_object_def set_object_def
                  simp del: K_bind_def) apply (simp only: modify_def[symmetric]) apply (rule monad_commuteI2) apply monad_commute_default apply monad_eq done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do set_cdt c;
set_original slot val
od = do set_original slot val;
set_cdt c
od proof (prove)
goal (1 subgoal):
 1. do do s <- get;
put (s\<lparr>cdt := c\<rparr>)
od;
r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(slot := val)))
od = do do r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(slot := val)))
od;
s <- get;
put (s\<lparr>cdt := c\<rparr>)
od proof (prove)
goal (1 subgoal):
 1. do modify (cdt_update (\<lambda>_. c));
r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(slot := val)))
od = do do r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(slot := val)))
od;
modify (cdt_update (\<lambda>_. c))
od proof (prove)
goal (2 subgoals):
 1. monad_commute ?P (modify (cdt_update (\<lambda>_. c))) (do r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(slot := val)))
od)
 2. \<And>s. ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. (\<forall>x. (\<exists>xa. xa \<in> fst (gets is_original_cap (s\<lparr>cdt := c\<rparr>)) \<and> x = fst xa) = (\<exists>xa. xa \<in> fst (gets is_original_cap s) \<and> x = fst xa)) \<and> snd (gets is_original_cap (s\<lparr>cdt := c\<rparr>)) = snd (gets is_original_cap s)) and (\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(slot := val), cdt := c\<rparr> = s\<lparr>cdt := c, is_original_cap := (is_original_cap s)(slot := val)\<rparr>)) s proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma K_bind_assoc:
  "(do (do f; g od); h od) = (do f; g; h od)" by (simp add: bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do do f;
g
od;
h
od = do f;
g;
h
od
theory CNode_AC

lemma aag_cap_auth_max_free_index_update[simp]:
  "aag_cap_auth aag (pasObjectAbs aag x) (max_free_index_update y) =
   aag_cap_auth aag (pasObjectAbs aag x) y" by (clarsimp simp: aag_cap_auth_def free_index_update_def cap_links_asid_slot_def cap_links_irq_def
              split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. aag_cap_auth aag (pasObjectAbs aag x) (max_free_index_update y) = aag_cap_auth aag (pasObjectAbs aag x) y
theory CNode_AC

lemma empty_slot_shuffle:
  "(do set_cdt c;
       empty_slot_ext slot slot_p;
       set_original slot False;
       set_cap NullCap slot;
       post_cap_deletion NullCap od) =
   (do set_cap NullCap slot;
       empty_slot_ext slot slot_p;
       set_original slot False;
       set_cdt c;
       post_cap_deletion NullCap od :: (det_ext state \<Rightarrow> _))" by (simp only: set_cdt_empty_slot_ext_comm[THEN K_bind_eqI', simplified K_bind_assoc]
                 set_cdt_set_original_comm[THEN K_bind_eqI', simplified K_bind_assoc]
                 set_cdt_set_cap_comm[THEN K_bind_eqI', simplified K_bind_assoc]
                 set_original_set_cap_comm[THEN K_bind_eqI', simplified K_bind_assoc]
                 set_cap_empty_slot_ext_comm[THEN K_bind_eqI', simplified K_bind_assoc])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do set_cdt c;
empty_slot_ext slot slot_p;
set_original slot False;
set_cap NullCap slot;
post_cap_deletion NullCap
od = do set_cap NullCap slot;
empty_slot_ext slot slot_p;
set_original slot False;
set_cdt c;
post_cap_deletion NullCap
od
theory CNode_AC

lemma pas_refined_original_cap_update[simp]:
  "pas_refined aag (is_original_cap_update f s) = pas_refined aag s" by (simp add: pas_refined_def state_objs_to_policy_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag (is_original_cap_update f s) = pas_refined aag s
theory CNode_AC

lemma pas_refined_machine_state_update[simp]:
  "pas_refined aag (machine_state_update f s) = pas_refined aag s" by (simp add: pas_refined_def state_objs_to_policy_def state_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag (machine_state_update f s) = pas_refined aag s
theory CNode_AC

lemma pas_refined_interrupt_states_update[simp]:
  "pas_refined aag (interrupt_states_update f s) = pas_refined aag s" by (simp add: pas_refined_def state_objs_to_policy_def state_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag (interrupt_states_update f s) = pas_refined aag s
theory CNode_AC

lemma update_cdt_pas_refined:
  "\<lbrace>pas_refined aag and (\<lambda>s. \<forall>x y. c (cdt s) x = Some y \<and> cdt s x \<noteq> Some y
                                   \<longrightarrow> (is_transferable (caps_of_state s x) \<or>
                                        abs_has_auth_to aag Control (fst y) (fst x))
                                     \<and> abs_has_auth_to aag DeleteDerived (fst y) (fst x))\<rbrace>
   update_cdt c
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: update_cdt_def) apply (wp set_cdt_pas_refined) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (\<lambda>s. \<forall>x y. c (cdt s) x = Some y \<and> cdt s x \<noteq> Some y \<longrightarrow> (is_transferable_in x s \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag)\<rbrace> update_cdt c \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (\<lambda>s. \<forall>a b aa. (\<exists>ba. c (cdt s) (a, b) = Some (aa, ba) \<and> cdt s (a, b) \<noteq> Some (aa, ba)) \<longrightarrow> (is_transferable_in (a, b) s \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag)\<rbrace> do t <- gets cdt;
set_cdt (c t)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and (\<lambda>s. \<forall>a b aa. (\<exists>ba. c (cdt s) (a, b) = Some (aa, ba) \<and> cdt s (a, b) \<noteq> Some (aa, ba)) \<longrightarrow> (is_transferable_in (a, b) s \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag)) s \<Longrightarrow> (pas_refined aag and (\<lambda>sa. \<forall>x y. c (cdt s) x = Some y \<and> cdt sa x \<noteq> Some y \<longrightarrow> (is_transferable_in x sa \<or> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag)) s proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma state_objs_to_policy_more_update[simp]:
  "state_objs_to_policy (trans_state f s) =
   state_objs_to_policy s" by (simp add: state_objs_to_policy_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_objs_to_policy (trans_state f s) = state_objs_to_policy s
theory CNode_AC

lemma set_untyped_cap_as_full_cdt_is_original_cap:
  "\<lbrace>\<lambda>s. P (cdt s) (is_original_cap s)\<rbrace>
   set_untyped_cap_as_full src_cap new_cap src_slot
   \<lbrace>\<lambda>_ s. P (cdt s) (is_original_cap s)\<rbrace>" unfolding set_untyped_cap_as_full_def apply (rule hoare_pre) apply (wp set_cap_caps_of_state2) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s) (is_original_cap s)\<rbrace> set_untyped_cap_as_full src_cap new_cap src_slot \<lbrace>\<lambda>_ s. P (cdt s) (is_original_cap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s) (is_original_cap s)\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap new_cap \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap then set_cap (max_free_index_update src_cap) src_slot else return () \<lbrace>\<lambda>_ s. P (cdt s) (is_original_cap s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap new_cap \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap then set_cap (max_free_index_update src_cap) src_slot else return () \<lbrace>\<lambda>_ s. P (cdt s) (is_original_cap s)\<rbrace>
 2. \<And>s. P (cdt s) (is_original_cap s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cdt s) (is_original_cap s) \<Longrightarrow> (is_untyped_cap src_cap \<and> is_untyped_cap new_cap \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap \<longrightarrow> P (cdt s) (is_original_cap s)) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap new_cap \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap) \<longrightarrow> P (cdt s) (is_original_cap s)) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma untyped_not_transferable:
  "is_untyped_cap cap \<Longrightarrow> \<not> is_transferable (Some cap)" by (fastforce simp: is_cap_simps elim!: is_transferable.cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_untyped_cap cap \<Longrightarrow> \<not> is_transferable_cap cap
theory CNode_AC

lemma is_transferable_max_free_index_update[simp]:
 "is_transferable (Some (max_free_index_update cap)) = is_transferable (Some cap)" by (simp add: is_transferable.simps free_index_update_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_transferable_cap (max_free_index_update cap) = is_transferable_cap cap
theory CNode_AC

lemma set_untyped_cap_as_full_is_transferable[wp]:
  "set_untyped_cap_as_full src_cap new_cap slot \<lbrace>\<lambda>s. \<not> is_transferable (caps_of_state s other_slot)\<rbrace>" apply (clarsimp simp: set_untyped_cap_as_full_def) apply wp using untyped_not_transferable max_free_index_update_preserve_untyped by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> is_transferable_in other_slot s\<rbrace> set_untyped_cap_as_full src_cap new_cap slot \<lbrace>\<lambda>_ s. \<not> is_transferable_in other_slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap new_cap; obj_ref_of src_cap = obj_ref_of new_cap; cap_bits_untyped src_cap = cap_bits_untyped new_cap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> is_transferable_in other_slot s\<rbrace> set_cap (max_free_index_update src_cap) slot \<lbrace>\<lambda>_ s. \<not> is_transferable_in other_slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap new_cap; obj_ref_of src_cap = obj_ref_of new_cap; cap_bits_untyped src_cap = cap_bits_untyped new_cap; \<not> is_transferable_in other_slot s\<rbrakk> \<Longrightarrow> \<not> is_transferable (((caps_of_state s)(slot \<mapsto> max_free_index_update src_cap)) other_slot) proof (prove)
using this:
is_untyped_cap ?cap \<Longrightarrow> \<not> is_transferable_cap ?cap
is_untyped_cap ?c \<Longrightarrow> is_untyped_cap (max_free_index_update ?c)

goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap new_cap; obj_ref_of src_cap = obj_ref_of new_cap; cap_bits_untyped src_cap = cap_bits_untyped new_cap; \<not> is_transferable_in other_slot s\<rbrakk> \<Longrightarrow> \<not> is_transferable (((caps_of_state s)(slot \<mapsto> max_free_index_update src_cap)) other_slot)
theory CNode_AC

lemma cap_links_irq_Nullcap [simp]:
  "cap_links_irq aag l NullCap" unfolding cap_links_irq_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_links_irq aag l NullCap proof (prove)
goal (1 subgoal):
 1. \<forall>irq\<in>cap_irqs_controlled NullCap. (l, Control, pasIRQAbs aag irq) \<in> pasPolicy aag
theory CNode_AC

lemma aag_cap_auth_NullCap [simp]:
  "aag_cap_auth aag l NullCap" unfolding aag_cap_auth_def by (simp add: clas_no_asid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. aag_cap_auth aag l NullCap proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>obj_refs_ac NullCap. \<forall>auth\<in>cap_auth_conferred NullCap. (l, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range NullCap. (l, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag l NullCap \<and> cap_links_irq aag l NullCap
theory CNode_AC

lemma cap_insert_pas_refined_not_transferable:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb
                    and not cte_wp_at is_transferable_cap src_slot
                    and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot)
                                                          \<and> pas_cap_cur_auth aag new_cap) \<rbrace>
   cap_insert new_cap src_slot dest_slot
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" by (wpsimp wp: cap_insert_pas_refined')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and not cte_wp_at is_transferable_cap src_slot and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)\<rbrace> cap_insert new_cap src_slot dest_slot \<lbrace>\<lambda>_. pas_refined aag\<rbrace>