5.4.4 Local Steps
A Reach local step occurs in the body of
It represents the actions taken by a single participant in an application.
Any statements valid for a computation are valid for a local step.
Any expressions valid for a computation are valid for a local step.
However, some additional expressions are allowed.
An interaction expression, written
interact.METHOD(EXPR_0, ..., EXPR_n), where
METHOD is an identifier bound in the participant interact interface to a function type, and
EXPR_n are expressions that evaluates to the result of an interaction with a frontend that receives the evaluation of the
n expressions and sends a value.
An interaction expression may also be written
KEY is bound in the participant interact interface to a non-function type.
An interaction expression may only occur in a local step.
An assumption where
claim evaluates to
true with honest frontends.
This may only appear in a local step.
The declassify primitive performs a declassification of the given argument.
Returns two values,
[ commitment, salt ], where
salt is the result of calling
commitment is the digest of