theory Example_Valid_StateH

lemma kh0H_dom:
  "dom kh0H = {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr,
              irq_cnode_ptr, ntfn_ptr} \<union>
             irq_node_offs_range \<union>
             cnode_offs_range Silc_cnode_ptr \<union>
             cnode_offs_range High_cnode_ptr \<union>
             cnode_offs_range Low_cnode_ptr \<union>
             pd_offs_range init_global_pd \<union>
             pd_offs_range High_pd_ptr \<union>
             pd_offs_range Low_pd_ptr \<union>
             pt_offs_range High_pt_ptr \<union>
             pt_offs_range Low_pt_ptr" apply (rule equalityI) apply (simp add: kh0H_def dom_def) apply (clarsimp simp: offs_in_range option_update_range_def not_in_range_None split: if_split_asm) apply (clarsimp simp: dom_def) apply (rule conjI, clarsimp simp: kh0H_def option_update_range_def kh0H_dom_distinct not_in_range_None split: option.splits)+ apply (force dest: irq_node_offs_range_correct) by (rule conjI |
         clarsimp simp: kh0H_def option_update_range_def kh0H_dom_distinct not_in_range_None split: option.splits,
         frule offs_range_correct,
         clarsimp simp: kh0H_all_obj_def cnode_offs_range_def pd_offs_range_def pt_offs_range_def split: if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom kh0H = {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr proof (prove)
goal (2 subgoals):
 1. dom kh0H \<subseteq> {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr
 2. {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr \<subseteq> dom kh0H proof (prove)
goal (2 subgoals):
 1. {a. \<exists>y. option_update_range (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) else None) (option_update_range (Low_cte Low_cnode_ptr) (option_update_range (High_cte High_cnode_ptr) (option_update_range (Silc_cte Silc_cnode_ptr) (option_update_range [ntfn_ptr \<mapsto> KONotification ntfnH] (option_update_range [irq_cnode_ptr \<mapsto> KOCTE irq_cte] (option_update_range (Low_pdH Low_pd_ptr) (option_update_range (High_pdH High_pd_ptr) (option_update_range (Low_ptH Low_pt_ptr) (option_update_range (High_ptH High_pt_ptr) (option_update_range [Low_tcb_ptr \<mapsto> KOTCB Low_tcbH] (option_update_range [High_tcb_ptr \<mapsto> KOTCB High_tcbH] (option_update_range [idle_tcb_ptr \<mapsto> KOTCB idle_tcbH] (option_update_range (global_pdH' init_global_pd) (option_update_range [init_globals_frame \<mapsto> KOUserData] (\<lambda>x. None))))))))))))))) a = Some y} \<subseteq> insert init_globals_frame (insert idle_tcb_ptr (insert High_tcb_ptr (insert Low_tcb_ptr (insert irq_cnode_ptr (insert ntfn_ptr (irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr))))))
 2. {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr \<subseteq> dom kh0H proof (prove)
goal (1 subgoal):
 1. {init_globals_frame, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, irq_cnode_ptr, ntfn_ptr} \<union> irq_node_offs_range \<union> cnode_offs_range Silc_cnode_ptr \<union> cnode_offs_range High_cnode_ptr \<union> cnode_offs_range Low_cnode_ptr \<union> pd_offs_range init_global_pd \<union> pd_offs_range High_pd_ptr \<union> pd_offs_range Low_pd_ptr \<union> pt_offs_range High_pt_ptr \<union> pt_offs_range Low_pt_ptr \<subseteq> dom kh0H proof (prove)
goal (1 subgoal):
 1. irq_node_offs_range \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> cnode_offs_range Silc_cnode_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pd_offs_range init_global_pd \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pd_offs_range High_pd_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pd_offs_range Low_pd_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pt_offs_range High_pt_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pt_offs_range Low_pt_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> irq_node_offs_range; global_pdH' init_global_pd x = None; High_ptH High_pt_ptr x = None; Low_ptH Low_pt_ptr x = None; High_pdH High_pd_ptr x = None; Low_pdH Low_pd_ptr x = None; Silc_cte Silc_cnode_ptr x = None; High_cte High_cnode_ptr x = None; Low_cte Low_cnode_ptr x = None; x \<noteq> init_globals_frame; x \<noteq> idle_tcb_ptr; x \<noteq> High_tcb_ptr; x \<noteq> Low_tcb_ptr; x \<noteq> irq_cnode_ptr; x \<noteq> ntfn_ptr\<rbrakk> \<Longrightarrow> \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x
 2. cnode_offs_range Silc_cnode_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pd_offs_range init_global_pd \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pd_offs_range High_pd_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pd_offs_range Low_pd_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pt_offs_range High_pt_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pt_offs_range Low_pt_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} proof (prove)
goal (1 subgoal):
 1. cnode_offs_range Silc_cnode_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> cnode_offs_range High_cnode_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> cnode_offs_range Low_cnode_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pd_offs_range init_global_pd \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pd_offs_range High_pd_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pd_offs_range Low_pd_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pt_offs_range High_pt_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y} \<and> pt_offs_range Low_pt_ptr \<subseteq> {a. \<exists>y. kh0H a = Some y}