Skip to content

Generate linear and quadratic constraints from padded sumcheck proof #39

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 29, 2025
Merged

Generate linear and quadratic constraints from padded sumcheck proof #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
196 changes: 143 additions & 53 deletions src/circuit.rs
View file
Open in desktop

Large diffs are not rendered by default.

34 changes: 33 additions & 1 deletion src/fields/field2_128/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ use subtle::ConstantTimeEq;

use crate::{
Codec,
fields::{CodecFieldElement, FieldElement},
fields::{CodecFieldElement, FieldElement, LagrangePolynomialFieldElement},
};

/// An element of the field GF(2^128).
Expand All @@ -44,6 +44,38 @@ impl CodecFieldElement for Field2_128 {
const NUM_BITS: u32 = 128;
}

impl LagrangePolynomialFieldElement for Field2_128 {
fn sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF2 = GF(2)
// x = polygen(GF2)
// GF2_128.<x> = GF2.extension(x^128 + x^7 + x^2 + x + 1)
// GF2_128(x).inverse().to_integer()
Self::from_u128(170141183460469231731687303715884105795)
}

fn one_minus_sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF2 = GF(2)
// x = polygen(GF2)
// GF2_128.<x> = GF2.extension(x^128 + x^7 + x^2 + x + 1)
// GF2_128(1 - x).inverse().to_integer()
Self::from_u128(340282366920938463463374607431768211330)
}

fn sumcheck_p2_squared_minus_sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF2 = GF(2)
// x = polygen(GF2)
// GF2_128.<x> = GF2.extension(x^128 + x^7 + x^2 + x + 1)
// GF2_128(x^2 - x).inverse().to_integer()
Self::from_u128(170141183460469231731687303715884105665)
}
}

impl Debug for Field2_128 {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "Field2_128(0x{:032x})", self.0)
Expand Down
31 changes: 30 additions & 1 deletion src/fields/fieldp128/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use subtle::ConstantTimeEq;
use crate::{
Codec,
fields::{
CodecFieldElement, FieldElement,
CodecFieldElement, FieldElement, LagrangePolynomialFieldElement,
fieldp128::ops::{
fiat_p128_add, fiat_p128_from_bytes, fiat_p128_from_montgomery,
fiat_p128_montgomery_domain_field_element, fiat_p128_mul,
Expand Down Expand Up @@ -95,6 +95,35 @@ impl CodecFieldElement for FieldP128 {
const NUM_BITS: u32 = 128;
}

impl LagrangePolynomialFieldElement for FieldP128 {
fn sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF(2^128-2^108+1)(2).inverse().to_bytes(byteorder='little')
//
// Unwrap safety: this constant is a valid field element.
Self::try_from(b"\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf8\xff\x7f").unwrap()
}

fn one_minus_sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF(2^128-2^108+1)(1 - 2).inverse().to_bytes(byteorder='little')
//
// Unwrap safety: this constant is a valid field element.
Self::try_from(b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf0\xff\xff").unwrap()
}

fn sumcheck_p2_squared_minus_sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF(2^128-2^108+1)(2^2 - 2).inverse().to_bytes(byteorder='little')
//
// Unwrap safety: this constant is a valid field element.
Self::try_from(b"\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf8\xff\x7f").unwrap()
}
}

impl Debug for FieldP128 {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
let residue = self.as_residue();
Expand Down
46 changes: 45 additions & 1 deletion src/fields/fieldp256/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use subtle::ConstantTimeEq;
use crate::{
Codec,
fields::{
CodecFieldElement, FieldElement,
CodecFieldElement, FieldElement, LagrangePolynomialFieldElement,
fieldp256::ops::{
fiat_p256_add, fiat_p256_from_bytes, fiat_p256_from_montgomery,
fiat_p256_montgomery_domain_field_element, fiat_p256_mul,
Expand Down Expand Up @@ -90,6 +90,50 @@ impl CodecFieldElement for FieldP256 {
const NUM_BITS: u32 = 256;
}

impl LagrangePolynomialFieldElement for FieldP256 {
fn sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF(0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff)(2) \
// .inverse().to_bytes(byteorder='little')
//
// Unwrap safety: this constant is a valid field element.
Self::try_from(
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\
\x00\x00\x80\x00\x00\x00\x80\xff\xff\xff\x7f",
)
.unwrap()
}

fn one_minus_sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF(0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff)(1 - 2) \
// .inverse().to_bytes(byteorder='little')
//
// Unwrap safety: this constant is a valid field element.
Self::try_from(
b"\xfe\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\
\x00\x00\x00\x01\x00\x00\x00\xff\xff\xff\xff",
)
.unwrap()
}

fn sumcheck_p2_squared_minus_sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF(0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff)(2^2 - 2) \
// .inverse().to_bytes(byteorder='little')
//
// Unwrap safety: this constant is a valid field element.
Self::try_from(
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\
\x00\x00\x80\x00\x00\x00\x80\xff\xff\xff\x7f",
)
.unwrap()
}
}

impl Debug for FieldP256 {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
let residue = self.as_residue();
Expand Down
49 changes: 48 additions & 1 deletion src/fields/fieldp521/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use subtle::ConstantTimeEq;
use crate::{
Codec,
fields::{
CodecFieldElement, FieldElement,
CodecFieldElement, FieldElement, LagrangePolynomialFieldElement,
fieldp521::ops::{
fiat_p521_carry_add, fiat_p521_carry_mul, fiat_p521_carry_opp, fiat_p521_carry_square,
fiat_p521_carry_sub, fiat_p521_from_bytes, fiat_p521_loose_field_element,
Expand Down Expand Up @@ -83,6 +83,53 @@ impl CodecFieldElement for FieldP521 {
const NUM_BITS: u32 = 521;
}

impl LagrangePolynomialFieldElement for FieldP521 {
fn sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF(2^521 - 1)(2).inverse().to_bytes(byteorder='little')
//
// Unwrap safety: this constant is a valid field element.
Self::try_from(
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
\x00\x00\x01",
)
.unwrap()
}

fn one_minus_sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF(2^521 - 1)(1 - 2).inverse().to_bytes(byteorder='little')
//
// Unwrap safety: this constant is a valid field element.
Self::try_from(
b"\xfe\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\
\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\
\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\
\xff\xff\x01",
)
.unwrap()
}

fn sumcheck_p2_squared_minus_sumcheck_p2_mul_inv() -> Self {
// Computed in SageMath:
//
// GF(2^521 - 1)(2^2 - 2).inverse().to_bytes(byteorder='little')
//
// Unwrap safety: this constant is a valid field element.
Self::try_from(
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\
\x00\x00\x01",
)
.unwrap()
}
}

impl Debug for FieldP521 {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
let mut bytes = [0u8; 66];
Expand Down
112 changes: 110 additions & 2 deletions src/fields/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,63 @@ pub trait CodecFieldElement:
}
}

/// Elements of a field in which we can interpolate polynomials up to degree two. Our nodes are
/// `x_0 = 0`, `x_1 = 1`, and `x_2 = SUMCHECK_P2` in the field. Since we only have three nodes, we
/// can work out each Lagrange basis polynomial by hand. We precompute the denominators to avoid
/// implementing division.
///
/// For details see [Section 6.6][1] and [2].
///
/// # Bugs
///
/// The methods `sumcheck_p2_mul_inv`, `one_minus_sumcheck_p2_mul_inv`,
/// `sumcheck_p2_squared_minus_sumcheck_p2_mul_inv` should be constants ([3]).
///
/// [1]: https://datatracker.ietf.org/doc/html/draft-google-cfrg-libzk-01#section-6.6
/// [2]: https://en.wikipedia.org/wiki/Lagrange_polynomial#Definition
/// [3]: https://github.com/abetterinternet/zk-cred-longfellow/issues/40
pub trait LagrangePolynomialFieldElement: FieldElement {
/// Evaluate the 0th Lagrange basis polynomial at x.
fn lagrange_basis_polynomial_0(x: Self) -> Self {
// (x - x_1) * (x - x_2)
(x - Self::ONE) * (x - Self::SUMCHECK_P2)
// (x_0 - x_1) * (x_0 - x_2) = (0 - 1) * (0 - SUMCHECK_P2) = SUMCHECK_P2
* Self::sumcheck_p2_mul_inv()
}

/// Evaluate the 1st Lagrange basis polynomial at x.
fn lagrange_basis_polynomial_1(x: Self) -> Self {
// (x - x_0) * (x - x_2)
(x - Self::ZERO) * (x - Self::SUMCHECK_P2)
// (x_1 - x_0) * (x_1 - x_2) = (1 - 0) * (1 - SUMCHECK_P2) = 1 - SUMCHECK_P2
* Self::one_minus_sumcheck_p2_mul_inv()
}

/// Evaluate the 2nd Lagrange basis polynomial at x.
fn lagrange_basis_polynomial_2(x: Self) -> Self {
// (x - x_0) * (x - x_1)
(x - Self::ZERO) * (x - Self::ONE)
// (x_2 - x_0) * (x_2 - x_1) = (SUMCHECK_P2 - 0) * (SUMCHECK_P2 - 1)
// = SUMCHECK_P2^2 - SUMCHECK_P2
* Self::sumcheck_p2_squared_minus_sumcheck_p2_mul_inv()
}

/// The multiplicative inverse of `SUMCHECK_P2`. Denominator of the 0th Lagrange basis
/// polynomial.
// TODO: This could probably be a constant.
fn sumcheck_p2_mul_inv() -> Self;

/// The multiplicative inverse of `1 - SUMCHECK_P2`. Denominator of the 1st Lagrange basis
/// polynomial.
// TODO: This could probably be a constant.
fn one_minus_sumcheck_p2_mul_inv() -> Self;

/// The multiplicative inverse of `SUMCHECK_P2^2 - SUMCHECK_P2`. Denominator of the 2nd Lagrange
/// basis polynomial.
// TODO: This could probably be a constant.
fn sumcheck_p2_squared_minus_sumcheck_p2_mul_inv() -> Self;
}

/// Field identifier. According to the draft specification, the encoding is of variable length ([1])
/// but in the Longfellow implementation ([2]), they're always 3 bytes long.
///
Expand Down Expand Up @@ -248,12 +305,11 @@ mod tests {
fields::{
CodecFieldElement, FieldElement, FieldId, SerializedFieldElement,
field2_128::Field2_128, fieldp128::FieldP128, fieldp256::FieldP256,
fieldp256_2::FieldP256_2,
},
};
use std::io::Cursor;

use super::fieldp521::FieldP521;
use super::{LagrangePolynomialFieldElement, fieldp256_2::FieldP256_2, fieldp521::FieldP521};

#[test]
fn codec_roundtrip_field_p128() {
Expand Down Expand Up @@ -480,22 +536,38 @@ mod tests {
assert_eq!(F::from_u128(u64::MAX as u128), F::from(u64::MAX));
}

fn field_element_test_mul_inv<F: LagrangePolynomialFieldElement>() {
assert_eq!(F::sumcheck_p2_mul_inv() * F::SUMCHECK_P2, F::ONE);
assert_eq!(
F::one_minus_sumcheck_p2_mul_inv() * (F::ONE - F::SUMCHECK_P2),
F::ONE
);
assert_eq!(
F::sumcheck_p2_squared_minus_sumcheck_p2_mul_inv()
* ((F::SUMCHECK_P2 * F::SUMCHECK_P2) - F::SUMCHECK_P2),
F::ONE
);
}

#[test]
fn test_field_p256() {
field_element_test_large_characteristic::<FieldP256>();
field_element_test_codec::<FieldP256>(true);
field_element_test_mul_inv::<FieldP256>();
}

#[test]
fn test_field_p128() {
field_element_test_large_characteristic::<FieldP128>();
field_element_test_codec::<FieldP128>(true);
field_element_test_mul_inv::<FieldP128>();
}

#[test]
fn test_field_p521() {
field_element_test_large_characteristic::<FieldP521>();
field_element_test_codec::<FieldP521>(true);
field_element_test_mul_inv::<FieldP521>();
}

#[test]
Expand All @@ -506,6 +578,7 @@ mod tests {
#[test]
fn test_field_2_128() {
field_element_test_codec::<Field2_128>(false);
field_element_test_mul_inv::<Field2_128>();
}

#[test]
Expand Down Expand Up @@ -567,4 +640,39 @@ mod tests {
fn sample() {
FieldP128::sample();
}

fn lagrange_basis_polynomial_test<FE: LagrangePolynomialFieldElement>() {
// lag_i is 1 at i and 0 at the other nodes
assert_eq!(FE::lagrange_basis_polynomial_0(FE::ZERO), FE::ONE);
assert_eq!(FE::lagrange_basis_polynomial_0(FE::ONE), FE::ZERO);
assert_eq!(FE::lagrange_basis_polynomial_0(FE::SUMCHECK_P2), FE::ZERO);

assert_eq!(FE::lagrange_basis_polynomial_1(FE::ZERO), FE::ZERO);
assert_eq!(FE::lagrange_basis_polynomial_1(FE::ONE), FE::ONE);
assert_eq!(FE::lagrange_basis_polynomial_1(FE::SUMCHECK_P2), FE::ZERO);

assert_eq!(FE::lagrange_basis_polynomial_2(FE::ZERO), FE::ZERO);
assert_eq!(FE::lagrange_basis_polynomial_2(FE::ONE), FE::ZERO);
assert_eq!(FE::lagrange_basis_polynomial_2(FE::SUMCHECK_P2), FE::ONE);
}

#[test]
fn lagrange_basis_polynomial_field_p128() {
lagrange_basis_polynomial_test::<FieldP128>();
}

#[test]
fn lagrange_basis_polynomial_field_p256() {
lagrange_basis_polynomial_test::<FieldP256>();
}

#[test]
fn lagrange_basis_polynomial_field_p521() {
lagrange_basis_polynomial_test::<FieldP521>();
}

#[test]
fn lagrange_basis_polynomial_field_2_128() {
lagrange_basis_polynomial_test::<Field2_128>();
}
}
Loading