ADR-01 on Atomkraft Architecture #7
Conversation
docs/src/01adr-cli.md
Outdated
| ``` | ||
| where: | ||
|
|
||
| - `<binary>` is the name or path to a Cosmos-SDK based blockchain binary (e.g. `gaiad`); |
There was a problem hiding this comment.
do we want to have a set of supported binaries for the early prototype? (Instead of allowing users to give any path. We can leave this for a later feature)
docs/src/01adr-cli.md
Outdated
| Upon successful command execution, the testnet should be in operational step, and keep running; the testnet mnemonic is returned to the user. The proposed command format: | ||
|
|
||
| ``` | ||
| atomkraft testnet <binary> <genesis-config> <node-config> |
There was a problem hiding this comment.
| atomkraft testnet <binary> <genesis-config> <node-config> | |
| atomkraft testnet <binary> [<genesis-config>] [<node-config>] |
I suggest turning configs into optional arguments: if not specified, some healthy defaults are used. In line with the previous comment, if we are using only a set of supported binaries, we can have meaningful defaults specified for them
docs/src/01adr-cli.md
Outdated
| atomkraft explorer [<address>] | ||
| ``` | ||
|
|
||
| where `<address>` is the optional address for the blockchain explorer to connect to. If omitted, the explorer should connect to the testnet launched last. |
There was a problem hiding this comment.
It was already suggested in our zoom chat that for the early prototype we should only go with a single testnet
docs/src/01adr-cli.md
Outdated
|
|
||
| ## Generate test trace | ||
|
|
||
| A user has written a TLA+ model, and wants to generate some traces for test assertions from the model, so that they can understand the model behavior, and use some of the generated test traces later for executing on a testnet. |
There was a problem hiding this comment.
| A user has written a TLA+ model, and wants to generate some traces for test assertions from the model, so that they can understand the model behavior, and use some of the generated test traces later for executing on a testnet. | |
| A user has written a TLA+ model, and wants to generate some traces for test assertions from the model so that they can use some of the generated test traces later for executing on a testnet. |
I agree that understanding a model behavior is also useful: but we should probably differentiate between the two by having two different commands; one for generating tests from test assertions (under the hood: negating the predicate and finding a counterexamples) and the other for making sure that basic expected invariants hold for the model
docs/src/01adr-cli.md
Outdated
| Upon successful command execution, the generated test trace in the ITF format should be saved to disk. The proposed command format: | ||
|
|
||
| ``` | ||
| atomkraft trace <model> <model-config> <test-assertion> |
There was a problem hiding this comment.
| atomkraft trace <model> <model-config> <test-assertion> | |
| atomkraft trace <model> <model-config> <test-assertion> [<path-for-trace>] |
Adding an option to generate a path where to save the trace. (If not given, a default path is used)
docs/src/01adr-cli.md
Outdated
| - `<test-assertion>` is the name of the model operator describing the desired test trace. | ||
|
|
||
|
|
||
| ## Generate reactor stub |
There was a problem hiding this comment.
I strongly support this feature. For the first prototype it can probably be only basics, but it is a good way to help users wrap their heads around what are all the parts that are needed. (For later stages, we can equip those with ever more details, comments, or generated parts of the code based on standard transactions)
There was a problem hiding this comment.
Overall the idea is fine except for some details.
But this CLI is tightly coupled with MBT. What are our solutions if someone just wants to write a PBT or BDD test using Atomkraft? How one can generate stubs for them?
Pytest plugins solve that. We provide a testnet scaffolding, and a cosmos-SDK client - and a user can write their own tests in pytest. It can be MBT - for which we provide libraries, or it can be BDD or PBT for which python has other libraries.
docs/src/01adr-cli.md
Outdated
|
|
||
| A user wants to set up a Cosmos-SDK testnet, using a specific binary of their choice, so that the testnet can later be used either for exploration or testing. | ||
|
|
||
| Upon successful command execution, the testnet should be in operational step, and keep running; the testnet mnemonic is returned to the user. The proposed command format: |
There was a problem hiding this comment.
The usage is very similar to docker. You start a container and get a mnemonic globally.
Implementation-wise, this is not difficult for the cosmos-SDK chains.
But we have to decide whether we are maintaining a global context or a project-level context?
In my opinion, project-level context is good enough for a prototype.
docs/src/01adr-cli.md
Outdated
|
|
||
| A user has written a TLA+ model, and wants to generate some traces for test assertions from the model, so that they can understand the model behavior, and use some of the generated test traces later for executing on a testnet. | ||
|
|
||
| Upon successful command execution, the generated test trace in the ITF format should be saved to disk. The proposed command format: |
There was a problem hiding this comment.
I would prefer an option for modelator.shell here. This will allow users to tweak initial states, constants, test scenario predicates, etc.
docs/src/01adr-cli.md
Outdated
|
|
||
| A user has either a TLA+ model, or a test trace, and wants to write a reactor that transforms trace steps into transactions, so that they can be executed on a testnet. For that purpose, Atomkraft generates a reactor stub, which user only needs to fill with concrete actions. | ||
|
|
||
| Upon successful command execution, a Python file should be generated, which contains Python function stubs for all relevant model actions. |
There was a problem hiding this comment.
This is a nice idea. But in my opinion, this won't be useful unless we really start doing really cool.
Right now a complete test stub would look similar to the following.
import pytest
from modelator.pytest import itf, mbt, step
@step("action1")
def action1(testnet, tla_var1, tla_var2):
pass
@step("action2")
def action2(testnet, tla_var1, tla_var2):
pass
@mbt("model.tla", keypath="last_tx.name")
def test_mbt():
pass
@itf("trace.itf.json", keypath="last_tx.name")
def test_trace():
pass
It will be useful if we can somehow fill up action1 and action2 methods with appropriate arguments and code. But I feel, that is hard.
There was a problem hiding this comment.
By the way, generating code for these methods can be easy - if the model specifications have a known pattern.
If two users are using two different specification models for Authz model, how will Atomkraft be consistent with both of them?
Unless we start parsing TLA+ and generating code. And that is equivalent to generating python code from TLA+ specification.
docs/src/01adr-cli.md
Outdated
| | ----------------- | --------:| --------------:| | ||
| | Andrey Kuprianov | 1 | July 11, 2022 | | ||
|
|
||
| This ADR describes the command-line interface of Atomkraft, and how it is supposed to be used by the users as a standalone tool. It *does not* describe other possible usage scenarios, e.g. integration with testing frameworks (such as Pytest). We structure the description around the tool use cases. |
There was a problem hiding this comment.
Atomkraft CLI should only be similar to a scaffolding tool for a pytest project. (ignite-cli to cosmos-sdk)
Once the project is setup with Atomkraft, a user can also use pytest to perform tests.
Atomkraft CLI can have some out-of-box commands wrapping pytest.
docs/src/01adr-cli.md
Outdated
|
|
||
| An example workflow with customization points: | ||
|
|
||
| 1. A user comes to the new blockchain. They want to check that Atomkraft is able to interact with it, so they run `atomkraft testnet ...` |
There was a problem hiding this comment.
Do we really need to launch a testnet separately? Testnet should be auto launched when atomkraft test is run and shutdown (or stored in some log directory) when it is finished.
There was a problem hiding this comment.
If this is about using explorer on running testnet, we can store the testnet and respawn the testnet when someone wants to inspect.
andrey-kuprianov
changed the title
Closes #6.
Rendered version of ADR-01, to facilitate early feedback.