research-capacitor 0.1.0

Decentralized inference network CLI for automated mathematical research via Lean code generation

Research Capacitor

Research Capacitor is a standalone Python CLI for a decentralized inference network focused on mathematical research and Lean 4 code generation. Nodes connect directly to Supabase for coordination and ledger state, while local inference runs through llama.cpp.

The project now also includes a backend-owned research loop:

• research_jobs track high-level requester goals and budgets
• research_episodes track individual conjecture-search campaigns under a job
• proof_attempts track every queued attempt, repair, and verifier result
• the FastAPI backend can run an internal worker that keeps the provider queue full and schedules repairs
• rc research-run now seeds a backend-managed research job
• rc research-status shows backend-managed job, episode, and attempt progress

The goal is simple:

• requesters reserve Compute Credits to submit proof-generation work
• providers earn Compute Credits by running local inference
• the ledger records reserves, transfers, and releases explicitly

System Overview

Research Capacitor has two node roles:

• requester: submits proof-generation tasks
• provider: polls the network, claims tasks, runs inference, and settles results
• both: does both on a single machine

There is no separate coordinator service in the current architecture. Supabase is used for:

• node registration and heartbeats
• task queueing
• result storage
• credit balance tracking
• ledger entries
• secure RPC-based state transitions

Local inference is done entirely on the node. During rc init, provider-capable nodes detect available hardware, pick the largest supported model that fits, and can download it automatically.

How The Network Works

The end-to-end flow is:

1. A node runs rc init and registers itself in Supabase.
2. A requester runs rc submit "..." --budget N.
3. The network moves the full task budget from available balance into reserved balance.
4. A provider running rc serve claims the task and runs local inference through llama.cpp.
5. When the task completes, the network stores the result plus runtime accounting data.
6. On completion, the network transfers the billed amount to the provider.
7. Any unused reservation is released back to the requester's available balance.
8. If a task fails, it is requeued until retry budget is exhausted. On final failure, the full reservation is released.

Task claiming is exclusive per queued task. A single research job can fan out into many queued attempts, but each tasks.id is claimed atomically by at most one provider at a time.

For autonomous research jobs, the backend repeats that flow multiple times:

1. requester submits a high-level research job and budget
2. backend creates a conjecture-search episode
3. backend enqueues one or more provider attempts across active episodes
4. provider generates Lean output
5. backend verifies the generated Lean
6. if verification fails, backend feeds diagnostics into a repair prompt
7. backend enqueues the next repair attempt when needed
8. repeat until the theorem is verified or the job exhausts its budget

Credit And Settlement Model

The network uses 1 credit = 1 TFLOP. Internally, the ledger stores integer microcredits, where 1 microcredit = 1 MFLOP = 0.000001 TFLOP.

Submission

When a requester submits a task:

• the full budget moves from balance to reserved_balance
• the reservation is recorded in transactions

Completion

When a provider completes a task:

• the runtime records actual prompt tokens, generated tokens, loaded model parameter count, and eval timings
• the system computes actual model-work MFLOPs from the exact loaded GGUF and actual processed tokens
• the system treats those MFLOPs as the exact integer credit subunits used for settlement
• the provider receives a transfer of min(actual_credit_subunits, task_budget_subunits)
• any unused reservation is released back to the requester

This means:

• requester reserve = full submitted budget
• provider transfer = billed compute
• requester release = unused reserved budget

So for a successful task:

reserve = transfer + release

Failure / Retry

Each task has retry state:

• attempt_count
• max_attempts
• lease timestamps and error metadata

Failure behavior:

• non-final failure: task returns to pending
• final failure: task moves to failed and the requester receives a full release of the held budget
• stale claimed/running tasks are automatically requeued when leases expire

What "Actual Compute" Means

Research Capacitor now uses:

• the exact loaded GGUF model parameter count from llama.cpp
• the actual prompt token count
• the actual generated token count

It does not use the old static catalog estimate anymore.

The raw MFLOP telemetry is model-work accounting:

2 * model_params * (prompt_tokens + generated_tokens) / 1e6

Credits are then settled in exact TFLOP subunits:

billable_credit_subunits = actual_mflops
billable_tflops = billable_credit_subunits / 1_000_000

This is accurate for billing the actual loaded model and actual processed tokens. It is not a hardware performance-counter reading of every fused CPU, Metal, or CUDA kernel, because llama.cpp does not expose a portable per-kernel FLOP counter through the Python API.

Installation

git clone https://github.com/t0mCS/Compute-Capacitor.git
cd Compute-Capacitor
./scripts/install_rc.sh

That installer creates an isolated virtualenv under ~/.local/share/research-capacitor, symlinks rc into ~/.local/bin, and works without requiring npm or a pre-existing project venv.

If you prefer pipx, install directly from the repo:

pipx install git+https://github.com/t0mCS/Compute-Capacitor.git

For local development, keep using an editable install:

python3 -m venv .venv
source .venv/bin/activate
pip install -e .

Supabase Setup

1. Create a Supabase project.
2. Open the SQL Editor.
3. Run supabase/schema.sql.
4. Run supabase/hardening.sql.
5. Run supabase/reservation_runtime.sql.

schema.sql creates the base tables and types. hardening.sql enables the secure RPC-based operating mode:

• revokes direct table access from client roles
• enables RLS
• exposes narrow SECURITY DEFINER RPCs for registration, reads, and public status access

Production note: backend-owned orchestration RPCs and store_verified_lemma should be called with the Supabase service-role key, not a publishable client key.

reservation_runtime.sql installs the canonical reservation-mode runtime RPCs:

• reserves credits when a task is submitted
• transfers billed credits to the provider on completion
• releases unused or failed reservations back to the requester
• requeues or fails expired leased tasks safely

If you already applied an older version of the project schema, rerun all three files in order so the base schema, hardening layer, and reservation runtime are brought back into sync.

If you want to wipe runtime state without dropping the schema, run supabase/clear_runtime.sql before reapplying the SQL files or starting a fresh soak.

After clearing runtime state, re-register the requester and any providers you plan to use, then fund the requester or mark it as unlimited_budget = true before starting a soak.

Quick Start

1. Initialize A Node

rc init \
  --name "my-node" \
  --role both \
  --supabase-url "https://YOUR_PROJECT.supabase.co" \
  --supabase-key "YOUR_PUBLISHABLE_KEY"

Or with environment variables:

export SUPABASE_URL="https://YOUR_PROJECT.supabase.co"
export SUPABASE_KEY="YOUR_PUBLISHABLE_KEY"
rc init --name "my-node" --role both

What rc init does:

• generates a local node ID
• writes ~/.rc/config.toml
• detects hardware
• selects a model automatically for provider-capable nodes
• optionally downloads the model
• registers the node in Supabase
• creates the node and balance rows, but does not automatically mint test credits

After a fresh reset, fund the requester before submitting work. Two simple SQL-editor options are:

UPDATE nodes
SET unlimited_budget = true
WHERE id = 'YOUR_REQUESTER_NODE_ID';

INSERT INTO credit_balances (node_id, balance, reserved_balance, updated_at)
VALUES ('YOUR_REQUESTER_NODE_ID', 100, 0, now())
ON CONFLICT (node_id)
DO UPDATE SET balance = EXCLUDED.balance,
              reserved_balance = EXCLUDED.reserved_balance,
              updated_at = now();

2. Run As A Provider

rc serve --poll-interval 2 --max-tokens 256 --temperature 0.2

3. Submit A Task

rc submit "Prove in Lean that for every natural number n, n = n." --budget 1.25

You can also submit richer queued work:

rc submit "Repair this failed proof..." --task-type proof_repair --metadata-json '{"domain":"naturals"}'

4. Check Status

rc status TASK_ID
rc research-status

5. Check Balance And Ledger

rc balance
rc ledger --limit 20

6. Run Backend-Owned Research

Start the backend worker:

export SUPABASE_URL="https://YOUR_PROJECT.supabase.co"
export SUPABASE_KEY="YOUR_PUBLISHABLE_KEY"
export RESEARCH_BACKEND_ENABLED=1
uvicorn backend.main:app --reload

Then submit a high-level research job:

rc research-run \
  --domain naturals \
  --total-budget 25 \
  --budget-per-attempt 1 \
  --max-concurrent-episodes 3

The CLI now defaults backend-managed research commands to the deployed Azure backend. To point a node at a different backend, pass --backend-url or set RC_BACKEND_URL.

CLI Commands

All commands are exposed through rc.

rc init

Initialize a node and register it with the network.

Example:

rc init \
  --name "provider-1" \
  --role provider \
  --supabase-url "https://YOUR_PROJECT.supabase.co" \
  --supabase-key "YOUR_PUBLISHABLE_KEY"

Useful options:

• --name, -n: display name
• --role, -r: provider, requester, or both
• --supabase-url: Supabase project URL
• --supabase-key: Supabase publishable key
• --backend-url: backend base URL for research orchestration; defaults to the deployed Azure app or RC_BACKEND_URL
• --model, -m: override auto-selected model
• --skip-model-download: register without downloading the model yet

rc serve

Run a provider loop.

What it does:

• sends secure heartbeats
• polls for pending tasks
• claims one task atomically
• marks it running
• renews task leases and node heartbeats while inference is still running
• runs local inference
• settles completion or failure through secure RPCs

Important:

• many providers can work on the same research job at once
• they do that by claiming different queued attempts under that job
• two providers should not claim the same task because claim_task uses FOR UPDATE SKIP LOCKED

Example:

rc serve \
  --poll-interval 2 \
  --max-tokens 256 \
  --temperature 0.2 \
  --threads 2 \
  --lease-seconds 300 \
  --keepalive-interval 30

Useful options:

• --model, -m: override configured model
• --poll-interval, -p: seconds between queue polls
• --max-tokens: completion cap
• --temperature, -t: sampling temperature
• --threads: inference threads per provider; defaults to splitting local CPU capacity across concurrent local providers
• --ctx-size: llama.cpp context window
• --gpu-layers: override GPU offload layer count
• --lease-seconds: task lease duration; renewed while inference runs
• --keepalive-interval: interval between in-task heartbeats and lease renewal attempts

rc submit

Submit a Lean-proof-generation task.

Example:

rc submit "Show in Lean that True implies True." --budget 500

Useful options:

• positional prompt: the problem statement
• --model, -m: override model label stored with the task
• --budget, -b: maximum TFLOP credits to reserve for the task; fractional values such as 0.25 or 1.5 are allowed
• --task-type: classify the queued work, for example lean_proof_gen, proof_attempt, proof_repair, or counterexample_search
• --metadata-json: attach structured JSON metadata that providers can use to shape the prompt

rc research-run

Submit a backend-managed research job.

What it does:

• sends one high-level research goal to the backend
• lets the backend worker create conjecture-search episodes
• lets the backend fill the provider queue with proof or repair prompts
• returns the created research job id so you can inspect progress

Example:

rc research-run \
  --total-budget 25 \
  --max-concurrent-episodes 3 \
  --budget-per-attempt 1 \
  --max-attempts-per-episode 4

rc research-status

Inspect backend-managed research jobs, episodes, and proof-attempt history.

Examples:

rc research-status
rc research-status JOB_ID

rc status

Inspect a task.

Example:

rc status c4a239c7-4adc-4d0e-82ac-3263aad880a0

What it shows:

• task status
• model
• budget
• retry count
• generated Lean output
• actual compute in TFLOPs
• billed credits
• prompt and generated token counts
• eval time
• last error for failed/requeued work

rc balance

Show the current credit balance for the local node.

Example:

rc balance

rc ledger

Show recent credit movements for the local node.

Example:

rc ledger --limit 20

Ledger entry types:

• reserve: requester moved budget from available to reserved
• transfer: reserved credits settled to the provider
• release: reserved credits returned to the requester
• historical projects may still contain older burn, mint, and refund rows from before the reservation migration

rc rotate-secret

Rotate the local node bearer secret through the secure RPC layer.

Example:

rc rotate-secret

What it does:

• generates a fresh local node secret
• asks Supabase to replace the old secret hash atomically
• writes the new secret into ~/.rc/config.toml only after the server confirms the change

Local Configuration

The CLI stores its local config at:

~/.rc/config.toml

It contains:

• node identity
• node secret used for authenticated RPC calls
• selected role
• Supabase URL and key
• chosen model
• downloaded model path
• hardware summary

Database Shape

The Supabase schema uses five main tables:

• nodes
• credit_balances
• tasks
• task_results
• transactions

Important task fields include:

• status
• research_episode_id
• attempt_index
• parent_attempt_id
• task_metadata
• credit_budget
• attempt_count
• max_attempts
• lease_expires_at
• claimed_at
• started_at
• completed_at
• failed_at
• last_error

Important task result fields include:

• mflops_used
• billed_mflops
• prompt_tokens
• generated_tokens
• model_params
• prefill_eval_ms
• decode_eval_ms
• total_eval_ms

mflops_used remains the raw telemetry field. billed_mflops is the legacy result column name used for exact settled credit subunits, where 1 billed_mflops = 0.000001 TFLOP credit.

Research-specific tables:

• research_jobs
• research_episodes
• proof_attempts

Security Model

The current secure mode is:

• no direct client reads or writes to sensitive tables
• RPC-only state transitions
• atomic settlement in Postgres functions
• node-secret authenticated task and balance RPCs
• RLS enabled across the main tables

What this protects against:

• direct balance editing with the publishable key
• direct task insertion or task mutation from the client
• non-atomic ledger settlement

Current limitation:

• node identity is authenticated with a locally stored bearer secret, not a public-key signature scheme
• a stolen local config would still let an attacker act as that node until the secret is rotated

So the system is much safer than the initial version, but it is not yet a fully trustless identity model. A future version should rotate secrets cleanly or move to signed task-claim messages.

Web Dashboard

The repo now includes a read-only network dashboard in web/.

What it shows:

• healthy, online, and stale node counts
• pending / assigned / running / completed / failed task totals
• 24-hour throughput, success rate, reserves, transfers, releases, and legacy burn/mint/refund totals when present
• recent tasks, recent ledger activity, active nodes, and model mix

The dashboard reads through public, sanitized RPCs defined in supabase/hardening.sql:

• get_public_network_summary()
• get_public_recent_tasks(p_limit integer)
• get_public_recent_activity(p_limit integer)
• get_public_nodes(p_limit integer)

Dashboard Setup

1. Reapply supabase/hardening.sql in Supabase so the public dashboard RPCs exist.
2. Create web/.env.local with:

VITE_SUPABASE_URL="https://YOUR_PROJECT.supabase.co"
VITE_SUPABASE_ANON_KEY="YOUR_PUBLISHABLE_KEY"

3. Start the dashboard:

cd web
npm install
npm run dev

4. Build for production:

cd web
npm run build

If the environment variables are missing, the dashboard falls back to demo data so the UI can still be previewed locally.

Typical Workflows

Provider

rc init --name "provider-1" --role provider --supabase-url "$SUPABASE_URL" --supabase-key "$SUPABASE_KEY"
rc serve --poll-interval 2 --max-tokens 256 --temperature 0.2

Requester

rc init --name "requester-1" --role requester --supabase-url "$SUPABASE_URL" --supabase-key "$SUPABASE_KEY"
rc submit "Prove in Lean that if P is true then P is true." --budget 500
rc status TASK_ID
rc balance
rc ledger

Single Machine Demo

rc init --name "demo-node" --role both --supabase-url "$SUPABASE_URL" --supabase-key "$SUPABASE_KEY"
rc serve --threads 1 --max-tokens 128
# in another shell
rc submit "Prove in Lean that 1 = 1." --budget 100

Integration Testing

The repo includes an opt-in live integration harness for:

• claim -> run -> renew -> complete
• lease expiry -> requeue -> reclaim
• node secret rotation
• autonomous episode-style soak submission when scripts/overnight_soak.py --research-mode is used

Run it against a real Supabase project with a funded requester config:

RC_RUN_INTEGRATION_TESTS=1 \
RC_INTEGRATION_REQUESTER_CONFIG="$HOME/.rc/config.toml" \
python -m unittest tests.test_runtime_integration -v

For a short live soak after a reset:

python scripts/overnight_soak.py \
  --requester-config "$HOME/.rc/config.toml" \
  --provider-count 2 \
  --duration-hours 0.05 \
  --queue-depth 2 \
  --task-budget 1 \
  --submit-interval 10 \
  --monitor-interval 10 \
  --threads 1 \
  --max-tokens 32

Notes:

• the integration suite expects an empty queue before it starts
• it uses real RPCs and real credit settlement, so run it against a disposable or controlled project
• if rotate_node_secret was added recently, reapply supabase/hardening.sql before running the rotation test

Development Notes

• Inference uses llama-cpp-python.
• Model selection prefers the largest supported model that fits detected memory.
• The CLI is designed to run on CPU, Apple Silicon, and CUDA-capable hosts supported by llama.cpp.
• Existing projects should reapply supabase/hardening.sql and supabase/reservation_runtime.sql whenever RPC signatures or settlement columns change.
• Provider liveness now stays fresh during long inference runs via in-task heartbeats and lease renewal.
• On a single machine running many local providers, set --threads conservatively to avoid CPU oversubscription and throughput collapse.