CBMC: Increase OBJECT_BITS in poly_invntt_tomont proof

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: Increase OBJECT_BITS in poly_invntt_tomont proof #402

Closed hanno-becker closed 1 week ago

hanno-becker commented 1 week ago

We see spurious failures of poly_invntt_tomont, and bumping OBJECT_BITS is an attempt to fix those. It's to be determined whether this is indeed the root cause.