theory CNodeInv_AI

lemma set_mrs_typ_at [wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_mrs p' b m \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (simp add: set_mrs_def bind_assoc set_object_def get_object_def) apply (cases b) apply simp apply wp apply clarsimp apply (drule get_tcb_SomeD) apply (clarsimp simp: obj_at_def) apply (clarsimp simp: zipWithM_x_mapM split_def
             split del: if_split) apply (wp mapM_wp') apply clarsimp apply (drule get_tcb_SomeD) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_mrs p' b m \<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 p');
x <- gets kheap;
xa <- assert (\<exists>y. x p' = Some y);
x <- assert (a_type (the (x p')) = ATCB);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(p' \<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>);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length m)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) m);
return $ nat_to_len $ min (length m) msg_max_length
od
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. b = None \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do tcb <- gets_the (get_tcb p');
x <- gets kheap;
xa <- assert (\<exists>y. x p' = Some y);
x <- assert (a_type (the (x p')) = ATCB);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(p' \<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>);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length m)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) m);
return $ nat_to_len $ min (length m) msg_max_length
od
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
 2. \<And>a. b = Some a \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do tcb <- gets_the (get_tcb p');
x <- gets kheap;
xa <- assert (\<exists>y. x p' = Some y);
x <- assert (a_type (the (x p')) = ATCB);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(p' \<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>);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length m)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) m);
return $ nat_to_len $ min (length m) msg_max_length
od
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. b = None \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do tcb <- gets_the (get_tcb p');
x <- gets kheap;
xa <- assert (\<exists>y. x p' = Some y);
x <- assert (a_type (the (x p')) = ATCB);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(p' \<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>);
return (nat_to_len (min (length msg_registers) (length m)))
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
 2. \<And>a. b = Some a \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do tcb <- gets_the (get_tcb p');
x <- gets kheap;
xa <- assert (\<exists>y. x p' = Some y);
x <- assert (a_type (the (x p')) = ATCB);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(p' \<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>);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length m)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) m);
return $ nat_to_len $ min (length m) msg_max_length
od
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>b = None; P (typ_at T p s)\<rbrakk> \<Longrightarrow> get_tcb p' s \<noteq> None \<longrightarrow> (\<exists>y. kheap s p' = Some y) \<longrightarrow> a_type (the (kheap s p')) = ATCB \<longrightarrow> P (typ_at T p (s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (the (get_tcb p' 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 p' s))) reg) (tcb_arch (the (get_tcb p' s)))\<rparr>))\<rparr>))
 2. \<And>a. b = Some a \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do tcb <- gets_the (get_tcb p');
x <- gets kheap;
xa <- assert (\<exists>y. x p' = Some y);
x <- assert (a_type (the (x p')) = ATCB);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(p' \<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>);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length m)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) m);
return $ nat_to_len $ min (length m) msg_max_length
od
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb. \<lbrakk>b = None; P (typ_at T p s); get_tcb p' s = Some y; kheap s p' = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (typ_at T p (s\<lparr>kheap := \<lambda>a. if a = p' then Some (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>)) else kheap s a\<rparr>))
 2. \<And>a. b = Some a \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do tcb <- gets_the (get_tcb p');
x <- gets kheap;
xa <- assert (\<exists>y. x p' = Some y);
x <- assert (a_type (the (x p')) = ATCB);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(p' \<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>);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length m)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) m);
return $ nat_to_len $ min (length m) msg_max_length
od
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb. \<lbrakk>b = None; P (typ_at T p s); kheap s p' = Some (TCB tcb); kheap s p' = Some (TCB y)\<rbrakk> \<Longrightarrow> P (typ_at T p (s\<lparr>kheap := \<lambda>a. if a = p' then Some (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>)) else kheap s a\<rparr>))
 2. \<And>a. b = Some a \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do tcb <- gets_the (get_tcb p');
x <- gets kheap;
xa <- assert (\<exists>y. x p' = Some y);
x <- assert (a_type (the (x p')) = ATCB);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(p' \<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>);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length m)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) m);
return $ nat_to_len $ min (length m) msg_max_length
od
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. b = Some a \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do tcb <- gets_the (get_tcb p');
x <- gets kheap;
xa <- assert (\<exists>y. x p' = Some y);
x <- assert (a_type (the (x p')) = ATCB);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(p' \<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>);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length m)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) m);
return $ nat_to_len $ min (length m) msg_max_length
od
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. b = Some a \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do tcb <- gets_the (get_tcb p');
x <- gets kheap;
xa <- assert (\<exists>y. x p' = Some y);
x <- assert (a_type (the (x p')) = ATCB);
x <- get;
y <- put (x\<lparr>kheap := (kheap x)(p' \<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>);
_ <- mapM (\<lambda>p. store_word_offs a (fst p) (snd p)) (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) m));
return (nat_to_len (min (length m) msg_max_length))
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a s. \<lbrakk>b = Some a; P (typ_at T p s)\<rbrakk> \<Longrightarrow> get_tcb p' s \<noteq> None \<longrightarrow> (\<exists>y. kheap s p' = Some y) \<longrightarrow> a_type (the (kheap s p')) = ATCB \<longrightarrow> P (typ_at T p (s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (the (get_tcb p' 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 p' s))) reg) (tcb_arch (the (get_tcb p' s)))\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>a s y tcb. \<lbrakk>b = Some a; P (typ_at T p s); get_tcb p' s = Some y; kheap s p' = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (typ_at T p (s\<lparr>kheap := \<lambda>a. if a = p' then Some (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>)) else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>a s y tcb. \<lbrakk>b = Some a; P (typ_at T p s); kheap s p' = Some (TCB tcb); kheap s p' = Some (TCB y)\<rbrakk> \<Longrightarrow> P (typ_at T p (s\<lparr>kheap := \<lambda>a. if a = p' then Some (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>)) else kheap s a\<rparr>)) proof (prove)
goal:
No subgoals!