theory Example_Valid_State

lemma valid_obj_s0[simp]:
  "valid_obj Low_cnode_ptr  Low_cnode s0_internal"
  "valid_obj High_cnode_ptr High_cnode s0_internal"
  "valid_obj Silc_cnode_ptr Silc_cnode s0_internal"
  "valid_obj ntfn_ptr        ntfn s0_internal"
  "valid_obj irq_cnode_ptr  irq_cnode s0_internal"
  "valid_obj Low_pd_ptr     Low_pd s0_internal"
  "valid_obj High_pd_ptr    High_pd s0_internal"
  "valid_obj Low_pt_ptr     Low_pt s0_internal"
  "valid_obj High_pt_ptr    High_pt s0_internal"
  "valid_obj Low_tcb_ptr    Low_tcb s0_internal"
  "valid_obj High_tcb_ptr   High_tcb s0_internal"
  "valid_obj idle_tcb_ptr   idle_tcb s0_internal"
  "valid_obj init_global_pd (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)
            (ucast (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {}))))
                                     s0_internal"
  "valid_obj init_globals_frame (ArchObj (DataPage False ARMSmallPage)) s0_internal" apply (simp_all add: valid_obj_def kh0_obj_def) apply (simp add: valid_cs_def Low_caps_ran High_caps_ran Silc_caps_ran
                               valid_cs_size_def word_bits_def cte_level_bits_def)+ apply (simp add: valid_ntfn_def obj_at_def s0_internal_def kh0_def
                            High_tcb_def is_tcb_def) apply (simp add: valid_cs_def valid_cs_size_def word_bits_def cte_level_bits_def) apply (simp add: well_formed_cnode_n_def) apply (fastforce simp: Low_pd'_def High_pd'_def Low_pt'_def High_pt'_def
                                Low_pt_ptr_def High_pt_ptr_def
                                shared_page_ptr_phys_def shared_page_ptr_virt_def
                                valid_vm_rights_def vm_kernel_only_def
                                kernel_base_def pageBits_def pt_bits_def vmsz_aligned_def
                                is_aligned_def[THEN iffD2]
                                is_aligned_addrFromPPtr_n)+ apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def
                           valid_ipc_buffer_cap_def valid_tcb_state_def valid_arch_tcb_def
           | simp add: obj_at_def s0_internal_def kh0_def kh0_obj_def is_ntfn_def
                       is_valid_vtable_root_def)+ apply (simp add: valid_vm_rights_def vm_kernel_only_def
                   kernel_base_def pageBits_def vmsz_aligned_def
                   is_aligned_def[THEN iffD2]
                   is_aligned_addrFromPPtr_n) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((valid_obj Low_cnode_ptr Low_cnode s0_internal &&& valid_obj High_cnode_ptr High_cnode s0_internal &&& valid_obj Silc_cnode_ptr Silc_cnode s0_internal) &&& (valid_obj ntfn_ptr ntfn s0_internal &&& valid_obj irq_cnode_ptr irq_cnode s0_internal) &&& valid_obj Low_pd_ptr Low_pd s0_internal &&& valid_obj High_pd_ptr High_pd s0_internal) &&& (valid_obj Low_pt_ptr Low_pt s0_internal &&& valid_obj High_pt_ptr High_pt s0_internal &&& valid_obj Low_tcb_ptr Low_tcb s0_internal) &&& (valid_obj High_tcb_ptr High_tcb s0_internal &&& valid_obj idle_tcb_ptr idle_tcb s0_internal) &&& valid_obj init_global_pd (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) s0_internal &&& valid_obj init_globals_frame (ArchObj (DataPage False ARMSmallPage)) s0_internal proof (prove)
goal (13 subgoals):
 1. valid_cs 10 Low_caps s0_internal
 2. valid_cs 10 High_caps s0_internal
 3. valid_cs 10 Silc_caps s0_internal
 4. valid_ntfn \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr> s0_internal
 5. valid_cs 0 [[] \<mapsto> NullCap] s0_internal
 6. \<forall>x. wellformed_pde (Low_pd' x)
 7. \<forall>x. wellformed_pde (High_pd' x)
 8. \<forall>x. wellformed_pte (Low_pt' x)
 9. \<forall>x. wellformed_pte (High_pt' x)
 10. valid_tcb Low_tcb_ptr \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
A total of 13 subgoals... proof (prove)
goal (10 subgoals):
 1. valid_ntfn \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr> s0_internal
 2. valid_cs 0 [[] \<mapsto> NullCap] s0_internal
 3. \<forall>x. wellformed_pde (Low_pd' x)
 4. \<forall>x. wellformed_pde (High_pd' x)
 5. \<forall>x. wellformed_pte (Low_pt' x)
 6. \<forall>x. wellformed_pte (High_pt' x)
 7. valid_tcb Low_tcb_ptr \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
 8. valid_tcb High_tcb_ptr \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
 9. valid_tcb idle_tcb_ptr \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr> s0_internal
 10. {} \<in> valid_vm_rights \<and> vmsz_aligned (addrFromPPtr kernel_base) ARMSection proof (prove)
goal (9 subgoals):
 1. valid_cs 0 [[] \<mapsto> NullCap] s0_internal
 2. \<forall>x. wellformed_pde (Low_pd' x)
 3. \<forall>x. wellformed_pde (High_pd' x)
 4. \<forall>x. wellformed_pte (Low_pt' x)
 5. \<forall>x. wellformed_pte (High_pt' x)
 6. valid_tcb Low_tcb_ptr \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
 7. valid_tcb High_tcb_ptr \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
 8. valid_tcb idle_tcb_ptr \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr> s0_internal
 9. {} \<in> valid_vm_rights \<and> vmsz_aligned (addrFromPPtr kernel_base) ARMSection proof (prove)
goal (9 subgoals):
 1. well_formed_cnode_n 0 [[] \<mapsto> NullCap]
 2. \<forall>x. wellformed_pde (Low_pd' x)
 3. \<forall>x. wellformed_pde (High_pd' x)
 4. \<forall>x. wellformed_pte (Low_pt' x)
 5. \<forall>x. wellformed_pte (High_pt' x)
 6. valid_tcb Low_tcb_ptr \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
 7. valid_tcb High_tcb_ptr \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
 8. valid_tcb idle_tcb_ptr \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr> s0_internal
 9. {} \<in> valid_vm_rights \<and> vmsz_aligned (addrFromPPtr kernel_base) ARMSection proof (prove)
goal (8 subgoals):
 1. \<forall>x. wellformed_pde (Low_pd' x)
 2. \<forall>x. wellformed_pde (High_pd' x)
 3. \<forall>x. wellformed_pte (Low_pt' x)
 4. \<forall>x. wellformed_pte (High_pt' x)
 5. valid_tcb Low_tcb_ptr \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
 6. valid_tcb High_tcb_ptr \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
 7. valid_tcb idle_tcb_ptr \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr> s0_internal
 8. {} \<in> valid_vm_rights \<and> vmsz_aligned (addrFromPPtr kernel_base) ARMSection proof (prove)
goal (4 subgoals):
 1. valid_tcb Low_tcb_ptr \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
 2. valid_tcb High_tcb_ptr \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr> s0_internal
 3. valid_tcb idle_tcb_ptr \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr> s0_internal
 4. {} \<in> valid_vm_rights \<and> vmsz_aligned (addrFromPPtr kernel_base) ARMSection proof (prove)
goal (1 subgoal):
 1. {} \<in> valid_vm_rights \<and> vmsz_aligned (addrFromPPtr kernel_base) ARMSection proof (prove)
goal:
No subgoals!