Invariants (I₁–I₇)
Properties that must never be violated in the Micro Socket methodology.
I₁ – No Unauthorized Access (ACL)
No user or service may access a topic they are not allowed to.
- Formal: ∀ message (topic, user) : (¬ACL(topic, user) ⇒ message not sent).
- Implementation: ACL check on every SUBSCRIBE/PUBLISH; userId from token; user→topic mapping in Redis/DB.
I₂ – No Double Processing (Dedup)
An event with the same messageId or idempotencyKey is processed only once.
- Formal: If a second PUBLISH with the same id arrives, the event is ignored.
- Implementation: Dedup set at gateway (Redis Set or in-memory); sliding window TTL.
I₃ – Consistent Ordering
Per-topic send order is preserved.
- Formal: For a topic, if t₁ < t₂ then t₁ is delivered first.
- Implementation: Monotonic
seqNoon every message; client lastSeq check; replay on gap.
I₄ – Delivery Guarantee
On QoS≥1 channels messages are not lost; at least once (or exactly-once) delivery.
- Formal: If a QoS≥1 message is accepted, the client receives MESSAGE at least once; retransmit if no ACK.
- Implementation: ACK mechanism; retry MESSAGE sends.
I₅ – Latency SLOs
e.g. p99 latency ≤ X ms; alert if exceeded.
- Formal: P(latency ≤ SLO) ≥ Y%.
- Implementation: Measure publish→deliver time; Prometheus; p50/p95/p99 metrics.
I₆ – Continuity (Resume)
After a short outage the client continues without loss.
- Formal: After disconnect and reconnect, all messages in between are delivered.
- Implementation: RESUME(sessionId, lastSeq); gateway fills gap via replay.
I₇ – Data Integrity
Message content is not altered (checksum/HMAC or TLS).
- Formal: Content cannot be changed on the wire; verified end-to-end.
- Implementation: TLS; optional message signature (HMAC).
Summary Table
| Invariant | Brief description |
|---|---|
| I₁ | ACL: no unauthorized topic access |
| I₂ | Dedup: same messageId processed once |
| I₃ | Ordering: seqNo preserves order |
| I₄ | Delivery: QoS≥1 at least once + ACK/retry |
| I₅ | SLO: p50/p95/p99 latency target |
| I₆ | Resume: continue after disconnect with no gap |
| I₇ | Integrity: TLS / signature |
See Algorithms and Node.js Gateway for details.