hax_lib/
dummy.rs

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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
#[cfg(feature = "macros")]
pub use crate::proc_macros::*;

#[macro_export]
macro_rules! debug_assert {
    ($($arg:tt)*) => {
        ::core::debug_assert!($($arg)*);
    };
}

#[macro_export]
macro_rules! assert {
    ($($arg:tt)*) => {
        ::core::assert!($($arg)*);
    };
}

#[macro_export]
macro_rules! assume {
    ($formula:expr) => {
        ()
    };
}

pub fn forall<T>(_f: impl Fn(T) -> bool) -> bool {
    true
}

pub fn exists<T>(_f: impl Fn(T) -> bool) -> bool {
    true
}

pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool {
    !lhs || rhs()
}

#[doc(hidden)]
pub fn inline(_: &str) {}

#[doc(hidden)]
pub fn inline_unsafe<T>(_: &str) -> T {
    unreachable!()
}

#[doc(hidden)]
pub fn _internal_loop_invariant<T, P: FnOnce(T) -> bool>(_: P) {}

pub trait Refinement {
    type InnerType;
    fn new(x: Self::InnerType) -> Self;
    fn get(self) -> Self::InnerType;
    fn get_mut(&mut self) -> &mut Self::InnerType;
    fn invariant(value: Self::InnerType) -> bool;
}

pub trait RefineAs<RefinedType> {
    fn into_checked(self) -> RefinedType;
}

pub mod int {
    #[derive(Clone, Copy)]
    pub struct Int(pub u8);

    impl Int {
        pub fn new(x: impl Into<u8>) -> Self {
            Int(x.into())
        }
        pub fn get(self) -> u8 {
            self.0
        }
    }

    impl Int {}
    impl Int {}
    impl Int {}
    impl Int {}

    impl Int {
        pub fn pow2(self) -> Self {
            self
        }
        pub fn _unsafe_from_str(_s: &str) -> Self {
            Int(0)
        }
    }

    pub trait Abstraction {
        type AbstractType;
        fn lift(self) -> Self::AbstractType;
    }

    pub trait Concretization<T> {
        fn concretize(self) -> T;
    }

    impl Abstraction for u8 {
        type AbstractType = Int;
        fn lift(self) -> Self::AbstractType {
            Int(0)
        }
    }

    impl Concretization<u32> for Int {
        fn concretize(self) -> u32 {
            0
        }
    }
}