search

pq-code-package / mlkem-native

High-assurance, high-performance ML-KEM implementation for mobile, pc, and server targets
https://pq-code-package.github.io/mlkem-native/dev/bench/
Apache License 2.0
11 stars 9 forks source link

CBMC: Add spec + proof for gen_matrix_entry_x4 and gen_matrix #365

Closed hanno-becker closed 2 weeks ago

hanno-becker commented 2 weeks ago

Much harder than anticipated. See the individual commit messages for detailed descriptions of the pre-work that had to happen.