theory Example_Valid_State

lemma respects_device_trivial:
  "pspace_respects_device_region s0_internal"
  "cap_refs_respects_device_region s0_internal" apply (clarsimp simp: s0_internal_def pspace_respects_device_region_def machine_state0_def device_mem_def
                        in_device_frame_def kh0_obj_def obj_at_kh_def obj_at_def kh0_def
                 split: if_splits)[1] apply fastforce apply (clarsimp simp: cap_refs_respects_device_region_def Invariants_AI.cte_wp_at_caps_of_state
                        cap_range_respects_device_region_def machine_state0_def) apply (intro conjI impI) apply (drule s0_caps_of_state) apply fastforce apply (clarsimp simp: s0_internal_def machine_state0_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_respects_device_region s0_internal &&& cap_refs_respects_device_region s0_internal proof (prove)
goal (2 subgoals):
 1. (\<lambda>p. if \<exists>sz. ((\<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = p && ~~ mask (pageBitsForSize sz)) \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = Low_cnode_ptr \<longrightarrow> a_type (CNode 10 Low_caps) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> Low_cnode_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = High_cnode_ptr \<longrightarrow> a_type (CNode 10 High_caps) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> High_cnode_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = Silc_cnode_ptr \<longrightarrow> a_type (CNode 10 Silc_caps) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> Silc_cnode_ptr \<longrightarrow> p && ~~ mask (pageBitsForSize sz) \<noteq> ntfn_ptr \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> ntfn_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = irq_cnode_ptr \<longrightarrow> a_type (CNode 0 [[] \<mapsto> NullCap]) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> irq_cnode_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = Low_pd_ptr \<longrightarrow> a_type (ArchObj (PageDirectory Low_pd')) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> Low_pd_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = High_pd_ptr \<longrightarrow> a_type (ArchObj (PageDirectory High_pd')) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> High_pd_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = Low_pt_ptr \<longrightarrow> a_type (ArchObj (PageTable Low_pt')) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> Low_pt_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = High_pt_ptr \<longrightarrow> a_type (ArchObj (PageTable High_pt')) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> High_pt_ptr \<longrightarrow> p && ~~ mask (pageBitsForSize sz) \<noteq> Low_tcb_ptr \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> Low_tcb_ptr \<longrightarrow> p && ~~ mask (pageBitsForSize sz) \<noteq> High_tcb_ptr \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> High_tcb_ptr \<longrightarrow> p && ~~ mask (pageBitsForSize sz) \<noteq> idle_tcb_ptr \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> idle_tcb_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = init_globals_frame \<longrightarrow> a_type (ArchObj (DataPage False ARMSmallPage)) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> init_globals_frame \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = init_global_pd \<longrightarrow> a_type (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> init_global_pd \<longrightarrow> a_type (CNode 0 (empty_cnode 0)) = AArch (ADeviceData sz)))))))))))))))) \<and> ((\<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> p && ~~ mask (pageBitsForSize sz)) \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = Low_cnode_ptr \<longrightarrow> a_type (CNode 10 Low_caps) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> Low_cnode_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = High_cnode_ptr \<longrightarrow> a_type (CNode 10 High_caps) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> High_cnode_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = Silc_cnode_ptr \<longrightarrow> a_type (CNode 10 Silc_caps) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> Silc_cnode_ptr \<longrightarrow> p && ~~ mask (pageBitsForSize sz) \<noteq> ntfn_ptr \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> ntfn_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = irq_cnode_ptr \<longrightarrow> a_type (CNode 0 [[] \<mapsto> NullCap]) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> irq_cnode_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = Low_pd_ptr \<longrightarrow> a_type (ArchObj (PageDirectory Low_pd')) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> Low_pd_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = High_pd_ptr \<longrightarrow> a_type (ArchObj (PageDirectory High_pd')) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> High_pd_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = Low_pt_ptr \<longrightarrow> a_type (ArchObj (PageTable Low_pt')) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> Low_pt_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = High_pt_ptr \<longrightarrow> a_type (ArchObj (PageTable High_pt')) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> High_pt_ptr \<longrightarrow> p && ~~ mask (pageBitsForSize sz) \<noteq> Low_tcb_ptr \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> Low_tcb_ptr \<longrightarrow> p && ~~ mask (pageBitsForSize sz) \<noteq> High_tcb_ptr \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> High_tcb_ptr \<longrightarrow> p && ~~ mask (pageBitsForSize sz) \<noteq> idle_tcb_ptr \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> idle_tcb_ptr \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = init_globals_frame \<longrightarrow> a_type (ArchObj (DataPage False ARMSmallPage)) = AArch (ADeviceData sz)) \<and> (p && ~~ mask (pageBitsForSize sz) \<noteq> init_globals_frame \<longrightarrow> (p && ~~ mask (pageBitsForSize sz) = init_global_pd \<longrightarrow> a_type (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) = AArch (ADeviceData sz)) \<and> p && ~~ mask (pageBitsForSize sz) = init_global_pd)))))))))))))) then Some p else None) = (\<lambda>x. None)
 2. cap_refs_respects_device_region s0_internal proof (prove)
goal (1 subgoal):
 1. cap_refs_respects_device_region s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. (cap_is_device cap \<longrightarrow> caps_of_state s0_internal (a, b) = Some cap \<longrightarrow> cap_range cap \<subseteq> dom (device_state (machine_state s0_internal))) \<and> (\<not> cap_is_device cap \<longrightarrow> caps_of_state s0_internal (a, b) = Some cap \<longrightarrow> cap_range cap \<subseteq> - dom (device_state (machine_state s0_internal))) proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>cap_is_device cap; caps_of_state s0_internal (a, b) = Some cap\<rbrakk> \<Longrightarrow> cap_range cap \<subseteq> dom (device_state (machine_state s0_internal))
 2. \<And>a b cap. \<lbrakk>\<not> cap_is_device cap; caps_of_state s0_internal (a, b) = Some cap\<rbrakk> \<Longrightarrow> cap_range cap \<subseteq> - dom (device_state (machine_state s0_internal)) proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>cap_is_device cap; cap = NullCap \<or> ((a, b), cap) \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)}\<rbrakk> \<Longrightarrow> cap_range cap \<subseteq> dom (device_state (machine_state s0_internal))
 2. \<And>a b cap. \<lbrakk>\<not> cap_is_device cap; caps_of_state s0_internal (a, b) = Some cap\<rbrakk> \<Longrightarrow> cap_range cap \<subseteq> - dom (device_state (machine_state s0_internal)) proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>\<not> cap_is_device cap; caps_of_state s0_internal (a, b) = Some cap\<rbrakk> \<Longrightarrow> cap_range cap \<subseteq> - dom (device_state (machine_state s0_internal)) proof (prove)
goal:
No subgoals!