improv_verified/lib.rs
1//! Small, pure integer kernels of the Improv engine, with Verus specifications
2//! and machine-checked proofs.
3//!
4//! Each kernel lives in a `verus! { ... }` block: a `spec fn` says what it
5//! means, the executable function `ensures` it, and `cargo-verus verify -p
6//! improv_verified` (see `scripts/verify.sh`) checks the proof. Under plain
7//! cargo the specs and proofs are erased and the functions are ordinary Rust,
8//! which is what the engine calls: the proven code is the code that runs.
9//!
10//! Floating-point arithmetic is out of scope (Verus does not reason about
11//! `f64`), so every kernel takes and returns integers; the engine does the
12//! float range checks and truncation before calling in.
13
14#![cfg_attr(coverage_nightly, feature(coverage_attribute))]
15// The attribute is only used inside #[cfg(test)] modules, so non-test
16// coverage builds would otherwise warn that the feature is unused.
17#![cfg_attr(coverage_nightly, allow(unused_features))]
18
19pub mod bits;
20pub mod gcd;
21pub mod graph;
22pub mod keys;
23pub mod radix;
24pub mod take;