tendermint-rs
tendermint-rs copied to clipboard
Extend Testgen to generate Validator sets
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 totendermint-testgen
binary. - in the Jsonatr transform above, invoke
tendermint_valset
for the array of identifiers, instead of mapping thetendermint_validator
.
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.
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.