可验证 Rust

已验证 crate 的源代码

lib.rs:

可验证 Rust

一组 crate，旨在促进形式化可验证 Rust 代码的开发。

类型级别编程允许我们实现编译器可以验证的逻辑，这使得在编译时而不是在运行时捕捉到错误成为可能。

假设我们有一个算法，其运行时间呈指数级增长。我们希望将工作集中元素的数量限制在合理的范围内，比如 128，以确保算法每次都能在合理的时间内完成。

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]

“已验证”crate 是建立在“typenum”crate 的基础上，并为“verify_macro”crate 中的“#[verify]”宏提供了语法糖来定义类型级别值。您可以用“#[verify]”（仍在开发中）来注释几乎任何项，并且您可以在通常使用类型如“<A as Add<B>>::Output的地方简单地写出“{ A + B }。”

更多完整的示例，请参阅“vec”模块。以下是一个简化的片段

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<...>

您可能已经注意到了那些看起来像这样 _: Verify<{ ... }, ...> 的奇怪 WHERE 子句。这个 Verify "特性行为" 由 #[verify] 属性处理。您可以认为每个参数都是一个表达式，必须评估为 "true" 才能编译。这允许我们在代码中添加额外的编译时检查以提高安全性。

$ 编译

基于 typenum crate，verified crate 被构建。自然，编译器错误可能会变得相当复杂。在这里，我不小心在 vec 模块中某处将 2 键入为 1。这可能是您可能看到的不太神秘的错误之一...

$ 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 尝试通过在可能的情况下将类型转换为简单的算术表达式来帮助。

$ 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)`

安装

$ cargo install cargo-verify

升级

$ cargo install --force cargo-verify

或使用 $ cargo build 克隆并构建，然后将二进制文件放置在您的 $PATH 中。

用法

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