From ae0375fc6d587eb11f1bb0710536c0edefb82b2a Mon Sep 17 00:00:00 2001 From: Richord Date: Tue, 17 Jan 2023 10:07:34 -0800 Subject: [PATCH 1/7] added padding advice column --- specs/exp-proof.md | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/specs/exp-proof.md b/specs/exp-proof.md index effd7bad9..b3ab663ad 100644 --- a/specs/exp-proof.md +++ b/specs/exp-proof.md @@ -26,10 +26,11 @@ The exponentiation circuit consists of the following columns: 2. `exp_table`: The columns from [exponentiation table](./tables.md#exponentiation-table) 3. `mul_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 that `729 * 729 == 531441 (mod 2^256)`. 4. `parity_check`: The columns from a multiplication gadget, responsible for checking the parity (odd/even) of the `exponent` at the specific step of exponentiation trace. Depending on whether the `exponent` is odd or even, we calculate the `exponent` at the next step. +5. `padding`: An advice column to indicate whether or not the current row is a padding row. ## Circuit Constraints -- For every row where `is_step == true`, except the last step, validate that: +- For every row where `is_step == true` and `padding == false`, 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 multiplicand `a` in the current row. For instance, if we consider `row_0` (`531441 * 3 = 1594323`) and `row_1` (`729 * 729 = 531441`) from the above example, `d_1` is `531441` and `a_0` is also `531441`. - `identifier` MUST be the same across subsequent steps, i.e. `identifier::cur_step == identifier::next_step`. @@ -38,7 +39,7 @@ The exponentiation circuit consists of the following columns: - `exp_table.is_step` MUST be boolean. - `exp_table.is_last` MUST be boolean. -- For every row where `is_step == true`, validate that: +- For every row where `is_step == true` and `padding == false`, validate that: - `exponentiation_lo` MUST equal `mul_gadget`'s multiplication result `d_lo`. - `exponentiation_hi` MUST equal `mul_gadget`'s multiplication result `d_hi`. - Since we are only performing multiplication with the equation `a * b + c == d`, `c` in the `mul_gadget` MUST equal `0`. @@ -71,6 +72,11 @@ The exponentiation circuit consists of the following columns: - Both multiplicand's of the `mul_gadget`, i.e. `a` and `b` MUST equal `base` of the exponentiation operation, that is: - `mul_gadget.a == base` - `mul_gadget.b == base` (for both these cases we equate each 64-bit limb) +- For every row where `padding == true`, validate that: + - next row is also `padding == true` + - all other columns are set to 0 + + ## Code From e6e2232f74eaebfbd108d7d98bd506052e72112f Mon Sep 17 00:00:00 2001 From: Richard Zhang Date: Thu, 19 Jan 2023 17:59:02 -0800 Subject: [PATCH 2/7] added python spec code and added is_final col --- specs/exp-proof.md | 3 +- src/zkevm_specs/evm/table.py | 2 ++ src/zkevm_specs/evm/typing.py | 6 +++- src/zkevm_specs/exp_circuit.py | 53 +++++++++++++++++++++++++--------- 4 files changed, 49 insertions(+), 15 deletions(-) diff --git a/specs/exp-proof.md b/specs/exp-proof.md index b3ab663ad..7ee0713ec 100644 --- a/specs/exp-proof.md +++ b/specs/exp-proof.md @@ -27,6 +27,7 @@ The exponentiation circuit consists of the following columns: 3. `mul_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 that `729 * 729 == 531441 (mod 2^256)`. 4. `parity_check`: The columns from a multiplication gadget, responsible for checking the parity (odd/even) of the `exponent` at the specific step of exponentiation trace. Depending on whether the `exponent` is odd or even, we calculate the `exponent` at the next step. 5. `padding`: An advice column to indicate whether or not the current row is a padding row. +6. `is_final`: An advice column to indicate whether or not the current row is the last row in the circuit. ## Circuit Constraints @@ -72,7 +73,7 @@ The exponentiation circuit consists of the following columns: - Both multiplicand's of the `mul_gadget`, i.e. `a` and `b` MUST equal `base` of the exponentiation operation, that is: - `mul_gadget.a == base` - `mul_gadget.b == base` (for both these cases we equate each 64-bit limb) -- For every row where `padding == true`, validate that: +- For every row where `padding == true` and `is_final == false`, validate that: - next row is also `padding == true` - all other columns are set to 0 diff --git a/src/zkevm_specs/evm/table.py b/src/zkevm_specs/evm/table.py index 5d2627b2f..a8f9d8ce6 100644 --- a/src/zkevm_specs/evm/table.py +++ b/src/zkevm_specs/evm/table.py @@ -480,6 +480,8 @@ class KeccakTableRow(TableRow): @dataclass class ExpCircuitRow(TableRow): q_usable: FQ + padding: FQ + is_final: FQ # columns from the exponentiation table is_step: FQ identifier: FQ # rw_counter diff --git a/src/zkevm_specs/evm/typing.py b/src/zkevm_specs/evm/typing.py index cec6dc81b..f0df5c357 100644 --- a/src/zkevm_specs/evm/typing.py +++ b/src/zkevm_specs/evm/typing.py @@ -819,7 +819,9 @@ def _append_steps( def _append_padding_row(self, identifier: IntOrFQ): self.rows.append( ExpCircuitRow( - q_usable=FQ.zero(), + q_usable = FQ.one(), + padding = FQ.one(), + is_final = FQ.one(), is_step=FQ.zero(), identifier=FQ(identifier), is_last=FQ.zero(), @@ -852,6 +854,8 @@ def _append_step( self.rows.append( ExpCircuitRow( q_usable=FQ.one(), + padding = FQ.zero(), + is_final = FQ.zero(), is_step=FQ.one(), identifier=FQ(identifier), is_last=FQ(is_last), diff --git a/src/zkevm_specs/exp_circuit.py b/src/zkevm_specs/exp_circuit.py index ebe3941bc..5d22d2bc4 100644 --- a/src/zkevm_specs/exp_circuit.py +++ b/src/zkevm_specs/exp_circuit.py @@ -13,8 +13,8 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): - # for every step except the last - with cs.condition(rows[0].is_step * (1 - rows[0].is_last)) as cs: + # for every non-padded step except the last + with cs.condition(rows[0].is_step * (1 - rows[0].is_last) * (1 - rows[0].padding)) as cs: # base is the same across rows. cs.constrain_equal(rows[0].base, rows[1].base) # multiplication result from the "next" row `d` must be used as @@ -23,15 +23,12 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): # identifier does not change over the steps of an exponentiation trace. cs.constrain_equal(rows[0].identifier, rows[1].identifier) - # for every step - with cs.condition(rows[0].is_step) as cs: + # for every non-padded step + with cs.condition(rows[0].is_step * (1 - rows[0].padding)) as cs: # is_last is boolean. cs.constrain_bool(rows[0].is_last) # remainder (r), i.e. odd/even parity of exponent is boolean. cs.constrain_bool(rows[0].r) - # is_last == 1 is followed by unusable row. - # is_last == 0 is following by usable row. - cs.constrain_equal(rows[0].is_last, (1 - rows[1].q_usable)) # multiplication is assigned correctly _overflow, carry_lo_hi, additional_constraints = mul_add_words( rows[0].a, rows[0].b, rows[0].c, rows[0].d @@ -53,8 +50,8 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): cs.constrain_equal(additional_constraints[0][0], additional_constraints[0][1]) cs.constrain_equal(additional_constraints[1][0], additional_constraints[1][1]) - # for all steps (except the last), where exponent is odd - with cs.condition(rows[0].is_step * (1 - rows[0].is_last) * rows[0].r.expr()) as cs: + # for all non-padded steps (except the last), where exponent is odd + with cs.condition(rows[0].is_step * (1 - rows[0].is_last) * rows[0].r.expr() * (1 - rows[0].padding)) as cs: # exponent::next == exponent::cur - 1 cur_lo, cur_hi = word_to_lo_hi(rows[0].exponent) next_lo, next_hi = word_to_lo_hi(rows[1].exponent) @@ -65,8 +62,8 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): # b == base cs.constrain_equal(rows[0].base, rows[0].b) - # for all steps (except the last), where exponent is even - with cs.condition(rows[0].is_step * (1 - rows[0].is_last) * (1 - rows[0].r.expr())) as cs: + # for all non-padded steps (except the last), where exponent is even + with cs.condition(rows[0].is_step * (1 - rows[0].is_last) * (1 - rows[0].r.expr()) * (1 - rows[0].padding)) as cs: # exponent::next == exponent::cur / 2 cur_lo, cur_hi = word_to_lo_hi(rows[0].exponent) next_lo, next_hi = word_to_lo_hi(rows[1].exponent) @@ -77,8 +74,8 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): # a == b cs.constrain_equal(rows[0].a, rows[0].b) - # for the last step - with cs.condition(rows[0].is_last) as cs: + # for the last non-padded step + with cs.condition(rows[0].is_last * (1 - rows[0].padding)) as cs: # exponent == 2 exponent_lo, exponent_hi = word_to_lo_hi(rows[0].exponent) cs.constrain_equal(exponent_lo, FQ(2)) @@ -87,6 +84,36 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): cs.constrain_equal(rows[0].base, rows[0].a) # b == base cs.constrain_equal(rows[0].base, rows[0].b) + # followed by padding + cs.constrain_equal(rows[1].padding, FQ(1)) + + # for padding + with cs.condition(rows[0].padding * (1 - rows[0].is_final)) as cs: + # padding::next == padding::cur + cs.constrain_equal(rows[1].padding, rows[0].padding) + # is_step == 0 + cs.constrain_zero(rows[0].is_step) + # is_last == 0 + cs.constrain_zero(rows[0].is_last) + # base == 0 + cs.constrain_zero(rows[0].base) + # exponent == 0 + cs.constrain_zero(rows[0].exponent) + # exponentiation == 0 + cs.constrain_zero(rows[0].exponentiation) + # a == 0 + cs.constrain_zero(rows[0].a) + # b == 0 + cs.constrain_zero(rows[0].b) + # c == 0 + cs.constrain_zero(rows[0].c) + # d == 0 + cs.constrain_zero(rows[0].d) + # q == 0 + cs.constrain_zero(rows[0].q) + # r == 0 + cs.constrain_zero(rows[0].r) + def verify_exp_circuit(exp_circuit: ExpCircuit): From 953d537f0cf645e84f4b5f451289d5696696c481 Mon Sep 17 00:00:00 2001 From: Richard Zhang Date: Sun, 22 Jan 2023 12:56:34 -0800 Subject: [PATCH 3/7] fixed lint errors --- src/zkevm_specs/evm/typing.py | 10 +++++----- src/zkevm_specs/exp_circuit.py | 9 ++++++--- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/zkevm_specs/evm/typing.py b/src/zkevm_specs/evm/typing.py index f0df5c357..4ca1204bc 100644 --- a/src/zkevm_specs/evm/typing.py +++ b/src/zkevm_specs/evm/typing.py @@ -819,9 +819,9 @@ def _append_steps( def _append_padding_row(self, identifier: IntOrFQ): self.rows.append( ExpCircuitRow( - q_usable = FQ.one(), - padding = FQ.one(), - is_final = FQ.one(), + q_usable=FQ.one(), + padding=FQ.one(), + is_final=FQ.one(), is_step=FQ.zero(), identifier=FQ(identifier), is_last=FQ.zero(), @@ -854,8 +854,8 @@ def _append_step( self.rows.append( ExpCircuitRow( q_usable=FQ.one(), - padding = FQ.zero(), - is_final = FQ.zero(), + padding=FQ.zero(), + is_final=FQ.zero(), is_step=FQ.one(), identifier=FQ(identifier), is_last=FQ(is_last), diff --git a/src/zkevm_specs/exp_circuit.py b/src/zkevm_specs/exp_circuit.py index 5d22d2bc4..53c9d4b7f 100644 --- a/src/zkevm_specs/exp_circuit.py +++ b/src/zkevm_specs/exp_circuit.py @@ -51,7 +51,9 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): cs.constrain_equal(additional_constraints[1][0], additional_constraints[1][1]) # for all non-padded steps (except the last), where exponent is odd - with cs.condition(rows[0].is_step * (1 - rows[0].is_last) * rows[0].r.expr() * (1 - rows[0].padding)) as cs: + with cs.condition( + rows[0].is_step * (1 - rows[0].is_last) * rows[0].r.expr() * (1 - rows[0].padding) + ) as cs: # exponent::next == exponent::cur - 1 cur_lo, cur_hi = word_to_lo_hi(rows[0].exponent) next_lo, next_hi = word_to_lo_hi(rows[1].exponent) @@ -63,7 +65,9 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): cs.constrain_equal(rows[0].base, rows[0].b) # for all non-padded steps (except the last), where exponent is even - with cs.condition(rows[0].is_step * (1 - rows[0].is_last) * (1 - rows[0].r.expr()) * (1 - rows[0].padding)) as cs: + with cs.condition( + rows[0].is_step * (1 - rows[0].is_last) * (1 - rows[0].r.expr()) * (1 - rows[0].padding) + ) as cs: # exponent::next == exponent::cur / 2 cur_lo, cur_hi = word_to_lo_hi(rows[0].exponent) next_lo, next_hi = word_to_lo_hi(rows[1].exponent) @@ -115,7 +119,6 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): cs.constrain_zero(rows[0].r) - def verify_exp_circuit(exp_circuit: ExpCircuit): cs = ConstraintSystem() exp_table = exp_circuit.table() From 735cc398aeecdc08d746676db367437cefaef3b4 Mon Sep 17 00:00:00 2001 From: Richard Zhang Date: Wed, 25 Jan 2023 09:24:08 -0800 Subject: [PATCH 4/7] added padding 1^1 --- specs/exp-proof.md | 9 ++---- src/zkevm_specs/evm/table.py | 2 -- src/zkevm_specs/evm/typing.py | 40 ++++++++++++------------- src/zkevm_specs/exp_circuit.py | 53 +++++++--------------------------- 4 files changed, 32 insertions(+), 72 deletions(-) diff --git a/specs/exp-proof.md b/specs/exp-proof.md index 7ee0713ec..e22b0ca85 100644 --- a/specs/exp-proof.md +++ b/specs/exp-proof.md @@ -26,12 +26,10 @@ The exponentiation circuit consists of the following columns: 2. `exp_table`: The columns from [exponentiation table](./tables.md#exponentiation-table) 3. `mul_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 that `729 * 729 == 531441 (mod 2^256)`. 4. `parity_check`: The columns from a multiplication gadget, responsible for checking the parity (odd/even) of the `exponent` at the specific step of exponentiation trace. Depending on whether the `exponent` is odd or even, we calculate the `exponent` at the next step. -5. `padding`: An advice column to indicate whether or not the current row is a padding row. -6. `is_final`: An advice column to indicate whether or not the current row is the last row in the circuit. ## Circuit Constraints -- For every row where `is_step == true` and `padding == false`, except the last step, validate that: +- 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 multiplicand `a` in the current row. For instance, if we consider `row_0` (`531441 * 3 = 1594323`) and `row_1` (`729 * 729 = 531441`) from the above example, `d_1` is `531441` and `a_0` is also `531441`. - `identifier` MUST be the same across subsequent steps, i.e. `identifier::cur_step == identifier::next_step`. @@ -40,7 +38,7 @@ The exponentiation circuit consists of the following columns: - `exp_table.is_step` MUST be boolean. - `exp_table.is_last` MUST be boolean. -- For every row where `is_step == true` and `padding == false`, validate that: +- For every row where `is_step == true`, validate that: - `exponentiation_lo` MUST equal `mul_gadget`'s multiplication result `d_lo`. - `exponentiation_hi` MUST equal `mul_gadget`'s multiplication result `d_hi`. - Since we are only performing multiplication with the equation `a * b + c == d`, `c` in the `mul_gadget` MUST equal `0`. @@ -73,9 +71,6 @@ The exponentiation circuit consists of the following columns: - Both multiplicand's of the `mul_gadget`, i.e. `a` and `b` MUST equal `base` of the exponentiation operation, that is: - `mul_gadget.a == base` - `mul_gadget.b == base` (for both these cases we equate each 64-bit limb) -- For every row where `padding == true` and `is_final == false`, validate that: - - next row is also `padding == true` - - all other columns are set to 0 diff --git a/src/zkevm_specs/evm/table.py b/src/zkevm_specs/evm/table.py index a8f9d8ce6..5d2627b2f 100644 --- a/src/zkevm_specs/evm/table.py +++ b/src/zkevm_specs/evm/table.py @@ -480,8 +480,6 @@ class KeccakTableRow(TableRow): @dataclass class ExpCircuitRow(TableRow): q_usable: FQ - padding: FQ - is_final: FQ # columns from the exponentiation table is_step: FQ identifier: FQ # rw_counter diff --git a/src/zkevm_specs/evm/typing.py b/src/zkevm_specs/evm/typing.py index 4ca1204bc..6029a04b4 100644 --- a/src/zkevm_specs/evm/typing.py +++ b/src/zkevm_specs/evm/typing.py @@ -744,6 +744,8 @@ class ExpCircuit: rows: List[ExpCircuitRow] pad_rows: List[ExpCircuitRow] + MAX_EXP_STEPS = 100 + def __init__(self, pad_rows: Optional[List[ExpCircuitRow]] = None) -> None: self.rows = [] self.pad_rows = [] @@ -817,25 +819,25 @@ def _append_steps( exponent = exponent - 1 def _append_padding_row(self, identifier: IntOrFQ): - self.rows.append( - ExpCircuitRow( - q_usable=FQ.one(), - padding=FQ.one(), - is_final=FQ.one(), - is_step=FQ.zero(), - identifier=FQ(identifier), - is_last=FQ.zero(), - base=RLC(0), - exponent=RLC(0), - exponentiation=RLC(0), - a=RLC(0), - b=RLC(0), - c=RLC(0), - d=RLC(0), - q=RLC(0), - r=RLC(0), + rows_left = self.MAX_EXP_STEPS - len(self.rows) + for i in range(rows_left): + self.rows.append( + ExpCircuitRow( + q_usable=FQ.one(), + is_step=FQ.zero(), + identifier=FQ(identifier), + is_last=FQ.zero(), + base=RLC(1), + exponent=RLC(1), + exponentiation=RLC(1), + a=RLC(1), + b=RLC(1), + c=RLC(0), + d=RLC(1), + q=RLC(0), + r=RLC(1), + ) ) - ) def _append_step( self, @@ -854,8 +856,6 @@ def _append_step( self.rows.append( ExpCircuitRow( q_usable=FQ.one(), - padding=FQ.zero(), - is_final=FQ.zero(), is_step=FQ.one(), identifier=FQ(identifier), is_last=FQ(is_last), diff --git a/src/zkevm_specs/exp_circuit.py b/src/zkevm_specs/exp_circuit.py index 53c9d4b7f..5255da8fa 100644 --- a/src/zkevm_specs/exp_circuit.py +++ b/src/zkevm_specs/exp_circuit.py @@ -13,8 +13,8 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): - # for every non-padded step except the last - with cs.condition(rows[0].is_step * (1 - rows[0].is_last) * (1 - rows[0].padding)) as cs: + # for every step except the last + with cs.condition(rows[0].is_step * (1 - rows[0].is_last)) as cs: # base is the same across rows. cs.constrain_equal(rows[0].base, rows[1].base) # multiplication result from the "next" row `d` must be used as @@ -23,8 +23,8 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): # identifier does not change over the steps of an exponentiation trace. cs.constrain_equal(rows[0].identifier, rows[1].identifier) - # for every non-padded step - with cs.condition(rows[0].is_step * (1 - rows[0].padding)) as cs: + # for every step + with cs.condition(rows[0].is_step) as cs: # is_last is boolean. cs.constrain_bool(rows[0].is_last) # remainder (r), i.e. odd/even parity of exponent is boolean. @@ -50,10 +50,8 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): cs.constrain_equal(additional_constraints[0][0], additional_constraints[0][1]) cs.constrain_equal(additional_constraints[1][0], additional_constraints[1][1]) - # for all non-padded steps (except the last), where exponent is odd - with cs.condition( - rows[0].is_step * (1 - rows[0].is_last) * rows[0].r.expr() * (1 - rows[0].padding) - ) as cs: + # for all steps (except the last), where exponent is odd + with cs.condition(rows[0].is_step * (1 - rows[0].is_last) * rows[0].r.expr()) as cs: # exponent::next == exponent::cur - 1 cur_lo, cur_hi = word_to_lo_hi(rows[0].exponent) next_lo, next_hi = word_to_lo_hi(rows[1].exponent) @@ -64,10 +62,8 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): # b == base cs.constrain_equal(rows[0].base, rows[0].b) - # for all non-padded steps (except the last), where exponent is even - with cs.condition( - rows[0].is_step * (1 - rows[0].is_last) * (1 - rows[0].r.expr()) * (1 - rows[0].padding) - ) as cs: + # for all steps (except the last), where exponent is even + with cs.condition(rows[0].is_step * (1 - rows[0].is_last) * (1 - rows[0].r.expr())) as cs: # exponent::next == exponent::cur / 2 cur_lo, cur_hi = word_to_lo_hi(rows[0].exponent) next_lo, next_hi = word_to_lo_hi(rows[1].exponent) @@ -78,8 +74,8 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): # a == b cs.constrain_equal(rows[0].a, rows[0].b) - # for the last non-padded step - with cs.condition(rows[0].is_last * (1 - rows[0].padding)) as cs: + # for the last step + with cs.condition(rows[0].is_last) as cs: # exponent == 2 exponent_lo, exponent_hi = word_to_lo_hi(rows[0].exponent) cs.constrain_equal(exponent_lo, FQ(2)) @@ -88,35 +84,6 @@ def verify_step(cs: ConstraintSystem, rows: List[ExpCircuitRow]): cs.constrain_equal(rows[0].base, rows[0].a) # b == base cs.constrain_equal(rows[0].base, rows[0].b) - # followed by padding - cs.constrain_equal(rows[1].padding, FQ(1)) - - # for padding - with cs.condition(rows[0].padding * (1 - rows[0].is_final)) as cs: - # padding::next == padding::cur - cs.constrain_equal(rows[1].padding, rows[0].padding) - # is_step == 0 - cs.constrain_zero(rows[0].is_step) - # is_last == 0 - cs.constrain_zero(rows[0].is_last) - # base == 0 - cs.constrain_zero(rows[0].base) - # exponent == 0 - cs.constrain_zero(rows[0].exponent) - # exponentiation == 0 - cs.constrain_zero(rows[0].exponentiation) - # a == 0 - cs.constrain_zero(rows[0].a) - # b == 0 - cs.constrain_zero(rows[0].b) - # c == 0 - cs.constrain_zero(rows[0].c) - # d == 0 - cs.constrain_zero(rows[0].d) - # q == 0 - cs.constrain_zero(rows[0].q) - # r == 0 - cs.constrain_zero(rows[0].r) def verify_exp_circuit(exp_circuit: ExpCircuit): From 4ea541cdcafb1012250181a4fe7e9c67668c3352 Mon Sep 17 00:00:00 2001 From: Richard Zhang Date: Mon, 30 Jan 2023 14:11:05 -0800 Subject: [PATCH 5/7] nit changes --- specs/exp-proof.md | 2 -- src/zkevm_specs/evm/typing.py | 14 +++++++------- tests/evm/test_exp.py | 2 +- 3 files changed, 8 insertions(+), 10 deletions(-) diff --git a/specs/exp-proof.md b/specs/exp-proof.md index e22b0ca85..effd7bad9 100644 --- a/specs/exp-proof.md +++ b/specs/exp-proof.md @@ -72,8 +72,6 @@ The exponentiation circuit consists of the following columns: - `mul_gadget.a == base` - `mul_gadget.b == base` (for both these cases we equate each 64-bit limb) - - ## Code Please refer to [Exponentiation Circuit Verification](`src/zkevm-specs/exp_circuit.py`). diff --git a/src/zkevm_specs/evm/typing.py b/src/zkevm_specs/evm/typing.py index 6029a04b4..77bc03600 100644 --- a/src/zkevm_specs/evm/typing.py +++ b/src/zkevm_specs/evm/typing.py @@ -743,14 +743,14 @@ def add(self, data: bytes, r: FQ) -> KeccakCircuit: class ExpCircuit: rows: List[ExpCircuitRow] pad_rows: List[ExpCircuitRow] + max_exp_steps: int - MAX_EXP_STEPS = 100 - - def __init__(self, pad_rows: Optional[List[ExpCircuitRow]] = None) -> None: + def __init__(self, pad_rows: Optional[List[ExpCircuitRow]] = None, max_exp_steps: Optional[int] = 100) -> None: self.rows = [] self.pad_rows = [] if pad_rows is not None: self.pad_rows = pad_rows + self.max_exp_steps = max_exp_steps def table(self) -> Sequence[ExpCircuitRow]: return self.rows + self.pad_rows @@ -760,7 +760,6 @@ def add_event(self, base: int, exponent: int, randomness: FQ, identifier: IntOrF exponentiation = self._exp_by_squaring(base, exponent, steps) steps.reverse() self._append_steps(base, exponent, exponentiation, steps, randomness, identifier) - self._append_padding_row(identifier) return self def _exp_by_squaring(self, base: int, exponent: int, steps: List[Tuple[int, int, int]]): @@ -818,14 +817,14 @@ def _append_steps( # exponent is odd exponent = exponent - 1 - def _append_padding_row(self, identifier: IntOrFQ): - rows_left = self.MAX_EXP_STEPS - len(self.rows) + def fill_dummy_events(self): + rows_left = self.max_exp_steps - len(self.rows) for i in range(rows_left): self.rows.append( ExpCircuitRow( q_usable=FQ.one(), is_step=FQ.zero(), - identifier=FQ(identifier), + identifier=FQ.zero(), is_last=FQ.zero(), base=RLC(1), exponent=RLC(1), @@ -838,6 +837,7 @@ def _append_padding_row(self, identifier: IntOrFQ): r=RLC(1), ) ) + return self def _append_step( self, diff --git a/tests/evm/test_exp.py b/tests/evm/test_exp.py index 99dfba6a8..b4b7dd30a 100644 --- a/tests/evm/test_exp.py +++ b/tests/evm/test_exp.py @@ -69,7 +69,7 @@ def test_exp(base: int, exponent: int): .stack_write(CALL_ID, 1023, exponentiation_rlc) ) - exp_circuit = ExpCircuit().add_event(base, exponent, randomness, rw_dict.rw_counter) + exp_circuit = ExpCircuit().add_event(base, exponent, randomness, rw_dict.rw_counter).fill_dummy_events() tables = Tables( block_table=set(Block().table_assignments(randomness)), From c004b8d7637c2991eab1b25ee45c4381d8e1c329 Mon Sep 17 00:00:00 2001 From: Richard Zhang Date: Tue, 14 Feb 2023 09:31:32 -0800 Subject: [PATCH 6/7] convert steps -> rows and removed pad_rows --- src/zkevm_specs/evm/typing.py | 12 +++++------- tests/evm/test_exp.py | 4 +++- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/zkevm_specs/evm/typing.py b/src/zkevm_specs/evm/typing.py index 77bc03600..749c343cc 100644 --- a/src/zkevm_specs/evm/typing.py +++ b/src/zkevm_specs/evm/typing.py @@ -742,18 +742,15 @@ def add(self, data: bytes, r: FQ) -> KeccakCircuit: class ExpCircuit: rows: List[ExpCircuitRow] - pad_rows: List[ExpCircuitRow] max_exp_steps: int + OFFSET_INCREMENT = 7 - def __init__(self, pad_rows: Optional[List[ExpCircuitRow]] = None, max_exp_steps: Optional[int] = 100) -> None: + def __init__(self, max_exp_steps: Optional[int] = 100) -> None: self.rows = [] - self.pad_rows = [] - if pad_rows is not None: - self.pad_rows = pad_rows self.max_exp_steps = max_exp_steps def table(self) -> Sequence[ExpCircuitRow]: - return self.rows + self.pad_rows + return self.rows def add_event(self, base: int, exponent: int, randomness: FQ, identifier: IntOrFQ): steps: List[Tuple[int, int, int]] = [] @@ -818,7 +815,8 @@ def _append_steps( exponent = exponent - 1 def fill_dummy_events(self): - rows_left = self.max_exp_steps - len(self.rows) + max_exp_rows = self.max_exp_steps * self.OFFSET_INCREMENT + rows_left = max_exp_rows - len(self.rows) for i in range(rows_left): self.rows.append( ExpCircuitRow( diff --git a/tests/evm/test_exp.py b/tests/evm/test_exp.py index b4b7dd30a..930fcf372 100644 --- a/tests/evm/test_exp.py +++ b/tests/evm/test_exp.py @@ -69,7 +69,9 @@ def test_exp(base: int, exponent: int): .stack_write(CALL_ID, 1023, exponentiation_rlc) ) - exp_circuit = ExpCircuit().add_event(base, exponent, randomness, rw_dict.rw_counter).fill_dummy_events() + exp_circuit = ( + ExpCircuit().add_event(base, exponent, randomness, rw_dict.rw_counter).fill_dummy_events() + ) tables = Tables( block_table=set(Block().table_assignments(randomness)), From 818fe50a8c314742408c5308f0a7dca2f5fff100 Mon Sep 17 00:00:00 2001 From: Richard Zhang Date: Thu, 9 Mar 2023 10:47:04 -0800 Subject: [PATCH 7/7] fixed typing issue --- src/zkevm_specs/evm/typing.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/zkevm_specs/evm/typing.py b/src/zkevm_specs/evm/typing.py index 749c343cc..7c7ee3b49 100644 --- a/src/zkevm_specs/evm/typing.py +++ b/src/zkevm_specs/evm/typing.py @@ -745,7 +745,7 @@ class ExpCircuit: max_exp_steps: int OFFSET_INCREMENT = 7 - def __init__(self, max_exp_steps: Optional[int] = 100) -> None: + def __init__(self, max_exp_steps: int = 100) -> None: self.rows = [] self.max_exp_steps = max_exp_steps