tendermint-rs icon indicating copy to clipboard operation
tendermint-rs copied to clipboard

Extend Testgen to generate Validator sets

Open andrey-kuprianov opened this issue 4 years ago • 2 comments

After extending Tendermint Validator Set with the total_voting_power field, the model-based tests stopped to work.

The reason for that behavior is that validator sets are not first class citizens in the Testgen. Instead, when generating validator sets via Jsonatr transform, we map Testgen validator generation over the array of abstract validator identifiers, as produced by Apalache. This was ok, until total_voting_power, that requires treating Validator Set as a datastructure on its own.

The solution is as follows:

  • add ValidatorSet to Testgen, and generate it in the same way as all other datastructures.
  • add valset command to tendermint-testgen binary.
  • in the Jsonatr transform above, invoke tendermint_valset for the array of identifiers, instead of mapping the tendermint_validator.

andrey-kuprianov avatar Nov 09 '20 20:11 andrey-kuprianov

Thanks @andrey-kuprianov , we definitely need to make this improvement to Testgen. On a second thought, does it make sense to use validator::Set::new(validators, voting_power) instead of the old valset constructor since we do not currently make use of total_voting_power in Testgen apart from construction. I think it'll be easier to quickly unblock things this way.

Shivani912 avatar Nov 10 '20 08:11 Shivani912

With #730, we have introduced the ValidatorSet to testgen and can be generated like other data structures. But, we still need to integrate it with other data structures (header, commit, etc.) - see this comment. Doing that will require both steps 2 & 3 to be implemented.

Shivani912 avatar Dec 11 '20 10:12 Shivani912