Skip to main content

omnibias.core.realization.witness

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.realization.witness
Module contract & mathematical conventions

Exact real realization and Laurent closure witnesses tied to a source map.

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.

CLASS

AlgebraicRealizationWitness​

omnibias.core.realization.AlgebraicRealizationWitnessSource ↗
class AlgebraicRealizationWitness

Dataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.

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

Parameters

NameType & defaultContract
source_fingerprintdataclass fieldstrRequiredSee the operation contract and implementation below.
fielddataclass fieldRealAlgebraicFieldRequiredSee the operation contract and implementation below.
parametersdataclass fieldtuple[AlgebraicNumber, ...]RequiredSee the operation contract and implementation below.
targetdataclass fieldtuple[Fraction, ...]RequiredSee the operation contract and implementation below.
Executed regression · random real binary networks are never excluded

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.

def test_random_real_binary_networks_are_never_excluded():
    rng = random.Random(802)
    for _ in range(16):
        a, b, c, d = [Q(rng.randrange(-3, 4)) for _ in range(4)]
        rows = []
        for _ in range(3):
            u, v = [Q(rng.randrange(-2, 3)) for _ in range(2)]
            rows.append([u * a * a + v * c * c, 2 * (u * a * b + v * c * d), u * b * b + v * d * d])
        report = classify_binary_quadratic(rows)
        assert report.status == "realizable" and report.witness.verify(report.source)
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_random_real_binary_networks_are_never_excluded" -q

Fields & methods

source_fingerprintfield
source_fingerprint: str

Declared str field on AlgebraicRealizationWitness. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
fieldfield
field: RealAlgebraicField

Declared RealAlgebraicField field on AlgebraicRealizationWitness. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
parametersfield
parameters: tuple[AlgebraicNumber, ...]

Declared tuple[AlgebraicNumber, ...] field on AlgebraicRealizationWitness. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
targetfield
target: tuple[Fraction, ...]

Declared tuple[Fraction, ...] field on AlgebraicRealizationWitness. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
__post_init__method
__post_init__(self) -> None

See the class contract above and the exact method implementation below.

Returns: None

Executed regression · random real binary networks are never excluded

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.

def test_random_real_binary_networks_are_never_excluded():
    rng = random.Random(802)
    for _ in range(16):
        a, b, c, d = [Q(rng.randrange(-3, 4)) for _ in range(4)]
        rows = []
        for _ in range(3):
            u, v = [Q(rng.randrange(-2, 3)) for _ in range(2)]
            rows.append([u * a * a + v * c * c, 2 * (u * a * b + v * c * d), u * b * b + v * d * d])
        report = classify_binary_quadratic(rows)
        assert report.status == "realizable" and report.witness.verify(report.source)
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_random_real_binary_networks_are_never_excluded" -q
Method implementation
    def __post_init__(self) -> None:
        object.__setattr__(self, "target", tuple(map(rational, self.target)))
View source ↗
to_payloadmethod
to_payload(self) -> dict[str, object]

See the class contract above and the exact method implementation below.

Returns: dict[str, object]

Executed regression · portable rational algebraic and closure witnesses bind source

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.

def test_portable_rational_algebraic_and_closure_witnesses_bind_source():
    import json

    for report in (
        classify_linear([[1, 2], [0, 1]], (2,)),
        classify_binary_quadratic([[1, 0, 2], [0, 1, 0]]),
        classify_binary_quadratic([[1, 0, 0], [0, 1, 0]]),
    ):
        witness = report.witness or report.closure_path
        payload = json.loads(json.dumps(witness.to_payload()))
        assert witness_from_payload(payload, report.source).verify(report.source)
        payload["target"][0] = [100, 1]
        with pytest.raises(ValueError):
            witness_from_payload(payload, report.source)
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_portable_rational_algebraic_and_closure_witnesses_bind_source" -q
Method implementation
    def to_payload(self) -> dict[str, object]:
        return {
            "kind": "algebraic_realization",
            "source_fingerprint": self.source_fingerprint,
            "primitive": [_q(rational(x)) for x in self.field.polynomial],
            "isolating_interval": [_q(rational(self.field.lo)), _q(rational(self.field.hi))],
            "parameters": [[_q(x) for x in p.coefficients] for p in self.parameters],
            "target": [_q(x) for x in self.target],
        }
View source ↗
verifymethod
verify(self, source: PolynomialRealizationMap) -> bool

See the class contract above and the exact method implementation below.

Parameters

NameType & defaultContract
sourcepositional-or-keywordPolynomialRealizationMapRequiredSee the operation contract and implementation below.

Returns: bool

Method implementation
    def verify(self, source: PolynomialRealizationMap) -> bool:
        if (
            self.source_fingerprint != source.fingerprint
            or len(self.target) != len(source.polynomials)
            or len(self.parameters) != source.spec.n_params
            or any(p.field != self.field for p in self.parameters)
        ):
            return False
        return all(
            (algebraic_evaluate(p, self.parameters, self.field) - target).is_zero()
            for p, target in zip(source.polynomials, self.target, strict=True)
        )
View source ↗
Read the implementation
class AlgebraicRealizationWitness:
    source_fingerprint: str
    field: RealAlgebraicField
    parameters: tuple[AlgebraicNumber, ...]
    target: tuple[Fraction, ...]

    def __post_init__(self) -> None:
        object.__setattr__(self, "target", tuple(map(rational, self.target)))

    def to_payload(self) -> dict[str, object]:
        return {
            "kind": "algebraic_realization",
            "source_fingerprint": self.source_fingerprint,
            "primitive": [_q(rational(x)) for x in self.field.polynomial],
            "isolating_interval": [_q(rational(self.field.lo)), _q(rational(self.field.hi))],
            "parameters": [[_q(x) for x in p.coefficients] for p in self.parameters],
            "target": [_q(x) for x in self.target],
        }

    def verify(self, source: PolynomialRealizationMap) -> bool:
        if (
            self.source_fingerprint != source.fingerprint
            or len(self.target) != len(source.polynomials)
            or len(self.parameters) != source.spec.n_params
            or any(p.field != self.field for p in self.parameters)
        ):
            return False
        return all(
            (algebraic_evaluate(p, self.parameters, self.field) - target).is_zero()
            for p, target in zip(source.polynomials, self.target, strict=True)
        )
Other public import paths
  • omnibias.core.realization.AlgebraicRealizationWitness
  • omnibias.core.realization.witness.AlgebraicRealizationWitness
CLASS

LaurentClosureWitness​

omnibias.core.realization.LaurentClosureWitnessSource ↗
class LaurentClosureWitness

Dataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.

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

Parameters

NameType & defaultContract
source_fingerprintdataclass fieldstrRequiredSee the operation contract and implementation below.
parametersdataclass fieldtuple[LaurentPolynomial, ...]RequiredSee the operation contract and implementation below.
targetdataclass fieldtuple[Fraction, ...]RequiredSee the operation contract and implementation below.
radiusdataclass fieldFractionDefault: Fraction(1)See the operation contract and implementation below.
Executed regression · resealed arithmetic tampering is not hidden by source seal

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.

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::test_resealed_arithmetic_tampering_is_not_hidden_by_source_seal[0]" -q

Fields & methods

source_fingerprintfield
source_fingerprint: str

Declared str field on LaurentClosureWitness. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
parametersfield
parameters: tuple[LaurentPolynomial, ...]

Declared tuple[LaurentPolynomial, ...] field on LaurentClosureWitness. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
targetfield
target: tuple[Fraction, ...]

Declared tuple[Fraction, ...] field on LaurentClosureWitness. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
radiusfield
radius: Fraction = Fraction(1)

Declared Fraction field on LaurentClosureWitness. Default expression: Fraction(1).

View source ↗
__post_init__method
__post_init__(self) -> None

See the class contract above and the exact method implementation below.

Returns: None

Executed regression · resealed arithmetic tampering is not hidden by source seal

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.

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::test_resealed_arithmetic_tampering_is_not_hidden_by_source_seal[0]" -q
Method implementation
    def __post_init__(self) -> None:
        object.__setattr__(self, "target", tuple(map(rational, self.target)))
        object.__setattr__(self, "radius", rational(self.radius))
View source ↗
to_payloadmethod
to_payload(self) -> dict[str, object]

See the class contract above and the exact method implementation below.

Returns: dict[str, object]

Executed regression · portable rational algebraic and closure witnesses bind source

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.

def test_portable_rational_algebraic_and_closure_witnesses_bind_source():
    import json

    for report in (
        classify_linear([[1, 2], [0, 1]], (2,)),
        classify_binary_quadratic([[1, 0, 2], [0, 1, 0]]),
        classify_binary_quadratic([[1, 0, 0], [0, 1, 0]]),
    ):
        witness = report.witness or report.closure_path
        payload = json.loads(json.dumps(witness.to_payload()))
        assert witness_from_payload(payload, report.source).verify(report.source)
        payload["target"][0] = [100, 1]
        with pytest.raises(ValueError):
            witness_from_payload(payload, report.source)
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_portable_rational_algebraic_and_closure_witnesses_bind_source" -q
Method implementation
    def to_payload(self) -> dict[str, object]:
        return {
            "kind": "laurent_closure",
            "source_fingerprint": self.source_fingerprint,
            "parameters": [[[k, _q(c)] for k, c in p.terms] for p in self.parameters],
            "target": [_q(x) for x in self.target],
            "radius": _q(self.radius),
        }
View source ↗
realized_pathmethod
realized_path(self, source: PolynomialRealizationMap) -> tuple[LaurentPolynomial, ...]

See the class contract above and the exact method implementation below.

Parameters

NameType & defaultContract
sourcepositional-or-keywordPolynomialRealizationMapRequiredSee the operation contract and implementation below.

Returns: tuple[LaurentPolynomial, ...]

Validation & failure cases
  • When source.fingerprint != self.source_fingerprint or len(self.parameters) != source.spec.n_params, raises ValueError('closure path is bound to a different source').
Method implementation
    def realized_path(self, source: PolynomialRealizationMap) -> tuple[LaurentPolynomial, ...]:
        if (
            source.fingerprint != self.source_fingerprint
            or len(self.parameters) != source.spec.n_params
        ):
            raise ValueError("closure path is bound to a different source")
        outputs = []
        for p in source.polynomials:
            value = LaurentPolynomial({})
            for idx, c in p.terms:
                term = LaurentPolynomial({0: c})
                for parameter, exponent in zip(self.parameters, idx, strict=True):
                    term = term * parameter**exponent
                value = value + term
            outputs.append(value)
        return tuple(outputs)
View source ↗
verifymethod
verify(self, source: PolynomialRealizationMap) -> bool

See the class contract above and the exact method implementation below.

Parameters

NameType & defaultContract
sourcepositional-or-keywordPolynomialRealizationMapRequiredSee the operation contract and implementation below.

Returns: bool

Executed regression · resealed arithmetic tampering is not hidden by source seal

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.

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::test_resealed_arithmetic_tampering_is_not_hidden_by_source_seal[0]" -q
Method implementation
    def verify(self, source: PolynomialRealizationMap) -> bool:
        if self.radius <= 0 or len(self.target) != len(source.polynomials):
            return False
        try:
            path = self.realized_path(source)
        except ValueError:
            return False
        return all(
            not any(k < 0 for k, _ in p.terms) and dict(p.terms).get(0, Fraction(0)) == t
            for p, t in zip(path, self.target, strict=True)
        )
View source ↗
coefficient_error_boundsmethod
coefficient_error_bounds(self, source: PolynomialRealizationMap, radius: Rational | None=None) -> tuple[Fraction, ...]

See the class contract above and the exact method implementation below.

Parameters

NameType & defaultContract
sourcepositional-or-keywordPolynomialRealizationMapRequiredSee the operation contract and implementation below.
radiuspositional-or-keywordRational | NoneDefault: NoneSee the operation contract and implementation below.

Returns: tuple[Fraction, ...]

Validation & failure cases
  • When not self.verify(source) or not 0 < rho <= self.radius, raises ValueError('verified path and radius within the certified interval required').
Executed regression · resealed arithmetic tampering is not hidden by source seal

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.

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::test_resealed_arithmetic_tampering_is_not_hidden_by_source_seal[0]" -q
Method implementation
    def coefficient_error_bounds(
        self, source: PolynomialRealizationMap, radius: Rational | None = None
    ) -> tuple[Fraction, ...]:
        rho = self.radius if radius is None else rational(radius)
        if not self.verify(source) or not 0 < rho <= self.radius:
            raise ValueError("verified path and radius within the certified interval required")
        return tuple(
            sum((abs(c) * rho**k for k, c in p.terms if k > 0), Fraction(0))
            for p in self.realized_path(source)
        )
View source ↗
Read the implementation
class LaurentClosureWitness:
    source_fingerprint: str
    parameters: tuple[LaurentPolynomial, ...]
    target: tuple[Fraction, ...]
    radius: Fraction = Fraction(1)

    def __post_init__(self) -> None:
        object.__setattr__(self, "target", tuple(map(rational, self.target)))
        object.__setattr__(self, "radius", rational(self.radius))

    def to_payload(self) -> dict[str, object]:
        return {
            "kind": "laurent_closure",
            "source_fingerprint": self.source_fingerprint,
            "parameters": [[[k, _q(c)] for k, c in p.terms] for p in self.parameters],
            "target": [_q(x) for x in self.target],
            "radius": _q(self.radius),
        }

    def realized_path(self, source: PolynomialRealizationMap) -> tuple[LaurentPolynomial, ...]:
        if (
            source.fingerprint != self.source_fingerprint
            or len(self.parameters) != source.spec.n_params
        ):
            raise ValueError("closure path is bound to a different source")
        outputs = []
        for p in source.polynomials:
            value = LaurentPolynomial({})
            for idx, c in p.terms:
                term = LaurentPolynomial({0: c})
                for parameter, exponent in zip(self.parameters, idx, strict=True):
                    term = term * parameter**exponent
                value = value + term
            outputs.append(value)
        return tuple(outputs)

    def verify(self, source: PolynomialRealizationMap) -> bool:
        if self.radius <= 0 or len(self.target) != len(source.polynomials):
            return False
        try:
            path = self.realized_path(source)
        except ValueError:
            return False
        return all(
            not any(k < 0 for k, _ in p.terms) and dict(p.terms).get(0, Fraction(0)) == t
            for p, t in zip(path, self.target, strict=True)
        )

    def coefficient_error_bounds(
        self, source: PolynomialRealizationMap, radius: Rational | None = None
    ) -> tuple[Fraction, ...]:
        rho = self.radius if radius is None else rational(radius)
        if not self.verify(source) or not 0 < rho <= self.radius:
            raise ValueError("verified path and radius within the certified interval required")
        return tuple(
            sum((abs(c) * rho**k for k, c in p.terms if k > 0), Fraction(0))
            for p in self.realized_path(source)
        )
Other public import paths
  • omnibias.core.realization.LaurentClosureWitness
  • omnibias.core.realization.witness.LaurentClosureWitness
CLASS

LaurentPolynomial​

omnibias.core.realization.LaurentPolynomialSource ↗
class LaurentPolynomial

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

Parameters

NameType & defaultContract
termspositional-or-keywordMapping[int, Rational]RequiredSee the operation contract and implementation below.
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.

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[certificate3]" -q
Regression example · complete binary quadratic real vs closure

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.

def test_complete_binary_quadratic_real_vs_closure(c, status):
    report = classify_binary_quadratic(c)
    assert report.status == status
    if report.witness:
        assert report.witness.verify(report.source)
    if report.closure_path:
        path = report.closure_path
        assert path.verify(report.source)
        error = path.coefficient_error_bounds(report.source, Q(1, 10))
        theta = tuple(p.evaluate(Q(1, 10)) for p in path.parameters)
        actual = tuple(x for row in report.source.evaluate(theta) for x in row)
        assert all(abs(a - b) <= e for a, b, e in zip(actual, report.target, error, strict=True))
        assert not replace(path, target=tuple(x + 1 for x in path.target)).verify(report.source)
        divergent = replace(path, parameters=(LaurentPolynomial({-1: 1}), *path.parameters[1:]))
        assert not divergent.verify(report.source)
python -m pytest packages/omnibias-core/tests/test_realization_algebra.py -k test_complete_binary_quadratic_real_vs_closure -q

Fields & methods

termsfield
terms: tuple[tuple[int, Fraction], ...]

Declared tuple[tuple[int, Fraction], ...] field on LaurentPolynomial. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
__init__method
__init__(self, terms: Mapping[int, Rational]) -> None

See the class contract above and the exact method implementation below.

Parameters

NameType & defaultContract
termspositional-or-keywordMapping[int, Rational]RequiredSee the operation contract and implementation below.

Returns: None

Validation & failure cases
  • When any((isinstance(k, bool) or not isinstance(k, int) for k in terms)), raises ValueError('Laurent powers must be integers').
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.

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[certificate3]" -q
Method implementation
    def __init__(self, terms: Mapping[int, Rational]) -> None:
        if any(isinstance(k, bool) or not isinstance(k, int) for k in terms):
            raise ValueError("Laurent powers must be integers")
        object.__setattr__(
            self, "terms", tuple(sorted((k, rational(v)) for k, v in terms.items() if rational(v)))
        )
View source ↗
__add__method
__add__(self, other: LaurentPolynomial) -> LaurentPolynomial

See the class contract above and the exact method implementation below.

Parameters

NameType & defaultContract
otherpositional-or-keywordLaurentPolynomialRequiredSee the operation contract and implementation below.

Returns: LaurentPolynomial

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.

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[certificate3]" -q
Method implementation
    def __add__(self, other: LaurentPolynomial) -> LaurentPolynomial:
        result = dict(self.terms)
        for k, c in other.terms:
            result[k] = result.get(k, Fraction(0)) + c
        return LaurentPolynomial(result)
View source ↗
__mul__method
__mul__(self, other: LaurentPolynomial) -> LaurentPolynomial

See the class contract above and the exact method implementation below.

Parameters

NameType & defaultContract
otherpositional-or-keywordLaurentPolynomialRequiredSee the operation contract and implementation below.

Returns: LaurentPolynomial

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.

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[certificate3]" -q
Method implementation
    def __mul__(self, other: LaurentPolynomial) -> LaurentPolynomial:
        result: dict[int, Fraction] = {}
        for i, c in self.terms:
            for j, d in other.terms:
                result[i + j] = result.get(i + j, Fraction(0)) + c * d
        return LaurentPolynomial(result)
View source ↗
__pow__method
__pow__(self, exponent: int) -> LaurentPolynomial

See the class contract above and the exact method implementation below.

Parameters

NameType & defaultContract
exponentpositional-or-keywordintRequiredSee the operation contract and implementation below.

Returns: LaurentPolynomial

Validation & failure cases
  • When type(exponent) is not int or exponent < 0, raises ValueError('only nonnegative powers of a Laurent polynomial are supported').
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.

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[certificate3]" -q
Method implementation
    def __pow__(self, exponent: int) -> LaurentPolynomial:
        if type(exponent) is not int or exponent < 0:
            raise ValueError("only nonnegative powers of a Laurent polynomial are supported")
        result, base = LaurentPolynomial({0: 1}), self
        while exponent:
            if exponent & 1:
                result = result * base
            exponent //= 2
            if exponent:
                base = base * base
        return result
View source ↗
evaluatemethod
evaluate(self, epsilon: Rational) -> Fraction

See the class contract above and the exact method implementation below.

Parameters

NameType & defaultContract
epsilonpositional-or-keywordRationalRequiredSee the operation contract and implementation below.

Returns: Fraction

Validation & failure cases
  • When not e and any((k < 0 for k, _ in self.terms)), raises ZeroDivisionError('Laurent path is defined away from zero').
Executed regression · complete binary quadratic real vs closure

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.

def test_complete_binary_quadratic_real_vs_closure(c, status):
    report = classify_binary_quadratic(c)
    assert report.status == status
    if report.witness:
        assert report.witness.verify(report.source)
    if report.closure_path:
        path = report.closure_path
        assert path.verify(report.source)
        error = path.coefficient_error_bounds(report.source, Q(1, 10))
        theta = tuple(p.evaluate(Q(1, 10)) for p in path.parameters)
        actual = tuple(x for row in report.source.evaluate(theta) for x in row)
        assert all(abs(a - b) <= e for a, b, e in zip(actual, report.target, error, strict=True))
        assert not replace(path, target=tuple(x + 1 for x in path.target)).verify(report.source)
        divergent = replace(path, parameters=(LaurentPolynomial({-1: 1}), *path.parameters[1:]))
        assert not divergent.verify(report.source)
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_complete_binary_quadratic_real_vs_closure[c0-closure_only]" -q
Method implementation
    def evaluate(self, epsilon: Rational) -> Fraction:
        e = rational(epsilon)
        if not e and any(k < 0 for k, _ in self.terms):
            raise ZeroDivisionError("Laurent path is defined away from zero")
        return sum((v * e**k for k, v in self.terms), Fraction(0))
View source ↗
Read the implementation
class LaurentPolynomial:
    terms: tuple[tuple[int, Fraction], ...]

    def __init__(self, terms: Mapping[int, Rational]) -> None:
        if any(isinstance(k, bool) or not isinstance(k, int) for k in terms):
            raise ValueError("Laurent powers must be integers")
        object.__setattr__(
            self, "terms", tuple(sorted((k, rational(v)) for k, v in terms.items() if rational(v)))
        )

    def __add__(self, other: LaurentPolynomial) -> LaurentPolynomial:
        result = dict(self.terms)
        for k, c in other.terms:
            result[k] = result.get(k, Fraction(0)) + c
        return LaurentPolynomial(result)

    def __mul__(self, other: LaurentPolynomial) -> LaurentPolynomial:
        result: dict[int, Fraction] = {}
        for i, c in self.terms:
            for j, d in other.terms:
                result[i + j] = result.get(i + j, Fraction(0)) + c * d
        return LaurentPolynomial(result)

    def __pow__(self, exponent: int) -> LaurentPolynomial:
        if type(exponent) is not int or exponent < 0:
            raise ValueError("only nonnegative powers of a Laurent polynomial are supported")
        result, base = LaurentPolynomial({0: 1}), self
        while exponent:
            if exponent & 1:
                result = result * base
            exponent //= 2
            if exponent:
                base = base * base
        return result

    def evaluate(self, epsilon: Rational) -> Fraction:
        e = rational(epsilon)
        if not e and any(k < 0 for k, _ in self.terms):
            raise ZeroDivisionError("Laurent path is defined away from zero")
        return sum((v * e**k for k, v in self.terms), Fraction(0))
Other public import paths
  • omnibias.core.realization.LaurentPolynomial
  • omnibias.core.realization.witness.LaurentPolynomial
CLASS

RationalRealizationWitness​

omnibias.core.realization.RationalRealizationWitnessSource ↗
class RationalRealizationWitness

Dataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.

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

Parameters

NameType & defaultContract
source_fingerprintdataclass fieldstrRequiredSee the operation contract and implementation below.
parametersdataclass fieldtuple[Fraction, ...]RequiredSee the operation contract and implementation below.
targetdataclass fieldtuple[Fraction, ...]RequiredSee the operation contract and implementation below.
Executed regression · linear membership arbitrary depth

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.

def test_linear_membership_arbitrary_depth(hidden):
    report = classify_linear([[1, 2, 3], [-1, 2, 0]], hidden)
    assert report.status == "realizable" and report.witness.verify(report.source)
    assert not replace(report.witness, target=tuple(t + 1 for t in report.target)).verify(
        report.source
    )
    assert classify_linear([[1, 0], [0, 1]], (1, 3)).status == "excluded"
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_linear_membership_arbitrary_depth[hidden0]" -q

Fields & methods

source_fingerprintfield
source_fingerprint: str

Declared str field on RationalRealizationWitness. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
parametersfield
parameters: tuple[Fraction, ...]

Declared tuple[Fraction, ...] field on RationalRealizationWitness. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
targetfield
target: tuple[Fraction, ...]

Declared tuple[Fraction, ...] field on RationalRealizationWitness. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
__post_init__method
__post_init__(self) -> None

See the class contract above and the exact method implementation below.

Returns: None

Executed regression · linear membership arbitrary depth

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.

def test_linear_membership_arbitrary_depth(hidden):
    report = classify_linear([[1, 2, 3], [-1, 2, 0]], hidden)
    assert report.status == "realizable" and report.witness.verify(report.source)
    assert not replace(report.witness, target=tuple(t + 1 for t in report.target)).verify(
        report.source
    )
    assert classify_linear([[1, 0], [0, 1]], (1, 3)).status == "excluded"
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_linear_membership_arbitrary_depth[hidden0]" -q
Method implementation
    def __post_init__(self) -> None:
        object.__setattr__(self, "parameters", tuple(map(rational, self.parameters)))
        object.__setattr__(self, "target", tuple(map(rational, self.target)))
View source ↗
to_payloadmethod
to_payload(self) -> dict[str, object]

See the class contract above and the exact method implementation below.

Returns: dict[str, object]

Executed regression · portable rational algebraic and closure witnesses bind source

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.

def test_portable_rational_algebraic_and_closure_witnesses_bind_source():
    import json

    for report in (
        classify_linear([[1, 2], [0, 1]], (2,)),
        classify_binary_quadratic([[1, 0, 2], [0, 1, 0]]),
        classify_binary_quadratic([[1, 0, 0], [0, 1, 0]]),
    ):
        witness = report.witness or report.closure_path
        payload = json.loads(json.dumps(witness.to_payload()))
        assert witness_from_payload(payload, report.source).verify(report.source)
        payload["target"][0] = [100, 1]
        with pytest.raises(ValueError):
            witness_from_payload(payload, report.source)
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_portable_rational_algebraic_and_closure_witnesses_bind_source" -q
Method implementation
    def to_payload(self) -> dict[str, object]:
        return {
            "kind": "rational_realization",
            "source_fingerprint": self.source_fingerprint,
            "parameters": [_q(x) for x in self.parameters],
            "target": [_q(x) for x in self.target],
        }
View source ↗
verifymethod
verify(self, source: PolynomialRealizationMap) -> bool

See the class contract above and the exact method implementation below.

Parameters

NameType & defaultContract
sourcepositional-or-keywordPolynomialRealizationMapRequiredSee the operation contract and implementation below.

Returns: bool

Executed regression · linear membership arbitrary depth

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.

def test_linear_membership_arbitrary_depth(hidden):
    report = classify_linear([[1, 2, 3], [-1, 2, 0]], hidden)
    assert report.status == "realizable" and report.witness.verify(report.source)
    assert not replace(report.witness, target=tuple(t + 1 for t in report.target)).verify(
        report.source
    )
    assert classify_linear([[1, 0], [0, 1]], (1, 3)).status == "excluded"
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_linear_membership_arbitrary_depth[hidden0]" -q
Method implementation
    def verify(self, source: PolynomialRealizationMap) -> bool:
        return (
            self.source_fingerprint == source.fingerprint
            and len(self.target) == len(source.polynomials)
            and len(self.parameters) == source.spec.n_params
            and tuple(p.evaluate(self.parameters) for p in source.polynomials) == self.target
        )
View source ↗
Read the implementation
class RationalRealizationWitness:
    source_fingerprint: str
    parameters: tuple[Fraction, ...]
    target: tuple[Fraction, ...]

    def __post_init__(self) -> None:
        object.__setattr__(self, "parameters", tuple(map(rational, self.parameters)))
        object.__setattr__(self, "target", tuple(map(rational, self.target)))

    def to_payload(self) -> dict[str, object]:
        return {
            "kind": "rational_realization",
            "source_fingerprint": self.source_fingerprint,
            "parameters": [_q(x) for x in self.parameters],
            "target": [_q(x) for x in self.target],
        }

    def verify(self, source: PolynomialRealizationMap) -> bool:
        return (
            self.source_fingerprint == source.fingerprint
            and len(self.target) == len(source.polynomials)
            and len(self.parameters) == source.spec.n_params
            and tuple(p.evaluate(self.parameters) for p in source.polynomials) == self.target
        )
Other public import paths
  • omnibias.core.realization.RationalRealizationWitness
  • omnibias.core.realization.witness.RationalRealizationWitness
FUNCTION

algebraic_evaluate​

omnibias.core.realization.witness.algebraic_evaluateSource ↗
algebraic_evaluate(polynomial: SparsePolynomial, parameters: Sequence[AlgebraicNumber], field: RealAlgebraicField) -> AlgebraicNumber

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

Parameters

NameType & defaultContract
polynomialpositional-or-keywordSparsePolynomialRequiredSee the operation contract and implementation below.
parameterspositional-or-keywordSequence[AlgebraicNumber]RequiredSee the operation contract and implementation below.
fieldpositional-or-keywordRealAlgebraicFieldRequiredSee the operation contract and implementation below.
ReturnsAlgebraicNumber
Explicit validation & failure cases
  • When len(parameters) != polynomial.nvars or any((p.field != field for p in parameters)), raises ValueError('incompatible algebraic parameters').

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

Executed regression · random real binary networks are never excluded

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.

def test_random_real_binary_networks_are_never_excluded():
    rng = random.Random(802)
    for _ in range(16):
        a, b, c, d = [Q(rng.randrange(-3, 4)) for _ in range(4)]
        rows = []
        for _ in range(3):
            u, v = [Q(rng.randrange(-2, 3)) for _ in range(2)]
            rows.append([u * a * a + v * c * c, 2 * (u * a * b + v * c * d), u * b * b + v * d * d])
        report = classify_binary_quadratic(rows)
        assert report.status == "realizable" and report.witness.verify(report.source)
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_random_real_binary_networks_are_never_excluded" -q
Read the implementation
def algebraic_evaluate(
    polynomial: SparsePolynomial, parameters: Sequence[AlgebraicNumber], field: RealAlgebraicField
) -> AlgebraicNumber:
    if len(parameters) != polynomial.nvars or any(p.field != field for p in parameters):
        raise ValueError("incompatible algebraic parameters")
    result = field.constant(0)
    for idx, coeff in polynomial.terms:
        term = field.constant(coeff)
        for p, exponent in zip(parameters, idx, strict=True):
            term = term * p**exponent
        result = result + term
    return result
FUNCTION

rational_realization_witness​

omnibias.core.realization.rational_realization_witnessSource ↗
rational_realization_witness(source: PolynomialRealizationMap, parameters: Sequence[Rational], target: Sequence[Rational]) -> RationalRealizationWitness

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

Parameters

NameType & defaultContract
sourcepositional-or-keywordPolynomialRealizationMapRequiredSee the operation contract and implementation below.
parameterspositional-or-keywordSequence[Rational]RequiredSee the operation contract and implementation below.
targetpositional-or-keywordSequence[Rational]RequiredSee the operation contract and implementation below.
ReturnsRationalRealizationWitness
Explicit validation & failure cases
  • When not out.verify(source), raises ValueError("parameters do not realize this source map's target").

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

Executed regression · linear membership arbitrary depth

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.

def test_linear_membership_arbitrary_depth(hidden):
    report = classify_linear([[1, 2, 3], [-1, 2, 0]], hidden)
    assert report.status == "realizable" and report.witness.verify(report.source)
    assert not replace(report.witness, target=tuple(t + 1 for t in report.target)).verify(
        report.source
    )
    assert classify_linear([[1, 0], [0, 1]], (1, 3)).status == "excluded"
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_linear_membership_arbitrary_depth[hidden0]" -q
Read the implementation
def rational_realization_witness(
    source: PolynomialRealizationMap, parameters: Sequence[Rational], target: Sequence[Rational]
) -> RationalRealizationWitness:
    out = RationalRealizationWitness(
        source.fingerprint, tuple(map(rational, parameters)), tuple(map(rational, target))
    )
    if not out.verify(source):
        raise ValueError("parameters do not realize this source map's target")
    return out
Other public import paths
  • omnibias.core.realization.rational_realization_witness
  • omnibias.core.realization.witness.rational_realization_witness
FUNCTION

witness_from_payload​

omnibias.core.realization.witness.witness_from_payloadSource ↗
witness_from_payload(payload: Mapping[str, Any], source: PolynomialRealizationMap) -> RationalRealizationWitness | AlgebraicRealizationWitness | LaurentClosureWitness

Decode a portable exact witness and replay it against its original map.

Parameters

NameType & defaultContract
payloadpositional-or-keywordMapping[str, Any]RequiredSee the operation contract and implementation below.
sourcepositional-or-keywordPolynomialRealizationMapRequiredSee the operation contract and implementation below.
ReturnsRationalRealizationWitness | AlgebraicRealizationWitness | LaurentClosureWitness
Explicit validation & failure cases
  • When payload.get('source_fingerprint') != source.fingerprint, raises ValueError('witness source fingerprint differs').
  • When len(endpoints) != 2, raises ValueError('primitive root needs two endpoints').
  • When len(term) != 2 or type(term[0]) is not int or term[0] in terms, raises ValueError('malformed Laurent coefficient').
  • When not result.verify(source), raises ValueError('decoded witness failed exact source replay').

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

Executed regression · portable rational algebraic and closure witnesses bind source

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.

def test_portable_rational_algebraic_and_closure_witnesses_bind_source():
    import json

    for report in (
        classify_linear([[1, 2], [0, 1]], (2,)),
        classify_binary_quadratic([[1, 0, 2], [0, 1, 0]]),
        classify_binary_quadratic([[1, 0, 0], [0, 1, 0]]),
    ):
        witness = report.witness or report.closure_path
        payload = json.loads(json.dumps(witness.to_payload()))
        assert witness_from_payload(payload, report.source).verify(report.source)
        payload["target"][0] = [100, 1]
        with pytest.raises(ValueError):
            witness_from_payload(payload, report.source)
python -m pytest "packages/omnibias-core/tests/test_realization_algebra.py::test_portable_rational_algebraic_and_closure_witnesses_bind_source" -q
Read the implementation
def witness_from_payload(
    payload: Mapping[str, Any], source: PolynomialRealizationMap
) -> RationalRealizationWitness | AlgebraicRealizationWitness | LaurentClosureWitness:
    """Decode a portable exact witness and replay it against its original map."""
    if payload.get("source_fingerprint") != source.fingerprint:
        raise ValueError("witness source fingerprint differs")
    try:
        target = tuple(_decode_q(x) for x in payload["target"])
        result: RationalRealizationWitness | AlgebraicRealizationWitness | LaurentClosureWitness
        if payload["kind"] == "rational_realization":
            result = RationalRealizationWitness(
                source.fingerprint, tuple(_decode_q(x) for x in payload["parameters"]), target
            )
        elif payload["kind"] == "algebraic_realization":
            endpoints = payload["isolating_interval"]
            if len(endpoints) != 2:
                raise ValueError("primitive root needs two endpoints")
            field = RealAlgebraicField(
                tuple(_decode_q(x) for x in payload["primitive"]),
                _decode_q(endpoints[0]),
                _decode_q(endpoints[1]),
            )
            parameters = tuple(
                field.number(tuple(_decode_q(x) for x in row)) for row in payload["parameters"]
            )
            result = AlgebraicRealizationWitness(source.fingerprint, field, parameters, target)
        elif payload["kind"] == "laurent_closure":
            paths = []
            for row in payload["parameters"]:
                terms = {}
                for term in row:
                    if len(term) != 2 or type(term[0]) is not int or term[0] in terms:
                        raise ValueError("malformed Laurent coefficient")
                    terms[term[0]] = _decode_q(term[1])
                paths.append(LaurentPolynomial(terms))
            result = LaurentClosureWitness(
                source.fingerprint, tuple(paths), target, _decode_q(payload["radius"])
            )
        else:
            raise ValueError("unsupported exact witness kind")
        if not result.verify(source):
            raise ValueError("decoded witness failed exact source replay")
        return result
    except (TypeError, KeyError, IndexError) as exc:
        raise ValueError("malformed exact realization witness") from exc