Home / Projects / Orchestrata Ultimate / Decisions / ADR index / ADR-0010
ADR-0010: Constitutional invariants require stratified negation
| field | value |
|---|---|
| Status | Accepted |
| Date | 2026-07-23 |
| Register | factory (docs/adr, 4-digit ids) |
| Source | docs/adr/0010-constitutional-invariants-require-stratified-negation.md — permalink at bdafa201a (unchanged on master since that commit) |
| Wiki register entry | ADR-0010 (wiki status: Accepted) |
The record
- Status: Accepted
- Date: 2026-07-23
- Spec: SPEC-033 §1
Context
The layered rulebase promises that a lower layer never widens a higher one (project rules cannot
loosen the Constitution). Because rule subsumption is undecidable for unrestricted Prolog, the design
enforced this syntactically: lower layers may only touch declared extension_point/1 predicates,
checked by a meta-lint on .pl diffs.
That is unsound under negation-as-failure. NAF makes the rulebase non-monotonic: adding a clause — even one touching only sanctioned extension points — can flip a constitutional check from block to allow by supplying an alternative derivation.
Concretely: the Constitution blocks deploy unless \+ unsafe(X). A project-layer rule, using only
sanctioned extension predicates, adds a derivation making safe_override(X) succeed; a permissive
unsafe/1 consults it; unsafe(X) now fails; deploy unblocks. The meta-lint sees only extension-point
predicates touched, and passes. "Only touches extension points" (syntactic) does not entail "does not
widen an invariant" (semantic).
Decision
Constitutional invariants MUST NOT depend, via negation-as-failure, on any extension_point/1
predicate — i.e. the rulebase is stratified so that no constitutional check can be flipped by a
lower-layer addition.
The condition is on polarity, not merely on NAF: a positive dependency of a permit rule on an extension predicate also widens, and is equally disallowed.
Enforced mechanically by the stratification meta-lint (SPEC-033 B17).
Alternatives rejected
- Syntactic extension-point restriction alone — demonstrably unsound (above).
- Full semantic subsumption checking — undecidable for unrestricted Prolog; disallowed by discipline rather than attempted.
- Removing NAF from the rulebase — would remove the expressiveness that motivated Prolog.
Consequences
- Constrains how the Constitution may be written: invariants must be expressible without negative (or permit-positive) dependence on extension points. This is a real authoring restriction.
- Requires the ban on dynamic predicate construction (ADR-0025); otherwise the dependency graph the lint analyses is not statically knowable and the guarantee evaporates.
- The Constitution must ship with its own test suite (SPEC-033 B17) — an invariant nobody tests is an assertion, not a guarantee.
Provenance
Round-3 Opus, with the safe_override scenario, showing the syntactic lint passes while the invariant
is violated. Polarity refinement and the meta-predicate dependency raised in the same review.
Related ADRs
- Also mentioned: ADR-0025
Rulings cited
None.