fineness

A framework that certifies numerical and stochastic software.

This document uses Simplified Technical English (ASD-STE100, Issue 8). It follows the STE writing rules. An approved-dictionary tool does not verify it yet.

A result cannot have a higher trust level than its least-certified input. Also, a check certifies nothing until you show that the check can fail, and that it did not fail.

fineness finds one type of error. This error does not stop the program. The program gives a number that seems correct, but no independent method verifies the number. fineness makes four rules mandatory. Read PLAN.md for the full design.

Status

Version 0.2.0 has the core object, the mutation engine, and the ledger. The core object is Estimate. An Estimate cannot exist without a measured standard error. The object also has the agreement functions. These functions compare two estimates inside a measured band. When the two estimates have their raw draws, the comparison uses the paired difference. The shared noise then becomes zero.

The mutation engine adds @check and @mutation. A check compares an estimate with a reference. A mutation breaks the code, and the engine confirms that the check fails. A check that no mutation can detect has the status UNCERTIFYING.

The ledger adds trust levels and the one-direction rule. A component cannot have a higher level than its weakest input. The command fineness verify is the CI gate.

Version 0.3.0 adds two source tools. The independence tool measures whether two functions share a code path, so provenance="independent" becomes a measured fact. The held-out tools split the data and guard against a leak between the fit and the eval.

Version 0.4.0 adds a completeness critic. The command fineness mutants changes small operators in a module and reports how many of these changes a check detects. A change that survives is a gap in the check.

Version 0.4.1 adds two items from real-world use. A check marked exact=True (a deterministic comparison) can earn L2 without a measured band. The command fineness mutants refuses a numba module, because each mutant would recompile the JIT kernels.

Version 0.4.2 separates the two failures of the command. Exit code 1 is a result: the gate found a red ledger or an UNCERTIFYING check, and the build must stop. Exit code 2 is not a result: the command could not run. A name is wrong, a file is absent, or the tool needs an optional dependency. Exit code 2 prints one line. A traceback stays for an unexpected error only.

The pre-registration tool comes later. See PLAN.md, section 13.

Installation

pip install fineness            # the core is stdlib-only
pip install "fineness[yaml]"    # a .yaml ledger needs PyYAML; a .json ledger needs nothing
pip install "fineness[auto]"    # `fineness mutants` on a numpy module

Installation from source

1. Open a terminal in the project folder.

2. Type this command to install the package:

   pip install -e ".[dev]"
   

3. Type this command to run the tests:

   pytest
   

The core uses only the Python standard library. It needs Python 3.10 or a later version. It does not need numpy.

Function of the core object

The standard error is mandatory. This rule is the reason for the object.

from fineness import Estimate

Estimate(0.5)                    # the object raises MissingErrorBar
Estimate(0.5, se=0.02)           # correct
Estimate(0.5, se=0.0)            # correct, but you must state that the value is exact

The agreement function compares two estimates inside a measured band.

rake = Estimate(0.0914, se=0.0013, estimand="rake_pct at pot=12000")
ref  = Estimate(0.0900, se=0.0011, estimand="rake_pct raise-line")

rake.agrees_with(ref, tol="2se")   # a measured band, not a fixed floor
# <Verdict PASS residual=+0.0014 z=0.82 tol=2 se paired=False>

If the two estimates have their raw samples, the function uses the paired difference. The shared noise becomes zero. The function then compares the difference, and not two independent means.

The mutation engine

A check compares an estimate with a reference. A mutation breaks the code. The engine runs the check again and confirms that the check now fails. A mutation that the check detects has the status KILLED. A mutation that the check does not detect has the status SURVIVED. A SURVIVED mutation means that the check is blind. So a check certifies only when it passes and it detects every mutation.

import math
import pi_estimator
from fineness import check, mutation

@check(against="math.pi", tol="4se", provenance="independent")
def pi_matches_closed_form():
    est = pi_estimator.estimate_pi()
    return est.agrees_with(math.pi, tol="4se")

@mutation(pi_matches_closed_form, describe="use the factor 3 in the place of 4")
def _mut_wrong_factor(patch):
    patch.replace("pi_estimator.FACTOR", 3.0)

Run the engine:

import checks, fineness
print(fineness.report(fineness.run_all(seed=0)))

CHECK pi_matches_closed_form                       PASS  (residual 0.6 se)
  - mut: use the factor 3 in the place of 4           KILLED   (residual 89.9 se)  ok
  - mut: report a standard error near zero            KILLED   (residual 6407346.4 se)  ok
  CERTIFYING? YES

The examples/mc_pi/ folder has the full example. For pytest, fineness.pytest_cases() gives one test for each check and one test for each mutation.

The ledger

The ledger records a trust level for each component and its inputs. The level goes from L0 to L3. The effective level of a component has three limits: the declared level, the local evidence, and the level of each input. It is not higher than any of them. So a result cannot have a higher level than its weakest input.

# fineness.ledger.yaml
components:
  pi_estimate:
    level: L2
    evidence: [pi_matches_closed_form]
  pi_report:
    level: L2
    inputs: [pi_estimate]      # it inherits the level of pi_estimate

The command fineness verify loads the ledger, computes the effective level of each component, and fails on a component that declares a level above the limit:

fineness verify --ledger fineness.ledger.yaml --import checks

The level contract: L1 needs an independent certifying check. L2 adds a measured band. L3 adds a passing invariant and a scope. A blind check (a check with a surviving mutation) supports no level above L0.

Independence and held-out data

Two functions are independent when they share no domain module. The independence tool measures this. So a check can prove that its reference does not share a code path with the estimator:

from fineness import assert_independent

@check(against="brute_force", tol="2se", provenance="independent")
def foo_matches():
    assert_independent(estimate_foo, brute_force)     # measured, not only a claim
    return estimate_foo(x).agrees_with(brute_force(x), tol="2se")

A mutation that makes the reference share the estimator code then breaks the check. The measurement is a heuristic on the direct module dependencies, so a clean result means "no shared domain module", not "proven independent".

The held-out tools split the data and guard against a leak. A Dataset splits into a train part and a test part. Each part records its use, and the guard reports a leak:

from fineness import Dataset

ds = Dataset(rows, name="data")
train, test = ds.split(test_frac=0.5, seed=0)
model = fit(train.use_for("fit"))
score = evaluate(model, test.use_for("eval"))
ds.assert_no_leakage()      # fails if a split served both a fit and an eval

The examples/held_out/ folder shows the guard. On separable data the accuracy is 1.0 on the train part and on the test part. So the number hides the leak. Only the guard finds it.

The completeness critic

The authored mutations record the failure modes that a person thinks of. The command fineness mutants adds a second signal. It changes small operators in a module (for example + to -, or < to >=). It then reports how many of these changes the check detects. A change that survives is a gap: the check plus its assertions are blind to that change.

fineness mutants --module pi_estimator --check pi_matches_closed_form --import checks

AUTO-MUTANTS  module=pi_estimator  check=pi_matches_closed_form
  killed=12  survived=2  errored=0  score=0.86
  survivors (the check is blind to these changes):
    - line 17 col 25: 20000 -> 20001
    - line 24 col 10: Div -> Mult

This is a coverage signal, not evidence. The ledger does not use it. Some survivors are equivalent changes with no effect, so a person judges the list. In the example above the second survivor is a real gap. The check confirms the value of pi, but it does not confirm the standard error. So a wrong standard error survives.

Difference from other tools

Each other tool does one part of the work. pytest runs the code. hypothesis makes input data. mutmut measures the coverage of a test suite. great_expectations tests the shape of data. No tool does the central task.

fineness has one main difference. A check that cannot fail is an error. Also, the trust level of a number cannot be higher than its weakest input. See PLAN.md, section 14, for the full comparison.

Documentation rules

The documents follow the ASD-STE100 writing rules. A checker verifies the objective rules on each pull request. Run the checker:

python tools/ste_check.py README.md PLAN.md

The checker tests the objective rules. It gives an error for a long sentence, a contraction, a Latin abbreviation, an ampersand character, or a non-STE word. It gives a warning for a heuristic rule: the passive voice, an "-ing" verb form, or a long paragraph. The CI fails on an error. A warning is advisory. The checker does not verify the approved STE dictionary.

License

Apache-2.0. Read the LICENSE file.