impl comparator gadgets for fields and integers

This commit is contained in:
collin 2020-06-25 15:58:37 -07:00
parent cc8a3d9878
commit 7233e55dc1
5 changed files with 202 additions and 82 deletions

View File

@ -0,0 +1,28 @@
use snarkos_errors::gadgets::SynthesisError;
use snarkos_models::{
curves::Field,
gadgets::{r1cs::ConstraintSystem, utilities::boolean::Boolean},
};
pub trait EvaluateLtGadget<F: Field> {
fn less_than<CS: ConstraintSystem<F>>(&self, cs: CS, other: &Self) -> Result<Boolean, SynthesisError>;
}
// implementing `EvaluateLtGadget` will implement `ComparatorGadget`
pub trait ComparatorGadget<F: Field>
where
Self: EvaluateLtGadget<F>,
{
fn greater_than<CS: ConstraintSystem<F>>(&self, cs: CS, other: &Self) -> Result<Boolean, SynthesisError> {
other.less_than(cs, other)
}
fn less_than_or_equal<CS: ConstraintSystem<F>>(&self, cs: CS, other: &Self) -> Result<Boolean, SynthesisError> {
let is_gt = self.greater_than(cs, other)?;
Ok(is_gt.not())
}
fn greater_than_or_equal<CS: ConstraintSystem<F>>(&self, cs: CS, other: &Self) -> Result<Boolean, SynthesisError> {
other.less_than_or_equal(cs, self)
}
}

View File

@ -1,6 +1,7 @@
//! Methods to enforce constraints on expressions in a resolved Leo program.
use crate::{
comparator::{ComparatorGadget, EvaluateLtGadget},
constraints::{ConstrainedCircuitMember, ConstrainedProgram, ConstrainedValue},
enforce_and,
enforce_or,
@ -72,11 +73,11 @@ impl<F: Field + PrimeField, G: GroupType<F>> ConstrainedProgram<F, G> {
(ConstrainedValue::Integer(num_1), ConstrainedValue::Integer(num_2)) => {
Ok(ConstrainedValue::Integer(num_1.add(cs, num_2, span)?))
}
(ConstrainedValue::Field(fe_1), ConstrainedValue::Field(fe_2)) => {
Ok(ConstrainedValue::Field(fe_1.add(cs, &fe_2, span)?))
(ConstrainedValue::Field(field_1), ConstrainedValue::Field(field_2)) => {
Ok(ConstrainedValue::Field(field_1.add(cs, &field_2, span)?))
}
(ConstrainedValue::Group(ge_1), ConstrainedValue::Group(ge_2)) => {
Ok(ConstrainedValue::Group(ge_1.add(cs, &ge_2, span)?))
(ConstrainedValue::Group(point_1), ConstrainedValue::Group(point_2)) => {
Ok(ConstrainedValue::Group(point_1.add(cs, &point_2, span)?))
}
(ConstrainedValue::Unresolved(string), val_2) => {
let val_1 = ConstrainedValue::from_other(string, &val_2, span.clone())?;
@ -104,11 +105,11 @@ impl<F: Field + PrimeField, G: GroupType<F>> ConstrainedProgram<F, G> {
(ConstrainedValue::Integer(num_1), ConstrainedValue::Integer(num_2)) => {
Ok(ConstrainedValue::Integer(num_1.sub(cs, num_2, span)?))
}
(ConstrainedValue::Field(fe_1), ConstrainedValue::Field(fe_2)) => {
Ok(ConstrainedValue::Field(fe_1.sub(cs, &fe_2, span)?))
(ConstrainedValue::Field(field_1), ConstrainedValue::Field(field_2)) => {
Ok(ConstrainedValue::Field(field_1.sub(cs, &field_2, span)?))
}
(ConstrainedValue::Group(ge_1), ConstrainedValue::Group(ge_2)) => {
Ok(ConstrainedValue::Group(ge_1.sub(cs, &ge_2, span)?))
(ConstrainedValue::Group(point_1), ConstrainedValue::Group(point_2)) => {
Ok(ConstrainedValue::Group(point_1.sub(cs, &point_2, span)?))
}
(ConstrainedValue::Unresolved(string), val_2) => {
let val_1 = ConstrainedValue::from_other(string, &val_2, span.clone())?;
@ -136,8 +137,8 @@ impl<F: Field + PrimeField, G: GroupType<F>> ConstrainedProgram<F, G> {
(ConstrainedValue::Integer(num_1), ConstrainedValue::Integer(num_2)) => {
Ok(ConstrainedValue::Integer(num_1.mul(cs, num_2, span)?))
}
(ConstrainedValue::Field(fe_1), ConstrainedValue::Field(fe_2)) => {
Ok(ConstrainedValue::Field(fe_1.mul(cs, &fe_2, span)?))
(ConstrainedValue::Field(field_1), ConstrainedValue::Field(field_2)) => {
Ok(ConstrainedValue::Field(field_1.mul(cs, &field_2, span)?))
}
(ConstrainedValue::Unresolved(string), val_2) => {
let val_1 = ConstrainedValue::from_other(string, &val_2, span.clone())?;
@ -167,8 +168,8 @@ impl<F: Field + PrimeField, G: GroupType<F>> ConstrainedProgram<F, G> {
(ConstrainedValue::Integer(num_1), ConstrainedValue::Integer(num_2)) => {
Ok(ConstrainedValue::Integer(num_1.div(cs, num_2, span)?))
}
(ConstrainedValue::Field(fe_1), ConstrainedValue::Field(fe_2)) => {
Ok(ConstrainedValue::Field(fe_1.div(cs, &fe_2, span)?))
(ConstrainedValue::Field(field_1), ConstrainedValue::Field(field_2)) => {
Ok(ConstrainedValue::Field(field_1.div(cs, &field_2, span)?))
}
(ConstrainedValue::Unresolved(string), val_2) => {
let val_1 = ConstrainedValue::from_other(string, &val_2, span.clone())?;
@ -229,11 +230,11 @@ impl<F: Field + PrimeField, G: GroupType<F>> ConstrainedProgram<F, G> {
(ConstrainedValue::Integer(num_1), ConstrainedValue::Integer(num_2)) => {
num_1.evaluate_equal(unique_namespace, &num_2)
}
(ConstrainedValue::Field(fe_1), ConstrainedValue::Field(fe_2)) => {
fe_1.evaluate_equal(unique_namespace, &fe_2)
(ConstrainedValue::Field(field_1), ConstrainedValue::Field(field_2)) => {
field_1.evaluate_equal(unique_namespace, &field_2)
}
(ConstrainedValue::Group(ge_1), ConstrainedValue::Group(ge_2)) => {
ge_1.evaluate_equal(unique_namespace, &ge_2)
(ConstrainedValue::Group(point_1), ConstrainedValue::Group(point_2)) => {
point_1.evaluate_equal(unique_namespace, &point_2)
}
(ConstrainedValue::Unresolved(string), val_2) => {
let val_1 = ConstrainedValue::from_other(string, &val_2, span.clone())?;
@ -252,133 +253,157 @@ impl<F: Field + PrimeField, G: GroupType<F>> ConstrainedProgram<F, G> {
};
let boolean =
constraint_result.map_err(|e| ExpressionError::cannot_enforce(format!("evaluate equals"), e, span))?;
constraint_result.map_err(|e| ExpressionError::cannot_enforce(format!("evaluate equal"), e, span))?;
Ok(ConstrainedValue::Boolean(boolean))
}
//TODO: unsafe for allocated values
fn evaluate_ge_expression(
fn evaluate_ge_expression<CS: ConstraintSystem<F>>(
&mut self,
cs: &mut CS,
left: ConstrainedValue<F, G>,
right: ConstrainedValue<F, G>,
span: Span,
) -> Result<ConstrainedValue<F, G>, ExpressionError> {
match (left, right) {
let mut unique_namespace = cs.ns(|| format!("evaluate {} >= {} {}:{}", left, right, span.line, span.start));
let constraint_result = match (left, right) {
(ConstrainedValue::Integer(num_1), ConstrainedValue::Integer(num_2)) => {
let result = num_1.ge(&num_2);
Ok(ConstrainedValue::Boolean(Boolean::Constant(result)))
num_1.greater_than_or_equal(unique_namespace, &num_2)
}
(ConstrainedValue::Field(fe_1), ConstrainedValue::Field(fe_2)) => {
let result = fe_1.ge(&fe_2);
Ok(ConstrainedValue::Boolean(Boolean::Constant(result)))
(ConstrainedValue::Field(field_1), ConstrainedValue::Field(field_2)) => {
field_1.greater_than_or_equal(unique_namespace, &field_2)
}
(ConstrainedValue::Unresolved(string), val_2) => {
let val_1 = ConstrainedValue::from_other(string, &val_2, span.clone())?;
self.evaluate_ge_expression(val_1, val_2, span)
return self.evaluate_ge_expression(&mut unique_namespace, val_1, val_2, span);
}
(val_1, ConstrainedValue::Unresolved(string)) => {
let val_2 = ConstrainedValue::from_other(string, &val_1, span.clone())?;
self.evaluate_ge_expression(val_1, val_2, span)
return self.evaluate_ge_expression(&mut unique_namespace, val_1, val_2, span);
}
(val_1, val_2) => Err(ExpressionError::incompatible_types(
format!("{} >= {}", val_1, val_2),
span,
)),
}
(val_1, val_2) => {
return Err(ExpressionError::incompatible_types(
format!("{} >= {}", val_1, val_2),
span,
));
}
};
let boolean = constraint_result
.map_err(|e| ExpressionError::cannot_enforce(format!("evaluate greater than or equal"), e, span))?;
Ok(ConstrainedValue::Boolean(boolean))
}
//TODO: unsafe for allocated values
fn evaluate_gt_expression(
fn evaluate_gt_expression<CS: ConstraintSystem<F>>(
&mut self,
cs: &mut CS,
left: ConstrainedValue<F, G>,
right: ConstrainedValue<F, G>,
span: Span,
) -> Result<ConstrainedValue<F, G>, ExpressionError> {
match (left, right) {
let mut unique_namespace = cs.ns(|| format!("evaluate {} > {} {}:{}", left, right, span.line, span.start));
let constraint_result = match (left, right) {
(ConstrainedValue::Integer(num_1), ConstrainedValue::Integer(num_2)) => {
let result = num_1.gt(&num_2);
Ok(ConstrainedValue::Boolean(Boolean::Constant(result)))
num_1.greater_than(unique_namespace, &num_2)
}
(ConstrainedValue::Field(fe_1), ConstrainedValue::Field(fe_2)) => {
let result = fe_1.gt(&fe_2);
Ok(ConstrainedValue::Boolean(Boolean::Constant(result)))
(ConstrainedValue::Field(field_1), ConstrainedValue::Field(field_2)) => {
field_1.greater_than(unique_namespace, &field_2)
}
(ConstrainedValue::Unresolved(string), val_2) => {
let val_1 = ConstrainedValue::from_other(string, &val_2, span.clone())?;
self.evaluate_gt_expression(val_1, val_2, span)
return self.evaluate_gt_expression(&mut unique_namespace, val_1, val_2, span);
}
(val_1, ConstrainedValue::Unresolved(string)) => {
let val_2 = ConstrainedValue::from_other(string, &val_1, span.clone())?;
self.evaluate_gt_expression(val_1, val_2, span)
return self.evaluate_gt_expression(&mut unique_namespace, val_1, val_2, span);
}
(val_1, val_2) => Err(ExpressionError::incompatible_types(
format!("{} > {}", val_1, val_2),
span,
)),
}
(val_1, val_2) => {
return Err(ExpressionError::incompatible_types(
format!("{} > {}", val_1, val_2),
span,
));
}
};
let boolean = constraint_result
.map_err(|e| ExpressionError::cannot_enforce(format!("evaluate greater than"), e, span))?;
Ok(ConstrainedValue::Boolean(boolean))
}
//TODO: unsafe for allocated values
fn evaluate_le_expression(
fn evaluate_le_expression<CS: ConstraintSystem<F>>(
&mut self,
cs: &mut CS,
left: ConstrainedValue<F, G>,
right: ConstrainedValue<F, G>,
span: Span,
) -> Result<ConstrainedValue<F, G>, ExpressionError> {
match (left, right) {
let mut unique_namespace = cs.ns(|| format!("evaluate {} <= {} {}:{}", left, right, span.line, span.start));
let constraint_result = match (left, right) {
(ConstrainedValue::Integer(num_1), ConstrainedValue::Integer(num_2)) => {
let result = num_1.le(&num_2);
Ok(ConstrainedValue::Boolean(Boolean::Constant(result)))
num_1.less_than_or_equal(unique_namespace, &num_2)
}
(ConstrainedValue::Field(fe_1), ConstrainedValue::Field(fe_2)) => {
let result = fe_1.le(&fe_2);
Ok(ConstrainedValue::Boolean(Boolean::Constant(result)))
(ConstrainedValue::Field(field_1), ConstrainedValue::Field(field_2)) => {
field_1.less_than_or_equal(unique_namespace, &field_2)
}
(ConstrainedValue::Unresolved(string), val_2) => {
let val_1 = ConstrainedValue::from_other(string, &val_2, span.clone())?;
self.evaluate_le_expression(val_1, val_2, span)
return self.evaluate_le_expression(&mut unique_namespace, val_1, val_2, span);
}
(val_1, ConstrainedValue::Unresolved(string)) => {
let val_2 = ConstrainedValue::from_other(string, &val_1, span.clone())?;
self.evaluate_le_expression(val_1, val_2, span)
return self.evaluate_le_expression(&mut unique_namespace, val_1, val_2, span);
}
(val_1, val_2) => Err(ExpressionError::incompatible_types(
format!("{} <= {}", val_1, val_2),
span,
)),
}
(val_1, val_2) => {
return Err(ExpressionError::incompatible_types(
format!("{} <= {}", val_1, val_2),
span,
));
}
};
let boolean = constraint_result
.map_err(|e| ExpressionError::cannot_enforce(format!("evaluate less than or equal"), e, span))?;
Ok(ConstrainedValue::Boolean(boolean))
}
//TODO: unsafe for allocated values
fn evaluate_lt_expression(
fn evaluate_lt_expression<CS: ConstraintSystem<F>>(
&mut self,
cs: &mut CS,
left: ConstrainedValue<F, G>,
right: ConstrainedValue<F, G>,
span: Span,
) -> Result<ConstrainedValue<F, G>, ExpressionError> {
match (left, right) {
let mut unique_namespace = cs.ns(|| format!("evaluate {} < {} {}:{}", left, right, span.line, span.start));
let constraint_result = match (left, right) {
(ConstrainedValue::Integer(num_1), ConstrainedValue::Integer(num_2)) => {
let result = num_1.lt(&num_2);
Ok(ConstrainedValue::Boolean(Boolean::Constant(result)))
num_1.less_than(unique_namespace, &num_2)
}
(ConstrainedValue::Field(fe_1), ConstrainedValue::Field(fe_2)) => {
let result = fe_1.lt(&fe_2);
Ok(ConstrainedValue::Boolean(Boolean::Constant(result)))
(ConstrainedValue::Field(field_1), ConstrainedValue::Field(field_2)) => {
field_1.less_than(unique_namespace, &field_2)
}
(ConstrainedValue::Unresolved(string), val_2) => {
let val_1 = ConstrainedValue::from_other(string, &val_2, span.clone())?;
self.evaluate_lt_expression(val_1, val_2, span)
return self.evaluate_lt_expression(&mut unique_namespace, val_1, val_2, span);
}
(val_1, ConstrainedValue::Unresolved(string)) => {
let val_2 = ConstrainedValue::from_other(string, &val_1, span.clone())?;
self.evaluate_lt_expression(val_1, val_2, span)
return self.evaluate_lt_expression(&mut unique_namespace, val_1, val_2, span);
}
(val_1, val_2) => Err(ExpressionError::incompatible_types(
format!("{} < {}", val_1, val_2,),
span,
)),
}
(val_1, val_2) => {
return Err(ExpressionError::incompatible_types(
format!("{} < {}", val_1, val_2),
span,
));
}
};
let boolean =
constraint_result.map_err(|e| ExpressionError::cannot_enforce(format!("evaluate less than"), e, span))?;
Ok(ConstrainedValue::Boolean(boolean))
}
/// Enforce ternary conditional expression
@ -1034,7 +1059,7 @@ impl<F: Field + PrimeField, G: GroupType<F>> ConstrainedProgram<F, G> {
span.clone(),
)?;
Ok(self.evaluate_ge_expression(resolved_left, resolved_right, span)?)
Ok(self.evaluate_ge_expression(cs, resolved_left, resolved_right, span)?)
}
Expression::Gt(left, right, span) => {
let (resolved_left, resolved_right) = self.enforce_binary_expression(
@ -1047,7 +1072,7 @@ impl<F: Field + PrimeField, G: GroupType<F>> ConstrainedProgram<F, G> {
span.clone(),
)?;
Ok(self.evaluate_gt_expression(resolved_left, resolved_right, span)?)
Ok(self.evaluate_gt_expression(cs, resolved_left, resolved_right, span)?)
}
Expression::Le(left, right, span) => {
let (resolved_left, resolved_right) = self.enforce_binary_expression(
@ -1060,7 +1085,7 @@ impl<F: Field + PrimeField, G: GroupType<F>> ConstrainedProgram<F, G> {
span.clone(),
)?;
Ok(self.evaluate_le_expression(resolved_left, resolved_right, span)?)
Ok(self.evaluate_le_expression(cs, resolved_left, resolved_right, span)?)
}
Expression::Lt(left, right, span) => {
let (resolved_left, resolved_right) = self.enforce_binary_expression(
@ -1073,7 +1098,7 @@ impl<F: Field + PrimeField, G: GroupType<F>> ConstrainedProgram<F, G> {
span.clone(),
)?;
Ok(self.evaluate_lt_expression(resolved_left, resolved_right, span)?)
Ok(self.evaluate_lt_expression(cs, resolved_left, resolved_right, span)?)
}
// Conditionals

View File

@ -1,5 +1,5 @@
//! Conversion of integer declarations to constraints in Leo.
use crate::errors::IntegerError;
use crate::{errors::IntegerError, ComparatorGadget, EvaluateLtGadget};
use leo_types::{InputValue, IntegerType, Span};
use snarkos_errors::gadgets::SynthesisError;
@ -88,6 +88,16 @@ impl Integer {
Ok(value as usize)
}
pub fn to_bits_le(&self) -> Vec<Boolean> {
match self {
Integer::U8(num) => num.bits.clone(),
Integer::U16(num) => num.bits.clone(),
Integer::U32(num) => num.bits.clone(),
Integer::U64(num) => num.bits.clone(),
Integer::U128(num) => num.bits.clone(),
}
}
pub fn get_type(&self) -> IntegerType {
match self {
Integer::U8(_u8) => IntegerType::U8,
@ -435,6 +445,34 @@ impl<F: Field + PrimeField> EvaluateEqGadget<F> for Integer {
}
}
impl<F: Field + PrimeField> EvaluateLtGadget<F> for Integer {
fn less_than<CS: ConstraintSystem<F>>(&self, mut cs: CS, other: &Self) -> Result<Boolean, SynthesisError> {
if self.to_bits_le().len() != other.to_bits_le().len() {
return Err(SynthesisError::Unsatisfiable);
}
for (i, (self_bit, other_bit)) in self
.to_bits_le()
.iter()
.rev()
.zip(other.to_bits_le().iter().rev())
.enumerate()
{
let is_less = Boolean::and(&mut cs, self_bit, &other_bit.not())?;
if is_less.eq(&Boolean::constant(true)) {
return Ok(is_less);
} else if i == self.to_bits_le().len() - 1 {
return Ok(is_less);
}
}
Err(SynthesisError::Unsatisfiable)
}
}
impl<F: Field + PrimeField> ComparatorGadget<F> for Integer {}
impl<F: Field + PrimeField> EqGadget<F> for Integer {}
impl<F: Field + PrimeField> ConditionalEqGadget<F> for Integer {

View File

@ -3,6 +3,9 @@
pub(crate) mod boolean;
pub(crate) use boolean::*;
pub(crate) mod comparator;
pub(crate) use comparator::*;
pub mod function;
pub use function::*;

View File

@ -3,6 +3,7 @@
use crate::errors::FieldError;
use leo_types::Span;
use crate::{ComparatorGadget, EvaluateLtGadget};
use snarkos_errors::gadgets::SynthesisError;
use snarkos_models::{
curves::{Field, PrimeField},
@ -210,6 +211,31 @@ impl<F: Field + PrimeField> EvaluateEqGadget<F> for FieldType<F> {
}
}
impl<F: Field + PrimeField> EvaluateLtGadget<F> for FieldType<F> {
fn less_than<CS: ConstraintSystem<F>>(&self, mut cs: CS, other: &Self) -> Result<Boolean, SynthesisError> {
match (self, other) {
(FieldType::Constant(first), FieldType::Constant(second)) => Ok(Boolean::constant(first.lt(second))),
(FieldType::Allocated(allocated), FieldType::Constant(constant))
| (FieldType::Constant(constant), FieldType::Allocated(allocated)) => {
let bool_option = allocated.value.map(|f| f.lt(constant));
Boolean::alloc(&mut cs.ns(|| "less than"), || {
bool_option.ok_or(SynthesisError::AssignmentMissing)
})
}
(FieldType::Allocated(first), FieldType::Allocated(second)) => {
let bool_option = first.value.and_then(|a| second.value.map(|b| a.eq(&b)));
Boolean::alloc(&mut cs.ns(|| "evaluate_equal"), || {
bool_option.ok_or(SynthesisError::AssignmentMissing)
})
}
}
}
}
impl<F: Field + PrimeField> ComparatorGadget<F> for FieldType<F> {}
impl<F: Field + PrimeField> EqGadget<F> for FieldType<F> {}
impl<F: Field + PrimeField> ConditionalEqGadget<F> for FieldType<F> {