Files
darkfi/script/research/zk/sumcheck.sage
2024-07-17 15:16:08 +02:00

67 lines
1.3 KiB
Python
Raw Permalink Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
# Boolean hypercube means a bitstring
# 3d boolean hypercube = ℤ₂³
var("x y z")
f = 3*x*y + 5*x*z + 2*x*y*z + 6
claimed_eval = sum([
f(x=0, y=0, z=0),
f(x=0, y=0, z=1),
f(x=0, y=1, z=0),
f(x=0, y=1, z=1),
f(x=1, y=0, z=0),
f(x=1, y=0, z=1),
f(x=1, y=1, z=0),
f(x=1, y=1, z=1),
])
# We will now prove the claim
assert claimed_eval == 66
# Prover constructs g1 such that g1(0) + g1(1) == claimed_eval
g1_0 = sum([
f(x=0, y=0, z=0),
f(x=0, y=0, z=1),
f(x=0, y=1, z=0),
f(x=0, y=1, z=1),
])
g1_1 = sum([
f(x=1, y=0, z=0),
f(x=1, y=0, z=1),
f(x=1, y=1, z=0),
f(x=1, y=1, z=1),
])
g1 = (1 - x)*g1_0 + x*g1_1
# Verifier:
assert g1(x=0) + g1(x=1) == claimed_eval
r1 = 2
# Prover now constructs g2(y) such that g1(r1) == g2(0) + g2(1)
g2_0 = sum([
f(x=r1, y=0, z=0),
f(x=r1, y=0, z=1),
])
g2_1 = sum([
f(x=r1, y=1, z=0),
f(x=r1, y=1, z=1),
])
g2 = (1 - y)*g2_0 + y*g2_1
# Verifier
assert g2(y=0) + g2(y=1) == g1(x=r1)
r2 = 7
# Prover constructs g3(z) : g2(r2) == g3(0) + g3(1)
g3_0 = f(x=r1, y=r2, z=0)
g3_1 = f(x=r1, y=r2, z=1)
g3 = (1 - z)*g3_0 + z*g3_1
# Now verifier picks a random challenge
α = 9
# and checks f(r1, r2, α) == g3(α)
assert f(x=r1, y=r2, z=α) == g3(z=α)
# The verifier is now convinced the claimed_eval is correct.
# They did not need to sum a whole load of evaluations.