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.

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! `#[defeats]` priority + a `check` compliance invariant in one build
//! (issue #373). See `statute.ar` for the model and the expected breach
//! calculus. This package proves that the lex-specialis defeat plane and
//! catalog `check`s COMPOSE — the check evaluates over the warranted
//! (post-defeat) extent, so a defeated obligation does not trip it.

mod statute;

statute.ar

//! Lex-specialis `#[defeats]` priority AND a `check` compliance
//! invariant, in ONE module (issue #373).
//!
//! Before #373 these two features were mutually exclusive: `ox build`
//! refused any module carrying BOTH a `check` and a
//! `#[defeats]`/`#[default]` defeat plane (the static-discharge
//! evaluator ran the strict path only and would over-fire checks on
//! defeated conclusions). That blocked the realistic legal consumer —
//! one that wants the vocabulary's free `check`s AND defeasible norm
//! priority. The fix composes them: a `check` is a constraint over what
//! the program *concludes*, and under a defeat plane the conclusions are
//! the WARRANTED (post-defeat) extent. So a check evaluates over the
//! warranted set — a tuple defeated away does not trip a check that
//! would have fired on it; a surviving tuple does.
//!
//! The model — a rent-obligation breach calculus with a force-majeure
//! exemption (lex specialis) and a compliance invariant:
//!
//!   * `obligated(o)` — every outstanding obligation is in breach by
//!     default (`#[default]`, `#[label(general)]`).
//!   * `exempt(o)` — a force-majeure obligation is excused, and that
//!     exemption `#[defeats(obligated.general(o))]` the general clause
//!     for exactly the exempt obligations (per-tuple lex specialis).
//!   * `UnreviewedBreach` — a `check` compliance invariant: an
//!     obligation that is IN BREACH (warranted) but not flagged for
//!     review is a violation. It reads the WARRANTED `obligated` head,
//!     so it must NOT fire on an exempted obligation.
//!
//! Expected breach (warranted `obligated`) over the obligations below:
//!   ob1  outstanding, not exempt, reviewed     → breach, NO violation
//!   ob2  outstanding, FORCE MAJEURE (exempt)    → defeated away
//!   ob3  outstanding, not exempt, NOT reviewed  → breach + violation
//!
//!   ⇒ obligated = { ob1, ob3 };  UnreviewedBreach fires on { ob3 }

pub type Obligation {
    mut outstanding: Bool,
    mut forceMajeure: Bool,
    mut reviewed: Bool,
    mut highValue: Bool,
}

pub type Outstanding <: Obligation iff { self.outstanding == true };
pub type ForceMajeure <: Obligation iff { self.forceMajeure == true };

// General norm (overridable): an outstanding obligation is in breach by
// default — labeled so the specific exemption can name it.
#[default]
#[label (general)]
pub derive obligated(o) :- Outstanding(o);

// Lex specialis: a force-majeure obligation is exempt, and the exemption
// defeats the general breach clause for exactly the exempt obligations.
#[defeats (obligated.general(o))]
pub derive exempt(o) :- ForceMajeure(o);

// Compliance invariant (a `check`): an obligation in breach (warranted)
// that has not been flagged for review is a violation. Reads the
// post-defeat `obligated` head — an exempted obligation is NOT in
// warranted breach, so this never fires on the force-majeure case even
// though it is `Outstanding` (the general clause's body).
pub check UnreviewedBreach(o: Obligation) :-
    obligated(o),
    o.reviewed == false => Diagnostic {
        severity: Severity::Error,
        code: "Compliance::E001",
        message: "obligation in breach has not been reviewed"
    };

// A TRANSITIVE downstream relation: a high-value obligation in breach is
// a "serious" breach. This is a NON-defeasible rule that JOINS the
// defeasible `obligated` head — it must see the WARRANTED extent, so it
// does NOT classify the exempted (defeated-away) obligation as serious
// even when that obligation is high-value. This pins the retraction-safe
// recompute: the warranted `obligated` is seeded as EDB and this rule
// recomputes over it (a monotone fixpoint over the raw extent would have
// leaked the defeated tuple in).
pub derive seriousBreach(o) :- obligated(o), o.highValue == true;

// A compliance invariant over the TRANSITIVE downstream relation: a
// serious breach must be escalated. This `check` reads `seriousBreach`,
// which itself joins the defeasible `obligated` head — so the check sees
// the warranted recompute. An exempted high-value obligation is NOT a
// warranted serious breach, so this never fires on it (the retraction-
// safe path: the defeated `obligated` tuple does not leak through the
// downstream join into the check).
pub type Escalated;
pub check UnescalatedSeriousBreach(o: Obligation) :-
    seriousBreach(o),
    not Escalated(o) => Diagnostic {
        severity: Severity::Error,
        code: "Compliance::E002",
        message: "serious breach has not been escalated"
    };
pub fact Escalated(ghost);

pub mutate openObligation(
    o: Obligation,
    outstanding: Bool,
    forceMajeure: Bool,
    reviewed: Bool,
    highValue: Bool
) {
    insert iof(o, Obligation);
    update o: Obligation set {
        outstanding = outstanding,
        forceMajeure = forceMajeure,
        reviewed = reviewed,
        highValue = highValue
    }
}

pub query breaches() -> obligated;
pub query exemptions() -> exempt;
pub query seriousBreaches() -> seriousBreach;