import { describe, expect, it } from "vitest";
import fc from "fast-check";
import type { Message } from "@slackwsh/contracts";
import { ChannelSync } from "./channel-sync";
import { MessageStore } from "./message-store";
import { clampReadSeq, channelUnreadCount, threadUnreadCount } from "./invariants";
import { runTrace } from "./harness/world";
import { NO_FAULTS } from "./harness/sim";

function msg(seq: number, overrides: Partial<Message> = {}): Message {
  return {
    id: seq,
    workspaceId: 1,
    channelId: 1,
    seq,
    clientMsgId: `00000000-0000-4000-8000-${seq.toString(16).padStart(12, "0")}`,
    authorId: 1,
    type: "text",
    text: `msg ${seq}`,
    blocks: { v: 1, doc: {} },
    revision: 0,
    parentId: null,
    isBroadcast: false,
    threadReplyCount: 0,
    threadLastReplyAt: null,
    editedAt: null,
    deletedAt: null,
    createdAt: new Date(0).toISOString(),
    ...overrides,
  };
}

describe("I1–I9 property suite (fast-check)", () => {
  it("I1–I9 hold for random action traces with injected faults", async () => {
    await fc.assert(
      fc.asyncProperty(fc.integer({ min: 1, max: 0x7fffffff }), async (seed) => {
        await runTrace({ seed, actionCount: 16 });
      }),
      { numRuns: 40, timeout: 20_000 },
    );
  }, 90_000);

  it("I4: random ack/mark-unread sequences never produce a negative cursor", () => {
    fc.assert(
      fc.property(
        fc.array(fc.record({ seq: fc.nat({ max: 40 }), decrease: fc.boolean() }), { minLength: 1, maxLength: 30 }),
        (ops) => {
          let cursor = 0;
          for (const op of ops) {
            cursor = clampReadSeq(cursor, op.seq, op.decrease);
            expect(cursor).toBeGreaterThanOrEqual(0);
          }
        },
      ),
      { numRuns: 100 },
    );
  });

  it("I5/I5b: channel unread never includes hidden replies; thread unread does", () => {
    fc.assert(
      fc.property(
        fc.array(
          fc.record({
            author: fc.constantFrom(1, 2),
            parent: fc.constantFrom(null, 1) as fc.Arbitrary<number | null>,
            broadcast: fc.boolean(),
            deleted: fc.boolean(),
          }),
          { minLength: 1, maxLength: 12 },
        ),
        fc.nat({ max: 12 }),
        (rows, lastRead) => {
          const log = rows.map((row, i) =>
            msg(i + 1, {
              id: i + 1,
              authorId: row.author,
              parentId: i === 0 ? null : row.parent,
              isBroadcast: row.broadcast,
              deletedAt: row.deleted ? new Date(0).toISOString() : null,
            }),
          );
          const channel = channelUnreadCount(log, lastRead, 1);
          const naive = log.filter(
            (m) => m.seq > lastRead && Number(m.authorId) !== 1 && m.deletedAt == null,
          ).length;
          expect(channel).toBeLessThanOrEqual(naive);
          const hidden = log.filter(
            (m) =>
              m.seq > lastRead &&
              Number(m.authorId) !== 1 &&
              m.deletedAt == null &&
              m.parentId != null &&
              !m.isBroadcast,
          ).length;
          expect(channel).toBe(naive - hidden);
          expect(threadUnreadCount(log, 1, 0, 1)).toBeGreaterThanOrEqual(0);
        },
      ),
      { numRuns: 80 },
    );
  });

  it("I7: live events buffered during catch-up never render ahead of backfill", async () => {
    await fc.assert(
      fc.asyncProperty(
        fc.array(fc.integer({ min: 2, max: 12 }), { minLength: 1, maxLength: 6 }),
        async (liveSeqs) => {
          const unique = [...new Set(liveSeqs)].sort((a, b) => a - b);
          const store = new MessageStore();
          let release!: (v: Message[]) => void;
          const fetch = () => new Promise<Message[]>((resolve) => (release = resolve));
          const sync = new ChannelSync("1", store, fetch, 0);
          const started = sync.start();
          for (const seq of unique) await sync.onLiveMessage(msg(seq));
          expect(store.getMessages("1")).toHaveLength(0);
          expect(sync.getState()).toBe("catchingUp");
          release([msg(1)]);
          await started;
          expect(sync.getState()).toBe("live");
          const seqs = store.getMessages("1").map((m) => m.seq);
          expect(seqs[0]).toBe(1);
          for (let i = 1; i < seqs.length; i++) expect(seqs[i]!).toBeGreaterThan(seqs[i - 1]!);
        },
      ),
      { numRuns: 30 },
    );
  });

  it("a clean (no-fault) two-client send still converges", async () => {
    await runTrace({
      seed: 1,
      faults: NO_FAULTS,
      actions: [
        { type: "send", client: 0, kind: "plain" },
        { type: "send", client: 1, kind: "mention" },
        { type: "reply", client: 0, broadcast: false },
        { type: "reply", client: 1, broadcast: true },
        { type: "ack", client: 0 },
        { type: "ackThread", client: 0 },
      ],
    });
  });
});