Typechecking crashes with IllegalArgumentException: Unsupported expression on unbounded quantification (e.g., \A x: P).

[nano-o]

Description

I am trying to set things up to model-check Voting.tla with Apalache. I would like to reuse Voting.tla as much as possible, so I created ApaVoting.tla, which instantiates Voting.tla, and ApaVoting.cfg, which substitutes 2 definitions of Voting.tla that are problematic for Apalache. However Apalache crashes as below.

See this PR for context: tlaplus/Examples#112

Impact

I have to duplicate most of Voting.tla in order to analyze with Apalache instead of being able to reuse it. See Voting2.tla and ApaVoting2.tla

The command line parameters used to run the tool

script/run-docker.sh typecheck  ApaVoting.tla

Expected behavior

No error

Log files

2024-01-22T23:36:12,394 [main] INFO  a.f.a.t.Tool\$ - # APALACHE version: 0.44.2 | build: v0.44.2
2024-01-22T23:36:12,401 [main] INFO  a.f.a.t.t.o.TypeCheckCmd - Type checking ApaVoting.tla
2024-01-22T23:36:12,491 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser
2024-01-22T23:36:12,822 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser [OK]
2024-01-22T23:36:12,823 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat
2024-01-22T23:36:12,823 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
2024-01-22T23:36:13,037 [main] ERROR a.f.a.t.Tool\$ - Unhandled exception
java.lang.IllegalArgumentException: Unsupported expression: ∀g: (∀h: (((C!WFInductiveDefines(g, S, Def)) ∧ (C!WFInductiveDefines(h, S, Def))) ⇒ (g = h)))
	at at.forsyte.apalache.tla.typecheck.etc.ToEtcExpr.transform(ToEtcExpr.scala:896)
	at at.forsyte.apalache.tla.typecheck.etc.ToEtcExpr.apply(ToEtcExpr.scala:162)
	at at.forsyte.apalache.tla.typecheck.etc.ToEtcExpr.operDefToDecl(ToEtcExpr.scala:90)
	at at.forsyte.apalache.tla.typecheck.etc.ToEtcExpr.apply(ToEtcExpr.scala:52)
	at at.forsyte.apalache.tla.typecheck.TypeCheckerTool.\$anonfun\$check\$1(TypeCheckerTool.scala:46)
	at scala.collection.immutable.List.foldRight(List.scala:352)
	at at.forsyte.apalache.tla.typecheck.TypeCheckerTool.check(TypeCheckerTool.scala:45)
	at at.forsyte.apalache.tla.passes.typecheck.EtcTypeCheckerPassImpl.execute(EtcTypeCheckerPassImpl.scala:54)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.exec(PassChainExecutor.scala:64)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$3(PassChainExecutor.scala:53)
	at scala.util.Either.flatMap(Either.scala:352)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$1(PassChainExecutor.scala:51)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
	at scala.collection.LinearSeqOps.foldLeft\$(LinearSeq.scala:179)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.runOnPasses(PassChainExecutor.scala:44)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:34)
	at at.forsyte.apalache.tla.tooling.opt.TypeCheckCmd.run(TypeCheckCmd.scala:41)
	at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:138)
	at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:118)
	at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)

System information

• Apalache version: 0.44.2 build v0.44.2
• OS: Linux
• JDK version: 17.0.9

Triage checklist (for maintainers)

• Reproduce the bug on the main development branch.
• Add the issue to the apalache GitHub project.
• If the bug is high impact, ensure someone available is assigned to fix it.

[shonfeder]

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

[shonfeder]

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)

[nano-o]

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?

[shonfeder]

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

[shonfeder]

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:

https://github.com/informalsystems/apalache/blob/99fb4d288aff9a7b19079366e9c09b033058f8e4/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala#L894-L896

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.

[shonfeder]

@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?

[nano-o]

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

[nano-o]

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