Verify ML-DSA: portable/encoding/commitment

[karthikbhargavan]

Verify https://github.com/cryspen/libcrux/blob/main/libcrux-ml-dsa/src/simd/portable/encoding/commitment.rs

• Write a spec for the functions
• Design tactic to prove correctness
• Prove panic freedom
• Prove correctness

[W95Psp]

The F* spec for the function will be something like:

let n = ${serialized.len()} in
let inputs = bit_vec_of_int_t_array ${simd_unit.values} n in
let outputs = bit_vec_of_int_t_array ${future(serialized)} 8 in
(forall (i: nat {i < 8 * n}). inputs i == outputs i)

In other words, the two following sequences of bits should be equal. Let n be the length of serialized.

• the n first bits of the 8 i32 found in simd_unit.value;
• the 8 bits of each u8 in serialized after calling (serialize(simd_unit, serialized)).

For the tactic, the previous tactic should work, but we need to make fold_enumerated_chunked_slice normalizable: currently it is not defined, we only have a signature.

Questions:

• shall we still do F*-only specs, or do we want to reflect that in Rust? no, we still will do that in F*

[W95Psp]

cryspen/hax#1238 was required for this to happen.
That PR is now in the merge queue.