vyre_spec/
engine_invariant.rs

1//! Frozen engine-invariant identifiers used by conformance certificates.
2
3use core::fmt;
4
5/// Stable engine invariant identifier in the frozen data contract.
6///
7/// The numeric value matches the `I{N}` naming in the vyre specification.
8/// These numbers are permanent: new invariants add new variants, while
9/// existing variants never change meaning. Example: `EngineInvariant::I4`
10/// identifies the IR wire-format round-trip invariant.
11#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
12#[non_exhaustive]
13pub enum EngineInvariant {
14    /// I1 Determinism.
15    I1 = 1,
16    /// I2 Composition commutativity with lowering.
17    I2 = 2,
18    /// I3 Backend equivalence.
19    I3 = 3,
20    /// I4 IR wire-format round-trip.
21    I4 = 4,
22    /// I5 Validation soundness.
23    I5 = 5,
24    /// I6 Validation completeness, partial.
25    I6 = 6,
26    /// I7 Law monotonicity under composition.
27    I7 = 7,
28    /// I8 Reference agreement.
29    I8 = 8,
30    /// I9 Law falsifiability.
31    I9 = 9,
32    /// I10 Bounded allocation.
33    I10 = 10,
34    /// I11 No panic.
35    I11 = 11,
36    /// I12 No undefined behaviour.
37    I12 = 12,
38    /// I13 Userspace stability.
39    I13 = 13,
40    /// I14 Non-exhaustive discipline.
41    I14 = 14,
42    /// I15 Certificate stability.
43    I15 = 15,
44}
45
46/// Public alias for stable invariant identifiers.
47pub type InvariantId = EngineInvariant;
48
49impl fmt::Display for EngineInvariant {
50    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
51        write!(f, "I{}", self.ordinal())
52    }
53}
54
55impl EngineInvariant {
56    /// Stable one-based invariant number.
57    #[must_use]
58    pub const fn ordinal(&self) -> u8 {
59        match self {
60            Self::I1 => 1,
61            Self::I2 => 2,
62            Self::I3 => 3,
63            Self::I4 => 4,
64            Self::I5 => 5,
65            Self::I6 => 6,
66            Self::I7 => 7,
67            Self::I8 => 8,
68            Self::I9 => 9,
69            Self::I10 => 10,
70            Self::I11 => 11,
71            Self::I12 => 12,
72            Self::I13 => 13,
73            Self::I14 => 14,
74            Self::I15 => 15,
75        }
76    }
77
78    /// Iterate over every known invariant id in declaration order.
79    pub fn iter() -> impl Iterator<Item = Self> {
80        [
81            Self::I1,
82            Self::I2,
83            Self::I3,
84            Self::I4,
85            Self::I5,
86            Self::I6,
87            Self::I7,
88            Self::I8,
89            Self::I9,
90            Self::I10,
91            Self::I11,
92            Self::I12,
93            Self::I13,
94            Self::I14,
95            Self::I15,
96        ]
97        .into_iter()
98    }
99}
vyre_spec/engine_invariant.rs

vyre_spec/
engine_invariant.rs
