theory Ipc_AI

lemma set_mrs_only_idle [wp]:
  "\<lbrace>only_idle\<rbrace> set_mrs t b m \<lbrace>\<lambda>_. only_idle\<rbrace>" apply (simp add: set_mrs_def split_def zipWithM_x_mapM
                   set_object_def get_object_def
              cong: option.case_cong
               del: upt.simps) apply (wp mapM_wp'|wpc)+ apply (clarsimp simp del: fun_upd_apply) apply (erule only_idle_tcb_update) apply (drule get_tcb_SomeD) apply (fastforce simp: obj_at_def) by (simp add: get_tcb_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> set_mrs t b m \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> do tcb <- gets_the (get_tcb t);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
case b of None \<Rightarrow> return (nat_to_len (min (length msg_registers) (length m))) | Some pptr \<Rightarrow> do _ <- mapM (\<lambda>p. store_word_offs pptr (fst p) (snd p)) (zip [Suc (length msg_registers)..<Suc msg_max_length] (drop (length msg_registers) m));
return (nat_to_len (min (length m) msg_max_length))
od
od \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. only_idle s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> (b = None \<longrightarrow> only_idle (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch (the (get_tcb t s))) reg) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) \<and> (\<forall>x. b = Some x \<longrightarrow> only_idle (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch (the (get_tcb t s))) reg) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>only_idle s; get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> only_idle (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch y) reg) (tcb_arch y)\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ko_at (TCB (?t51 s y tcb)) t s
 2. \<And>s y tcb. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> tcb_state (?t51 s y tcb) = tcb_state (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch y) reg) (tcb_arch y)\<rparr>) \<or> tcb_state (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch y) reg) (tcb_arch y)\<rparr>) \<noteq> IdleThreadState proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb. \<lbrakk>kheap s t = Some (TCB tcb); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> ko_at (TCB (?t51 s y tcb)) t s
 2. \<And>s y tcb. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> tcb_state (?t51 s y tcb) = tcb_state (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch y) reg) (tcb_arch y)\<rparr>) \<or> tcb_state (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch y) reg) (tcb_arch y)\<rparr>) \<noteq> IdleThreadState proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> tcb_state tcb = tcb_state (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch y) reg) (tcb_arch y)\<rparr>) \<or> tcb_state (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length m) msg_registers) then m ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch y) reg) (tcb_arch y)\<rparr>) \<noteq> IdleThreadState