Skip to content
Merged
Show file tree
Hide file tree
Changes from all 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
8 changes: 4 additions & 4 deletions plonk/src/nightfall/accumulation/circuit/atomic_gadgets.rs
Original file line number Diff line number Diff line change
Expand Up @@ -322,8 +322,8 @@ mod tests {
circuit
.finalize_for_recursive_mle_arithmetization::<RescueCRHF<FqBn254>>()
.unwrap();
let pi = circuit.public_input().unwrap()[0];
circuit.check_circuit_satisfiability(&[pi]).unwrap();
let pi = circuit.public_input().unwrap();
circuit.check_circuit_satisfiability(&pi).unwrap();
}

#[test]
Expand Down Expand Up @@ -450,8 +450,8 @@ mod tests {
circuit
.finalize_for_recursive_mle_arithmetization::<RescueCRHF<FrBn254>>()
.unwrap();
let pi = circuit.public_input().unwrap()[0];
circuit.check_circuit_satisfiability(&[pi]).unwrap();
let pi = circuit.public_input().unwrap();
circuit.check_circuit_satisfiability(&pi).unwrap();
let srs_size = circuit.num_gates().ilog2() as usize;
let srs = Zeromorph::<UnivariateIpaPCS<Grumpkin>>::gen_srs_for_testing(&mut rng, srs_size)
.unwrap();
Expand Down
26 changes: 18 additions & 8 deletions plonk/src/nightfall/circuit/plonk_partial_verifier/gadgets.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ use super::{
#[allow(clippy::too_many_arguments)]
pub fn compute_scalars_for_native_field<F: PrimeField + RescueParameter>(
circuit: &mut PlonkCircuit<F>,
pi: &Variable,
pi: &[Variable; 2],
challenges: &ChallengesVar,
proof_evals: &ProofEvalsVarNative,
lookup_evals: &Option<PlookupEvalsVarNative>,
Expand Down Expand Up @@ -275,7 +275,7 @@ pub fn compute_scalars_for_native_field<F: PrimeField + RescueParameter>(
#[allow(clippy::too_many_arguments)]
pub(crate) fn compute_scalars_for_native_field_base<F: PrimeField + RescueParameter>(
circuit: &mut PlonkCircuit<F>,
pi: &Variable,
pi: &[Variable; 2],
challenges: &ChallengesVar,
proof_evals: &ProofEvalsVarNative,
lookup_evals: &Option<PlookupEvalsVarNative>,
Expand Down Expand Up @@ -307,6 +307,7 @@ pub(crate) fn compute_scalars_for_native_field_base<F: PrimeField + RescueParame
let evals = poly::evaluate_poly_helper_native_base(
circuit,
challenges.zeta,
vk_var.domain.gen,
gen_inv_var,
vk_var.domain.domain_size,
max_domain_size,
Expand Down Expand Up @@ -767,26 +768,35 @@ mod test {
// 5. Verification

for (i, proof) in proofs.iter().enumerate() {
let pi = public_inputs[i][0];
let pi = public_inputs[i].clone();
let mut transcript = <RescueTranscript<F> as Transcript>::new_transcript(b"mle_plonk");
let mle_challenges = MLEChallenges::new_recursion(&proof.proof, &[pi], &mut transcript)
let mle_challenges = MLEChallenges::new_recursion(&proof.proof, &pi, &mut transcript)
.map_err(|_| {
CircuitError::ParameterError("MLE challenge generation failed".to_string())
})?;
CircuitError::ParameterError("MLE challenge generation failed".to_string())
})?;

let mut plonk_circuit = PlonkCircuit::<F>::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
let mle_proof_var = SAMLEProofVar::from_struct::<P>(&mut plonk_circuit, &proof.proof)?;

let mut transcript_var = RescueTranscriptVar::<F>::new_transcript(&mut plonk_circuit);
let pi_var = plonk_circuit.create_emulated_variable(pi)?;
let pi_vars: [EmulatedVariable<P::ScalarField>; 2] = pi
.iter()
.map(|val| plonk_circuit.create_emulated_variable(*val))
.collect::<Result<Vec<_>, CircuitError>>()?
.try_into()
.map_err(|_| {
CircuitError::ParameterError(
"Couldn't convert public inputs to fixed length array".to_string(),
)
})?;
let mle_challenges_var =
EmulatedMLEChallenges::<E::ScalarField>::compute_challenges_vars::<
PCS,
P,
RescueTranscriptVar<F>,
>(
&mut plonk_circuit,
&pi_var,
&pi_vars,
&mle_proof_var,
&mut transcript_var,
)?;
Expand Down
23 changes: 17 additions & 6 deletions plonk/src/nightfall/circuit/plonk_partial_verifier/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -936,7 +936,9 @@ mod test {
circuit
.finalize_for_recursive_arithmetization::<RescueCRHF<P::ScalarField>>()
.unwrap();
let pi = circuit.public_input().unwrap()[0];
let pi: [P::ScalarField; 2] = circuit.public_input()?.try_into().map_err(|_| {
CircuitError::ParameterError("Couldn't convert to fixed length array".to_string())
})?;
let max_degree = circuit.srs_size(blind)?;
let srs = FFTPlonk::<PCS>::universal_setup_for_testing(max_degree, rng).unwrap();

Expand All @@ -954,7 +956,7 @@ mod test {
let pcs_info = verifier
.prepare_pcs_info::<RescueTranscript<P::BaseField>>(
&vk,
&[pi],
&pi,
&proof.proof,
&None,
blind,
Expand All @@ -969,7 +971,7 @@ mod test {

let challenges = FFTVerifier::<PCS>::compute_challenges::<
RescueTranscript<P::BaseField>,
>(&vk, &[pi], &proof.proof, &None)?;
>(&vk, &pi, &proof.proof, &None)?;

let mut circuit = PlonkCircuit::<P::ScalarField>::new_turbo_plonk();
let tau = circuit.create_variable(challenges.tau)?;
Expand Down Expand Up @@ -999,11 +1001,20 @@ mod test {
&proof.proof.plookup_proof.as_ref().unwrap().poly_evals,
)?;

let pi_var = circuit.create_variable(pi)?;
let pi_vars: [Variable; 2] = pi
.iter()
.map(|val| circuit.create_variable(*val))
.collect::<Result<Vec<Variable>, CircuitError>>()?
.try_into()
.map_err(|_| {
CircuitError::ParameterError(
"Couldn't convert to fixed length array".to_string(),
)
})?;

let scalars = compute_scalars_for_native_field::<P::ScalarField>(
&mut circuit,
&pi_var,
&pi_vars,
&challenges_var,
&proof_evals,
&Some(lookup_evals),
Expand Down Expand Up @@ -1083,7 +1094,7 @@ mod test {
let vk_k = vec![Fr254::zero(); 6];
let scalars = compute_scalars_for_native_field::<Fr254>(
&mut circuit,
&0,
&[0, 0],
&challenges_var,
&proof_evals,
&Some(lookup_evals),
Expand Down
81 changes: 59 additions & 22 deletions plonk/src/nightfall/circuit/plonk_partial_verifier/poly.rs
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ where
/// This helper function generate the variables for the following data
/// - Circuit evaluation of vanishing polynomial at point `zeta` i.e., output =
/// zeta ^ domain_size - 1 mod Fr::modulus
/// - Evaluations of the first and the last lagrange polynomial at point `zeta`
/// - Evaluations of the first, second and last lagrange polynomial at point `zeta`
///
/// Note that outputs and zeta are both Fr element
/// so this needs to be carried out over a non-native circuit
Expand All @@ -138,7 +138,7 @@ pub(super) fn evaluate_poly_helper_native<F>(
zeta_var: Variable,
gen_inv: F,
domain_size: usize,
) -> Result<[Variable; 4], CircuitError>
) -> Result<[Variable; 5], CircuitError>
where
F: PrimeField + RescueParameter,
{
Expand All @@ -158,10 +158,16 @@ where

// ================================
// evaluate lagrange at 1
// lagrange_1_eval = (zeta^n - 1) / (zeta - 1) / domain_size
// lagrange_1_eval = (zeta^n - 1) / (domain_size * (zeta - 1))
//
// which is proven via
// domain_size * lagrange_1_eval * (zeta - 1) = zeta^n - 1 mod Fr::modulus
//
// similarly we calculate
// lagrange_2_eval = (zeta^n - 1) * omega / (domain_size * (zeta - omega)) = (zeta^n - 1) / (domain_size * (zeta * omega^{-1} - 1))
// and
// lagrange_n_eval = (zeta^n - 1) * omega^{-1} / (domain_size * (zeta - omega^{-1})) = (zeta^n - 1) / (domain_size * (zeta * omega - 1))
//
// ================================

let domain_size = F::from(domain_size as u64);
Expand All @@ -178,31 +184,42 @@ where
// Constrain the lagrange_1_eval to be correct.
circuit.mul_gate(divisor_var, lagrange_1_eval_var, zeta_n_minus_one_var)?;

// Compute lagrange_2_eval
let divisor_var = circuit.lin_comb(&[domain_size * gen_inv], &(-domain_size), &[zeta_var])?;
let divisor = circuit.witness(divisor_var)?;
let lagrange_2_eval = zeta_n_minus_one / divisor;
let lagrange_2_eval_var = circuit.create_variable(lagrange_2_eval)?;
// Constrain the lagrange_2_eval to be correct.
circuit.mul_gate(divisor_var, lagrange_2_eval_var, zeta_n_minus_one_var)?;

let gen = gen_inv
.inverse()
.ok_or(CircuitError::ParameterError("Inverse Failed".to_string()))?;
// Compute lagrange_n_eval
let divisor_var = circuit.lin_comb(&[domain_size], &(-domain_size * gen_inv), &[zeta_var])?;
let numerator_var = circuit.mul_constant(zeta_n_minus_one_var, &gen_inv)?;
let divisor_var = circuit.lin_comb(&[domain_size * gen], &(-domain_size), &[zeta_var])?;
let divisor = circuit.witness(divisor_var)?;
let numerator = circuit.witness(numerator_var)?;
let lagrange_n_eval = numerator / divisor;
let lagrange_n_eval = zeta_n_minus_one / divisor;
let lagrange_n_eval_var = circuit.create_variable(lagrange_n_eval)?;
// Constrain the lagrange_n_eval to be correct.
circuit.mul_gate(divisor_var, lagrange_n_eval_var, numerator_var)?;
circuit.mul_gate(divisor_var, lagrange_n_eval_var, zeta_n_minus_one_var)?;

Ok([
zeta_n_var,
zeta_n_minus_one_var,
lagrange_1_eval_var,
lagrange_2_eval_var,
lagrange_n_eval_var,
])
}

pub(super) fn evaluate_poly_helper_native_base<F>(
circuit: &mut PlonkCircuit<F>,
zeta_var: Variable,
gen_var: Variable,
gen_inv_var: Variable,
domain_size_var: Variable,
max_domain_size: usize,
) -> Result<[Variable; 4], CircuitError>
) -> Result<[Variable; 5], CircuitError>
where
F: PrimeField + RescueParameter,
{
Expand All @@ -216,10 +233,16 @@ where

// ================================
// evaluate lagrange at 1
// lagrange_1_eval = (zeta^n - 1) / (zeta - 1) / domain_size
// lagrange_1_eval = (zeta^n - 1) / (domain_size * (zeta - 1))
//
// which is proven via
// domain_size * lagrange_1_eval * (zeta - 1) = zeta^n - 1 mod Fr::modulus
//
// similarly we calculate
// lagrange_2_eval = (zeta^n - 1) * omega / (domain_size * (zeta - omega))
// and
// lagrange_n_eval = (zeta^n - 1) * omega^{-1} / (domain_size * (zeta - omega^{-1}))
//
// ================================

// lagrange_1_eval
Expand All @@ -237,6 +260,19 @@ where
// Constrain the lagrange_1_eval to be correct.
circuit.mul_gate(divisor_var, lagrange_1_eval_var, zeta_n_minus_one_var)?;

// Compute lagrange_2_eval
let divisor_var = circuit.mul_add(
&[domain_size_var, zeta_var, domain_size_var, gen_var],
&[F::one(), -F::one()],
)?;
let numerator_var = circuit.mul(zeta_n_minus_one_var, gen_var)?;
let divisor = circuit.witness(divisor_var)?;
let numerator = circuit.witness(numerator_var)?;
let lagrange_2_eval = numerator / divisor;
let lagrange_2_eval_var = circuit.create_variable(lagrange_2_eval)?;
// Constrain the lagrange_n_eval to be correct.
circuit.mul_gate(divisor_var, lagrange_2_eval_var, numerator_var)?;

// Compute lagrange_n_eval
let divisor_var = circuit.mul_add(
&[domain_size_var, zeta_var, domain_size_var, gen_inv_var],
Expand All @@ -254,6 +290,7 @@ where
zeta_n_var,
zeta_n_minus_one_var,
lagrange_1_eval_var,
lagrange_2_eval_var,
lagrange_n_eval_var,
])
}
Expand Down Expand Up @@ -431,8 +468,8 @@ pub(super) fn compute_lin_poly_constant_term_circuit_native<F>(
gen_inv: &F,
challenges: &ChallengesVar,
proof_evals: &ProofEvalsVarNative,
pi: &Variable,
evals: &[Variable; 4],
pi: &[Variable; 2],
evals: &[Variable; 5],
lookup_evals: &Option<PlookupEvalsVarNative>,
) -> Result<Variable, CircuitError>
where
Expand Down Expand Up @@ -493,7 +530,7 @@ where
prod = circuit.mul(tmp, prod)?;

// r_plonk
let pi_eval = circuit.mul(*pi, evals[2])?;
let pi_eval = circuit.mul_add(&[pi[0], evals[2], pi[1], evals[3]], &[F::one(), F::one()])?;
let wires = [pi_eval, prod, evals[2], challenges.alphas[1]];
let non_lookup = circuit.gen_quad_poly(
&wires,
Expand All @@ -512,7 +549,7 @@ where
];
let tmp = circuit.lc(&wires, &[F::one(), -F::one(), -F::one(), F::zero()])?;
let term_one = circuit.mul_add(
&[evals[3], tmp, evals[2], challenges.alphas[0]],
&[evals[4], tmp, evals[2], challenges.alphas[0]],
&[F::one(), -F::one()],
)?;

Expand Down Expand Up @@ -581,8 +618,8 @@ pub(super) fn compute_lin_poly_constant_term_circuit_native_base<F>(
gen_inv_var: &Variable,
challenges: &ChallengesVar,
proof_evals: &ProofEvalsVarNative,
pi: &Variable,
evals: &[Variable; 4],
pi: &[Variable; 2],
evals: &[Variable; 5],
lookup_evals: &Option<PlookupEvalsVarNative>,
) -> Result<Variable, CircuitError>
where
Expand Down Expand Up @@ -643,7 +680,7 @@ where
prod = circuit.mul(tmp, prod)?;

// r_plonk
let pi_eval = circuit.mul(*pi, evals[2])?;
let pi_eval = circuit.mul_add(&[pi[0], evals[2], pi[1], evals[3]], &[F::one(), F::one()])?;
let wires = [pi_eval, prod, evals[2], challenges.alphas[1]];
let non_lookup = circuit.gen_quad_poly(
&wires,
Expand All @@ -662,7 +699,7 @@ where
];
let tmp = circuit.lc(&wires, &[F::one(), -F::one(), -F::one(), F::zero()])?;
let term_one = circuit.mul_add(
&[evals[3], tmp, evals[2], challenges.alphas[0]],
&[evals[4], tmp, evals[2], challenges.alphas[0]],
&[F::one(), -F::one()],
)?;

Expand Down Expand Up @@ -760,7 +797,7 @@ pub fn linearization_scalars_circuit_native<F>(
circuit: &mut PlonkCircuit<F>,
vk_k: &[F],
challenges: &ChallengesVar,
evals: &[Variable; 4],
evals: &[Variable; 5],
poly_evals: &ProofEvalsVarNative,
lookup_evals: &Option<PlookupEvalsVarNative>,
gen_inv: &F,
Expand Down Expand Up @@ -1004,7 +1041,7 @@ where
challenges.alphas[0],
evals[2],
challenges.alphas[1],
evals[3],
evals[4],
],
&[F::one(), F::one()],
)?;
Expand Down Expand Up @@ -1081,7 +1118,7 @@ pub fn linearization_scalars_circuit_native_base<F>(
circuit: &mut PlonkCircuit<F>,
vk_k: &[Variable],
challenges: &ChallengesVar,
evals: &[Variable; 4],
evals: &[Variable; 5],
poly_evals: &ProofEvalsVarNative,
lookup_evals: &Option<PlookupEvalsVarNative>,
gen_inv_var: &Variable,
Expand Down Expand Up @@ -1318,7 +1355,7 @@ where
challenges.alphas[0],
evals[2],
challenges.alphas[1],
evals[3],
evals[4],
],
&[F::one(), F::one()],
)?;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -278,7 +278,7 @@ pub struct Bn254OutputScalarsAndBasesVar {
/// The proof generated by the recursive prover.
pub proof: Bn254ProofScalarsandBasesVar,
/// The hash of the public inputs to this proof stored in the clear.
pub pi_hash: Fr254,
pub pi_hash: [Fr254; 2],
/// The transcript of the proof stored in the clear.
pub transcript: RescueTranscript<Fr254>,
}
Expand Down
Loading
Loading