Userspace: factories, programs, and the polis

The kernel is eight verbs; applications are everything else — and "everything else" is one pattern: a factory publishes a descriptor (a slot layout plus a Pred program), create mints a cell from it, and from that moment the executor enforces the program on every turn that touches the cell. An application's rules are substrate-enforced, not app bookkeeping; the app cannot forget to check them, because it is not the one checking.

The factory patterns

The recurring coordination shapes ship as verified factories — each one a cell program whose safety keystones are proven against the kernel:

The shape is always the same: the value at stake lives in the minted cell's own balance column (funding it is an ordinary move in; settling it is an ordinary move out — so conservation is the ordinary kernel law, with no side table), and the lifecycle is a slot governed by a Pred state machine. An escrow, concretely: OPEN settles to RELEASED under a witness gate or to REFUNDED under a time gate; both terminals are inert; double-resolution is impossible (EscrowFactory.no_double_resolve, release_requires_condition); and value can never be stranded (open_releasable / open_refundable).

The recurring services an application actually wants — lines of credit, private group channels, asynchronous mailboxes, durable storage — are named factory patterns called organs, and because they are all just Preds on a cell, they compose: one cell can wear four organs at once.

Apps inherit theorems

An app proves its contract by consuming receipts against descriptors, not by re-modeling the kernel: the Verify toolkit (Dregg2/Verify/{Contract,Frames,Tactics} and the gated variants) lets an application state "my poll's tally is monotone, one ballot one vote" and discharge it from the descriptor's constraints plus the kernel's guarantees. The runtime half mirrors the Lean half exactly: cell/src/blueprint.rs builds per-deal descriptors whose state_constraints are the verified state machines, and sdk/src/factories.rs (create_escrow_cell, release_escrow, fulfill_obligation, …) emits the corresponding turns.

The polis: governance as cells

Governance needs no kernel support, because governance is cells all the way down. The polis layer (starbridge-apps/polis) ships three cell families, each a content-addressed factory whose state_constraints ARE the machine:

• a council proposal is a cell running DRAFT → PROPOSED → {REJECTED, APPROVED → EXECUTED}: one write-once proposal hash, a monotone approval bit per member, and an AffineLe gate so certifying demands Σ approvals ≥ M in the post-state — the executor, not the operator, counts the votes; terminal states have no outgoing transition row, so no double execute;
• a constitution is a per-version cell whose parameters are pinned literals for its whole life — amendment is reissue: an amendment proposal cell stages the successor's descriptor hash as a pinned literal, demands M-of-N certification, and its ENACT step is rejected before the cooling height (TemporalGate); the receipt chain of the ceremony is the forward certification;
• a worker mandate — an orchestrator's budgeted delegation to one agent — is a cell whose budget slice IS its funded balance (overspend cannot commit: kernel conservation, not bookkeeping), whose tool scope is a pinned commitment, and whose REVOKED state is terminally inert.

A citizen can read the constitution of a polis, because it is a page of predicates, and can verify that what happened obeyed it, because the receipts say so. Legibility is a shipped surface, not a slogan: inspect_council (starbridge_polis::council) decodes a proposal cell's machine from its 8 slots, and the same decoder runs in the CLI (dregg polis council), the Discord /council-status command, and the explorer's Polis inspectors (<dregg-council> / <dregg-constitution> / <dregg-mandate>). That is the product: not a chain with apps on top, but polities whose rules are checkable by the people living under them.

Live instances

These descriptors exist tonight — generated by running the real Rust constructors, not written for this page:

Grounding

• metatheory/Dregg2/Apps/EscrowFactory.lean, ObligationFactory.lean, BridgeCell.lean — the settlement keystones (mintEscrowCell_installs_state_machine, no_double_resolve, release_conserves, settle_requires_live_target, …).
• cell/src/blueprint.rs — the runtime descriptors, with the Lean modules as their stated spec.
• sdk/src/factories.rs — the turn builders for each pattern.
• Dregg2/Substrate/VerbRegistry.lean §FACTORY-PROVENANCE — every factory pattern names the module that carries its proofs.

← 5 · The light client · The organs → · 7 · The trust boundary →