ZoKrates

ZoKrates provides a single thread of execution with a few flow constructs.

Function calls help make programs clear and modular.

Arguments are passed by value.

Function parameters can be declared as mutable to allow for mutation within the function's body. However, mutable function arguments are still passed by value, so the original value can never be mutated.

def incr(field mut a) -> field {
    a = a + 1;
    return a;
}

def main() {
    field x = 1;
    field res = incr(x);
    assert(x == 1); // x has not changed
    return;
}

Generic parameters, if any, must be compile-time constants. They are inferred by the compiler if that is possible, but can also be provided explicitly.

def foo<N, P>() -> field[P] {
    return [42; P];
}

def main() -> field[2] {
    // `P` is inferred from the declaration of `res`, while `N` is provided explicitly
    field[2] res = foo::<3, _>();
    return res;
}

A conditional expression allows you to branch your code depending on a boolean condition.

def main(field x) -> field {
    field y = if x + 2 == 3 { 1 } else { 5 };
    return y;
}

The conditional expression can also be written using a ternary operator:

def main(field x) -> field {
    field y = x + 2 == 3 ? 1 : 5;
    return y;
}

There are two important caveats when it comes to conditional expressions. Before we go into them, let's define two concepts:

• for an execution of the program, an executed branch is a branch which has to be paid for when executing the program, generating proofs, etc.
• for an execution of the program, a logically executed branch is a branch which is "chosen" by the condition of an if-expression. This is the more intuitive notion of execution, and there is only one for each if-expression.

Now the two caveats:

• Both branches are always executed. No short-circuiting happens based on the value of the condition. Therefore, the complexity of a program in terms of the number of constraints it compiles down to is the sum of the cost of all branches.

def cheap(field x) -> field {
    return x + 1;
}

def expensive(field x) -> field {
    return x**1000;
}

def main(field x) -> field {
    return if x == 1 {
        cheap(x)
    } else {
        expensive(x) // both branches executed
    };
}

• An unsatisfied constraint inside any branch will make the whole execution fail, even if this branch is not logically executed. Also, the compiler itself inserts assertions which can fail. This can lead to unexpected results:

def main(field x) -> field {
    return if x == 0 {
        0
    } else {
        1 / x // executed even for x := 0, which leads to the execution failing
    };
}

The reason for these caveats is that the program is compiled down to an arithmetic circuit. This construct does not support jumping to a branch depending on a condition as you could do on traditional architectures. Instead, all branches are inlined as if they were printed on a circuit board.

For loops are available with the following syntax:

def main() -> u32 {
    u32 mut res = 0;
    for u32 i in 0..4 {
        for u32 j in i..5 {
            res = res + i;
        }
    }
    return res;
}

The bounds have to be constant at compile-time, therefore they cannot depend on execution inputs. They can depend on generic parameters. The range is half-open, meaning it is bounded inclusively below and exclusively above. The range start..end contains all values within start <= x < end. The range is empty if start >= end.

For loops are only syntactic sugar for repeating a block of statements many times. No condition of the type index < max is being checked at run-time after each iteration. Instead, at compile-time, the index is incremented and the block is executed again. Therefore, assigning to the loop index does not have any influence on the number of iterations performed and is considered bad practice.

Any boolean can be asserted to be true using the assert function.

def main() {
    assert(1f + 1f == 2f);
    return;
}

If any assertion fails, execution stops as no valid proof could be generated from it.