Worked examples, walkable
The eight real applications from the Build page, each opened
up: what it does, the cell slots it lays out, the
constraints that make its rules unbreakable, the
turns that drive it — and a live try-it against a node. Every
structural fact below is read straight from the app's manifest.json, which
is generated from the Rust source of truth; nothing here is hand-maintained narrative
except the plain-language description of each rule.
The vocabulary of a guarantee
A dregg app does not enforce its own rules in application code. It mints generic constraints onto a factory-born cell at birth, and the executor refuses any turn that would violate them. The same small vocabulary appears across every app:
- WriteOnce
- a slot may be written once, then is frozen forever
- Immutable
- a slot is fixed at birth and may never be written
- Monotonic
- a slot’s value may only ever increase
- StrictMonotonic
- a slot must strictly increase on each write — no re-entry
- MonotonicSequence
- a counter that advances by exactly one, in order
- FieldLteField
- one slot must always stay ≤ another (an invariant pair)
- SenderAuthorized
- only a sender authorized by a public root may write
These constraints have a Lean semantics and the executor that checks them refines that spec — see verified guarantees for the full effect and constraint catalogs (generated from the Lean source, drift-guarded).
The userspace stance
Every app on this page is buildable from dregg-native primitives only — the answer to “I need a custom rule” is never a new effect, it is the generic Caveat, StateConstraint, Authorization, or Factory you would compose it from. The nameservice app is the documented paint-by-numbers exemplar; the building-apps guide walks the pattern.