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: Usize> {
    elements: Vec<E>,
    size: Size,
}

#[verify]
fn really_really_really_slow_routine<E, Size: Usize>(working_set: Collection<E, Size>)
where
    // Restrict the size of the working set.
    _: Verify<{ Size < 128 }>
{
    todo! {}
}

type U128 = U<U<U<U<U<U<U<U<T, B1>, B0>, B0>, B0>, B0>, B0>, B0>, B0>;
type U127 = U<U<U<U<U<U<U<T, B0>, B1>, B1>, B1>, B1>, B1>, B1>;

fn main() {
    // No problem here...
    really_really_really_slow_routine::<String, U127>(Default::default());

    // XXX: Does not compile because our working set is one element too large.
    really_really_really_slow_routine::<String, U128>(Default::default());
}

Re-exports

pub use crate::bool::Bool;

pub use crate::bool::False;

pub use crate::bool::True;

pub use crate::ops::And;

pub use crate::ops::Compare;

pub use crate::ops::Equal;

pub use crate::ops::Ge;

pub use crate::ops::Greater;

pub use crate::ops::Gt;

pub use crate::ops::Le;

pub use crate::ops::Less;

pub use crate::ops::Lt;

pub use crate::ops::Ne;

pub use crate::ops::Or;

pub use crate::ops::Ordering;

pub use crate::ops::Same;

pub use crate::usize::Usize;

pub use crate::usize::B0;

pub use crate::usize::B1;

pub use crate::usize::T;

pub use crate::usize::U;

Modules

bool	Types and traits for representing booleans as types.
ops	Types and traits for representing binary and unary operations as types.
usize	Types and traits for representing unsigned integers as types.

Macros

impl_bool_ops

Traits

Add	The addition operator +.
BitAnd	The bitwise AND operator &.
BitOr	The bitwise OR operator |.
BitXor	The bitwise XOR operator ^.
Not	The unary logical negation operator !.

Attribute Macros

verify