Improve proof speed of invntt_layer()

[rod-chapman]

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]

@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]

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]

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

main (75f52dc): 14s, 12s, 12s
this PR (777a962): 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]

Looking at the CI

• This PR (777a962): https://github.com/pq-code-package/mlkem-native/actions/runs/11891527348/job/33132598924
• main (75f52dc): https://github.com/pq-code-package/mlkem-native/actions/runs/11892007517/job/33134210894

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

[rod-chapman]

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]

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