Skip to main content
API REFERENCE/omnibias-core

omnibias.core.proof.certificate

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

Certificate format v1: a versioned, canonical, tamper-evident schema.

omnibias produces many independently checkable certificates (interval / Taylor -model enclosures, spectral gaps, blow-up witnesses). This module gives them a **single canonical on-disk form** so that they can be hashed, diffed, replayed, and handed to a Lean kernel for a *kernel-checked* theorem.

Design

  • **Bit-exact floats.** Every float is stored as its IEEE-754 hex() string, so a sealed certificate round-trips to the last bit on any platform -- essential when the number *is* a rigorous bound.
  • **Canonical JSON.** canonical_json sorts keys, uses compact separators, and tags any stray float with a {"__f64__": "0x..."} marker so the digest is independent of dict ordering and decimal formatting.
  • **Tamper-evident.** seal_certificate appends a sha256 digest over the canonical body; verify_certificate_digest recomputes it, so any mutation (a widened bound, a flipped flag) invalidates the certificate.

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 →
CONSTANT

CERTIFICATE_SCHEMA_VERSION​

omnibias.core.proof.CERTIFICATE_SCHEMA_VERSIONSource ↗
CERTIFICATE_SCHEMA_VERSION = '1.0'

The current certificate schema version.

Regression example · seal and verify digest

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_seal_and_verify_digest() -> None:
    cert = interval_certificate("x in [0,1]", Interval(0.0, 1.0))
    assert cert["schema_version"] == CERTIFICATE_SCHEMA_VERSION
    assert cert["digest"].startswith("sha256:")
    assert verify_certificate_digest(cert)
    assert schema_errors_v1(cert) == []
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_seal_and_verify_digest -q
Regression example · schema errors catch hand built designated payload on libm

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_schema_errors_catch_hand_built_designated_payload_on_libm() -> None:
    hand = seal_certificate(
        {
            "schema_version": CERTIFICATE_SCHEMA_VERSION,
            "claim": "hand-built conditional interval",
            "payload": {"type": "interval"},
            "honesty": {"unproven_claim": False},
            "meta": {TRANSCEND_BACKEND_KEY: "libm_fallback"},
        }
    )
    assert any("designated rigorous" in error for error in schema_errors_v1(hand))
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_schema_errors_catch_hand_built_designated_payload_on_libm -q
Read the implementation
CERTIFICATE_SCHEMA_VERSION = "1.0"
Other public import paths
  • omnibias.core.proof.CERTIFICATE_SCHEMA_VERSION
  • omnibias.core.proof.certificate.CERTIFICATE_SCHEMA_VERSION
CONSTANT

CONDITIONAL_TRANSCEND_BACKENDS​

omnibias.core.proof.certificate.CONDITIONAL_TRANSCEND_BACKENDSSource ↗
CONDITIONAL_TRANSCEND_BACKENDS = frozenset({'libm', BACKEND_LIBM_FALLBACK})

Backend stamps that mark *conditionally* rigorous transcendental enclosures. Includes the legacy "libm" alias so older sealed certificates / hand-built meta still trip the seal-time and schema gates.

Read the implementation
CONDITIONAL_TRANSCEND_BACKENDS = frozenset({"libm", BACKEND_LIBM_FALLBACK})
CONSTANT

Cert​

omnibias.core.proof.certificate.CertSource ↗
Cert = dict[str, Any]

This exported constant is defined by the expression above. Its exact value and annotation come from the pinned source; use it with the module contract.

Read the implementation
Cert = dict[str, Any]
CONSTANT

NO_TRANSCENDENTAL_BACKEND​

omnibias.core.proof.certificate.NO_TRANSCENDENTAL_BACKENDSource ↗
NO_TRANSCENDENTAL_BACKEND = 'not_used'

This exported constant is defined by the expression above. Its exact value and annotation come from the pinned source; use it with the module contract.

Regression example · pure rational interval does not acquire a libm stamp

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_pure_rational_interval_does_not_acquire_a_libm_stamp(
    monkeypatch: pytest.MonkeyPatch,
) -> None:
    """No evaluated transcendental is distinct from a conditional fallback."""
    from omnibias.core.verified import transcend

    monkeypatch.setattr(transcend, "_mpmath", lambda: None)
    transcend.clear_libm_fallback_used()
    cert = make_certificate(claim="rational only", payload={"type": "interval"})
    assert certificate_transcend_backend(cert) == NO_TRANSCENDENTAL_BACKEND
    assert certificate_is_unconditional(cert)
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_pure_rational_interval_does_not_acquire_a_libm_stamp -q
Read the implementation
NO_TRANSCENDENTAL_BACKEND = "not_used"
CONSTANT

RESERVED_HONESTY_KEYS​

omnibias.core.proof.certificate.RESERVED_HONESTY_KEYSSource ↗
RESERVED_HONESTY_KEYS = frozenset({THEOREM_PROVER_VERIFIED_KEY})

Honesty keys that producers may not supply. These are earned by the Lean kernel / ProofMachine, never asserted into a sealed certificate body. Supplying any of them raises ValueError.

Read the implementation
RESERVED_HONESTY_KEYS = frozenset({THEOREM_PROVER_VERIFIED_KEY})
CONSTANT

RIGOROUS_TRANSCENDENTAL_PAYLOAD_TYPES​

omnibias.core.proof.certificate.RIGOROUS_TRANSCENDENTAL_PAYLOAD_TYPESSource ↗
RIGOROUS_TRANSCENDENTAL_PAYLOAD_TYPES = frozenset({'interval', 'taylor_model', 'positive_definite', 'spectral gap', 'spectral_gap', 'pinn_aposteriori_error'})

Payload kinds that represent rigorous enclosures and must never be sealed with provenance from the conditionally-rigorous libm fallback. A certificate with no transcendental evaluation is stamped "not_used" and is allowed; this set refuses the fallback stamp itself, not rational interval algebra.

Regression example · designated payload refuses conditional transcendental stamp

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_designated_payload_refuses_conditional_transcendental_stamp(
    payload_type: str,
) -> None:
    with pytest.raises(RuntimeError, match="designated rigorous payload"):
        make_certificate(
            claim="conditionally rigorous",
            payload={"type": payload_type},
            meta={TRANSCEND_BACKEND_KEY: "libm_fallback"},
        )
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_designated_payload_refuses_conditional_transcendental_stamp -q
Read the implementation
RIGOROUS_TRANSCENDENTAL_PAYLOAD_TYPES = frozenset(
    {
        "interval",
        "taylor_model",
        "positive_definite",
        "spectral gap",
        "spectral_gap",
        "pinn_aposteriori_error",
    }
)
CONSTANT

SUPPORTED_SCHEMA_VERSIONS​

omnibias.core.proof.SUPPORTED_SCHEMA_VERSIONSSource ↗
SUPPORTED_SCHEMA_VERSIONS = frozenset({'1.0'})

Schema versions this module can validate / decode.

Read the implementation
SUPPORTED_SCHEMA_VERSIONS = frozenset({"1.0"})
Other public import paths
  • omnibias.core.proof.SUPPORTED_SCHEMA_VERSIONS
  • omnibias.core.proof.certificate.SUPPORTED_SCHEMA_VERSIONS
CONSTANT

THEOREM_PROVER_VERIFIED_KEY​

omnibias.core.proof.FORMAL_CLAIM_KEYSource ↗
THEOREM_PROVER_VERIFIED_KEY = 'theorem_prover_verified'

Honesty key earned **only** by a genuine Lean-kernel / ProofMachine pass. Producers must never supply it to make_certificate (or any other honesty entry point); the sealed body must never carry it.

Regression example · forgery error names the offending field

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_forgery_error_names_the_offending_field() -> None:
    (error,) = formal_claim_forgery_errors({FORMAL_CLAIM_KEY: True}, context="bundle.honesty")
    assert error.startswith(f"bundle.honesty.{FORMAL_CLAIM_KEY}")
python -m pytest packages/omnibias-core/tests/test_proof_machine.py -k test_forgery_error_names_the_offending_field -q
Regression example · honest artifact declares nothing and passes

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_honest_artifact_declares_nothing_and_passes() -> None:
    assert formal_claim_forgery_errors({FORMAL_CLAIM_KEY: False}) == []
    assert formal_claim_forgery_errors({}) == []
    assert formal_claim_forgery_errors(None) == []
python -m pytest packages/omnibias-core/tests/test_proof_machine.py -k test_honest_artifact_declares_nothing_and_passes -q
Read the implementation
THEOREM_PROVER_VERIFIED_KEY = "theorem_prover_verified"
Other public import paths
  • omnibias.core.proof.FORMAL_CLAIM_KEY
  • omnibias.core.proof.certificate.THEOREM_PROVER_VERIFIED_KEY
CONSTANT

TRANSCEND_BACKEND_KEY​

omnibias.core.proof.certificate.TRANSCEND_BACKEND_KEYSource ↗
TRANSCEND_BACKEND_KEY = 'transcend_backend'

meta key recording which transcendental backend was available when the enclosure was sealed (see omnibias.core.verified.transcend). Stamped automatically by make_certificate so the provenance can never be forgotten by an individual producer. Values are "mpmath" or "libm_fallback" when a transcendental enclosure was used, and "not_used" when no transcendental enclosure fed the certificate.

Regression example · designated payload refuses conditional transcendental stamp

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_designated_payload_refuses_conditional_transcendental_stamp(
    payload_type: str,
) -> None:
    with pytest.raises(RuntimeError, match="designated rigorous payload"):
        make_certificate(
            claim="conditionally rigorous",
            payload={"type": payload_type},
            meta={TRANSCEND_BACKEND_KEY: "libm_fallback"},
        )
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_designated_payload_refuses_conditional_transcendental_stamp -q
Regression example · caller supplied backend provenance is preserved

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_caller_supplied_backend_provenance_is_preserved() -> None:
    # Re-sealing a decoded certificate must keep the original machine's backend,
    # not silently acquire the re-sealing machine's.
    cert = make_certificate(
        claim="c", payload={"type": "interval"}, meta={TRANSCEND_BACKEND_KEY: "arb"}
    )
    assert certificate_transcend_backend(cert) == "arb"
    assert certificate_is_unconditional(cert)
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_caller_supplied_backend_provenance_is_preserved -q
Read the implementation
TRANSCEND_BACKEND_KEY = "transcend_backend"
CONSTANT

UNCONDITIONAL_CLAIM_KEY​

omnibias.core.proof.certificate.UNCONDITIONAL_CLAIM_KEYSource ↗
UNCONDITIONAL_CLAIM_KEY = 'unconditional_transcendentals'

honesty key by which a producer may assert that its enclosure rests on no unverified libm assumption. Asserting it while sealed on a conditional backend is refused by make_certificate (at seal time) and by func:schema_errors_v1 (on already-sealed / hand-built certificates).

Regression example · schema errors catch hand built unconditional on libm

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_schema_errors_catch_hand_built_unconditional_on_libm() -> None:
    # Already-sealed / hand-built certificates still fail schema validation.
    from omnibias.core.proof.certificate import seal_certificate

    hand = seal_certificate(
        {
            "schema_version": CERTIFICATE_SCHEMA_VERSION,
            "claim": "forged unconditional",
            "payload": {"type": "interval"},
            "honesty": {"unproven_claim": False, UNCONDITIONAL_CLAIM_KEY: True},
            "meta": {TRANSCEND_BACKEND_KEY: "libm_fallback"},
        }
    )
    errors = schema_errors_v1(hand)
    assert any(UNCONDITIONAL_CLAIM_KEY in e and "libm" in e for e in errors), errors
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_schema_errors_catch_hand_built_unconditional_on_libm -q
Regression example · certificate cannot silently use libm fallback

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_certificate_cannot_silently_use_libm_fallback(
    monkeypatch: pytest.MonkeyPatch,
) -> None:
    """Certificate path records libm_fallback and refuses unconditional sealing."""
    from omnibias.core.verified import transcend

    monkeypatch.setattr(transcend, "_mpmath", lambda: None)
    transcend.clear_libm_fallback_used()
    assert transcend.backend_name() == "libm_fallback"

    # Exploratory use is allowed and marks the sticky flag.
    enc = transcend.exp_iv(Interval.point(0.0))
    assert enc.contains(1.0)
    assert transcend.libm_fallback_used()

    # Designated rigorous payloads cannot merely record the conditional backend.
    with pytest.raises(RuntimeError, match="designated rigorous payload"):
        make_certificate(claim="exploratory", payload={"type": "interval"})

    # Unconditional / strict sealing cannot silently proceed on the fallback.
    with pytest.raises(RuntimeError):
        make_certificate(
            claim="must be rigorous",
            payload={"type": "interval"},
            honesty={"unproven_claim": False, UNCONDITIONAL_CLAIM_KEY: True},
        )
    prev = transcend.set_strict_backend(True)
    try:
        with pytest.raises(RuntimeError):
            make_certificate(claim="strict", payload={"type": "interval"})
    finally:
        transcend.set_strict_backend(prev)
        transcend.clear_libm_fallback_used()
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_certificate_cannot_silently_use_libm_fallback -q
Read the implementation
UNCONDITIONAL_CLAIM_KEY = "unconditional_transcendentals"
CONSTANT

UNCONDITIONAL_TRANSCEND_BACKENDS​

omnibias.core.proof.certificate.UNCONDITIONAL_TRANSCEND_BACKENDSSource ↗
UNCONDITIONAL_TRANSCEND_BACKENDS = frozenset({'arb', 'mpfr', 'mpmath'})

Transcendental backends whose enclosures are *unconditionally* rigorous. The stdlib libm_fallback path is deliberately absent: it is rigorous only *given* that the platform's math error stays inside the assumed ulp budget, which the language does not guarantee.

Regression example · unknown provenance is treated as conditional

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_unknown_provenance_is_treated_as_conditional() -> None:
    # A hand-built or pre-stamp certificate must never pass for rigorous.
    for cert in ({}, {"meta": {}}, {"meta": "not-a-mapping"}, {"meta": {TRANSCEND_BACKEND_KEY: 7}}):
        assert certificate_transcend_backend(cert) is None
        assert not certificate_is_unconditional(cert)
    assert not certificate_is_unconditional({"meta": {TRANSCEND_BACKEND_KEY: "libm"}})
    assert not certificate_is_unconditional(
        {"meta": {TRANSCEND_BACKEND_KEY: "libm_fallback"}}
    )
    for good in UNCONDITIONAL_TRANSCEND_BACKENDS:
        assert certificate_is_unconditional({"meta": {TRANSCEND_BACKEND_KEY: good}})
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_unknown_provenance_is_treated_as_conditional -q
Read the implementation
UNCONDITIONAL_TRANSCEND_BACKENDS = frozenset({"arb", "mpfr", "mpmath"})
FUNCTION

canonical_json​

omnibias.core.proof.canonical_jsonSource ↗
canonical_json(cert: Mapping[str, Any]) -> str

Deterministic JSON string of cert (sorted keys, hex-tagged floats).

Parameters

NameType & defaultContract
certpositional-or-keywordMapping[str, Any]RequiredSee the operation contract and implementation below.
Returnsstr
Executed regression · canonical json is order independent

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_canonical_json_is_order_independent() -> None:
    a = {"b": 1, "a": {"y": 2, "x": 3}}
    b = {"a": {"x": 3, "y": 2}, "b": 1}
    assert canonical_json(a) == canonical_json(b)
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_canonical_json_is_order_independent" -q
Read the implementation
def canonical_json(cert: Mapping[str, Any]) -> str:
    """Deterministic JSON string of ``cert`` (sorted keys, hex-tagged floats)."""
    return json.dumps(
        _canonicalize(dict(cert)),
        sort_keys=True,
        separators=(",", ":"),
        ensure_ascii=True,
    )
Other public import paths
  • omnibias.core.proof.canonical_json
  • omnibias.core.proof.certificate.canonical_json
FUNCTION

certificate_digest​

omnibias.core.proof.certificate_digestSource ↗
certificate_digest(cert: Mapping[str, Any]) -> str

"sha256:<hex>" over the canonical body (excluding any digest key).

Parameters

NameType & defaultContract
certpositional-or-keywordMapping[str, Any]RequiredSee the operation contract and implementation below.
Returnsstr
Executed regression · honesty defaults to no unproven claim

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_honesty_defaults_to_no_unproven_claim() -> None:
    cert = make_certificate(claim="benign", payload={"type": "interval"})
    assert cert["honesty"] == {"unproven_claim": False}
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_honesty_defaults_to_no_unproven_claim" -q
Regression example · digest is stable under reserialization

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_digest_is_stable_under_reserialization() -> None:
    tm = TaylorModel(0.0, 1.0, [Interval(2.0, 2.0), Interval(3.0, 3.0)], Interval(-0.1, 0.1))
    cert = taylor_model_certificate("f enclosure", tm)
    # Recomputing the digest from the body must reproduce the sealed digest.
    assert certificate_digest(cert) == cert["digest"]
    # Re-sealing is idempotent.
    assert seal_certificate(cert)["digest"] == cert["digest"]
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_digest_is_stable_under_reserialization -q
Read the implementation
def certificate_digest(cert: Mapping[str, Any]) -> str:
    """``"sha256:<hex>"`` over the canonical body (excluding any ``digest`` key)."""
    body = {k: v for k, v in cert.items() if k != "digest"}
    return "sha256:" + hashlib.sha256(canonical_json(body).encode("utf-8")).hexdigest()
Related APIsomnibias.core.proof.canonical_json↗
Other public import paths
  • omnibias.core.proof.certificate_digest
  • omnibias.core.proof.certificate.certificate_digest
FUNCTION

certificate_is_unconditional​

omnibias.core.proof.certificate.certificate_is_unconditionalSource ↗
certificate_is_unconditional(cert: Mapping[str, Any]) -> bool

True iff cert records a backend that needs no libm assumption.

An absent or unrecognised stamp answers False: soundness claims default to the weaker reading, so unknown provenance never passes for rigorous.

Parameters

NameType & defaultContract
certpositional-or-keywordMapping[str, Any]RequiredSee the operation contract and implementation below.
Returnsbool
Executed regression · caller supplied backend provenance is preserved

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_caller_supplied_backend_provenance_is_preserved() -> None:
    # Re-sealing a decoded certificate must keep the original machine's backend,
    # not silently acquire the re-sealing machine's.
    cert = make_certificate(
        claim="c", payload={"type": "interval"}, meta={TRANSCEND_BACKEND_KEY: "arb"}
    )
    assert certificate_transcend_backend(cert) == "arb"
    assert certificate_is_unconditional(cert)
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_caller_supplied_backend_provenance_is_preserved" -q
Regression example · pure rational interval does not acquire a libm stamp

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_pure_rational_interval_does_not_acquire_a_libm_stamp(
    monkeypatch: pytest.MonkeyPatch,
) -> None:
    """No evaluated transcendental is distinct from a conditional fallback."""
    from omnibias.core.verified import transcend

    monkeypatch.setattr(transcend, "_mpmath", lambda: None)
    transcend.clear_libm_fallback_used()
    cert = make_certificate(claim="rational only", payload={"type": "interval"})
    assert certificate_transcend_backend(cert) == NO_TRANSCENDENTAL_BACKEND
    assert certificate_is_unconditional(cert)
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_pure_rational_interval_does_not_acquire_a_libm_stamp -q
Read the implementation
def certificate_is_unconditional(cert: Mapping[str, Any]) -> bool:
    """``True`` iff ``cert`` records a backend that needs no libm assumption.

    An absent or unrecognised stamp answers ``False``: soundness claims default to
    the weaker reading, so unknown provenance never passes for rigorous.
    """
    return certificate_transcend_backend(cert) in (
        UNCONDITIONAL_TRANSCEND_BACKENDS | {NO_TRANSCENDENTAL_BACKEND}
    )
Related APIsomnibias.core.proof.certificate.certificate_transcend_backend↗
FUNCTION

certificate_transcend_backend​

omnibias.core.proof.certificate.certificate_transcend_backendSource ↗
certificate_transcend_backend(cert: Mapping[str, Any]) -> str | None

The backend recorded in cert's meta, or None when absent.

None means *unknown provenance* -- a certificate sealed before the stamp existed, or built by hand -- which callers must treat as conditional, not as a licence to assume the rigorous backend.

Parameters

NameType & defaultContract
certpositional-or-keywordMapping[str, Any]RequiredSee the operation contract and implementation below.
Returnsstr | None
Executed regression · seal and verify digest

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_seal_and_verify_digest() -> None:
    cert = interval_certificate("x in [0,1]", Interval(0.0, 1.0))
    assert cert["schema_version"] == CERTIFICATE_SCHEMA_VERSION
    assert cert["digest"].startswith("sha256:")
    assert verify_certificate_digest(cert)
    assert schema_errors_v1(cert) == []
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_seal_and_verify_digest" -q
Regression example · caller supplied backend provenance is preserved

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_caller_supplied_backend_provenance_is_preserved() -> None:
    # Re-sealing a decoded certificate must keep the original machine's backend,
    # not silently acquire the re-sealing machine's.
    cert = make_certificate(
        claim="c", payload={"type": "interval"}, meta={TRANSCEND_BACKEND_KEY: "arb"}
    )
    assert certificate_transcend_backend(cert) == "arb"
    assert certificate_is_unconditional(cert)
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_caller_supplied_backend_provenance_is_preserved -q
Read the implementation
def certificate_transcend_backend(cert: Mapping[str, Any]) -> str | None:
    """The backend recorded in ``cert``'s ``meta``, or ``None`` when absent.

    ``None`` means *unknown provenance* -- a certificate sealed before the stamp
    existed, or built by hand -- which callers must treat as conditional, not as
    a licence to assume the rigorous backend.
    """
    meta = cert.get("meta")
    if not isinstance(meta, Mapping):
        return None
    recorded = meta.get(TRANSCEND_BACKEND_KEY)
    return recorded if isinstance(recorded, str) else None
FUNCTION

decode_interval​

omnibias.core.proof.decode_intervalSource ↗
decode_interval(d: Mapping[str, Any]) -> Interval

Inverse of encode_interval.

Parameters

NameType & defaultContract
dpositional-or-keywordMapping[str, Any]RequiredSee the operation contract and implementation below.
ReturnsInterval
Executed regression · interval roundtrip is bit exact

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_interval_roundtrip_is_bit_exact() -> None:
    iv = Interval(0.1, 0.1 + 1e-16)  # endpoints not exactly representable in decimal
    again = decode_interval(encode_interval(iv))
    assert again.lo == iv.lo
    assert again.hi == iv.hi
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_interval_roundtrip_is_bit_exact" -q
Regression example · conditioning certificate rank deficient is honest

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_conditioning_certificate_rank_deficient_is_honest() -> None:
    a = _rand_low_rank(random.Random(3), 4, 3)
    cert = conditioning_certificate(a)
    assert schema_errors_v1(cert) == []
    assert cert["payload"]["positive_definite"] is False
    assert decode_interval(cert["payload"]["condition_number"]).hi == math.inf
python -m pytest packages/omnibias-core/tests/verified/test_conditioning.py -k test_conditioning_certificate_rank_deficient_is_honest -q
Read the implementation
def decode_interval(d: Mapping[str, Any]) -> Interval:
    """Inverse of :func:`encode_interval`."""
    return Interval(_dec_float(d["lo"]), _dec_float(d["hi"]))
Related APIsomnibias.core.verified.Interval↗
Other public import paths
  • omnibias.core.proof.decode_interval
  • omnibias.core.proof.certificate.decode_interval
FUNCTION

decode_interval_matrix​

omnibias.core.proof.decode_interval_matrixSource ↗
decode_interval_matrix(rows: Sequence[Sequence[Mapping[str, Any]]]) -> list[list[Interval]]

Inverse of encode_interval_matrix.

Parameters

NameType & defaultContract
rowspositional-or-keywordSequence[Sequence[Mapping[str, Any]]]RequiredSee the operation contract and implementation below.
Returnslist[list[Interval]]
Read the implementation
def decode_interval_matrix(rows: Sequence[Sequence[Mapping[str, Any]]]) -> list[list[Interval]]:
    """Inverse of :func:`encode_interval_matrix`."""
    return [[decode_interval(iv) for iv in row] for row in rows]
Related APIsomnibias.core.proof.decode_interval↗
Other public import paths
  • omnibias.core.proof.decode_interval_matrix
  • omnibias.core.proof.certificate.decode_interval_matrix
FUNCTION

decode_taylor_model​

omnibias.core.proof.decode_taylor_modelSource ↗
decode_taylor_model(d: Mapping[str, Any]) -> TaylorModel

Inverse of encode_taylor_model.

Parameters

NameType & defaultContract
dpositional-or-keywordMapping[str, Any]RequiredSee the operation contract and implementation below.
ReturnsTaylorModel
Executed regression · taylor model roundtrip is bit exact

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_taylor_model_roundtrip_is_bit_exact() -> None:
    tm = TaylorModel(
        0.3,
        0.25,
        [Interval(1.0, 1.0), Interval(-0.5, -0.4999999999999999), Interval(0.0, 1e-17)],
        Interval(-1e-12, 1e-12),
    )
    again = decode_taylor_model(encode_taylor_model(tm))
    assert again.center == tm.center
    assert again.radius == tm.radius
    assert again.order == tm.order
    assert [(c.lo, c.hi) for c in again.coeffs] == [(c.lo, c.hi) for c in tm.coeffs]
    assert (again.remainder.lo, again.remainder.hi) == (tm.remainder.lo, tm.remainder.hi)
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_taylor_model_roundtrip_is_bit_exact" -q
Regression example · interval roundtrip is bit exact

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_roundtrip_is_bit_exact() -> None:
    iv = Interval(0.1, 0.1 + 1e-16)  # endpoints not exactly representable in decimal
    again = decode_interval(encode_interval(iv))
    assert again.lo == iv.lo
    assert again.hi == iv.hi
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_interval_roundtrip_is_bit_exact -q
Read the implementation
def decode_taylor_model(d: Mapping[str, Any]) -> TaylorModel:
    """Inverse of :func:`encode_taylor_model`."""
    return TaylorModel(
        _dec_float(d["center"]),
        _dec_float(d["radius"]),
        [decode_interval(c) for c in d["coeffs"]],
        decode_interval(d["remainder"]),
    )
Related APIsomnibias.core.proof.decode_interval↗omnibias.core.verified.TaylorModel↗
Other public import paths
  • omnibias.core.proof.decode_taylor_model
  • omnibias.core.proof.certificate.decode_taylor_model
FUNCTION

encode_interval​

omnibias.core.proof.encode_intervalSource ↗
encode_interval(iv: Interval) -> dict[str, str]

Bit-exact JSON encoding of an Interval.

Parameters

NameType & defaultContract
ivpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
Returnsdict[str, str]
Executed regression · certificate is tamper evident

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_certificate_is_tamper_evident() -> None:
    cert = conditioning_certificate(_GRID[4])
    cert["payload"]["positive_definite"] = False  # flip a claim
    assert not verify_certificate_digest(cert)
python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_certificate_is_tamper_evident" -q
Regression example · interval roundtrip is bit exact

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_roundtrip_is_bit_exact() -> None:
    iv = Interval(0.1, 0.1 + 1e-16)  # endpoints not exactly representable in decimal
    again = decode_interval(encode_interval(iv))
    assert again.lo == iv.lo
    assert again.hi == iv.hi
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_interval_roundtrip_is_bit_exact -q
Read the implementation
def encode_interval(iv: Interval) -> dict[str, str]:
    """Bit-exact JSON encoding of an :class:`Interval`."""
    return {"lo": _enc_float(iv.lo), "hi": _enc_float(iv.hi)}
Other public import paths
  • omnibias.core.proof.encode_interval
  • omnibias.core.proof.certificate.encode_interval
FUNCTION

encode_interval_matrix​

omnibias.core.proof.encode_interval_matrixSource ↗
encode_interval_matrix(rows: Sequence[Sequence[Interval]]) -> list[list[dict[str, str]]]

Bit-exact JSON encoding of a matrix (sequence of rows) of Interval.

Parameters

NameType & defaultContract
rowspositional-or-keywordSequence[Sequence[Interval]]RequiredSee the operation contract and implementation below.
Returnslist[list[dict[str, str]]]
Read the implementation
def encode_interval_matrix(rows: Sequence[Sequence[Interval]]) -> list[list[dict[str, str]]]:
    """Bit-exact JSON encoding of a matrix (sequence of rows) of :class:`Interval`."""
    return [[encode_interval(iv) for iv in row] for row in rows]
Related APIsomnibias.core.proof.encode_interval↗
Other public import paths
  • omnibias.core.proof.encode_interval_matrix
  • omnibias.core.proof.certificate.encode_interval_matrix
FUNCTION

encode_taylor_model​

omnibias.core.proof.encode_taylor_modelSource ↗
encode_taylor_model(tm: TaylorModel) -> dict[str, Any]

Bit-exact JSON encoding of a TaylorModel.

Parameters

NameType & defaultContract
tmpositional-or-keywordTaylorModelRequiredSee the operation contract and implementation below.
Returnsdict[str, Any]
Executed regression · digest is stable under reserialization

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_digest_is_stable_under_reserialization() -> None:
    tm = TaylorModel(0.0, 1.0, [Interval(2.0, 2.0), Interval(3.0, 3.0)], Interval(-0.1, 0.1))
    cert = taylor_model_certificate("f enclosure", tm)
    # Recomputing the digest from the body must reproduce the sealed digest.
    assert certificate_digest(cert) == cert["digest"]
    # Re-sealing is idempotent.
    assert seal_certificate(cert)["digest"] == cert["digest"]
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_digest_is_stable_under_reserialization" -q
Regression example · taylor model roundtrip is bit exact

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_taylor_model_roundtrip_is_bit_exact() -> None:
    tm = TaylorModel(
        0.3,
        0.25,
        [Interval(1.0, 1.0), Interval(-0.5, -0.4999999999999999), Interval(0.0, 1e-17)],
        Interval(-1e-12, 1e-12),
    )
    again = decode_taylor_model(encode_taylor_model(tm))
    assert again.center == tm.center
    assert again.radius == tm.radius
    assert again.order == tm.order
    assert [(c.lo, c.hi) for c in again.coeffs] == [(c.lo, c.hi) for c in tm.coeffs]
    assert (again.remainder.lo, again.remainder.hi) == (tm.remainder.lo, tm.remainder.hi)
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_taylor_model_roundtrip_is_bit_exact -q
Read the implementation
def encode_taylor_model(tm: TaylorModel) -> dict[str, Any]:
    """Bit-exact JSON encoding of a :class:`TaylorModel`."""
    return {
        "center": _enc_float(tm.center),
        "radius": _enc_float(tm.radius),
        "order": tm.order,
        "coeffs": [encode_interval(c) for c in tm.coeffs],
        "remainder": encode_interval(tm.remainder),
    }
Related APIsomnibias.core.proof.encode_interval↗
Other public import paths
  • omnibias.core.proof.encode_taylor_model
  • omnibias.core.proof.certificate.encode_taylor_model
FUNCTION

interval_certificate​

omnibias.core.proof.interval_certificateSource ↗
interval_certificate(claim: str, interval: Interval, *, honesty: Mapping[str, bool] | None=None, meta: Mapping[str, Any] | None=None) -> Cert

A sealed certificate asserting a quantity lies in interval.

Parameters

NameType & defaultContract
claimpositional-or-keywordstrRequiredSee the operation contract and implementation below.
intervalpositional-or-keywordIntervalRequiredSee the operation contract and implementation below.
honestykeyword-onlyMapping[str, bool] | NoneDefault: NoneSee the operation contract and implementation below.
metakeyword-onlyMapping[str, Any] | NoneDefault: NoneSee the operation contract and implementation below.
ReturnsCert
Executed regression · generate negative interval obligation

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_generate_negative_interval_obligation() -> None:
    cert = interval_certificate("q", Interval(-2.0, -0.5))
    src = generate_obligation(cert)
    assert src is not None
    assert "enclosed_quantity_neg" in src
python -m pytest "packages/omnibias-core/tests/test_lean_check.py::test_generate_negative_interval_obligation" -q
Regression example · generate positive interval obligation

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_generate_positive_interval_obligation() -> None:
    cert = interval_certificate("q", Interval(0.5, 2.0))
    src = generate_obligation(cert)
    assert src is not None
    assert "enclosed_quantity_pos" in src
    assert "ZInterval.Mem" in src
python -m pytest packages/omnibias-core/tests/test_lean_check.py -k test_generate_positive_interval_obligation -q
Read the implementation
def interval_certificate(
    claim: str,
    interval: Interval,
    *,
    honesty: Mapping[str, bool] | None = None,
    meta: Mapping[str, Any] | None = None,
) -> Cert:
    """A sealed certificate asserting a quantity lies in ``interval``."""
    payload = {"type": "interval", "interval": encode_interval(interval)}
    return make_certificate(claim=claim, payload=payload, honesty=honesty, meta=meta)
Related APIsomnibias.core.proof.encode_interval↗omnibias.core.proof.make_certificate↗
Other public import paths
  • omnibias.core.proof.interval_certificate
  • omnibias.core.proof.certificate.interval_certificate
FUNCTION

make_certificate​

omnibias.core.proof.make_certificateSource ↗
make_certificate(*, claim: str, payload: Mapping[str, Any], honesty: Mapping[str, bool] | None=None, meta: Mapping[str, Any] | None=None) -> Cert

Build and seal a v1 certificate around payload.

honesty defaults to {"unproven_claim": False} -- the omnibias convention that unsupported claims are not certified.

Reserved honesty keys (RESERVED_HONESTY_KEYS, at minimum THEOREM_PROVER_VERIFIED_KEY) may **not** be supplied: they are earned only by the Lean kernel / ProofMachine. Passing one raises ValueError.

The transcendental backend is stamped into meta under TRANSCEND_BACKEND_KEY unless the caller already supplied it (so a decoded certificate re-sealed elsewhere keeps its original provenance rather than acquiring the *re-sealing* machine's). Recording it here rather than in each producer means a certificate can never quietly hide that its bounds rest on the conditionally-rigorous libm_fallback path; read it back with certificate_is_unconditional.

Seal-time enforcement (cannot be bypassed by forgetting to call ~omnibias.core.verified.transcend.require_rigorous_backend):

  • If honesty asserts UNCONDITIONAL_CLAIM_KEY, or ~omnibias.core.verified.transcend.strict_backend / ~omnibias.core.verified.transcend.certificate_mode is active, the rigorous (mpmath) backend is *required* -- sealing raises RuntimeError on the libm fallback.
  • If a transcendental enclosure was already produced via the libm fallback (~omnibias.core.verified.transcend.libm_fallback_used) while the same unconditional / strict gate is active, sealing likewise raises: the payload cannot silently claim unconditional soundness.
  • Designated rigorous enclosure payloads are refused whenever their provenance records the conditional libm fallback. Pure rational interval algebra receives a "not_used" stamp and remains sealable without an optional transcendental package.

Parameters

NameType & defaultContract
claimkeyword-onlystrRequiredSee the operation contract and implementation below.
payloadkeyword-onlyMapping[str, Any]RequiredSee the operation contract and implementation below.
honestykeyword-onlyMapping[str, bool] | NoneDefault: NoneSee the operation contract and implementation below.
metakeyword-onlyMapping[str, Any] | NoneDefault: NoneSee the operation contract and implementation below.
ReturnsCert
Explicit validation & failure cases
  • When designated_rigorous_payload and stamped in CONDITIONAL_TRANSCEND_BACKENDS, raises RuntimeError(f'refusing to seal designated rigorous payload type {payload_type!r}: a transcendental enclosure was produced under the conditionally-rigorous libm_fallback backend. Recompute with mpmath before sealing.').
  • When stamped in CONDITIONAL_TRANSCEND_BACKENDS or (libm_fallback_used() and stamped not in UNCONDITIONAL_TRANSCEND_BACKENDS), raises RuntimeError('refusing to seal an unconditional / strict-mode certificate: a transcendental enclosure was produced under the conditionally-rigorous libm_fallback backend (or the stamp records it). Install mpmath, enter certificate_mode(), and recompute the enclosure before sealing.').

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

Executed regression · honesty defaults to no unproven claim

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_honesty_defaults_to_no_unproven_claim() -> None:
    cert = make_certificate(claim="benign", payload={"type": "interval"})
    assert cert["honesty"] == {"unproven_claim": False}
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_honesty_defaults_to_no_unproven_claim" -q
Regression example · domain subdivision covers no gaps false cases

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_domain_subdivision_covers_no_gaps_false_cases(
    leaves: tuple[SubdivisionLeaf, ...], resolution: int
) -> None:
    cert = DomainSubdivisionCertificate(resolution=resolution, leaves=leaves)
    assert cert.covers_no_gaps() is False
python -m pytest packages/omnibias-core/tests/test_replay.py -k test_domain_subdivision_covers_no_gaps_false_cases -q
Read the implementation
def make_certificate(
    *,
    claim: str,
    payload: Mapping[str, Any],
    honesty: Mapping[str, bool] | None = None,
    meta: Mapping[str, Any] | None = None,
) -> Cert:
    """Build and seal a v1 certificate around ``payload``.

    ``honesty`` defaults to ``{"unproven_claim": False}`` -- the omnibias convention
    that unsupported claims are not certified.

    Reserved honesty keys (:data:`RESERVED_HONESTY_KEYS`, at minimum
    :data:`THEOREM_PROVER_VERIFIED_KEY`) may **not** be supplied: they are earned
    only by the Lean kernel / ProofMachine.  Passing one raises
    :class:`ValueError`.

    The transcendental backend is stamped into ``meta`` under
    :data:`TRANSCEND_BACKEND_KEY` unless the caller already supplied it (so a
    decoded certificate re-sealed elsewhere keeps its original provenance rather
    than acquiring the *re-sealing* machine's).  Recording it here rather than in
    each producer means a certificate can never quietly hide that its bounds rest
    on the conditionally-rigorous ``libm_fallback`` path; read it back with
    :func:`certificate_is_unconditional`.

    Seal-time enforcement (cannot be bypassed by forgetting to call
    :func:`~omnibias.core.verified.transcend.require_rigorous_backend`):

    * If ``honesty`` asserts :data:`UNCONDITIONAL_CLAIM_KEY`, or
      :func:`~omnibias.core.verified.transcend.strict_backend` /
      :func:`~omnibias.core.verified.transcend.certificate_mode` is active, the
      rigorous (mpmath) backend is *required* -- sealing raises
      :class:`RuntimeError` on the libm fallback.
    * If a transcendental enclosure was already produced via the libm fallback
      (:func:`~omnibias.core.verified.transcend.libm_fallback_used`) while the
      same unconditional / strict gate is active, sealing likewise raises: the
      payload cannot silently claim unconditional soundness.
    * Designated rigorous enclosure payloads are refused whenever their
      provenance records the conditional libm fallback.  Pure rational interval
      algebra receives a ``"not_used"`` stamp and remains sealable without an
      optional transcendental package.
    """
    honesty_out = _honesty_without_reserved(honesty)
    meta_out = dict(meta) if meta is not None else {}
    # Prefer an explicit caller stamp; otherwise record the rigorous backend
    # that actually fed the payload.  No transcendental invocation is distinct
    # from a libm fallback: rational interval algebra must not acquire a
    # conditional stamp simply because mpmath is optional.
    if TRANSCEND_BACKEND_KEY not in meta_out:
        stamped = BACKEND_LIBM_FALLBACK if libm_fallback_used() else (
            backend_name() if backend_name() in UNCONDITIONAL_TRANSCEND_BACKENDS else NO_TRANSCENDENTAL_BACKEND
        )
        meta_out[TRANSCEND_BACKEND_KEY] = stamped

    stamped_raw = meta_out.get(TRANSCEND_BACKEND_KEY)
    stamped = stamped_raw if isinstance(stamped_raw, str) else ""
    payload_type_raw = payload.get("type")
    payload_type = payload_type_raw if isinstance(payload_type_raw, str) else ""
    designated_rigorous_payload = payload_type in RIGOROUS_TRANSCENDENTAL_PAYLOAD_TYPES
    if designated_rigorous_payload and stamped in CONDITIONAL_TRANSCEND_BACKENDS:
        raise RuntimeError(
            "refusing to seal designated rigorous payload type "
            f"{payload_type!r}: a transcendental enclosure was produced under "
            "the conditionally-rigorous libm_fallback backend. Recompute with "
            "mpmath before sealing."
        )

    needs_rigorous = bool(honesty_out.get(UNCONDITIONAL_CLAIM_KEY, False)) or strict_backend()
    if needs_rigorous:
        # mpmath must be available *now*, and the sealed stamp must not claim the
        # conditional path.  A sticky libm_fallback_used() under a still-missing
        # mpmath is already caught by require_rigorous_backend(); when a caller
        # tries to launder a hand-stamped libm_fallback meta while mpmath is
        # present, the stamp check below refuses.
        require_rigorous_backend()
        if stamped in CONDITIONAL_TRANSCEND_BACKENDS or (
            libm_fallback_used() and stamped not in UNCONDITIONAL_TRANSCEND_BACKENDS
        ):
            raise RuntimeError(
                "refusing to seal an unconditional / strict-mode certificate: a "
                "transcendental enclosure was produced under the conditionally-"
                "rigorous libm_fallback backend (or the stamp records it). Install "
                "mpmath, enter certificate_mode(), and recompute the enclosure "
                "before sealing."
            )

    cert: Cert = {
        "schema_version": CERTIFICATE_SCHEMA_VERSION,
        "claim": str(claim),
        "payload": dict(payload),
        "honesty": honesty_out,
        "meta": meta_out,
    }
    return seal_certificate(cert)
Related APIsomnibias.core.proof.seal_certificate↗omnibias.core.verified.backend_name↗omnibias.core.verified.libm_fallback_used↗omnibias.core.verified.require_rigorous_backend↗omnibias.core.verified.strict_backend↗
Other public import paths
  • omnibias.core.proof.make_certificate
  • omnibias.core.proof.certificate.make_certificate
FUNCTION

positive_definite_certificate​

omnibias.core.proof.positive_definite_certificateSource ↗
positive_definite_certificate(claim: str, pivots: Sequence[Interval], *, matrix: Sequence[Sequence[Interval]] | None=None, honesty: Mapping[str, bool] | None=None, meta: Mapping[str, Any] | None=None) -> Cert

A sealed certificate that a symmetric interval matrix box is positive definite.

pivots are the interval LDL^T pivots D_jj of the matrix box (from omnibias.core.verified.eig_operator.interval_ldlt_pivots). The matrix box is certified positive definite exactly when every pivot has a strictly positive lower endpoint (zero negative inertia). The optional matrix records the enclosed symmetric matrix the pivots factorise, for provenance and a future division-free L D L^T reconstruction check.

Unlike the single-scalar eig_min interval an interval_certificate would seal, the Lean bridge turns this payload into the kernel-verified *inertia-vector* obligation allPivotsPos (matrix_positive_definite_certified) -- the full positive-definiteness statement rather than its scalar shadow.

Parameters

NameType & defaultContract
claimpositional-or-keywordstrRequiredSee the operation contract and implementation below.
pivotspositional-or-keywordSequence[Interval]RequiredSee the operation contract and implementation below.
matrixkeyword-onlySequence[Sequence[Interval]] | NoneDefault: NoneSee the operation contract and implementation below.
honestykeyword-onlyMapping[str, bool] | NoneDefault: NoneSee the operation contract and implementation below.
metakeyword-onlyMapping[str, Any] | NoneDefault: NoneSee the operation contract and implementation below.
ReturnsCert
Executed regression · pd certificate tamper is rejected before lean

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_pd_certificate_tamper_is_rejected_before_lean() -> None:
    cert = positive_definite_certificate("H is PD", [Interval(0.5, 0.75), Interval(2.0, 3.0)])
    tampered = dict(cert)
    tampered["payload"] = {**cert["payload"], "n": 99}  # body changed, digest stale
    result = check_certificate(tampered)
    assert result.verified is False
    assert "digest" in result.detail
python -m pytest "packages/omnibias-core/tests/test_lean_check.py::test_pd_certificate_tamper_is_rejected_before_lean" -q
Regression example · generate pd obligation none when a pivot is not positive

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_generate_pd_obligation_none_when_a_pivot_is_not_positive() -> None:
    # A pivot whose lower endpoint is not strictly positive is not a PD obligation.
    straddle = positive_definite_certificate("not PD", [Interval(0.5, 1.0), Interval(-0.1, 2.0)])
    assert generate_obligation(straddle) is None
    zero_lo = positive_definite_certificate("not PD", [Interval(0.0, 1.0)])
    assert generate_obligation(zero_lo) is None
python -m pytest packages/omnibias-core/tests/test_lean_check.py -k test_generate_pd_obligation_none_when_a_pivot_is_not_positive -q
Read the implementation
def positive_definite_certificate(
    claim: str,
    pivots: Sequence[Interval],
    *,
    matrix: Sequence[Sequence[Interval]] | None = None,
    honesty: Mapping[str, bool] | None = None,
    meta: Mapping[str, Any] | None = None,
) -> Cert:
    r"""A sealed certificate that a symmetric interval matrix box is positive definite.

    ``pivots`` are the interval ``LDL^T`` pivots ``D_jj`` of the matrix box (from
    :func:`omnibias.core.verified.eig_operator.interval_ldlt_pivots`).  The matrix box is
    certified positive definite exactly when every pivot has a strictly positive lower
    endpoint (zero negative inertia).  The optional ``matrix`` records the enclosed
    symmetric matrix the pivots factorise, for provenance and a future division-free
    ``L D L^T`` reconstruction check.

    Unlike the single-scalar ``eig_min`` interval an :func:`interval_certificate` would
    seal, the Lean bridge turns this payload into the kernel-verified *inertia-vector*
    obligation ``allPivotsPos`` (``matrix_positive_definite_certified``) -- the full
    positive-definiteness statement rather than its scalar shadow.
    """
    pivot_list = list(pivots)
    payload: dict[str, Any] = {
        "type": "positive_definite",
        "n": len(pivot_list),
        "pivots": [encode_interval(p) for p in pivot_list],
    }
    if matrix is not None:
        payload["matrix"] = encode_interval_matrix(matrix)
    return make_certificate(claim=claim, payload=payload, honesty=honesty, meta=meta)
Related APIsomnibias.core.proof.encode_interval↗omnibias.core.proof.encode_interval_matrix↗omnibias.core.proof.make_certificate↗
Other public import paths
  • omnibias.core.proof.positive_definite_certificate
  • omnibias.core.proof.certificate.positive_definite_certificate
FUNCTION

schema_errors_v1​

omnibias.core.proof.schema_errors_v1Source ↗
schema_errors_v1(cert: Mapping[str, Any]) -> list[str]

Structural validation of a v1 certificate (empty list == valid).

Parameters

NameType & defaultContract
certpositional-or-keywordMapping[str, Any]RequiredSee the operation contract and implementation below.
Returnslist[str]
Executed regression · seal and verify digest

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_seal_and_verify_digest() -> None:
    cert = interval_certificate("x in [0,1]", Interval(0.0, 1.0))
    assert cert["schema_version"] == CERTIFICATE_SCHEMA_VERSION
    assert cert["digest"].startswith("sha256:")
    assert verify_certificate_digest(cert)
    assert schema_errors_v1(cert) == []
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_seal_and_verify_digest" -q
Regression example · conditioning certificate rank deficient is honest

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_conditioning_certificate_rank_deficient_is_honest() -> None:
    a = _rand_low_rank(random.Random(3), 4, 3)
    cert = conditioning_certificate(a)
    assert schema_errors_v1(cert) == []
    assert cert["payload"]["positive_definite"] is False
    assert decode_interval(cert["payload"]["condition_number"]).hi == math.inf
python -m pytest packages/omnibias-core/tests/verified/test_conditioning.py -k test_conditioning_certificate_rank_deficient_is_honest -q
Read the implementation
def schema_errors_v1(cert: Mapping[str, Any]) -> list[str]:
    """Structural validation of a v1 certificate (empty list == valid)."""
    errors: list[str] = []
    version = cert.get("schema_version")
    if version not in SUPPORTED_SCHEMA_VERSIONS:
        errors.append(f"unsupported schema_version {version!r}")
    for key in ("claim", "payload", "honesty", "digest"):
        if key not in cert:
            errors.append(f"missing required field {key!r}")
    if "claim" in cert and not isinstance(cert["claim"], str):
        errors.append("'claim' must be a string")
    if "payload" in cert and not isinstance(cert["payload"], Mapping):
        errors.append("'payload' must be a mapping")
    if "honesty" in cert and not isinstance(cert["honesty"], Mapping):
        errors.append("'honesty' must be a mapping")
    honesty = cert.get("honesty")
    if isinstance(honesty, Mapping):
        reserved = sorted(k for k in honesty if k in RESERVED_HONESTY_KEYS)
        if reserved:
            errors.append(
                f"honesty must not contain reserved key(s) {reserved}; "
                f"{THEOREM_PROVER_VERIFIED_KEY} is earned only by the Lean kernel "
                "/ ProofMachine"
            )
        if bool(honesty.get(UNCONDITIONAL_CLAIM_KEY, False)) and not certificate_is_unconditional(
            cert
        ):
            recorded = certificate_transcend_backend(cert)
            errors.append(
                f"honesty.{UNCONDITIONAL_CLAIM_KEY} is asserted but the certificate was "
                f"sealed on transcendental backend {recorded!r}, whose rigour is only "
                "conditional on the platform libm error budget; install mpmath and "
                "re-seal, or drop the claim"
            )
    payload = cert.get("payload")
    if isinstance(payload, Mapping):
        payload_type = payload.get("type")
        recorded = certificate_transcend_backend(cert)
        if (
            isinstance(payload_type, str)
            and payload_type in RIGOROUS_TRANSCENDENTAL_PAYLOAD_TYPES
            and recorded in CONDITIONAL_TRANSCEND_BACKENDS
        ):
            errors.append(
                f"payload type {payload_type!r} is designated rigorous but its "
                f"transcendental backend {recorded!r} is conditional; recompute "
                "with mpmath before sealing"
            )
    if "digest" in cert and not verify_certificate_digest(cert):
        errors.append("digest mismatch (tampered or stale certificate)")
    return errors
Related APIsomnibias.core.proof.certificate.certificate_is_unconditional↗omnibias.core.proof.certificate.certificate_transcend_backend↗omnibias.core.proof.verify_certificate_digest↗
Other public import paths
  • omnibias.core.proof.schema_errors_v1
  • omnibias.core.proof.certificate.schema_errors_v1
FUNCTION

seal_certificate​

omnibias.core.proof.seal_certificateSource ↗
seal_certificate(cert: Mapping[str, Any]) -> Cert

Return a copy with schema_version set and a fresh digest appended.

Parameters

NameType & defaultContract
certpositional-or-keywordMapping[str, Any]RequiredSee the operation contract and implementation below.
ReturnsCert
Executed regression · honesty defaults to no unproven claim

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_honesty_defaults_to_no_unproven_claim() -> None:
    cert = make_certificate(claim="benign", payload={"type": "interval"})
    assert cert["honesty"] == {"unproven_claim": False}
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_honesty_defaults_to_no_unproven_claim" -q
Regression example · generate negative interval obligation

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_generate_negative_interval_obligation() -> None:
    cert = interval_certificate("q", Interval(-2.0, -0.5))
    src = generate_obligation(cert)
    assert src is not None
    assert "enclosed_quantity_neg" in src
python -m pytest packages/omnibias-core/tests/test_lean_check.py -k test_generate_negative_interval_obligation -q
Read the implementation
def seal_certificate(cert: Mapping[str, Any]) -> Cert:
    """Return a copy with ``schema_version`` set and a fresh ``digest`` appended."""
    out: Cert = {k: v for k, v in cert.items() if k != "digest"}
    out.setdefault("schema_version", CERTIFICATE_SCHEMA_VERSION)
    out["digest"] = certificate_digest(out)
    return out
Related APIsomnibias.core.proof.certificate_digest↗
Other public import paths
  • omnibias.core.proof.seal_certificate
  • omnibias.core.proof.certificate.seal_certificate
FUNCTION

taylor_model_certificate​

omnibias.core.proof.taylor_model_certificateSource ↗
taylor_model_certificate(claim: str, model: TaylorModel, *, honesty: Mapping[str, bool] | None=None, meta: Mapping[str, Any] | None=None) -> Cert

A sealed certificate carrying a TaylorModel enclosure.

Parameters

NameType & defaultContract
claimpositional-or-keywordstrRequiredSee the operation contract and implementation below.
modelpositional-or-keywordTaylorModelRequiredSee the operation contract and implementation below.
honestykeyword-onlyMapping[str, bool] | NoneDefault: NoneSee the operation contract and implementation below.
metakeyword-onlyMapping[str, Any] | NoneDefault: NoneSee the operation contract and implementation below.
ReturnsCert
Executed regression · digest is stable under reserialization

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_digest_is_stable_under_reserialization() -> None:
    tm = TaylorModel(0.0, 1.0, [Interval(2.0, 2.0), Interval(3.0, 3.0)], Interval(-0.1, 0.1))
    cert = taylor_model_certificate("f enclosure", tm)
    # Recomputing the digest from the body must reproduce the sealed digest.
    assert certificate_digest(cert) == cert["digest"]
    # Re-sealing is idempotent.
    assert seal_certificate(cert)["digest"] == cert["digest"]
python -m pytest "packages/omnibias-core/tests/test_certificate.py::test_digest_is_stable_under_reserialization" -q
Regression example · every certificate records its transcendental backend

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_every_certificate_records_its_transcendental_backend() -> None:
    # Stamped centrally, so no individual producer can forget the provenance.
    for cert in (
        make_certificate(claim="c", payload={"type": "interval"}),
        interval_certificate("x in [0,1]", Interval(0.0, 1.0)),
        taylor_model_certificate(
            "tm",
            TaylorModel(0.0, 0.25, [Interval(1.0, 1.0), Interval(0.5, 0.5)], Interval(-1e-12, 1e-12)),
        ),
    ):
        recorded = certificate_transcend_backend(cert)
        assert isinstance(recorded, str) and recorded
        assert cert["meta"][TRANSCEND_BACKEND_KEY] == recorded
        assert not schema_errors_v1(cert)
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_every_certificate_records_its_transcendental_backend -q
Read the implementation
def taylor_model_certificate(
    claim: str,
    model: TaylorModel,
    *,
    honesty: Mapping[str, bool] | None = None,
    meta: Mapping[str, Any] | None = None,
) -> Cert:
    """A sealed certificate carrying a :class:`TaylorModel` enclosure."""
    payload = {"type": "taylor_model", "taylor_model": encode_taylor_model(model)}
    return make_certificate(claim=claim, payload=payload, honesty=honesty, meta=meta)
Related APIsomnibias.core.proof.encode_taylor_model↗omnibias.core.proof.make_certificate↗
Other public import paths
  • omnibias.core.proof.taylor_model_certificate
  • omnibias.core.proof.certificate.taylor_model_certificate
FUNCTION

verify_certificate_digest​

omnibias.core.proof.verify_certificate_digestSource ↗
verify_certificate_digest(cert: Mapping[str, Any]) -> bool

True iff cert carries a digest that matches its body.

Parameters

NameType & defaultContract
certpositional-or-keywordMapping[str, Any]RequiredSee the operation contract and implementation below.
Returnsbool
Executed regression · certificate is tamper evident

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_certificate_is_tamper_evident() -> None:
    cert = conditioning_certificate(_GRID[4])
    cert["payload"]["positive_definite"] = False  # flip a claim
    assert not verify_certificate_digest(cert)
python -m pytest "packages/omnibias-core/tests/verified/test_conditioning.py::test_certificate_is_tamper_evident" -q
Regression example · seal and verify digest

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_seal_and_verify_digest() -> None:
    cert = interval_certificate("x in [0,1]", Interval(0.0, 1.0))
    assert cert["schema_version"] == CERTIFICATE_SCHEMA_VERSION
    assert cert["digest"].startswith("sha256:")
    assert verify_certificate_digest(cert)
    assert schema_errors_v1(cert) == []
python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_seal_and_verify_digest -q
Read the implementation
def verify_certificate_digest(cert: Mapping[str, Any]) -> bool:
    """``True`` iff ``cert`` carries a ``digest`` that matches its body."""
    digest = cert.get("digest")
    if not isinstance(digest, str):
        return False
    return digest == certificate_digest(cert)
Related APIsomnibias.core.proof.certificate_digest↗
Other public import paths
  • omnibias.core.proof.verify_certificate_digest
  • omnibias.core.proof.certificate.verify_certificate_digest
← Package overviewRunnable learning examples →