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

use std::fmt::Debug;

use crate::{
    bitvector::{BitvectorBound, CBound},
    concr::{CConcreteBitvector, UnsignedBitvector},
    forward::ReadWrite,
    misc::LightIndex,
};

use super::light::LightArray;

#[derive(Clone, Hash, PartialEq, Eq)]
pub struct Array<const I: u32, const E: u32> {
    pub(super) inner: LightArray<UnsignedBitvector<CBound<I>>, CConcreteBitvector<E>>,
}

impl<const I: u32, const E: u32> Array<I, E> {
    pub fn new_filled(element: CConcreteBitvector<E>) -> Self {
        Self {
            inner: LightArray::new_filled(CBound, element),
        }
    }

    pub fn from_inner(
        inner: LightArray<UnsignedBitvector<CBound<I>>, CConcreteBitvector<E>>,
    ) -> Self {
        Self { inner }
    }
}

impl<const I: u32, const W: u32> ReadWrite for &Array<I, W> {
    type Index = CConcreteBitvector<I>;
    type Element = CConcreteBitvector<W>;
    type Deref = Array<I, W>;

    fn read(self, index: Self::Index) -> Self::Element {
        self.inner[index.as_unsigned()]
    }

    fn write(self, index: Self::Index, element: Self::Element) -> Self::Deref {
        let mut result = self.clone();
        result.inner.write(index.as_unsigned(), element);
        result
    }
}
impl<const I: u32, const W: u32> Debug for Array<I, W> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        self.inner.fmt(f)
    }
}

impl<I: BitvectorBound> LightIndex for UnsignedBitvector<I> {
    type Bound = I;

    fn bound(&self) -> Self::Bound {
        self.bound()
    }

    fn to_u64(self) -> u64 {
        self.to_u64()
    }

    fn zero(bound: Self::Bound) -> Self {
        Self::zero(bound)
    }

    fn one(bound: Self::Bound) -> Self {
        Self::one(bound)
    }
}