5.4.6 Computations
This section describes the common features available in all Reach contexts.
5.4.6.1 Comments
// singleline comment
/* multiline
* comment
*/
Comments are text that is ignored by the compiler. Text starting with // up until the end of the line forms a singleline comment. Text enclosed with /* and */ forms a multiline comment. It is invalid to nest a multiline comment within a multiline comment.
5.4.6.2 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 }.
5.4.6.3 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.
5.4.6.3.1 const and function
An identifier definition is either a value definition or a function definition. Each of these introduces one or more bound identifiers.
—
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›  ::=  ‹id› 

   [ ‹LHStupleseq› ] 

   { ‹LHSobjseq› } 
 ‹LHStupleseq›  ::=  

   ... ‹LHS› 

   ‹LHS› 

   ‹LHS› , ‹LHStupleseq› 
 ‹LHSobjseq›  ::=  

   ... ‹LHS› 

   ‹LHSobjelem› 

   ‹LHSobjelem› , ‹LHSobjseq› 
 ‹LHSobjelem›  ::=  ‹id› 

   ‹propertyName› : ‹LHS› 
 ‹propertyName›  ::=  ‹id› 

   ‹string› 

   ‹number› 

   [ ‹expr› ] 
RHS
must be compatible with the given LHS
.
That is, if a LHS
is an ‹LHStupleseq›, then the corresponding RHS
must be a tuple with the correct number of elements.
If a LHS
is an ‹LHSobjseq›, 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.
—
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 lefthand sides LHS_0
through LHS_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,
is invalid. This restriction is independent of whether a binding is only known to a single participant. For example,
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];
5.4.6.3.2 return
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,
is invalid, because the first return
’s tail is not empty.
5.4.6.3.3 if
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,
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.
5.4.6.3.4 switch
const mi = Maybe(UInt).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(UInt)
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
).
5.4.6.3.5 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,
evaluates to 4
, but
is erroneous, because the identifier x
is not bound outside the block statement.
5.4.6.3.6 Expression statements
4;
f(2, true);
An expression, E
, in a statement position is equivalent to the block statement { return E; }
.
5.4.6.4 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.
5.4.6.4.1 Identifier reference
X
Y
Z
An identifier, written ID
, is an expression that evaluates to the value of the bound identifier.
The identifier this
has a special meaning inside of a local step (i.e. the body of an only
or each
expression), as well as in a consensus step (i.e. the tail of publish
or pay
statement and before a commit
statement). For details, see this and this.
5.4.6.4.2 Function application
assert( amount <= heap1 )
step( moveA )
digest( coinFlip )
interact.random()
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.
5.4.6.4.3 Types
Reach’s types are represented with programs by the following identifiers and constructors:
UInt
, which denotes an unsigned integer.UInt.max
is the largest value that may be assigned to aUInt
.Bytes(length)
, which denotes a string of bytes of length at mostlength
.Digest
, which denotes a digest.Fun([Domain_0, ..., Domain_N], Range)
, which denotes a function type.Tuple(Field_0, ..., FieldN)
, which denotes a tuple. (Refer to Tuples for constructing tuples.)Object({key_0: Type_0, ..., key_N: Type_N})
, which denotes an object. (Refer to Objects for constructing objects.)Array(ElementType, size)
, which denotes a staticallysized array. (Refer to array for constructing arrays.)Data({variant_0: Type_0, ..., variant_N: Type_N})
, which denotes a tagged union (or sum type). (Refer to Data for constructing data instances.)
Object
and Data
are commonly used to implemented algebraic data types in Reach.
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.
5.4.6.4.4 Literal values
10
0xdeadbeef
007
10
34.5432
true
false
null
"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.
Numeric literals must obey the bit width of UInt
if they are used as UInt
values at runtime, but if they only appear at compiletime, then they may be any positive number.
Reach provides abstractions for working with Int
s and signed FixedPoint
numbers.
Int
s may be defined by applying the unary +
and 
operators to values of type UInt
.
Reach provides syntactic sugar for defining signed FixedPoint
numbers, in base 10, with decimal syntax.
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.
5.4.6.4.5 Operator expression
An operator is a special identifier, which is either a unary operator, or a binary operator.
—
A unary expression, written UNAOP EXPR_rhs
, where EXPR_rhs
is an expression and UNAOP
is one of the unary operators: !  + typeof. All the unary operators, besides typeof
, have a
corresponding named version in the standard library.
It is invalid to use unary operations on the wrong types of values.
When applied to values of type UInt
, unary 
and +
operators will cast
their arguments to type Int
. The unary 
and +
operations are defined for
values of type: Int
, and FixedPoint
.
—
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 ===
) and !=
(and !==
) operate on all atomic values.
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 corresponding named function in the standard library.
While &&
and 
may not evaluate their second argument,
their corresponding named functions and
and or
, always do.
polyEq(a, b) // eq on all types
boolEq(a, b) // eq on Bool
typeEq(a, b) // eq on types
intEq(a, b) // eq on UInt
digestEq(a, b) // eq on Digest
addressEq(a, b) // eq on Addresses
fxeq(a, b) // eq on FixedPoint
ieq(a, b) // eq on Int
==
is a function which operates on all types.
Both arguments must be of the same type.
Specialized functions exist for equality checking on each supported type.
—
If verifyArithmetic
is true
, then arithmetic operations automatically make a static assertion that their arguments would not overflow the bit width of the enable consensus networks.
If it is false
, then the connector will ensure this dynamically.
5.4.6.4.6 xor
xor(false, false); // false
xor(false, true); // true
xor(true, false); // true
xor(true, true); // false
xor(Bool, Bool)
returns true
only when the inputs differ in value.
5.4.6.4.7 Parenthesized expression
An expression may be parenthesized, as in (EXPR)
.
5.4.6.4.8 Tuples
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.
5.4.6.4.9 array
Converts a tuple of homogeneous values of the specific type into an array.
5.4.6.4.10 Element reference
arr[3]
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.
5.4.6.4.11 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.
5.4.6.4.12 Array & tuple update: Tuple.set, Array.set, and .set
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.
5.4.6.4.13 Array group operations
Array.iota
Array.iota(5)
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 compiletime.
Array.replicate && .replicate
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 compiletime.
Array.concat && .concat
Array.concat(x, y)
concatenates the two arrays x
and y
.
This may be abbreviated as x.concat(y)
.
Array.empty
Array_empty
Array.empty
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 && .zip
Array.zip(x, y)
returns a new array the same size as x
and y
(which must be the same size) whose elements are tuples of the elements of x
and y
.
This may be abbreviated as x.zip(y)
.
Array.map && .map
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 && .reduce
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)
.
Array.forEach && .forEach
Array.forEach(arr, f)
iterates the function f
over the elements of the array arr
, discarding the result.
This may be abbreviated as arr.forEach(f)
.
Array.all && .all
Array.all(arr, f)
determines whether the predicate, f, is satisfied
by every element of the array, arr.
Array.any && .any
Array.any(arr, f)
determines whether the predicate, f, is satisfied
by at least one element of the array, arr.
Array.or && .or
Array.or(arr)
returns the disjunction of an array of Bool
s.
Array.and && .and
Array.and(arr)
returns the conjunction of an array of Bool
s.
Array.includes && .includes
Array.includes(arr, x)
determines whether the array includes
the element, x.
Array.indexOf && .indexOf
Array.indexOf(arr, x)
returns the index of the first element
in the given array that is equal to x. The return value is of type Maybe(UInt)
. If
the value is not present in the array, None
is returned.
Array.findIndex && .findIndex
Array.findIndex(arr, f)
returns the index of the first element
in the given array that satisfies the predicate f. The return value is of type Maybe(UInt)
. If
no value in the array satisfies the predicate, None
is returned.
Array.count && .count
Array.count(arr, f)
returns the number of elements in arr that
satisfy the predicate, f.
Array.min && .min
Array.min(arr)
returns the lowest number in an array of UInts.
Array.max && .max
Array.max(arr)
returns the largest number in an array of UInts.
Array.sum && .sum
Array.sum(arr)
returns the sum of an array of UInts.
Array.product && .product
Array.product(arr)
returns the product of an array of UInts.
Array.average && .average
Array.average(arr)
returns the mean of an array of UInts.
5.4.6.4.14 Objects
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.
5.4.6.4.15 Field reference
obj.x
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.
5.4.6.4.16 Object.set
Returns a new object identical to obj
,
except that field fld
is replaced with val
.
5.4.6.4.17 Object.setIfUnset
Object.setIfUnset(obj, fld, val);
Object_setIfUnset(obj, fld, val);
Returns a new object identical to obj
,
except that field fld
is val
if fld
is not already present in obj
.
5.4.6.4.18 Object.has
Object.has(obj, fld);
Returns a boolean indicating whether the object has the field fld
. This is statically known.
5.4.6.4.19 Data
const Taste = Data({Salty: Null,
Spicy: Null,
Sweet: Null,
Umami: Null});
const burger = Taste.Umami();
const Shape = Data({ Circle: Object({r: UInt}),
Square: Object({s: UInt}),
Rect: Object({w: UInt, h: UInt}) });
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.
5.4.6.4.20 Maybe
const MayInt = Maybe(UInt);
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 builtin Data
type, Maybe
, which has two variants: Some
and None
.
Maybe
is defined by
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
.
isNone
is a convenience method that determines whether the variant is isNone.
isSome
is a convenience method that determines whether the variant is isSome.
5.4.6.4.21 Either
Either
is defined by
Either
can be used to represent values with two possible types.
Similar to Maybe, Either may be used to represent values that are correct or erroneous. A successful result is stored, by convention, in Right. Unlike None, Left may carry additional information about the error.
either(e, onLeft, onRight)
For an Either value, e, either
will either apply the function onLeft or onRight to the appropriate variant value.
const e = Either(UInt, Bool);
const l = e.Left(1);
const r = e.Right(true);
isLeft(l); // true
isRight(l); // false
const x = fromLeft(l, 0); // x = 1
const y = fromRight(l, false); // y = false
isLeft
is a convenience method that determines whether the variant is Left.
isRight
is a convenience method that determines whether the variant is Right.
fromLeft(e, default)
is a convenience method that returns the value in Left,
or default if the variant is Right.
fromRight(e, default)
is a convenience method that returns the value in Right,
or default if the variant is Left.
5.4.6.4.22 match
const Value = Data({
EBool: Bool,
EInt: UInt,
ENull: Null,
});
const v1 = Value.EBool(true);
const v2 = Value.EInt(200);
const isTruthy = (v) =>
v.match({
EBool: (b) => { return b },
EInt : (i) => { return i != 0 },
ENull: () => { return false }
});
assert(isTruthy(v1));
assert(isTruthy(v2));
A match expression, written VAR.match({ CASE ... })
, where VAR is a variable
bound to a data instance and CASE is VARIANT: FUNCTION, where VARIANT is a
variant or default
, and FUNCTION is a function that takes the same parameters as the
variant constructor, or no parameters if the variant has a type of Null
.
match
is similar to a switch statement, but since it is an expression, it
can be conveniently used in places like the right hand side of an assignment statement.
Similar to a switch statement, the cases are expected to be exhaustive and nonredundant, all cases have empty tails, and it may only include a consensus transfer in its cases if it is within a consensus step.
5.4.6.4.23 Conditional expression
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
.
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.
5.4.6.4.24 Arrow expression
(() => 4)
((x) => x + 1)
((x) => { const y = x + 1;
return y + 1; })
((x, y) => { assert(x + y == 3); })(1, 2);
((x, y) => { assert(x + y == 3); })(...[1, 2]);
(([x, y]) => { assert(x + y == 3); })([1, 2]);
(({x, y}) => { assert(x + y == 3); })({x: 1, y: 2});
(([x, [y]]) => { assert(x + y == 3); })([1,[2]]);
(([x, {y}]) => { assert(x + y == 3); })([1,{ y: 2 }]);
An arrow expression, written (LHS_0, ..., LHS_n) => EXPR
, where LHS_0
through LHS_n
are lefthand sides and EXPR
is an expression, evaluates to an function which is an abstraction of EXPR
over n
values compatible with the respective lefthand side.
5.4.6.4.25 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([UInt], Bool)
which tells you if its argument is one of the enum’s values,
and the next N values are distinct UInt
s.
5.4.6.4.26 assert
The Reach compiler will produce a counterexample (i.e. an assignment of the identifiers in the program to falsify the
claim
) when an invalidclaim
is provided. It is possible to write aclaim
that actually always evaluates totrue
, but for which our current approach cannot prove always evaluates totrue
; if this is the case, Reach will fail to compile the program, reporting that its analysis is incomplete. Reach will never produce an erroneous counterexample.
See the guide section on verification to better understand how and what to verify in your program.
5.4.6.4.27 forall
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
5.4.6.4.28 possible
A possibility assertion which is only valid if it is possible for claim
to evaluate to true
with honest frontends and participants.
It accepts an optional bytes argument, which is included in any reported violation.
5.4.6.4.29 digest
The digest primitive performs a cryptographic hash of the binary encoding of the given arguments.
This returns a Digest
value.
The exact algorithm used depends on the connector.
5.4.6.4.30 balance
The balance primitive returns the balance of the contract account for the DApp.
5.4.6.4.31 lastConsensusTime
The lastConsensusTime primitive returns the time of the last publication of the DApp.
This may not be available if there was no such previous publication, such as at the beginning of an application where deployMode
is 'firstMsg'
.
Why is there no thisConsensusTime? Some networks do not support observing the time of a consensus operation until after it has finalized. This aides scalability, because it increases the number of times when an operation could be finalized.
5.4.6.4.32 makeDeadline
const [ timeRemaining, keepGoing ] = makeDeadline(10);
makeDeadline(deadline)
takes an UInt
as an argument and returns a pair of functions
that can be used for dealing with absolute deadlines. It internally determines the end time based off of the deadline
and the last consensus time—at the time of calling makeDeadline
. timeRemaining will calculate the difference
between the end time and the current last consensus time. keepGoing determines whether the current last consensus time
is less than the end time. It is typical to use the two fields for the while and timeout field of a parallel_reduce
expression. For example:
const [ timeRemaining, keepGoing ] = makeDeadline(10);
const _ = parallel_reduce(...)
.invariant(...)
.while( keepGoing() )
.case(...)
.timeout( timeRemaining(), ...)
5.4.6.4.33 implies
Returns true
if x
is false
or y
is true
.
5.4.6.4.34 ensure
Makes a static assertion that pred(x)
is true
and returns x
.
5.4.6.4.35 hasRandom
A participant interact interface which specifies random as a function that takes no arguments and returns an unsigned integer of bit width bits.
5.4.6.4.36 compose
Creates a new function that applies it’s argument to g, then pipes the result to the function f. The argument type of f must be the return type of g.
5.4.6.4.37 sqrt
Calculates an approximate square root of the first argument. This method utilizes
the Babylonian Method for computing
the square root. The second argument must be an UInt
whose value is known at compile time, which represents the number
of iterations the algorithm should perform.
For reference, when performing 5
iterations, the algorithm can reliably calculate the square root
up to 32 squared, or 1,024. When performing 10
iterations, the algorithm can reliably calculate the
square root up to 580 squared, or 336,400.
5.4.6.4.38 pow
pow(base, power, precision)
Calculates the approximate value of raising base to power.
The third argument must be an UInt
whose value is known at compile time, which represents the number
of iterations the algorithm should perform. For reference, 6 iterations provides enough accuracy to calculate
up to 2^64  1, so the largest power it can compute is 63.
5.4.6.4.39 Signed Integers
The standard library provides abstractions for dealing with signed integers. The following definitions
are used to represent Int
s:
Int is represented as an object, as opposed to a scalar value, because some platforms that Reach targets do not provide native support for signed integers.
int(Bool, UInt)
is shorthand for defining an Int
record. You may also
use the +
and 
unary operators to declare integers instead of UInt
s.
int(Pos, 4); // represents 4
int(Neg, 4); // represents 4
4; // represents 4
+4; // represents 4 : Int
4; // represents 4 : UInt
iadd(x, y)
adds the Int
x and the Int
y.
isub(x, y)
subtracts the Int
y from the Int
x.
imul(x, y)
multiplies the Int
x and the Int
y.
idiv(x, y)
divides the Int
x by the Int
y.
imod(x, y)
finds the remainder of dividing the Int
x by the Int
y.
ilt(x, y)
determines whether x is less than y.
ile(x, y)
determines whether x is less than or equal to y.
igt(x, y)
determines whether x is greather than y.
ige(x, y)
determines whether x is greater than or equal to y.
ieq(x, y)
determines whether x is equal to y.
ine(x, y)
determines whether x is not equal to y.
5.4.6.4.40 FixedPoint Numbers
FixedPoint
is defined by
FixedPoint
can be used to represent numbers with a fixed number of digits after the decimal point.
They are handy for representing fractional values, especially in base 10. The value of a fixed point number is determined
by dividing the underlying integer value, i, by its scale factor, scale. For example, we could
represent the value 1.234
with { sign: Pos, i: { scale: 1000, i : 1234 } }
or fx(1000)(Pos, 1234)
.
Alternatively, Reach provides syntactic sugar for defining FixedPoint
numbers. One can simply write
1.234
, which will assume the value is in base 10. A scale factor of 1000 correlates to 3 decimal
places of precision. Similarly, a scale factor of 100 would have 2 decimal places of precision.
fx(scale)(i)
will return a function that can be used to
instantiate fixed point numbers with a particular scale factor.
fxint(Int)
will cast the Int
arg as a FixedPoint
number with a scale of 1.
fxrescale(x, scale)
will convert a fixed point number from using
one scale to another. This operation can result in loss of precision, as demonstrated in the above example.
const x = fx(1000)(Pos, 824345); // x = 824.345
const y = 45.67;
fxunify(x, y); // => [ 1000, 824.345, 45.670 ]
fxunify(x, y)
will convert the fixed point numbers
to use the same scale. The larger scale of the two arguments will be chosen. The function will return a 3tuple consisting
of the common scale and the newly scaled values.
fxadd(x, y)
adds two fixed point numbers.
fxsub(x, y)
subtracts two fixed point numbers.
fxmul(x, y)
multiplies two fixed point numbers.
fxdiv(34.56, 1.234, 10) // => 28
fxdiv(34.56, 1.234, 100000) // => 28.0064
fxdiv(x, y, scale_factor)
divides two fixed point numbers. The numerator, x,
will be multiplied by the scale factor to provide a more precise answer. For example,
fxmod(x, y)
finds the remainder of dividing x by y.
fxfloor(x)
returns the greatest integer not greater than x.
fxsqrt(x, k)
approximates the sqrt of the fixed number, x, using
k iterations of the sqrt
algorithm.
const base = 2.0;
const power = 0.33;
fxpow(base, power, 10, 1000); // 1.260
fxpow(base, power, 10, 10000); // 1.2599
fxpow(base, power, 10, 1000000); // 1.259921
fxpow(base, power, precision, scalePrecision)
approximates the power of the fixed number, base,
raised to the fixed point number, power. The third argument must be an UInt
whose value is known
at compile time, which represents the number of iterations the algorithm should perform.
The scalePrecision argument must be a UInt and represents the scale of the return value. Choosing a larger
scalePrecision allows for more precision when approximating the power, as demonstrated in the example below:
fxpowi(base, power, precision)
approximates the power of the fixed number, base,
raised to the Int
, power. The third argument must be an UInt
whose value is known
at compile time, which represents the number of iterations the algorithm should perform. For reference, 6 iterations
provides enough accuracy to calculate up to 2^64  1, so the largest power it can compute is 63.
fxpowui(5.8, 3, 10); // 195.112
fxpowui(base, power, precision)
approximates the power of
the fixed number, base, raised to the UInt
, power. The third
argument must be an UInt
whose value is known at compile time.
fxcmp(op, x, y)
applies the comparison
operator to the two fixed point numbers after unifying their scales.
There are convenience methods defined for comparing fixed point numbers:
fxlt(x, y)
tests whether x is less than y.
fxle(x, y)
tests whether x is less than or equal to y.
fxgt(x, y)
tests whether x is greater than y.
fxge(x, y)
tests whether x is greater than or equal to y.
fxeq(x, y)
tests whether x is equal to y.