Configuration and environment variables¶

Consolidated index of environment variables across the four platform repos, with the cross-repo contracts called out first — those are the settings where a mismatch between two repos causes a silent or confusing production failure.

Names and defaults only

This page documents variable names, defaults, and which repos must agree. Never record secret values here. Real values live in .env files (gitignored), AWS Secrets Manager, or the ECS task role.

Per-repo templates are the authoritative source:

Repo	Template
verilib-frontend	`.env.example`, `docker/compose.env`, `docker/.env.stack`
verilib-atomizer	`deploy/config/example.env`
local_validate	`.env.example`
verilib-cli	`.verilib/config.json` — see CLI config and files

Cross-repo contracts¶

These must match across repos. Each row is a real failure mode, not a style preference.

Contract	Frontend	Atomizer	Cert worker	What breaks on mismatch
RabbitMQ vhost	`RABBITMQ_VHOST` (default `verilib`)	`RABBITMQ_VHOST`	`RABBITMQ_VHOST` (required, no default)	Peers connect successfully to different vhosts and silently exchange no messages. The cert worker deliberately refuses to start without an explicit value rather than fall back.
Cert manifest bucket	`S3_CERT_BUCKET`	—	`S3_BUCKET`	The frontend health-checks its bucket at startup and cannot fetch manifests the worker wrote elsewhere. Note the different variable names for the same bucket.
Repo tree bucket	(upload target)	`S3_BUCKET`	`S3_REPOS_BUCKET`	The cert worker downloads the parent repo tree from where the atomizer wrote it; a mismatch means "tree not found" on every certify.
GitHub token encryption	`JWT_KEY`	`GITHUB_TOKEN_ENCRYPTION_KEY` or `JWT_KEY`	—	The upload processor cannot decrypt the ciphertext the frontend put on the message; every private-repo clone fails.
Queue topology arguments	`BaseQueue.php`	`broker/topology.py`	`broker/topology.py`	RabbitMQ 406 `PRECONDITION_FAILED` closes the channel of whichever peer declares second.
Queue / exchange names	Queue classes	`<PREFIX>_EXCHANGE` / `_QUEUE` / `_ROUTING_KEY`	same	Messages published to an exchange nobody consumes. Override only in lockstep.
Probe schema version	—	Schema 3.0 parsers	Schema 3.0 manifest	Parse failures after a probe upgrade — see Probe ecosystem.

`PROOF_LANGUAGE_ID_MAP` is environment-specific¶

proof_language_id on an atomize.request selects the probe. The mapping is configuration, not a stable contract, and the two tracked values differ:

Source	Value
Code default / `docs/protocols/atomize.md`	`1:Rust,2:Lean,3:Aeneas`
`deploy/config/example.env` (deployment)	`10:Rust,2:Lean,11:Aeneas`

Read the deployed value before assuming 1/2/3. The ids correspond to rows in the frontend's languages table, so they diverge whenever that table is seeded differently.

RabbitMQ¶

Shared by the atomizer and cert workers (broker/config.py in both repos).

Variable	Default	Notes
`RABBITMQ_HOST`	(required)
`RABBITMQ_PORT`	`5672`
`RABBITMQ_VHOST`	required in local_validate; `/` in atomizer code; `verilib` in frontend and deploy example	See the contract table above.
`RABBITMQ_USER` / `RABBITMQ_PASSWORD`	`guest` / `guest`	In production these come from AWS Secrets Manager via `RABBITMQ_SECRET_ARN`, never from a file.
`RABBITMQ_TLS`	`0`
`RABBITMQ_PREFETCH`	`1`	Kept at 1 so a slow message can't starve sibling workers.
`RABBITMQ_HEARTBEAT`	`60`
`RABBITMQ_CLIENT_NAME`	per repo	e.g. `verilib-local-validate`.
`RABBITMQ_MGMT_PORT`	`15672`	Management API, polled by the queue-depth Lambda.

Queue name overrides follow <PREFIX>_EXCHANGE / _QUEUE / _ROUTING_KEY for each of UPLOAD_REQUEST, UPLOAD_RESPONSE, ATOMIZE_REQUEST, ATOMIZE_RESPONSE, LIVELOG, VALIDATE_REQUEST, VALIDATE_RESPONSE, VALIDATE_LIVELOG, PROMOTE_REQUEST, PROMOTE_RESPONSE. Full inventory: Message contracts.

S3¶

Variable	Repos	Default	Notes
`S3_BUCKET`	atomizer, cert worker	(required)	Different meaning per repo: repo trees in the atomizer, cert manifests in the worker.
`S3_REPOS_BUCKET`	cert worker	`verilib-repos`	Where the atomizer's uploaded trees live.
`S3_CERT_BUCKET`	frontend	—	Must equal the cert worker's `S3_BUCKET`.
`AWS_REGION`	all	`us-east-1`	The deploy example uses `eu-north-1`.
`S3_ENDPOINT_URL`	all	blank = real AWS	Set for MinIO / S3-compatible backends.
`S3_MAX_CONCURRENCY`	cert worker	`8`
`AWS_ACCESS_KEY_ID` / `AWS_SECRET_ACCESS_KEY`	local dev only	—	Production uses the ECS task IAM role; no keys are set.

Key layouts: repo trees at s3://<bucket>/<repo_id>/, cert artifacts at s3://<bucket>/cert/<repo_id>/<filename>.

Database (frontend and legacy atomizer paths only)¶

Variable	Notes
`DB_HOST`	MySQL host. Amazon RDS endpoint in production; the Compose service name (`mysql`) in local development. See Managed.
`DB_PORT`	`3306`. Define it once — see the warning below.
`DB_NAME`, `DB_USER`	`verilib` in both RDS and the Compose stack.
`DB_PASSWORD`	The RDS master password for that environment; the Compose default locally. Read from the host's gitignored `.env` — see Managed → Credentials.
`DB_TYPE`	Frontend; e.g. `eloquent`.

A duplicate DB_PORT breaks auth while pages still work

The frontend's two connection sites disagree about the port: public/core/Database.php builds the PDO DSN without a port (driver default 3306), while public/api/user/User.php passes DB_PORT to mysqli_connect. A leftover second DB_PORT= line later in .env wins, so PDO queries keep reaching the database while the auth API connects to the wrong port — which presents as a failed login or an unrendered page rather than a connection error. Keep exactly one DB_PORT= line — 3306, unless a local stack has been remapped to publish MySQL elsewhere.

Dotenv is immutable — restart PHP after changing DB_*

public/bootstrap.php loads the env file in immutable mode, so a variable already in the PHP process environment overrides the file. Reload PHP-FPM and Apache, and restart the DB-writing workers (upload_response, atomize_response, validate_response, livelog, validate_livelog), or the old connection settings stay live.

Compose-only variables¶

These configure the containers themselves, not the PHP application, so they live in the file passed as --env-file rather than in the app's .env. The full local stack reads docker/.env.stack (committed defaults):

Variable	Notes
`MYSQL_VERSION`	Tag for the `mysql` image — keep it on 8.0 to match the schema dump.
`MYSQL_DATABASE`, `MYSQL_USER`, `MYSQL_PASSWORD`, `MYSQL_ROOT_PASSWORD`	Consumed by the MySQL image on first start to create the database and user. They seed the container; the app still reads `DB_NAME` / `DB_USER` / `DB_PASSWORD`, so the two sets must agree. Changing them after the volume exists has no effect until the volume is recreated.
`APACHE_VERSION`	Tag for the Apache image.
`PROJECT_ROOT`	Host path mounted as the document root.

The older docker-compose.yml path uses .env.docker.dev, which spells the same MySQL values DB_NAME / DB_USERNAME / DB_PASSWORD / DB_ROOT_PASSWORD plus COMPOSE_PROJECT_NAME. Note DB_USERNAME there is the container-seeding name, distinct from the application's DB_USER.

The cert workers have no DB_* variables at all — that is a deliberate architectural property, not an omission. See Worker.

Probes¶

Variable	Default	Notes
`ATOMIZER_LANGUAGES`	`Rust,Lean,Aeneas`	Which plugins to enable. Deploy example uses `Lean,Aeneas,Rust`.
`PROOF_LANGUAGE_ID_MAP`	see above
`PROBE_VERUS_BIN`	`~/.cargo/bin/probe-verus`	Native binary (local mode).
`PROBE_LEAN_BIN`	`~/.elan/bin/probe-lean`
`PROBE_AENEAS_BIN`	`~/.cargo/bin/probe-aeneas`
`PROBE_VERUS_DOCKER_IMAGE`	`probe-verus:latest`	Docker image — preferred over the native binary when set.
`PROBE_LEAN_DOCKER_IMAGE`	`probe-lean:latest`
`PROBE_AENEAS_DOCKER_IMAGE`	`probe-aeneas:latest`
`PROBE_VERUS_VERSION` / `PROBE_AENEAS_VERSION` / `PROBE_LEAN_VERSION`	e.g. `6.10.1` / `0.11.0` / `latest`	Image tags built by `build_and_push.sh`.
`PROBE_OUTPUT_DIR`	`./probe-out`	Cert worker; manifest read from `<dir>/cert<repo_id>/probe-manifest-complete.json`.
`PROBE_DOCKER_*` (+ `_LEAN` / `_AENEAS`)	—	Cert worker build/run/push controls.
`WORKER_REQUIRE_DOCKER`	—	Entrypoint check; the atomize processor needs a host Docker socket.
`LEAN_REPO_LANGUAGE_ID`, `AENEAS_REPO_LANGUAGE_ID`	—	Cert worker probe-kind resolution.

Runtime and retries¶

Variable	Default	Notes
`CLI_TIMEOUT`	`4800`	Probe subprocess timeout in seconds. Must stay ≤ the broker's `consumer_timeout` or RabbitMQ kills the channel mid-probe.
`UPLOAD_MAX_RETRIES`	`5`
`ATOMIZE_MAX_RETRIES`	`5` (deploy example: `3`)
`JOB_MAX_ATTEMPTS`	`5`	Cert workers.
`UPLOAD_WORKDIR` / `ATOMIZE_WORKDIR`	system tmp	Ephemeral scratch; see Disk cleanup.
`WORKDIR_ROOT`	`/var/verilib/work`	Host path bind-mounted into the ECS task.
`POLL_INTERVAL`, `MAX_WORKERS`, `MAX_RETRIES`, `DEFAULT_USER_ID`, `REPOS_BASE_PATH`	—	Legacy DB-poll mode only. Not used by queue workers.

Frontend¶

Variable	Notes
`USE_NEW_UI_TOOLS`	`1` = Gulp bundles under `public/assets/dist/`; `0` = legacy `public/assets/js/` + `style/`.
`MODE`	`development` or `production` — controls asset fingerprinting.
`USE_AUTH_SYSTEM`	Enable auth.
`SHOW_ERRORS`, `DEBUG_MODE`	Dev diagnostics. Must be off in production.
`SOCKET_URL`, `SOCKET_PORT`	PHP WebSocket service (`socket.php`).
`JWT_KEY`	JWT signing material and the GitHub-token encryption key fallback — see the contract table.
`SENDGRID_API_KEY`	Outbound email (optional).
`UPLOADER`, `UPLOADER_BASE_PATH`	Upload backend mode (e.g. `local`).
`CLI_EXCHANGE`, `CLI_QUEUE`, `CLI_ROUTING_KEY`	CLI traffic queue wiring (`cli_exchange` / `cli_queue` / `cli_routing_key`).
`GITHUB_APP_CLIENT_ID`, `GITHUB_APP_CLIENT_SECRET`	GitHub App OAuth; also optionally set on the upload processor for in-memory token refresh during clone.

On-chain (cert worker only)¶

Group	Variables
Sepolia	`ETH_CERTIFY_ENABLED`, `SEPOLIA_RPC_URL`, `SEPOLIA_PRIVATE_KEY` (or `PRIVATE_KEY`), `CERTIFY_ADDRESS`, `ETH_CERTIFY_CHAIN_ID` (default `11155111`), `ETH_CERTIFY_DEDUP_FROM_BLOCK`, `ETH_CERTIFY_DEDUP_REQUIRED` (default fail-open)
Mainnet	`MAINNET_CERTIFY_ENABLED`, `MAINNET_RPC_URL`, `MAINNET_CERTIFY_ADDRESS`, `MAINNET_PRIVATE_KEY` (or `MAINNET_CERTIFY_PRIVATE_KEY`), `ETH_MAINNET_CHAIN_ID` (default `1`), `MAINNET_CERTIFY_DEDUP_FROM_BLOCK`, `MAINNET_CERTIFY_DEDUP_REQUIRED` (default fail-closed)

The asymmetry is deliberate: mainnet spends real gas, so if the dedup scan cannot confirm the bundle is new, the job retries rather than risk a duplicate anchor. Set *_DEDUP_FROM_BLOCK to the Certify deploy block — public RPCs cap eth_getLogs ranges and an earliest scan will fail. See Certify contract.

Deployment (atomizer AWS)¶

Non-secret per-environment config in deploy/config/<env>.env:

Variable	Example	Notes
`ENV_NAME`	`dev`	Used in resource names.
`AWS_ACCOUNT_ID`, `AWS_REGION`	—
`CLUSTER_NAME`	`verilib-atomizer-dev`	ECS cluster.
`DESIRED_COUNT`	`1`	Initial task count; the autoscaler manages it after.
`TASK_ROLE_NAME`, `EXECUTION_ROLE_NAME`	—	Created manually; ARNs derived from the account id.
`RABBITMQ_SECRET_ARN`	full ARN incl. 6-char suffix	Secrets Manager entry holding `RABBITMQ_USER` / `RABBITMQ_PASSWORD`.
`IMAGE_TAG`	`latest` or a git sha
`WORKER_REPO`, `PROBE_*_REPO`	`verilib/worker`, …	ECR repository names.
`ATOMIZE_MIN_TASKS` / `ATOMIZE_MAX_TASKS`	`1` / `10`
`UPLOAD_MIN_TASKS` / `UPLOAD_MAX_TASKS`	`1` / `5`
`ATOMIZE_TARGET_MSG_PER_CONSUMER`	`0.5`	See the note below.
`UPLOAD_TARGET_MSG_PER_CONSUMER`	`1`	Uploads are short; tolerate ~1 queued message per worker.
`LAMBDA_FUNCTION_NAME`, `LAMBDA_ROLE_NAME`, `LAMBDA_SCHEDULE_RATE`, `METRIC_NAMESPACE`	`verilib-queue-depth-publisher`, …, `1 minute`, `Verilib/RabbitMQ`	Queue-depth publisher.

Target-tracking targets must be below 1

Target tracking keeps the metric at the target, not below it. ATOMIZE_TARGET_MSG_PER_CONSUMER=1 means "one backlog message per worker is acceptable — don't scale". Use a value < 1 (0.5 is the tracked default) for "scale out as soon as a second message waits". The value must be > 0; target tracking forbids 0.

Per-service CPU/memory are hardcoded in deploy/templates/*.taskdef.json rather than exposed here, because they encode the Docker-out-of-Docker packing rule: the atomize processor must reserve enough RAM to cover the probe container it spawns via /var/run/docker.sock.