Module epochs 

Committees, epochs, and how a node comes to trust one.

A committee is identified by an Epoch, and epochs are managed on the admin chain: created by AdminOperation::CreateCommittee, retired by AdminOperation::RemoveCommittee. Every certificate is judged by the committee for the epoch its block declares, so before anything can be verified a node must know which committee that is.

This module is about where that knowledge comes from. The results here are what let the rest of the specification induct on epochs at all.

Traits

CommitteeKnowledgeIsWellFounded

Theorem (No committee certifies its own introduction). For every epoch, a node can learn that epoch’s committee only from evidence certified under a strictly earlier epoch, or — for epoch zero alone — from network configuration that is not a certificate at all. The relation “the committee for e was learned from a certificate in epoch e'” is therefore well founded, with e' < e.