ProvenQueue.idr

-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--
-- ProvenQueue.idr — Proven-servers QueueConn bindings for RPA Elysium
--
-- Imports and re-exports proven-queueconn types adapted for RPA Elysium's
-- event consumption layer.  The Hybrid Automation Router (HAR) routes events
-- 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
--   DeliveryGuarantee →  configurable per-workflow
--   QueueOp           →  operations the workflow engine can perform

module ProvenQueue

import Types

%default total

---------------------------------------------------------------------------
-- QueueOp — operations the workflow engine can perform on the event queue.
-- Matches proven-queueconn QueueConn.Types.QueueOp exactly.
---------------------------------------------------------------------------

||| Operations that the RPA workflow engine can perform against the
||| event queue (backed by HAR routing).
public export
data QueueOp : Type where
  ||| Publish an event (e.g., emit a derived event from a workflow step).
  Publish     : QueueOp  -- proven-queueconn tag: 0
  ||| Subscribe to receive routed events from HAR.
  Subscribe   : QueueOp  -- proven-queueconn tag: 1
  ||| Acknowledge successful processing of an automation event.
  Acknowledge : QueueOp  -- proven-queueconn tag: 2
  ||| Reject an event, optionally requesting redelivery.
  Reject      : QueueOp  -- proven-queueconn tag: 3
  ||| Inspect the next event without removing it from the queue.
  Peek        : QueueOp  -- proven-queueconn tag: 4
  ||| Remove all pending events from the queue.
  Purge       : QueueOp  -- proven-queueconn tag: 5

||| C ABI tag values — MUST match proven-queueconn encoding.
public export
queueOpTag : QueueOp -> Bits8
queueOpTag Publish     = 0
queueOpTag Subscribe   = 1
queueOpTag Acknowledge = 2
queueOpTag Reject      = 3
queueOpTag Peek        = 4
queueOpTag Purge       = 5

public export
Show QueueOp where
  show Publish     = "Publish"
  show Subscribe   = "Subscribe"
  show Acknowledge = "Acknowledge"
  show Reject      = "Reject"
  show Peek        = "Peek"
  show Purge       = "Purge"

---------------------------------------------------------------------------
-- DeliveryGuarantee — message delivery semantics, configurable per
-- workflow.
-- Matches proven-queueconn QueueConn.Types.DeliveryGuarantee exactly.
---------------------------------------------------------------------------

||| The delivery guarantee level for event processing.
||| Configurable per-workflow: idempotent workflows can use AtLeastOnce
||| while stateful workflows should use ExactlyOnce.
public export
data DeliveryGuarantee : Type where
  ||| Fire-and-forget.  Events may be lost but never duplicated.
  AtMostOnce  : DeliveryGuarantee  -- proven-queueconn tag: 0
  ||| Events are guaranteed delivered but may arrive more than once.
  AtLeastOnce : DeliveryGuarantee  -- proven-queueconn tag: 1
  ||| Events are delivered exactly once (requires idempotency or
  ||| transactional coordination).
  ExactlyOnce : DeliveryGuarantee  -- proven-queueconn tag: 2

||| C ABI tag values — MUST match proven-queueconn encoding.
public export
deliveryGuaranteeTag : DeliveryGuarantee -> Bits8
deliveryGuaranteeTag AtMostOnce  = 0
deliveryGuaranteeTag AtLeastOnce = 1
deliveryGuaranteeTag ExactlyOnce = 2

public export
Show DeliveryGuarantee where
  show AtMostOnce  = "AtMostOnce"
  show AtLeastOnce = "AtLeastOnce"
  show ExactlyOnce = "ExactlyOnce"

---------------------------------------------------------------------------
-- QueueState — the subscription lifecycle for receiving routed events
-- from HAR.
-- Matches proven-queueconn QueueConn.Types.QueueState exactly.
---------------------------------------------------------------------------

||| The lifecycle state of the event queue subscription.
public export
data QueueState : Type where
  ||| No subscription established to the event router.
  Disconnected : QueueState  -- proven-queueconn tag: 0
  ||| Subscription established and operational.
  Connected    : QueueState  -- proven-queueconn tag: 1
  ||| Actively consuming routed events from HAR.
  Consuming    : QueueState  -- proven-queueconn tag: 2
  ||| Actively producing events (e.g., derived events from workflow steps).
  Producing    : QueueState  -- proven-queueconn tag: 3
  ||| Subscription has entered a failed state.
  Failed       : QueueState  -- proven-queueconn tag: 4

||| C ABI tag values — MUST match proven-queueconn encoding.
public export
queueStateTag : QueueState -> Bits8
queueStateTag Disconnected = 0
queueStateTag Connected    = 1
queueStateTag Consuming    = 2
queueStateTag Producing    = 3
queueStateTag Failed       = 4

public export
Show QueueState where
  show Disconnected = "Disconnected"
  show Connected    = "Connected"
  show Consuming    = "Consuming"
  show Producing    = "Producing"
  show Failed       = "Failed"

---------------------------------------------------------------------------
-- MessageState — the lifecycle of an individual automation event as it
-- moves through the workflow engine's processing pipeline.
-- Matches proven-queueconn QueueConn.Types.MessageState exactly.
---------------------------------------------------------------------------

||| The lifecycle state of an individual automation event in the queue.
public export
data MessageState : Type where
  ||| The event is enqueued and awaiting delivery to a workflow.
  Pending      : MessageState  -- proven-queueconn tag: 0
  ||| The event has been delivered to a workflow but not yet acknowledged.
  Delivered    : MessageState  -- proven-queueconn tag: 1
  ||| The workflow acknowledged successful processing.
  Acknowledged : MessageState  -- proven-queueconn tag: 2
  ||| The workflow rejected the event.
  Rejected     : MessageState  -- proven-queueconn tag: 3
  ||| The event exceeded its retry limit and was moved to dead-letter.
  DeadLettered : MessageState  -- proven-queueconn tag: 4
  ||| The event's TTL has elapsed and it was discarded.
  Expired      : MessageState  -- proven-queueconn tag: 5

||| C ABI tag values — MUST match proven-queueconn encoding.
public export
messageStateTag : MessageState -> Bits8
messageStateTag Pending      = 0
messageStateTag Delivered    = 1
messageStateTag Acknowledged = 2
messageStateTag Rejected     = 3
messageStateTag DeadLettered = 4
messageStateTag Expired      = 5

public export
Show MessageState where
  show Pending      = "Pending"
  show Delivered    = "Delivered"
  show Acknowledged = "Acknowledged"
  show Rejected     = "Rejected"
  show DeadLettered = "DeadLettered"
  show Expired      = "Expired"

---------------------------------------------------------------------------
-- QueueError — error categories for event queue operations.
-- 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: 1
  ||| The specified queue does not exist.
  QueueNotFound      : QueueError  -- proven-queueconn tag: 2
  ||| The event payload exceeds the maximum allowed size.
  MessageTooLarge    : QueueError  -- proven-queueconn tag: 3
  ||| The queue or account quota has been exceeded.
  QuotaExceeded      : QueueError  -- proven-queueconn tag: 4
  ||| The acknowledgement was not received within the timeout window.
  AckTimeout         : QueueError  -- proven-queueconn tag: 5
  ||| The caller lacks permission for this queue operation.
  Unauthorized       : QueueError  -- proven-queueconn tag: 6
  ||| The event payload could not be serialised or deserialised.
  SerializationError : QueueError  -- proven-queueconn tag: 7

||| C ABI tag values — MUST match the canonical proven-queueconn encoding.
public export
queueErrorTag : QueueError -> Bits8
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"
  show QuotaExceeded      = "QuotaExceeded"
  show AckTimeout         = "AckTimeout"
  show Unauthorized       = "Unauthorized"
  show SerializationError = "SerializationError"

---------------------------------------------------------------------------
-- Valid queue state transitions — proof-carrying types that ensure
-- only legal subscription lifecycle transitions can be constructed.
---------------------------------------------------------------------------

||| Proof that a queue state transition from `from` to `to` is valid.
public export
data ValidQueueTransition : (from : QueueState) -> (to : QueueState) -> Type where
  ||| Disconnected → Connected: establish subscription to HAR.
  Connect         : ValidQueueTransition Disconnected Connected
  ||| Connected → Consuming: begin consuming routed events.
  StartConsuming  : ValidQueueTransition Connected Consuming
  ||| Connected → Producing: begin producing derived events.
  StartProducing  : ValidQueueTransition Connected Producing
  ||| Consuming → Connected: stop consuming but keep connection.
  StopConsuming   : ValidQueueTransition Consuming Connected
  ||| Producing → Connected: stop producing but keep connection.
  StopProducing   : ValidQueueTransition Producing Connected
  ||| Connected → Disconnected: cleanly disconnect.
  Disconnect      : ValidQueueTransition Connected Disconnected
  ||| Any → Failed: connection failure (from Connected).
  FailConnected   : ValidQueueTransition Connected Failed
  ||| Any → Failed: connection failure (from Consuming).
  FailConsuming   : ValidQueueTransition Consuming Failed
  ||| Any → Failed: connection failure (from Producing).
  FailProducing   : ValidQueueTransition Producing Failed
  ||| Failed → Disconnected: reset after failure.
  ResetFailed     : ValidQueueTransition Failed Disconnected

public export
Show (ValidQueueTransition from to) where
  show Connect        = "Connect (Disconnected → Connected)"
  show StartConsuming = "StartConsuming (Connected → Consuming)"
  show StartProducing = "StartProducing (Connected → Producing)"
  show StopConsuming  = "StopConsuming (Consuming → Connected)"
  show StopProducing  = "StopProducing (Producing → Connected)"
  show Disconnect     = "Disconnect (Connected → Disconnected)"
  show FailConnected  = "FailConnected (Connected → Failed)"
  show FailConsuming  = "FailConsuming (Consuming → Failed)"
  show FailProducing  = "FailProducing (Producing → Failed)"
  show ResetFailed    = "ResetFailed (Failed → Disconnected)"