theory Ipc_DR

lemma transfer_caps_loop_None:
  "dcorres dc \<top>
           (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs)
           (Endpoint_D.transfer_caps_loop ep rcv caps None)
           (return x)" apply (induct caps arbitrary: x) apply simp apply clarsimp apply (rule corres_dummy_return_r) apply (rule corres_guard_imp) apply (rule corres_split[where r'=dc]) apply (rule dcorres_dummy_corrupt_ipc_buffer) apply assumption apply wp+ apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop ep rcv caps None) (return x) proof (prove)
goal (2 subgoals):
 1. \<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop ep rcv [] None) (return x)
 2. \<And>a caps x. (\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop ep rcv caps None) (return x)) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop ep rcv (a # caps) None) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>a caps x. (\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop ep rcv caps None) (return x)) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop ep rcv (a # caps) None) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>a caps x. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (do y <- corrupt_ipc_buffer rcv True;
Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>a caps x. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (do y <- corrupt_ipc_buffer rcv True;
Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None
od) (return x >>= return) proof (prove)
goal (3 subgoals):
 1. \<And>a caps x. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a)\<rbrakk> \<Longrightarrow> dcorres dc (?Q13 a caps x) (?Q'13 a caps x) (do y <- corrupt_ipc_buffer rcv True;
Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None
od) (return x >>= return)
 2. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); True\<rbrakk> \<Longrightarrow> ?Q13 a caps x s
 3. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'13 a caps x s proof (prove)
goal (6 subgoals):
 1. \<And>a caps x. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a)\<rbrakk> \<Longrightarrow> dcorres dc (?P17 a caps x) (?P'17 a caps x) (corrupt_ipc_buffer rcv True) (return x)
 2. \<And>a caps x y xa. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); dc y xa\<rbrakk> \<Longrightarrow> dcorres dc (?R17 a caps x y) (?R'17 a caps x xa) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return xa)
 3. \<And>a caps x. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 a caps x\<rbrace> corrupt_ipc_buffer rcv True \<lbrace>?R17 a caps x\<rbrace>
 4. \<And>a caps x. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 a caps x\<rbrace> return x \<lbrace>?R'17 a caps x\<rbrace>
 5. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); True\<rbrakk> \<Longrightarrow> (?P17 a caps x and ?Q17 a caps x) s
 6. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'17 a caps x and ?Q'17 a caps x) s proof (prove)
goal (5 subgoals):
 1. \<And>a caps x y xa. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); dc y xa\<rbrakk> \<Longrightarrow> dcorres dc (?R17 a caps x y) (?R'17 a caps x xa) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return xa)
 2. \<And>a caps x. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 a caps x\<rbrace> corrupt_ipc_buffer rcv True \<lbrace>?R17 a caps x\<rbrace>
 3. \<And>a caps x. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 a caps x\<rbrace> return x \<lbrace>?R'17 a caps x\<rbrace>
 4. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 a caps x) s
 5. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) s\<rbrakk> \<Longrightarrow> (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs and ?Q'17 a caps x) s proof (prove)
goal (4 subgoals):
 1. \<And>a caps x. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 a caps x\<rbrace> corrupt_ipc_buffer rcv True \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>a caps x. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 a caps x\<rbrace> return x \<lbrace>\<lambda>xa. tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs\<rbrace>
 3. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 a caps x) s
 4. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) s\<rbrakk> \<Longrightarrow> (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs and ?Q'17 a caps x) s proof (prove)
goal (2 subgoals):
 1. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 2. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) s\<rbrakk> \<Longrightarrow> (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs and (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs)) s proof (prove)
goal (1 subgoal):
 1. \<And>a caps x s. \<lbrakk>\<And>x. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) (Endpoint_D.transfer_caps_loop (Some (cap_object a)) rcv caps None) (return x); Types_D.is_ep_cap a; ep = Some (cap_object a); (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs) s\<rbrakk> \<Longrightarrow> (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs and (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs)) s proof (prove)
goal:
No subgoals!