State protocols: affine tokens — an unspent (terminal) state token must not be OWN001

[PhysShell]

Описание

State-protocol tokens ([ProtocolToken] ref structs) are lowered as linear resources. A token bound to a named local and never spent is reported as OWN001. The terminal state hits this most directly: in TB-MVP-01, ShippedOrder has no transition by construction, so binding it is a finding that cannot be fixed.

OrderProtocol.WithApproved(order, approved =>
{
    var shipped = approved.Ship(now, 1);   // OWN001 today: 'shipped' is never "disposed"
});

Proposal: make state tokens affine (use at most once).

• Dropping a token stays legal: unspent is clean.
• Using a token after a transition stays an error (OWN002).
• A copy that is used stays an error (OWN005).

Мотивация / сценарий

The limit is pinned in the codebase, not discovered later:

• known gap G6, frontend/roslyn/protocol-samples/cases/G6_capability_not_spent.cs, expected ["OWN001"], with the comment "Expected once tokens are affine: clean";
• limit K1 in TB-MVP-01, samples/OrderBackend/corpus/limits/K1_named_terminal_token.cs.txt, expected ["OWN001"];
• P-010 pillar 9: "the affine view of a token (an unspent one is OWN001 today)".

The sample works around it by never binding a token it does not spend: it writes draft.Submit(now); as an expression statement. That workaround constrains the developer-facing API. The natural ShippedOrder shipped = approved.Ship(...) from the TB-MVP brief cannot be written clean.

Acceptance:

• G6 and K1 flip to [] on both engines (Python reference and Rust port), and the CLI output stays byte-identical;
• L1 (OWN002), L2 (OWN005), C8, C9 and C11a are unchanged;
• ordinary IDisposable resources stay linear: OWN001 on a leaked disposable is unchanged. The affine rule applies only to the protocol-token resource kind.

Альтернативы

• Keep linear tokens and document the expression-statement pattern. This is the current state: it works, but the terminal state stays a trap.
• Generator-side workaround. Terminal transitions would return void. That hides the state type the protocol declares, and does not fix G6 (a region whose token is never used).
• Expected scope: probably a new resource kind or a token flag in OwnIR. That is a vocabulary change, so it needs an owner ruling on an OwnIR version bump and on the T0 amendment, as with feat(ownir)!: OwnIR v2 — must-understand proven_call (H1) + T0 Amendment 2 #390.

Область

analyzer (dataflow / loans / permissions)

Refs: TB-MVP-01 (#391), docs/notes/tb-mvp-01-report.md.