Defeat plane + check, in one module

Area: Defeasible reasoning Teaches: a #[defeats] lex-specialis priority plane and a check compliance invariant composing in the same build — a check evaluates over the warranted (post-defeat) extent, so a defeated conclusion never trips it. Prerequisites: lex specialis, and check invariants (see check constraints). Run: ox build examples/legal_obligations_compose_v0 && ox run-scenario examples/legal_obligations_compose_v0

A realistic legal consumer wants both: a vocabulary’s free compliance checks and defeasible norm priority. These were once mutually exclusive — ox build refused any module carrying both a check and a #[defeats]/#[default] plane, because the static-discharge evaluator ran the strict path only and would over-fire checks on conclusions the defeat plane removes. The fix composes them on a single principle: a check is a constraint over what the program concludes, and under a defeat plane the conclusions are the warranted, post-defeat extent.

What to read in statute.ar

A lex-specialis defeat plane — the general breach norm, defeated by a force-majeure exemption per-tuple:

#[default]
#[label(general)]
pub derive obligated(o) :- Outstanding(o);

#[defeats(obligated.general(o))]
pub derive exempt(o) :- ForceMajeure(o);

A check that reads the defeasible head. UnreviewedBreach fires on an obligation that is in breach but not reviewed. It reads the warranted obligated, so it must not fire on an exempted obligation — even though that obligation is still Outstanding (the general clause’s body):

pub check UnreviewedBreach(o: Obligation) :-
    obligated(o),
    o.reviewed == false
    => Diagnostic { severity: Severity::Error, code: "Compliance::E001", … };

A transitive downstream rule joins the defeasible head. seriousBreach is a non-defeasible rule that joins obligated — it must see the warranted extent, so it does not classify a defeated (exempted) obligation as serious even when that obligation is high-value. A second check, UnescalatedSeriousBreach, reads seriousBreach, so the defeated tuple must not leak through the downstream join into a check either:

pub derive seriousBreach(o) :- obligated(o), o.highValue == true;

This is the retraction-safe path: the warranted obligated is what every downstream consumer — checks and joins alike — observes.

Running it

The scenario opens three obligations:

ob1  outstanding, not force-majeure, reviewed     → breach, no violation
ob2  outstanding, FORCE MAJEURE (exempt), UNreviewed, high-value → defeated out of obligated
ob3  outstanding, not force-majeure, reviewed     → breach, no violation

The queries report:

query statute::breaches:        2 row(s)   — warranted obligated = { ob1, ob3 }
query statute::exemptions:      1 row(s)   — { ob2 }
query statute::seriousBreaches: 0 row(s)   — no high-value warranted breach

ob2 is both force-majeure and high-value, yet it appears in neither breaches nor seriousBreaches: the defeat removes it from obligated, and that removal propagates through the downstream join. ob2 is also the one unreviewed obligation — and yet UnreviewedBreach never fires on it, precisely because the check reads the warranted obligated and the defeat already removed ob2 from it (ob1 and ob3 are reviewed, so they trip nothing either). So the scenario commits cleanly — and the reason is the lesson: a module carrying both a defeat plane and a check now builds, and the check sees only the post-defeat extent.

Honest caveats (what runs today)

• The check’s firing behavior over the warranted extent — that UnreviewedBreach fires on an unreviewed warranted breach and does not fire on the exempted (defeated-away) obligation, and likewise for the transitive seriousBreach/UnescalatedSeriousBreach chain — is exercised by separate corpus tests with unreviewed obligations, not by this clean scenario. The scenario shows the module building and running; the corpus tests show the check discriminating.

This example is compiled and run in CI; the warranted breach extent and the check-firing behavior over it (including the transitive downstream relation) are pinned by corpus tests (oxc-runtime/tests/examples_corpus.rs), so the defeat↔check composition can’t drift.