theory Example_Valid_State

lemma valid_objs_s0:
  "valid_objs s0_internal" apply (clarsimp simp: valid_objs_def) apply (subst(asm) s0_internal_def kh0_def)+ apply (simp split: if_split_asm) apply force+ apply (clarsimp simp: valid_obj_def valid_cs_def empty_cnode_def valid_cs_size_def ran_def
                        cte_level_bits_def word_bits_def well_formed_cnode_n_def dom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_objs s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>ptr y. kheap s0_internal ptr = Some y \<Longrightarrow> valid_obj ptr y s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>ptr y. kheap \<lparr>kheap = (\<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)), 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> ptr = Some y \<Longrightarrow> valid_obj ptr y s0_internal proof (prove)
goal (3 subgoals):
 1. \<And>ptr y. \<lbrakk>ptr = init_global_pd; ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {}))) = y\<rbrakk> \<Longrightarrow> valid_obj init_global_pd y s0_internal
 2. \<And>ptr y. \<lbrakk>ptr = init_globals_frame; ArchObj (DataPage False ARMSmallPage) = y\<rbrakk> \<Longrightarrow> valid_obj init_globals_frame y s0_internal
 3. \<And>ptr y irq. \<lbrakk>ptr \<noteq> init_global_pd; ptr \<noteq> init_globals_frame; ptr \<noteq> idle_tcb_ptr; ptr \<noteq> High_tcb_ptr; ptr \<noteq> Low_tcb_ptr; ptr \<noteq> High_pt_ptr; ptr \<noteq> Low_pt_ptr; ptr \<noteq> High_pd_ptr; ptr \<noteq> Low_pd_ptr; ptr \<noteq> irq_cnode_ptr; ptr \<noteq> ntfn_ptr; ptr \<noteq> Silc_cnode_ptr; ptr \<noteq> High_cnode_ptr; ptr \<noteq> Low_cnode_ptr; init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = ptr; CNode 0 (empty_cnode 0) = y\<rbrakk> \<Longrightarrow> valid_obj ptr y s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>ptr y irq. \<lbrakk>ptr \<noteq> init_global_pd; ptr \<noteq> init_globals_frame; ptr \<noteq> idle_tcb_ptr; ptr \<noteq> High_tcb_ptr; ptr \<noteq> Low_tcb_ptr; ptr \<noteq> High_pt_ptr; ptr \<noteq> Low_pt_ptr; ptr \<noteq> High_pd_ptr; ptr \<noteq> Low_pd_ptr; ptr \<noteq> irq_cnode_ptr; ptr \<noteq> ntfn_ptr; ptr \<noteq> Silc_cnode_ptr; ptr \<noteq> High_cnode_ptr; ptr \<noteq> Low_cnode_ptr; init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = ptr; CNode 0 (empty_cnode 0) = y\<rbrakk> \<Longrightarrow> valid_obj ptr y s0_internal proof (prove)
goal:
No subgoals!