theory Ipc_AI

lemma set_mrs_valid_objs [wp]:
  "\<lbrace>valid_objs\<rbrace> set_mrs t a msgs \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (cases a) apply (simp add: set_mrs_redux) apply (wp thread_set_valid_objs_triv) apply (auto simp: tcb_cap_cases_def)[1] apply (simp add: valid_arch_arch_tcb_set_registers)+ apply (simp add: set_mrs_redux zipWithM_x_mapM split_def
                   store_word_offs_def
            split del: if_split) apply (wp mapM_wp' thread_set_valid_objs_triv | simp)+ apply (auto simp: tcb_cap_cases_def valid_arch_arch_tcb_set_registers) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> set_mrs t a msgs \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. a = None \<Longrightarrow> \<lbrace>valid_objs\<rbrace> set_mrs t a msgs \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 2. \<And>aa. a = Some aa \<Longrightarrow> \<lbrace>valid_objs\<rbrace> set_mrs t a msgs \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. a = None \<Longrightarrow> \<lbrace>valid_objs\<rbrace> do y <- thread_set (\<lambda>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>) t;
return (nat_to_len (min (length msg_registers) (length msgs)))
od \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 2. \<And>aa. a = Some aa \<Longrightarrow> \<lbrace>valid_objs\<rbrace> set_mrs t a msgs \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>tcb. a = None \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (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>) = getF tcb
 2. \<And>tcb. a = None \<Longrightarrow> tcb_state (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>) = tcb_state tcb
 3. \<And>tcb. a = None \<Longrightarrow> tcb_ipc_buffer (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>) = tcb_ipc_buffer tcb \<or> tcb_ipc_buffer (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>) = 0
 4. \<And>tcb. a = None \<Longrightarrow> tcb_fault_handler (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>) \<noteq> tcb_fault_handler tcb \<longrightarrow> length (tcb_fault_handler (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>)) = word_bits
 5. \<And>tcb. a = None \<Longrightarrow> tcb_fault (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>) \<noteq> tcb_fault tcb \<longrightarrow> (case tcb_fault (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>) of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f)
 6. \<And>tcb. a = None \<Longrightarrow> tcb_bound_notification (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>) \<noteq> tcb_bound_notification tcb \<longrightarrow> tcb_bound_notification (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>) = None
 7. \<And>tcb s. a = None \<Longrightarrow> valid_arch_tcb (tcb_arch (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>)) s = valid_arch_tcb (tcb_arch tcb) s
 8. \<And>s. \<lbrakk>a = None; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s
 9. \<And>aa. a = Some aa \<Longrightarrow> \<lbrace>valid_objs\<rbrace> set_mrs t a msgs \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>tcb. a = None \<Longrightarrow> tcb_state (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>) = tcb_state tcb
 2. \<And>tcb. a = None \<Longrightarrow> tcb_ipc_buffer (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>) = tcb_ipc_buffer tcb \<or> tcb_ipc_buffer (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>) = 0
 3. \<And>tcb. a = None \<Longrightarrow> tcb_fault_handler (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>) \<noteq> tcb_fault_handler tcb \<longrightarrow> length (tcb_fault_handler (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>)) = word_bits
 4. \<And>tcb. a = None \<Longrightarrow> tcb_fault (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>) \<noteq> tcb_fault tcb \<longrightarrow> (case tcb_fault (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>) of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f)
 5. \<And>tcb. a = None \<Longrightarrow> tcb_bound_notification (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>) \<noteq> tcb_bound_notification tcb \<longrightarrow> tcb_bound_notification (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>) = None
 6. \<And>tcb s. a = None \<Longrightarrow> valid_arch_tcb (tcb_arch (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>)) s = valid_arch_tcb (tcb_arch tcb) s
 7. \<And>s. \<lbrakk>a = None; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s
 8. \<And>aa. a = Some aa \<Longrightarrow> \<lbrace>valid_objs\<rbrace> set_mrs t a msgs \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>aa. a = Some aa \<Longrightarrow> \<lbrace>valid_objs\<rbrace> set_mrs t (Some aa) msgs \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>aa. a = Some aa \<Longrightarrow> \<lbrace>valid_objs\<rbrace> do _ <- do y <- thread_set (\<lambda>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>) t;
mapM (\<lambda>p. do y <- do s <- get;
assert (in_user_frame (aa + word_of_nat (fst p) * word_of_nat word_size) s)
od;
do_machine_op (storeWord (aa + word_of_nat (fst p) * word_of_nat word_size) (snd p))
od) (zip (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) (drop (length msg_registers) msgs))
od;
return (nat_to_len (min (length msgs) msg_max_length))
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>aa tcb. a = Some aa \<Longrightarrow> \<forall>x\<in>ran tcb_cap_cases. case x of (getF, v) \<Rightarrow> getF (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>) = getF tcb
 2. \<And>aa tcb. a = Some aa \<Longrightarrow> tcb_state (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>) = tcb_state tcb
 3. \<And>aa tcb. a = Some aa \<Longrightarrow> tcb_ipc_buffer (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>) = tcb_ipc_buffer tcb \<or> tcb_ipc_buffer (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>) = 0
 4. \<And>aa tcb. a = Some aa \<Longrightarrow> tcb_fault_handler (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>) \<noteq> tcb_fault_handler tcb \<longrightarrow> length (tcb_fault_handler (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>)) = word_bits
 5. \<And>aa tcb. a = Some aa \<Longrightarrow> tcb_fault (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>) \<noteq> tcb_fault tcb \<longrightarrow> (case tcb_fault (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>) of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f)
 6. \<And>aa tcb. a = Some aa \<Longrightarrow> tcb_bound_notification (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>) \<noteq> tcb_bound_notification tcb \<longrightarrow> tcb_bound_notification (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>) = None
 7. \<And>aa tcb s. a = Some aa \<Longrightarrow> valid_arch_tcb (tcb_arch (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>)) s = valid_arch_tcb (tcb_arch tcb) s
 8. \<And>aa s. \<lbrakk>a = Some aa; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal:
No subgoals!