|
|
|---|
|
|
|
|---|
Under-specified indices for choosing round leaders.
Every even round has a leader validator. We model that via an underspecified function that returns a natural number at each round. We only use the function on non-zero even rounds, since round 0 and odd rounds have no leaders. The natural number is reduced modulo the number of validators, and the resulting number is used as an index in the totally ordered set of validator addresses.
We only constrain this under-specified function to return a natural number. We also guard it to require a natural number as input (which we could tighten it to non-zero even natural number).
This approach to modeling leader choice amount to this under-specified being universally quantified: everything proved about the model holds for every concrete choice of the function. This is adequate for proving properties over single runs of the system (for every possible run, but just one round at a time). For properties involving multiple runs of the system, using a single under-constrained function would constrain the multiple runs to always choose the same leader at every round, which may not be adequate. But in this case, we can extend this under-constrained function to take an additional ``seed'' input, which makes it possible to return different natural numbers for the same round but for different seeds. Then the seed can be added to the internal state of the system; the seed never needs to change with events, but different initial states may have different seeds, and thus the multiple runs involved in a property of interest may be given different seeds, thus allowing them to choose different leaders at the same round.
In some literature, the distinction between properties over single runs vs. properties over multiple runs is describes as `properties' for the former and `hyperproperties' for the latter. We generally prefer to use the term `property' in the more general mathematical sense, and talk about (properties of) single or multiple runs when the distinction is relevant.
Theorem:
(defthm natp-of-leader-index (natp (leader-index round)) :rule-classes (:rewrite :type-prescription))