theory Detype_AI

lemma valid_obj: "\<And>p obj. \<lbrakk> valid_obj p obj s; ko_at obj p s \<rbrakk>
                             \<Longrightarrow> valid_obj p obj (detype (untyped_range cap) s)" apply (clarsimp simp: valid_obj_def
                   split: Structures_A.kernel_object.split_asm) apply (clarsimp simp: valid_cs_def) apply (drule well_formed_cnode_valid_cs_size) apply (rule valid_cap) apply fastforce apply (rule valid_cap2) apply (erule ranE) apply (fastforce simp: obj_at_def intro!: cte_wp_at_cteI) apply (frule refs_of) apply (clarsimp simp: valid_tcb_def obj_at_def tcb_arch_detype) apply (rule conjI) apply (erule ballEI) apply (clarsimp elim!: ranE) apply (erule valid_cap [OF _ valid_cap2]) apply (fastforce intro!: cte_wp_at_tcbI) apply (clarsimp simp: valid_tcb_state_def valid_bound_ntfn_def
                      split: Structures_A.thread_state.split_asm option.splits) apply (frule refs_of) apply (rename_tac endpoint) apply (case_tac endpoint, (fastforce simp: valid_ep_def)+) apply (frule refs_of) apply (rename_tac notification ntfn_ext) apply (case_tac "ntfn_obj ntfn_ext") apply (auto simp: valid_ntfn_def ntfn_bound_refs_def split: option.splits) apply (auto intro: arch_valid_obj) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p obj. \<lbrakk>valid_obj p obj s; ko_at obj p s\<rbrakk> \<Longrightarrow> valid_obj p obj (detype (untyped_range cap) s) proof (prove)
goal (5 subgoals):
 1. \<And>p x11 x12. \<lbrakk>ko_at (CNode x11 x12) p s; valid_cs x11 x12 s\<rbrakk> \<Longrightarrow> valid_cs x11 x12 (detype (untyped_range cap) s)
 2. \<And>p x2. \<lbrakk>ko_at (TCB x2) p s; valid_tcb p x2 s\<rbrakk> \<Longrightarrow> valid_tcb p x2 (detype (untyped_range cap) s)
 3. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 4. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 5. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (5 subgoals):
 1. \<And>p x11 x12 capa. \<lbrakk>ko_at (CNode x11 x12) p s; capa \<in> ran x12; \<forall>cap\<in>ran x12. s \<turnstile> cap; valid_cs_size x11 x12\<rbrakk> \<Longrightarrow> detype (untyped_range cap) s \<turnstile> capa
 2. \<And>p x2. \<lbrakk>ko_at (TCB x2) p s; valid_tcb p x2 s\<rbrakk> \<Longrightarrow> valid_tcb p x2 (detype (untyped_range cap) s)
 3. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 4. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 5. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (5 subgoals):
 1. \<And>p x11 x12 capa. \<lbrakk>ko_at (CNode x11 x12) p s; capa \<in> ran x12; \<forall>cap\<in>ran x12. s \<turnstile> cap; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> detype (untyped_range cap) s \<turnstile> capa
 2. \<And>p x2. \<lbrakk>ko_at (TCB x2) p s; valid_tcb p x2 s\<rbrakk> \<Longrightarrow> valid_tcb p x2 (detype (untyped_range cap) s)
 3. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 4. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 5. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (6 subgoals):
 1. \<And>p x11 x12 cap. \<lbrakk>ko_at (CNode x11 x12) p s; cap \<in> ran x12; \<forall>cap\<in>ran x12. s \<turnstile> cap; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 2. \<And>p x11 x12 capa. \<lbrakk>ko_at (CNode x11 x12) p s; capa \<in> ran x12; \<forall>cap\<in>ran x12. s \<turnstile> cap; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> obj_reply_refs capa \<subseteq> UNIV - untyped_range cap
 3. \<And>p x2. \<lbrakk>ko_at (TCB x2) p s; valid_tcb p x2 s\<rbrakk> \<Longrightarrow> valid_tcb p x2 (detype (untyped_range cap) s)
 4. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 5. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 6. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (5 subgoals):
 1. \<And>p x11 x12 capa. \<lbrakk>ko_at (CNode x11 x12) p s; capa \<in> ran x12; \<forall>cap\<in>ran x12. s \<turnstile> cap; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> obj_reply_refs capa \<subseteq> UNIV - untyped_range cap
 2. \<And>p x2. \<lbrakk>ko_at (TCB x2) p s; valid_tcb p x2 s\<rbrakk> \<Longrightarrow> valid_tcb p x2 (detype (untyped_range cap) s)
 3. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 4. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 5. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (5 subgoals):
 1. \<And>p x11 x12 cap. \<lbrakk>ko_at (CNode x11 x12) p s; cap \<in> ran x12; \<forall>cap\<in>ran x12. s \<turnstile> cap; well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> \<exists>p. cte_wp_at ((=) cap) p s
 2. \<And>p x2. \<lbrakk>ko_at (TCB x2) p s; valid_tcb p x2 s\<rbrakk> \<Longrightarrow> valid_tcb p x2 (detype (untyped_range cap) s)
 3. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 4. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 5. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (5 subgoals):
 1. \<And>p x11 x12 cap x. \<lbrakk>ko_at (CNode x11 x12) p s; \<forall>cap\<in>ran x12. s \<turnstile> cap; well_formed_cnode_n x11 x12; x12 x = Some cap\<rbrakk> \<Longrightarrow> \<exists>p. cte_wp_at ((=) cap) p s
 2. \<And>p x2. \<lbrakk>ko_at (TCB x2) p s; valid_tcb p x2 s\<rbrakk> \<Longrightarrow> valid_tcb p x2 (detype (untyped_range cap) s)
 3. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 4. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 5. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (4 subgoals):
 1. \<And>p x2. \<lbrakk>ko_at (TCB x2) p s; valid_tcb p x2 s\<rbrakk> \<Longrightarrow> valid_tcb p x2 (detype (untyped_range cap) s)
 2. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 3. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 4. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (4 subgoals):
 1. \<And>p x2. \<lbrakk>ko_at (TCB x2) p s; valid_tcb p x2 s; refs_of (TCB x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV\<rbrakk> \<Longrightarrow> valid_tcb p x2 (detype (untyped_range cap) s)
 2. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 3. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 4. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (4 subgoals):
 1. \<And>p x2. \<lbrakk>kheap s p = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2)); tcb_st_refs_of (tcb_state x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; tcb_bound_refs (tcb_bound_notification x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> detype (untyped_range cap) s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2))) \<and> valid_tcb_state (tcb_state x2) (detype (untyped_range cap) s) \<and> valid_bound_ntfn (tcb_bound_notification x2) (detype (untyped_range cap) s)
 2. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 3. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 4. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (5 subgoals):
 1. \<And>p x2. \<lbrakk>kheap s p = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2)); tcb_st_refs_of (tcb_state x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; tcb_bound_refs (tcb_bound_notification x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> detype (untyped_range cap) s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2))
 2. \<And>p x2. \<lbrakk>kheap s p = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2)); tcb_st_refs_of (tcb_state x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; tcb_bound_refs (tcb_bound_notification x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) (detype (untyped_range cap) s) \<and> valid_bound_ntfn (tcb_bound_notification x2) (detype (untyped_range cap) s)
 3. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 4. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 5. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (5 subgoals):
 1. \<And>p x2 x. \<lbrakk>kheap s p = Some (TCB x2); tcb_st_refs_of (tcb_state x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; tcb_bound_refs (tcb_bound_notification x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s; x \<in> ran tcb_cap_cases; case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2))\<rbrakk> \<Longrightarrow> case x of (getF, ab) \<Rightarrow> detype (untyped_range cap) s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2))
 2. \<And>p x2. \<lbrakk>kheap s p = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2)); tcb_st_refs_of (tcb_state x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; tcb_bound_refs (tcb_bound_notification x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) (detype (untyped_range cap) s) \<and> valid_bound_ntfn (tcb_bound_notification x2) (detype (untyped_range cap) s)
 3. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 4. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 5. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (5 subgoals):
 1. \<And>p x2 a aa b x. \<lbrakk>kheap s p = Some (TCB x2); tcb_st_refs_of (tcb_state x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; tcb_bound_refs (tcb_bound_notification x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s; tcb_cap_cases x = Some (a, aa, b); s \<turnstile> a x2; b p (tcb_state x2) (a x2)\<rbrakk> \<Longrightarrow> detype (untyped_range cap) s \<turnstile> a x2
 2. \<And>p x2. \<lbrakk>kheap s p = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2)); tcb_st_refs_of (tcb_state x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; tcb_bound_refs (tcb_bound_notification x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) (detype (untyped_range cap) s) \<and> valid_bound_ntfn (tcb_bound_notification x2) (detype (untyped_range cap) s)
 3. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 4. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 5. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (5 subgoals):
 1. \<And>p x2 a aa b x. \<lbrakk>kheap s p = Some (TCB x2); tcb_st_refs_of (tcb_state x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; tcb_bound_refs (tcb_bound_notification x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s; tcb_cap_cases x = Some (a, aa, b); b p (tcb_state x2) (a x2)\<rbrakk> \<Longrightarrow> \<exists>p. cte_wp_at ((=) (a x2)) p s
 2. \<And>p x2. \<lbrakk>kheap s p = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2)); tcb_st_refs_of (tcb_state x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; tcb_bound_refs (tcb_bound_notification x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) (detype (untyped_range cap) s) \<and> valid_bound_ntfn (tcb_bound_notification x2) (detype (untyped_range cap) s)
 3. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 4. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 5. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (4 subgoals):
 1. \<And>p x2. \<lbrakk>kheap s p = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p (tcb_state x2) (getF x2)); tcb_st_refs_of (tcb_state x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; tcb_bound_refs (tcb_bound_notification x2) \<subseteq> UNIV - untyped_range cap \<times> UNIV; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) (detype (untyped_range cap) s) \<and> valid_bound_ntfn (tcb_bound_notification x2) (detype (untyped_range cap) s)
 2. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 3. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 4. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (3 subgoals):
 1. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 2. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 3. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (3 subgoals):
 1. \<And>p x3. \<lbrakk>ko_at (Endpoint x3) p s; valid_ep x3 s; refs_of (Endpoint x3) \<subseteq> UNIV - untyped_range cap \<times> UNIV\<rbrakk> \<Longrightarrow> valid_ep x3 (detype (untyped_range cap) s)
 2. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 3. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (3 subgoals):
 1. \<And>p endpoint. \<lbrakk>ko_at (Endpoint endpoint) p s; valid_ep endpoint s; refs_of (Endpoint endpoint) \<subseteq> UNIV - untyped_range cap \<times> UNIV\<rbrakk> \<Longrightarrow> valid_ep endpoint (detype (untyped_range cap) s)
 2. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 3. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (2 subgoals):
 1. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 2. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (2 subgoals):
 1. \<And>p x4. \<lbrakk>ko_at (Notification x4) p s; valid_ntfn x4 s; refs_of (Notification x4) \<subseteq> UNIV - untyped_range cap \<times> UNIV\<rbrakk> \<Longrightarrow> valid_ntfn x4 (detype (untyped_range cap) s)
 2. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (2 subgoals):
 1. \<And>notification ntfn_ext. \<lbrakk>ko_at (Notification ntfn_ext) notification s; valid_ntfn ntfn_ext s; refs_of (Notification ntfn_ext) \<subseteq> UNIV - untyped_range cap \<times> UNIV\<rbrakk> \<Longrightarrow> valid_ntfn ntfn_ext (detype (untyped_range cap) s)
 2. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (4 subgoals):
 1. \<And>notification ntfn_ext. \<lbrakk>ko_at (Notification ntfn_ext) notification s; valid_ntfn ntfn_ext s; refs_of (Notification ntfn_ext) \<subseteq> UNIV - untyped_range cap \<times> UNIV; ntfn_obj ntfn_ext = IdleNtfn\<rbrakk> \<Longrightarrow> valid_ntfn ntfn_ext (detype (untyped_range cap) s)
 2. \<And>notification ntfn_ext x2. \<lbrakk>ko_at (Notification ntfn_ext) notification s; valid_ntfn ntfn_ext s; refs_of (Notification ntfn_ext) \<subseteq> UNIV - untyped_range cap \<times> UNIV; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> valid_ntfn ntfn_ext (detype (untyped_range cap) s)
 3. \<And>notification ntfn_ext x3. \<lbrakk>ko_at (Notification ntfn_ext) notification s; valid_ntfn ntfn_ext s; refs_of (Notification ntfn_ext) \<subseteq> UNIV - untyped_range cap \<times> UNIV; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> valid_ntfn ntfn_ext (detype (untyped_range cap) s)
 4. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>p x5. \<lbrakk>ako_at x5 p s; arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (detype (untyped_range cap) s) proof (prove)
goal:
No subgoals!