symfonic.kernel.contracts.run_admission

run_admission

Inherited erase admissions, proved once when a kernel run starts (CORE-199/194).

A capability that captures an erase admission per kernel run (keyed on its :class:~symfonic.kernel.contracts.run_identity.RunLineage) declares a prover here. The kernel calls every declared prover before a run's first stage, so a run descending from a capture a forget has since covered refuses before any prompt-assembly stage, provider call, tool or effect -- whether or not the run composes that capability itself. A worker that composes no memory at all is held to the captures of the runs it was started inside.

The kernel imports no memory runtime: a prover is declared by the module that keeps the captures, when it is imported. A process that never imported one holds no capture, so there is nothing to prove. A prover receives the run's whole ancestry and proves only captures recorded on those lineages, each on its capturing ancestor's own store; a run with no lineage -- one started outside any run -- inherits nothing.

A capture lives on stores bound to the loop its run was issued on. A run on another loop -- work a worker hands to a thread running its own loop -- does not drive those stores from there (review P2-1): each ancestor is proved on its own loop, through run_coroutine_threadsafe. An owner loop that no longer runs is proved here, where a store bound to it fails typed; one that does not answer within :data:OWNER_LOOP_TIMEOUT refuses. Neither skips.

A run whose lineage is unresolved -- it names a parent or root never issued in this process, or one released since -- cannot show which captures it inherits, so it refuses after the provers, even where none is declared (a process that never imported memory). That holds a recovered pause, whose paused run has ended: no persisted proof names it, and dropping a capability from the composition does not make it provable (CORE-194 owner rule). A prover may refuse it first with its own typed error. A run naming nothing is a root and a run naming a live run descends from it: both are admitted.

One persisted proof exists (CORE-194 owner answer, 2026-10-15): a pause minted by a live, resolved, parentless run on whose lineage no declared witness reports a capture. :func:provable_root is what continuation_attestation asks before it seals that proof; that module alone admits a verified one. A prover declared without a witness makes every run unprovable as a root.

declare_inherited_admission

declare_inherited_admission(prover: InheritedAdmissionProver, *, captured: CaptureWitness | None = None) -> None

Declare prover for every run started from now on; idempotent.

captured answers whether the module holds a capture on given runs; without it no run can be proved a capture-free root (:func:provable_root).

Source code in src/symfonic/kernel/contracts/run_admission.py

def declare_inherited_admission(
    prover: InheritedAdmissionProver, *, captured: CaptureWitness | None = None
) -> None:
    """Declare ``prover`` for every run started from now on; idempotent.

    ``captured`` answers whether the module holds a capture on given runs;
    without it no run can be proved a capture-free root (:func:`provable_root`).
    """
    if prover not in _PROVERS:
        _PROVERS.append(prover)
    if captured is not None:
        _WITNESSES[prover] = captured

memory_in

memory_in(effects: Any, stages: Any) -> bool

Whether compiled authority reaches memory; unreadable authority does.

Source code in src/symfonic/kernel/contracts/run_admission.py

def memory_in(effects: Any, stages: Any) -> bool:
    """Whether compiled authority reaches memory; unreadable authority does."""
    try:
        families = set(effects)
        families.update(effect for stage in stages for effect in stage.effects)
    except Exception:  # noqa: BLE001 - cannot be read, cannot be proved memory-free
        return True
    return any(str(family).startswith("memory") for family in families)

provable_root

provable_root(run_id: str) -> bool

Whether the running run is run_id, a resolved root no capture is held on.

True only for the issued lineage of run_id itself -- not a child, a spawned worker, a recovered or unresolved run -- stamped memory-free from its compiled plan with no descendant that touched memory, and only when every declared prover has a witness and none reports a capture on it.

Source code in src/symfonic/kernel/contracts/run_admission.py

def provable_root(run_id: str) -> bool:
    """Whether the running run is ``run_id``, a resolved root no capture is held on.

    True only for the issued lineage of ``run_id`` itself -- not a child, a
    spawned worker, a recovered or unresolved run -- stamped memory-free from
    its compiled plan with no descendant that touched memory, and only when
    every declared prover has a witness and none reports a capture on it.
    """
    from symfonic.kernel.contracts.run_identity import _ISSUED, current_run_lineage

    lineage = current_run_lineage()
    if (
        not run_id
        or lineage is None
        or lineage.run_id != run_id
        or lineage.parents
        or lineage.unresolved
        or lineage.memory is not False
        or _ISSUED.get(run_id) is not lineage
    ):
        return False
    runs = (lineage,)
    for prover in tuple(_PROVERS):
        witness = _WITNESSES.get(prover)
        if witness is None or witness(runs):
            return False
    return True

prove_ancestry_of async

prove_ancestry_of(lineage: Any) -> None

Prove lineage's ancestry now, each run on its owner loop, as a run start does.

For a capability about to make a durable effect on behalf of a run that has not started yet, from a task whose context does not carry that run: it passes the lineage its run will descend from, so a stale capture refuses before the effect instead of after it. It refuses nothing a run start would not; the run's own start still proves it again.

Source code in src/symfonic/kernel/contracts/run_admission.py

async def prove_ancestry_of(lineage: Any) -> None:
    """Prove ``lineage``'s ancestry now, each run on its owner loop, as a run start does.

    For a capability about to make a durable effect on behalf of a run that has
    not started yet, from a task whose context does not carry that run: it
    passes the lineage its run will descend from, so a stale capture refuses
    before the effect instead of after it. It refuses nothing a run start would
    not; the run's own start still proves it again.
    """
    if lineage is not None and _PROVERS:
        from symfonic.kernel.contracts.run_identity import run_ancestry

        await _prove_owned(run_ancestry(lineage))

prove_inherited async

prove_inherited() -> None

Refuse unless every capture the running run inherits is still current.

Source code in src/symfonic/kernel/contracts/run_admission.py

async def prove_inherited() -> None:
    """Refuse unless every capture the running run inherits is still current."""
    from symfonic.kernel.contracts.run_identity import current_run_lineage, run_ancestry

    lineage = current_run_lineage()
    if lineage is None:
        return
    if _PROVERS:
        await _prove_owned(run_ancestry(lineage))
    if lineage.unresolved:
        from symfonic.core.contracts.errors import ContractViolationError

        raise ContractViolationError(UNPROVABLE_LINEAGE)

refuse_unprovable

refuse_unprovable(*run_ids: str | None) -> None

Refuse now if a run naming run_ids as parent or root could not prove them.

For a host about to spend a pause before the resumed run starts: that run would refuse at its start (:func:prove_inherited), so asking first keeps the pause unspent. A named id must belong to a run issued here and alive.

Source code in src/symfonic/kernel/contracts/run_admission.py

def refuse_unprovable(*run_ids: str | None) -> None:
    """Refuse now if a run naming ``run_ids`` as parent or root could not prove them.

    For a host about to spend a pause before the resumed run starts: that run
    would refuse at its start (:func:`prove_inherited`), so asking first keeps
    the pause unspent. A named id must belong to a run issued here and alive.
    """
    if unprovable(*run_ids):
        from symfonic.core.contracts.errors import ContractViolationError

        raise ContractViolationError(UNPROVABLE_LINEAGE)

unprovable

unprovable(*run_ids: str | None) -> bool

Whether :func:refuse_unprovable would refuse run_ids now.

Source code in src/symfonic/kernel/contracts/run_admission.py

def unprovable(*run_ids: str | None) -> bool:
    """Whether :func:`refuse_unprovable` would refuse ``run_ids`` now."""
    from symfonic.kernel.contracts.run_identity import _ISSUED

    return any(run_id and _ISSUED.get(run_id) is None for run_id in run_ids)