Skip to content
Merged
Show file tree
Hide file tree
Changes from 4 commits
Commits
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
28 changes: 13 additions & 15 deletions ceno_zkvm/src/gadgets/poseidon2.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,25 +41,23 @@ impl<F: Field, const WIDTH: usize, const HALF_FULL_ROUNDS: usize, const PARTIAL_
fn from(value: Vec<F>) -> Self {
let mut iter = value.into_iter();
let mut beginning_full_round_constants = [[F::ZERO; WIDTH]; HALF_FULL_ROUNDS];
for round in 0..HALF_FULL_ROUNDS {
for i in 0..WIDTH {
beginning_full_round_constants[round][i] =
iter.next().expect("insufficient round constants");
}
}

beginning_full_round_constants.iter_mut().for_each(|arr| {
arr.iter_mut()
.for_each(|c| *c = iter.next().expect("insufficient round constants"))
});

let mut partial_round_constants = [F::ZERO; PARTIAL_ROUNDS];
for round in 0..PARTIAL_ROUNDS {
partial_round_constants[round] = iter.next().expect("insufficient round constants");
}

partial_round_constants
.iter_mut()
.for_each(|arr| *arr = iter.next().expect("insufficient round constants"));

let mut ending_full_round_constants = [[F::ZERO; WIDTH]; HALF_FULL_ROUNDS];
for round in 0..HALF_FULL_ROUNDS {
for i in 0..WIDTH {
ending_full_round_constants[round][i] =
iter.next().expect("insufficient round constants");
}
}
ending_full_round_constants.iter_mut().for_each(|arr| {
arr.iter_mut()
.for_each(|c| *c = iter.next().expect("insufficient round constants"))
});

assert!(iter.next().is_none(), "round constants are too many");

Expand Down
2 changes: 1 addition & 1 deletion ceno_zkvm/src/instructions/global.rs
Original file line number Diff line number Diff line change
Expand Up @@ -298,7 +298,7 @@ pub struct GlobalChipInput<E: ExtensionField> {
}

impl<E: ExtensionField> GlobalChip<E> {
fn assign_instance<'a>(
fn assign_instance(
config: &GlobalConfig<E>,
instance: &mut [E::BaseField],
_lk_multiplicity: &mut LkMultiplicity,
Expand Down
2 changes: 1 addition & 1 deletion ceno_zkvm/src/instructions/riscv/rv32im/mmu.rs
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ impl<E: ExtensionField> MmuConfig<'_, E> {
&self.local_final_circuit,
&(shard_ctx, all_records.as_slice()),
)?;
witness.assign_global_chip_circuit(cs, &shard_ctx, &self.ram_bus_circuit)?;
witness.assign_global_chip_circuit(cs, shard_ctx, &self.ram_bus_circuit)?;

Ok(())
}
Expand Down
1 change: 1 addition & 0 deletions ceno_zkvm/src/scheme.rs
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,7 @@ pub struct PublicValues {
}

impl PublicValues {
#[allow(clippy::too_many_arguments)]
pub fn new(
exit_code: u32,
init_pc: u32,
Expand Down
1 change: 1 addition & 0 deletions ceno_zkvm/src/scheme/cpu/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ pub type TowerRelationOutput<E> = (

// accumulate N=2^n EC points into one EC point using affine coordinates
// in one layer which borrows ideas from the [Quark paper](https://eprint.iacr.org/2020/1275.pdf)
#[derive(Default)]
Comment thread
hero78119 marked this conversation as resolved.
Outdated
pub struct CpuEccProver;

impl CpuEccProver {
Expand Down
189 changes: 16 additions & 173 deletions ceno_zkvm/src/scheme/utils.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
use crate::{
scheme::{
constants::{MIN_PAR_SIZE, SEPTIC_JACOBIAN_NUM_MLES},
constants::MIN_PAR_SIZE,
hal::{MainSumcheckProver, ProofInput, ProverDevice},
septic_curve::{SepticExtension, SepticJacobianPoint},
},
structs::ComposedConstrainSystem,
};
Expand All @@ -27,7 +26,7 @@ use rayon::{
},
prelude::ParallelSliceMut,
};
use std::{array::from_fn, iter, sync::Arc};
use std::{iter, sync::Arc};
use witness::next_pow2_instance_padding;

// first computes the masked mle'[j] = mle[j] if j < num_instance, else default
Expand Down Expand Up @@ -294,10 +293,7 @@ pub fn infer_tower_product_witness<E: ExtensionField>(
.map(|index| {
// avoid the overhead of vector initialization
let mut evaluations: Vec<E> = Vec::with_capacity(output_len);
unsafe {
// will be filled immediately
evaluations.set_len(output_len);
}
let remaining = evaluations.spare_capacity_mut();

input_layer.chunks_exact(2).enumerate().for_each(|(i, f)| {
match (f[0].evaluations(), f[1].evaluations()) {
Expand All @@ -307,24 +303,28 @@ pub fn infer_tower_product_witness<E: ExtensionField>(
if i == 0 {
(start..(start + output_len))
.into_par_iter()
.zip(evaluations.par_iter_mut())
.zip(remaining.par_iter_mut())
.with_min_len(MIN_PAR_SIZE)
.for_each(|(index, evaluations)| {
*evaluations = f1[index] * f2[index]
evaluations.write(f1[index] * f2[index]);
});
} else {
(start..(start + output_len))
.into_par_iter()
.zip(evaluations.par_iter_mut())
.zip(remaining.par_iter_mut())
.with_min_len(MIN_PAR_SIZE)
.for_each(|(index, evaluations)| {
*evaluations *= f1[index] * f2[index]
evaluations.write(f1[index] * f2[index]);
});
}
}
_ => unreachable!("must be extension field"),
}
});

unsafe {
evaluations.set_len(output_len);
}
evaluations.into_mle()
})
.collect_vec();
Expand All @@ -336,94 +336,6 @@ pub fn infer_tower_product_witness<E: ExtensionField>(
wit_layers
}

/// Infer from input layer (layer n) to the output layer (layer 0)
/// Note that each layer has 3 * 7 * 2 multilinear polynomials since we use jacobian coordinates.
///
/// The relation between layer i and layer i+1 is as follows:
/// (x1', y1', z1')[b] = jacobian_add( (x1, y1, z1)[0,b], (x2, y2, z2)[1,b] )
/// (x2', y2', z2')[b] = jacobian_add( (x3, y3, z3)[0,b], (x4, y4, z4)[1,b] )
///
/// TODO handle jacobian_add & jacobian_double at the same time
pub fn infer_septic_sum_witness<E: ExtensionField>(
p_mles: Vec<MultilinearExtension<E>>,
) -> Vec<Vec<MultilinearExtension<E>>> {
assert_eq!(p_mles.len(), SEPTIC_JACOBIAN_NUM_MLES * 2);
assert!(p_mles.iter().map(|p| p.num_vars()).all_equal());

// +1 as the input layer has 2*N points where N = 2^num_vars
// and the output layer has 2 points
let num_layers = p_mles[0].num_vars() + 1;
println!("{num_layers} layers in total");

let mut layers = Vec::with_capacity(num_layers);
layers.push(p_mles);

for layer in (0..num_layers - 1).rev() {
let input_layer = layers.last().unwrap();
let p = input_layer[0..SEPTIC_JACOBIAN_NUM_MLES]
.iter()
.map(|mle| mle.get_base_field_vec())
.collect_vec();
let q = input_layer[SEPTIC_JACOBIAN_NUM_MLES..]
.iter()
.map(|mle| mle.get_base_field_vec())
.collect_vec();

let output_len = p[0].len() / 2;
let mut outputs: Vec<E::BaseField> =
Vec::with_capacity(SEPTIC_JACOBIAN_NUM_MLES * 2 * output_len);
unsafe {
// will be filled immediately
outputs.set_len(SEPTIC_JACOBIAN_NUM_MLES * 2 * output_len);
}

(0..2).for_each(|chunk| {
(0..output_len)
.into_par_iter()
.with_min_len(MIN_PAR_SIZE)
.zip_eq(outputs.par_chunks_mut(SEPTIC_JACOBIAN_NUM_MLES * 2))
.for_each(|(idx, output)| {
let row = chunk * output_len + idx;
let offset = chunk * SEPTIC_JACOBIAN_NUM_MLES;

let p1 = SepticJacobianPoint {
x: SepticExtension(from_fn(|i| p[i][row])),
y: SepticExtension(from_fn(|i| p[i + 7][row])),
z: SepticExtension(from_fn(|i| p[i + 14][row])),
};
let p2 = SepticJacobianPoint {
x: SepticExtension(from_fn(|i| q[i][row])),
y: SepticExtension(from_fn(|i| q[i + 7][row])),
z: SepticExtension(from_fn(|i| q[i + 14][row])),
};
assert!(p1.is_on_curve(), "{layer}, {row}");
assert!(p2.is_on_curve(), "{layer}, {row}");

let p3 = &p1 + &p2;

output[offset..offset + 7].clone_from_slice(&p3.x);
output[offset + 7..offset + 14].clone_from_slice(&p3.y);
output[offset + 14..offset + 21].clone_from_slice(&p3.z);
});
});

// transpose
let output_mles = (0..SEPTIC_JACOBIAN_NUM_MLES * 2)
.map(|i| {
(0..output_len)
.into_par_iter()
.map(|j| outputs[j * SEPTIC_JACOBIAN_NUM_MLES * 2 + i])
.collect::<Vec<_>>()
.into_mle()
})
.collect_vec();
layers.push(output_mles);
}

layers.reverse();
layers
}

#[tracing::instrument(
skip_all,
name = "build_main_witness",
Expand Down Expand Up @@ -641,23 +553,18 @@ pub fn gkr_witness<
#[cfg(test)]
mod tests {

use ff_ext::{BabyBearExt4, FieldInto, GoldilocksExt2};
use ff_ext::{FieldInto, GoldilocksExt2};
use itertools::Itertools;
use multilinear_extensions::{
commutative_op_mle_pair,
mle::{ArcMultilinearExtension, FieldType, IntoMLE, MultilinearExtension},
smart_slice::SmartSlice,
util::{ceil_log2, transpose},
util::ceil_log2,
};
use p3::{babybear::BabyBear, field::FieldAlgebra};
use p3::field::FieldAlgebra;

use crate::scheme::{
constants::SEPTIC_JACOBIAN_NUM_MLES,
septic_curve::{SepticExtension, SepticJacobianPoint, SepticPoint},
utils::{
infer_septic_sum_witness, infer_tower_logup_witness, infer_tower_product_witness,
interleaving_mles_to_mles,
},
use crate::scheme::utils::{
infer_tower_logup_witness, infer_tower_product_witness, interleaving_mles_to_mles,
};

#[test]
Expand Down Expand Up @@ -964,68 +871,4 @@ mod tests {
]))
);
}

#[test]
fn test_infer_septic_addition_witness() {
type F = BabyBear;
type E = BabyBearExt4;

let n_points = 1 << 6;
let mut rng = rand::thread_rng();
// sample n points
let points: Vec<SepticJacobianPoint<F>> = (0..n_points)
.map(|_| SepticJacobianPoint::<F>::random(&mut rng))
.collect_vec();

// transform points to row major matrix
let trace = points[0..n_points / 2]
.iter()
.zip(points[n_points / 2..n_points].iter())
.map(|(p, q)| {
[p, q]
.iter()
.flat_map(|p| p.x.0.iter().chain(p.y.0.iter()).chain(p.z.0.iter()))
.copied()
.collect_vec()
})
.collect_vec();

// transpose row major matrix to column major matrix
let p_mles: Vec<MultilinearExtension<E>> = transpose(trace)
.into_iter()
.map(|v| v.into_mle())
.collect_vec();

let layers = infer_septic_sum_witness(p_mles);
let output_layer = &layers[0];
assert!(output_layer.iter().all(|mle| mle.num_vars() == 0));
assert!(output_layer.len() == SEPTIC_JACOBIAN_NUM_MLES * 2);

// recover points from output layer
let output_points: Vec<SepticJacobianPoint<F>> = output_layer
.chunks_exact(SEPTIC_JACOBIAN_NUM_MLES)
.map(|mles| {
mles.iter()
.map(|mle| mle.get_base_field_vec()[0])
.collect_vec()
})
.map(|chunk| SepticJacobianPoint {
x: SepticExtension(chunk[0..7].try_into().unwrap()),
y: SepticExtension(chunk[7..14].try_into().unwrap()),
z: SepticExtension(chunk[14..21].try_into().unwrap()),
})
.collect_vec();
assert!(output_points.iter().all(|p| p.is_on_curve()));
assert_eq!(output_points.len(), 2);

let point_acc: SepticPoint<F> = output_points
.into_iter()
.sum::<SepticJacobianPoint<F>>()
.into_affine();
let expected_acc: SepticPoint<F> = points
.into_iter()
.sum::<SepticJacobianPoint<F>>()
.into_affine();
assert_eq!(point_acc, expected_acc);
}
}
3 changes: 2 additions & 1 deletion ceno_zkvm/src/scheme/verifier.rs
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMVerifier<E, PCS>
&self,
vm_proof: ZKVMProof<E, PCS>,
transcript: impl ForkableTranscript<E>,
expect_halt: bool,
_expect_halt: bool,
) -> Result<bool, ZKVMError> {
// require ecall/halt proof to exist, depending whether we expect a halt.
// let has_halt = vm_proof.has_halt(&self.vk);
Expand Down Expand Up @@ -969,6 +969,7 @@ impl TowerVerify {
}
}

#[derive(Default)]
pub struct EccVerifier;

impl EccVerifier {
Expand Down
Loading