Check that definitions from modes respect their scope

[bugarela]

TNT has modes that define what expressions can be used inside a definition. We are currently ignoring this and everything is allowed in any mode. We should make a pass after name resolution that checks semantically if definitions of a mode contain only expressions allowed in that mode.

[bugarela]

There's currently no way of differentiating state and stateless modes. One idea is to add the pure keyword as a prefix to any stateless definitions.

[bugarela]

state and stateless operators can be used as parameters to high order operators. However, without specification of which mode the parameter has, we don't have a way to infer/check the mode of the high order operator itself. @shonfeder proposed to require this specification in the signature. We could have something like

pure def MyOperator: (pure (int) => bool, str) => bool
// => ok
def MyOperator: (pure (int) => bool, str) => bool
// => ok
pure def MyOperator: ((int) => bool, str) => bool
// => Error: unpure operator used by pure operator
def MyOperator: ((int) => bool, str) => bool

Alternatively, we could use a stateful/stateless syntax so this is always specified (versus omitted/present pure):

stateless def MyOperator: (stateless (int) => bool, str) => bool
// => ok
stateful def MyOperator: (stateless (int) => bool, str) => bool
// => ok
stateless def MyOperator: (stateful (int) => bool, str) => bool
// => Error: unpure operator used by pure operator
stateful def MyOperator: (stateful (int) => bool, str) => bool

WDYT? @shonfeder @konnov
I think I like the first one better. pure can be completely optional and we could tip people to include it via linting, i.e.:

💡 This operator is stateless, include the keyword pure

[bugarela]

I've created a milestone to track progress on the effect system: https://github.com/informalsystems/tnt/milestone/3

When that's finished, we should decide on how to use modes to restrict an expression's effect and add some checks.

[bugarela]

Upon further understanding of operator's effects, we realize almost all operators should take parameters with a Read[*] effect. Take integer addition for example:

iadd: (Read[p1], Read[p2]) => Read[p1, p2]

Even tho it represents a pure function, it can propagate reads:

x: Read['x']
1: Pure
x + 1: Read['x']

So perhaps the desired definition for the pure mode is something like: An operator that doesn't add any read effect on top of the reads of its parameters.

[konnov]

#187 hopefully unblocks this issue