Module index_ext::tag

Statically elide bounds checks with the type system.

Rough mechanism

The main idea is to use types as a compile time tag to identify a particular length of a slice without storing this bound in the instances associated with the constraint. For this, we utilize strategies such as generativity or concrete compile time tags.

This allows us to construct wrapper types for indices and slices that guarantees its accesses to be in-bounds when combined with any other value with the same tag. Critically, these indices and slices can be stored and acted on independent of each other and without introducing borrow coupling between them. The type system guarantees a bounds-check free code path for indexing into the slices by adding an indexing operator which unconditionally performs the unsafe access.

This works particularly well for programs with fixed size buffers, i.e. kernels, bootloaders, embedded, high-assurance programs. If you encapsulate the ExactSize instance containing the authoritative source of the associated length then you can have a very high confidence in have ran appropriate access and bounds checks before accesses.

Built-in Tag types

There are a couple of different methods for creating tag types with such associations:

1. As a compile time constant. The Constant and Const offer different ways of defining the associated length as a fixed number. The former let’s you give it a type as a name while the latter is based on generic parameters.

2. The generative way. The Generative type is unique for every created instance, by having a unique lifetime parameter. That is, you can not choose its lifetime parameters freely. Instead, to create an instance you write a function prepared to handle arbitrary lifetime and the library hands an instance to you. This makes the exact lifetime opaque to you and the compiler which forces all non-local code to assume that it is indeed unique and it can not be unified with any other. We associate such a Generative instance with the length of the one slice provided during its construction.

3. And finally one might come up with an internal naming scheme where types are used to express unique bounds. This requires some unsafe code and the programmers guarantee of uniqueness of values but permits the combination of runtime values with 'static lifetime of the tag.

Each tag relates to one specific length of slices, without encoding that value itself into values but rather this is a ‘hidden’ variable. Usage of the tag guarantees a separation between slices associated with the tag and all indices. This allows transitive reasoning: All Slice with that exact same tag are at least as long as all the sizes in Prefix structs of the same lifetime and strictly for Idx. Note that it even allows passing information on a slice’s length across function boundaries by explicitly mentioning the same tag such as a generative lifetime twice.

Use with_ref and with_mut as main entry functions or one the constructors on the type Generative. Note the interaction with the generativity crate which provides a macro that doesn’t influence code flow, instead of requiring a closure wrapper like the methods given in this crate.

The interface also permits some mutable operations on indices. These operations are restricted to some that can not make the new value exceed the bound of the hidden variable (such as: monotonically decreasing operations).

The module even provides an ‘algebra’ for type level tags themselves. you can dynamically prove two tags to be equivalent, comparable, etc, by asserting that of the hidden variables associated with each tag. This does not necessarily require the hidden value to be concrete but it is most powerful when you locally haven an ExactSize representing that hidden value. Then you can leverage these facts (which are also encoded as zero-sized types) to substitute tags in different manner. See the TagLessEq and TagEq types as well as the many combinators on ExactSize, Prefix, and Idx.

Checked constant bounds

Alternatively we can choose other unique type instances. By that we mean that for any particular type exactly one value must be used to construct ExactSize. One possible way is if this is simply a constant which is implemented by the Constant wrapper and its ConstantSource trait. For example one may define:

use index_ext::tag::{Constant, ConstantSource, ExactSize};

const BUFFER_SIZE: usize = 4096;
struct BufferSize4K;

impl ConstantSource for BufferSize4K {
    const LEN: usize = BUFFER_SIZE;
}

const LEN: ExactSize<Constant<BufferSize4K>> = Constant::EXACT_SIZE;

Structs

• Boxed
  An owned, allocated slice with a checked length.
• Capacity
  A number that overestimates the guaranteed size of a number of slices.
• Const
  A tag using a const generic length parameter.
• Constant
  A tag using a ConstantSource.
• ExactSize
  The exact length separating slices and indices for a tag.
• Generative
  A generative lifetime.
• Idx
  A valid index for all slices of the same length.
• IdxBox
  An allocation of bounded indices that can be retrieved with a bound.
• NonZeroLen
  The length of a non-empty slice.
• Prefix
  The length of a particular slice (or a number of slices).
• Slice
  A slice with a unique type tag.
• TagEq
  A proof that two tags refer to equal lengths.
• TagLessEq
  A proof that the length if A is smaller or equal to B.
• TagNamed
  A unique tag, ‘named’ by its type parameter.

Traits

• ConstantSource
  A type that names a constant buffer size.
• Tag
  A type suitable for tagging length, indices, and containers.

Functions

• with_mut
  Enter a region for soundly indexing a mutable slice without bounds checks.
• with_ref
  Enter a region for soundly indexing a slice without bounds checks.