Rearranging modules in the Tendermint spec

[konnov]

Refactoring the Tendermint spec a bit. Imports and exports do not seem to work as expected.

Update: imports and exports work with the new flattening, so we're finally opening this PR

[konnov]

Not sure why export does not work in TendermintTest. @bugarela, could you have a look?

[bugarela]

Not sure why export does not work in TendermintTest. @bugarela, could you have a look?

Probably because of this: #949 (reply in thread)

I'll try it with my local change and see if it fixes the problem

[bugarela]

Unrelated: I'm not getting syntax hightlightning in the added files. Seems like our global config mapping .qnt -> Bluspec is not working 😢

[bugarela]

My fix makes it so typecheck succeeds, but I still couldn't run the tests. Running quint run TendermintModels.qnt --init=n4_f1::Init --step=n4_f1::Next gives me some weird errors about constants not being found. Looking into that!

[bugarela]

Ok, I found the problem but don't know the fix won't be super easy.

The problem here is with flattening and constants. In TendermintTest, each constant is present with two names, i.e. Corr exists as both Corr and TM::Corr. Since flattening doesn't care about visibility (as any visibility issues should be flagged before hand by the name resolver), it copies all of definitions from TendermintTest to TendermintModels, under each namespace.

So it is copying n4_f1::Corr and n4_f1::TM::Corr. Overriding constants only overrides the first one (since we are not doing TendermintTest(Corr = 1, TM::Corr = 1), which of course we shouldn't have to), and therefore the constant n4_f1::TM::Corr is left without a value, which results in an error in the compiler since it expects all constants to be defined.

I'll probably need to implement some visibility sensitiveness in the flattener as well. The other option is implementing the new flattener I mentioned in the beginning of the week, which will only flatten actually used definitions - that should fix the problem because, if the name resolver passed, then no TM:: names are ever used. I'll explore these solutions.

[konnov]

The problem here is with flattening and constants. In TendermintTest, each constant is present with two names, i.e. Corr exists as both Corr and TM::Corr. Since flattening doesn't care about visibility (as any visibility issues should be flagged before hand by the name resolver), it copies all of definitions from TendermintTest to TendermintModels, under each namespace.

As far as I understand,Corr and TM::Corr are both pointing to the same constant definition with the same id. I would expect the flattener to copy the same definition once.

By the way, I had to do import as TM just because I wanted to do export TM.*, as there is no other way of exporting all definitions. Introducing export * would solve the actual issue in this example.

[bugarela]

I just noticed we don't support export ... from statements. That would also serve as a workaround here: export Tendermint.* from "./Tendermint", and you don't need TM.

[bugarela]

@konnov I hope you don't mind, I've taken this over a bit to test it with the new flattener - and it works 😄 I just had to add some type annotations for the stuff I tried to run.

One thing that is not working is unit tests. It's the same problem I just fixed for verify: since the tests are not used (as far as the flattener knows), they are not copied to the main module and then the test runner finds no tests. I'm looking for a solution.

[konnov]

That's really cool!