Regarding compressions

[vincentvbh]

Platform:
Which platform does this concern?

• platform independent
• aarch64
• x86_64
• rv64
• other

Issue category:

Which part(s) of mlkem-native does this issue concern:

• core crypto: ML-KEM
• core crypto: FIPS202
• documentation
• integration
• CBMC
• CI
• Testing

I notice that currently the compression functions are updated. The Barrett-based compressions were already released here https://github.com/vincentvbh/Compressions. You can find various implementations for each of them, including Armv7-M, Armv7E-M, Armv8-A Neon, and AVX2. Some of the implementations are also formally verified and the paper will be out soon.

The optimization relies on the following:

• Work on the signed integer instead of unsigned ones.
• Sharpening the precision of Barrett-based compressions with brute-force testing.

The resulting computations are formally verified and remove the need to convert elements from signed integers to unsigned.
Additional details will be public once the paper is published, and detailed explanations of the implementations are included in my thesis that I'm currently working.

Vincent Hwang

[vincentvbh]

Oops! The Armv7-M implementations are only in a private repo and not in the repo mentioned earlier. Anyway, the Armv7-M implementations are just the straightforward assembly of the C versions.

[vincentvbh]

See earlier PR here pq-crystals/kyber#83.

[hanno-becker]

@vincentvbh Thanks for bringing this to our attention! I can't say we would / would not want this off hand, but a good base for discussions would be a draft PR exemplifying your approach by adjusting some of the C compression routines. We'd also need to confirm that CBMC can still prove correctness of your code, please have a try (for 16-bit arithmetic, most things can just be brute-forced, so I'm not worried). We'd rather not want to pull in a third verification toolchain in addition to CBMC and HOL-Light.

[mkannwischer]

Thanks for the pointer @vincentvbh.

Do you have an estimate on the performance impact on AArch64 (or x86_64) platforms?

[hanno-becker]

On second thought, let's keep discussing the merits and impact of the proposal here first; no PR needed for now. @vincentvbh Please share your paper once available.

[mkannwischer]

@vincentvbh could you please clarify if you think some code in mlkem-native can be improved or if this issue is mostly a pointer to your work that we should consider? It isn't entirely clear to me.

[vincentvbh]

The code in mlkem-native could be improved: Take compressd_10 and compressd_11 as examples, they are using uint64_t. We can instead use int32_t if we keep the elements as signed integers instead.

[vincentvbh]

See https://github.com/vincentvbh/Compressions/blob/main/src/test.c#L101 and https://github.com/vincentvbh/Compressions/blob/main/src/test.c#L109 for the C implementation and https://github.com/vincentvbh/Compressions/blob/main/src/avx2.c for the avx2 one and https://github.com/vincentvbh/Compressions/blob/main/src/neon.c for the neon one.