Typechecking crashes with `IllegalArgumentException: Unsupported expression` on unbounded quantification (e.g., `\A x: P`). about apalache HOT 8 OPEN

Ah sorry that's what you are suggesting in Item 2 above.

from apalache.

Thank you for the report! Any chance you could provide a minimal reproduction? That would help expedite debugging.

from apalache.

Nevermind! I can reproduce this on

https://github.com/tlaplus/Examples/blob/adccef97931d44120a64ba88054b5ab085f8c50d/specifications/lamport_mutex/WellFoundedInduction.tla#L151

with

$  apalache-mc typecheck WellFoundedInduction.tla 

The type checker is chocking on the second formula of

WFInductiveDefines(f, S, Def(_,_)) ==
     f = [x \in S |-> Def(f, x)]
                      
                    
WFInductiveUnique(S, Def(_,_)) ==
  \A g, h : /\ WFInductiveDefines(g, S, Def)
            /\ WFInductiveDefines(h, S, Def)
            => (g = h)

from apalache.

Yes, sorry I should have dug a little deeper here. A simpler example is to run apalach-mc typecheck WellFoundedInduction.tla (WellFoundedInduction.tla). Are you able to reproduce that?

from apalache.

No worries! I found it quickly. This is a great report as is, I was just being greedy in asking for more :D

from apalache.

Got it

Minimal repro

---------------------------- MODULE test --------------------------
Foo == \A g: TRUE
=================================================================

Dagnosis

The crash is an error in the type checker, as the offending case says it should not be reachable:

But the root cause of the impact on your work is the fact that we do not support unbounded quantification. See https://apalache.informal.systems/docs/lang/logic.html#unbounded-universal-quantifier. So, e.g., if we add a bound to the quantified g in Foo == \A g \in S: TRUE`, we don't hit this problem.

Voting.tla is picking up its dependency on this formula (in the WellFoundedInduction module) only via the instantiation of Consensus in

https://github.com/nano-o/TLA--Examples/blob/43c2814b56af9a3e5d3ee7f6663a72be94f9ca48/specifications/Paxos/Voting.tla#L187-L193

Proposed workaround

To unblock your work, aiming to reuse as much of Voting.tla as possible, could you move that instantiation and the final theorem that depends on it into an extension of Voting.tla?

In general, the current workaround for this kind of limitation -- i.e. where a TLA+ spec includes some theorems which Apalache does not support -- is to factor the theorems into an extension of the module we mean to check.

Fixes

I am considering at least two fixes two address this report:

• 1. Fix the error in the type checker in one of three ways:
  • (a) identify and report unsupported expressions before passing them to the type checker, or
  • (b) catch and diagnose this kind of issue based on the exception raised in the type checker
  • (c) support type checking expressions of this sort without issues, and only raise an error if they make it into model checking.
• 2. We might try to find a way to prune the IR before we pass them on to static analysis.
  • This would allow us to eliminate stuff we don't support (like theorems) before we raise errors about them. This would allow supporting a larger subset of existing TLA+ specs.
  • There should probably be a flag to control this optimization, as users may want use the typechecker even on code we don't support in model checking.

Prioritization

Since the functional limitation follows from known and documented unsupported TLA+ expressions, and since we have a known and documented workaround suitable for any practical model checking effort, I think we can classify this as a non-critical UX bug.

from apalache.

@nano-o Sorry there isn't an easy fix to allow you to use Voting.tla as is, but hopefully the needed changes could be small enough it would be accepted into the Examples?

from apalache.

It looks to me like the problematic definitions are only used in TLAPS proofs. So could Apalache just ignore them?

from apalache.