kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_AI

lemma weak_derived_cte_refs_abs:
  "weak_derived c c' \<Longrightarrow> cte_refs c' = cte_refs c" apply (clarsimp simp: weak_derived_def copy_of_def) apply (auto simp: same_object_as_def is_cap_simps bits_of_def
             split: if_split_asm cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived c c' \<Longrightarrow> cte_refs c' = cte_refs c proof (prove)
goal (1 subgoal):
 1. (if is_untyped_cap c' then c' = c else same_object_as c' c \<and> is_reply_cap c' = is_reply_cap c \<and> is_master_reply_cap c' = is_master_reply_cap c) \<and> cap_asid c = cap_asid c' \<and> cap_asid_base c = cap_asid_base c' \<and> cap_vptr c = cap_vptr c' \<or> c' = c \<Longrightarrow> cte_refs c' = cte_refs c proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_move_src_slot_Null:
  "\<lbrace>cte_at src and K(src \<noteq> dest)\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_ s. cte_wp_at ((=) cap.NullCap) src s\<rbrace>" unfolding cap_move_def by (wp set_cdt_cte_wp_at set_cap_cte_wp_at' | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) src and K (src \<noteq> dest)\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. cte_wp_at ((=) NullCap) src\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) src and K (src \<noteq> dest)\<rbrace> do set_cap cap dest;
set_cap NullCap src;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
parent <- return $ cdt src;
cdt' <- return $ cdt(dest := parent, src := None);
set_cdt (\<lambda>r. if cdt' r = Some src then Some dest else cdt' r);
do_extended_op (cap_move_ext src dest src_p dest_p);
is_original <- gets is_original_cap;
set_original dest (is_original src);
set_original src False
od \<lbrace>\<lambda>_. cte_wp_at ((=) NullCap) src\<rbrace>
theory CNodeInv_AI

lemma is_final_cap_is_final[wp]:
  "\<lbrace>\<top>\<rbrace> is_final_cap cap \<lbrace>\<lambda>rv s. rv = is_final_cap' cap s\<rbrace>" unfolding is_final_cap_def by wp simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> is_final_cap cap \<lbrace>\<lambda>rv s. rv = is_final_cap' cap s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> gets (is_final_cap' cap) \<lbrace>\<lambda>rv s. rv = is_final_cap' cap s\<rbrace>
theory CNodeInv_AI

lemma real_cte_not_reply_masterD:
  "\<And>P ptr.
   \<lbrakk> real_cte_at ptr s; valid_reply_masters s; valid_objs s \<rbrakk> \<Longrightarrow>
   cte_wp_at (\<lambda>cap. \<not> is_master_reply_cap cap) ptr s" apply clarsimp apply (subgoal_tac "\<not> tcb_at a s") apply (clarsimp simp: cap_table_at_cte_at cte_wp_at_not_reply_master) apply (clarsimp simp: obj_at_def is_tcb is_cap_table) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P ptr. \<lbrakk>real_cte_at ptr s; valid_reply_masters s; valid_objs s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<not> is_master_reply_cap cap) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cap_table_at (length b) a s; valid_reply_masters s; valid_objs s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<not> is_master_reply_cap cap) (a, b) s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cap_table_at (length b) a s; valid_reply_masters s; valid_objs s; \<not> tcb_at a s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<not> is_master_reply_cap cap) (a, b) s
 2. \<And>a b. \<lbrakk>cap_table_at (length b) a s; valid_reply_masters s; valid_objs s\<rbrakk> \<Longrightarrow> \<not> tcb_at a s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cap_table_at (length b) a s; valid_reply_masters s; valid_objs s\<rbrakk> \<Longrightarrow> \<not> tcb_at a s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma real_cte_weak_derived_not_reply_masterD:
  "\<And>cap ptr.
   \<lbrakk> cte_wp_at (weak_derived cap) ptr s; real_cte_at ptr s;
     valid_reply_masters s; valid_objs s \<rbrakk> \<Longrightarrow>
   \<not> is_master_reply_cap cap" by (fastforce simp: cte_wp_at_caps_of_state weak_derived_replies
              dest!: real_cte_not_reply_masterD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cap ptr. \<lbrakk>cte_wp_at (weak_derived cap) ptr s; real_cte_at ptr s; valid_reply_masters s; valid_objs s\<rbrakk> \<Longrightarrow> \<not> is_master_reply_cap cap
theory CNodeInv_AI

lemma real_cte_is_derived_not_replyD:
  "\<And>m p cap ptr.
   \<lbrakk> cte_wp_at (is_derived m p cap) ptr s; real_cte_at ptr s;
     valid_reply_masters s; valid_objs s \<rbrakk> \<Longrightarrow>
   \<not> is_reply_cap cap" by (fastforce simp: cte_wp_at_caps_of_state is_derived_def
              dest!: real_cte_not_reply_masterD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m p cap ptr. \<lbrakk>cte_wp_at (is_derived m p cap) ptr s; real_cte_at ptr s; valid_reply_masters s; valid_objs s\<rbrakk> \<Longrightarrow> \<not> is_reply_cap cap
theory CNodeInv_AI

lemma cap_irqs_is_derived:
  "is_derived m ptr cap cap' \<Longrightarrow> cap_irqs cap = cap_irqs cap'" by (clarsimp simp: is_derived_def cap_master_cap_irqs split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m ptr cap cap' \<Longrightarrow> cap_irqs cap = cap_irqs cap'
theory CNodeInv_AI

lemma tcb_cap_valid_mdb[simp]:
  "tcb_cap_valid cap p (cdt_update mfn s) = tcb_cap_valid cap p s" by (simp add: tcb_cap_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid cap p (cdt_update mfn s) = tcb_cap_valid cap p s
theory CNodeInv_AI

lemma tcb_cap_valid_is_original_cap[simp]:
  "tcb_cap_valid cap p (is_original_cap_update mfn s) = tcb_cap_valid cap p s" by (simp add: tcb_cap_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid cap p (is_original_cap_update mfn s) = tcb_cap_valid cap p s
theory CNodeInv_AI

lemma corres_underlying_lift_ex1:
  assumes c: "\<And>v. corres_underlying sr nf nf' r (P v and Q) P' a c"
  shows "corres_underlying sr nf nf' r ((\<lambda>s. \<exists>v. P v s) and Q) P' a c" unfolding corres_underlying_def apply clarsimp apply (cut_tac v = v in c) apply (auto simp: corres_underlying_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r ((\<lambda>s. \<exists>v. P v s) and Q) P' a c proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>sr. ((\<lambda>s. \<exists>v. P v s) and Q) s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (c s'). \<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c s')) proof (prove)
goal (1 subgoal):
 1. \<And>aa b v. \<lbrakk>(aa, b) \<in> sr; P v aa; Q aa; P' b; nf \<longrightarrow> \<not> snd (a aa)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c b)) proof (prove)
goal (1 subgoal):
 1. \<And>aa b v. \<lbrakk>(aa, b) \<in> sr; P v aa; Q aa; P' b; nf \<longrightarrow> \<not> snd (a aa); corres_underlying sr nf nf' r (P v and Q) P' a c\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c b)) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma corres_underlying_lift_ex2:
  assumes c: "\<And>v. corres_underlying sr nf nf' r P (P' v and Q) a c"
  shows "corres_underlying sr nf nf' r P ((\<lambda>s. \<exists>v. P' v s) and Q) a c" unfolding corres_underlying_def apply clarsimp apply (cut_tac v = v in c) apply (auto simp: corres_underlying_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P ((\<lambda>s. \<exists>v. P' v s) and Q) a c proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>sr. P s \<and> ((\<lambda>s. \<exists>v. P' v s) and Q) s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (c s'). \<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c s')) proof (prove)
goal (1 subgoal):
 1. \<And>aa b v. \<lbrakk>(aa, b) \<in> sr; P aa; Q b; P' v b; nf \<longrightarrow> \<not> snd (a aa)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c b)) proof (prove)
goal (1 subgoal):
 1. \<And>aa b v. \<lbrakk>(aa, b) \<in> sr; P aa; Q b; P' v b; nf \<longrightarrow> \<not> snd (a aa); corres_underlying sr nf nf' r P (P' v and Q) a c\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c b)) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma real_cte_halted_if_tcb[simp]:
  "real_cte_at (a, b) s \<Longrightarrow> halted_if_tcb a s" by (clarsimp simp: halted_if_tcb_def obj_at_def is_cap_table is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. real_cte_at (a, b) s \<Longrightarrow> halted_if_tcb a s
theory CNodeInv_AI

lemma descendants_of_empty:
  "x \<notin> descendants_of cref Map.empty" by (simp add: descendants_of_def cdt_parent_rel_def is_cdt_parent_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> descendants_of cref (\<lambda>x. None)
theory CNodeInv_AI

lemma has_parent_cte_at:"valid_mdb s \<Longrightarrow> (cdt s) c = Some p \<Longrightarrow> cte_at c s" apply (rule cte_wp_cte_at) apply (simp add: valid_mdb_def mdb_cte_at_def del: split_paired_All) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; cdt s c = Some p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) c s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; cdt s c = Some p\<rbrakk> \<Longrightarrow> cte_wp_at ?P c s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p c. cdt s c = Some p \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) p s \<and> cte_wp_at ((\<noteq>) NullCap) c s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s c = Some p\<rbrakk> \<Longrightarrow> cte_wp_at ?P c s proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma set_cap_in_device_frame[wp]:
  "\<lbrace>in_device_frame buffer\<rbrace> set_cap cap ref \<lbrace>\<lambda>_. in_device_frame buffer\<rbrace>" by (simp add: in_device_frame_def) (wp hoare_vcg_ex_lift set_cap_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_device_frame buffer\<rbrace> set_cap cap ref \<lbrace>\<lambda>_. in_device_frame buffer\<rbrace>
theory ArchCNodeInv_AI

lemma derive_cap_objrefs [CNodeInv_AI_assms]:
  "\<lbrace>\<lambda>s. P (obj_refs cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv)\<rbrace>,-" by (wpsimp simp: arch_derive_cap_def derive_cap_def) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_refs cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv)\<rbrace>, -
theory ArchCNodeInv_AI

lemma derive_cap_zobjrefs [CNodeInv_AI_assms]:
  "\<lbrace>\<lambda>s. P (zobj_refs cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (zobj_refs rv)\<rbrace>,-" by (wpsimp simp: arch_derive_cap_def derive_cap_def) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (zobj_refs cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (zobj_refs rv)\<rbrace>, -
theory ArchCNodeInv_AI

lemma update_cap_objrefs [CNodeInv_AI_assms]:
  "\<lbrakk> update_cap_data P dt cap \<noteq> NullCap \<rbrakk> \<Longrightarrow>
     obj_refs (update_cap_data P dt cap) = obj_refs cap" by (case_tac cap,
      simp_all add: update_cap_data_closedform arch_update_cap_data_def
             split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_cap_data P dt cap \<noteq> NullCap \<Longrightarrow> obj_refs (update_cap_data P dt cap) = obj_refs cap
theory ArchCNodeInv_AI

lemma update_cap_zobjrefs [CNodeInv_AI_assms]:
  "\<lbrakk> update_cap_data P dt cap \<noteq> cap.NullCap \<rbrakk> \<Longrightarrow>
     zobj_refs (update_cap_data P dt cap) = zobj_refs cap" apply (case_tac cap,
      simp_all add: update_cap_data_closedform arch_update_cap_data_def
             split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_cap_data P dt cap \<noteq> NullCap \<Longrightarrow> zobj_refs (update_cap_data P dt cap) = zobj_refs cap proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma weak_derived_cap_is_device[CNodeInv_AI_assms]:
  "\<lbrakk>weak_derived c' c\<rbrakk> \<Longrightarrow>  cap_is_device c = cap_is_device c'" apply (auto simp: weak_derived_def copy_of_def is_cap_simps
                    same_object_as_def2
             split: if_split_asm
             dest!: master_cap_eq_is_device_cap_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived c' c \<Longrightarrow> cap_is_device c = cap_is_device c' proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma cap_asid_update_cap_data [CNodeInv_AI_assms]:
  "update_cap_data P x c \<noteq> NullCap
         \<Longrightarrow> cap_asid (update_cap_data P x c) = cap_asid c" apply (simp add: update_cap_data_def split del: if_split split: if_split_asm) apply (auto simp: is_cap_simps Let_def the_cnode_cap_def cap_master_cap_def
                    badge_update_def arch_update_cap_data_def
             split: arch_cap.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_cap_data P x c \<noteq> NullCap \<Longrightarrow> cap_asid (update_cap_data P x c) = cap_asid c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_ep_cap c; cap_ep_badge c = 0; \<not> P; badge_update x c \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_asid (badge_update x c) = cap_asid c
 2. \<lbrakk>\<not> is_ep_cap c; is_ntfn_cap c; cap_ep_badge c = 0; \<not> P; badge_update x c \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_asid (badge_update x c) = cap_asid c
 3. \<lbrakk>\<not> is_ep_cap c; \<not> is_ntfn_cap c; is_cnode_cap c; (case the_cnode_cap c of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((x >> 3) && mask 5) + bits then NullCap else CNodeCap oref bits (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))) \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_asid (case the_cnode_cap c of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((x >> 3) && mask 5) + bits then NullCap else CNodeCap oref bits (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))) = cap_asid c
 4. \<lbrakk>\<not> is_ep_cap c; \<not> is_ntfn_cap c; \<not> is_cnode_cap c; is_arch_cap c; arch_update_cap_data P x (the_arch_cap c) \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_asid (arch_update_cap_data P x (the_arch_cap c)) = cap_asid c proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma cap_vptr_update_cap_data [CNodeInv_AI_assms]:
  "update_cap_data P x c \<noteq> NullCap
         \<Longrightarrow> cap_vptr (update_cap_data P x c) = cap_vptr c" apply (simp add: update_cap_data_def split del: if_split split: if_split_asm) apply (auto simp: is_cap_simps Let_def the_cnode_cap_def cap_master_cap_def
                    badge_update_def arch_update_cap_data_def
             split: arch_cap.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_cap_data P x c \<noteq> NullCap \<Longrightarrow> cap_vptr (update_cap_data P x c) = cap_vptr c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_ep_cap c; cap_ep_badge c = 0; \<not> P; badge_update x c \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_vptr (badge_update x c) = cap_vptr c
 2. \<lbrakk>\<not> is_ep_cap c; is_ntfn_cap c; cap_ep_badge c = 0; \<not> P; badge_update x c \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_vptr (badge_update x c) = cap_vptr c
 3. \<lbrakk>\<not> is_ep_cap c; \<not> is_ntfn_cap c; is_cnode_cap c; (case the_cnode_cap c of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((x >> 3) && mask 5) + bits then NullCap else CNodeCap oref bits (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))) \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_vptr (case the_cnode_cap c of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((x >> 3) && mask 5) + bits then NullCap else CNodeCap oref bits (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))) = cap_vptr c
 4. \<lbrakk>\<not> is_ep_cap c; \<not> is_ntfn_cap c; \<not> is_cnode_cap c; is_arch_cap c; arch_update_cap_data P x (the_arch_cap c) \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_vptr (arch_update_cap_data P x (the_arch_cap c)) = cap_vptr c proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma cap_asid_base_update_cap_data [CNodeInv_AI_assms]:
  "update_cap_data P x c \<noteq> NullCap
         \<Longrightarrow> cap_asid_base (update_cap_data P x c) = cap_asid_base c" apply (simp add: update_cap_data_def split del: if_split split: if_split_asm) apply (auto simp: is_cap_simps Let_def the_cnode_cap_def cap_master_cap_def
                    badge_update_def arch_update_cap_data_def
             split: arch_cap.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_cap_data P x c \<noteq> NullCap \<Longrightarrow> cap_asid_base (update_cap_data P x c) = cap_asid_base c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_ep_cap c; cap_ep_badge c = 0; \<not> P; badge_update x c \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_asid_base (badge_update x c) = cap_asid_base c
 2. \<lbrakk>\<not> is_ep_cap c; is_ntfn_cap c; cap_ep_badge c = 0; \<not> P; badge_update x c \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_asid_base (badge_update x c) = cap_asid_base c
 3. \<lbrakk>\<not> is_ep_cap c; \<not> is_ntfn_cap c; is_cnode_cap c; (case the_cnode_cap c of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((x >> 3) && mask 5) + bits then NullCap else CNodeCap oref bits (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))) \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_asid_base (case the_cnode_cap c of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((x >> 3) && mask 5) + bits then NullCap else CNodeCap oref bits (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))) = cap_asid_base c
 4. \<lbrakk>\<not> is_ep_cap c; \<not> is_ntfn_cap c; \<not> is_cnode_cap c; is_arch_cap c; arch_update_cap_data P x (the_arch_cap c) \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_asid_base (arch_update_cap_data P x (the_arch_cap c)) = cap_asid_base c proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma is_reply_update_cap_data [simp]:
  "is_reply_cap (update_cap_data P x c) = is_reply_cap c" by (simp add:is_reply_cap_def update_cap_data_def arch_update_cap_data_def the_cnode_cap_def
               is_arch_cap_def badge_update_def split:cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_reply_cap (update_cap_data P x c) = is_reply_cap c
theory ArchCNodeInv_AI

lemma is_master_reply_update_cap_data[simp]:
  "is_master_reply_cap (update_cap_data P x c) = is_master_reply_cap c" by (simp add:is_master_reply_cap_def update_cap_data_def arch_update_cap_data_def
               the_cnode_cap_def is_arch_cap_def badge_update_def split:cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_master_reply_cap (update_cap_data P x c) = is_master_reply_cap c
theory ArchCNodeInv_AI

lemma cap_badge_update_cap_data [CNodeInv_AI_assms]:
  "update_cap_data False x c \<noteq> NullCap \<and> (bdg, cap_badge c) \<in> capBadge_ordering False
       \<longrightarrow> (bdg, cap_badge (update_cap_data False x c)) \<in> capBadge_ordering False" apply clarsimp apply (erule capBadge_ordering_trans) apply (simp add: update_cap_data_def split del: if_split split: if_split_asm) apply (auto simp: is_cap_simps Let_def the_cnode_cap_def cap_master_cap_def
                    badge_update_def arch_update_cap_data_def
             split: arch_cap.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_cap_data False x c \<noteq> NullCap \<and> (bdg, cap_badge c) \<in> capBadge_ordering False \<longrightarrow> (bdg, cap_badge (update_cap_data False x c)) \<in> capBadge_ordering False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>update_cap_data False x c \<noteq> NullCap; (bdg, cap_badge c) \<in> capBadge_ordering False\<rbrakk> \<Longrightarrow> (bdg, cap_badge (update_cap_data False x c)) \<in> capBadge_ordering False proof (prove)
goal (1 subgoal):
 1. update_cap_data False x c \<noteq> NullCap \<Longrightarrow> (cap_badge c, cap_badge (update_cap_data False x c)) \<in> capBadge_ordering False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_ep_cap c; cap_ep_badge c = 0; badge_update x c \<noteq> NullCap\<rbrakk> \<Longrightarrow> (cap_badge c, cap_badge (badge_update x c)) \<in> capBadge_ordering False
 2. \<lbrakk>\<not> is_ep_cap c; is_ntfn_cap c; cap_ep_badge c = 0; badge_update x c \<noteq> NullCap\<rbrakk> \<Longrightarrow> (cap_badge c, cap_badge (badge_update x c)) \<in> capBadge_ordering False
 3. \<lbrakk>\<not> is_ep_cap c; \<not> is_ntfn_cap c; is_cnode_cap c; (case the_cnode_cap c of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((x >> 3) && mask 5) + bits then NullCap else CNodeCap oref bits (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))) \<noteq> NullCap\<rbrakk> \<Longrightarrow> (cap_badge c, cap_badge (case the_cnode_cap c of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((x >> 3) && mask 5) + bits then NullCap else CNodeCap oref bits (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18))))) \<in> capBadge_ordering False
 4. \<lbrakk>\<not> is_ep_cap c; \<not> is_ntfn_cap c; \<not> is_cnode_cap c; is_arch_cap c; arch_update_cap_data False x (the_arch_cap c) \<noteq> NullCap\<rbrakk> \<Longrightarrow> (cap_badge c, cap_badge (arch_update_cap_data False x (the_arch_cap c))) \<in> capBadge_ordering False proof (prove)
goal:
No subgoals!
theory ArchCNodeInv_AI

lemma cap_vptr_rights_update[simp, CNodeInv_AI_assms]:
  "cap_vptr (cap_rights_update f c) = cap_vptr c" by (simp add: cap_vptr_def cap_rights_update_def acap_rights_update_def
           split: cap.splits arch_cap.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_vptr (cap_rights_update f c) = cap_vptr c
theory ArchCNodeInv_AI

lemma cap_vptr_mask[simp, CNodeInv_AI_assms]:
  "cap_vptr (mask_cap m c) = cap_vptr c" by (simp add: mask_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_vptr (mask_cap m c) = cap_vptr c
theory ArchCNodeInv_AI

lemma cap_asid_base_rights [simp, CNodeInv_AI_assms]:
  "cap_asid_base (cap_rights_update R c) = cap_asid_base c" by (auto simp add: cap_rights_update_def acap_rights_update_def
           split: cap.splits arch_cap.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_asid_base (cap_rights_update R c) = cap_asid_base c
theory ArchCNodeInv_AI

lemma cap_asid_base_mask[simp, CNodeInv_AI_assms]:
  "cap_asid_base (mask_cap m c) = cap_asid_base c" by (simp add: mask_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_asid_base (mask_cap m c) = cap_asid_base c