Cardano Updates

This remains a work-in-progress.

This remains a work-in-progress.

Nixify formal-spec enhancement step in CI

This prevents re-building and re-processing of the formal spec html
files when the sources did not change (via a nix cache hit)

Fix nix builds of jupyterlab packages

This is likely unused and whoever can build this, can also just run
jupyterlab directly via nix.

Splits CommitteeSelection::WfaLs into per-epoch persistent voters and
per-EB non-persistent voters, each backed by stake-weighted lotteries.
Vote bodies carry no explicit weight; aggregators derive weight from
external state, mirroring CIP-0164.

WfaLs now has { persistent_voters, non_persistent_voters } (defaults
480 + 120, matching sim-rs e30087cdf). Per-startup wFA committee is
allocated identically by every node from the stake registry + a
shared seed (genesis_time_unix), so each node knows its own seat
count and every other pool's without communication.

Per-EB NPV: each pool computes a deterministic eligibility signature
from (voter_id, eb_hash, eb_slot) — modeling a CIP-0164 VRF output —
and seeds a per-stake-unit Bernoulli lottery from it. The signature
is what travels on the wire; the count of wins is reconstructed
independently by every aggregator from the signature plus the
voter's ledger-resolved stake.

A pool may emit up to two bodies per EB: one PV (if it holds ≥1 seat
in the persistent committee) and one NPV (if it won ≥1 lottery trial).

Quorum threshold is now weight-based:
  Σ weight ≥ quorum_weight_fraction × expected_committee_size
where weight is committee[voter_id] for PV and count_npv_wins(...) for
NPV. expected_committee_size = Σ committee_seats + n_npv (e.g. 600
under defaults). EveryoneVotes / StakeCentile keep simpler unit-weight
semantics with no NPV path.

VoteDecision enum and decide_vote method removed; replaced by per-mode
committee construction at startup plus signature-driven NPV at vote
time. Telemetry: voted_stake → voted_weight on LeiosQuorumReached and
LeiosElectionExpired.

Cluster-verified: WfaLs at 25-node uniform stake produces 19 PV seats
per node (480/25), expected committee 600, quorum at 450 reached
reliably; RbCertifiedEb fires.

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

Pure function `allocate_persistent_seats(registry, n_pv, seed)` returning
a per-pool seat count. Stake-weighted multinomial: each of `n_pv` seats
is an independent draw from the cumulative stake distribution.

Given identical inputs (registry + seed), every node arrives at the same
committee without communication — mirroring how a real Cardano node
derives the wFA persistent committee from the ledger at epoch boundaries.

Function is currently unused; integration with the WfaLs vote path lands
in the next commit.

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

Analysis of data/simulation/pseudo-mainnet/topology-v2.yaml:
- 750 nodes, 534 (71.2%) zero-stake relays
- 216 pools, top-200 ≈ 95% cumulative
- Pool stakes log-rank slope ≈ -0.06 (saturation-flat, not heavy-tail)

Add "mainnet-shaped" strategy that captures the dominant shape:
relay_fraction = 0.71 of nodes get stake 0; remaining pools split the
total uniformly (matches Cardano's k=500 saturation cap, where pools
cluster near equal stake). Pools occupy low indices.

Skews per-pool stake aren't modeled — slope is gentle enough that
uniform-among-pools is within 5% on the prefix-sum metrics that
matter for committee selection.

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

Each node now receives the network-wide stake distribution at startup —
a Vec<StakeEntry { node_id, stake }> exposed as
production.stake_registry. Mirrors what a real node reads from the
ledger at epoch boundaries, fixed at startup for testing.

net-cluster writes the registry as [[production.stake_registry]]
array-of-tables in each per-node overlay; identical content across
nodes so each makes the same ranked-stake committee decisions.

Plumbing only — not yet consumed by voting code. Top-stake-fraction
and ranked-persistent WfaLs will use this in a later commit.

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

Adds rb-certified to the node FlashType. When a node emits an RB with
certified_eb=true, its topology-graph circle flashes with a gold border
(#ffd54f) and gold box-shadow glow, matching the EventLog highlight for
the same event.

Priority: rolledback > rb-certified > produced > received. RbCertifiedEb
fires alongside RBGenerated on the same producer; the cert flash always
wins.

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

Add three telemetry events surfacing the Leios certification path:
- LeiosQuorumReached { node, eb_slot, voted_stake, voters } — per-node,
  fired when local vote tally first crosses quorum_stake_fraction × total_stake.
  Useful for quorum-propagation latency analysis (multiple per EB).
- RbCertifiedEb { node, rb_slot, eb_slot } — per-RB, fired only on the
  producing node when the emitted RB header carries certified_eb=true.
- LeiosElectionExpired { node, eb_slot, had_quorum, voted_stake, voters } —
  fired when an election is pruned past leios_dedup_window with final tally.

record_vote now returns Option<QuorumFormed> so the caller knows when
quorum first fires. LeiosConsensus buffers these in pending_telemetry,
drained by main.rs after on_slot/on_validation_outcome.

EventLog UI:
- Default unmapped-type color was #999 (3-char hex), which became invalid
  5-char #99922 after alpha concatenation, causing inconsistent rendering
  for TipAdvanced and other unmapped events. Use #999999 + complete the
  color map for all common types.
- RbCertifiedEb gets a distinctive gold-glow highlight (bigger, bold,
  thicker border, stronger bg, box shadow) since it's the moneyshot event.

Cluster-verified: 275 LeiosQuorumReached and 11 RbCertifiedEb (= 12 RBs
minus 1 first block before any cert was eligible) over 12 EBs in a 5-min
run with EveryoneVotes + tx_rate=2.0. LeiosElectionExpired fires past
the 1013-slot pipeline+dedup window (covered by unit test).

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

Folds cluster-status.sh, tx generation count, Leios pipeline tally
(eb elections / votes / quorum), recent block production, telemetry
event-type summary, and node-0 validation lag into one report.

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

Vote bodies now carry voter_stake; record_vote sums per-EB voter stakes
and fires quorum when Σ(voter_stake) ≥ quorum_stake_fraction × total_stake
(default 0.75). Replaces the MVP "≥3 unique voters" threshold.

Plan updated with WfaLs sortition formula gap (per_node × stake_fraction
under-shoots target by ~25× at uniform stake; three fix options sketched),
missing telemetry events (LeiosCertFormed, RbCertifiedEb, LeiosElectionExpired),
and TX bitmap selection policy gap.

Cluster-verified: with EveryoneVotes, 25/25 nodes detect quorum on every EB;
WfaLs at uniform stake never reaches quorum (expected — formula gap).

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

- check-progress.sh: shows running sim processes and sweep log status
- CLAUDE.md: documents script usage, directory structure, configuration,
  engine modes, and reproducibility for the CIP experiment suite

Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>

Also fixes multiple labels