From afdb9311fa5ae48e261b4200ed1b189a26fe386e Mon Sep 17 00:00:00 2001 From: dark64 Date: Tue, 26 Sep 2023 11:25:29 +0200 Subject: [PATCH 1/5] implement field idiv and rem ops --- Cargo.toml | 2 +- zokrates_analysis/src/expression_validator.rs | 2 +- .../src/flatten_complex_types.rs | 6 + zokrates_analysis/src/panic_extractor.rs | 19 +++ zokrates_analysis/src/propagation.rs | 97 ++++++++++++++- zokrates_analysis/src/zir_propagation.rs | 112 +++++++++++++++++- zokrates_ast/src/common/operators.rs | 7 ++ zokrates_ast/src/ir/check.rs | 6 +- zokrates_ast/src/ir/serialize.rs | 4 +- zokrates_ast/src/typed/folder.rs | 8 ++ zokrates_ast/src/typed/integer.rs | 13 ++ zokrates_ast/src/typed/mod.rs | 22 ++++ zokrates_ast/src/typed/result_folder.rs | 8 ++ zokrates_ast/src/untyped/from_ast.rs | 4 + zokrates_ast/src/untyped/mod.rs | 2 + zokrates_ast/src/zir/folder.rs | 8 ++ zokrates_ast/src/zir/mod.rs | 20 ++++ zokrates_ast/src/zir/result_folder.rs | 12 ++ zokrates_codegen/src/lib.rs | 74 ++++++++++++ zokrates_core/src/semantics.rs | 38 ++++++ .../tests/tests/assembly/idiv.json | 46 +++++++ .../tests/tests/assembly/idiv.zok | 11 ++ zokrates_core_test/tests/tests/idiv.json | 70 +++++++++++ zokrates_core_test/tests/tests/idiv.zok | 3 + .../tests/tests/panics/deep_branch.zok | 16 +-- .../tests/tests/panics/panic_isolation.zok | 4 +- zokrates_interpreter/src/lib.rs | 1 - zokrates_parser/src/zokrates.pest | 7 +- zokrates_pest_ast/src/lib.rs | 3 + .../stdlib/hashes/blake2/blake2s_p.zok | 6 +- .../stdlib/hashes/sha256/1024bitPadded.zok | 4 +- .../stdlib/hashes/sha256/256bitPadded.zok | 2 +- .../stdlib/utils/pack/bool/unpack.zok | 4 +- 33 files changed, 602 insertions(+), 39 deletions(-) create mode 100644 zokrates_core_test/tests/tests/assembly/idiv.json create mode 100644 zokrates_core_test/tests/tests/assembly/idiv.zok create mode 100644 zokrates_core_test/tests/tests/idiv.json create mode 100644 zokrates_core_test/tests/tests/idiv.zok diff --git a/Cargo.toml b/Cargo.toml index 81d2c241e..d866d5e73 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -25,4 +25,4 @@ members = [ ] [profile.dev] -opt-level = 1 \ No newline at end of file +# opt-level = 1 \ No newline at end of file diff --git a/zokrates_analysis/src/expression_validator.rs b/zokrates_analysis/src/expression_validator.rs index 9dcd63413..d735d7d78 100644 --- a/zokrates_analysis/src/expression_validator.rs +++ b/zokrates_analysis/src/expression_validator.rs @@ -44,7 +44,7 @@ impl<'ast, T: Field> ResultFolder<'ast, T> for ExpressionValidator { | FieldElementExpression::Xor(_) | FieldElementExpression::LeftShift(_) | FieldElementExpression::RightShift(_) => Err(Error(format!( - "Found non-constant bitwise operation in field element expression `{}`", + "Field element expression `{}` must be a constant expression", e ))), FieldElementExpression::Pow(e) => { diff --git a/zokrates_analysis/src/flatten_complex_types.rs b/zokrates_analysis/src/flatten_complex_types.rs index 3aa597cba..b81ce0814 100644 --- a/zokrates_analysis/src/flatten_complex_types.rs +++ b/zokrates_analysis/src/flatten_complex_types.rs @@ -1101,6 +1101,12 @@ fn fold_field_expression<'ast, T: Field>( typed::FieldElementExpression::Div(e) => { zir::FieldElementExpression::Div(f.fold_binary_expression(statements_buffer, e)) } + typed::FieldElementExpression::IDiv(e) => { + zir::FieldElementExpression::IDiv(f.fold_binary_expression(statements_buffer, e)) + } + typed::FieldElementExpression::Rem(e) => { + zir::FieldElementExpression::Rem(f.fold_binary_expression(statements_buffer, e)) + } typed::FieldElementExpression::Pow(e) => { zir::FieldElementExpression::Pow(f.fold_binary_expression(statements_buffer, e)) } diff --git a/zokrates_analysis/src/panic_extractor.rs b/zokrates_analysis/src/panic_extractor.rs index dd2628cd5..db157af18 100644 --- a/zokrates_analysis/src/panic_extractor.rs +++ b/zokrates_analysis/src/panic_extractor.rs @@ -89,6 +89,25 @@ impl<'ast, T: Field> Folder<'ast, T> for PanicExtractor<'ast, T> { ); FieldElementExpression::div(n, d) } + FieldElementExpression::IDiv(e) => { + let n = self.fold_field_expression(*e.left); + let d = self.fold_field_expression(*e.right); + self.panic_buffer.push( + ZirStatement::assertion( + BooleanExpression::not( + BooleanExpression::field_eq( + d.clone().span(span), + FieldElementExpression::value(T::zero()).span(span), + ) + .span(span), + ) + .span(span), + RuntimeError::DivisionByZero, + ) + .span(span), + ); + FieldElementExpression::idiv(n, d) + } e => fold_field_expression_cases(self, e), } } diff --git a/zokrates_analysis/src/propagation.rs b/zokrates_analysis/src/propagation.rs index 03c98c38b..5e7d09d20 100644 --- a/zokrates_analysis/src/propagation.rs +++ b/zokrates_analysis/src/propagation.rs @@ -42,14 +42,12 @@ impl fmt::Display for Error { Error::Type(s) => write!(f, "{}", s), Error::AssertionFailed(err) => write!(f, "Assertion failed ({})", err), Error::InvalidValue(s) => write!(f, "{}", s), - Error::OutOfBounds(index, size) => write!( - f, - "Out of bounds index ({} >= {}) found during static analysis", - index, size - ), + Error::OutOfBounds(index, size) => { + write!(f, "Out of bounds index ({} >= {})", index, size) + } Error::VariableLength(message) => write!(f, "{}", message), Error::DivisionByZero => { - write!(f, "Division by zero detected during static analysis",) + write!(f, "Division by zero detected",) } } } @@ -856,6 +854,22 @@ impl<'ast, T: Field> ResultFolder<'ast, T> for Propagator<'ast, T> { Ok(UExpression::and(e1.annotate(bitwidth), e2.annotate(bitwidth)).into_inner()) } }, + UExpressionInner::Or(e) => match ( + self.fold_uint_expression(*e.left)?.into_inner(), + self.fold_uint_expression(*e.right)?.into_inner(), + ) { + (UExpressionInner::Value(v1), UExpressionInner::Value(v2)) => { + Ok(UExpression::value(v1.value | v2.value)) + } + (UExpressionInner::Value(v), e) | (e, UExpressionInner::Value(v)) + if v.value == 0 => + { + Ok(e) + } + (e1, e2) => { + Ok(UExpression::or(e1.annotate(bitwidth), e2.annotate(bitwidth)).into_inner()) + } + }, UExpressionInner::Not(e) => { let e = self.fold_uint_expression(*e.inner)?.into_inner(); match e { @@ -939,6 +953,35 @@ impl<'ast, T: Field> ResultFolder<'ast, T> for Propagator<'ast, T> { (e1, e2) => Ok(e1 / e2), } } + FieldElementExpression::IDiv(e) => { + let left = self.fold_field_expression(*e.left)?; + let right = self.fold_field_expression(*e.right)?; + + Ok(match (left, right) { + (FieldElementExpression::Value(n1), FieldElementExpression::Value(n2)) => { + FieldElementExpression::value( + T::try_from(n1.value.to_biguint().div(n2.value.to_biguint())).unwrap(), + ) + } + (e1, e2) => FieldElementExpression::idiv(e1, e2), + }) + } + FieldElementExpression::Rem(e) => { + let left = self.fold_field_expression(*e.left)?; + let right = self.fold_field_expression(*e.right)?; + + Ok(match (left, right) { + (_, FieldElementExpression::Value(n)) if n.value == T::from(1) => { + FieldElementExpression::value(T::zero()) + } + (FieldElementExpression::Value(n1), FieldElementExpression::Value(n2)) => { + FieldElementExpression::value( + T::try_from(n1.value.to_biguint().rem(n2.value.to_biguint())).unwrap(), + ) + } + (e1, e2) => e1 % e2, + }) + } FieldElementExpression::Neg(e) => match self.fold_field_expression(*e.inner)? { FieldElementExpression::Value(n) => { Ok(FieldElementExpression::value(T::zero() - n.value)) @@ -1606,6 +1649,48 @@ mod tests { ); } + #[test] + fn idiv() { + let e = FieldElementExpression::idiv( + FieldElementExpression::value(Bn128Field::from(7)), + FieldElementExpression::value(Bn128Field::from(2)), + ); + + assert_eq!( + Propagator::default().fold_field_expression(e), + Ok(FieldElementExpression::value(Bn128Field::from(3))) + ); + } + + #[test] + fn rem() { + let mut propagator = Propagator::default(); + + assert_eq!( + propagator.fold_field_expression(FieldElementExpression::rem( + FieldElementExpression::value(Bn128Field::from(5)), + FieldElementExpression::value(Bn128Field::from(2)), + )), + Ok(FieldElementExpression::value(Bn128Field::from(1))) + ); + + assert_eq!( + propagator.fold_field_expression(FieldElementExpression::rem( + FieldElementExpression::value(Bn128Field::from(2)), + FieldElementExpression::value(Bn128Field::from(5)), + )), + Ok(FieldElementExpression::value(Bn128Field::from(2))) + ); + + assert_eq!( + propagator.fold_field_expression(FieldElementExpression::rem( + FieldElementExpression::identifier("a".into()), + FieldElementExpression::value(Bn128Field::from(1)), + )), + Ok(FieldElementExpression::value(Bn128Field::from(0))) + ); + } + #[test] fn pow() { let e = FieldElementExpression::pow( diff --git a/zokrates_analysis/src/zir_propagation.rs b/zokrates_analysis/src/zir_propagation.rs index d826099d5..5be11bd5a 100644 --- a/zokrates_analysis/src/zir_propagation.rs +++ b/zokrates_analysis/src/zir_propagation.rs @@ -30,13 +30,11 @@ pub enum Error { impl fmt::Display for Error { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { match self { - Error::OutOfBounds(index, size) => write!( - f, - "Out of bounds index ({} >= {}) found in zir during static analysis", - index, size - ), + Error::OutOfBounds(index, size) => { + write!(f, "Out of bounds index ({} >= {})", index, size) + } Error::DivisionByZero => { - write!(f, "Division by zero detected in zir during static analysis",) + write!(f, "Division by zero detected",) } Error::AssertionFailed(err) => write!(f, "Assertion failed ({})", err), } @@ -343,6 +341,42 @@ impl<'ast, T: Field> ResultFolder<'ast, T> for ZirPropagator<'ast, T> { (e1, e2) => Ok(FieldElementExpression::div(e1, e2).span(e.span)), } } + FieldElementExpression::IDiv(e) => { + let left = self.fold_field_expression(*e.left)?; + let right = self.fold_field_expression(*e.right)?; + + match (left, right) { + (_, FieldElementExpression::Value(n)) if n.value == T::from(0) => { + Err(Error::DivisionByZero) + } + (e, FieldElementExpression::Value(n)) if n.value == T::from(1) => Ok(e), + (FieldElementExpression::Value(n1), FieldElementExpression::Value(n2)) => { + Ok(FieldElementExpression::value( + T::try_from(n1.value.to_biguint().div(n2.value.to_biguint())).unwrap(), + )) + } + (e1, e2) => Ok(FieldElementExpression::idiv(e1, e2).span(e.span)), + } + } + FieldElementExpression::Rem(e) => { + let left = self.fold_field_expression(*e.left)?; + let right = self.fold_field_expression(*e.right)?; + + match (left, right) { + (_, FieldElementExpression::Value(n)) if n.value == T::from(0) => { + Err(Error::DivisionByZero) + } + (_, FieldElementExpression::Value(n)) if n.value == T::from(1) => { + Ok(FieldElementExpression::value(T::zero())) + } + (FieldElementExpression::Value(n1), FieldElementExpression::Value(n2)) => { + Ok(FieldElementExpression::value( + T::try_from(n1.value.to_biguint().rem(n2.value.to_biguint())).unwrap(), + )) + } + (e1, e2) => Ok(FieldElementExpression::rem(e1, e2).span(e.span)), + } + } FieldElementExpression::Pow(e) => { let exponent = self.fold_uint_expression(*e.right)?; match (self.fold_field_expression(*e.left)?, exponent.into_inner()) { @@ -1099,6 +1133,72 @@ mod tests { ); } + #[test] + fn idiv() { + let mut propagator = ZirPropagator::default(); + + assert_eq!( + propagator.fold_field_expression(FieldElementExpression::idiv( + FieldElementExpression::value(Bn128Field::from(7)), + FieldElementExpression::value(Bn128Field::from(2)), + )), + Ok(FieldElementExpression::value(Bn128Field::from(3))) + ); + + assert_eq!( + propagator.fold_field_expression(FieldElementExpression::idiv( + FieldElementExpression::identifier("a".into()), + FieldElementExpression::value(Bn128Field::from(1)), + )), + Ok(FieldElementExpression::identifier("a".into())) + ); + + assert_eq!( + propagator.fold_field_expression(FieldElementExpression::idiv( + FieldElementExpression::identifier("a".into()), + FieldElementExpression::value(Bn128Field::from(0)), + )), + Err(Error::DivisionByZero) + ); + } + + #[test] + fn rem() { + let mut propagator = ZirPropagator::default(); + + assert_eq!( + propagator.fold_field_expression(FieldElementExpression::rem( + FieldElementExpression::value(Bn128Field::from(5)), + FieldElementExpression::value(Bn128Field::from(2)), + )), + Ok(FieldElementExpression::value(Bn128Field::from(1))) + ); + + assert_eq!( + propagator.fold_field_expression(FieldElementExpression::rem( + FieldElementExpression::value(Bn128Field::from(2)), + FieldElementExpression::value(Bn128Field::from(5)), + )), + Ok(FieldElementExpression::value(Bn128Field::from(2))) + ); + + assert_eq!( + propagator.fold_field_expression(FieldElementExpression::rem( + FieldElementExpression::identifier("a".into()), + FieldElementExpression::value(Bn128Field::from(1)), + )), + Ok(FieldElementExpression::value(Bn128Field::from(0))) + ); + + assert_eq!( + propagator.fold_field_expression(FieldElementExpression::div( + FieldElementExpression::identifier("a".into()), + FieldElementExpression::value(Bn128Field::from(0)), + )), + Err(Error::DivisionByZero) + ); + } + #[test] fn pow() { let mut propagator = ZirPropagator::::default(); diff --git a/zokrates_ast/src/common/operators.rs b/zokrates_ast/src/common/operators.rs index 18a26cec2..268959762 100644 --- a/zokrates_ast/src/common/operators.rs +++ b/zokrates_ast/src/common/operators.rs @@ -37,6 +37,13 @@ impl OperatorStr for OpDiv { const STR: &'static str = "/"; } +#[derive(Clone, PartialEq, Debug, Hash, Eq, PartialOrd, Ord)] +pub struct OpIDiv; + +impl OperatorStr for OpIDiv { + const STR: &'static str = "\\"; +} + #[derive(Clone, PartialEq, Debug, Hash, Eq, PartialOrd, Ord)] pub struct OpRem; diff --git a/zokrates_ast/src/ir/check.rs b/zokrates_ast/src/ir/check.rs index e4c1652ae..d49439fde 100644 --- a/zokrates_ast/src/ir/check.rs +++ b/zokrates_ast/src/ir/check.rs @@ -4,6 +4,7 @@ use crate::ir::Parameter; use crate::ir::ProgIterator; use crate::ir::Statement; use crate::ir::Variable; +use crate::Solver; use std::collections::HashSet; use zokrates_field::Field; @@ -46,7 +47,10 @@ impl<'ast, T: Field> Folder<'ast, T> for UnconstrainedVariableDetector { &mut self, d: DirectiveStatement<'ast, T>, ) -> Vec> { - self.variables.extend(d.outputs.iter()); + match d.solver { + Solver::Zir(_) => {} // we do not check variables introduced by assembly + _ => self.variables.extend(d.outputs.iter()), // this is not necessary, but we keep it as a sanity check + }; vec![Statement::Directive(d)] } } diff --git a/zokrates_ast/src/ir/serialize.rs b/zokrates_ast/src/ir/serialize.rs index 4e5ff7a23..3d77aea75 100644 --- a/zokrates_ast/src/ir/serialize.rs +++ b/zokrates_ast/src/ir/serialize.rs @@ -222,10 +222,10 @@ impl<'ast, T: Field, I: IntoIterator>> ProgIterator<'a if matches!(s, Statement::Constraint(..)) { count += 1; } - let s: Vec> = solver_indexer + let s: Vec> = unconstrained_variable_detector .fold_statement(s) .into_iter() - .flat_map(|s| unconstrained_variable_detector.fold_statement(s)) + .flat_map(|s| solver_indexer.fold_statement(s)) .collect(); for s in s { serde_cbor::to_writer(&mut w, &s)?; diff --git a/zokrates_ast/src/typed/folder.rs b/zokrates_ast/src/typed/folder.rs index 424109bf3..a5af5e1ac 100644 --- a/zokrates_ast/src/typed/folder.rs +++ b/zokrates_ast/src/typed/folder.rs @@ -1073,6 +1073,14 @@ pub fn fold_field_expression_cases<'ast, T: Field, F: Folder<'ast, T>>( BinaryOrExpression::Binary(e) => Div(e), BinaryOrExpression::Expression(u) => u, }, + IDiv(e) => match f.fold_binary_expression(&Type::FieldElement, e) { + BinaryOrExpression::Binary(e) => IDiv(e), + BinaryOrExpression::Expression(u) => u, + }, + Rem(e) => match f.fold_binary_expression(&Type::FieldElement, e) { + BinaryOrExpression::Binary(e) => Rem(e), + BinaryOrExpression::Expression(u) => u, + }, Pow(e) => match f.fold_binary_expression(&Type::FieldElement, e) { BinaryOrExpression::Binary(e) => Pow(e), BinaryOrExpression::Expression(u) => u, diff --git a/zokrates_ast/src/typed/integer.rs b/zokrates_ast/src/typed/integer.rs index b2d1f0371..96a198cc5 100644 --- a/zokrates_ast/src/typed/integer.rs +++ b/zokrates_ast/src/typed/integer.rs @@ -317,6 +317,14 @@ pub enum IntExpression<'ast, T> { IntExpression<'ast, T>, >, ), + IDiv( + BinaryExpression< + OpIDiv, + IntExpression<'ast, T>, + IntExpression<'ast, T>, + IntExpression<'ast, T>, + >, + ), Rem( BinaryExpression< OpRem, @@ -434,6 +442,10 @@ impl<'ast, T> Neg for IntExpression<'ast, T> { } impl<'ast, T> IntExpression<'ast, T> { + pub fn idiv(self, other: Self) -> Self { + IntExpression::IDiv(BinaryExpression::new(self, other)) + } + pub fn pow(self, other: Self) -> Self { IntExpression::Pow(BinaryExpression::new(self, other)) } @@ -470,6 +482,7 @@ impl<'ast, T: fmt::Display> fmt::Display for IntExpression<'ast, T> { IntExpression::Pos(ref e) => write!(f, "{}", e), IntExpression::Neg(ref e) => write!(f, "{}", e), IntExpression::Div(ref e) => write!(f, "{}", e), + IntExpression::IDiv(ref e) => write!(f, "{}", e), IntExpression::Rem(ref e) => write!(f, "{}", e), IntExpression::Pow(ref e) => write!(f, "{}", e), IntExpression::Select(ref select) => write!(f, "{}", select), diff --git a/zokrates_ast/src/typed/mod.rs b/zokrates_ast/src/typed/mod.rs index 11786660c..8d84ee242 100644 --- a/zokrates_ast/src/typed/mod.rs +++ b/zokrates_ast/src/typed/mod.rs @@ -1376,6 +1376,8 @@ pub enum FieldElementExpression<'ast, T> { Sub(BinaryExpression), Mult(BinaryExpression), Div(BinaryExpression), + IDiv(BinaryExpression), + Rem(BinaryExpression), Pow(BinaryExpression, Self>), And(BinaryExpression), Or(BinaryExpression), @@ -1517,7 +1519,19 @@ impl<'ast, T> std::ops::Neg for FieldElementExpression<'ast, T> { } } +impl<'ast, T> std::ops::Rem for FieldElementExpression<'ast, T> { + type Output = Self; + + fn rem(self, other: Self) -> Self::Output { + FieldElementExpression::Rem(BinaryExpression::new(self, other)) + } +} + impl<'ast, T: Field> FieldElementExpression<'ast, T> { + pub fn idiv(self, other: Self) -> Self { + FieldElementExpression::IDiv(BinaryExpression::new(self, other)) + } + pub fn pow(self, other: UExpression<'ast, T>) -> Self { FieldElementExpression::Pow(BinaryExpression::new(self, other)) } @@ -2104,6 +2118,8 @@ impl<'ast, T: fmt::Display> fmt::Display for FieldElementExpression<'ast, T> { FieldElementExpression::Sub(ref e) => write!(f, "{}", e), FieldElementExpression::Mult(ref e) => write!(f, "{}", e), FieldElementExpression::Div(ref e) => write!(f, "{}", e), + FieldElementExpression::IDiv(ref e) => write!(f, "{}", e), + FieldElementExpression::Rem(ref e) => write!(f, "{}", e), FieldElementExpression::Pow(ref e) => write!(f, "{}", e), FieldElementExpression::Neg(ref e) => write!(f, "{}", e), FieldElementExpression::Pos(ref e) => write!(f, "{}", e), @@ -2270,6 +2286,8 @@ impl<'ast, T> WithSpan for FieldElementExpression<'ast, T> { Sub(e) => Sub(e.span(span)), Pow(e) => Pow(e.span(span)), Div(e) => Div(e.span(span)), + IDiv(e) => IDiv(e.span(span)), + Rem(e) => Rem(e.span(span)), Pos(e) => Pos(e.span(span)), Neg(e) => Neg(e.span(span)), And(e) => And(e.span(span)), @@ -2295,6 +2313,8 @@ impl<'ast, T> WithSpan for FieldElementExpression<'ast, T> { Sub(e) => e.get_span(), Mult(e) => e.get_span(), Div(e) => e.get_span(), + IDiv(e) => e.get_span(), + Rem(e) => e.get_span(), Pow(e) => e.get_span(), Neg(e) => e.get_span(), Pos(e) => e.get_span(), @@ -2529,6 +2549,7 @@ impl<'ast, T> WithSpan for IntExpression<'ast, T> { Sub(e) => Sub(e.span(span)), Mult(e) => Mult(e.span(span)), Div(e) => Div(e.span(span)), + IDiv(e) => IDiv(e.span(span)), Rem(e) => Rem(e.span(span)), Pow(e) => Pow(e.span(span)), Xor(e) => Xor(e.span(span)), @@ -2552,6 +2573,7 @@ impl<'ast, T> WithSpan for IntExpression<'ast, T> { Sub(e) => e.get_span(), Mult(e) => e.get_span(), Div(e) => e.get_span(), + IDiv(e) => e.get_span(), Rem(e) => e.get_span(), Pow(e) => e.get_span(), Xor(e) => e.get_span(), diff --git a/zokrates_ast/src/typed/result_folder.rs b/zokrates_ast/src/typed/result_folder.rs index d8541add0..dc3d38aff 100644 --- a/zokrates_ast/src/typed/result_folder.rs +++ b/zokrates_ast/src/typed/result_folder.rs @@ -1162,6 +1162,14 @@ pub fn fold_field_expression_cases<'ast, T: Field, F: ResultFolder<'ast, T>>( BinaryOrExpression::Binary(e) => Div(e), BinaryOrExpression::Expression(u) => u, }, + IDiv(e) => match f.fold_binary_expression(&Type::FieldElement, e)? { + BinaryOrExpression::Binary(e) => IDiv(e), + BinaryOrExpression::Expression(u) => u, + }, + Rem(e) => match f.fold_binary_expression(&Type::FieldElement, e)? { + BinaryOrExpression::Binary(e) => Rem(e), + BinaryOrExpression::Expression(u) => u, + }, Pow(e) => match f.fold_binary_expression(&Type::FieldElement, e)? { BinaryOrExpression::Binary(e) => Pow(e), BinaryOrExpression::Expression(u) => u, diff --git a/zokrates_ast/src/untyped/from_ast.rs b/zokrates_ast/src/untyped/from_ast.rs index ff37ce6ba..820424c8a 100644 --- a/zokrates_ast/src/untyped/from_ast.rs +++ b/zokrates_ast/src/untyped/from_ast.rs @@ -405,6 +405,10 @@ impl<'ast> From> for untyped::ExpressionNode<'ast> Box::new(untyped::ExpressionNode::from(*expression.left)), Box::new(untyped::ExpressionNode::from(*expression.right)), ), + pest::BinaryOperator::IDiv => untyped::Expression::IDiv( + Box::new(untyped::ExpressionNode::from(*expression.left)), + Box::new(untyped::ExpressionNode::from(*expression.right)), + ), pest::BinaryOperator::Rem => untyped::Expression::Rem( Box::new(untyped::ExpressionNode::from(*expression.left)), Box::new(untyped::ExpressionNode::from(*expression.right)), diff --git a/zokrates_ast/src/untyped/mod.rs b/zokrates_ast/src/untyped/mod.rs index c0f77ea64..26541a90a 100644 --- a/zokrates_ast/src/untyped/mod.rs +++ b/zokrates_ast/src/untyped/mod.rs @@ -610,6 +610,7 @@ pub enum Expression<'ast> { Sub(Box>, Box>), Mult(Box>, Box>), Div(Box>, Box>), + IDiv(Box>, Box>), Rem(Box>, Box>), Pow(Box>, Box>), Neg(Box>), @@ -658,6 +659,7 @@ impl<'ast> fmt::Display for Expression<'ast> { Expression::Sub(ref lhs, ref rhs) => write!(f, "({} - {})", lhs, rhs), Expression::Mult(ref lhs, ref rhs) => write!(f, "({} * {})", lhs, rhs), Expression::Div(ref lhs, ref rhs) => write!(f, "({} / {})", lhs, rhs), + Expression::IDiv(ref lhs, ref rhs) => write!(f, "({} \\ {})", lhs, rhs), Expression::Rem(ref lhs, ref rhs) => write!(f, "({} % {})", lhs, rhs), Expression::Pow(ref lhs, ref rhs) => write!(f, "({}**{})", lhs, rhs), Expression::Neg(ref e) => write!(f, "(-{})", e), diff --git a/zokrates_ast/src/zir/folder.rs b/zokrates_ast/src/zir/folder.rs index b536ccc78..3bd723251 100644 --- a/zokrates_ast/src/zir/folder.rs +++ b/zokrates_ast/src/zir/folder.rs @@ -464,6 +464,14 @@ pub fn fold_field_expression_cases<'ast, T: Field, F: Folder<'ast, T>>( BinaryOrExpression::Binary(e) => FieldElementExpression::Div(e), BinaryOrExpression::Expression(e) => e, }, + FieldElementExpression::IDiv(e) => match f.fold_binary_expression(&Type::FieldElement, e) { + BinaryOrExpression::Binary(e) => FieldElementExpression::IDiv(e), + BinaryOrExpression::Expression(e) => e, + }, + FieldElementExpression::Rem(e) => match f.fold_binary_expression(&Type::FieldElement, e) { + BinaryOrExpression::Binary(e) => FieldElementExpression::Rem(e), + BinaryOrExpression::Expression(e) => e, + }, FieldElementExpression::Pow(e) => match f.fold_binary_expression(&Type::FieldElement, e) { BinaryOrExpression::Binary(e) => FieldElementExpression::Pow(e), BinaryOrExpression::Expression(e) => e, diff --git a/zokrates_ast/src/zir/mod.rs b/zokrates_ast/src/zir/mod.rs index 62025adf0..e3b616925 100644 --- a/zokrates_ast/src/zir/mod.rs +++ b/zokrates_ast/src/zir/mod.rs @@ -716,6 +716,8 @@ pub enum FieldElementExpression<'ast, T> { Sub(BinaryExpression), Mult(BinaryExpression), Div(BinaryExpression), + IDiv(BinaryExpression), + Rem(BinaryExpression), Pow(BinaryExpression, Self>), And(BinaryExpression), Or(BinaryExpression), @@ -730,6 +732,10 @@ impl<'ast, T> FieldElementExpression<'ast, T> { Self::Value(ValueExpression::new(n)) } + pub fn idiv(self, right: Self) -> Self { + Self::IDiv(BinaryExpression::new(self, right)) + } + pub fn pow(self, right: UExpression<'ast, T>) -> Self { Self::Pow(BinaryExpression::new(self, right)) } @@ -757,6 +763,14 @@ impl<'ast, T> FieldElementExpression<'ast, T> { } } +impl<'ast, T: Field> std::ops::Rem for FieldElementExpression<'ast, T> { + type Output = Self; + + fn rem(self, other: Self) -> Self { + FieldElementExpression::Rem(BinaryExpression::new(self, other)) + } +} + impl<'ast, T: Field> std::ops::BitAnd for FieldElementExpression<'ast, T> { type Output = Self; @@ -889,6 +903,8 @@ impl<'ast, T: fmt::Display> fmt::Display for FieldElementExpression<'ast, T> { FieldElementExpression::Sub(ref e) => write!(f, "{}", e), FieldElementExpression::Mult(ref e) => write!(f, "{}", e), FieldElementExpression::Div(ref e) => write!(f, "{}", e), + FieldElementExpression::IDiv(ref e) => write!(f, "{}", e), + FieldElementExpression::Rem(ref e) => write!(f, "{}", e), FieldElementExpression::Pow(ref e) => write!(f, "{}", e), FieldElementExpression::And(ref e) => write!(f, "{}", e), FieldElementExpression::Or(ref e) => write!(f, "{}", e), @@ -1342,6 +1358,8 @@ impl<'ast, T> WithSpan for FieldElementExpression<'ast, T> { Sub(e) => Sub(e.span(span)), Mult(e) => Mult(e.span(span)), Div(e) => Div(e.span(span)), + IDiv(e) => IDiv(e.span(span)), + Rem(e) => Rem(e.span(span)), Pow(e) => Pow(e.span(span)), And(e) => And(e.span(span)), Or(e) => Or(e.span(span)), @@ -1362,6 +1380,8 @@ impl<'ast, T> WithSpan for FieldElementExpression<'ast, T> { Sub(e) => e.get_span(), Mult(e) => e.get_span(), Div(e) => e.get_span(), + IDiv(e) => e.get_span(), + Rem(e) => e.get_span(), Pow(e) => e.get_span(), And(e) => e.get_span(), Or(e) => e.get_span(), diff --git a/zokrates_ast/src/zir/result_folder.rs b/zokrates_ast/src/zir/result_folder.rs index d368d972d..c956c093e 100644 --- a/zokrates_ast/src/zir/result_folder.rs +++ b/zokrates_ast/src/zir/result_folder.rs @@ -525,6 +525,18 @@ pub fn fold_field_expression_cases<'ast, T: Field, F: ResultFolder<'ast, T>>( BinaryOrExpression::Expression(e) => e, } } + FieldElementExpression::IDiv(e) => { + match f.fold_binary_expression(&Type::FieldElement, e)? { + BinaryOrExpression::Binary(e) => FieldElementExpression::IDiv(e), + BinaryOrExpression::Expression(e) => e, + } + } + FieldElementExpression::Rem(e) => { + match f.fold_binary_expression(&Type::FieldElement, e)? { + BinaryOrExpression::Binary(e) => FieldElementExpression::Rem(e), + BinaryOrExpression::Expression(e) => e, + } + } FieldElementExpression::Pow(e) => { match f.fold_binary_expression(&Type::FieldElement, e)? { BinaryOrExpression::Binary(e) => FieldElementExpression::Pow(e), diff --git a/zokrates_codegen/src/lib.rs b/zokrates_codegen/src/lib.rs index 685c78d31..defcdc4f4 100644 --- a/zokrates_codegen/src/lib.rs +++ b/zokrates_codegen/src/lib.rs @@ -2262,6 +2262,80 @@ impl<'ast, T: Field> Flattener<'ast, T> { inverse.into() } + FieldElementExpression::IDiv(e) => { + let left_flattened = self.flatten_field_expression(statements_flattened, *e.left); + let right_flattened = self.flatten_field_expression(statements_flattened, *e.right); + let new_left: FlatExpression = { + let id = self.use_sym(); + statements_flattened.push_back(FlatStatement::definition(id, left_flattened)); + id.into() + }; + let new_right: FlatExpression = { + let id = self.use_sym(); + statements_flattened.push_back(FlatStatement::definition(id, right_flattened)); + id.into() + }; + + // q is the quotient and r is the remainder + // we simply need to constrain `a = b * q + r` and `0 <= r < b` to hold + let q = self.use_sym(); + let r = self.use_sym(); + + // # q, r = a \ b + statements_flattened.push_back(FlatStatement::directive( + vec![q, r], + Solver::EuclideanDiv, + vec![new_left.clone(), new_right.clone()], + )); + + // q * b == a - r + statements_flattened.push_back(FlatStatement::condition( + FlatExpression::sub(new_left, r.into()), + FlatExpression::mul(q.into(), new_right), + RuntimeError::Euclidean, + )); + + // todo: enforce `r < b` + + q.into() + } + FieldElementExpression::Rem(e) => { + let left_flattened = self.flatten_field_expression(statements_flattened, *e.left); + let right_flattened = self.flatten_field_expression(statements_flattened, *e.right); + let new_left: FlatExpression = { + let id = self.use_sym(); + statements_flattened.push_back(FlatStatement::definition(id, left_flattened)); + id.into() + }; + let new_right: FlatExpression = { + let id = self.use_sym(); + statements_flattened.push_back(FlatStatement::definition(id, right_flattened)); + id.into() + }; + + // q is the quotient and r is the remainder + // we simply need to constrain `a = b * q + r` and `0 <= r < b` to hold + let q = self.use_sym(); + let r = self.use_sym(); + + // # q, r = a \ b + statements_flattened.push_back(FlatStatement::directive( + vec![q, r], + Solver::EuclideanDiv, + vec![new_left.clone(), new_right.clone()], + )); + + // q * b == a - r + statements_flattened.push_back(FlatStatement::condition( + FlatExpression::sub(new_left, r.into()), + FlatExpression::mul(q.into(), new_right), + RuntimeError::Euclidean, + )); + + // todo: enforce `r < b` + + r.into() + } FieldElementExpression::Pow(e) => { match e.right.into_inner() { UExpressionInner::Value(ref exp) => { diff --git a/zokrates_core/src/semantics.rs b/zokrates_core/src/semantics.rs index b1646e11c..54e801c74 100644 --- a/zokrates_core/src/semantics.rs +++ b/zokrates_core/src/semantics.rs @@ -2625,6 +2625,38 @@ impl<'ast, T: Field> Checker<'ast, T> { }), } } + Expression::IDiv(e1, e2) => { + let e1_checked = self.check_expression(*e1, module_id, types)?; + let e2_checked = self.check_expression(*e2, module_id, types)?; + + use self::TypedExpression::*; + + let (e1_checked, e2_checked) = TypedExpression::align_without_integers( + e1_checked, e2_checked, + ) + .map_err(|(e1, e2)| ErrorInner { + span: Some(span), + message: format!("Cannot apply `\\` to {}, {}", e1.get_type(), e2.get_type()), + })?; + + match (e1_checked, e2_checked) { + (Int(e1), Int(e2)) => Ok(IntExpression::idiv(e1, e2).into()), + (FieldElement(e1), FieldElement(e2)) => Ok(FieldElementExpression::idiv(e1, e2).into()), + (Uint(e1), Uint(e2)) + if e1.get_type() == e2.get_type() => + { + Ok((e1 / e2).into()) // intentional `\` => `/` + } + (t1, t2) => Err(ErrorInner { + span: Some(span), + message: format!( + "Cannot apply `\\` to {}, {}", + t1.get_type(), + t2.get_type() + ), + }), + } + } Expression::Rem(e1, e2) => { let e1_checked = self.check_expression(*e1, module_id, types)?; let e2_checked = self.check_expression(*e2, module_id, types)?; @@ -2638,6 +2670,12 @@ impl<'ast, T: Field> Checker<'ast, T> { })?; match (e1_checked, e2_checked) { + (TypedExpression::Int(e1), TypedExpression::Int(e2)) => { + Ok((e1 % e2).into()) + } + (TypedExpression::FieldElement(e1), TypedExpression::FieldElement(e2)) => { + Ok((e1 % e2).into()) + } (TypedExpression::Uint(e1), TypedExpression::Uint(e2)) if e1.get_type() == e2.get_type() => { diff --git a/zokrates_core_test/tests/tests/assembly/idiv.json b/zokrates_core_test/tests/tests/assembly/idiv.json new file mode 100644 index 000000000..f1cbd2897 --- /dev/null +++ b/zokrates_core_test/tests/tests/assembly/idiv.json @@ -0,0 +1,46 @@ +{ + "curves": ["Bn128"], + "max_constraint_count": 261, + "tests": [ + { + "input": { + "values": ["4", "2"] + }, + "output": { + "Ok": { + "value": ["2", "0"] + } + } + }, + { + "input": { + "values": ["2", "4"] + }, + "output": { + "Ok": { + "value": ["0", "2"] + } + } + }, + { + "input": { + "values": ["5", "2"] + }, + "output": { + "Ok": { + "value": ["2", "1"] + } + } + }, + { + "input": { + "values": ["10", "7"] + }, + "output": { + "Ok": { + "value": ["1", "3"] + } + } + } + ] +} diff --git a/zokrates_core_test/tests/tests/assembly/idiv.zok b/zokrates_core_test/tests/tests/assembly/idiv.zok new file mode 100644 index 000000000..c97f3a2e1 --- /dev/null +++ b/zokrates_core_test/tests/tests/assembly/idiv.zok @@ -0,0 +1,11 @@ +def main(field a, field b) -> (field, field) { + field mut q = 0; + field mut r = 0; + asm { + q <-- a \ b; + r <-- a - q * b; + a === b * q + r; + } + assert(r < b); + return (q, r); +} \ No newline at end of file diff --git a/zokrates_core_test/tests/tests/idiv.json b/zokrates_core_test/tests/tests/idiv.json new file mode 100644 index 000000000..69c40a969 --- /dev/null +++ b/zokrates_core_test/tests/tests/idiv.json @@ -0,0 +1,70 @@ +{ + "max_constraint_count": 3, + "curves": ["Bn128", "Bls12_381", "Bls12_377", "Bw6_761"], + "tests": [ + { + "input": { + "values": ["0", "0"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "error": "Inverse" + } + } + } + }, + { + "input": { + "values": ["1", "0"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "error": "Inverse" + } + } + } + }, + { + "input": { + "values": ["0", "1"] + }, + "output": { + "Ok": { + "value": "0" + } + } + }, + { + "input": { + "values": ["2", "2"] + }, + "output": { + "Ok": { + "value": "1" + } + } + }, + { + "input": { + "values": ["4", "2"] + }, + "output": { + "Ok": { + "value": "2" + } + } + }, + { + "input": { + "values": ["5", "2"] + }, + "output": { + "Ok": { + "value": "2" + } + } + } + ] +} diff --git a/zokrates_core_test/tests/tests/idiv.zok b/zokrates_core_test/tests/tests/idiv.zok new file mode 100644 index 000000000..63b9005b4 --- /dev/null +++ b/zokrates_core_test/tests/tests/idiv.zok @@ -0,0 +1,3 @@ +def main(field x, field y) -> field { + return x \ y; +} \ No newline at end of file diff --git a/zokrates_core_test/tests/tests/panics/deep_branch.zok b/zokrates_core_test/tests/tests/panics/deep_branch.zok index fca9bbe23..18735c6db 100644 --- a/zokrates_core_test/tests/tests/panics/deep_branch.zok +++ b/zokrates_core_test/tests/tests/panics/deep_branch.zok @@ -4,13 +4,13 @@ def check(bool[N] conditions, bool[N] expected) -> bool[3] { } def main(bool[3] conditions) -> bool[3] { - return conditions[0] ? \ - conditions[1] ? \ - conditions[2] ? check(conditions, [true, true, true]) : check(conditions, [true, true, false]) : \ - conditions[2] ? check(conditions, [true, false, true]) : \ - check(conditions, [true, false, false]) : \ - conditions[1] ? \ - conditions[2] ? check(conditions, [false, true, true]) : check(conditions, [false, true, false]) : \ - conditions[2] ? check(conditions, [false, false, true]) : \ + return conditions[0] ? + conditions[1] ? + conditions[2] ? check(conditions, [true, true, true]) : check(conditions, [true, true, false]) : + conditions[2] ? check(conditions, [true, false, true]) : + check(conditions, [true, false, false]) : + conditions[1] ? + conditions[2] ? check(conditions, [false, true, true]) : check(conditions, [false, true, false]) : + conditions[2] ? check(conditions, [false, false, true]) : check(conditions, [false, false, false]); } \ No newline at end of file diff --git a/zokrates_core_test/tests/tests/panics/panic_isolation.zok b/zokrates_core_test/tests/tests/panics/panic_isolation.zok index 276bcc58b..f5a9348d5 100644 --- a/zokrates_core_test/tests/tests/panics/panic_isolation.zok +++ b/zokrates_core_test/tests/tests/panics/panic_isolation.zok @@ -32,7 +32,7 @@ def main(bool condition, field[2] a, field x) -> (bool, field[2], field) { // first branch asserts that `condition` is true, second branch asserts that `condition` is false. This should never throw. // first branch asserts that all elements in `a` are 1, 2 in the second branch. This should throw only if `a` is neither ones or zeroes // first branch asserts that `x` is zero and returns it, second branch asserts that `x` isn't 0 and returns its inverse (which internally generates a failing assert if x is 0). This should never throw - return (condition ? yes(condition) : no(condition), \ - condition ? ones(a) : twos(a), \ + return (condition ? yes(condition) : no(condition), + condition ? ones(a) : twos(a), x == 0 ? zero(x) : inverse(x)); } \ No newline at end of file diff --git a/zokrates_interpreter/src/lib.rs b/zokrates_interpreter/src/lib.rs index 9e9bff770..af974ef57 100644 --- a/zokrates_interpreter/src/lib.rs +++ b/zokrates_interpreter/src/lib.rs @@ -293,7 +293,6 @@ impl Interpreter { let c = inputs[2]; vec![a * (b - c) + c] } - Solver::Div => vec![inputs[0].checked_div(&inputs[1]).unwrap_or_else(T::one)], Solver::EuclideanDiv => { use num::CheckedDiv; diff --git a/zokrates_parser/src/zokrates.pest b/zokrates_parser/src/zokrates.pest index af4998e09..b3b5d8820 100644 --- a/zokrates_parser/src/zokrates.pest +++ b/zokrates_parser/src/zokrates.pest @@ -171,6 +171,7 @@ op_add = {"+"} op_sub = {"-"} op_mul = {"*"} op_div = {"/"} +op_idiv = @{"\\"} op_rem = {"%"} op_pow = @{"**"} op_not = {"!"} @@ -181,15 +182,15 @@ op_right_shift = @{">>"} op_ternary = {"?" ~ expression ~ ":"} // `op_pow` is *not* in `op_binary` because its precedence is handled in this parser rather than down the line in precedence climbing -op_binary = _ { op_or | op_and | op_bit_xor | op_bit_and | op_bit_or | op_left_shift | op_right_shift | op_equal | op_not_equal | op_lte | op_lt | op_gte | op_gt | op_add | op_sub | op_mul | op_div | op_rem | op_ternary } +op_binary = _ { op_or | op_and | op_bit_xor | op_bit_and | op_bit_or | op_left_shift | op_right_shift | op_equal | op_not_equal | op_lte | op_lt | op_gte | op_gt | op_add | op_sub | op_mul | op_div | op_idiv | op_rem | op_ternary } op_unary = { op_pos | op_neg | op_not } -WHITESPACE = _{ " " | "\t" | "\\" | COMMENT | NEWLINE } +WHITESPACE = _{ " " | "\t" | COMMENT | NEWLINE } COMMENT = _{ ("/*" ~ (!"*/" ~ ANY)* ~ "*/") | ("//" ~ (!NEWLINE ~ ANY)*) } // the ordering of reserved keywords matters: if "as" is before "assert", then "assert" gets parsed as (as)(sert) and incorrectly // accepted keyword = @{ - "log"|"assert"|"as"|"bool"|"const"|"def"|"else"|"false"|"field"|"for"|"if"|"import"|"from"| + "log"|"assert"|"as"|"asm"|"bool"|"const"|"def"|"else"|"false"|"field"|"for"|"if"|"import"|"from"| "in"|"mut"|"private"|"public"|"return"|"struct"|"true"|"type"|"u8"|"u16"|"u32"|"u64" } diff --git a/zokrates_pest_ast/src/lib.rs b/zokrates_pest_ast/src/lib.rs index 2fca23ac2..5aed66a70 100644 --- a/zokrates_pest_ast/src/lib.rs +++ b/zokrates_pest_ast/src/lib.rs @@ -60,6 +60,7 @@ mod ast { Operator::new(Rule::op_add, Assoc::Left) | Operator::new(Rule::op_sub, Assoc::Left), Operator::new(Rule::op_mul, Assoc::Left) | Operator::new(Rule::op_div, Assoc::Left) + | Operator::new(Rule::op_idiv, Assoc::Left) | Operator::new(Rule::op_rem, Assoc::Left), ]) } @@ -81,6 +82,7 @@ mod ast { Rule::op_sub => Expression::binary(BinaryOperator::Sub, lhs, rhs, span), Rule::op_mul => Expression::binary(BinaryOperator::Mul, lhs, rhs, span), Rule::op_div => Expression::binary(BinaryOperator::Div, lhs, rhs, span), + Rule::op_idiv => Expression::binary(BinaryOperator::IDiv, lhs, rhs, span), Rule::op_rem => Expression::binary(BinaryOperator::Rem, lhs, rhs, span), Rule::op_equal => Expression::binary(BinaryOperator::Eq, lhs, rhs, span), Rule::op_not_equal => Expression::binary(BinaryOperator::NotEq, lhs, rhs, span), @@ -498,6 +500,7 @@ mod ast { Sub, Mul, Div, + IDiv, Rem, Eq, NotEq, diff --git a/zokrates_stdlib/stdlib/hashes/blake2/blake2s_p.zok b/zokrates_stdlib/stdlib/hashes/blake2/blake2s_p.zok index 628566aa6..1b0689417 100644 --- a/zokrates_stdlib/stdlib/hashes/blake2/blake2s_p.zok +++ b/zokrates_stdlib/stdlib/hashes/blake2/blake2s_p.zok @@ -30,9 +30,9 @@ def rotr32(u32 x) -> u32 { // change endianness def swap_u32(u32 val) -> u32 { - return (val << 24) | \ - ((val << 8) & 0x00ff0000) | \ - ((val >> 8) & 0x0000ff00) | \ + return (val << 24) | + ((val << 8) & 0x00ff0000) | + ((val >> 8) & 0x0000ff00) | ((val >> 24) & 0x000000ff); } diff --git a/zokrates_stdlib/stdlib/hashes/sha256/1024bitPadded.zok b/zokrates_stdlib/stdlib/hashes/sha256/1024bitPadded.zok index b2e50eb0d..5d8b79541 100644 --- a/zokrates_stdlib/stdlib/hashes/sha256/1024bitPadded.zok +++ b/zokrates_stdlib/stdlib/hashes/sha256/1024bitPadded.zok @@ -7,7 +7,7 @@ def main(u32[8] a, u32[8] b, u32[8] c, u32[8] d) -> u32[8] { // Hash is computed on the full 1024bit block size // padding does not fit in the first two blocks // add dummy block (single "1" followed by "0" + total length) - u32[8] dummyblock1 = [ \ + u32[8] dummyblock1 = [ 0x80000000, 0x00000000, 0x00000000, @@ -18,7 +18,7 @@ def main(u32[8] a, u32[8] b, u32[8] c, u32[8] d) -> u32[8] { 0x00000000 ]; - u32[8] dummyblock2 = [ \ + u32[8] dummyblock2 = [ 0x00000000, 0x00000000, 0x00000000, diff --git a/zokrates_stdlib/stdlib/hashes/sha256/256bitPadded.zok b/zokrates_stdlib/stdlib/hashes/sha256/256bitPadded.zok index e7fca109b..471563d23 100644 --- a/zokrates_stdlib/stdlib/hashes/sha256/256bitPadded.zok +++ b/zokrates_stdlib/stdlib/hashes/sha256/256bitPadded.zok @@ -7,7 +7,7 @@ def main(u32[8] a) -> u32[8] { // Hash is computed on 256 bits of input // padding fits in the remaining 256 bits of the first block // add dummy block (single "1" followed by "0" + total length) - u32[8] dummyblock1 = [ \ + u32[8] dummyblock1 = [ 0x80000000, 0x00000000, 0x00000000, diff --git a/zokrates_stdlib/stdlib/utils/pack/bool/unpack.zok b/zokrates_stdlib/stdlib/utils/pack/bool/unpack.zok index dbfba7b71..e810b5842 100644 --- a/zokrates_stdlib/stdlib/utils/pack/bool/unpack.zok +++ b/zokrates_stdlib/stdlib/utils/pack/bool/unpack.zok @@ -5,8 +5,8 @@ from "EMBED" import bit_array_le; // Unpack a field element as N big endian bits def main(field i) -> bool[N] { bool[N] res = unpack_unchecked(i); - assert(N >= FIELD_SIZE_IN_BITS \ - ? bit_array_le(res, [...[false; N - FIELD_SIZE_IN_BITS], ...unpack_unchecked::(-1)]) \ + assert(N >= FIELD_SIZE_IN_BITS + ? bit_array_le(res, [...[false; N - FIELD_SIZE_IN_BITS], ...unpack_unchecked::(-1)]) : true); return res; } \ No newline at end of file From 9f592dc9ef1937bb3224822a7d95a2c217056d27 Mon Sep 17 00:00:00 2001 From: dark64 Date: Tue, 26 Sep 2023 11:43:51 +0200 Subject: [PATCH 2/5] revert opt-level comment --- Cargo.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index d866d5e73..81d2c241e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -25,4 +25,4 @@ members = [ ] [profile.dev] -# opt-level = 1 \ No newline at end of file +opt-level = 1 \ No newline at end of file From 11bee6aa7d2a4f1e6e78c4688f020d6b6027904b Mon Sep 17 00:00:00 2001 From: dark64 Date: Wed, 15 Nov 2023 12:10:23 +0300 Subject: [PATCH 3/5] use existing euclidean division impl --- zokrates_codegen/src/lib.rs | 118 ++++++------------ .../tests/tests/assembly/idiv.json | 2 +- zokrates_core_test/tests/tests/idiv.json | 2 +- 3 files changed, 40 insertions(+), 82 deletions(-) diff --git a/zokrates_codegen/src/lib.rs b/zokrates_codegen/src/lib.rs index bad7d16c5..cb678adef 100644 --- a/zokrates_codegen/src/lib.rs +++ b/zokrates_codegen/src/lib.rs @@ -1278,16 +1278,10 @@ impl<'ast, T: Field> Flattener<'ast, T> { fn euclidean_division( &mut self, statements_flattened: &mut FlatStatements<'ast, T>, - target_bitwidth: UBitwidth, - left: UExpression<'ast, T>, - right: UExpression<'ast, T>, + target_bitwidth: usize, + left_flattened: FlatExpression, + right_flattened: FlatExpression, ) -> (FlatExpression, FlatExpression) { - let left_flattened = self - .flatten_uint_expression(statements_flattened, left) - .get_field_unchecked(); - let right_flattened = self - .flatten_uint_expression(statements_flattened, right) - .get_field_unchecked(); let n = if left_flattened.is_linear() { left_flattened } else { @@ -1313,8 +1307,6 @@ impl<'ast, T: Field> Flattener<'ast, T> { vec![n.clone(), d.clone()], )); - let target_bitwidth = target_bitwidth.to_usize(); - // q in range let _ = self.get_bits_unchecked( &FlatUExpression::with_field(FlatExpression::from(q)), @@ -1337,7 +1329,7 @@ impl<'ast, T: Field> Flattener<'ast, T> { let _ = self.get_bits_unchecked( &FlatUExpression::with_field(FlatExpression::add( FlatExpression::sub(r.into(), d.clone()), - FlatExpression::value(T::from(2_u128.pow(target_bitwidth as u32))), + FlatExpression::value(T::from(2).pow(target_bitwidth)), )), target_bitwidth, target_bitwidth, @@ -1558,21 +1550,35 @@ impl<'ast, T: Field> Flattener<'ast, T> { FlatUExpression::with_field(FlatExpression::identifier(res)) } UExpressionInner::Div(e) => { + let left_flattened = self + .flatten_uint_expression(statements_flattened, *e.left) + .get_field_unchecked(); + let right_flattened = self + .flatten_uint_expression(statements_flattened, *e.right) + .get_field_unchecked(); + let (q, _) = self.euclidean_division( statements_flattened, - target_bitwidth, - *e.left, - *e.right, + target_bitwidth.to_usize(), + left_flattened, + right_flattened, ); FlatUExpression::with_field(q) } UExpressionInner::Rem(e) => { + let left_flattened = self + .flatten_uint_expression(statements_flattened, *e.left) + .get_field_unchecked(); + let right_flattened = self + .flatten_uint_expression(statements_flattened, *e.right) + .get_field_unchecked(); + let (_, r) = self.euclidean_division( statements_flattened, - target_bitwidth, - *e.left, - *e.right, + target_bitwidth.to_usize(), + left_flattened, + right_flattened, ); FlatUExpression::with_field(r) @@ -2196,76 +2202,28 @@ impl<'ast, T: Field> Flattener<'ast, T> { FieldElementExpression::IDiv(e) => { let left_flattened = self.flatten_field_expression(statements_flattened, *e.left); let right_flattened = self.flatten_field_expression(statements_flattened, *e.right); - let new_left: FlatExpression = { - let id = self.use_sym(); - statements_flattened.push_back(FlatStatement::definition(id, left_flattened)); - id.into() - }; - let new_right: FlatExpression = { - let id = self.use_sym(); - statements_flattened.push_back(FlatStatement::definition(id, right_flattened)); - id.into() - }; - - // q is the quotient and r is the remainder - // we simply need to constrain `a = b * q + r` and `0 <= r < b` to hold - let q = self.use_sym(); - let r = self.use_sym(); - // # q, r = a \ b - statements_flattened.push_back(FlatStatement::directive( - vec![q, r], - Solver::EuclideanDiv, - vec![new_left.clone(), new_right.clone()], - )); - - // q * b == a - r - statements_flattened.push_back(FlatStatement::condition( - FlatExpression::sub(new_left, r.into()), - FlatExpression::mul(q.into(), new_right), - RuntimeError::Euclidean, - )); - - // todo: enforce `r < b` + let (q, _) = self.euclidean_division( + statements_flattened, + T::get_required_bits() - 2, + left_flattened, + right_flattened, + ); - q.into() + q } FieldElementExpression::Rem(e) => { let left_flattened = self.flatten_field_expression(statements_flattened, *e.left); let right_flattened = self.flatten_field_expression(statements_flattened, *e.right); - let new_left: FlatExpression = { - let id = self.use_sym(); - statements_flattened.push_back(FlatStatement::definition(id, left_flattened)); - id.into() - }; - let new_right: FlatExpression = { - let id = self.use_sym(); - statements_flattened.push_back(FlatStatement::definition(id, right_flattened)); - id.into() - }; - // q is the quotient and r is the remainder - // we simply need to constrain `a = b * q + r` and `0 <= r < b` to hold - let q = self.use_sym(); - let r = self.use_sym(); - - // # q, r = a \ b - statements_flattened.push_back(FlatStatement::directive( - vec![q, r], - Solver::EuclideanDiv, - vec![new_left.clone(), new_right.clone()], - )); - - // q * b == a - r - statements_flattened.push_back(FlatStatement::condition( - FlatExpression::sub(new_left, r.into()), - FlatExpression::mul(q.into(), new_right), - RuntimeError::Euclidean, - )); - - // todo: enforce `r < b` + let (_, r) = self.euclidean_division( + statements_flattened, + T::get_required_bits() - 2, + left_flattened, + right_flattened, + ); - r.into() + r } FieldElementExpression::Pow(e) => { match e.right.into_inner() { diff --git a/zokrates_core_test/tests/tests/assembly/idiv.json b/zokrates_core_test/tests/tests/assembly/idiv.json index f1cbd2897..5ad510935 100644 --- a/zokrates_core_test/tests/tests/assembly/idiv.json +++ b/zokrates_core_test/tests/tests/assembly/idiv.json @@ -1,6 +1,6 @@ { "curves": ["Bn128"], - "max_constraint_count": 261, + "max_constraint_count": 766, "tests": [ { "input": { diff --git a/zokrates_core_test/tests/tests/idiv.json b/zokrates_core_test/tests/tests/idiv.json index 69c40a969..e4d861e12 100644 --- a/zokrates_core_test/tests/tests/idiv.json +++ b/zokrates_core_test/tests/tests/idiv.json @@ -1,5 +1,5 @@ { - "max_constraint_count": 3, + "max_constraint_count": 1131, "curves": ["Bn128", "Bls12_381", "Bls12_377", "Bw6_761"], "tests": [ { From a11c1ba0a74487267b050b37062828c68b383cab Mon Sep 17 00:00:00 2001 From: dark64 Date: Wed, 15 Nov 2023 12:23:46 +0300 Subject: [PATCH 4/5] update book, add changelog --- changelogs/unreleased/1349-dark64 | 1 + zokrates_book/src/language/operators.md | 36 +++++++++++++------------ 2 files changed, 20 insertions(+), 17 deletions(-) create mode 100644 changelogs/unreleased/1349-dark64 diff --git a/changelogs/unreleased/1349-dark64 b/changelogs/unreleased/1349-dark64 new file mode 100644 index 000000000..bd626a565 --- /dev/null +++ b/changelogs/unreleased/1349-dark64 @@ -0,0 +1 @@ +Implement field division and remainder operations using euclidean division \ No newline at end of file diff --git a/zokrates_book/src/language/operators.md b/zokrates_book/src/language/operators.md index efd27eeba..171f684d2 100644 --- a/zokrates_book/src/language/operators.md +++ b/zokrates_book/src/language/operators.md @@ -3,25 +3,27 @@ The following table lists the precedence and associativity of all operators. Operators are listed top to bottom, in ascending precedence. Operators in the same cell have the same precedence. Operators are binary, unless the syntax is provided. -| Operator | Description | `field` | `u8/u16` `u32/u64` | `bool` | Associativity | -|--------------------------------------------|------------------------------------------------------------|------------------------------|-------------------------------|-----------------------------|---------------| -| `**`
| Power | ✓[^1] |   |   | Left | -| `+x`
`-x`
`!x`
| Positive
Negative
Negation
| ✓
✓
  | ✓
✓
✓ |  
 
✓ | Right | -| `*`
`/`
`%`
| Multiplication
Division
Remainder
| ✓
✓
  | ✓
✓
✓ |  
 
  | Left | -| `+`
`-`
| Addition
Subtraction
| ✓ | ✓ |   | Left | -| `<<`
`>>`
| Left shift
Right shift
|   | ✓[^2] |   | Left | -| `&` | Bitwise AND |   | ✓ |   | Left | -| | | Bitwise OR |   | ✓ |   | Left | -| `^` | Bitwise XOR |   | ✓ |   | Left | -| `>=`
`>`
`<=`
`<` | Greater or equal
Greater
Lower or equal
Lower
| ✓[^3] | ✓ |   | Left | -| `!=`
`==`
| Not Equal
Equal
| ✓ | ✓ | ✓ | Left | -| `&&` | Boolean AND |   |   | ✓ | Left | -| || | Boolean OR |   |   | ✓ | Left | -| `c ? x : y`

`if c { x } else { y }` | Conditional expression | ✓ | ✓ | ✓ | Right | +| Operator | Description | `field` | `u8/u16` `u32/u64` | `bool` | Associativity | +|--------------------------------------------|------------------------------------------------------------|-----------------------------------|-------------------------------|-----------------------------|---------------| +| `**`
| Power | ✓[^1] |   |   | Left | +| `+x`
`-x`
`!x`
| Positive
Negative
Negation
| ✓
✓
  | ✓
✓
✓ |  
 
✓ | Right | +| `*`
`/`
`%`
| Multiplication
Division
Remainder
| ✓
✓[^2]
✓ | ✓
✓
✓ |  
 
  | Left | +| `+`
`-`
| Addition
Subtraction
| ✓ | ✓ |   | Left | +| `<<`
`>>`
| Left shift
Right shift
|   | ✓[^3] |   | Left | +| `&` | Bitwise AND |   | ✓ |   | Left | +| | | Bitwise OR |   | ✓ |   | Left | +| `^` | Bitwise XOR |   | ✓ |   | Left | +| `>=`
`>`
`<=`
`<` | Greater or equal
Greater
Lower or equal
Lower
| ✓[^4] | ✓ |   | Left | +| `!=`
`==`
| Not Equal
Equal
| ✓ | ✓ | ✓ | Left | +| `&&` | Boolean AND |   |   | ✓ | Left | +| || | Boolean OR |   |   | ✓ | Left | +| `c ? x : y`

`if c { x } else { y }` | Conditional expression | ✓ | ✓ | ✓ | Right | [^1]: The exponent must be a compile-time constant of type `u32` -[^2]: The right operand must be a compile time constant of type `u32` +[^2]: Field division is defined as multiplication by the inverse modulo `p`. Use `\` to get the quotient of the integer division. -[^3]: If neither of the operands can be determined to be a compile-time constant, then we have a restriction: for the check `a < b`, if the field prime `p` is represented on `N` bits, `|a - b|` must fit in `N - 2` bits. +[^3]: The right operand must be a compile time constant of type `u32` + +[^4]: If neither of the operands can be determined to be a compile-time constant, then we have a restriction: for the check `a < b`, if the field prime `p` is represented on `N` bits, `|a - b|` must fit in `N - 2` bits. Failing to respect this condition will lead to a runtime error. From 37e16992d8bb300781a3063814c17543b8914624 Mon Sep 17 00:00:00 2001 From: dark64 Date: Wed, 15 Nov 2023 16:16:49 +0300 Subject: [PATCH 5/5] add rem test --- zokrates_analysis/src/panic_extractor.rs | 38 ++++++++++ zokrates_core_test/tests/tests/rem.json | 70 +++++++++++++++++++ zokrates_core_test/tests/tests/rem.zok | 3 + .../tests/tests/uint/u16/rem.json | 12 ++++ .../tests/tests/uint/u32/rem.json | 12 ++++ .../tests/tests/uint/u64/rem.json | 12 ++++ .../tests/tests/uint/u8/rem.json | 12 ++++ 7 files changed, 159 insertions(+) create mode 100644 zokrates_core_test/tests/tests/rem.json create mode 100644 zokrates_core_test/tests/tests/rem.zok diff --git a/zokrates_analysis/src/panic_extractor.rs b/zokrates_analysis/src/panic_extractor.rs index db157af18..bcf31a400 100644 --- a/zokrates_analysis/src/panic_extractor.rs +++ b/zokrates_analysis/src/panic_extractor.rs @@ -108,6 +108,25 @@ impl<'ast, T: Field> Folder<'ast, T> for PanicExtractor<'ast, T> { ); FieldElementExpression::idiv(n, d) } + FieldElementExpression::Rem(e) => { + let n = self.fold_field_expression(*e.left); + let d = self.fold_field_expression(*e.right); + self.panic_buffer.push( + ZirStatement::assertion( + BooleanExpression::not( + BooleanExpression::field_eq( + d.clone().span(span), + FieldElementExpression::value(T::zero()).span(span), + ) + .span(span), + ) + .span(span), + RuntimeError::DivisionByZero, + ) + .span(span), + ); + FieldElementExpression::rem(n, d) + } e => fold_field_expression_cases(self, e), } } @@ -169,6 +188,25 @@ impl<'ast, T: Field> Folder<'ast, T> for PanicExtractor<'ast, T> { ); UExpression::div(n, d).into_inner() } + UExpressionInner::Rem(e) => { + let n = self.fold_uint_expression(*e.left); + let d = self.fold_uint_expression(*e.right); + self.panic_buffer.push( + ZirStatement::assertion( + BooleanExpression::not( + BooleanExpression::uint_eq( + d.clone().span(span), + UExpression::value(0).annotate(b).span(span), + ) + .span(span), + ) + .span(span), + RuntimeError::DivisionByZero, + ) + .span(span), + ); + UExpression::rem(n, d).into_inner() + } e => fold_uint_expression_cases(self, b, e), } } diff --git a/zokrates_core_test/tests/tests/rem.json b/zokrates_core_test/tests/tests/rem.json new file mode 100644 index 000000000..f43813da1 --- /dev/null +++ b/zokrates_core_test/tests/tests/rem.json @@ -0,0 +1,70 @@ +{ + "max_constraint_count": 1131, + "curves": ["Bn128", "Bls12_381", "Bls12_377", "Bw6_761"], + "tests": [ + { + "input": { + "values": ["0", "0"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "error": "Inverse" + } + } + } + }, + { + "input": { + "values": ["1", "0"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "error": "Inverse" + } + } + } + }, + { + "input": { + "values": ["0", "1"] + }, + "output": { + "Ok": { + "value": "0" + } + } + }, + { + "input": { + "values": ["2", "2"] + }, + "output": { + "Ok": { + "value": "0" + } + } + }, + { + "input": { + "values": ["4", "2"] + }, + "output": { + "Ok": { + "value": "0" + } + } + }, + { + "input": { + "values": ["5", "2"] + }, + "output": { + "Ok": { + "value": "1" + } + } + } + ] +} diff --git a/zokrates_core_test/tests/tests/rem.zok b/zokrates_core_test/tests/tests/rem.zok new file mode 100644 index 000000000..1d8b95e29 --- /dev/null +++ b/zokrates_core_test/tests/tests/rem.zok @@ -0,0 +1,3 @@ +def main(field x, field y) -> field { + return x % y; +} \ No newline at end of file diff --git a/zokrates_core_test/tests/tests/uint/u16/rem.json b/zokrates_core_test/tests/tests/uint/u16/rem.json index afebdba57..61cf2701d 100644 --- a/zokrates_core_test/tests/tests/uint/u16/rem.json +++ b/zokrates_core_test/tests/tests/uint/u16/rem.json @@ -2,6 +2,18 @@ "entry_point": "./tests/tests/uint/u16/rem.zok", "max_constraint_count": 88, "tests": [ + { + "input": { + "values": ["0x0001", "0x0000"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "error": "Inverse" + } + } + } + }, { "input": { "values": ["0x0002", "0x0004"] diff --git a/zokrates_core_test/tests/tests/uint/u32/rem.json b/zokrates_core_test/tests/tests/uint/u32/rem.json index 4b24f228a..5d68dff29 100644 --- a/zokrates_core_test/tests/tests/uint/u32/rem.json +++ b/zokrates_core_test/tests/tests/uint/u32/rem.json @@ -2,6 +2,18 @@ "entry_point": "./tests/tests/uint/u32/rem.zok", "max_constraint_count": 168, "tests": [ + { + "input": { + "values": ["0x00000001", "0x00000000"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "error": "Inverse" + } + } + } + }, { "input": { "values": ["0x00000002", "0x00000004"] diff --git a/zokrates_core_test/tests/tests/uint/u64/rem.json b/zokrates_core_test/tests/tests/uint/u64/rem.json index c10e559b6..80a13a596 100644 --- a/zokrates_core_test/tests/tests/uint/u64/rem.json +++ b/zokrates_core_test/tests/tests/uint/u64/rem.json @@ -2,6 +2,18 @@ "entry_point": "./tests/tests/uint/u64/rem.zok", "max_constraint_count": 328, "tests": [ + { + "input": { + "values": ["0x0000000000000001", "0x0000000000000000"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "error": "Inverse" + } + } + } + }, { "input": { "values": ["0x0000000000000002", "0x0000000000000004"] diff --git a/zokrates_core_test/tests/tests/uint/u8/rem.json b/zokrates_core_test/tests/tests/uint/u8/rem.json index 587194ab6..a22bbc3c5 100644 --- a/zokrates_core_test/tests/tests/uint/u8/rem.json +++ b/zokrates_core_test/tests/tests/uint/u8/rem.json @@ -2,6 +2,18 @@ "entry_point": "./tests/tests/uint/u8/rem.zok", "max_constraint_count": 48, "tests": [ + { + "input": { + "values": ["0x01", "0x00"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "error": "Inverse" + } + } + } + }, { "input": { "values": ["0x02", "0x04"]