Semantic profile registry¶

zeroproofml.semantics packages an immutable, machine-readable profile for the real four-signed common-meadow scope. The identifiers SIG_CM:1, SCM4_EQ:1, SCM4_RANGE:1, R_SCM4:1, and Q_SCM4:1 name distinct roles; they are not interchangeable theories.

The retained profile uses direct division. SCM4_EQ is the pinned equation inventory and proof basis. SCM4_RANGE is a separate executable range predicate and is not imported into an unconditional rewrite table. CM_ALL is project-local notation.

from zeroproofml.semantics import Q_SCM4, SCM4_PROFILE, SCM4_PROFILE_HASH

assert SCM4_PROFILE.identifier == Q_SCM4.value
assert len(SCM4_PROFILE_HASH) == 64

Profile JSON rejects unknown mandatory fields and unsupported major versions. The canonical SHA-256 covers the resolved registry, including its division, sign, gauge, zero, operator, equation, conditional-rule, range, and reduct metadata. FloatingProfileId separately identifies a bounded backend/dtype refinement contract.

The refinement registry is also immutable and collision rejecting. Each floating identifier resolves to exactly one descriptor and SHA-256:

from zeroproofml.refinement import (
    REFINEMENT_PROFILE_REGISTRY_SHA256,
    PYTHON_FLOAT64_STRICT,
    resolve_refinement_profile,
)

resolved = resolve_refinement_profile(
    str(PYTHON_FLOAT64_STRICT.identifier),
    expected_sha256=PYTHON_FLOAT64_STRICT.sha256,
)
assert resolved is PYTHON_FLOAT64_STRICT
assert len(REFINEMENT_PROFILE_REGISTRY_SHA256) == 64

A descriptor that reuses a registered identifier with different contents is rejected. Experimental profiles require an explicit separate registry and are unqualified. Results, refinement reports, bundles, checkpoints, and snapshots carry both the identifier and digest when the refinement identity is load-bearing.

Custom evidence retains the immutable registry that validated it. Its compact serialization still contains the ID/hash pair, so deserialization must receive the same registry explicitly; the default loader fails closed instead of consulting mutable process-global state:

from zeroproofml.refinement import RefinementProfile, RefinementProfileRegistry
from zeroproofml.semantics import (
    ExecutionEvidence,
    FloatingProfileId,
    SemanticResult,
)

experimental_profile = RefinementProfile(
    identifier=FloatingProfileId(
        policy="experimental", dtype="float64", backend="python"
    ),
    operators=frozenset({"add"}),
)
registry = RefinementProfileRegistry((experimental_profile,), qualified=False)
evidence = ExecutionEvidence.for_profile(experimental_profile, registry=registry)
encoded = SemanticResult.computed_finite(1.0, execution_evidence=evidence).to_dict()
restored = SemanticResult.from_dict(encoded, refinement_registry=registry)

QualificationState.QUALIFIED is rejected unless the supplied immutable registry is explicitly qualification-authorized. The built-in registry is not qualification-authorized merely because its profiles ship with the package.

Loaded registry data is recursively immutable: conditional-rule dictionaries, nested metadata, and extensions cannot be mutated after their identity hash is computed. to_dict() returns an independent mutable JSON value for tooling that needs to prepare a proposed profile revision.