Skip to content

Message contracts

RabbitMQ is the integration surface between all four platform repos. Every cross-repo action — upload, atomize, certify, promote — is a message, not an HTTP call. This page is the cross-repo index of those contracts: the shared envelope, the topology pattern every queue follows, the five pipelines, and the invariants that must hold on both sides of each queue.

Source of truth

The upload and atomize contracts are fully specified upstream in verilib-atomizer/docs/protocols/ — this page summarizes and links.

The validate / promote contracts have no upstream prose spec; the authoritative definitions are local_validate/broker/messages.py and broker/topology.py. They are documented in full below.

Peers

Pipeline Publisher Consumer Response consumer
upload frontend (PHP) atomizer upload-processor frontend
atomize frontend (PHP) atomizer atomize-processor frontend
livelog atomize-processor frontend (joblogs insert) —
validate frontend (PHP) local_validate validate_processor frontend
promote frontend (PHP) local_validate promote_processor frontend

The frontend is the sole MySQL writer on every one of these paths. Workers are headless; the cert workers are additionally DB-free (no DB_* env vars at all) — every value they need to do their job arrives on the message.

Shared envelope

Every message in every pipeline carries the same correlation keys:

Field Type Semantics
event_id string UUID-4, fresh per message. Minted by each publisher.
request_id string UUID-4, echoed verbatim along the whole chain. Identifies the originating user-facing API call.
metadata.produced_at string ISO-8601 UTC timestamp of publication.
metadata.* any Free-form forward-compatibility bag. Consumers must ignore unknown keys.

Publishers also set the AMQP correlation_id property to request_id, so broker tooling can correlate without unpacking the body. Bodies are JSON, application/json / utf-8.

There is no schema / schema_version on the wire — each queue carries exactly one message type, so per-message tagging would be redundant. Evolution is handled by additive fields plus the ignore-unknown-keys rule.

Topology pattern

Every business queue is declared with the same three-part shape, in both BaseQueue::setup (PHP) and broker.topology.declare (Python):

flowchart LR
  pub[Publisher] -->|routing key| mx[main exchange<br/>direct]
  mx --> mq[main queue<br/>x-max-priority=10]
  mq --> con[Consumer]
  con -->|transient failure| rx[retry exchange<br/>topic]
  rx --> rq[retry queue<br/>TTL 50s + DLX]
  rq -.->|dead-letters back after 50s| mx
  con -->|poison message| ex[error exchange<br/>topic]
  ex --> eq[error queue<br/>terminal]
Object Naming Arguments
Main exchange <name>_exchange direct
Main queue <name>_queue x-max-priority=10
Retry exchange <queue>_retry_exchange topic
Retry queue <queue>_retry_queue x-message-ttl=50000, x-dead-letter-exchange=<main exchange>, bound with #
Error exchange <queue>_error_exchange topic
Error queue <queue>_error_queue terminal; drained by ops

Topology arguments must change on both sides in the same PR

RabbitMQ rejects a re-declaration with different arguments via a 406 PRECONDITION_FAILED that closes the channel. Whichever peer declares a shared queue second dies if any argument diverges. x-max-priority, x-message-ttl, and x-dead-letter-exchange are therefore a joint contract between verilib-frontend and the worker repos.

This failure mode is deliberate — a contract mismatch should fail loudly at startup rather than silently drop messages.

Queue inventory

Queue Exchange Routing key Env prefix
upload_request_queue upload_request_exchange upload.request UPLOAD_REQUEST_*
upload_response_queue upload_response_exchange upload.response UPLOAD_RESPONSE_*
atomize_request_queue atomize_request_exchange atomize.request ATOMIZE_REQUEST_*
atomize_response_queue atomize_response_exchange atomize.response ATOMIZE_RESPONSE_*
livelog_queue livelog_exchange livelog LIVELOG_*
validate_request_queue validate_request_exchange validate.request VALIDATE_REQUEST_*
validate_response_queue validate_response_exchange validate.response VALIDATE_RESPONSE_*
validate_livelog_queue validate_livelog_exchange validate.livelog VALIDATE_LIVELOG_*
promote_request_queue promote_request_exchange promote.request PROMOTE_REQUEST_*
promote_response_queue promote_response_exchange promote.response PROMOTE_RESPONSE_*

Each name is overridable via <PREFIX>_EXCHANGE / _QUEUE / _ROUTING_KEY — but only if renamed on both peers. See Configuration and environment variables.

Upload pipeline

Full spec: docs/protocols/upload.md.

upload.request — key fields: repo_id (doubles as the S3 prefix), user_id, language_id, proof_language_id, and a source object.

There is no explicit "upload" vs "reclone" operation field. The worker always uploads to s3://<bucket>/<repo_id>/ after clearing that prefix first — so first-upload and reclone are the same code path.

source.mode Behaviour
repo_url git clone --depth 1 into scratch, mirror working tree (excluding .git) to S3. Supports <url>@<branch> and <repo>/tree/main/<subfolder> (sparse --filter=tree:0 clone) forms, combinable.
raw_code Write source.code_raw directly to s3://<bucket>/<repo_id>/<source.filename>. No clone, no scratch dir.

Private-repo credentials travel on the message, encrypted:

github_repo_visibility github_access_token Clone behaviour
public or NULL NULL Anonymous HTTPS clone
private NULL Permanent error — authorization required
any set (AES-256-CBC ciphertext) Decrypt, GET /repos/{owner}/{repo} preflight, clone via https://x-access-token:<token>@github.com/...

The upload processor never reads tokens from MySQL. It decrypts with GITHUB_TOKEN_ENCRYPTION_KEY (falling back to JWT_KEY), which must match the frontend's value.

upload.response — status (success / error), s3_uri, commit_sha (only for repo_url mode), echoed language_id / proof_language_id / verifier_version_id so the frontend needs no follow-up DB read, plus a stats block (files_uploaded, bytes_uploaded, duration_ms) that is always present and zeroed on error.

Atomize pipeline

Full spec: docs/protocols/atomize.md.

atomize.request — s3_uri, commit_sha, repo_id, language_id, proof_language_id.

Probe selection is driven by proof_language_id, mapped through the PROOF_LANGUAGE_ID_MAP env var:

The default map does not match production

The protocol doc documents the code default 1:Rust,2:Lean,3:Aeneas, but the tracked deployment example (deploy/config/example.env) sets PROOF_LANGUAGE_ID_MAP=10:Rust,2:Lean,11:Aeneas. The ids are environment configuration, not a stable contract — always read the deployed value rather than assuming 1/2/3. See Configuration and environment variables.

atomize.response — status, s3_output_uri (the probe JSON), language (name string), stats.atom_count, stats.duration_ms.

livelog — streamed progress, one message per step, consumed by the frontend into joblogs. Carries repo_id, event_id (correlating to the atomize request), event, status (info / success / error / warning), and optional counters (atom_count, extracted, total, dep_count, duration_seconds).

Event types: repo_start, repo_step, repo_cleanup, repo_probe_extract, repo_parse, repo_extract_bodies, repo_persist_deps, repo_persist_atoms, repo_restore_backup, repo_complete, repo_error.

Validate pipeline

Defined by local_validate/broker/messages.py. Not documented upstream — this is the reference.

validate.request

Published by PHP when a user with the Certifier permission clicks Certify.

Field Type Required Notes
certificate_id int yes The addressable target — the certificates row.
repo_id int yes Doubles as the S3 manifest prefix (cert/<repo_id>/) and as a build/logging token.
parent_repo_id int no Defaults 0. The repo the cert snapshot was cloned from; its tree is read from s3://<S3_REPOS_BUCKET>/<parent_repo_id>/.
image_tag int no Defaults 1.
repo_url, branch, commit string no Default "". Source coordinates for the probe build.
language_id int? no With has_aeneas_proof_language, resolves which probe kind to run.
has_aeneas_proof_language bool no Defaults false.
cert_probe_kind string? no Explicit override; bypasses the language_id resolution.
cargo_package, workdir, rust_root string no Default "". Probe build parameters.
eth_certify_enabled bool? no Per-certificate override of the worker's ETH_CERTIFY_ENABLED. Lets one cert skip the chain step.
cert_metadata object no Free-form.

Missing or null certificate_id / repo_id raises ValueError — the message is unaddressable and goes to the error queue.

validate.response

status is success or error (enum ValidateResponseStatus). PHP consumes this and is the sole writer of the resulting certificate row.

Field Notes
certificate_id, repo_id Echoed; certificate_id is required.
status success | error.
s3_output_uri s3://<S3_BUCKET>/cert/<repo_id>/probe-manifest-complete.json.
manifest_sha256 Hash of the manifest — the value anchored on-chain.
resolved_commit The commit the probe image actually baked (dalekLiteResolvedCommit).
verified_functions_count Numerator for the certificate page.
to_be_verified Denominator.
verification_success Bool — did the probe run itself succeed.
docker_hub_image_digest sha256:… when the image was pushed; feeds the content hash.
sepolia_certify_tx_hash Present when the Sepolia anchor succeeded. See Testnet.
chain_scope e.g. testnet_and_mainnet.
mainnet_migration_status e.g. complete.
probe_extract_completed_at_utc ISO-8601.
error { "message": str } on error, else null.

validate.livelog

Streamed probe progress on validate_livelog_queue, mirroring the atomize livelog role for the cert path.

Promote pipeline

Mainnet anchoring is a separate pipeline, not part of the validate consumer. See Mainnet.

promote.request

The frontend — as sole DB owner — resolves the three values the on-chain call hashes and sends them, so the worker still needs no database:

Field Maps to certificate column
certificate_id (required — the target row)
repo_id —
commit dalekLiteResolvedCommit
docker_hub_digest dockerHubImageDigest
manifest_sha256 manifestSha256

promote.response

Field Notes
status success | error.
mainnet_certify_tx_hash The mainnet transaction.
chain_scope Set to testnet_and_mainnet by the success factory.
mainnet_migration_status Set to complete by the success factory.
error { "message": str } on error.

See Certify contract for what these hashes commit to on-chain and who is allowed to submit the transaction.

Failure routing

All pipelines use the same three-tier model:

Tier Trigger Destination Visible to the user?
Transient S3 throttling, broker hiccups, unexpected exceptions <queue>_retry_exchange → back to main queue after 50 s No — only the final outcome reaches the response queue
Permanent git clone failure, probe failure, validation error with a recoverable envelope, retry budget exhausted …Response(status="error") on the response queue Yes — PHP surfaces error.message
Poison Payload has no extractable repo_id / certificate_id, so no response can be addressed <queue>_error_exchange with an error-report envelope No — drained by ops

Retry budgets: UPLOAD_MAX_RETRIES / ATOMIZE_MAX_RETRIES (code default 5; the tracked deploy example sets atomize to 3), and JOB_MAX_ATTEMPTS (default 5) for the cert workers.

The poison-message envelope preserves PHP's BaseQueue::reportError keys plus the raw payload, so messages can be replayed:

{
  "event_id":   "uuid",
  "request_id": "uuid",
  "error":      { "message": "...", "code": 0, "file": "", "line": 0, "trace": "" },
  "original_message": { "…": "the original request payload" },
  "metadata":   { "produced_at": "2026-04-28T20:00:00+00:00" }
}

Schema evolution rules

  1. Additive changes are non-breaking. Both the PHP and Python from_dict implementations ignore unknown keys and default missing optional fields.
  2. Renaming or removing a field is breaking and needs a coordinated rollout: publish the new field on the producer first, consume it on the worker, then drop the old field.
  3. Topology arguments must change simultaneously on both peers — see the warning above.