vyre-conform
vyre-conform is a maintainer harness. For runtime use, consume vyre + vyre-reference + a backend (e.g. vyre-wgpu).
Conformance prover for vyre backends — binary verdict on byte-level correctness.
What this crate does
Every backend must pass certify() to ship in Santh. There is no middle ground,
no 83% passing, and no known limitations section. vyre-conform is the immune
system: it runs the full enforcement pipeline against every registered operation
and returns either a ConformanceCertificate or an actionable error. If a
backend fails a single gate on a single op, the entire verdict is Err. That
rigor is the point — at infrastructure scale, partial correctness is
indistinguishable from corruption.
The crate does not trust comments, prose specs, or manual test logs. It treats every claim as hostile evidence until the CPU reference, the algebraic law engine, the parity harness, the mutation catalog, and the adversarial gauntlet all agree. The output is an archival certificate that records the exact backend version, registry hash, witness counts, and per-operation outcomes. That certificate is the only artifact that matters when another team asks whether a backend is safe to run in production.
Quick example
use ;
use MyBackend;
The example assumes MyBackend implements WgslBackend. The registry::all_specs()
call returns the complete locked operation set. CertificateStrength::Standard
requires at least one million witnesses per declared law.
The 8-gate pipeline
Each operation is admitted through eight redundant enforcement layers. Every layer must pass for every registered op, or the certificate is withheld.
| Gate | Name | What it proves |
|---|---|---|
| L1 | Executable Spec | The cpu_fn compiles, runs, and returns the declared output shape without panics, stubs, or dead code. |
| L2 | Law Inference | Every declared algebraic law holds on exhaustive u8 and witnessed u32 probes; false laws are rejected. |
| L3 | Reference Interpreter | Backend output matches the CPU reference byte-for-byte across boundaries, equivalence classes, and generated inputs. |
| L4 | Mutation Gate | Known defect classes are killed by the test surface; surviving mutants are treated as critical bugs in the suite itself. |
| L5 | Adversarial Gauntlet | Hand-written hostile witnesses, edge cases, and regression seeds do not escape detection. |
| L6 | Stability | Repeated runs stay deterministic across seeds, sessions, and machines; any divergence is a hard failure. |
| L7 | Composition Proof | Declared operation chains agree with direct computation, end-to-end, for every registered composer. |
| L8 | Feedback Loop | Every gap test and regression case from prior findings stays fixed forever in the append-only corpus. |
Additional dedicated gates run in parallel against the same backend:
- Category A / B / C — safety classification enforcement. Category A ops are safe primitives. Category B ops are safe only under declared preconditions. Category C ops are explicitly unsafe or unsupported on some backends.
- OOB — out-of-bounds behavior, buffer init policy, and memory-sanitizer equivalence are checked on every buffer access pattern.
- Atomics — memory-ordering correctness and atomic operation soundness are validated against the reference memory model.
- Barriers — workgroup barrier uniformity and divergence checks ensure that invalid barrier placements are caught before they reach hardware.
- Wire format — exact serialization equivalence across every backend path guarantees that networked or persistent state is portable.
- Determinism — identical inputs produce identical outputs on every run, across adapters and driver versions.
- Float semantics — strict floating-point parity and approximate-track validation within declared ULP tolerance prevent silent numeric drift.
Extending conform
New capability is added in exactly one file, with zero modifications elsewhere. The discovery mechanisms are registry-scanned or module-registered, so there are no central match statements to update and no boilerplate registration files.
- Enforcement gate — implement
EnforceGateand the layer runner discovers it automatically at startup. - Oracle — implement
Oracleand register it in the hierarchy resolver to provide an independent expected-output source for parity checks. - Archetype — implement
Archetypeto define new input-shape families for generators, composers, and witness corpora. - Mutation class — implement
MutationClassto expand the adversarial catalog with new source-rewrite categories.
Community contributors can also add TOML rules, boundary witnesses, and regression
seeds without writing Rust. The rule loader ingests files from the rules/
directory and merges them into the registry at build time.
See CONTRIBUTING.md in the repository root for the full clone-to-PR path,
including TOML rule authoring, witness corpus conventions, and backend trait
implementation requirements.
Conformance levels
Levels are cumulative. A higher level implies every lower gate passed for every operation on every certificate track.
| Level | Requirement |
|---|---|
| L1 | Parity evidence — backend output matches the CPU reference for all generated inputs and boundary values. |
| L2 | Algebraic evidence — all declared laws verify on the backend under the selected witness budget with no violations. |
| L3 | Composition evidence — operation chains and engine invariants preserve end-to-end correctness for all registered composers. |
| L4 | Full certificate — all gates pass, including mutation kill, adversarial gauntlet, stability, and float semantics. |
The certificate also reports independent tracks: integer, strict float (L1f / L2f),
and approximate (L1a). A backend may be L4 on integers while still pending on
strict float ops; the certificate reports the exact proven level per track so
callers know precisely what is covered.
Self-audit
Conform ships with a meta-conformance test that walks the registry and screams when it finds missing WGSL, inapplicable laws, stub-shaped CPU references, placeholder tests, registry depth gaps, duplicate op ids, or skipped reference verification. Run it before every commit:
License
This project is licensed under either of
- Apache License, Version 2.0
- MIT license
at your option.