Generator of Tendermint types for unit, integration, and model-based testing

[andrey-kuprianov]

As it is documented already in many places, we need to develop a simple generator for complex tendermint-rs types.

Such a generator can be used for multiple purposes:

• generate complex types for unit tests (#381, comment on #330, #383)
• generate input for integration tests (#331, 290)
• in model-based testing (MBT), transform an abstract counterexample from a model checker (e.g. Apalache) into a concrete integration test
• may be for isolation purposes, like to isolate LIghtClient types from complete Tendermint types (#387)

The generator should have the following characteristics for the above applications:

• the generated object graphs should have correct relationships between objects (e.g., a header and a commit for it)
• have a programmer-friendly Rust API allowing to generate types with minimal input. The API should allow both to use defaults for many parameters, as well as to set them explicitely.
• for MBT, it should provide a CLI, allowing to access it, obeying the above principles from other languages / frameworks.

Here I describe the proposed solution, which is currently being implemented in tendermint-testgen

Rust API

Each tendermint type that need to be generated receives a companion type, which lists all possible options for generating this type.
Here is an example Validator struct, a companion for tendermint::validator::Info:

pub struct Validator {
  id: Option<String>,
  voting_power: Option<u64>,
  proposer_priority: Option<i64>,
}

Such validator companion can be generated then using the builder pattern as follows:

let val = Validator::new("a").voting_power(10).proposer_priority(100);

Only the parameters of the new() constructor are necessary, everything else is optional and can be omitted. In the case of a validator, it can be generated from a simple string identifier
Similarly, for a header the only required parameter is a set of validators (e.g. time then defaults to now()), and for a commit only requires a header.

Thus, the following code could then generate a header and commit companions from the two validators a and b:

let validators = vec![Validator::new("a"), Validator::new("b")];
let header = Header::new(&validators).height(100);
let commit = Commit::new(&header).round(10);

And the real Tendermint objects can be then produced from the companions as follows:

let block_header = header.produce().unwrap();
let block_commit = commit.produce().unwrap();

Command-line interface

For MBT we need to be able to generate Tendermint objects from outside of Rust. We assume that the following prerequisites are met:

• The user has a favorite model-checker (e.g. Apalache), which is able to produce counterexamples in JSON (Apalache can of course do it).
• The user has a way to execute an integration test, written in JSON, and including all necessary details, against his implementation (which e.g. LightClient can do).
• There is a tool that is capable to translate between related but different JSON formats (e.g., our JSON Artifact Translator).

The workflow then, from a birds eye view is such:

1. A user creates a TLA+ spec, that is an abstraction of the implementation he wants to test
2. The user describes an invariant, which, when violated, would produce an interesting behavior as a counterexample
3. The user runs, manually, or as part of automated test generation, his favorite model checker, and gets a counterexample.
4. As the counterexample is abstract, i.e. some important implementation-level details are not present. Thus, it needs to be translated from the abstract to the concrete form. Such a translation can be described with a simple declarative spec, like this one

The only part, which is missing in the above transformation step, is the translation of the abstract counterexample types into the concrete implementation types.
This is also under implementation in tendermint-testgen, a CLI utility which is based on the same companion types as described above.

The CLI parameters can be supplied in two ways:

• via STDIN: in that case they are expected to be a valid JSON object,
  with each parameter being a field of this object. Accepting input from STDIN allows to integrate the tool into transformation chains with other tools
• via command line arguments to the specific command. This allows either to use the utility as a standalone tool, or to customize the output produced from STDIN otherwise.

If a parameter is supplied both via STDIN and CLI, the latter is given preference.

In case a particular object can be produced from a single parameter
(like validator), there is a shortcut that allows to provide this parameter
directly via STDIN, without wrapping it into JSON object.
E.g., in the validator case, the following are equivalent:

tendermint-testgen validator --id a --voting-power 3
echo -n '{"id": "a", "voting_power": 3}' | tendermint-testgen --stdin validator
echo -n a | tendermint-testgen --stdin validator --voting-power 3
echo -n '{"id": "a"}' | tendermint-testgen --stdin validator --voting-power 3
echo -n '{"id": "a", "voting_power": 100}' | tendermint-testgen --stdin validator --voting-power 3

The result is a JSON object printed out on STDOUT; the result of the any above commands is:

{
  "address": "730D3D6B2E9F4F0F23879458F2D02E0004F0F241",
  "pub_key": {
    "type": "tendermint/PubKeyEd25519",
    "value": "YnT69eNDaRaNU7teDTcyBedSD0B/Ziqx+sejm0wQba0="
  },
  "voting_power": "3",
  "proposer_priority": null
}    

[andrey-kuprianov]

merged by 877c586