The stream log · dive 02

The order theorem

Stream order, id sort, and mint order are one fact — proven by construction, not by example.

The log is replayable in the order things happened without a second index because of a single equality: stream order == id sort == mint order. It is not a property the writer hopes holds at run time — it is a theorem proven by construction in EchoMQ.Stream.Id, in two joined steps: branded byte order equals snowflake order within one namespace (the kind door), and the entry id is an order-preserving image of the snowflake (the A1 mapping). Pick a pair of ids on the right and see all three orderings agree, then read why a violation surfaces as :nonmonotonic.

The two-step proof Sort equivalence The honest signal Pattern & implementation References

The proof · step the two moves

The proof, in two steps

Step 1 — branded byte order equals snowflake integer order. A branded id is namespace ++ base62₁₁(snowflake). EchoData.Base62 is the order-preserving fixed-width codec — its alphabet is 0-9A-Za-z in ascending byte order, so the lexical order of the eleven characters equals the numeric order of the snowflake. For a fixed namespace, the leading three bytes are constant, so the byte order of the whole 14-byte string equals the snowflake's numeric order. The qualifier is load-bearing: this holds only within one namespace, because the namespace bytes compare first. That is exactly why the writer admits one brand per stream.

# echo_mq — EchoMQ.Stream.Id
# evt?/1: the kind predicate the writer calls before any wire. One brand per
# stream (EVT) is what keeps "byte order == integer order" sound — base62 byte
# order equals int order only WITHIN one namespace.
def evt?(branded) when is_binary(branded) do
  match?({:ok, "EVT", _snow}, BrandedId.parse(branded))
end

def evt?(_), do: false

Step 2 — the entry id is an order-preserving image of the snowflake. Write the snowflake as snow = ms_part <<< 22 ||| tail22. The A1 mapping emits the pair (ms_part + epoch, tail22). Because the snowflake packs the timestamp high and the node|seq tail in the low 22 bits with no overlap, snow_a < snow_b exactly when (ms_a, tail_a) < (ms_b, tail_b) lexicographically — which is precisely the pair XADD compares. The + epoch is a constant monotone shift, so it preserves order. Therefore snow_a < snow_b ⇔ xadd_id(a) < xadd_id(b).

# echo_mq — EchoMQ.Stream.Id
# xadd_id/1: the order-preserving image. ms = the REAL Unix-ms (ts packed high);
# tail22 = the 22-bit node|seq (packed low, no overlap with ts). The emitted pair
# (ms, tail22) is exactly what XADD compares — so snow order ⇔ entry-id order.
def xadd_id(branded) when is_binary(branded) do
  case BrandedId.parse(branded) do
    {:ok, "EVT", snow} -> {:ok, "#{Snowflake.unix_ms(snow)}-#{snow &&& 0x3FFFFF}"}
    {:ok, _other_ns, _snow} -> {:error, :kind}    # well-formed, wrong namespace
    :error -> {:error, :malformed}                 # not a branded id at all
  end
end

The two decisions are not independent: one brand per stream (the kind door) and the field-correspondence id (the A1 map) are joined precisely so the orderings agree. The order is a compile-time theorem, not a runtime hope.

Sort equivalence

Pick two minted EVT ids and see the three orderings line up: which branded string sorts first lexically, which snowflake is the smaller integer, and which entry id XADD would place earlier. They always agree — that is the theorem made visible. The model is the real xadd_id/1 arithmetic over fixed ids; the comparison runs in your browser.

Three orderings, one answer

id A

id B

Two different brands would sort by their letters, not their snowflakes — which is why the cross-namespace comparison is neither required nor sound, and why the kind door admits exactly one brand per stream. Within EVT, the three orderings are the same order.

The honest signal

XADD with an explicit id rejects any id equal to or smaller than the stream's current top. For a single writer that is impossible to trigger: the mint cell is a strictly-monotone counter, so successive mints are strictly increasing snowflakes, which (by the theorem) are strictly increasing entry ids, which always exceed the top. The writer never retries, never falls back to a * autogenerated id. So the rejection appears only when the invariant is actually broken upstream — two writers on one stream, or a misconfiguration — and the writer surfaces the truth rather than hiding it.

# echo_mq — EchoMQ.Stream (inside append_id/5)
# The ONLY error mapped to :nonmonotonic is Valkey's verbatim "id ≤ top"
# rejection — the wire telling the truth that an upstream mint-order violation
# happened. NEVER swallowed, NEVER retried with a "*" autogen id (which would
# hide the violation and break the order theorem). Every OTHER reply is verbatim.
case Connector.command(conn, parts) do
  {:ok, id} when is_binary(id) -> {:ok, branded}
  {:ok, {:error_reply, @id_too_small}} -> {:error, :nonmonotonic}
  {:ok, {:error_reply, msg}} -> {:error, {:error_reply, msg}}
  {:error, _} = err -> err
end

# @id_too_small is the verbatim Valkey message:
# "ERR The ID specified in XADD is equal or smaller than the target stream top item"

A single monotone writer can never be rejected, so a rejection is information: the wire is reporting a real mint-order violation. Mapping it to a typed :nonmonotonic keeps the failure honest and recognizable — never papered over with a * retry that would hide the break.

Pattern & implementation

the pattern (Redis Patterns Applied)

A log orders entries by their id, and readers replay in id order; the ordering is usually a runtime property of how ids are assigned. Streams & Events teaches the ordered log.

the implementation (echo_mq)

The ordering is a compile-time theorem: the order-preserving Base62 codec plus the high-ts / low-tail packing make stream position a provable image of mint order — within one namespace, which evt?/1 enforces. A real violation surfaces as :nonmonotonic.

The pattern says: the id orders the log. The implementation proves the id order is the mint order — by construction, not by hope — and refuses to hide a violation behind an autogenerated id.

Recap — one fact, three names

The order theorem is two joined steps: branded byte order equals snowflake order within one namespace (the kind door), and the entry id is an order-preserving image of the snowflake (the A1 mapping). A single monotone writer can never be rejected; a true violation surfaces as {:error, :nonmonotonic}. The next dive reads the ordered log back and shows the branded id is stored as the entry's own field.

Next in the module: The claims-only id — the branded id stored as the stream id field, and the minimal XRANGE read-back in mint order.

References

Where the order theorem and the non-monotonic signal are grounded, and the stream semantics they rest on.

Sources

Valkey — Introduction to Streams — the entry-id ordering and the id ≤ top rejection.
Valkey — XADD — the explicit-id append the theorem makes safe.
Lamport — Time, Clocks, and the Ordering of Events — the total order the mint instant defines.
Kreps — The Log — the ordered, replayable log as the unifying abstraction.

Related in this course

The stream log — the module this dive belongs to.
The host-side mint — the append and the A1 mapping.
The claims-only id — reading the ordered log back.
The Protocol — the branded-id contract the order rests on.
redis-patterns · Streams & Events — the ordered-log pattern.