Build, Boot, and Test

The commands below are the current local workflow for the x86_64 QEMU target. The root Cargo configuration defaults to x86_64-unknown-none, so host tests must use the repo aliases instead of bare cargo test. This page explains the main workflows rather than inventorying every focused proof target. The workflow-gates registry defines named checks and their applicability; the Makefile remains authoritative for concrete targets.

Prerequisites

Expected host tools:

• Rust nightly from rust-toolchain.toml
• make
• qemu-system-x86_64
• xorriso
• curl, sha256sum, and standard build tools for pinned tool downloads
• Go, used by the Makefile to install the pinned CUE compiler when needed
• A Telnet client for the optional focused loopback shell demo
• Chromium, Chromium Browser, or Google Chrome for the optional remote-session CapSet browser UI automation
• Optional policy and proof tools for extended checks: cargo-deny, cargo-audit, cargo-fuzz, cargo-miri, and cargo-kani

The Makefile pins and verifies:

• Limine at the commit recorded in Makefile
• Cap’n Proto compiler version 1.2.0
• CUE version 0.16.0

Pinned repo-selected tools are installed under CAPOS_TOOLS_ROOT, which defaults to the per-user $HOME/.capos-tools cache. Override CAPOS_TOOLS_ROOT=/path/to/cache when a host needs a different cache location.

Build the ISO

Use the default target when you need the current bootable capOS image.

make

This builds:

• the kernel with the default bare-metal target;
• the standalone init userspace binary used by focused spawn proofs;
• release-built demo service binaries under demos/;
• the capos-rt userspace binaries, including the shell proof;
• manifest.bin from system.cue;
• capos.iso with Limine boot files.

Relevant files: Makefile, limine.conf, system.cue, tools/mkmanifest/.

Compare Build Provenance

Use make build-provenance to write the local build record at target/build-provenance.txt. To compare two retained records locally:

make build-provenance-compare \
  BASE_PROVENANCE=path/to/base-build-provenance.txt \
  CANDIDATE_PROVENANCE=path/to/candidate-build-provenance.txt

The comparison ignores the generated timestamp and allowed local path-root movement under worktree target/ directories or .capos-tools/ caches. It fails for material provenance drift, including source commit changes, manifest or artifact hash changes, embedded binary hash changes, OVMF identity/hash changes, Rust compiler date/commit changes, host-tool version or package identity changes, and operating-system identity changes.

To compare a branch build against its base build environment, use the environment policy:

make build-provenance-compare \
  BUILD_PROVENANCE_COMPARE_POLICY=ci-environment \
  BASE_PROVENANCE=path/to/base-build-provenance.txt \
  CANDIDATE_PROVENANCE=path/to/candidate-build-provenance.txt

That mode allows expected source and artifact hash changes while still failing for runner, GitHub-hosted image, Rust, selected-tool, package-identity, OVMF selection, and OVMF hash drift. Run it yourself over two retained records: CI fires only on release tags and workflow_dispatch, so nothing compares base against head automatically. It is an environment-drift check, not a production reproducibility claim.

Local synthetic comparison checks may create scratch records under target/provenance-fixtures/ or Python bytecode caches under tools/. Clean those scratch artifacts with:

make build-provenance-compare-clean

Boot QEMU

Use the default run targets to boot either the operator-facing system or the scripted login-path smoke.

make run
make run-smoke
make test-default-boot

make run is the operator-facing boot path. It builds the ISO with the qemu feature, boots QEMU with the interactive terminal UART on stdio, attaches virtio-net with host-local remote CapSet forwarding, and writes the separate kernel/debug UART log to target/qemu-console.log. The run output prints the actual forwarded port as remote CapSet: tcp 127.0.0.1 <port> -> guest :2327.

make run-smoke exercises the focused init-owned shell login path. make test-default-boot separately boots the default system.cue service graph; the focused smoke overrides the manifest and cannot substitute for that gate.

QEMU proof-outcome classifications are recorded per harness in docs/workflow/qemu-proof-outcome-adoption.toml, with their class semantics defined by the QEMU proof outcome contract. Harnesses recorded as status-1-only adopt the shared three-outcome classifier. Multi-pass harnesses classify each status-bearing QEMU boot independently. These harnesses report one of three outcomes:

• Pass: QEMU reaches the proof’s expected exit and every transcript assertion succeeds.
• Assertion failure: the run produces evidence that does not satisfy the proof, including an unexpected exit or missing transcript assertion. The harness exits with status 1.
• Startup stall: timeout exits with status 124 and the kernel UART log is an existing zero-byte file. The harness emits a startup-stall diagnostic and exits with status 3. This classifies the observed run, not its cause: a host startup stall and a pre-UART guest regression have the same signature. Rerun the same target once and classify the rerun independently. If the rerun also stalls, stop retrying and treat the proof as failed pending diagnosis, including early-boot regressions. Harnesses do not retry automatically, and a startup-stall outcome never passes the proof.

Developers can opt into that one-rerun policy without changing any proof recipe:

tools/run-proof-with-stall-retry.sh <make-target> [make-args...]

The wrapper runs each attempt serially (make -j1) without a PTY. Combined attempt output streams incrementally to the wrapper’s stderr and is retained in a unique log. The exact startup-stall diagnostic and its matching Make Error 3 record stay in that private log but are omitted from the live stream when the wrapper classifies the attempt as a retryable stall; the structured attempt status, classification, and log path remain on stdout. This keeps a passing rerun from leaving failure-shaped text in outer grep-based proof logs. The wrapper retries at most once, and only when the first attempt contains both the exact startup-stall diagnostic from tools/qemu-startup-stall-guard.sh and Make’s matching Error 3 recipe record. GNU Make normalizes a failed recipe to outer status 2, so the wrapper reports both that outer attempt status and the guard’s status-3 classification. It prints every attempted log path and status. A passing rerun exits 0 while retaining the first stall log; a second classified stall exits 3. Any assertion, build, non-empty-UART timeout, or other failure is not retried and retains the Make process’s status.

Each attempt log retains at most 1 MiB total. When earlier output is discarded, its marker reports the exact number of original output bytes retained after the marker itself. The private log directory retains at most 64 run directories and never deletes evidence automatically; remove retained run-* directories or select another CAPOS_PROOF_RETRY_LOG_DIR when it is full. Log setup, capture, and retention-cap failures exit 125 before reporting a proof result. The restrictive log permissions do not change the umask inherited by the proof recipe.

The plaintext loopback Telnet research demo was a Phase B fixture, not part of the default operator path. Its targets are retired because they depended on the removed qemu-only kernel TCP listener. Use make test-login for current in-guest shell coverage and make test-cloud-prod-network-stack-smoltcp-tcp-listener-roundtrip for the current Phase C userspace TCP socket proof.

The same make run boot starts the remote-session CapSet gateway. To run the host CLI against it, use the printed port:

cargo run --manifest-path tools/remote-session-client/Cargo.toml \
  --target x86_64-unknown-linux-gnu \
  --bin remote-session-client -- --host 127.0.0.1 --port <port>

Add --launch-adventure to that command when you want the CLI to start the default-manifest Adventure service graph through serviceLaunch and require a running status.

To run the trusted local web bridge against the same QEMU instance:

CAPOS_REMOTE_SESSION_PORT=<port> make remote-session-ui

Then open http://127.0.0.1:3337/. The Rust bridge holds the TCP stream, remote session state, and backend-held remote CapSet; the browser receives only view models, launch/status descriptors, denial diagnostics, call results, and redacted transcript rows. The former automated kernel-listener browser proof is retired. Use make run-cloud-prod-remote-session-web-ui-l4 for the current Phase C Web UI L4 browser proof.

A Tauri desktop wrapper is available as a repo-local check/dev layer over the same Rust backend. The repo-local make remote-session-tauri target first runs a policy preflight over the reviewed scaffold, then checks for the Tauri CLI and Linux build prerequisites, reports dependency and scaffold status, and runs a deterministic wrapper check when those prerequisites are present. It follows the official Tauri v2 Linux prerequisite shape, including WebKitGTK 4.1, libxdo, OpenSSL, AppIndicator, and Rsvg development packages where applicable. Missing dependencies fail with explicit diagnostics and point back to the supported local web bridge. The operator command shape is:

CAPOS_REMOTE_SESSION_PORT=<port> make remote-session-tauri

Set CAPOS_REMOTE_SESSION_TAURI_MODE=dev to launch cargo tauri dev. CAPOS_REMOTE_SESSION_TAURI_MODE=policy tools/remote-session-tauri.sh runs only the scaffold guardrail and does not require Tauri system packages or a desktop session. CAPOS_REMOTE_SESSION_TAURI_MODE=package and CAPOS_REMOTE_SESSION_TAURI_MODE=automation are intentionally blocked with diagnostics describing the remaining packaging and desktop-automation review work. This policy preflight proves only that the current wrapper remains a check/dev scaffold with packaging disabled, the loopback URL pinned, a single main window, default core:default permission scope, and no app-specific Tauri command/plugin authority. It is not a distributable packaging or desktop automation proof. make remote-session-ui remains the supported fallback host UI path and uses the same backend-held authority boundary.

Default make run starts chat, the remote-session gateway, and shell services. It embeds Adventure server/NPC/client binaries and the terminal Paperclips binary. The current remote-session Adventure slice makes serviceLaunch a real restricted backend launch in that default manifest: the trusted backend/gateway starts adventure-server plus simple NPC companions through an approved service-runner profile and attaches or retains backend-held descriptors/caps for the Adventure/chat-facing services. Run it by starting make run, noting the printed remote CapSet forwarding port, and then using either the host CLI or CAPOS_REMOTE_SESSION_PORT=<printed-port> make remote-session-ui. make test-paperclips remains the focused authoritative Paperclips server proof; default-manifest Paperclips launch is not implemented by this slice. Raw ProcessSpawner, process owner handles, endpoint owner caps, local cap ids, result-cap slots, and browser-held capOS caps are non-goals for this UI path. Process handles stay backend-local.

GCE Web UI Proof Target Map

Use the selected-milestone proof targets below to choose the narrowest evidence gate for the GCE self-hosted Web UI ladder. Local QEMU/cloudboot targets do not prove live provider reachability, and private GCE targets do not authorize public ingress or TLS exposure.

The run-cloud-prod-remote-session-web-ui-l4 browser tail needs a headless-capable Chromium/Chrome. tools/qemu-remote-session-self-served-ui-harness.sh resolves one in this order: an explicit CAPOS_REMOTE_SESSION_UI_BROWSER override, then a non-snap browser on PATH, then a Chrome-for-Testing binary in the puppeteer cache ($HOME/.cache/puppeteer, overridable with CAPOS_REMOTE_SESSION_PUPPETEER_CACHE). Snap-backed chromium wrappers are rejected because snap requires a user systemd/logind session bus and a snap-managed cgroup that a detached/headless worker lacks; the harness fails early with the typed blocker remote-session-web-ui-l4: BLOCKED no-headless-browser-runtime and remediation steps rather than skipping the browser assertions. When unprivileged user namespaces and a usable root-owned setuid sandbox helper are both unavailable (for example on a constrained AppArmor worker), a non-snap Chrome is launched with --no-sandbox; when either sandbox mechanism is available it is kept. CAPOS_REMOTE_SESSION_UI_NO_SANDBOX=0|1 overrides those probes. The pure selection and sandbox helpers are covered by tools/qemu-remote-session-self-served-ui-harness.sh --self-test, which the L4 gate runs before booting QEMU.

make run-smoke uses the focused init-owned system-smoke.cue verification path. It drives the login and shell session through the terminal UART, captures the kernel log and terminal transcript separately, and checks that the kernel boot-launched standalone init, init launched capos-shell as the supervised shell service with its scoped grants, and the guest reached the expected audit, shell-bundle, child-isolation, stale-handle, and no-password-echo assertions before QEMU exits. This remains distinct from the default system.cue path, whose init-owned graph starts the full operator-facing service set.

Spawn Smoke

Use the spawn smoke when changes affect manifest-owned process creation, ProcessSpawner behavior, or bootstrap capability wiring.

make run-spawn

This boots with system-spawn.cue, the focused init-owned manifest retained for ProcessSpawner checks. Only init is boot-launched by the kernel; init uses ProcessSpawner to launch endpoint, IPC, VirtualMemory, Timer, ThreadControl, the single-thread runtime checkpoint, FrameAllocator cleanup, and hostile spawn demo children, wait for ProcessHandles, and exercise hostile spawn inputs. The target captures the kernel log separately and runs tools/qemu-spawn-smoke.sh to assert the single-init boot markers, BootPackage validation, child spawn/exit records, Timer now/sleep and per-process sleep quota proof lines, runtime FS-base proof lines, the single-thread runtime map/protect/unmap plus park-fallback checkpoint, manifest child waits, and clean halt.

Shell and Terminal Smokes

Use these focused QEMU smokes for shell, terminal, credential, and login paths. The Manifest and Service Startup page defines the init-owned graph contract and distinguishes the manifests migrated under the init mandate – every boot manifest’s init binary must be init – from manifests such as the shell-log pair that were already compliant.

make test-shell
make test-shell-log
make test-terminal
make run-credential
make test-login
make test-login-setup

• make test-shell boots the focused system-shell.cue manifest (no pre-provisioned verifier) and exercises the shell entirely in its anonymous session: CapSet listing, typed capability inspection, typed application-error display, anonymous-session metadata, the anonymous launcher rejecting spawn-test because its allowlist is empty, and clean exit.
• make test-shell-uptime boots two focused manifests to prove the shell uptime command over a granted monotonic Timer cap: the timer-granted manifest reads uptime twice across a sleep and asserts a bounded, strictly-increasing since-boot value; the timer-less manifest asserts the fail-soft “unavailable” path (the command never panics without the grant).
• make test-shell-log boots two focused manifests to prove the shell log command over a granted read-only LogReader cap. Both boots run log-producer services that fill the bounded kernel recent-record ring through scoped LogSink caps (nothing kernel-side writes to that ring on its own), and they land more records than one kernel read window returns, so the granted boot asserts log pages on nextCursor to report them all and never surfaces the below-threshold debug records the sink dropped. The grant-less manifest keeps the identical producers, so its fail-soft “unavailable” path is proved to be about the missing cap rather than an empty ring.
• make test-shell-fs boots two focused manifests to prove the shell ls/cat filesystem-browse commands over a granted read-only Directory cap: the granted manifest (a CAPOSRO1 virtio-blk backer with known readme.txt/ data.bin entries) asserts ls lists both entries, cat readme.txt prints the known bytes, cat data.bin reports the bounded binary window, and a missing entry fails closed while the shell stays usable; the grant-less manifest asserts the fail-soft “unavailable” path.
• make test-terminal boots the focused system-terminal.cue manifest and exercises the TerminalSession substrate: visible and hidden echo input, bounded readLine, structured cancellation, and stale-input scrubbing between prompts.
• make run-credential boots the focused CredentialStore proof manifest.
• make test-login boots the focused password-login manifest and proves the shell’s login command prompting for username> before hidden password>, failing generically on a wrong password, succeeding for the demo account, swapping from the anonymous bundle to the operator bundle, and performing exact-grant child launch plus stale-handle release.
• make test-login-setup boots the no-password first-boot setup manifest and proves that setup creates a volatile credential, discloses that volatility, chains into the login upgrade path, and reaches the same narrow operator shell bundle.

Durable account storage and multi-verifier local accounts are still future work; the current username-aware login path selects the manifest-seeded operator-kind account and any volatile first-boot credential record that setup creates.

Focused Service Smokes

Use these targets to prove resident services and demo clients still launch through the intended shell-granted authorities. Most focused proofs now declare their assertions as data in tools/proofs/*.markers; see Proof Marker Sets for the format, for adding a proof, and for make proof-marker-mutation-check / make proof-registry-check.

make test-chat
make test-adventure
make test-paperclips
make test-revocable-read
make test-memoryobject-shared
make test-ringtap-failing-call

• make test-chat boots the focused First Chat manifest and proves a shell-spawned client can send a line through the resident singleton chat service using the broker-issued operator chat endpoint and observe the resident bot reply.
• make test-adventure boots the focused adventure manifest and proves the shell-spawned client can drive the current scripted mission through explicit StdIO, adventure, and chat endpoint grants.
• make test-paperclips boots the focused Paperclips terminal demo manifest, authenticates the shell, starts Paperclips server services, first launches the clean-room terminal client with explicit StdIO plus the normal PaperclipsGame endpoint, proves normal server authority cannot invoke run <ms>, rejects a forged proof_accelerator: @timer grant, then relaunches against the proof server endpoint with the explicit proof_accelerator proof authority for the accelerated transcript. The server owns generated content, game state, regular timer cadence, unlock checks, and game-rule mutation, and server-mode client help is rendered from structured server command specs. That transcript rejects an early locked autoclipper purchase, rejects an over-budget wire purchase, rejects bulk manual production, rejects a high-price sale with zero current demand, rejects manual production after automation drains wire, drives one-at-a-time manual production, explicit sales, repeatable marketing, autoclipper unlock, real-time automation, generated typed Cap’n Proto content loading, scaled business-phase production, precision-rollers, design-search, forecast-engine, the survey-drones transition to == autonomous phase ==, representative autonomous drone/factory scaling with local-matter conversion and additional clip production, the mesh-coordination and seed-probes cosmic transition, bounded probe replication and production, locked final-conversion, and clean client/shell exit.
• make test-revocable-read exercises the revocation transcript for endpoint and boot-package authority loss.
• make test-memoryobject-shared proves MemoryObject-backed parent/child sharing and cleanup.
• make test-ringtap-failing-call enables debug_tap, drives a known typed launcher failure, and runs the ringtap viewer over the captured log.

Networking and Measurement Targets

Use these targets for the current network proof path and benchmark-only measurement image.

make run-net
make qemu-net-harness
make test-measure

• make run-net attaches a QEMU virtio-net PCI device and exercises current PCI enumeration, virtio transport setup, and TX descriptor completion diagnostics, plus ARP resolution and ICMP echo validation against the QEMU user-mode gateway.
• make qemu-net-harness runs the scripted net smoke path.
• make test-measure enables the separate measure feature for benchmark-only counters and cycle measurements. It boots system-measure.cue, where init spawns ring-nop and grants the measurement-only NullCap and ParkBench caps through ProcessSpawner. The demo prints ring/NullCap baselines plus a park-shaped comparison between compact authority-checked SQEs and generic Cap’n Proto methods. The kernel summary includes per-segment dispatch counts, total cycles, and averages for SQE processing, validation, cap lookup, capnp decode, method body dispatch, CQE posting, and waiter wake/check. Do not treat it as the normal dispatch build. The QEMU phase has a 180-second default bound; set QEMU_MEASURE_TIMEOUT on the Make invocation to override it.

Formatting and Generated Code

Use these local checks before claiming source formatting or generated artifacts are current.

make fmt
make fmt-check
make workflow-check
make generated-code-check
make check

• make fmt formats the kernel workspace plus standalone init, demos, and capos-rt crates.
• make fmt-check verifies formatting without modifying files.
• make workflow-check validates workflow policy, Markdown links, documentation budgets, and evidence trailers. Use the gate registry to derive the additional checks made mandatory by changed paths.
• make generated-code-check verifies checked-in Cap’n Proto generated code against the repo-pinned compiler path and checks generated adventure plus Paperclips content against their CUE sources.
• make check runs the repository’s aggregate local check target. Consult the gate registry for its current composition rather than copying that inventory here.

Host Tests

Use these host-side checks for shared logic and userspace build surfaces that do not require a QEMU boot.

cargo test-config
cargo test-ring-loom
cargo test-lib
cargo test-mkmanifest
tools/check-userspace-runtime-surface.sh
make webui-secret-gating-check
make capos-rt-check
make init-capos-build
make demos-capos-build
make shell-capos-build
make capos-rt-capos-build

• cargo test-config runs shared config, manifest, ring, and CapSet tests on the host target.
• cargo test-ring-loom runs the bounded Loom model for SQ/CQ protocol invariants.
• cargo test-lib runs host tests for pure shared logic such as ELF parsing, capability tables, frame allocation, and related property tests.
• cargo test-mkmanifest runs host tests for manifest generation.
• tools/check-userspace-runtime-surface.sh verifies capos-rt owns the userspace entry, panic, allocator, and raw syscall surface.
• make webui-secret-gating-check holds two Web UI security invariants that no QEMU transcript can express: a short-circuiting secret compare still answers 401, and the L4 smoke always builds with probe-seams on. It pins the constant_time_eq call-site count per secret-holding file, so removing any secret comparison fails the gate however the revert is spelled; it flags newly added ==/!= comparisons whose operands name a session/CSRF secret or are byte slices; and it requires every discovered /api/probe/* and /api/stale-* route arm to sit directly behind #[cfg(feature = "probe-seams")] unless allowlisted. The census and the operand lint are complementary: the census catches removals the lint cannot see (a secret bound to a role name such as stored), the lint catches additions the census cannot see. Neither sees a compare that is both newly added and role-named; the script header states that limit rather than implying full coverage. The script self-tests every layer before running, so a gate that stopped being able to fail is itself a failure. make webui-secret-gating-binary-check additionally asserts a default-feature build ships no proof-only route, using /api/logout as a positive control.
• make capos-rt-check builds the standalone runtime smoke binary against targets/x86_64-unknown-capos.json, matching the userspace target used by the boot image.
• make init-capos-build, make demos-capos-build, make shell-capos-build, and make capos-rt-capos-build expose focused custom-target build wrappers for the booted userspace crates and runtime smoke binary.

Extended Verification

Use the extended verification set for shared logic, dependency policy, fuzz targets, and bounded proof gates that are heavier than the normal host-test loop.

make dependency-policy-check
make fuzz-build
make fuzz-smoke
make kani-lib
cargo miri-lib

These require optional tools. Use them when changing dependency policy, manifest parsing, ELF parsing, capability-table/frame logic, or proof-covered shared code. make dependency-policy-check covers Rust deny/audit checks and the docs Node lockfile/audit gate with npm lifecycle scripts disabled. See the Security and Verification Proposal for the rationale behind the extended verification tiers. make kani-lib runs the bounded mandatory cap-table/frame gate.

Validation Rule

For behavior changes, a clean build is not enough. The relevant QEMU process must exercise the behavior and print observable output that proves the path works. make run-smoke is the default login-path gate; make run-spawn, make test-shell, make test-terminal, make run-credential, make test-login, make test-login-setup, make test-chat, make test-adventure, make test-paperclips, make test-revocable-read, make test-memoryobject-shared, make run-net, make qemu-net-harness, make test-ringtap-failing-call, or make test-measure are additional gates for their specific features.