-
Notifications
You must be signed in to change notification settings - Fork 7
Add SelectF128 sortition implementation #8
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
37 commits
Select commit
Hold shift + click to select a range
6c91e65
add f128 deterministic sortition implementation
cce b479649
add FuzzF128Ops
cce c4febea
trim comments
cce 623a567
add direct 256-bit digest-to-f128 ratio conversion and passes an f128…
cce 0b07a39
add TestSelectF128RatioExactlyOne
cce b646576
add f128 sub, compute 1-p natively in newBinomialF128
jannotti 789f596
add f128 div, drop big.Float from newBinomialF128 entirely
jannotti a6645ef
fuzz sub and div in FuzzF128Ops, add BenchmarkSelectF128
cce da28510
take expectedSize as uint64 in SelectF128
cce 9902d6d
update comment
cce 0fdbb9d
correct ratio==1.0 docs: both walk outcomes occur; pin both branches
cce eec84b8
clarify tail-edge divergence wording in SelectF128 doc
cce 6b0359c
short-circuit the walk when the accumulated CDF freezes
cce e59c909
document frozen-tail risk under consensus bounds
cce 0861bcf
make the f128 exponent explicitly int64
cce acafe69
fix divU rounding for shallow quotients (divisors above ~2^62)
cce ea6538c
add pgregory.net/rapid property tests beside the go fuzz targets
cce 228fc16
export SelectF128MaxMoney as the walk's domain bound
cce 924c168
lower SelectF128MaxMoney to 2^56 with a corrected exponent-safety proof
cce e2531e7
seed TestSortitionBasic deterministically
cce c190cfa
seed the fuzz blind spots, band the rapid generators, add a monotonic…
cce 4008e65
pin the defensive primitive arms with direct unit tests
cce 118d53f
add 512-bit tolerance oracle, knife-edge tests, and a mutation campaign
cce 24e9501
add an independent-formula exact oracle and a distribution test
cce 8552735
mutation_check: suppress rapid failfiles from killed mutants
cce 43b0ab0
run the mutation campaign in CI
cce d5f8c1e
scale the straddle step to the boundary's own ulp
cce 003ae1b
bump actions versions
cce f3f8709
go version for actions
cce b7835fb
fix args in windows CI
cce 237ce64
test: add independent f128 and CDF oracles
cce 288b270
test: harden f128 oracle and liveness coverage
cce 357a49c
fix CI and update copyright
cce 5c06920
CI: use original job name
cce 193a7f9
ci: add native linux/386 leg to exercise 32-bit int
cce 51f9204
ci: add emulated linux/arm/v7 leg (Raspberry Pi target)
cce 26c0c59
CI: add cancel-in-progress: true
cce File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,28 @@ | ||
| name: Regenerate numerical oracle | ||
|
|
||
| on: | ||
| schedule: | ||
| # The full supply-scale Arb corpus takes roughly two minutes. Running it | ||
| # nightly catches certificate/generator drift without burdening every PR. | ||
| - cron: "17 5 * * *" | ||
| workflow_dispatch: | ||
|
|
||
| permissions: | ||
| contents: read | ||
|
|
||
| jobs: | ||
| arb-certificates: | ||
| name: Verify Arb certificates | ||
| runs-on: ubuntu-latest | ||
| timeout-minutes: 15 | ||
| steps: | ||
| - uses: actions/checkout@v7 | ||
| - uses: actions/setup-python@v6 | ||
| with: | ||
| python-version: "3.11" | ||
| cache: pip | ||
| cache-dependency-path: tools/requirements-oracle.txt | ||
| - name: Install python-flint | ||
| run: python -m pip install -r tools/requirements-oracle.txt | ||
| - name: Regenerate and compare certified quantiles | ||
| run: python tools/generate_arb_oracle.py --check testdata/f128_arb_certificates.json |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| .venv-oracle/ |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,95 @@ | ||
| # Testing sortition | ||
|
|
||
| The test suite combines bit-identical differential testing, independent exact | ||
| mathematics, metamorphic properties, certified offline vectors, and mutation | ||
| testing. No single oracle is treated as sufficient for the consensus-critical | ||
| `SelectF128` path. | ||
|
|
||
| ## Common commands | ||
|
|
||
| ```sh | ||
| # Complete ordinary suite | ||
| go test -count=1 ./... | ||
|
|
||
| # Property tests at the depth used by CI | ||
| go test -run TestRapid -rapid.checks=20000 -count=1 ./... | ||
|
|
||
|
cce marked this conversation as resolved.
|
||
| # Curated production and test-oracle mutation campaign | ||
| go run mutation_check.go | ||
|
|
||
| # Longer fuzzing runs | ||
| go test -run xxx -fuzz FuzzF128Ops -fuzztime 10m | ||
| go test -run xxx -fuzz FuzzSelectF128 -fuzztime 10m | ||
| ``` | ||
|
|
||
| ## Assurance layers | ||
|
|
||
| | Approach | Purpose | Location | | ||
| |---|---|---| | ||
| | Ordinary and compatibility tests | Basic sortition behavior, benchmarks, agreement with the deployed C++/Boost path, defined frozen-tail behavior, and current-scale regression cases | `sortition_test.go`, `f128_test.go` | | ||
| | Bit-identical 128-bit oracle | Mirrors the production CDF walk with 128-bit `math/big.Float`; detects implementation defects in the hand-written integer arithmetic | `selectBigOracle` and related tests in `f128_test.go` | | ||
| | Primitive differential fuzzing | Checks f128 arithmetic against `big.Float`, with constructed tie/carry seeds and magnitude-banded rapid generators | `FuzzF128Ops` in `f128_test.go`, `TestRapidF128Ops` in `f128_rapid_test.go` | | ||
| | Exact-integer RNE oracle | Computes normalization and round-to-nearest-even solely with `big.Int` quotient/remainder arithmetic, avoiding shared reliance on `big.Float` | `f128_integer_oracle_test.go` | | ||
| | Division certificates | Proves sampled `divStep` digits satisfy `U = q*V + R` and `0 <= R < V`, including quotient-estimate corner paths | `TestDivStepExactCertificate` in `f128_integer_oracle_test.go` | | ||
| | Exact binomial formula | Builds the CDF from binomial coefficients and integer cross-products rather than the production PMF recurrence | `f128_exact_test.go`, `cdf_exhaustive_test.go` | | ||
| | 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` | | ||
| | 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` | | ||
| | Mutation testing | Applies curated bugs to production code and in-process test oracles; every non-equivalent mutant must be killed | `mutation_check.go` | | ||
|
|
||
| ## Arb corpus | ||
|
|
||
| The Arb generator is an offline tool and is not a dependency of ordinary | ||
| `go test`. Set it up in an ignored virtual environment: | ||
|
|
||
| ```sh | ||
| python3 -m venv .venv-oracle | ||
| .venv-oracle/bin/pip install -r tools/requirements-oracle.txt | ||
| ``` | ||
|
|
||
| Regenerate the corpus or verify it without rewriting the checked-in file: | ||
|
|
||
| ```sh | ||
| .venv-oracle/bin/python tools/generate_arb_oracle.py \ | ||
| > testdata/f128_arb_certificates.json | ||
|
|
||
| .venv-oracle/bin/python tools/generate_arb_oracle.py \ | ||
| --check testdata/f128_arb_certificates.json | ||
| ``` | ||
|
|
||
| The Go certificate test exactly compares the stored dyadic endpoints with the | ||
| digest ratio. Trust in the external tool is limited to Arb's assertion that | ||
| 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. | ||
| - `money` must remain below `SelectF128MaxMoney`. The maximum-domain exponent | ||
| audit checks the worst representable `1-p` combination without performing a | ||
| supply-sized walk. | ||
| - Large-money in-process oracles have a committee-scale step budget. A broken | ||
| reference must fail loudly instead of hanging while attempting trillions of | ||
| iterations. | ||
| - Randomized tests use deterministic seeds. Measure-zero events such as exact | ||
| ties and inclusive boundaries are constructed explicitly rather than left | ||
| to sampling. | ||
| - Tests with skip or clamp paths need anti-vacuity counts or mandatory spot | ||
| cases proving that meaningful assertions ran. | ||
|
|
||
| ## Continuous integration | ||
|
|
||
| - `.github/workflows/test.yml` runs builds, ordinary tests, and 20,000-check | ||
| rapid properties across Linux amd64/arm64, macOS amd64/arm64, and Windows | ||
| amd64. It also runs the mutation campaign on Linux. | ||
| - `.github/workflows/oracle.yml` regenerates and compares the complete Arb | ||
| corpus nightly and on manual dispatch. | ||
|
|
||
| When arithmetic or recurrence semantics change, update the relevant | ||
| independent oracle and exact/certified vectors deliberately, then rerun the | ||
| full suite and mutation campaign. A changed knife-edge pin is evidence that | ||
| the numerical trajectory changed and should be explained in the commit. | ||
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.