From 25dad55f38f471a20163782d166b8dd07e5d618d Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 23 Oct 2026 05:55:33 +0000 Subject: [PATCH 1/2] =?UTF-8?q?docs:=20reject=20ADR=200016=20=E2=80=94=20C?= =?UTF-8?q?lawQL=20stays=20TypeScript/Effect/Bun/celld?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit No Rust product path: dual-process e2e showed no memory win and a latency cost. Withdraw clawql-cellrt; keep Lean/TLA+/gdp-ts; close dataplane stack. Co-authored-by: Daniel Smith --- ...isolation-agent-substrate-sandbox-celld.md | 14 +- docs/adr/0014-formal-methods-tla-lean.md | 4 +- docs/adr/0016-rust-dataplane-spike.md | 129 +--- docs/design/correctness-by-construction.md | 48 +- docs/streams/clawql-cellrt.md | 634 +----------------- 5 files changed, 73 insertions(+), 756 deletions(-) diff --git a/docs/adr/0011-isolation-agent-substrate-sandbox-celld.md b/docs/adr/0011-isolation-agent-substrate-sandbox-celld.md index e1fd5791c..7fd50b0a6 100644 --- a/docs/adr/0011-isolation-agent-substrate-sandbox-celld.md +++ b/docs/adr/0011-isolation-agent-substrate-sandbox-celld.md @@ -1,14 +1,14 @@ --- -title: "Isolation Architecture: Agent Substrate for clawql-sandbox, celld for clawql-cellrt" +title: "Isolation Architecture: Agent Substrate for clawql-sandbox, celld for durable cells" status: "September 2026 — decided, part of 8.0.0" version: "0.1" adr: "0011" -package: "packages/clawql-sandbox/ (Agent Substrate adoption) + celld / clawql-cellrt (unchanged V8-isolate model)" +package: "packages/clawql-sandbox/ (Agent Substrate adoption) + celld (V8-isolate durable cells; clawql-cellrt withdrawn)" --- # ADR 0011: Isolation Architecture -## Agent Substrate for clawql-sandbox, celld for clawql-cellrt +## Agent Substrate for clawql-sandbox, celld for durable cells **September 2026 · Decided · Part of 8.0.0** @@ -20,7 +20,7 @@ package: "packages/clawql-sandbox/ (Agent Substrate adoption) + celld / clawql-c **Implementation honesty (as of this ADR's first code drop):** the tree ships a ClawQL-owned **control-plane adapter** (in-process mock + optional HTTP client to an operator-provided URL). It does **not** yet vendor or depend on Google's Agent Substrate packages/CRDs. Until that integration lands, treat “adopts Agent Substrate” as the architectural decision + selection/WORM scaffolding, not as a claim that Substrate microVMs are running in this repo. -`clawql-cellrt` / **celld** continues to use celld's V8-isolate model, unchanged. **These are not competing choices for the same problem** — they are the correct backend for two genuinely different problems. This ADR exists so that distinction is never silently re-litigated by treating "Agent Substrate is newer/denser/Google-backed" as a reason to also apply it to celld's workload. +**celld** continues to use the V8-isolate model for durable cells / Streams / ProgramCellDO. A planned owned Rust runtime (`clawql-cellrt`) was **withdrawn** ([ADR 0016](./0016-rust-dataplane-spike.md) Rejected; [`clawql-cellrt.md`](../streams/clawql-cellrt.md)). **Agent Substrate and celld are not competing choices for the same problem** — they are the correct backend for two genuinely different problems. This ADR exists so that distinction is never silently re-litigated by treating "Agent Substrate is newer/denser/Google-backed" as a reason to also apply it to celld's workload. --- @@ -36,7 +36,7 @@ Adopting Agent Substrate **supersedes** the earlier parked question of whether ` ### 3.1 Different problems -| | Agent Substrate / `clawql-sandbox` | celld / `clawql-cellrt` | +| | Agent Substrate / `clawql-sandbox` | celld (durable cells) | | ----------------- | -------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------ | | Threat model | Untrusted / unpredictable code; host-escape, credential theft, exfiltration risk | Fixed-shape TypeScript orchestration; no `child_process`/`fs`/`net` by construction | | Question answered | How do I safely run code I cannot fully trust or predict? | How do I run enormous numbers of small, already-trusted-by-construction pieces as cheaply as possible? | @@ -60,7 +60,7 @@ uncontained? bounded pre-declared actions, still independently enforced by Panguard regardless of host isolation - -> celld / clawql-cellrt (V8 isolate) + -> celld (V8 isolate) ``` New workloads must classify explicitly against this rule in their introducing specification — never by analogy to "we already use Agent Substrate elsewhere" or "we already use celld elsewhere." @@ -97,7 +97,7 @@ As of this writing, Agent Substrate is open source and generally available for * | This ADR | `docs/adr/0011-isolation-agent-substrate-sandbox-celld.md` | | Backend | `packages/clawql-sandbox/src/agent-substrate/` | | Decision rule | `packages/clawql-sandbox/src/isolation-decision.ts` | -| celld / cellrt note | `docs/streams/clawql-celld.md`, `docs/streams/clawql-cellrt.md` (isolation rule; runtime unchanged) | +| celld note | `docs/streams/clawql-celld.md` (isolation rule); `docs/streams/clawql-cellrt.md` (withdrawn) | --- diff --git a/docs/adr/0014-formal-methods-tla-lean.md b/docs/adr/0014-formal-methods-tla-lean.md index 4c135c5fc..95240768a 100644 --- a/docs/adr/0014-formal-methods-tla-lean.md +++ b/docs/adr/0014-formal-methods-tla-lean.md @@ -2,7 +2,7 @@ - Status: Accepted - Date: 2026-10-07 -- Related: [ADR 0013 gdp-ts](./0013-gdp-ts-compile-time-auth-proofs.md), [ADR 0015 program mode](./0015-program-mode-alongside-search-execute.md) (batch Merkle mandates + Lean IFC), [ADR 0016 Rust data-plane spike](./0016-rust-dataplane-spike.md) (Verus trial), [correctness by construction](../design/correctness-by-construction.md), [execute pause/resume](../specs/risk/execute-pause-resume-v0.1.md), [`formal/tla/mandate/`](../../formal/tla/mandate/), [`formal/tla/events/`](../../formal/tla/events/), [`formal/lean/`](../../formal/lean/) +- Related: [ADR 0013 gdp-ts](./0013-gdp-ts-compile-time-auth-proofs.md), [ADR 0015 program mode](./0015-program-mode-alongside-search-execute.md) (batch Merkle mandates + Lean IFC), [ADR 0016 Rust data-plane spike](./0016-rust-dataplane-spike.md) (**Rejected** — no Verus/Rust track), [correctness by construction](../design/correctness-by-construction.md), [execute pause/resume](../specs/risk/execute-pause-resume-v0.1.md), [`formal/tla/mandate/`](../../formal/tla/mandate/), [`formal/tla/events/`](../../formal/tla/events/), [`formal/lean/`](../../formal/lean/) ## Context @@ -11,7 +11,7 @@ ClawQL’s risk splits into two classes E2E and gdp-ts do not close: 1. **Concurrency and protocol bugs** — races across gateway replicas, retries, expiry, resume. 2. **Decision logic bugs** — risk classification, approval policy, information-flow, mandate binding. -Lean and TLA+ (or Quint) are the mature tools for those halves. Bend is watch-only. **Verus** (PDD Kit trial) is scoped on the Rust data-plane policy kernel in [ADR 0016](./0016-rust-dataplane-spike.md); Kani / celld sandbox proofs remain later. +Lean and TLA+ (or Quint) are the mature tools for those halves. Bend is watch-only. A Verus / Rust data-plane trial was scoped in [ADR 0016](./0016-rust-dataplane-spike.md) and **Rejected** (2026-10-23): ClawQL stays TypeScript + Effect + Bun + celld; policy oracles remain Lean + differential vs production TS. ## Decision diff --git a/docs/adr/0016-rust-dataplane-spike.md b/docs/adr/0016-rust-dataplane-spike.md index a0d4662f6..b4fc2e38a 100644 --- a/docs/adr/0016-rust-dataplane-spike.md +++ b/docs/adr/0016-rust-dataplane-spike.md @@ -1,122 +1,57 @@ # ADR 0016: Rust data-plane spike (execute hot path + Verus trial) -- Status: Proposed +- Status: **Rejected** - Date: 2026-10-22 -- Related: [ADR 0014 formal methods](./0014-formal-methods-tla-lean.md) · [ADR 0015 program mode](./0015-program-mode-alongside-search-execute.md) · [ADR 0011 isolation](./0011-isolation-agent-substrate-sandbox-celld.md) · [ADR 0013 gdp-ts](./0013-gdp-ts-compile-time-auth-proofs.md) · [correctness by construction](../design/correctness-by-construction.md) · [`clawql-cellrt`](../streams/clawql-cellrt.md) · [dominance roadmap](../benchmarks/dominance-roadmap.md) · [measured defaults](../benchmarks/cloudflare-multiturn/measured-defaults.md) · [`formal/lean/`](../../formal/lean/) +- Decided: 2026-10-23 +- Related: [ADR 0014 formal methods](./0014-formal-methods-tla-lean.md) · [ADR 0015 program mode](./0015-program-mode-alongside-search-execute.md) · [ADR 0011 isolation](./0011-isolation-agent-substrate-sandbox-celld.md) · [ADR 0013 gdp-ts](./0013-gdp-ts-compile-time-auth-proofs.md) · [correctness by construction](../design/correctness-by-construction.md) · [`clawql-celld`](../streams/clawql-celld.md) · [measured defaults](../benchmarks/cloudflare-multiturn/measured-defaults.md) · [`formal/lean/`](../../formal/lean/) ## Context -ClawQL’s formal stack today proves **models**, not the production TypeScript that runs: +This ADR proposed a thin Rust Streamable-HTTP execute plane (`clawql-dataplane`) plus a Verus trial on the approval-policy kernel, to chase memory/tail vs Bun/`--smol` and to prove production policy code. -| Layer | What it proves | Gap | -| ---------- | --------------------------------------------- | ------------------------------------------------------------- | -| **TLA+** | Mandate / batch / event protocols | Design of races and crash boundaries — not the gateway binary | -| **Lean** | Approval policy + IFC oracles | Executable model; production matches via differential sample | -| **gdp-ts** | Compile-time capability flow on TS call sites | Types, not runtime semantics | - -Microsoft Research’s **Proof Driven Development Kit (PDD Kit)** + **Verus** (GitHub Universe, Oct 2026) aims at a different claim: prove that **the Rust code that runs** meets a formal spec for every input. Where proof is not possible, it falls back to tests and computer-use agents. That only applies if security-critical pieces are actually written in Rust. - -Separately, Bun/`--smol` plateaus near **~130 MB** anon under lean listen **on the October 15 build**, within ~35–45 MB of peer Go/Rust gateways ([measured defaults](../benchmarks/cloudflare-multiturn/measured-defaults.md)). Tip lean probe is higher (~170–260 MB) — a **separate lean-floor open item** from the JSON `_streamMapping` climb ([memory-plateau](../benchmarks/cloudflare-multiturn/memory-plateau.md)). Week-2 baseline: tip Bun **after** the climb fix plateaus, then remasure lean (or accept a named new floor). Do not compare Rust against the leaking climb. Tail latency and residual gateway overhead on the execute path remain open levers ([executor side-by-side](../benchmarks/executor-comparison/), [hot-path RSS map](../../Memory/execute-hotpath-rss-growth-sources-ranking.md) in vault). A Rust **data plane** for the known-operation execute path is the natural place to try both: memory/tail gains **and** Verus-backed policy kernels. - -This is **not** [`clawql-cellrt`](../streams/clawql-cellrt.md) (owned Durable-Objects-style Rust + Wasmtime cell runtime). The spike is a thin Streamable-HTTP gateway in front of today’s TypeScript host. cellrt remains the Streams/cell substrate plan. - -ADR 0014 deferred Verus/Kani to “later for celld’s Rust sandbox core.” This ADR promotes a **scoped Verus trial on the data-plane policy kernel** first — smaller surface, Lean properties already written. +ClawQL’s lasting formal stack remains **TLA+** (protocols), **Lean** (policy oracles + differential vs TypeScript), and **gdp-ts** (compile-time capability flow). See [ADR 0014](./0014-formal-methods-tla-lean.md). ## Decision question (one) **Does moving the known-operation `execute` hot path to Rust close memory and tail gaps enough to justify building it properly, and can its critical pure pieces be proved correct with Verus (PDD Kit trial)?** -Evidence answers go/no-go. A finished product is out of scope. - -## Decision (spike shape) - -### In: one path, end to end - -Known-operation `execute` over Streamable HTTP (JSON mode) — ClawQL’s fastest-growing path and the one every latency/RSS board exercises: - -| Slice | Spike behavior | Production anchors (today) | -| ---------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| **MCP endpoint** | Streamable HTTP; `tools/call` for `execute` + minimal `tools/list` | [`src/http/mcp-http-server.ts`](../../src/http/mcp-http-server.ts) — start from official Rust MCP SDK (`rmcp`) | -| **Catalog** | Read-only from the existing SQLite catalog the TypeScript build already produces; no new format | SQLite catalog / OOP catalog path used by host today | -| **Governance** | API-key or token verify → risk class → allow / park / deny → session IFC labels → single-use mandate consume (same conditional Postgres `UPDATE…WHERE` as TLA+ Consume) | [`execute-core.ts`](../../packages/clawql-api/src/execute/execute-core.ts), [`classify-operation-risk.ts`](../../packages/clawql-api/src/risk/classify-operation-risk.ts), [`session-ifc-enforce.ts`](../../packages/clawql-api/src/ifc/session-ifc-enforce.ts), [`pending-execution-store.ts`](../../packages/clawql-api/src/pending/pending-execution-store.ts) | -| **Upstream** | Pooled HTTP client with keep-alive | REST execute path in `clawql-api` | -| **Results** | Projection, `where` via a Rust JMESPath crate, result budget | [`where-filter.ts`](../../packages/clawql-api/src/execute/where-filter.ts) | -| **Audit** | Same hash-chained process-WORM format so existing verifiers work | [`clawql-audit`](../../packages/clawql-audit/) | - -### Out (stay TypeScript) - -Console, catalog **building**, search/discovery, program mode / durable journal, decision sites, memory tools, OpenAPPA, OAuth server, celld isolate path, optional tools. The Rust process **forwards** non-execute traffic to the existing TypeScript server. - -### Architecture - -``` -Client ──Streamable HTTP──▶ Rust data plane ──execute hot path──▶ upstream APIs - │ - └── other MCP / tools ──forward──▶ TypeScript host (unchanged) -``` - -One process boundary. If the spike fails, delete the Rust process; Helm/Bun host stays. - -### How correctness is established - -1. **Differential tests vs TypeScript** — same requests through both paths must agree on results, park/deny/allow decisions, and audit records. Fuzz JMESPath/`where` specifically (highest semantic-drift risk between crates). -2. **Existing boards remasured through the Rust path** (not new category claims): - - Governance / policy-depth — [`docs/benchmarks/governance-policy-depth/`](../benchmarks/governance-policy-depth/) - - Multi-attack injection — [`docs/benchmarks/security-suite/multi-attack-injection/`](../benchmarks/security-suite/multi-attack-injection/) - - Approval integrity — [`docs/benchmarks/security-suite/approval-integrity/`](../benchmarks/security-suite/approval-integrity/) - - Gateway multi / Cloudflare multiturn latency+RSS arms — [`gateway-multi-comparison`](../benchmarks/gateway-multi-comparison/), [`cloudflare-multiturn`](../benchmarks/cloudflare-multiturn/) -3. **Verus proofs (PDD Kit trial) on three small pure components** — Lean properties become the starting specs: - -| Component | Properties (from Lean / production) | Sources | -| -------------------- | ------------------------------------------------------------------------------------------ | ----------------------------------------------------------------------------------------------------------------------------------------------------------- | -| **Policy evaluator** | No self-approval; N-of-M needs N distinct people; deny destructive when configured | [`formal/lean/ApprovalPolicy.lean`](../../formal/lean/ApprovalPolicy.lean), [`approval-policy.ts`](../../packages/clawql-api/src/policy/approval-policy.ts) | -| **Label merge** | Labels only grow; overflow merge moves toward untrusted; write iff combined label may flow | [`formal/lean/InformationFlow.lean`](../../formal/lean/InformationFlow.lean), [`labels.ts`](../../packages/clawql-api/src/ifc/labels.ts) | -| **Approval digests** | Canonical args → same digest; any arg change → different digest (`argsHash`) | [`args-hash.ts`](../../packages/clawql-api/src/pending/args-hash.ts) | - -**Not AgentDojo.** There is no in-tree AgentDojo board; do not invent one for the spike ([agentready proposal](../proposals/agentready-act-safely.md) forbids claiming AgentDojo until published). Multi-attack + approval-integrity are the adversarial remasure set. - -**What Verus will not cover (keep TLA+ / Lean / differential):** +## Decision (spike outcome) — 2026-10-23 -- Distributed races, crashes, DB atomicity → TLA+ ([`formal/tla/mandate/`](../../formal/tla/mandate/)) -- Spec mistakes → humans review specs (PDD Kit framing); Lean gives the head start -- Research maturity → prove **one** kernel before planning a factory around it +**Rejected.** ClawQL stays a **TypeScript + Effect TS v4** codebase with **Bun** as the default host runtime, **celld** for durable isolate/Streams workloads, and **Node** only for compatibility where required. **No Rust** in the product tree (no `crates/`, no Verus kernels, no dual-process dataplane). -### What to measure (bars set before coding) +### Evidence that drove no-go -Baselines from Bun lean listen / peer boards ([measured defaults](../benchmarks/cloudflare-multiturn/measured-defaults.md)): +| Evidence | Result | +| --- | --- | +| Component plane (direct MCP → Rust) | Governed CF known-op ~**15.8 MB** vs Bun ~**128 MB** — looks like a large density win **if** you ignore the Bun host | +| Product path (Bun → Rust forward, e2e) | Summed Anonymous RSS ~**124.8 MB** vs Bun-only ~**124.4 MB** — **tied**; dataplane-only RSS is not a product cite | +| Latency (e2e) | Forward hop costs session p50 (~**21 ms** dual vs ~**13 ms** Bun-only) and worsens call p999 | +| Peers | MCPJungle / agentgateway still ~**99–102 MB** — dual-process does not take memory leadership | +| Ops | Two processes, catalog/version skew, claim complexity — not justified by e2e numbers | -| Metric | Baseline (today) | Spike go bar (proposed) | -| ----------------------- | ---------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------ | -| **Anon RSS under load** | Bun ~**125–130 MB** (**Oct 15 build**); tip lean ~**173 MB**; peers ~**99–103 MB** | ≤ **half of tip Bun after leak fix** **or** within peer band with clear headroom — pick one bar in Phase 0 and freeze it | -| **Latency** | p50 / p99 / p999 on equal-arm REST execute | Clearly better **p999** than Bun host on the same board; unexplained HTTP stalls gone or explained | -| **Clients / instance** | Bun median **84** @ p99 ≤ 100 ms (HTTP multiplex) | Meet or beat Bun on the same workflow | -| **Correctness** | — | **Zero** differential mismatches on the agreed suite | +Spike branches measured the stack; they are **not** to be merged. Production remains single-process Bun (or celld for the isolate path). -**Proposed go criterion (freeze in Phase 0):** memory ≤ half Bun **or** ≤ peer gateway band with ≥20 MB headroom; clearly better p999; zero differential diffs; Verus proves at least the policy evaluator (label merge + digests are stretch). Otherwise TypeScript/Bun stays, and the write-up records why cheaply. +### What we keep -## Phases (technical milestones, not a calendar) +1. **Bun `--smol`** as default host MCP (product ladder: celld isolate → Bun host → Node minority). +2. **celld** for Streams / ProgramCellDO durability ([ADR 0011](./0011-isolation-agent-substrate-sandbox-celld.md), [`clawql-celld`](../streams/clawql-celld.md)). +3. **Lean + TLA+ + gdp-ts** as the formal story ([ADR 0014](./0014-formal-methods-tla-lean.md)). No Verus / Kani track. +4. Memory and latency work continues **inside** TypeScript/Bun (lean listen, catalog, HTTP path) — not via a second language. -| Phase | Deliverable | Exit | -| -------------------------- | ------------------------------------------------------------------------------------------------------------------------------------ | --------------------------------------------------- | -| **0 — Freeze** | Bar spreadsheet, board list, crate layout under `crates/clawql-dataplane/`, Verus/PDD Kit toolchain pin, differential harness sketch | Written bars + harness stub merged | -| **A — Bare fast path** | Endpoint + catalog read + upstream call + `where`/projection; **no** governance | Latency/RSS vs Bun; if no signal, stop | -| **B — Governance + audit** | Risk → IFC → consume → WORM; differential suite green | Diff = 0 on suite | -| **C — Proof + boards** | Verus on policy (± labels/digests); remasure governance + multi-attack + approval-integrity + one latency/RSS board (3 runs) | Proofs or honest “could not prove X”; board numbers | -| **D — Decision** | Spike report + **go/no-go** recorded in this ADR (status → Accepted/Rejected) | Single owner decision | +### What we discard -If go: plan for Rust to become the **only** policy-engine implementation (called from TypeScript via FFI/gRPC/WASM as needed). Dual implementations drifting is the long-term risk that kills the win. +- `crates/clawql-dataplane` and any `crates/` Rust workspace +- `formal/verus/` +- Dual-process forward (`CLAWQL_DATAPLANE_*`), Helm dataplane stack, dataplane Docker image +- Planned **clawql-cellrt** Rust runtime — durability stays on **celld**; see [`clawql-cellrt.md`](../streams/clawql-cellrt.md) (withdrawn) ## Consequences -- **Accepted go:** invest in productionizing the data plane; keep TLA+ for protocols; migrate Lean oracles → Verus specs as source of truth for the three kernels; retire dual TS evaluators over time. -- **Rejected / no-go:** delete `crates/clawql-dataplane/`; Bun/TS remains default; keep Lean+differential as the policy story; optional note that Verus was tried and what blocked it. -- **cellrt unchanged:** DO/cell substrate stays [`clawql-cellrt`](../streams/clawql-cellrt.md); this ADR does not authorize building cellrt. -- **Copy:** do not claim “mathematically proven policy” until Verus proofs land **and** the go decision is Accepted. Until then: “Lean oracle + differential” (ADR 0014 wording). +- Do **not** merge open dataplane / Verus / density-baseline Rust PRs into `main`. +- Do **not** cite dataplane-only RSS on clawql.com/benchmarks. +- Copy: ClawQL is TypeScript/Effect/Bun/celld — not a Rust gateway project. +- Future memory wins must show up on **single-process** (or honest multi-process **sum**) boards against peers. -## Out of scope for the spike +## Out of scope (historical) -- Replacing Bun as default Helm host -- Program mode / celld ProgramCellDO in Rust -- Full MCP tool surface -- Shipping PDD Kit / Chopin as a customer-facing product -- AgentDojo or any unpublished peer board +The spike never authorized replacing Bun as default Helm host, rewriting program mode in Rust, or shipping PDD Kit as a customer product. Those remain out of scope under Rejected as well. diff --git a/docs/design/correctness-by-construction.md b/docs/design/correctness-by-construction.md index 575bef59f..badd15eff 100644 --- a/docs/design/correctness-by-construction.md +++ b/docs/design/correctness-by-construction.md @@ -1,15 +1,15 @@ --- -title: "Correctness by construction — NASA Power of 10, SPARK Ada, Effect-TS, Rust + TLA+" -status: "Draft · August 2026" -applies_to: "clawql-tee · clawql-cellrt · clawql-streams · clawql-ouroboros · Effect packages · OpenBench / LAB gates" +title: "Correctness by construction — NASA Power of 10, SPARK Ada, Effect-TS, TLA+/Lean" +status: "Draft · August 2026 · amended 2026-10-23 (no Rust product path)" +applies_to: "clawql-streams · clawql-celld · clawql-ouroboros · Effect packages · OpenBench / LAB gates" companions: "docs/security/security-ontology-knowledge-loop.md · docs/benchmarks/harvey-lab-campaign-memory.md" --- -# Correctness by construction — NASA, SPARK, Effect-TS, Rust +# Correctness by construction — NASA, SPARK, Effect-TS, TLA+/Lean -**August 2026 · Draft** +**August 2026 · Draft** (Rust/cellrt product path withdrawn — [ADR 0016](../adr/0016-rust-dataplane-spike.md) Rejected) -**Related:** [clawql-tee](../streams/clawql-tee.md) · [clawql-cellrt](../streams/clawql-cellrt.md) · [clawql-streams](../streams/clawql-streams.md) · [Effect rearchitecture](./effect-ts-modularization-rearchitecture-plan.md) · [Ouroboros](../ouroboros/clawql-ouroboros.md) · [Security↔ontology loop](../security/security-ontology-knowledge-loop.md) · [LAB campaign memory](../benchmarks/harvey-lab-campaign-memory.md) +**Related:** [clawql-celld](../streams/clawql-celld.md) · [clawql-streams](../streams/clawql-streams.md) · [Effect rearchitecture](./effect-ts-modularization-rearchitecture-plan.md) · [Ouroboros](../ouroboros/clawql-ouroboros.md) · [Security↔ontology loop](../security/security-ontology-knowledge-loop.md) · [LAB campaign memory](../benchmarks/harvey-lab-campaign-memory.md) · [ADR 0014](../adr/0014-formal-methods-tla-lean.md) This note consolidates transferable lessons from: @@ -17,7 +17,7 @@ This note consolidates transferable lessons from: 2. **Shuttle-era process discipline** (IBM Federal Systems — extremely low defect density via specs, independent review, defect-driven process) 3. **Ada / SPARK** — contracts, information flow, Ravenscar-style concurrency 4. **What Effect-TS already buys on the TypeScript side** -5. **What safe Rust + TLA+/Alloy buy on the cellrt/tee side** +5. **What TLA+/Lean + gdp-ts buy for ClawQL protocols and policy** (no Verus/Rust track) **Thesis (shared with Jane Street / OxCaml-style thinking):** do not rely on programmer discipline. Make incorrect states **unrepresentable**, **uncompilable**, **unpromotable**, or **exhaustively ruled out** — preferably before code exists. @@ -96,35 +96,19 @@ Already in ClawQL’s direction ([Effect rearchitecture](./effect-ts-modularizat --- -## 5. Rust (cellrt / tee) — three layers +## 5. Formal models (design time) — TLA+ / Lean / gdp-ts -### Layer 1 — Type system (compile time) - -- Ownership: non-`Clone` `VirtualKey` / single-holder semantics -- `Send` / `Sync` for cross-task safety -- Exhaustive `enum` cell state machine -- Newtypes (`Percentage`, `CellId`, …) with validating constructors -- `Result` + `?` + `#[must_use]` on WORM writes - -### Layer 2 — Runtime assertions - -- `assert!` on production invariants; `debug_assert!` for expensive checks -- Checked arithmetic on budgets -- Explicit collection upper bounds on security-critical paths - -### Layer 3 — Formal models (design time) - -Per [ADR 0014](../adr/0014-formal-methods-tla-lean.md): +ClawQL does **not** ship a Rust product plane ([ADR 0016](../adr/0016-rust-dataplane-spike.md) Rejected; `clawql-cellrt` withdrawn). Correctness-by-construction on the host is **Effect-TS + TypeScript types**; protocol/policy proofs stay: | Tool | Role | | ---------------- | ----------------------------------------------------------------------------------------- | | **TLA+ / Quint** | Protocol interleavings — mandates, events, jobs, promotion | -| **Lean** | Policy kernel oracle + differential tests (follow-on) | +| **Lean** | Policy kernel oracle + differential tests vs production TypeScript | | **gdp-ts** | Compile-time capability flow ([ADR 0013](../adr/0013-gdp-ts-compile-time-auth-proofs.md)) | **P0 protocol model (started):** [`formal/tla/mandate/`](../../formal/tla/mandate/) — pending-execution mandate lifecycle (at-most-once side effect, digest bind, approver ≠ requester). -Still planned for tee/cellrt: +Still useful model targets (implemented in TS/celld, proved in TLA+/Lean as earned): 1. **Key uniqueness** — no two Running cells share an active virtual key 2. **WORM append-only** — written entries never mutate @@ -179,12 +163,10 @@ Same loop as [security↔ontology](../security/security-ontology-knowledge-loop. | Priority | Work | | -------- | --------------------------------------------------------------------------------------------------------------- | -| **P0** | Document required caps on streams/Ouroboros APIs; WORM-fail → halt policy in tee/cellrt specs | +| **P0** | Document required caps on streams/Ouroboros APIs; WORM-fail → halt policy in celld/Streams specs | | **P0** | Effect Schema at remaining untrusted boundaries; STM/Ref for budget paths in inference/payments | | **P0** | TLA+ mandate lifecycle ([`formal/tla/mandate/`](../../formal/tla/mandate/), ADR 0014) — then Lean policy oracle | -| **P1** | TLA+ sketches for key uniqueness + WORM append-only + cell liveness (before heavy tee Rust) | -| **P1** | Rust newtypes + exhaustive cell FSM + `#[must_use]` WORM APIs in cellrt | -| **P2** | Preallocated cell pools; Wasmtime memory ceilings after init | +| **P1** | TLA+ sketches for key uniqueness + WORM append-only + cell liveness (celld path) | | **P2** | Wire demotion / escalation into ontology FailedStrategy / SecurityEvent (companion specs) | --- @@ -197,10 +179,10 @@ Same loop as [security↔ontology](../security/security-ontology-knowledge-loop. | Unbounded agent loops | **Forbidden** — caps required | | Failed WORM write | **Fail closed / halt cell** | | Effect-TS role | Primary DbC/DI/concurrency tool on TS; not a substitute for TLA+ on global invariants | -| Rust role | Memory/ownership/FSM; plus asserts; plus TLA+ for three tee invariants | +| Language / runtime | TypeScript + Effect v4 on Bun (default); celld for durable isolates; **no Rust** | | SPARK/Ada | Inspiration for contracts + info flow + Ravenscar — not “rewrite ClawQL in Ada” | | Process | Spec-before-code; defects improve gates/ontology/security loop | --- -_Companion to clawql-tee / cellrt · Effect modularization · security↔ontology knowledge loop · LAB campaign memory · Constitutional Ouroboros_ +_Companion to celld / Streams · Effect modularization · security↔ontology knowledge loop · LAB campaign memory · Constitutional Ouroboros_ diff --git a/docs/streams/clawql-cellrt.md b/docs/streams/clawql-cellrt.md index f35118308..756303cdd 100644 --- a/docs/streams/clawql-cellrt.md +++ b/docs/streams/clawql-cellrt.md @@ -1,626 +1,26 @@ -# clawql-cellrt — Specification v0.1 +# clawql-cellrt — Withdrawn -**Hands-on walkthrough:** [Streams getting started (Learn)](https://docs.clawql.com/learn/streams-getting-started) — Labs 1–3 for schedule + NATS today; **§4** in the reading order for cellrt. +**Status:** **Withdrawn** · 2026-10-23 +**Superseded by:** [`clawql-celld.md`](./clawql-celld.md) + [ADR 0011](../adr/0011-isolation-agent-substrate-sandbox-celld.md) · [ADR 0016](../adr/0016-rust-dataplane-spike.md) (**Rejected**) -**Status:** Draft · August 2026 · v0.1 -**Language:** Rust (+ Wasmtime; Effect-TS tool surface via WASM component) -**Package:** `clawql-cellrt` (planned — `crates/clawql-cellrt`) -**Depends on:** [`clawql-streams`](./clawql-streams.md) v0.2 · [`clawql-celld.md`](./clawql-celld.md) · [`clawql-inference`](../inference/clawql-inference.md) · `@clawql/wasm-polyfills` (planned) · `@clawql/effect-wasm` (planned) -**Repo home:** ClawQL monorepo — `crates/clawql-cellrt/` (not a separate product repo) -**Related:** [`clawql-tee.md`](./clawql-tee.md) · [`clawql-tee-airgap-audit.md`](./clawql-tee-airgap-audit.md) · [`clawql-durable-objects.md`](./clawql-durable-objects.md) · [`../specs/network/clawql-network-v0.1.md`](../specs/network/clawql-network-v0.1.md) · [`mcp-api-adapter`](../mcp/mcp-api-adapter.md) · [defense-in-depth](../security/clawql-security-defense-in-depth.md) · [codegraph](../plugins/codegraph.md) · [correctness-by-construction](../design/correctness-by-construction.md) (NASA/SPARK → Rust + TLA+ for key/WORM/liveness invariants) +## Decision ---- +ClawQL will **not** build an owned Rust/Wasmtime cell runtime (`crates/clawql-cellrt`). -## 1. What this is +| Layer | Owner | +| --- | --- | +| Host MCP (search, execute, plugins, memory, OAuth, …) | **TypeScript + Effect TS v4** on **Bun** (default); Node for compatibility | +| Durable isolate / Streams / ProgramCellDO | **celld** (self-hosted Durable Objects–compatible runtime) | +| Formal methods | **TLA+** + **Lean** + **gdp-ts** — not Verus/Rust | -`clawql-cellrt` is ClawQL's **owned cell runtime** — a Rust binary that provides a Durable Objects–style execution model purpose-built for ClawQL workloads, with embedded security monitoring, inference gateway, HashiCorp Vault integration, and full observability. +ADR 0016 rejected a Rust execute data plane after dual-process e2e boards showed **no product memory win** (summed Bun+dataplane ≈ Bun-only) and a latency cost. The same product stance applies here: do not introduce a Rust toolchain or `crates/` tree into ClawQL. -It is **not** a general-purpose DO runtime and **not** a Node `worker_threads` reimplementation. It is the ClawQL-specific production runtime that celld would need to be if ClawQL owned it end-to-end. +## What to use instead -**Not the execute data-plane spike.** A separate proposal ([ADR 0016](../adr/0016-rust-dataplane-spike.md)) scopes a thin Rust Streamable-HTTP gateway for known-operation `execute` (memory/tail + Verus trial on policy kernels). That spike forwards everything else to today’s TypeScript host; it does **not** authorize building cellrt. +- Streams / durable programs: [`clawql-celld.md`](./clawql-celld.md), Streams getting started on docs.clawql.com +- Isolation boundaries: [ADR 0011](../adr/0011-isolation-agent-substrate-sandbox-celld.md) (celld for cells; Agent Substrate for `sandbox_exec`) +- Host runtime ladder: celld (isolate) → Bun (default host) → Node (minority) -### Why build rather than only use celld +## Historical note -| Concern | celld (adopt) | clawql-cellrt (own) | -| ------------------ | ----------------------------------------- | ----------------------------------------------------------------------------- | -| Status | Alpha; hostile multi-tenant not supported | ClawQL-owned; production target | -| Security story | V8 isolate + operator mesh | Rust memory safety + eBPF + WASM capability sandbox | -| Vault / inference | External sidecars / HTTP | Embedded dynamic secrets + model escalation + virtual keys | -| Observability | External | Embedded OTel + Prometheus + Langfuse | -| Tool execution | JS bundle in V8 | Bootstrap: HTTP → clawql-mcp; full: `clawql-core.wasm` in Wasmtime | -| Workers API parity | High (same surface as Cloudflare) | Different API (Rust cell trait + WIT); session _contract_ shared with Streams | - -**Streams v0.2 still adopts celld** for the Workers/DO JavaScript path and as an interim self-hosted option. **cellrt is the ClawQL-owned production path** when sovereignty, security-in-depth, and embedded ClawQL capabilities matter more than Cloudflare Workers API parity. - -**Do not build a custom DO runtime on Node `worker_threads`.** cellrt is Rust + Wasmtime. celld remains the Workers-API-compatible self-hosted option. - -### Isolation architecture (ADR 0011) - -`clawql-cellrt` / celld **do not** adopt Agent Substrate. Agent Substrate is the isolation backend for **`clawql-sandbox`** (untrusted arbitrary code). Cell workloads remain V8-isolate (celld) or the owned Rust/Wasmtime path (cellrt). Replacing cell isolation with microVMs would regress cold-start for a threat model cells structurally do not have. See [`docs/adr/0011-isolation-agent-substrate-sandbox-celld.md`](../adr/0011-isolation-agent-substrate-sandbox-celld.md). - -### Repo placement (decision of record) - -cellrt is **not** a general-purpose DO runtime (unlike celld). It is tightly coupled to ClawQL: - -- Virtual keys issued/validated by clawql-inference -- WORM event types and LTX bucket layout are ClawQL-specific -- WASM component is `clawql-core.wasm` with a ClawQL WIT world -- Vault injects ClawQL provider secret shapes -- Streams significance filters / subscriptions drive cell spawn -- RTP/OBT emission uses ClawQL training-data formats - -**Keep cellrt in the ClawQL monorepo** under `crates/clawql-cellrt/`. Accept Rust toolchain friction in a TypeScript-primary repo; cross-repo integration tests and Helm/release coordination would cost more. TypeScript companions (`@clawql/wasm-polyfills`, `@clawql/effect-wasm`) stay under `packages/`. - -**Extractable standalone:** the bucket coordination layer (compare-and-swap leases, LTX replication, peer HMAC) has no ClawQL-specific dependencies — publish later as `bucket-coordinator` on crates.io. Everything else remains ClawQL infrastructure. - -### Bootstrap path - -HTTP boundary ships first. Cells call a local `clawql-mcp` HTTP server for tool execution while the WASM path is built. Each tool that runs in-process replaces one HTTP call. The transition is invisible to MCP clients. Nothing blocks shipping cellrt coordination + lifecycle before Effect-TS → WASM is complete. - -### Path to clawql-tee - -cellrt as specified is **software security** (Rust, eBPF, WASM sandbox, Cosign, WORM). [`clawql-tee`](./clawql-tee.md) adds hardware-enforced guarantees (AMD SEV-SNP / Intel TDX, attestation-gated Vault secrets, optional NVIDIA GPU CC) and [`air-gap QR audit transport`](./clawql-tee-airgap-audit.md) so a verifier need not trust the operator or the network path. - ---- - -## 2. Architecture overview - -```text -clawql-cellrt binary (Rust, static, ~50–80 MB target) -│ -├─ Fleet coordinator (Tokio async) -│ ├─ S3/R2 bucket as coordinator (compare-and-swap ownership leases) -│ ├─ LTX replication (SQLite WAL segments → bucket, RPO=0) -│ ├─ Peer authentication (HMAC-SHA256, WireGuard-compatible) -│ ├─ Node discovery (bucket-based, no membership protocol) -│ └─ Fault recovery (ownership lease expiry → another node acquires) -│ -├─ Cell runtime (per-cell, Tokio task) -│ ├─ Wasmtime engine (embedded, one instance per cell) -│ │ └─ clawql-core.wasm (Effect-TS via ComponentizeJS + jco) -│ │ ├─ search · execute · memory_* · audit · cache -│ │ ├─ clawql-ontology (structured filter queries) -│ │ └─ mcp-api-adapter (six protocol surfaces) -│ ├─ Capability grants (network, storage, crypto — explicit WIT imports) -│ ├─ HTTP handler (axum, per-cell) -│ ├─ WebSocket handler (tokio-tungstenite, hibernation via task suspend) -│ └─ Alarm scheduler (tokio time::sleep_until, durable via SQLite) -│ -├─ Storage (per-cell) -│ ├─ SQLite via rusqlite (WAL mode, per-cell file) -│ ├─ LTX writer (streams WAL segments to bucket coordinator) -│ └─ WORM guarantees (acknowledge write only after bucket replication) -│ -├─ Security layer (clawql-security embedded) -│ ├─ eBPF program loader (libbpf-rs, Linux only) -│ ├─ Syscall monitor (Falco-equivalent rules engine) -│ ├─ WASM capability enforcer (validates WIT imports at instantiation) -│ ├─ Virtual key lifecycle (Rust struct, scoped to cell ID) -│ └─ Cosign binary attestation (verified at startup via sigstore-rs) -│ -├─ Inference layer (clawql-inference embedded) -│ ├─ model-escalation router (Frugal → Standard → Frontier based on policy.yaml) -│ ├─ Virtual key manager (issue on spawn, expire on drop) -│ ├─ Budget enforcer (hard cap, DeductionService via HTTP) -│ └─ WORM inference call store (SQLite, LTX-replicated) -│ -├─ Vault client (HashiCorp Vault dynamic secrets) -│ ├─ AppRole auth (VAULT_ROLE_ID + VAULT_SECRET_ID) -│ ├─ Dynamic secret lease on cell spawn -│ ├─ Secret injection into WASM env before instantiation -│ └─ Lease renewal tied to cell alarm lifecycle -│ -└─ Observability (embedded) - ├─ OTel SDK (opentelemetry-rust — traces, metrics, logs) - ├─ Prometheus exporter (/metrics on fleet HTTP) - ├─ Langfuse forwarder (RTP/OBT training data emission) - └─ Structured logging (tracing → JSON → Loki push) -``` - ---- - -## 3. Rust crate structure - -Monorepo layout (ClawQL repo root): - -```text -packages/ — TypeScript (npm) - clawql-core/ - clawql-streams/ - mcp-api-adapter/ - wasm-polyfills/ — @clawql/wasm-polyfills (planned) - effect-wasm/ — @clawql/effect-wasm (planned) - -crates/ - clawql-cellrt/ — Cargo workspace (ClawQL-specific) - Cargo.toml - cellrt-coordinator/ — wraps bucket-coordinator + ClawQL fleet semantics - cellrt-runtime/ — cell lifecycle, Wasmtime, HTTP/WS, alarms - cellrt-storage/ — SQLite + LTX WORM - cellrt-security/ — eBPF, capability enforcer, Cosign startup - cellrt-attestation/ — SEV-SNP/TDX remote attestation (tee path) - cellrt-inference/ — model escalation, virtual keys, call store - cellrt-vault/ — AppRole bootstrap; attestation auth for tee - cellrt-observability/ — OTel, Prometheus, Langfuse - cellrt-cli/ — start / deploy / diagnose / audit export - -# Extract later (crates.io, no ClawQL deps): -bucket-coordinator — CAS leases, LTX, peer HMAC over S3/R2 -``` - -| Crate | Responsibility | -| ---------------------- | ------------------------------------------------------------------------------ | -| `cellrt-coordinator` | Fleet join, leases, peer auth (depends on `bucket-coordinator` when extracted) | -| `cellrt-runtime` | Per-cell Tokio task, Wasmtime / HTTP bootstrap, axum, WebSocket, alarms | -| `cellrt-storage` | rusqlite WAL, LTX writer, WORM ack-after-replication | -| `cellrt-security` | eBPF rules, WIT import validation, Cosign binary verify | -| `cellrt-attestation` | AMD SEV-SNP / Intel TDX reports, VCEK/PCS chain, JWT delivery, QR frame bind | -| `cellrt-inference` | model-escalation router, virtual key issue/expire, budget, WORM call store | -| `cellrt-vault` | Dynamic secrets; AppRole → attestation-gated release when tee enabled | -| `cellrt-observability` | OTel, Prometheus `/metrics`, Langfuse RTP/OBT | -| `cellrt-cli` | Binary entry + `audit export` for air-gap QR sequence | - ---- - -## 4. Cell lifecycle - -### 4.1 Spawn - -```rust -pub struct CellId(String); // "agent:{subscription_id}:{event_id}" - -pub async fn spawn_cell( - id: CellId, - config: CellConfig, - coordinator: &FleetCoordinator, -) -> Result { - // 1. Acquire ownership lease (compare-and-swap in bucket) - let lease = coordinator.acquire_lease(&id).await?; - - // 2. Initialize per-cell SQLite (WAL mode) - let db = CellStorage::open(&id).await?; - - // 3. Request dynamic secrets from Vault - let secrets = VaultClient::request_dynamic_secrets(&config.vault_role).await?; - - // 4. Issue virtual key (scoped to cell ID) - let virtual_key = VirtualKeyManager::issue( - VirtualKeyParams { - scope: id.clone(), - budget_tokens: config.budget_tokens, - ttl_ms: config.virtual_key_ttl_ms, - } - ).await?; - - // 5. Write WORM spawn record (LTX → bucket before ack) - db.worm_append(WormEvent { - event_type: "CELL_SPAWNED", - cell_id: id.clone(), - virtual_key_id: virtual_key.id.clone(), - subscription_id: config.subscription_id.clone(), - event_hash: config.event_hash.clone(), - timestamp: Utc::now(), - }).await?; - - // 6. Instantiate WASM (or HTTP bootstrap) with capability grants + secrets - let wasm_instance = WasmRuntime::instantiate( - &id, - WasmConfig { - component_path: coordinator.resolve_component_path().await?, - env: secrets.to_env_map(), - virtual_key: virtual_key.clone(), - capabilities: config.allowed_capabilities, - } - ).await?; - - // 7. Set alarm for virtual key TTL (durable — survives process restart) - db.set_alarm(Utc::now() + Duration::milliseconds(config.virtual_key_ttl_ms)).await?; - - // 8. Start HTTP + WebSocket handlers - let http_server = CellHttpServer::start(&id, wasm_instance.clone()).await?; - - Ok(CellHandle { id, db, wasm_instance, virtual_key, http_server, lease }) -} -``` - -### 4.2 Request handling - -```rust -impl CellHandle { - pub async fn handle_request(&self, req: CellRequest) -> Result { - self.inference.check_budget(&self.virtual_key).await?; - - // Bootstrap: HTTP → clawql-mcp - // Full: in-process WASM via Wasmtime - let result = self.wasm_instance.call_tool(req).await?; - - self.db.worm_append(WormEvent { - event_type: "TOOL_CALL", - tool_name: req.tool_name.clone(), - input_hash: sha256(&req.arguments), - atr_scope_check: result.atr_result.clone(), - timestamp: Utc::now(), - }).await?; - - Ok(result.into()) - } -} -``` - -### 4.3 Alarm (virtual key TTL + cleanup) - -```rust -impl CellHandle { - pub async fn handle_alarm(&self) -> Result<()> { - self.inference.expire_key(&self.virtual_key).await?; - self.flush_training_data().await?; - - self.db.worm_append(WormEvent { - event_type: "CELL_DESTROYED", - virtual_key_id: self.virtual_key.id.clone(), - exit_reason: "ttl_expired", - tokens_used: self.inference.tokens_used(), - timestamp: Utc::now(), - }).await?; - - self.coordinator.release_lease(&self.id).await?; - self.db.close().await?; // LTX replication completes before close returns - Ok(()) - } -} -``` - -Idempotent cell naming mirrors Streams / celld: `agent:{subscriptionId}:{eventId}` — at-most-one writer per cell name on replay. - ---- - -## 5. WASM capability model - -### 5.1 WIT world definition - -The WASM component (`clawql-core.wasm`) declares host capabilities via WIT. cellrt grants only what is declared. Undeclared capabilities are **structurally absent** (not linked), not merely blocked at runtime. - -```text -// clawql-core.wit -world clawql-core { - // Network — fetch only, no raw TCP - import wasi:http/outgoing-handler@0.2.0 - - // Storage — cell SQLite only, no filesystem - import clawql:storage/cell-storage - - // Crypto — subset of Web Crypto - import clawql:crypto/digest // SHA-256/384/512 - import clawql:crypto/hmac // HMAC sign/verify - import clawql:crypto/random // randomUUID, getRandomValues - import clawql:crypto/aes-gcm // AES-GCM encrypt/decrypt - - // Node polyfills (from @clawql/wasm-polyfills) - import clawql:polyfills/async-local-storage - import clawql:polyfills/event-emitter - import clawql:polyfills/buffer - import clawql:polyfills/node-crypto // subset — maps to clawql:crypto/* - - // Inference — model calls via virtual key - import clawql:inference/call // model-escalated, budget-enforced - - // Audit — WORM writes via host (not direct SQLite) - import clawql:audit/worm-append - - // Exports — host → component - export clawql:tools/call-tool - export clawql:tools/list-tools - export clawql:mcp/handle-request - export clawql:mcp/handle-websocket -} -``` - -### 5.2 Capability enforcer - -At WASM instantiation, cellrt validates imports against allowed capabilities and builds a linker with **only** granted host imports. A denied import fails instantiation with `CapabilityDenied` — the component never runs. - -### 5.3 What the WASM component cannot do - -Structurally absent: - -- Raw TCP/UDP sockets -- Filesystem access (`node:fs`, WASI filesystem) -- Process spawning (`node:child_process`) -- Shared memory across cells -- Direct SQLite access (must use `clawql:storage/cell-storage`) -- Direct model API calls (must use `clawql:inference/call` with virtual key enforcement) -- WORM writes without audit trail (must use `clawql:audit/worm-append`) - ---- - -## 6. Virtual key lifecycle in Rust - -```rust -#[derive(Clone, Debug)] -pub struct VirtualKey { - pub id: Uuid, - pub cell_id: CellId, - pub budget_tokens: u32, - pub tokens_used: Arc, - pub expires_at: DateTime, - pub state: Arc>, -} - -#[derive(Debug, PartialEq)] -pub enum VirtualKeyState { - Active, - BudgetExhausted, - Expired, - Revoked, -} -``` - -- Issued on cell spawn, scoped to `CellId` (`agent:{subscriptionId}:{eventId}`). -- Budget checked before every inference call; exhaustion is a one-way state transition. -- `Drop` on `CellHandle` expires the key even on panic paths (best-effort async expire). -- Alarm path also expires the key and flushes RTP/OBT training data (Streams §7). - -The type system enforces one-way lifecycle: `Active` → `BudgetExhausted` | `Expired` | `Revoked`. A leaked key from a destroyed cell is already expired at the inference gateway. - ---- - -## 7. LTX replication and WORM - -Every SQLite write is a WORM write because LTX replication acknowledges only after the WAL segment is durable in the bucket (**RPO=0**). - -```text -storage.put / worm_append - │ - ▼ -SQLite WAL frame - │ - ▼ -LTX segment → cells/{cell_id}/{txn_id}.ltx (bucket ACK) - │ - ▼ -caller receives Ok(()) // not before bucket ACK -``` - -An auditor reconstructs a cell's history from LTX segments with `sqlite3` — no live system access required. Recommended lifecycle: move agent cell LTX to cold storage after 90 days; retain indefinitely for regulated deployments. - ---- - -## 8. Security layer - -### 8.1 eBPF monitoring (Linux) - -cellrt embeds a Falco-equivalent rules engine via `libbpf-rs`. Production requires Linux kernel ≥ 5.8. On macOS (development), the eBPF layer is a no-op stub — **cellrt on macOS is not production-equivalent**. - -Example attach points: `sys_enter_execve`, `sys_enter_connect`, `sys_enter_openat`. Unexpected exec / egress produces `SecurityAlert` events into the observability pipeline. - -### 8.2 Cosign binary attestation - -On startup, cellrt verifies its own Cosign/Sigstore attestation. A tampered or unsigned binary fails to start (Layer 0 supply-chain guarantee applied to the runtime itself). - -### 8.3 Peer network - -Same posture as celld: peer protocol is HMAC-authenticated plain HTTP. Run peers on a private network or WireGuard/Tailscale; terminate TLS at ingress (nginx/Istio). Scope bucket credentials to the fleet bucket only. - ---- - -## 9. Fleet coordination - -### 9.1 Node discovery via bucket - -No membership list. No control plane. Nodes write/renew leases under `nodes/{node_id}` in the shared bucket. Peers with unexpired leases are reachable peers. - -### 9.2 Cell ownership (compare-and-swap) - -Conditional put on `leases/{cell_id}` (S3 `If-None-Match: *` / R2 equivalent). Lease TTL ~30s with renewal. On node death, another node acquires the lease, rebuilds SQLite from LTX segments, and resumes. - -Adding a node: point it at the same bucket. No join command. No membership list. - ---- - -## 10. Effect-TS → WASM build path - -ClawQL core is Effect-TS. Solving Effect → WASM is an ecosystem contribution, not a ClawQL-only fork. - -### 10.1 Prerequisites (planned packages) - -**`@clawql/wasm-polyfills`** — WASI 0.2 host imports for Node APIs Effect needs: `async_hooks` (AsyncLocalStorage), `buffer`, `events`, `stream`, `crypto` subset. - -**`@clawql/effect-wasm`** — Effect scheduler shim for non-Node runtimes (`WasmScheduler`, `WasmRuntime`, `WasmSafe` type that excludes Node I/O for safe `runSync` inside WASM). - -**Hardest risk:** Effect fiber scheduler internals. Use [`codegraph`](../plugins/codegraph.md) to map `Effect.runFork` → leaf Node APIs (`process.nextTick`, `queueMicrotask`, `AsyncLocalStorage`) before writing the shim. Open an Effect-team issue for a scheduler hook point before patching internals. - -### 10.2 Build pipeline - -```bash -# 1. Bundle with polyfill aliases (provider set compile-time constant — no dynamic import) -CLAWQL_PROVIDER=legal \ -esbuild packages/clawql-core/src/index.ts \ - --bundle --platform=browser --target=es2022 \ - --alias:node:async_hooks=@clawql/wasm-polyfills/async-hooks \ - --alias:node:crypto=@clawql/wasm-polyfills/crypto \ - --outfile=dist/clawql-core.bundle.js - -# 2. Componentize -jco componentize dist/clawql-core.bundle.js \ - --wit clawql-core.wit --world clawql-core \ - --out dist/clawql-core.wasm - -# Must stay under 64 MiB target (CI gate) -wc -c dist/clawql-core.wasm -``` - -### 10.3 Bootstrap path (before WASM) - -```rust -pub enum WasmMode { - Http { endpoint: Url, auth: BearerToken }, // → local clawql-mcp - Wasm { store: Store, instance: Instance }, -} -``` - -Mode is **auto-detected**: if `clawql-core.wasm` is absent, HTTP mode enables. No operator flag required. - ---- - -## 11. Deployment - -### 11.1 Single binary - -```bash -cargo build --release --target x86_64-unknown-linux-musl -# Static binary; target ~50–80 MB (Wasmtime ~20 MB + component ~15 MB) - -cosign verify-blob \ - --certificate-identity-regexp ".*clawql-cellrt.*" \ - --certificate-oidc-issuer https://token.actions.githubusercontent.com \ - --signature clawql-cellrt.sig \ - clawql-cellrt -``` - -### 11.2 Start a fleet node - -```bash -export CELLRT_BUCKET=s3://clawql-streams-state -export CELLRT_S3_ENDPOINT=https://${CF_ACCOUNT_ID}.r2.cloudflarestorage.com -export CELLRT_ADVERTISE=cellrt-node-a.internal:8080 -export CELLRT_LISTEN=0.0.0.0:8080 -export VAULT_ADDR=https://vault.internal:8200 -export VAULT_ROLE_ID=${VAULT_ROLE_ID} -export VAULT_SECRET_ID=${VAULT_SECRET_ID} -export CLAWQL_INFERENCE_ENDPOINT=http://clawql-inference.internal:8080 - -clawql-cellrt start -``` - -### 11.3 Deploy WASM bundle / diagnose - -```bash -npm run build:wasm -w clawql-core -clawql-cellrt deploy dist/clawql-core.wasm --bucket "$CELLRT_BUCKET" --endpoint "$CELLRT_S3_ENDPOINT" - -clawql-cellrt diagnose --bucket "$CELLRT_BUCKET" --endpoint "$CELLRT_S3_ENDPOINT" -# Reports: nodes, cells/node, LTX lag, virtual keys, Vault leases, eBPF status, attestation -``` - -### 11.4 Helm values (additions) - -```yaml -cellrt: - enabled: false - image: ghcr.io/danielsmithdevelopment/clawql-cellrt:latest - replicas: 2 - bucket: clawql-streams-state - vault: - enabled: true - addr: "" - inference: - endpoint: "" - security: - ebpf: true # Linux only — disable for macOS/dev - attestation: true # Cosign binary verification on startup - tee: - enabled: false # AMD SEV-SNP / Intel TDX — see clawql-tee.md - substrate: sev-snp # sev-snp | tdx | nitro - attestationGatedVault: false - airgapAudit: - enabled: false # see clawql-tee-airgap-audit.md - observability: - otel: - enabled: true - endpoint: "" - langfuse: - enabled: false - prometheus: - enabled: true - port: 9090 - wasmMode: http # http (bootstrap) | wasm (full) -``` - -CLI surface under Streams: `clawql streams cellrt start|deploy|diagnose|scale|audit export` (alongside existing `clawql streams celld …`). - ---- - -## 12. Comparison - -| | celld | clawql-cellrt | -| ---------------------- | ------------------------------ | ---------------------------------------------------------- | -| **Runtime** | V8 (Workers/DO JS API) | Wasmtime (Rust host) | -| **Language** | JavaScript / TypeScript | Rust + WASM component | -| **Security** | Alpha; no hostile multi-tenant | Rust memory safety + eBPF + WASM sandbox | -| **Vault** | External sidecar | Embedded dynamic secret injection | -| **Inference** | External HTTP | Embedded model escalation + virtual keys | -| **Observability** | External | Embedded OTel + Langfuse + Prometheus | -| **Binary attestation** | Upstream GH attestation | Cosign verify on startup | -| **Hardware TEE** | No | Planned — [`clawql-tee`](./clawql-tee.md) (SEV-SNP / TDX) | -| **Air-gap audit** | No | Planned — [`QR transport`](./clawql-tee-airgap-audit.md) | -| **Capability model** | Isolate ambient APIs | WIT — explicit capability grants | -| **Bootstrap** | N/A | HTTP → clawql-mcp (ships immediately) | -| **Full path** | JS bundle in V8 | `clawql-core.wasm` in-process | -| **Repo** | denoland/celld | ClawQL monorepo `crates/clawql-cellrt/` | -| **Coordination** | S3 bucket | S3 bucket (same pattern; extractable `bucket-coordinator`) | -| **LTX / WORM** | Yes | Yes | -| **License** | Apache 2.0 | Apache 2.0 | - -### Three deployment modes - -| Mode | Mechanism | Best for | -| ---- | ------------------------------------------- | ------------------------------------- | -| A | Cloudflare Workers (existing DO code path) | Hosted SaaS | -| B | **cellrt** self-hosted (bucket coordinator) | Sovereign / security-first production | -| C | K8s HPA on NATS lag | Regulated / air-gapped; no DO runtime | - -celld remains available as Mode B' for operators who want Workers API parity on self-hosted hardware while cellrt matures. - ---- - -## 13. Build sequence - -| Week | Focus | Exit criteria | -| ---- | ----------------------------------------------------------------- | --------------------------------------------------------- | -| 1 | Coordination: leases, LTX, peer HMAC | Multi-node acquire/fail/recover tests green | -| 2 | Cell runtime HTTP bootstrap + Vault + virtual keys | Spawn cell → tool via clawql-mcp → WORM in bucket | -| 3 | Security: Cosign, eBPF (Linux), capability enforcer stub | Tampered binary rejected; denied import fails instantiate | -| 4 | Observability + CLI + Helm | `diagnose`, `/metrics`, Langfuse opt-in | -| 5–6 | `@clawql/wasm-polyfills` | Standalone npm; polyfill surface tests | -| 7 | `@clawql/effect-wasm` + Effect-team scheduler hook issue | Minimal fiber schedule works in Wasmtime | -| 8 | clawql-core WASM build (`cache`, `audit` first) | Valid component < 64 MiB | -| 9 | Wasmtime integration (replace HTTP for ported tools) | In-process tool calls + WORM correct | -| 10 | Hardening, Wasmtime vs WasmEdge bench, C&H B-7.1 smoke via cellrt | Production readiness checklist | - -Shipable surface at **week 4** (HTTP bootstrap). Full Wasmtime path at **week 10**. - -**TEE track (after week 4 bootstrap):** `cellrt-attestation` + Vault attestation auth → SEV-SNP demo → optional GPU CC → air-gap QR export. See [`clawql-tee.md`](./clawql-tee.md) § build sequence. - ---- - -## 14. Open questions - -1. **Wasmtime vs WasmEdge.** Prefer Wasmtime (Bytecode Alliance, component model maturity). Re-benchmark WasmEdge in week 10. -2. **Effect scheduler shim correctness.** Highest technical risk. Open Effect-team issue in week 7 _before_ relying on internal patches. Use codegraph for Node-API blast radius first. -3. **eBPF on non-Linux.** macOS/dev is stub-only; document in Helm and PICERL that production security monitoring requires Linux. -4. **Bundle size at full tool surface.** ComponentizeJS embeds SpiderMonkey (~7 MB). Trim via `CLAWQL_PROVIDER=` subsets; CI fails above 64 MiB. -5. **Cloudflare Workers adapter for the same WASM component.** Verify wrangler / Workers component-model support for the WIT world before locking host import names. -6. **Relationship to celld in Helm defaults.** Until cellrt ships, `streams.scalingBackend` remains `kubernetes` \| `celld` \| `cloudflare`. Add `cellrt` when week-4 bootstrap lands. -7. **`bucket-coordinator` extract timing.** When to publish the coordination layer to crates.io vs keep it private to the cellrt workspace. -8. **TEE substrate default.** Prefer AMD SEV-SNP for sovereign root-of-trust; keep Nitro as simplest demo path. Confirm first customer hardware. - ---- - -## Further reading - -- [`docs/streams/clawql-streams.md`](./clawql-streams.md) — Streams Specification v0.2 -- [`docs/streams/clawql-celld.md`](./clawql-celld.md) — Workers/DO-compatible self-hosted path -- [`docs/streams/clawql-tee.md`](./clawql-tee.md) — hardware TEE + attestation-gated secrets -- [`docs/streams/clawql-tee-airgap-audit.md`](./clawql-tee-airgap-audit.md) — QR air-gap audit transport -- [`docs/streams/clawql-durable-objects.md`](./clawql-durable-objects.md) — session / sidecar / virtual key contract -- [`docs/inference/clawql-inference.md`](../inference/clawql-inference.md) — model escalation, virtual keys, call store -- [`docs/mcp/mcp-api-adapter.md`](../mcp/mcp-api-adapter.md) — six protocol surfaces -- [`docs/plugins/codegraph.md`](../plugins/codegraph.md) — Effect scheduler feasibility / blast radius -- [`docs/security/clawql-security-defense-in-depth.md`](../security/clawql-security-defense-in-depth.md) — security positioning -- [celld](https://celld.dev/) · [Bytecode Alliance Component Model](https://component-model.bytecodealliance.org/) · [Wasmtime](https://wasmtime.dev/) - ---- - -_clawql-cellrt · Specification v0.1 · August 2026 · Draft_ -_Companion: ClawQL Streams Spec v0.2 · ClawQL Celld Integration Spec · clawql-tee_ -_Planned crate path: `crates/clawql-cellrt` (ClawQL monorepo)_ +An earlier draft of this page specified a Rust + Wasmtime `clawql-cellrt` binary (~50–80 MB target) in-repo under `crates/clawql-cellrt/`. That plan is cancelled. Do not scaffold the crate; do not cite cellrt as a shipping path. From 7f8a06d1f7c77ee3e87092206b5f1599b26b72ba Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Fri, 23 Oct 2026 05:59:40 +0000 Subject: [PATCH 2/2] style: apply Prettier [prettier-autofix] --- ...0011-isolation-agent-substrate-sandbox-celld.md | 12 ++++++------ docs/adr/0016-rust-dataplane-spike.md | 14 +++++++------- docs/streams/clawql-cellrt.md | 8 ++++---- 3 files changed, 17 insertions(+), 17 deletions(-) diff --git a/docs/adr/0011-isolation-agent-substrate-sandbox-celld.md b/docs/adr/0011-isolation-agent-substrate-sandbox-celld.md index 7fd50b0a6..a5ccfeda6 100644 --- a/docs/adr/0011-isolation-agent-substrate-sandbox-celld.md +++ b/docs/adr/0011-isolation-agent-substrate-sandbox-celld.md @@ -92,12 +92,12 @@ As of this writing, Agent Substrate is open source and generally available for * ## 6. Implementation map -| Artifact | Path | -| ------------------- | --------------------------------------------------------------------------------------------------- | -| This ADR | `docs/adr/0011-isolation-agent-substrate-sandbox-celld.md` | -| Backend | `packages/clawql-sandbox/src/agent-substrate/` | -| Decision rule | `packages/clawql-sandbox/src/isolation-decision.ts` | -| celld note | `docs/streams/clawql-celld.md` (isolation rule); `docs/streams/clawql-cellrt.md` (withdrawn) | +| Artifact | Path | +| ------------- | -------------------------------------------------------------------------------------------- | +| This ADR | `docs/adr/0011-isolation-agent-substrate-sandbox-celld.md` | +| Backend | `packages/clawql-sandbox/src/agent-substrate/` | +| Decision rule | `packages/clawql-sandbox/src/isolation-decision.ts` | +| celld note | `docs/streams/clawql-celld.md` (isolation rule); `docs/streams/clawql-cellrt.md` (withdrawn) | --- diff --git a/docs/adr/0016-rust-dataplane-spike.md b/docs/adr/0016-rust-dataplane-spike.md index b4fc2e38a..6efcc55e9 100644 --- a/docs/adr/0016-rust-dataplane-spike.md +++ b/docs/adr/0016-rust-dataplane-spike.md @@ -21,13 +21,13 @@ ClawQL’s lasting formal stack remains **TLA+** (protocols), **Lean** (policy o ### Evidence that drove no-go -| Evidence | Result | -| --- | --- | -| Component plane (direct MCP → Rust) | Governed CF known-op ~**15.8 MB** vs Bun ~**128 MB** — looks like a large density win **if** you ignore the Bun host | -| Product path (Bun → Rust forward, e2e) | Summed Anonymous RSS ~**124.8 MB** vs Bun-only ~**124.4 MB** — **tied**; dataplane-only RSS is not a product cite | -| Latency (e2e) | Forward hop costs session p50 (~**21 ms** dual vs ~**13 ms** Bun-only) and worsens call p999 | -| Peers | MCPJungle / agentgateway still ~**99–102 MB** — dual-process does not take memory leadership | -| Ops | Two processes, catalog/version skew, claim complexity — not justified by e2e numbers | +| Evidence | Result | +| -------------------------------------- | -------------------------------------------------------------------------------------------------------------------- | +| Component plane (direct MCP → Rust) | Governed CF known-op ~**15.8 MB** vs Bun ~**128 MB** — looks like a large density win **if** you ignore the Bun host | +| Product path (Bun → Rust forward, e2e) | Summed Anonymous RSS ~**124.8 MB** vs Bun-only ~**124.4 MB** — **tied**; dataplane-only RSS is not a product cite | +| Latency (e2e) | Forward hop costs session p50 (~**21 ms** dual vs ~**13 ms** Bun-only) and worsens call p999 | +| Peers | MCPJungle / agentgateway still ~**99–102 MB** — dual-process does not take memory leadership | +| Ops | Two processes, catalog/version skew, claim complexity — not justified by e2e numbers | Spike branches measured the stack; they are **not** to be merged. Production remains single-process Bun (or celld for the isolate path). diff --git a/docs/streams/clawql-cellrt.md b/docs/streams/clawql-cellrt.md index 756303cdd..972ba93c8 100644 --- a/docs/streams/clawql-cellrt.md +++ b/docs/streams/clawql-cellrt.md @@ -7,11 +7,11 @@ ClawQL will **not** build an owned Rust/Wasmtime cell runtime (`crates/clawql-cellrt`). -| Layer | Owner | -| --- | --- | +| Layer | Owner | +| ----------------------------------------------------- | -------------------------------------------------------------------------- | | Host MCP (search, execute, plugins, memory, OAuth, …) | **TypeScript + Effect TS v4** on **Bun** (default); Node for compatibility | -| Durable isolate / Streams / ProgramCellDO | **celld** (self-hosted Durable Objects–compatible runtime) | -| Formal methods | **TLA+** + **Lean** + **gdp-ts** — not Verus/Rust | +| Durable isolate / Streams / ProgramCellDO | **celld** (self-hosted Durable Objects–compatible runtime) | +| Formal methods | **TLA+** + **Lean** + **gdp-ts** — not Verus/Rust | ADR 0016 rejected a Rust execute data plane after dual-process e2e boards showed **no product memory win** (summed Bun+dataplane ≈ Bun-only) and a latency cost. The same product stance applies here: do not introduce a Rust toolchain or `crates/` tree into ClawQL.