karthikbhargavan

Still seeing some bad examples, e.g. https://github.com/cryspen/libcrux/blob/9097d098ba27f5f99ea14397399ad0d0ee5cf395/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti#L66

I found a few other instances of this. I think this has to have a higher priority since the bug and its fix are quite obscure.

lets eliminate all instances in libcrux to test first On Thu, Nov 28, 2024, 09:44 Lucas Franceschino ***@***.***> wrote: > Well, we did no any work towards this 😅 >...

Here is an actual bug: when I write ``` #[ensures(|out| fstar!("v $LEN < pow2 32 ==> $out == Spec.Utils.map_array (Spec.Utils.v_PRF $LEN) $input"))] fn PRFxN(input: &[[u8; 33]; K]) -> [[u8; LEN];...

https://github.com/cryspen/libcrux/pull/598

yes. i will update with status and plans

Did a big push in this PR: https://github.com/cryspen/libcrux/pull/589 More work coming this week.

Almost done with this now. Want to do another round of cleanups and merge to main.

Closing this in favor of a "merging dev to main" Issue: https://github.com/cryspen/libcrux/issues/613

A grep for the patter "& [" yields: src/arithmetic.rs src/encoding/commitment.rs src/encoding/error.rs src/encoding/t1.rs src/encoding/verification_key.rs src/encoding/t0.rs src/encoding/gamma1.rs src/encoding/signing_key.rs src/encoding/signature.rs src/hash_functions.rs src/matrix.rs src/ml_dsa_44.rs src/ml_dsa_65.rs src/ml_dsa_87.rs src/ml_dsa_generic/instantiations/avx2.rs src/ml_dsa_generic/multiplexing.rs src/ml_dsa_generic/instantiations.rs src/ml_dsa_generic.rs src/polynomial.rs src/pre_hash.rs src/sample.rs src/samplex4.rs...