omnibias.core.proof
Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.
import omnibias.core.proofModule contract & mathematical conventions
Numerical certificates with schema, replay, and formal-verification gates.
Concrete applications register their own provers. A successful verdict must pass the certificate schema and requested independent checks. Formal status is earned only by a successful kernel check.
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.
catalogModule ↗certificateModule ↗conditionModule ↗discoveryModule ↗inequalityModule ↗lean_checkModule ↗lean_lockModule ↗liftModule ↗obligationsModule ↗observeModule ↗realization_algebra_replayModule ↗realization_replayModule ↗replayModule ↗Imports & aliases
These names share a definition with another public module. Follow a name for its full contract, parameters, and examples.
| Import from this module | Canonical reference |
|---|---|
ALL_CONDITION_SORTS | omnibias.core.proof.ALL_CONDITION_SORTS |
CERTIFICATE_SCHEMA_VERSION | omnibias.core.proof.CERTIFICATE_SCHEMA_VERSION |
CatalogEntry | omnibias.core.proof.CatalogEntry |
Characterization | omnibias.core.proof.Characterization |
ClassHit | omnibias.core.proof.ClassHit |
ClassMemory | omnibias.core.proof.ClassMemory |
ClassSelection | omnibias.core.proof.ClassSelection |
ConditionHypothesis | omnibias.core.proof.ConditionHypothesis |
ConditionSort | omnibias.core.proof.ConditionSort |
ConditionToken | omnibias.core.proof.ConditionToken |
CoordinateNewton | omnibias.core.proof.CoordinateNewton |
DiscoveredEquation | omnibias.core.proof.DiscoveredEquation |
DiscoveryResult | omnibias.core.proof.DiscoveryResult |
DomainSubdivisionCertificate | omnibias.core.proof.DomainSubdivisionCertificate |
ExactCheck | omnibias.core.proof.ExactCheck |
FEATURE_DIM | omnibias.core.proof.FEATURE_DIM |
FORMAL_CLAIM_KEY | omnibias.core.proof.FORMAL_CLAIM_KEY |
FiniteFamily | omnibias.core.proof.FiniteFamily |
FrequencyGate | omnibias.core.proof.FrequencyGate |
GrammarGrowthFamily | omnibias.core.proof.GrammarGrowthFamily |
GrammarSpec | omnibias.core.proof.GrammarSpec |
INEQUALITY_KIND | omnibias.core.proof.INEQUALITY_KIND |
InequalityBackend | omnibias.core.proof.InequalityBackend |
InequalitySort | omnibias.core.proof.InequalitySort |
InequalitySystem | omnibias.core.proof.InequalitySystem |
IntegerIntervalFamily | omnibias.core.proof.IntegerIntervalFamily |
KindMetaFamily | omnibias.core.proof.KindMetaFamily |
LeanCheckResult | omnibias.core.proof.LeanCheckResult |
LinearSpanFamily | omnibias.core.proof.LinearSpanFamily |
Obligation | omnibias.core.proof.Obligation |
Observation | omnibias.core.proof.Observation |
OneHotAnneal | omnibias.core.proof.OneHotAnneal |
Proposal | omnibias.core.proof.Proposal |
RationalStencil | omnibias.core.proof.RationalStencil |
RationalSupport | omnibias.core.proof.RationalSupport |
RationalWitness | omnibias.core.proof.RationalWitness |
ReplayCertificateReport | omnibias.core.proof.ReplayCertificateReport |
ReplayRecorder | omnibias.core.proof.ReplayRecorder |
ReplayStep | omnibias.core.proof.ReplayStep |
ReplayTrace | omnibias.core.proof.ReplayTrace |
SUPPORTED_SCHEMA_VERSIONS | omnibias.core.proof.SUPPORTED_SCHEMA_VERSIONS |
ScoreGuidedWalk | omnibias.core.proof.ScoreGuidedWalk |
Statement | omnibias.core.proof.Statement |
StencilCertificateReport | omnibias.core.proof.StencilCertificateReport |
SubdivisionLeaf | omnibias.core.proof.SubdivisionLeaf |
apply_constructor | omnibias.core.proof.apply_constructor |
as_fraction | omnibias.core.proof.as_fraction |
bind_sorts | omnibias.core.proof.bind_sorts |
build_inequality_machine | omnibias.core.proof.build_inequality_machine |
canonical_json | omnibias.core.proof.canonical_json |
catalog_entry | omnibias.core.proof.catalog_entry |
certificate_digest | omnibias.core.proof.certificate_digest |
check_certificate | omnibias.core.proof.check_certificate |
class_hit_from_check | omnibias.core.proof.class_hit_from_check |
condition_honesty | omnibias.core.proof.condition_honesty |
curated_rational_stencils | omnibias.core.proof.curated_rational_stencils |
decode_interval | omnibias.core.proof.decode_interval |
decode_interval_matrix | omnibias.core.proof.decode_interval_matrix |
decode_taylor_model | omnibias.core.proof.decode_taylor_model |
default_inequality_honesty | omnibias.core.proof.default_inequality_honesty |
discover | omnibias.core.proof.discover |
emit_condition | omnibias.core.proof.emit_condition |
encode_interval | omnibias.core.proof.encode_interval |
encode_interval_matrix | omnibias.core.proof.encode_interval_matrix |
encode_taylor_model | omnibias.core.proof.encode_taylor_model |
generate_obligation | omnibias.core.proof.generate_obligation |
get_proposer | omnibias.core.proof.get_proposer |
grow_neighbors | omnibias.core.proof.grow_neighbors |
inequality_backend | omnibias.core.proof.inequality_backend |
inequality_prover | omnibias.core.proof.inequality_prover |
integer_null_space | omnibias.core.proof.integer_null_space |
interval_certificate | omnibias.core.proof.interval_certificate |
kernel_root | omnibias.core.proof.kernel_root |
lean_check_available | omnibias.core.proof.lean_check_available |
list_catalog | omnibias.core.proof.list_catalog |
list_condition_sorts | omnibias.core.proof.list_condition_sorts |
list_inequality_backends | omnibias.core.proof.list_inequality_backends |
load_inequality_stack | omnibias.core.proof.load_inequality_stack |
locked_catalog | omnibias.core.proof.locked_catalog |
make_certificate | omnibias.core.proof.make_certificate |
poisedness_obligation | omnibias.core.proof.poisedness_obligation |
positive_definite_certificate | omnibias.core.proof.positive_definite_certificate |
prove_inequality | omnibias.core.proof.prove_inequality |
rank_class_hits | omnibias.core.proof.rank_class_hits |
record_ldlt_diagonal_trace | omnibias.core.proof.record_ldlt_diagonal_trace |
register_catalog | omnibias.core.proof.register_catalog |
register_condition_sort | omnibias.core.proof.register_condition_sort |
register_inequality_backend | omnibias.core.proof.register_inequality_backend |
replay_inequality | omnibias.core.proof.replay_inequality |
residual_identically_zero | omnibias.core.proof.residual_identically_zero |
run_discovery | omnibias.core.proof.run_discovery |
run_inequality_pipeline | omnibias.core.proof.run_inequality_pipeline |
schema_errors_v1 | omnibias.core.proof.schema_errors_v1 |
seal_certificate | omnibias.core.proof.seal_certificate |
seal_domain_subdivision_certificate | omnibias.core.proof.seal_domain_subdivision_certificate |
seal_poisedness_certificate | omnibias.core.proof.seal_poisedness_certificate |
seal_replay_certificate | omnibias.core.proof.seal_replay_certificate |
seal_stencil_certificate | omnibias.core.proof.seal_stencil_certificate |
select_class | omnibias.core.proof.select_class |
solve_inequality | omnibias.core.proof.solve_inequality |
stencil_consistency_obligation | omnibias.core.proof.stencil_consistency_obligation |
taylor_model_certificate | omnibias.core.proof.taylor_model_certificate |
verify_certificate_digest | omnibias.core.proof.verify_certificate_digest |
Certificate
omnibias.core.proof.CertificateSource ↗Certificate = dict[str, Any]A certificate is a plain JSON-serialisable mapping (the omnibias convention).
Regression example · honesty gate still ignores the formal claim
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_honesty_gate_still_ignores_the_formal_claim() -> None:
"""The conjecture-side rule and the artifact-side rule must agree."""
cert: Certificate = {"honesty": {FORMAL_CLAIM_KEY: False}}
conjecture = Conjecture("x", "k", {}, claims={FORMAL_CLAIM_KEY: True})
# honesty_gate defers to ProofMachine.evaluate, which consults the kernel.
assert honesty_gate(conjecture, cert) is Truepython -m pytest packages/omnibias-core/tests/test_proof_machine.py -k test_honesty_gate_still_ignores_the_formal_claim -qRegression example · honesty gate passes when no claims or supported
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_honesty_gate_passes_when_no_claims_or_supported() -> None:
conj = Conjecture("x", "k", {})
assert honesty_gate(conj, None) is True
cert: Certificate = {"honesty": {"interval_verified": True}}
conj2 = Conjecture("y", "k", {}, claims={"interval_verified": True})
assert honesty_gate(conj2, cert) is True
conj3 = Conjecture("z", "k", {}, claims={"unproven_claim": True})
assert honesty_gate(conj3, cert) is Falsepython -m pytest packages/omnibias-core/tests/test_proof_machine.py -k test_honesty_gate_passes_when_no_claims_or_supported -qRead the implementation
Certificate = dict[str, Any]Conjecture
omnibias.core.proof.ConjectureSource ↗class ConjectureDataclass 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 statement to be adjudicated by the ProofMachine.
Parameters
name: Human-readable label (free text), e.g. "positive residual margin".
kind: The dispatch key a prover matches on, e.g. "positive_residual_margin".
data: Inputs forwarded to the prover (e.g. {"coeffs": [...], "scales": [...]}).
claims: Honesty claims the conjecture *asserts*. Each True entry must be supported by the produced certificate's honesty flags or the verdict is downgraded to BLOCKED (the honesty gate). Leave empty for the normal "is this model statement certified?" question.
Parameters
| Name | Type & default | Contract |
|---|---|---|
namedataclass field | strRequired | Human-readable label (free text), e.g. "positive residual margin". |
kinddataclass field | strRequired | The dispatch key a prover matches on, e.g. "positive_residual_margin". |
datadataclass field | Mapping[str, Any]Default: field(default_factory=dict) | Inputs forwarded to the prover (e.g. {"coeffs": [...], "scales": [...]}). |
claimsdataclass field | Mapping[str, bool]Default: field(default_factory=dict) | Honesty claims the conjecture *asserts*. Each True entry must be supported by the produced certificate's honesty flags or the verdict is downgraded to BLOCKED (the honesty gate). Leave empty for the normal "is this model statement certified?" question. |
Regression example · machine accepts valid sealed certificate
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_machine_accepts_valid_sealed_certificate -qRegression example · machine blocks unknown kind
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_blocks_unknown_kind() -> None:
machine = ProofMachine().register(_sign_prover())
verdict = machine.evaluate(Conjecture("x", "unknown", {}))
assert verdict.status == "BLOCKED"
assert verdict.prover == "<none>"
assert any("no registered prover" in o for o in verdict.obligations)python -m pytest packages/omnibias-core/tests/test_proof_machine.py -k test_machine_blocks_unknown_kind -qFields & methods
kindfield
kind: strThe dispatch key a prover matches on, e.g. "positive_residual_margin".
datafield
data: Mapping[str, Any] = field(default_factory=dict)Inputs forwarded to the prover (e.g. {"coeffs": [...], "scales": [...]}).
claimsfield
claims: Mapping[str, bool] = field(default_factory=dict)Honesty claims the conjecture *asserts*. Each True entry must be supported by the produced certificate's honesty flags or the verdict is downgraded to BLOCKED (the honesty gate). Leave empty for the normal "is this model statement certified?" question.
Read the implementation
class Conjecture:
"""A statement to be adjudicated by the :class:`ProofMachine`.
Parameters
----------
name:
Human-readable label (free text), e.g. ``"positive residual margin"``.
kind:
The dispatch key a prover matches on, e.g. ``"positive_residual_margin"``.
data:
Inputs forwarded to the prover (e.g. ``{"coeffs": [...], "scales": [...]}``).
claims:
Honesty claims the conjecture *asserts*. Each ``True`` entry must be
supported by the produced certificate's ``honesty`` flags or the verdict
is downgraded to ``BLOCKED`` (the honesty gate). Leave empty for the
normal "is this model statement certified?" question.
"""
name: str
kind: str
data: Mapping[str, Any] = field(default_factory=dict)
claims: Mapping[str, bool] = field(default_factory=dict)FunctionProver
omnibias.core.proof.FunctionProverSource ↗class FunctionProverDataclass 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.
Adapter that builds a Prover from plain callables.
Lets a downstream package register an existing certificate generator without
writing a class: supply the kinds it handles, a function mapping a
Conjecture to a ProofAttempt, and (optionally) the schema
validator and the independent replay twin.
Parameters
| Name | Type & default | Contract |
|---|---|---|
namedataclass field | strRequired | See the operation contract and implementation below. |
kindsdataclass field | frozenset[str]Required | See the operation contract and implementation below. |
prove_fndataclass field | Callable[[Conjecture], ProofAttempt]Required | See the operation contract and implementation below. |
schema_fndataclass field | Callable[[Certificate], list[str]] | NoneDefault: None | See the operation contract and implementation below. |
replay_fndataclass field | Callable[[Certificate], bool | None] | NoneDefault: None | See the operation contract and implementation below. |
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qRegression example · machine records certificate schema version
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_records_certificate_schema_version() -> None:
cert = interval_certificate("x in [0,1]", Interval(0.0, 1.0))
def prove(_c: Conjecture) -> ProofAttempt:
return ProofAttempt(status="PROVED", certificate=cert)
machine = ProofMachine().register(
FunctionProver(name="iv", kinds=frozenset({"iv_demo"}), prove_fn=prove)
)
verdict = machine.evaluate(Conjecture(name="demo", kind="iv_demo"))
assert verdict.status == "PROVED"
assert verdict.certificate_schema_version == CERTIFICATE_SCHEMA_VERSION
assert verdict.theorem_prover_verified is Falsepython -m pytest packages/omnibias-core/tests/test_certificate.py -k test_machine_records_certificate_schema_version -qFields & methods
namefield
name: strDeclared str field on FunctionProver. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗kindsfield
kinds: frozenset[str]Declared frozenset[str] field on FunctionProver. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗prove_fnfield
prove_fn: Callable[[Conjecture], ProofAttempt]Declared Callable[[Conjecture], ProofAttempt] field on FunctionProver. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗schema_fnfield
schema_fn: Callable[[Certificate], list[str]] | None = NoneDeclared Callable[[Certificate], list[str]] | None field on FunctionProver. Default expression: None.
replay_fnfield
replay_fn: Callable[[Certificate], bool | None] | None = NoneDeclared Callable[[Certificate], bool | None] | None field on FunctionProver. Default expression: None.
handlesmethod
handles(self, conjecture: Conjecture) -> boolSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
conjecturepositional-or-keyword | ConjectureRequired | See the operation contract and implementation below. |
Returns: bool
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qMethod implementation
def handles(self, conjecture: Conjecture) -> bool:
return conjecture.kind in self.kindsattemptmethod
attempt(self, conjecture: Conjecture) -> ProofAttemptSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
conjecturepositional-or-keyword | ConjectureRequired | See the operation contract and implementation below. |
Returns: ProofAttempt
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qMethod implementation
def attempt(self, conjecture: Conjecture) -> ProofAttempt:
return self.prove_fn(conjecture)schema_errorsmethod
schema_errors(self, certificate: Certificate) -> list[str]See the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
certificatepositional-or-keyword | CertificateRequired | See the operation contract and implementation below. |
Returns: list[str]
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qMethod implementation
def schema_errors(self, certificate: Certificate) -> list[str]:
return [] if self.schema_fn is None else list(self.schema_fn(certificate))replaymethod
replay(self, certificate: Certificate) -> bool | NoneSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
certificatepositional-or-keyword | CertificateRequired | See the operation contract and implementation below. |
Returns: bool | None
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qMethod implementation
def replay(self, certificate: Certificate) -> bool | None:
return None if self.replay_fn is None else self.replay_fn(certificate)Read the implementation
class FunctionProver:
"""Adapter that builds a :class:`Prover` from plain callables.
Lets a downstream package register an existing certificate generator without
writing a class: supply the kinds it handles, a function mapping a
:class:`Conjecture` to a :class:`ProofAttempt`, and (optionally) the schema
validator and the independent replay twin.
"""
name: str
kinds: frozenset[str]
prove_fn: Callable[[Conjecture], ProofAttempt]
schema_fn: Callable[[Certificate], list[str]] | None = None
replay_fn: Callable[[Certificate], bool | None] | None = None
def handles(self, conjecture: Conjecture) -> bool:
return conjecture.kind in self.kinds
def attempt(self, conjecture: Conjecture) -> ProofAttempt:
return self.prove_fn(conjecture)
def schema_errors(self, certificate: Certificate) -> list[str]:
return [] if self.schema_fn is None else list(self.schema_fn(certificate))
def replay(self, certificate: Certificate) -> bool | None:
return None if self.replay_fn is None else self.replay_fn(certificate)ProofAttempt
omnibias.core.proof.ProofAttemptSource ↗class ProofAttemptDataclass 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.
What a prover returns: its intrinsic verdict plus any artifact.
The machine still applies the schema gate, the replay check, and the honesty
gate on top of this, so a prover may return PROVED and still be
downgraded to BLOCKED by the machine if those checks fail.
Parameters
| Name | Type & default | Contract |
|---|---|---|
statusdataclass field | VerdictStatusRequired | See the operation contract and implementation below. |
certificatedataclass field | Certificate | NoneDefault: None | See the operation contract and implementation below. |
obligationsdataclass field | tuple[str, ...]Default: () | See the operation contract and implementation below. |
detaildataclass field | strDefault: '' | See the operation contract and implementation below. |
Regression example · machine records certificate schema version
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_records_certificate_schema_version() -> None:
cert = interval_certificate("x in [0,1]", Interval(0.0, 1.0))
def prove(_c: Conjecture) -> ProofAttempt:
return ProofAttempt(status="PROVED", certificate=cert)
machine = ProofMachine().register(
FunctionProver(name="iv", kinds=frozenset({"iv_demo"}), prove_fn=prove)
)
verdict = machine.evaluate(Conjecture(name="demo", kind="iv_demo"))
assert verdict.status == "PROVED"
assert verdict.certificate_schema_version == CERTIFICATE_SCHEMA_VERSION
assert verdict.theorem_prover_verified is Falsepython -m pytest packages/omnibias-core/tests/test_certificate.py -k test_machine_records_certificate_schema_version -qRegression example · strict mode does not change unsealed default behaviour
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_strict_mode_does_not_change_unsealed_default_behaviour() -> None:
# Default (non-strict) verdicts are unaffected for unsealed certs without a twin.
def prove(_conjecture: Conjecture) -> ProofAttempt:
return ProofAttempt(
status="PROVED", certificate={"value": 1.0, "honesty": {"unproven_claim": False}}
)
machine = ProofMachine().register(
FunctionProver(name="plain", kinds=frozenset({"plain"}), prove_fn=prove)
)
verdict = machine.evaluate(Conjecture("x", "plain", {}))
assert verdict.status == "PROVED"
assert verdict.replay_ok is Nonepython -m pytest packages/omnibias-core/tests/test_certificate_audit_regressions.py -k test_strict_mode_does_not_change_unsealed_default_behaviour -qFields & methods
statusfield
status: VerdictStatusDeclared VerdictStatus field on ProofAttempt. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗certificatefield
certificate: Certificate | None = NoneDeclared Certificate | None field on ProofAttempt. Default expression: None.
obligationsfield
obligations: tuple[str, ...] = ()Declared tuple[str, ...] field on ProofAttempt. Default expression: ().
Read the implementation
class ProofAttempt:
"""What a prover returns: its intrinsic verdict plus any artifact.
The machine still applies the schema gate, the replay check, and the honesty
gate on top of this, so a prover may return ``PROVED`` and still be
downgraded to ``BLOCKED`` by the machine if those checks fail.
"""
status: VerdictStatus
certificate: Certificate | None = None
obligations: tuple[str, ...] = ()
detail: str = ""ProofMachine
omnibias.core.proof.ProofMachineSource ↗class ProofMachineDispatch a Conjecture to a prover and adjudicate a Verdict.
Pipeline: select prover -> attempt -> schema gate -> independent replay
-> honesty gate. A prover's PROVED (or DISPROVED) is downgraded to
BLOCKED whenever the schema is invalid, an independent replay disagrees,
or (for PROVED) an asserted honesty claim is unsupported.
Parameters
| Name | Type & default | Contract |
|---|---|---|
registrypositional-or-keyword | ProverRegistry | NoneDefault: None | See the operation contract and implementation below. |
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qRegression example · machine blocks unknown kind
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_blocks_unknown_kind() -> None:
machine = ProofMachine().register(_sign_prover())
verdict = machine.evaluate(Conjecture("x", "unknown", {}))
assert verdict.status == "BLOCKED"
assert verdict.prover == "<none>"
assert any("no registered prover" in o for o in verdict.obligations)python -m pytest packages/omnibias-core/tests/test_proof_machine.py -k test_machine_blocks_unknown_kind -qFields & methods
__init__method
__init__(self, registry: ProverRegistry | None=None) -> NoneSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
registrypositional-or-keyword | ProverRegistry | NoneDefault: None | See the operation contract and implementation below. |
Returns: None
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qMethod implementation
def __init__(self, registry: ProverRegistry | None = None) -> None:
self.registry: ProverRegistry = registry if registry is not None else ProverRegistry()registermethod
register(self, prover: Prover) -> ProofMachineSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
proverpositional-or-keyword | ProverRequired | See the operation contract and implementation below. |
Returns: ProofMachine
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qMethod implementation
def register(self, prover: Prover) -> ProofMachine:
self.registry.register(prover)
return selfproversproperty
provers(self) -> tuple[Prover, ...]See the class contract above and the exact method implementation below.
Returns: tuple[Prover, ...]
Method implementation
def provers(self) -> tuple[Prover, ...]:
return self.registry.proverskindsmethod
kinds(self) -> tuple[str, ...]See the class contract above and the exact method implementation below.
Returns: tuple[str, ...]
Executed regression · machine proves disproves and blocks
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_proves_disproves_and_blocks() -> None:
machine = ProofMachine().register(_sign_prover())
assert machine.kinds() == ("sign",)
proved = machine.evaluate(Conjecture("pos", "sign", {"value": 3.0}))
assert proved.status == "PROVED"
assert proved.proved is True
assert proved.schema_ok is True
assert proved.replay_ok is True
assert proved.honesty_ok is True
disproved = machine.evaluate(Conjecture("neg", "sign", {"value": -3.0}))
assert disproved.status == "DISPROVED"
assert disproved.disproved is True
blocked = machine.evaluate(Conjecture("zero", "sign", {"value": 0.0}))
assert blocked.status == "BLOCKED"
assert "value is zero" in blocked.obligationspython -m pytest "packages/omnibias-core/tests/test_proof_machine.py::test_machine_proves_disproves_and_blocks" -qMethod implementation
def kinds(self) -> tuple[str, ...]:
return self.registry.kinds()evaluatemethod
evaluate(self, conjecture: Conjecture, *, replay: bool=True, lean_check: bool=False, strict: bool=False) -> VerdictAdjudicate a single conjecture.
Two always-on gates run on any certificate (both non-breaking, because they only fire on certificates that opt into the relevant format):
- **digest gate** -- if the certificate carries a
digestit must match its body (~omnibias.core.proof.certificate.verify_certificate_digest), so a tampered or stale sealed certificate is downgraded toBLOCKED; - **v1 schema gate** -- a certificate whose
schema_versionis a supported v1 envelope is additionally validated with~omnibias.core.proof.certificate.schema_errors_v1.
When strict is true a PROVED/DISPROVED verdict additionally
requires (i) a certificate, (ii) a present *and* valid tamper-evident
digest, and (iii) an independent replay twin that **agrees**
(replay_ok is True; None or False blocks). This is the
"treat the verdict as tamper-evident *and* independently replayed" mode;
the default (non-strict) preserves graceful degradation when a replay twin
or a digest is absent.
When lean_check is true (or the conjecture asserts the
theorem_prover_verified claim) and a Lean toolchain is available, the
produced certificate's finite obligation is re-checked by the Lean kernel
(omnibias.core.proof.lean_check); the resulting
Verdict.theorem_prover_verified flag is set only on a genuine
kernel pass. Asserting the claim without a passing kernel downgrades a
PROVED verdict to BLOCKED (the formal honesty gate).
Parameters
| Name | Type & default | Contract |
|---|---|---|
conjecturepositional-or-keyword | ConjectureRequired | See the operation contract and implementation below. |
replaykeyword-only | boolDefault: True | See the operation contract and implementation below. |
lean_checkkeyword-only | boolDefault: False | See the operation contract and implementation below. |
strictkeyword-only | boolDefault: False | See the operation contract and implementation below. |
Returns: Verdict
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qMethod implementation
def evaluate(
self,
conjecture: Conjecture,
*,
replay: bool = True,
lean_check: bool = False,
strict: bool = False,
) -> Verdict:
"""Adjudicate a single conjecture.
Two always-on gates run on any certificate (both non-breaking, because they
only fire on certificates that opt into the relevant format):
* **digest gate** -- if the certificate carries a ``digest`` it must match
its body (:func:`~omnibias.core.proof.certificate.verify_certificate_digest`),
so a tampered or stale sealed certificate is downgraded to ``BLOCKED``;
* **v1 schema gate** -- a certificate whose ``schema_version`` is a
supported v1 envelope is additionally validated with
:func:`~omnibias.core.proof.certificate.schema_errors_v1`.
When ``strict`` is true a ``PROVED``/``DISPROVED`` verdict additionally
requires (i) a certificate, (ii) a present *and* valid tamper-evident
digest, and (iii) an independent replay twin that **agrees**
(``replay_ok is True``; ``None`` or ``False`` blocks). This is the
"treat the verdict as tamper-evident *and* independently replayed" mode;
the default (non-strict) preserves graceful degradation when a replay twin
or a digest is absent.
When ``lean_check`` is true (or the conjecture asserts the
``theorem_prover_verified`` claim) and a Lean toolchain is available, the
produced certificate's finite obligation is re-checked by the Lean kernel
(:mod:`omnibias.core.proof.lean_check`); the resulting
:attr:`Verdict.theorem_prover_verified` flag is set only on a genuine
kernel pass. Asserting the claim without a passing kernel downgrades a
``PROVED`` verdict to ``BLOCKED`` (the formal honesty gate).
"""
prover = self.registry.select(conjecture)
if prover is None:
return Verdict(
status="BLOCKED",
conjecture=conjecture.name,
kind=conjecture.kind,
prover="<none>",
certificate=None,
obligations=(
f"no registered prover handles kind {conjecture.kind!r}",
),
schema_ok=False,
replay_ok=None,
honesty_ok=honesty_gate(conjecture, None),
detail="no prover registered for this kind",
)
attempt = prover.attempt(conjecture)
certificate = attempt.certificate
obligations: list[str] = list(attempt.obligations)
schema_ok = True
if certificate is not None:
errors = prover.schema_errors(certificate)
if errors:
schema_ok = False
obligations.extend(f"schema: {message}" for message in errors)
# Tamper-evidence (always on): a certificate that carries a digest must
# match its body (the same check the Lean bridge runs). Only fires on
# sealed certs, so the many unsealed certified-evidence certs are unaffected.
if "digest" in certificate and not verify_certificate_digest(certificate):
schema_ok = False
obligations.append(
"schema: certificate digest mismatch (tampered or stale)"
)
honesty_ok = honesty_gate(conjecture, certificate)
replay_ok: bool | None = None
if (replay or strict) and certificate is not None:
replay_ok = prover.replay(certificate)
status: VerdictStatus = attempt.status
if status in ("PROVED", "DISPROVED"):
if not schema_ok:
status = "BLOCKED"
obligations.append("schema validation failed")
if replay_ok is False:
status = "BLOCKED"
obligations.append("independent replay disagreed with the certificate")
if strict:
if certificate is None:
status = "BLOCKED"
obligations.append("strict mode: no certificate to adjudicate")
else:
if "digest" not in certificate:
status = "BLOCKED"
obligations.append(
"strict mode: an unsealed certificate (no tamper-evident "
"digest) cannot back a strict verdict"
)
# Require a well-formed v1 envelope (claim/payload/honesty/digest
# present and the digest valid).
v1_errors = schema_errors_v1(certificate)
if v1_errors:
status = "BLOCKED"
obligations.extend(
f"strict mode schema(v1): {message}" for message in v1_errors
)
if replay_ok is not True:
status = "BLOCKED"
obligations.append(
"strict mode: requires an independent replay twin that "
"agrees (replay_ok must be True)"
)
if status == "PROVED" and not honesty_ok:
status = "BLOCKED"
obligations.append(
"honesty gate: an asserted claim is not supported by the "
"certificate's honesty flags (no external evidence attached)"
)
schema_version: str | None = None
if certificate is not None:
candidate = certificate.get("schema_version")
if isinstance(candidate, str):
schema_version = candidate
# Formal (Lean-kernel) gate: set theorem_prover_verified only on a genuine
# kernel pass; an asserted-but-unbacked formal claim blocks a PROVED verdict.
claims_formal = bool(conjecture.claims.get(FORMAL_CLAIM_KEY, False))
theorem_prover_verified = False
if (lean_check or claims_formal) and certificate is not None and status in (
"PROVED",
"DISPROVED",
):
from omnibias.core.proof.lean_check import check_certificate
theorem_prover_verified = check_certificate(certificate).verified
if status == "PROVED" and claims_formal and not theorem_prover_verified:
status = "BLOCKED"
honesty_ok = False
obligations.append(
"honesty gate: 'theorem_prover_verified' asserted but the Lean "
"kernel did not verify the certificate's obligation"
)
return Verdict(
status=status,
conjecture=conjecture.name,
kind=conjecture.kind,
prover=prover.name,
certificate=certificate,
obligations=tuple(obligations),
schema_ok=schema_ok,
replay_ok=replay_ok,
honesty_ok=honesty_ok,
detail=attempt.detail,
certificate_schema_version=schema_version,
theorem_prover_verified=theorem_prover_verified,
)evaluate_allmethod
evaluate_all(self, conjectures: Iterable[Conjecture], *, replay: bool=True, lean_check: bool=False, strict: bool=False) -> list[Verdict]See the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
conjecturespositional-or-keyword | Iterable[Conjecture]Required | See the operation contract and implementation below. |
replaykeyword-only | boolDefault: True | See the operation contract and implementation below. |
lean_checkkeyword-only | boolDefault: False | See the operation contract and implementation below. |
strictkeyword-only | boolDefault: False | See the operation contract and implementation below. |
Returns: list[Verdict]
Executed regression · evaluate all batches
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_evaluate_all_batches() -> None:
machine = ProofMachine().register(_sign_prover())
conjectures = [
Conjecture("a", "sign", {"value": 1.0}),
Conjecture("b", "sign", {"value": -1.0}),
]
verdicts = machine.evaluate_all(conjectures)
assert [v.status for v in verdicts] == ["PROVED", "DISPROVED"]
assert verdicts[0].summary()["status"] == "PROVED"python -m pytest "packages/omnibias-core/tests/test_proof_machine.py::test_evaluate_all_batches" -qMethod implementation
def evaluate_all(
self,
conjectures: Iterable[Conjecture],
*,
replay: bool = True,
lean_check: bool = False,
strict: bool = False,
) -> list[Verdict]:
return [
self.evaluate(conjecture, replay=replay, lean_check=lean_check, strict=strict)
for conjecture in conjectures
]registryattribute
registry: ProverRegistry = registry if registry is not None else ProverRegistry()Public instance attribute assigned by __init__. The source assignment is registry = registry if registry is not None else ProverRegistry(); it describes instance state, not a literal constructor default.
Read the implementation
class ProofMachine:
"""Dispatch a :class:`Conjecture` to a prover and adjudicate a :class:`Verdict`.
Pipeline: select prover -> ``attempt`` -> schema gate -> independent replay
-> honesty gate. A prover's ``PROVED`` (or ``DISPROVED``) is downgraded to
``BLOCKED`` whenever the schema is invalid, an independent replay disagrees,
or (for ``PROVED``) an asserted honesty claim is unsupported.
"""
def __init__(self, registry: ProverRegistry | None = None) -> None:
self.registry: ProverRegistry = registry if registry is not None else ProverRegistry()
def register(self, prover: Prover) -> ProofMachine:
self.registry.register(prover)
return self
@property
def provers(self) -> tuple[Prover, ...]:
return self.registry.provers
def kinds(self) -> tuple[str, ...]:
return self.registry.kinds()
def evaluate(
self,
conjecture: Conjecture,
*,
replay: bool = True,
lean_check: bool = False,
strict: bool = False,
) -> Verdict:
"""Adjudicate a single conjecture.
Two always-on gates run on any certificate (both non-breaking, because they
only fire on certificates that opt into the relevant format):
* **digest gate** -- if the certificate carries a ``digest`` it must match
its body (:func:`~omnibias.core.proof.certificate.verify_certificate_digest`),
so a tampered or stale sealed certificate is downgraded to ``BLOCKED``;
* **v1 schema gate** -- a certificate whose ``schema_version`` is a
supported v1 envelope is additionally validated with
:func:`~omnibias.core.proof.certificate.schema_errors_v1`.
When ``strict`` is true a ``PROVED``/``DISPROVED`` verdict additionally
requires (i) a certificate, (ii) a present *and* valid tamper-evident
digest, and (iii) an independent replay twin that **agrees**
(``replay_ok is True``; ``None`` or ``False`` blocks). This is the
"treat the verdict as tamper-evident *and* independently replayed" mode;
the default (non-strict) preserves graceful degradation when a replay twin
or a digest is absent.
When ``lean_check`` is true (or the conjecture asserts the
``theorem_prover_verified`` claim) and a Lean toolchain is available, the
produced certificate's finite obligation is re-checked by the Lean kernel
(:mod:`omnibias.core.proof.lean_check`); the resulting
:attr:`Verdict.theorem_prover_verified` flag is set only on a genuine
kernel pass. Asserting the claim without a passing kernel downgrades a
``PROVED`` verdict to ``BLOCKED`` (the formal honesty gate).
"""
prover = self.registry.select(conjecture)
if prover is None:
return Verdict(
status="BLOCKED",
conjecture=conjecture.name,
kind=conjecture.kind,
prover="<none>",
certificate=None,
obligations=(
f"no registered prover handles kind {conjecture.kind!r}",
),
schema_ok=False,
replay_ok=None,
honesty_ok=honesty_gate(conjecture, None),
detail="no prover registered for this kind",
)
attempt = prover.attempt(conjecture)
certificate = attempt.certificate
obligations: list[str] = list(attempt.obligations)
schema_ok = True
if certificate is not None:
errors = prover.schema_errors(certificate)
if errors:
schema_ok = False
obligations.extend(f"schema: {message}" for message in errors)
# Tamper-evidence (always on): a certificate that carries a digest must
# match its body (the same check the Lean bridge runs). Only fires on
# sealed certs, so the many unsealed certified-evidence certs are unaffected.
if "digest" in certificate and not verify_certificate_digest(certificate):
schema_ok = False
obligations.append(
"schema: certificate digest mismatch (tampered or stale)"
)
honesty_ok = honesty_gate(conjecture, certificate)
replay_ok: bool | None = None
if (replay or strict) and certificate is not None:
replay_ok = prover.replay(certificate)
status: VerdictStatus = attempt.status
if status in ("PROVED", "DISPROVED"):
if not schema_ok:
status = "BLOCKED"
obligations.append("schema validation failed")
if replay_ok is False:
status = "BLOCKED"
obligations.append("independent replay disagreed with the certificate")
if strict:
if certificate is None:
status = "BLOCKED"
obligations.append("strict mode: no certificate to adjudicate")
else:
if "digest" not in certificate:
status = "BLOCKED"
obligations.append(
"strict mode: an unsealed certificate (no tamper-evident "
"digest) cannot back a strict verdict"
)
# Require a well-formed v1 envelope (claim/payload/honesty/digest
# present and the digest valid).
v1_errors = schema_errors_v1(certificate)
if v1_errors:
status = "BLOCKED"
obligations.extend(
f"strict mode schema(v1): {message}" for message in v1_errors
)
if replay_ok is not True:
status = "BLOCKED"
obligations.append(
"strict mode: requires an independent replay twin that "
"agrees (replay_ok must be True)"
)
if status == "PROVED" and not honesty_ok:
status = "BLOCKED"
obligations.append(
"honesty gate: an asserted claim is not supported by the "
"certificate's honesty flags (no external evidence attached)"
)
schema_version: str | None = None
if certificate is not None:
candidate = certificate.get("schema_version")
if isinstance(candidate, str):
schema_version = candidate
# Formal (Lean-kernel) gate: set theorem_prover_verified only on a genuine
# kernel pass; an asserted-but-unbacked formal claim blocks a PROVED verdict.
claims_formal = bool(conjecture.claims.get(FORMAL_CLAIM_KEY, False))
theorem_prover_verified = False
if (lean_check or claims_formal) and certificate is not None and status in (
"PROVED",
"DISPROVED",
):
from omnibias.core.proof.lean_check import check_certificate
theorem_prover_verified = check_certificate(certificate).verified
if status == "PROVED" and claims_formal and not theorem_prover_verified:
status = "BLOCKED"
honesty_ok = False
obligations.append(
"honesty gate: 'theorem_prover_verified' asserted but the Lean "
"kernel did not verify the certificate's obligation"
)
return Verdict(
status=status,
conjecture=conjecture.name,
kind=conjecture.kind,
prover=prover.name,
certificate=certificate,
obligations=tuple(obligations),
schema_ok=schema_ok,
replay_ok=replay_ok,
honesty_ok=honesty_ok,
detail=attempt.detail,
certificate_schema_version=schema_version,
theorem_prover_verified=theorem_prover_verified,
)
def evaluate_all(
self,
conjectures: Iterable[Conjecture],
*,
replay: bool = True,
lean_check: bool = False,
strict: bool = False,
) -> list[Verdict]:
return [
self.evaluate(conjecture, replay=replay, lean_check=lean_check, strict=strict)
for conjecture in conjectures
]Prover
omnibias.core.proof.ProverSource ↗class Prover(Protocol)Structural protocol every prover satisfies.
handles selects on Conjecture.kind; attempt produces a
ProofAttempt; schema_errors validates a certificate (empty list
== valid); replay runs an *independent* recomputation and returns
True/False (or None when no twin exists).
name is declared **read-only**: a mutable name: str member would demand
a settable attribute, which the frozen FunctionProver adapter cannot
provide, so no frozen prover could satisfy this protocol under a strict type
check. A read-only member accepts both plain attributes and properties.
Fields & methods
nameproperty
name(self) -> strSee the class contract above and the exact method implementation below.
Returns: str
Method implementation
def name(self) -> str: ...handlesmethod
handles(self, conjecture: Conjecture) -> boolSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
conjecturepositional-or-keyword | ConjectureRequired | See the operation contract and implementation below. |
Returns: bool
Method implementation
def handles(self, conjecture: Conjecture) -> bool: ...attemptmethod
attempt(self, conjecture: Conjecture) -> ProofAttemptSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
conjecturepositional-or-keyword | ConjectureRequired | See the operation contract and implementation below. |
Returns: ProofAttempt
Method implementation
def attempt(self, conjecture: Conjecture) -> ProofAttempt: ...schema_errorsmethod
schema_errors(self, certificate: Certificate) -> list[str]See the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
certificatepositional-or-keyword | CertificateRequired | See the operation contract and implementation below. |
Returns: list[str]
Method implementation
def schema_errors(self, certificate: Certificate) -> list[str]: ...replaymethod
replay(self, certificate: Certificate) -> bool | NoneSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
certificatepositional-or-keyword | CertificateRequired | See the operation contract and implementation below. |
Returns: bool | None
Method implementation
def replay(self, certificate: Certificate) -> bool | None: ...Read the implementation
class Prover(Protocol):
"""Structural protocol every prover satisfies.
``handles`` selects on :attr:`Conjecture.kind`; ``attempt`` produces a
:class:`ProofAttempt`; ``schema_errors`` validates a certificate (empty list
== valid); ``replay`` runs an *independent* recomputation and returns
``True``/``False`` (or ``None`` when no twin exists).
``name`` is declared **read-only**: a mutable ``name: str`` member would demand
a settable attribute, which the frozen :class:`FunctionProver` adapter cannot
provide, so no frozen prover could satisfy this protocol under a strict type
check. A read-only member accepts both plain attributes and properties.
"""
@property
def name(self) -> str: ...
def handles(self, conjecture: Conjecture) -> bool: ...
def attempt(self, conjecture: Conjecture) -> ProofAttempt: ...
def schema_errors(self, certificate: Certificate) -> list[str]: ...
def replay(self, certificate: Certificate) -> bool | None: ...ProverRegistry
omnibias.core.proof.ProverRegistrySource ↗class ProverRegistryAn ordered collection of provers with kind-based selection.
Parameters
| Name | Type & default | Contract |
|---|---|---|
proverspositional-or-keyword | Iterable[Prover] | NoneDefault: None | See the operation contract and implementation below. |
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qRegression example · registry select first match and replay none keeps verdict
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_registry_select_first_match_and_replay_none_keeps_verdict() -> None:
def prove(conjecture: Conjecture) -> ProofAttempt:
return ProofAttempt(status="PROVED", certificate={"honesty": {}})
prover = FunctionProver(name="noreplay", kinds=frozenset({"k"}), prove_fn=prove)
registry = ProverRegistry([prover])
assert registry.select(Conjecture("a", "k", {})) is prover
assert registry.select(Conjecture("a", "other", {})) is None
machine = ProofMachine(registry)
verdict = machine.evaluate(Conjecture("a", "k", {}))
assert isinstance(verdict, Verdict)
# No replay twin -> replay_ok is None and the PROVED verdict stands.
assert verdict.replay_ok is None
assert verdict.status == "PROVED"python -m pytest packages/omnibias-core/tests/test_proof_machine.py -k test_registry_select_first_match_and_replay_none_keeps_verdict -qFields & methods
__init__method
__init__(self, provers: Iterable[Prover] | None=None) -> NoneSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
proverspositional-or-keyword | Iterable[Prover] | NoneDefault: None | See the operation contract and implementation below. |
Returns: None
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qMethod implementation
def __init__(self, provers: Iterable[Prover] | None = None) -> None:
self._provers: list[Prover] = list(provers) if provers is not None else []registermethod
register(self, prover: Prover) -> ProverRegistryAppend prover (returns self for chaining).
Parameters
| Name | Type & default | Contract |
|---|---|---|
proverpositional-or-keyword | ProverRequired | See the operation contract and implementation below. |
Returns: ProverRegistry
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qMethod implementation
def register(self, prover: Prover) -> ProverRegistry:
"""Append ``prover`` (returns ``self`` for chaining)."""
self._provers.append(prover)
return selfextendmethod
extend(self, provers: Iterable[Prover]) -> ProverRegistrySee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
proverspositional-or-keyword | Iterable[Prover]Required | See the operation contract and implementation below. |
Returns: ProverRegistry
Method implementation
def extend(self, provers: Iterable[Prover]) -> ProverRegistry:
for prover in provers:
self._provers.append(prover)
return selfproversproperty
provers(self) -> tuple[Prover, ...]See the class contract above and the exact method implementation below.
Returns: tuple[Prover, ...]
Method implementation
def provers(self) -> tuple[Prover, ...]:
return tuple(self._provers)kindsmethod
kinds(self) -> tuple[str, ...]All conjecture kinds handled by at least one registered prover.
Returns: tuple[str, ...]
Executed regression · machine proves disproves and blocks
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_proves_disproves_and_blocks() -> None:
machine = ProofMachine().register(_sign_prover())
assert machine.kinds() == ("sign",)
proved = machine.evaluate(Conjecture("pos", "sign", {"value": 3.0}))
assert proved.status == "PROVED"
assert proved.proved is True
assert proved.schema_ok is True
assert proved.replay_ok is True
assert proved.honesty_ok is True
disproved = machine.evaluate(Conjecture("neg", "sign", {"value": -3.0}))
assert disproved.status == "DISPROVED"
assert disproved.disproved is True
blocked = machine.evaluate(Conjecture("zero", "sign", {"value": 0.0}))
assert blocked.status == "BLOCKED"
assert "value is zero" in blocked.obligationspython -m pytest "packages/omnibias-core/tests/test_proof_machine.py::test_machine_proves_disproves_and_blocks" -qMethod implementation
def kinds(self) -> tuple[str, ...]:
"""All conjecture kinds handled by at least one registered prover."""
seen: dict[str, None] = {}
for prover in self._provers:
kinds = getattr(prover, "kinds", None)
if kinds is not None:
for kind in kinds:
seen[str(kind)] = None
return tuple(seen)selectmethod
select(self, conjecture: Conjecture) -> Prover | NoneThe first registered prover that handles conjecture (or None).
Parameters
| Name | Type & default | Contract |
|---|---|---|
conjecturepositional-or-keyword | ConjectureRequired | See the operation contract and implementation below. |
Returns: Prover | None
Executed regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qMethod implementation
def select(self, conjecture: Conjecture) -> Prover | None:
"""The first registered prover that handles ``conjecture`` (or ``None``)."""
for prover in self._provers:
if prover.handles(conjecture):
return prover
return NoneRead the implementation
class ProverRegistry:
"""An ordered collection of provers with kind-based selection."""
def __init__(self, provers: Iterable[Prover] | None = None) -> None:
self._provers: list[Prover] = list(provers) if provers is not None else []
def register(self, prover: Prover) -> ProverRegistry:
"""Append ``prover`` (returns ``self`` for chaining)."""
self._provers.append(prover)
return self
def extend(self, provers: Iterable[Prover]) -> ProverRegistry:
for prover in provers:
self._provers.append(prover)
return self
@property
def provers(self) -> tuple[Prover, ...]:
return tuple(self._provers)
def kinds(self) -> tuple[str, ...]:
"""All conjecture kinds handled by at least one registered prover."""
seen: dict[str, None] = {}
for prover in self._provers:
kinds = getattr(prover, "kinds", None)
if kinds is not None:
for kind in kinds:
seen[str(kind)] = None
return tuple(seen)
def select(self, conjecture: Conjecture) -> Prover | None:
"""The first registered prover that handles ``conjecture`` (or ``None``)."""
for prover in self._provers:
if prover.handles(conjecture):
return prover
return NoneVerdict
omnibias.core.proof.VerdictSource ↗class VerdictDataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.
The machine's adjudication of a Conjecture.
Parameters
| Name | Type & default | Contract |
|---|---|---|
statusdataclass field | VerdictStatusRequired | See the operation contract and implementation below. |
conjecturedataclass field | strRequired | See the operation contract and implementation below. |
kinddataclass field | strRequired | See the operation contract and implementation below. |
proverdataclass field | strRequired | See the operation contract and implementation below. |
certificatedataclass field | Certificate | NoneRequired | See the operation contract and implementation below. |
obligationsdataclass field | tuple[str, ...]Required | See the operation contract and implementation below. |
schema_okdataclass field | boolRequired | See the operation contract and implementation below. |
replay_okdataclass field | bool | NoneRequired | See the operation contract and implementation below. |
honesty_okdataclass field | boolRequired | See the operation contract and implementation below. |
detaildataclass field | strDefault: '' | See the operation contract and implementation below. |
certificate_schema_versiondataclass field | str | NoneDefault: None | See the operation contract and implementation below. |
theorem_prover_verifieddataclass field | boolDefault: False | See the operation contract and implementation below. |
Executed regression · evaluate all batches
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_evaluate_all_batches() -> None:
machine = ProofMachine().register(_sign_prover())
conjectures = [
Conjecture("a", "sign", {"value": 1.0}),
Conjecture("b", "sign", {"value": -1.0}),
]
verdicts = machine.evaluate_all(conjectures)
assert [v.status for v in verdicts] == ["PROVED", "DISPROVED"]
assert verdicts[0].summary()["status"] == "PROVED"python -m pytest "packages/omnibias-core/tests/test_proof_machine.py::test_evaluate_all_batches" -qRegression example · verdict has new fields with defaults
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_verdict_has_new_fields_with_defaults() -> None:
v = Verdict(
status="PROVED",
conjecture="c",
kind="k",
prover="p",
certificate=None,
obligations=(),
schema_ok=True,
replay_ok=None,
honesty_ok=True,
)
assert v.certificate_schema_version is None
assert v.theorem_prover_verified is False
assert v.summary()["theorem_prover_verified"] is Falsepython -m pytest packages/omnibias-core/tests/test_certificate.py -k test_verdict_has_new_fields_with_defaults -qFields & methods
statusfield
status: VerdictStatusDeclared VerdictStatus field on Verdict. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗conjecturefield
conjecture: strDeclared str field on Verdict. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗kindfield
kind: strDeclared str field on Verdict. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗proverfield
prover: strDeclared str field on Verdict. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗certificatefield
certificate: Certificate | NoneDeclared Certificate | None field on Verdict. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗obligationsfield
obligations: tuple[str, ...]Declared tuple[str, ...] field on Verdict. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗schema_okfield
schema_ok: boolDeclared bool field on Verdict. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗replay_okfield
replay_ok: bool | NoneDeclared bool | None field on Verdict. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗honesty_okfield
honesty_ok: boolDeclared bool field on Verdict. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗certificate_schema_versionfield
certificate_schema_version: str | None = NoneThe schema_version carried by the certificate.
Regression example · verdict has new fields with defaults
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_verdict_has_new_fields_with_defaults() -> None:
v = Verdict(
status="PROVED",
conjecture="c",
kind="k",
prover="p",
certificate=None,
obligations=(),
schema_ok=True,
replay_ok=None,
honesty_ok=True,
)
assert v.certificate_schema_version is None
assert v.theorem_prover_verified is False
assert v.summary()["theorem_prover_verified"] is Falsepython -m pytest packages/omnibias-core/tests/test_certificate.py -k test_verdict_has_new_fields_with_defaults -qtheorem_prover_verifiedfield
theorem_prover_verified: bool = FalseTrue only when a formal theorem-prover kernel re-checked the
certificate (set by the Lean bridge); False otherwise.
Regression example · verdict has new fields with defaults
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_verdict_has_new_fields_with_defaults() -> None:
v = Verdict(
status="PROVED",
conjecture="c",
kind="k",
prover="p",
certificate=None,
obligations=(),
schema_ok=True,
replay_ok=None,
honesty_ok=True,
)
assert v.certificate_schema_version is None
assert v.theorem_prover_verified is False
assert v.summary()["theorem_prover_verified"] is Falsepython -m pytest packages/omnibias-core/tests/test_certificate.py -k test_verdict_has_new_fields_with_defaults -qprovedproperty
proved(self) -> boolSee the class contract above and the exact method implementation below.
Returns: bool
Executed regression · machine proves disproves and blocks
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_proves_disproves_and_blocks() -> None:
machine = ProofMachine().register(_sign_prover())
assert machine.kinds() == ("sign",)
proved = machine.evaluate(Conjecture("pos", "sign", {"value": 3.0}))
assert proved.status == "PROVED"
assert proved.proved is True
assert proved.schema_ok is True
assert proved.replay_ok is True
assert proved.honesty_ok is True
disproved = machine.evaluate(Conjecture("neg", "sign", {"value": -3.0}))
assert disproved.status == "DISPROVED"
assert disproved.disproved is True
blocked = machine.evaluate(Conjecture("zero", "sign", {"value": 0.0}))
assert blocked.status == "BLOCKED"
assert "value is zero" in blocked.obligationspython -m pytest "packages/omnibias-core/tests/test_proof_machine.py::test_machine_proves_disproves_and_blocks" -qMethod implementation
def proved(self) -> bool:
return self.status == "PROVED"disprovedproperty
disproved(self) -> boolSee the class contract above and the exact method implementation below.
Returns: bool
Executed regression · machine proves disproves and blocks
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_proves_disproves_and_blocks() -> None:
machine = ProofMachine().register(_sign_prover())
assert machine.kinds() == ("sign",)
proved = machine.evaluate(Conjecture("pos", "sign", {"value": 3.0}))
assert proved.status == "PROVED"
assert proved.proved is True
assert proved.schema_ok is True
assert proved.replay_ok is True
assert proved.honesty_ok is True
disproved = machine.evaluate(Conjecture("neg", "sign", {"value": -3.0}))
assert disproved.status == "DISPROVED"
assert disproved.disproved is True
blocked = machine.evaluate(Conjecture("zero", "sign", {"value": 0.0}))
assert blocked.status == "BLOCKED"
assert "value is zero" in blocked.obligationspython -m pytest "packages/omnibias-core/tests/test_proof_machine.py::test_machine_proves_disproves_and_blocks" -qMethod implementation
def disproved(self) -> bool:
return self.status == "DISPROVED"blockedproperty
blocked(self) -> boolSee the class contract above and the exact method implementation below.
Returns: bool
Method implementation
def blocked(self) -> bool:
return self.status == "BLOCKED"summarymethod
summary(self) -> dict[str, Any]A small JSON-serialisable digest (omits the full certificate).
Returns: dict[str, Any]
Executed regression · evaluate all batches
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_evaluate_all_batches() -> None:
machine = ProofMachine().register(_sign_prover())
conjectures = [
Conjecture("a", "sign", {"value": 1.0}),
Conjecture("b", "sign", {"value": -1.0}),
]
verdicts = machine.evaluate_all(conjectures)
assert [v.status for v in verdicts] == ["PROVED", "DISPROVED"]
assert verdicts[0].summary()["status"] == "PROVED"python -m pytest "packages/omnibias-core/tests/test_proof_machine.py::test_evaluate_all_batches" -qMethod implementation
def summary(self) -> dict[str, Any]:
"""A small JSON-serialisable digest (omits the full certificate)."""
return {
"status": self.status,
"conjecture": self.conjecture,
"kind": self.kind,
"prover": self.prover,
"schema_ok": self.schema_ok,
"replay_ok": self.replay_ok,
"honesty_ok": self.honesty_ok,
"obligations": list(self.obligations),
"detail": self.detail,
"certificate_schema_version": self.certificate_schema_version,
"theorem_prover_verified": self.theorem_prover_verified,
}Read the implementation
class Verdict:
"""The machine's adjudication of a :class:`Conjecture`."""
status: VerdictStatus
conjecture: str
kind: str
prover: str
certificate: Certificate | None
obligations: tuple[str, ...]
schema_ok: bool
replay_ok: bool | None
honesty_ok: bool
detail: str = ""
#: The ``schema_version`` carried by the certificate.
certificate_schema_version: str | None = None
#: ``True`` only when a formal theorem-prover kernel re-checked the
#: certificate (set by the Lean bridge); ``False`` otherwise.
theorem_prover_verified: bool = False
@property
def proved(self) -> bool:
return self.status == "PROVED"
@property
def disproved(self) -> bool:
return self.status == "DISPROVED"
@property
def blocked(self) -> bool:
return self.status == "BLOCKED"
def summary(self) -> dict[str, Any]:
"""A small JSON-serialisable digest (omits the full certificate)."""
return {
"status": self.status,
"conjecture": self.conjecture,
"kind": self.kind,
"prover": self.prover,
"schema_ok": self.schema_ok,
"replay_ok": self.replay_ok,
"honesty_ok": self.honesty_ok,
"obligations": list(self.obligations),
"detail": self.detail,
"certificate_schema_version": self.certificate_schema_version,
"theorem_prover_verified": self.theorem_prover_verified,
}VerdictStatus
omnibias.core.proof.VerdictStatusSource ↗VerdictStatus = Literal['PROVED', 'DISPROVED', 'BLOCKED']The three terminal verdicts.
Read the implementation
VerdictStatus = Literal["PROVED", "DISPROVED", "BLOCKED"]formal_claim_forgery_errors
omnibias.core.proof.formal_claim_forgery_errorsSource ↗formal_claim_forgery_errors(honesty: Mapping[str, Any] | None, *, certificate: Certificate | None=None, context: str='honesty') -> list[str]Reject a *self-declared* theorem_prover_verified.
FORMAL_CLAIM_KEY is **earned** by a genuine Lean kernel pass, never
asserted by the artifact that benefits from it. ProofMachine.evaluate
already enforces that for conjectures, but any consumer that reads the flag
straight out of a *stored* bundle (a JSON file on disk, which anyone can edit)
would trust the artifact's own word for it. That is the one shape in which the
claim can be forged, so validators call this helper and treat a non-empty
result as a schema error.
A truthy declaration is accepted only when certificate is supplied *and*
the kernel genuinely verifies its obligation. With no Lean toolchain present
the bridge reports unverified, so the flag stays refused -- graceful
degradation must never become silent acceptance.
Parameters
honesty: The artifact's honesty mapping (None and non-mappings are treated as declaring nothing).
certificate: The certificate whose finite obligation the kernel should re-check. Omit it to refuse every truthy declaration outright.
context: Dotted prefix used in the message, so the caller's schema report points at the offending field.
Returns
list[str] Empty when nothing is declared or the declaration is kernel-backed; otherwise a single explanatory error.
Parameters
| Name | Type & default | Contract |
|---|---|---|
honestypositional-or-keyword | Mapping[str, Any] | NoneRequired | The artifact's honesty mapping (None and non-mappings are treated as declaring nothing). |
certificatekeyword-only | Certificate | NoneDefault: None | The certificate whose finite obligation the kernel should re-check. Omit it to refuse every truthy declaration outright. |
contextkeyword-only | strDefault: 'honesty' | Dotted prefix used in the message, so the caller's schema report points at the offending field. |
list[str]Executed regression · forgery error names the offending field
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_forgery_error_names_the_offending_field() -> None:
(error,) = formal_claim_forgery_errors({FORMAL_CLAIM_KEY: True}, context="bundle.honesty")
assert error.startswith(f"bundle.honesty.{FORMAL_CLAIM_KEY}")python -m pytest "packages/omnibias-core/tests/test_proof_machine.py::test_forgery_error_names_the_offending_field" -qRegression example · honest artifact declares nothing and passes
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_honest_artifact_declares_nothing_and_passes() -> None:
assert formal_claim_forgery_errors({FORMAL_CLAIM_KEY: False}) == []
assert formal_claim_forgery_errors({}) == []
assert formal_claim_forgery_errors(None) == []python -m pytest packages/omnibias-core/tests/test_proof_machine.py -k test_honest_artifact_declares_nothing_and_passes -qRead the implementation
def formal_claim_forgery_errors(
honesty: Mapping[str, Any] | None,
*,
certificate: Certificate | None = None,
context: str = "honesty",
) -> list[str]:
"""Reject a *self-declared* ``theorem_prover_verified``.
:data:`FORMAL_CLAIM_KEY` is **earned** by a genuine Lean kernel pass, never
asserted by the artifact that benefits from it. :meth:`ProofMachine.evaluate`
already enforces that for conjectures, but any consumer that reads the flag
straight out of a *stored* bundle (a JSON file on disk, which anyone can edit)
would trust the artifact's own word for it. That is the one shape in which the
claim can be forged, so validators call this helper and treat a non-empty
result as a schema error.
A truthy declaration is accepted only when ``certificate`` is supplied *and*
the kernel genuinely verifies its obligation. With no Lean toolchain present
the bridge reports unverified, so the flag stays refused -- graceful
degradation must never become silent acceptance.
Parameters
----------
honesty:
The artifact's ``honesty`` mapping (``None`` and non-mappings are treated
as declaring nothing).
certificate:
The certificate whose finite obligation the kernel should re-check. Omit
it to refuse every truthy declaration outright.
context:
Dotted prefix used in the message, so the caller's schema report points at
the offending field.
Returns
-------
list[str]
Empty when nothing is declared or the declaration is kernel-backed;
otherwise a single explanatory error.
"""
if not isinstance(honesty, Mapping) or not bool(honesty.get(FORMAL_CLAIM_KEY, False)):
return []
if certificate is not None:
from omnibias.core.proof.lean_check import check_certificate
if check_certificate(certificate).verified:
return []
return [
f"{context}.{FORMAL_CLAIM_KEY} is declared true but no Lean kernel pass "
"supports it; the flag is earned by a genuine `lake build`, never asserted "
"by the artifact claiming it"
]honesty_gate
omnibias.core.proof.honesty_gateSource ↗honesty_gate(conjecture: Conjecture, certificate: Certificate | None) -> boolTrue iff every asserted honesty claim is backed by the certificate.
An asserted claims[key] == True requires certificate["honesty"][key]
to be truthy. No assertions (the default) always passes.
Parameters
| Name | Type & default | Contract |
|---|---|---|
conjecturepositional-or-keyword | ConjectureRequired | See the operation contract and implementation below. |
certificatepositional-or-keyword | Certificate | NoneRequired | See the operation contract and implementation below. |
boolExecuted regression · machine accepts valid sealed certificate
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_machine_accepts_valid_sealed_certificate() -> None:
machine = ProofMachine().register(_sealed_prover(tamper=False))
verdict = machine.evaluate(Conjecture("x", "sealed", {}))
assert verdict.status == "PROVED"
assert verdict.schema_ok is Truepython -m pytest "packages/omnibias-core/tests/test_certificate_audit_regressions.py::test_machine_accepts_valid_sealed_certificate" -qRegression example · honesty gate still ignores the formal claim
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_honesty_gate_still_ignores_the_formal_claim() -> None:
"""The conjecture-side rule and the artifact-side rule must agree."""
cert: Certificate = {"honesty": {FORMAL_CLAIM_KEY: False}}
conjecture = Conjecture("x", "k", {}, claims={FORMAL_CLAIM_KEY: True})
# honesty_gate defers to ProofMachine.evaluate, which consults the kernel.
assert honesty_gate(conjecture, cert) is Truepython -m pytest packages/omnibias-core/tests/test_proof_machine.py -k test_honesty_gate_still_ignores_the_formal_claim -qRead the implementation
def honesty_gate(conjecture: Conjecture, certificate: Certificate | None) -> bool:
"""``True`` iff every asserted honesty claim is backed by the certificate.
An asserted ``claims[key] == True`` requires ``certificate["honesty"][key]``
to be truthy. No assertions (the default) always passes.
"""
if not conjecture.claims:
return True
honesty: Mapping[str, Any] = {}
if certificate is not None:
candidate = certificate.get("honesty", {})
if isinstance(candidate, Mapping):
honesty = candidate
for key, asserted in conjecture.claims.items():
if key == FORMAL_CLAIM_KEY:
continue # earned by the Lean kernel, not a certificate honesty flag
if asserted and not bool(honesty.get(key, False)):
return False
return Truekernel_earned_theorem_prover_verified
omnibias.core.proof.kernel_earned_theorem_prover_verifiedSource ↗kernel_earned_theorem_prover_verified(bundle: Mapping[str, Any]) -> boolWhether a Lean kernel pass backs bundle -- never trust honesty self-claims.
Looks for a sealed v1 certificate under bundle["certificate"], or treats
bundle itself as the certificate when it already carries a digest+payload.
Calls ~omnibias.core.proof.lean_check.check_certificate in either case
(degrades to False when Lean is absent or the digest is missing/mismatched).
Parameters
| Name | Type & default | Contract |
|---|---|---|
bundlepositional-or-keyword | Mapping[str, Any]Required | See the operation contract and implementation below. |
boolRead the implementation
def kernel_earned_theorem_prover_verified(bundle: Mapping[str, Any]) -> bool:
"""Whether a Lean kernel pass backs ``bundle`` -- never trust honesty self-claims.
Looks for a sealed v1 certificate under ``bundle["certificate"]``, or treats
``bundle`` itself as the certificate when it already carries a digest+payload.
Calls :func:`~omnibias.core.proof.lean_check.check_certificate` in either case
(degrades to ``False`` when Lean is absent or the digest is missing/mismatched).
"""
cert: Mapping[str, Any] | None = None
nested = bundle.get("certificate")
if isinstance(nested, Mapping):
cert = nested
elif isinstance(bundle.get("digest"), str) and isinstance(bundle.get("payload"), Mapping):
cert = bundle
if cert is None:
return False
return bool(check_certificate(cert).verified)