Whitepaper Outline

Section-by-section sketch of the capOS whitepaper. Each section lists its supporting docs and its evidence dependency on evidence-gaps.md. The actual draft now lives at papers/schema-as-abi/main.typ; this file is the structural reference and stays in docs/paper/ alongside the plan and evidence-gap tracker. When a section’s evidence lands, update the draft in the same task that updates this outline and evidence-gaps.md.

§1. Introduction

• Problem: kernel ABIs are typically C-header syscall conventions plus a separate rights/permission machinery; capability OSes typically still keep rights, IPC, and serialization as three layers.
• Thesis (one paragraph): schema-as-ABI collapses these layers.
• Contributions list. Map each contribution to a paper section and to a Tier-1 artifact in evidence-gaps.md.

Backed by: docs/overview.md, docs/capability-model.md.

§2. Background and Related Work

• seL4: untyped IPC, kernel-managed rights, formal verification. Source: docs/research/sel4.md.
• Zircon: typed kernel objects, fixed syscalls. Source: docs/research/ (Zircon notes).
• EROS / CapROS: persistent capabilities without schema-as-wire.
• Genode: component-typed RPC over kernel IPC primitives. Source: docs/research/genode.md.
• Plan 9: universal-interface as file I/O.
• capnp-rpc: prior art for schema-driven RPC; capOS pulls this layer into the kernel boundary.
• LLVM/target customization: relevant for the userspace runtime story.

Backed by: docs/research.md and docs/research/*.

§3. Capability Model

• Typed schema = permission. No parallel rights bitmask.
• Narrowing via wrapper capabilities, not flag reduction.
• Generation tags, copy/move semantics, release ABI.
• Service objects vs. badged endpoints (the badge migration).

Backed by: docs/capability-model.md, docs/proposals/service-object-capabilities-proposal.md, docs/architecture/capability-ring.md, docs/authority-accounting-transfer-design.md.

Evidence dependency: claim C1 in evidence-gaps.md.

§4. Ring Transport

• SQ/CQ shared-memory ring as the only kernel boundary.
• cap_enter semantics: flush pending SQEs, wait for completions or timeout.
• Opcode set: CALL, RECV, RETURN, RELEASE, NOP. Reserved Finish.
• Direct-switch IPC handoff.
• Transport errors and CQE error model.
• Loom protocol model.
• Backpressure, fairness, scheduler-tick polling rules.

Backed by: docs/architecture/capability-ring.md, docs/architecture/ipc-endpoints.md, code in kernel/src/cap/ring.rs, capos-config/tests/ring_loom.rs, capos-rt/src/ring.rs.

Evidence dependency: C2.

§5. Capability Lifecycle

• Copy, move, release.
• Revocation: epoch model, Revocable Read proof.
• Resource accounting: per-process ledger, exactly-once transfer rollback.
• Service objects replacing badges.

Backed by: docs/authority-accounting-transfer-design.md, docs/proposals/service-object-capabilities-proposal.md, docs/backlog/stage-6-capability-semantics.md.

Evidence dependency: C1.

§6. System Composition

• Manifest-driven boot, init service graph.
• Authority broker, sessions, anonymous/operator/SSH-public-key paths.
• Demo services: First Chat, Adventure, SSH Shell Gateway as the end-to-end auth/identity boundary.

Backed by: docs/architecture/manifest-startup.md, docs/proposals/service-architecture-proposal.md, docs/proposals/user-identity-and-policy-proposal.md, docs/proposals/ssh-shell-proposal.md, docs/security/trust-boundaries.md.

Evidence dependency: C2 plus completion of selected SSH milestone.

§7. Verification and Engineering Process

• Kani / Loom / Miri / panic-surface inventory: scope, bounds, gaps.
• Dependency policy, pinned trusted inputs.
• Workplan / review discipline as part of the methodology.
• Collaboration methodology: dedicated worktrees per task, mandatory gates, REVIEW_FINDINGS as durable open-issue tracking, merge-back-to-main rule.

Backed by: docs/proposals/security-and-verification-proposal.md, docs/security/verification-workflow.md, docs/panic-surface-inventory.md, docs/trusted-build-inputs.md, REVIEW.md, REVIEW_FINDINGS.md, WORKPLAN.md.

Evidence dependency: C5.

§8. Evaluation

• cap_enter round-trip latency.
• Ring throughput.
• Endpoint IPC: scheduler path vs. direct-switch.
• Schema dispatch vs. NullCap baseline.
• Memory cost per capability slot.
• Persistence proof-of-concept: round-trip integrity.
• Network-transparency proof-of-concept: cross-instance call latency.

Evidence dependency: C2, C3, C4. All three artifacts are currently missing or partial; do not begin drafting this section until they exist.

§9. Limitations

Honest framing, written before §1 is tightened. Likely items:

• Single architecture (x86_64). aarch64 deferred.
• Partial SMP at time of writing; reflect actual state.
• Persistence and network-transparency demonstrated as proofs-of-concept, not production subsystems.
• Verification scoped to listed invariants; not whole-kernel.
• No production hardware path; QEMU-only artifact.

§10. Future Work

Reference docs/roadmap.md Future Tracks rather than restating them. Topics: aarch64, GPU, live upgrade, persistence-at-scale, formal MAC/MIC, Go/WASI, cloud metadata, federated multi-instance demos.

§11. Collaboration Methodology Note

Short standalone section.

• Workflow: per-task worktrees, mandatory verification gates, REVIEW.md conventions, REVIEW_FINDINGS.md as durable open-issue tracking, merge-back-to-main discipline.
• What this enabled: surfacing review and merge hygiene against changing publication assumptions while keeping evidence-driven sequencing intact.
• Reproducibility kit: pinned toolchains, ISO build, QEMU smoke targets.

§12. Conclusion

To be written last, after §8 numbers exist.

Appendices (candidate)

• A. Schema excerpt for one representative capability with method-by-method ABI commentary.
• B. Reproducibility kit: exact commands, pinned commits, expected outputs.
• C. Build/boot flow diagram.
• D. Process model diagram.