The firmament — dregg on seL4
The firmament is the deterministic ground robigalia's apps run on. It is the boundary that holds them and gives them capabilities — and it embeds the verified dregg executor as a protection domain on the seL4 microkernel. Every app turn runs through that domain; nothing reaches durable state except through a turn it accepted. The apps inside are pure, deterministic, and replayable — not by good behaviour, but because the firmament makes ambient authority structurally absent.
The central claim is one a stranger can check by running it: an seL4 capability and a dregg capability are the same abstraction at two points on a distance parameter. A local install is a first-class deployment with strong properties; reaching the network is seamless, not a port. And it boots today.
One capability, local to global
A firmament capability is a handle (target, rights) an app holds and may
invoke, attenuate (rights' ⊆ rights), or delegate. The interface is the
same whether the target is near or far — the app does not see which backing it holds:
An seL4 kernel object
A CNode slot, an endpoint, a frame. The invocation is a kernel syscall; revocation is seL4_CNode_Revoke; granting a sub-capability is seL4_CNode_Mint with reduced rights. Adoption is attenuation, enforced in hardware by the MMU and the cap-derivation tree.
A dregg cell on a federation
A (possibly remote) cell. The invocation is a turn through the executor; revocation is the group-key epoch lift; granting is a delegation turn gated on the proven granted ⊆ held. The same attenuate / delegate / invoke verbs, the same receipts and proofs.
Dispatch by target alone
One handle type, one router. The app calls resolve or attenuate_and_grant; the router dispatches to the kernel (local) or the executor→net path (distributed) by the handle's target. A widening grant is refused identically at both backings.
This is not just a design — it is a runnable crate (sel4/dregg-firmament/)
wired to the real dregg capability semantics, so it never reinvents
granted ⊆ held. One backing-agnostic app function invokes, attenuates, and
delegates both a local kernel object and a real dregg cell through one router and one
handle type — the real executor in the loop, tests green.
At n=1, the distributed bounds collapse
The honest bounds on a distributed capability are distance bounds, parametrized
by the topology n — the number of machines the target is spread across. The
firmament is where n=1: everything is on one seL4 machine, so the
distributed bounds become strong local properties. A local install is not "distributed
dregg, crippled to one box" — it is the collapsed limit of one model, where the
distance parameter is pinned to its minimum.
| operation | n > 1 (distributed) | n = 1 (firmament, local) |
|---|---|---|
| Revocation | eventual: the epoch lift must propagate; an in-flight invocation may still land | immediate: seL4_CNode_Revoke is synchronous; the cap is dead the instant the syscall returns |
| Checkpoint | a consistent cut across machines (Chandy–Lamport); may be stale | consistent: one domain's cap-state + memory captured atomically |
| Commit | quorum / finality latency; final only after the blocklace finalizes it | synchronous: the durable store writes the commit record in one transaction before the turn returns |
| Agreement | FLP-bounded; needs a consensus round | trivial: one machine is its own quorum |
The product promise is the fluid reach-out: an app runs first-class on
the local firmament with the strong n=1 properties, and the moment one of
its programs reaches out to the network — invokes a capability whose target is a cell on
a remote federation — it flows into native distributed dregg with no seam. The
same handle, the same verbs, the same proofs; only the bounds relax as n
rises. n=1 is a stepping stone, never a terminus: the same binary scales out
without a rewrite, because there was only ever one model.
Where each capability and trust boundary sits
The firmament is a small assembly of protection domains. The seL4 capability partition is the trust boundary: a domain can only touch what it holds a capability for. The verified executor is the heart, and it holds no device and no network capability — it is pure compute over bytes, and the verified semantics is the only authority over state transitions.
| protection domain | role | trust boundary |
|---|---|---|
| executor-PD heart | runs every turn through the verified complete-turn executor | holds no device cap, no network cap — pure compute; the verified semantics is the only authority over state |
| verifier-PD | independent proof checking: proof-in → verdict-out | holds no prover authority, no state cap — a verifier with no callback into a prover, enforced by a missing capability |
| persist-PD | the durable store: commit log, checkpoints, snapshot + overlay | the sole holder of the storage-device cap — the only domain that can touch the disk |
| net-PD edge | the network edge: virtio-net driver; turn ingress | the sole holder of the NIC cap — signature-checks a turn before the executor sees it; bad signatures never reach the heart. The n>1 end of the gradation. |
| app-PDs | the deterministic, replayable apps | hold only the caps the firmament minted — cannot reach a clock, an RNG, a socket, a device, or another app's memory. Ambient authority is structurally absent. |
A domain checkpoint is a dregg snapshot
seL4 can freeze a protection domain's capability state and memory and thaw it later;
dregg has a snapshot model where recover = checkpoint ⊕ overlay = replay (a
verified recovery equation). The firmament marries them: a domain checkpoint is a
dregg snapshot. Because an app is deterministic — no hidden state — its entire observable
state is its cell forest, so the snapshot captures it completely: no torn state, no lost
mutation, no double-apply. And a root tooth makes the thaw unforgeable —
the joiner independently recomputes the reconstructed root and refuses if it does not
match the one the federation attested, so a server cannot ship a self-consistent snapshot
of a different ledger. Freezing and thawing an app is
seal → ship → apply-verified → unseal.
Real protection-domains on seL4, in QEMU
This is no longer a paper scaffold. The Robigalia v0 demo brings real Rust components up as seL4 protection domains, booting under QEMU on a native toolchain — no Docker, no Linux VM. Serial logs from the real boots are captured. The boot ladder:
| rung | what it is | status |
|---|---|---|
| M0 | a Rust protection-domain prints its banner on seL4 | boots (aarch64) |
| M1 | the verifier PD: bundle-in → verify → verdict-out, with an anti-ghost reject | boots (aarch64) |
| M2 | the rbg DirectoryCell PD (versioned CAS, membership ACL, factory slot-caveat) — the Robigalia heart | boots (aarch64) |
| M-STARK | the verifier-stark PD: a real cryptographic STARK (BabyBear + BLAKE3 + FRI + Fiat-Shamir) proved and verified on-device, with the anti-ghost tooth | boots (aarch64) — a verified heart organ |
| executor-PD heart | the Lean kernel execFullForestG itself — the exact gated function the node runs — inside a protection domain: a real turn executes, nonce ticks, the anti-ghost property holds | boots (aarch64) — the verified heart, running |
| M3 | networking: the virtio-net driver PD probes a real device on the wire — device_type=Network, the NIC up with its MAC | driver boots; the smoltcp client PD + ring assembly remains |
| M5 | retarget to riscv64 (OpenSBI → seL4 → userspace → the dregg PD) | boots (M0 on riscv64) |
The M-STARK rung is the one to run first: it proves a real AIR, verifies it (ACCEPT),
and shows the teeth — a tampered proof rejects ("Trace Merkle proof failed"), a wrong
public input rejects ("Public inputs mismatch"). It is the genuine
dregg-circuit STARK carried into a no-std seL4 PD — byte-identical
prove/verify, no Lean, no libuv, no GMP, deterministic so it needs no entropy source.
git clone https://github.com/emberian/dregg && cd dregg/sel4
./setup.sh # Microkit SDK + toolchain (native macOS, Apple Silicon)
make run-stark # a REAL on-device STARK: prove, verify, reject a tampered proof
make run # the rbg DirectoryCell PD (M2)
make run-riscv # M0 on riscv64The executor-PD runs the exact function the node runs
The heart of the firmament is the Lean-compiled complete-turn executor —
execFullForestG, the same gated function the deployed node calls — embedded
as a protection domain. It boots: inside a real seL4 protection domain
under QEMU a turn arrives, the executor decodes it, runs the verified
decode → step → encode, ticks the nonce, emits the receipt, and the
anti-ghost property holds. The Lean-runtime port long called the one true blocker
is closed — the runtime embeds single-threaded, with no global allocator override and no
IO event-loop, the three properties measured rather than assumed (the Lean closure
recompiled to ELF, linked against an ELF Lean runtime; GMP for the target real). No model
of the node sits in the heart; the function the proofs are about is the function the heart
runs.
What remains is productionization, not a wall: supplying the cryptographic floor to the executor-PD from the verifier-stark PD (so the heart and the proof checker are distinct authorities), and assembling the decomposed five-PD topology above into one bootable image where each device cap lives only in its owning domain. Until that assembly lands, the demos run the heart organs one at a time — the executor-PD (real verified turn), the verifier-stark PD (real STARK), the net driver (the wire) — each a genuine seL4 boot with serial captured.
pg-dregg — your node is your Postgres
Apps need durable state that is queryable like a database and verified like a turn. pg-dregg is a PostgreSQL extension that makes reads free SQL and writes verified turns — first-class from both directions:
Caps as row-level security
An ordinary postgres-heavy app gains dregg's verified capabilities as RLS, with zero dregg infrastructure to learn beyond a token string. A policy reads dregg_admits(token, 'read', id, …) — the same decision the kernel makes, from the same token. Attenuation chains, offline delegation, time-boxing, caveats, and per-credential revocation arrive without leaking into the mental model beyond the policy line.
Postgres is a native dregg surface
State is queryable SQL: the commit log projects into tables — cells, receipts, caps, the blocklace. The explorer becomes "your capabilities, expressed as the rows you may SELECT." SDKs query through pg with the bearer token they already hold. The mirror is the store.
The discipline RLS structurally lacks
A SQL USING predicate is stateless, first-party, and non-delegable by construction — a flat session string with no token, no issuer signature, no attenuation chain to reason over. The capability properties are not "hard to write" in SQL; they are inexpressible. pg-dregg makes the verified token the policy substrate instead.
Keep going
sel4/ in the repo.