Quint -> TLA+ transpilation fixes

[bugarela]

Hello

I was running into some issues when using Apalache to transpile Quint into TLA+. There were even parsing errors with invalid parenthesis. After much debugging, I got to fix all of the ones I know of, except for the assignments in init (which are not a big deal because there's only one init per spec so it's always easy to manually fix those).

Here are the issues:

1. Whenever we had a default eliminator on a match, we would produce something like QUINT_LAMBDA1([]), but [] is not a valid TLA+ expression. I've replaced it with {}.
2. When accessing a map (function) with lists as domains, we need to do something like map[<<1, 2>>] but the pretty printer was removing the tuple wrapper on this and producing map[1, 2] instead which is not right.

• I don't know why this existed. On the test, seems like it could have something to do with recursive operators, which as I understand should have been removed. It was also introduced in a recursive-operator related PR: https://github.com/apalache-mc/apalache/pull/312/files#diff-9f17d2b8582a6882dd7eb194ab597fa265a8f5423e02b724b767af7a3c444a01

3. For Quint's unit type, we were producing "U_OF_UNIT" and this was causing a TLC-specific error: TLC tried to compare some value like [ "tag" |-> "Some", value |-> 1 ] with "U_OF_UNIT" for its fingerprint generation and it failed at comparing. Replacing "U_OF_UNIT" with [ "tag" |-> "UNIT" ] fixed this problem, so that's what I did.
4. Lastly, the most complicated one: applying operators to LET-IN arguments doesn't work on TLC, and the Apalache representation transforms a lot of things into this format. I didn't want to touch anything that could affect Apalache's internals, so I only changed how this things get printed. Something that has this structure on Apalache IR:

Foo(LET A(param1, param2) == param1 + param2 IN A(1, 2))

will be printed as:

LET A(param1, param2) == param1 + param2 IN Foo(A(1, 2))

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entries added to ./unreleased/ for any new functionality

[konnov]

This is a nice set of fixes. Thanks a lot! I have a question about two of the changes, trying to pinpoint the cases where it is actually required.

[konnov]

Why do we have to remove this? In TLA+, f[x, y] is a short-form for f[<<x, y>>]. Look at this example: https://gist.github.com/konnov/ce0ca9071dbe75b936e96dbd99224f0d

[bugarela]

It does work like that for tuples, but not for sequences:

--------------------------------- MODULE test ---------------------------------
EXTENDS Integers, Sequences

VARIABLES
  f

Init ==
  f = [ l \in {<<1>>, <<>>, <<1, 2>>} |-> Len(l) ]

Next ==
  UNCHANGED f

Inv ==
  f[<<1>>] = 1

Inv2 ==
  f[1] = 1

=============================================================================

TLC fails to check Inv2 here:

Error: Attempted to check equality of the function << >> with the value:
1
While working on the initial state:
f = (<<>> :> 0 @@ <<1>> :> 1 @@ <<1, 2>> :> 2)

Error: TLC was unable to fingerprint.

I believe there is no way to disambiguate between tuples and sequences at this point, so the only option was to remove it completely.

[konnov]

Do you have an example of what does not work exactly? For instance, this one works in TLC: https://gist.github.com/konnov/e7df8586a9865027dc4abfc07188e060

[bugarela]

Oh interesting, I only realize this now, but this problem only happens with high-order operators. Here's an example that doesn't work:

--------------------------------- MODULE test ---------------------------------
EXTENDS Integers

VARIABLES z

F(f(_), x) == f(x)

G(x) == F(LET H(y) == y * 2 IN H, x)

Init ==
  z = G(3)

Next ==
  UNCHANGED z

=============================================================================

TLC Errors:

*** Errors: 2

line 8, col 11 to line 8, col 32 of module test

An expression appears as argument number 1 (counting from 1) to operator 'F', in a position an operator is required.


line 8, col 9 to line 8, col 36 of module test

Argument number 1 to operator 'F'
should be a 1-parameter operator.

[konnov]

Right. This is because operators are not values in TLA+

[konnov]

Do you mean something like this?

LET A(x, y) == x + y IN F(A)

Actually, this one should work if F is declared as F(A(_)) == ...

[bugarela]

Not sure if I understand the question. I'm saying this one works:

LET A(x, y) == x + y IN F(A)

while this one doesn't:

F(LET A(x, y) == x + y IN A)