Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions TESTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -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` |
Expand Down
74 changes: 74 additions & 0 deletions f128_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
}
}
50 changes: 50 additions & 0 deletions sortition.go
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down
Loading