/ script / research / zk / sumcheck.sage
sumcheck.sage
 1  # Boolean hypercube means a bitstring
 2  # 3d boolean hypercube = ℤ₂³
 3  var("x y z")
 4  
 5  f = 3*x*y + 5*x*z + 2*x*y*z + 6
 6  
 7  claimed_eval = sum([
 8      f(x=0, y=0, z=0),
 9      f(x=0, y=0, z=1),
10      f(x=0, y=1, z=0),
11      f(x=0, y=1, z=1),
12      f(x=1, y=0, z=0),
13      f(x=1, y=0, z=1),
14      f(x=1, y=1, z=0),
15      f(x=1, y=1, z=1),
16  ])
17  # We will now prove the claim
18  assert claimed_eval == 66
19  
20  # Prover constructs g1 such that g1(0) + g1(1) == claimed_eval
21  g1_0 = sum([
22      f(x=0, y=0, z=0),
23      f(x=0, y=0, z=1),
24      f(x=0, y=1, z=0),
25      f(x=0, y=1, z=1),
26  ])
27  g1_1 = sum([
28      f(x=1, y=0, z=0),
29      f(x=1, y=0, z=1),
30      f(x=1, y=1, z=0),
31      f(x=1, y=1, z=1),
32  ])
33  g1 = (1 - x)*g1_0 + x*g1_1
34  
35  # Verifier:
36  assert g1(x=0) + g1(x=1) == claimed_eval
37  r1 = 2
38  
39  # Prover now constructs g2(y) such that g1(r1) == g2(0) + g2(1)
40  g2_0 = sum([
41      f(x=r1, y=0, z=0),
42      f(x=r1, y=0, z=1),
43  ])
44  g2_1 = sum([
45      f(x=r1, y=1, z=0),
46      f(x=r1, y=1, z=1),
47  ])
48  g2 = (1 - y)*g2_0 + y*g2_1
49  
50  # Verifier
51  assert g2(y=0) + g2(y=1) == g1(x=r1)
52  r2 = 7
53  
54  # Prover constructs g3(z) : g2(r2) == g3(0) + g3(1)
55  g3_0 = f(x=r1, y=r2, z=0)
56  g3_1 = f(x=r1, y=r2, z=1)
57  g3 = (1 - z)*g3_0 + z*g3_1
58  
59  # Now verifier picks a random challenge
60  α = 9
61  # and checks f(r1, r2, α) == g3(α)
62  assert f(x=r1, y=r2, z=α) == g3(z=α)
63  
64  # The verifier is now convinced the claimed_eval is correct.
65  # They did not need to sum a whole load of evaluations.
66