Module index_ext::tag [−][src]
Expand description
Not quite dependent typing for eliding bounds checks.
Rough mechanism
The main idea is to use types as a compile time tag to identify a particular exact length bound without storing this bound in all instances associated with it. Thusly, we can construct indices that are guaranteed in-bounds of slices tagged with the same type, while storing them independent of each other and without introducing any borrow coupling. This then guarantees a bounds-check free code path for indexing into the slices.
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:
-
As a compile time constant. The
Constant
andConst
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. -
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 be 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. -
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 guarantees that all Slice
with that exact same tag are at least as long
as all the sizes in Len
structs of the same lifetime and each Idx
is bounded by some
Len
. While this may seem very restrictive at first, it still allows you to pass
information on a slice’s length across function boundaries by explicitly mentioning the same
lifetime twice. Additionally you’re allowed some mutable operations on indices that can not
exceed the original bounds.
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.
Additionally, the module provides an ‘algebra’ for tags such that you can dynamically prove two
tags to be equivalent, comparable, etc. Then you can leverage these facts (which are also
encoded as types) to substitute tags in different manner. See the LessEq
and [Eq
] types
as well as the many combinators on ExactSize
, Len
, 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
An owned, allocated slice with a checked length.
A number that overestimates the guaranteed size of a number of slices.
A tag using a const generic length parameter.
A tag using a ConstantSource
.
A proof that two tags refer to equal lengths.
The exact length separating slices and indices for a tag.
A generative lifetime.
A valid index for all slices of the same length.
An allocation of bounded indices that can be retrieved with a bound.
The length of a particular slice (or a number of slices).
A proof that the length if A is smaller or equal to B.
A named unique tag.
The length of a non-empty slice.
A slice with a unique type tag.
Traits
A type that names a constant buffer size.
A type suitable for tagging length, indices, and containers.