Skip to content

GraphQL extract store

VeriLib keeps MySQL as the authoritative store for live repo pages, but dynamic chart blocks need fast, historical reads over atomization snapshots. The GraphQL extract store (verilib-graphql) answers that: after each successful atomize it captures a timestamped snapshot of the probe envelope and serves it through a read-only Hasura GraphQL API.

The stack runs on three dedicated EC2 hosts — VQD (dev), VQS (staging), VQP (prod) — one per VeriLib environment. Each host is self-contained (Postgres + Hasura + ingest relay in Docker Compose) and pairs with the matching frontend and RabbitMQ broker.

Architecture

flowchart LR
  atomize[Atomize completes]
  php[Frontend AtomizeService]
  mq[RabbitMQ graphql.ingest]
  relay[ingest-relay on VQ*]
  s3[(S3 probe JSON)]
  pg[(Postgres extracts + atoms)]
  hasura[Hasura GraphQL :8092]

  atomize --> php
  php -->|fire-and-forget publish| mq
  mq --> relay
  relay --> s3
  relay --> pg
  hasura --> pg
  1. Publish — After atomization commits to MySQL, AtomizeService calls GraphqlIngestPublisher, which pushes a minimal graphql.ingest message to RabbitMQ. Broker failure is logged only; it never rolls back the atomize response.
  2. Ingest — The Python ingest-relay on the paired VQ* host consumes the message, reads the probe JSON from S3, copies a timestamped snapshot key, and appends one extracts row plus atoms rows to Postgres. Ingest is idempotent on (repo_id, content_sha).
  3. Query — Hasura exposes Postgres as GraphQL. Clients send x-hasura-api-key; the auth webhook grants a read-only role.

Object storage remains the source of truth for raw probe envelopes. Postgres stores only the fields charts need, plus precomputed statistics.

Repository and stack

Piece Location
Source repo verilib-graphql
Frontend publisher GraphqlIngestPublisher, GraphqlIngestQueue in verilib-frontend
Trigger point AtomizeService::enqueueGraphqlIngest() after a successful atomize response

Docker Compose services on each VQ* host:

Service Role Default host port
postgres Extract store (extracts, atoms) 5432
graphql-engine Hasura GraphQL API + console 8092
auth-webhook Validates x-hasura-api-key internal only
ingest-relay RabbitMQ consumer + /healthz, /backfill 8081

Environment hosts (VQD / VQS / VQP)

Each GraphQL host is pinned to one VeriLib environment. The relay consumes from that environment's RabbitMQ broker and reads from its S3 probe bucket.

Host SSH alias AWS host (us-east-2) Paired frontend RabbitMQ broker S3 bucket
VQD ssh VQD ec2-52-15-47-42 VD (demo dev) DEV ec2-13-217-33-22 verilib-atomizer
VQS ssh VQS ec2-18-222-200-78 VS (staging) STG ec2-54-89-205-210 staging bucket
VQP ssh VQP ec2-3-15-179-4 VP (verilib.org) PROD ec2-54-174-43-132 verilib-atomizer-prod

Instance type: t3.medium (64 GB root volume). IAM: per-host instance profile (verilib-graphql-vqd, verilib-graphql-vqs, verilib-graphql-vqp) scoped to the paired bucket: read access to probe JSON plus s3:PutObject on */.verilib/probes/extracts/* only, so the relay can write timestamped snapshots. No long-lived access keys on the hosts.

Pages read the store through /api/vq

The Stats UI still reads the PHP REST API, but page blocks (vqstats, vqextracts, vqatoms, and the vq chart source) read this store. The browser never calls Hasura: the Next.js app exposes POST /api/vq, which checks per-repo access with the PHP API and then queries Hasura with a server-side key. Hasura itself has no per-repo ACL, so never ship its API key to the browser. See Dynamic chart pages.

Data model

Table Purpose
extracts One row per atomization snapshot: repo_id, captured_at, commit_sha, pipeline, s3_uri, content_sha, aggregate counters (verified, in_progress, …), and a counters JSON breakdown. Unique on (repo_id, content_sha).
atoms Per-atom rows for grouped and tabular charts: code_path, statement_type, language, verification_status, specified, untracked. FK to extracts.

Schema source: hasura/migrations/default/1000000000000_init/up.sql in the graphql repo.

Message contract (graphql.ingest)

Published by the frontend; consumed only by the ingest-relay. See Message contracts — GraphQL ingest pipeline.

Field Required Notes
event_id yes Fresh UUID per message
request_id yes Echoes the atomize request
repo_id yes Repository id
s3_output_uri yes s3://… pointer to the probe JSON the relay fetches
commit_sha no Git commit when available
metadata.produced_at yes ISO-8601 UTC

Queue declaration is intentionally minimal

Unlike other platform queues, GraphqlIngestQueue declares only the main direct exchange, queue (x-max-priority=10), and bind — no topic retry/error exchanges. The relay must declare the same shape. A mismatch produces 406 PRECONDITION_FAILED and silent publish failures on the PHP side. See GraphQL VQ* ops.

GraphQL access

Endpoint Auth
http://<vq-host>:8092/v1/graphql Header x-hasura-api-key: <GRAPHQL_API_KEY>
http://<vq-host>:8092 (console) HASURA_GRAPHQL_ADMIN_SECRET

Example — latest snapshot stats for a repo:

query ($repo: Int!) {
  extracts(
    where: { repo_id: { _eq: $repo } }
    order_by: { captured_at: desc }
    limit: 1
  ) {
    captured_at
    verified
    verified_trusted
    in_progress
    unspecified
    failed
    atom_count
    counters
  }
}

Example — atoms of the latest snapshot (for table charts):

query ($repo: Int!) {
  extracts(
    where: { repo_id: { _eq: $repo } }
    order_by: { captured_at: desc }
    limit: 1
  ) {
    atoms {
      code_path
      statement_type
      verification_status
      specified
      untracked
    }
  }
}

Local development

git clone https://github.com/Beneficial-AI-Foundation/verilib-graphql.git
cd verilib-graphql
cp .env.example .env   # fill PG, Hasura, S3, RabbitMQ
docker compose up -d --build
curl -s http://localhost:8081/healthz   # {"ok":true}

Point RABBITMQ_* at a reachable broker (or a local RabbitMQ container) and S3_* at a bucket that holds probe JSON. The frontend's GRAPHQL_INGEST_* names must match the relay's .env.