dregg / Dragon's Egg — the technical index
a formally verified, distributed object-capability operating system. robigalia the project · dregg the kernel · deos the desktop. deos runs on dregg runs in robigalia.
The human-facing, educational site is https://www.dregg.net —
this page is the dense technical index: written for LLMs, experts, and developers, organized as
entry points into the repository at github.com/emberian/dregg.
Every link below points at a real file at
HEAD or a live surface on this site.
The full dense product site — every subsystem page with its theorem names, test counts,
and seam ledgers — lives at /deep/.
A turn is the exercise of an attenuable, proof-carrying token over owned state,
leaving a verifiable receipt.
The kernel is a Lean 4 program with machine-checked soundness, and it is the exact function
the running node executes (execFullForestG, linked via
dregg-lean-ffi/).
All proof circuits are emitted from proved Lean modules as byte-pinned descriptors; Rust authors zero
constraint semantics. Research software: the named seams below are named, there has been no
independent audit, and it is not for anything security-critical.
The model — four substances, eight verbs#
A cell is the unit of isolation and identity. Everything a cell holds is one of four substances, each with its own discipline:
- value — linear per-asset balances. An asset is its issuer cell, which carries −supply, so every asset’s sum is identically zero.
- state — a heap of programmable slots plus a nonce, guarded by the cell’s own program (a predicate over its transitions).
- authority — a capability tree (c-list) that grows only by authorized, receipt-disclosed production from held connectivity, and narrows freely.
- evidence — monotone nullifier / commitment / epoch ledgers. Birth and retirement bracket the cell lifecycle.
The kernel is eight verbs — create · write · move · grant · revoke · shield/unshield ·
lifecycle · exercise — with machine-checked minimality (each verb irreplaceable) and
completeness (they cover every effect) theorems. The catalog is generated from
VerbRegistry.lean;
nothing in it is hand-asserted. Queues, escrows, auctions, namespaces, councils, bridges, channels
are cell-program patterns over these verbs, not kernel primitives. A turn is an atomic,
capability-gated transition across one or more cells — a forest of effects with delegation edges;
delegation only attenuates (granted ≤ held). All four guard polarities — caveat, program,
precondition, intent-demand — are one Pred algebra; holding a capability means being able
to exhibit the witness that discharges its caveats.
The five guarantees + the running entry#
Stated as Lean theorems in
AssuranceCase.lean,
each pinned by #assert_axioms to exactly {propext, Classical.choice, Quot.sound},
each with non-vacuity witnesses. The reading companion is
docs/reference/lean-assurance.md.
| guarantee | theorem | statement | |
|---|---|---|---|
| A | Authority | authority_guarantee |
Every state change is justified by an unforgeable, non-amplified, fresh token chain. Production (mint) is gated on holding the issuer’s capability; the gate discriminates — it is not := True. |
| B | Conservation | conservation_guarantee · conservation_guarantee_step |
Per asset, the resource sum is identically zero on every reachable state. Under AssetId := CellId every asset is its issuer cell; mint, burn, and fees are ordinary moves against negative-capable wells. |
| C | Integrity | integrity_guarantee · integrity_guarantee_whole_turn_covered |
A receipt binds the whole post-state; circuit and executor provably produce the same receipt. Tampering a field the effect did not legitimately touch makes the turn unprovable (anti-ghost). |
| D | Freshness | freshness_guarantee |
No replay, no double-spend: a committed spend’s nullifier was fresh (in-circuit sorted-tree non-membership), revocation takes effect at finality, and a stored capability cannot outlive its grantor’s revocation (retrieval-epoch rule). |
| E | Unfoolability | unfoolability_guarantee |
A light client checking only the aggregate root learns A–D for the entire history, re-witnessing nothing; a tampered or reordered aggregate cannot bind. Conjoins light_client_verifies_whole_history with conserves_from_verification; the anti-ghost tooth is tampered_aggregate_cannot_bind. |
| R | Running entry | running_entry_sound |
A∧B∧C hold over execFullForestG itself — the exact gated function the deployed node invokes — not just an abstract model. |
| Composed apex | deployed_system_secure |
ONE theorem whose conclusion is the conjunction A ∧ B ∧ C ∧ D ∧ E over one committed running-entry forest. |
Assumed, named, never hidden. The cryptographic floor enters as typed hypotheses, never
axiom: Poseidon2 collision-resistance, BLAKE3 CR, Ed25519 EUF-CMA, HMAC/PRF,
AEAD, FRI/STARK soundness, BLS quorum certs, post-GST synchrony.
Open, named. The largest open distance from l4v-grade is the deployed-binary bridge — the
Lean→C/.a link correspondence and the wire-codec translation validation
(dregg-lean-ffi/src/marshal.rs)
are stated as obligations, not yet proven. Key-leak blast radius is bounded to the attenuation-closure of
the leaked c-list (Metatheory/KeyLeak.lean).
The open-obligation ledger is metatheory/CLAIMS.md § OPEN.
No independent audit. Not for anything security-critical.
For LLMs and machine readers#
Dense, narration-free, file:line-grounded. Read in this order.
- README-LLMs.md — the machine-facing reference: the one sentence, nouns/verbs, the architectural laws, the execution+proof architecture, the crate map, build/test/verify, working conventions for agents.
- docs/OVERVIEW.md — the whole-system what-is: model in four words, the map, where to go next.
- docs/reference/ — 23 per-subsystem references grounded to
file:lineat HEAD (index: README.md). When any other doc and a reference disagree, the reference wins. Full inventory below. - metatheory/CLAIMS.md — the axiom ledger, human half: exactly what is proved and what is not, with honesty labels (PROVED-axiom-clean / rests-on-§8-primitive / honest-OPEN).
- Dregg2/Claims.lean — the axiom ledger, machine half: the corpus-wide pin-net (165 theorem pins + 50 namespace pins); a silently-regressed keystone breaks the build at the ledger.
- Dregg2/AssuranceCase.lean — the load-bearing apex, organized by guarantee; each apex followed by
#assert_axiomson itself and its keystone DAG. - docs/KERNEL.md — the verified kernel core.
- metatheory/CONSTRUCTIVE-KNOWLEDGE.md — the conceptual spine: a capability is constructive knowledge; to hold one is to exhibit a witness that verifies.
- REORIENT.md — the architectural laws and build notes; the durable orientation record (then HORIZONLOG.md, the named-follow-up burn-down).
- docs/guide/AGENT-QUICKSTART.md — you are an agent; how to earn, spend, and run on dregg in a few lines (pay → lease → metered workload → receipts).
The reference set (docs/reference/ — Rust subsystems)
- cells.md — cells & substances: sovereign capability-secure state folded into one canonical commitment.
- turns.md —
dregg-turn: Turn → CallForest → Action → Effect, executed atomically with journaled rollback and a chained receipt. - umem.md — universal memory: the witnessed key→value store whose committed root is its boundary; six domains, per-cell heaps, umem-refs, time travel.
- services.md — cells as service objects:
InterfaceDescriptor, theinvoke()front door (noEffect::Invoke), the kvstore exemplar. - circuit.md — descriptor circuit & light client: a turn proven as a batch STARK, folded into a constant-size recursive whole-chain aggregate.
- faithful-commitment.md — the faithful state commitment: every Merkle-root component at 8-felt (~124-bit), shape-matched keystones, named residuals.
- persist.md —
dregg-persist: the node’s durable redb store; crash-consistent commit log, torn-tail recovery, the Lean-verified recover = checkpoint ⊕ overlay model. - auth.md — macaroons, biscuits & capabilities: two authorization mechanisms converging on one idea — a key may only narrow.
- node.md —
dregg-node: the federation daemon — cipherclerk host, consensus participant, localhost HTTP/WS API. - sdk.md — the SDK & embedding:
dregg-sdk(offline core) +dregg-sdk-net(networked layer). - captp.md — CapTP / promises / conditional turns: pipelining grants latency, not authority.
- deos-view.md —
deos-view: renderer extraction over one gpui-freedeos.ui.*view-tree; native and web HTML renderers. - deos-js.md — the JS scripting surface: real SpiderMonkey drives sovereign cells via cap-gated verified turns.
- cockpit.md — starbridge-v2 shell: cap-first window manager, verified-scene compositor, the shared-fork membrane, login/logout cap ceremony.
- firmament.md — firmament & seL4: one Capability handle dispatched to four backings over an emulated seL4 CNode kernel.
- wasm-web.md — wasm & in-browser deos: two cdylib crates compiling the real verified substrate to wasm32.
- dsl-apps.md —
dregg-dsl(one constraint → eight backends), the app framework (cap-gated affordances),starbridge-apps.
The reference set (docs/reference/ — Lean theory)
- lean-kernel.md — the l4v-shaped spec ⊑ design formalization: conservation algebra, the law layer, the fail-closed Exec machine, Exec ⊑ Spec.
- lean-authority.md — authority = production under non-forgeability: the attenuation algebra, credential lifecycle, the macaroon↔kernel-gate bridge.
- lean-circuit.md — circuit soundness / unfoolability: the apex
lightclient_unfoolable, per-effect refinement, whole-history aggregation, settlement soundness. - lean-conserve.md — conservation & supply: the six-color linearity law, per-domain Σδ = 0 over an arbitrary value monoid, the
conservetactics. - lean-distributed.md — distributed theory: single-machine proofs reindexed over a topology — settlement soundness at the tip, the membrane, revocation, joint turns.
- lean-assurance.md — the assurance case as a reading artifact: guarantee → keystone theorem-DAG, the
#assert_axiomshygiene mechanism, the §8 carrier floor.
For developers#
There is no public server; everything runs from a clean checkout on localhost. The verified
build needs the gitignored Lean seed archive
(scripts/fetch-lean-seed.sh fetches a prebuilt one);
a plain cargo build without it is the un-verified marshal-only node, which refuses to start
without an explicit opt-in.
- QUICKSTART.md — dregg in 15 minutes: run a node, sign a real turn, the guided demo, a governance ceremony, the site in your browser. Verified vs marshal-only explained first.
- scripts/run-node-10min.sh — the one-command path: fetch seed → build → run → report which producer mode you got.
- docs/guide/ — the developer onramp, in order: BUILD-WITH-DREGG.md (the model + your first app + the core build patterns), WHAT-YOU-CAN-BUILD.md (a gallery, each capability anchored to a runnable exemplar), DEOS-FROM-THE-WEB.md (card-worlds firing real turns over an in-tab executor), AGENT-QUICKSTART.md (the agent economy loop), SERVICE-ECONOMY-SDK.md (per-call → underlying-turn mapping), CONFINED-AGENTS.md (rent a confined, verifiable agent — an OS-jailed grain body), FEDERATION-JOIN.md (join a live federation, no genesis re-roll).
- docs/MANUAL/ — the trail guide for a person who is not the author: USER.md (use deos) · DEVELOPER.md (build the unified workspace, write a deos-js program).
- SDKs — the same shape in every language, with an inescapable authorization step (
.turn().sign().submit()): sdk/ (Rust;AgentRuntimeembeds the executor) · sdk-ts/ (TypeScript,@dregg/sdk, browser-parsable) · sdk-py/ (Python; embeds the real Lean kernel via FFI). Reference: docs/reference/sdk.md. - sdk/examples/agent_business_loop.rs — the runnable agent-economy loop: fund → lease → metered run → receipts.
- cli/ — the
dreggbinary: key management (dregg id), turns, the app-machine decoders, the guideddemo. - node/src/mcp/ — the MCP server: every AI tool-call carries a biscuit-style capability the node admits or refuses through the Lean producer gate. Manual: docs/deos/DREGG-MCP.md.
- pg-dregg/ — capabilities as PostgreSQL row-level security + durable verified workflows (
dregg_admits('read', id)is the same decision the kernel makes); the workflow spine is src/workflow.rs. - app-framework/ + starbridge-apps/ — the deos app framework (GatedAffordance, DeosApp) and the userspace apps built on it. What an app is: docs/deos/DURABLE-WORKFLOW.md (a cap-mandated, verified, durable workflow) and APPS-AS-CELLS.md.
- docs/WALKTHROUGH.md — the end-to-end tour · docs/ONBOARDING.md — contributor orientation.
- The browser doors — no install at all: the live demos on this site run the verified executor client-side in your tab.
For operators#
- docs/OPERATOR-ONBOARDING.md — from zero to a running, joined node.
- docs/guide/FEDERATION-JOIN.md — joining a federation live: candidate proposes, quorum approves, the committee advances at the next wave boundary; the
federation_idnever changes. - docs/ops/ — first-responder + lifecycle runbooks for the native deploy: MONITORING.md · INCIDENT-RESPONSE.md · KEY-MANAGEMENT.md · DISASTER-RECOVERY.md · UPGRADE.md.
- docs/BUILD-LEAN-LINKED-NODE.md — building the verified (Lean-linked) node · docs/LEAN-SEED-ARTIFACT.md — what the seed archive is and how it is produced/fetched.
- docs/deos/DEV-NODE-RUNBOOK.md — the dev-node runbook · HOMELAB-N3-RUNBOOK.md — a three-node homelab federation.
- docs/deos/SELF-HOSTING-LOOP.md — the system editing, building, and operating itself · LOG-A-HERMES-IN.md — log an agent in (the identical login ceremony with a narrower capability template).
For provers and experts#
The system itself is metatheory/
(Lean 4, library Dregg2): the eight-verb kernel, the gated executor, the circuit IR +
descriptor emission, the assurance case, the deos modeling. l4v-shaped: abstract spec → executable
design → refinement proofs. Build: cd metatheory && lake build.
- AssuranceCase.lean — the apex by guarantee (the table above) · Claims.lean — the build-enforced pin-net · CLAIMS.md — the skeptic-facing ledger.
- Dregg2/Tactics.lean —
#assert_axioms/#assert_all_clean: elaborates to an error unless the declaration’s axiom set is exactly the three standard kernel axioms · metatheory/docs/AXIOM-HYGIENE.md — the hygiene discipline. - Substrate/VerbRegistry.lean — the verb catalog source of truth (minimality + completeness are theorems, not prose).
- Spec/ExecRefinement.lean — Exec ⊑ Abstract: the abstract state is witness-free; the symbolic/full witness-mode split (turn/src/collapse.rs) is exactly what the refinement throws away.
- Dregg2/Circuit/ — the circuit IR + descriptor emission: constraints generated from proved Lean modules as byte-pinned, SHA-256-fingerprinted artifacts; the Rust prover (circuit/) interprets them and authors zero constraint semantics.
- Metatheory/KeyLeak.lean — a leaked key is a compromised principal: blast radius bounded to the attenuation-closure of the leaked c-list; the named open construction is Settlement Soundness.
- The deos models (deos adds zero new trust — every UI primitive reduces to a kernel theorem):
GatedAffordance.lean (cap-gate × state-gate buttons) ·
Transclusion.lean (provenanced citation) ·
Rehydration.lean (membranes compose
is_attenuation; a forwarded view can never amplify) · DocMerge.lean (branch-and-stitch merge correctness) · FlowRefine.lean (decidable flow refinement:decideRefines, sound and complete) · Protocol/Workflow.lean + Deos/WorkflowBridge.lean (a step is a verified turn; the surface renders the choreography, it does not fork it). - The deployment seam, in the open:
dregg-lean-ffi/ (Lean executor →
libdregg_lean.a→ the node’s C-ABI entry) · src/marshal.rs (the wire-codec translation-validation obligation) · docs/RUST-LEAN-EXECUTOR-PARITY.md (the parity gauntlet) · docs/RECEIPT-CONTRACT.md · docs/FAITHFUL-COMMITMENT-LAW.md · docs/VERIFIED-STORAGE.md. - Design corpora: docs/deos/ (the deos vision + design set: DEOS.md, HIG.md, COCKPIT-UX.md, HYPERDREGGMEDIA.md, DOCUMENT-LANGUAGE.md, SESSION-LOGIN.md, DEOS-DISTRIBUTION.md, WEB-DEOS.md, and ~150 more) · docs/design-frontiers/ · docs/desktop-os-research/ · docs/audit/ (adversarial gap audits).
Live demos on this site#
Every surface below is static and client-side: the verified executor is compiled to WebAssembly and runs in your tab — no backend, no account. A click is a real cap-gated verified turn against an in-tab ledger.
| surface | what it is |
|---|---|
| /deos/ | The deos cockpit (WebImage skin): cells, a moldable inspector, per-cell affordances, the ocap graph. Fire an authorized affordance → a verified turn commits, leaving a receipt in the log. |
| /cards/ | The deos-js card gallery — counter, reflective inspector, tally board, kv-store, and doc-collab with conflicts as first-class objects — each card a real verified turn over the in-tab executor. |
| /explorer/ | Caps-as-rows: your capabilities expressed as the rows you may read; change a token’s caveats and watch the visible rows narrow, fail-closed. The browser twin of pg-dregg’s cap-gated RLS. |
| /light-client/ | Verify a whole finalized history in ONE recursive STARK, in-tab, re-executing nothing. Ships a real pre-folded aggregate (history.json); a tampered trust anchor is refused, not laundered. The executable counterpart of guarantee E. |
| /transclusion/ | Xanadu made honest: a transcluded span is a verified dregg:// finalized read. Amend the source and the live quote follows; forge the bytes and the quote is refused with ContentHashMismatch; every quote leaves a receipt-pinned backlink. Verification lightens; nothing else does. |
| /dregg-works/ | The trustless-host front door: publish = commit blake3(page) to your cell in a receipted turn; the host serves bytes it cannot alter undetected. Embeddable scripts: verify-badge.js (re-hash the served body against the on-chain commitment) and transclude.js (carry a verified dregg:// quote on any web page). |
| /deos-viewer/ | The desktop in a link: a shared desktop is a tape (pinned instant + message sequence + claimed root), replayed through the verified executor by the reader’s own viewer — the headline is a root equality, not an image. |
| /atlas/ | The comprehension atlas: an interactive, grounded map of the whole protocol and its UI surfaces. Source + build: docs/atlas/ (vanilla HTML/CSS/JS, no build step). |
| /cockpit-gpui/ | The full native gpui renderer on a WebGPU canvas, driving the same in-tab executor. Heavier; present only when the gpui-web build resolved in this deploy. |
The repository map#
| where | what |
|---|---|
| metatheory/ | The system itself, in Lean 4 (library Dregg2): kernel, gated executor, circuit IR + descriptor emission, assurance case, deos modeling. |
| dregg-lean-ffi/ | The link: compiles the Lean executor into libdregg_lean.a and exports the entry the node calls. |
| node/ | The daemon: HTTP/MCP API, gossip + blocklace sync, block production driven by the Lean producer. |
| circuit/ | The STARK stack: the Lean-descriptor interpreter (the prover), Plonky3 (BabyBear · Poseidon2 · FRI), recursive aggregation, the light-client verifier. No hand-authored AIRs. |
| cell/ · cell-crypto/ · turn/ · wire/ | The Rust data plane: zero-crypto cell types (the four substances + programs); the crypto (notes, value-commitments, seal/stealth); turn types + executor + witness-mode/collapse; the wire codec. |
| blocklace/ · federation/ · captp/ · coord/ | The signed, equivocation-detecting, BFT-final DAG; committee machinery; capability transport (OCapN; the data plane is captp/src/data_plane.rs); coordination protocols. |
| dregg-doc/ | The document language: a Pijul-shaped patch core — changes as first-class objects, conflicts as objects, the branch-and-stitch pushout merge — plus a ropey↔patch bridge. |
| pg-dregg/ | dregg capabilities + durable verified workflows as a PostgreSQL extension (RLS + the AUTHZ → CHAIN → APPLY write spine). |
| starbridge-v2/ · starbridge-web-surface/ | deos: the native gpui cockpit embedding the real executor (src/dock/ panes, session.rs login=root-cap, powerbox.rs designate-then-attenuate) + the web-surface/affordance/rehydration stack. |
| deos-zed/ · deos-terminal/ · deos-matrix/ · deos-hermes/ | The dock apps: a code editor, a real PTY terminal, a Matrix client carrying rehydratable membranes, a ToolGateway-gated agent bridge — deos editing, building, and operating itself. |
| sdk/ · sdk-ts/ · sdk-py/ · cli/ | The three SDKs + the dregg CLI. |
| wasm/ · site/ | The in-browser executor (standalone workspace) and this site’s source (see colophon). |
| app-framework/ · starbridge-apps/ | The deos app framework + the userspace apps built on the substrate. |
| dregg-deploy/ | DreggDL, declarative deployment specs: an over-grant in a spec is caught as in-forest capability amplification before anything deploys. |
| sel4/ | The Robigalia/seL4 embedding: protection-domain crates, the Microkit assembly, the booting executor PD (the Lean kernel inside a real seL4 protection domain, under QEMU), the crypto floor. Reference: docs/reference/firmament.md. |
| discord-bot/ | Councils, real signed turns, cipherclerk macaroons — not a read-only mirror. |
| docs/ | The design documents; OVERVIEW.md is the top. |
This site#
This page and every demo surface are static files assembled by scripts/build-pages-dist.sh from site/ (source layout + build knobs: site/README.md) and deployed by the manual-dispatch pages workflow — green-or-bust: a broken wasm crate fails the deploy; nothing stale ships. The wasm executors are built from wasm/ and starbridge-v2/web/ at deploy time. The human-facing, educational site is dregg.net; this index is the machine- and expert-facing half of the split, written to be read by LLMs as much as by people.