1 个不稳定版本
| 0.2.3 | 2020年6月17日 |
|---|
#2056 在 Rust模式
53KB
1.5K SLoC
可验证Rust
一套crate集合，用于简化形式化可验证Rust代码的开发。
类型级别编程允许我们实现编译器可以验证的逻辑，这使得我们能够在编译时而不是在运行时捕获错误。
假设我们有一个算法，其运行时间呈指数增长。我们希望能够
将工作集的元素数量限制在一个合理的数量，比如128，以确保算法每次都能在合理的时间内完成。
#[verify]
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());
}
The verified crate 是基于 typenum crate 构建的，并提供了一种通过 #[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<...>
你可能已经注意到了那些看起来很奇怪的where子句，例如：_: Verify<{ ... }, ...>。这个Verify "特性"由#[verify]属性处理。你可以将每个参数视为一个表达式，必须评估为"true"才能编译。这使我们能够通过额外的编译时检查来提高代码的安全性。
$ cargo-verify
verified包建立在typenum包之上。当然，编译器错误可能会变得相当复杂。这里，我无意中在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 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]...
依赖关系
~4–5.5MB
~107K SLoC