diff --git a/include/eurydice/core.h b/include/eurydice/core.h
index 3e99bf8d..8b80ca91 100644
--- a/include/eurydice/core.h
+++ b/include/eurydice/core.h
@@ -173,17 +173,23 @@ static inline size_t core_num__usize__wrapping_mul(size_t x, size_t y) {
 }
 
 static inline uint64_t core_num__u64__rotate_left(uint64_t x0, uint32_t x1) {
+  assert(x1 < 64);
   return (x0 << x1) | (x0 >> ((-x1) & 63));
 }
 
+static inline uint32_t core_num__u32__rotate_left(uint32_t x0, uint32_t x1) {
+  assert(x1 < 32);
+  return (x0 << x1) | (x0 >> ((-x1) & 31));
+}
+
 static inline void core_ops_arith__i32__add_assign(int32_t *x0, int32_t *x1) {
   *x0 = *x0 + *x1;
 }
 
-static inline uint8_t Eurydice_bitand_pv_u8(uint8_t *p, uint8_t v) {
+static inline uint8_t Eurydice_bitand_pv_u8(const uint8_t *p, uint8_t v) {
   return (*p) & v;
 }
-static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) {
+static inline uint8_t Eurydice_shr_pv_u8(const uint8_t *p, int32_t v) {
   return (*p) >> v;
 }
 static inline uint32_t Eurydice_min_u32(uint32_t x, uint32_t y) {
@@ -191,13 +197,13 @@ static inline uint32_t Eurydice_min_u32(uint32_t x, uint32_t y) {
 }
 
 static inline uint8_t
-core_ops_bit__core__ops__bit__BitAnd_u8__u8__for___a__u8___bitand(uint8_t *x0,
+core_ops_bit__core__ops__bit__BitAnd_u8__u8__for__0__u8___bitand(const uint8_t *x0,
                                                                   uint8_t x1) {
   return Eurydice_bitand_pv_u8(x0, x1);
 }
 
 static inline uint8_t
-core_ops_bit__core__ops__bit__Shr_i32__u8__for___a__u8___shr(uint8_t *x0,
+core_ops_bit__core__ops__bit__Shr_i32__u8__for__0__u8___shr(const uint8_t *x0,
                                                              int32_t x1) {
   return Eurydice_shr_pv_u8(x0, x1);
 }
@@ -209,6 +215,10 @@ core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__N
   return *x0;
 }
 
+#define core_option__core__option__Option_T__TraitClause_0___is_some(X, _0, \
+                                                                     _1)    \
+  ((X)->tag == 1)
+
 #if defined(__cplusplus) && !defined(KRML_CXX17_COMPAT)
 }
 #endif
diff --git a/include/eurydice/slice.h b/include/eurydice/slice.h
index fa4e139a..b497a0a2 100644
--- a/include/eurydice/slice.h
+++ b/include/eurydice/slice.h
@@ -2,6 +2,7 @@
 
 #include <inttypes.h>
 #include <stdlib.h>
+#include <string.h>
 
 // SLICES, ARRAYS, ETC.
 
@@ -42,6 +43,9 @@ typedef struct Eurydice_mut_borrow_slice_i16_s {
   (KRML_CLITERAL(ret_t){EURYDICE_CFIELD(.ptr =)(ptr_)->data,                   \
                         EURYDICE_CFIELD(.meta =) len_})
 
+#define core_array___Array_T__N___as_mut_slice(len_, ptr_, t, ret_t) \
+  core_array___Array_T__N___as_slice(len_, ptr_, t, ret_t)
+
 #define core_array__core__clone__Clone_for__Array_T__N___clone(                \
     len, src, elem_type, _ret_t)                                               \
   (*(src))
@@ -59,6 +63,10 @@ typedef struct Eurydice_mut_borrow_slice_i16_s {
 #define Eurydice_array_eq_slice_mut(sz, a1, s2, t, _)                          \
   Eurydice_array_eq_slice_shared(sz, a1, s2, t, _)
 
+#define Eurydice_slice_eq_shared(s1, s2, t, _) \
+  ((s1)->meta == (s2)->meta &&                 \
+   memcmp((s1)->ptr, (s2)->ptr, (s1)->meta * sizeof(t)) == 0)
+
 // DEPRECATED -- should no longer be generated
 #define core_array_equality__core__cmp__PartialEq__Array_U__N___for__Array_T__N___eq( \
     sz, a1, a2, t, _, _ret_t)                                                         \