theory TCB_DP

lemma decode_invocation_tcb_rv':
"\<lbrace>\<lambda>s. P (
     ThreadControl
        (cap_object cap)
         cap_ref
        (Some fault_ep)
        (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot))
        (Some (vroot_cap, vroot_slot))
        (Some ((reset_mem_mapping ipcbuff_cap),ipcbuff_slot))) s \<and>
   caps = [(croot_cap,croot_slot), (vroot_cap,vroot_slot), (ipcbuff_cap, ipcbuff_slot)]@xs \<and>
   cap_has_object cap \<and> buffer \<noteq> 0 \<rbrace>
decode_tcb_invocation cap cap_ref caps (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer)
\<lbrace>P\<rbrace>, -" apply (clarsimp simp: decode_tcb_invocation_def) apply wp apply (wp throw_on_none_rvR)+ apply (safe) apply (clarsimp simp: get_index_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot))) s \<and> caps = [(croot_cap, croot_slot), (vroot_cap, vroot_slot), (ipcbuff_cap, ipcbuff_slot)] @ xs \<and> cap_has_object cap \<and> buffer \<noteq> 0\<rbrace> decode_tcb_invocation cap cap_ref caps (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer) \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot))) s \<and> caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs \<and> cap_has_object cap \<and> buffer \<noteq> 0\<rbrace> doE cspace_root <- throw_on_none (get_index caps 0);
vspace_root <- throw_on_none (get_index caps (Suc 0));
buffer_frame <- throw_on_none (get_index caps 2);
returnOk (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data (fst cspace_root) cspace_root_data, snd cspace_root)) (Some vspace_root) (if buffer \<noteq> 0 then Some (reset_mem_mapping (fst buffer_frame), snd buffer_frame) else None))
odE \<sqinter> throw \<lbrace>P\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>cspace_root vspace_root. \<lbrace>?P'11 cspace_root vspace_root\<rbrace> throw_on_none (get_index caps 2) \<lbrace>\<lambda>buffer_frame. P (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data (fst cspace_root) cspace_root_data, snd cspace_root)) (Some vspace_root) (if buffer \<noteq> 0 then Some (reset_mem_mapping (fst buffer_frame), snd buffer_frame) else None))\<rbrace>, -
 2. \<And>cspace_root. \<lbrace>?B6 cspace_root\<rbrace> throw_on_none (get_index caps (Suc 0)) \<lbrace>\<lambda>vspace_root s. True \<and> ?P'11 cspace_root vspace_root s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?P'4\<rbrace> throw_on_none (get_index caps 0) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?P'3\<rbrace> throw \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. P (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot))) s \<and> caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs \<and> cap_has_object cap \<and> buffer \<noteq> 0 \<Longrightarrow> ((\<lambda>s. True \<and> ?P'4 s) and ?P'3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot))) s \<and> caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs \<and> cap_has_object cap \<and> buffer \<noteq> 0 \<Longrightarrow> ((\<lambda>s. True \<and> True \<and> (case get_index caps 0 of None \<Rightarrow> True | Some y \<Rightarrow> True \<and> (case get_index caps (Suc 0) of None \<Rightarrow> True | Some ya \<Rightarrow> True \<and> (case get_index caps 2 of None \<Rightarrow> True | Some yb \<Rightarrow> P (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data (fst y) cspace_root_data, snd y)) (Some ya) (if buffer \<noteq> 0 then Some (reset_mem_mapping (fst yb), snd yb) else None)) s)))) and (\<lambda>s. True \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot))) s; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; buffer \<noteq> 0\<rbrakk> \<Longrightarrow> case get_index ((croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs) 0 of None \<Rightarrow> True | Some y \<Rightarrow> True \<and> (case get_index ((croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs) (Suc 0) of None \<Rightarrow> True | Some ya \<Rightarrow> True \<and> (case get_index ((croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs) 2 of None \<Rightarrow> True | Some yb \<Rightarrow> P (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data (fst y) cspace_root_data, snd y)) (Some ya) (if buffer \<noteq> 0 then Some (reset_mem_mapping (fst yb), snd yb) else None)) s)) proof (prove)
goal:
No subgoals!