creusot_std/logic/
real.rs

1//! Real numbers
2use crate::{
3    invariant::{InhabitedInvariant, Subset},
4    logic::ops::{AddLogic, DivLogic, MulLogic, NegLogic, SubLogic},
5    prelude::*,
6};
7#[cfg(all(creusot, feature = "num-rational"))]
8use num_rational::BigRational;
9
10#[builtin("real.Real.real")]
11pub struct Real;
12
13#[cfg(all(creusot, feature = "num-rational"))]
14impl DeepModel for BigRational {
15    type DeepModelTy = Real;
16
17    #[logic(opaque)]
18    fn deep_model(self) -> Self::DeepModelTy {
19        dead
20    }
21}
22
23impl Real {
24    #[logic]
25    #[builtin("real.FromInt.from_int")]
26    pub fn from_int(_: Int) -> Self {
27        dead
28    }
29}
30
31impl PartialOrdLogic for Real {
32    #[logic]
33    #[builtin("real.Real.(<)")]
34    fn lt_log(self, _: Self) -> bool {
35        dead
36    }
37
38    #[logic]
39    #[builtin("real.Real.(<=)")]
40    fn le_log(self, _: Self) -> bool {
41        dead
42    }
43
44    #[logic]
45    #[ensures(!(self < self))]
46    fn irreflexive(self) {}
47
48    #[logic]
49    #[requires(x < y)]
50    #[requires(y < z)]
51    #[ensures(x < z)]
52    fn transitive(x: Self, y: Self, z: Self) {}
53
54    #[logic]
55    #[ensures((self <= other) == (self < other || self == other))]
56    fn le_lt_log(self, other: Self) {}
57}
58
59impl OrdLogic for Real {
60    #[logic]
61    #[ensures(self < other || self == other || other < self)]
62    fn lt_log_total(self, other: Self) {}
63}
64
65impl AddLogic for Real {
66    type Output = Self;
67    #[logic]
68    #[builtin("real.Real.(+)")]
69    #[allow(unused_variables)]
70    fn add_logic(self, other: Self) -> Self {
71        dead
72    }
73}
74
75impl SubLogic for Real {
76    type Output = Self;
77    #[logic]
78    #[builtin("real.Real.(-)")]
79    #[allow(unused_variables)]
80    fn sub_logic(self, other: Self) -> Self {
81        dead
82    }
83}
84
85impl MulLogic for Real {
86    type Output = Self;
87    #[logic]
88    #[builtin("real.Real.(*)")]
89    #[allow(unused_variables)]
90    fn mul_logic(self, other: Self) -> Self {
91        dead
92    }
93}
94
95impl DivLogic for Real {
96    type Output = Self;
97    #[logic]
98    #[builtin("real.Real.(/)")]
99    #[allow(unused_variables)]
100    fn div_logic(self, other: Self) -> Self {
101        dead
102    }
103}
104
105impl NegLogic for Real {
106    type Output = Self;
107    #[logic]
108    #[builtin("real.Real.(-_)")]
109    fn neg_logic(self) -> Self {
110        dead
111    }
112}
113
114struct PositiveRealInner(Real);
115
116impl Invariant for PositiveRealInner {
117    #[logic]
118    fn invariant(self) -> bool {
119        self.0 > Real::from_int(0)
120    }
121}
122
123impl InhabitedInvariant for PositiveRealInner {
124    #[logic]
125    #[ensures(result.invariant())]
126    fn inhabits() -> Self {
127        Self(Real::from_int(1))
128    }
129}
130
131/// Natural numbers, i.e., integers that are greater or equal to 0.
132pub struct PositiveReal(Subset<PositiveRealInner>);
133
134impl PositiveReal {
135    #[logic]
136    #[ensures(result > Real::from_int(0))]
137    pub fn to_real(self) -> Real {
138        pearlite! { self.0.inner().0 }
139    }
140
141    #[logic]
142    #[requires(n > Real::from_int(0))]
143    #[ensures(result.to_real() == n)]
144    pub fn new(n: Real) -> PositiveReal {
145        PositiveReal(Subset::new_logic(PositiveRealInner(n)))
146    }
147
148    #[logic(open)]
149    #[ensures(#[trigger(self == other)] result == (self == other))]
150    pub fn ext_eq(self, other: Self) -> bool {
151        let _ = Subset::<PositiveRealInner>::inner_inj;
152        self.to_real() == other.to_real()
153    }
154
155    #[logic(open, inline)]
156    pub fn from_int(i: Int) -> Self {
157        Self::new(Real::from_int(i))
158    }
159}
160
161impl PartialOrdLogic for PositiveReal {
162    #[logic(open)]
163    fn le_log(self, o: Self) -> bool {
164        self.to_real() <= o.to_real()
165    }
166
167    #[logic(open)]
168    fn lt_log(self, o: Self) -> bool {
169        self.to_real() < o.to_real()
170    }
171
172    #[logic]
173    #[ensures(!(self < self))]
174    fn irreflexive(self) {}
175
176    #[logic]
177    #[requires(x < y)]
178    #[requires(y < z)]
179    #[ensures(x < z)]
180    fn transitive(x: Self, y: Self, z: Self) {}
181
182    #[logic(law)]
183    #[ensures((self <= other) == (self < other || self == other))]
184    fn le_lt_log(self, other: Self) {
185        let _ = PositiveReal::ext_eq;
186    }
187}
188
189impl OrdLogic for PositiveReal {
190    #[logic(law)]
191    #[ensures(self < other || self == other || other < self)]
192    fn lt_log_total(self, other: Self) {
193        let _ = PositiveReal::ext_eq;
194    }
195}
196
197impl AddLogic for PositiveReal {
198    type Output = Self;
199    #[logic]
200    #[ensures(result.to_real() == self.to_real() + other.to_real())]
201    fn add_logic(self, other: Self) -> Self {
202        Self::new(self.to_real() + other.to_real())
203    }
204}
205
206impl MulLogic for PositiveReal {
207    type Output = Self;
208    #[logic]
209    #[ensures(result.to_real() == self.to_real() * other.to_real())]
210    fn mul_logic(self, other: Self) -> Self {
211        Self::new(self.to_real() * other.to_real())
212    }
213}
214
215impl DivLogic for PositiveReal {
216    type Output = Self;
217    #[logic]
218    #[ensures(result.to_real() == self.to_real() / other.to_real())]
219    fn div_logic(self, other: Self) -> Self {
220        Self::new(self.to_real() / other.to_real())
221    }
222}
creusot_std/logic/real.rs

creusot_std/logic/
real.rs
