Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
175 changes: 167 additions & 8 deletions services/api/NOTES.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# AxiomCode production build — W1 + W2
# AxiomCode production build — W1 + W2, then W3 + W4 (code) + W5

Local working copy built from `api-prototype/` (state/secret files —
keys.txt, meter.jsonl, revoked.txt — deliberately excluded). Nothing
Expand Down Expand Up @@ -55,7 +55,6 @@ pushed anywhere; this tree is for review/checkpoint.
system temp) and removed in a `finally` block in both servers.

## Tests — 14 passed, 0 failed (`~/ax-venv/bin/python -m pytest tests/ -q`)

- test_ca.py (6): key persistence + 0600 perms; issue→verify
round-trip (v2 fields, 90-day window); tampered verdict and mangled
signature fail; wrong key fails (bad_signature); published payload
Expand All @@ -76,19 +75,179 @@ pushed anywhere; this tree is for review/checkpoint.
CA/store wiring, not Lean. Real-Lean behaviour was proven by the
prototype demo (2026-09-26) and the engine suite.

## Left stubbed / out of scope (later workstreams)
## Left stubbed / out of scope after W1/W2 (status updated by W3–W5 below)

- Revocation is operator-side only (store.revoke) — no public revoke
endpoint, same as the prototype; an authenticated admin path is
still to be designed.
- API-key enforcement on REST (prototype had none; MCP bearer auth
unchanged, including its known mutable-identity issue — W3 scope).
- Trial limits (10 cases), certificate withholding until payment,
Stripe entitlement/webhooks, quotas, rate limits, idempotency —
not in W1/W2 scope.
- ~~API-key enforcement on REST~~ — done in W3 (below).
- ~~Trial limits (10 cases), certificate withholding until payment,
Stripe entitlement/webhooks, quotas, rate limits~~ — done in
W3/W4/W5 (below). Idempotency: webhook grants are idempotent on
Stripe ids; request-level idempotency keys are still open.
- restart_rest.sh / restart_mcp.sh were not copied from the prototype
(they point at prototype paths/ports).
- Ruff: clean except deliberate fail-closed broad `except` catches
(BLE001 in ca/certs/billing legacy path, S112 in the legacy JSONL
reader) and import-order notes where sys.path setup must precede
imports — all inherited patterns, left as-is intentionally.

## W3 — Access control + trial enforcement

- **API keys** (`store.py`): `Store.create_api_key(label)` returns a
plaintext `axk_<token_urlsafe(32)>` exactly once; the store keeps
ONLY its SHA-256 hash (`api_keys`: key_hash PK, label, created_at,
revoked) plus an audit event carrying hash + label. Operator CLI:
`python -m store create-key --label "Acme"` (prints the key once).
`revoke_api_key(key_hash)` revokes by hash. Nothing anywhere logs
or persists a plaintext key.
- **Identity = key hash.** Everywhere a caller identity is recorded
(meter_events.key_id, certificate key_id, limits, grants) it is the
key's SHA-256 hash — stable and joinable, not a secret. Request
bodies carry no identity at all.
- **REST**: `/verify` and `/check` require a key (`X-Api-Key` header
or `Authorization: Bearer`); missing / unknown / revoked → 401.
The old `rest-anonymous` metering identity is gone. `/check` is a
read: it consumes no trial case and no credits. Open endpoints:
`/health`, `/.well-known/axiomcode-keys.json`, and `/revoked`
(the public CRL — publishing it is the point, same as X.509).
- **MCP**: bearer auth now validates against the store, replacing
keys.txt / `billing.load_keys` (the mutable-identity hole is
closed: `_KEY` binds the authenticated key's hash per request, and
no tool takes an identity parameter, so callers cannot meter or
spend as another key). The server process's own key comes from
`AXIOMCODE_API_KEY` and is provisioned at startup if unknown
(`ensure_api_key`, label `AXIOMCODE_API_KEY_LABEL`, default
"mcp-server"); a store revocation is never undone by a restart.
- **Trial** (shared flow, `verify_service.execute_verification` —
both servers run the same code so the interfaces cannot drift):
balance = sum(credit_grants) − metered credits used
(`store.balance_for`). Balance > 0 → paid case (proof, meter,
issue + record cert). Else, while trial cases used < 10 → free
trial case: proof runs, a zero-credit meter event flagged
`trial = 1` is recorded (that flag is how cases are counted), the
response is `{verified, attempts, certificate: None, usage,
trial: {cases_used, cases_left, certificates: "unlock with a
credit pack"}}` and NO certificate is recorded. Trial exhausted
and balance ≤ 0 → refused with 402 (REST) / a payment_required
error object (MCP) BEFORE the prover is invoked — no free compute.
Edge: a positive-but-tiny balance takes the paid path and may go
slightly negative on that call (metering is post-hoc by design).
- **Limits** (`limits.py`, per-process state): sliding-window rate
limit per key, default 60 req/min (`AXIOMCODE_RATE_LIMIT_PER_MIN`)
→ 429; per-key proof concurrency cap, default 2
(`AXIOMCODE_MAX_CONCURRENT_PROOFS`), non-blocking → 429 /
too_many_concurrent_proofs.
- **Store additions**: tables `api_keys`, `credit_grants`
(external_id UNIQUE → grant idempotency), `meter_events.trial`
column (added by an idempotent ALTER migration for W2 stores).
`grant_credits` returns False on a duplicate external_id instead
of raising, so webhook replays are naturally no-ops.
- **PR #21 hardening fixes**: (i) `ca.issue()` applies CA-fixed
fields (version, alg, kid, serial, issuer, validity window) AFTER
the subject spread — subjects can no longer override them, and a
subject-supplied "signature" is always replaced; (ii)
`verify_certificate` rejects a cert whose kid ≠ the verifying
key's kid (reason `unknown_kid`) after the signature check, so a
wrong key still reports `bad_signature` as before; (iii)
`record_cert` / `revoke` write the state row AND their audit event
in ONE transaction (rollback on error); (iv) **audit chain format
v2**: hash = SHA-256(prev_hash | event_type | ts | canonical
payload) — re-typing or re-dating a stored event now breaks the
chain too. The store is pre-production, so no migration of W2
chains is owed; a W2-created DB must not be mixed with v2 writers.

## W4 — Stripe billing (code layer only; no live calls anywhere)

- `stripe_billing.py`: pack catalogue starter 1,000cr/$10, growth
5,000cr/$50, scale 20,000cr/$200 (doctrine unchanged); price IDs
from `AXIOMCODE_STRIPE_PRICE_STARTER/_GROWTH/_SCALE`.
`build_checkout_payload(pack, key_hash)` is pure; the session
carries the key HASH as client_reference_id + metadata (never the
plaintext key). The API call sits behind `StripeClient`
(lazy SDK import) — tests inject a fake client.
- Webhook core `handle_webhook(store, payload, signature,
verify_signature)`: the route wires verify_signature to
`stripe.Webhook.construct_event`; tests pass a trivial callable.
`checkout.session.completed` → grant the pack's credits with
external_id = session id (replays grant nothing), plus a
zero-credit link row keyed by the session's payment_intent id
(source `stripe_pi_for:<session id>`) so refunds can find the
grant. `charge.refunded` → negative grant reversing the original
(external_id `<session>:refund:<charge id>`, replay-safe);
refunds for unknown payments return handled=False for deploy-time
monitoring to alert on.
- Route `POST /billing/webhook` in verify_api.py: without the
`stripe` package or `STRIPE_WEBHOOK_SECRET` it answers 501 with a
clear log line rather than accepting unverifiable events.
- **Still stubbed (deploy-time)**: creating the products/prices in
the live Stripe account, setting the price-id env vars,
`STRIPE_SECRET_KEY` / `STRIPE_WEBHOOK_SECRET`, and endpoint
registration in the Stripe dashboard. No network call exists in
any tested path.

## W5 — Job isolation

- Submission size cap: `AXIOMCODE_MAX_CODE_BYTES` (default 262144)
→ 413 / code_too_large, checked before proving on both interfaces.
- Proof timeout: `AXIOMCODE_PROOF_TIMEOUT_S` (default 600) enforced
in `verify_service.run_proof` around the prover call → 504 /
proof_timeout. Implemented with a worker thread (threads cannot be
killed): on timeout the response goes out, the temp project is
removed by the finally block, and the orphaned prover thread dies
against the removed directory. Hard-kill process isolation is a
possible future step if abuse shows up.
- Per-job temp projects stay unique (`mkdtemp` under
`AXIOMCODE_WORK_ROOT`) and are always removed; shared mutable
state between concurrent jobs is only the store (single
connection + lock, WAL) and the limiter/gate (internally locked).

## Env vars (new in W3–W5)

- `AXIOMCODE_TRIAL_CASES` (10), `AXIOMCODE_RATE_LIMIT_PER_MIN` (60),
`AXIOMCODE_MAX_CONCURRENT_PROOFS` (2), `AXIOMCODE_MAX_CODE_BYTES`
(262144), `AXIOMCODE_PROOF_TIMEOUT_S` (600)
- `AXIOMCODE_API_KEY`, `AXIOMCODE_API_KEY_LABEL` (MCP server key)
- `AXIOMCODE_STRIPE_PRICE_STARTER/_GROWTH/_SCALE`,
`AXIOMCODE_CHECKOUT_SUCCESS_URL`, `AXIOMCODE_CHECKOUT_CANCEL_URL`,
`STRIPE_SECRET_KEY`, `STRIPE_WEBHOOK_SECRET` (deploy-time)

## Tests — 40 passed, 0 failed (also clean under
## `-W error::DeprecationWarning`)

- test_access.py (9, new): 401 for missing/unknown key and for a
caller-supplied body identity; X-Api-Key and Bearer both work;
revoked key → 401; /health, keys payload, /revoked stay open;
/check consumes no trial case and no credits; full trial flow —
10 free cases with certificate=None and zero credits, no cert
recorded, 11th refused 402 with the prover never invoked, grant →
cert issued; rate limit 429; size cap 413; proof timeout 504 with
the temp dir cleaned up.
- test_billing_flow.py (10, new): balance = grants − metered
credits; trial meter events don't spend balance; grant idempotency
on external_id; only key hashes are stored; checkout payload shape
+ error cases; fake-client session creation; webhook grants pack
credits exactly once across replays; refund reverses exactly once;
unknown refund / unhandled event types; bad signature propagates;
webhook route answers 501 until Stripe is configured.
- test_hardening.py (7, new): subject cannot override issuer /
serial / kid / alg / version / validity in issue(); cert signed by
one key but naming another's kid is rejected (`unknown_kid`);
chain detects event_type tamper (broken_seq 1) and ts tamper
(broken_seq 2); concurrency gate unit behaviour; a second
concurrent proof for the same key is rejected while one runs;
MCP trial flow + tools expose no identity parameter.
- test_ca.py / test_store.py / test_wiring.py (14, updated):
wiring tests now authenticate (provisioned key + fixture grant)
and assert hash-keyed identity; all W1/W2 behaviour unchanged.
- Smoke (manual, not in suite): `python -m store create-key` issues
a key whose plaintext appears nowhere in the DB file; MCP server
with `AXIOMCODE_API_KEY` set provisions and authenticates it.
- Ruff: `ruff check` is clean for all service modules under the repo
config (verified in a repo-shaped tree — sibling-module import
order is first-party-sensitive, so it must be checked in-repo, not
from this directory). New files are `ruff format`-clean; store.py
and the older test files keep their W1/W2 formatting (ruff format
is not the repo gate for this subtree, and restyling them would
bury the functional diff). Pre-existing exceptions unchanged:
E741 in legacy certs.py, test-file import grouping as merged.
21 changes: 19 additions & 2 deletions services/api/billing.py
Original file line number Diff line number Diff line change
Expand Up @@ -81,9 +81,22 @@ def _is_store(target) -> bool:
return hasattr(target, "record_meter") and hasattr(target, "usage_for")


def meter(target, key_id: str, code_sha: str, verified: bool, compute_s: float, pricing: dict | None = None) -> dict:
def meter(
target,
key_id: str,
code_sha: str,
verified: bool,
compute_s: float,
pricing: dict | None = None,
trial: bool = False,
) -> dict:
"""Record one metered call. `target` is the durable Store
(production) or a legacy JSONL path. Returns the entry."""
(production) or a legacy JSONL path. Returns the entry.

Trial calls (W3) are FREE: the charge is computed as usual (the
rate fields stay on the entry for transparency) but credits/usd
are recorded as 0 and the entry is flagged trial — the store
counts those rows as the key's consumed trial cases."""
bill = charge_for(compute_s, pricing)
entry = {
"ts": int(time.time()),
Expand All @@ -92,6 +105,10 @@ def meter(target, key_id: str, code_sha: str, verified: bool, compute_s: float,
"verified": verified,
**bill,
}
if trial:
entry["credits"] = 0.0
entry["usd"] = 0.0
entry["trial"] = True
if _is_store(target):
entry_out: dict = target.record_meter(entry)
return entry_out
Expand Down
11 changes: 9 additions & 2 deletions services/api/ca.py
Original file line number Diff line number Diff line change
Expand Up @@ -117,17 +117,20 @@ def sign_body(self, body: dict) -> str:

def issue(self, subject: dict) -> dict:
"""Issue a v2 certificate. `subject` holds the verdict fields
(code_sha256, verified, attempts, toolchain, key_id, ...)."""
(code_sha256, verified, attempts, toolchain, key_id, ...).
The CA-fixed fields (version, alg, kid, serial, issuer,
validity window) are applied AFTER the subject spread, so a
subject can never override them (PR #21 review hardening)."""
now = int(time.time())
cert = {
**subject,
"version": 2,
"alg": ALG,
"kid": self.kid,
"serial": uuid.uuid4().hex[:16],
"issuer": ISSUER,
"valid_from": now,
"valid_until": now + VALIDITY_DAYS * 86400,
**subject,
}
cert["signature"] = self.sign_body(cert)
return cert
Expand Down Expand Up @@ -170,6 +173,10 @@ def verify_certificate(cert: dict, public_key=None, ca: CA | None = None) -> dic
pub.verify(base64.b64decode(sig_b64), canonical(body))
except Exception: # InvalidSignature, malformed base64, wrong key type
return {"valid": False, "reason": "bad_signature"}
if cert.get("kid") != kid_for(pub):
# The signature verifies under this key but the cert names a
# different one — not a cert this key stands behind.
return {"valid": False, "reason": "unknown_kid"}
now = int(time.time())
if now < cert.get("valid_from", 0):
return {"valid": False, "reason": "not_yet_valid"}
Expand Down
74 changes: 74 additions & 0 deletions services/api/limits.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
"""AxiomCode request limits (W3) — per-key rate limiting + proof
concurrency, in-process and dependency-free.

RateLimiter: sliding window per key (default 60 requests / 60 s,
AXIOMCODE_RATE_LIMIT_PER_MIN). ConcurrencyGate: at most N proofs in
flight per key (default 2, AXIOMCODE_MAX_CONCURRENT_PROOFS) — a Lean
build is the expensive unit, so concurrency is gated separately from
request rate.

State is per-process by design: each server process enforces its own
limits. (A multi-process deployment would move these to the store;
the single-host launch topology does not need it.)
"""

import os
import threading
import time
from collections import deque

RATE_LIMIT_PER_MIN = int(os.environ.get("AXIOMCODE_RATE_LIMIT_PER_MIN", "60"))
MAX_CONCURRENT_PROOFS = int(os.environ.get("AXIOMCODE_MAX_CONCURRENT_PROOFS", "2"))


class RateLimiter:
"""Sliding-window limiter: allow(key) is True while fewer than
`limit` requests from `key` landed in the last `window_s` seconds."""

def __init__(self, limit: int = RATE_LIMIT_PER_MIN, window_s: float = 60.0):
self.limit = limit
self.window_s = window_s
self._hits: dict[str, deque] = {}
self._lock = threading.Lock()

def allow(self, key: str) -> bool:
now = time.monotonic()
cutoff = now - self.window_s
with self._lock:
hits = self._hits.setdefault(key, deque())
while hits and hits[0] <= cutoff:
hits.popleft()
if len(hits) >= self.limit:
return False
hits.append(now)
return True


class ConcurrencyGate:
"""Per-key cap on simultaneous proofs. acquire() is non-blocking:
False means the key is already at its cap (caller answers 429 /
a rate_limited error rather than queueing unboundedly)."""

def __init__(self, limit: int = MAX_CONCURRENT_PROOFS):
self.limit = limit
self._in_flight: dict[str, int] = {}
self._lock = threading.Lock()

def acquire(self, key: str) -> bool:
with self._lock:
if self._in_flight.get(key, 0) >= self.limit:
return False
self._in_flight[key] = self._in_flight.get(key, 0) + 1
return True

def release(self, key: str) -> None:
with self._lock:
n = self._in_flight.get(key, 0)
if n <= 1:
self._in_flight.pop(key, None)
else:
self._in_flight[key] = n - 1

def in_flight(self, key: str) -> int:
with self._lock:
return self._in_flight.get(key, 0)
Loading
Loading