Add full type check for SHA3 portable

[parrot7483]

This PR adds full type checking for the SHA3 portable version for https://github.com/cryspen/libcrux/issues/395

Extract using hax.py extract --portable, prove using hax.py prove.

Besides prove code the following things where changed:

• reorder functions in libcrux-sha3/src/generic_keccak/xof.rs
• The absorb_full function in libcrux-sha3/src/generic_keccak/xof.rs previously did not always consume the internal buffer when it was full. This state could only be reached by misusing the API. The only bug I found.
• split up the rho and pi function for verification purpose

This version contains a few things I would consider "hacks"

• The extraction for the squeeze does not work. We add the expected F* code using hax_lib::fstar::replace
• impl From<u32> for Algorithm does not work because of the panic.
• In libcrux-sha3/src/generic_keccak/xof.rs the #[hax_lib::fstar::options("...")] has no effect. I use an hax_lib::fstar::before instead

[parrot7483]

@franziskuskiefer I applied your feedback and also cherry-picked one commit from my AVX/NEON branch adding the correct precondition on the traits and doing some light refactoring (mainly having consistent names for variables).

[parrot7483]

@franziskuskiefer I applied your review. cherry-picked https://github.com/cryspen/libcrux/pull/1157/commits/1064d0d2423630c0482d5d76039b38fe99214415 from SIMD branch. Merged main.

[parrot7483]

I have a tendency to pressing these big green buttons on github messing everything up. sorry.