Imports and exports

[konnov]

As we have discussed, in the recent implementation of import and export keywords, we have (somewhat unexpectedly) introduced a large feature space. The purpose of this discussion is to enumerate all possible combinations of using import and export and figure out which behaviour is considered valid. This is needed for synchronisation between the VSCode plugin, quint repl, quint run, quint test, and quint verify.

[konnov]

Use case 1.

module A {
  var x: int

  action aInit = x' = 0
  action aStep = x' = x + 1
}

module B {
  import A.*

  action bInit = aInit
  // x is visible in bStep
  action bStep = all { x >= 0, aStep }
}

// C can be the internal module constructed by REPL
module C {
  import B.*

  action cInit = bInit
  action cStep = bStep
  // aInit, aStep, and x are not visible in C 
}

The expectation. The module B imports all the definitions from A, without reexporting them, C uses the definitions of B.

The VSCode is OK ✅

REPL ✅:

$ quint repl -r t.qnt::C                                           
Quint REPL 0.11.1
Type ".exit" to exit, or ".help" for more information

>>> cInit
true
>>> cStep
true
>>> 

The simulator ✅:

$ quint run --main=C --init=cInit --step=cStep t.qnt

The transpiler ✅:

$ quint verify --main=C --init=cInit --step=cStep t.qnt

[konnov]

Use case 2.

module A {
  var x: int

  action aInit = x' = 0
  action aStep = x' = x + 1
}

module B {
  import A as A2
  export A2.*

  action bInit = A2::aInit
  // x is visible in bStep
  action bStep = all { A2::x >= 0, A2::aStep }
}

// C can be the internal module constructed by REPL
module C {
  import B.*

  action cInit = bInit
  action cStep = bStep
  // aInit, aStep, and x are visible in C
  action cInit2 = aInit
  action cStep2 = all { x >= 0, aStep }
}

The expectation. export A2.* exports all definitions of A without the prefix A2. Hence, C should have access to the definitions aInit and x.

This does not work in VSCode ❌

This does not work in REPL ❌

$ quint repl -r t.qnt::C                                          
Quint REPL 0.11.2
Type ".exit" to exit, or ".help" for more information
syntax error: error: Failed to resolve name aInit in definition for cInit2, in module C
  action cInit2 = aInit
                  ^^^^^

This does not work in the simulator ❌

$ quint run --main=C --init=cInit --step=cStep t.qnt              
.../quint/t.qnt:24:19 - error: Failed to resolve name aInit in definition for cInit2, in module C
24:   action cInit2 = aInit
                      ^^^^^

This does not work in the transpiler ❌

$ quint verify --main=C --init=cInit --step=cStep t.qnt
.../quint/t.qnt:24:19 - error: Failed to resolve name aInit in definition for cInit2, in module C
24:   action cInit2 = aInit
                      ^^^^^

[konnov]

@bugarela, do we expect this spec to work?

[bugarela]

Yes. I couldn't find any obvious issue, I'd have to debug it to understand why it is not working.

[bugarela]

This was a small bug in the name collector, where I was not saving the table for A2 (only with instances, not for imports). I fixed it locally and this example works on all commands.

[bugarela]

Here it is #1030

[konnov]

Use case 3. The third use case using a single instance.

module A {
  const N: int
  var x: int

  action aInit = x' = 0
  action aStep = x' = x + N
}

module B {
  import A(N=2) as A2
  export A2.*

  action bInit = A2::aInit
  // x is visible in bStep
  action bStep = all { A2::x >= 0, A2::aStep }
}

// C can be the internal module constructed by REPL
module C {
  import B.*

  action cInit = bInit
  action cStep = bStep
  // aInit, aStep, and x are visible in C
  action cInit2 = aInit
  action cStep2 = all { x >= 0, aStep }
}

The expectation. import A(N=2) as A2 creates a new instance of A with N=2 and places all definitions under the namespace A2. C imports all definitions of B, including aInit and x (without the need for the prefix A2).

This does work in VSCode ✅

REPL is quite confused here ❌

$ quint repl -r t.qnt::C                               
Quint REPL 0.11.2
Type ".exit" to exit, or ".help" for more information

>>> cInit
true
[warning] some variables are undefined: x
>>> cStep
true
[warning] some variables are undefined: x
>>> A::x
syntax error: error: Failed to resolve name A::x in definition for q::input, in module __repl__
A::x
^^^^


>>> x
runtime error: error: Variable x is not set
  var x: int
  ^^^^^^^^^^

<undefined value>

This works in the simulator, though it uses the variable A2::x, even though export A2.* should have exported A2::x as x 🎲

$ quint run --main=C --init=cInit --step=cStep t.qnt   
An example execution:

[State 0] { A2::x: 0 }
...

The Apalache transpiler is confused ❌

$ quint verify --main=C --init=cInit --step=cStep t.qnt
error: Assignment error: No assignments found for: x

[bugarela]

The REPL is confused because it doesn't know that both A2::x and x refer to the same variable. While bInit and bStep are manipulating A2::x, cInit2 and cStep2 are manipulating x.

It works in the simulator since cInit2 and cStep2 are not called at all.

[konnov]

Use case 4. For some reason it works, though it works somewhat unexpected.

module A {
  const N: int
  var x: int

  action aInit = x' = 0
  action aStep = x' = x + N
}

module B {
  import A(N=2).*

  action bInit = aInit
  // x is visible in bStep
  action bStep = all { x >= 0, aStep }
}

The expectation. import A(N=2).* creates an instances of A with N=2 and adds all definitions into the namespace of B. However, I would not expect import A(N=2).* to export the definitions of A.

This works in VSCode ✅

This works in REPL but it may be confusing 🪲

$ quint repl -r t.qnt::B
Quint REPL 0.11.2
Type ".exit" to exit, or ".help" for more information

>>> bInit
true
>>> bStep
true
>>> x
2

Although it works in REPL, I did not expect it. Apparently, when we instantiate a module, it is exported automatically. I think this is where we have got confused: Normal imports do not export names, whereas instances export names.

What makes it worse, when I import the module B via import instead of -r, it stops working ❌

$ quint repl
Quint REPL 0.11.2
Type ".exit" to exit, or ".help" for more information
>>> import B.* from "./t"
syntax error: error: [QNT404] Module B not found
import B.* from "./t"
^^^^^^^^^^^^^^^^^^^^^


>>>

It works in the simulator as expected ✅

$ quint run --main=B --init=bInit --step=bStep t.qnt
An example execution:

[State 0] { x: 0 }
...

It works in the transpiler as expected ✅

$ quint verify --main=B --init=bInit --step=bStep t.qnt

[bugarela]

What makes it worse, when I import the module B via import instead of -r, it stops working

I'm pretty sure that's an unrelated bug

[bugarela]

As for why aInit is available in the REPL even tho it is not exported, I found the reason and was able to fix it: flattening assumes the name resolver already caught any errors (such as aInit not being available), and then doesn't worry about visibility. However, in incremental compilation, by the time we type aInit into the REPL, it would have already resolved the names (which worked before we typed aInit) and flattened, and adding aInit to the flattened version of the module is not an issue.

I fixed it by keeping the original unflattened modules in the compilation state, and then using that to resolve names. This way, an error is flagged when we type aInit:

$ quint repl -r t.qnt::B
Quint REPL 0.12.0
Type ".exit" to exit, or ".help" for more information

>>> aInit
syntax error: error: [QNT404] Name 'aInit' not found
aInit
^^^^^

>>> bInit
true

[bugarela]

Fix is here: #1031

[konnov]

Use case 5.

module A {
  const N: int
  var x: int

  action aInit = x' = 0
  action aStep = x' = x + N
}

module B {
  import A(N=2) as A2
  import A(N=3) as A3

  action bInit = all { A2::aInit, A3::bInit }
  action bStep = all { A2::aStep, A3::bStep }
}

The expectation. import A(N=2) as A2 creates an instance of A with N=2 and places all new definitions under the namespace A2. import A(N=3) as A3 does a similar thing but for N=3 and the namespace A3. Both A2::aInit and A3::bInit should be visible in B.

The VSCode is not working ❌

REPL is not working ❌

$ quint repl -r t.qnt::B                               
Quint REPL 0.11.2
Type ".exit" to exit, or ".help" for more information
syntax error: error: Failed to resolve name A3::bInit in definition for bInit, in module B
  action bInit = all { A2::aInit, A3::bInit }
                                  ^^^^^^^^^

The simulator is not working ❌

$ quint run --main=B --init=bInit --step=bStep t.qnt
.../quint/t.qnt:13:35 - error: Failed to resolve name A3::bInit in definition for bInit, in module B
13:   action bInit = all { A2::aInit, A3::bInit }

The transpiler is not working ❌

$ quint verify --main=B --init=bInit --step=bStep t.qnt
.../quint/t.qnt:13:35 - error: Failed to resolve name A3::bInit in definition for bInit, in module B
13:   action bInit = all { A2::aInit, A3::bInit }

[bugarela]

I think you meant A3::aInit (and A3::aStep) in this example.

[konnov]

Indeed, there was a typo. Here is the revised version, which is failing in the effect checker.

module A {
  const N: int
  var x: int

  action aInit = x' = 0
  action aStep = x' = x + N
}

module B {
  import A(N=2) as A2
  import A(N=3) as A3

  action bInit = all { A2::aInit, A3::aInit }
  action bStep = all { A2::aStep, A3::aStep }
}

[bugarela]

#1290 fixes this

[konnov]

Use case 6. Exporting all the names from the namespace.

Consider the following example:

module A {
  const N: int
  var x: int

  action aInit = x' = 0
  action aStep = x' = x + N
}

module B {
  import A.*
  export *

  action bInit = A2::aInit
  // x is visible in bStep
  action bStep = all { A2::x >= 0, A2::aStep }
}

// C can be the internal module constructed by REPL
module C {
  import B(N = 2).*
  export *

  action cInit = bInit
  action cStep = bStep
  // aInit, aStep, and x are visible in C
  action cInit2 = aInit
  action cStep2 = all { x >= 0, aStep }
}

Expected behavior. All names of A are imported into B and exported by B. Further, C produces an instance of B and exports all the names (including those of the instance).

Currently, we do not have syntax for that. However, it should be really easy to introduce export *. This patterns is needed, for instance, in Tendermint.

[konnov]

@bugarela wdyt? It looks like export * can compensate for many problems. It may also be the default option for the people who are lost in imports.

[bugarela]

Seems like a good idea! Easy to use and easy to implement :)

[konnov]

Use case 7. Importing and exporting names across files.

Consider the following three module definitions scattered across three files:

File A.qnt:

module A {
  const N: int
  var x: int

  action aInit = x' = 0
  action aStep = x' = x + N
}

File B.qnt:

module B {
  import A as A2 from "./A"
  export A2.*

  action bInit = A2::aInit
  // x is visible in bStep
  action bStep = all { A2::x >= 0, A2::aStep }
}

File C.qnt:

module C {
  import B(N = 2) as B2 from "./B"
  export B2.*

  action cInit = bInit
  action cStep = bStep
  // aInit, aStep, and x are visible in C
  action cInit2 = aInit
  action cStep2 = all { x >= 0, aStep }
}

Expected behavior. Module B imports and exports all names that are defined in the module A, which is defined in the file A.qnt. Module C instantiates B for N=2 and exports all names defined in B.

Current behavior. The parser does not accept B.qnt and C.qnt:

$ quint parse B.qnt
.../B.qnt:3:3 - error: [QNT405] Module 'A2' not found
3:   export A2.*
     ^^^^^^^^^^^

error: parsing failed

$ quint parse C.qnt
.../B.qnt:3:3 - error: [QNT405] Module 'A2' not found
3:   export B2.*
     ^^^^^^^^^^^

.../C.qnt:2:3 - error: [QNT406] Instantiation error: 'N' not found in 'B'
2:   import B(N = 2) as B2 from "./B"
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.../C.qnt:2:12 - error: [QNT404] Name 'B2::N' not found
2:   import B(N = 2) as B2 from "./B"
              ^

.../C.qnt:8:19 - error: [QNT404] Name 'aInit' not found
8:   action cInit2 = aInit
                     ^^^^^

.../C.qnt:9:25 - error: [QNT404] Name 'x' not found
9:   action cStep2 = all { x >= 0, aStep }
                           ^

.../C.qnt:9:33 - error: [QNT404] Name 'aStep' not found
9:   action cStep2 = all { x >= 0, aStep }
                                   ^^^^^

error: parsing failed

[bugarela]

This is the same problem of #949 (reply in thread). My fix for that also fixes this.

[bugarela]

After meeting about this subject twice this week, here's what we believe we should do:

• Use instance keyword for instances (instead of using import)
• Allow instancing modules that don't have any constants
• Restrict export of instances to export <instance-name>

With this, we should end up with the following semantics:

Imports: import <module> [as <alias> | .<name>] [from <file>]

1. Importing a module with no constants: a simple standard import
2. Importing a module with constants: if B imports A and A has constants, B will have any of these constants that are referenced by the usage of A in B.
   • This is the current behavior, and although very implicit, it works well for the few use cases that we have (i.e. Tendermint). We might want to reconsider this once we have more use cases.

Imported definitions are static in the sense that all occurrences of the same original def, in different modules or with different namespaces, always have the same id, meaning they are always treated as the same component. For example, importing a module with state variables under two different names (i.e. import A as A1 and import A as A2) will result in two names for each state variable, but updating either of those names will affect the other.

>>> import A as A1

>>> import A as A2

>>> A1::x' = 1
true
>>> A2::x
1

Instances: instance <module>[(<overrides>)] [as <alias>] [from <file>]

• Instancing a module always replaces all constants with pure values. An error should be raise if there is an override missing for a module's constant.
• Instancing a module always generates new IR components for all the components in the module being instanced
  • Therefore, even if the module has no constants, it makes sense to instance it if you want fresh state variables.

Desired behavior (not implemented yet):

>>> instance A as A1

>>> instance A as A2

>>> A1::x' = 1
true
>>> A2::x' = 2
true
>>> A1::x
1
>>> A2::x
2

Exports: export <module> [as <alias> | .<name>]

Exporting should behave like there is always a matching import/instance for each export. That is, it should be impossible to export a name that is not available in the module.

1. Exporting imported names

• import A as A1 can be exported with either export A as A1 or export A1
• import A can be exported with export A
• import A.* can be exported with export A.*
• import A.name can be exported with export A.name

2. Exporting instanced names

• instance A(...) as A1 can be exported with export A1

All other usages of export should result in an error.

cc @konnov @Kukovec @shonfeder

[shonfeder]

Thanks for the writeup!

A few notes:

1. Let's use this opportunity to replace the incongruous . syntax for value imports with the more consistent :: syntax, so that it matches how we reference these values. Any objections?
2. The behavior on importing modules with constants seems like a foot gun. One of our aims to make quint intuitive to programmers. Making import silently act like a class extends but on the module level really goes against this. The fact that we are using this in one place doesn't seem like a good justification for keeping this behavior, IMO. We can just find a more intuitive and explicit syntax, and change the one or two places we are using it.
3. Related to (2), what the behavior around importing a single value from a module given these semantics seems particularly confusing. Could you outline what is supposed to happen if we have module A { const X:int; val foo = X }; module B { import A::foo }?

All the rest sounds great to me! 🎉

[bugarela]

1. Yes! No objections
2. I see your point, but I also don't have any better ideas. Do you have something in mind?
3. I agree it's confusing. This currently works:

module A { const X: int val foo = X }
module B { import A.* export A.* }
module C { import B(X=1) as B1 }

But replacing * with foo results in a sort of impossible situation: the runtime requires that X is set for B (i.e. import B(X=1) ...), but the name resolver won't let you set X because X is not a constant in B (until flattening happens). So, in practice, we don't allow that to happen - which I think its a good thing? Do you have a behavior in mind you think should happen, or is it improving the error messages the thing to be done here?

[shonfeder]

3. Here's the behavior I am seeing on HEAD:

Given

module A {
  const X: int
  val f = X
}

module B {
  import A.f

  val g = f
}

module C {
  import B

  val h = B::g
}

module D {
  import C.h

  val i = h
}

quint typecheck succeeds.

However, loading the modules in the repl, we find that modules B, C, and D are
(afaict) broken and unusable at run time. E.g.:

$  quint -r t.qnt
Quint REPL 0.14.3
Type ".exit" to exit, or ".help" for more information
>>> import D

>>> D::i
compile error: error: QNT500: Uninitialized const D::B::X. Use: import <moduleName>(D::B::X=<value>).*
  const X: int
  ^^^^^^^^^^^^

compile error: error: Name D::B::X not found
  val f = X
          ^

compile error: error: QNT500: Uninitialized const B::D::B::X. Use: import <moduleName>(B::D::B::X=<value>).*
  const X: int
  ^^^^^^^^^^^^

compile error: error: Name B::D::B::X not found
  val f = X
          ^


>>> import D(X = 2) as D1
syntax error: error: [QNT406] Instantiation error: 'X' not found in 'D'
import D(X = 2) as D1
^^^^^^^^^^^^^^^^^^^^^

syntax error: error: [QNT404] Name 'D1::X' not found
import D(X = 2) as D1
         ^


>>> import A(X = 2) as A1
compile error: error: QNT500: Uninitialized const D::B::X. Use: import <moduleName>(D::B::X=<value>).*
  const X: int
  ^^^^^^^^^^^^

compile error: error: Name D::B::X not found
  val f = X
          ^

compile error: error: QNT500: Uninitialized const B::D::B::X. Use: import <moduleName>(B::D::B::X=<value>).*
  const X: int
  ^^^^^^^^^^^^

compile error: error: Name B::D::B::X not found
  val f = X
          ^

However, if we use the import M[.ident] ; export M.* construct, then we can
both import a single value from A and inherit its constants:

module A {
  const X: int
  val f = X
}

module B {
  import A.f
  export A.*

  val g = f
}

>>> import B(X=2) as B1

>>> B1::g
2

As I understand things, modules that declare constants are parametric. We should
indeed error when trying to access any data inside a parametric term, but this
should happen during static checking, just as in this analogous case:

>>> def A(X:int): {X:int, f:int} = {X:X, f:X}

>>> A.f
static analysis error: error: [QNT000] Couldn't unify oper and rec
Trying to unify (int) => { X: int, f: int } and { f: t0 | tail_t0 }

A.f
^^^

>>> A(2).f
2

A.f is invalid because the statics of quint dictate that record projection is
ill-typed on a parametric value, i.e., an operator. Similarly, import A::f is
invalid because the statics of quint dictate that module projection is ill-typed
on a parametric module, (i.e., a "functor" in MLese :) ).

In short: our modules have types. They are either non-parametric modules of type
module, or parametric modules of type (c1: t1, ..., cn: tn) ==> module

2. I can elaborate on my reasoning here, but basically I think we should add an extends keyword as the complement of instance.

moudle M {
  extends A
}

extends should only work on parametric modules, and will cause M to inherit constants.