The dregg ontology
dregg's behavior is a small, fixed vocabulary: a turn is a list of
effects, and a cell guards its own state with a
cell program built from predicate constraints.
Everything below is generated directly from the verified source by
site/tools/gen-ontology-catalog.js — the effect set from the Lean
kernel (FullActionA), the predicate language from the Rust cell
evaluator (cell/src/program.rs) — so this page cannot drift from
the system it documents.
Effects — what a turn can do
Every variant of FullActionA: its wire mnemonic, typed
arguments, one-line semantics, and the Authority.Auth facet
it requires. Search and filter by category.
Predicates — how a cell guards itself
A cell's CellProgram decides which transitions it accepts. The
Language reference tab lists every StateConstraint,
the four program kinds, and the six transition guards. The
Compose & test tab lets you model an (old → new)
8-slot state, stack constraints, 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").
metatheory/Dregg2/Exec/TurnExecutorFull.lean (FullActionA,
requiredFacetA) + Dregg2/Exec/FFI.lean
(encodeActionW wire codec). Predicate catalog ←
cell/src/program.rs (CellProgram,
StateConstraint, TransitionGuard), cross-checked
against wasm/src/bindings.rs. Regenerate with
node site/tools/gen-ontology-catalog.js; a drift check
(--check) fails the build if either catalog is stale.