ZoKrates

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 experienced developers to minimize constraint count of an arithmetic circuit.

The usage of assembly blocks in ZoKrates is experimental. In particular, while assembly blocks help minimise constraint count in some cases, they currently can at the same time lead to larger compiler output and slower witness generation.

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:

def main(field a, field b) -> field {
    field mut c = 0;
    field mut invb = 0;
    asm {
        invb <-- b == 0 ? 0 : 1 / b;
        invb * b === 1;
        c <-- invb * a;
        a === b * c;
    }
    return c;
}

Note that operator <-- is used for unconstrained assignment and can be easily misused. This operator does not generate constraints, which could result in unconstrained variables in the constraint system.

Unconstrained assignment <-- allows assignment to variables with complex types. The type must consist of field elements only (eg. field[3]):

field[3] mut c = [0; 3];
asm {
    c <-- [2, 2, 4];
    c[0] * c[1] === c[2];
}

In some cases we can combine the witness assignment and constraint generation with the <== operator (constrained assignment):

asm {
    c <== 1 - a*b;
}

which is equivalent to:

asm {
    c <-- 1 - a*b;
    c === 1 - a*b;
}

In the case of constrained assignment <==, both sides of the statement have to be of type field.

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:

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:

asm {
    x * (x - 1) === 0;
}

will be transformed to:

asm {
    x === x * x;
}

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.

This call is unsafe because it is the responsibility of the user to constrain the field input:

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 convert `x` to `bool` afterwards, as we constrained it properly
    // if we failed to constrain `x` to `0` or `1`, the call to `field_to_bool_unsafe` introduces undefined behavior
    // `field_to_bool_unsafe` call does not produce any extra constraints
    bool out = field_to_bool_unsafe(x);
    return out;
}