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
5.4.6 Computations
On this page: Comments Blocks Statements const and function
function return
return if
else switch
default Block statements Expression statements Expressions Identifier reference Function application Types
type  Of
is  Type Literal values
null Operator expression
poly  Eq
poly  Neq
bool  Eq
bytes  Eq
type  Eq
int  Eq Parenthesized expression Tuples array
array Element reference Array & tuple length:   Tuple.length, Array.length, and .length
length Array & tuple update:   Tuple.set, Array.set, and .set
set Array group operations:   Array.iota, Array.concat & .concat, Array.empty, Array.zip & .zip, Array.map & .map, Array.reduce & .reduce, and Array.replicate
reduce Objects Field reference Object.set
Object_  set Data Maybe
from  Maybe Conditional expression
ite Arrow expression
=> make  Enum
make  Enum assert
assert forall
forall possible
possible digest
digest balance
balance implies
implies ensure
ensure has  Random
has  Random
5.4.6 Computations

This section describes the common features available in all Reach contexts. Comments

// single-line comment
/* multi-line
 * comment

Comments are text that is ignored by the compiler. Text starting with // up until the end of the line forms a single-line comment. Text enclosed with /* and */ forms a multi-line comment. It is invalid to nest a multi-line comment within a multi-line comment. Blocks

{ return 42; }
{ const x = 31;
  return x + 11; }
{ if ( x < y ) {
    return "Why";
  } else {
    return "Ecks"; } } 

A block is a sequence of statements surrounded by braces, i.e. { and }. Statements

This section describes the statements which are allowed in any Reach context.

Each statement affects the meaning of the subsequent statements, which is called its tail. For example, if {X; Y; Z;} is a block, then X’s tail is {Y; Z;} and Y’s tail is {Z;}.

Distinct from tails are continuations which include everything after the statement. For example, in {{X; Y;}; Z;}, X’s tail is just Y, but its continuation is {Y;}; Z;.

Tails are statically apparent from the structure of the program source code, while continuations are influenced by function calls.

A sequence of statements that does not end in a terminator statement (a statement with no tail), such as a return statement, continue statement, or exit statement is treated as if it ended with return null;.

The remainder of this section enumerates each kind of statement. const and function

An identifier definition is either a value definition or a function definition. Each of these introduces one or more bound identifiers.

const DELAY = 10;
const [ Good, Bad ] = [ 42, 43 ]; 

Valid identifiers follow the same rules as JavaScript identifiers: they may consist of Unicode alphanumeric characters, or _ or $, but may not begin with a digit.

A value definition is written const LHS = RHS;.

LHS must obey the grammar:







[ LHS-tuple-seq ]



{ LHS-obj-seq }






... LHS






LHS , LHS-tuple-seq






... LHS






id , LHS-obj-seq

RHS must be compatible with the given LHS. That is, if a LHS is an LHS-tuple-seq, then the corresponding RHS must be a tuple with the correct number of elements. If a LHS is an LHS-obj-seq, then the corresponding RHS must be an object with the correct fields.

Those values are available as their corresponding bound identifiers in the statement’s tail.

function randomBool() {
  return (interact.random() % 2) == 0; }; 

A function definition, written function FUN(ARG_0, ..., ARG_n) BLOCK;, defines FUN as a function which abstracts its function body, the block BLOCK, over the identifiers ARG_0 through ARG_n.

All identifiers in Reach programs must be unbound at the position of the program where they are bound, i.e., it is invalid to shadow identifiers with new definitions. For example,

const x = 3;
const x = 4; 

is invalid. This restriction is independent of whether a binding is only known to a single participant. For example,

Alice.only(() => {
  const x = 3; });
Bob.only(() => {
  const x = 3; }); 

is invalid.

The special identifier _ is an exception to this rule. The _ binding is always considered to be unbound. This means means that _ is both an identifier that can never be read, as well as an identifier that may be bound many times. This may be useful for ignoring unwanted values, for example:

const [_, x, _] = [1, 2, 3]; return

return 17;
return 3 + 4;
return f(2, false);

A return statement, written return EXPR;, where EXPR is an expression evaluates to the same value as EXPR. As a special case, return; is interpreted the same as return null;.

A return statement returns its value to the surrounding function application.

A return statement is a terminator statement, so it must have an empty tail. For example,

{ return 1;
  return 2; } 

is invalid, because the first return’s tail is not empty. if

if ( 1 + 2 < 3 ) {
  return "Yes!";
} else {
  return "No, waaah!"; } 

A conditional statement, written if (COND) NOT_FALSE else FALSE, where COND is an expression and NOT_FALSE and FALSE as statements (potentially block statements), selects between the NOT_FALSE statement and FALSE statement based on whether COND evaluates to false.

Both NOT_FALSE and FALSE have empty tails, i.e. the tail of the conditional statement is not propagated. For example,

if ( x < y ) {
  const z = 3; }
else {
  const z = 4; }
return z; 

is erroneous, because the identifier z is not bound outside the conditional statement.

A conditional statement may only include a consensus transfer in NOT_FALSE or FALSE if it is within a consensus step, because its statements are in the same context as the conditional statement itself. switch

const mi = Maybe(UInt256).Some(42);
switch ( mi ) {
 case None: return 8;
 case Some: return mi + 10; }
switch ( mi ) {
 case None: return 8;
 default: return 41; } 

A switch statement, written switch (VAR) { CASE ... }, where VAR is a variable bound to a data instance and CASE is either case VARIANT: STMT ..., where VARIANT is a variant, or default: STMT ..., STMT is a sequence of statements, selects the appropriate sequence of statements based on which variant VAR holds. Within the body of a switch case, VAR has the type of variant; i.e. in a Some case of a Maybe(UInt256) switch, the variable is bound to an integer.

All cases have empty tails, i.e. the tail of the switch statement is not propagated.

A switch statement may only include a consensus transfer in its cases if it is within a consensus step, because its statements are in the same context as the conditional statement itself.

It is invalid for a case to appear multiple times, or be missing, or to be superfluous (i.e. for a variant that does not exist in the Data type of VAR). Block statements

A block statement is when a block occurs in a statement position, then it establishes a local, separate scope for the definitions of identifiers within that block. In other words, the block is evaluated for effect, but the tail of the statements within the block are isolated from the surrounding tail. For example,

const x = 4;
return x; 

evaluates to 4, but

{ const x = 4; }
return x; 

is erroneous, because the identifier x is not bound outside the block statement. Expression statements

f(2, true); 

An expression, E, in a statement position is equivalent to the block statement { return E; }. Expressions

This section describes the expressions which are allowed in any Reach context. There are a large variety of different expressions in Reach programs.

The remainder of this section enumerates each kind of expression. Identifier reference


An identifier, written ID, is an expression that evaluates to the value of the bound identifier. Function application

assert( amount <= heap1 )
step( moveA )
digest( coinFlip )
declassify( _coinFlip ) 

A function application, written EXPR_rator(EXPR_rand_0, ..., EXPR_rand_n), where EXPR_rator and EXPR_rand_0 through EXPR_rand_n are expressions that evaluate to one value. EXPR_rator must evaluate to an abstraction over n values or a primitive of arity n. A spread expression (...expr) may appear in the list of operands to a function application, in which case the elements of the expr are spliced in place. Types

Reach’s types are represented with programs by the following identifiers and constructors:

Object and Data are commonly used to implemented algebraic data types in Reach.

typeOf(x)  // type
isType(t) // Bool

The typeOf primitive function is the same as typeof: it returns the type of its argument. The isType function returns true if its argument is a type. Any expression satisfying isType is compiled away and does not exist at runtime. Literal values

"reality bytes"
'it just does' 

A literal value, written VALUE, is an expression that evaluates to the given value. The null literal may be written as null. Numeric literals may be written in decimal, hexadecimal, or octal. Boolean literals may be written as true or false. String literals (aka byte strings) may be written between double or single quotes (with no distinction between the different styles) and use the same escaping rules as JavaScript. Operator expression

An operator is a special identifier, which is either a unary operator, or a binary operator.

! a
- a
typeof a

A unary expression, written UNAOP EXPR_rhs, where EXPR_rhs is an expression and UNAOP is one of the unary operators: ! - typeof.

It is invalid to use unary operations on the wrong types of values.

a && b
a || b
a + b
a - b
a * b
a / b
a % b
a | b
a & b
a ^ b
a << b
a >> b
a == b
a != b
a === b
a !== b
a > b
a >= b
a <= b
a < b 

Bitwise operations are not supported by all consensus networks and greatly decrease the efficiency of verification.

A binary expression, written EXPR_lhs BINOP EXPR_rhs, where EXPR_lhs and EXPR_rhs are expressions and BINOP is one of the binary operators: && || + - * / % | & ^ << >> == != === !== > >= <= <. The operators == and != operate on numbers, while the operators === and !== operate on byte strings. Numeric operations, like + and >, only operate on numbers. Since all numbers in Reach are integers, operations like / truncate their result. Boolean operations, like &&, only operate on booleans. It is invalid to use binary operations on the wrong types of values.

and(a, b)     // &&
or(a, b)      // ||
add(a, b)     // +
sub(a, b)     // -
mul(a, b)     // *
div(a, b)     // /
mod(a, b)     // %
lt(a, b)      // <
le(a, b)      // <=
ge(a, b)      // >=
gt(a, b)      // >
lsh(a, b)     // <<
rsh(a, b)     // >>
band(a, b)    // &
bior(a, b)    // |
bxor(a, b)    // ^
polyEq(a, b)  // ==, ===
polyNeq(a, b) // !=, !==

All binary expression operators have a corresponidng named function in the standard library. Note that while && and || may not evaluate their second argument, their corresponding named functions and and or, always do.

polyEq(a, b)  // eq on Bool, Bytes, types, or UInt256
boolEq(a, b)  // eq on Bool
bytesEq(a, b) // eq on Bytes
typeEq(a, b)  // eq on types
intEq(a, b)   // eq on UInt256

Note that == is a function which operates on multiple types. Both arguments must be of the same type. Specialized functions exist for equality checking on each supported type. Parenthesized expression

(a + b) - c 

An expression may be parenthesized, as in (EXPR). Tuples

[ ]
[ 1, 2 + 3, 4 * 5 ] 

A tuple literal, written [ EXPR_0, ..., EXPR_n ], is an expression which evaluates to a tuple of n values, where EXPR_0 through EXPR_n are expressions.

...expr may appear inside tuple expressions, in which case the spreaded expression must evaluate to a tuple or array, which is spliced in place. array

const x = array([1, 2, 3]); 

Converts a tuple of homogenueous values into an array. Element reference


A reference, written REF_EXPR[IDX_EXPR], where REF_EXPR is an expression that evaluates to an array or a tuple and IDX_EXPR is an expression that evaluates to a natural number which is less than the size of the array, selects the element at the given index of the array. Indices start at zero. Array & tuple length: Tuple.length, Array.length, and .length


Tuple.length Returns the length of the given tuple.

Array.length Returns the length of the given array.

Both may be abbreviated as expr.length where expr evaluates to a tuple or an array. Array & tuple update: Tuple.set, Array.set, and .set

Tuple.set(tup, idx, val);
tup.set(idx, val);
Array.set(arr, idx, val);
arr.set(idx, val); 

Tuple.set Returns a new tuple identical to tup, except that index idx is replaced with val.

Array.set Returns a new array identical to arr, except that index idx is replaced with val.

Both may be abbreviated as expr.set(idx, val) where expr evaluates to a tuple or an array. Array group operations: Array.iota, Array.concat & .concat, Array.empty, Array.zip & .zip, Array.map & .map, Array.reduce & .reduce, and Array.replicate


Array.iota(len) returns an array of length len, where each element is the same as its index. For example, Array.iota(4) returns [0, 1, 2, 3]. The given len must evaluate to an integer at compile-time.

Array.replicate(5, "five")
Array_replicate(5, "five") 

Array.replicate(len, val) returns an array of length len, where each element is val. For example, Array.replicate(4, "four") returns ["four", "four", "four", "four"]. The given len must evaluate to an integer at compile-time.

Array.concat(x, y)

Array.concat(x, y) concatenates the two arrays x and y. This may be abbreviated as x.concat(y).


Array.empty is an array with no elements. It is the identity element of Array.concat. It may also be written Array_empty.

Array.zip(x, y)

Array.zip(x, y) returns a new array the same size as x and y (which must be thes same size) whose elements are tuples of the elements of x and y. This may be abbreviated as x.zip(y).

Array.map(arr, f)

Array.map(arr, f) returns a new array, arr_mapped, the same size as arr, where arr_mapped[i] = f(arr[i]) for all i. For example, Array.iota(4).map(x => x+1) returns [1, 2, 3, 4]. This may be abbreviated as arr.map(f).

This function is generalized to an arbitrary number of arrays of the same size, which are provided before the f argument. For example, Array.iota(4).map(Array.iota(4), add) returns [0, 2, 4, 6].

Array.reduce(arr, z, f)
arr.reduce(z, f) 

Array.reduce(arr, z, f) returns the left fold of the function f over the given array with the initial value z. For example, Array.iota(4).reduce(0, add) returns ((0 + 1) + 2) + 3 = 6. This may be abbreviated as arr.reduce(z, f).

This function is generalized to an arbitrary number of arrays of the same size, which are provided before the z argument. For example, Array.iota(4).reduce(Array.iota(4), 0, (x, y, z) => (z + x + y)) returns ((((0 + 0 + 0) + 1 + 1) + 2 + 2) + 3 + 3). Objects

{ }
{ x: 3, "yo-yo": 4 }
{ [1 < 2 ? "one" : "two"]: 5 }

An object literal, typically written { KEY_0: EXPR_0, ..., KEY_n: EXPR_n }, where KEY_0 through KEY_n are identifiers or string literals and EXPR_0 through EXPR_n are expressions, is an expression which evaluates to an object with fields KEY_0 through KEY_n.

Additional object literal syntax exists for convenience, such as:

{ ...obj, z: 5 }

An object splice, where all fields from obj are copied into the object; these fields may be accompanied by additional fields specified afterwards.

{ x, z: 5 }

Shorthand for { x: x, z: 5}, where x is any bound identifier. Field reference


An object reference, written OBJ.FIELD, where OBJ is an expression of type object, and FIELD is a valid identifier, accesses the FIELD field of object OBJ. Object.set

Object.set(obj, fld, val);
Object_set(obj, fld, val);
{ ...obj, [fld]: val };

Returns a new object identical to obj, except that field fld is replaced with val. Data

const Taste = Data({Salty: Null,
                    Spicy: Null,
                    Sweet: Null,
                    Umami: Null});
const burger = Taste.Umami();

const Shape = Data({ Circle: Object({r: UInt256}),
                     Square: Object({s: UInt256}),
                     Rect: Object({w: UInt256, h: UInt256}) });
const nice = Shape.Circle({r: 5}); 

A data instance is written DATA.VARIANT(VALUE), where DATA is Data type, VARIANT is the name of one of DATA’s variants, and VALUE is a value matching the type of the variant. As a special case, when the type of a variant is Null, the VALUE may be omitted, as shown in the definition of burger in the same above.

Data instances are consumed by switch statements. Maybe

const MayInt = Maybe(UInt256);
const bidA = MayInt.Some(42);
const bidB = MayInt.None(null);

const getBid = (m) => fromMaybe(m, (() => 0), ((x) => x));
const bidSum = getBid(bidA) + getBid(bidB);
assert(bidSum == 42); 

Option types are represented in Reach through the built-in Data type, Maybe, which has two variants: Some and None.

Maybe is defined by

export const Maybe = (A) => Data({None: Null, Some: A}); 

This means it is a function that returns a Data type specialized to a particular type in the Some variant.

Maybe instances can be conveniently consumed by fromMaybe(mValue, onNone, onSome), where onNone is a function of no arguments which is called when mValue is None, onSome is a function of on argument which is called with the value when mValue is Some, and mValue is a data instance of Maybe. Conditional expression

choosesFirst ? [ heap1 - amount, heap2 ] : [ heap1, heap2 - amount ] 

A conditional expression, written COND_E ? NOT_FALSE_E : FALSE_E, where COND_E, NOT_FALSE_E, and FALSE_E are expressions, selects between the values which NOT_FALSE_E and FALSE_E evaluate to based on whether COND_E evaluates to false.

ite(choosesFirst, [heap1 - amount, heap2], [heap1, heap2 - amount])

Conditional expressions may also be written with the ite function, however, note that this function always evaluates both of its branches, while the regular conditional expression only evaluates one branch. Arrow expression

(() => 4)
((x) => x + 1)
((x) => { const y = x + 1;
          return y + 1; }) 

An arrow expression, written (ID_0, ..., ID_n) => EXPR, where ID_0 through ID_n are identifiers and EXPR is an expression, evaluates to an function which is an abstraction of EXPR over n values. makeEnum

const [ isHand, ROCK, PAPER, SCISSORS ] = makeEnum(3); 

An enumeration (or enum, for short), can be created by calling the makeEnum function, as in makeEnum(N), where N is the number of distinct values in the enum. This produces a tuple of N+1 values, where the first value is a Fun([UInt256], Bool) which tells you if its argument is one of the enum’s values, and the next N values are distinct UInt256s. assert

assert( claim ) 

A static assertion which is only valid if claim always evaluates to true.

The Reach compiler will produce a counter-example (i.e. an assignment of the identifiers in the program to falsify the claim) when an invalid claim is provided. It is possible to write a claim that actually always evaluates to true, but for which our current approach cannot prove always evaluates to true; if this is the case, Reach will fail to compile the program, reporting that its analysis is incomplete. Reach will never produce an erroneous counter-example.

See the guide section on verification to better understand how and what to verify in your program. forall

forall( Type )
forall( Type, (var) => BLOCK ) 

The single argument version returns an abstract value of the given type. It may only be referenced inside of assertions; any other reference is invalid.

The two argument version is an abbreviation of calling the second argument with the result of forall(Type). This is convenient for writing general claims about expressions, such as

forall(UInt256, (x) => assert(x == x)); possible

possible( claim ) 

A possibility assertion which is only valid if it is possible for claim to evaluate to true with honest frontends and participants. digest

digest( arg_0, ..., arg_n ) 

The digest primitive performs a cryptographic hash of the binary encoding of the given arguments, using the Keccak256 algorithm. balance


The balance primitive returns the balance of the contract account for the DApp. implies

implies( x, y ) 

Returns true if x is false or y is true. ensure

ensure( pred, x ) 

Makes a static assertion that pred(x) is true and returns x. hasRandom


A participant interact interface which specifies random as a function that takes no arguments are returns an unsigined integer of 256 bits.