Optimize clMul in Binary Common

[dhsorens]

Context

CompPoly/Fields/Binary/Common.lean contains this TODO above clMul:

optimize clMul, potentially using Karatsuba decomposition

clMul is currently a straightforward fold over 256 bits.

Proposed work

• Replace the current implementation with a faster approach (Karatsuba or another documented strategy).
• Keep the public API unchanged.

Acceptance criteria

• clMul/clSq behavior is unchanged on representative test cases.
• proofs and/or tests to show correctness

[DimitriosMitsios]

@dhsorens Can I work on it?

[dhsorens]

@DimitriosMitsios yes, please! :)

[chung-thai-nguyen]

@DimitriosMitsios FYI — I'm adding some clarification as you work on this. Since we don’t have concrete benchmarks, success for this problem can be evaluated through measurable improvements in mathematical efficiency (& performance efficiency ofc)

For example: reducing the number of XOR operations by half; cutting the BitVec size by half without increasing the number of XORs; etc.

Improvements along those lines would serve as useful success metrics.

[DimitriosMitsios]

@chung-thai-nguyen Sorry for the very late reply, I finally found time to work on the issue. I was thinking of implementing Karatsuba and providing proofs for correctness. Regarding tests, I think that Common.lean is not the place to include tests. Should I write some tests and share the results in the PR?

Given the long delay already, I will try to finish this soon!

[chung-thai-nguyen]

@DimitriosMitsios yes you can create another file to showcase some stress tests (e.g. a large amount of operations) that can be enable when needed, but won't add burden to the build process. I recommend looking from a broader view and optimize the whole clSq if possible, I think it has some space for optimizations. Improvements like 25% faster are expected.

[DimitriosMitsios]

@chung-thai-nguyen I managed to implement Karatsuba's algorithm and construct a version which is faster by around 24% in some preliminary tests (more are needed to conclude!).

I have a question about the signature of clMul. Currently clMul (a b : B256) : B256 which would silently truncate the output if a and b are actually longer that 128 bit. In CompPoly, clMul is always called with to256 applied to the input to ensure that bitvectors are of correct length and the same condition is imposed in toPoly_clMul_no_overflow.

Why don't we define clMul (a b : B128) : B256 instead?

[chung-thai-nguyen]

@DimitriosMitsios

• 24% is really good
• The output of clMul will be reduced module gHashPoly so it's not a simple truncation. I mean the high bits (128 - 255) contribute into the product.
• We set a b: B256 to account for the case where a or b has degree = 128 (so they are represented by 129 bits). This emerged somewhere in the proofs so we had toPoly_clMul_no_overflow. However, the code has changed since then so I'm not sure if this is true anymore, you can give it a try if you have time.