Lease obligations: lex specialis as stratified negation
Area: Defeasible reasoning Teaches: expressing lex specialis (a specific exemption overriding a general breach norm) with stratified negation rather than the
#[defeats]directive plane — the form you reach for when a module also imports a check-bearing vocabulary. Plus a real breach calculus over an imported deontic vocabulary. Prerequisites: lex specialis via#[defeats], defeat plane + check, and cross-package vocabulary (use legal_vocab_v0::…). Run:ox build examples/legal_obligations_v0 && ox run-scenario examples/legal_obligations_v0
This is the flagship legal-obligations model: a lease creates a rent obligation running from a tenant (debtor) to a landlord (creditor), declared against the separate legal_vocab_v0 deontic vocabulary. An obligation past its due date and unperformed is in breach — unless a force-majeure exemption applies. That “unless” is lex specialis again, but written a different way than the previous two examples, and the why is the lesson.
What to read in lease.ar
Lex specialis as stratified negation. The general breach norm fires unless the specific exemption holds; the exemption lives in a strictly-lower stratum, so not exempt(o) is well-defined:
pub derive outstanding(o) :- o: RentObligation, o.performed == false, o.due < today();
pub derive exempt(o) :- o: ExemptObligation, outstanding(o);
pub derive breach(o) :- outstanding(o), not exempt(o);
The resolution is identical to the #[defeats] lex-specialis in legal_priority_v0 — the specific rule wins for exactly the exempt obligations — but expressed with negation instead of a defeat directive.
Why not #[defeats] here? This package imports the check-bearing legal_vocab_v0, and ox build refuses any module that has both a check and a #[defeats]/#[default] plane in scope (check-discharge runs the strict path only). So when a defeat plane and an imported check can’t coexist in one build, stratified negation gives the same lex-specialis resolution and composes with the vocabulary’s catalog checks. (The composing case — defeat plane and check in one module, post-fix — is legal_obligations_compose_v0.)
A second, additive breach path for a long-stale obligation, still subtracting the exemption:
pub derive breach(o) :-
o: RentObligation, o.performed == false, not exempt(o),
o.due + 365.days < today();
The force-majeure exemption protects the obligor on this path too — it is not unconditionally overridden by staleness.
A derived penalty value bound in the rule head, rate × days-late, staying in the exact numeric tower:
pub derive penaltyOwed(o, amount) :- breach(o), amount = o.rate * o.daysLate;
Running it
The scenario opens four obligations against an evaluation clock of “today”:
ob1 due 2020-01-01, unperformed, NOT exempt → breach (long-overdue path keeps it in at every clock)
ob2 due 2026-05-01, unperformed, EXEMPT → not in breach (lex specialis subtracts it)
ob3 due 2026-05-01, unperformed, NOT exempt → breach (outstanding, not exempt)
ob4 due 2026-05-01, PERFORMED → not in breach (discharged)
The queries report:
query lease::outstanding_obligations: 3 row(s) — { ob1, ob2, ob3 } (ob4 performed)
query lease::exempt_obligations: 1 row(s) — { ob2 }
query lease::breached_obligations: 2 row(s) — { ob1, ob3 } (ob2 exempt; ob4 performed)
query lease::penalties: 2 row(s) — (ob1, 1500) and (ob3, 250)
ob2 is outstanding but exempt, so the exemption subtracts it from breach on both paths — the lex-specialis point. The penalties are rate × daysLate: ob1 is 50.00 × 30 = 1500, ob3 is 25.00 × 10 = 250, both exact Decimal × Int.
Honest caveats (what runs today)
#[defeats]andcheckare mutually exclusive in one build (the wall this model documents). The canonical RFD 0028 spelling of lex specialis is the#[defeats]directive plane, proven standalone inlegal_priority_v0; it cannot be used here because this package imports a check-bearing vocabulary. Stratified negation is the composing form.- Days-late is recorded, not computed from the dates. A penalty cannot be derived from elapsed time inside a rule: there is no
Duration → Intday-count extractor, andtoday()/now()as a rule-body operand is refused with OE1316. SodaysLateis stamped as anIntat breach time (recordBreach) rather than computed fromtoday() - due.
This example is compiled and run in CI; the breach calculus over the cross-package vocabulary — the {ob1, ob3} breach extent and the 1500/250 penalties — is pinned by a CLI-pipeline test (oxc-driver/tests/cli_pipeline.rs), so the lex-specialis-via-negation behavior 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
//! `legal_obligations_v0` — a real, Sharpe-style legal-obligations model
//! authored IN Argon against the SEPARATE `legal_vocab_v0` deontic vocabulary
//! (RFD 0030). This is the v0.2.1 legal-demo forcing function: it exercises the
//! whole stack in one served package — cross-package vocabulary dependency
//! (#350), deontic metatypes + the `directed_obligation` metarel as imported
//! keywords (#311/#350), temporal `#date#` deadlines and `today()` / `+ N.days`
//! date arithmetic (#366), lex-specialis norm priority (a specific exemption
//! overriding the general breach norm), and a derived penalty value (#351) —
//! and is then SERVED over HTTP and driven through the obligation lifecycle
//! (#353; see `demo.toml` for the in-process harness and the PR transcript for
//! the served `/v1` run).
//!
//! ## The legal scenario
//!
//! A lease contract creates a rent obligation running FROM a tenant (debtor) TO
//! a landlord (creditor) — a `directed_obligation`, the deontic relation the
//! vocabulary ships. The obligation carries a `due` date (its VALID time: it
//! does not hold before the rent period begins) and a daily late penalty rate.
//! A rent obligation past its due date and unperformed is in BREACH — UNLESS a
//! force-majeure exemption applies, which OVERRIDES the general breach norm
//! (lex specialis: the specific exemption beats the general norm). An
//! obligation more than one year (365 days) past due is in breach via a
//! SECOND, independent breach path (the long-overdue path) — an additive
//! derivation that catches a long-stale obligation even when some other excuse
//! would otherwise apply, but which STILL subtracts the lex-specialis
//! exemption (`not exempt`): a force-majeure-exempt obligation is excluded from
//! breach on either path. The penalty owed on a breached obligation is a
//! DERIVED value: `rate × days-late`.
//!
//! ## What each construct proves (the canary trail)
//!
//! * `use legal_vocab_v0::{ obligation, party, directed_obligation };` — the
//! consumer never declares these introducers; it imports them from a
//! package it does not own and uses them as keywords. Cross-package vocab
//! dependency (#350) + deontic metatypes as introducers (#311/RFD 0031).
//!
//! * `RentObligation <: TimedObligation` declared with the imported
//! `obligation` keyword; `Tenant`/`Landlord <: LegalSubject` with the
//! imported `party` keyword; `owes(...)` declared with the imported
//! `directed_obligation` metarel, whose BOTH endpoints the vocabulary
//! constrains to be `party`-sorted (#311 — a directed obligation between
//! two legal subjects, verified across the boundary; the wrong-sorted
//! refusal is in `examples/legal_catalog_bad_v0`).
//!
//! * `insert iof(o, RentObligation) at due` — the obligation's membership
//! takes the VALID time of the rent period (#366 valid-time at-writes): the
//! obligation did not hold before `due`.
//!
//! * `o.due < today()` and `o.due + 365.days < today()` — breach is
//! `today()` past the due date, plus a second additive clause for a stale
//! (> 1 year / 365 days overdue) obligation. That second clause is an
//! independent breach path but still carries `not exempt(o)`, so the
//! lex-specialis exemption subtracts on it too (it does not unconditionally
//! override the exemption). `today()` reads the evaluation clock, fixed for
//! the fixpoint, and `+ N.days` is exact day-granular date arithmetic
//! (#366).
//!
//! * `breach(o) :- outstanding(o), not exempt(o)` — lex specialis as
//! stratified negation: the general breach norm fires unless the specific
//! exemption holds. See the WALL note below on why this served model does
//! NOT use the `#[defeats]` directive plane.
//!
//! * `amount = o.rate * o.daysLate` — a DERIVED computed value in a rule head
//! (#351/RFD 0029 body-level binding `=`): the late penalty owed,
//! `Decimal × Int`, staying in the exact numeric tower.
//!
//! ## Walls this package documents (see the PR wall list)
//!
//! * `#[defeats]` + `check` are mutually exclusive in one build. The
//! canonical RFD 0028 lex-specialis spelling is the `#[defeats]` directive
//! plane (proven standalone in `examples/legal_priority_v0`). This served
//! model imports the CHECK-BEARING `legal_vocab_v0`, and `ox build` refuses
//! any module that has BOTH a `check` and a `#[defeats]`/`#[default]` plane
//! in scope (check-discharge runs the strict path only and would over-fire
//! checks on defeated conclusions — `oxc-runtime/src/checks.rs`). So lex
//! specialis is expressed here with stratified negation, which composes
//! with the vocabulary's catalog checks. Filed as a FINAL-gate wall.
//!
//! * A penalty cannot be computed from elapsed time INSIDE a rule. Two
//! mechanisms block it, and neither is a `Decimal × Duration` type refusal
//! (a bare `Decimal * Duration` over a `Duration` field type-checks clean):
//! (1) there is no `Duration → Int` day-count extractor, so an elapsed
//! `Duration` cannot be turned into the `Int` multiplier the penalty needs;
//! and (2) date subtraction against the evaluation clock is not available in
//! a rule body — `today()` / `now()` inside a rule is refused with OE1316,
//! so `today() - due` cannot be formed to produce the elapsed span in the
//! first place. So `daysLate` is recorded as an `Int` at breach time
//! (`recordBreach`) rather than computed from the dates in the rule. Filed
//! as a wall (#374).
mod lease;
lease.ar
//! The lease-obligations model. See `root.ar` for the scenario and the
//! construct-by-construct canary trail.
// The deontic vocabulary's introducer keywords + upper concepts, imported
// across the package boundary (RFD 0030). The consumer declares its concepts
// WITH these keywords; it never declares the keywords themselves.
use legal_vocab_v0::{ obligation, party, directed_obligation };
use legal_vocab_v0::{ LegalSubject, Contract, TimedObligation };
// ── Parties (the legal subjects) ──
//
// `Tenant` and `Landlord` are declared with the vocabulary's `party`
// introducer and specialize its `LegalSubject` root — so both are `party`-
// sorted, which is what the `directed_obligation` metarel requires of its
// endpoints (#311). `name` is a plain ABox field.
pub party Tenant <: LegalSubject {
name: String,
}
pub party Landlord <: LegalSubject {
name: String,
}
// ── The contract (a UFO relator) ──
//
// A `Lease` is declared with the vocabulary's `legal_relator` root `Contract`:
// the relator that bundles and truthmakes the rent obligations.
pub type Lease <: Contract {
mut address: String,
}
// ── The rent obligation ──
//
// `RentObligation` is declared with the imported `obligation` keyword and
// specializes the vocabulary's `TimedObligation` root — so it inherits the
// `due: Date` deadline field and is anchored (the vocabulary's
// `OrphanObligationConcept` check, were it in scope, would NOT fire on it).
// `rate` is the daily late penalty; `daysLate` is recorded when the breach is
// observed (see the Wall note in root.ar — elapsed time cannot be computed
// inside a rule: there is no `Duration → Int` day-count extractor and `today()`
// inside a rule is refused with OE1316, so days-late is recorded as an `Int` at
// breach time rather than derived from the dates).
pub obligation RentObligation <: TimedObligation {
mut rate: Decimal,
mut daysLate: Int,
mut performed: Bool,
}
// A force-majeure exemption is a SPECIFIC kind of rent obligation: one the
// modeler has flagged as excused (a flood, a declared emergency). The
// lex-specialis exemption defeats the general breach claim.
pub type ExemptObligation <: RentObligation;
// ── The deontic relation (imported metarel) ──
//
// `owes` is declared with the imported `directed_obligation` metarel
// introducer. Its endpoints are `party`-sorted (Tenant debtor → Landlord
// creditor), satisfying the metarel's cross-package endpoint constraint (#311).
pub directed_obligation owes(mut debtor: Tenant, creditor: Landlord);
// `binds` ties an obligation to its contract (the relator's truthmaking edge).
pub rel binds(contract: Lease, ob: RentObligation);
// ════════════════════════════════════════════════════════════════════
// Breach calculus — lex specialis (a specific exemption overrides the
// general breach norm)
// ════════════════════════════════════════════════════════════════════
//
// NOTE on the priority mechanism (a documented wall — see root.ar). The
// canonical RFD 0028 spelling of lex specialis is the `#[defeats]` directive
// plane: `#[default] breach :- outstanding` defeated by
// `#[defeats(breach(o))] exempt :- ExemptObligation(o)`. That spelling is
// proven standalone in `examples/legal_priority_v0`. It CANNOT be used here:
// this package imports the check-bearing `legal_vocab_v0`, and `ox build`
// refuses any module that has BOTH a `check` and a `#[defeats]`/`#[default]`
// plane in scope (check-discharge runs the strict path only). So this served
// model expresses the SAME lex-specialis resolution with stratified negation —
// the general norm fires unless the specific exemption holds — which composes
// with the vocabulary's catalog checks. Filed as a FINAL-gate wall.
// An obligation is OUTSTANDING if it is past its due date and not yet
// performed. (`today()` parses as a comparison operand in either position —
// `o.due < today()` and `today() > o.due` are equivalent since #375.)
pub derive outstanding(o) :- o: RentObligation, o.performed == false, o.due < today();
// The EXCEPTION (lex specialis): a force-majeure exemption excuses an
// outstanding obligation. The more specific norm.
pub derive exempt(o) :- o: ExemptObligation, outstanding(o);
// The GENERAL norm, overridden by the specific exemption: an outstanding
// obligation is in breach UNLESS it is exempt (stratified negation — the
// exemption lives in a strictly-lower stratum). Lex specialis: the specific
// rule wins for exactly the exempt obligations; a non-exempt outstanding
// obligation stays in breach.
pub derive breach(o) :- outstanding(o), not exempt(o);
// The STALE-OBLIGATION clause: an obligation more than a year past due is in
// breach. This is a SECOND, independent breach path (a disjunctive head): it
// fires on a long-stale obligation even if some other excuse would otherwise
// apply, EXCEPT the lex-specialis exemption, which it still subtracts (`not
// exempt`) — a force-majeure exemption protects the obligor here. Demonstrates
// `+ N.days` exact day-granular date arithmetic (#366) as a second, additive
// derivation of the same `breach` head.
//
// Determinism over time: ob1 (due 2020-01-01) is always past `due + 365.days`,
// so this clause fires on ob1 for every evaluation clock (it is the rule that
// keeps ob1 in breach independent of the general path). The recent 2026
// obligations are protected by `not exempt` (ob2) or are already in breach via
// the general path (ob3) — so the breach extent is the same {ob1, ob3} at every
// clock past their due dates, which is the property the corpus test pins.
pub derive breach(o) :-
o: RentObligation,
o.performed == false,
not exempt(o),
o.due + 365.days < today();
// ── Derived penalty value (#351 / RFD 0029) ──
//
// The late penalty owed on a breached obligation: `rate × days-late`, a
// computed value bound in the rule head via the body-level binding `=`
// (single `=`, assignment; distinct from the `==` filter). `Decimal × Int`
// stays in the exact numeric tower.
pub derive penaltyOwed(o, amount) :- breach(o), amount = o.rate * o.daysLate;
// ════════════════════════════════════════════════════════════════════
// Obligation lifecycle — the mutations served over HTTP (#353)
// ════════════════════════════════════════════════════════════════════
//
// `openObligation` mints the obligation, the parties, and the contract over
// HTTP (entity-typed params take a symbolic name and mint a fresh individual —
// R-B5), stamps the obligation's VALID time at its `due` date (#366), and wires
// the deontic + relator edges. `recordPerformance` discharges it (no breach).
// `recordBreach` records the observed days-late (the penalty input).
pub mutate openObligation(
o: RentObligation,
contract: Lease,
tenant: Tenant,
landlord: Landlord,
address: String,
due: Date,
rate: Decimal
) {
insert iof(tenant, Tenant);
insert iof(landlord, Landlord);
insert iof(contract, Lease);
update contract: Lease set { address = address };
insert iof(o, RentObligation) at due;
update o: RentObligation set { due = due, rate = rate, daysLate = 0, performed = false };
insert owes(tenant, landlord);
insert binds(contract, o);
}
// Mark the obligation performed — it leaves the outstanding/breach set.
pub mutate recordPerformance(o: RentObligation) {
update o: RentObligation set { performed = true }
}
// Record an observed breach: stamp the days-late (the penalty multiplier).
pub mutate recordBreach(o: RentObligation, daysLate: Int) {
update o: RentObligation set { daysLate = daysLate }
}
// Flag an obligation as force-majeure exempt (reclassify into the specific
// `ExemptObligation` subtype — the lex-specialis exception).
pub mutate grantExemption(o: ExemptObligation) {
insert iof(o, ExemptObligation)
}
// ── Queries (the served read surface) ──
pub query outstanding_obligations() -> outstanding;
pub query breached_obligations() -> breach;
pub query exempt_obligations() -> exempt;
pub query penalties() -> penaltyOwed;