mck 0.7.1

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89

use std::fmt::Debug;
use std::hash::Hash;

use serde::{Deserialize, Serialize};

pub trait MetaEq {
    fn meta_eq(&self, other: &Self) -> bool;
}

pub trait Meta<P: Clone>: Sized {
    fn proto_first(&self) -> P;
    fn proto_increment(&self, proto: &mut P) -> bool;

    fn into_proto_iter(self) -> ProtoIterator<Self, P> {
        ProtoIterator {
            meta: self,
            current_proto: None,
        }
    }
}

/// Wrapper structure allowing to use meta-equality as equality.
///
/// Types in meta wrap can be compared against each other.
/// Outside the meta-wrap, there is no danger of confusing
/// meta-equality with equality.
#[derive(Serialize, Deserialize)]
pub struct MetaWrap<E: MetaEq>(pub E);

impl<E: MetaEq> PartialEq for MetaWrap<E> {
    fn eq(&self, other: &Self) -> bool {
        self.0.meta_eq(&other.0)
    }
}
impl<E: MetaEq> Eq for MetaWrap<E> {}

impl<E: MetaEq + Debug> Debug for MetaWrap<E> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        // just debug the field
        self.0.fmt(f)
    }
}

impl<E: MetaEq + Clone> Clone for MetaWrap<E> {
    fn clone(&self) -> Self {
        Self(self.0.clone())
    }
}

impl<E: MetaEq + Copy> Copy for MetaWrap<E> {}

impl<E: MetaEq + Hash> Hash for MetaWrap<E> {
    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
        self.0.hash(state);
    }
}

pub struct ProtoIterator<M: Meta<P>, P: Clone> {
    meta: M,
    current_proto: Option<P>,
}

impl<M: Meta<P>, P: Clone> Iterator for ProtoIterator<M, P> {
    type Item = P;

    fn next(&mut self) -> Option<P> {
        let current = self.current_proto.take();
        self.current_proto = if let Some(mut current) = current {
            if self.meta.proto_increment(&mut current) {
                Some(current)
            } else {
                None
            }
        } else {
            Some(self.meta.proto_first())
        };
        self.current_proto.clone()
    }
}

pub trait MachineMisc {
    fn panic_message(panic_id: u32) -> &'static str;
    fn machine() -> &'static [u8];
}

// TODO: integrate Join, Phi, and apply_join
pub trait Join {
    fn join(self, other: &Self) -> Self;
}