API REFERENCE/omnibias-struct

omnibias.struct.decode

0.1.0a2AlphaPython >=3.10AGPL / commercial

Differentiable dynamic programs for sequences and parses, structured distributions, and finite-temperature bounds.

import omnibias.struct.decode

Module contract & mathematical conventions

Public certified-decoding surface -- prove the Viterbi winner survives an eps-ball.

Re-exports the rigorous decoding certifier from omnibias.struct._core.decode: certify_decoding (worst-case winner-vs-runner-up margin over an emission L_inf ball, enumeration-free), its DAG / DTW generalization certify_decoding_dag (the same margin over an edge L_inf ball, so it covers the alignment / DTW lattices), the DecodingCertificate / DAGDecodingCertificate they return, and the sealing + optional-Lean bridges. Decoding is backend-agnostic (a sign fact about the beta -> inf max-plus semiring), so there is a single numpy implementation rather than torch / jax twins; pass a backend tensor's .detach().cpu().numpy() (torch) or np.asarray(...) (jax) as the emissions.

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 →

CLASS

DAGDecodingCertificate

omnibias.struct.decode.DAGDecodingCertificateSource ↗

class DAGDecodingCertificate

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.

Certified worst-case margin of a DAG shortest-path decode over an edge eps-ball.

Generalizes DecodingCertificate from the linear chain to any topologically ordered ~omnibias.struct.DAG (so it also covers the alignment / DTW lattices, which are DAGs). margin soundly encloses M = min_{q != p*} [cost(q, w) - cost(p*, w) - eps * |edges(q) triangle edges(p*)|] -- the worst-case cost gap of the winning path p* against every other path when each edge weight is perturbed within eps. Certified stable iff margin.lo > 0; scope is the local_box.

Parameters

Name	Type & default	Contract
certifieddataclass field	boolRequired	See the operation contract and implementation below.
winnerdataclass field	tuple[int, ...]Required	See the operation contract and implementation below.
epsdataclass field	floatRequired	See the operation contract and implementation below.
margindataclass field	IntervalRequired	See the operation contract and implementation below.
num_nodesdataclass field	intRequired	See the operation contract and implementation below.
num_edgesdataclass field	intRequired	See the operation contract and implementation below.

Executed regression · dag margin matches bruteforce

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_dag_margin_matches_bruteforce(eps: float) -> None:
    cert = certify_decoding_dag(_DIAMOND_EDGES, _DIAMOND, eps)
    assert abs(cert.min_margin - _dag_worst_margin(_DIAMOND, _DIAMOND_EDGES, eps)) < 1e-9

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_dag_margin_matches_bruteforce[0.05]" -q

Fields & methods

certifiedfield

certified: bool

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

View source ↗

winnerfield

winner: tuple[int, ...]

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

View source ↗

epsfield

eps: float

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

View source ↗

marginfield

margin: Interval

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

View source ↗

num_nodesfield

num_nodes: int

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

View source ↗

num_edgesfield

num_edges: int

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

View source ↗

min_marginproperty

min_margin(self) -> float

Certified lower bound on the worst-case winner-vs-runner-up cost margin.

Returns: float

Executed regression · dag margin matches bruteforce

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_dag_margin_matches_bruteforce(eps: float) -> None:
    cert = certify_decoding_dag(_DIAMOND_EDGES, _DIAMOND, eps)
    assert abs(cert.min_margin - _dag_worst_margin(_DIAMOND, _DIAMOND_EDGES, eps)) < 1e-9

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_dag_margin_matches_bruteforce[0.05]" -q

Method implementation

    def min_margin(self) -> float:
        """Certified lower bound on the worst-case winner-vs-runner-up cost margin."""
        return float(self.margin.lo)

View source ↗

Read the implementation

class DAGDecodingCertificate:
    r"""Certified worst-case margin of a DAG shortest-path decode over an edge ``eps``-ball.

    Generalizes :class:`DecodingCertificate` from the linear chain to any topologically
    ordered :class:`~omnibias.struct.DAG` (so it also covers the alignment / DTW lattices,
    which are DAGs). ``margin`` soundly encloses
    ``M = min_{q != p*} [cost(q, w) - cost(p*, w) - eps * |edges(q) triangle edges(p*)|]``
    -- the worst-case cost gap of the winning path ``p*`` against every other path when each
    edge weight is perturbed within ``eps``. Certified stable iff ``margin.lo > 0``; scope is
    the ``local_box``.
    """

    certified: bool
    winner: tuple[int, ...]
    eps: float
    margin: Interval
    num_nodes: int
    num_edges: int

    @property
    def min_margin(self) -> float:
        """Certified lower bound on the worst-case winner-vs-runner-up cost margin."""
        return float(self.margin.lo)

CLASS

DAGDecodingProofVerdict

omnibias.struct.decode.DAGDecodingProofVerdictSource ↗

class DAGDecodingProofVerdict

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.

A sealed DAG-decoding certificate plus its Lean-kernel adjudication.

Parameters

Name	Type & default	Contract
certificatedataclass field	CertRequired	See the operation contract and implementation below.
decodingdataclass field	DAGDecodingCertificateRequired	See the operation contract and implementation below.
obligationdataclass field	str | NoneRequired	See the operation contract and implementation below.
leandataclass field	LeanCheckResultRequired	See the operation contract and implementation below.

Executed regression · dag seal is digest verifiable and lean bridge is honest

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_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    cert = certify_decoding_dag(_DIAMOND_EDGES, _DIAMOND, eps=0.1)
    sealed = seal_dag_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_dag_decoding_certificate(cert)
    assert verdict.sealed_ok
    assert verdict.obligation_generated
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Fields & methods

certificatefield

certificate: Cert

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

View source ↗

decodingfield

decoding: DAGDecodingCertificate

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

View source ↗

obligationfield

obligation: str | None

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

View source ↗

leanfield

lean: LeanCheckResult

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

View source ↗

theorem_prover_verifiedproperty

theorem_prover_verified(self) -> bool

True only on a genuine Lean lake build pass (never forged).

Returns: bool

Executed regression · dag seal is digest verifiable and lean bridge is honest

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_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    cert = certify_decoding_dag(_DIAMOND_EDGES, _DIAMOND, eps=0.1)
    sealed = seal_dag_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_dag_decoding_certificate(cert)
    assert verdict.sealed_ok
    assert verdict.obligation_generated
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Method implementation

    def theorem_prover_verified(self) -> bool:
        """``True`` only on a genuine Lean ``lake build`` pass (never forged)."""
        return bool(self.lean.verified)

View source ↗

sealed_okproperty

sealed_ok(self) -> bool

Whether the certificate's tamper-evident digest matches its body.

Returns: bool

Executed regression · dag seal is digest verifiable and lean bridge is honest

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_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    cert = certify_decoding_dag(_DIAMOND_EDGES, _DIAMOND, eps=0.1)
    sealed = seal_dag_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_dag_decoding_certificate(cert)
    assert verdict.sealed_ok
    assert verdict.obligation_generated
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Method implementation

    def sealed_ok(self) -> bool:
        """Whether the certificate's tamper-evident digest matches its body."""
        return bool(verify_certificate_digest(self.certificate))

View source ↗

obligation_generatedproperty

obligation_generated(self) -> bool

Whether a finite, Lean-checkable positivity obligation was produced.

Returns: bool

Executed regression · dag seal is digest verifiable and lean bridge is honest

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_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    cert = certify_decoding_dag(_DIAMOND_EDGES, _DIAMOND, eps=0.1)
    sealed = seal_dag_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_dag_decoding_certificate(cert)
    assert verdict.sealed_ok
    assert verdict.obligation_generated
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Method implementation

    def obligation_generated(self) -> bool:
        """Whether a finite, Lean-checkable positivity obligation was produced."""
        return self.obligation is not None

View source ↗

Read the implementation

class DAGDecodingProofVerdict:
    """A sealed DAG-decoding certificate plus its Lean-kernel adjudication."""

    certificate: Cert
    decoding: DAGDecodingCertificate
    obligation: str | None
    lean: LeanCheckResult

    @property
    def theorem_prover_verified(self) -> bool:
        """``True`` only on a genuine Lean ``lake build`` pass (never forged)."""
        return bool(self.lean.verified)

    @property
    def sealed_ok(self) -> bool:
        """Whether the certificate's tamper-evident digest matches its body."""
        return bool(verify_certificate_digest(self.certificate))

    @property
    def obligation_generated(self) -> bool:
        """Whether a finite, Lean-checkable positivity obligation was produced."""
        return self.obligation is not None

Related APIsomnibias.core.proof.verify_certificate_digest↗

CLASS

DecodingCertificate

omnibias.struct.decode.DecodingCertificateSource ↗

class DecodingCertificate

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.

Certified worst-case margin of the Viterbi winner over an emission eps-ball.

margin soundly (and tightly) encloses M = min_{x in box} [score(p*, x) - max_{p != p*} score(p, x)]; the decode is certified stable iff margin.lo > 0 (the winner is the unique argmax for every emission matrix within eps of the nominal input). Scope is the local_box.

Parameters

Name	Type & default	Contract
certifieddataclass field	boolRequired	See the operation contract and implementation below.
winnerdataclass field	tuple[int, ...]Required	See the operation contract and implementation below.
epsdataclass field	floatRequired	See the operation contract and implementation below.
margindataclass field	IntervalRequired	See the operation contract and implementation below.
n_stepsdataclass field	intRequired	See the operation contract and implementation below.
n_statesdataclass field	intRequired	See the operation contract and implementation below.

Executed regression · certifies well separated winner and matches viterbi

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_certifies_well_separated_winner_and_matches_viterbi() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.25)
    _, winner = viterbi(ChainTrellis(emis, trans, np.zeros(2)))
    assert cert.winner == winner
    assert cert.certified
    assert cert.min_margin > 0.0

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_certifies_well_separated_winner_and_matches_viterbi" -q

Fields & methods

certifiedfield

certified: bool

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

View source ↗

winnerfield

winner: tuple[int, ...]

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

View source ↗

epsfield

eps: float

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

View source ↗

marginfield

margin: Interval

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

View source ↗

n_stepsfield

n_steps: int

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

View source ↗

n_statesfield

n_states: int

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

View source ↗

min_marginproperty

min_margin(self) -> float

Certified lower bound on the worst-case winner-vs-runner-up margin.

Returns: float

Executed regression · certifies well separated winner and matches viterbi

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_certifies_well_separated_winner_and_matches_viterbi() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.25)
    _, winner = viterbi(ChainTrellis(emis, trans, np.zeros(2)))
    assert cert.winner == winner
    assert cert.certified
    assert cert.min_margin > 0.0

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_certifies_well_separated_winner_and_matches_viterbi" -q

Method implementation

    def min_margin(self) -> float:
        """Certified lower bound on the worst-case winner-vs-runner-up margin."""
        return float(self.margin.lo)

View source ↗

Read the implementation

class DecodingCertificate:
    r"""Certified worst-case margin of the Viterbi winner over an emission ``eps``-ball.

    ``margin`` soundly (and tightly) encloses
    ``M = min_{x in box} [score(p*, x) - max_{p != p*} score(p, x)]``; the decode is certified
    stable iff ``margin.lo > 0`` (the winner is the unique argmax for every emission matrix
    within ``eps`` of the nominal input). Scope is the ``local_box``.
    """

    certified: bool
    winner: tuple[int, ...]
    eps: float
    margin: Interval
    n_steps: int
    n_states: int

    @property
    def min_margin(self) -> float:
        """Certified lower bound on the worst-case winner-vs-runner-up margin."""
        return float(self.margin.lo)

CLASS

DecodingProofVerdict

omnibias.struct.decode.DecodingProofVerdictSource ↗

class DecodingProofVerdict

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.

A sealed decoding certificate plus its Lean-kernel adjudication.

Parameters

Name	Type & default	Contract
certificatedataclass field	CertRequired	See the operation contract and implementation below.
decodingdataclass field	DecodingCertificateRequired	See the operation contract and implementation below.
obligationdataclass field	str | NoneRequired	See the operation contract and implementation below.
leandataclass field	LeanCheckResultRequired	See the operation contract and implementation below.

Executed regression · seal is digest verifiable and lean bridge is honest

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_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.2)
    sealed = seal_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_decoding_certificate(cert)
    assert verdict.sealed_ok  # tamper-evident digest matches
    assert verdict.obligation_generated  # margin.lo > 0 -> enclosed_quantity_pos
    # theorem_prover_verified is exactly the (real) lake verdict -- never forged.
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Fields & methods

certificatefield

certificate: Cert

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

View source ↗

decodingfield

decoding: DecodingCertificate

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

View source ↗

obligationfield

obligation: str | None

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

View source ↗

leanfield

lean: LeanCheckResult

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

View source ↗

theorem_prover_verifiedproperty

theorem_prover_verified(self) -> bool

True only on a genuine Lean lake build pass (never forged).

Returns: bool

Executed regression · seal is digest verifiable and lean bridge is honest

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_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.2)
    sealed = seal_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_decoding_certificate(cert)
    assert verdict.sealed_ok  # tamper-evident digest matches
    assert verdict.obligation_generated  # margin.lo > 0 -> enclosed_quantity_pos
    # theorem_prover_verified is exactly the (real) lake verdict -- never forged.
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Method implementation

    def theorem_prover_verified(self) -> bool:
        """``True`` only on a genuine Lean ``lake build`` pass (never forged)."""
        return bool(self.lean.verified)

View source ↗

sealed_okproperty

sealed_ok(self) -> bool

Whether the certificate's tamper-evident digest matches its body.

Returns: bool

Executed regression · seal is digest verifiable and lean bridge is honest

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_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.2)
    sealed = seal_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_decoding_certificate(cert)
    assert verdict.sealed_ok  # tamper-evident digest matches
    assert verdict.obligation_generated  # margin.lo > 0 -> enclosed_quantity_pos
    # theorem_prover_verified is exactly the (real) lake verdict -- never forged.
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Method implementation

    def sealed_ok(self) -> bool:
        """Whether the certificate's tamper-evident digest matches its body."""
        return bool(verify_certificate_digest(self.certificate))

View source ↗

obligation_generatedproperty

obligation_generated(self) -> bool

Whether a finite, Lean-checkable positivity obligation was produced.

Returns: bool

Executed regression · seal is digest verifiable and lean bridge is honest

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_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.2)
    sealed = seal_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_decoding_certificate(cert)
    assert verdict.sealed_ok  # tamper-evident digest matches
    assert verdict.obligation_generated  # margin.lo > 0 -> enclosed_quantity_pos
    # theorem_prover_verified is exactly the (real) lake verdict -- never forged.
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Method implementation

    def obligation_generated(self) -> bool:
        """Whether a finite, Lean-checkable positivity obligation was produced."""
        return self.obligation is not None

View source ↗

Read the implementation

class DecodingProofVerdict:
    """A sealed decoding certificate plus its Lean-kernel adjudication."""

    certificate: Cert
    decoding: DecodingCertificate
    obligation: str | None
    lean: LeanCheckResult

    @property
    def theorem_prover_verified(self) -> bool:
        """``True`` only on a genuine Lean ``lake build`` pass (never forged)."""
        return bool(self.lean.verified)

    @property
    def sealed_ok(self) -> bool:
        """Whether the certificate's tamper-evident digest matches its body."""
        return bool(verify_certificate_digest(self.certificate))

    @property
    def obligation_generated(self) -> bool:
        """Whether a finite, Lean-checkable positivity obligation was produced."""
        return self.obligation is not None

Related APIsomnibias.core.proof.verify_certificate_digest↗

FUNCTION

certify_decoding

omnibias.struct.decode.certify_decodingSource ↗

certify_decoding(emissions: Sequence[Sequence[float]], transitions: Sequence[Sequence[float]], eps: float, *, start: Sequence[float] | None=None) -> DecodingCertificate

Certify the linear-chain Viterbi decode over ||x - emissions||_inf <= eps.

emissions is the (T, S) nominal input (the perturbed quantity); transitions (S, S) and start (S,) are exact model parameters. The winner p* is the decode at emissions; the returned DecodingCertificate encloses the worst-case margin over the box (sound, not tight; local_box scope).

Parameters

Name	Type & default	Contract
emissionspositional-or-keyword	Sequence[Sequence[float]]Required	See the operation contract and implementation below.
transitionspositional-or-keyword	Sequence[Sequence[float]]Required	See the operation contract and implementation below.
epspositional-or-keyword	floatRequired	See the operation contract and implementation below.
startkeyword-only	Sequence[float] | NoneDefault: None	See the operation contract and implementation below.

ReturnsDecodingCertificate

Explicit validation & failure cases

• When eps < 0.0, raises ValueError(f'eps must be non-negative, got {eps}').
• When n_states < 2, raises ValueError('certify_decoding needs n_states >= 2 (no runner-up otherwise)').

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

Executed regression · margin interval encloses center margin

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_margin_interval_encloses_center_margin() -> None:
    emis = np.array([[2.0, 0.0], [0.0, 2.0], [2.0, 0.0]])
    trans = np.array([[0.3, 0.1], [0.1, 0.3]])
    start = np.zeros(2)
    cert = certify_decoding(emis, trans, eps=0.2, start=start)
    center = _margin_at(emis, trans, start, cert.winner)
    assert cert.margin.lo - TOL <= center <= cert.margin.hi + TOL

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_margin_interval_encloses_center_margin" -q

Regression example · certifies well separated winner and matches viterbi

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_certifies_well_separated_winner_and_matches_viterbi() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.25)
    _, winner = viterbi(ChainTrellis(emis, trans, np.zeros(2)))
    assert cert.winner == winner
    assert cert.certified
    assert cert.min_margin > 0.0

python -m pytest packages/omnibias-struct/tests/test_decode.py -k test_certifies_well_separated_winner_and_matches_viterbi -q

Read the implementation

def certify_decoding(
    emissions: Sequence[Sequence[float]],
    transitions: Sequence[Sequence[float]],
    eps: float,
    *,
    start: Sequence[float] | None = None,
) -> DecodingCertificate:
    r"""Certify the linear-chain Viterbi decode over ``||x - emissions||_inf <= eps``.

    ``emissions`` is the ``(T, S)`` nominal input (the perturbed quantity); ``transitions``
    ``(S, S)`` and ``start`` ``(S,)`` are exact model parameters. The winner ``p*`` is the
    decode at ``emissions``; the returned :class:`DecodingCertificate` encloses the
    worst-case margin over the box (sound, not tight; ``local_box`` scope).
    """
    if eps < 0.0:
        raise ValueError(f"eps must be non-negative, got {eps}")
    emis = np.asarray(emissions, dtype=float)
    trans = np.asarray(transitions, dtype=float)
    n_steps, n_states = emis.shape
    if n_states < 2:
        raise ValueError("certify_decoding needs n_states >= 2 (no runner-up otherwise)")
    start_arr = np.zeros(n_states) if start is None else np.asarray(start, dtype=float)

    _, winner = viterbi(ChainTrellis(emis, trans, start_arr))

    # Reduced weights, measured *relative to the winner* so shared emissions cancel exactly.
    # re_emit[t][s] encloses emit[t, p*[t]] - emit[t, s] over the box (0 exactly on the winner);
    # transition / start differences are exact (those parameters are not perturbed).
    pad = Interval(-eps, eps)
    win_emit_iv = [Interval.point(float(emis[t, winner[t]])) + pad for t in range(n_steps)]

    def re_emit(t: int, s: int) -> Interval:
        if s == winner[t]:
            return Interval.point(0.0)
        return win_emit_iv[t] - (Interval.point(float(emis[t, s])) + pad)

    def re_trans(t: int, sp: int, s: int) -> Interval:
        # winner edge p*[t-1] -> p*[t] minus competitor edge sp -> s (exact).
        w = float(trans[winner[t - 1], winner[t]])
        return Interval.point(w - float(trans[sp, s]))

    def re_start(s: int) -> Interval:
        return Interval.point(float(start_arr[winner[0]]) - float(start_arr[s]))

    # dev[t][s] = min reduced margin of a prefix ending at (t, s) that has already
    # deviated from the winner in >= 1 step (the winner-aligned prefix stays exactly 0).
    dev: list[Interval] = [
        _INF if s == winner[0] else re_emit(0, s) + re_start(s) for s in range(n_states)
    ]
    for t in range(1, n_steps):
        # best_any[sp]: min reduced prefix to (t-1, sp) over deviated *or* on-winner. The
        # on-winner (exactly 0) prefix exists only at sp == p*[t-1].
        zero = Interval.point(0.0)
        best_any = [
            _iv_min([dev[sp], zero]) if sp == winner[t - 1] else dev[sp] for sp in range(n_states)
        ]
        nxt: list[Interval] = []
        for s in range(n_states):
            if s != winner[t]:
                # This step itself deviates, so the on-winner prefix is admissible too.
                cands = [best_any[sp] + re_trans(t, sp, s) for sp in range(n_states)]
            else:
                # Landing back on the winner: continuing the on-winner 0 prefix does NOT
                # deviate, so at sp == p*[t-1] only an already-deviated prefix (dev) counts.
                cands = [dev[sp] + re_trans(t, sp, s) for sp in range(n_states)]
            nxt.append(re_emit(t, s) + _iv_min(cands))
        dev = nxt

    margin = _iv_min(dev)  # worst-case winner-vs-any-other-path margin over the box
    return DecodingCertificate(
        certified=margin.lo > 0.0,
        winner=tuple(int(w) for w in winner),
        eps=float(eps),
        margin=margin,
        n_steps=int(n_steps),
        n_states=int(n_states),
    )

Related APIsomnibias.core.verified.Interval↗omnibias.struct.decode.DecodingCertificate↗omnibias.struct.viterbi↗omnibias.struct.ChainTrellis↗

FUNCTION

certify_decoding_dag

omnibias.struct.decode.certify_decoding_dagSource ↗

certify_decoding_dag(weights: Mapping[tuple[int, int], float] | Sequence[Sequence[float]], dag: DAG, eps: float) -> DAGDecodingCertificate

Certify the DAG shortest-path decode over ||w - weights||_inf <= eps on the edges.

weights supplies the nominal edge costs (a {(u, v): w} map or a dense (n, n) matrix; only the dag edges are read); every edge is perturbed independently within eps. Working in edge weights *reduced relative to the winner* -- w'_e = w_e - eps + 2 eps [e in p*] -- turns the worst-case margin into one deviation-tracking min-plus shortest path (no path enumeration): shared edges cancel, so the enclosure is tight. Returns a DAGDecodingCertificate (sound, local_box scope).

Parameters

Name	Type & default	Contract
weightspositional-or-keyword	Mapping[tuple[int, int], float] | Sequence[Sequence[float]]Required	See the operation contract and implementation below.
dagpositional-or-keyword	DAGRequired	See the operation contract and implementation below.
epspositional-or-keyword	floatRequired	See the operation contract and implementation below.

ReturnsDAGDecodingCertificate

Explicit validation & failure cases

• When eps < 0.0, raises ValueError(f'eps must be non-negative, got {eps}').

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

Executed regression · dag large ball not certified

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_dag_large_ball_not_certified() -> None:
    cert = certify_decoding_dag(_DIAMOND_EDGES, _DIAMOND, eps=5.0)
    assert not cert.certified

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_dag_large_ball_not_certified" -q

Regression example · dag margin matches bruteforce

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_dag_margin_matches_bruteforce(eps: float) -> None:
    cert = certify_decoding_dag(_DIAMOND_EDGES, _DIAMOND, eps)
    assert abs(cert.min_margin - _dag_worst_margin(_DIAMOND, _DIAMOND_EDGES, eps)) < 1e-9

python -m pytest packages/omnibias-struct/tests/test_decode.py -k test_dag_margin_matches_bruteforce -q

Read the implementation

def certify_decoding_dag(
    weights: Mapping[tuple[int, int], float] | Sequence[Sequence[float]],
    dag: DAG,
    eps: float,
) -> DAGDecodingCertificate:
    r"""Certify the DAG shortest-path decode over ``||w - weights||_inf <= eps`` on the edges.

    ``weights`` supplies the nominal edge costs (a ``{(u, v): w}`` map or a dense
    ``(n, n)`` matrix; only the ``dag`` edges are read); every edge is perturbed independently
    within ``eps``. Working in edge weights *reduced relative to the winner* -- ``w'_e =
    w_e - eps + 2 eps [e in p*]`` -- turns the worst-case margin into one deviation-tracking
    min-plus shortest path (``no`` path enumeration): shared edges cancel, so the enclosure is
    tight. Returns a :class:`DAGDecodingCertificate` (sound, ``local_box`` scope).
    """
    if eps < 0.0:
        raise ValueError(f"eps must be non-negative, got {eps}")
    wmat = dag.weight_matrix() if not isinstance(weights, Mapping) else None

    def w_of(u: int, v: int) -> float:
        if isinstance(weights, Mapping):
            return float(weights[(u, v)])
        return float(weights[u][v]) if wmat is None else float(wmat[u, v])

    _, winner = shortest_path(dag)
    win_edges = set(zip(winner[:-1], winner[1:], strict=True))
    eps_iv = Interval.point(float(eps))
    two_eps = Interval.point(2.0 * float(eps))

    def w_prime(u: int, v: int) -> Interval:
        base = Interval.point(w_of(u, v)) - eps_iv
        return base + two_eps if (u, v) in win_edges else base

    # on[v]: cost' of the (unique) prefix that still follows p*; dev[v]: best deviated prefix.
    on: list[Interval | None] = [None] * dag.num_nodes
    dev: list[Interval | None] = [None] * dag.num_nodes
    on[dag.source] = Interval.point(0.0)
    for v in range(dag.num_nodes):
        for u in dag.incoming(v):
            wp = w_prime(u, v)
            on_edge = (u, v) in win_edges
            on_u = on[u]
            if on_u is not None:
                cand = on_u + wp
                if on_edge:
                    cur_on = on[v]
                    on[v] = cand if cur_on is None else _iv_min([cur_on, cand])
                else:
                    cur_dev = dev[v]
                    dev[v] = cand if cur_dev is None else _iv_min([cur_dev, cand])
            dev_u = dev[u]
            if dev_u is not None:
                cand = dev_u + wp
                cur_dev2 = dev[v]
                dev[v] = cand if cur_dev2 is None else _iv_min([cur_dev2, cand])

    winner_cost = Interval.point(sum(w_of(u, v) for (u, v) in win_edges))
    offset = winner_cost + Interval.point(float(eps) * len(win_edges))
    dev_sink = dev[dag.sink]
    margin = _INF if dev_sink is None else dev_sink - offset  # no competitor -> unique decode
    return DAGDecodingCertificate(
        certified=margin.lo > 0.0,
        winner=tuple(int(v) for v in winner),
        eps=float(eps),
        margin=margin,
        num_nodes=int(dag.num_nodes),
        num_edges=int(len(dag.edges)),
    )

Related APIsomnibias.struct.decode.DAGDecodingCertificate↗omnibias.struct.shortest_path↗

FUNCTION

check_dag_decoding_certificate

omnibias.struct.decode.check_dag_decoding_certificateSource ↗

check_dag_decoding_certificate(cert: DAGDecodingCertificate, *, meta: dict[str, Any] | None=None, timeout: float=600.0, start: Path | None=None) -> DAGDecodingProofVerdict

Seal a DAGDecodingCertificate and run the Lean-kernel bridge on it.

theorem_prover_verified is set only on a real kernel pass; with no Lean toolchain the bridge degrades gracefully, so this is safe in normal CI.

Parameters

Name	Type & default	Contract
certpositional-or-keyword	DAGDecodingCertificateRequired	See the operation contract and implementation below.
metakeyword-only	dict[str, Any] | NoneDefault: None	See the operation contract and implementation below.
timeoutkeyword-only	floatDefault: 600.0	See the operation contract and implementation below.
startkeyword-only	Path | NoneDefault: None	See the operation contract and implementation below.

ReturnsDAGDecodingProofVerdict

Executed regression · dag seal is digest verifiable and lean bridge is honest

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_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    cert = certify_decoding_dag(_DIAMOND_EDGES, _DIAMOND, eps=0.1)
    sealed = seal_dag_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_dag_decoding_certificate(cert)
    assert verdict.sealed_ok
    assert verdict.obligation_generated
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Regression example · seal is digest verifiable and lean bridge 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_seal_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.2)
    sealed = seal_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_decoding_certificate(cert)
    assert verdict.sealed_ok  # tamper-evident digest matches
    assert verdict.obligation_generated  # margin.lo > 0 -> enclosed_quantity_pos
    # theorem_prover_verified is exactly the (real) lake verdict -- never forged.
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest packages/omnibias-struct/tests/test_decode.py -k test_seal_is_digest_verifiable_and_lean_bridge_is_honest -q

Read the implementation

def check_dag_decoding_certificate(
    cert: DAGDecodingCertificate,
    *,
    meta: dict[str, Any] | None = None,
    timeout: float = 600.0,
    start: Path | None = None,
) -> DAGDecodingProofVerdict:
    r"""Seal a :class:`DAGDecodingCertificate` and run the Lean-kernel bridge on it.

    ``theorem_prover_verified`` is set only on a real kernel pass; with no Lean toolchain the
    bridge degrades gracefully, so this is safe in normal CI.
    """
    sealed = seal_dag_decoding_certificate(cert, meta=meta)
    obligation = generate_obligation(sealed)
    lean = check_certificate(sealed, timeout=timeout, start=start)
    return DAGDecodingProofVerdict(sealed, cert, obligation, lean)

Related APIsomnibias.core.proof.check_certificate↗omnibias.core.proof.generate_obligation↗omnibias.struct.decode.DAGDecodingProofVerdict↗omnibias.struct.decode.seal_dag_decoding_certificate↗

FUNCTION

check_decoding_certificate

omnibias.struct.decode.check_decoding_certificateSource ↗

check_decoding_certificate(cert: DecodingCertificate, *, meta: dict[str, Any] | None=None, timeout: float=600.0, start: Path | None=None) -> DecodingProofVerdict

Seal a DecodingCertificate and run the Lean-kernel bridge on it.

theorem_prover_verified is set only on a real kernel pass; with no Lean toolchain the bridge degrades gracefully (lean.available is False), so this is safe in normal CI.

Parameters

Name	Type & default	Contract
certpositional-or-keyword	DecodingCertificateRequired	See the operation contract and implementation below.
metakeyword-only	dict[str, Any] | NoneDefault: None	See the operation contract and implementation below.
timeoutkeyword-only	floatDefault: 600.0	See the operation contract and implementation below.
startkeyword-only	Path | NoneDefault: None	See the operation contract and implementation below.

ReturnsDecodingProofVerdict

Executed regression · seal is digest verifiable and lean bridge is honest

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_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.2)
    sealed = seal_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_decoding_certificate(cert)
    assert verdict.sealed_ok  # tamper-evident digest matches
    assert verdict.obligation_generated  # margin.lo > 0 -> enclosed_quantity_pos
    # theorem_prover_verified is exactly the (real) lake verdict -- never forged.
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Read the implementation

def check_decoding_certificate(
    cert: DecodingCertificate,
    *,
    meta: dict[str, Any] | None = None,
    timeout: float = 600.0,
    start: Path | None = None,
) -> DecodingProofVerdict:
    r"""Seal a :class:`DecodingCertificate` and run the Lean-kernel bridge on it.

    ``theorem_prover_verified`` is set only on a real kernel pass; with no Lean toolchain the
    bridge degrades gracefully (``lean.available is False``), so this is safe in normal CI.
    """
    sealed = seal_decoding_certificate(cert, meta=meta)
    obligation = generate_obligation(sealed)
    lean = check_certificate(sealed, timeout=timeout, start=start)
    return DecodingProofVerdict(sealed, cert, obligation, lean)

Related APIsomnibias.core.proof.check_certificate↗omnibias.core.proof.generate_obligation↗omnibias.struct.decode.DecodingProofVerdict↗omnibias.struct.decode.seal_decoding_certificate↗

FUNCTION

seal_dag_decoding_certificate

omnibias.struct.decode.seal_dag_decoding_certificateSource ↗

seal_dag_decoding_certificate(cert: DAGDecodingCertificate, *, meta: dict[str, Any] | None=None) -> Cert

Seal a DAGDecodingCertificate as a tamper-evident v1 interval certificate.

Mirrors seal_decoding_certificate: the sealed payload is the worst-case margin interval, which the Lean bridge turns into the finite enclosed_quantity_pos obligation when margin.lo > 0. Honesty flags fix unproven_claim=False and record local_box.

Parameters

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

ReturnsCert

Executed regression · dag seal is digest verifiable and lean bridge is honest

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_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    cert = certify_decoding_dag(_DIAMOND_EDGES, _DIAMOND, eps=0.1)
    sealed = seal_dag_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_dag_decoding_certificate(cert)
    assert verdict.sealed_ok
    assert verdict.obligation_generated
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_dag_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Regression example · seal is digest verifiable and lean bridge 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_seal_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.2)
    sealed = seal_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_decoding_certificate(cert)
    assert verdict.sealed_ok  # tamper-evident digest matches
    assert verdict.obligation_generated  # margin.lo > 0 -> enclosed_quantity_pos
    # theorem_prover_verified is exactly the (real) lake verdict -- never forged.
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest packages/omnibias-struct/tests/test_decode.py -k test_seal_is_digest_verifiable_and_lean_bridge_is_honest -q

Read the implementation

def seal_dag_decoding_certificate(
    cert: DAGDecodingCertificate, *, meta: dict[str, Any] | None = None
) -> Cert:
    r"""Seal a :class:`DAGDecodingCertificate` as a tamper-evident v1 interval certificate.

    Mirrors :func:`seal_decoding_certificate`: the sealed payload is the worst-case margin
    interval, which the Lean bridge turns into the finite ``enclosed_quantity_pos`` obligation
    when ``margin.lo > 0``. Honesty flags fix ``unproven_claim=False`` and record ``local_box``.
    """
    claim = (
        f"DAG shortest-path decode {cert.winner} is the unique argmin over the edge "
        f"L_inf ball of radius {cert.eps!r}: worst-case margin in "
        f"[{cert.margin.lo!r}, {cert.margin.hi!r}]"
    )
    payload_meta: dict[str, Any] = {
        "winner": list(cert.winner),
        "eps": cert.eps,
        "num_nodes": cert.num_nodes,
        "num_edges": cert.num_edges,
        "scope": "local_box",
        "label": "interval (outward-rounded reduced min-plus deviation margin; tight)",
    }
    if meta:
        payload_meta.update(meta)
    return interval_certificate(
        claim, cert.margin, honesty={"unproven_claim": False, "local_box": True}, meta=payload_meta
    )

Related APIsomnibias.core.proof.interval_certificate↗

FUNCTION

seal_decoding_certificate

omnibias.struct.decode.seal_decoding_certificateSource ↗

seal_decoding_certificate(cert: DecodingCertificate, *, meta: dict[str, Any] | None=None) -> Cert

Seal a DecodingCertificate as a tamper-evident v1 interval certificate.

The sealed payload is the worst-case margin interval; when margin.lo > 0 the Lean bridge turns it into the finite enclosed_quantity_pos obligation. Honesty flags fix unproven_claim=False and record the local_box scope (the omnibias convention).

Parameters

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

ReturnsCert

Executed regression · seal is digest verifiable and lean bridge is honest

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_is_digest_verifiable_and_lean_bridge_is_honest() -> None:
    emis = np.array([[3.0, 0.0], [0.0, 3.0], [3.0, 0.0]])
    trans = np.array([[1.0, 0.0], [0.0, 1.0]])
    cert = certify_decoding(emis, trans, eps=0.2)
    sealed = seal_decoding_certificate(cert)
    assert sealed["honesty"]["unproven_claim"] is False
    verdict = check_decoding_certificate(cert)
    assert verdict.sealed_ok  # tamper-evident digest matches
    assert verdict.obligation_generated  # margin.lo > 0 -> enclosed_quantity_pos
    # theorem_prover_verified is exactly the (real) lake verdict -- never forged.
    assert verdict.theorem_prover_verified == verdict.lean.verified
    if not verdict.lean.available:
        assert verdict.theorem_prover_verified is False

python -m pytest "packages/omnibias-struct/tests/test_decode.py::test_seal_is_digest_verifiable_and_lean_bridge_is_honest" -q

Read the implementation

def seal_decoding_certificate(cert: DecodingCertificate, *, meta: dict[str, Any] | None = None) -> Cert:
    r"""Seal a :class:`DecodingCertificate` as a tamper-evident v1 interval certificate.

    The sealed payload is the worst-case margin interval; when ``margin.lo > 0`` the Lean
    bridge turns it into the finite ``enclosed_quantity_pos`` obligation. Honesty flags fix
    ``unproven_claim=False`` and record the ``local_box`` scope (the omnibias convention).
    """
    claim = (
        f"Viterbi decode {cert.winner} is the unique argmax over the emission "
        f"L_inf ball of radius {cert.eps!r}: worst-case margin in "
        f"[{cert.margin.lo!r}, {cert.margin.hi!r}]"
    )
    payload_meta: dict[str, Any] = {
        "winner": list(cert.winner),
        "eps": cert.eps,
        "n_steps": cert.n_steps,
        "n_states": cert.n_states,
        "scope": "local_box",
        "label": "interval (outward-rounded reduced min-plus margin; tight)",
    }
    if meta:
        payload_meta.update(meta)
    return interval_certificate(
        claim, cert.margin, honesty={"unproven_claim": False, "local_box": True}, meta=payload_meta
    )

Related APIsomnibias.core.proof.interval_certificate↗

← Package overviewRunnable learning examples →