Skip to content
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
63 commits
Select commit Hold shift + click to select a range
755ca64
generate septic sum layer witnesses
kunxian-xia Sep 8, 2025
3862bc5
support ec add in tower verifier: wip
kunxian-xia Sep 9, 2025
3ac7ffc
ecc accumulation batched into tower verifier
kunxian-xia Sep 10, 2025
c8f1013
wip
kunxian-xia Sep 11, 2025
0350253
simplify
kunxian-xia Sep 11, 2025
9dd7ade
batch ec add into tower prover wip-1
kunxian-xia Sep 12, 2025
f22d7aa
revisit infer_septic_addition_witness
kunxian-xia Sep 15, 2025
7b366a1
sample random point on curve
kunxian-xia Sep 16, 2025
58d9d22
add sqrt
kunxian-xia Sep 17, 2025
463a431
fix ec add
kunxian-xia Sep 17, 2025
56c7aa4
infer_ec_sum_witness unit test
kunxian-xia Sep 18, 2025
c5c9c11
return point at infinity for Default
kunxian-xia Sep 19, 2025
dc4445a
finish infer septic addition unit test
kunxian-xia Sep 19, 2025
7887206
adjust the ec add sumchecks
kunxian-xia Sep 22, 2025
febb1f2
support jacobian coordinates
kunxian-xia Sep 23, 2025
a266248
infer septic sum using jacobian coordinates
kunxian-xia Sep 24, 2025
d22f76d
update tower verifier for jacobian coordinates
kunxian-xia Sep 25, 2025
a662a49
jacobian coordinates in tower's sumcheck
kunxian-xia Sep 26, 2025
502b7b2
add quark prover for ecc addition
kunxian-xia Sep 29, 2025
c3391bb
sanity check on quark's zerocheck
kunxian-xia Sep 29, 2025
ed67cd3
delete ec addition using tower tree
kunxian-xia Sep 29, 2025
be0629c
delete
kunxian-xia Sep 29, 2025
74af34f
clean
kunxian-xia Sep 29, 2025
94ac488
add selector to turn off affine_add when b = 1...1
kunxian-xia Sep 29, 2025
6074b14
add quark ecc verifier
kunxian-xia Sep 30, 2025
f3392ea
reorg
kunxian-xia Sep 30, 2025
06312d6
refine comments
kunxian-xia Sep 30, 2025
96a181f
refine comments
kunxian-xia Sep 30, 2025
d2e0d51
add poseidon2 gadget
kunxian-xia Oct 10, 2025
7248eec
global chip wip
kunxian-xia Oct 13, 2025
912747e
upgrade gkr-backend to v1.0.0-alpha.10
kunxian-xia Oct 13, 2025
27113d1
Merge remote-tracking branch 'origin/master' into feat/septic_global_…
kunxian-xia Oct 13, 2025
098afb9
chore
kunxian-xia Oct 13, 2025
6e2f8d6
make Instruction stateful
kunxian-xia Oct 13, 2025
160291e
make all opcode circuits to be stateful
kunxian-xia Oct 13, 2025
8860169
fmt
kunxian-xia Oct 13, 2025
706aa08
global chip unit test wip
kunxian-xia Oct 14, 2025
4d7423b
finish most constraints for Global chip
kunxian-xia Oct 14, 2025
4900dc8
global chip unit test wip2
kunxian-xia Oct 16, 2025
64ab29e
remove r_record / w_record
kunxian-xia Oct 16, 2025
9649633
wip3
kunxian-xia Oct 19, 2025
f20e970
make record to be trait Instruction's associated type
kunxian-xia Oct 19, 2025
cfd9870
wip4
kunxian-xia Oct 19, 2025
253043f
wip5
kunxian-xia Oct 19, 2025
ae46b8e
wip6
kunxian-xia Oct 19, 2025
6601cf1
evaluate selector with context
kunxian-xia Oct 20, 2025
7efb21a
switch gkr-backend
kunxian-xia Oct 21, 2025
636ab8e
fix
kunxian-xia Oct 21, 2025
052b567
enable poseidon2
kunxian-xia Oct 21, 2025
9e5df7d
integrate ecc quark iop wip
kunxian-xia Oct 22, 2025
de8397f
non-pow2 septic elliptic curve points add IOP (#1081)
hero78119 Oct 27, 2025
bcd3eb9
Feat: integrate ecc quark prover into prover's and verifier's workflo…
kunxian-xia Oct 28, 2025
1686647
Merge remote-tracking branch 'origin/feat/multi_shard' into feat/sept…
kunxian-xia Oct 28, 2025
2d8d643
chores: fix quick error in e2e (#1096)
hero78119 Oct 28, 2025
9676da8
rw record ramtype expression (#1098)
hero78119 Oct 29, 2025
2d5ed66
Feat: integrate `Global` chip into e2e workflow (#1099)
kunxian-xia Oct 30, 2025
a8a06a5
Fix integration bugs (#1102)
kunxian-xia Oct 31, 2025
2214fdc
extract shard id from cycle (#1101)
hero78119 Oct 31, 2025
3860d14
revert stateful trait Instruction (#1105)
kunxian-xia Oct 31, 2025
5af8392
refactor ec points witness assignments (#1100)
hero78119 Oct 31, 2025
9917b61
#1061 cleanup (#1106)
kunxian-xia Oct 31, 2025
184b82c
bug fix of global chip (#1109)
hero78119 Nov 2, 2025
11e42d2
CI: disable `fibonacci + goldilocks` integration test (#1110)
kunxian-xia Nov 3, 2025
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
1 change: 1 addition & 0 deletions ceno_zkvm/src/scheme.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ pub mod cpu;
pub mod gpu;
pub mod hal;
pub mod prover;
pub mod septic_curve;
pub mod utils;
pub mod verifier;

Expand Down
239 changes: 239 additions & 0 deletions ceno_zkvm/src/scheme/septic_curve.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,239 @@
// The extension field and curve definition are adapted from
// https://github.com/succinctlabs/sp1/blob/v5.2.1/crates/stark/src/septic_curve.rs
use p3::field::Field;
use std::ops::{Add, Deref, Mul, Sub};

/// F[z] / (z^6 - z - 4)
///
/// ```sage
/// # finite field F = GF(2^31 - 2^27 + 1)
/// p = 2^31 - 2^27 + 1
/// F = GF(p)
///
/// # polynomial ring over F
/// R.<x> = PolynomialRing(F)
/// f = x^6 - x - 4
///
/// # check if f(x) is irreducible
/// print(f.is_irreducible())
/// ```
pub struct SexticExtension<F>([F; 6]);

/// F[z] / (z^7 - 2z - 5)
///
/// ```sage
/// # finite field F = GF(2^31 - 2^27 + 1)
/// p = 2^31 - 2^27 + 1
/// F = GF(p)
///
/// # polynomial ring over F
/// R.<x> = PolynomialRing(F)
/// f = x^7 - 2x - 5
///
/// # check if f(x) is irreducible
/// print(f.is_irreducible())
/// ```
#[derive(Clone, Debug, Default, PartialEq)]
pub struct SepticExtension<F>(pub [F; 7]);

impl<F: Copy + Clone + Default> From<&[F]> for SepticExtension<F> {
fn from(slice: &[F]) -> Self {
assert!(slice.len() == 7);
let mut arr = [F::default(); 7];
arr.copy_from_slice(&slice[0..7]);
Self(arr)
}
}

impl<F> Deref for SepticExtension<F> {
type Target = [F];

fn deref(&self) -> &[F] {
&self.0
}
}

impl<F: Field> SepticExtension<F> {
pub fn is_zero(&self) -> bool {
self.0.iter().all(|c| *c == F::ZERO)
}

pub fn inverse(&self) -> Option<Self> {
match self.is_zero() {
true => None,
false => {
todo!()
}
}
}

pub fn square(&self) -> Self {
let mut result = [F::ZERO; 7];
let two = F::from_canonical_u32(2);
let five = F::from_canonical_u32(5);

// i < j
for i in 0..7 {
for j in (i + 1)..7 {
let term = two * self.0[i] * self.0[j];
let mut index = i + j;
if index < 7 {
result[index] += term;
} else {
index -= 7;
// x^7 = 2x + 5
result[index] += five * term;
result[index + 1] += two * term;
}
}
}
// i == j
result[0] += self.0[0] * self.0[0];
result[2] += self.0[1] * self.0[1];
result[4] += self.0[2] * self.0[2];
result[6] += self.0[3] * self.0[3];
// a4^2 * x^8 = a4^2 * (2x + 5)x = 5a4^2 * x + 2a4^2 * x^2
let term = self.0[4] * self.0[4];
result[1] += five * term;
result[2] += two * term;
// a5^2 * x^10 = a5^2 * (2x + 5)x^3 = 5a5^2 * x^3 + 2a5^2 * x^4
let term = self.0[5] * self.0[5];
result[3] += five * term;
result[4] += two * term;
// a6^2 * x^12 = a6^2 * (2x + 5)x^5 = 5a6^2 * x^5 + 2a6^2 * x^6
let term = self.0[6] * self.0[6];
result[5] += five * term;
result[6] += two * term;

Self(result)
}
}

impl<F: Field> From<[u32; 7]> for SepticExtension<F> {
fn from(arr: [u32; 7]) -> Self {
let mut result = [F::ZERO; 7];
for i in 0..7 {
result[i] = F::from_canonical_u32(arr[i]);
}
Self(result)
}
}

impl<F: Field> Add<&Self> for SepticExtension<F> {
type Output = Self;

fn add(self, other: &Self) -> Self {
let mut result = [F::ZERO; 7];
for i in 0..7 {
result[i] = self.0[i] + other.0[i];
}
Self(result)
}
}

impl<F: Field> Add for SepticExtension<F> {
type Output = Self;

fn add(self, other: Self) -> Self {
self.add(&other)
}
}

impl<F: Field> Sub<&Self> for SepticExtension<F> {
type Output = Self;

fn sub(self, other: &Self) -> Self {
let mut result = [F::ZERO; 7];
for i in 0..7 {
result[i] = self.0[i] - other.0[i];
}
Self(result)
}
}

impl<F: Field> Sub for SepticExtension<F> {
type Output = Self;

fn sub(self, other: Self) -> Self {
self.sub(&other)
}
}

impl<F: Field> Mul<&Self> for SepticExtension<F> {
type Output = Self;

fn mul(self, other: &Self) -> Self {
let mut result = [F::ZERO; 7];
let five = F::from_canonical_u32(5);
let two = F::from_canonical_u32(2);
for i in 0..7 {
for j in 0..7 {
let term = self.0[i] * other.0[j];
let mut index = i + j;
if index < 7 {
result[index] += term;
} else {
index -= 7;
// x^7 = 2x + 5
result[index] += five * term;
result[index + 1] += two * term;
}
}
}
Self(result)
}
}

impl<F: Field> Mul for SepticExtension<F> {
type Output = Self;

fn mul(self, other: Self) -> Self {
self.mul(&other)
}
}

/// A point on the short Weierstrass curve defined by
/// y^2 = x^3 + 2x + 26z^5
/// over the extension field F[z] / (z^7 - 2z - 5).
///
/// Note that
/// 1. its cofactor is 1
/// 2. its order is a large prime number of 31x7 bits
#[derive(Clone, Debug, Default, PartialEq)]
pub struct SepticPoint<F> {
pub x: SepticExtension<F>,
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

a tiny question: it seems SepticExtension extension field is also a field, so in future both could be define separately?, e.g.

pub struct SepticPoint<F, E<BaseField = F>> {
    pub x: E,
    pub y: E,
}

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yeah, this should work.

pub y: SepticExtension<F>,
}

impl<F: Field> Add<Self> for SepticPoint<F> {
type Output = Self;

fn add(self, other: Self) -> Self {
assert!(other.x != self.x, "other = self or other = -self");
let slope = (other.y - &self.y) * (other.x.clone() - &self.x).inverse().unwrap();
let x = slope.square() - (self.x.clone() + other.x);
let y = slope * (x.clone() - self.x) - self.y;

Self { x, y }
}
}

#[cfg(test)]
mod tests {
use super::SepticExtension;
use p3::babybear::BabyBear;

type F = BabyBear;
#[test]
fn test_septic_extension_arithmetic() {
// a = z, b = z^6 + z^5 + z^4
let a: SepticExtension<F> = SepticExtension::from([0, 1, 0, 0, 0, 0, 0]);
let b: SepticExtension<F> = SepticExtension::from([0, 0, 0, 0, 1, 1, 1]);

assert_eq!(
a * b,
// z^5 + z^6 + 2*z + 5
SepticExtension::from([5, 2, 0, 0, 0, 1, 1])
)
}
}
72 changes: 72 additions & 0 deletions ceno_zkvm/src/scheme/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ use crate::{
scheme::{
constants::MIN_PAR_SIZE,
hal::{MainSumcheckProver, ProofInput, ProverDevice},
septic_curve::{SepticExtension, SepticPoint},
},
structs::ComposedConstrainSystem,
};
Expand All @@ -20,6 +21,7 @@ use multilinear_extensions::{
mle::{ArcMultilinearExtension, FieldType, IntoMLE, MultilinearExtension},
util::ceil_log2,
};
use p3::matrix::{Matrix, dense::RowMajorMatrix};
use rayon::{
iter::{
IndexedParallelIterator, IntoParallelIterator, IntoParallelRefIterator,
Expand Down Expand Up @@ -297,6 +299,76 @@ pub(crate) fn infer_tower_product_witness<E: ExtensionField>(
wit_layers
}

pub fn log2_strict_usize(n: usize) -> usize {
assert!(n.is_power_of_two());
n.trailing_zeros() as usize
}

pub fn infer_septic_sum_witness<E: ExtensionField>(
p_mles: RowMajorMatrix<E::BaseField>,
q_mles: RowMajorMatrix<E::BaseField>,
) -> Vec<Vec<MultilinearExtension<E>>> {
assert!(p_mles.width() > 0);
let num_layers = log2_strict_usize(p_mles.height());

let mut layers = Vec::with_capacity(num_layers);
layers.push(vec![p_mles, q_mles]);
for i in (0..num_layers).rev() {
let last_layer = layers.last().unwrap();
let (p, q) = (&last_layer[0], &last_layer[1]);

let num_rows = p.height();
let new_p = RowMajorMatrix::new(
(0..num_rows / 2)
.into_par_iter()
.flat_map_iter(|row| {
let p = p.row_slice(row);
let q = q.row_slice(row);

let p1 = SepticPoint {
x: SepticExtension(std::array::from_fn(|i| p[i])),
y: SepticExtension(std::array::from_fn(|i| p[i + 7])),
};
let p2 = SepticPoint {
x: SepticExtension(std::array::from_fn(|i| q[i])),
y: SepticExtension(std::array::from_fn(|i| q[i + 7])),
};
let q = p1 + p2;
q.x.0.iter().chain(q.y.0.iter()).copied()
})
.collect::<Vec<_>>(),
14,
);
let new_q = RowMajorMatrix::new(
((num_rows / 2)..num_rows)
.into_par_iter()
.flat_map_iter(|row| {
let p = p.row_slice(row);
let q = q.row_slice(row);

let p1 = SepticPoint {
x: SepticExtension(std::array::from_fn(|i| p[i])),
y: SepticExtension(std::array::from_fn(|i| p[i + 7])),
};
let p2 = SepticPoint {
x: SepticExtension(std::array::from_fn(|i| q[i])),
y: SepticExtension(std::array::from_fn(|i| q[i + 7])),
};
let q = p1 + p2;
q.x.0.iter().chain(q.y.0.iter()).copied()
})
.collect::<Vec<_>>(),
14,
);
layers.push(vec![new_p, new_q]);
}

layers
.iter()
.rev()
.map(|layer| layer.iter().map(|m| m.into_mles()).collect::<Vec<_>>())
}

pub fn build_main_witness<
'a,
E: ExtensionField,
Expand Down
Loading
Loading