feat/#325 precomiple ecPairing

specs/precompile/06ecAdd.md

@@ -12,7 +12,7 @@ Two points are recovered from input. The field is expressed as `32` bytes for ea
 input[0; 31] (32 bytes): x1
 input[32; 63] (32 bytes): y1
 input[64; 95] (32 bytes): x2
-input[96; 128] (32 bytes): y2
+input[96; 127] (32 bytes): y2
 ```
 
 These two points are added and the result is returned. The result size is `64` bytes and $x$ and $y$ are in Montgomery.

specs/precompile/08ecPairing.md

@@ -0,0 +1,52 @@
+# ecPairing precompile
+
+## Procedure
+
+The `ecPairing` precompile computes the bilinear map between two given points in the groups G1 and G2, respectively, over the alt_bn128 curve.
+
+### Circuit behavior
+
+The input is arbitrarily many pairs of elliptic curve points. Each pair is given as a six 32-bytes values and is constructed as follows
+
+```
+input[0; 31] (32 bytes): x1
+input[32; 63] (32 bytes): y1
+input[64; 95] (32 bytes): x2
+input[96; 127] (32 bytes): y2
+input[128; 159] (32 bytes): x3 (result)
+input[160; 191] (32 bytes): y3 (result)
+```
+
+The first two 32-bytes values represent the first point (px, py) from group G1, the next four 32-bytes values represent the other point (qx, qy) from group G2.
+
+The bn254Pairing code first checks that a multiple of 6 elements have been sent, and then performs the pairings check(s). The check that is performed for two pairs is e(p1, q1) = e(-p2, q2) which is equivalent to the check e(p1, q1) * e(p2, q2) = 1.
+
+The output is 1 if all pairing checks were successful, otherwise it returns 0.
+
+```
+input[0; 31] (32 bytes): success
+```
+
+The pairing checks fail if not having a multiple of 6 32-bytes values or in the case of the points not being on the curve. In these cases all the provided gas is consumed. For these cases, the variable is_valid is set to 0. The variable output denotes whether the pairing checks were successful (in the case of is_valid = 1)
+### Gas cost
+
+1. A constant gas cost: 45,000
+2. A dynamic gas cost: 34,000 * (len(data) / 192)
+
+If the input is not valid, all gas provided is consumed.
+
+## Constraints
+
+1. If the length of the input is not a multiple of 192 bytes
+  - output is 0
+2. If the input is empty which means it's a successful call,
+  - `input_rlc` is zero
+  - output is 1
+3. `ecc_table` lookup
+4. If `is_valid` is false,
+  - output is 0
+  - consume all the remaining gas
+
+## Code
+
+Please refer to `src/zkevm_specs/evm_circuit/execution/precompiles/ec_pairing.py`.

src/zkevm_specs/ecc_circuit.py

@@ -1,10 +1,11 @@
 from __future__ import annotations
 from typing import List, NamedTuple, Tuple
-from py_ecc.bn128.bn128_curve import is_on_curve, b
+from py_ecc.bn128.bn128_curve import is_on_curve, b, b2, multiply
+from py_ecc.bn128 import bn128_curve
 
-from zkevm_specs.util.arithmetic import FP
+from zkevm_specs.util.arithmetic import FP, RLC
 from .evm_circuit import EccTableRow
-from .util import ConstraintSystem, FQ, Word, ECCVerifyChip
+from .util import ConstraintSystem, FQ, Word, ECCVerifyChip, ECCPairingVerifyChip
 from zkevm_specs.evm_circuit.table import EccOpTag
 
 
@@ -17,9 +18,14 @@ class EccCircuitRow:
 
     ecc_chip: ECCVerifyChip
 
-    def __init__(self, row: EccTableRow, ecc_chip: ECCVerifyChip) -> None:
+    ecc_pairing_chip: ECCPairingVerifyChip
+
+    def __init__(
+        self, row: EccTableRow, ecc_chip: ECCVerifyChip, ecc_pairing_chip: ECCPairingVerifyChip
+    ) -> None:
         self.row = row
         self.ecc_chip = ecc_chip
+        self.ecc_pairing_chip = ecc_pairing_chip
 
     @classmethod
     def check_fq(cls, value: int) -> bool:
@@ -36,8 +42,6 @@ def assign(
             return cls.assign_add(p[0], p[1], out)
         elif op_type == EccOpTag.Mul:
             return cls.assign_mul(p[0], p[1], out)
-        elif op_type == EccOpTag.Pairing:
-            return cls.assign_pairing(p, out)
         else:
             raise TypeError(f"Not supported type: {op_type}")
 
@@ -92,7 +96,7 @@ def assign_add(cls, p0: Tuple[Word, Word], p1: Tuple[Word, Word], out: Tuple[FP,
             FQ(is_valid),
         )
 
-        return cls(ecc_table, ecc_chip)
+        return cls(ecc_table, ecc_chip, None)
 
     @classmethod
     def assign_mul(cls, p0: Tuple[Word, Word], p1: Tuple[Word, Word], out: Tuple[Word, Word]):
@@ -135,29 +139,132 @@ def assign_mul(cls, p0: Tuple[Word, Word], p1: Tuple[Word, Word], out: Tuple[Wor
             FQ(is_valid),
         )
 
-        return cls(ecc_table, ecc_chip)
+        return cls(ecc_table, ecc_chip, None)
 
     @classmethod
-    def assign_pairing(cls, p: List[Tuple[Word, Word]], out: Tuple[Word, Word]):
-        raise NotImplementedError("assign_pairing is not supported yet")
+    def assign_pairing(
+        cls, pts: List[Tuple[Word, Word, Word, Word, Word, Word]], out: Word, keccak_randomness: FQ
+    ):
+        ps_g1 = []
+        qs_g2 = []
+        is_valid = True
+        input_bytes = bytearray(b"")
+        num_of_pairings = 0
+        for p in pts:
+            p_x = p[0].int_value()
+            p_y = p[1].int_value()
+            q_x1 = p[3].int_value()
+            q_x2 = p[2].int_value()
+            q_y1 = p[5].int_value()
+            q_y2 = p[4].int_value()
+
+            p_g1 = (FP(p_x), FP(p_y))
+            q_g2 = (
+                bn128_curve.FQ2([q_x1, q_x2]),
+                bn128_curve.FQ2([q_y1, q_y2]),
+            )
+            ps_g1.append(p_g1)
+            qs_g2.append(q_g2)
+
+            ### verify validity of input points
+            # 1. values of p0, p1 and p2 are within FQ.field_modulus
+            precheck_px = cls.check_fq(p_x)
+            precheck_py = cls.check_fq(p_y)
+            precheck_qx1 = cls.check_fq(q_x1)
+            precheck_qx2 = cls.check_fq(q_x2)
+            precheck_qy1 = cls.check_fq(q_y1)
+            precheck_qy2 = cls.check_fq(q_y2)
+
+            # 2. p0 on G1, and p1 and p2 on G2 are all on the curve
+            # (0, 0) represents an infinite point in the circuit
+            point1_g1 = None if p_x == 0 and p_y == 0 else p_g1
+            point2_g2 = None if q_x1 == 0 and q_x2 == 0 and q_y1 == 0 and q_y2 == 0 else q_g2
+
+            # 3.point * curve order == infinity
+            # ref: https://github.com/ethereum/execution-specs/blob/master/src/ethereum/paris/vm/precompiled_contracts/alt_bn128.py#L142-L149
+            result = multiply(point1_g1, bn128_curve.curve_order)
+            valid_p = True if result is None else False
+            result = multiply(point2_g2, bn128_curve.curve_order)
+            valid_q = True if result is None else False
+
+            is_valid_points = (
+                is_on_curve(point1_g1, b) and is_on_curve(point2_g2, b2) and valid_p and valid_q
+            )
+
+            is_valid = is_valid and (
+                precheck_px
+                and precheck_py
+                and precheck_qx1
+                and precheck_qx2
+                and precheck_qy1
+                and precheck_qy2
+                and is_valid_points
+            )
+
+            # construct input bytes for RLC
+            input_bytes.extend(p_x.to_bytes(32, "little"))
+            input_bytes.extend(p_y.to_bytes(32, "little"))
+            input_bytes.extend(q_x1.to_bytes(32, "little"))
+            input_bytes.extend(q_x2.to_bytes(32, "little"))
+            input_bytes.extend(q_y1.to_bytes(32, "little"))
+            input_bytes.extend(q_y2.to_bytes(32, "little"))
+            num_of_pairings += 1
+
+        ecc_pairing_chip = ECCPairingVerifyChip.assign(
+            p=ps_g1,
+            q=qs_g2,
+            output=out.lo.expr(),
+        )
+        ecc_table = EccTableRow(
+            FQ(EccOpTag.Pairing),
+            Word(0),
+            Word(0),
+            Word(0),
+            Word(0),
+            RLC(
+                bytes(reversed(input_bytes)), keccak_randomness, n_bytes=num_of_pairings * 192
+            ).expr(),
+            out.hi.expr(),
+            out.lo.expr(),
+            FQ(is_valid),
+        )
+
+        return cls(ecc_table, None, ecc_pairing_chip)
 
     def verify(
-        self, cs: ConstraintSystem, max_add_ops: int, max_mul_ops: int, max_pairing_ops: int
+        self,
+        cs: ConstraintSystem,
+        max_add_ops: int,
+        max_mul_ops: int,
+        max_pairing_ops: int,
+        keccak_randomness: FQ,
     ):
-        # Copy constraints between EccTable and ECCVerifyChip
-        cs.constrain_equal_word(Word(self.ecc_chip.p0[0].n), self.row.px)
-        cs.constrain_equal_word(Word(self.ecc_chip.p0[1].n), self.row.py)
-        cs.constrain_equal_word(Word(self.ecc_chip.p1[0].n), self.row.qx)
-        cs.constrain_equal_word(Word(self.ecc_chip.p1[1].n), self.row.qy)
-        cs.constrain_equal(self.ecc_chip.output[0], self.row.out_x)
-        cs.constrain_equal(self.ecc_chip.output[1], self.row.out_y)
-
         is_add = cs.is_equal(self.row.op_type, FQ(EccOpTag.Add))
         is_mul = cs.is_equal(self.row.op_type, FQ(EccOpTag.Mul))
         is_pairing = cs.is_equal(self.row.op_type, FQ(EccOpTag.Pairing))
+
         # Must be one of above operations
         cs.constrain_equal(is_add + is_mul + is_pairing, FQ(1))
 
+        # Copy constraints between EccTable and ECCVerifyChip
+        if is_add == FQ.one() or is_mul == FQ.one():
+            cs.constrain_equal_word(Word(self.ecc_chip.p0[0].n), self.row.px)
+            cs.constrain_equal_word(Word(self.ecc_chip.p0[1].n), self.row.py)
+            cs.constrain_equal_word(Word(self.ecc_chip.p1[0].n), self.row.qx)
+            cs.constrain_equal_word(Word(self.ecc_chip.p1[1].n), self.row.qy)
+            cs.constrain_equal(self.ecc_chip.output[0], self.row.out_x)
+            cs.constrain_equal(self.ecc_chip.output[1], self.row.out_y)
+            # input_rlc is zero bcs it's only used in pairing
+            cs.constrain_zero(self.row.input_rlc)
+        else:  # if is_pairing is true
+            # p and q are all zero. All input points are RLCed and stored in input_rlc
+            cs.constrain_zero_word(self.row.px)
+            cs.constrain_zero_word(self.row.py)
+            cs.constrain_zero_word(self.row.qx)
+            cs.constrain_zero_word(self.row.qy)
+
+        cs.constrain_bool(self.row.is_valid)
+
         num_add = 0
         num_mul = 0
         num_pairing = 0
@@ -180,36 +287,50 @@ def verify(
             assert (
                 num_pairing <= max_pairing_ops
             ), f"exceeds max number of pairing operation, max_pairing_ops: {max_pairing_ops}"
-            self.verify_pairing(cs)
+            self.verify_pairing(cs, keccak_randomness)
 
     def verify_add(self, cs: ConstraintSystem):
-        # input_rlc is zero bcs it's only used in pairing
-        cs.constrain_zero(self.row.input_rlc)
-
         cs.constrain_equal(FQ(self.ecc_chip.verify_add()), self.row.is_valid)
 
     def verify_mul(self, cs: ConstraintSystem):
-        # input_rlc is zero bcs it's only used in pairing
-        cs.constrain_zero(self.row.input_rlc)
-        # qy is zero bcs q is a scalar in ecMul and we only use qx
+        # qy is zero bcs q is scalar in ecMul so we only use qx
         cs.constrain_zero_word(self.row.qy)
 
         cs.constrain_equal(FQ(self.ecc_chip.verify_mul()), self.row.is_valid)
 
-    def verify_pairing(self, cs: ConstraintSystem):
-        # p and q are all zero. All input points are RLCed and stored in input_rlc
-        cs.constrain_zero(self.row.px)
-        cs.constrain_zero(self.row.py)
-        cs.constrain_zero(self.row.qx)
-        cs.constrain_zero(self.row.qy)
-        # output of pairing is either 0 or 1 and stored in the lower part
+    def verify_pairing(self, cs: ConstraintSystem, keccak_randomness: FQ):
+        # output of pairing is stored in row.outy
         cs.constrain_zero(self.row.out_x)
-        cs.constrain_bool(self.row.out_y)
-        # TODO: fixing it in ecPairing PR
-        # see https://github.com/privacy-scaling-explorations/zkevm-specs/pull/500#discussion_r1383072583
-        cs.constrain_equal(self.row.out_y, self.row.is_valid)
-
-        cs.constrain_equal(FQ(self.ecc_chip.verify_pairing()), self.row.is_valid)
+        cs.constrain_equal(self.ecc_pairing_chip.output, self.row.out_y)
+
+        num_of_pairings = 0
+        input_bytes = bytearray(b"")
+        for p, q in zip(self.ecc_pairing_chip.p, self.ecc_pairing_chip.q):
+            pp = None if p[0].n == 0 and p[1].n == 0 else (p[0], p[1])
+            pq = None if q[0].coeffs == (0, 0) and q[1].coeffs == (0, 0) else (q[0], q[1])
+            # point * curve order == infinity
+            result = multiply(pp, bn128_curve.curve_order)
+            valid_p = FQ.one() if result is None else FQ.zero()
+            result = multiply(pq, bn128_curve.curve_order)
+            valid_q = FQ.one() if result is None else FQ.zero()
+            cs.constrain_equal(valid_p + valid_q, FQ(2))
+
+            # concatenate input points for rlc
+            input_bytes.extend(p[0].n.to_bytes(32, "little"))
+            input_bytes.extend(p[1].n.to_bytes(32, "little"))
+            input_bytes.extend(q[0].coeffs[0].n.to_bytes(32, "little"))
+            input_bytes.extend(q[0].coeffs[1].n.to_bytes(32, "little"))
+            input_bytes.extend(q[1].coeffs[0].n.to_bytes(32, "little"))
+            input_bytes.extend(q[1].coeffs[1].n.to_bytes(32, "little"))
+            num_of_pairings += 1
+
+        # constrain the value of input_rlc in a row equals the rlc value of cells in ecc_pairing_chip
+        inputs_rlc = RLC(
+            bytes(reversed(input_bytes)), keccak_randomness, n_bytes=num_of_pairings * 192
+        ).expr()
+        cs.constrain_equal(self.row.input_rlc, inputs_rlc)
+
+        cs.constrain_equal(FQ(self.ecc_pairing_chip.verify_pairing()), self.row.out_y)
 
 
 class EcAdd(NamedTuple):
@@ -262,7 +383,7 @@ def append_pairing(self, op: EcPairing):
         self.pairing_ops.append(op)
 
 
-def circuit2rows(circuit: EccCircuit) -> List[EccCircuitRow]:
+def circuit2rows(circuit: EccCircuit, randomness_keccak: FQ) -> List[EccCircuitRow]:
     rows: List[EccCircuitRow] = []
     for op in circuit.add_ops:
         row = EccCircuitRow.assign(
@@ -282,30 +403,31 @@ def circuit2rows(circuit: EccCircuit) -> List[EccCircuitRow]:
         )
         rows.append(row)
     for op in circuit.pairing_ops:
-        points: List[Word] = []
-        for i, g1_pt in enumerate(op.g1_pts):
-            points.append(g1_pt[0])
-            points.append(g1_pt[1])
-            points.append(op.g2_pts[i][0])
-            points.append(op.g2_pts[i][1])
-            points.append(op.g2_pts[i][2])
-            points.append(op.g2_pts[i][3])
-
-        row = EccCircuitRow.assign(
-            EccOpTag.Pairing,
-            points,
-            (FP(0), FP(op.out)),
-        )
+        points: List[Tuple[Word, Word, Word, Word, Word, Word]] = []
+        for g1_pt, g2_pt in zip(op.g1_pts, op.g2_pts):
+            points.append(
+                (
+                    Word(g1_pt[0]),
+                    Word(g1_pt[1]),
+                    Word(g2_pt[0]),
+                    Word(g2_pt[1]),
+                    Word(g2_pt[2]),
+                    Word(g2_pt[3]),
+                )
+            )
+        row = EccCircuitRow.assign_pairing(points, Word(op.out), randomness_keccak)
         rows.append(row)
 
     return rows
 
 
-def verify_circuit(circuit: EccCircuit) -> None:
+def verify_circuit(circuit: EccCircuit, randomness_keccak: FQ) -> None:
     """
     Entry level circuit verification function
     """
     cs = ConstraintSystem()
-    rows = circuit2rows(circuit)
+    rows = circuit2rows(circuit, randomness_keccak)
     for row in rows:
-        row.verify(cs, circuit.max_add_ops, circuit.max_mul_ops, circuit.max_pairing_ops)
+        row.verify(
+            cs, circuit.max_add_ops, circuit.max_mul_ops, circuit.max_pairing_ops, randomness_keccak
+        )