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

Improve proof speed of invntt_layer() #411

Closed rod-chapman closed 2 days ago

rod-chapman commented 1 week ago

For this proof we tell CBMC to remove constraints that are not in the cone of influcence of the proof obligations using the --slice-formula option.

Experiment shows this reduces proof time for this subprogram from about 40s to about 12s on a developer's laptop.

Total proof time (using 8 CPU cores on M1 MacBook Pro) before: 3m 46s after: 3m 7s

All tests OK All proofs OK lint OK

hanno-becker commented 5 days ago

@rod-chapman The speed gain seems well within the variance of runtime, isn't it? If so, I'd prefer not to add the flag.

rod-chapman commented 4 days ago

Well... I see "variance of runtime" in the CI as a bug in the CI system. Adding --slice-formula consistently saves 22s of CPU time of this one proof for me, every time. Impact on a multi-core machine running all the proofs will vary, of course.

mkannwischer commented 3 days ago

I've measured this on my i7-1360P for 3 runs each (time MLKEM_K=3 make result in the invntt_layer dir)

main (75f52dc1c259d69bb4e30ef86886a9c0e01c5935): 14s, 12s, 12s this PR (777a9624c46f37ef000201eb0f1bdc0355079e49): 12s, 14s, 12s

This does not seem to be a bottleneck for me and the PR does not change anything. Am I doing something wrong?

mkannwischer commented 3 days ago

Looking at the CI

I also see 13-14 seconds on Graviton 3. Is this really that much slower on Apple M1?

rod-chapman commented 3 days ago

I am checking. In short: it's a problem with Z3 on macOS, where run time and memory consumption are an order of magnitude more than on Graviton/Linux and Intel/Linux. Even within the NIX shell, the same version of Z3 running on the same input files actually differs in behaviour on all 3 platforms.

rod-chapman commented 2 days ago

I have opened https://github.com/Z3Prover/z3/issues/7457 to report this problem with Z3. On short: it diverges on macOS for reasons as yet unknown. Suggest we close this issue here.