Add `generate` operator

[konnov]

Hello :octocat:!

I would like to add an experimental contribution, namely, the operator generate that mirrors Apalache!Gen. This operator should unlock the feature of Apalache that is sometimes used to reason about inductive invariants. This PR:

• [x] adds the operator generate
• [x] adds an error for generate in the simulator, as it is not clear to me how one would implement that in the simulator
• [x] prepares the ground for translation in Apalache, see https://github.com/informalsystems/apalache/pull/2916
• [x] Tests added for any new code
• [x] Entries added to the respective CHANGELOG.md for any new functionality

[netlify[bot]]

❌ Deploy Preview for quint-docs failed. Why did it fail? →

Name	Link
🔨 Latest commit	4df3ae530f71b88318494b4ad95d9fa47c8407a8
🔍 Latest deploy log	https://app.netlify.com/sites/quint-docs/deploys/667da4508e7f2d00083bd613

[bugarela]

Hi! Thanks Igor, I'll take a look when I can.

Please ignore the Netlify bot, I'm still not done setting it up

[bugarela]

Hey @konnov, I finally took a look at these and I feel like I need more context here. I don't think the name "generate" is very informative, and maybe we should have something more tuned to the particular use case where it is necessary.

A couple of months ago, I introduced an operator called allListsUpTo https://github.com/informalsystems/quint/pull/1442 (that only works on the simulator). Do you think that we can approach this by adding an allSetsUpTo and mapping those into Apalache!Gen calls on the Apalache side? Or did I misunderstood this and it should do something completely different?

[konnov]

Hey @konnov, I finally took a look at these and I feel like I need more context here. I don't think the name "generate" is very informative, and maybe we should have something more tuned to the particular use case where it is necessary.

A couple of months ago, I introduced an operator called allListsUpTo #1442 (that only works on the simulator). Do you think that we can approach this by adding an allSetsUpTo and mapping those into Apalache!Gen calls on the Apalache side? Or did I misunderstood this and it should do something completely different?

Hey @bugarela, yeah, I can see how generate could be confusing. However, it's kind of similar to the generators in property-based testing. It simply generates a value of the proper type (given by the example) that has up to a given number of elements, in case it is a non-scalar type such as a set or a list. The difference from PBT is that generation does not happen at random, but is done by the solver. I can see how using a set instead of a single element could be easier to understand for the people who know TLA+. However, the way generate works now is more in line with oneOf, which could be also expressed as a quantifier over a set

[bugarela]

Ok, so that makes me even more in favor of having the current:

nondet a = Int.allListsUpTo(10).oneOf()

and, in addition, the Set version:

nondet a = Int.allSetsUpTo(10).oneOf()

I'm using the infinite set Int in these examples because iiuc that's the behavior of Apalache!Gen. Could we also use Apalache!Gen for a bounded set like Set(1,2,3).allListsUpTo(10).oneOf()? If not, is it feasible to use a filter, like the equivalent of Int.allSetsUpTo(10).filter(s => s.in(Set(1,2,3))).oneOf()? We could take care of that during the conversion to Apalache IR

[konnov]

Well, this would definitely play nice for the set of all integers, as it is a built-in set. Imagine you would like to generate a set of structures, e.g., of the shape { x: Set[int], y: int -> bool }. Now, if you would like to pass a set, you are basically replacing the type with the set. It's very much what TLA+ people are doing when they are writing TypeOK. However, this approach does not play well with Apalache, as it sometimes starts to unfold the sets. This is exactly what we are trying to avoid with Apalache!Gen.

[bugarela]

I have to thoughts here:

1. The most natural way for a non TLA+ expert to write this would probably be

nondet size = 0.to(10).oneOf()
0.to(size).map(_ =>
  nondet x = Int.oneOf()
  nondet y = setOfMaps(Int, Bool).oneOf()
  { x: x, y: y }
)

Of course, this doesn't work. But I'd like to try and get closer to this intuition than introducing a magical generate operator. Even if that means adding a keyword.

2. We shouldn't require users to write a dummy value like { x: Set(0), y: Map(0 -> false) }. I'd rather require a type annotation, since Quint is a typed language.

[konnov]

I have to thoughts here:

1. The most natural way for a non TLA+ expert to write this would probably be

nondet size = 0.to(10).oneOf()
0.to(size).map(_ =>
  nondet x = Int.oneOf()
  nondet y = setOfMaps(Int, Bool).oneOf()
  { x: x, y: y }
)

This looks really complicated. I agree that this is similar to how one would do it in a property-based framework, since most of them are functional. However, we don't have to do complicated things just because someone did them in the past. Thinking about with a fresh head, I would say that the most natural way for a non-TLA+ person to write this would be something like:

fresh a: { x: Set[int], y: int -> bool } up to 10

I am kind of making up keywords here. The point is that we essentially have to declare a fresh variable and limit its scope.

Of course, this doesn't work. But I'd like to try and get closer to this intuition than introducing a magical generate operator. Even if that means adding a keyword.

2. We shouldn't require users to write a dummy value like { x: Set(0), y: Map(0 -> false) }. I'd rather require a type annotation, since Quint is a typed language.

Yes, this would be great. As an alternative, we could have this form:

nondet a: { x: Set[int], y: int -> bool } = generate(10)

[konnov]

bumped the version of apalache to 0.45.3

[konnov]

Hey @bugarela! Any thoughts on this feature? I really need something like to work on an inductive invariant, see example.

[bugarela]

Hi! I guess we agreed on a solution at the end of the last discussion. However, I'm having trouble picturing the use case for this and therefore assessing the priority here, as this doesn't seem trivial to implement.

IIRC, we talked over zoom and you said you'd try to come up with an example to demonstrate where you need this. Are you still willing to do this? We could also jump into a call sometime, whatever works best.

[konnov]

Hi! I guess we agreed on a solution at the end of the last discussion. However, I'm having trouble picturing the use case for this and therefore assessing the priority here, as this doesn't seem trivial to implement.

IIRC, we talked over zoom and you said you'd try to come up with an example to demonstrate where you need this. Are you still willing to do this? We could also jump into a call sometime, whatever works best.

There is a link to the WIP example in my reply. Sure, happy to jump on a call!

[konnov]

@bugarela I have just described the need for value generators in detail in Apalache: https://github.com/apalache-mc/apalache/discussions/3014

I agree that what we currently have in Apalache is a hack, though it's hard to tell how long it would take to implement a better version (proposed there).

[konnov]

@bugarela is there any chance to have this PR merged? I think other operators have been added since then and this one is not significantly worse then those

[bugarela]

Hi @konnov. This has been in my TODO since we last discuss, but I never decide what do to about it. Sorry about leaving it hanging.

I think we should merge it, while renaming it to apalache::generate, to ensure that people who use it are aware this is Apalache-specific. WDYT? I'd still like to think more about this feature and introduce a more complete version of it, but that might take even more time, so this should unblock advanced users for now.

At some point, you suggested:

nondet a: { x: Set[int], y: int -> bool } = generate(10)

We could also support both (see q::debug for a built-in that has an optional argument), and/or add support for this format later on.

And I find it objectively better than the version in the PR. If you think it is a reasonable amount of work make this change, I think it would look much better and even feel closer to Apalache's Gen which, from what I gather, also uses the type annotation instead of a value in the parameters.

[konnov]

Hey @bugarela! Thanks for coming back to this. Yes, this form would be significantly better:

nondet a: { x: Set[int], y: int -> bool } = generate(10)

Let me check how hard it would be to implement this one

[konnov]

@bugarela I've updated the command syntax to be:

nondet x: <type> = generate(<bound>)
<expr>

As soon as we have a new release of Apalache that includes https://github.com/apalache-mc/apalache/pull/3138, we can finally make it work.

[konnov]

Here is the PR introducing the new version of Apalache: https://github.com/informalsystems/quint/pull/1735

[konnov]

Fixed the broken docs and formatting. Please re-run the tests :)

[thpani]

@bugarela any chance of cutting a release with this?

[bugarela]

@thpani yes, I was planning on doing it today! I'll do it in an hour or two.

[bugarela]

@thpani done!

[thpani]

@bugarela thank you! 🙏