kamiyo_kani/
lib.rs

1//! Reusable Kani formal verification harnesses for Solana program math.
2//!
3//! This crate is intentionally a no-op in normal builds. Everything is gated
4//! behind `cfg(kani)`.
5
6#[cfg(kani)]
7pub mod generators;
8
9#[cfg(kani)]
10pub mod token;
11
12#[cfg(kani)]
13pub mod staking;
14
15#[cfg(kani)]
16pub mod bounds;
17
18#[cfg(kani)]
19pub mod math;
20
21#[cfg(kani)]
22pub mod risk;
23
24#[cfg(all(kani, feature = "solana-agent"))]
25pub mod agent;
26
27#[cfg(all(kani, feature = "solana-account-info"))]
28pub mod account_info;
29
30#[cfg(test)]
31fn coverage_probe(value: u8) -> u8 {
32    value.saturating_add(1)
33}
34
35#[cfg(test)]
36mod tests {
37    use super::coverage_probe;
38
39    #[test]
40    fn coverage_probe_saturates() {
41        assert_eq!(coverage_probe(0), 1);
42        assert_eq!(coverage_probe(u8::MAX), u8::MAX);
43    }
44}