Skip to content

symfonic.capabilities.human.drain

drain

The drain proof: when legacy-pinned tokens have provably gone (CUT-AIR-3).

Three things have to hold before "they are gone" is a fact rather than a snapshot, and each of them is a separate refusal here so an operator reading a DrainProof learns which one is missing.

A horizon. Without a recorded retirement date there is nothing to drain to, so the count is not evidence of anything.

The deadline. Nothing issued before the horizon can outlive horizon + maximum TTL. Until that moment has passed, a token minted just before the horizon could still be redeemed, so an empty count proves nothing — the bound is what turns a count into a proof.

Reach. A count is a statement about whatever tables it was taken from. Taken from one worker's memory it cannot speak for a deployment, however empty it is, so scope travels with the verdict and a process-scoped count never reports drained.

DrainProof dataclass

DrainProof(drained: bool, outstanding: int, reason: str, horizon: float | None = None, deadline: float | None = None, scope: str = PROCESS)

Whether every legacy-pinned token has drained, and why not if not.

prove_drain

prove_drain(*, horizon: float | None, maximum_ttl_seconds: float, outstanding: int, moment: float, scope: str) -> DrainProof

The whole verdict, from four numbers and where they were counted.

Source code in src/symfonic/capabilities/human/drain.py
def prove_drain(
    *,
    horizon: float | None,
    maximum_ttl_seconds: float,
    outstanding: int,
    moment: float,
    scope: str,
) -> DrainProof:
    """The whole verdict, from four numbers and where they were counted."""
    if horizon is None:
        return DrainProof(
            drained=False,
            outstanding=outstanding,
            reason="no retirement horizon is recorded, so there is nothing to drain to",
            scope=scope,
        )
    deadline = horizon + maximum_ttl_seconds
    if outstanding:
        reason = f"{outstanding} legacy-pinned tokens are still outstanding"
    elif moment < deadline:
        reason = (
            f"the drain deadline {deadline} has not been reached; until it has, a "
            "token minted just before the horizon could still be redeemed, so an "
            "empty count proves nothing"
        )
    elif scope != DEPLOYMENT:
        reason = (
            "the deadline has passed with nothing outstanding here, but this "
            "ledger's issuance table is one process's memory: a drain proof is a "
            "statement about the deployment, and a count taken from a single "
            "worker cannot make it"
        )
    else:
        return DrainProof(
            drained=True,
            outstanding=0,
            reason="no legacy-pinned token is outstanding and none can be: the "
            "maximum lifetime has elapsed since the retirement horizon",
            horizon=horizon,
            deadline=deadline,
            scope=scope,
        )
    return DrainProof(
        drained=False,
        outstanding=outstanding,
        reason=reason,
        horizon=horizon,
        deadline=deadline,
        scope=scope,
    )