Crate verified

Source
Expand description

§Verifiable Rust

A collection of crates 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 where the 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());
}

§#[verify]

The verified crate is built on top of the typenum crate, and provides syntactic sugar for defining type-level values via the #[verify] macro from the verify_macro crate. You can annotate almost any item with #[verify] (still a work in progress), and anywhere you would typically use a type like <A as Add<B>>::Output, you can now simply write { A + B }.

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)
    }
}

§Verify<…>

You may have noticed the strange where clauses that look like _: Verify<{ ... }, ...>. This Verify “trait” is processed by the #[verify] attribute. You can think of each argument as an expression that must evaluate to “true” in order to compile. This allows us to instrument our code with additional compile time checks for added safety.

§$ Compiling

The verified crate is built on top of the typenum crate. Naturally, the compiler errors can get pretty hairy. Here, I’ve accidentally typed 2 instead of 1 somewhere in the vec module. This is perhaps one of the less cryptic errors you may see…

$ cargo build

error[E0277]: cannot add `typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>` to `Size`
  --> verified/src/vec.rs:44:19
   |
44 |         (self, e).into()
   |                   ^^^^ no implementation for `Size + typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>`
   |
   = help: the trait `std::ops::Add<typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>>` is not implemented for `Size`
help: consider further restricting this bound with `+ std::ops::Add<typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>>`
  --> verified/src/vec.rs:28:12
   |
28 | impl<Size: Unsigned, Element> Vec<Size, Element> {
   |            ^^^^^^^^
   = note: required because of the requirements on the impl of `std::convert::From<(vec::Vec<Size, Element>, Element)>` for `vec::Vec<<Size as std::ops::Add<typenum::uint::UInt<typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>, typenum::bit::B0>>>::Output, Element>`
   = note: required because of the requirements on the impl of `std::convert::Into<vec::Vec<<Size as std::ops::Add<typenum::uint::UInt<typenum::uint::UInt<typenum::uint::UTerm, typenum::bit::B1>, typenum::bit::B0>>>::Output, Element>>` for `(vec::Vec<Size, Element>, Element)`

cargo-verify tries to help by translating types into simple arithmetic expressions where possible.

§$ cargo-verify

$ cargo verify build

error[E0277]: cannot add `1` to `Size`
  --> verified/src/vec.rs:44:19
   |
44 |         (self, e).into()
   |                   ^^^^ no implementation for `Size + 1`
   |
   = help: the trait `{ _ + 1 }` is not implemented for `Size`
help: consider further restricting this bound with `+ { _ + 1 }`
  --> verified/src/vec.rs:28:12
   |
28 | impl<Size: Unsigned, Element> Vec<Size, Element> {
   |            ^^^^^^^^
   = note: required because of the requirements on the impl of `std::convert::From<(vec::Vec<Size, Element>, Element)>` for `vec::Vec<{ Size + 2 }, Element>`
   = note: required because of the requirements on the impl of `std::convert::Into<vec::Vec<{ Size + 2 }, Element>>` for `(vec::Vec<Size, Element>, Element)`

§Install

$ cargo install cargo-verify

To upgrade:

$ cargo install --force cargo-verify

Or clone and build with $ cargo build then place the binary in your $PATH.

§Usage

$ cargo verify [COMMAND] [OPTIONS]...

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 op! macro instead.
  • type_operators
    Useful type operators that are not defined in core::ops.
  • uint
    Type-level unsigned integers.
  • vec

Macros§

  • assert_type
    Asserts that a type is True, aka B1.
  • assert_type_eq
    Asserts that two types are the same.
  • cmpDeprecated
    A convenience macro for comparing type numbers. Use op! instead.
  • op
    Convenient type operations.
  • tarr
    Create a new type-level array. 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 Cmp, this is the type equivalent to the enum variant core::cmp::Ordering::Equal.
  • Greater
    A potential output from Cmp, this is the type equivalent to the enum variant core::cmp::Ordering::Greater.
  • Less
    A potential output from Cmp, this is the type equivalent to the enum variant core::cmp::Ordering::Less.
  • NInt
    Type-level signed integers with negative sign.
  • PInt
    Type-level signed integers with positive sign.
  • TArr
    TArr is a type that acts as an array of types. It is defined similarly to UInt, only its values can be more than bits, and it is designed to act as an array. So you can only add two if they have the same number of elements, for example.
  • UInt
    UInt is defined recursively, where B is the least significant bit and U is the rest of the number. Conceptually, U should be bound by the trait Unsigned and B should be bound by the trait Bit, but enforcing these bounds causes linear instead of logrithmic scaling in some places, so they are left off for now. They may be enforced in future.
  • UTerm
    The terminating type for UInt; it always comes after the most significant bit. UTerm by itself represents zero, which is aliased to U0.
  • 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 Self and Rhs. It provides a similar functionality to the function core::cmp::Ord::cmp but for types.
  • Div
    The division operator /.
  • Gcd
    A type operator that computes the greatest common divisor of Self and Rhs.
  • Integer
    The marker trait for compile time signed integers.
  • IsEqual
    A type operator that returns True if Self == Rhs, otherwise returns False.
  • IsGreater
    A type operator that returns True if Self > Rhs, otherwise returns False.
  • IsGreaterOrEqual
    A type operator that returns True if Self >= Rhs, otherwise returns False.
  • IsLess
    A type operator that returns True if Self < Rhs, otherwise returns False.
  • IsLessOrEqual
    A type operator that returns True if Self <= Rhs, otherwise returns False.
  • IsNotEqual
    A type operator that returns True if Self != Rhs, otherwise returns False.
  • Len
    A type operator that gives the length of an Array or the number of bits in a UInt.
  • Logarithm2
    A type operator for taking the integer binary logarithm of Self.
  • Max
    A type operator that returns the maximum of Self and Rhs.
  • Min
    A type operator that returns the minimum of Self and Rhs.
  • Mul
    The multiplication operator *.
  • NonZero
    A marker trait to designate that a type is not zero. All number types in this crate implement NonZero except B0, U0, and Z0.
  • Not
    The unary logical negation operator !.
  • Ord
    A Marker trait for the types Greater, Equal, and Less.
  • PartialDiv
    Division as a partial function. This type operator performs division just as Div, but is only defined when the result is an integer (i.e. there is no remainder).
  • 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 Rhs is the same as Self, it is mainly useful for writing macros that can take arbitrary binary or unary operators.
  • Shl
    The left shift operator <<. Note that because this trait is implemented for all integer types with multiple right-hand-side types, Rust’s type checker has special handling for _ << _, setting the result type for integer operations to the type of the left-hand-side operand. This means that though a << b and a.shl(b) are one and the same from an evaluation standpoint, they are different when it comes to type inference.
  • Shr
    The right shift operator >>. Note that because this trait is implemented for all integer types with multiple right-hand-side types, Rust’s type checker has special handling for _ >> _, setting the result type for integer operations to the type of the left-hand-side operand. This means that though a >> b and a.shr(b) are one and the same from an evaluation standpoint, they are different when it comes to type inference.
  • SquareRoot
    A type operator for taking the integer square root of Self.
  • Sub
    The subtraction operator -.
  • ToInt
    A type operator for taking a concrete integer value from a type.
  • TypeArray
    The marker trait for type-level arrays of type-level numbers.
  • Unsigned
    The marker trait for compile time unsigned integers.
  • Zero
    A marker trait to designate that a type is zero. Only B0, U0, and Z0 implement this trait.

Type Aliases§

Attribute Macros§