karthikbhargavan

When writing the following contracts on an `impl` block, several errors are triggered: ``` #[hax_lib::attributes] impl TryDecodeOps for [U32; N] { #[hax_lib::requires(N < 65536 / 4)] #[hax_lib::ensures(|result| if x.len() ==...

Merge dev to main

1

We need to merge the proofs in dev to main.

Remove admits, improve proof performance for ML-KEM

4

We still have some admits in the proofs. Some of these are because of F* performance. (The code verifies on some machines and not others). Other admits are simply things...

Port Arithmetic proofs from ML-KEM to ML-DSA

2

This requires #585

[ML-KEM] Link NTT Proofs to High-Level Spec

2

The arithmetic and NTT functions need to be properly linked to MLKEM.Spec rather than to localised specifications. - [x] vector/portable/arithmetic.rs - [x] vector/portable/ntt.rs - [x] vector/avx2/arithmetic.rs - [ ] vector/avx2/ntt.rs...

The recommended style for projects using `hax` is to make the dependence on `hax-lib` optional by guarding all uses of hax attributes with `cfg_attr(hax, ...)`. However, this does not work...

Restructuring P-Curves to enable more curves

2

## Proposed changes This PR restructures and generalizes the P-256 code in HACL* to allow for multiple curves. Subsequent PRs will add P-384 and P-521. ## Types of changes What...