Repository navigation
feat(session-protocol): atem-session v1 contract, Rust core and shared fixtures - #68
Merged
Merged
Conversation
…r joint review Atem-side draft of the shared contract for the approved session-multiplexing design: identities and generations, hello, session registry, 15 s control leases, submissions with durable receipts, error codes, fixture format. Trust, freshness, encryption and QR grants are placeholders for the joint spec. 🤖 Built with SMT <smt@agora.build>
Authenticated attachments and fenced resume; one binding object for session, terminal and chat requests; lease as the only control path on upgraded connections; normative monotonic lease rules, input-epoch fencing and repeat acquire; receipts bound to the full target and kind with host-computed RFC 8785 digests; kind-specific completion, crash boundaries, approval reserved; registry revisions and tombstones; representation bounds; structured fixtures with a fake clock and digest vectors. Section 9 stays a joint gate. 🤖 Built with SMT <smt@agora.build>
One lease authority per session across legacy and upgraded connections (terminal-v1 control maps onto it; unscoped legacy mutations refused while a remote holder exists); lease replies correlated by re, deadlines from the request's send time and checked before applying; runtime epochs and per-attachment sequences for the registry with resync and no resurrection; exact terminal-v1/chat-v1 envelopes with data.binding; receipt state transitions and the accepted/executing crash distinction; fixture schema with host context, deterministic clock and reordering; more RFC 8785 vectors (UTF-16 key order, escapes, safe-integer bounds, rejects); three new fixtures. 🤖 Built with SMT <smt@agora.build>
Managed sessions reject unscoped legacy mutations whether or not a remote holder exists (after reclaim, release and expiry too); legacy terminal-v1 control keeps every check before mapping onto acquire. Repeat acquire uses min(previous deadline, send time + ms_left, authorization deadline). Fixtures: executable legacy scenario with an explicit subscription and captured values, repeat-acquire deadline 31500 then input off; schema gains capture/substitution and local/remote write counters. runtime_epoch and seq are bounded counters; one runtime_gen per accepted epoch; snapshot before applying a new epoch. 🤖 Built with SMT <smt@agora.build>
Receipts: durable exits from executing for ordinary dispatch failures — rejected only with proof of no side effect, outcome_unknown after a possible partial effect or agent exit; per-kind rules for prompt, interrupt and stop; never retried, duplicates and post-restart queries return the final receipt; two new fixtures. Descriptors: every field required in snapshots and changes (no patches); the registry fixture uses complete descriptors. Leases: expiry is now >= deadline on host and client; the repeat-acquire fixture expects control and input off at 31500. 🤖 Built with SMT <smt@agora.build>
🤖 Built with SMT <smt@agora.build>
🤖 Built with SMT <smt@agora.build>
🤖 Built with SMT <smt@agora.build>
… shared fixtures LeaseClient applies the §5 reply-correlation rules: one reply per outstanding acquire/renew, unknown or duplicate `re` dropped, the acknowledged deadline checked (now >= deadline) before applying, deadline = send time + ms_left capped by authorization, repeat acquire never extends. RegistryClient applies §4: runtime_epoch fencing with a fixed runtime_gen per epoch, per-attachment seq, gap -> list with resync discard, removal without resurrection. fixtures.rs runs every designs/protocol/fixtures/*.json scenario through the strict decoder: client scenarios against these machines, host scenarios via a HostUnderTest trait (plan Task 3); until then they are skipped by name and the count is pinned. Also drops a duplicate size check in wire::decode and documents -0 and unknown-field number handling. 🤖 Built with SMT <smt@agora.build>
At the user's direction there is no backward compatibility (Atem and Astation update together): agentInput, agentPrompt, voice prompts, userCommand, terminal-v1 control/lease_id, unbound chat submit and provider-name terminal ids are removed and refused with no effect; every remote mutation is a session-v1 message with a binding and the current lease. The legacy-connection fixture is replaced by removed-ops-have-no-effect. Needs Astation's review. 🤖 Built with SMT <smt@agora.build>
… feat/session-protocol
wire: removed families (agentInput, agentPrompt, voiceCommand, voiceToggle, userCommand), terminal-v1 control/controller, lease_id and unbound terminal-v1/chat-v1 requests fail with DecodeError::removed set, so the host answers unsupported_version with no effect. terminal-v1 requests decode into TerminalRequest (session-id terminal ids, mandatory binding, no lease_id); chat-v1 open/close/submit need their binding, a session-id agentId and a UUID requestId. The placeholder lease_id shape check is gone. fixtures: no `upgraded` client field; `expect` takes the next message of its `type`/`op`, leaving others queued; `expect_none` checks every type (schema.md updated). 🤖 Built with SMT <smt@agora.build>
- wire: terminal-v1 list/sessions are removed (session-v1 list is the only registry, noted in the contract's r6 §0 list); decode returns the typed TerminalRequest on FamilyMessage::request. - LeaseClient: tracks the highest lease_epoch seen (grants and lease_changed, also while a viewer) and drops older grants; a renew reply for another epoch ends control; release needs control; deadline_ms(now) is None once now >= deadline. - Harness: requests must use the client's setup attachment_gen; holds_lease_epoch is refused in client scenarios; the undocumented `after` assert key is gone; sent_list counts only lists the registry machine requested. - late-renew fixture: a duplicate earlier reply while a later renew is pending is dropped, then that renew's reply applies. 🤖 Built with SMT <smt@agora.build>
… receipts — with shared fixtures 🤖 Built with SMT <smt@agora.build>
…thout ticks, family errors 🤖 Built with SMT <smt@agora.build>
…closed sessions stay closed, stricter shared fixtures 🤖 Built with SMT <smt@agora.build>
This was referenced Oct 16, 2026
This was referenced Oct 17, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The atem-session v1 contract (r6.2, accepted by Astation for compatibility mode at r5; r6 removes legacy paths — no backward compatibility) and Atem's transport-free Rust implementation, plus the shared fixtures.
designs/protocol/atem-session-v1.md,designs/protocol/fixtures/(16 scenarios, schema, RFC 8785 digest vectors).src/session_protocol/: strict wire decoding (bounds, duplicate keys, unsafe integers, lone surrogates), RFC 8785 canonical digest, lease/registry client state machines, the host authority (registry with per-attachment sequence and runtime epochs, 15 s leases with local input winning and input-epoch fencing, receipts with durable transitions, dispatch-failure rules and crash recovery), a data-driven fixture runner.Testing
All 16 shared fixtures and the digest vectors pass in Rust; 120+ protocol unit tests.
Generated with SMT smt@agora.build