mirror of
https://github.com/ProvableHQ/leo.git
synced 2024-09-11 05:45:30 +03:00
impl field comparator functionality
This commit is contained in:
parent
f071764548
commit
1bfc31c4d5
@ -1,4 +1,7 @@
|
||||
function main() -> (fe) {
|
||||
a = 2fe ** 3;
|
||||
return a
|
||||
if (4fe >= 4fe) {
|
||||
return 5fe
|
||||
} else {
|
||||
return 2fe
|
||||
}
|
||||
}
|
@ -93,7 +93,7 @@ impl<F: Field + PrimeField, CS: ConstraintSystem<F>> ResolvedProgram<F, CS> {
|
||||
ResolvedValue::Boolean(Boolean::Constant(bool))
|
||||
}
|
||||
|
||||
pub(crate) fn enforce_not(value: ResolvedValue<F>) -> ResolvedValue<F> {
|
||||
pub(crate) fn evaluate_not(value: ResolvedValue<F>) -> ResolvedValue<F> {
|
||||
match value {
|
||||
ResolvedValue::Boolean(boolean) => ResolvedValue::Boolean(boolean.not()),
|
||||
value => unimplemented!("cannot enforce not on non-boolean value {}", value),
|
||||
|
@ -133,7 +133,71 @@ impl<F: Field + PrimeField, CS: ConstraintSystem<F>> ResolvedProgram<F, CS> {
|
||||
(ResolvedValue::FieldElement(fe1), ResolvedValue::FieldElement(fe2)) => {
|
||||
Self::field_eq(fe1, fe2)
|
||||
}
|
||||
(val1, val2) => unimplemented!("cannot enforce equality between {} == {}", val1, val2),
|
||||
(val1, val2) => unimplemented!("cannot evaluate {} == {}", val1, val2),
|
||||
}
|
||||
}
|
||||
|
||||
fn evaluate_geq_expression(
|
||||
&mut self,
|
||||
left: ResolvedValue<F>,
|
||||
right: ResolvedValue<F>,
|
||||
) -> ResolvedValue<F> {
|
||||
match (left, right) {
|
||||
(ResolvedValue::FieldElement(fe1), ResolvedValue::FieldElement(fe2)) => {
|
||||
Self::field_geq(fe1, fe2)
|
||||
}
|
||||
(val1, val2) => unimplemented!(
|
||||
"cannot evaluate {} >= {}, values must be fields",
|
||||
val1,
|
||||
val2
|
||||
),
|
||||
}
|
||||
}
|
||||
|
||||
fn evaluate_gt_expression(
|
||||
&mut self,
|
||||
left: ResolvedValue<F>,
|
||||
right: ResolvedValue<F>,
|
||||
) -> ResolvedValue<F> {
|
||||
match (left, right) {
|
||||
(ResolvedValue::FieldElement(fe1), ResolvedValue::FieldElement(fe2)) => {
|
||||
Self::field_gt(fe1, fe2)
|
||||
}
|
||||
(val1, val2) => {
|
||||
unimplemented!("cannot evaluate {} > {}, values must be fields", val1, val2)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn evaluate_leq_expression(
|
||||
&mut self,
|
||||
left: ResolvedValue<F>,
|
||||
right: ResolvedValue<F>,
|
||||
) -> ResolvedValue<F> {
|
||||
match (left, right) {
|
||||
(ResolvedValue::FieldElement(fe1), ResolvedValue::FieldElement(fe2)) => {
|
||||
Self::field_leq(fe1, fe2)
|
||||
}
|
||||
(val1, val2) => unimplemented!(
|
||||
"cannot evaluate {} <= {}, values must be fields",
|
||||
val1,
|
||||
val2
|
||||
),
|
||||
}
|
||||
}
|
||||
|
||||
fn evaluate_lt_expression(
|
||||
&mut self,
|
||||
left: ResolvedValue<F>,
|
||||
right: ResolvedValue<F>,
|
||||
) -> ResolvedValue<F> {
|
||||
match (left, right) {
|
||||
(ResolvedValue::FieldElement(fe1), ResolvedValue::FieldElement(fe2)) => {
|
||||
Self::field_lt(fe1, fe2)
|
||||
}
|
||||
(val1, val2) => {
|
||||
unimplemented!("cannot evaluate {} < {}, values must be fields", val1, val2)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -152,7 +216,7 @@ impl<F: Field + PrimeField, CS: ConstraintSystem<F>> ResolvedProgram<F, CS> {
|
||||
Self::enforce_u32_eq(cs, num1, num2)
|
||||
}
|
||||
(ResolvedValue::FieldElement(fe1), ResolvedValue::FieldElement(fe2)) => {
|
||||
self.enforce_field_eq(fe1, fe2)
|
||||
self.enforce_field_eq(cs, fe1, fe2)
|
||||
}
|
||||
(val1, val2) => unimplemented!("cannot enforce equality between {} == {}", val1, val2),
|
||||
}
|
||||
@ -404,7 +468,7 @@ impl<F: Field + PrimeField, CS: ConstraintSystem<F>> ResolvedProgram<F, CS> {
|
||||
}
|
||||
|
||||
// Boolean operations
|
||||
Expression::Not(expression) => Self::enforce_not(self.enforce_expression(
|
||||
Expression::Not(expression) => Self::evaluate_not(self.enforce_expression(
|
||||
cs,
|
||||
file_scope,
|
||||
function_scope,
|
||||
@ -435,16 +499,36 @@ impl<F: Field + PrimeField, CS: ConstraintSystem<F>> ResolvedProgram<F, CS> {
|
||||
self.evaluate_eq_expression(resolved_left, resolved_right)
|
||||
}
|
||||
Expression::Geq(left, right) => {
|
||||
unimplemented!("expression {} >= {} unimplemented", left, right)
|
||||
let resolved_left =
|
||||
self.enforce_expression(cs, file_scope.clone(), function_scope.clone(), *left);
|
||||
let resolved_right =
|
||||
self.enforce_expression(cs, file_scope.clone(), function_scope.clone(), *right);
|
||||
|
||||
self.evaluate_geq_expression(resolved_left, resolved_right)
|
||||
}
|
||||
Expression::Gt(left, right) => {
|
||||
unimplemented!("expression {} > {} unimplemented", left, right)
|
||||
let resolved_left =
|
||||
self.enforce_expression(cs, file_scope.clone(), function_scope.clone(), *left);
|
||||
let resolved_right =
|
||||
self.enforce_expression(cs, file_scope.clone(), function_scope.clone(), *right);
|
||||
|
||||
self.evaluate_gt_expression(resolved_left, resolved_right)
|
||||
}
|
||||
Expression::Leq(left, right) => {
|
||||
unimplemented!("expression {} <= {} unimplemented", left, right)
|
||||
let resolved_left =
|
||||
self.enforce_expression(cs, file_scope.clone(), function_scope.clone(), *left);
|
||||
let resolved_right =
|
||||
self.enforce_expression(cs, file_scope.clone(), function_scope.clone(), *right);
|
||||
|
||||
self.evaluate_leq_expression(resolved_left, resolved_right)
|
||||
}
|
||||
Expression::Lt(left, right) => {
|
||||
unimplemented!("expression {} < {} unimplemented", left, right)
|
||||
let resolved_left =
|
||||
self.enforce_expression(cs, file_scope.clone(), function_scope.clone(), *left);
|
||||
let resolved_right =
|
||||
self.enforce_expression(cs, file_scope.clone(), function_scope.clone(), *right);
|
||||
|
||||
self.evaluate_lt_expression(resolved_left, resolved_right)
|
||||
}
|
||||
|
||||
// Conditionals
|
||||
|
@ -4,6 +4,7 @@ use crate::constraints::{ResolvedProgram, ResolvedValue};
|
||||
use crate::{new_variable_from_variable, Parameter, Variable};
|
||||
|
||||
use snarkos_models::curves::{Field, PrimeField};
|
||||
use snarkos_models::gadgets::r1cs::LinearCombination;
|
||||
use snarkos_models::gadgets::utilities::uint32::UInt32;
|
||||
use snarkos_models::gadgets::{r1cs::ConstraintSystem, utilities::boolean::Boolean};
|
||||
// use std::ops::{Add, Div, Mul, Neg, Sub};
|
||||
@ -90,8 +91,34 @@ impl<F: Field + PrimeField, CS: ConstraintSystem<F>> ResolvedProgram<F, CS> {
|
||||
pub(crate) fn field_eq(fe1: F, fe2: F) -> ResolvedValue<F> {
|
||||
ResolvedValue::Boolean(Boolean::Constant(fe1.eq(&fe2)))
|
||||
}
|
||||
pub(crate) fn enforce_field_eq(&mut self, _fe1: F, _fe2: F) -> ResolvedValue<F> {
|
||||
unimplemented!("field equality enforcement not implemented")
|
||||
|
||||
pub(crate) fn field_geq(fe1: F, fe2: F) -> ResolvedValue<F> {
|
||||
ResolvedValue::Boolean(Boolean::Constant(fe1.ge(&fe2)))
|
||||
}
|
||||
|
||||
pub(crate) fn field_gt(fe1: F, fe2: F) -> ResolvedValue<F> {
|
||||
ResolvedValue::Boolean(Boolean::Constant(fe1.gt(&fe2)))
|
||||
}
|
||||
|
||||
pub(crate) fn field_leq(fe1: F, fe2: F) -> ResolvedValue<F> {
|
||||
ResolvedValue::Boolean(Boolean::Constant(fe1.le(&fe2)))
|
||||
}
|
||||
|
||||
pub(crate) fn field_lt(fe1: F, fe2: F) -> ResolvedValue<F> {
|
||||
ResolvedValue::Boolean(Boolean::Constant(fe1.lt(&fe2)))
|
||||
}
|
||||
|
||||
pub(crate) fn enforce_field_eq(&mut self, cs: &mut CS, fe1: F, fe2: F) -> ResolvedValue<F> {
|
||||
let mut lc = LinearCombination::zero();
|
||||
|
||||
// add (fe1 * 1) and subtract (fe2 * 1) from the linear combination
|
||||
lc = lc + (fe1, CS::one()) - (fe2, CS::one());
|
||||
|
||||
// enforce that the linear combination is zero
|
||||
cs.enforce(|| "field equality", |lc| lc, |lc| lc, |_| lc);
|
||||
|
||||
// return success
|
||||
ResolvedValue::Boolean(Boolean::constant(true))
|
||||
}
|
||||
|
||||
pub(crate) fn enforce_field_add(&mut self, fe1: F, fe2: F) -> ResolvedValue<F> {
|
||||
|
@ -32,10 +32,14 @@ operation_mul = { "*" }
|
||||
operation_div = { "/" }
|
||||
operation_pow = { "**" }
|
||||
|
||||
operation_binary = _{
|
||||
operation_and | operation_or |
|
||||
operation_compare = _{
|
||||
operation_eq | operation_neq |
|
||||
operation_geq | operation_gt | operation_leq | operation_lt |
|
||||
operation_geq | operation_gt |
|
||||
operation_leq | operation_lt
|
||||
}
|
||||
|
||||
operation_binary = _{
|
||||
operation_compare | operation_and | operation_or |
|
||||
operation_add | operation_sub | operation_pow | operation_mul | operation_div
|
||||
}
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user