Baller

The content on this page was written by AI under human supervision.

Baller is the BootLoops package for calculations in ball arithmetic, where every number is stored as a midpoint together with a radius guaranteed to contain the true value. You give it an expression, an iteration, an integral, a linear differential equation to continue along a path, or a candidate solution of a system of equations; it returns an enclosure with a proven error bound, the decimal digits that the bound certifies, or an error saying it could not certify what you asked for. The arithmetic is done by Arb through the python-flint bindings; Baller adds driver routines, certification tests, consistency checks and source checks around it.

What it does

Floating-point code can converge confidently to a wrong answer. The standard demonstration is Muller's recurrence $x_{n+1} = 111 - 1130/x_n + 3000/(x_n x_{n-1})$ with $x_0 = 2$, $x_1 = -4$: the true limit is 6, but in double precision the sequence settles on exactly 100. In ball arithmetic the radius instead grows until the result reads "unknown", and Baller's top-level routines build on that. run executes an expression or an iteration in ball arithmetic at a working precision you choose. solve reruns at doubled precision until the number of digits you asked for is certified; at its precision cap it raises SolveRefused, reporting the digits it did achieve, instead of returning an unqualified number. render prints only the digits the radius certifies; a value with none comes back as the marked string UNCERTIFIED[~mid +/- rad] rather than as a bare number. One convention differs from Arb's. When an iteration divides by a ball containing zero, the radius becomes infinite and the midpoint continues as the plain fixed-precision value; you still see where floating point would have gone, and the result stays marked uncertified.

Five modules sit below the top level. baller.quad computes definite integrals with a proven error bound through Arb's rigorous integrator, and also exposes POSQ as quad.posq, imported from the neighboring tools/posq/ package rather than copied. baller.transport continues the solution vector of a linear differential equation with polynomial coefficients from point to point in short Taylor steps, each with a proven bound on the truncated tail. baller.certify turns a numerical candidate into a proven statement with the Krawczyk test: if a certain interval image of a box lies strictly inside the box, the box contains exactly one zero of the system. Its block_krawczyk module handles Jacobians of block-arrow shape (many independent diagonal blocks plus a shared border, as in hierarchical statistical models) at a cost linear in the number of blocks. It can also certify the Hessian positive definite over the box, which together proves a strict local minimum; a refusal names the failing block or border and the margin. Clinch is built on this module.

baller.contract is for quantities computed two independent ways. dual runs both routes and returns the primary value only if they agree to the number of digits you set; otherwise it raises DualPathDisagreement carrying both values, and nothing is averaged. Tripwire applies the same comparison to a deterministic sample of the calls inside a loop. The mutation tester in baller.mutation tests a test: it makes small value-changing edits to scratch copies of a source file and confirms that your acceptance command passes on the untouched copy and fails on every edited one. baller.hygiene holds source checks for precision mistakes that recur in mpmath and python-flint code, such as a working precision written as a fixed literal or a change to flint's global ctx.prec that is never restored. These checks (lints) read a Python file and report risky patterns without running it.

The largest of these checks, dps_lint, is a command-line checker for programs that use mpmath. An mpmath number keeps the precision it was created with, and Python evaluates module-level assignments, default arguments, decorators and class bodies at import time, usually before the line that raises mp.mp.dps from its default of 15 digits. A constant such as T = mp.mpf(-1)/3 built there feeds a 15-digit value into a 100-digit calculation, and the answer is wrong from about the seventeenth digit with no warning. dps_lint reports every such use. It also reports three mistakes that matter only once the file is imported by another: an import that resets the importer's precision, a constant frozen at import (both found when the importing file is checked in the same call), and a precision set only under if __name__ == '__main__':. A further rule flags complex-step mp.diff applied to a function that branches on real comparisons. It exits with status 1 if it found anything. Beside the lints sit runtime helpers for watching radii and restoring precision, and purity_scan, which sorts the numeric literals in a list of Python or C files into a JSON report for a person to review.

Enclosures from run, solve, quad, transport and certify are rigorous provided the functions you pass in are themselves evaluated in ball arithmetic (arb/acb values throughout). The source checks are advisory; a clean report is not a proof. The transport, certification and Monte Carlo engines are copies of code written for specific studies, included with recorded checksums, as are three further module families under vendor/ (listed under Routines). baller.verify() raises VendorTamperError on any mismatch, so call it first. Baller does not do Taylor-model enclosures (see ERAS) and does not wrap or rename Arb's functions (see Arb and mpmath). One pitfall: in python-flint 0.8, x**2 of an arb ball containing zero returns NaN, so write x*x in functions evaluated over a box.

Examples

Run Muller's recurrence at a fixed precision, then with the adaptive driver. The lines are the package's documented quick start:

import sys; sys.path.insert(0, "<your-checkout>/tools/baller")
import baller
baller.verify()
from baller import quad, transport, certify, contract, hygiene
r = baller.run(lambda xp, x: 111 - 1130/x + 3000/(x*xp), x0=(2, -4),
               n=100, dps=50)
res = baller.solve(lambda xp, x: 111 - 1130/x + 3000/(x*xp), 16,
                   x0=(2, -4), n=100)
print(baller.render(res, digits=17))       # -> 6.0000000160995649

r.values holds $x_0$ through $x_{100}$ as balls at 50 digits. baller.render(r.values[30]) prints 6.0056: the radius at step 30 is about $10^{-5}$, so only those digits are certified. A few steps later a divisor ball contains zero (r.blown_at records where), and baller.render(r.values[100]) returns a string beginning UNCERTIFIED whose midpoint is near 100, which is where plain floating point ends up. solve tries 30, 60, 120 and 240 digits (res.attempts) and certifies 6.0000000160995649 at 240; with max_dps=60 it raises SolveRefused with achieved_digits == 0.

Compute a definite integral with a proven error bound. From the self-test suite:

from baller import quad
r = quad.integral_certified(lambda x, _: 4/(1+x**2), 0, 1, prec_dps=60)
right = quad.integral_certified(lambda x, a: x.sqrt(analytic=a), 1, 4, prec_dps=40)

r is a dictionary with 'mid_str', 'rad', 'certified_digits' (at least 50 here; the integral is $\pi$) and 'ball'. The integrand receives the point and Arb's analyticity flag. An integrand with a branch point, such as a square root, must forward the flag as the second call does; a version that ignores it returns a finite but wrong ball. Pass max_rad= to make an over-wide result raise BallBlown.

Compare a quantity computed two ways. From the self-test suite:

from baller.contract import dual, Tripwire, DualPathDisagreement
v, cert = dual(lambda: 1.2345678901234, lambda: 1.2345678901239, digits=10)
dual(lambda: 1.0, lambda: 1.001, digits=6)

The first call returns the primary value unchanged with a record of the digits of agreement. The second raises DualPathDisagreement (three digits of agreement against a threshold of six); the exception carries both values, and neither should be used.

Check an mpmath program for precision set too late. The case from the checker's own documentation: a constant and a default argument built before the precision is raised.

# evaluator.py
import mpmath as mp
T = mp.mpf(-1)/3
def f(x=mp.mpf('0.02')):
    mp.mp.dps = 100
    return x + T
python3 <your-checkout>/tools/baller/baller/dps_lint.py evaluator.py

Two findings are printed, one per line in the form file:line: [where] what :: source line, here evaluator.py:3: [module-level] mp.mpf :: T = mp.mpf(-1)/3 and evaluator.py:4: [default-arg in f()] mp.mpf :: def f(x=mp.mpf('0.02')):; a count goes to standard error and the exit status is 1. The repair is to set mp.mp.dps at the top of the module, or to build T inside the function and fill the default at call time. Directories are searched recursively, and a program should be passed together with the modules it imports, because the cross-file rules only see files given in the same call; a clean run prints dps_lint: clean (N file(s)) to standard error and exits 0.

Routines

Top level (import baller)

baller.quad

baller.transport

baller.certify

baller.contract

baller.hygiene

baller.hygiene.dps_lint (mpmath precision set too late; standard library only)

Vendored modules (vendor/; add the directory to sys.path and import)

Self-tests

Used on this site

Requirements and source

Python 3 with python-flint (Arb), mpmath, numpy, scipy (for mc), sympy (for the exact part of pipe_vac) and pytest (for the certlane part of the self-tests). POSQ and Wayfinder are imported from the same tools/ directory, as laid out in the repository; set BALLER_TOOLS_ROOT if they live elsewhere. dps_lint and purity_scan are part of this package and need only the standard library; the code they check is parsed, never executed, so mpmath need not be installed to run dps_lint. To run the self-tests, change to a scratch directory outside tools/ (the script refuses to run inside the source tree) and run

python3 <your-checkout>/tools/baller/battery/battery.py

The script prints PASS or FAIL per part and one OVERALL line, takes about two minutes, and writes BALLER_BATTERY_SUMMARY.json in the current directory. The POSQ part reports a named SKIP if POSQ's C kernel cannot be built on your machine (it is compiled from source at first use, which needs a C compiler and the FLINT development headers). The three vendor/ module families write output to the current directory (variables such as VALMONO_OUT and SD_ENGINE_OUT override it), never into vendor/, where an extra file makes baller.verify() fail. The code is tools/baller/ in BootLoops' bootloops-dev repository (GitHub organization BootLoops-ai), released under the MIT license. Arb is public software from the FLINT project (LGPL, flintlib.org), used unmodified. A longer write-up is available as a PDF.

← back to the tools index