Skip to main content

Module vec

certeza

Module vec 

Source
Expand description

§TruenoVec - A Growable Array Type with Verified Correctness

This module provides TruenoVec<T>, a custom growable vector implementation that demonstrates the certeza framework’s tiered testing approach:

  • Tier 1: Unit tests for basic functionality (sub-second feedback)
  • Tier 2: Property-based tests verifying algebraic properties (1-5 minutes)
  • Tier 3: Formal verification of critical invariants with Kani (hours)

§Safety Invariants

The following invariants are maintained and formally verified:

  1. ptr is either null or points to valid memory for capacity elements
  2. len <= capacity at all times
  3. Elements [0..len) are initialized
  4. Elements [len..capacity) are uninitialized

§Risk Classification

Very High Risk - Contains unsafe code for manual memory management. Full verification framework applied:

  • Property-based testing
  • 95%+ coverage requirement

  • 85% mutation score target

  • Formal verification of invariants

§Example

use certeza::TruenoVec;

let mut vec = TruenoVec::new();
vec.push(1);
vec.push(2);
vec.push(3);

assert_eq!(vec.len(), 3);
assert_eq!(vec.get(1), Some(&2));
assert_eq!(vec.pop(), Some(3));

Structs§

IntoIter
Consuming iterator over TruenoVec<T>.
Iter
Immutable iterator over TruenoVec<T>.
IterMut
Mutable iterator over TruenoVec<T>.
TruenoVec
A growable array type with verified correctness properties.