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

Speed up CBMC proof of polyvec_tobytes() #353

Closed hanno-becker closed 2 weeks ago

hanno-becker commented 2 weeks ago

This was running very slowly. This commit reduces the runtime from minutes to seconds by switching to smt2 and using a loop invariant.

hanno-becker commented 2 weeks ago

Integrated into #348