theory TCB_DP

lemma tcb_update_thread_slot_wp:
 "\<lbrace><(target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R> and K (\<not> is_untyped_cap (ipc_buffer_cap))\<rbrace>
     tcb_update_thread_slot target_tcb tcb_cap_slot thread_slot (ipc_buffer_cap, ipc_buffer_slot)
    \<lbrace>\<lambda>_. <(target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R>\<rbrace>, \<lbrace>E\<rbrace>" apply (clarsimp simp: tcb_update_thread_slot_def) apply (rule hoare_name_pre_state) apply (clarsimp) apply wp apply (wp insert_cap_child_wp) apply (wp insert_cap_sibling_wp get_cap_rv)+ apply (safe) apply (sep_solve) apply (drule not_memory_cap_reset_asid') apply (clarsimp simp: is_memory_cap_def split:cdl_cap.splits) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType)\<rbrace> tcb_update_thread_slot target_tcb tcb_cap_slot thread_slot (ipc_buffer_cap, ipc_buffer_slot) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType)\<rbrace> do thread_cap <- get_cap tcb_cap_slot;
when (thread_cap = TcbCap target_tcb) (insert_cap_child ipc_buffer_cap ipc_buffer_slot (target_tcb, thread_slot) \<sqinter> insert_cap_sibling ipc_buffer_cap ipc_buffer_slot (target_tcb, thread_slot))
od \<lbrace>\<lambda>_. cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> do thread_cap <- get_cap tcb_cap_slot;
when (thread_cap = TcbCap target_tcb) (insert_cap_child ipc_buffer_cap ipc_buffer_slot (target_tcb, thread_slot) \<sqinter> insert_cap_sibling ipc_buffer_cap ipc_buffer_slot (target_tcb, thread_slot))
od \<lbrace>\<lambda>_. cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do thread_cap <- get_cap tcb_cap_slot;
when (thread_cap = TcbCap target_tcb) (insert_cap_child ipc_buffer_cap ipc_buffer_slot (target_tcb, thread_slot) \<sqinter> insert_cap_sibling ipc_buffer_cap ipc_buffer_slot (target_tcb, thread_slot))
od \<lbrace>\<lambda>_. cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s thread_cap. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type ipc_buffer_cap \<noteq> Some UntypedType; thread_cap = TcbCap target_tcb\<rbrakk> \<Longrightarrow> \<lbrace>?P6 s thread_cap\<rbrace> insert_cap_child ipc_buffer_cap ipc_buffer_slot (target_tcb, thread_slot) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)\<rbrace>
 2. \<And>s thread_cap. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type ipc_buffer_cap \<noteq> Some UntypedType; thread_cap = TcbCap target_tcb\<rbrakk> \<Longrightarrow> \<lbrace>?P'6 s thread_cap\<rbrace> insert_cap_sibling ipc_buffer_cap ipc_buffer_slot (target_tcb, thread_slot) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)\<rbrace>
 3. \<And>s. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> \<lbrace>?Q3 s\<rbrace> get_cap tcb_cap_slot \<lbrace>\<lambda>thread_cap. if thread_cap = TcbCap target_tcb then ?P6 s thread_cap and ?P'6 s thread_cap else cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)\<rbrace>
 4. \<And>s sa. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type ipc_buffer_cap \<noteq> Some UntypedType; s = sa\<rbrakk> \<Longrightarrow> ?Q3 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s thread_cap. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type ipc_buffer_cap \<noteq> Some UntypedType; thread_cap = TcbCap target_tcb\<rbrakk> \<Longrightarrow> \<lbrace>?P'6 s thread_cap\<rbrace> insert_cap_sibling ipc_buffer_cap ipc_buffer_slot (target_tcb, thread_slot) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)\<rbrace>
 2. \<And>s. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> \<lbrace>?Q3 s\<rbrace> get_cap tcb_cap_slot \<lbrace>\<lambda>thread_cap. if thread_cap = TcbCap target_tcb then cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType) and ?P'6 s thread_cap else cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)\<rbrace>
 3. \<And>s sa. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type ipc_buffer_cap \<noteq> Some UntypedType; s = sa\<rbrakk> \<Longrightarrow> ?Q3 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type ipc_buffer_cap \<noteq> Some UntypedType; s = sa\<rbrakk> \<Longrightarrow> cdl.lift (tcb_cap_slot \<mapsto>c ?cap14 s \<and>* ?R14 s) sa \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid (?cap14 s) \<longrightarrow> (if c = TcbCap target_tcb then cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType) and (cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType)) else cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)) sa) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sa; cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> cdl.lift (tcb_cap_slot \<mapsto>c ?cap14 sa \<and>* ?R14 sa) sa
 2. \<And>s sa c. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sa; cap_type ipc_buffer_cap \<noteq> Some UntypedType; reset_cap_asid c = reset_cap_asid (?cap14 sa)\<rbrakk> \<Longrightarrow> (if c = TcbCap target_tcb then cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType) and (cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType)) else cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa c. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sa; cap_type ipc_buffer_cap \<noteq> Some UntypedType; reset_cap_asid c = reset_cap_asid (TcbCap target_tcb)\<rbrakk> \<Longrightarrow> (if c = TcbCap target_tcb then cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType) and (cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType)) else cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s sa c. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sa; cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> \<not> is_memory_cap (TcbCap target_tcb)
 2. \<And>s sa c. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sa; cap_type ipc_buffer_cap \<noteq> Some UntypedType; c = TcbCap target_tcb\<rbrakk> \<Longrightarrow> (if c = TcbCap target_tcb then cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType) and (cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType)) else cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa c. \<lbrakk>cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sa; cap_type ipc_buffer_cap \<noteq> Some UntypedType; c = TcbCap target_tcb\<rbrakk> \<Longrightarrow> (if c = TcbCap target_tcb then cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType) and (cdl.lift ((target_tcb, thread_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType)) else cdl.lift ((target_tcb, thread_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R)) sa proof (prove)
goal:
No subgoals!