machine-check-machine 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

use std::collections::BTreeSet;

use crate::wir::{WIdent, WItemFn, YConverted, YStage};

#[derive(Clone, Debug, Hash)]
pub struct WProperty<Y: YStage> {
    pub subproperties: Vec<WSubproperty<Y>>,
}

#[derive(Clone, Debug, Hash)]
pub enum WSubproperty<Y: YStage> {
    Func(WSubpropertyFunc<Y>),
    FixedPoint(WSubpropertyFixedPoint),
    Next(WSubpropertyNext),
}

#[derive(Clone, Debug, Hash)]
pub struct WSubpropertyFunc<Y: YStage> {
    pub parent: Option<usize>,
    pub func: WItemFn<Y>,
    pub children: Vec<usize>,
    pub display: Option<String>,
}

#[derive(Clone, Debug, Hash)]
pub struct WSubpropertyFixedPoint {
    pub parent: Option<usize>,
    pub greatest: bool,
    pub variable: WIdent,
    pub inner: usize,
    pub display: Option<String>,
}

#[derive(Clone, Debug, Hash)]
pub struct WSubpropertyNext {
    pub parent: Option<usize>,
    pub universal: bool,
    pub inner: usize,
    pub display: Option<String>,
}

impl<Y: YStage> WSubproperty<Y> {
    pub fn children(&self) -> &[usize] {
        match self {
            WSubproperty::Func(subprop) => &subprop.children,
            WSubproperty::FixedPoint(fixed_point) => std::slice::from_ref(&fixed_point.inner),
            WSubproperty::Next(next) => std::slice::from_ref(&next.inner),
        }
    }
}

impl WSubproperty<YConverted> {
    pub fn dependencies(&self) -> BTreeSet<usize> {
        match self {
            WSubproperty::Func(subprop) => {
                let mut dependencies = BTreeSet::new();
                for input_arg in &subprop.func.signature.inputs {
                    let input_var_name = input_arg.ident.name();
                    if let Some(stripped) = input_var_name.strip_prefix("__mck_subproperty_") {
                        let Ok(input_subproperty_index) = stripped.parse::<usize>() else {
                            panic!("Input subproperty should have valid index");
                        };
                        dependencies.insert(input_subproperty_index);
                    }
                }
                dependencies
            }
            WSubproperty::FixedPoint(fixed_point) => BTreeSet::from([fixed_point.inner]),
            WSubproperty::Next(next) => BTreeSet::from([next.inner]),
        }
    }
}

pub trait IntoSyn<T> {
    fn into_syn(self) -> T;
}