Binary state machine
The Binary State Machine is one of the six secondary state machines receiving instructions from the Main SM Executor. It is responsible for the execution of all binary operations in the zkProver.
As a secondary state machine, the Binary State Machine has the executor part (the Binary SM Executor) and an internal Binary PIL program, which is a set of verification rules, written in the PIL language. The Binary SM Executor is written in two languages: Javascript and C/C++.
Binary operations on 256-bit strings¶
The zkEVM performs the following binary operations on 256-bit strings:
- The addition operation, denoted by
( ), adds two 256-bit numbers, - The subtraction operation, denoted by
( ), computes the difference between two 256-bit numbers, - The less-than operation, denoted by
( ), checks if a 256-bit number is smaller than another 256-bit number, without considering the signs the numbers, - The signed less-than operation, denoted by
( ), checks if a 256-bit number is smaller than another 256-bit number, but takes into consideration the respective signs of the numbers, - The equal operation, denoted by
( ), checks if two 256-bit numbers are equal, - The AND operation, denoted by
( ), computes the bit-wise “AND” of two numbers, - The OR operation, denoted by
( ), computes the bit-wise “OR” of two numbers, - The XOR operation, denoted by
( ), computes the bit-wise “XOR” of two numbers, - The NOT operation, denoted by
( ), computes the bit-wise “NOT” of a binary number.
Addition and subtraction operations¶
In order to understand how the
Below figure shows these codifications for 3-bit strings but the idea can be easily extended to 256-bit strings.
Adding two strings is performed bit-by-bit using the corresponding carry.
For example, add the 3-bit strings
-
Start with an initial
and add the least significant bits, , so the next carry becomes . -
Next, add the second least-significant bits using the previous carry,
, this time the next carry is . -
Finally, add the most significant bits,
, with the final carry being . -
As a result:
with .
The sum
In other words, the same binary sum can be done for both signed integers and for unsigned integers.
Signed and unsigned ‘Less Than’ operations¶
The operations
When comparing unsigned integers using
For example,
But when comparing signed integers using
-
If the most-significant bits of the two strings being compared is the same, the natural order applies. For example,
. i.e., . Compare with Figure 1 above. -
However, if the most significant bits of strings being compared are different, then the order must be flipped (bigger numbers start with 0). For example,
. i.e., .
Finally, notice that with unsigned integers, there is a caveat since 4 and -4 have the same codification.
AND, OR and XOR operations¶
Consider the bit-wise operations;
The below table depicts the truth tables of
Notice that we do not consider the
The design of Binary SM¶
The Executor of the Binary SM records the trace of each computation in the state machine, and this computational trace is used to prove correctness of computations.
The execution trace is typically in the form of 256-bit strings. And the polynomial constraints, which every correct execution trace must satisfy, are described in a PIL file (or ‘code’).
For the Binary SM, these computations refer to the aforementioned binary operations, and use special codes for each of the operations.
Codes for the binary operations¶
Each operation that the Binary SM checks has an opcode as shown in the table below.
In instances where none of the defined binary operations is carried out, the Binary SM’s operation is considered to be a
Internal byte plookups¶
The Binary SM is internally designed to use Plookups of bytes for all the binary operations.
It uses Plookups that contain all the possible input bytes and output byte combinations,
where
When executing a binary operation between the 256-bit input strings, an execution trace is generated in cycles of
At each step, the corresponding byte-wise operation and any required extra information such as ‘carries’ or auxiliary values, form part of the computation trace.
Additionally, each
Connection with the Main SM¶
The constraint that connects the execution trace of the Main SM with the execution trace of the Binary SM is a Plookup, which is performed at each row of the Binary SM execution trace when the cycle is completed (this is when a register called
The Plookup checks the operation code, the registries for the input and output 256-bit strings, and the final carry.
Operating at byte-level¶
This section provides examples of how the byte-wise operations work.
A
where each
Example 1
If
Addition¶
Here is how the addition operation on two
Observe that adding two bytes
For example, if
In byte-form,
Consider now the process of adding two bytes.
Example 2.
Take for instance,
-
First add the less significant bytes:
-
Then, add the next significant byte,
The previous scheme depicts several cases that need to be treated separately;
-
If
and , then the sum is simply, -
If
but , then does not fit in a single byte. Hence, the sum of and has to be written asfor some byte
. The addition is then computed as follows,
-
If
, then we have that:for some byte
. Then we can write
Consider the following two scenarios:
-
If
, then the sum will take the form:Therefore, the byte decomposition of
is -
If
, then the byte decomposition of is:
Observe that addition of
Subtraction¶
Reducing Subtraction to byte-level turns out to be trickier than Addition case.
Suppose
Observe that
However, we know that the result is
In order to get this result, notice that the operation can be described as follows,
The output byte decomposition is
Nonetheless, it may be necessary to look at more examples so as to better understand how subtraction works at byte-level in a more general sense.
Consider now a subtraction of numbers with
First analyse the first two bytes, as in the previous example,
But now observe that
Observe that the previous example is included in this case.
In general, let
We have two possible cases,
- If
, then provides the corresponding -th byte of the representation of . - If
then we should compute the corresponding -th byte of the representation of as,
However, we need to discuss the last step of our example. Observe that we can not perform the operation
Observe that this is also included in the case when
Less than¶
We want to describe the less than comparator byte-wise. For
Hence, we can not decide with this byte. And the same happens with the second byte, they are both equal to
However, the problem with our setup is that we must start with the less significant byte and climb up to the most significant byte. The strategy will be to use some kind of a carry in order to “carry” the decisions from previous bytes. Let us do an example step by step, now with
we will set up
Henceforth, we should output a
- If
, we set to . If we are at the most significant byte, we output . - If
, we let unchanged in order to maintain the previous decision. If we are at the most significant byte, we output . - If
, we set to . If we are at the most significant byte, we output .
Signed less than¶
In computer science, the most common method of representing signed integers on computers, is called two’s complement. When the most significant bit is a one, the number is signed as negative. The way to express a negative integer
using the two’s complement encoding, because
Hence,
Hence, observe that
We will describe a method to compare signed integers byte-wise. First of all, let us analyze the order among all the signed bytes, in order to understand how to compare them. Once we achieve this, the strategy will be very similar to the previous Less Than.
Let
is the binary representation of
because
- If
and , then . - If
and , then . - If
, the order is the usual one and hence, we already know how to compare and .
Recall that we are processing the bytes of
- First of all, we start comparing
and .
(a) If
(b) Otherwise we set
- For all
, we compare and .
(a) If
(b) If
© Otherwise, we set
- Now, we have to compare the last byte. We follow the described strategy of comparing the signs:
(a) If
(b) If
© If
1. If $a_{31} < b_{31}$, we output a $1$, so $a < b$.
2. If $a_{31} = b_{31}$, we output the previous $\texttt{carry}$, maintaining the last decision.
3. Otherwise, we output a $0$, so $a \not < b$.
Let us exemplify the previous procedure setting
Equality¶
We want to describe the equality comparator byte-wise. For unsigned
Let us compare
We will describe an algorithm in order to proceed processing all the bytes. We will use a carry to mark up when a difference among bytes has
-
First of all, since no differences have been found up to this point, set
equal to . -
Now, compare
and ,
(a) If
(b) If
- When comparing bytes
and for .
(a) If
(b) Hence, if
Bitwise operations¶
We will describe all bitwise operations at once because they are the easiest ones, since we do not need to introduce carries.
Now, the idea is to extend this operation bitwise. That is, if we have the following binary representations of
for
For example, if
The Binary SM in summary¶
The Binary SM has 8 registries, each with a 32-bit Input/Output capacity. i.e., a total of 256 bits.
It carries out binary computations in accordance with instructions from the Main SM Executor.
The binary operations it executes, together with their specific opcodes, are:
-
The common operations; the No-Operation
NOP
, AdditionADD
and SubtractionSUB
. Their corresponding special opcodes are;0
,1
and2
, respectively. -
The Boolean operations;
LT
,GT
,SLT
,SGT
,EQ
andISZERO
. Their special opcodes are,3
,4
,5
,6
and7
, respectively. -
The logical operations;
AND
,OR
,XOR
andNOT
, each with its special opcode;9
,10
,11
and12
, respectively.
Firstly, the Binary SM Executor translates the Binary Actions into the PIL language.
Secondly, it executes the Binary Actions.
And thirdly, it uses the Binary PIL program, to check correct execution of the Binary Actions using Plookup.
Translation to PIL language¶
It builds the constant polynomials, which are generated once-off at the beginning. These are;
- the 4 bits long operation code
P_OPCODE
, - the 1-bit Carry-in
P_CIN
, - the Last-byte
P_LAST
, - the 1 byte input polynomials
P_A
andP_B
, - the 16-bit output polynomial
P_C
, - the 1-bit Carry-out
P_COUT
.
It also creates constants required in the Binary PIL program;
RESET
is used to reset registry values every time the state machine completes a cycle of state transitions,FACTOR
, which is an array of size 8, is used for correct placement of output registry values.
Execution of Binary actions¶
The crux of the Binary SM Executor is in the lines 371 to 636
of sm_binary.js. This is where it executes Binary Actions.
-
It takes the committed polynomials A, B and C, and breaks them into bytes (in little-endian form).
-
It sequentially pushes each triplet of bytes (
freeInA
,freeInB
,freeInC
) into their corresponding registries (ai
,bi
,ci
).
It runs one for-loop for all committed polynomials (A, B, C), over all the bytes of the 8 registries, which are altogether 32 bytes per committed polynomial.
Recall that LATCH_SIZE = REGISTERS_NUM * BYTES_PER_REGISTER
= 8 registries * 4 bytes. It hence amounts to 32 bytes for each committed polynomial.
-
Once the 256-bit LATCH is built, it checks the opcodes and then computes the required binary operations in accordance with the instructions of the Main SM.
-
It also generates the final registries.
The Binary PIL (program)¶
There are two types of inputs to the Binary PIL program: the constant polynomials and the committed polynomials.
The program operates byte-wise to carry out 256-bit Plookup operations.
Each row of the lookup table is a vector of the form; { P_LAST
, P_OPCODE
, P_A
, P_B
, P_CIN
, P_C
, P_COUT
}, consisting of the constant polynomials created by the Binary SM Executor. As seen above,
P_LAST
is the Last-byte,P_OPCODE
is the 4-bit operation code,P_A
andP_B
, are the 1-byte input polynomials,-
P_CIN
is the 1-bit Carry-in, -
P_C
is the 16-bit output polynomial, P_COUT
is the 1-bit Carry-out.
The Binary PIL program takes in byte-size inputs, as in the Binary SM Executor, each 256-bit input committed polynomial is first broken into 32 bytes.
For each of the 32 triplets freeInA
, freeInB
and freeInC
, tallying with the three 256-bit committed polynomials A,B and C, the Binary PIL program,
- Prepares a Plookup input vector of the form; {
last
,opcode
,freeInA
,freeInB
,cIn
,freeInC
,cOut
}, where each element is a byte. - Runs Plookup,
{last,opcode,freeInA,freeInB,cIn,freeInC,cOut} in {P_LAST,P_OPCODE,P_A,P_B,P_CIN,P_C,P_COUT};
- Resets registry values at the end of the 32 cycles using
RESET
, and utilisingFACTOR
for correct placement of values. For e.g.,a0' = a0 * (1 - RESET) + freeInA * FACTOR[0];
Special variables, useCarry
and c0Temp
, are used for managing updates and assignments of values, particularly for Boolean operations, where the output c0
registry value is either TRUE = 1
or FALSE = 0
. Hence the Lines 104 and 105 of code;
Line 104. c0Temp' = c0Temp * (1 - RESET) + freeInC * FACTOR[0];
Line 105. c0' = useCarry * (cOut - c0Temp ) + c0Temp;
For all non-Boolean operations; the default value for useCarry
is zero, making c0' = c0Temp
. The value of c0'
is therefore of the same form as other ci'
update values.
- The output of the Binary PIL program is therefore a report of either
pass
orfail
.
Source code¶
The Polygon zkEVM repository is available on GitHub.
Binary SM Executor: sm_binary.js
Binary SM PIL: binary.pil
Test Vectors: binary_test.js