theory Invocation_DP

lemma update_thread_intent_update:
  "\<lbrace>\<lambda>s. < P > s\<rbrace>
   update_thread cur_thread (cdl_tcb_intent_update f)
   \<lbrace>\<lambda>rv s. < P > s\<rbrace>" apply (rule sep_nonimpact_valid_lift) apply (simp add:update_thread_def set_object_def get_thread_def) apply (wp  | wpc | simp add:object_at_def
     intent_reset_def set_object_def)+ apply (simp add:object_clean_def intent_reset_def
     object_slots_def asid_reset_def update_slots_def) apply fastforce apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift P\<rbrace> update_thread cur_thread (cdl_tcb_intent_update f) \<lbrace>\<lambda>rv. cdl.lift P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr P A. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> update_thread cur_thread (cdl_tcb_intent_update f) \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>
 2. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> update_thread cur_thread (cdl_tcb_intent_update f) \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr P A. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> do t <- get_object cur_thread;
case t of Tcb tcb \<Rightarrow> set_object cur_thread (Tcb (cdl_tcb_intent_update f tcb)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>
 2. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> update_thread cur_thread (cdl_tcb_intent_update f) \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr P A s. A (\<exists>object. cdl_objects s ptr = Some object \<and> P (object_clean object)) \<Longrightarrow> (\<exists>y. cdl_objects s cur_thread = Some y) \<longrightarrow> ptr = cur_thread \<longrightarrow> (\<forall>x. the (cdl_objects s cur_thread) = Tcb x \<longrightarrow> A (P (object_clean (Tcb (cdl_tcb_intent_update f x)))))
 2. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> update_thread cur_thread (cdl_tcb_intent_update f) \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr P A s. A (\<exists>object. cdl_objects s ptr = Some object \<and> P (case case object of Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := reset_cap_asid o_M (case object of Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | PageTable x \<Rightarrow> cdl_page_table_caps x | PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := reset_cap_asid o_M (case object of Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | PageTable x \<Rightarrow> cdl_page_table_caps x | PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None)\<rparr>) | AsidPool x \<Rightarrow> AsidPool (x\<lparr>cdl_asid_pool_caps := reset_cap_asid o_M (case object of Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | PageTable x \<Rightarrow> cdl_page_table_caps x | PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None)\<rparr>) | PageTable x \<Rightarrow> PageTable (x\<lparr>cdl_page_table_caps := reset_cap_asid o_M (case object of Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | PageTable x \<Rightarrow> cdl_page_table_caps x | PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None)\<rparr>) | PageDirectory x \<Rightarrow> PageDirectory (x\<lparr>cdl_page_directory_caps := reset_cap_asid o_M (case object of Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | PageTable x \<Rightarrow> cdl_page_table_caps x | PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None)\<rparr>) | IRQNode x \<Rightarrow> IRQNode (x\<lparr>cdl_irq_node_caps := reset_cap_asid o_M (case object of Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | PageTable x \<Rightarrow> cdl_page_table_caps x | PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None)\<rparr>) | _ \<Rightarrow> object of Endpoint \<Rightarrow> Endpoint | Notification \<Rightarrow> Notification | Tcb tcb \<Rightarrow> Tcb (tcb\<lparr>cdl_tcb_intent := undefined\<rparr>) | CNode x \<Rightarrow> CNode x | AsidPool x \<Rightarrow> AsidPool x | PageTable x \<Rightarrow> PageTable x | PageDirectory x \<Rightarrow> PageDirectory x | Frame x \<Rightarrow> Frame x | Untyped \<Rightarrow> Untyped | IRQNode x \<Rightarrow> IRQNode x)) \<Longrightarrow> (\<exists>y. cdl_objects s cur_thread = Some y) \<longrightarrow> ptr = cur_thread \<longrightarrow> (\<forall>x. the (cdl_objects s cur_thread) = Tcb x \<longrightarrow> A (P (Tcb (x\<lparr>cdl_tcb_caps := reset_cap_asid o_M cdl_tcb_caps x, cdl_tcb_intent := undefined\<rparr>))))
 2. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> update_thread cur_thread (cdl_tcb_intent_update f) \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> update_thread cur_thread (cdl_tcb_intent_update f) \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal:
No subgoals!