Translate existential predicates

.github/workflows/ci.yml

@@ -82,6 +82,7 @@ jobs:
           CHARON: ${{needs.select-dep-versions.outputs.charon}}
           AENEAS: ${{needs.select-dep-versions.outputs.aeneas}}
         run: |
+          echo 'Using the aeneas commit selected by `select-dep-versions`'
           nix flake update --refresh \
               charon aeneas \
               --override-input charon github:aeneasverif/charon/$CHARON \
@@ -99,6 +100,7 @@ jobs:
           CHARON: ${{needs.select-dep-versions.outputs.charon}}
           EURYDICE: ${{needs.select-dep-versions.outputs.eurydice}}
         run: |
+          echo 'Using the eurydice commit selected by `select-dep-versions`'
           nix flake update --refresh \
               charon eurydice \
               --override-input charon github:aeneasverif/charon/$CHARON \
@@ -117,6 +119,7 @@ jobs:
           EURYDICE: ${{needs.select-dep-versions.outputs.eurydice}}
           LIBCRUX: ${{needs.select-dep-versions.outputs.libcrux}}
         run: |
+          echo 'Using the eurydice and libcrux commits selected by `select-dep-versions`'
           nix flake update --refresh \
               charon eurydice \
               --override-input charon github:aeneasverif/charon/$CHARON \

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.115"
+let supported_charon_version = "0.1.116"

charon-ml/src/NameMatcher.ml

@@ -996,12 +996,15 @@ and ty_to_pattern_aux (ctx : 'fun_body ctx) (c : to_pat_config)
         else Some (ty_to_pattern_aux ctx c m output)
       in
       EArrow (inputs, output)
+  | TError _ -> EVar None
   | TRawPtr (ty, RMut) -> ERawPtr (Mut, ty_to_pattern_aux ctx c m ty)
   | TRawPtr (ty, RShared) -> ERawPtr (Not, ty_to_pattern_aux ctx c m ty)
-  | TFnDef _ -> raise (Failure "Unimplemented: FnDef")
-  | TDynTrait _ -> raise (Failure "Unimplemented: DynTrait")
-  | TNever -> raise (Failure "Unimplemented: Never")
-  | TError _ -> EVar None
+  | _ ->
+      let fmt_env = ctx_to_fmt_env ctx in
+      raise
+        (Failure
+           ("Can't convert type to pattern: "
+           ^ PrintTypes.ty_to_string fmt_env ty))
 
 and trait_ref_item_with_generics_to_pattern (ctx : 'fun_body ctx)
     (c : to_pat_config) (m : constraints) (trait_ref : T.trait_ref)

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -197,6 +197,7 @@ and binder_kind_of_json (ctx : of_json_ctx) (js : json) :
         let* x_1 = trait_item_name_of_json ctx x_1 in
         Ok (BKTraitMethod (x_0, x_1))
     | `String "InherentImplBlock" -> Ok BKInherentImplBlock
+    | `String "Dyn" -> Ok BKDyn
     | `String "Other" -> Ok BKOther
     | _ -> Error "")
 
@@ -600,11 +601,13 @@ and discriminant_layout_of_json (ctx : of_json_ctx) (js : json) :
         Ok ({ offset; tag_ty; encoding } : discriminant_layout)
     | _ -> Error "")
 
-and existential_predicate_of_json (ctx : of_json_ctx) (js : json) :
-    (existential_predicate, string) result =
+and dyn_predicate_of_json (ctx : of_json_ctx) (js : json) :
+    (dyn_predicate, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
-    | `Null -> Ok ()
+    | `Assoc [ ("binder", binder) ] ->
+        let* binder = binder_of_json ty_of_json ctx binder in
+        Ok ({ binder } : dyn_predicate)
     | _ -> Error "")
 
 and field_of_json (ctx : of_json_ctx) (js : json) : (field, string) result =
@@ -1790,7 +1793,7 @@ and ty_of_json (ctx : of_json_ctx) (js : json) : (ty, string) result =
         let* x_1 = trait_item_name_of_json ctx x_1 in
         Ok (TTraitType (x_0, x_1))
     | `Assoc [ ("DynTrait", dyn_trait) ] ->
-        let* dyn_trait = existential_predicate_of_json ctx dyn_trait in
+        let* dyn_trait = dyn_predicate_of_json ctx dyn_trait in
         Ok (TDynTrait dyn_trait)
     | `Assoc [ ("FnPtr", fn_ptr) ] ->
         let* fn_ptr =