Opcode
components work, let’s walk through the implementation of the AddOpcode
component.
Figure 1: The AddOpcode columns
AddOpcode
component. Note that the dst_val
, op0_val
, and op1_val
columns are actually 28 columns each (to support 28 9-bit limbs), but we show them as single columns for brevity.
To reiterate what an Opcode
component does from the Main Components section, it verifies the following:
VerifyInstruction
component.Opcode
component using the flags.op0
, op1
, and dst
computed with the registers and the offsets are correct using the Memory
component.Opcode
component is done correctly.pc
, ap
, fp
) is done correctly using the flags.ADD
opcode here. For item 5, the specs for a valid state transition can be found in Section 4.5 of the Cairo paper.
In this section, we will focus on how item 4 is implemented.
op0
, op1
, and dst
are correctly accessed from the Memory
table, we now check that the addition of two 252-bit integers is done correctly, i.e. op0 + op1 = dst
. As noted in the Felt252 to M31 section, a 252-bit integer is stored as 28 9-bit limbs, so we need to check addition for each of the 28 limbs.
We will incrementally build up to the final constraint.
op0[0] + op1[0] - dst[0]
by 2^9
since this quantity is either 2^9
(if a carry exists) or 0
(if no carry exists). Dividing by 2^9
yields 1
or 0
, respectively. To check that the carry is either 0
or 1
, we add the constraint carry_limb_0 * (carry_limb_0 - 1) = 0
. For the final limb, we simply check that the addition is correct.
P
(i.e., op0 + op1 = dst + P
). To check this, we introduce a witness variable sub_p_bit
, a 1-bit value set to 1 if there is an overflow. Note that since P = 2^251 + 17 * 2^192 + 1
, we only subtract in the three limbs where P
has a non-zero limb: 0
, 22
, 27
.
Now let’s revisit the constraints:
sub_p_bit
is a bit. Then, we subtract sub_p_bit
from the first limb, sub_p_bit * 136
from the 22nd limb, and sub_p_bit * 256
from the 27th limb. (Note that 136
and 256
are the values of P
in the 22nd and 27th limbs, respectively.)
A caveat of this approach is that subtracting sub_p_bit
can introduce an underflow, i.e., (op0[0] + op1[0] - dst[0] - sub_p_bit) / 2^9 = -1
. This means that carry_limb_0
can be -1
as well as 0
or 1
. Thus, we update the constraint for all carries to the following:
carry_limb_1 = (op0[0] + op1[0] - dst[0] - sub_p_bit) / 2^9
would require a dedicated column for carry_limb_1
. Instead, we keep carry_limb_1
as an intermediate value and inline the equation when computing the next carry. For example, the second-limb carry is computed as follows:
2^9
with multiplication by 2^22
, which is equivalent in the M31 field since 2^9
and 2^22
are multiplicative inverses—i.e., 2^9 * 2^22 = 1 mod 2^31 - 1
.
So the final constraint looks like this:
AddOpcode
component: the enabler
column.
As the name suggests, this column enables or disables the constraint for the current row.
It is used to support the dummy rows added to the end of the table to make the number of rows a power of two.
In other words, it is set to 1
for all valid ADD
opcode calls and 0
for all dummy rows.