Engine: propagate trait generics arguments

[W95Psp]

This PR requires #698.

This PR propagates trait generics arguments throughout the engine.

On the F* output:

• now the calls to methods will always be method #self_type #trait_generic_arg1 ... #trait_generic_argN #Typeclasses.solve #method_generic_type1 ... #method_generic_typeM method_generic_const1 ... method_generic_constI meth_arg1 ... meth_argJ
• traits and inductive (enums/structs) should have all their argument explicit

Todo:

• use the information in the F* backend
• propagate the information in the proof libs

When undrafted, this PR should fix #719

[W95Psp]

I think this should work, maybe there are a few things in the library we need to fix, but we will discover those by running hax on various things.

@mamonet can you try this branch on ml-kem?
If you run in anything suspicious related to implcits or something similar, tell me directly!

[franziskuskiefer]

@W95Psp this doesn't build with the same issue as in the visitor PR

# File "utils/generate_visitors/errors.ml", line 27, characters 29-35:
# 27 |     | UnsupportedCoreType of string
#                                   ^^^^^^

[W95Psp]

Ah, yes, thanks @franziskuskiefer, will rebase this PR with generate-visitors to propagate that change

[franziskuskiefer]

lgtm when it works for @mamonet

[mamonet]

This PR seems to be solving the issue. I went through the instances that I'm aware of, and all of them verified successfully. However, I got one undesired change here https://github.com/cryspen/libcrux/blob/dev_ml_kem_lax/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti#L35-L37
This create an error Expected type Type but t_PolynomialRingElement v_Vector has type i1: Vector.Traits.t_Operations v_Vector -> Type0 in references of t_PolynomialRingElement
Here is the original type https://github.com/cryspen/libcrux/blob/main/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti#L35-L37

[W95Psp]

Fantastic!
Thanks for your feedback! I see what it is, give me 10-15 minutes I will push a fix!

[W95Psp]

@mamonet, I pushed a commit, can you tell me if that's fixing that regression? 😃

[mamonet]

Of course, just 2 minutes to report back

[mamonet]

The fix gets t_PolynomialRingElement back to what it is, I think this PR is in a good shape now.

[W95Psp]

Ah, that's great news!
I'm gonna rebase the PR to main, and then we can merge it! 🥳