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.
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: // `P` is inferred from the declaration of `res`, while `N` is provided explicitly field res = foo::<3, _>() return res
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-isolationfeature comes with overhead for each assertion in each branch, and this overhead compounds when deeply nesting conditionals.
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 < maxis 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
def main() -> (): assert(1f + 1f == 2f) return
If any assertion fails, execution stops as no valid proof could be generated from it.