1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109

//! 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.
//!
//! ```compile_fail
//! 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)
//!     }
//! }
//! ```

pub mod vec;
pub use std::ops::{Add, BitAnd, BitOr, BitXor, Div, Mul, Not, Rem, Shl, Shr, Sub};
pub use typenum::*;
pub use verify_macro::verify;