Sound unchecked indexing in Rust using “generativity”; a type system approach to indices, pointers and ranges that are trusted to be in bounds.
We are developing our own “algebra” for transformations of in bounds ranges.
Apart from trusted single indices and pointers, there are intervals like
Range<'id, P>
(indices) and PRange<'id, T, P>
(pointers).
These particles use marker types to for example enable certain methods only for ranges that are known to be nonempty.
This is an experiment. The API is all of inconsistent, incomplete and redundant, but it explores interesting concepts.
Basic Parts
-
A scope is created using the
scope
function; inside this scope, there is aContainer
object that has two roles: (1) it gives out or vets trusted indices, pointers and ranges (2) it provides access to the underlying data through these indices and ranges. -
The container and its indices and ranges are “branded” with a lifetime parameter
'id
which is an identity marker. Branded items can't leave their scope, and they tie the items uniquely to a particular container. This makes it possible to trust them. -
Index<'id>
is a trusted index -
Range<'id, P>
is a trusted range. -
PIndex<'id, T>
andPRange<'id, T, P>
are equivalent toIndex
andRange
, but they use trusted raw pointers instead. -
For a range, if the proof parameter
P
isNonEmpty
, then the range is known to have at least one element. An observation: A non-empty range always has a valid front index, so it is interchangeable with the index representation. -
indices and pointers also use the same proof parameter. A
NonEmpty
index points to a valid element, while anUnknown
index is an edge index (it can be used to slice the container, but not to dereference to an element). -
All ranges have a
.first()
method to get the first index or pointer in the range, but it's only when the range is nonempty that the returned particle is alsoNonEmpty
and thus dereferenceable.
Borrowing Rules
- The indices, pointers and ranges are freely copyable and do not track mutability or exclusive access themselves. All access to the underlying data goes through the Container, for example by indexing the container with a trusted particle.
Example
Find the lower bound index for element elt
with a binary search using pointer ranges:
use scope;
// Find the lower bound for "2", which is the point exactly between the ones and the twos.
let data = ;
assert_eq!;