theory Ipc_AI

lemma set_mrs_valid_ioc[wp]:
  "\<And>thread buf msgs.
    \<lbrace>valid_ioc :: 'state_ext state \<Rightarrow> bool\<rbrace>
      set_mrs thread buf msgs
    \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (simp add: set_mrs_def) apply (wp | wpc)+ apply (simp only: zipWithM_x_mapM_x split_def) apply (wp mapM_x_wp' set_object_valid_ioc_caps hoare_weak_lift_imp
        | simp)+ apply (clarsimp simp: obj_at_def get_tcb_def valid_ioc_def
                  split: option.splits Structures_A.kernel_object.splits) apply (drule spec, drule spec, erule impE, assumption) apply (clarsimp simp: cap_of_def tcb_cnode_map_tcb_cap_cases
                        cte_wp_at_cases null_filter_def) apply (simp add: tcb_cap_cases_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>thread buf msgs. \<lbrace>valid_ioc\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread buf msgs. \<lbrace>valid_ioc\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>));
case buf of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length msgs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) msgs);
return $ nat_to_len $ min (length msgs) msg_max_length
od
od \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread buf msgs tcb x x2. buf = Some x2 \<Longrightarrow> \<lbrace>?R12 thread buf msgs tcb x x2\<rbrace> zipWithM_x (store_word_offs x2) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) msgs) \<lbrace>\<lambda>xa. valid_ioc\<rbrace>
 2. \<And>thread buf msgs tcb. \<lbrace>?B1 thread buf msgs tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>)) \<lbrace>\<lambda>x s. (buf = None \<longrightarrow> valid_ioc s) \<and> (\<forall>xa. buf = Some xa \<longrightarrow> ?R12 thread buf msgs tcb x xa s)\<rbrace>
 3. \<And>thread buf msgs. \<lbrace>?Q thread buf msgs\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1 thread buf msgs\<rbrace>
 4. \<And>thread buf msgs s. valid_ioc s \<Longrightarrow> ?Q thread buf msgs s proof (prove)
goal (4 subgoals):
 1. \<And>thread buf msgs tcb x x2. buf = Some x2 \<Longrightarrow> \<lbrace>?R12 thread (Some x2) msgs tcb x x2\<rbrace> mapM_x (\<lambda>p. store_word_offs x2 (fst p) (snd p)) (zip [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) msgs)) \<lbrace>\<lambda>xa. valid_ioc\<rbrace>
 2. \<And>thread buf msgs tcb. \<lbrace>?B1 thread buf msgs tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>)) \<lbrace>\<lambda>x s. (buf = None \<longrightarrow> valid_ioc s) \<and> (\<forall>xa. buf = Some xa \<longrightarrow> ?R12 thread buf msgs tcb x xa s)\<rbrace>
 3. \<And>thread buf msgs. \<lbrace>?Q thread buf msgs\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1 thread buf msgs\<rbrace>
 4. \<And>thread buf msgs s. valid_ioc s \<Longrightarrow> ?Q thread buf msgs s proof (prove)
goal (1 subgoal):
 1. \<And>thread msgs s. valid_ioc s \<Longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> typ_at ATCB thread s \<and> (\<forall>b. is_original_cap s (thread, b) \<longrightarrow> (\<exists>y. null_filter (cap_of (TCB (the (get_tcb thread s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch (the (get_tcb thread s))) reg) (tcb_arch (the (get_tcb thread s)))\<rparr>))) b = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>thread msgs s x2 b. \<lbrakk>\<forall>a b. is_original_cap s (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s; kheap s thread = Some (TCB x2); is_original_cap s (thread, b)\<rbrakk> \<Longrightarrow> \<exists>y. null_filter (cap_of (TCB (x2\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch x2) reg) (tcb_arch x2)\<rparr>))) b = Some y proof (prove)
goal (1 subgoal):
 1. \<And>thread msgs s x2 b. \<lbrakk>kheap s thread = Some (TCB x2); is_original_cap s (thread, b); cte_wp_at (\<lambda>x. x \<noteq> NullCap) (thread, b) s\<rbrakk> \<Longrightarrow> \<exists>y. null_filter (cap_of (TCB (x2\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch x2) reg) (tcb_arch x2)\<rparr>))) b = Some y proof (prove)
goal (1 subgoal):
 1. \<And>thread msgs s x2 b get seta restr. \<lbrakk>kheap s thread = Some (TCB x2); is_original_cap s (thread, b); get x2 \<noteq> NullCap; tcb_cap_cases b = Some (get, seta, restr); get (x2\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch x2) reg) (tcb_arch x2)\<rparr>) = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!