Invariantes (I₁–I₇)

Propiedades que nunca deben violarse en la metodología Micro Socket.

I₁ – Sin acceso no autorizado (ACL)

Ningún usuario o servicio puede acceder a un topic no permitido.

Formal: ∀ mensaje (topic, user) : (¬ACL(topic, user) ⇒ mensaje no enviado).
Implementación: Comprobación ACL en cada SUBSCRIBE/PUBLISH; userId desde token; mapeo user→topic en Redis/DB.

Un evento con el mismo messageId o idempotencyKey se procesa solo una vez.

Formal: Si llega un segundo PUBLISH con el mismo id, el evento se ignora.
Implementación: Conjunto dedup en gateway (Redis Set o en memoria); TTL ventana deslizante.

Se preserva el orden de envío por topic.

Formal: Para un topic, si t₁ < t₂ entonces t₁ se entrega primero.
Implementación: seqNo monótono en cada mensaje; comprobación lastSeq en cliente; replay en huecos.

En canales QoS≥1 los mensajes no se pierden; entrega al menos una vez (o exactamente una).

Formal: Si se acepta un mensaje QoS≥1, el cliente recibe MESSAGE al menos una vez; retransmitir si no hay ACK.
Implementación: Mecanismo ACK; reintento de envíos MESSAGE.

p. ej. latencia p99 ≤ X ms; alerta si se supera.

Formal: P(latencia ≤ SLO) ≥ Y%.
Implementación: Medir tiempo publish→deliver; Prometheus; métricas p50/p95/p99.

Tras una interrupción breve el cliente continúa sin pérdida.

Formal: Tras desconectar y reconectar, se entregan todos los mensajes intermedios.
Implementación: RESUME(sessionId, lastSeq); el gateway rellena huecos con replay.

El contenido del mensaje no se altera (checksum/HMAC o TLS).

Formal: El contenido no puede modificarse en tránsito; verificado de extremo a extremo.
Implementación: TLS; firma de mensaje opcional (HMAC).

Invariante	Descripción breve
I₁	ACL: sin acceso no autorizado al topic
I₂	Dedup: mismo messageId procesado una vez
I₃	Orden: seqNo preserva el orden
I₄	Entrega: QoS≥1 al menos una vez + ACK/retry
I₅	SLO: objetivo de latencia p50/p95/p99
I₆	Resume: continuar tras desconexión sin huecos
I₇	Integridad: TLS / firma