ZK-Bootcamp - Homework 8 - R1CS
!python -m pip install py-ecc
from py_ecc.optimized_bn128 import G1, G2, add, multiply, pairing, is_on_curve, b, b2, neg
import numpy as np
Problem 1
Create a graph with 2 nodes and 1 edge and write constraints for a 3-coloring. T the 3-coloring to a rank 1 constraint system.
# Consider the 2 nodes to be {x,y}
# Consider the three available colors to be {1,2,3}
# Ensure each node only has one color
# (1-x)*(2-x)*(3-x) === 0
# (1-y)*(2-y)*(3-y) === 0
# Ensure the two nodes have different colors
# Truth table:
# x | y | x.y | yes/no
# 1 | 1 | 1 | no
# 1 | 2 | 2 | yes
# 1 | 3 | 3 | yes
# 2 | 1 | 2 | yes
# 2 | 2 | 4 | no
# 2 | 3 | 6 | yes
# 3 | 1 | 3 | yes
# 3 | 2 | 6 | yes
# 3 | 3 | 9 | no
# The yes condition is that x.y == 2 or 3 or 6
# (2 - x.y)*(3 - x.y)*(6 - x.y) === 0
# So the final constraints are:
# Constraint 1 - (1-x)*(2-x)*(3-x) === 0
# Constraint 2 - (1-y)*(2-y)*(3-y) === 0
# Constraint 3 - (2 - x.y)*(3 - x.y)*(6 - x.y) === 0
# In R1CS, a constraint can only have one multiplication.
# Converting Constraint 1 to R1CS form:
# (1-x).(2-x).(3-x) === 0
# -x.x.x + 6.x.x - 11.x + 6 === 0
# a === x.x
# -x.a + 6.a - 11.x + 6 === 0
# Converting Constraint 2 to R1CS form:
# b === y.y
# -y.b + 6.b - 11.y + 6 === 0
# Converting Constraint 3 to R1CS form:
# c === x.y
# (2 - c)*(3 - c)*(6 - c) === 0
# -c.c.c + 11.c.c - 36c + 36 === 0
# d = c.c
# -d.c + 11.d - 36.c + 36 === 0
# This is a simple R1CS circuit for the problem of coloring two nodes with three colors
# a === x.x
# b === y.y
# c === x.y
# d === c.c
# -x.a + 6.a - 11.x + 6 === 0
# -y.b + 6.b - 11.y + 6 === 0
# -d.c + 11.d - 36.c + 36 === 0
Problem 2
Write python code that takes an R1CS matrix A, B, and C and a witness vector w and verifies.
Aw ⊙ Bw − Cw = 0
Where ⊙ is the hadamard (element-wise) product.
Use this to code to check your answer above is correct.
# The R1CS constraints as matrices A, B, C:
# Aw . Bw = Cw
A = [
[0, 1, 0, 0, 0, 0, 0],
[0, 0, 1, 0, 0, 0, 0],
[0, 1, 0, 0, 0, 0, 0],
[0, 0, 0, 0, 0, 1, 0],
[0, 1, 0, 0, 0, 0, 0],
[0, 0, 1, 0, 0, 0, 0],
[0, 0, 0, 0, 0, 0, 1],
]
B = [
[0, 1, 0, 0, 0, 0, 0],
[0, 0, 1, 0, 0, 0, 0],
[0, 0, 1, 0, 0, 0, 0],
[0, 0, 0, 0, 0, 1, 0],
[0, 0, 0, 1, 0, 0, 0],
[0, 0, 0, 0, 1, 0, 0],
[0, 0, 0, 0, 0, 1, 0],
]
C = [
[0, 0, 0, 1, 0, 0, 0],
[0, 0, 0, 0, 1, 0, 0],
[0, 0, 0, 0, 0, 1, 0],
[0, 0, 0, 0, 0, 0, 1],
[6, -11, 0, 6, 0, 0, 0],
[6, 0, -11, 0, 6, 0, 0],
[36, 0, 0, 0, 0, -36, 11],
]
def verify_r1cs(A, B, C, w):
Aw = np.matmul(A, w)
Bw = np.matmul(B, w)
Cw = np.matmul(C, w)
Aw_Bw = np.multiply(Aw, Bw)
return np.all(Aw_Bw == Cw)
def get_witness_vector(x, y):
a = x * x
b = y * y
c = x * y
d = c * c
return [1, x, y, a, b, c, d]
# Valid Witness
x, y = 1, 2
assert verify_r1cs(A, B, C, get_witness_vector(x, y)) == True
# Invalid Witness - same color
x, y = 1, 1
assert verify_r1cs(A, B, C, get_witness_vector(x, y)) == False
# Invalid Witness - disallowed color
x, y = 1, 5
assert verify_r1cs(A, B, C, get_witness_vector(x, y)) == False
Problem 3
Given an R1CS of the form
\[L\mathbf{\vec{[s]_1}}\odot R\mathbf{\vec{[s]_2}} = O\mathbf{\vec{[s]}_{1}}\odot\vec{[G_2]_2}\]Where L, R, and O are n x m matrices of field elements and s is a vector of G1, G2, or G1 points
Write python code that verifies the formula.
You can check the equality of G12 points in Python this way:
a = pairing(multiply(G2, 5), multiply(G1, 8))
b = pairing(multiply(G2, 10), multiply(G1, 4))
eq(a, b)
def get_witness_vector_g1(x, y):
witness = get_witness_vector(x, y)
return [multiply(G1, w) for w in witness]
def get_witness_vector_g2(x, y):
witness = get_witness_vector(x, y)
return [multiply(G2, w) for w in witness]
def get_witness_vectors(x, y):
witness_g1 = get_witness_vector_g1(x, y)
witness_g2 = get_witness_vector_g2(x, y)
return witness_g1, witness_g2
# Multiplies the constraint matrices A, B, C with the witness vectors w1, w2
def matmul(matrix, w):
result_m = []
for i in range(len(matrix)):
row_sum = None
for j in range(len(w)):
matrix_point = matrix[i][j]
scaled_point = None
if matrix_point < 0:
scaled_point = neg(multiply(w[j], -matrix_point)) # Negate the point if the matrix entry is negative
else:
scaled_point = multiply(w[j], matrix_point)
if row_sum is None:
row_sum = scaled_point
else:
row_sum = add(row_sum, scaled_point)
result_m.append(row_sum)
return result_m
# Pairing multiplication of two matrices Aw1 and Bw2
def pairing_mul(matrix_2, matrix_1):
assert len(matrix_2) == len(matrix_1)
result = []
for b2_point, b1_point in zip(matrix_2, matrix_1):
assert is_on_curve(b2_point, b2) and is_on_curve(b1_point, b)
result.append(pairing(b2_point, b1_point))
return result
def verify_r1cs_field(A, B, C, w1, w2):
# Ensure all points in w1 and w2 are on the curve
assert all(is_on_curve(pt, b) for pt in w1) == True
assert all(is_on_curve(pt, b2) for pt in w2) == True
# Ensure points in w1 and w2 are derived from the same scalar w
assert len(w1) == len(w2)
assert all(pairing(G2, w1[i]) == pairing(w2[i], G1) for i in range(len(w1))) == True
# Ensure the constraints are satisfied
Aw1 = matmul(A, w1)
Bw2 = matmul(B, w2)
Aw1_Bw2 = pairing_mul(Bw2, Aw1)
Cw1 = matmul(C, w1)
return all(Aw1_Bw2[i] == pairing(G2, Cw1[i]) for i in range(len(Aw1_Bw2)))
# Valid Witness in Field
x, y = 1, 2
witness_g1, witness_g2 = get_witness_vectors(x, y)
assert verify_r1cs_field(A, B, C, witness_g1, witness_g2) == True
# Invalid Witness - same color
x, y = 1, 1
witness_g1, witness_g2 = get_witness_vectors(x, y)
assert verify_r1cs_field(A, B, C, witness_g1, witness_g2) == False
# Invalid Witness - disallowed color
x, y = 1, 5
witness_g1, witness_g2 = get_witness_vectors(x, y)
assert verify_r1cs_field(A, B, C, witness_g1, witness_g2) == False