Functional correctness for portable encoding commitment

[W95Psp]

This PR adds a specification and a proof for the serialize function of simd/portable/encoding/commitment in ML-DSA.

To do so, I had to take split the function in many smaller functions.

Fixes #745.

[franziskuskiefer]

Only a few nits and questions

[franziskuskiefer]

I filed AeneasVerif/eurydice#138 for the C failure. Unfortunately, I don't see a workaround for this right now.

[karthikbhargavan]

I opened an issue for follow-up improvements: #777
Let's add to that as we review and merge this PR.

[karthikbhargavan]

@W95Psp I adapted the code and changed the proof accordingly.
Please review and then: address the z3 version issue on CI (likely pinning to 4.13.3 would work)

I have no idea what the build failures with address sanitizer are doing on macos-latest.

[W95Psp]

Seems OK to me, though we should do something about the proofs: already my calc thing is too big for such a small function, now with the asserts that's a bit overwhelming.
But that works.

For Z3, I updated the job to use latest F*, which ships with Z3 4.13.3.

[W95Psp]

I experimented a bit with unrolling loops @karthikbhargavan, in branch lf-portable-encoding-commitment-experiment-unroll.

Sadly, this doesn't work out of the box, because of subslices.
I tried to define locally []. and update slice to have quantifiers everywhere, but that doesn't help.
Shall I investigate more?

[karthikbhargavan]

This PR still has an ASAN failure on Rust nightly on macos-latest.
However, I am going to merge it and do any necessary fixes in a future PR.