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.1.1 Security levels and scope
5.4.1 Validity

Reach imposes further restrictions on syntactically well-formed programs. These restrictions are described throughout this manual using the term valid to refer to constructions that obey the restrictions, and the term invalid to refer to constructions that do not obey them.

It is always invalid to use a value with an operation for which it is undefined. For example, 1 + true is invalid. In other words, Reach enforces a static type discipline.

5.4.1.1 Security levels and scope

The text of Reach program is public knowledge to all participants. However, any value that comes from an interaction expression is a secret which only that participant knows. Furthermore, any values derived from secret values are also secret. A value, X, is considered derived from another, Y, if the value of Y is provided to a primitive operation to arrive at X, or if Y is used as part of a conditional that influences the definition of X. Secrets can only be made public by using the declassify primitive.

When secret values are bound to an identifier within a local step, the identifier name MUST be prefixed by an underscore (_).

When public values are bound to an identifier, regardless of context, the identifier name MUST NOT be prefixed by an underscore (_).

Consequently, identifiers which appear inside of a function definition or arrow expression MAY be prefixed by an underscore. This will cause a compiler error if any value bound to that identifier is public.