diff --git a/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy b/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy
index d395eff2e..72473b0e0 100644
--- a/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy
+++ b/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy
@@ -100,8 +100,9 @@ lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (d
   done
 
 crunch (bcorres)bcorres[wp]:
-  decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_set_mcpriority,
-  decode_set_sched_params,decode_bind_notification,decode_unbind_notification truncate_state
+  decode_set_ipc_buffer, decode_set_space, decode_set_priority,
+  decode_set_mcpriority, decode_set_sched_params, decode_bind_notification,
+  decode_unbind_notification, decode_set_tls_base truncate_state
 
 lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
      (decode_tcb_configure b (cap.ThreadCap c) d e)"
diff --git a/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy b/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy
index 4af57df6d..e437926aa 100644
--- a/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy
+++ b/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy
@@ -43,8 +43,10 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
          bool.splits list.splits thread_state.splits split_def catch_def sum.splits
          Let_def wp: zipWithM_x_empty_fail)
 
-crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
-  decode_set_priority, decode_set_mcpriority, decode_set_sched_params
+crunch (empty_fail) empty_fail[wp]:
+  decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
+  decode_set_priority, decode_set_mcpriority, decode_set_sched_params,
+  decode_set_tls_base
   (simp: cap.splits arch_cap.splits split_def)
 
 lemma decode_tcb_invocation_empty_fail[wp]:
diff --git a/proof/invariant-abstract/ARM_HYP/ArchBCorres2_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchBCorres2_AI.thy
index cbac8600d..2c9ea1473 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchBCorres2_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchBCorres2_AI.thy
@@ -103,8 +103,9 @@ lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (d
   done
 
 crunch (bcorres)bcorres[wp]:
-  decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_set_mcpriority,
-  decode_set_sched_params,decode_bind_notification,decode_unbind_notification truncate_state
+  decode_set_ipc_buffer, decode_set_space, decode_set_priority,
+  decode_set_mcpriority, decode_set_sched_params, decode_bind_notification,
+  decode_unbind_notification, decode_set_tls_base truncate_state
 
 lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
      (decode_tcb_configure b (cap.ThreadCap c) d e)"
diff --git a/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy
index 02d123a98..bfe22d2aa 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy
@@ -43,8 +43,10 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
          bool.splits list.splits thread_state.splits split_def catch_def sum.splits
          Let_def wp: zipWithM_x_empty_fail empty_fail_addressTranslateS1CPR)
 
-crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
-  decode_set_priority, decode_set_mcpriority, decode_set_sched_params
+crunch (empty_fail) empty_fail[wp]:
+  decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
+  decode_set_priority, decode_set_mcpriority, decode_set_sched_params,
+  decode_set_tls_base
   (simp: cap.splits arch_cap.splits split_def)
 
 crunch (empty_fail) empty_fail[wp]: decode_vcpu_invocation
diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy
index 6bdc4f37f..cd9e2146d 100644
--- a/proof/invariant-abstract/DetSchedSchedule_AI.thy
+++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy
@@ -1922,12 +1922,18 @@ crunch it[wp]: suspend "\<lambda> s. P (idle_thread s)"
 
 context DetSchedSchedule_AI begin
 lemma invoke_tcb_valid_sched[wp]:
-  "\<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf ti\<rbrace> invoke_tcb ti \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
+  "\<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf ti\<rbrace>
+     invoke_tcb ti
+   \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
   apply (cases ti, simp_all only:)
-        apply (wp mapM_x_wp | simp | rule subset_refl | rule reschedule_preserves_valid_shed | clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap | intro impI conjI)+
-   apply (rename_tac option)
-   apply (case_tac option)
-    apply (wp mapM_x_wp | simp | rule subset_refl | clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap | intro impI conjI)+
+        apply (wp mapM_x_wp | simp | rule subset_refl | rule reschedule_preserves_valid_shed |
+               clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap |
+               intro impI conjI)+
+    apply (rename_tac option)
+    apply (case_tac option)
+     apply (wp mapM_x_wp | simp | rule subset_refl |
+            clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap |
+            rule reschedule_preserves_valid_shed | intro impI conjI)+
   done
 end
 
diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy
index db2124700..438b8f3ba 100644
--- a/proof/invariant-abstract/Tcb_AI.thy
+++ b/proof/invariant-abstract/Tcb_AI.thy
@@ -771,6 +771,7 @@ where
                                                 \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfnptr
                                           and ex_nonz_cap_to ntfnptr
                                           and bound_tcb_at (op = None) t) ))"
+| "tcb_inv_wf (SetTLSBase t tls_base) = (tcb_at t and ex_nonz_cap_to t)"
 
 end
 
@@ -835,18 +836,19 @@ lemma (in Tcb_AI) tcbinv_invs:
      invoke_tcb ti
    \<lbrace>\<lambda>rv. invs\<rbrace>"
   apply (case_tac ti, simp_all only:)
-        apply ((wp writereg_invs readreg_invs copyreg_invs tc_invs
-             | simp
-             | clarsimp simp: invs_def valid_state_def valid_pspace_def
-                       dest!: idle_no_ex_cap
-                       split: option.split
-             | rule conjI)+)[6]
-  apply (rename_tac option)
-  apply (case_tac option, simp_all)
-   apply (rule hoare_pre)
-    apply ((wp unbind_notification_invs get_simple_ko_wp | simp)+)[2]
-  apply (wp bind_notification_invs)
-  apply clarsimp
+         apply ((wp writereg_invs readreg_invs copyreg_invs tc_invs
+              | simp
+              | clarsimp simp: invs_def valid_state_def valid_pspace_def
+                        dest!: idle_no_ex_cap
+                        split: option.split
+              | rule conjI)+)[6]
+   apply (rename_tac option)
+   apply (case_tac option, simp_all)
+    apply (rule hoare_pre)
+     apply ((wp unbind_notification_invs get_simple_ko_wp | simp)+)[2]
+   apply (wp bind_notification_invs)
+   apply clarsimp
+  apply wpsimp
   done
 
 lemma inj_ucast: "\<lbrakk> uc = ucast; is_up uc \<rbrakk> \<Longrightarrow> inj uc"
@@ -868,23 +870,31 @@ lemma decode_readreg_inv:
   "\<lbrace>P\<rbrace> decode_read_registers args (cap.ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace>"
   apply (rule hoare_pre)
    apply (simp add: decode_read_registers_def whenE_def | rule conjI | clarsimp
-            | wp_once | wpcw)+
+          | wp_once | wpcw)+
   done
 
 lemma decode_writereg_inv:
   "\<lbrace>P\<rbrace> decode_write_registers args (cap.ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace>"
   apply (rule hoare_pre)
-   apply (simp add: decode_write_registers_def whenE_def
-                          split del: if_split
-            | wp_once | wpcw)+
+   apply (simp   add: decode_write_registers_def whenE_def
+           split del: if_split
+          | wp_once | wpcw)+
   done
 
 lemma decode_copyreg_inv:
   "\<lbrace>P\<rbrace> decode_copy_registers args (cap.ThreadCap t) extras \<lbrace>\<lambda>rv. P\<rbrace>"
   apply (rule hoare_pre)
-   apply (simp add: decode_copy_registers_def whenE_def
-                          split del: if_split
-            | wp_once | wpcw)+
+   apply (simp   add: decode_copy_registers_def whenE_def
+           split del: if_split
+          | wp_once | wpcw)+
+  done
+
+lemma decode_set_tls_base_inv:
+  "\<lbrace>P\<rbrace> decode_set_tls_base args (cap.ThreadCap t) \<lbrace>\<lambda>rv. P\<rbrace>"
+  apply (rule hoare_pre)
+   apply (simp   add: decode_set_tls_base_def whenE_def
+           split del: if_split
+          | wp_once | wpcw)+
   done
 
 lemma (in Tcb_AI) decode_readreg_wf:
@@ -922,6 +932,15 @@ lemma (in Tcb_AI) decode_copyreg_wf:
   apply (clarsimp simp: valid_cap_def[where c="cap.ThreadCap t" for t])
   done
 
+lemma (in Tcb_AI) decode_set_tls_base_wf:
+  "\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
+     decode_set_tls_base args (cap.ThreadCap t)
+   \<lbrace>tcb_inv_wf\<rbrace>,-"
+  apply (simp add: decode_set_tls_base_def whenE_def
+             cong: list.case_cong split del: if_split)
+  apply wpsimp
+  done
+
 declare alternativeE_wp[wp]
 declare alternativeE_R_wp[wp]
 
@@ -1201,18 +1220,20 @@ lemma decode_bind_notification_inv[wp]:
              split_del: if_split)
 
 lemma (in Tcb_AI) decode_tcb_inv_inv:
-  "\<lbrace>P::'state_ext state \<Rightarrow> bool\<rbrace> decode_tcb_invocation label args (cap.ThreadCap t) slot extras \<lbrace>\<lambda>rv. P\<rbrace>"
-  apply (simp add: decode_tcb_invocation_def Let_def
+  "\<lbrace>P::'state_ext state \<Rightarrow> bool\<rbrace>
+     decode_tcb_invocation label args (cap.ThreadCap t) slot extras
+   \<lbrace>\<lambda>rv. P\<rbrace>"
+  apply (simp add: decode_tcb_invocation_def Let_def decode_set_tls_base_def
              cong: if_cong
         split del: if_split)
   apply (rule hoare_pre)
    apply (wpc
         | wp decode_readreg_inv decode_writereg_inv
-             decode_copyreg_inv decode_tcb_conf_inv)+
+             decode_copyreg_inv decode_tcb_conf_inv
+             decode_set_tls_base_inv)+
   apply simp
   done
 
-
 lemma real_cte_at_not_tcb_at:
   "real_cte_at (x, y) s \<Longrightarrow> \<not> tcb_at x s"
   by (clarsimp simp: obj_at_def is_tcb is_cap_table)
@@ -1258,7 +1279,8 @@ lemma decode_tcb_inv_wf:
    apply wpc
    apply (wp decode_tcb_conf_wf decode_readreg_wf
              decode_writereg_wf decode_copyreg_wf
-             decode_bind_notification_wf decode_unbind_notification_wf decode_set_priority_wf)+
+             decode_bind_notification_wf decode_unbind_notification_wf
+             decode_set_priority_wf decode_set_tls_base_wf)+
   apply (clarsimp simp: real_cte_at_cte)
   apply (fastforce simp: real_cte_at_not_tcb_at)
   done
diff --git a/proof/invariant-abstract/X64/ArchBCorres2_AI.thy b/proof/invariant-abstract/X64/ArchBCorres2_AI.thy
index c22ff1d0e..24d17d08f 100644
--- a/proof/invariant-abstract/X64/ArchBCorres2_AI.thy
+++ b/proof/invariant-abstract/X64/ArchBCorres2_AI.thy
@@ -101,7 +101,10 @@ lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (d
   apply (wp | wpc | simp add: split_def | intro impI conjI)+
   done
 
-crunch (bcorres)bcorres[wp]: decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_set_mcpriority,decode_set_sched_params,decode_bind_notification,decode_unbind_notification truncate_state
+crunch (bcorres)bcorres[wp]:
+  decode_set_ipc_buffer, decode_set_space, decode_set_priority,
+  decode_set_mcpriority, decode_set_sched_params, decode_bind_notification,
+  decode_unbind_notification, decode_set_tls_base truncate_state
 
 lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
      (decode_tcb_configure b (cap.ThreadCap c) d e)"
diff --git a/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy b/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy
index 2e8025717..c002c1945 100644
--- a/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy
+++ b/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy
@@ -51,8 +51,10 @@ lemma port_in_empty_fail[simp, intro!]:
   apply (simp add: port_in_def)
   by (wp | simp add: ef)+
 
-crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
-  decode_set_priority, decode_set_mcpriority, decode_set_sched_params
+crunch (empty_fail) empty_fail[wp]:
+  decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
+  decode_set_priority, decode_set_mcpriority, decode_set_sched_params,
+  decode_set_tls_base
   (simp: cap.splits arch_cap.splits split_def)
 
 lemma decode_tcb_invocation_empty_fail[wp]:
diff --git a/proof/refine/ARM/Orphanage.thy b/proof/refine/ARM/Orphanage.thy
index c78b477d6..55d3d02db 100644
--- a/proof/refine/ARM/Orphanage.thy
+++ b/proof/refine/ARM/Orphanage.thy
@@ -1970,6 +1970,16 @@ lemma copyreg_no_orphans:
   apply (fastforce simp: invs'_def valid_state'_def dest!: global'_no_ex_cap)
   done
 
+lemma settlsbase_no_orphans:
+  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
+     invokeTCB (tcbinvocation.SetTLSBase src dest)
+   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
+  unfolding invokeTCB_def performTransfer_def
+  apply simp
+  apply (wp hoare_vcg_if_lift static_imp_wp)
+   apply (wpsimp wp: hoare_vcg_imp_lift' mapM_x_wp' asUser_no_orphans)+
+  done
+
 lemma almost_no_orphans_no_orphans:
   "\<lbrakk> almost_no_orphans t s; \<not> is_active_tcb_ptr t s \<rbrakk> \<Longrightarrow> no_orphans s"
   by (auto simp: almost_no_orphans_def no_orphans_def all_active_tcb_ptrs_def)
@@ -2072,7 +2082,7 @@ lemma invokeTCB_no_orphans [wp]:
      apply (rename_tac option)
      apply (case_tac option)
       apply ((wp | simp add: invokeTCB_def)+)[2]
-    apply (wp writereg_no_orphans readreg_no_orphans copyreg_no_orphans | clarsimp)+
+    apply (wp writereg_no_orphans readreg_no_orphans copyreg_no_orphans settlsbase_no_orphans | clarsimp)+
   done
 
 lemma invokeCNode_no_orphans [wp]:
diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy
index 5bf0accab..e2c0b506b 100644
--- a/proof/refine/ARM/Tcb_R.thy
+++ b/proof/refine/ARM/Tcb_R.thy
@@ -1607,6 +1607,8 @@ where
     = (x = tcbinvocation.Resume a)"
 | "tcbinv_relation (tcb_invocation.NotificationControl t ntfnptr) x
     = (x = tcbinvocation.NotificationControl t ntfnptr)"
+| "tcbinv_relation (tcb_invocation.SetTLSBase ref w) x
+    = (x = tcbinvocation.SetTLSBase ref w)"
 
 primrec
   tcb_inv_wf' :: "tcbinvocation \<Rightarrow> kernel_state \<Rightarrow> bool"
@@ -1644,6 +1646,8 @@ where
                                            \<and> (\<forall>q. ntfnObj ko \<noteq> WaitingNtfn q)) ntfnptr
                                           and ex_nonz_cap_to' ntfnptr
                                           and bound_tcb_at' (op = None) t) )"
+| "tcb_inv_wf' (tcbinvocation.SetTLSBase ref w)
+             = (tcb_at' ref and ex_nonz_cap_to' ref)"
 
 lemma tcbinv_corres:
  "tcbinv_relation ti ti' \<Longrightarrow>
@@ -1652,42 +1656,53 @@ lemma tcbinv_corres:
          (invs' and sch_act_simple and tcb_inv_wf' ti')
          (invoke_tcb ti) (invokeTCB ti')"
   apply (case_tac ti, simp_all only: tcbinv_relation.simps valid_tcb_invocation_def)
-        apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
-       apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
-      apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
-     apply (clarsimp simp del: invoke_tcb.simps)
-     apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
-     apply (rule_tac F="is_aligned word 5" in corres_req)
-      apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
-     apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
-      apply (clarsimp simp: is_cnode_or_valid_arch_def
-                     split: option.split option.split_asm)
-     apply clarsimp
-     apply (auto split: option.split_asm simp: newroot_rel_def)[1]
+         apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
+        apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
+       apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
+      apply (clarsimp simp del: invoke_tcb.simps)
+      apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
+      apply (rule_tac F="is_aligned word 5" in corres_req)
+       apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
+      apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
+       apply (clarsimp simp: is_cnode_or_valid_arch_def
+                      split: option.split option.split_asm)
+      apply clarsimp
+      apply (auto split: option.split_asm simp: newroot_rel_def)[1]
+     apply (simp add: invokeTCB_def liftM_def[symmetric]
+                      o_def dc_def[symmetric])
+     apply (rule corres_guard_imp [OF suspend_corres], simp+)
     apply (simp add: invokeTCB_def liftM_def[symmetric]
                      o_def dc_def[symmetric])
-    apply (rule corres_guard_imp [OF suspend_corres], simp+)
-   apply (simp add: invokeTCB_def liftM_def[symmetric]
-                    o_def dc_def[symmetric])
-   apply (rule corres_guard_imp [OF restart_corres], simp+)
-  apply (simp add:invokeTCB_def)
-  apply (rename_tac option)
-  apply (case_tac option)
+    apply (rule corres_guard_imp [OF restart_corres], simp+)
+   apply (simp add:invokeTCB_def)
+   apply (rename_tac option)
+   apply (case_tac option)
+    apply simp
+    apply (rule corres_guard_imp)
+      apply (rule corres_split[OF _ unbind_notification_corres])
+        apply (rule corres_trivial, simp)
+       apply wp+
+     apply (clarsimp)
+    apply clarsimp
    apply simp
    apply (rule corres_guard_imp)
-     apply (rule corres_split[OF _ unbind_notification_corres])
+     apply (rule corres_split[OF _ bind_notification_corres])
        apply (rule corres_trivial, simp)
       apply wp+
-    apply (clarsimp)
-   apply clarsimp
-  apply simp
+    apply clarsimp
+    apply (clarsimp simp: obj_at_def is_ntfn)
+   apply (clarsimp simp: obj_at'_def projectKOs)
+  apply (simp add: invokeTCB_def tlsBaseRegister_def)
   apply (rule corres_guard_imp)
-    apply (rule corres_split[OF _ bind_notification_corres])
-      apply (rule corres_trivial, simp)
-     apply wp+
-   apply clarsimp
-   apply (clarsimp simp: obj_at_def is_ntfn)
-  apply (clarsimp simp: obj_at'_def projectKOs)
+    apply (rule corres_split[OF _ TcbAcc_R.user_setreg_corres])
+      apply (rule corres_split[OF _ Bits_R.gct_corres])
+        apply (rule corres_split[OF _ Corres_UL.corres_when])
+            apply (rule corres_trivial, simp)
+           apply simp
+          apply (rule TcbAcc_R.rescheduleRequired_corres)
+         apply (wpsimp wp: hoare_drop_imp)+
+   apply (clarsimp simp: valid_sched_weak_strg einvs_valid_etcbs)
+  apply (clarsimp simp: Tcb_R.invs_valid_queues' Invariants_H.invs_queues)
   done
 
 lemma tcbBoundNotification_caps_safe[simp]:
@@ -1770,22 +1785,29 @@ lemma tcbntfn_invs':
    apply (wp unbindNotification_invs bindNotification_invs' | simp)+
   done
 
+lemma setTLSBase_invs'[wp]:
+  "\<lbrace>invs' and tcb_inv_wf' (tcbinvocation.SetTLSBase tcb tls_base)\<rbrace>
+       invokeTCB (tcbinvocation.SetTLSBase tcb tls_base)
+   \<lbrace>\<lambda>rv. invs'\<rbrace>"
+  by (wpsimp simp: invokeTCB_def)
+
 lemma tcbinv_invs':
   "\<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' ti\<rbrace>
      invokeTCB ti
    \<lbrace>\<lambda>rv. invs'\<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 (wp restart_invs')
         apply (clarsimp simp: invs'_def valid_state'_def
-                       dest!: global'_no_ex_cap)
-       apply (simp add: invokeTCB_def)
-       apply (wp restart_invs')
-       apply (clarsimp simp: invs'_def valid_state'_def
-                      dest!: global'_no_ex_cap)
-      apply (wp tc_invs')
-      apply (clarsimp split: option.split dest!: isCapDs)
-     apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs' | simp)+
+                        dest!: global'_no_ex_cap)
+       apply (wp tc_invs')
+       apply (clarsimp split: option.split dest!: isCapDs)
+      apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs'
+             | simp)+
   done
 
 crunch_ignore (add: setNextPC getRestartPC)
@@ -2577,6 +2599,14 @@ lemma decode_unbind_notification_corres:
    apply auto
   done
 
+lemma decode_set_tls_base_corres:
+  "corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t)
+          (decode_set_tls_base w (cap.ThreadCap t))
+          (decodeSetTLSBase w (capability.ThreadCap t))"
+  apply (clarsimp simp: decode_set_tls_base_def decodeSetTLSBase_def returnOk_def
+                 split: list.split)
+  by (rule sym, rule ucast_id)
+
 lemma decode_tcb_inv_corres:
  "\<lbrakk> c = Structures_A.ThreadCap t; cap_relation c c';
       list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras';
@@ -2603,7 +2633,8 @@ lemma decode_tcb_inv_corres:
              corres_guard_imp[OF decode_set_ipc_corres]
              corres_guard_imp[OF decode_set_space_corres]
              corres_guard_imp[OF decode_bind_notification_corres]
-             corres_guard_imp[OF decode_unbind_notification_corres],
+             corres_guard_imp[OF decode_unbind_notification_corres]
+             corres_guard_imp[OF decode_set_tls_base_corres],
          simp_all add: valid_cap_simps valid_cap_simps' invs_def valid_sched_def)
   apply (auto simp: list_all2_map1 list_all2_map2
              elim!: list_all2_mono)
@@ -2645,6 +2676,14 @@ lemma decodeUnbindNotification_wf:
   apply (auto simp: obj_at'_def pred_tcb_at'_def)
   done
 
+lemma decodeSetTLSBase_wf:
+  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace>
+     decodeSetTLSBase w (capability.ThreadCap t)
+   \<lbrace>tcb_inv_wf'\<rbrace>,-"
+  apply (simp add: decodeSetTLSBase_def
+             cong: list.case_cong)
+  by wpsimp
+
 lemma decodeTCBInv_wf:
   "\<lbrace>invs' and tcb_at' t and cte_at' slot and ex_nonz_cap_to' t
          and (\<lambda>s. \<forall>x \<in> set extras. real_cte_at' (snd x) s
@@ -2654,7 +2693,7 @@ lemma decodeTCBInv_wf:
   apply (simp add: decodeTCBInvocation_def Let_def
               cong: if_cong invocation_label.case_cong split del: if_split)
   apply (rule hoare_pre)
-   apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf
+   apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf decodeSetTLSBase_wf
              decodeCopyReg_wf decodeBindNotification_wf decodeUnbindNotification_wf)+)
   apply (clarsimp simp: real_cte_at')
   apply (fastforce simp: real_cte_at_not_tcb_at' objBits_defs)
@@ -2711,6 +2750,7 @@ lemma invokeTCB_makes_simple':
         apply ((wp restart_makes_simple' suspend_makes_simple'
                   mapM_x_wp'
                      | simp cong: if_cong)+)[5]
+    apply (wpsimp split: if_split)
    apply (rule hoare_pre)
     apply ((simp split del: if_split
              | wp cteDelete_makes_simple' checkCap_inv [where P="st_tcb_at' simple' t"]
diff --git a/proof/refine/ARM_HYP/Tcb_R.thy b/proof/refine/ARM_HYP/Tcb_R.thy
index 7007736c2..01c3eaa7a 100644
--- a/proof/refine/ARM_HYP/Tcb_R.thy
+++ b/proof/refine/ARM_HYP/Tcb_R.thy
@@ -1598,6 +1598,8 @@ where
     = (x = tcbinvocation.Resume a)"
 | "tcbinv_relation (tcb_invocation.NotificationControl t ntfnptr) x
     = (x = tcbinvocation.NotificationControl t ntfnptr)"
+| "tcbinv_relation (tcb_invocation.SetTLSBase ref w) x
+    = (x = tcbinvocation.SetTLSBase ref w)"
 
 primrec
   tcb_inv_wf' :: "tcbinvocation \<Rightarrow> kernel_state \<Rightarrow> bool"
@@ -1635,6 +1637,8 @@ where
                                            \<and> (\<forall>q. ntfnObj ko \<noteq> WaitingNtfn q)) ntfnptr
                                           and ex_nonz_cap_to' ntfnptr
                                           and bound_tcb_at' (op = None) t) )"
+| "tcb_inv_wf' (tcbinvocation.SetTLSBase ref w)
+             = (tcb_at' ref and ex_nonz_cap_to' ref)"
 
 lemma tcbinv_corres:
  "tcbinv_relation ti ti' \<Longrightarrow>
@@ -1643,43 +1647,54 @@ lemma tcbinv_corres:
          (invs' and sch_act_simple and tcb_inv_wf' ti')
          (invoke_tcb ti) (invokeTCB ti')"
   apply (case_tac ti, simp_all only: tcbinv_relation.simps valid_tcb_invocation_def)
-        apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
-       apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
-      apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
-     apply (clarsimp simp del: invoke_tcb.simps)
-     apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
-     apply (rule_tac F="is_aligned word 5" in corres_req)
-      apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
-     apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
-      subgoal
-      by (clarsimp simp: is_cnode_or_valid_arch_def
-                  split: option.split option.split_asm)
-     apply clarsimp
-     apply (auto split: option.split_asm simp: newroot_rel_def)[1]
+         apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
+        apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
+       apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
+      apply (clarsimp simp del: invoke_tcb.simps)
+      apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
+      apply (rule_tac F="is_aligned word 5" in corres_req)
+       apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
+      apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
+       subgoal
+       by (clarsimp simp: is_cnode_or_valid_arch_def
+                   split: option.split option.split_asm)
+      apply clarsimp
+      apply (auto split: option.split_asm simp: newroot_rel_def)[1]
+     apply (simp add: invokeTCB_def liftM_def[symmetric]
+                      o_def dc_def[symmetric])
+     apply (rule corres_guard_imp [OF suspend_corres], simp+)
     apply (simp add: invokeTCB_def liftM_def[symmetric]
                      o_def dc_def[symmetric])
-    apply (rule corres_guard_imp [OF suspend_corres], simp+)
-   apply (simp add: invokeTCB_def liftM_def[symmetric]
-                    o_def dc_def[symmetric])
-   apply (rule corres_guard_imp [OF restart_corres], simp+)
-  apply (simp add:invokeTCB_def)
-  apply (rename_tac option)
-  apply (case_tac option)
+    apply (rule corres_guard_imp [OF restart_corres], simp+)
+   apply (simp add: invokeTCB_def)
+   apply (rename_tac option)
+   apply (case_tac option)
+    apply simp
+    apply (rule corres_guard_imp)
+      apply (rule corres_split[OF _ unbind_notification_corres])
+        apply (rule corres_trivial, simp)
+       apply wp+
+     apply clarsimp
+    apply clarsimp
    apply simp
    apply (rule corres_guard_imp)
-     apply (rule corres_split[OF _ unbind_notification_corres])
+     apply (rule corres_split[OF _ bind_notification_corres])
        apply (rule corres_trivial, simp)
       apply wp+
-    apply (clarsimp)
-   apply clarsimp
-  apply simp
+    apply clarsimp
+    apply (clarsimp simp: obj_at_def is_ntfn)
+   apply (clarsimp simp: obj_at'_def projectKOs)
+  apply (simp add: invokeTCB_def tlsBaseRegister_def)
   apply (rule corres_guard_imp)
-    apply (rule corres_split[OF _ bind_notification_corres])
-      apply (rule corres_trivial, simp)
-     apply wp+
-   apply clarsimp
-   apply (clarsimp simp: obj_at_def is_ntfn)
-  apply (clarsimp simp: obj_at'_def projectKOs)
+    apply (rule corres_split[OF _ TcbAcc_R.user_setreg_corres])
+      apply (rule corres_split[OF _ Bits_R.gct_corres])
+        apply (rule corres_split[OF _ Corres_UL.corres_when])
+            apply (rule corres_trivial, simp)
+           apply simp
+          apply (rule TcbAcc_R.rescheduleRequired_corres)
+         apply (wpsimp wp: hoare_drop_imp)+
+   apply (clarsimp simp: valid_sched_weak_strg einvs_valid_etcbs)
+  apply (clarsimp simp: Tcb_R.invs_valid_queues' Invariants_H.invs_queues)
   done
 
 lemma tcbBoundNotification_caps_safe[simp]:
@@ -1762,22 +1777,29 @@ lemma tcbntfn_invs':
    apply (wp unbindNotification_invs bindNotification_invs' | simp)+
   done
 
+lemma setTLSBase_invs'[wp]:
+  "\<lbrace>invs' and tcb_inv_wf' (tcbinvocation.SetTLSBase tcb tls_base)\<rbrace>
+       invokeTCB (tcbinvocation.SetTLSBase tcb tls_base)
+   \<lbrace>\<lambda>rv. invs'\<rbrace>"
+  by (wpsimp simp: invokeTCB_def)
+
 lemma tcbinv_invs':
   "\<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' ti\<rbrace>
      invokeTCB ti
    \<lbrace>\<lambda>rv. invs'\<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 (wp restart_invs')
         apply (clarsimp simp: invs'_def valid_state'_def
-                       dest!: global'_no_ex_cap)
-       apply (simp add: invokeTCB_def)
-       apply (wp restart_invs')
-       apply (clarsimp simp: invs'_def valid_state'_def
-                      dest!: global'_no_ex_cap)
-      apply (wp tc_invs')
-      apply (clarsimp split: option.split dest!: isCapDs)
-     apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs' | simp)+
+                        dest!: global'_no_ex_cap)
+       apply (wp tc_invs')
+       apply (clarsimp split: option.split dest!: isCapDs)
+      apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs'
+             | simp)+
   done
 
 crunch_ignore (add: setNextPC getRestartPC)
@@ -2569,6 +2591,14 @@ lemma decode_unbind_notification_corres:
    apply auto
   done
 
+lemma decode_set_tls_base_corres:
+  "corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t)
+          (decode_set_tls_base w (cap.ThreadCap t))
+          (decodeSetTLSBase w (capability.ThreadCap t))"
+  apply (clarsimp simp: decode_set_tls_base_def decodeSetTLSBase_def returnOk_def
+                 split: list.split)
+  by (rule sym, rule ucast_id)
+
 lemma decode_tcb_inv_corres:
  "\<lbrakk> c = Structures_A.ThreadCap t; cap_relation c c';
       list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras';
@@ -2595,7 +2625,8 @@ lemma decode_tcb_inv_corres:
              corres_guard_imp[OF decode_set_ipc_corres]
              corres_guard_imp[OF decode_set_space_corres]
              corres_guard_imp[OF decode_bind_notification_corres]
-             corres_guard_imp[OF decode_unbind_notification_corres],
+             corres_guard_imp[OF decode_unbind_notification_corres]
+             corres_guard_imp[OF decode_set_tls_base_corres],
          simp_all add: valid_cap_simps valid_cap_simps' invs_def valid_sched_def)
   apply (auto simp: list_all2_map1 list_all2_map2
              elim!: list_all2_mono)
@@ -2637,6 +2668,14 @@ lemma decodeUnbindNotification_wf:
   apply (auto simp: obj_at'_def pred_tcb_at'_def)
   done
 
+lemma decodeSetTLSBase_wf:
+  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace>
+     decodeSetTLSBase w (capability.ThreadCap t)
+   \<lbrace>tcb_inv_wf'\<rbrace>,-"
+  apply (simp add: decodeSetTLSBase_def
+             cong: list.case_cong)
+  by wpsimp
+
 lemma decodeTCBInv_wf:
   "\<lbrace>invs' and tcb_at' t and cte_at' slot and ex_nonz_cap_to' t
          and (\<lambda>s. \<forall>x \<in> set extras. real_cte_at' (snd x) s
@@ -2646,7 +2685,7 @@ lemma decodeTCBInv_wf:
   apply (simp add: decodeTCBInvocation_def Let_def
               cong: if_cong invocation_label.case_cong split del: if_split)
   apply (rule hoare_pre)
-   apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf
+   apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf decodeSetTLSBase_wf
              decodeCopyReg_wf decodeBindNotification_wf decodeUnbindNotification_wf)+)
   apply (clarsimp simp: real_cte_at')
   apply (fastforce simp: real_cte_at_not_tcb_at' objBits_defs)
@@ -2703,6 +2742,7 @@ lemma invokeTCB_makes_simple':
         apply ((wp restart_makes_simple' suspend_makes_simple'
                   mapM_x_wp'
                      | simp cong: if_cong)+)[5]
+    apply (wpsimp split: if_split)
    apply (rule hoare_pre)
     apply ((simp split del: if_split
              | wp cteDelete_makes_simple' checkCap_inv [where P="st_tcb_at' simple' t"]
diff --git a/proof/refine/X64/Tcb_R.thy b/proof/refine/X64/Tcb_R.thy
index a72b8a758..c53e5e149 100644
--- a/proof/refine/X64/Tcb_R.thy
+++ b/proof/refine/X64/Tcb_R.thy
@@ -1638,6 +1638,8 @@ where
     = (x = tcbinvocation.Resume a)"
 | "tcbinv_relation (tcb_invocation.NotificationControl t ntfnptr) x
     = (x = tcbinvocation.NotificationControl t ntfnptr)"
+| "tcbinv_relation (tcb_invocation.SetTLSBase ref w) x
+    = (x = tcbinvocation.SetTLSBase ref w)"
 
 primrec
   tcb_inv_wf' :: "tcbinvocation \<Rightarrow> kernel_state \<Rightarrow> bool"
@@ -1675,6 +1677,8 @@ where
                                            \<and> (\<forall>q. ntfnObj ko \<noteq> WaitingNtfn q)) ntfnptr
                                           and ex_nonz_cap_to' ntfnptr
                                           and bound_tcb_at' (op = None) t) )"
+| "tcb_inv_wf' (tcbinvocation.SetTLSBase ref w)
+             = (tcb_at' ref and ex_nonz_cap_to' ref)"
 
 lemma tcbinv_corres:
  "tcbinv_relation ti ti' \<Longrightarrow>
@@ -1683,42 +1687,53 @@ lemma tcbinv_corres:
          (invs' and sch_act_simple and tcb_inv_wf' ti')
          (invoke_tcb ti) (invokeTCB ti')"
   apply (case_tac ti, simp_all only: tcbinv_relation.simps valid_tcb_invocation_def)
-        apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
-       apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
-      apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
-     apply (clarsimp simp del: invoke_tcb.simps)
-     apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
-     apply (rule_tac F="is_aligned word 5" in corres_req)
-      apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
-     apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
-      apply (clarsimp simp: is_cnode_or_valid_arch_def
-                     split: option.split option.split_asm)
-     apply clarsimp
-     apply (auto split: option.split_asm simp: newroot_rel_def)[1]
+         apply (rule corres_guard_imp [OF writereg_corres], simp+)[1]
+        apply (rule corres_guard_imp [OF readreg_corres], simp+)[1]
+       apply (rule corres_guard_imp [OF copyreg_corres], simp+)[1]
+      apply (clarsimp simp del: invoke_tcb.simps)
+      apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11)
+      apply (rule_tac F="is_aligned word 5" in corres_req)
+       apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned])
+      apply (rule corres_guard_imp [OF tc_corres], clarsimp+)
+       apply (clarsimp simp: is_cnode_or_valid_arch_def
+                      split: option.split option.split_asm)
+      apply clarsimp
+      apply (auto split: option.split_asm simp: newroot_rel_def)[1]
+     apply (simp add: invokeTCB_def liftM_def[symmetric]
+                      o_def dc_def[symmetric])
+     apply (rule corres_guard_imp [OF suspend_corres], simp+)
     apply (simp add: invokeTCB_def liftM_def[symmetric]
                      o_def dc_def[symmetric])
-    apply (rule corres_guard_imp [OF suspend_corres], simp+)
-   apply (simp add: invokeTCB_def liftM_def[symmetric]
-                    o_def dc_def[symmetric])
-   apply (rule corres_guard_imp [OF restart_corres], simp+)
-  apply (simp add:invokeTCB_def)
-  apply (rename_tac option)
-  apply (case_tac option)
+    apply (rule corres_guard_imp [OF restart_corres], simp+)
+   apply (simp add:invokeTCB_def)
+   apply (rename_tac option)
+   apply (case_tac option)
+    apply simp
+    apply (rule corres_guard_imp)
+      apply (rule corres_split[OF _ unbind_notification_corres])
+        apply (rule corres_trivial, simp)
+       apply wp+
+     apply (clarsimp)
+    apply clarsimp
    apply simp
    apply (rule corres_guard_imp)
-     apply (rule corres_split[OF _ unbind_notification_corres])
+     apply (rule corres_split[OF _ bind_notification_corres])
        apply (rule corres_trivial, simp)
       apply wp+
-    apply (clarsimp)
-   apply clarsimp
-  apply simp
+    apply clarsimp
+    apply (clarsimp simp: obj_at_def is_ntfn)
+   apply (clarsimp simp: obj_at'_def projectKOs)
+  apply (simp add: invokeTCB_def tlsBaseRegister_def)
   apply (rule corres_guard_imp)
-    apply (rule corres_split[OF _ bind_notification_corres])
-      apply (rule corres_trivial, simp)
-     apply wp+
-   apply clarsimp
-   apply (clarsimp simp: obj_at_def is_ntfn)
-  apply (clarsimp simp: obj_at'_def projectKOs)
+    apply (rule corres_split[OF _ TcbAcc_R.user_setreg_corres])
+      apply (rule corres_split[OF _ Bits_R.gct_corres])
+        apply (rule corres_split[OF _ Corres_UL.corres_when])
+            apply (rule corres_trivial, simp)
+           apply simp
+          apply (rule TcbAcc_R.rescheduleRequired_corres)
+         apply (wpsimp wp: hoare_drop_imp)+
+   apply (clarsimp simp: valid_sched_weak_strg einvs_valid_etcbs)
+  apply (clarsimp simp: Tcb_R.invs_valid_queues' Invariants_H.invs_queues)
   done
 
 lemma tcbBoundNotification_caps_safe[simp]:
@@ -1801,22 +1816,29 @@ lemma tcbntfn_invs':
    apply (wp unbindNotification_invs bindNotification_invs' | simp)+
   done
 
+lemma setTLSBase_invs'[wp]:
+  "\<lbrace>invs' and tcb_inv_wf' (tcbinvocation.SetTLSBase tcb tls_base)\<rbrace>
+       invokeTCB (tcbinvocation.SetTLSBase tcb tls_base)
+   \<lbrace>\<lambda>rv. invs'\<rbrace>"
+  by (wpsimp simp: invokeTCB_def)
+
 lemma tcbinv_invs':
   "\<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' ti\<rbrace>
      invokeTCB ti
    \<lbrace>\<lambda>rv. invs'\<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 (wp restart_invs')
         apply (clarsimp simp: invs'_def valid_state'_def
-                       dest!: global'_no_ex_cap)
-       apply (simp add: invokeTCB_def)
-       apply (wp restart_invs')
-       apply (clarsimp simp: invs'_def valid_state'_def
-                      dest!: global'_no_ex_cap)
-      apply (wp tc_invs')
-      apply (clarsimp split: option.split dest!: isCapDs)
-     apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs' | simp)+
+                        dest!: global'_no_ex_cap)
+       apply (wp tc_invs')
+       apply (clarsimp split: option.split dest!: isCapDs)
+      apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs'
+             | simp)+
   done
 
 crunch_ignore (add: setNextPC getRestartPC)
@@ -2608,6 +2630,14 @@ lemma decode_unbind_notification_corres:
    apply auto
   done
 
+lemma decode_set_tls_base_corres:
+  "corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t)
+          (decode_set_tls_base w (cap.ThreadCap t))
+          (decodeSetTLSBase w (capability.ThreadCap t))"
+  apply (clarsimp simp: decode_set_tls_base_def decodeSetTLSBase_def returnOk_def
+                 split: list.split)
+  by (rule sym, rule ucast_id)
+
 lemma decode_tcb_inv_corres:
  "\<lbrakk> c = Structures_A.ThreadCap t; cap_relation c c';
       list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras';
@@ -2634,7 +2664,8 @@ lemma decode_tcb_inv_corres:
              corres_guard_imp[OF decode_set_ipc_corres]
              corres_guard_imp[OF decode_set_space_corres]
              corres_guard_imp[OF decode_bind_notification_corres]
-             corres_guard_imp[OF decode_unbind_notification_corres],
+             corres_guard_imp[OF decode_unbind_notification_corres]
+             corres_guard_imp[OF decode_set_tls_base_corres],
          simp_all add: valid_cap_simps valid_cap_simps' invs_def valid_sched_def)
   apply (auto simp: list_all2_map1 list_all2_map2
              elim!: list_all2_mono)
@@ -2676,6 +2707,14 @@ lemma decodeUnbindNotification_wf:
   apply (auto simp: obj_at'_def pred_tcb_at'_def)
   done
 
+lemma decodeSetTLSBase_wf:
+  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace>
+     decodeSetTLSBase w (capability.ThreadCap t)
+   \<lbrace>tcb_inv_wf'\<rbrace>,-"
+  apply (simp add: decodeSetTLSBase_def
+             cong: list.case_cong)
+  by wpsimp
+
 lemma decodeTCBInv_wf:
   "\<lbrace>invs' and tcb_at' t and cte_at' slot and ex_nonz_cap_to' t
          and (\<lambda>s. \<forall>x \<in> set extras. real_cte_at' (snd x) s
@@ -2685,7 +2724,7 @@ lemma decodeTCBInv_wf:
   apply (simp add: decodeTCBInvocation_def Let_def
               cong: if_cong invocation_label.case_cong split del: if_split)
   apply (rule hoare_pre)
-   apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf
+   apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf decodeSetTLSBase_wf
              decodeCopyReg_wf decodeBindNotification_wf decodeUnbindNotification_wf)+)
   apply (clarsimp simp: real_cte_at')
   apply (fastforce simp: real_cte_at_not_tcb_at' objBits_defs)
@@ -2742,6 +2781,7 @@ lemma invokeTCB_makes_simple':
         apply ((wp restart_makes_simple' suspend_makes_simple'
                   mapM_x_wp'
                      | simp cong: if_cong)+)[5]
+    apply (wpsimp split: if_split)
    apply (rule hoare_pre)
     apply ((simp split del: if_split
              | wp cteDelete_makes_simple' checkCap_inv [where P="st_tcb_at' simple' t"]