ruvector-verified

Proof-carrying vector operations for Rust. Every dimension check, HNSW insert, and pipeline composition produces a machine-checked proof witness -- catching bugs that assert! misses, with less than 2% runtime overhead.

Built on lean-agentic dependent types. Part of the RuVector ecosystem.

The Problem

Vector databases silently corrupt results when dimensions mismatch. A 384-dim query against a 768-dim index doesn't panic -- it returns wrong answers. Traditional approaches either:

• Runtime assert! -- panics in production, no proof trail
• Const generics -- catches errors at compile time, but can't handle dynamic dimensions from user input, config files, or model outputs

The Solution

ruvector-verified generates formal proofs that dimensions match, types align, and pipelines compose correctly. Each proof is a replayable term -- not just a boolean check -- producing an 82-byte attestation that can be stored, audited, or embedded in RVF witness chains.

use ruvector_verified::{ProofEnvironment, prove_dim_eq, vector_types};

let mut env = ProofEnvironment::new(); // ~470ns, pre-loaded with 11 type declarations

// Prove dimensions match -- returns a reusable proof term, not just Ok/Err
let proof_id = prove_dim_eq(&mut env, 384, 384)?;   // ~500ns first call, ~15ns cached

// Wrong dimensions produce typed errors, not panics
let err = prove_dim_eq(&mut env, 384, 128);          // Err(DimensionMismatch { expected: 384, actual: 128 })

// Batch-verify 1000 vectors in ~11us (11ns per vector)
let vecs: Vec<&[f32]> = vectors.iter().map(|v| v.as_slice()).collect();
let verified = vector_types::verify_batch_dimensions(&mut env, 384, &vecs)?;
assert_eq!(verified.value, 1000);  // verified.proof_id traces back to the proof term

// Create an 82-byte attestation for audit/storage
let attestation = ruvector_verified::proof_store::create_attestation(&env, proof_id);
let bytes = attestation.to_bytes();  // embeddable in RVF witness chain (type 0x0E)

Key Capabilities

• Sub-microsecond proofs -- dimension equality in 496ns, batch verification at 11ns/vector
• Proof-carrying results -- every VerifiedOp<T> bundles the result with its proof term ID
• 3-tier gated routing -- automatically routes proofs to Reflex (<10ns), Standard (<1us), or Deep (<100us) based on complexity
• 82-byte attestations -- formal proof witnesses that serialize into RVF containers
• Thread-local pools -- zero-contention resource reuse, 876ns acquire with auto-return
• Pipeline composition -- type-safe A -> B >> B -> C stage chaining with machine-checked proofs
• Works with Vec<f32> -- no special array types required, verifies standard Rust slices

Performance

All operations benchmarked on a single core (no SIMD, no parallelism):

Overhead vs unverified operations: <2% on batch vector ingest.

Features

# Minimal: just dimension proofs
ruvector-verified = "0.1.0"

# All optimizations (recommended for production)
ruvector-verified = { version = "0.1.0", features = ["ultra"] }

# Everything
ruvector-verified = { version = "0.1.0", features = ["ultra", "all-proofs", "serde"] }

Architecture

                        +-----------------------+
                        |   ProofEnvironment    |  Pre-loaded type declarations
                        |  (symbols, cache,     |  Nat, RuVec, Eq, HnswIndex, ...
                        |   term allocator)     |
                        +-----------+-----------+
                                    |
           +------------------------+------------------------+
           |                        |                        |
   +-------v-------+    +----------v----------+    +--------v--------+
   | vector_types  |    |     pipeline        |    |  proof_store    |
   | prove_dim_eq  |    | compose_stages      |    | ProofAttestation|
   | verify_batch  |    | compose_chain       |    | 82-byte witness |
   +-------+-------+    +----------+----------+    +--------+--------+
           |                        |                        |
           +----------- gated routing (3-tier) -------------+
           |            Reflex | Standard | Deep             |
           +-------- FastTermArena (bump + dedup) ----------+
           |        ConversionCache (open-addressing)        |
           +---------- pools (thread-local reuse) ----------+

Comparison

Core API

Dimension Proofs

use ruvector_verified::{ProofEnvironment, prove_dim_eq, vector_types};

let mut env = ProofEnvironment::new();

// Prove dimensions match (returns proof term ID)
let proof_id = prove_dim_eq(&mut env, 384, 384)?;

// Verify a single vector against an index
let vector = vec![0.5f32; 384];
let verified = vector_types::verified_dim_check(&mut env, 384, &vector)?;
// verified.proof_id is the machine-checked proof

// Batch verify
let batch: Vec<&[f32]> = vectors.iter().map(|v| v.as_slice()).collect();
let batch_ok = vector_types::verify_batch_dimensions(&mut env, 384, &batch)?;
assert_eq!(batch_ok.value, vectors.len());

Pipeline Composition

use ruvector_verified::{ProofEnvironment, VerifiedStage, pipeline::compose_stages};

let mut env = ProofEnvironment::new();

// Type-safe pipeline: Embedding(384) -> Quantized(128) -> Index
let embed: VerifiedStage<(), ()> = VerifiedStage::new("embed", 0, 1, 2);
let quant: VerifiedStage<(), ()> = VerifiedStage::new("quantize", 1, 2, 3);
let composed = compose_stages(&embed, &quant, &mut env)?;
assert_eq!(composed.name(), "embed >> quantize");

Proof Attestation (82-byte Witness)

use ruvector_verified::{ProofEnvironment, proof_store};

let mut env = ProofEnvironment::new();
let proof_id = env.alloc_term();

let attestation = proof_store::create_attestation(&env, proof_id);
let bytes = attestation.to_bytes(); // exactly 82 bytes
assert_eq!(bytes.len(), 82);

// Round-trip
let recovered = ruvector_verified::ProofAttestation::from_bytes(&bytes)?;

FastTermArena (feature: fast-arena)

O(1) bump allocation with 4-wide linear probe dedup cache. Modeled after ruvector-solver's SolverArena.

use ruvector_verified::fast_arena::{FastTermArena, fx_hash_pair};

let arena = FastTermArena::with_capacity(4096);

// First intern: cache miss, allocates new term
let (id, was_cached) = arena.intern(fx_hash_pair(384, 384));
assert!(!was_cached);

// Second intern: cache hit, returns same ID in ~1.6ns
let (id2, was_cached) = arena.intern(fx_hash_pair(384, 384));
assert!(was_cached);
assert_eq!(id, id2);

// O(1) reset
arena.reset();
assert_eq!(arena.term_count(), 0);

// Statistics
let stats = arena.stats();
println!("hit rate: {:.1}%", stats.cache_hit_rate() * 100.0);

Gated Proof Routing (feature: gated-proofs)

Routes proof obligations to the cheapest sufficient compute tier. Inspired by ruvector-mincut-gated-transformer's GateController.

use ruvector_verified::{ProofEnvironment, gated::{route_proof, ProofKind, ProofTier}};

let env = ProofEnvironment::new();

// Reflexivity -> Reflex tier (~1.2ns)
let decision = route_proof(ProofKind::Reflexivity, &env);
assert!(matches!(decision.tier, ProofTier::Reflex));

// Dimension equality -> Reflex tier (literal comparison)
let decision = route_proof(
    ProofKind::DimensionEquality { expected: 384, actual: 384 },
    &env,
);
assert_eq!(decision.estimated_steps, 1);

// Long pipeline -> Deep tier (full kernel)
let decision = route_proof(
    ProofKind::PipelineComposition { stages: 10 },
    &env,
);
assert!(matches!(decision.tier, ProofTier::Deep));

Tier latency targets:

ConversionCache

Open-addressing conversion result cache with FxHash. Modeled after ruvector-mincut's PathDistanceCache.

use ruvector_verified::cache::ConversionCache;

let mut cache = ConversionCache::with_capacity(1024);

cache.insert(/* term_id */ 0, /* ctx_len */ 384, /* result_id */ 42);
assert_eq!(cache.get(0, 384), Some(42));

let stats = cache.stats();
println!("hit rate: {:.1}%", stats.hit_rate() * 100.0);

Thread-Local Pools

Zero-contention resource reuse via Drop-based auto-return.

use ruvector_verified::pools;

{
    let resources = pools::acquire(); // ~876ns
    // resources.env: fresh ProofEnvironment
    // resources.scratch: reusable HashMap
} // auto-returned to pool on drop

let (acquires, hits, hit_rate) = pools::pool_stats();

Verified HNSW operations that prove dimensionality and metric compatibility before allowing insert/query.

use ruvector_verified::{ProofEnvironment, vector_types};

let mut env = ProofEnvironment::new();

// Prove insert preconditions
let vector = vec![1.0f32; 384];
let verified = vector_types::verified_insert(&mut env, 384, &vector, "L2")?;
assert_eq!(verified.value.dim, 384);
assert_eq!(verified.value.metric, "L2");

// Build typed index type term
let index_type = vector_types::mk_hnsw_index_type(&mut env, 384, "Cosine")?;

All errors are typed via VerificationError:

use ruvector_verified::error::VerificationError;

match result {
    Err(VerificationError::DimensionMismatch { expected, actual }) => {
        eprintln!("vector has {actual} dimensions, index expects {expected}");
    }
    Err(VerificationError::TypeCheckFailed(msg)) => {
        eprintln!("type check failed: {msg}");
    }
    Err(VerificationError::ConversionTimeout { max_reductions }) => {
        eprintln!("proof too complex: exceeded {max_reductions} steps");
    }
    Err(VerificationError::ArenaExhausted { allocated }) => {
        eprintln!("arena full: {allocated} terms");
    }
    _ => {}
}

Error variants: DimensionMismatch, TypeCheckFailed, ProofConstructionFailed, ConversionTimeout, UnificationFailed, ArenaExhausted, DeclarationNotFound, AttestationError

ProofEnvironment::new() pre-registers these domain types:

# All benchmarks
cargo bench -p ruvector-verified --features "ultra,hnsw-proofs"

# Quick run
cargo bench -p ruvector-verified --features "ultra,hnsw-proofs" -- --quick

# Specific group
cargo bench -p ruvector-verified --features ultra -- "prove_dim_eq"

Sample output (AMD EPYC, single core):

prove_dim_eq/384          time:   [496 ns]
mk_vector_type/384        time:   [503 ns]
ProofEnvironment::new     time:   [466 ns]
pool_acquire_release      time:   [876 ns]
env_reset                 time:   [379 ns]
cache_lookup_1000_hits    time:   [9.6 us]
attestation_roundtrip     time:   [<1 ns]

See examples/rvf-kernel-optimized for a complete example that combines:

• Verified vector ingest with dimension proofs
• Linux kernel + eBPF embedding into RVF containers
• 3-tier gated proof routing
• FastTermArena dedup with 99%+ cache hit rate
• 82-byte proof attestations in the RVF witness chain

cargo run -p rvf-kernel-optimized
cargo test -p rvf-kernel-optimized
cargo bench -p rvf-kernel-optimized

Minimum Supported Rust Version

1.77

License

MIT OR Apache-2.0