theory Example_Valid_StateH

lemma valid_caps_s0H[simp]:
  notes pdeBits_def[simp] objBits_defs[simp]
  shows
  "valid_cap' NullCap s0H_internal"
  "valid_cap' (ThreadCap Low_tcb_ptr) s0H_internal"
  "valid_cap' (ThreadCap High_tcb_ptr) s0H_internal"
  "valid_cap' (CNodeCap Low_cnode_ptr 10 2 10) s0H_internal"
  "valid_cap' (CNodeCap High_cnode_ptr 10 2 10) s0H_internal"
  "valid_cap' (CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal"
  "valid_cap' (ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal"
  "valid_cap' (ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal"
  "valid_cap' (NotificationCap ntfn_ptr 0 True False) s0H_internal"
  "valid_cap' (NotificationCap ntfn_ptr 0 False True) s0H_internal"
  "valid_cap' (ReplyCap Low_tcb_ptr True True) s0H_internal"
  "valid_cap' (ReplyCap High_tcb_ptr True True) s0H_internal" supply option.case_cong[cong] if_cong[cong] apply (simp
        | simp add: valid_cap'_def s0H_internal_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def projectKO_eq project_inject,
          intro conjI,
             simp add: objBitsKO_def s0_ptrs_aligned,
            simp add: objBitsKO_def,
           simp add: objBitsKO_def s0_ptrs_aligned mask_def,
          rule pspace_distinctD'[OF _ s0H_pspace_distinct', simplified s0H_internal_def],
          simp)+ apply (simp add: valid_cap'_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def projectKO_eq project_inject) apply (intro conjI) apply (simp add: objBitsKO_def s0_ptrs_aligned) apply (simp add: objBitsKO_def) apply (simp add: objBitsKO_def s0_ptrs_aligned mask_def) apply (clarsimp simp: Low_cte_def Low_cte'_def Low_capsH_def cnode_offs_min2 cnode_offs_max2 cnode_offs_aligned2 add.commute s0_ptrs_aligned cte_level_bits_def objBitsKO_def empty_cte_def) apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct', simplified cte_level_bits_def]) apply (simp add: Low_cte_def Low_cte'_def Low_capsH_def empty_cte_def cnode_offs_min2 cnode_offs_max2 cnode_offs_aligned2 add.commute s0_ptrs_aligned cte_level_bits_def objBitsKO_def) apply (simp add: valid_cap'_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def projectKO_eq project_inject) apply (intro conjI) apply (simp add: objBitsKO_def s0_ptrs_aligned) apply (simp add: objBitsKO_def) apply (simp add: objBitsKO_def s0_ptrs_aligned mask_def) apply (clarsimp simp: High_cte_def High_cte'_def High_capsH_def cnode_offs_min2 cnode_offs_max2 cnode_offs_aligned2 add.commute s0_ptrs_aligned cte_level_bits_def objBitsKO_def empty_cte_def) apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct', simplified cte_level_bits_def]) apply (simp add: High_cte_def High_cte'_def High_capsH_def empty_cte_def cnode_offs_min2 cnode_offs_max2 cnode_offs_aligned2 add.commute s0_ptrs_aligned cte_level_bits_def objBitsKO_def) apply (simp add: valid_cap'_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def projectKO_eq project_inject) apply (intro conjI) apply (simp add: objBitsKO_def s0_ptrs_aligned) apply (simp add: objBitsKO_def) apply (simp add: objBitsKO_def s0_ptrs_aligned mask_def) apply (clarsimp simp: Silc_cte_def Silc_cte'_def Silc_capsH_def cnode_offs_min2 cnode_offs_max2 cnode_offs_aligned2 add.commute s0_ptrs_aligned cte_level_bits_def objBitsKO_def empty_cte_def) apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct', simplified cte_level_bits_def]) apply (simp add: Silc_cte_def Silc_cte'_def Silc_capsH_def empty_cte_def cnode_offs_min2 cnode_offs_max2 cnode_offs_aligned2 add.commute s0_ptrs_aligned cte_level_bits_def objBitsKO_def) apply (simp add: valid_cap'_def capAligned_def word_bits_def Low_asid_def asid_low_bits_def asid_bits_def s0_ptrs_aligned page_directory_at'_def pdBits_def pageBits_def) apply (clarsimp simp: typ_at'_def ko_wp_at'_def) apply (drule less_t2n_ex_ucast[where n=12 and 'b=12, simplified]) apply (clarsimp simp: Low_pdH_def pd_offs_aligned pd_offs_min pd_offs_max s0_ptrs_aligned add.commute objBitsKO_def archObjSize_def) apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct']) apply (simp add: Low_pdH_def pd_offs_aligned pd_offs_min pd_offs_max s0_ptrs_aligned objBitsKO_def archObjSize_def add.commute) apply (simp add: valid_cap'_def capAligned_def word_bits_def High_asid_def asid_low_bits_def asid_bits_def s0_ptrs_aligned page_directory_at'_def pdBits_def pageBits_def) apply (clarsimp simp: typ_at'_def ko_wp_at'_def) apply (drule less_t2n_ex_ucast[where n=12 and 'b=12, simplified]) apply (clarsimp simp: High_pdH_def pd_offs_aligned pd_offs_min pd_offs_max s0_ptrs_aligned add.commute objBitsKO_def archObjSize_def) apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct']) apply (simp add: High_pdH_def pd_offs_aligned pd_offs_min pd_offs_max s0_ptrs_aligned objBitsKO_def archObjSize_def add.commute) apply (simp add: valid_cap'_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def projectKO_eq project_inject Low_asid_def asid_low_bits_def asid_bits_def objBitsKO_def ntfnH_def) apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct', simplified]) apply (simp add: ntfnH_def objBitsKO_def) apply (simp add: valid_cap'_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def projectKO_eq project_inject Low_asid_def asid_low_bits_def asid_bits_def objBitsKO_def ntfnH_def) apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct']) apply (simp add: ntfnH_def objBitsKO_def) by (simp
        | simp add: valid_cap'_def s0H_internal_def capAligned_def word_bits_def objBits_def s0_ptrs_aligned obj_at'_def projectKO_eq project_inject Low_asid_def asid_low_bits_def asid_bits_def,
          intro conjI,
             simp add: objBitsKO_def s0_ptrs_aligned,
            simp add: objBitsKO_def,
           simp add: objBitsKO_def s0_ptrs_aligned mask_def,
          rule pspace_distinctD'[OF _ s0H_pspace_distinct', simplified s0H_internal_def],
          simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((valid_cap' capability.NullCap s0H_internal &&& valid_cap' (capability.ThreadCap Low_tcb_ptr) s0H_internal &&& valid_cap' (capability.ThreadCap High_tcb_ptr) s0H_internal) &&& valid_cap' (capability.CNodeCap Low_cnode_ptr 10 2 10) s0H_internal &&& valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal &&& valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal) &&& (valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal &&& valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal &&& valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal) &&& valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal &&& valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal &&& valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (1 subgoal):
 1. ((valid_cap' capability.NullCap s0H_internal &&& valid_cap' (capability.ThreadCap Low_tcb_ptr) s0H_internal &&& valid_cap' (capability.ThreadCap High_tcb_ptr) s0H_internal) &&& valid_cap' (capability.CNodeCap Low_cnode_ptr 10 2 10) s0H_internal &&& valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal &&& valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal) &&& (valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal &&& valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal &&& valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal) &&& valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal &&& valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal &&& valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (9 subgoals):
 1. valid_cap' (capability.CNodeCap Low_cnode_ptr 10 2 10) s0H_internal
 2. valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal
 3. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 5. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 7. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 8. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 9. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (9 subgoals):
 1. is_aligned Low_cnode_ptr (objBitsKO (KOCTE undefined) + 10) \<and> objBitsKO (KOCTE undefined) < 22 \<and> 2 && mask 10 = 2 \<and> (\<forall>addr. \<exists>ko. Low_cte Low_cnode_ptr (Low_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (Low_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (Low_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal)
 2. valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal
 3. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 5. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 7. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 8. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 9. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (12 subgoals):
 1. is_aligned Low_cnode_ptr (objBitsKO (KOCTE undefined) + 10)
 2. objBitsKO (KOCTE undefined) < 22
 3. 2 && mask 10 = 2
 4. \<forall>addr. \<exists>ko. Low_cte Low_cnode_ptr (Low_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (Low_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (Low_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 5. valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal
 6. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 7. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 8. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 9. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 10. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. objBitsKO (KOCTE undefined) < 22
 2. 2 && mask 10 = 2
 3. \<forall>addr. \<exists>ko. Low_cte Low_cnode_ptr (Low_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (Low_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (Low_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 4. valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal
 5. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 6. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 7. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 8. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 9. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 10. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. 2 && mask 10 = 2
 2. \<forall>addr. \<exists>ko. Low_cte Low_cnode_ptr (Low_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (Low_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (Low_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 3. valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal
 4. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 5. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 6. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 7. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 8. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 9. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 10. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (9 subgoals):
 1. \<forall>addr. \<exists>ko. Low_cte Low_cnode_ptr (Low_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (Low_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (Low_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 2. valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal
 3. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 5. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 7. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 8. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 9. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (9 subgoals):
 1. \<And>addr. ps_clear (Low_cnode_ptr + 0x10 * (addr && mask 10)) 4 s0H_internal
 2. valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal
 3. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 5. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 7. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 8. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 9. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (9 subgoals):
 1. \<And>addr. \<exists>v. ksPSpace s0H_internal (Low_cnode_ptr + 0x10 * (addr && mask 10)) = Some v \<and> objBitsKO v = 4
 2. valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal
 3. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 5. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 7. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 8. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 9. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (8 subgoals):
 1. valid_cap' (capability.CNodeCap High_cnode_ptr 10 2 10) s0H_internal
 2. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 7. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 8. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (8 subgoals):
 1. is_aligned High_cnode_ptr (objBitsKO (KOCTE undefined) + 10) \<and> objBitsKO (KOCTE undefined) < 22 \<and> 2 && mask 10 = 2 \<and> (\<forall>addr. \<exists>ko. High_cte High_cnode_ptr (High_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (High_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (High_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal)
 2. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 7. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 8. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (11 subgoals):
 1. is_aligned High_cnode_ptr (objBitsKO (KOCTE undefined) + 10)
 2. objBitsKO (KOCTE undefined) < 22
 3. 2 && mask 10 = 2
 4. \<forall>addr. \<exists>ko. High_cte High_cnode_ptr (High_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (High_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (High_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 5. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 6. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 7. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 8. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 9. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 10. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. objBitsKO (KOCTE undefined) < 22
 2. 2 && mask 10 = 2
 3. \<forall>addr. \<exists>ko. High_cte High_cnode_ptr (High_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (High_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (High_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 4. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 5. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 6. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 7. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 8. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 9. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 10. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (9 subgoals):
 1. 2 && mask 10 = 2
 2. \<forall>addr. \<exists>ko. High_cte High_cnode_ptr (High_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (High_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (High_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 3. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 5. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 7. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 8. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 9. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (8 subgoals):
 1. \<forall>addr. \<exists>ko. High_cte High_cnode_ptr (High_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (High_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (High_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 2. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 7. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 8. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (8 subgoals):
 1. \<And>addr. ps_clear (High_cnode_ptr + 0x10 * (addr && mask 10)) 4 s0H_internal
 2. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 7. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 8. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (8 subgoals):
 1. \<And>addr. \<exists>v. ksPSpace s0H_internal (High_cnode_ptr + 0x10 * (addr && mask 10)) = Some v \<and> objBitsKO v = 4
 2. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 7. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 8. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (7 subgoals):
 1. valid_cap' (capability.CNodeCap Silc_cnode_ptr 10 2 10) s0H_internal
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 6. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 7. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (7 subgoals):
 1. is_aligned Silc_cnode_ptr (objBitsKO (KOCTE undefined) + 10) \<and> objBitsKO (KOCTE undefined) < 22 \<and> 2 && mask 10 = 2 \<and> (\<forall>addr. \<exists>ko. Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (Silc_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (Silc_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal)
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 6. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 7. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (10 subgoals):
 1. is_aligned Silc_cnode_ptr (objBitsKO (KOCTE undefined) + 10)
 2. objBitsKO (KOCTE undefined) < 22
 3. 2 && mask 10 = 2
 4. \<forall>addr. \<exists>ko. Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (Silc_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (Silc_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 5. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 6. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 7. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 8. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 9. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 10. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (9 subgoals):
 1. objBitsKO (KOCTE undefined) < 22
 2. 2 && mask 10 = 2
 3. \<forall>addr. \<exists>ko. Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (Silc_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (Silc_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 5. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 7. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 8. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 9. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (8 subgoals):
 1. 2 && mask 10 = 2
 2. \<forall>addr. \<exists>ko. Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (Silc_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (Silc_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 4. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 6. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 7. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 8. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (7 subgoals):
 1. \<forall>addr. \<exists>ko. Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + 0x10 * (addr && mask 10)) = Some ko \<and> is_aligned (Silc_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) \<and> (\<exists>obj. KOCTE obj = ko) \<and> ps_clear (Silc_cnode_ptr + 0x10 * (addr && mask 10)) (objBitsKO ko) s0H_internal
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 6. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 7. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (7 subgoals):
 1. \<And>addr. ps_clear (Silc_cnode_ptr + 0x10 * (addr && mask 10)) 4 s0H_internal
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 6. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 7. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (7 subgoals):
 1. \<And>addr. \<exists>v. ksPSpace s0H_internal (Silc_cnode_ptr + 0x10 * (addr && mask 10)) = Some v \<and> objBitsKO v = 4
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 3. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 5. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 6. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 7. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (6 subgoals):
 1. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) s0H_internal
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 5. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 6. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (6 subgoals):
 1. \<forall>y<0x1000. pde_at' (Low_pd_ptr + (y << 2)) s0H_internal
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 5. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 6. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (6 subgoals):
 1. \<And>y. y < 0x1000 \<Longrightarrow> \<exists>ko. kh0H (Low_pd_ptr + (y << 2)) = Some ko \<and> is_aligned (Low_pd_ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (Low_pd_ptr + (y << 2)) (objBitsKO ko) s0H_internal
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 5. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 6. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (6 subgoals):
 1. \<And>y. \<exists>ya. y = UCAST(12 \<rightarrow> 32) ya \<Longrightarrow> \<exists>ko. kh0H (Low_pd_ptr + (y << 2)) = Some ko \<and> is_aligned (Low_pd_ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (Low_pd_ptr + (y << 2)) (objBitsKO ko) s0H_internal
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 5. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 6. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (6 subgoals):
 1. \<And>ya. ps_clear (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) ya << 2)) 2 s0H_internal
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 5. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 6. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (6 subgoals):
 1. \<And>ya. \<exists>v. ksPSpace s0H_internal (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) ya << 2)) = Some v \<and> objBitsKO v = 2
 2. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 4. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 5. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 6. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (5 subgoals):
 1. valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) s0H_internal
 2. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 4. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 5. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (5 subgoals):
 1. \<forall>y<0x1000. pde_at' (High_pd_ptr + (y << 2)) s0H_internal
 2. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 4. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 5. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (5 subgoals):
 1. \<And>y. y < 0x1000 \<Longrightarrow> \<exists>ko. kh0H (High_pd_ptr + (y << 2)) = Some ko \<and> is_aligned (High_pd_ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (High_pd_ptr + (y << 2)) (objBitsKO ko) s0H_internal
 2. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 4. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 5. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (5 subgoals):
 1. \<And>y. \<exists>ya. y = UCAST(12 \<rightarrow> 32) ya \<Longrightarrow> \<exists>ko. kh0H (High_pd_ptr + (y << 2)) = Some ko \<and> is_aligned (High_pd_ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (High_pd_ptr + (y << 2)) (objBitsKO ko) s0H_internal
 2. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 4. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 5. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (5 subgoals):
 1. \<And>ya. ps_clear (High_pd_ptr + (UCAST(12 \<rightarrow> 32) ya << 2)) 2 s0H_internal
 2. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 4. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 5. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (5 subgoals):
 1. \<And>ya. \<exists>v. ksPSpace s0H_internal (High_pd_ptr + (UCAST(12 \<rightarrow> 32) ya << 2)) = Some v \<and> objBitsKO v = 2
 2. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 3. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 4. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 5. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (4 subgoals):
 1. valid_cap' (capability.NotificationCap ntfn_ptr 0 True False) s0H_internal
 2. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 3. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 4. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (4 subgoals):
 1. ps_clear ntfn_ptr 4 s0H_internal
 2. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 3. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 4. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (4 subgoals):
 1. \<exists>v. kh0H ntfn_ptr = Some v \<and> objBitsKO v = 4
 2. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 3. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 4. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (3 subgoals):
 1. valid_cap' (capability.NotificationCap ntfn_ptr 0 False True) s0H_internal
 2. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 3. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (3 subgoals):
 1. ps_clear ntfn_ptr 4 s0H_internal
 2. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 3. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (3 subgoals):
 1. \<exists>v. ksPSpace s0H_internal ntfn_ptr = Some v \<and> objBitsKO v = 4
 2. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 3. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal proof (prove)
goal (2 subgoals):
 1. valid_cap' (capability.ReplyCap Low_tcb_ptr True True) s0H_internal
 2. valid_cap' (capability.ReplyCap High_tcb_ptr True True) s0H_internal