karthikbhargavan

Restore SHA-3 speed by inlining absorb_inner

2

## Proposed changes This PR fixes Issue #954 by restoring the `inline_for_extraction` flags for `absorb_inner`. The trade-off is that the resulting C code is larger because the code in this...

This PR adds two attributes, one for adding `KRML_MUSTINLINE` and one for adding `__attribute((target("..."))`. Still needs tests.

A more complete spec of ML-KEM

2

This PR fills out some of the functions of the ML-KEM spec that had not been previously specified and does a general clean up of the spec in prep for...

This PR adds specs to the PRFxN and SHAKE APIs in hash_functions.rs. Note: SHAKE APIs are WIP Note: hax throws an error at this line: https://github.com/cryspen/libcrux/blob/847e1383fd52fb586ff8ff1f747db8904036a714/libcrux-ml-kem/src/hash_functions.rs#L451 ``` Fatal error: exception...

Formally Verify ML-KEM (Portable + AVX2)

1

Some dependencies: * ML-KEM Spec: [https://github.com/cryspen/libcrux/issues/144](https://github.com/cryspen/libcrux/issues/144) * Intrinsics Spec: [https://github.com/cryspen/libcrux/issues/452](https://github.com/cryspen/libcrux/issues/452) * Secret Independence: [https://github.com/cryspen/libcrux/issues/453](https://github.com/cryspen/libcrux/issues/453) * Bounded Integers: [https://github.com/hacspec/hax/issues/798](https://github.com/hacspec/hax/issues/798) * Iterators:[https://github.com/hacspec/hax/issues/394](https://github.com/hacspec/hax/issues/394), [https://github.com/hacspec/hax/issues/605](https://github.com/hacspec/hax/issues/605) ML-KEM Verification tasks: * vector/portable - [x] vector\_type.rs *...

Secret Independence for ML-KEM and ML-DSA

2

We need to prove secret-independence for the code in libcrux-ml-kem and libcrux-ml-dsa This will require merging some ongoing work in https://github.com/hacspec/hax/tree/karthik/secret-integers

To formally verify ML-KEM code, we need to add pre- and post-conditions for the code in libcrux-intrinsics.

Fix C build and benchmarks on Windows CI

2

Current the code in `libcrux-ml-kem/cg` does not build on Windows/MSVC and the so this build and the corresponding tests are disabled in `.github/workflows/c.yml`. We should debug and enable these, and...

Verify libcrux-sha3

1

Verify the libcrux-sha3 crate and show that libcrux-ml-kem and libcrux-ml-dsa use it correctly.

```rust #[hax_lib::fstar::after("let lemma (a:u8) (b:u8) : Lemma (ensures (f(f([a,b])) == [a,b])) = ()")] fn f(x: [u8; 2]) -> [u8; 2] { match x { [a, b] => [b, a] }...