5.4 Programs
5.4.1 Validity
5.4.2 Modules
5.4.3 Steps
5.4.4 Local Steps
5.4.5 Consensus Steps
5.4.6 Computations
On this page: Statements commit
commit Participant.set and .set
Participant while
while continue
continue Expressions transfer
transfer require
require check  Commitment
check  Commitment
5.4.5 Consensus Steps

A Reach consensus step occurs in the continuation of a consensus transfer statement. It represents the actions taken by the consensus network contract of an application. Statements

Any statements valid for a computation are valid for a consensus step. However, some additional statements are allowed. commit


A commit statement, written commit();, commits to statement’s continuation as the next step of the DApp computation. In other words, it ends the current consensus step and allows more local steps. Participant.set and .set

Participant.set(PART, ADDR);

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. while

var [ heap1, heap2 ] = [ 21, 21 ];
invariant(balance() == 2 * wagerAmount);
while ( heap1 + heap2 > 0 ) {
  [ heap1, heap2 ] = [ heap1 - 1, heap2 ];
  continue; } 

A while statement may occur within a consensus step and is written:


where 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 INVARIANT_EXPR, COND_EXPR, BLOCK, and the tail of the while statement.

Read about finding loop invariants in the Reach guide. continue

[ heap1, heap2 ] = [ heap1 - 1, heap2 ];

A continue statement may occur within a while statement’s block and is written:


where the identifiers bound by LHS are a subset of the variables bound by the nearest enclosing while statement and UPDATE_EXPR is an expression which may be bound by LHS.

A continue statement is a terminator statement, so it must have an empty tail.

A continue statement may be written without the preceding identifier update, which is equivalent to writing

[] = [];

A continue statement must be dominated by a consensus transfer, which means that the body of a while statement must always commit(); before calling continue;. This restriction may be lifted in future versions of Reach, which will perform termination checking. Expressions

Any expressions valid for a computation are valid for a consensus step. However, some additional expressions are allowed. transfer


A transfer expression, written transfer(AMOUNT_EXPR).to(PART), where 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. require

require( claim ) 

An requirement where claim evaluates to true with honest participants. This may only appear in a consensus step. checkCommitment

checkCommitment( commitment, salt, x ) 

Makes a requirement that commitment is the digest of salt and x.