1# R1CS-to-CCS (https://eprint.iacr.org/2023/552) Sage prototype
  2
  3# utils
  4def matrix_vector_product(M, v):
  5    n = M.nrows()
  6    r = [F(0)] * n
  7    for i in range(0, n):
  8        for j in range(0, M.ncols()):
  9            r[i] += M[i][j] * v[j]
 10    return r
 11def hadamard_product(a, b):
 12    n = len(a)
 13    r = [None] * n
 14    for i in range(0, n):
 15        r[i] = a[i] * b[i]
 16    return r
 17def vec_add(a, b):
 18    n = len(a)
 19    r = [None] * n
 20    for i in range(0, n):
 21        r[i] = a[i] + b[i]
 22    return r
 23def vec_elem_mul(a, s):
 24    r = [None] * len(a)
 25    for i in range(0, len(a)):
 26        r[i] = a[i] * s
 27    return r
 28# end of utils
 29
 30
 31# can use any finite field, using a small one for the example
 32F = GF(101)
 33
 34# R1CS matrices for: x^3 + x + 5 = y (example from article
 35# https://www.vitalik.ca/general/2016/12/10/qap.html )
 36A = matrix([
 37    [F(0), 1, 0, 0, 0, 0],
 38    [0, 0, 0, 1, 0, 0],
 39    [0, 1, 0, 0, 1, 0],
 40    [5, 0, 0, 0, 0, 1],
 41    ])
 42B = matrix([
 43    [F(0), 1, 0, 0, 0, 0],
 44    [0, 1, 0, 0, 0, 0],
 45    [1, 0, 0, 0, 0, 0],
 46    [1, 0, 0, 0, 0, 0],
 47    ])
 48C = matrix([
 49    [F(0), 0, 0, 1, 0, 0],
 50    [0, 0, 0, 0, 1, 0],
 51    [0, 0, 0, 0, 0, 1],
 52    [0, 0, 1, 0, 0, 0],
 53    ])
 54
 55print("R1CS matrices:")
 56print("A:", A)
 57print("B:", B)
 58print("C:", C)
 59
 60
 61z = [F(1), 3, 35, 9, 27, 30]
 62print("z:", z)
 63
 64assert len(z) == A.ncols()
 65
 66n = A.ncols() # == len(z)
 67m = A.nrows()
 68#  l = len(io) # not used for now
 69
 70# check R1CS relation
 71Az = matrix_vector_product(A, z)
 72Bz = matrix_vector_product(B, z)
 73Cz = matrix_vector_product(C, z)
 74print("\nR1CS relation check (Az ∘ Bz == Cz):", hadamard_product(Az, Bz) == Cz)
 75assert hadamard_product(Az, Bz) == Cz
 76
 77
 78# Translate R1CS into CCS:
 79print("\ntranslate R1CS into CCS:")
 80
 81# fixed parameters (and n, m, l are direct from R1CS)
 82t=3
 83q=2
 84d=2
 85S1=[0,1]
 86S2=[2]
 87S = [S1, S2]
 88c0=1
 89c1=-1
 90c = [c0, c1]
 91
 92M = [A, B, C]
 93
 94print("CCS values:")
 95print("n: %s, m: %s, t: %s, q: %s, d: %s" % (n, m, t, q, d))
 96print("M:", M)
 97print("z:", z)
 98print("S:", S)
 99print("c:", c)
100
101# check CCS relation (this is agnostic to R1CS, for any CCS instance)
102r = [F(0)] * m
103for i in range(0, q):
104    hadamard_output = [F(1)]*m
105    for j in S[i]:
106        hadamard_output = hadamard_product(hadamard_output,
107                matrix_vector_product(M[j], z))
108
109    r = vec_add(r, vec_elem_mul(hadamard_output, c[i]))
110
111print("\nCCS relation check (∑ cᵢ ⋅ ◯ Mⱼ z == 0):", r == [0]*m)
112assert r == [0]*m