Keccak Gate

The Keccak gadget is comprised of 3 circuit gates (Xor16, Rot64, and Zero)

Keccak works with 64-bit words. The state is represented using matrix of 64 bit words. Each compression step of Keccak consists of 24 rounds. Let us denote the state matrix with (indexing elements as ), from which we derive further states as follows in each round. Each round then consists of the following 5 steps:

for and is the rotation offset defined for Keccak. The values are in the table below extracted from the Keccak reference

x = 3x = 4x = 0x = 1x = 2
y = 2155231310171
y = 155276363006
y = 0289101190
y = 41207821066253
y = 3211361054515

Design Approach:

The atomic operations are XOR, ROT, NOT, AND. In the sections below, we will describe the gates for these operations. Below are some common approaches followed in their design.

To fit within 15 wires, we first decompose each word into its lower and upper 32-bit components. A gate for an atomic operation works with those 32-bit components at a time.

Before we describe the specific gate design approaches, below are some constraints in the Kimchi framework that dictated those approaches.

  • only 4 lookups per row
  • only first 7 columns are available to the permutation polynomial


It is clear from the definition of the rotation gate that its constraints are complete (meaning that honest instances always satisfy the constraints). It is left to be proven that the proposal is sound. In this section, we will give a proof that as soon as we perform the range checks on the excess and shifted parts of the input, only one possible assignment satisfies the constraints. This means that there is no dishonest instance that can make the constraints pass. We will also give an example where one could find wrong rotation witnesses that would satisfy the constraints if we did not check the range.

Necessity of range checks

First of all, we will illustrate the necessity of range-checks with a simple example. For the sake of readability, we will use some toy field lengths. In particular, let us assume that our words have 4 bits, meaning all of the elements between 0x0 and 0xF. Next, we will be using the native field .

As we will later see, this choice of field lengths is not enough to perform any 4-bit rotation, since the operations in the constraints would overflow the native field. Nonetheless, it will be sufficient for our example where we will only rotate by 1 bit.

Assume we want to rotate the word 0b1101 (meaning 13) by 1 bit to the left. This gives us the rotated word 0b1011 (meaning 11). The excess part of the word is 0b1, whereas the shifted part corresponds to 0b1010. We recall the constraints for the rotation gate:

Applied to our example, this results in the following equations:

We can easily check that the proposed values of the shifted 0b1010=10 and the excess 0b1=1 values satisfy the above constraint because and . Now, the question is: can we find another value for excess and shifted, such that their addition results in an incorrect rotated word?

The answer to this question is yes, due to diophantine equations. We basically want to find such that . The solution to this equation is:

We chose these word and field lengths to better understand the behaviour of the solution. Here, we can see two “classes” of evaluations.

  • If we choose an even , then will have the following shape:

    • Meaning, if then .
  • If on the other hand, we chose an odd , then will have the following shape instead:

    • Meaning, if then .

Thus, possible solutions to the diophantine equation are:

Note that our valid witness is part of that set of solutions, meaning and . Of course, we can also find another dishonest instantiation such as and . Perhaps one could think that we do not need to worry about this case, because the resulting rotation word would be , and if we later use that result as an input to a subsequent gate such as XOR, the value would not fit and at some point the constraint system would complain. Nonetheless, we still have other solutions to worry about, such as or , since they would result in a rotated word that would fit in the word length of 4 bits, yet would be incorrect (not equal to ).

All of the above incorrect solutions differ in one thing: they have different bit lengths. This means that we need to range check the values for the excess and shifted witnesses to make sure they have the correct length.

Sufficiency of range checks

In the following, we will give a proof that performing range checks for these values is not only necessary but also sufficient to prove that the rotation gate is sound. In other words, we will prove there are no two possible solutions of the decomposition constraint that have the correct bit lengths. Now, for the sake of robustness, we will consider 64-bit words and fields with at least twice the bit length of the words (as is our case).

We will proceed by contradiction. Suppose there are two different solutions to the following diophantic equation:

where is a parameter to instantiate the solutions, is the word to be rotated, is the rotation amount, and is the field length.

Then, that means that there are two different solutions, and with at least or . We will show that this is impossible.

If both are solutions to the same equation, then: means that . Moving terms to the left side, we have an equivalent equality: . There are three cases to consider:

  • and : then and this can only happen if . But since , then cannot be smaller than as it was assumed. CONTRADICTION.

  • and : then and this can only happen if . But since , then cannot be smaller than as it was assumed. CONTRADICTION.

  • and : then we have something like .

    • This means for any .
    • According to the assumption, both and . This means, the difference lies anywhere in between the following interval:
    • We plug in this interval to the above equation to obtain the following interval for :
    • We look at this interval from both sides of the inequality: and and we wonder if is at all possible. We rewrite as follows:
    • But this can only happen if , which is impossible since we assume . CONTRADICTION.
  • EOP.