ruvector_verified/
invariants.rs

1//! Pre-built invariant library.
2//!
3//! Registers RuVector's core type declarations into a lean-agentic
4//! proof environment so that verification functions can reference them.
5
6/// Well-known symbol names used throughout the verification layer.
7pub mod symbols {
8    pub const NAT: &str = "Nat";
9    pub const RUVEC: &str = "RuVec";
10    pub const EQ: &str = "Eq";
11    pub const EQ_REFL: &str = "Eq.refl";
12    pub const DISTANCE_METRIC: &str = "DistanceMetric";
13    pub const L2: &str = "DistanceMetric.L2";
14    pub const COSINE: &str = "DistanceMetric.Cosine";
15    pub const DOT: &str = "DistanceMetric.Dot";
16    pub const HNSW_INDEX: &str = "HnswIndex";
17    pub const INSERT_RESULT: &str = "InsertResult";
18    pub const PIPELINE_STAGE: &str = "PipelineStage";
19    pub const TYPE_UNIVERSE: &str = "Type";
20}
21
22/// Pre-registered type declarations available after calling `register_builtins`.
23///
24/// These mirror the RuVector domain:
25/// - `Nat` : Type (natural numbers for dimensions)
26/// - `RuVec` : Nat -> Type (dimension-indexed vectors)
27/// - `Eq` : {A : Type} -> A -> A -> Type (propositional equality)
28/// - `Eq.refl` : {A : Type} -> (a : A) -> Eq a a (reflexivity proof)
29/// - `DistanceMetric` : Type (L2, Cosine, Dot)
30/// - `HnswIndex` : Nat -> DistanceMetric -> Type
31/// - `InsertResult` : Type
32/// - `PipelineStage` : Type -> Type -> Type
33pub fn builtin_declarations() -> Vec<BuiltinDecl> {
34    vec![
35        BuiltinDecl { name: symbols::NAT, arity: 0, doc: "Natural numbers" },
36        BuiltinDecl { name: symbols::RUVEC, arity: 1, doc: "Dimension-indexed vector" },
37        BuiltinDecl { name: symbols::EQ, arity: 2, doc: "Propositional equality" },
38        BuiltinDecl { name: symbols::EQ_REFL, arity: 1, doc: "Reflexivity proof" },
39        BuiltinDecl { name: symbols::DISTANCE_METRIC, arity: 0, doc: "Distance metric enum" },
40        BuiltinDecl { name: symbols::L2, arity: 0, doc: "L2 Euclidean distance" },
41        BuiltinDecl { name: symbols::COSINE, arity: 0, doc: "Cosine distance" },
42        BuiltinDecl { name: symbols::DOT, arity: 0, doc: "Dot product distance" },
43        BuiltinDecl { name: symbols::HNSW_INDEX, arity: 2, doc: "HNSW index type" },
44        BuiltinDecl { name: symbols::INSERT_RESULT, arity: 0, doc: "Insert result type" },
45        BuiltinDecl { name: symbols::PIPELINE_STAGE, arity: 2, doc: "Typed pipeline stage" },
46    ]
47}
48
49/// A built-in type declaration to register in the proof environment.
50#[derive(Debug, Clone)]
51pub struct BuiltinDecl {
52    /// Symbol name.
53    pub name: &'static str,
54    /// Number of type parameters.
55    pub arity: u32,
56    /// Documentation.
57    pub doc: &'static str,
58}
59
60/// Register all built-in RuVector types into the proof environment's symbol table.
61///
62/// This is called once during `ProofEnvironment::new()` to make domain types
63/// available for proof construction.
64pub fn register_builtin_symbols(symbols: &mut Vec<String>) {
65    for decl in builtin_declarations() {
66        if !symbols.contains(&decl.name.to_string()) {
67            symbols.push(decl.name.to_string());
68        }
69    }
70}
71
72#[cfg(test)]
73mod tests {
74    use super::*;
75
76    #[test]
77    fn builtin_declarations_complete() {
78        let decls = builtin_declarations();
79        assert!(decls.len() >= 11, "expected at least 11 builtins, got {}", decls.len());
80    }
81
82    #[test]
83    fn all_builtins_have_names() {
84        for decl in builtin_declarations() {
85            assert!(!decl.name.is_empty());
86            assert!(!decl.doc.is_empty());
87        }
88    }
89
90    #[test]
91    fn register_symbols_no_duplicates() {
92        let mut syms = vec!["Nat".to_string()]; // pre-existing
93        register_builtin_symbols(&mut syms);
94        let nat_count = syms.iter().filter(|s| *s == "Nat").count();
95        assert_eq!(nat_count, 1, "Nat should not be duplicated");
96    }
97
98    #[test]
99    fn symbol_constants_valid() {
100        assert_eq!(symbols::NAT, "Nat");
101        assert_eq!(symbols::RUVEC, "RuVec");
102        assert_eq!(symbols::EQ_REFL, "Eq.refl");
103    }
104}
ruvector_verified/invariants.rs

ruvector_verified/
invariants.rs
