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:
5.4.5.1 Statements
5.4.5.1.1 commit
commit
5.4.5.1.2 only and each
5.4.5.1.3 View Objects
5.4.5.1.4 Participant.set and .set
5.4.5.1.5 while
var
invariant
while
5.4.5.1.6 continue
continue
5.4.5.1.7 parallel  Reduce
parallel  Reduce
time  Remaining
throw  Timeout
5.4.5.2 Expressions
5.4.5.2.1 this
5.4.5.2.2 transfer
transfer
5.4.5.2.3 require
require
5.4.5.2.4 check  Commitment
check  Commitment
5.4.5.2.5 Remote objects
remote
bill
with  Bill
5.4.5.2.6 Mappings:   creation and modification
Map
5.4.5.2.7 Sets:   creation and modification
Set
insert
remove
member
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.

5.4.5.1 Statements

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

5.4.5.1.1 commit

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.

5.4.5.1.2 only and each

only and each are allowed in consensus steps and are executed by backends once they observe the completion of the consensus step (i.e., after the associated commit statement.)

5.4.5.1.3 View Objects

vNFT.owner.set(creator);

If VIEW is a view object, then its fields are the elements of the associated view. Each of these fields are bound to an object with an set method that accepts the function or value to be bound to that view at the current step, and all steps dominated by the current step (unless otherwise overridden.) If this function is not provided with an argument, then the corresponding view is unset.

For example, consider the following program:

 1    'reach 0.1';
 2    
 3    const Tlast = Maybe(Address);
 4    const Ti = Maybe(UInt);
 5    const T = Tuple(Tlast, Ti);
 6    
 7    export const main =
 8     Reach.App({},
 9      [ Participant('Alice', { checkView: Fun([T], Null) }),
10        Participant('Bob', {}),
11        View('Main', { last: Address, i: UInt }),
12      ],
13      (A, B, vMain) => {
14        const checkView = (x) =>
15          A.only(() => interact.checkView(x));
16    
17        // The contract doesn't exist yet, so no view
18        checkView([Tlast.None(), Ti.None()]);
19    
20        A.publish();
21        vMain.i.set(1);
22        vMain.last.set(A);
23        // These views are now visible
24        checkView([Tlast.Some(A), Ti.Some(1)]);
25        commit();
26    
27        // Block race of Alice and Bob for Alice to observe the state
28        A.publish();
29        commit();
30    
31        B.publish();
32        vMain.i.set(2);
33        vMain.last.set(B);
34        if ( A != B ) {
35          // The views above are visible
36          checkView([Tlast.Some(B), Ti.Some(2)]);
37          commit();
38        } else {
39          // Or, we overwrite them
40          vMain.i.set(3);
41          vMain.last.set();
42          checkView([Tlast.None(), Ti.Some(3)]);
43          commit();
44        }
45    
46        A.publish();
47        // The contract doesn't exist anymore, so no view
48        checkView([Tlast.None(), Ti.None()]);
49        commit();
50    
51        exit();
52      });

In this program, the Reach backend calls the frontend interact function, checkView with the expected value of the views at each point in the program. The frontend compares that value with what is returned by

[ await ctc.getViews().Main.last(),
  await ctc.getViews().Main.i() ]

When a view is bound to a function, it may inspect any values in its scope, including linear state.

5.4.5.1.4 Participant.set and .set

Participant.set(PART, ADDR);
PART.set(ADDR); 

After execution, the given participant is fixed to the given address. It is invalid to attempt to .set a participant class. 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.

5.4.5.1.5 while

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

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

var LHS = INIT_EXPR;
BLOCK; // optional
invariant(INVARIANT_EXPR);
while( COND_EXPR ) BLOCK 

where LHS is a valid left-hand side of an identifier definition where the expression INIT_EXPR is the right-hand side, and BLOCK is an optional block that may define bindings that use the LHS values which are bound inside the rest of the while and its tail, 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.

5.4.5.1.6 continue

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

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

LHS = UPDATE_EXPR;
continue; 

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

[] = [];
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 continue;. This restriction may be lifted in future versions of Reach, which will perform termination checking.

5.4.5.1.7 parallelReduce

const [ keepGoing, as, bs ] =
  parallelReduce([ true, 0, 0 ])
  .invariant(balance() == 2 * wager)
  .while(keepGoing)
  .case(Alice, (() => ({
    when: declassify(interact.keepGoing()) })),
    (_) => {
      each([Alice, Bob], () => {
        interact.roundWinnerWas(true); });
      return [ true, 1 + as, bs ]; })
  .case(Bob, (() => ({
    when: declassify(interact.keepGoing()) })),
    (_) => {
      each([Alice, Bob], () => {
        interact.roundWinnerWas(false); });
      return [ true, as, 1 + bs ]; })
  .timeout(deadline, () => {
    showOutcome(TIMEOUT)();
    race(Alice, Bob).publish();
    return [ false, as, bs ]; });

A parallel reduce statement is written:

const LHS =
  parallelReduce(INIT_EXPR)
  .invariant(INVARIANT_EXPR)
  .while(COND_EXPR)
  .paySpec(TOKENS_EXPR)
  .case(PART_EXPR,
    PUBLISH_EXPR,
    PAY_EXPR,
    CONSENSUS_EXPR)
  .timeout(DELAY_EXPR, () =>
    TIMEOUT_BLOCK);

The LHS and INIT_EXPR are like the initialization component of a while loop; and, the .invariant and .while components are like the invariant and condition of a while loop; while the .case, .timeout, and .paySpec components are like the corresponding components of a fork statement.

The .case component may be repeated many times, provided the PART_EXPRs each evaluate to a unique participant, just like in a fork statement.

.timeRemaining

When dealing with absolute deadlines in parallelReduce, there is a common pattern in the TIMEOUT_BLOCK to have participants race to publish and return the accumulator. There is a shorthand, .timeRemaining, available for this situation:

const [ timeRemaining, keepGoing ] = makeDeadline(deadline);
const [ x, y, z ] =
  parallelReduce([ 1, 2, 3 ])
    .while(keepGoing())
    ...
    .timeRemaining(timeRemaining()) 

which will expand to:

.timeout(timeRemaining(), () => {
  race(...Participants).publish();
  return [ x, y, z ]; }) 

.throwTimeout

.throwTimeout is a shorthand that will throw the accumulator as an exception when a timeout occurs. Therefore, a parallelReduce that uses this branch must be inside of a try statement. For example,

try {
  const [ x, y, z ] =
    parallelReduce([ 1, 2, 3 ])
    ...
    .throwTimeout(deadline)
} catch (e) { ... } 

will expand throwTimeout to:

.timeout(deadline, () => {
  throw [ x, y, z ]; }) 

A parallel reduce statement is essentially an abbreviation of pattern of a while loop combined with a fork statement that you could write yourself. This is an extremely common pattern in decentralized applications.

The idea is that there are some values (the LHS) which after intialization will be repeatedly updated uniquely by each of the racing participants until the condition does not hold.

var LHS = INIT_EXPR;
invariant(INVARIANT_EXPR)
while(COND_EXPR) {
  fork()
  .case(PART_EXPR,
    PUBLISH_EXPR,
    PAY_EXPR,
    (m) => {
      LHS = CONSENSUS_EXPR(m);
      continue; })
  .timeout(DELAY_EXPR, () =>
    TIMEOUT_BLOCK);
}

5.4.5.2 Expressions

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

5.4.5.2.1 this

Inside of a consensus step, this refers to the address of the participant that performed the consensus transfer. This is useful when the consensus transfer was initiated by a race expression.

5.4.5.2.2 transfer

transfer(10).to(Alice);
transfer(2, gil).to(Alice); 

A transfer expression, written transfer(AMOUNT_EXPR).to(PART), where AMOUNT_EXPR is an expression that evaluates to an unsigned integer, 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 also be written transfer(AMOUNT_EXPR, TOKEN_EXPR).to(PART), where TOKEN_EXPR is a Token, which transfers non-network tokens of the specified type.

A transfer expression may only occur within a consensus step.

5.4.5.2.3 require

require( claim, [msg] ) 

A requirement where claim evaluates to true with honest participants. This may only appear in a consensus step. It accepts an optional bytes argument, which is included in any reported violation.

5.4.5.2.4 checkCommitment

checkCommitment( commitment, salt, x ) 

Makes a requirement that commitment is the digest of salt and x. This is used in a consensus step after makeCommitment was used in a local step.

5.4.5.2.5 Remote objects

const randomOracle =
  remote( randomOracleAddr, {
    getRandom: Fun([], UInt),
  });
const randomVal = randomOracle.getRandom.pay(randomFee)();

A remote object is representation of a foreign contract in a Reach application. During a consensus step, a Reach computation may consensually communicate with such an object via a prescribed interface.

A remote object is constructed by calling the remote function with an address and an interface—an object where each key is bound to a function type. For example:

const randomOracle =
  remote( randomOracleAddr, {
    getRandom: Fun([], UInt),
  });
const token =
  remote( tokenAddr, {
    balanceOf: Fun([Address], UInt),
    transferTo: Fun([UInt, Addres], Null),
  });

Once constructed, the fields of a remote object represent those remote contract interactions, referred to as remote functions. For example, randomOracle.getRandom, token.balanceOf, and token.transferTo are remote functions in the example.

A remote function may be invoked by calling it with the appropriate arguments, whereupon it returns the specified output. In addition, a remote function may be augmented with one of the following operations:

5.4.5.2.6 Mappings: creation and modification

const bidsM = new Map(UInt);
bidsM[this] = 17;
delete bidsM[this];

A new mapping of linear state may be constructed in a consensus step by writing new Map(TYPE_EXPR), where TYPE_EXPR is some type.

This returns a value which may be used to dereference particular mappings via map[ADDR_EXPR], where ADDR_EXPR is an address. Such dereferences return a value of type Maybe(TYPE_EXPR), because the mapping may not contain a value for ADDR_EXPR.

A mapping may be modified by writing map[ADDR_EXPR] = VALUE_EXPR to install VALUE_EXPR (of type TYPE_EXPR) at ADDR_EXPR, or by writing delete map[ADDR_EXPR] to remove the mapping entry. Such modifications may only occur in a consensus step.

5.4.5.2.7 Sets: creation and modification

const bidders = new Set();
bidders.insert(Alice);
bidders.remove(Alice);
bidders.member(Alice); // false

A Set is another container for linear state. It is simply a type alias of Map(Null); it is only useful for tracking Addresses. Because a Set is internally a Map, it may only be constructed in a consensus step.

A Set may be modified by writing s.insert(ADDRESS) to install ADDRESS in the set, s, or s.remove(ADDRESS) to remove the ADDRESS from the set. Such modifications may only occur in a consensus step.

s.member(ADDRESS) will return a Bool representing whether the address is in the set.