feat(engine) Extract vals for trait impls in interface only mode.

[maximebuyse]

Implements the action plan in #1113

[maximebuyse]

@karthikbhargavan You can test this branch and see if it solves your problem.

[karthikbhargavan]

We seem to be dropping generic arguments in the val, we should keep them (e.g. v_SIZE below):

 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_2 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
-    f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemCiphertext v_SIZE) -> true);
-    f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemCiphertext v_SIZE
-  }
+val impl_2:Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE)

[maximebuyse]

We seem to be dropping generic arguments in the val, we should keep them (e.g. v_SIZE below):

 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_2 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
-    f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemCiphertext v_SIZE) -> true);
-    f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemCiphertext v_SIZE
-  }
+val impl_2:Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE)

I pushed a fix

[karthikbhargavan]

Tested on ml-kem, works, at least for lax checking,.