diff --git a/.gitignore b/.gitignore index efe1267f..95498994 100644 --- a/.gitignore +++ b/.gitignore @@ -7,3 +7,6 @@ example # Nix /.direnv/ + +# quint verify (Apalache) output +/_apalache-out/ diff --git a/PROTOCOL.md b/PROTOCOL.md index 453b50e2..93d96ded 100644 --- a/PROTOCOL.md +++ b/PROTOCOL.md @@ -51,6 +51,8 @@ The protocol specification defines semantics around: Note that this protocol specification does NOT detail the language-level specifics of how the client returns results to the caller and how the server executes the procedure invocations but rather the wire-level protocol that the client and server must adhere to. +[`spec/river.qnt`](./spec/README.md) is an executable [Quint](https://quint-lang.org) model of this document, and the test suite checks the implementation against it. + ## Clients, servers, and RPCs - A 'client' can initiate remote procedure calls to the server @@ -474,26 +476,26 @@ server: ! ##### Subscription -A `subscription` procedure starts with the client sending a single message with the `StreamOpenBit` set and remains open until either side ends the stream by sending a `ControlClose` message. The party receiving the `ControlClose` message must respond with a final `ControlClose` message. If the client initiates the closing, it MUST continue to accept data until the other side sends a `ControlClose` message. +A `subscription` procedure starts with the client sending a single message with `StreamOpenBit` and `StreamClosedBit` set, so the client sends nothing else on the stream. The server may send any number of messages and ends the stream by sending a `ControlClose` message. The client ends a subscription early by cancelling it, which is an immediate full close. -Client initiated close: +Server initiated close: ``` -client: > { -server: - -- - -- { +client: x +server: - -- - { ``` -Server initiated close: +Client cancellation: ``` -client: > { -server: - -- - { +client: x ! +server: - -- - ``` Protocol error (abrupt close): ``` -client: > (any further messages are ignored) +client: x (any further messages are ignored) server: - -- ! ``` diff --git a/__tests__/conformance/conformance.test.ts b/__tests__/conformance/conformance.test.ts new file mode 100644 index 00000000..e0e30d97 --- /dev/null +++ b/__tests__/conformance/conformance.test.ts @@ -0,0 +1,113 @@ +import { beforeAll, describe, expect, test } from 'vitest'; +import { BinaryCodec, NaiveJsonCodec, type Codec } from '../../codec'; +import { ProtoCodec } from '../../protobuf/codec'; +import type { Trace } from './model'; +import { scenarioTraces, traceBatches } from './quint'; +import { formatOutcome, replay, type KnownBug } from './replay'; + +/** + * Replays traces of spec/river.qnt against the real transports, router, and + * client over each codec, failing on the first step where the two disagree. + * See spec/README.md. + * + * QUINT_SEED seed for the random traces (default 0x5eed); `random` + * picks a fresh one, shown in the test name + * QUINT_TRACES how many random traces (default 100) + * QUINT_STEPS steps per random trace (default 60) + * QUINT_BACKEND typescript (default) or rust, for long local runs + * QUINT_VERBOSE print how each random trace ended + */ +const SEED = + process.env.QUINT_SEED === 'random' + ? `0x${Math.floor(Math.random() * 2 ** 32).toString(16)}` + : process.env.QUINT_SEED ?? '0x5eed'; +const TRACES = Number(process.env.QUINT_TRACES ?? '100'); +const STEPS = Number(process.env.QUINT_STEPS ?? '60'); + +/** + * Divergences the model has found that are not fixed yet. Random traces stop + * just before a known bug's trigger; once a bug is fixed, its scenario stops + * reproducing and the entry has to go. + */ +const KNOWN_BUGS: Array = []; + +/** Every trace is replayed over each codec the transports can use. */ +const CODECS: Array<{ name: string; codec: Codec }> = [ + { name: 'json', codec: NaiveJsonCodec }, + { name: 'binary', codec: BinaryCodec }, + { name: 'proto', codec: ProtoCodec }, +]; + +async function failuresOf( + traces: Array, + codec: Codec, + tally?: Record, +): Promise> { + const failures: Array = []; + for (const trace of traces) { + const outcome = await replay(trace, KNOWN_BUGS, codec); + if (tally) { + const key = outcome.kind === 'known-bug' ? outcome.bug.id : outcome.kind; + tally[key] = (tally[key] ?? 0) + 1; + } + + if (outcome.kind === 'diverged' || outcome.kind === 'error') { + failures.push(formatOutcome(trace, outcome)); + if (failures.length >= 3) break; + } + } + + return failures; +} + +let scenarios: Array = []; +beforeAll(() => { + scenarios = scenarioTraces(); +}, 120_000); + +describe.each(CODECS)( + 'the implementation conforms to spec/river.qnt over the $name codec', + ({ codec }) => { + test('every scenario in spec/river_test.qnt replays identically', async () => { + expect(scenarios.length).toBeGreaterThan(0); + expect((await failuresOf(scenarios, codec)).join('\n\n')).toBe(''); + }, 60_000); + + if (KNOWN_BUGS.length > 0) { + test.each(KNOWN_BUGS)('known bug $id still reproduces', async (bug) => { + const trace = scenarios.find((t) => + t.name.includes(`${bug.scenario}_`), + ); + if (!trace) throw new Error(`no scenario named ${bug.scenario}`); + + const outcome = await replay(trace, [], codec); + expect( + outcome.kind === 'diverged' || outcome.kind === 'error', + `${bug.id} no longer reproduces: remove it from KNOWN_BUGS`, + ).toBe(true); + }); + } + }, +); + +test(`${TRACES} random traces (seed ${SEED}) replay identically over every codec`, async () => { + const failures: Array = []; + const tallies = new Map( + CODECS.map(({ name }) => [name, {} as Record]), + ); + for (const batch of traceBatches({ + seed: SEED, + count: TRACES, + maxSteps: STEPS, + })) { + for (const { name, codec } of CODECS) { + const found = await failuresOf(batch, codec, tallies.get(name)); + failures.push(...found.map((failure) => `[${name} codec] ${failure}`)); + } + + if (failures.length > 0) break; + } + + if (process.env.QUINT_VERBOSE) console.log(Object.fromEntries(tallies)); + expect(failures.slice(0, 3).join('\n\n')).toBe(''); +}, 1_800_000); diff --git a/__tests__/conformance/harness.ts b/__tests__/conformance/harness.ts new file mode 100644 index 00000000..f4b6df08 --- /dev/null +++ b/__tests__/conformance/harness.ts @@ -0,0 +1,768 @@ +import type { Clock } from '@sinonjs/fake-timers'; +import { Type } from 'typebox'; +import { Ok, Procedure, createServiceSchema, type Result } from '../../router'; +import { createClient } from '../../router/client'; +import { createServer } from '../../router/server'; +import { NaiveJsonCodec } from '../../codec/json'; +import type { Codec } from '../../codec/types'; +import { + ControlFlags, + type OpaqueTransportMessage, +} from '../../transport/message'; +import { SessionState } from '../../transport/sessionStateMachine/common'; +import { + ScriptedClientTransport, + ScriptedNetwork, + ScriptedServerTransport, +} from './network'; +import { some, type QAction, type QCfg, type QState } from './model'; +import type { + Body, + ClientStreamView, + ConnView, + Frame, + Msg, + ProcTag, + Projection, + Res, + ServerStreamView, + SessionView, +} from './projection'; + +export const CLIENT_ID = 'client'; +export const SERVER_ID = 'SERVER'; + +const Init = Type.Object({ sid: Type.Number() }); +const Payload = Type.Object({ v: Type.Number() }); +const ServiceSchema = createServiceSchema(); + +interface Deferred { + promise: Promise; + resolve: (value: T) => void; + reject: (err: Error) => void; +} + +function deferred(): Deferred { + let resolve: ((value: T) => void) | undefined; + let reject: ((err: Error) => void) | undefined; + const promise = new Promise((res, rej) => { + resolve = res; + reject = rej; + }); + if (!resolve || !reject) throw new Error('unreachable'); + + return { promise, resolve, reject }; +} + +function toRes(result: unknown): Res { + const r = result as { + ok: boolean; + payload: { v?: number; code?: string }; + }; + + return r.ok + ? { ok: true, v: r.payload.v ?? Number.NaN } + : { ok: false, code: r.payload.code ?? '' }; +} + +function isClosed(readable: object): boolean { + return (readable as { isClosed: () => boolean }).isClosed(); +} + +/** Consumes a readable in the background, recording everything it yields. */ +function drain(readable: object, into: Array) { + void (async () => { + for await (const result of readable as AsyncIterable) { + into.push(toRes(result)); + } + })(); +} + +/** + * Handles on one server-side procedure invocation. Handlers stay pending until + * the trace resolves or rejects them, so the trace decides when servers reply. + */ +interface ServerRecord { + respond: (v: number) => void; + fail: () => void; + cancel: () => void; + write?: (v: number) => void; + closeWritable?: () => void; + writable?: () => boolean; + readableClosed?: () => boolean; + values?: Array; +} + +interface ClientRecord { + abort: AbortController; + write?: (v: number) => void; + close?: () => void; + writable?: () => boolean; + readableClosed?: () => boolean; + results: Array; + finalize?: () => void; + /** The awaited result of an rpc, or of an upload once finalized. */ + single?: { settled: boolean; value: Res | null }; +} + +const unexpected = () => { + throw new Error('model asked this procedure type for something it cannot do'); +}; + +function makeServices(h: Harness) { + return { + svc: ServiceSchema.define({ + rpc: Procedure.rpc({ + requestInit: Init, + responseData: Payload, + handler: async ({ ctx, reqInit }) => { + const done = deferred>(); + h.registerServer(reqInit.sid, { + respond: (v) => { + done.resolve(Ok({ v })); + }, + fail: () => { + done.reject(new Error('handler threw')); + }, + cancel: () => { + ctx.cancel(); + }, + }); + + return done.promise; + }, + }), + stream: Procedure.stream({ + requestInit: Init, + requestData: Payload, + responseData: Payload, + handler: async ({ ctx, reqInit, reqReadable, resWritable }) => { + const done = deferred(); + const values: Array = []; + h.registerServer(reqInit.sid, { + respond: unexpected, + fail: () => { + done.reject(new Error('handler threw')); + }, + cancel: () => { + ctx.cancel(); + }, + write: (v) => { + resWritable.write(Ok({ v })); + }, + closeWritable: () => { + resWritable.close(); + }, + writable: () => resWritable.isWritable(), + readableClosed: () => isClosed(reqReadable), + values, + }); + drain(reqReadable, values); + + return done.promise; + }, + }), + upload: Procedure.upload({ + requestInit: Init, + requestData: Payload, + responseData: Payload, + handler: async ({ ctx, reqInit, reqReadable }) => { + const done = deferred>(); + const values: Array = []; + h.registerServer(reqInit.sid, { + respond: (v) => { + done.resolve(Ok({ v })); + }, + fail: () => { + done.reject(new Error('handler threw')); + }, + cancel: () => { + ctx.cancel(); + }, + readableClosed: () => isClosed(reqReadable), + values, + }); + drain(reqReadable, values); + + return done.promise; + }, + }), + sub: Procedure.subscription({ + requestInit: Init, + responseData: Payload, + handler: async ({ ctx, reqInit, resWritable }) => { + const done = deferred(); + h.registerServer(reqInit.sid, { + respond: unexpected, + fail: () => { + done.reject(new Error('handler threw')); + }, + cancel: () => { + ctx.cancel(); + }, + write: (v) => { + resWritable.write(Ok({ v })); + }, + closeWritable: () => { + resWritable.close(); + }, + writable: () => resWritable.isWritable(), + }); + + return done.promise; + }, + }), + }), + }; +} + +type Services = ReturnType; + +interface RouterInternals { + streams: Map; + serverCancelledStreams: Map }>; +} + +const procTags: Record = { + rpc: 'PRpc', + stream: 'PStream', + upload: 'PUpload', + sub: 'PSubscription', +}; + +/** Lets every pending promise callback run, without touching fake timers. */ +export function flush(): Promise { + return new Promise((resolve) => { + setImmediate(resolve); + }); +} + +/** + * The system under test: a real client and server transport, router, and + * client, wired through a {@link ScriptedNetwork}, running on a fake clock that + * only advances when the trace says so. + */ +export class Harness { + readonly network = new ScriptedNetwork(); + readonly clientTransport: ScriptedClientTransport; + serverTransport: ScriptedServerTransport; + private readonly client: ReturnType>; + private server: ReturnType; + private readonly sessionOptions; + private readonly codec: Codec; + private readonly clock: Clock; + private readonly t0 = Date.now(); + + private readonly cErrs: Array = []; + private readonly sErrs: Array = []; + private cViolations = 0; + private sViolations = 0; + + /** Real session and stream ids, mapped to the model's integers. */ + private readonly sessIds = new Map(); + private readonly streamIds = new Map(); + private readonly realStreamIds = new Map(); + + private readonly clientRecords = new Map(); + private serverRecords = new Map(); + /** Handler invocations per stream id since the server started. */ + private serverRuns = new Map(); + + constructor(cfg: QCfg, clock: Clock, codec: Codec = NaiveJsonCodec) { + this.clock = clock; + this.codec = codec; + this.sessionOptions = { + codec, + heartbeatIntervalMs: cfg.heartbeat, + heartbeatsUntilDead: cfg.heartbeatsUntilDead, + sessionDisconnectGraceMs: cfg.grace, + connectionTimeoutMs: cfg.connectTimeout, + handshakeTimeoutMs: cfg.handshakeTimeout, + enableTransparentSessionReconnects: true, + }; + + this.clientTransport = new ScriptedClientTransport( + CLIENT_ID, + this.network, + { + ...this.sessionOptions, + baseIntervalMs: cfg.backoff, + maxBackoffMs: cfg.backoff, + maxJitterMs: 0, + attemptBudgetCapacity: Number.MAX_SAFE_INTEGER, + // the restore interval never fires within a trace + budgetRestoreIntervalMs: 1_000_000_000, + }, + ); + this.clientTransport.bindLogger((_msg, ctx) => { + if (ctx?.tags?.includes('invariant-violation')) this.cViolations++; + }, 'warn'); + this.clientTransport.addEventListener('protocolError', (evt) => { + this.cErrs.push(evt.type as unknown as string); + }); + + this.client = createClient(this.clientTransport, SERVER_ID, { + eagerlyConnect: false, + }); + + const { transport, server } = this.startServer(); + this.serverTransport = transport; + this.server = server; + } + + private startServer() { + const transport = new ScriptedServerTransport( + SERVER_ID, + this.network, + this.sessionOptions, + ); + transport.bindLogger((_msg, ctx) => { + if (ctx?.tags?.includes('invariant-violation')) this.sViolations++; + }, 'warn'); + transport.addEventListener('protocolError', (evt) => { + this.sErrs.push(evt.type as unknown as string); + }); + + return { transport, server: createServer(transport, makeServices(this)) }; + } + + registerServer(sid: number, record: ServerRecord) { + this.serverRuns.set(sid, (this.serverRuns.get(sid) ?? 0) + 1); + this.serverRecords.set(sid, record); + } + + private clientRecord(sid: number): ClientRecord { + const record = this.clientRecords.get(sid); + if (!record) throw new Error(`no client stream ${sid}`); + + return record; + } + + private serverRecord(sid: number): ServerRecord { + const record = this.serverRecords.get(sid); + if (!record) throw new Error(`no server stream ${sid}`); + + return record; + } + + async apply(action: QAction) { + switch (action.tag) { + case 'AInit': + break; + case 'AInvoke': + this.invoke(action.value.sid, action.value.pt.tag); + break; + case 'AWrite': + (this.clientRecord(action.value.sid).write ?? unexpected)( + action.value.v, + ); + break; + case 'AClose': + (this.clientRecord(action.value).close ?? unexpected)(); + break; + case 'AFinalize': + (this.clientRecord(action.value).finalize ?? unexpected)(); + break; + case 'ACancel': + this.clientRecord(action.value).abort.abort(); + break; + case 'ARespond': + this.serverRecord(action.value.sid).respond(action.value.v); + break; + case 'ASWrite': + (this.serverRecord(action.value.sid).write ?? unexpected)( + action.value.v, + ); + break; + case 'ASClose': + (this.serverRecord(action.value).closeWritable ?? unexpected)(); + break; + case 'ASCancel': + this.serverRecord(action.value).cancel(); + break; + case 'AThrow': + this.serverRecord(action.value).fail(); + break; + case 'ADeliver': + this.network.deliver(action.value.conn, action.value.toServer); + break; + case 'ADrop': + this.network.drop(action.value.conn, action.value.toServer); + break; + case 'ABreak': + this.network.close(action.value); + break; + case 'ACloseEvent': + this.network.closeEvent(action.value.conn, action.value.server); + break; + case 'AGarbage': + this.network.garbage(action.value.conn, action.value.server); + break; + case 'ADialOk': + this.network.completeDial(action.value); + break; + case 'ADialFail': + this.network.failDial(action.value); + break; + case 'ATick': + this.clock.tick(action.value); + break; + case 'AFire': + // exactly one timer: same-instant timers are separate model steps + this.clock.next(); + break; + case 'ARestart': + this.restartServer(); + break; + case 'AServerClose': + this.serverTransport.close(); + break; + case 'AHardDisconnect': + this.clientTransport.hardDisconnect(); + break; + } + + await flush(); + } + + private invoke(sid: number, pt: ProcTag) { + const abort = new AbortController(); + const options = { signal: abort.signal }; + const init = { sid }; + const record: ClientRecord = { abort, results: [] }; + const settle = (res: unknown) => { + record.single = { settled: true, value: toRes(res) }; + }; + + switch (pt) { + case 'PRpc': { + record.single = { settled: false, value: null }; + void this.client.svc.rpc.rpc(init, options).then(settle); + break; + } + case 'PStream': { + const { reqWritable, resReadable } = this.client.svc.stream.stream( + init, + options, + ); + record.write = (v) => { + reqWritable.write({ v }); + }; + record.close = () => { + reqWritable.close(); + }; + record.writable = () => reqWritable.isWritable(); + record.readableClosed = () => isClosed(resReadable); + drain(resReadable, record.results); + break; + } + case 'PUpload': { + const { reqWritable, finalize } = this.client.svc.upload.upload( + init, + options, + ); + record.write = (v) => { + reqWritable.write({ v }); + }; + record.close = () => { + reqWritable.close(); + }; + record.finalize = () => { + record.single = { settled: false, value: null }; + void finalize().then(settle); + }; + record.writable = () => reqWritable.isWritable(); + break; + } + case 'PSubscription': { + const { resReadable } = this.client.svc.sub.subscribe(init, options); + record.readableClosed = () => isClosed(resReadable); + drain(resReadable, record.results); + break; + } + } + + this.clientRecords.set(sid, record); + this.learnStreamId(sid); + } + + /** The init message an invocation just buffered carries the real stream id. */ + private learnStreamId(sid: number) { + const session = this.clientTransport.sessions.get(SERVER_ID); + for (const encoded of session?.sendBuffer ?? []) { + const payload = encoded.msg.payload as { sid?: unknown } | null; + if (payload?.sid === sid) { + this.streamIds.set(encoded.msg.streamId, sid); + this.realStreamIds.set(sid, encoded.msg.streamId); + + return; + } + } + + throw new Error(`no init message buffered for stream ${sid}`); + } + + private restartServer() { + this.network.crashServer(); + this.serverTransport.crash(); + this.serverRecords = new Map(); + this.serverRuns = new Map(); + const { transport, server } = this.startServer(); + this.serverTransport = transport; + this.server = server; + } + + dispose() { + try { + this.clientTransport.close(); + this.serverTransport.close(); + } catch { + // teardown after a divergence may hit inconsistent state; nothing to report + } + } + + ////////////////////////////////////////////////////////////////////////////// + // Projection + ////////////////////////////////////////////////////////////////////////////// + + /** + * Model and implementation name sessions differently; the first time a real + * session appears where the model has one, they are unified. + */ + private sessFor(realId: string, modelSess: number | undefined): number { + const known = this.sessIds.get(realId); + if (known !== undefined) return known; + if (modelSess === undefined) return -1; + if ([...this.sessIds.values()].includes(modelSess)) return -1; + this.sessIds.set(realId, modelSess); + + return modelSess; + } + + private decode(bytes: Uint8Array): OpaqueTransportMessage { + return this.codec.fromBuffer(bytes) as OpaqueTransportMessage; + } + + private projectBody(msg: OpaqueTransportMessage, toServer: boolean): Body { + const flags = msg.controlFlags; + const has = (bit: ControlFlags) => (flags & bit) !== 0; + const payload = msg.payload as Record; + if (has(ControlFlags.AckBit)) return { kind: 'Heartbeat' }; + if (has(ControlFlags.StreamOpenBit)) { + return { + kind: 'SInit', + sid: payload.sid as number, + pt: procTags[msg.procedureName ?? ''], + close: has(ControlFlags.StreamClosedBit), + }; + } + + const sid = this.streamIds.get(msg.streamId) ?? -1; + if (has(ControlFlags.StreamCancelBit)) { + const err = payload.payload as { code: string }; + + return { kind: 'SCancel', sid, code: err.code }; + } + + if (has(ControlFlags.StreamClosedBit) && payload.type === 'CLOSE') { + return { kind: 'SClose', sid }; + } + + if (toServer) return { kind: 'SData', sid, v: payload.v as number }; + const ok = payload.payload as { v: number }; + + return { + kind: 'SResult', + sid, + v: ok.v, + close: has(ControlFlags.StreamClosedBit), + }; + } + + private projectMsg(bytes: Uint8Array, toServer: boolean): Msg { + const msg = this.decode(bytes); + + return { + seq: msg.seq, + ack: msg.ack, + body: this.projectBody(msg, toServer), + }; + } + + private projectFrame(bytes: Uint8Array, toServer: boolean): Frame { + const msg = this.decode(bytes); + const payload = msg.payload as Record | null; + if (payload?.type === 'HANDSHAKE_REQ') { + const expected = payload.expectedSessionState as { + nextExpectedSeq: number; + nextSentSeq: number; + }; + + return { + kind: 'HsReq', + sess: this.sessIds.get(payload.sessionId as string) ?? -1, + nextExpectedSeq: expected.nextExpectedSeq, + nextSentSeq: expected.nextSentSeq, + }; + } + + if (payload?.type === 'HANDSHAKE_RESP') { + const status = payload.status as { + ok: boolean; + sessionId?: string; + code?: string; + }; + + return status.ok + ? { + kind: 'HsResp', + ok: true, + sess: this.sessIds.get(status.sessionId ?? '') ?? -1, + code: '', + } + : { kind: 'HsResp', ok: false, sess: 0, code: status.code ?? '' }; + } + + return { + kind: 'Data', + seq: msg.seq, + ack: msg.ack, + body: this.projectBody(msg, toServer), + }; + } + + private projectClient(model: QState): SessionView | null { + const session = this.clientTransport.sessions.get(SERVER_ID); + if (!session) return null; + + const sess = this.sessFor(session.id, some(model.client.session)?.sess); + const buf = session.sendBuffer.map((m) => this.projectMsg(m.data, true)); + const common = { + sess, + state: session.state as string, + seq: session.seq, + ack: session.ack, + seqSent: session.seqSent, + buf, + }; + + switch (session.state) { + case SessionState.Connected: + return { ...common, on: session.conn.linkId, grace: null }; + case SessionState.Handshaking: + return { + ...common, + on: session.conn.linkId, + grace: session.graceExpiryTime - this.t0, + }; + case SessionState.Connecting: + return { + ...common, + on: this.network.lastDial, + grace: session.graceExpiryTime - this.t0, + }; + case SessionState.NoConnection: + case SessionState.BackingOff: + return { + ...common, + on: null, + grace: session.graceExpiryTime - this.t0, + }; + } + } + + private projectServer(model: QState): SessionView | null { + const session = this.serverTransport.sessions.get(CLIENT_ID); + if (!session) return null; + + const common = { + sess: this.sessFor(session.id, some(model.server.session)?.sess), + state: session.state as string, + seq: session.seq, + ack: session.ack, + seqSent: session.seqSent, + buf: session.sendBuffer.map((m) => this.projectMsg(m.data, false)), + }; + + return session.state === SessionState.Connected + ? { ...common, on: session.conn.linkId, grace: null } + : { ...common, on: null, grace: session.graceExpiryTime - this.t0 }; + } + + private projectClientStream(record: ClientRecord): ClientStreamView { + const { single, readableClosed } = record; + if (readableClosed) { + return { + w: record.writable?.() ?? null, + r: !readableClosed(), + results: [...record.results], + }; + } + + return { + w: record.writable?.() ?? null, + r: single ? !single.settled : null, + results: single ? (single.value ? [single.value] : []) : null, + }; + } + + project(model: QState): Projection { + const router = this.server as unknown as RouterInternals; + + const conns: Record = {}; + for (const link of this.network.links.values()) { + conns[link.id] = { + toServer: link.toServer.map((b) => this.projectFrame(b, true)), + toClient: link.toClient.map((b) => this.projectFrame(b, false)), + closed: link.closed, + clientEv: link.clientEv, + serverEv: link.serverEv, + }; + } + + const cStreams: Record = {}; + for (const [sid, record] of this.clientRecords) { + cStreams[sid] = this.projectClientStream(record); + } + + const sStreams: Record = {}; + for (const [sid, record] of this.serverRecords) { + const realId = this.realStreamIds.get(sid) ?? ''; + sStreams[sid] = { + r: record.readableClosed ? !record.readableClosed() : null, + w: record.writable?.() ?? null, + inMap: router.streams.has(realId), + runs: this.serverRuns.get(sid) ?? 0, + values: record.values ? [...record.values] : null, + }; + } + + const tombstones = router.serverCancelledStreams.get(CLIENT_ID)?.items; + + return { + now: Date.now() - this.t0, + client: this.projectClient(model), + server: { + closed: this.serverTransport.getStatus() === 'closed', + pending: Array.from( + this.serverTransport.pendingSessions, + (pending) => pending.conn.linkId, + ).sort((a, b) => a - b), + session: this.projectServer(model), + tombstones: Array.from( + tombstones ?? [], + (id) => this.streamIds.get(id) ?? -1, + ).sort((a, b) => a - b), + }, + conns, + dials: [...this.network.dials.keys()].sort((a, b) => a - b), + cStreams, + sStreams, + cErrs: [...this.cErrs], + sErrs: [...this.sErrs], + cViolations: this.cViolations, + sViolations: this.sViolations, + timers: this.clock.countTimers(), + }; + } +} diff --git a/__tests__/conformance/model.ts b/__tests__/conformance/model.ts new file mode 100644 index 00000000..7677c490 --- /dev/null +++ b/__tests__/conformance/model.ts @@ -0,0 +1,433 @@ +import type { + Body, + ClientStreamView, + ConnView, + Frame, + Msg, + ProcTag, + Projection, + Res, + ServerStreamView, + SessionView, +} from './projection'; + +/** + * Types of spec/river.qnt state after ITF decoding: integers become numbers, + * sets become arrays, maps become Maps, and sum types become `{ tag, value }`. + */ + +export interface Variant { + tag: T; + value: V; +} + +type Unit = Array; + +export type QOption = Variant<'Some', T> | Variant<'None'>; + +export interface QTimer { + at: number; + id: number; +} + +export type QProcType = Variant; + +export type QRes = Variant<'ROk', number> | Variant<'RErr', string>; + +export type QBody = + | Variant<'Heartbeat'> + | Variant<'SInit', { sid: number; pt: QProcType; close: boolean }> + | Variant<'SData', { sid: number; v: number }> + | Variant<'SResult', { sid: number; v: number; close: boolean }> + | Variant<'SClose', number> + | Variant<'SCancel', { sid: number; code: string }>; + +export interface QMsg { + seq: number; + ack: number; + body: QBody; + sess: number; +} + +export type QFrame = + | Variant< + 'HsReq', + { sess: number; nextExpectedSeq: number; nextSentSeq: number } + > + | Variant<'HsResp', { ok: boolean; sess: number; code: string }> + | Variant<'Data', QMsg>; + +export interface QConn { + toServer: Array; + toClient: Array; + closed: boolean; + clientEv: boolean; + serverEv: boolean; +} + +export type QCState = + | Variant<'CNoConn'> + | Variant<'CBackingOff'> + | Variant<'CConnecting', number> + | Variant<'CHandshaking', number> + | Variant<'CConnected', number>; + +export type QSState = Variant<'SNoConn'> | Variant<'SConnected', number>; + +interface QSessionCommon { + sess: number; + seq: number; + ack: number; + seqSent: number; + buf: Array; + grace: QOption; + wd: QOption; + lastInbound: number; +} + +export interface QClientSession extends QSessionCommon { + st: QCState; + stTimer: QOption; +} + +export interface QServerSession extends QSessionCommon { + st: QSState; + hb: QOption; +} + +export interface QCStream { + pt: QProcType; + sess: number; + w: boolean; + r: boolean; + clean: boolean; + listening: boolean; + aborted: boolean; + results: Array; + written: Array; + gotCancel: boolean; + finalized: boolean; + sentClose: boolean; +} + +export interface QSStream { + pt: QProcType; + sess: number; + r: boolean; + w: boolean; + clean: boolean; + inMap: boolean; + handlerDone: boolean; + runs: number; + values: Array; + written: Array; + gotCancel: boolean; + sentClose: boolean; +} + +export interface QCfg { + grace: number; + connectTimeout: number; + handshakeTimeout: number; + backoff: number; + heartbeat: number; + heartbeatsUntilDead: number; + maxStreams: number; + maxWrites: number; +} + +export interface QState { + cfg: QCfg; + now: number; + ids: { + sess: number; + conn: number; + dial: number; + stream: number; + timer: number; + }; + client: { + session: QOption; + attempts: number; + restoreActive: boolean; + }; + server: { + pending: Map; + session: QOption; + tombstones: Array; + epoch: number; + closed: boolean; + }; + conns: Map; + dials: Array; + cStreams: Map; + sStreams: Map; + obs: { + cErrs: Array; + sErrs: Array; + cOoo: number; + sOoo: number; + rejections: Array; + }; +} + +export type QTimerRef = + | Variant<'TClientGrace'> + | Variant<'TClientState'> + | Variant<'TClientWd'> + | Variant<'TPendingHs', number> + | Variant<'TServerGrace'> + | Variant<'TServerWd'> + | Variant<'TServerHb'>; + +export type QAction = + | Variant<'AInit'> + | Variant<'AInvoke', { sid: number; pt: QProcType }> + | Variant<'AWrite', { sid: number; v: number }> + | Variant<'AClose', number> + | Variant<'AFinalize', number> + | Variant<'ACancel', number> + | Variant<'ARespond', { sid: number; v: number }> + | Variant<'ASWrite', { sid: number; v: number }> + | Variant<'ASClose', number> + | Variant<'ASCancel', number> + | Variant<'AThrow', number> + | Variant<'ADeliver', { conn: number; toServer: boolean }> + | Variant<'ADrop', { conn: number; toServer: boolean }> + | Variant<'ABreak', number> + | Variant<'ACloseEvent', { conn: number; server: boolean }> + | Variant<'AGarbage', { conn: number; server: boolean }> + | Variant<'ADialOk', number> + | Variant<'ADialFail', number> + | Variant<'ATick', number> + | Variant<'AFire', QTimerRef> + | Variant<'ARestart'> + | Variant<'AServerClose'> + | Variant<'AHardDisconnect'>; + +export interface TraceStep { + st: QState; + action: QAction; +} + +export interface Trace { + name: string; + steps: Array; +} + +/** Decodes Informal Trace Format values into plain JavaScript values. */ +export function decodeItf(value: unknown): unknown { + if (Array.isArray(value)) return value.map(decodeItf); + if (typeof value !== 'object' || value === null) return value; + + const obj = value as Record; + if ('#bigint' in obj) return Number(obj['#bigint']); + if ('#set' in obj) return (obj['#set'] as Array).map(decodeItf); + if ('#tup' in obj) return (obj['#tup'] as Array).map(decodeItf); + if ('#map' in obj) { + const entries = obj['#map'] as Array<[unknown, unknown]>; + + return new Map(entries.map(([k, v]) => [decodeItf(k), decodeItf(v)])); + } + + return Object.fromEntries( + Object.entries(obj).map(([k, v]) => [k, decodeItf(v)]), + ); +} + +function variable(state: Record, name: string): unknown { + for (const [key, value] of Object.entries(state)) { + if (key === name || key.endsWith(`::${name}`)) return value; + } + + throw new Error(`trace state has no variable ${name}`); +} + +export function parseTrace(name: string, json: string): Trace { + const itf = JSON.parse(json) as { states: Array> }; + + return { + name, + steps: itf.states.map((state) => ({ + st: decodeItf(variable(state, 'st')) as QState, + action: decodeItf(variable(state, 'lastAction')) as QAction, + })), + }; +} + +export function some(option: QOption): T | null { + return option.tag === 'Some' ? option.value : null; +} + +const clientStateNames: Record = { + CNoConn: 'NoConnection', + CBackingOff: 'BackingOff', + CConnecting: 'Connecting', + CHandshaking: 'Handshaking', + CConnected: 'Connected', +}; + +function projectBody(body: QBody): Body { + switch (body.tag) { + case 'Heartbeat': + return { kind: 'Heartbeat' }; + case 'SInit': + return { + kind: 'SInit', + sid: body.value.sid, + pt: body.value.pt.tag, + close: body.value.close, + }; + case 'SData': + return { kind: 'SData', sid: body.value.sid, v: body.value.v }; + case 'SResult': + return { + kind: 'SResult', + sid: body.value.sid, + v: body.value.v, + close: body.value.close, + }; + case 'SClose': + return { kind: 'SClose', sid: body.value }; + case 'SCancel': + return { kind: 'SCancel', sid: body.value.sid, code: body.value.code }; + } +} + +function projectMsg(msg: QMsg): Msg { + return { seq: msg.seq, ack: msg.ack, body: projectBody(msg.body) }; +} + +function projectFrame(frame: QFrame): Frame { + switch (frame.tag) { + case 'HsReq': + return { kind: 'HsReq', ...frame.value }; + case 'HsResp': + return { kind: 'HsResp', ...frame.value }; + case 'Data': + return { kind: 'Data', ...projectMsg(frame.value) }; + } +} + +function projectRes(res: QRes): Res { + return res.tag === 'ROk' + ? { ok: true, v: res.value } + : { ok: false, code: res.value }; +} + +function graceDeadline(grace: QOption): number | null { + return some(grace)?.at ?? null; +} + +function projectClientSession(cs: QClientSession): SessionView { + const on = + cs.st.tag === 'CConnecting' || + cs.st.tag === 'CHandshaking' || + cs.st.tag === 'CConnected' + ? cs.st.value + : null; + + return { + sess: cs.sess, + state: clientStateNames[cs.st.tag], + on, + seq: cs.seq, + ack: cs.ack, + seqSent: cs.seqSent, + buf: cs.buf.map(projectMsg), + grace: graceDeadline(cs.grace), + }; +} + +function projectServerSession(ss: QServerSession): SessionView { + return { + sess: ss.sess, + state: ss.st.tag === 'SConnected' ? 'Connected' : 'NoConnection', + on: ss.st.tag === 'SConnected' ? ss.st.value : null, + seq: ss.seq, + ack: ss.ack, + seqSent: ss.seqSent, + buf: ss.buf.map(projectMsg), + grace: graceDeadline(ss.grace), + }; +} + +/** Pending timers in the implementation, including the retry budget's restore interval. */ +export function timerCount(st: QState): number { + const present = (o: QOption) => (o.tag === 'Some' ? 1 : 0); + const cs = some(st.client.session); + const ss = some(st.server.session); + const clientTimers = cs + ? present(cs.grace) + present(cs.stTimer) + present(cs.wd) + : 0; + const serverTimers = ss + ? present(ss.grace) + present(ss.wd) + present(ss.hb) + : 0; + + return ( + clientTimers + + st.server.pending.size + + serverTimers + + (st.client.restoreActive ? 1 : 0) + ); +} + +export function projectModel(st: QState): Projection { + const conns: Record = {}; + for (const [id, conn] of st.conns) { + conns[id] = { + toServer: conn.toServer.map(projectFrame), + toClient: conn.toClient.map(projectFrame), + closed: conn.closed, + clientEv: conn.clientEv, + serverEv: conn.serverEv, + }; + } + + const cStreams: Record = {}; + for (const [sid, c] of st.cStreams) { + cStreams[sid] = { w: c.w, r: c.r, results: c.results.map(projectRes) }; + } + + const sStreams: Record = {}; + for (const [sid, x] of st.sStreams) { + sStreams[sid] = { + r: x.r, + w: x.w, + inMap: x.inMap, + runs: x.runs, + values: x.values.map(projectRes), + }; + } + + const cs = some(st.client.session); + const ss = some(st.server.session); + + return { + now: st.now, + client: cs ? projectClientSession(cs) : null, + server: { + closed: st.server.closed, + pending: [...st.server.pending.keys()].sort((a, b) => a - b), + session: ss ? projectServerSession(ss) : null, + tombstones: [...st.server.tombstones].sort((a, b) => a - b), + }, + conns, + dials: [...st.dials].sort((a, b) => a - b), + cStreams, + sStreams, + cErrs: st.obs.cErrs, + sErrs: st.obs.sErrs, + cViolations: st.obs.cOoo, + sViolations: st.obs.sOoo, + timers: timerCount(st), + }; +} + +export function describeAction(action: QAction): string { + if (Array.isArray(action.value) && action.value.length === 0) { + return action.tag; + } + + return `${action.tag}(${JSON.stringify(action.value)})`; +} diff --git a/__tests__/conformance/network.ts b/__tests__/conformance/network.ts new file mode 100644 index 00000000..2e68ca2d --- /dev/null +++ b/__tests__/conformance/network.ts @@ -0,0 +1,211 @@ +import { Connection } from '../../transport/connection'; +import { ClientTransport } from '../../transport/client'; +import { ServerTransport } from '../../transport/server'; +import type { + ProvidedClientTransportOptions, + ProvidedServerTransportOptions, +} from '../../transport/options'; +import type { TransportClientId } from '../../transport/message'; + +/** Bytes no codec can decode. */ +const GARBAGE = new Uint8Array([0x7b]); + +type Side = 'client' | 'server'; + +/** + * One end of a scripted link. Like WebSocket.send on a closing socket, a send + * after the link closed is silently discarded rather than reported as a failure. + */ +export class ScriptedConnection extends Connection { + readonly linkId: number; + private readonly network: ScriptedNetwork; + private readonly side: Side; + + constructor(network: ScriptedNetwork, linkId: number, side: Side) { + super(); + this.network = network; + this.linkId = linkId; + this.side = side; + } + + send(payload: Uint8Array): boolean { + this.network.send(this.linkId, this.side, payload); + + return true; + } + + close(): void { + this.network.close(this.linkId); + } +} + +export interface Link { + id: number; + toServer: Array; + toClient: Array; + closed: boolean; + clientEv: boolean; + serverEv: boolean; + client: ScriptedConnection; + server: ScriptedConnection; +} + +interface PendingDial { + resolve: (conn: ScriptedConnection) => void; + reject: (err: Error) => void; +} + +/** + * A network where nothing happens until the test says so: dials stay pending, + * frames sit in flight, and close events wait until delivered explicitly. This + * lets a model trace choose every interleaving. + */ +export class ScriptedNetwork { + readonly links = new Map(); + readonly dials = new Map(); + private nextLink = 1; + private nextDial = 1; + acceptor: ((conn: ScriptedConnection) => void) | undefined; + + /** The most recent dial, which a Connecting client is waiting on. */ + get lastDial(): number { + return this.nextDial - 1; + } + + dial(): Promise { + const id = this.nextDial++; + + return new Promise((resolve, reject) => { + this.dials.set(id, { resolve, reject }); + }); + } + + /** The server accepts the connection before the client's dial resolves. */ + completeDial(dialId: number) { + const dial = this.takeDial(dialId); + const id = this.nextLink++; + const link: Link = { + id, + toServer: [], + toClient: [], + closed: false, + clientEv: false, + serverEv: false, + client: new ScriptedConnection(this, id, 'client'), + server: new ScriptedConnection(this, id, 'server'), + }; + this.links.set(id, link); + this.acceptor?.(link.server); + dial.resolve(link.client); + } + + failDial(dialId: number) { + this.takeDial(dialId).reject(new Error('dial failed')); + } + + send(linkId: number, from: Side, payload: Uint8Array) { + const link = this.link(linkId); + if (link.closed) return; + + (from === 'client' ? link.toServer : link.toClient).push(payload); + } + + close(linkId: number) { + this.link(linkId).closed = true; + } + + deliver(linkId: number, toServer: boolean) { + const link = this.link(linkId); + const frame = (toServer ? link.toServer : link.toClient).shift(); + if (!frame) throw new Error(`no frame in flight on link ${linkId}`); + + (toServer ? link.server : link.client).onData(frame); + } + + drop(linkId: number, toServer: boolean) { + const link = this.link(linkId); + (toServer ? link.toServer : link.toClient).shift(); + } + + /** A close event reaches one side; frames still headed there are lost. */ + closeEvent(linkId: number, toServer: boolean) { + const link = this.link(linkId); + if (toServer) { + link.serverEv = true; + link.toServer = []; + link.server.onClose(); + } else { + link.clientEv = true; + link.toClient = []; + link.client.onClose(); + } + } + + garbage(linkId: number, toServer: boolean) { + const link = this.link(linkId); + (toServer ? link.server : link.client).onData(GARBAGE); + } + + /** The server process dies: its side of every link is gone. */ + crashServer() { + for (const link of this.links.values()) { + link.closed = true; + link.serverEv = true; + link.toServer = []; + } + } + + private link(id: number): Link { + const link = this.links.get(id); + if (!link) throw new Error(`unknown link ${id}`); + + return link; + } + + private takeDial(id: number): PendingDial { + const dial = this.dials.get(id); + if (!dial) throw new Error(`unknown dial ${id}`); + this.dials.delete(id); + + return dial; + } +} + +export class ScriptedClientTransport extends ClientTransport { + private readonly network: ScriptedNetwork; + + constructor( + clientId: TransportClientId, + network: ScriptedNetwork, + options?: ProvidedClientTransportOptions, + ) { + super(clientId, options); + this.network = network; + } + + protected createNewOutgoingConnection(): Promise { + return this.network.dial(); + } +} + +export class ScriptedServerTransport extends ServerTransport { + constructor( + clientId: TransportClientId, + network: ScriptedNetwork, + options?: ProvidedServerTransportOptions, + ) { + super(clientId, options); + network.acceptor = (conn) => { + this.handleConnection(conn); + }; + } + + /** Process death: handshakes in progress vanish along with everything else. */ + crash() { + for (const pending of Array.from(this.pendingSessions)) { + this.deletePendingSession(pending); + } + + this.close(); + } +} diff --git a/__tests__/conformance/projection.ts b/__tests__/conformance/projection.ts new file mode 100644 index 00000000..8e3bf515 --- /dev/null +++ b/__tests__/conformance/projection.ts @@ -0,0 +1,150 @@ +/** + * The comparable view of a protocol state. The model (spec/river.qnt) and the + * TypeScript implementation are each projected into this shape after every + * step of a trace, and the two projections must be equal. + */ + +export type Body = + | { kind: 'Heartbeat' } + | { kind: 'SInit'; sid: number; pt: ProcTag; close: boolean } + | { kind: 'SData'; sid: number; v: number } + | { kind: 'SResult'; sid: number; v: number; close: boolean } + | { kind: 'SClose'; sid: number } + | { kind: 'SCancel'; sid: number; code: string }; + +export type ProcTag = 'PRpc' | 'PStream' | 'PUpload' | 'PSubscription'; + +export interface Msg { + seq: number; + ack: number; + body: Body; +} + +export type Frame = + | { + kind: 'HsReq'; + sess: number; + nextExpectedSeq: number; + nextSentSeq: number; + } + | { kind: 'HsResp'; ok: boolean; sess: number; code: string } + | ({ kind: 'Data' } & Msg); + +export type Res = { ok: true; v: number } | { ok: false; code: string }; + +export interface SessionView { + sess: number; + state: string; + /** The dial a Connecting session waits on, or the connection otherwise. */ + on: number | null; + seq: number; + ack: number; + seqSent: number; + buf: Array; + grace: number | null; +} + +export interface ConnView { + toServer: Array; + toClient: Array; + closed: boolean; + clientEv: boolean; + serverEv: boolean; +} + +/** `null` marks a field the implementation does not expose for this procedure type. */ +export interface ClientStreamView { + w: boolean | null; + r: boolean | null; + results: Array | null; +} + +export interface ServerStreamView { + r: boolean | null; + w: boolean | null; + inMap: boolean; + /** Handler invocations for this stream id since the server started. */ + runs: number; + values: Array | null; +} + +export interface Projection { + now: number; + client: SessionView | null; + server: { + closed: boolean; + pending: Array; + session: SessionView | null; + tombstones: Array; + }; + conns: Record; + dials: Array; + cStreams: Record; + sStreams: Record; + cErrs: Array; + sErrs: Array; + cViolations: number; + sViolations: number; + timers: number; +} + +/** + * Hides from the model projection the stream fields the implementation cannot + * observe, so they don't count as differences. + */ +export function maskUnobservable(model: Projection, impl: Projection) { + for (const [sid, view] of Object.entries(impl.cStreams)) { + const modelView = model.cStreams[sid] as ClientStreamView | undefined; + if (!modelView) continue; + if (view.w === null) modelView.w = null; + if (view.r === null) modelView.r = null; + if (view.results === null) modelView.results = null; + } + + for (const [sid, view] of Object.entries(impl.sStreams)) { + const modelView = model.sStreams[sid] as ServerStreamView | undefined; + if (!modelView) continue; + if (view.r === null) modelView.r = null; + if (view.w === null) modelView.w = null; + if (view.values === null) modelView.values = null; + } +} + +export interface Difference { + path: string; + model: unknown; + impl: unknown; +} + +/** Every leaf where the two values differ, keyed by its path. */ +export function diff( + model: unknown, + impl: unknown, + path = '', +): Array { + if (Object.is(model, impl)) return []; + + const bothObjects = + typeof model === 'object' && + typeof impl === 'object' && + model !== null && + impl !== null && + Array.isArray(model) === Array.isArray(impl); + if (!bothObjects) return [{ path: path || '.', model, impl }]; + + if (Array.isArray(model) && Array.isArray(impl)) { + if (model.length !== impl.length) { + return [{ path: path || '.', model, impl }]; + } + + return model.flatMap((item, i) => diff(item, impl[i], `${path}[${i}]`)); + } + + const left = model as Record; + const right = impl as Record; + const keys = new Set([...Object.keys(left), ...Object.keys(right)]); + + return [...keys] + .sort() + .flatMap((key) => diff(left[key], right[key], `${path}.${key}`)); +} diff --git a/__tests__/conformance/quint.ts b/__tests__/conformance/quint.ts new file mode 100644 index 00000000..a111abd3 --- /dev/null +++ b/__tests__/conformance/quint.ts @@ -0,0 +1,178 @@ +import { execFileSync } from 'node:child_process'; +import { mkdtempSync, readdirSync, readFileSync, rmSync } from 'node:fs'; +import { tmpdir } from 'node:os'; +import path from 'node:path'; +import { fileURLToPath } from 'node:url'; +import { describeAction, parseTrace, type Trace } from './model'; + +const repoRoot = path.resolve( + path.dirname(fileURLToPath(import.meta.url)), + '..', + '..', +); + +export const SPEC = path.join(repoRoot, 'spec', 'river.qnt'); +export const SPEC_TESTS = path.join(repoRoot, 'spec', 'river_test.qnt'); + +const QUINT_CLI = path.join( + repoRoot, + 'node_modules', + '@informalsystems', + 'quint', + 'dist', + 'src', + 'cli.js', +); + +/** + * The TypeScript simulator needs nothing beyond node_modules; the faster Rust + * one downloads a binary on first use, so it is opt-in for long local hunts. + */ +const BACKEND = process.env.QUINT_BACKEND ?? 'typescript'; + +function quint(args: Array) { + try { + execFileSync(process.execPath, [QUINT_CLI, ...args, '--backend', BACKEND], { + cwd: repoRoot, + stdio: ['ignore', 'pipe', 'pipe'], + maxBuffer: 64 * 1024 * 1024, + }); + } catch (err) { + // quint prints the failing scenario or the invariant counterexample + const { stdout, stderr } = err as { stdout?: Buffer; stderr?: Buffer }; + throw new Error( + `quint ${args[0]} failed\n${String(stdout ?? '')}${String(stderr ?? '')}`, + ); + } +} + +function readTraces(dir: string, label: string): Array { + return readdirSync(dir) + .filter((file) => file.endsWith('.itf.json')) + .sort((a, b) => a.localeCompare(b, undefined, { numeric: true })) + .map((file) => + parseTrace( + `${label} ${file}`, + readFileSync(path.join(dir, file), 'utf8'), + ), + ); +} + +/** The command line that reruns a quint invocation, printing every state. */ +function reproduce(args: Array): string { + const shown = args.map((arg) => + path.isAbsolute(arg) ? path.relative(repoRoot, arg) : arg, + ); + + return `npx quint ${[...shown, '--backend', BACKEND, '--verbosity', '3'].join( + ' ', + )}`; +} + +/** + * Runs quint with ITF output in a fresh directory and parses the traces. On + * failure the directory is kept, and the error names it, lists the steps of + * the first trace (the counterexample or failing scenario), and gives the + * command that reproduces the run. + */ +function quintTraces(args: Array, label: string): Array { + const dir = mkdtempSync(path.join(tmpdir(), 'river-quint-')); + const itf = path.join( + dir, + label === 'scenario' ? '{test}_{seq}.itf.json' : 'trace_{seq}.itf.json', + ); + try { + quint([...args, '--verbosity', '1', '--out-itf', itf]); + } catch (err) { + const lines = [(err as Error).message.trimEnd()]; + try { + const traces = readTraces(dir, label); + if (traces.length > 0) { + const first = traces[0]; + lines.push( + `steps of ${first.name}:`, + ...first.steps + .slice(1) + .map((step, n) => ` ${n + 1}. ${describeAction(step.action)}`), + ); + } + } catch { + // quint may have stopped before writing a complete trace + } + + lines.push(`traces kept in ${dir}`, `reproduce: ${reproduce(args)}`); + throw new Error(lines.join('\n')); + } + + try { + return readTraces(dir, label); + } finally { + rmSync(dir, { recursive: true, force: true }); + } +} + +/** + * Random traces of the model's `step` relation, reproducible from the seed. + * The same run checks an invariant (`safety` by default) on every state. + */ +export function generateTraces(opts: { + seed: string; + count: number; + maxSteps: number; + invariant?: string; +}): Array { + return quintTraces( + [ + 'run', + SPEC, + '--max-samples', + String(opts.count), + '--n-traces', + String(opts.count), + '--max-steps', + String(opts.maxSteps), + '--seed', + opts.seed, + '--invariant', + opts.invariant ?? 'safety', + ], + `seed ${opts.seed} (max ${opts.maxSteps} steps)`, + ); +} + +/** Traces per quint run: quint holds all of a run's traces in memory. */ +const BATCH_SIZE = 100; + +/** + * `count` random traces in batches, so memory stays bounded however many are + * asked for. Batch i uses the seed plus i, which its traces' names show. + */ +export function* traceBatches(opts: { + seed: string; + count: number; + maxSteps: number; +}): Generator> { + const base = BigInt(opts.seed); + for (let i = 0; i * BATCH_SIZE < opts.count; i++) { + yield generateTraces({ + seed: `0x${(base + BigInt(i)).toString(16)}`, + count: Math.min(BATCH_SIZE, opts.count - i * BATCH_SIZE), + maxSteps: opts.maxSteps, + }); + } +} + +/** The fixed scenarios written as `run` definitions in spec/river_test.qnt. */ +export function scenarioTraces(match?: string): Array { + return quintTraces( + [ + 'test', + SPEC_TESTS, + ...(match ? ['--match', match] : []), + // scenarios are deterministic apart from the fault generator's seed + '--max-samples', + '1', + ], + 'scenario', + ); +} diff --git a/__tests__/conformance/replay.ts b/__tests__/conformance/replay.ts new file mode 100644 index 00000000..2f57e4e4 --- /dev/null +++ b/__tests__/conformance/replay.ts @@ -0,0 +1,152 @@ +import { vi } from 'vitest'; +import FakeTimers from '@sinonjs/fake-timers'; +import type { Codec } from '../../codec/types'; +import { Harness } from './harness'; +import { + describeAction, + projectModel, + type QAction, + type QState, + type Trace, +} from './model'; +import { diff, maskUnobservable, type Difference } from './projection'; + +/** + * A divergence the model has already found and the implementation still has. + * Replay stops just before the triggering action, so the remaining traces keep + * checking everything else until the bug is fixed and its entry removed. + */ +export interface KnownBug { + id: string; + summary: string; + /** The spec/river_test.qnt run that reproduces it. */ + scenario: string; + matches: (before: QState, action: QAction) => boolean; +} + +export type Outcome = + | { kind: 'ok'; steps: number } + | { kind: 'known-bug'; bug: KnownBug; step: number } + | { + kind: 'diverged'; + step: number; + action: string; + differences: Array; + history: Array; + } + | { + kind: 'error'; + step: number; + action: string; + error: unknown; + history: Array; + }; + +/** + * Replays a model trace against the implementation, comparing the two + * projections after the initial state and after every action. + */ +export async function replay( + trace: Trace, + knownBugs: ReadonlyArray = [], + codec?: Codec, +): Promise { + // a clock of our own rather than vitest's: its next() fires exactly one timer + vi.useRealTimers(); + const clock = FakeTimers.install({ + now: 0, + toFake: [ + 'setTimeout', + 'clearTimeout', + 'setInterval', + 'clearInterval', + 'Date', + ], + }); + + const rejections: Array = []; + const onRejection = (reason: unknown) => rejections.push(reason); + process.on('unhandledRejection', onRejection); + + const harness = new Harness(trace.steps[0].st.cfg, clock, codec); + const history: Array = []; + try { + for (const [i, { st, action }] of trace.steps.entries()) { + const described = describeAction(action); + if (i > 0) { + const before = trace.steps[i - 1].st; + const bug = knownBugs.find((b) => b.matches(before, action)); + if (bug) return { kind: 'known-bug', bug, step: i }; + + history.push(described); + try { + await harness.apply(action); + } catch (error) { + return { kind: 'error', step: i, action: described, error, history }; + } + + if (rejections.length > 0) { + return { + kind: 'error', + step: i, + action: described, + error: rejections[0], + history, + }; + } + } + + const model = projectModel(st); + const impl = harness.project(st); + maskUnobservable(model, impl); + const differences = diff(model, impl); + if (differences.length > 0) { + return { + kind: 'diverged', + step: i, + action: described, + differences, + history, + }; + } + } + + return { kind: 'ok', steps: trace.steps.length }; + } finally { + harness.dispose(); + process.off('unhandledRejection', onRejection); + clock.uninstall(); + } +} + +export function formatOutcome(trace: Trace, outcome: Outcome): string { + switch (outcome.kind) { + case 'ok': + return `${trace.name}: ok (${outcome.steps} states)`; + case 'known-bug': + return `${trace.name}: stopped at step ${outcome.step} on known bug ${outcome.bug.id}`; + case 'error': + return [ + `${trace.name}: implementation threw at step ${outcome.step} (${outcome.action})`, + ` ${String( + outcome.error instanceof Error ? outcome.error.stack : outcome.error, + )}`, + ' actions:', + ...outcome.history.map((a, i) => ` ${i + 1}. ${a}`), + ].join('\n'); + case 'diverged': + return [ + `${trace.name}: diverged from the model at step ${outcome.step} (${outcome.action})`, + ...outcome.differences + .slice(0, 25) + .map( + (d) => + ` ${d.path}\n model: ${JSON.stringify( + d.model, + )}\n impl: ${JSON.stringify(d.impl)}`, + ), + ' actions:', + ...outcome.history.map((a, i) => ` ${i + 1}. ${a}`), + ].join('\n'); + } +} diff --git a/package-lock.json b/package-lock.json index 57e67c48..61f3b5e7 100644 --- a/package-lock.json +++ b/package-lock.json @@ -17,10 +17,12 @@ "devDependencies": { "@bufbuild/buf": "^1.67.0", "@hegeldev/hegel": "^0.4.5", + "@informalsystems/quint": "^0.33.0", "@opentelemetry/api": "^1.7.0", "@opentelemetry/context-async-hooks": "^1.26.0", "@opentelemetry/core": "^1.7.0", "@opentelemetry/sdk-trace-base": "^1.24.1", + "@sinonjs/fake-timers": "^15.4.0", "@stylistic/eslint-plugin": "^2.6.4", "@types/ws": "^8.5.5", "@typescript-eslint/eslint-plugin": "^7.8.0", @@ -690,6 +692,58 @@ "node": "^12.22.0 || ^14.17.0 || >=16.0.0" } }, + "node_modules/@grpc/grpc-js": { + "version": "1.14.5", + "resolved": "https://registry.npmjs.org/@grpc/grpc-js/-/grpc-js-1.14.5.tgz", + "integrity": "sha512-7VZM+SVdEcUUqSQeNI3zM8Qs/BhQKZndPo2h5VkYkAM8Iz0wJIa8mKV5ekQGqG8UUsnkQ0NMxIxwkIHYvj0qOw==", + "dev": true, + "license": "Apache-2.0", + "dependencies": { + "@grpc/proto-loader": "^0.8.0", + "@js-sdsl/ordered-map": "^4.4.2" + }, + "engines": { + "node": ">=12.10.0" + } + }, + "node_modules/@grpc/grpc-js/node_modules/@grpc/proto-loader": { + "version": "0.8.1", + "resolved": "https://registry.npmjs.org/@grpc/proto-loader/-/proto-loader-0.8.1.tgz", + "integrity": "sha512-wtF6h+DY6M3YaDBPAmvuuA6jV8Sif9MjtOI5euKFWRgCDl5PeDpPsHR9u2l6St5ceY8AZgoNDww5+HvEsXFsGg==", + "dev": true, + "license": "Apache-2.0", + "dependencies": { + "lodash.camelcase": "^4.3.0", + "long": "^5.0.0", + "protobufjs": "^7.5.5", + "yargs": "^17.7.2" + }, + "bin": { + "proto-loader-gen-types": "build/bin/proto-loader-gen-types.js" + }, + "engines": { + "node": ">=6" + } + }, + "node_modules/@grpc/proto-loader": { + "version": "0.7.15", + "resolved": "https://registry.npmjs.org/@grpc/proto-loader/-/proto-loader-0.7.15.tgz", + "integrity": "sha512-tMXdRCfYVixjuFK+Hk0Q1s38gV9zDiDJfWL3h1rv4Qc39oILCu1TRTDt7+fGUI8K4G1Fj125Hx/ru3azECWTyQ==", + "dev": true, + "license": "Apache-2.0", + "dependencies": { + "lodash.camelcase": "^4.3.0", + "long": "^5.0.0", + "protobufjs": "^7.2.5", + "yargs": "^17.7.2" + }, + "bin": { + "proto-loader-gen-types": "build/bin/proto-loader-gen-types.js" + }, + "engines": { + "node": ">=6" + } + }, "node_modules/@hegeldev/hegel": { "version": "0.4.5", "resolved": "https://registry.npmjs.org/@hegeldev/hegel/-/hegel-0.4.5.tgz", @@ -822,6 +876,43 @@ "integrity": "sha512-6EwiSjwWYP7pTckG6I5eyFANjPhmPjUX9JRLUSfNPC7FX7zK9gyZAfUEaECL6ALTpGX5AjnBq3C9XmVWPitNpw==", "dev": true }, + "node_modules/@informalsystems/quint": { + "version": "0.33.0", + "resolved": "https://registry.npmjs.org/@informalsystems/quint/-/quint-0.33.0.tgz", + "integrity": "sha512-1hr+l+3wyKimjNXNl9lovpwmH5C9Ck898FL4yGbuEmFPiz7YRqvFvsB9hlHsaYukXqdUY5nuFKn/qiCon0O88g==", + "dev": true, + "license": "Apache 2.0", + "dependencies": { + "@grpc/grpc-js": "^1.11.1", + "@grpc/proto-loader": "^0.7.7", + "@octokit/request": "^8.1.1", + "@sweet-monads/either": "~3.2.0", + "@sweet-monads/maybe": "~3.2.0", + "@types/line-column": "^1.0.0", + "@types/lodash.clonedeep": "4.5.0", + "@types/seedrandom": "^3.0.4", + "adm-zip": "^0.5.16", + "antlr4ts": "^0.5.0-alpha.4", + "chalk": "^4.1.2", + "cli-progress": "^3.12.0", + "cross-spawn": "^7.0.6", + "eol": "^0.9.1", + "immutable": "^4.3.0", + "json-bigint": "^1.0.0", + "line-column": "^1.0.2", + "lodash": "^4.17.21", + "lodash.clonedeep": "4.5.0", + "seedrandom": "^3.0.5", + "tar": "^7.5.13", + "yargs": "^17.7.2" + }, + "bin": { + "quint": "dist/src/cli.js" + }, + "engines": { + "node": ">=18" + } + }, "node_modules/@isaacs/cliui": { "version": "8.0.2", "resolved": "https://registry.npmjs.org/@isaacs/cliui/-/cliui-8.0.2.tgz", @@ -869,6 +960,19 @@ "url": "https://github.com/chalk/strip-ansi?sponsor=1" } }, + "node_modules/@isaacs/fs-minipass": { + "version": "4.0.1", + "resolved": "https://registry.npmjs.org/@isaacs/fs-minipass/-/fs-minipass-4.0.1.tgz", + "integrity": "sha512-wgm9Ehl2jpeqP3zw/7mo3kRHFp5MEDhqAdwy1fTGkHAwnkGOVsgpvQhL8B5n1qlb01jV3n/bI0ZfZp5lWA1k4w==", + "dev": true, + "license": "ISC", + "dependencies": { + "minipass": "^7.0.4" + }, + "engines": { + "node": ">=18.0.0" + } + }, "node_modules/@jridgewell/gen-mapping": { "version": "0.3.8", "resolved": "https://registry.npmjs.org/@jridgewell/gen-mapping/-/gen-mapping-0.3.8.tgz", @@ -922,6 +1026,17 @@ "@jridgewell/sourcemap-codec": "^1.4.14" } }, + "node_modules/@js-sdsl/ordered-map": { + "version": "4.4.2", + "resolved": "https://registry.npmjs.org/@js-sdsl/ordered-map/-/ordered-map-4.4.2.tgz", + "integrity": "sha512-iUKgm52T8HOE/makSxjqoWhe95ZJA1/G1sYsGev2JDKUSS14KAgg1LHb+Ba+IPow0xflbnSkOsZcO08C7w1gYw==", + "dev": true, + "license": "MIT", + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/js-sdsl" + } + }, "node_modules/@koromix/koffi-darwin-arm64": { "version": "3.1.5", "resolved": "https://registry.npmjs.org/@koromix/koffi-darwin-arm64/-/koffi-darwin-arm64-3.1.5.tgz", @@ -1205,6 +1320,68 @@ "node": ">= 8" } }, + "node_modules/@octokit/endpoint": { + "version": "9.0.6", + "resolved": "https://registry.npmjs.org/@octokit/endpoint/-/endpoint-9.0.6.tgz", + "integrity": "sha512-H1fNTMA57HbkFESSt3Y9+FBICv+0jFceJFPWDePYlR/iMGrwM5ph+Dd4XRQs+8X+PUFURLQgX9ChPfhJ/1uNQw==", + "dev": true, + "license": "MIT", + "dependencies": { + "@octokit/types": "^13.1.0", + "universal-user-agent": "^6.0.0" + }, + "engines": { + "node": ">= 18" + } + }, + "node_modules/@octokit/openapi-types": { + "version": "24.2.0", + "resolved": "https://registry.npmjs.org/@octokit/openapi-types/-/openapi-types-24.2.0.tgz", + "integrity": "sha512-9sIH3nSUttelJSXUrmGzl7QUBFul0/mB8HRYl3fOlgHbIWG+WnYDXU3v/2zMtAvuzZ/ed00Ei6on975FhBfzrg==", + "dev": true, + "license": "MIT" + }, + "node_modules/@octokit/request": { + "version": "8.4.1", + "resolved": "https://registry.npmjs.org/@octokit/request/-/request-8.4.1.tgz", + "integrity": "sha512-qnB2+SY3hkCmBxZsR/MPCybNmbJe4KAlfWErXq+rBKkQJlbjdJeS85VI9r8UqeLYLvnAenU8Q1okM/0MBsAGXw==", + "dev": true, + "license": "MIT", + "dependencies": { + "@octokit/endpoint": "^9.0.6", + "@octokit/request-error": "^5.1.1", + "@octokit/types": "^13.1.0", + "universal-user-agent": "^6.0.0" + }, + "engines": { + "node": ">= 18" + } + }, + "node_modules/@octokit/request-error": { + "version": "5.1.1", + "resolved": "https://registry.npmjs.org/@octokit/request-error/-/request-error-5.1.1.tgz", + "integrity": "sha512-v9iyEQJH6ZntoENr9/yXxjuezh4My67CBSu9r6Ve/05Iu5gNgnisNWOsoJHTP6k0Rr0+HQIpnH+kyammu90q/g==", + "dev": true, + "license": "MIT", + "dependencies": { + "@octokit/types": "^13.1.0", + "deprecation": "^2.0.0", + "once": "^1.4.0" + }, + "engines": { + "node": ">= 18" + } + }, + "node_modules/@octokit/types": { + "version": "13.10.0", + "resolved": "https://registry.npmjs.org/@octokit/types/-/types-13.10.0.tgz", + "integrity": "sha512-ifLaO34EbbPj0Xgro4G5lP5asESjwHracYJvVaPIyXMuiuXLlhic3S47cBdTb+jfODkTE5YtGCLt3Ay3+J97sA==", + "dev": true, + "license": "MIT", + "dependencies": { + "@octokit/openapi-types": "^24.2.0" + } + }, "node_modules/@opentelemetry/api": { "version": "1.8.0", "resolved": "https://registry.npmjs.org/@opentelemetry/api/-/api-1.8.0.tgz", @@ -1313,6 +1490,72 @@ "dev": true, "license": "MIT" }, + "node_modules/@protobufjs/aspromise": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/aspromise/-/aspromise-1.1.2.tgz", + "integrity": "sha512-j+gKExEuLmKwvz3OgROXtrJ2UG2x8Ch2YZUxahh+s1F2HZ+wAceUNLkvy6zKCPVRkU++ZWQrdxsUeQXmcg4uoQ==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/base64": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/base64/-/base64-1.1.2.tgz", + "integrity": "sha512-AZkcAA5vnN/v4PDqKyMR5lx7hZttPDgClv83E//FMNhR2TMcLUhfRUBHCmSl0oi9zMgDDqRUJkSxO3wm85+XLg==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/codegen": { + "version": "2.0.5", + "resolved": "https://registry.npmjs.org/@protobufjs/codegen/-/codegen-2.0.5.tgz", + "integrity": "sha512-zgXFLzW3Ap33e6d0Wlj4MGIm6Ce8O89n/apUaGNB/jx+hw+ruWEp7EwGUshdLKVRCxZW12fp9r40E1mQrf/34g==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/eventemitter": { + "version": "1.1.1", + "resolved": "https://registry.npmjs.org/@protobufjs/eventemitter/-/eventemitter-1.1.1.tgz", + "integrity": "sha512-vW1GmwMZNnL+gMRaovlh9yZX74kc+TTU3FObkkurpMaRtBfLP3ldjS9KQWlwZgraRE0+dheEEoAxdzcJQ8eXZg==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/fetch": { + "version": "1.1.1", + "resolved": "https://registry.npmjs.org/@protobufjs/fetch/-/fetch-1.1.1.tgz", + "integrity": "sha512-GpptLrs57adMSuHi3VNj0mAF8dwh36LMaYF6XyJ6JMWlVsc+t42tm1HSEDmOs3A8fC9yyeisgLhsTVQokOZ0zw==", + "dev": true, + "license": "BSD-3-Clause", + "dependencies": { + "@protobufjs/aspromise": "^1.1.1" + } + }, + "node_modules/@protobufjs/float": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/@protobufjs/float/-/float-1.0.2.tgz", + "integrity": "sha512-Ddb+kVXlXst9d+R9PfTIxh1EdNkgoRe5tOX6t01f1lYWOvJnSPDBlG241QLzcyPdoNTsblLUdujGSE4RzrTZGQ==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/path": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/path/-/path-1.1.2.tgz", + "integrity": "sha512-6JOcJ5Tm08dOHAbdR3GrvP+yUUfkjG5ePsHYczMFLq3ZmMkAD98cDgcT2iA1lJ9NVwFd4tH/iSSoe44YWkltEA==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/pool": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/@protobufjs/pool/-/pool-1.1.0.tgz", + "integrity": "sha512-0kELaGSIDBKvcgS4zkjz1PeddatrjYcmMWOlAuAPwAeccUrPHdUqo/J6LiymHHEiJT5NrF1UVwxY14f+fy4WQw==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/utf8": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/utf8/-/utf8-1.1.2.tgz", + "integrity": "sha512-b1UQwcEZ4yCnMCD8DAL1VlbvBJE9/IX4FTIp7BG1xYpf29SLazLSrqUkj4w7Y5y7cCVP6E5tcqqcI0xemPkHug==", + "dev": true, + "license": "BSD-3-Clause" + }, "node_modules/@rollup/rollup-android-arm-eabi": { "version": "4.59.0", "resolved": "https://registry.npmjs.org/@rollup/rollup-android-arm-eabi/-/rollup-android-arm-eabi-4.59.0.tgz", @@ -1638,6 +1881,26 @@ "win32" ] }, + "node_modules/@sinonjs/commons": { + "version": "3.0.1", + "resolved": "https://registry.npmjs.org/@sinonjs/commons/-/commons-3.0.1.tgz", + "integrity": "sha512-K3mCHKQ9sVh8o1C9cxkwxaOmXoAMlDxC1mYyHrjqOWEcBjYr76t96zL2zlj5dUGZ3HSw240X1qgH3Mjf1yJWpQ==", + "dev": true, + "license": "BSD-3-Clause", + "dependencies": { + "type-detect": "4.0.8" + } + }, + "node_modules/@sinonjs/fake-timers": { + "version": "15.4.0", + "resolved": "https://registry.npmjs.org/@sinonjs/fake-timers/-/fake-timers-15.4.0.tgz", + "integrity": "sha512-DsG+8/LscQIQg68J6Ef3dv10u6nVyetYn923s3/sus5eaGfTo1of5WMZSLf0UJc9KDuKPilPH0UDJCjvNbDNCA==", + "dev": true, + "license": "BSD-3-Clause", + "dependencies": { + "@sinonjs/commons": "^3.0.1" + } + }, "node_modules/@stylistic/eslint-plugin": { "version": "2.6.4", "resolved": "https://registry.npmjs.org/@stylistic/eslint-plugin/-/eslint-plugin-2.6.4.tgz", @@ -1915,6 +2178,33 @@ "url": "https://github.com/sponsors/isaacs" } }, + "node_modules/@sweet-monads/either": { + "version": "3.2.0", + "resolved": "https://registry.npmjs.org/@sweet-monads/either/-/either-3.2.0.tgz", + "integrity": "sha512-n+nR0b60GRTKb+D76qhTf4NEBXU9zfpigYYEtKtSYbV+5+i5gxr9jFd64pYkY2O7hVsb/G7nspbAeFni/i1ltA==", + "dev": true, + "license": "MIT", + "dependencies": { + "@sweet-monads/interfaces": "^3.2.0" + } + }, + "node_modules/@sweet-monads/interfaces": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@sweet-monads/interfaces/-/interfaces-3.3.0.tgz", + "integrity": "sha512-66akGvjPD4lizQy+w4JSltJilc2w/QPdw8lPAniLJGHwyjmrw9xMJLx76Q/GDnbCU59Werses4aZJLWOlJrL5A==", + "dev": true, + "license": "MIT" + }, + "node_modules/@sweet-monads/maybe": { + "version": "3.2.0", + "resolved": "https://registry.npmjs.org/@sweet-monads/maybe/-/maybe-3.2.0.tgz", + "integrity": "sha512-/t+K0D/kBfkYOkZaePEsrK868at0M9UIEVgehcM0xscrCSZhKWGteE41vl2XJQqh8WyiFo/mZ5y7eAPSYzS+pg==", + "dev": true, + "license": "MIT", + "dependencies": { + "@sweet-monads/interfaces": "^3.2.0" + } + }, "node_modules/@types/chai": { "version": "5.2.3", "resolved": "https://registry.npmjs.org/@types/chai/-/chai-5.2.3.tgz", @@ -1953,12 +2243,43 @@ "integrity": "sha512-5+fP8P8MFNC+AyZCDxrB2pkZFPGzqQWUzpSeuuVLvm8VMcorNYavBqoFcxK8bQz4Qsbn4oUEEem4wDLfcysGHA==", "dev": true }, + "node_modules/@types/line-column": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/@types/line-column/-/line-column-1.0.2.tgz", + "integrity": "sha512-099oFQmp/Tlf20xW5XI5R4F69N6lF/zQ09XDzc3R5BOLFlqIotgKoNIyj0HD4fQLWcGDreDJv8k/BkLJscrDrw==", + "dev": true, + "license": "MIT" + }, + "node_modules/@types/lodash": { + "version": "4.17.25", + "resolved": "https://registry.npmjs.org/@types/lodash/-/lodash-4.17.25.tgz", + "integrity": "sha512-+K1NIO8I+F9/wNulfVvu23QYd0Pe9/OCqRrim4NoYIf1VoEDL90Ve4ClzpyqBLc7NpGGWRvYNCKZ1BE/Jpf8dQ==", + "dev": true, + "license": "MIT" + }, + "node_modules/@types/lodash.clonedeep": { + "version": "4.5.0", + "resolved": "https://registry.npmjs.org/@types/lodash.clonedeep/-/lodash.clonedeep-4.5.0.tgz", + "integrity": "sha512-IHijjFVPJTvzvrNPz+6nQy5lZQb7uh807RfTIEaQBrZXrIGjZy0L2dEb3hju34J0eqbXLCY6Hub/g81Jl4pGCA==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/lodash": "*" + } + }, "node_modules/@types/node": { "version": "20.5.7", "resolved": "https://registry.npmjs.org/@types/node/-/node-20.5.7.tgz", "integrity": "sha512-dP7f3LdZIysZnmvP3ANJYTSwg+wLLl8p7RqniVlV7j+oXSXAbt9h0WIBFmJy5inWZoX9wZN6eXx+YXd9Rh3RBA==", "dev": true }, + "node_modules/@types/seedrandom": { + "version": "3.0.8", + "resolved": "https://registry.npmjs.org/@types/seedrandom/-/seedrandom-3.0.8.tgz", + "integrity": "sha512-TY1eezMU2zH2ozQoAFAQFOPpvP15g+ZgSfTZt31AUUH/Rxtnz3H+A/Sv1Snw2/amp//omibc+AEkTaA8KUeOLQ==", + "dev": true, + "license": "MIT" + }, "node_modules/@types/ws": { "version": "8.5.5", "resolved": "https://registry.npmjs.org/@types/ws/-/ws-8.5.5.tgz", @@ -2333,6 +2654,16 @@ "acorn": "^6.0.0 || ^7.0.0 || ^8.0.0" } }, + "node_modules/adm-zip": { + "version": "0.6.1", + "resolved": "https://registry.npmjs.org/adm-zip/-/adm-zip-0.6.1.tgz", + "integrity": "sha512-Xwrja8nx9e5o2N1my4DsKCeKpdrnACyr1wtbPxBDgGzKzKyE9kRtBFA8mWldI+RVlD7CBZNWY/wQ2+ydwOR6kQ==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=14.0" + } + }, "node_modules/ajv": { "version": "6.12.6", "resolved": "https://registry.npmjs.org/ajv/-/ajv-6.12.6.tgz", @@ -2371,6 +2702,13 @@ "url": "https://github.com/chalk/ansi-styles?sponsor=1" } }, + "node_modules/antlr4ts": { + "version": "0.5.0-alpha.4", + "resolved": "https://registry.npmjs.org/antlr4ts/-/antlr4ts-0.5.0-alpha.4.tgz", + "integrity": "sha512-WPQDt1B74OfPv/IMS2ekXAKkTZIHl88uMetg6q3OTqgFxZ/dxDXI0EWLyZid/1Pe6hTftyg5N7gel5wNAGxXyQ==", + "dev": true, + "license": "BSD-3-Clause" + }, "node_modules/any-promise": { "version": "1.3.0", "resolved": "https://registry.npmjs.org/any-promise/-/any-promise-1.3.0.tgz", @@ -2408,6 +2746,16 @@ "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw==", "dev": true }, + "node_modules/bignumber.js": { + "version": "9.3.1", + "resolved": "https://registry.npmjs.org/bignumber.js/-/bignumber.js-9.3.1.tgz", + "integrity": "sha512-Ko0uX15oIUS7wJ3Rb30Fs6SkVbLmPBAKdlm7q9+ak9bbIeFf0MwuBsQV6z7+X768/cHsfg+WlysDWJcmthjsjQ==", + "dev": true, + "license": "MIT", + "engines": { + "node": "*" + } + }, "node_modules/brace-expansion": { "version": "1.1.18", "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.18.tgz", @@ -2536,6 +2884,122 @@ "url": "https://paulmillr.com/funding/" } }, + "node_modules/chownr": { + "version": "3.0.0", + "resolved": "https://registry.npmjs.org/chownr/-/chownr-3.0.0.tgz", + "integrity": "sha512-+IxzY9BZOQd/XuYPRmrvEVjF/nqj5kgT4kEq7VofrDoM1MxoRjEWkrCC3EtLi59TVawxTAn+orJwFQcrqEN1+g==", + "dev": true, + "license": "BlueOak-1.0.0", + "engines": { + "node": ">=18" + } + }, + "node_modules/cli-progress": { + "version": "3.12.0", + "resolved": "https://registry.npmjs.org/cli-progress/-/cli-progress-3.12.0.tgz", + "integrity": "sha512-tRkV3HJ1ASwm19THiiLIXLO7Im7wlTuKnvkYaTkyoAPefqjNg7W7DHKUlGRxy9vxDvbyCYQkQozvptuMkGCg8A==", + "dev": true, + "license": "MIT", + "dependencies": { + "string-width": "^4.2.3" + }, + "engines": { + "node": ">=4" + } + }, + "node_modules/cli-progress/node_modules/emoji-regex": { + "version": "8.0.0", + "resolved": "https://registry.npmjs.org/emoji-regex/-/emoji-regex-8.0.0.tgz", + "integrity": "sha512-MSjYzcWNOA0ewAHpz0MxpYFvwg6yjy1NG3xteoqz644VCo/RPgnr1/GGt+ic3iJTzQ8Eu3TdM14SawnVUmGE6A==", + "dev": true, + "license": "MIT" + }, + "node_modules/cli-progress/node_modules/string-width": { + "version": "4.2.3", + "resolved": "https://registry.npmjs.org/string-width/-/string-width-4.2.3.tgz", + "integrity": "sha512-wKyQRQpjJ0sIp62ErSZdGsjMJWsap5oRNihHhu6G7JVO/9jIB6UyevL+tXuOqrng8j/cxKTWyWUwvSTriiZz/g==", + "dev": true, + "license": "MIT", + "dependencies": { + "emoji-regex": "^8.0.0", + "is-fullwidth-code-point": "^3.0.0", + "strip-ansi": "^6.0.1" + }, + "engines": { + "node": ">=8" + } + }, + "node_modules/cliui": { + "version": "8.0.1", + "resolved": "https://registry.npmjs.org/cliui/-/cliui-8.0.1.tgz", + "integrity": "sha512-BSeNnyus75C4//NQ9gQt1/csTXyo/8Sb+afLAkzAptFuMsod9HFokGNudZpi/oQV73hnVK+sR+5PVRMd+Dr7YQ==", + "dev": true, + "license": "ISC", + "dependencies": { + "string-width": "^4.2.0", + "strip-ansi": "^6.0.1", + "wrap-ansi": "^7.0.0" + }, + "engines": { + "node": ">=12" + } + }, + "node_modules/cliui/node_modules/ansi-styles": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz", + "integrity": "sha512-zbB9rCJAT1rbjiVDb2hqKFHNYLxgtk8NURxZ3IZwD3F6NtxbXZQCnnSi1Lkx+IDohdPlFp222wVALIheZJQSEg==", + "dev": true, + "license": "MIT", + "dependencies": { + "color-convert": "^2.0.1" + }, + "engines": { + "node": ">=8" + }, + "funding": { + "url": "https://github.com/chalk/ansi-styles?sponsor=1" + } + }, + "node_modules/cliui/node_modules/emoji-regex": { + "version": "8.0.0", + "resolved": "https://registry.npmjs.org/emoji-regex/-/emoji-regex-8.0.0.tgz", + "integrity": "sha512-MSjYzcWNOA0ewAHpz0MxpYFvwg6yjy1NG3xteoqz644VCo/RPgnr1/GGt+ic3iJTzQ8Eu3TdM14SawnVUmGE6A==", + "dev": true, + "license": "MIT" + }, + "node_modules/cliui/node_modules/string-width": { + "version": "4.2.3", + "resolved": "https://registry.npmjs.org/string-width/-/string-width-4.2.3.tgz", + "integrity": "sha512-wKyQRQpjJ0sIp62ErSZdGsjMJWsap5oRNihHhu6G7JVO/9jIB6UyevL+tXuOqrng8j/cxKTWyWUwvSTriiZz/g==", + "dev": true, + "license": "MIT", + "dependencies": { + "emoji-regex": "^8.0.0", + "is-fullwidth-code-point": "^3.0.0", + "strip-ansi": "^6.0.1" + }, + "engines": { + "node": ">=8" + } + }, + "node_modules/cliui/node_modules/wrap-ansi": { + "version": "7.0.0", + "resolved": "https://registry.npmjs.org/wrap-ansi/-/wrap-ansi-7.0.0.tgz", + "integrity": "sha512-YVGIj2kamLSTxw6NsZjoBxfSwsn0ycdesmc4p+Q21c5zPuZ1pl+NfxVdxPtdHvmNVOQ6XSYG4AUtyt/Fi7D16Q==", + "dev": true, + "license": "MIT", + "dependencies": { + "ansi-styles": "^4.0.0", + "string-width": "^4.1.0", + "strip-ansi": "^6.0.0" + }, + "engines": { + "node": ">=10" + }, + "funding": { + "url": "https://github.com/chalk/wrap-ansi?sponsor=1" + } + }, "node_modules/color-convert": { "version": "2.0.1", "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz", @@ -2633,6 +3097,13 @@ "integrity": "sha512-oIPzksmTg4/MriiaYGO+okXDT7ztn/w3Eptv/+gSIdMdKsJo0u4CfYNFJPy+4SKMuCqGw2wxnA+URMg3t8a/bQ==", "dev": true }, + "node_modules/deprecation": { + "version": "2.3.1", + "resolved": "https://registry.npmjs.org/deprecation/-/deprecation-2.3.1.tgz", + "integrity": "sha512-xmHIy4F3scKVwMsQ4WnVaS8bHOx0DmVwRywosKhaILI0ywMDWPtBSku2HNxRvF7jtwDRsoEwYQSfbxj8b7RlJQ==", + "dev": true, + "license": "ISC" + }, "node_modules/dir-glob": { "version": "3.0.1", "resolved": "https://registry.npmjs.org/dir-glob/-/dir-glob-3.0.1.tgz", @@ -2671,6 +3142,13 @@ "dev": true, "license": "MIT" }, + "node_modules/eol": { + "version": "0.9.1", + "resolved": "https://registry.npmjs.org/eol/-/eol-0.9.1.tgz", + "integrity": "sha512-Ds/TEoZjwggRoz/Q2O7SE3i4Jm66mqTDfmdHdq/7DKVk3bro9Q8h6WdXKdPqFLMoqxrDK5SVRzHVPOS6uuGtrg==", + "dev": true, + "license": "MIT" + }, "node_modules/es-module-lexer": { "version": "1.7.0", "resolved": "https://registry.npmjs.org/es-module-lexer/-/es-module-lexer-1.7.0.tgz", @@ -2718,6 +3196,16 @@ "@esbuild/win32-x64": "0.25.1" } }, + "node_modules/escalade": { + "version": "3.2.0", + "resolved": "https://registry.npmjs.org/escalade/-/escalade-3.2.0.tgz", + "integrity": "sha512-WUj2qlxaQtO4g6Pq5c29GTcWGDyd8itL8zTlipgECz3JesAiiOKotd8JU6otB3PACgG6xkJUyVhboMS+bje/jA==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=6" + } + }, "node_modules/escape-string-regexp": { "version": "4.0.0", "resolved": "https://registry.npmjs.org/escape-string-regexp/-/escape-string-regexp-4.0.0.tgz", @@ -3108,6 +3596,16 @@ "node": "^8.16.0 || ^10.6.0 || >=11.0.0" } }, + "node_modules/get-caller-file": { + "version": "2.0.5", + "resolved": "https://registry.npmjs.org/get-caller-file/-/get-caller-file-2.0.5.tgz", + "integrity": "sha512-DyFP3BM/3YHTQOCUL/w0OZHR0lpKeGrxotcHWcqNEdnltqFwXVfhEBQ94eIo34AfQpo0rGki4cyIiftY06h2Fg==", + "dev": true, + "license": "ISC", + "engines": { + "node": "6.* || 8.* || >= 10.*" + } + }, "node_modules/glob": { "version": "7.1.6", "resolved": "https://registry.npmjs.org/glob/-/glob-7.1.6.tgz", @@ -3199,6 +3697,13 @@ "node": ">= 4" } }, + "node_modules/immutable": { + "version": "4.3.9", + "resolved": "https://registry.npmjs.org/immutable/-/immutable-4.3.9.tgz", + "integrity": "sha512-ObHy4YN7ycwZOUCLI1/6svfyAFu7vL8RhAvVu/bh/RZW9EPlOyDaQ9jDQWCtdqzaXUjgXZCW1migtHE7YI7UGQ==", + "dev": true, + "license": "MIT" + }, "node_modules/import-fresh": { "version": "3.3.0", "resolved": "https://registry.npmjs.org/import-fresh/-/import-fresh-3.3.0.tgz", @@ -3298,12 +3803,32 @@ "node": ">=8" } }, + "node_modules/isarray": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/isarray/-/isarray-1.0.0.tgz", + "integrity": "sha512-VLghIWNM6ELQzo7zwmcg0NmTVyWKYjvIeM83yjp0wRDTmUnrM678fQbcKBo6n2CJEF0szoG//ytg+TKla89ALQ==", + "dev": true, + "license": "MIT" + }, "node_modules/isexe": { "version": "2.0.0", "resolved": "https://registry.npmjs.org/isexe/-/isexe-2.0.0.tgz", "integrity": "sha512-RHxMLp9lnKHGHRng9QFhRCMbYAcVpn69smSGcq3f36xjgVVWThj4qqLbTLlq7Ssj8B+fIQ1EuCEGI2lKsyQeIw==", "dev": true }, + "node_modules/isobject": { + "version": "2.1.0", + "resolved": "https://registry.npmjs.org/isobject/-/isobject-2.1.0.tgz", + "integrity": "sha512-+OUdGJlgjOBZDfxnDjYYG6zp487z0JGNQq3cYQYg5f5hKR+syHMsaztzGeml/4kGG55CSpKSpWTY+jYGgsHLgA==", + "dev": true, + "license": "MIT", + "dependencies": { + "isarray": "1.0.0" + }, + "engines": { + "node": ">=0.10.0" + } + }, "node_modules/jackspeak": { "version": "3.4.3", "resolved": "https://registry.npmjs.org/jackspeak/-/jackspeak-3.4.3.tgz", @@ -3358,6 +3883,16 @@ "js-yaml": "bin/js-yaml.js" } }, + "node_modules/json-bigint": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/json-bigint/-/json-bigint-1.0.0.tgz", + "integrity": "sha512-SiPv/8VpZuWbvLSMtTDU8hEfrZWg/mH/nV/b4o0CYbSxu1UIQPLdwKOCIyLQX+VIPO5vrLX3i8qtqFyhdPSUSQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "bignumber.js": "^9.0.0" + } + }, "node_modules/json-buffer": { "version": "3.0.1", "resolved": "https://registry.npmjs.org/json-buffer/-/json-buffer-3.0.1.tgz", @@ -3438,6 +3973,17 @@ "url": "https://github.com/sponsors/antonk52" } }, + "node_modules/line-column": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/line-column/-/line-column-1.0.2.tgz", + "integrity": "sha512-Ktrjk5noGYlHsVnYWh62FLVs4hTb8A3e+vucNZMgPeAOITdshMSgv4cCZQeRDjm7+goqmo6+liZwTXo+U3sVww==", + "dev": true, + "license": "MIT", + "dependencies": { + "isarray": "^1.0.0", + "isobject": "^2.0.0" + } + }, "node_modules/lines-and-columns": { "version": "1.2.4", "resolved": "https://registry.npmjs.org/lines-and-columns/-/lines-and-columns-1.2.4.tgz", @@ -3470,12 +4016,40 @@ "url": "https://github.com/sponsors/sindresorhus" } }, + "node_modules/lodash": { + "version": "4.18.1", + "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.18.1.tgz", + "integrity": "sha512-dMInicTPVE8d1e5otfwmmjlxkZoUpiVLwyeTdUsi/Caj/gfzzblBcCE5sRHV/AsjuCmxWrte2TNGSYuCeCq+0Q==", + "dev": true, + "license": "MIT" + }, + "node_modules/lodash.camelcase": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/lodash.camelcase/-/lodash.camelcase-4.3.0.tgz", + "integrity": "sha512-TwuEnCnxbc3rAvhf/LbG7tJUDzhqXyFnv3dtzLOPgCG/hODL7WFnsbwktkD7yUV0RrreP/l1PALq/YSg6VvjlA==", + "dev": true, + "license": "MIT" + }, + "node_modules/lodash.clonedeep": { + "version": "4.5.0", + "resolved": "https://registry.npmjs.org/lodash.clonedeep/-/lodash.clonedeep-4.5.0.tgz", + "integrity": "sha512-H5ZhCF25riFd9uB5UCkVKo61m3S/xZk1x4wA6yp/L3RFP6Z/eHH1ymQcGLo7J3GMPfm0V/7m1tryHuGVxpqEBQ==", + "dev": true, + "license": "MIT" + }, "node_modules/lodash.merge": { "version": "4.6.2", "resolved": "https://registry.npmjs.org/lodash.merge/-/lodash.merge-4.6.2.tgz", "integrity": "sha512-0KpjqXRVvrYyCsX1swR/XTK0va6VQkQM6MNo7PqW77ByjAhoARA8EfrP1N4+KlKj8YS0ZUCtRT/YUuhyYDujIQ==", "dev": true }, + "node_modules/long": { + "version": "5.3.2", + "resolved": "https://registry.npmjs.org/long/-/long-5.3.2.tgz", + "integrity": "sha512-mNAgZ1GmyNhD7AuqnTG3/VQ26o760+ZYBPKjPvugO8+nLbYfX6TVpJPseBvopbdY+qpZ/lKUnmEc1LeZYS3QAA==", + "dev": true, + "license": "Apache-2.0" + }, "node_modules/loupe": { "version": "3.2.1", "resolved": "https://registry.npmjs.org/loupe/-/loupe-3.2.1.tgz", @@ -3542,6 +4116,19 @@ "node": ">=16 || 14 >=14.17" } }, + "node_modules/minizlib": { + "version": "3.1.0", + "resolved": "https://registry.npmjs.org/minizlib/-/minizlib-3.1.0.tgz", + "integrity": "sha512-KZxYo1BUkWD2TVFLr0MQoM8vUUigWD3LlD83a/75BqC+4qE0Hb1Vo5v1FgcfaNXvfXzr+5EhQ6ing/CaBijTlw==", + "dev": true, + "license": "MIT", + "dependencies": { + "minipass": "^7.1.2" + }, + "engines": { + "node": ">= 18" + } + }, "node_modules/mlly": { "version": "1.8.0", "resolved": "https://registry.npmjs.org/mlly/-/mlly-1.8.0.tgz", @@ -3939,6 +4526,30 @@ "node": ">=6.0.0" } }, + "node_modules/protobufjs": { + "version": "7.6.6", + "resolved": "https://registry.npmjs.org/protobufjs/-/protobufjs-7.6.6.tgz", + "integrity": "sha512-dYDWdjSl5RNb7SgPxGQcRU+GtvP7s2fpkrY0r432PcOIaZ0/rBcxEZnQN67iJhFuQiVw754JDoPruPCNdGsbjg==", + "dev": true, + "hasInstallScript": true, + "license": "BSD-3-Clause", + "dependencies": { + "@protobufjs/aspromise": "^1.1.2", + "@protobufjs/base64": "^1.1.2", + "@protobufjs/codegen": "^2.0.5", + "@protobufjs/eventemitter": "^1.1.1", + "@protobufjs/fetch": "^1.1.1", + "@protobufjs/float": "^1.0.2", + "@protobufjs/path": "^1.1.2", + "@protobufjs/pool": "^1.1.0", + "@protobufjs/utf8": "^1.1.1", + "@types/node": ">=13.7.0", + "long": "^5.3.2" + }, + "engines": { + "node": ">=12.0.0" + } + }, "node_modules/punycode": { "version": "2.3.0", "resolved": "https://registry.npmjs.org/punycode/-/punycode-2.3.0.tgz", @@ -3982,6 +4593,16 @@ "url": "https://paulmillr.com/funding/" } }, + "node_modules/require-directory": { + "version": "2.1.1", + "resolved": "https://registry.npmjs.org/require-directory/-/require-directory-2.1.1.tgz", + "integrity": "sha512-fGxEI7+wsG9xrvdjsrlmL22OMTTiHRwAMroiEeMgq8gzoLC/PQr7RsRDSTLUg/bZAZtF+TVIkHc6/4RIKrui+Q==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=0.10.0" + } + }, "node_modules/resolve-from": { "version": "5.0.0", "resolved": "https://registry.npmjs.org/resolve-from/-/resolve-from-5.0.0.tgz", @@ -4083,6 +4704,13 @@ "queue-microtask": "^1.2.2" } }, + "node_modules/seedrandom": { + "version": "3.0.5", + "resolved": "https://registry.npmjs.org/seedrandom/-/seedrandom-3.0.5.tgz", + "integrity": "sha512-8OwmbklUNzwezjGInmZ+2clQmExQPvomqjL7LFqOYqtmuxRgQYqOD3mHaU+MvZn5FLUeVxVfQjwLZW/n/JFuqg==", + "dev": true, + "license": "MIT" + }, "node_modules/semver": { "version": "7.6.2", "resolved": "https://registry.npmjs.org/semver/-/semver-7.6.2.tgz", @@ -4407,6 +5035,23 @@ "url": "https://opencollective.com/unts" } }, + "node_modules/tar": { + "version": "7.5.22", + "resolved": "https://registry.npmjs.org/tar/-/tar-7.5.22.tgz", + "integrity": "sha512-MFO/QzvtAOmJbkhOaCTvbGcFN9L9b+JunIsDwaKljSOdcLMea3NJ1k9Usz/rjdfSXTq4dfzfeS7W4p4YOAAHeA==", + "dev": true, + "license": "BlueOak-1.0.0", + "dependencies": { + "@isaacs/fs-minipass": "^4.0.0", + "chownr": "^3.0.0", + "minipass": "^7.1.2", + "minizlib": "^3.1.0", + "yallist": "^5.0.0" + }, + "engines": { + "node": ">=18" + } + }, "node_modules/text-table": { "version": "0.2.0", "resolved": "https://registry.npmjs.org/text-table/-/text-table-0.2.0.tgz", @@ -5084,6 +5729,16 @@ "node": ">= 0.8.0" } }, + "node_modules/type-detect": { + "version": "4.0.8", + "resolved": "https://registry.npmjs.org/type-detect/-/type-detect-4.0.8.tgz", + "integrity": "sha512-0fr/mIH1dlO+x7TlcMy+bIDqKPsw/70tVyeHW787goQjhmqaZe10uwLujubK9q9Lg6Fiho1KUKDYz0Z7k7g5/g==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=4" + } + }, "node_modules/type-fest": { "version": "0.20.2", "resolved": "https://registry.npmjs.org/type-fest/-/type-fest-0.20.2.tgz", @@ -5122,6 +5777,13 @@ "integrity": "sha512-9a4/uxlTWJ4+a5i0ooc1rU7C7YOw3wT+UGqdeNNHWnOF9qcMBgLRS+4IYUqbczewFx4mLEig6gawh7X6mFlEkA==", "dev": true }, + "node_modules/universal-user-agent": { + "version": "6.0.1", + "resolved": "https://registry.npmjs.org/universal-user-agent/-/universal-user-agent-6.0.1.tgz", + "integrity": "sha512-yCzhz6FN2wU1NiiQRogkTQszlQSlpWaw8SvVegAc+bDxbzHgh1vX8uIe8OYyMH6DwH+sdTJsgMl36+mSMdRJIQ==", + "dev": true, + "license": "ISC" + }, "node_modules/uri-js": { "version": "4.4.1", "resolved": "https://registry.npmjs.org/uri-js/-/uri-js-4.4.1.tgz", @@ -5501,6 +6163,77 @@ "optional": true } } + }, + "node_modules/y18n": { + "version": "5.0.8", + "resolved": "https://registry.npmjs.org/y18n/-/y18n-5.0.8.tgz", + "integrity": "sha512-0pfFzegeDWJHJIAmTLRP2DwHjdF5s7jo9tuztdQxAhINCdvS+3nGINqPd00AphqJR/0LhANUS6/+7SCb98YOfA==", + "dev": true, + "license": "ISC", + "engines": { + "node": ">=10" + } + }, + "node_modules/yallist": { + "version": "5.0.0", + "resolved": "https://registry.npmjs.org/yallist/-/yallist-5.0.0.tgz", + "integrity": "sha512-YgvUTfwqyc7UXVMrB+SImsVYSmTS8X/tSrtdNZMImM+n7+QTriRXyXim0mBrTXNeqzVF0KWGgHPeiyViFFrNDw==", + "dev": true, + "license": "BlueOak-1.0.0", + "engines": { + "node": ">=18" + } + }, + "node_modules/yargs": { + "version": "17.7.3", + "resolved": "https://registry.npmjs.org/yargs/-/yargs-17.7.3.tgz", + "integrity": "sha512-GZtjxm/J/4TSxuL3FNYjCmLktBTnIw/rVmKSIyKeYAZpmJB2ig9VauCC5xsa82GNKVKDAqpOn3KVzNt0zmrU0g==", + "dev": true, + "license": "MIT", + "dependencies": { + "cliui": "^8.0.1", + "escalade": "^3.1.1", + "get-caller-file": "^2.0.5", + "require-directory": "^2.1.1", + "string-width": "^4.2.3", + "y18n": "^5.0.5", + "yargs-parser": "^21.1.1" + }, + "engines": { + "node": ">=12" + } + }, + "node_modules/yargs-parser": { + "version": "21.1.1", + "resolved": "https://registry.npmjs.org/yargs-parser/-/yargs-parser-21.1.1.tgz", + "integrity": "sha512-tVpsJW7DdjecAiFpbIB1e3qxIQsE6NoPc5/eTdrbbIC4h0LVsWhnoa3g+m2HclBIujHzsxZ4VJVA+GUuc2/LBw==", + "dev": true, + "license": "ISC", + "engines": { + "node": ">=12" + } + }, + "node_modules/yargs/node_modules/emoji-regex": { + "version": "8.0.0", + "resolved": "https://registry.npmjs.org/emoji-regex/-/emoji-regex-8.0.0.tgz", + "integrity": "sha512-MSjYzcWNOA0ewAHpz0MxpYFvwg6yjy1NG3xteoqz644VCo/RPgnr1/GGt+ic3iJTzQ8Eu3TdM14SawnVUmGE6A==", + "dev": true, + "license": "MIT" + }, + "node_modules/yargs/node_modules/string-width": { + "version": "4.2.3", + "resolved": "https://registry.npmjs.org/string-width/-/string-width-4.2.3.tgz", + "integrity": "sha512-wKyQRQpjJ0sIp62ErSZdGsjMJWsap5oRNihHhu6G7JVO/9jIB6UyevL+tXuOqrng8j/cxKTWyWUwvSTriiZz/g==", + "dev": true, + "license": "MIT", + "dependencies": { + "emoji-regex": "^8.0.0", + "is-fullwidth-code-point": "^3.0.0", + "strip-ansi": "^6.0.1" + }, + "engines": { + "node": ">=8" + } } }, "dependencies": { @@ -5793,12 +6526,48 @@ "strip-json-comments": "^3.1.1" } }, - "@eslint/js": { - "version": "8.57.0", - "resolved": "https://registry.npmjs.org/@eslint/js/-/js-8.57.0.tgz", - "integrity": "sha512-Ys+3g2TaW7gADOJzPt83SJtCDhMjndcDMFVQ/Tj9iA1BfJzFKD9mAUXT3OenpuPHbI6P/myECxRJrofUsDx/5g==", - "dev": true - }, + "@eslint/js": { + "version": "8.57.0", + "resolved": "https://registry.npmjs.org/@eslint/js/-/js-8.57.0.tgz", + "integrity": "sha512-Ys+3g2TaW7gADOJzPt83SJtCDhMjndcDMFVQ/Tj9iA1BfJzFKD9mAUXT3OenpuPHbI6P/myECxRJrofUsDx/5g==", + "dev": true + }, + "@grpc/grpc-js": { + "version": "1.14.5", + "resolved": "https://registry.npmjs.org/@grpc/grpc-js/-/grpc-js-1.14.5.tgz", + "integrity": "sha512-7VZM+SVdEcUUqSQeNI3zM8Qs/BhQKZndPo2h5VkYkAM8Iz0wJIa8mKV5ekQGqG8UUsnkQ0NMxIxwkIHYvj0qOw==", + "dev": true, + "requires": { + "@grpc/proto-loader": "^0.8.0", + "@js-sdsl/ordered-map": "^4.4.2" + }, + "dependencies": { + "@grpc/proto-loader": { + "version": "0.8.1", + "resolved": "https://registry.npmjs.org/@grpc/proto-loader/-/proto-loader-0.8.1.tgz", + "integrity": "sha512-wtF6h+DY6M3YaDBPAmvuuA6jV8Sif9MjtOI5euKFWRgCDl5PeDpPsHR9u2l6St5ceY8AZgoNDww5+HvEsXFsGg==", + "dev": true, + "requires": { + "lodash.camelcase": "^4.3.0", + "long": "^5.0.0", + "protobufjs": "^7.5.5", + "yargs": "^17.7.2" + } + } + } + }, + "@grpc/proto-loader": { + "version": "0.7.15", + "resolved": "https://registry.npmjs.org/@grpc/proto-loader/-/proto-loader-0.7.15.tgz", + "integrity": "sha512-tMXdRCfYVixjuFK+Hk0Q1s38gV9zDiDJfWL3h1rv4Qc39oILCu1TRTDt7+fGUI8K4G1Fj125Hx/ru3azECWTyQ==", + "dev": true, + "requires": { + "lodash.camelcase": "^4.3.0", + "long": "^5.0.0", + "protobufjs": "^7.2.5", + "yargs": "^17.7.2" + } + }, "@hegeldev/hegel": { "version": "0.4.5", "resolved": "https://registry.npmjs.org/@hegeldev/hegel/-/hegel-0.4.5.tgz", @@ -5871,6 +6640,36 @@ "integrity": "sha512-6EwiSjwWYP7pTckG6I5eyFANjPhmPjUX9JRLUSfNPC7FX7zK9gyZAfUEaECL6ALTpGX5AjnBq3C9XmVWPitNpw==", "dev": true }, + "@informalsystems/quint": { + "version": "0.33.0", + "resolved": "https://registry.npmjs.org/@informalsystems/quint/-/quint-0.33.0.tgz", + "integrity": "sha512-1hr+l+3wyKimjNXNl9lovpwmH5C9Ck898FL4yGbuEmFPiz7YRqvFvsB9hlHsaYukXqdUY5nuFKn/qiCon0O88g==", + "dev": true, + "requires": { + "@grpc/grpc-js": "^1.11.1", + "@grpc/proto-loader": "^0.7.7", + "@octokit/request": "^8.1.1", + "@sweet-monads/either": "~3.2.0", + "@sweet-monads/maybe": "~3.2.0", + "@types/line-column": "^1.0.0", + "@types/lodash.clonedeep": "4.5.0", + "@types/seedrandom": "^3.0.4", + "adm-zip": "^0.6.1", + "antlr4ts": "^0.5.0-alpha.4", + "chalk": "^4.1.2", + "cli-progress": "^3.12.0", + "cross-spawn": "^7.0.6", + "eol": "^0.9.1", + "immutable": "^4.3.0", + "json-bigint": "^1.0.0", + "line-column": "^1.0.2", + "lodash": "^4.17.21", + "lodash.clonedeep": "4.5.0", + "seedrandom": "^3.0.5", + "tar": "^7.5.13", + "yargs": "^17.7.2" + } + }, "@isaacs/cliui": { "version": "8.0.2", "resolved": "https://registry.npmjs.org/@isaacs/cliui/-/cliui-8.0.2.tgz", @@ -5902,6 +6701,15 @@ } } }, + "@isaacs/fs-minipass": { + "version": "4.0.1", + "resolved": "https://registry.npmjs.org/@isaacs/fs-minipass/-/fs-minipass-4.0.1.tgz", + "integrity": "sha512-wgm9Ehl2jpeqP3zw/7mo3kRHFp5MEDhqAdwy1fTGkHAwnkGOVsgpvQhL8B5n1qlb01jV3n/bI0ZfZp5lWA1k4w==", + "dev": true, + "requires": { + "minipass": "^7.0.4" + } + }, "@jridgewell/gen-mapping": { "version": "0.3.8", "resolved": "https://registry.npmjs.org/@jridgewell/gen-mapping/-/gen-mapping-0.3.8.tgz", @@ -5941,6 +6749,12 @@ "@jridgewell/sourcemap-codec": "^1.4.14" } }, + "@js-sdsl/ordered-map": { + "version": "4.4.2", + "resolved": "https://registry.npmjs.org/@js-sdsl/ordered-map/-/ordered-map-4.4.2.tgz", + "integrity": "sha512-iUKgm52T8HOE/makSxjqoWhe95ZJA1/G1sYsGev2JDKUSS14KAgg1LHb+Ba+IPow0xflbnSkOsZcO08C7w1gYw==", + "dev": true + }, "@koromix/koffi-darwin-arm64": { "version": "3.1.5", "resolved": "https://registry.npmjs.org/@koromix/koffi-darwin-arm64/-/koffi-darwin-arm64-3.1.5.tgz", @@ -6077,6 +6891,54 @@ "fastq": "^1.6.0" } }, + "@octokit/endpoint": { + "version": "9.0.6", + "resolved": "https://registry.npmjs.org/@octokit/endpoint/-/endpoint-9.0.6.tgz", + "integrity": "sha512-H1fNTMA57HbkFESSt3Y9+FBICv+0jFceJFPWDePYlR/iMGrwM5ph+Dd4XRQs+8X+PUFURLQgX9ChPfhJ/1uNQw==", + "dev": true, + "requires": { + "@octokit/types": "^13.1.0", + "universal-user-agent": "^6.0.0" + } + }, + "@octokit/openapi-types": { + "version": "24.2.0", + "resolved": "https://registry.npmjs.org/@octokit/openapi-types/-/openapi-types-24.2.0.tgz", + "integrity": "sha512-9sIH3nSUttelJSXUrmGzl7QUBFul0/mB8HRYl3fOlgHbIWG+WnYDXU3v/2zMtAvuzZ/ed00Ei6on975FhBfzrg==", + "dev": true + }, + "@octokit/request": { + "version": "8.4.1", + "resolved": "https://registry.npmjs.org/@octokit/request/-/request-8.4.1.tgz", + "integrity": "sha512-qnB2+SY3hkCmBxZsR/MPCybNmbJe4KAlfWErXq+rBKkQJlbjdJeS85VI9r8UqeLYLvnAenU8Q1okM/0MBsAGXw==", + "dev": true, + "requires": { + "@octokit/endpoint": "^9.0.6", + "@octokit/request-error": "^5.1.1", + "@octokit/types": "^13.1.0", + "universal-user-agent": "^6.0.0" + } + }, + "@octokit/request-error": { + "version": "5.1.1", + "resolved": "https://registry.npmjs.org/@octokit/request-error/-/request-error-5.1.1.tgz", + "integrity": "sha512-v9iyEQJH6ZntoENr9/yXxjuezh4My67CBSu9r6Ve/05Iu5gNgnisNWOsoJHTP6k0Rr0+HQIpnH+kyammu90q/g==", + "dev": true, + "requires": { + "@octokit/types": "^13.1.0", + "deprecation": "^2.0.0", + "once": "^1.4.0" + } + }, + "@octokit/types": { + "version": "13.10.0", + "resolved": "https://registry.npmjs.org/@octokit/types/-/types-13.10.0.tgz", + "integrity": "sha512-ifLaO34EbbPj0Xgro4G5lP5asESjwHracYJvVaPIyXMuiuXLlhic3S47cBdTb+jfODkTE5YtGCLt3Ay3+J97sA==", + "dev": true, + "requires": { + "@octokit/openapi-types": "^24.2.0" + } + }, "@opentelemetry/api": { "version": "1.8.0", "resolved": "https://registry.npmjs.org/@opentelemetry/api/-/api-1.8.0.tgz", @@ -6145,6 +7007,63 @@ "integrity": "sha512-8LduaNlMZGwdZ6qWrKlfa+2M4gahzFkprZiAt2TF8uS0qQgBizKXpXURqvTJ4WtmupWxaLqjRb2UCTe72mu+Aw==", "dev": true }, + "@protobufjs/aspromise": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/aspromise/-/aspromise-1.1.2.tgz", + "integrity": "sha512-j+gKExEuLmKwvz3OgROXtrJ2UG2x8Ch2YZUxahh+s1F2HZ+wAceUNLkvy6zKCPVRkU++ZWQrdxsUeQXmcg4uoQ==", + "dev": true + }, + "@protobufjs/base64": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/base64/-/base64-1.1.2.tgz", + "integrity": "sha512-AZkcAA5vnN/v4PDqKyMR5lx7hZttPDgClv83E//FMNhR2TMcLUhfRUBHCmSl0oi9zMgDDqRUJkSxO3wm85+XLg==", + "dev": true + }, + "@protobufjs/codegen": { + "version": "2.0.5", + "resolved": "https://registry.npmjs.org/@protobufjs/codegen/-/codegen-2.0.5.tgz", + "integrity": "sha512-zgXFLzW3Ap33e6d0Wlj4MGIm6Ce8O89n/apUaGNB/jx+hw+ruWEp7EwGUshdLKVRCxZW12fp9r40E1mQrf/34g==", + "dev": true + }, + "@protobufjs/eventemitter": { + "version": "1.1.1", + "resolved": "https://registry.npmjs.org/@protobufjs/eventemitter/-/eventemitter-1.1.1.tgz", + "integrity": "sha512-vW1GmwMZNnL+gMRaovlh9yZX74kc+TTU3FObkkurpMaRtBfLP3ldjS9KQWlwZgraRE0+dheEEoAxdzcJQ8eXZg==", + "dev": true + }, + "@protobufjs/fetch": { + "version": "1.1.1", + "resolved": "https://registry.npmjs.org/@protobufjs/fetch/-/fetch-1.1.1.tgz", + "integrity": "sha512-GpptLrs57adMSuHi3VNj0mAF8dwh36LMaYF6XyJ6JMWlVsc+t42tm1HSEDmOs3A8fC9yyeisgLhsTVQokOZ0zw==", + "dev": true, + "requires": { + "@protobufjs/aspromise": "^1.1.1" + } + }, + "@protobufjs/float": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/@protobufjs/float/-/float-1.0.2.tgz", + "integrity": "sha512-Ddb+kVXlXst9d+R9PfTIxh1EdNkgoRe5tOX6t01f1lYWOvJnSPDBlG241QLzcyPdoNTsblLUdujGSE4RzrTZGQ==", + "dev": true + }, + "@protobufjs/path": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/path/-/path-1.1.2.tgz", + "integrity": "sha512-6JOcJ5Tm08dOHAbdR3GrvP+yUUfkjG5ePsHYczMFLq3ZmMkAD98cDgcT2iA1lJ9NVwFd4tH/iSSoe44YWkltEA==", + "dev": true + }, + "@protobufjs/pool": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/@protobufjs/pool/-/pool-1.1.0.tgz", + "integrity": "sha512-0kELaGSIDBKvcgS4zkjz1PeddatrjYcmMWOlAuAPwAeccUrPHdUqo/J6LiymHHEiJT5NrF1UVwxY14f+fy4WQw==", + "dev": true + }, + "@protobufjs/utf8": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/utf8/-/utf8-1.1.2.tgz", + "integrity": "sha512-b1UQwcEZ4yCnMCD8DAL1VlbvBJE9/IX4FTIp7BG1xYpf29SLazLSrqUkj4w7Y5y7cCVP6E5tcqqcI0xemPkHug==", + "dev": true + }, "@rollup/rollup-android-arm-eabi": { "version": "4.59.0", "resolved": "https://registry.npmjs.org/@rollup/rollup-android-arm-eabi/-/rollup-android-arm-eabi-4.59.0.tgz", @@ -6320,6 +7239,24 @@ "dev": true, "optional": true }, + "@sinonjs/commons": { + "version": "3.0.1", + "resolved": "https://registry.npmjs.org/@sinonjs/commons/-/commons-3.0.1.tgz", + "integrity": "sha512-K3mCHKQ9sVh8o1C9cxkwxaOmXoAMlDxC1mYyHrjqOWEcBjYr76t96zL2zlj5dUGZ3HSw240X1qgH3Mjf1yJWpQ==", + "dev": true, + "requires": { + "type-detect": "4.0.8" + } + }, + "@sinonjs/fake-timers": { + "version": "15.4.0", + "resolved": "https://registry.npmjs.org/@sinonjs/fake-timers/-/fake-timers-15.4.0.tgz", + "integrity": "sha512-DsG+8/LscQIQg68J6Ef3dv10u6nVyetYn923s3/sus5eaGfTo1of5WMZSLf0UJc9KDuKPilPH0UDJCjvNbDNCA==", + "dev": true, + "requires": { + "@sinonjs/commons": "^3.0.1" + } + }, "@stylistic/eslint-plugin": { "version": "2.6.4", "resolved": "https://registry.npmjs.org/@stylistic/eslint-plugin/-/eslint-plugin-2.6.4.tgz", @@ -6497,6 +7434,30 @@ } } }, + "@sweet-monads/either": { + "version": "3.2.0", + "resolved": "https://registry.npmjs.org/@sweet-monads/either/-/either-3.2.0.tgz", + "integrity": "sha512-n+nR0b60GRTKb+D76qhTf4NEBXU9zfpigYYEtKtSYbV+5+i5gxr9jFd64pYkY2O7hVsb/G7nspbAeFni/i1ltA==", + "dev": true, + "requires": { + "@sweet-monads/interfaces": "^3.2.0" + } + }, + "@sweet-monads/interfaces": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@sweet-monads/interfaces/-/interfaces-3.3.0.tgz", + "integrity": "sha512-66akGvjPD4lizQy+w4JSltJilc2w/QPdw8lPAniLJGHwyjmrw9xMJLx76Q/GDnbCU59Werses4aZJLWOlJrL5A==", + "dev": true + }, + "@sweet-monads/maybe": { + "version": "3.2.0", + "resolved": "https://registry.npmjs.org/@sweet-monads/maybe/-/maybe-3.2.0.tgz", + "integrity": "sha512-/t+K0D/kBfkYOkZaePEsrK868at0M9UIEVgehcM0xscrCSZhKWGteE41vl2XJQqh8WyiFo/mZ5y7eAPSYzS+pg==", + "dev": true, + "requires": { + "@sweet-monads/interfaces": "^3.2.0" + } + }, "@types/chai": { "version": "5.2.3", "resolved": "https://registry.npmjs.org/@types/chai/-/chai-5.2.3.tgz", @@ -6535,12 +7496,39 @@ "integrity": "sha512-5+fP8P8MFNC+AyZCDxrB2pkZFPGzqQWUzpSeuuVLvm8VMcorNYavBqoFcxK8bQz4Qsbn4oUEEem4wDLfcysGHA==", "dev": true }, + "@types/line-column": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/@types/line-column/-/line-column-1.0.2.tgz", + "integrity": "sha512-099oFQmp/Tlf20xW5XI5R4F69N6lF/zQ09XDzc3R5BOLFlqIotgKoNIyj0HD4fQLWcGDreDJv8k/BkLJscrDrw==", + "dev": true + }, + "@types/lodash": { + "version": "4.17.25", + "resolved": "https://registry.npmjs.org/@types/lodash/-/lodash-4.17.25.tgz", + "integrity": "sha512-+K1NIO8I+F9/wNulfVvu23QYd0Pe9/OCqRrim4NoYIf1VoEDL90Ve4ClzpyqBLc7NpGGWRvYNCKZ1BE/Jpf8dQ==", + "dev": true + }, + "@types/lodash.clonedeep": { + "version": "4.5.0", + "resolved": "https://registry.npmjs.org/@types/lodash.clonedeep/-/lodash.clonedeep-4.5.0.tgz", + "integrity": "sha512-IHijjFVPJTvzvrNPz+6nQy5lZQb7uh807RfTIEaQBrZXrIGjZy0L2dEb3hju34J0eqbXLCY6Hub/g81Jl4pGCA==", + "dev": true, + "requires": { + "@types/lodash": "*" + } + }, "@types/node": { "version": "20.5.7", "resolved": "https://registry.npmjs.org/@types/node/-/node-20.5.7.tgz", "integrity": "sha512-dP7f3LdZIysZnmvP3ANJYTSwg+wLLl8p7RqniVlV7j+oXSXAbt9h0WIBFmJy5inWZoX9wZN6eXx+YXd9Rh3RBA==", "dev": true }, + "@types/seedrandom": { + "version": "3.0.8", + "resolved": "https://registry.npmjs.org/@types/seedrandom/-/seedrandom-3.0.8.tgz", + "integrity": "sha512-TY1eezMU2zH2ozQoAFAQFOPpvP15g+ZgSfTZt31AUUH/Rxtnz3H+A/Sv1Snw2/amp//omibc+AEkTaA8KUeOLQ==", + "dev": true + }, "@types/ws": { "version": "8.5.5", "resolved": "https://registry.npmjs.org/@types/ws/-/ws-8.5.5.tgz", @@ -6775,6 +7763,12 @@ "dev": true, "requires": {} }, + "adm-zip": { + "version": "0.6.1", + "resolved": "https://registry.npmjs.org/adm-zip/-/adm-zip-0.6.1.tgz", + "integrity": "sha512-Xwrja8nx9e5o2N1my4DsKCeKpdrnACyr1wtbPxBDgGzKzKyE9kRtBFA8mWldI+RVlD7CBZNWY/wQ2+ydwOR6kQ==", + "dev": true + }, "ajv": { "version": "6.12.6", "resolved": "https://registry.npmjs.org/ajv/-/ajv-6.12.6.tgz", @@ -6799,6 +7793,12 @@ "integrity": "sha512-bN798gFfQX+viw3R7yrGWRqnrN2oRkEkUjjl4JNn4E8GxxbjtG3FbrEIIY3l8/hrwUwIeCZvi4QuOTP4MErVug==", "dev": true }, + "antlr4ts": { + "version": "0.5.0-alpha.4", + "resolved": "https://registry.npmjs.org/antlr4ts/-/antlr4ts-0.5.0-alpha.4.tgz", + "integrity": "sha512-WPQDt1B74OfPv/IMS2ekXAKkTZIHl88uMetg6q3OTqgFxZ/dxDXI0EWLyZid/1Pe6hTftyg5N7gel5wNAGxXyQ==", + "dev": true + }, "any-promise": { "version": "1.3.0", "resolved": "https://registry.npmjs.org/any-promise/-/any-promise-1.3.0.tgz", @@ -6829,6 +7829,12 @@ "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw==", "dev": true }, + "bignumber.js": { + "version": "9.3.1", + "resolved": "https://registry.npmjs.org/bignumber.js/-/bignumber.js-9.3.1.tgz", + "integrity": "sha512-Ko0uX15oIUS7wJ3Rb30Fs6SkVbLmPBAKdlm7q9+ak9bbIeFf0MwuBsQV6z7+X768/cHsfg+WlysDWJcmthjsjQ==", + "dev": true + }, "brace-expansion": { "version": "1.1.18", "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.18.tgz", @@ -6918,6 +7924,90 @@ "readdirp": "^4.0.1" } }, + "chownr": { + "version": "3.0.0", + "resolved": "https://registry.npmjs.org/chownr/-/chownr-3.0.0.tgz", + "integrity": "sha512-+IxzY9BZOQd/XuYPRmrvEVjF/nqj5kgT4kEq7VofrDoM1MxoRjEWkrCC3EtLi59TVawxTAn+orJwFQcrqEN1+g==", + "dev": true + }, + "cli-progress": { + "version": "3.12.0", + "resolved": "https://registry.npmjs.org/cli-progress/-/cli-progress-3.12.0.tgz", + "integrity": "sha512-tRkV3HJ1ASwm19THiiLIXLO7Im7wlTuKnvkYaTkyoAPefqjNg7W7DHKUlGRxy9vxDvbyCYQkQozvptuMkGCg8A==", + "dev": true, + "requires": { + "string-width": "^4.2.3" + }, + "dependencies": { + "emoji-regex": { + "version": "8.0.0", + "resolved": "https://registry.npmjs.org/emoji-regex/-/emoji-regex-8.0.0.tgz", + "integrity": "sha512-MSjYzcWNOA0ewAHpz0MxpYFvwg6yjy1NG3xteoqz644VCo/RPgnr1/GGt+ic3iJTzQ8Eu3TdM14SawnVUmGE6A==", + "dev": true + }, + "string-width": { + "version": "4.2.3", + "resolved": "https://registry.npmjs.org/string-width/-/string-width-4.2.3.tgz", + "integrity": "sha512-wKyQRQpjJ0sIp62ErSZdGsjMJWsap5oRNihHhu6G7JVO/9jIB6UyevL+tXuOqrng8j/cxKTWyWUwvSTriiZz/g==", + "dev": true, + "requires": { + "emoji-regex": "^8.0.0", + "is-fullwidth-code-point": "^3.0.0", + "strip-ansi": "^6.0.1" + } + } + } + }, + "cliui": { + "version": "8.0.1", + "resolved": "https://registry.npmjs.org/cliui/-/cliui-8.0.1.tgz", + "integrity": "sha512-BSeNnyus75C4//NQ9gQt1/csTXyo/8Sb+afLAkzAptFuMsod9HFokGNudZpi/oQV73hnVK+sR+5PVRMd+Dr7YQ==", + "dev": true, + "requires": { + "string-width": "^4.2.0", + "strip-ansi": "^6.0.1", + "wrap-ansi": "^7.0.0" + }, + "dependencies": { + "ansi-styles": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz", + "integrity": "sha512-zbB9rCJAT1rbjiVDb2hqKFHNYLxgtk8NURxZ3IZwD3F6NtxbXZQCnnSi1Lkx+IDohdPlFp222wVALIheZJQSEg==", + "dev": true, + "requires": { + "color-convert": "^2.0.1" + } + }, + "emoji-regex": { + "version": "8.0.0", + "resolved": "https://registry.npmjs.org/emoji-regex/-/emoji-regex-8.0.0.tgz", + "integrity": "sha512-MSjYzcWNOA0ewAHpz0MxpYFvwg6yjy1NG3xteoqz644VCo/RPgnr1/GGt+ic3iJTzQ8Eu3TdM14SawnVUmGE6A==", + "dev": true + }, + "string-width": { + "version": "4.2.3", + "resolved": "https://registry.npmjs.org/string-width/-/string-width-4.2.3.tgz", + "integrity": "sha512-wKyQRQpjJ0sIp62ErSZdGsjMJWsap5oRNihHhu6G7JVO/9jIB6UyevL+tXuOqrng8j/cxKTWyWUwvSTriiZz/g==", + "dev": true, + "requires": { + "emoji-regex": "^8.0.0", + "is-fullwidth-code-point": "^3.0.0", + "strip-ansi": "^6.0.1" + } + }, + "wrap-ansi": { + "version": "7.0.0", + "resolved": "https://registry.npmjs.org/wrap-ansi/-/wrap-ansi-7.0.0.tgz", + "integrity": "sha512-YVGIj2kamLSTxw6NsZjoBxfSwsn0ycdesmc4p+Q21c5zPuZ1pl+NfxVdxPtdHvmNVOQ6XSYG4AUtyt/Fi7D16Q==", + "dev": true, + "requires": { + "ansi-styles": "^4.0.0", + "string-width": "^4.1.0", + "strip-ansi": "^6.0.0" + } + } + } + }, "color-convert": { "version": "2.0.1", "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz", @@ -6989,6 +8079,12 @@ "integrity": "sha512-oIPzksmTg4/MriiaYGO+okXDT7ztn/w3Eptv/+gSIdMdKsJo0u4CfYNFJPy+4SKMuCqGw2wxnA+URMg3t8a/bQ==", "dev": true }, + "deprecation": { + "version": "2.3.1", + "resolved": "https://registry.npmjs.org/deprecation/-/deprecation-2.3.1.tgz", + "integrity": "sha512-xmHIy4F3scKVwMsQ4WnVaS8bHOx0DmVwRywosKhaILI0ywMDWPtBSku2HNxRvF7jtwDRsoEwYQSfbxj8b7RlJQ==", + "dev": true + }, "dir-glob": { "version": "3.0.1", "resolved": "https://registry.npmjs.org/dir-glob/-/dir-glob-3.0.1.tgz", @@ -7019,6 +8115,12 @@ "integrity": "sha512-L18DaJsXSUk2+42pv8mLs5jJT2hqFkFE4j21wOmgbUqsZ2hL72NsUU785g9RXgo3s0ZNgVl42TiHp3ZtOv/Vyg==", "dev": true }, + "eol": { + "version": "0.9.1", + "resolved": "https://registry.npmjs.org/eol/-/eol-0.9.1.tgz", + "integrity": "sha512-Ds/TEoZjwggRoz/Q2O7SE3i4Jm66mqTDfmdHdq/7DKVk3bro9Q8h6WdXKdPqFLMoqxrDK5SVRzHVPOS6uuGtrg==", + "dev": true + }, "es-module-lexer": { "version": "1.7.0", "resolved": "https://registry.npmjs.org/es-module-lexer/-/es-module-lexer-1.7.0.tgz", @@ -7058,6 +8160,12 @@ "@esbuild/win32-x64": "0.25.1" } }, + "escalade": { + "version": "3.2.0", + "resolved": "https://registry.npmjs.org/escalade/-/escalade-3.2.0.tgz", + "integrity": "sha512-WUj2qlxaQtO4g6Pq5c29GTcWGDyd8itL8zTlipgECz3JesAiiOKotd8JU6otB3PACgG6xkJUyVhboMS+bje/jA==", + "dev": true + }, "escape-string-regexp": { "version": "4.0.0", "resolved": "https://registry.npmjs.org/escape-string-regexp/-/escape-string-regexp-4.0.0.tgz", @@ -7341,6 +8449,12 @@ "dev": true, "optional": true }, + "get-caller-file": { + "version": "2.0.5", + "resolved": "https://registry.npmjs.org/get-caller-file/-/get-caller-file-2.0.5.tgz", + "integrity": "sha512-DyFP3BM/3YHTQOCUL/w0OZHR0lpKeGrxotcHWcqNEdnltqFwXVfhEBQ94eIo34AfQpo0rGki4cyIiftY06h2Fg==", + "dev": true + }, "glob": { "version": "7.1.6", "resolved": "https://registry.npmjs.org/glob/-/glob-7.1.6.tgz", @@ -7405,6 +8519,12 @@ "integrity": "sha512-5Fytz/IraMjqpwfd34ke28PTVMjZjJG2MPn5t7OE4eUCUNf8BAa7b5WUS9/Qvr6mwOQS7Mk6vdsMno5he+T8Xw==", "dev": true }, + "immutable": { + "version": "4.3.9", + "resolved": "https://registry.npmjs.org/immutable/-/immutable-4.3.9.tgz", + "integrity": "sha512-ObHy4YN7ycwZOUCLI1/6svfyAFu7vL8RhAvVu/bh/RZW9EPlOyDaQ9jDQWCtdqzaXUjgXZCW1migtHE7YI7UGQ==", + "dev": true + }, "import-fresh": { "version": "3.3.0", "resolved": "https://registry.npmjs.org/import-fresh/-/import-fresh-3.3.0.tgz", @@ -7478,12 +8598,27 @@ "integrity": "sha512-Fd4gABb+ycGAmKou8eMftCupSir5lRxqf4aD/vd0cD2qc4HL07OjCeuHMr8Ro4CoMaeCKDB0/ECBOVWjTwUvPQ==", "dev": true }, + "isarray": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/isarray/-/isarray-1.0.0.tgz", + "integrity": "sha512-VLghIWNM6ELQzo7zwmcg0NmTVyWKYjvIeM83yjp0wRDTmUnrM678fQbcKBo6n2CJEF0szoG//ytg+TKla89ALQ==", + "dev": true + }, "isexe": { "version": "2.0.0", "resolved": "https://registry.npmjs.org/isexe/-/isexe-2.0.0.tgz", "integrity": "sha512-RHxMLp9lnKHGHRng9QFhRCMbYAcVpn69smSGcq3f36xjgVVWThj4qqLbTLlq7Ssj8B+fIQ1EuCEGI2lKsyQeIw==", "dev": true }, + "isobject": { + "version": "2.1.0", + "resolved": "https://registry.npmjs.org/isobject/-/isobject-2.1.0.tgz", + "integrity": "sha512-+OUdGJlgjOBZDfxnDjYYG6zp487z0JGNQq3cYQYg5f5hKR+syHMsaztzGeml/4kGG55CSpKSpWTY+jYGgsHLgA==", + "dev": true, + "requires": { + "isarray": "1.0.0" + } + }, "jackspeak": { "version": "3.4.3", "resolved": "https://registry.npmjs.org/jackspeak/-/jackspeak-3.4.3.tgz", @@ -7515,6 +8650,15 @@ "argparse": "^2.0.1" } }, + "json-bigint": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/json-bigint/-/json-bigint-1.0.0.tgz", + "integrity": "sha512-SiPv/8VpZuWbvLSMtTDU8hEfrZWg/mH/nV/b4o0CYbSxu1UIQPLdwKOCIyLQX+VIPO5vrLX3i8qtqFyhdPSUSQ==", + "dev": true, + "requires": { + "bignumber.js": "^9.0.0" + } + }, "json-buffer": { "version": "3.0.1", "resolved": "https://registry.npmjs.org/json-buffer/-/json-buffer-3.0.1.tgz", @@ -7581,6 +8725,16 @@ "integrity": "sha512-/vlFKAoH5Cgt3Ie+JLhRbwOsCQePABiU3tJ1egGvyQ+33R/vcwM2Zl2QR/LzjsBeItPt3oSVXapn+m4nQDvpzw==", "dev": true }, + "line-column": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/line-column/-/line-column-1.0.2.tgz", + "integrity": "sha512-Ktrjk5noGYlHsVnYWh62FLVs4hTb8A3e+vucNZMgPeAOITdshMSgv4cCZQeRDjm7+goqmo6+liZwTXo+U3sVww==", + "dev": true, + "requires": { + "isarray": "^1.0.0", + "isobject": "^2.0.0" + } + }, "lines-and-columns": { "version": "1.2.4", "resolved": "https://registry.npmjs.org/lines-and-columns/-/lines-and-columns-1.2.4.tgz", @@ -7602,12 +8756,36 @@ "p-locate": "^5.0.0" } }, + "lodash": { + "version": "4.18.1", + "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.18.1.tgz", + "integrity": "sha512-dMInicTPVE8d1e5otfwmmjlxkZoUpiVLwyeTdUsi/Caj/gfzzblBcCE5sRHV/AsjuCmxWrte2TNGSYuCeCq+0Q==", + "dev": true + }, + "lodash.camelcase": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/lodash.camelcase/-/lodash.camelcase-4.3.0.tgz", + "integrity": "sha512-TwuEnCnxbc3rAvhf/LbG7tJUDzhqXyFnv3dtzLOPgCG/hODL7WFnsbwktkD7yUV0RrreP/l1PALq/YSg6VvjlA==", + "dev": true + }, + "lodash.clonedeep": { + "version": "4.5.0", + "resolved": "https://registry.npmjs.org/lodash.clonedeep/-/lodash.clonedeep-4.5.0.tgz", + "integrity": "sha512-H5ZhCF25riFd9uB5UCkVKo61m3S/xZk1x4wA6yp/L3RFP6Z/eHH1ymQcGLo7J3GMPfm0V/7m1tryHuGVxpqEBQ==", + "dev": true + }, "lodash.merge": { "version": "4.6.2", "resolved": "https://registry.npmjs.org/lodash.merge/-/lodash.merge-4.6.2.tgz", "integrity": "sha512-0KpjqXRVvrYyCsX1swR/XTK0va6VQkQM6MNo7PqW77ByjAhoARA8EfrP1N4+KlKj8YS0ZUCtRT/YUuhyYDujIQ==", "dev": true }, + "long": { + "version": "5.3.2", + "resolved": "https://registry.npmjs.org/long/-/long-5.3.2.tgz", + "integrity": "sha512-mNAgZ1GmyNhD7AuqnTG3/VQ26o760+ZYBPKjPvugO8+nLbYfX6TVpJPseBvopbdY+qpZ/lKUnmEc1LeZYS3QAA==", + "dev": true + }, "loupe": { "version": "3.2.1", "resolved": "https://registry.npmjs.org/loupe/-/loupe-3.2.1.tgz", @@ -7660,6 +8838,15 @@ "integrity": "sha512-qOOzS1cBTWYF4BH8fVePDBOO9iptMnGUEZwNc/cMWnTV2nVLZ7VoNWEPHkYczZA0pdoA7dl6e7FL659nX9S2aw==", "dev": true }, + "minizlib": { + "version": "3.1.0", + "resolved": "https://registry.npmjs.org/minizlib/-/minizlib-3.1.0.tgz", + "integrity": "sha512-KZxYo1BUkWD2TVFLr0MQoM8vUUigWD3LlD83a/75BqC+4qE0Hb1Vo5v1FgcfaNXvfXzr+5EhQ6ing/CaBijTlw==", + "dev": true, + "requires": { + "minipass": "^7.1.2" + } + }, "mlly": { "version": "1.8.0", "resolved": "https://registry.npmjs.org/mlly/-/mlly-1.8.0.tgz", @@ -7900,6 +9087,25 @@ "fast-diff": "^1.1.2" } }, + "protobufjs": { + "version": "7.6.6", + "resolved": "https://registry.npmjs.org/protobufjs/-/protobufjs-7.6.6.tgz", + "integrity": "sha512-dYDWdjSl5RNb7SgPxGQcRU+GtvP7s2fpkrY0r432PcOIaZ0/rBcxEZnQN67iJhFuQiVw754JDoPruPCNdGsbjg==", + "dev": true, + "requires": { + "@protobufjs/aspromise": "^1.1.2", + "@protobufjs/base64": "^1.1.2", + "@protobufjs/codegen": "^2.0.5", + "@protobufjs/eventemitter": "^1.1.1", + "@protobufjs/fetch": "^1.1.1", + "@protobufjs/float": "^1.0.2", + "@protobufjs/path": "^1.1.2", + "@protobufjs/pool": "^1.1.0", + "@protobufjs/utf8": "^1.1.1", + "@types/node": ">=13.7.0", + "long": "^5.3.2" + } + }, "punycode": { "version": "2.3.0", "resolved": "https://registry.npmjs.org/punycode/-/punycode-2.3.0.tgz", @@ -7918,6 +9124,12 @@ "integrity": "sha512-GDhwkLfywWL2s6vEjyhri+eXmfH6j1L7JE27WhqLeYzoh/A3DBaYGEj2H/HFZCn/kMfim73FXxEJTw06WtxQwg==", "dev": true }, + "require-directory": { + "version": "2.1.1", + "resolved": "https://registry.npmjs.org/require-directory/-/require-directory-2.1.1.tgz", + "integrity": "sha512-fGxEI7+wsG9xrvdjsrlmL22OMTTiHRwAMroiEeMgq8gzoLC/PQr7RsRDSTLUg/bZAZtF+TVIkHc6/4RIKrui+Q==", + "dev": true + }, "resolve-from": { "version": "5.0.0", "resolved": "https://registry.npmjs.org/resolve-from/-/resolve-from-5.0.0.tgz", @@ -7983,6 +9195,12 @@ "queue-microtask": "^1.2.2" } }, + "seedrandom": { + "version": "3.0.5", + "resolved": "https://registry.npmjs.org/seedrandom/-/seedrandom-3.0.5.tgz", + "integrity": "sha512-8OwmbklUNzwezjGInmZ+2clQmExQPvomqjL7LFqOYqtmuxRgQYqOD3mHaU+MvZn5FLUeVxVfQjwLZW/n/JFuqg==", + "dev": true + }, "semver": { "version": "7.6.2", "resolved": "https://registry.npmjs.org/semver/-/semver-7.6.2.tgz", @@ -8205,6 +9423,19 @@ "tslib": "^2.6.2" } }, + "tar": { + "version": "7.5.22", + "resolved": "https://registry.npmjs.org/tar/-/tar-7.5.22.tgz", + "integrity": "sha512-MFO/QzvtAOmJbkhOaCTvbGcFN9L9b+JunIsDwaKljSOdcLMea3NJ1k9Usz/rjdfSXTq4dfzfeS7W4p4YOAAHeA==", + "dev": true, + "requires": { + "@isaacs/fs-minipass": "^4.0.0", + "chownr": "^3.0.0", + "minipass": "^7.1.2", + "minizlib": "^3.1.0", + "yallist": "^5.0.0" + } + }, "text-table": { "version": "0.2.0", "resolved": "https://registry.npmjs.org/text-table/-/text-table-0.2.0.tgz", @@ -8569,6 +9800,12 @@ "prelude-ls": "^1.2.1" } }, + "type-detect": { + "version": "4.0.8", + "resolved": "https://registry.npmjs.org/type-detect/-/type-detect-4.0.8.tgz", + "integrity": "sha512-0fr/mIH1dlO+x7TlcMy+bIDqKPsw/70tVyeHW787goQjhmqaZe10uwLujubK9q9Lg6Fiho1KUKDYz0Z7k7g5/g==", + "dev": true + }, "type-fest": { "version": "0.20.2", "resolved": "https://registry.npmjs.org/type-fest/-/type-fest-0.20.2.tgz", @@ -8593,6 +9830,12 @@ "integrity": "sha512-9a4/uxlTWJ4+a5i0ooc1rU7C7YOw3wT+UGqdeNNHWnOF9qcMBgLRS+4IYUqbczewFx4mLEig6gawh7X6mFlEkA==", "dev": true }, + "universal-user-agent": { + "version": "6.0.1", + "resolved": "https://registry.npmjs.org/universal-user-agent/-/universal-user-agent-6.0.1.tgz", + "integrity": "sha512-yCzhz6FN2wU1NiiQRogkTQszlQSlpWaw8SvVegAc+bDxbzHgh1vX8uIe8OYyMH6DwH+sdTJsgMl36+mSMdRJIQ==", + "dev": true + }, "uri-js": { "version": "4.4.1", "resolved": "https://registry.npmjs.org/uri-js/-/uri-js-4.4.1.tgz", @@ -8781,6 +10024,58 @@ "resolved": "https://registry.npmjs.org/ws/-/ws-8.21.0.tgz", "integrity": "sha512-Vsp28b7DRcimFQvrqu2Wek3z1iYxDCWqHYB8Qsnk/S4RfaCQzPGPyBNuVjJV3cd6UiKtUtp6sNM77gWvzcCH+g==", "requires": {} + }, + "y18n": { + "version": "5.0.8", + "resolved": "https://registry.npmjs.org/y18n/-/y18n-5.0.8.tgz", + "integrity": "sha512-0pfFzegeDWJHJIAmTLRP2DwHjdF5s7jo9tuztdQxAhINCdvS+3nGINqPd00AphqJR/0LhANUS6/+7SCb98YOfA==", + "dev": true + }, + "yallist": { + "version": "5.0.0", + "resolved": "https://registry.npmjs.org/yallist/-/yallist-5.0.0.tgz", + "integrity": "sha512-YgvUTfwqyc7UXVMrB+SImsVYSmTS8X/tSrtdNZMImM+n7+QTriRXyXim0mBrTXNeqzVF0KWGgHPeiyViFFrNDw==", + "dev": true + }, + "yargs": { + "version": "17.7.3", + "resolved": "https://registry.npmjs.org/yargs/-/yargs-17.7.3.tgz", + "integrity": "sha512-GZtjxm/J/4TSxuL3FNYjCmLktBTnIw/rVmKSIyKeYAZpmJB2ig9VauCC5xsa82GNKVKDAqpOn3KVzNt0zmrU0g==", + "dev": true, + "requires": { + "cliui": "^8.0.1", + "escalade": "^3.1.1", + "get-caller-file": "^2.0.5", + "require-directory": "^2.1.1", + "string-width": "^4.2.3", + "y18n": "^5.0.5", + "yargs-parser": "^21.1.1" + }, + "dependencies": { + "emoji-regex": { + "version": "8.0.0", + "resolved": "https://registry.npmjs.org/emoji-regex/-/emoji-regex-8.0.0.tgz", + "integrity": "sha512-MSjYzcWNOA0ewAHpz0MxpYFvwg6yjy1NG3xteoqz644VCo/RPgnr1/GGt+ic3iJTzQ8Eu3TdM14SawnVUmGE6A==", + "dev": true + }, + "string-width": { + "version": "4.2.3", + "resolved": "https://registry.npmjs.org/string-width/-/string-width-4.2.3.tgz", + "integrity": "sha512-wKyQRQpjJ0sIp62ErSZdGsjMJWsap5oRNihHhu6G7JVO/9jIB6UyevL+tXuOqrng8j/cxKTWyWUwvSTriiZz/g==", + "dev": true, + "requires": { + "emoji-regex": "^8.0.0", + "is-fullwidth-code-point": "^3.0.0", + "strip-ansi": "^6.0.1" + } + } + } + }, + "yargs-parser": { + "version": "21.1.1", + "resolved": "https://registry.npmjs.org/yargs-parser/-/yargs-parser-21.1.1.tgz", + "integrity": "sha512-tVpsJW7DdjecAiFpbIB1e3qxIQsE6NoPc5/eTdrbbIC4h0LVsWhnoa3g+m2HclBIujHzsxZ4VJVA+GUuc2/LBw==", + "dev": true } } } diff --git a/package.json b/package.json index 838d7387..eba9039a 100644 --- a/package.json +++ b/package.json @@ -38,10 +38,12 @@ "devDependencies": { "@bufbuild/buf": "^1.67.0", "@hegeldev/hegel": "^0.4.5", + "@informalsystems/quint": "^0.33.0", "@opentelemetry/api": "^1.7.0", "@opentelemetry/context-async-hooks": "^1.26.0", "@opentelemetry/core": "^1.7.0", "@opentelemetry/sdk-trace-base": "^1.24.1", + "@sinonjs/fake-timers": "^15.4.0", "@stylistic/eslint-plugin": "^2.6.4", "@types/ws": "^8.5.5", "@typescript-eslint/eslint-plugin": "^7.8.0", @@ -71,7 +73,16 @@ "test": "vitest", "test:single": "vitest run --reporter=dot", "test:flake": "./flake.sh", - "bench": "vitest bench" + "bench": "vitest bench", + "spec:typecheck": "quint typecheck spec/river.qnt && quint typecheck spec/river_test.qnt", + "spec:test": "quint test spec/river_test.qnt --max-samples 1", + "spec:check": "quint run spec/river.qnt --invariant safety --max-samples 2000 --max-steps 80", + "spec:hunt": "QUINT_SEED=random QUINT_TRACES=2000 QUINT_STEPS=80 QUINT_BACKEND=rust QUINT_VERBOSE=1 vitest run __tests__/conformance" + }, + "overrides": { + "@informalsystems/quint": { + "adm-zip": "^0.6.1" + } }, "engines": { "node": ">=20.11.0" diff --git a/spec/README.md b/spec/README.md new file mode 100644 index 00000000..89d69c82 --- /dev/null +++ b/spec/README.md @@ -0,0 +1,94 @@ +# River protocol model + +[`river.qnt`](./river.qnt) is an executable model of [PROTOCOL.md](../PROTOCOL.md), written in [Quint](https://quint-lang.org). The test suite replays the model's traces against the TypeScript implementation and compares the two after every step, so any disagreement means one of them is wrong. + +- `river.qnt`: the model's state, transitions, `step` actions, invariants, and witnesses +- `river_test.qnt`: scenarios, one per protocol behavior or bug the model found +- [`__tests__/conformance`](../__tests__/conformance): the harness that replays traces against the implementation + +## What it models + +One client and one server carry up to three procedures of any kind (rpc, stream, upload, subscription) over connections that can lose frames, garble them, or break: + +- connecting: backoff, connection and handshake timeouts, and the client and server session state machines +- the handshake: transparent reconnects, hard reconnects, and each reason the server rejects a session +- sequencing: seq/ack, the send buffer, retransmission on reconnect, and duplicate and out-of-order detection +- the grace period, heartbeats, and the phantom-disconnect watchdog +- stream lifecycles: writes, half-closes, cancellation from either side, handler errors, and teardown when a session ends +- faults: frame loss, undecodable frames, broken connections whose close events reach each side at different times, failed dials, server restarts, `ServerTransport.close()`, and `hardDisconnect()` + +The model does not distinguish codecs; instead, the conformance suite replays every trace over each of them. Version negotiation, handshake metadata, re-handshaking, and multiple clients are out of scope. Frames on a connection arrive in order or not at all, which is what River's transports guarantee. Timers are explicit deadlines, and time moves only when a timer fires or `tickBy` advances it. + +## Invariants + +`safety` combines the invariants below, and every simulated state is checked against it. + +| Invariant | Holds when | +| ------------------------- | ------------------------------------------------------------------------------------------------- | +| `exactlyOnceInOrder` | each side of a stream has received a prefix of what the other side wrote, with nothing duplicated | +| `noCrossSession` | a session never processes a message sent by another session | +| `noAckBeyondSent` | no ack covers a message the peer never sent | +| `sendOrdering` | the implementation's send-ordering assertion never trips | +| `bufferHoldsUnacked` | while both sides share a session, every unacknowledged message is still in its sender's buffer | +| `acksBounded` | neither side acknowledges more than the other has sent | +| `noNeedlessRejection` | a reconnect to a session the server still holds is never rejected for mismatched sequence numbers | +| `graceWhileDisconnected` | a disconnected session always has its grace timer running | +| `watchdogWhileConnected` | a live connection always has a watchdog | +| `teardownResolvesStreams` | when a session ends, every stream it carried is resolved on both sides | +| `closeIsFinal` | after a side closes a stream, it sends nothing more on it except a cancel | +| `closedServerIsEmpty` | a closed server transport holds no sessions and no pending handshakes | + +`cancelIsFinal` (nothing is sent on a stream after its cancel arrives) is kept out of `safety` because the implementation breaks it; see [Bugs found](#bugs-found). The `w*` values are witnesses: `quint run --witnesses wTransparentReconnect wServerRestarted ...` reports how many traces reach each one, which shows whether simulation actually exercises a path. + +## Running it + +| Command | What it does | +| ------------------------ | ------------------------------------------------------------------------------------------------- | +| `npm run spec:typecheck` | typecheck the model and its scenarios | +| `npm run spec:test` | run the scenarios in `river_test.qnt` | +| `npm run spec:check` | simulate 2,000 random traces of 80 steps and check `safety` | +| `npm test` | includes the conformance suite | +| `npm run spec:hunt` | replay 2,000 random traces of 80 steps over every codec, from a fresh random seed (a few minutes) | + +`spec:check` and `spec:hunt` use Quint's Rust simulator, which downloads a binary the first time it runs. Everything in `npm test` uses the TypeScript simulator, so it needs nothing beyond `node_modules`. + +## Conformance + +The suite in `__tests__/conformance` replays model traces against a real `ClientTransport`, `ServerTransport`, router, and client: + +1. `quint run` generates random traces of the weighted `step` action, checking `safety` on every state along the way, and `quint test` produces one trace per scenario. +2. The harness performs each step against the implementation. A scripted in-memory network (`network.ts`) holds frames until the trace delivers, drops, or garbles them. A fake clock from `@sinonjs/fake-timers` advances only when the trace fires a timer or advances time, and timers due at the same moment fire one per step in scheduling order, as in the model. +3. After each step, both sides are projected onto the same observable state: session states, seq/ack, send buffers, frames in flight, stream states, delivered values, how many times each handler ran, upload results once `finalize()` is called, protocol errors, and the number of pending timers. The first difference fails the test with a diff and the steps that led to it. + +The traces are generated once and replayed over each codec the transports support: JSON, binary, and proto. For each codec, the suite runs every scenario, checks that each known bug still reproduces, and replays 100 random traces of 60 steps. Environment variables tune the random part: + +| Variable | Default | Meaning | +| --------------- | ------------ | ------------------------------------------------------------ | +| `QUINT_SEED` | `0x5eed` | seed for the random traces; `random` picks one and prints it | +| `QUINT_TRACES` | `100` | number of random traces | +| `QUINT_STEPS` | `60` | steps per trace | +| `QUINT_BACKEND` | `typescript` | `rust` is faster but downloads a binary | +| `QUINT_VERBOSE` | unset | print how each trace ended | + +### When conformance fails + +Rerun with the printed seed to reproduce, then decide which side is wrong: + +- If the implementation's behavior is intended or PROTOCOL.md allows it, fix the model. +- If the implementation breaks the protocol, add a scenario that reproduces the bug to `river_test.qnt` and an entry to `KNOWN_BUGS` in `conformance.test.ts`. Random traces then stop just before the bug's trigger, so they keep finding other divergences. Once the bug is fixed, its scenario stops reproducing, and the suite fails until the entry is removed. + +## Bugs found + +The model found two implementation bugs. Both are fixed, and their scenarios stay as regression tests: + +- `invalidHandshakeResponseTest`: an undecodable handshake response made `ClientTransport` throw from the connection's data listener instead of tearing the session down, because `onInvalidHandshake` deleted the `SessionConnecting` state the handshake had already consumed. +- `serverCloseDuringHandshakeTest`: `ServerTransport.close()` left connections that were still handshaking open. One that completed afterwards created a session on the closed transport that kept sending heartbeats while dropping every message. + +One deviation from PROTOCOL.md is still open (`serverClosesAfterClientCancelTest`): the server answers a client's cancel of a stream or subscription with a `ControlClose`, although a cancel is an immediate full close. The model follows the implementation here so the conformance suite stays green, and `quint run spec/river.qnt --invariant cancelIsFinal` finds the violation in seconds. + +Exactly-once delivery holds within a server process, not across restarts (`serverRestartBeforeFirstReplyReplaysTest`). If the server restarts before the client hears anything from it, the client's reconnect looks like a brand-new session because both sequence numbers are still 0. The new server accepts it, and the replayed call runs a second time. + +## Limits + +- `quint run` samples traces; it does not prove the invariants. Bounded model checking with Apalache (`quint verify`) does not currently work, because Quint's JSON encoding of this model exceeds Apalache's 20 MB input limit. +- The configuration is small: three streams with up to two writes each. Timer durations are distinct primes (backoff 23, heartbeat 97, connection timeout 113, handshake timeout 139, grace 401) so that different kinds of timer rarely land on the same instant, and the harness passes the same values to the implementation. diff --git a/spec/river.qnt b/spec/river.qnt new file mode 100644 index 00000000..23ef7a0e --- /dev/null +++ b/spec/river.qnt @@ -0,0 +1,1728 @@ +// -*- mode: Bluespec; -*- + +/// Executable model of the River protocol (PROTOCOL.md, v2.0). +/// +/// One client transport and one server transport talk over a network that can +/// delay, drop, and corrupt frames, break connections, and deliver close events +/// late. The server can restart (losing all state) and the client can hard +/// disconnect. Above the session layer, the model runs the four procedure types +/// with their close, cancel, and teardown rules. +/// +/// Timers carry explicit deadlines and creation order, mirroring how the +/// TypeScript transports schedule them, so every trace this model produces can +/// be replayed step by step against the real implementation under fake timers. +/// `__tests__/conformance` does exactly that: the model is both the protocol +/// specification checked by `quint run` and the oracle for the implementation. +module river { + ////////////////////////////////////////////////////////////////////////////// + // Types + ////////////////////////////////////////////////////////////////////////////// + + type Option[a] = Some(a) | None + + type Cfg = { + grace: int, + connectTimeout: int, + handshakeTimeout: int, + backoff: int, + heartbeat: int, + heartbeatsUntilDead: int, + maxStreams: int, + maxWrites: int, + } + + /// A pending timer. Timers due at the same instant fire in creation order. + type Timer = { at: int, id: int } + + type ProcType = PRpc | PStream | PUpload | PSubscription + + /// A value pushed into a Readable. + type Res = ROk(int) | RErr(str) + + /// Payloads of sequenced transport messages ("Lifetime of streams"). + type Body = + // AckBit heartbeat + | Heartbeat + // StreamOpenBit, plus StreamClosedBit for rpc and subscription + | SInit({ sid: int, pt: ProcType, close: bool }) + // client request data, no control flags + | SData({ sid: int, v: int }) + // server Ok result, StreamClosedBit for rpc and upload + | SResult({ sid: int, v: int, close: bool }) + // ControlClose with StreamClosedBit, either direction + | SClose(int) + // StreamCancelBit with a ProtocolError, either direction + | SCancel({ sid: int, code: str }) + + /// `sess` is bookkeeping only: the session incarnation that sent the message. + type Msg = { seq: int, ack: int, body: Body, sess: int } + + type HsReqFrame = { sess: int, nextExpectedSeq: int, nextSentSeq: int } + type HsRespFrame = { ok: bool, sess: int, code: str } + + type Frame = HsReq(HsReqFrame) | HsResp(HsRespFrame) | Data(Msg) + + /// A wire connection. Once closed (by either side or by the network), later + /// sends are discarded, like WebSocket.send on a closing socket. Frames + /// already in flight may still arrive until that side's close event. + type Conn = { + toServer: List[Frame], + toClient: List[Frame], + closed: bool, + clientEv: bool, + serverEv: bool, + } + + /// Client session states; the dial or connection each one is waiting on. + type CState = CNoConn | CBackingOff | CConnecting(int) | CHandshaking(int) | CConnected(int) + + type ClientSession = { + sess: int, + st: CState, + seq: int, + ack: int, + seqSent: int, + buf: List[Msg], + grace: Option[Timer], + // backoff, connection timeout, or handshake timeout depending on `st` + stTimer: Option[Timer], + wd: Option[Timer], + lastInbound: int, + } + + type ClientT = { + session: Option[ClientSession], + // LeakyBucketRateLimit budget consumed; never restored in this configuration + attempts: int, + // the budget restore interval is pending + restoreActive: bool, + } + + /// A server connection in WaitingForHandshake. + type Pending = { hs: Timer, gotHandshake: bool } + + type SState = SNoConn | SConnected(int) + + type ServerSession = { + sess: int, + st: SState, + seq: int, + ack: int, + seqSent: int, + buf: List[Msg], + grace: Option[Timer], + wd: Option[Timer], + hb: Option[Timer], + lastInbound: int, + } + + type ServerT = { + pending: int -> Pending, + session: Option[ServerSession], + // the router's cancelled-stream tombstones for this client + tombstones: Set[int], + epoch: int, + // ServerTransport.close() was called; the process keeps running + closed: bool, + } + + /// Client half of a procedure stream (router/client.ts). + type CStream = { + pt: ProcType, + sess: int, + w: bool, + r: bool, + clean: bool, + listening: bool, + aborted: bool, + // upload only: finalize() was called, so its result is observable + finalized: bool, + results: List[Res], + written: List[int], + gotCancel: bool, + sentClose: bool, + } + + /// Server half of a procedure stream (router/server.ts). + type SStream = { + pt: ProcType, + sess: int, + r: bool, + w: bool, + clean: bool, + inMap: bool, + handlerDone: bool, + // handler invocations for this stream id in this server process + runs: int, + values: List[Res], + written: List[int], + gotCancel: bool, + sentClose: bool, + } + + /// Observations the invariants and the conformance harness read. + type Obs = { + // protocolError events, by type + cErrs: List[str], + sErrs: List[str], + // out-of-order receipts (each logs an invariant-violation) + cOoo: int, + sOoo: int, + // why the server rejected handshakes + rejections: List[str], + crossSession: bool, + ackBeyondSent: bool, + sendOrder: bool, + sentAfterCancel: bool, + sentAfterClose: bool, + } + + type Ids = { sess: int, conn: int, dial: int, stream: int, timer: int } + + type State = { + cfg: Cfg, + now: int, + // inside a timer callback, where a zero delay schedules one tick later + inTimer: bool, + ids: Ids, + client: ClientT, + server: ServerT, + conns: int -> Conn, + dials: Set[int], + cStreams: int -> CStream, + sStreams: int -> SStream, + obs: Obs, + } + + type TimerRef = + | TClientGrace + | TClientState + | TClientWd + | TPendingHs(int) + | TServerGrace + | TServerWd + | TServerHb + + type Action = + | AInit + | AInvoke({ sid: int, pt: ProcType }) + | AWrite({ sid: int, v: int }) + | AClose(int) + | AFinalize(int) + | ACancel(int) + | ARespond({ sid: int, v: int }) + | ASWrite({ sid: int, v: int }) + | ASClose(int) + | ASCancel(int) + | AThrow(int) + | ADeliver({ conn: int, toServer: bool }) + | ADrop({ conn: int, toServer: bool }) + | ABreak(int) + | ACloseEvent({ conn: int, server: bool }) + | AGarbage({ conn: int, server: bool }) + | ADialOk(int) + | ADialFail(int) + | ATick(int) + | AFire(TimerRef) + | ARestart + | AServerClose + | AHardDisconnect + + ////////////////////////////////////////////////////////////////////////////// + // Configuration + ////////////////////////////////////////////////////////////////////////////// + + /// Distinct, mostly prime durations keep timer ties rare. The grace period + /// exceeds connectTimeout + handshakeTimeout, as SessionOptions recommends. + pure val CFG: Cfg = { + grace: 401, + connectTimeout: 113, + handshakeTimeout: 139, + backoff: 23, + heartbeat: 97, + heartbeatsUntilDead: 2, + maxStreams: 3, + maxWrites: 2, + } + + pure val TICKS = Set(1, 7, 29, 61) + + pure val SESSION_STATE_MISMATCH = "SESSION_STATE_MISMATCH" + pure val HANDSHAKE_FAILED = "handshake_failed" + pure val INVALID_MESSAGE = "invalid_message" + + ////////////////////////////////////////////////////////////////////////////// + // Helpers + ////////////////////////////////////////////////////////////////////////////// + + pure def max(a: int, b: int): int = if (a > b) a else b + + pure def isSomeTimer(o: Option[Timer]): bool = match o { + | Some(_) => true + | None => false + } + + pure def removeKey(m: int -> Pending, k: int): int -> Pending = + m.keys().exclude(Set(k)).mapBy(x => m.get(x)) + + /// Schedules a timer. Delays clamp at zero, and like the fake clock the + /// conformance harness uses, a zero delay inside a timer callback lands one + /// tick later. `id` is the scheduling order that breaks ties between timers + /// due at the same instant. + pure def allocTimer(s: State, at: int): { s: State, t: Timer } = { + val delay = max(0, at - s.now) + val effective = if (delay == 0 and s.inTimer) 1 else delay + { + s: { ...s, ids: { ...s.ids, timer: s.ids.timer + 1 } }, + t: { at: s.now + effective, id: s.ids.timer }, + } + } + + /// An interval re-arms by its period and, like a freshly scheduled timer, + /// takes the latest scheduling order. + pure def rearmInterval(s: State, t: Timer): { s: State, t: Timer } = { + s: { ...s, ids: { ...s.ids, timer: s.ids.timer + 1 } }, + t: { at: t.at + s.cfg.heartbeat, id: s.ids.timer }, + } + + pure def setClient(s: State, cs: Option[ClientSession]): State = + { ...s, client: { ...s.client, session: cs } } + + pure def setServer(s: State, ss: Option[ServerSession]): State = + { ...s, server: { ...s.server, session: ss } } + + pure def setCStream(s: State, sid: int, c: CStream): State = + { ...s, cStreams: s.cStreams.set(sid, c) } + + pure def setSStream(s: State, sid: int, x: SStream): State = + { ...s, sStreams: s.sStreams.set(sid, x) } + + pure def addCErr(s: State, e: str): State = + { ...s, obs: { ...s.obs, cErrs: s.obs.cErrs.append(e) } } + + pure def addSErr(s: State, e: str): State = + { ...s, obs: { ...s.obs, sErrs: s.obs.sErrs.append(e) } } + + pure def graceAt(o: Option[Timer], fallback: int): int = match o { + | Some(t) => t.at + | None => fallback + } + + /// IdentifiedSession.nextSeq: the first seq a reconnect would (re)send. + pure def nextSeq(buf: List[Msg], seq: int): int = + if (buf.length() > 0) buf[0].seq else seq + + pure def bodySid(b: Body): int = match b { + | Heartbeat => -1 + | SInit(x) => x.sid + | SData(x) => x.sid + | SResult(x) => x.sid + | SClose(x) => x + | SCancel(x) => x.sid + } + + pure def isCancelBody(b: Body): bool = match b { + | SCancel(_) => true + | _ => false + } + + pure def closesWithInit(pt: ProcType): bool = pt == PRpc or pt == PSubscription + + pure def closesWithResponse(pt: ProcType): bool = pt == PRpc or pt == PUpload + + pure def acceptsRequests(pt: ProcType): bool = pt == PStream or pt == PUpload + + pure def oks(l: List[Res]): List[int] = + l.foldl([], (acc, r) => match r { + | ROk(v) => acc.append(v) + | RErr(_) => acc + }) + + pure def isPrefix(a: List[int], b: List[int]): bool = + a.length() <= b.length() and a.indices().forall(i => a[i] == b[i]) + + pure def bufHas(buf: List[Msg], k: int): bool = + buf.foldl(false, (acc, m) => acc or m.seq == k) + + pure def bufCovers(buf: List[Msg], lo: int, hi: int): bool = + lo >= hi or range(lo, hi).foldl(true, (acc, k) => acc and bufHas(buf, k)) + + ////////////////////////////////////////////////////////////////////////////// + // Network + ////////////////////////////////////////////////////////////////////////////// + + pure def push(s: State, c: int, toServer: bool, f: Frame): State = { + val cn = s.conns.get(c) + if (cn.closed) s + else if (toServer) { ...s, conns: s.conns.set(c, { ...cn, toServer: cn.toServer.append(f) }) } + else { ...s, conns: s.conns.set(c, { ...cn, toClient: cn.toClient.append(f) }) } + } + + pure def closeConn(s: State, c: int): State = + { ...s, conns: s.conns.set(c, { ...s.conns.get(c), closed: true }) } + + ////////////////////////////////////////////////////////////////////////////// + // Session layer: sending + ////////////////////////////////////////////////////////////////////////////// + + /// SessionConnected.send / IdentifiedSession.send on the client: every + /// message gets the next seq and stays buffered until acknowledged. + pure def clientSend(s: State, body: Body): State = match s.client.session { + | None => s + | Some(cs) => { + val m = { seq: cs.seq, ack: cs.ack, body: body, sess: cs.sess } + val cs1 = { ...cs, seq: cs.seq + 1, buf: cs.buf.append(m) } + match cs.st { + | CConnected(c) => { + val s1 = if (m.seq > cs.seqSent + 1) { ...s, obs: { ...s.obs, sendOrder: true } } else s + setClient(push(s1, c, true, Data(m)), Some({ ...cs1, seqSent: m.seq })) + } + | _ => setClient(s, Some(cs1)) + } + } + } + + pure def serverSend(s: State, body: Body): State = match s.server.session { + | None => s + | Some(ss) => { + val m = { seq: ss.seq, ack: ss.ack, body: body, sess: ss.sess } + val ss1 = { ...ss, seq: ss.seq + 1, buf: ss.buf.append(m) } + match ss.st { + | SConnected(c) => { + val s1 = if (m.seq > ss.seqSent + 1) { ...s, obs: { ...s.obs, sendOrder: true } } else s + setServer(push(s1, c, false, Data(m)), Some({ ...ss1, seqSent: m.seq })) + } + | SNoConn => setServer(s, Some(ss1)) + } + } + } + + pure def resendStep(acc: { s: State, seqSent: int }, m: Msg, c: int, toServer: bool): { s: State, seqSent: int } = { + val s1 = if (m.seq > acc.seqSent + 1) { ...acc.s, obs: { ...acc.s.obs, sendOrder: true } } else acc.s + { s: push(s1, c, toServer, Data(m)), seqSent: m.seq } + } + + /// SessionConnected.sendBufferedMessages after a (re)handshake. + pure def clientSendBuffered(s: State): State = match s.client.session { + | Some(cs) => match cs.st { + | CConnected(c) => { + val r = cs.buf.foldl({ s: s, seqSent: cs.seqSent }, (acc, m) => resendStep(acc, m, c, true)) + setClient(r.s, Some({ ...cs, seqSent: r.seqSent })) + } + | _ => s + } + | None => s + } + + pure def serverSendBuffered(s: State): State = match s.server.session { + | Some(ss) => match ss.st { + | SConnected(c) => { + val r = ss.buf.foldl({ s: s, seqSent: ss.seqSent }, (acc, m) => resendStep(acc, m, c, false)) + setServer(r.s, Some({ ...ss, seqSent: r.seqSent })) + } + | SNoConn => s + } + | None => s + } + + ////////////////////////////////////////////////////////////////////////////// + // Router: client side (router/client.ts) + ////////////////////////////////////////////////////////////////////////////// + + pure def clientStreamSend(s: State, sid: int, body: Body, isClose: bool): State = { + val c = s.cStreams.get(sid) + val o1 = if (c.gotCancel) { ...s.obs, sentAfterCancel: true } else s.obs + val o2 = if (c.sentClose and not(isCancelBody(body))) { ...o1, sentAfterClose: true } else o1 + val s1 = { ...s, obs: o2 } + val s2 = if (isClose) setCStream(s1, sid, { ...c, sentClose: true }) else s1 + clientSend(s2, body) + } + + /// Readable closes; listeners are removed once both halves are closed. + pure def cCloseReadable(c: CStream): CStream = + { ...c, r: false, listening: if (not(c.w)) false else c.listening } + + /// onSessionStatus('closing') for one stream: UNEXPECTED_DISCONNECT. + pure def cStreamOnClosing(s: State, sid: int, sess: int): State = { + val c = s.cStreams.get(sid) + if (not(c.listening) or c.sess != sess) s + else { + val res = if (c.r) c.results.append(RErr("UNEXPECTED_DISCONNECT")) else c.results + setCStream(s, sid, { ...c, clean: false, r: false, w: false, listening: false, results: res }) + } + } + + pure def clientRouterRecv(s: State, b: Body): State = { + val sid = bodySid(b) + if (not(s.cStreams.keys().contains(sid))) s + else { + val c = s.cStreams.get(sid) + if (not(c.listening)) s + else match b { + | SCancel(x) => { + val res = if (c.r) c.results.append(RErr(x.code)) else c.results + setCStream(s, sid, { ...c, clean: false, gotCancel: true, r: false, w: false, listening: false, results: res }) + } + | SResult(x) => + if (not(c.r)) s + else { + val c1 = { ...c, results: c.results.append(ROk(x.v)) } + setCStream(s, sid, if (x.close) cCloseReadable(c1) else c1) + } + | SClose(_) => if (not(c.r)) s else setCStream(s, sid, cCloseReadable(c)) + | _ => s + } + } + } + + ////////////////////////////////////////////////////////////////////////////// + // Router: server side (router/server.ts) + ////////////////////////////////////////////////////////////////////////////// + + pure def serverStreamSend(s: State, sid: int, body: Body, isClose: bool): State = { + val x = s.sStreams.get(sid) + val o1 = if (x.gotCancel) { ...s.obs, sentAfterCancel: true } else s.obs + val o2 = if (x.sentClose and not(isCancelBody(body))) { ...o1, sentAfterClose: true } else o1 + val s1 = { ...s, obs: o2 } + val s2 = if (isClose) setSStream(s1, sid, { ...x, sentClose: true }) else s1 + serverSend(s2, body) + } + + pure def sCloseReadable(x: SStream): SStream = + { ...x, r: false, inMap: if (not(x.w)) false else x.inMap } + + /// resWritable.close(): stream and subscription announce the close unless + /// the stream ended abruptly; rpc and upload already closed with the result. + pure def serverCloseWritable(s: State, sid: int): State = { + val x = s.sStreams.get(sid) + if (not(x.w)) s + else { + val s1 = setSStream(s, sid, { ...x, w: false }) + val s2 = if (not(closesWithResponse(x.pt)) and x.clean) serverStreamSend(s1, sid, SClose(sid), true) else s1 + val x2 = s2.sStreams.get(sid) + if (not(x2.r)) setSStream(s2, sid, { ...x2, inMap: false }) else s2 + } + } + + /// onServerCancel: abrupt full close plus a cancel to the client. + pure def serverOnCancel(s: State, sid: int, code: str): State = { + val x = s.sStreams.get(sid) + if (not(x.r) and not(x.w)) s + else { + val x1 = { ...x, clean: false } + val x2 = if (x1.r) sCloseReadable({ ...x1, values: x1.values.append(RErr(code)) }) else x1 + val s1 = serverCloseWritable(setSStream(s, sid, x2), sid) + val s2 = { ...s1, server: { ...s1.server, tombstones: s1.server.tombstones.union(Set(sid)) } } + serverStreamSend(s2, sid, SCancel({ sid: sid, code: code }), false) + } + } + + pure def serverStreamHandle(s: State, sid: int, b: Body): State = { + val x = s.sStreams.get(sid) + match b { + | SCancel(y) => { + val x1 = { ...x, gotCancel: true } + val x2 = if (x1.r) sCloseReadable({ ...x1, values: x1.values.append(RErr(y.code)) }) else x1 + serverCloseWritable(setSStream(s, sid, x2), sid) + } + | SData(y) => + if (x.r and acceptsRequests(x.pt)) setSStream(s, sid, { ...x, values: x.values.append(ROk(y.v)) }) + else serverOnCancel(s, sid, "INVALID_REQUEST") + | SClose(_) => + if (x.r) setSStream(s, sid, sCloseReadable(x)) else serverOnCancel(s, sid, "INVALID_REQUEST") + | _ => serverOnCancel(s, sid, "INVALID_REQUEST") + } + } + + pure def serverOpenStream(s: State, sid: int, pt: ProcType, close: bool): State = { + val sess = match s.server.session { + | Some(ss) => ss.sess + | None => 0 + } + // a stream id can open again in the same process after its session ends + val runs = if (s.sStreams.keys().contains(sid)) s.sStreams.get(sid).runs else 0 + val x = { + pt: pt, + sess: sess, + r: not(close), + w: true, + clean: true, + inMap: true, + handlerDone: false, + runs: runs + 1, + values: [], + written: [], + gotCancel: false, + sentClose: false, + } + { ...s, sStreams: s.sStreams.put(sid, x) } + } + + pure def serverRouterRecv(s: State, b: Body): State = { + val sid = bodySid(b) + val known = s.sStreams.keys().contains(sid) and s.sStreams.get(sid).inMap + if (known) serverStreamHandle(s, sid, b) + else if (s.server.tombstones.contains(sid)) s + else match b { + | SInit(x) => serverOpenStream(s, x.sid, x.pt, x.close) + | _ => { + // validateNewProcStream: no StreamOpenBit on an unknown stream + val s1 = { ...s, server: { ...s.server, tombstones: s.server.tombstones.union(Set(sid)) } } + serverSend(s1, SCancel({ sid: sid, code: "INVALID_REQUEST" })) + } + } + } + + pure def sStreamOnClosing(s: State, sid: int): State = { + val x = s.sStreams.get(sid) + if (not(x.inMap)) s + else { + val v = if (x.r) x.values.append(RErr("UNEXPECTED_DISCONNECT")) else x.values + setSStream(s, sid, { ...x, clean: false, r: false, w: false, inMap: false, values: v }) + } + } + + ////////////////////////////////////////////////////////////////////////////// + // Session lifecycle: client (transport/client.ts) + ////////////////////////////////////////////////////////////////////////////// + + pure def clientCreateSession(s: State): State = { + val g = allocTimer(s, s.now + s.cfg.grace) + val s1 = { ...g.s, ids: { ...g.s.ids, sess: g.s.ids.sess + 1 } } + setClient(s1, Some({ + sess: s.ids.sess, + st: CNoConn, + seq: 0, + ack: 0, + seqSent: 0, + buf: [], + grace: Some(g.t), + stTimer: None, + wd: None, + lastInbound: s.now, + })) + } + + /// ClientTransport.connect: create a session if needed, then back off. + pure def clientConnect(s: State): State = { + val s1 = match s.client.session { + | Some(_) => s + | None => clientCreateSession(s) + } + match s1.client.session { + | Some(cs) => + if (cs.st == CNoConn) { + val backoff = if (s1.client.attempts == 0) 0 else s1.cfg.backoff + val s2 = { ...s1, client: { ...s1.client, attempts: s1.client.attempts + 1, restoreActive: false } } + // SessionBackingOff re-arms the carried grace deadline, then the backoff + val g = allocTimer(s2, max(s2.now, graceAt(cs.grace, s2.now))) + val b = allocTimer(g.s, g.s.now + backoff) + setClient(b.s, Some({ ...cs, st: CBackingOff, grace: Some(g.t), stTimer: Some(b.t) })) + } else s1 + | None => s1 + } + } + + /// Transport.deleteSession on the client: every stream bound to the session + /// resolves with UNEXPECTED_DISCONNECT, then the session closes its connection. + pure def clientDeleteSession(s: State): State = match s.client.session { + | None => s + | Some(cs) => { + val s1 = s.cStreams.keys().fold(s, (acc, sid) => cStreamOnClosing(acc, sid, cs.sess)) + val s2 = match cs.st { + | CHandshaking(c) => closeConn(s1, c) + | CConnected(c) => closeConn(s1, c) + | _ => s1 + } + setClient(s2, None) + } + } + + /// onConnClosed: Handshaking or Connected to NoConnection, then reconnect. + pure def clientConnLost(s: State): State = match s.client.session { + | Some(cs) => match cs.st { + | CHandshaking(c) => { + val s1 = closeConn(s, c) + val g = allocTimer(s1, max(s1.now, graceAt(cs.grace, s1.now))) + clientConnect(setClient(g.s, Some({ ...cs, st: CNoConn, grace: Some(g.t), stTimer: None }))) + } + | CConnected(c) => { + val s1 = closeConn(s, c) + val g = allocTimer(s1, s1.now + s1.cfg.grace) + clientConnect(setClient(g.s, Some({ ...cs, st: CNoConn, grace: Some(g.t), stTimer: None, wd: None }))) + } + | _ => s + } + | None => s + } + + /// onConnectingFailed: dial failure or connection timeout. + pure def clientConnectingFailed(s: State): State = match s.client.session { + | Some(cs) => match cs.st { + | CConnecting(_) => { + val g = allocTimer(s, max(s.now, graceAt(cs.grace, s.now))) + clientConnect(setClient(g.s, Some({ ...cs, st: CNoConn, grace: Some(g.t), stTimer: None }))) + } + | _ => s + } + | None => s + } + + /// onBackoffFinished: dial, then wait in Connecting. + pure def clientBackoffDone(s: State): State = match s.client.session { + | Some(cs) => { + val d = s.ids.dial + val s1 = { ...s, ids: { ...s.ids, dial: d + 1 }, dials: s.dials.union(Set(d)) } + val g = allocTimer(s1, max(s1.now, graceAt(cs.grace, s1.now))) + val t = allocTimer(g.s, g.s.now + g.s.cfg.connectTimeout) + setClient(t.s, Some({ ...cs, st: CConnecting(d), grace: Some(g.t), stTimer: Some(t.t) })) + } + | None => s + } + + pure def clientOnHsResp(s: State, r: HsRespFrame): State = match s.client.session { + | Some(cs) => + if (not(r.ok)) { + val s1 = clientDeleteSession(s) + if (r.code == SESSION_STATE_MISMATCH) clientConnect(s1) else addCErr(s1, HANDSHAKE_FAILED) + } else if (r.sess != cs.sess) clientDeleteSession(s) + else match cs.st { + | CHandshaking(c) => { + val w = allocTimer(s, s.now + s.cfg.heartbeat) + val s1 = setClient(w.s, Some({ ...cs, st: CConnected(c), grace: None, stTimer: None, wd: Some(w.t), lastInbound: w.s.now })) + val s2 = clientSendBuffered(s1) + { ...s2, client: { ...s2.client, restoreActive: true } } + } + | _ => s + } + | None => s + } + + /// SessionConnected.onMessageData on the client. + pure def clientRecvData(s: State, m: Msg): State = match s.client.session { + | Some(cs) => match cs.st { + | CConnected(c) => + if (m.seq < cs.ack) s + else if (m.seq > cs.ack) closeConn({ ...s, obs: { ...s.obs, cOoo: s.obs.cOoo + 1 } }, c) + else { + val cs1 = { ...cs, buf: cs.buf.select(x => x.seq >= m.ack), ack: m.seq + 1, lastInbound: s.now } + val o1 = if (m.sess != cs.sess) { ...s.obs, crossSession: true } else s.obs + val o2 = if (m.ack > cs.seq) { ...o1, ackBeyondSent: true } else o1 + val s1 = setClient({ ...s, obs: o2 }, Some(cs1)) + match m.body { + // passive heartbeating: echo every heartbeat + | Heartbeat => clientSend(s1, Heartbeat) + | _ => clientRouterRecv(s1, m.body) + } + } + | _ => s + } + | None => s + } + + ////////////////////////////////////////////////////////////////////////////// + // Session lifecycle: server (transport/server.ts) + ////////////////////////////////////////////////////////////////////////////// + + pure def deletePending(s: State, c: int): State = { + val s1 = closeConn(s, c) + { ...s1, server: { ...s1.server, pending: removeKey(s1.server.pending, c) } } + } + + /// Transport.deleteSession on the server: streams see UNEXPECTED_DISCONNECT, + /// tombstones go, and the session closes its connection. + pure def serverDeleteSession(s: State): State = match s.server.session { + | None => s + | Some(ss) => { + val s1 = s.sStreams.keys().fold(s, (acc, sid) => sStreamOnClosing(acc, sid)) + val s2 = { ...s1, server: { ...s1.server, tombstones: Set() } } + val s3 = match ss.st { + | SConnected(c) => closeConn(s2, c) + | SNoConn => s2 + } + setServer(s3, None) + } + } + + /// ConnectedToNoConnection on the server. + pure def serverConnLost(s: State): State = match s.server.session { + | Some(ss) => match ss.st { + | SConnected(c) => { + val s1 = closeConn(s, c) + val g = allocTimer(s1, s1.now + s1.cfg.grace) + setServer(g.s, Some({ ...ss, st: SNoConn, grace: Some(g.t), wd: None, hb: None })) + } + | SNoConn => s + } + | None => s + } + + pure def serverReject(s: State, c: int, code: str, cause: str): State = { + val s1 = push(s, c, false, HsResp({ ok: false, sess: 0, code: code })) + val s2 = addSErr({ ...s1, obs: { ...s1.obs, rejections: s1.obs.rejections.append(cause) } }, HANDSHAKE_FAILED) + deletePending(s2, c) + } + + pure def freshServerSession(sess: int): ServerSession = { + sess: sess, + st: SNoConn, + seq: 0, + ack: 0, + seqSent: 0, + buf: [], + grace: None, + wd: None, + hb: None, + lastInbound: 0, + } + + pure def serverAccept(s: State, c: int, sess: int, inherit: bool): State = { + val s1 = push(s, c, false, HsResp({ ok: true, sess: sess, code: "" })) + val s2 = { ...s1, server: { ...s1.server, pending: removeKey(s1.server.pending, c) } } + val w = allocTimer(s2, s2.now + s2.cfg.heartbeat) + val base = match s2.server.session { + | Some(old) => if (inherit) old else freshServerSession(sess) + | None => freshServerSession(sess) + } + val ss = { ...base, sess: sess, st: SConnected(c), grace: None, wd: Some(w.t), hb: None, lastInbound: s2.now } + val s3 = serverSendBuffered(setServer(w.s, Some(ss))) + val h = allocTimer(s3, s3.now + s3.cfg.heartbeat) + match h.s.server.session { + | Some(ss3) => setServer(h.s, Some({ ...ss3, hb: Some(h.t) })) + | None => h.s + } + } + + pure def serverAcceptOrUnknown(s: State, c: int, h: HsReqFrame): State = + if (h.nextSentSeq > 0 or h.nextExpectedSeq > 0) serverReject(s, c, SESSION_STATE_MISMATCH, "UNKNOWN_SESSION") + else serverAccept(s, c, h.sess, false) + + /// onHandshakeRequest: new session, unknown session, transparent reconnect, + /// or hard reconnect. + pure def serverOnHsReq(s: State, c: int, h: HsReqFrame): State = { + val p = s.server.pending.get(c) + if (p.gotHandshake) deletePending(s, c) + else { + val s0 = { ...s, server: { ...s.server, pending: s.server.pending.set(c, { ...p, gotHandshake: true }) } } + match s0.server.session { + | Some(old) => + if (old.sess == h.sess) { + if (h.nextSentSeq > old.ack) serverReject(s0, c, SESSION_STATE_MISMATCH, "FUTURE_CLIENT") + else if (nextSeq(old.buf, old.seq) > h.nextExpectedSeq) serverReject(s0, c, SESSION_STATE_MISMATCH, "FUTURE_SERVER") + else serverAccept(serverConnLost(s0), c, h.sess, true) + } else serverAcceptOrUnknown(serverDeleteSession(s0), c, h) + | None => serverAcceptOrUnknown(s0, c, h) + } + } + } + + pure def serverRecvData(s: State, m: Msg): State = match s.server.session { + | Some(ss) => match ss.st { + | SConnected(c) => + if (m.seq < ss.ack) s + else if (m.seq > ss.ack) closeConn({ ...s, obs: { ...s.obs, sOoo: s.obs.sOoo + 1 } }, c) + else { + val ss1 = { ...ss, buf: ss.buf.select(x => x.seq >= m.ack), ack: m.seq + 1, lastInbound: s.now } + val o1 = if (m.sess != ss.sess) { ...s.obs, crossSession: true } else s.obs + val o2 = if (m.ack > ss.seq) { ...o1, ackBeyondSent: true } else o1 + val s1 = setServer({ ...s, obs: o2 }, Some(ss1)) + match m.body { + // the server heartbeats actively, so it does not echo + | Heartbeat => s1 + | _ => serverRouterRecv(s1, m.body) + } + } + | SNoConn => s + } + | None => s + } + + ////////////////////////////////////////////////////////////////////////////// + // Frames, close events, garbage + ////////////////////////////////////////////////////////////////////////////// + + pure def serverOnFrame(s: State, c: int, f: Frame): State = + if (s.server.pending.keys().contains(c)) match f { + | HsReq(h) => serverOnHsReq(s, c, h) + | _ => serverReject(s, c, "MALFORMED_HANDSHAKE", "MALFORMED") + } + else match s.server.session { + | Some(ss) => + if (ss.st == SConnected(c)) match f { + | Data(m) => serverRecvData(s, m) + | _ => s + } else s + | None => s + } + + pure def clientOnFrame(s: State, c: int, f: Frame): State = match s.client.session { + | Some(cs) => match cs.st { + | CHandshaking(x) => + if (x != c) s + else match f { + | HsResp(r) => clientOnHsResp(s, r) + | _ => clientDeleteSession(s) + } + | CConnected(x) => + if (x != c) s + else match f { + | Data(m) => clientRecvData(s, m) + | _ => s + } + | _ => s + } + | None => s + } + + pure def deliver(s: State, c: int, toServer: bool): State = { + val cn = s.conns.get(c) + if (toServer) serverOnFrame({ ...s, conns: s.conns.set(c, { ...cn, toServer: cn.toServer.tail() }) }, c, cn.toServer.head()) + else clientOnFrame({ ...s, conns: s.conns.set(c, { ...cn, toClient: cn.toClient.tail() }) }, c, cn.toClient.head()) + } + + pure def drop(s: State, c: int, toServer: bool): State = { + val cn = s.conns.get(c) + if (toServer) { ...s, conns: s.conns.set(c, { ...cn, toServer: cn.toServer.tail() }) } + else { ...s, conns: s.conns.set(c, { ...cn, toClient: cn.toClient.tail() }) } + } + + /// A close event reaches one side; frames still headed there are lost. + pure def closeEvent(s: State, c: int, server: bool): State = { + val cn = s.conns.get(c) + if (server) { + val s1 = { ...s, conns: s.conns.set(c, { ...cn, serverEv: true, toServer: [] }) } + if (s1.server.pending.keys().contains(c)) deletePending(s1, c) + else match s1.server.session { + | Some(ss) => if (ss.st == SConnected(c)) serverConnLost(s1) else s1 + | None => s1 + } + } else { + val s1 = { ...s, conns: s.conns.set(c, { ...cn, clientEv: true, toClient: [] }) } + match s1.client.session { + | Some(cs) => match cs.st { + | CHandshaking(x) => if (x == c) clientConnLost(s1) else s1 + | CConnected(x) => if (x == c) clientConnLost(s1) else s1 + | _ => s1 + } + | None => s1 + } + } + } + + /// An undecodable frame. PROTOCOL.md: an invalid handshake or an invalid + /// message destroys the session (the server drops a pending connection). + pure def garbage(s: State, c: int, server: bool): State = + if (server) { + if (s.server.pending.keys().contains(c)) deletePending(addSErr(s, HANDSHAKE_FAILED), c) + else match s.server.session { + | Some(ss) => if (ss.st == SConnected(c)) serverDeleteSession(addSErr(s, INVALID_MESSAGE)) else s + | None => s + } + } else match s.client.session { + | Some(cs) => match cs.st { + | CHandshaking(x) => if (x == c) clientDeleteSession(addCErr(s, HANDSHAKE_FAILED)) else s + | CConnected(x) => if (x == c) clientDeleteSession(addCErr(s, INVALID_MESSAGE)) else s + | _ => s + } + | None => s + } + + /// A successful dial: the server accepts first, then the client either starts + /// handshaking or, if it already gave up on this dial, closes the connection. + pure def dialOk(s: State, d: int): State = { + val c = s.ids.conn + val s1 = { + ...s, + ids: { ...s.ids, conn: c + 1 }, + dials: s.dials.exclude(Set(d)), + conns: s.conns.put(c, { toServer: [], toClient: [], closed: false, clientEv: false, serverEv: false }), + } + // a closed server transport ignores new connections + val s2 = if (s1.server.closed) s1 else { + val h = allocTimer(s1, s1.now + s1.cfg.handshakeTimeout) + { ...h.s, server: { ...h.s.server, pending: h.s.server.pending.put(c, { hs: h.t, gotHandshake: false }) } } + } + match s2.client.session { + | Some(cs) => + if (cs.st == CConnecting(d)) { + val g = allocTimer(s2, max(s2.now, graceAt(cs.grace, s2.now))) + val t = allocTimer(g.s, g.s.now + g.s.cfg.handshakeTimeout) + val s3 = setClient(t.s, Some({ ...cs, st: CHandshaking(c), grace: Some(g.t), stTimer: Some(t.t) })) + push(s3, c, true, HsReq({ sess: cs.sess, nextExpectedSeq: cs.ack, nextSentSeq: nextSeq(cs.buf, cs.seq) })) + } else closeConn(s2, c) + | None => closeConn(s2, c) + } + } + + pure def dialFail(s: State, d: int): State = { + val s1 = { ...s, dials: s.dials.exclude(Set(d)) } + match s1.client.session { + | Some(cs) => if (cs.st == CConnecting(d)) clientConnectingFailed(s1) else s1 + | None => s1 + } + } + + /// The server process dies: its side of every connection is gone, frames in + /// flight to it are lost, and it forgets all sessions and streams. + pure def serverRestart(s: State): State = { + val conns1 = s.conns.keys().mapBy(k => { ...s.conns.get(k), closed: true, serverEv: true, toServer: [] }) + { + ...s, + conns: conns1, + server: { pending: Map(), session: None, tombstones: Set(), epoch: s.server.epoch + 1, closed: false }, + sStreams: Map(), + } + } + + /// ServerTransport.close() in a process that keeps running: every session + /// and every connection still waiting for its handshake goes away. + pure def serverShutdown(s: State): State = { + val s1 = serverDeleteSession(s) + val s2 = s1.server.pending.keys().fold(s1, (acc, c) => deletePending(acc, c)) + { ...s2, server: { ...s2.server, closed: true } } + } + + ////////////////////////////////////////////////////////////////////////////// + // Timers + ////////////////////////////////////////////////////////////////////////////// + + pure def optTimer(o: Option[Timer], ref: TimerRef): Set[{ ref: TimerRef, t: Timer }] = match o { + | Some(t) => Set({ ref: ref, t: t }) + | None => Set() + } + + pure def armed(s: State): Set[{ ref: TimerRef, t: Timer }] = { + val c = match s.client.session { + | Some(cs) => optTimer(cs.grace, TClientGrace).union(optTimer(cs.stTimer, TClientState)).union(optTimer(cs.wd, TClientWd)) + | None => Set() + } + val p = s.server.pending.keys().map(k => { ref: TPendingHs(k), t: s.server.pending.get(k).hs }) + val v = match s.server.session { + | Some(ss) => optTimer(ss.grace, TServerGrace).union(optTimer(ss.wd, TServerWd)).union(optTimer(ss.hb, TServerHb)) + | None => Set() + } + c.union(p).union(v) + } + + pure def earlier(a: Timer, b: Timer): bool = a.at < b.at or (a.at == b.at and a.id < b.id) + + pure def nextTimer(s: State): Option[{ ref: TimerRef, t: Timer }] = + armed(s).fold(None, (acc, x) => match acc { + | None => Some(x) + | Some(y) => if (earlier(x.t, y.t)) Some(x) else acc + }) + + /// Pending timers in the implementation, including the retry budget's restore interval. + pure def timerCount(s: State): int = + armed(s).size() + (if (s.client.restoreActive) 1 else 0) + + /// The heartbeat watchdog: an interval that closes the connection once the + /// peer has been silent for heartbeatsUntilDead heartbeats. + pure def watchdogDead(s: State, lastInbound: int): bool = + s.now - lastInbound >= s.cfg.heartbeat * s.cfg.heartbeatsUntilDead + + pure def fire(s0: State, ref: TimerRef, t: Timer): State = { + val after = fireIn({ ...s0, now: t.at, inTimer: true }, ref, t) + { ...after, inTimer: false } + } + + pure def fireIn(s: State, ref: TimerRef, t: Timer): State = { + match ref { + | TClientGrace => clientDeleteSession(s) + | TClientState => match s.client.session { + | Some(cs) => match cs.st { + | CBackingOff => clientBackoffDone(s) + | CConnecting(_) => clientConnectingFailed(s) + | CHandshaking(_) => clientConnLost(s) + | _ => s + } + | None => s + } + | TClientWd => match s.client.session { + | Some(cs) => match cs.st { + | CConnected(c) => { + val r = rearmInterval(s, t) + if (watchdogDead(r.s, cs.lastInbound)) closeConn(setClient(r.s, Some({ ...cs, wd: None })), c) + else setClient(r.s, Some({ ...cs, wd: Some(r.t) })) + } + | _ => s + } + | None => s + } + | TPendingHs(c) => deletePending(s, c) + | TServerGrace => serverDeleteSession(s) + | TServerWd => match s.server.session { + | Some(ss) => match ss.st { + | SConnected(c) => { + val r = rearmInterval(s, t) + if (watchdogDead(r.s, ss.lastInbound)) closeConn(setServer(r.s, Some({ ...ss, wd: None })), c) + else setServer(r.s, Some({ ...ss, wd: Some(r.t) })) + } + | SNoConn => s + } + | None => s + } + | TServerHb => match s.server.session { + | Some(ss) => { + val r = rearmInterval(s, t) + serverSend(setServer(r.s, Some({ ...ss, hb: Some(r.t) })), Heartbeat) + } + | None => s + } + } + } + + ////////////////////////////////////////////////////////////////////////////// + // Application operations + ////////////////////////////////////////////////////////////////////////////// + + /// createClient proxy with connectOnInvoke, then handleProc. + pure def clientInvoke(s: State, pt: ProcType): State = { + val s1 = match s.client.session { + | Some(_) => s + | None => clientConnect(s) + } + match s1.client.session { + | Some(cs) => { + val sid = s1.ids.stream + val cwi = closesWithInit(pt) + val c = { + pt: pt, + sess: cs.sess, + w: true, + r: true, + clean: true, + listening: true, + finalized: false, + aborted: false, + results: [], + written: [], + gotCancel: false, + sentClose: cwi, + } + val s2 = { ...s1, ids: { ...s1.ids, stream: sid + 1 }, cStreams: s1.cStreams.put(sid, c) } + val s3 = clientSend(s2, SInit({ sid: sid, pt: pt, close: cwi })) + if (cwi) setCStream(s3, sid, { ...s3.cStreams.get(sid), w: false }) else s3 + } + | None => s1 + } + } + + pure def clientWrite(s: State, sid: int): State = { + val c = s.cStreams.get(sid) + val v = c.written.length() + 1 + clientStreamSend(setCStream(s, sid, { ...c, written: c.written.append(v) }), sid, SData({ sid: sid, v: v }), false) + } + + pure def clientClose(s: State, sid: int): State = { + val c = s.cStreams.get(sid) + val c1 = { ...c, w: false } + val s1 = setCStream(s, sid, c1) + val s2 = if (c.clean) clientStreamSend(s1, sid, SClose(sid), true) else s1 + val c2 = s2.cStreams.get(sid) + if (not(c2.r)) setCStream(s2, sid, { ...c2, listening: false }) else s2 + } + + /// onClientCancel via the call's AbortSignal. + pure def clientCancel(s: State, sid: int): State = { + val c = s.cStreams.get(sid) + val res = if (c.r) c.results.append(RErr("CANCEL")) else c.results + val c1 = { ...c, aborted: true, clean: false, r: false, w: false, listening: false, results: res } + clientStreamSend(setCStream(s, sid, c1), sid, SCancel({ sid: sid, code: "CANCEL" }), false) + } + + /// rpc/upload handler resolves with Ok(v): the result closes the response. + pure def serverRespond(s: State, sid: int): State = { + val x = { ...s.sStreams.get(sid), handlerDone: true } + if (not(x.w)) setSStream(s, sid, x) + else { + val v = 100 + x.written.length() + 1 + val s1 = setSStream(s, sid, { ...x, written: x.written.append(v) }) + serverCloseWritable(serverStreamSend(s1, sid, SResult({ sid: sid, v: v, close: true }), true), sid) + } + } + + pure def serverWrite(s: State, sid: int): State = { + val x = s.sStreams.get(sid) + val v = 100 + x.written.length() + 1 + serverStreamSend(setSStream(s, sid, { ...x, written: x.written.append(v) }), sid, SResult({ sid: sid, v: v, close: false }), false) + } + + pure def serverThrow(s: State, sid: int): State = + serverOnCancel(setSStream(s, sid, { ...s.sStreams.get(sid), handlerDone: true }), sid, "UNCAUGHT_ERROR") + + ////////////////////////////////////////////////////////////////////////////// + // State machine + ////////////////////////////////////////////////////////////////////////////// + + var st: State + var lastAction: Action + + /// A linear congruential generator that only `step` reads, to make faults + /// rare. The simulator retries nondeterministic picks until an action is + /// enabled, so a guard on a random pick cannot lower an action's frequency; + /// a guard on state it cannot choose can. `stepAll` ignores it. + var rng: int + + pure def nextRng(r: int): int = (r * 1103515245 + 12345) % 2147483648 + + /// True on roughly one step in `n`, from the generator's high bits. + pure def oneIn(r: int, n: int): bool = (r / 65536) % n == 0 + + pure val initState: State = { + cfg: CFG, + now: 0, + inTimer: false, + ids: { sess: 1, conn: 1, dial: 1, stream: 1, timer: 1 }, + client: { session: None, attempts: 0, restoreActive: false }, + server: { pending: Map(), session: None, tombstones: Set(), epoch: 0, closed: false }, + conns: Map(), + dials: Set(), + cStreams: Map(), + sStreams: Map(), + obs: { + cErrs: [], + sErrs: [], + cOoo: 0, + sOoo: 0, + rejections: [], + crossSession: false, + ackBeyondSent: false, + sendOrder: false, + sentAfterCancel: false, + sentAfterClose: false, + }, + } + + action init = { + // each trace gets its own fault schedule + nondet seed = oneOf(1.to(1000000)) + all { + st' = initState, + lastAction' = AInit, + rng' = seed, + } + } + + action invokeAs(pt: ProcType): bool = all { + st.ids.stream <= st.cfg.maxStreams, + st' = clientInvoke(st, pt), + lastAction' = AInvoke({ sid: st.ids.stream, pt: pt }), + rng' = nextRng(rng), + } + + action writeOn(sid: int): bool = all { + st.cStreams.keys().contains(sid), + val c = st.cStreams.get(sid) + all { + acceptsRequests(c.pt), + c.w, + c.written.length() < st.cfg.maxWrites, + st' = clientWrite(st, sid), + lastAction' = AWrite({ sid: sid, v: c.written.length() + 1 }), + rng' = nextRng(rng), + }, + } + + action closeOn(sid: int): bool = all { + st.cStreams.keys().contains(sid), + acceptsRequests(st.cStreams.get(sid).pt), + st.cStreams.get(sid).w, + st' = clientClose(st, sid), + lastAction' = AClose(sid), + rng' = nextRng(rng), + } + + /// An upload's finalize(): closes the writable if it is still open, then + /// awaits the result. Allowed once, whatever state the stream is in. + action finalizeOn(sid: int): bool = all { + st.cStreams.keys().contains(sid), + val c = st.cStreams.get(sid) + all { + c.pt == PUpload, + not(c.finalized), + val s1 = if (c.w) clientClose(st, sid) else st + st' = setCStream(s1, sid, { ...s1.cStreams.get(sid), finalized: true }), + lastAction' = AFinalize(sid), + rng' = nextRng(rng), + }, + } + + action cancelOn(sid: int): bool = all { + st.cStreams.keys().contains(sid), + st.cStreams.get(sid).listening, + not(st.cStreams.get(sid).aborted), + st' = clientCancel(st, sid), + lastAction' = ACancel(sid), + rng' = nextRng(rng), + } + + action respondOn(sid: int): bool = all { + st.sStreams.keys().contains(sid), + closesWithResponse(st.sStreams.get(sid).pt), + not(st.sStreams.get(sid).handlerDone), + st' = serverRespond(st, sid), + lastAction' = ARespond({ sid: sid, v: 100 + st.sStreams.get(sid).written.length() + 1 }), + rng' = nextRng(rng), + } + + action serverWriteOn(sid: int): bool = all { + st.sStreams.keys().contains(sid), + val x = st.sStreams.get(sid) + all { + not(closesWithResponse(x.pt)), + x.w, + x.written.length() < st.cfg.maxWrites, + st' = serverWrite(st, sid), + lastAction' = ASWrite({ sid: sid, v: 100 + x.written.length() + 1 }), + rng' = nextRng(rng), + }, + } + + action serverCloseOn(sid: int): bool = all { + st.sStreams.keys().contains(sid), + not(closesWithResponse(st.sStreams.get(sid).pt)), + st.sStreams.get(sid).w, + st' = serverCloseWritable(st, sid), + lastAction' = ASClose(sid), + rng' = nextRng(rng), + } + + action serverCancelOn(sid: int): bool = all { + st.sStreams.keys().contains(sid), + st.sStreams.get(sid).r or st.sStreams.get(sid).w, + st' = serverOnCancel(st, sid, "CANCEL"), + lastAction' = ASCancel(sid), + rng' = nextRng(rng), + } + + action throwOn(sid: int): bool = all { + st.sStreams.keys().contains(sid), + not(st.sStreams.get(sid).handlerDone), + st' = serverThrow(st, sid), + lastAction' = AThrow(sid), + rng' = nextRng(rng), + } + + action deliverOn(c: int, toServer: bool): bool = all { + st.conns.keys().contains(c), + val cn = st.conns.get(c) + if (toServer) all { cn.toServer.length() > 0, not(cn.serverEv) } + else all { cn.toClient.length() > 0, not(cn.clientEv) }, + st' = deliver(st, c, toServer), + lastAction' = ADeliver({ conn: c, toServer: toServer }), + rng' = nextRng(rng), + } + + action dropOn(c: int, toServer: bool): bool = all { + st.conns.keys().contains(c), + val cn = st.conns.get(c) + if (toServer) cn.toServer.length() > 0 else cn.toClient.length() > 0, + st' = drop(st, c, toServer), + lastAction' = ADrop({ conn: c, toServer: toServer }), + rng' = nextRng(rng), + } + + action breakOn(c: int): bool = all { + st.conns.keys().contains(c), + not(st.conns.get(c).closed), + st' = closeConn(st, c), + lastAction' = ABreak(c), + rng' = nextRng(rng), + } + + action closeEventOn(c: int, server: bool): bool = all { + st.conns.keys().contains(c), + val cn = st.conns.get(c) + all { cn.closed, if (server) not(cn.serverEv) else not(cn.clientEv) }, + st' = closeEvent(st, c, server), + lastAction' = ACloseEvent({ conn: c, server: server }), + rng' = nextRng(rng), + } + + action garbageOn(c: int, server: bool): bool = all { + st.conns.keys().contains(c), + val cn = st.conns.get(c) + if (server) not(cn.serverEv) else not(cn.clientEv), + st' = garbage(st, c, server), + lastAction' = AGarbage({ conn: c, server: server }), + rng' = nextRng(rng), + } + + action dialOkOn(d: int): bool = all { + st.dials.contains(d), + st' = dialOk(st, d), + lastAction' = ADialOk(d), + rng' = nextRng(rng), + } + + action dialFailOn(d: int): bool = all { + st.dials.contains(d), + st' = dialFail(st, d), + lastAction' = ADialFail(d), + rng' = nextRng(rng), + } + + action tickBy(dt: int): bool = all { + dt > 0, + match nextTimer(st) { + | Some(x) => st.now + dt < x.t.at + | None => true + }, + st' = { ...st, now: st.now + dt }, + lastAction' = ATick(dt), + rng' = nextRng(rng), + } + + action fireTimer = all { + armed(st) != Set(), + match nextTimer(st) { + | Some(x) => all { st' = fire(st, x.ref, x.t), lastAction' = AFire(x.ref), rng' = nextRng(rng) } + | None => all { st' = st, lastAction' = lastAction, rng' = rng } + }, + } + + action restart = all { + st' = serverRestart(st), + lastAction' = ARestart, + rng' = nextRng(rng), + } + + action hardDisconnect = all { + st' = clientDeleteSession(st), + lastAction' = AHardDisconnect, + rng' = nextRng(rng), + } + + action serverClose = all { + not(st.server.closed), + st' = serverShutdown(st), + lastAction' = AServerClose, + rng' = nextRng(rng), + } + + /// Streams where the application on either side can still act. + pure def activeStreams(s: State): Set[int] = s.cStreams.keys().filter(sid => { + val c = s.cStreams.get(sid) + val clientCan = c.listening + val serverCan = s.sStreams.keys().contains(sid) and { + val x = s.sStreams.get(sid) + x.r or x.w or not(x.handlerDone) + } + clientCan or serverCan + }) + + pure def deliverable(s: State): Set[{ conn: int, toServer: bool }] = + s.conns.keys().fold(Set(), (acc, k) => { + val cn = s.conns.get(k) + val a1 = if (cn.toServer.length() > 0 and not(cn.serverEv)) acc.union(Set({ conn: k, toServer: true })) else acc + if (cn.toClient.length() > 0 and not(cn.clientEv)) a1.union(Set({ conn: k, toServer: false })) else a1 + }) + + pure def closeEventsDue(s: State): Set[{ conn: int, server: bool }] = + s.conns.keys().fold(Set(), (acc, k) => { + val cn = s.conns.get(k) + val a1 = if (cn.closed and not(cn.serverEv)) acc.union(Set({ conn: k, server: true })) else acc + if (cn.closed and not(cn.clientEv)) a1.union(Set({ conn: k, server: false })) else a1 + }) + + pure def openConns(s: State): Set[int] = s.conns.keys().filter(k => not(s.conns.get(k).closed)) + + action onStream = all { + activeStreams(st) != Set(), + nondet sid = oneOf(activeStreams(st)) + any { + writeOn(sid), + closeOn(sid), + finalizeOn(sid), + cancelOn(sid), + respondOn(sid), + serverWriteOn(sid), + serverCloseOn(sid), + serverCancelOn(sid), + throwOn(sid), + }, + } + + action deliverAny = all { + deliverable(st) != Set(), + nondet x = oneOf(deliverable(st)) + deliverOn(x.conn, x.toServer), + } + + action closeEventAny = all { + closeEventsDue(st) != Set(), + nondet x = oneOf(closeEventsDue(st)) + closeEventOn(x.conn, x.server), + } + + action onDial = all { + st.dials != Set(), + nondet d = oneOf(st.dials) + dialOkOn(d), + } + + action networkFault = any { + all { + deliverable(st) != Set(), + nondet x = oneOf(deliverable(st)) + any { dropOn(x.conn, x.toServer), garbageOn(x.conn, x.toServer) }, + }, + all { + openConns(st) != Set(), + nondet c = oneOf(openConns(st)) + nondet toServer = oneOf(Set(true, false)) + any { breakOn(c), garbageOn(c, toServer) }, + }, + } + + action dialFailAny = all { + st.dials != Set(), + nondet d = oneOf(st.dials) + dialFailOn(d), + } + + action progress = any { + nondet pt = oneOf(Set(PRpc, PStream, PUpload, PSubscription)) + invokeAs(pt), + onStream, + onStream, + deliverAny, + deliverAny, + deliverAny, + closeEventAny, + onDial, + nondet dt = oneOf(TICKS) + tickBy(dt), + fireTimer, + } + + /// The network is usually fast relative to heartbeats: on most steps where a + /// frame is in flight, the next thing that happens is its delivery. + pure def deliverPromptly(s: State, r: int): bool = + deliverable(s) != Set() and not(oneIn(r, 3)) + + /// Faults are rare relative to progress, and process-level faults rarer still, + /// so traces get far enough to exercise reconnects rather than only teardown. + action step = { + val r2 = nextRng(rng) + val r3 = nextRng(r2) + any { + all { deliverPromptly(st, rng), deliverAny }, + all { + not(deliverPromptly(st, rng)), + any { + progress, + all { oneIn(r2, 2), networkFault }, + all { oneIn(r2, 4), dialFailAny }, + all { oneIn(r3, 80), restart }, + all { oneIn(nextRng(r3), 80), hardDisconnect }, + all { oneIn(nextRng(nextRng(r3)), 200), serverClose }, + }, + }, + } + } + + /// Every behavior, unweighted: the step relation for exhaustive checking. + action stepAll = any { + progress, + networkFault, + dialFailAny, + restart, + hardDisconnect, + serverClose, + } + + ////////////////////////////////////////////////////////////////////////////// + // Invariants (claims PROTOCOL.md makes) + ////////////////////////////////////////////////////////////////////////////// + + /// "Exactly once delivery": every stream sees a prefix of what its peer + /// wrote, in order, with nothing duplicated. + val exactlyOnceInOrder = st.sStreams.keys().forall(sid => + st.cStreams.keys().contains(sid) implies all { + isPrefix(oks(st.sStreams.get(sid).values), st.cStreams.get(sid).written), + isPrefix(oks(st.cStreams.get(sid).results), st.sStreams.get(sid).written), + } + ) + + /// A session never processes a message sent by a different session. + val noCrossSession = not(st.obs.crossSession) + + /// An ack never covers messages the receiver has not sent. + val noAckBeyondSent = not(st.obs.ackBeyondSent) + + /// assertSendOrdering never trips. + val sendOrdering = not(st.obs.sendOrder) + + pure def sameSession(s: State): bool = match s.client.session { + | Some(cs) => match s.server.session { + | Some(ss) => cs.sess == ss.sess + | None => false + } + | None => false + } + + /// Unacknowledged messages are never dropped from the send buffer. + val bufferHoldsUnacked = sameSession(st) implies match st.client.session { + | Some(cs) => match st.server.session { + | Some(ss) => bufCovers(cs.buf, ss.ack, cs.seq) and bufCovers(ss.buf, cs.ack, ss.seq) + | None => true + } + | None => true + } + + /// Neither side has acknowledged more than its peer sent. + val acksBounded = sameSession(st) implies match st.client.session { + | Some(cs) => match st.server.session { + | Some(ss) => cs.ack <= ss.seq and ss.ack <= cs.seq + | None => true + } + | None => true + } + + /// SESSION_STATE_MISMATCH for a session the server still holds only happens + /// when state was actually lost, which correct peers never cause. + val noNeedlessRejection = st.obs.rejections.foldl(true, (ok, r) => ok and r != "FUTURE_CLIENT" and r != "FUTURE_SERVER") + + /// A disconnected session is always on its way to teardown. + val graceWhileDisconnected = all { + match st.client.session { + | Some(cs) => match cs.st { + | CConnected(_) => not(isSomeTimer(cs.grace)) + | _ => isSomeTimer(cs.grace) + } + | None => true + }, + match st.server.session { + | Some(ss) => match ss.st { + | SConnected(_) => not(isSomeTimer(ss.grace)) + | SNoConn => isSomeTimer(ss.grace) + } + | None => true + }, + } + + /// A live connection is always watched for phantom disconnects. + val watchdogWhileConnected = all { + match st.client.session { + | Some(cs) => match cs.st { + | CConnected(c) => st.conns.get(c).closed or isSomeTimer(cs.wd) + | _ => true + } + | None => true + }, + match st.server.session { + | Some(ss) => match ss.st { + | SConnected(c) => st.conns.get(c).closed or isSomeTimer(ss.wd) + | SNoConn => true + } + | None => true + }, + } + + pure def cStreamResolved(s: State, sid: int): bool = { + val c = s.cStreams.get(sid) + val live = match s.client.session { + | Some(cs) => cs.sess == c.sess + | None => false + } + live or (not(c.r) and not(c.w) and not(c.listening)) + } + + pure def sStreamResolved(s: State, sid: int): bool = { + val x = s.sStreams.get(sid) + val live = match s.server.session { + | Some(ss) => ss.sess == x.sess + | None => false + } + live or (not(x.r) and not(x.w) and not(x.inMap)) + } + + /// When a session dies, every stream it carried is resolved on both sides. + val teardownResolvesStreams = all { + st.cStreams.keys().forall(sid => cStreamResolved(st, sid)), + st.sStreams.keys().forall(sid => sStreamResolved(st, sid)), + } + + /// "A full-close is ... when a cancellation happens which results in an + /// immediate full-close": nothing is sent on a stream after its cancel arrives. + val cancelIsFinal = not(st.obs.sentAfterCancel) + + /// "The closing party MUST NOT send any more messages" (cancel excepted). + val closeIsFinal = not(st.obs.sentAfterClose) + + ////////////////////////////////////////////////////////////////////////////// + // Witnesses: `quint run --witnesses` counts the traces that reach each one, + // which shows whether simulation actually exercises the interesting paths. + ////////////////////////////////////////////////////////////////////////////// + + val wConnected = match st.client.session { + | Some(cs) => match cs.st { + | CConnected(_) => true + | _ => false + } + | None => false + } + + /// Still on the first session, but over a later connection. + val wTransparentReconnect = match st.client.session { + | Some(cs) => match cs.st { + | CConnected(c) => cs.sess == 1 and c > 1 + | _ => false + } + | None => false + } + + val wNewSessionAfterLoss = match st.client.session { + | Some(cs) => match cs.st { + | CConnected(_) => cs.sess > 1 + | _ => false + } + | None => false + } + + val wOutOfOrder = st.obs.cOoo + st.obs.sOoo > 0 + + val wRejected = st.obs.rejections.length() > 0 + + val wDisconnectResolved = st.cStreams.keys().exists(sid => st.cStreams.get(sid).results.foldl(false, (acc, r) => acc or r == RErr("UNEXPECTED_DISCONNECT"))) + + val wStreamCompleted = st.cStreams.keys().exists(sid => { + val c = st.cStreams.get(sid) + not(c.r) and oks(c.results).length() > 0 + }) + + val wCancelled = st.cStreams.keys().exists(sid => st.cStreams.get(sid).gotCancel) + + val wServerRestarted = st.server.epoch > 0 + + /// A closed server transport holds no sessions and no pending handshakes. + val closedServerIsEmpty = st.server.closed implies all { + st.server.session == None, + st.server.pending.keys() == Set(), + } + + val wServerClosed = st.server.closed + + /// An upload finalized after it failed: cancelled, or its session ended. + val wUploadFinalizedAfterError = st.cStreams.keys().exists(sid => { + val c = st.cStreams.get(sid) + c.pt == PUpload and c.finalized and c.results.length() > 0 and oks(c.results).length() == 0 + }) + + val safety = all { + closedServerIsEmpty, + exactlyOnceInOrder, + noCrossSession, + noAckBeyondSent, + sendOrdering, + bufferHoldsUnacked, + acksBounded, + noNeedlessRejection, + graceWhileDisconnected, + watchdogWhileConnected, + teardownResolvesStreams, + closeIsFinal, + } +} diff --git a/spec/river_test.qnt b/spec/river_test.qnt new file mode 100644 index 00000000..e4f21638 --- /dev/null +++ b/spec/river_test.qnt @@ -0,0 +1,210 @@ +// -*- mode: Bluespec; -*- + +/// Scenarios for spec/river.qnt. Each `run` drives the model through one +/// behavior PROTOCOL.md describes and checks the outcome. `quint test` runs +/// them, and the conformance suite replays every one of them against the +/// TypeScript implementation. +module river_test { + import river.* from "./river" + + pure def clientIs(s: State, sess: int, cst: CState): bool = match s.client.session { + | Some(cs) => cs.sess == sess and cs.st == cst + | None => false + } + + /// Invoke, connect, and get the first stream's init to the server. + action connectWith(pt: ProcType): bool = + invokeAs(pt) + // the first connection attempt has no backoff + .then(fireTimer) + .then(dialOkOn(1)) + // handshake request, then response; the buffered init goes out + .then(deliverOn(1, true)) + .then(deliverOn(1, false)) + // the init opens the stream on the server + .then(deliverOn(1, true)) + + /// rpc: one request, one response that closes the call. + run rpcRoundTripTest = + init + .then(connectWith(PRpc)) + .then(respondOn(1)) + .then(deliverOn(1, false)) + .expect(all { + st.cStreams.get(1).results == [ROk(101)], + not(st.cStreams.get(1).r), + not(st.sStreams.get(1).inMap), + }) + + /// "Transparent reconnects": a lost frame makes the server see a gap, it + /// closes the connection, and the reconnect retransmits the send buffer, so + /// the stream still sees every value exactly once and in order. + run transparentReconnectAfterFrameLossTest = + init + .then(connectWith(PStream)) + .then(writeOn(1)) + .then(writeOn(1)) + // the first value is lost; the second arrives early + .then(dropOn(1, true)) + .then(deliverOn(1, true)) + .then(closeEventOn(1, true)) + .then(closeEventOn(1, false)) + // back off, then redial + .then(fireTimer) + .then(dialOkOn(2)) + // the server still holds the session, so the reconnect is transparent + .then(deliverOn(2, true)) + .then(deliverOn(2, false)) + // the retransmitted init is a duplicate; both values follow + .then(deliverOn(2, true)) + .then(deliverOn(2, true)) + .then(deliverOn(2, true)) + .expect(all { + st.sStreams.get(1).values == [ROk(1), ROk(2)], + st.obs.sOoo == 1, + clientIs(st, 1, CConnected(2)), + }) + + /// "Hard reconnect": the server restarts after acknowledging the client, so + /// it rejects the old session; the in-flight call resolves with + /// UNEXPECTED_DISCONNECT and the client starts a fresh session. + run hardReconnectAfterServerRestartTest = + init + .then(connectWith(PRpc)) + // server watchdog, then a heartbeat that acknowledges the init + .then(fireTimer) + .then(fireTimer) + .then(deliverOn(1, false)) + .then(restart) + .then(closeEventOn(1, false)) + .then(fireTimer) + .then(dialOkOn(2)) + .then(deliverOn(2, true)) + .then(deliverOn(2, false)) + .expect(all { + st.cStreams.get(1).results == [RErr("UNEXPECTED_DISCONNECT")], + st.obs.rejections == ["UNKNOWN_SESSION"], + st.obs.cErrs == [], + clientIs(st, 2, CBackingOff), + }) + + /// Exactly-once holds per server process: if the server restarts before the + /// client hears anything from it, the new server cannot tell the reconnect + /// from a new session, accepts it, and runs the replayed call a second time. + run serverRestartBeforeFirstReplyReplaysTest = + init + .then(connectWith(PRpc)) + .then(restart) + .then(closeEventOn(1, false)) + .then(fireTimer) + .then(dialOkOn(2)) + .then(deliverOn(2, true)) + .then(deliverOn(2, false)) + .then(deliverOn(2, true)) + .expect(all { + st.sStreams.get(1).inMap, + st.obs.rejections == [], + clientIs(st, 1, CConnected(2)), + }) + + /// The grace period bounds how long a disconnected session lingers: when + /// reconnecting keeps failing, both sides tear the session down and resolve + /// the stream with UNEXPECTED_DISCONNECT. + run graceExpiryResolvesStreamsTest = + init + .then(connectWith(PStream)) + .then(breakOn(1)) + .then(closeEventOn(1, false)) + .then(closeEventOn(1, true)) + // backoff, connection timeout, backoff, timeout, backoff, then both graces + .then(7.reps(_ => fireTimer)) + .expect(all { + st.client.session == None, + st.server.session == None, + st.cStreams.get(1).results == [RErr("UNEXPECTED_DISCONNECT")], + st.sStreams.get(1).values == [RErr("UNEXPECTED_DISCONNECT")], + not(st.sStreams.get(1).w), + not(st.sStreams.get(1).inMap), + }) + + /// An upload can be finalized after it was cancelled: the result is the + /// cancellation. + run uploadFinalizedAfterCancelTest = + init + .then(connectWith(PUpload)) + .then(cancelOn(1)) + .then(finalizeOn(1)) + .expect(all { + st.cStreams.get(1).finalized, + st.cStreams.get(1).results == [RErr("CANCEL")], + }) + + /// An upload can be finalized after its session ended: the result is + /// UNEXPECTED_DISCONNECT. + run uploadFinalizedAfterDisconnectTest = + init + .then(connectWith(PUpload)) + .then(breakOn(1)) + .then(closeEventOn(1, false)) + .then(closeEventOn(1, true)) + .then(7.reps(_ => fireTimer)) + .then(finalizeOn(1)) + .expect(all { + st.client.session == None, + st.cStreams.get(1).finalized, + st.cStreams.get(1).results == [RErr("UNEXPECTED_DISCONNECT")], + }) + + /// "Detecting phantom disconnects": when nothing arrives for + /// heartbeatsUntilDead heartbeat intervals, the watchdog closes the connection. + run watchdogClosesSilentConnectionTest = + init + .then(connectWith(PStream)) + // heartbeats go out but nothing is delivered from here on + .then(4.reps(_ => fireTimer)) + .expect(all { + st.conns.get(1).closed, + st.now == st.cfg.heartbeat * st.cfg.heartbeatsUntilDead, + }) + + /// Known deviation: a cancellation is an immediate full close, yet the + /// server answers a client's cancel of a subscription with a ControlClose. + run serverClosesAfterClientCancelTest = + init + .then(connectWith(PSubscription)) + .then(cancelOn(1)) + .then(deliverOn(1, true)) + .expect(all { + st.obs.sentAfterCancel, + st.conns.get(1).toClient.length() == 1, + }) + + /// An undecodable handshake response destroys the session + /// ("Handshaking -> x"). The implementation used to throw here instead. + run invalidHandshakeResponseTest = + init + .then(invokeAs(PRpc)) + .then(fireTimer) + .then(dialOkOn(1)) + .then(garbageOn(1, false)) + .expect(all { + st.client.session == None, + st.obs.cErrs == [HANDSHAKE_FAILED], + st.cStreams.get(1).results == [RErr("UNEXPECTED_DISCONNECT")], + }) + + /// A closed server transport does not complete a handshake that was still in + /// flight when it closed. The implementation used to create a session here. + run serverCloseDuringHandshakeTest = + init + .then(invokeAs(PRpc)) + .then(fireTimer) + .then(dialOkOn(1)) + .then(serverClose) + .then(deliverOn(1, true)) + .expect(all { + st.server.session == None, + st.server.pending.keys() == Set(), + st.conns.get(1).closed, + }) +} diff --git a/transport/client.ts b/transport/client.ts index 83e1a9b4..ea4f52ba 100644 --- a/transport/client.ts +++ b/transport/client.ts @@ -320,7 +320,7 @@ export abstract class ClientTransport< `invalid handshake: ${reason}`, handshakingSession.loggingMetadata, ); - this.deleteSession(session, { unhealthy: true }); + this.deleteSession(handshakingSession, { unhealthy: true }); this.protocolError({ type: ProtocolError.HandshakeFailed, code, diff --git a/transport/server.ts b/transport/server.ts index f25d8d2d..769830fb 100644 --- a/transport/server.ts +++ b/transport/server.ts @@ -111,6 +111,16 @@ export abstract class ServerTransport< this.pendingSessions.delete(pendingSession); } + close() { + // a connection still waiting for its handshake would otherwise complete it + // and create a session on the closed transport + for (const pendingSession of Array.from(this.pendingSessions)) { + this.deletePendingSession(pendingSession); + } + + super.close(); + } + protected deleteSession( session: ServerSession, options?: DeleteSessionOptions,