theory Example_Valid_State

lemma valid_pspace_s0[simp]:
  "valid_pspace s0_internal" apply (simp add: valid_pspace_def pspace_distinct_s0 pspace_aligned_s0 valid_objs_s0) apply (rule conjI) apply (clarsimp simp: if_live_then_nonz_cap_def) apply (subst(asm) s0_internal_def) apply (clarsimp simp: live_def hyp_live_def obj_at_def kh0_def kh0_obj_def s0_ptr_defs split: if_split_asm) apply (clarsimp simp: ex_nonz_cap_to_def) apply (rule_tac x="High_cnode_ptr" in exI) apply (rule_tac x="the_nat_to_bl_10 1" in exI) apply (force simp: cte_wp_at_cases s0_internal_def kh0_def kh0_obj_def s0_ptr_defs tcb_cap_cases_def High_caps_def the_nat_to_bl_def nat_to_bl_def well_formed_cnode_n_def dom_empty_cnode) apply (clarsimp simp: ex_nonz_cap_to_def) apply (rule_tac x="Low_cnode_ptr" in exI) apply (rule_tac x="the_nat_to_bl_10 1" in exI) apply (force simp: cte_wp_at_cases s0_internal_def kh0_def kh0_obj_def s0_ptr_defs tcb_cap_cases_def Low_caps_def the_nat_to_bl_def nat_to_bl_def well_formed_cnode_n_def dom_empty_cnode) apply (clarsimp simp: ex_nonz_cap_to_def) apply (rule_tac x="High_cnode_ptr" in exI) apply (rule_tac x="the_nat_to_bl_10 318" in exI) apply (force simp: cte_wp_at_cases s0_internal_def kh0_def kh0_obj_def s0_ptr_defs tcb_cap_cases_def High_caps_def the_nat_to_bl_def nat_to_bl_def well_formed_cnode_n_def dom_empty_cnode) apply (rule conjI) apply (simp add: Invariants_AI.cte_wp_at_caps_of_state zombies_final_def) apply (force dest: s0_caps_of_state simp: is_zombie_def) apply (rule conjI) apply (clarsimp simp: sym_refs_def state_refs_of_def state_hyp_refs_of_def s0_internal_def) apply (subst(asm) kh0_def) apply (clarsimp split: if_split_asm) apply (simp add: refs_of_def kh0_def s0_ptr_defs kh0_obj_def)+ apply (clarsimp simp: sym_refs_def state_hyp_refs_of_def s0_internal_def) apply (subst(asm) kh0_def) apply (clarsimp split: if_split_asm) by (simp add: refs_of_def kh0_def s0_ptr_defs kh0_obj_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pspace s0_internal proof (prove)
goal (1 subgoal):
 1. if_live_then_nonz_cap s0_internal \<and> zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. if_live_then_nonz_cap s0_internal
 2. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. \<And>ptr. obj_at live ptr s0_internal \<Longrightarrow> ex_nonz_cap_to ptr s0_internal
 2. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. \<And>ptr. obj_at live ptr \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr> \<Longrightarrow> ex_nonz_cap_to ptr s0_internal
 2. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (4 subgoals):
 1. ex_nonz_cap_to 0xE0000400 s0_internal
 2. ex_nonz_cap_to 0xE0000200 s0_internal
 3. ex_nonz_cap_to 0xE0000010 s0_internal
 4. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (4 subgoals):
 1. \<exists>a b. cte_wp_at (\<lambda>c. 0xE0000400 \<in> zobj_refs c) (a, b) s0_internal
 2. ex_nonz_cap_to 0xE0000200 s0_internal
 3. ex_nonz_cap_to 0xE0000010 s0_internal
 4. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (4 subgoals):
 1. \<exists>b. cte_wp_at (\<lambda>c. 0xE0000400 \<in> zobj_refs c) (High_cnode_ptr, b) s0_internal
 2. ex_nonz_cap_to 0xE0000200 s0_internal
 3. ex_nonz_cap_to 0xE0000010 s0_internal
 4. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (4 subgoals):
 1. cte_wp_at (\<lambda>c. 0xE0000400 \<in> zobj_refs c) (High_cnode_ptr, the_nat_to_bl 10 1) s0_internal
 2. ex_nonz_cap_to 0xE0000200 s0_internal
 3. ex_nonz_cap_to 0xE0000010 s0_internal
 4. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (3 subgoals):
 1. ex_nonz_cap_to 0xE0000200 s0_internal
 2. ex_nonz_cap_to 0xE0000010 s0_internal
 3. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (3 subgoals):
 1. \<exists>a b. cte_wp_at (\<lambda>c. 0xE0000200 \<in> zobj_refs c) (a, b) s0_internal
 2. ex_nonz_cap_to 0xE0000010 s0_internal
 3. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (3 subgoals):
 1. \<exists>b. cte_wp_at (\<lambda>c. 0xE0000200 \<in> zobj_refs c) (Low_cnode_ptr, b) s0_internal
 2. ex_nonz_cap_to 0xE0000010 s0_internal
 3. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (3 subgoals):
 1. cte_wp_at (\<lambda>c. 0xE0000200 \<in> zobj_refs c) (Low_cnode_ptr, the_nat_to_bl 10 1) s0_internal
 2. ex_nonz_cap_to 0xE0000010 s0_internal
 3. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. ex_nonz_cap_to 0xE0000010 s0_internal
 2. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. \<exists>a b. cte_wp_at (\<lambda>c. 0xE0000010 \<in> zobj_refs c) (a, b) s0_internal
 2. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. \<exists>b. cte_wp_at (\<lambda>c. 0xE0000010 \<in> zobj_refs c) (High_cnode_ptr, b) s0_internal
 2. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. cte_wp_at (\<lambda>c. 0xE0000010 \<in> zobj_refs c) (High_cnode_ptr, the_nat_to_bl 10 318) s0_internal
 2. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (1 subgoal):
 1. zombies_final s0_internal \<and> sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. zombies_final s0_internal
 2. sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. \<forall>a b. (\<exists>cap. caps_of_state s0_internal (a, b) = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cap. caps_of_state s0_internal (a, b) = Some cap \<and> is_final_cap' cap s0_internal)
 2. sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (1 subgoal):
 1. sym_refs (state_refs_of s0_internal) \<and> sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. sym_refs (state_refs_of s0_internal)
 2. sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. (a, b) \<in> (case kh0 x of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x) \<Longrightarrow> (x, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 2. sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. (a, b) \<in> (case ((\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> Low_cnode, High_cnode_ptr \<mapsto> High_cnode, Silc_cnode_ptr \<mapsto> Silc_cnode, ntfn_ptr \<mapsto> ntfn, irq_cnode_ptr \<mapsto> irq_cnode, Low_pd_ptr \<mapsto> Low_pd, High_pd_ptr \<mapsto> High_pd, Low_pt_ptr \<mapsto> Low_pt, High_pt_ptr \<mapsto> High_pt, Low_tcb_ptr \<mapsto> Low_tcb, High_tcb_ptr \<mapsto> High_tcb, idle_tcb_ptr \<mapsto> idle_tcb, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory global_pd))) x of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x) \<Longrightarrow> (x, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 2. sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (13 subgoals):
 1. \<And>a b. (a, b) \<in> refs_of idle_tcb \<Longrightarrow> (idle_tcb_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 2. \<And>a b. (a, b) \<in> refs_of High_tcb \<Longrightarrow> (High_tcb_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 3. \<And>a b. (a, b) \<in> refs_of Low_tcb \<Longrightarrow> (Low_tcb_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 4. \<And>a b. (a, b) \<in> refs_of High_pt \<Longrightarrow> (High_pt_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 5. \<And>a b. (a, b) \<in> refs_of Low_pt \<Longrightarrow> (Low_pt_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 6. \<And>a b. (a, b) \<in> refs_of High_pd \<Longrightarrow> (High_pd_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 7. \<And>a b. (a, b) \<in> refs_of Low_pd \<Longrightarrow> (Low_pd_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 8. \<And>a b. (a, b) \<in> refs_of irq_cnode \<Longrightarrow> (irq_cnode_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 9. \<And>a b. (a, b) \<in> refs_of ntfn \<Longrightarrow> (ntfn_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
 10. \<And>a b. (a, b) \<in> refs_of Silc_cnode \<Longrightarrow> (Silc_cnode_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. sym_refs (state_hyp_refs_of s0_internal) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> (case kh0 x of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x) \<Longrightarrow> (x, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> (case ((\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> Low_cnode, High_cnode_ptr \<mapsto> High_cnode, Silc_cnode_ptr \<mapsto> Silc_cnode, ntfn_ptr \<mapsto> ntfn, irq_cnode_ptr \<mapsto> irq_cnode, Low_pd_ptr \<mapsto> Low_pd, High_pd_ptr \<mapsto> High_pd, Low_pt_ptr \<mapsto> Low_pt, High_pt_ptr \<mapsto> High_pt, Low_tcb_ptr \<mapsto> Low_tcb, High_tcb_ptr \<mapsto> High_tcb, idle_tcb_ptr \<mapsto> idle_tcb, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory global_pd))) x of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x) \<Longrightarrow> (x, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x) proof (prove)
goal (12 subgoals):
 1. \<And>a b. (a, b) \<in> hyp_refs_of idle_tcb \<Longrightarrow> (idle_tcb_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x)
 2. \<And>a b. (a, b) \<in> hyp_refs_of High_tcb \<Longrightarrow> (High_tcb_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x)
 3. \<And>a b. (a, b) \<in> hyp_refs_of Low_tcb \<Longrightarrow> (Low_tcb_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x)
 4. \<And>a b. (a, b) \<in> hyp_refs_of High_pt \<Longrightarrow> (High_pt_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x)
 5. \<And>a b. (a, b) \<in> hyp_refs_of Low_pt \<Longrightarrow> (Low_pt_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x)
 6. \<And>a b. (a, b) \<in> hyp_refs_of High_pd \<Longrightarrow> (High_pd_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x)
 7. \<And>a b. (a, b) \<in> hyp_refs_of Low_pd \<Longrightarrow> (Low_pd_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x)
 8. \<And>a b. (a, b) \<in> hyp_refs_of irq_cnode \<Longrightarrow> (irq_cnode_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x)
 9. \<And>a b. (a, b) \<in> hyp_refs_of ntfn \<Longrightarrow> (ntfn_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x)
 10. \<And>a b. (a, b) \<in> hyp_refs_of Silc_cnode \<Longrightarrow> (Silc_cnode_ptr, symreftype b) \<in> (case kh0 a of None \<Rightarrow> {} | Some x \<Rightarrow> hyp_refs_of x)
A total of 12 subgoals...