bgv : Add a verifier for Rotate

[Maokami]

I believe there should be a check ensuring that the dimension of the ciphertext, which serves as the operand of rotation, is two.

Justification:

• SEAL throw an error when the above condition is violated: https://github.com/microsoft/SEAL/blob/206648d0e4634e5c61dcf9370676630268290b59/native/src/seal/evaluator.h#L1046
• There's a bug in OpenFHE when the above condition is violated: https://github.com/openfheorg/openfhe-development/issues/575

However, due to my lack of HE knowledge, I don't know why the rotation doesn't work when the dimension of ciphertext is greater than 2. Let me know if anyone knows!

[j2kun]

I will summarize the work needed to do this in HEIR, in case you are looking to dip your feet into the coding. A high-level explanation of how verifiers work is here.

• Add let hasVerifier = 1; to the BGV rotate op in BGVOps.td
• Add a new implementation of a function with signature LogicalResult RotateOp::verify() { ... } to BGVDialect.cpp that makes the required check and reports an error if it fails.
• Add a lit test in tests/bgv that uses --verify-diagnostics to assert the appropriate error message is reported when verification fails. A good example is here

[asraa]

Let me know if anyone knows!

While I don't think it's theoretically impossible to apply a galois rotation on a length 3 ciphertext, I think the reason both implementations avoid doing so is because the Galois Keys are computed to switch the ciphertext from being encrypted from a key (1, s^i) to a (1, s). If the ciphertext has length 3, then I'm not sure why there aren't static size checks, but the key switching matrix would only apply to the first two polys of the ciphertext and then probably leave an incorrect result.

[Maokami]

@j2kun @asraa Thank you for the pointers and explanations!

Before I start writing verifiers, I believe it's essential to establish the specification of the operations.

Based on this issue and this conversation, it's challenging to determine which inputs are valid for each operation of the HE schemes. In this case, should we really reject cases where c.dim != 2 in rotate(c)? As @asraa pointed out, theoretically speaking, isn't it valid operation?

One viable option is to follow the lead of existing libraries. For rotations, to the best of my knowledge, SEAL, OpenFHE, and Lattigo all prohibit the case where c.dim != 2. Would it be acceptable to create a verifier based on these criteria?

[j2kun]

I think prohibiting c.dim != 2 is acceptable. And generally speaking, my philosophy of software design is that it's better to start with a strict definition and relax it or generalize it only once you have a good reason to.

[j2kun]

Thanks again @Maokami! Please let me know if there is any other topic you want to work on in the project. I'm happy to help.

[Maokami]

Thank you for your help! I'll take a closer look at the project to see if there's any other stuff I can contribute.