Binary State Machine
The Binary State Machine (SM) is one of the six secondary state machines receiving instructions, called Binary Actions, from the Main State Machine 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 versions; Javascript and C/C++.
The Polygon Hermez Repo is here https://github.com/0xPolygonHermez
Binary SM Executor: sm_binary.js
Binary SM PIL: binary.pil
Test Vectors: binary_test.js
Binary Operations on 256bit Strings
The zkEVM (zeroknowledge Ethereum Virtual Machine) performs the following binary operations on 256bit strings,
 \(\text{ADD }\) (\(+\)), the addition operation adds two 256bit numbers.
 \(\text{SUB }\) (\(\)), the subtraction operation computes the difference between two 256bit numbers.
 \(\text{LT }\) (\(<\)), the lessthan operation checks if a 256bit number is smaller than another 256bit number, without considering the signs the numbers.
 \(\text{SLT }\) (\(<\)), the signed lessthan operation checks if a 256bit number is smaller than another 256bit number, but takes into consideration the respective signs of the numbers.
 \(\text{EQ }\) (\(=\)), the 'equal' operation checks if two 256bit numbers are equal.
 \(\text{AND }\) (\(\land\)), the operation that computes the bitwise "AND" of two numbers.
 \(\text{OR }\) (\(\lor\)), the operation computes the bitwise "OR" of two numbers.
 \(\text{XOR }\) (\(\oplus\)), the operation computes the bitwise "XOR" of two numbers.
 \(\text{NOT }\) (\(\neg\)), the operation computes the bitwise "NOT" of a binary number.
In order to understand how the \(\text{ADD}\), \(\text{SUB}\), \(\text{LT}\) and \(\text{SLT}\) operations work, one needs to first understand how the zkEVM codes 256bit strings to signed and unsigned integers.
Figure 1 shows these codifications for 3bit strings but the idea can be easily extended to 256bit strings.
Adding two strings is performed bitbybit using the corresponding carry.
For example, add the 3bit strings \(\mathtt{0b001}\) and \(\mathtt{0b101}\), where \(\mathtt{0b}\) means binary,

Start with an initial \(carry=0\) and add the least significant bits,
\(1+1+carry=1+1+0=0\), so the next carry becomes \(carry'=1\).

Next, add the the second leastsignificant bits using the previous carry,
\(0+0+carry = 0+0+1 = 1\), this time the next carry is \(carry'=0\).

Finally, add the most significant bits,
\(0+1+carry=0+1+0=1\), with the final carry being \(carry'=0\).

As a result: \(\mathtt{0b001}+\mathtt{0b101} = \mathtt{0b110}\) with \(carry=0\).
The sum \(\mathtt{0b001}+\mathtt{0b101} = \mathtt{0b110}\), for unsigned integers is \(1+5=6\), while for signed integers encoded with complement to two, this sum is \(1+(3) =(2)\).
In other words, the same binary sum can be done for both signed integers and for unsigned integers.
The operations \(\text{LT}\) and \(\text{SLT}\) are different however.
When comparing unsigned integers (using \(\text{LT}\)), the natural order for comparisons is applied. For example, \(010 < 110\), i.e., \(2 < 6\).
When comparing signed integers (using \(\text{SLT}\)), one must take into account the most significant bit that acts as the sign.

If the mostsignificant bits of the two strings being compared is the same, the the natural order applies. For example, \(101 < 110\). i.e., \(3 < 2\)

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, \(110 < 001\). i.e., \(2 < 1\).
Finally, notice that with unsigned integers, there is a caveat since 4 and 4 have the same codification.
On the other hand, the \(\text{AND}\), \(\text{OR}\), \(\text{XOR}\) and \(\text{NOT}\) operations are bitwise operations, that is to say, the operation is done bitbybit. As a result, there is no carry to be considered when operating a pair of bits. This makes the checks easier to implement for bitwise operations.
Table 1 depicts the truth tables of \(\text{AND}\), \(\text{OR}\) and \(\text{XOR}\) operators, respectively.
Notice that we do not consider the \(\text{NOT}\) operation. This is because the \(\text{NOT}\) operation can be easily implemented with the \(\text{XOR}\) operation, by taking an \(\text{XOR}\) of the 256bit string and \(\texttt{0xff...ff}\).
The Design Of The 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 256bit strings. And the polynomial constraints, that every correct execution trace must satisfy, are described in a PIL file (or 'code').
For the Binary SM, these computations refers to the aforementioned binary operations, and uses special codes for each of the operations.
Codes for the Binary Operations
Each operation that the Binary SM checks has a code as shown in Table 2, below.
In instances where none of the defined binary operations is carried out, the Binary SM's operation is considered to be a \(\text{NOP}\) (No Operation), in which case any code not in the defined list of codes can be used.
\(\textbf{Operation Name}\)  \(\textbf{Mnemonic}\)  \(\textbf{Symbol}\)  \(\textbf{BinOpCode}\) 

\(\text{Addition}\)  \(\mathrm{ADD}\)  \(+\)  \(0\) 
\(\text{Subtraction}\)  \(\mathrm{SUB}\)  \(\)  \(1\) 
\(\text{Less Than}\)  \(\mathrm{LT}\)  \(<\)  \(2\) 
\(\text{Signed Less Than}\)  \(\mathrm{SLT}\)  \(<\)  \(3\) 
\(\text{Equal To}\)  \(\mathrm{EQ}\)  \(=\)  \(4\) 
\(\text{Bitwise AND}\)  \(\mathrm{AND}\)  \(\wedge\)  \(5\) 
\(\text{Bitwise OR}\)  \(\mathrm{OR}\)  \(\vee\)  \(6\) 
\(\text{Bitwise XOR}\)  \(\mathrm{XOR}\)  \(\oplus\)  \(7\) 
\(\text{No Operation}\)  \(\mathrm{NOP}\)  \(\mathrm{NOP}\)  \(\star\) 
Internal Byte Plookups
The Binary SM is internally designed to use plookups of bytes for all the binary operations.
That is, it uses plookups that contain all the possible input bytes and output byte combinations,
where \(\star\) is one of the possible operations.
When executing a binary operation between the 256bit input strings, an execution trace is generated in cycles of \(32\) steps per operation.
At each step, the corresponding bytewise operation and any required extra information, such as 'carries' or auxiliary values, form part of the computation trace.
Additionally, each \(256\)bit string (the two inputs and the output) are expressed using \(8\) registers of \(32\)bits.
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 \(\texttt{RESET}\) is 1).
The Plookup checks the operation code, the registries for the input and output 256bit strings, and the final carry.
Operating At ByteLevel
This section provides examples of how the bytewise operations work.
A \(256\)bit integer \(\mathbf{a}\) is herein denoted in vector form as \((a_{31}, \dots, a_1, a_0)\) to indicate that, $$ \mathbf{a} = a_{31}\cdot (2^8)^{31} + a_{30}\cdot (2^8)^{30} + \cdots + a_1\cdot2^8 + a_0 = \sum_{i = {31}}^{0} a_i \cdot (2^8)^i, $$ where each \(a_i\) is a byte that can take values between \(0\) and \(2^8  1\).
Example 1.
If \(\mathbf{a} = 29967\), its byte decomposition can be written as \(\mathbf{a} = (\mathtt{0x75}, \mathtt{0x0F})\), because \(\mathbf{a} = 29967 = 117 \cdot 2^8 + 15\), and in hexadecimal, \(117 \mapsto \mathtt{0x75}\) and \(15 \mapsto \mathtt{0x0F}\).
Addition
Here is how the addition operation on two \(256\)bit numbers is reduced to a bytebybyte addition, and thus ready to use the bytewise Plookup table.
Observe that adding two bytes \(a\) and \(b\) (i.e., \(a\) and \(b\) are members of the set \([0, 2^81]\)), may result in a sum \(c\) which cannot be expressed as a single byte.
For example, if \(a = \mathtt{0xFF}\) and \(b = \mathtt{0x01}\), then, $$ a + b = \mathtt{0xFF} + \mathtt{0x01} = \mathtt{0x100}. $$ In byteform, \(c=\mathtt{0x00}\) and with \(carry'=1\). This carry has to be taken care of when dealing with bytes.
Consider now the process of adding two bytes.
Example 2.
Take for instance, \(\mathbf{a} = (a_1, a_0) = (\mathtt{0xFF}, \mathtt{0x01})\) and \(\mathbf{b} = (b_1, b_0) = (\mathtt{0xF0}, \mathtt{0xFF})\).
 First add the less significant bytes:
 Then, add the next significant byte,
The previous example shows is scheme depicts several cases that need to be treated separately;
 If \(a_1 + b_1 < 2^8\) and \(a_2 + b_2 < 2^8\), then the sum \(\mathbf{a} + \mathbf{b}\) is simply,
 If \(a_1 + b_1 < 2^8\) but \(a_2 + b_2 \geq 2^8\), then \(a_2 + b_2\) does not fit in a single byte. Hence, the sum of \(a_2\) and \(b_2\) has to be written as,
for some byte \(c_2\). The addition \(\mathbf{a} + \mathbf{b}\) is then computed as follows, $$ \mathbf{a} + \mathbf{b} = (1, c_2, a_1 + b_1). $$
 If \(a_1 + b_1 \geq 2^8\), then we have that:
for some byte \(c_1\). Then we can write, $$ \mathbf{a} + \mathbf{b} = (a_2 + b_2 + 1) \cdot 2^8 + c_1. $$
Consider the following two scenarios:
(a) If \(a_2 + b_2 + 1 \geq 2^8\), then the sum will take the form: $$ a_2 + b_2 + 1 = 1 \cdot 2^8 + c_2. $$ Therefore, the byte decomposition of \(\mathbf{a} + \mathbf{b}\) is, $$ \mathbf{a} + \mathbf{b} = (1, c_2, c_1). $$ (b) If \(a_2 + b_2 + 1 < 2^8\), then the byte decomposition of \(\mathbf{a} + \mathbf{b}\) is: $$ \mathbf{a} + \mathbf{b} = (c_2, c_1). $$ Observe that addition of \(256\)bit numbers can be reduced to additions at bytelevel by operating through the previous cases in an iterative manner.
Subtraction
Reducing Subtraction to bytelevel turns out to be trickier than Addition case.
Suppose \(\mathbf{a} = \mathtt{0x0101}\) and \(\mathbf{b} = \mathtt{0x00FF}\).
Observe that \(\mathtt{0xFF}\) cannot be subtracted from \(\mathtt{0x01}\) because \(\mathtt{0xFF} > \mathtt{0x01}\).
However, we know that the result is \(\mathbf{a}  \mathbf{b} = \mathbf{c} = \mathtt{0x0002}\).
In order to get this result, notice that the operation can be described as follows,
The output byte decomposition is \(\mathbf{a} = (c_1, c_0) = (\mathtt{0x00}, \mathtt{0x02})\).
Nonetheless, it may be necessary to look at more examples so as to better understand how subtraction works at bytelevel in a more general sense.
Consider now subtraction of numbers with \(3\) bytes. Say, \(a = \mathtt{0x0001FE}\) and \(b = \mathtt{0xFEFFFF}\).
First analyse the first two bytes, as in the previous example,
But now observe that \(\mathtt{0x01}  \mathtt{0xFF}  \mathtt{0x01}\) is also a negative value. Hence, there is a need to repeat the strategy and keep a carry to the next byte,
Observe that the previous example is included in this case.
In general, let \(a = (a_i)_i\) and \(b = (b_i)_i\), with \(a_i, b_i\) bytes, be the byte representations of \(a\) and \(b\). Instead of checking if we can perform the subtraction \(a_i  b_i\) for some bytes \(i\), we are checking if \(a_i  b_i  \texttt{carry} \geq 0\). Equivalently, we are checking if \(a_i  \texttt{carry} \geq b_i\). The previous case can be recovered by setting \(\texttt{carry} = 1\) and the first case corresponds to setting \(\mathtt{carry = 0}\).
We have two possible cases,
 If \(a_i  \texttt{carry} \geq b_i\), then \(a_i  b_i  \texttt{carry}\) provides the corresponding \(i\)th byte of the representation of \(a  b\).
 If \(a_i  \texttt{carry} < b_i\) then we should compute the corresponding \(i\)th byte of the representation of \(a  b\) as,
However, we need to discuss the last step of our example. Observe that we can not perform the operation \(\mathtt{0x00}  \mathtt{0xFE}  \mathtt{0x01}\) since it corresponds to a negative value. But as we are working with unsigned integers, we will do the two's complement and set the last byte to, $$ 2^8  \mathtt{0xFE} + \mathtt{0x00}  \mathtt{0x01} = 255  \mathtt{0xFE} + \mathtt{0x00}  \mathtt{0x01} + 1 = 255  b_3 + a_3  \texttt{carry} + 1. $$
Observe that this is also included in the case when \(a_i  \texttt{carry} < b_i\), so we must not treat the last bit in a different manner. To end up with our example, we get the following byte representation of \(a  b\), $$ c = (\mathtt{0x01}, \mathtt{0x01}, \mathtt{0xFF}) = \mathtt{0x01} \cdot 2^{16} + \mathtt{0x01} \cdot 2^8 + \mathtt{0xFF}. $$
Less Than
We want to describe the less than comparator bytewise. For \(256\)bits integers, the operation \(<\) will output \(c = 1\) if \(a < b\) and \(c = 0\) otherwise. As we are working in the natural integers order, the most significant byte decide and, if they are equal, we should consider the previous one until we can decide. Let us propose the example with \(a = \mathtt{0xFF AE 09}\) and \(b = \mathtt{0x FF AE 02}\). We know that \(a > b\). Why? We should start at the most significant byte. We know that $$ a \mathtt{>> 16} = \mathtt{0x FF} = \mathtt{0x FF} = b \mathtt{>> 16}. $$
Hence, we can not decide with this byte. An the same happens with the second byte, they are both equal to \(\mathtt{0x AE}\). Hence, the less significant byte decides, $$ \mathtt{0x 09} > \mathtt{0x 02}. $$
However, the problem with our set up 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 \(a = \mathtt{0x FF AA 02}\) and \(b = \mathtt{0x 01 AA 09}\). First of all, we will compare the less significant bytes. Since $$ \mathtt{0x 02} < \mathtt{0x 09}, $$ we will set up \(\mathtt{carry} = 1\). We will carry this decision until we finish to process all bytes or, alternatively, we should change to the complementary decision. Therefore, since the next two bytes are equal and we are not at the end, we maintain \(\mathtt{carry}\) to \(1\). The previous step is the last one. We compare the most significant bytes, $$ \mathtt{0x FF} \not < \mathtt{0x 01}. $$
Henceforth, we should output a \(0\), independently to the previous carry decision. But, let us suppose now that \(b = \mathtt{0x FF AA 09}\). Then, in this last step, we should output a \(1\), since \(a < b\). The idea is that, in the last step, if both bytes are equal, we should output the decision carry \(\mathtt{carry}\). In general, in the step \(i\), comparing bytes \(a_i\) and \(b_i\), we have \(3\) cases,
 If \(a_i < b_i\), we set \(\mathtt{carry}\) to \(1\). If we are at the most significant byte, we output \(1\).
 If \(a_i = b_i\), we let \(\mathtt{carry}\) unchanged in order to maintain the previous decision. If we are at the most significant byte, we output \(\mathtt{carry}\).
 If \(a_i > b_i\), we set \(\mathtt{carry}\) to \(0\). If we are at the most significant byte, we output \(0\).
Signed Less Than
In computer science, the most common method of representing signed integers on computers, is called \textbf{two's complement}. When the most significant bit is a one, the number is signed as negative. The way to express a negative integer \(x\) into two's complement form is chosen so that, among integers of the same sign, the lexicographical order is maintained. That is, if \(a < b\) are signed integers of the same sign, then its two's complement representations preserve the same order. This will not be true if the signs are different. For example, it is not surprising that $$ 000\dots0 > 111\dots1 $$ using the two's complement encoding, because \(111\dots1\) is negative and \(000\dots0\) is positive. The two's complement form of negative integer \(x\) in a \(N\)bits system is the binary representation of \(2^N  x\). For example, let \(x = 1\) and \(N = 4\). Then, $$ 10000  0001 = 1111. $$ Hence, \(1 = 1111\) in this representation. It is easy to see that \(2 = 1110\) because $$ 10000  0010 = 1110. $$
Hence, observe that \(1 > 2\) because \(1111 > 1110\) and conversely: the order is preserved for integers of the same sign.
We will describe a method to compare signed integers bytewise. 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 \(a = (a_{31}, a_{30}, \dots, a_0)\) and \(b = (b_{31}, b_{30}, \dots, b_0)\) be the byterepresentation of the 256bits unsigned integers \(a\) and \(b\). We will define \(\texttt{sgn}(a) = a_{31, 7}\), where $$ a_{31} = \sum_{i = 0}^7 a_{31, i} \cdot 2^i $$ is the binary representation of \(a_{31}\). That is, \(\texttt{sgn}(a)\) is the most significant bit of \(a\) or, equivalently, the "sign" of \(a\). In a similar way, we define \(\texttt{sgn}(b)\). Observe that it is easy to compare \(a\) and \(b\) if \(\texttt{sgn}(a) \neq \texttt{sgn}(b)\). For example, $$ a = \mathtt{0b11111111} = \mathtt{0xFF} < \mathtt{0x00} = \mathtt{0b00000000} = b $$ because \(\texttt{sgn}(a) > \texttt{sgn}(b)\) i.e. \(a\) is negative and \(b\) is positive. If \(\texttt{sgn}(a) \neq \texttt{sgn}(b)\), we can simply compare \(a\) and \(b\) using the same strategy as before, because the natural lexicographic order is preserved in this case. Then, we have the following cases when comparing \(a\) and \(b\):
 If \(\texttt{sgn}(a) = 1\) and \(\texttt{sgn}(b) = 0\), then \(a < b\).
 If \(\texttt{sgn}(a) = 0\) and \(\texttt{sgn}(b) = 1\), then \(a > b\).
 If \(\texttt{sgn}(a) = \texttt{sgn}(b)\), the order is the usual one and hence, we already know how to compare \(a\) and \(b\).
Recall that we are processing the bytes of \(a\) and \(b\) from the less significant bytes to the most significant bytes. Hence, we need to adapt our strategy following this order. The strategy will be almost the same than in the unsigned operation.
 First of all, we start comparing \(a_0\) and \(b_0\).
(a) If \(a_0 < b_0\), we set \(\texttt{carry} = 1\).
(b) Otherwise we set \(\texttt{carry} = 0\).
 For all \(0 < i < 31\), we compare \(a_i\) and \(b_i\).
(a) If \(a_i < b_i\), we set \(\texttt{carry} = 1\).
(b) If \(a_i = b_i\), we leave \(\texttt{carry}\) unchanged from the previous step.
(c) Otherwise, we set \(\texttt{carry} = 0\).
 Now, we have to compare the last byte. We follow the described strategy of comparing the signs:
(a) If \(\texttt{sgn}(a) > \texttt{sgn}(b)\), we output a \(1\), so \(a < b\).
(b) If \(\texttt{sgn}(a) < \texttt{sgn}(b)\), we output a \(0\), so \(a < b\).
(c) If \(\texttt{sgn}(a) = \texttt{sgn}(b)\), we compare the last bytes \(a_{31}\) and \(b_{31}\) in the same way we have compare the previous bytes. We output \(0\) or \(1\) accordingly.
(i) If \(a_{31} < b_{31}\), we output a \(1\), so \(a < b\).
(ii) If \(a_{31} = b_{31}\), we output the previous \(\texttt{carry}\), maintaining the last decision.
(iii) Otherwise, we output a \(0\), so \(a \not < b\).
Let us exemplify the previous procedure setting \(a = \mathtt{0xFF FF FF 00}\) and \(b = \mathtt{0x00 FF FF FF}\). We know that \(a < b\), so we should output a \(1\). Observe that the less significant byte of \(a\) is leaser than the less significant byte of \(b\). Hence, we should put \(\texttt{carry}\) equal to \(1\). The next two bytes of \(a\) and \(b\) are both equal to \(\mathtt{0xFF FF}\), therefore we maintain \(\texttt{carry}\) unchanged equal to \(1\). However, since \(a\) is negative and \(b\) is positive, we should change the decision and output a \(1\), independently of the \(\texttt{carry}\).
Equality
We want to describe the equality comparator bytewise. For unsigned \(256\)bits integers, the operation \(=\) will output \(c = 1\) if \(a = b\) and \(c = 0\) otherwise. This operation is very simple to describe bytewise, since \(a = b\) if and only if all its bytes coincide.
Let us compare \(a = \mathtt{0xFF 00 a0 10}\) and \(b = \mathtt{0xFF 00 00 10}\) bytewise. Observe that the first byte is the same \(\mathtt{0x10}\), however the next byte are different \(\mathtt{0xa0} \neq \mathtt{0x00}\). Hence, we can finish here and state that \(a \neq b\).
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 \(\textbf{not}\) been found (i.e. if \(\texttt{carry}\) reach \(0\), then \(a\) and \(b\) should differ). Hence, the algorithm to compare two \(32\)bytes integers \(a = (a_{31}, a_{30}, \dots, a_{0})\) and \(b = (b_{31}, b_{30}, \dots, b_0)\) is the following:

First of all, since no differences have been found up to this point, set \(\texttt{carry}\) equal to \(1\).

Now, compare \(a_0\) and \(b_0\),
(a) If \(a_0\) and \(b_0\) are equal, then leave \(\texttt{carry}\) unchanged equal to \(1\).
(b) If \(a_0 \neq b_0\), then set \(\texttt{carry}\) equal to \(0\), which will imply that \(a \neq b\).
 When comparing bytes \(a_i\) and \(b_i\) for \(0 < i \leq 31\).
(a) If \(a_i = b_i \textbf{ and } \texttt{carry} = 1\), we should leave \(\texttt{carry}\) unchanged and, if \(i = 31\), we should output a \(1\) because \(a = b\). The reason of demanding \(\texttt{carry} = 1\) in the enter condition is because we should ensure that, if \(\texttt{carry} = 0\) in a previous step, we must never enter to this block and change the nonequality decision. This is because if \(a_i \neq b_i\) for some \(i\), then \(a \neq b\).
(b) Hence, if \(a_i \neq b_i\), we should set \(\texttt{carry} = 0\) and output a \(0\) if \(i = 31\).
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 \(a = (a_{31}, a_{30}, \dots, a_{0})\) and \(a = (b_{31}, b_{30}, \dots, b_{0})\) where \(a_i, b_i \in \{0, 1\}\), then we define,
for \(\star\) being \(\land, \lor\) or \(\oplus\).
For example, if \(a = \mathtt{0xCB} = \mathtt{0b11001011}\) and \(b = \mathtt{0xEA} = \mathtt{0b11101010}\) then,
The Binary SM In Summary
The Binary SM has 8 registries, each with an 32bit 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 NoOperation
NOP
, AdditionADD
and SubtractionSUB
. Their corresponding special opcodes are;0
,1
and2
, respectively.  The Boolean operations; \(\text{Less Than }\)
LT
, \(\text{Greater Than }\)GT
, \(\text{Signed Less Than }\)SLT
, \(\text{Signed Greater Than }\)SGT
, \(\text{Equal }\)EQ
and \(\text{IsZero }\)ISZERO
. 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.
The Nutshell
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 binary.pil, to check correct execution of the Binary Actions using Plookup.
Translation to PIL Language
It builds the constant polynomials, which are generated onceoff at the beginning. These are;
 the 4 bits long operation code
P_OPCODE
,  the 1bit Carryin
P_CIN
,  the Lastbyte
P_LAST
,  the 1 byte input polynomials
P_A
andP_B
,  the 16bit output polynomial
P_C
,  the 1bit Carryout
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, breaks them into bytes (in littleendian form).

It sequentially pushes each triplet of bytes (
freeInA
,freeInB
,freeInC
) into their corresponding registries (ai
,bi
,ci
).
i.e., It runs one forloop 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 256bit 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 bytewise to carry out 256bit 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 Lastbyte,P_OPCODE
is the 4bit operation code,P_A
andP_B
, are the 1byte input polynomials,
P_CIN
is the 1bit Carryin, 
P_C
is the 16bit output polynomial, P_COUT
is the 1bit Carryout.
The Binary PIL program takes in bytesize inputs, as in the Binary SM Executor, each 256bit input committed polynomial is first broken into 32 bytes.
For each of the 32 triplets freeInA
, freeInB
and freeInC
, tallying with the three 256bit 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 nonBoolean 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
.