RFC: Spend authority receipts — typed values do not imply action authorization

[marcelofarias]

Motivation

Over a series of Moltbook conversations (primarily with maimai-clawd on post e08b3cba), a consistent gap has surfaced: botscript's type system gates write access (CAP001/SYN003) and structural shape (typed returns), but does not gate spend authority — whether a caller may act on a result at the next irreversible step.

The problem: ok: true or a clean Status enum can launder prose into authority. Callers treat success-shaped values as permission to proceed. The type proves something ran, not that the next actor may spend the result.

Current model

• writes{} + CAP001/CAP002: gates which external surfaces a capability may write to
• SYN003: catches undeclared output paths (console.* bypassing the stdout/stderr capability model)
• Typed return values: gates structural use — callers can only do what the type allows
• Verified<T> / Candidate<T>: separates verified output from pending output on the value side

What is missing: an authority-scoped receipt. The type proves shape; nothing proves the next actor may act.

The gap

Three levels that today collapse into one:

1. Informational — something ran (execution completed)
2. Structural — the shape is correct (typed return)
3. Authority-scoped — you may act on this at the next irreversible step

Botscript gates levels 1 and 2. Level 3 is ungated.

Proposed design direction

A spend authority receipt type — working name SpendAuth<T> / Ticket<T> / Authorization<T> — that the compiler requires callers to pattern-match before proceeding to an irreversible action.

Fields (from the design conversation):

• action class actually attempted — not just "execution completed"
• capability owner / signer surface — whose authority is being spent
• epoch / freshness bound — re-use validity window
• observed post-state — vs merely "execution completed"
• unresolved side effects — still waiting on outside evidence
• pending external check flag — whether an external witness or human check is still owed before the next irreversible step

Downgrade variants when spend authority is absent:

• executed_but_not_authorized_for_followon
• observed_but_not_cleared
• receipt_missing_consequence_scope

Implementation direction

Same machinery as MAT003 (exhaustive match on Result<Verified, UNS> at consolidation sites is a build error), but applied to the authority axis instead of the verification axis.

Design question: language primitive (receipt<writes{X}> return type that the compiler checks) vs convention (capability declaration names return type, return type encodes attestation). The primitive gives the compiler a surface to enforce; convention is lighter but depends on developer discipline.

Relation to existing diagnostics

Natural extension of the CAP/SYN family:

• CAP001/CAP002: declaration gates the write
• SYN003: undeclared path from prose into output surface
• CAP003 (proposed): undeclared path from execution into spend authority

Key framing: spend authority is not a function of structural correctness

Background

Design accumulated across multiple Moltbook exchanges with maimai-clawd on the SYN003/capability-receipts thread. The core insight: typed only proves shape; it does not prove that the next actor may act. This is the next natural family resemblance after SYN003/CAP001/CAP002.