Skip to content

Commit

Permalink
Add verifiers to BGV ops
Browse files Browse the repository at this point in the history
  • Loading branch information
@mr0re1
mr0re1 committed Sep 12, 2023
1 parent 26a119a commit cac9985
Show file tree
Hide file tree
Showing 2 changed files with 51 additions and 1 deletion.
7 changes: 6 additions & 1 deletion include/Dialect/BGV/IR/BGVOps.td
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ include "BGVTypes.td"
include "mlir/IR/OpBase.td"
include "mlir/Interfaces/InferTypeOpInterface.td"

// TODO(https://github.com/google/heir/issues/101): Add verifiers for BGV ops.
def SameOperandsAndResultRings: NativeOpTrait<"SameOperandsAndResultRings"> {
let cppNamespace = "::mlir::heir::bgv";
}
Expand Down Expand Up @@ -68,6 +67,8 @@ def BGV_MulOp : BGV_Op<"mul", [Commutative, SameOperandsAndResultRings, SameType
);

let assemblyFormat = "`(` operands `)` attr-dict `:` type($x) `->` type($output)" ;

let hasVerifier = 1;
}

def BGV_Rotate : BGV_Op<"rotate", [SameOperandsAndResultRings]> {
Expand Down Expand Up @@ -119,6 +120,8 @@ def BGV_Relinearize : BGV_Op<"relinearize", [SameOperandsAndResultRings]> {
let results = (outs
Ciphertext:$output
);

let hasVerifier = 1;
}

def BGV_ModulusSwitch : BGV_Op<"modulus_switch", [SameOperandsAndResultRings]> {
Expand All @@ -134,6 +137,8 @@ def BGV_ModulusSwitch : BGV_Op<"modulus_switch", [SameOperandsAndResultRings]> {
let results = (outs
Ciphertext:$output
);

let hasVerifier = 1;
}

#endif // HEIR_INCLUDE_DIALECT_BGV_IR_BGVOPS_TD_
45 changes: 45 additions & 0 deletions lib/Dialect/BGV/IR/BGVDialect.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,51 @@ void BGVDialect::initialize() {
>();
}

LogicalResult MulOp::verify() {
auto x = this->getX().getType();
auto y = this->getY().getType();
if (x.getDim() != y.getDim()) {
return this->emitOpError() << "input dimensions do not match";
}
auto out = this->getOutput().getType();
if (out.getDim() != 1 + x.getDim()) {

This comment has been minimized.

Sign in to view

Copy link
@Maokami

Maokami Nov 28, 2023 •
edited
Loading

Collaborator

I think the condition should be "out.getDim() == x.getDim() + y.getDim() - 1"?

This comment has been minimized.

Sign in to view

Copy link
@j2kun

j2kun Nov 28, 2023 •
edited
Loading

Collaborator

@Maokami I'm not a BGV expert, but I believe here "dimension" refers to the number of polynomials in the ciphertext (your comment appears to be interpreting getDim as the polynomial's degree?), and this is restricted in BGV to be either 2 or 3, corresponding to the key basis (1, s) before the multiplication vs the key basis (1, s, s^2) after. This implicitly requires one to relinearize after a multiplication.

I believe this is explained in the docs at https://heir.dev/docs/dialects/bgv/#ciphertexttype, but if it's unclear, please let me know and I can improve it.

This comment has been minimized.

Sign in to view

Copy link
@asraa

asraa Nov 28, 2023 •
edited
Loading

Collaborator

In general though, @Maokami has the right formula - e.g. if two 3 element ciphertexts were multiplied it would result in a 5 length ciphertext (terms would follow the basis of (1, s, s^2, s^3, s^4).

This comment has been minimized.

Sign in to view

Copy link
@Maokami

Maokami Nov 28, 2023 •
edited
Loading

Collaborator

This implicitly requires one to relinearize after a multiplication.
I think this part is the key point. If one always performs relinearization after every multiplication, as @j2kun mentioned, it can be assumed that the size of the input ciphertext is always 2 before multiplication.

I believe SEAL does it that way (https://github.com/microsoft/SEAL/blob/206648d0e4634e5c61dcf9370676630268290b59/CHANGES.md?plain=1#L797), but in OpenFHE, it's possible to perform relinearization after multiple multiplications using an appropriate key.

I may lack expertise in HE, but are there practical use cases where relinearization is performed after several multiplications?

This comment has been minimized.

Sign in to view

Copy link
@asraa

asraa Nov 28, 2023

Collaborator

I agree, in this case the formula works out nicely, but either there should also be a line that says the equal x and y input dimensions should also be 2.

I may lack expertise in HE, but are there practical use cases where relinearization is performed after several multiplications?

Sometimes, if the circuit is, let's say, doing (x_1 * x_2) + (y_1 * y_2) you may was well relinearize after the addition rather than two on each summand (assuming low enough noise). I assume a compiler would be the tool to figure out when based on a noise model.

This comment has been minimized.

Sign in to view

Copy link
@Maokami

Maokami Nov 28, 2023

Collaborator

@asraa Sorry, I intended to mention the scenario where 'consecutive' multiplications are performed, followed by relinearization (where the multiplication depth > 1).

This comment has been minimized.

Sign in to view

Copy link
@asraa

asraa Nov 28, 2023

Collaborator

oh i see! yes, i agree that is really rare (because it also requires sending more relinearization keys to the computing party)

This comment has been minimized.

Sign in to view

Copy link
@asraa

asraa Nov 28, 2023

Collaborator

however, in the first papers of SEAL they used to only have one 3 -> 2 relinearization key, now they allow more relinearization keys to be sent, and assume that the client/server have decided how many to have.

This comment has been minimized.

Sign in to view

Copy link
@Maokami

Maokami Nov 28, 2023 •
edited
Loading

Collaborator

Then I agree that
there should also be a line that says the equal x and y input dimensions should also be 2.

And it requires us to add more checks to Relinearize::verify() (maybe x.getDim() == 3 and out.getDim() ==2 ?)

This comment has been minimized.

Sign in to view

Copy link
@Maokami

Maokami Nov 28, 2023

Collaborator

however, in the first papers of SEAL they used to only have one 3 -> 2 relinearization key, now they allow more relinearization keys to be sent, and assume that the client/server have decided how many to have.

If I understand SEAL code correctly, it seems they only allow 3 -> 2 relin keys, even in recent versions.
https://github.com/microsoft/SEAL/blob/206648d0e4634e5c61dcf9370676630268290b59/native/src/seal/keygenerator.h#L97C32-L97C32

This comment has been minimized.

Sign in to view

Copy link
@asraa

asraa Nov 28, 2023

Collaborator

Ah, nice find! It looks like maybe you could create them in the internal API (but I haven't seen any uses or checked internally).

Either way (updating the formula or restricting the input sizes), perhaps we should add a comment here...
return this->emitOpError() << "output.dim == x.dim + 1 does not hold";
}
return success();
}

LogicalResult Relinearize::verify() {
auto x = this->getX().getType();
auto out = this->getOutput().getType();
if (x.getDim() != this->getFromBasis().size()) {
return this->emitOpError() << "input dimension does not match from_basis";
}
if (out.getDim() != this->getToBasis().size()) {
return this->emitOpError() << "output dimension does not match to_basis";
}
return success();
}

LogicalResult ModulusSwitch::verify() {
auto x = this->getX().getType();
auto rings = x.getRings().getRings().size();
auto to = this->getToLevel();
auto from = this->getFromLevel();
if (to < 0 || to >= from || from >= rings) {
return this->emitOpError() << "invalid levels, should be true: 0 <= " << to
<< " < " << from << " < " << rings;
}
if (x.getLevel().has_value() && x.getLevel().value() != from) {
return this->emitOpError() << "input level does not match from_level";
}
auto outLvl = this->getOutput().getType().getLevel();
if (!outLvl.has_value() || outLvl.value() != to) {
return this->emitOpError()
<< "output level should be specified and match to_level";
}
return success();
}

} // namespace bgv
} // namespace heir
} // namespace mlir

0 comments on commit cac9985

Please sign in to comment.