diff --git a/plonk/CHANGELOG.md b/plonk/CHANGELOG.md index 2d8cf25d5..86cfd675f 100644 --- a/plonk/CHANGELOG.md +++ b/plonk/CHANGELOG.md @@ -3,6 +3,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## Untracked + +### Changes + +- [#894](https://github.com/EspressoSystems/jellyfish/pull/893): Circuit bug: range-check the limb decomposition of the Fiat-Shamir challenges in the recursive PlonK verifier. The limbs of `alpha`, `beta`, `gamma`, `zeta`, `u` and `v` were bound to the squeezed challenge by a single linear constraint, so non-canonical decompositions were admissible and made the emulated multiplications compute wrong residues. This changes the recursive verifier circuit, and therefore its verifying key. + ## 0.8.0 ### Breaking Changes diff --git a/plonk/src/circuit/plonk_verifier/structs.rs b/plonk/src/circuit/plonk_verifier/structs.rs index 19eea3db4..34967dd6f 100644 --- a/plonk/src/circuit/plonk_verifier/structs.rs +++ b/plonk/src/circuit/plonk_verifier/structs.rs @@ -36,17 +36,44 @@ pub(crate) struct ChallengesFpElemVar { pub(crate) u: FpElemVar, } -pub(crate) fn challenge_var_to_fp_elem_var( +/// Split a challenge variable into limbs, enforcing that each limb is in +/// `[0, 2^m)`. +/// +/// `FpElemVar::new_unchecked` only binds the limbs to the challenge with the +/// single linear constraint `limb_0 + 2^m * limb_1 = challenge`, which a prover +/// can also satisfy with non-canonical limbs. Since the challenges are consumed +/// by `mod_mul`, which reads the limbs back as integers, non-canonical limbs +/// make the emulated arithmetic wrap the native modulus and produce a wrong +/// residue modulo the emulated one. The transcript range-checks only the +/// squeezed challenge, never its decomposition, so the range checks have to +/// happen here. +/// +/// Once `jf-relation` is released with `FpElemVar::new_checked`, this helper +/// can be replaced by a call to it. +fn challenge_var_to_range_checked_limbs( circuit: &mut PlonkCircuit, - challenge_var: &ChallengesVar, + challenge_var: Variable, non_native_field_info: &NonNativeFieldInfo, -) -> Result, CircuitError> { - let alpha_fp_elem_var = FpElemVar::new_unchecked( +) -> Result, CircuitError> { + let elem = FpElemVar::new_unchecked( circuit, - challenge_var.alpha, + challenge_var, non_native_field_info.m, non_native_field_info.two_power_m, )?; + let (limb_0, limb_1) = elem.components(); + circuit.enforce_in_range(limb_0, non_native_field_info.m)?; + circuit.enforce_in_range(limb_1, non_native_field_info.m)?; + Ok(elem) +} + +pub(crate) fn challenge_var_to_fp_elem_var( + circuit: &mut PlonkCircuit, + challenge_var: &ChallengesVar, + non_native_field_info: &NonNativeFieldInfo, +) -> Result, CircuitError> { + let alpha_fp_elem_var = + challenge_var_to_range_checked_limbs(circuit, challenge_var.alpha, non_native_field_info)?; let alpha_2_fp_elem_var = circuit.mod_mul( &alpha_fp_elem_var, &alpha_fp_elem_var, @@ -60,36 +87,23 @@ pub(crate) fn challenge_var_to_fp_elem_var( Ok(ChallengesFpElemVar { alphas: [alpha_fp_elem_var, alpha_2_fp_elem_var, alpha_3_fp_elem_var], - beta: FpElemVar::new_unchecked( + beta: challenge_var_to_range_checked_limbs( circuit, challenge_var.beta, - non_native_field_info.m, - non_native_field_info.two_power_m, + non_native_field_info, )?, - gamma: FpElemVar::new_unchecked( + gamma: challenge_var_to_range_checked_limbs( circuit, challenge_var.gamma, - non_native_field_info.m, - non_native_field_info.two_power_m, + non_native_field_info, )?, - zeta: FpElemVar::new_unchecked( + zeta: challenge_var_to_range_checked_limbs( circuit, challenge_var.zeta, - non_native_field_info.m, - non_native_field_info.two_power_m, - )?, - u: FpElemVar::new_unchecked( - circuit, - challenge_var.u, - non_native_field_info.m, - non_native_field_info.two_power_m, - )?, - v: FpElemVar::new_unchecked( - circuit, - challenge_var.v, - non_native_field_info.m, - non_native_field_info.two_power_m, + non_native_field_info, )?, + u: challenge_var_to_range_checked_limbs(circuit, challenge_var.u, non_native_field_info)?, + v: challenge_var_to_range_checked_limbs(circuit, challenge_var.v, non_native_field_info)?, }) } @@ -188,3 +202,61 @@ pub(crate) struct NonNativeFieldInfo { pub(crate) modulus_in_f: F, pub(crate) modulus_fp_elem: FpElem, } + +#[cfg(test)] +mod test { + use super::*; + use ark_bls12_377::{Fq as Fq377, Fr as Fr377}; + use ark_ff::{BigInteger, Field}; + use ark_std::One; + use jf_relation::Circuit; + + const RANGE_BIT_LEN_FOR_TEST: usize = 16; + + // Regression test: the limb decomposition of every Fiat-Shamir challenge + // must be range-checked. + // + // `FpElemVar::new_unchecked` binds the limbs to the challenge with a single + // linear constraint, `vars.0 + 2^m * vars.1 = challenge`, which a prover can + // satisfy with non-canonical limbs by shifting one down by `2^m` and the + // other up by 1. The challenges are then consumed by `mod_mul`, which reads + // the limbs as integers -- so an aliased challenge wraps the native modulus + // and multiplies by a wrong residue modulo the emulated one, breaking the + // soundness of the in-circuit verifier. The transcript range-checks only the + // squeezed challenge (< 2^248), never its decomposition. + #[test] + fn test_challenge_limbs_are_range_checked() -> Result<(), CircuitError> { + let m = 128; + let two_power_m = Fq377::from(2u8).pow([m as u64]); + let modulus_in_f = + Fq377::from_le_bytes_mod_order(&::MODULUS.to_bytes_le()); + let non_native_field_info = NonNativeFieldInfo:: { + m, + two_power_m: Some(two_power_m), + modulus_in_f, + modulus_fp_elem: FpElem::new(&modulus_in_f, m, Some(two_power_m))?, + }; + + let mut circuit = PlonkCircuit::::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST); + let challenge_var = ChallengesVar { + alpha: circuit.create_variable(Fq377::from(7u8))?, + beta: circuit.create_variable(Fq377::from(11u8))?, + gamma: circuit.create_variable(Fq377::from(13u8))?, + zeta: circuit.create_variable(Fq377::from(17u8))?, + v: circuit.create_variable(Fq377::from(19u8))?, + u: circuit.create_variable(Fq377::from(23u8))?, + }; + let challenges_fp_elem_var = + challenge_var_to_fp_elem_var(&mut circuit, &challenge_var, &non_native_field_info)?; + assert!(circuit.check_circuit_satisfiability(&[]).is_ok()); + + // `beta` is not consumed inside `challenge_var_to_fp_elem_var`, so the + // limb range checks are the only thing that can reject the alias. + let (beta_0, beta_1) = challenges_fp_elem_var.beta.components(); + *circuit.witness_mut(beta_0) -= two_power_m; + *circuit.witness_mut(beta_1) += Fq377::one(); + assert!(circuit.check_circuit_satisfiability(&[]).is_err()); + + Ok(()) + } +} diff --git a/relation/CHANGELOG.md b/relation/CHANGELOG.md index caceb5caa..6f99368ff 100644 --- a/relation/CHANGELOG.md +++ b/relation/CHANGELOG.md @@ -8,6 +8,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Changes - [#843](https://github.com/EspressoSystems/jellyfish/pull/843): replace unmaintained `derivative` with `derive_where`. +- [#894](https://github.com/EspressoSystems/jellyfish/pull/893): Circuit bug: range-check the limb decomposition of `FpElemVar`. Adds `FpElemVar::new_checked` and uses it for the outputs of `mod_add`, `mod_add_constant`, `mod_add_vec` and `mod_negate`, whose limbs were previously underconstrained. ## 0.5.0 diff --git a/relation/src/gadgets/ultraplonk/mod_arith.rs b/relation/src/gadgets/ultraplonk/mod_arith.rs index 166d3f253..dd6c59a54 100644 --- a/relation/src/gadgets/ultraplonk/mod_arith.rs +++ b/relation/src/gadgets/ultraplonk/mod_arith.rs @@ -97,9 +97,22 @@ pub struct FpElemVar { impl FpElemVar { /// Create an FpElemVar from Fp element variable `var` and split parameter /// `m`. Does not perform range checks on the resulting variables. - /// To create an `FpElemVar` from a field element, consider to - /// use `new_from_field_element` instead (which comes with - /// a range proof for the field element). + /// + /// # Warning + /// The only constraint added is `vars.0 + 2^m * vars.1 = var`, which every + /// limb pair whose weighted sum matches `var` over the native field + /// satisfies -- not just the canonical decomposition. + /// Every operation that reads the limbs back as *integers* -- + /// [`PlonkCircuit::mod_mul`], [`PlonkCircuit::mod_mul_constant`] and the + /// modular addition gates -- is sound only while both limbs are known to be + /// in `[0, 2^m)`; a non-canonical assignment makes those gates wrap the + /// native modulus and yield a wrong residue modulo the emulated one. + /// + /// Only use this constructor when the limbs are already range-checked by + /// construction (e.g. the outputs of [`PlonkCircuit::mod_mul`]) or when the + /// value never enters modular arithmetic. Otherwise use + /// [`Self::new_checked`], or [`Self::new_from_field_element`] when starting + /// from a field element rather than an existing variable. pub fn new_unchecked( cs: &mut PlonkCircuit, var: Variable, @@ -121,6 +134,26 @@ impl FpElemVar { }) } + /// Create an FpElemVar from Fp element variable `var` and split parameter + /// `m`, enforcing both that the limbs recompose to `var` and that each limb + /// is in `[0, 2^m)`. + /// + /// This is the sound counterpart of [`Self::new_unchecked`]: the range + /// checks pin down the canonical decomposition, which is what the modular + /// arithmetic gates assume of their operands. + /// Requires a lookup table. + pub fn new_checked( + cs: &mut PlonkCircuit, + var: Variable, + m: usize, + two_power_m: Option, + ) -> Result { + let elem = Self::new_unchecked(cs, var, m, two_power_m)?; + cs.range_gate_with_lookup(elem.vars.0, m)?; + cs.range_gate_with_lookup(elem.vars.1, m)?; + Ok(elem) + } + /// Convert into a single variable with value `witness[vars.0] + 2^m * /// witness[vars.1]` pub fn convert_to_var(&self, cs: &mut PlonkCircuit) -> Result { @@ -342,7 +375,7 @@ impl PlonkCircuit { let num_range_blocks = self.num_range_blocks()?; let res = self.mod_add_internal(&[x_var, y_var], p.field_elem(), num_range_blocks)?; - FpElemVar::new_unchecked(self, res, x.m, Some(p.two_power_m)) + FpElemVar::new_checked(self, res, x.m, Some(p.two_power_m)) } /// Modular addition gate: @@ -432,7 +465,7 @@ impl PlonkCircuit { self.quad_poly_gate(&wires, &q_lc, &q_mul, q_o, q_c)?; - FpElemVar::new_unchecked(self, remainder_var, x.m, Some(p.two_power_m)) + FpElemVar::new_checked(self, remainder_var, x.m, Some(p.two_power_m)) } /// Modular addition gate: @@ -474,7 +507,7 @@ impl PlonkCircuit { let num_range_blocks = self.num_range_blocks()?; let res = self.mod_add_internal(x_vars.as_ref(), p.field_elem(), num_range_blocks)?; - FpElemVar::new_unchecked(self, res, p.m, Some(p.two_power_m)) + FpElemVar::new_checked(self, res, p.m, Some(p.two_power_m)) } /// Modular multiplication gate: @@ -864,7 +897,7 @@ impl PlonkCircuit { self.lc_gate(&wires, &coeffs)?; - FpElemVar::new_unchecked(self, x_neg_var, x.m, Some(x.two_power_m)) + FpElemVar::new_checked(self, x_neg_var, x.m, Some(x.two_power_m)) } } @@ -978,6 +1011,100 @@ mod test { Ok(circuit) } + // Regression test for the limb decomposition of an `FpElemVar`. + // + // `new_unchecked` only enforces `vars.0 + 2^m * vars.1 = var` over the + // native field, which admits a whole family of limb assignments besides the + // canonical one: shifting one limb down by `2^m` and the other up by 1 + // leaves the constraint satisfied. The aliased limbs then stand for a + // different *integer*, and the modular arithmetic gates -- which read the + // limbs as integers -- wrap the native modulus and compute a wrong residue + // modulo the emulated one. `new_checked` range-checks both limbs, which + // pins down the canonical decomposition and rejects the alias. + #[test] + fn test_fp_elem_var_limb_aliasing() -> Result<(), CircuitError> { + test_fp_elem_var_limb_aliasing_helper::()?; + test_fp_elem_var_limb_aliasing_helper::()?; + test_fp_elem_var_limb_aliasing_helper::()?; + test_fp_elem_var_limb_aliasing_helper::() + } + fn test_fp_elem_var_limb_aliasing_helper() -> Result<(), CircuitError> { + let m = RANGE_BIT_LEN_FOR_TEST * 4; + let two_power_m = F::from(2u8).pow([m as u64]); + // canonical limbs are (5, 3), both well inside [0, 2^m) + let val = F::from(3u8) * two_power_m + F::from(5u8); + + // `new_unchecked` leaves the decomposition underconstrained: the aliased + // witness satisfies the circuit just as well as the canonical one. + let (mut circuit, elem) = build_limb_aliasing_circuit::(val, m, false)?; + assert!(circuit.check_circuit_satisfiability(&[]).is_ok()); + alias_limbs(&mut circuit, &elem); + assert!(circuit.check_circuit_satisfiability(&[]).is_ok()); + + // `new_checked` accepts the canonical witness and rejects the alias. + let (mut circuit, elem) = build_limb_aliasing_circuit::(val, m, true)?; + assert!(circuit.check_circuit_satisfiability(&[]).is_ok()); + alias_limbs(&mut circuit, &elem); + assert!(circuit.check_circuit_satisfiability(&[]).is_err()); + + Ok(()) + } + fn build_limb_aliasing_circuit( + val: F, + m: usize, + checked: bool, + ) -> Result<(PlonkCircuit, FpElemVar), CircuitError> { + let mut circuit: PlonkCircuit = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST); + let var = circuit.create_variable(val)?; + let elem = if checked { + FpElemVar::new_checked(&mut circuit, var, m, None)? + } else { + FpElemVar::new_unchecked(&mut circuit, var, m, None)? + }; + Ok((circuit, elem)) + } + // Move the limbs off their canonical values while preserving + // `vars.0 + 2^m * vars.1`, as a malicious prover would. + fn alias_limbs(circuit: &mut PlonkCircuit, elem: &FpElemVar) { + let (var0, var1) = elem.components(); + let two_power_m = elem.two_power_m(); + *circuit.witness_mut(var0) -= two_power_m; + *circuit.witness_mut(var1) += F::one(); + } + + // The outputs of the modular addition gates are re-split into limbs too, so + // they need the same treatment: an aliased sum feeding a `mod_mul` is the + // same soundness break one step removed from the inputs. + #[test] + fn test_mod_add_output_limbs_are_range_checked() -> Result<(), CircuitError> { + test_mod_add_output_limbs_helper::()?; + test_mod_add_output_limbs_helper::()?; + test_mod_add_output_limbs_helper::()?; + test_mod_add_output_limbs_helper::() + } + fn test_mod_add_output_limbs_helper() -> Result<(), CircuitError> { + let m = RANGE_BIT_LEN_FOR_TEST * 4; + let p = F::from(RANGE_SIZE_FOR_TEST as u32).pow([10u64]); + let p_split = FpElem::new(&p, m, None)?; + + let mut circuit: PlonkCircuit = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST); + let x_var = circuit.create_variable(F::from(7u8))?; + let y_var = circuit.create_variable(F::from(11u8))?; + let x = FpElemVar::new_checked(&mut circuit, x_var, m, Some(p_split.two_power_m()))?; + let y = FpElemVar::new_checked(&mut circuit, y_var, m, Some(p_split.two_power_m()))?; + // No consumer of `sum` on purpose: the only constraints that can reject + // an aliased limb assignment here are the range checks on the limbs of + // the sum itself. Without them the aliased witness satisfies the + // circuit, and the wrong residue is invisible to every later gate. + let sum = circuit.mod_add(&x, &y, &p_split)?; + assert!(circuit.check_circuit_satisfiability(&[]).is_ok()); + + alias_limbs(&mut circuit, &sum); + assert!(circuit.check_circuit_satisfiability(&[]).is_err()); + + Ok(()) + } + // ======================================== // mod add internal // ========================================