karthikbhargavan

This PR modifies the F* parameters to make the nightly proof CI work again. Fixes https://github.com/cryspen/libcrux/issues/953

Use ghost state

5

Cloning values before mutation just so that we can refer to them in invariants and proofs is not a great style for Rust since it may and sometimes does blow...

Mutable Style for ML-KEM

13

Transforming ML-KEM to use &muts everywhere. #947 [skip changelog]

Type-based secret independence

5

This is an initial PR to include type-based secret independence in Libcrux. The new crate `secrets` introduces types and functions for secret integers. A future PR will provide a more...

This is a Work-in-Progress PR that adds support for AES-GCM. It is inspired by existing work in HACL* for this primitive. The PR contains three implementations of AES and three...

Some optimizations for SHA-3 on Aarch64

3

Using new intrinsics and improving load performance for portable. This is worth testing on multiple Arm machines, because the cargo benchmarks are a bit iffy. On my machine, the performance...

Meta: Improve Specs and Reduce Annotations for ML-DSA Proofs

3

While the first goal for ML-DSA verification is to get robust proofs in place, we would like to investigate and implement improvements in the style and follow them as we...

Verify ML-DSA: Add length pre- and post-conditions to functions

1

This is more of a meta-issue, but we will start with specific modules. We need to add length pre- and post-conditions on all functions that have slice inputs. As an...

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

This PR switches slices to use a functional array model. Examples pass, but it needs CI checks, and we need to test it on other repositories. Warning: breaking change.