Trait EventuallyCorrectLeader 

pub trait EventuallyCorrectLeader:
    RoundAdvancement
    + LeaderFairness
    + ActiveCorrectDriver
    + LeaderEligibility { }

Lemma (Eventually a correct owner leads a round that starts after GST). Under ActiveCorrectDriver, LeaderFairness and RoundAdvancement, there are infinitely many SingleLeader rounds after GST whose leader is the correct driver’s owner.

Proof. By RoundAdvancement the common round grows without bound after GST, so infinitely many single-leader rounds begin after GST — the round sequence passes through SingleLeader(0), SingleLeader(1), … by ChainOwnership::next_round, and only leaves them for Validator rounds on u32 overflow or via fallback. By LeaderFairness the driver’s owner is the leader of infinitely many of them, and by LeaderEligibility being the leader is exactly what ChainManager::can_propose requires. ∎

In Validator rounds the same argument applies with the committee’s account keys as the owner set; the correct driver is then a validator operator’s client.

Implementors