[−][src]Crate verified
This crate, in conjunction with the verify_macro
crate, aims to facilitate the development of
formally verifiable rust code.
Type level programming allows us to implement logic that can be verified by the compiler, which makes it possible to catch bugs at compile time, rather than at runtime.
Say we have an algorithm who's runtime scales exponentially. We would like to be able to restrict the number of elements in our working set to a reasonable number, let's say 128, in order to ensure that the algorithm completes in a reasonable amount of time, every time.
use verified::*; #[derive(Default)] struct Collection<E, Size: Unsigned> { elements: Vec<E>, size: Size, } #[verify] fn slow_routine<E, Size: Unsigned>(working_set: Collection<E, Size>) where // Restrict the size of the working set. _: Verify<{ Size < 128 }, { Size > 0 }> { // TODO } fn main() { // No problem here... slow_routine::<String, U1>(Default::default()); slow_routine::<String, U127>(Default::default()); // XXX: Does not compile because our working set is empty. slow_routine::<String, U0>(Default::default()); // XXX: Does not compile because our working set is one element too large. slow_routine::<String, U128>(Default::default()); }
For a more complete example, see the vec
module. Here is an abbreviated snippet:
use verified::*; use std::vec::Vec as Raw; pub struct Vec<Size: Unsigned, Element>(Size, Raw<Element>); #[verify] impl<Size: Unsigned, Element> Vec<Size, Element> { pub fn append<OtherSize: Unsigned>( self, other: Vec<OtherSize, Element>, ) -> Vec<{ Size + OtherSize }, Element> { self + other } pub fn pop(self) -> (Vec<{ Size - 1 }, Element>, Element) where _: Verify<{ Size > 0 }>, { self.into() } pub fn push(self, e: Element) -> Vec<{ Size + 1 }, Element> { (self, e).into() } } #[verify] impl<SizeL: Unsigned, SizeR: Unsigned, Element> std::ops::Add<Vec<SizeR, Element>> for Vec<SizeL, Element> { type Output = Vec<{ SizeL + SizeR }, Element>; fn add(self, Vec(os, mut ov): Vec<SizeR, Element>) -> Self::Output { let Self(s, mut v) = self; v.append(&mut ov); Vec(s + os, v) } } #[verify] impl<Size: Unsigned, Element> std::convert::From<(Vec<Size, Element>, Element)> for Vec<{ Size + 1 }, Element> { fn from((Vec(_, mut v), e): (Vec<Size, Element>, Element)) -> Self { v.push(e); Self(Default::default(), v) } } #[verify] impl<Size: Unsigned, Element> std::convert::From<Vec<Size, Element>> for (Vec<{ Size - 1 }, Element>, Element) where _: Verify<{ Size > 0 }>, { fn from(Vec(_, mut v): Vec<Size, Element>) -> Self { let e = v.pop().unwrap(); (Vec(Default::default(), v), e) } }
Modules
array | A type-level array of type-level numbers. |
bit | Type-level bits. |
consts | Type aliases for many constants. |
int | Type-level signed integers. |
marker_traits | All of the marker traits used in typenum. |
operator_aliases | Aliases for the type operators used in this crate.
Their purpose is to increase the ergonomics of performing operations on the types defined
here. For even more ergonomics, consider using the |
type_operators | Useful type operators that are not defined in |
uint | Type-level unsigned integers. |
vec |
Macros
assert_type | Asserts that a type is |
assert_type_eq | Asserts that two types are the same. |
cmp | Deprecated A convenience macro for comparing type numbers. Use |
op | Convenient type operations. |
tarr | Create a new type-level arrray. Only usable on Rust 1.13.0 or newer. |
vec |
Structs
ATerm | The terminating type for type arrays. |
B0 | The type-level bit 0. |
B1 | The type-level bit 1. |
Equal | A potential output from |
Greater | A potential output from |
Less | A potential output from |
NInt | Type-level signed integers with negative sign. |
PInt | Type-level signed integers with positive sign. |
TArr |
|
UInt |
|
UTerm | The terminating type for |
Z0 | The type-level signed integer 0. |
Traits
Abs | A type operator that returns the absolute value. |
Add | The addition operator |
Bit | The marker trait for compile time bits. |
BitAnd | The bitwise AND operator |
BitOr | The bitwise OR operator |
BitXor | The bitwise XOR operator |
Cmp | A type operator for comparing |
Div | The division operator |
Gcd | A type operator that computes the greatest common divisor of |
Integer | The marker trait for compile time signed integers. |
IsEqual | A type operator that returns |
IsGreater | A type operator that returns |
IsGreaterOrEqual | A type operator that returns |
IsLess | A type operator that returns |
IsLessOrEqual | A type operator that returns |
IsNotEqual | A type operator that returns |
Len | A type operator that gives the length of an |
Logarithm2 | A type operator for taking the integer binary logarithm of |
Max | A type operator that returns the maximum of |
Min | A type operator that returns the minimum of |
Mul | The multiplication operator |
NonZero | A marker trait to designate that a type is not zero. All number types in this
crate implement |
Not | The unary logical negation operator |
Ord | A Marker trait for the types |
PartialDiv | Division as a partial function. This type operator performs division just as |
Pow | A type operator that provides exponentiation by repeated squaring. |
PowerOfTwo | The marker trait for type-level numbers which are a power of two. |
Rem | The remainder operator |
Same | A type operator that ensures that |
Shl | The left shift operator |
Shr | The right shift operator |
SquareRoot | A type operator for taking the integer square root of |
Sub | The subtraction operator |
TypeArray | The marker trait for type-level arrays of type-level numbers. |
Unsigned | The marker trait for compile time unsigned integers. |
Type Definitions
Attribute Macros
verify |