Vord

Architecture Decision Record

0010. The Vör verification contract and the edge-independence property test

Context

The constitution (ADR-0001 rule 1) is the project's reason to exist: the common authentication and authorization path MUST be satisfied by stateless cryptographic verification, never a read of the strongly-consistent core. ADR-0001 also promised that this is testable — that "has the design secretly re-monolithized?" should be a mechanical check, not a matter of opinion, mirroring Wyrd's deterministic-simulation discipline for its commit protocol (Wyrd ADR-0009).

That promise is the most important thing the project can make concrete, and it has two halves that belong together in one record: the contract of the verification plane (Vör) — narrow enough that violating rule 1 is a type error, not a code-review judgement — and the property test that proves a verification decision survives the core being gone. This ADR fixes both. It is the keystone the walking skeleton's definition of done is written against (the implementation arc), and the Vord analog of Wyrd's "the commit is proven atomic under fault injection."

Decision

1. The CredentialVerifier (Vör) contract

Define the verification seam so that a core read is unrepresentable within it:

  • Inputs: the presented token or credential; public key material (the cached JWKS, ADR-0003 / ADR-0023); a trusted clock (ADR-0033); and the cached signed status list (ADR-0005) together with its locally-persisted freshness state — the monotonic counter and last-accepted iat that ADR-0032 requires a verifier to keep. Nothing else.
  • Output: a verification decision (valid / invalid, with the verified claims), and nothing that requires a write.
  • The negative constraint is structural: the trait's signature carries no handle to the strongly-consistent core — no metadata-store client, no session store, no authoritative revocation set. A Vör implementation cannot read the core because it is never given the means to. Rule 1 is enforced by the type system at the seam, not by reviewer vigilance.

Everything Vör needs is either in the self-contained token (signatures, claims, the format version it rejects if unknown — ADR-0003) or in an edge-cached, independently-signed projection (JWKS, status list) that is itself verifiable without a core read (its integrity and freshness discipline is ADR-0043). The contract includes the algorithm discipline of ADR-0003's register: the verifier rejects alg: none, any algorithm not bound to the presented kid, and any token without a kid — signature checks never negotiate. Authorization decisions that genuinely need read-your-writes are a separate seam (the Authorizer, ADR-0006) that may present a consistency token (ADR-0004); Vör itself stays pure.

2. The edge-independence property test

The headline correctness property, asserted in deterministic simulation (madsim, per ADR-0002 and Wyrd ADR-0009) from the walking skeleton onward:

With the strongly-consistent core made unavailable, every verification decision for an already-issued, unexpired, unrevoked token completes correctly — and decisions for expired or status-list-revoked tokens still correctly fail — using only public key material, a clock, and the cached status list, for as long as those cached projections are within their freshness budgets (ADR-0032, ADR-0039).

The test makes the core disappear (partition or kill it in the simulator) and asserts Vör is unaffected. A seed that ever finds a verification path reaching for the core is committed as a permanent regression test. This is the mechanical answer to ADR-0001's "has the design re-monolithized?": if the property fails, the design has, and CI says so.

The guarantee is bounded autonomy, not indefinite autonomy. A status list or JWKS is a projection of core state; with the core down, no fresh one can be minted, and once the cached copy exceeds its max-age the edge fails closed by design (ADR-0032) — continuing to accept an arbitrarily stale list would quietly disable revocation. The core-outage survival window therefore is the projection freshness budget, published and validated as such (ADR-0039). The DST scenario asserts both phases: inside the window, verification is correct and core-independent; past it, the edge rejects rather than guesses.

3. Scope of the guarantee

Edge-independence covers verification, which is the hot path. It does not cover issuance (Modgud, ADR-0009) — minting a new token legitimately touches the core, and is allowed to fail when the core is down. That asymmetry is the constitution working as intended: the system keeps verifying (the read-dominated common case) through a core outage, and only new logins are affected. The property test asserts exactly this boundary, not more.

4. It is a warm-edge property; a cold edge fails closed

Edge-independence holds for an edge whose caches are warm — the JWKS and the status list it needs are already present. It deliberately does not promise verification from a cold edge during a core outage. A node brought up with an empty cache, or handed a token signed with a kid it has never seen (a key rotated during the outage, ADR-0023), has no public material to check the signature against and fails closed — it rejects rather than guesses. This is the safe direction: a signature cannot be verified without its key, so the only honest answer is no. The guarantee is therefore "a warm edge keeps verifying through a core outage," not "any edge verifies anything through a core outage." Warming a cold edge and learning a new kid both require the publication path (the JWKS and status-list endpoints — ADR-0023, ADR-0005, ADR-0043) to be reachable, and the freshness budgets there are the stated edges of the guarantee. The property test exercises the warm case and asserts the cold case fails closed, so the precondition is mechanical, not a footnote.

Consequences

  • Rule 1 stops being a principle one must remember and becomes a property the compiler and the simulator enforce — the single most important guardrail against the "feature gravity toward a central read" that ADR-0001 names as the standing threat.
  • The contract shapes the crate structure (ADR-0013): the Vör crate depends only on the token format and the projection caches, never on the core client, and the dependency graph makes that visible.
  • Every later feature that touches verification (MFA assurance in the token, ADR-0020; SAML reduced to edge-verifiable JWTs, ADR-0017) is validated by re-running this same property with the feature present — a standing, composable check rather than a one-time proof.
  • The freshness limits of the cached projections (how stale the status list may be, ADR-0005 / ADR-0032; key-distribution latency, ADR-0023) are the honest edges of the guarantee and are quantified in the budget registry (ADR-0039), not hidden here — and they are also the published bound on how long an edge survives a core outage before failing closed.