İnvariant'lar (I₁–I₇)

Micro Socket metodolojisinde asla bozulmaması gereken özellikler aşağıdadır.

I₁ – Yetkisiz Erişim Olmaması (ACL)

Hiçbir kullanıcı veya servis, izin verilmemiş bir topic'e erişemez.

Formal: ∀ mesaj (topic, user) : (¬ACL(topic, user) ⇒ mesaj gönderilmez)
Uygulama: Her SUBSCRIBE/PUBLISH'ta ACL kontrolü; token'dan userId; Redis/DB'de user→topic eşlemesi.

Aynı messageId veya idempotencyKey ile gelen olay yalnızca bir kez işlenir.

Formal: Aynı id ile ikinci PUBLISH gelirse olay yok sayılır.
Uygulama: Gateway'te dedup set (Redis Set veya in-memory); sliding window TTL.

Her topic için gönderim sırası korunur.

Formal: topic için t₁ < t₂ ise t₁ önce teslim edilir.
Uygulama: Her mesajda monotonik seqNo; client'ta lastSeq kontrolü; gap varsa replay.

QoS≥1 kanallarda mesaj kaybolmaz; en az bir kez (veya exactly-once) teslimat.

Formal: QoS≥1 mesaj kabul edildiyse istemci en az bir kez MESSAGE alır; ACK gelmezse yeniden gönderim.
Uygulama: ACK mekanizması; retry ile MESSAGE tekrar gönderimi.

Örn. p99 gecikmesi ≤ X ms; aşılırsa uyarı.

Formal: P(latency ≤ SLO) ≥ %Y.
Uygulama: publish→deliver süresi ölçümü; Prometheus; p50/p95/p99 metrikleri.

Kısa kesintide istemci kayıp yaşamadan kaldığı yerden devam eder.

Formal: Bağlantı kesilip yeniden bağlanıldığında aradaki mesajlar eksiksiz iletilir.
Uygulama: RESUME(sessionId, lastSeq); gateway gap'i replay ile kapatır.

Mesaj içeriği bozulmaz (checksum/HMAC veya TLS).

İnvariant	Kısa Açıklama
I₁	ACL: yetkisiz topic erişimi yok
I₂	Dedup: aynı messageId tek işlem
I₃	Sıralama: seqNo ile sıra korunur
I₄	Teslim: QoS≥1 en az bir kez + ACK/retry
I₅	SLO: p50/p95/p99 gecikme hedefi
I₆	Resume: kesinti sonrası gap'siz devam
I₇	Bütünlük: TLS / imza

Her biri için detaylı algoritma ve Node.js örnekleri: Algoritmalar ve Node.js Gateway.