# Glossary
## Approximate operation
An operation explicitly declared as approximate, carrying a declared ULP
tolerance. Verified against the tolerance, not bit-exactly. Runs under the
approximate track (L1a) and is never mixed with strict operations in the
same certificate entry. Examples: `FReduceApprox`, `FSinApprox`, `RcpApprox`.
## AlgebraicLaw
An `AlgebraicLaw` is a formal mathematical property that an operation must
satisfy, such as commutativity, associativity, identity, self-inverse, or
bounded output. Laws define structural truth: they describe what kind of
function an operation is across its whole domain, not just what it returns for
one input.
## BoundaryValue
A `BoundaryValue` is an explicit input that must be tested because it lies on
an edge where bugs concentrate: zero, one, maximum values, overflow points,
shift widths, empty buffers, one-past-end indexes, and class transitions.
Boundary values are part of an `OpSpec` and are never optional coverage.
## Certificate
A `Certificate` is the structured result of running the conformance suite
against a backend. It records the backend identity, suite version, operation
versions, verification level, seeds, coverage, failures, and performance
baselines where applicable; the certificate is the conformance claim.
## Combined verification
Combined verification runs both exhaustive verification on a small complete
domain and witnessed verification on the full domain. It proves every small
case and samples the real production-width domain with deterministic witnesses,
making it the practical default for algebraic confidence.
## Conformance Level
A `Conformance Level` is a permanent named strength of verification. vyre
tracks conformance in three parallel tracks:
- **Integer track (L1-L4):** L1 is bit-exact parity on generated inputs, L2
adds algebraic verification, L3 verifies engine invariants, L4 is the full
production level with composition and performance baselines.
- **Float track (L1f-L4f):** bit-exact IEEE 754 matching against a
correctly-rounded reference, plus float algebraic laws, plus tensor engine
verification, plus ML composition proofs.
- **Approximate track (L1a):** ULP-tolerance matching for operations
explicitly declared as approximate.
Tracks are independent. A backend can achieve L4 integer and only L2f float,
or L4f float and L2 integer, or any other combination. Tracks never mix in
a single certificate entry. See `certification/levels.md` for the full
specification.
## ConformanceSuite
`ConformanceSuite` is the orchestrator that loads registered specifications,
generates deterministic inputs, dispatches backend shaders, compares GPU bytes
to CPU bytes, replays regressions, runs composition checks, and returns
failures or a publishable certificate.
## Counterexample
A `Counterexample` is a concrete input that disproves a claim. For parity it is
an input whose GPU bytes differ from CPU bytes; for a law it is a tuple such as
`a`, `b`, and `c` where the two sides of the law produce different values.
## Coverage
`Coverage` measures how much of the input space is proven or represented by the
suite. In vyre-conform it is based on equivalence classes, boundary values,
law checks, exhaustive domains, witnessed domains, and regressions, not merely
on the number of tests executed.
## CpuReferenceFn
`CpuReferenceFn` is the Rust function that defines point truth for an
operation or engine. Given input bytes, it returns the exact output bytes a
conforming backend must return; for any individual input, the CPU reference is
the specification.
## Determinism check
A `Determinism check` runs the same valid input through the same backend more
than once and requires byte-identical output each time. Failure indicates a
race, uninitialized memory, scheduling dependence, or backend nondeterminism.
## EngineSpec
`EngineSpec` defines a composed vyre engine such as a DFA, evaluator, or
scatter engine. Unlike `OpSpec`, it is centered on invariants rather than
algebraic laws because engines are stateful programs whose correctness is
defined by global behavioral guarantees.
## EquivalenceClass
An `EquivalenceClass` partitions the input space into regions that should
exercise the same semantic behavior. The suite must test at least one
representative from each class and all boundaries between classes so coverage
describes structure rather than raw sample count.
## Exhaustive verification
`Exhaustive verification` checks every value or tuple in a bounded domain,
such as every `u8` pair for a binary operation. Within that domain it is a
complete proof: no untested input exists there.
## Invariant
An `Invariant` is a property that must remain true for an engine across all
valid executions, such as deterministic output, no lost output, no duplicate
output, ordered output, bounded resources, termination, atomic linearizability,
or workgroup-size independence.
## LawViolation
A `LawViolation` is the structured report emitted when an algebraic law fails.
It records the operation, law name, concrete inputs, left-hand side, right-hand
side, and an actionable explanation that lets the backend or spec author fix
the defect.
## OpSpec
`OpSpec` is the complete specification of one vyre operation. It includes the
operation ID, signature, CPU reference function, WGSL reference fragment,
algebraic laws, equivalence classes, boundary values, comparator, calling
convention, version, and preferred conformance workgroup size.
## ParityFailure
A `ParityFailure` is a CPU-versus-backend mismatch for one generated,
boundary, regression, or composed input. It proves that the backend did not
return the bytes required by the CPU reference for that specific point query.
## Regression
A `Regression` is a previously observed failure persisted as a replayable
input. Regressions are rerun forever so a fixed bug cannot silently return and
so the suite becomes stricter as real backend failures are discovered.
## VyreBackend
`VyreBackend` is the runtime adapter implemented by each backend vendor or
project. It receives complete WGSL, input bytes, output size, and dispatch
configuration, then returns exactly the output bytes or an actionable error.
## Witness
A `Witness` is a deterministic sample from the full input domain used to
support witnessed verification. A passing witness supports the claim; a
failing witness becomes a counterexample and is persisted for regression
replay.
## Witnessed verification
`Witnessed verification` checks a deterministic set of random or adversarial
inputs in the full production domain, such as `u32`. It is not exhaustive, but
it exercises values that small-domain proofs cannot reach.