kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_R

lemma createObjects_aligned2:
  "\<lbrace>\<lambda>s. is_aligned ptr (objBitsKO ko + gbits) \<and> n < 2 ^ word_bits \<and> n \<noteq> 0
      \<and> aln < word_bits
      \<and> aln = objBitsKO ko + gbits\<rbrace>
    createObjects ptr n ko gbits
   \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. is_aligned x aln\<rbrace>" apply (rule hoare_name_pre_state) apply simp apply (rule hoare_pre, wp createObjects_aligned, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned ptr (objBitsKO ko + gbits) \<and> n < 2 ^ word_bits \<and> n \<noteq> 0 \<and> aln < word_bits \<and> aln = objBitsKO ko + gbits\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. is_aligned x aln\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. is_aligned ptr (objBitsKO ko + gbits) \<and> n < 2 ^ word_bits \<and> n \<noteq> 0 \<and> aln < word_bits \<and> aln = objBitsKO ko + gbits \<Longrightarrow> \<lbrace>(=) s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. is_aligned x aln\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. is_aligned ptr (objBitsKO ko + gbits) \<and> n < 2 ^ word_bits \<and> 0 < n \<and> aln < word_bits \<and> aln = objBitsKO ko + gbits \<Longrightarrow> \<lbrace>(=) s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. is_aligned x (objBitsKO ko + gbits)\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_R

lemma range_cover_n_wb:
  "range_cover (ptr :: obj_ref) sz us n \<Longrightarrow> n < 2 ^ word_bits" apply (rule order_le_less_trans, erule range_cover.range_cover_n_le(2)) apply (clarsimp simp: range_cover_def) apply (simp add: word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz us n \<Longrightarrow> n < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz us n \<Longrightarrow> 2 ^ (sz - us) < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr us; sz < 32; us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> sz - us < word_bits proof (prove)
goal:
No subgoals!
theory Retype_R

lemma objBits_if_dev:
    "objBitsKO (if dev then KOUserDataDevice else KOUserData) = pageBits" by (simp add: objBitsKO_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. objBitsKO (if dev then KOUserDataDevice else KOUserData) = pageBits
theory Retype_R

lemma other_objs_default_relation:
  "\<lbrakk> case ty of Structures_A.EndpointObject \<Rightarrow> ko = injectKO (makeObject :: endpoint)
             | Structures_A.NotificationObject \<Rightarrow> ko = injectKO (makeObject :: Structures_H.notification)
             | Structures_A.TCBObject \<Rightarrow> ko = injectKO (makeObject :: tcb)
             | _ \<Rightarrow> False \<rbrakk> \<Longrightarrow>
    obj_relation_retype (default_object ty dev n) ko" apply (rule obj_relation_retype_other_obj) apply (clarsimp simp: default_object_def
                         is_other_obj_relation_type_def
                  split: Structures_A.apiobject_type.split_asm) apply (clarsimp simp: other_obj_relation_def default_object_def
                        ep_relation_def ntfn_relation_def
                        tcb_relation_def default_tcb_def makeObject_tcb
                        makeObject_cte new_context_def newContext_def
                        default_ep_def makeObject_endpoint default_notification_def
                        makeObject_notification default_ntfn_def
                        fault_rel_optionation_def
                        initContext_def
                        arch_tcb_context_get_def atcbContextGet_def
                        default_arch_tcb_def newArchTCB_def
                        arch_tcb_relation_def
                 split: Structures_A.apiobject_type.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. case ty of Structures_A.apiobject_type.TCBObject \<Rightarrow> ko = injectKO makeObject | Structures_A.apiobject_type.EndpointObject \<Rightarrow> ko = injectKO makeObject | Structures_A.apiobject_type.NotificationObject \<Rightarrow> ko = injectKO makeObject | _ \<Rightarrow> False \<Longrightarrow> obj_relation_retype (default_object ty dev n) ko proof (prove)
goal (2 subgoals):
 1. case ty of Structures_A.apiobject_type.TCBObject \<Rightarrow> ko = injectKO makeObject | Structures_A.apiobject_type.EndpointObject \<Rightarrow> ko = injectKO makeObject | Structures_A.apiobject_type.NotificationObject \<Rightarrow> ko = injectKO makeObject | _ \<Rightarrow> False \<Longrightarrow> is_other_obj_relation_type (a_type (default_object ty dev n))
 2. case ty of Structures_A.apiobject_type.TCBObject \<Rightarrow> ko = injectKO makeObject | Structures_A.apiobject_type.EndpointObject \<Rightarrow> ko = injectKO makeObject | Structures_A.apiobject_type.NotificationObject \<Rightarrow> ko = injectKO makeObject | _ \<Rightarrow> False \<Longrightarrow> other_obj_relation (default_object ty dev n) ko proof (prove)
goal (1 subgoal):
 1. case ty of Structures_A.apiobject_type.TCBObject \<Rightarrow> ko = injectKO makeObject | Structures_A.apiobject_type.EndpointObject \<Rightarrow> ko = injectKO makeObject | Structures_A.apiobject_type.NotificationObject \<Rightarrow> ko = injectKO makeObject | _ \<Rightarrow> False \<Longrightarrow> other_obj_relation (default_object ty dev n) ko proof (prove)
goal:
No subgoals!
theory Retype_R

lemma pagetable_relation_retype:
  "obj_relation_retype (default_object (ArchObject PageTableObj) dev n)
                       (KOArch (KOPTE makeObject))" apply (simp add: default_object_def default_arch_object_def
                   makeObject_pte obj_relation_retype_def
                   objBits_simps archObjSize_def
                   pte_relation_def) apply (clarsimp simp: range_composition[symmetric]
                        shiftl_t2n field_simps) apply (subst image_comp [symmetric, where g=ucast, unfolded o_def]) apply (simp add: ucast_range_less pteBits_def) apply (fastforce simp:pte_relation_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_relation_retype (default_object (ArchObject PageTableObj) dev n) (KOArch (KOPTE makeObject)) proof (prove)
goal (1 subgoal):
 1. pteBits \<le> 10 \<and> (\<forall>p. fst ` range (\<lambda>x. (p + (UCAST(8 \<rightarrow> 32) x << 2), \<lambda>ko ko'. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<exists>pte. ko' = KOArch (KOPTE pte) \<and> pte_relation_aligned x (pt x) pte))) = {p + x * 2 ^ pteBits |x. x < 2 ^ (10 - pteBits)}) \<and> (\<forall>x. pte_relation_aligned x ARM_A.InvalidPTE ARM_H.InvalidPTE) proof (prove)
goal (1 subgoal):
 1. pteBits \<le> 10 \<and> (\<forall>p. range (\<lambda>x. p + UCAST(8 \<rightarrow> 32) x * 4) = {p + x * 2 ^ pteBits |x. x < 2 ^ (10 - pteBits)}) \<and> (\<forall>x. pte_relation_aligned x ARM_A.InvalidPTE ARM_H.InvalidPTE) proof (prove)
goal (1 subgoal):
 1. pteBits \<le> 10 \<and> (\<forall>p. (\<lambda>a. p + a * 4) ` range UCAST(8 \<rightarrow> 32) = {p + x * 2 ^ pteBits |x. x < 2 ^ (10 - pteBits)}) \<and> (\<forall>x. pte_relation_aligned x ARM_A.InvalidPTE ARM_H.InvalidPTE) proof (prove)
goal (1 subgoal):
 1. (\<forall>p. (\<lambda>x. p + x * 4) ` {x. x < 0x100} = {p + x * 4 |x. x < 0x100}) \<and> (\<forall>x. pte_relation_aligned x ARM_A.InvalidPTE ARM_H.InvalidPTE) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma pagedirectory_relation_retype:
  "obj_relation_retype (default_object (ArchObject PageDirectoryObj) dev n)
                       (KOArch (KOPDE makeObject))" apply (simp add: default_object_def default_arch_object_def
                   makeObject_pde obj_relation_retype_def
                   objBits_simps archObjSize_def
                   pde_relation_def) apply (clarsimp simp: range_composition[symmetric]
                        shiftl_t2n field_simps) apply (subst image_comp [symmetric, where g=ucast, unfolded o_def]) apply (simp add: ucast_range_less pdeBits_def) apply (fastforce simp:pde_relation_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_relation_retype (default_object (ArchObject PageDirectoryObj) dev n) (KOArch (KOPDE makeObject)) proof (prove)
goal (1 subgoal):
 1. pdeBits \<le> 14 \<and> (\<forall>p. fst ` range (\<lambda>x. (p + (UCAST(12 \<rightarrow> 32) x << 2), \<lambda>ko ko'. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<exists>pde. ko' = KOArch (KOPDE pde) \<and> pde_relation_aligned x (pd x) pde))) = {p + x * 2 ^ pdeBits |x. x < 2 ^ (14 - pdeBits)}) \<and> (\<forall>x. pde_relation_aligned x ARM_A.InvalidPDE ARM_H.InvalidPDE) proof (prove)
goal (1 subgoal):
 1. pdeBits \<le> 14 \<and> (\<forall>p. range (\<lambda>x. p + UCAST(12 \<rightarrow> 32) x * 4) = {p + x * 2 ^ pdeBits |x. x < 2 ^ (14 - pdeBits)}) \<and> (\<forall>x. pde_relation_aligned x ARM_A.InvalidPDE ARM_H.InvalidPDE) proof (prove)
goal (1 subgoal):
 1. pdeBits \<le> 14 \<and> (\<forall>p. (\<lambda>a. p + a * 4) ` range UCAST(12 \<rightarrow> 32) = {p + x * 2 ^ pdeBits |x. x < 2 ^ (14 - pdeBits)}) \<and> (\<forall>x. pde_relation_aligned x ARM_A.InvalidPDE ARM_H.InvalidPDE) proof (prove)
goal (1 subgoal):
 1. (\<forall>p. (\<lambda>x. p + x * 4) ` {x. x < 0x1000} = {p + x * 4 |x. x < 0x1000}) \<and> (\<forall>x. pde_relation_aligned x ARM_A.InvalidPDE ARM_H.InvalidPDE) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma init_arch_objects_APIType_map2:
  "init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs =
     (case ty of APIObjectType _ \<Rightarrow> return ()
   | _ \<Rightarrow> init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs)" apply (clarsimp split: ARM_H.object_type.split) apply (simp add: init_arch_objects_def APIType_map2_def
            split: apiobject_type.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs = (case ty of APIObjectType x \<Rightarrow> return () | _ \<Rightarrow> init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs) proof (prove)
goal (1 subgoal):
 1. \<And>x1. ty = APIObjectType x1 \<Longrightarrow> init_arch_objects (APIType_map2 (Inr (APIObjectType x1))) ptr bits sz refs = return () proof (prove)
goal:
No subgoals!
theory Retype_R

lemma copyGlobalMappings_cte_wp_at[wp]:
  "\<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace>
     copyGlobalMappings pd
   \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>" apply (simp add: copyGlobalMappings_def) apply (wp mapM_x_wp') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> copyGlobalMappings pd \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (pd + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_R

lemma nullPointer_0_simp[simp]:
  "(nullPointer = 0) = True" by (simp add: nullPointer_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (nullPointer = 0) = True
theory Retype_R

lemma capRange_Null [simp]: "capRange NullCap = {}" by (simp add: capRange_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange capability.NullCap = {}
theory Retype_R

lemma no_0_n: "no_0 n" using no_0 by (simp add: no_0_def n_def 0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 n proof (prove)
using this:
no_0 m

goal (1 subgoal):
 1. no_0 n
theory Retype_R

lemma n_next:
  "n \<turnstile> c \<leadsto> c' = (if P c then c' = 0 else m \<turnstile> c \<leadsto> c')" by (simp add: mdb_next_unfold n_def makeObject_cte nullPointer_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> c \<leadsto> c' = (if P c then c' = 0 else m \<turnstile> c \<leadsto> c')
theory Retype_R

lemma n_prev:
  "n \<turnstile> c \<leftarrow> c' = (if P c' then c = 0 else m \<turnstile> c \<leftarrow> c')" by (simp add: mdb_prev_def n_def makeObject_cte nullPointer_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> c \<leftarrow> c' = (if P c' then c = 0 else m \<turnstile> c \<leftarrow> c')
theory Retype_R

lemma next_not_P:
  "m \<turnstile> c \<leadsto> c' \<Longrightarrow> \<not>P c" by (clarsimp simp: mdb_next_unfold dest!: P)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> c \<leadsto> c' \<Longrightarrow> \<not> P c
theory Retype_R

lemma m_next_trancl:
  "m \<turnstile> c \<leadsto>\<^sup>+ c' \<Longrightarrow> n \<turnstile> c \<leadsto>\<^sup>+ c'" apply (erule trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp: n_next) apply (drule next_not_P) apply simp apply (erule trancl_trans) apply (rule r_into_trancl) apply (clarsimp simp: n_next) apply (drule next_not_P) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> c \<leadsto>\<^sup>+ c' \<Longrightarrow> n \<turnstile> c \<leadsto>\<^sup>+ c' proof (prove)
goal (2 subgoals):
 1. \<And>y. m \<turnstile> c \<leadsto> y \<Longrightarrow> n \<turnstile> c \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> n \<turnstile> c \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. m \<turnstile> c \<leadsto> y \<Longrightarrow> n \<turnstile> c \<leadsto> y
 2. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> n \<turnstile> c \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m \<turnstile> c \<leadsto> y; P c\<rbrakk> \<Longrightarrow> y = 0
 2. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> n \<turnstile> c \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>P c; \<not> P c\<rbrakk> \<Longrightarrow> y = 0
 2. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> n \<turnstile> c \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> n \<turnstile> c \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z\<rbrakk> \<Longrightarrow> n \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z\<rbrakk> \<Longrightarrow> n \<turnstile> y \<leadsto> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; P y\<rbrakk> \<Longrightarrow> z = 0 proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; P y; \<not> P y\<rbrakk> \<Longrightarrow> z = 0 proof (prove)
goal:
No subgoals!
theory Retype_R

lemma P_to_0:
  "P c \<Longrightarrow> n \<turnstile> c \<leadsto>\<^sup>+ 0" by (rule r_into_trancl) (simp add: n_next)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P c \<Longrightarrow> n \<turnstile> c \<leadsto>\<^sup>+ 0
theory Retype_R

lemma n_trancl_eq:
  "n \<turnstile> c \<leadsto>\<^sup>+ c' = (if P c then c' = 0 else m \<turnstile> c \<leadsto>\<^sup>+ c')" by (auto dest: m_next_trancl n_next_trancl P_to_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> c \<leadsto>\<^sup>+ c' = (if P c then c' = 0 else m \<turnstile> c \<leadsto>\<^sup>+ c')
theory Retype_R

lemma n_rtrancl_eq:
  "n \<turnstile> c \<leadsto>\<^sup>* c' = (if P c then c' = 0 \<or> c = c' else m \<turnstile> c \<leadsto>\<^sup>* c')" by (auto simp: n_trancl_eq rtrancl_eq_or_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> c \<leadsto>\<^sup>* c' = (if P c then c' = 0 \<or> c = c' else m \<turnstile> c \<leadsto>\<^sup>* c')
theory Retype_R

lemma dom_n:
  "dom n = dom m \<union> Collect P" by (auto simp add: n_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom n = dom m \<union> Collect P
theory Retype_R

lemma mdb_chain_0_n: "mdb_chain_0 n" using chain by (auto simp: mdb_chain_0_def dom_n n_trancl_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 n proof (prove)
using this:
mdb_chain_0 m

goal (1 subgoal):
 1. mdb_chain_0 n
theory Retype_R

lemma n_Some_eq:
  "(n p = Some (CTE cap node)) =
  (if P p then cap = NullCap \<and> node = nullMDBNode
          else m p = Some (CTE cap node))" by (auto simp: n_def makeObject_cte)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n p = Some (CTE cap node)) = (if P p then cap = capability.NullCap \<and> node = nullMDBNode else m p = Some (CTE cap node))
theory Retype_R

lemma valid_badges_n: "valid_badges n" proof - from valid have "valid_badges m" .. thus ?thesis apply (clarsimp simp: valid_badges_def) apply (simp add: n_Some_eq n_next split: if_split_asm) apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_badges n proof (state)
goal (1 subgoal):
 1. valid_badges n proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_badges m proof (state)
this:
valid_badges m

goal (1 subgoal):
 1. valid_badges n proof (prove)
using this:
valid_badges m

goal (1 subgoal):
 1. valid_badges n proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>\<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); n p = Some (CTE cap node); n p' = Some (CTE cap' node'); n \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>m \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; \<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node')); \<not> P p; m p = Some (CTE cap node); \<not> P p'; m p' = Some (CTE cap' node')\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal:
No subgoals! proof (state)
this:
valid_badges n

goal:
No subgoals!