Skip to content

Commit 4be42ea

Browse files
tgeoghegantgeoghegan
committed
Ligero constraints from the padded sumcheck proof
Implements generation of linear and quadratic constraints from a padded sumcheck proof, specified in 6.6 [1] and 4.4 [2]. - `fields`: for efficient computation of Lagrange basis polynomials, we add trait `LagrangePolynomialFieldElement`, which defines methods for the basis polynomial denomimators and methods for evaluating basis polynomials 0, 1, and 2. - `sumcheck/witness`: computes the layout of the witness vector, needed for symbolic manipulation of quantities in constraints and eventually for construction of Ligero commitment and proof. - `sumcheck/symbolic`: allows computing symbolic expressions consisting of terms of the form `a + bx`, where `a` is a known quantity, `x` is some unknown element of the witness vector and `b` is a constant scale factor. - `sumcheck/bind`: implements the `bindeq` function of 6.2 [3]. - `sumcheck/mod`: sumcheck prover now emits the witness vector and Fiat-Shamir transcript so they may be used to validate constraints. - `sumcheck/constraints`: implements the constraint generation of 6.6. In order to valiate the correctness of all this, we also modify `longfellow-zk` to emit a Ligero commitment and constraints when running `zk_test.cc` [4]. More work on test vector generation from C++ is needed. [1]: https://datatracker.ietf.org/doc/html/draft-google-cfrg-libzk-01#section-4.4 [2]: https://datatracker.ietf.org/doc/html/draft-google-cfrg-libzk-01#section-6.6 [3]: https://datatracker.ietf.org/doc/html/draft-google-cfrg-libzk-01#section-6.2 [4]: https://github.com/tgeoghegan/longfellow-zk/tree/constraint-test-vector
1 parent 66caf9f commit 4be42ea

File tree

14 files changed

+1617
-199
lines changed

14 files changed

+1617
-199
lines changed

‎src/circuit.rs‎

Lines changed: 143 additions & 53 deletions
Large diffs are not rendered by default.

‎src/fields/field2_128/mod.rs‎

Lines changed: 46 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ use subtle::ConstantTimeEq;
1717

1818
use crate::{
1919
Codec,
20-
fields::{CodecFieldElement, FieldElement},
20+
fields::{CodecFieldElement, FieldElement, LagrangePolynomialFieldElement},
2121
};
2222

2323
/// An element of the field GF(2^128).
@@ -44,6 +44,51 @@ impl CodecFieldElement for Field2_128 {
4444
const NUM_BITS: u32 = 128;
4545
}
4646

47+
impl LagrangePolynomialFieldElement for Field2_128 {
48+
fn sumcheck_p2_mul_inv() -> Self {
49+
// Computed in SageMath:
50+
//
51+
// GF2 = GF(2)
52+
// x = polygen(GF2)
53+
// GF2_128.<x> = GF2.extension(x^128 + x^7 + x^2 + x + 1)
54+
// GF2_128(x).to_bytes(byteorder='little')
55+
//
56+
// Unwrap safety: this constant is a valid field element.
57+
Self::try_from(b"C\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80".as_slice())
58+
.unwrap()
59+
}
60+
61+
fn one_minus_sumcheck_p2_mul_inv() -> Self {
62+
// Computed in SageMath:
63+
//
64+
// GF2 = GF(2)
65+
// x = polygen(GF2)
66+
// GF2_128.<x> = GF2.extension(x^128 + x^7 + x^2 + x + 1)
67+
// GF2_128(1 - x).inverse().to_bytes(byteorder='little')
68+
//
69+
// Unwrap safety: this constant is a valid field element.
70+
Self::try_from(
71+
b"\x82\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff".as_slice(),
72+
)
73+
.unwrap()
74+
}
75+
76+
fn sumcheck_p2_squared_minus_sumcheck_p2_mul_inv() -> Self {
77+
// Computed in SageMath:
78+
//
79+
// GF2 = GF(2)
80+
// x = polygen(GF2)
81+
// GF2_128.<x> = GF2.extension(x^128 + x^7 + x^2 + x + 1)
82+
// GF2_128(x^2 - x).inverse().to_bytes(byteorder='little')
83+
//
84+
// Unwrap safety: this constant is a valid field element.
85+
Self::try_from(
86+
b"\xc1\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x7f".as_slice(),
87+
)
88+
.unwrap()
89+
}
90+
}
91+
4792
impl Debug for Field2_128 {
4893
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
4994
write!(f, "Field2_128(0x{:032x})", self.0)

‎src/fields/fieldp128/mod.rs‎

Lines changed: 30 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ use subtle::ConstantTimeEq;
1111
use crate::{
1212
Codec,
1313
fields::{
14-
CodecFieldElement, FieldElement,
14+
CodecFieldElement, FieldElement, LagrangePolynomialFieldElement,
1515
fieldp128::ops::{
1616
fiat_p128_add, fiat_p128_from_bytes, fiat_p128_from_montgomery,
1717
fiat_p128_montgomery_domain_field_element, fiat_p128_mul,
@@ -95,6 +95,35 @@ impl CodecFieldElement for FieldP128 {
9595
const NUM_BITS: u32 = 128;
9696
}
9797

98+
impl LagrangePolynomialFieldElement for FieldP128 {
99+
fn sumcheck_p2_mul_inv() -> Self {
100+
// Computed in SageMath:
101+
//
102+
// GF(2^128-2^108+1)(2).inverse().to_bytes(byteorder='little')
103+
//
104+
// Unwrap safety: this constant is a valid field element.
105+
Self::try_from(b"\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf8\xff\x7f").unwrap()
106+
}
107+
108+
fn one_minus_sumcheck_p2_mul_inv() -> Self {
109+
// Computed in SageMath:
110+
//
111+
// GF(2^128-2^108+1)(1 - 2).inverse().to_bytes(byteorder='little')
112+
//
113+
// Unwrap safety: this constant is a valid field element.
114+
Self::try_from(b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf0\xff\xff").unwrap()
115+
}
116+
117+
fn sumcheck_p2_squared_minus_sumcheck_p2_mul_inv() -> Self {
118+
// Computed in SageMath:
119+
//
120+
// GF(2^128-2^108+1)(2^2 - 2).inverse().to_bytes(byteorder='little')
121+
//
122+
// Unwrap safety: this constant is a valid field element.
123+
Self::try_from(b"\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf8\xff\x7f").unwrap()
124+
}
125+
}
126+
98127
impl Debug for FieldP128 {
99128
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
100129
let residue = self.as_residue();

‎src/fields/fieldp256/mod.rs‎

Lines changed: 45 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ use subtle::ConstantTimeEq;
1111
use crate::{
1212
Codec,
1313
fields::{
14-
CodecFieldElement, FieldElement,
14+
CodecFieldElement, FieldElement, LagrangePolynomialFieldElement,
1515
fieldp256::ops::{
1616
fiat_p256_add, fiat_p256_from_bytes, fiat_p256_from_montgomery,
1717
fiat_p256_montgomery_domain_field_element, fiat_p256_mul,
@@ -90,6 +90,50 @@ impl CodecFieldElement for FieldP256 {
9090
const NUM_BITS: u32 = 256;
9191
}
9292

93+
impl LagrangePolynomialFieldElement for FieldP256 {
94+
fn sumcheck_p2_mul_inv() -> Self {
95+
// Computed in SageMath:
96+
//
97+
// GF(0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff)(2) \
98+
// .inverse().to_bytes(byteorder='little')
99+
//
100+
// Unwrap safety: this constant is a valid field element.
101+
Self::try_from(
102+
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\
103+
\x00\x00\x80\x00\x00\x00\x80\xff\xff\xff\x7f",
104+
)
105+
.unwrap()
106+
}
107+
108+
fn one_minus_sumcheck_p2_mul_inv() -> Self {
109+
// Computed in SageMath:
110+
//
111+
// GF(0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff)(1 - 2) \
112+
// .inverse().to_bytes(byteorder='little')
113+
//
114+
// Unwrap safety: this constant is a valid field element.
115+
Self::try_from(
116+
b"\xfe\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\
117+
\x00\x00\x00\x01\x00\x00\x00\xff\xff\xff\xff",
118+
)
119+
.unwrap()
120+
}
121+
122+
fn sumcheck_p2_squared_minus_sumcheck_p2_mul_inv() -> Self {
123+
// Computed in SageMath:
124+
//
125+
// GF(0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff)(2^2 - 2) \
126+
// .inverse().to_bytes(byteorder='little')
127+
//
128+
// Unwrap safety: this constant is a valid field element.
129+
Self::try_from(
130+
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\
131+
\x00\x00\x80\x00\x00\x00\x80\xff\xff\xff\x7f",
132+
)
133+
.unwrap()
134+
}
135+
}
136+
93137
impl Debug for FieldP256 {
94138
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
95139
let residue = self.as_residue();

‎src/fields/fieldp521/mod.rs‎

Lines changed: 48 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ use subtle::ConstantTimeEq;
1111
use crate::{
1212
Codec,
1313
fields::{
14-
CodecFieldElement, FieldElement,
14+
CodecFieldElement, FieldElement, LagrangePolynomialFieldElement,
1515
fieldp521::ops::{
1616
fiat_p521_carry_add, fiat_p521_carry_mul, fiat_p521_carry_opp, fiat_p521_carry_square,
1717
fiat_p521_carry_sub, fiat_p521_from_bytes, fiat_p521_loose_field_element,
@@ -83,6 +83,53 @@ impl CodecFieldElement for FieldP521 {
8383
const NUM_BITS: u32 = 521;
8484
}
8585

86+
impl LagrangePolynomialFieldElement for FieldP521 {
87+
fn sumcheck_p2_mul_inv() -> Self {
88+
// Computed in SageMath:
89+
//
90+
// GF(2^521 - 1)(2).inverse().to_bytes(byteorder='little')
91+
//
92+
// Unwrap safety: this constant is a valid field element.
93+
Self::try_from(
94+
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
95+
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
96+
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
97+
\x00\x00\x01",
98+
)
99+
.unwrap()
100+
}
101+
102+
fn one_minus_sumcheck_p2_mul_inv() -> Self {
103+
// Computed in SageMath:
104+
//
105+
// GF(2^521 - 1)(1 - 2).inverse().to_bytes(byteorder='little')
106+
//
107+
// Unwrap safety: this constant is a valid field element.
108+
Self::try_from(
109+
b"\xfe\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\
110+
\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\
111+
\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\
112+
\xff\xff\x01",
113+
)
114+
.unwrap()
115+
}
116+
117+
fn sumcheck_p2_squared_minus_sumcheck_p2_mul_inv() -> Self {
118+
// Computed in SageMath:
119+
//
120+
// GF(2^521 - 1)(2^2 - 2).inverse().to_bytes(byteorder='little')
121+
//
122+
// Unwrap safety: this constant is a valid field element.
123+
Self::try_from(
124+
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
125+
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
126+
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
127+
\x00\x00\x01",
128+
)
129+
.unwrap()
130+
}
131+
}
132+
86133
impl Debug for FieldP521 {
87134
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
88135
let mut bytes = [0u8; 66];

‎src/fields/mod.rs‎

Lines changed: 110 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,63 @@ pub trait CodecFieldElement:
117117
}
118118
}
119119

120+
/// Elements of a field in which we can interpolate polynomials up to degree two. Our nodes are
121+
/// `x_0 = 0`, `x_1 = 1`, and `x_2 = SUMCHECK_P2` in the field. Since we only have three nodes, we
122+
/// can work out each Lagrange basis polynomial by hand. We precompute the denominators to avoid
123+
/// implementing division.
124+
///
125+
/// For details see [Section 6.6][1] and [2].
126+
///
127+
/// # Bugs
128+
///
129+
/// The methods `sumcheck_p2_mul_inv`, `one_minus_sumcheck_p2_mul_inv`,
130+
/// `sumcheck_p2_squared_minus_sumcheck_p2_mul_inv` should be constants ([3]).
131+
///
132+
/// [1]: https://datatracker.ietf.org/doc/html/draft-google-cfrg-libzk-01#section-6.6
133+
/// [2]: https://en.wikipedia.org/wiki/Lagrange_polynomial#Definition
134+
/// [3]: https://github.com/abetterinternet/zk-cred-longfellow/issues/40
135+
pub trait LagrangePolynomialFieldElement: FieldElement {
136+
/// Evaluate the 0th Lagrange basis polynomial at x.
137+
fn lagrange_basis_polynomial_0(x: Self) -> Self {
138+
// (x - x_1) * (x - x_2)
139+
(x - Self::ONE) * (x - Self::SUMCHECK_P2)
140+
// (x_0 - x_1) * (x_0 - x_2) = (0 - 1) * (0 - SUMCHECK_P2) = SUMCHECK_P2
141+
* Self::sumcheck_p2_mul_inv()
142+
}
143+
144+
/// Evaluate the 1st Lagrange basis polynomial at x.
145+
fn lagrange_basis_polynomial_1(x: Self) -> Self {
146+
// (x - x_0) * (x - x_2)
147+
(x - Self::ZERO) * (x - Self::SUMCHECK_P2)
148+
// (x_1 - x_0) * (x_1 - x_2) = (1 - 0) * (1 - SUMCHECK_P2) = 1 - SUMCHECK_P2
149+
* Self::one_minus_sumcheck_p2_mul_inv()
150+
}
151+
152+
/// Evaluate the 2nd Lagrange basis polynomial at x.
153+
fn lagrange_basis_polynomial_2(x: Self) -> Self {
154+
// (x - x_0) * (x - x_1)
155+
(x - Self::ZERO) * (x - Self::ONE)
156+
// (x_2 - x_0) * (x_2 - x_1) = (SUMCHECK_P2 - 0) * (SUMCHECK_P2 - 1)
157+
// = SUMCHECK_P2^2 - SUMCHECK_P2
158+
* Self::sumcheck_p2_squared_minus_sumcheck_p2_mul_inv()
159+
}
160+
161+
/// The multiplicative inverse of `SUMCHECK_P2`. Denominator of the 0th Lagrange basis
162+
/// polynomial.
163+
// TODO: This could probably be a constant.
164+
fn sumcheck_p2_mul_inv() -> Self;
165+
166+
/// The multiplicative inverse of `1 - SUMCHECK_P2`. Denominator of the 1st Lagrange basis
167+
/// polynomial.
168+
// TODO: This could probably be a constant.
169+
fn one_minus_sumcheck_p2_mul_inv() -> Self;
170+
171+
/// The multiplicative inverse of `SUMCHECK_P2^2 - SUMCHECK_P2`. Denominator of the 2nd Lagrange
172+
/// basis polynomial.
173+
// TODO: This could probably be a constant.
174+
fn sumcheck_p2_squared_minus_sumcheck_p2_mul_inv() -> Self;
175+
}
176+
120177
/// Field identifier. According to the draft specification, the encoding is of variable length ([1])
121178
/// but in the Longfellow implementation ([2]), they're always 3 bytes long.
122179
///
@@ -248,12 +305,11 @@ mod tests {
248305
fields::{
249306
CodecFieldElement, FieldElement, FieldId, SerializedFieldElement,
250307
field2_128::Field2_128, fieldp128::FieldP128, fieldp256::FieldP256,
251-
fieldp256_2::FieldP256_2,
252308
},
253309
};
254310
use std::io::Cursor;
255311

256-
use super::fieldp521::FieldP521;
312+
use super::{LagrangePolynomialFieldElement, fieldp256_2::FieldP256_2, fieldp521::FieldP521};
257313

258314
#[test]
259315
fn codec_roundtrip_field_p128() {
@@ -480,22 +536,38 @@ mod tests {
480536
assert_eq!(F::from_u128(u64::MAX as u128), F::from(u64::MAX));
481537
}
482538

539+
fn field_element_test_mul_inv<F: LagrangePolynomialFieldElement>() {
540+
assert_eq!(F::sumcheck_p2_mul_inv() * F::SUMCHECK_P2, F::ONE);
541+
assert_eq!(
542+
F::one_minus_sumcheck_p2_mul_inv() * (F::ONE - F::SUMCHECK_P2),
543+
F::ONE
544+
);
545+
assert_eq!(
546+
F::sumcheck_p2_squared_minus_sumcheck_p2_mul_inv()
547+
* ((F::SUMCHECK_P2 * F::SUMCHECK_P2) - F::SUMCHECK_P2),
548+
F::ONE
549+
);
550+
}
551+
483552
#[test]
484553
fn test_field_p256() {
485554
field_element_test_large_characteristic::<FieldP256>();
486555
field_element_test_codec::<FieldP256>(true);
556+
field_element_test_mul_inv::<FieldP256>();
487557
}
488558

489559
#[test]
490560
fn test_field_p128() {
491561
field_element_test_large_characteristic::<FieldP128>();
492562
field_element_test_codec::<FieldP128>(true);
563+
field_element_test_mul_inv::<FieldP128>();
493564
}
494565

495566
#[test]
496567
fn test_field_p521() {
497568
field_element_test_large_characteristic::<FieldP521>();
498569
field_element_test_codec::<FieldP521>(true);
570+
field_element_test_mul_inv::<FieldP521>();
499571
}
500572

501573
#[test]
@@ -506,6 +578,7 @@ mod tests {
506578
#[test]
507579
fn test_field_2_128() {
508580
field_element_test_codec::<Field2_128>(false);
581+
field_element_test_mul_inv::<Field2_128>();
509582
}
510583

511584
#[test]
@@ -567,4 +640,39 @@ mod tests {
567640
fn sample() {
568641
FieldP128::sample();
569642
}
643+
644+
fn lagrange_basis_polynomial_test<FE: LagrangePolynomialFieldElement>() {
645+
// lag_i is 1 at i and 0 at the other nodes
646+
assert_eq!(FE::lagrange_basis_polynomial_0(FE::ZERO), FE::ONE);
647+
assert_eq!(FE::lagrange_basis_polynomial_0(FE::ONE), FE::ZERO);
648+
assert_eq!(FE::lagrange_basis_polynomial_0(FE::SUMCHECK_P2), FE::ZERO);
649+
650+
assert_eq!(FE::lagrange_basis_polynomial_1(FE::ZERO), FE::ZERO);
651+
assert_eq!(FE::lagrange_basis_polynomial_1(FE::ONE), FE::ONE);
652+
assert_eq!(FE::lagrange_basis_polynomial_1(FE::SUMCHECK_P2), FE::ZERO);
653+
654+
assert_eq!(FE::lagrange_basis_polynomial_2(FE::ZERO), FE::ZERO);
655+
assert_eq!(FE::lagrange_basis_polynomial_2(FE::ONE), FE::ZERO);
656+
assert_eq!(FE::lagrange_basis_polynomial_2(FE::SUMCHECK_P2), FE::ONE);
657+
}
658+
659+
#[test]
660+
fn lagrange_basis_polynomial_field_p128() {
661+
lagrange_basis_polynomial_test::<FieldP128>();
662+
}
663+
664+
#[test]
665+
fn lagrange_basis_polynomial_field_p256() {
666+
lagrange_basis_polynomial_test::<FieldP256>();
667+
}
668+
669+
#[test]
670+
fn lagrange_basis_polynomial_field_p521() {
671+
lagrange_basis_polynomial_test::<FieldP521>();
672+
}
673+
674+
#[test]
675+
fn lagrange_basis_polynomial_field_2_128() {
676+
lagrange_basis_polynomial_test::<Field2_128>();
677+
}
570678
}

0 commit comments

Comments
 (0)