theory SyscallArgs_C

lemma getMRs_tcbContext:
  "\<lbrace>\<lambda>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s\<rbrace>
  getMRs thread buffer info
  \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (ARM_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace>" apply (rule hoare_assume_pre) apply (elim conjE) apply (thin_tac "thread = t" for t) apply (clarsimp simp add: getMRs_def) apply (wp|wpc)+ apply (rule_tac P="n < length x" in hoare_gen_asm) apply (clarsimp simp: nth_append) apply (wp mapM_wp' hoare_weak_lift_imp)+ apply simp apply (rule asUser_cur_obj_at') apply (simp add: getRegister_def msgRegisters_unfold) apply (simp add: mapM_Cons bind_assoc mapM_empty) apply wp apply (wp hoare_drop_imps hoare_vcg_all_lift) apply (wp asUser_cur_obj_at') apply (simp add: getRegister_def msgRegisters_unfold) apply (simp add: mapM_Cons bind_assoc mapM_empty) apply (wp asUser_const_rv) apply clarsimp apply (wp asUser_const_rv) apply (clarsimp simp: n_msgRegisters_def msgRegisters_unfold) apply (simp add: nth_Cons' cur_tcb'_def split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s\<rbrace> getMRs thread buffer info \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s \<Longrightarrow> \<lbrace>\<lambda>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s\<rbrace> getMRs thread buffer info \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); thread = ksCurThread s; cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s\<rbrace> getMRs thread buffer info \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s\<rbrace> getMRs thread buffer info \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. thread = ksCurThread s \<and> cur_tcb' s\<rbrace> do hardwareMRValues <- asUser thread (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser;
return (take (unat (msgLength info)) hardwareMRValues @ take (unat (msgLength info) - length hardwareMRValues) bufferMRValues)
od \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s x x2 xa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; buffer = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B28 s x x2 xa\<rbrace> mapM loadWordUser xa \<lbrace>\<lambda>bufferMRValues a. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = (take (unat (msgLength info)) x @ take (unat (msgLength info) - length x) bufferMRValues) ! n) (ksCurThread a) a\<rbrace>
 2. \<And>s x x2. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; buffer = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 s x x2\<rbrace> return (map (\<lambda>x. x2 + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) \<lbrace>?B28 s x x2\<rbrace>
 3. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>x sa. (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = (take (unat (msgLength info)) x @ take (unat (msgLength info) - length x) []) ! n) (ksCurThread sa) sa) \<and> (\<forall>xa. buffer = Some xa \<longrightarrow> ?R22 s x xa sa)\<rbrace>
 4. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> ?Q9 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s x x2 xa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; buffer = Some x2; n < length x\<rbrakk> \<Longrightarrow> \<lbrace>?P'30 s x x2 xa\<rbrace> mapM loadWordUser xa \<lbrace>\<lambda>bufferMRValues a. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = (take (unat (msgLength info)) x @ take (unat (msgLength info) - length x) bufferMRValues) ! n) (ksCurThread a) a\<rbrace>
 2. \<And>s x x2. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; buffer = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 s x x2\<rbrace> return (map (\<lambda>x. x2 + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) \<lbrace>\<lambda>xa. ?P'30 s x x2 xa and K (n < length x)\<rbrace>
 3. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>x sa. (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = (take (unat (msgLength info)) x @ take (unat (msgLength info) - length x) []) ! n) (ksCurThread sa) sa) \<and> (\<forall>xa. buffer = Some xa \<longrightarrow> ?R22 s x xa sa)\<rbrace>
 4. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> ?Q9 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s x x2 xa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; buffer = Some x2; n < length x\<rbrakk> \<Longrightarrow> \<lbrace>?P'30 s x x2 xa\<rbrace> mapM loadWordUser xa \<lbrace>\<lambda>bufferMRValues a. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = x ! n) (ksCurThread a) a\<rbrace>
 2. \<And>s x x2. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; buffer = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 s x x2\<rbrace> return (map (\<lambda>x. x2 + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) \<lbrace>\<lambda>xa. ?P'30 s x x2 xa and K (n < length x)\<rbrace>
 3. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>x sa. (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = (take (unat (msgLength info)) x @ take (unat (msgLength info) - length x) []) ! n) (ksCurThread sa) sa) \<and> (\<forall>xa. buffer = Some xa \<longrightarrow> ?R22 s x xa sa)\<rbrace>
 4. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> ?Q9 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'44 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = (take (unat (msgLength info)) rv @ take (unat (msgLength info) - length rv) []) ! n) (ksCurThread s) s\<rbrace>
 2. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'43 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. \<forall>x. buffer = Some x \<longrightarrow> ((\<lambda>a. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread a) a) and K (n < length rv)) s\<rbrace>
 3. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> ?P'44 s sa) \<and> ?P'43 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'44 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace>
 2. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'43 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. \<forall>x. buffer = Some x \<longrightarrow> ((\<lambda>a. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread a) a) and K (n < length rv)) s\<rbrace>
 3. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> ?P'44 s sa) \<and> ?P'43 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P46 s\<rbrace> mapM getRegister TCB_H.msgRegisters \<lbrace>\<lambda>a b. b (TCB_H.msgRegisters ! n) = a ! n\<rbrace>
 2. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'43 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. \<forall>x. buffer = Some x \<longrightarrow> ((\<lambda>a. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread a) a) and K (n < length rv)) s\<rbrace>
 3. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. ?P46 s (atcbContextGet (tcbArch tcb))) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> ?P'43 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P46 s\<rbrace> mapM (\<lambda>a. gets (\<lambda>uc. uc a)) [register.R2, register.R3, register.R4, register.R5] \<lbrace>\<lambda>a b. b ([register.R2, register.R3, register.R4, register.R5] ! n) = a ! n\<rbrace>
 2. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'43 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. \<forall>x. buffer = Some x \<longrightarrow> ((\<lambda>a. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread a) a) and K (n < length rv)) s\<rbrace>
 3. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. ?P46 s (atcbContextGet (tcbArch tcb))) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> ?P'43 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P46 s\<rbrace> do y <- gets (\<lambda>uc. uc register.R2);
x <- gets (\<lambda>uc. uc register.R3);
xa <- gets (\<lambda>uc. uc register.R4);
ya <- gets (\<lambda>uc. uc register.R5);
return [y, x, xa, ya]
od \<lbrace>\<lambda>a b. b ([register.R2, register.R3, register.R4, register.R5] ! n) = a ! n\<rbrace>
 2. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'43 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. \<forall>x. buffer = Some x \<longrightarrow> ((\<lambda>a. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread a) a) and K (n < length rv)) s\<rbrace>
 3. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. ?P46 s (atcbContextGet (tcbArch tcb))) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> ?P'43 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'43 s\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. \<forall>x. buffer = Some x \<longrightarrow> ((\<lambda>a. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread a) a) and K (n < length rv)) s\<rbrace>
 2. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> ?P'43 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P67 s x\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (TCB_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s \<and> K (n < length rv) s\<rbrace>
 2. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> (\<forall>x. ?P67 s x sa) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P73 s x\<rbrace> mapM getRegister TCB_H.msgRegisters \<lbrace>\<lambda>a b. b (TCB_H.msgRegisters ! n) = a ! n\<rbrace>
 2. \<And>s x. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'72 s x\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv. K (n < length rv)\<rbrace>
 3. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> (\<forall>x. (obj_at' (\<lambda>tcb. ?P73 s x (atcbContextGet (tcbArch tcb))) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> ?P'72 s x sa) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P73 s x\<rbrace> mapM (\<lambda>a. gets (\<lambda>uc. uc a)) [register.R2, register.R3, register.R4, register.R5] \<lbrace>\<lambda>a b. b ([register.R2, register.R3, register.R4, register.R5] ! n) = a ! n\<rbrace>
 2. \<And>s x. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'72 s x\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv. K (n < length rv)\<rbrace>
 3. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> (\<forall>x. (obj_at' (\<lambda>tcb. ?P73 s x (atcbContextGet (tcbArch tcb))) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> ?P'72 s x sa) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P73 s x\<rbrace> do y <- gets (\<lambda>uc. uc register.R2);
x <- gets (\<lambda>uc. uc register.R3);
xa <- gets (\<lambda>uc. uc register.R4);
ya <- gets (\<lambda>uc. uc register.R5);
return [y, x, xa, ya]
od \<lbrace>\<lambda>a b. b ([register.R2, register.R3, register.R4, register.R5] ! n) = a ! n\<rbrace>
 2. \<And>s x. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'72 s x\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv. K (n < length rv)\<rbrace>
 3. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> (\<forall>x. (obj_at' (\<lambda>tcb. ?P73 s x (atcbContextGet (tcbArch tcb))) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> ?P'72 s x sa) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'72 s x\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv. K (n < length rv)\<rbrace>
 2. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> (\<forall>x. (obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> ?P'72 s x sa) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'72 s x\<rbrace> asUser thread (mapM getRegister TCB_H.msgRegisters) \<lbrace>\<lambda>rv s. n < length rv\<rbrace>
 2. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> (\<forall>x. (obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> ?P'72 s x sa) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>n < unat n_msgRegisters; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa \<and> cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> (\<forall>x. (obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa \<and> thread = ksCurThread sa) \<and> n < length TCB_H.msgRegisters) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>n < 4; n < unat (msgLength info); cur_tcb' s; thread = ksCurThread sa; cur_tcb' sa\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa) \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) ([register.R2, register.R3, register.R4, register.R5] ! n) = [atcbContextGet (tcbArch tcb) register.R2, atcbContextGet (tcbArch tcb) register.R3, atcbContextGet (tcbArch tcb) register.R4, atcbContextGet (tcbArch tcb) register.R5] ! n) (ksCurThread sa) sa proof (prove)
goal:
No subgoals!