Skip to content

SOUNDNESS.md

Latest commit

 

History

History
1227 lines (997 loc) · 53.9 KB

SOUNDNESS.md

File metadata and controls

1227 lines (997 loc) · 53.9 KB
Raw

VelesDB Soundness Documentation

Purpose: Enable Rust senior reviewers to audit unsafe code without reading the entire codebase. Last Updated: 2026-06-12 (full production unsafe audit — 34 source files; inventory: grep -rlE 'unsafe (\{|fn|impl)' crates/velesdb-core/src --include='*.rs', test-only files excluded)

Table of Contents

  1. Overview
  2. SIMD Intrinsics
  3. Memory Allocation
  4. Memory-Mapped I/O
  5. Pointer Operations
  6. HNSW Graph Unsafe Operations
  7. API-Contract unsafe (No UB)
  8. Concurrency
  9. FFI Boundaries
  10. Soundness Checklist

Overview

VelesDB uses unsafe code in the following categories:

Category Purpose Files
SIMD (consolidated) AVX-512/AVX2/NEON distance kernels simd_native/x86_avx512.rs, simd_native/x86_avx2/, simd_native/x86_avx2_similarity.rs, simd_native/neon.rs, simd_neon.rs
SIMD (dispatch) Runtime feature detection + dispatch to ISA kernels simd_native/dispatch/ (mod.rs, dot.rs, euclidean.rs, cosine.rs, hamming.rs)
SIMD (reduction) Horizontal sum helpers for accumulator registers simd_native/reduction.rs
SIMD (ADC) Asymmetric Distance Computation for PQ search simd_native/adc.rs
SIMD (RaBitQ) AVX-512 VPOPCNTDQ for binary Hamming distance simd_native/x86_avx512.rs (kernels consolidated; quantization/rabitq*.rs contains no unsafe)
SIMD (trigram) AVX2/AVX-512 trigram extraction index/trigram/simd.rs
SIMD (bench helpers) Direct kernel calls behind runtime feature detection internal_bench.rs
Prefetch (x86) Software prefetch hints (_mm_prefetch) simd_native/prefetch.rs, perf_optimizations.rs
Prefetch (ARM64) Inline ASM prfm instructions simd_neon_prefetch.rs
Alloc Custom aligned allocations + RAII perf_optimizations.rs, alloc_guard.rs, contiguous_ops.rs, contiguous_resize.rs
Mmap Memory-mapped file I/O storage/mmap.rs, storage/mmap_capacity.rs, storage/mmap/wal_replay.rs, storage/guard.rs
Pointers Raw pointer operations for performance storage/vector_bytes.rs, storage/compaction.rs
HNSW unchecked get_unchecked on hot-path vector access index/hnsw/native/graph/neighbors.rs, search.rs, search_state.rs
HNSW drop order ManuallyDrop::drop for field ordering index/hnsw/index/mod.rs, index/hnsw/index/vacuum.rs
Send/Sync Manual Send/Sync impls index/hnsw/native_inner.rs, simd_native/dispatch/mod.rs
API-contract marker unsafe fn flagging a logical (not memory) contract collection/any_collection.rs
FFI Python (PyO3), WASM, Mobile bindings velesdb-python/, velesdb-wasm/, velesdb-mobile/

The former MaybeUninit graph-edge memory pool (collection/graph/memory_pool/) has been removed from the codebase; its section was dropped from this audit accordingly.

SIMD Intrinsics

Module: crates/velesdb-core/src/simd_native/x86_avx512.rs

Functions (all unsafe fn with #[target_feature(enable = "avx512f")]):

  • dot_product_avx512() / dot_product_avx512_4acc() / dot_product_avx512_8acc()
  • squared_l2_avx512() / squared_l2_avx512_4acc() / squared_l2_avx512_8acc()
  • cosine_fused_avx512() / cosine_fused_avx512_4acc() / cosine_fused_avx512_8acc()
  • hamming_avx512() / hamming_avx512_4acc() - Hamming distance on f32 vectors
  • jaccard_avx512() / jaccard_avx512_4acc() / jaccard_avx512_8acc()
  • hamming_binary_avx512() / hamming_binary_avx512_vpopcntdq() - Binary Hamming

Invariants:

  1. #[target_feature(enable = "avx512f")] enforces CPU feature at function level
  2. Runtime feature detection via simd_level() ALWAYS precedes the call
  3. a.len() == b.len() is asserted in the public dispatch API
  4. Unaligned loads (_mm512_loadu_ps) used throughout - no alignment requirement
  5. Masked remainder handling via _mm512_maskz_loadu_ps for tail elements
  6. Multi-accumulator variants (4-acc, 8-acc) use ILP to hide FMA latency

Modules: crates/velesdb-core/src/simd_native/x86_avx2/dot.rs and simd_native/x86_avx2/l2.rs

Functions (all unsafe fn with #[target_feature(enable = "avx2,fma")]):

  • dot_product_avx2() / dot_product_avx2_1acc() / dot_product_avx2_4acc()
  • squared_l2_avx2() / squared_l2_avx2_1acc() / squared_l2_avx2_4acc()
  • dot_avx2_remainder() / dot_avx2_tail_under16() - remainder handling

Invariants:

  1. #[target_feature(enable = "avx2,fma")] enforces CPU features
  2. Pointer arithmetic bounded by a.len() (loop end pointer = a.as_ptr().add(len))
  3. Unaligned loads via _mm256_loadu_ps
  4. Remainder loops handle len % (4*8) or len % 8 elements safely

Module: crates/velesdb-core/src/simd_native/x86_avx2_similarity.rs

Functions (all unsafe fn with #[target_feature(enable = "avx2,fma")]):

  • cosine_fused_avx2() / cosine_fused_avx2_2acc() - Fused cosine similarity
  • hamming_avx2() - Hamming distance (f32 vectors)
  • hamming_binary_avx2() - Binary Hamming distance (u64 vectors)
  • jaccard_avx2() - Jaccard similarity
  • Helper functions: cosine_avx2_remainder(), hamming_avx2_fp_acc(), jaccard_avx2_remainder()

Invariants: Same as AVX2 dot/L2 above. hamming_binary_avx2 operates on &[u64] slices with popcount via _mm256_set_epi8 LUT.

Module: crates/velesdb-core/src/simd_native/neon.rs

Functions (all unsafe fn with #[target_feature(enable = "neon")], #[cfg(target_arch = "aarch64")]):

  • dot_product_neon() / squared_l2_neon() / cosine_neon() / hamming_neon()
  • jaccard_neon() / hamming_binary_neon()
  • Safe wrappers: dot_product_neon_safe(), euclidean_neon_safe(), etc.

Invariants:

  1. #[cfg(target_arch = "aarch64")] guarantees NEON availability (mandatory on AArch64)
  2. debug_assert_eq!(a.len(), b.len()) at function entry
  3. Loop bounds chunks = len / 4 ensure pointer arithmetic stays in bounds
  4. Unrolled remainder handles len % 4 elements via scalar indexing

Why It's Sound:

// SAFETY: NEON load and FMA require in-bounds pointers.
// - Condition 1: Loop invariant `offset + 4 <= chunks * 4 <= len`.
// - Condition 2: `a` and `b` have equal length (debug assertion).
let va = vld1q_f32(a.as_ptr().add(offset));
let vb = vld1q_f32(b.as_ptr().add(offset));
sum = vfmaq_f32(sum, va, vb);

Module: crates/velesdb-core/src/simd_neon.rs

Standalone NEON implementations (same pattern as simd_native/neon.rs). Contains dot_product_neon, euclidean_squared_neon, cosine_neon, cosine_normalized_neon with identical invariant structure.

Module: crates/velesdb-core/src/simd_native/dispatch/ (5 files)

Files:

  • simd_native/dispatch/mod.rs — unsafe impl Send/Sync for DistanceEngine
  • simd_native/dispatch/dot.rs — Dot product dispatch to AVX-512/AVX2/scalar
  • simd_native/dispatch/euclidean.rs — Euclidean/L2 dispatch + scale_inplace_avx2
  • simd_native/dispatch/cosine.rs — Cosine similarity dispatch
  • simd_native/dispatch/hamming.rs — Hamming/Jaccard/binary Hamming dispatch

Pattern: Each dispatch function checks simd_level() (cached runtime detection) and calls the appropriate unsafe target-featured kernel.

pub fn dot_product_native(a: &[f32], b: &[f32]) -> f32 {
    assert_eq!(a.len(), b.len());
    match simd_level() {
        SimdLevel::Avx512 if a.len() >= 1024 =>
            // SAFETY: simd_level() confirmed AVX-512F support.
            unsafe { dot_product_avx512_8acc(a, b) },
        // ...
    }
}

dispatch/mod.rs: Contains unsafe impl Send/Sync for DistanceEngine.

// SAFETY: DistanceEngine stores only function pointers and a usize dimension.
// - Condition 1: Function pointers are Copy + Send + Sync.
// - Condition 2: usize is a primitive with no interior mutability.
unsafe impl Send for DistanceEngine {}
unsafe impl Sync for DistanceEngine {}

dispatch/euclidean.rs: Contains unsafe fn scale_inplace_avx2() for in-place vector normalization using _mm256_mul_ps.

Why Dispatch Is Sound:

  • simd_level() caches OnceLock<SimdLevel> from is_x86_feature_detected!
  • Every unsafe call site is preceded by an simd_level() match arm
  • Dimension assertions are in the public API before any unsafe call
  • DistanceEngine::dispatch enforces assert_eq! (release mode included) on both input lengths and the engine dimension: kernels are pre-resolved for a fixed dimension, so a mismatched call would otherwise read out of bounds

Module: crates/velesdb-core/src/simd_native/reduction.rs

Functions:

  • hsum_avx256() - Horizontal sum of AVX2 __m256 register
  • hsum_avx512() - Horizontal sum of AVX-512 __m512 register
  • reduce_4acc_avx256() / reduce_4acc_avx512() - 4-accumulator reduction

Macros (expand inside unsafe contexts at call sites):

  • simd_4acc_dot_loop! / simd_4acc_l2_loop! - 4-accumulator unrolled loops
  • simd_8acc_dot_loop! / simd_8acc_l2_loop! - 8-accumulator unrolled loops

Invariants:

  1. All functions require CPU features enforced by #[target_feature]
  2. No pointer arithmetic or memory access - operate purely on register values
  3. Macros accept only validated pointers from loop-bounded callers

Why It's Sound:

// SAFETY: All intrinsics require AVX2 which is guaranteed by #[target_feature].
// No pointer arithmetic or memory access — operates purely on register values.

Module: crates/velesdb-core/src/simd_native/adc.rs

Functions:

  • adc_distances_batch() - Public dispatch for PQ ADC distance computation
  • adc_single_avx2() - AVX2 gather-based ADC (8 subspaces per iteration)
  • adc_single_neon() - NEON ADC (4 subspaces per iteration, get_unchecked)

Invariants:

  1. Runtime feature detection via simd_level() before calling SIMD path
  2. code.len() == m asserted via debug_assert_eq! in each kernel
  3. code[i] < k for all i asserted via debug_assert! at function entry
  4. AVX2 gather indices computed as subspace * k + code[subspace], bounded by m * k
  5. Scalar fallback exists for CPUs without AVX2 or NEON
  6. (#895) The code[i] < k precondition (3) — only a debug_assert! here — is upheld for codes originating from a deserialized on-disk codebook by load-time validation: every PQ code is checked < num_centroids and the OPQ rotation length == dim * dim after deserialization (quantization/pq.rs, quantization/pq_persistence.rs). An invalid code is skipped gracefully rather than reaching the gather, so the release-mode OOB gather / scalar-path panic class is closed before the unsafe kernel runs.

Why It's Sound:

// AVX2: _mm256_i32gather_ps reads f32 at base_ptr + index * 4.
// Each index = subspace * k + code[subspace] < m * k = lut.len().
// Scale = 4 = size_of::<f32>(), matching lut element type.
let gathered = _mm256_i32gather_ps::<4>(lut.as_ptr(), indices);

// NEON: get_unchecked with bounds verified by debug_assert at entry.
let vals: [f32; 4] = [
    *lut.get_unchecked(base * k + usize::from(*code.get_unchecked(base))),
    // ...
];

Module: crates/velesdb-core/src/simd_native/prefetch.rs

Functions:

  • prefetch_vector() - Prefetch &[f32] into L1 cache (_mm_prefetch / NEON)
  • prefetch_vector_from_u16() - Prefetch &[u16] (PQ code vectors)
  • prefetch_vector_u64() - Prefetch &[u64] (RaBitQ binary codes)
  • prefetch_vector_multi_cache_line() - Multi-level cache prefetch (L1/L2/L3)
  • prefetch_multi_x86() / prefetch_multi_arm64() - Platform-specific helpers

Invariants:

  1. _mm_prefetch is a non-faulting hint instruction on x86_64
  2. Pointer offsets are bounded by vector_bytes checks before unsafe { base.add(...) }
  3. ARM64 prefetch_multi_arm64() uses unsafe { base.add() } only when vector_bytes > offset is verified
  4. Graceful degradation: no-op on unsupported architectures

Module: crates/velesdb-core/src/simd_neon_prefetch.rs

Functions (all #[cfg(target_arch = "aarch64")]):

  • prefetch_read_l1() / prefetch_read_l2() / prefetch_read_l3() - Read prefetch
  • prefetch_write_l1() - Write prefetch
  • prefetch_vector_neon() - Multi-line vector prefetch with 128B stride

Unsafe: Inline assembly core::arch::asm!("prfm pldl1keep, [{ptr}]")

Invariants:

  1. ARM prfm instructions are non-faulting hints (ARM Architecture Reference Manual)
  2. Invalid or out-of-bounds pointers are tolerated by hardware
  3. options(nostack, preserves_flags) ensures no stack or flag side effects
  4. Pointer offsets in prefetch_vector_neon() are guarded by vector_bytes > offset

Why It's Sound:

// SAFETY: `asm!(prfm ...)` emits a prefetch hint only.
// - Condition 1: `prfm` does not dereference memory architecturally.
// - Condition 2: Invalid pointers are tolerated by hardware for prefetch hints.
unsafe {
    core::arch::asm!(
        "prfm pldl1keep, [{ptr}]",
        ptr = in(reg) ptr,
        options(nostack, preserves_flags)
    );
}

Forbidden Scenarios:

  • None: all prefetch instructions (x86 _mm_prefetch, ARM prfm) are architecturally non-faulting hints. Invalid addresses are silently ignored.

Why It's Sound (shared across all SIMD kernels):

// Public API enforces precondition
pub fn dot_product_native(a: &[f32], b: &[f32]) -> f32 {
    assert_eq!(a.len(), b.len(), "Vector dimensions must match");
    
    match simd_level() {  // Cached runtime detection
        SimdLevel::Avx512 => unsafe { dot_product_avx512(a, b) },
        // ...
    }
}

Forbidden Scenarios:

  • Calling any target-featured function without runtime feature detection
  • Passing slices of different lengths
  • Using aligned load intrinsics on potentially unaligned data

Module: crates/velesdb-core/src/index/trigram/simd.rs

Functions:

  • extract_trigrams_avx2_inner()
  • extract_trigrams_avx512_inner()

Invariants:

  1. Runtime feature detection before unsafe call
  2. Bounds checking: i + 34 <= len before 32-byte access
  3. Prefetch addresses are within allocated buffer

Module: crates/velesdb-core/src/internal_bench.rs

Functions: cosine_avx2_2acc(), cosine_avx2_4acc(), cosine_avx512() — hidden bench-only helpers that call the AVX2/AVX-512 cosine kernels directly (bypassing the dispatcher) for internal performance comparisons.

Invariants:

  1. Each helper checks is_x86_feature_detected!("avx2") + "fma" (or "avx512f") immediately before the unsafe call and returns None when the feature is absent
  2. The called kernels are the same #[target_feature] functions audited in the x86_avx2/ and x86_avx512.rs sections above; slice-length contracts are identical
  3. The module is compiled into the production crate (pub mod internal_bench) but is only reachable from benchmark harnesses

RaBitQ SIMD (Binary Hamming Distance)

Module: crates/velesdb-core/src/simd_native/x86_avx512.rs (binary Hamming kernels; dispatched from simd_native/dispatch/hamming.rs. The quantization/rabitq*.rs files contain no unsafe.)

Function: hamming_binary_avx512_vpopcntdq()

Uses _mm512_popcnt_epi64 to compute Hamming distance on 512-bit binary vectors. This instruction is available on Ice Lake+ (Intel) and Zen4+ (AMD) processors with the AVX-512 VPOPCNTDQ extension.

Invariants:

  1. Runtime feature detection via has_avx512vpopcntdq() ALWAYS precedes the unsafe call
  2. #[target_feature(enable = "avx512f,avx512vpopcntdq")] enforces CPU feature requirement at the function level
  3. Input binary vectors have matching lengths (asserted before unsafe call)
  4. // SAFETY: comments present on all unsafe SIMD blocks

Fallback: Scalar popcount loop that iterates u64 words and sums count_ones(). This path is always safe and requires no CPU feature gates.

Why It's Sound:

// Public API checks feature before dispatching
if has_avx512vpopcntdq() {
    // SAFETY: Feature detection confirmed AVX-512 VPOPCNTDQ support.
    // Input slices have equal length (asserted above).
    unsafe { hamming_binary_avx512_vpopcntdq(a, b) }
} else {
    hamming_binary_scalar(a, b)  // Always-safe fallback
}

Forbidden Scenarios:

  • Calling hamming_binary_avx512_vpopcntdq without checking has_avx512vpopcntdq()
  • Passing binary vectors of different lengths

Prefetch Instructions

Module: crates/velesdb-core/src/perf_optimizations.rs

Function: ContiguousVectors::prefetch(node_id)

Issues software prefetch hints (_mm_prefetch with _MM_HINT_T0) to bring neighbor vector data into L1 cache before it is needed during HNSW search.

Invariants:

  1. Prefetch to an invalid or out-of-bounds address is architecturally a no-op on x86 (Intel SDM Vol. 2, Section 4.3 "PREFETCHh": "A PREFETCHh instruction is treated as a NOP if the memory address points to a non-cacheable memory region")
  2. Prefetch count is bounded by the HNSW neighbor list size (M=16..64), so the number of prefetch instructions per search step is small and predictable
  3. No memory faults, no side effects beyond cache line fills

Why It's Sound:

// SAFETY: _mm_prefetch is a hint instruction that cannot fault.
// Even if node_id is out of bounds, the prefetch address is simply
// ignored by the CPU. No memory access occurs — only a cache hint.
unsafe {
    _mm_prefetch(ptr.cast::<i8>(), _MM_HINT_T0);
}

Forbidden Scenarios:

  • None: prefetch is architecturally safe for any address on x86. However, callers should still prefer valid addresses for meaningful cache benefit.

Memory Allocation

Module: crates/velesdb-core/src/perf_optimizations.rs

Struct: ContiguousVectors

Invariants (documented in code as EPIC-032/US-002):

  1. data is always non-null (enforced by NonNull<f32>)
  2. data points to memory allocated with 64-byte alignment
  3. capacity * dimension * sizeof(f32) bytes are always allocated
  4. count <= capacity is always maintained
  5. (#899) All offset/capacity arithmetic (index * dimension, capacity * 2, ensure_capacity(index + 1)) uses checked_mul/checked_add. An overflow returns an error instead of wrapping, so a crafted index can no longer wrap an offset to a small value and drive an out-of-bounds copy_nonoverlapping write in release builds.

Why It's Sound:

// NonNull guarantees non-null at type level
let data = NonNull::new(ptr.cast::<f32>())
    .expect("Failed to allocate: out of memory");

// Bounds checked before access
pub fn get(&self, index: usize) -> Option<&[f32]> {
    if index >= self.count {
        return None;
    }
    // SAFETY: Index is within bounds (checked above)
    Some(unsafe { std::slice::from_raw_parts(...) })
}

Send/Sync Implementation:

// SAFETY: ContiguousVectors owns its data and doesn't share mutable access
unsafe impl Send for ContiguousVectors {}
unsafe impl Sync for ContiguousVectors {}

This is sound because:

  • Single owner (no aliasing)
  • No interior mutability without &mut self
  • Memory is not thread-local

Module: crates/velesdb-core/src/contiguous_ops.rs

Struct: ContiguousVectors (impl block — extends perf_optimizations.rs)

Critical Operations:

  1. reorder_copy() - Out-of-place vector reordering with dealloc + copy_nonoverlapping
  2. Drop for ContiguousVectors - Deallocates the raw buffer via dealloc

Invariants:

  1. old_idx < self.count is bounds-checked before copy_nonoverlapping
  2. new_idx < new_order.len() == self.count ensures destination is in bounds
  3. Source and destination buffers are distinct (non-overlapping) allocations
  4. AllocGuard provides panic-safety: if copy_permuted_vectors panics, the guard deallocates the new buffer; the old buffer remains valid
  5. Drop::drop uses NonNull invariant (pointer is always non-null)

Why It's Sound:

// SAFETY: src is within the current allocation (old_idx < count, count <= capacity).
// dst is within the new allocation (new_idx < new_order.len() == count).
// Both buffers are distinct (non-overlapping) allocations.
unsafe {
    ptr::copy_nonoverlapping(
        self.data.as_ptr().add(old_idx * dim),
        dst.add(new_idx * dim),
        dim,
    );
}

// Drop: SAFETY: data was allocated with this layout, is non-null (NonNull invariant)
unsafe { dealloc(self.data.as_ptr().cast::<u8>(), layout); }

Module: crates/velesdb-core/src/contiguous_resize.rs

Struct: ContiguousVectors (impl block — capacity growth path)

Critical Operations:

  1. alloc_and_copy() - allocates the new buffer via AllocGuard::new_zeroed and migrates existing vectors with ptr::copy_nonoverlapping
  2. Resize epilogue - dealloc of the old buffer after the copy succeeds

Invariants:

  1. Source (src) and destination (new_data) are distinct allocations, so copy_nonoverlapping never aliases; both are NonNull and 64-byte aligned by Self::layout
  2. copy_size = count * dimension is bounded by the old allocation (count <= capacity) and by the new layout (new_capacity > capacity)
  3. AllocGuard provides panic-safety: if the copy panics, the guard frees the new buffer; ownership transfers via guard.into_raw() only after success
  4. The old buffer is deallocated with the layout it was allocated with (old_layout recomputed from dimension/capacity), and only after self.data is about to be replaced — state update is all-or-nothing

Module: crates/velesdb-core/src/alloc_guard.rs

Struct: AllocGuard - RAII guard for raw allocations

Invariants:

  1. ptr is either valid or owns_memory = false
  2. layout matches the allocation
  3. Drop deallocates if and only if owns_memory = true
  4. (#899) new/new_zeroed return None when layout.size() exceeds the process-wide per-allocation ceiling (DEFAULT_ALLOC_BYTE_LIMIT, 1 TiB; configurable via set_alloc_byte_limit). This is a deliberately high backstop against pathological/attacker-controlled or arithmetic-wrapped sizes — far above any single contiguous buffer VelesDB legitimately allocates, so it never rejects a real index. It is threaded through the ContiguousVectors construct / resize / reorder allocation paths plus the check_alloc_bound pre-check. It does not affect soundness of the RAII guarantee; it only narrows which requests reach the system allocator. Primary defense against untrusted sizes remains the per-artifact load-time validation (file-length-bounded counts, see below) — AllocGuard only catches whatever slips past those local checks.

Why It's Sound:

impl Drop for AllocGuard {
    fn drop(&mut self) {
        if self.owns_memory {
            // SAFETY: ptr was allocated with self.layout and we own it
            unsafe { dealloc(self.ptr.as_ptr(), self.layout); }
        }
    }
}

// SAFETY: Raw memory has no thread affinity
unsafe impl Send for AllocGuard {}
// NOT Sync - concurrent access to raw memory is unsafe

Memory-Mapped I/O

Module: crates/velesdb-core/src/storage/mmap.rs

Critical Operations:

  1. MmapMut::map_mut() - Creates memory mapping
  2. ensure_capacity() - Resizes the mmap (remap)
  3. get_vector() - Returns a guarded slice into mmap

Invariants:

  1. File is always set_len() before mapping
  2. Mmap is flushed before unmap/remap
  3. Epoch counter invalidates guards after remap
  4. Offsets are always 4-byte aligned (f32)

Why It's Sound:

// SAFETY: data_file is a valid, open file with set_len() called
let mmap = unsafe { MmapMut::map_mut(&data_file)? };

// Remap with epoch invalidation
*mmap = unsafe { MmapMut::map_mut(&self.data_file)? };
self.remap_epoch.fetch_add(1, Ordering::Release);  // Invalidate old guards

Forbidden Scenarios:

  • ❌ Accessing mmap after resize without re-acquiring guard
  • ❌ Creating mapping for file with size 0
  • ❌ Using guard after epoch mismatch

Module: crates/velesdb-core/src/storage/mmap_capacity.rs

Function: MmapStorage::ensure_capacity()

Critical Operation: Remaps the memory-mapped file after resizing via unsafe { MmapMut::map_mut(&self.data_file)? }.

Invariants:

  1. data_file.set_len(new_len) is called BEFORE remapping, ensuring the file is large enough for the new mapping
  2. Old mmap is flushed before remap (mmap.flush())
  3. Epoch counter is incremented after remap to invalidate stale guards
  4. Write lock on self.mmap is held during the entire resize operation

Why It's Sound:

self.data_file.set_len(new_len)?;
// SAFETY: data_file has been resized with set_len(new_len) above.
// - Condition 1: File was resized to new_len before remapping.
// - Condition 2: Old mmap is dropped when we assign the new one.
// - Condition 3: File remains open with read+write permissions.
*mmap = unsafe { MmapMut::map_mut(&self.data_file)? };
self.remap_epoch.fetch_add(1, Ordering::Release);

Module: crates/velesdb-core/src/storage/mmap/wal_replay.rs

Struct: ReplayTarget — grows the mmap during CRC-framed WAL replay so recovered vectors extending past the last flushed size are not dropped.

Critical Operation: ensure_capacity() remaps via unsafe { MmapMut::map_mut(self.data_file)? } after growing the backing file.

Invariants:

  1. data_file.set_len(new_len) is called BEFORE remapping (new_len = required_len + MIN_GROWTH, mirroring the live growth floor), so the file fully covers the new mapping range
  2. The old mmap is flushed (mmap.flush()) before the remap and dropped on assignment
  3. data_file is the read+write handle that owns the file; replay runs during Collection::open, before any concurrent reader exists, so no guard/epoch coordination is needed on this path

Why It's Sound:

self.data_file.set_len(new_len)?;
// SAFETY: `set_len(new_len)` resized the backing file to fully cover the
// mapping range before remapping; the old mapping is dropped on assign.
*self.mmap = unsafe { MmapMut::map_mut(self.data_file)? };

Module: crates/velesdb-core/src/storage/guard.rs

Struct: VectorSliceGuard - Safe wrapper for mmap slices

Invariants:

  1. Holds RwLockReadGuard - prevents concurrent remap
  2. epoch_at_creation == current_epoch must hold for access
  3. Pointer derived from guard, valid for guard's lifetime

Why Send+Sync Is Sound:

// SAFETY: VectorSliceGuard is Send+Sync because:
// 1. Underlying data is in memory-mapped file (shared memory)
// 2. RwLockReadGuard ensures exclusive read access
// 3. Pointer is derived from guard, valid for its lifetime
// 4. Epoch check prevents access after remap
// 5. Data is read-only
unsafe impl Send for VectorSliceGuard<'_> {}
unsafe impl Sync for VectorSliceGuard<'_> {}

Additional invariant — parking_lot features must stay off: the Send impl moves a parking_lot::RwLockReadGuard<'a, MmapMut> across threads. This is sound only because the workspace enables no parking_lot features. With deadlock_detection or send_guard enabled, a RwLockReadGuard carries per-thread bookkeeping that is corrupted when the guard is released on a thread other than the one that acquired it. Do not enable either feature without revisiting this impl. (Verified: no Cargo.toml in the workspace enables a parking_lot feature — every dependant pins the bare parking_lot = "0.12" / version-only form, and velesdb-core's [dependencies.parking_lot] table declares version only.)

Pointer Operations

Module: crates/velesdb-core/src/storage/vector_bytes.rs

Functions:

  • vector_to_bytes() - &[f32] → &[u8]
  • bytes_to_vector() - &[u8] → Vec<f32>

Invariants:

  1. f32 has no invalid bit patterns
  2. Slice layout is well-defined and contiguous
  3. Lifetime of output tied to input (for vector_to_bytes)
  4. bytes.len() >= dimension * 4 (asserted for bytes_to_vector)

Why It's Sound:

// SAFETY: f32 has no invalid bit patterns, slice is contiguous
pub(super) fn vector_to_bytes(vector: &[f32]) -> &[u8] {
    unsafe {
        std::slice::from_raw_parts(
            vector.as_ptr().cast::<u8>(),
            std::mem::size_of_val(vector)
        )
    }
}

// Copy-based conversion - safe for any alignment
pub(super) fn bytes_to_vector(bytes: &[u8], dimension: usize) -> Vec<f32> {
    assert!(bytes.len() >= dimension * std::mem::size_of::<f32>());
    let mut vector = vec![0.0f32; dimension];
    // SAFETY: bounds verified above, copy_nonoverlapping doesn't require alignment
    unsafe {
        std::ptr::copy_nonoverlapping(bytes.as_ptr(), vector.as_mut_ptr().cast::<u8>(), ...);
    }
    vector
}

Module: crates/velesdb-core/src/storage/compaction.rs

Platform-Specific Operations:

  • punch_hole_linux() - fallocate with FALLOC_FL_PUNCH_HOLE
  • punch_hole_windows() - FSCTL_SET_ZERO_DATA

Invariants:

  1. File descriptor/handle is valid (from std::fs::File)
  2. Syscall parameters are bounds-checked
  3. Fallback exists if filesystem doesn't support operation

Why It's Sound:

// SAFETY: fallocate is a valid syscall, fd is a valid file descriptor
let ret = unsafe { libc::fallocate(fd, mode, offset as libc::off_t, len as libc::off_t) };

HNSW Graph Unsafe Operations

Unchecked Vector Access: neighbors.rs, search.rs, search_state.rs

Modules:

  • crates/velesdb-core/src/index/hnsw/native/graph/neighbors.rs
  • crates/velesdb-core/src/index/hnsw/native/graph/search.rs
  • crates/velesdb-core/src/index/hnsw/native/graph/search_state.rs

Operation: vectors.get_unchecked(node_id) on ContiguousVectors

These three files form the HNSW search and neighbor selection hot path. They use get_unchecked to eliminate bounds checks on vector access during graph traversal, where the node IDs are guaranteed valid by construction.

Invariants:

  1. Every node_id passed to get_unchecked was obtained from the graph's neighbor lists, which only contain IDs of successfully inserted nodes
  2. ContiguousVectors stores vectors at indices assigned by the monotonic counter in NativeHnsw.count - a node is inserted into vectors BEFORE it appears in any neighbor list
  3. Vectors are never removed from ContiguousVectors during the lifetime of a search (vectors outlive graph references)
  4. (#894) For a graph loaded from disk — the untrusted-input path — invariant 1 is upheld by load-time validation in index/hnsw/native/graph_io.rs: the header count_check must equal the vector count, entry_point < count, and every neighbor ID is checked < count before being stored in a layer. A file violating any of these is rejected with InvalidData at load, so no out-of-range ID ever reaches get_unchecked on the search hot path (the release-mode OOB read class is closed at the source).

Usage in neighbors.rs (neighbor selection with VAMANA diversification):

// SAFETY: candidate_id is a valid node_id from search results,
// which only contains IDs of successfully inserted nodes.
let candidate_vec = unsafe { vectors.get_unchecked(candidate_id) };

Usage in search.rs (greedy descent + layer search):

// SAFETY: entry/neighbor is a valid node_id from entry_point or
// the graph's neighbor list, always IDs of inserted nodes.
let entry_vec = unsafe { vectors.get_unchecked(entry) };
let neighbor_vec = unsafe { vectors.get_unchecked(neighbor) };

Usage in search_state.rs (batch neighbor gathering):

// SAFETY: neighbor is a valid node_id from the graph's neighbor list,
// only containing IDs of successfully inserted nodes.
let vec = unsafe { vectors.get_unchecked(neighbor) };

Forbidden Scenarios:

  • Using get_unchecked with user-provided IDs (must go through mappings first)
  • Accessing vectors after a vacuum/rebuild (stale indices)
  • Using get_unchecked outside the vectors+layers read lock scope

Drop Order: index/mod.rs and vacuum.rs

Modules:

  • crates/velesdb-core/src/index/hnsw/index/mod.rs
  • crates/velesdb-core/src/index/hnsw/index/vacuum.rs

Operation: ManuallyDrop::drop(&mut *inner_guard)

HnswIndex wraps its HnswInner in ManuallyDrop to enforce a drop-order invariant: inner (the HNSW graph) must be dropped BEFORE io_holder (reserved for future disk-backed backends that may own borrowed data).

Invariants (Drop for HnswIndex):

  1. inner is wrapped in ManuallyDrop to suppress automatic drop
  2. Write lock guarantees exclusive access during drop (no concurrent readers)
  3. Drop::drop is the only call site for ManuallyDrop::drop on inner
  4. io_holder field is declared AFTER inner (enforced by test_field_order_io_holder_after_inner)

Invariants (vacuum()):

  1. Exclusive write lock is held on inner_guard during the swap
  2. ManuallyDrop::drop is called exactly once before replacement
  3. The old value is immediately replaced with ManuallyDrop::new(new_inner)

Why It's Sound:

// Drop impl:
// SAFETY: ManuallyDrop::drop requires exclusive ownership and a single call.
// - Condition 1: Write lock guarantees no concurrent access.
// - Condition 2: This Drop impl is the only site that calls ManuallyDrop::drop.
unsafe { ManuallyDrop::drop(&mut *self.inner.write()); }

// Vacuum:
// SAFETY: We hold exclusive write lock. Called exactly once before replacement.
unsafe { ManuallyDrop::drop(&mut *inner_guard); }
*inner_guard = ManuallyDrop::new(new_inner);

Send/Sync: native_inner.rs

Module: crates/velesdb-core/src/index/hnsw/native_inner.rs

Operations: unsafe impl Send for NativeHnswInner and unsafe impl Sync for NativeHnswInner

Invariants:

  1. Internal mutability is synchronized via parking_lot::RwLock and atomics
  2. No thread-affine resources (thread-local state, file descriptors) are stored
  3. All exposed APIs respect the lock hierarchy (vectors → layers → neighbors)

Why It's Sound:

// SAFETY: `NativeHnswInner` is `Send` because ownership transfer preserves invariants.
// - Condition 1: Internal mutability is synchronized via `parking_lot::RwLock`/atomics.
// - Condition 2: No thread-affine resources are stored in the wrapper.
unsafe impl Send for NativeHnswInner {}

// SAFETY: `NativeHnswInner` is `Sync` because shared references are concurrency-safe.
// - Condition 1: Concurrent access to mutable graph state is lock/atomic protected.
// - Condition 2: Exposed APIs do not bypass synchronization primitives.
unsafe impl Sync for NativeHnswInner {}

API-Contract unsafe (No UB)

Module: crates/velesdb-core/src/collection/any_collection.rs

Function: AnyCollection::into_vector_unchecked() — converts any collection variant (Vector/Graph/Metadata) into a VectorCollection without checking the variant.

Why it is marked unsafe: violating the caller contract is not memory-unsafe and cannot cause UB. The marker flags a logical contract: calling vector-specific methods on a VectorCollection obtained from a Graph or Metadata variant yields logically unsound results (empty or misleading), because the underlying storage holds no homogeneous vector index.

Invariants (caller contract):

  1. Branch on is_vector() first and only invoke vector-specific methods on the Vector variant, or
  2. Restrict usage to the surface shared by all three collection kinds (config, flush, diagnostics, name, point_count, execute_query_str) — this is what the Python/Mobile/Tauri bindings do.

Prefer the safe, variant-checked into_vector() (returns Result) when the caller can branch. A type-safe refactor eliminating this method is tracked in docs/TECH_DEBT_REGISTRY.md (pre-seed audit finding F2.2).

Concurrency

Atomic Operations

Used In: storage/mmap.rs, perf_optimizations.rs, index/hnsw/native/graph/

Pattern 1: Epoch-based invalidation

// Writer side (during remap)
self.remap_epoch.fetch_add(1, Ordering::Release);

// Reader side (in guard)
let current = self.epoch_ptr.load(Ordering::Acquire);
assert!(current == self.epoch_at_creation, "Mmap was remapped");

Why It's Sound:

  • Release/Acquire ordering ensures visibility
  • Guard panics if epoch mismatches (fail-safe)
  • No data race: old pointers are never dereferenced after epoch change

Pattern 2: entry-point moves under the promotion lock (HNSW)

NativeHnsw stores entry_point and max_layer as AtomicUsize, which searches load without a lock. Every write takes promotion: Mutex<()> (rank 8, before vectors): the first claim of an empty graph, each promotion together with the anchor reparenting that follows it, and the renumbering reorder_for_locality applies (#2259).

// First insert: under the lock, CAS from NO_ENTRY_POINT, then set max_layer
self.entry_point.compare_exchange(
    NO_ENTRY_POINT, node_id, Ordering::AcqRel, Ordering::Acquire
);
// Layer promotion: under the lock, check again, store max_layer, swap the
// entry point, then reparent the anchor tree
self.max_layer.store(node_layer, Ordering::Release);
let previous = self.entry_point.swap(node_id, Ordering::AcqRel);
self.reparent_entry_point(previous, node_id);

Why It's Sound:

  • Writers are serialized, so two promotions never interleave: the later one cannot clear the anchor the earlier one has just given its node, which would strand the tree below it.
  • AcqRel on the CAS and the swap makes the new entry point visible to every later Acquire load.
  • The transient window between the max_layer store and the swap is safe: readers seeing the old entry point at the new max layer encounter empty neighbor lists and perform a no-op descent.
  • A node at or below the maximum layer, the common case, returns before taking the lock; promotion occurs O(log_M(N)) times per index lifetime.

HNSW Slot Allocation

Module: crates/velesdb-core/src/index/hnsw/sharded_mappings.rs, crates/velesdb-core/src/index/hnsw/native_inner.rs, crates/velesdb-core/src/index/hnsw/index/batch.rs, crates/velesdb-core/src/index/hnsw/direct_writer.rs, crates/velesdb-core/src/index/hnsw/upsert.rs, crates/velesdb-core/src/index/hnsw/index/mod.rs, crates/velesdb-core/src/index/hnsw/native_index.rs, crates/velesdb-core/src/index/hnsw/index/vacuum.rs, crates/velesdb-core/src/collection/streaming/async_index_builder.rs

A slot is an index into the graph's ContiguousVectors, and the arena is its only allocator: a slot exists once a vector has been pushed into it, and the push returns it. Every insert path — single, batch, the vacuum rebuild and the bulk path's direct writer — places the vector first and then maps the id to the slot it got (ShardedMappings::assign). Nothing predicts a slot.

  1. Validate dimensions — every vector of a batch is checked before the graph sees any, so a mismatch leaves the index untouched.
  2. Place (place, place_parallel, and place_unlinked for the direct writer) — the arena appends under its own lock and returns each slot as a Placed token, in input order.
  3. Assign — each id is mapped to its slot. An id that was already mapped leaves its old slot behind as a tombstone; an id repeated within a batch ends on its last occurrence.

The direct writer's slots are linked later, where they are, and nothing places them again (#2264). The async builder queues their ids, not their vectors, and its drain (HnswIndex::link_placed) resolves each id to its slot under the read guard. It skips an id deleted since and a slot already linked — the id was upserted through the graph since, or a vacuum rebuilt the graph with it — and links an id queued twice once, at the slot of its last write. An index with its exact-distance features off gives the direct writer no slot to fill; the builder then places those vectors itself.

Invariant: a mapping only ever names a slot that already holds that id's vector, so two writers — a bulk load's direct writer and a single upsert, say — cannot hand one slot to two ids. Debug builds check part of it in assign: a slot whose reverse entry names another id panics before either map changes.

Invariant: the index read guard is held from placement to assignment. reorder_for_locality and vacuum renumber slots under the write lock, so no slot can move between the push that returned it and the mapping that names it; vacuum rebuilds the mappings before it releases that lock. assign takes the Placed token a placement returns, never a bare slot, and the token borrows the guard the placement ran under: releasing that guard before the slot is mapped does not compile (E0505). Placements mint the token; outside tests (Placed::for_test) the one exception is Placed::installed, which vacuum uses for its rebuilt graph: it makes a token from a bare slot under a write guard and trusts its caller that the slot is that graph's. The token ties a mapping to a guard's lifetime, not to a particular index; each call site keeps an index's guard and its mappings together.

Invariant: remove holds the index read guard across its two map writes: soft_delete borrows the graph, so releasing the guard first does not compile. reorder_for_locality re-maps under the write guard by snapshotting the forward map, clearing both maps and reinserting: one overlapping a delete could map the deleted id again, and one between its two writes could erase the reverse entry of the id that took its slot. vacuum re-maps under the write guard too, so no delete lands inside its re-map either. As with Placed, the borrow proves a borrow of some graph (through its guard, for an index's own), not that it is this index's graph: each call site keeps an index's guard and its mappings together.

Invariant: a write made while vacuum rebuilds survives its swap (#2262). vacuum snapshots each live id with its slot under a read guard, rebuilds without one, copies the writes made meanwhile into the new graph in catch-up rounds that hold a read guard only to list them and copy their vectors out, then re-maps under the write guard from the mappings as they stand, not from the snapshot. An id still on the slot its vector was read from, by the snapshot or a catch-up round, takes the slot that vector got in the new graph. An id on any other slot was inserted or upserted since: its vector is copied from the old graph into the new one, one insert at a time, before the old graph is dropped. No rayon work runs under the write guard: a rayon worker parked on the index lock by a batch search cannot run it, and a vacuum that waited on one hung. A snapshot id no longer mapped was deleted since, and stays deleted; its node in the new graph is a tombstone, and counted as one: the re-map sets next_idx to the new graph's slot count, so tombstone_count, which is what triggers a vacuum, counts every slot no id names, wherever it falls. "Still on its snapshot slot" means "untouched" because the arena never hands a slot out twice and nothing renumbers meanwhile: vacuum and reorder_for_locality share a maintenance lock, taken before the index lock and never by a writer or a save. The rebuild reads M, ef_construction and alpha from the graph it replaces, so a vacuum keeps the parameters the index was built with, and a save after it persists them. With no live id the rebuild still runs, into an empty graph, so an index whose ids are all deleted is left with no tombstone. Tests: writes_racing_a_vacuum_survive_it, writes_racing_a_vacuum_of_an_sq8_index_survive_it, deletes_racing_a_vacuum_keep_the_tombstone_count_exact, vacuum_keeps_the_index_parameters and vacuum_of_an_index_with_no_live_id_empties_it in index/hnsw/index_tests.rs, and a_vacuum_carrying_writes_finishes_beside_batch_searches in tests/vacuum_beside_batch_search.rs.

Invariant: a save persists mappings that name only slots of the graph it persists, each holding the vector of the id that names it (#2262). save copies the mappings under the read guard it dumps the graph under, before the dump (persistence::dump_graph): every slot they name already holds its vector, the arena only grows while the guard is held, and a renumber needs the write guard. That ordering is not left to timing to test: the dump carries a window on its far side, and a_write_in_the_save_window_never_names_a_slot_the_graph_lacks writes into it. With the copy first the write is named by nobody; with the copy moved after the dump the same write is named by the mappings and absent from the graph, and the reload refuses it. The copy reads the forward map once and derives the reverse map from it, so the two agree while writers run. The persisted next_idx is the slot count the dump wrote, so a slot placed after the copy, which no saved id names, reloads as a tombstone. The graph's own dump holds the arena's read guard across its vectors file and its graph file, in the declared order (vectors, then layers): no node is pushed in between, so the graph file names no node the vectors file lacks. Saves of one index run one at a time, under a lock of their own that vacuum never takes: two at once into one directory read the same generation and stamped it over each other's files. HnswIndex and NativeHnswIndex each hold that lock -- the second was missed at first, and the invariant is stated of saves, not of one of the two wrappers over the same files. Tests: writes_racing_a_save_reload_consistent, a_write_in_the_save_window_never_names_a_slot_the_graph_lacks, batch_inserts_racing_a_save_reload_consistent, a_save_racing_a_vacuum_reloads_consistent, saves_racing_into_one_directory_reload_consistent and native_saves_racing_into_one_directory_reload_consistent.

Invariant: a refused vector or batch maps nothing, so there is nothing to roll back. A batch the graph refuses part-way leaves the nodes it already placed unmapped, as tombstones vacuum reclaims.

Why it used to be otherwise (#2246): the mappings kept a counter of their own. They predicted a slot at registration, the graph pushed wherever the arena was, and a reconcile step corrected the mapping afterwards; the direct writer wrote at the predicted slot and never reconciled. With a bulk load and single upserts running together the two counters diverged, and each of three runs of tests/concurrent_bulk_slots.rs lost 611 to 645 of 6 400 ids — unfindable even by an exhaustive scan, or answering with another id's vector.

Cross-reference: The Collection-level pipeline (crud.rs: batch_store_all -> per_point_updates, then crud_indexing.rs: bulk_index_or_defer) calls insert_batch_parallel in its last phase. The crash recovery implications are documented in CONCURRENCY_MODEL.md.

HNSW Reachability Anchors

Module: crates/velesdb-core/src/index/hnsw/native/graph/anchors.rs, crates/velesdb-core/src/index/hnsw/native/layer.rs, crates/velesdb-core/src/index/hnsw/native/graph/neighbors.rs, crates/velesdb-core/src/index/hnsw/native/graph/insert.rs

Every base-layer node other than the entry point records an anchor: the node whose list holds one edge to it that eviction never removes (#2259). Anchors take four bytes a slot (AtomicU32, the width node ids have on disk), allocated with the base layer.

Invariant, outside a promotion: anchor_of(x) == a implies x is in a's base-layer list, and a is itself anchored or is the entry point, which has no anchor. The anchors therefore form a tree rooted at the entry point, and every anchored node is reachable from it over the base layer. Reachable is the guarantee: a search starts from where its greedy descent lands and stops on stagnation, so it still walks that graph approximately.

  • Set and checked under the parent's list lock. link_protected makes sure x is in a's list and records the anchor inside the same with_neighbors_mut closure; evict_most_redundant scans a list under that lock and skips every entry anchored to its owner. An evictor can never see the anchor without the edge, nor remove the edge after the anchor.
  • Eviction never removes an anchor edge: both eviction sites skip every entry anchored to the list's owner, so an evictee's anchor, once it has one, is another list's edge; a batch mate still connecting gets its own from the pass after its chunk. When every entry of a full list is protected, link_protected places the edge one level down the tree instead, in a protected child picked by spread_protected_child, so no list grows past its cap; only after 32 levels would one grow by one. connect_back_with_pruning skips adding the newcomer to such a list.
  • Every node gets one. A single insert anchors its node from the first anchored node of its own list; a parallel batch anchors each node as soon as one of its neighbours is, then retries the rest until a pass adds nothing, and links what remains from the entry point. The first insert into an empty graph claims the entry point under the promotion lock (claim_first_entry_point): a node that loses that claim, a single insert or a batch's first node, connects through the winner.
  • The root moves with the entry point. A promoted entry point drops its own anchor and takes the previous one into its subtree (reparent_entry_point), under the promotion lock and in the same step as the swap: two promotions never interleave their reparenting.
  • Renumbering and loading. Layer::remap_ids moves and renames anchors with the lists they describe. A loaded graph rebuilds them as a breadth-first tree from the entry point, since they are not persisted, then anchors each node that walk missed from its own list: a graph saved before #2259 is repaired when it is loaded.

Interior Mutability Invariants: RaBitQPrecisionHnsw

Module: crates/velesdb-core/src/index/hnsw/ (RaBitQ integration)

RaBitQPrecisionHnsw uses RwLock and Mutex for interior mutability of its quantization state. The following invariants guarantee that no undefined behavior or data inconsistency can occur:

State transition invariants:

Field Invariant
rabitq_index Transitions from None to Some(Arc<RaBitQIndex>) exactly once during the lifetime of the struct. Once set, the value is immutable (only read-locked thereafter).
rabitq_store Grows monotonically after training. Only push operations occur (append-only). No elements are removed or reordered on the hot path.
training_buffer Accumulates raw vectors before training. After training completes, the buffer is cleared (clear()) and deallocated (shrink_to_fit()), reducing to zero capacity.

Memory safety invariants:

  • No raw pointer arithmetic exists in the RaBitQ code path. All vector access goes through safe Vec, Arc, and slice APIs.
  • The double-check locking pattern in train_rabitq() prevents duplicate training: the function re-checks rabitq_index under a write lock after initially observing None under a read lock. This ensures exactly-once training semantics even under concurrent calls.
  • Store-before-index ordering (see CONCURRENCY_MODEL.md) prevents search threads from observing a trained index with an empty store.

Why It's Sound:

  • RwLock/Mutex from parking_lot never poison, so lock acquisition cannot fail.
  • The one-time write to rabitq_index followed by read-only access is a well-established "initialize once, read many" pattern with no data race.
  • rabitq_store serializes writes via RwLock::write(), and each write holds the lock for a single Vec::push, minimizing contention.

Lock Ordering (MobileGraphStore)

Rule: edges → outgoing → incoming → nodes

The lock-order contract is documented per write method in crates/velesdb-mobile/src/graph.rs (each # Lock Order doc section); every write path acquires the four locks in this fixed order so no cycle can form.

FFI Boundaries

PyO3 (crates/velesdb-python/)

Pattern: Arc::as_ptr for lifetime management

fn get_core_memory(&self) -> PyResult<CoreSemanticMemory<'_>> {
    // SAFETY: We own the Arc, so the pointer is valid for lifetime of self
    let db_ref = unsafe { &*Arc::as_ptr(&self.db) };
    CoreSemanticMemory::new_from_db(db_ref, self.dimension).map_err(to_py_err)
}

Why It's Sound:

  • Arc is owned by self
  • Returned reference has lifetime '_ tied to &self
  • No use-after-free possible while self exists

WASM (crates/velesdb-wasm/src/serialization.rs)

Pattern: Byte slice reinterpretation

// SAFETY: f32 and [u8; 4] have same size, WASM is little-endian
let data_as_bytes: &mut [u8] = unsafe {
    core::slice::from_raw_parts_mut(data.as_mut_ptr().cast::<u8>(), total_floats * 4)
};

Invariants:

  1. WASM is always little-endian (spec requirement)
  2. f32 is 4 bytes, IEEE 754
  3. Buffer allocated with correct size before reinterpret

Soundness Checklist

For All Unsafe Code

  • All unsafe fn have # Safety documentation
  • All unsafe {} blocks have // SAFETY: comments
  • Preconditions are enforced before unsafe operations
  • No undefined behavior with valid inputs
  • Invariants are documented and maintained

For SIMD

  • Runtime feature detection precedes usage
  • #[target_feature] matches the intrinsics used
  • Slice lengths validated before access
  • Fallback path exists for unsupported CPUs

For Memory Operations

  • Pointers are non-null (use NonNull when possible)
  • Alignment requirements documented and enforced
  • Bounds checked before access
  • Lifetimes correctly tied to source data

For Concurrency

  • Lock ordering documented and consistent
  • Atomic orderings are correct (Release/Acquire pairs)
  • Send/Sync implementations have safety comments
  • No data races possible

For FFI

  • Input validation at boundary
  • Panic safety (no unwinding across FFI)
  • Lifetime management documented

References

Last updated: 2026-08-09 · Applies to: velesdb-core 6.0.0 (this stamp tracks the document revision; this revision adds the parking_lot-features invariant to the VectorSliceGuard entry. The underlying unsafe audit was last run in full on 2026-06-12, as stated at the top of this page)