Skip to main content
API REFERENCE/omnibias-core

omnibias.core.proof.replay

0.5.0rc1Release candidatePython >=3.10Apache-2.0

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

import omnibias.core.proof.replay
Module contract & mathematical conventions

Finite straight-line replay traces + domain-subdivision coverage (phase1-lean-replay).

Two small, additive, **opt-in** capabilities that let the Lean kernel (formal/omnibias-verified-kernel) genuinely re-derive a piece of an ~omnibias.core.verified.interval.Interval computation, instead of merely trusting a Python-reported conclusion:

  • ReplayTrace (built by ReplayRecorder) -- an ordered, serializable intermediate representation of a straight-line program over the Interval primitives literal / sub / mul. This is **not** a speculative universal IR: it covers exactly the vocabulary the one instrumented call site in this module (record_ldlt_diagonal_trace) needs. Adding add / div / sqrt / reciprocal replay support is future work, gated on a concrete call site and a matching ZInterval kernel lemma -- see Omnibias/Replay.lean.
  • DomainSubdivisionCertificate -- the finite list of leaf boxes a branch-and-bound / bisection search actually visited, plus a ~DomainSubdivisionCertificate.covers_no_gaps combinatorial check that they tile the claimed starting domain edge-to-edge.

Recording is a pure **side channel**: ReplayRecorder and record_ldlt_diagonal_trace are new, independent code paths that do not import, call, wrap, or otherwise alter omnibias.core.verified.eig_operator. No existing function's signature, default behavior, or return value changes because this module exists; a caller who never constructs a ReplayRecorder is unaffected.

omnibias.core.proof.lean_check extends its existing obligation dispatch to recognize the interval_replay_trace and domain_subdivision payload shapes emitted here (ReplayTrace.to_payload, DomainSubdivisionCertificate.to_payload) and emits a Lean obligation against the generic, reusable checkers in Omnibias/Replay.lean / Omnibias/Subdivision.lean. theorem_prover_verified is earned only by that genuine lake build; this module never sets it itself.

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

DomainSubdivisionCertificate​

omnibias.core.proof.DomainSubdivisionCertificateSource ↗
class DomainSubdivisionCertificate

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.

Finite coverage certificate for a branch-and-bound leaf list.

resolution fixes the common integer denominator for [0, resolution]; leaves is the list of visited leaves **in the order they must tile the domain** (sorted by lo; the caller is responsible for that ordering, since visitation order in a real branch-and-bound search need not match left-to-right order).

covers_no_gaps exactly mirrors the combinatorics of Omnibias.Subdivision.coversNoGaps in formal/omnibias-verified-kernel, so Python and Lean agree by construction, not by coincidence -- but it is a convenience self-check only. The authoritative gate is the emitted Lean obligation (coversNoGaps ... := by decide), genuinely re-derived by the Lean kernel; omnibias.core.proof.lean_check additionally refuses to emit that obligation at all when this Python-side check already fails, exactly like the existing positive-definite-pivot and poisedness obligations gate on a Python-side truth check before asking Lean to re-derive it.

Parameters

NameType & defaultContract
resolutiondataclass fieldintRequiredSee the operation contract and implementation below.
leavesdataclass fieldtuple[SubdivisionLeaf, ...]RequiredSee the operation contract and implementation below.
Executed regression · domain subdivision covers no gaps false cases

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_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::test_domain_subdivision_covers_no_gaps_false_cases[leaves0-10]" -q
Regression example · domain subdivision covers no gaps true for a clean partition

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_true_for_a_clean_partition() -> None:
    leaves = (
        SubdivisionLeaf(0, 4, "count_below(1/4) == 0"),
        SubdivisionLeaf(4, 10, "count_below(1/2) == 1"),
        SubdivisionLeaf(10, 16, "count_below(1) == 2"),
    )
    cert = DomainSubdivisionCertificate(resolution=16, leaves=leaves)
    assert cert.covers_no_gaps() is True
python -m pytest packages/omnibias-core/tests/test_replay.py -k test_domain_subdivision_covers_no_gaps_true_for_a_clean_partition -q

Fields & methods

resolutionfield
resolution: int

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

View source ↗
leavesfield
leaves: tuple[SubdivisionLeaf, ...]

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

View source ↗
__post_init__method
__post_init__(self) -> None

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

Returns: None

Validation & failure cases
  • When self.resolution <= 0, raises ValueError('resolution must be positive').
  • When not self.leaves, raises ValueError('DomainSubdivisionCertificate requires at least one leaf').
Executed regression · domain subdivision covers no gaps false cases

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_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::test_domain_subdivision_covers_no_gaps_false_cases[leaves0-10]" -q
Method implementation
    def __post_init__(self) -> None:
        if self.resolution <= 0:
            raise ValueError("resolution must be positive")
        if not self.leaves:
            raise ValueError("DomainSubdivisionCertificate requires at least one leaf")
View source ↗
covers_no_gapsmethod
covers_no_gaps(self) -> bool

True iff the leaves tile [0, resolution] edge-to-edge: the first leaf starts at 0, each leaf starts exactly where the previous one ended, and the last leaf ends at resolution.

Returns: bool

Executed regression · domain subdivision covers no gaps false cases

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_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::test_domain_subdivision_covers_no_gaps_false_cases[leaves0-10]" -q
Method implementation
    def covers_no_gaps(self) -> bool:
        """``True`` iff the leaves tile ``[0, resolution]`` edge-to-edge:
        the first leaf starts at ``0``, each leaf starts exactly where the
        previous one ended, and the last leaf ends at ``resolution``."""
        first = self.leaves[0]
        if first.lo != 0:
            return False
        prev_hi = first.lo
        for leaf in self.leaves:
            if leaf.lo != prev_hi:
                return False
            prev_hi = leaf.hi
        return prev_hi == self.resolution
View source ↗
to_payloadmethod
to_payload(self) -> dict[str, object]

The domain_subdivision certificate payload omnibias.core.proof.lean_check dispatches on.

Returns: dict[str, object]

Executed regression · generate domain subdivision obligation contains expected 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_generate_domain_subdivision_obligation_contains_expected_lean() -> None:
    leaves = (SubdivisionLeaf(0, 4, "a"), SubdivisionLeaf(4, 10, "b"))
    subdivision = DomainSubdivisionCertificate(resolution=10, leaves=leaves)
    cert = make_certificate(claim="bisection coverage", payload=subdivision.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Subdivision" in src
    assert "Omnibias.Subdivision.coversNoGaps" in src
    assert "by decide" in src
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_domain_subdivision_obligation_contains_expected_lean" -q
Method implementation
    def to_payload(self) -> dict[str, object]:
        """The ``domain_subdivision`` certificate payload
        :mod:`omnibias.core.proof.lean_check` dispatches on."""
        return {
            "type": "domain_subdivision",
            "resolution": self.resolution,
            "leaves": [
                {"lo": leaf.lo, "hi": leaf.hi, "conclusion": leaf.conclusion} for leaf in self.leaves
            ],
        }
View source ↗
Read the implementation
class DomainSubdivisionCertificate:
    """Finite coverage certificate for a branch-and-bound leaf list.

    ``resolution`` fixes the common integer denominator for
    ``[0, resolution]``; ``leaves`` is the list of visited leaves **in the
    order they must tile the domain** (sorted by ``lo``; the caller is
    responsible for that ordering, since visitation order in a real
    branch-and-bound search need not match left-to-right order).

    :meth:`covers_no_gaps` exactly mirrors the combinatorics of
    ``Omnibias.Subdivision.coversNoGaps`` in
    ``formal/omnibias-verified-kernel``, so Python and Lean agree by
    construction, not by coincidence -- but it is a convenience self-check
    only. The authoritative gate is the emitted Lean obligation
    (``coversNoGaps ... := by decide``), genuinely re-derived by the Lean
    kernel; :mod:`omnibias.core.proof.lean_check` additionally refuses to
    emit that obligation at all when this Python-side check already fails,
    exactly like the existing positive-definite-pivot and poisedness
    obligations gate on a Python-side truth check before asking Lean to
    re-derive it.
    """

    resolution: int
    leaves: tuple[SubdivisionLeaf, ...]

    def __post_init__(self) -> None:
        if self.resolution <= 0:
            raise ValueError("resolution must be positive")
        if not self.leaves:
            raise ValueError("DomainSubdivisionCertificate requires at least one leaf")

    def covers_no_gaps(self) -> bool:
        """``True`` iff the leaves tile ``[0, resolution]`` edge-to-edge:
        the first leaf starts at ``0``, each leaf starts exactly where the
        previous one ended, and the last leaf ends at ``resolution``."""
        first = self.leaves[0]
        if first.lo != 0:
            return False
        prev_hi = first.lo
        for leaf in self.leaves:
            if leaf.lo != prev_hi:
                return False
            prev_hi = leaf.hi
        return prev_hi == self.resolution

    def to_payload(self) -> dict[str, object]:
        """The ``domain_subdivision`` certificate payload
        :mod:`omnibias.core.proof.lean_check` dispatches on."""
        return {
            "type": "domain_subdivision",
            "resolution": self.resolution,
            "leaves": [
                {"lo": leaf.lo, "hi": leaf.hi, "conclusion": leaf.conclusion} for leaf in self.leaves
            ],
        }
Other public import paths
  • omnibias.core.proof.DomainSubdivisionCertificate
  • omnibias.core.proof.replay.DomainSubdivisionCertificate
CONSTANT

Matrix​

omnibias.core.proof.replay.MatrixSource ↗
Matrix = Sequence[Sequence[IntervalLike]]

A symmetric matrix of interval-like entries, as accepted by func:record_ldlt_diagonal_trace (mirrors eig_operator.Matrix).

Read the implementation
Matrix = Sequence[Sequence[IntervalLike]]
CLASS

ReplayCertificateReport​

omnibias.core.proof.ReplayCertificateReportSource ↗
class ReplayCertificateReport

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 certificate plus the Lean-kernel verdict for one replay-style obligation (an ReplayTrace or a DomainSubdivisionCertificate).

theorem_prover_verified reuses the exact flag every other omnibias certificate kind earns from omnibias.core.proof.lean_check.check_certificate -- it means the same thing here as everywhere else: a genuine lake build re-checked this certificate's finite obligation and accepted it. It is False whenever the Lean toolchain is unavailable or the kernel rejected the obligation; this module never sets it itself.

Parameters

NameType & defaultContract
certificatedataclass fielddict[str, Any]RequiredSee the operation contract and implementation below.
theorem_prover_verifieddataclass fieldboolRequiredSee the operation contract and implementation below.
leandataclass fieldLeanCheckResult | NoneRequiredSee the operation contract and implementation below.

Fields & methods

certificatefield
certificate: dict[str, Any]

Declared dict[str, Any] field on ReplayCertificateReport. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗
theorem_prover_verifiedfield
theorem_prover_verified: bool

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

View source ↗
leanfield
lean: LeanCheckResult | None

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

View source ↗
Read the implementation
class ReplayCertificateReport:
    """A sealed certificate plus the Lean-kernel verdict for one replay-style
    obligation (an :class:`ReplayTrace` or a :class:`DomainSubdivisionCertificate`).

    ``theorem_prover_verified`` reuses the exact flag every other omnibias
    certificate kind earns from :func:`omnibias.core.proof.lean_check.check_certificate`
    -- it means the same thing here as everywhere else: a genuine ``lake
    build`` re-checked this certificate's finite obligation and accepted
    it. It is ``False`` whenever the Lean toolchain is unavailable or the
    kernel rejected the obligation; this module never sets it itself.
    """

    certificate: dict[str, Any]
    theorem_prover_verified: bool
    lean: LeanCheckResult | None
Other public import paths
  • omnibias.core.proof.ReplayCertificateReport
  • omnibias.core.proof.replay.ReplayCertificateReport
CONSTANT

ReplayOp​

omnibias.core.proof.replay.ReplayOpSource ↗
ReplayOp = Literal['literal', 'sub', 'mul']

The replay-trace operation vocabulary this module supports. Scoped to exactly what record_ldlt_diagonal_trace needs -- see the module docstring for why this is intentionally not a bigger universal IR.

Read the implementation
ReplayOp = Literal["literal", "sub", "mul"]
CLASS

ReplayRecorder​

omnibias.core.proof.ReplayRecorderSource ↗
class ReplayRecorder

Append-only, opt-in recorder of Interval primitive operations.

Instantiate one per run, feed it operands the caller already has (as prior step indices from literal / sub / mul), and call trace at the end. The recorder does not intercept, wrap, or monkeypatch any existing function -- it is a plain object a caller opts into using; a caller that never constructs one changes no behavior for anyone else.

Every arithmetic method calls the real Interval operator (never a reimplementation), so the recorded endpoints are bit-for-bit identical to what an uninstrumented computation would have produced.

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q

Fields & methods

__init__method
__init__(self) -> None

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

Returns: None

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def __init__(self) -> None:
        self._steps: list[ReplayStep] = []
View source ↗
__len__method
__len__(self) -> int

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

Returns: int

Method implementation
    def __len__(self) -> int:
        return len(self._steps)
View source ↗
valuemethod
value(self, index: int) -> Interval

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

Parameters

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

Returns: Interval

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def value(self, index: int) -> Interval:
        return self._steps[index].value()
View source ↗
literalmethod
literal(self, value: IntervalLike) -> int

Record a trusted input (a matrix entry, or a value derived by an operation outside this trace's vocabulary, e.g. reciprocal).

Parameters

NameType & defaultContract
valuepositional-or-keywordIntervalLikeRequiredSee the operation contract and implementation below.

Returns: int

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def literal(self, value: IntervalLike) -> int:
        """Record a trusted input (a matrix entry, or a value derived by an
        operation outside this trace's vocabulary, e.g. ``reciprocal``)."""
        iv = Interval.from_value(value)
        self._steps.append(ReplayStep("literal", (), iv.lo, iv.hi))
        return len(self._steps) - 1
View source ↗
submethod
sub(self, a: int, b: int) -> int

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

Parameters

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

Returns: int

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def sub(self, a: int, b: int) -> int:
        result = self.value(a) - self.value(b)
        self._steps.append(ReplayStep("sub", (a, b), result.lo, result.hi))
        return len(self._steps) - 1
View source ↗
mulmethod
mul(self, a: int, b: int) -> int

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

Parameters

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

Returns: int

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def mul(self, a: int, b: int) -> int:
        result = self.value(a) * self.value(b)
        self._steps.append(ReplayStep("mul", (a, b), result.lo, result.hi))
        return len(self._steps) - 1
View source ↗
tracemethod
trace(self, conclusions: Sequence[int]=()) -> ReplayTrace

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

Parameters

NameType & defaultContract
conclusionspositional-or-keywordSequence[int]Default: ()See the operation contract and implementation below.

Returns: ReplayTrace

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def trace(self, conclusions: Sequence[int] = ()) -> ReplayTrace:
        return ReplayTrace(tuple(self._steps), tuple(conclusions))
View source ↗
Read the implementation
class ReplayRecorder:
    """Append-only, opt-in recorder of ``Interval`` primitive operations.

    Instantiate one per run, feed it operands the caller already has (as
    prior step indices from :meth:`literal` / :meth:`sub` / :meth:`mul`),
    and call :meth:`trace` at the end. The recorder does not intercept,
    wrap, or monkeypatch any existing function -- it is a plain object a
    caller opts into using; a caller that never constructs one changes no
    behavior for anyone else.

    Every arithmetic method calls the real ``Interval`` operator (never a
    reimplementation), so the recorded endpoints are bit-for-bit identical
    to what an uninstrumented computation would have produced.
    """

    def __init__(self) -> None:
        self._steps: list[ReplayStep] = []

    def __len__(self) -> int:
        return len(self._steps)

    def value(self, index: int) -> Interval:
        return self._steps[index].value()

    def literal(self, value: IntervalLike) -> int:
        """Record a trusted input (a matrix entry, or a value derived by an
        operation outside this trace's vocabulary, e.g. ``reciprocal``)."""
        iv = Interval.from_value(value)
        self._steps.append(ReplayStep("literal", (), iv.lo, iv.hi))
        return len(self._steps) - 1

    def sub(self, a: int, b: int) -> int:
        result = self.value(a) - self.value(b)
        self._steps.append(ReplayStep("sub", (a, b), result.lo, result.hi))
        return len(self._steps) - 1

    def mul(self, a: int, b: int) -> int:
        result = self.value(a) * self.value(b)
        self._steps.append(ReplayStep("mul", (a, b), result.lo, result.hi))
        return len(self._steps) - 1

    def trace(self, conclusions: Sequence[int] = ()) -> ReplayTrace:
        return ReplayTrace(tuple(self._steps), tuple(conclusions))
Related APIsomnibias.core.proof.ReplayStep↗omnibias.core.proof.ReplayTrace↗
Other public import paths
  • omnibias.core.proof.ReplayRecorder
  • omnibias.core.proof.replay.ReplayRecorder
CLASS

ReplayStep​

omnibias.core.proof.ReplayStepSource ↗
class ReplayStep

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.

One step of a straight-line Interval derivation.

op is "literal" (a trusted input, not derived from any prior step -- args is empty), "sub", or "mul" (each with exactly two prior-step indices in args). lo/hi are the *actual* Interval endpoints Python computed for this step: this dataclass only records what already happened, it never recomputes or re-derives anything itself.

Parameters

NameType & defaultContract
opdataclass fieldReplayOpRequiredSee the operation contract and implementation below.
argsdataclass fieldtuple[int, ...]RequiredSee the operation contract and implementation below.
lodataclass fieldfloatRequiredSee the operation contract and implementation below.
hidataclass fieldfloatRequiredSee the operation contract and implementation below.
Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Regression example · replay trace structural validation

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_replay_trace_structural_validation() -> None:
    with pytest.raises(ValueError, match="non-prior index"):
        ReplayTrace((ReplayStep("sub", (0, 1), 0.0, 1.0),))
    with pytest.raises(ValueError, match="expects 0 operand"):
        ReplayStep("literal", (1,), 0.0, 1.0)
    with pytest.raises(ValueError, match="expects 2 operand"):
        ReplayStep("mul", (0,), 0.0, 1.0)
    with pytest.raises(ValueError, match="unsupported replay op"):
        ReplayStep("div", (), 0.0, 1.0)  # type: ignore[arg-type]
    with pytest.raises(ValueError):
        ReplayTrace(())  # at least one step required
    with pytest.raises(ValueError, match="out of range"):
        ReplayTrace((ReplayStep("literal", (), 0.0, 1.0),), conclusions=(5,))
python -m pytest packages/omnibias-core/tests/test_replay.py -k test_replay_trace_structural_validation -q

Fields & methods

opfield
op: ReplayOp

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

View source ↗
argsfield
args: tuple[int, ...]

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

View source ↗
lofield
lo: float

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

View source ↗
hifield
hi: float

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

View source ↗
__post_init__method
__post_init__(self) -> None

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

Returns: None

Validation & failure cases
  • When self.op not in _REPLAY_OPS, raises ValueError(f'unsupported replay op {self.op!r}; expected one of {sorted(_REPLAY_OPS)}').
  • When len(self.args) != want, raises ValueError(f'{self.op!r} step expects {want} operand indices, got {len(self.args)}').
  • When self.lo > self.hi, raises ValueError(f'empty recorded interval: lo={self.lo!r} > hi={self.hi!r}').
Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def __post_init__(self) -> None:
        if self.op not in _REPLAY_OPS:
            raise ValueError(f"unsupported replay op {self.op!r}; expected one of {sorted(_REPLAY_OPS)}")
        want = 0 if self.op == "literal" else 2
        if len(self.args) != want:
            raise ValueError(f"{self.op!r} step expects {want} operand indices, got {len(self.args)}")
        if self.lo > self.hi:
            raise ValueError(f"empty recorded interval: lo={self.lo!r} > hi={self.hi!r}")
View source ↗
valuemethod
value(self) -> Interval

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

Returns: Interval

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def value(self) -> Interval:
        return Interval(self.lo, self.hi)
View source ↗
to_jsonmethod
to_json(self) -> dict[str, object]

A JSON-safe dict using the repository's float.hex() convention for exact endpoint serialization (matching omnibias.core.proof.certificate).

Returns: dict[str, object]

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def to_json(self) -> dict[str, object]:
        """A JSON-safe dict using the repository's ``float.hex()`` convention
        for exact endpoint serialization (matching
        :mod:`omnibias.core.proof.certificate`)."""
        return {
            "op": self.op,
            "args": list(self.args),
            "lo": float(self.lo).hex(),
            "hi": float(self.hi).hex(),
        }
View source ↗
Read the implementation
class ReplayStep:
    """One step of a straight-line ``Interval`` derivation.

    ``op`` is ``"literal"`` (a trusted input, not derived from any prior
    step -- ``args`` is empty), ``"sub"``, or ``"mul"`` (each with exactly
    two prior-step indices in ``args``). ``lo``/``hi`` are the *actual*
    ``Interval`` endpoints Python computed for this step: this dataclass
    only records what already happened, it never recomputes or re-derives
    anything itself.
    """

    op: ReplayOp
    args: tuple[int, ...]
    lo: float
    hi: float

    def __post_init__(self) -> None:
        if self.op not in _REPLAY_OPS:
            raise ValueError(f"unsupported replay op {self.op!r}; expected one of {sorted(_REPLAY_OPS)}")
        want = 0 if self.op == "literal" else 2
        if len(self.args) != want:
            raise ValueError(f"{self.op!r} step expects {want} operand indices, got {len(self.args)}")
        if self.lo > self.hi:
            raise ValueError(f"empty recorded interval: lo={self.lo!r} > hi={self.hi!r}")

    def value(self) -> Interval:
        return Interval(self.lo, self.hi)

    def to_json(self) -> dict[str, object]:
        """A JSON-safe dict using the repository's ``float.hex()`` convention
        for exact endpoint serialization (matching
        :mod:`omnibias.core.proof.certificate`)."""
        return {
            "op": self.op,
            "args": list(self.args),
            "lo": float(self.lo).hex(),
            "hi": float(self.hi).hex(),
        }
Related APIsomnibias.core.verified.Interval↗
Other public import paths
  • omnibias.core.proof.ReplayStep
  • omnibias.core.proof.replay.ReplayStep
CLASS

ReplayTrace​

omnibias.core.proof.ReplayTraceSource ↗
class ReplayTrace

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 finite, ordered straight-line trace over Interval primitives.

steps[i].args may only index strictly earlier entries (< i), so the trace is a genuine straight-line program, safe to replay front-to-back with no forward references. conclusions names the subset of step indices that are the run's sound "answers" (e.g. each pivot D_jj) -- bookkeeping for callers and for the sealed certificate payload; it is not interpreted by the replay checker itself, which re-derives *every* sub/mul step regardless of whether it is a named conclusion.

Validation here is purely **structural** (well-formed shape, in-range operand indices): it does *not* check that any step's recorded envelope is the arithmetically correct composition of its operands. That is exactly what the emitted Lean obligation (Omnibias.Replay.replayOk ... := by decide) checks, genuinely, in the Lean kernel -- deliberately independent of this Python implementation.

Parameters

NameType & defaultContract
stepsdataclass fieldtuple[ReplayStep, ...]RequiredSee the operation contract and implementation below.
conclusionsdataclass fieldtuple[int, ...]Default: ()See the operation contract and implementation below.
Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Regression example · replay trace structural validation

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_replay_trace_structural_validation() -> None:
    with pytest.raises(ValueError, match="non-prior index"):
        ReplayTrace((ReplayStep("sub", (0, 1), 0.0, 1.0),))
    with pytest.raises(ValueError, match="expects 0 operand"):
        ReplayStep("literal", (1,), 0.0, 1.0)
    with pytest.raises(ValueError, match="expects 2 operand"):
        ReplayStep("mul", (0,), 0.0, 1.0)
    with pytest.raises(ValueError, match="unsupported replay op"):
        ReplayStep("div", (), 0.0, 1.0)  # type: ignore[arg-type]
    with pytest.raises(ValueError):
        ReplayTrace(())  # at least one step required
    with pytest.raises(ValueError, match="out of range"):
        ReplayTrace((ReplayStep("literal", (), 0.0, 1.0),), conclusions=(5,))
python -m pytest packages/omnibias-core/tests/test_replay.py -k test_replay_trace_structural_validation -q

Fields & methods

stepsfield
steps: tuple[ReplayStep, ...]

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

View source ↗
conclusionsfield
conclusions: tuple[int, ...] = ()

Declared tuple[int, ...] field on ReplayTrace. Default expression: ().

View source ↗
__post_init__method
__post_init__(self) -> None

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

Returns: None

Validation & failure cases
  • When not self.steps, raises ValueError('ReplayTrace requires at least one step').
  • When not 0 <= a < i, raises ValueError(f'step {i} ({step.op!r}) references non-prior index {a}').
  • When not 0 <= c < n, raises ValueError(f'conclusion index {c} out of range [0, {n})').
Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def __post_init__(self) -> None:
        if not self.steps:
            raise ValueError("ReplayTrace requires at least one step")
        n = len(self.steps)
        for i, step in enumerate(self.steps):
            for a in step.args:
                if not (0 <= a < i):
                    raise ValueError(f"step {i} ({step.op!r}) references non-prior index {a}")
        for c in self.conclusions:
            if not (0 <= c < n):
                raise ValueError(f"conclusion index {c} out of range [0, {n})")
View source ↗
valuemethod
value(self, index: int) -> Interval

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

Parameters

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

Returns: Interval

Executed regression · record ldlt diagonal trace matches direct computation bit for bit

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_record_ldlt_diagonal_trace_matches_direct_computation_bit_for_bit() -> None:
    """Recording is a true no-op on the underlying arithmetic: the traced
    pivots are bit-for-bit identical to the uninstrumented
    ``interval_ldlt_pivots`` on the same input."""
    direct = interval_ldlt_pivots(_SPD_3X3)
    traced, trace = record_ldlt_diagonal_trace(_SPD_3X3)
    assert direct is not None and traced is not None
    assert len(direct) == len(traced) == 3
    for expected, got in zip(direct, traced, strict=True):
        assert expected.lo == got.lo
        assert expected.hi == got.hi
    # Every named conclusion's value matches the corresponding pivot.
    assert trace.conclusion_values() == traced
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_record_ldlt_diagonal_trace_matches_direct_computation_bit_for_bit" -q
Method implementation
    def value(self, index: int) -> Interval:
        return self.steps[index].value()
View source ↗
conclusion_valuesmethod
conclusion_values(self) -> tuple[Interval, ...]

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

Returns: tuple[Interval, ...]

Executed regression · record ldlt diagonal trace matches direct computation bit for bit

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_record_ldlt_diagonal_trace_matches_direct_computation_bit_for_bit() -> None:
    """Recording is a true no-op on the underlying arithmetic: the traced
    pivots are bit-for-bit identical to the uninstrumented
    ``interval_ldlt_pivots`` on the same input."""
    direct = interval_ldlt_pivots(_SPD_3X3)
    traced, trace = record_ldlt_diagonal_trace(_SPD_3X3)
    assert direct is not None and traced is not None
    assert len(direct) == len(traced) == 3
    for expected, got in zip(direct, traced, strict=True):
        assert expected.lo == got.lo
        assert expected.hi == got.hi
    # Every named conclusion's value matches the corresponding pivot.
    assert trace.conclusion_values() == traced
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_record_ldlt_diagonal_trace_matches_direct_computation_bit_for_bit" -q
Method implementation
    def conclusion_values(self) -> tuple[Interval, ...]:
        return tuple(self.value(i) for i in self.conclusions)
View source ↗
to_payloadmethod
to_payload(self) -> dict[str, object]

The interval_replay_trace certificate payload omnibias.core.proof.lean_check dispatches on.

Returns: dict[str, object]

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Method implementation
    def to_payload(self) -> dict[str, object]:
        """The ``interval_replay_trace`` certificate payload
        :mod:`omnibias.core.proof.lean_check` dispatches on."""
        return {
            "type": "interval_replay_trace",
            "steps": [s.to_json() for s in self.steps],
            "conclusions": list(self.conclusions),
        }
View source ↗
Read the implementation
class ReplayTrace:
    """A finite, ordered straight-line trace over ``Interval`` primitives.

    ``steps[i].args`` may only index strictly earlier entries (``< i``), so
    the trace is a genuine straight-line program, safe to replay
    front-to-back with no forward references. ``conclusions`` names the
    subset of step indices that are the run's sound "answers" (e.g. each
    pivot ``D_jj``) -- bookkeeping for callers and for the sealed
    certificate payload; it is not interpreted by the replay checker
    itself, which re-derives *every* ``sub``/``mul`` step regardless of
    whether it is a named conclusion.

    Validation here is purely **structural** (well-formed shape, in-range
    operand indices): it does *not* check that any step's recorded
    envelope is the arithmetically correct composition of its operands.
    That is exactly what the emitted Lean obligation
    (``Omnibias.Replay.replayOk ... := by decide``) checks, genuinely, in
    the Lean kernel -- deliberately independent of this Python
    implementation.
    """

    steps: tuple[ReplayStep, ...]
    conclusions: tuple[int, ...] = ()

    def __post_init__(self) -> None:
        if not self.steps:
            raise ValueError("ReplayTrace requires at least one step")
        n = len(self.steps)
        for i, step in enumerate(self.steps):
            for a in step.args:
                if not (0 <= a < i):
                    raise ValueError(f"step {i} ({step.op!r}) references non-prior index {a}")
        for c in self.conclusions:
            if not (0 <= c < n):
                raise ValueError(f"conclusion index {c} out of range [0, {n})")

    def value(self, index: int) -> Interval:
        return self.steps[index].value()

    def conclusion_values(self) -> tuple[Interval, ...]:
        return tuple(self.value(i) for i in self.conclusions)

    def to_payload(self) -> dict[str, object]:
        """The ``interval_replay_trace`` certificate payload
        :mod:`omnibias.core.proof.lean_check` dispatches on."""
        return {
            "type": "interval_replay_trace",
            "steps": [s.to_json() for s in self.steps],
            "conclusions": list(self.conclusions),
        }
Other public import paths
  • omnibias.core.proof.ReplayTrace
  • omnibias.core.proof.replay.ReplayTrace
CLASS

SubdivisionLeaf​

omnibias.core.proof.SubdivisionLeafSource ↗
class SubdivisionLeaf

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.

One visited leaf of a branch-and-bound / bisection search.

lo/hi are integer sub-range boundaries of [0, resolution] (the box lo / resolution .. hi / resolution of the claimed starting domain, over the shared resolution of the enclosing DomainSubdivisionCertificate). conclusion is a short, human-readable label for whatever sound, per-leaf fact the search established there (e.g. "eigenvalue count below midpoint >= k"); it is not interpreted by the coverage check, which only verifies the leaves tile the domain with no gap.

Parameters

NameType & defaultContract
lodataclass fieldintRequiredSee the operation contract and implementation below.
hidataclass fieldintRequiredSee the operation contract and implementation below.
conclusiondataclass fieldstrDefault: ''See the operation contract and implementation below.
Executed regression · domain subdivision covers no gaps true for a clean partition

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_domain_subdivision_covers_no_gaps_true_for_a_clean_partition() -> None:
    leaves = (
        SubdivisionLeaf(0, 4, "count_below(1/4) == 0"),
        SubdivisionLeaf(4, 10, "count_below(1/2) == 1"),
        SubdivisionLeaf(10, 16, "count_below(1) == 2"),
    )
    cert = DomainSubdivisionCertificate(resolution=16, leaves=leaves)
    assert cert.covers_no_gaps() is True
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_domain_subdivision_covers_no_gaps_true_for_a_clean_partition" -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

Fields & methods

lofield
lo: int

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

View source ↗
hifield
hi: int

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

View source ↗
conclusionfield
conclusion: str = ''

Declared str field on SubdivisionLeaf. Default expression: ''.

View source ↗
__post_init__method
__post_init__(self) -> None

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

Returns: None

Validation & failure cases
  • When self.lo >= self.hi, raises ValueError(f'leaf must be non-empty: lo={self.lo} >= hi={self.hi}').
Executed regression · domain subdivision covers no gaps true for a clean partition

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_domain_subdivision_covers_no_gaps_true_for_a_clean_partition() -> None:
    leaves = (
        SubdivisionLeaf(0, 4, "count_below(1/4) == 0"),
        SubdivisionLeaf(4, 10, "count_below(1/2) == 1"),
        SubdivisionLeaf(10, 16, "count_below(1) == 2"),
    )
    cert = DomainSubdivisionCertificate(resolution=16, leaves=leaves)
    assert cert.covers_no_gaps() is True
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_domain_subdivision_covers_no_gaps_true_for_a_clean_partition" -q
Method implementation
    def __post_init__(self) -> None:
        if self.lo >= self.hi:
            raise ValueError(f"leaf must be non-empty: lo={self.lo} >= hi={self.hi}")
View source ↗
Read the implementation
class SubdivisionLeaf:
    """One visited leaf of a branch-and-bound / bisection search.

    ``lo``/``hi`` are integer sub-range boundaries of ``[0, resolution]``
    (the box ``lo / resolution .. hi / resolution`` of the claimed
    starting domain, over the shared ``resolution`` of the enclosing
    :class:`DomainSubdivisionCertificate`). ``conclusion`` is a short,
    human-readable label for whatever sound, per-leaf fact the search
    established there (e.g. ``"eigenvalue count below midpoint >= k"``);
    it is not interpreted by the coverage check, which only verifies the
    leaves tile the domain with no gap.
    """

    lo: int
    hi: int
    conclusion: str = ""

    def __post_init__(self) -> None:
        if self.lo >= self.hi:
            raise ValueError(f"leaf must be non-empty: lo={self.lo} >= hi={self.hi}")
Other public import paths
  • omnibias.core.proof.SubdivisionLeaf
  • omnibias.core.proof.replay.SubdivisionLeaf
FUNCTION

record_ldlt_diagonal_trace​

omnibias.core.proof.record_ldlt_diagonal_traceSource ↗
record_ldlt_diagonal_trace(matrix: Matrix) -> tuple[tuple[Interval, ...] | None, ReplayTrace]

Instrumented mirror of the pivot recurrence in omnibias.core.verified.eig_operator._ldlt_pivots, recording a ReplayTrace of every sub/mul step alongside each trusted literal input.

This is a **thin, independent copy** of that recurrence, not a wrapper around it: it does not import, call, or alter omnibias.core.verified.eig_operator in any way, so adding it can never change that module's behavior for any existing caller. It is verified (in tests/proof/test_replay.py) to reproduce interval_ldlt_pivots(matrix) bit-for-bit on the same input.

Trust boundary (mirrors the one Omnibias/LDLT.lean already documents for the division-bearing factorisation): the reciprocal 1 / D_jj needed for each off-diagonal L entry is *not* itself replayed -- ZInterval has no division -- so it is recorded as a trusted ~ReplayRecorder.literal, exactly like a raw matrix entry. Only the sub/mul steps of the diagonal-pivot and off-diagonal-factor recurrences are genuinely replayed by the Lean checker.

Returns (None, trace) as soon as a pivot interval straddles zero (mirroring _ldlt_pivots's own None early return -- the trace still records every step taken before that point), or (pivots, trace) with the full length-n pivot tuple.

Parameters

NameType & defaultContract
matrixpositional-or-keywordMatrixRequiredSee the operation contract and implementation below.
Returnstuple[tuple[Interval, ...] | None, ReplayTrace]
Explicit validation & failure cases
  • When n == 0, raises ValueError('matrix must be non-empty').
  • When len(row) != n, raises ValueError('matrix must be square').

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

Executed regression · generate replay obligation contains expected 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_generate_replay_obligation_contains_expected_lean() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_2X2)
    cert = make_certificate(claim="LDLT diagonal-pivot replay", payload=trace.to_payload())
    src = generate_obligation(cert)
    assert src is not None
    assert "import Omnibias.Replay" in src
    assert "Omnibias.Replay.replayOk" in src
    assert "by decide" in src
    assert src.count("⟨") == len(trace.steps)
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_generate_replay_obligation_contains_expected_lean" -q
Regression example · record ldlt diagonal trace is independent of eig operator

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_record_ldlt_diagonal_trace_is_independent_of_eig_operator() -> None:
    """Calling the instrumented recorder never touches, imports as a side
    effect, or otherwise perturbs ``eig_operator`` -- an uninstrumented call
    before and after recording returns the identical result."""
    before = interval_ldlt_pivots(_SPD_2X2)
    record_ldlt_diagonal_trace(_SPD_2X2)
    after = interval_ldlt_pivots(_SPD_2X2)
    assert before == after
python -m pytest packages/omnibias-core/tests/test_replay.py -k test_record_ldlt_diagonal_trace_is_independent_of_eig_operator -q
Read the implementation
def record_ldlt_diagonal_trace(matrix: Matrix) -> tuple[tuple[Interval, ...] | None, ReplayTrace]:
    r"""Instrumented mirror of the pivot recurrence in
    ``omnibias.core.verified.eig_operator._ldlt_pivots``, recording a
    :class:`ReplayTrace` of every ``sub``/``mul`` step alongside each
    trusted literal input.

    This is a **thin, independent copy** of that recurrence, not a wrapper
    around it: it does not import, call, or alter
    :mod:`omnibias.core.verified.eig_operator` in any way, so adding it can
    never change that module's behavior for any existing caller. It is
    verified (in ``tests/proof/test_replay.py``) to reproduce
    ``interval_ldlt_pivots(matrix)`` bit-for-bit on the same input.

    Trust boundary (mirrors the one ``Omnibias/LDLT.lean`` already
    documents for the division-bearing factorisation): the reciprocal
    ``1 / D_jj`` needed for each off-diagonal ``L`` entry is *not* itself
    replayed -- ``ZInterval`` has no division -- so it is recorded as a
    trusted :meth:`~ReplayRecorder.literal`, exactly like a raw matrix
    entry. Only the ``sub``/``mul`` steps of the diagonal-pivot and
    off-diagonal-factor recurrences are genuinely replayed by the Lean
    checker.

    Returns ``(None, trace)`` as soon as a pivot interval straddles zero
    (mirroring ``_ldlt_pivots``'s own ``None`` early return -- the trace
    still records every step taken before that point), or ``(pivots,
    trace)`` with the full length-``n`` pivot tuple.
    """
    rows = [[Interval.from_value(x) for x in row] for row in matrix]
    n = len(rows)
    if n == 0:
        raise ValueError("matrix must be non-empty")
    for row in rows:
        if len(row) != n:
            raise ValueError("matrix must be square")

    rec = ReplayRecorder()
    lmat: list[list[Interval]] = [[Interval.point(0.0) for _ in range(n)] for _ in range(n)]
    d: list[Interval] = [Interval.point(0.0) for _ in range(n)]
    l_index: list[list[int]] = [[-1] * n for _ in range(n)]
    d_index: list[int] = [-1] * n
    conclusions: list[int] = []

    for j in range(n):
        lmat[j][j] = Interval.point(1.0)
        dj = rows[j][j]
        dj_idx = rec.literal(dj)
        for k in range(j):
            sq_idx = rec.mul(l_index[j][k], l_index[j][k])
            term_idx = rec.mul(sq_idx, d_index[k])
            dj_idx = rec.sub(dj_idx, term_idx)
            dj = dj - lmat[j][k] * lmat[j][k] * d[k]
        if dj.lo <= 0.0 <= dj.hi:
            return None, rec.trace(tuple(conclusions))
        d[j] = dj
        d_index[j] = dj_idx
        conclusions.append(dj_idx)
        inv = dj.reciprocal()
        inv_idx = rec.literal(inv)
        for i in range(j + 1, n):
            lij = rows[i][j]
            lij_idx = rec.literal(lij)
            for k in range(j):
                sq_idx = rec.mul(l_index[i][k], l_index[j][k])
                term_idx = rec.mul(sq_idx, d_index[k])
                lij_idx = rec.sub(lij_idx, term_idx)
                lij = lij - lmat[i][k] * lmat[j][k] * d[k]
            final_idx = rec.mul(lij_idx, inv_idx)
            lmat[i][j] = lij * inv
            l_index[i][j] = final_idx

    return tuple(d), rec.trace(tuple(conclusions))
Related APIsomnibias.core.proof.ReplayRecorder↗
Other public import paths
  • omnibias.core.proof.record_ldlt_diagonal_trace
  • omnibias.core.proof.replay.record_ldlt_diagonal_trace
FUNCTION

seal_domain_subdivision_certificate​

omnibias.core.proof.seal_domain_subdivision_certificateSource ↗
seal_domain_subdivision_certificate(subdivision: DomainSubdivisionCertificate, *, claim: str, run_lean: bool=True) -> ReplayCertificateReport

Seal subdivision as a v1 certificate and, if requested, drive the Lean coverage checker (Omnibias.Subdivision.coversNoGaps).

Same graceful-degradation contract as seal_replay_certificate.

Parameters

NameType & defaultContract
subdivisionpositional-or-keywordDomainSubdivisionCertificateRequiredSee the operation contract and implementation below.
claimkeyword-onlystrRequiredSee the operation contract and implementation below.
run_leankeyword-onlyboolDefault: TrueSee the operation contract and implementation below.
ReturnsReplayCertificateReport
Executed regression · domain subdivision certificate seal degrades gracefully

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_domain_subdivision_certificate_seal_degrades_gracefully() -> None:
    leaves = (
        SubdivisionLeaf(0, 4, "count_below(1/4) == 0"),
        SubdivisionLeaf(4, 10, "count_below(1/2) == 1"),
        SubdivisionLeaf(10, 16, "count_below(1) == 2"),
    )
    cert_obj = DomainSubdivisionCertificate(resolution=16, leaves=leaves)
    report = seal_domain_subdivision_certificate(
        cert_obj, claim="bisection leaves cover [0, 16] with no gap"
    )
    if lean_check_available():  # pragma: no cover - Lean-equipped environment only
        assert report.theorem_prover_verified is True
        assert report.lean is not None and report.lean.verified is True
    else:
        assert report.theorem_prover_verified is False
        assert report.lean is not None
        assert report.lean.available is False
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_domain_subdivision_certificate_seal_degrades_gracefully" -q
Regression example · replay certificate seal degrades gracefully

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_replay_certificate_seal_degrades_gracefully() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_3X3)
    report = seal_replay_certificate(
        trace, claim="LDLT diagonal-pivot recurrence replay for a 3x3 SPD matrix box"
    )
    assert verify_certificate_digest(report.certificate)
    assert "theorem_prover_verified" not in report.certificate.get("honesty", {})
    if lean_check_available():  # pragma: no cover - Lean-equipped environment only
        assert report.theorem_prover_verified is True
        assert report.lean is not None and report.lean.verified is True
    else:
        assert report.theorem_prover_verified is False
        assert report.lean is not None
        assert report.lean.available is False
python -m pytest packages/omnibias-core/tests/test_replay.py -k test_replay_certificate_seal_degrades_gracefully -q
Read the implementation
def seal_domain_subdivision_certificate(
    subdivision: DomainSubdivisionCertificate, *, claim: str, run_lean: bool = True
) -> ReplayCertificateReport:
    """Seal ``subdivision`` as a v1 certificate and, if requested, drive the
    Lean coverage checker (``Omnibias.Subdivision.coversNoGaps``).

    Same graceful-degradation contract as :func:`seal_replay_certificate`.
    """
    cert = make_certificate(claim=claim, payload=subdivision.to_payload())
    lean: LeanCheckResult | None = None
    verified = False
    if run_lean:
        lean = check_certificate(cert)
        verified = bool(lean.verified)
    return ReplayCertificateReport(certificate=cert, theorem_prover_verified=verified, lean=lean)
Related APIsomnibias.core.proof.make_certificate↗omnibias.core.proof.check_certificate↗omnibias.core.proof.ReplayCertificateReport↗
Other public import paths
  • omnibias.core.proof.seal_domain_subdivision_certificate
  • omnibias.core.proof.replay.seal_domain_subdivision_certificate
FUNCTION

seal_replay_certificate​

omnibias.core.proof.seal_replay_certificateSource ↗
seal_replay_certificate(trace: ReplayTrace, *, claim: str, run_lean: bool=True) -> ReplayCertificateReport

Seal trace as a v1 certificate and, if requested, drive the Lean replay checker (Omnibias.Replay.replayOk).

run_lean=False seals the certificate without invoking lake at all (useful for structural-only tests); run_lean=True (the default) calls omnibias.core.proof.lean_check.check_certificate, which itself degrades gracefully -- available=False, verified=False -- when no Lean toolchain is present, exactly like every other obligation kind.

Parameters

NameType & defaultContract
tracepositional-or-keywordReplayTraceRequiredSee the operation contract and implementation below.
claimkeyword-onlystrRequiredSee the operation contract and implementation below.
run_leankeyword-onlyboolDefault: TrueSee the operation contract and implementation below.
ReturnsReplayCertificateReport
Executed regression · replay certificate seal degrades gracefully

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_replay_certificate_seal_degrades_gracefully() -> None:
    _, trace = record_ldlt_diagonal_trace(_SPD_3X3)
    report = seal_replay_certificate(
        trace, claim="LDLT diagonal-pivot recurrence replay for a 3x3 SPD matrix box"
    )
    assert verify_certificate_digest(report.certificate)
    assert "theorem_prover_verified" not in report.certificate.get("honesty", {})
    if lean_check_available():  # pragma: no cover - Lean-equipped environment only
        assert report.theorem_prover_verified is True
        assert report.lean is not None and report.lean.verified is True
    else:
        assert report.theorem_prover_verified is False
        assert report.lean is not None
        assert report.lean.available is False
python -m pytest "packages/omnibias-core/tests/test_replay.py::test_replay_certificate_seal_degrades_gracefully" -q
Read the implementation
def seal_replay_certificate(
    trace: ReplayTrace, *, claim: str, run_lean: bool = True
) -> ReplayCertificateReport:
    """Seal ``trace`` as a v1 certificate and, if requested, drive the Lean
    replay checker (``Omnibias.Replay.replayOk``).

    ``run_lean=False`` seals the certificate without invoking ``lake`` at
    all (useful for structural-only tests); ``run_lean=True`` (the
    default) calls :func:`omnibias.core.proof.lean_check.check_certificate`,
    which itself degrades gracefully -- ``available=False``,
    ``verified=False`` -- when no Lean toolchain is present, exactly like
    every other obligation kind.
    """
    cert = make_certificate(claim=claim, payload=trace.to_payload())
    lean: LeanCheckResult | None = None
    verified = False
    if run_lean:
        lean = check_certificate(cert)
        verified = bool(lean.verified)
    return ReplayCertificateReport(certificate=cert, theorem_prover_verified=verified, lean=lean)
Related APIsomnibias.core.proof.make_certificate↗omnibias.core.proof.check_certificate↗omnibias.core.proof.ReplayCertificateReport↗
Other public import paths
  • omnibias.core.proof.seal_replay_certificate
  • omnibias.core.proof.replay.seal_replay_certificate
← Package overviewRunnable learning examples →