Module references considered differently SANY and TLAPM

[kape1395]

Here is a situation where a module extends ref and ref2. They both internally contain a local instance of the module sub.

In this module:

---- MODULE test_li ----
EXTENDS test_li_ref, test_li_ref2                        \* Works with TLAPS
\* EXTENDS test_li_ref, test_li_ref2, test_li_sub        \* Works with SANY
THEOREM ASSUME NEW a, NEW b, AnotherOperator(a, b, =) PROVE a = b
    BY DEF AnotherOperator, ImportantOperator
====

The TLAPS proof works if I extend ref and ref2 and fails if I add sub to the extends list. The failure:

[ERROR]: Could not prove or check:
           ASSUME AnotherOperator(a, b, op(_, _)) ==
                    ImportantOperator(a, b, op),
                  ImportantOperator_1(a, b, op(_, _)) == op(a, b),
                  NEW CONSTANT a,
                  NEW CONSTANT b,
                  AnotherOperator(a, b, =) 
           PROVE  a = b

For the SANY parser, the situation is the opposite. It fails if I omit the sub module in the extends clause with

Unknown operator: `ImportantOperator'.
DEF clause entry should describe a defined operator.

Below are the referenced modules.

---- MODULE test_li_sub ----
ImportantOperator(a, b, op(_, _)) == op(a, b)
====

---- MODULE test_li_ref ----
LOCAL INSTANCE test_li_sub
AnotherOperator(a, b, op(_, _)) == ImportantOperator(a, b, op)
====

---- MODULE test_li_ref2 ----
LOCAL INSTANCE test_li_sub
AnotherOperator2(a, b, op(_, _)) == ImportantOperator(a, b, op)
====

I don't know if SANY or TLAPS should be fixed.

[muenchnerkindl]

Ah, local instances ... personally, I think they should be removed from TLA+. Or perhaps there should be a mechanism for opening up local contexts.

Concerning your question, I think that TLAPS is wrong in accepting the statement of the theorem. Since the definition of ImportantOperator local, it is not exported by modules ref or ref2, and one should not be able to use it in module test_li. Presumably SANY is right, although it is not entirely clear to me how it determines that EXTENDing sub actually imports the same ImportantOperator as the one from the local instance(s). TLAPS tries to err on the cautious side by assigning a new name ImportantOperator_1 to the operator that comes from the EXTENDed module – but then, I don't understand what it thinks that ImportantOperator refers to (perhaps just an uninterpreted operator?).

The details of module semantics are explained in section 17.5 of Specifying Systems but I'd say that the description is not crystal-clear.

As long as local instances are part of TLA+, I think the choice that SANY makes is sensible because it allows a user to refer to the definitions of local operators by tracing the origins of the operators from the INSTANCEd and the EXTENDed modules to be the same. Alternatively, one would have to assert and prove theorems about the operator inside module test_li_sub, then restate these theorems in the modules that instantiate it.

[kape1395]

@muenchnerkindl, I faced this problem in PR https://github.com/tlaplus/CommunityModules/pull/99. Maybe those local instances should be replaced by EXTENDS instead of trying to make them work properly.

[muenchnerkindl]

Actually, they used to be EXTENDS but then they were converted for better hygiene of names, and I guess that makes sense in principle. Reverting them back to EXTENDS or plain INSTANCEs would certainly make life easier for the prover but eventually I think we need to figure out a way to handle local instances (or in fact, any local definitions) properly. The way SANY handles the combination of EXTENDS and INSTANCE seems to be feasible, so perhaps we should get TLAPS to do the same. But there are probably more urgent issues.

@damiendoligez What do you think?

[kape1395]

The proofs can refer to sub-expressions with ! notation. Could the proof access the local definitions by test_li_ref!ImportantOperator?

The SANY approach is not clear to me as a user because it's not obvious how the local instances relate to the definitions obtained by EXTENDS. And it would probably not work for different modules having local definitions with the same name and different meanings. After reading section 17.5 of Specifying Systems, I imagine that's a permitted case.

[muenchnerkindl]

The ! notation works for named instances: after

S == INSTANCE test_lib_sub

you can (and in fact have to) write S!ImportantOperator. It does not work for anonymous INSTANCE or for EXTENDS. Also, if S is a LOCAL INSTANCE then you still cannot refer to S!ImportantOperator in a module that EXTENDS the instantiating module (such as your module test_li).

SANY traces back the origin of operators. But you certainly cannot EXTEND two different modules that define an operator of the same name. Again, I am not defending the module system of TLA+: I am sure it could be improved – but that's the current state.

[kape1395]

A question from another angle. Why do the theorems and their proofs tend to be put separately from the main specification/definitions?

[muenchnerkindl]

For adding theorems about standard modules, we didn't want to touch TLA+'s standard library that seems to be cast in stone. Also, TLC users probably just don't care about theorems.

The proofs were separated from the theorems later simply because we found it unwieldy to browse the theorems when 80% of the module text was proofs. Better display and navigation capabilities would have helped to avoid this. For example, Isabelle can generate pdfs that either represent the full theory or elide the proofs. (One downside of having separate _theorems and _proofs modules is that they have to be kept in sync.)