Django-Theorem

The control plane and data science lab for Theorem, an agent harness built on a Rust graph substrate.

Theorem is a rust, rust is the runtime. Django-theorem is how we improve the runtime.

---

Django service for Theorem business/fleet management: tenancy, identity (WorkOS shadow rows), billing, machine API keys, offload orchestration, feature flags, and support notes.

It also owns the authenticated theorem.competence.v1 fit/refit job boundary. The competence worker fits selection-corrected Beta-Bernoulli scorers, publishes content-addressed prior/model artifacts, and exposes inspectable recovery state.

Index discovery and TabICLv2 corpus executors are available through POST /internal/index/execute with offload:invoke machine-key admission. See executor contracts, model provenance and validation.

Stack

• Django 5.x + django-ninja
• Celery (broker: Valkey/Redis)
• argon2-cffi (machine key hashes)
• psycopg (Postgres via PgBouncer)
• RunPod Serverless v2 lifecycle client for GPU/Python workloads
• RunPod Pods REST lifecycle client for long-running Prime-RL jobs
• Separate Fly app and Celery queue offload.r for R workloads (agent name "R")
• Debian Graphviz 2.42.2-7+deb12u1 (linked runtime 2.43.0)/PyGraphviz positions plus bounded PlantUML and Diagrams rendering

Quick start

python3 -m venv .venv
source .venv/bin/activate
pip install -r requirements.txt
cp .env.example .env
python manage.py migrate
python manage.py createsuperuser
python manage.py runserver 0.0.0.0:8001

Celery worker (default queue):

celery -A theorem_control worker -l info

Celery beat (competence sleep-cycle recovery/refit dispatch):

celery -A theorem_control beat -l info

R queue worker (separate image with pinned R + renv + rpy2):

celery -A theorem_control worker -l info -Q offload.r

The deployment image is Dockerfile.r; it performs the same R/rpy2/renv preflight as the Fly R worker before starting Celery.

Environment variables

Postgres schemas / roles

See sql/roles.sql:

• theorem_control owns schema control
• theorem_spine owns schema spine, with column-limited SELECT on D3 read models

Django sets search_path=control,public. Settings force DISABLE_SERVER_SIDE_CURSORS=True and CONN_MAX_AGE=0.

D3 tables Rust may SELECT

HTTP surface

• POST /webhooks/workos — WorkOS events (signature required)
• POST /internal/offload/invoke — enqueue a tenant-bound Celery task
• POST /internal/offload/artifact-upload — mint a tenant-scoped, short-lived Arrow upload URL
• GET /internal/offload/{job_id} — return the caller tenant's job status + ArrowBatch descriptor
• POST /internal/offload/{job_id}/cancel — cancel the caller tenant's job
• POST /internal/extraction/submit — plan and fan out a tenant corpus extraction
• GET /internal/extraction/{job_id} — return extraction and per-shard Arrow descriptors
• POST /internal/extraction/{job_id}/cancel — cancel every non-terminal shard
• POST /internal/extraction/review — append candidate review decisions
• GET /internal/extraction/review?since=<iso> — stream decisions for non-spine callers
• POST /internal/rl/eval — enqueue a tenant-owned verifiers evaluation
• POST /internal/rl/train — launch a digest-pinned Prime-RL RunPod Pod
• GET /internal/rl/runs/{run_id} — verify and return run artifacts
• POST /internal/rl/runs/{run_id}/cancel — cancel a run and terminate its Pod
• POST /internal/competence/fit — submit a tenant/project-bound competence fit
• POST /internal/competence/refit — submit a refit bound to a previous scorer
• GET /internal/competence/jobs/{job_id} — inspect fit/refit state and artifacts
• POST /internal/competence/jobs/{job_id}/cleanup — remove exact owned artifacts
• POST /internal/layout/compute — return deterministic Graphviz center positions
• POST /internal/rendering/plantuml — render SANDBOX PlantUML to tenant-owned SVG
• POST /internal/rendering/diagrams — render restricted Diagrams source to tenant-owned PNG/SVG
• POST /internal/rendering/descriptor — refresh a short-lived descriptor for one exact tenant-owned render key
• /admin/ — ops console (revoke key, re-run job, reset usage, impersonate grant)
• GET /healthz

Offload machine-key admission

Every /internal/offload/* request requires Authorization: Bearer thk_.... Keys are minted in the Django admin and belong to exactly one tenant; callers never submit a tenant_id. Grant only the scopes required by the caller:

offload:* grants all three offload scopes. Revoked, expired, inactive-tenant, or unknown keys are refused; job lookups are filtered to the admitted tenant.

Reinforcement-learning machine-key admission

RL routes use rl:eval, rl:train, rl:read, and rl:cancel; rl:* grants all four. Tenant identity comes only from the verified machine key. A nested tenant or tenant_id is treated as an equality assertion and refused if it does not match.

Run submission is idempotent by tenant and operation_id; reusing an operation ID with a changed taskset, config digest, image digest, or operation fails closed. Training accepts only an OCI image reference with a full SHA-256 digest. The worker gives the Pod tenant/run-scoped presigned upload capabilities, ingests the resulting traces into Arrow, verifies digest, schema, and row count on readback, and only then mints Trajectory and GraderVerdict rows. Status reads repeat artifact verification before issuing download URLs.

The committed tests use a byte-preserving storage double and mocked RunPod REST transport. They prove control-flow and integrity behavior but do not substitute for a live Pod, hosted object storage, or a real Prime-RL reward curve.

Extraction machine-key admission

Extraction routes use extraction:submit, extraction:read, and extraction:review; extraction:* grants all three. Tenant identity always comes from the verified machine key. Any nested tenant or tenant_id in a request is treated only as an equality assertion and is refused on mismatch.

The parent ledger stores job and shard state, while candidate rows remain in verified Arrow artifacts. Review decisions are append-only Postgres rows; a newer decision for the same candidate digest supersedes an older decision. Rust reads those rows through the column-limited theorem_spine role and owns graph admission.

The committed extraction fixture is a deterministic stub replay and is not a live GPU receipt. After deploying the dedicated extraction endpoint, run the hosted boundary oracle with a disposable machine key carrying offload:invoke, extraction:submit, and extraction:read:

THEOREM_EXTRACTION_LIVE_MACHINE_KEY=thk_... \
python manage.py extraction_live_smoke \
  --base-url https://travis-django-theorem-personal.fly.dev \
  --timeout-seconds 900

Exit zero means the fixture input was uploaded through a presigned capability, the deployed extraction job succeeded, and every returned shard was downloaded and independently verified for digest, Arrow schema, and row count. It does not imply that the still-uncommitted Rust companion contract is byte-identical.

Competence machine-key admission

The competence routes use competence:fit, competence:read, and competence:cleanup; competence:* grants all three. Each request carries the tenant UUID as part of its content-addressed scope, but that value never selects authority: it must equal the tenant derived from the verified machine key.

theorem.competence.v1 carries lineage-de-duplicated sufficient evidence and content-addressed scorer/prior references, not raw graph state or authority. Exact operation retries reuse one job. Reusing the key with a changed payload fails closed. Cleanup is restricted to the artifacts persisted for the exact tenant, project, candidate, and job.

The worker uses training survival to establish a Beta prior and W02-corrected held-out outcomes for the posterior. Fit/refit output is immutable: exact retry reuses the job, refit binds the prior scorer and rejects reused lineage, and a status cannot become succeeded until both artifacts pass readback.

The fixture at contracts/theorem.competence.v1.fixture.json is explicitly a deterministic wire fixture. The W14 known-truth suite exercises the real fitter with a byte-preserving local storage double; neither proves hosted object storage or deployment behavior.

The complete wire, worker/Beat, evidence-class, and cleanup contract is in docs/competence-exchange-v1.md. Run the hosted boundary oracle inside the Fly web machine so credentials remain private:

python manage.py competence_live_smoke \
  --base-url https://travis-django-theorem-personal.fly.dev \
  --timeout-seconds 120 \
  --confirm-live-cleanup

This proves the public deployed boundary and real artifact readback/cleanup. Its disposable scorer evidence remains a deterministic fixture and is not promotion evidence.

Graph layout and rendering

/internal/layout/compute requires layout:compute (or layout:*). Callers send stable node/edge IDs and measured pixel sizes; Django selects a policy row, serializes sorted DOT, executes PyGraphviz in a deadline-bound subprocess, and returns center coordinates with the exact Graphviz version, effective policy, and an input digest. Canonical response bytes are cached under a tenant-scoped Valkey key. The service never mutates graph content.

All three /internal/rendering/* routes require rendering:render (or rendering:*). The descriptor route derives the tenant from that admitted key, verifies the exact content-addressed object and digest, and presigns a fresh GET; it does not accept a payload tenant or mint a URL before storage readback. PlantUML is forced to SVG under its SANDBOX security profile. Diagrams source is statically refused if any import names a package outside diagrams; the isolated interpreter repeats that import check at runtime. This is capability admission plus resource hygiene, not a Python security sandbox. Both renderers run synchronously in temporary working directories and isolated process groups with a credential-free child environment, deadlines, and pre-buffer file-size caps; the Linux deployment additionally applies CPU and address-space rlimits. Same-container execution is still not an isolation boundary for adversarial Python; deployments admitting untrusted Diagrams source must move that worker to a credential-free sandbox or sidecar.

Rendered bytes are read back after upload and published as tenants/<tenant-id>/renders/<sha256>.<ext> with a short-lived presigned GET. The Docker image binds APT to snapshot 20260801T000000Z, pins Debian Graphviz 2.42.2-7+deb12u1 (which reports linked runtime 2.43.0), compiles PyGraphviz 2.0.1 against that library, installs Diagrams 0.25.1 and OpenJDK 17, and checksum-verifies the PlantUML 1.2026.6 jar. contracts/theorem.layout.v1.fixture.json is a strict wire fixture; its named coordinates are not a substitute for the native container or hosted/authenticated oracles.

Evidence is intentionally split by boundary:

Replay the native rendering boundary without installing host packages:

TMPDIR=/tmp .venv/bin/python scripts/run-rendering-native-oracles.py

Exit 0 is the only passing native-renderer receipt. Exit 1 means an identity, checksum, render, refusal, bound, or cleanup oracle failed; it is not a prerequisite skip.

The helper downloads PlantUML 1.2026.6 and the official Graphviz 14.1.5 release into a bounded temporary directory, verifies both reviewed SHA-256 values, builds Graphviz under that temporary prefix, and calls the production PlantUML and isolated Diagrams functions. It requires real SVG and PNG bytes, digest-derived tenant render keys, SANDBOX local-include refusal, a refusal that names a forbidden Diagrams import, and complete temporary-state cleanup. This is native renderer evidence only: Graphviz 14.1.5 does not substitute for the declared image's Debian Graphviz 2.42.2-7+deb12u1 package and linked runtime 2.43.0.

Run the declared-image preflight and gate with:

.venv/bin/python scripts/run-rendering-container-oracles.py

The command inventories Docker, Podman, Colima/Lima, Finch, nerdctl, Apple container, and OrbStack without starting or installing a service. With an already-usable image client and at least 20 GiB free, it builds Dockerfile, checks exact Graphviz, PyGraphviz, Diagrams, Java, and PlantUML identities, runs both production renderers, manage.py check, and the cold layout fixture, then removes its helper-owned image tag. Missing runtime or disk capacity exits with prerequisite status 2; host Graphviz is never credited as declared-image evidence. Hosted/authenticated proof remains the separate live test below. Exit 0 alone proves the declared image. Exit 2 means a named host prerequisite is absent and keeps the gate open. Exit 1 means the declared recipe or an executed image probe violated its oracle.

Run the deployed smoke with a machine key carrying both layout:compute and rendering:render. The test downloads each signed artifact and verifies its digest; keep the key in the environment, never in the repository:

THEOREM_LAYOUT_RENDERING_LIVE_BASE_URL=https://control.example \
THEOREM_LAYOUT_RENDERING_LIVE_MACHINE_KEY=thk_... \
.venv/bin/pytest -q -m live tests/test_layout_rendering_live.py

fly.layout-test.toml is the production-isolated hosted layout oracle used by TheoremWeb staging. It deploys the same image with one web process, a dedicated SQLite volume, and no production Postgres, Valkey, RunPod, or object-storage credentials. Machine keys are minted inside that app for the staging tenant and are stored only in the consuming Fly app's secrets.

The exact 31-node/44-edge Agent Chat board is committed as contracts/theorem.layout.v1.agent-chat-plan.fixture.json and is the default deployed board input. THEOREM_CHAT_PLAN_LAYOUT_FIXTURE may override that path for an explicitly versioned successor. Set THEOREM_LAYOUT_LIVE_VALKEY_URL to run the separate deployed Valkey cache oracle. Neither gate accepts the two-node wire fixture as a substitute.

To run every hosted row in one invocation, provide all three variables:

THEOREM_LAYOUT_RENDERING_LIVE_BASE_URL=https://control.example \
THEOREM_LAYOUT_RENDERING_LIVE_MACHINE_KEY=thk_... \
THEOREM_LAYOUT_LIVE_VALKEY_URL=redis://hosted-valkey.example:6379/0 \
.venv/bin/pytest -q -m live tests/test_layout_rendering_live.py

Pytest exit 0 is credit only for rows that actually executed. A zero exit with skipped rows is not a hosted receipt; inspect the summary and require zero skips for the intended set.

Run the complete bounded local replay with:

.venv/bin/python scripts/run-layout-local-oracles.py

Exit 0 means the helper-owned receipt contained exactly four expected tests, four passes, and zero skips/failures/errors, followed by bounded process/port/ temporary-state cleanup. Exit 1 means a prerequisite or oracle failed. Exit 130 means interruption completed its cleanup; neither nonzero status is a pass.

Before downloading MinIO, the replay resolves THEOREM_TEST_VALKEY_SERVER or valkey-server on PATH, requires its real path to be executable, and verifies the Valkey server v=<version> identity. The exact resolved binary is then started on a dynamically selected loopback port with a temporary data directory; a missing or invalid Valkey installation is fatal rather than a pytest skip. The helper downloads the immutable official Darwin/ARM64 MinIO archive minio.RELEASE.2025-09-07T16-13-09Z into a separate temporary directory and checks the reviewed SHA-256 before making it executable. MinIO receives fresh credentials, data, config, API port, and console port for that invocation. The helper proves the binary and S3 server identity, then invokes exactly the four required local-oracle test node IDs in a separate allowlisted environment. Inherited pytest controls, plugins, credentials, hosted endpoints, MinIO controls, and proxy settings are not passed to either child; loopback NO_PROXY is explicit. A helper-owned JUnit receipt must identify all four tests with four passes, zero skips, zero failures, and zero errors before the success line is emitted. Finally, the helper requires the processes, ports, and temporary state to be gone. It accepts no endpoint argument, so moto or an operator-selected loopback service cannot receive real-process credit.

The direct pytest module remains useful when an operator already owns a local S3-compatible process:

.venv/bin/pytest -q tests/test_layout_local_oracles.py

Its artifact-store case requires all THEOREM_LAYOUT_LOCAL_S3_* variables and refuses non-loopback endpoints. That operator-hosted path is separate from the pinned disposable-MinIO replay above.

Reproduce the Agent Chat fixture from the immutable Theorem Plan object with:

.venv/bin/python scripts/check-agent-chat-layout-fixture.py \
  --theorem-repo '/path/to/Theorem'

The checker reads generation 15 with git show at commit f125a04118fce2e7a971b89d663d24a4cf2caa43, assigns edge IDs in source task/dependency order, classifies an edge as verifies only when the source names the target as its verification sibling, applies the documented W/V/plan node sizes, and then sorts nodes and edges for the wire fixture. The source-topology receipt is SHA-256 over UTF-8 JSON containing sorted node IDs and sorted {from,to} pairs, encoded with sorted object keys and separators , and :. The request receipt uses the same canonical JSON encoding over the complete generated layout_request.

RunPod and R execution contract

The default Python worker submits an asynchronous job to POST /v2/{endpoint}/run, persists the returned RunPod job id in control_job, polls GET /v2/{endpoint}/status/{job_id}, and cancels the remote job on the control-plane deadline or user cancellation. The endpoint must return:

{
  "schema_json": "<Arrow schema JSON>",
  "rows": 42,
  "payload_digest": "sha256:<content-addressed-output>"
}

inside its final output object. The descriptor—not Arrow bytes—crosses the control-plane request. Each live input descriptor must name an artifact_key under tenants/<tenant-id>/; the worker receives only a short-lived presigned GET for that input and PUT for the server-selected output key. Django downloads the output itself and verifies the reported digest, schema, and row count before marking the job successful. The status response mints a fresh tenant-authorized download_url; no S3 credential is returned to a caller or RunPod.

Implemented operations:

The remaining TabFM, GNN, mixed-model, and survival operations return explicit errors until their operation-specific runners are implemented. They never manufacture an output descriptor from a digest.

Tests

source .venv/bin/activate
pip install pytest pytest-django
CELERY_TASK_ALWAYS_EAGER=1 pytest -q
# or
CELERY_TASK_ALWAYS_EAGER=1 python manage.py test tests

tests/test_schema_roles.py skips unless DATABASE_URL points at Postgres. When roles from sql/roles.sql are applied, it also asserts GRANT/REVOKE live permission errors (A1).

A3 — control schema contract (CI)

After migrate and applying sql/roles.sql on a scratch Postgres, from a pinned Theorem checkout run:

export CONTROL_DATABASE_URL='postgres://theorem_spine:...@localhost:5432/theorem'
cargo test -p rustyred-thg-catalog --lib control_schema_contract_holds -- --ignored

Wire this into CI on every Django migration change so column drift fails the contract before Rust read-model clients break.

Spec

Implements the Django half of SPEC-THEOREM-CONTROL-PLANE-1.0 (Theorem docs/plans/control-plane/).