Skip to content

Schema

The MySQL schema lives in verilib-frontend — it is a frontend-owned database, not a shared one. The rest of the docs reference its tables constantly (repos.status_id, certificates.status=pending, atomsdependencies); this page defines them.

How this page was derived

There is no checked-in base DDL in the repo. The full schema is applied from a db.sql dump provided out of band (see the full-stack Compose file). What is tracked and verifiable: the Eloquent models under public/app/Models/, the incremental migrations in sql/, and the dev seed docker/seed-dev.sql.

Column lists below come from those sources. Treat them as the shape, not an exhaustive DDL — check the deployed schema for exact types, nullability, and indexes.

Entity model

erDiagram
  users          ||--o{ repos        : owns
  users          ||--o{ apikeys      : has
  users }o--||     roles             : role_id
  users          ||--o{ permissions  : granted
  tasks          ||--o{ permissions  : gates
  repos          ||--o{ codes        : contains
  repos          ||--o{ reposfolders : "folder tree"
  repos          ||--o{ reposhares   : "shared with"
  repos          ||--|| repostats    : "progress snapshot"
  repos          ||--o{ molecules    : groups
  repos          ||--o{ atoms        : contains
  repos          ||--o{ certificates : "snapshot of"
  codes          ||--o{ atoms        : "declares"
  codes          ||--o{ packages     : exposes
  packages       ||--o{ snippets     : has
  atoms          ||--o{ atomsdependencies : "parent edge"
  atoms          ||--o{ atomissues   : has
  atoms          ||--o{ atomslabel   : tagged
  atoms          ||--o{ bounties     : "open on"
  labels         ||--o{ atomslabel   : applied
  languages      ||--o{ codes        : language_id
  languages      ||--o{ verifierversions : versions
  types          ||--o{ codes        : type_id
  statuses       ||--o{ repos        : status_id
  statuses       ||--o{ codes        : status_id
  statuses       ||--o{ atoms        : status_id
  jobs           ||--o{ joblogs      : logs

Core tables

repos

The unit a user uploads and the platform atomizes. repos.id doubles as the S3 prefix for the uploaded tree (s3://<bucket>/<repo_id>/) and as the addressing key on every queue message.

id, summary, description, url, branch, pubtime, status_id, user_id, verifierversion_id

Private-repo GitHub OAuth ciphertext is also stored on this table (github_access_token, github_refresh_token, github_token_expires_at, github_auth_login, github_repo_visibility) and copied onto the queue message rather than read from here by the worker. See Message contracts.

codes

A source file within a repo.

id, summary, description, language_id, prooflanguage_id, type_id, status_id, repo_id, folder_id, filepath, pubtime, user_id, numlines

prooflanguage_id is what becomes proof_language_id on an atomize.request and selects the probe — via a configurable map, not a fixed one. See PROOF_LANGUAGE_ID_MAP.

atoms

One declaration — the node type behind everything the graph UI draws.

id, identifier, full_identifier, statement_type, code_id, repo_id, parent_id, level, type, status_id, specified, disabled, user_id, scip

Column Maps to probe field
full_identifier the atom's code-name URI key in the Schema 3.0 data map
identifier display-name
type / statement_type kind
specified derived from specs / primary-spec
disabled untracked (is-disabled pre-Schema 3.0)
status_id derived from verification-status

See JSON mapping and Probe ecosystem.

atomsdependencies

The graph edges.

parentatom_id, childatom_id, sortorder, user_id, primaryspec

One row per dependency in an atom's dependencies array. primaryspec marks the edge to the atom's primary specification.

certificates

A frozen, certified snapshot of a repo. Written only by PHP — the cert workers never touch MySQL.

Column Notes
status A varchar, not a statuses FK. pending on insert; ready or an error state after validate.response. Compared as LOWER(TRIM(status)).
manifestSha256 Hash of probe-manifest-complete.json — the value anchored on-chain.
dalekLiteResolvedCommit The commit the probe image actually baked.
dockerHubImageDigest sha256:… of the published probe image.
sepoliaCertifyTxHash varchar(78), nullable.
mainnetCertifyTxHash varchar(78), nullable.
chainScope varchar(32), default unset. One of unset, testnet_only, mainnet_only, testnet_and_mainnet.
mainnetMigrationStatus varchar(32), default none. One of none, pending, complete.

chainScope and mainnetMigrationStatus were added by scripts/sql/certificates_chain_scope_migration.sql, which backfills scope from the existing tx-hash columns and marks ready + testnet_only rows as pending promotion. Those three hash columns are exactly what the frontend puts on a promote.request so the worker stays DB-free.

Access control

Table Columns Notes
roles seeded 1 admin, 2 moderator, 3 user See Roles
tasks id, label, description, sortorder, server, user_id Seeded platform tasks include 45 Feature Repo, 46 Certifier
permissions task_id, workeruser_id, status, manageruser_id Per-user grant of a task. See Permissions

Supporting tables

Table Role
users id, email, name, realname, firstname, lastname, pwdhash, role_id, mailinglistinfo
apikeys user_id, hash, name — CLI authentication
reposfolders id, name, repo_id, parent_id, user_id — repo browser tree
reposhares repo_id, user_id, email
repostats repo_id, total_functions, extracted, verified, spec_only, draft, not_started, snapshot_date — the progress chart series
atomlayouts layout, repo_id, parent_id, user_id — saved graph layouts
molecules id, name, repo_id, sortorder, user_id — atom groupings
packages / snippets Published code units and their text
atomissues / labels / atomslabel Per-atom issues and tagging
bounties atom_id, claimuser_id, text, claimed_amount, status
jobs / joblogs joblogs is where livelog messages land (log, element_id, logtype, process_id)
languages / versions / verifierversions / types / statuses Lookup tables
comments, codesratings, applications, codeapplications, actions, ranges, updates, atomizerlogs Secondary features

Write ownership

The architecture rests on a strict division of who may write what. This is an invariant, not a convention — breaking it is how the platform gets inconsistent.

Tables Writer Notes
certificates PHP frontend only Applies validate.response / promote.response. The cert workers have no DB_* env vars at all.
atoms, atomsdependencies, atom snippets, codes verification fields atomizer (atomize-processor) Written directly during persistence.
repos (status, S3 metadata, GitHub tokens) PHP frontend Applies upload.response.
joblogs PHP frontend Consumes livelog.
Everything else (users, permissions, bounties, labels, …) PHP frontend Product surface.
Component DB access
verilib-frontend Read/write — sole writer for everything except atoms
verilib-atomizer Read/write — atoms, dependencies, code verification status
local_validate None. DB-free by design
verilib-cli None — talks to the API

Migrations

Numbered plain-SQL files in sql/, applied in order: 1.sql … 25.sql. There is no migration framework, no migrations tracking table in the repo, and no down-migrations.

Things to know before adding one:

  • The sequence has a gap — there is no 17.sql.
  • One file is out of band — 6_backfill_usernames.sql is a data backfill paired with 6.sql.
  • Some migrations live elsewhere — scripts/sql/ holds standalone migrations (e.g. certificates_chain_scope_migration.sql) with their own apply command in a header comment.
  • Migrations may seed data, not just DDL. sql/23.sql seeds roles; sql/25.sql seeds tasks and grants permissions by role. Both use ON DUPLICATE KEY UPDATE / INSERT IGNORE to stay re-runnable.

To add one: create sql/26.sql, make it idempotent, and put the apply command in a header comment.

Unknowns

Who applies migrations in staging and production, and in what order relative to a deploy, is not documented in the repo. Until Deployment procedure covers it, confirm with the team before applying anything to a shared environment.