Prove it on a live queue

The whole system holds, meters itself, and reports honestly — watched in front of you.

This is the last page of the course. It closes the Proof pillar by exercising the bus on a running codemojex queue: run the conformance suite so the contract holds (EchoMQ.Conformance.run/2 → {:ok, n}), attach a meter and watch the [:emq, :job, …] lifecycle events flow as a game job runs (EchoMQ.Meter), then read the plane so the queue answers how it is doing without being asked to change anything (EchoMQ.Metrics). Proven, observed, answered — step through it on the right.

1 · Run 2 · Meter 3 · Read The session References

The three proofs · step through each check

Beat 1 — run the contract

The bus contract is not asserted in prose; it is run. EchoMQ.Conformance.run/2 drives every scenario — each a name and a one-line contract — against a live server, on per-scenario sub-queues it purges when it is done, printing one CONF line per scenario and a closing tally. It answers {:ok, n} when every scenario passes, or {:error, failed_names} with the names that did not. Point it at a sub-queue of the live codemojex queue and the whole contract runs against the same server the game plays on.

# run the bus contract against the LIVE server, under a codemojex sub-queue.
# run/2 loops scenarios() in run order, runs each on `queue <> "." <> name`,
# PURGES what it mints, prints one CONF line each + a closing tally, and returns
# {:ok, n} on all-pass / {:error, failed_names} otherwise.
{:ok, n} = EchoMQ.Conformance.run(Codemojex.Bus.conn(), "cm.conf")
# CONF fence ok — the version fence is claimed before any work …
# CONF mint  ok — enqueue writes the three-field row: state pending, attempts 0, payload
# CONF claim ok — claim mints token 1, returns the payload, moves the row to active
# … one CONF line per scenario …
# CONFORMANCE n/n

n is the count of scenarios that passed — it is not pinned on this page, because the set grows by additive minor: prior scenarios stay byte-frozen and git-verified, each new one is probe-registered, and the count is re-pinned in the suite's own pinning tests. The shape is the contract, not the number — drive each scenario against a live server, assert the externally visible verdict, answer {:ok, n} when they all hold. A port of the bus in another runtime is conformant exactly when it drives the same server to the same verdicts: the polyglot promise made testable.

And because the suite purges what it mints, running it against cm.conf leaves the real codemojex queues untouched — the contract is proven beside live traffic, not on top of it.

The contract holds because it is run, not asserted — {:ok, n} is the whole bus, proven against the same server the game plays on.

Beat 2 — attach a meter, watch the lifecycle

A holding contract is the floor. The next question is how is it doing right now — and the bus answers that two ways. The push side is EchoMQ.Meter: the job lifecycle metered the standard Elixir :telemetry way, re-rooted under [:emq, …], one event tree with the connector's own [:emq, :connector, …]. Attach a handler to the lifecycle events and every codemojex job that runs fires them as it moves.

# echo/apps/echo_mq — EchoMQ.Meter.attach_many/4 over the live bus.
# Each suffix is rooted [:emq | suffix] BEFORE it reaches :telemetry.attach_many,
# so the handler subscribes to the bus's own tree. With NO :telemetry loaded this
# whole call answers :ok as a no-op — the bus carries no dependency edge.
:ok =
  EchoMQ.Meter.attach_many(
    "cm-feed",
    [[:job, :add], [:job, :start], [:job, :complete], [:job, :fail]],
    fn event, measurements, metadata, _config ->
      # event :: [:emq, :job, :start | :complete | …] — already rooted under :emq
      Logger.info("#{inspect(event)} q=#{metadata.queue} job=#{metadata.job_id}")
    end,
    nil
  )

Now play the game. Codemojex.Guesses.submit/3 enqueues a guess on the player's fair lane (EchoMQ.Lanes.enqueue(conn, "cm", player, job, payload)), Codemojex.ScoreWorker claims and scores it, and Codemojex.NotificationWorker drains the cm.notify queue to push the result. Each transition the bus meters emits onto the tree — job_added/4, job_started/4, job_completed/5, and job_failed/6 are the convenience emitters that fire [:emq, :job, :add | :start | :complete | :fail] — so the attached handler sees the codemojex job's whole life flow past, queue and job id in the metadata, with no change to any transition script.

The cost is named, and it is zero. Every emission guards :erlang.function_exported(:telemetry, :execute, 3): with no :telemetry dependency loaded, an emit is a no-op and the attach_many above answers :ok with no effect — the bus carries no :telemetry dependency edge, a host opts in by adding the dependency itself. (The surface is named EchoMQ.Meter — a collision-free name, deliberately not a plainer one, so it never shadows another module on the shared code path.) Metering is a thing the host turns on, not a tax the bus charges.

Attach a handler and the lifecycle reports itself — [:emq, :job, …] events flow as the game plays, at zero cost when no one is listening.

Beat 3 — read the plane

Push tells you when things happen. Pull answers a question on demand, and changes nothing in the asking: EchoMQ.Metrics is a set of pure-read verbs over the bus's as-built structures — every verb observes, none mutates. Ask the live codemojex queue how it is doing.

# echo/apps/echo_mq — EchoMQ.Metrics: pure reads over the live codemojex queue.
# per-state counts over the four sorted sets (+ the completed/failed counter
# the completion transition leaves no set for) — a pure read; an unregistered
# state name is {:error, {:unknown_state, name}}, never an open read.
{:ok, counts} =
  EchoMQ.Metrics.get_counts(Codemojex.Bus.conn(), "cm",
    ["pending", "active", "schedule", "dead"])
# => {:ok, %{"pending" => 7, "active" => 3, "schedule" => 1, "dead" => 0}}

# one player's lane backlog — codemojex names each lane by the player's PLR id
{:ok, depth} = EchoMQ.Metrics.lane_depth(Codemojex.Bus.conn(), "cm", player_id)
# => {:ok, 4}

# the read-and-refuse gate at the concurrency ceiling — a read that refuses
EchoMQ.Metrics.is_maxed(Codemojex.Bus.conn(), "cm")
# => :ok               (below the ceiling — a claim may proceed)
# => {:error, :rate}   (at the ceiling — a worker should back off, not claim)

get_counts/3 reads ZCARD of each state's sorted set (and the terminal-outcome counter for completed/failed, which the completion transition leaves no set for); an unregistered state name is {:error, {:unknown_state, name}}, never an open read. lane_depth/3 answers the pending depth behind one player's lane — codemojex names each lane by the player's PLR id, so the read tells you exactly how far one player is backed up. is_maxed/2 reads the active set against the configured ceiling and answers :ok below it or {:error, :rate} at it — a read that refuses, moving nothing. Every read script declares its keys, so the {q} slot is pinned even on a metric-only request; the read plane is honest by construction.

This is the system answering for itself: counts, lane depth, the rate gate — read off the same structures the queue runs on, with no transition, no mutation, no phantom write.

The queue answers how it is doing without being asked to change — counts, lane depth, and the rate gate are pure reads over the live structures.

The session — one round, all three proofs

Run a single codemojex round and watch all three proofs in one feed. First the contract runs and answers {:ok, n}. Then advance the round: each guess fires the [:emq, :job, …] lifecycle events to the attached meter as Codemojex.ScoreWorker scores it. At any point, read the plane and the queue answers its counts, the player's lane depth, and the rate gate — a pure read that changes nothing. Proven once, observed throughout, answered on demand.

The live-session runner · run the contract, advance the round, read the plane

sourcesignaldetail

The runner steps the real lifecycle. EchoMQ.Conformance.run/2 answers {:ok, n} first — the contract holds before the round begins. Codemojex.Guesses.submit/3 enqueues each guess on the player's lane, Codemojex.ScoreWorker scores it with Codemojex.Scoring.score/2 and the bus emits [:emq, :job, :start] then [:emq, :job, :complete] to the attached meter, and a read the plane at any point answers get_counts/3, lane_depth/3, and is_maxed/2 over the live structures — pure reads that move nothing. The contract held before, holds during, and holds after.

One round, three proofs, one queue — the contract proven, the lifecycle observed, and the plane answered, all on the same live server.

Pattern → implementation

The pattern side — run a conformance contract, meter the work with telemetry, and read the system's state without changing it — is what Redis Patterns Applied frames as running a queue in production. Here it is built from the implementation side, over a live codemojex queue.

the pattern (Redis Patterns Applied)

Prove the contract, meter the work, and read the system's state on demand — the operations a queue earns in production. Production operations frames the moves; coordination frames the atomicity the suite proves.

the implementation (echo_mq)

EchoMQ.Conformance.run/2 → {:ok, n}, EchoMQ.Meter.attach_many/4 on the [:emq, :job, …] tree, and the EchoMQ.Metrics read plane (get_counts/3, lane_depth/3, is_maxed/2) — the real shipped verbs, run over a live codemojex queue.

The same idea read two ways — the pattern names prove it, meter it, read it; the pillar runs the shipped verbs that do, against the same server the game plays on.

Recap — the pillar, exercised

The Proof pillar taught three concerns: the conformance suite that runs the contract, the telemetry surface and the read plane that report on the running system, and the benchmark frontier still ahead. This workshop exercised the two that are shipped, on one live queue. Run the suite and the contract answers {:ok, n}. Attach a meter and the codemojex lifecycle reports itself as [:emq, :job, …] events, at zero cost when no one listens. Read the plane and the queue answers its counts, its lane depths, and its rate gate without changing anything. The system holds, meters itself, and reports honestly — proven, observed, and answered. That is the whole bus, on a live queue, the close of the course.

The architecture law these proofs realize — the four libraries composed as one umbrella, one identity carried through — is the BCS together chapter.

References

Where the metering surface, the read primitives, and the run-not-assert idea are grounded.

Sources

Elixir — the :telemetry library — the standard metering surface EchoMQ.Meter re-roots under [:emq, …]; the bus carries no edge to it until a host opts in.
Erlang/OTP — :telemetry.execute/3 — the guarded call every emission checks for before firing (zero cost when absent).
Valkey — ZCARD — the per-state count the read plane reads off each sorted set.
Valkey — HGET — the row-field and counter read behind get_job / get_metrics.
Beck — Test-Driven Development — the verdict-asserting scenario as the contract: run, not asserted.

Related in this course

The conformance suite — beat 1: the bus contract as runnable scenarios.
Telemetry & the read plane — beats 2 and 3: push (the meter) and pull (the read plane).
The Proof — the pillar this workshop closes.
The Queue — the lifecycle the meter watches and the read plane reports.
The Bus — the second pillar the suite proves whole.
The Cache — the third product surface.
redis-patterns · coordination — the atomicity the suite proves, from the pattern side.
redis-patterns · production operations — running the tier, the pattern side of this workshop.
bcs · together — the architecture law: the four libraries as one umbrella.