diff --git a/t.code b/t.code deleted file mode 100644 index a38f522b..00000000 --- a/t.code +++ /dev/null @@ -1,16 +0,0 @@ -from "./u.code" import Fooo - -struct Bar { - a: field, - a: field, - c: field, -} - -struct Baz { - a: Bar -} - -def main(Bar a, Bar b, bool c) -> (Bar): - Bar bar = Bar { a: 1, b: 1, c: 1 } - return if false then a else bar fi - diff --git a/u.code b/u.code deleted file mode 100644 index f420f0f2..00000000 --- a/u.code +++ /dev/null @@ -1,4 +0,0 @@ -struct Foo { - a: field, - b: field[2], -} \ No newline at end of file diff --git a/zokrates_core/src/compile.rs b/zokrates_core/src/compile.rs index 82990bcf..861b76ca 100644 --- a/zokrates_core/src/compile.rs +++ b/zokrates_core/src/compile.rs @@ -138,8 +138,6 @@ pub fn compile>( let source = arena.alloc(source); - println!("{:?}", source); - let compiled = compile_program(source, location.clone(), resolve_option, &arena)?; // check semantics diff --git a/zokrates_core/src/flatten/mod.rs b/zokrates_core/src/flatten/mod.rs index f4a7d972..c92eb68b 100644 --- a/zokrates_core/src/flatten/mod.rs +++ b/zokrates_core/src/flatten/mod.rs @@ -1548,7 +1548,7 @@ impl<'ast, T: Field> Flattener<'ast, T> { let arguments_flattened = funct .arguments .into_iter() - .flat_map(|p| self.use_parameter(&p, &mut statements_flattened)) + .flat_map(|p| self.use_parameter(&p)) .collect(); // flatten statements in functions and apply substitution @@ -1602,19 +1602,8 @@ impl<'ast, T: Field> Flattener<'ast, T> { vars } - fn use_parameter( - &mut self, - parameter: &Parameter<'ast>, - statements: &mut Vec>, - ) -> Vec { + fn use_parameter(&mut self, parameter: &Parameter<'ast>) -> Vec { let variables = self.use_variable(¶meter.id); - match parameter.id.get_type() { - Type::Boolean => statements.extend(Self::boolean_constraint(&variables)), - Type::Array(box Type::Boolean, _) => { - statements.extend(Self::boolean_constraint(&variables)) - } - _ => {} - }; variables .into_iter() @@ -1635,21 +1624,6 @@ impl<'ast, T: Field> Flattener<'ast, T> { (0..count).map(|_| self.issue_new_variable()).collect() } - fn boolean_constraint(variables: &Vec) -> Vec> { - variables - .iter() - .map(|v| { - FlatStatement::Condition( - FlatExpression::Identifier(*v), - FlatExpression::Mult( - box FlatExpression::Identifier(*v), - box FlatExpression::Identifier(*v), - ), - ) - }) - .collect() - } - // create an internal variable. We do not register it in the layout fn use_sym(&mut self) -> FlatVariable { self.issue_new_variable() diff --git a/zokrates_core/src/static_analysis/constrain_inputs.rs b/zokrates_core/src/static_analysis/constrain_inputs.rs new file mode 100644 index 00000000..711024f7 --- /dev/null +++ b/zokrates_core/src/static_analysis/constrain_inputs.rs @@ -0,0 +1,120 @@ +//! Add runtime boolean checks on user inputs +//! Example: +//! ``` +//! struct Foo { +//! bar: bool +//! } +//! +//! def main(Foo f) -> (): +//! f.bar == f.bar && f.bar +//! return +//! ``` +//! @file unroll.rs +//! @author Thibaut Schaeffer +//! @date 2018 + +use crate::typed_absy::folder::Folder; +use crate::typed_absy::types::Type; +use crate::typed_absy::*; +use zokrates_field::field::Field; + +pub struct InputConstrainer<'ast, T: Field> { + constraints: Vec>, +} + +impl<'ast, T: Field> InputConstrainer<'ast, T> { + fn new() -> Self { + InputConstrainer { + constraints: vec![], + } + } + + pub fn constrain(p: TypedProgram) -> TypedProgram { + InputConstrainer::new().fold_program(p) + } + + fn constrain_expression(&mut self, e: TypedExpression<'ast, T>) { + match e { + TypedExpression::FieldElement(_) => {} + TypedExpression::Boolean(b) => self.constraints.push(TypedStatement::Condition( + b.clone().into(), + BooleanExpression::And(box b.clone(), box b).into(), + )), + TypedExpression::Array(a) => { + for i in 0..a.size() { + let e = match a.inner_type() { + Type::FieldElement => FieldElementExpression::select( + a.clone(), + FieldElementExpression::Number(T::from(i)), + ) + .into(), + Type::Boolean => BooleanExpression::select( + a.clone(), + FieldElementExpression::Number(T::from(i)), + ) + .into(), + Type::Array(..) => ArrayExpression::select( + a.clone(), + FieldElementExpression::Number(T::from(i)), + ) + .into(), + Type::Struct(..) => StructExpression::select( + a.clone(), + FieldElementExpression::Number(T::from(i)), + ) + .into(), + }; + + self.constrain_expression(e); + } + } + TypedExpression::Struct(s) => { + for (id, ty) in s.ty() { + let e = match ty { + Type::FieldElement => { + FieldElementExpression::member(s.clone(), id.clone()).into() + } + Type::Boolean => BooleanExpression::member(s.clone(), id.clone()).into(), + Type::Array(..) => ArrayExpression::member(s.clone(), id.clone()).into(), + Type::Struct(..) => StructExpression::member(s.clone(), id.clone()).into(), + }; + + self.constrain_expression(e); + } + } + } + } +} + +impl<'ast, T: Field> Folder<'ast, T> for InputConstrainer<'ast, T> { + fn fold_parameter(&mut self, p: Parameter<'ast>) -> Parameter<'ast> { + let v = p.id.clone(); + + let e = match v.get_type() { + Type::FieldElement => FieldElementExpression::Identifier(v.id).into(), + Type::Boolean => BooleanExpression::Identifier(v.id).into(), + Type::Struct(members) => StructExpressionInner::Identifier(v.id) + .annotate(members) + .into(), + Type::Array(box ty, size) => ArrayExpressionInner::Identifier(v.id) + .annotate(ty, size) + .into(), + }; + + self.constrain_expression(e); + + p + } + + fn fold_function(&mut self, f: TypedFunction<'ast, T>) -> TypedFunction<'ast, T> { + TypedFunction { + arguments: f + .arguments + .into_iter() + .map(|a| self.fold_parameter(a)) + .collect(), + statements: self.constraints.drain(..).chain(f.statements).collect(), + ..f + } + } +} diff --git a/zokrates_core/src/static_analysis/mod.rs b/zokrates_core/src/static_analysis/mod.rs index 386d4c49..e2c2e10d 100644 --- a/zokrates_core/src/static_analysis/mod.rs +++ b/zokrates_core/src/static_analysis/mod.rs @@ -4,11 +4,13 @@ //! @author Thibaut Schaeffer //! @date 2018 +mod constrain_inputs; mod flat_propagation; mod inline; mod propagation; mod unroll; +use self::constrain_inputs::InputConstrainer; use self::inline::Inliner; use self::propagation::Propagator; use self::unroll::Unroller; @@ -24,11 +26,12 @@ impl<'ast, T: Field> Analyse for TypedProgram<'ast, T> { fn analyse(self) -> Self { // unroll let r = Unroller::unroll(self); - println!("{}", r); // inline let r = Inliner::inline(r); // propagate let r = Propagator::propagate(r); + // constrain inputs + let r = InputConstrainer::constrain(r); r } } diff --git a/zokrates_core_test/tests/tests/arrays/identity.code b/zokrates_core_test/tests/tests/arrays/identity.code new file mode 100644 index 00000000..8c97930b --- /dev/null +++ b/zokrates_core_test/tests/tests/arrays/identity.code @@ -0,0 +1,2 @@ +def main(bool[3] a) -> (bool[3]): + return a \ No newline at end of file diff --git a/zokrates_core_test/tests/tests/arrays/identity.json b/zokrates_core_test/tests/tests/arrays/identity.json new file mode 100644 index 00000000..e6a36236 --- /dev/null +++ b/zokrates_core_test/tests/tests/arrays/identity.json @@ -0,0 +1,38 @@ +{ + "entry_point": "./tests/tests/arrays/identity.code", + "tests": [ + { + "input": { + "values": ["0", "0", "0"] + }, + "output": { + "Ok": { + "values": ["0", "0", "0"] + } + } + }, + { + "input": { + "values": ["1", "0", "1"] + }, + "output": { + "Ok": { + "values": ["1", "0", "1"] + } + } + }, + { + "input": { + "values": ["2", "1", "1"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "left": "4", + "right": "2" + } + } + } + } + ] +} \ No newline at end of file diff --git a/zokrates_core_test/tests/tests/structs/identity.code b/zokrates_core_test/tests/tests/structs/identity.code new file mode 100644 index 00000000..041e79ed --- /dev/null +++ b/zokrates_core_test/tests/tests/structs/identity.code @@ -0,0 +1,7 @@ +struct A { + a: field, + b: bool +} + +def main(A a) -> (A): + return a \ No newline at end of file diff --git a/zokrates_core_test/tests/tests/structs/identity.json b/zokrates_core_test/tests/tests/structs/identity.json new file mode 100644 index 00000000..db4b136e --- /dev/null +++ b/zokrates_core_test/tests/tests/structs/identity.json @@ -0,0 +1,38 @@ +{ + "entry_point": "./tests/tests/structs/identity.code", + "tests": [ + { + "input": { + "values": ["42", "0"] + }, + "output": { + "Ok": { + "values": ["42", "0"] + } + } + }, + { + "input": { + "values": ["42", "1"] + }, + "output": { + "Ok": { + "values": ["42", "1"] + } + } + }, + { + "input": { + "values": ["42", "3"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "left": "9", + "right": "3" + } + } + } + } + ] +} \ No newline at end of file