Control Flow

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

Function calls

Function calls help make programs clear and modular.

Arguments are passed by value.

def incr(field 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 paramaters, 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

If-expressions

An if-expression allows you to branch your code depending on a boolean condition.

def main(field x) -> field:
  field y = if x + 2 == 3 then 1 else 5 fi
  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 then\
        cheap(x)\// executed
        else\
        expensive(x)\// also executed
    fi
  • 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 then\
        0\
        else\
        1/x\// executed even for x := 0, which leads to the execution failing
    fi

The experimental flag --branch-isolation can be activated in the CLI in order to restrict any unsatisfied constraint to make the execution fail only if it is in a logically executed branch. This way, the execution of the program above will always succeed.

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. The branch-isolation feature comes with overhead for each assertion in each branch, and this overhead compounds when deeply nesting conditionals.

For loops

For loops are available with the following syntax:

def main() -> u32:
    u32 res = 0
    for u32 i in 0..4 do
        for u32 j in i..5 do
            res = res + i
        endfor
    endfor
    return res

The bounds have to be constant at compile-time, therefore they cannot depend on execution inputs. They can depend on generic parameters.

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.

Assertions

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.