1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
//! Engine invariants — properties that composed engines must maintain.
//!
//! Individual op correctness does not imply engine correctness.
//! These invariants define what engines must guarantee beyond
//! their constituent ops being correct.
/// An invariant that an engine must maintain.
#[derive(Debug, Clone, PartialEq)]
pub enum EngineInvariant {
/// The engine produces identical results for identical inputs.
/// Violations indicate race conditions, uninitialized memory,
/// or nondeterministic scheduling.
Deterministic,
/// Every input event that should produce output does produce output.
/// No matches lost, no findings dropped, no events swallowed.
NoOutputLost,
/// No duplicate outputs for the same input event.
NoDuplicateOutput,
/// Output appears in a defined order (e.g., sorted by offset).
OutputOrdered,
/// The engine's internal stack/queue never overflows or underflows.
BoundedResources,
/// The engine terminates for all valid inputs within bounded time.
Termination,
/// Atomic operations are linearizable — concurrent access produces
/// results consistent with some sequential ordering.
AtomicLinearizable,
/// The engine produces the same result regardless of workgroup size.
/// A DFA that works at `workgroup_size=64` but breaks at `256` violates this.
WorkgroupInvariant,
/// Custom invariant with a description and check function.
Custom {
/// Human-readable name.
name: &'static str,
/// What this invariant asserts.
description: &'static str,
},
}
impl EngineInvariant {
/// Human-readable name.
///
/// The name is used as a stable key in test reports and CI annotations.
/// It must be lowercase_snake_case so that log parsers do not have to
/// handle spaces or punctuation.
#[must_use]
#[inline]
pub fn name(&self) -> &str {
match self {
Self::Deterministic => "deterministic",
Self::NoOutputLost => "no-output-lost",
Self::NoDuplicateOutput => "no-duplicate-output",
Self::OutputOrdered => "output-ordered",
Self::BoundedResources => "bounded-resources",
Self::Termination => "termination",
Self::AtomicLinearizable => "atomic-linearizable",
Self::WorkgroupInvariant => "workgroup-invariant",
Self::Custom { name, .. } => name,
}
}
}