Update toolchain

c/memory.c

@@ -99,8 +99,8 @@ uint32_t* mmap_sizes_init (size_t len) {
 /// Mman2
 
 // large allocator init
-Impl_Core_node__K___Prims_dtuple2___uint8_t_____size_t** mmap_ptr_metadata_init() {
-  return (Impl_Core_node__K___Prims_dtuple2___uint8_t_____size_t**) mmap_init(sizeof(Impl_Core_node__K___Prims_dtuple2___uint8_t_____size_t*));
+Impl_Trees_Cast_M_data** mmap_ptr_metadata_init() {
+  return (Impl_Trees_Cast_M_data**) mmap_init(sizeof(Impl_Trees_Cast_M_data*));
 }
 
 /// MemoryTrap.fst

c/utils.c

@@ -25,8 +25,8 @@ size_t builtin_mul_overflow(size_t x, size_t y) {
 
 // required comparison using uintptr_t
 uint64_t Impl_Trees_Cast_M_cmp(
-  K___Prims_dtuple2___uint8_t_____size_t x,
-  K___Prims_dtuple2___uint8_t_____size_t y) {
+  Impl_Trees_Cast_M_data x,
+  Impl_Trees_Cast_M_data y) {
   uintptr_t x_cast = (uintptr_t) x.fst;
   uintptr_t y_cast = (uintptr_t) y.fst;
   if (x_cast == y_cast) {
@@ -60,16 +60,16 @@ bool check_zeroing_u8(uint8_t* ptr, size_t len) {
 }
 
 // required casts
-Impl_Core_node__K___Prims_dtuple2___uint8_t_____size_t* Impl_Trees_Cast_M_array_u8__to__ref_node(uint8_t* arr) {
+Impl_Trees_Cast_M_data* Impl_Trees_Cast_M_array_u8__to__ref_node(uint8_t* arr) {
   // see lib_avl_mono/Impl.Trees.Types.fst
-  static_assert(sizeof(Impl_Core_node__K___Prims_dtuple2___uint8_t_____size_t) <= 64);
-  return (Impl_Core_node__K___Prims_dtuple2___uint8_t_____size_t*) arr;
+  static_assert(sizeof(Impl_Trees_Cast_M_data) <= 64);
+  return (Impl_Trees_Cast_M_data*) arr;
 }
-uint8_t* Impl_Trees_Cast_M_ref_node__to__array_u8(Impl_Core_node__K___Prims_dtuple2___uint8_t_____size_t* r) {
+uint8_t* Impl_Trees_Cast_M_ref_node__to__array_u8(Impl_Trees_Cast_M_data* r) {
   return (uint8_t*) r;
 }
 
-void FatalError_die_from_avl_node_malloc_failure (Impl_Core_node__K___Prims_dtuple2___uint8_t_____size_t, uint8_t* ptr) {
+void FatalError_die_from_avl_node_malloc_failure (Impl_Trees_Cast_M_data, uint8_t* ptr) {
   fatal_error("large allocator: AVL node allocation failed");
 }
 void FatalError_die_from_avl_node_free_failure (uint8_t* ptr) {

dist/ArrayList.c

@@ -24,10 +24,7 @@ size_t ArrayList_remove(ArrayList_cell *r, size_t hd1, size_t idx)
     ArrayList_cell prev1 = { .prev = prev.prev, .next = cell1.next, .data = prev.data };
     r[cell1.prev] = prev1;
   }
-  if (hd1 == idx)
-    return cell1.next;
-  else
-    return hd1;
+  return hd1 == idx ? cell1.next : hd1;
 }
 
 void ArrayList_insert(ArrayList_cell *r, size_t hd, size_t idx, uint32_t v)

dist/Bitmap5.c

@@ -11,10 +11,7 @@ bool Bitmap5_bm_get(uint64_t *arr, uint32_t k)
   uint64_t x = arr[k_index];
   uint64_t r1 = x >> k2;
   uint64_t r2 = r1 & 1ULL;
-  if (r2 == 1ULL)
-    return true;
-  else
-    return false;
+  return r2 == 1ULL;
 }
 
 void Bitmap5_bm_set(uint64_t *arr, uint32_t k)

dist/PtrdiffWrapper.c

@@ -6,9 +6,6 @@
 size_t PtrdiffWrapper_mmap_actual_size(size_t size)
 {
   size_t rem = size % (size_t)4096U;
-  if (rem != (size_t)0U)
-    return size - rem + (size_t)4096U;
-  else
-    return size;
+  return rem != (size_t)0U ? size - rem + (size_t)4096U : size;
 }
 

dist/SizeClassSelection.c

@@ -5,9 +5,9 @@
 
 #include "ExternUtils.h"
 
-krml_checked_int_t SizeClassSelection__n = (krml_checked_int_t)131072;
+krml_checked_int_t SizeClassSelection__n = 131072;
 
-krml_checked_int_t SizeClassSelection__k = (krml_checked_int_t)17;
+krml_checked_int_t SizeClassSelection__k = 17;
 
 uint32_t SizeClassSelection_log2u64(uint64_t x)
 {

dist/Slabs.c

@@ -42,11 +42,7 @@ update_quarantine2_aux(
     ArrayList_cell prev1 = { .prev = prev.prev, .next = cell.next, .data = prev.data };
     md_region[cell.prev] = prev1;
   }
-  size_t hd_;
-  if (idx5 == idx6)
-    hd_ = cell.next;
-  else
-    hd_ = idx5;
+  size_t hd_ = idx5 == idx6 ? cell.next : idx5;
   size_t sz_ = idx7 - (size_t)1U;
   ArrayListGen_tuple3 idxs = { .x = hd_, .y = tl_, .z = sz_ };
   ArrayList_insert(md_region, idx1, idx6, 0U);
@@ -143,11 +139,7 @@ SlabsFree_deallocate_slab(
             ArrayList_cell cell2 = { .prev = pos, .next = cell1.next, .data = cell1.data };
             md_region[idxs.y] = cell2;
           }
-          size_t tl_;
-          if (idxs.y == (size_t)16777217U)
-            tl_ = pos;
-          else
-            tl_ = idxs.z;
+          size_t tl_ = idxs.y == (size_t)16777217U ? pos : idxs.z;
           size_t sz_ = idxs.w + (size_t)1U;
           ArrayListGen_tuple2 idxs_ = { .x1 = tl_, .y1 = sz_ };
           update_quarantine3(sc, slab_region, idx7_, idxs);
@@ -203,11 +195,7 @@ SlabsFree_deallocate_slab(
             ArrayList_cell cell2 = { .prev = pos, .next = cell1.next, .data = cell1.data };
             md_region[idxs.y] = cell2;
           }
-          size_t tl_;
-          if (idxs.y == (size_t)16777217U)
-            tl_ = pos;
-          else
-            tl_ = idxs.z;
+          size_t tl_ = idxs.y == (size_t)16777217U ? pos : idxs.z;
           size_t sz_ = idxs.w + (size_t)1U;
           ArrayListGen_tuple2 idxs_ = { .x1 = tl_, .y1 = sz_ };
           update_quarantine3(sc, slab_region, idx7_, idxs);
@@ -284,11 +272,7 @@ allocate_slab_aux_4_aux1(
     ArrayList_cell prev1 = { .prev = prev.prev, .next = cell.next, .data = prev.data };
     md_region[cell.prev] = prev1;
   }
-  size_t hd_;
-  if (idx5 == idx6)
-    hd_ = cell.next;
-  else
-    hd_ = idx5;
+  size_t hd_ = idx5 == idx6 ? cell.next : idx5;
   size_t sz_ = idx7 - (size_t)1U;
   ArrayListGen_tuple3 idxs = { .x = hd_, .y = tl_, .z = sz_ };
   ArrayList_insert(md_region, idx1, idx6, 0U);

dist/Slots.c

@@ -28,11 +28,7 @@ static uint32_t get_free_slot(Constants_sc_full_ size_class, uint64_t *bitmap)
   uint32_t nb_slots_v = Utils2_nb_slots(size_class);
   uint32_t bound = nb_slots_v / 64U;
   uint32_t nb_slots_v_rem = nb_slots_v % 64U;
-  uint32_t bound2;
-  if (nb_slots_v_rem == 0U)
-    bound2 = 64U;
-  else
-    bound2 = nb_slots_v_rem;
+  uint32_t bound2 = nb_slots_v_rem == 0U ? 64U : nb_slots_v_rem;
   uint64_t full = Utils2_full_n(bound2);
   uint64_t x1 = bitmap[0U];
   if (x1 == full && bound > 1U)