pq-code-package
Standardize on signed integers in quantifiers and loops.
Conjecture: it is better for proof performance and stability to use signed "int" types for quantifiers, loop indexing expressions, for loop counters. This PR implements this change to gain data on its impact on proof and runtime performance.
Specifically, use signed "int" for:
- for loop counters
- quantified expressions
- variables and struct fields that count or index into arrays
- formal parameters for array indexes, offsets and counts
Additionally, strengthen pre-conditions on polyvecl_add() and polyveck_add() to stabilize proof of those functions for all parameter sets.
Opening a PR here to get Benchmark results.
This change, if we want it, should be coordinated with mlkem-native. However, I seem to remember that we have done a round-trip on this one already on mlkem-native, changing to int and back. If there is a larger win to be had, OK (the CI should tell!), but otherwise I prefer not to change this again for now. There's a lot of issues open at the moment that we should work on first.
Proof results, running on an r7g instance with -j16 (so as close as I can get to the CI runner that we use for CBMC). The first figure is real-time, the second is CPU "user" time,
Branch main:
MLDSA-44: 6m56s, 40m57s
MLDSA-65: 5m13s, 45m38s
MLDSA-87: 8m03s, 52m10s
Branch signed_loop_quants:
MLDSA-44: 3m39s, 31m42s
MLDSA-65: 3m29s, 34m57s
MLDSA-87: 7m41s, 40m36s
The proof performance looks really good, but runtime performance is affected by 1-5% for the C backend(s), particularly on Intel/AMD. I will look at the "components" benchmark to see what's going on.
The performance degradation appears to be concentrated in the Inverse NTT in the C backend. Not sure what's going on.