Portable Kernel Core

One crate, four link targets

chio-kernel-core is #![no_std] with extern crate alloc and #![deny(unsafe_code)]. Its module doc states the posture at source level: the crate never names std::*. Four crates in the tree link it: the hosted shell chio-kernel, the wasm-bindgen adapter chio-kernel-browser, the UniFFI adapter chio-kernel-mobile, and the C ABI in crates/sdk/chio-cpp-kernel-ffi.

The three FFI adapters route a governed action through one core entry point, evaluate_with_full_floor_and_root. The hosted shell is the exception. It wraps that same call as evaluate_portable_verdict, which formal/proof-manifest.toml registers as the shell entry point inside the bounded verified core, but that method has no non-test caller in the repo. Production admission goes through verify_capability_full_pre_admit, which enters the core at verify_capability_full_with_root and runs the rest of dispatch in chio-kernel.

Portability here is a build result, not a design intention. scripts/check-portable-kernel.sh compiles the crate twice, and the adapters carry their own qualification scripts on top. Every crate, script, and workflow named below is in the tree. Guarantees and limits collects the places where a claim is narrower than it sounds, including the checks the portable adapters do not run at all.

The four build shapes

One line in that table is easy to skim past. Only the browser adapter is no_std end to end. Mobile and the C ABI are ordinary hosted builds that link a portable core, which is why both reach for std::collections::BTreeMap and std::time::SystemTime in their own code. The core’s portability buys them the absence of tokio, rusqlite, and a socket, not a no_std obligation of their own.

The unsafe posture differs the same way. The core and the browser adapter both carry #![deny(unsafe_code)]. The mobile crate cannot: UniFFI’s build-script-generated scaffolding declares the #[no_mangle] extern "C" symbols Swift and Kotlin link against, and a crate-root deny would reject generated code the crate does not author. Its three submodules (clock, rng, errors) carry #![forbid(unsafe_code)] instead. The crate root, which is where all eleven entry points live and where include_scaffolding! pulls the generated shim in, carries neither attribute; the source is free of unsafe by inspection, not by lint. The C ABI holds exactly two unsafe blocks, both SAFETY-commented: CStr::from_ptr after a null check, and Vec::from_raw_parts in chio_kernel_buffer_free.

Clock and Rng are the whole seam

A portable core that computes verdicts still needs two things it cannot compute: the time, and fresh bytes. Both arrive as traits with one method each, and no other platform facility is named in the crate. Three further traits are also injected rather than implemented, but they carry policy instead of platform: Guard, BudgetRegistry, and TrustRootResolver. What the adapters pass for those three is the substance of the section after this one.

/// Abstract monotonic wall-clock exposing Unix seconds.
///
/// Implementations MUST return a value consistent with the signed
/// `issued_at` / `expires_at` fields on capabilities. The verdict path is
/// fail-closed against clock errors: if `now_unix_secs` returns a value in
/// the past of `issued_at` or past `expires_at`, the capability is rejected.
pub trait Clock {
    /// Current Unix timestamp in seconds.
    fn now_unix_secs(&self) -> u64;
}

Rng is the same shape: fn fill_bytes(&self, dest: &mut [u8]), with a doc comment requiring cryptographically strong output and a deliberate absence of anything else, so adapters can route straight to a native CSPRNG. Who actually implements them is more interesting than the traits.

Two rows deserve the emphasis. The hosted shell implements neither seam: it pins a timestamp it already owns and hands the core a FixedClock, so the second a hosted decision is evaluated at is fixed before the core is entered, not sampled inside it. And the entropy seam is barely used at all. Mobile and the C ABI both take a 32-byte Ed25519 signing seed as lowercase hex from the caller, so the only place an adapter reads its own Rng is the browser’s mint_signing_seed_hex. Do not read Rng as a live dependency on every path; it is a seam that exists so a portable target can mint a key without importing an OS.

Both traits fail toward refusal. BrowserClock divides milliseconds by 1000 and truncates, which can only make now smaller and therefore biases toward not yet valid rather than still valid past expiry; a non-finite or non-positive Date.now() returns 0, an f64 past u64::MAX saturates to expired, and MobileClock clamps to 0 before the epoch. Both browser types have host-target stubs so the rlib links for native tests: BrowserClock returns 0 and WebCryptoRng::try_new always errors, which is only reachable off wasm, where the entry points are cfg-gated out. Rng has no error channel, so every implementation zero-fills on failure, including the core’s test-only NullRng. The zero buffer is not the safety property; the callers are. mint_signing_seed_hex rejects an all-zero seed with weak_entropy, and both browser signers and backend_from_seed_hex on mobile check for it before they build a keypair.

The C ABI does not. Its two signers call Keypair::from_seed_hex directly, and that constructor validates hex and length only, so a 32-byte zero seed is accepted and signs. Nothing in the C path is holding the invariant the other two adapters hold, and no test covers it. A C++ embedder that mints its own seed owns that check.

The portability gate

#!/usr/bin/env bash

set -euo pipefail

ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
cd "$ROOT_DIR"

export CARGO_TARGET_DIR="${CARGO_TARGET_DIR:-target/portable-kernel}"

rustup target add wasm32-unknown-unknown >/dev/null

echo "[portable-kernel] building host target with --no-default-features"
cargo build -p chio-kernel-core --no-default-features

echo "[portable-kernel] building wasm32-unknown-unknown with --no-default-features"
cargo build -p chio-kernel-core --target wasm32-unknown-unknown --no-default-features

echo "[portable-kernel] ok"

info: component rust-std for target wasm32-unknown-unknown is up to date
[portable-kernel] building host target with --no-default-features
...
    Finished `dev` profile [unoptimized] target(s) in 13.99s
[portable-kernel] building wasm32-unknown-unknown with --no-default-features
...
    Finished `dev` profile [unoptimized] target(s) in 18.60s
[portable-kernel] ok

The elided lines are cargo compiling dependencies: 63 Compiling lines for the host target and 64 for wasm32. The extra crates on the wasm side are wasm-bindgen and js-sys, which arrive through getrandom on that target. The script exits 0, and both builds together took 33 seconds from a cold target/portable-kernel directory on an M-series laptop.

That is the whole script. It proves one thing precisely: the crate compiles with no default features, both natively and for a target with no std to fall back on. The feature graph is arranged so this is the only configuration that matters. Every optional feature implies std: revocation-view because arc-swap needs a hosted runtime, fuzz because libFuzzer does, dudect because its harness pulls clap and OS time. Turning defaults off turns all of them off together, so there is no half-portable build to reason about.

The gate runs from scripts/ci-workspace.sh, which scripts/qualify-release.sh calls first, which the Release Qualification workflow runs on push to main and on manual dispatch. It is also a gate_commands entry in formal/proof-manifest.toml, and scripts/generate-proof-report.sh executes that list rather than only validating it, which gives the gate a second run inside the nightly workspace proof report. Both invocations are post-merge. The PR-tier script scripts/ci-pr-tier.sh does not include it and no workflow references it directly, so a change that breaks the portable build is caught after merge rather than before.

Four things the script does not do, in case its name suggests otherwise. It builds and does not test, so no behavior is exercised on the wasm target here. It applies no artifact size budget: the nightly browser-kernel-twiggy workflow measures the bundle and writes budget_enforcement: advisory into its own manifest, so no size threshold is enforced anywhere in the repo. It never builds wasm32-wasip1, which the crate’s doc comment and README both name as a supported environment. The only recipe for that triple anywhere in the repo is a proposed workflow snippet inside PORTABLE-KERNEL-ARCHITECTURE.md. And it says nothing about the adapters, which qualify separately, both under nightly and under release qualification: qualify-portable-browser.sh drives wasm-pack test --release --headless --chrome and records artifact bytes plus an evaluate latency, and qualify-mobile-kernel.sh runs four lanes and marks each pass, fail, or environment_dependent so an iOS or Android claim stays tied to the toolchain actually present on the qualifying host. That script fails unless at least one target-backed mobile lane runs and passes. Read those lanes precisely: only the host lane runs a test (--test ffi_roundtrip). The three target-backed lanes are release cross-compiles for aarch64-apple-ios, aarch64-apple-ios-sim, and aarch64-linux-android. No Chio test executes on a device or a simulator.

One evaluation, three wire mappings

The three FFI adapters converge to an almost identical body. Each parses a JSON envelope, refuses authorization extensions it cannot authenticate, decodes trusted issuer keys from hex, seeds a per-request InMemoryBudgetRegistry from caller-supplied parent-budget snapshots, pins CapabilityCryptoFloor::AllowClassical, passes an empty guard slice, and calls evaluate_with_full_floor_and_root. The registry is constructed inside the call and dropped when it returns, so sibling-sum admission is enforced against the snapshot the caller supplied and nothing accumulates between calls. Everything up to the verdict is shared. What differs is how each maps that verdict onto the wire.

The browser row is a policy decision, not a capability gap. Two fields in EvaluationVerdictJson are unconditional constants regardless of the verdict: authorized: false and guards_evaluated: false, and the reason it substitutes on an allow says why in the payload itself: capability-only browser evaluation requires a mediated prevent receipt before execution. A browser caller cannot construct a response from this adapter that claims authorization. The third row is defensive rather than live. The core never emits PendingApproval: a guard that returns it is rewritten to GuardDenied, and the EvaluationVerdict doc comment says so outright. Each adapter still writes the arm, because its wire enum mirrors the shell’s three-valued one and a synchronous request-and-response has nowhere to put a human decision. Match on the two verdicts the core can actually return.

Mobile and the C ABI are held byte-identical by test. crates/kernel/chio-kernel-mobile/tests/cross_ffi_parity.rs pulls the C ABI crate in as a source module with #[path = "../../../sdk/chio-cpp-kernel-ffi/src/lib.rs"], drives both entry points over a three-case fixture (allow_echo, deny_unknown_tool, deny_unknown_server), and asserts mobile.as_bytes() == cpp.as_bytes() on the verdict JSON. Two further tests assert both refuse a negotiated aggregate-invocation or cumulative-approval family whose direct root token does not match. The comparison is narrower than it looks: it compiles the C ABI as Rust rather than linking the staticlib through the C header, and the browser adapter is not in it, which is exactly why the browser can diverge without a test firing. It diverges twice. It maps the allow row differently, and its signer overwrites body.kernel_key with the key derived from the seed, where mobile and the C ABI refuse a body whose kernel_key does not already match.

What every portable adapter refuses

• Authorization it cannot authenticate. A request carrying a governed_intent, an approval_token or approval_tokens, a threshold_approval_proposal, or a supplemental_authorization is parsed and then rejected before evaluation begins. The fields are declared explicitly on each wire type so they are refused rather than silently dropped.
• Two capability features outright. A token carrying an aggregate_invocation_budget or a cumulative-approval scope is denied inside the core before subject binding, with the reason capability feature unsupported on this runtime: aggregate invocation enforcement or its cumulative-approval counterpart. Enforcing either needs durable cross-call state that no portable adapter has, so the portable path refuses the token rather than under-enforcing it. The cross-FFI parity test pins the exact string.
• A guard pipeline. All three pass &[]. Capability signature, crypto floor, time bounds, subject binding, portable scope match, and sibling-sum admission all still run; the seven-guard default pipeline does not.
• Anything that needs state. No adapter consults a revocation list, checks a DPoP proof, or persists a receipt. The core has no revocation lookup by construction, and none of the three installs a revocation view or a receipt store on top of it. An allow from a portable adapter says the capability verified and matched at the supplied time; it does not say the capability is still live, and no receipt exists until the host app ships one somewhere.
• Signing without the preimage. The public signer on each adapter recomputes content_hash over the caller-supplied canonical content inside the trust boundary and refuses on mismatch. The browser refuses outright when the preimage is absent rather than falling back. A separately named relay entry point exists for transports that only forward a body an upstream trusted producer already minted, and it is not the default on any of the three.
• A stale ABI. CHIO_CPP_KERNEL_FFI_ABI_VERSION is 2, bumped when the signer gained its third pointer argument under an unchanged symbol name. A C++ client that gates on chio_kernel_ffi_abi_version() fails closed instead of calling the three-argument symbol with a dangling pointer.

Coverage is not uniform. verify_passport is exposed by the mobile UDL and by the C ABI and appears nowhere in the browser crate, despite the browser manifest’s comment claiming otherwise. Hardware attestation is mobile only: App Attest and Play Integrity challenge and verification entry points come from chio-custody-hw, and verify_mobile_receipt answers with an explicit "status": "shape_only", authoritative: false, authorized: false. Take that response as a shape check, not an authorization.

The language SDKs are not embedded kernels

Four packages embed the decision core: the Rust shell, the wasm bundle, the mobile static and shared libraries, and the C static library. The Python, Go, and TypeScript SDKs are none of them. They are hosted-session clients that talk to a running kernel over HTTP. sdks/python/chio-py/ARCHITECTURE.md names its facade as one "for hosted sessions, auth, receipt queries, nested callback helpers, and errors", and ChioClient takes a base_url and a bearer token and posts JSON-RPC. sdks/go/chio-go/ARCHITECTURE.md assigns its client, session, transport, auth, and nested packages to the hosted SDK runtime, and records that the parity check "requires neither CGO nor native bindings". The TypeScript SDK exports the same shape.

Each of the three ships an invariants module, and it is worth being exact about what that is. It holds canonical JSON, SHA-256 hashing, Ed25519 signing and verification, and structural checks for capabilities, receipts, and signed manifests, written natively in each language so a client can verify what a kernel produced without linking Rust. It reads the decision recorded on a receipt; it never produces one. There is no guard pipeline and no evaluate. A Python or Go process cannot decide a governed action locally; it can only check the cryptography and the shape of artifacts a kernel already decided.

Guarantees and limits

Next steps

• Core & Shell · the other half of this split: what the core decides, what it fences out, and where each fenced item files
• Capabilities · the token every portable adapter verifies before anything else runs
• The Three Verdicts · the enum these adapters map, and what every other consumer of it does
• Receipts & Audit · the canonical body and the recompute-and-refuse signer all four targets share
• Fail-Closed Semantics · the refusal discipline the clock clamps and the zero-seed checks are instances of
• Node Overview · the process the desktop shell becomes once it opens a store
• Assumptions & TCB · the bounded proof claim the portability gate is a gate command for