Unchanged syntax/behavior

[bugarela]

In a recent Quint meeting, I've discussed with Igor about three different ways we could handle unchanged in Quint. Some of the ideas we discussed were already suggested in the past, but I don't really know who suggested what. Let's recycle these ideas in this discussion and try to reach consensus.

An important constraint I'm taking as a premise is that there is no perfect solution that requires no user definitions and can infer the expected behavior. To exemplify this, take the following action definition:

action StutterOnNegativeX = {
    x < 0
}

action Next = {
    & y <- y + 1
    & StutterOnNegativeX
}

If the author's intention was to define stuttering steps over states where x < 0, a possibly expected behavior here would be to raise an error saying that y is assigned twice. If we give no resource for the user to specify a stuttering step, we lose the ability to point out this type of errors.

Option 1 - Declare what is unchanged

The TLA+ way: make it so the user has to explicitly list all variables that are unchanged, either via an operator or with manual assignments (i.e. x <- x).

Option 2 - Declare what is changed

Each action should declare which variables it changes, and we could use * for "changes all variables". This makes it easier to introduce implicit unchanged statements for all the declared variables at each action as a conjunction.

action<*> StutterOnNegativeX = {
    x < 0
}

action<y> Add1toY = {
    y <- y + 1
}

action Next = {
    & Add1toY
    & StutterOnNegativeX
} // => error

Option 3 - All action definitions fully define variables

This is implicit behavior that requires no typing from the user but relies on users reading the documentation. In this approach, it's like all actions are action<*> in Option 2, so we always introduce unchanged statements at each action definition (that is, a named action).

No Option

We could also choose to just introduce unchanged statements at the Next action. In this case, a user could be explicit in a more verbose way if they want to:

action StutterOnNegativeX = {
    & x < 0
    & x <- x
    & y <- y
}

action Next = {
    & y <- y + 1
    & StutterOnNegativeX
} // => error

[bugarela]

Personally, I'm in favor of Option 2. I feel like it is a good signature to enforce, and we could make it not an overhead to the "lazy" users by adding some IDE hints to remove or add variables to the signature with one click. My second option would be "No Option" at the language level, but with good linting that points out you should have fully defined named actions as a good practice (i.e. "Add x <- x to make this action fully defined").

[konnov]

In Option 2, shall we write Next<*> instead of Next below:

action Next = {
    & Add1toY
    & StutterOnNegativeX
} // => error

Alternatively, we could also assume that A without brackets is equivalent to A<*>.

[bugarela]

I think we should write Next<*> (it was actually my mistake not to do it in the example). Typing <*> is an opportunity for the user to remember they have to specify some variables.

[Kukovec]

Shouldn't that be action<*> Next, not action Next<*>?

[thpani]

In my mind, if we support a wildcard <*>, plenty of people will just accept it as syntax and use it everywhere. I don't think this leads to good specs.

[bugarela]

It's not as simple as just "use it everywhere". If it is used everywhere when it shouldn't, we will have collisions, since it is the same thing as writing x <- x twice. I think it's just a matter of having good error messages to explain why there is an error because of multiple <*> usages. Imagine this example where <*> is used everywhere

action<*> StutterOnNegativeX = {
    x < 0
}

action<*> Add1toY = {
    y <- y + 1
}

action<*> Next = {
    & Add1toY
    & StutterOnNegativeX
} // => error

Our error message could be something like

y is changed more than once in expression:
    & Add1toY
    & StutterOnNegative

Definitions for y found at:
action<*> StutterOnNegativeX
action<*> Add1toY

[konnov]

I also like Option 2. As in my comment above, we can have the best of two worlds: A<vars> specifies that vars should be updated (perhaps, with the old values), whereas A specifies that all variables should be updated.

[bugarela]

@Kukovec @shonfeder @rodrigo7491 @thpani @p-offtermatt I should have mentioned you before, what are your opinions on this, if any?

[thpani]

Edit: I misunderstood the original proposal, see #70 (comment).

In favor of option 2 with implicit wildcard <*> and calling it something other than "changed".

My previous post, for the record:

I have a strong opinion on this: I'm in favor of either

• option 1, or
• option 2 without a wildcard, if we can statically determine (and fail) if a variable listed in A<changed> is not actually changed.

Rationale: Writing specifications should be as easy as possible, but not at the cost of giving up rigor.
To me, the main purpose of unchanged is that provides a fail-safe that checks (to some degree) that what I wrote is what I meant.
To this extent, I like option 1, because it actually forces me to write the inverse of what I likely have in my head (i.e., how the state changes).

[thpani]

Yes, that's exactly my point. We should therefore not pick (1), because it is misaligned with expectations.

And my point is that we should pick (1), because it is misaligned with expectations.

[Kukovec]

I'm long past the point of believing syntax that "makes people think about what they write" actually does that.

[thpani]

And I don't believe that everything people complain about needs fixing 🤷
People generally don't know what they want.

Yes, but it's one we can circumvent, by having the language match up closer to what people expect.

I'm pointing out that this does not come at zero cost, and we should be conscious of it.

[konnov]

@konnov keeps pointing out that Leslie Lamport was incredibly smart in defining the features of TLA+. I don't think UNCHANGED is an instance where he failed.

Part of the problem comes from the fact that there is no difference between actions and predicates in TLA+. They are all just formulas, even worse, they are just expressions, since everything is untyped. There is actually a notion of a level in TLA+, but it is defined inductively and nobody knows about it.

One of the important features in Quint is that we do distinguish predicates, actions, temporal formulas, and other expressions. Also, we use explicit notation x <- e for delayed assignment instead of next(x) = e in actions. The latter form is left to temporal formulas. So yes, we make actions a bit closer to programming languages, as we actually want engineers to use Quint. As Jure said, we have seen a lot of trouble caused by UNCHANGED. It is common to copy & paste the UNCHANGED statements and forget to update them. We have a pass that finds these issues while looking for assignment candidates.

Given that we have a more rigid structure with actions and delayed assignments, there is a hope that we can compute what is changed/unchanged automatically. It is definitely an additional feature that requires some form of static analysis/type inference, which would make writing a full-featured transpiler. Perhaps, we can combine it with the mode inference.

[thpani]

Just had a very helpful offline discussion with @Kukovec. My confusion was that I thought this is somehow related to TLA+'s UNCHANGED operator in that it constrains the transition relation. Jure just told me this is not so. One takeaway: we shouldn't call this "(un)changed", it may confuse ppl coming from TLA+. Maybe "assignment declaration" or similar is a better name.

[Kukovec]

I'm mostly in favor of (2), and if you want syntax simplifications you can just have <*> be implicit.

[p-offtermatt]

I like 2) the most, but dislike the syntactic sugar of having action be equivalent to action<*>.
It makes specifications easier to understand to have this pattern be explicit, and in my opinion it's reasonably short.
The replacement could also explicitly be performed by an IDE, instead of implicitly by the parser.

I'd also appreciate a way to group variables, for instance

counterVariables = set(c1, c2, c3)
stateVariables = set(s1, s2, s3)
msgVariables = set(m1,m2,m3)

action<counterVariables> DoCounterStuff = {
}

action<stateVariables, counterVariables> DoStateAndCounterStuff = {
}

...

For me, 1) has one major issue: when I want to add a new part to the spec, with a new variable that I want to change only in some new actions, I have to go back and change parts that are completely unrelated to this new variable. This can certainly be phrased as a benefit as well, since it forces me to go over the spec and actually see whether the new changes affect anything that I wrote before.

[shonfeder]

I think having named subsets of state variables that are all accessed together would be very nice.

[thpani]

I tried to follow @gabrielamafra's comment above, but I'm thoroughly confused by now. A few questions for clarification:

Let’s say we have an action A = { y <- y + 1 }, what is the operational semantics of taking A from a state { (x,y) | x=0 /\ y=0 }? Is it { (x,y) | x=0 /\ y=1 } or { (x,y) | y = 1 }? Do we have this defined somewhere?

Also, for option 2, would a definition action<x>

• declare a contract that x should be changed by the subsequent definition (and if so, what does this mean, i.e., does x <- x constitute a "change"?), or
• change the semantics of the subsequent definition, to something where x is havoced?

[Kukovec]

Okay, so option 2 is not the dual of UNCHANGED in TLA+?

UNCHANGED x is syntax sugar for x' = x. action<x> A under either option 1 or 2 is a syntax contract and has no TLA interpretation. The difference between option 1 and option 2 has nothing to do with the operator UNCHANGED, but with whether or not an exception is thrown if x <-x is present or missing respectively.

Error because the set of successor states is infinite, or because of the CHANGED/UNCHANGED annotation?

Because the state space is infinite.

And if both A and B have CHANGED annotations, we require their changed variable sets to be disjoint?

Yes.

[konnov]

Yeah. That's why we should avoid the word "changed". @thpani, you are right, in TLA+ CHANGED x is defined as x' /= x and hence (CHANGED x) <=> ~(UNCHANGED x).

Maybe touches x is a good term here. Basically, we want an indication, whether a variable x is defined by an assignment or by an implicitly inferred unchanged(x). If a variable x' is not mentioned in a formula, then x can have an arbitrary value in a next state (this is the semantics of TLA+). We simply want to avoid that "undefinedness".

[Kukovec]

I'd favor action<x> A to read as "A promises x"

[bugarela]

The difference between option 1 and option 2 has nothing to do with the operator UNCHANGED, but with whether or not an exception is thrown if x <-x is present or missing respectively.

Actually, my proposal on option 2 is that we implicitly add UNCHANGED(xi) statements for each unassigned variable in action A<x0, ..., xn>. I don't think we should do option 2 just for the sake of throwing exceptions, forcing the users to write both action A<y> and y <- y whenever a variable is unchanged.

[Kukovec]

If anything, you should be adding UNCHANGED y if you see action<x> A with some x <- e (assuming x,y are the only vars). If you don't want to mutate y, don't add it to <_>.

[thpani]

Another thought: this screams "user study" at me. We can find a bunch of people and show them the code snippets above, maybe with a brief paragraph of description about what's declared inside action<...>.
Then ask them for the semantics of each action, and maybe also what happens if one adds a fresh variable.
If they can figure it out intuitively for one of the options, shouldn't that be the one we choose? (And if they can't, wouldn't it show that we still have work to do?)

My only concern is if this is an economical solution, but we might recycle it for further questions about the language design + tooling.

[konnov]

Definitely. Once we have a working VSCode plugin, we should try it with our engineers. We just know from our previous discussions that every single engineer was annoyed by UNCHANGED.

[shonfeder]

One relevant thread of prior discussion can be found at https://informalsystems.slack.com/archives/CU8E7J9LL/p1629983648002000, this also hits upon a syntax essentially equivalent to (2), and Andrey notes there that he also hit on essentially the same approach earlier https://informalsystems.slack.com/archives/CU8E7J9LL/p1630058228030600. The fact that three different people have been drawn to the same idea independently seems to say something about its intuitive appeal :)

[shonfeder]

This kicks around some ideas based on things that have come up in conversation, stuff suggested in #62 (comment) and earlier in this discussion, and from other things I've seen around.

Note that all the concrete syntax suggested here is just for example, and what
I'm hoping to explore is a more uniform way of tracking and declaring the
interaction between effects and the state variables affected. Any suggestions
for alternative concrete syntax that helps works towards this improved clarity
and uniformity would be super helpful.

Perhaps we could consider an approach that unifies the mode system with the
declaration and static analysis of memory region access? I think this might
produce a more uniform and predictable syntax, which could be easier to analyze
statically, more readily able to advantage of techniques for effect systems, and
easier for users to reason about. Here's a thought experiment, just for
consideration:

To start, suppose we get consolidate the 5 different expression-level keywords:
val, def, pred, action, and temporal. We could just limit the keywords
to a few high-level concepts:

• Define an expression with def
• Define a module with module
• Define a variable with var
• Define a constant with const

I think we're agreed that what we are currently calling "modes" can also be
understood as "effects" (and perhaps there is also some benefit in using
"effects" for the state/stateless/action distinction, so as not to confuse the
difference between these kinds of operators with temporal modalities that come
into play when dealing with temporal operators?).

Instead of determining the effect by using a mix of different brackets,
keywords, and implicit inference based on body content, lets experiment with
using some of the conventions used in languages that support an effect system.

In particular, consider how it might look if we follow languages like
Flix or
others that use a "
type-and-effect system". These languages indicate the effect of an
expression by conjoining the type annotation of an expression with its effect
annotation, usually separated by some special characters. Just for the sake of
this exploration, let's use the pattern Effect[params]{type}

So that

def foo : E[x1,x2]{t}

is read to say

expression foo is an expression of type T with effect E on regions x1
and x2

Since state variables (memory regions) are super important for TLA, let's also
consider we should introducing a lexical indicator to make it really obvious
whenever a state variable is in play. I'll borrow from OCaml's syntax for type
variables, and use ' as a prefix for all state variables. This will help with
differentiating type variables and parameters from memory region parameters.

Now, let's suppose we have the following kinds of effects:

• Pure{t} aka Stateless: as per our last meeting, this is a referentially
  transparent expressions that always resolve to the same expression of type t
  when given the same arguments (nullary expressions being a degenerate case).
  Since it is pure, it cannot effect any memory regions. This can be taken as
  the default, so that foo : t means foo : Pure{t}.
• Read['x1,...,'xn]{t} aka State: expressions of type t that can read from
  memory regions (state variables) 'x1, ..., 'xn.
• Update['x1,...,'xn] aka Action: expressions that can update memory regions
  'x1, ..., 'xn. Since these can only ever be of type bool, we can always
  omit the type.
• Temporal: temporal operators (I won't discuss these in this note, but I
  wonder if we could learn something about the relation between temporal
  modalities and the regimentation of effects by considering alternative
  approaches to effects, such as that presented in "Contextual Modal Types for
  Algebraic Effects and Handlers" where the
  effects "are managed by programming constructs corresponding to the logical
  introduction and elimination forms for the [] modality".)

Whenever the type is omitted, we can understand the value of the expression to
be bool, since this seems to be a sensible for TLA operators. And whenever the
effect is omitted, we can understand the effect to be Pure.

I've also suggested a slight renaming trying to make the significance of the
effect on the memory regions very clear.

So, a pure operator from an int to an int would just be

def Foo(x: int): int = {
  // ...
}

A state predicate would need to specify the memory regions it can access. So
adapting the example used to spark the discussion, we'd have:

def StutterOnNegativeX: Read['x] = {
    x < 0
}

An operator that read from the state and returns an int would need to specify
its type:

def XPlusOne: Read['x]{int} = { 'x + 1 }

An action would need to specify the memory regions it can update. But we can
use the same wildcard idea @bugarela suggests whenever we know we'll need to
update (or read) everything:

def Next: Update[*] = {
    & 'y <- XPlusOne + 1
    & StutterOnNegativeX
}

Here's a sketch exploring how we might precisely describe higher order operators
that effect regions based on the regions effected by their arguments. This
example borrows the "splat" syntax used in some other languages, so ...'foo, 'x would match a sequence of regions which must at least include the variable
'x, all other regions going into the sequence of regions in 'foo. We also
use & in the effect annotation to indicate the combination of two compatible
effects (perhaps it's not a great idea to overload this operator?):

def HigherOrd(a, pureOp, readOp):
    (T => U, U => Read[...'vars, 'x]{int}) => Read[...'vars, 'y] & Update['x] = {
  & 'y < 19
  & 'x <- readOp(pureOp(a)) + XPlusOne
}

HigherOrd would update 'x, and it would read but not update everything in
'vars along with 'y.

Anything interesting in any of this to y'all?

[konnov]

I think the way you present effects is by retrofitting the existing type system. This makes types barely readable, at least from the syntactic point of view. I agree that the last example is not a great idea. We should not let actions to be parameters of other actions.

IMO the effect types that you are describing would be useful for inferring modes and effects on the variables. However, I don't think that we should overcomplicate the syntax to: (1) combine effects with other types, (2) do it like in other languages.

[shonfeder]

However, I don't think that we should overcomplicate the syntax to: (1) combine effects with other types, (2) do it like in other languages.

re: (1) The point is not to be like other languages for its own sake, but to take inspiration where it might be useful.

re: (2) This suggestion exactly doesn't combine the effects with other types. As noted, it takes the types and effects system approach that separates the types from the effects. If they were combined, the effects would syntactically be just like any other type. An equivalent syntax could put the effect before the declaration. Perhaps a better syntax would be use always use the prefix keyword for operators (with pure/stateless being optional?). So this could look more or less just like what's been proposed:

pure foo ...
read<x, y> foo...
action<x, y> foo ...
temporal foo ....

And then using the prefix syntax for parameter annotations @bugarela proposed in #62 (comment)?

If actions should not be parameters to operators, won't we need to enforce that somehow in our static analysis? Nothing about the syntax I propose makes that required afaict. The question is how do you express the constraints on what operators can be given to what operators as arguments?

This makes types barely readable, at least from the syntactic point of view.

In terms of the concrete syntax, we could consider any other form of ascii representation that you'd find more readable. The question I'm after is whether it's not better to have single, uniform way of designating what operators have what modes and which variables they access, rather than piecing that together from different indicators in different places. (Currently from a mix of prefixed key words, implicitly, and the particular use of brackets).

It would be nice to have one place to look to figure out what mode an operator has and which variables it will effect (if any), given its mode.

[shonfeder]

(1) combine effects with other types

One other thought here: isn't it the case that our semantics require combining effects with types in at least some ways? iiuc, the effects determine the allowed values of operators, insofar as actions and temporal operators can only be bool and they cannot be supplied as paramters to other operators.

Iiuc, we also already have effect polymorphic higher order operators in the lanuguage, that make the effect of values provided as arguments determine the effect of the operator. My reading of

| `exists`          | Stateless, State, Temporal             | Mode of `P` |

is that (using the bad notation i proposed here):

exists : (set(T), T => E[...vs]{bool}) => E[...vs]{bool}

Where E is an effect-variable, that will propagate the effect of the second argument to exists.

But annotating exists seems like a nice test case! I wonder, how we would express the type and effect of exists with the current syntax? Would we just leave it impossible for a user to write an operator like exists?

[bugarela]

I've stumbled upon an interesting case, so I'm posting it here for us to reflect. But first, to update the context: we already have a working effect system capable of preventing multiple updates of the same variable and ensuring disjunctions are balanced (all branches update the same set of variables) based on Shon's last comment (thanks Shon!).

I noticed this definitions in a spec from Zach:

MaybeUpdateBlock ==
    \/ block' = block + 1
    \/ UNCHANGED block

Considering option 2, this is how I thought we could write the same definition in TNT:

action<block> MaybeUpdateBlock = {
  | block <- block + 1
  | block <- block
}

or even

action<block> MaybeUpdateBlock = {
  | block <- block + 1
  | true
}

Both TNT versions are not terrible, but I do think they look worse than the TLA+ version, so it might be a case to pay attention to.

My first thought is to introduce an operator that takes an expression e and returns e | true so we can write something like

action<block> MaybeUpdateBlock =  maybe(block <- block + 1)

we could also consider adding unchanged(x) as an alias to x <- x, but that might be confusing to newcomers, as they might assume it works as in TLA+ (with all the associated issues).

I'm not confident that this is actually an issue, nor that my proposed operator is a good solution. I'd just like to register the idea and see what you guys think @konnov @Kukovec @shonfeder @rodrigo7491 @thpani

[konnov]

Except that doesn't work. In action<x> { x <- x + 1 | false }, the false branch does not explicitly assign x, but even with the proposed solution would not stutter x.

I am not sure I understand this example. The false branch is never executed, so we do not know (or don't care) about whether x got assigned anything or not.

[thpani]

Right. Because you're interpreting it as a logic constraint.
My point is that there is no unambigous "computational" or "operational" reading. You have to read it as a logic constraint.

Then true should also be true, independent of what you're declaring as "changed" in <...>.

[thpani]

Another concern here is the usability of this construct.

The <...> declaration may be dozens of lines above the | true branch and out-of-view when the user writes the branch.
I don't think we can expect users to track in their head what variables they did declare as "changed" while writing the action body.

[konnov]

I don't think we can expect users to track in their head what variables they did declare as "changed" while writing the action body.

This calls for a user study. Can we imagine conducting one?

[thpani]

I think a good exercise (and prerequisite for a user study) would be to actually write down a language docs-level explanation of the intended behavior of the changed annotation.
I expect this "smart" version of <...> to be quite difficult to teach to users.

[konnov]

That an interesting observation. I have not thought about it. Both of your versions in Quint looks fine to me. We could introduce a constant skip that is equivalent to true, just to make the true version look better.

[konnov]

I have just found a simple workaround to keep the effects checker happy:

  // An auxilliary action that keeps all variables unchanged.
  // In the future, such a change could be computed automatically:
  // https://github.com/informalsystems/quint/discussions/70
  action keepVars = all {
    balances' = balances,
    accounts' = accounts,
  }

  // test that a simple `send` goes through
  run sendOkTest = {
    init
      .then(send("alice", "bob", Map("atom" -> 3)))
      .then(all {
        assert(balances.get("alice").get("atom") == 27),
        assert(balances.get("bob").get("atom") == 4),
        keepVars,
      })
  }

My idea was just to write an assert(...) in the next state after executing send. The effect checker complained, as it could not find assignments to variables. It seems that keepVars is a simple workaround here. The only annoying thing to me is that I had to wrap asserts in all { ... }. On the other hand, I would have to do it in any case, since I wanted to have several asserts.

This actually makes me wonder, whether we want to place unchanged automatically, if there is a simple pattern that we can just explain to people. Conceptually, it is not different from UNCHANGED in TLA+. However, there is one big plus in Quint: the effect checker will complain, if a variable is assigned twice, which happens to me in TLA+ quite a lot.

[konnov]

I remember that @bugarela and myself were discussing another approach to the problem that is not documented here. Documenting it for completeness (also to get rid of my todo).

We have been trying to figure out what is better: (1) Specifying which variables should be unchanged, or (2) specifying which variables should have assignments. Both (1) and (2) have various good use cases. Why don't we find a way to specify the both?

Here is my proposal: introduce two operators: unchanged<x, y, z> { ... } and scope<x, y, z> { ... }

Branches

Before we define the semantics of scope and unchanged, we have to define the branches of an action. For an action $A$, we define the set of subexpressions $Br(A)$ by induction:

• if $A$ does not contain if, all, any, then $Br(A) = { A }$.
• if $A$ is of the form if (P) B else C, then $Br(A) = Br(B) \cup Br(C)$.
• if $A$ is of the form all { A_1, ..., A_n } for some $n$, then $Br(A) = Br(A_1) \cup \dots \cup Br(A_n)$.
• if $A$ is of the form any { A_1, ..., A_n } for some $n$, then $Br(A) = Br(A_1) \cup \dots \cup Br(A_n)$.

Semantics of unchanged

This operator can be applied only inside action definitions. We define unchanged<x_1, ..., x_k> { A } to be an action C that is constructed from A by replacing its branches as follows:

If A_i \in Br(A) and the effect of A_i is Read(...) & Update([y_1, ..., y_m]), and $\{ x_1, ..., x_k \} \setminus \{ y_1, ..., y_m \} = \{ z_1, ..., z_p\}$ (treat variables as names not values) then $A_i$ is replaced with all { A_i, z_1' = z_1, ..., z_p' = z_p }.

Example:

action StutterOnNegativeX = unchanged<x> {
  x < 0
}

action Next = all {
  y' = y + 1,
  StutterOnNegativeX,
}

In our example, StutterOnNegativeX is equivalent to:

all {
  x < 0,
  x' = x,
}

Semantics of scope

Semantically, scope<x, y, z> { A } is equivalent to A. However, the effect checker must ensure that the effect of A is Read([...]) & Update([x, y, z]).

Example:

action step1 = scope<x, y, z> { any {
  Foo,
  Bar,
}}

action step2 = scope<x> { any {
  Foo,
  Bar,
}}

action Foo = all {
  x' = x + 1,
  y' = y - 1,
}

action Bar = all {
  x' = x * 2,
  y' = y + 1,
}

In the above example, Foo and Bar are updating the same set of variables (x and y), they are not updating z. The effect checker should complain about step1 and step2, since scope inside them require $\{ x, y, z \}$ and $\{ x \}$, respectively.

List of variable names

Similar to TLA+, we often would like to introduce a list of variable names once and reuse it. For example, to avoid long lists in unchanged<...> { A }. Here is a syntax that I like:

// define a shorthand for a list of variable names
names myVars = <a, b, c, d, e>

// use the list of variable names
action step = scope<*myVars> { ... }

[konnov]

Also, we can play a bit with the syntax for names, so it looks more familiar, at least to a weird combo of a Lisp and C programmer:

symbol *myVars = '[a, b, c, d, e]

One thing that always bothered me about TLA+ and Quint is that variable names are used in two roles:

• as a way of referring to the variable value, e.g., as in x + y
• as a way to refer to the variable itself, e.g., UNCHANGED <<x, y, z>>

Lisp has a solution to it: We can write 'x or (quote x).

[shonfeder]

We discussed the idea for the scope operator in our quint chat today with
@bugarela and @kucovec. Two related concerns were raised:

1. The proposed scope operator is a no-op w/r/t operational semantics, that
   actually serves as an effect annotation. But in the context of a language
   that already has syntax for type and "mode" annotations, it's not clear why
   this particular annotation should be disguised as a "regular operator". In
   fact, it is not even a regular operator, since it would introduce the
   convention of operators that can take angle-bracketed parameters. Given our
   current syntax, we feel that a conservative extension to the grammar would be
   more concordant than a pseudo-operator, especially considering that this
   would require a change to the grammar in any case.

2. Via the with operator for record updates, we've already seen that supposed
   operators that have special statics cause confusion for users, since it
   tricks them into thinking the operator can be used like any other operator
   given appropriately typed arguments. In contrast, the special form we've
   introduced for record updates makes it impossible to confuse a record update
   as an operator that can be applied to a variable v : str. I am worried that
   we will hit similar confusing behavior if scope is introduced as an
   operator. E.g.,

   What is the meaning of this operator if it is nested?

   scope<a,b> { scope<a,b,c> { Expr } }

   Would this be invalid or would it expand the inner scope to include a c?
   If the latter, what happens to the promise implied by the outer scope,
   that only a and b would be updated? If the former, how do we explain
   to users why this repeated application of an operator defined as
   scope {A} == A is illegal?

   What would be the meaning of

   scope<a,b> { scope<> { Expr } }

   Is it invalid, or would the inner scope be expected to update no variables
   despite the promise implied by the outer scope?

   Things are even less clear to me in the case of higher order operators:

   S.map(f => scope<> { f })

   Would this be legal? If scope is "just a normal operator" it seems like this
   should be allowed, but I'm not sure what the meaning or utility would be.

   We also discussed the possibility of treating the eventual syntax for region
   annotations as sugar for (something like) the proposed scope annotation
   that this operator-like syntax. This could keep our core grammar simpler
   without offering the possible footguns to users. This is similar to our
   handling of with.

I am also worried that the semantics of unchanged proposed here will be
confusing to readers and writers. Looking at your example

action step1 = unchanged<x, y, z> {
     scope<x, y> { any {
         Foo,
         Bar,
     }},
}

I would read the outer unchanged operator to say explicitly that x and y are "unchanged",
but the inner operator should require that x and y get updated, which must
then be happening in Foo or Bar. So what takes precedence: the updates in
Foo/Bar or the prominent outer unchanged? By the semantics you've given
x and y would actually end up changing, but I'm worried that this is sure to
lead to confusion by people who expect an operator to do what is says.

We also came up with an alternative proposal to annotations, that is an improved
take on the general approach to annotations described in
#70 (comment),
but I'll write that up tomorrow in a separate thread.

[shonfeder]

One thing that always bothered me about TLA+ and Quint is that variable names are used in two roles:
...
Lisp has a solution to it: We can write 'x or (quote x).

I am a big fan of introducing lexical markers to call out state vars! :D #629

Your suggestion reminds me of the practice in ML of marking the difference between a reference and reference's value via a !:

let x = ref 0
let () = 
  assert (x == ref 0);
  assert (!x == 0);
  x := 1;
  assert (!x == 1) 

Coincidentally, your idea of "quoting" state vars in unchanged matches my suggestion for disambiguating state variables in effect annotations when I suggested the type and effect system in #70 (comment):

def StutterOnNegativeX: Read['x] = {
    x < 0
}

tho I was thinking of ML's ' on type variables rather than quoting. In the context of unchanged having some sort of "this is a reference not a value" mark does makes sense to me! Tho i worry it might prove redundant if we understand unchanged to be a special form in any case. Contrary to TLA+, where UCHANGED is just an operator that takes a sequence of state variables, in the context of quint, you proposal already has a special, unique syntactic context for state variables within the <...>, which seems like that should be enough to signal that we are not dealing with the values of the state variables?

[konnov]

Thanks for summarising our chat, @shonfeder! It's actually quite illuminating that we had similar discussions about a year ago. Now I can see better what you meant with the effect annotations. We definitely can introduce effect annotations instead of scope. My only worry is to keep the syntax approachable. As I mentioned during the meeting, Dafny has the following syntax for requires/ensures/reads/modifies, which give us an example of extending a function signature in a user-friendly way:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
  requires 0 < y
  ensures less < x < more
{
  more := x + y;
  less := x - y;
}

predicate sorted(a: array<int>)
  reads a
{
  forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}

Inspired by this idea, here is the possible syntax for specifying the effects:

action init
  reads()
  modifies(clientState, serverState) = {
  ...
}

action createTransaction
  modifies(clientState) = {
 ...
}

action processTransaction
  modifies(serverState) = {
 ...
}

action step
    modifies(serverState, clientState) = any {
  unchanged<serverState> { createTransaction },
  unchanged<clientState> { processTransaction },
}

In case reads or modifies are omitted, they should be treated as unspecified, so the effect checker should infer the effects, instead of enforcing them. This is similar to how we are treating types with the type checker.

I am still not sure about unchanged though. We typically need it inside code blocks, especially in combination with if-else and any.

[konnov]

Another take on unchanged. In TLA+, UNCHANGED <<x, y>> is equivalent to x' = x /\ y' = y. In the above proposal, unchanged<x, y> { ... } adds assignments only on the branches, where additional assignments are needed.

We were always thinking that we could use something like modifies(x, y) to fill in the missing assignments. However, modifies(x, y) is an assertion about the exact set of variables that must be assigned. This is important, as specification authors may miss assignments by accident (this surely happened to me many times).

What is missing is some form of a hint that requires an action to introduce x' = x for all missing assignments. So it would be more like a directive/macro rather than an assertion. This directive changes an expression by adding missing assignments, where required. This is why I wanted to introduce unchanged<x, y> { ... }. But I agree that it has non-trivial semantics and smells like a macro, though it would be a very intelligent macro that knows effects. In this sense, UNCHANGED <<x, y>> of TLA+ is a much simpler macro that is purely syntactic. Additionally, TLA+ has a few macro-like action/temporal operators such as [A]_vars, <A>_vars, WF_vars(A), etc.

Now that I am thinking about it, I am not sure I know of any "macros" in programming languages that have similar behavior.