theory Example_Valid_StateH

lemma map_to_ctes_kh0H_simps'[simp]:
  "map_to_ctes kh0H (Low_cnode_ptr + 0x13E0) = Some
    (CTE (NotificationCap ntfn_ptr 0 True False) (MDB (Silc_cnode_ptr + 0x13E0) 0 False False))"
  "map_to_ctes kh0H (Low_cnode_ptr + 0x30) = Some
    (CTE (ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)))
         (MDB 0 (Low_tcb_ptr + 0x10) False False))"
  "map_to_ctes kh0H (Low_cnode_ptr + 0x20) = Some
    (CTE (CNodeCap Low_cnode_ptr 10 2 10) (MDB 0 Low_tcb_ptr False False))"
  "map_to_ctes kh0H (Low_cnode_ptr + 0x10) = Some (CTE (ThreadCap Low_tcb_ptr) Null_mdb)"
  "map_to_ctes kh0H (High_cnode_ptr + 0x13E0) = Some
    (CTE (NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False))"
  "map_to_ctes kh0H (High_cnode_ptr + 0x30) = Some
    (CTE (ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)))
         (MDB 0 (High_tcb_ptr + 0x10) False False))"
  "map_to_ctes kh0H (High_cnode_ptr + 0x20) = Some
    (CTE (CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False))"
  "map_to_ctes kh0H (High_cnode_ptr + 0x10) = Some (CTE (ThreadCap High_tcb_ptr) Null_mdb)"
  "map_to_ctes kh0H (Silc_cnode_ptr + 0x13E0) = Some
    (CTE (NotificationCap ntfn_ptr 0 True False)
         (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))"
  "map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some
    (CTE (CNodeCap Silc_cnode_ptr 10 2 10) Null_mdb)" apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 318", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 3", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 2", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) apply (clarsimp simp: map_to_ctes_kh0H_simps(3)[where x="the_nat_to_bl_10 1", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 318", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 3", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 2", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) apply (clarsimp simp: map_to_ctes_kh0H_simps(4)[where x="the_nat_to_bl_10 1", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) apply (clarsimp simp: map_to_ctes_kh0H_simps(5)[where x="the_nat_to_bl_10 318", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) apply (clarsimp simp: map_to_ctes_kh0H_simps(5)[where x="the_nat_to_bl_10 2", simplified the_nat_to_bl_simps, simplified] kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps, fastforce simp: s0_ptr_defs is_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((map_to_ctes kh0H (Low_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (Silc_cnode_ptr + 0x13E0) 0 False False)) &&& map_to_ctes kh0H (Low_cnode_ptr + 0x30) = Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB 0 (Low_tcb_ptr + 0x10) False False))) &&& map_to_ctes kh0H (Low_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB 0 Low_tcb_ptr False False)) &&& map_to_ctes kh0H (Low_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap Low_tcb_ptr) (MDB 0 0 False False)) &&& map_to_ctes kh0H (High_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False))) &&& (map_to_ctes kh0H (High_cnode_ptr + 0x30) = Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False)) &&& map_to_ctes kh0H (High_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False))) &&& map_to_ctes kh0H (High_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False)) &&& map_to_ctes kh0H (Silc_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) &&& map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) proof (prove)
goal (9 subgoals):
 1. map_to_ctes kh0H (Low_cnode_ptr + 0x30) = Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB 0 (Low_tcb_ptr + 0x10) False False))
 2. map_to_ctes kh0H (Low_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB 0 Low_tcb_ptr False False))
 3. map_to_ctes kh0H (Low_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap Low_tcb_ptr) (MDB 0 0 False False))
 4. map_to_ctes kh0H (High_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False))
 5. map_to_ctes kh0H (High_cnode_ptr + 0x30) = Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False))
 6. map_to_ctes kh0H (High_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False))
 7. map_to_ctes kh0H (High_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False))
 8. map_to_ctes kh0H (Silc_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))
 9. map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) proof (prove)
goal (8 subgoals):
 1. map_to_ctes kh0H (Low_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB 0 Low_tcb_ptr False False))
 2. map_to_ctes kh0H (Low_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap Low_tcb_ptr) (MDB 0 0 False False))
 3. map_to_ctes kh0H (High_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False))
 4. map_to_ctes kh0H (High_cnode_ptr + 0x30) = Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False))
 5. map_to_ctes kh0H (High_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False))
 6. map_to_ctes kh0H (High_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False))
 7. map_to_ctes kh0H (Silc_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))
 8. map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) proof (prove)
goal (7 subgoals):
 1. map_to_ctes kh0H (Low_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap Low_tcb_ptr) (MDB 0 0 False False))
 2. map_to_ctes kh0H (High_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False))
 3. map_to_ctes kh0H (High_cnode_ptr + 0x30) = Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False))
 4. map_to_ctes kh0H (High_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False))
 5. map_to_ctes kh0H (High_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False))
 6. map_to_ctes kh0H (Silc_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))
 7. map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) proof (prove)
goal (6 subgoals):
 1. map_to_ctes kh0H (High_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False))
 2. map_to_ctes kh0H (High_cnode_ptr + 0x30) = Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False))
 3. map_to_ctes kh0H (High_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False))
 4. map_to_ctes kh0H (High_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False))
 5. map_to_ctes kh0H (Silc_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))
 6. map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) proof (prove)
goal (5 subgoals):
 1. map_to_ctes kh0H (High_cnode_ptr + 0x30) = Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False))
 2. map_to_ctes kh0H (High_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False))
 3. map_to_ctes kh0H (High_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False))
 4. map_to_ctes kh0H (Silc_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))
 5. map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) proof (prove)
goal (4 subgoals):
 1. map_to_ctes kh0H (High_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False))
 2. map_to_ctes kh0H (High_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False))
 3. map_to_ctes kh0H (Silc_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))
 4. map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) proof (prove)
goal (3 subgoals):
 1. map_to_ctes kh0H (High_cnode_ptr + 0x10) = Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False))
 2. map_to_ctes kh0H (Silc_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))
 3. map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) proof (prove)
goal (2 subgoals):
 1. map_to_ctes kh0H (Silc_cnode_ptr + 0x13E0) = Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))
 2. map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) proof (prove)
goal (1 subgoal):
 1. map_to_ctes kh0H (Silc_cnode_ptr + 0x20) = Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) proof (prove)
goal:
No subgoals!