Skip to content

Python API · Submodule

alkahest.crosscheck

Cross-CAS differential testing — ask a second CAS the same question.

Certificates cover the fragment where Alkahest can prove its answer. Outside that fragment there is nothing checking the answer at all, and the failure that matters for a search loop is not a crash but a silent error: a confident, plausible, wrong result that the loop then builds a hundred derived claims on top of (see tests/silent_errors/README.md). An independent implementation is the cheapest instrument that catches exactly those.

This module runs one query through Alkahest and through an oracle and reports whether they agree — as a four-valued outcome, never a boolean:

agree Both systems answered, and a named comparison rung settled it. diverge Both systems answered and the answers are not the same. The record names two suspects, carries the witness point and both values, and never words itself as "Alkahest is right". incomparable The question could not be posed identically to both systems (an untranslatable node, an assumption context with no faithful mapping, an operation one side refused). Never collapsed into agree. unavailable No oracle is installed. Also never agree — a loop that believes it is cross-checking and is not is worse off than one that knows it isn't.

Quick start

Python

>>> import alkahest as ak
>>> from alkahest.crosscheck import check, oracles
>>> "sympy" in oracles()          # None when SymPy is not installed
True
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> out = check("integrate", ak.sin(x), x)
>>> out.outcome in {"agree", "unavailable"}
True

Design notes

One translator, not four. tests/ already carries four hand-rolled _expr_to_sympy helpers, each covering a different subset. Translator is the one implementation; the tests are meant to migrate onto it. Building the QA harness and the runtime mode separately would produce two translators that disagree, which is the worst possible outcome for a tool whose entire job is detecting disagreement.

Total-or-refuse. Every tag Expr.node() can emit appears in Translator._DISPATCH; an unknown tag, an unmapped primitive, or an assumption context with no faithful counterpart raises CrossCheckError (E-XCHECK-001), which check() turns into incomparable. False divergences are worse than no signal — they train both the loop and the team to ignore the alarm, and a best-effort translator manufactures them by construction.

Opt-in per call site. There is deliberately no context(crosscheck=True): that would put an oracle round-trip on every call, and stage-2 falsification runs millions of times. Call check() where you want it — at stage-5 recording frequency, hundreds of times, not millions.

See docs/mdbook/src/crosscheck.md.

class

class crosscheck.CrossCheck

The outcome of one differential check.

Attributes

operationstr: Operation checked.
outcome{"agree", "diverge", "incomparable", "unavailable"}: See the module docstring. Truthiness is deliberately not defined on this class: if check(...) would read as "it agreed" and would be true for three of the four outcomes under any obvious convention.
rungint or None: Which rung settled it (see RUNG_NAMES); None when nothing did.
reasonstr: Stable short code for why — "invariant_holds", "no_oracle", "untranslatable", "alkahest_refused", "oracle_refused", "ladder_exhausted", and so on. Machine triage should switch on this, not on detail.
detailstr: One human sentence.
oracle, oracle_versionstr or None: Which system answered, at which version.
alkahest_value, oracle_valuestr or None: Both answers, rendered.
witnessdict or None: {"point", "alkahest", "oracle", "enclosure"} when a pointwise witness exists.
divergenceDivergence or None: Populated iff outcome == "diverge".
conclusivebool: Whether the settling rung proves what it reports. Rung 3 agreement is sampled, so it is reported as agreement with conclusive=False rather than being silently promoted or silently discarded.
elapsed_msfloat: Wall-clock cost of the check, oracle round trip included.

Properties

operation: str

outcome: str

rung: int | None

reason: str

detail: str

oracle: str | None

oracle_version: str | None

alkahest_value: str | None

oracle_value: str | None

witness: dict[str, Any] | None

divergence: Divergence | None

conclusive: bool

elapsed_ms: float

rung_name: str | None

Human name of rung (see RUNG_NAMES).

checked: bool

Did a comparison actually happen?

False for incomparable and unavailable. Provided so the common mistake — treating "no signal" as "clean" — has to be written out explicitly.

Methods

as_dict() → dict[str, Any]

JSON-serialisable view.

class

class crosscheck.Divergence

Two systems answered, and the answers are not the same.

The wording is constrained on purpose. A divergence names two suspects: it is evidence that one of the two is wrong, and on its own it is never evidence about which. support carries whatever the rigorous escalation could establish, and its default is "unresolved".

Attributes

operationstr: Operation that diverged.
oracle, oracle_versionstr: Which independent system, at which version. Without the version a recorded divergence rots the first time the oracle changes an answer.
pointdict: Witness: symbol name -> value at which the two disagree. Empty when the divergence is symbolic rather than pointwise.
alkahest_value, oracle_valuestr: Both values, rendered. Never one without the other.
alkahest_enclosuretuple of float, optional: Rigorous ball-arithmetic enclosure computed on the Alkahest side.
support{"unresolved", "alkahest_supported", "oracle_supported"}: What the rigorous escalation established. "oracle_supported" means an operation invariant was rigorously refuted on the Alkahest side — a silent-error finding, and the case that should be routed into tests/silent_errors/corpus/.
regiondict or None: When verified_sign() certified that the failing invariant residual keeps one sign across the whole sampling box, the box: {"x": [0.35, 2.65]}. That upgrades a finding from "wrong at this point" to "wrong on this interval", which is a much shorter argument to hand a reviewer.
detailstr: One sentence, phrased symmetrically.

Properties

operation: str

oracle: str

oracle_version: str

point: dict[str, float]

alkahest_value: str

oracle_value: str

alkahest_enclosure: tuple[float, float] | None

support: str

region: dict[str, list[float]] | None

detail: str

silent_error_candidate: bool

Is this a case for tests/silent_errors/corpus/?

True exactly when rigorous ball arithmetic refuted the Alkahest side of an operation invariant. That is the finding worth converting into a permanent regression gate; everything else is a lead.

Methods

statement() → str

One-line rendering that attributes blame to neither system.

as_dict() → dict[str, Any]

JSON-serialisable view.

class

class crosscheck.FrozenCase

One previously-observed comparison, pinned to an oracle version range.

The per-PR half of the two-tier arrangement. Every case records the oracle version range its expectation was established against: without that the corpus rots silently the first time the oracle changes an answer, which it will, and a red gate would then be indistinguishable from a real regression.

Attributes

idstr: Stable, never reused.
operationstr: An OPERATIONS key.
buildcallable: pool -> tuple of arguments for check(). Takes the pool so each run gets a fresh one.
expectedstr: Expected CrossCheck.outcome.
expected_reasonstr or None: Expected CrossCheck.reason, when the case is pinning why.
oraclestr: Oracle name the expectation belongs to.
oracle_versionsstr: Comma-separated PEP-440-ish range, e.g. ">=1.12,<2". A case whose range excludes the installed version is skipped, not failed.
found_bystr: "seeded sweep, seed=..." or a hand-written provenance note. The ratchet: a divergence the nightly finds must land here.
notestr: What this case is protecting.

Properties

id: str

operation: str

build: Callable[[Any], tuple[Any, ...]]

expected: str

oracle: str

oracle_versions: str

found_by: str

note: str

expected_reason: str | None

Methods

applies_to(version: str) → bool

Does this case's expectation cover version of its oracle?

class

class crosscheck.Operation

How one operation is posed to both systems, and how it is compared.

Attributes

namestr: Matches the alkahest module attribute of the same name.
rungstuple of int: Ladder rungs to attempt, in order. Rung 4 leads wherever it exists, because it sidesteps equal-up-to-a-constant, up-to-ordering and up-to-a-unit entirely — the three things that make naive comparison of antiderivatives, solution sets and factorisations produce nothing but noise.
invariantstr or None: Name of the rung-4 invariant, or None when the operation has none.
result{"expr", "solutions"}: Shape of the answer, which decides how it is compared and rendered.
normalizestr or None: Operation-specific normalisation applied to the Alkahest answer before the ladder runs — currently only "strip_big_o". This is not a rung: it removes a difference in how the two systems spell the same answer, and it must never remove a difference in the answer itself.

Properties

name: str

rungs: tuple[int, ...]

invariant: str | None

result: str

normalize: str | None

class

class crosscheck.Oracle(ABC)

An independent CAS the comparator can interrogate.

The comparator talks to oracles only through this interface, so a second implementation (Wolfram, Maxima, a pinned older Alkahest) drops in without the ladder changing. Two consequences worth stating:

every method may answer "I don't know" — is_zero() returns None, run() raises — and the comparator turns that into incomparable rather than guessing;
lift() is optional in effect but not in signature: it is what lets rung 2 be attempted independently in both systems, which is what makes "either one proved it" a defensible notion of agreement.

Attributes

namestr: Stable short identifier, used as the key in oracles().

Properties

name: str

version: str

Version string of the backing system. Recorded on every result.

Methods

available() → bool

classmethod

Is this oracle usable in this process right now?

translate(expr: Any, *, assumptions: Any=None) → Any

Alkahest Expr -> a term in this oracle's language.

lift(obj: Any, pool: Any) → Any

This oracle's term -> an Alkahest Expr, or refuse.

render(obj: Any) → str

Human-readable rendering, for witnesses and reports.

canonical(obj: Any) → str

Canonical string form, for rung 1.

supports(operation: str) → bool

Can this oracle answer operation at all?

run(operation: str, args: Mapping[str, Any]) → Any

Perform operation in this oracle's own engine.

Raises

CrossCheckError: E-XCHECK-004 when the oracle declines or returns an unevaluated form; a refusal is not a divergence.

is_zero(obj: Any) → bool | None

True/False if decided, None if the oracle could not.

diff(obj: Any, var: Any) → Any

Derivative of obj with respect to the translated variable var.

subs(obj: Any, bindings: Mapping[Any, Any]) → Any

Substitute translated terms for translated symbols.

subs_by_name(obj: Any, point: Mapping[str, float]) → Any

Substitute numbers for free symbols matched by name.

Distinct from subs() because the comparator only ever knows the Alkahest symbol names at a witness point, and rebuilding an oracle symbol from a name would have to re-derive its assumption flags — get that wrong and the substitution silently misses.

to_float(obj: Any) → float | None

Numeric value of obj, or None when it has none.

class

class crosscheck.SweepReport

Result of a seeded differential sweep.

Attributes

seedint: Print this. A sweep is only useful as a bug report if the run that found something can be reproduced exactly.
oracle, oracle_versionstr or None: Which system, at which version. A sweep that turns red after a SymPy upgrade is a different event from one that turns red after an Alkahest change, and only the recorded version tells them apart.
checkstuple of CrossCheck: Every check run, in order.

Properties

seed: int

oracle: str | None

oracle_version: str | None

checks: tuple[CrossCheck, ...]

findings: tuple[CrossCheck, ...]

Checks whose outcome was diverge.

silent_error_candidates: tuple[CrossCheck, ...]

Findings where Alkahest's side was rigorously refuted.

Methods

counts() → dict[str, int]

Outcome histogram, total over OUTCOMES.

to_dict() → dict[str, Any]

JSON-serialisable view, suitable for filing as a CI artifact.

summary() → str

One-screen report; print it from the nightly job.

class

class crosscheck.SymPyOracle()

SymPy as the reference implementation.

The first oracle, and the one the frozen corpus is pinned against. Its version is recorded on every record: without that the corpus rots silently the first time SymPy changes an answer, which it will.

Raises

CrossCheckError: E-XCHECK-002 on construction when SymPy is not importable. The absence is loud by construction — there is no code path in which a missing SymPy yields agreement.

Properties

version: str

Methods

available() → bool

classmethod

translate(expr: Any, *, assumptions: Any=None) → Any

lift(obj: Any, pool: Any) → Any

SymPy term -> Alkahest Expr, refusing anything not exactly representable.

Deliberately narrow. A lift that "mostly works" would put an approximated value into the Alkahest-side rung-2 attempt, and a wrong answer there is indistinguishable from the divergence the module exists to find.

render(obj: Any) → str

canonical(obj: Any) → str

supports(operation: str) → bool

run(operation: str, args: Mapping[str, Any]) → Any

is_zero(obj: Any) → bool | None

diff(obj: Any, var: Any) → Any

subs(obj: Any, bindings: Mapping[Any, Any]) → Any

subs_by_name(obj: Any, point: Mapping[str, float]) → Any

to_float(obj: Any) → float | None

class

class crosscheck.SymPyTranslator(sympy_module: Any)

Translator into SymPy's expression language.

class

class crosscheck.Translator()

Walk an Expr into another CAS's term language.

Subclass once per oracle. The walk, the dispatch table, and the refusal discipline live here; a subclass supplies only the leaf and node constructors of its target language.

The dispatch table is total over NODE_TAGS — that is the property that makes a divergence informative, and tests/test_crosscheck.py asserts it against the tags the Rust binding can actually emit rather than against this list, so a new node kind fails the build instead of quietly translating to nothing.

Assumptions

translate() accepts the governing Assumptions and maps its predicates onto per-symbol flags. A predicate with no faithful counterpart (a relation between two symbols, a disjunction, a bound on a composite expression) raises rather than being dropped: dropping it asks the oracle a weaker question and any divergence that follows is an artefact of the harness.

Methods

translate(expr: Any, *, assumptions: Any=None) → Any

Translate expr, honouring assumptions, or refuse.

Parameters

exprExpr or DerivedResult: The expression to translate.
assumptionsAssumptions, optional: Governing assumption context. When None, the ambient active_assumptions() context is used, so a check run inside with alkahest.context(assumptions=...) asks the oracle the same conditioned question the caller asked Alkahest.

Returns

object: A term in the oracle's language.

Raises

CrossCheckError: E-XCHECK-001 for an unknown node tag, an unmapped primitive, or an assumption with no faithful counterpart.

assumption_flags(assumptions: Any) → dict[str, dict[str, bool]]

Public view of the symbol-flag mapping derived from assumptions.

constant

crosscheck.FROZEN_CORPUS

FROZEN_CORPUS = (FrozenCase(id='integrate_polynomial', operation='integrate', build=_case_polynomial_antiderivative, expected='agree', expected_reason='invariant_holds', fou…

No docstring.

constant

crosscheck.FUNCTION_MAP

FUNCTION_MAP = {'abs': 'Abs', 'acos': 'acos', 'acosh': 'acosh', 'arg': 'arg', 'asin': 'asin', 'asinh': 'asinh', 'atan': 'atan', 'atan2': 'atan2', 'atanh': 'atanh', 'ceil': …

No docstring.

constant

crosscheck.NODE_TAGS

NODE_TAGS = frozenset({'symbol', 'integer', 'rational', 'float', 'add', 'mul', 'pow', 'func', 'piecewise', 'predicate', 'forall', 'exists', 'big_o', 'root_sum'})

No docstring.

constant

crosscheck.OPERATIONS

OPERATIONS = {'diff': Operation('diff', (1, 2, 3), None), 'integrate': Operation('integrate', (4, 1, 2, 3), 'antiderivative'), 'simplify': Operation('simplify', (4, 1, 2,…

No docstring.

constant

crosscheck.OUTCOMES

OUTCOMES = ('agree', 'diverge', 'incomparable', 'unavailable')

No docstring.

constant

crosscheck.PREDICATE_KINDS

PREDICATE_KINDS = frozenset({'lt', 'le', 'gt', 'ge', 'eq', 'ne', 'and', 'or', 'not', 'true', 'false'})

No docstring.

constant

crosscheck.REFUSED_FUNCTIONS

REFUSED_FUNCTIONS = {'zeta_prime': 'SymPy has no `zeta_prime` function: it spells the derivative `Derivative(zeta(s), s)`, an unevaluated form a name-for-name table cannot expre…

No docstring.

constant

crosscheck.RUNG_NAMES

RUNG_NAMES = {1: 'syntactic', 2: 'symbolic', 3: 'rigorous_numeric', 4: 'invariant'}

No docstring.

constant

crosscheck.SAMPLE_BOX

SAMPLE_BOX = (0.35, 2.65)

No docstring.

constant

crosscheck.SWEEP_OPERATIONS

SWEEP_OPERATIONS = ('diff', 'integrate', 'simplify')

No docstring.