Expand description
Well-typed counters and register descriptors.
This module provides session types which encode a strict chain of modification
to map semantic indices within a BitSlice to the electrical register values
used to interact with the memory bus.
The main advantage of the types in 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 seed 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 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 seed type that describes memory
operations, and is used to create selection masks BitSel and BitMask.
!
Structs
A semantic index counter within a register element R.
Marks an index that is invalid for a register type.
A multi-bit selection mask for a register R.
An electrical position counter within a register element R.
A one-hot selection mask for a register element R.
A semantic index counter within or one bit past the end of a register
element R.