theory ArchIpc_AI

lemma do_ipc_transfer_respects_device_region[Ipc_AI_cont_assms]:
  "\<lbrace>cap_refs_respects_device_region and tcb_at t and  valid_objs and valid_mdb\<rbrace>
   do_ipc_transfer t ep bg grt r
   \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" apply (wpsimp simp: do_ipc_transfer_def do_normal_transfer_def transfer_caps_def bind_assoc
                  wp: hoare_vcg_all_lift hoare_drop_imps)+ apply (subst ball_conj_distrib) apply (wpsimp wp: get_rs_cte_at2 thread_get_wp hoare_weak_lift_imp grs_distinct
                           hoare_vcg_ball_lift hoare_vcg_all_lift hoare_vcg_conj_lift
                     simp: obj_at_def is_tcb_def)+ apply (simp split: kernel_object.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and tcb_at t and valid_objs and valid_mdb\<rbrace> do_ipc_transfer t ep bg grt r \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>recv_buffer send_buffer mi x xa xb. \<lbrace>?P'58 recv_buffer send_buffer mi x xa xb\<rbrace> get_receive_slots r recv_buffer \<lbrace>\<lambda>rv s. (\<forall>slot\<in>set rv. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot s) \<and> (\<forall>x\<in>set x. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) \<and> distinct rv\<rbrace>
 2. \<And>recv_buffer send_buffer mi x. \<lbrace>?B24 recv_buffer send_buffer mi x\<rbrace> copy_mrs t send_buffer r recv_buffer (mi_length mi) \<lbrace>\<lambda>xa s. cap_refs_respects_device_region s \<and> (\<forall>xb. (cap_refs_respects_device_region and valid_objs and valid_mdb) s \<and> ?P'58 recv_buffer send_buffer mi x xa xb s)\<rbrace>
 3. \<And>recv_buffer send_buffer mi. \<lbrace>?B22 recv_buffer send_buffer mi\<rbrace> if grt then lookup_extra_caps t send_buffer mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?B24 recv_buffer send_buffer mi\<rbrace>
 4. \<And>recv_buffer send_buffer. \<lbrace>?B16 recv_buffer (ds_id None) send_buffer\<rbrace> get_message_info t \<lbrace>?B22 recv_buffer send_buffer\<rbrace>
 5. \<And>recv_buffer fault. fault = None \<Longrightarrow> \<lbrace>?R12 recv_buffer fault\<rbrace> lookup_ipc_buffer False t \<lbrace>?B16 recv_buffer fault\<rbrace>
 6. \<And>recv_buffer fault x2. fault = Some x2 \<Longrightarrow> \<lbrace>?R13 recv_buffer fault x2\<rbrace> do_fault_transfer bg t r recv_buffer \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>
 7. \<And>recv_buffer. \<lbrace>?B2 recv_buffer\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> ?R12 recv_buffer fault s) \<and> (\<forall>x. fault = Some x \<longrightarrow> ?R13 recv_buffer fault x s)\<rbrace>
 8. \<lbrace>?Q1\<rbrace> lookup_ipc_buffer True r \<lbrace>?B2\<rbrace>
 9. \<And>s. (cap_refs_respects_device_region and tcb_at t and valid_objs and valid_mdb) s \<Longrightarrow> ?Q1 s proof (prove)
goal (9 subgoals):
 1. \<And>recv_buffer send_buffer mi x xa xb. \<lbrace>?P'66 recv_buffer recv_buffer send_buffer mi x xa xb (?send_buffer65 recv_buffer send_buffer mi x xa xb) (?mi65 recv_buffer send_buffer mi x xa xb) x (?xa65 recv_buffer send_buffer mi x xa xb) (?xb65 recv_buffer send_buffer mi x xa xb)\<rbrace> get_receive_slots r recv_buffer \<lbrace>\<lambda>rv s. ((\<forall>x\<in>set rv. real_cte_at x s) \<and> (\<forall>x\<in>set rv. cte_wp_at (\<lambda>cap. cap = NullCap) x s)) \<and> (\<forall>x\<in>set x. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) \<and> distinct rv\<rbrace>
 2. \<And>recv_buffer send_buffer mi x. \<lbrace>?B24 recv_buffer send_buffer mi x\<rbrace> copy_mrs t send_buffer r recv_buffer (mi_length mi) \<lbrace>\<lambda>xa s. cap_refs_respects_device_region s \<and> (\<forall>xb. (cap_refs_respects_device_region and valid_objs and valid_mdb) s \<and> ?P'66 recv_buffer recv_buffer send_buffer mi x xa xb (?send_buffer65 recv_buffer send_buffer mi x xa xb) (?mi65 recv_buffer send_buffer mi x xa xb) x (?xa65 recv_buffer send_buffer mi x xa xb) (?xb65 recv_buffer send_buffer mi x xa xb) s)\<rbrace>
 3. \<And>recv_buffer send_buffer mi. \<lbrace>?B22 recv_buffer send_buffer mi\<rbrace> if grt then lookup_extra_caps t send_buffer mi <catch> (\<lambda>y. return []) else return [] \<lbrace>?B24 recv_buffer send_buffer mi\<rbrace>
 4. \<And>recv_buffer send_buffer. \<lbrace>?B16 recv_buffer (ds_id None) send_buffer\<rbrace> get_message_info t \<lbrace>?B22 recv_buffer send_buffer\<rbrace>
 5. \<And>recv_buffer fault. fault = None \<Longrightarrow> \<lbrace>?R12 recv_buffer fault\<rbrace> lookup_ipc_buffer False t \<lbrace>?B16 recv_buffer fault\<rbrace>
 6. \<And>recv_buffer fault x2. fault = Some x2 \<Longrightarrow> \<lbrace>?R13 recv_buffer fault x2\<rbrace> do_fault_transfer bg t r recv_buffer \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>
 7. \<And>recv_buffer. \<lbrace>?B2 recv_buffer\<rbrace> thread_get tcb_fault t \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> ?R12 recv_buffer fault s) \<and> (\<forall>x. fault = Some x \<longrightarrow> ?R13 recv_buffer fault x s)\<rbrace>
 8. \<lbrace>?Q1\<rbrace> lookup_ipc_buffer True r \<lbrace>?B2\<rbrace>
 9. \<And>s. (cap_refs_respects_device_region and tcb_at t and valid_objs and valid_mdb) s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>cap_refs_respects_device_region s; valid_objs s; valid_mdb s; kheap s t = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> \<exists>tcb. ko = TCB tcb proof (prove)
goal:
No subgoals!