-
Notifications
You must be signed in to change notification settings - Fork 808
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Keccak circuit implementation #268
Conversation
e9c2cec
to
065c930
Compare
Since the state is always carried as an `AssignedCell`, this utility fn helps to dettach the `Cell` from it's value `F`. And this is implemented for N-lenght arrays.
This is the way on which al the configs are implemented. And so, we cannot be using `region + offset` approach in any part of the keccak_circuit. Therefore Xi has been refactored to use a `Layouter` in order to witness it's data.
This makes the implementation of the out-of-circuit primitives for keccak much closer and similar to the inner circuit ones. That makes it a lot more confortable to make tests or work within the codebase.
Co-authored-by: Chih Cheng Liang <chihchengliang@gmail.com>
Adapts the configure fn of `KeccakPermutation` according to: #305
065c930
to
720a44a
Compare
Since the base conversion table is provided outside but the rho one is internal to the permutation, they both require to be loaded from different sources. Co-authored-by: Chih Cheng Liang <chihchengliang@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
First-pass review.
@@ -148,7 +148,7 @@ impl<F: FieldExt> BaseConversionConfig<F> { | |||
region.constrain_equal(input_acc_cell, input_coef_cell)?; | |||
region.constrain_equal(output_acc_cell, output_coef_cell)?; | |||
} else if offset == input_coefs.len() - 1 { | |||
region.constrain_equal(input_acc_cell, input.0)?; | |||
//region.constrain_equal(input_acc_cell, input.0)?; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this meant to be commented out?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is. We reviewed that with @ChihChengLiang and this leads to a Permutation err as we copy from different cells different rounds.
We should maybe look into this a bit more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we need to enable that copy constraint to bind the output of the base conversion. I imagine we now have the flow like the following. The
| ["Mixing result copies and constraints"]
flag(cell) ------(copy)--> computation_pathA ---> resultA(cell) ---(copy)--> | right_side(cell)
neg_flag(cell) --(copy)--> computation_pathB ---> resultB(cell) ---(copy)--> | left_side(cell)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
per offline discussion with @CPerezz, the copy constraint is required, but it might be difficult to enable in this PR. We can enable it in a future PR.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
First pass on gates
Add missing comments, explanations and spelling errors. Co-authored-by: ying tong <yingtong@z.cash>
877f471
to
fcfcda0
Compare
As said by CC: We should split 3 polys here. Otherwise, the prover can witness values not satisfying individual polys but satisfying the summation poly. Proof: let x=flag, y=negated_flag flag_consistency: x + y - 1 bool_constraint for x: x(1-x) bool_constraint for y: y(1-y) summation: x + y - 1 + x(1-x) + y(1-y) = 0 falsifying example: x=2 and y=1 Co-authored-by: Chih Cheng Liang <chihchengliang@gmail.com>
fcfcda0
to
c496844
Compare
The Removing just these two constraints makes the circuit have a much more reasonable extended domain of just x8 bigger. The max degree of 7 is then caused by lookups (which have expressions up to degree 3 as input, but because they are used in the lookup an extra degree of 4 is added with current halo2 with zk), so probably still possible to get it down further with some additional tweaks, but of course will have much less impact than fixing the two constraints above and may end up not being worth it. |
@Brechtpd Nice catch for the performance bottleneck. Do you think using a lookup table check for step2_acc and step3_acc would improve the performance? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM modulo some small suggestions.
Another nitpick: I think we should avoid prefixing variable names with an underscore _
, because that makes the compiler not warn us when these variables are unused.
keccak256/src/circuit.rs
Outdated
// start of the loop. | ||
state = { | ||
// TODO: That could be a Fixed column. | ||
// Witness 1 for the activation flag. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, I think we should make this a Selector.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Found some undeleted comments
89351d0
to
36928a4
Compare
Sorry @ChihChengLiang as mentioned in private, this was the result of pushing some debugging lines that I was not planning to push. I've force-pushed so that the history is clean now. |
This PR implements the entire keccak permutation circuit (No padding) to be used as a gadget or a final circuit.
Resolves: #218
Resolves: #273