XAO invariants, version 1 (draft)¶
Status: draft, XAO version 0.2. Vectors: spec/xybern-formats-v1/vectors/invariants.json (format xao-invariants-v1).
The invariants are the properties authority must hold everywhere in the Xybern Authorisation Layer. They are defined once as pure functions over plain data and used at decision time, in Charter lint, and in the conformance suite. An implementer's checker exposes check_invariant(invariant_id, inputs) -> bool (true when the invariant holds) and must reach the expect of every vector, holds or violated.
| Id | Version | Inputs | Holds when |
|---|---|---|---|
| INV-001 no widening | 1 | child, parent (grants: action_families, scopes, argument_bounds, budgets, resources) |
Every child family is covered by a parent family (* in the parent covers all); child scopes are a subset; for every family and field the parent bounds, the child bounds it at least as tightly (max no larger, min no smaller, in a subset); every numeric budget the parent sets is set no larger in the child; every child resource pattern is covered by a parent pattern |
| INV-002 validity window | 1 | not_before, expires_at, now (ISO 8601 UTC) |
not_before <= now < expires_at; a missing bound is open |
| INV-003 revocation is final | 1 | status |
status is not one of revoked, expired, closed, inactive, killed, denied, rejected, superseded, retired |
| INV-004 principal intersection | 1 | delegate_decision, principal_decision, optional requester, resolver |
The delegate's decision is at least as strict as the principal's (allow < allow_with_warning < escalate < block), and requester != resolver |
| INV-005 arguments within bounds | 1 | grants, action_type, metadata |
For every bounded family covering the action and every bounded field: a present value satisfies max, min, in, not_in; an absent value is a violation when the bound is required (the default) |
| INV-006 resource within authority | 1 | grants.resources, resource.class |
The list is absent or contains *, or some pattern glob-matches the class (patterns may carry #instance_hash, ignored for class matching) |
| INV-007 accountable issuer | 1 | issuer |
issuer is present |
| INV-008 mission alignment | 1 | mission (spec), action_type, metadata |
No forbidden outcome's capability covers the action; the data class (metadata.data_classification) is not forbidden and, when an allowed list exists, is in it; the amount is within financial.max_single_amount; some allowed outcome's capability covers the action within its max_amount |
A finding is {"invariant", "version", "holds", "subject", "reason"}. Versions rise only when a statement changes; a stored slice names the version it was evaluated under.