diff --git a/src/abi/LinearDispatch.eph b/src/abi/LinearDispatch.eph index 08d0a16..7fac39c 100644 --- a/src/abi/LinearDispatch.eph +++ b/src/abi/LinearDispatch.eph @@ -26,6 +26,15 @@ module RpaElysium.Abi.LinearDispatch --- exactly one handler — it cannot be duplicated or silently dropped. --- The `linear` qualifier ensures the compiler rejects code paths that --- would lose or duplicate the event. +--- +--- This is the consumer-side view of the shared ABI's `RoutedEnvelope` +--- (abi/SHARED-QUEUE-ABI.adoc, abi_version=1; Rust binding `har-abi`). Field +--- correspondence: `eventId`↔`event_id`, `kind`↔`category`, `source`↔the +--- `source` header, `payload`↔the opaque (base64-on-wire) `payload`. The wire +--- envelope additionally carries `abi_version`, `priority`, `guarantee`, +--- `content_type`, `headers`, and `created_at`; a real decoding consumer (a +--- follow-up Rust crate) will surface those. This linear type is retained as +--- the proof-level exactly-once contract over the decoded event. type RoutedEvent linear = { eventId : String , source : String @@ -138,8 +147,10 @@ fn releaseLease (lease : QueueLease) -> LeaseReceipt = --- start and automatically released at the end, ensuring no leak even --- if the processing function raises an error. --- ---- This is the idiomatic pattern for consuming routed events: ---- withLease "rpa-events" AtLeastOnce now \lease -> +--- This is the idiomatic pattern for consuming routed events. The queue name +--- is the canonical shared-ABI inbound subject `har..inbound` +--- (retiring the old ad-hoc `rpa-events`): +--- withLease "har.rpa-elysium.inbound" AtLeastOnce now \lease -> --- let! event = receiveEvent lease in --- processEvent event fn withLease diff --git a/src/abi/ProvenQueue.idr b/src/abi/ProvenQueue.idr index 0672cdd..83c6027 100644 --- a/src/abi/ProvenQueue.idr +++ b/src/abi/ProvenQueue.idr @@ -8,6 +8,14 @@ -- to RPA Elysium workflows; this module provides the type-safe queue -- interface for receiving and processing those routed events. -- +-- ADOPTION (2026-07-07): this module is now a *binding of the shared queue ABI* +-- (abi_version=1) whose normative source is HAR's `abi/SHARED-QUEUE-ABI.adoc` +-- and Rust binding `har-abi`, NOT an independently authored copy. Tag values +-- MUST match that spec (in particular QueueError is 0=NoError + 1..7, the +-- canonical proven-queueconn C-ABI layout). The wire codec is `RoutedEnvelope` +-- / `RoutedReceipt` and the inbound subject is `har.rpa-elysium.inbound`; see +-- `LinearDispatch.eph`. +-- -- Mapping: -- QueueState → subscription lifecycle for receiving routed events -- MessageState → tracking individual automation events through processing @@ -173,40 +181,48 @@ Show MessageState where --------------------------------------------------------------------------- -- QueueError — error categories for event queue operations. --- Matches proven-queueconn QueueConn.Types.QueueError exactly. +-- Matches the canonical proven-queueconn QueueConn.Types.QueueError exactly: +-- tag 0 is the NoError success sentinel (proven-queueconn's NONE), and the +-- seven real errors are 1..7. (Corrected 2026-07-07 to adopt the shared-queue +-- ABI, abi_version=1: the previous 0..6 numbering diverged from the canonical +-- C header. See har-abi / abi/SHARED-QUEUE-ABI.adoc.) --------------------------------------------------------------------------- ||| Error categories that the event queue connector can report. public export data QueueError : Type where + ||| No error — the success sentinel the C ABI returns (proven-queueconn NONE). + NoError : QueueError -- proven-queueconn tag: 0 ||| The connection to the event router was lost. - ConnectionLost : QueueError -- proven-queueconn tag: 0 + ConnectionLost : QueueError -- proven-queueconn tag: 1 ||| The specified queue does not exist. - QueueNotFound : QueueError -- proven-queueconn tag: 1 + QueueNotFound : QueueError -- proven-queueconn tag: 2 ||| The event payload exceeds the maximum allowed size. - MessageTooLarge : QueueError -- proven-queueconn tag: 2 + MessageTooLarge : QueueError -- proven-queueconn tag: 3 ||| The queue or account quota has been exceeded. - QuotaExceeded : QueueError -- proven-queueconn tag: 3 + QuotaExceeded : QueueError -- proven-queueconn tag: 4 ||| The acknowledgement was not received within the timeout window. - AckTimeout : QueueError -- proven-queueconn tag: 4 + AckTimeout : QueueError -- proven-queueconn tag: 5 ||| The caller lacks permission for this queue operation. - Unauthorized : QueueError -- proven-queueconn tag: 5 + Unauthorized : QueueError -- proven-queueconn tag: 6 ||| The event payload could not be serialised or deserialised. - SerializationError : QueueError -- proven-queueconn tag: 6 + SerializationError : QueueError -- proven-queueconn tag: 7 -||| C ABI tag values — MUST match proven-queueconn encoding. +||| C ABI tag values — MUST match the canonical proven-queueconn encoding. public export queueErrorTag : QueueError -> Bits8 -queueErrorTag ConnectionLost = 0 -queueErrorTag QueueNotFound = 1 -queueErrorTag MessageTooLarge = 2 -queueErrorTag QuotaExceeded = 3 -queueErrorTag AckTimeout = 4 -queueErrorTag Unauthorized = 5 -queueErrorTag SerializationError = 6 +queueErrorTag NoError = 0 +queueErrorTag ConnectionLost = 1 +queueErrorTag QueueNotFound = 2 +queueErrorTag MessageTooLarge = 3 +queueErrorTag QuotaExceeded = 4 +queueErrorTag AckTimeout = 5 +queueErrorTag Unauthorized = 6 +queueErrorTag SerializationError = 7 public export Show QueueError where + show NoError = "NoError" show ConnectionLost = "ConnectionLost" show QueueNotFound = "QueueNotFound" show MessageTooLarge = "MessageTooLarge"