#indices #vec #check #fixed #once #bounds #valid

yanked fixed_vec

Ghosts of Departed Proofs for checking valid indices of Vec's once

0.1.0 Jul 30, 2020

#46 in #indices

MIT/Apache

21KB
344 lines

fixed_vec

Bounds check indices only once, instead of over and over if the indices will be re-used:

use fixed_vec::{name, FixedVec};

let v = vec![0u32; 10];
let v = name!(v);
let mut v = FixedVec::fix(v);

// Perform the two index checks here:
let index_a = v.check_index(...).unwrap();
let index_b = v.check_index(...).unwrap();

for _ in 0..100 {
    // These do *not* perform bounds checks!
    // At compile time, v and index_a must match
    *v.get_mut(index_a) += 5;
    *v.get_mut(index_b) += 10;
}

let v = v.unfix();

// continue using v...

See the concept post for more information.

Dependencies

~1.5MB
~34K SLoC