What Survives a Crash

Overview

A governed call can be interrupted anywhere. The process is killed, the future is dropped, a caller cancels, a panic unwinds. The question a reader should be able to answer is narrow and uncomfortable: can a side effect exist that no receipt records?

The kernel answers it by splitting on whether the tool-server dispatch await has been entered. Before that moment nothing reached the tool server, so every pre-execution mutation is reversed and a clean unwind writes no receipt at all. After that moment the tool may have run, so the kernel refuses to release anything and always writes a signed record of the call it cannot account for.

Model

The bit, and where it is set

PostAdmissionDropGuard is constructed once an evaluation has been admitted and holds the request, the capability, the pre-execution budget mutation, the payment authorization, the buffered child receipts, and the durable operation. It carries two booleans that decide its own destructor: armed, cleared on the normal exit, and dispatch_started.

    /// Mark that the tool-server dispatch await has been entered. After this
    /// point a dropped future may correspond to an executed side effect, so
    /// the drop path must record a cancellation receipt and fail closed on
    /// reservations.
    pub(crate) fn mark_dispatch_started(&mut self) {
        self.dispatch_started = true;
    }

The call site puts the bit exactly where the meaning changes. In async_evaluation_core.rs the guard is built with its durable operation attached, mark_dispatch_started() runs on the next line, and the line after that is the await on dispatch_resolved_server_within_budget. Nothing between the flag and the await can reach a tool server, and nothing after the await can be assumed not to have.

impl Drop for PostAdmissionDropGuard<'_> {
    fn drop(&mut self) {
        if !self.armed {
            return;
        }

        if !self.dispatch_started {
            // Pre-dispatch drop (or a panic unwinding before dispatch).
            // Nothing was written to the tool server, so no side effect is
            // possible: fully reverse every pre-execution mutation. A clean
            // unwind records NO cancellation receipt; a cleanup fault records
            // a signed fault receipt (see `handle_pre_dispatch_drop`).
            self.handle_pre_dispatch_drop();
            return;
        }

The durable operation record

An admitted call also has a durable identity. AdmissionOperationV1 holds a binding, its attachments, a state, a dispatch state, an optional dispatch-commit binding, a coordinator lease epoch, a monotonic version, the last error, and a terminal replay record. The state is one of 18 variants, 7 of them terminal and 7 of them before dispatch.

pub enum AdmissionOperationState {
    Prepared,
    BrokerAttemptRegistered,
    ApprovalRequired,
    BudgetAuthorized,
    ApprovalReserved,
    ReadyToDispatch,
    CapturePending,
    DispatchCommitted,
    Finalizing,
    Completed,
    CompensatedBeforeDispatch,
    NotAcceptedAfterDispatchCommit,
    OutcomeUnknownAfterDispatch,
    /// The delivered output did not match a grant's committed output
    /// digest. A signed Deny is persisted; the open hold is released and
    /// zero is captured.
    DeniedAfterDelivery,
    MutationReady,
    MutationSubmitted,
    EconomicMutationApplied,
    EconomicMutationNotApplied,
}

The reason the bands carry no arrows is worth reading in the source. Legality for a dispatch operation is computed, not looked up: which transitions exist depends on whether the operation requires a broker attempt, a budget capture, or an approval.

pub(super) fn is_legal_transition(
    kind: AdmissionOperationKind,
    requirements: AdmissionParticipantRequirements,
    from: AdmissionOperationState,
    to: AdmissionOperationState,
) -> bool {
    if kind == AdmissionOperationKind::GovernedEconomicMutation {
        return matches!(
            (from, to),
            (
                AdmissionOperationState::Prepared,
                AdmissionOperationState::MutationReady
            ) | (
                AdmissionOperationState::MutationReady,
                AdmissionOperationState::MutationSubmitted
            ) | (
                AdmissionOperationState::Prepared
                    | AdmissionOperationState::MutationReady
                    | AdmissionOperationState::MutationSubmitted,
                AdmissionOperationState::EconomicMutationNotApplied
            ) | (
                AdmissionOperationState::MutationSubmitted,
                AdmissionOperationState::EconomicMutationApplied
            )
        );
    }
    if !kind.uses_dispatch() {
        return false;
    }
    if to == AdmissionOperationState::CompensatedBeforeDispatch {
        return from.is_pre_dispatch() && predispatch_state_enabled(requirements, from);
    }
    let ready_source = if requirements.approval {
        AdmissionOperationState::ApprovalReserved
    } else if requirements.budget_capture {
        AdmissionOperationState::BudgetAuthorized
    } else {
        AdmissionOperationState::Prepared
    };
    match to {
        AdmissionOperationState::BrokerAttemptRegistered => {
            requirements.broker_attempt && from == AdmissionOperationState::Prepared
        }
        AdmissionOperationState::BudgetAuthorized => {
            requirements.budget_capture
                && ((requirements.approval && from == AdmissionOperationState::ApprovalRequired)
                    || from
                        == if requirements.broker_attempt {
                            AdmissionOperationState::BrokerAttemptRegistered
                        } else {
                            AdmissionOperationState::Prepared
                        })
        }
        AdmissionOperationState::ApprovalRequired => {
            requirements.budget_capture
                && requirements.approval
                && from
                    == if requirements.broker_attempt {
                        AdmissionOperationState::BrokerAttemptRegistered
                    } else {
                        AdmissionOperationState::Prepared
                    }
        }
        AdmissionOperationState::ApprovalReserved => {
            requirements.approval
                && from
                    == if requirements.budget_capture {
                        AdmissionOperationState::BudgetAuthorized
                    } else {
                        AdmissionOperationState::Prepared
                    }
        }
        AdmissionOperationState::ReadyToDispatch => {
            from == ready_source
                || (kind == AdmissionOperationKind::ToolDispatch
                    && requirements.budget_capture
                    && requirements.approval
                    && from == AdmissionOperationState::BudgetAuthorized)
        }
        AdmissionOperationState::CapturePending => {
            requirements.budget_capture && from == AdmissionOperationState::ReadyToDispatch
        }
        AdmissionOperationState::DispatchCommitted => {
            from == if requirements.budget_capture {
                AdmissionOperationState::CapturePending
            } else {
                AdmissionOperationState::ReadyToDispatch
            }
        }
        AdmissionOperationState::Finalizing
        | AdmissionOperationState::NotAcceptedAfterDispatchCommit
        | AdmissionOperationState::OutcomeUnknownAfterDispatch => {
            from == AdmissionOperationState::DispatchCommitted
                || (to == AdmissionOperationState::OutcomeUnknownAfterDispatch
                    && from == AdmissionOperationState::Finalizing)
        }
        AdmissionOperationState::Completed => from == AdmissionOperationState::Finalizing,
        // A delivery-digest mismatch is decided during finalization, so
        // the only legal predecessor is Finalizing.
        AdmissionOperationState::DeniedAfterDelivery => from == AdmissionOperationState::Finalizing,
        _ => false,
    }
}

The other kind that shares the enum does have a closed table. A governed economic mutation moves between 5 states over 6 legal moves, and the figure draws them because the source enumerates them.

How it works

Before dispatch, everything reverses

handle_pre_dispatch_drop runs four reversal steps, each attempted independently so one failure does not abandon the rest, and collects the failures rather than returning them. A destructor cannot propagate an error, so best-effort with collected faults is the only honest shape.

1. Monetary hold reversal. When the budget mutation produced a charge result, the budget charge and the payment authorization are unwound together. A failure records the budget hold id and the payment authorization id.
2. Invocation-only budget reversal. A non-monetary grant with max_invocations incremented a counter at admission. That increment is reversed so a call that never dispatched does not permanently consume a slot. The step is gated on the Invocation variants so a charge already handled by step one is not reversed twice.
3. Runtime-admission reservation release. The reserved destructive lease, treaty continuation, and swarm continuation ids are read out of the admission metadata and released. A failure names those ids so an operator can find a reservation that is stuck.
4. Delegated child-budget lease release. Released only when this evaluation actually took a lease. The release is reference-counted: it decrements the holder count and frees the edge, returning the share to the parent, only when this was the last holder.

If every step succeeded and the call had a durable operation, the guard terminalizes it through compensate_durable_admission_after_pre_dispatch_cleanup, which refuses if the stored operation has changed, has already reached a terminal state, or carries a dispatch commit. A clean unwind writes no cancellation receipt; that receipt-free exit is the intended one. Any fault at all flips that: the guard records a signed cancellation receipt whose chio_runtime metadata carries pre_dispatch_cleanup_failed and one entry per failing step, each with its step name, redacted reason, and the hold ids it was unwinding.

Which pre-dispatch states can reverse is itself a predicate over the participants, for the same reason the transition table is.

pub(super) fn predispatch_state_enabled(
    requirements: AdmissionParticipantRequirements,
    state: AdmissionOperationState,
) -> bool {
    match state {
        AdmissionOperationState::Prepared | AdmissionOperationState::ReadyToDispatch => true,
        AdmissionOperationState::BrokerAttemptRegistered => requirements.broker_attempt,
        AdmissionOperationState::ApprovalRequired => {
            requirements.budget_capture && requirements.approval
        }
        AdmissionOperationState::BudgetAuthorized | AdmissionOperationState::CapturePending => {
            requirements.budget_capture
        }
        AdmissionOperationState::ApprovalReserved => requirements.approval,
        _ => false,
    }
}

After dispatch, the call is recorded

The post-dispatch branch does three different things, in an order that matters.

1. Buffered child receipts flush first. The nested-flow bridge buffers already-signed child receipts inside the guard rather than on the evaluation stack frame, precisely so a post-dispatch drop can still write them. The child operations completed and were signed before the parent was canceled, so on an append-only log they precede the parent cancellation receipt. Discarding them with the dropped future would leave completed child requests off the log. Each receipt is recorded independently, a failure logs an audit_fault and does not abandon the receipts queued behind it, and the buffer is drained unconditionally so a later drop cannot re-record.
2. Reservations are retained, and a receipt is always written. The guard does not release the runtime-admission reservations it would have released before dispatch. Releasing a single-use destructive lease here would license a replay of an effect that may already have happened. The retained reservations are marked in the receipt metadata so the burned lease is auditable and an operator can recover it deliberately. A signed cancellation receipt is recorded unconditionally, carrying the reason constant for the branch that produced it.
3. The durable operation is terminalized. The dispatch commit landed but the return never did, so without this the operation would stay non-terminal and reject every replay of that request id until the next startup sweep. terminalize_dispatch_committed_admission commits outcome_unknown_after_dispatch and refuses outright if a durable tool outcome already exists, so it cannot overwrite a return that did complete. Startup recovery calls the same function.

Four reason constants name the branches, and they are the strings a reader will find in the receipt.

const POST_ADMISSION_DROP_REASON: &str = "tool evaluation future dropped after admission";
const POST_DISPATCH_CREDENTIAL_COMMIT_FAILURE_REASON: &str =
    "dispatch credential commit failed after tool execution";
const POST_DISPATCH_URL_ELICITATION_REASON: &str =
    "tool server returned URL elicitation after dispatch; outcome is unknown";
const PRE_DISPATCH_CLEANUP_FAULT_REASON: &str =
    "tool evaluation future dropped before dispatch with cleanup fault";

Exactly once, and what enforces it

Recording an ambiguous outcome is only half the problem. The other half is making sure a retry of the same call cannot execute twice. That is the execution nonce: a short-lived, single-use token the kernel attaches to an allow response, which a tool server presents before executing. The kernel rejects a nonce that is stale past nonce_ttl_secs or already replayed, which closes the window between evaluate() and tool-server execution that DPoP alone leaves open.

The nonce body binds an opaque nonce_id to the exact tuple of subject, capability, server, tool, request_id, and parameter_hash, so substituting a nonce between unrelated calls fails the binding check. The kernel signs the whole body with its receipt-signing key, so a tool server verifies authenticity without a round trip. Replay is prevented by the store.

/// Persistence boundary for replay-prevention of execution nonces.
///
/// Implementations MUST ensure that `reserve(nonce_id)` returns `true`
/// exactly once per nonce identifier. All subsequent calls for the same
/// identifier return `false`. Fail-closed: any internal error is returned
/// via `KernelError` so the caller can deny the request.
pub trait ExecutionNonceStore: Send + Sync {
    /// Attempt to reserve (consume) the given nonce identifier.
    ///
    /// * `Ok(true)`  -- nonce was fresh; it is now marked consumed.
    /// * `Ok(false)` -- nonce has already been consumed (replay detected).
    /// * `Err(_)`    -- the store is unreachable or corrupted; fail-closed.

A durable store must retain the consumed marker at least as long as the signed nonce stays valid, which is why reserve_until takes the signed expiry: a row pruned early would let the nonce be replayed inside its remaining validity window. A store that advertises supports_dispatch_reservations can also take an owned reservation before dispatch and roll it back afterward, but only the owner may roll it back, and only after a failure known to precede any tool side effect. A store that does not advertise the capability returns an error from rollback_dispatch_reservation rather than guessing.

Guarantees and limits

Status: shipped, in chio-kernel. The guarantees below are the destructor's two branches and the admission state machine; the limits are what those two branches do not promise.

• No unrecorded side effect after dispatch. Once the dispatch await is entered, the drop path always records a signed cancellation receipt, and the buffered child receipts are flushed onto the append-only log first so the ordering on the log matches the ordering of the operations.
• No burned budget before dispatch. A drop before the await reverses the monetary hold, the invocation counter, the runtime-admission reservations, and the delegated child-budget lease. A clean reversal writes no receipt, so the absence of a receipt for an admitted call means the four reversals succeeded.
• A stuck hold is on the log, not lost. Any reversal failure produces a signed receipt naming the failing step and the hold or reservation ids that step was unwinding, so an operator locates the stuck hold from the receipt rather than by cross-referencing admission metadata.
• Ambiguity is recorded as ambiguity. A post-dispatch drop terminalizes the durable operation at outcome_unknown_after_dispatch rather than at completed or compensated_before_dispatch. The receipt says the outcome is unknown, because it is.
• Limit: reservations are retained, not resolved. Failing closed after dispatch means a single-use destructive lease stays consumed even when the tool never ran. That is a deliberate choice against replay, and recovering the lease is an operator action taken against the receipt metadata that records it.
• Limit: the drop path is best-effort. A destructor cannot return an error or panic. If even the cancellation receipt cannot be recorded, the guard logs with an audit_fault field and continues. Receipt durability past that point is a property of the receipt store, not of the guard.
• Limit: the nonce store must be durable to survive a restart. The in-memory store is an LRU cache keyed on the nonce id. Exactly-once across a process restart requires a store that persists the consumed marker until the signed expiry.
• Limit: the nonce is installed, not implied. The feature turns on when a deployment installs an ExecutionNonceConfig. With no config installed the kernel mints no nonce. With one installed and require_nonce left at its default of false, allow responses carry nonces and dispatch verifies any nonce presented, but a caller that omits one still works. Setting require_nonce makes every execution-bound dispatch present a fresh nonce.

Next steps

• Receipts · the signed record every branch here writes
• Node State on Disk · the stores that hold the admission record and the nonce
• Failure & Recovery · the startup sweep that terminalizes what a crash left open
• Budgets & Metering · holds, reconciliation, and the execution nonce in the money path
• Determinism and Replay · replaying a receipt log against the current build