theory Syscall_R

lemma sts_valid_inv'[wp]:
  "\<lbrace>valid_invocation' i\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_invocation' i\<rbrace>" apply (case_tac i, simp_all add: sts_valid_untyped_inv' sts_valid_arch_inv') apply (wp | simp)+ defer apply (rename_tac cnode_invocation) apply (case_tac cnode_invocation, simp_all add: cte_wp_at_ctes_of) apply (wp | simp)+ apply (rename_tac irqcontrol_invocation) apply (case_tac irqcontrol_invocation, simp_all) apply (rename_tac arch_irqhandler_issue) apply (case_tac arch_irqhandler_issue) apply (wp | simp add: irq_issued'_def)+ apply (rename_tac irqhandler_invocation) apply (case_tac irqhandler_invocation, simp_all) apply (wp hoare_vcg_ex_lift ex_cte_cap_to'_pres | simp)+ apply (rename_tac tcbinvocation) apply (case_tac tcbinvocation,
      simp_all add: setThreadState_tcb',
      auto  intro!: hoare_vcg_conj_lift hoare_vcg_disj_lift
      simp only: imp_conv_disj simp_thms pred_conj_def,
      auto  intro!: hoare_vcg_prop
      sts_cap_to' sts_cte_cap_to'
      setThreadState_typ_ats
      split: option.splits)[1] apply (wp sts_bound_tcb_at' hoare_vcg_all_lift hoare_vcg_const_imp_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_invocation' i\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_invocation' i\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x21 x22 x23 x24. i = Invocations_H.invocation.InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>ep_at' x21 and ex_nonz_cap_to' x21\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ep_at' x21 and ex_nonz_cap_to' x21\<rbrace>
 2. \<And>x31 x32. i = Invocations_H.invocation.InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>ntfn_at' x31 and ex_nonz_cap_to' x31\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ntfn_at' x31 and ex_nonz_cap_to' x31\<rbrace>
 3. \<And>x41 x42 x43. i = Invocations_H.invocation.InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>tcb_at' x41 and cte_wp_at' (\<lambda>cte. \<exists>gr. cteCap cte = capability.ReplyCap x41 False gr) x42\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_at' x41 and cte_wp_at' (\<lambda>cte. \<exists>gr. cteCap cte = capability.ReplyCap x41 False gr) x42\<rbrace>
 4. \<And>x51 x52. i = Invocations_H.invocation.InvokeDomain x51 x52 \<Longrightarrow> \<lbrace>tcb_at' x51 and (\<lambda>y. x52 \<le> maxDomain)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_at' x51 and (\<lambda>y. x52 \<le> maxDomain)\<rbrace>
 5. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace>
 6. \<And>x7. i = Invocations_H.invocation.InvokeCNode x7 \<Longrightarrow> \<lbrace>valid_cnode_inv' x7\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_cnode_inv' x7\<rbrace>
 7. \<And>x8. i = Invocations_H.invocation.InvokeIRQControl x8 \<Longrightarrow> \<lbrace>irq_control_inv_valid' x8\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_control_inv_valid' x8\<rbrace>
 8. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace>
 2. \<And>x7. i = Invocations_H.invocation.InvokeCNode x7 \<Longrightarrow> \<lbrace>valid_cnode_inv' x7\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_cnode_inv' x7\<rbrace>
 3. \<And>x8. i = Invocations_H.invocation.InvokeIRQControl x8 \<Longrightarrow> \<lbrace>irq_control_inv_valid' x8\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_control_inv_valid' x8\<rbrace>
 4. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x7. i = Invocations_H.invocation.InvokeCNode x7 \<Longrightarrow> \<lbrace>valid_cnode_inv' x7\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_cnode_inv' x7\<rbrace>
 2. \<And>x8. i = Invocations_H.invocation.InvokeIRQControl x8 \<Longrightarrow> \<lbrace>irq_control_inv_valid' x8\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_control_inv_valid' x8\<rbrace>
 3. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace>
 4. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cnode_invocation. i = Invocations_H.invocation.InvokeCNode cnode_invocation \<Longrightarrow> \<lbrace>valid_cnode_inv' cnode_invocation\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_cnode_inv' cnode_invocation\<rbrace>
 2. \<And>x8. i = Invocations_H.invocation.InvokeIRQControl x8 \<Longrightarrow> \<lbrace>irq_control_inv_valid' x8\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_control_inv_valid' x8\<rbrace>
 3. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace>
 4. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>cnode_invocation x11 x12 x13. \<lbrakk>i = Invocations_H.invocation.InvokeCNode (Insert x11 x12 x13); cnode_invocation = Insert x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>valid_cap' x11 and (\<lambda>s. \<exists>cte. ctes_of s x12 = Some cte \<and> is_derived' (ctes_of s) x12 x11 (cteCap cte)) and cte_wp_at' (untyped_derived_eq x11 \<circ> cteCap) x12 and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x13 and (\<lambda>s. x12 \<noteq> x13) and ex_cte_cap_wp_to' (\<lambda>_. True) x13\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_cap' x11 and (\<lambda>s. \<exists>cte. ctes_of s x12 = Some cte \<and> is_derived' (ctes_of s) x12 x11 (cteCap cte)) and cte_wp_at' (untyped_derived_eq x11 \<circ> cteCap) x12 and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x13 and (\<lambda>s. x12 \<noteq> x13) and ex_cte_cap_wp_to' (\<lambda>_. True) x13\<rbrace>
 2. \<And>cnode_invocation x21 x22 x23 x24 x25. \<lbrakk>i = Invocations_H.invocation.InvokeCNode (Rotate x21 x22 x23 x24 x25); cnode_invocation = Rotate x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>valid_cap' x21 and valid_cap' x22 and cte_wp_at' (\<lambda>c. weak_derived' x21 (cteCap c)) x23 and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x21) x23 and cte_wp_at' (\<lambda>c. weak_derived' x22 (cteCap c)) x24 and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x22) x24 and (\<lambda>y. x23 \<noteq> x24 \<and> x24 \<noteq> x25 \<and> x21 \<noteq> capability.NullCap \<and> x22 \<noteq> capability.NullCap) and (\<lambda>s. x23 \<noteq> x25 \<longrightarrow> (\<exists>cte. ctes_of s x25 = Some cte \<and> cteCap cte = capability.NullCap)) and (\<lambda>s. ex_cte_cap_wp_to' (\<lambda>_. True) x24 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x25 s)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_cap' x21 and valid_cap' x22 and cte_wp_at' (\<lambda>c. weak_derived' x21 (cteCap c)) x23 and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x21) x23 and cte_wp_at' (\<lambda>c. weak_derived' x22 (cteCap c)) x24 and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x22) x24 and (\<lambda>y. x23 \<noteq> x24 \<and> x24 \<noteq> x25 \<and> x21 \<noteq> capability.NullCap \<and> x22 \<noteq> capability.NullCap) and (\<lambda>s. x23 \<noteq> x25 \<longrightarrow> (\<exists>cte. ctes_of s x25 = Some cte \<and> cteCap cte = capability.NullCap)) and (\<lambda>s. ex_cte_cap_wp_to' (\<lambda>_. True) x24 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x25 s)\<rbrace>
 3. \<And>cnode_invocation x3. \<lbrakk>i = Invocations_H.invocation.InvokeCNode (Revoke x3); cnode_invocation = Revoke x3\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>_. True) x3\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) x3\<rbrace>
 4. \<And>cnode_invocation x41 x42 x43. \<lbrakk>i = Invocations_H.invocation.InvokeCNode (Move x41 x42 x43); cnode_invocation = Move x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. weak_derived' x41 (cteCap c)) x42 and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x41) x42 and cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x42 and valid_cap' x41 and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x43 and ex_cte_cap_wp_to' (\<lambda>_. True) x43\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. weak_derived' x41 (cteCap c)) x42 and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cteCap c = x41) x42 and cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x42 and valid_cap' x41 and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x43 and ex_cte_cap_wp_to' (\<lambda>_. True) x43\<rbrace>
 5. \<And>cnode_invocation x5. \<lbrakk>i = Invocations_H.invocation.InvokeCNode (CancelBadgedSends x5); cnode_invocation = CancelBadgedSends x5\<rbrakk> \<Longrightarrow> \<lbrace>valid_cap' x5 and (\<lambda>y. hasCancelSendRights x5)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_cap' x5 and (\<lambda>y. hasCancelSendRights x5)\<rbrace>
 6. \<And>cnode_invocation x6. \<lbrakk>i = Invocations_H.invocation.InvokeCNode (SaveCaller x6); cnode_invocation = SaveCaller x6\<rbrakk> \<Longrightarrow> \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True) x6 and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' (\<lambda>_. True) x6 and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x6\<rbrace>
 7. \<And>cnode_invocation x7. \<lbrakk>i = Invocations_H.invocation.InvokeCNode (Delete x7); cnode_invocation = Delete x7\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>_. True) x7\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) x7\<rbrace>
 8. \<And>x8. i = Invocations_H.invocation.InvokeIRQControl x8 \<Longrightarrow> \<lbrace>irq_control_inv_valid' x8\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_control_inv_valid' x8\<rbrace>
 9. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace>
 10. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x8. i = Invocations_H.invocation.InvokeIRQControl x8 \<Longrightarrow> \<lbrace>irq_control_inv_valid' x8\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_control_inv_valid' x8\<rbrace>
 2. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace>
 3. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>irqcontrol_invocation. i = Invocations_H.invocation.InvokeIRQControl irqcontrol_invocation \<Longrightarrow> \<lbrace>irq_control_inv_valid' irqcontrol_invocation\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_control_inv_valid' irqcontrol_invocation\<rbrace>
 2. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace>
 3. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>irqcontrol_invocation x1. \<lbrakk>i = Invocations_H.invocation.InvokeIRQControl (irqcontrol_invocation.ArchIRQControl x1); irqcontrol_invocation = irqcontrol_invocation.ArchIRQControl x1\<rbrakk> \<Longrightarrow> \<lbrace>arch_irq_control_inv_valid' x1\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. arch_irq_control_inv_valid' x1\<rbrace>
 2. \<And>irqcontrol_invocation x21 x22 x23. \<lbrakk>i = Invocations_H.invocation.InvokeIRQControl (Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23); irqcontrol_invocation = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x22 and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) x23 and ex_cte_cap_wp_to' (\<lambda>_. True) x22 and real_cte_at' x22 and Not \<circ> irq_issued' x21 and (\<lambda>y. x21 \<le> maxIRQ)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x22 and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) x23 and ex_cte_cap_wp_to' (\<lambda>_. True) x22 and real_cte_at' x22 and Not \<circ> irq_issued' x21 and (\<lambda>y. x21 \<le> maxIRQ)\<rbrace>
 3. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace>
 4. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>irqcontrol_invocation arch_irqhandler_issue. \<lbrakk>i = Invocations_H.invocation.InvokeIRQControl (irqcontrol_invocation.ArchIRQControl arch_irqhandler_issue); irqcontrol_invocation = irqcontrol_invocation.ArchIRQControl arch_irqhandler_issue\<rbrakk> \<Longrightarrow> \<lbrace>arch_irq_control_inv_valid' arch_irqhandler_issue\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. arch_irq_control_inv_valid' arch_irqhandler_issue\<rbrace>
 2. \<And>irqcontrol_invocation x21 x22 x23. \<lbrakk>i = Invocations_H.invocation.InvokeIRQControl (Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23); irqcontrol_invocation = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x22 and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) x23 and ex_cte_cap_wp_to' (\<lambda>_. True) x22 and real_cte_at' x22 and Not \<circ> irq_issued' x21 and (\<lambda>y. x21 \<le> maxIRQ)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x22 and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) x23 and ex_cte_cap_wp_to' (\<lambda>_. True) x22 and real_cte_at' x22 and Not \<circ> irq_issued' x21 and (\<lambda>y. x21 \<le> maxIRQ)\<rbrace>
 3. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace>
 4. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>irqcontrol_invocation arch_irqhandler_issue x1 x2 x3 x4. \<lbrakk>i = Invocations_H.invocation.InvokeIRQControl (irqcontrol_invocation.ArchIRQControl arch_irqhandler_issue); irqcontrol_invocation = irqcontrol_invocation.ArchIRQControl arch_irqhandler_issue; arch_irqhandler_issue = local.irqcontrol_invocation.IssueIRQHandler x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>arch_irq_control_inv_valid' arch_irqhandler_issue\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. arch_irq_control_inv_valid' arch_irqhandler_issue\<rbrace>
 2. \<And>irqcontrol_invocation x21 x22 x23. \<lbrakk>i = Invocations_H.invocation.InvokeIRQControl (Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23); irqcontrol_invocation = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x22 and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) x23 and ex_cte_cap_wp_to' (\<lambda>_. True) x22 and real_cte_at' x22 and Not \<circ> irq_issued' x21 and (\<lambda>y. x21 \<le> maxIRQ)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x22 and cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQControlCap) x23 and ex_cte_cap_wp_to' (\<lambda>_. True) x22 and real_cte_at' x22 and Not \<circ> irq_issued' x21 and (\<lambda>y. x21 \<le> maxIRQ)\<rbrace>
 3. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace>
 4. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>irq_handler_inv_valid' x9\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' x9\<rbrace>
 2. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>irqhandler_invocation. i = Invocations_H.invocation.InvokeIRQHandler irqhandler_invocation \<Longrightarrow> \<lbrace>irq_handler_inv_valid' irqhandler_invocation\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. irq_handler_inv_valid' irqhandler_invocation\<rbrace>
 2. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>irqhandler_invocation x1. \<lbrakk>i = Invocations_H.invocation.InvokeIRQHandler (AckIRQ x1); irqhandler_invocation = AckIRQ x1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. intStateIRQTable (ksInterruptState s) x1 \<noteq> irqstate.IRQInactive\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) x1 \<noteq> irqstate.IRQInactive\<rbrace>
 2. \<And>irqhandler_invocation x2. \<lbrakk>i = Invocations_H.invocation.InvokeIRQHandler (irqhandler_invocation.ClearIRQHandler x2); irqhandler_invocation = irqhandler_invocation.ClearIRQHandler x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> setThreadState st t \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>irqhandler_invocation x31 x32 x33. \<lbrakk>i = Invocations_H.invocation.InvokeIRQHandler (irqhandler_invocation.SetIRQHandler x31 x32 x33); irqhandler_invocation = irqhandler_invocation.SetIRQHandler x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>valid_cap' x32 and valid_cap' (capability.IRQHandlerCap x31) and (\<lambda>y. isNotificationCap x32) and cte_wp_at' (badge_derived' x32 \<circ> cteCap) x33 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap x31) ptr' s) and ex_cte_cap_wp_to' isCNodeCap x33\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_cap' x32 and valid_cap' (capability.IRQHandlerCap x31) and (\<lambda>y. isNotificationCap x32) and cte_wp_at' (badge_derived' x32 \<circ> cteCap) x33 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap x31) ptr' s) and ex_cte_cap_wp_to' isCNodeCap x33\<rbrace>
 4. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>tcb_inv_wf' x6\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' x6\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tcbinvocation. i = Invocations_H.invocation.InvokeTCB tcbinvocation \<Longrightarrow> \<lbrace>tcb_inv_wf' tcbinvocation\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. tcb_inv_wf' tcbinvocation\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 x38. i = Invocations_H.invocation.InvokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>a b. x35 = Some (a, b) \<longrightarrow> mcpriority_tcb_at' ((\<le>) a) b s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. \<forall>a b. x35 = Some (a, b) \<longrightarrow> mcpriority_tcb_at' ((\<le>) a) b s\<rbrace>
 2. \<And>x31 x32 x33 x34 x35 x36 x37 x38. i = Invocations_H.invocation.InvokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>a b. x34 = Some (a, b) \<longrightarrow> mcpriority_tcb_at' ((\<le>) a) b s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. \<forall>a b. x34 = Some (a, b) \<longrightarrow> mcpriority_tcb_at' ((\<le>) a) b s\<rbrace>
 3. \<And>x41 x2. i = Invocations_H.invocation.InvokeTCB (tcbinvocation.NotificationControl x41 (Some x2)) \<Longrightarrow> \<lbrace>\<lambda>x. obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) x2 x \<and> ex_nonz_cap_to' x2 x \<and> bound_tcb_at' ((=) None) x41 x\<rbrace> setThreadState st t \<lbrace>\<lambda>rv x. obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) x2 x \<and> ex_nonz_cap_to' x2 x \<and> bound_tcb_at' ((=) None) x41 x\<rbrace> proof (prove)
goal:
No subgoals!