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.2 Modules
On this page: Statements export
export import
from Expressions Reach.App
deploy  Mode
verify  Arithmetic
verify  Per  Connector
ALGO Participant Constructors
Participant  Class
5.4.2 Modules

A Reach source file is a textual file which specifies a Reach module. It is traditionally given the file extension rsh, e.g. "dao.rsh".

A module starts with 'reach 0.1'; followed by a sequence of imports and identifier definitions. A module can only be compiled or used if it contain one or more exports.

See the guide section on versions to understand how Reach uses version numbers like this. Statements

Any statements valid for a computation are valid for a module. However, some additional statements are allowed. export

Module-level identifier definitions may be exported by writing export in front of them. For example,

export const x = 1;
export const [a, b, ...more] = [ 0, 1, 2, 3, 4 ];
export function add1(x) { return x + 1; };
are valid exports.

Module-level identifiers may also be exported after the fact, and may be renamed during export. For example:

const w = 2;
const z = 0;
export {w, z as zero};

Identifiers from other modules may be re-exported (and renamed), even if they are not imported in the current module. For example:

export {u, x as other_x} from './other-module.rsh';

An exported identifier in a given module may be imported by other modules. import

import 'games-of-chance.rsh';

When a module, X, contains an import, written import "LIB.rsh";, then the path "LIB.rsh" must resolve to another Reach source file. The exports from the module defined by "LIB.rsh" are included in the set of bound identifiers in X.

import {flipCoin, rollDice as d6} from 'games-of-chance.rsh';

Import statements may limit or rename the imported identifiers.

import * as gamesOfChance from 'games-of-chance.rsh';

Imports may instead bind the entire module to a single identifier, which is an object with fields corresponding to that module’s exports.

Import cycles are invalid.

The path given to an import may not include .. to specify files outside the current directory nor may it be an absolute path.

It must be a relative path, which is resolved relative to the parent directory of the source file in which they appear. Expressions

Any expressions valid for a computation are valid for a module. However, some additional expressions are allowed. Reach.App

export const main =
  Reach.App({}, [Participant("A", {displayResult: Fun(Int, Null)})], (A) => {
    const result = 0;
    A.only(() => { interact.displayResult(result); })
    return result;

Reach.App is a function which accepts three arguments: options, participantDefinitions, and program.

The options must be an object. It supports the following options:



'constructor' (default) or 'firstMsg'


Determines whether contract should be deployed independently ('constructor') or as part of the first publication ('firstMsg'). If deployed as part of the first publication, then the first publication must precede all uses of wait and .timeout. See the guide on deployment modes for a discussion of why to choose a particular mode.








true or false (default)


Determines whether arithmetic operations automatically introduce static assertions that they do not overflow beyond UInt.max. This defaults to false, because it is onerous to verify. We recommend turning it on before final deployment, but leaving it off during development. When it is false, connectors will ensure that overflows do not actually occur on the network.








true or false (default)


Determines whether verification is done per connector, or once for a generic connector. When this is true, then connector-specific constants, like UInt.max, will be instantiated to literal numbers. This concretization of these constants can induce performance degradation in the verifier.








[ETH, ALGO] (default)


A tuple of the connectors that the application should be compiled for. By default, all available connectors are chosen.

The participantDefinitions argument is a tuple of participant constructors.

The program argument must be a syntactic arrow expression. The arguments to this arrow must match the number and order of participantDefinitions. The function body is the program to be compiled. It specifies a step, which means its content is specified by Steps. When it returns, it must be in a step, as well; which means that its content cannot end within a consensus step.

If the result of Reach.App is eventually bound to an identifier that is exported, then it may be a target given to the compiler, as discussed in the section on usage. Participant Constructors

A participant constructor is used for declaring a logical actor in a Reach program. A participant and participant class may be declared with

Participant(participantName, participantInteractInterface)


ParticipantClass(participantName, participantInteractInterface)


participantName is a string which indicates the name of the participant function in the generated backend code. Each participantName must be unique.

participantInteractInterface is a participant interact interface, an object where each field indicates the type of a function or value which must be provided to the backend by the frontend for interacting with the participant.