Studio

A guided IDE for authoring dregg turns, predicates, and cell programs from the system's own vocabulary. Pick effects and constraints from the catalog, compose with guided forms (not raw JSON), see live validation and a local simulation, then submit a real turn to a node. Everything here is generated directly from the verified source — the effect set from the Lean kernel (FullActionA), the predicate language from the cell evaluator (cell/src/program.rs), the submit shapes from the node API (node/src/api.rs) — so it cannot drift from the running system.

1 Compose

Pick an effect from the catalog and fill its typed fields. Stack effects into a turn — no JSON by hand.

2 Validate

Each field is checked against the node's real submit schema. The flow won't advance until your turn is valid.

3 Simulate

See the (old → new) state diff for the parts modeled locally — and an honest "needs executor" label for the rest.

4 Submit

Send the turn to a live node and read its real accept/reject verdict. Got it — hide this.

Compose a turn from the thin-HTTP effect kinds the node accepts directly (set_field, transfer, emit_event, increment_nonce), validate it, simulate the field-write fragment, and submit it to a node. The remaining ontology effects (30 in all) go through the typed SDK signed-envelope path — browse them under Effect catalog.

A FactoryDescriptor is how the polis grows: it mints cells born with perpetual state constraints the executor enforces on every turn for the cell's whole life — the pattern that replaces whole kernel-verb families (escrow, obligation, bridge, council) with factory-born cells. Compose the constraint set with the catalog explainer inline, watch the live proof badges (substrate guarantees from the Lean assurance case; per-constraint enforcement; the source-stated limits of the grammar), then export the exact descriptor JSON the runtime deploys. The escrow / obligation / council / constitution worked examples are generated by running the real Rust constructors.

A cell guards its own state with a CellProgram built from StateConstraint predicates. The Language reference tab lists every constraint, the program kinds, and the transition guards; the Compose & test tab lets you stack constraints over an (old → new) state and watch them accept or reject — evaluated against a faithful mirror of the executor's field-comparison semantics (witness/proof constraints are honestly labeled "needs executor").

Every FullActionA effect variant: its wire mnemonic, typed arguments, one-line semantics, and the Authority.Auth facet it requires. Search and filter by category to find the effect you need.

Provenance. Effect catalog & turn composer ← metatheory/Dregg2/Exec/TurnExecutorFull.lean (FullActionA, requiredFacetA) + Dregg2/Exec/FFI.lean. Submit shapes ← node/src/api.rs (TurnEffectSpec — the JSON /api/turns/submit deserializes). Predicate language ← cell/src/program.rs, cross-checked against wasm/src/bindings.rs. Proof badges ← metatheory/Dregg2/AssuranceCase.lean (statements, keystone DAGs, #assert_axioms pins — every pin certified by Lean's own collectAxioms audit to rest only on the kernel triple). Factory worked examples ← running cell/src/blueprint.rs + starbridge-apps/polis constructors (site/tools/gen-factory-samples.sh). Regenerate with node site/tools/gen-ontology-catalog.js; a drift check (--check) fails the build if any catalog is stale. The compose / validate / simulate / author steps need no node; only submit touches the network.