import { describe, it, expect, vi, beforeEach, afterEach } from 'vitest'
import fc from 'fast-check'
import { EventEmitter } from 'node:events'

// --- Mocks ---

const mockFindByDevice = vi.fn()
const mockHasExchanges = vi.fn()
const mockGetMetadata = vi.fn()
const mockDeleteByDevice = vi.fn()
const mockFindAfterSequence = vi.fn()

vi.mock('#models/exchange', () => ({
  default: {
    findByDevice: (...args: any[]) => mockFindByDevice(...args),
    hasExchanges: (...args: any[]) => mockHasExchanges(...args),
    getMetadata: (...args: any[]) => mockGetMetadata(...args),
    deleteByDevice: (...args: any[]) => mockDeleteByDevice(...args),
    findAfterSequence: (...args: any[]) => mockFindAfterSequence(...args),
  },
}))

const mockIsTraced = vi.fn()

vi.mock('#services/tr069_trace_service', () => ({
  Tr069TraceService: {
    getInstance: () => ({
      isTraced: mockIsTraced,
    }),
  },
}))

const mockEmitter = new EventEmitter()
const mockSubscribe = vi.fn((deviceId: string, listener: Function) => {
  mockEmitter.on(`exchange:${deviceId}`, listener as any)
})
const mockUnsubscribe = vi.fn((deviceId: string, listener: Function) => {
  mockEmitter.off(`exchange:${deviceId}`, listener as any)
})

vi.mock('#services/exchange_store_service', () => ({
  ExchangeStoreService: {
    getInstance: () => ({
      subscribe: mockSubscribe,
      unsubscribe: mockUnsubscribe,
    }),
  },
}))

vi.mock('#config/exchange_store', () => ({
  default: {
    maxMessagesPerDevice: 5000,
    readTimeoutMs: 5000,
    sse: {
      inactivityTimeoutMs: 300_000,
      absoluteTimeoutMs: 7_200_000,
      maxConnectionsPerDevice: 5,
      retryIntervalMs: 3000,
    },
    featureFlags: {
      persistence: true,
      sseEnabled: true,
      apiSource: 'mongodb',
    },
  },
}))

vi.mock('@adonisjs/core/services/logger', () => ({
  default: {
    info: vi.fn(),
    error: vi.fn(),
    warn: vi.fn(),
    debug: vi.fn(),
  },
}))

import ExchangeController from '../../../app/controllers/exchange_controller.js'

// --- Helpers ---

const PBT_NUM_RUNS = 100

function createStreamContext(options: { deviceId: string; lastEventId?: string }) {
  const written: string[] = []
  const headers: Record<string, string> = {}
  let headWritten = false
  let statusCode = 0
  let ended = false
  const reqEmitter = new EventEmitter()

  const nodeRes = {
    writeHead: vi.fn((code: number, hdrs: Record<string, string>) => {
      statusCode = code
      Object.assign(headers, hdrs)
      headWritten = true
    }),
    write: vi.fn((chunk: string) => {
      written.push(chunk)
    }),
    end: vi.fn(() => {
      ended = true
    }),
  }

  const responseObj = {
    response: nodeRes,
    status: vi.fn(function (this: any, code: number) {
      statusCode = code
      return this
    }),
    json: vi.fn((data: any) => data),
  }

  const ctx = {
    params: { deviceId: options.deviceId },
    request: {
      header: vi.fn((name: string) => {
        if (name === 'Last-Event-ID') return options.lastEventId
        return undefined
      }),
      request: reqEmitter,
      id: () => 'test-correlation-id',
    },
    response: responseObj,
  }

  return {
    ctx: ctx as any,
    nodeRes,
    reqEmitter,
    getWritten: () => written,
    getHeaders: () => headers,
    isHeadWritten: () => headWritten,
    isEnded: () => ended,
    getStatusCode: () => statusCode,
  }
}

/**
 * Parse SSE events from raw written chunks.
 * Returns an array of { id, data } objects for each event.
 */
function parseSSEEvents(chunks: string[]): Array<{ id: number; data: any }> {
  const events: Array<{ id: number; data: any }> = []

  for (const chunk of chunks) {
    // Skip retry messages
    if (chunk.startsWith('retry:')) continue

    const lines = chunk.trim().split('\n')
    let id: number | null = null
    let data: string | null = null

    for (const line of lines) {
      if (line.startsWith('id: ')) {
        id = Number(line.slice(4))
      } else if (line.startsWith('data: ')) {
        data = line.slice(6)
      }
    }

    if (id !== null && data !== null) {
      events.push({ id, data: JSON.parse(data) })
    }
  }

  return events
}

// --- Arbitraries ---

/**
 * Generate a valid sequence number (positive integer).
 */
const arbSequenceNumber = fc.integer({ min: 0, max: 100_000 })

/**
 * Generate a set of exchanges with strictly increasing sequence numbers starting after a given N.
 */
function arbExchangesAfterN(n: number, count: number) {
  return Array.from({ length: count }, (_, i) => ({
    deviceId: 'device-test',
    direction: i % 2 === 0 ? 'CPE→ACS' : ('ACS→CPE' as const),
    timestamp: new Date(Date.now() + (i + 1) * 1000).toISOString(),
    sessionId: `10.0.0.1:54321->192.168.1.1:8080`,
    cwmpMethod: 'Inform',
    rawXml: '<soap/>',
    sequenceNumber: n + i + 1,
  }))
}

/**
 * Generate a random count of exchanges to return after reconnection (1 to 20).
 */
const arbExchangeCount = fc.integer({ min: 1, max: 20 })

/**
 * Generate a random device ID.
 */
const arbDeviceId = fc
  .array(fc.constantFrom(...'abcdefghijklmnopqrstuvwxyz0123456789-'.split('')), {
    minLength: 5,
    maxLength: 20,
  })
  .map((chars) => chars.join(''))

/**
 * Arbitrary that generates a CwmpExchange with a given or random sequenceNumber.
 */
const arbDirection = fc.constantFrom('CPE→ACS' as const, 'ACS→CPE' as const)

const arbCwmpMethod = fc.constantFrom(
  'Inform',
  'GetParameterValues',
  'GetParameterValuesResponse',
  'SetParameterValues',
  'SetParameterValuesResponse',
  'AddObject',
  'DeleteObject',
  'Download',
  'Upload',
  'Reboot',
  'FactoryReset',
  'Fault',
  'InformResponse',
  'Empty',
  'Unknown'
)

function arbExchangeWithSeq(seqArb: fc.Arbitrary<number>) {
  return fc
    .record({
      deviceId: arbDeviceId,
      direction: arbDirection,
      timestamp: fc
        .integer({ min: 1577836800000, max: 1924905600000 }) // 2020-01-01 to 2030-12-31
        .map((ms) => new Date(ms).toISOString()),
      sessionId: fc
        .tuple(
          fc.ipV4(),
          fc.integer({ min: 1024, max: 65535 }),
          fc.ipV4(),
          fc.integer({ min: 1, max: 65535 })
        )
        .map(([ip1, port1, ip2, port2]) => `${ip1}:${port1}->${ip2}:${port2}`),
      cwmpMethod: arbCwmpMethod,
      rawXml: fc
        .string({ minLength: 0, maxLength: 100 })
        .map((s) => `<soap-env:Envelope>${s.replace(/[<>&]/g, 'x')}</soap-env:Envelope>`),
      sequenceNumber: seqArb,
    })
}

// ─── Property Tests ──────────────────────────────────────────────────────────

/**
 * Property 13: SSE Event ID Consistency
 * Validates: Requirements 6.9
 *
 * For any CWMP exchange emitted via SSE, the event `id` field SHALL equal
 * the exchange's `sequenceNumber`, ensuring unique and ordered event identification
 * for reconnection support.
 */
describe('Property 13: SSE Event ID Consistency', () => {
  let controller: ExchangeController

  beforeEach(() => {
    vi.clearAllMocks()
    vi.useFakeTimers()
    controller = new ExchangeController()
    mockFindAfterSequence.mockResolvedValue([])
    mockIsTraced.mockReturnValue(true)
  })

  afterEach(() => {
    vi.useRealTimers()
    mockEmitter.removeAllListeners()
  })

  it('SSE event id field equals the exchange sequenceNumber for any emitted exchange', () => {
    return fc.assert(
      fc.asyncProperty(
        arbExchangeWithSeq(fc.integer({ min: 1, max: 2_147_483_647 })),
        async (exchange) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)
          mockFindAfterSequence.mockResolvedValue([])

          const { ctx, getWritten, reqEmitter } = createStreamContext({
            deviceId: exchange.deviceId,
          })

          await controller.stream(ctx)

          // Emit the exchange via the EventEmitter
          mockEmitter.emit(`exchange:${exchange.deviceId}`, exchange)

          const events = parseSSEEvents(getWritten())

          // Exactly one event emitted
          expect(events).toHaveLength(1)

          // The event id must equal the exchange's sequenceNumber
          expect(events[0].id).toBe(exchange.sequenceNumber)

          // Clean up
          reqEmitter.emit('close')
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('SSE event id equals sequenceNumber for the first message (sequenceNumber=1)', () => {
    return fc.assert(
      fc.asyncProperty(
        arbExchangeWithSeq(fc.constant(1)),
        async (exchange) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)
          mockFindAfterSequence.mockResolvedValue([])

          const { ctx, getWritten, reqEmitter } = createStreamContext({
            deviceId: exchange.deviceId,
          })

          await controller.stream(ctx)

          mockEmitter.emit(`exchange:${exchange.deviceId}`, exchange)

          const events = parseSSEEvents(getWritten())
          expect(events).toHaveLength(1)
          expect(events[0].id).toBe(1)

          reqEmitter.emit('close')
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('SSE event id equals sequenceNumber for large sequence numbers', () => {
    return fc.assert(
      fc.asyncProperty(
        arbExchangeWithSeq(fc.integer({ min: 100_000, max: 2_147_483_647 })),
        async (exchange) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)
          mockFindAfterSequence.mockResolvedValue([])

          const { ctx, getWritten, reqEmitter } = createStreamContext({
            deviceId: exchange.deviceId,
          })

          await controller.stream(ctx)

          mockEmitter.emit(`exchange:${exchange.deviceId}`, exchange)

          const events = parseSSEEvents(getWritten())
          expect(events).toHaveLength(1)
          expect(events[0].id).toBe(exchange.sequenceNumber)

          reqEmitter.emit('close')
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('multiple consecutive SSE events each have id matching their respective sequenceNumber', () => {
    const arbSeqList = fc
      .uniqueArray(fc.integer({ min: 1, max: 100_000 }), { minLength: 2, maxLength: 10 })
      .map((seqs) => seqs.sort((a, b) => a - b))

    return fc.assert(
      fc.asyncProperty(arbSeqList, arbDeviceId, async (seqs, deviceId) => {
        vi.clearAllMocks()
        mockIsTraced.mockReturnValue(true)
        mockFindAfterSequence.mockResolvedValue([])

        const { ctx, getWritten, reqEmitter } = createStreamContext({ deviceId })

        await controller.stream(ctx)

        // Emit multiple exchanges with distinct sequence numbers
        for (const seq of seqs) {
          const exchange = {
            deviceId,
            direction: 'CPE→ACS' as const,
            timestamp: new Date(Date.now() + seq * 1000).toISOString(),
            sessionId: '10.0.0.1:54321->192.168.1.1:8080',
            cwmpMethod: 'Inform',
            rawXml: '<soap-env:Envelope><cwmp:Inform/></soap-env:Envelope>',
            sequenceNumber: seq,
          }
          mockEmitter.emit(`exchange:${deviceId}`, exchange)
        }

        const events = parseSSEEvents(getWritten())

        expect(events).toHaveLength(seqs.length)

        // Each event's id must match the corresponding sequenceNumber
        for (let i = 0; i < seqs.length; i++) {
          expect(events[i].id).toBe(seqs[i])
        }

        reqEmitter.emit('close')
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('SSE events from Last-Event-ID reconnection also have id matching sequenceNumber', () => {
    const arbReconnectionData = fc
      .tuple(
        arbDeviceId,
        fc.uniqueArray(fc.integer({ min: 6, max: 1000 }), { minLength: 1, maxLength: 5 })
      )
      .map(([deviceId, seqs]) => ({
        deviceId,
        exchanges: seqs.sort((a, b) => a - b).map((seq) => ({
          deviceId,
          direction: 'CPE→ACS' as const,
          timestamp: new Date(Date.now() + seq * 1000).toISOString(),
          sessionId: '10.0.0.1:54321->192.168.1.1:8080',
          cwmpMethod: 'Inform',
          rawXml: '<soap-env:Envelope><cwmp:Inform/></soap-env:Envelope>',
          sequenceNumber: seq,
        })),
      }))

    return fc.assert(
      fc.asyncProperty(arbReconnectionData, async ({ deviceId, exchanges }) => {
        vi.clearAllMocks()
        mockIsTraced.mockReturnValue(true)
        mockFindAfterSequence.mockResolvedValue(exchanges)

        const { ctx, getWritten, reqEmitter } = createStreamContext({
          deviceId,
          lastEventId: '5',
        })

        await controller.stream(ctx)

        const events = parseSSEEvents(getWritten())

        // Each event id must match its exchange's sequenceNumber
        for (let i = 0; i < exchanges.length; i++) {
          expect(events[i].id).toBe(exchanges[i].sequenceNumber)
        }

        reqEmitter.emit('close')
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('SSE event format is always "id: <sequenceNumber>\\ndata: <JSON>\\n\\n"', () => {
    return fc.assert(
      fc.asyncProperty(
        arbExchangeWithSeq(fc.integer({ min: 1, max: 2_147_483_647 })),
        async (exchange) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)
          mockFindAfterSequence.mockResolvedValue([])

          const { ctx, getWritten, reqEmitter } = createStreamContext({
            deviceId: exchange.deviceId,
          })

          await controller.stream(ctx)

          mockEmitter.emit(`exchange:${exchange.deviceId}`, exchange)

          const written = getWritten()
          // Skip retry message, get the SSE event
          const sseEvent = written[written.length - 1]

          // Verify format: "id: <number>\ndata: <json>\n\n"
          const parts = sseEvent.split('\n')
          expect(parts.length).toBe(4) // "id: ...", "data: ...", "", ""
          expect(parts[0]).toMatch(/^id: \d+$/)
          expect(parts[1]).toMatch(/^data: .+$/)
          expect(parts[2]).toBe('')
          expect(parts[3]).toBe('')

          // Parse id back and verify it matches sequenceNumber
          const parsedId = Number.parseInt(parts[0].replace('id: ', ''), 10)
          expect(parsedId).toBe(exchange.sequenceNumber)

          // Parse data and verify it contains the correct sequenceNumber
          const parsedData = JSON.parse(parts[1].replace('data: ', ''))
          expect(parsedData.sequenceNumber).toBe(exchange.sequenceNumber)

          reqEmitter.emit('close')
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })
})

/**
 * Property 14: SSE Reconnection Continuity (Last-Event-ID)
 * Validates: Requirements 6.8
 *
 * For any SSE reconnection providing Last-Event-ID=N, the server SHALL resume
 * streaming only exchanges with sequence number > N, producing zero duplicate messages.
 */
describe('Property 14: SSE Reconnection Continuity (Last-Event-ID)', () => {
  let controller: ExchangeController

  beforeEach(() => {
    vi.clearAllMocks()
    vi.useFakeTimers()
    controller = new ExchangeController()
  })

  afterEach(() => {
    vi.useRealTimers()
    mockEmitter.removeAllListeners()
  })

  it('reconnection with Last-Event-ID=N resumes only exchanges with seq > N (zero duplicates)', () => {
    return fc.assert(
      fc.asyncProperty(
        arbSequenceNumber,
        arbExchangeCount,
        arbDeviceId,
        async (lastSeq, count, deviceId) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)

          // Generate exchanges that should be returned after reconnection
          // All must have sequenceNumber > lastSeq
          const missedExchanges = arbExchangesAfterN(lastSeq, count).map((e) => ({
            ...e,
            deviceId,
          }))

          mockFindAfterSequence.mockResolvedValue(missedExchanges)

          const { ctx, getWritten, reqEmitter } = createStreamContext({
            deviceId,
            lastEventId: String(lastSeq),
          })

          await controller.stream(ctx)

          // Verify findAfterSequence was called with the correct arguments
          expect(mockFindAfterSequence).toHaveBeenCalledWith(deviceId, lastSeq)

          // Parse SSE events from written output
          const events = parseSSEEvents(getWritten())

          // Property: all event IDs must be > lastSeq (no duplicates)
          for (const event of events) {
            expect(event.id).toBeGreaterThan(lastSeq)
          }

          // Property: number of events equals the number of missed exchanges
          expect(events).toHaveLength(missedExchanges.length)

          // Property: no duplicate IDs in the events
          const ids = events.map((e) => e.id)
          const uniqueIds = new Set(ids)
          expect(uniqueIds.size).toBe(ids.length)

          // Property: events are in sequence order (ascending)
          for (let i = 1; i < events.length; i++) {
            expect(events[i].id).toBeGreaterThan(events[i - 1].id)
          }

          // Clean up SSE connection
          reqEmitter.emit('close')
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('Last-Event-ID=0 returns all exchanges from the beginning (seq > 0)', () => {
    return fc.assert(
      fc.asyncProperty(arbExchangeCount, arbDeviceId, async (count, deviceId) => {
        vi.clearAllMocks()
        mockIsTraced.mockReturnValue(true)

        const allExchanges = arbExchangesAfterN(0, count).map((e) => ({
          ...e,
          deviceId,
        }))

        mockFindAfterSequence.mockResolvedValue(allExchanges)

        const { ctx, getWritten, reqEmitter } = createStreamContext({
          deviceId,
          lastEventId: '0',
        })

        await controller.stream(ctx)

        // findAfterSequence called with seqNumber=0
        expect(mockFindAfterSequence).toHaveBeenCalledWith(deviceId, 0)

        const events = parseSSEEvents(getWritten())

        // All events must have seq > 0
        for (const event of events) {
          expect(event.id).toBeGreaterThan(0)
        }

        // Correct count of events
        expect(events).toHaveLength(allExchanges.length)

        // Clean up
        reqEmitter.emit('close')
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('very large Last-Event-ID returns zero exchanges when none exist beyond it', () => {
    return fc.assert(
      fc.asyncProperty(
        fc.integer({ min: 50_000, max: 1_000_000 }),
        arbDeviceId,
        async (largeSeq, deviceId) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)

          // No exchanges exist beyond the large sequence number
          mockFindAfterSequence.mockResolvedValue([])

          const { ctx, getWritten, reqEmitter } = createStreamContext({
            deviceId,
            lastEventId: String(largeSeq),
          })

          await controller.stream(ctx)

          expect(mockFindAfterSequence).toHaveBeenCalledWith(deviceId, largeSeq)

          // Only the retry message should be written, no SSE events
          const events = parseSSEEvents(getWritten())
          expect(events).toHaveLength(0)

          // Clean up
          reqEmitter.emit('close')
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('reconnection events combined with live events produce no duplicates', () => {
    return fc.assert(
      fc.asyncProperty(
        arbSequenceNumber,
        fc.integer({ min: 1, max: 10 }),
        fc.integer({ min: 1, max: 10 }),
        arbDeviceId,
        async (lastSeq, missedCount, liveCount, deviceId) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)

          // Missed exchanges (seq > lastSeq, up to lastSeq + missedCount)
          const missedExchanges = arbExchangesAfterN(lastSeq, missedCount).map((e) => ({
            ...e,
            deviceId,
          }))

          mockFindAfterSequence.mockResolvedValue(missedExchanges)

          const { ctx, getWritten, reqEmitter } = createStreamContext({
            deviceId,
            lastEventId: String(lastSeq),
          })

          await controller.stream(ctx)

          // Simulate live exchanges arriving after reconnection
          // Their sequence numbers continue from where missed left off
          const highestMissedSeq = lastSeq + missedCount
          for (let i = 1; i <= liveCount; i++) {
            const liveExchange = {
              deviceId,
              direction: 'CPE→ACS',
              timestamp: new Date(Date.now() + (missedCount + i) * 1000).toISOString(),
              sessionId: '10.0.0.1:54321->192.168.1.1:8080',
              cwmpMethod: 'GetParameterValues',
              rawXml: '<soap/>',
              sequenceNumber: highestMissedSeq + i,
            }
            mockEmitter.emit(`exchange:${deviceId}`, liveExchange)
          }

          const events = parseSSEEvents(getWritten())

          // Total events = missed + live
          expect(events).toHaveLength(missedCount + liveCount)

          // All event IDs must be > lastSeq
          for (const event of events) {
            expect(event.id).toBeGreaterThan(lastSeq)
          }

          // No duplicate IDs
          const ids = events.map((e) => e.id)
          const uniqueIds = new Set(ids)
          expect(uniqueIds.size).toBe(ids.length)

          // Events should be in ascending order (missed first, then live)
          for (let i = 1; i < events.length; i++) {
            expect(events[i].id).toBeGreaterThan(events[i - 1].id)
          }

          // Clean up
          reqEmitter.emit('close')
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })
})


// --- Helpers for Property 5 ---

function createHttpContext(overrides: {
  params?: Record<string, string>
  qs?: Record<string, any>
} = {}) {
  const responseData: { status?: number; body?: any } = {}

  const response = {
    status(code: number) {
      responseData.status = code
      return this
    },
    json(data: any) {
      responseData.body = data
      return { status: responseData.status, body: data }
    },
    send(data: any) {
      responseData.body = data
      return { status: responseData.status, body: data }
    },
  }

  const request = {
    qs: () => overrides.qs || {},
    id: () => 'test-correlation-id',
  }

  return {
    params: overrides.params || {},
    request,
    response,
    responseData,
  } as any
}

/**
 * Property 5: API Result Ordering
 * Validates: Requirements 2.1
 *
 * For any set of persisted exchanges and any valid query to the exchanges API,
 * the returned array SHALL be ordered by timestamp ascending with no inversions.
 */
describe('Property 5: API Result Ordering', () => {
  let controller: ExchangeController

  beforeEach(() => {
    vi.clearAllMocks()
    controller = new ExchangeController()
  })

  // ─── Arbitraries ─────────────────────────────────────────────────────────────

  /**
   * Generate a random ISO 8601 timestamp using integer epoch milliseconds for stability.
   * Range: 2024-01-01 to 2025-12-31
   */
  const MIN_TS = new Date('2024-01-01T00:00:00.000Z').getTime()
  const MAX_TS = new Date('2025-12-31T23:59:59.999Z').getTime()

  const arbTimestamp = fc
    .integer({ min: MIN_TS, max: MAX_TS })
    .map((ms) => new Date(ms).toISOString())

  /**
   * Generate a random CWMP direction.
   */
  const arbDirection = fc.constantFrom('CPE→ACS' as const, 'ACS→CPE' as const)

  /**
   * Generate a random CWMP method name.
   */
  const arbCwmpMethod = fc.constantFrom(
    'Inform',
    'InformResponse',
    'GetParameterValues',
    'GetParameterValuesResponse',
    'SetParameterValues',
    'SetParameterValuesResponse',
    'Download',
    'Reboot',
    'Empty',
    'Unknown'
  )

  /**
   * Generate a list of exchanges (1 to 50) already sorted by timestamp ascending.
   * This simulates what ExchangeModel.findByDevice returns (it sorts by timestamp: 1).
   * Uses integer timestamps to avoid Invalid Date issues during shrinking.
   */
  const arbSortedExchanges = fc
    .array(fc.integer({ min: MIN_TS, max: MAX_TS }), { minLength: 1, maxLength: 50 })
    .map((epochMs) => {
      // Sort ascending to simulate the model's sort behavior
      const sorted = [...epochMs].sort((a, b) => a - b)
      return sorted.map((ms, idx) => ({
        deviceId: 'device-test',
        direction: (idx % 2 === 0 ? 'CPE→ACS' : 'ACS→CPE') as 'CPE→ACS' | 'ACS→CPE',
        timestamp: new Date(ms).toISOString(),
        sessionId: '10.0.0.1:54321->192.168.1.1:8080',
        cwmpMethod: 'Inform',
        rawXml: '<soap:Envelope><cwmp:Inform/></soap:Envelope>',
        sequenceNumber: idx + 1,
      }))
    })

  // ─── Property Tests ──────────────────────────────────────────────────────────

  it('returned exchanges are always ordered by timestamp ascending (no inversions)', () => {
    return fc.assert(
      fc.asyncProperty(arbSortedExchanges, async (exchanges) => {
        // Setup: device is traced and has exchanges
        mockIsTraced.mockReturnValue(true)
        mockHasExchanges.mockResolvedValue(true)
        mockFindByDevice.mockResolvedValue(exchanges)
        mockGetMetadata.mockResolvedValue({
          recordedFrom: exchanges[0]?.timestamp ?? null,
          recordedUntil: exchanges[exchanges.length - 1]?.timestamp ?? null,
          count: exchanges.length,
        })

        const ctx = createHttpContext({ params: { deviceId: 'device-test' } })
        const result = await controller.index(ctx)

        expect(result.status).toBe(200)
        const returned = result.body.exchanges

        // Verify: no timestamp inversions (each timestamp >= previous)
        for (let i = 1; i < returned.length; i++) {
          const prev = new Date(returned[i - 1].timestamp).getTime()
          const curr = new Date(returned[i].timestamp).getTime()
          expect(curr).toBeGreaterThanOrEqual(prev)
        }
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('empty exchange set returns 200 with empty array (trivially ordered)', () => {
    return fc.assert(
      fc.asyncProperty(fc.constant(null), async () => {
        mockIsTraced.mockReturnValue(true)
        mockHasExchanges.mockResolvedValue(true)
        mockFindByDevice.mockResolvedValue([])
        mockGetMetadata.mockResolvedValue({
          recordedFrom: null,
          recordedUntil: null,
          count: 0,
        })

        const ctx = createHttpContext({ params: { deviceId: 'device-test' } })
        const result = await controller.index(ctx)

        expect(result.status).toBe(200)
        expect(result.body.exchanges).toEqual([])
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('single exchange is trivially ordered', () => {
    return fc.assert(
      fc.asyncProperty(
        arbTimestamp,
        arbDirection,
        arbCwmpMethod,
        async (timestamp, direction, cwmpMethod) => {
          const exchange = {
            deviceId: 'device-test',
            direction,
            timestamp,
            sessionId: '10.0.0.1:54321->192.168.1.1:8080',
            cwmpMethod,
            rawXml: `<soap:Envelope><cwmp:${cwmpMethod}/></soap:Envelope>`,
            sequenceNumber: 1,
          }

          mockIsTraced.mockReturnValue(true)
          mockHasExchanges.mockResolvedValue(true)
          mockFindByDevice.mockResolvedValue([exchange])
          mockGetMetadata.mockResolvedValue({
            recordedFrom: timestamp,
            recordedUntil: timestamp,
            count: 1,
          })

          const ctx = createHttpContext({ params: { deviceId: 'device-test' } })
          const result = await controller.index(ctx)

          expect(result.status).toBe(200)
          expect(result.body.exchanges).toHaveLength(1)
          expect(result.body.exchanges[0].timestamp).toBe(timestamp)
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('exchanges with duplicate timestamps maintain stable order (no inversions)', () => {
    return fc.assert(
      fc.asyncProperty(
        arbTimestamp,
        fc.integer({ min: 2, max: 20 }),
        async (timestamp, count) => {
          // All exchanges have the same timestamp - still valid ordering
          const exchanges = Array.from({ length: count }, (_, idx) => ({
            deviceId: 'device-test',
            direction: idx % 2 === 0 ? ('CPE→ACS' as const) : ('ACS→CPE' as const),
            timestamp,
            sessionId: '10.0.0.1:54321->192.168.1.1:8080',
            cwmpMethod: 'Inform',
            rawXml: '<soap:Envelope><cwmp:Inform/></soap:Envelope>',
            sequenceNumber: idx + 1,
          }))

          mockIsTraced.mockReturnValue(true)
          mockHasExchanges.mockResolvedValue(true)
          mockFindByDevice.mockResolvedValue(exchanges)
          mockGetMetadata.mockResolvedValue({
            recordedFrom: timestamp,
            recordedUntil: timestamp,
            count,
          })

          const ctx = createHttpContext({ params: { deviceId: 'device-test' } })
          const result = await controller.index(ctx)

          expect(result.status).toBe(200)
          const returned = result.body.exchanges

          // With duplicate timestamps, no inversions means each >= previous
          for (let i = 1; i < returned.length; i++) {
            const prev = new Date(returned[i - 1].timestamp).getTime()
            const curr = new Date(returned[i].timestamp).getTime()
            expect(curr).toBeGreaterThanOrEqual(prev)
          }
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('controller preserves the ordering from the model (does not reorder)', () => {
    return fc.assert(
      fc.asyncProperty(arbSortedExchanges, async (exchanges) => {
        mockIsTraced.mockReturnValue(true)
        mockHasExchanges.mockResolvedValue(true)
        mockFindByDevice.mockResolvedValue(exchanges)
        mockGetMetadata.mockResolvedValue({
          recordedFrom: exchanges[0]?.timestamp ?? null,
          recordedUntil: exchanges[exchanges.length - 1]?.timestamp ?? null,
          count: exchanges.length,
        })

        const ctx = createHttpContext({ params: { deviceId: 'device-test' } })
        const result = await controller.index(ctx)

        expect(result.status).toBe(200)
        const returned = result.body.exchanges

        // The controller must pass through the model results in the same order
        expect(returned).toHaveLength(exchanges.length)
        for (let i = 0; i < returned.length; i++) {
          expect(returned[i].timestamp).toBe(exchanges[i].timestamp)
          expect(returned[i].sequenceNumber).toBe(exchanges[i].sequenceNumber)
        }
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })
})


/**
 * Property 6: Limit Parameter Validation and Capping
 * Validates: Requirements 2.2, 2.3
 *
 * For any numeric limit value in the range [1, 1000], the API SHALL return at most `limit` messages;
 * for any omitted limit, the default SHALL be 200;
 * for any limit value that is non-numeric or < 1, the API SHALL return HTTP 400.
 */
describe('Property 6: Limit Parameter Validation and Capping', () => {
  let controller: ExchangeController

  // ─── Helpers ─────────────────────────────────────────────────────────────────

  function createHttpContext(overrides: { params?: Record<string, string>; qs?: Record<string, any> } = {}) {
    const responseData: { status?: number; body?: any } = {}

    const response = {
      status(code: number) {
        responseData.status = code
        return this
      },
      json(data: any) {
        responseData.body = data
        return { status: responseData.status, body: data }
      },
      send(data: any) {
        responseData.body = data
        return { status: responseData.status, body: data }
      },
    }

    const request = {
      qs: () => overrides.qs || {},
      id: () => 'test-correlation-id',
    }

    return {
      params: overrides.params || {},
      request,
      response,
      responseData,
    } as any
  }

  function generateExchanges(count: number): any[] {
    const exchanges = []
    const baseTime = new Date('2025-01-15T10:00:00.000Z').getTime()
    for (let i = 0; i < count; i++) {
      exchanges.push({
        deviceId: 'device-test',
        direction: i % 2 === 0 ? 'CPE→ACS' : 'ACS→CPE',
        timestamp: new Date(baseTime + i * 1000).toISOString(),
        sessionId: '10.0.0.1:54321->192.168.1.1:8080',
        cwmpMethod: 'Inform',
        rawXml: '<soap/>',
        sequenceNumber: i + 1,
      })
    }
    return exchanges
  }

  // ─── Arbitraries ─────────────────────────────────────────────────────────────

  /**
   * Arbitrary for valid limit values in the range [1, 1000] (integers).
   */
  const arbValidLimit = fc.integer({ min: 1, max: 1000 })

  /**
   * Arbitrary for limit values above 1000 that should be clamped to 1000.
   */
  const arbOverLimit = fc.integer({ min: 1001, max: 100_000 })

  /**
   * Arbitrary for non-numeric limit values (strings that don't parse as valid numbers).
   */
  const arbNonNumericLimit = fc.oneof(
    fc.constantFrom('abc', 'NaN', 'Infinity', '-Infinity', 'null', 'undefined', 'true', 'false'),
    fc
      .string({ minLength: 1, maxLength: 20 })
      .filter((s) => {
        const parsed = Number(s)
        // Exclude strings that parse as valid finite numbers
        return !Number.isFinite(parsed) && s.trim() !== ''
      })
  )

  /**
   * Arbitrary for limit values less than 1 (zero and negatives).
   */
  const arbLessThanOne = fc.integer({ min: -10000, max: 0 })

  /**
   * Arbitrary for float/non-integer numeric values (valid numbers but not integers).
   */
  const arbFloatLimit = fc
    .tuple(fc.integer({ min: 1, max: 999 }), fc.integer({ min: 1, max: 99 }))
    .map(([whole, fraction]) => `${whole}.${fraction}`)

  // ─── Setup ───────────────────────────────────────────────────────────────────

  beforeEach(() => {
    vi.clearAllMocks()
    controller = new ExchangeController()
    // Default: device is traced and has exchanges
    mockIsTraced.mockReturnValue(true)
    mockHasExchanges.mockResolvedValue(true)
    mockGetMetadata.mockResolvedValue({
      recordedFrom: '2025-01-15T10:00:00.000Z',
      recordedUntil: '2025-01-15T10:30:00.000Z',
      count: 500,
    })
  })

  // ─── Property Tests ──────────────────────────────────────────────────────────

  it('valid limit [1,1000] → findByDevice called with that limit and returns at most `limit` messages', () => {
    return fc.assert(
      fc.asyncProperty(arbValidLimit, async (limit) => {
        vi.clearAllMocks()
        mockIsTraced.mockReturnValue(true)
        mockHasExchanges.mockResolvedValue(true)
        mockGetMetadata.mockResolvedValue({
          recordedFrom: '2025-01-15T10:00:00.000Z',
          recordedUntil: '2025-01-15T10:30:00.000Z',
          count: 500,
        })

        // Return exactly min(limit, 500) messages (simulating DB respecting limit)
        const returnedCount = Math.min(limit, 500)
        const exchanges = generateExchanges(returnedCount)
        mockFindByDevice.mockResolvedValue(exchanges)

        const ctx = createHttpContext({
          params: { deviceId: 'device-test' },
          qs: { limit: String(limit) },
        })
        const result = await controller.index(ctx)

        // Should pass limit to the model
        expect(mockFindByDevice).toHaveBeenCalledWith('device-test', {
          limit,
          after: undefined,
          before: undefined,
          latest: false,
        })

        // Should return 200 with at most `limit` messages
        expect(result.status).toBe(200)
        expect(result.body.exchanges.length).toBeLessThanOrEqual(limit)
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('limit above 1000 → clamped to 1000', () => {
    return fc.assert(
      fc.asyncProperty(arbOverLimit, async (limit) => {
        vi.clearAllMocks()
        mockIsTraced.mockReturnValue(true)
        mockHasExchanges.mockResolvedValue(true)
        mockGetMetadata.mockResolvedValue({
          recordedFrom: '2025-01-15T10:00:00.000Z',
          recordedUntil: '2025-01-15T10:30:00.000Z',
          count: 500,
        })
        mockFindByDevice.mockResolvedValue(generateExchanges(500))

        const ctx = createHttpContext({
          params: { deviceId: 'device-test' },
          qs: { limit: String(limit) },
        })
        const result = await controller.index(ctx)

        // Should clamp to 1000
        expect(mockFindByDevice).toHaveBeenCalledWith('device-test', {
          limit: 1000,
          after: undefined,
          before: undefined,
          latest: false,
        })
        expect(result.status).toBe(200)
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('omitted limit → default of 200 is used', () => {
    return fc.assert(
      fc.asyncProperty(fc.constant(undefined), async () => {
        vi.clearAllMocks()
        mockIsTraced.mockReturnValue(true)
        mockHasExchanges.mockResolvedValue(true)
        mockGetMetadata.mockResolvedValue({
          recordedFrom: '2025-01-15T10:00:00.000Z',
          recordedUntil: '2025-01-15T10:30:00.000Z',
          count: 500,
        })
        mockFindByDevice.mockResolvedValue(generateExchanges(200))

        const ctx = createHttpContext({
          params: { deviceId: 'device-test' },
          qs: {},
        })
        const result = await controller.index(ctx)

        // Should use default limit of 200
        expect(mockFindByDevice).toHaveBeenCalledWith('device-test', {
          limit: 200,
          after: undefined,
          before: undefined,
          latest: false,
        })
        expect(result.status).toBe(200)
        expect(result.body.exchanges.length).toBeLessThanOrEqual(200)
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('non-numeric limit → HTTP 400', () => {
    return fc.assert(
      fc.asyncProperty(arbNonNumericLimit, async (limit) => {
        vi.clearAllMocks()

        const ctx = createHttpContext({
          params: { deviceId: 'device-test' },
          qs: { limit },
        })
        const result = await controller.index(ctx)

        expect(result.status).toBe(400)
        expect(result.body.error).toContain('Invalid limit')
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('limit < 1 (zero and negatives) → HTTP 400', () => {
    return fc.assert(
      fc.asyncProperty(arbLessThanOne, async (limit) => {
        vi.clearAllMocks()

        const ctx = createHttpContext({
          params: { deviceId: 'device-test' },
          qs: { limit: String(limit) },
        })
        const result = await controller.index(ctx)

        expect(result.status).toBe(400)
        expect(result.body.error).toContain('Invalid limit')
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('float limit values → HTTP 400 (must be integer)', () => {
    return fc.assert(
      fc.asyncProperty(arbFloatLimit, async (limit) => {
        vi.clearAllMocks()

        const ctx = createHttpContext({
          params: { deviceId: 'device-test' },
          qs: { limit },
        })
        const result = await controller.index(ctx)

        expect(result.status).toBe(400)
        expect(result.body.error).toContain('Invalid limit')
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('for any valid limit, the returned exchange count never exceeds the requested limit', () => {
    return fc.assert(
      fc.asyncProperty(
        arbValidLimit,
        fc.integer({ min: 0, max: 2000 }),
        async (limit, totalAvailable) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)
          mockHasExchanges.mockResolvedValue(true)
          mockGetMetadata.mockResolvedValue({
            recordedFrom: '2025-01-15T10:00:00.000Z',
            recordedUntil: '2025-01-15T10:30:00.000Z',
            count: totalAvailable,
          })

          // Simulate DB returning min(limit, available) messages
          const returnedCount = Math.min(limit, totalAvailable)
          mockFindByDevice.mockResolvedValue(generateExchanges(returnedCount))

          const ctx = createHttpContext({
            params: { deviceId: 'device-test' },
            qs: { limit: String(limit) },
          })
          const result = await controller.index(ctx)

          expect(result.status).toBe(200)
          expect(result.body.exchanges.length).toBeLessThanOrEqual(limit)
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })
})

/**
 * Property 7: After Parameter Filtering
 * Validates: Requirements 2.4, 2.5
 *
 * For any valid ISO 8601 timestamp passed as the `after` query parameter, all returned exchanges
 * SHALL have a timestamp strictly greater than the specified value; for any invalid timestamp
 * string, the API SHALL return HTTP 400.
 */
describe('Property 7: After Parameter Filtering', () => {
  let controller: ExchangeController

  beforeEach(() => {
    vi.clearAllMocks()
    controller = new ExchangeController()
    mockIsTraced.mockReturnValue(true)
    mockHasExchanges.mockResolvedValue(true)
    mockGetMetadata.mockResolvedValue({
      recordedFrom: '2020-01-01T00:00:00.000Z',
      recordedUntil: '2030-12-31T23:59:59.999Z',
      count: 100,
    })
  })

  // ─── Arbitraries ─────────────────────────────────────────────────────────────

  /**
   * Generate valid ISO 8601 timestamps across a wide range of dates (full format with Z suffix).
   * Uses integer milliseconds to avoid Invalid Date issues with fc.date().
   */
  const arbValidIso8601 = fc
    .integer({
      min: 0, // 1970-01-01T00:00:00.000Z
      max: 4102444799999, // ~2099-12-31T23:59:59.999Z
    })
    .map((ms) => new Date(ms).toISOString())

  /**
   * Generate valid ISO 8601 date-only format (YYYY-MM-DD).
   */
  const arbValidIso8601DateOnly = fc
    .record({
      year: fc.integer({ min: 1970, max: 2100 }),
      month: fc.integer({ min: 1, max: 12 }),
      day: fc.integer({ min: 1, max: 28 }),
    })
    .map(({ year, month, day }) => {
      const m = String(month).padStart(2, '0')
      const d = String(day).padStart(2, '0')
      return `${year}-${m}-${d}`
    })

  /**
   * Generate valid ISO 8601 timestamps with timezone offsets.
   */
  const arbValidIso8601WithOffset = fc
    .record({
      year: fc.integer({ min: 1970, max: 2100 }),
      month: fc.integer({ min: 1, max: 12 }),
      day: fc.integer({ min: 1, max: 28 }),
      hour: fc.integer({ min: 0, max: 23 }),
      minute: fc.integer({ min: 0, max: 59 }),
      second: fc.integer({ min: 0, max: 59 }),
      offsetHour: fc.integer({ min: 0, max: 14 }),
      offsetMinute: fc.constantFrom(0, 30, 45),
      offsetSign: fc.constantFrom('+', '-'),
    })
    .map(({ year, month, day, hour, minute, second, offsetHour, offsetMinute, offsetSign }) => {
      const m = String(month).padStart(2, '0')
      const d = String(day).padStart(2, '0')
      const h = String(hour).padStart(2, '0')
      const min = String(minute).padStart(2, '0')
      const sec = String(second).padStart(2, '0')
      const oh = String(offsetHour).padStart(2, '0')
      const om = String(offsetMinute).padStart(2, '0')
      return `${year}-${m}-${d}T${h}:${min}:${sec}${offsetSign}${oh}:${om}`
    })

  /**
   * Generate clearly invalid timestamp strings that should not pass ISO 8601 validation.
   */
  const arbInvalidTimestamp = fc.oneof(
    // Random strings that are not dates
    fc.string({ minLength: 1, maxLength: 50 }).filter((s) => {
      const date = new Date(s)
      if (isNaN(date.getTime())) return true
      const iso8601Pattern =
        /^\d{4}-\d{2}-\d{2}(T\d{2}:\d{2}(:\d{2}(\.\d{1,6})?)?(Z|[+-]\d{2}:?\d{2})?)?$/
      return !iso8601Pattern.test(s)
    }),
    // Well-known invalid patterns
    fc.constantFrom(
      'not-a-date',
      '2025-13-01',
      '2025-01-32',
      'yesterday',
      '01/15/2025',
      '15-Jan-2025',
      '2025/01/15',
      '2025-1-1',
      'abc123',
      '99999-01-01',
      '2025-00-01',
      '2025-01-00',
      'T10:30:00Z',
      '2025-01-15T25:00:00Z',
      '2025-01-15T10:60:00Z',
      '2025-01-15T10:30:60Z'
    )
  )

  /**
   * Generate exchange data with timestamps guaranteed to be strictly after a given reference.
   */
  function makeExchangesAfter(afterTimestamp: string, count: number) {
    const afterMs = new Date(afterTimestamp).getTime()
    const exchanges = []
    for (let i = 1; i <= count; i++) {
      const ts = new Date(afterMs + i * 1000).toISOString()
      exchanges.push({
        deviceId: 'device-prop7',
        direction: i % 2 === 0 ? 'CPE→ACS' : 'ACS→CPE',
        timestamp: ts,
        sessionId: '10.0.0.1:54321->192.168.1.1:8080',
        cwmpMethod: 'Inform',
        rawXml: '<soap/>',
        sequenceNumber: i,
      })
    }
    return exchanges
  }

  // ─── Property Tests ──────────────────────────────────────────────────────────

  it('valid ISO 8601 full timestamps: all returned exchanges have timestamp > after value', () => {
    return fc.assert(
      fc.asyncProperty(
        arbValidIso8601,
        fc.integer({ min: 0, max: 20 }),
        async (afterTs, exchangeCount) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)
          mockHasExchanges.mockResolvedValue(true)
          mockGetMetadata.mockResolvedValue({
            recordedFrom: '2020-01-01T00:00:00.000Z',
            recordedUntil: '2030-12-31T23:59:59.999Z',
            count: 100,
          })

          // Simulate exchanges all strictly after `afterTs`
          const exchanges = makeExchangesAfter(afterTs, exchangeCount)
          mockFindByDevice.mockResolvedValue(exchanges)

          const ctx = createHttpContext({
            params: { deviceId: 'device-prop7' },
            qs: { after: afterTs },
          })

          const result = await controller.index(ctx)

          expect(result.status).toBe(200)

          // Verify the `after` param was passed correctly to the model
          expect(mockFindByDevice).toHaveBeenCalledWith(
            'device-prop7',
            expect.objectContaining({ after: afterTs })
          )

          // All returned exchanges must have timestamp > after
          const afterDate = new Date(afterTs).getTime()
          for (const exchange of result.body.exchanges) {
            const exchangeDate = new Date(exchange.timestamp).getTime()
            expect(exchangeDate).toBeGreaterThan(afterDate)
          }
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('valid ISO 8601 date-only format: accepted and passed to model', () => {
    return fc.assert(
      fc.asyncProperty(arbValidIso8601DateOnly, async (afterTs) => {
        vi.clearAllMocks()
        mockIsTraced.mockReturnValue(true)
        mockHasExchanges.mockResolvedValue(true)
        mockGetMetadata.mockResolvedValue({
          recordedFrom: '2020-01-01T00:00:00.000Z',
          recordedUntil: '2030-12-31T23:59:59.999Z',
          count: 100,
        })
        mockFindByDevice.mockResolvedValue([])

        const ctx = createHttpContext({
          params: { deviceId: 'device-prop7' },
          qs: { after: afterTs },
        })

        const result = await controller.index(ctx)

        expect(result.status).toBe(200)
        expect(mockFindByDevice).toHaveBeenCalledWith(
          'device-prop7',
          expect.objectContaining({ after: afterTs })
        )
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('valid ISO 8601 with timezone offsets: accepted and passed to model', () => {
    return fc.assert(
      fc.asyncProperty(arbValidIso8601WithOffset, async (afterTs) => {
        vi.clearAllMocks()
        mockIsTraced.mockReturnValue(true)
        mockHasExchanges.mockResolvedValue(true)
        mockGetMetadata.mockResolvedValue({
          recordedFrom: '2020-01-01T00:00:00.000Z',
          recordedUntil: '2030-12-31T23:59:59.999Z',
          count: 100,
        })
        mockFindByDevice.mockResolvedValue([])

        const ctx = createHttpContext({
          params: { deviceId: 'device-prop7' },
          qs: { after: afterTs },
        })

        const result = await controller.index(ctx)

        expect(result.status).toBe(200)
        expect(mockFindByDevice).toHaveBeenCalledWith(
          'device-prop7',
          expect.objectContaining({ after: afterTs })
        )
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('invalid timestamp strings: API returns HTTP 400', () => {
    return fc.assert(
      fc.asyncProperty(arbInvalidTimestamp, async (invalidTs) => {
        vi.clearAllMocks()

        const ctx = createHttpContext({
          params: { deviceId: 'device-prop7' },
          qs: { after: invalidTs },
        })

        const result = await controller.index(ctx)

        expect(result.status).toBe(400)
        expect(result.body.error).toContain('Invalid after')
      }),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('returned exchanges are guaranteed to have timestamps strictly greater than after value', () => {
    return fc.assert(
      fc.asyncProperty(
        arbValidIso8601,
        fc.integer({ min: 1, max: 50 }),
        async (afterTs, count) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)
          mockHasExchanges.mockResolvedValue(true)
          mockGetMetadata.mockResolvedValue({
            recordedFrom: '2020-01-01T00:00:00.000Z',
            recordedUntil: '2030-12-31T23:59:59.999Z',
            count: 100,
          })

          // Model returns exchanges all strictly after afterTs
          const exchanges = makeExchangesAfter(afterTs, count)
          mockFindByDevice.mockResolvedValue(exchanges)

          const ctx = createHttpContext({
            params: { deviceId: 'device-prop7' },
            qs: { after: afterTs },
          })

          const result = await controller.index(ctx)

          expect(result.status).toBe(200)
          const afterMs = new Date(afterTs).getTime()

          for (const ex of result.body.exchanges) {
            const exMs = new Date(ex.timestamp).getTime()
            expect(exMs).toBeGreaterThan(afterMs)
          }

          // No exchange should violate the constraint
          const violating = result.body.exchanges.filter(
            (ex: any) => new Date(ex.timestamp).getTime() <= afterMs
          )
          expect(violating).toHaveLength(0)
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('future dates as after: accepted as valid ISO 8601 and returns empty results', () => {
    return fc.assert(
      fc.asyncProperty(
        fc.integer({ min: 3786912000000, max: 4102444799999 }).map((ms) => new Date(ms).toISOString()),
        async (futureTs) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)
          mockHasExchanges.mockResolvedValue(true)
          mockGetMetadata.mockResolvedValue({
            recordedFrom: '2020-01-01T00:00:00.000Z',
            recordedUntil: '2030-12-31T23:59:59.999Z',
            count: 100,
          })
          mockFindByDevice.mockResolvedValue([])

          const ctx = createHttpContext({
            params: { deviceId: 'device-prop7' },
            qs: { after: futureTs },
          })

          const result = await controller.index(ctx)

          expect(result.status).toBe(200)
          expect(result.body.exchanges).toHaveLength(0)
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })

  it('epoch timestamp (1970-01-01T00:00:00.000Z): accepted as valid and returns all subsequent exchanges', () => {
    return fc.assert(
      fc.asyncProperty(
        fc.integer({ min: 1, max: 20 }),
        async (count) => {
          vi.clearAllMocks()
          mockIsTraced.mockReturnValue(true)
          mockHasExchanges.mockResolvedValue(true)
          mockGetMetadata.mockResolvedValue({
            recordedFrom: '2020-01-01T00:00:00.000Z',
            recordedUntil: '2030-12-31T23:59:59.999Z',
            count: 100,
          })

          const epochTimestamp = '1970-01-01T00:00:00.000Z'
          const exchanges = makeExchangesAfter(epochTimestamp, count)
          mockFindByDevice.mockResolvedValue(exchanges)

          const ctx = createHttpContext({
            params: { deviceId: 'device-prop7' },
            qs: { after: epochTimestamp },
          })

          const result = await controller.index(ctx)

          expect(result.status).toBe(200)
          expect(result.body.exchanges).toHaveLength(count)

          const epochMs = new Date(epochTimestamp).getTime()
          for (const ex of result.body.exchanges) {
            expect(new Date(ex.timestamp).getTime()).toBeGreaterThan(epochMs)
          }
        }
      ),
      { numRuns: PBT_NUM_RUNS }
    )
  })
})