hax-lib 0.3.6

Hax-specific helpers for Rust programs
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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146

use crate::abstraction::*;
use core::ops::*;

/// Represent a logical proposition, that may be not computable.
#[derive(Clone, Copy, Debug)]
pub struct Prop(bool);

/// This module provides monomorphic constructors for `Prop`.
/// Hax rewrite more elaborated versions (see `forall` or `AndBit` below) to those monomorphic constructors.
pub mod constructors {
    use super::Prop;
    pub const fn from_bool(b: bool) -> Prop {
        Prop(b)
    }
    pub fn and(lhs: Prop, other: Prop) -> Prop {
        Prop(lhs.0 && other.0)
    }
    pub fn or(lhs: Prop, other: Prop) -> Prop {
        Prop(lhs.0 || other.0)
    }
    pub fn not(lhs: Prop) -> Prop {
        Prop(!lhs.0)
    }

    /// Logical equality between two value of *any* type
    pub fn eq<T>(_lhs: T, _rhs: T) -> Prop {
        Prop(true)
    }

    pub fn ne<T>(_lhs: T, _rhs: T) -> Prop {
        Prop(true)
    }

    pub fn implies(lhs: Prop, other: Prop) -> Prop {
        Prop(lhs.0 || !other.0)
    }

    pub fn forall<A, F: Fn(A) -> Prop>(_pred: F) -> Prop {
        Prop(true)
    }

    pub fn exists<A, F: Fn(A) -> Prop>(_pred: F) -> Prop {
        Prop(true)
    }
}

impl Prop {
    /// Lifts a boolean to a logical proposition.
    pub const fn from_bool(b: bool) -> Self {
        constructors::from_bool(b)
    }
    /// Conjuction of two propositions.
    pub fn and(self, other: impl Into<Self>) -> Self {
        constructors::and(self, other.into())
    }
    /// Disjunction of two propositions.
    pub fn or(self, other: impl Into<Self>) -> Self {
        constructors::or(self, other.into())
    }
    /// Negation of a proposition.
    pub fn not(self) -> Self {
        constructors::not(self)
    }
    /// Equality between two propositions.
    pub fn eq(self, other: impl Into<Self>) -> Self {
        constructors::eq(self, other.into())
    }
    /// Equality between two propositions.
    pub fn ne(self, other: impl Into<Self>) -> Self {
        constructors::ne(self, other.into())
    }
    /// Logical implication.
    pub fn implies(self, other: impl Into<Self>) -> Self {
        constructors::implies(self, other.into())
    }
}

impl Abstraction for bool {
    type AbstractType = Prop;
    fn lift(self) -> Self::AbstractType {
        Prop(self)
    }
}

pub trait ToProp {
    fn to_prop(self) -> Prop;
}
impl ToProp for bool {
    fn to_prop(self) -> Prop {
        self.lift()
    }
}

impl From<bool> for Prop {
    fn from(value: bool) -> Self {
        Prop(value)
    }
}

impl<T: Into<Prop>> BitAnd<T> for Prop {
    type Output = Prop;
    fn bitand(self, rhs: T) -> Self::Output {
        Prop(self.0 & rhs.into().0)
    }
}

impl<T: Into<Prop>> BitOr<T> for Prop {
    type Output = Prop;
    fn bitor(self, rhs: T) -> Self::Output {
        Prop(self.0 | rhs.into().0)
    }
}

impl Not for Prop {
    type Output = Prop;
    fn not(self) -> Self::Output {
        Prop(!self.0)
    }
}

/// The universal quantifier. This should be used only for Hax code: in
/// Rust, this is always true.
///
/// # Example:
///
/// The Rust expression `forall(|x: T| phi(x))` corresponds to `∀ (x: T), phi(x)`.
pub fn forall<T, U: Into<Prop>>(f: impl Fn(T) -> U) -> Prop {
    constructors::forall(|x| f(x).into())
}

/// The existential quantifier. This should be used only for Hax code: in
/// Rust, this is always true.
///
/// # Example:
///
/// The Rust expression `exists(|x: T| phi(x))` corresponds to `∃ (x: T), phi(x)`.
pub fn exists<T, U: Into<Prop>>(f: impl Fn(T) -> U) -> Prop {
    constructors::exists(|x| f(x).into())
}

/// The logical implication `a ==> b`.
pub fn implies(lhs: impl Into<Prop>, rhs: impl Into<Prop>) -> Prop {
    constructors::implies(lhs.into(), rhs.into())
}

pub use constructors::eq;