Introduce `allListsUpTo`

[bugarela]

Hello :octocat:

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?

• [X] Tests added for any new code
• [X] Documentation added for any new functionality
• [x] 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.

[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.

[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 :sweat_smile:. 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.