Any statements valid for a computation are valid for a consensus step. However, some additional statements are allowed.
Assigns the given participant to the given address. If a backend is running for this participant and its address does not match the given address, then it will abort. This may only occur within a consensus step.
Workshop: Relay Account is a good introductory project that demonstrates how to use this feature of Reach.
A while statement may occur within a consensus step and is written:
LHS is a valid left-hand side of an identifier definition where the expression
INIT_EXPR is the right-hand side, and
INVARIANT_EXPR is an expression, called the loop invariant, that must be true before and after every execution of the block
BLOCK, and if
COND_EXPR is true, then the block executes, and if not, then the loop terminates and control transfers to the continuation of the while statement. The identifiers bound by
LHS are bound within
BLOCK, and the tail of the while statement.
Read about finding loop invariants in the Reach guide.
[ heap1, heap2 ] = [ heap1 - 1, heap2 ]; continue;
LHS = UPDATE_EXPR; continue;
A continue statement may be written without the preceding identifier update, which is equivalent to writing
 = ; continue;
A continue statement must be dominated by a consensus transfer, which means that the body of a while statement must always
commit(); before calling
This restriction may be lifted in future versions of Reach, which will perform termination checking.
Any expressions valid for a computation are valid for a consensus step. However, some additional expressions are allowed.
A transfer expression, written
AMOUNT_EXPR is an expression that evaluates to a natural number and
PART is a participant identifier, performs a transfer of network tokens from the contract to the named participant.
AMOUNT_EXPR must evaluate to less than or equal to the balance of network tokens in the contract account. A transfer expression may only occur within a consensus step.