From cc58115e8f412a48893e6760227bc73e66afa0cf Mon Sep 17 00:00:00 2001 From: Tom Grosso Date: Tue, 1 Oct 2024 16:12:43 -0300 Subject: [PATCH 1/3] Add line folding --- stwo_cairo_verifier/src/fri.cairo | 1 + stwo_cairo_verifier/src/fri/folding.cairo | 70 +++++++++++++++++ stwo_cairo_verifier/src/lib.cairo | 1 + stwo_cairo_verifier/src/poly.cairo | 5 +- stwo_cairo_verifier/src/poly/line.cairo | 95 +++++++++++++++++++++-- stwo_cairo_verifier/src/utils.cairo | 40 +++++++++- 6 files changed, 204 insertions(+), 8 deletions(-) create mode 100644 stwo_cairo_verifier/src/fri.cairo create mode 100644 stwo_cairo_verifier/src/fri/folding.cairo diff --git a/stwo_cairo_verifier/src/fri.cairo b/stwo_cairo_verifier/src/fri.cairo new file mode 100644 index 00000000..df23e97e --- /dev/null +++ b/stwo_cairo_verifier/src/fri.cairo @@ -0,0 +1 @@ +pub mod folding; diff --git a/stwo_cairo_verifier/src/fri/folding.cairo b/stwo_cairo_verifier/src/fri/folding.cairo new file mode 100644 index 00000000..b76bf78e --- /dev/null +++ b/stwo_cairo_verifier/src/fri/folding.cairo @@ -0,0 +1,70 @@ +use stwo_cairo_verifier::fields::m31::M31Trait; +use stwo_cairo_verifier::circle::{Coset, CosetImpl}; +use stwo_cairo_verifier::poly::line::{LineDomain, LineDomainImpl}; +use stwo_cairo_verifier::fields::qm31::{QM31, qm31}; +use stwo_cairo_verifier::fields::m31::M31; +use stwo_cairo_verifier::utils::{bit_reverse_index, pow}; +use stwo_cairo_verifier::poly::line::{LineEvaluation, LineEvaluationImpl}; +pub const CIRCLE_TO_LINE_FOLD_STEP: u32 = 1; +pub const FOLD_STEP: u32 = 1; + +/// Folds a degree `d` polynomial into a degree `d/2` polynomial. +pub fn fold_line(eval: @LineEvaluation, alpha: QM31) -> LineEvaluation { + let domain = eval.domain; + let mut values: Array = array![]; + let mut i = 0; + while i < eval.values.len() / 2 { + let x = domain.at(bit_reverse_index(i * pow(2, FOLD_STEP), domain.log_size())); + let f_x = eval.values[2 * i]; + let f_neg_x = eval.values[2 * i + 1]; + let (f0, f1) = ibutterfly(*f_x, *f_neg_x, x.inverse()); + values.append(f0 + alpha * f1); + i += 1; + }; + LineEvaluationImpl::new(domain.double(), values) +} +pub fn ibutterfly(v0: QM31, v1: QM31, itwid: M31) -> (QM31, QM31) { + (v0 + v1, (v0 - v1) * itwid.into()) +} +mod test { + use stwo_cairo_verifier::poly::line::{ + LineEvaluation, SparseLineEvaluation, SparseLineEvaluationImpl + }; + use stwo_cairo_verifier::fields::m31::M31Trait; + use stwo_cairo_verifier::circle::{Coset, CosetImpl}; + use stwo_cairo_verifier::poly::line::{LineDomain, LineDomainImpl}; + use stwo_cairo_verifier::fields::qm31::{QM31, qm31}; + use stwo_cairo_verifier::fields::m31::M31; + use stwo_cairo_verifier::utils::{bit_reverse_index, pow}; + use stwo_cairo_verifier::fri::folding::{FOLD_STEP, CIRCLE_TO_LINE_FOLD_STEP}; + #[test] + fn test_fold_line_1() { + let domain = LineDomainImpl::new(CosetImpl::new(67108864, 1)); + let values = array![ + qm31(440443058, 1252794525, 1129773609, 1309365757), + qm31(974589897, 1592795796, 649052897, 863407657) + ]; + let sparse_line_evaluation = SparseLineEvaluation { + subline_evals: array![LineEvaluation { values, domain }] + }; + let alpha = qm31(1047716961, 506143067, 1065078409, 990356067); + let result = sparse_line_evaluation.fold(alpha); + let expected_result = array![qm31(515899232, 1030391528, 1006544539, 11142505)]; + assert_eq!(expected_result, result); + } + #[test] + fn test_fold_line_2() { + let domain = LineDomainImpl::new(CosetImpl::new(553648128, 1)); + let values = array![ + qm31(730692421, 1363821003, 2146256633, 106012305), + qm31(1387266930, 149259209, 1148988082, 1930518101) + ]; + let sparse_line_evaluation = SparseLineEvaluation { + subline_evals: array![LineEvaluation { values, domain }] + }; + let alpha = qm31(2084521793, 1326105747, 548635876, 1532708504); + let result = sparse_line_evaluation.fold(alpha); + let expected_result = array![qm31(1379727866, 1083096056, 1409020369, 1977903500)]; + assert_eq!(expected_result, result); + } +} diff --git a/stwo_cairo_verifier/src/lib.cairo b/stwo_cairo_verifier/src/lib.cairo index 35fa7705..8aa28a12 100644 --- a/stwo_cairo_verifier/src/lib.cairo +++ b/stwo_cairo_verifier/src/lib.cairo @@ -4,6 +4,7 @@ mod fields; mod poly; mod utils; mod vcs; +mod fri; pub use fields::{BaseField, SecureField}; diff --git a/stwo_cairo_verifier/src/poly.cairo b/stwo_cairo_verifier/src/poly.cairo index 41c6f0c7..0d5a1c72 100644 --- a/stwo_cairo_verifier/src/poly.cairo +++ b/stwo_cairo_verifier/src/poly.cairo @@ -1,3 +1,4 @@ pub mod circle; -mod line; -mod utils; +pub mod line; +pub mod utils; + diff --git a/stwo_cairo_verifier/src/poly/line.cairo b/stwo_cairo_verifier/src/poly/line.cairo index 74dfaba4..8493b0c6 100644 --- a/stwo_cairo_verifier/src/poly/line.cairo +++ b/stwo_cairo_verifier/src/poly/line.cairo @@ -1,21 +1,33 @@ -use stwo_cairo_verifier::fields::SecureField; -use stwo_cairo_verifier::fields::m31::m31; +use core::option::OptionTrait; +use core::clone::Clone; +use core::result::ResultTrait; use stwo_cairo_verifier::poly::utils::fold; +use stwo_cairo_verifier::fields::SecureField; +use stwo_cairo_verifier::fields::m31::{M31, m31, M31Trait}; +use stwo_cairo_verifier::fields::qm31::{QM31, qm31}; +use stwo_cairo_verifier::utils::pow; +use stwo_cairo_verifier::circle::{Coset, CosetImpl}; +use stwo_cairo_verifier::fri::folding::fold_line; -/// A univariate polynomial represented by its coefficients in the line part of the FFT-basis -/// in bit reversed order. -#[derive(Drop, Clone)] +/// A univariate polynomial defined on a [LineDomain]. +#[derive(Debug, Drop, Clone)] pub struct LinePoly { + /// Coefficients of the polynomial in [line_ifft] algorithm's basis. + /// + /// The coefficients are stored in bit-reversed order. pub coeffs: Array, + /// The number of coefficients stored as `log2(len(coeffs))`. pub log_size: u32, } #[generate_trait] pub impl LinePolyImpl of LinePolyTrait { + /// Returns the number of coefficients. fn len(self: @LinePoly) -> usize { self.coeffs.len() } + /// Evaluates the polynomial at a single point. fn eval_at_point(self: @LinePoly, mut x: SecureField) -> SecureField { let mut doublings = array![]; let mut i = 0; @@ -30,6 +42,79 @@ pub impl LinePolyImpl of LinePolyTrait { } } +/// Domain comprising of the x-coordinates of points in a [Coset]. +/// +/// For use with univariate polynomials. +#[derive(Copy, Drop, Debug)] +pub struct LineDomain { + pub coset: Coset, +} + +#[generate_trait] +pub impl LineDomainImpl of LineDomainTrait { + /// Returns a domain comprising of the x-coordinates of points in a coset. + fn new(coset: Coset) -> LineDomain { + LineDomain { coset: coset } + } + + /// Returns the `i`th domain element. + fn at(self: @LineDomain, index: usize) -> M31 { + self.coset.at(index).x + } + + /// Returns the size of the domain. + fn size(self: @LineDomain) -> usize { + self.coset.size() + } + + /// Returns the log size of the domain. + fn log_size(self: @LineDomain) -> usize { + *self.coset.log_size + } + + /// Returns a new domain comprising of all points in current domain doubled. + fn double(self: @LineDomain) -> LineDomain { + LineDomain { coset: self.coset.double() } + } +} + +/// Evaluations of a univariate polynomial on a [LineDomain]. +#[derive(Drop)] +pub struct LineEvaluation { + pub values: Array, + pub domain: LineDomain +} + +#[generate_trait] +pub impl LineEvaluationImpl of LineEvaluationTrait { + /// Creates new [LineEvaluation] from a set of polynomial evaluations over a [LineDomain]. + fn new(domain: LineDomain, values: Array) -> LineEvaluation { + assert_eq!(values.len(), domain.size()); + LineEvaluation { values: values, domain: domain } + } +} + +/// Holds a small foldable subset of univariate SecureField polynomial evaluations. +/// Evaluation is held at the CPU backend. +#[derive(Drop)] +pub struct SparseLineEvaluation { + pub subline_evals: Array, +} + +#[generate_trait] +pub impl SparseLineEvaluationImpl of SparseLineEvaluationTrait { + fn fold(self: @SparseLineEvaluation, alpha: QM31) -> Array { + let mut i = 0; + let mut res: Array = array![]; + while i < self.subline_evals.len() { + let line_evaluation = fold_line(self.subline_evals[i], alpha); + res.append(*line_evaluation.values.at(0)); + i += 1; + }; + return res; + } +} + #[cfg(test)] mod tests { diff --git a/stwo_cairo_verifier/src/utils.cairo b/stwo_cairo_verifier/src/utils.cairo index b444247c..426e8eeb 100644 --- a/stwo_cairo_verifier/src/utils.cairo +++ b/stwo_cairo_verifier/src/utils.cairo @@ -97,9 +97,22 @@ pub fn pow(base: u32, mut exponent: u32) -> u32 { result } +pub fn bit_reverse_index(mut index: usize, mut bits: u32) -> usize { + assert!(bits < 32); + let mut result = 0; + let mut pow_of_two = 1; + while bits > 0 { + result *= 2; + result = result | ((index / pow_of_two) & 1); + pow_of_two *= 2; + bits -= 1; + }; + result +} + #[cfg(test)] mod tests { - use super::pow; + use super::{pow, bit_reverse_index}; #[test] fn test_pow() { @@ -109,5 +122,30 @@ mod tests { assert_eq!(4096, pow(2, 12)); assert_eq!(1048576, pow(2, 20)); } + + #[test] + fn test_bit_reverse() { + // 1 bit + assert_eq!(0, bit_reverse_index(0, 1)); + assert_eq!(1, bit_reverse_index(1, 1)); + + // 2 bits + assert_eq!(0, bit_reverse_index(0, 2)); + assert_eq!(2, bit_reverse_index(1, 2)); + assert_eq!(1, bit_reverse_index(2, 2)); + assert_eq!(3, bit_reverse_index(3, 2)); + + // 3 bits + assert_eq!(0, bit_reverse_index(0, 3)); + assert_eq!(4, bit_reverse_index(1, 3)); + assert_eq!(2, bit_reverse_index(2, 3)); + assert_eq!(6, bit_reverse_index(3, 3)); + + // 16 bits + assert_eq!(24415, bit_reverse_index(64250, 16)); + + // 31 bits + assert_eq!(16448250, bit_reverse_index(800042880, 31)); + } } From 843fb386ed7997add917a5cad48528e174906975 Mon Sep 17 00:00:00 2001 From: Tom Grosso Date: Tue, 1 Oct 2024 16:26:17 -0300 Subject: [PATCH 2/3] Generalize field in CirclePoint --- stwo_cairo_verifier/src/circle.cairo | 189 ++++++++++++++++++---- stwo_cairo_verifier/src/fields/qm31.cairo | 4 + stwo_cairo_verifier/src/poly/circle.cairo | 13 +- 3 files changed, 165 insertions(+), 41 deletions(-) diff --git a/stwo_cairo_verifier/src/circle.cairo b/stwo_cairo_verifier/src/circle.cairo index 3601cfe8..27fa4512 100644 --- a/stwo_cairo_verifier/src/circle.cairo +++ b/stwo_cairo_verifier/src/circle.cairo @@ -1,8 +1,11 @@ -use stwo_cairo_verifier::fields::m31::{M31, m31}; +use stwo_cairo_verifier::fields::m31::M31; +use stwo_cairo_verifier::fields::qm31::{QM31, QM31Trait}; use super::utils::pow; +use core::num::traits::zero::Zero; +use core::num::traits::one::One; -pub const M31_CIRCLE_GEN: CirclePointM31 = - CirclePointM31 { x: M31 { inner: 2 }, y: M31 { inner: 1268011823 }, }; +pub const M31_CIRCLE_GEN: CirclePoint = + CirclePoint:: { x: M31 { inner: 2 }, y: M31 { inner: 1268011823 }, }; pub const CIRCLE_LOG_ORDER: u32 = 31; @@ -15,22 +18,27 @@ pub const CIRCLE_ORDER_BIT_MASK: u32 = 0x7fffffff; // `U32_BIT_MASK` equals 2^32 - 1 pub const U32_BIT_MASK: u64 = 0xffffffff; +/// A point on the complex circle. Treated as an additive group. #[derive(Drop, Copy, Debug, PartialEq, Eq)] -pub struct CirclePointM31 { - pub x: M31, - pub y: M31, +pub struct CirclePoint { + pub x: F, + pub y: F } -#[generate_trait] -pub impl CirclePointM31Impl of CirclePointM31Trait { +pub trait CirclePointTrait, +Sub, +Mul, +Drop, +Copy, +Zero, +One> { // Returns the neutral element of the circle. - fn zero() -> CirclePointM31 { - CirclePointM31 { x: m31(1), y: m31(0) } + fn zero() -> CirclePoint { + CirclePoint:: { x: One::::one(), y: Zero::::zero() } } - fn mul(self: @CirclePointM31, mut scalar: u32) -> CirclePointM31 { - let mut result = Self::zero(); - let mut cur = *self; + fn mul( + self: @CirclePoint, initial_scalar: u128 + ) -> CirclePoint< + F + > { + let mut scalar = initial_scalar; + let mut result: CirclePoint = Self::zero(); + let mut cur: CirclePoint = *self; while scalar > 0 { if scalar & 1 == 1 { result = result + cur; @@ -42,13 +50,28 @@ pub impl CirclePointM31Impl of CirclePointM31Trait { } } -impl CirclePointM31Add of Add { +impl CirclePointAdd, +Sub, +Mul, +Drop, +Copy> of Add> { // The operation of the circle as a group with additive notation. - fn add(lhs: CirclePointM31, rhs: CirclePointM31) -> CirclePointM31 { - CirclePointM31 { x: lhs.x * rhs.x - lhs.y * rhs.y, y: lhs.x * rhs.y + lhs.y * rhs.x } + fn add(lhs: CirclePoint, rhs: CirclePoint) -> CirclePoint { + CirclePoint:: { x: lhs.x * rhs.x - lhs.y * rhs.y, y: lhs.x * rhs.y + lhs.y * rhs.x } + } +} + +pub impl CirclePointM31Impl of CirclePointTrait {} + +pub impl CirclePointQM31Impl of CirclePointTrait {} + +trait ComplexConjugate { + fn complex_conjugate(self: CirclePoint) -> CirclePoint; +} + +pub impl ComplexConjugateImpl of ComplexConjugate { + fn complex_conjugate(self: CirclePoint) -> CirclePoint { + CirclePoint { x: self.x.complex_conjugate(), y: self.y.complex_conjugate() } } } +/// Represents the coset initial + . #[derive(Copy, Clone, Debug, PartialEq, Eq, Drop)] pub struct Coset { // This is an index in the range [0, 2^31) @@ -86,36 +109,63 @@ pub impl CosetImpl of CosetTrait { } } - fn at(self: @Coset, index: usize) -> CirclePointM31 { - M31_CIRCLE_GEN.mul(self.index_at(index)) + fn at(self: @Coset, index: usize) -> CirclePoint:: { + M31_CIRCLE_GEN.mul(self.index_at(index).into()) } + /// Returns the size of the coset. fn size(self: @Coset) -> usize { pow(2, *self.log_size) } + + /// Creates a coset of the form G_2n + \. + /// For example, for n=8, we get the point indices \[1,3,5,7,9,11,13,15\]. + fn odds(log_size: u32) -> Coset { + //CIRCLE_LOG_ORDER + let subgroup_generator_index = Self::subgroup_generator_index(log_size); + Self::new(subgroup_generator_index, log_size) + } + + /// Creates a coset of the form G_4n + . + /// For example, for n=8, we get the point indices \[1,5,9,13,17,21,25,29\]. + /// Its conjugate will be \[3,7,11,15,19,23,27,31\]. + fn half_odds(log_size: u32) -> Coset { + Self::new(Self::subgroup_generator_index(log_size + 2), log_size) + } + + fn subgroup_generator_index(log_size: u32) -> u32 { + assert!(log_size <= CIRCLE_LOG_ORDER); + pow(2, CIRCLE_LOG_ORDER - log_size) + } } #[cfg(test)] mod tests { - use super::{M31_CIRCLE_GEN, CIRCLE_ORDER, CirclePointM31, CirclePointM31Impl, Coset, CosetImpl}; - use stwo_cairo_verifier::fields::m31::m31; + use super::{M31_CIRCLE_GEN, CIRCLE_ORDER, CirclePoint, CirclePointM31Impl, Coset, CosetImpl}; + use core::option::OptionTrait; + use core::array::ArrayTrait; + use core::traits::TryInto; + use super::CirclePointQM31Impl; + use stwo_cairo_verifier::fields::m31::{m31, M31}; + use stwo_cairo_verifier::fields::qm31::{qm31, QM31, QM31One}; + use stwo_cairo_verifier::utils::pow; #[test] fn test_add_1() { - let i = CirclePointM31 { x: m31(0), y: m31(1) }; + let i = CirclePoint:: { x: m31(0), y: m31(1) }; let result = i + i; - let expected_result = CirclePointM31 { x: -m31(1), y: m31(0) }; + let expected_result = CirclePoint:: { x: -m31(1), y: m31(0) }; assert_eq!(result, expected_result); } #[test] fn test_add_2() { - let point_1 = CirclePointM31 { x: m31(750649172), y: m31(1991648574) }; - let point_2 = CirclePointM31 { x: m31(1737427771), y: m31(309481134) }; + let point_1 = CirclePoint:: { x: m31(750649172), y: m31(1991648574) }; + let point_2 = CirclePoint:: { x: m31(1737427771), y: m31(309481134) }; let result = point_1 + point_2; - let expected_result = CirclePointM31 { x: m31(1476625263), y: m31(1040927458) }; + let expected_result = CirclePoint:: { x: m31(1476625263), y: m31(1040927458) }; assert_eq!(result, expected_result); } @@ -123,13 +173,13 @@ mod tests { #[test] fn test_zero_1() { let result = CirclePointM31Impl::zero(); - let expected_result = CirclePointM31 { x: m31(1), y: m31(0) }; + let expected_result = CirclePoint:: { x: m31(1), y: m31(0) }; assert_eq!(result, expected_result); } #[test] fn test_zero_2() { - let point_1 = CirclePointM31 { x: m31(750649172), y: m31(1991648574) }; + let point_1 = CirclePoint:: { x: m31(750649172), y: m31(1991648574) }; let point_2 = CirclePointM31Impl::zero(); let expected_result = point_1.clone(); let result = point_1 + point_2; @@ -139,7 +189,7 @@ mod tests { #[test] fn test_mul_1() { - let point_1 = CirclePointM31 { x: m31(750649172), y: m31(1991648574) }; + let point_1 = CirclePoint:: { x: m31(750649172), y: m31(1991648574) }; let result = point_1.mul(5); let expected_result = point_1 + point_1 + point_1 + point_1 + point_1; @@ -148,7 +198,7 @@ mod tests { #[test] fn test_mul_2() { - let point_1 = CirclePointM31 { x: m31(750649172), y: m31(1991648574) }; + let point_1 = CirclePoint:: { x: m31(750649172), y: m31(1991648574) }; let result = point_1.mul(8); let mut expected_result = point_1 + point_1; expected_result = expected_result + expected_result; @@ -159,9 +209,9 @@ mod tests { #[test] fn test_mul_3() { - let point_1 = CirclePointM31 { x: m31(750649172), y: m31(1991648574) }; + let point_1 = CirclePoint:: { x: m31(750649172), y: m31(1991648574) }; let result = point_1.mul(418776494); - let expected_result = CirclePointM31 { x: m31(1987283985), y: m31(1500510905) }; + let expected_result = CirclePoint:: { x: m31(1987283985), y: m31(1500510905) }; assert_eq!(result, expected_result); } @@ -169,13 +219,20 @@ mod tests { #[test] fn test_generator_order() { let half_order = CIRCLE_ORDER / 2; - let mut result = M31_CIRCLE_GEN.mul(half_order); - let expected_result = CirclePointM31 { x: -m31(1), y: m31(0) }; + let mut result = M31_CIRCLE_GEN.mul(half_order.into()); + let expected_result = CirclePoint:: { x: -m31(1), y: m31(0) }; // Assert `M31_CIRCLE_GEN^{2^30}` equals `-1`. assert_eq!(expected_result, result); } + #[test] + fn test_generator() { + let mut result = M31_CIRCLE_GEN.mul(pow(2, 30).try_into().unwrap()); + let expected_result = CirclePoint:: { x: -m31(1), y: m31(0) }; + assert_eq!(expected_result, result); + } + #[test] fn test_coset_index_at() { let coset = Coset { initial_index: 16777216, log_size: 5, step_size: 67108864 }; @@ -204,7 +261,7 @@ mod tests { fn test_coset_at() { let coset = Coset { initial_index: 16777216, step_size: 67108864, log_size: 5 }; let result = coset.at(17); - let expected_result = CirclePointM31 { x: m31(7144319), y: m31(1742797653) }; + let expected_result = CirclePoint:: { x: m31(7144319), y: m31(1742797653) }; assert_eq!(expected_result, result); } @@ -215,5 +272,69 @@ mod tests { let expected_result = 32; assert_eq!(result, expected_result); } + + #[test] + fn test_qm31_circle_gen() { + let P4: u128 = 21267647892944572736998860269687930881; + + let QM31_CIRCLE_GEN: CirclePoint = CirclePoint::< + QM31 + > { + x: qm31(1, 0, 478637715, 513582971), + y: qm31(992285211, 649143431, 740191619, 1186584352), + }; + + let first_prime = 2; + let last_prime = 368140581013; + let prime_factors: Array<(u128, u32)> = array![ + (first_prime, 33), + (3, 2), + (5, 1), + (7, 1), + (11, 1), + (31, 1), + (151, 1), + (331, 1), + (733, 1), + (1709, 1), + (last_prime, 1), + ]; + + let product = iter_product(first_prime, @prime_factors, last_prime); + + assert_eq!(product, P4 - 1); + + assert_eq!( + QM31_CIRCLE_GEN.x * QM31_CIRCLE_GEN.x + QM31_CIRCLE_GEN.y * QM31_CIRCLE_GEN.y, + QM31One::one() + ); + + assert_eq!(QM31_CIRCLE_GEN.mul(P4 - 1), CirclePointQM31Impl::zero()); + + let mut i = 0; + while i < prime_factors.len() { + let (p, _) = *prime_factors.at(i); + assert_ne!(QM31_CIRCLE_GEN.mul((P4 - 1) / p.into()), CirclePointQM31Impl::zero()); + + i = i + 1; + } + } + + fn iter_product( + first_prime: u128, prime_factors: @Array<(u128, u32)>, last_prime: u128 + ) -> u128 { + let mut accum_product: u128 = 1; + accum_product = accum_product + * pow(first_prime.try_into().unwrap(), 31).into() + * 4; // * 2^33 + let mut i = 1; + while i < prime_factors.len() - 1 { + let (prime, exponent): (u128, u32) = *prime_factors.at(i); + accum_product = accum_product * pow(prime.try_into().unwrap(), exponent).into(); + i = i + 1; + }; + accum_product = accum_product * last_prime; + accum_product + } } diff --git a/stwo_cairo_verifier/src/fields/qm31.cairo b/stwo_cairo_verifier/src/fields/qm31.cairo index f76d4707..a16ad775 100644 --- a/stwo_cairo_verifier/src/fields/qm31.cairo +++ b/stwo_cairo_verifier/src/fields/qm31.cairo @@ -30,6 +30,10 @@ pub impl QM31Impl of QM31Trait { let denom_inverse = denom.inverse(); QM31 { a: self.a * denom_inverse, b: -self.b * denom_inverse } } + + fn complex_conjugate(self: QM31) -> QM31 { + QM31 { a: self.a, b: -self.b } + } } pub impl QM31Add of core::traits::Add { diff --git a/stwo_cairo_verifier/src/poly/circle.cairo b/stwo_cairo_verifier/src/poly/circle.cairo index bd8dd34f..270313bc 100644 --- a/stwo_cairo_verifier/src/poly/circle.cairo +++ b/stwo_cairo_verifier/src/poly/circle.cairo @@ -1,11 +1,10 @@ -use stwo_cairo_verifier::circle::CirclePointM31Trait; use core::option::OptionTrait; use core::clone::Clone; use core::result::ResultTrait; use stwo_cairo_verifier::fields::m31::{M31, m31}; use stwo_cairo_verifier::utils::pow; use stwo_cairo_verifier::circle::{ - Coset, CosetImpl, CirclePointM31, CirclePointM31Impl, M31_CIRCLE_GEN, CIRCLE_ORDER + Coset, CosetImpl, CirclePoint, CirclePointM31Impl, M31_CIRCLE_GEN, CIRCLE_ORDER }; /// A valid domain for circle polynomial interpolation and evaluation. @@ -31,8 +30,8 @@ pub impl CircleDomainImpl of CircleDomainTrait { } } - fn at(self: @CircleDomain, index: usize) -> CirclePointM31 { - M31_CIRCLE_GEN.mul(self.index_at(index)) + fn at(self: @CircleDomain, index: usize) -> CirclePoint:: { + M31_CIRCLE_GEN.mul(self.index_at(index).into()) } } @@ -41,7 +40,7 @@ pub impl CircleDomainImpl of CircleDomainTrait { mod tests { use super::{CircleDomain, CircleDomainTrait}; use stwo_cairo_verifier::circle::{ - Coset, CosetImpl, CirclePointM31, CirclePointM31Impl, M31_CIRCLE_GEN, CIRCLE_ORDER + Coset, CosetImpl, CirclePoint, CirclePointM31Impl, M31_CIRCLE_GEN, CIRCLE_ORDER }; use stwo_cairo_verifier::fields::m31::{M31, m31}; @@ -51,7 +50,7 @@ mod tests { let domain = CircleDomain { half_coset }; let index = 17; let result = domain.at(index); - let expected_result = CirclePointM31 { x: m31(7144319), y: m31(1742797653) }; + let expected_result = CirclePoint:: { x: m31(7144319), y: m31(1742797653) }; assert_eq!(expected_result, result); } @@ -61,7 +60,7 @@ mod tests { let domain = CircleDomain { half_coset }; let index = 37; let result = domain.at(index); - let expected_result = CirclePointM31 { x: m31(9803698), y: m31(2079025011) }; + let expected_result = CirclePoint:: { x: m31(9803698), y: m31(2079025011) }; assert_eq!(expected_result, result); } } From 1a31facc5942f781c663f84f4499424746cf9b9f Mon Sep 17 00:00:00 2001 From: Tom Grosso Date: Tue, 1 Oct 2024 17:05:39 -0300 Subject: [PATCH 3/3] Add circle evaluatio with fold_circle_into_line --- stwo_cairo_verifier/src/fri.cairo | 1 + stwo_cairo_verifier/src/fri/folding.cairo | 60 ++++++- stwo_cairo_verifier/src/fri/verifier.cairo | 2 + stwo_cairo_verifier/src/poly/circle.cairo | 176 ++++++++++++++++++--- 4 files changed, 210 insertions(+), 29 deletions(-) create mode 100644 stwo_cairo_verifier/src/fri/verifier.cairo diff --git a/stwo_cairo_verifier/src/fri.cairo b/stwo_cairo_verifier/src/fri.cairo index df23e97e..dad6f043 100644 --- a/stwo_cairo_verifier/src/fri.cairo +++ b/stwo_cairo_verifier/src/fri.cairo @@ -1 +1,2 @@ pub mod folding; +pub mod verifier; diff --git a/stwo_cairo_verifier/src/fri/folding.cairo b/stwo_cairo_verifier/src/fri/folding.cairo index b76bf78e..1ec71da4 100644 --- a/stwo_cairo_verifier/src/fri/folding.cairo +++ b/stwo_cairo_verifier/src/fri/folding.cairo @@ -1,12 +1,16 @@ use stwo_cairo_verifier::fields::m31::M31Trait; use stwo_cairo_verifier::circle::{Coset, CosetImpl}; +use stwo_cairo_verifier::poly::circle::{CircleDomain, CircleDomainImpl}; use stwo_cairo_verifier::poly::line::{LineDomain, LineDomainImpl}; use stwo_cairo_verifier::fields::qm31::{QM31, qm31}; use stwo_cairo_verifier::fields::m31::M31; use stwo_cairo_verifier::utils::{bit_reverse_index, pow}; +use stwo_cairo_verifier::fri::verifier::{FOLD_STEP, CIRCLE_TO_LINE_FOLD_STEP}; +use stwo_cairo_verifier::poly::circle::{ + CircleEvaluation, SparseCircleEvaluation, SparseCircleEvaluationImpl +}; use stwo_cairo_verifier::poly::line::{LineEvaluation, LineEvaluationImpl}; -pub const CIRCLE_TO_LINE_FOLD_STEP: u32 = 1; -pub const FOLD_STEP: u32 = 1; + /// Folds a degree `d` polynomial into a degree `d/2` polynomial. pub fn fold_line(eval: @LineEvaluation, alpha: QM31) -> LineEvaluation { @@ -21,22 +25,57 @@ pub fn fold_line(eval: @LineEvaluation, alpha: QM31) -> LineEvaluation { values.append(f0 + alpha * f1); i += 1; }; + LineEvaluationImpl::new(domain.double(), values) } + + +/// Folds and accumulates a degree `d` circle polynomial into a degree `d/2` univariate +/// polynomial. +/// +/// Let `src` be the evaluation of a circle polynomial `f` on a +/// [`CircleDomain`] `E`. This function computes evaluations of `f' = f0 +/// + alpha * f1` on the x-coordinates of `E` such that `2f(p) = f0(px) + py * f1(px)`. The +/// evaluations of `f'` are accumulated into `dst` by the formula `dst = dst * alpha^2 + +/// f'`. +pub fn fold_circle_into_line(eval: @CircleEvaluation, alpha: QM31) -> LineEvaluation { + let domain = eval.domain; + let mut values = array![]; + let mut i = 0; + while i < eval.values.len() / 2 { + let p = domain + .at(bit_reverse_index(i * pow(2, CIRCLE_TO_LINE_FOLD_STEP), domain.log_size())); + let f_p = eval.values[2 * i]; + let f_neg_p = eval.values[2 * i + 1]; + let (f0, f1) = ibutterfly(*f_p, *f_neg_p, p.y.inverse()); + values.append(f0 + alpha * f1); + i += 1; + }; + LineEvaluation { values, domain: LineDomainImpl::new(*domain.half_coset) } +} + pub fn ibutterfly(v0: QM31, v1: QM31, itwid: M31) -> (QM31, QM31) { (v0 + v1, (v0 - v1) * itwid.into()) } + + mod test { use stwo_cairo_verifier::poly::line::{ LineEvaluation, SparseLineEvaluation, SparseLineEvaluationImpl }; use stwo_cairo_verifier::fields::m31::M31Trait; use stwo_cairo_verifier::circle::{Coset, CosetImpl}; + use stwo_cairo_verifier::poly::circle::{CircleDomain, CircleDomainImpl}; use stwo_cairo_verifier::poly::line::{LineDomain, LineDomainImpl}; use stwo_cairo_verifier::fields::qm31::{QM31, qm31}; use stwo_cairo_verifier::fields::m31::M31; use stwo_cairo_verifier::utils::{bit_reverse_index, pow}; - use stwo_cairo_verifier::fri::folding::{FOLD_STEP, CIRCLE_TO_LINE_FOLD_STEP}; + use stwo_cairo_verifier::fri::verifier::{FOLD_STEP, CIRCLE_TO_LINE_FOLD_STEP}; + use stwo_cairo_verifier::poly::circle::{ + CircleEvaluation, SparseCircleEvaluation, SparseCircleEvaluationImpl + }; + + #[test] fn test_fold_line_1() { let domain = LineDomainImpl::new(CosetImpl::new(67108864, 1)); @@ -52,6 +91,7 @@ mod test { let expected_result = array![qm31(515899232, 1030391528, 1006544539, 11142505)]; assert_eq!(expected_result, result); } + #[test] fn test_fold_line_2() { let domain = LineDomainImpl::new(CosetImpl::new(553648128, 1)); @@ -67,4 +107,18 @@ mod test { let expected_result = array![qm31(1379727866, 1083096056, 1409020369, 1977903500)]; assert_eq!(expected_result, result); } + + + #[test] + fn test_fold_circle_into_line_1() { + let domain = CircleDomain { half_coset: CosetImpl::new(553648128, 0) }; + let values = array![qm31(807167738, 0, 0, 0), qm31(1359821401, 0, 0, 0)]; + let sparse_circle_evaluation: SparseCircleEvaluation = SparseCircleEvaluation { + subcircle_evals: array![CircleEvaluation { values, domain }] + }; + let alpha = qm31(260773061, 362745443, 1347591543, 1084609991); + let result = sparse_circle_evaluation.fold(alpha); + let expected_result = array![qm31(730692421, 1363821003, 2146256633, 106012305)]; + assert_eq!(expected_result, result); + } } diff --git a/stwo_cairo_verifier/src/fri/verifier.cairo b/stwo_cairo_verifier/src/fri/verifier.cairo new file mode 100644 index 00000000..d7121081 --- /dev/null +++ b/stwo_cairo_verifier/src/fri/verifier.cairo @@ -0,0 +1,2 @@ +pub const CIRCLE_TO_LINE_FOLD_STEP: u32 = 1; +pub const FOLD_STEP: u32 = 1; diff --git a/stwo_cairo_verifier/src/poly/circle.cairo b/stwo_cairo_verifier/src/poly/circle.cairo index 270313bc..35f08b38 100644 --- a/stwo_cairo_verifier/src/poly/circle.cairo +++ b/stwo_cairo_verifier/src/poly/circle.cairo @@ -1,14 +1,16 @@ +use stwo_cairo_verifier::circle::CirclePointTrait; use core::option::OptionTrait; use core::clone::Clone; use core::result::ResultTrait; +use stwo_cairo_verifier::fields::qm31::{QM31, qm31}; use stwo_cairo_verifier::fields::m31::{M31, m31}; use stwo_cairo_verifier::utils::pow; use stwo_cairo_verifier::circle::{ Coset, CosetImpl, CirclePoint, CirclePointM31Impl, M31_CIRCLE_GEN, CIRCLE_ORDER }; +use stwo_cairo_verifier::fri::folding::fold_circle_into_line; /// A valid domain for circle polynomial interpolation and evaluation. -/// /// Valid domains are a disjoint union of two conjugate cosets: `+-C + `. /// The ordering defined on this domain is `C + iG_n`, and then `-C - iG_n`. #[derive(Debug, Copy, Drop, PartialEq, Eq)] @@ -18,10 +20,23 @@ pub struct CircleDomain { #[generate_trait] pub impl CircleDomainImpl of CircleDomainTrait { + /// Given a coset C + , constructs the circle domain +-C + (i.e., + /// this coset and its conjugate). + fn new(half_coset: Coset) -> CircleDomain { + CircleDomain { half_coset } + } + + /// Returns the size of the domain. + fn size(self: @CircleDomain) -> usize { + pow(2, self.log_size()) + } + + /// Returns the log size of the domain. fn log_size(self: @CircleDomain) -> usize { *self.half_coset.log_size + 1 } + /// Returns the circle point index of the `i`th domain element. fn index_at(self: @CircleDomain, index: usize) -> usize { if index < self.half_coset.size() { self.half_coset.index_at(index) @@ -30,37 +45,146 @@ pub impl CircleDomainImpl of CircleDomainTrait { } } - fn at(self: @CircleDomain, index: usize) -> CirclePoint:: { + /// Returns the `i` th domain element. + fn at(self: @CircleDomain, index: usize) -> CirclePoint { M31_CIRCLE_GEN.mul(self.index_at(index).into()) } + + fn new_with_log_size(log_size: u32) -> CircleDomain { + CircleDomain { half_coset: CosetImpl::half_odds(log_size - 1) } + } } +/// An evaluation defined on a [CircleDomain]. +/// The values are ordered according to the [CircleDomain] ordering. +#[derive(Debug, Drop, Clone, PartialEq, Eq)] +pub struct CircleEvaluation { + pub values: Array, + pub domain: CircleDomain, +} -#[cfg(test)] -mod tests { - use super::{CircleDomain, CircleDomainTrait}; - use stwo_cairo_verifier::circle::{ - Coset, CosetImpl, CirclePoint, CirclePointM31Impl, M31_CIRCLE_GEN, CIRCLE_ORDER - }; - use stwo_cairo_verifier::fields::m31::{M31, m31}; - - #[test] - fn test_circle_domain_at_1() { - let half_coset = Coset { initial_index: 16777216, step_size: 67108864, log_size: 5 }; - let domain = CircleDomain { half_coset }; - let index = 17; - let result = domain.at(index); - let expected_result = CirclePoint:: { x: m31(7144319), y: m31(1742797653) }; - assert_eq!(expected_result, result); +#[generate_trait] +pub impl CircleEvaluationImpl of CircleEvaluationTrait { + fn new(domain: CircleDomain, values: Array) -> CircleEvaluation { + CircleEvaluation { values: values, domain: domain } } +} + +/// Holds a foldable subset of circle polynomial evaluations. +#[derive(Drop, Clone, Debug, PartialEq)] +pub struct SparseCircleEvaluation { + pub subcircle_evals: Array +} - #[test] - fn test_circle_domain_at_2() { - let half_coset = Coset { initial_index: 16777216, step_size: 67108864, log_size: 5 }; - let domain = CircleDomain { half_coset }; - let index = 37; - let result = domain.at(index); - let expected_result = CirclePoint:: { x: m31(9803698), y: m31(2079025011) }; - assert_eq!(expected_result, result); +#[generate_trait] +pub impl SparseCircleEvaluationImpl of SparseCircleEvaluationImplTrait { + fn new(subcircle_evals: Array) -> SparseCircleEvaluation { + SparseCircleEvaluation { subcircle_evals: subcircle_evals } } + + fn accumulate( + self: @SparseCircleEvaluation, rhs: @SparseCircleEvaluation, alpha: QM31 + ) -> SparseCircleEvaluation { + assert_eq!(self.subcircle_evals.len(), rhs.subcircle_evals.len()); + let mut subcircle_evals = array![]; + let mut i = 0; + while i < self.subcircle_evals.len() { + let lhs = self.subcircle_evals[i]; + let rhs = rhs.subcircle_evals[i]; + let mut values = array![]; + assert_eq!(lhs.values.len(), rhs.values.len()); + let mut j = 0; + while j < lhs.values.len() { + values.append(*lhs.values[j] * alpha + *rhs.values[j]); + j += 1; + }; + subcircle_evals.append(CircleEvaluation { domain: *lhs.domain, values }); + i += 1; + }; + + SparseCircleEvaluation { subcircle_evals } + } + + fn fold(self: @SparseCircleEvaluation, alpha: QM31) -> Array { + let mut i = 0; + let mut res: Array = array![]; + while i < self.subcircle_evals.len() { + let circle_evaluation = fold_circle_into_line(self.subcircle_evals[i], alpha); + res.append(*circle_evaluation.values.at(0)); + i += 1; + }; + return res; + } +} + +#[test] +fn test_circle_domain_at_1() { + let half_coset = Coset { initial_index: 16777216, step_size: 67108864, log_size: 5 }; + let domain = CircleDomain { half_coset }; + let index = 17; + let result = domain.at(index); + let expected_result = CirclePoint:: { x: m31(7144319), y: m31(1742797653) }; + assert_eq!(expected_result, result); +} + +#[test] +fn test_circle_domain_at_2() { + let half_coset = Coset { initial_index: 16777216, step_size: 67108864, log_size: 5 }; + let domain = CircleDomain { half_coset }; + let index = 37; + let result = domain.at(index); + let expected_result = CirclePoint:: { x: m31(9803698), y: m31(2079025011) }; + assert_eq!(expected_result, result); } + +#[test] +fn test_accumulate_1() { + let alpha = qm31(984186742, 463356387, 533637878, 1417871498); + let lhs = SparseCircleEvaluation { + subcircle_evals: array![ + CircleEvaluation { + values: array![qm31(28672, 0, 0, 0), qm31(36864, 0, 0, 0)], + domain: CircleDomain { half_coset: CosetImpl::new(16777216, 0) } + }, + CircleEvaluation { + values: array![qm31(28672, 0, 0, 0), qm31(36864, 0, 0, 0)], + domain: CircleDomain { half_coset: CosetImpl::new(2030043136, 0) } + }, + CircleEvaluation { + values: array![qm31(2147454975, 0, 0, 0), qm31(2147446783, 0, 0, 0)], + domain: CircleDomain { half_coset: CosetImpl::new(2097152000, 0) } + }, + ] + }; + let rhs = lhs.clone(); + let result = lhs.accumulate(@rhs, alpha); + + let expected_result = SparseCircleEvaluation { + subcircle_evals: array![ + CircleEvaluation { + values: array![ + qm31(667173716, 1020487722, 1791736788, 1346152946), + qm31(1471361534, 84922130, 1076528072, 810417939) + ], + domain: CircleDomain { half_coset: CosetImpl::new(16777216, 0) } + }, + CircleEvaluation { + values: array![ + qm31(667173716, 1020487722, 1791736788, 1346152946), + qm31(1471361534, 84922130, 1076528072, 810417939) + ], + domain: CircleDomain { half_coset: CosetImpl::new(2030043136, 0) } + }, + CircleEvaluation { + values: array![ + qm31(1480309931, 1126995925, 355746859, 801330701), + qm31(676122113, 2062561517, 1070955575, 1337065708) + ], + domain: CircleDomain { half_coset: CosetImpl::new(2097152000, 0) } + }, + ] + }; + + assert_eq!(expected_result, result); +} +