Skip to content

Add SelectF128 sortition implementation#8

Merged
cce merged 37 commits into
mainfrom
sortition-f128
Jul 22, 2026
Merged

Add SelectF128 sortition implementation#8
cce merged 37 commits into
mainfrom
sortition-f128

Conversation

@cce

@cce cce commented Jul 21, 2026

Copy link
Copy Markdown
Collaborator

This adds SelectF128, a pure Go implementation of Select that uses a custom 128-bit float implementation (in f128.go) for performant, deterministic sortition with no platform dependencies.

cce and others added 8 commits June 19, 2026 15:20
1-p is exact for any float64 p, so compute it with a native f128
subtraction instead of big.Float, dropping one f128FromBigFloat
conversion (~6 fewer allocs, ~17% off newBinomialF128). sub is done
exactly in a 192-bit field so it is correct under cancellation, and is
fuzz-checked bit-identical to the big.Float oracle.
Compute p/(1-p) with a native round-to-nearest-even f128 divide (128/128
via Knuth long division, used once per setup) instead of big.Float. With
the earlier native 1-p, newBinomialF128 is now heap-free apart from the
returned struct: 658ns/19allocs -> 195ns/1alloc, and the SelectF128 common
path drops 984ns/25allocs -> 535ns/7allocs (the remaining allocs are the
VRF->ratio big.Float work shared with Select).

div is fuzz-checked bit-identical to the big.Float oracle via SelectF128,
and TestDivVsBig cross-checks it directly against a 128-bit big.Float
divide on 5M broad random operands. Removes the now-dead f128FromBigFloat,
f128bigMask, and toBigFloat helpers and the math/big import.
sub was previously exercised only through the (1, p) operand shape in newBinomialF128; fuzz it across the full operand space, with seeds for the sticky/borrow path (exponent diff >= 65) and near-equal cancellation. Fuzz div alongside TestDivVsBig for ongoing corpus-driven coverage.

Also correct the newBinomialF128 comment: 1-p is correctly rounded rather than exact for p below ~2^-76 (it still matches the 128-bit big.Float oracle bit-for-bit, which is the property the fuzz checks). BenchmarkSelectF128 mirrors BenchmarkSortition for direct comparison with the cgo/Boost path.
@cce

cce commented Jul 21, 2026

Copy link
Copy Markdown
Collaborator Author

Benchmark results

Measured at head a6645ef with the in-tree benchmarks, which run the cgo/Boost Select and the pure-Go SelectF128 with identical parameters (money=1e6, total=1e12, expectedSize=2500, random VRF digests):

go test -run xxx -bench 'BenchmarkSortition|BenchmarkSelectF128' -benchmem -count=10
goos: darwin
goarch: arm64
pkg: github.com/algorand/sortition
cpu: Apple M2 Max
              │    sec/op     │
SelectF128-12     158.9n ± 1%
Sortition-12      356.5n ± 0%

              │     B/op      │
SelectF128-12      96.00 ± 0%
Sortition-12       480.0 ± 0%

              │   allocs/op   │
SelectF128-12      1.000 ± 0%
Sortition-12       6.000 ± 0%

(Sortition = the existing cgo/Boost Select; go1.26.2, -count=10, summarized with benchstat.)

SelectF128 is ~2.2x faster than the cgo path, with 1 heap allocation per call vs 6. The remaining allocation is the *binomialF128 evaluator struct; the walk itself -- digest-to-ratio conversion, all f128 arithmetic -- is heap-free.

The gains compounded across the PR's commits: the original f128 walk still spent ~984ns/25 allocs in big.Float setup, the native sub/div cut that to ~535ns/7 allocs, and the direct 256-bit digest-to-f128 ratio conversion removed the remaining big.Float/big.Int VRF work, landing at ~159ns/1 alloc.

Comment thread sortition.go Outdated
The committee size is a uint64 in the protocol (CommitteeSize(proto)); the float64 parameter only mirrored the C++ double signature and forced casts at every caller. Passing the exact integers lets each PMF-recurrence constant be a SINGLE round-to-nearest-even f128 divide of exact values -- q = (total-expected)/total and pq = expected/(total-expected) -- instead of stacking roundings through an intermediate float64 p (float64(totalMoney) is itself inexact above 2^53). Invalid probabilities (NaN/Inf/negative/fractional) become unrepresentable and p >= 1 is an exact integer comparison, so the differential fuzz no longer needs any input filtering.

f128FromFloat64 loses its only caller and is removed; sub and its norm192s helper likewise lose theirs (1-p is now a direct divide of exact integers, one rounding instead of two) and are removed along with their fuzz checks. The oracle mirrors the integer-quotient constants. Boost agreement is unchanged (200000/200000); the fuzz explored the new signature for 8.1M execs clean. Setup now does two divs instead of convert+sub+div: ~170ns/op (was ~159), still 1 alloc.
@cce

cce commented Jul 21, 2026

Copy link
Copy Markdown
Collaborator Author

Updated benchmark results (integer expectedSize)

da28510 changes SelectF128 to take the committee size as uint64 -- the type it actually is in the protocol (CommitteeSize(proto); go-algorand's credential.go currently casts it to float64 just to call Select). The distribution constants are then each a single round-to-nearest-even f128 divide of exact integers:

1-p     = (totalMoney-expectedSize) / totalMoney
p/(1-p) = expectedSize / (totalMoney-expectedSize)

instead of stacking roundings through an intermediate float64 p (note float64(totalMoney) is itself inexact above 2^53 ~= 9.0e15 uA, and max supply is 1e16). It also makes invalid probabilities unrepresentable -- no NaN/Inf/negative/fractional sizes -- and p >= 1 becomes the exact integer comparison expectedSize >= totalMoney, so the differential fuzz now runs with no input filtering at all (8.1M execs clean on the new signature, Boost agreement still 200000/200000).

Same setup as the previous numbers (Apple M2 Max, go1.26.2, -count=10, benchstat):

              │    sec/op     │
SelectF128-12     170.4n ± 1%
Sortition-12      354.6n ± 1%

              │     B/op      │
SelectF128-12      96.00 ± 0%
Sortition-12       480.0 ± 0%

              │   allocs/op   │
SelectF128-12      1.000 ± 0%
Sortition-12       6.000 ± 0%

Still ~2.1x faster than the cgo/Boost path with 1 alloc vs 6. Setup is ~11ns slower than the previous measurement (170.4n vs 158.9n): forming both constants as full 128/128 divides costs slightly more than the old convert + subtract + divide, in exchange for one-rounding accuracy. f128FromFloat64, sub, and its norm192s helper lost their remaining callers in this change and are removed (~130 lines).

cce added 3 commits July 21, 2026 08:07
At ratio exactly 1.0 (only the all-0xff digest IS exactly 1.0; the rest of the top 2^-129 digest interval rounds up to it), the accumulated f128 CDF reaches exactly 1.0 only for some distributions, decided at ulp granularity: money=1954/exp=1500 stops at j=3 with total=1_999_999_999_999_964 but falls through with total=2_000_000_000_000_000, 36 more. Other distributions never get within half an ulp of 1.0 (p=1/2 with money=100 leaves cdf(99) = 1 - 2^-100, 2^28 ulps short) and the walk runs to money -- which, with the rounded threshold fixed at 1.0, is also the exact-CDF count, since the exact CDF is < 1 for every j < money. The previous text presented the early stop as the behavior and money as hypothetical; this had it backwards.

Reframe the f128 round-to-nearest rationale accordingly: RNE is required because every result must be the correctly-rounded 128-bit value to stay bit-identical to the 128-bit big.Float oracle; the ratio==1.0 edge is a consequence, not the requirement. Boost's double CDF -- evaluated independently per j via ibetac rather than accumulated -- can also saturate to 1.0 on its far coarser grid, potentially at a different (typically earlier) j, so old-vs-new divergence at this edge can be as large as money vs. a few.

TestSelectF128RatioExactlyOne now pins both branches and both boundaries: the hair-trigger total pair (j=3 vs money), the provably-stuck money=100/p=1/2 case, and the exact tie money=129/p=1/2 where true cdf(128) = 1 - 2^-129 sits precisely on the rounding midpoint and ties-to-even rounds it up to 1.0 (stops at j=128). The rounds-to-1.0 digest is constructed with exactly 129 leading one bits, the minimal such digest.
The compressed 'as large as money vs. a few' read as a typo (money is the parameter, not a quantity of currency). Spell it out: at a near-maximum digest one implementation may stop within a few steps of the binomial tail while the other returns the full trial count money.

@nullun nullun left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've mostly looked through the tests and fuzzers to try and make sure what's being tested make sense, but here's a few things that were brought up by Claude. None of them are issues with how we use it in go-algorand, but they're more aligned with a total supply larger than what we have.


divU rounding - divU mis-rounds by one ulp whenever the divisor exceeds half the mantissa's top word (u > ~2^62), which the sortition walk could only reach if its step index j - bounded by money, a microalgo stake capped by Algorand's 10^16 µA (~2^53) total supply - were ~460× the entire supply; so while no Algorand input is affected, I'd suggest handling the two shallow-quotient cases explicitly (deriving round/sticky from the actual division remainder) so the round-to-nearest-even contract is unconditionally true, and locking it in with a large-divisor fuzz seed and a differential test against big.Float.

int64 exponent - the f128 exponent is a platform-sized int, which is 32 bits on architectures go-algorand has historically shipped on (arm32/386) and would silently wrap there for extreme stake/probability combinations, undermining the "bit-identical on every platform" claim that motivates replacing the cgo/Boost Select in the first place - real consensus parameters (stakes ≤ 2^54 µA, p = committeeSize/totalOnlineStake ≈ 10^-13, committees of 20–6000) keep every exponent in the low thousands, but I'd still recommend making it explicitly int64 so correctness doesn't depend on GOARCH.

Domain guard - the walk's money < 2^57 validity bound is currently prose describing undefined behavior, protected only by economic invariants living in go-algorand (the 10B Algo supply cap and credential.go's panic when a voter's stake exceeds total online money); consider having SelectF128 enforce the edge itself with an explicit panic - it keeps ~8 bits of headroom above any reachable stake, and means a future supply change (say, an inflationary model) or reuse with a larger-supply token would fail loudly instead of silently misrounding consensus.

cce added 2 commits July 21, 2026 10:59
pmf(0) = (1-p)^money amplifies the 2^-129 rounding of 1-p by up to the trial count, and pmf(0) scales every PMF term, so the accumulated CDF settles at a plateau that can sit ~money*2^-129 below 1 (~2^-78 at supply-sized money). A digest ratio between the plateau and 1.0 (e.g. 2^256-1-2^176, ratio ~1-2^-80, with money == total == 2e15) sits above every boundary without rounding to 1.0, and the walk previously ground through all 2e15 no-op iterations -- hours of CPU on the consensus path -- before returning money.

Detect the freeze instead: once an add cannot move cum while pmf strictly shrank, no later term can move it either (the rounded step factor is < 1 and only decreases; round-to-nearest is monotone), so the walk returns money immediately -- the identical result the plain walk reaches, in O(binomial tail) time. FuzzSelectF128 continuously validates the short-circuit against the oracle's full walk, and TestSelectF128FrozenTailReturnsMoney pins the supply-sized case for both the 2^-80 digest and ratio exactly 1.0.

The count in the stuck sliver stays DEFINED as money: reaching it requires a VRF hash within ~2^-78 of the maximum, which cannot be ground for, so the 192-bit-pmf(0) variant that would return the exact binomial-tail crossing there (parked on sortition-f128-pmf192) is not worth its added audit surface under current consensus parameters. Documented in the SelectF128 tail-edge note.
Replace the unreachable-tail wording with the accepted probabilistic bound and its no-grinding assumption. Pin current go-algorand committee behavior at the base minimum, payout eligibility landmarks, mainnet supply ceiling, and original report while showing that Boost terminates at finite double-CDF boundaries.
@cce

cce commented Jul 21, 2026

Copy link
Copy Markdown
Collaborator Author

A reviewer noticed that for supply-scale stake, the accumulated f128 CDF can permanently plateau below valid digest ratios: raising 1-p to the money-th power amplifies its single 2^-129 rounding by the trial count, and pmf(0) scales every PMF term, so the CDF settles as much as money × 2^-129 below 1. A digest ratio between that plateau and 1.0—e.g. 2^256-1-2^176, ratio ≈ 1-2^-80, with money = totalMoney = 2e15 and committee size 1500—then sits above every boundary without rounding to 1.0, and the walk ground through all 2×10^15 no-op iterations (hours of CPU) before returning money, where the exact binomial-tail crossing is 1913. The differential fuzz could not have caught this: the big.Float oracle computes the identical plateau.

There is a prototype higher-precision fix in 2375ec3 on the sortition-f128-pmf192 branch, which computes pmf(0) with a custom 192-bit quotient/multiply/power implementation. It returns the exact 1913 crossing for the reported input, but adds substantial consensus-critical arithmetic and audit surface, plus roughly 100 ns to every selection. Given that the interval is unreachable under go-algorand's threat model—registered keys and an unpredictable seed prevent targeting it, and go-algorand is the only consumer—the tradeoff does not seem justified.

The committed resolution is:

  • 6b0359c: detect when the accumulated CDF can no longer change and return money immediately. This changes the pathological walk from up to money iterations to approximately the binomial-tail length. The early return is provably the result the unshortened walk would reach, and FuzzSelectF128 continuously validates the short-circuited walk against the oracle's full walk.
  • e59c909: document this as an explicitly accepted statistical edge and add regression coverage using current go-algorand parameters and balance bounds.

The affected interval for an account with stake m is approximately m × 2^-129. Summing the first-order bound over all online accounts gives approximately totalMoney × 2^-129 per committee selection, independent of stake splitting—around 2^-78 for 2e15 online microalgos and 2^-76 at the 1e16 mainnet supply ceiling.

The new tests demonstrate consensus-permitted cases:

Case Stake (microalgos) Committee size Digest gap from 1 SelectF128 Boost Select
Proposer 1,999,999,999,999,999 20 2^-81 money 67
Base minimum 100,000 5,000 2^-115 money 2
Payout minimum landmark 30,000,000,000 5,000 2^-97 money 6
Payout maximum landmark 70,000,000,000,000 5,000 2^-86 money 94
Mainnet supply ceiling 10,000,000,000,000,000 5,000 2^-78 money 5,598
Reported certification case 2,000,000,000,000,000 1,500 2^-80 money 1,832

The 30,000–70,000,000 Algo values are payout-eligibility landmarks, not voting caps; accounts outside that interval can still participate. Total online stake is the mainnet supply for the four committee-size-5,000 rows and equals the account stake for the Proposer and Reported rows.

Boost does not have the liveness problem because it evaluates each CDF independently with ibetac; these near-maximum ratios round to binary64 1.0, and its CDF reaches 1.0 after a finite tail walk. It has its own tail-accuracy artifact—the reported exact crossing is 1913, while Boost returns 1832—but it does not iterate to money. The pinned Boost values reproduce exactly on darwin/arm64 (Apple libm) and linux/amd64 (glibc); a mismatch on some other platform would itself demonstrate the deployed path's libm nondeterminism, while the SelectF128 assertions are platform-invariant.

This intentionally treats the f128 stuck band as a defined negligible-probability edge rather than adding the larger 192-bit implementation.

cce added 8 commits July 21, 2026 11:51
The exponent was a platform-sized int, which is 32 bits on 386/arm. No reachable input wraps it -- consensus parameters keep every exponent in the low thousands, and even the unfiltered fuzz domain stays near 2*10^5 -- but that made the cross-GOARCH bit-identity guarantee depend on magnitudes staying small rather than on the type. Also restructure add's alignment check to compare exponents in int64 BEFORE converting to a uint shift count: uint is likewise 32-bit on those platforms, and the naive type swap would leave a truncation that could alias a huge exponent difference to a small shift.
divU folded the division remainder's sticky marker into the last quotient digit. For deep quotients that digit sits safely below the round bit, but once the divisor exceeds ~2^62 the quotient has at most 129 significant bits and the marker lands at the round bit (corrupting ties) or inside the mantissa (off by an ulp about half the time). The sortition walk cannot reach the broken region -- its divisor is the step index, bounded by money, ~2^53 at the supply -- but the round-to-nearest-even contract claimed by the doc was false there. Compute a 256-bit quotient instead: two full fraction digits keep the round bit inside computed digits for every divisor, and the remainder only ever contributes to sticky. norm192 and shl192 lose their last caller and are removed.

This survived ~30M FuzzF128Ops execs because go's mutator explores integers locally around corpus values and the seeds had u=7 and u=1: planted next to a u~2^63 seed, the fuzzer failed on the seed itself. Add two large-divisor seeds and TestDivUVsBig, a 2M-case differential test against big.Float with log-spread divisor magnitudes.
rapid generates fresh values across the full input space every run, with explicit magnitude-band guidance layered on its boundary bias, complementing go fuzzing's corpus mutation, which dwells near seed values: the divU shallow-quotient misrounding survived ~30M fuzz execs but rapid found and minimized it within its first hundred generated cases (a={2^63+1,0}, u=2^64-1). TestRapidF128Ops mirrors FuzzF128Ops over the primitives; TestRapidSelectF128VsOracle mirrors FuzzSelectF128 end to end, drawing digests both uniformly and from the near-maximum regime. Both run 100 cases per ordinary go test invocation; raise with -rapid.checks for long runs.
The money < 2^57 validity bound was prose describing undefined behavior, protected only by economic invariants living in go-algorand. Export it as a constant instead of enforcing it at runtime: below the bound every exponent in the walk fits int64 even at the most extreme representable probability (1-p >= 2^-64 gives |exp| <= 64*(money-1) < 2^63), and it keeps ~8 bits of headroom over the 10^16 microalgo supply. Consumers assert their supply invariants against the constant in their own test suites -- go-algorand will read it and fail if vFuture/vcurrent consensus parameters could exceed it -- so a future economics change fails loudly in a test rather than silently misrounding consensus. TestSelectF128MaxMoneyHeadroom is the local tripwire.
The previous proof forgot that the stored f128 exponent includes the mantissa normalization offset: v = M*2^exp with M in [2^127,2^128) means exp is about log2(v)-127, so (1-p)^money at the extreme representable probability (1-p just above 2^-64) needs a stored exponent near -64*money-127, not -64*(money-1). At money = 2^57-1, admitted by the old bound, that is about -2^63-63 and wraps int64: empirically, newBinomialF128(2^64-2, 2^64-1, 2^57-1) produces pmf(0) with exponent +9223372036854775745. Intermediate a.exp+b.exp sums inside mul reach about -64*money-256 and wrap slightly earlier still.

At 2^56 every stored exponent and intermediate stays within ~2^62+2^8, a factor-of-two margin. The doc also overstated the headroom: the bound sits ~7x (about 2.8 bits) above the 10^16 microalgo supply, not 8 bits; the tripwire test now requires 2 bits and states the actual figure, and the rapid divisor band reads the constant instead of a literal.
Since Go 1.20 the global math/rand is randomly seeded, and the test's 2% tolerance is only ~2 sigma at N=1000: measured 21 failures in 500 runs. A fixed seed keeps the sanity check stable in CI. This flake predates the SelectF128 work (the test exercises the cgo Select only) and explains a one-off suite failure observed while validating unrelated changes.
…ity property

Go's mutator explores integers locally around corpus values, so every input regime needs a seed planted in it. Coverage of f128.go from the seed corpus alone had 31 uncovered blocks; this brings it to 6, all provably-unreachable defensive arms. New FuzzF128Ops seeds: constructed exact-tie vectors for mul (both tie directions), an add tie at exponent gap 128 into an all-ones mantissa (exercising carry-out renormalization), gap 129 (addend fully below the round bit), constructed divStep qhat-cap vectors (plain and rhat-carry), a mined refine-decrement-overflow vector, denormalized mantissas, and a zero operand. New FuzzSelectF128 seeds: an exact-halfway digest (the denominator-correction branch, ~2^-128 density), small digests reaching each normalization word, fall-through-to-money via both the full walk (p=1/2) and the freeze short-circuit (tiny p), p just below 1 (deep exponents), extreme total/expected magnitudes, and totalMoney == 0. All tie/carry/divStep vectors were constructed or mined by an instrumented search and are verified against big.Float by the fuzz bodies themselves on every go test run.

The one uncovered branch worth a comment instead of a seed: divStep's add-back is believed unreachable -- the refine loop runs to fixpoint with an exact 128-bit test (equivalent to U - qhat*V >= 0), unlike Knuth's Algorithm D, which bounds the D3 adjustment and needs D6; a 3M-case instrumented search never fired it. Documented at the branch.

The rapid tests gain structure-banded mantissa generation (uniform/sparse/dense, raising tie and carry densities from ~2^-64), banded exponent gaps around add's 64/127/128/129 alignment boundaries, oracle-independent mul/add commutativity checks, and TestRapidSelectF128DigestMonotonic: the selection count is non-decreasing in the digest, an exact property of the walk that needs no oracle. That narrows, but does not close, the differential tests' structural blind spot: a defect mirrored into the oracle now cannot violate ordering unnoticed, but an order-preserving one (like the pmf(0) plateau, where the stuck band returns the maximal count) would still pass; that class is covered by the dedicated frozen-tail pins instead.

CI runs the rapid tests at -rapid.checks=20000 in a separate workflow step: deep enough to sample every generator band reliably (the divU shallow-quotient bug reproduced within ~30 banded cases), ~1.3s on a laptop.
Full-suite coverage showed shl128's n==0 and n>=128 arms, shr128's n>=128 arm, f128FromUint64(0), and cmp's zero-operand arms as unreachable: norm128 only shifts by 1..127 and CDF boundaries are never zero, so neither the walk nor any differential harness can exercise them. They are total functions with defined answers, so TestF128PrimitiveEdges asserts them by direct call, turning untested defensive code into tested semantics. f128.go coverage is now 100% minus one branch: divStep's add-back, which is unreachable under any inputs (the fixpoint-refinement argument does not even need divStep's preconditions) and stays documented rather than covered. Package coverage: 98.1%.
nullun
nullun previously approved these changes Jul 21, 2026

@nullun nullun left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can't identify any other issues. Everything looks good to me.

Three assurance layers beyond differential-vs-oracle testing, which is structurally blind to defects mirrored into the oracle (see docs/2026-07-21-sortition-f128-testing-blind-spots.md in the go-algorand docs area). TestSelectF128NearExactMath compares the walk against a 512-bit reference with the near-exact digest ratio and requires agreement within one boundary everywhere outside the defined frozen sliver, including supply-scale spot cases that nothing previously checked against any reference; the spots carry a mustAssert flag so a carve-out change can never silently skip them (an early version of the sliver bound misused big.Float SetMantExp, which multiplies rather than sets the exponent, and the spots passed vacuously until the flag caught it). TestSelectF128BoundaryStraddle constructs digests one ratio-ulp below, at, and above oracle CDF boundaries and requires bit-level agreement plus monotone transitions exactly where knife-edge bugs live. TestRapidSelectF128ScaleInvariance requires bit-identical results under power-of-two scaling of totalMoney and expectedSize, an exact oracle-free metamorphic property.

mutation_check.go (go run mutation_check.go) applies 33 curated single-site mutants to f128.go and requires the fast suite to kill each: 28 killed, 5 survive as proven-equivalent with the proof recorded in the table (among them: div cannot produce exact ties, the halfway correction makes n0's sticky redundant, and the refine loop's strictness is immaterial on exact digits). The campaign found two real gaps, both fixed here: no test broke a mul hi-branch tie through p0 alone (new constructed seeds for mul, add gap-128, divU remainder-only sticky, and a halfway-plus-low-bit digest family), and norm128 -- now used only as the harnesses' input constructor -- could corrupt values invisibly because the reference was derived downstream of it (the fuzz body now checks it against the raw words).
cce added 9 commits July 21, 2026 13:28
The differential oracle shares the PMF recurrence with the implementation, so a shared algebra error would pass every differential test. selectExactRat computes the walk against the exact binomial CDF from first principles: stdlib big.Int.Binomial coefficients and pure integer cross-multiplication (t * T^money <= cdfNum(j) * (2^256-1)) -- no recurrence, no rounding, no floating point. TestSelectF128VsExactRat requires agreement within one boundary for money <= 50, over random inputs, near-maximum digests, and digests constructed to sit exactly on true CDF boundaries.

TestSelectF128Distribution mirrors TestSortitionBasic (which covers only the cgo path) for SelectF128 at toy and realistic stake scales with a fixed seed: summed selection weight must track N * money * p within 2%. Oracle-free and formula-free, so a gross semantic error fails it even if perfectly mirrored everywhere else. Both tests join the mutation campaign's kill suite via the TestSelectF128 pattern; the campaign still reports 33 mutants, 28 killed, 5 proven-equivalent, 0 unexpected.
Killed mutants fail the rapid tests by design, and each failure wrote a minimized reproducer under testdata/rapid that would then rerun as a stale regression case against the restored code. Pass -rapid.nofailfile in the kill suite.
A separate single-platform job runs go run mutation_check.go on every push: a weakened test lets a mutant survive and a semantic change to the arithmetic kills a proven-equivalent mutant or orphans a target string, so the kill-rate claim stays continuously verified instead of decaying into a stale number. The mutant table is deliberately coupled to the exact arithmetic lines it guards; editing those lines requires updating the table. Also drop an out-of-repo doc path from the tool header.
TestSelectF128BoundaryStraddle stepped candidate digests by a fixed 2^128 digest units, which is one f128 ratio ulp only for boundaries in [0.5, 1); for small boundaries (a large-mean cdf(0) can sit at 2^-2000) the candidates landed many ulps away, diluting the straddle into ordinary sampling. Derive the step from the boundary's MantExp (2^(exp-128) in digest units, clamped to one digest unit when the ulp is finer than the digest grid), and assert the candidate window genuinely brackets the boundary whenever no candidate was clamped at the digest range's ends.
Add exact-integer primitive checks, an exhaustive small-domain boundary grid, and offline Arb-certified large-money quantile vectors.

Include the new tests in the curated mutation campaign and pin the optional oracle dependency.
Add exact, multiprecision, trajectory, metamorphic, and mutation checks for the f128 CDF walk.

Schedule certified Arb corpus verification and document the testing layers and developer commands in TESTING.md.
Comment thread mutation_check.go
Comment thread .github/workflows/test.yml
Comment thread f128_trajectory_test.go
Comment on lines +95 to +97
if got := SelectF128(money, total, expected, Digest{}); got != 0 {
t.Fatalf("domain-edge ratio zero selected %d, want 0", got)
}

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the only end-to-end SelectF128 call with money near the 2^56 domain bound, but it uses the zero digest, so the walk exits immediately at j=0. That means the band between the mainnet supply (~2^53) and SelectF128MaxMoney (2^56) is covered by the exponent-overflow audit only. No test in that range ever compares an actual selection against an oracle with a nonzero digest.

Not blocking, since the audited exponent bound is what actually matters here, but worth either adding one oracle-compared case with a nonzero digest above 10^16, or a note documenting that coverage in this band is intentionally audit-only.

@cce cce Jul 22, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm a little nervous adding something like a panic on this end but I did export sortition.SelectF128MaxMoney so it could be used in a test like TestSortitionMoneyDomain in algorand/go-algorand#6672, or a check like the ones on the calling side like
https://github.com/algorand/go-algorand/blob/66af8f8c2f47fdf70077cf40ea116fefa660364f/data/committee/credential.go#L102-L108

Comment thread .github/workflows/test.yml
cce added 4 commits July 22, 2026 12:17
Go's int is 32-bit on GOARCH=386, the platform width that motivates the explicitly-int64 f128 exponent. x86-64 runs i386 user code natively, so this validates cross-GOARCH bit-identity with no QEMU; gcc/g++-multilib supplies the 32-bit toolchain for the cgo/Boost build (Go adds -m32 automatically).
armv7 (GOARM=7) has the same 32-bit int as 386 but on real ARM hardware like the Raspberry Pi. It has no native path on the amd64 runner, so it runs under QEMU via a foreign-arch container; the stock golang image carries gcc/g++ and Boost is vendored, so no extra install is needed. Emulated and thus the slowest leg, so it runs only the default rapid depth.

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR adds a new deterministic, pure-Go sortition implementation (SelectF128) built on a custom software 128-bit floating type (f128) and introduces a multi-layer testing/oracle strategy (including offline Arb-certified vectors) plus CI automation to continuously validate determinism and numerical correctness.

Changes:

  • Implement SelectF128 and its supporting f128 arithmetic and binomial CDF walk in pure Go for bit-identical, platform-independent results.
  • Add extensive correctness verification: big.Float differential oracle, exact-integer rounding oracle, exact binomial math, exhaustive grids, Arb-certified large-money vectors, rapid properties, fuzzing, and a curated mutation campaign.
  • Add offline Arb oracle tooling + certificates, update docs/runbooks, and expand CI to run cross-arch tests, mutation checks, and nightly oracle verification.

Reviewed changes

Copilot reviewed 20 out of 22 changed files in this pull request and generated 5 comments.

Show a summary per file
File Description
tools/requirements-oracle.txt Pins the Python dependency used for the offline Arb certificate generator.
tools/generate_arb_oracle.py Offline generator/verifier for rigorous Arb-based binomial-CDF certificates.
TESTING.md Documents the testing strategy and developer runbook for the new deterministic path.
testdata/f128_arb_certificates.json Checked-in Arb-certified vectors used as an independent correctness oracle.
sortition.go Introduces SelectF128 and the exported SelectF128MaxMoney domain bound.
sortition_test.go Stabilizes baseline sanity test inputs and adds a bound “tripwire” test.
README.md Links to TESTING.md and updates copyright.
oracle_hardening_test.go Adds hardening tests to ensure high-precision oracles converge and match certified/exact results.
mutation_check.go Adds a curated mutation-testing harness to continuously validate test strength.
go.mod Updates Go version and adds pgregory.net/rapid dependency.
go.sum Adds checksums for the rapid dependency.
f128.go Implements software f128 arithmetic and the deterministic CDF walk used by SelectF128.
f128_trajectory_test.go Adds trajectory/liveness and “freeze” correctness tests plus step-count bounds.
f128_test.go Adds fuzz targets, differential oracle checks, edge-case tests, and benchmarks for SelectF128/f128.
f128_rapid_test.go Adds rapid property tests and metamorphic properties for f128 and SelectF128.
f128_integer_oracle_test.go Adds an exact-integer oracle for rounding/normalization to avoid big.Float circularity.
f128_exact_test.go Adds near-exact/high-precision comparisons and exact-rational / exact-CDF validations.
f128_arb_certificate_test.go Verifies the Arb certificate inequalities and pins SelectF128 to certified quantiles.
cdf_exhaustive_test.go Adds exhaustive small-domain boundary-grid testing against exact binomial math.
.gitignore Ignores the local Python virtualenv used for the offline oracle.
.github/workflows/test.yml Expands CI coverage across OS/arch (incl. 32-bit) and adds rapid+mutation jobs.
.github/workflows/oracle.yml Adds scheduled/manual workflow to verify Arb corpus reproducibility.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread f128_test.go
Comment thread f128_test.go
Comment thread TESTING.md
Comment thread f128_rapid_test.go
Comment thread sortition_test.go
Comment thread f128.go
// digest ratio directly at f128 precision, and the success probability as its
// exact integer numerator and denominator rather than a float64 quotient.
//
// Precondition: money < SelectF128MaxMoney (2^56). Below that bound no int64

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

idk, maybe to have an explicit check money < SelectF128MaxMoney in SelectF128

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I didn't want to add an error return, I guess I could have though, but was planning to add a check to the calling side like we already have in
https://github.com/algorand/go-algorand/blob/66af8f8c2f47fdf70077cf40ea116fefa660364f/data/committee/credential.go#L102-L108

@cce
cce merged commit d1d6e8e into main Jul 22, 2026
10 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants