tlapm ending abnormally with Invalid_argument("List.combine") in level or arity checking

[lemmy]

TLAPS has been terminating unexpectedly on an existing proof since the pre-release https://github.com/tlaplus/tlapm/releases/tag/202208050903. This issue appears to be linked to level checking.

$ tools/tlaps15pre/bin/tlapm --cleanfp BlockingQueueFair.tla
(* fingerprints file ".tlacache/FiniteSets.tlaps/fingerprints" removed *)
(* created new ".tlacache/FiniteSets.tlaps/FiniteSets.thy" *)
(* fingerprints written in ".tlacache/FiniteSets.tlaps/fingerprints" *)
File "/workspaces/BlockingQueue/tools/tlaps15pre/lib/tlaps/FiniteSets.tla", line 1, character 1 to line 23, character 77:
[INFO]: All 0 obligation proved.
(* fingerprints file ".tlacache/TLAPS.tlaps/fingerprints" removed *)
(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "./TLAPS.tla", line 1, character 1 to line 311, character 77:
[INFO]: All 0 obligation proved.
(* fingerprints file ".tlacache/BlockingQueue.tlaps/fingerprints" removed *)
(* created new ".tlacache/BlockingQueue.tlaps/BlockingQueue.thy" *)
(* fingerprints written in ".tlacache/BlockingQueue.tlaps/fingerprints" *)
File "./BlockingQueue.tla", line 1, character 1 to line 152, character 77:
[INFO]: All 1 obligation proved.
 tlapm ending abnormally with Invalid_argument("List.combine")
Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Stdlib__list.combine in file "list.ml", line 305, characters 36-49
Called from E_levels.level_computation#expr.apply_operator.f in file "e_levels.ml", line 228, characters 28-55
Called from E_levels.level_computation#expr.apply_operator in file "e_levels.ml", line 234, characters 27-55
Called from E_levels.level_computation#expr in file "e_levels.ml", line 492, characters 23-40
Called from E_levels.level_computation#expr in file "e_levels.ml", line 620, characters 21-38
Called from E_action.lambdify in file "e_action.ml", line 2090, characters 12-39
Called from M_elab.lambdify_definition in file "m_elab.ml", line 244, characters 23-44
Called from M_elab.lambdify_enabled_cdot.object#definition in file "m_elab.ml", line 273, characters 21-46
Called from M_visit.map#module_unit in file "m_visit.ml", line 48, characters 12-47
Called from M_visit.map#module_units.f in file "m_visit.ml", line 33, characters 27-49
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from M_visit.map#module_units in file "m_visit.ml", line 36, characters 31-75
Called from M_elab.lambdify_enabled_cdot in file "m_elab.ml", line 302, characters 20-47
Called from M_elab.instantiate in file "m_elab.ml", line 530, characters 15-44
Called from M_elab.normalize.spin.create_instance in file "m_elab.ml", line 1349, characters 16-98
Called from M_elab.normalize in file "m_elab.ml", line 1457, characters 12-66
Called from Tlapm.process_module in file "tlapm.ml", line 293, characters 29-68
Called from Tlapm.main.f in file "tlapm.ml", line 503, characters 23-43
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Tlapm.main in file "tlapm.ml", line 506, characters 13-40
Called from Tlapm.init in file "tlapm.ml", line 518, characters 8-33

For comparison, 1.4.6 accepts BlockingQueue.tla just fine:

$ tools/tlaps/bin/tlapm --cleanfp BlockingQueueFair.tla
(* fingerprints file "BlockingQueueFair.tlaps/fingerprints" removed *)
** Unexpanded symbols: ---

** Unexpanded symbols: IsInjective, Get, vars, Put

** Unexpanded symbols: IsInjective, Next, vars

** Unexpanded symbols: IsInjective, Next, vars

** Unexpanded symbols: Next, vars, Put

** Unexpanded symbols: Next, vars

** Unexpanded symbols: IsInjective, Next, vars

** Unexpanded symbols: Next, Get, vars

** Unexpanded symbols: Next, vars

** Unexpanded symbols: IsInjective, Next

** Unexpanded symbols: ---

** Unexpanded symbols: BQS!vars, Get, vars, Put, BQS!Next, TypeInv

** Unexpanded symbols: BQS!vars, Next, vars, BQS!Next, TypeInv

** Unexpanded symbols: BQS!vars, Next, vars, BQS!Next, TypeInv

** Unexpanded symbols: BQS!vars, Next, vars, BQS!Next, TypeInv

** Unexpanded symbols: BQS!Get, Next, BQS!NotifyOther, vars, Put, TypeInv

** Unexpanded symbols: BQS!vars, Next, vars, BQS!Next, TypeInv

** Unexpanded symbols: BQS!vars, Next, vars, BQS!Next, TypeInv

** Unexpanded symbols: Next, BQS!Put, Get, BQS!NotifyOther, vars, TypeInv

** Unexpanded symbols: BQS!Get, Next, BQS!Put, TypeInv

(* created new "BlockingQueueFair.tlaps/BlockingQueueFair.thy" *)
(* fingerprints written in "BlockingQueueFair.tlaps/fingerprints" *)
$ tools/tlaps/bin/tlapm --version
1.4.5 (build 33809)

[lemmy]

Latest and greatest (6acb3cb) errors out right away:

-> % ~/.opam/5.1.0/bin/tlapm --version                      
6acb3cb

-> % ~/.opam/5.1.0/bin/tlapm --cleanfp BlockingQueueFair.tla
File "./BlockingQueue.tla", line 126, characters 21-28:
Error: Invalid number of arguments
 tlapm ending abnormally with Failure("Expr.Levels: ARITY")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm_lib__E_levels.level_computation#expr.apply_operator.f in file "src/expr/e_levels.ml", line 229, characters 20-49
Called from Tlapm_lib__E_levels.level_computation#expr.apply_operator in file "src/expr/e_levels.ml", line 236, characters 27-55
Called from Tlapm_lib__E_levels.level_computation#expr in file "src/expr/e_levels.ml", line 865, characters 21-36
Called from Tlapm_lib__E_levels.level_computation#expr in file "src/expr/e_levels.ml", line 622, characters 21-38
Called from Stdlib__List.rev_map.rmap_f in file "list.ml", line 105, characters 22-25
Called from Tlapm_lib__Ext.List.map in file "src/util/ext.ml", line 48, characters 22-37
Called from Tlapm_lib__E_levels.level_computation#expr.max_args_level in file "src/expr/e_levels.ml", line 148, characters 22-51
Called from Tlapm_lib__E_levels.level_computation#expr.level_info_from_args in file "src/expr/e_levels.ml", line 157, characters 43-66
Called from Tlapm_lib__E_levels.level_computation#expr in file "src/expr/e_levels.ml", line 606, characters 36-63
Called from Tlapm_lib__E_action.lambdify in file "src/expr/e_action.ml", line 1634, characters 12-39
Called from Tlapm_lib__M_elab.lambdify_expr in file "src/module/m_elab.ml" (inlined), line 228, characters 15-160
Called from Tlapm_lib__M_elab.lambdify_definition in file "src/module/m_elab.ml", line 243, characters 23-44
Called from Tlapm_lib__M_elab.lambdify_enabled_cdot.object#definition in file "src/module/m_elab.ml", line 272, characters 21-46
Called from Tlapm_lib__M_visit.map#module_unit in file "src/module/m_visit.ml", line 49, characters 12-47
Called from Tlapm_lib__M_visit.map#module_units.f in file "src/module/m_visit.ml", line 34, characters 27-49
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib__M_visit.map#module_units in file "src/module/m_visit.ml", line 37, characters 31-75
Called from Tlapm_lib__M_elab.lambdify_enabled_cdot in file "src/module/m_elab.ml", line 301, characters 20-47
Called from Tlapm_lib__M_elab.instantiate in file "src/module/m_elab.ml", line 529, characters 15-44
Called from Tlapm_lib__M_elab.normalize.spin.create_instance in file "src/module/m_elab.ml", line 1166, characters 16-98
Called from Tlapm_lib__M_elab.normalize in file "src/module/m_elab.ml", line 1274, characters 12-66
Called from Tlapm_lib.process_module in file "src/tlapm_lib.ml", line 320, characters 29-68
Called from Tlapm_lib.main.f in file "src/tlapm_lib.ml", line 574, characters 23-43
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib.main in file "src/tlapm_lib.ml", line 577, characters 13-40
Called from Tlapm_lib.init in file "src/tlapm_lib.ml", line 589, characters 8-33

[kape1395]

That's the minimal example that fails similarly. B1 is parsed successfully, but when parsing B2, it fails at B1 on Op(x).

---- MODULE B1 ----
Op(x) == TRUE
USE TRUE
OpAll == \A x : Op(x)
====

and

---- MODULE B2 ----
INSTANCE B1
====

Here, it is important to have an operator with an argument and USE of something before applying that operator.
@muenchnerkindl, maybe that points you to some particular place in the code?

The errors:

$ tlapm B1.tla 
(* created new ".tlacache/B1.tlaps/B1.thy" *)
(* fingerprints written in ".tlacache/B1.tlaps/fingerprints" *)
File "./B1.tla", line 1, character 1 to line 5, character 4:
[INFO]: All 1 obligation proved.

$ tlapm B2.tla 
 tlapm ending abnormally with Failure("unknown bound variable")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm_lib__E_levels.level_computation#expr in file "src/expr/e_levels.ml", line 254, characters 22-46
Called from Tlapm_lib__E_levels.level_computation#expr in file "src/expr/e_levels.ml", line 557, characters 22-38
Called from Tlapm_lib__E_levels.level_computation#expr in file "src/expr/e_levels.ml", line 622, characters 21-38
Called from Tlapm_lib__E_action.lambdify in file "src/expr/e_action.ml", line 1634, characters 12-39
Called from Tlapm_lib__M_elab.lambdify_expr in file "src/module/m_elab.ml" (inlined), line 228, characters 15-160
Called from Tlapm_lib__M_elab.lambdify_definition in file "src/module/m_elab.ml", line 243, characters 23-44
Called from Tlapm_lib__M_elab.lambdify_enabled_cdot.object#definition in file "src/module/m_elab.ml", line 272, characters 21-46
Called from Tlapm_lib__M_visit.map#module_unit in file "src/module/m_visit.ml", line 49, characters 12-47
Called from Tlapm_lib__M_visit.map#module_units.f in file "src/module/m_visit.ml", line 34, characters 27-49
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib__M_visit.map#module_units in file "src/module/m_visit.ml", line 37, characters 31-75
Called from Tlapm_lib__M_elab.lambdify_enabled_cdot in file "src/module/m_elab.ml", line 301, characters 20-47
Called from Tlapm_lib__M_elab.instantiate in file "src/module/m_elab.ml", line 529, characters 15-44
Called from Tlapm_lib__M_elab.normalize.spin.create_instance in file "src/module/m_elab.ml", line 1166, characters 16-98
Called from Tlapm_lib__M_elab.normalize in file "src/module/m_elab.ml", line 1274, characters 12-66
Called from Tlapm_lib.process_module in file "src/tlapm_lib.ml", line 320, characters 29-68
Called from Tlapm_lib.main.f in file "src/tlapm_lib.ml", line 574, characters 23-43
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib.main in file "src/tlapm_lib.ml", line 577, characters 13-40
Called from Tlapm_lib.init in file "src/tlapm_lib.ml", line 589, characters 8-33

[lemmy]

Removing the USE from BlockingQueue.tla allows TLAPS to prove BlockingQueueSplit.tla. However, BlockingQueueFair.tla fails with a new error that mentions EnabledWrapper, which is not defined or declared in my workspace:

-> % opam exec -- tlapm --nofp BlockingQueueFair.tla
File "./BlockingQueue.tla", line 116, characters 44-52:
[INFO]: Auto-expanding the definition of operator:  Put

File "./BlockingQueue.tla", line 36, characters 10-31:
[INFO]: Auto-expanding the definition of operator:  NotifyOther

File "./BlockingQueue.tla", line 38, characters 10-16:
[INFO]: Auto-expanding the definition of operator:  Wait

<unknown location>:
Error: Operator "EnabledWrapper" not found
 tlapm ending abnormally with Failure("Expr.Anon: 4")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm_lib__E_visit.map#expr in file "src/expr/e_visit.ml", line 273, characters 22-37
Called from Tlapm_lib__E_action.lambdify_action_operators#expand in file "src/expr/e_action.ml", line 941, characters 17-45
Called from Tlapm_lib__E_action.lambdify in file "src/expr/e_action.ml", line 1640, characters 12-142
Called from Tlapm_lib__M_elab.lambdify_expr in file "src/module/m_elab.ml" (inlined), line 228, characters 15-160
Called from Tlapm_lib__M_elab.lambdify_definition in file "src/module/m_elab.ml", line 243, characters 23-44
Called from Tlapm_lib__M_elab.lambdify_enabled_cdot.object#definition in file "src/module/m_elab.ml", line 272, characters 21-46
Called from Tlapm_lib__M_visit.map#module_unit in file "src/module/m_visit.ml", line 49, characters 12-47
Called from Tlapm_lib__M_visit.map#module_units.f in file "src/module/m_visit.ml", line 34, characters 27-49
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib__M_visit.map#module_units in file "src/module/m_visit.ml", line 37, characters 31-75
Called from Tlapm_lib__M_elab.lambdify_enabled_cdot in file "src/module/m_elab.ml", line 301, characters 20-47
Called from Tlapm_lib__M_elab.instantiate in file "src/module/m_elab.ml", line 529, characters 15-44
Called from Tlapm_lib__M_elab.normalize.spin.create_instance in file "src/module/m_elab.ml", line 1166, characters 16-98
Called from Tlapm_lib__M_elab.normalize in file "src/module/m_elab.ml", line 1274, characters 12-66
Called from Tlapm_lib.process_module in file "src/tlapm_lib.ml", line 320, characters 29-68
Called from Tlapm_lib.main.f in file "src/tlapm_lib.ml", line 574, characters 23-43
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib.main in file "src/tlapm_lib.ml", line 577, characters 13-40
Called from Tlapm_lib.init in file "src/tlapm_lib.ml", line 589, characters 8-33

[lemmy]

The EnabledWrapper error appears to be coming from the two levels of refinement: BGFair refines BGSplit refines BQ. No error if the INSTANCE statement removed in BQSplit.

diff --git a/BlockingQueueFair.tla b/BlockingQueueFair.tla
index 4c6fc6e..60b9596 100644
--- a/BlockingQueueFair.tla
+++ b/BlockingQueueFair.tla
@@ -78,11 +78,11 @@ BQS == INSTANCE BlockingQueueSplit WITH waitSetC <- Range(waitSeqC),
 BQSSpec == BQS!Spec
 THEOREM Spec => BQSSpec

-BQSFairSpec == BQS!A!FairSpec
-THEOREM FairSpec => BQSFairSpec
+\* BQSFairSpec == BQS!A!FairSpec
+\* THEOREM FairSpec => BQSFairSpec

-BQSStarvation == BQS!A!Starvation
-THEOREM FairSpec => BQSStarvation
+\* BQSStarvation == BQS!A!Starvation
+\* THEOREM FairSpec => BQSStarvation
 -----------------------------------------------------------------------------

 TypeInv == /\ Len(buffer) \in 0..BufCapacity
@@ -92,7 +92,6 @@ TypeInv == /\ Len(buffer) \in 0..BufCapacity
            \* Consumers
            /\ waitSeqC \in Seq(Consumers)
            /\ IsInjective(waitSeqC) \* no duplicates (thread is either asleep or not)!
-
 INSTANCE TLAPS

 (* Prove TypeInv inductive. *)
@@ -144,7 +143,7 @@ THEOREM ITypeInv == Spec => []TypeInv
   <2>4. QED
     BY <2>1, <2>2, <2>3 DEF Next
 <1>3. QED BY <1>1, <1>2, PTL DEF Spec
-
+====
 -----------------------------------------------------------------------------

diff --git a/BlockingQueueSplit.tla b/BlockingQueueSplit.tla
index afc10a0..ce224c9 100644
--- a/BlockingQueueSplit.tla
+++ b/BlockingQueueSplit.tla
@@ -73,8 +73,8 @@ Spec == Init /\ [][Next]_vars
 (* BlockingQueueSplit refines BlockingQueue. The refinement mapping is *)
 (* straight forward in this case. The union of waitSetC and waitSetP   *)
 (* maps to waitSet in the high-level spec BlockingQueue.               *)
+====
 A == INSTANCE BlockingQueue WITH waitSet <- (waitSetC \cup waitSetP)
-
 (* A!Spec is not a valid value in the config BlockingQueueSplit.cfg.   *)
 ASpec == A!Spec