From 65ea034520dc0cecc1244d0d6eb861d06d1dcfb2 Mon Sep 17 00:00:00 2001 From: dark64 Date: Tue, 22 Nov 2022 19:45:01 +0100 Subject: [PATCH] add assembly section to the book --- zokrates_book/src/SUMMARY.md | 1 + zokrates_book/src/language/assembly.md | 107 ++++++++++++++++++ .../tests/tests/assembly/condition.zok | 3 +- 3 files changed, 109 insertions(+), 2 deletions(-) create mode 100644 zokrates_book/src/language/assembly.md diff --git a/zokrates_book/src/SUMMARY.md b/zokrates_book/src/SUMMARY.md index 298f9043..5d2830cb 100644 --- a/zokrates_book/src/SUMMARY.md +++ b/zokrates_book/src/SUMMARY.md @@ -16,6 +16,7 @@ - [Comments](language/comments.md) - [Macros](language/macros.md) - [Logging](language/logging.md) + - [Assembly](language/assembly.md) - [Toolbox](toolbox/index.md) - [CLI](toolbox/cli.md) diff --git a/zokrates_book/src/language/assembly.md b/zokrates_book/src/language/assembly.md new file mode 100644 index 00000000..9d7cfcb3 --- /dev/null +++ b/zokrates_book/src/language/assembly.md @@ -0,0 +1,107 @@ +## Assembly + +ZoKrates allows developers to define constraints through assembly blocks. Assembly blocks are considered **unsafe**, as safety and correctness of the resulting arithmetic circuit is in the hands of the developer. Usage of assembly is recommended only in optimization efforts for the experienced developers to minimize constraint count of an arithmetic circuit. + +## Writing assembly + +All constraints must be enclosed within an `asm` block. In an assembly block we can do the following: + +1. Assign to a witness variable using `<--` +2. Define a constraint using `===` + +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; + } +} +``` + +> The operator `<--` can be sometimes misused, as this operator does not generate any constraints, resulting in unconstrained variables in the constraint system. + +In some cases we can combine the witness assignment and constraint generation with the `<==` operator: + +```zok +asm { + c <== 1 - a*b; +} +``` + +which is equivalent to: + +```zok +asm { + c <-- 1 - a*b; + c === 1 - a*b; +} +``` + +A constraint can contain arithmetic expressions that are built using multiplication, addition, and other variables or `field` values. Only quadratic expressions are allowed to be included in constraints. Non-quadratic expressions or usage of other arithmetic operators like division or power are not allowed as constraints, but can be used in the witness assignment expression. + +The following code is not allowed: + +```zok +asm { + d === a*b*c; +} +``` + +as the constraint `d === a*b*c` is not quadratic. + +In some cases, ZoKrates will apply minor transformations on the defined constraints in order to meet the correct format: + +```zok +asm { + x * (x - 1) === 0; +} +``` + +will be transformed to: + +```zok +asm { + x === x * x; +} +``` + +## Type casting + +Assembly is a low-level part of the compiler which does not have type safety. In some cases we might want to do zero-cost conversions between `field` and `bool` type. + +### field_to_bool_unsafe + +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; +} +``` + +### bool_to_field + +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; +} +``` \ No newline at end of file diff --git a/zokrates_core_test/tests/tests/assembly/condition.zok b/zokrates_core_test/tests/tests/assembly/condition.zok index 9530ce7a..05aff5e3 100644 --- a/zokrates_core_test/tests/tests/assembly/condition.zok +++ b/zokrates_core_test/tests/tests/assembly/condition.zok @@ -1,8 +1,7 @@ def main(field c, field l, field r) -> field { field mut out = 0; asm { - out <-- c != 0 ? l : r; - out - r === c * (l - r); + out <== c * l + (1 - c) * r; } return out; } \ No newline at end of file