# Constraints

**In one sentence:** `constraint` expresses a mandatory relation between the
already established (facts, positions) but infers nothing: the `when`
antecedent true and the `require` requirement false is a
violated/conflicted/undetermined finding in the results, not a new fact
and not a sanction. The author takes it when a case’s coherence must be
checked without making the checked inferable.

The language specification treats a constraint as a check, not an
inference: when the antecedent holds and the requirement fails, the engine
writes a finding, adds no support, and imposes no sanction. Prohibitions —
norms with a holder, a window, and a lifecycle — live on the
[prohibitions page](/constructs/prohibition/).

## 1. When to use and when not to

| Instead | Selection rule |
|---|---|
| `constraint` vs `rule strict` | A rule infers the consequent as a new fact with support; a constraint adds no logical support. If `Y` must follow from `X`, write a rule; if a case with `X` but without `Y` is incoherent, a constraint. `X only_if Y` desugars exactly into a constraint, not into a rule |
| `constraint` vs `prohibition` | A prohibition is a norm with a holder, a window, and a lifecycle; a constraint is a validation finding without holder or window, computed on every evaluation. A prohibition’s violation is a position violation; a constraint’s failure is a finding without sanction: a sanction is encoded by a separate rule on established facts |
| `constraint` vs `definition … necessary` | A definition’s necessary half is also a constraint (“concept requires condition”) but with the `was_derived_from` provenance edge and a place in the theory. A one-off coherence condition is a bare constraint; a condition entering a concept is a definition |
| `require` vs a power’s `valid_when` | `valid_when` is an exercise-validity condition: without it the effect does not materialize. `require` is a coherence check without effect: without it nothing is extinguished, only a finding is written |

## 2. Minimal example

Package `research.constraint.enrolled_needs_consent`: a child’s enrolment requires a
guardian’s consent. Consent is inferred by a rule from a fact; the
constraint only checks coherence.

```law
rule ConsentFromGuardian strict {
    for c: Child;
    for g: Guardian;
    when consent(g, c);
    then has_consent(c);
}

constraint EnrolledNeedsConsent(c: Child) {
    when enrolled(c);
    require has_consent(c);
    severity error;
    message "зачисление требует согласия законного представителя";
}
```

Case 01 facts: `enrolled(ann)` + `consent(maria, ann)`. Query:
`evaluate truth(has_consent(ann))`.

Actual engine answer:

```text
law test research.constraint.enrolled_needs_consent: мир research.constraint.enrolled_needs_consent
  ok   [research.constraint.enrolled_needs_consent#authored] tests/01-consent-present.lawtest / urn:query:research-constraint-01
  ok   [research.constraint.enrolled_needs_consent#authored] tests/02-consent-missing.lawtest / urn:query:research-constraint-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0
```

`law engine check` — `check OK`, no warnings.

Sensitivity is double. First, removing the `consent` fact changes the answer
to the same query from Established to Not established, not refuted
(the consent-missing test): the constraint did **not** infer
`has_consent` from `enrolled` — the key property (“adds no logical
support”) visible right in the run. Second, the constraint’s own verdict
follows the verdict table: antecedent Established + requirement Established
→ satisfied (case 01, no issue), antecedent Established + requirement
Not established, not refuted → undetermined with `missing_inputs` (case 02). The `law test` output shows only query statuses —
findings live in the results with a constraint result kind,
which was not printed separately in these runs.

Second package `research.constraint.certified_needs_test` — the same device in the
standards domain with `severity warning`: certified equipment must hold a
passed test record. Case 02 (record present, certificate absent) answers
Established on the record query: the constraint is untriggered without the
antecedent and stays silent — no finding. Runs — 2/2, `check OK`.

## 3. Example by domain

- **Religion (inheritance fiqh):** package `faraid.shares` (Faraid inheritance shares, Islamic law) —
  `constraint SonImpliesMaleDescendant` (see the
  [corpus forms](/constructs/constraint/corpus-forms/)): a declared son means an inheriting male-line
  descendant; inference by rule is deliberately forbidden, otherwise
  negation on `has_male_descendant` would stop working. Exemplary “check,
  don’t infer”.
- **Standard (IFRS):** package `eu.ias.provisions` (IAS 37, provisions) —
  `constraint Para14RequiresPresentObligation`: a recognised provision
  requires a present obligation; `severity error` with an expanded `message`
  from the paragraph 14 text.
- **Custom:** package `custom.warlpiri.kinship` (Warlpiri kinship, Australian customary law) —
  `constraint WrongSkinMarriageConstraint`: Warlpiri marriage
  classes as case incoherence, not as a holder-bearing prohibition.
- **Teaching cases:** package `research.constraint.enrolled_needs_consent` (guardianship,
  `severity error`), package `research.constraint.certified_needs_test` (standard, `severity
  warning`).

## 4. How the engine answers

Table — actual runs of this section’s teaching packages (query statuses):

| Facts | Question | Answer | Why |
|---|---|---|---|
| `enrolled`, `consent` | `has_consent` | Established | rule inferred; constraint satisfied, no issue |
| `enrolled` | `has_consent` | Not established, not refuted | constraint infers nothing; its verdict is undetermined |
| `certified`, `lab_passed` | `test_passed` | Established | rule inferred; constraint satisfied |
| `lab_passed` | `test_passed` | Established | rule fires without certificate; constraint untriggered and silent |

The full verdict table (antecedent Established ×
requirement Established/Refuted/Contradiction/Not established, not refuted → satisfied/
violated/conflicted/undetermined; a conflicted antecedent →
conflicted). In 0.2 a constraint evaluates on every evaluation —
after all strata and the norm runtime, before
the answer. The result is a results element with
a constraint result kind, applicable status, and a stable
runtime id; the `constraint_check`
proof node is a graph root. A violated verdict gives issue `CONSTRAINT_VIOLATED`,
conflicted gives `CONSTRAINT_CONFLICTED`; satisfied and undetermined
produce no issue. `severity critical` is written as `error` with
`details.severity = "critical"`. These details were not printed separately
in the section’s runs and are stated from the language description.

## Grounding: which substitutions are checked

Substitutions are enumerated over the positive binding literals of the
scope-and-when conjunction. Enumeration includes atoms with Contradiction status: a
contradictory antecedent is a finding (conflicted), not a reason to hide
it. A substitution whose antecedent support pair is negative-only is untriggered
— it has no result. For an undetermined verdict, the `missing_inputs` field names
the requirement literals with Not established, not refuted status.
The implicit-established wrapper
(`require age(p)` lowers to `established(age(p))`, like a body literal)
reads four-valued — otherwise Contradiction/Not established, not refuted outcomes would not exist;
other status tests (`not_known`, `supported`, `refuted`, `unknown`) stay
boolean.

A judge in requirement: the requirement can carry the
judgment channel. On an undetermined verdict with an open judge, the
result carries an evaluation status of `REQUIRES_JUDGMENT` and
`judgment_requests` with constraint addresses;
the verdict and `missing_inputs` are unchanged.

## 5. Common mistakes

1. Expecting inference from a constraint: `require Y` does not establish
   `Y` — Not established, not refuted where the author expected Established (pitfalls,
   item 1).
2. Expecting a sanction: a constraint’s failure is a finding, a violation
   is inferred from a position instance by a separate rule
   (pitfalls, item 2).
3. A constraint as a producer: the “constraint reads what it infers” cycle —
   a constraint cannot be a producer for its strata (pitfalls, item
   3).
4. Repeated `scope`/`effective`, silently skipped body elements —
   `LDC-E1329`/`LDC-E0201` (pitfalls, item 4).
5. `effective` outside the law date: the constraint silently does not apply
   (pitfalls, item 5).
6. An unexecutable body: formulas outside the executable subset — issue
   `NON_EXECUTABLE_CONSTRAINT`, the constraint is not evaluated
   (pitfalls, item 6).

## 6. References

- Neighbour pages: [prohibitions](/constructs/prohibition/),
  [definitions](/constructs/definition/), [powers](/constructs/power/).
- The pitfalls page lists the diagnostics (`LDC-E1329`, `LDC-E0201`) with
  wrong forms and fixes.