ruvector_verified/
error.rs

1//! Verification error types.
2//!
3//! Maps lean-agentic kernel errors to RuVector verification errors.
4
5use thiserror::Error;
6
7/// Errors from the formal verification layer.
8#[derive(Debug, Error)]
9pub enum VerificationError {
10    /// Vector dimension does not match the index dimension.
11    #[error("dimension mismatch: expected {expected}, got {actual}")]
12    DimensionMismatch {
13        expected: u32,
14        actual: u32,
15    },
16
17    /// The lean-agentic type checker rejected the proof term.
18    #[error("type check failed: {0}")]
19    TypeCheckFailed(String),
20
21    /// Proof construction failed during term building.
22    #[error("proof construction failed: {0}")]
23    ProofConstructionFailed(String),
24
25    /// The conversion engine exhausted its fuel budget.
26    #[error("conversion timeout: exceeded {max_reductions} reduction steps")]
27    ConversionTimeout {
28        max_reductions: u32,
29    },
30
31    /// Unification of proof constraints failed.
32    #[error("unification failed: {0}")]
33    UnificationFailed(String),
34
35    /// The arena ran out of term slots.
36    #[error("arena exhausted: {allocated} terms allocated")]
37    ArenaExhausted {
38        allocated: u32,
39    },
40
41    /// A required declaration was not found in the proof environment.
42    #[error("declaration not found: {name}")]
43    DeclarationNotFound {
44        name: String,
45    },
46
47    /// Ed25519 proof signing or verification failed.
48    #[error("attestation error: {0}")]
49    AttestationError(String),
50}
51
52/// Convenience type alias.
53pub type Result<T> = std::result::Result<T, VerificationError>;
54
55#[cfg(test)]
56mod tests {
57    use super::*;
58
59    #[test]
60    fn error_display_dimension_mismatch() {
61        let e = VerificationError::DimensionMismatch { expected: 128, actual: 256 };
62        assert_eq!(e.to_string(), "dimension mismatch: expected 128, got 256");
63    }
64
65    #[test]
66    fn error_display_type_check() {
67        let e = VerificationError::TypeCheckFailed("bad term".into());
68        assert_eq!(e.to_string(), "type check failed: bad term");
69    }
70
71    #[test]
72    fn error_display_timeout() {
73        let e = VerificationError::ConversionTimeout { max_reductions: 10000 };
74        assert_eq!(e.to_string(), "conversion timeout: exceeded 10000 reduction steps");
75    }
76
77    #[test]
78    fn error_display_arena() {
79        let e = VerificationError::ArenaExhausted { allocated: 42 };
80        assert_eq!(e.to_string(), "arena exhausted: 42 terms allocated");
81    }
82
83    #[test]
84    fn error_display_attestation() {
85        let e = VerificationError::AttestationError("sig invalid".into());
86        assert_eq!(e.to_string(), "attestation error: sig invalid");
87    }
88}
ruvector_verified/error.rs

ruvector_verified/
error.rs
