theory VSpacePre_AI

lemma set_mrs_typ_at[wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_mrs t buf mrs \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (simp add: set_mrs_def zipWithM_x_mapM split_def
                   store_word_offs_def set_object_def get_object_def
              cong: option.case_cong
              split del: if_split) apply (wp hoare_vcg_split_case_option) apply (rule mapM_wp [where S=UNIV, simplified]) apply (wp | simp)+ apply (clarsimp simp: obj_at_def a_type_def
                  dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_mrs t buf mrs \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<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 mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
case buf of None \<Rightarrow> return (nat_to_len (min (length msg_registers) (length mrs))) | Some pptr \<Rightarrow> do _ <- mapM (\<lambda>p. do s <- get;
y <- assert (in_user_frame (pptr + word_of_nat (fst p) * word_of_nat word_size) s);
do_machine_op (storeWord (pptr + 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) mrs));
return (nat_to_len (min (length mrs) msg_max_length))
od
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tcb x xa pptr. xa = Some pptr \<Longrightarrow> \<lbrace>?Q7 tcb x xa pptr\<rbrace> mapM (\<lambda>p. do s <- get;
y <- assert (in_user_frame (pptr + word_of_nat (fst p) * word_of_nat word_size) s);
do_machine_op (storeWord (pptr + 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) mrs)) \<lbrace>\<lambda>xb a. P (typ_at T p a)\<rbrace>
 2. \<And>tcb. \<lbrace>?B5 tcb\<rbrace> 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 mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>))\<rparr>)
od \<lbrace>\<lambda>x s. (buf = None \<longrightarrow> P (typ_at T p s)) \<and> (\<forall>y. buf = Some y \<longrightarrow> ?Q7 tcb x buf y s)\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>?B5\<rbrace>
 4. \<And>s. P (typ_at T p s) \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>tcb x xa pptr xb. xa = Some pptr \<Longrightarrow> \<lbrace>\<lambda>a. P (typ_at T p a)\<rbrace> do s <- get;
y <- assert (in_user_frame (pptr + word_of_nat (fst xb) * word_of_nat word_size) s);
do_machine_op (storeWord (pptr + word_of_nat (fst xb) * word_of_nat word_size) (snd xb))
od \<lbrace>\<lambda>xb a. P (typ_at T p a)\<rbrace>
 2. \<And>tcb. \<lbrace>?B5 tcb\<rbrace> 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 mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>))\<rparr>)
od \<lbrace>\<lambda>x s. (buf = None \<longrightarrow> P (typ_at T p s)) \<and> (\<forall>y. buf = Some y \<longrightarrow> P (typ_at T p s))\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>?B5\<rbrace>
 4. \<And>s. P (typ_at T p s) \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (typ_at T p s) \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> (buf = None \<longrightarrow> P (typ_at T p (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! 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>)) else kheap s a\<rparr>))) \<and> ((\<exists>y. buf = Some y) \<longrightarrow> P (typ_at T p (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! 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>)) else kheap s a\<rparr>))) proof (prove)
goal:
No subgoals!