TpxTransport

---- MODULE TpxTransport ---- (***************************************************************************) (* A single-caller model-inference transport seam with two providers *) (* behind one interface (model_transport_t). *) (* *) (* - ANTHROPIC speaks the caller's Messages protocol natively. *) (* - TPX speaks a foreign OpenAI-compatible protocol; the transport *) (* translates requests out and responses back, and the translation *) (* must be a bijection on tool ids (tool_use/tool_result pairs map *) (* to tool_calls / role:"tool" messages and back). *) (* *) (* Provider selection happens once at net init: a static key selects *) (* ANTHROPIC; otherwise an OAuth token selects TPX; otherwise no provider *) (* and every exchange fails with a 401-like error. Selection is fixed for *) (* the boot. *) (* *) (* Checked properties (all safety, finite turns): *) (* ShapeInv - bodies handed to the caller are always Messages-shaped *) (* PairingInv - tool ids survive translation with no drops/dups, and *) (* every emitted tool_use is answered by exactly one *) (* tool_result in the next request (or the turn aborts *) (* with an error) *) (* SelectionInv - provider is the deterministic function of credentials *) (* SelectionStable - credentials and provider never change after boot *) (* Termination - via CHECK_DEADLOCK: every mid-exchange state *) (* progresses to a delivered response or an error *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS ToolIds, \* small set of model-value tool ids MaxTurns, \* bound on exchanges per boot ANTHROPIC, TPX, NONE Providers == {ANTHROPIC, TPX, NONE} Shapes == {"messages", "openai"} Phases == {"idle", "req", "resp"} Outcomes == {"none", "ok", "err"} VARIABLES hasKey, \* static API key present at boot hasToken, \* OAuth bearer token present at boot provider, \* provider chosen at net init, fixed for the boot turn, \* completed exchanges phase, \* where the current exchange is pending, \* tool_use ids the model emitted, awaiting tool_result reqIds, \* tool_result ids in the caller's outbound Messages request wireShape, \* protocol shape of the body currently on the wire wireIds, \* tool ids carried by the body on the wire emitted, \* ids the provider actually emitted (pre-translation truth) gotShape, \* shape of the last body handed back to the caller lastOutcome \* result of the last completed exchange vars == <<hasKey, hasToken, provider, turn, phase, pending, reqIds, wireShape, wireIds, emitted, gotShape, lastOutcome>> \* Deterministic selection at net init: key wins, then token, then nothing. Select(k, t) == IF k THEN ANTHROPIC ELSE IF t THEN TPX ELSE NONE \* The protocol each provider speaks on the wire. NativeShape(p) == IF p = TPX THEN "openai" ELSE "messages" Init == /\ hasKey \in BOOLEAN /\ hasToken \in BOOLEAN /\ provider = Select(hasKey, hasToken) /\ turn = 0 /\ phase = "idle" /\ pending = {} /\ reqIds = {} /\ wireShape = "messages" /\ wireIds = {} /\ emitted = {} /\ gotShape = "messages" /\ lastOutcome = "none" CredsUnchanged == UNCHANGED <<hasKey, hasToken, provider>> \* Caller answers every pending tool_use with exactly one tool_result and \* sends a Messages-protocol body. The transport frames it natively \* (ANTHROPIC) or translates it to the foreign shape (TPX); either way the \* translation carries exactly the caller's tool ids. CallerSend == /\ phase = "idle" /\ turn < MaxTurns /\ provider # NONE /\ reqIds' = pending /\ wireShape' = NativeShape(provider) /\ wireIds' = pending /\ phase' = "req" /\ UNCHANGED <<turn, pending, emitted, gotShape, lastOutcome>> /\ CredsUnchanged \* Caller cannot produce tool results: the turn aborts with an error and \* the pending obligations are discarded with it. CallerAbort == /\ phase = "idle" /\ turn < MaxTurns /\ provider # NONE /\ pending # {} /\ lastOutcome' = "err" /\ pending' = {} /\ turn' = turn + 1 /\ UNCHANGED <<phase, reqIds, wireShape, wireIds, emitted, gotShape>> /\ CredsUnchanged \* No credentials were present at boot: the exchange fails immediately \* with a 401-like MODEL_* error. NoProvider == /\ phase = "idle" /\ turn < MaxTurns /\ provider = NONE /\ lastOutcome' = "err" /\ turn' = turn + 1 /\ UNCHANGED <<phase, pending, reqIds, wireShape, wireIds, emitted, gotShape>> /\ CredsUnchanged \* The provider replies in its native shape, emitting any subset of tool \* ids as tool_use blocks (ANTHROPIC) or tool_calls (TPX). ProviderReply == /\ phase = "req" /\ \E ids \in SUBSET ToolIds : /\ emitted' = ids /\ wireIds' = ids /\ wireShape' = NativeShape(provider) /\ phase' = "resp" /\ UNCHANGED <<turn, pending, reqIds, gotShape, lastOutcome>> /\ CredsUnchanged \* Network, TLS, HTTP or protocol failure: the exchange ends in an error. ProviderFail == /\ phase = "req" /\ lastOutcome' = "err" /\ pending' = {} /\ phase' = "idle" /\ turn' = turn + 1 /\ UNCHANGED <<reqIds, wireShape, wireIds, emitted, gotShape>> /\ CredsUnchanged \* The transport hands the caller a Messages-shaped body. A foreign-shaped \* response is translated back first; the reverse translation is a \* bijection on tool ids, so the caller's new obligations are exactly the \* ids the provider emitted. Deliver == /\ phase = "resp" /\ gotShape' = IF wireShape = "openai" THEN "messages" ELSE wireShape /\ pending' = wireIds /\ lastOutcome' = "ok" /\ phase' = "idle" /\ turn' = turn + 1 /\ UNCHANGED <<reqIds, wireShape, wireIds, emitted>> /\ CredsUnchanged \* Terminal self-loop once the turn budget is spent, so deadlock checking \* certifies that every non-final state makes progress. Halted == /\ phase = "idle" /\ turn = MaxTurns /\ UNCHANGED vars Next == \/ CallerSend \/ CallerAbort \/ NoProvider \/ ProviderReply \/ ProviderFail \/ Deliver \/ Halted Spec == Init /\ [][Next]_vars ---------------------------------------------------------------------------- TypeOK == /\ hasKey \in BOOLEAN /\ hasToken \in BOOLEAN /\ provider \in Providers /\ turn \in 0..MaxTurns /\ phase \in Phases /\ pending \subseteq ToolIds /\ reqIds \subseteq ToolIds /\ wireShape \in Shapes /\ wireIds \subseteq ToolIds /\ emitted \subseteq ToolIds /\ gotShape \in Shapes /\ lastOutcome \in Outcomes \* (1) The caller only ever sees Messages-shaped bodies, regardless of \* which provider is behind the transport. ShapeInv == gotShape = "messages" \* (2) Tool id pairing survives translation in both directions: the wire \* carries exactly the caller's tool_result ids on the way out and \* exactly the provider's emitted ids on the way back, and after \* delivery the caller's obligations equal what the provider emitted. PairingInv == /\ (phase = "req") => (wireIds = reqIds /\ reqIds = pending) /\ (phase = "resp") => (wireIds = emitted) /\ (phase = "idle" /\ lastOutcome = "ok") => (pending = emitted) \* (3) Provider selection is the deterministic function of the boot-time \* credentials; key wins over token, no credentials means no provider. SelectionInv == provider = Select(hasKey, hasToken) \* Bounded turns; nothing escapes the phase machine. BoundedInv == turn <= MaxTurns \* Selection is stable: credentials and the chosen provider never change \* after boot. SelectionStable == [][CredsUnchanged]_vars ====

SPECIFICATION Spec CONSTANTS MaxTurns = 3 ToolIds = {t1, t2} ANTHROPIC = ANTHROPIC TPX = TPX NONE = NONE INVARIANTS TypeOK ShapeInv PairingInv SelectionInv BoundedInv PROPERTY SelectionStable CHECK_DEADLOCK TRUE