Check assumptions during simulation

[romac]

See: #1450

module parent {
    const N: int

    action init = true
    action step = true
}

module small {
    import parent(N = 42).*

    assume LargeN = N > 100
}

module large {
    import parent(N = 200).*

    assume LargeN = N > 100
}

❯ npm run debug -- run --main small assume.qnt

error: [QNT510] assume1.qnt:11:5 - error: Assumption failed
11:     assume LargeN = N > 100
        ^^^^^^^^^^^^^^^^^^^^^^^

error: Runtime error

❯ npm run debug -- run --main large assume.qnt
(...)

[ok] No violation found (216ms).

---

• 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]

Hi! It is awesome that you managed to make it work with such a small change.

However, there is one problem that you couldn't predict. I'm almost done with a big change to the simulator that will make this a bit harder.

In my new version, I eliminate flattening, so we don't have the issue of discarding assumes anymore. However, we only compile/evaluate expressions that are used (i.e. in quint run we only evaluate init, step and inv and anything that gets used by them).

So I think, ideally, we should have an additional pass that goes through assumptions in all modules and checks them, before compilation. On this pass, I believe it is possible to re-use most of your code here. But it will require a larger change in general. Therefore, I'd rather hold this change until my new evaluator gets merged, so we don't introduce one more thing to block it.

On a separate note: I don't remember how assumptions work in TLA+, but if they can refer to state variables, then we need to make sure we evaluate the assumptions for every single state we explore. This should be easier (I think) to do in the new evaluator (if it is the case).

[romac]

No problem, happy to figure out how to do this properly on top of your changes after those are merged.

[romac]

Note in case that was not clear that this PR does not solve the issue of assumes getting lost in flattening, but only adds checks for those found in leaf modules.