theory Example_Valid_StateH

lemma mdb_next_s0H:
  "p' \<noteq> 0 \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> p' =
     (p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or>
     p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or>
     p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or>
     p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or>
     p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or>
     p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30)" apply (rule iffI) apply (simp add: next_unfold') apply (elim exE conjE) apply (frule map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all)[1] apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def ucast_shiftr_13E s0_ptrs_aligned split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def ucast_shiftr_13E s0_ptrs_aligned split: if_split_asm) apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def ucast_shiftr_13E s0_ptrs_aligned split: if_split_asm) apply (clarsimp simp: next_unfold' map_to_ctes_kh0H_dom) apply (elim disjE, simp_all add: kh0H_all_obj_def') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p' \<noteq> 0 \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> p' = (p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' \<noteq> 0; \<exists>cte. map_to_ctes kh0H p = Some cte \<and> mdbNext (cteMDBNode cte) = p'\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H p = Some cte; mdbNext (cteMDBNode cte) = p'\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H p = Some cte; mdbNext (cteMDBNode cte) = p'; p = idle_tcb_ptr \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p = idle_tcb_ptr + 0x10 \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p = idle_tcb_ptr + 0x20 \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p = idle_tcb_ptr + 0x30 \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p = idle_tcb_ptr + 0x40 \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p = Low_tcb_ptr \<and> cte = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> p = Low_tcb_ptr + 0x10 \<and> cte = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> p = Low_tcb_ptr + 0x20 \<and> cte = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> p = Low_tcb_ptr + 0x30 \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p = Low_tcb_ptr + 0x40 \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p = High_tcb_ptr \<and> cte = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> p = High_tcb_ptr + 0x10 \<and> cte = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> p = High_tcb_ptr + 0x20 \<and> cte = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> p = High_tcb_ptr + 0x30 \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p = High_tcb_ptr + 0x40 \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p = irq_cnode_ptr \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p \<in> irq_node_offs_range \<and> cte = CTE capability.NullCap (MDB 0 0 False False) \<or> p \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr p \<noteq> None \<and> cte = the (Silc_cte_cte Silc_cnode_ptr p) \<or> p \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr p \<noteq> None \<and> cte = the (High_cte_cte High_cnode_ptr p) \<or> p \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr p \<noteq> None \<and> cte = the (Low_cte_cte Low_cnode_ptr p)\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> p' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H p = Silc_cte_cte Silc_cnode_ptr p; mdbNext (cteMDBNode (the (Silc_cte_cte Silc_cnode_ptr p))) = p'; p \<in> cnode_offs_range Silc_cnode_ptr \<and> (\<exists>y. Silc_cte_cte Silc_cnode_ptr p = Some y)\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H p = High_cte_cte High_cnode_ptr p; mdbNext (cteMDBNode (the (High_cte_cte High_cnode_ptr p))) = p'; p \<in> cnode_offs_range High_cnode_ptr \<and> (\<exists>y. High_cte_cte High_cnode_ptr p = Some y)\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 3. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H p = Low_cte_cte Low_cnode_ptr p; mdbNext (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p))) = p'; p \<in> cnode_offs_range Low_cnode_ptr \<and> (\<exists>y. Low_cte_cte Low_cnode_ptr p = Some y)\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 4. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H p = High_cte_cte High_cnode_ptr p; mdbNext (cteMDBNode (the (High_cte_cte High_cnode_ptr p))) = p'; p \<in> cnode_offs_range High_cnode_ptr \<and> (\<exists>y. High_cte_cte High_cnode_ptr p = Some y)\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H p = Low_cte_cte Low_cnode_ptr p; mdbNext (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p))) = p'; p \<in> cnode_offs_range Low_cnode_ptr \<and> (\<exists>y. Low_cte_cte Low_cnode_ptr p = Some y)\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 3. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H p = Low_cte_cte Low_cnode_ptr p; mdbNext (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p))) = p'; p \<in> cnode_offs_range Low_cnode_ptr \<and> (\<exists>y. Low_cte_cte Low_cnode_ptr p = Some y)\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> \<exists>cte. map_to_ctes kh0H p = Some cte \<and> mdbNext (cteMDBNode cte) = p' proof (prove)
goal:
No subgoals!