diff --git a/docs/astrid-ai-native-os-workplan.md b/docs/astrid-ai-native-os-workplan.md index 9d8ca81a4..733ecd19c 100644 --- a/docs/astrid-ai-native-os-workplan.md +++ b/docs/astrid-ai-native-os-workplan.md @@ -156,8 +156,12 @@ not become a ring-0 ABI. - [x] Record ADRs for protection domains, capability object representation, handle transfer, revocation, fault endpoints, scheduling, and audit ordering: [Astrid Kernel Architecture Decision Records](astrid-kernel-adrs.md). -- [ ] Define the support-policy vocabulary: experimental machine, supported host, - supported capsule contract, verified claim, and known residual risk. +- [x] Define the support-policy vocabulary: experimental machine, supported host, + supported capsule contract, verified claim, and known residual risk: + [Astrid Kernel Support-Policy Vocabulary](astrid-kernel-support-policy.md). +- [x] Sketch the version-zero native ABI with no path, no stringly syscall, and no + ambient-authority handle (the charter's Milestone 0 exit gate): + [Astrid Kernel v0 ABI Sketch](astrid-kernel-abi-sketch.md). Exit condition: every security or compatibility claim names its enforcing component and planned evidence. No guarantee depends on “the architecture should prevent it.” diff --git a/docs/astrid-kernel-abi-sketch.md b/docs/astrid-kernel-abi-sketch.md new file mode 100644 index 000000000..f41238e15 --- /dev/null +++ b/docs/astrid-kernel-abi-sketch.md @@ -0,0 +1,255 @@ +# Astrid Kernel v0 ABI Sketch + +Status: Milestone 0 exit artifact; the version-zero native ABI shape, not a stable contract + +Last reviewed: 2026-07-21 + +Companions: [kernel charter](astrid-kernel-charter.md), +[ADRs](astrid-kernel-adrs.md), +[requirement-to-evidence matrix](astrid-kernel-evidence-matrix.md), +[native-kernel scope](astrid-native-kernel.md) + +This is the version-zero sketch of the native ABI between ring 0 and a +ring-3 domain. It is the last Milestone 0 exit artifact, and the charter sets +its acceptance bar directly: the sketch must have "no path, no stringly +syscall, and no ambient-authority handle" (charter §2, exit gate). It exists +to prove the seven ADRs compose into a coherent, capability-oriented, +non-POSIX operation set before any of it is implemented. + +**This is a sketch, not a contract.** The native ABI is private and versioned +(charter §4.1); it is explicitly *not* a supported capsule contract (support +policy). Capsules target `wasm32-unknown-unknown` and the `astrid:*` WIT +worlds; the runtime host translates those into these operations. Nothing here +is a stable interface, and every signature will move during implementation. +What must *not* move is the shape: capability-oriented, totally fallible, +bounded, path-free, string-subject-free, ambient-free. + +## Reading the sketch + +Types are written in a neutral pseudo-IDL, pointer-width explicit, `no_std` +and fuzzable by construction (charter §4.6). The conventions: + +- `Cap` — a capability, named only by a per-domain table **slot index** + (`u32`), never a pointer or a string (ADR-K2). Every `Cap` argument is a + slot; the kernel resolves slot → entry → generation-checked object. +- `Rights` — a bitmask; operations that derive a capability take a requested + mask and the result is `requested ∩ source` (ADR-K3), never wider. +- `Result` — every operation is total: it returns `Ok(T)` or a typed + `Fault`; there is no undefined argument space and no panic (charter §4.3; + REQ-ABI-1). +- Bounded — every length, count, and buffer has a declared compile-time + ceiling charged to the caller's budget (charter §4.4; REQ-ABI-4). `&[u8]` + in a signature means "bounded slice with a stated max," never unbounded. +- All multi-field inputs are copied and validated once at the boundary + (charter §4.6; REQ-ABI-2). + +Handles carry a generation (ADR-K2); a stale generation faults before any +state changes. Nothing in the ABI takes an address, a path, a name, or a +topic string as an authority-bearing argument. + +## Object and fault types + +``` +Domain // a protection domain (ADR-K1) +CapTable // a domain's capability table (ADR-K2), addressed by slot +SchedContext // CPU budget+period as a capability (ADR-K6) +FaultEndpoint // one per domain, birth-reserved death slot (ADR-K5) +MemRegion // a bounded, W^X-typed physical/virtual region +Endpoint // a bounded typed IPC rendezvous/queue object +DeviceObj // a kernel-discovered device claim (driver contract) +DmaBuffer // a broker-owned bounded DMA buffer (TM §6) +AuditRoot // the monotonic order + hash accumulator (ADR-K7) + +Fault { // the typed failure of any operation + kind: enum { BadSlot, StaleGeneration, RightsExceeded, OutOfRange, + PoolExhausted, WouldWiden, Unbounded, NotPermitted, Busy }, + detail: u64 // operation-specific, never a pointer or string +} + +DeathRecord { // delivered exactly once to a FaultEndpoint (ADR-K5) + domain: DomainId, + cause: enum { Trap, PageFault, BudgetExhausted, Killed, Revoked }, + final_accounting: Accounting, + generation: u64 +} +``` + +## Operation families + +The families follow the scope document's minimal ABI (scope §2.2), refined by +the ADRs and extended with the legibility family the charter requires from v0. + +### Domain (ADR-K1) + +``` +domain_create(image: Cap, plan_slot: u32, rights: Rights) -> Result +domain_start(d: Cap) -> Result<()> +domain_stop(d: Cap) -> Result<()> +domain_inspect(d: Cap) -> Result // read-only projection +domain_destroy(d: Cap) -> Result<()> // → revocation (ADR-K4) +``` + +`domain_create` mints a domain only within the authority the measured boot +plan derived to the caller (`plan_slot`); a manifest claim is never authority +(charter §2.10; REQ-CAP-4). No domain names another by string or index it was +not granted. + +### Memory (charter §3; ADR-K1) + +``` +mem_alloc(pool: Cap, class: MemClass) -> Result // fixed-slot (ADR-K1) +mem_map(d: Cap, region: Cap, rights: Rights) -> Result<()> // W^X enforced +mem_unmap(d: Cap, region: Cap) -> Result<()> +mem_share(region: Cap, to: Cap, rights: Rights) -> Result // ∩, never widen +``` + +`mem_map` faults with `WouldWiden` on any request for a write+execute mapping +(REQ-MEM-4). Allocation faults `PoolExhausted` per class, never fragmenting +(ADR-K1; REQ-MEM-1). + +### IPC (charter §4; ADR-K3) + +``` +ipc_endpoint_create(pool: Cap) -> Result +ipc_send(ep: Cap, msg: &Message, caps: &[Cap]) -> Result<()> // caps: bounded +ipc_recv(ep: Cap, buf: &mut Message) -> Result +ipc_call(ep: Cap, msg: &Message, caps: &[Cap]) -> Result +``` + +`caps` is the explicit, bounded set of capabilities transferred (ADR-K3): +each is derived into the receiver's table with `requested ∩ source` rights. +A capability the message does not name is not transferred. `Message` is a +bounded typed payload with a declared ceiling; there is no unbounded byte +stream and no path/topic string as a routing subject — routing is by +endpoint capability, not by name. + +### Wait and time (charter §3) + +``` +wait(on: &[WaitCap], deadline: Nanos) -> Result // on: bounded +yield_now() -> () +time_monotonic() -> Nanos +random_bytes(buf: &mut [u8]) -> Result<()> // buf: bounded +``` + +`wait` blocks on a bounded set of endpoints/timers/fault-endpoints until one +is ready or the deadline passes. Time is monotonic ring-0 time (ADR-K6's +budget accounting is separate and unforgeable). Entropy is a typed host +effect, matching the existing `astrid:sys` random source. + +### Scheduling (ADR-K6) + +``` +sched_context_create(pool: Cap, budget: Nanos, period: Nanos) -> Result +sched_bind(d: Cap, sc: Cap) -> Result<()> +sched_derive(sc: Cap, budget: Nanos, period: Nanos) -> Result // ≤ source +``` + +A domain runs only while bound to a scheduling context with budget +(ADR-K6). `sched_derive` produces a child context whose budget is never +larger than the source's — CPU attenuates on delegation exactly like every +other authority. Budget exhaustion raises `BudgetExhausted` to the domain's +fault endpoint. + +### Fault and supervision (ADR-K5) + +``` +fault_endpoint_create(pool: Cap, for_domain: Cap) -> Result +fault_recv(fe: Cap, buf: &mut DeathRecord) -> Result<()> +``` + +The death-record delivery slot is reserved from the recovery pool at +`domain_create` time and bound to the endpoint, so delivery never allocates +and never fails for want of capacity (ADR-K5; REQ-FAULT-5). A supervisor +holds the `fault_recv` capability; a domain never holds the fault authority +over itself (ADR-K4; REQ-FAULT-3). + +### Device and DMA (driver contract; TM §6) + +``` +device_claim(plan_slot: u32) -> Result // kernel-discovered only +device_queue(dev: Cap) -> Result // mediated queue +dma_buffer_alloc(pool: Cap, len: Bounded) -> Result // broker-owned +dma_map(dev: Cap, buf: Cap, dir: Direction) -> Result<()> // IOMMU-domain scoped +dma_unmap(dev: Cap, buf: Cap) -> Result<()> // strict invalidation +irq_wait(dev: Cap) -> Result<()> // deferred bottom half +``` + +Only kernel-discovered devices are claimable, and only within the boot plan +(TM §6). The v0 device surface is mediated queues and broker-owned DMA +buffers — no raw MMIO, no arbitrary physical address, no ATS-trusted +translation (TM §6; REQ-DMA-1..5). `dma_map` is scoped to the device's IOMMU +domain and mappings are minted only for broker-owned buffers, never live +kernel memory. + +### Trust and audit (ADR-K7) + +``` +audit_stamp(event: &AuditEvent) -> Result // monotonic total order +audit_root() -> Result // attested, never parsed +measure_verify(obj: Cap) -> Result +``` + +`audit_stamp` assigns a monotonic sequence and advances the hash accumulator; +ring 0 orders and roots but never interprets the record (charter §2; ADR-K7). +The user-space audit domain reads the ordered stream and builds the +BLAKE3-sealed, ed25519-signed chain. + +### Legibility (charter §3) — the AI-kernel family + +``` +legible_enumerate(rel: RelationKind) -> Result // domain-visible only +legible_subscribe(rel: RelationKind, sink: Cap) -> Result // bounded deltas +``` + +This is the family that makes the kernel the ground floor of the system +ontology (charter §3). `legible_enumerate` returns the caller-visible +projection of an object-table relation — domains, capabilities, endpoints, +scheduling contexts — as typed tuples read directly from the tables, never a +mirrored store (ADR-K2; REQ-LEG-1). `legible_subscribe` delivers bounded +deltas to a sink endpoint, in the Genode report/ROM shape (TM §10). Every +relation is capability-gated per relation and domain-visible only +(REQ-LEG-2); relations carrying timing-correlated counters are rate-limited +and quantized (REQ-LEG-3). This is an ABI family, not a debug channel: the +base relations a user-space reasoner reads as fact are emitted here because +they *are* ring 0's state. + +### Debug (charter §3; scope §2.2) + +``` +debug_write(buf: &[u8]) -> Result<()> // bounded; capability-gated or absent in production +``` + +Bounded boot diagnostics only, capability-gated, and absent in a production +image. It is never an authority path. + +## What is deliberately absent + +The absences are the proof the sketch meets its bar: + +- **No path or name** as an authority argument — every subject is a `Cap` + slot. There is no `open(path)`, no `connect(name)`, no `lookup(string)`. +- **No ambient handle** — nothing returns authority the caller did not derive + from a capability it already held or from the measured plan. +- **No POSIX** — no `fork`, `exec`, `signal`, file descriptor, user/group, or + environment. +- **No unbounded input** — every buffer, list, and count has a declared + ceiling. +- **No inference** — nothing here evaluates a model, a similarity, or a + nonzero-temperature operation; the legibility family emits facts, it does + not reason over them (charter §2 item 7). +- **No raw device authority** — no arbitrary MMIO, port I/O, physical + address, or unconstrained map (TM §6). +- **No dynamic kernel code** — no operation loads a module into ring 0. + +## From sketch to Milestone 1 + +The Milestone 1 skeleton (scope §9) implements the boot, allocator, +exception, and timer substrate beneath this ABI, exposing only the smallest +subset needed for the first vertical slice: `domain_create`/`start`, one +`mem_*`, one `ipc_*` pair, `wait`, `fault_recv`, and `debug_write`. The +device, DMA, and full legibility families arrive with their milestones (M6, +M3). Each operation lands with the evidence-matrix rows that falsify it, so +the ABI grows only as fast as its tests. This sketch is the shape those +signatures must keep; the charter's amendment procedure governs any change to +the shape, not merely to a signature.