theory Detype_R

lemma locateCTE_ret_neq:
  "\<lbrace>ko_wp_at' (\<lambda>x. koTypeOf x \<noteq> TCBT \<and> koTypeOf x \<noteq> CTET) ptr\<rbrace>
  locateCTE src \<lbrace>\<lambda>r s. ptr \<noteq> r\<rbrace>" apply (clarsimp simp add:valid_def) apply (frule use_valid[OF _ locateCTE_case]) apply simp apply (frule(1) use_valid[OF _ locateCTE_inv]) apply (clarsimp simp:ko_wp_at'_def koTypeOf_def) apply (auto split:Structures_H.kernel_object.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>x. koTypeOf x \<noteq> TCBT \<and> koTypeOf x \<noteq> CTET) ptr\<rbrace> locateCTE src \<lbrace>\<lambda>r s. ptr \<noteq> r\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>ko_wp_at' (\<lambda>x. koTypeOf x \<noteq> TCBT \<and> koTypeOf x \<noteq> CTET) ptr s; (ptr, b) \<in> fst (locateCTE src s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>ko_wp_at' (\<lambda>x. koTypeOf x \<noteq> TCBT \<and> koTypeOf x \<noteq> CTET) ptr s; (ptr, b) \<in> fst (locateCTE src s)\<rbrakk> \<Longrightarrow> True
 2. \<And>s b. \<lbrakk>ko_wp_at' (\<lambda>x. koTypeOf x \<noteq> TCBT \<and> koTypeOf x \<noteq> CTET) ptr s; (ptr, b) \<in> fst (locateCTE src s); \<exists>obj. ksPSpace b ptr = Some obj \<and> (case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>ko_wp_at' (\<lambda>x. koTypeOf x \<noteq> TCBT \<and> koTypeOf x \<noteq> CTET) ptr s; (ptr, b) \<in> fst (locateCTE src s); \<exists>obj. ksPSpace b ptr = Some obj \<and> (case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>ko_wp_at' (\<lambda>x. koTypeOf x \<noteq> TCBT \<and> koTypeOf x \<noteq> CTET) ptr s; (ptr, b) \<in> fst (locateCTE src s); \<exists>obj. ksPSpace b ptr = Some obj \<and> (case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False); ko_wp_at' (\<lambda>x. koTypeOf x \<noteq> TCBT \<and> koTypeOf x \<noteq> CTET) ptr b\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s b ko obj. \<lbrakk>(ptr, b) \<in> fst (locateCTE src s); ksPSpace s ptr = Some ko; case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ksPSpace b ptr = Some obj; is_aligned ptr (objBitsKO ko); is_aligned ptr (objBitsKO obj); Structures_H.kernel_object.rec_kernel_object (\<lambda>e. EndpointT) (\<lambda>e. NotificationT) KernelDataT UserDataT UserDataDeviceT (\<lambda>e. TCBT) (\<lambda>e. CTET) (\<lambda>e. ArchT (archTypeOf e)) ko \<noteq> TCBT; Structures_H.kernel_object.rec_kernel_object (\<lambda>e. EndpointT) (\<lambda>e. NotificationT) KernelDataT UserDataT UserDataDeviceT (\<lambda>e. TCBT) (\<lambda>e. CTET) (\<lambda>e. ArchT (archTypeOf e)) obj \<noteq> TCBT; Structures_H.kernel_object.rec_kernel_object (\<lambda>e. EndpointT) (\<lambda>e. NotificationT) KernelDataT UserDataT UserDataDeviceT (\<lambda>e. TCBT) (\<lambda>e. CTET) (\<lambda>e. ArchT (archTypeOf e)) ko \<noteq> CTET; ps_clear ptr (objBitsKO ko) s; Structures_H.kernel_object.rec_kernel_object (\<lambda>e. EndpointT) (\<lambda>e. NotificationT) KernelDataT UserDataT UserDataDeviceT (\<lambda>e. TCBT) (\<lambda>e. CTET) (\<lambda>e. ArchT (archTypeOf e)) obj \<noteq> CTET; ps_clear ptr (objBitsKO obj) b\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!