[Peras 23] wFA^LS and EveryoneVotes voting committee implementations

[agustinmista]

This PR implements two concrete voting committee strategies:

1. Weighted Fait-Accompli with Local Sortition (WFALS), and
2. A simpler one where every pool with positive stake can vote (EveryoneVotes)

While Peras will use WFALS at the beginning, EveryoneVotes serves as a baseline for future benchmarks, as well as a starting point for Leios shall they end up opting for a simpler approach.

NOTES:

• WFALS depends on two separate sub-componenents:

  • WFA: the pure weighted Fait-Accompli seat split algorithm, which relies on an "extended stake distribution" ExtWFAStakeDistr (a sorted array of pools with cumulative stake). The latter can be precomputed at the beginning of an epoch and shared across multiple voting committees (e.g. shared between Leios and Peras).
  • LS: the Local Sortition check for non-persistent voters, mapping their VRF outputs into seats sampled through a Poisson distribution.

• For simplicity, EveryoneVotes reuses the same ExtWFAStakeDistr as WFALS. This way, if Leios is instantiated with EveryoneVotes, it could still use the same precomputed data as Peras.

• Both voting committee implementations defined their own abstract vote and certificate type and it's up to the clients to marshal between these types and their concrete ones (possibly using the same underlying representation and serialization routines)

[dnadales]

Could you give an example here (eg pubkey I guess?)

[dnadales]

Suggested change

	-- | Evaluate whether a voter with its give stake and relatile position in the
	-- | Evaluate whether a voter with the given stake and relative position in the

[dnadales]

evalVRF errors come from the VRF layer (invalid proof, signing-key issues), not from vote-signature verification — reporting them as InvalidVoteSignature is misleading and also leaves the purpose-built LocalSortitionError String constructor (declared at L164) as dead code.

Suggest swapping to bimap LocalSortitionError id. Propagates to both call sites (implCheckShouldVote L281 and implVerifyVote L361) and makes the existing error constructor actually reachable.

[dnadales]

NEMap.fromAscList voters silently deduplicates entries with the same SeatIndex, while sconcat voteSignatures on the line below keeps every signature. If any two elements of voters share a seat index, the resulting cert has fewer seat entries than signatures; downstream, trivialVerifyAggregateVoteSignature (Committee/Crypto.hs L181–183) rejects it with an opaque "number of keys and signatures do not match" string.

The root cause sits at the class level: VotesWithSameTarget (Committee/Class.hs L119–123) guarantees shared election and candidate but makes no claim about voter distinctness, and ensureSameTarget does not enforce any. Byzantine voters can legitimately produce same-seat-index votes with different signatures / VRF outputs, so this is not purely a caller-hygiene issue.

Three options; worth choosing one:

• (a) Strengthen VotesWithSameTarget to carry a distinctness guarantee on a per-instance voter-identity key (enforced in ensureSameTarget).
• (b) Change forgeCert's return to Either (VotingCommitteeError …) (Cert …) so duplicates can be rejected with a dedicated error constructor.
• (c) Document at the class level that forgeCert callers must pre-deduplicate — band-aid, weakest of the three.

[dnadales]

Same class-level concern as noted on WFALS.hs — NESet.fromList here silently dedupes seat indices while sconcat below retains every signature. The fix is structural, at VotesWithSameTarget in Committee/Class.hs.

[dnadales]

Comment typos collected across both files:

• WFA.hs L186: "with its give stake and relatile position" → given, relative
• WFALS.hs L162: "committe" → committee
• WFALS.hs L383: "NOTE: theres is" → there is

One-line fixes, grouped here for visibility.

[dnadales]

Import polish, bundled:

1. WFALS.hs L55 — import Data.Data (Proxy (..)): Data.Data re-exports Proxy for historical reasons, but the canonical location is Data.Proxy. EveryoneVotes.hs L36 already uses Data.Proxy in this PR, so switching here aligns the two modules.

2. EveryoneVotes.hs L25–26 — NonZero is imported twice:

import Cardano.Ledger.BaseTypes (HasZero (..), NonZero, Nonce)
import Cardano.Ledger.BaseTypes.NonZero (NonZero (..), nonZero)

Harmless but easy to trim: drop NonZero from the first line (the second brings it in with constructors already).

[dnadales]

mapAccumR (right-to-left) is load-bearing here: seat 0's cumulative stake ends up equal to the total, and the last seat's cumulative equals its own stake. Flipping to mapAccumL would silently invert the cumulative semantics, corrupting isAbovePersistentSeatThreshold.

The direction is encoded in a single character (R vs L) which is easy to skim past. A brief comment at the call site would help:

-- mapAccumR (right-to-left) so seat 0's cumulative = total stake
-- and the last seat's cumulative = its own stake.

Follow-up worth considering: PR #1977's model already uses a phantom-typed Cumulative phase (WFALS/Model.hs L88, L451 — Stake Ledger Cumulative) that mechanically distinguishes left- from right-cumulative. Mirroring this on the real Cumulative a type in Committee/Types.hs would make the direction a compile-time guarantee rather than a comment-level contract. Larger refactor, but aligns real and model implementations.

Test gap: PR #1977 tests the direction on the model, and the real impl is pinned to the model via modelConformsToRealImplementation — so direction regressions are caught transitively. A direct property on the real implementation (cumulative[0] == sum of all stakes, cumulative[lastSeat] == stake at last seat) would make the invariant explicit at the implementation side, not just indirect via conformance. Small addition to WFALS/Tests.hs.

[dnadales]

Docstring precision nit: "Cumulated stake of voters with smaller or equal stake than the current one" is accurate when there are no ties. With ties, the tiebreaker splits equal-stake pools across seat indices, and the cumulative at seat i only includes the subset of equal-stake pools that come after seat i in tiebreaker order (plus the current voter) — not all equal-stake pools.

The mathematically clean characterization is just seat-index-based:

-- | Cumulated stake of voters at the current seat index or later in sorted order.
--   Equivalently: total stake of voters with stake ≤ this voter's, with ties
--   resolved by the tiebreaker.
Cumulative LedgerStake ->

Matters only at ties, but a reader building a mental model from the current wording may underestimate how the tiebreaker affects "equal stake" accounting.

[dnadales]

This module's header is a single line ("Local sortition used by non-persistent members of the voting committee") with no reference to the paper or CIP-0164. Compare with WFALS.hs L13–29, which cites the Fait-Accompli paper with DOI and eprint link.

Since LS.hs implements non-trivial numerical machinery (Poisson thresholding, Taylor expansion), a reader trying to verify the implementation against a spec currently has to go hunting. Two lines would close the gap:

-- | Local sortition for non-persistent voters.
--
-- Implements the @LS@ component of the wFA^LS scheme from the
-- Fait-Accompli Committee Selection paper
-- (https://eprint.iacr.org/2023/1273.pdf, §<section>).
--
-- Also specified in CIP-0164:
-- https://github.com/cardano-scaling/CIPs/blob/leios/CIP-0164/README.md

(Author should supply the correct paper section — I have not cross-referenced.)