Reference 21 never

21. never

A top-level declaration asserting that a configuration of state is impossible — a refinement that is empty, always. It takes the ordinary predicate grammar (## Predicate expressions), or a named refinement:

never (Account where balance >= 0 and suspended)    -- "an account in good standing is never suspended"
never (Customer where referrer == this)             -- "no customer refers themselves"
never SuspendedInGoodStanding                       -- the same statement over a named refinement

requires states the same prohibition from the other side. VerifyFill requires pharmacist is LicensedPharmacist says every VerifyFill satisfies the predicate: it is never (VerifyFill where pharmacist is not LicensedPharmacist), and the compiler derives that complement when it reads the declaration — comparisons flip, and and or exchange, membership and non-membership exchange — so everything downstream sees the forbidden configuration a never would state. The subject is any shape or refinement name (ScheduleTwoPrescription requires refillsAuthorized == 0), and the predicate is the ordinary grammar with one addition: inside a requirement, membership may be spelled to be (VerifyFill requires pharmacist to be LicensedPharmacist), the sentence an owner says. to be takes a refinement name and nothing else; optionality, emptiness, and non-membership keep their one spelling (is some, is not empty, is not), and outside a requirement to be is an error. The forbidden configuration is always spelled with is, whatever the requirement wrote. The two spellings are one construct, and which to write is which sentence the owner said. A books rule is naturally a never: never (PriceChange where unitPrice < 0). A role gate on the committer has a third spelling, the act's header: transient act VerifyFill by LicensedPharmacist { ... } means by Staff plus VerifyFill requires actor to be LicensedPharmacist, one desugaring (§22, "The actor"), and the body line stays legal beside it — written when the condition is not a bare role, or when the author wants the gate as a line of its own. An agreement between fields, or a value drawn from a list, is naturally a requirement, and reads inside out as a never:

VerifyFill requires actor to be LicensedPharmacist                         -- "only a licensed pharmacist verifies" (or `by LicensedPharmacist` in the header)
FillPrescription requires filledBy to be Technician or filledBy to be Pharmacist   -- the actor, bound `as filledBy`
Fill requires fillNumber == count(prescription.fills where fillNumber <= this.fillNumber)
Staff requires role == "pharmacist" or role == "technician" or role == "admin"

The pharmacy spec writes eighteen of its forty prohibitions this way (examples/pharmacy/pharmacy.velle). A rejection quotes the declaration as the author wrote it: a requirement renders as the requirement unmet, a never as the forbidden configuration reached.

Enforced at transaction end. A never constrains the settled world — every transaction's final state — never the intermediate commits inside the envelope. A $50 deposit lands against a −$20 suspended account: at the deposit's commit the account transiently is balance >= 0 and suspended, and the restoring rule, firing as a consequence within the same transaction, settles it clean — valid. Per-commit enforcement would reject the deposit, or make its legality depend on sibling firing order, which must provably never matter (## rule, "Transactions and after commit"). The prohibition promises what the world settles to, not the path: a transition-watching rule may observe a mid-transaction pass through the configuration.

A never or a requires declares a prohibition — a requirement's prohibition is its complement — and a prohibition is one of three things, by who it binds. A refusal binds the caller: the prohibition is on a transient act (§4), it is checked once, and the record the request leaves behind carries nothing. It is checked at the door when the request's handling leaves what the predicate reads alone, and at the settled transaction otherwise ("Enforcement follows who can violate", below). A constraint binds the books: the prohibition is on a persistent shape (never (Customer where referrer == this)), it holds at the end of every transaction for as long as the record exists, and any act or tick that would leave the books otherwise is rejected. A guarantee binds the spec's own rules: only rules can produce the state (never (Account where balance >= 0 and suspended) where only rules write balance and suspended), nobody is ever refused, and the compiler proves the rules cannot reach it. A product owner's sentence usually sounds like a refusal ("turn away a spray on a halted trial"); a never on a persistent shape is always a constraint ("the records never show a spray on a halted trial"). The two are different kinds of statement with different subjects, not one rule read two ways: a refusal is about the request, binds that request, and is silent afterwards; a constraint is about the books, binds whoever would break them, and its enforcement points are derived, not chosen. One constraint, never (Shipment where order is CancelledOrder), rejects a shipment arriving for a cancelled order and a cancellation arriving for a shipped order alike, and names the shipment either way, because the shipment is the record the sentence is about; an author who means only to turn away a request writes the prohibition over a transient act (examples/shipping/shipping.velle). Where the prohibition is written decides which it is. The same business sentence, written over the transient request, binds only that request; written over the record, it binds the books for as long as the record exists. "Nobody submits an invoice with a due date in the past" is a sentence about the submission, and an invoice whose due date has passed is an ordinary state — the books hold one every time a due date passes unpaid, and the business acts on it (billing's OverdueInvoice refinement and its RemindOverdue rule, examples/billing/billing.velle). Written over the transient act, never (SubmitInvoice where dueOn < today), it is a refusal: the clock is read once, at the moment of the request, the submission is turned away, the record a rule creates from an accepted submission is never checked against it, and an invoice may age past its due date freely. Written over the record, never (Invoice where dueOn < today), it is a constraint that every invoice on the books would have to satisfy at the end of every transaction, which none can once its due date passes, and the validator refuses the declaration (checks.md V30, below). The refusal therefore needs the request and the record to be two shapes — a transient act answered by a rule that creates the record, the ordinary transient spelling of §4 (billing's BillCustomer and the OpenInvoice rule that records the Invoice from it, examples/billing/billing.velle). A prohibition written over a persistent act is a constraint, because committing a persistent act is the record (§4): there is no moment at which the sentence binds the request without also binding what it left on the books. Both placements of the invoice sentence are exhibited side by side in compiler/src/test/kotlin/velle/ValidatorTest.kt (the two V30 tests over SubmitInvoice and Invoice). A rejection is first-class information: a refusal carries the act, the records that would be in the forbidden state, the record the act was about, and the evaluation that found it, as data, with a readable message rendered from the same data; a tick's rejection carries the rule and the record it ran for in the act's place and reaches the harness as an exception (evaluation.md, "Errors, refusals, and retry" and "Ticks").

Enforcement follows who can violate. A guarantee — a prohibition whose predicate reads only rule-written data — is proven: the compiler proves it inductively over the statically-known writers — whole-spec, fail-closed — and a writer that can end a transaction inside the configuration is one connected diagnostic naming both sides: "SuspendManually can end a transaction violating never (Account where balance >= 0 and suspended) — condition the act, restore within the transaction, or retract the prohibition." A refusal or a constraint — a prohibition violable only by external acts — is enforced by rejection: no static analysis stops tomorrow's request, so its enforcement is compiled into the runtime — the transpiled code evaluates the declared nevers against external data and rejects a violating act. The transaction end is the meaning: a prohibition constrains the settled transaction, and the rejection names the act in flight. The door is where the end check can be done early with the same verdict: a prohibition whose predicate reads nothing any rule writes, creates, or deletes cannot change its verdict by the rules running, so it is evaluated once, at the act's own commit, over the state as it would stand with the act's closure landed and nothing else done, and skipped at the end. Nothing is checked twice. One spelling serves either moment: never (AssayReading where count(assay.assayReadings where hoursElapsed == this.hoursElapsed) > 1) counts the arriving reading among its siblings at the door, before any rule reads the new state, so a rule that depends on the prohibition (a latest ... by hoursElapsed over the series) never evaluates against a state the prohibition forbids, and the caller receives the refusal the author wrote rather than an error from inside a rule. A prohibition whose predicate reads what the rules move — a fill request numbered against a count the request's own handling grows — is evaluated at the end only, after the handling, and refuses the request if the settled books violate it; a sentence about the books that the request's handling makes true belongs on the record the handling produces, as a constraint (patterns.md, "Three answers to one request"). A rule that fires with nobody asking — on a schedule, or behind the after commit boundary — joins the constraint's inductive proof the way a guarantee's writers do: a record its firing creates whose shape the constraint consults is a validation error, because the firing would be refused at every tick with no caller to answer and the spec would be instructing and forbidding the same record; the discharges are a condition the prohibition cannot reach, restoring the books within the firing, or retracting the prohibition (checks.md V29, V10, V26). The clock is such a writer too: time advancing is a commit, the tick, with nobody asking, so a constraint on a persistent shape whose predicate reads today or now, directly or through a refinement it consults, is a validation error (checks.md V30). The books could age into the forbidden state with no act to refuse, and since every violating record is collected, two aged records would leave the books unrepairable from inside the system. Its discharges: state it on a transient request, where the clock is read once at the moment of the act (never (PlantTrial where trial is not PermittedTrial) in place of never (Planting where trial is not PermittedTrial)); record the decision as a field the prohibition reads instead of the clock; or retract it, when the sentence is the state the business acts on rather than a prohibition (never (Invoice where paidOn is none and dueOn < today) is an OverdueInvoice refinement and a scheduled rule). What validation never saw — a record that arrived through a legacy mapping and aged into a constraint — is still rejected at the runtime: at the next act, or thrown at the next tick. That rejection lands below the language, alongside data that can't inhabit the shape's type at all; the language declares the business fact, compilation emits the machinery (## Open / unresolved, compiled guardrails). Data arriving through a legacy mapping wasn't born behind the guardrail — a never over mapped shapes carries a validation obligation at the mapping.

An established never is a proof input. Beyond being checked, it is spent: never (Customer where referrer == this) is what lets the one-writer disjointness analysis prove that writes reached by different paths (customer.tier and customer.referrer.tier, fired by one commit) can never collide. The author states the prohibition; the prover uses it. "Established" means every derived obligation is discharged — never follows the same declare-once playbook as frozen (## Refinements, "Frozen fields"): the compiler derives an obligation per potential violator — author-side fixes for the writers of a guarantee, emitted guardrails at the boundary, validation at legacy mappings — and only a fully-discharged prohibition is spendable, so it is never merely checked and never merely assumed. How coarse the provers can be while spending prohibitions rides with the confluence calibration (OQ16).