Module bitvec::index

Typed metadata of memory elements.

This module provides types which guarantee certain properties about working with individual bits of memory elements.

The main advantage of the types in this module is that they provide type-dependent range constrictions for index values, making it impossible to have an index out of bounds for a memory element, and creating a sequence of type transformations that give assurance about the continued validity of each value in its surrounding context.

By eliminating public constructors from arbitrary integers, bitvec can guarantee that only it can produce seed values, and only trusted functions can transform their numeric values or types, until the program reaches the property it requires. This chain of assurance means that operations that interact with memory can be confident in the correctness of their actions and effects.

Type Sequence

The library produces BitIdx values from region computation. These types cannot be publicly constructed, and are only ever the result of pointer analysis. As such, they rely on correctness of the memory regions provided to library entry points, and those entry points can leverage the Rust type system to ensure safety there.

BitIdx is transformed to BitPos through the BitOrder trait, which has an associated verification function to prove that implementations are correct. BitPos is the only type that can describe memory operations, and is used to create selection masks of BitSel and BitMask.

Structs

BitIdx	A semantic index of a single bit within a memory element M.
BitMask	A multi-bit selection mask.
BitPos	An electrical position of a single bit within a memory element M.
BitSel	A one-hot selection mask, to be applied to a memory element M.
BitTail	Semantic index of a dead bit after a live region.