First version of external core models.

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "hax-lib/core-models"]
+	path = hax-lib/core-models
+	url = https://github.com/cryspen/rust-core-models

Cargo.toml

@@ -17,7 +17,7 @@ members = [
      "rust-engine",
      "rust-engine/macros",
 ]
-exclude = ["tests", "rustc-coverage-tests", "rust-engine/tests", "hax-lib/core-models"]
+exclude = ["tests", "rustc-coverage-tests", "rust-engine/tests", "hax-lib/core-models", "hax-lib/std"]
 default-members = [
      "frontend/exporter",
      "frontend/exporter/options",

engine/backends/fstar/fstar_backend.ml

@@ -829,13 +829,9 @@ struct
       | GCType { goal; name } ->
           let typ = c_trait_goal span goal in
           Some { kind = Tcresolve; ident = F.id name; typ }
-      | GCProjection { impl = { kind = LocalBound { id }; _ }; assoc_item; typ }
-        ->
-          let proj =
-            F.term
-            @@ F.AST.Project
-                 (F.term @@ F.AST.Var (F.lid [ id ]), pconcrete_ident assoc_item)
-          in
+      | GCProjection { impl; assoc_item; typ } ->
+          let* i = pimpl_expr span impl in
+          let proj = F.term @@ F.AST.Project (i, pconcrete_ident assoc_item) in
           let typ =
             F.mk_refined "_" (F.term_of_string "unit") (fun ~x ->
                 F.term