`icse23` uses a parameter as upper bound to `range()`

[thpani]

icse23 doesn't go through Apalache; there's an (existentially quantified) upper bound to range/2:

https://github.com/informalsystems/quint/blob/c07ad1448d0b2f64c91806e8c95f8fbb8aa6c5eb/examples/solidity/icse23-fig7/lottery.qnt#L300-L301

where

https://github.com/informalsystems/quint/blob/c07ad1448d0b2f64c91806e8c95f8fbb8aa6c5eb/examples/solidity/icse23-fig7/lottery.qnt#L274-L276

Possible solution: provide some kind of generators to cover this functionality.

[lucab]

I also hit this limitation when trying to produce a List with a non-deterministic (but bounded) length.

After some searching I found this entry in Apalache documentation: https://apalache-mc.org/docs/apalache/known-issues.html#integer-ranges-with-non-constant-bounds. As mentioned there, making the bounds more explicit will make the verifier happy.

A workaround for this was also mentioned in a Zulip thread: https://informal-systems.zulipchat.com/#narrow/stream/378959-quint/topic/Integer.20ranges.20with.20non-constant.20bounds.

For my usecase, I ended up implementing the logic for a range(0, randomLen) in this way:

pure val maxLen: int = 5
nondet randomLen = 0.to(maxLen).oneOf()
pure val myList = boundedRange(randomLen, maxLen)

pure def boundedRange(rangeEnd: int, boundMax: int): List[int] = {
    range(0, boundMax).select({ x => 0 <= x and x <= rangeEnd })
}