From fd361d68f380cff86f5630b8e0c9913446eb53de Mon Sep 17 00:00:00 2001 From: dark64 Date: Tue, 22 Nov 2022 20:32:49 +0100 Subject: [PATCH] more tests --- zokrates_analysis/src/propagation.rs | 1 + zokrates_ast/src/common/embed.rs | 8 ++++ zokrates_book/src/language/assembly.md | 30 ++------------- .../examples/book/assembly/bool_to_field.zok | 8 ++++ .../examples/book/assembly/division.zok | 7 ++++ .../examples/book/assembly/field_to_bool.zok | 12 ++++++ zokrates_codegen/src/lib.rs | 1 + zokrates_core/src/imports.rs | 4 ++ .../tests/tests/assembly/less_than.json | 36 ++++++++++++++++++ .../tests/tests/assembly/less_than.zok | 14 +++++++ .../tests/tests/embed/bool_to_field.json | 26 +++++++++++++ .../tests/tests/embed/bool_to_field.zok | 6 +++ .../tests/tests/embed/field_to_bool.json | 38 +++++++++++++++++++ .../tests/tests/embed/field_to_bool.zok | 9 +++++ 14 files changed, 173 insertions(+), 27 deletions(-) create mode 100644 zokrates_cli/examples/book/assembly/bool_to_field.zok create mode 100644 zokrates_cli/examples/book/assembly/division.zok create mode 100644 zokrates_cli/examples/book/assembly/field_to_bool.zok create mode 100644 zokrates_core_test/tests/tests/assembly/less_than.json create mode 100644 zokrates_core_test/tests/tests/assembly/less_than.zok create mode 100644 zokrates_core_test/tests/tests/embed/bool_to_field.json create mode 100644 zokrates_core_test/tests/tests/embed/bool_to_field.zok create mode 100644 zokrates_core_test/tests/tests/embed/field_to_bool.json create mode 100644 zokrates_core_test/tests/tests/embed/field_to_bool.zok diff --git a/zokrates_analysis/src/propagation.rs b/zokrates_analysis/src/propagation.rs index 1369fc04..f6808921 100644 --- a/zokrates_analysis/src/propagation.rs +++ b/zokrates_analysis/src/propagation.rs @@ -400,6 +400,7 @@ impl<'ast, 'a, T: Field> ResultFolder<'ast, T> for Propagator<'ast, 'a, T> { true => { let r: Option> = match embed_call.embed { FlatEmbed::FieldToBoolUnsafe => Ok(None), // todo + FlatEmbed::BoolToField => Ok(None), // todo FlatEmbed::BitArrayLe => Ok(None), // todo FlatEmbed::U64FromBits => Ok(Some(process_u_from_bits( &embed_call.arguments, diff --git a/zokrates_ast/src/common/embed.rs b/zokrates_ast/src/common/embed.rs index 58294142..3f961cd9 100644 --- a/zokrates_ast/src/common/embed.rs +++ b/zokrates_ast/src/common/embed.rs @@ -32,6 +32,7 @@ cfg_if::cfg_if! { #[derive(Debug, Clone, PartialEq, Eq, Hash, Copy, PartialOrd, Ord, Serialize, Deserialize)] pub enum FlatEmbed { FieldToBoolUnsafe, + BoolToField, BitArrayLe, Unpack, U8ToBits, @@ -54,6 +55,9 @@ impl FlatEmbed { FlatEmbed::FieldToBoolUnsafe => UnresolvedSignature::new() .inputs(vec![UnresolvedType::FieldElement.into()]) .output(UnresolvedType::Boolean.into()), + FlatEmbed::BoolToField => UnresolvedSignature::new() + .inputs(vec![UnresolvedType::Boolean.into()]) + .output(UnresolvedType::FieldElement.into()), FlatEmbed::BitArrayLe => UnresolvedSignature::new() .generics(vec![ConstantGenericNode::mock("N")]) .inputs(vec![ @@ -193,6 +197,9 @@ impl FlatEmbed { FlatEmbed::FieldToBoolUnsafe => DeclarationSignature::new() .inputs(vec![DeclarationType::FieldElement]) .output(DeclarationType::Boolean), + FlatEmbed::BoolToField => DeclarationSignature::new() + .inputs(vec![DeclarationType::Boolean]) + .output(DeclarationType::FieldElement), FlatEmbed::BitArrayLe => DeclarationSignature::new() .generics(vec![Some(DeclarationConstant::Generic( GenericIdentifier::with_name("N").with_index(0), @@ -300,6 +307,7 @@ impl FlatEmbed { pub fn id(&self) -> &'static str { match self { FlatEmbed::FieldToBoolUnsafe => "_FIELD_TO_BOOL_UNSAFE", + FlatEmbed::BoolToField => "_BOOL_TO_FIELD", FlatEmbed::BitArrayLe => "_BIT_ARRAY_LT", FlatEmbed::Unpack => "_UNPACK", FlatEmbed::U8ToBits => "_U8_TO_BITS", diff --git a/zokrates_book/src/language/assembly.md b/zokrates_book/src/language/assembly.md index 9d7cfcb3..a6782a6d 100644 --- a/zokrates_book/src/language/assembly.md +++ b/zokrates_book/src/language/assembly.md @@ -12,13 +12,7 @@ All constraints must be enclosed within an `asm` block. In an assembly block we Assigning a value, in general, should be combined with adding a constraint: ```zok -def main(field a, field b) { - field mut c = 0; - asm { - c <-- a / b; - a === b * c; - } -} +{{#include ../../../zokrates_cli/examples/book/assembly/division.zok}} ``` > The operator `<--` can be sometimes misused, as this operator does not generate any constraints, resulting in unconstrained variables in the constraint system. @@ -77,18 +71,7 @@ Assembly is a low-level part of the compiler which does not have type safety. In This call is unsafe because it is the responsibility of the user to constrain the field input: ```zok -from "EMBED" import field_to_bool_unsafe; - -def main(field x) -> bool { - // we constrain `x` to be 0 or 1 - asm { - x * (x - 1) === 0; - } - // we can treat `x` as `bool` afterwards, as we constrained it properly - // `field_to_bool_unsafe` call does not produce any extra constraints - bool out = field_to_bool_unsafe(x); - return out; -} +{{#include ../../../zokrates_cli/examples/book/assembly/field_to_bool.zok}} ``` ### bool_to_field @@ -96,12 +79,5 @@ def main(field x) -> bool { This call is safe as `bool` types are constrained by the compiler: ```zok -from "EMBED" import bool_to_field; - -def main(bool x) -> field { - // `x` is constrained by the compiler automatically so we can safely - // treat it as `field` with no extra cost - field out = bool_to_field(x); - return out; -} +{{#include ../../../zokrates_cli/examples/book/assembly/bool_to_field.zok}} ``` \ No newline at end of file diff --git a/zokrates_cli/examples/book/assembly/bool_to_field.zok b/zokrates_cli/examples/book/assembly/bool_to_field.zok new file mode 100644 index 00000000..4c1284b0 --- /dev/null +++ b/zokrates_cli/examples/book/assembly/bool_to_field.zok @@ -0,0 +1,8 @@ +from "EMBED" import bool_to_field; + +def main(bool x) -> field { + // `x` is constrained by the compiler automatically so we can safely + // treat it as `field` with no extra cost + field out = bool_to_field(x); + return out; +} \ No newline at end of file diff --git a/zokrates_cli/examples/book/assembly/division.zok b/zokrates_cli/examples/book/assembly/division.zok new file mode 100644 index 00000000..c38e18ee --- /dev/null +++ b/zokrates_cli/examples/book/assembly/division.zok @@ -0,0 +1,7 @@ +def main(field a, field b) { + field mut c = 0; + asm { + c <-- a / b; + a === b * c; + } +} \ No newline at end of file diff --git a/zokrates_cli/examples/book/assembly/field_to_bool.zok b/zokrates_cli/examples/book/assembly/field_to_bool.zok new file mode 100644 index 00000000..b213b346 --- /dev/null +++ b/zokrates_cli/examples/book/assembly/field_to_bool.zok @@ -0,0 +1,12 @@ +from "EMBED" import field_to_bool_unsafe; + +def main(field x) -> bool { + // we constrain `x` to be 0 or 1 + asm { + x * (x - 1) === 0; + } + // we can treat `x` as `bool` afterwards, as we constrained it properly + // `field_to_bool_unsafe` call does not produce any extra constraints + bool out = field_to_bool_unsafe(x); + return out; +} \ No newline at end of file diff --git a/zokrates_codegen/src/lib.rs b/zokrates_codegen/src/lib.rs index 4c08dd73..25317391 100644 --- a/zokrates_codegen/src/lib.rs +++ b/zokrates_codegen/src/lib.rs @@ -1050,6 +1050,7 @@ impl<'ast, T: Field> Flattener<'ast, T> { match embed { FlatEmbed::FieldToBoolUnsafe => vec![params.pop().unwrap()], + FlatEmbed::BoolToField => vec![params.pop().unwrap()], FlatEmbed::U8ToBits => self.u_to_bits(params.pop().unwrap(), 8.into()), FlatEmbed::U16ToBits => self.u_to_bits(params.pop().unwrap(), 16.into()), FlatEmbed::U32ToBits => self.u_to_bits(params.pop().unwrap(), 32.into()), diff --git a/zokrates_core/src/imports.rs b/zokrates_core/src/imports.rs index f7fa95f1..4bdf4940 100644 --- a/zokrates_core/src/imports.rs +++ b/zokrates_core/src/imports.rs @@ -151,6 +151,10 @@ impl Importer { id: symbol.get_alias(), symbol: Symbol::Flat(FlatEmbed::FieldToBoolUnsafe), }, + "bool_to_field" => SymbolDeclaration { + id: symbol.get_alias(), + symbol: Symbol::Flat(FlatEmbed::BoolToField), + }, "bit_array_le" => SymbolDeclaration { id: symbol.get_alias(), symbol: Symbol::Flat(FlatEmbed::BitArrayLe), diff --git a/zokrates_core_test/tests/tests/assembly/less_than.json b/zokrates_core_test/tests/tests/assembly/less_than.json new file mode 100644 index 00000000..91eaaa07 --- /dev/null +++ b/zokrates_core_test/tests/tests/assembly/less_than.json @@ -0,0 +1,36 @@ +{ + "curves": ["Bn128"], + "max_constraint_count": 7, + "tests": [ + { + "input": { + "values": ["2", "2"] + }, + "output": { + "Ok": { + "value": false + } + } + }, + { + "input": { + "values": ["4", "2"] + }, + "output": { + "Ok": { + "value": false + } + } + }, + { + "input": { + "values": ["2", "4"] + }, + "output": { + "Ok": { + "value": true + } + } + } + ] +} diff --git a/zokrates_core_test/tests/tests/assembly/less_than.zok b/zokrates_core_test/tests/tests/assembly/less_than.zok new file mode 100644 index 00000000..8af9235d --- /dev/null +++ b/zokrates_core_test/tests/tests/assembly/less_than.zok @@ -0,0 +1,14 @@ +from "EMBED" import field_to_bool_unsafe; +from "field" import FIELD_SIZE_IN_BITS; +from "./bitify" import bitify; + +def less_than(field a, field b) -> bool { + assert(N < FIELD_SIZE_IN_BITS - 1); + field[N + 1] bits = bitify(a + (1f << N) - b); + bool out = field_to_bool_unsafe(1 - bits[N]); + return out; +} + +def main(field a, field b) -> bool { + return less_than::<4>(a, b); +} \ No newline at end of file diff --git a/zokrates_core_test/tests/tests/embed/bool_to_field.json b/zokrates_core_test/tests/tests/embed/bool_to_field.json new file mode 100644 index 00000000..5e78b298 --- /dev/null +++ b/zokrates_core_test/tests/tests/embed/bool_to_field.json @@ -0,0 +1,26 @@ +{ + "curves": ["Bn128"], + "max_constraint_count": 2, + "tests": [ + { + "input": { + "values": [false] + }, + "output": { + "Ok": { + "value": "0" + } + } + }, + { + "input": { + "values": [true] + }, + "output": { + "Ok": { + "value": "1" + } + } + } + ] +} diff --git a/zokrates_core_test/tests/tests/embed/bool_to_field.zok b/zokrates_core_test/tests/tests/embed/bool_to_field.zok new file mode 100644 index 00000000..457ac06d --- /dev/null +++ b/zokrates_core_test/tests/tests/embed/bool_to_field.zok @@ -0,0 +1,6 @@ +from "EMBED" import bool_to_field; + +def main(bool x) -> field { + field out = bool_to_field(x); + return out; +} \ No newline at end of file diff --git a/zokrates_core_test/tests/tests/embed/field_to_bool.json b/zokrates_core_test/tests/tests/embed/field_to_bool.json new file mode 100644 index 00000000..d24af7e0 --- /dev/null +++ b/zokrates_core_test/tests/tests/embed/field_to_bool.json @@ -0,0 +1,38 @@ +{ + "curves": ["Bn128"], + "max_constraint_count": 2, + "tests": [ + { + "input": { + "values": ["0"] + }, + "output": { + "Ok": { + "value": false + } + } + }, + { + "input": { + "values": ["1"] + }, + "output": { + "Ok": { + "value": true + } + } + }, + { + "input": { + "values": ["2"] + }, + "output": { + "Err": { + "UnsatisfiedConstraint": { + "error": "UserConstraint" + } + } + } + } + ] +} diff --git a/zokrates_core_test/tests/tests/embed/field_to_bool.zok b/zokrates_core_test/tests/tests/embed/field_to_bool.zok new file mode 100644 index 00000000..ebf77e9b --- /dev/null +++ b/zokrates_core_test/tests/tests/embed/field_to_bool.zok @@ -0,0 +1,9 @@ +from "EMBED" import field_to_bool_unsafe; + +def main(field x) -> bool { + asm { + x * (x - 1) === 0; + } + bool out = field_to_bool_unsafe(x); + return out; +} \ No newline at end of file