ProvableHQ/leo
1
1
Fork 0
mirror of https://github.com/ProvableHQ/leo.git synced 2024-12-26 11:45:00 +03:00
Code Issues Packages Projects Releases Wiki Activity

impl binary adder, rca, addition test

Browse Source
This commit is contained in:
collin 2020-07-10 18:05:37 -07:00
parent 390296126b
commit 159e7cba9d
13 changed files with 155 additions and 83 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
gadgets/src/binary/adder.rs Normal file
View File

@ -0,0 +1,39 @@
use snarkos_errors::gadgets::SynthesisError;
use snarkos_models::{
curves::Field,
gadgets::{r1cs::ConstraintSystem, utilities::boolean::Boolean},
};
/// Single bit binary adder with carry bit
/// sum = (a XOR b) XOR carry
/// carry = a AND b OR carry AND (a XOR b)
/// Returns (sum, carry)
pub trait FullAdder<'a, F: Field>
where
Self: std::marker::Sized,
{
fn add<CS: ConstraintSystem<F>>(
cs: CS,
a: &'a Self,
b: &'a Self,
carry: &'a Self,
) -> Result<(Self, Self), SynthesisError>;
}
impl<'a, F: Field> FullAdder<'a, F> for Boolean {
fn add<CS: ConstraintSystem<F>>(
mut cs: CS,
a: &'a Self,
b: &'a Self,
carry: &'a Self,
) -> Result<(Self, Self), SynthesisError> {
let a_x_b = Boolean::xor(cs.ns(|| format!("a XOR b")), a, b)?;
let sum = Boolean::xor(cs.ns(|| format!("adder sum")), &a_x_b, carry)?;
let c1 = Boolean::and(cs.ns(|| format!("a AND b")), a, b)?;
let c2 = Boolean::and(cs.ns(|| format!("carry AND (a XOR b)")), carry, &a_x_b)?;
let carry = Boolean::or(cs.ns(|| format!("c1 OR c2")), &c1, &c2)?;
Ok((sum, carry))
}
}

6
gadgets/src/binary/mod.rs Normal file
View File

@ -0,0 +1,6 @@
#[macro_use]
pub mod adder;
pub use self::adder::*;
pub mod rca;
pub use self::rca::*;

44
gadgets/src/binary/rca.rs Normal file
View File

@ -0,0 +1,44 @@
use crate::{binary::FullAdder, signed_integer::*};
use snarkos_errors::gadgets::SynthesisError;
use snarkos_models::{
curves::PrimeField,
gadgets::{r1cs::ConstraintSystem, utilities::boolean::Boolean},
};
/// Returns the bitwise sum of a n-bit number with carry bit
pub trait RippleCarryAdder<Rhs = Self>
where
Self: std::marker::Sized,
{
#[must_use]
fn add_bits<F: PrimeField, CS: ConstraintSystem<F>>(
&self,
cs: CS,
other: &Self,
) -> Result<Vec<Boolean>, SynthesisError>;
}
macro_rules! rpc_impl {
($($gadget: ident)*) => ($(
impl RippleCarryAdder for $gadget {
fn add_bits<F: PrimeField, CS: ConstraintSystem<F>>(&self, mut cs: CS, other: &Self) -> Result<Vec<Boolean>, SynthesisError> {
let mut result = vec![];
let mut carry = Boolean::constant(false);
for (i, (a, b)) in self.bits.iter().zip(other.bits.iter()).enumerate() {
let (sum, next) = Boolean::add(cs.ns(|| format!("rpc {}", i)), a, b, &carry)?;
carry = next;
result.push(sum);
}
// append the carry bit to the end
result.push(carry);
Ok(result)
}
}
)*)
}
rpc_impl!(Int8 Int16 Int32 Int64);

3
gadgets/src/errors/signed_integer.rs
View File

@ -2,6 +2,9 @@ use snarkos_errors::gadgets::SynthesisError;
#[derive(Debug, Error)]
pub enum IntegerError {
#[error("Integer overflow")]
Overflow,
#[error("{}", _0)]
SynthesisError(#[from] SynthesisError),
}

2
gadgets/src/lib.rs
View File

@ -1,6 +1,8 @@
#[macro_use]
extern crate thiserror;
pub mod binary;
pub mod errors;
pub mod signed_integer;

72
gadgets/src/signed_integer/arithmetic/add.rs
View File

@ -1,4 +1,4 @@
use crate::{errors::IntegerError, Int, Int128, Int16, Int32, Int64, Int8};
use crate::{binary::RippleCarryAdder, errors::IntegerError, Int, Int16, Int32, Int64, Int8};
use snarkos_models::{
curves::{fp_parameters::FpParameters, PrimeField},
@ -28,60 +28,42 @@ macro_rules! add_int_impl {
// in the scalar field
assert!(F::Params::MODULUS_BITS >= 128);
// Compute the maximum value of the sum so we allocate enough bits for the result
// Compute the maximum value of the sum
let mut max_value = 2i128 * i128::from(<$gadget as Int>::IntegerType::max_value());
// Keep track of the resulting value
let mut result_value = self.value.clone().map(|v| i128::from(v));
// Accumulate the value
let result_value = match (self.value, other.value) {
(Some(a), Some(b)) => {
// check for addition overflow here
let val = match a.checked_add(b) {
Some(val) => val,
None => return Err(IntegerError::Overflow)
};
Some(i128::from(val))
},
_ => {
// If any of the operands have unknown value, we won't
// know the value of the result
None
}
};
// This is a linear combination that we will enforce to be zero
let mut lc = LinearCombination::zero();
let mut all_constants = true;
// Accumulate the value
match other.value {
Some(val) => {
result_value.as_mut().map(|v| *v += i128::from(val));
}
None => {
// If any of the operands have unknown value, we won't
// know the value of the result
result_value = None;
}
}
let mut bits = self.add_bits(cs.ns(|| format!("bits")), other)?;
// we discard the carry since we check for overflow above
let _carry = bits.pop();
// Iterate over each bit_gadget of self and add each bit to
// the linear combination
let mut coeff = F::one();
for bit in &self.bits {
match *bit {
Boolean::Is(ref bit) => {
all_constants = false;
// Add the coeff * bit_gadget
lc = lc + (coeff, bit.get_variable());
}
Boolean::Not(ref bit) => {
all_constants = false;
// Add coeff * (1 - bit_gadget) = coeff * ONE - coeff * bit_gadget
lc = lc + (coeff, CS::one()) - (coeff, bit.get_variable());
}
Boolean::Constant(bit) => {
if bit {
lc = lc + (coeff, CS::one());
}
}
}
coeff.double_in_place();
}
// Iterate over each bit_gadget of self and add each bit to
// the linear combination
for bit in &other.bits {
match *bit {
for bit in bits {
match bit {
Boolean::Is(ref bit) => {
all_constants = false;
@ -107,8 +89,6 @@ macro_rules! add_int_impl {
// The value of the actual result is modulo 2 ^ $size
let modular_value = result_value.map(|v| v as <$gadget as Int>::IntegerType);
println!("{}", modular_value.unwrap());
if all_constants && modular_value.is_some() {
// We can just return a constant, rather than
// unpacking the result into allocated bits.
@ -154,4 +134,4 @@ macro_rules! add_int_impl {
)*)
}
add_int_impl!(Int8 Int16 Int32 Int64 Int128);
add_int_impl!(Int8 Int16 Int32 Int64);

4
gadgets/src/signed_integer/arithmetic/div.rs
View File

@ -1,4 +1,4 @@
use crate::{errors::IntegerError, Int128, Int16, Int32, Int64, Int8};
use crate::{errors::IntegerError, Int16, Int32, Int64, Int8};
use snarkos_models::{curves::PrimeField, gadgets::r1cs::ConstraintSystem};
/// Modular division for a signed integer gadget
@ -20,4 +20,4 @@ macro_rules! div_int_impl {
)*)
}
div_int_impl!(Int8 Int16 Int32 Int64 Int128);
div_int_impl!(Int8 Int16 Int32 Int64);

4
gadgets/src/signed_integer/arithmetic/mul.rs
View File

@ -1,4 +1,4 @@
use crate::{errors::IntegerError, Int128, Int16, Int32, Int64, Int8};
use crate::{errors::IntegerError, Int16, Int32, Int64, Int8};
use snarkos_models::{curves::PrimeField, gadgets::r1cs::ConstraintSystem};
/// Modular multiplication for a signed integer gadget
@ -20,4 +20,4 @@ macro_rules! mul_int_impl {
)*)
}
mul_int_impl!(Int8 Int16 Int32 Int64 Int128);
mul_int_impl!(Int8 Int16 Int32 Int64);

4
gadgets/src/signed_integer/arithmetic/pow.rs
View File

@ -1,4 +1,4 @@
use crate::{errors::IntegerError, Int128, Int16, Int32, Int64, Int8};
use crate::{errors::IntegerError, Int16, Int32, Int64, Int8};
use snarkos_models::{curves::PrimeField, gadgets::r1cs::ConstraintSystem};
/// Modular exponentiation for a signed integer gadget
@ -20,4 +20,4 @@ macro_rules! pow_int_impl {
)*)
}
pow_int_impl!(Int8 Int16 Int32 Int64 Int128);
pow_int_impl!(Int8 Int16 Int32 Int64);

4
gadgets/src/signed_integer/arithmetic/sub.rs
View File

@ -1,4 +1,4 @@
use crate::{errors::IntegerError, Int128, Int16, Int32, Int64, Int8};
use crate::{errors::IntegerError, Int16, Int32, Int64, Int8};
use snarkos_models::{curves::PrimeField, gadgets::r1cs::ConstraintSystem};
/// Modular subtraction for a signed integer gadget
@ -20,4 +20,4 @@ macro_rules! sub_int_impl {
)*)
}
sub_int_impl!(Int8 Int16 Int32 Int64 Int128);
sub_int_impl!(Int8 Int16 Int32 Int64);

1
gadgets/src/signed_integer/int_impl.rs
View File

@ -81,4 +81,3 @@ int_impl!(Int8, i8, 8);
int_impl!(Int16, i16, 16);
int_impl!(Int32, i32, 32);
int_impl!(Int64, i64, 64);
int_impl!(Int128, i128, 128);

4
gadgets/src/signed_integer/utilities/alloc.rs
View File

@ -1,4 +1,4 @@
use crate::{Int, Int128, Int16, Int32, Int64, Int8};
use crate::{Int, Int16, Int32, Int64, Int8};
use core::borrow::Borrow;
use snarkos_errors::gadgets::SynthesisError;
@ -99,4 +99,4 @@ macro_rules! alloc_int_impl {
)*)
}
alloc_int_impl!(Int8 Int16 Int32 Int64 Int128);
alloc_int_impl!(Int8 Int16 Int32 Int64);

51
gadgets/tests/signed_integer/i8.rs
View File

@ -53,7 +53,10 @@ fn test_int8_add_constants() {
let a_bit = Int8::constant(a);
let b_bit = Int8::constant(b);
let expected = a.wrapping_add(b);
let expected = match a.checked_add(b) {
Some(valid) => valid,
None => continue,
};
let r = a_bit.add(cs.ns(|| "addition"), &b_bit).unwrap();
@ -67,39 +70,35 @@ fn test_int8_add_constants() {
fn test_int8_add() {
let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
// for _ in 0..1000 {
let mut cs = TestConstraintSystem::<Fr>::new();
for _ in 0..1000 {
let mut cs = TestConstraintSystem::<Fr>::new();
// let a: i8 = rng.gen();
// let b: i8 = rng.gen();
let a = 15i8;
let b = -5i8;
let a: i8 = rng.gen();
let b: i8 = rng.gen();
println!("a {}", a);
println!("b {}", b);
let expected = match a.checked_add(b) {
Some(valid) => valid,
None => continue,
};
let expected = a.wrapping_add(b);
let a_bit = Int8::alloc(cs.ns(|| "a_bit"), || Ok(a)).unwrap();
let b_bit = Int8::alloc(cs.ns(|| "b_bit"), || Ok(b)).unwrap();
let a_bit = Int8::alloc(cs.ns(|| "a_bit"), || Ok(a)).unwrap();
let b_bit = Int8::alloc(cs.ns(|| "b_bit"), || Ok(b)).unwrap();
let r = a_bit.add(cs.ns(|| "addition"), &b_bit).unwrap();
let r = a_bit.add(cs.ns(|| "addition"), &b_bit).unwrap();
assert!(cs.is_satisfied());
println!("{:?}", r.bits);
assert!(r.value == Some(expected));
assert!(cs.is_satisfied());
check_all_allocated_bits(expected, r);
assert!(r.value == Some(expected));
// Flip a bit_gadget and see if the addition constraint still works
if cs.get("addition/result bit_gadget 0/boolean").is_zero() {
cs.set("addition/result bit_gadget 0/boolean", Fr::one());
} else {
cs.set("addition/result bit_gadget 0/boolean", Fr::zero());
}
check_all_allocated_bits(expected, r);
// Flip a bit_gadget and see if the addition constraint still works
if cs.get("addition/result bit_gadget 0/boolean").is_zero() {
cs.set("addition/result bit_gadget 0/boolean", Fr::one());
} else {
cs.set("addition/result bit_gadget 0/boolean", Fr::zero());
assert!(!cs.is_satisfied());
}
assert!(!cs.is_satisfied());
// }
}