theory Frame_SD

lemma set_cdl_tcb_field_wp:
  assumes fields_cong:
  "\<And>tcb tcb'. object_clean (object_wipe_slots (Tcb tcb)) = object_clean (object_wipe_slots (Tcb tcb'))
  \<Longrightarrow> object_clean (object_wipe_slots (Tcb (f tcb))) = object_clean (object_wipe_slots (Tcb (f tcb')))"
  assumes slots_simp:
  "\<And>tcb. object_slots (Tcb (f tcb)) = object_slots (Tcb tcb)"
  shows
  "\<lbrace>\<lambda>s. <obj_id \<mapsto>f Tcb tcb \<and>* R> s\<rbrace>
    update_thread obj_id f
   \<lbrace>\<lambda>rv s. <obj_id \<mapsto>f Tcb (f tcb) \<and>* R> s\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: update_thread_def get_thread_def) apply (frule sep_map_f_tcb_at) apply simp apply (clarsimp simp:object_at_def) apply (wp|wpc|simp)+ apply (rename_tac cdl_tcb) apply (rule_tac P =
                 "object_clean (object_wipe_slots (Tcb cdl_tcb)) = object_clean (object_wipe_slots (Tcb tcb))"
                 in hoare_gen_asm) apply (rule_tac obj_p = "Tcb tcb" in set_object_cdl_field_wp[OF slots_simp  ]) apply (simp add:object_type_simps object_wipe_slots_object_clean)+ apply (drule_tac tcb = cdl_tcb in fields_cong) apply simp apply wp+ apply (clarsimp simp: object_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R)\<rbrace> update_thread obj_id f \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> update_thread obj_id f \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> do t <- get_object obj_id;
case t of Tcb tcb \<Rightarrow> set_object obj_id (Tcb (f tcb)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> is_tcb (Tcb tcb)
 2. \<And>s. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; tcb_at' (\<lambda>tcba. object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb))) obj_id s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do t <- get_object obj_id;
case t of Tcb tcb \<Rightarrow> set_object obj_id (Tcb (f tcb)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; tcb_at' (\<lambda>tcba. object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb))) obj_id s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do t <- get_object obj_id;
case t of Tcb tcb \<Rightarrow> set_object obj_id (Tcb (f tcb)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s tcba. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_object obj_id >>= case_cdl_object fail fail (\<lambda>tcb. set_object obj_id (Tcb (f tcb))) (\<lambda>cdl_cnode_ext. fail) (\<lambda>cdl_asid_pool_ext. fail) (\<lambda>cdl_page_table_ext. fail) (\<lambda>cdl_page_directory_ext. fail) (\<lambda>cdl_frame_ext. fail) fail (\<lambda>cdl_irq_node_ext. fail) \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>s tcba x x3. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Tcb x3\<rbrakk> \<Longrightarrow> \<lbrace>?R44 s tcba (Tcb x3) x3\<rbrace> set_object obj_id (Tcb (f x3)) \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 2. \<And>s tcba x x4. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = CNode x4\<rbrakk> \<Longrightarrow> \<lbrace>?R45 s tcba x x4\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 3. \<And>s tcba x x5. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = AsidPool x5\<rbrakk> \<Longrightarrow> \<lbrace>?R46 s tcba x x5\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 4. \<And>s tcba x x6. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageTable x6\<rbrakk> \<Longrightarrow> \<lbrace>?R47 s tcba x x6\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 5. \<And>s tcba x x7. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageDirectory x7\<rbrakk> \<Longrightarrow> \<lbrace>?R48 s tcba x x7\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 6. \<And>s tcba x x8. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Frame x8\<rbrakk> \<Longrightarrow> \<lbrace>?R49 s tcba x x8\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 7. \<And>s tcba x. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R50 s tcba x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 8. \<And>s tcba x x10. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = IRQNode x10\<rbrakk> \<Longrightarrow> \<lbrace>?R51 s tcba x x10\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 9. \<And>s tcba. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s tcba\<rbrace> get_object obj_id \<lbrace>\<lambda>x sa. (x = Endpoint \<longrightarrow> True) \<and> (x = Notification \<longrightarrow> True) \<and> (\<forall>xa. x = Tcb xa \<longrightarrow> ?R44 s tcba x xa sa) \<and> (\<forall>xa. x = CNode xa \<longrightarrow> ?R45 s tcba x xa sa) \<and> (\<forall>xa. x = AsidPool xa \<longrightarrow> ?R46 s tcba x xa sa) \<and> (\<forall>xa. x = PageTable xa \<longrightarrow> ?R47 s tcba x xa sa) \<and> (\<forall>xa. x = PageDirectory xa \<longrightarrow> ?R48 s tcba x xa sa) \<and> (\<forall>xa. x = Frame xa \<longrightarrow> ?R49 s tcba x xa sa) \<and> (x = Untyped \<longrightarrow> ?R50 s tcba x sa) \<and> (\<forall>xa. x = IRQNode xa \<longrightarrow> ?R51 s tcba x xa sa)\<rbrace>
 10. \<And>s tcba sa. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); s = sa\<rbrakk> \<Longrightarrow> ?Q10 s tcba sa proof (prove)
goal (10 subgoals):
 1. \<And>s tcba x cdl_tcb. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Tcb cdl_tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R44 s tcba (Tcb cdl_tcb) cdl_tcb\<rbrace> set_object obj_id (Tcb (f cdl_tcb)) \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 2. \<And>s tcba x x4. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = CNode x4\<rbrakk> \<Longrightarrow> \<lbrace>?R45 s tcba x x4\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 3. \<And>s tcba x x5. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = AsidPool x5\<rbrakk> \<Longrightarrow> \<lbrace>?R46 s tcba x x5\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 4. \<And>s tcba x x6. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageTable x6\<rbrakk> \<Longrightarrow> \<lbrace>?R47 s tcba x x6\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 5. \<And>s tcba x x7. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageDirectory x7\<rbrakk> \<Longrightarrow> \<lbrace>?R48 s tcba x x7\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 6. \<And>s tcba x x8. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Frame x8\<rbrakk> \<Longrightarrow> \<lbrace>?R49 s tcba x x8\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 7. \<And>s tcba x. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R50 s tcba x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 8. \<And>s tcba x x10. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = IRQNode x10\<rbrakk> \<Longrightarrow> \<lbrace>?R51 s tcba x x10\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 9. \<And>s tcba. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s tcba\<rbrace> get_object obj_id \<lbrace>\<lambda>x sa. (x = Endpoint \<longrightarrow> True) \<and> (x = Notification \<longrightarrow> True) \<and> (\<forall>xa. x = Tcb xa \<longrightarrow> ?R44 s tcba x xa sa) \<and> (\<forall>xa. x = CNode xa \<longrightarrow> ?R45 s tcba x xa sa) \<and> (\<forall>xa. x = AsidPool xa \<longrightarrow> ?R46 s tcba x xa sa) \<and> (\<forall>xa. x = PageTable xa \<longrightarrow> ?R47 s tcba x xa sa) \<and> (\<forall>xa. x = PageDirectory xa \<longrightarrow> ?R48 s tcba x xa sa) \<and> (\<forall>xa. x = Frame xa \<longrightarrow> ?R49 s tcba x xa sa) \<and> (x = Untyped \<longrightarrow> ?R50 s tcba x sa) \<and> (\<forall>xa. x = IRQNode xa \<longrightarrow> ?R51 s tcba x xa sa)\<rbrace>
 10. \<And>s tcba sa. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); s = sa\<rbrakk> \<Longrightarrow> ?Q10 s tcba sa proof (prove)
goal (10 subgoals):
 1. \<And>s tcba x cdl_tcb. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Tcb cdl_tcb; object_clean (object_wipe_slots (Tcb cdl_tcb)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> \<lbrace>?P'69 s tcba (Tcb cdl_tcb) cdl_tcb\<rbrace> set_object obj_id (Tcb (f cdl_tcb)) \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 2. \<And>s tcba x x4. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = CNode x4\<rbrakk> \<Longrightarrow> \<lbrace>?R45 s tcba x x4\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 3. \<And>s tcba x x5. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = AsidPool x5\<rbrakk> \<Longrightarrow> \<lbrace>?R46 s tcba x x5\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 4. \<And>s tcba x x6. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageTable x6\<rbrakk> \<Longrightarrow> \<lbrace>?R47 s tcba x x6\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 5. \<And>s tcba x x7. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageDirectory x7\<rbrakk> \<Longrightarrow> \<lbrace>?R48 s tcba x x7\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 6. \<And>s tcba x x8. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Frame x8\<rbrakk> \<Longrightarrow> \<lbrace>?R49 s tcba x x8\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 7. \<And>s tcba x. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R50 s tcba x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 8. \<And>s tcba x x10. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = IRQNode x10\<rbrakk> \<Longrightarrow> \<lbrace>?R51 s tcba x x10\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 9. \<And>s tcba. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s tcba\<rbrace> get_object obj_id \<lbrace>\<lambda>x sa. (x = Endpoint \<longrightarrow> True) \<and> (x = Notification \<longrightarrow> True) \<and> (\<forall>xa. x = Tcb xa \<longrightarrow> (?P'69 s tcba x xa and K (object_clean (object_wipe_slots x) = object_clean (object_wipe_slots (Tcb tcb)))) sa) \<and> (\<forall>xa. x = CNode xa \<longrightarrow> ?R45 s tcba x xa sa) \<and> (\<forall>xa. x = AsidPool xa \<longrightarrow> ?R46 s tcba x xa sa) \<and> (\<forall>xa. x = PageTable xa \<longrightarrow> ?R47 s tcba x xa sa) \<and> (\<forall>xa. x = PageDirectory xa \<longrightarrow> ?R48 s tcba x xa sa) \<and> (\<forall>xa. x = Frame xa \<longrightarrow> ?R49 s tcba x xa sa) \<and> (x = Untyped \<longrightarrow> ?R50 s tcba x sa) \<and> (\<forall>xa. x = IRQNode xa \<longrightarrow> ?R51 s tcba x xa sa)\<rbrace>
 10. \<And>s tcba sa. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); s = sa\<rbrakk> \<Longrightarrow> ?Q10 s tcba sa proof (prove)
goal (13 subgoals):
 1. \<And>s tcba x cdl_tcb. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Tcb cdl_tcb; object_clean (object_wipe_slots (Tcb cdl_tcb)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> object_type (Tcb (f cdl_tcb)) = object_type (Tcb cdl_tcb)
 2. \<And>s tcba x cdl_tcb. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Tcb cdl_tcb; object_clean (object_wipe_slots (Tcb cdl_tcb)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> object_type (Tcb (f tcb)) = object_type (Tcb cdl_tcb)
 3. \<And>s tcba x cdl_tcb. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Tcb cdl_tcb; object_clean (object_wipe_slots (Tcb cdl_tcb)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> object_type (Tcb tcb) = object_type (Tcb cdl_tcb)
 4. \<And>s tcba x cdl_tcb. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Tcb cdl_tcb; object_clean (object_wipe_slots (Tcb cdl_tcb)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> object_wipe_slots (object_clean (Tcb (f tcb))) = object_wipe_slots (object_clean (Tcb (f cdl_tcb)))
 5. \<And>s tcba x x4. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = CNode x4\<rbrakk> \<Longrightarrow> \<lbrace>?R45 s tcba x x4\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 6. \<And>s tcba x x5. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = AsidPool x5\<rbrakk> \<Longrightarrow> \<lbrace>?R46 s tcba x x5\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 7. \<And>s tcba x x6. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageTable x6\<rbrakk> \<Longrightarrow> \<lbrace>?R47 s tcba x x6\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 8. \<And>s tcba x x7. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageDirectory x7\<rbrakk> \<Longrightarrow> \<lbrace>?R48 s tcba x x7\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 9. \<And>s tcba x x8. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Frame x8\<rbrakk> \<Longrightarrow> \<lbrace>?R49 s tcba x x8\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 10. \<And>s tcba x. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R50 s tcba x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s tcba x cdl_tcb. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Tcb cdl_tcb; object_clean (object_wipe_slots (Tcb cdl_tcb)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> object_clean (object_wipe_slots (Tcb (f tcb))) = object_clean (object_wipe_slots (Tcb (f cdl_tcb)))
 2. \<And>s tcba x x4. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = CNode x4\<rbrakk> \<Longrightarrow> \<lbrace>?R45 s tcba x x4\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 3. \<And>s tcba x x5. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = AsidPool x5\<rbrakk> \<Longrightarrow> \<lbrace>?R46 s tcba x x5\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 4. \<And>s tcba x x6. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageTable x6\<rbrakk> \<Longrightarrow> \<lbrace>?R47 s tcba x x6\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 5. \<And>s tcba x x7. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageDirectory x7\<rbrakk> \<Longrightarrow> \<lbrace>?R48 s tcba x x7\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 6. \<And>s tcba x x8. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Frame x8\<rbrakk> \<Longrightarrow> \<lbrace>?R49 s tcba x x8\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 7. \<And>s tcba x. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R50 s tcba x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 8. \<And>s tcba x x10. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = IRQNode x10\<rbrakk> \<Longrightarrow> \<lbrace>?R51 s tcba x x10\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 9. \<And>s tcba. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s tcba\<rbrace> get_object obj_id \<lbrace>\<lambda>x sa. (x = Endpoint \<longrightarrow> True) \<and> (x = Notification \<longrightarrow> True) \<and> (\<forall>xa. x = Tcb xa \<longrightarrow> ((\<lambda>a. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) a \<and> ko_at x obj_id a) and K (object_clean (object_wipe_slots x) = object_clean (object_wipe_slots (Tcb tcb)))) sa) \<and> (\<forall>xa. x = CNode xa \<longrightarrow> ?R45 s tcba x xa sa) \<and> (\<forall>xa. x = AsidPool xa \<longrightarrow> ?R46 s tcba x xa sa) \<and> (\<forall>xa. x = PageTable xa \<longrightarrow> ?R47 s tcba x xa sa) \<and> (\<forall>xa. x = PageDirectory xa \<longrightarrow> ?R48 s tcba x xa sa) \<and> (\<forall>xa. x = Frame xa \<longrightarrow> ?R49 s tcba x xa sa) \<and> (x = Untyped \<longrightarrow> ?R50 s tcba x sa) \<and> (\<forall>xa. x = IRQNode xa \<longrightarrow> ?R51 s tcba x xa sa)\<rbrace>
 10. \<And>s tcba sa. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); s = sa\<rbrakk> \<Longrightarrow> ?Q10 s tcba sa proof (prove)
goal (10 subgoals):
 1. \<And>s tcba x cdl_tcb. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Tcb cdl_tcb; object_clean (object_wipe_slots (Tcb (f cdl_tcb))) = object_clean (object_wipe_slots (Tcb (f tcb)))\<rbrakk> \<Longrightarrow> object_clean (object_wipe_slots (Tcb (f tcb))) = object_clean (object_wipe_slots (Tcb (f cdl_tcb)))
 2. \<And>s tcba x x4. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = CNode x4\<rbrakk> \<Longrightarrow> \<lbrace>?R45 s tcba x x4\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 3. \<And>s tcba x x5. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = AsidPool x5\<rbrakk> \<Longrightarrow> \<lbrace>?R46 s tcba x x5\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 4. \<And>s tcba x x6. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageTable x6\<rbrakk> \<Longrightarrow> \<lbrace>?R47 s tcba x x6\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 5. \<And>s tcba x x7. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageDirectory x7\<rbrakk> \<Longrightarrow> \<lbrace>?R48 s tcba x x7\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 6. \<And>s tcba x x8. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Frame x8\<rbrakk> \<Longrightarrow> \<lbrace>?R49 s tcba x x8\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 7. \<And>s tcba x. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R50 s tcba x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 8. \<And>s tcba x x10. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = IRQNode x10\<rbrakk> \<Longrightarrow> \<lbrace>?R51 s tcba x x10\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 9. \<And>s tcba. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s tcba\<rbrace> get_object obj_id \<lbrace>\<lambda>x sa. (x = Endpoint \<longrightarrow> True) \<and> (x = Notification \<longrightarrow> True) \<and> (\<forall>xa. x = Tcb xa \<longrightarrow> ((\<lambda>a. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) a \<and> ko_at x obj_id a) and K (object_clean (object_wipe_slots x) = object_clean (object_wipe_slots (Tcb tcb)))) sa) \<and> (\<forall>xa. x = CNode xa \<longrightarrow> ?R45 s tcba x xa sa) \<and> (\<forall>xa. x = AsidPool xa \<longrightarrow> ?R46 s tcba x xa sa) \<and> (\<forall>xa. x = PageTable xa \<longrightarrow> ?R47 s tcba x xa sa) \<and> (\<forall>xa. x = PageDirectory xa \<longrightarrow> ?R48 s tcba x xa sa) \<and> (\<forall>xa. x = Frame xa \<longrightarrow> ?R49 s tcba x xa sa) \<and> (x = Untyped \<longrightarrow> ?R50 s tcba x sa) \<and> (\<forall>xa. x = IRQNode xa \<longrightarrow> ?R51 s tcba x xa sa)\<rbrace>
 10. \<And>s tcba sa. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); s = sa\<rbrakk> \<Longrightarrow> ?Q10 s tcba sa proof (prove)
goal (9 subgoals):
 1. \<And>s tcba x x4. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = CNode x4\<rbrakk> \<Longrightarrow> \<lbrace>?R45 s tcba x x4\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 2. \<And>s tcba x x5. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = AsidPool x5\<rbrakk> \<Longrightarrow> \<lbrace>?R46 s tcba x x5\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 3. \<And>s tcba x x6. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageTable x6\<rbrakk> \<Longrightarrow> \<lbrace>?R47 s tcba x x6\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 4. \<And>s tcba x x7. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = PageDirectory x7\<rbrakk> \<Longrightarrow> \<lbrace>?R48 s tcba x x7\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 5. \<And>s tcba x x8. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Frame x8\<rbrakk> \<Longrightarrow> \<lbrace>?R49 s tcba x x8\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 6. \<And>s tcba x. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R50 s tcba x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 7. \<And>s tcba x x10. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); x = IRQNode x10\<rbrakk> \<Longrightarrow> \<lbrace>?R51 s tcba x x10\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (f tcb) \<and>* R)\<rbrace>
 8. \<And>s tcba. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb))\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 s tcba\<rbrace> get_object obj_id \<lbrace>\<lambda>x sa. (x = Endpoint \<longrightarrow> True) \<and> (x = Notification \<longrightarrow> True) \<and> (\<forall>xa. x = Tcb xa \<longrightarrow> ((\<lambda>a. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) a \<and> ko_at x obj_id a) and K (object_clean (object_wipe_slots x) = object_clean (object_wipe_slots (Tcb tcb)))) sa) \<and> (\<forall>xa. x = CNode xa \<longrightarrow> ?R45 s tcba x xa sa) \<and> (\<forall>xa. x = AsidPool xa \<longrightarrow> ?R46 s tcba x xa sa) \<and> (\<forall>xa. x = PageTable xa \<longrightarrow> ?R47 s tcba x xa sa) \<and> (\<forall>xa. x = PageDirectory xa \<longrightarrow> ?R48 s tcba x xa sa) \<and> (\<forall>xa. x = Frame xa \<longrightarrow> ?R49 s tcba x xa sa) \<and> (x = Untyped \<longrightarrow> ?R50 s tcba x sa) \<and> (\<forall>xa. x = IRQNode xa \<longrightarrow> ?R51 s tcba x xa sa)\<rbrace>
 9. \<And>s tcba sa. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); s = sa\<rbrakk> \<Longrightarrow> ?Q10 s tcba sa proof (prove)
goal (1 subgoal):
 1. \<And>s tcba sa. \<lbrakk>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcba); object_clean (object_wipe_slots (Tcb tcba)) = object_clean (object_wipe_slots (Tcb tcb)); s = sa\<rbrakk> \<Longrightarrow> cdl_objects sa obj_id \<noteq> None \<longrightarrow> (the (cdl_objects sa obj_id) = Endpoint \<longrightarrow> True) \<and> (the (cdl_objects sa obj_id) = Notification \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects sa obj_id) = Tcb x \<longrightarrow> ((\<lambda>a. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) a \<and> ko_at (the (cdl_objects sa obj_id)) obj_id a) and K (object_clean (object_wipe_slots (the (cdl_objects sa obj_id))) = object_clean (object_wipe_slots (Tcb tcb)))) sa) \<and> (\<forall>x. the (cdl_objects sa obj_id) = CNode x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects sa obj_id) = AsidPool x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects sa obj_id) = PageTable x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects sa obj_id) = PageDirectory x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects sa obj_id) = Frame x \<longrightarrow> True) \<and> (the (cdl_objects sa obj_id) = Untyped \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects sa obj_id) = IRQNode x \<longrightarrow> True) proof (prove)
goal:
No subgoals!