A strange performance/OOM issue in quint run

[konnov]

When I am running quint run against this spec, it makes no progress at all. On 100k samples, it even ran out of memory. I suspect non-terminating recursion:

$ quint run --max-samples=10 --max-steps=10 --invariant=unfreezeCannotBeReplayedInv main.qnt
Running... [                                        ] 0% | ETA: 0s | 0/10 samples

[konnov]

In the end, it ran out of memory. There is nothing interesting in the stack trace though:

FATAL ERROR: Ineffective mark-compacts near heap limit Allocation failed - JavaScript heap out of memory

[bugarela]

Debugging this. Found which expression is causing the issue:

main.qnt:1218:47 - error: [QNT501] hanging
1218:                 ALL_MEMBERS.powerset().forall(signers => {
                                                    ^^^^^^^^^^^^
1219:                     val digest = _securityCouncilHashTypedDataV4(
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1220:                         keccak256(abi_encode3(UNFREEZE_TYPEHASH, AbiInt(evm.securityCouncil.unfreezeNonce), AbiInt(validUntil)))
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1221:                     )
      ^^^^^^^^^^^^^^^^^^^^^
1222:                     val signatures = signDigest(signers, digest)
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1223:                     val evm2 = evm.externalCall(sender, SECURITY_COUNCIL_ADDR, FunctionUnfreeze)
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1224:                     val result = securityCouncil::Unfreeze(evm2, validUntil, signers, signatures)
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1225:                     isOk(result) implies {
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1226:                         isErr(securityCouncil::Unfreeze(result.v, validUntil, signers, signatures))
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1227:                     }
      ^^^^^^^^^^^^^^^^^^^^^
1228:                 })
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[bugarela]

@konnov the problem is actually that ALL_MEMBERS is way to big to compute the powerset for, and forall requires Quint to actually enumerate the ALL_MEMBERS.powerset() expression.

Just to make sure, I tried reducing some sets that compose ALL_MEMBERS and it worked.

    pure val SECURITY_COUNCIL_MEMBERS = Set("sc1", "sc2")
    pure val SECURITY_COUNCIL_MEMBERS_QUORUM = SECURITY_COUNCIL_MEMBERS.powerset().filter(ms => ms.size() >= 9)
    pure val GUARDIAN_MEMBERS = Set("g1")
    pure val ZK_FOUNDATION_MEMBERS = Set("zkf1")
    pure val NON_MEMBERS = Set("nobody1", ZERO_ADDRESS)

Having a timeout with nice reporting of which expression timed out would be the best UX here - but for now, I can manually debug for anyone in need 😅