invariant_reference/
lib.rs

1use std::fmt::Debug;
2
3pub trait Invariant {
4    const MESSAGE: &str;
5}
6
7#[diagnostic::on_unimplemented(
8    message = "The invariant {Self} is not proven",
9    note = "use `invariant_established!({Self}[{N}])` macro where the invariant is established."
10)]
11pub trait InvariantProof<const N: usize> {}
12
13#[macro_export]
14macro_rules! invariant_established {
15    ($name:path [$n:literal], why = $lit:literal) => {
16        #[allow(non_local_definitions)]
17        impl $crate::InvariantProof<$n> for $name {}
18    };
19    ($name:path, why = $lit:literal) => {
20        #[allow(non_local_definitions)]
21        impl $crate::InvariantProof<0> for $name {}
22    };
23}
24
25pub trait OptionExt<T> {
26    fn unwrap_under_invariant<I: Invariant>(self) -> T;
27}
28
29impl<T> OptionExt<T> for Option<T> {
30    fn unwrap_under_invariant<I: Invariant>(self) -> T {
31        self.unwrap_or_else(|| {
32            panic!(
33                "unwrapping called on None value; violation of invariant: {}",
34                I::MESSAGE
35            )
36        })
37    }
38}
39
40pub trait ResultExt<T, E> {
41    fn unwrap_under_invariant<I: Invariant>(self) -> T;
42}
43
44impl<T, E> ResultExt<T, E> for Result<T, E>
45where
46    E: Debug,
47{
48    fn unwrap_under_invariant<I: Invariant>(self) -> T {
49        self.unwrap_or_else(|error| {
50            panic!(
51                "unwrapping called on Err value: {error:?}; violation of invariant: {}",
52                I::MESSAGE
53            )
54        })
55    }
56}
invariant_reference/lib.rs

invariant_reference/
lib.rs
