Franziskus Kiefer

and bump tls_codec dependency

- [ ] measure stack usage - [ ] SHAKE 256 Xof - [ ] benchmarks

spdx license for ml-kem

1

cc #376

The hax extraction on main is broken because the patches don't apply cleanly anymore. But we're moving to the new version anyway https://github.com/cryspen/libcrux/actions/runs/9671649730 - [ ] disable patches on ci...

- [ ] Benchmarks - [ ] Tests - [ ] Measure stack usage

When https://github.com/hacspec/hax/issues/616 is fixed we can undo all the ugliness of moving code out of `impl` blocks.

[ML-KEM] Cleanup unpacked API benchmarks

1

All of these should use the macros in here, then they become only a few lines. But we can clean that up later if you prefer and file an issue....

PQCP release workflow

6

This issue tracks the pqcp packaging and release policies. - [ ] #376 - [ ] #377 - [ ] #381 - CI - [ ] #378 - [ ]...

Verify ML-DSA

2

The proofs require three levels of work: - [x] extract F* #341 - [ ] Lax-checking the F* code (also on CI) - [ ] Verifying the platform-dependent code (simd/portable...