46 lines
2.0 KiB
Markdown
46 lines
2.0 KiB
Markdown
# Bit Indices
|
|
|
|
This module provides well-typed counters for working with bit-storage registers.
|
|
The session types encode a strict chain of custody for translating semantic
|
|
indices within [`BitSlice`] regions into real effects in memory.
|
|
|
|
The main advantage of types within this module is that they provide
|
|
register-dependent range requirements for counter values, making it impossible
|
|
to have an index out of bounds for a register. They also create a sequence of
|
|
type transformations that assure the library 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 initial values, and only trusted functions
|
|
can transform their numeric values or types, until the program reaches the
|
|
property that it requires. This chain of assurance means that memory operations
|
|
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 the 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. The
|
|
[`order`] module provides verification functions that implementors can use to
|
|
demonstrate correctness. `BitPos` is the basis type that describes memory
|
|
operations, and is used to create the selection masks [`BitSel`] and
|
|
[`BitMask`].
|
|
|
|
## Usage
|
|
|
|
The types in this module should only be used by client crates in their test
|
|
suites. They have no other purpose, and conjuring values for them is potentially
|
|
memory-unsafe.
|
|
|
|
[`BitIdx`]: self::BitIdx
|
|
[`BitMask`]: self::BitMask
|
|
[`BitOrder`]: crate::order::BitOrder
|
|
[`BitPos`]: self::BitPos
|
|
[`BitSel`]: self::BitSel
|
|
[`BitSlice`]: crate::slice::BitSlice
|
|
[`order`]: crate::order
|