SI1 ★ — RemoteOperationProgress channel isolation over the REAL wire.
Two RemoteOperations are fired CONCURRENTLY, each processing a DIFFERENT number of records (1 vs 2)
and each with its own onProgress collector. The server publishes both ops' progress onto the one
shared RemoteOperationProgress topic; the inline filter payload.ChannelId === args.channelId
must route each op's events ONLY to that op's subscription. The proof is by CONTRADICTION: if the
filter leaked (e.g. broadcast to all subscribers), one op's collector would receive events bearing
the OTHER op's discriminator.
Two independent, non-vacuous assertions:
(a) RESULT ROUTING — each caller's Output.processed equals its OWN record count (1 vs 2), proving
the mutation result returned to the right caller (this leg never degrades).
(b) PROGRESS ISOLATION — each collector's events carry ONLY that op's discriminator. Preferred
discriminator is Handle (the per-run ProcessRunID); falls back to Total (the record count).
If the server emits progress with NEITHER discriminator, (b) skips-as-pass with a loud note
while (a) still stands — never a vacuous pass, never a false failure.
SI1 ★ — RemoteOperationProgress channel isolation over the REAL wire.
Two RemoteOperations are fired CONCURRENTLY, each processing a DIFFERENT number of records (1 vs 2) and each with its own
onProgresscollector. The server publishes both ops' progress onto the one sharedRemoteOperationProgresstopic; the inline filterpayload.ChannelId === args.channelIdmust route each op's events ONLY to that op's subscription. The proof is by CONTRADICTION: if the filter leaked (e.g. broadcast to all subscribers), one op's collector would receive events bearing the OTHER op's discriminator.Two independent, non-vacuous assertions: (a) RESULT ROUTING — each caller's
Output.processedequals its OWN record count (1 vs 2), proving the mutation result returned to the right caller (this leg never degrades). (b) PROGRESS ISOLATION — each collector's events carry ONLY that op's discriminator. Preferred discriminator isHandle(the per-run ProcessRunID); falls back toTotal(the record count). If the server emits progress with NEITHER discriminator, (b) skips-as-pass with a loud note while (a) still stands — never a vacuous pass, never a false failure.