diff --git a/TESTING.md b/TESTING.md index 89351a3..436e56c 100644 --- a/TESTING.md +++ b/TESTING.md @@ -35,6 +35,7 @@ go test -run xxx -fuzz FuzzSelectF128 -fuzztime 10m | Exhaustive boundary grids | Enumerates small parameter domains and checks digest integers below, at, and above every exact CDF boundary, with anti-vacuity counters | `cdf_exhaustive_test.go`, `oracle_hardening_test.go` | | Higher-precision convergence | Requires the 512- and 1024-bit CDF walks to converge and compares them with exact small-domain results and certified large-money results | `selectAtPrecision` in `f128_exact_test.go`, tests in `oracle_hardening_test.go` | | Internal trajectory and liveness | Checks PMF/CDF error envelopes and monotonicity, audits the maximum-domain exponent path, proves bounded freeze permanence, and pins CDF-evaluation limits | `f128_trajectory_test.go` | +| Weight-gap pinning | Verifies the reachable-result gap behind `SelectF128MaxWeightFactor`: CDF freeze indexes stay below the factor for every current consensus committee size across stake scales, so consumers can reject the frozen-tail plateau exactly | `TestSelectF128WeightGap` in `f128_test.go` | | Metamorphic properties | Checks digest monotonicity, power-of-two and arbitrary common-factor probability scaling, primitive identities, and arithmetic order properties without a numeric oracle | `f128_rapid_test.go` | | Distribution sanity | Checks aggregate selection weight against the expected binomial mean without reusing the CDF formula | `TestSelectF128Distribution` in `f128_exact_test.go` | | Arb-certified quantiles | Uses Arb's regularized incomplete beta implementation to certify large-money quantile inequalities with rigorous dyadic endpoints | `tools/generate_arb_oracle.py`, `testdata/f128_arb_certificates.json`, `f128_arb_certificate_test.go` | diff --git a/f128_test.go b/f128_test.go index 2b00ee2..27562b3 100644 --- a/f128_test.go +++ b/f128_test.go @@ -609,3 +609,77 @@ func TestSelectF128FrozenTailReportedCase(t *testing.T) { t.Fatalf("SelectF128=%d, want money=%d for ratio exactly 1.0", got, onlineStake) } } + +// TestSelectF128WeightGap pins the structural gap that makes +// SelectF128MaxWeightFactor a sound rejection threshold. A walk result j is +// reachable only if the f128 CDF strictly increases at j, and the CDF +// freezes permanently once adding a (strictly shrinking) PMF term no longer +// moves the accumulated sum, so the reachable results for a distribution are +// exactly: indexes up to the freeze index, and money itself (the defined +// frozen-tail plateau result). Nothing in between can occur. +// +// The freeze index grows with the account's expected selection count +// lambda = money*expectedSize/totalMoney <= expectedSize, so a sole account +// holding all online stake (money == totalMoney, lambda == expectedSize) is +// the worst case per committee size. This test steps the CDF recurrence +// directly for every committee size in current go-algorand consensus use +// (v41 inherits NumProposers=20, LateCommitteeSize=500, CertCommitteeSize=1500, +// RedoCommitteeSize=2400, SoftCommitteeSize=2990, NextCommitteeSize=5000, +// DownCommitteeSize=6000) at three stake scales -- roughly current mainnet +// online stake, the genesis supply ceiling, and the domain bound -- and +// asserts the freeze index stays below SelectF128MaxWeightFactor*expectedSize +// while the plateau result money sits far above it. +// +// The factor is deliberately the smallest sound integer: the freeze quantile +// is ~5.2x expectedSize at NumProposers=20 (freeze index 104 against a bound +// of 120) and shrinks toward ~1.2x as committees grow. The thin-looking +// margin at the smallest committee is a deterministic property of the +// arithmetic, recomputed here on every run, not a measurement with error +// bars. Two changes would invalidate the factor and must fail here first: a +// committee smaller than 20 (ruled out by policy -- shrinking committees +// weakens the chain's security assumptions -- and asserted by go-algorand's +// TestSortitionWeightBound), and any precision change to the walk (guard +// bits raise the freeze indexes toward the exact-arithmetic ceiling, +// ~7.5x expectedSize at expectedSize=20, above the factor). +func TestSelectF128WeightGap(t *testing.T) { + committees := []uint64{20, 500, 1500, 2400, 2990, 5000, 6000} + totals := []uint64{ + 2_000_000_000_000_000, // approximately current mainnet online stake + 10_000_000_000_000_000, // mainnet genesis supply ceiling + SelectF128MaxMoney - 1, // domain bound for the money argument + } + + for _, cs := range committees { + for _, total := range totals { + money := total // sole online account: lambda == cs, the per-committee worst case + bound := SelectF128MaxWeightFactor * cs + + if money <= bound { + t.Fatalf("cs=%d total=%d: money %d not above bound %d; plateau would pass the bound", + cs, total, money, bound) + } + + b := newBinomialF128(cs, total, money) + if b == nil { + t.Fatalf("cs=%d total=%d: degenerate distribution", cs, total) + } + // Step far past the bound before giving up. A CDF that saturates + // at exactly 1.0 also freezes (the next add is a no-op with a + // shrinking PMF), so every distribution in domain must freeze + // within a small multiple of the tail quantile. + limit := 10 * bound + b.cdf(limit) + if !b.frozen { + t.Fatalf("cs=%d total=%d: CDF did not freeze within %d steps; gap analysis does not apply", + cs, total, limit) + } + // b.at is the step whose add was first observed to be a no-op, so + // the largest reachable non-plateau result is strictly below it. + if b.at > bound { + t.Fatalf("cs=%d total=%d: freeze index %d above bound %d = %d*%d; reachable weight would be rejected", + cs, total, b.at, bound, SelectF128MaxWeightFactor, cs) + } + t.Logf("cs=%d total=%d: freeze index %d, bound %d, plateau result %d", cs, total, b.at, bound, money) + } + } +} diff --git a/sortition.go b/sortition.go index 77dd5cd..379c9ae 100644 --- a/sortition.go +++ b/sortition.go @@ -76,6 +76,52 @@ func Select(money uint64, totalMoney uint64, expectedSize float64, vrfOutput Dig // of silently misrounding consensus. const SelectF128MaxMoney = uint64(1) << 56 +// SelectF128MaxWeightFactor bounds the statistically plausible SelectF128 +// result. The walk cannot return a result strictly between its CDF freeze +// index and money: each result j needs the f128 CDF to strictly increase at +// j, and the CDF freezes once adding the next PMF term no longer moves the +// accumulated sum. The sum sits just below 1, in the +// binade whose ULP spacing is 2^-128 (128-bit mantissa), so terms under +// ~2^-129 -- half that spacing -- are no-ops. The largest reachable +// pre-freeze index is therefore about the binomial quantile where the PMF +// term falls to ~2^-129. For the committee sizes in current +// go-algorand consensus use that quantile is at most ~5.2*expectedSize +// (at expectedSize=20, today's NumProposers; the multiple shrinks toward +// ~1.2 as committees grow -- a future committee smaller than 20 would need +// this factor re-derived). Inside the sliver the result is DEFINED as +// money, the account's entire stake, and no result strictly between the +// freeze index and money is reachable at all, so any threshold in the gap +// separates the two regimes exactly. Note that money itself is an ordinary +// result for a small stake -- a 5-microalgo account can have all 5 +// microalgos selected -- and such results pass the bound, since money <= +// factor*expectedSize makes rejection impossible for that account. Only a +// stake above the bound can be rejected, and for such a stake the only +// reachable result above the bound is the plateau's money. +// TestSelectF128WeightGap pins the freeze indexes below this factor across +// current committee sizes and stake scales. +// +// Consumers that treat the result as trusted voting power or as a loop +// bound should reject results above SelectF128MaxWeightFactor*expectedSize. +// The factor must exceed ~5.2 to admit every reachable non-plateau result, +// and in go-algorand it must stay below MinBalance/DownCommitteeSize = +// 100_000/6_000 ~= 16.7 so that a plateau result -- at least the 100,000 +// microalgo minimum stake -- exceeds the bound for every committee size. +// Every factor in that window rejects the identical, otherwise-unreachable +// set, so 6 -- the smallest sound integer -- is chosen to keep the most +// headroom under MinBalance as committees grow. Taking the tight end leans +// on two commitments, each enforced by a test. First, committee sizes never +// shrink below today's smallest of 20: reducing them would weaken the +// chain's security assumptions independent of sortition, and go-algorand's +// TestSortitionWeightBound asserts the floor. Second, the walk's precision +// stays as it is: guard bits would raise the freeze quantile toward the +// exact-arithmetic ceiling of ~7.5*expectedSize at expectedSize=20, so any +// plateau-narrowing change must re-derive this factor, and +// TestSelectF128WeightGap fails the moment the indexes cross the bound. +// Rejecting a credential changes what validates and is therefore a +// consensus rule: it must ride the same protocol upgrade gate as the switch +// to SelectF128 itself. +const SelectF128MaxWeightFactor = 6 + // SelectF128 is a deterministic sortition function. It evaluates both the VRF // ratio and binomial CDF at f128 precision using software integer arithmetic, so // its result is bit-reproducible across platforms. money must be below @@ -143,6 +189,10 @@ const SelectF128MaxMoney = uint64(1) << 56 // rather than the exact binomial-tail crossing. Computing pmf(0) with guard // bits could narrow the interval, at the cost of additional consensus-critical // arithmetic and audit surface. +// +// Because the frozen CDF makes every count strictly between the freeze index +// and money unreachable, a consumer can reject the sliver exactly rather than +// probabilistically: see SelectF128MaxWeightFactor. func SelectF128(money uint64, totalMoney uint64, expectedSize uint64, vrfOutput Digest) uint64 { ratio := f128FromDigestRatio(vrfOutput) return binomialCDFWalkF128(expectedSize, totalMoney, ratio, money)