Introduce allListsUpTo

[bugarela]

Hello

This introduces a new operator called allListsUpTo to be a limited version of the allLists operator. It's currently quite cumbersome to obtain a nondeterministic list value, and this will help.

I'm doing something for the first time (for Quint) here: I'm introducing this as a spell (to be in the stdlib eventually), not as a builtin, but I am including an internal implementation for it. I think this is similar to what TLC does for some operators: have them defined in TLA+ but then internally use a Java implementation.

The reason I need to overwrite the Quint definition with an internal implementation is that the Quint definition needs to use allLists(), which is unsupported by the compiler.

The reason I don't want it to be a normal builtin operator is that it would require many more changes, including on Apalache. This way, Apalache should be able to handle the spell (since Apalache handles allLists()).

I hope this is a good idea. It doesn't fit perfectly now that we don't have a stdlib, but it should only improve and it doesn't look really bad right now. Let me know what you think!

UPDATE

I was assuming the wrong thing about Apalache being able to handle allLists().

• https://apalache.informal.systems/docs/apalache/known-issues.html#using-seqs

TLC also can't handle it.

My bad! I guess this should be a builtin then. In fact, I don't see a reason to keep allLists in this scenario - WDYT?

• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• Feature table on README.md updated for any listed functionality

[bugarela]

Although it shouldn't take more than a few hours to fix this, I'd prefer doing that in another PR later due exclusively to me wanting to merge all the necessary stuff for Ivan's workshop presentation as soon as possible, and this is one of them.

This already works and I tested it a bunch in the Cosmwasm stuff, so it's probably better to move with this version for the workshop anyway.

[p-offtermatt]

I appreciate wanting to merge these quickly, but I don't really know if it makes sense to even merge this to only change almost everything about it promptly afterwards. At least my instinct is to just change the behaviour in this PR.

Also, I tried this out locally and it doesn't work currently for me.
If I do it like this:

   pure def allListsUpTo(s: Set[a], max_length: int): Set[List[a]] = {
        s.allLists().filter(l => l.length() <= max_length)
    }
    
    action step = {
        set1' = Set(1,2,3,4,5).allListsUpTo(3)
    }

I get an error from Apalache.
Quint tells me this:

Error: internal error: unhandled verification error at pass PreprocessingPass
    at handleVerificationFailure (/Users/offtermatt/projects/quint/quint/dist/src/apalache.js:92:19)
    at handleResponse (/Users/offtermatt/projects/quint/quint/dist/src/apalache.js:107:43)
    at process.processTicksAndRejections (node:internal/process/task_queues:95:5)

and when I have apalache in server mode, I also get this error:

<unknown>: unsupported expression: Seq(_) produces an infinite set of unbounded sequences. See: https://apalache.informal.systems/docs/apalache/known-issues.html#using-seqs E@08:35:49.549

And if I try without repeating the allListsUpTo definition, I get a simple compile error:

error: [QNT404] Name 'allListsUpTo' not found

Maybe I did something wrong with compiling, I just ran make quint

[bugarela]

@p-offtermatt I think there is a misunderstanding here, sorry! I realize my description doesn't make this clear enough.

This will not work with Apalache now, neither this version or the improved one, because we will need to change something on the Apalache side for this.

I thought I could make it work with Apalache "for free" by defining this on top of allLists(), but that doesn't work because Apalache can't handle the infinite set. Since we can't define the allListsUpTo operator with existing operators, we need to have it as a builtin, which means adding another case to a match branch in Apalache and defining how to translate this to ApalacheIR.

The difference in the Quint side is much less impactful:
Now:

• not fully prepared for it to be a builtin operator (more changes will be necessary)
• error on Apalache mentions allLists()
  When I improve it:
• allListsUpTo will be a normal builtin operator (no spell for it)
• error on Apalache will mention something about an unknown operator called allListsUpTo

I think I will need the improved version to make it work with Apalache, but nonetheless I'll definetly need an update on Apalache side, and I haven't thought about how to represent this in TLA+/ApalacheIR yet. This is mainly for the simulator.

[p-offtermatt]

Oh, okay, got it.

LGTM then, thanks for clarifying!

I still would probably advise for addressing the Quint side in this PR, since I don't think it's great to have this half-hacked version in the main branch, but I wouldn't block it for this, so I'll approve

[bugarela]

Makes sense! Since I found a way to proceed with #1444 without having to fix #1443, I think I have spare time to fix the Quint side of this. The Apalache part is more complicated :/

[p-offtermatt]

I think the Apalache part can come later no worries! I just think the half spell/half built-in would be good to get into full built-in :)

[bugarela]

All went smooth, so it was actually quite easy 😅. Do you want to take another look? @p-offtermatt

I feel like we should get rid of allLists if it doesn't work anywhere. We can talk about it in the next co-design meeting - I have other thoughts about builtin operators to discuss.

[p-offtermatt]

LGTM, awesome that it worked so well!