assert rejects: unit-testing that a constraint refuses bad data

Area: Testing Teaches: the negative-enforcement half of the test atom (§17.14). Argon is a constraint language, so a model’s most important property is which writes its invariants turn away — assert rejects { … } runs a write block against an isolated world and PASSes when the write is refused. An optional (Pkg::Code) pins the exact rejecting code. Prerequisites: refinement (where invariants); check constraints (delta guards). Run: ox test examples/assert_rejects_v0

The positive test forms — assert <expr> and assert [not] derivable — say what a model accepts or derives. They cannot say what it refuses. assert rejects { <writes> } is the missing half: it runs its block against an isolated copy of the test world, and a write-path guard rejection is a PASS (the rejected transaction commits nothing). An accepted write FAILs; a non-guard error — a typo, an unbound name — ERRORs loudly and never masquerades as a passing rejection.

What to read

The constraints under test in model.ar: a where-invariant concept (membership asserted, balance >= 0 enforced at the write with OE0668) and a check delta-guard (a new over-100t truck refused with Fleet::E001):

pub type Solvent <: Account where { self.balance >= 0 };

pub check OverweightTruck(v: Truck) :-
    v.weight > 100
    => Diagnostic { severity: Severity::Error, code: "Fleet::E001", /* … */ };

The tests in tests/mod.ar exercise each rejection mode. A where-invariant violation, a code-pinned check rejection, the same rejection without a pin, and a legal write that must NOT satisfy a rejection assertion:

test "a negative balance is rejected by the where-invariant" {
    let a = insert Solvent { balance: 100 };
    assert rejects { update a: Account set { balance = -50 } };
}

test "an overweight truck is rejected by its check, by code" {
    assert rejects(Fleet::E001) { let t = insert Truck { weight: 200 }; };
}

test "a within-limit balance is accepted" {
    let a = insert Solvent { balance: 100 };
    update a: Account set { balance = 50 };
    assert a.balance == 50;        // the positive form tests an accepted write
}

Running it

ox test discovers every test "name" { … } block, runs each against a fresh store, and reports pass/fail/error (it exits non-zero if any fails or errors — CI-usable):

$ ox test examples/assert_rejects_v0
PASS  a negative balance is rejected by the where-invariant
PASS  an overweight truck is rejected by its check, by code
PASS  an overweight truck is rejected by its check
PASS  a within-limit balance is accepted

4 passed, 0 failed, 0 errored, 0 inconclusive

The decisive contrast is the last test against the first three: setting a Solvent account to -50 is refused by the where-invariant (so assert rejects passes), but setting it to 50 is accepted — and an accepted write is tested with the positive assert a.balance == 50, never with assert rejects. The code-pinned variant passes only on its exact code: assert rejects(Fleet::E001) would FAIL, not pass, if the write were turned away by some other guard.

Honest caveats (what runs today)

• assert rejects is satisfied by a write-path guard rejection (a where-invariant OE0668 or a check delta-guard). A non-guard error inside the block (an unbound name, a type error) is an ERROR, not a PASS — the form does not let a broken test launder itself into a green rejection.
• Each block runs against an isolated copy of the test world, so a rejected transaction leaves no residue for the next test.

This example is compiled and run in CI; a CLI test (oxc-driver/tests/cli_pipeline.rs) runs ox test examples/assert_rejects_v0 and asserts it stays green, and a companion test pins that the test runner classifies every outcome (pass / fail / error), so the negative-enforcement surface can’t drift from the language.