|
|
|---|
|
|
|
|---|
Leader at a round, given a committee active at that round.
We introduce a constrained function that, given a round number and a committee, returns an address in the committee. This is the chosen leader at that round.
An AleoBFT implementation may, for example, hash the round number, reduce it modulo the number of validators, and pick the validator corresponding to that index according to some ordering of the validators in the committee. But in our model we can just use a constrained function, as the details do not matter, at least for the kind of properties that we are proving in the near future.
Theorem:
(defthm addressp-of-leader-at-round (addressp (leader-at-round round commtt)))
Theorem:
(defthm leader-in-committee (in (leader-at-round round commtt) (committee-members commtt)))
Theorem:
(defthm leader-at-round-of-pos-fix (equal (leader-at-round (pos-fix round) commtt) (leader-at-round round commtt)))
Theorem:
(defthm leader-at-round-of-committee-fix (equal (leader-at-round round (committee-fix commtt)) (leader-at-round round commtt)))