[MLKEM] Proofs for avx2 serialize

[W95Psp]

We need to:

• replicate the tactic proof I'm doing for [ML-KEM] Complete portable serialize proofs #515 and [ML-KEM] Backport portable serialize proofs #481
• prove that correct with respect to the spec
• Look at 1 4 10 12

[franziskuskiefer]

Shouldn't this be in progress? @W95Psp @karthikbhargavan can you update?

[karthikbhargavan]

The tactic is done and has been successfully applied on some functions, but needs some debugging for the other serialization functions. This will need to wait till Lucas gets back,

[jschneider-bensch]

Should we try to get this in quickly before this is done? #518

I'm thinking we don't want to touch the code after the proofs are done.

[franziskuskiefer]

@W95Psp let us know if you want #518 in before, or leave it out for now.

[W95Psp]

I don't really know, but I think that's not important: we don't care about [de]serialize_11 currently, so we can postpone it I believe.

[karthikbhargavan]

Merged.