assume is not propagated to Apalache

[konnov]

Consider assumes.qnt:

module assumes {
    const N: int
    const F: int

    var msgs: Set[str]

    assume Majority = N > 3 * F

    action init = {
        msgs' = Set()
    }

    action step = {
        msgs' = msgs
    }
}

module instance {
    import assumes(N = 2, F = 1).*
}

Running quint verify does not result into any warnings or error messages, even though the assumption of Majority is obviously violated:

$ quint verify --main=instance --invariant=inv assumes.qnt

[romac]

@bugarela From what I can tell, the Majority assume is present in the typechecked AST but not in the LookupTable returned by parsePhase3importAndNameResolution, and is subsequently lost after flattening.

[bugarela]

Yes @romac, anything not used is discarded in flattening. Here, init and step are implicitly used, because the default values of --init and --step options match them and therefore we "add" them to the main module for simulation.

I think the problem with assume is actually bigger than this: we don't do anything with assumptions at all, not even in the Quint side. If we implement some assumption checking in the simulator, we will need to make sure it is in the lookup table and flattened modules, and therefore it will end up being sent to Apalache.

[romac]

Yes @romac, anything not used is discarded in flattening. Here, init and step are implicitly used, because the default values of --init and --step options match them and therefore we "add" them to the main module for simulation.

Right, so I guess a potential solution would be to implicitly reference or copy all assumptions from imported modules?

I think the problem with assume is actually bigger than this: we don't do anything with assumptions at all, not even in the Quint side. If we implement some assumption checking in the simulator, we will need to make sure it is in the lookup table and flattened modules, and therefore it will end up being sent to Apalache.

What I would suggest doing is first ensure we do not loseassumptions in the first place, so that they will be passed along to Apalache already. Then we can figure out how to check them during simulation. Would that work for you?

[romac]

I believe I managed to implement assumptions checking in the simulator, but of course right it only works if the assumption is in the main module: #1487