Update charon

flake.nix

@@ -89,10 +89,12 @@
       checks.default = packages.default.tests;
       devShells.default = pkgs.mkShell {
         packages = [
+          pkgs.fstar
+          pkgs.clang
+          pkgs.clang-tools # For clang-format
           pkgs.ocamlPackages.ocaml
           pkgs.ocamlPackages.ocamlformat
           pkgs.ocamlPackages.menhir
-          pkgs.clang-tools # For clang-format
         ];
 
         inputsFrom = [

include/eurydice_glue.h

@@ -85,7 +85,7 @@ typedef struct {
 
 #define Eurydice_array_eq(sz, a1, a2, t, _, _ret_t)                            \
   (memcmp(a1, a2, sz * sizeof(t)) == 0)
-#define core_array_equality___core__cmp__PartialEq__Array_B__N___for__Array_A__N____eq \
+#define core_array_equality___core__cmp__PartialEq__Array_U__N___for__Array_T__N____eq \
   Eurydice_array_eq
 
 #define core_slice___Slice_T___split_at(slice, mid, element_type, ret_t)       \
@@ -135,6 +135,21 @@ core_convert_num___core__convert__From_i32__for_i64__59__from(int32_t x) {
   return x;
 }
 
+static inline uint64_t
+core_convert_num___core__convert__From_u8__for_u64__66__from(uint8_t x) {
+  return x;
+}
+
+static inline uint64_t
+core_convert_num___core__convert__From_u16__for_u64__70__from(uint16_t x) {
+  return x;
+}
+
+static inline size_t
+core_convert_num___core__convert__From_u16__for_usize__96__from(uint16_t x) {
+  return x;
+}
+
 static inline uint32_t core_num__u8_6__count_ones(uint8_t x0) {
 #ifdef _MSC_VER
   return __popcnt(x0);
@@ -163,9 +178,15 @@ static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) {
   return (*p) >> v;
 }
 
-// ITERATORS
+#define core_num_nonzero_private_NonZeroUsizeInner size_t
+static inline core_num_nonzero_private_NonZeroUsizeInner
+core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__NonZeroUsizeInner__26__clone(
+  core_num_nonzero_private_NonZeroUsizeInner *x0
+) {
+  return *x0;
+}
 
-#define core_num_nonzero_NonZeroUsize size_t
+// ITERATORS
 #define Eurydice_range_iter_next(iter_ptr, t, ret_t)                           \
   (((iter_ptr)->start == (iter_ptr)->end)                                      \
        ? (CLITERAL(ret_t){.tag = core_option_None})                            \
@@ -183,6 +204,9 @@ static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) {
 #define Eurydice_into_iter(x, t, _ret_t) (x)
 #define core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter \
   Eurydice_into_iter
+// This name changed on 20240627
+#define core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I__1__into_iter \
+  Eurydice_into_iter
 
 typedef struct {
   Eurydice_slice slice;
@@ -214,11 +238,16 @@ static inline Eurydice_slice chunk_next(Eurydice_chunks *chunks,
       .chunk_size = sz_})
 #define core_slice_iter_Chunks Eurydice_chunks
 #define core_slice_iter_ChunksExact Eurydice_chunks
-#define core_slice_iter___core__iter__traits__iterator__Iterator_for_core__slice__iter__Chunks__a__T___70__next( \
+#define Eurydice_chunks_next( \
     iter, t, ret_t)                                                                                              \
   (((iter)->slice.len == 0) ? ((ret_t){.tag = core_option_None})                                                 \
                             : ((ret_t){.tag = core_option_Some,                                                  \
                                        .f0 = chunk_next(iter, sizeof(t))}))
+#define core_slice_iter___core__iter__traits__iterator__Iterator_for_core__slice__iter__Chunks__a__T___70__next \
+  Eurydice_chunks_next
+// This name changed on 20240627
+#define core_slice_iter___core__iter__traits__iterator__Iterator_for_core__slice__iter__Chunks__a__T___71__next \
+  Eurydice_chunks_next
 #define core_slice_iter__core__slice__iter__ChunksExact__a__T__89__next(       \
     iter, t, _ret_t)                                                           \
   core_slice_iter__core__slice__iter__Chunks__a__T__70__next(iter, t)

lib/Builtin.ml

@@ -40,6 +40,10 @@ let result = ["core"; "result"], "Result"
 let mk_result t1 t2 =
   K.TApp (result, [ t1; t2 ])
 
+let nonzero = ["core"; "num"; "nonzero"], "NonZero"
+let mk_nonzero t =
+  K.TApp (nonzero, [ t ])
+
 (* A record to hold a builtin function with all relevant information for both
    krml and the transpilation phase in AstOfLlbc *)
 
@@ -342,6 +346,10 @@ let unwrap: K.decl =
       with_type t_T (EAbort (Some t_T, Some "unwrap not Ok"))
     ])))
 
+let nonzero_def = K.DType (nonzero, [], 0, 1, Abbrev (TBound 0))
+
+(* -------------------------------------------------------------------------- *)
+
 type usage = Used | Unused
 
 let replacements = List.map (fun decl ->
@@ -380,6 +388,8 @@ let files = [
     replace;
     bitand_pv_u8;
     shr_pv_u8;
+  ] @ [
+    nonzero_def
   ] in
   "Eurydice", externals
 ]

scripts/update-charon-pin.sh

@@ -9,3 +9,4 @@ CHARON_BRANCH="$(git -C "$CHARON_DIR" rev-parse --abbrev-ref HEAD)"
 CHARON_COMMIT="$(git -C "$CHARON_DIR" rev-parse HEAD)"
 echo 'Taking the commit from your local charon directory. The charon branch is `'"$CHARON_BRANCH"'`'
 nix flake lock --extra-experimental-features nix-command --extra-experimental-features flakes --override-input charon "github:aeneasverif/charon/$CHARON_COMMIT"
+nix flake lock --extra-experimental-features nix-command --extra-experimental-features flakes --update-input charon/rust-overlay