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

creusot_std/logic/
real.rs
