Principles and verification

Ten rules hold across the package, and each one has machinery that keeps the code to it. This page states the rules, then the checks.

Ten invariants

From the normative top-level design. The shapes of a Refusal, a Gate and a run record elsewhere on this site are what these rules look like once they reach code.

1. One fact has one place of declaration. The Graph is the single source of model truth.
2. Compile first, then execute. An optimization must verify its premise; when the premise fails, refuse or degrade, never apply it silently.
3. Keep statistical objects distinct. Prior, likelihood, marginal likelihood term, evidence and posterior may not share names.
4. Every conclusion has an applicability. When a required diagnostic is missing, abstain rather than default to trusted.
5. The approximation level must be visible. Exact, certified deterministic, Monte Carlo and heuristic may not blur into one kind of result.
6. Run conditions must be traceable. Seed, dtype, device, backend, version, data identity and budget are part of the result.
7. External backends do not define the core API. An adapter obeys bayesmith's task and result protocol.
8. An agent cannot bypass a gate. It may only choose among the legal actions the current state exposes.
9. Failure is a first-class artifact. A Refusal states its evidence, the failed premise and the available remedies, not just exception text.
10. Eliminate before brute force. Structure that can be reliably identified and eliminated exactly takes precedence over a general, expensive algorithm.

Four of them are enforced by a test rather than by review:

The test suite has two layers

The heavy numerical-gate boundary grids and mutation grids are marked full; everything else is the fast layer, run before a commit and selected with -m "not full". That split can hide a loss of coverage, so a meta-test guards it: every registered numerical gate must keep at least one executable cell in the fast layer, and the selected cells must run and agree with the registry. The fast layer cannot quietly become "no numerical-gate coverage".

Every threshold has a provenance

A numerical threshold in this package is registered rather than written inline. Each entry records where the number came from, as one of derived, borrowed, magic, exact-or-domain and API-contract, together with the quantity it bounds, the outcome it admits and refuses, its oracle, the input axes to sweep including their extremes, and how it may be mutated (two-sided, static-only or policy-only).

The registry is itself checked: the committed source manifest must match a fresh scan of the tree, a registered atom must really live under the source it claims, an entry may not authenticate its own non-canonical mutation target, and "static" may not be used to avoid a two-sided grid that a threshold deserves.

References that share nothing with the implementation

Comparing two readings that share an implementation proves little: the package records a case where two such readings agreed on a log density of −225.65 while the truth was −364.95. So the exact routes are checked against references chosen for what they do not share.

• A dense reference assembles the block's operator column by column on a basis of its domain and solves the normal equations with NumPy. It shares the model, as it must, and shares none of the linear algebra: no linearization, no vector-Jacobian products, no conjugate gradients.
• NUTS is the cross-check for the exact routes, because a graph that qualifies for an exact solve can also be run through the general sampler. Its own recovery is measured against a closed-form conjugate posterior whose prior and likelihood precisions are chosen so that a silently dropped prior term would show.
• The evidence assembly is checked against a hand derivation and against quadrature of the graph's own joint density, because its natural sibling route shares too many seams to be independent. The package says so in its own source.

A guard is tested by building the bypass

Two guards here assert a property rather than a spelling, and both were repaired after a reviewer wrote the code that walked past them.

The first requires that the package stamps one producer on its artifacts. Written as a search for a constructor call, it stayed green when the duplicate was introduced under an alias. It now asserts identity: every module exporting that name must export the same object, and a second construction is a different object however it is spelled.

The second requires that the model-checking gate decides no number of its own. Written as a search for float literals and comparison operators, it was literally true of a bypass that spelled its threshold int("40") and compared with operator.lt, which passed every test in the file while turning a required check's failure into a pass. It now asserts the consequence: a filed slot must hold the very object the owning check returned.

Mutation, with the exit codes taken seriously

A repair that cannot show what it still kills is not finished. Gate mutations run in process: the harness recompiles one function, installs it for the duration of a context manager, proves the mutated expression was reached, and restores on every exit path without editing a file. Wider mutation runs are a written protocol with recorded tables, and its rules come from damage: restore only the path the mutant touched, clear the bytecode cache between mutation and restore, and commit before mutating, because the restore is to the last commit and will otherwise revert unfinished work. Only exit code 1 counts as a kill; an interrupted run or a run that collected nothing is neither a kill nor a pass.

The suite meets Linux before a version number is spent

Four release tags were burned by a suite that met Linux only in the publishing job, which runs after the tag is pushed and a version number is spent once used. One of those releases failed there with sixteen failures while the same wheel passed on the development laptop, most of them fixtures that had written down one machine's arithmetic and called it a property.

On every push and pull request a workflow now builds both distributions on Linux, rebuilds the wheel from the extracted source archive and runs the fast layer from that archive against the installed wheel, so a packaging fault or a platform-dependent fixture surfaces before any tag exists. The release job then runs the full suite on Linux against the built wheel, and nothing is uploaded unless it passes. The runner pool is heterogeneous, and a boundary cell can pass on one CPU and fail on another, so a green run is evidence about the machine it drew. Only exit code 1 is scored as a test failure.

What a fixture may do about a platform difference is a rule in its own right: construct the stress deterministically, or assert the property with a band whose form is derived, or make the platform-dependent premise conditional while the contract stays unconditional, or skip loudly. Widening a tolerance to reach green is not on the list, and this documentation follows the same rule: recorded numbers carry the platform they were measured on, and the test suite re-checks the structure rather than the digits.

The documents are checked too

Every page under docs/ declares its own status, exactly one document is normative, and the index is generated from those declarations. A test compares the two directions, so a new page with no status and an index row pointing at nothing both fail. This site is rebuilt and compared against the source on every run, and the plans it prints are re-measured. See contributing and verification for the commands.