Skip to content

Commit

Permalink
Prevent addition overflow
Browse files Browse the repository at this point in the history
  • Loading branch information
vicsn committed May 24, 2023
1 parent 0c8a7f6 commit 47de13c
Show file tree
Hide file tree
Showing 17 changed files with 91 additions and 75 deletions.
17 changes: 8 additions & 9 deletions algorithms/src/snark/marlin/ahp/indexer/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -160,15 +160,14 @@ impl<F: PrimeField, MM: MarlinMode> CanonicalSerialize for Circuit<F, MM> {

#[allow(unused_mut, unused_variables)]
fn serialized_size(&self, mode: Compress) -> usize {
let mut size = 0;
size += self.index_info.serialized_size(mode);
size += self.a.serialized_size(mode);
size += self.b.serialized_size(mode);
size += self.c.serialized_size(mode);
size += self.a_arith.serialized_size(mode);
size += self.b_arith.serialized_size(mode);
size += self.c_arith.serialized_size(mode);
size
0usize
.saturating_add(self.index_info.serialized_size(mode))
.saturating_add(self.a.serialized_size(mode))
.saturating_add(self.b.serialized_size(mode))
.saturating_add(self.c.serialized_size(mode))
.saturating_add(self.a_arith.serialized_size(mode))
.saturating_add(self.b_arith.serialized_size(mode))
.saturating_add(self.c_arith.serialized_size(mode))
}
}

Expand Down
26 changes: 13 additions & 13 deletions algorithms/src/snark/marlin/ahp/indexer/constraint_system.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
// along with the snarkVM library. If not, see <https://www.gnu.org/licenses/>.

use crate::snark::marlin::ahp::matrices::{make_matrices_square, padded_matrix_dim, to_matrix_helper};
use anyhow::anyhow;
use snarkvm_fields::Field;
use snarkvm_r1cs::{errors::SynthesisError, ConstraintSystem as CS, Index as VarIndex, LinearCombination, Variable};
use snarkvm_utilities::serialize::*;
Expand Down Expand Up @@ -58,16 +59,14 @@ impl<F: Field> ConstraintSystem<F> {
}

#[inline]
pub(crate) fn make_matrices_square(&mut self) {
let num_variables = self.num_public_variables + self.num_private_variables;
pub(crate) fn make_matrices_square(&mut self) -> Result<(), SynthesisError> {
let num_variables =
self.num_public_variables.checked_add(self.num_private_variables).ok_or_else(|| anyhow!("overflow"))?;
let matrix_dim = padded_matrix_dim(num_variables, self.num_constraints);
make_matrices_square(self, num_variables);
assert_eq!(self.num_public_variables + self.num_private_variables, self.num_constraints, "padding failed!");
assert_eq!(
self.num_public_variables + self.num_private_variables,
matrix_dim,
"padding does not result in expected matrix size!"
);
make_matrices_square(self, num_variables)?;
assert_eq!(num_variables, self.num_constraints, "padding failed!");
assert_eq!(num_variables, matrix_dim, "padding does not result in expected matrix size!");
Ok(())
}

#[inline]
Expand All @@ -90,7 +89,7 @@ impl<F: Field> CS<F> for ConstraintSystem<F> {
// function for obtaining one.

let index = self.num_private_variables;
self.num_private_variables += 1;
self.num_private_variables = self.num_private_variables.checked_add(1).ok_or_else(|| anyhow!("overflow"))?;

Ok(Variable::new_unchecked(VarIndex::Private(index)))
}
Expand All @@ -106,12 +105,12 @@ impl<F: Field> CS<F> for ConstraintSystem<F> {
// function for obtaining one.

let index = self.num_public_variables;
self.num_public_variables += 1;
self.num_public_variables = self.num_public_variables.checked_add(1).ok_or_else(|| anyhow!("overflow"))?;

Ok(Variable::new_unchecked(VarIndex::Public(index)))
}

fn enforce<A, AR, LA, LB, LC>(&mut self, _: A, a: LA, b: LB, c: LC)
fn enforce<A, AR, LA, LB, LC>(&mut self, _: A, a: LA, b: LB, c: LC) -> Result<(), SynthesisError>
where
A: FnOnce() -> AR,
AR: AsRef<str>,
Expand All @@ -123,7 +122,8 @@ impl<F: Field> CS<F> for ConstraintSystem<F> {
self.b.push(Self::make_row(&b(LinearCombination::zero())));
self.c.push(Self::make_row(&c(LinearCombination::zero())));

self.num_constraints += 1;
self.num_constraints = self.num_constraints.checked_add(1).ok_or_else(|| anyhow!("overflow"))?;
Ok(())
}

fn push_namespace<NR, N>(&mut self, _: N)
Expand Down
2 changes: 1 addition & 1 deletion algorithms/src/snark/marlin/ahp/indexer/indexer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ impl<F: PrimeField, MM: MarlinMode> AHPForR1CS<F, MM> {

let padding_time = start_timer!(|| "Padding matrices to make them square");
crate::snark::marlin::ahp::matrices::pad_input_for_indexer_and_prover(&mut ics);
ics.make_matrices_square();
ics.make_matrices_square()?;

let a = ics.a_matrix();
let b = ics.b_matrix();
Expand Down
12 changes: 8 additions & 4 deletions algorithms/src/snark/marlin/ahp/matrices.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ use crate::{
};
use itertools::Itertools;
use snarkvm_fields::{batch_inversion, Field, PrimeField};
use snarkvm_r1cs::{ConstraintSystem, Index as VarIndex};
use snarkvm_r1cs::{ConstraintSystem, Index as VarIndex, SynthesisError};
use snarkvm_utilities::{cfg_iter, cfg_iter_mut, serialize::*};

use hashbrown::HashMap;
Expand Down Expand Up @@ -75,22 +75,26 @@ pub(crate) fn pad_input_for_indexer_and_prover<F: PrimeField, CS: ConstraintSyst
}
}

pub(crate) fn make_matrices_square<F: Field, CS: ConstraintSystem<F>>(cs: &mut CS, num_formatted_variables: usize) {
pub(crate) fn make_matrices_square<F: Field, CS: ConstraintSystem<F>>(
cs: &mut CS,
num_formatted_variables: usize,
) -> Result<(), SynthesisError> {
let num_constraints = cs.num_constraints();
let matrix_padding = ((num_formatted_variables as isize) - (num_constraints as isize)).abs();

if num_formatted_variables > num_constraints {
use core::convert::identity as iden;
// Add dummy constraints of the form 0 * 0 == 0
for i in 0..matrix_padding {
cs.enforce(|| format!("pad_constraint_{i}"), iden, iden, iden);
cs.enforce(|| format!("pad_constraint_{i}"), iden, iden, iden)?;
}
} else {
// Add dummy unconstrained variables
for i in 0..matrix_padding {
let _ = cs.alloc(|| format!("pad_variable_{i}"), || Ok(F::one())).expect("alloc failed");
let _ = cs.alloc(|| format!("pad_variable_{i}"), || Ok(F::one()))?;
}
}
Ok(())
}

#[derive(Clone, Debug, CanonicalSerialize, CanonicalDeserialize, PartialEq, Eq)]
Expand Down
20 changes: 12 additions & 8 deletions algorithms/src/snark/marlin/ahp/prover/constraint_system.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
// along with the snarkVM library. If not, see <https://www.gnu.org/licenses/>.

use crate::snark::marlin::ahp::matrices::make_matrices_square;
use anyhow::anyhow;
use snarkvm_fields::Field;
use snarkvm_r1cs::{errors::SynthesisError, ConstraintSystem as CS, Index as VarIndex, LinearCombination, Variable};

Expand Down Expand Up @@ -51,10 +52,12 @@ impl<F: Field> ConstraintSystem<F> {
input[1..].to_vec()
}

pub(crate) fn make_matrices_square(&mut self) {
let num_variables = self.num_public_variables + self.num_private_variables;
make_matrices_square(self, num_variables);
assert_eq!(self.num_public_variables + self.num_private_variables, self.num_constraints, "padding failed!");
pub(crate) fn make_matrices_square(&mut self) -> Result<(), SynthesisError> {
let num_variables =
self.num_public_variables.checked_add(self.num_private_variables).ok_or_else(|| anyhow!("overflow"))?;
make_matrices_square(self, num_variables)?;
assert_eq!(num_variables, self.num_constraints, "padding failed!");
Ok(())
}
}

Expand All @@ -69,7 +72,7 @@ impl<F: Field> CS<F> for ConstraintSystem<F> {
AR: AsRef<str>,
{
let index = self.num_private_variables;
self.num_private_variables += 1;
self.num_private_variables = self.num_private_variables.checked_add(1).ok_or_else(|| anyhow!("overflow"))?;

self.private_variables.push(f()?);
Ok(Variable::new_unchecked(VarIndex::Private(index)))
Expand All @@ -83,22 +86,23 @@ impl<F: Field> CS<F> for ConstraintSystem<F> {
AR: AsRef<str>,
{
let index = self.num_public_variables;
self.num_public_variables += 1;
self.num_public_variables = self.num_public_variables.checked_add(1).ok_or_else(|| anyhow!("overflow"))?;

self.public_variables.push(f()?);
Ok(Variable::new_unchecked(VarIndex::Public(index)))
}

#[inline]
fn enforce<A, AR, LA, LB, LC>(&mut self, _: A, _: LA, _: LB, _: LC)
fn enforce<A, AR, LA, LB, LC>(&mut self, _: A, _: LA, _: LB, _: LC) -> Result<(), SynthesisError>
where
A: FnOnce() -> AR,
AR: AsRef<str>,
LA: FnOnce(LinearCombination<F>) -> LinearCombination<F>,
LB: FnOnce(LinearCombination<F>) -> LinearCombination<F>,
LC: FnOnce(LinearCombination<F>) -> LinearCombination<F>,
{
self.num_constraints += 1;
self.num_constraints = self.num_constraints.checked_add(1).ok_or_else(|| anyhow!("overflow"))?;
Ok(())
}

fn push_namespace<NR, N>(&mut self, _: N)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ impl<F: PrimeField, MM: MarlinMode> AHPForR1CS<F, MM> {
circuit.id
));
crate::snark::marlin::ahp::matrices::pad_input_for_indexer_and_prover(&mut pcs);
pcs.make_matrices_square();
pcs.make_matrices_square()?;
end_timer!(padding_time);

let prover::ConstraintSystem {
Expand Down
5 changes: 3 additions & 2 deletions algorithms/src/snark/marlin/ahp/prover/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ impl<'a, F: PrimeField, MM: MarlinMode> State<'a, F, MM> {
) -> Result<Self, AHPError> {
let mut max_constraint_domain: Option<EvaluationDomain<F>> = None;
let mut max_non_zero_domain: Option<EvaluationDomain<F>> = None;
let mut total_instances = 0;
let mut total_instances: u32 = 0;
let circuit_specific_states = indices_and_assignments
.into_iter()
.map(|(circuit, variable_assignments)| {
Expand All @@ -115,7 +115,8 @@ impl<'a, F: PrimeField, MM: MarlinMode> State<'a, F, MM> {
let first_padded_public_inputs = &variable_assignments[0].0;
let input_domain = EvaluationDomain::new(first_padded_public_inputs.len()).unwrap();
let batch_size = variable_assignments.len().try_into()?;
total_instances += batch_size;
total_instances =
total_instances.checked_add(batch_size).ok_or_else(|| anyhow::anyhow!("Batch size too large"))?;
let batch_size_usize = batch_size as usize;
let mut z_as = Vec::with_capacity(batch_size_usize);
let mut z_bs = Vec::with_capacity(batch_size_usize);
Expand Down
40 changes: 19 additions & 21 deletions algorithms/src/snark/marlin/data_structures/proof.rs
Original file line number Diff line number Diff line change
Expand Up @@ -72,16 +72,15 @@ impl<E: PairingEngine> Commitments<E> {
}

fn serialized_size(&self, compress: Compress) -> usize {
let mut size = 0;
size += serialized_vec_size_without_len(&self.witness_commitments, compress);
size += CanonicalSerialize::serialized_size(&self.mask_poly, compress);
size += CanonicalSerialize::serialized_size(&self.g_1, compress);
size += CanonicalSerialize::serialized_size(&self.h_1, compress);
size += serialized_vec_size_without_len(&self.g_a_commitments, compress);
size += serialized_vec_size_without_len(&self.g_b_commitments, compress);
size += serialized_vec_size_without_len(&self.g_c_commitments, compress);
size += CanonicalSerialize::serialized_size(&self.h_2, compress);
size
0usize
.saturating_add(serialized_vec_size_without_len(&self.witness_commitments, compress))
.saturating_add(CanonicalSerialize::serialized_size(&self.mask_poly, compress))
.saturating_add(CanonicalSerialize::serialized_size(&self.g_1, compress))
.saturating_add(CanonicalSerialize::serialized_size(&self.h_1, compress))
.saturating_add(serialized_vec_size_without_len(&self.g_a_commitments, compress))
.saturating_add(serialized_vec_size_without_len(&self.g_b_commitments, compress))
.saturating_add(serialized_vec_size_without_len(&self.g_c_commitments, compress))
.saturating_add(CanonicalSerialize::serialized_size(&self.h_2, compress))
}

fn deserialize_with_mode<R: snarkvm_utilities::Read>(
Expand Down Expand Up @@ -148,15 +147,14 @@ impl<F: PrimeField> Evaluations<F> {
}

fn serialized_size(&self, compress: Compress) -> usize {
let mut size = 0;
let mut size = 0usize;
for z_b_eval_circuit in &self.z_b_evals {
size += serialized_vec_size_without_len(z_b_eval_circuit, compress);
size = size.saturating_add(serialized_vec_size_without_len(z_b_eval_circuit, compress));
}
size += CanonicalSerialize::serialized_size(&self.g_1_eval, compress);
size += serialized_vec_size_without_len(&self.g_a_evals, compress);
size += serialized_vec_size_without_len(&self.g_b_evals, compress);
size += serialized_vec_size_without_len(&self.g_c_evals, compress);
size
size.saturating_add(CanonicalSerialize::serialized_size(&self.g_1_eval, compress))
.saturating_add(serialized_vec_size_without_len(&self.g_a_evals, compress))
.saturating_add(serialized_vec_size_without_len(&self.g_b_evals, compress))
.saturating_add(serialized_vec_size_without_len(&self.g_c_evals, compress))
}

fn deserialize_with_mode<R: snarkvm_utilities::Read>(
Expand Down Expand Up @@ -283,10 +281,10 @@ impl<E: PairingEngine> Proof<E> {
msg: ahp::prover::ThirdMessage<E::Fr>,
pc_proof: sonic_pc::BatchLCProof<E>,
) -> Result<Self, SNARKError> {
let mut total_instances = 0;
let mut total_instances = 0usize;
let mut batch_sizes = Vec::with_capacity(batch_sizes_in.len());
for (z_b_evals, batch_size) in evaluations.z_b_evals.iter().zip(batch_sizes_in.values()) {
total_instances += batch_size;
total_instances = total_instances.saturating_add(*batch_size);
batch_sizes.push(u32::try_from(*batch_size)?);
if z_b_evals.len() != *batch_size {
return Err(SNARKError::BatchSizeMismatch);
Expand All @@ -299,9 +297,9 @@ impl<E: PairingEngine> Proof<E> {
}

pub fn batch_sizes(&self) -> Result<&[u32], SNARKError> {
let mut total_instances = 0;
let mut total_instances = 0u32;
for (z_b_evals_i, &batch_size) in self.evaluations.z_b_evals.iter().zip(self.batch_sizes.iter()) {
total_instances += batch_size;
total_instances = total_instances.saturating_add(batch_size);
if u32::try_from(z_b_evals_i.len())? != batch_size {
return Err(SNARKError::BatchSizeMismatch);
}
Expand Down
9 changes: 7 additions & 2 deletions algorithms/src/snark/marlin/data_structures/test_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,11 +67,16 @@ impl<ConstraintF: Field> ConstraintSynthesizer<ConstraintF> for TestCircuit<Cons

let mul_constraints = self.mul_depth - 1;
for i in 0..(self.num_constraints - mul_constraints) {
cs.enforce(|| format!("constraint {i}"), |lc| lc + a, |lc| lc + b, |lc| lc + mul_vars[0]);
cs.enforce(|| format!("constraint {i}"), |lc| lc + a, |lc| lc + b, |lc| lc + mul_vars[0])?;
}

for i in 0..mul_constraints {
cs.enforce(|| format!("constraint_mul {i}"), |lc| lc + mul_vars[i], |lc| lc + b, |lc| lc + mul_vars[i + 1]);
cs.enforce(
|| format!("constraint_mul {i}"),
|lc| lc + mul_vars[i],
|lc| lc + b,
|lc| lc + mul_vars[i + 1],
)?;
}

Ok(())
Expand Down
4 changes: 2 additions & 2 deletions algorithms/src/snark/marlin/marlin.rs
Original file line number Diff line number Diff line change
Expand Up @@ -391,7 +391,7 @@ where
let mut batch_sizes = BTreeMap::new();
let mut circuit_infos = BTreeMap::new();
let mut inputs_and_batch_sizes = BTreeMap::new();
let mut total_instances = 0;
let mut total_instances = 0u32;
let mut public_inputs = BTreeMap::new(); // inputs need to live longer than the rest of prover_state
let mut circuit_ids = Vec::with_capacity(keys_to_constraints.len());
for pk in keys_to_constraints.keys() {
Expand All @@ -404,7 +404,7 @@ where
circuit_infos.insert(circuit_id, &pk.circuit_verifying_key.circuit_info);
inputs_and_batch_sizes.insert(circuit_id, (batch_size, padded_public_input));
public_inputs.insert(circuit_id, public_input);
total_instances += batch_size;
total_instances = total_instances.saturating_add(batch_size);

let batch_size = usize::try_from(batch_size)?;
batch_sizes.insert(circuit_id, batch_size);
Expand Down
2 changes: 1 addition & 1 deletion circuit/environment/src/helpers/assignment.rs
Original file line number Diff line number Diff line change
Expand Up @@ -206,7 +206,7 @@ impl<F: PrimeField> snarkvm_r1cs::ConstraintSynthesizer<F> for Assignment<F> {
|lc| lc + convert_linear_combination(a),
|lc| lc + convert_linear_combination(b),
|lc| lc + convert_linear_combination(c),
);
)?;
}

// Ensure the given `cs` matches in size with the first system.
Expand Down
2 changes: 1 addition & 1 deletion circuit/environment/src/helpers/converter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ impl<F: PrimeField> R1CS<F> {
|lc| lc + convert_linear_combination(a),
|lc| lc + convert_linear_combination(b),
|lc| lc + convert_linear_combination(c),
);
)?;
}

// Ensure the given `cs` matches in size with the first system.
Expand Down
10 changes: 6 additions & 4 deletions r1cs/src/constraint_counter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
// along with the snarkVM library. If not, see <https://www.gnu.org/licenses/>.

use crate::{errors::SynthesisError, ConstraintSystem, Index, LinearCombination, Variable};
use anyhow::anyhow;
use snarkvm_fields::Field;

/// Constraint counter for testing purposes.
Expand All @@ -35,7 +36,7 @@ impl<ConstraintF: Field> ConstraintSystem<ConstraintF> for ConstraintCounter {
AR: AsRef<str>,
{
let var = Variable::new_unchecked(Index::Private(self.num_private_variables));
self.num_private_variables += 1;
self.num_private_variables = self.num_private_variables.checked_add(1).ok_or_else(|| anyhow!("overflow"))?;
Ok(var)
}

Expand All @@ -46,20 +47,21 @@ impl<ConstraintF: Field> ConstraintSystem<ConstraintF> for ConstraintCounter {
AR: AsRef<str>,
{
let var = Variable::new_unchecked(Index::Public(self.num_public_variables));
self.num_public_variables += 1;
self.num_public_variables = self.num_public_variables.checked_add(1).ok_or_else(|| anyhow!("overflow"))?;

Ok(var)
}

fn enforce<A, AR, LA, LB, LC>(&mut self, _: A, _: LA, _: LB, _: LC)
fn enforce<A, AR, LA, LB, LC>(&mut self, _: A, _: LA, _: LB, _: LC) -> Result<(), SynthesisError>
where
A: FnOnce() -> AR,
AR: AsRef<str>,
LA: FnOnce(LinearCombination<ConstraintF>) -> LinearCombination<ConstraintF>,
LB: FnOnce(LinearCombination<ConstraintF>) -> LinearCombination<ConstraintF>,
LC: FnOnce(LinearCombination<ConstraintF>) -> LinearCombination<ConstraintF>,
{
self.num_constraints += 1;
self.num_constraints = self.num_constraints.checked_add(1).ok_or_else(|| anyhow!("overflow"))?;
Ok(())
}

fn push_namespace<NR, N>(&mut self, _: N)
Expand Down
Loading

0 comments on commit 47de13c

Please sign in to comment.