vyre-conform 0.1.0

Conformance suite for vyre backends — proves byte-identical output to CPU reference
Documentation

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 vyre_conform::{certify, registry, CertificateStrength, WgslBackend};
use my_backend::MyBackend;

fn main() {
    let backend = MyBackend::new();
    let specs = registry::all_specs();

    match certify(&backend, &specs, CertificateStrength::Standard) {
        Ok(cert) => println!(
            "Santh-worthy: {} ops verified",
            cert.ops().len()
        ),
        Err(v) => {
            eprintln!("NOT conformant: {}", v);
            std::process::exit(1);
        }
    }
}

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 EnforceGate and the layer runner discovers it automatically at startup.
  • Oracle — implement Oracle and register it in the hierarchy resolver to provide an independent expected-output source for parity checks.
  • Archetype — implement Archetype to define new input-shape families for generators, composers, and witness corpora.
  • Mutation class — implement MutationClass to 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:

cargo test -p vyre-conform --test conform_self_audit_must_scream

License

This project is licensed under either of

  • Apache License, Version 2.0
  • MIT license

at your option.