Improve speed of proof of matvec_mul()

pq-code-package / mlkem-native

High-assurance, high-performance ML-KEM implementation for mobile, pc, and server targets

Apache License 2.0

11 stars 9 forks source link

Closed rod-chapman closed 1 week ago

rod-chapman commented 1 week ago

Adjust modelling of arrays in CBMC for proof of this function, as recommended by CBMC team (See CBMC Issue 8505).

Proof for this function reduces from 70 seconds to about 9 seconds on desktop.

All tests OK All proofs OK lint OK

rod-chapman commented 1 week ago

Comment added to Makefile