theory PageTableDuplicates

lemma invokeTCB_valid_duplicates'[wp]:
  "\<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' ti and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
     invokeTCB ti
   \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (case_tac ti, simp_all only:) apply (simp add: invokeTCB_def) apply wp apply (clarsimp simp: invs'_def valid_state'_def
                      dest!: global'_no_ex_cap) apply (simp add: invokeTCB_def) apply wp apply (clarsimp simp: invs'_def valid_state'_def
                     dest!: global'_no_ex_cap) apply (wp tc_valid_duplicates') apply (clarsimp split:option.splits) apply (rename_tac option) apply (case_tac option, simp_all) apply (simp add:invokeTCB_def | wp mapM_x_wp' | intro impI conjI | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' ti and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB ti \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x1. ti = tcbinvocation.Suspend x1 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.Suspend x1) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.Suspend x1) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x2. ti = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.Resume x2) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 8. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x1. ti = tcbinvocation.Suspend x1 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x1 and ex_nonz_cap_to' x1) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- ThreadDecls_H.suspend x1;
return []
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x2. ti = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.Resume x2) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 8. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x1 s. \<lbrakk>ti = tcbinvocation.Suspend x1; (invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x1 and ex_nonz_cap_to' x1) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 2. \<And>x2. ti = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.Resume x2) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 8. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x2. ti = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.Resume x2) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x2. ti = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x2 and ex_nonz_cap_to' x2) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- ThreadDecls_H.restart x2;
return []
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x2 s. \<lbrakk>ti = tcbinvocation.Resume x2; (invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x2 and ex_nonz_cap_to' x2) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 2. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 x38 s. \<lbrakk>ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38; (invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' x31 and ex_nonz_cap_to' x31 and (case x36 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case x36 of None \<Rightarrow> True | Some x \<Rightarrow> (isCNodeCap \<circ> fst) x) and (case x37 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case x37 of None \<Rightarrow> True | Some x \<Rightarrow> (isValidVTableRoot \<circ> fst) x) and (case case x38 of None \<Rightarrow> None | Some x \<Rightarrow> (case_option None (Some \<circ> fst) \<circ> snd) x of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_cap' x) and K (valid_option_prio x35) and K (valid_option_prio x34) and K (case case x38 of None \<Rightarrow> None | Some x \<Rightarrow> (case_option None (Some \<circ> fst) \<circ> snd) x of None \<Rightarrow> True | Some x \<Rightarrow> isArchObjectCap x) and K (case x38 of None \<Rightarrow> True | Some x \<Rightarrow> (swp is_aligned msg_align_bits \<circ> fst) x)) s
 2. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 option. ti = tcbinvocation.NotificationControl x41 option \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 option) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 option) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x41 option. \<lbrakk>ti = tcbinvocation.NotificationControl x41 None; option = None\<rbrakk> \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x41 and ex_nonz_cap_to' x41) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 None) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x41 option a. \<lbrakk>ti = tcbinvocation.NotificationControl x41 (Some a); option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x41 and ex_nonz_cap_to' x41 and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) x41)) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 (Some a)) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x51 and ex_nonz_cap_to' x51) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x61 and ex_nonz_cap_to' x61) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x71 and tcb_at' x72 and ex_nonz_cap_to' x72 and ex_nonz_cap_to' x71) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x81 and ex_nonz_cap_to' x81) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal:
No subgoals!