API REFERENCE/omnibias-core

omnibias.core.proof.realization_replay

0.5.0rc1Release candidatePython >=3.10Apache-2.0

Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.

import omnibias.core.proof.realization_replay

Module contract & mathematical conventions

Finite rational replay whose source operands occur in the Lean proposition.

The architecture-to-coefficient compiler and analytic enclosure producers are outside this finite theorem. An expected source digest binds a replay to the caller's original claim; a re-sealed different source is a different claim.

Shared formulas do not imply universal floating-point identity. Verify dtype, shape, derivative-order support, and the stated numerical assumptions for the path you use.

Module source ↗Source revision 9a2d73df0573Running reference examples →

FUNCTION

generate_replay_obligation

omnibias.core.proof.realization_replay.generate_replay_obligationSource ↗

generate_replay_obligation(cert: Mapping[str, Any], *, mathlib: bool=False) -> str | None

Emit even a false, structurally valid claim so Lean rejects its arithmetic.

Only exact integers parsed by this module can enter generated source. Malformed, unsealed or operand-substituted payloads are refused beforehand.

Parameters

Name	Type & default	Contract
certpositional-or-keyword	Mapping[str, Any]Required	See the operation contract and implementation below.
mathlibkeyword-only	boolDefault: False	See the operation contract and implementation below.

Returnsstr | None

Executed regression · actual kernel build when toolchain available

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_actual_kernel_build_when_toolchain_available(certificate):
    from omnibias.core.proof.lean_check import check_certificate, lean_check_available

    if not lean_check_available():
        pytest.skip("Lean toolchain unavailable")
    assert check_certificate(certificate).verified

python -m pytest "packages/omnibias-core/tests/proof/test_realization_replay.py::test_actual_kernel_build_when_toolchain_available[certificate0]" -q

Regression example · generic algebra replay is exact and emits both registers

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_generic_algebra_replay_is_exact_and_emits_both_registers(certificate):
    assert verify_replay_certificate(certificate)
    assert "decide +kernel" in generate_replay_obligation(certificate)
    assert "OmnibiasAnalytic.RealizationAlgebra" in generate_replay_obligation(
        certificate, mathlib=True
    )

python -m pytest packages/omnibias-core/tests/proof/test_realization_algebra_replay.py -k test_generic_algebra_replay_is_exact_and_emits_both_registers -q

Read the implementation

def generate_replay_obligation(cert: Mapping[str, Any], *, mathlib: bool = False) -> str | None:
    """Emit even a false, structurally valid claim so Lean rejects its arithmetic.

    Only exact integers parsed by this module can enter generated source.
    Malformed, unsealed or operand-substituted payloads are refused beforehand.
    """
    try:
        p = _payload(cert, None)
        from omnibias.core.proof.realization_algebra_replay import (
            ADVANCED_KINDS,
            generate_algebra_obligation,
        )

        if p["kind"] in ADVANCED_KINDS:
            return generate_algebra_obligation(cert, mathlib=mathlib)
        namespace = "OmnibiasAnalytic" if mathlib else "Omnibias"
        body: str
        if p["kind"] == "krawczyk_replay":
            s = p["source"]
            center = tuple(_fraction(x) for x in s["center"])
            if not center or type(s["require_contraction"]) is not bool:
                return None
            c_lit = _list([_literal(x) for x in center])
            g_lit = _list([_iv_literal(_decode_iv(x)) for x in s["gradient"]])
            h_lit = _list(
                [_list([_iv_literal(_decode_iv(x)) for x in row]) for row in s["hessian"]]
            )
            r_lit = _matrix_literal(_matrix(s["preconditioner"]))
            b_lit = _list([_iv_literal(_decode_iv(x)) for x in s["box"]])
            body = (
                f"def center : List Rat := {c_lit}\ndef gradient : List RI := {g_lit}\n"
                f"def hessian : RIMatrix := {h_lit}\ndef R : Matrix := {r_lit}\ndef box : List RI := {b_lit}\n"
                "theorem obligation : krawczykDataValid center gradient hessian R box = true ∧ "
                f"determinant {len(center)} R ≠ 0 ∧ "
                "strictIncluded (krawczykImage center gradient hessian R box) box = true"
            )
            if s["require_contraction"]:
                body += f" ∧ rowContraction (krawczykResidual hessian R {len(center)}) = true"
            if s.get("stationary_box") is not None:
                root_box_literal = _list([_iv_literal(_decode_iv(x)) for x in s["stationary_box"]])
                body += f" ∧ included (krawczykImage center gradient hessian R box) {root_box_literal} = true"
            body += " := by decide +kernel\n"
        elif p["kind"] == "interval_ldlt":
            intervals = [[_decode_iv(x) for x in row] for row in p["source"]]
            if not intervals:
                return None
            literal = _list([_list([_iv_literal(x) for x in row]) for row in intervals])
            body = (
                f"def A : RIMatrix := {literal}\ntheorem obligation : "
                f"validSymmetric A {len(intervals)} = true ∧ positivePivots {len(intervals)} A = true := by decide +kernel\n"
            )
        elif p["kind"] == "strict_box_inclusion":
            inner = _list([_iv_literal(_decode_iv(x)) for x in p["source"]["inner"]])
            outer = _list([_iv_literal(_decode_iv(x)) for x in p["source"]["outer"]])
            if not p["source"]["inner"]:
                return None
            body = (
                f"theorem obligation : strictIncluded {inner} {outer} = true := by decide +kernel\n"
            )
        elif p["kind"] == "interval_error_budget":
            error = _iv_literal(_decode_iv(p["source"]["error"]))
            budget = _literal(_fraction(p["source"]["budget"]))
            body = (
                f"theorem obligation : errorBudget {error} {budget} = true := by decide +kernel\n"
            )
        elif p["kind"] == "matrix_rank":
            a, b, c = _matrix(p["source"]), _matrix(p["left"]), _matrix(p["right"])
            rows, cols, r = _indices(p["minor_rows"]), _indices(p["minor_cols"]), p["rank"]
            if not a or not a[0] or type(r) is not int or r < 0 or r > min(len(a), len(a[0])):
                return None
            if len(rows) != r or len(cols) != r or len(set(rows)) != r or len(set(cols)) != r:
                return None
            if any(i >= len(a) for i in rows) or any(j >= len(a[0]) for j in cols):
                return None
            ri, ci = _list([str(i) for i in rows]), _list([str(i) for i in cols])
            value = _literal(_fraction(p["minor_value"]))
            body = (
                f"def A : Matrix := {_matrix_literal(a)}\ndef B : Matrix := {_matrix_literal(b)}\n"
                f"def C : Matrix := {_matrix_literal(c)}\n"
                f"theorem obligation : shape A {len(a)} {len(a[0])} = true ∧ "
                f"shape B {len(a)} {r} = true ∧ shape C {r} {len(a[0])} = true ∧ "
                f"A = multiply B C {len(a[0])} ∧ "
                f"determinant {r} (minor A {ri} {ci}) = {value} ∧ {value} ≠ 0 := by decide +kernel\n"
            )
        elif p["kind"] in ("polynomial_evaluation", "polynomial_inequality"):
            polys = tuple(_polynomial(f) for f in p["source"])
            point = tuple(_fraction(x) for x in p["point"])
            if not polys or any(f.nvars != len(point) for f in polys):
                return None
            definitions = [f"def point : List Rat := {_list([_literal(x) for x in point])}"]
            for i, f in enumerate(polys):
                terms = _list(
                    [f"({_list([str(k) for k in idx])}, {_literal(q)})" for idx, q in f.terms]
                )
                definitions.append(f"def p{i} : Polynomial := {terms}")
            claims: list[str] = []
            if p["kind"] == "polynomial_evaluation":
                expected = tuple(_fraction(x) for x in p["expected"])
                if len(polys) != len(expected):
                    return None
                claims = [f"evaluate p{i} point = {_literal(q)}" for i, q in enumerate(expected)]
            else:
                rels = p["relations"]
                if len(polys) != len(rels) or any(rel not in ("eq", "ge", "gt") for rel in rels):
                    return None
                symbols = {"eq": "=", "ge": "≥", "gt": ">"}
                claims = [f"evaluate p{i} point {symbols[rel]} 0" for i, rel in enumerate(rels)]
            body = (
                "\n".join(definitions)
                + "\ntheorem obligation : "
                + " ∧ ".join(claims)
                + " := by decide +kernel\n"
            )
        else:
            return None
        return (
            f"import {namespace}.RealizationReplay\nset_option maxRecDepth 100000\n"
            f"set_option maxHeartbeats 0\nopen {namespace}.RealizationReplay\n"
            f"namespace {namespace}.Generated\n{body}end {namespace}.Generated\n"
        )
    except (ValueError, TypeError, KeyError, IndexError, ZeroDivisionError, AlgebraBudgetExceeded):
        return None

FUNCTION

interval_error_budget_certificate

omnibias.core.proof.realization_replay.interval_error_budget_certificateSource ↗

interval_error_budget_certificate(error: Sequence[Rational], budget: Rational) -> Cert

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

Parameters

Name	Type & default	Contract
errorpositional-or-keyword	Sequence[Rational]Required	See the operation contract and implementation below.
budgetpositional-or-keyword	RationalRequired	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When bound < 0 or iv[0] < -bound or iv[1] > bound, raises ValueError('error exceeds budget').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · resealed rank factor substitution cannot borrow original minor

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_resealed_rank_factor_substitution_cannot_borrow_original_minor():
    certificate = _examples()[2]
    false = deepcopy(certificate)
    false["payload"]["left"][0][0] = [100, 1]
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_replay.py::test_resealed_rank_factor_substitution_cannot_borrow_original_minor" -q

Regression example · reject malformed or naked pivot inputs

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_reject_malformed_or_naked_pivot_inputs():
    false = deepcopy(_examples()[0])
    false["payload"]["point"][0] = [True, 1]
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is None
    with pytest.raises(ValueError):
        strict_box_inclusion_certificate([(0, 1)], [(0, 2)])
    with pytest.raises(ValueError):
        interval_error_budget_certificate((-2, 1), 1)

python -m pytest packages/omnibias-core/tests/proof/test_realization_replay.py -k test_reject_malformed_or_naked_pivot_inputs -q

Read the implementation

def interval_error_budget_certificate(error: Sequence[Rational], budget: Rational) -> Cert:
    iv, bound = _interval(error), rational(budget)
    if bound < 0 or iv[0] < -bound or iv[1] > bound:
        raise ValueError("error exceeds budget")
    return _seal("interval_error_budget", {"error": _iv_payload(iv), "budget": _q(bound)})

Related APIsomnibias.core.realization.polynomial.rational↗

FUNCTION

interval_ldlt_replay_certificate

omnibias.core.proof.realization_replay.interval_ldlt_replay_certificateSource ↗

interval_ldlt_replay_certificate(matrix: Sequence[Sequence[Sequence[Rational]]]) -> Cert

Recompute positive rational interval Schur pivots from original operands.

The finite Lean theorem evaluates this arithmetic; real enclosure provenance and the general LDL positive-definiteness implication are upstream facts.

Parameters

Name	Type & default	Contract
matrixpositional-or-keyword	Sequence[Sequence[Sequence[Rational]]]Required	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When not _positive_pivots(a), raises ValueError('interval LDL did not prove strictly positive pivots').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · resealed rank factor substitution cannot borrow original minor

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_resealed_rank_factor_substitution_cannot_borrow_original_minor():
    certificate = _examples()[2]
    false = deepcopy(certificate)
    false["payload"]["left"][0][0] = [100, 1]
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_replay.py::test_resealed_rank_factor_substitution_cannot_borrow_original_minor" -q

Regression example · interval ldlt is bound to original matrix even when resealed

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_interval_ldlt_is_bound_to_original_matrix_even_when_resealed():
    certificate = _examples()[4]
    false = deepcopy(certificate)
    false["payload"]["source"][0][0] = [[-3, 1], [-2, 1]]
    false["payload"]["source_digest"] = source_digest(false["payload"]["source"])
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert not verify_replay_certificate(
        false, expected_source_digest=certificate["payload"]["source_digest"]
    )
    assert "positivePivots" in generate_replay_obligation(false)
    with pytest.raises(ValueError):
        interval_ldlt_replay_certificate([[(-3, -2), (0, 0)], [(0, 0), (2, 3)]])

python -m pytest packages/omnibias-core/tests/proof/test_realization_replay.py -k test_interval_ldlt_is_bound_to_original_matrix_even_when_resealed -q

Read the implementation

def interval_ldlt_replay_certificate(matrix: Sequence[Sequence[Sequence[Rational]]]) -> Cert:
    """Recompute positive rational interval Schur pivots from original operands.

    The finite Lean theorem evaluates this arithmetic; real enclosure provenance
    and the general LDL positive-definiteness implication are upstream facts.
    """
    a = [[_interval(x) for x in row] for row in matrix]
    if not _positive_pivots(a):
        raise ValueError("interval LDL did not prove strictly positive pivots")
    return _seal("interval_ldlt", [[_iv_payload(x) for x in row] for row in a])

FUNCTION

krawczyk_replay_certificate

omnibias.core.proof.realization_replay.krawczyk_replay_certificateSource ↗

krawczyk_replay_certificate(center: Sequence[Rational], gradient: Sequence[Sequence[Rational]], hessian: Sequence[Sequence[Sequence[Rational]]], preconditioner: Sequence[Sequence[Rational]], box: Sequence[Sequence[Rational]], *, require_contraction: bool=True, stationary_box: Sequence[Sequence[Rational]] | None=None) -> Cert

Replay K=X0-R*g+(I-R*H)(X-X0), strict inclusion and invertibility.

Gradient/Hessian enclosure provenance and differentiability are explicit analytic dependencies; Lean recomputes the complete finite interval image.

Parameters

Name	Type & default	Contract
centerpositional-or-keyword	Sequence[Rational]Required	See the operation contract and implementation below.
gradientpositional-or-keyword	Sequence[Sequence[Rational]]Required	See the operation contract and implementation below.
hessianpositional-or-keyword	Sequence[Sequence[Sequence[Rational]]]Required	See the operation contract and implementation below.
preconditionerpositional-or-keyword	Sequence[Sequence[Rational]]Required	See the operation contract and implementation below.
boxpositional-or-keyword	Sequence[Sequence[Rational]]Required	See the operation contract and implementation below.
require_contractionkeyword-only	boolDefault: True	See the operation contract and implementation below.
stationary_boxkeyword-only	Sequence[Sequence[Rational]] | NoneDefault: None	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When not determinant(r) or any((not b[0] < a[0] <= a[1] < b[1] for a, b in zip(image, bounds, strict=True))), raises ValueError('Krawczyk image is not strictly included or preconditioner is singular').
• When require_contraction and (not contraction), raises ValueError('Krawczyk row contraction was not proved').
• When root_box is not None and (len(root_box) != len(image) or any((not b[0] <= a[0] <= a[1] <= b[1] for a, b in zip(image, root_box, strict=True)))), raises ValueError('claimed stationary box does not contain the Krawczyk image').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · resealed rank factor substitution cannot borrow original minor

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_resealed_rank_factor_substitution_cannot_borrow_original_minor():
    certificate = _examples()[2]
    false = deepcopy(certificate)
    false["payload"]["left"][0][0] = [100, 1]
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_replay.py::test_resealed_rank_factor_substitution_cannot_borrow_original_minor" -q

Regression example · actual kernel build when toolchain available

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_actual_kernel_build_when_toolchain_available(certificate):
    from omnibias.core.proof.lean_check import check_certificate, lean_check_available

    if not lean_check_available():
        pytest.skip("Lean toolchain unavailable")
    assert check_certificate(certificate).verified

python -m pytest packages/omnibias-core/tests/proof/test_realization_replay.py -k test_actual_kernel_build_when_toolchain_available -q

Read the implementation

def krawczyk_replay_certificate(
    center: Sequence[Rational],
    gradient: Sequence[Sequence[Rational]],
    hessian: Sequence[Sequence[Sequence[Rational]]],
    preconditioner: Sequence[Sequence[Rational]],
    box: Sequence[Sequence[Rational]],
    *,
    require_contraction: bool = True,
    stationary_box: Sequence[Sequence[Rational]] | None = None,
) -> Cert:
    """Replay K=X0-R*g+(I-R*H)(X-X0), strict inclusion and invertibility.

    Gradient/Hessian enclosure provenance and differentiability are explicit
    analytic dependencies; Lean recomputes the complete finite interval image.
    """
    c = tuple(map(rational, center))
    g = tuple(map(_interval, gradient))
    h = tuple(tuple(map(_interval, row)) for row in hessian)
    r, bounds = matrix(preconditioner), tuple(map(_interval, box))
    image, contraction = _krawczyk(c, g, h, r, bounds)
    if not determinant(r) or any(
        not b[0] < a[0] <= a[1] < b[1] for a, b in zip(image, bounds, strict=True)
    ):
        raise ValueError("Krawczyk image is not strictly included or preconditioner is singular")
    if require_contraction and not contraction:
        raise ValueError("Krawczyk row contraction was not proved")
    root_box = None if stationary_box is None else tuple(map(_interval, stationary_box))
    if root_box is not None and (
        len(root_box) != len(image)
        or any(not b[0] <= a[0] <= a[1] <= b[1] for a, b in zip(image, root_box, strict=True))
    ):
        raise ValueError("claimed stationary box does not contain the Krawczyk image")
    return _seal(
        "krawczyk_replay",
        {
            "center": [_q(x) for x in c],
            "gradient": [_iv_payload(x) for x in g],
            "hessian": [[_iv_payload(x) for x in row] for row in h],
            "preconditioner": [[_q(x) for x in row] for row in r],
            "box": [_iv_payload(x) for x in bounds],
            "require_contraction": require_contraction,
            "stationary_box": None if root_box is None else [_iv_payload(x) for x in root_box],
        },
    )

Related APIsomnibias.core.realization.rank.determinant↗omnibias.core.realization.rank.matrix↗

FUNCTION

polynomial_evaluation_certificate

omnibias.core.proof.realization_replay.polynomial_evaluation_certificateSource ↗

polynomial_evaluation_certificate(polynomials: Sequence[SparsePolynomial], point: Sequence[Rational], expected: Sequence[Rational]) -> Cert

Bind explicit coefficient polynomials, rational parameters and readout.

Parameters

Name	Type & default	Contract
polynomialspositional-or-keyword	Sequence[SparsePolynomial]Required	See the operation contract and implementation below.
pointpositional-or-keyword	Sequence[Rational]Required	See the operation contract and implementation below.
expectedpositional-or-keyword	Sequence[Rational]Required	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When not polynomials or len(polynomials) != len(target) or any((f.nvars != len(p) for f in polynomials)), raises ValueError('polynomial replay dimensions differ').
• When tuple((f.evaluate(p) for f in polynomials)) != target, raises ValueError('polynomial evaluation does not equal target').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · resealed rank factor substitution cannot borrow original minor

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_resealed_rank_factor_substitution_cannot_borrow_original_minor():
    certificate = _examples()[2]
    false = deepcopy(certificate)
    false["payload"]["left"][0][0] = [100, 1]
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_replay.py::test_resealed_rank_factor_substitution_cannot_borrow_original_minor" -q

Read the implementation

def polynomial_evaluation_certificate(
    polynomials: Sequence[SparsePolynomial],
    point: Sequence[Rational],
    expected: Sequence[Rational],
) -> Cert:
    """Bind explicit coefficient polynomials, rational parameters and readout."""
    p = tuple(rational(x) for x in point)
    target = tuple(rational(x) for x in expected)
    if (
        not polynomials
        or len(polynomials) != len(target)
        or any(f.nvars != len(p) for f in polynomials)
    ):
        raise ValueError("polynomial replay dimensions differ")
    if tuple(f.evaluate(p) for f in polynomials) != target:
        raise ValueError("polynomial evaluation does not equal target")
    return _seal(
        "polynomial_evaluation",
        [f.to_payload() for f in polynomials],
        point=[_q(x) for x in p],
        expected=[_q(x) for x in target],
    )

Related APIsomnibias.core.realization.polynomial.rational↗

FUNCTION

polynomial_inequality_certificate

omnibias.core.proof.realization_replay.polynomial_inequality_certificateSource ↗

polynomial_inequality_certificate(polynomials: Sequence[SparsePolynomial], point: Sequence[Rational], relations: Sequence[Relation]) -> Cert

Prove explicit rational expressions are zero/nonnegative/positive.

Parameters

Name	Type & default	Contract
polynomialspositional-or-keyword	Sequence[SparsePolynomial]Required	See the operation contract and implementation below.
pointpositional-or-keyword	Sequence[Rational]Required	See the operation contract and implementation below.
relationspositional-or-keyword	Sequence[Relation]Required	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When not polynomials or len(polynomials) != len(relations) or any((f.nvars != len(p) for f in polynomials)), raises ValueError('polynomial inequality dimensions differ').
• When any((rel not in ('eq', 'ge', 'gt') for rel in relations)), raises ValueError('unknown relation').
• When not (value == 0 if rel == 'eq' else value >= 0 if rel == 'ge' else value > 0), raises ValueError('false polynomial inequality').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · resealed rank factor substitution cannot borrow original minor

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_resealed_rank_factor_substitution_cannot_borrow_original_minor():
    certificate = _examples()[2]
    false = deepcopy(certificate)
    false["payload"]["left"][0][0] = [100, 1]
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_replay.py::test_resealed_rank_factor_substitution_cannot_borrow_original_minor" -q

Read the implementation

def polynomial_inequality_certificate(
    polynomials: Sequence[SparsePolynomial],
    point: Sequence[Rational],
    relations: Sequence[Relation],
) -> Cert:
    """Prove explicit rational expressions are zero/nonnegative/positive."""
    p = tuple(rational(x) for x in point)
    if (
        not polynomials
        or len(polynomials) != len(relations)
        or any(f.nvars != len(p) for f in polynomials)
    ):
        raise ValueError("polynomial inequality dimensions differ")
    if any(rel not in ("eq", "ge", "gt") for rel in relations):
        raise ValueError("unknown relation")
    for f, rel in zip(polynomials, relations, strict=True):
        value = f.evaluate(p)
        if not (value == 0 if rel == "eq" else value >= 0 if rel == "ge" else value > 0):
            raise ValueError("false polynomial inequality")
    return _seal(
        "polynomial_inequality",
        [f.to_payload() for f in polynomials],
        point=[_q(x) for x in p],
        relations=list(relations),
    )

Related APIsomnibias.core.realization.polynomial.rational↗

FUNCTION

rank_replay_certificate

omnibias.core.proof.realization_replay.rank_replay_certificateSource ↗

rank_replay_certificate(witness: ExactRankWitness) -> Cert

Prove A=B C and a recomputed nonzero source minor, with full operands.

These finite facts support the standard rank sandwich; the emitted theorem itself asserts the factorization and minor, not an abstract rank theorem.

Parameters

Name	Type & default	Contract
witnesspositional-or-keyword	ExactRankWitnessRequired	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When not witness.verify(), raises ValueError('invalid rank witness').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · resealed rank factor substitution cannot borrow original minor

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_resealed_rank_factor_substitution_cannot_borrow_original_minor():
    certificate = _examples()[2]
    false = deepcopy(certificate)
    false["payload"]["left"][0][0] = [100, 1]
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_replay.py::test_resealed_rank_factor_substitution_cannot_borrow_original_minor" -q

Read the implementation

def rank_replay_certificate(witness: ExactRankWitness) -> Cert:
    """Prove A=B C and a recomputed nonzero source minor, with full operands.

    These finite facts support the standard rank sandwich; the emitted theorem
    itself asserts the factorization and minor, not an abstract rank theorem.
    """
    if not witness.verify():
        raise ValueError("invalid rank witness")
    return _seal(
        "matrix_rank",
        [[_q(x) for x in row] for row in witness.source],
        rank=witness.rank,
        left=[[_q(x) for x in row] for row in witness.left],
        right=[[_q(x) for x in row] for row in witness.right],
        minor_rows=list(witness.minor_rows),
        minor_cols=list(witness.minor_cols),
        minor_value=_q(witness.minor_value),
    )

FUNCTION

source_digest

omnibias.core.proof.realization_replay.source_digestSource ↗

source_digest(source: object) -> str

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

Parameters

Name	Type & default	Contract
sourcepositional-or-keyword	objectRequired	See the operation contract and implementation below.

Returnsstr

Executed regression · actual kernel build when toolchain available

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_actual_kernel_build_when_toolchain_available(certificate):
    from omnibias.core.proof.lean_check import check_certificate, lean_check_available

    if not lean_check_available():
        pytest.skip("Lean toolchain unavailable")
    assert check_certificate(certificate).verified

python -m pytest "packages/omnibias-core/tests/proof/test_realization_replay.py::test_actual_kernel_build_when_toolchain_available[certificate0]" -q

Regression example · resealed arithmetic tampering is not hidden by source seal

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_resealed_arithmetic_tampering_is_not_hidden_by_source_seal(index):
    false = deepcopy(_examples()[index])
    p, s = false["payload"], false["payload"]["source"]
    if index <= 1:
        s["chain"][1][0] = [999, 1]
    elif index == 2:
        p["quotients"][0] = [[999, 1]]
    elif index == 3:
        s["parameters"][0] = [[-1, [1, 1]]]
    else:
        p["tree"]["midpoint"] = [2, 1]
    p["source_digest"] = source_digest(s)
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest packages/omnibias-core/tests/proof/test_realization_algebra_replay.py -k test_resealed_arithmetic_tampering_is_not_hidden_by_source_seal -q

Read the implementation

def source_digest(source: object) -> str:
    return hashlib.sha256(canonical_json({"source": source}).encode()).hexdigest()

Related APIsomnibias.core.proof.canonical_json↗

FUNCTION

strict_box_inclusion_certificate

omnibias.core.proof.realization_replay.strict_box_inclusion_certificateSource ↗

strict_box_inclusion_certificate(inner: Sequence[Sequence[Rational]], outer: Sequence[Sequence[Rational]]) -> Cert

The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.

Parameters

Name	Type & default	Contract
innerpositional-or-keyword	Sequence[Sequence[Rational]]Required	See the operation contract and implementation below.
outerpositional-or-keyword	Sequence[Sequence[Rational]]Required	See the operation contract and implementation below.

ReturnsCert

Explicit validation & failure cases

• When not a or len(a) != len(b) or any((not y[0] < x[0] <= x[1] < y[1] for x, y in zip(a, b, strict=True))), raises ValueError('box is not strictly included').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · resealed rank factor substitution cannot borrow original minor

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_resealed_rank_factor_substitution_cannot_borrow_original_minor():
    certificate = _examples()[2]
    false = deepcopy(certificate)
    false["payload"]["left"][0][0] = [100, 1]
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest "packages/omnibias-core/tests/proof/test_realization_replay.py::test_resealed_rank_factor_substitution_cannot_borrow_original_minor" -q

Regression example · reject malformed or naked pivot inputs

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_reject_malformed_or_naked_pivot_inputs():
    false = deepcopy(_examples()[0])
    false["payload"]["point"][0] = [True, 1]
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is None
    with pytest.raises(ValueError):
        strict_box_inclusion_certificate([(0, 1)], [(0, 2)])
    with pytest.raises(ValueError):
        interval_error_budget_certificate((-2, 1), 1)

python -m pytest packages/omnibias-core/tests/proof/test_realization_replay.py -k test_reject_malformed_or_naked_pivot_inputs -q

Read the implementation

def strict_box_inclusion_certificate(
    inner: Sequence[Sequence[Rational]], outer: Sequence[Sequence[Rational]]
) -> Cert:
    a, b = tuple(map(_interval, inner)), tuple(map(_interval, outer))
    if (
        not a
        or len(a) != len(b)
        or any(not (y[0] < x[0] <= x[1] < y[1]) for x, y in zip(a, b, strict=True))
    ):
        raise ValueError("box is not strictly included")
    return _seal(
        "strict_box_inclusion",
        {"inner": [_iv_payload(x) for x in a], "outer": [_iv_payload(x) for x in b]},
    )

FUNCTION

verify_replay_certificate

omnibias.core.proof.realization_replay.verify_replay_certificateSource ↗

verify_replay_certificate(cert: Mapping[str, Any], *, expected_source_digest: str | None=None) -> bool

Independently recompute a sealed finite replay in exact Python arithmetic.

Parameters

Name	Type & default	Contract
certpositional-or-keyword	Mapping[str, Any]Required	See the operation contract and implementation below.
expected_source_digestkeyword-only	str | NoneDefault: None	See the operation contract and implementation below.

Returnsbool

Executed regression · generic algebra replay is exact and emits both registers

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_generic_algebra_replay_is_exact_and_emits_both_registers(certificate):
    assert verify_replay_certificate(certificate)
    assert "decide +kernel" in generate_replay_obligation(certificate)
    assert "OmnibiasAnalytic.RealizationAlgebra" in generate_replay_obligation(
        certificate, mathlib=True
    )

python -m pytest "packages/omnibias-core/tests/proof/test_realization_algebra_replay.py::test_generic_algebra_replay_is_exact_and_emits_both_registers[certificate0]" -q

Regression example · resealed rank factor substitution cannot borrow original minor

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_resealed_rank_factor_substitution_cannot_borrow_original_minor():
    certificate = _examples()[2]
    false = deepcopy(certificate)
    false["payload"]["left"][0][0] = [100, 1]
    false = seal_certificate(false)
    assert not verify_replay_certificate(false)
    assert generate_replay_obligation(false) is not None

python -m pytest packages/omnibias-core/tests/proof/test_realization_replay.py -k test_resealed_rank_factor_substitution_cannot_borrow_original_minor -q

Read the implementation

def verify_replay_certificate(
    cert: Mapping[str, Any], *, expected_source_digest: str | None = None
) -> bool:
    """Independently recompute a sealed finite replay in exact Python arithmetic."""
    try:
        p = _payload(cert, expected_source_digest)
        from omnibias.core.proof.realization_algebra_replay import (
            ADVANCED_KINDS,
            verify_algebra_replay,
        )

        if p["kind"] in ADVANCED_KINDS:
            return verify_algebra_replay(cert)
        if p["kind"] == "krawczyk_replay":
            s = p["source"]
            c = tuple(_fraction(x) for x in s["center"])
            g = tuple(_decode_iv(x) for x in s["gradient"])
            h = tuple(tuple(_decode_iv(x) for x in row) for row in s["hessian"])
            r = _matrix(s["preconditioner"])
            bounds = tuple(_decode_iv(x) for x in s["box"])
            image, contraction = _krawczyk(c, g, h, r, bounds)
            if s.get("stationary_box") is not None:
                root_box = tuple(_decode_iv(x) for x in s["stationary_box"])
                if len(root_box) != len(image) or any(
                    not b[0] <= a[0] <= a[1] <= b[1] for a, b in zip(image, root_box, strict=True)
                ):
                    return False
            return (
                type(s["require_contraction"]) is bool
                and bool(determinant(r))
                and all(b[0] < a[0] <= a[1] < b[1] for a, b in zip(image, bounds, strict=True))
                and (not s["require_contraction"] or contraction)
            )
        if p["kind"] == "interval_ldlt":
            return _positive_pivots([[_decode_iv(x) for x in row] for row in p["source"]])
        if p["kind"] == "strict_box_inclusion":
            a = tuple(_decode_iv(x) for x in p["source"]["inner"])
            b = tuple(_decode_iv(x) for x in p["source"]["outer"])
            return (
                bool(a)
                and len(a) == len(b)
                and all(y[0] < x[0] <= x[1] < y[1] for x, y in zip(a, b, strict=True))
            )
        if p["kind"] == "interval_error_budget":
            lo, hi = _decode_iv(p["source"]["error"])
            bound = _fraction(p["source"]["budget"])
            return bound >= 0 and -bound <= lo <= hi <= bound
        if p["kind"] == "matrix_rank":
            if type(p["rank"]) is not int:
                return False
            return ExactRankWitness(
                _matrix(p["source"]),
                p["rank"],
                _matrix(p["left"]),
                _matrix(p["right"]),
                _indices(p["minor_rows"]),
                _indices(p["minor_cols"]),
                _fraction(p["minor_value"]),
            ).verify()
        polys = tuple(_polynomial(f) for f in p["source"])
        point = tuple(_fraction(x) for x in p["point"])
        values = tuple(f.evaluate(point) for f in polys)
        if p["kind"] == "polynomial_evaluation":
            return values == tuple(_fraction(x) for x in p["expected"])
        if p["kind"] == "polynomial_inequality":
            rels = p["relations"]
            return len(values) == len(rels) and all(
                value == 0
                if rel == "eq"
                else value >= 0
                if rel == "ge"
                else value > 0
                if rel == "gt"
                else False
                for value, rel in zip(values, rels, strict=True)
            )
        return False
    except (ValueError, TypeError, KeyError, IndexError, ZeroDivisionError, AlgebraBudgetExceeded):
        return False

Related APIsomnibias.core.realization.ExactRankWitness↗omnibias.core.realization.rank.determinant↗

← Package overviewRunnable learning examples →