Skip to content

Admin Probe Version Manager — Interface Spec & Implementation Plan

Purpose

VeriLib runs multiple proof languages (Lean, Verus, Aeneas, Dafny, …). Each language can have several installed probe / verifier toolchain versions. Today those versions are stored in verifierversions and selected per repo via repos.verifierversion_id, but there is no admin UI to manage them, no write API, and no way to install new probe releases without manual backend work.

This document defines an admin interface in VeriLib FE (role-gated) that lets authorized users:

  • See which probe versions are installed on the atomizer backend
  • Control which versions are available for selection
  • Set defaults at global (per proof language), user, or repo scope
  • Request download / installation of newer probe releases from the backend

The atomizer worker remains responsible for actually running probes; the frontend and VeriLib API own catalog, policy, and defaults.

Problem statement

Constraint Why it matters
One probe version per language is not enough Lean 4.7 vs 4.14, Verus stable vs prerelease, Aeneas pins, etc.
Repos need different versions Experiments, migration, customer-specific pins
Deploying a new probe today is operational Requires backend/infra changes; no self-service path for admins
Upload UI already exposes a version dropdown Data comes from GET /v2/verifier/versions/{prooflanguage_id} but catalog is static / DB-seeded

Goal: make probe version management a first-class admin capability without blocking on a full "admin portal" — start with probe versions only; other admin tools can follow the same pattern.

Current state (VeriLib FE)

Version selection flow

  1. Upload / edit UI loads proof languages from GET /v2/languages.
  2. UI loads versions from GET /v2/verifier/versions/{prooflanguage_id} (VerifierController::getVersions).
  3. User picks verifierversion_id; stored on repos.verifierversion_id.
  4. Queue messages (UploadRequestMessage, UploadAtomizeRequest) carry verifier_version_id and verified_version (string from verifierversions.version).
  5. External atomizer worker maps verified_version → Docker image / probe binary (outside this repo).

Data model

verifierversions (no formal migration in sql/; seeded in dev):

Column Usage
id PK; repos.verifierversion_id FK
language_id Filter for listing — semantics inconsistent (seed uses 'lean' string; API receives numeric proof language id)
version Toolchain string sent to worker (e.g. 4.7.0, stable)
sortorder Display order
user_id Creator / audit

repos.verifierversion_id — per-repo selection.

Separate: versions table (compiler display versions) — not probe versions.

Authorization patterns to reuse

Pattern Location Notes
Platform role users.role_id (1=admin, 2=moderator, 3=user) Admins bypass unpublished repo access
Task permissions tasks + permissions e.g. Project Admin (tasks.slug), Feature Repo, Certifier
Slug-scoped admin API ProjectScreenController GET/PUT /v2/project-screen/:slug, Users::userCanAdminProjectScreen()
Repo RBAC PermissionsConfig, RBACMiddleware Owner/editor/viewer — not for platform admin

Gaps

  • Read-only version API; no CRUD
  • No admin permission task for probe management
  • No UI beyond upload dropdown
  • language_id on verifierversions vs numeric prooflanguage_id mismatch
  • Changing verifierversion_id on repo update does not auto re-atomize
  • Version list endpoint is unauthenticated
  • Worker install / download not exposed via API
  • TS type VerifierVersion.prooflanguage_id does not match API response

Target architecture

┌─────────────────────────────────────────────────────────────────┐
│  VeriLib FE — Admin Probe Version Manager (React)               │
│  /admin/probe-versions  (role: Probe Version Admin or admin)    │
└────────────────────────────┬────────────────────────────────────┘
                             │ REST
┌────────────────────────────▼────────────────────────────────────┐
│  VeriLib API (verilib-frontend)                                   │
│  • Catalog CRUD (verifierversions + defaults)                   │
│  • Proxy: list installed probes on atomizer                       │
│  • Proxy: trigger probe download / install                        │
└────────────┬───────────────────────────────┬────────────────────┘
             │                               │
             ▼                               ▼
┌────────────────────────┐    ┌────────────────────────────────────┐
│  MySQL                  │    │  Atomizer admin API (new)          │
│  verifierversions       │    │  GET  /admin/probes/installed      │
│  probe_defaults (new)   │    │  GET  /admin/probes/releases       │
│  users / repos pins     │    │  POST /admin/probes/install        │
└────────────────────────┘    └────────────────────────────────────┘
             │
             ▼
┌────────────────────────┐
│  Queue workers          │
│  upload / atomize       │  ← consume verified_version from message
└────────────────────────┘

Separation of concerns

  • FE: catalog UI, defaults UI, install requests, audit display
  • VeriLib API: permissions, persistence, validation, orchestration
  • Atomizer: filesystem / Docker images, listing installed artifacts, pulling releases

Admin interface specification

Access

  • Route: /admin/probe-versions (or under existing admin nav when it exists)
  • Visible only if Users::userCanManageProbeVersions($userId) or users.role_id === 1 (admin)
  • All mutating API routes require the same check + session auth
  • Non-admins: 404 or redirect (prefer 404 to avoid leaking feature existence)

Page layout

  • Title: Probe versions
  • Subtitle: manage installed probe toolchains and defaults per proof language

Section A — Proof language selector

  • Tabs or dropdown: Lean, Verus, Aeneas, Dafny, … (from GET /v2/languages where type is proof or both)
  • Shows active proof language id (numeric, canonical)

Section B — Installed catalog (VeriLib DB)

Table columns:

Column Description
Version verifierversions.version (display + worker string)
Label Optional human label (new column)
Docker tag / artifact ref Optional mapping for worker (new column)
Status available / disabled
Default badge if global default for this language
Sort order drag or numeric
Installed on backend yes/no (from atomizer installed list)
Actions Edit, Disable, Set as default, Delete (if unused)

Actions:

  • Add version — manual row (version string, label, docker tag, sort order)
  • Sync from backend — merge atomizer installed list into catalog (mark installed, offer import)
  • Set as global default — writes probe_defaults row

Section C — Available upstream releases (atomizer)

  • List from atomizer GET /admin/probes/releases?language=lean (or proof language key)
  • Columns: release tag, published date, already installed
  • Action: Install → POST install on atomizer, poll job status, refresh installed list
  • Optional: Install and add to catalog — install + create verifierversions row + set available

Section D — Defaults hierarchy (read-focused v1; edit in v2)

Display effective default resolution for selected language:

  1. Repo override (repos.verifierversion_id when set explicitly)
  2. User override (new: user_probe_defaults)
  3. Global default (probe_defaults)

v1 can show global default only; repo/user overrides remain existing upload flow until phase 2.

Section E — Audit / activity (optional v1)

  • Last install request, user, timestamp, outcome
  • Stored in probe_install_jobs or atomizer callback

Upload / edit repo UX (consumer, not admin page)

  • Dropdown continues to use GET /v2/verifier/versions/{prooflanguage_id} but returns only available versions, sorted by sortorder
  • Pre-select: repo's verifierversion_id, else resolved default for user/language
  • If repo's pinned version is disabled, show warning + force re-select

Data model changes

Migration sql/34.sql (proposed)

Fix and extend verifierversions:

-- Canonical FK to languages.id (proof language)
ALTER TABLE verifierversions
  ADD COLUMN prooflanguage_id INT NULL AFTER id,
  ADD COLUMN label VARCHAR(128) NULL AFTER version,
  ADD COLUMN docker_tag VARCHAR(128) NULL AFTER label,
  ADD COLUMN is_available TINYINT(1) NOT NULL DEFAULT 1 AFTER docker_tag,
  ADD COLUMN created_at TIMESTAMP NOT NULL DEFAULT CURRENT_TIMESTAMP,
  ADD INDEX idx_verifierversions_prooflanguage (prooflanguage_id, sortorder);

-- Backfill prooflanguage_id from legacy language_id where possible
-- (one-time UPDATE joining languages.name — run in migration script)

Global defaults:

CREATE TABLE probe_defaults (
  prooflanguage_id INT NOT NULL PRIMARY KEY,
  verifierversion_id INT NOT NULL,
  updated_at TIMESTAMP NOT NULL DEFAULT CURRENT_TIMESTAMP ON UPDATE CURRENT_TIMESTAMP,
  updated_by INT NULL,
  FOREIGN KEY (verifierversion_id) REFERENCES verifierversions(id)
);

User defaults (phase 2):

CREATE TABLE user_probe_defaults (
  user_id INT NOT NULL,
  prooflanguage_id INT NOT NULL,
  verifierversion_id INT NOT NULL,
  PRIMARY KEY (user_id, prooflanguage_id)
);

Install job log (optional):

CREATE TABLE probe_install_jobs (
  id INT AUTO_INCREMENT PRIMARY KEY,
  prooflanguage_id INT NOT NULL,
  release_tag VARCHAR(128) NOT NULL,
  status ENUM('pending','running','succeeded','failed') NOT NULL DEFAULT 'pending',
  requested_by INT NULL,
  atomizer_job_id VARCHAR(64) NULL,
  error_message TEXT NULL,
  created_at TIMESTAMP NOT NULL DEFAULT CURRENT_TIMESTAMP,
  finished_at TIMESTAMP NULL
);

Permissions seed:

INSERT INTO tasks (label, description, slug, sortorder, server, user_id)
SELECT 'Probe Version Admin', 'Manage probe versions and defaults', 'probe-versions', 54, '0', NULL
FROM DUAL WHERE NOT EXISTS (SELECT 1 FROM tasks WHERE slug = 'probe-versions');

INSERT IGNORE INTO permissions (task_id, workeruser_id, status, manageruser_id)
SELECT t.id, u.id, 1, NULL
FROM users u JOIN tasks t ON t.slug = 'probe-versions'
WHERE u.role_id = 1;

Backend API (VeriLib FE)

Public / upload (existing, hardened)

Method Path Change
GET /v2/verifier/versions/{prooflanguage_id} Filter is_available=1; fix join on prooflanguage_id; require auth optional (recommend auth)

Admin catalog

Method Path Description
GET /v2/admin/probe-versions List all versions; query ?prooflanguage_id=
POST /v2/admin/probe-versions Create catalog entry
PUT /v2/admin/probe-versions/{id} Update label, docker_tag, sortorder, is_available
DELETE /v2/admin/probe-versions/{id} Soft-delete or hard-delete if no repos reference
PUT /v2/admin/probe-defaults/{prooflanguage_id} Set global default { verifierversion_id }
GET /v2/admin/probe-defaults List global defaults

All routes: CheckUserMiddleware + Users::userCanManageProbeVersions().

Atomizer proxy (VeriLib → atomizer)

Method Path Description
GET /v2/admin/probe-versions/installed Proxy atomizer installed list
GET /v2/admin/probe-versions/releases Proxy upstream releases
POST /v2/admin/probe-versions/install Body: { prooflanguage_id, release_tag }; creates job row, calls atomizer

Implement in ProbeVersionController mirroring ProjectScreenController structure.

Users.php addition:

public static function userCanManageProbeVersions(?int $userId): bool
{
    if ($userId === null) return false;
    if (/* role_id === 1 */) return true;
    return self::userHasTaskPermission($userId, 'Probe Version Admin');
}

Atomizer backend (separate repo — contract)

New admin endpoints on atomizer service (authenticated service-to-service or forwarded user token):

Method Path Description
GET /admin/probes/installed [{ language, version, docker_tag, path, installed_at }]
GET /admin/probes/releases Query language; list GitHub/container registry releases
POST /admin/probes/install { language, release_tag } → async job id
GET /admin/probes/install/{job_id} Job status

Install script (atomizer): CLI or internal module that:

  1. Resolves release tag for language (Lean toolchain repo, Verus image, Aeneas pin file, …)
  2. Pulls Docker image or downloads binary bundle
  3. Registers installed version in local manifest (atomizer reads this when validating queue messages)

VeriLib FE does not pull images directly; it only triggers atomizer.

Frontend implementation (React)

New files

File Purpose
src/pages/admin/ProbeVersionAdmin.tsx Main page
src/components/admin/ProbeVersionTable.tsx Catalog table
src/components/admin/ProbeReleasePanel.tsx Upstream releases + install
src/components/admin/ProbeDefaultSelector.tsx Global default control
src/services/probeVersionApi.ts Admin API client
Route in App router /admin/probe-versions

Patterns to copy

  • Permission gate: same as Signal Shot can_edit from API, or load GET /v2/admin/probe-versions/meta returning { can_manage: bool }
  • Forms: SignalShotConfigEditor modal pattern for edit row
  • Tables: repo stats / upload form select options

API hooks

  • useQuery(['probeVersions', prooflanguageId])
  • useMutation for create/update/install with toast + refetch
  • Poll install job status every N seconds until terminal state

Today RepoController::update does not re-queue atomize when only verifierversion_id changes.

Add:

  • If verifierversion_id changes and user confirms (or admin policy flag), enqueue re-atomize similar to POST /v2/repo/reatomize/:repo_id
  • Upload UI: checkbox "Re-run atomization with new probe version"

Document in admin UI that changing global default does not mutate existing repos.

Implementation plan

Phase 1 — Catalog & permissions (foundation)

Database

  • Add sql/34.sql: extend verifierversions, create probe_defaults, task + permission seed
  • Backfill prooflanguage_id from legacy language_id values

Backend

  • ProbeVersionController with GET/POST/PUT/DELETE catalog + GET/PUT defaults
  • Users::userCanManageProbeVersions()
  • Fix VerifierController::getVersions to query prooflanguage_id and is_available=1
  • Register routes in public/app/routes.php with auth middleware

Frontend

  • Admin page: language tabs, catalog table, add/edit/disable, set global default
  • No atomizer install yet — manual DB / seed still OK

Exit criteria

  • Admin can enable/disable versions and set global default per proof language
  • Upload dropdown reflects catalog changes
  • Only Probe Version Admin (and platform admin) can access admin routes

Phase 2 — Atomizer integration (install & sync)

Atomizer repo

  • Implement installed list, releases list, install job API
  • Manifest file co-located with worker images

VeriLib API

  • Proxy endpoints + probe_install_jobs logging
  • "Sync from backend" merges installed into catalog

Frontend

  • Releases panel, Install button, job status polling
  • "Installed on backend" column populated

Exit criteria

  • Admin can install a new release from UI without SSH / hackathon deploy
  • Installed state visible in catalog

Phase 3 — Defaults hierarchy & repo pins

Database

  • user_probe_defaults table

Backend

  • CRUD for user defaults (admin sets for any user, or user self-service later)
  • Helper ProbeVersionResolver::resolve($userId, $repoId, $prooflanguageId) used by upload create + edit-info

Frontend

  • User default column in admin (optional)
  • Upload form: show effective default source (repo / user / global)

Repo update

  • Re-atomize on version change (with confirmation)

Exit criteria

  • New repos get correct default without manual dropdown selection
  • Per-repo override still works via existing upload/edit

Phase 4 — Hardening & ops

  • Authenticate public version list or rate-limit
  • Prevent delete of version referenced by repos (FK or check + archive)
  • Audit log for catalog changes
  • Align TS types with API (VerifierVersion includes prooflanguage_id, is_available, label)
  • Documentation for mapping version string → worker Docker tag per language
  • Staging/prod migration runbook (sql/34.sql via scripts/run-migrations.sh)

Open decisions

Decision Options Recommendation
Admin vs moderator Probe Version Admin task only vs role_id=1 only Task + auto-grant admins (same as Project Admin)
Delete vs disable Hard delete vs is_available=0 Disable only; delete if zero repo references
language_id migration Backfill vs new column only Add prooflanguage_id, deprecate language_id
Install scope Per language server vs global atomizer pool Match current queue partition (Lean/Aeneas/Verus workers)
User self-service defaults Phase 3 admin-only vs user settings page Admin-only first
Area Path
Version list API public/app/Controllers/Verifier/VerifierController.php
Upload version pick react-graph-standard/src/components/upload/UploadForm.tsx
Repo version field public/app/Controllers/Repo/RepoController.php
Queue payload public/app/Lib/Queue/UploadRequestMessage.php
Permission pattern public/app/Models/Users.php, sql/32.sql
Admin screen pattern public/app/Controllers/ProjectScreen/ProjectScreenController.php
Atomize consumer public/app/Services/AtomizeService.php

Out of scope (for this feature)

  • Full general-purpose admin portal (users, queues, certificates, featured repos)
  • Cert page hardcoded probe_verus_version manifests (stats.php, cert5050) — separate unification
  • Automatic upgrade of all repos when global default changes
  • Probe version management inside atomizer worker runtime (only install/list API)

Success metrics

  • Admin can add/disable a probe version without DB access
  • Admin can install a new release without infra SSH
  • Upload flow shows only allowed versions for selected proof language
  • Existing repos keep their pin until explicitly changed or re-atomized
  • Clear audit trail of install requests and catalog edits