diff --git a/camkes/glue-proofs/Libsel4.thy b/camkes/glue-proofs/Libsel4.thy
deleted file mode 100644
index e2ce00840..000000000
--- a/camkes/glue-proofs/Libsel4.thy
+++ /dev/null
@@ -1,393 +0,0 @@
-theory Libsel4 imports
-  "../../tools/c-parser/CTranslation"
-  "../../tools/autocorres/AutoCorres"
-  "../../tools/autocorres/NonDetMonadEx"
-begin
-
-(* This theory contains some lemmas about libsel4 that are useful for CAmkES systems, but are likely
- * useful for other user-level reasoning on seL4 as well.
- *)
-
-(* Load the fragment of libsel4 we need for reasoning about seL4_GetMR and seL4_SetMR. *)
-install_C_file "libsel4.c"
-
-autocorres [ts_rules=nondet, no_heap_abs=seL4_SetMR] "libsel4.c"
-
-context libsel4 begin
-
-abbreviation "seL4_MsgMaxLength \<equiv> 120"
-
-lemma le_step_down:"\<lbrakk>(i::int) < n; i = n - 1 \<Longrightarrow> P; i < n - 1 \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-  apply arith
-  done
-
-(* Avoid having to hold Isabelle's hand with "unat (of_int x)". *)
-lemma unat_nat[simp]:"\<lbrakk>(i::int) \<ge> 0; i < seL4_MsgMaxLength\<rbrakk> \<Longrightarrow> unat ((of_int i)::sword32) = nat i"
-  apply (erule le_step_down, simp, simp)+
-  done
-
-(* A manually abstracted version of seL4_SetMR. A future version of AutoCorres should translate
- * seL4_SetMR to this automatically.
- *)
-definition
-  seL4_SetMR_lifted' :: "int \<Rightarrow> word32 \<Rightarrow> (lifted_globals, unit) nondet_monad"
-where
-  "seL4_SetMR_lifted' i val \<equiv>
-   do
-     ret' \<leftarrow> seL4_GetIPCBuffer';
-     guard (\<lambda>s. i < seL4_MsgMaxLength);
-     guard (\<lambda>s. 0 \<le> i);
-     modify (\<lambda>s. s \<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(ret' :=
-        msg_C_update  (
-            \<lambda>a. Arrays.update a (nat i) val) (heap_seL4_IPCBuffer__C s ret')
-          )  \<rparr>)
-  od"
-
-definition
-  globals_frame_intact :: "lifted_globals \<Rightarrow> bool"
-where
-  "globals_frame_intact s \<equiv> is_valid_seL4_IPCBuffer__C'ptr s (Ptr (scast seL4_GlobalsFrame))"
-definition
-  ipc_buffer_valid :: "lifted_globals \<Rightarrow> bool"
-where
-  "ipc_buffer_valid s \<equiv> is_valid_seL4_IPCBuffer__C s
-      (heap_seL4_IPCBuffer__C'ptr s (Ptr (scast seL4_GlobalsFrame)))"
-
-(* seL4_GetMR and seL4_SetMR call seL4_GetIPCBuffer, so we're going to need a WP lemma about it. *)
-lemma seL4_GetIPCBuffer_wp[THEN validNF_make_schematic_post, simplified]:
-  "\<forall>s'. \<lbrace>\<lambda>s. globals_frame_intact s \<and>
-             s = s'\<rbrace>
-     seL4_GetIPCBuffer'
-   \<lbrace>\<lambda>r s. r = heap_seL4_IPCBuffer__C'ptr s (Ptr (scast seL4_GlobalsFrame)) \<and>
-          s = s'\<rbrace>!"
-  apply (rule allI)
-  apply (simp add:seL4_GetIPCBuffer'_def)
-  apply wp
-  apply (clarsimp simp:globals_frame_intact_def)
-  done
-
-(* Functional versions of seL4_SetMR and seL4_GetMR. See how these are used below for stating
- * transformations on states.
- *)
-definition
-  setMR :: "lifted_globals \<Rightarrow> nat \<Rightarrow> word32 \<Rightarrow> lifted_globals"
-where
-  "setMR s i v \<equiv>
-      s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)
-        (heap_seL4_IPCBuffer__C'ptr s (Ptr (scast seL4_GlobalsFrame)) :=
-          msg_C_update (\<lambda>a. Arrays.update a i v)
-            (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s
-              (Ptr (scast seL4_GlobalsFrame)))))\<rparr>"
-definition
-  getMR :: "lifted_globals \<Rightarrow> nat \<Rightarrow> word32"
-where
-  "getMR s i \<equiv>
-       index (msg_C (heap_seL4_IPCBuffer__C s
-            (heap_seL4_IPCBuffer__C'ptr s (Ptr (scast seL4_GlobalsFrame))))) i"
-
-lemma getMR_setMR:
-  "\<lbrakk>i < seL4_MsgMaxLength\<rbrakk> \<Longrightarrow> getMR (setMR s j v) i = (if i = j then v else getMR s i)"
-  apply (simp add:getMR_def setMR_def fun_upd_def)
-  done
-
-lemma msg_update_id:"msg_C_update (\<lambda>r. Arrays.update r i (index (msg_C y) i)) y = y"
-  apply (cut_tac f="(\<lambda>r. Arrays.update r i (index (msg_C y) i))" and
-                 f'=id and r=y and r'=y in seL4_IPCBuffer__C_fold_congs(2))
-     apply simp+
-  apply (simp add:id_def) 
-  apply (metis seL4_IPCBuffer__C_accupd_diff(22) seL4_IPCBuffer__C_accupd_diff(24)
-               seL4_IPCBuffer__C_accupd_diff(26) seL4_IPCBuffer__C_accupd_diff(28)
-               seL4_IPCBuffer__C_accupd_diff(30) seL4_IPCBuffer__C_accupd_diff(41)
-               seL4_IPCBuffer__C_accupd_same(2) seL4_IPCBuffer__C_idupdates(1))
-  done
-
-lemma setMR_getMR:
-  "setMR s i (getMR s i) = s"
-  apply (simp add:setMR_def getMR_def)
-  apply (subst msg_update_id)
-  apply simp
-  done
-
-lemma if_fold:"(if P then Q else if P then R else S) = (if P then Q else S)"
-  by presburger
-
-lemma setMR_setMR[simp]:"setMR (setMR s i x) i y = setMR s i y"
-  apply (simp add:setMR_def fun_upd_def)
-  apply (subst if_fold)
-  apply (subst comp_def, subst update_update)
-  apply simp
-  done
-
-lemma seL4_GetMR_wp[wp_unsafe]:
-  "\<lbrace>\<lambda>s. (i::int) \<ge> 0 \<and>
-            i < seL4_MsgMaxLength \<and>
-            globals_frame_intact s \<and>
-            ipc_buffer_valid s \<and>
-            P (getMR s (nat i)) s\<rbrace>
-     seL4_GetMR' i
-   \<lbrace>P\<rbrace>!"
-  apply (simp add:seL4_GetMR'_def)
-  apply (wp seL4_GetIPCBuffer_wp)
-  apply (simp add:globals_frame_intact_def ipc_buffer_valid_def getMR_def)
-  done
-
-end
-
-locale SetMR = libsel4 +
-  (* This assumption should go away in future when the abstraction is performed automatically. *)
-  assumes seL4_SetMR_axiom:"exec_concrete lift_global_heap (seL4_SetMR' i val) =
-                                seL4_SetMR_lifted' i val"
-begin
-
-lemma seL4_SetMR_wp[wp_unsafe]:
-  notes seL4_SetMR_axiom[simp]
-  shows
-  "\<lbrace>\<lambda>s. globals_frame_intact s \<and>
-        ipc_buffer_valid s \<and>
-        i \<ge> 0 \<and>
-        i < seL4_MsgMaxLength \<and>
-        (\<forall>x. P x (setMR s (nat i) v))\<rbrace>
-     exec_concrete lift_global_heap (seL4_SetMR' i v)
-   \<lbrace>P\<rbrace>!"
-  apply (simp add:seL4_SetMR_lifted'_def)
-  apply (wp seL4_GetIPCBuffer_wp)
-  apply (simp add:setMR_def globals_frame_intact_def ipc_buffer_valid_def)
-  done
-
-(* When you write to a message register and then read back from the same register, you get the value
- * you wrote and the only state you have affected is that register.
- *)
-lemma "\<forall>(i::int) x. \<lbrace>\<lambda>s. i \<ge> 0 \<and> i < seL4_MsgMaxLength \<and>
-                         globals_frame_intact s \<and>
-                         ipc_buffer_valid s \<and>
-                         P (setMR s (nat i) x)\<rbrace>
-         do exec_concrete lift_global_heap (seL4_SetMR' i x);
-            seL4_GetMR' i
-         od
-             \<lbrace>\<lambda>r s. globals_frame_intact s \<and>
-                    ipc_buffer_valid s \<and>
-                    r = x \<and>
-                    P s\<rbrace>!"
-  apply (rule allI)+
-  apply (wp seL4_GetMR_wp seL4_SetMR_wp)
-  apply clarsimp
-  apply (subst getMR_setMR)
-   apply (erule le_step_down, simp, simp)+
-  apply (simp add:setMR_def getMR_def globals_frame_intact_def ipc_buffer_valid_def)
-  done
-
-(* seL4_SetMR run twice on the same register is the same as just running the second invocation. *)
-lemma SetMR_SetMR:"\<forall>(i::int) x y. \<lbrace>\<lambda>s. i \<ge> 0 \<and> i < seL4_MsgMaxLength \<and>
-                           globals_frame_intact s \<and>
-                           ipc_buffer_valid s \<and>
-                           P (setMR s (nat i) y)\<rbrace>
-         do exec_concrete lift_global_heap (seL4_SetMR' i x);
-            exec_concrete lift_global_heap (seL4_SetMR' i y)
-         od
-             \<lbrace>\<lambda>_ s. globals_frame_intact s \<and>
-                    ipc_buffer_valid s \<and>
-                    P s\<rbrace>!"
-  apply (rule allI)+
-  apply (wp seL4_SetMR_wp)
-  apply clarsimp
-  apply (simp add:setMR_def globals_frame_intact_def ipc_buffer_valid_def)
-  done
-
-(* seL4_SetMR with the value that is already in that message register does nothing. *)
-lemma "\<forall>(i::int) x s'. \<lbrace>\<lambda>s. i \<ge> 0 \<and> i < seL4_MsgMaxLength \<and>
-                            globals_frame_intact s \<and>
-                            ipc_buffer_valid s \<and>
-                            x = getMR s (nat i) \<and>
-                            s = s'\<rbrace>
-          exec_concrete lift_global_heap (seL4_SetMR' i x)
-        \<lbrace>\<lambda>_ s. s = s'\<rbrace>!"
-  apply (rule allI)+
-  apply (wp seL4_SetMR_wp)
-  apply clarsimp
-  apply (simp add:setMR_getMR)
-  done
-
-(* SetMRs on distinct registers can be reordered. You probably never want to use this lemma, but
- * it's nice to know it's true.
- *)
-lemma SetMR_reorder:"\<lbrakk>i \<noteq> j\<rbrakk> \<Longrightarrow> do exec_concrete lift_global_heap (seL4_SetMR' i x);
-                    exec_concrete lift_global_heap (seL4_SetMR' j y)
-                 od
-               = do exec_concrete lift_global_heap (seL4_SetMR' j y);
-                    exec_concrete lift_global_heap (seL4_SetMR' i x)
-                 od"
-  apply (subst seL4_SetMR_axiom)+
-  apply (case_tac "i < 0 \<or> j < 0")
-   apply (simp add:seL4_SetMR_lifted'_def seL4_GetIPCBuffer'_def bind_assoc seL4_GlobalsFrame_def)
-   apply (monad_eq)
-   apply (auto simp: fun_upd_def o_def split: split_if split_if_asm)[1]
-  apply (simp add:seL4_SetMR_lifted'_def seL4_GetIPCBuffer'_def bind_assoc seL4_GlobalsFrame_def)
-  apply (monad_eq)
-  apply (auto simp: fun_upd_def o_def split: split_if split_if_asm)[1]
-  done
-
-lemma SetMR_reorder2:
-      "do exec_concrete lift_global_heap (seL4_SetMR' i x);
-          exec_concrete lift_global_heap (seL4_SetMR' j x)
-       od
-          = do exec_concrete lift_global_heap (seL4_SetMR' j x);
-               exec_concrete lift_global_heap (seL4_SetMR' i x)
-            od"
-  apply (case_tac "i = j")
-   apply clarsimp
-  apply (rule SetMR_reorder)
-  apply assumption
-  done
-
-definition
-  messageInfo_new :: "word32 \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> word32"
-where
-  "messageInfo_new label capsUnwrapped extraCaps len \<equiv>
-    (label && 0xFFFFF << 12) || (capsUnwrapped && 7 << 9) || (extraCaps && 3 << 7) || (len && 0x7F)"
-
-lemma seL4_MessageInfo_new_wp[THEN validNF_make_schematic_post, simplified]:"\<forall>s'. \<lbrace>\<lambda>s. s = s'\<rbrace>
-              seL4_MessageInfo_new' l c e len
-            \<lbrace>\<lambda>r s. index (words_C r) 0 = messageInfo_new l c e len \<and> s = s'\<rbrace>!"
-  apply (rule allI)
-  apply (simp add:seL4_MessageInfo_new'_def)
-  apply wp
-  apply (clarsimp simp:messageInfo_new_def word_bw_comms word_bw_lcs)
-  apply (metis (no_types, hide_lams) word_bw_assocs(2))
-  done
-
-definition
-  MessageInfo_get_length :: "seL4_MessageInfo_C \<Rightarrow> word32"
-where
-  "MessageInfo_get_length info = (index (words_C info) 0) && 0x7f"
-
-lemma seL4_MessageInfo_get_length_wp[THEN validNF_make_schematic_post, simplified]:
-  "\<forall>s'. \<lbrace>\<lambda>s. s = s'\<rbrace>
-     seL4_MessageInfo_get_length' info
-        \<lbrace>\<lambda>r s. r = MessageInfo_get_length info \<and> s = s'\<rbrace>!"
-  apply (rule allI)
-  apply (simp add:seL4_MessageInfo_get_length'_def MessageInfo_get_length_def)
-  apply wp
-  apply simp
-  done
-
-definition
-  MessageInfo_get_label :: "seL4_MessageInfo_C \<Rightarrow> word32"
-where
-  "MessageInfo_get_label info = (index (words_C info) 0) && 0xFFFFF000 >> 12"
-
-lemma seL4_MessageInfo_get_label_wp[THEN validNF_make_schematic_post, simplified]:
-  "\<forall>s'. \<lbrace>\<lambda>s. s = s'\<rbrace>
-     seL4_MessageInfo_get_label' info
-        \<lbrace>\<lambda>r s. r = MessageInfo_get_label info \<and> s = s'\<rbrace>!"
-  apply (rule allI)
-  apply (simp add:seL4_MessageInfo_get_label'_def MessageInfo_get_label_def)
-  apply wp
-  apply simp
-  done
-
-definition
-  MessageInfo_get_capsUnwrapped :: "seL4_MessageInfo_C \<Rightarrow> word32"
-where
-  "MessageInfo_get_capsUnwrapped info = (index (words_C info) 0) && 0xE00 >> 9"
-
-lemma seL4_MessageInfo_get_capsUnwrapped_wp[THEN validNF_make_schematic_post, simplified]:
-  "\<forall>s'. \<lbrace>\<lambda>s. s = s'\<rbrace>
-     seL4_MessageInfo_get_capsUnwrapped' info
-        \<lbrace>\<lambda>r s. r = MessageInfo_get_capsUnwrapped info \<and> s = s'\<rbrace>!"
-  apply (rule allI)
-  apply (simp add:seL4_MessageInfo_get_capsUnwrapped'_def MessageInfo_get_capsUnwrapped_def)
-  apply wp
-  apply simp
-  done
-  
-definition
-  MessageInfo_get_extraCaps :: "seL4_MessageInfo_C \<Rightarrow> word32"
-where
-  "MessageInfo_get_extraCaps info = (index (words_C info) 0) && 0x180 >> 7"
-
-lemma seL4_MessageInfo_get_extraCaps_wp[THEN validNF_make_schematic_post, simplified]:
-  "\<forall>s'. \<lbrace>\<lambda>s. s = s'\<rbrace>
-     seL4_MessageInfo_get_extraCaps' info
-        \<lbrace>\<lambda>r s. r = MessageInfo_get_extraCaps info \<and> s = s'\<rbrace>!"
-  apply (rule allI)
-  apply (simp add:seL4_MessageInfo_get_extraCaps'_def MessageInfo_get_extraCaps_def)
-  apply wp
-  apply simp
-  done
-
-(* FIXME: MOVE *)
-lemma le_mask_imp_and_mask:"(x::word32) \<le> mask n \<Longrightarrow> x && mask n = x"
-  by (metis and_mask_eq_iff_le_mask)
-
-(* FIXME: MOVE *)
-lemma or_not_mask_nop:"((x::word32) || ~~ mask n) && mask n = x && mask n"
-  by (metis word_and_not word_ao_dist2 word_bw_comms(1) word_log_esimps(3))
-
-(* FIXME: MOVE *)
-lemma mask_exceed:"n \<ge> 32 \<Longrightarrow> (x::word32) && ~~ mask n = 0"
-  apply (metis (erased, hide_lams) is_aligned_neg_mask is_aligned_neg_mask_eq mask_32_max_word
-                                   word_bool_alg.compl_one word_bool_alg.conj_zero_right)
-  done
-
-(* FIXME: MOVE *)
-lemma mask_subsume:"\<lbrakk>n \<le> m\<rbrakk> \<Longrightarrow> ((x::word32) || y && mask n) && ~~ mask m = x && ~~ mask m"
-  apply (subst word_ao_dist)
-  apply (subgoal_tac "(y && mask n) && ~~ mask m = 0")
-   apply simp
-  by (metis (no_types, hide_lams) is_aligned_mask is_aligned_weaken word_and_not word_bool_alg.conj_zero_right word_bw_comms(1) word_bw_lcs(1))
-
-(* FIXME: MOVE *)
-lemma mask_twice2:"n \<le> m \<Longrightarrow> ((x::word32) && mask m) && mask n = x && mask n"
-  by (metis mask_twice min_def)
-
-(* FIXME: MOVE *)
-lemma not_mask_twice:"n \<le> m \<Longrightarrow> ((x::word32) && ~~ mask n) && ~~ mask m = x && ~~ mask m"
-  apply (subst word_bw_assocs(1))
-  apply (simp add:mask_def)
-  by (metis (erased, hide_lams) is_aligned_neg_mask is_aligned_neg_mask_eq mask_def shiftl_1 word_bitwise_m1_simps(2) word_bw_comms(1))
-
-lemma seL4_MessageInfo_set_length_wp[THEN validNF_make_schematic_post, simplified]:
-  "\<forall>s'. \<lbrace>\<lambda>s. s = s' \<and> len \<le> 0x7f\<rbrace>
-     seL4_MessageInfo_set_length' info len
-        \<lbrace>\<lambda>r s. MessageInfo_get_length r = len \<and>
-               MessageInfo_get_label info = MessageInfo_get_label r \<and>
-               MessageInfo_get_capsUnwrapped info = MessageInfo_get_capsUnwrapped r \<and>
-               MessageInfo_get_extraCaps info = MessageInfo_get_extraCaps r \<and>
-               s = s'\<rbrace>!"
-  apply (rule allI)
-  apply (simp add:seL4_MessageInfo_set_length'_def MessageInfo_get_length_def)
-  apply wp
-  apply clarsimp
-  apply (rule conjI)
-   apply (cut_tac x=len and n=7 in le_mask_imp_and_mask)
-    apply (simp add:mask_def)+
-   apply (subst word_oa_dist)
-   apply (subst word_bw_assocs(1))
-   apply (cut_tac x=len and n=7 in or_not_mask_nop)
-   apply (subst (asm) word_bw_comms(2))
-   apply (clarsimp simp:mask_def)
-  apply (simp add:MessageInfo_get_label_def)
-  apply (cut_tac x="index (words_C info) 0 && ~~ mask 7" and n=7 and
-                 m=12 and y=len in mask_subsume)
-   apply simp+
-  apply (simp add:mask_def)
-  apply (cut_tac x="index (words_C info) 0" and n=7 and m=12 in not_mask_twice)
-   apply (simp add:mask_def)+
-  apply (rule conjI)
-   apply (simp add:MessageInfo_get_capsUnwrapped_def)
-   apply (subst word_ao_dist)
-   apply (cut_tac x=len and y="0x7f" and z="0xe00" in word_bw_assocs(1))
-   apply simp
-   apply (subst word_bw_assocs(1))
-   apply simp
-  apply (simp add:MessageInfo_get_extraCaps_def)
-  apply (subst word_ao_dist)
-  apply (cut_tac x=len and y="0x7f" and z="0x180" in word_bw_assocs(1))
-  apply simp
-  apply (subst word_bw_assocs(1))
-  apply simp
-  done
-
-end
-
-end
diff --git a/camkes/glue-proofs/libsel4.c b/camkes/glue-proofs/libsel4.c
deleted file mode 100644
index 1fb91f254..000000000
--- a/camkes/glue-proofs/libsel4.c
+++ /dev/null
@@ -1,63 +0,0 @@
-/* Relevant parts of libsel4 */
-typedef unsigned int uint32_t;
-typedef uint32_t seL4_Word;
-typedef seL4_Word seL4_CPtr;
-struct seL4_MessageInfo {
-    uint32_t words[1];
-};
-typedef struct seL4_MessageInfo seL4_MessageInfo_t;
-struct seL4_IPCBuffer_ {
-    seL4_MessageInfo_t tag;
-    seL4_Word msg[120];
-    seL4_Word userData;
-    seL4_Word caps_or_badges[3];
-    seL4_CPtr receiveCNode;
-    seL4_CPtr receiveIndex;
-    seL4_Word receiveDepth;
-};
-typedef struct seL4_IPCBuffer_ seL4_IPCBuffer;
-static inline seL4_MessageInfo_t __attribute__((__const__)) seL4_MessageInfo_new(uint32_t label, uint32_t capsUnwrapped, uint32_t extraCaps, uint32_t length)  {
-    seL4_MessageInfo_t seL4_MessageInfo;
-    seL4_MessageInfo.words[0] = 0;
-    ((void)0);
-    seL4_MessageInfo.words[0] |= (label & 1048575) << 12;
-    ((void)0);
-    seL4_MessageInfo.words[0] |= (capsUnwrapped & 7) << 9;
-    ((void)0);
-    seL4_MessageInfo.words[0] |= (extraCaps & 3) << 7;
-    ((void)0);
-    seL4_MessageInfo.words[0] |= (length & 127) << 0;
-    return seL4_MessageInfo;
-}
-static inline uint32_t __attribute__((__const__))
-seL4_MessageInfo_get_label(seL4_MessageInfo_t seL4_MessageInfo) {
-    return (seL4_MessageInfo.words[0] & 0xfffff000) >> 12;
-}
-static inline uint32_t __attribute__((__const__))
-seL4_MessageInfo_get_capsUnwrapped(seL4_MessageInfo_t seL4_MessageInfo) {
-    return (seL4_MessageInfo.words[0] & 0xe00) >> 9;
-}
-static inline uint32_t __attribute__((__const__))
-seL4_MessageInfo_get_extraCaps(seL4_MessageInfo_t seL4_MessageInfo) {
-    return (seL4_MessageInfo.words[0] & 0x180) >> 7;
-}
-static inline uint32_t __attribute__((__const__)) seL4_MessageInfo_get_length(seL4_MessageInfo_t seL4_MessageInfo) {
-    return (seL4_MessageInfo.words[0] & 0x7f) >> 0;
-}
-static inline seL4_MessageInfo_t __attribute__((__const__)) seL4_MessageInfo_set_length(seL4_MessageInfo_t seL4_MessageInfo, uint32_t v) {
-    seL4_MessageInfo.words[0] &= ~0x7f;
-    seL4_MessageInfo.words[0] |= (v << 0) & 0x7f;
-    return seL4_MessageInfo;
-}
-enum  {
-    seL4_GlobalsFrame = 4294950912U
-};
-static inline seL4_IPCBuffer *seL4_GetIPCBuffer() {
-    return *(seL4_IPCBuffer **)seL4_GlobalsFrame;
-}
-static inline seL4_Word seL4_GetMR(int i) {
-    return seL4_GetIPCBuffer()->msg[i];
-}
-static inline void seL4_SetMR(int i, seL4_Word mr) {
-    seL4_GetIPCBuffer()->msg[i] = mr;
-}