Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add an AllocatedNum addition constraint #39

Merged
merged 2 commits into from
Oct 22, 2023
Merged
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
53 changes: 53 additions & 0 deletions crates/bellpepper-core/src/gadgets/num.rs
Original file line number Diff line number Diff line change
Expand Up @@ -276,6 +276,38 @@ impl<Scalar: PrimeField> AllocatedNum<Scalar> {
Ok(bits.into_iter().map(Boolean::from).collect())
}

pub fn add<CS>(&self, mut cs: CS, other: &Self) -> Result<Self, SynthesisError>
where
CS: ConstraintSystem<Scalar>,
{
let mut value = None;

let var = cs.alloc(
|| "sum num",
|| {
let mut tmp = self.value.ok_or(SynthesisError::AssignmentMissing)?;
tmp.add_assign(other.value.ok_or(SynthesisError::AssignmentMissing)?);

value = Some(tmp);

Ok(tmp)
},
)?;

// Constrain: (a + b) * 1 = a + b
cs.enforce(
|| "addition constraint",
|lc| lc + self.variable + other.variable,
|lc| lc + CS::one(),
|lc| lc + var,
);

Ok(AllocatedNum {
value,
variable: var,
})
}

pub fn mul<CS>(&self, mut cs: CS, other: &Self) -> Result<Self, SynthesisError>
where
CS: ConstraintSystem<Scalar>,
Expand Down Expand Up @@ -539,6 +571,27 @@ mod test {
assert!(cs.get("num") == Fr::ONE);
}

#[test]
fn test_num_addition() {
Copy link
Contributor

Choose a reason for hiding this comment

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

It would be great to see some negative testing here.
Another useful tool would be to exemplify the modular nature of the addition, e.g. by using something close to the field modulus as one of the operands.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I have updated the test.

let mut cs = TestConstraintSystem::<Fr>::new();

let mut char = Fr::char();
char[0] -= 1u8;
let mod_minus_one = Fr::from_repr(char);
assert!(bool::from(mod_minus_one.is_some()));
let mod_minus_one = mod_minus_one.unwrap();

let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(mod_minus_one)).unwrap();
let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::ONE)).unwrap();
let c = a.add(&mut cs, &b).unwrap();

assert!(cs.is_satisfied());
assert!(cs.get("sum num") == Fr::ZERO);
assert!(c.value.unwrap() == Fr::ZERO);
cs.set("sum num", Fr::ONE);
assert!(!cs.is_satisfied());
Comment on lines +588 to +592
Copy link
Contributor Author

@varunthakore varunthakore Oct 21, 2023

Choose a reason for hiding this comment

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

@huitseeker By negative testing, do you mean to add tests such that the constraint system is not satisfied ? I am checking for this on lines 591-592.

}

#[test]
fn test_num_squaring() {
let mut cs = TestConstraintSystem::<Fr>::new();
Expand Down
Loading