SelectF128: update frozen CDF index behavior

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` |
+| Frozen-tail output pinning | Compares promoted indexes with high-precision and Boost tail counts, and bounds maximum-digest outputs across current committee sizes, stake fractions, and supply scales | `TestSelectF128CurrentConsensusFrozenTail` and `TestSelectF128CurrentCommitteeOutputCeiling` 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` |
@@ -66,9 +67,11 @@ those endpoints enclose the true incomplete-beta CDF.
 
 ## Important test semantics
 
-- The near-one frozen-tail sliver is defined to return `money`. Exact-math
-  tolerance tests exclude that interval deliberately; dedicated tests pin its
-  behavior and liveness at current-scale values.
+- The near-one frozen-tail sliver promotes the first permanently frozen CDF
+  boundary to 1 and returns its finite index. Exact-math tolerance tests
+  exclude that interval deliberately because this is a precision policy, not
+  the exact binomial quantile; dedicated tests pin its behavior and liveness
+  at current-scale values.
 - `money` must remain below `SelectF128MaxMoney`. The maximum-domain exponent
   audit checks the worst representable `1-p` combination without performing a
   supply-sized walk.

f128.go

@@ -37,8 +37,9 @@ import (
 // It also shapes the ratio == 1.0 edge (all-0xff digest, or any digest with
 // >= 129 leading one bits): for some distributions the accumulated cdf rounds
 // up to exactly 1.0 at an early j and the walk stops there; in others it stays
-// below 1.0 for all j < money and the walk runs to money (see
-// TestSelectF128RatioExactlyOne and the SelectF128 doc comment).
+// below 1.0 and either freezes, causing the walk to return the promoted freeze
+// index, or remains live through every j < money and legitimately falls through
+// to money (see TestSelectF128RatioExactlyOne and the SelectF128 doc comment).
 type f128 struct {
 	hi, lo uint64
 	// exp is explicitly 64-bit: int is 32 bits on 386/arm, and a
@@ -525,16 +526,21 @@ func (b *binomialF128) cdf(j uint64) f128 {
 //	    double boundary = cdf(dist, j);               boundary := dist.cdf(j)
 //	    if (ratio <= boundary) {                      if ratio.cmp(boundary) <= 0 {
 //	      return j;                                     return j
-//	    }                                           }
-//	  }                                           }
-//	  return money;                               return money
-//	}                                           }
+//	    }                                             }
+//	                                                  if dist.frozen {
+//	                                                    return j
+//	                                                  }
+//	  }                                             }
+//	  return money;                                 return money
+//	}                                             }
 //
 // Boost computes cdf(dist, j) = ibetac(j+1, n-j, p) afresh each step in hardware
 // double, whereas dist.cdf(j) returns the same mathematical value as a running
 // PMF sum in software f128 (see binomialF128). The f128 path also receives the
 // digest ratio directly at f128 precision, and the success probability as its
 // exact integer numerator and denominator rather than a float64 quotient.
+// The frozen branch has no C++ counterpart: it is the documented SelectF128
+// policy for an f128 running sum that can no longer represent later CDF mass.
 //
 // Precondition: money < SelectF128MaxMoney (2^56). Below that bound no int64
 // exponent arithmetic in the walk can wrap, even at the most extreme
@@ -544,10 +550,18 @@ func (b *binomialF128) cdf(j uint64) f128 {
 // bound is undefined (Boost's Select cannot evaluate such money either).
 func binomialCDFWalkF128(expectedSize, totalMoney uint64, ratio f128, money uint64) uint64 {
 	dist := newBinomialF128(expectedSize, totalMoney, money)
-	if dist == nil { // p >= 1: cdf(j)==0 for j<money, cdf(money)==1
+	if dist == nil {
+		// newBinomialF128 returns nil iff expectedSize >= totalMoney.
+		// For nonzero totalMoney this is p >= 1: cdf(j)==0 for j<money,
+		// cdf(money)==1. The otherwise undefined totalMoney==0 case
+		// deliberately shares these deterministic degenerate semantics.
 		if ratio.isZero() {
+			// The inclusive inverse-CDF convention makes ratio 0 select the
+			// first index, 0.
 			return 0
 		}
+		// A positive ratio cannot cross any cdf(j)==0 boundary for j<money;
+		// it crosses cdf(money)==1, so the selected count is money.
 		return money
 	}
 	for j := uint64(0); j < money; j++ {
@@ -556,13 +570,20 @@ func binomialCDFWalkF128(expectedSize, totalMoney uint64, ratio f128, money uint
 			return j
 		}
 		if dist.frozen {
-			// The boundary can never increase again, so no remaining j can be
-			// selected: return the result the full walk would reach, without
-			// stepping through the up-to-money no-op iterations (for a
-			// near-maximum ratio above the CDF's plateau that walk could
-			// otherwise take hours at supply-sized money).
-			return money
+			// The boundary can never increase again. Promote the first frozen
+			// boundary to 1 and return its index, assigning the unresolved tail
+			// to one finite result instead of falling through to money after up
+			// to money no-op iterations. Using this first no-op index, rather
+			// than the preceding boundary, keeps the promoted tail above every
+			// ordinary crossing and preserves monotonicity in the digest.
+			return j
 		}
 	}
+	// Every represented boundary for j < money stayed below ratio without
+	// freezing, so the selected count is the ordinary inverse-CDF endpoint
+	// X=money. This is legitimately reachable for small distributions (for
+	// example ratio 1 at money=100, p=1/2; see
+	// TestSelectF128RatioExactlyOne) and is the same final endpoint used by the
+	// Boost reference walk.
 	return money
 }

f128_exact_test.go

@@ -74,10 +74,10 @@ func selectHighPrec(money, totalMoney, expectedSize uint64, vrfOutput Digest) ui
 }
 
 // inFrozenSliver reports whether the digest ratio is within the carved-out
-// near-1.0 region where the 128-bit walk's answer is DEFINED as money (see
-// the SelectF128 doc comment) and tolerance against exact math does not
-// apply. The bound (money+2)*2^-122 covers the plateau's ~money*2^-129 with
-// two orders of margin, including the boundary-crowding zone just above it.
+// near-1.0 region where the 128-bit walk promotes its first frozen boundary
+// to 1 (see the SelectF128 doc comment), so tolerance against exact math does
+// not apply. The bound (money+2)*2^-122 covers the plateau's ~money*2^-129
+// with two orders of margin, including the boundary-crowding zone above it.
 func inFrozenSliver(money uint64, ratio *big.Float) bool {
 	gap := new(big.Float).SetPrec(512).Sub(new(big.Float).SetPrec(512).SetInt64(1), ratio)
 	bound := new(big.Float).SetMantExp(new(big.Float).SetPrec(64).SetUint64(money+2), -122)

f128_rapid_test.go

@@ -272,9 +272,13 @@ func TestRapidF128Metamorphic(t *testing.T) {
 // the digest. This holds exactly -- the digest-to-ratio conversion is monotone
 // (round-to-nearest of a monotone quotient, and the halfway correction only
 // ever rounds up), and a larger ratio can only cross the same CDF boundaries
-// later or freeze to money. The differential tests share one structural blind
-// spot: a defect mirrored into the big.Float oracle (as the pmf(0) plateau
-// was) is invisible to them; a property test against mathematics is not.
+// later, reach the promoted freeze index, or fall through to money. Uniformly
+// generated digests cannot actually reach the frozen tail at these magnitudes
+// (with money <= 3000 the sliver is at most ~2^-117 of digest space), so
+// TestSelectF128FrozenTransitionMonotonic below brackets it deterministically.
+// The differential tests share one structural blind spot: a defect mirrored
+// into the big.Float oracle (as the pmf(0) plateau was) is invisible to them;
+// a property test against mathematics is not.
 func TestRapidSelectF128DigestMonotonic(t *testing.T) {
 	rapid.Check(t, func(t *rapid.T) {
 		money := rapid.Uint64Range(0, 3000).Draw(t, "money")
@@ -294,3 +298,41 @@ func TestRapidSelectF128DigestMonotonic(t *testing.T) {
 		}
 	})
 }
+
+// TestSelectF128FrozenTransitionMonotonic pins monotonicity across the frozen
+// transition, which the uniform generator above has effectively zero chance
+// of entering. Each pair brackets a pinned consensus distribution's plateau
+// boundary: the smaller digest must resolve as an ordinary crossing, the
+// larger must take the frozen branch, and ordering must hold between them.
+// The instrumented walk makes the branch assertion non-vacuous rather than
+// trusting the digest construction.
+func TestSelectF128FrozenTransitionMonotonic(t *testing.T) {
+	cases := []struct {
+		name                   string
+		money, total, expected uint64
+		belowBit, inBit        uint
+	}{
+		// gaps 2^-66 (below the ~2^-76 plateau) and 2^-78 (inside it)
+		{"supply ceiling 5000", 10_000_000_000_000_000, 10_000_000_000_000_000, 5000, 190, 178},
+		// gaps 2^-60 (below the ~2^-78 plateau) and 2^-80 (inside it)
+		{"online 1500", 2_000_000_000_000_000, 2_000_000_000_000_000, 1500, 196, 176},
+	}
+	for _, c := range cases {
+		dBelow := maxDigestMinusPowerOfTwo(c.belowBit)
+		dIn := maxDigestMinusPowerOfTwo(c.inBit)
+		below, _, frozeBelow := selectF128WithStepCount(c.money, c.total, c.expected, dBelow)
+		in, _, frozeIn := selectF128WithStepCount(c.money, c.total, c.expected, dIn)
+		if frozeBelow || !frozeIn {
+			t.Fatalf("%s: pair does not bracket the plateau: frozeBelow=%v frozeIn=%v", c.name, frozeBelow, frozeIn)
+		}
+		if below >= in {
+			t.Fatalf("%s: monotonicity across the frozen transition: crossing %d >= freeze index %d", c.name, below, in)
+		}
+		if got := SelectF128(c.money, c.total, c.expected, dBelow); got != below {
+			t.Fatalf("%s: SelectF128(below)=%d != instrumented walk %d", c.name, got, below)
+		}
+		if got := SelectF128(c.money, c.total, c.expected, dIn); got != in {
+			t.Fatalf("%s: SelectF128(in)=%d != instrumented walk %d", c.name, got, in)
+		}
+	}
+}