Validator context

A validator context specifies the set of protocol participants and their stakes. It consists of:

• a finite type \mathsf{Validator} with decidable equality,

• a total stake function \mathsf{stake} : \mathsf{Validator} \to \mathbb{N}.

The finiteness of \mathsf{Validator} (formalised as a Fintype instance) is essential: it provides Finset.univ : Finset Validator (the set of all validators), which is used in link_supporters to collect the supporters of a checkpoint link.

Most definitions in Core are parameterised explicitly by Validator, [DecidableEq Validator], [Fintype Validator], and stake rather than by a bundled context, so ValidatorContext serves primarily as documentation of the required assumptions.

Coq source: Validator.v. Coq declares Validator : finType and stake : {fmap Validator -> nat} as global parameters with a totality axiom; Lean replaces the partial finite map with a total function and bundles the assumptions into a structure.

Data

• Validator — the type of protocol participants,

• instDecidableEq — a DecidableEq instance on Validator,

• instFintype — a Fintype instance on Validator (finiteness),

• stake — a total function \mathsf{stake} : \mathsf{Validator} \to \mathbb{N}.

The first three fields jointly provide a finite type with decidable equality; the fourth assigns a natural-number weight to each participant.

Intended semantics

The Gasper paper idealizes stake as a positive real of average 1 (total N). Modelling it as \mathbb{N}, as the Coq development does, keeps all weight arithmetic exact; the only divergence from that idealization is that zero-stake validators are permitted, and these contribute nothing to any quorum or threshold weight.

Non-assumptions

This structure does not assume:

• positivity of \mathsf{stake} — zero-stake validators are allowed;

• injectivity of \mathsf{stake} — distinct validators may share a weight;

• non-emptiness of Validator — the empty population is a legal context;

• any normalization of the total weight (no fixed total N, no average 1).

Provenance

This is a first-class value, not a global axiom. Most Core definitions take Validator, [DecidableEq Validator], [Fintype Validator], and stake as explicit parameters rather than this bundle, so the structure serves mainly to document the required assumptions in one place.