# Engine Specifications
An `EngineSpec` defines a composed vyre engine rather than a single primitive
operation. Engines include components such as DFA execution, evaluators,
scatter pipelines, or dataflow engines. Their correctness depends on global
execution behavior, not only on the correctness of individual ops.
## Structure
An engine specification contains:
- `id`: a stable engine identifier such as `engine.dfa`.
- `description`: a human-readable statement of the engine's role.
- `invariants`: the engine properties that must hold for all valid programs.
- `cpu_fn`: an optional CPU reference for structured point comparison.
## Difference From OpSpec
`OpSpec` uses algebraic laws because primitive operations are functions with
mathematical identities. `EngineSpec` uses invariants because engines are
composed executions with scheduling, memory, ordering, and resource behavior.
An operation can be commutative or associative. An engine cannot usually be
described that way. Instead, it must preserve outputs, avoid duplicates,
terminate, respect atomics, and behave the same across valid workgroup sizes.
## Invariants
`Deterministic` means identical valid inputs produce identical output bytes on
every run. Failure indicates a race, uninitialized memory, or scheduling
dependence.
`NoOutputLost` means every input event that should produce an output does
produce one. Matches, findings, emitted records, and state transitions must not
be silently dropped.
`NoDuplicateOutput` means the engine emits each logical output at most once.
Parallel work distribution must not cause duplicate matches or repeated
records.
`OutputOrdered` means outputs appear in the defined order for that engine,
such as increasing offset or stable input order.
`BoundedResources` means internal queues, stacks, scratch buffers, and work
lists do not overflow, underflow, or grow without a specified bound.
`Termination` means every valid input completes within the engine's bounded
execution model. Infinite loops and unbounded retries are conformance failures.
`AtomicLinearizable` means concurrent atomic effects are consistent with some
sequential ordering. Return values must be values that actually existed before
the corresponding atomic operation in that order.
`WorkgroupInvariant` means changing valid workgroup size does not change the
engine's logical output. A backend that passes at size `64` and fails at size
`256` is not conforming.
## Testing
Engine conformance generates random valid programs and structured inputs from
deterministic seeds, runs them through the backend, and checks every declared
invariant. When a CPU reference exists, the suite also compares engine output
against that reference. Failing inputs are persisted as regressions and replayed
in future runs.
The engine checker must reject invalid programs during validation, not during
undefined GPU execution. For valid programs, backend errors are conformance
failures unless they are documented resource-limit errors outside the tested
configuration.