§20. Later phases — design notes carried forward

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

Not Phase A work; kept so the design is not lost.

Model service (B). The model is treated as an adversary: its judgement is never trusted and is not a vector, because any proposal it can make is one an attacker with the same socket could make, and every proposal passes the same checks. What must hold is containment (I9). Until I9 is proved in E, it is held by the unit’s sandbox, which is normative: DynamicUser=; no capabilities; ProtectSystem=strict, ProtectHome=yes, PrivateTmp=yes, read-only access to the model files and the report socket; RestrictAddressFamilies=AF_UNIX, widened only for a declared remote endpoint (future-work §3); a SystemCallFilter= allowlist; device access limited to the GPU’s render node when GPU inference is enabled; the proposal socket as its only write path. Gym case (B): from inside the service, attempt every other write path (the journal, the override file, the store, another unit’s socket, a capability-changing syscall); each fails and none leaves a trace outside the service. Unprivileged systemd service; reads reports over a Unix socket; emits Proposals. Boot model ~4B at 4-bit on CPU via mistral.rs or candle; RAM floor 8 GB. Residency is declared like any other unit: unit:model-service desired Resident when All[Not(Foreground), memory free ≥ model size + headroom], otherwise Unloaded. Loads lazily when an incident escalates to it (zero steady-state memory; 5–15 s cold start); unloads after a declared idle period (default 10 min) and immediately on GPU or memory pressure from any foreground principal: the user’s session always outranks agent inference. If an escalation arrives while loading is not allowed, it falls back in order to the deterministic path, CPU inference where available outside quiet mode, a configured remote endpoint (future-work §3) within its disclosure profile, or deferral until the condition clears. It never loads over a foreground app. keep_warm offered at ≥ 16 GB outside quiet mode. Summoned only on DiagnoserExhausted or intent < 0.5. Tools: inventory, health report (including attempts and the incident), dependency graph, config read, local manual search, ask-user, propose (cataloged changes or new catalog entries for human review; never raw Nix). All text inputs tagged untrusted. Training: distillation in the gym, scored on diagnoser-failed and held-out faults. Model planner: largest catalog model that fits measured resources; installed as a Tested generation; switched only if it beats the currently active model on repair accuracy; falls back to the boot model on resource loss. Catalog models hash-pinned with training manifest and eval results.

Approval broker and secure attention (C, E). Separate process minting ApprovalTokens for any principal holding approval capability (§11), never for its own proposals. C: its own socket and a confirmation surface the compositor cannot draw over. E: a kernel-intercepted secure attention key hands the display to the broker.

Remote principals, apps, fleets (future). The endpoint catalog and relay for remote agents, app capability manifests, fleet membership (Raft and BFT behind one interface, BFT the intended default), attestation, and gossip of shared knowledge are directions in docs/future-work.md §3–§5. The hooks in §9 (signed external desired state) and §10 (signed health report), and the reserved Actor::Agent, exist so they can arrive without reopening the proven crates.

Rust system layer (D). Snix (git.snix.dev/snix/snix; crates GPL-3.0, protobuf definitions MIT) as the GenerationBackend, spoken to over its MIT protocols from a separate process. Rust PID 1 plus supervisor as UnitBackend, driven by Requires edges with Wants preserved as weak. Rust CoW filesystem as SnapshotBackend. relibc for Rust std (vendors openlibm, C; a named exception). Store integrity is proven for content-addressed paths and signature-and-NAR-hash-checked for input-addressed ones. Backend contracts are revised at the start of D from docs/assumptions.md and docs/deviations.md.

Asterinas (E). Fork at a pinned release (0.19.0 at writing). Driver priority for a reference laptop: NVMe, input, display → Wi-Fi, Ethernet, USB → audio, power, suspend → GPU modesetting → GPU 3D/compute (port Nova or Tyr) → Bluetooth, webcam, fingerprint. Firmware blobs allowed. Desktop: Smithay compositor with Rust software renderer; iced UI; COSMIC later. Verification: OSTD (vostd), executor, policy, diagnoser, broker, switch/rollback, store integrity, model channel, core update path. Core image: signed bundle installed only with project signature plus secure attention; previous core stays bootable.

Trust base accepted as unproven at every phase: firmware, bootloader, Rust compiler, CPU; plus the Linux kernel and systemd in A–D.