informalsystems/quintPublic

NotificationsYou must be signed in to change notification settings
Fork79
Star950

Imports and exports#949

konnov started this conversation inUser stories

konnov

Jun 15, 2023

· 9 comments· 16 replies

Return to top

Discussion options

konnov
Jun 15, 2023

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

You must be logged in to vote

Replies: 9 comments 16 replies

Comment options

konnov
Jun 15, 2023
Author

Use case 1.

module A{  var x: intaction aInit= x'=0action aStep= x'= x+1}module B{importA.*action bInit= aInit// x is visible in bStepaction bStep= all{ x>=0, aStep}}// C can be the internal module constructed by REPLmodule C{importB.*action cInit= bInitaction cStep= bStep// aInit, aStep, and x are not visible in C}

The expectation. The moduleB imports all the definitions fromA, without reexporting them,C uses the definitions ofB.

The VSCode is OK ✅

REPL ✅:

$ quint repl-r t.qnt::C                                           Quint REPL0.11.1Type".exit" to exit,or".help"for more information>>> cInittrue>>> cSteptrue>>>

The simulator ✅:

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

The transpiler ✅:

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

You must be logged in to vote

0 replies

Comment options

konnov
Jun 15, 2023
Author

Use case 2.

module A{  var x: intaction aInit= x'=0action aStep= x'= x+1}module B{importA as A2exportA2.*action bInit= A2::aInit// x is visible in bStepaction bStep= all{ A2::x>=0, A2::aStep}}// C can be the internal module constructed by REPLmodule C{importB.*action cInit= bInitaction cStep= bStep// aInit, aStep, and x are visible in Caction cInit2= aInitaction cStep2= all{ x>=0, aStep}}

The expectation.export A2.* exports all definitions ofA without the prefixA2. Hence,C should have access to the definitionsaInit andx.

This does not work in VSCode ❌

This does not work in REPL ❌

$ quint repl-r t.qnt::C                                          Quint REPL0.11.2Type".exit" to exit,or".help"for more informationsyntax error: error: Failed to resolve name aInit in definitionfor cInit2, inmodule Caction 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 definitionfor cInit2, inmodule C24: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 definitionfor cInit2, inmodule C24:action cInit2= aInit^^^^^

You must be logged in to vote

4 replies

Comment options

konnov Jun 20, 2023
Author

@bugarela, do we expect this spec to work?

Comment options

bugarela Jun 20, 2023
Maintainer

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

Comment options

bugarela Jul 6, 2023
Maintainer

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.

Comment options

bugarela Jul 10, 2023
Maintainer

Here it is#1030

Comment options

konnov
Jun 20, 2023
Author

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

module A{  const N: int  var x: intaction aInit= x'=0action aStep= x'= x+ N}module B{importA(N=2) as A2exportA2.*action bInit= A2::aInit// x is visible in bStepaction bStep= all{ A2::x>=0, A2::aStep}}// C can be the internal module constructed by REPLmodule C{importB.*action cInit= bInitaction cStep= bStep// aInit, aStep, and x are visible in Caction cInit2= aInitaction cStep2= all{ x>=0, aStep}}

The expectation.import A(N=2) as A2 creates a new instance ofA withN=2 and places all definitions under the namespaceA2.C imports all definitions ofB, includingaInit andx (without the need for the prefixA2).

This does work in VSCode ✅

REPL is quite confused here ❌

$ quint repl-r t.qnt::C                               Quint REPL0.11.2Type".exit" to exit,or".help"for more information>>> cInittrue[warning] some variables are undefined: x>>> cSteptrue[warning] some variables are undefined: x>>> A::xsyntax error: error: Failed to resolve name A::x in definitionfor q::input, inmodule __repl__A::x^^^^>>> xruntime error: error: Variable x isnot set  var x: int^^^^^^^^^^<undefined value>

This works in the simulator, though it uses the variableA2::x, even thoughexport A2.* should have exportedA2::x asx 🎲

$ 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.qnterror: Assignment error: No assignments found for: x

You must be logged in to vote

1 reply

Comment options

bugarela Jul 6, 2023
Maintainer

The REPL is confused because it doesn't know that bothA2::x andx refer to the same variable. WhilebInit andbStep are manipulatingA2::x,cInit2 andcStep2 are manipulatingx.

It works in the simulator sincecInit2 andcStep2 are not called at all.

Comment options

konnov
Jun 20, 2023
Author

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

module A{  const N: int  var x: intaction aInit= x'=0action aStep= x'= x+ N}module B{importA(N=2).*action bInit= aInit// x is visible in bStepaction bStep= all{ x>=0, aStep}}

The expectation.import A(N=2).* creates an instances ofA withN=2 and adds all definitions into the namespace ofB. However, I would not expectimport A(N=2).* to export the definitions ofA.

This works in VSCode ✅

This works in REPL but it may be confusing 🪲

$ quint repl-r t.qnt::BQuint REPL0.11.2Type".exit" to exit,or".help"for more information>>> bInittrue>>> bSteptrue>>> x2

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 moduleB viaimport instead of-r, it stops working ❌

$ quint replQuint REPL0.11.2Type".exit" to exit,or".help"for more information>>>import B.* from"./t"syntax error: error:[QNT404]Module Bnot foundimportB.* from"./t"^^^^^^^^^^^^^^^^^^^^^>>>

It works in the simulator as expected ✅

$ quint run--main=B--init=bInit--step=bStep t.qntAn example execution:[State0] {x:0}...

It works in the transpiler as expected ✅

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

You must be logged in to vote

3 replies

Comment options

bugarela Jul 6, 2023
Maintainer

What makes it worse, when I import the moduleB viaimport instead of-r, it stops working

I'm pretty sure that's an unrelated bug

Comment options

bugarela Jul 6, 2023
Maintainer

As for whyaInit 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 asaInit not being available), and then doesn't worry about visibility. However, in incremental compilation, by the time we typeaInit into the REPL, it would have already resolved the names (which worked before we typedaInit) and flattened, and addingaInit 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 typeaInit:

$ quint repl -r t.qnt::BQuint REPL 0.12.0Type ".exit" to exit, or ".help" for more information>>> aInitsyntax error: error: [QNT404] Name 'aInit' not foundaInit^^^^^>>> bInittrue

Comment options

bugarela Jul 10, 2023
Maintainer

Fix is here:#1031

Comment options

konnov
Jun 20, 2023
Author

Use case 5.

module A{  const N: int  var x: intaction aInit= x'=0action aStep= x'= x+ N}module B{importA(N=2) as A2importA(N=3) as A3action bInit= all{ A2::aInit, A3::bInit}action bStep= all{ A2::aStep, A3::bStep}}

The expectation.import A(N=2) as A2 creates an instance ofA withN=2 and places all new definitions under the namespaceA2.import A(N=3) as A3 does a similar thing but forN=3 and the namespaceA3. BothA2::aInit andA3::bInit should be visible inB.

The VSCode is not working ❌

REPL is not working ❌

$ quint repl-r t.qnt::B                               Quint REPL0.11.2Type".exit" to exit,or".help"for more informationsyntax error: error: Failed to resolve name A3::bInit in definitionfor bInit, inmodule Baction 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 definitionfor bInit, inmodule B13: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 definitionfor bInit, inmodule B13:action bInit= all{ A2::aInit, A3::bInit}

You must be logged in to vote

3 replies

Comment options

bugarela Jun 20, 2023
Maintainer

I think you meantA3::aInit (andA3::aStep) in this example.

Comment options

konnov Jul 6, 2023
Author

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

module A{  const N: int  var x: intaction aInit= x'=0action aStep= x'= x+ N}module B{importA(N=2) as A2importA(N=3) as A3action bInit= all{ A2::aInit, A3::aInit}action bStep= all{ A2::aStep, A3::aStep}}

Comment options

bugarela Dec 5, 2023
Maintainer

#1290 fixes this

Comment options

konnov
Jul 7, 2023
Author

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

Consider the following example:

module A{  const N: int  var x: intaction aInit= x'=0action aStep= x'= x+ N}module B{importA.*  export*action bInit= A2::aInit// x is visible in bStepaction bStep= all{ A2::x>=0, A2::aStep}}// C can be the internal module constructed by REPLmodule C{importB(N=2).*  export*action cInit= bInitaction cStep= bStep// aInit, aStep, and x are visible in Caction cInit2= aInitaction cStep2= all{ x>=0, aStep}}

Expected behavior.All names ofA are imported intoB and exported byB. Further,C produces an instance ofB 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 introduceexport *. This patterns is needed, for instance, inTendermint.

You must be logged in to vote

2 replies

Comment options

konnov Jul 7, 2023
Author

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

Comment options

bugarela Jul 7, 2023
Maintainer

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

Comment options

konnov
Jul 7, 2023
Author

Use case 7. Importing and exporting names across files.

Consider the following three module definitions scattered across three files:

FileA.qnt:

module A{  const N: int  var x: intaction aInit= x'=0action aStep= x'= x+ N}

FileB.qnt:

module B{importA as A2 from"./A"exportA2.*action bInit= A2::aInit// x is visible in bStepaction bStep= all{ A2::x>=0, A2::aStep}}

FileC.qnt:

module C{importB(N=2) as B2 from"./B"exportB2.*action cInit= bInitaction cStep= bStep// aInit, aStep, and x are visible in Caction cInit2= aInitaction cStep2= all{ x>=0, aStep}}

Expected behavior. ModuleB imports and exports all names that are defined in the moduleA, which is defined in the fileA.qnt. ModuleC instantiatesB forN=2 and exports all names defined inB.

Current behavior. The parser does not acceptB.qnt andC.qnt:

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

$ quint parse C.qnt.../B.qnt:3:3 - error: [QNT405] Module'A2' not found3:export B2.*     ^^^^^^^^^^^.../C.qnt:2:3 - error: [QNT406] Instantiation error:'N' not foundin'B'2:   import B(N = 2) as B2 from"./B"     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^.../C.qnt:2:12 - error: [QNT404] Name'B2::N' not found2:   import B(N = 2) as B2 from"./B"              ^.../C.qnt:8:19 - error: [QNT404] Name'aInit' not found8:   action cInit2 = aInit                     ^^^^^.../C.qnt:9:25 - error: [QNT404] Name'x' not found9:   action cStep2 = all { x>= 0, aStep }                           ^.../C.qnt:9:33 - error: [QNT404] Name'aStep' not found9:   action cStep2 = all { x>= 0, aStep }                                   ^^^^^error: parsing failed

You must be logged in to vote

1 reply

Comment options

bugarela Jul 7, 2023
Maintainer

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

Comment options

bugarela
Sep 14, 2023
Maintainer

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

Useinstance keyword for instances (instead of usingimport)
Allow instancing modules that don't have any constants
Restrict export of instances toexport <instance-name>

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

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

Importing a module with no constants: a simple standard import
Importing a module with constants: ifB importsA andA has constants,B will have any of these constants that are referenced by the usage ofA inB.
- 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 andimport 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' = 1true>>> A2::x1

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' = 1true>>> A2::x' = 2true>>> A1::x1>>> A2::x2

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.

Exporting imported names

import A as A1 can be exported with eitherexport A as A1 orexport A1
import A can be exported withexport A
import A.* can be exported withexport A.*
import A.name can be exported withexport A.name

Exporting instanced names

instance A(...) as A1 can be exported withexport A1

All other usages of export should result in an error.

cc@konnov @Kukovec @shonfeder

You must be logged in to vote

2 replies

Comment options

shonfeder Sep 18, 2023

Thanks for the writeup!

A few notes:

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?
The behavior on importing modules with constants seems like a foot gun. One of our aims to make quint intuitive to programmers. Makingimport silently act like a classextends 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.
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 havemodule A { const X:int; val foo = X }; module B { import A::foo }?

All the rest sounds great to me! 🎉

Comment options

bugarela Sep 19, 2023
Maintainer

Yes! No objections
I see your point, but I also don't have any better ideas. Do you have something in mind?
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* withfoo results in a sort of impossible situation: the runtime requires thatX is set forB (i.e.import B(X=1) ...), but the name resolver won't let you setX becauseX is not a constant inB (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?

Comment options

shonfeder
Sep 26, 2023

Here's the behavior I am seeing on HEAD:

Given

moduleA {  constX: intvalf=X}moduleB {importA.fvalg= f}moduleC {importBvalh=B::g}moduleD {importC.hvali= 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.qntQuint REPL 0.14.3Type ".exit" to exit, or ".help" for more information>>> import D>>> D::icompile 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 D1syntax error: error: [QNT406] Instantiation error: 'X' not found in 'D'import D(X = 2) as D1^^^^^^^^^^^^^^^^^^^^^syntax error: error: [QNT404] Name 'D1::X' not foundimport D(X = 2) as D1         ^>>> import A(X = 2) as A1compile 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 theimport M[.ident] ; export M.* construct, then we can
both import a single value fromA 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::g2

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.fstatic analysis error: error: [QNT000] Couldn't unify oper and recTrying to unify (int) => { X: int, f: int } and { f: t0 | tail_t0 }A.f^^^>>> A(2).f2

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

I can elaborate on my reasoning here, but basically I think we should add anextends keyword as the complement ofinstance.

moudle M {  extends A}

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

You must be logged in to vote

0 replies

Movatterモバイル変換

Imports and exports#949

Uh oh!

Uh oh!

konnovJun 15, 2023

Replies: 9 comments· 16 replies

Uh oh!

Uh oh!

konnovJun 15, 2023 Author

Uh oh!

Uh oh!

konnovJun 15, 2023 Author

Uh oh!

konnovJun 20, 2023 Author

Uh oh!

bugarelaJun 20, 2023 Maintainer

Uh oh!

bugarelaJul 6, 2023 Maintainer

Uh oh!

bugarelaJul 10, 2023 Maintainer

Uh oh!

Uh oh!

konnovJun 20, 2023 Author

Uh oh!

bugarelaJul 6, 2023 Maintainer

Uh oh!

Uh oh!

konnovJun 20, 2023 Author

Uh oh!

bugarelaJul 6, 2023 Maintainer

Uh oh!

bugarelaJul 6, 2023 Maintainer

Uh oh!

bugarelaJul 10, 2023 Maintainer

Uh oh!

Uh oh!

konnovJun 20, 2023 Author

Uh oh!

bugarelaJun 20, 2023 Maintainer

Uh oh!

konnovJul 6, 2023 Author

Uh oh!

bugarelaDec 5, 2023 Maintainer

Uh oh!

konnovJul 7, 2023 Author

Uh oh!

konnovJul 7, 2023 Author

Uh oh!

bugarelaJul 7, 2023 Maintainer

Uh oh!

konnovJul 7, 2023 Author

Uh oh!

bugarelaJul 7, 2023 Maintainer

Uh oh!

bugarelaSep 14, 2023 Maintainer

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

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

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

Uh oh!

shonfederSep 18, 2023

Uh oh!

Uh oh!

bugarelaSep 19, 2023 Maintainer

Uh oh!

shonfederSep 26, 2023

Uh oh!

konnov
Jun 15, 2023

Replies: 9 comments 16 replies

konnov
Jun 15, 2023
Author

konnov
Jun 15, 2023
Author

konnov Jun 20, 2023
Author

bugarela Jun 20, 2023
Maintainer

bugarela Jul 6, 2023
Maintainer

bugarela Jul 10, 2023
Maintainer

konnov
Jun 20, 2023
Author

bugarela Jul 6, 2023
Maintainer

konnov
Jun 20, 2023
Author

bugarela Jul 6, 2023
Maintainer

bugarela Jul 6, 2023
Maintainer

bugarela Jul 10, 2023
Maintainer

konnov
Jun 20, 2023
Author

bugarela Jun 20, 2023
Maintainer

konnov Jul 6, 2023
Author

bugarela Dec 5, 2023
Maintainer

konnov
Jul 7, 2023
Author

konnov Jul 7, 2023
Author

bugarela Jul 7, 2023
Maintainer

konnov
Jul 7, 2023
Author

bugarela Jul 7, 2023
Maintainer

bugarela
Sep 14, 2023
Maintainer

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

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

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

shonfeder Sep 18, 2023

bugarela Sep 19, 2023
Maintainer

shonfeder
Sep 26, 2023