# Whitepaper Evidence Gaps

Live tracking of which paper claims still lack artifact-level evidence and
which workplan slice will close each gap. Update this file in the same task
that closes a gap. When a gap closes, also update the corresponding `#todo`
block in the paper draft at `papers/schema-as-abi/main.typ`.


## Claim C1: Schema-typed methods replace parallel rights

**Status: partial.**

- [x] Capability dispatch via `CapObject` + capnp schema (kernel + capos-rt).
- [x] Authority narrowing via wrapper capabilities (no rights bitmask).
- [x] Stage 6 Gate 0: delegated endpoint relabeling containment.
- [x] Transitional service-object representation and selector preservation
      substrate for endpoint-backed service facets.
- [x] Historical service-object routing/lifecycle proof: synthetic
      receiver-cookie spoofing, lifecycle, and transfer coverage in commit
      `a4655f0`.
- [x] Session-Bound Invocation Context Gate 1: one immutable session context per
      process, with child inheritance and hostile second-session injection
      checks, demonstrated by `make run-session-context`.
- [ ] Session-Bound Invocation Context Gate 2: privacy-preserving endpoint
      caller-session metadata, explicit subject disclosure, and payload
      spoofing/disclosure hostile checks.
- [ ] Session-Bound Invocation Context Gate 3: chat / adventure / stdio
      migrated off caller-selected endpoint identity to session-keyed service
      authority.
- [ ] Trust-boundary doc refresh recording the post-migration state.

Closes via: `docs/backlog/session-bound-invocation-context.md`. Already next on
the mainline path per `WORKPLAN.md`.

## Claim C2: Ring + one progress syscall is a sufficient boundary

**Status: implementation done, numbers missing.**

- [x] `cap_enter` semantics, SQ/CQ ring, CALL/RECV/RETURN/RELEASE/NOP.
- [x] Direct-switch IPC handoff.
- [x] Loom protocol model.
- [x] `make run-measure` benchmark-only feature scaffolding.
- [ ] Reproducible measurement run that records:
  - `cap_enter` warm/cold round-trip latency
  - SQE dispatch throughput
  - Endpoint IPC: scheduler vs. direct-switch handoff latency
  - Schema dispatch overhead vs. NullCap baseline
  - Memory cost per capability slot
- [ ] Tracked path for measurement output so the paper can cite a commit.
- [ ] Optional: comparison numbers from published seL4/Zircon literature
      where the comparison is fair.

Closes via: a dedicated measurement-harness slice. Not yet in
`WORKPLAN.md`; promote when scheduling allows.

## Claim C3: Wire format enables persistence

**Status: missing.**

- [ ] Minimal RAM-backed `Store` capability.
- [ ] One non-trivial capability whose state is serialized via its capnp
      schema, dumped, and restored across kernel reboot in QEMU.
- [ ] Method call on the restored capability returns the expected result.
- [ ] QEMU smoke target wired to this proof.
- [ ] Documentation explicitly scoping this to "paper evidence" rather than
      the full storage proposal in
      `docs/proposals/storage-and-naming-proposal.md`.

Closes via: a paper-scoped persistence-PoC slice, narrower than the
storage proposal. Not in `WORKPLAN.md` yet.

## Claim C4: Wire format enables network transparency

**Status: missing.**

- [ ] `RemoteCap` shim forwarding one capnp method call over an established
      TCP capability.
- [ ] Working setup: two capOS QEMU guests, or one capOS guest plus a host
      capnp stub.
- [ ] QEMU smoke target proving end-to-end success and clean teardown.
- [ ] Documentation explicitly scoping this to "paper evidence" rather than
      a general network-transparency subsystem.

Closes via: a paper-scoped network-transparency-PoC slice. Naturally rides on
the SSH/Telnet networking work in `docs/backlog/runtime-network-shell.md`.

## Claim C5: Practical kernel verification at this size

**Status: strong, needs distillation.**

- [x] Bounded Kani gates: cap-table, frame-bitmap, transfer rollback,
      resource accounting.
- [x] Loom ring model.
- [x] Miri host-test path.
- [x] Panic-surface inventory.
- [x] Dependency policy (`cargo-deny`, `cargo-audit`).
- [x] Trusted build inputs inventory.
- [ ] Ring protocol Kani proof (currently Loom-only) -- Tier-2 strengthener.
- [ ] Concise summary table for the paper: invariant, tool, scope, bounds.

Closes via: `docs/backlog/security-verification.md` plus a paper-section
distillation pass.

## Cross-cutting strengtheners

Not blocking the thesis, but materially raise quality:

- [ ] **SSH Shell Gateway** end-to-end. Paused behind the selected
      Session-Bound Invocation Context milestone, but still the concrete
      external-facing artifact for §6 when remote shell work resumes.
- [ ] **Full concurrent SMP scheduling.** Removes a single-CPU asterisk.
- [ ] **One non-toy demo** beyond Adventure / First Chat: storage-backed or
      federated, depending on which composes with C3 / C4.

## How to update this file

Update in the same task that lands the artifact. When ticking a checkbox:

1. Reference the closing commit or branch.
2. If the closing artifact reframes the claim, update `plan.md` and
   `outline.md` in the same task.
3. If a Tier-1 gap closes, revisit `WORKPLAN.md` to verify paper-driven
   sequencing still matches the next mainline slice.