The exponentiation proof validates entries in the exponentiation circuit, which includes the exponentiation table. Each EXP
opcode performed in a block's transactions is mapped to an exponentiation trace, more specifically these are the intermediate multiplication steps produced while exponentiation by squaring.
For instance, 3 ^ 13 == 1594323 (mod 2^256)
is mapped to the following steps:
3 * 3 = 9
9 * 3 = 27
27 * 27 = 729
729 * 729 = 531441
531441 * 3 = 1594323
Moving on, we refer each of the above multiplication steps as:
a * b + c = d
while validating the equation using a MulAddWordsGadget
where c == 0
.
For a detailed algorithm, please refer the design document.
The exponentiation circuit consists of the following columns:
q_usable
: A selector to indicate whether or not the current row will be used in the circuit's layout.exp_table
: The columns from exponentiation tablemul_gadget
: The columns from a multiplication gadget, responsible for validating that each step within the exponentiation trace was multiplied correctly. For instance, in the above example we would want to verify that729 * 729 == 531441 (mod 2^256)
.parity_check
: The columns from a multiplication gadget, responsible for checking the parity (odd/even) of theexponent
at the specific step of exponentiation trace. Depending on whether theexponent
is odd or even, we calculate theexponent
at the next step.
-
For every row where
is_step == true
, except the last step, validate that:base
MUST be the same across subsequent steps.- Multiplication result
d
from the next row MUST be equal to the first multiplicanda
in the current row. For instance, if we considerrow_0
(531441 * 3 = 1594323
) androw_1
(729 * 729 = 531441
) from the above example,d_1
is531441
anda_0
is also531441
. identifier
MUST be the same across subsequent steps, i.e.identifier::cur_step == identifier::next_step
.
-
For every row, validate that:
exp_table.is_step
MUST be boolean.exp_table.is_last
MUST be boolean.
-
For every row where
is_step == true
, validate that:exponentiation_lo
MUST equalmul_gadget
's multiplication resultd_lo
.exponentiation_hi
MUST equalmul_gadget
's multiplication resultd_hi
.- Since we are only performing multiplication with the equation
a * b + c == d
,c
in themul_gadget
MUST equal0
. - Since we are performing
2 * q + r == exponent
in theparity_check
multiplication gadget,r
is boolean, that is:r_hi
MUST equal0
.r_lo
MUST be boolean.overflow
in theparity_check
MUST equal0
.
- If parity check is
odd
, i.e.parity_check.r_lo == 1
:exponent
MUST reduce by 1, which means:- Low 128 bits of
exponent::next
MUST equal low 128 bits ofexponent::cur - 1
. - High 128 bits of
exponent::next
MUST equal high 128 bits ofexponent::cur
.
- Low 128 bits of
exponent
is odd also means it was a multiplication bybase
operation, that is:- For each limb,
exp_table.base_limb == mul_gadget.b
.
- For each limb,
- If parity check if
even
, i.e.parity_check.r_lo == 0
:exponent
MUST reduce toexponent // 2
, which means:- Low 128 bits of
exponent::cur
MUST equal low 128 bits ofparity_check
's multiplication resultd
.- That is,
exp_table.exponent_lo == parity_check.d_lo
.
- That is,
- High 128 bits of
exponent::cur
MUST equal high 128 bits ofparity_check
's multiplication resultd
.- That is,
exp_table.exponent_hi == parity_check.d_hi
.
- That is,
- Low 128 bits of
exponent::next
MUST equal low 128 bits ofparity_check
's multiplicandq
.- That is,
exp_table.exponent_lo::next == parity_check.q_lo
. We computeq_lo
using the 64-bit limbs ofq
.
- That is,
- High 128 bits of
exponent::next
MUST equal high 128 bits ofparity_check
's multiplicandq
.- That is,
exp_table.exponent_hi::next == parity_check.q_hi
. We computeq_hi
using the 64-bit limbs ofq
.
- That is,
- Low 128 bits of
exponent
is even also means it was a squaring operation, that is:mul_gadget
's multiplicands MUST be equal, or,mul_gadget.a == mul_gadget.b
.
-
For the last step, i.e.
is_last == true
, validate thata * a == a^2 (mod 2^256)
:exponent
MUST equal2
, that is:exp_table.exponent_lo == 2
exp_table.exponent_hi == 0
- Both multiplicand's of the
mul_gadget
, i.e.a
andb
MUST equalbase
of the exponentiation operation, that is:mul_gadget.a == base
mul_gadget.b == base
(for both these cases we equate each 64-bit limb)
Please refer to Exponentiation Circuit Verification.