symfonic.capabilities.memory.erase_admission

erase_admission

Explicit erase admissions for raw PostgreSQL v1 memory mutations (CORE-199 P3-4).

Every admin forget's memory erase, memory-only or joint, advances a forward-only generation row in the memory database itself, in the transaction that deletes the content (postgres_memory_generation). A joint forget's transcript erase also advances one in the log's database (postgres_conversation_generation). Every raw graph-only PostgreSQL v1 write, flush and discard then reads, under the tenant mutation lock the memory erase also takes, the memory generations covering its own scope on its own connection -- the durable proof, independent of process and pool object -- and the conversation generations on memory's own pool and on every log pool memory_capabilities composed with that pool in this process. The mutation must account for each covering row with an :class:Admission:

• An admission is a value -- the generations its holder observed before it read -- and is presented for one call through :func:admitted. It is never inherited from a run's ambient context, so a task that strips its context loses nothing it could present, and a task that keeps an admission keeps an old one, which refuses.
• A mutation without an admission accounts for nothing: it may not write into a scope any completed admin forget covers.
• A pool memory_capabilities composed a fenced turn over requires one (:func:require_admission): every mutation through it must present a memory fence on that pool, or run inside a kernel run that captured one. Code that strips its context, or a caller holding the composition's store outside any run, refuses rather than writing what a turn read anywhere -- a sibling, a parent, or the erased scope itself (CORE-199 review F1).

Admissions are minted only by a turn's capture before it reads (turn_generation); nothing public mints one. The admin service's own writes present the running turn's admission, and a caller with none -- outside any run, or in a run that captured nothing -- refuses: a contextless caller never observes a fresh one (CORE-199 review F2, owner decision). Nothing is admitted by absence.

Admission

Admission(fences: Iterable[Fence], *, _mint: object = None)

The fences a mutation presents; immutable and not constructible by callers.

Source code in src/symfonic/capabilities/memory/erase_admission.py

def __init__(self, fences: Iterable[Fence], *, _mint: object = None) -> None:
    if _mint is not _MINT:
        raise MemoryContractError(FORGED)
    self._fences = tuple(fences)

AdmittedMemory

AdmittedMemory(store: Any, admission: Admission)

A store's mutations, each presenting one fixed admission.

Source code in src/symfonic/capabilities/memory/erase_admission.py

def __init__(self, store: Any, admission: Admission) -> None:
    if type(admission) is not Admission:
        raise MemoryContractError(FORGED)
    self._store = store
    self._admission = admission

Fence dataclass

Fence(pool: Any, path: str, token: tuple[tuple[str, int], ...], tolerant: bool, memory: bool = False)

The generations covering path on one authority, when observed.

memory fences hold memory_erase_generations rows, read on the memory database; the others hold a conversation generation table's.

admitted

admitted(admission: Admission) -> Iterator[None]

Present admission to the mutations made inside this call.

Source code in src/symfonic/capabilities/memory/erase_admission.py

@contextmanager
def admitted(admission: Admission) -> Iterator[None]:
    """Present ``admission`` to the mutations made inside this call."""
    if type(admission) is not Admission:
        raise MemoryContractError(FORGED)
    token = _ADMITTED.set(admission)
    try:
        yield
    finally:
        _ADMITTED.reset(token)

authorities

authorities(pool: Any) -> tuple[tuple[Any, bool], ...]

(authority, tolerant): memory's own pool first, then bound logs.

Source code in src/symfonic/capabilities/memory/erase_admission.py

def authorities(pool: Any) -> tuple[tuple[Any, bool], ...]:
    """``(authority, tolerant)``: memory's own pool first, then bound logs."""
    return ((pool, True), *((log, False) for log in _LOGS.get(pool, ())))

bind_log

bind_log(pool: Any, log_pool: Any) -> None

Make log_pool an authority for every mutation through pool.

Source code in src/symfonic/capabilities/memory/erase_admission.py

def bind_log(pool: Any, log_pool: Any) -> None:
    """Make ``log_pool`` an authority for every mutation through ``pool``."""
    logs = _LOGS.setdefault(pool, [])
    if log_pool is not pool and not any(known is log_pool for known in logs):
        logs.append(log_pool)

carries

carries(pool: Any, fences: Iterable[Fence]) -> bool

Some fence in fences is a memory capture on pool itself.

Source code in src/symfonic/capabilities/memory/erase_admission.py

def carries(pool: Any, fences: Iterable[Fence]) -> bool:
    """Some fence in ``fences`` is a memory capture on ``pool`` itself."""
    return any(fence.memory and fence.pool is pool for fence in fences)

memory_pool

memory_pool(store: Any) -> Any

The PostgreSQL pool a store's mutation fence locks on, or None.

Source code in src/symfonic/capabilities/memory/erase_admission.py

def memory_pool(store: Any) -> Any:
    """The PostgreSQL pool a store's mutation fence locks on, or None."""
    from symfonic.capabilities.memory.mutations import _PostgresMutationFence

    fence = getattr(store, "_mutations", None)
    return fence._pool if type(fence) is _PostgresMutationFence else None  # noqa: SLF001

observe_all async

observe_all(pool: Any, path: str, *, strict: bool = True) -> tuple[Fence, ...]

Memory's own generations first, then each conversation authority's.

strict (a turn) refuses where the memory generation table is absent.

Source code in src/symfonic/capabilities/memory/erase_admission.py

async def observe_all(pool: Any, path: str, *, strict: bool = True) -> tuple[Fence, ...]:
    """Memory's own generations first, then each conversation authority's.

    ``strict`` (a turn) refuses where the memory generation table is absent.
    """
    from symfonic.memory.backends.postgres_conversation_generation import observe
    from symfonic.memory.backends.postgres_memory_generation import capture

    memory = Fence(pool, path, await capture(pool, path, strict=strict), not strict, True)
    return (
        memory,
        *[
            Fence(authority, path, await observe(authority, path, tolerant=tolerant), tolerant)
            for authority, tolerant in authorities(pool)
        ],
    )

require_admission

require_admission(pool: Any) -> None

Refuse every later mutation through pool that carries no admission.

Only ever adds a refusal, for the life of the pool object.

Source code in src/symfonic/capabilities/memory/erase_admission.py

def require_admission(pool: Any) -> None:
    """Refuse every later mutation through ``pool`` that carries no admission.

    Only ever adds a refusal, for the life of the pool object.
    """
    _REQUIRED.add(pool)

require_mutation async

require_mutation(pool: Any, path: str | None, ambient: Iterable[Fence]) -> None

Called by the PostgreSQL mutation fence after its tenant lock.

Re-proves every presented and ambient fence exactly, accounts for every generation covering path on every authority, and refuses a fenced pool's mutation that carries no fence on it -- after the memory read, so a tampered table still answers as unguarded. path is None only for mutations that name no native v1 scope.

Source code in src/symfonic/capabilities/memory/erase_admission.py

async def require_mutation(pool: Any, path: str | None, ambient: Iterable[Fence]) -> None:
    """Called by the PostgreSQL mutation fence after its tenant lock.

    Re-proves every presented and ambient fence exactly, accounts for every
    generation covering ``path`` on every authority, and refuses a fenced
    pool's mutation that carries no fence on it -- after the memory read, so
    a tampered table still answers as unguarded. ``path`` is None only for
    mutations that name no native v1 scope.
    """
    from symfonic.memory.backends.postgres_conversation_generation import require_accounted

    admission = _ADMITTED.get()
    if admission is not None or pool in _REQUIRED:
        resolved_lineage()  # the whole worker, whatever scope it writes
    presented = admission.fences if admission is not None else ()
    proved: set[tuple[int, str, tuple[tuple[str, int], ...], bool]] = set()
    for fence in (*presented, *ambient):
        key = (id(fence.pool), fence.path, fence.token, fence.memory)
        if key not in proved:
            proved.add(key)
            await _prove(fence)
    if path is None:
        return
    await _account_memory(pool, path, presented, admission is not None)  # attests first
    if pool in _REQUIRED and not carries(pool, (*presented, *ambient)):
        raise MemoryContractError(UNADMITTED)
    for authority, tolerant in authorities(pool):
        own = [fence for fence in presented if not fence.memory and fence.pool is authority]
        if any(fence.path == path for fence in own):
            continue  # proved exactly above
        accounted = frozenset(pair for fence in own for pair in fence.token)
        await require_accounted(
            authority, path, accounted, tolerant=tolerant, admitted=admission is not None
        )

resolved_lineage

resolved_lineage() -> Any

The running kernel run's lineage; refuses one that cannot be proved.

A run naming an ancestor that ended and was released may descend from a capture a forget has since covered: every fenced read and write refuses.

Source code in src/symfonic/capabilities/memory/erase_admission.py

def resolved_lineage() -> Any:
    """The running kernel run's lineage; refuses one that cannot be proved.

    A run naming an ancestor that ended and was released may descend from a
    capture a forget has since covered: every fenced read and write refuses.
    """
    from symfonic.kernel.contracts.run_identity import current_run_lineage

    lineage = current_run_lineage()
    if lineage is not None and lineage.unresolved:
        raise MemoryContractError(UNRESOLVED)
    return lineage